Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-gesa2.opb
MD5SUM837e3a0cb21dfdb0a0a99b7f963c12dc
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1057564785233
Optimality of the best value was proved NO
Number of terms in the objective function 9432
Biggest coefficient in the objective function 409031671808
Number of bits for the biggest coefficient in the objective function 39
Sum of the numbers in the objective function 179181298104960
Number of bits of the sum of numbers in the objective function 48
Biggest number in a constraint 409031671808
Number of bits of the biggest number in a constraint 39
Biggest sum of numbers in a constraint 179181298104960
Number of bits of the biggest sum of numbers48
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.27
Number of variables13368
Total number of constraints1872
Number of constraints which are clauses48
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints1824
Minimum length of a constraint2
Maximum length of a constraint209

Trace number 6198

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        881736 kB
Buffers:         22924 kB
Cached:         101396 kB
SwapCached:        868 kB
Active:          41972 kB
Inactive:        84980 kB
HighTotal:      131008 kB
HighFree:        27328 kB
LowTotal:       903652 kB
LowFree:        854408 kB
SwapTotal:     2097892 kB
SwapFree:      2096540 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5712 kB
Slab:            20268 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:38:44 (client local time) WITH STATUS 0 IN 1200.06 SECONDS
stats: 3358 7 1200.06 0

Solver Data

