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/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-UMTS.opb
MD5SUM87bf784911047f4cd00952d2cf8f9593
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 55110269
Optimality of the best value was proved NO
Number of terms in the objective function 3666
Biggest coefficient in the objective function 184242176
Number of bits for the biggest coefficient in the objective function 28
Sum of the numbers in the objective function 22915217490
Number of bits of the sum of numbers in the objective function 35
Biggest number in a constraint 128000000000
Number of bits of the biggest number in a constraint 37
Biggest sum of numbers in a constraint 128001048575
Number of bits of the biggest sum of numbers37
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.12
Number of variables5178
Total number of constraints7267
Number of constraints which are clauses2785
Number of constraints which are cardinality constraints (but not clauses)4230
Number of constraints which are nor clauses,nor cardinality constraints252
Minimum length of a constraint1
Maximum length of a constraint391

Trace number 6344

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        918148 kB
Buffers:          8100 kB
Cached:          80640 kB
SwapCached:        612 kB
Active:          19832 kB
Inactive:        71380 kB
HighTotal:      131008 kB
HighFree:        46312 kB
LowTotal:       903652 kB
LowFree:        871836 kB
SwapTotal:     2097892 kB
SwapFree:      2096676 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5676 kB
Slab:            19552 kB
Committed_AS:    64316 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 06:06:45 (client local time) WITH STATUS 0 IN 1206.65 SECONDS
stats: 3505 7 1206.65 0

Solver Data

