| Name | mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-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 wulflinc10 THE 2005-09-20 03:54:13 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3321 boxname=wulflinc10 idbench=977 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: c5ca7819a7dcae16ff6045242cdd1f87 /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-protfold.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-protfold.opb IDLAUNCH: 3321 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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: 784304 kB Buffers: 38476 kB Cached: 184200 kB SwapCached: 228 kB Active: 84404 kB Inactive: 141288 kB HighTotal: 131008 kB HighFree: 5628 kB LowTotal: 903652 kB LowFree: 778676 kB SwapTotal: 2097136 kB SwapFree: 2096756 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6280 kB Slab: 18988 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 04:14:23 (client local time) WITH STATUS 10 IN 1207.73 SECONDS stats: 3321 7 1207.73 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/14416/stat): 14416 (minisat+_script) R 14415 14416 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797261727 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/14416/statm): 174 3 169 147 0 27 0 [pid=14416] 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=14417 New process pid=14418 New process pid=14419 execve syscall for /bin/sed executable 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 One traced child (pid=14418) exited with status: 0 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=14419) exited with status: 0 One traced child (pid=14417) exited with status: 0 New process pid=14420 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-protfold.opb [startup+10.0031 s] Raw data (loadavg): 0.93 0.97 0.91 2/57 14420 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 3345 0 0 0 965 15 0 0 25 0 1 0 1797261732 14069760 3166 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 3435 3166 145 145 0 3290 0 [pid=14420] vsize: 13740 Current children cumulated CPU time (s) 9.8 Current children cumulated vsize (Kb) 15864 [startup+20.0037 s] Raw data (loadavg): 0.94 0.97 0.91 2/57 14420 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 3966 0 0 0 1954 18 0 0 25 0 1 0 1797261732 16617472 3787 4294967295 134512640 135094434 3221224432 3221223024 134557372 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14420/statm): 4057 3787 145 145 0 3912 0 [pid=14420] vsize: 16228 Current children cumulated CPU time (s) 19.72 Current children cumulated vsize (Kb) 18352 [startup+30.0053 s] Raw data (loadavg): 0.95 0.97 0.91 2/57 14420 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 4605 0 0 0 2942 22 0 0 25 0 1 0 1797261732 19251200 4426 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 4700 4426 145 145 0 4555 0 [pid=14420] vsize: 18800 Current children cumulated CPU time (s) 29.64 Current children cumulated vsize (Kb) 20924 [startup+40.0048 s] Raw data (loadavg): 0.96 0.97 0.91 2/57 14420 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 5214 0 0 0 3930 28 0 0 25 0 1 0 1797261732 21733376 5035 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 5306 5035 145 145 0 5161 0 [pid=14420] vsize: 21224 Current children cumulated CPU time (s) 39.58 Current children cumulated vsize (Kb) 23348 [startup+50.0054 s] Raw data (loadavg): 0.96 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 5792 0 0 0 4918 33 0 0 25 0 1 0 1797261732 24092672 5613 4294967295 134512640 135094434 3221224432 3221223088 134557978 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 5882 5613 145 145 0 5737 0 [pid=14420] vsize: 23528 Current children cumulated CPU time (s) 49.51 Current children cumulated vsize (Kb) 25652 [startup+60.006 s] Raw data (loadavg): 0.97 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 6336 0 0 0 5908 36 0 0 25 0 1 0 1797261732 26370048 6157 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14420/statm): 6438 6157 145 145 0 6293 0 [pid=14420] vsize: 25752 Current children cumulated CPU time (s) 59.44 Current children cumulated vsize (Kb) 27876 [startup+70.0065 s] Raw data (loadavg): 0.97 0.97 0.91 1/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) T 14416 14416 22582 0 -1 0 6942 0 0 0 6897 40 0 0 25 0 1 0 1797261732 28856320 6763 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/14420/statm): 7045 6763 145 145 0 6900 0 [pid=14420] vsize: 28180 Current children cumulated CPU time (s) 69.37 Current children cumulated vsize (Kb) 30304 [startup+80.007 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 7534 0 0 0 7888 45 0 0 25 0 1 0 1797261732 31277056 7355 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 7636 7355 145 145 0 7491 0 [pid=14420] vsize: 30544 Current children cumulated CPU time (s) 79.33 Current children cumulated vsize (Kb) 32668 [startup+90.0076 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 8061 0 0 0 8880 47 0 0 25 0 1 0 1797261732 33423360 7882 4294967295 134512640 135094434 3221224432 3221223024 134556918 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 8160 7882 145 145 0 8015 0 [pid=14420] vsize: 32640 Current children cumulated CPU time (s) 89.27 Current children cumulated vsize (Kb) 34764 [startup+100.008 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 8566 0 0 0 9873 50 0 0 25 0 1 0 1797261732 35491840 8387 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 8665 8387 145 145 0 8520 0 [pid=14420] vsize: 34660 Current children cumulated CPU time (s) 99.23 Current children cumulated vsize (Kb) 36784 [startup+110.009 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 9097 0 0 0 10864 54 0 0 25 0 1 0 1797261732 37654528 8918 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 9193 8918 145 145 0 9048 0 [pid=14420] vsize: 36772 Current children cumulated CPU time (s) 109.18 Current children cumulated vsize (Kb) 38896 [startup+120.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 9585 0 0 0 11855 57 0 0 25 0 1 0 1797261732 39641088 9406 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 9678 9406 145 145 0 9533 0 [pid=14420] vsize: 38712 Current children cumulated CPU time (s) 119.12 Current children cumulated vsize (Kb) 40836 [startup+130.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 10112 0 0 0 12846 61 0 0 25 0 1 0 1797261732 41922560 9933 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 10235 9933 145 145 0 10090 0 [pid=14420] vsize: 40940 Current children cumulated CPU time (s) 129.07 Current children cumulated vsize (Kb) 43064 [startup+140.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 10686 0 0 0 13834 66 0 0 25 0 1 0 1797261732 44265472 10507 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 10807 10507 145 145 0 10662 0 [pid=14420] vsize: 43228 Current children cumulated CPU time (s) 139 Current children cumulated vsize (Kb) 45352 [startup+150.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 11178 0 0 0 14825 71 0 0 25 0 1 0 1797261732 46272512 10999 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 11297 10999 145 145 0 11152 0 [pid=14420] vsize: 45188 Current children cumulated CPU time (s) 148.96 Current children cumulated vsize (Kb) 47312 [startup+160.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 11610 0 0 0 15819 73 0 0 25 0 1 0 1797261732 48029696 11431 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 11726 11431 145 145 0 11581 0 [pid=14420] vsize: 46904 Current children cumulated CPU time (s) 158.92 Current children cumulated vsize (Kb) 49028 [startup+170.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 12316 0 0 0 16808 77 0 0 23 0 1 0 1797261732 50913280 12137 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 12430 12137 145 145 0 12285 0 [pid=14420] vsize: 49720 Current children cumulated CPU time (s) 168.85 Current children cumulated vsize (Kb) 51844 [startup+180.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 12956 0 0 0 17797 82 0 0 25 0 1 0 1797261732 53530624 12777 4294967295 134512640 135094434 3221224432 3221223104 134556210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14420/statm): 13069 12777 145 145 0 12924 0 [pid=14420] vsize: 52276 Current children cumulated CPU time (s) 178.79 Current children cumulated vsize (Kb) 54400 [startup+190.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 13538 0 0 0 18789 85 0 0 25 0 1 0 1797261732 55906304 13359 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 13649 13359 145 145 0 13504 0 [pid=14420] vsize: 54596 Current children cumulated CPU time (s) 188.74 Current children cumulated vsize (Kb) 56720 [startup+200.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 14106 0 0 0 19781 89 0 0 25 0 1 0 1797261732 58228736 13927 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 14216 13927 145 145 0 14071 0 [pid=14420] vsize: 56864 Current children cumulated CPU time (s) 198.7 Current children cumulated vsize (Kb) 58988 [startup+210.013 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) T 14416 14416 22582 0 -1 0 14653 0 0 0 20773 92 0 0 25 0 1 0 1797261732 60461056 14474 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/14420/statm): 14761 14474 145 145 0 14616 0 [pid=14420] vsize: 59044 Current children cumulated CPU time (s) 208.65 Current children cumulated vsize (Kb) 61168 [startup+220.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 15147 0 0 0 21765 95 0 0 25 0 1 0 1797261732 62496768 14968 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 15258 14968 145 145 0 15113 0 [pid=14420] vsize: 61032 Current children cumulated CPU time (s) 218.6 Current children cumulated vsize (Kb) 63156 [startup+230.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 15642 0 0 0 22758 98 0 0 25 0 1 0 1797261732 64532480 15463 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 15755 15463 145 145 0 15610 0 [pid=14420] vsize: 63020 Current children cumulated CPU time (s) 228.56 Current children cumulated vsize (Kb) 65144 [startup+240.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 16143 0 0 0 23750 102 0 0 25 0 1 0 1797261732 66592768 15964 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 16258 15964 145 145 0 16113 0 [pid=14420] vsize: 65032 Current children cumulated CPU time (s) 238.52 Current children cumulated vsize (Kb) 67156 [startup+250.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 16626 0 0 0 24745 104 0 0 25 0 1 0 1797261732 68575232 16447 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 16742 16447 145 145 0 16597 0 [pid=14420] vsize: 66968 Current children cumulated CPU time (s) 248.49 Current children cumulated vsize (Kb) 69092 [startup+260.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 17110 0 0 0 25738 106 0 0 25 0 1 0 1797261732 70557696 16931 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 17226 16931 145 145 0 17081 0 [pid=14420] vsize: 68904 Current children cumulated CPU time (s) 258.44 Current children cumulated vsize (Kb) 71028 [startup+270.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 17649 0 0 0 26731 109 0 0 25 0 1 0 1797261732 72757248 17470 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 17763 17470 145 145 0 17618 0 [pid=14420] vsize: 71052 Current children cumulated CPU time (s) 268.4 Current children cumulated vsize (Kb) 73176 [startup+280.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 18145 0 0 0 27724 113 0 0 25 0 1 0 1797261732 74801152 17966 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 18262 17966 145 145 0 18117 0 [pid=14420] vsize: 73048 Current children cumulated CPU time (s) 278.37 Current children cumulated vsize (Kb) 75172 [startup+290.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 18543 0 0 0 28716 117 0 0 25 0 1 0 1797261732 76423168 18364 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14420/statm): 18658 18364 145 145 0 18513 0 [pid=14420] vsize: 74632 Current children cumulated CPU time (s) 288.33 Current children cumulated vsize (Kb) 76756 [startup+300.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 18868 0 0 0 29710 120 0 0 25 0 1 0 1797261732 77746176 18689 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14420/statm): 18981 18689 145 145 0 18836 0 [pid=14420] vsize: 75924 Current children cumulated CPU time (s) 298.3 Current children cumulated vsize (Kb) 78048 [startup+310.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 19234 0 0 0 30702 125 0 0 25 0 1 0 1797261732 79237120 19055 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14420/statm): 19345 19055 145 145 0 19200 0 [pid=14420] vsize: 77380 Current children cumulated CPU time (s) 308.27 Current children cumulated vsize (Kb) 79504 [startup+320.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 19565 0 0 0 31696 127 0 0 25 0 1 0 1797261732 80846848 19386 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14420/statm): 19738 19386 145 145 0 19593 0 [pid=14420] vsize: 78952 Current children cumulated CPU time (s) 318.23 Current children cumulated vsize (Kb) 81076 [startup+330.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 19854 0 0 0 32689 130 0 0 25 0 1 0 1797261732 82018304 19675 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14420/statm): 20024 19675 145 145 0 19879 0 [pid=14420] vsize: 80096 Current children cumulated CPU time (s) 328.19 Current children cumulated vsize (Kb) 82220 [startup+340.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 20139 0 0 0 33684 133 0 0 25 0 1 0 1797261732 83189760 19960 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14420/statm): 20310 19960 145 145 0 20165 0 [pid=14420] vsize: 81240 Current children cumulated CPU time (s) 338.17 Current children cumulated vsize (Kb) 83364 [startup+350.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 20404 0 0 0 34679 135 0 0 25 0 1 0 1797261732 84262912 20225 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14420/statm): 20572 20225 145 145 0 20427 0 [pid=14420] vsize: 82288 Current children cumulated CPU time (s) 348.14 Current children cumulated vsize (Kb) 84412 [startup+360.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 20664 0 0 0 35672 139 0 0 25 0 1 0 1797261732 85327872 20485 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14420/statm): 20832 20485 145 145 0 20687 0 [pid=14420] vsize: 83328 Current children cumulated CPU time (s) 358.11 Current children cumulated vsize (Kb) 85452 [startup+370.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 20930 0 0 0 36667 142 0 0 25 0 1 0 1797261732 86409216 20751 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14420/statm): 21096 20751 145 145 0 20951 0 [pid=14420] vsize: 84384 Current children cumulated CPU time (s) 368.09 Current children cumulated vsize (Kb) 86508 [startup+380.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 21221 0 0 0 37661 144 0 0 25 0 1 0 1797261732 87597056 21042 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14420/statm): 21386 21042 145 145 0 21241 0 [pid=14420] vsize: 85544 Current children cumulated CPU time (s) 378.05 Current children cumulated vsize (Kb) 87668 [startup+390.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 21472 0 0 0 38656 146 0 0 25 0 1 0 1797261732 88641536 21293 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14420/statm): 21641 21293 145 145 0 21496 0 [pid=14420] vsize: 86564 Current children cumulated CPU time (s) 388.02 Current children cumulated vsize (Kb) 88688 [startup+400.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 21724 0 0 0 39650 149 0 0 25 0 1 0 1797261732 89673728 21545 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14420/statm): 21893 21545 145 145 0 21748 0 [pid=14420] vsize: 87572 Current children cumulated CPU time (s) 397.99 Current children cumulated vsize (Kb) 89696 [startup+410.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 22015 0 0 0 40644 152 0 0 25 0 1 0 1797261732 90869760 21836 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14420/statm): 22185 21836 145 145 0 22040 0 [pid=14420] vsize: 88740 Current children cumulated CPU time (s) 407.96 Current children cumulated vsize (Kb) 90864 [startup+420.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 22284 0 0 0 41638 154 0 0 25 0 1 0 1797261732 91983872 22105 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 22457 22105 145 145 0 22312 0 [pid=14420] vsize: 89828 Current children cumulated CPU time (s) 417.92 Current children cumulated vsize (Kb) 91952 [startup+430.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 22539 0 0 0 42634 156 0 0 25 0 1 0 1797261732 93040640 22360 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 22715 22360 145 145 0 22570 0 [pid=14420] vsize: 90860 Current children cumulated CPU time (s) 427.9 Current children cumulated vsize (Kb) 92984 [startup+440.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 22763 0 0 0 43630 158 0 0 25 0 1 0 1797261732 93958144 22584 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 22939 22584 145 145 0 22794 0 [pid=14420] vsize: 91756 Current children cumulated CPU time (s) 437.88 Current children cumulated vsize (Kb) 93880 [startup+450.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 22988 0 0 0 44627 160 0 0 25 0 1 0 1797261732 94896128 22809 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 23168 22809 145 145 0 23023 0 [pid=14420] vsize: 92672 Current children cumulated CPU time (s) 447.87 Current children cumulated vsize (Kb) 94796 [startup+460.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 23229 0 0 0 45624 161 0 0 25 0 1 0 1797261732 95879168 23050 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 23408 23050 145 145 0 23263 0 [pid=14420] vsize: 93632 Current children cumulated CPU time (s) 457.85 Current children cumulated vsize (Kb) 95756 [startup+470.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 23506 0 0 0 46618 163 0 0 25 0 1 0 1797261732 97021952 23327 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14420/statm): 23687 23327 145 145 0 23542 0 [pid=14420] vsize: 94748 Current children cumulated CPU time (s) 467.81 Current children cumulated vsize (Kb) 96872 [startup+480.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 23730 0 0 0 47614 164 0 0 25 0 1 0 1797261732 97939456 23551 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 23911 23551 145 145 0 23766 0 [pid=14420] vsize: 95644 Current children cumulated CPU time (s) 477.78 Current children cumulated vsize (Kb) 97768 [startup+490.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 23976 0 0 0 48610 166 0 0 25 0 1 0 1797261732 98942976 23797 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 24156 23797 145 145 0 24011 0 [pid=14420] vsize: 96624 Current children cumulated CPU time (s) 487.76 Current children cumulated vsize (Kb) 98748 [startup+500.032 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) T 14416 14416 22582 0 -1 0 24301 0 0 0 49606 169 0 0 25 0 1 0 1797261732 100270080 24122 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/14420/statm): 24480 24122 145 145 0 24335 0 [pid=14420] vsize: 97920 Current children cumulated CPU time (s) 497.75 Current children cumulated vsize (Kb) 100044 [startup+510.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 24541 0 0 0 50603 170 0 0 25 0 1 0 1797261732 101253120 24362 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 24720 24362 145 145 0 24575 0 [pid=14420] vsize: 98880 Current children cumulated CPU time (s) 507.73 Current children cumulated vsize (Kb) 101004 [startup+520.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 24793 0 0 0 51599 172 0 0 25 0 1 0 1797261732 102281216 24614 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 24971 24614 145 145 0 24826 0 [pid=14420] vsize: 99884 Current children cumulated CPU time (s) 517.71 Current children cumulated vsize (Kb) 102008 [startup+530.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 25051 0 0 0 52595 174 0 0 25 0 1 0 1797261732 103337984 24872 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 25229 24872 145 145 0 25084 0 [pid=14420] vsize: 100916 Current children cumulated CPU time (s) 527.69 Current children cumulated vsize (Kb) 103040 [startup+540.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 25312 0 0 0 53590 175 0 0 25 0 1 0 1797261732 104402944 25133 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 25489 25133 145 145 0 25344 0 [pid=14420] vsize: 101956 Current children cumulated CPU time (s) 537.65 Current children cumulated vsize (Kb) 104080 [startup+550.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 25569 0 0 0 54587 176 0 0 25 0 1 0 1797261732 105443328 25390 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 25743 25390 145 145 0 25598 0 [pid=14420] vsize: 102972 Current children cumulated CPU time (s) 547.63 Current children cumulated vsize (Kb) 105096 [startup+560.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 25782 0 0 0 55584 177 0 0 25 0 1 0 1797261732 106328064 25603 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 25959 25603 145 145 0 25814 0 [pid=14420] vsize: 103836 Current children cumulated CPU time (s) 557.61 Current children cumulated vsize (Kb) 105960 [startup+570.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 25985 0 0 0 56580 179 0 0 25 0 1 0 1797261732 107167744 25806 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26164 25806 145 145 0 26019 0 [pid=14420] vsize: 104656 Current children cumulated CPU time (s) 567.59 Current children cumulated vsize (Kb) 106780 [startup+580.095 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26205 0 0 0 57575 181 0 0 25 0 1 0 1797261732 108085248 26026 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26388 26026 145 145 0 26243 0 [pid=14420] vsize: 105552 Current children cumulated CPU time (s) 577.56 Current children cumulated vsize (Kb) 107676 [startup+590.096 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26403 0 0 0 58572 182 0 0 25 0 1 0 1797261732 108879872 26224 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26582 26224 145 145 0 26437 0 [pid=14420] vsize: 106328 Current children cumulated CPU time (s) 587.54 Current children cumulated vsize (Kb) 108452 [startup+600.097 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26572 0 0 0 59570 183 0 0 25 0 1 0 1797261732 109572096 26393 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26393 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 597.53 Current children cumulated vsize (Kb) 109128 [startup+610.098 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26572 0 0 0 60570 183 0 0 25 0 1 0 1797261732 109572096 26393 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26393 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 607.53 Current children cumulated vsize (Kb) 109128 [startup+620.097 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26573 0 0 0 61570 183 0 0 25 0 1 0 1797261732 109572096 26394 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26394 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 617.53 Current children cumulated vsize (Kb) 109128 [startup+630.098 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26574 0 0 0 62570 183 0 0 25 0 1 0 1797261732 109572096 26395 4294967295 134512640 135094434 3221224432 3221223024 134557013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26395 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 627.53 Current children cumulated vsize (Kb) 109128 [startup+640.098 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26574 0 0 0 63570 183 0 0 25 0 1 0 1797261732 109572096 26395 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26395 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 637.53 Current children cumulated vsize (Kb) 109128 [startup+650.099 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26574 0 0 0 64571 183 0 0 25 0 1 0 1797261732 109572096 26395 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26395 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 647.54 Current children cumulated vsize (Kb) 109128 [startup+660.099 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26574 0 0 0 65571 183 0 0 25 0 1 0 1797261732 109572096 26395 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26395 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 657.54 Current children cumulated vsize (Kb) 109128 [startup+670.099 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26574 0 0 0 66571 183 0 0 25 0 1 0 1797261732 109572096 26395 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26395 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 667.54 Current children cumulated vsize (Kb) 109128 [startup+680.101 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26574 0 0 0 67571 183 0 0 25 0 1 0 1797261732 109572096 26395 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26395 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 677.54 Current children cumulated vsize (Kb) 109128 [startup+690.101 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26574 0 0 0 68572 183 0 0 25 0 1 0 1797261732 109572096 26395 4294967295 134512640 135094434 3221224432 3221223024 134557375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26395 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 687.55 Current children cumulated vsize (Kb) 109128 [startup+700.102 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26574 0 0 0 69572 183 0 0 25 0 1 0 1797261732 109572096 26395 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26395 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 697.55 Current children cumulated vsize (Kb) 109128 [startup+710.102 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26574 0 0 0 70572 183 0 0 25 0 1 0 1797261732 109572096 26395 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26395 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 707.55 Current children cumulated vsize (Kb) 109128 [startup+720.103 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26574 0 0 0 71572 183 0 0 25 0 1 0 1797261732 109572096 26395 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26395 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 717.55 Current children cumulated vsize (Kb) 109128 [startup+730.103 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26575 0 0 0 72573 183 0 0 25 0 1 0 1797261732 109572096 26396 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26396 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 727.56 Current children cumulated vsize (Kb) 109128 [startup+740.104 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 73572 183 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 737.55 Current children cumulated vsize (Kb) 109128 [startup+750.105 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 74572 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223024 134556823 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 747.56 Current children cumulated vsize (Kb) 109128 [startup+760.106 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 75572 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 757.56 Current children cumulated vsize (Kb) 109128 [startup+770.106 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 76572 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 767.56 Current children cumulated vsize (Kb) 109128 [startup+780.108 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 77573 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 777.57 Current children cumulated vsize (Kb) 109128 [startup+790.108 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 78573 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134558286 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 787.57 Current children cumulated vsize (Kb) 109128 [startup+800.109 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 79573 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 797.57 Current children cumulated vsize (Kb) 109128 [startup+810.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 80573 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 807.57 Current children cumulated vsize (Kb) 109128 [startup+820.109 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 81574 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 817.58 Current children cumulated vsize (Kb) 109128 [startup+830.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 82574 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 827.58 Current children cumulated vsize (Kb) 109128 [startup+840.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 83574 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 837.58 Current children cumulated vsize (Kb) 109128 [startup+850.112 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 84575 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 847.59 Current children cumulated vsize (Kb) 109128 [startup+860.112 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 85575 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 857.59 Current children cumulated vsize (Kb) 109128 [startup+870.113 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 86575 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 867.59 Current children cumulated vsize (Kb) 109128 [startup+880.114 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 87575 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 877.59 Current children cumulated vsize (Kb) 109128 [startup+890.114 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 88576 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 887.6 Current children cumulated vsize (Kb) 109128 [startup+900.116 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 89576 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 897.6 Current children cumulated vsize (Kb) 109128 [startup+910.116 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 90576 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 907.6 Current children cumulated vsize (Kb) 109128 [startup+920.117 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 91576 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 917.6 Current children cumulated vsize (Kb) 109128 [startup+930.117 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 92577 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 927.61 Current children cumulated vsize (Kb) 109128 [startup+940.118 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 93577 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 937.61 Current children cumulated vsize (Kb) 109128 [startup+950.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 94577 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 947.61 Current children cumulated vsize (Kb) 109128 [startup+960.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 95577 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 957.61 Current children cumulated vsize (Kb) 109128 [startup+970.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 96578 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 967.62 Current children cumulated vsize (Kb) 109128 [startup+980.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 97578 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 977.62 Current children cumulated vsize (Kb) 109128 [startup+990.121 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 98578 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 987.62 Current children cumulated vsize (Kb) 109128 [startup+1000.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 99578 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 997.62 Current children cumulated vsize (Kb) 109128 [startup+1010.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 100579 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223104 134556485 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 1007.63 Current children cumulated vsize (Kb) 109128 [startup+1020.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 101579 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 1017.63 Current children cumulated vsize (Kb) 109128 [startup+1030.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26576 0 0 0 102579 184 0 0 25 0 1 0 1797261732 109572096 26397 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26751 26397 145 145 0 26606 0 [pid=14420] vsize: 107004 Current children cumulated CPU time (s) 1027.63 Current children cumulated vsize (Kb) 109128 [startup+1040.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 103578 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1037.62 Current children cumulated vsize (Kb) 109316 [startup+1050.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 104578 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221222960 134783376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1047.62 Current children cumulated vsize (Kb) 109316 [startup+1060.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 105579 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1057.63 Current children cumulated vsize (Kb) 109316 [startup+1070.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 106579 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1067.63 Current children cumulated vsize (Kb) 109316 [startup+1080.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 107579 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1077.63 Current children cumulated vsize (Kb) 109316 [startup+1090.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 108579 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1087.63 Current children cumulated vsize (Kb) 109316 [startup+1100.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 109579 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1097.63 Current children cumulated vsize (Kb) 109316 [startup+1110.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 110580 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1107.64 Current children cumulated vsize (Kb) 109316 [startup+1120.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 111580 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1117.64 Current children cumulated vsize (Kb) 109316 [startup+1130.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 112580 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221223024 134557514 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1127.64 Current children cumulated vsize (Kb) 109316 [startup+1140.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 113580 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1137.64 Current children cumulated vsize (Kb) 109316 [startup+1150.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 114581 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221223024 134557369 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1147.65 Current children cumulated vsize (Kb) 109316 [startup+1160.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 115581 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1157.65 Current children cumulated vsize (Kb) 109316 [startup+1170.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 116581 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1167.65 Current children cumulated vsize (Kb) 109316 [startup+1180.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 117581 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1177.65 Current children cumulated vsize (Kb) 109316 [startup+1190.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 118582 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1187.66 Current children cumulated vsize (Kb) 109316 [startup+1200.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 119582 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1197.66 Current children cumulated vsize (Kb) 109316 [startup+1210.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 120582 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1207.66 Current children cumulated vsize (Kb) 109316 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14422 Raw data (/proc/14416/stat): 14416 (minisat+_script) S 14415 14416 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797261727 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14416/statm): 531 226 485 147 0 384 0 [pid=14416] vsize: 2124 Raw data (/proc/14420/stat): 14420 (minisat+_64-bit) R 14416 14416 22582 0 -1 0 26603 0 0 0 120582 184 0 0 25 0 1 0 1797261732 109764608 26424 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14420/statm): 26798 26424 145 145 0 26653 0 [pid=14420] vsize: 107192 Current children cumulated CPU time (s) 1207.66 Current children cumulated vsize (Kb) 109316 Sending SIGTERM to -14416 Sleeping 2 seconds One traced child (pid=14416) ended because it received signal 15 (SIGTERM) One traced child (pid=14420) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.2 CPU time (s): 1207.73 CPU user time (s): 1205.83 CPU system time (s): 1.89971 CPU usage (%): 99.7963 Max. virtual memory (cumulated for all children) (Kb): 109316
ERROR: no interpretation found !