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-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-gesa2.opb
MD5SUMa1d50263b520d58c9e2807bbf8bc2f07
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1777334285746
Optimality of the best value was proved NO
Number of terms in the objective function 9432
Biggest coefficient in the objective function 409031671808
Number of bits for the biggest coefficient in the objective function 39
Sum of the numbers in the objective function 179181298104960
Number of bits of the sum of numbers in the objective function 48
Biggest number in a constraint 409031671808
Number of bits of the biggest number in a constraint 39
Biggest sum of numbers in a constraint 179181298104960
Number of bits of the biggest sum of numbers48
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.33
Number of variables13368
Total number of constraints2112
Number of constraints which are clauses48
Number of constraints which are cardinality constraints (but not clauses)240
Number of constraints which are nor clauses,nor cardinality constraints1824
Minimum length of a constraint1
Maximum length of a constraint209

Trace number 6131

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        885492 kB
Buffers:         20404 kB
Cached:         100108 kB
SwapCached:        868 kB
Active:          38464 kB
Inactive:        84716 kB
HighTotal:      131008 kB
HighFree:        28476 kB
LowTotal:       903652 kB
LowFree:        857016 kB
SwapTotal:     2097892 kB
SwapFree:      2096540 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           5704 kB
Slab:            20180 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:58:18 (client local time) WITH STATUS 0 IN 1200.06 SECONDS
stats: 3294 7 1200.06 0

Solver Data

