| Name | mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-protfold.opb |
| MD5SUM | c5ca7819a7dcae16ff6045242cdd1f87 |
| Bench Category | optimization, small integers (OPTSMALLINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | -21 |
| Optimality of the best value was proved | NO |
| Number of terms in the objective function | 120 |
| Biggest coefficient in the objective function | 1 |
| Number of bits for the biggest coefficient in the objective function | 1 |
| Sum of the numbers in the objective function | 120 |
| Number of bits of the sum of numbers in the objective function | 7 |
| Biggest number in a constraint | 18 |
| Number of bits of the biggest number in a constraint | 5 |
| Biggest sum of numbers in a constraint | 900 |
| Number of bits of the biggest sum of numbers | 10 |
| Best result obtained on this benchmark | SAT |
| Best CPU time to get the best result obtained on this benchmark | 1195.11 |
| Number of variables | 1835 |
| Total number of constraints | 3947 |
| Number of constraints which are clauses | 1906 |
| Number of constraints which are cardinality constraints (but not clauses) | 1921 |
| Number of constraints which are nor clauses,nor cardinality constraints | 120 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 882 |
LAUNCH ON wulflinc17 THE 2005-09-19 03:51:30 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2937 boxname=wulflinc17 idbench=593 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: c5ca7819a7dcae16ff6045242cdd1f87 /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-protfold.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-protfold.opb IDLAUNCH: 2937 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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: 904228 kB Buffers: 34808 kB Cached: 68444 kB SwapCached: 516 kB Active: 57456 kB Inactive: 48220 kB HighTotal: 131008 kB HighFree: 60060 kB LowTotal: 903652 kB LowFree: 844168 kB SwapTotal: 2097892 kB SwapFree: 2096672 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5680 kB Slab: 19136 kB Committed_AS: 64184 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 04:11:42 (client local time) WITH STATUS 10 IN 1208.85 SECONDS stats: 2937 7 1208.85 10
c Parsing PB file... c Converting 2149 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ##################################### c -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................. c ---[1908]---> BDD-cost: 98 c ---[1907]---> BDD-cost: 98 c ---[1906]---> BDD-cost: 98 c ---[1905]---> BDD-cost: 98 c ---[1904]---> BDD-cost: 98 c ---[1903]---> BDD-cost: 98 c ---[1902]---> BDD-cost: 98 c ---[1901]---> BDD-cost: 98 c ---[1900]---> BDD-cost: 98 c ---[1899]---> BDD-cost: 98 c ---[1898]---> BDD-cost: 98 c ---[1897]---> BDD-cost: 98 c ---[1896]---> BDD-cost: 98 c ---[1895]---> BDD-cost: 98 c ---[1894]---> BDD-cost: 98 c ---[1893]---> BDD-cost: 98 c ---[1892]---> BDD-cost: 98 c ---[1891]---> BDD-cost: 98 c ---[1890]---> BDD-cost: 98 c ---[1889]---> BDD-cost: 98 c ---[1888]---> BDD-cost: 98 c ---[1887]---> BDD-cost: 98 c ---[1886]---> BDD-cost: 98 c ---[1885]---> BDD-cost: 98 c ---[1884]---> BDD-cost: 98 c ---[1883]---> BDD-cost: 98 c ---[1882]---> BDD-cost: 98 c ---[1881]---> BDD-cost: 98 c ---[1880]---> BDD-cost: 98 c ---[1879]---> BDD-cost: 98 c ---[1878]---> BDD-cost: 98 c ---[1877]---> BDD-cost: 98 c ---[1876]---> BDD-cost: 98 c ---[1875]---> BDD-cost: 98 c ---[1874]---> BDD-cost: 98 c ---[1873]---> BDD-cost: 98 c ---[1872]---> BDD-cost: 98 c ---[1871]---> BDD-cost: 98 c ---[1870]---> BDD-cost: 98 c ---[1869]---> BDD-cost: 98 c ---[1868]---> BDD-cost: 98 c ---[1867]---> BDD-cost: 98 c ---[1866]---> BDD-cost: 98 c ---[1865]---> BDD-cost: 98 c ---[1864]---> BDD-cost: 98 c ---[1863]---> BDD-cost: 98 c ---[1862]---> BDD-cost: 98 c ---[1861]---> BDD-cost: 98 c ---[1860]---> BDD-cost: 98 c ---[1859]---> BDD-cost: 98 c ---[1858]---> BDD-cost: 98 c ---[1857]---> BDD-cost: 98 c ---[1856]---> BDD-cost: 98 c ---[1855]---> BDD-cost: 98 c ---[1854]---> BDD-cost: 98 c ---[1853]---> BDD-cost: 98 c ---[1852]---> BDD-cost: 98 c ---[1851]---> BDD-cost: 98 c ---[1850]---> BDD-cost: 98 c ---[1849]---> BDD-cost: 98 c ---[1848]---> BDD-cost: 98 c ---[1847]---> BDD-cost: 98 c ---[1846]---> BDD-cost: 98 c ---[1845]---> BDD-cost: 98 c ---[1844]---> BDD-cost: 98 c ---[1843]---> BDD-cost: 98 c ---[1842]---> BDD-cost: 98 c ---[1841]---> BDD-cost: 98 c ---[1840]---> BDD-cost: 98 c ---[1839]---> BDD-cost: 98 c ---[1838]---> BDD-cost: 98 c ---[1837]---> BDD-cost: 98 c ---[1836]---> BDD-cost: 98 c ---[1835]---> BDD-cost: 98 c ---[1834]---> BDD-cost: 98 c ---[1833]---> BDD-cost: 98 c ---[1832]---> BDD-cost: 98 c ---[1831]---> BDD-cost: 98 c ---[1830]---> BDD-cost: 98 c ---[1829]---> BDD-cost: 98 c ---[1828]---> BDD-cost: 98 c ---[1827]---> BDD-cost: 98 c ---[1826]---> BDD-cost: 98 c ---[1825]---> BDD-cost: 98 c ---[1824]---> BDD-cost: 98 c ---[1823]---> BDD-cost: 98 c ---[1822]---> BDD-cost: 98 c ---[1821]---> BDD-cost: 98 c ---[1820]---> BDD-cost: 98 c ---[1819]---> BDD-cost: 98 c ---[1818]---> BDD-cost: 98 c ---[1817]---> BDD-cost: 98 c ---[1816]---> BDD-cost: 98 c ---[1815]---> BDD-cost: 98 c ---[1814]---> BDD-cost: 98 c ---[1813]---> BDD-cost: 98 c ---[1812]---> BDD-cost: 98 c ---[1811]---> BDD-cost: 98 c ---[1810]---> BDD-cost: 98 c ---[1809]---> BDD-cost: 98 c ---[1808]---> BDD-cost: 98 c ---[1807]---> BDD-cost: 98 c ---[1806]---> BDD-cost: 98 c ---[1805]---> BDD-cost: 98 c ---[1804]---> BDD-cost: 98 c ---[1803]---> BDD-cost: 98 c ---[1802]---> BDD-cost: 98 c ---[1801]---> BDD-cost: 98 c ---[1800]---> BDD-cost: 98 c ---[1799]---> BDD-cost: 98 c ---[1798]---> BDD-cost: 98 c ---[1797]---> BDD-cost: 98 c ---[1796]---> BDD-cost: 98 c ---[1795]---> BDD-cost: 98 c ---[1794]---> BDD-cost: 98 c ---[1793]---> BDD-cost: 98 c ---[1792]---> BDD-cost: 98 c ---[1791]---> BDD-cost: 98 c ---[1790]---> BDD-cost: 98 c ---[1789]---> BDD-cost: 98 c ---[1787]---> Adder-cost: 1658 maxlim: 816 bits: 10/10 c ---[1785]---> Adder-cost: 1752 maxlim: 864 bits: 10/10 c ---[1783]---> BDD-cost: 95 c ---[1781]---> BDD-cost: 95 c ---[1779]---> BDD-cost: 95 c ---[1777]---> BDD-cost: 95 c ---[1775]---> BDD-cost: 95 c ---[1773]---> BDD-cost: 95 c ---[1771]---> BDD-cost: 95 c ---[1769]---> BDD-cost: 95 c ---[1767]---> BDD-cost: 95 c ---[1765]---> BDD-cost: 95 c ---[1763]---> BDD-cost: 95 c ---[1761]---> BDD-cost: 95 c ---[1759]---> BDD-cost: 95 c ---[1757]---> BDD-cost: 95 c ---[1755]---> BDD-cost: 95 c ---[1753]---> BDD-cost: 95 c ---[1751]---> BDD-cost: 95 c ---[1749]---> BDD-cost: 95 c ---[1747]---> BDD-cost: 95 c ---[1745]---> BDD-cost: 95 c ---[1743]---> BDD-cost: 95 c ---[1741]---> BDD-cost: 95 c ---[1739]---> BDD-cost: 95 c ---[1737]---> BDD-cost: 95 c ---[1735]---> BDD-cost: 95 c ---[1733]---> BDD-cost: 95 c ---[1731]---> BDD-cost: 95 c ---[1729]---> BDD-cost: 95 c ---[1727]---> BDD-cost: 95 c ---[1725]---> BDD-cost: 95 c ---[1723]---> BDD-cost: 95 c ---[1721]---> BDD-cost: 95 c ---[1719]---> BDD-cost: 95 c ---[1717]---> BDD-cost: 95 c ---[1715]---> BDD-cost: 95 c ---[1714]---> BDD-cost: 67 c ---[1713]---> BDD-cost: 67 c ---[1712]---> BDD-cost: 67 c ---[1711]---> BDD-cost: 67 c ---[1710]---> BDD-cost: 67 c ---[1709]---> BDD-cost: 67 c ---[1708]---> BDD-cost: 67 c ---[1707]---> BDD-cost: 67 c ---[1706]---> BDD-cost: 67 c ---[1705]---> BDD-cost: 67 c ---[1704]---> BDD-cost: 67 c ---[1703]---> BDD-cost: 67 c ---[1702]---> BDD-cost: 67 c ---[1701]---> BDD-cost: 67 c ---[1700]---> BDD-cost: 67 c ---[1699]---> BDD-cost: 67 c ---[1698]---> BDD-cost: 67 c ---[1697]---> BDD-cost: 67 c ---[1696]---> BDD-cost: 67 c ---[1695]---> BDD-cost: 67 c ---[1694]---> BDD-cost: 67 c ---[1693]---> BDD-cost: 67 c ---[1692]---> BDD-cost: 67 c ---[1691]---> BDD-cost: 67 c ---[1690]---> BDD-cost: 67 c ---[1689]---> BDD-cost: 67 c ---[1688]---> BDD-cost: 67 c ---[1687]---> BDD-cost: 67 c ---[1686]---> BDD-cost: 67 c ---[1685]---> BDD-cost: 67 c ---[1684]---> BDD-cost: 67 c ---[1683]---> BDD-cost: 67 c ---[1682]---> BDD-cost: 67 c ---[1681]---> BDD-cost: 67 c ---[1680]---> BDD-cost: 67 c ---[1679]---> BDD-cost: 67 c ---[1678]---> BDD-cost: 67 c ---[1677]---> BDD-cost: 67 c ---[1676]---> BDD-cost: 67 c ---[1675]---> BDD-cost: 67 c ---[1674]---> BDD-cost: 67 c ---[1673]---> BDD-cost: 67 c ---[1672]---> BDD-cost: 67 c ---[1671]---> BDD-cost: 67 c ---[1670]---> BDD-cost: 67 c ---[1669]---> BDD-cost: 67 c ---[1668]---> BDD-cost: 67 c ---[1667]---> BDD-cost: 67 c ---[1666]---> BDD-cost: 67 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 73037 226843 | 24345 0 0 nan | 0.000 % | c | 103 | 73011 226755 | 26779 101 8954 88.7 | 1.045 % | c ============================================================================== c [1mFound solution: -19[0m c ---[ 0]---> Sorter-cost: 2744 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 155 | 75766 233266 | 25255 153 12731 83.2 | 1.045 % | c | 255 | 75766 233266 | 27780 253 17942 70.9 | 0.974 % | c | 405 | 75766 233266 | 30558 403 34078 84.6 | 0.974 % | c | 631 | 75766 233266 | 33614 629 53358 84.8 | 0.974 % | c | 968 | 75766 233266 | 36975 966 113686 117.7 | 0.974 % | c | 1474 | 75759 233243 | 40673 1471 156890 106.7 | 0.978 % | c | 2235 | 75759 233243 | 44740 2232 301014 134.9 | 0.978 % | c | 3375 | 75759 233243 | 49214 3372 428346 127.0 | 0.978 % | c | 5083 | 75759 233243 | 54136 5080 595434 117.2 | 0.978 % | c | 7648 | 75759 233243 | 59549 7645 1308768 171.2 | 0.978 % | c | 11496 | 75759 233243 | 65504 11493 2006373 174.6 | 0.978 % | c | 17263 | 75759 233243 | 72055 17260 3041655 176.2 | 0.978 % | c | 25912 | 75759 233243 | 79261 25909 5528810 213.4 | 0.978 % | c | 38891 | 75759 233243 | 87187 38888 7986840 205.4 | 0.978 % | c | 58353 | 75759 233243 | 95905 58350 14831501 254.2 | 0.978 % | c | 87546 | 75759 233243 | 105496 87543 19435262 222.0 | 0.978 % | c | 131335 | 75752 233220 | 116046 41101 5658706 137.7 | 0.982 % | c ============================================================================== c [1mFound solution: -20[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 175373 | 75716 233147 | 25238 85136 20802504 244.3 | 0.982 % | c | 175475 | 75716 233147 | 27761 15435 3944168 255.5 | 1.072 % | c | 175628 | 75716 233147 | 30537 15588 3971074 254.8 | 1.072 % | c | 175853 | 75716 233147 | 33591 15813 3997539 252.8 | 1.072 % | c | 176190 | 75716 233147 | 36950 16150 4033186 249.7 | 1.072 % | c | 176696 | 75716 233147 | 40646 16656 4118073 247.2 | 1.072 % | c | 177459 | 75716 233147 | 44710 17419 4348647 249.6 | 1.072 % | c | 178598 | 75716 233147 | 49181 18558 4497021 242.3 | 1.072 % | c | 180307 | 75716 233147 | 54099 20267 4760378 234.9 | 1.072 % | c | 182870 | 75716 233147 | 59509 22830 5498072 240.8 | 1.072 % | c | 186716 | 75665 233018 | 65460 26673 6332616 237.4 | 1.151 % | c | 192484 | 75665 233018 | 72006 32441 7694372 237.2 | 1.151 % | c | 201133 | 75665 233018 | 79207 41090 10631407 258.7 | 1.151 % | c | 214109 | 75658 232995 | 87128 54065 12859837 237.9 | 1.155 % | c c *** TERMINATED *** s SATISFIABLE v -N_0x23_1_0x23_2_bit0 -N_0x23_2_0x23_3_bit0 -N_0x23_3_0x23_4_bit0 -N_0x23_4_0x23_5_bit0 -N_0x23_5_0x23_6_bit0 -N_0x23_6_0x23_7_bit0 -N_0x23_8_0x23_9_bit0 -N_0x23_9_0x23_10_bit0 -N_0x23_10_0x23_11_bit0 -N_0x23_11_0x23_12_bit0 -N_0x23_12_0x23_13_bit0 N_0x23_13_0x23_14_bit0 -N_0x23_15_0x23_16_bit0 -N_0x23_16_0x23_17_bit0 N_0x23_17_0x23_18_bit0 -N_0x23_18_0x23_19_bit0 -N_0x23_19_0x23_20_bit0 -N_0x23_20_0x23_21_bit0 -N_0x23_22_0x23_23_bit0 -N_0x23_23_0x23_24_bit0 -N_0x23_24_0x23_25_bit0 -N_0x23_25_0x23_26_bit0 -N_0x23_26_0x23_27_bit0 N_0x23_27_0x23_28_bit0 -N_0x23_29_0x23_30_bit0 -N_0x23_30_0x23_31_bit0 -N_0x23_31_0x23_32_bit0 N_0x23_32_0x23_33_bit0 -N_0x23_33_0x23_34_bit0 -N_0x23_34_0x23_35_bit0 -N_0x23_36_0x23_37_bit0 -N_0x23_37_0x23_38_bit0 N_0x23_38_0x23_39_bit0 N_0x23_39_0x23_40_bit0 -N_0x23_40_0x23_41_bit0 -N_0x23_41_0x23_42_bit0 -N_0x23_43_0x23_44_bit0 -N_0x23_44_0x23_45_bit0 -N_0x23_45_0x23_46_bit0 -N_0x23_46_0x23_47_bit0 -N_0x23_47_0x23_48_bit0 -N_0x23_48_0x23_49_bit0 -N_0x23_1_0x23_8_bit0 -N_0x23_2_0x23_9_bit0 N_0x23_3_0x23_10_bit0 -N_0x23_4_0x23_11_bit0 -N_0x23_5_0x23_12_bit0 -N_0x23_6_0x23_13_bit0 N_0x23_7_0x23_14_bit0 -N_0x23_8_0x23_15_bit0 -N_0x23_9_0x23_16_bit0 N_0x23_10_0x23_17_bit0 -N_0x23_11_0x23_18_bit0 -N_0x23_12_0x23_19_bit0 -N_0x23_13_0x23_20_bit0 -N_0x23_14_0x23_21_bit0 -N_0x23_15_0x23_22_bit0 -N_0x23_16_0x23_23_bit0 -N_0x23_17_0x23_24_bit0 N_0x23_18_0x23_25_bit0 -N_0x23_19_0x23_26_bit0 -N_0x23_20_0x23_27_bit0 -N_0x23_21_0x23_28_bit0 -N_0x23_22_0x23_29_bit0 -N_0x23_23_0x23_30_bit0 -N_0x23_24_0x23_31_bit0 N_0x23_25_0x23_32_bit0 -N_0x23_26_0x23_33_bit0 -N_0x23_27_0x23_34_bit0 N_0x23_28_0x23_35_bit0 -N_0x23_29_0x23_36_bit0 -N_0x23_30_0x23_37_bit0 -N_0x23_31_0x23_38_bit0 N_0x23_32_0x23_39_bit0 N_0x23_33_0x23_40_bit0 -N_0x23_34_0x23_41_bit0 -N_0x23_35_0x23_42_bit0 -N_0x23_36_0x23_43_bit0 -N_0x23_37_0x23_44_bit0 -N_0x23_38_0x23_45_bit0 -N_0x23_39_0x23_46_bit0 -N_0x23_40_0x23_47_bit0 -N_0x23_41_0x23_48_bit0 -N_0x23_42_0x23_49_bit0 -N_0x23_1_0x23_9_bit0 -N_0x23_2_0x23_10_bit0 -N_0x23_3_0x23_11_bit0 -N_0x23_4_0x23_12_bit0 N_0x23_5_0x23_13_bit0 -N_0x23_6_0x23_14_bit0 -N_0x23_8_0x23_16_bit0 -N_0x23_9_0x23_17_bit0 N_0x23_10_0x23_18_bit0 -N_0x23_11_0x23_19_bit0 -N_0x23_12_0x23_20_bit0 -N_0x23_13_0x23_21_bit0 -N_0x23_15_0x23_23_bit0 -N_0x23_16_0x23_24_bit0 N_0x23_17_0x23_25_bit0 -N_0x23_18_0x23_26_bit0 -N_0x23_19_0x23_27_bit0 -N_0x23_20_0x23_28_bit0 -N_0x23_22_0x23_30_bit0 -N_0x23_23_0x23_31_bit0 -N_0x23_24_0x23_32_bit0 N_0x23_25_0x23_33_bit0 -N_0x23_26_0x23_34_bit0 N_0x23_27_0x23_35_bit0 -N_0x23_29_0x23_37_bit0 -N_0x23_30_0x23_38_bit0 -N_0x23_31_0x23_39_bit0 N_0x23_32_0x23_40_bit0 -N_0x23_33_0x23_41_bit0 -N_0x23_34_0x23_42_bit0 -N_0x23_36_0x23_44_bit0 -N_0x23_37_0x23_45_bit0 -N_0x23_38_0x23_46_bit0 -N_0x23_39_0x23_47_bit0 -N_0x23_40_0x23_48_bit0 -N_0x23_41_0x23_49_bit0 -x_0x23_49_0x23_34_bit0 -x_0x23_49_0x23_32_bit0 -x_0x23_49_0x23_30_bit0 -x_0x23_49_0x23_29_bit0 -x_0x23_49_0x23_27_bit0 -x_0x23_49_0x23_26_bit0 -x_0x23_49_0x23_23_bit0 -x_0x23_49_0x23_20_bit0 -x_0x23_49_0x23_18_bit0 -x_0x23_49_0x23_16_bit0 -x_0x23_49_0x23_13_bit0 -x_0x23_49_0x23_11_bit0 -x_0x23_49_0x23_9_bit0 -x_0x23_49_0x23_8_bit0 -x_0x23_49_0x23_6_bit0 -x_0x23_49_0x23_3_bit0 -x_0x23_49_0x23_1_bit0 -x_0x23_48_0x23_34_bit0 -x_0x23_48_0x23_32_bit0 -x_0x23_48_0x23_30_bit0 -x_0x23_48_0x23_29_bit0 -x_0x23_48_0x23_27_bit0 -x_0x23_48_0x23_26_bit0 -x_0x23_48_0x23_23_bit0 -x_0x23_48_0x23_20_bit0 -x_0x23_48_0x23_18_bit0 -x_0x23_48_0x23_16_bit0 -x_0x23_48_0x23_13_bit0 -x_0x23_48_0x23_11_bit0 -x_0x23_48_0x23_9_bit0 -x_0x23_48_0x23_8_bit0 -x_0x23_48_0x23_6_bit0 -x_0x23_48_0x23_3_bit0 -x_0x23_48_0x23_1_bit0 -x_0x23_47_0x23_34_bit0 -x_0x23_47_0x23_32_bit0 -x_0x23_47_0x23_30_bit0 -x_0x23_47_0x23_29_bit0 -x_0x23_47_0x23_27_bit0 -x_0x23_47_0x23_26_bit0 -x_0x23_47_0x23_23_bit0 -x_0x23_47_0x23_20_bit0 -x_0x23_47_0x23_18_bit0 -x_0x23_47_0x23_16_bit0 -x_0x23_47_0x23_13_bit0 -x_0x23_47_0x23_11_bit0 -x_0x23_47_0x23_9_bit0 -x_0x23_47_0x23_8_bit0 -x_0x23_47_0x23_6_bit0 -x_0x23_47_0x23_3_bit0 -x_0x23_47_0x23_1_bit0 -x_0x23_46_0x23_34_bit0 -x_0x23_46_0x23_32_bit0 -x_0x23_46_0x23_30_bit0 -x_0x23_46_0x23_29_bit0 -x_0x23_46_0x23_27_bit0 -x_0x23_46_0x23_26_bit0 -x_0x23_46_0x23_23_bit0 -x_0x23_46_0x23_20_bit0 -x_0x23_46_0x23_18_bit0 -x_0x23_46_0x23_16_bit0 -x_0x23_46_0x23_13_bit0 -x_0x23_46_0x23_11_bit0 -x_0x23_46_0x23_9_bit0 -x_0x23_46_0x23_8_bit0 -x_0x23_46_0x23_6_bit0 -x_0x23_46_0x23_3_bit0 -x_0x23_46_0x23_1_bit0 -x_0x23_45_0x23_34_bit0 -x_0x23_45_0x23_32_bit0 -x_0x23_45_0x23_30_bit0 -x_0x23_45_0x23_29_bit0 -x_0x23_45_0x23_27_bit0 -x_0x23_45_0x23_26_bit0 -x_0x23_45_0x23_23_bit0 -x_0x23_45_0x23_20_bit0 -x_0x23_45_0x23_18_bit0 -x_0x23_45_0x23_16_bit0 -x_0x23_45_0x23_13_bit0 -x_0x23_45_0x23_11_bit0 -x_0x23_45_0x23_9_bit0 -x_0x23_45_0x23_8_bit0 -x_0x23_45_0x23_6_bit0 -x_0x23_45_0x23_3_bit0 -x_0x23_45_0x23_1_bit0 -x_0x23_44_0x23_34_bit0 -x_0x23_44_0x23_32_bit0 -x_0x23_44_0x23_30_bit0 -x_0x23_44_0x23_29_bit0 -x_0x23_44_0x23_27_bit0 -x_0x23_44_0x23_26_bit0 -x_0x23_44_0x23_23_bit0 -x_0x23_44_0x23_20_bit0 -x_0x23_44_0x23_18_bit0 -x_0x23_44_0x23_16_bit0 -x_0x23_44_0x23_13_bit0 -x_0x23_44_0x23_11_bit0 -x_0x23_44_0x23_9_bit0 -x_0x23_44_0x23_8_bit0 -x_0x23_44_0x23_6_bit0 -x_0x23_44_0x23_3_bit0 -x_0x23_44_0x23_1_bit0 -x_0x23_43_0x23_34_bit0 -x_0x23_43_0x23_32_bit0 -x_0x23_43_0x23_30_bit0 -x_0x23_43_0x23_29_bit0 -x_0x23_43_0x23_27_bit0 -x_0x23_43_0x23_26_bit0 -x_0x23_43_0x23_23_bit0 -x_0x23_43_0x23_20_bit0 -x_0x23_43_0x23_18_bit0 -x_0x23_43_0x23_16_bit0 -x_0x23_43_0x23_13_bit0 -x_0x23_43_0x23_11_bit0 -x_0x23_43_0x23_9_bit0 -x_0x23_43_0x23_8_bit0 -x_0x23_43_0x23_6_bit0 -x_0x23_43_0x23_3_bit0 -x_0x23_43_0x23_1_bit0 -x_0x23_42_0x23_34_bit0 -x_0x23_42_0x23_32_bit0 -x_0x23_42_0x23_30_bit0 -x_0x23_42_0x23_29_bit0 -x_0x23_42_0x23_27_bit0 -x_0x23_42_0x23_26_bit0 -x_0x23_42_0x23_23_bit0 -x_0x23_42_0x23_20_bit0 -x_0x23_42_0x23_18_bit0 -x_0x23_42_0x23_16_bit0 -x_0x23_42_0x23_13_bit0 -x_0x23_42_0x23_11_bit0 -x_0x23_42_0x23_9_bit0 -x_0x23_42_0x23_8_bit0 -x_0x23_42_0x23_6_bit0 -x_0x23_42_0x23_3_bit0 -x_0x23_42_0x23_1_bit0 -x_0x23_41_0x23_34_bit0 -x_0x23_41_0x23_32_bit0 -x_0x23_41_0x23_30_bit0 -x_0x23_41_0x23_29_bit0 -x_0x23_41_0x23_27_bit0 -x_0x23_41_0x23_26_bit0 -x_0x23_41_0x23_23_bit0 -x_0x23_41_0x23_20_bit0 -x_0x23_41_0x23_18_bit0 -x_0x23_41_0x23_16_bit0 -x_0x23_41_0x23_13_bit0 -x_0x23_41_0x23_11_bit0 -x_0x23_41_0x23_9_bit0 -x_0x23_41_0x23_8_bit0 -x_0x23_41_0x23_6_bit0 -x_0x23_41_0x23_3_bit0 -x_0x23_41_0x23_1_bit0 -x_0x23_40_0x23_34_bit0 -x_0x23_40_0x23_32_bit0 -x_0x23_40_0x23_30_bit0 -x_0x23_40_0x23_29_bit0 -x_0x23_40_0x23_27_bit0 -x_0x23_40_0x23_26_bit0 -x_0x23_40_0x23_23_bit0 x_0x23_40_0x23_20_bit0 -x_0x23_40_0x23_18_bit0 -x_0x23_40_0x23_16_bit0 -x_0x23_40_0x23_13_bit0 -x_0x23_40_0x23_11_bit0 -x_0x23_40_0x23_9_bit0 -x_0x23_40_0x23_8_bit0 -x_0x23_40_0x23_6_bit0 -x_0x23_40_0x23_3_bit0 -x_0x23_40_0x23_1_bit0 -x_0x23_39_0x23_34_bit0 -x_0x23_39_0x23_32_bit0 -x_0x23_39_0x23_30_bit0 -x_0x23_39_0x23_29_bit0 -x_0x23_39_0x23_27_bit0 -x_0x23_39_0x23_26_bit0 -x_0x23_39_0x23_23_bit0 -x_0x23_39_0x23_20_bit0 x_0x23_39_0x23_18_bit0 -x_0x23_39_0x23_16_bit0 -x_0x23_39_0x23_13_bit0 -x_0x23_39_0x23_11_bit0 -x_0x23_39_0x23_9_bit0 -x_0x23_39_0x23_8_bit0 -x_0x23_39_0x23_6_bit0 -x_0x23_39_0x23_3_bit0 -x_0x23_39_0x23_1_bit0 -x_0x23_38_0x23_34_bit0 -x_0x23_38_0x23_32_bit0 -x_0x23_38_0x23_30_bit0 -x_0x23_38_0x23_29_bit0 -x_0x23_38_0x23_27_bit0 -x_0x23_38_0x23_26_bit0 -x_0x23_38_0x23_23_bit0 -x_0x23_38_0x23_20_bit0 -x_0x23_38_0x23_18_bit0 x_0x23_38_0x23_16_bit0 -x_0x23_38_0x23_13_bit0 -x_0x23_38_0x23_11_bit0 -x_0x23_38_0x23_9_bit0 -x_0x23_38_0x23_8_bit0 -x_0x23_38_0x23_6_bit0 -x_0x23_38_0x23_3_bit0 -x_0x23_38_0x23_1_bit0 -x_0x23_37_0x23_34_bit0 -x_0x23_37_0x23_32_bit0 -x_0x23_37_0x23_30_bit0 -x_0x23_37_0x23_29_bit0 -x_0x23_37_0x23_27_bit0 -x_0x23_37_0x23_26_bit0 -x_0x23_37_0x23_23_bit0 -x_0x23_37_0x23_20_bit0 -x_0x23_37_0x23_18_bit0 -x_0x23_37_0x23_16_bit0 -x_0x23_37_0x23_13_bit0 -x_0x23_37_0x23_11_bit0 -x_0x23_37_0x23_9_bit0 -x_0x23_37_0x23_8_bit0 -x_0x23_37_0x23_6_bit0 -x_0x23_37_0x23_3_bit0 -x_0x23_37_0x23_1_bit0 -x_0x23_36_0x23_34_bit0 -x_0x23_36_0x23_32_bit0 -x_0x23_36_0x23_30_bit0 -x_0x23_36_0x23_29_bit0 -x_0x23_36_0x23_27_bit0 -x_0x23_36_0x23_26_bit0 -x_0x23_36_0x23_23_bit0 -x_0x23_36_0x23_20_bit0 -x_0x23_36_0x23_18_bit0 -x_0x23_36_0x23_16_bit0 -x_0x23_36_0x23_13_bit0 -x_0x23_36_0x23_11_bit0 -x_0x23_36_0x23_9_bit0 -x_0x23_36_0x23_8_bit0 -x_0x23_36_0x23_6_bit0 -x_0x23_36_0x23_3_bit0 -x_0x23_36_0x23_1_bit0 -x_0x23_35_0x23_34_bit0 -x_0x23_35_0x23_32_bit0 -x_0x23_35_0x23_30_bit0 -x_0x23_35_0x23_29_bit0 -x_0x23_35_0x23_27_bit0 x_0x23_35_0x23_26_bit0 -x_0x23_35_0x23_23_bit0 -x_0x23_35_0x23_20_bit0 -x_0x23_35_0x23_18_bit0 -x_0x23_35_0x23_16_bit0 -x_0x23_35_0x23_13_bit0 -x_0x23_35_0x23_11_bit0 -x_0x23_35_0x23_9_bit0 -x_0x23_35_0x23_8_bit0 -x_0x23_35_0x23_6_bit0 -x_0x23_35_0x23_3_bit0 -x_0x23_35_0x23_1_bit0 -x_0x23_34_0x23_34_bit0 -x_0x23_34_0x23_32_bit0 -x_0x23_34_0x23_30_bit0 -x_0x23_34_0x23_29_bit0 -x_0x23_34_0x23_27_bit0 -x_0x23_34_0x23_26_bit0 -x_0x23_34_0x23_23_bit0 -x_0x23_34_0x23_20_bit0 -x_0x23_34_0x23_18_bit0 -x_0x23_34_0x23_16_bit0 -x_0x23_34_0x23_13_bit0 -x_0x23_34_0x23_11_bit0 -x_0x23_34_0x23_9_bit0 -x_0x23_34_0x23_8_bit0 -x_0x23_34_0x23_6_bit0 -x_0x23_34_0x23_3_bit0 -x_0x23_34_0x23_1_bit0 -x_0x23_33_0x23_34_bit0 -x_0x23_33_0x23_32_bit0 -x_0x23_33_0x23_30_bit0 -x_0x23_33_0x23_29_bit0 -x_0x23_33_0x23_27_bit0 -x_0x23_33_0x23_26_bit0 x_0x23_33_0x23_23_bit0 -x_0x23_33_0x23_20_bit0 -x_0x23_33_0x23_18_bit0 -x_0x23_33_0x23_16_bit0 -x_0x23_33_0x23_13_bit0 -x_0x23_33_0x23_11_bit0 -x_0x23_33_0x23_9_bit0 -x_0x23_33_0x23_8_bit0 -x_0x23_33_0x23_6_bit0 -x_0x23_33_0x23_3_bit0 -x_0x23_33_0x23_1_bit0 -x_0x23_32_0x23_34_bit0 -x_0x23_32_0x23_32_bit0 -x_0x23_32_0x23_30_bit0 -x_0x23_32_0x23_29_bit0 -x_0x23_32_0x23_27_bit0 -x_0x23_32_0x23_26_bit0 -x_0x23_32_0x23_23_bit0 -x_0x23_32_0x23_20_bit0 -x_0x23_32_0x23_18_bit0 -x_0x23_32_0x23_16_bit0 x_0x23_32_0x23_13_bit0 -x_0x23_32_0x23_11_bit0 -x_0x23_32_0x23_9_bit0 -x_0x23_32_0x23_8_bit0 -x_0x23_32_0x23_6_bit0 -x_0x23_32_0x23_3_bit0 -x_0x23_32_0x23_1_bit0 -x_0x23_31_0x23_34_bit0 -x_0x23_31_0x23_32_bit0 -x_0x23_31_0x23_30_bit0 -x_0x23_31_0x23_29_bit0 -x_0x23_31_0x23_27_bit0 -x_0x23_31_0x23_26_bit0 -x_0x23_31_0x23_23_bit0 -x_0x23_31_0x23_20_bit0 -x_0x23_31_0x23_18_bit0 -x_0x23_31_0x23_16_bit0 -x_0x23_31_0x23_13_bit0 -x_0x23_31_0x23_11_bit0 -x_0x23_31_0x23_9_bit0 -x_0x23_31_0x23_8_bit0 -x_0x23_31_0x23_6_bit0 -x_0x23_31_0x23_3_bit0 -x_0x23_31_0x23_1_bit0 -x_0x23_30_0x23_34_bit0 -x_0x23_30_0x23_32_bit0 -x_0x23_30_0x23_30_bit0 -x_0x23_30_0x23_29_bit0 -x_0x23_30_0x23_27_bit0 -x_0x23_30_0x23_26_bit0 -x_0x23_30_0x23_23_bit0 -x_0x23_30_0x23_20_bit0 -x_0x23_30_0x23_18_bit0 -x_0x23_30_0x23_16_bit0 -x_0x23_30_0x23_13_bit0 -x_0x23_30_0x23_11_bit0 -x_0x23_30_0x23_9_bit0 -x_0x23_30_0x23_8_bit0 -x_0x23_30_0x23_6_bit0 -x_0x23_30_0x23_3_bit0 -x_0x23_30_0x23_1_bit0 -x_0x23_29_0x23_34_bit0 -x_0x23_29_0x23_32_bit0 -x_0x23_29_0x23_30_bit0 -x_0x23_29_0x23_29_bit0 -x_0x23_29_0x23_27_bit0 -x_0x23_29_0x23_26_bit0 -x_0x23_29_0x23_23_bit0 -x_0x23_29_0x23_20_bit0 -x_0x23_29_0x23_18_bit0 -x_0x23_29_0x23_16_bit0 -x_0x23_29_0x23_13_bit0 -x_0x23_29_0x23_11_bit0 -x_0x23_29_0x23_9_bit0 -x_0x23_29_0x23_8_bit0 -x_0x23_29_0x23_6_bit0 -x_0x23_29_0x23_3_bit0 -x_0x23_29_0x23_1_bit0 -x_0x23_28_0x23_34_bit0 -x_0x23_28_0x23_32_bit0 -x_0x23_28_0x23_30_bit0 -x_0x23_28_0x23_29_bit0 x_0x23_28_0x23_27_bit0 -x_0x23_28_0x23_26_bit0 -x_0x23_28_0x23_23_bit0 -x_0x23_28_0x23_20_bit0 -x_0x23_28_0x23_18_bit0 -x_0x23_28_0x23_16_bit0 -x_0x23_28_0x23_13_bit0 -x_0x23_28_0x23_11_bit0 -x_0x23_28_0x23_9_bit0 -x_0x23_28_0x23_8_bit0 -x_0x23_28_0x23_6_bit0 -x_0x23_28_0x23_3_bit0 -x_0x23_28_0x23_1_bit0 -x_0x23_27_0x23_34_bit0 -x_0x23_27_0x23_32_bit0 -x_0x23_27_0x23_30_bit0 -x_0x23_27_0x23_29_bit0 -x_0x23_27_0x23_27_bit0 -x_0x23_27_0x23_26_bit0 -x_0x23_27_0x23_23_bit0 -x_0x23_27_0x23_20_bit0 -x_0x23_27_0x23_18_bit0 -x_0x23_27_0x23_16_bit0 -x_0x23_27_0x23_13_bit0 -x_0x23_27_0x23_11_bit0 -x_0x23_27_0x23_9_bit0 -x_0x23_27_0x23_8_bit0 -x_0x23_27_0x23_6_bit0 -x_0x23_27_0x23_3_bit0 x_0x23_27_0x23_1_bit0 -x_0x23_26_0x23_34_bit0 -x_0x23_26_0x23_32_bit0 -x_0x23_26_0x23_30_bit0 -x_0x23_26_0x23_29_bit0 -x_0x23_26_0x23_27_bit0 -x_0x23_26_0x23_26_bit0 -x_0x23_26_0x23_23_bit0 -x_0x23_26_0x23_20_bit0 -x_0x23_26_0x23_18_bit0 -x_0x23_26_0x23_16_bit0 -x_0x23_26_0x23_13_bit0 -x_0x23_26_0x23_11_bit0 -x_0x23_26_0x23_9_bit0 -x_0x23_26_0x23_8_bit0 -x_0x23_26_0x23_6_bit0 -x_0x23_26_0x23_3_bit0 -x_0x23_26_0x23_1_bit0 -x_0x23_25_0x23_34_bit0 -x_0x23_25_0x23_32_bit0 -x_0x23_25_0x23_30_bit0 -x_0x23_25_0x23_29_bit0 -x_0x23_25_0x23_27_bit0 -x_0x23_25_0x23_26_bit0 -x_0x23_25_0x23_23_bit0 -x_0x23_25_0x23_20_bit0 -x_0x23_25_0x23_18_bit0 -x_0x23_25_0x23_16_bit0 -x_0x23_25_0x23_13_bit0 x_0x23_25_0x23_11_bit0 -x_0x23_25_0x23_9_bit0 -x_0x23_25_0x23_8_bit0 -x_0x23_25_0x23_6_bit0 -x_0x23_25_0x23_3_bit0 -x_0x23_25_0x23_1_bit0 -x_0x23_24_0x23_34_bit0 -x_0x23_24_0x23_32_bit0 -x_0x23_24_0x23_30_bit0 -x_0x23_24_0x23_29_bit0 -x_0x23_24_0x23_27_bit0 -x_0x23_24_0x23_26_bit0 -x_0x23_24_0x23_23_bit0 -x_0x23_24_0x23_20_bit0 -x_0x23_24_0x23_18_bit0 -x_0x23_24_0x23_16_bit0 -x_0x23_24_0x23_13_bit0 -x_0x23_24_0x23_11_bit0 -x_0x23_24_0x23_9_bit0 -x_0x23_24_0x23_8_bit0 -x_0x23_24_0x23_6_bit0 -x_0x23_24_0x23_3_bit0 -x_0x23_24_0x23_1_bit0 -x_0x23_23_0x23_34_bit0 -x_0x23_23_0x23_32_bit0 -x_0x23_23_0x23_30_bit0 -x_0x23_23_0x23_29_bit0 -x_0x23_23_0x23_27_bit0 -x_0x23_23_0x23_26_bit0 -x_0x23_23_0x23_23_bit0 -x_0x23_23_0x23_20_bit0 -x_0x23_23_0x23_18_bit0 -x_0x23_23_0x23_16_bit0 -x_0x23_23_0x23_13_bit0 -x_0x23_23_0x23_11_bit0 -x_0x23_23_0x23_9_bit0 -x_0x23_23_0x23_8_bit0 -x_0x23_23_0x23_6_bit0 -x_0x23_23_0x23_3_bit0 -x_0x23_23_0x23_1_bit0 -x_0x23_22_0x23_34_bit0 -x_0x23_22_0x23_32_bit0 -x_0x23_22_0x23_30_bit0 -x_0x23_22_0x23_29_bit0 -x_0x23_22_0x23_27_bit0 -x_0x23_22_0x23_26_bit0 -x_0x23_22_0x23_23_bit0 -x_0x23_22_0x23_20_bit0 -x_0x23_22_0x23_18_bit0 -x_0x23_22_0x23_16_bit0 -x_0x23_22_0x23_13_bit0 -x_0x23_22_0x23_11_bit0 -x_0x23_22_0x23_9_bit0 -x_0x23_22_0x23_8_bit0 -x_0x23_22_0x23_6_bit0 -x_0x23_22_0x23_3_bit0 -x_0x23_22_0x23_1_bit0 -x_0x23_21_0x23_34_bit0 -x_0x23_21_0x23_32_bit0 -x_0x23_21_0x23_30_bit0 -x_0x23_21_0x23_29_bit0 -x_0x23_21_0x23_27_bit0 -x_0x23_21_0x23_26_bit0 -x_0x23_21_0x23_23_bit0 -x_0x23_21_0x23_20_bit0 -x_0x23_21_0x23_18_bit0 -x_0x23_21_0x23_16_bit0 -x_0x23_21_0x23_13_bit0 -x_0x23_21_0x23_11_bit0 -x_0x23_21_0x23_9_bit0 -x_0x23_21_0x23_8_bit0 -x_0x23_21_0x23_6_bit0 -x_0x23_21_0x23_3_bit0 -x_0x23_21_0x23_1_bit0 -x_0x23_20_0x23_34_bit0 -x_0x23_20_0x23_32_bit0 -x_0x23_20_0x23_30_bit0 -x_0x23_20_0x23_29_bit0 -x_0x23_20_0x23_27_bit0 -x_0x23_20_0x23_26_bit0 -x_0x23_20_0x23_23_bit0 -x_0x23_20_0x23_20_bit0 -x_0x23_20_0x23_18_bit0 -x_0x23_20_0x23_16_bit0 -x_0x23_20_0x23_13_bit0 -x_0x23_20_0x23_11_bit0 -x_0x23_20_0x23_9_bit0 -x_0x23_20_0x23_8_bit0 -x_0x23_20_0x23_6_bit0 -x_0x23_20_0x23_3_bit0 -x_0x23_20_0x23_1_bit0 -x_0x23_19_0x23_34_bit0 -x_0x23_19_0x23_32_bit0 -x_0x23_19_0x23_30_bit0 -x_0x23_19_0x23_29_bit0 -x_0x23_19_0x23_27_bit0 -x_0x23_19_0x23_26_bit0 -x_0x23_19_0x23_23_bit0 -x_0x23_19_0x23_20_bit0 -x_0x23_19_0x23_18_bit0 -x_0x23_19_0x23_16_bit0 -x_0x23_19_0x23_13_bit0 -x_0x23_19_0x23_11_bit0 -x_0x23_19_0x23_9_bit0 -x_0x23_19_0x23_8_bit0 -x_0x23_19_0x23_6_bit0 -x_0x23_19_0x23_3_bit0 -x_0x23_19_0x23_1_bit0 -x_0x23_18_0x23_34_bit0 -x_0x23_18_0x23_32_bit0 -x_0x23_18_0x23_30_bit0 -x_0x23_18_0x23_29_bit0 -x_0x23_18_0x23_27_bit0 -x_0x23_18_0x23_26_bit0 -x_0x23_18_0x23_23_bit0 -x_0x23_18_0x23_20_bit0 -x_0x23_18_0x23_18_bit0 -x_0x23_18_0x23_16_bit0 -x_0x23_18_0x23_13_bit0 -x_0x23_18_0x23_11_bit0 x_0x23_18_0x23_9_bit0 -x_0x23_18_0x23_8_bit0 -x_0x23_18_0x23_6_bit0 -x_0x23_18_0x23_3_bit0 -x_0x23_18_0x23_1_bit0 -x_0x23_17_0x23_34_bit0 -x_0x23_17_0x23_32_bit0 -x_0x23_17_0x23_30_bit0 -x_0x23_17_0x23_29_bit0 -x_0x23_17_0x23_27_bit0 -x_0x23_17_0x23_26_bit0 -x_0x23_17_0x23_23_bit0 -x_0x23_17_0x23_20_bit0 -x_0x23_17_0x23_18_bit0 -x_0x23_17_0x23_16_bit0 -x_0x23_17_0x23_13_bit0 -x_0x23_17_0x23_11_bit0 -x_0x23_17_0x23_9_bit0 x_0x23_17_0x23_8_bit0 -x_0x23_17_0x23_6_bit0 -x_0x23_17_0x23_3_bit0 -x_0x23_17_0x23_1_bit0 -x_0x23_16_0x23_34_bit0 -x_0x23_16_0x23_32_bit0 -x_0x23_16_0x23_30_bit0 -x_0x23_16_0x23_29_bit0 -x_0x23_16_0x23_27_bit0 -x_0x23_16_0x23_26_bit0 -x_0x23_16_0x23_23_bit0 -x_0x23_16_0x23_20_bit0 -x_0x23_16_0x23_18_bit0 -x_0x23_16_0x23_16_bit0 -x_0x23_16_0x23_13_bit0 -x_0x23_16_0x23_11_bit0 -x_0x23_16_0x23_9_bit0 -x_0x23_16_0x23_8_bit0 -x_0x23_16_0x23_6_bit0 -x_0x23_16_0x23_3_bit0 -x_0x23_16_0x23_1_bit0 -x_0x23_15_0x23_34_bit0 -x_0x23_15_0x23_32_bit0 -x_0x23_15_0x23_30_bit0 -x_0x23_15_0x23_29_bit0 -x_0x23_15_0x23_27_bit0 -x_0x23_15_0x23_26_bit0 -x_0x23_15_0x23_23_bit0 -x_0x23_15_0x23_20_bit0 -x_0x23_15_0x23_18_bit0 -x_0x23_15_0x23_16_bit0 -x_0x23_15_0x23_13_bit0 -x_0x23_15_0x23_11_bit0 -x_0x23_15_0x23_9_bit0 -x_0x23_15_0x23_8_bit0 -x_0x23_15_0x23_6_bit0 -x_0x23_15_0x23_3_bit0 -x_0x23_15_0x23_1_bit0 -x_0x23_14_0x23_34_bit0 -x_0x23_14_0x23_32_bit0 -x_0x23_14_0x23_30_bit0 x_0x23_14_0x23_29_bit0 -x_0x23_14_0x23_27_bit0 -x_0x23_14_0x23_26_bit0 -x_0x23_14_0x23_23_bit0 -x_0x23_14_0x23_20_bit0 -x_0x23_14_0x23_18_bit0 -x_0x23_14_0x23_16_bit0 -x_0x23_14_0x23_13_bit0 -x_0x23_14_0x23_11_bit0 -x_0x23_14_0x23_9_bit0 -x_0x23_14_0x23_8_bit0 -x_0x23_14_0x23_6_bit0 -x_0x23_14_0x23_3_bit0 -x_0x23_14_0x23_1_bit0 -x_0x23_13_0x23_34_bit0 -x_0x23_13_0x23_32_bit0 -x_0x23_13_0x23_30_bit0 -x_0x23_13_0x23_29_bit0 -x_0x23_13_0x23_27_bit0 -x_0x23_13_0x23_26_bit0 -x_0x23_13_0x23_23_bit0 -x_0x23_13_0x23_20_bit0 -x_0x23_13_0x23_18_bit0 -x_0x23_13_0x23_16_bit0 -x_0x23_13_0x23_13_bit0 -x_0x23_13_0x23_11_bit0 -x_0x23_13_0x23_9_bit0 -x_0x23_13_0x23_8_bit0 -x_0x23_13_0x23_6_bit0 x_0x23_13_0x23_3_bit0 -x_0x23_13_0x23_1_bit0 -x_0x23_12_0x23_34_bit0 -x_0x23_12_0x23_32_bit0 -x_0x23_12_0x23_30_bit0 -x_0x23_12_0x23_29_bit0 -x_0x23_12_0x23_27_bit0 -x_0x23_12_0x23_26_bit0 -x_0x23_12_0x23_23_bit0 -x_0x23_12_0x23_20_bit0 -x_0x23_12_0x23_18_bit0 -x_0x23_12_0x23_16_bit0 -x_0x23_12_0x23_13_bit0 -x_0x23_12_0x23_11_bit0 -x_0x23_12_0x23_9_bit0 -x_0x23_12_0x23_8_bit0 -x_0x23_12_0x23_6_bit0 -x_0x23_12_0x23_3_bit0 -x_0x23_12_0x23_1_bit0 -x_0x23_11_0x23_34_bit0 -x_0x23_11_0x23_32_bit0 -x_0x23_11_0x23_30_bit0 -x_0x23_11_0x23_29_bit0 -x_0x23_11_0x23_27_bit0 -x_0x23_11_0x23_26_bit0 -x_0x23_11_0x23_23_bit0 -x_0x23_11_0x23_20_bit0 -x_0x23_11_0x23_18_bit0 -x_0x23_11_0x23_16_bit0 -x_0x23_11_0x23_13_bit0 -x_0x23_11_0x23_11_bit0 -x_0x23_11_0x23_9_bit0 -x_0x23_11_0x23_8_bit0 -x_0x23_11_0x23_6_bit0 -x_0x23_11_0x23_3_bit0 -x_0x23_11_0x23_1_bit0 -x_0x23_10_0x23_34_bit0 -x_0x23_10_0x23_32_bit0 -x_0x23_10_0x23_30_bit0 -x_0x23_10_0x23_29_bit0 -x_0x23_10_0x23_27_bit0 -x_0x23_10_0x23_26_bit0 -x_0x23_10_0x23_23_bit0 -x_0x23_10_0x23_20_bit0 -x_0x23_10_0x23_18_bit0 -x_0x23_10_0x23_16_bit0 -x_0x23_10_0x23_13_bit0 -x_0x23_10_0x23_11_bit0 -x_0x23_10_0x23_9_bit0 -x_0x23_10_0x23_8_bit0 x_0x23_10_0x23_6_bit0 -x_0x23_10_0x23_3_bit0 -x_0x23_10_0x23_1_bit0 -x_0x23_9_0x23_34_bit0 -x_0x23_9_0x23_32_bit0 -x_0x23_9_0x23_30_bit0 -x_0x23_9_0x23_29_bit0 -x_0x23_9_0x23_27_bit0 -x_0x23_9_0x23_26_bit0 -x_0x23_9_0x23_23_bit0 -x_0x23_9_0x23_20_bit0 -x_0x23_9_0x23_18_bit0 -x_0x23_9_0x23_16_bit0 -x_0x23_9_0x23_13_bit0 -x_0x23_9_0x23_11_bit0 -x_0x23_9_0x23_9_bit0 -x_0x23_9_0x23_8_bit0 -x_0x23_9_0x23_6_bit0 -x_0x23_9_0x23_3_bit0 -x_0x23_9_0x23_1_bit0 -x_0x23_8_0x23_34_bit0 -x_0x23_8_0x23_32_bit0 -x_0x23_8_0x23_30_bit0 -x_0x23_8_0x23_29_bit0 -x_0x23_8_0x23_27_bit0 -x_0x23_8_0x23_26_bit0 -x_0x23_8_0x23_23_bit0 -x_0x23_8_0x23_20_bit0 -x_0x23_8_0x23_18_bit0 -x_0x23_8_0x23_16_bit0 -x_0x23_8_0x23_13_bit0 -x_0x23_8_0x23_11_bit0 -x_0x23_8_0x23_9_bit0 -x_0x23_8_0x23_8_bit0 -x_0x23_8_0x23_6_bit0 -x_0x23_8_0x23_3_bit0 -x_0x23_8_0x23_1_bit0 -x_0x23_7_0x23_34_bit0 -x_0x23_7_0x23_32_bit0 x_0x23_7_0x23_30_bit0 -x_0x23_7_0x23_29_bit0 -x_0x23_7_0x23_27_bit0 -x_0x23_7_0x23_26_bit0 -x_0x23_7_0x23_23_bit0 -x_0x23_7_0x23_20_bit0 -x_0x23_7_0x23_18_bit0 -x_0x23_7_0x23_16_bit0 -x_0x23_7_0x23_13_bit0 -x_0x23_7_0x23_11_bit0 -x_0x23_7_0x23_9_bit0 -x_0x23_7_0x23_8_bit0 -x_0x23_7_0x23_6_bit0 -x_0x23_7_0x23_3_bit0 -x_0x23_7_0x23_1_bit0 -x_0x23_6_0x23_34_bit0 -x_0x23_6_0x23_32_bit0 -x_0x23_6_0x23_30_bit0 -x_0x23_6_0x23_29_bit0 -x_0x23_6_0x23_27_bit0 -x_0x23_6_0x23_26_bit0 -x_0x23_6_0x23_23_bit0 -x_0x23_6_0x23_20_bit0 -x_0x23_6_0x23_18_bit0 -x_0x23_6_0x23_16_bit0 -x_0x23_6_0x23_13_bit0 -x_0x23_6_0x23_11_bit0 -x_0x23_6_0x23_9_bit0 -x_0x23_6_0x23_8_bit0 -x_0x23_6_0x23_6_bit0 -x_0x23_6_0x23_3_bit0 -x_0x23_6_0x23_1_bit0 -x_0x23_5_0x23_34_bit0 x_0x23_5_0x23_32_bit0 -x_0x23_5_0x23_30_bit0 -x_0x23_5_0x23_29_bit0 -x_0x23_5_0x23_27_bit0 -x_0x23_5_0x23_26_bit0 -x_0x23_5_0x23_23_bit0 -x_0x23_5_0x23_20_bit0 -x_0x23_5_0x23_18_bit0 -x_0x23_5_0x23_16_bit0 -x_0x23_5_0x23_13_bit0 -x_0x23_5_0x23_11_bit0 -x_0x23_5_0x23_9_bit0 -x_0x23_5_0x23_8_bit0 -x_0x23_5_0x23_6_bit0 -x_0x23_5_0x23_3_bit0 -x_0x23_5_0x23_1_bit0 -x_0x23_4_0x23_34_bit0 -x_0x23_4_0x23_32_bit0 -x_0x23_4_0x23_30_bit0 -x_0x23_4_0x23_29_bit0 -x_0x23_4_0x23_27_bit0 -x_0x23_4_0x23_26_bit0 -x_0x23_4_0x23_23_bit0 -x_0x23_4_0x23_20_bit0 -x_0x23_4_0x23_18_bit0 -x_0x23_4_0x23_16_bit0 -x_0x23_4_0x23_13_bit0 -x_0x23_4_0x23_11_bit0 -x_0x23_4_0x23_9_bit0 -x_0x23_4_0x23_8_bit0 -x_0x23_4_0x23_6_bit0 -x_0x23_4_0x23_3_bit0 -x_0x23_4_0x23_1_bit0 x_0x23_3_0x23_34_bit0 -x_0x23_3_0x23_32_bit0 -x_0x23_3_0x23_30_bit0 -x_0x23_3_0x23_29_bit0 -x_0x23_3_0x23_27_bit0 -x_0x23_3_0x23_26_bit0 -x_0x23_3_0x23_23_bit0 -x_0x23_3_0x23_20_bit0 -x_0x23_3_0x23_18_bit0 -x_0x23_3_0x23_16_bit0 -x_0x23_3_0x23_13_bit0 -x_0x23_3_0x23_11_bit0 -x_0x23_3_0x23_9_bit0 -x_0x23_3_0x23_8_bit0 -x_0x23_3_0x23_6_bit0 -x_0x23_3_0x23_3_bit0 -x_0x23_3_0x23_1_bit0 -x_0x23_2_0x23_34_bit0 -x_0x23_2_0x23_32_bit0 -x_0x23_2_0x23_30_bit0 -x_0x23_2_0x23_29_bit0 -x_0x23_2_0x23_27_bit0 -x_0x23_2_0x23_26_bit0 -x_0x23_2_0x23_23_bit0 -x_0x23_2_0x23_20_bit0 -x_0x23_2_0x23_18_bit0 -x_0x23_2_0x23_16_bit0 -x_0x23_2_0x23_13_bit0 -x_0x23_2_0x23_11_bit0 -x_0x23_2_0x23_9_bit0 -x_0x23_2_0x23_8_bit0 -x_0x23_2_0x23_6_bit0 -x_0x23_2_0x23_3_bit0 -x_0x23_2_0x23_1_bit0 -x_0x23_1_0x23_34_bit0 -x_0x23_1_0x23_32_bit0 -x_0x23_1_0x23_30_bit0 -x_0x23_1_0x23_29_bit0 -x_0x23_1_0x23_27_bit0 -x_0x23_1_0x23_26_bit0 -x_0x23_1_0x23_23_bit0 -x_0x23_1_0x23_20_bit0 -x_0x23_1_0x23_18_bit0 -x_0x23_1_0x23_16_bit0 -x_0x23_1_0x23_13_bit0 -x_0x23_1_0x23_11_bit0 -x_0x23_1_0x23_9_bit0 -x_0x23_1_0x23_8_bit0 -x_0x23_1_0x23_6_bit0 -x_0x23_1_0x23_3_bit0 -x_0x23_1_0x23_1_bit0 -x_0x23_49_0x23_35_bit0 -x_0x23_49_0x23_33_bit0 -x_0x23_49_0x23_31_bit0 -x_0x23_49_0x23_28_bit0 -x_0x23_49_0x23_25_bit0 -x_0x23_49_0x23_24_bit0 -x_0x23_49_0x23_22_bit0 -x_0x23_49_0x23_21_bit0 -x_0x23_49_0x23_19_bit0 -x_0x23_49_0x23_17_bit0 -x_0x23_49_0x23_15_bit0 -x_0x23_49_0x23_14_bit0 -x_0x23_49_0x23_12_bit0 -x_0x23_49_0x23_10_bit0 -x_0x23_49_0x23_7_bit0 -x_0x23_49_0x23_5_bit0 -x_0x23_49_0x23_4_bit0 -x_0x23_49_0x23_2_bit0 -x_0x23_48_0x23_35_bit0 -x_0x23_48_0x23_33_bit0 -x_0x23_48_0x23_31_bit0 -x_0x23_48_0x23_28_bit0 -x_0x23_48_0x23_25_bit0 -x_0x23_48_0x23_24_bit0 -x_0x23_48_0x23_22_bit0 x_0x23_48_0x23_21_bit0 -x_0x23_48_0x23_19_bit0 -x_0x23_48_0x23_17_bit0 -x_0x23_48_0x23_15_bit0 -x_0x23_48_0x23_14_bit0 -x_0x23_48_0x23_12_bit0 -x_0x23_48_0x23_10_bit0 -x_0x23_48_0x23_7_bit0 -x_0x23_48_0x23_5_bit0 -x_0x23_48_0x23_4_bit0 -x_0x23_48_0x23_2_bit0 -x_0x23_47_0x23_35_bit0 -x_0x23_47_0x23_33_bit0 -x_0x23_47_0x23_31_bit0 -x_0x23_47_0x23_28_bit0 -x_0x23_47_0x23_25_bit0 -x_0x23_47_0x23_24_bit0 -x_0x23_47_0x23_22_bit0 -x_0x23_47_0x23_21_bit0 x_0x23_47_0x23_19_bit0 -x_0x23_47_0x23_17_bit0 -x_0x23_47_0x23_15_bit0 -x_0x23_47_0x23_14_bit0 -x_0x23_47_0x23_12_bit0 -x_0x23_47_0x23_10_bit0 -x_0x23_47_0x23_7_bit0 -x_0x23_47_0x23_5_bit0 -x_0x23_47_0x23_4_bit0 -x_0x23_47_0x23_2_bit0 -x_0x23_46_0x23_35_bit0 -x_0x23_46_0x23_33_bit0 -x_0x23_46_0x23_31_bit0 -x_0x23_46_0x23_28_bit0 -x_0x23_46_0x23_25_bit0 -x_0x23_46_0x23_24_bit0 -x_0x23_46_0x23_22_bit0 -x_0x23_46_0x23_21_bit0 -x_0x23_46_0x23_19_bit0 x_0x23_46_0x23_17_bit0 -x_0x23_46_0x23_15_bit0 -x_0x23_46_0x23_14_bit0 -x_0x23_46_0x23_12_bit0 -x_0x23_46_0x23_10_bit0 -x_0x23_46_0x23_7_bit0 -x_0x23_46_0x23_5_bit0 -x_0x23_46_0x23_4_bit0 -x_0x23_46_0x23_2_bit0 -x_0x23_45_0x23_35_bit0 -x_0x23_45_0x23_33_bit0 -x_0x23_45_0x23_31_bit0 -x_0x23_45_0x23_28_bit0 -x_0x23_45_0x23_25_bit0 -x_0x23_45_0x23_24_bit0 -x_0x23_45_0x23_22_bit0 -x_0x23_45_0x23_21_bit0 -x_0x23_45_0x23_19_bit0 -x_0x23_45_0x23_17_bit0 -x_0x23_45_0x23_15_bit0 -x_0x23_45_0x23_14_bit0 -x_0x23_45_0x23_12_bit0 -x_0x23_45_0x23_10_bit0 -x_0x23_45_0x23_7_bit0 -x_0x23_45_0x23_5_bit0 -x_0x23_45_0x23_4_bit0 -x_0x23_45_0x23_2_bit0 -x_0x23_44_0x23_35_bit0 -x_0x23_44_0x23_33_bit0 -x_0x23_44_0x23_31_bit0 -x_0x23_44_0x23_28_bit0 -x_0x23_44_0x23_25_bit0 -x_0x23_44_0x23_24_bit0 -x_0x23_44_0x23_22_bit0 -x_0x23_44_0x23_21_bit0 -x_0x23_44_0x23_19_bit0 -x_0x23_44_0x23_17_bit0 -x_0x23_44_0x23_15_bit0 -x_0x23_44_0x23_14_bit0 -x_0x23_44_0x23_12_bit0 -x_0x23_44_0x23_10_bit0 -x_0x23_44_0x23_7_bit0 -x_0x23_44_0x23_5_bit0 -x_0x23_44_0x23_4_bit0 -x_0x23_44_0x23_2_bit0 -x_0x23_43_0x23_35_bit0 -x_0x23_43_0x23_33_bit0 -x_0x23_43_0x23_31_bit0 -x_0x23_43_0x23_28_bit0 -x_0x23_43_0x23_25_bit0 -x_0x23_43_0x23_24_bit0 -x_0x23_43_0x23_22_bit0 -x_0x23_43_0x23_21_bit0 -x_0x23_43_0x23_19_bit0 -x_0x23_43_0x23_17_bit0 -x_0x23_43_0x23_15_bit0 -x_0x23_43_0x23_14_bit0 -x_0x23_43_0x23_12_bit0 -x_0x23_43_0x23_10_bit0 -x_0x23_43_0x23_7_bit0 -x_0x23_43_0x23_5_bit0 -x_0x23_43_0x23_4_bit0 -x_0x23_43_0x23_2_bit0 -x_0x23_42_0x23_35_bit0 -x_0x23_42_0x23_33_bit0 -x_0x23_42_0x23_31_bit0 -x_0x23_42_0x23_28_bit0 x_0x23_42_0x23_25_bit0 -x_0x23_42_0x23_24_bit0 -x_0x23_42_0x23_22_bit0 -x_0x23_42_0x23_21_bit0 -x_0x23_42_0x23_19_bit0 -x_0x23_42_0x23_17_bit0 -x_0x23_42_0x23_15_bit0 -x_0x23_42_0x23_14_bit0 -x_0x23_42_0x23_12_bit0 -x_0x23_42_0x23_10_bit0 -x_0x23_42_0x23_7_bit0 -x_0x23_42_0x23_5_bit0 -x_0x23_42_0x23_4_bit0 -x_0x23_42_0x23_2_bit0 -x_0x23_41_0x23_35_bit0 -x_0x23_41_0x23_33_bit0 -x_0x23_41_0x23_31_bit0 -x_0x23_41_0x23_28_bit0 -x_0x23_41_0x23_25_bit0 -x_0x23_41_0x23_24_bit0 x_0x23_41_0x23_22_bit0 -x_0x23_41_0x23_21_bit0 -x_0x23_41_0x23_19_bit0 -x_0x23_41_0x23_17_bit0 -x_0x23_41_0x23_15_bit0 -x_0x23_41_0x23_14_bit0 -x_0x23_41_0x23_12_bit0 -x_0x23_41_0x23_10_bit0 -x_0x23_41_0x23_7_bit0 -x_0x23_41_0x23_5_bit0 -x_0x23_41_0x23_4_bit0 -x_0x23_41_0x23_2_bit0 -x_0x23_40_0x23_35_bit0 -x_0x23_40_0x23_33_bit0 -x_0x23_40_0x23_31_bit0 -x_0x23_40_0x23_28_bit0 -x_0x23_40_0x23_25_bit0 -x_0x23_40_0x23_24_bit0 -x_0x23_40_0x23_22_bit0 -x_0x23_40_0x23_21_bit0 -x_0x23_40_0x23_19_bit0 -x_0x23_40_0x23_17_bit0 -x_0x23_40_0x23_15_bit0 -x_0x23_40_0x23_14_bit0 -x_0x23_40_0x23_12_bit0 -x_0x23_40_0x23_10_bit0 -x_0x23_40_0x23_7_bit0 -x_0x23_40_0x23_5_bit0 -x_0x23_40_0x23_4_bit0 -x_0x23_40_0x23_2_bit0 -x_0x23_39_0x23_35_bit0 -x_0x23_39_0x23_33_bit0 -x_0x23_39_0x23_31_bit0 -x_0x23_39_0x23_28_bit0 -x_0x23_39_0x23_25_bit0 -x_0x23_39_0x23_24_bit0 -x_0x23_39_0x23_22_bit0 -x_0x23_39_0x23_21_bit0 -x_0x23_39_0x23_19_bit0 -x_0x23_39_0x23_17_bit0 -x_0x23_39_0x23_15_bit0 -x_0x23_39_0x23_14_bit0 -x_0x23_39_0x23_12_bit0 -x_0x23_39_0x23_10_bit0 -x_0x23_39_0x23_7_bit0 -x_0x23_39_0x23_5_bit0 -x_0x23_39_0x23_4_bit0 -x_0x23_39_0x23_2_bit0 -x_0x23_38_0x23_35_bit0 -x_0x23_38_0x23_33_bit0 -x_0x23_38_0x23_31_bit0 -x_0x23_38_0x23_28_bit0 -x_0x23_38_0x23_25_bit0 -x_0x23_38_0x23_24_bit0 -x_0x23_38_0x23_22_bit0 -x_0x23_38_0x23_21_bit0 -x_0x23_38_0x23_19_bit0 -x_0x23_38_0x23_17_bit0 -x_0x23_38_0x23_15_bit0 -x_0x23_38_0x23_14_bit0 -x_0x23_38_0x23_12_bit0 -x_0x23_38_0x23_10_bit0 -x_0x23_38_0x23_7_bit0 -x_0x23_38_0x23_5_bit0 -x_0x23_38_0x23_4_bit0 -x_0x23_38_0x23_2_bit0 -x_0x23_37_0x23_35_bit0 -x_0x23_37_0x23_33_bit0 -x_0x23_37_0x23_31_bit0 -x_0x23_37_0x23_28_bit0 -x_0x23_37_0x23_25_bit0 -x_0x23_37_0x23_24_bit0 -x_0x23_37_0x23_22_bit0 -x_0x23_37_0x23_21_bit0 -x_0x23_37_0x23_19_bit0 -x_0x23_37_0x23_17_bit0 -x_0x23_37_0x23_15_bit0 -x_0x23_37_0x23_14_bit0 -x_0x23_37_0x23_12_bit0 -x_0x23_37_0x23_10_bit0 -x_0x23_37_0x23_7_bit0 -x_0x23_37_0x23_5_bit0 -x_0x23_37_0x23_4_bit0 -x_0x23_37_0x23_2_bit0 -x_0x23_36_0x23_35_bit0 -x_0x23_36_0x23_33_bit0 -x_0x23_36_0x23_31_bit0 -x_0x23_36_0x23_28_bit0 -x_0x23_36_0x23_25_bit0 -x_0x23_36_0x23_24_bit0 -x_0x23_36_0x23_22_bit0 -x_0x23_36_0x23_21_bit0 -x_0x23_36_0x23_19_bit0 -x_0x23_36_0x23_17_bit0 -x_0x23_36_0x23_15_bit0 -x_0x23_36_0x23_14_bit0 -x_0x23_36_0x23_12_bit0 -x_0x23_36_0x23_10_bit0 -x_0x23_36_0x23_7_bit0 -x_0x23_36_0x23_5_bit0 -x_0x23_36_0x23_4_bit0 -x_0x23_36_0x23_2_bit0 -x_0x23_35_0x23_35_bit0 -x_0x23_35_0x23_33_bit0 -x_0x23_35_0x23_31_bit0 -x_0x23_35_0x23_28_bit0 -x_0x23_35_0x23_25_bit0 -x_0x23_35_0x23_24_bit0 -x_0x23_35_0x23_22_bit0 -x_0x23_35_0x23_21_bit0 -x_0x23_35_0x23_19_bit0 -x_0x23_35_0x23_17_bit0 -x_0x23_35_0x23_15_bit0 -x_0x23_35_0x23_14_bit0 -x_0x23_35_0x23_12_bit0 -x_0x23_35_0x23_10_bit0 -x_0x23_35_0x23_7_bit0 -x_0x23_35_0x23_5_bit0 -x_0x23_35_0x23_4_bit0 -x_0x23_35_0x23_2_bit0 -x_0x23_34_0x23_35_bit0 -x_0x23_34_0x23_33_bit0 -x_0x23_34_0x23_31_bit0 -x_0x23_34_0x23_28_bit0 -x_0x23_34_0x23_25_bit0 x_0x23_34_0x23_24_bit0 -x_0x23_34_0x23_22_bit0 -x_0x23_34_0x23_21_bit0 -x_0x23_34_0x23_19_bit0 -x_0x23_34_0x23_17_bit0 -x_0x23_34_0x23_15_bit0 -x_0x23_34_0x23_14_bit0 -x_0x23_34_0x23_12_bit0 -x_0x23_34_0x23_10_bit0 -x_0x23_34_0x23_7_bit0 -x_0x23_34_0x23_5_bit0 -x_0x23_34_0x23_4_bit0 -x_0x23_34_0x23_2_bit0 -x_0x23_33_0x23_35_bit0 -x_0x23_33_0x23_33_bit0 -x_0x23_33_0x23_31_bit0 -x_0x23_33_0x23_28_bit0 -x_0x23_33_0x23_25_bit0 -x_0x23_33_0x23_24_bit0 -x_0x23_33_0x23_22_bit0 -x_0x23_33_0x23_21_bit0 -x_0x23_33_0x23_19_bit0 -x_0x23_33_0x23_17_bit0 -x_0x23_33_0x23_15_bit0 -x_0x23_33_0x23_14_bit0 -x_0x23_33_0x23_12_bit0 -x_0x23_33_0x23_10_bit0 -x_0x23_33_0x23_7_bit0 -x_0x23_33_0x23_5_bit0 -x_0x23_33_0x23_4_bit0 -x_0x23_33_0x23_2_bit0 -x_0x23_32_0x23_35_bit0 -x_0x23_32_0x23_33_bit0 -x_0x23_32_0x23_31_bit0 -x_0x23_32_0x23_28_bit0 -x_0x23_32_0x23_25_bit0 -x_0x23_32_0x23_24_bit0 -x_0x23_32_0x23_22_bit0 -x_0x23_32_0x23_21_bit0 -x_0x23_32_0x23_19_bit0 -x_0x23_32_0x23_17_bit0 -x_0x23_32_0x23_15_bit0 -x_0x23_32_0x23_14_bit0 -x_0x23_32_0x23_12_bit0 -x_0x23_32_0x23_10_bit0 -x_0x23_32_0x23_7_bit0 -x_0x23_32_0x23_5_bit0 -x_0x23_32_0x23_4_bit0 -x_0x23_32_0x23_2_bit0 -x_0x23_31_0x23_35_bit0 -x_0x23_31_0x23_33_bit0 -x_0x23_31_0x23_31_bit0 -x_0x23_31_0x23_28_bit0 -x_0x23_31_0x23_25_bit0 -x_0x23_31_0x23_24_bit0 -x_0x23_31_0x23_22_bit0 -x_0x23_31_0x23_21_bit0 -x_0x23_31_0x23_19_bit0 -x_0x23_31_0x23_17_bit0 -x_0x23_31_0x23_15_bit0 x_0x23_31_0x23_14_bit0 -x_0x23_31_0x23_12_bit0 -x_0x23_31_0x23_10_bit0 -x_0x23_31_0x23_7_bit0 -x_0x23_31_0x23_5_bit0 -x_0x23_31_0x23_4_bit0 -x_0x23_31_0x23_2_bit0 -x_0x23_30_0x23_35_bit0 -x_0x23_30_0x23_33_bit0 -x_0x23_30_0x23_31_bit0 -x_0x23_30_0x23_28_bit0 -x_0x23_30_0x23_25_bit0 -x_0x23_30_0x23_24_bit0 -x_0x23_30_0x23_22_bit0 -x_0x23_30_0x23_21_bit0 -x_0x23_30_0x23_19_bit0 -x_0x23_30_0x23_17_bit0 x_0x23_30_0x23_15_bit0 -x_0x23_30_0x23_14_bit0 -x_0x23_30_0x23_12_bit0 -x_0x23_30_0x23_10_bit0 -x_0x23_30_0x23_7_bit0 -x_0x23_30_0x23_5_bit0 -x_0x23_30_0x23_4_bit0 -x_0x23_30_0x23_2_bit0 -x_0x23_29_0x23_35_bit0 -x_0x23_29_0x23_33_bit0 -x_0x23_29_0x23_31_bit0 -x_0x23_29_0x23_28_bit0 -x_0x23_29_0x23_25_bit0 -x_0x23_29_0x23_24_bit0 -x_0x23_29_0x23_22_bit0 -x_0x23_29_0x23_21_bit0 -x_0x23_29_0x23_19_bit0 -x_0x23_29_0x23_17_bit0 -x_0x23_29_0x23_15_bit0 -x_0x23_29_0x23_14_bit0 -x_0x23_29_0x23_12_bit0 -x_0x23_29_0x23_10_bit0 -x_0x23_29_0x23_7_bit0 -x_0x23_29_0x23_5_bit0 -x_0x23_29_0x23_4_bit0 -x_0x23_29_0x23_2_bit0 -x_0x23_28_0x23_35_bit0 -x_0x23_28_0x23_33_bit0 -x_0x23_28_0x23_31_bit0 -x_0x23_28_0x23_28_bit0 -x_0x23_28_0x23_25_bit0 -x_0x23_28_0x23_24_bit0 -x_0x23_28_0x23_22_bit0 -x_0x23_28_0x23_21_bit0 -x_0x23_28_0x23_19_bit0 -x_0x23_28_0x23_17_bit0 -x_0x23_28_0x23_15_bit0 -x_0x23_28_0x23_14_bit0 -x_0x23_28_0x23_12_bit0 -x_0x23_28_0x23_10_bit0 -x_0x23_28_0x23_7_bit0 -x_0x23_28_0x23_5_bit0 -x_0x23_28_0x23_4_bit0 -x_0x23_28_0x23_2_bit0 -x_0x23_27_0x23_35_bit0 -x_0x23_27_0x23_33_bit0 -x_0x23_27_0x23_31_bit0 -x_0x23_27_0x23_28_bit0 -x_0x23_27_0x23_25_bit0 -x_0x23_27_0x23_24_bit0 -x_0x23_27_0x23_22_bit0 -x_0x23_27_0x23_21_bit0 -x_0x23_27_0x23_19_bit0 -x_0x23_27_0x23_17_bit0 -x_0x23_27_0x23_15_bit0 -x_0x23_27_0x23_14_bit0 -x_0x23_27_0x23_12_bit0 -x_0x23_27_0x23_10_bit0 -x_0x23_27_0x23_7_bit0 -x_0x23_27_0x23_5_bit0 -x_0x23_27_0x23_4_bit0 -x_0x23_27_0x23_2_bit0 -x_0x23_26_0x23_35_bit0 -x_0x23_26_0x23_33_bit0 -x_0x23_26_0x23_31_bit0 -x_0x23_26_0x23_28_bit0 -x_0x23_26_0x23_25_bit0 -x_0x23_26_0x23_24_bit0 -x_0x23_26_0x23_22_bit0 -x_0x23_26_0x23_21_bit0 -x_0x23_26_0x23_19_bit0 -x_0x23_26_0x23_17_bit0 -x_0x23_26_0x23_15_bit0 -x_0x23_26_0x23_14_bit0 -x_0x23_26_0x23_12_bit0 x_0x23_26_0x23_10_bit0 -x_0x23_26_0x23_7_bit0 -x_0x23_26_0x23_5_bit0 -x_0x23_26_0x23_4_bit0 -x_0x23_26_0x23_2_bit0 -x_0x23_25_0x23_35_bit0 -x_0x23_25_0x23_33_bit0 -x_0x23_25_0x23_31_bit0 -x_0x23_25_0x23_28_bit0 -x_0x23_25_0x23_25_bit0 -x_0x23_25_0x23_24_bit0 -x_0x23_25_0x23_22_bit0 -x_0x23_25_0x23_21_bit0 -x_0x23_25_0x23_19_bit0 -x_0x23_25_0x23_17_bit0 -x_0x23_25_0x23_15_bit0 -x_0x23_25_0x23_14_bit0 -x_0x23_25_0x23_12_bit0 -x_0x23_25_0x23_10_bit0 -x_0x23_25_0x23_7_bit0 -x_0x23_25_0x23_5_bit0 -x_0x23_25_0x23_4_bit0 -x_0x23_25_0x23_2_bit0 -x_0x23_24_0x23_35_bit0 -x_0x23_24_0x23_33_bit0 -x_0x23_24_0x23_31_bit0 -x_0x23_24_0x23_28_bit0 -x_0x23_24_0x23_25_bit0 -x_0x23_24_0x23_24_bit0 -x_0x23_24_0x23_22_bit0 -x_0x23_24_0x23_21_bit0 -x_0x23_24_0x23_19_bit0 -x_0x23_24_0x23_17_bit0 -x_0x23_24_0x23_15_bit0 -x_0x23_24_0x23_14_bit0 x_0x23_24_0x23_12_bit0 -x_0x23_24_0x23_10_bit0 -x_0x23_24_0x23_7_bit0 -x_0x23_24_0x23_5_bit0 -x_0x23_24_0x23_4_bit0 -x_0x23_24_0x23_2_bit0 -x_0x23_23_0x23_35_bit0 -x_0x23_23_0x23_33_bit0 -x_0x23_23_0x23_31_bit0 -x_0x23_23_0x23_28_bit0 -x_0x23_23_0x23_25_bit0 -x_0x23_23_0x23_24_bit0 -x_0x23_23_0x23_22_bit0 -x_0x23_23_0x23_21_bit0 -x_0x23_23_0x23_19_bit0 -x_0x23_23_0x23_17_bit0 -x_0x23_23_0x23_15_bit0 -x_0x23_23_0x23_14_bit0 -x_0x23_23_0x23_12_bit0 -x_0x23_23_0x23_10_bit0 -x_0x23_23_0x23_7_bit0 -x_0x23_23_0x23_5_bit0 -x_0x23_23_0x23_4_bit0 -x_0x23_23_0x23_2_bit0 -x_0x23_22_0x23_35_bit0 -x_0x23_22_0x23_33_bit0 -x_0x23_22_0x23_31_bit0 -x_0x23_22_0x23_28_bit0 -x_0x23_22_0x23_25_bit0 -x_0x23_22_0x23_24_bit0 -x_0x23_22_0x23_22_bit0 -x_0x23_22_0x23_21_bit0 -x_0x23_22_0x23_19_bit0 -x_0x23_22_0x23_17_bit0 -x_0x23_22_0x23_15_bit0 -x_0x23_22_0x23_14_bit0 -x_0x23_22_0x23_12_bit0 -x_0x23_22_0x23_10_bit0 -x_0x23_22_0x23_7_bit0 -x_0x23_22_0x23_5_bit0 -x_0x23_22_0x23_4_bit0 -x_0x23_22_0x23_2_bit0 -x_0x23_21_0x23_35_bit0 -x_0x23_21_0x23_33_bit0 -x_0x23_21_0x23_31_bit0 x_0x23_21_0x23_28_bit0 -x_0x23_21_0x23_25_bit0 -x_0x23_21_0x23_24_bit0 -x_0x23_21_0x23_22_bit0 -x_0x23_21_0x23_21_bit0 -x_0x23_21_0x23_19_bit0 -x_0x23_21_0x23_17_bit0 -x_0x23_21_0x23_15_bit0 -x_0x23_21_0x23_14_bit0 -x_0x23_21_0x23_12_bit0 -x_0x23_21_0x23_10_bit0 -x_0x23_21_0x23_7_bit0 -x_0x23_21_0x23_5_bit0 -x_0x23_21_0x23_4_bit0 -x_0x23_21_0x23_2_bit0 -x_0x23_20_0x23_35_bit0 -x_0x23_20_0x23_33_bit0 -x_0x23_20_0x23_31_bit0 -x_0x23_20_0x23_28_bit0 -x_0x23_20_0x23_25_bit0 -x_0x23_20_0x23_24_bit0 -x_0x23_20_0x23_22_bit0 -x_0x23_20_0x23_21_bit0 -x_0x23_20_0x23_19_bit0 -x_0x23_20_0x23_17_bit0 -x_0x23_20_0x23_15_bit0 -x_0x23_20_0x23_14_bit0 -x_0x23_20_0x23_12_bit0 -x_0x23_20_0x23_10_bit0 -x_0x23_20_0x23_7_bit0 -x_0x23_20_0x23_5_bit0 -x_0x23_20_0x23_4_bit0 x_0x23_20_0x23_2_bit0 -x_0x23_19_0x23_35_bit0 -x_0x23_19_0x23_33_bit0 -x_0x23_19_0x23_31_bit0 -x_0x23_19_0x23_28_bit0 -x_0x23_19_0x23_25_bit0 -x_0x23_19_0x23_24_bit0 -x_0x23_19_0x23_22_bit0 -x_0x23_19_0x23_21_bit0 -x_0x23_19_0x23_19_bit0 -x_0x23_19_0x23_17_bit0 -x_0x23_19_0x23_15_bit0 -x_0x23_19_0x23_14_bit0 -x_0x23_19_0x23_12_bit0 -x_0x23_19_0x23_10_bit0 -x_0x23_19_0x23_7_bit0 -x_0x23_19_0x23_5_bit0 -x_0x23_19_0x23_4_bit0 -x_0x23_19_0x23_2_bit0 -x_0x23_18_0x23_35_bit0 -x_0x23_18_0x23_33_bit0 -x_0x23_18_0x23_31_bit0 -x_0x23_18_0x23_28_bit0 -x_0x23_18_0x23_25_bit0 -x_0x23_18_0x23_24_bit0 -x_0x23_18_0x23_22_bit0 -x_0x23_18_0x23_21_bit0 -x_0x23_18_0x23_19_bit0 -x_0x23_18_0x23_17_bit0 -x_0x23_18_0x23_15_bit0 -x_0x23_18_0x23_14_bit0 -x_0x23_18_0x23_12_bit0 -x_0x23_18_0x23_10_bit0 -x_0x23_18_0x23_7_bit0 -x_0x23_18_0x23_5_bit0 -x_0x23_18_0x23_4_bit0 -x_0x23_18_0x23_2_bit0 -x_0x23_17_0x23_35_bit0 -x_0x23_17_0x23_33_bit0 -x_0x23_17_0x23_31_bit0 -x_0x23_17_0x23_28_bit0 -x_0x23_17_0x23_25_bit0 -x_0x23_17_0x23_24_bit0 -x_0x23_17_0x23_22_bit0 -x_0x23_17_0x23_21_bit0 -x_0x23_17_0x23_19_bit0 -x_0x23_17_0x23_17_bit0 -x_0x23_17_0x23_15_bit0 -x_0x23_17_0x23_14_bit0 -x_0x23_17_0x23_12_bit0 -x_0x23_17_0x23_10_bit0 -x_0x23_17_0x23_7_bit0 -x_0x23_17_0x23_5_bit0 -x_0x23_17_0x23_4_bit0 -x_0x23_17_0x23_2_bit0 -x_0x23_16_0x23_35_bit0 -x_0x23_16_0x23_33_bit0 -x_0x23_16_0x23_31_bit0 -x_0x23_16_0x23_28_bit0 -x_0x23_16_0x23_25_bit0 -x_0x23_16_0x23_24_bit0 -x_0x23_16_0x23_22_bit0 -x_0x23_16_0x23_21_bit0 -x_0x23_16_0x23_19_bit0 -x_0x23_16_0x23_17_bit0 -x_0x23_16_0x23_15_bit0 -x_0x23_16_0x23_14_bit0 -x_0x23_16_0x23_12_bit0 -x_0x23_16_0x23_10_bit0 -x_0x23_16_0x23_7_bit0 -x_0x23_16_0x23_5_bit0 -x_0x23_16_0x23_4_bit0 -x_0x23_16_0x23_2_bit0 -x_0x23_15_0x23_35_bit0 -x_0x23_15_0x23_33_bit0 -x_0x23_15_0x23_31_bit0 -x_0x23_15_0x23_28_bit0 -x_0x23_15_0x23_25_bit0 -x_0x23_15_0x23_24_bit0 -x_0x23_15_0x23_22_bit0 -x_0x23_15_0x23_21_bit0 -x_0x23_15_0x23_19_bit0 -x_0x23_15_0x23_17_bit0 -x_0x23_15_0x23_15_bit0 -x_0x23_15_0x23_14_bit0 -x_0x23_15_0x23_12_bit0 -x_0x23_15_0x23_10_bit0 -x_0x23_15_0x23_7_bit0 -x_0x23_15_0x23_5_bit0 -x_0x23_15_0x23_4_bit0 -x_0x23_15_0x23_2_bit0 -x_0x23_14_0x23_35_bit0 -x_0x23_14_0x23_33_bit0 -x_0x23_14_0x23_31_bit0 -x_0x23_14_0x23_28_bit0 -x_0x23_14_0x23_25_bit0 -x_0x23_14_0x23_24_bit0 -x_0x23_14_0x23_22_bit0 -x_0x23_14_0x23_21_bit0 -x_0x23_14_0x23_19_bit0 -x_0x23_14_0x23_17_bit0 -x_0x23_14_0x23_15_bit0 -x_0x23_14_0x23_14_bit0 -x_0x23_14_0x23_12_bit0 -x_0x23_14_0x23_10_bit0 -x_0x23_14_0x23_7_bit0 -x_0x23_14_0x23_5_bit0 -x_0x23_14_0x23_4_bit0 -x_0x23_14_0x23_2_bit0 -x_0x23_13_0x23_35_bit0 -x_0x23_13_0x23_33_bit0 -x_0x23_13_0x23_31_bit0 -x_0x23_13_0x23_28_bit0 -x_0x23_13_0x23_25_bit0 -x_0x23_13_0x23_24_bit0 -x_0x23_13_0x23_22_bit0 -x_0x23_13_0x23_21_bit0 -x_0x23_13_0x23_19_bit0 -x_0x23_13_0x23_17_bit0 -x_0x23_13_0x23_15_bit0 -x_0x23_13_0x23_14_bit0 -x_0x23_13_0x23_12_bit0 -x_0x23_13_0x23_10_bit0 -x_0x23_13_0x23_7_bit0 -x_0x23_13_0x23_5_bit0 -x_0x23_13_0x23_4_bit0 -x_0x23_13_0x23_2_bit0 -x_0x23_12_0x23_35_bit0 -x_0x23_12_0x23_33_bit0 -x_0x23_12_0x23_31_bit0 -x_0x23_12_0x23_28_bit0 -x_0x23_12_0x23_25_bit0 -x_0x23_12_0x23_24_bit0 -x_0x23_12_0x23_22_bit0 -x_0x23_12_0x23_21_bit0 -x_0x23_12_0x23_19_bit0 -x_0x23_12_0x23_17_bit0 -x_0x23_12_0x23_15_bit0 -x_0x23_12_0x23_14_bit0 -x_0x23_12_0x23_12_bit0 -x_0x23_12_0x23_10_bit0 -x_0x23_12_0x23_7_bit0 -x_0x23_12_0x23_5_bit0 x_0x23_12_0x23_4_bit0 -x_0x23_12_0x23_2_bit0 -x_0x23_11_0x23_35_bit0 -x_0x23_11_0x23_33_bit0 -x_0x23_11_0x23_31_bit0 -x_0x23_11_0x23_28_bit0 -x_0x23_11_0x23_25_bit0 -x_0x23_11_0x23_24_bit0 -x_0x23_11_0x23_22_bit0 -x_0x23_11_0x23_21_bit0 -x_0x23_11_0x23_19_bit0 -x_0x23_11_0x23_17_bit0 -x_0x23_11_0x23_15_bit0 -x_0x23_11_0x23_14_bit0 -x_0x23_11_0x23_12_bit0 -x_0x23_11_0x23_10_bit0 -x_0x23_11_0x23_7_bit0 x_0x23_11_0x23_5_bit0 -x_0x23_11_0x23_4_bit0 -x_0x23_11_0x23_2_bit0 -x_0x23_10_0x23_35_bit0 -x_0x23_10_0x23_33_bit0 -x_0x23_10_0x23_31_bit0 -x_0x23_10_0x23_28_bit0 -x_0x23_10_0x23_25_bit0 -x_0x23_10_0x23_24_bit0 -x_0x23_10_0x23_22_bit0 -x_0x23_10_0x23_21_bit0 -x_0x23_10_0x23_19_bit0 -x_0x23_10_0x23_17_bit0 -x_0x23_10_0x23_15_bit0 -x_0x23_10_0x23_14_bit0 -x_0x23_10_0x23_12_bit0 -x_0x23_10_0x23_10_bit0 -x_0x23_10_0x23_7_bit0 -x_0x23_10_0x23_5_bit0 -x_0x23_10_0x23_4_bit0 -x_0x23_10_0x23_2_bit0 -x_0x23_9_0x23_35_bit0 -x_0x23_9_0x23_33_bit0 -x_0x23_9_0x23_31_bit0 -x_0x23_9_0x23_28_bit0 -x_0x23_9_0x23_25_bit0 -x_0x23_9_0x23_24_bit0 -x_0x23_9_0x23_22_bit0 -x_0x23_9_0x23_21_bit0 -x_0x23_9_0x23_19_bit0 -x_0x23_9_0x23_17_bit0 -x_0x23_9_0x23_15_bit0 -x_0x23_9_0x23_14_bit0 -x_0x23_9_0x23_12_bit0 -x_0x23_9_0x23_10_bit0 x_0x23_9_0x23_7_bit0 -x_0x23_9_0x23_5_bit0 -x_0x23_9_0x23_4_bit0 -x_0x23_9_0x23_2_bit0 -x_0x23_8_0x23_35_bit0 -x_0x23_8_0x23_33_bit0 -x_0x23_8_0x23_31_bit0 -x_0x23_8_0x23_28_bit0 -x_0x23_8_0x23_25_bit0 -x_0x23_8_0x23_24_bit0 -x_0x23_8_0x23_22_bit0 -x_0x23_8_0x23_21_bit0 -x_0x23_8_0x23_19_bit0 -x_0x23_8_0x23_17_bit0 -x_0x23_8_0x23_15_bit0 -x_0x23_8_0x23_14_bit0 -x_0x23_8_0x23_12_bit0 -x_0x23_8_0x23_10_bit0 -x_0x23_8_0x23_7_bit0 -x_0x23_8_0x23_5_bit0 -x_0x23_8_0x23_4_bit0 -x_0x23_8_0x23_2_bit0 -x_0x23_7_0x23_35_bit0 -x_0x23_7_0x23_33_bit0 -x_0x23_7_0x23_31_bit0 -x_0x23_7_0x23_28_bit0 -x_0x23_7_0x23_25_bit0 -x_0x23_7_0x23_24_bit0 -x_0x23_7_0x23_22_bit0 -x_0x23_7_0x23_21_bit0 -x_0x23_7_0x23_19_bit0 -x_0x23_7_0x23_17_bit0 -x_0x23_7_0x23_15_bit0 -x_0x23_7_0x23_14_bit0 -x_0x23_7_0x23_12_bit0 -x_0x23_7_0x23_10_bit0 -x_0x23_7_0x23_7_bit0 -x_0x23_7_0x23_5_bit0 -x_0x23_7_0x23_4_bit0 -x_0x23_7_0x23_2_bit0 -x_0x23_6_0x23_35_bit0 -x_0x23_6_0x23_33_bit0 x_0x23_6_0x23_31_bit0 -x_0x23_6_0x23_28_bit0 -x_0x23_6_0x23_25_bit0 -x_0x23_6_0x23_24_bit0 -x_0x23_6_0x23_22_bit0 -x_0x23_6_0x23_21_bit0
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/31259/stat): 31259 (minisat+_script) R 31258 31259 19316 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846820111 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/31259/statm): 174 3 169 147 0 27 0 [pid=31259] 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=31260 New process pid=31261 New process pid=31262 execve syscall for /bin/sed executable One traced child (pid=31261) 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=31262) exited with status: 0 One traced child (pid=31260) exited with status: 0 New process pid=31263 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-protfold.opb [startup+10.004 s] Raw data (loadavg): 0.93 0.95 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 3334 0 0 0 962 16 0 0 25 0 1 0 1846820116 14024704 3155 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31263/statm): 3424 3155 145 145 0 3279 0 [pid=31263] vsize: 13696 Current children cumulated CPU time (s) 9.8 Current children cumulated vsize (Kb) 15820 [startup+20.0046 s] Raw data (loadavg): 0.94 0.96 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 3947 0 0 0 1953 21 0 0 25 0 1 0 1846820116 16539648 3768 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 4038 3768 145 145 0 3893 0 [pid=31263] vsize: 16152 Current children cumulated CPU time (s) 19.76 Current children cumulated vsize (Kb) 18276 [startup+30.0063 s] Raw data (loadavg): 0.95 0.96 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 4562 0 0 0 2940 27 0 0 25 0 1 0 1846820116 19079168 4383 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31263/statm): 4658 4383 145 145 0 4513 0 [pid=31263] vsize: 18632 Current children cumulated CPU time (s) 29.69 Current children cumulated vsize (Kb) 20756 [startup+40.0068 s] Raw data (loadavg): 0.95 0.96 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 5175 0 0 0 3928 32 0 0 25 0 1 0 1846820116 21573632 4996 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 5267 4996 145 145 0 5122 0 [pid=31263] vsize: 21068 Current children cumulated CPU time (s) 39.62 Current children cumulated vsize (Kb) 23192 [startup+50.0074 s] Raw data (loadavg): 0.96 0.96 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 5746 0 0 0 4916 36 0 0 25 0 1 0 1846820116 23904256 5567 4294967295 134512640 135094434 3221224432 3221223084 134556676 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 5836 5567 145 145 0 5691 0 [pid=31263] vsize: 23344 Current children cumulated CPU time (s) 49.54 Current children cumulated vsize (Kb) 25468 [startup+60.008 s] Raw data (loadavg): 0.97 0.96 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 6290 0 0 0 5908 40 0 0 25 0 1 0 1846820116 26185728 6111 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 6393 6111 145 145 0 6248 0 [pid=31263] vsize: 25572 Current children cumulated CPU time (s) 59.5 Current children cumulated vsize (Kb) 27696 [startup+70.0086 s] Raw data (loadavg): 0.97 0.96 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 6890 0 0 0 6898 44 0 0 25 0 1 0 1846820116 28643328 6711 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 6993 6711 145 145 0 6848 0 [pid=31263] vsize: 27972 Current children cumulated CPU time (s) 69.44 Current children cumulated vsize (Kb) 30096 [startup+80.0092 s] Raw data (loadavg): 0.98 0.96 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 7492 0 0 0 7891 46 0 0 25 0 1 0 1846820116 31100928 7313 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 7593 7313 145 145 0 7448 0 [pid=31263] vsize: 30372 Current children cumulated CPU time (s) 79.39 Current children cumulated vsize (Kb) 32496 [startup+90.0098 s] Raw data (loadavg): 0.98 0.96 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 8023 0 0 0 8883 50 0 0 25 0 1 0 1846820116 33267712 7844 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 8122 7844 145 145 0 7977 0 [pid=31263] vsize: 32488 Current children cumulated CPU time (s) 89.35 Current children cumulated vsize (Kb) 34612 [startup+100.01 s] Raw data (loadavg): 0.98 0.96 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 8527 0 0 0 9876 53 0 0 25 0 1 0 1846820116 35332096 8348 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 8626 8348 145 145 0 8481 0 [pid=31263] vsize: 34504 Current children cumulated CPU time (s) 99.31 Current children cumulated vsize (Kb) 36628 [startup+110.011 s] Raw data (loadavg): 0.98 0.96 0.97 1/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) T 31259 31259 19316 0 -1 0 9040 0 0 0 10865 57 0 0 25 0 1 0 1846820116 37421056 8861 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/31263/statm): 9136 8861 145 145 0 8991 0 [pid=31263] vsize: 36544 Current children cumulated CPU time (s) 109.24 Current children cumulated vsize (Kb) 38668 [startup+120.012 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 9529 0 0 0 11856 61 0 0 25 0 1 0 1846820116 39411712 9350 4294967295 134512640 135094434 3221224432 3221223024 134557366 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 9622 9350 145 145 0 9477 0 [pid=31263] vsize: 38488 Current children cumulated CPU time (s) 119.19 Current children cumulated vsize (Kb) 40612 [startup+130.012 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 10056 0 0 0 12846 65 0 0 25 0 1 0 1846820116 41697280 9877 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 10180 9877 145 145 0 10035 0 [pid=31263] vsize: 40720 Current children cumulated CPU time (s) 129.13 Current children cumulated vsize (Kb) 42844 [startup+140.013 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 10632 0 0 0 13836 70 0 0 25 0 1 0 1846820116 44048384 10453 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 10754 10453 145 145 0 10609 0 [pid=31263] vsize: 43016 Current children cumulated CPU time (s) 139.08 Current children cumulated vsize (Kb) 45140 [startup+150.013 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 11128 0 0 0 14826 74 0 0 25 0 1 0 1846820116 46067712 10949 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 11247 10949 145 145 0 11102 0 [pid=31263] vsize: 44988 Current children cumulated CPU time (s) 149.02 Current children cumulated vsize (Kb) 47112 [startup+160.014 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 11537 0 0 0 15818 77 0 0 25 0 1 0 1846820116 47734784 11358 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 11654 11358 145 145 0 11509 0 [pid=31263] vsize: 46616 Current children cumulated CPU time (s) 158.97 Current children cumulated vsize (Kb) 48740 [startup+170.014 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 12246 0 0 0 16808 82 0 0 25 0 1 0 1846820116 50626560 12067 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 12360 12067 145 145 0 12215 0 [pid=31263] vsize: 49440 Current children cumulated CPU time (s) 168.92 Current children cumulated vsize (Kb) 51564 [startup+180.014 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 12892 0 0 0 17799 85 0 0 25 0 1 0 1846820116 53268480 12713 4294967295 134512640 135094434 3221224432 3221223056 134557648 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 13005 12713 145 145 0 12860 0 [pid=31263] vsize: 52020 Current children cumulated CPU time (s) 178.86 Current children cumulated vsize (Kb) 54144 [startup+190.015 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 13481 0 0 0 18790 90 0 0 25 0 1 0 1846820116 55672832 13302 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 13592 13302 145 145 0 13447 0 [pid=31263] vsize: 54368 Current children cumulated CPU time (s) 188.82 Current children cumulated vsize (Kb) 56492 [startup+200.014 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 14040 0 0 0 19782 93 0 0 25 0 1 0 1846820116 57958400 13861 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 14150 13861 145 145 0 14005 0 [pid=31263] vsize: 56600 Current children cumulated CPU time (s) 198.77 Current children cumulated vsize (Kb) 58724 [startup+210.015 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 14587 0 0 0 20774 96 0 0 25 0 1 0 1846820116 60190720 14408 4294967295 134512640 135094434 3221224432 3221223088 134557843 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 14695 14408 145 145 0 14550 0 [pid=31263] vsize: 58780 Current children cumulated CPU time (s) 208.72 Current children cumulated vsize (Kb) 60904 [startup+220.016 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 15095 0 0 0 21767 99 0 0 25 0 1 0 1846820116 62283776 14916 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 15206 14916 145 145 0 15061 0 [pid=31263] vsize: 60824 Current children cumulated CPU time (s) 218.68 Current children cumulated vsize (Kb) 62948 [startup+230.016 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 15583 0 0 0 22759 102 0 0 25 0 1 0 1846820116 64290816 15404 4294967295 134512640 135094434 3221224432 3221223024 134557328 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 15696 15404 145 145 0 15551 0 [pid=31263] vsize: 62784 Current children cumulated CPU time (s) 228.63 Current children cumulated vsize (Kb) 64908 [startup+240.017 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 16096 0 0 0 23752 105 0 0 25 0 1 0 1846820116 66400256 15917 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 16211 15917 145 145 0 16066 0 [pid=31263] vsize: 64844 Current children cumulated CPU time (s) 238.59 Current children cumulated vsize (Kb) 66968 [startup+250.017 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 16578 0 0 0 24744 109 0 0 25 0 1 0 1846820116 68382720 16399 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 16695 16399 145 145 0 16550 0 [pid=31263] vsize: 66780 Current children cumulated CPU time (s) 248.55 Current children cumulated vsize (Kb) 68904 [startup+260.018 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 17054 0 0 0 25737 112 0 0 25 0 1 0 1846820116 70328320 16875 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 17170 16875 145 145 0 17025 0 [pid=31263] vsize: 68680 Current children cumulated CPU time (s) 258.51 Current children cumulated vsize (Kb) 70804 [startup+270.019 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 17604 0 0 0 26729 115 0 0 25 0 1 0 1846820116 72572928 17425 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 17718 17425 145 145 0 17573 0 [pid=31263] vsize: 70872 Current children cumulated CPU time (s) 268.46 Current children cumulated vsize (Kb) 72996 [startup+280.02 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 18104 0 0 0 27720 119 0 0 25 0 1 0 1846820116 74620928 17925 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 18218 17925 145 145 0 18073 0 [pid=31263] vsize: 72872 Current children cumulated CPU time (s) 278.41 Current children cumulated vsize (Kb) 74996 [startup+290.021 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 18511 0 0 0 28711 122 0 0 25 0 1 0 1846820116 76292096 18332 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 18626 18332 145 145 0 18481 0 [pid=31263] vsize: 74504 Current children cumulated CPU time (s) 288.35 Current children cumulated vsize (Kb) 76628 [startup+300.022 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 18834 0 0 0 29704 125 0 0 25 0 1 0 1846820116 77606912 18655 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 18947 18655 145 145 0 18802 0 [pid=31263] vsize: 75788 Current children cumulated CPU time (s) 298.31 Current children cumulated vsize (Kb) 77912 [startup+310.022 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 19183 0 0 0 30696 128 0 0 25 0 1 0 1846820116 79028224 19004 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 19294 19004 145 145 0 19149 0 [pid=31263] vsize: 77176 Current children cumulated CPU time (s) 308.26 Current children cumulated vsize (Kb) 79300 [startup+320.022 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 19518 0 0 0 31690 131 0 0 25 0 1 0 1846820116 80654336 19339 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 19691 19339 145 145 0 19546 0 [pid=31263] vsize: 78764 Current children cumulated CPU time (s) 318.23 Current children cumulated vsize (Kb) 80888 [startup+330.023 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 19816 0 0 0 32685 133 0 0 25 0 1 0 1846820116 81862656 19637 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 19986 19637 145 145 0 19841 0 [pid=31263] vsize: 79944 Current children cumulated CPU time (s) 328.2 Current children cumulated vsize (Kb) 82068 [startup+340.024 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 20092 0 0 0 33679 136 0 0 25 0 1 0 1846820116 82997248 19913 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 20263 19913 145 145 0 20118 0 [pid=31263] vsize: 81052 Current children cumulated CPU time (s) 338.17 Current children cumulated vsize (Kb) 83176 [startup+350.024 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 20364 0 0 0 34675 138 0 0 25 0 1 0 1846820116 84099072 20185 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 20532 20185 145 145 0 20387 0 [pid=31263] vsize: 82128 Current children cumulated CPU time (s) 348.15 Current children cumulated vsize (Kb) 84252 [startup+360.024 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 20613 0 0 0 35670 139 0 0 25 0 1 0 1846820116 85118976 20434 4294967295 134512640 135094434 3221224432 3221223120 134554793 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 20781 20434 145 145 0 20636 0 [pid=31263] vsize: 83124 Current children cumulated CPU time (s) 358.11 Current children cumulated vsize (Kb) 85248 [startup+370.025 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 20883 0 0 0 36663 142 0 0 25 0 1 0 1846820116 86216704 20704 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 21049 20704 145 145 0 20904 0 [pid=31263] vsize: 84196 Current children cumulated CPU time (s) 368.07 Current children cumulated vsize (Kb) 86320 [startup+380.025 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 21160 0 0 0 37657 145 0 0 25 0 1 0 1846820116 87351296 20981 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 21326 20981 145 145 0 21181 0 [pid=31263] vsize: 85304 Current children cumulated CPU time (s) 378.04 Current children cumulated vsize (Kb) 87428 [startup+390.026 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 21431 0 0 0 38651 147 0 0 25 0 1 0 1846820116 88465408 21252 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31263/statm): 21598 21252 145 145 0 21453 0 [pid=31263] vsize: 86392 Current children cumulated CPU time (s) 388 Current children cumulated vsize (Kb) 88516 [startup+400.027 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 21669 0 0 0 39647 149 0 0 25 0 1 0 1846820116 89448448 21490 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31263/statm): 21838 21490 145 145 0 21693 0 [pid=31263] vsize: 87352 Current children cumulated CPU time (s) 397.98 Current children cumulated vsize (Kb) 89476 [startup+410.027 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 21951 0 0 0 40640 152 0 0 25 0 1 0 1846820116 90607616 21772 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31263/statm): 22121 21772 145 145 0 21976 0 [pid=31263] vsize: 88484 Current children cumulated CPU time (s) 407.94 Current children cumulated vsize (Kb) 90608 [startup+420.028 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 22216 0 0 0 41634 154 0 0 25 0 1 0 1846820116 91701248 22037 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31263/statm): 22388 22037 145 145 0 22243 0 [pid=31263] vsize: 89552 Current children cumulated CPU time (s) 417.9 Current children cumulated vsize (Kb) 91676 [startup+430.029 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 22468 0 0 0 42629 157 0 0 25 0 1 0 1846820116 92749824 22289 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 22644 22289 145 145 0 22499 0 [pid=31263] vsize: 90576 Current children cumulated CPU time (s) 427.88 Current children cumulated vsize (Kb) 92700 [startup+440.03 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 22709 0 0 0 43624 159 0 0 25 0 1 0 1846820116 93728768 22530 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 22883 22530 145 145 0 22738 0 [pid=31263] vsize: 91532 Current children cumulated CPU time (s) 437.85 Current children cumulated vsize (Kb) 93656 [startup+450.031 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 22936 0 0 0 44619 161 0 0 25 0 1 0 1846820116 94683136 22757 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 23116 22757 145 145 0 22971 0 [pid=31263] vsize: 92464 Current children cumulated CPU time (s) 447.82 Current children cumulated vsize (Kb) 94588 [startup+460.031 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 23171 0 0 0 45615 163 0 0 25 0 1 0 1846820116 95645696 22992 4294967295 134512640 135094434 3221224432 3221223056 134557587 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 23351 22992 145 145 0 23206 0 [pid=31263] vsize: 93404 Current children cumulated CPU time (s) 457.8 Current children cumulated vsize (Kb) 95528 [startup+470.032 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 23449 0 0 0 46608 166 0 0 25 0 1 0 1846820116 96772096 23270 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31263/statm): 23626 23270 145 145 0 23481 0 [pid=31263] vsize: 94504 Current children cumulated CPU time (s) 467.76 Current children cumulated vsize (Kb) 96628 [startup+480.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 23677 0 0 0 47604 168 0 0 25 0 1 0 1846820116 97726464 23498 4294967295 134512640 135094434 3221224432 3221223024 134557178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 23859 23498 145 145 0 23714 0 [pid=31263] vsize: 95436 Current children cumulated CPU time (s) 477.74 Current children cumulated vsize (Kb) 97560 [startup+490.034 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 23895 0 0 0 48600 170 0 0 25 0 1 0 1846820116 98611200 23716 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 24075 23716 145 145 0 23930 0 [pid=31263] vsize: 96300 Current children cumulated CPU time (s) 487.72 Current children cumulated vsize (Kb) 98424 [startup+500.035 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 24229 0 0 0 49594 173 0 0 25 0 1 0 1846820116 99975168 24050 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 24408 24050 145 145 0 24263 0 [pid=31263] vsize: 97632 Current children cumulated CPU time (s) 497.69 Current children cumulated vsize (Kb) 99756 [startup+510.035 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 24486 0 0 0 50589 175 0 0 25 0 1 0 1846820116 101027840 24307 4294967295 134512640 135094434 3221224432 3221223104 134555753 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 24665 24307 145 145 0 24520 0 [pid=31263] vsize: 98660 Current children cumulated CPU time (s) 507.66 Current children cumulated vsize (Kb) 100784 [startup+520.036 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 24732 0 0 0 51584 178 0 0 25 0 1 0 1846820116 102035456 24553 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 24911 24553 145 145 0 24766 0 [pid=31263] vsize: 99644 Current children cumulated CPU time (s) 517.64 Current children cumulated vsize (Kb) 101768 [startup+530.036 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 24987 0 0 0 52581 180 0 0 25 0 1 0 1846820116 103075840 24808 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 25165 24808 145 145 0 25020 0 [pid=31263] vsize: 100660 Current children cumulated CPU time (s) 527.63 Current children cumulated vsize (Kb) 102784 [startup+540.037 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 25250 0 0 0 53576 181 0 0 25 0 1 0 1846820116 104144896 25071 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 25426 25071 145 145 0 25281 0 [pid=31263] vsize: 101704 Current children cumulated CPU time (s) 537.59 Current children cumulated vsize (Kb) 103828 [startup+550.037 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 25504 0 0 0 54571 184 0 0 25 0 1 0 1846820116 105177088 25325 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 25678 25325 145 145 0 25533 0 [pid=31263] vsize: 102712 Current children cumulated CPU time (s) 547.57 Current children cumulated vsize (Kb) 104836 [startup+560.037 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 25732 0 0 0 55567 185 0 0 25 0 1 0 1846820116 106131456 25553 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 25911 25553 145 145 0 25766 0 [pid=31263] vsize: 103644 Current children cumulated CPU time (s) 557.54 Current children cumulated vsize (Kb) 105768 [startup+570.038 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 25929 0 0 0 56563 187 0 0 25 0 1 0 1846820116 106942464 25750 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26109 25750 145 145 0 25964 0 [pid=31263] vsize: 104436 Current children cumulated CPU time (s) 567.52 Current children cumulated vsize (Kb) 106560 [startup+580.038 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26159 0 0 0 57560 189 0 0 25 0 1 0 1846820116 107888640 25980 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26340 25980 145 145 0 26195 0 [pid=31263] vsize: 105360 Current children cumulated CPU time (s) 577.51 Current children cumulated vsize (Kb) 107484 [startup+590.039 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26360 0 0 0 58558 189 0 0 25 0 1 0 1846820116 108707840 26181 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26540 26181 145 145 0 26395 0 [pid=31263] vsize: 106160 Current children cumulated CPU time (s) 587.49 Current children cumulated vsize (Kb) 108284 [startup+600.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26565 0 0 0 59554 191 0 0 25 0 1 0 1846820116 109547520 26386 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26745 26386 145 145 0 26600 0 [pid=31263] vsize: 106980 Current children cumulated CPU time (s) 597.47 Current children cumulated vsize (Kb) 109104 [startup+610.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26572 0 0 0 60555 191 0 0 25 0 1 0 1846820116 109572096 26393 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26393 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 607.48 Current children cumulated vsize (Kb) 109128 [startup+620.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26573 0 0 0 61555 191 0 0 25 0 1 0 1846820116 109572096 26394 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26394 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 617.48 Current children cumulated vsize (Kb) 109128 [startup+630.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26573 0 0 0 62555 191 0 0 25 0 1 0 1846820116 109572096 26394 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26394 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 627.48 Current children cumulated vsize (Kb) 109128 [startup+640.041 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26574 0 0 0 63555 191 0 0 25 0 1 0 1846820116 109572096 26395 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26395 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 637.48 Current children cumulated vsize (Kb) 109128 [startup+650.042 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26574 0 0 0 64555 191 0 0 25 0 1 0 1846820116 109572096 26395 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26395 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 647.48 Current children cumulated vsize (Kb) 109128 [startup+660.042 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26574 0 0 0 65556 191 0 0 25 0 1 0 1846820116 109572096 26395 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26395 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 657.49 Current children cumulated vsize (Kb) 109128 [startup+670.043 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26574 0 0 0 66556 191 0 0 25 0 1 0 1846820116 109572096 26395 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26395 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 667.49 Current children cumulated vsize (Kb) 109128 [startup+680.043 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26574 0 0 0 67556 191 0 0 25 0 1 0 1846820116 109572096 26395 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26395 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 677.49 Current children cumulated vsize (Kb) 109128 [startup+690.044 s] Raw data (loadavg): 1.07 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26574 0 0 0 68676 192 0 0 25 0 1 0 1846820116 109572096 26395 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26395 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 688.7 Current children cumulated vsize (Kb) 109128 [startup+701.244 s] Raw data (loadavg): 1.06 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26574 0 0 0 69676 192 0 0 25 0 1 0 1846820116 109572096 26395 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26395 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 698.7 Current children cumulated vsize (Kb) 109128 [startup+711.245 s] Raw data (loadavg): 1.05 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26574 0 0 0 70676 192 0 0 25 0 1 0 1846820116 109572096 26395 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26395 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 708.7 Current children cumulated vsize (Kb) 109128 [startup+721.244 s] Raw data (loadavg): 1.04 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26574 0 0 0 71677 192 0 0 25 0 1 0 1846820116 109572096 26395 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26395 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 718.71 Current children cumulated vsize (Kb) 109128 [startup+731.245 s] Raw data (loadavg): 1.04 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26575 0 0 0 72677 192 0 0 25 0 1 0 1846820116 109572096 26396 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26396 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 728.71 Current children cumulated vsize (Kb) 109128 [startup+741.246 s] Raw data (loadavg): 1.03 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 73676 192 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 738.7 Current children cumulated vsize (Kb) 109128 [startup+751.245 s] Raw data (loadavg): 1.03 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 74677 192 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 748.71 Current children cumulated vsize (Kb) 109128 [startup+761.246 s] Raw data (loadavg): 1.02 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 75677 192 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 758.71 Current children cumulated vsize (Kb) 109128 [startup+771.246 s] Raw data (loadavg): 1.02 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 76677 192 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 768.71 Current children cumulated vsize (Kb) 109128 [startup+781.247 s] Raw data (loadavg): 1.01 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 77677 192 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 778.71 Current children cumulated vsize (Kb) 109128 [startup+791.248 s] Raw data (loadavg): 1.01 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 78676 192 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 788.7 Current children cumulated vsize (Kb) 109128 [startup+801.247 s] Raw data (loadavg): 1.01 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 79677 192 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 798.71 Current children cumulated vsize (Kb) 109128 [startup+811.249 s] Raw data (loadavg): 1.01 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 80677 192 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 808.71 Current children cumulated vsize (Kb) 109128 [startup+821.249 s] Raw data (loadavg): 1.01 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 81677 192 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 818.71 Current children cumulated vsize (Kb) 109128 [startup+831.25 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 82678 192 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 828.72 Current children cumulated vsize (Kb) 109128 [startup+841.251 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 83678 192 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 838.72 Current children cumulated vsize (Kb) 109128 [startup+851.251 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 84678 193 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 848.73 Current children cumulated vsize (Kb) 109128 [startup+861.252 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 85678 193 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 858.73 Current children cumulated vsize (Kb) 109128 [startup+871.252 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 86678 193 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 868.73 Current children cumulated vsize (Kb) 109128 [startup+881.254 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 87678 194 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 878.74 Current children cumulated vsize (Kb) 109128 [startup+891.255 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 88677 194 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223120 134554687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 888.73 Current children cumulated vsize (Kb) 109128 [startup+901.255 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 89677 194 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223104 134556454 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 898.73 Current children cumulated vsize (Kb) 109128 [startup+911.257 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 90677 195 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 908.74 Current children cumulated vsize (Kb) 109128 [startup+921.256 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 91677 195 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 918.74 Current children cumulated vsize (Kb) 109128 [startup+931.257 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 92677 195 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 928.74 Current children cumulated vsize (Kb) 109128 [startup+941.258 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 93677 195 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223024 134556815 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 938.74 Current children cumulated vsize (Kb) 109128 [startup+951.258 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 94678 195 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 948.75 Current children cumulated vsize (Kb) 109128 [startup+961.259 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 95678 195 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 958.75 Current children cumulated vsize (Kb) 109128 [startup+971.259 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 96678 196 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 968.76 Current children cumulated vsize (Kb) 109128 [startup+981.261 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 97678 196 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223024 134557128 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 978.76 Current children cumulated vsize (Kb) 109128 [startup+991.262 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 98678 196 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 988.76 Current children cumulated vsize (Kb) 109128 [startup+1001.26 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 99678 196 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 998.76 Current children cumulated vsize (Kb) 109128 [startup+1011.26 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 100678 196 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 1008.76 Current children cumulated vsize (Kb) 109128 [startup+1021.26 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 101679 196 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 1018.77 Current children cumulated vsize (Kb) 109128 [startup+1031.26 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26576 0 0 0 102679 196 0 0 25 0 1 0 1846820116 109572096 26397 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26751 26397 145 145 0 26606 0 [pid=31263] vsize: 107004 Current children cumulated CPU time (s) 1028.77 Current children cumulated vsize (Kb) 109128 [startup+1041.26 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 103678 197 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1038.77 Current children cumulated vsize (Kb) 109316 [startup+1051.27 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 104677 197 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1048.76 Current children cumulated vsize (Kb) 109316 [startup+1061.27 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 105678 197 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1058.77 Current children cumulated vsize (Kb) 109316 [startup+1071.27 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 106678 197 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1068.77 Current children cumulated vsize (Kb) 109316 [startup+1081.27 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 107678 197 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1078.77 Current children cumulated vsize (Kb) 109316 [startup+1091.27 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 108678 197 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223056 134557583 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1088.77 Current children cumulated vsize (Kb) 109316 [startup+1101.27 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 109678 197 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1098.77 Current children cumulated vsize (Kb) 109316 [startup+1111.27 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 110678 198 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1108.78 Current children cumulated vsize (Kb) 109316 [startup+1121.27 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 111678 198 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223104 134556275 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1118.78 Current children cumulated vsize (Kb) 109316 [startup+1131.27 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 112679 198 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223024 134556757 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1128.79 Current children cumulated vsize (Kb) 109316 [startup+1141.27 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 113679 198 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1138.79 Current children cumulated vsize (Kb) 109316 [startup+1151.27 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 114679 198 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1148.79 Current children cumulated vsize (Kb) 109316 [startup+1161.27 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 115679 198 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1158.79 Current children cumulated vsize (Kb) 109316 [startup+1171.27 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 116679 198 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1168.79 Current children cumulated vsize (Kb) 109316 [startup+1181.27 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 117679 198 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1178.79 Current children cumulated vsize (Kb) 109316 [startup+1191.27 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 118680 198 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1188.8 Current children cumulated vsize (Kb) 109316 [startup+1201.27 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 119680 198 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1198.8 Current children cumulated vsize (Kb) 109316 [startup+1211.27 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 120680 198 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1208.8 Current children cumulated vsize (Kb) 109316 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1211.28 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 31263 Raw data (/proc/31259/stat): 31259 (minisat+_script) S 31258 31259 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846820111 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/31259/statm): 531 226 485 147 0 384 0 [pid=31259] vsize: 2124 Raw data (/proc/31263/stat): 31263 (minisat+_64-bit) R 31259 31259 19316 0 -1 0 26603 0 0 0 120680 198 0 0 25 0 1 0 1846820116 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31263/statm): 26798 26424 145 145 0 26653 0 [pid=31263] vsize: 107192 Current children cumulated CPU time (s) 1208.8 Current children cumulated vsize (Kb) 109316 Sending SIGTERM to -31259 Sleeping 2 seconds One traced child (pid=31259) ended because it received signal 15 (SIGTERM) One traced child (pid=31263) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1211.34 CPU time (s): 1208.85 CPU user time (s): 1206.81 CPU system time (s): 2.03669 CPU usage (%): 99.7946 Max. virtual memory (cumulated for all children) (Kb): 109316
ERROR: no interpretation found !