Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-sp97ar.opb
MD5SUM501db04e3c45fac1238dfa119cd7abd9
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 282020
Biggest coefficient in the objective function 2456844338462720
Number of bits for the biggest coefficient in the objective function 52
Sum of the numbers in the objective function -2082450254578026316
Number of bits of the sum of numbers in the objective function 64
Biggest number in a constraint 2456844338462720
Number of bits of the biggest number in a constraint 52
Biggest sum of numbers in a constraint -2082450254578026316
Number of bits of the biggest sum of numbers64
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables282020
Total number of constraints1761
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints1761
Minimum length of a constraint20
Maximum length of a constraint49260

Trace number 4498

Launcher Data

LAUNCH ON wulflinc5 THE 2005-09-19 17:44:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2957 boxname=wulflinc5 idbench=613 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  501db04e3c45fac1238dfa119cd7abd9  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-sp97ar.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-sp97ar.opb
IDLAUNCH: 2957
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        780408 kB
Buffers:         35592 kB
Cached:         193672 kB
SwapCached:        780 kB
Active:         180060 kB
Inactive:        51920 kB
HighTotal:      131008 kB
HighFree:         3724 kB
LowTotal:       903652 kB
LowFree:        776684 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:               8 kB
Writeback:           0 kB
Mapped:           5804 kB
Slab:            16516 kB
Committed_AS:    64300 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 18:04:41 (client local time) WITH STATUS 0 IN 1202.6 SECONDS
stats: 2957 7 1202.6 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 14105] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 1739 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ===========
c   -- Clauses(.)/Splits(s): s...s.ssssssss.ss........ss...ssss..ss.s..ss.s..s..ssssssssssss...s.s.ss.s.s..s.s..s..s...sss.ss.s...s.s.s..ssss..s.ss.s..ss.s.s......sss..ss.ss...sssss.s..ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss.ssssssssss.ssssssssssssssss.ssss..sss..s..s...sss...s.s..ssssss.ss.ssss.sss...s....ssssssss..s.ss....sssssss.s.sssssssssssssss.ss.ss.ssss.s..sssssssssss..ss.ssssss.sss.sss..ss..s...ss.s.ss.sss.ssssss...ss.sssssssss.sss.ss.ss.s.sssssssss.ssss..ss..s.ssss.s.s.....ssss...s.s..sssss.ss....s...s.
c ---[2139]---> BDD-cost:   19
c ---[2138]---> BDD-cost:   27
c ---[2137]---> BDD-cost:   27
c ---[2136]---> BDD-cost:   27
c ---[2135]---> BDD-cost:   25
c ---[2134]---> BDD-cost:   25
c ---[2133]---> BDD-cost:    3
c ---[2132]---> BDD-cost:   19
c ---[2130]---> BDD-cost:    3
c ---[2127]---> BDD-cost:    7
c ---[2126]---> BDD-cost:   11
c ---[2125]---> BDD-cost:   19
c ---[2124]---> BDD-cost:   11
c ---[2123]---> BDD-cost:   19
c ---[2122]---> BDD-cost:    9
c ---[2121]---> BDD-cost:   11
c ---[2120]---> BDD-cost:    7
c ---[2119]---> BDD-cost:    7
c ---[2117]---> BDD-cost:   31
c ---[2116]---> BDD-cost:   31
c ---[2115]---> BDD-cost:   21
c ---[2114]---> BDD-cost:   23
c ---[2113]---> BDD-cost:   19
c ---[2112]---> BDD-cost:   19
c ---[2111]---> BDD-cost:   27
c ---[2110]---> BDD-cost:   33
c ---[2109]---> BDD-cost:   29
c ---[2108]---> BDD-cost:   27
c ---[2106]---> BDD-cost:    7
c ---[2105]---> BDD-cost:   27
c ---[2104]---> BDD-cost:   33
c ---[2103]---> BDD-cost:   37
c ---[2102]---> BDD-cost:   37
c ---[2101]---> BDD-cost:   37
c ---[2100]---> BDD-cost:   37
c ---[2099]---> BDD-cost:   37
c ---[2098]---> BDD-cost:    7
c ---[2097]---> BDD-cost:   19
c ---[2095]---> BDD-cost:    9
c ---[2094]---> BDD-cost:    7
c ---[2093]---> BDD-cost:    5
c ---[2092]---> BDD-cost:   19
c ---[2091]---> BDD-cost:   23
c ---[2090]---> BDD-cost:    3
c ---[2089]---> BDD-cost:   27
c ---[2088]---> BDD-cost:   27
c ---[2087]---> BDD-cost:   29
c ---[2086]---> BDD-cost:   19
c ---[2084]---> BDD-cost:   19
c ---[2083]---> BDD-cost:   19
c ---[2082]---> BDD-cost:   31
c ---[2081]---> BDD-cost:   37
c ---[2080]---> BDD-cost:   31
c ---[2079]---> BDD-cost:   37
c ---[2078]---> BDD-cost:   11
c ---[2077]---> BDD-cost:   13
c ---[2076]---> BDD-cost:   13
c ---[2075]---> BDD-cost:   37
c ---[2073]---> BDD-cost:   37
c ---[2072]---> BDD-cost:   37
c ---[2071]---> BDD-cost:   37
c ---[2070]---> BDD-cost:   31
c ---[2069]---> BDD-cost:   37
c ---[2068]---> BDD-cost:   31
c ---[2067]---> BDD-cost:   37
c ---[2066]---> BDD-cost:   19
c ---[2065]---> BDD-cost:   19
c ---[2064]---> BDD-cost:    7
c ---[2062]---> BDD-cost:   11
c ---[2061]---> BDD-cost:   27
c ---[2060]---> BDD-cost:   31
c ---[2059]---> BDD-cost:   37
c ---[2058]---> BDD-cost:   27
c ---[2057]---> BDD-cost:   37
c ---[2056]---> BDD-cost:   29
c ---[2055]---> BDD-cost:    7
c ---[2054]---> BDD-cost:    7
c ---[2053]---> BDD-cost:    7
c ---[2051]---> BDD-cost:    7
c ---[2050]---> BDD-cost:   27
c ---[2049]---> BDD-cost:   27
c ---[2048]---> BDD-cost:   37
c ---[2047]---> BDD-cost:   11
c ---[2046]---> BDD-cost:   37
c ---[2045]---> BDD-cost:    7
c ---[2044]---> BDD-cost:   11
c ---[2043]---> BDD-cost:   23
c ---[2042]---> BDD-cost:   29
c ---[2040]---> BDD-cost:   37
c ---[2039]---> BDD-cost:   29
c ---[2038]---> BDD-cost:    7
c ---[2037]---> BDD-cost:   29
c ---[2036]---> BDD-cost:   37
c ---[2035]---> BDD-cost:   19
c ---[2034]---> BDD-cost:   29
c ---[2033]---> BDD-cost:   37
c ---[2032]---> BDD-cost:   27
c ---[2031]---> BDD-cost:    9
c ---[2028]---> BDD-cost:   27
c ---[2027]---> BDD-cost:   27
c ---[2026]---> BDD-cost:   21
c ---[2025]---> BDD-cost:    9
c ---[2024]---> BDD-cost:   11
c ---[2023]---> BDD-cost:   29
c ---[2022]---> BDD-cost:   37
c ---[2021]---> BDD-cost:   37
c ---[2020]---> BDD-cost:   37
c ---[2019]---> BDD-cost:   37
c ---[2017]---> BDD-cost:   37
c ---[2016]---> BDD-cost:   27
c ---[2015]---> BDD-cost:   19
c ---[2014]---> BDD-cost:   27
c ---[2013]---> BDD-cost:   27
c ---[2012]---> BDD-cost:   37
c ---[2011]---> BDD-cost:   25
c ---[2010]---> BDD-cost:    9
c ---[2009]---> BDD-cost:   19
c ---[2008]---> BDD-cost:    9
c ---[2006]---> BDD-cost:    9
c ---[2005]---> BDD-cost:    9
c ---[2004]---> BDD-cost:    7
c ---[2003]---> BDD-cost:    5
c ---[2002]---> BDD-cost:   19
c ---[2001]---> BDD-cost:    3
c ---[2000]---> BDD-cost:    5
c ---[1999]---> BDD-cost:   19
c ---[1998]---> BDD-cost:   19
c ---[1997]---> BDD-cost:   27
c ---[1994]---> BDD-cost:   27
c ---[1993]---> BDD-cost:   27
c ---[1991]---> BDD-cost:    7
c ---[1990]---> BDD-cost:    3
c ---[1989]---> BDD-cost:    9
c ---[1988]---> BDD-cost:    7
c ---[1985]---> BDD-cost:    9
c ---[1984]---> BDD-cost:   27
c ---[1983]---> BDD-cost:   25
c ---[1982]---> BDD-cost:   27
c ---[1981]---> BDD-cost:   27
c ---[1979]---> BDD-cost:    3
c ---[1977]---> BDD-cost:    9
c ---[1976]---> BDD-cost:    9
c ---[1975]---> BDD-cost:   23
c ---[1974]---> BDD-cost:   19
c ---[1973]---> BDD-cost:   19
c ---[1972]---> BDD-cost:   19
c ---[1971]---> BDD-cost:   23
c ---[1970]---> BDD-cost:   37
c ---[1969]---> BDD-cost:   27
c ---[1968]---> BDD-cost:   19
c ---[1966]---> BDD-cost:   19
c ---[1965]---> BDD-cost:   19
c ---[1964]---> BDD-cost:   37
c ---[1963]---> BDD-cost:   19
c ---[1962]---> BDD-cost:   19
c ---[1961]---> BDD-cost:   23
c ---[1960]---> BDD-cost:   23
c ---[1959]---> BDD-cost:   23
c ---[1958]---> BDD-cost:   19
c ---[1957]---> BDD-cost:   23
c ---[1955]---> BDD-cost:    7
c ---[1953]---> BDD-cost:    5
c ---[1952]---> BDD-cost:    5
c ---[1951]---> BDD-cost:    7
c ---[1949]---> BDD-cost:    5
c ---[1947]---> BDD-cost:    5
c ---[1946]---> BDD-cost:   27
c ---[1944]---> BDD-cost:   27
c ---[1943]---> BDD-cost:   19
c ---[1942]---> BDD-cost:   19
c ---[1941]---> BDD-cost:   19
c ---[1940]---> BDD-cost:   19
c ---[1939]---> BDD-cost:   19
c ---[1938]---> BDD-cost:    7
c ---[1937]---> BDD-cost:   19
c ---[1936]---> BDD-cost:   27
c ---[1935]---> BDD-cost:    7
c ---[1933]---> BDD-cost:    7
c ---[1932]---> BDD-cost:   27
c ---[1931]---> BDD-cost:   27
c ---[1930]---> BDD-cost:    7
c ---[1929]---> BDD-cost:    7
c ---[1928]---> BDD-cost:   19
c ---[1927]---> BDD-cost:    7
c ---[1926]---> BDD-cost:   19
c ---[1925]---> BDD-cost:    7
c ---[1924]---> BDD-cost:    7
c ---[1921]---> BDD-cost:   19
c ---[1920]---> BDD-cost:   19
c ---[1919]---> BDD-cost:   19
c ---[1918]---> BDD-cost:   19
c ---[1917]---> BDD-cost:   31
c ---[1916]---> BDD-cost:   19
c ---[1915]---> BDD-cost:   19
c ---[1914]---> BDD-cost:    7
c ---[1913]---> BDD-cost:   19
c ---[1912]---> BDD-cost:   19
c ---[1910]---> BDD-cost:   19
c ---[1909]---> BDD-cost:   27
c ---[1908]---> BDD-cost:   27
c ---[1907]---> BDD-cost:    7
c ---[1906]---> BDD-cost:    7
c ---[1905]---> BDD-cost:    7
c ---[1904]---> BDD-cost:   27
c ---[1903]---> BDD-cost:    7
c ---[1902]---> BDD-cost:   19
c ---[1901]---> BDD-cost:   37
c ---[1899]---> BDD-cost:   27
c ---[1898]---> BDD-cost:   19
c ---[1897]---> BDD-cost:    7
c ---[1896]---> BDD-cost:   37
c ---[1895]---> BDD-cost:   37
c ---[1894]---> BDD-cost:   37
c ---[1893]---> BDD-cost:   19
c ---[1892]---> BDD-cost:   27
c ---[1891]---> BDD-cost:   33
c ---[1890]---> BDD-cost:   37
c ---[1888]---> BDD-cost:    7
c ---[1887]---> BDD-cost:    7
c ---[1886]---> BDD-cost:    9
c ---[1885]---> BDD-cost:    3
c ---[1884]---> BDD-cost:    3
c ---[1883]---> BDD-cost:    7
c ---[1882]---> BDD-cost:    7
c ---[1881]---> BDD-cost: 1710
c ---[1880]---> BDD-cost:   11
c ---[1879]---> BDD-cost:    7
c ---[1878]---> BDD-cost:    7
c ---[1877]---> BDD-cost:    7
c ---[1876]---> BDD-cost:   27
c ---[1875]---> BDD-cost:    7
c ---[1874]---> BDD-cost:    7
c ---[1873]---> BDD-cost:    3
c ---[1872]---> BDD-cost:    3
c ---[1870]---> BDD-cost:    7
c ---[1869]---> BDD-cost:    7
c ---[1868]---> BDD-cost:    5
c ---[1867]---> BDD-cost:    7
c ---[1866]---> BDD-cost:    7
c ---[1865]---> BDD-cost:    3
c ---[1864]---> BDD-cost:   19
c ---[1863]---> BDD-cost:   13
c ---[1862]---> BDD-cost:   19
c ---[1861]---> BDD-cost:   31
c ---[1859]---> BDD-cost:   37
c ---[1858]---> BDD-cost:   13
c ---[1857]---> BDD-cost:   37
c ---[1856]---> BDD-cost:   27
c ---[1855]---> BDD-cost:   27
c ---[1854]---> BDD-cost:   19
c ---[1853]---> BDD-cost:   31
c ---[1852]---> BDD-cost:   37
c ---[1851]---> BDD-cost:   15
c ---[1850]---> BDD-cost:   37
c ---[1848]---> BDD-cost:   19
c ---[1847]---> BDD-cost:   27
c ---[1846]---> BDD-cost:   19
c ---[1845]---> BDD-cost:   19
c ---[1844]---> BDD-cost:   19
c ---[1843]---> BDD-cost:   29
c ---[1842]---> BDD-cost:   37
c ---[1841]---> BDD-cost:   19
c ---[1840]---> BDD-cost:   15
c ---[1839]---> BDD-cost:   37
c ---[1837]---> BDD-cost:   27
c ---[1836]---> BDD-cost:   27
c ---[1835]---> BDD-cost:   19
c ---[1834]---> BDD-cost:   27
c ---[1833]---> BDD-cost:   31
c ---[1832]---> BDD-cost:   37
c ---[1831]---> BDD-cost:   17
c ---[1830]---> BDD-cost:   37
c ---[1829]---> BDD-cost:   15
c ---[1828]---> BDD-cost:   27
c ---[1826]---> BDD-cost:   27
c ---[1825]---> BDD-cost:   27
c ---[1824]---> BDD-cost:   27
c ---[1823]---> BDD-cost:   37
c ---[1822]---> BDD-cost:   27
c ---[1821]---> BDD-cost:    3
c ---[1820]---> BDD-cost:   27
c ---[1819]---> BDD-cost:    7
c ---[1818]---> BDD-cost:    9
c ---[1817]---> BDD-cost:    5
c ---[1814]---> BDD-cost:   11
c ---[1813]---> BDD-cost:   29
c ---[1812]---> BDD-cost:   27
c ---[1811]---> BDD-cost:   23
c ---[1810]---> BDD-cost:   19
c ---[1809]---> BDD-cost:   27
c ---[1808]---> BDD-cost:   27
c ---[1806]---> BDD-cost:    3
c ---[1805]---> BDD-cost:    9
c ---[1802]---> BDD-cost:    5
c ---[1801]---> BDD-cost:    5
c ---[1800]---> BDD-cost:    3
c ---[1799]---> BDD-cost:    3
c ---[1798]---> BDD-cost:    9
c ---[1797]---> BDD-cost:    3
c ---[1796]---> BDD-cost:    9
c ---[1795]---> BDD-cost:    9
c ---[1791]---> BDD-cost:    9
c ---[1790]---> BDD-cost:   11
c ---[1789]---> BDD-cost:    3
c ---[1788]---> BDD-cost:   13
c ---[1786]---> BDD-cost:   13
c ---[1785]---> BDD-cost:    9
c ---[1784]---> BDD-cost:   37
c ---[1783]---> BDD-cost:   37
c ---[1781]---> BDD-cost:   31
c ---[1780]---> BDD-cost:    5
c ---[1779]---> BDD-cost:    7
c ---[1778]---> BDD-cost:    9
c ---[1777]---> BDD-cost:   11
c ---[1776]---> BDD-cost:   11
c ---[1775]---> BDD-cost:   29
c ---[1774]---> BDD-cost:   21
c ---[1773]---> BDD-cost:   37
c ---[1772]---> BDD-cost:   27
c ---[1770]---> BDD-cost:   37
c ---[1769]---> BDD-cost:   29
c ---[1768]---> BDD-cost:    5
c ---[1767]---> BDD-cost:    7
c ---[1766]---> BDD-cost:    9
c ---[1765]---> BDD-cost:   11
c ---[1764]---> BDD-cost:   11
c ---[1763]---> BDD-cost:   31
c ---[1762]---> BDD-cost:   21
c ---[1761]---> BDD-cost:   11
c ---[1759]---> BDD-cost:   29
c ---[1758]---> BDD-cost:   29
c ---[1757]---> BDD-cost:   11
c ---[1756]---> BDD-cost:   31
c ---[1755]---> BDD-cost:   27
c ---[1754]---> BDD-cost:   37
c ---[1753]---> BDD-cost:   35
c ---[1752]---> BDD-cost:   19
c ---[1751]---> BDD-cost:   31
c ---[1750]---> BDD-cost:   15
c ---[1748]---> BDD-cost:   31
c ---[1747]---> BDD-cost:   31
c ---[1746]---> BDD-cost:   31
c ---[1745]---> BDD-cost:   15
c ---[1744]---> BDD-cost:   27
c ---[1743]---> BDD-cost:   27
c ---[1742]---> BDD-cost:   29
c ---[1741]---> BDD-cost:   15
c ---[1740]---> BDD-cost:   19
c ---[1739]---> BDD-cost:   29
c ---[1737]---> BDD-cost:   19
c ---[1736]---> BDD-cost:   37
c ---[1735]---> BDD-cost:   37
c ---[1734]---> BDD-cost:   35
c ---[1733]---> BDD-cost:   29
c ---[1732]---> BDD-cost:   37
c ---[1731]---> BDD-cost:   29
c ---[1730]---> BDD-cost:   19
c ---[1729]---> BDD-cost:   37
c ---[1728]---> BDD-cost:   27
c ---[1726]---> BDD-cost:   19
c ---[1725]---> BDD-cost:   29
c ---[1724]---> BDD-cost:   27
c ---[1723]---> BDD-cost:   19
c ---[1722]---> BDD-cost:   31
c ---[1721]---> BDD-cost:   31
c ---[1720]---> BDD-cost:   29
c ---[1719]---> BDD-cost:   15
c ---[1718]---> BDD-cost:   25
c ---[1717]---> BDD-cost:    7
c ---[1715]---> BDD-cost:   19
c ---[1714]---> BDD-cost:    3
c ---[1713]---> BDD-cost:   27
c ---[1712]---> BDD-cost:   27
c ---[1711]---> BDD-cost:   31
c ---[1710]---> BDD-cost:   29
c ---[1709]---> BDD-cost:   31
c ---[1708]---> BDD-cost:   29
c ---[1707]---> BDD-cost:    7
c ---[1706]---> BDD-cost:   27
c ---[1703]---> BDD-cost:   19
c ---[1702]---> BDD-cost:   11
c ---[1701]---> BDD-cost:   27
c ---[1700]---> BDD-cost:   19
c ---[1699]---> BDD-cost:   37
c ---[1698]---> BDD-cost:   29
c ---[1697]---> BDD-cost:   31
c ---[1696]---> BDD-cost:   19
c ---[1695]---> BDD-cost:   19
c ---[1694]---> BDD-cost:   37
c ---[1692]---> BDD-cost:   21
c ---[1691]---> BDD-cost:   37
c ---[1690]---> BDD-cost:   27
c ---[1689]---> BDD-cost:   27
c ---[1688]---> BDD-cost:   19
c ---[1687]---> BDD-cost:   19
c ---[1686]---> BDD-cost:   31
c ---[1685]---> BDD-cost:   31
c ---[1684]---> BDD-cost:   19
c ---[1683]---> BDD-cost:   13
c ---[1681]---> BDD-cost:    7
c ---[1680]---> BDD-cost:   11
c ---[1679]---> BDD-cost:    5
c ---[1678]---> BDD-cost:    7
c ---[1677]---> BDD-cost:    7
c ---[1676]---> BDD-cost:    7
c ---[1675]---> BDD-cost:   27
c ---[1674]---> BDD-cost:   27
c ---[1673]---> BDD-cost:    7
c ---[1672]---> BDD-cost:    7
c ---[1670]---> BDD-cost:    7
c ---[1669]---> BDD-cost:    7
c ---[1668]---> BDD-cost:    3
c ---[1667]---> BDD-cost:    7
c ---[1666]---> BDD-cost:    7
c ---[1664]---> BDD-cost:    3
c ---[1663]---> BDD-cost:    9
c ---[1662]---> BDD-cost:    9
c ---[1660]---> BDD-cost:    9
c ---[1659]---> BDD-cost:   29
c ---[1658]---> BDD-cost:   29
c ---[1657]---> BDD-cost:   31
c ---[1656]---> BDD-cost:   31
c ---[1655]---> BDD-cost:   37
c ---[1654]---> BDD-cost:   37
c ---[1653]---> BDD-cost:   31
c ---[1652]---> BDD-cost:   25
c ---[1651]---> BDD-cost:   25
c ---[1649]---> BDD-cost:   33
c ---[1648]---> BDD-cost:   37
c ---[1647]---> BDD-cost:   31
c ---[1646]---> BDD-cost:   29
c ---[1645]---> BDD-cost:   29
c ---[1644]---> BDD-cost:   37
c ---[1643]---> BDD-cost:   31
c ---[1642]---> BDD-cost:   37
c ---[1641]---> BDD-cost:   15
c ---[1640]---> BDD-cost:   31
c ---[1638]---> BDD-cost:   37
c ---[1637]---> BDD-cost:   29
c ---[1636]---> BDD-cost:   29
c ---[1635]---> BDD-cost:   37
c ---[1634]---> BDD-cost:   29
c ---[1633]---> BDD-cost:   25
c ---[1632]---> BDD-cost:   31
c ---[1631]---> BDD-cost:   37
c ---[1629]---> BDD-cost:    9
c ---[1626]---> BDD-cost:   37
c ---[1625]---> BDD-cost:   25
c ---[1624]---> BDD-cost:   37
c ---[1623]---> BDD-cost:   25
c ---[1622]---> BDD-cost:   37
c ---[1621]---> BDD-cost:   11
c ---[1620]---> BDD-cost:   37
c ---[1619]---> BDD-cost:   37
c ---[1618]---> BDD-cost:   31
c ---[1616]---> BDD-cost:   29
c ---[1615]---> BDD-cost:   37
c ---[1614]---> BDD-cost:   27
c ---[1613]---> BDD-cost:   37
c ---[1612]---> BDD-cost:   37
c ---[1611]---> BDD-cost:   15
c ---[1610]---> BDD-cost:    7
c ---[1609]---> BDD-cost:   29
c ---[1608]---> BDD-cost:   31
c ---[1607]---> BDD-cost:   13
c ---[1605]---> BDD-cost:   37
c ---[1603]---> BDD-cost:    7
c ---[1602]---> BDD-cost:   19
c ---[1601]---> BDD-cost:    7
c ---[1600]---> BDD-cost:    5
c ---[1599]---> BDD-cost:   19
c ---[1598]---> BDD-cost:   19
c ---[1597]---> BDD-cost:   19
c ---[1596]---> BDD-cost:   27
c ---[1593]---> BDD-cost:    3
c ---[1592]---> BDD-cost:   37
c ---[1591]---> BDD-cost:   37
c ---[1590]---> BDD-cost:   37
c ---[1589]---> BDD-cost:   37
c ---[1588]---> BDD-cost:    3
c ---[1587]---> BDD-cost:   37
c ---[1586]---> BDD-cost:   27
c ---[1585]---> BDD-cost:   33
c ---[1584]---> BDD-cost:   37
c ---[1582]---> BDD-cost:   37
c ---[1581]---> BDD-cost:   25
c ---[1580]---> BDD-cost:   37
c ---[1579]---> BDD-cost:   37
c ---[1578]---> BDD-cost:    9
c ---[1577]---> BDD-cost:    9
c ---[1576]---> BDD-cost:    3
c ---[1572]---> BDD-cost:    5
c ---[1570]---> BDD-cost:    5
c ---[1569]---> BDD-cost:    5
c ---[1568]---> BDD-cost:    5
c ---[1567]---> BDD-cost:   27
c ---[1566]---> BDD-cost:   27
c ---[1565]---> BDD-cost:   27
c ---[1564]---> BDD-cost:   27
c ---[1562]---> BDD-cost:    9
c ---[1561]---> BDD-cost:    9
c ---[1560]---> BDD-cost:   27
c ---[1559]---> BDD-cost:   19
c ---[1558]---> BDD-cost:   19
c ---[1557]---> BDD-cost:    5
c ---[1556]---> BDD-cost:   11
c ---[1555]---> BDD-cost:    5
c ---[1554]---> BDD-cost:   11
c ---[1553]---> BDD-cost:   31
c ---[1551]---> BDD-cost:   31
c ---[1550]---> BDD-cost:   31
c ---[1549]---> BDD-cost:    7
c ---[1548]---> BDD-cost:   11
c ---[1547]---> BDD-cost:   27
c ---[1546]---> BDD-cost:   27
c ---[1545]---> BDD-cost:   19
c ---[1544]---> BDD-cost:    5
c ---[1543]---> BDD-cost:    3
c ---[1542]---> BDD-cost:   23
c ---[1540]---> BDD-cost:   37
c ---[1539]---> BDD-cost:   19
c ---[1538]---> BDD-cost:   19
c ---[1537]---> BDD-cost:   19
c ---[1536]---> BDD-cost:   19
c ---[1535]---> BDD-cost:   27
c ---[1534]---> BDD-cost:   19
c ---[1533]---> BDD-cost:   19
c ---[1532]---> BDD-cost:   27
c ---[1531]---> BDD-cost:   25
c ---[1529]---> BDD-cost:   27
c ---[1528]---> BDD-cost:   27
c ---[1527]---> BDD-cost:   27
c ---[1526]---> BDD-cost:   27
c ---[1525]---> BDD-cost:   19
c ---[1524]---> BDD-cost:   27
c ---[1523]---> BDD-cost:   27
c ---[1522]---> BDD-cost:   37
c ---[1521]---> BDD-cost:   27
c ---[1520]---> BDD-cost:    5
c ---[1518]---> BDD-cost:   19
c ---[1517]---> BDD-cost:    5
c ---[1516]---> BDD-cost:    5
c ---[1515]---> BDD-cost:    5
c ---[1514]---> BDD-cost:    5
c ---[1513]---> BDD-cost:    5
c ---[1512]---> BDD-cost:    5
c ---[1511]---> BDD-cost:    9
c ---[1510]---> BDD-cost:   27
c ---[1509]---> BDD-cost:    5
c ---[1507]---> BDD-cost:    3
c ---[1506]---> BDD-cost:    3
c ---[1505]---> BDD-cost:    3
c ---[1504]---> BDD-cost:    5
c ---[1503]---> BDD-cost:    5
c ---[1502]---> BDD-cost:    5
c ---[1501]---> BDD-cost:   27
c ---[1500]---> BDD-cost:   35
c ---[1499]---> BDD-cost:   15
c ---[1498]---> BDD-cost:   27
c ---[1496]---> BDD-cost:   27
c ---[1495]---> BDD-cost:   27
c ---[1494]---> BDD-cost:   37
c ---[1493]---> BDD-cost:   27
c ---[1492]---> BDD-cost:   37
c ---[1491]---> BDD-cost:    9
c ---[1490]---> BDD-cost:    9
c ---[1489]---> BDD-cost:    9
c ---[1484]---> BDD-cost:   11
c ---[1483]---> BDD-cost:    3
c ---[1482]---> BDD-cost:   13
c ---[1481]---> BDD-cost:    9
c ---[1480]---> BDD-cost:   19
c ---[1479]---> BDD-cost:   27
c ---[1478]---> BDD-cost:   19
c ---[1477]---> BDD-cost:   27
c ---[1476]---> BDD-cost:   27
c ---[1475]---> BDD-cost:   27
c ---[1473]---> BDD-cost:   27
c ---[1472]---> BDD-cost:    3
c ---[1471]---> BDD-cost:   37
c ---[1470]---> BDD-cost:   29
c ---[1469]---> BDD-cost:   33
c ---[1468]---> BDD-cost:   29
c ---[1467]---> BDD-cost:   37
c ---[1466]---> BDD-cost:    3
c ---[1464]---> BDD-cost:    3
c ---[1462]---> BDD-cost:    3
c ---[1461]---> BDD-cost:    3
c ---[1460]---> BDD-cost:    3
c ---[1459]---> BDD-cost:    5
c ---[1458]---> BDD-cost:   27
c ---[1457]---> BDD-cost:   19
c ---[1456]---> BDD-cost:    5
c ---[1455]---> BDD-cost:    7
c ---[1453]---> BDD-cost:    9
c ---[1452]---> BDD-cost:   13
c ---[1451]---> BDD-cost:    7
c ---[1450]---> BDD-cost:   19
c ---[1449]---> BDD-cost:   23
c ---[1448]---> BDD-cost:    5
c ---[1447]---> BDD-cost:    5
c ---[1446]---> BDD-cost:   19
c ---[1445]---> BDD-cost:   27
c ---[1444]---> BDD-cost:    5
c ---[1442]---> BDD-cost:   19
c ---[1441]---> BDD-cost:   27
c ---[1440]---> BDD-cost:   27
c ---[1439]---> BDD-cost:   27
c ---[1438]---> BDD-cost:   27
c ---[1437]---> BDD-cost:   27
c ---[1436]---> BDD-cost:   25
c ---[1435]---> BDD-cost:   19
c ---[1434]---> BDD-cost:   23
c ---[1433]---> BDD-cost:    3
c ---[1431]---> BDD-cost:   27
c ---[1430]---> BDD-cost:   27
c ---[1429]---> BDD-cost:   27
c ---[1428]---> BDD-cost:   27
c ---[1427]---> BDD-cost:   27
c ---[1426]---> BDD-cost:   27
c ---[1425]---> BDD-cost:    3
c ---[1424]---> BDD-cost:    3
c ---[1423]---> BDD-cost:    3
c ---[1422]---> BDD-cost:    3
c ---[1420]---> BDD-cost:    7
c ---[1419]---> BDD-cost:    7
c ---[1417]---> BDD-cost:    3
c ---[1416]---> BDD-cost:    7
c ---[1415]---> BDD-cost:    7
c ---[1413]---> BDD-cost:   27
c ---[1409]---> BDD-cost:   19
c ---[1408]---> BDD-cost:   37
c ---[1407]---> BDD-cost:   19
c ---[1406]---> BDD-cost:   23
c ---[1405]---> BDD-cost:   29
c ---[1404]---> BDD-cost:   31
c ---[1403]---> BDD-cost:   31
c ---[1401]---> BDD-cost:   37
c ---[1400]---> BDD-cost:   11
c ---[1399]---> BDD-cost:   11
c ---[1398]---> BDD-cost:    5
c ---[1396]---> BDD-cost:    5
c ---[1395]---> BDD-cost:   11
c ---[1394]---> BDD-cost:   21
c ---[1393]---> BDD-cost:   37
c ---[1392]---> BDD-cost:   31
c ---[1390]---> BDD-cost:    5
c ---[1389]---> BDD-cost:   31
c ---[1388]---> BDD-cost:   19
c ---[1387]---> BDD-cost:   29
c ---[1386]---> BDD-cost:   37
c ---[1385]---> BDD-cost:   29
c ---[1384]---> BDD-cost:   31
c ---[1383]---> BDD-cost:   21
c ---[1382]---> BDD-cost:    5
c ---[1378]---> BDD-cost:   31
c ---[1377]---> BDD-cost:   37
c ---[1376]---> BDD-cost:   29
c ---[1375]---> BDD-cost:   31
c ---[1374]---> BDD-cost:   27
c ---[1373]---> BDD-cost:   19
c ---[1372]---> BDD-cost:   37
c ---[1371]---> BDD-cost:   37
c ---[1370]---> BDD-cost:   29
c ---[1369]---> BDD-cost:   19
c ---[1367]---> BDD-cost:   37
c ---[1366]---> BDD-cost:   23
c ---[1365]---> BDD-cost:   35
c ---[1364]---> BDD-cost:   37
c ---[1363]---> BDD-cost:   19
c ---[1362]---> BDD-cost:   19
c ---[1361]---> BDD-cost:   23
c ---[1360]---> BDD-cost:   15
c ---[1359]---> BDD-cost:   15
c ---[1358]---> BDD-cost:    9
c ---[1357]---> BDD-cost: 6392
c ---[1356]---> BDD-cost:    3
c ---[1355]---> BDD-cost:   21
c ---[1354]---> BDD-cost:   23
c ---[1353]---> BDD-cost:   19
c ---[1352]---> BDD-cost:   19
c ---[1351]---> BDD-cost:   23
c ---[1350]---> BDD-cost:    7
c ---[1349]---> BDD-cost:   27
c ---[1348]---> BDD-cost:   37
c ---[1347]---> BDD-cost:   29
c ---[1346]---> Adder-cost: 4750   maxlim: 20   bits: 6/5
c ---[1345]---> BDD-cost:   37
c ---[1344]---> BDD-cost:   15
c ---[1343]---> BDD-cost:   27
c ---[1342]---> BDD-cost:   27
c ---[1341]---> BDD-cost:   27
c ---[1340]---> BDD-cost:   27
c ---[1339]---> BDD-cost:   27
c ---[1338]---> BDD-cost:   31
c ---[1337]---> BDD-cost:   25
c ---[1336]---> BDD-cost:   27
c ---[1334]---> BDD-cost:   27
c ---[1333]---> BDD-cost:   27
c ---[1332]---> BDD-cost:   37
c ---[1331]---> BDD-cost:   15
c ---[1330]---> BDD-cost:    3
c ---[1329]---> BDD-cost:    7
c ---[1328]---> BDD-cost:    5
c ---[1327]---> BDD-cost:    5
c ---[1325]---> BDD-cost:   27
c ---[1324]---> BDD-cost:   27
c ---[1323]---> BDD-cost:   27
c ---[1322]---> BDD-cost:   27
c ---[1321]---> BDD-cost:   11
c ---[1319]---> BDD-cost:    3
c ---[1317]---> BDD-cost:    3
c ---[1316]---> BDD-cost:    3
c ---[1305]---> BDD-cost: 6529
c ---[1225]---> BDD-cost: 4492
c ---[1160]---> Adder-cost: 4287   maxlim: 12   bits: 5/4
c ---[1135]---> Adder-cost: 1014   maxlim: 12   bits: 5/4
c ---[1115]---> BDD-cost:   19
c ---[1054]---> BDD-cost: 2117
c ---[ 898]---> BDD-cost:   19
c ---[ 897]---> BDD-cost:   19
c ---[ 896]---> BDD-cost:   27
c ---[ 895]---> BDD-cost:   27
c ---[ 894]---> BDD-cost:   15
c ---[ 893]---> BDD-cost:   29
c ---[ 892]---> BDD-cost:   23
c ---[ 891]---> BDD-cost:   29
c ---[ 890]---> BDD-cost:   27
c ---[ 889]---> BDD-cost:   29
c ---[ 887]---> BDD-cost:   19
c ---[ 886]---> BDD-cost:   21
c ---[ 885]---> BDD-cost:   17
c ---[ 884]---> BDD-cost:   29
c ---[ 883]---> BDD-cost:   37
c ---[ 882]---> BDD-cost:   37
c ---[ 881]---> BDD-cost:   37
c ---[ 880]---> BDD-cost:   27
c ---[ 879]---> BDD-cost:   27
c ---[ 878]---> BDD-cost:   27
c ---[ 876]---> BDD-cost:   19
c ---[ 875]---> BDD-cost:   27
c ---[ 874]---> BDD-cost:   19
c ---[ 873]---> BDD-cost:   37
c ---[ 872]---> BDD-cost:   15
c ---[ 871]---> BDD-cost:   27
c ---[ 870]---> BDD-cost:   15
c ---[ 869]---> BDD-cost:    5
c ---[ 868]---> BDD-cost:   19
c ---[ 867]---> BDD-cost:   27
c ---[ 865]---> BDD-cost:   23
c ---[ 864]---> BDD-cost:   23
c ---[ 863]---> BDD-cost:   23
c ---[ 862]---> BDD-cost:   23
c ---[ 861]---> BDD-cost:   19
c ---[ 860]---> BDD-cost:   31
c ---[ 859]---> BDD-cost:   19
c ---[ 858]---> BDD-cost:   19
c ---[ 857]---> BDD-cost:    3
c ---[ 856]---> BDD-cost:   19
c ---[ 854]---> BDD-cost:    5
c ---[ 853]---> BDD-cost:   27
c ---[ 852]---> BDD-cost:   19
c ---[ 851]---> BDD-cost:   19
c ---[ 850]---> BDD-cost:   19
c ---[ 849]---> BDD-cost:    9
c ---[ 848]---> BDD-cost:   27
c ---[ 847]---> BDD-cost:   19
c ---[ 846]---> BDD-cost:   23
c ---[ 845]---> BDD-cost:   23
c ---[ 842]---> BDD-cost:   23
c ---[ 841]---> BDD-cost:    3
c ---[ 840]---> BDD-cost:   19
c ---[ 839]---> BDD-cost:   19
c ---[ 838]---> BDD-cost:   23
c ---[ 837]---> BDD-cost:   19
c ---[ 836]---> BDD-cost:   19
c ---[ 835]---> BDD-cost:   19
c ---[ 834]---> BDD-cost:   19
c ---[ 833]---> BDD-cost:   19
c ---[ 831]---> BDD-cost:   23
c ---[ 830]---> BDD-cost:   23
c ---[ 829]---> BDD-cost:   19
c ---[ 828]---> BDD-cost:   19
c ---[ 827]---> BDD-cost:   19
c ---[ 826]---> BDD-cost:    5
c ---[ 825]---> BDD-cost:   27
c ---[ 824]---> BDD-cost:   23
c ---[ 823]---> BDD-cost:   19
c ---[ 822]---> BDD-cost:   19
c ---[ 820]---> BDD-cost:   19
c ---[ 819]---> BDD-cost:   19
c ---[ 818]---> BDD-cost:   19
c ---[ 817]---> BDD-cost:   23
c ---[ 816]---> BDD-cost:   23
c ---[ 815]---> BDD-cost:   23
c ---[ 814]---> BDD-cost:   23
c ---[ 813]---> BDD-cost:    5
c ---[ 812]---> BDD-cost:   19
c ---[ 811]---> BDD-cost:   19
c ---[ 809]---> BDD-cost:   19
c ---[ 808]---> BDD-cost:   19
c ---[ 807]---> BDD-cost:   19
c ---[ 806]---> BDD-cost:   19
c ---[ 805]---> BDD-cost:   19
c ---[ 804]---> BDD-cost:   19
c ---[ 803]---> BDD-cost:   19
c ---[ 802]---> BDD-cost:   19
c ---[ 801]---> BDD-cost:   25
c ---[ 800]---> BDD-cost:   25
c ---[ 799]---> BDD-cost: 7839
c ---[ 798]---> BDD-cost:   23
c ---[ 797]---> BDD-cost:   23
c ---[ 796]---> BDD-cost:   23
c ---[ 795]---> BDD-cost:   25
c ---[ 794]---> BDD-cost:   23
c ---[ 793]---> BDD-cost:   25
c ---[ 792]---> BDD-cost:    5
c ---[ 791]---> BDD-cost:   31
c ---[ 790]---> BDD-cost:   27
c ---[ 789]---> BDD-cost:    3
c ---[ 787]---> BDD-cost:    3
c ---[ 786]---> BDD-cost:   27
c ---[ 785]---> BDD-cost:   27
c ---[ 784]---> BDD-cost:   27
c ---[ 783]---> BDD-cost:   27
c ---[ 782]---> BDD-cost:   27
c ---[ 781]---> BDD-cost:    9
c ---[ 780]---> BDD-cost:    5
c ---[ 779]---> BDD-cost:    3
c ---[ 778]---> BDD-cost:    3
c ---[ 777]---> BDD-cost: 6871
c ---[ 776]---> BDD-cost:    3
c ---[ 775]---> BDD-cost:   25
c ---[ 774]---> BDD-cost:   27
c ---[ 773]---> BDD-cost:   29
c ---[ 772]---> BDD-cost:   27
c ---[ 771]---> BDD-cost:   27
c ---[ 770]---> BDD-cost:   29
c ---[ 769]---> BDD-cost:   27
c ---[ 768]---> BDD-cost:   25
c ---[ 767]---> BDD-cost:   37
c ---[ 766]---> Adder-cost: 4736   maxlim: 26   bits: 6/5
c ---[ 765]---> BDD-cost:   37
c ---[ 764]---> BDD-cost:   27
c ---[ 763]---> BDD-cost:   37
c ---[ 762]---> BDD-cost:   27
c ---[ 761]---> BDD-cost:   27
c ---[ 760]---> BDD-cost:   27
c ---[ 759]---> BDD-cost:   27
c ---[ 758]---> BDD-cost:   27
c ---[ 757]---> BDD-cost:   31
c ---[ 756]---> BDD-cost:   31
c ---[ 754]---> BDD-cost:   27
c ---[ 753]---> BDD-cost:   25
c ---[ 752]---> BDD-cost:   37
c ---[ 751]---> BDD-cost:   37
c ---[ 750]---> BDD-cost:   37
c ---[ 749]---> BDD-cost:   27
c ---[ 748]---> BDD-cost:   25
c ---[ 747]---> BDD-cost:   27
c ---[ 746]---> BDD-cost:    9
c ---[ 745]---> BDD-cost:   25
c ---[ 743]---> BDD-cost:   27
c ---[ 742]---> BDD-cost:   27
c ---[ 741]---> BDD-cost:   27
c ---[ 740]---> BDD-cost:   37
c ---[ 739]---> BDD-cost:   37
c ---[ 738]---> BDD-cost:   27
c ---[ 737]---> BDD-cost:   27
c ---[ 736]---> BDD-cost:   27
c ---[ 735]---> BDD-cost:   37
c ---[ 734]---> BDD-cost:   27
c ---[ 731]---> BDD-cost:   27
c ---[ 730]---> BDD-cost:   37
c ---[ 729]---> BDD-cost:    5
c ---[ 728]---> BDD-cost:    5
c ---[ 727]---> BDD-cost:   37
c ---[ 725]---> BDD-cost:   27
c ---[ 724]---> BDD-cost:   31
c ---[ 723]---> BDD-cost:   19
c ---[ 720]---> BDD-cost:   27
c ---[ 719]---> BDD-cost:   27
c ---[ 718]---> BDD-cost:   37
c ---[ 717]---> BDD-cost:   37
c ---[ 716]---> BDD-cost:   19
c ---[ 715]---> BDD-cost:   27
c ---[ 714]---> BDD-cost:   23
c ---[ 712]---> BDD-cost:    3
c ---[ 711]---> BDD-cost:   27
c ---[ 709]---> BDD-cost:    5
c ---[ 708]---> BDD-cost:    7
c ---[ 707]---> BDD-cost:   27
c ---[ 706]---> BDD-cost:   27
c ---[ 705]---> BDD-cost:   27
c ---[ 704]---> BDD-cost:   27
c ---[ 703]---> BDD-cost:   27
c ---[ 702]---> BDD-cost:   27
c ---[ 701]---> BDD-cost:   27
c ---[ 700]---> BDD-cost:   27
c ---[ 698]---> BDD-cost:   27
c ---[ 697]---> BDD-cost:   27
c ---[ 696]---> BDD-cost:   19
c ---[ 695]---> BDD-cost:    3
c ---[ 694]---> BDD-cost:    7
c ---[ 693]---> BDD-cost:   19
c ---[ 692]---> BDD-cost:    9
c ---[ 691]---> BDD-cost:   37
c ---[ 690]---> BDD-cost:   37
c ---[ 689]---> BDD-cost:   37
c ---[ 687]---> BDD-cost:   27
c ---[ 686]---> BDD-cost:   27
c ---[ 685]---> BDD-cost:    5
c ---[ 684]---> BDD-cost:   19
c ---[ 683]---> BDD-cost:    5
c ---[ 682]---> BDD-cost:   27
c ---[ 681]---> BDD-cost:   27
c ---[ 680]---> BDD-cost:   27
c ---[ 679]---> BDD-cost:   27
c ---[ 678]---> BDD-cost:   19
c ---[ 675]---> BDD-cost:   29
c ---[ 674]---> BDD-cost:   19
c ---[ 673]---> BDD-cost:   27
c ---[ 672]---> BDD-cost:   19
c ---[ 671]---> BDD-cost:   27
c ---[ 670]---> BDD-cost:   19
c ---[ 669]---> BDD-cost:    3
c ---[ 668]---> BDD-cost:    3
c ---[ 667]---> BDD-cost:   19
c ---[ 664]---> BDD-cost:   27
c ---[ 663]---> BDD-cost:    3
c ---[ 662]---> BDD-cost:   27
c ---[ 661]---> BDD-cost:   37
c ---[ 660]---> BDD-cost:   27
c ---[ 659]---> BDD-cost:   27
c ---[ 658]---> BDD-cost:   27
c ---[ 657]---> BDD-cost:   27
c ---[ 656]---> BDD-cost:   15
c ---[ 654]---> BDD-cost:   27
c ---[ 653]---> BDD-cost:   27
c ---[ 652]---> BDD-cost:   27
c ---[ 651]---> BDD-cost:   27
c ---[ 650]---> BDD-cost:   25
c ---[ 649]---> BDD-cost:   37
c ---[ 648]---> BDD-cost:   31
c ---[ 647]---> BDD-cost:   37
c ---[ 646]---> BDD-cost:    5
c ---[ 645]---> BDD-cost:   19
c ---[ 643]---> BDD-cost:   27
c ---[ 642]---> BDD-cost:    3
c ---[ 640]---> BDD-cost:   19
c ---[ 638]---> BDD-cost:    3
c ---[ 636]---> BDD-cost:   31
c ---[ 635]---> BDD-cost:   23
c ---[ 634]---> BDD-cost:   25
c ---[ 632]---> BDD-cost:   37
c ---[ 631]---> BDD-cost:   31
c ---[ 630]---> BDD-cost:   27
c ---[ 629]---> BDD-cost:   19
c ---[ 628]---> BDD-cost:   27
c ---[ 627]---> BDD-cost:   19
c ---[ 626]---> BDD-cost:   19
c ---[ 625]---> BDD-cost:   19
c ---[ 624]---> BDD-cost:   37
c ---[ 623]---> BDD-cost:   37
c ---[ 620]---> BDD-cost:   27
c ---[ 619]---> BDD-cost:   27
c ---[ 618]---> BDD-cost:   27
c ---[ 617]---> BDD-cost:   19
c ---[ 616]---> BDD-cost:   27
c ---[ 615]---> BDD-cost:   27
c ---[ 614]---> BDD-cost:   37
c ---[ 613]---> BDD-cost:   25
c ---[ 612]---> BDD-cost:   19
c ---[ 611]---> BDD-cost:   19
c ---[ 609]---> BDD-cost:   13
c ---[ 608]---> BDD-cost:   19
c ---[ 607]---> BDD-cost:   19
c ---[ 606]---> BDD-cost:   19
c ---[ 605]---> BDD-cost:    7
c ---[ 604]---> BDD-cost:    7
c ---[ 603]---> BDD-cost:   27
c ---[ 602]---> BDD-cost:   27
c ---[ 601]---> BDD-cost:    5
c ---[ 600]---> BDD-cost: 8648
c ---[ 599]---> BDD-cost:    7
c ---[ 598]---> BDD-cost:    5
c ---[ 597]---> BDD-cost:    3
c ---[ 596]---> BDD-cost:    7
c ---[ 595]---> BDD-cost:   35
c ---[ 594]---> BDD-cost:   37
c ---[ 593]---> BDD-cost:   19
c ---[ 592]---> BDD-cost:   31
c ---[ 591]---> BDD-cost:   15
c ---[ 589]---> BDD-cost:   25
c ---[ 588]---> BDD-cost:   15
c ---[ 587]---> BDD-cost:   37
c ---[ 586]---> BDD-cost:   37
c ---[ 585]---> BDD-cost:   29
c ---[ 584]---> BDD-cost:    3
c ---[ 583]---> BDD-cost:    7
c ---[ 582]---> BDD-cost:   19
c ---[ 580]---> BDD-cost:    7
c ---[ 578]---> BDD-cost:   37
c ---[ 577]---> BDD-cost:   27
c ---[ 576]---> BDD-cost:   27
c ---[ 575]---> BDD-cost:   25
c ---[ 574]---> BDD-cost:   27
c ---[ 573]---> BDD-cost:   27
c ---[ 572]---> BDD-cost:   27
c ---[ 571]---> BDD-cost:    3
c ---[ 567]---> BDD-cost:   33
c ---[ 566]---> BDD-cost:   29
c ---[ 565]---> BDD-cost:   31
c ---[ 564]---> BDD-cost:   37
c ---[ 563]---> BDD-cost:   31
c ---[ 562]---> BDD-cost:   15
c ---[ 561]---> BDD-cost:   13
c ---[ 560]---> BDD-cost:   29
c ---[ 559]---> BDD-cost:   37
c ---[ 557]---> BDD-cost:   13
c ---[ 556]---> BDD-cost:   37
c ---[ 555]---> BDD-cost:   27
c ---[ 554]---> BDD-cost:   27
c ---[ 553]---> BDD-cost:   19
c ---[ 552]---> BDD-cost:   15
c ---[ 551]---> BDD-cost:   37
c ---[ 550]---> BDD-cost:   15
c ---[ 549]---> BDD-cost:   27
c ---[ 548]---> BDD-cost:   29
c ---[ 546]---> BDD-cost:   29
c ---[ 545]---> BDD-cost:   31
c ---[ 544]---> BDD-cost:   37
c ---[ 543]---> BDD-cost:   37
c ---[ 542]---> BDD-cost:   31
c ---[ 541]---> BDD-cost:   29
c ---[ 540]---> BDD-cost:   31
c ---[ 539]---> BDD-cost:   31
c ---[ 538]---> BDD-cost:   31
c ---[ 537]---> BDD-cost:   37
c ---[ 535]---> BDD-cost:   31
c ---[ 534]---> BDD-cost:   31
c ---[ 533]---> BDD-cost:   31
c ---[ 532]---> BDD-cost:   29
c ---[ 531]---> BDD-cost:   29
c ---[ 530]---> BDD-cost:   29
c ---[ 529]---> BDD-cost:   29
c ---[ 528]---> BDD-cost:   31
c ---[ 527]---> BDD-cost:   37
c ---[ 526]---> BDD-cost:   37
c ---[ 524]---> BDD-cost:   37
c ---[ 523]---> BDD-cost:   37
c ---[ 522]---> BDD-cost:   35
c ---[ 521]---> BDD-cost:   33
c ---[ 520]---> BDD-cost:   37
c ---[ 519]---> BDD-cost:   35
c ---[ 518]---> BDD-cost:   37
c ---[ 517]---> BDD-cost:   31
c ---[ 516]---> BDD-cost:   31
c ---[ 515]---> BDD-cost:   31
c ---[ 512]---> BDD-cost:   33
c ---[ 511]---> BDD-cost:   37
c ---[ 510]---> BDD-cost:   31
c ---[ 509]---> BDD-cost:   31
c ---[ 508]---> BDD-cost:   31
c ---[ 507]---> BDD-cost:   31
c ---[ 506]---> BDD-cost:   29
c ---[ 505]---> BDD-cost:   31
c ---[ 504]---> BDD-cost:   37
c ---[ 503]---> BDD-cost:   29
c ---[ 501]---> BDD-cost:   37
c ---[ 500]---> BDD-cost:   33
c ---[ 499]---> BDD-cost:   31
c ---[ 498]---> BDD-cost:   29
c ---[ 497]---> BDD-cost:   31
c ---[ 496]---> BDD-cost:   29
c ---[ 495]---> BDD-cost:   31
c ---[ 494]---> BDD-cost:   35
c ---[ 493]---> BDD-cost:   37
c ---[ 492]---> BDD-cost:   29
c ---[ 490]---> BDD-cost:   29
c ---[ 489]---> BDD-cost:   31
c ---[ 488]---> BDD-cost:   31
c ---[ 487]---> BDD-cost:   35
c ---[ 485]---> BDD-cost:    5
c ---[ 484]---> BDD-cost:    3
c ---[ 483]---> BDD-cost:    9
c ---[ 482]---> BDD-cost:    9
c ---[ 481]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:   19
c ---[ 478]---> BDD-cost:   19
c ---[ 477]---> BDD-cost:   37
c ---[ 476]---> BDD-cost:   37
c ---[ 475]---> BDD-cost:   29
c ---[ 474]---> BDD-cost:    5
c ---[ 473]---> BDD-cost:   13
c ---[ 472]---> BDD-cost:    9
c ---[ 471]---> BDD-cost:   11
c ---[ 470]---> BDD-cost:    3
c ---[ 468]---> BDD-cost:   31
c ---[ 467]---> BDD-cost:   21
c ---[ 466]---> BDD-cost:   23
c ---[ 465]---> BDD-cost:   19
c ---[ 464]---> BDD-cost:    5
c ---[ 463]---> BDD-cost:    5
c ---[ 462]---> BDD-cost:    7
c ---[ 461]---> BDD-cost:    7
c ---[ 460]---> BDD-cost:   19
c ---[ 459]---> BDD-cost:   19
c ---[ 457]---> BDD-cost:   37
c ---[ 456]---> BDD-cost:    5
c ---[ 455]---> BDD-cost:   11
c ---[ 454]---> BDD-cost:   31
c ---[ 453]---> BDD-cost:   31
c ---[ 451]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:    9
c ---[ 449]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:    5
c ---[ 446]---> BDD-cost:   19
c ---[ 445]---> BDD-cost:   23
c ---[ 443]---> BDD-cost:   27
c ---[ 442]---> BDD-cost:   27
c ---[ 441]---> BDD-cost:   19
c ---[ 440]---> BDD-cost:    3
c ---[ 439]---> BDD-cost:   37
c ---[ 438]---> BDD-cost:   27
c ---[ 437]---> BDD-cost:   27
c ---[ 435]---> BDD-cost:   27
c ---[ 434]---> BDD-cost:   19
c ---[ 433]---> BDD-cost:   27
c ---[ 432]---> BDD-cost:   27
c ---[ 431]---> BDD-cost:   27
c ---[ 430]---> BDD-cost:   19
c ---[ 428]---> BDD-cost:    3
c ---[ 424]---> BDD-cost:    3
c ---[ 423]---> BDD-cost:    9
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    5
c ---[ 420]---> BDD-cost:   19
c ---[ 419]---> BDD-cost:   19
c ---[ 418]---> BDD-cost:    3
c ---[ 417]---> BDD-cost:    5
c ---[ 416]---> BDD-cost:   27
c ---[ 415]---> BDD-cost:    5
c ---[ 413]---> BDD-cost:   27
c ---[ 412]---> BDD-cost:   27
c ---[ 411]---> BDD-cost:   19
c ---[ 410]---> BDD-cost:    3
c ---[ 409]---> BDD-cost:    7
c ---[ 408]---> BDD-cost:   37
c ---[ 407]---> BDD-cost:   37
c ---[ 406]---> BDD-cost:   27
c ---[ 405]---> BDD-cost:   27
c ---[ 404]---> BDD-cost:   27
c ---[ 403]---> BDD-cost: 2076
c ---[ 402]---> BDD-cost:  908
c ---[ 401]---> BDD-cost:  282
c ---[ 400]---> BDD-cost:   66
c ---[ 399]---> BDD-cost:   24
c ---[ 398]---> BDD-cost:  458
c ---[ 397]---> BDD-cost:    1
c ---[ 396]---> BDD-cost:  142
c ---[ 395]---> BDD-cost:   69
c ---[ 394]---> BDD-cost:   69
c ---[ 393]---> BDD-cost:  188
c ---[ 392]---> BDD-cost:   60
c ---[ 391]---> BDD-cost:  286
c ---[ 390]---> BDD-cost:   76
c ---[ 389]---> BDD-cost:  136
c ---[ 388]---> BDD-cost:  212
c ---[ 387]---> BDD-cost:  286
c ---[ 386]---> BDD-cost: 1841
c ---[ 385]---> BDD-cost: 2354
c ---[ 384]---> Adder-cost: 957   maxlim: 14   bits: 5/4
c ---[ 383]---> BDD-cost:   62
c ---[ 382]---> BDD-cost:   70
c ---[ 381]---> BDD-cost:   36
c ---[ 380]---> BDD-cost:   22
c ---[ 379]---> BDD-cost:   32
c ---[ 378]---> BDD-cost:   56
c ---[ 377]---> BDD-cost: 1461
c ---[ 376]---> BDD-cost: 1569
c ---[ 375]---> BDD-cost:  846
c ---[ 374]---> BDD-cost:   95
c ---[ 373]---> BDD-cost:  151
c ---[ 372]---> BDD-cost:  371
c ---[ 371]---> BDD-cost:  296
c ---[ 370]---> BDD-cost:  521
c ---[ 369]---> BDD-cost:  151
c ---[ 368]---> Adder-cost: 110   maxlim: 11   bits: 5/4
c ---[ 367]---> BDD-cost: 3498
c ---[ 366]---> BDD-cost:  238
c ---[ 365]---> BDD-cost:   72
c ---[ 364]---> BDD-cost:   24
c ---[ 363]---> BDD-cost:   12
c ---[ 362]---> BDD-cost:   70
c ---[ 361]---> BDD-cost:    6
c ---[ 360]---> BDD-cost:  108
c ---[ 359]---> BDD-cost:   38
c ---[ 358]---> BDD-cost: 3147
c ---[ 357]---> BDD-cost:   56
c ---[ 356]---> BDD-cost:   74
c ---[ 355]---> BDD-cost:  116
c ---[ 354]---> BDD-cost:   28
c ---[ 353]---> BDD-cost:  302
c ---[ 352]---> BDD-cost:   72
c ---[ 351]---> BDD-cost:   78
c ---[ 350]---> BDD-cost:  663
c ---[ 349]---> BDD-cost: 1344
c ---[ 348]---> BDD-cost:  277
c ---[ 347]---> BDD-cost:  114
c ---[ 346]---> BDD-cost:   26
c ---[ 345]---> BDD-cost:  996
c ---[ 344]---> BDD-cost:   14
c ---[ 343]---> BDD-cost:    8
c ---[ 342]---> BDD-cost:  124
c ---[ 341]---> BDD-cost:   28
c ---[ 340]---> BDD-cost:  511
c ---[ 339]---> BDD-cost: 1291
c ---[ 338]---> BDD-cost:  595
c ---[ 337]---> BDD-cost: 1788
c ---[ 336]---> BDD-cost: 2664
c ---[ 335]---> BDD-cost: 2280
c ---[ 334]---> BDD-cost: 3516
c ---[ 333]---> BDD-cost:   38
c ---[ 332]---> BDD-cost: 2211
c ---[ 331]---> BDD-cost: 2709
c ---[ 330]---> BDD-cost:   24
c ---[ 329]---> BDD-cost:   92
c ---[ 328]---> BDD-cost:   46
c ---[ 327]---> BDD-cost:  312
c ---[ 326]---> BDD-cost:   94
c ---[ 325]---> BDD-cost:   44
c ---[ 324]---> BDD-cost:   20
c ---[ 323]---> BDD-cost:   62
c ---[ 322]---> BDD-cost:    8
c ---[ 321]---> BDD-cost:  306
c ---[ 320]---> BDD-cost:  342
c ---[ 319]---> BDD-cost: 4547
c ---[ 318]---> BDD-cost:  548
c ---[ 317]---> BDD-cost:  781
c ---[ 316]---> BDD-cost:  627
c ---[ 315]---> BDD-cost: 1748
c ---[ 314]---> BDD-cost:  720
c ---[ 313]---> BDD-cost:  880
c ---[ 312]---> BDD-cost: 3295
c ---[ 311]---> BDD-cost: 1668
c ---[ 310]---> BDD-cost: 2411
c ---[ 309]---> BDD-cost: 2415
c ---[ 308]---> BDD-cost: 2403
c ---[ 307]---> BDD-cost:  860
c ---[ 306]---> BDD-cost:  462
c ---[ 305]---> BDD-cost:  176
c ---[ 304]---> BDD-cost: 1611
c ---[ 303]---> BDD-cost:  871
c ---[ 302]---> BDD-cost:  949
c ---[ 301]---> BDD-cost:  196
c ---[ 300]---> BDD-cost:  221
c ---[ 299]---> BDD-cost: 2254
c ---[ 298]---> BDD-cost: 2011
c ---[ 297]---> BDD-cost: 3585
c ---[ 296]---> BDD-cost:  277
c ---[ 295]---> BDD-cost:  303
c ---[ 294]---> BDD-cost: 3565
c ---[ 293]---> BDD-cost:  498
c ---[ 292]---> BDD-cost: 2702
c ---[ 291]---> BDD-cost:  954
c ---[ 290]---> BDD-cost: 1050
c ---[ 289]---> BDD-cost:  997
c ---[ 288]---> BDD-cost: 1251
c ---[ 287]---> BDD-cost: 2066
c ---[ 286]---> BDD-cost: 2373
c ---[ 285]---> BDD-cost:  250
c ---[ 284]---> BDD-cost:  280
c ---[ 283]---> BDD-cost:  158
c ---[ 282]---> BDD-cost:  834
c ---[ 281]---> BDD-cost: 3948
c ---[ 280]---> BDD-cost: 4777
c ---[ 279]---> BDD-cost: 4829
c ---[ 278]---> BDD-cost: 2776
c ---[ 277]---> BDD-cost:  178
c ---[ 276]---> BDD-cost:  203
c ---[ 275]---> BDD-cost: 1409
c ---[ 274]---> BDD-cost:  106
c ---[ 273]---> BDD-cost:  121
c ---[ 272]---> BDD-cost:  290
c ---[ 271]---> BDD-cost: 1672
c ---[ 270]---> BDD-cost: 2035
c ---[ 269]---> BDD-cost:  610
c ---[ 268]---> BDD-cost:  675
c ---[ 267]---> BDD-cost: 1359
c ---[ 266]---> BDD-cost: 1630
c ---[

Watcher Data

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/19108/stat): 19108 (minisat+_script) R 19107 19108 824 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1793571639 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/19108/statm): 174 3 169 147 0 27 0
[pid=19108] 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=19109
New process pid=19110
New process pid=19111
execve syscall for /bin/sed executable
One traced child (pid=19110) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=19111) exited with status: 0
One traced child (pid=19109) exited with status: 0
New process pid=19112
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-sp97ar.opb
One traced child (pid=19112) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=19113
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-sp97ar.opb