c Parsing PB file...
c Converting 1872 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################
c   -- Clauses(.)/Splits(s): ................................................................................................sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss................................................sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[2051]---> BDD-cost:    2
c ---[2046]---> BDD-cost:    2
c ---[2041]---> BDD-cost:    2
c ---[2036]---> BDD-cost:    2
c ---[2031]---> BDD-cost:    2
c ---[2026]---> BDD-cost:    2
c ---[2021]---> BDD-cost:    2
c ---[2016]---> BDD-cost:    2
c ---[2011]---> BDD-cost:    2
c ---[2006]---> BDD-cost:    2
c ---[2001]---> BDD-cost:    2
c ---[1996]---> BDD-cost:    2
c ---[1991]---> BDD-cost:    2
c ---[1986]---> BDD-cost:    2
c ---[1981]---> BDD-cost:    2
c ---[1976]---> BDD-cost:    2
c ---[1971]---> BDD-cost:    2
c ---[1966]---> BDD-cost:    2
c ---[1961]---> BDD-cost:    2
c ---[1956]---> BDD-cost:    2
c ---[1951]---> BDD-cost:    2
c ---[1946]---> BDD-cost:    2
c ---[1941]---> BDD-cost:    2
c ---[1936]---> BDD-cost:    2
c ---[1931]---> BDD-cost:    7
c ---[1930]---> BDD-cost:    7
c ---[1929]---> BDD-cost:    7
c ---[1928]---> BDD-cost:    7
c ---[1927]---> BDD-cost:    7
c ---[1926]---> BDD-cost:    9
c ---[1925]---> BDD-cost:    8
c ---[1924]---> BDD-cost:    8
c ---[1923]---> BDD-cost:    8
c ---[1922]---> BDD-cost:    8
c ---[1921]---> BDD-cost:    8
c ---[1920]---> BDD-cost:    7
c ---[1919]---> BDD-cost:    8
c ---[1918]---> BDD-cost:    7
c ---[1917]---> BDD-cost:    7
c ---[1916]---> BDD-cost:    7
c ---[1915]---> BDD-cost:    7
c ---[1914]---> BDD-cost:    7
c ---[1913]---> BDD-cost:    9
c ---[1912]---> BDD-cost:    8
c ---[1911]---> BDD-cost:    8
c ---[1910]---> BDD-cost:    8
c ---[1909]---> BDD-cost:    8
c ---[1908]---> BDD-cost:    8
c ---[1907]---> BDD-cost:    7
c ---[1906]---> BDD-cost:    8
c ---[1905]---> BDD-cost:    7
c ---[1904]---> BDD-cost:    7
c ---[1903]---> BDD-cost:    7
c ---[1902]---> BDD-cost:    7
c ---[1901]---> BDD-cost:    7
c ---[1900]---> BDD-cost:    9
c ---[1899]---> BDD-cost:    8
c ---[1898]---> BDD-cost:    8
c ---[1897]---> BDD-cost:    8
c ---[1896]---> BDD-cost:    8
c ---[1895]---> BDD-cost:    8
c ---[1894]---> BDD-cost:    7
c ---[1893]---> BDD-cost:    8
c ---[1892]---> BDD-cost:    7
c ---[1891]---> BDD-cost:    7
c ---[1890]---> BDD-cost:    7
c ---[1889]---> BDD-cost:    7
c ---[1888]---> BDD-cost:    7
c ---[1887]---> BDD-cost:    9
c ---[1886]---> BDD-cost:    8
c ---[1885]---> BDD-cost:    8
c ---[1884]---> BDD-cost:    8
c ---[1883]---> BDD-cost:    8
c ---[1882]---> BDD-cost:    8
c ---[1881]---> BDD-cost:    7
c ---[1880]---> BDD-cost:    8
c ---[1879]---> BDD-cost:    7
c ---[1878]---> BDD-cost:    7
c ---[1877]---> BDD-cost:    7
c ---[1876]---> BDD-cost:    7
c ---[1875]---> BDD-cost:    7
c ---[1874]---> BDD-cost:    9
c ---[1873]---> BDD-cost:    8
c ---[1872]---> BDD-cost:    8
c ---[1871]---> BDD-cost:    8
c ---[1870]---> BDD-cost:    8
c ---[1869]---> BDD-cost:    8
c ---[1868]---> BDD-cost:    7
c ---[1867]---> BDD-cost:    8
c ---[1866]---> BDD-cost:    7
c ---[1865]---> BDD-cost:    7
c ---[1864]---> BDD-cost:    7
c ---[1863]---> BDD-cost:    7
c ---[1862]---> BDD-cost:    7
c ---[1861]---> BDD-cost:    9
c ---[1860]---> BDD-cost:    8
c ---[1859]---> BDD-cost:    8
c ---[1858]---> BDD-cost:    8
c ---[1857]---> BDD-cost:    8
c ---[1856]---> BDD-cost:    8
c ---[1855]---> BDD-cost:    7
c ---[1854]---> BDD-cost:    8
c ---[1853]---> BDD-cost:    7
c ---[1852]---> BDD-cost:    7
c ---[1851]---> BDD-cost:    7
c ---[1850]---> BDD-cost:    7
c ---[1849]---> BDD-cost:    7
c ---[1848]---> BDD-cost:    9
c ---[1847]---> BDD-cost:    8
c ---[1846]---> BDD-cost:    8
c ---[1845]---> BDD-cost:    8
c ---[1844]---> BDD-cost:    8
c ---[1843]---> BDD-cost:    8
c ---[1842]---> BDD-cost:    7
c ---[1841]---> BDD-cost:    8
c ---[1840]---> BDD-cost:    7
c ---[1839]---> BDD-cost:    7
c ---[1838]---> BDD-cost:    7
c ---[1837]---> BDD-cost:    7
c ---[1836]---> BDD-cost:    7
c ---[1835]---> BDD-cost:    9
c ---[1834]---> BDD-cost:    8
c ---[1833]---> BDD-cost:    8
c ---[1832]---> BDD-cost:    8
c ---[1831]---> BDD-cost:    8
c ---[1830]---> BDD-cost:    8
c ---[1829]---> BDD-cost:    7
c ---[1828]---> BDD-cost:    8
c ---[1827]---> BDD-cost:    7
c ---[1826]---> BDD-cost:    7
c ---[1825]---> BDD-cost:    7
c ---[1824]---> BDD-cost:    7
c ---[1823]---> BDD-cost:    7
c ---[1822]---> BDD-cost:    9
c ---[1821]---> BDD-cost:    8
c ---[1820]---> BDD-cost:    8
c ---[1819]---> BDD-cost:    8
c ---[1818]---> BDD-cost:    8
c ---[1817]---> BDD-cost:    8
c ---[1816]---> BDD-cost:    7
c ---[1815]---> BDD-cost:    8
c ---[1814]---> BDD-cost:    7
c ---[1813]---> BDD-cost:    7
c ---[1812]---> BDD-cost:    7
c ---[1811]---> BDD-cost:    7
c ---[1810]---> BDD-cost:    7
c ---[1809]---> BDD-cost:    9
c ---[1808]---> BDD-cost:    8
c ---[1807]---> BDD-cost:    8
c ---[1806]---> BDD-cost:    8
c ---[1805]---> BDD-cost:    8
c ---[1804]---> BDD-cost:    8
c ---[1803]---> BDD-cost:    7
c ---[1802]---> BDD-cost:    8
c ---[1801]---> BDD-cost:    7
c ---[1800]---> BDD-cost:    7
c ---[1799]---> BDD-cost:    7
c ---[1798]---> BDD-cost:    7
c ---[1797]---> BDD-cost:    7
c ---[1796]---> BDD-cost:    9
c ---[1795]---> BDD-cost:    8
c ---[1794]---> BDD-cost:    8
c ---[1793]---> BDD-cost:    8
c ---[1792]---> BDD-cost:    8
c ---[1791]---> BDD-cost:    8
c ---[1790]---> BDD-cost:    7
c ---[1789]---> BDD-cost:    8
c ---[1788]---> BDD-cost:    7
c ---[1787]---> BDD-cost:    7
c ---[1786]---> BDD-cost:    7
c ---[1785]---> BDD-cost:    7
c ---[1784]---> BDD-cost:    7
c ---[1783]---> BDD-cost:    9
c ---[1782]---> BDD-cost:    8
c ---[1781]---> BDD-cost:    8
c ---[1780]---> BDD-cost:    8
c ---[1779]---> BDD-cost:    8
c ---[1778]---> BDD-cost:    8
c ---[1777]---> BDD-cost:    7
c ---[1776]---> BDD-cost:    8
c ---[1775]---> BDD-cost:    7
c ---[1774]---> BDD-cost:    7
c ---[1773]---> BDD-cost:    7
c ---[1772]---> BDD-cost:    7
c ---[1771]---> BDD-cost:    7
c ---[1770]---> BDD-cost:    9
c ---[1769]---> BDD-cost:    8
c ---[1768]---> BDD-cost:    8
c ---[1767]---> BDD-cost:    8
c ---[1766]---> BDD-cost:    8
c ---[1765]---> BDD-cost:    8
c ---[1764]---> BDD-cost:    7
c ---[1763]---> BDD-cost:    8
c ---[1762]---> BDD-cost:    7
c ---[1761]---> BDD-cost:    7
c ---[1760]---> BDD-cost:    7
c ---[1759]---> BDD-cost:    7
c ---[1758]---> BDD-cost:    7
c ---[1757]---> BDD-cost:    9
c ---[1756]---> BDD-cost:    8
c ---[1755]---> BDD-cost:    8
c ---[1754]---> BDD-cost:    8
c ---[1753]---> BDD-cost:    8
c ---[1752]---> BDD-cost:    8
c ---[1751]---> BDD-cost:    7
c ---[1750]---> BDD-cost:    8
c ---[1749]---> BDD-cost:    7
c ---[1748]---> BDD-cost:    7
c ---[1747]---> BDD-cost:    7
c ---[1746]---> BDD-cost:    7
c ---[1745]---> BDD-cost:    7
c ---[1744]---> BDD-cost:    9
c ---[1743]---> BDD-cost:    8
c ---[1742]---> BDD-cost:    8
c ---[1741]---> BDD-cost:    8
c ---[1740]---> BDD-cost:    8
c ---[1739]---> BDD-cost:    8
c ---[1738]---> BDD-cost:    7
c ---[1737]---> BDD-cost:    8
c ---[1736]---> BDD-cost:    7
c ---[1735]---> BDD-cost:    7
c ---[1734]---> BDD-cost:    7
c ---[1733]---> BDD-cost:    7
c ---[1732]---> BDD-cost:    7
c ---[1731]---> BDD-cost:    9
c ---[1730]---> BDD-cost:    8
c ---[1729]---> BDD-cost:    8
c ---[1728]---> BDD-cost:    8
c ---[1727]---> BDD-cost:    8
c ---[1726]---> BDD-cost:    8
c ---[1725]---> BDD-cost:    7
c ---[1724]---> BDD-cost:    8
c ---[1723]---> BDD-cost:    7
c ---[1722]---> BDD-cost:    7
c ---[1721]---> BDD-cost:    7
c ---[1720]---> BDD-cost:    7
c ---[1719]---> BDD-cost:    7
c ---[1718]---> BDD-cost:    9
c ---[1717]---> BDD-cost:    8
c ---[1716]---> BDD-cost:    8
c ---[1715]---> BDD-cost:    8
c ---[1714]---> BDD-cost:    8
c ---[1713]---> BDD-cost:    8
c ---[1712]---> BDD-cost:    7
c ---[1711]---> BDD-cost:    8
c ---[1710]---> BDD-cost:    7
c ---[1709]---> BDD-cost:    7
c ---[1708]---> BDD-cost:    7
c ---[1707]---> BDD-cost:    7
c ---[1706]---> BDD-cost:    7
c ---[1705]---> BDD-cost:    9
c ---[1704]---> BDD-cost:    8
c ---[1703]---> BDD-cost:    8
c ---[1702]---> BDD-cost:    8
c ---[1701]---> BDD-cost:    8
c ---[1700]---> BDD-cost:    8
c ---[1699]---> BDD-cost:    7
c ---[1698]---> BDD-cost:    8
c ---[1697]---> BDD-cost:    7
c ---[1696]---> BDD-cost:    7
c ---[1695]---> BDD-cost:    7
c ---[1694]---> BDD-cost:    7
c ---[1693]---> BDD-cost:    7
c ---[1692]---> BDD-cost:    9
c ---[1691]---> BDD-cost:    8
c ---[1690]---> BDD-cost:    8
c ---[1689]---> BDD-cost:    8
c ---[1688]---> BDD-cost:    8
c ---[1687]---> BDD-cost:    8
c ---[1686]---> BDD-cost:    7
c ---[1685]---> BDD-cost:    8
c ---[1684]---> BDD-cost:    7
c ---[1683]---> BDD-cost:    7
c ---[1682]---> BDD-cost:    7
c ---[1681]---> BDD-cost:    7
c ---[1680]---> BDD-cost:    7
c ---[1679]---> BDD-cost:    9
c ---[1678]---> BDD-cost:    8
c ---[1677]---> BDD-cost:    8
c ---[1676]---> BDD-cost:    8
c ---[1675]---> BDD-cost:    8
c ---[1674]---> BDD-cost:    8
c ---[1673]---> BDD-cost:    7
c ---[1672]---> BDD-cost:    8
c ---[1671]---> BDD-cost:    7
c ---[1670]---> BDD-cost:    7
c ---[1669]---> BDD-cost:    7
c ---[1668]---> BDD-cost:    7
c ---[1667]---> BDD-cost:    7
c ---[1666]---> BDD-cost:    9
c ---[1665]---> BDD-cost:    8
c ---[1664]---> BDD-cost:    8
c ---[1663]---> BDD-cost:    8
c ---[1662]---> BDD-cost:    8
c ---[1661]---> BDD-cost:    8
c ---[1660]---> BDD-cost:    7
c ---[1659]---> BDD-cost:    8
c ---[1658]---> BDD-cost:    7
c ---[1657]---> BDD-cost:    7
c ---[1656]---> BDD-cost:    7
c ---[1655]---> BDD-cost:    7
c ---[1654]---> BDD-cost:    7
c ---[1653]---> BDD-cost:    9
c ---[1652]---> BDD-cost:    8
c ---[1651]---> BDD-cost:    8
c ---[1650]---> BDD-cost:    8
c ---[1649]---> BDD-cost:    8
c ---[1648]---> BDD-cost:    8
c ---[1647]---> BDD-cost:    7
c ---[1646]---> BDD-cost:    8
c ---[1645]---> BDD-cost:    7
c ---[1644]---> BDD-cost:    7
c ---[1643]---> BDD-cost:    7
c ---[1642]---> BDD-cost:    7
c ---[1641]---> BDD-cost:    7
c ---[1640]---> BDD-cost:    9
c ---[1639]---> BDD-cost:    8
c ---[1638]---> BDD-cost:    8
c ---[1637]---> BDD-cost:    8
c ---[1636]---> BDD-cost:    8
c ---[1635]---> BDD-cost:    8
c ---[1634]---> BDD-cost:    7
c ---[1633]---> BDD-cost:    8
c ---[1632]---> BDD-cost:    7
c ---[1631]---> BDD-cost:    7
c ---[1630]---> BDD-cost:    7
c ---[1629]---> BDD-cost:    7
c ---[1628]---> BDD-cost:    7
c ---[1627]---> BDD-cost:    9
c ---[1626]---> BDD-cost:    8
c ---[1625]---> BDD-cost:    8
c ---[1624]---> BDD-cost:    8
c ---[1623]---> BDD-cost:    8
c ---[1622]---> BDD-cost:    8
c ---[1621]---> BDD-cost:    7
c ---[1620]---> BDD-cost:    8
c ---[1619]---> Adder-cost: 1880   maxlim: 10472559999   bits: 35/34
c ---[1618]---> Adder-cost: 1880   maxlim: 14035823999   bits: 35/34
c ---[1616]---> BDD-cost:   45
c ---[1615]---> BDD-cost:   45
c ---[1614]---> BDD-cost:   45
c ---[1613]---> BDD-cost:   45
c ---[1612]---> BDD-cost:   45
c ---[1611]---> BDD-cost:   45
c ---[1610]---> BDD-cost:   45
c ---[1609]---> BDD-cost:   45
c ---[1608]---> BDD-cost:   45
c ---[1607]---> BDD-cost:   45
c ---[1605]---> BDD-cost:   45
c ---[1604]---> BDD-cost:   45
c ---[1603]---> BDD-cost:   45
c ---[1602]---> BDD-cost:   45
c ---[1601]---> BDD-cost:   45
c ---[1600]---> BDD-cost:   45
c ---[1599]---> BDD-cost:   45
c ---[1598]---> BDD-cost:   45
c ---[1597]---> BDD-cost:   45
c ---[1596]---> BDD-cost:   45
c ---[1594]---> BDD-cost:   45
c ---[1593]---> BDD-cost:   45
c ---[1592]---> BDD-cost:   45
c ---[1591]---> BDD-cost:   45
c ---[1590]---> BDD-cost:   45
c ---[1589]---> BDD-cost:   45
c ---[1588]---> BDD-cost:   45
c ---[1587]---> BDD-cost:   45
c ---[1586]---> BDD-cost:   45
c ---[1585]---> BDD-cost:   45
c ---[1584]---> BDD-cost:    4
c ---[1583]---> BDD-cost:   45
c ---[1582]---> BDD-cost:   45
c ---[1581]---> BDD-cost:   45
c ---[1573]---> BDD-cost:    6
c ---[1562]---> BDD-cost:    7
c ---[1555]---> BDD-cost:    9
c ---[1554]---> BDD-cost:    9
c ---[1553]---> BDD-cost:    9
c ---[1552]---> BDD-cost:    9
c ---[1551]---> BDD-cost:    7
c ---[1550]---> BDD-cost:    9
c ---[1549]---> BDD-cost:    9
c ---[1548]---> BDD-cost:    9
c ---[1547]---> BDD-cost:    9
c ---[1546]---> BDD-cost:    9
c ---[1545]---> BDD-cost:    9
c ---[1544]---> BDD-cost:    9
c ---[1543]---> BDD-cost:    9
c ---[1542]---> BDD-cost:    9
c ---[1541]---> BDD-cost:    9
c ---[1540]---> BDD-cost:    7
c ---[1539]---> BDD-cost:    9
c ---[1538]---> BDD-cost:    9
c ---[1537]---> BDD-cost:    9
c ---[1536]---> BDD-cost:    9
c ---[1535]---> BDD-cost:    9
c ---[1534]---> BDD-cost:    9
c ---[1533]---> BDD-cost:    9
c ---[1532]---> BDD-cost:    9
c ---[1531]---> BDD-cost:    9
c ---[1530]---> BDD-cost:    9
c ---[1529]---> BDD-cost:    7
c ---[1528]---> BDD-cost:    9
c ---[1527]---> BDD-cost:    9
c ---[1526]---> BDD-cost:    9
c ---[1525]---> BDD-cost:    9
c ---[1524]---> BDD-cost:    9
c ---[1523]---> BDD-cost:    9
c ---[1522]---> BDD-cost:    9
c ---[1521]---> BDD-cost:    9
c ---[1520]---> BDD-cost:    9
c ---[1519]---> BDD-cost:    9
c ---[1518]---> BDD-cost:    6
c ---[1517]---> BDD-cost:    9
c ---[1516]---> BDD-cost:    9
c ---[1515]---> BDD-cost:    9
c ---[1514]---> BDD-cost:    9
c ---[1513]---> BDD-cost:    9
c ---[1512]---> BDD-cost:    9
c ---[1511]---> BDD-cost:    9
c ---[1510]---> BDD-cost:    9
c ---[1509]---> BDD-cost:    9
c ---[1508]---> BDD-cost:    9
c ---[1507]---> Adder-cost: 1880   maxlim: 14127471999   bits: 35/34
c ---[1506]---> BDD-cost:    5
c ---[1505]---> BDD-cost:    9
c ---[1504]---> BDD-cost:    9
c ---[1495]---> BDD-cost:    6
c ---[1484]---> BDD-cost:    7
c ---[1478]---> BDD-cost:    9
c ---[1477]---> BDD-cost:    9
c ---[1476]---> BDD-cost:    9
c ---[1475]---> BDD-cost:    9
c ---[1474]---> BDD-cost:    9
c ---[1473]---> BDD-cost:    7
c ---[1472]---> BDD-cost:    9
c ---[1471]---> BDD-cost:    9
c ---[1470]---> BDD-cost:    9
c ---[1469]---> BDD-cost:    9
c ---[1468]---> BDD-cost:    9
c ---[1467]---> BDD-cost:    9
c ---[1466]---> BDD-cost:    9
c ---[1465]---> BDD-cost:    9
c ---[1464]---> BDD-cost:    9
c ---[1463]---> BDD-cost:    9
c ---[1462]---> BDD-cost:    7
c ---[1461]---> BDD-cost:    9
c ---[1460]---> BDD-cost:    9
c ---[1459]---> BDD-cost:    9
c ---[1458]---> BDD-cost:    9
c ---[1457]---> BDD-cost:    9
c ---[1456]---> BDD-cost:    9
c ---[1455]---> BDD-cost:    9
c ---[1454]---> BDD-cost:    9
c ---[1451]---> BDD-cost:    7
c ---[1440]---> BDD-cost:    7
c ---[1429]---> BDD-cost:    8
c ---[1418]---> BDD-cost:    7
c ---[1407]---> BDD-cost:    5
c ---[1402]---> BDD-cost:    9
c ---[1401]---> BDD-cost:    9
c ---[1400]---> BDD-cost:    9
c ---[1399]---> BDD-cost:    9
c ---[1398]---> BDD-cost:    9
c ---[1397]---> BDD-cost:    9
c ---[1396]---> Adder-cost: 1880   maxlim: 14036335999   bits: 35/34
c ---[1395]---> BDD-cost:    4
c ---[1394]---> BDD-cost:    9
c ---[1393]---> BDD-cost:    9
c ---[1392]---> BDD-cost:    9
c ---[1391]---> BDD-cost:    9
c ---[1390]---> BDD-cost:    9
c ---[1389]---> BDD-cost:    9
c ---[1388]---> BDD-cost:    9
c ---[1387]---> BDD-cost:    9
c ---[1386]---> BDD-cost:    9
c ---[1385]---> BDD-cost:    9
c ---[1384]---> BDD-cost:   21
c ---[1383]---> BDD-cost:    9
c ---[1382]---> BDD-cost:    9
c ---[1381]---> BDD-cost:    9
c ---[1380]---> BDD-cost:    9
c ---[1379]---> BDD-cost:    9
c ---[1378]---> BDD-cost:    9
c ---[1377]---> BDD-cost:    9
c ---[1325]---> BDD-cost:   18
c ---[1324]---> BDD-cost:   18
c ---[1323]---> BDD-cost:   18
c ---[1322]---> BDD-cost:   18
c ---[1321]---> BDD-cost:   18
c ---[1320]---> BDD-cost:   18
c ---[1319]---> BDD-cost:   18
c ---[1317]---> BDD-cost:   18
c ---[1316]---> BDD-cost:   18
c ---[1315]---> BDD-cost:   18
c ---[1314]---> BDD-cost:   18
c ---[1313]---> BDD-cost:   18
c ---[1312]---> BDD-cost:   18
c ---[1311]---> BDD-cost:   18
c ---[1310]---> BDD-cost:   18
c ---[1309]---> BDD

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/17047/stat): 17047 (minisat+_script) R 17046 17047 16528 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855368067 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/17047/statm): 174 3 169 147 0 27 0
[pid=17047] 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=17048
New process pid=17049
New process pid=17050
execve syscall for /bin/sed executable
One traced child (pid=17049) 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=17050) exited with status: 0
One traced child (pid=17048) exited with status: 0
New process pid=17051
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-gesa2.opb