c Parsing PB file...
c Converting 1872 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[2051]---> BDD-cost:    2
c ---[2046]---> BDD-cost:    2
c ---[2041]---> BDD-cost:    2
c ---[2036]---> BDD-cost:    2
c ---[2031]---> BDD-cost:    2
c ---[2026]---> BDD-cost:    2
c ---[2021]---> BDD-cost:    2
c ---[2016]---> BDD-cost:    2
c ---[2011]---> BDD-cost:    2
c ---[2006]---> BDD-cost:    2
c ---[2001]---> BDD-cost:    2
c ---[1996]---> BDD-cost:    2
c ---[1991]---> BDD-cost:    2
c ---[1986]---> BDD-cost:    2
c ---[1981]---> BDD-cost:    2
c ---[1976]---> BDD-cost:    2
c ---[1971]---> BDD-cost:    2
c ---[1966]---> BDD-cost:    2
c ---[1961]---> BDD-cost:    2
c ---[1956]---> BDD-cost:    2
c ---[1951]---> BDD-cost:    2
c ---[1946]---> BDD-cost:    2
c ---[1941]---> BDD-cost:    2
c ---[1936]---> BDD-cost:    2
c ---[1931]---> BDD-cost:    7
c ---[1930]---> BDD-cost:    7
c ---[1929]---> BDD-cost:    7
c ---[1928]---> BDD-cost:    7
c ---[1927]---> BDD-cost:    7
c ---[1926]---> BDD-cost:    9
c ---[1925]---> BDD-cost:    8
c ---[1924]---> BDD-cost:    8
c ---[1923]---> BDD-cost:    8
c ---[1922]---> BDD-cost:    8
c ---[1921]---> BDD-cost:    8
c ---[1920]---> BDD-cost:    7
c ---[1919]---> BDD-cost:    8
c ---[1918]---> BDD-cost:    7
c ---[1917]---> BDD-cost:    7
c ---[1916]---> BDD-cost:    7
c ---[1915]---> BDD-cost:    7
c ---[1914]---> BDD-cost:    7
c ---[1913]---> BDD-cost:    9
c ---[1912]---> BDD-cost:    8
c ---[1911]---> BDD-cost:    8
c ---[1910]---> BDD-cost:    8
c ---[1909]---> BDD-cost:    8
c ---[1908]---> BDD-cost:    8
c ---[1907]---> BDD-cost:    7
c ---[1906]---> BDD-cost:    8
c ---[1905]---> BDD-cost:    7
c ---[1904]---> BDD-cost:    7
c ---[1903]---> BDD-cost:    7
c ---[1902]---> BDD-cost:    7
c ---[1901]---> BDD-cost:    7
c ---[1900]---> BDD-cost:    9
c ---[1899]---> BDD-cost:    8
c ---[1898]---> BDD-cost:    8
c ---[1897]---> BDD-cost:    8
c ---[1896]---> BDD-cost:    8
c ---[1895]---> BDD-cost:    8
c ---[1894]---> BDD-cost:    7
c ---[1893]---> BDD-cost:    8
c ---[1892]---> BDD-cost:    7
c ---[1891]---> BDD-cost:    7
c ---[1890]---> BDD-cost:    7
c ---[1889]---> BDD-cost:    7
c ---[1888]---> BDD-cost:    7
c ---[1887]---> BDD-cost:    9
c ---[1886]---> BDD-cost:    8
c ---[1885]---> BDD-cost:    8
c ---[1884]---> BDD-cost:    8
c ---[1883]---> BDD-cost:    8
c ---[1882]---> BDD-cost:    8
c ---[1881]---> BDD-cost:    7
c ---[1880]---> BDD-cost:    8
c ---[1879]---> BDD-cost:    7
c ---[1878]---> BDD-cost:    7
c ---[1877]---> BDD-cost:    7
c ---[1876]---> BDD-cost:    7
c ---[1875]---> BDD-cost:    7
c ---[1874]---> BDD-cost:    9
c ---[1873]---> BDD-cost:    8
c ---[1872]---> BDD-cost:    8
c ---[1871]---> BDD-cost:    8
c ---[1870]---> BDD-cost:    8
c ---[1869]---> BDD-cost:    8
c ---[1868]---> BDD-cost:    7
c ---[1867]---> BDD-cost:    8
c ---[1866]---> BDD-cost:    7
c ---[1865]---> BDD-cost:    7
c ---[1864]---> BDD-cost:    7
c ---[1863]---> BDD-cost:    7
c ---[1862]---> BDD-cost:    7
c ---[1861]---> BDD-cost:    9
c ---[1860]---> BDD-cost:    8
c ---[1859]---> BDD-cost:    8
c ---[1858]---> BDD-cost:    8
c ---[1857]---> BDD-cost:    8
c ---[1856]---> BDD-cost:    8
c ---[1855]---> BDD-cost:    7
c ---[1854]---> BDD-cost:    8
c ---[1853]---> BDD-cost:    7
c ---[1852]---> BDD-cost:    7
c ---[1851]---> BDD-cost:    7
c ---[1850]---> BDD-cost:    7
c ---[1849]---> BDD-cost:    7
c ---[1848]---> BDD-cost:    9
c ---[1847]---> BDD-cost:    8
c ---[1846]---> BDD-cost:    8
c ---[1845]---> BDD-cost:    8
c ---[1844]---> BDD-cost:    8
c ---[1843]---> BDD-cost:    8
c ---[1842]---> BDD-cost:    7
c ---[1841]---> BDD-cost:    8
c ---[1840]---> BDD-cost:    7
c ---[1839]---> BDD-cost:    7
c ---[1838]---> BDD-cost:    7
c ---[1837]---> BDD-cost:    7
c ---[1836]---> BDD-cost:    7
c ---[1835]---> BDD-cost:    9
c ---[1834]---> BDD-cost:    8
c ---[1833]---> BDD-cost:    8
c ---[1832]---> BDD-cost:    8
c ---[1831]---> BDD-cost:    8
c ---[1830]---> BDD-cost:    8
c ---[1829]---> BDD-cost:    7
c ---[1828]---> BDD-cost:    8
c ---[1827]---> BDD-cost:    7
c ---[1826]---> BDD-cost:    7
c ---[1825]---> BDD-cost:    7
c ---[1824]---> BDD-cost:    7
c ---[1823]---> BDD-cost:    7
c ---[1822]---> BDD-cost:    9
c ---[1821]---> BDD-cost:    8
c ---[1820]---> BDD-cost:    8
c ---[1819]---> BDD-cost:    8
c ---[1818]---> BDD-cost:    8
c ---[1817]---> BDD-cost:    8
c ---[1816]---> BDD-cost:    7
c ---[1815]---> BDD-cost:    8
c ---[1814]---> BDD-cost:    7
c ---[1813]---> BDD-cost:    7
c ---[1812]---> BDD-cost:    7
c ---[1811]---> BDD-cost:    7
c ---[1810]---> BDD-cost:    7
c ---[1809]---> BDD-cost:    9
c ---[1808]---> BDD-cost:    8
c ---[1807]---> BDD-cost:    8
c ---[1806]---> BDD-cost:    8
c ---[1805]---> BDD-cost:    8
c ---[1804]---> BDD-cost:    8
c ---[1803]---> BDD-cost:    7
c ---[1802]---> BDD-cost:    8
c ---[1801]---> BDD-cost:    7
c ---[1800]---> BDD-cost:    7
c ---[1799]---> BDD-cost:    7
c ---[1798]---> BDD-cost:    7
c ---[1797]---> BDD-cost:    7
c ---[1796]---> BDD-cost:    9
c ---[1795]---> BDD-cost:    8
c ---[1794]---> BDD-cost:    8
c ---[1793]---> BDD-cost:    8
c ---[1792]---> BDD-cost:    8
c ---[1791]---> BDD-cost:    8
c ---[1790]---> BDD-cost:    7
c ---[1789]---> BDD-cost:    8
c ---[1788]---> BDD-cost:    7
c ---[1787]---> BDD-cost:    7
c ---[1786]---> BDD-cost:    7
c ---[1785]---> BDD-cost:    7
c ---[1784]---> BDD-cost:    7
c ---[1783]---> BDD-cost:    9
c ---[1782]---> BDD-cost:    8
c ---[1781]---> BDD-cost:    8
c ---[1780]---> BDD-cost:    8
c ---[1779]---> BDD-cost:    8
c ---[1778]---> BDD-cost:    8
c ---[1777]---> BDD-cost:    7
c ---[1776]---> BDD-cost:    8
c ---[1775]---> BDD-cost:    7
c ---[1774]---> BDD-cost:    7
c ---[1773]---> BDD-cost:    7
c ---[1772]---> BDD-cost:    7
c ---[1771]---> BDD-cost:    7
c ---[1770]---> BDD-cost:    9
c ---[1769]---> BDD-cost:    8
c ---[1768]---> BDD-cost:    8
c ---[1767]---> BDD-cost:    8
c ---[1766]---> BDD-cost:    8
c ---[1765]---> BDD-cost:    8
c ---[1764]---> BDD-cost:    7
c ---[1763]---> BDD-cost:    8
c ---[1762]---> BDD-cost:    7
c ---[1761]---> BDD-cost:    7
c ---[1760]---> BDD-cost:    7
c ---[1759]---> BDD-cost:    7
c ---[1758]---> BDD-cost:    7
c ---[1757]---> BDD-cost:    9
c ---[1756]---> BDD-cost:    8
c ---[1755]---> BDD-cost:    8
c ---[1754]---> BDD-cost:    8
c ---[1753]---> BDD-cost:    8
c ---[1752]---> BDD-cost:    8
c ---[1751]---> BDD-cost:    7
c ---[1750]---> BDD-cost:    8
c ---[1749]---> BDD-cost:    7
c ---[1748]---> BDD-cost:    7
c ---[1747]---> BDD-cost:    7
c ---[1746]---> BDD-cost:    7
c ---[1745]---> BDD-cost:    7
c ---[1744]---> BDD-cost:    9
c ---[1743]---> BDD-cost:    8
c ---[1742]---> BDD-cost:    8
c ---[1741]---> BDD-cost:    8
c ---[1740]---> BDD-cost:    8
c ---[1739]---> BDD-cost:    8
c ---[1738]---> BDD-cost:    7
c ---[1737]---> BDD-cost:    8
c ---[1736]---> BDD-cost:    7
c ---[1735]---> BDD-cost:    7
c ---[1734]---> BDD-cost:    7
c ---[1733]---> BDD-cost:    7
c ---[1732]---> BDD-cost:    7
c ---[1731]---> BDD-cost:    9
c ---[1730]---> BDD-cost:    8
c ---[1729]---> BDD-cost:    8
c ---[1728]---> BDD-cost:    8
c ---[1727]---> BDD-cost:    8
c ---[1726]---> BDD-cost:    8
c ---[1725]---> BDD-cost:    7
c ---[1724]---> BDD-cost:    8
c ---[1723]---> BDD-cost:    7
c ---[1722]---> BDD-cost:    7
c ---[1721]---> BDD-cost:    7
c ---[1720]---> BDD-cost:    7
c ---[1719]---> BDD-cost:    7
c ---[1718]---> BDD-cost:    9
c ---[1717]---> BDD-cost:    8
c ---[1716]---> BDD-cost:    8
c ---[1715]---> BDD-cost:    8
c ---[1714]---> BDD

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

[startup+10.0043 s]
Raw data (loadavg): 0.93 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 1937 0 0 0 975 9 0 0 25 0 1 0 1855610682 6848512 1555 4294967295 134512640 135094434 3221224432 3221219520 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1672 1555 145 145 0 1527 0
[pid=17334] vsize: 6688
Current children cumulated CPU time (s) 9.84
Current children cumulated vsize (Kb) 8812