c Parsing PB file...
c Converting 2057 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #############################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssss..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................ssssssssssss.
c ---[2079]---> BDD-cost:   21
c ---[2077]---> BDD-cost:   21
c ---[2075]---> BDD-cost:   21
c ---[2073]---> BDD-cost:   21
c ---[2071]---> BDD-cost:   21
c ---[2069]---> BDD-cost:   21
c ---[2067]---> BDD-cost:   21
c ---[2065]---> BDD-cost:   21
c ---[2063]---> BDD-cost:   21
c ---[2061]---> BDD-cost:   21
c ---[2059]---> BDD-cost:   21
c ---[2057]---> BDD-cost:   21
c ---[2055]---> BDD-cost:   21
c ---[2053]---> BDD-cost:   21
c ---[2051]---> BDD-cost:   21
c ---[2049]---> BDD-cost:   21
c ---[2047]---> BDD-cost:   21
c ---[2045]---> BDD-cost:   21
c ---[2043]---> BDD-cost:   21
c ---[2041]---> BDD-cost:   19
c ---[2039]---> BDD-cost:   21
c ---[2037]---> BDD-cost:   21
c ---[2035]---> BDD-cost:   21
c ---[2033]---> BDD-cost:   21
c ---[2031]---> BDD-cost:   21
c ---[2029]---> BDD-cost:   21
c ---[2027]---> BDD-cost:   21
c ---[2025]---> BDD-cost:   21
c ---[2023]---> BDD-cost:   21
c ---[2021]---> BDD-cost:   21
c ---[2019]---> BDD-cost:   19
c ---[2017]---> BDD-cost:   19
c ---[2015]---> BDD-cost:   21
c ---[2013]---> BDD-cost:   21
c ---[2011]---> BDD-cost:   21
c ---[2009]---> BDD-cost:   21
c ---[2007]---> BDD-cost:   21
c ---[2005]---> BDD-cost:   21
c ---[2003]---> BDD-cost:   21
c ---[2001]---> BDD-cost:   21
c ---[1999]---> BDD-cost:   21
c ---[1997]---> BDD-cost:   21
c ---[1995]---> BDD-cost:   21
c ---[1993]---> BDD-cost:   21
c ---[1991]---> BDD-cost:   21
c ---[1989]---> BDD-cost:   21
c ---[1987]---> BDD-cost:   21
c ---[1985]---> BDD-cost:   21
c ---[1983]---> BDD-cost:   21
c ---[1981]---> BDD-cost:   19
c ---[1979]---> BDD-cost:   21
c ---[1977]---> BDD-cost:   21
c ---[1975]---> BDD-cost:   21
c ---[1973]---> BDD-cost:   19
c ---[1971]---> BDD-cost:   21
c ---[1969]---> BDD-cost:   19
c ---[1967]---> BDD-cost:   21
c ---[1965]---> BDD-cost:   21
c ---[1963]---> BDD-cost:   21
c ---[1961]---> BDD-cost:   21
c ---[1959]---> BDD-cost:   19
c ---[1957]---> BDD-cost:   15
c ---[1955]---> BDD-cost:   21
c ---[1953]---> BDD-cost:   15
c ---[1951]---> BDD-cost:   19
c ---[1949]---> BDD-cost:   17
c ---[1947]---> BDD-cost:   17
c ---[1945]---> BDD-cost:   15
c ---[1943]---> BDD-cost:   19
c ---[1941]---> BDD-cost:   15
c ---[1939]---> BDD-cost:   17
c ---[1937]---> BDD-cost:   17
c ---[1935]---> BDD-cost:   15
c ---[1933]---> BDD-cost:   21
c ---[1931]---> BDD-cost:   15
c ---[1929]---> BDD-cost:   17
c ---[1927]---> BDD-cost:   15
c ---[1925]---> BDD-cost:   21
c ---[1923]---> BDD-cost:   19
c ---[1921]---> BDD-cost:   21
c ---[1919]---> BDD-cost:   15
c ---[1917]---> BDD-cost:   19
c ---[1915]---> BDD-cost:   19
c ---[1913]---> BDD-cost:   19
c ---[1911]---> BDD-cost:   15
c ---[1909]---> BDD-cost:   13
c ---[1907]---> BDD-cost:   17
c ---[1905]---> BDD-cost:   15
c ---[1903]---> BDD-cost:   17
c ---[1901]---> BDD-cost:   17
c ---[1899]---> BDD-cost:   19
c ---[1897]---> BDD-cost:   19
c ---[1895]---> BDD-cost:   15
c ---[1893]---> BDD-cost:   19
c ---[1891]---> BDD-cost:   15
c ---[1889]---> BDD-cost:   19
c ---[1887]---> BDD-cost:   19
c ---[1885]---> BDD-cost:   17
c ---[1883]---> BDD-cost:   21
c ---[1881]---> BDD-cost:   15
c ---[1879]---> BDD-cost:   13
c ---[1877]---> BDD-cost:   19
c ---[1875]---> BDD-cost:   17
c ---[1873]---> BDD-cost:   19
c ---[1871]---> BDD-cost:   19
c ---[1869]---> BDD-cost:   11
c ---[1867]---> BDD-cost:   15
c ---[1865]---> BDD-cost:   15
c ---[1863]---> BDD-cost:   17
c ---[1861]---> BDD-cost:   11
c ---[1859]---> BDD-cost:    5
c ---[1857]---> BDD-cost:   13
c ---[1855]---> BDD-cost:   13
c ---[1853]---> BDD-cost:   11
c ---[1851]---> BDD-cost:    7
c ---[1849]---> BDD-cost:    1
c ---[1847]---> BDD-cost:    1
c ---[1845]---> BDD-cost:   11
c ---[1843]---> BDD-cost:    9
c ---[1841]---> BDD-cost:    1
c ---[1839]---> BDD-cost:   15
c ---[1837]---> BDD-cost:    3
c ---[1835]---> BDD-cost:   15
c ---[1833]---> BDD-cost:    9
c ---[1831]---> BDD-cost:    9
c ---[1829]---> BDD-cost:    7
c ---[1827]---> BDD-cost:    5
c ---[1825]---> BDD-cost:   11
c ---[1823]---> BDD-cost:    3
c ---[1821]---> BDD-cost:    5
c ---[1819]---> BDD-cost:    9
c ---[1817]---> BDD-cost:   11
c ---[1815]---> BDD-cost:    7
c ---[1813]---> BDD-cost:    7
c ---[1811]---> BDD-cost:    7
c ---[1809]---> BDD-cost:    3
c ---[1807]---> BDD-cost:    1
c ---[1805]---> BDD-cost:    9
c ---[1803]---> BDD-cost:   13
c ---[1801]---> BDD-cost:    7
c ---[1799]---> BDD-cost:    1
c ---[1797]---> BDD-cost:   15
c ---[1795]---> BDD-cost:    9
c ---[1793]---> BDD-cost:   13
c ---[1791]---> BDD-cost:    5
c ---[1789]---> BDD-cost:    9
c ---[1787]---> BDD-cost:   13
c ---[1785]---> BDD-cost:    1
c ---[1783]---> BDD-cost:   15
c ---[1782]---> Adder-cost: 704   maxlim: 3660   bits: 13/12
c ---[1781]---> Adder-cost: 704   maxlim: 3632   bits: 13/12
c ---[1780]---> Adder-cost: 596   maxlim: 2992   bits: 12/12
c ---[1779]---> Adder-cost: 726   maxlim: 3659   bits: 13/12
c ---[1778]---> Adder-cost: 704   maxlim: 3660   bits: 13/12
c ---[1777]---> Adder-cost: 596   maxlim: 2992   bits: 12/12
c ---[1776]---> Adder-cost: 640   maxlim: 3233   bits: 13/12
c ---[1775]---> Adder-cost: 586   maxlim: 2867   bits: 12/12
c ---[1774]---> Adder-cost: 532   maxlim: 2604   bits: 12/12
c ---[1773]---> Adder-cost: 640   maxlim: 3236   bits: 13/12
c ---[1772]---> Adder-cost: 662   maxlim: 3208   bits: 13/12
c ---[1771]---> Adder-cost: 610   maxlim: 2927   bits: 12/12
c ---[1770]---> Adder-cost: 266   maxlim: 132   bits: 8/8
c ---[1769]---> Adder-cost: 266   maxlim: 131   bits: 8/8
c ---[1768]---> Adder-cost: 228   maxlim: 110   bits: 8/7
c ---[1767]---> Adder-cost: 266   maxlim: 132   bits: 8/8
c ---[1766]---> Adder-cost: 266   maxlim: 132   bits: 8/8
c ---[1765]---> Adder-cost: 228   maxlim: 110   bits: 8/7
c ---[1764]---> Adder-cost: 244   maxlim: 120   bits: 8/7
c ---[1763]---> Adder-cost: 228   maxlim: 110   bits: 8/7
c ---[1762]---> Adder-cost: 204   maxlim: 99   bits: 8/7
c ---[1761]---> Adder-cost: 242   maxlim: 117   bits: 8/7
c ---[1760]---> Adder-cost: 234   maxlim: 115   bits: 8/7
c ---[1759]---> Adder-cost: 218   maxlim: 108   bits: 8/7
c ---[1758]---> Adder-cost: 136   maxlim: 132   bits: 8/8
c ---[1757]---> Adder-cost: 136   maxlim: 131   bits: 8/8
c ---[1756]---> Adder-cost: 114   maxlim: 110   bits: 8/7
c ---[1755]---> Adder-cost: 136   maxlim: 132   bits: 8/8
c ---[1754]---> Adder-cost: 136   maxlim: 132   bits: 8/8
c ---[1753]---> Adder-cost: 114   maxlim: 110   bits: 8/7
c ---[1752]---> Adder-cost: 122   maxlim: 120   bits: 8/7
c ---[1751]---> Adder-cost: 114   maxlim: 110   bits: 8/7
c ---[1750]---> Adder-cost: 106   maxlim: 99   bits: 8/7
c ---[1749]---> Adder-cost: 120   maxlim: 117   bits: 8/7
c ---[1748]---> Adder-cost: 116   maxlim: 115   bits: 8/7
c ---[1747]---> Adder-cost: 114   maxlim: 108   bits: 8/7
c ---[1734]---> BDD-cost:    9
c ---[1733]---> BDD-cost:    9
c ---[1732]---> BDD-cost:    9
c ---[1731]---> BDD-cost:    9
c ---[1730]---> BDD-cost:    9
c ---[1729]---> BDD-cost:    9
c ---[1728]---> BDD-cost:    9
c ---[1727]---> BDD-cost:    9
c ---[1726]---> BDD-cost:    9
c ---[1725]---> BDD-cost:    9
c ---[1724]---> BDD-cost:    9
c ---[1723]---> BDD-cost:    9
c ---[1722]---> BDD-cost:    9
c ---[1721]---> BDD-cost:    9
c ---[1720]---> BDD-cost:    9
c ---[1719]---> BDD-cost:    9
c ---[1718]---> BDD-cost:    9
c ---[1717]---> BDD-cost:    9
c ---[1716]---> BDD-cost:    9
c ---[1715]---> BDD-cost:    9
c ---[1714]---> BDD-cost:    9
c ---[1713]---> BDD-cost:    9
c ---[1712]---> BDD-cost:    9
c ---[1711]---> BDD-cost:    9
c ---[1710]---> BDD-cost:    9
c ---[1709]---> BDD-cost:    9
c ---[1708]---> BDD-cost:    9
c ---[1707]---> BDD-cost:    9
c ---[1706]---> BDD-cost:    9
c ---[1705]---> BDD-cost:    9
c ---[1704]---> BDD-cost:    9
c ---[1703]---> BDD-cost:    9
c ---[1702]---> BDD-cost:    9
c ---[1701]---> BDD-cost:    9
c ---[1700]---> BDD-cost:    9
c ---[1699]---> BDD-cost:    9
c ---[1698]---> BDD-cost:    9
c ---[1697]---> BDD-cost:    9
c ---[1696]---> BDD-cost:    9
c ---[1695]---> BDD-cost:    9
c ---[1694]---> BDD-cost:    9
c ---[1693]---> BDD-cost:    9
c ---[1692]---> BDD-cost:    9
c ---[1691]---> BDD-cost:    9
c ---[1690]---> BDD-cost:    9
c ---[1689]---> BDD-cost:    9
c ---[1688]---> BDD-cost:    9
c ---[1687]---> BDD-cost:    9
c ---[1686]---> BDD-cost:    9
c ---[1685]---> BDD-cost:    9
c ---[1684]---> BDD-cost:    9
c ---[1683]---> BDD-cost:    9
c ---[1682]---> BDD-cost:    9
c ---[1681]---> BDD-cost:    9
c ---[1680]---> BDD-cost:    9
c ---[1679]---> BDD-cost:    9
c ---[1678]---> BDD-cost:    9
c ---[1677]---> BDD-cost:    9
c ---[1676]---> BDD-cost:    9
c ---[1675]---> BDD-cost:    9
c ---[1674]---> BDD-cost:    9
c ---[1673]---> BDD-cost:    9
c ---[1672]---> BDD-cost:    9
c ---[1671]---> BDD-cost:    9
c ---[1670]---> BDD-cost:    9
c ---[1669]---> BDD-cost:    9
c ---[1668]---> Adder-cost: 440   maxlim: 6291443   bits: 23/23
c ---[1667]---> Adder-cost: 362   maxlim: 5242869   bits: 23/23
c ---[1666]---> Adder-cost: 398   maxlim: 5767156   bits: 23/23
c ---[1665]---> Adder-cost: 440   maxlim: 6291443   bits: 23/23
c ---[1664]---> Adder-cost: 440   maxlim: 6291443   bits: 23/23
c ---[1663]---> Sorter-cost: 3437     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1661]---> Adder-cost: 649   maxlim: 468608   bits: 20/19
c ---[1659]---> Adder-cost: 657   maxlim: 465024   bits: 20/19
c ---[1657]---> Adder-cost: 583   maxlim: 383104   bits: 20/19
c ---[1655]---> Adder-cost: 647   maxlim: 468480   bits: 20/19
c ---[1653]---> Adder-cost: 649   maxlim: 468608   bits: 20/19
c ---[1651]---> Adder-cost: 583   maxlim: 383104   bits: 20/19
c ---[1649]---> Adder-cost: 607   maxlim: 413952   bits: 20/19
c ---[1647]---> Adder-cost: 573   maxlim: 367104   bits: 20/19
c ---[1645]---> Adder-cost: 599   maxlim: 333440   bits: 20/19
c ---[1643]---> Adder-cost: 724   maxlim: 414336   bits: 20/19
c ---[1641]---> Adder-cost: 680   maxlim: 410752   bits: 20/19
c ---[1639]---> Adder-cost: 609   maxlim: 374784   bits: 20/19
c ---[1638]---> BDD-cost:   19
c ---[1637]---> BDD-cost:   19
c ---[1636]---> BDD-cost:   19
c ---[1635]---> BDD-cost:   19
c ---[1634]---> BDD-cost:   19
c ---[1633]---> BDD-cost:   19
c ---[1632]---> BDD-cost:   19
c ---[1631]---> BDD-cost:   19
c ---[1630]---> BDD-cost:   19
c ---[1629]---> BDD-cost:   19
c ---[1628]---> BDD-cost:   19
c ---[1627]---> BDD-cost:   19
c ---[1626]---> BDD-cost:   19
c ---[1625]---> BDD-cost:   19
c ---[1624]---> BDD-cost:   19
c ---[1623]---> BDD-cost:   19
c ---[1622]---> BDD-cost:   19
c ---[1621]---> BDD-cost:   19
c ---[1620]---> BDD-cost:   19
c ---[1619]---> BDD-cost:   19
c ---[1618]---> BDD-cost:   19
c ---[1617]---> BDD-cost:   19
c ---[1616]---> BDD-cost:   19
c ---[1615]---> BDD-cost:   19
c ---[1614]---> BDD-cost:   19
c ---[1613]---> BDD-cost:   19
c ---[1612]---> BDD-cost:   19
c ---[1611]---> BDD-cost:   19
c ---[1610]---> BDD-cost:   19
c ---[1609]---> BDD-cost:   19
c ---[1608]---> BDD-cost:   19
c ---[1607]---> BDD-cost:   19
c ---[1606]---> BDD-cost:   19
c ---[1605]---> BDD-cost:   19
c ---[1604]---> BDD-cost:   19
c ---[1603]---> BDD-cost:   19
c ---[1602]---> BDD-cost:   19
c ---[1601]---> BDD-cost:   19
c ---[1600]---> BDD-cost:   19
c ---[1599]---> BDD-cost:   19
c ---[1598]---> BDD-cost:   19
c ---[1597]---> BDD-cost:   19
c ---[1596]---> BDD-cost:   19
c ---[1595]---> BDD-cost:   19
c ---[1594]---> BDD-cost:   19
c ---[1593]---> BDD-cost:   19
c ---[1592]---> BDD-cost:   19
c ---[1591]---> BDD-cost:   19
c ---[1590]---> BDD-cost:   19
c ---[1589]---> BDD-cost:   19
c ---[1588]---> BDD-cost:   19
c ---[1587]---> BDD-cost:   19
c ---[1586]---> BDD-cost:   19
c ---[1585]---> BDD-cost:   19
c ---[1584]---> BDD-cost:   19
c ---[1583]---> BDD-cost:   19
c ---[1582]---> BDD-cost:   19
c ---[1581]---> BDD-cost:   19
c ---[1580]---> BDD-cost:   19
c ---[1579]---> BDD-cost:   19
c ---[1578]---> BDD-cost:   19
c ---[1577]---> BDD-cost:   19
c ---[1576]---> BDD-cost:   19
c ---[1575]---> BDD-cost:   19
c ---[1574]---> BDD-cost:   19
c ---[1573]---> BDD-cost:   19
c ---[1572]---> Adder-cost: 216   maxlim: 6131   bits: 13/13
c ---[1571]---> Sorter-cost: 1778     Base: 2 2 2 2 2 2 2 2
c ---[1570]---> Sorter-cost: 2027     Base: 2 2 2 2 2 2 2 2
c ---[1569]---> Adder-cost: 216   maxlim: 6131   bits: 13/13
c ---[1568]---> Adder-cost: 216   maxlim: 6131   bits: 13/13
c ---[1567]---> Sorter-cost: 1520     Base: 2 2 2 2 2 2 2 2
c ---[1553]---> BDD-cost:   18
c ---[1551]---> BDD-cost:   18
c ---[1549]---> BDD-cost:   18
c ---[1547]---> BDD-cost:   18
c ---[1545]---> BDD-cost:   18
c ---[1543]---> BDD-cost:   18
c ---[1541]---> BDD-cost:   18
c ---[1539]---> BDD-cost:   18
c ---[1537]---> BDD-cost:   12
c ---[1535]---> BDD-cost:   15
c ---[1533]---> BDD-cost:   15
c ---[1531]---> BDD-cost:   12
c ---[  23]---> Adder-cost: 741   maxlim: 1264   bits: 12/11
c ---[  22]---> Adder-cost: 737   maxlim: 1255   bits: 12/11
c ---[  21]---> Adder-cost: 631   maxlim: 1036   bits: 12/11
c ---[  20]---> Adder-cost: 791   maxlim: 1264   bits: 12/11
c ---[  19]---> Adder-cost: 741   maxlim: 1264   bits: 12/11
c ---[  18]---> Adder-cost: 631   maxlim: 1036   bits: 12/11
c ---[  17]---> Adder-cost: 711   maxlim: 1124   bits: 12/11
c ---[  16]---> Adder-cost: 688   maxlim: 1005   bits: 11/10
c ---[  15]---> Adder-cost: 542   maxlim: 908   bits: 11/10
c ---[  14]---> Adder-cost: 696   maxlim: 1118   bits: 12/11
c ---[  13]---> Adder-cost: 656   maxlim: 1107   bits: 12/11
c ---[  12]---> Adder-cost: 606   maxlim: 1016   bits: 11/10
c ---[  11]---> BDD-cost:   12
c ---[  10]---> BDD-cost:   12
c ---[   9]---> BDD-cost:   12
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:   12
c ---[   6]---> BDD-cost:   12
c ---[   5]---> BDD-cost:   12
c ---[   4]---> BDD-cost:   12
c ---[   3]---> BDD-cost:    8
c ---[   2]---> BDD-cost:   10
c ---[   1]---> BDD-cost:   10
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  240803   822464 |   80267       0        0     nan |  0.000 % |
c |       101 |  240803   822464 |   88293     101      354     3.5 |  6.471 % |
c |       251 |  240722   822253 |   97123     240     1004     4.2 |  6.511 % |
c |       477 |  240664   822113 |  106835     462     1891     4.1 |  6.541 % |
c |       814 |  240617   821999 |  117518     794     3513     4.4 |  6.571 % |
c |      1321 |  240604   821970 |  129270    1300     6835     5.3 |  6.582 % |
c |      2081 |  240132   820795 |  142197    2042    11479     5.6 |  6.842 % |
c |      3220 |  240055   820622 |  156417    3175    19822     6.2 |  6.899 % |
c |      4929 |  239437   819109 |  172059    4846    42501     8.8 |  7.283 % |
c |      7491 |  239412   819042 |  189265    7404    95242    12.9 |  7.294 % |
c |     11335 |  239399   818996 |  208191   11247   316402    28.1 |  7.296 % |
c |     17105 |  239338   818805 |  229011   17009   481980    28.3 |  7.313 % |
c |     25755 |  239226   818446 |  251912   25639   791453    30.9 |  7.349 % |
c |     38730 |  237679   814576 |  277103   38481  1377468    35.8 |  8.283 % |
c |     58191 |  236814   811725 |  304813   57879  2332505    40.3 |  8.564 % |
c |     87383 |  236262   810014 |  335295   87034  3896929    44.8 |  8.756 % |
c |    131172 |  236019   809323 |  368824  130772  6037488    46.2 |  8.871 % |
c |    196857 |  235198   806962 |  405707  196326  9276321    47.2 |  9.231 % |
c |    295384 |  234125   804093 |  446277  294724 15204559    51.6 |  9.787 % |
c |    443173 |  232855   800381 |  490905  442342 24197118    54.7 | 10.367 % |
c |    664856 |  231702   797191 |  539996  173585  8485304    48.9 | 10.996 % |

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/7709/stat): 7709 (minisat+_script) R 7708 7709 19316 0 -1 0 19 0 0 0 0 0 0 0 21 0 1 0 1856151952 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/7709/statm): 174 3 169 147 0 27 0
[pid=7709] 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=7710
New process pid=7711
New process pid=7712
execve syscall for /bin/sed executable
One traced child (pid=7711) 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=7712) exited with status: 0
One traced child (pid=7710) exited with status: 0
New process pid=7713
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-UMTS.opb