[startup+10.0039 s]
Raw data (loadavg): 0.96 0.96 0.71 1/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) T 19108 19108 824 0 -1 0 12132 0 0 0 879 58 0 0 23 0 1 0 1793571649 68308992 11498 4294967295 134512640 135167914 3221224448 3221223100 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/19113/statm): 16677 11498 162 162 0 16515 0
[pid=19113] vsize: 66708
Current children cumulated CPU time (s) 9.42
Current children cumulated vsize (Kb) 68836

[startup+20.0046 s]
Raw data (loadavg): 0.97 0.96 0.71 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 15005 0 0 0 1847 72 0 0 25 0 1 0 1793571649 72560640 12694 4294967295 134512640 135167914 3221224448 3221222864 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 17715 12694 162 162 0 17553 0
[pid=19113] vsize: 70860
Current children cumulated CPU time (s) 19.24
Current children cumulated vsize (Kb) 72988

[startup+30.0053 s]
Raw data (loadavg): 0.97 0.96 0.71 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 16442 0 0 0 2827 83 0 0 25 0 1 0 1793571649 75698176 12995 4294967295 134512640 135167914 3221224448 3221222800 134516620 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 18481 12995 162 162 0 18319 0
[pid=19113] vsize: 73924
Current children cumulated CPU time (s) 29.15
Current children cumulated vsize (Kb) 76052