[startup+20.005 s]
Raw data (loadavg): 0.94 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 1937 0 0 0 1975 9 0 0 25 0 1 0 1855610682 6848512 1555 4294967295 134512640 135094434 3221224432 3221219264 134677035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1672 1555 145 145 0 1527 0
[pid=17334] vsize: 6688
Current children cumulated CPU time (s) 19.84
Current children cumulated vsize (Kb) 8812

[startup+30.0057 s]
Raw data (loadavg): 0.95 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 1937 0 0 0 2975 9 0 0 25 0 1 0 1855610682 6848512 1555 4294967295 134512640 135094434 3221224432 3221220048 134600215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1672 1555 145 145 0 1527 0
[pid=17334] vsize: 6688
Current children cumulated CPU time (s) 29.84
Current children cumulated vsize (Kb) 8812

[startup+40.0064 s]
Raw data (loadavg): 0.96 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 1937 0 0 0 3975 9 0 0 25 0 1 0 1855610682 6848512 1555 4294967295 134512640 135094434 3221224432 3221219264 134676301 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1672 1555 145 145 0 1527 0
[pid=17334] vsize: 6688
Current children cumulated CPU time (s) 39.84
Current children cumulated vsize (Kb) 8812

[startup+50.007 s]
Raw data (loadavg): 0.96 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 1937 0 0 0 4975 9 0 0 25 0 1 0 1855610682 6848512 1555 4294967295 134512640 135094434 3221224432 3221220112 134677091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1672 1555 145 145 0 1527 0
[pid=17334] vsize: 6688
Current children cumulated CPU time (s) 49.84
Current children cumulated vsize (Kb) 8812

[startup+60.0077 s]
Raw data (loadavg): 0.97 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 1937 0 0 0 5976 9 0 0 25 0 1 0 1855610682 6848512 1555 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1672 1555 145 145 0 1527 0
[pid=17334] vsize: 6688
Current children cumulated CPU time (s) 59.85
Current children cumulated vsize (Kb) 8812

[startup+70.0084 s]
Raw data (loadavg): 0.97 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 1937 0 0 0 6976 9 0 0 25 0 1 0 1855610682 6848512 1555 4294967295 134512640 135094434 3221224432 3221219952 134677078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1672 1555 145 145 0 1527 0
[pid=17334] vsize: 6688
Current children cumulated CPU time (s) 69.85
Current children cumulated vsize (Kb) 8812