[startup+10.0028 s]
Raw data (loadavg): 0.95 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 5235 0 0 0 948 22 0 0 25 0 1 0 1856151956 22327296 5038 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 5451 5038 145 145 0 5306 0
[pid=7713] vsize: 21804
Current children cumulated CPU time (s) 9.71
Current children cumulated vsize (Kb) 23928

[startup+20.0034 s]
Raw data (loadavg): 0.96 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 5719 0 0 0 1940 25 0 0 25 0 1 0 1856151956 24293376 5522 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 5931 5522 145 145 0 5786 0
[pid=7713] vsize: 23724
Current children cumulated CPU time (s) 19.66
Current children cumulated vsize (Kb) 25848

[startup+30.004 s]
Raw data (loadavg): 0.97 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 6562 0 0 0 2927 30 0 0 25 0 1 0 1856151956 27742208 6365 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 6773 6365 145 145 0 6628 0
[pid=7713] vsize: 27092
Current children cumulated CPU time (s) 29.58
Current children cumulated vsize (Kb) 29216

[startup+40.0046 s]
Raw data (loadavg): 0.97 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 6970 0 0 0 3922 33 0 0 25 0 1 0 1856151956 29519872 6773 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 7207 6773 145 145 0 7062 0
[pid=7713] vsize: 28828
Current children cumulated CPU time (s) 39.56
Current children cumulated vsize (Kb) 30952