[startup+40.0061 s]
Raw data (loadavg): 0.98 0.96 0.72 1/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) T 19108 19108 824 0 -1 0 18949 0 0 0 3796 98 0 0 25 0 1 0 1793571649 79339520 13636 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/19113/statm): 19370 13636 162 162 0 19208 0
[pid=19113] vsize: 77480
Current children cumulated CPU time (s) 38.99
Current children cumulated vsize (Kb) 79608

[startup+50.0068 s]
Raw data (loadavg): 0.98 0.96 0.72 1/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) T 19108 19108 824 0 -1 0 21613 0 0 0 4754 120 0 0 25 0 1 0 1793571649 84127744 14861 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/19113/statm): 20539 14861 162 162 0 20377 0
[pid=19113] vsize: 82156
Current children cumulated CPU time (s) 48.79
Current children cumulated vsize (Kb) 84284

[startup+60.0076 s]
Raw data (loadavg): 0.98 0.96 0.72 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 26162 0 0 0 5695 145 0 0 25 0 1 0 1793571649 93044736 16905 4294967295 134512640 135167914 3221224448 3221221248 134522468 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 22716 16905 162 162 0 22554 0
[pid=19113] vsize: 90864
Current children cumulated CPU time (s) 58.45
Current children cumulated vsize (Kb) 92992