[startup+10.0039 s]
Raw data (loadavg): 0.93 0.96 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 1869 0 0 0 978 9 0 0 25 0 1 0 1855368072 6672384 1487 4294967295 134512640 135094434 3221224432 3221219344 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1629 1487 145 145 0 1484 0
[pid=17051] vsize: 6516
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 8640

[startup+20.0066 s]
Raw data (loadavg): 0.94 0.96 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 1869 0 0 0 1978 9 0 0 25 0 1 0 1855368072 6672384 1487 4294967295 134512640 135094434 3221224432 3221219344 134677290 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1629 1487 145 145 0 1484 0
[pid=17051] vsize: 6516
Current children cumulated CPU time (s) 19.87
Current children cumulated vsize (Kb) 8640

[startup+30.0082 s]
Raw data (loadavg): 0.95 0.96 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 1869 0 0 0 2978 9 0 0 25 0 1 0 1855368072 6672384 1487 4294967295 134512640 135094434 3221224432 3221219064 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1629 1487 145 145 0 1484 0
[pid=17051] vsize: 6516
Current children cumulated CPU time (s) 29.87
Current children cumulated vsize (Kb) 8640

[startup+40.0089 s]
Raw data (loadavg): 0.96 0.96 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 1869 0 0 0 3979 9 0 0 25 0 1 0 1855368072 6672384 1487 4294967295 134512640 135094434 3221224432 3221219520 134600204 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1629 1487 145 145 0 1484 0
[pid=17051] vsize: 6516
Current children cumulated CPU time (s) 39.88
Current children cumulated vsize (Kb) 8640