[startup+50.0052 s]
Raw data (loadavg): 0.98 0.99 0.99 1/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) T 7709 7709 19316 0 -1 0 7242 0 0 0 4917 34 0 0 25 0 1 0 1856151956 30613504 7045 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7713/statm): 7474 7045 145 145 0 7329 0
[pid=7713] vsize: 29896
Current children cumulated CPU time (s) 49.52
Current children cumulated vsize (Kb) 32020

[startup+60.0058 s]
Raw data (loadavg): 0.98 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 7911 0 0 0 5906 40 0 0 25 0 1 0 1856151956 33312768 7714 4294967295 134512640 135094434 3221224432 3221223088 134557832 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 8133 7714 145 145 0 7988 0
[pid=7713] vsize: 32532
Current children cumulated CPU time (s) 59.47
Current children cumulated vsize (Kb) 34656

[startup+70.0064 s]
Raw data (loadavg): 0.98 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 8193 0 0 0 6901 42 0 0 25 0 1 0 1856151956 34447360 7996 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 8410 7996 145 145 0 8265 0
[pid=7713] vsize: 33640
Current children cumulated CPU time (s) 69.44
Current children cumulated vsize (Kb) 35764

[startup+80.007 s]
Raw data (loadavg): 0.98 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 8829 0 0 0 7889 46 0 0 25 0 1 0 1856151956 37277696 8632 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 9101 8632 145 145 0 8956 0
[pid=7713] vsize: 36404
Current children cumulated CPU time (s) 79.36
Current children cumulated vsize (Kb) 38528