[startup+70.0083 s]
Raw data (loadavg): 0.98 0.97 0.73 1/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) T 19108 19108 824 0 -1 0 29938 0 0 0 6639 171 0 0 25 0 1 0 1793571649 96845824 17702 4294967295 134512640 135167914 3221224448 3221222572 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/19113/statm): 23644 17702 162 162 0 23482 0
[pid=19113] vsize: 94576
Current children cumulated CPU time (s) 68.15
Current children cumulated vsize (Kb) 96704

[startup+80.01 s]
Raw data (loadavg): 0.99 0.97 0.73 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 34880 0 0 0 7588 194 0 0 25 0 1 0 1793571649 104714240 19507 4294967295 134512640 135167914 3221224448 3221222828 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 25565 19507 162 162 0 25403 0
[pid=19113] vsize: 102260
Current children cumulated CPU time (s) 77.87
Current children cumulated vsize (Kb) 104388

[startup+90.0107 s]
Raw data (loadavg): 0.99 0.97 0.73 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 39808 0 0 0 8535 220 0 0 25 0 1 0 1793571649 110206976 20650 4294967295 134512640 135167914 3221224448 3221221280 134693582 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19113/statm): 26906 20650 162 162 0 26744 0
[pid=19113] vsize: 107624
Current children cumulated CPU time (s) 87.6
Current children cumulated vsize (Kb) 109752