[startup+80.0091 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 1937 0 0 0 7976 9 0 0 25 0 1 0 1855610682 6848512 1555 4294967295 134512640 135094434 3221224432 3221221104 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1672 1555 145 145 0 1527 0
[pid=17334] vsize: 6688
Current children cumulated CPU time (s) 79.85
Current children cumulated vsize (Kb) 8812

[startup+90.0098 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 1937 0 0 0 8976 9 0 0 25 0 1 0 1855610682 6848512 1555 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1672 1555 145 145 0 1527 0
[pid=17334] vsize: 6688
Current children cumulated CPU time (s) 89.85
Current children cumulated vsize (Kb) 8812

[startup+100.01 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 1937 0 0 0 9977 9 0 0 25 0 1 0 1855610682 6848512 1555 4294967295 134512640 135094434 3221224432 3221220544 134677147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1672 1555 145 145 0 1527 0
[pid=17334] vsize: 6688
Current children cumulated CPU time (s) 99.86
Current children cumulated vsize (Kb) 8812

[startup+110.011 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 1937 0 0 0 10977 9 0 0 25 0 1 0 1855610682 6848512 1555 4294967295 134512640 135094434 3221224432 3221220848 134677099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1672 1555 145 145 0 1527 0
[pid=17334] vsize: 6688
Current children cumulated CPU time (s) 109.86
Current children cumulated vsize (Kb) 8812

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 1937 0 0 0 11977 9 0 0 25 0 1 0 1855610682 6848512 1555 4294967295 134512640 135094434 3221224432 3221221984 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1672 1555 145 145 0 1527 0
[pid=17334] vsize: 6688
Current children cumulated CPU time (s) 119.86
Current children cumulated vsize (Kb) 8812

[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 1937 0 0 0 12977 10 0 0 25 0 1 0 1855610682 6848512 1555 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1672 1555 145 145 0 1527 0
[pid=17334] vsize: 6688
Current children cumulated CPU time (s) 129.87
Current children cumulated vsize (Kb) 8812

[startup+140.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 1937 0 0 0 13977 10 0 0 25 0 1 0 1855610682 6848512 1555 4294967295 134512640 135094434 3221224432 3221220144 134677035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1672 1555 145 145 0 1527 0
[pid=17334] vsize: 6688
Current children cumulated CPU time (s) 139.87
Current children cumulated vsize (Kb) 8812

[startup+150.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 1937 0 0 0 14978 10 0 0 25 0 1 0 1855610682 6848512 1555 4294967295 134512640 135094434 3221224432 3221221808 134600254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1672 1555 145 145 0 1527 0
[pid=17334] vsize: 6688
Current children cumulated CPU time (s) 149.88
Current children cumulated vsize (Kb) 8812

[startup+160.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2357 0 0 0 15976 11 0 0 25 0 1 0 1855610682 7589888 1727 4294967295 134512640 135094434 3221224432 3221220560 134600162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1727 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 159.87
Current children cumulated vsize (Kb) 9536

[startup+170.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2357 0 0 0 16977 11 0 0 25 0 1 0 1855610682 7589888 1727 4294967295 134512640 135094434 3221224432 3221220752 134600186 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1727 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 169.88
Current children cumulated vsize (Kb) 9536

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2357 0 0 0 17977 11 0 0 25 0 1 0 1855610682 7589888 1727 4294967295 134512640 135094434 3221224432 3221219696 134677284 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1727 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 179.88
Current children cumulated vsize (Kb) 9536

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2357 0 0 0 18977 11 0 0 25 0 1 0 1855610682 7589888 1727 4294967295 134512640 135094434 3221224432 3221219224 134676461 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1727 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 189.88
Current children cumulated vsize (Kb) 9536

[startup+200.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2357 0 0 0 19977 11 0 0 25 0 1 0 1855610682 7589888 1727 4294967295 134512640 135094434 3221224432 3221221104 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1727 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 199.88
Current children cumulated vsize (Kb) 9536

[startup+210.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2357 0 0 0 20978 11 0 0 25 0 1 0 1855610682 7589888 1727 4294967295 134512640 135094434 3221224432 3221220752 134677310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1727 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 209.89
Current children cumulated vsize (Kb) 9536

[startup+220.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2357 0 0 0 21978 11 0 0 25 0 1 0 1855610682 7589888 1727 4294967295 134512640 135094434 3221224432 3221220400 134677330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1727 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 219.89
Current children cumulated vsize (Kb) 9536

[startup+230.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2357 0 0 0 22978 11 0 0 25 0 1 0 1855610682 7589888 1727 4294967295 134512640 135094434 3221224432 3221220048 134677257 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1727 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 229.89
Current children cumulated vsize (Kb) 9536

[startup+240.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2357 0 0 0 23978 11 0 0 25 0 1 0 1855610682 7589888 1727 4294967295 134512640 135094434 3221224432 3221220224 134600904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1727 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 239.89
Current children cumulated vsize (Kb) 9536

[startup+250.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2357 0 0 0 24978 11 0 0 25 0 1 0 1855610682 7589888 1727 4294967295 134512640 135094434 3221224432 3221220144 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1727 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 249.89
Current children cumulated vsize (Kb) 9536

[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2357 0 0 0 25979 11 0 0 25 0 1 0 1855610682 7589888 1727 4294967295 134512640 135094434 3221224432 3221220904 134677149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1727 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 259.9
Current children cumulated vsize (Kb) 9536

[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2357 0 0 0 26979 11 0 0 25 0 1 0 1855610682 7589888 1727 4294967295 134512640 135094434 3221224432 3221221200 134677065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1727 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 269.9
Current children cumulated vsize (Kb) 9536

[startup+280.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2357 0 0 0 27979 11 0 0 25 0 1 0 1855610682 7589888 1727 4294967295 134512640 135094434 3221224432 3221219792 134677021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1727 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 279.9
Current children cumulated vsize (Kb) 9536

[startup+290.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2357 0 0 0 28979 11 0 0 25 0 1 0 1855610682 7589888 1727 4294967295 134512640 135094434 3221224432 3221221456 134600310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1727 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 289.9
Current children cumulated vsize (Kb) 9536

[startup+300.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2357 0 0 0 29980 11 0 0 25 0 1 0 1855610682 7589888 1727 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1727 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 299.91
Current children cumulated vsize (Kb) 9536

[startup+310.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2612 0 0 0 30979 12 0 0 25 0 1 0 1855610682 7589888 1734 4294967295 134512640 135094434 3221224432 3221219344 134677366 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1734 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 309.91
Current children cumulated vsize (Kb) 9536

[startup+320.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2612 0 0 0 31979 12 0 0 25 0 1 0 1855610682 7589888 1734 4294967295 134512640 135094434 3221224432 3221219440 134676301 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1734 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 319.91
Current children cumulated vsize (Kb) 9536

[startup+330.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2612 0 0 0 32979 12 0 0 25 0 1 0 1855610682 7589888 1734 4294967295 134512640 135094434 3221224432 3221220672 134677042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1734 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 329.91
Current children cumulated vsize (Kb) 9536

[startup+340.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2612 0 0 0 33980 12 0 0 25 0 1 0 1855610682 7589888 1734 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1734 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 339.92
Current children cumulated vsize (Kb) 9536

[startup+350.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2612 0 0 0 34980 12 0 0 25 0 1 0 1855610682 7589888 1734 4294967295 134512640 135094434 3221224432 3221219696 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1734 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 349.92
Current children cumulated vsize (Kb) 9536

[startup+360.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2612 0 0 0 35980 12 0 0 25 0 1 0 1855610682 7589888 1734 4294967295 134512640 135094434 3221224432 3221219652 134599876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1734 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 359.92
Current children cumulated vsize (Kb) 9536

[startup+370.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2612 0 0 0 36980 12 0 0 25 0 1 0 1855610682 7589888 1734 4294967295 134512640 135094434 3221224432 3221219580 134677228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1734 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 369.92
Current children cumulated vsize (Kb) 9536

[startup+380.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2612 0 0 0 37980 12 0 0 25 0 1 0 1855610682 7589888 1734 4294967295 134512640 135094434 3221224432 3221220384 134600246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1734 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 379.92
Current children cumulated vsize (Kb) 9536

[startup+390.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2612 0 0 0 38980 13 0 0 25 0 1 0 1855610682 7589888 1734 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1734 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 389.93
Current children cumulated vsize (Kb) 9536

[startup+400.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2612 0 0 0 39980 13 0 0 25 0 1 0 1855610682 7589888 1734 4294967295 134512640 135094434 3221224432 3221220048 134676522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1734 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 399.93
Current children cumulated vsize (Kb) 9536

[startup+410.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2612 0 0 0 40981 13 0 0 25 0 1 0 1855610682 7589888 1734 4294967295 134512640 135094434 3221224432 3221220460 134676460 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1734 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 409.94
Current children cumulated vsize (Kb) 9536

[startup+420.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2612 0 0 0 41981 13 0 0 25 0 1 0 1855610682 7589888 1734 4294967295 134512640 135094434 3221224432 3221220672 134677056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1734 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 419.94
Current children cumulated vsize (Kb) 9536

[startup+430.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2612 0 0 0 42981 13 0 0 25 0 1 0 1855610682 7589888 1734 4294967295 134512640 135094434 3221224432 3221219872 134676519 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1734 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 429.94
Current children cumulated vsize (Kb) 9536

[startup+440.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2612 0 0 0 43981 13 0 0 25 0 1 0 1855610682 7589888 1734 4294967295 134512640 135094434 3221224432 3221220224 134677351 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1734 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 439.94
Current children cumulated vsize (Kb) 9536

[startup+450.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 2612 0 0 0 44981 13 0 0 25 0 1 0 1855610682 7589888 1734 4294967295 134512640 135094434 3221224432 3221221200 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1853 1734 145 145 0 1708 0
[pid=17334] vsize: 7412
Current children cumulated CPU time (s) 449.94
Current children cumulated vsize (Kb) 9536

[startup+460.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 3333 0 0 0 45978 15 0 0 25 0 1 0 1855610682 7491584 1717 4294967295 134512640 135094434 3221224432 3221218992 134676601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1829 1717 145 145 0 1684 0
[pid=17334] vsize: 7316
Current children cumulated CPU time (s) 459.93
Current children cumulated vsize (Kb) 9440

[startup+470.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 3333 0 0 0 46978 15 0 0 25 0 1 0 1855610682 7491584 1717 4294967295 134512640 135094434 3221224432 3221219344 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1829 1717 145 145 0 1684 0
[pid=17334] vsize: 7316
Current children cumulated CPU time (s) 469.93
Current children cumulated vsize (Kb) 9440

[startup+480.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 3333 0 0 0 47978 15 0 0 25 0 1 0 1855610682 7491584 1717 4294967295 134512640 135094434 3221224432 3221219616 134676273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1829 1717 145 145 0 1684 0
[pid=17334] vsize: 7316
Current children cumulated CPU time (s) 479.93
Current children cumulated vsize (Kb) 9440

[startup+490.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 3333 0 0 0 48979 15 0 0 25 0 1 0 1855610682 7491584 1717 4294967295 134512640 135094434 3221224432 3221220368 134676993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1829 1717 145 145 0 1684 0
[pid=17334] vsize: 7316
Current children cumulated CPU time (s) 489.94
Current children cumulated vsize (Kb) 9440

[startup+500.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 3333 0 0 0 49979 15 0 0 25 0 1 0 1855610682 7491584 1717 4294967295 134512640 135094434 3221224432 3221219696 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1829 1717 145 145 0 1684 0
[pid=17334] vsize: 7316
Current children cumulated CPU time (s) 499.94
Current children cumulated vsize (Kb) 9440

[startup+510.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 3333 0 0 0 50979 15 0 0 25 0 1 0 1855610682 7491584 1717 4294967295 134512640 135094434 3221224432 3221219696 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1829 1717 145 145 0 1684 0
[pid=17334] vsize: 7316
Current children cumulated CPU time (s) 509.94
Current children cumulated vsize (Kb) 9440

[startup+520.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 3333 0 0 0 51979 16 0 0 25 0 1 0 1855610682 7491584 1717 4294967295 134512640 135094434 3221224432 3221220812 134676460 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1829 1717 145 145 0 1684 0
[pid=17334] vsize: 7316
Current children cumulated CPU time (s) 519.95
Current children cumulated vsize (Kb) 9440

[startup+530.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 3333 0 0 0 52979 16 0 0 25 0 1 0 1855610682 7491584 1717 4294967295 134512640 135094434 3221224432 3221220928 134677278 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1829 1717 145 145 0 1684 0
[pid=17334] vsize: 7316
Current children cumulated CPU time (s) 529.95
Current children cumulated vsize (Kb) 9440

[startup+540.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 3333 0 0 0 53979 16 0 0 25 0 1 0 1855610682 7491584 1717 4294967295 134512640 135094434 3221224432 3221220224 134676519 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1829 1717 145 145 0 1684 0
[pid=17334] vsize: 7316
Current children cumulated CPU time (s) 539.95
Current children cumulated vsize (Kb) 9440

[startup+550.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 3333 0 0 0 54980 16 0 0 25 0 1 0 1855610682 7491584 1717 4294967295 134512640 135094434 3221224432 3221219520 134676601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1829 1717 145 145 0 1684 0
[pid=17334] vsize: 7316
Current children cumulated CPU time (s) 549.96
Current children cumulated vsize (Kb) 9440

[startup+560.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 3333 0 0 0 55980 16 0 0 25 0 1 0 1855610682 7491584 1717 4294967295 134512640 135094434 3221224432 3221220784 134783376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1829 1717 145 145 0 1684 0
[pid=17334] vsize: 7316
Current children cumulated CPU time (s) 559.96
Current children cumulated vsize (Kb) 9440

[startup+570.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 3333 0 0 0 56980 16 0 0 25 0 1 0 1855610682 7491584 1717 4294967295 134512640 135094434 3221224432 3221220096 134676465 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1829 1717 145 145 0 1684 0
[pid=17334] vsize: 7316
Current children cumulated CPU time (s) 569.96
Current children cumulated vsize (Kb) 9440

[startup+580.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 3333 0 0 0 57980 16 0 0 25 0 1 0 1855610682 7491584 1717 4294967295 134512640 135094434 3221224432 3221220048 134600228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1829 1717 145 145 0 1684 0
[pid=17334] vsize: 7316
Current children cumulated CPU time (s) 579.96
Current children cumulated vsize (Kb) 9440

[startup+590.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 3333 0 0 0 58981 16 0 0 25 0 1 0 1855610682 7491584 1717 4294967295 134512640 135094434 3221224432 3221220472 134677084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1829 1717 145 145 0 1684 0
[pid=17334] vsize: 7316
Current children cumulated CPU time (s) 589.97
Current children cumulated vsize (Kb) 9440

[startup+600.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 3333 0 0 0 59981 16 0 0 25 0 1 0 1855610682 7491584 1717 4294967295 134512640 135094434 3221224432 3221220928 134601181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1829 1717 145 145 0 1684 0
[pid=17334] vsize: 7316
Current children cumulated CPU time (s) 599.97
Current children cumulated vsize (Kb) 9440

[startup+610.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 3333 0 0 0 60981 16 0 0 25 0 1 0 1855610682 7491584 1717 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1829 1717 145 145 0 1684 0
[pid=17334] vsize: 7316
Current children cumulated CPU time (s) 609.97
Current children cumulated vsize (Kb) 9440

[startup+620.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4201 0 0 0 61976 19 0 0 25 0 1 0 1855610682 7598080 1751 4294967295 134512640 135094434 3221224432 3221218960 134676993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1855 1751 145 145 0 1710 0
[pid=17334] vsize: 7420
Current children cumulated CPU time (s) 619.95
Current children cumulated vsize (Kb) 9544

[startup+630.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4201 0 0 0 62976 19 0 0 25 0 1 0 1855610682 7598080 1751 4294967295 134512640 135094434 3221224432 3221219156 134600731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1855 1751 145 145 0 1710 0
[pid=17334] vsize: 7420
Current children cumulated CPU time (s) 629.95
Current children cumulated vsize (Kb) 9544

[startup+640.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4201 0 0 0 63976 19 0 0 25 0 1 0 1855610682 7598080 1751 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1855 1751 145 145 0 1710 0
[pid=17334] vsize: 7420
Current children cumulated CPU time (s) 639.95
Current children cumulated vsize (Kb) 9544

[startup+650.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4201 0 0 0 64976 19 0 0 25 0 1 0 1855610682 7598080 1751 4294967295 134512640 135094434 3221224432 3221219676 134676988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1855 1751 145 145 0 1710 0
[pid=17334] vsize: 7420
Current children cumulated CPU time (s) 649.95
Current children cumulated vsize (Kb) 9544

[startup+660.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4201 0 0 0 65977 19 0 0 25 0 1 0 1855610682 7598080 1751 4294967295 134512640 135094434 3221224432 3221220144 134677021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1855 1751 145 145 0 1710 0
[pid=17334] vsize: 7420
Current children cumulated CPU time (s) 659.96
Current children cumulated vsize (Kb) 9544

[startup+670.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4201 0 0 0 66977 19 0 0 25 0 1 0 1855610682 7598080 1751 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1855 1751 145 145 0 1710 0
[pid=17334] vsize: 7420
Current children cumulated CPU time (s) 669.96
Current children cumulated vsize (Kb) 9544

[startup+680.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4201 0 0 0 67977 19 0 0 25 0 1 0 1855610682 7598080 1751 4294967295 134512640 135094434 3221224432 3221219752 134676609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1855 1751 145 145 0 1710 0
[pid=17334] vsize: 7420
Current children cumulated CPU time (s) 679.96
Current children cumulated vsize (Kb) 9544

[startup+690.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4201 0 0 0 68977 19 0 0 25 0 1 0 1855610682 7598080 1751 4294967295 134512640 135094434 3221224432 3221220648 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1855 1751 145 145 0 1710 0
[pid=17334] vsize: 7420
Current children cumulated CPU time (s) 689.96
Current children cumulated vsize (Kb) 9544

[startup+700.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4201 0 0 0 69978 19 0 0 25 0 1 0 1855610682 7598080 1751 4294967295 134512640 135094434 3221224432 3221220752 134600225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1855 1751 145 145 0 1710 0
[pid=17334] vsize: 7420
Current children cumulated CPU time (s) 699.97
Current children cumulated vsize (Kb) 9544

[startup+710.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4201 0 0 0 70978 20 0 0 25 0 1 0 1855610682 7598080 1751 4294967295 134512640 135094434 3221224432 3221220752 134600354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1855 1751 145 145 0 1710 0
[pid=17334] vsize: 7420
Current children cumulated CPU time (s) 709.98
Current children cumulated vsize (Kb) 9544

[startup+720.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4201 0 0 0 71978 20 0 0 25 0 1 0 1855610682 7598080 1751 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1855 1751 145 145 0 1710 0
[pid=17334] vsize: 7420
Current children cumulated CPU time (s) 719.98
Current children cumulated vsize (Kb) 9544

[startup+730.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4201 0 0 0 72978 20 0 0 25 0 1 0 1855610682 7598080 1751 4294967295 134512640 135094434 3221224432 3221221904 134676259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1855 1751 145 145 0 1710 0
[pid=17334] vsize: 7420
Current children cumulated CPU time (s) 729.98
Current children cumulated vsize (Kb) 9544

[startup+740.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4201 0 0 0 73978 20 0 0 25 0 1 0 1855610682 7598080 1751 4294967295 134512640 135094434 3221224432 3221220208 134600167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1855 1751 145 145 0 1710 0
[pid=17334] vsize: 7420
Current children cumulated CPU time (s) 739.98
Current children cumulated vsize (Kb) 9544

[startup+750.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4201 0 0 0 74979 20 0 0 25 0 1 0 1855610682 7598080 1751 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1855 1751 145 145 0 1710 0
[pid=17334] vsize: 7420
Current children cumulated CPU time (s) 749.99
Current children cumulated vsize (Kb) 9544

[startup+760.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4201 0 0 0 75979 20 0 0 25 0 1 0 1855610682 7598080 1751 4294967295 134512640 135094434 3221224432 3221221696 134676341 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1855 1751 145 145 0 1710 0
[pid=17334] vsize: 7420
Current children cumulated CPU time (s) 759.99
Current children cumulated vsize (Kb) 9544

[startup+770.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4548 0 0 0 76977 21 0 0 25 0 1 0 1855610682 7974912 1754 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1947 1754 145 145 0 1802 0
[pid=17334] vsize: 7788
Current children cumulated CPU time (s) 769.98
Current children cumulated vsize (Kb) 9912

[startup+780.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4548 0 0 0 77977 21 0 0 25 0 1 0 1855610682 7974912 1754 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1947 1754 145 145 0 1802 0
[pid=17334] vsize: 7788
Current children cumulated CPU time (s) 779.98
Current children cumulated vsize (Kb) 9912

[startup+790.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4548 0 0 0 78977 21 0 0 25 0 1 0 1855610682 7974912 1754 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1947 1754 145 145 0 1802 0
[pid=17334] vsize: 7788
Current children cumulated CPU time (s) 789.98
Current children cumulated vsize (Kb) 9912

[startup+800.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4548 0 0 0 79977 21 0 0 25 0 1 0 1855610682 7974912 1754 4294967295 134512640 135094434 3221224432 3221219244 134676331 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1947 1754 145 145 0 1802 0
[pid=17334] vsize: 7788
Current children cumulated CPU time (s) 799.98
Current children cumulated vsize (Kb) 9912

[startup+810.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4548 0 0 0 80978 21 0 0 25 0 1 0 1855610682 7974912 1754 4294967295 134512640 135094434 3221224432 3221221024 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1947 1754 145 145 0 1802 0
[pid=17334] vsize: 7788
Current children cumulated CPU time (s) 809.99
Current children cumulated vsize (Kb) 9912

[startup+820.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4548 0 0 0 81978 21 0 0 25 0 1 0 1855610682 7974912 1754 4294967295 134512640 135094434 3221224432 3221220752 134677346 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1947 1754 145 145 0 1802 0
[pid=17334] vsize: 7788
Current children cumulated CPU time (s) 819.99
Current children cumulated vsize (Kb) 9912

[startup+830.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4548 0 0 0 82978 21 0 0 25 0 1 0 1855610682 7974912 1754 4294967295 134512640 135094434 3221224432 3221220192 134676993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1947 1754 145 145 0 1802 0
[pid=17334] vsize: 7788
Current children cumulated CPU time (s) 829.99
Current children cumulated vsize (Kb) 9912

[startup+840.052 s]
Raw data (loadavg): 1.07 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4548 0 0 0 83978 21 0 0 25 0 1 0 1855610682 7974912 1754 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1947 1754 145 145 0 1802 0
[pid=17334] vsize: 7788
Current children cumulated CPU time (s) 839.99
Current children cumulated vsize (Kb) 9912

[startup+850.053 s]
Raw data (loadavg): 1.06 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4548 0 0 0 84978 21 0 0 25 0 1 0 1855610682 7974912 1754 4294967295 134512640 135094434 3221224432 3221220400 134600274 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1947 1754 145 145 0 1802 0
[pid=17334] vsize: 7788
Current children cumulated CPU time (s) 849.99
Current children cumulated vsize (Kb) 9912

[startup+860.053 s]
Raw data (loadavg): 1.05 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4548 0 0 0 85979 22 0 0 25 0 1 0 1855610682 7974912 1754 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1947 1754 145 145 0 1802 0
[pid=17334] vsize: 7788
Current children cumulated CPU time (s) 860.01
Current children cumulated vsize (Kb) 9912

[startup+870.054 s]
Raw data (loadavg): 1.04 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4548 0 0 0 86979 22 0 0 25 0 1 0 1855610682 7974912 1754 4294967295 134512640 135094434 3221224432 3221220576 134677346 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1947 1754 145 145 0 1802 0
[pid=17334] vsize: 7788
Current children cumulated CPU time (s) 870.01
Current children cumulated vsize (Kb) 9912

[startup+880.055 s]
Raw data (loadavg): 1.03 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4548 0 0 0 87979 22 0 0 25 0 1 0 1855610682 7974912 1754 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1947 1754 145 145 0 1802 0
[pid=17334] vsize: 7788
Current children cumulated CPU time (s) 880.01
Current children cumulated vsize (Kb) 9912

[startup+890.056 s]
Raw data (loadavg): 1.03 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4548 0 0 0 88979 22 0 0 25 0 1 0 1855610682 7974912 1754 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1947 1754 145 145 0 1802 0
[pid=17334] vsize: 7788
Current children cumulated CPU time (s) 890.01
Current children cumulated vsize (Kb) 9912

[startup+900.055 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4548 0 0 0 89979 22 0 0 25 0 1 0 1855610682 7974912 1754 4294967295 134512640 135094434 3221224432 3221221104 134677327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1947 1754 145 145 0 1802 0
[pid=17334] vsize: 7788
Current children cumulated CPU time (s) 900.01
Current children cumulated vsize (Kb) 9912

[startup+910.057 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 4548 0 0 0 90980 22 0 0 25 0 1 0 1855610682 7974912 1754 4294967295 134512640 135094434 3221224432 3221219520 134677271 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1947 1754 145 145 0 1802 0
[pid=17334] vsize: 7788
Current children cumulated CPU time (s) 910.02
Current children cumulated vsize (Kb) 9912

[startup+920.058 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 5464 0 0 0 91974 25 0 0 25 0 1 0 1855610682 7888896 1740 4294967295 134512640 135094434 3221224432 3221219696 134600254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1926 1740 145 145 0 1781 0
[pid=17334] vsize: 7704
Current children cumulated CPU time (s) 919.99
Current children cumulated vsize (Kb) 9828

[startup+930.058 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 5464 0 0 0 92975 25 0 0 25 0 1 0 1855610682 7888896 1740 4294967295 134512640 135094434 3221224432 3221219664 134676245 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1926 1740 145 145 0 1781 0
[pid=17334] vsize: 7704
Current children cumulated CPU time (s) 930
Current children cumulated vsize (Kb) 9828

[startup+940.059 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 5464 0 0 0 93975 25 0 0 25 0 1 0 1855610682 7888896 1740 4294967295 134512640 135094434 3221224432 3221220224 134676589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1926 1740 145 145 0 1781 0
[pid=17334] vsize: 7704
Current children cumulated CPU time (s) 940
Current children cumulated vsize (Kb) 9828

[startup+950.06 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 5464 0 0 0 94975 25 0 0 25 0 1 0 1855610682 7888896 1740 4294967295 134512640 135094434 3221224432 3221219792 134677138 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1926 1740 145 145 0 1781 0
[pid=17334] vsize: 7704
Current children cumulated CPU time (s) 950
Current children cumulated vsize (Kb) 9828

[startup+960.06 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 5464 0 0 0 95975 25 0 0 25 0 1 0 1855610682 7888896 1740 4294967295 134512640 135094434 3221224432 3221218992 134676589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1926 1740 145 145 0 1781 0
[pid=17334] vsize: 7704
Current children cumulated CPU time (s) 960
Current children cumulated vsize (Kb) 9828

[startup+970.061 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 5464 0 0 0 96975 25 0 0 25 0 1 0 1855610682 7888896 1740 4294967295 134512640 135094434 3221224432 3221219696 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1926 1740 145 145 0 1781 0
[pid=17334] vsize: 7704
Current children cumulated CPU time (s) 970
Current children cumulated vsize (Kb) 9828

[startup+980.062 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 5464 0 0 0 97976 25 0 0 25 0 1 0 1855610682 7888896 1740 4294967295 134512640 135094434 3221224432 3221220112 134677086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1926 1740 145 145 0 1781 0
[pid=17334] vsize: 7704
Current children cumulated CPU time (s) 980.01
Current children cumulated vsize (Kb) 9828

[startup+990.062 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 5464 0 0 0 98976 25 0 0 25 0 1 0 1855610682 7888896 1740 4294967295 134512640 135094434 3221224432 3221220400 134600151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1926 1740 145 145 0 1781 0
[pid=17334] vsize: 7704
Current children cumulated CPU time (s) 990.01
Current children cumulated vsize (Kb) 9828

[startup+1000.06 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 5464 0 0 0 99976 25 0 0 25 0 1 0 1855610682 7888896 1740 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1926 1740 145 145 0 1781 0
[pid=17334] vsize: 7704
Current children cumulated CPU time (s) 1000.01
Current children cumulated vsize (Kb) 9828

[startup+1010.06 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 5464 0 0 0 100976 25 0 0 25 0 1 0 1855610682 7888896 1740 4294967295 134512640 135094434 3221224432 3221219404 134677228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1926 1740 145 145 0 1781 0
[pid=17334] vsize: 7704
Current children cumulated CPU time (s) 1010.01
Current children cumulated vsize (Kb) 9828

[startup+1020.06 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 5464 0 0 0 101976 25 0 0 25 0 1 0 1855610682 7888896 1740 4294967295 134512640 135094434 3221224432 3221220048 134600228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1926 1740 145 145 0 1781 0
[pid=17334] vsize: 7704
Current children cumulated CPU time (s) 1020.01
Current children cumulated vsize (Kb) 9828

[startup+1030.06 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 5464 0 0 0 102976 25 0 0 25 0 1 0 1855610682 7888896 1740 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1926 1740 145 145 0 1781 0
[pid=17334] vsize: 7704
Current children cumulated CPU time (s) 1030.01
Current children cumulated vsize (Kb) 9828

[startup+1040.06 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 5464 0 0 0 103976 25 0 0 25 0 1 0 1855610682 7888896 1740 4294967295 134512640 135094434 3221224432 3221220196 134676380 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1926 1740 145 145 0 1781 0
[pid=17334] vsize: 7704
Current children cumulated CPU time (s) 1040.01
Current children cumulated vsize (Kb) 9828

[startup+1050.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 5464 0 0 0 104977 25 0 0 25 0 1 0 1855610682 7888896 1740 4294967295 134512640 135094434 3221224432 3221219872 134600186 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1926 1740 145 145 0 1781 0
[pid=17334] vsize: 7704
Current children cumulated CPU time (s) 1050.02
Current children cumulated vsize (Kb) 9828

[startup+1060.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 5464 0 0 0 105977 25 0 0 25 0 1 0 1855610682 7888896 1740 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1926 1740 145 145 0 1781 0
[pid=17334] vsize: 7704
Current children cumulated CPU time (s) 1060.02
Current children cumulated vsize (Kb) 9828

[startup+1070.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 6285 0 0 0 106974 28 0 0 25 0 1 0 1855610682 7938048 1759 4294967295 134512640 135094434 3221224432 3221219696 134677354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1938 1759 145 145 0 1793 0
[pid=17334] vsize: 7752
Current children cumulated CPU time (s) 1070.02
Current children cumulated vsize (Kb) 9876

[startup+1080.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 6285 0 0 0 107974 28 0 0 25 0 1 0 1855610682 7938048 1759 4294967295 134512640 135094434 3221224432 3221219768 134677084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1938 1759 145 145 0 1793 0
[pid=17334] vsize: 7752
Current children cumulated CPU time (s) 1080.02
Current children cumulated vsize (Kb) 9876

[startup+1090.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 6285 0 0 0 108974 28 0 0 25 0 1 0 1855610682 7938048 1759 4294967295 134512640 135094434 3221224432 3221219940 134677085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1938 1759 145 145 0 1793 0
[pid=17334] vsize: 7752
Current children cumulated CPU time (s) 1090.02
Current children cumulated vsize (Kb) 9876

[startup+1100.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 6285 0 0 0 109974 28 0 0 25 0 1 0 1855610682 7938048 1759 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1938 1759 145 145 0 1793 0
[pid=17334] vsize: 7752
Current children cumulated CPU time (s) 1100.02
Current children cumulated vsize (Kb) 9876

[startup+1110.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 6285 0 0 0 110974 28 0 0 25 0 1 0 1855610682 7938048 1759 4294967295 134512640 135094434 3221224432 3221220576 134600310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1938 1759 145 145 0 1793 0
[pid=17334] vsize: 7752
Current children cumulated CPU time (s) 1110.02
Current children cumulated vsize (Kb) 9876

[startup+1120.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 6285 0 0 0 111974 28 0 0 25 0 1 0 1855610682 7938048 1759 4294967295 134512640 135094434 3221224432 3221220460 134676460 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1938 1759 145 145 0 1793 0
[pid=17334] vsize: 7752
Current children cumulated CPU time (s) 1120.02
Current children cumulated vsize (Kb) 9876

[startup+1130.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 6285 0 0 0 112975 28 0 0 25 0 1 0 1855610682 7938048 1759 4294967295 134512640 135094434 3221224432 3221219944 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1938 1759 145 145 0 1793 0
[pid=17334] vsize: 7752
Current children cumulated CPU time (s) 1130.03
Current children cumulated vsize (Kb) 9876

[startup+1140.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 6285 0 0 0 113975 28 0 0 25 0 1 0 1855610682 7938048 1759 4294967295 134512640 135094434 3221224432 3221220672 134677028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1938 1759 145 145 0 1793 0
[pid=17334] vsize: 7752
Current children cumulated CPU time (s) 1140.03
Current children cumulated vsize (Kb) 9876

[startup+1150.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 6285 0 0 0 114975 28 0 0 25 0 1 0 1855610682 7938048 1759 4294967295 134512640 135094434 3221224432 3221219440 134677065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1938 1759 145 145 0 1793 0
[pid=17334] vsize: 7752
Current children cumulated CPU time (s) 1150.03
Current children cumulated vsize (Kb) 9876

[startup+1160.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 6285 0 0 0 115975 28 0 0 25 0 1 0 1855610682 7938048 1759 4294967295 134512640 135094434 3221224432 3221219696 134677257 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1938 1759 145 145 0 1793 0
[pid=17334] vsize: 7752
Current children cumulated CPU time (s) 1160.03
Current children cumulated vsize (Kb) 9876

[startup+1170.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 6285 0 0 0 116975 28 0 0 25 0 1 0 1855610682 7938048 1759 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1938 1759 145 145 0 1793 0
[pid=17334] vsize: 7752
Current children cumulated CPU time (s) 1170.03
Current children cumulated vsize (Kb) 9876

[startup+1180.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 6285 0 0 0 117975 28 0 0 25 0 1 0 1855610682 7938048 1759 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1938 1759 145 145 0 1793 0
[pid=17334] vsize: 7752
Current children cumulated CPU time (s) 1180.03
Current children cumulated vsize (Kb) 9876

[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 6285 0 0 0 118976 28 0 0 25 0 1 0 1855610682 7938048 1759 4294967295 134512640 135094434 3221224432 3221219696 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1938 1759 145 145 0 1793 0
[pid=17334] vsize: 7752
Current children cumulated CPU time (s) 1190.04
Current children cumulated vsize (Kb) 9876

[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 6285 0 0 0 119976 28 0 0 25 0 1 0 1855610682 7938048 1759 4294967295 134512640 135094434 3221224432 3221220928 134600307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1938 1759 145 145 0 1793 0
[pid=17334] vsize: 7752
Current children cumulated CPU time (s) 1200.04
Current children cumulated vsize (Kb) 9876



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 17334
Raw data (/proc/17330/stat): 17330 (minisat+_script) S 17329 17330 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855610677 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/17330/statm): 531 226 485 147 0 384 0
[pid=17330] vsize: 2124
Raw data (/proc/17334/stat): 17334 (minisat+_64-bit) R 17330 17330 16528 0 -1 0 6285 0 0 0 119976 28 0 0 25 0 1 0 1855610682 7938048 1759 4294967295 134512640 135094434 3221224432 3221221104 134677333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/17334/statm): 1938 1759 145 145 0 1793 0
[pid=17334] vsize: 7752
Current children cumulated CPU time (s) 1200.04
Current children cumulated vsize (Kb) 9876

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

Child status: 0
Real time (s): 1200.08
CPU time (s): 1200.06
CPU user time (s): 1199.76
CPU system time (s): 0.292955
CPU usage (%): 99.9979
Max. virtual memory (cumulated for all children) (Kb): 9912

Verifier Data

ERROR: no interpretation found !