[startup+50.0096 s]
Raw data (loadavg): 0.96 0.96 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 1869 0 0 0 4979 9 0 0 25 0 1 0 1855368072 6672384 1487 4294967295 134512640 135094434 3221224432 3221220128 134676328 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1629 1487 145 145 0 1484 0
[pid=17051] vsize: 6516
Current children cumulated CPU time (s) 49.88
Current children cumulated vsize (Kb) 8640

[startup+60.0103 s]
Raw data (loadavg): 0.97 0.96 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 1869 0 0 0 5979 9 0 0 25 0 1 0 1855368072 6672384 1487 4294967295 134512640 135094434 3221224432 3221220224 134600904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1629 1487 145 145 0 1484 0
[pid=17051] vsize: 6516
Current children cumulated CPU time (s) 59.88
Current children cumulated vsize (Kb) 8640

[startup+70.011 s]
Raw data (loadavg): 0.97 0.96 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 1869 0 0 0 6979 9 0 0 25 0 1 0 1855368072 6672384 1487 4294967295 134512640 135094434 3221224432 3221219872 134676601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1629 1487 145 145 0 1484 0
[pid=17051] vsize: 6516
Current children cumulated CPU time (s) 69.88
Current children cumulated vsize (Kb) 8640

[startup+80.0117 s]
Raw data (loadavg): 0.98 0.96 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 1869 0 0 0 7979 9 0 0 25 0 1 0 1855368072 6672384 1487 4294967295 134512640 135094434 3221224432 3221221072 134677147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1629 1487 145 145 0 1484 0
[pid=17051] vsize: 6516
Current children cumulated CPU time (s) 79.88
Current children cumulated vsize (Kb) 8640

[startup+90.0124 s]
Raw data (loadavg): 0.98 0.96 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 1869 0 0 0 8980 10 0 0 25 0 1 0 1855368072 6672384 1487 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1629 1487 145 145 0 1484 0
[pid=17051] vsize: 6516
Current children cumulated CPU time (s) 89.9
Current children cumulated vsize (Kb) 8640

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 1869 0 0 0 9979 10 0 0 25 0 1 0 1855368072 6672384 1487 4294967295 134512640 135094434 3221224432 3221220224 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1629 1487 145 145 0 1484 0
[pid=17051] vsize: 6516
Current children cumulated CPU time (s) 99.89
Current children cumulated vsize (Kb) 8640

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 1869 0 0 0 10980 10 0 0 25 0 1 0 1855368072 6672384 1487 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1629 1487 145 145 0 1484 0
[pid=17051] vsize: 6516
Current children cumulated CPU time (s) 109.9
Current children cumulated vsize (Kb) 8640