[startup+100.01 s]
Raw data (loadavg): 0.99 0.97 0.73 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 44166 0 0 0 9479 246 0 0 25 0 1 0 1793571649 117911552 22316 4294967295 134512640 135167914 3221224448 3221220192 134611915 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 28787 22316 162 162 0 28625 0
[pid=19113] vsize: 115148
Current children cumulated CPU time (s) 97.3
Current children cumulated vsize (Kb) 117276

[startup+110.012 s]
Raw data (loadavg): 0.99 0.97 0.73 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) T 19108 19108 824 0 -1 0 49190 0 0 0 10420 274 0 0 25 0 1 0 1793571649 123645952 23517 4294967295 134512640 135167914 3221224448 3221223384 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/19113/statm): 30187 23517 162 162 0 30025 0
[pid=19113] vsize: 120748
Current children cumulated CPU time (s) 106.99
Current children cumulated vsize (Kb) 122876

[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 53728 0 0 0 11367 300 0 0 25 0 1 0 1793571649 131289088 25331 4294967295 134512640 135167914 3221224448 3221222800 134693573 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 32053 25331 162 162 0 31891 0
[pid=19113] vsize: 128212
Current children cumulated CPU time (s) 116.72
Current children cumulated vsize (Kb) 130340

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 58536 0 0 0 12311 327 0 0 25 0 1 0 1793571649 138567680 26943 4294967295 134512640 135167914 3221224448 3221219116 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 33830 26943 162 162 0 33668 0
[pid=19113] vsize: 135320
Current children cumulated CPU time (s) 126.43
Current children cumulated vsize (Kb) 137448

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 63228 0 0 0 13254 351 0 0 25 0 1 0 1793571649 143212544 27822 4294967295 134512640 135167914 3221224448 3221222756 134843031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19113/statm): 34964 27822 162 162 0 34802 0
[pid=19113] vsize: 139856
Current children cumulated CPU time (s) 136.1
Current children cumulated vsize (Kb) 141984