[startup+90.0076 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 9424 0 0 0 8878 51 0 0 25 0 1 0 1856151956 39669760 9227 4294967295 134512640 135094434 3221224432 3221223104 134556468 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 9685 9227 145 145 0 9540 0
[pid=7713] vsize: 38740
Current children cumulated CPU time (s) 89.3
Current children cumulated vsize (Kb) 40864

[startup+100.008 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 10043 0 0 0 9868 55 0 0 25 0 1 0 1856151956 42168320 9846 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 10295 9846 145 145 0 10150 0
[pid=7713] vsize: 41180
Current children cumulated CPU time (s) 99.24
Current children cumulated vsize (Kb) 43304

[startup+110.009 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 10532 0 0 0 10860 58 0 0 25 0 1 0 1856151956 44138496 10335 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 10776 10335 145 145 0 10631 0
[pid=7713] vsize: 43104
Current children cumulated CPU time (s) 109.19
Current children cumulated vsize (Kb) 45228

[startup+120.009 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 11057 0 0 0 11851 62 0 0 25 0 1 0 1856151956 46268416 10860 4294967295 134512640 135094434 3221224432 3221222960 134783138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 11296 10860 145 145 0 11151 0
[pid=7713] vsize: 45184
Current children cumulated CPU time (s) 119.14
Current children cumulated vsize (Kb) 47308

[startup+130.009 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 11437 0 0 0 12845 64 0 0 25 0 1 0 1856151956 47788032 11240 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 11667 11240 145 145 0 11522 0
[pid=7713] vsize: 46668
Current children cumulated CPU time (s) 129.1
Current children cumulated vsize (Kb) 48792

[startup+140.011 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 11801 0 0 0 13837 68 0 0 25 0 1 0 1856151956 49254400 11604 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 12025 11604 145 145 0 11880 0
[pid=7713] vsize: 48100
Current children cumulated CPU time (s) 139.06
Current children cumulated vsize (Kb) 50224

[startup+150.011 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 12266 0 0 0 14830 71 0 0 25 0 1 0 1856151956 51126272 12069 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 12482 12069 145 145 0 12337 0
[pid=7713] vsize: 49928
Current children cumulated CPU time (s) 149.02
Current children cumulated vsize (Kb) 52052

[startup+160.011 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 12563 0 0 0 15826 72 0 0 25 0 1 0 1856151956 52842496 12366 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 12901 12366 145 145 0 12756 0
[pid=7713] vsize: 51604
Current children cumulated CPU time (s) 158.99
Current children cumulated vsize (Kb) 53728

[startup+170.011 s]
Raw data (loadavg): 0.99 0.99 0.99 1/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) T 7709 7709 19316 0 -1 0 13035 0 0 0 16819 74 0 0 25 0 1 0 1856151956 54734848 12838 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7713/statm): 13363 12838 145 145 0 13218 0
[pid=7713] vsize: 53452
Current children cumulated CPU time (s) 168.94
Current children cumulated vsize (Kb) 55576

[startup+180.012 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 13486 0 0 0 17812 78 0 0 25 0 1 0 1856151956 56545280 13289 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 13805 13289 145 145 0 13660 0
[pid=7713] vsize: 55220
Current children cumulated CPU time (s) 178.91
Current children cumulated vsize (Kb) 57344

[startup+190.013 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 13742 0 0 0 18807 79 0 0 25 0 1 0 1856151956 57577472 13545 4294967295 134512640 135094434 3221224432 3221223008 134785278 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 14057 13545 145 145 0 13912 0
[pid=7713] vsize: 56228
Current children cumulated CPU time (s) 188.87
Current children cumulated vsize (Kb) 58352

[startup+200.013 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 14552 0 0 0 19792 85 0 0 25 0 1 0 1856151956 60866560 14355 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 14860 14355 145 145 0 14715 0
[pid=7713] vsize: 59440
Current children cumulated CPU time (s) 198.78
Current children cumulated vsize (Kb) 61564

[startup+210.014 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 15035 0 0 0 20784 88 0 0 25 0 1 0 1856151956 62828544 14838 4294967295 134512640 135094434 3221224432 3221223044 134563074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 15339 14838 145 145 0 15194 0
[pid=7713] vsize: 61356
Current children cumulated CPU time (s) 208.73
Current children cumulated vsize (Kb) 63480

[startup+220.014 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 15463 0 0 0 21778 91 0 0 25 0 1 0 1856151956 64552960 15266 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 15760 15266 145 145 0 15615 0
[pid=7713] vsize: 63040
Current children cumulated CPU time (s) 218.7
Current children cumulated vsize (Kb) 65164

[startup+230.015 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 15951 0 0 0 22768 96 0 0 25 0 1 0 1856151956 66531328 15754 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 16243 15754 145 145 0 16098 0
[pid=7713] vsize: 64972
Current children cumulated CPU time (s) 228.65
Current children cumulated vsize (Kb) 67096

[startup+240.016 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 16339 0 0 0 23762 98 0 0 25 0 1 0 1856151956 68128768 16142 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 16633 16142 145 145 0 16488 0
[pid=7713] vsize: 66532
Current children cumulated CPU time (s) 238.61
Current children cumulated vsize (Kb) 68656

[startup+250.016 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 16668 0 0 0 24756 100 0 0 25 0 1 0 1856151956 69455872 16471 4294967295 134512640 135094434 3221224432 3221223104 134556288 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7713/statm): 16957 16471 145 145 0 16812 0
[pid=7713] vsize: 67828
Current children cumulated CPU time (s) 248.57
Current children cumulated vsize (Kb) 69952

[startup+260.017 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 17184 0 0 0 25746 104 0 0 25 0 1 0 1856151956 71540736 16987 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 17466 16987 145 145 0 17321 0
[pid=7713] vsize: 69864
Current children cumulated CPU time (s) 258.51
Current children cumulated vsize (Kb) 71988

[startup+270.017 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 17489 0 0 0 26741 106 0 0 25 0 1 0 1856151956 72773632 17292 4294967295 134512640 135094434 3221224432 3221223104 134555953 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 17767 17292 145 145 0 17622 0
[pid=7713] vsize: 71068
Current children cumulated CPU time (s) 268.48
Current children cumulated vsize (Kb) 73192

[startup+280.018 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 17764 0 0 0 27738 107 0 0 25 0 1 0 1856151956 73900032 17567 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 18042 17567 145 145 0 17897 0
[pid=7713] vsize: 72168
Current children cumulated CPU time (s) 278.46
Current children cumulated vsize (Kb) 74292

[startup+290.02 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 18098 0 0 0 28733 110 0 0 25 0 1 0 1856151956 75239424 17901 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 18369 17901 145 145 0 18224 0
[pid=7713] vsize: 73476
Current children cumulated CPU time (s) 288.44
Current children cumulated vsize (Kb) 75600

[startup+300.02 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 18307 0 0 0 29729 112 0 0 25 0 1 0 1856151956 76087296 18110 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 18576 18110 145 145 0 18431 0
[pid=7713] vsize: 74304
Current children cumulated CPU time (s) 298.42
Current children cumulated vsize (Kb) 76428

[startup+310.02 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 18538 0 0 0 30726 113 0 0 25 0 1 0 1856151956 77021184 18341 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 18804 18341 145 145 0 18659 0
[pid=7713] vsize: 75216
Current children cumulated CPU time (s) 308.4
Current children cumulated vsize (Kb) 77340

[startup+320.02 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 18820 0 0 0 31720 115 0 0 25 0 1 0 1856151956 78151680 18623 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 19080 18623 145 145 0 18935 0
[pid=7713] vsize: 76320
Current children cumulated CPU time (s) 318.36
Current children cumulated vsize (Kb) 78444

[startup+330.021 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 19249 0 0 0 32713 118 0 0 25 0 1 0 1856151956 79892480 19052 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 19505 19052 145 145 0 19360 0
[pid=7713] vsize: 78020
Current children cumulated CPU time (s) 328.32
Current children cumulated vsize (Kb) 80144

[startup+340.022 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 19688 0 0 0 33706 122 0 0 25 0 1 0 1856151956 81698816 19491 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 19946 19491 145 145 0 19801 0
[pid=7713] vsize: 79784
Current children cumulated CPU time (s) 338.29
Current children cumulated vsize (Kb) 81908

[startup+350.022 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 19919 0 0 0 34702 124 0 0 25 0 1 0 1856151956 82640896 19722 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 20176 19722 145 145 0 20031 0
[pid=7713] vsize: 80704
Current children cumulated CPU time (s) 348.27
Current children cumulated vsize (Kb) 82828

[startup+360.023 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 20313 0 0 0 35696 127 0 0 25 0 1 0 1856151956 84226048 20116 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 20563 20116 145 145 0 20418 0
[pid=7713] vsize: 82252
Current children cumulated CPU time (s) 358.24
Current children cumulated vsize (Kb) 84376

[startup+370.023 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 20813 0 0 0 36687 131 0 0 25 0 1 0 1856151956 86249472 20616 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 21057 20616 145 145 0 20912 0
[pid=7713] vsize: 84228
Current children cumulated CPU time (s) 368.19
Current children cumulated vsize (Kb) 86352

[startup+380.024 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 21307 0 0 0 37679 134 0 0 25 0 1 0 1856151956 89305088 21110 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 21803 21110 145 145 0 21658 0
[pid=7713] vsize: 87212
Current children cumulated CPU time (s) 378.14
Current children cumulated vsize (Kb) 89336

[startup+390.026 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 21701 0 0 0 38674 136 0 0 25 0 1 0 1856151956 90898432 21504 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 22192 21504 145 145 0 22047 0
[pid=7713] vsize: 88768
Current children cumulated CPU time (s) 388.11
Current children cumulated vsize (Kb) 90892

[startup+400.026 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 21984 0 0 0 39670 138 0 0 25 0 1 0 1856151956 92045312 21787 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 22472 21787 145 145 0 22327 0
[pid=7713] vsize: 89888
Current children cumulated CPU time (s) 398.09
Current children cumulated vsize (Kb) 92012

[startup+410.027 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 22522 0 0 0 40662 142 0 0 25 0 1 0 1856151956 94212096 22325 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 23001 22325 145 145 0 22856 0
[pid=7713] vsize: 92004
Current children cumulated CPU time (s) 408.05
Current children cumulated vsize (Kb) 94128

[startup+420.027 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 22985 0 0 0 41655 145 0 0 25 0 1 0 1856151956 96096256 22788 4294967295 134512640 135094434 3221224432 3221223136 134559017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 23461 22788 145 145 0 23316 0
[pid=7713] vsize: 93844
Current children cumulated CPU time (s) 418.01
Current children cumulated vsize (Kb) 95968

[startup+430.028 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 23153 0 0 0 42653 146 0 0 25 0 1 0 1856151956 96763904 22956 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 23624 22956 145 145 0 23479 0
[pid=7713] vsize: 94496
Current children cumulated CPU time (s) 428
Current children cumulated vsize (Kb) 96620

[startup+440.029 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 23491 0 0 0 43647 149 0 0 25 0 1 0 1856151956 98115584 23294 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7713/statm): 23954 23294 145 145 0 23809 0
[pid=7713] vsize: 95816
Current children cumulated CPU time (s) 437.97
Current children cumulated vsize (Kb) 97940

[startup+450.029 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 23873 0 0 0 44641 151 0 0 25 0 1 0 1856151956 99639296 23676 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 24326 23676 145 145 0 24181 0
[pid=7713] vsize: 97304
Current children cumulated CPU time (s) 447.93
Current children cumulated vsize (Kb) 99428

[startup+460.03 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 24253 0 0 0 45635 154 0 0 25 0 1 0 1856151956 101167104 24056 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 24699 24056 145 145 0 24554 0
[pid=7713] vsize: 98796
Current children cumulated CPU time (s) 457.9
Current children cumulated vsize (Kb) 100920

[startup+470.03 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 24598 0 0 0 46628 157 0 0 25 0 1 0 1856151956 102555648 24401 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 25038 24401 145 145 0 24893 0
[pid=7713] vsize: 100152
Current children cumulated CPU time (s) 467.86
Current children cumulated vsize (Kb) 102276

[startup+480.031 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 25264 0 0 0 47616 162 0 0 25 0 1 0 1856151956 105250816 25067 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 25696 25067 145 145 0 25551 0
[pid=7713] vsize: 102784
Current children cumulated CPU time (s) 477.79
Current children cumulated vsize (Kb) 104908

[startup+490.032 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 25688 0 0 0 48608 165 0 0 25 0 1 0 1856151956 106962944 25491 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 26114 25491 145 145 0 25969 0
[pid=7713] vsize: 104456
Current children cumulated CPU time (s) 487.74
Current children cumulated vsize (Kb) 106580

[startup+500.032 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 26031 0 0 0 49601 168 0 0 25 0 1 0 1856151956 108355584 25834 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 26454 25834 145 145 0 26309 0
[pid=7713] vsize: 105816
Current children cumulated CPU time (s) 497.7
Current children cumulated vsize (Kb) 107940

[startup+510.033 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 26204 0 0 0 50599 169 0 0 25 0 1 0 1856151956 109051904 26007 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 26624 26007 145 145 0 26479 0
[pid=7713] vsize: 106496
Current children cumulated CPU time (s) 507.69
Current children cumulated vsize (Kb) 108620

[startup+520.033 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 26251 0 0 0 51598 170 0 0 25 0 1 0 1856151956 109240320 26054 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 26670 26054 145 145 0 26525 0
[pid=7713] vsize: 106680
Current children cumulated CPU time (s) 517.69
Current children cumulated vsize (Kb) 108804

[startup+530.034 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 26798 0 0 0 52589 174 0 0 25 0 1 0 1856151956 111452160 26601 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 27210 26601 145 145 0 27065 0
[pid=7713] vsize: 108840
Current children cumulated CPU time (s) 527.64
Current children cumulated vsize (Kb) 110964

[startup+540.035 s]
Raw data (loadavg): 0.99 0.99 0.99 1/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) T 7709 7709 19316 0 -1 0 27527 0 0 0 53575 181 0 0 25 0 1 0 1856151956 114397184 27330 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7713/statm): 27929 27330 145 145 0 27784 0
[pid=7713] vsize: 111716
Current children cumulated CPU time (s) 537.57
Current children cumulated vsize (Kb) 113840

[startup+550.035 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 27997 0 0 0 54566 186 0 0 25 0 1 0 1856151956 116305920 27800 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 28395 27800 145 145 0 28250 0
[pid=7713] vsize: 113580
Current children cumulated CPU time (s) 547.53
Current children cumulated vsize (Kb) 115704

[startup+560.036 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 28417 0 0 0 55556 191 0 0 25 0 1 0 1856151956 118009856 28220 4294967295 134512640 135094434 3221224432 3221223136 134558999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7713/statm): 28811 28220 145 145 0 28666 0
[pid=7713] vsize: 115244
Current children cumulated CPU time (s) 557.48
Current children cumulated vsize (Kb) 117368

[startup+570.038 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 28604 0 0 0 56552 193 0 0 25 0 1 0 1856151956 118759424 28407 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 28994 28407 145 145 0 28849 0
[pid=7713] vsize: 115976
Current children cumulated CPU time (s) 567.46
Current children cumulated vsize (Kb) 118100

[startup+580.039 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 28949 0 0 0 57546 196 0 0 25 0 1 0 1856151956 120143872 28752 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 29332 28752 145 145 0 29187 0
[pid=7713] vsize: 117328
Current children cumulated CPU time (s) 577.43
Current children cumulated vsize (Kb) 119452

[startup+590.041 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 29243 0 0 0 58541 198 0 0 25 0 1 0 1856151956 121335808 29046 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 29623 29046 145 145 0 29478 0
[pid=7713] vsize: 118492
Current children cumulated CPU time (s) 587.4
Current children cumulated vsize (Kb) 120616

[startup+600.041 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 29488 0 0 0 59536 201 0 0 25 0 1 0 1856151956 122327040 29291 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 29865 29291 145 145 0 29720 0
[pid=7713] vsize: 119460
Current children cumulated CPU time (s) 597.38
Current children cumulated vsize (Kb) 121584

[startup+610.041 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 29578 0 0 0 60534 202 0 0 25 0 1 0 1856151956 122695680 29381 4294967295 134512640 135094434 3221224432 3221223092 134553489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 29955 29381 145 145 0 29810 0
[pid=7713] vsize: 119820
Current children cumulated CPU time (s) 607.37
Current children cumulated vsize (Kb) 121944

[startup+620.041 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 29804 0 0 0 61532 203 0 0 25 0 1 0 1856151956 123613184 29607 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 30179 29607 145 145 0 30034 0
[pid=7713] vsize: 120716
Current children cumulated CPU time (s) 617.36
Current children cumulated vsize (Kb) 122840

[startup+630.042 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 30170 0 0 0 62524 207 0 0 25 0 1 0 1856151956 125095936 29973 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 30541 29973 145 145 0 30396 0
[pid=7713] vsize: 122164
Current children cumulated CPU time (s) 627.32
Current children cumulated vsize (Kb) 124288

[startup+640.044 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 30677 0 0 0 63516 210 0 0 25 0 1 0 1856151956 127143936 30480 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 31041 30480 145 145 0 30896 0
[pid=7713] vsize: 124164
Current children cumulated CPU time (s) 637.27
Current children cumulated vsize (Kb) 126288

[startup+650.044 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) T 7709 7709 19316 0 -1 0 31409 0 0 0 64502 216 0 0 25 0 1 0 1856151956 130105344 31212 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7713/statm): 31764 31212 145 145 0 31619 0
[pid=7713] vsize: 127056
Current children cumulated CPU time (s) 647.19
Current children cumulated vsize (Kb) 129180

[startup+660.045 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 31840 0 0 0 65493 220 0 0 25 0 1 0 1856151956 131862528 31643 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 32193 31643 145 145 0 32048 0
[pid=7713] vsize: 128772
Current children cumulated CPU time (s) 657.14
Current children cumulated vsize (Kb) 130896

[startup+670.045 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 32337 0 0 0 66485 224 0 0 25 0 1 0 1856151956 133869568 32140 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 32683 32140 145 145 0 32538 0
[pid=7713] vsize: 130732
Current children cumulated CPU time (s) 667.1
Current children cumulated vsize (Kb) 132856

[startup+680.046 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 32793 0 0 0 67478 227 0 0 25 0 1 0 1856151956 135716864 32596 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 33134 32596 145 145 0 32989 0
[pid=7713] vsize: 132536
Current children cumulated CPU time (s) 677.06
Current children cumulated vsize (Kb) 134660

[startup+690.047 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 33366 0 0 0 68470 230 0 0 25 0 1 0 1856151956 138051584 33169 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 33704 33169 145 145 0 33559 0
[pid=7713] vsize: 134816
Current children cumulated CPU time (s) 687.01
Current children cumulated vsize (Kb) 136940

[startup+700.047 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) T 7709 7709 19316 0 -1 0 33821 0 0 0 69462 234 0 0 25 0 1 0 1856151956 139898880 33624 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7713/statm): 34155 33624 145 145 0 34010 0
[pid=7713] vsize: 136620
Current children cumulated CPU time (s) 696.97
Current children cumulated vsize (Kb) 138744

[startup+710.048 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 34092 0 0 0 70457 236 0 0 25 0 1 0 1856151956 140988416 33895 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 34421 33895 145 145 0 34276 0
[pid=7713] vsize: 137684
Current children cumulated CPU time (s) 706.94
Current children cumulated vsize (Kb) 139808

[startup+720.048 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 34261 0 0 0 71454 238 0 0 25 0 1 0 1856151956 141664256 34064 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 34586 34064 145 145 0 34441 0
[pid=7713] vsize: 138344
Current children cumulated CPU time (s) 716.93
Current children cumulated vsize (Kb) 140468

[startup+730.049 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 34519 0 0 0 72450 239 0 0 25 0 1 0 1856151956 142704640 34322 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 34840 34322 145 145 0 34695 0
[pid=7713] vsize: 139360
Current children cumulated CPU time (s) 726.9
Current children cumulated vsize (Kb) 141484

[startup+740.051 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 34771 0 0 0 73445 241 0 0 25 0 1 0 1856151956 143724544 34574 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 35089 34574 145 145 0 34944 0
[pid=7713] vsize: 140356
Current children cumulated CPU time (s) 736.87
Current children cumulated vsize (Kb) 142480

[startup+750.051 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 35041 0 0 0 74442 242 0 0 25 0 1 0 1856151956 144814080 34844 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 35355 34844 145 145 0 35210 0
[pid=7713] vsize: 141420
Current children cumulated CPU time (s) 746.85
Current children cumulated vsize (Kb) 143544

[startup+760.051 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 35253 0 0 0 75440 243 0 0 25 0 1 0 1856151956 145690624 35056 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 35569 35056 145 145 0 35424 0
[pid=7713] vsize: 142276
Current children cumulated CPU time (s) 756.84
Current children cumulated vsize (Kb) 144400

[startup+770.051 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 35433 0 0 0 76437 244 0 0 25 0 1 0 1856151956 146423808 35236 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 35748 35236 145 145 0 35603 0
[pid=7713] vsize: 142992
Current children cumulated CPU time (s) 766.82
Current children cumulated vsize (Kb) 145116

[startup+780.052 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 35623 0 0 0 77434 245 0 0 25 0 1 0 1856151956 147210240 35426 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 35940 35426 145 145 0 35795 0
[pid=7713] vsize: 143760
Current children cumulated CPU time (s) 776.8
Current children cumulated vsize (Kb) 145884

[startup+790.053 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 35852 0 0 0 78431 246 0 0 25 0 1 0 1856151956 148144128 35655 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 36168 35655 145 145 0 36023 0
[pid=7713] vsize: 144672
Current children cumulated CPU time (s) 786.78
Current children cumulated vsize (Kb) 146796

[startup+800.053 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 36035 0 0 0 79428 247 0 0 25 0 1 0 1856151956 148918272 35838 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 36357 35838 145 145 0 36212 0
[pid=7713] vsize: 145428
Current children cumulated CPU time (s) 796.76
Current children cumulated vsize (Kb) 147552

[startup+810.054 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 36185 0 0 0 80426 248 0 0 25 0 1 0 1856151956 149528576 35988 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 36506 35988 145 145 0 36361 0
[pid=7713] vsize: 146024
Current children cumulated CPU time (s) 806.75
Current children cumulated vsize (Kb) 148148

[startup+820.054 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 36387 0 0 0 81422 250 0 0 25 0 1 0 1856151956 150343680 36190 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 36705 36190 145 145 0 36560 0
[pid=7713] vsize: 146820
Current children cumulated CPU time (s) 816.73
Current children cumulated vsize (Kb) 148944

[startup+830.055 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 36573 0 0 0 82420 251 0 0 25 0 1 0 1856151956 151097344 36376 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 36889 36376 145 145 0 36744 0
[pid=7713] vsize: 147556
Current children cumulated CPU time (s) 826.72
Current children cumulated vsize (Kb) 149680

[startup+840.056 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 36873 0 0 0 83414 253 0 0 25 0 1 0 1856151956 152309760 36676 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 37185 36676 145 145 0 37040 0
[pid=7713] vsize: 148740
Current children cumulated CPU time (s) 836.68
Current children cumulated vsize (Kb) 150864

[startup+850.056 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 37390 0 0 0 84404 257 0 0 25 0 1 0 1856151956 154394624 37193 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 37694 37193 145 145 0 37549 0
[pid=7713] vsize: 150776
Current children cumulated CPU time (s) 846.62
Current children cumulated vsize (Kb) 152900

[startup+860.056 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 37705 0 0 0 85400 258 0 0 25 0 1 0 1856151956 155660288 37508 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38003 37508 145 145 0 37858 0
[pid=7713] vsize: 152012
Current children cumulated CPU time (s) 856.59
Current children cumulated vsize (Kb) 154136

[startup+870.057 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 37944 0 0 0 86396 260 0 0 25 0 1 0 1856151956 156626944 37747 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7713/statm): 38239 37747 145 145 0 38094 0
[pid=7713] vsize: 152956
Current children cumulated CPU time (s) 866.57
Current children cumulated vsize (Kb) 155080

[startup+880.058 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38167 0 0 0 87391 262 0 0 25 0 1 0 1856151956 157532160 37970 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38460 37970 145 145 0 38315 0
[pid=7713] vsize: 153840
Current children cumulated CPU time (s) 876.54
Current children cumulated vsize (Kb) 155964

[startup+890.06 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38427 0 0 0 88388 263 0 0 25 0 1 0 1856151956 158593024 38230 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38719 38230 145 145 0 38574 0
[pid=7713] vsize: 154876
Current children cumulated CPU time (s) 886.52
Current children cumulated vsize (Kb) 157000

[startup+900.06 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 89386 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 896.51
Current children cumulated vsize (Kb) 157416

[startup+910.06 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 90387 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 906.52
Current children cumulated vsize (Kb) 157416

[startup+920.06 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 91387 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 916.52
Current children cumulated vsize (Kb) 157416

[startup+930.061 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 92387 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 926.52
Current children cumulated vsize (Kb) 157416

[startup+940.062 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 93387 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 936.52
Current children cumulated vsize (Kb) 157416

[startup+950.062 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 94388 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 946.53
Current children cumulated vsize (Kb) 157416

[startup+960.063 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 95387 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 956.52
Current children cumulated vsize (Kb) 157416

[startup+970.063 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 96388 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 966.53
Current children cumulated vsize (Kb) 157416

[startup+980.064 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 97388 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 976.53
Current children cumulated vsize (Kb) 157416

[startup+990.065 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 98388 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 986.53
Current children cumulated vsize (Kb) 157416

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 99388 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 996.53
Current children cumulated vsize (Kb) 157416

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 100389 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1006.54
Current children cumulated vsize (Kb) 157416

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 101389 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1016.54
Current children cumulated vsize (Kb) 157416

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 102389 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1026.54
Current children cumulated vsize (Kb) 157416

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 103389 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1036.54
Current children cumulated vsize (Kb) 157416

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 104390 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1046.55
Current children cumulated vsize (Kb) 157416

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 105390 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1056.55
Current children cumulated vsize (Kb) 157416

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 106390 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1066.55
Current children cumulated vsize (Kb) 157416

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 107390 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1076.55
Current children cumulated vsize (Kb) 157416

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 108391 264 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1086.56
Current children cumulated vsize (Kb) 157416

[startup+1100.07 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 109390 265 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1096.56
Current children cumulated vsize (Kb) 157416

[startup+1110.07 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 110390 265 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1106.56
Current children cumulated vsize (Kb) 157416

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 111390 265 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1116.56
Current children cumulated vsize (Kb) 157416

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 112390 265 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1126.56
Current children cumulated vsize (Kb) 157416

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 113390 265 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1136.56
Current children cumulated vsize (Kb) 157416

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 114389 266 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1146.56
Current children cumulated vsize (Kb) 157416

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 115389 267 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1156.57
Current children cumulated vsize (Kb) 157416

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 116389 267 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221222912 134780706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1166.57
Current children cumulated vsize (Kb) 157416

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 117389 268 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1176.58
Current children cumulated vsize (Kb) 157416

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 118389 268 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1186.58
Current children cumulated vsize (Kb) 157416

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 119389 268 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1196.58
Current children cumulated vsize (Kb) 157416

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 120389 268 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1206.58
Current children cumulated vsize (Kb) 157416



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.99 0.99 2/57 7713
Raw data (/proc/7709/stat): 7709 (minisat+_script) S 7708 7709 19316 0 -1 0 289 239 0 0 0 1 0 0 20 0 1 0 1856151952 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7709/statm): 531 226 485 147 0 384 0
[pid=7709] vsize: 2124
Raw data (/proc/7713/stat): 7713 (minisat+_64-bit) R 7709 7709 19316 0 -1 0 38532 0 0 0 120389 268 0 0 25 0 1 0 1856151956 159019008 38335 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7713/statm): 38823 38335 145 145 0 38678 0
[pid=7713] vsize: 155292
Current children cumulated CPU time (s) 1206.58
Current children cumulated vsize (Kb) 157416

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

Child status: 0
Real time (s): 1210.16
CPU time (s): 1206.65
CPU user time (s): 1203.89
CPU system time (s): 2.75758
CPU usage (%): 99.7104
Max. virtual memory (cumulated for all children) (Kb): 157416

Verifier Data

ERROR: no interpretation found !