[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 1869 0 0 0 11980 10 0 0 25 0 1 0 1855368072 6672384 1487 4294967295 134512640 135094434 3221224432 3221221984 134600283 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1629 1487 145 145 0 1484 0
[pid=17051] vsize: 6516
Current children cumulated CPU time (s) 119.9
Current children cumulated vsize (Kb) 8640

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 1869 0 0 0 12980 10 0 0 25 0 1 0 1855368072 6672384 1487 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1629 1487 145 145 0 1484 0
[pid=17051] vsize: 6516
Current children cumulated CPU time (s) 129.9
Current children cumulated vsize (Kb) 8640

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 1869 0 0 0 13980 10 0 0 25 0 1 0 1855368072 6672384 1487 4294967295 134512640 135094434 3221224432 3221220848 134677065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1629 1487 145 145 0 1484 0
[pid=17051] vsize: 6516
Current children cumulated CPU time (s) 139.9
Current children cumulated vsize (Kb) 8640

[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 1869 0 0 0 14981 10 0 0 25 0 1 0 1855368072 6672384 1487 4294967295 134512640 135094434 3221224432 3221221280 134677351 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1629 1487 145 145 0 1484 0
[pid=17051] vsize: 6516
Current children cumulated CPU time (s) 149.91
Current children cumulated vsize (Kb) 8640

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2361 0 0 0 15978 12 0 0 25 0 1 0 1855368072 7319552 1635 4294967295 134512640 135094434 3221224432 3221219956 134677077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1787 1635 145 145 0 1642 0
[pid=17051] vsize: 7148
Current children cumulated CPU time (s) 159.9
Current children cumulated vsize (Kb) 9272

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2361 0 0 0 16978 12 0 0 25 0 1 0 1855368072 7319552 1635 4294967295 134512640 135094434 3221224432 3221220928 134600175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1787 1635 145 145 0 1642 0
[pid=17051] vsize: 7148
Current children cumulated CPU time (s) 169.9
Current children cumulated vsize (Kb) 9272

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2361 0 0 0 17979 12 0 0 25 0 1 0 1855368072 7319552 1635 4294967295 134512640 135094434 3221224432 3221219512 134600772 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1787 1635 145 145 0 1642 0
[pid=17051] vsize: 7148
Current children cumulated CPU time (s) 179.91
Current children cumulated vsize (Kb) 9272

[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2361 0 0 0 18979 12 0 0 25 0 1 0 1855368072 7319552 1635 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1787 1635 145 145 0 1642 0
[pid=17051] vsize: 7148
Current children cumulated CPU time (s) 189.91
Current children cumulated vsize (Kb) 9272

[startup+200.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2361 0 0 0 19979 12 0 0 25 0 1 0 1855368072 7319552 1635 4294967295 134512640 135094434 3221224432 3221221084 134676988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1787 1635 145 145 0 1642 0
[pid=17051] vsize: 7148
Current children cumulated CPU time (s) 199.91
Current children cumulated vsize (Kb) 9272

[startup+210.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2361 0 0 0 20979 12 0 0 25 0 1 0 1855368072 7319552 1635 4294967295 134512640 135094434 3221224432 3221220496 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1787 1635 145 145 0 1642 0
[pid=17051] vsize: 7148
Current children cumulated CPU time (s) 209.91
Current children cumulated vsize (Kb) 9272

[startup+220.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2361 0 0 0 21979 12 0 0 25 0 1 0 1855368072 7319552 1635 4294967295 134512640 135094434 3221224432 3221220128 134676328 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1787 1635 145 145 0 1642 0
[pid=17051] vsize: 7148
Current children cumulated CPU time (s) 219.91
Current children cumulated vsize (Kb) 9272

[startup+230.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2361 0 0 0 22979 12 0 0 25 0 1 0 1855368072 7319552 1635 4294967295 134512640 135094434 3221224432 3221219696 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1787 1635 145 145 0 1642 0
[pid=17051] vsize: 7148
Current children cumulated CPU time (s) 229.91
Current children cumulated vsize (Kb) 9272

[startup+240.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2361 0 0 0 23980 13 0 0 25 0 1 0 1855368072 7319552 1635 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1787 1635 145 145 0 1642 0
[pid=17051] vsize: 7148
Current children cumulated CPU time (s) 239.93
Current children cumulated vsize (Kb) 9272

[startup+250.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2361 0 0 0 24980 13 0 0 25 0 1 0 1855368072 7319552 1635 4294967295 134512640 135094434 3221224432 3221220144 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1787 1635 145 145 0 1642 0
[pid=17051] vsize: 7148
Current children cumulated CPU time (s) 249.93
Current children cumulated vsize (Kb) 9272

[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2361 0 0 0 25980 13 0 0 25 0 1 0 1855368072 7319552 1635 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1787 1635 145 145 0 1642 0
[pid=17051] vsize: 7148
Current children cumulated CPU time (s) 259.93
Current children cumulated vsize (Kb) 9272

[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2361 0 0 0 26980 13 0 0 25 0 1 0 1855368072 7319552 1635 4294967295 134512640 135094434 3221224432 3221220224 134677340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1787 1635 145 145 0 1642 0
[pid=17051] vsize: 7148
Current children cumulated CPU time (s) 269.93
Current children cumulated vsize (Kb) 9272

[startup+280.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2361 0 0 0 27980 13 0 0 25 0 1 0 1855368072 7319552 1635 4294967295 134512640 135094434 3221224432 3221219584 134677091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1787 1635 145 145 0 1642 0
[pid=17051] vsize: 7148
Current children cumulated CPU time (s) 279.93
Current children cumulated vsize (Kb) 9272

[startup+290.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2361 0 0 0 28980 13 0 0 25 0 1 0 1855368072 7319552 1635 4294967295 134512640 135094434 3221224432 3221220848 134676259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1787 1635 145 145 0 1642 0
[pid=17051] vsize: 7148
Current children cumulated CPU time (s) 289.93
Current children cumulated vsize (Kb) 9272

[startup+300.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2361 0 0 0 29981 13 0 0 25 0 1 0 1855368072 7319552 1635 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1787 1635 145 145 0 1642 0
[pid=17051] vsize: 7148
Current children cumulated CPU time (s) 299.94
Current children cumulated vsize (Kb) 9272

[startup+310.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2685 0 0 0 30979 14 0 0 25 0 1 0 1855368072 7340032 1647 4294967295 134512640 135094434 3221224432 3221218992 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17051/statm): 1792 1647 145 145 0 1647 0
[pid=17051] vsize: 7168
Current children cumulated CPU time (s) 309.93
Current children cumulated vsize (Kb) 9292

[startup+320.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2685 0 0 0 31979 14 0 0 25 0 1 0 1855368072 7340032 1647 4294967295 134512640 135094434 3221224432 3221219568 134677375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/17051/statm): 1792 1647 145 145 0 1647 0
[pid=17051] vsize: 7168
Current children cumulated CPU time (s) 319.93
Current children cumulated vsize (Kb) 9292

[startup+330.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2685 0 0 0 32979 14 0 0 25 0 1 0 1855368072 7340032 1647 4294967295 134512640 135094434 3221224432 3221219752 134676609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1792 1647 145 145 0 1647 0
[pid=17051] vsize: 7168
Current children cumulated CPU time (s) 329.93
Current children cumulated vsize (Kb) 9292

[startup+340.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2685 0 0 0 33979 14 0 0 25 0 1 0 1855368072 7340032 1647 4294967295 134512640 135094434 3221224432 3221220472 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1792 1647 145 145 0 1647 0
[pid=17051] vsize: 7168
Current children cumulated CPU time (s) 339.93
Current children cumulated vsize (Kb) 9292

[startup+350.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2685 0 0 0 34979 14 0 0 25 0 1 0 1855368072 7340032 1647 4294967295 134512640 135094434 3221224432 3221219344 134600267 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1792 1647 145 145 0 1647 0
[pid=17051] vsize: 7168
Current children cumulated CPU time (s) 349.93
Current children cumulated vsize (Kb) 9292

[startup+360.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2685 0 0 0 35979 14 0 0 25 0 1 0 1855368072 7340032 1647 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1792 1647 145 145 0 1647 0
[pid=17051] vsize: 7168
Current children cumulated CPU time (s) 359.93
Current children cumulated vsize (Kb) 9292

[startup+370.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2685 0 0 0 36979 14 0 0 25 0 1 0 1855368072 7340032 1647 4294967295 134512640 135094434 3221224432 3221220128 134676328 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1792 1647 145 145 0 1647 0
[pid=17051] vsize: 7168
Current children cumulated CPU time (s) 369.93
Current children cumulated vsize (Kb) 9292

[startup+380.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2685 0 0 0 37980 14 0 0 25 0 1 0 1855368072 7340032 1647 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1792 1647 145 145 0 1647 0
[pid=17051] vsize: 7168
Current children cumulated CPU time (s) 379.94
Current children cumulated vsize (Kb) 9292

[startup+390.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2685 0 0 0 38980 14 0 0 25 0 1 0 1855368072 7340032 1647 4294967295 134512640 135094434 3221224432 3221220752 134677287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1792 1647 145 145 0 1647 0
[pid=17051] vsize: 7168
Current children cumulated CPU time (s) 389.94
Current children cumulated vsize (Kb) 9292

[startup+400.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2685 0 0 0 39980 14 0 0 25 0 1 0 1855368072 7340032 1647 4294967295 134512640 135094434 3221224432 3221219168 134677248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1792 1647 145 145 0 1647 0
[pid=17051] vsize: 7168
Current children cumulated CPU time (s) 399.94
Current children cumulated vsize (Kb) 9292

[startup+410.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2685 0 0 0 40980 14 0 0 25 0 1 0 1855368072 7340032 1647 4294967295 134512640 135094434 3221224432 3221220552 134677149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1792 1647 145 145 0 1647 0
[pid=17051] vsize: 7168
Current children cumulated CPU time (s) 409.94
Current children cumulated vsize (Kb) 9292

[startup+420.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2685 0 0 0 41981 14 0 0 25 0 1 0 1855368072 7340032 1647 4294967295 134512640 135094434 3221224432 3221220928 134677313 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1792 1647 145 145 0 1647 0
[pid=17051] vsize: 7168
Current children cumulated CPU time (s) 419.95
Current children cumulated vsize (Kb) 9292

[startup+430.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2685 0 0 0 42981 14 0 0 25 0 1 0 1855368072 7340032 1647 4294967295 134512640 135094434 3221224432 3221220732 134676988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1792 1647 145 145 0 1647 0
[pid=17051] vsize: 7168
Current children cumulated CPU time (s) 429.95
Current children cumulated vsize (Kb) 9292

[startup+440.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2685 0 0 0 43981 14 0 0 25 0 1 0 1855368072 7340032 1647 4294967295 134512640 135094434 3221224432 3221221280 134676480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1792 1647 145 145 0 1647 0
[pid=17051] vsize: 7168
Current children cumulated CPU time (s) 439.95
Current children cumulated vsize (Kb) 9292

[startup+450.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 2685 0 0 0 44981 14 0 0 25 0 1 0 1855368072 7340032 1647 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1792 1647 145 145 0 1647 0
[pid=17051] vsize: 7168
Current children cumulated CPU time (s) 449.95
Current children cumulated vsize (Kb) 9292

[startup+460.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 3425 0 0 0 45978 17 0 0 25 0 1 0 1855368072 7294976 1649 4294967295 134512640 135094434 3221224432 3221219056 134676336 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1781 1649 145 145 0 1636 0
[pid=17051] vsize: 7124
Current children cumulated CPU time (s) 459.95
Current children cumulated vsize (Kb) 9248

[startup+470.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 3425 0 0 0 46978 17 0 0 25 0 1 0 1855368072 7294976 1649 4294967295 134512640 135094434 3221224432 3221219520 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1781 1649 145 145 0 1636 0
[pid=17051] vsize: 7124
Current children cumulated CPU time (s) 469.95
Current children cumulated vsize (Kb) 9248

[startup+480.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 3425 0 0 0 47978 17 0 0 25 0 1 0 1855368072 7294976 1649 4294967295 134512640 135094434 3221224432 3221221264 134600241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1781 1649 145 145 0 1636 0
[pid=17051] vsize: 7124
Current children cumulated CPU time (s) 479.95
Current children cumulated vsize (Kb) 9248

[startup+490.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 3425 0 0 0 48978 17 0 0 25 0 1 0 1855368072 7294976 1649 4294967295 134512640 135094434 3221224432 3221218992 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1781 1649 145 145 0 1636 0
[pid=17051] vsize: 7124
Current children cumulated CPU time (s) 489.95
Current children cumulated vsize (Kb) 9248

[startup+500.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 3425 0 0 0 49979 17 0 0 25 0 1 0 1855368072 7294976 1649 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1781 1649 145 145 0 1636 0
[pid=17051] vsize: 7124
Current children cumulated CPU time (s) 499.96
Current children cumulated vsize (Kb) 9248

[startup+510.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 3425 0 0 0 50979 17 0 0 25 0 1 0 1855368072 7294976 1649 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1781 1649 145 145 0 1636 0
[pid=17051] vsize: 7124
Current children cumulated CPU time (s) 509.96
Current children cumulated vsize (Kb) 9248

[startup+520.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 3425 0 0 0 51979 17 0 0 25 0 1 0 1855368072 7294976 1649 4294967295 134512640 135094434 3221224432 3221220652 134676331 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1781 1649 145 145 0 1636 0
[pid=17051] vsize: 7124
Current children cumulated CPU time (s) 519.96
Current children cumulated vsize (Kb) 9248

[startup+530.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 3425 0 0 0 52979 17 0 0 25 0 1 0 1855368072 7294976 1649 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1781 1649 145 145 0 1636 0
[pid=17051] vsize: 7124
Current children cumulated CPU time (s) 529.96
Current children cumulated vsize (Kb) 9248

[startup+540.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 3425 0 0 0 53979 17 0 0 25 0 1 0 1855368072 7294976 1649 4294967295 134512640 135094434 3221224432 3221220208 134600167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1781 1649 145 145 0 1636 0
[pid=17051] vsize: 7124
Current children cumulated CPU time (s) 539.96
Current children cumulated vsize (Kb) 9248

[startup+550.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 3425 0 0 0 54979 17 0 0 25 0 1 0 1855368072 7294976 1649 4294967295 134512640 135094434 3221224432 3221221200 134677099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1781 1649 145 145 0 1636 0
[pid=17051] vsize: 7124
Current children cumulated CPU time (s) 549.96
Current children cumulated vsize (Kb) 9248

[startup+560.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 3425 0 0 0 55979 17 0 0 25 0 1 0 1855368072 7294976 1649 4294967295 134512640 135094434 3221224432 3221220112 134677091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1781 1649 145 145 0 1636 0
[pid=17051] vsize: 7124
Current children cumulated CPU time (s) 559.96
Current children cumulated vsize (Kb) 9248

[startup+570.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 3425 0 0 0 56980 17 0 0 25 0 1 0 1855368072 7294976 1649 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1781 1649 145 145 0 1636 0
[pid=17051] vsize: 7124
Current children cumulated CPU time (s) 569.97
Current children cumulated vsize (Kb) 9248

[startup+580.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 3425 0 0 0 57980 17 0 0 25 0 1 0 1855368072 7294976 1649 4294967295 134512640 135094434 3221224432 3221220496 134676317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1781 1649 145 145 0 1636 0
[pid=17051] vsize: 7124
Current children cumulated CPU time (s) 579.97
Current children cumulated vsize (Kb) 9248

[startup+590.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 3425 0 0 0 58980 17 0 0 25 0 1 0 1855368072 7294976 1649 4294967295 134512640 135094434 3221224432 3221220224 134600267 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1781 1649 145 145 0 1636 0
[pid=17051] vsize: 7124
Current children cumulated CPU time (s) 589.97
Current children cumulated vsize (Kb) 9248

[startup+600.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 3425 0 0 0 59980 17 0 0 25 0 1 0 1855368072 7294976 1649 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1781 1649 145 145 0 1636 0
[pid=17051] vsize: 7124
Current children cumulated CPU time (s) 599.97
Current children cumulated vsize (Kb) 9248

[startup+610.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 3425 0 0 0 60980 18 0 0 25 0 1 0 1855368072 7294976 1649 4294967295 134512640 135094434 3221224432 3221220576 134677351 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1781 1649 145 145 0 1636 0
[pid=17051] vsize: 7124
Current children cumulated CPU time (s) 609.98
Current children cumulated vsize (Kb) 9248

[startup+620.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4259 0 0 0 61975 21 0 0 25 0 1 0 1855368072 7786496 1681 4294967295 134512640 135094434 3221224432 3221219520 134676589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1901 1681 145 145 0 1756 0
[pid=17051] vsize: 7604
Current children cumulated CPU time (s) 619.96
Current children cumulated vsize (Kb) 9728

[startup+630.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4259 0 0 0 62976 21 0 0 25 0 1 0 1855368072 7786496 1681 4294967295 134512640 135094434 3221224432 3221219344 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1901 1681 145 145 0 1756 0
[pid=17051] vsize: 7604
Current children cumulated CPU time (s) 629.97
Current children cumulated vsize (Kb) 9728

[startup+640.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17051
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4259 0 0 0 63976 21 0 0 25 0 1 0 1855368072 7786496 1681 4294967295 134512640 135094434 3221224432 3221220224 134600254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1901 1681 145 145 0 1756 0
[pid=17051] vsize: 7604
Current children cumulated CPU time (s) 639.97
Current children cumulated vsize (Kb) 9728

[startup+650.049 s]
Raw data (loadavg): 1.07 0.99 0.96 3/59 17099
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4259 0 0 0 64959 37 0 0 25 0 1 0 1855368072 7786496 1681 4294967295 134512640 135094434 3221224432 3221219696 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1901 1681 145 145 0 1756 0
[pid=17051] vsize: 7604
Current children cumulated CPU time (s) 649.96
Current children cumulated vsize (Kb) 9728

[startup+660.05 s]
Raw data (loadavg): 1.06 0.99 0.96 2/57 17102
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4259 0 0 0 65959 37 0 0 25 0 1 0 1855368072 7786496 1681 4294967295 134512640 135094434 3221224432 3221220108 134677228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1901 1681 145 145 0 1756 0
[pid=17051] vsize: 7604
Current children cumulated CPU time (s) 659.96
Current children cumulated vsize (Kb) 9728

[startup+670.051 s]
Raw data (loadavg): 1.05 0.99 0.96 2/57 17102
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4259 0 0 0 66959 37 0 0 25 0 1 0 1855368072 7786496 1681 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1901 1681 145 145 0 1756 0
[pid=17051] vsize: 7604
Current children cumulated CPU time (s) 669.96
Current children cumulated vsize (Kb) 9728

[startup+680.052 s]
Raw data (loadavg): 1.04 0.99 0.96 2/57 17102
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4259 0 0 0 67959 37 0 0 25 0 1 0 1855368072 7786496 1681 4294967295 134512640 135094434 3221224432 3221221272 134600234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1901 1681 145 145 0 1756 0
[pid=17051] vsize: 7604
Current children cumulated CPU time (s) 679.96
Current children cumulated vsize (Kb) 9728

[startup+690.052 s]
Raw data (loadavg): 1.04 0.99 0.96 2/57 17102
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4259 0 0 0 68960 38 0 0 25 0 1 0 1855368072 7786496 1681 4294967295 134512640 135094434 3221224432 3221218872 134676609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1901 1681 145 145 0 1756 0
[pid=17051] vsize: 7604
Current children cumulated CPU time (s) 689.98
Current children cumulated vsize (Kb) 9728

[startup+700.053 s]
Raw data (loadavg): 1.03 0.99 0.96 2/57 17102
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4259 0 0 0 69960 38 0 0 25 0 1 0 1855368072 7786496 1681 4294967295 134512640 135094434 3221224432 3221220224 134677300 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1901 1681 145 145 0 1756 0
[pid=17051] vsize: 7604
Current children cumulated CPU time (s) 699.98
Current children cumulated vsize (Kb) 9728

[startup+710.054 s]
Raw data (loadavg): 1.03 0.99 0.96 2/57 17102
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4259 0 0 0 70960 38 0 0 25 0 1 0 1855368072 7786496 1681 4294967295 134512640 135094434 3221224432 3221220048 134676601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1901 1681 145 145 0 1756 0
[pid=17051] vsize: 7604
Current children cumulated CPU time (s) 709.98
Current children cumulated vsize (Kb) 9728

[startup+720.054 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4259 0 0 0 71960 38 0 0 25 0 1 0 1855368072 7786496 1681 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1901 1681 145 145 0 1756 0
[pid=17051] vsize: 7604
Current children cumulated CPU time (s) 719.98
Current children cumulated vsize (Kb) 9728

[startup+730.055 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4259 0 0 0 72960 38 0 0 25 0 1 0 1855368072 7786496 1681 4294967295 134512640 135094434 3221224432 3221221100 134600233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1901 1681 145 145 0 1756 0
[pid=17051] vsize: 7604
Current children cumulated CPU time (s) 729.98
Current children cumulated vsize (Kb) 9728

[startup+740.056 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4259 0 0 0 73960 38 0 0 25 0 1 0 1855368072 7786496 1681 4294967295 134512640 135094434 3221224432 3221220752 134600904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1901 1681 145 145 0 1756 0
[pid=17051] vsize: 7604
Current children cumulated CPU time (s) 739.98
Current children cumulated vsize (Kb) 9728

[startup+750.057 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4259 0 0 0 74961 38 0 0 25 0 1 0 1855368072 7786496 1681 4294967295 134512640 135094434 3221224432 3221221104 134677333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1901 1681 145 145 0 1756 0
[pid=17051] vsize: 7604
Current children cumulated CPU time (s) 749.99
Current children cumulated vsize (Kb) 9728

[startup+760.057 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4259 0 0 0 75963 38 0 0 25 0 1 0 1855368072 7786496 1681 4294967295 134512640 135094434 3221224432 3221221164 134676460 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1901 1681 145 145 0 1756 0
[pid=17051] vsize: 7604
Current children cumulated CPU time (s) 760.01
Current children cumulated vsize (Kb) 9728

[startup+770.079 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4590 0 0 0 76962 39 0 0 25 0 1 0 1855368072 7692288 1668 4294967295 134512640 135094434 3221224432 3221219068 134676331 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1878 1668 145 145 0 1733 0
[pid=17051] vsize: 7512
Current children cumulated CPU time (s) 770.01
Current children cumulated vsize (Kb) 9636

[startup+780.08 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4590 0 0 0 77962 39 0 0 25 0 1 0 1855368072 7692288 1668 4294967295 134512640 135094434 3221224432 3221219344 134676516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1878 1668 145 145 0 1733 0
[pid=17051] vsize: 7512
Current children cumulated CPU time (s) 780.01
Current children cumulated vsize (Kb) 9636

[startup+790.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4590 0 0 0 78962 39 0 0 25 0 1 0 1855368072 7692288 1668 4294967295 134512640 135094434 3221224432 3221219344 134677313 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1878 1668 145 145 0 1733 0
[pid=17051] vsize: 7512
Current children cumulated CPU time (s) 790.01
Current children cumulated vsize (Kb) 9636

[startup+800.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4590 0 0 0 79962 39 0 0 25 0 1 0 1855368072 7692288 1668 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1878 1668 145 145 0 1733 0
[pid=17051] vsize: 7512
Current children cumulated CPU time (s) 800.01
Current children cumulated vsize (Kb) 9636

[startup+810.081 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4590 0 0 0 80962 39 0 0 25 0 1 0 1855368072 7692288 1668 4294967295 134512640 135094434 3221224432 3221220400 134676510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1878 1668 145 145 0 1733 0
[pid=17051] vsize: 7512
Current children cumulated CPU time (s) 810.01
Current children cumulated vsize (Kb) 9636

[startup+820.081 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4590 0 0 0 81962 39 0 0 25 0 1 0 1855368072 7692288 1668 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1878 1668 145 145 0 1733 0
[pid=17051] vsize: 7512
Current children cumulated CPU time (s) 820.01
Current children cumulated vsize (Kb) 9636

[startup+830.082 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4590 0 0 0 82962 39 0 0 25 0 1 0 1855368072 7692288 1668 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1878 1668 145 145 0 1733 0
[pid=17051] vsize: 7512
Current children cumulated CPU time (s) 830.01
Current children cumulated vsize (Kb) 9636

[startup+840.083 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4590 0 0 0 83963 39 0 0 25 0 1 0 1855368072 7692288 1668 4294967295 134512640 135094434 3221224432 3221220752 134600254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1878 1668 145 145 0 1733 0
[pid=17051] vsize: 7512
Current children cumulated CPU time (s) 840.02
Current children cumulated vsize (Kb) 9636

[startup+850.082 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4590 0 0 0 84963 39 0 0 25 0 1 0 1855368072 7692288 1668 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1878 1668 145 145 0 1733 0
[pid=17051] vsize: 7512
Current children cumulated CPU time (s) 850.02
Current children cumulated vsize (Kb) 9636

[startup+860.083 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4590 0 0 0 85963 39 0 0 25 0 1 0 1855368072 7692288 1668 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1878 1668 145 145 0 1733 0
[pid=17051] vsize: 7512
Current children cumulated CPU time (s) 860.02
Current children cumulated vsize (Kb) 9636

[startup+870.083 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4590 0 0 0 86963 39 0 0 25 0 1 0 1855368072 7692288 1668 4294967295 134512640 135094434 3221224432 3221221000 134677084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1878 1668 145 145 0 1733 0
[pid=17051] vsize: 7512
Current children cumulated CPU time (s) 870.02
Current children cumulated vsize (Kb) 9636

[startup+880.084 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4590 0 0 0 87963 40 0 0 25 0 1 0 1855368072 7692288 1668 4294967295 134512640 135094434 3221224432 3221221200 134677021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1878 1668 145 145 0 1733 0
[pid=17051] vsize: 7512
Current children cumulated CPU time (s) 880.03
Current children cumulated vsize (Kb) 9636

[startup+890.085 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4590 0 0 0 88963 40 0 0 25 0 1 0 1855368072 7692288 1668 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1878 1668 145 145 0 1733 0
[pid=17051] vsize: 7512
Current children cumulated CPU time (s) 890.03
Current children cumulated vsize (Kb) 9636

[startup+900.085 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4590 0 0 0 89964 40 0 0 25 0 1 0 1855368072 7692288 1668 4294967295 134512640 135094434 3221224432 3221220560 134600241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1878 1668 145 145 0 1733 0
[pid=17051] vsize: 7512
Current children cumulated CPU time (s) 900.04
Current children cumulated vsize (Kb) 9636

[startup+910.086 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 4590 0 0 0 90964 40 0 0 25 0 1 0 1855368072 7692288 1668 4294967295 134512640 135094434 3221224432 3221221280 134677363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1878 1668 145 145 0 1733 0
[pid=17051] vsize: 7512
Current children cumulated CPU time (s) 910.04
Current children cumulated vsize (Kb) 9636

[startup+920.085 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 5508 0 0 0 91958 43 0 0 25 0 1 0 1855368072 7741440 1689 4294967295 134512640 135094434 3221224432 3221218464 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1890 1689 145 145 0 1745 0
[pid=17051] vsize: 7560
Current children cumulated CPU time (s) 920.01
Current children cumulated vsize (Kb) 9684

[startup+930.086 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 5508 0 0 0 92958 43 0 0 25 0 1 0 1855368072 7741440 1689 4294967295 134512640 135094434 3221224432 3221219696 134676510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1890 1689 145 145 0 1745 0
[pid=17051] vsize: 7560
Current children cumulated CPU time (s) 930.01
Current children cumulated vsize (Kb) 9684

[startup+940.087 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 5508 0 0 0 93959 43 0 0 25 0 1 0 1855368072 7741440 1689 4294967295 134512640 135094434 3221224432 3221220020 134676380 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1890 1689 145 145 0 1745 0
[pid=17051] vsize: 7560
Current children cumulated CPU time (s) 940.02
Current children cumulated vsize (Kb) 9684

[startup+950.087 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17106
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 5508 0 0 0 94959 43 0 0 25 0 1 0 1855368072 7741440 1689 4294967295 134512640 135094434 3221224432 3221220048 134677248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1890 1689 145 145 0 1745 0
[pid=17051] vsize: 7560
Current children cumulated CPU time (s) 950.02
Current children cumulated vsize (Kb) 9684

[startup+960.088 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 5508 0 0 0 95959 43 0 0 25 0 1 0 1855368072 7741440 1689 4294967295 134512640 135094434 3221224432 3221220400 134600915 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1890 1689 145 145 0 1745 0
[pid=17051] vsize: 7560
Current children cumulated CPU time (s) 960.02
Current children cumulated vsize (Kb) 9684

[startup+970.088 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 5508 0 0 0 96959 44 0 0 25 0 1 0 1855368072 7741440 1689 4294967295 134512640 135094434 3221224432 3221220144 134677065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1890 1689 145 145 0 1745 0
[pid=17051] vsize: 7560
Current children cumulated CPU time (s) 970.03
Current children cumulated vsize (Kb) 9684

[startup+980.088 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 5508 0 0 0 97959 44 0 0 25 0 1 0 1855368072 7741440 1689 4294967295 134512640 135094434 3221224432 3221221104 134677278 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1890 1689 145 145 0 1745 0
[pid=17051] vsize: 7560
Current children cumulated CPU time (s) 980.03
Current children cumulated vsize (Kb) 9684

[startup+990.089 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 5508 0 0 0 98959 44 0 0 25 0 1 0 1855368072 7741440 1689 4294967295 134512640 135094434 3221224432 3221219696 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1890 1689 145 145 0 1745 0
[pid=17051] vsize: 7560
Current children cumulated CPU time (s) 990.03
Current children cumulated vsize (Kb) 9684

[startup+1000.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 5508 0 0 0 99959 44 0 0 25 0 1 0 1855368072 7741440 1689 4294967295 134512640 135094434 3221224432 3221219520 134600291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1890 1689 145 145 0 1745 0
[pid=17051] vsize: 7560
Current children cumulated CPU time (s) 1000.03
Current children cumulated vsize (Kb) 9684

[startup+1010.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 5508 0 0 0 100960 44 0 0 25 0 1 0 1855368072 7741440 1689 4294967295 134512640 135094434 3221224432 3221220752 134600175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1890 1689 145 145 0 1745 0
[pid=17051] vsize: 7560
Current children cumulated CPU time (s) 1010.04
Current children cumulated vsize (Kb) 9684

[startup+1020.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 5508 0 0 0 101960 44 0 0 25 0 1 0 1855368072 7741440 1689 4294967295 134512640 135094434 3221224432 3221220208 134600162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1890 1689 145 145 0 1745 0
[pid=17051] vsize: 7560
Current children cumulated CPU time (s) 1020.04
Current children cumulated vsize (Kb) 9684

[startup+1030.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 5508 0 0 0 102960 44 0 0 25 0 1 0 1855368072 7741440 1689 4294967295 134512640 135094434 3221224432 3221220496 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1890 1689 145 145 0 1745 0
[pid=17051] vsize: 7560
Current children cumulated CPU time (s) 1030.04
Current children cumulated vsize (Kb) 9684

[startup+1040.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 5508 0 0 0 103960 44 0 0 25 0 1 0 1855368072 7741440 1689 4294967295 134512640 135094434 3221224432 3221219696 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1890 1689 145 145 0 1745 0
[pid=17051] vsize: 7560
Current children cumulated CPU time (s) 1040.04
Current children cumulated vsize (Kb) 9684

[startup+1050.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 5508 0 0 0 104960 44 0 0 25 0 1 0 1855368072 7741440 1689 4294967295 134512640 135094434 3221224432 3221221280 134600186 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1890 1689 145 145 0 1745 0
[pid=17051] vsize: 7560
Current children cumulated CPU time (s) 1050.04
Current children cumulated vsize (Kb) 9684

[startup+1060.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 5508 0 0 0 105960 44 0 0 25 0 1 0 1855368072 7741440 1689 4294967295 134512640 135094434 3221224432 3221220224 134600307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1890 1689 145 145 0 1745 0
[pid=17051] vsize: 7560
Current children cumulated CPU time (s) 1060.04
Current children cumulated vsize (Kb) 9684

[startup+1070.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 6715 0 0 0 106954 48 0 0 25 0 1 0 1855368072 8105984 1787 4294967295 134512640 135094434 3221224432 3221219688 134600155 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1979 1787 145 145 0 1834 0
[pid=17051] vsize: 7916
Current children cumulated CPU time (s) 1070.02
Current children cumulated vsize (Kb) 10040

[startup+1080.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 6715 0 0 0 107954 48 0 0 25 0 1 0 1855368072 8105984 1787 4294967295 134512640 135094434 3221224432 3221219520 134600204 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1979 1787 145 145 0 1834 0
[pid=17051] vsize: 7916
Current children cumulated CPU time (s) 1080.02
Current children cumulated vsize (Kb) 10040

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 6715 0 0 0 108954 48 0 0 25 0 1 0 1855368072 8105984 1787 4294967295 134512640 135094434 3221224432 3221219344 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1979 1787 145 145 0 1834 0
[pid=17051] vsize: 7916
Current children cumulated CPU time (s) 1090.02
Current children cumulated vsize (Kb) 10040

[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 6715 0 0 0 109954 48 0 0 25 0 1 0 1855368072 8105984 1787 4294967295 134512640 135094434 3221224432 3221220020 134676380 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1979 1787 145 145 0 1834 0
[pid=17051] vsize: 7916
Current children cumulated CPU time (s) 1100.02
Current children cumulated vsize (Kb) 10040

[startup+1110.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 6715 0 0 0 110955 48 0 0 25 0 1 0 1855368072 8105984 1787 4294967295 134512640 135094434 3221224432 3221219520 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1979 1787 145 145 0 1834 0
[pid=17051] vsize: 7916
Current children cumulated CPU time (s) 1110.03
Current children cumulated vsize (Kb) 10040

[startup+1120.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 6715 0 0 0 111955 48 0 0 25 0 1 0 1855368072 8105984 1787 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1979 1787 145 145 0 1834 0
[pid=17051] vsize: 7916
Current children cumulated CPU time (s) 1120.03
Current children cumulated vsize (Kb) 10040

[startup+1130.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 6715 0 0 0 112955 48 0 0 25 0 1 0 1855368072 8105984 1787 4294967295 134512640 135094434 3221224432 3221220624 134677375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1979 1787 145 145 0 1834 0
[pid=17051] vsize: 7916
Current children cumulated CPU time (s) 1130.03
Current children cumulated vsize (Kb) 10040

[startup+1140.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 6715 0 0 0 113955 48 0 0 25 0 1 0 1855368072 8105984 1787 4294967295 134512640 135094434 3221224432 3221219968 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1979 1787 145 145 0 1834 0
[pid=17051] vsize: 7916
Current children cumulated CPU time (s) 1140.03
Current children cumulated vsize (Kb) 10040

[startup+1150.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 6715 0 0 0 114955 48 0 0 25 0 1 0 1855368072 8105984 1787 4294967295 134512640 135094434 3221224432 3221221456 134600301 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1979 1787 145 145 0 1834 0
[pid=17051] vsize: 7916
Current children cumulated CPU time (s) 1150.03
Current children cumulated vsize (Kb) 10040

[startup+1160.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 6715 0 0 0 115955 49 0 0 25 0 1 0 1855368072 8105984 1787 4294967295 134512640 135094434 3221224432 3221220576 134676601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1979 1787 145 145 0 1834 0
[pid=17051] vsize: 7916
Current children cumulated CPU time (s) 1160.04
Current children cumulated vsize (Kb) 10040

[startup+1170.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 6715 0 0 0 116956 49 0 0 25 0 1 0 1855368072 8105984 1787 4294967295 134512640 135094434 3221224432 3221220732 134677150 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1979 1787 145 145 0 1834 0
[pid=17051] vsize: 7916
Current children cumulated CPU time (s) 1170.05
Current children cumulated vsize (Kb) 10040

[startup+1180.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 6715 0 0 0 117956 49 0 0 25 0 1 0 1855368072 8105984 1787 4294967295 134512640 135094434 3221224432 3221220848 134676294 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1979 1787 145 145 0 1834 0
[pid=17051] vsize: 7916
Current children cumulated CPU time (s) 1180.05
Current children cumulated vsize (Kb) 10040

[startup+1190.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 6715 0 0 0 118956 49 0 0 25 0 1 0 1855368072 8105984 1787 4294967295 134512640 135094434 3221224432 3221220828 134676331 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1979 1787 145 145 0 1834 0
[pid=17051] vsize: 7916
Current children cumulated CPU time (s) 1190.05
Current children cumulated vsize (Kb) 10040

[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 6715 0 0 0 119956 49 0 0 25 0 1 0 1855368072 8105984 1787 4294967295 134512640 135094434 3221224432 3221220372 134676992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1979 1787 145 145 0 1834 0
[pid=17051] vsize: 7916
Current children cumulated CPU time (s) 1200.05
Current children cumulated vsize (Kb) 10040



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17108
Raw data (/proc/17047/stat): 17047 (minisat+_script) S 17046 17047 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855368067 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17047/statm): 531 226 485 147 0 384 0
[pid=17047] vsize: 2124
Raw data (/proc/17051/stat): 17051 (minisat+_64-bit) R 17047 17047 16528 0 -1 0 6715 0 0 0 119956 49 0 0 25 0 1 0 1855368072 8105984 1787 4294967295 134512640 135094434 3221224432 3221220048 134676519 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17051/statm): 1979 1787 145 145 0 1834 0
[pid=17051] vsize: 7916
Current children cumulated CPU time (s) 1200.05
Current children cumulated vsize (Kb) 10040

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

Child status: 0
Real time (s): 1200.11
CPU time (s): 1200.06
CPU user time (s): 1199.57
CPU system time (s): 0.496924
CPU usage (%): 99.9963
Max. virtual memory (cumulated for all children) (Kb): 10040

Verifier Data

ERROR: no interpretation found !