[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) T 19108 19108 824 0 -1 0 67378 0 0 0 14198 378 0 0 25 0 1 0 1793571649 148733952 29034 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/19113/statm): 36312 29034 162 162 0 36150 0
[pid=19113] vsize: 145248
Current children cumulated CPU time (s) 145.81
Current children cumulated vsize (Kb) 147376

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 71780 0 0 0 15139 405 0 0 25 0 1 0 1793571649 154402816 30297 4294967295 134512640 135167914 3221224448 3221220704 134610511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19113/statm): 37696 30297 162 162 0 37534 0
[pid=19113] vsize: 150784
Current children cumulated CPU time (s) 155.49
Current children cumulated vsize (Kb) 152912

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 76631 0 0 0 16078 434 0 0 25 0 1 0 1793571649 163864576 32549 4294967295 134512640 135167914 3221224448 3221219512 134693631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19113/statm): 40006 32549 162 162 0 39844 0
[pid=19113] vsize: 160024
Current children cumulated CPU time (s) 165.17
Current children cumulated vsize (Kb) 162152

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.75 1/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) T 19108 19108 824 0 -1 0 81258 0 0 0 17022 459 0 0 25 0 1 0 1793571649 168738816 33645 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/19113/statm): 41196 33645 162 162 0 41034 0
[pid=19113] vsize: 164784
Current children cumulated CPU time (s) 174.86
Current children cumulated vsize (Kb) 166912

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.75 1/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) T 19108 19108 824 0 -1 0 85160 0 0 0 17970 485 0 0 25 0 1 0 1793571649 174759936 34821 4294967295 134512640 135167914 3221224448 3221222572 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/19113/statm): 42666 34821 162 162 0 42504 0
[pid=19113] vsize: 170664
Current children cumulated CPU time (s) 184.6
Current children cumulated vsize (Kb) 172792

[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.75 1/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) T 19108 19108 824 0 -1 0 89420 0 0 0 18915 512 0 0 25 0 1 0 1793571649 180404224 36054 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/19113/statm): 44044 36054 162 162 0 43882 0
[pid=19113] vsize: 176176
Current children cumulated CPU time (s) 194.32
Current children cumulated vsize (Kb) 178304

[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 94047 0 0 0 19861 535 0 0 25 0 1 0 1793571649 189861888 38247 4294967295 134512640 135167914 3221224448 3221222128 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 46353 38247 162 162 0 46191 0
[pid=19113] vsize: 185412
Current children cumulated CPU time (s) 204.01
Current children cumulated vsize (Kb) 187540

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 98011 0 0 0 20810 558 0 0 25 0 1 0 1793571649 193323008 38986 4294967295 134512640 135167914 3221224448 3221223216 134695079 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19113/statm): 47198 38986 162 162 0 47036 0
[pid=19113] vsize: 188792
Current children cumulated CPU time (s) 213.73
Current children cumulated vsize (Kb) 190920

[startup+230.022 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 102856 0 0 0 21750 586 0 0 25 0 1 0 1793571649 203210752 41227 4294967295 134512640 135167914 3221224448 3221222816 134843030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 49612 41227 162 162 0 49450 0
[pid=19113] vsize: 198448
Current children cumulated CPU time (s) 223.41
Current children cumulated vsize (Kb) 200576

[startup+240.023 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 106666 0 0 0 22697 611 0 0 25 0 1 0 1793571649 207474688 42278 4294967295 134512640 135167914 3221224448 3221218896 134581226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 50653 42278 162 162 0 50491 0
[pid=19113] vsize: 202612
Current children cumulated CPU time (s) 233.13
Current children cumulated vsize (Kb) 204740

[startup+250.023 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 111790 0 0 0 23644 637 0 0 25 0 1 0 1793571649 211902464 43400 4294967295 134512640 135167914 3221224448 3221220944 134694444 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19113/statm): 51734 43400 162 162 0 51572 0
[pid=19113] vsize: 206936
Current children cumulated CPU time (s) 242.86
Current children cumulated vsize (Kb) 209064

[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 115252 0 0 0 24592 662 0 0 25 0 1 0 1793571649 217362432 44614 4294967295 134512640 135167914 3221224448 3221222896 134590812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19113/statm): 53067 44614 162 162 0 52905 0
[pid=19113] vsize: 212268
Current children cumulated CPU time (s) 252.59
Current children cumulated vsize (Kb) 214396

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 25532 693 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 262.3
Current children cumulated vsize (Kb) 235084

[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 26532 693 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223272 134691201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 272.3
Current children cumulated vsize (Kb) 235084

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 27532 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 282.31
Current children cumulated vsize (Kb) 235084

[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 28533 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223280 134596373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 292.32
Current children cumulated vsize (Kb) 235084

[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 29533 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223272 134691201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 302.32
Current children cumulated vsize (Kb) 235084

[startup+320.028 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 30533 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223204 134697070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 312.32
Current children cumulated vsize (Kb) 235084

[startup+330.029 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 31533 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 322.32
Current children cumulated vsize (Kb) 235084

[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 32534 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 332.33
Current children cumulated vsize (Kb) 235084

[startup+350.031 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 33534 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691401 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 342.33
Current children cumulated vsize (Kb) 235084

[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 34534 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223288 134596334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 352.33
Current children cumulated vsize (Kb) 235084

[startup+370.032 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 35534 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 362.33
Current children cumulated vsize (Kb) 235084

[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 36534 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134594254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 372.33
Current children cumulated vsize (Kb) 235084

[startup+390.034 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 37535 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 382.34
Current children cumulated vsize (Kb) 235084

[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 38535 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 392.34
Current children cumulated vsize (Kb) 235084

[startup+410.035 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 39535 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691242 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 402.34
Current children cumulated vsize (Kb) 235084

[startup+420.035 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 40535 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 412.34
Current children cumulated vsize (Kb) 235084

[startup+430.036 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 41535 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691366 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 422.34
Current children cumulated vsize (Kb) 235084

[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 42535 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223204 134697054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 432.34
Current children cumulated vsize (Kb) 235084

[startup+450.037 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 43536 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134594165 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 442.35
Current children cumulated vsize (Kb) 235084

[startup+460.038 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 44536 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223280 134596345 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 452.35
Current children cumulated vsize (Kb) 235084

[startup+470.038 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 45536 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 462.35
Current children cumulated vsize (Kb) 235084

[startup+480.039 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 46536 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 472.35
Current children cumulated vsize (Kb) 235084

[startup+490.04 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 47536 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 482.35
Current children cumulated vsize (Kb) 235084

[startup+500.041 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 48537 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 492.36
Current children cumulated vsize (Kb) 235084

[startup+510.041 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 49537 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223204 134697076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 502.36
Current children cumulated vsize (Kb) 235084

[startup+520.042 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 50537 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223204 134697070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 512.36
Current children cumulated vsize (Kb) 235084

[startup+530.044 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 51537 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 522.36
Current children cumulated vsize (Kb) 235084

[startup+540.044 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 52538 694 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223204 134697187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 532.37
Current children cumulated vsize (Kb) 235084

[startup+550.045 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 53538 695 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 542.38
Current children cumulated vsize (Kb) 235084

[startup+560.046 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 54538 695 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223204 134697187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 552.38
Current children cumulated vsize (Kb) 235084

[startup+570.047 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 55538 695 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223192 134693640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 562.38
Current children cumulated vsize (Kb) 235084

[startup+580.047 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 56538 695 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691401 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 572.38
Current children cumulated vsize (Kb) 235084

[startup+590.048 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 57539 695 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 582.39
Current children cumulated vsize (Kb) 235084

[startup+600.049 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 58539 695 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134594169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 592.39
Current children cumulated vsize (Kb) 235084

[startup+610.05 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 59539 695 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 602.39
Current children cumulated vsize (Kb) 235084

[startup+620.05 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 60539 695 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 612.39
Current children cumulated vsize (Kb) 235084

[startup+630.051 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 61540 695 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 622.4
Current children cumulated vsize (Kb) 235084

[startup+640.052 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 62540 695 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223288 134596352 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 632.4
Current children cumulated vsize (Kb) 235084

[startup+650.053 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 63540 695 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134596412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 642.4
Current children cumulated vsize (Kb) 235084

[startup+660.053 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 64540 695 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223208 134697041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 652.4
Current children cumulated vsize (Kb) 235084

[startup+670.054 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 65539 696 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134594169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 662.4
Current children cumulated vsize (Kb) 235084

[startup+680.055 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 66539 697 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223288 134596334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 672.41
Current children cumulated vsize (Kb) 235084

[startup+690.055 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 67539 697 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134596304 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 682.41
Current children cumulated vsize (Kb) 235084

[startup+700.056 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 68539 697 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223204 134697054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 692.41
Current children cumulated vsize (Kb) 235084

[startup+710.057 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 69539 698 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 702.42
Current children cumulated vsize (Kb) 235084

[startup+720.058 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 70539 698 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223280 134596373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 712.42
Current children cumulated vsize (Kb) 235084

[startup+730.059 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 71539 698 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223272 134691201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 722.42
Current children cumulated vsize (Kb) 235084

[startup+740.06 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 72539 698 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 732.42
Current children cumulated vsize (Kb) 235084

[startup+750.061 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 73539 698 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 742.42
Current children cumulated vsize (Kb) 235084

[startup+760.062 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 74540 698 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223288 134596334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 752.43
Current children cumulated vsize (Kb) 235084

[startup+770.063 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 75540 698 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691304 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 762.43
Current children cumulated vsize (Kb) 235084

[startup+780.064 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 76540 698 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691394 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 772.43
Current children cumulated vsize (Kb) 235084

[startup+790.065 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 77540 698 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 782.43
Current children cumulated vsize (Kb) 235084

[startup+800.064 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 78540 698 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223212 134697191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 792.43
Current children cumulated vsize (Kb) 235084

[startup+810.065 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 79540 699 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 802.44
Current children cumulated vsize (Kb) 235084

[startup+820.066 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 80540 699 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 812.44
Current children cumulated vsize (Kb) 235084

[startup+830.067 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 81541 699 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 822.45
Current children cumulated vsize (Kb) 235084

[startup+840.067 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 82541 699 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134594245 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 832.45
Current children cumulated vsize (Kb) 235084

[startup+850.068 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 83541 699 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691242 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 842.45
Current children cumulated vsize (Kb) 235084

[startup+860.069 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 84541 699 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 852.45
Current children cumulated vsize (Kb) 235084

[startup+870.07 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 85541 699 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691278 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 862.45
Current children cumulated vsize (Kb) 235084

[startup+880.071 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 86542 699 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223264 134522227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 872.46
Current children cumulated vsize (Kb) 235084

[startup+890.072 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 87542 699 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 882.46
Current children cumulated vsize (Kb) 235084

[startup+900.073 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 88542 699 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223204 134697070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 892.46
Current children cumulated vsize (Kb) 235084

[startup+910.074 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 89542 699 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691394 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 902.46
Current children cumulated vsize (Kb) 235084

[startup+920.075 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 90543 699 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 912.47
Current children cumulated vsize (Kb) 235084

[startup+930.076 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 91543 699 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223276 134691200 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 922.47
Current children cumulated vsize (Kb) 235084

[startup+940.077 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 92543 699 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 932.47
Current children cumulated vsize (Kb) 235084

[startup+950.077 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 93543 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 942.48
Current children cumulated vsize (Kb) 235084

[startup+960.078 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 94543 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223268 134522188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 952.48
Current children cumulated vsize (Kb) 235084

[startup+970.079 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 95543 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 962.48
Current children cumulated vsize (Kb) 235084

[startup+980.081 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 96544 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691366 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 972.49
Current children cumulated vsize (Kb) 235084

[startup+990.081 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 97544 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134596324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 982.49
Current children cumulated vsize (Kb) 235084

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 98544 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223204 134697187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 992.49
Current children cumulated vsize (Kb) 235084

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 99544 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 1002.49
Current children cumulated vsize (Kb) 235084

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 100545 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223056 134847370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 1012.5
Current children cumulated vsize (Kb) 235084

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 101545 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 1022.5
Current children cumulated vsize (Kb) 235084

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 102545 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 1032.5
Current children cumulated vsize (Kb) 235084

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 103545 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134594169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 1042.5
Current children cumulated vsize (Kb) 235084

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 104546 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 1052.51
Current children cumulated vsize (Kb) 235084

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 105545 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 1062.5
Current children cumulated vsize (Kb) 235084

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 106546 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 1072.51
Current children cumulated vsize (Kb) 235084

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 107546 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134596412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 1082.51
Current children cumulated vsize (Kb) 235084

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 108546 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 1092.51
Current children cumulated vsize (Kb) 235084

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 109546 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 1102.51
Current children cumulated vsize (Kb) 235084

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 110547 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 1112.52
Current children cumulated vsize (Kb) 235084

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 111547 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 1122.52
Current children cumulated vsize (Kb) 235084

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 112547 700 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 1132.52
Current children cumulated vsize (Kb) 235084

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 113547 701 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 1142.53
Current children cumulated vsize (Kb) 235084

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 114547 701 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 1152.53
Current children cumulated vsize (Kb) 235084

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 115548 701 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223296 134594169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 1162.54
Current children cumulated vsize (Kb) 235084

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121391 0 0 0 116548 701 0 0 25 0 1 0 1793571649 238546944 49877 4294967295 134512640 135167914 3221224448 3221223212 134697040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58239 49877 162 162 0 58077 0
[pid=19113] vsize: 232956
Current children cumulated CPU time (s) 1172.54
Current children cumulated vsize (Kb) 235084

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121395 0 0 0 117548 701 0 0 25 0 1 0 1793571649 231776256 48228 4294967295 134512640 135167914 3221224448 3221222576 134695319 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 56586 48228 162 162 0 56424 0
[pid=19113] vsize: 226344
Current children cumulated CPU time (s) 1182.54
Current children cumulated vsize (Kb) 228472

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 121904 0 0 0 118547 702 0 0 25 0 1 0 1793571649 235343872 48737 4294967295 134512640 135167914 3221224448 3221222876 134694320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 57457 48737 162 162 0 57295 0
[pid=19113] vsize: 229828
Current children cumulated CPU time (s) 1192.54
Current children cumulated vsize (Kb) 231956

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 123119 0 0 0 119545 705 0 0 25 0 1 0 1793571649 241213440 49952 4294967295 134512640 135167914 3221224448 3221122576 134516638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58890 49952 162 162 0 58728 0
[pid=19113] vsize: 235560
Current children cumulated CPU time (s) 1202.55
Current children cumulated vsize (Kb) 237688



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 19113
Raw data (/proc/19108/stat): 19108 (minisat+_script) S 19107 19108 824 0 -1 0 314 332 0 0 0 1 2 2 20 0 1 0 1793571639 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19108/statm): 532 234 485 147 0 385 0
[pid=19108] vsize: 2128
Raw data (/proc/19113/stat): 19113 (minisat+_bignum) R 19108 19108 824 0 -1 0 123119 0 0 0 119545 705 0 0 25 0 1 0 1793571649 241213440 49952 4294967295 134512640 135167914 3221224448 3221113856 134843012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19113/statm): 58890 49952 162 162 0 58728 0
[pid=19113] vsize: 235560
Current children cumulated CPU time (s) 1202.55
Current children cumulated vsize (Kb) 237688

Sending SIGTERM to -19108
Sleeping 2 seconds
One traced child (pid=19108) ended because it received signal 15 (SIGTERM)
One traced child (pid=19113) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1210.2
CPU time (s): 1202.6
CPU user time (s): 1195.45
CPU system time (s): 7.14691
CPU usage (%): 99.372
Max. virtual memory (cumulated for all children) (Kb): 237688

Verifier Data

ERROR: no interpretation found !