Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-gesa2.opb
MD5SUM2494c95ada0b8f878d2a63b66980e2c5
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 13488
Biggest coefficient in the objective function 418848431931392
Number of bits for the biggest coefficient in the objective function 49
Sum of the numbers in the objective function 180205740755072640
Number of bits of the sum of numbers in the objective function 58
Biggest number in a constraint 418848431931392
Number of bits of the biggest number in a constraint 49
Biggest sum of numbers in a constraint 180205740755072640
Number of bits of the biggest sum of numbers58
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables19344
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 constraint309

Trace number 4513

Launcher Data

LAUNCH ON wulflinc20 THE 2005-09-19 17:47:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2974 boxname=wulflinc20 idbench=630 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  2494c95ada0b8f878d2a63b66980e2c5  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-gesa2.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-gesa2.opb
IDLAUNCH: 2974
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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:        875444 kB
Buffers:         40540 kB
Cached:          87352 kB
SwapCached:        832 kB
Active:          73652 kB
Inactive:        56928 kB
HighTotal:      131008 kB
HighFree:        40320 kB
LowTotal:       903652 kB
LowFree:        835124 kB
SwapTotal:     2097892 kB
SwapFree:      2096604 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5736 kB
Slab:            22964 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 18:08:00 (client local time) WITH STATUS 0 IN 1209.85 SECONDS
stats: 2974 7 1209.85 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 1228] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
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:   10
c ---[1930]---> BDD-cost:   10
c ---[1929]---> BDD-cost:   10
c ---[1928]---> BDD-cost:   10
c ---[1927]---> BDD-cost:   10
c ---[1926]---> BDD-cost:   12
c ---[1925]---> BDD-cost:   11
c ---[1924]---> BDD-cost:   11
c ---[1923]---> BDD-cost:   11
c ---[1922]---> BDD-cost:   11
c ---[1921]---> BDD-cost:   11
c ---[1920]---> BDD-cost:   10
c ---[1919]---> BDD-cost:   11
c ---[1918]---> BDD-cost:   10
c ---[1917]---> BDD-cost:   10
c ---[1916]---> BDD-cost:   10
c ---[1915]---> BDD-cost:   10
c ---[1914]---> BDD-cost:   10
c ---[1913]---> BDD-cost:   12
c ---[1912]---> BDD-cost:   11
c ---[1911]---> BDD-cost:   11
c ---[1910]---> BDD-cost:   11
c ---[1909]---> BDD-cost:   11
c ---[1908]---> BDD-cost:   11
c ---[1907]---> BDD-cost:   10
c ---[1906]---> BDD-cost:   11
c ---[1905]---> BDD-cost:   10
c ---[1904]---> BDD-cost:   10
c ---[1903]---> BDD-cost:   10
c ---[1902]---> BDD-cost:   10
c ---[1901]---> BDD-cost:   10
c ---[1900]---> BDD-cost:   12
c ---[1899]---> BDD-cost:   11
c ---[1898]---> BDD-cost:   11
c ---[1897]---> BDD-cost:   11
c ---[1896]---> BDD-cost:   11
c ---[1895]---> BDD-cost:   11
c ---[1894]---> BDD-cost:   10
c ---[1893]---> BDD-cost:   11
c ---[1892]---> BDD-cost:   10
c ---[1891]---> BDD-cost:   10
c ---[1890]---> BDD-cost:   10
c ---[1889]---> BDD-cost:   10
c ---[1888]---> BDD-cost:   10
c ---[1887]---> BDD-cost:   12
c ---[1886]---> BDD-cost:   11
c ---[1885]---> BDD-cost:   11
c ---[1884]---> BDD-cost:   11
c ---[1883]---> BDD-cost:   11
c ---[1882]---> BDD-cost:   11
c ---[1881]---> BDD-cost:   10
c ---[1880]---> BDD-cost:   11
c ---[1879]---> BDD-cost:   10
c ---[1878]---> BDD-cost:   10
c ---[1877]---> BDD-cost:   10
c ---[1876]---> BDD-cost:   10
c ---[1875]---> BDD-cost:   10
c ---[1874]---> BDD-cost:   12
c ---[1873]---> BDD-cost:   11
c ---[1872]---> BDD-cost:   11
c ---[1871]---> BDD-cost:   11
c ---[1870]---> BDD-cost:   11
c ---[1869]---> BDD-cost:   11
c ---[1868]---> BDD-cost:   10
c ---[1867]---> BDD-cost:   11
c ---[1866]---> BDD-cost:   10
c ---[1865]---> BDD-cost:   10
c ---[1864]---> BDD-cost:   10
c ---[1863]---> BDD-cost:   10
c ---[1862]---> BDD-cost:   10
c ---[1861]---> BDD-cost:   12
c ---[1860]---> BDD-cost:   11
c ---[1859]---> BDD-cost:   11
c ---[1858]---> BDD-cost:   11
c ---[1857]---> BDD-cost:   11
c ---[1856]---> BDD-cost:   11
c ---[1855]---> BDD-cost:   10
c ---[1854]---> BDD-cost:   11
c ---[1853]---> BDD-cost:   10
c ---[1852]---> BDD-cost:   10
c ---[1851]---> BDD-cost:   10
c ---[1850]---> BDD-cost:   10
c ---[1849]---> BDD-cost:   10
c ---[1848]---> BDD-cost:   12
c ---[1847]---> BDD-cost:   11
c ---[1846]---> BDD-cost:   11
c ---[1845]---> BDD-cost:   11
c ---[1844]---> BDD-cost:   11
c ---[1843]---> BDD-cost:   11
c ---[1842]---> BDD-cost:   10
c ---[1841]---> BDD-cost:   11
c ---[1840]---> BDD-cost:   10
c ---[1839]---> BDD-cost:   10
c ---[1838]---> BDD-cost:   10
c ---[1837]---> BDD-cost:   10
c ---[1836]---> BDD-cost:   10
c ---[1835]---> BDD-cost:   12
c ---[1834]---> BDD-cost:   11
c ---[1833]---> BDD-cost:   11
c ---[1832]---> BDD-cost:   11
c ---[1831]---> BDD-cost:   11
c ---[1830]---> BDD-cost:   11
c ---[1829]---> BDD-cost:   10
c ---[1828]---> BDD-cost:   11
c ---[1827]---> BDD-cost:   10
c ---[1826]---> BDD-cost:   10
c ---[1825]---> BDD-cost:   10
c ---[1824]---> BDD-cost:   10
c ---[1823]---> BDD-cost:   10
c ---[1822]---> BDD-cost:   12
c ---[1821]---> BDD-cost:   11
c ---[1820]---> BDD-cost:   11
c ---[1819]---> BDD-cost:   11
c ---[1818]---> BDD-cost:   11
c ---[1817]---> BDD-cost:   11
c ---[1816]---> BDD-cost:   10
c ---[1815]---> BDD-cost:   11
c ---[1814]---> BDD-cost:   10
c ---[1813]---> BDD-cost:   10
c ---[1812]---> BDD-cost:   10
c ---[1811]---> BDD-cost:   10
c ---[1810]---> BDD-cost:   10
c ---[1809]---> BDD-cost:   12
c ---[1808]---> BDD-cost:   11
c ---[1807]---> BDD-cost:   11
c ---[1806]---> BDD-cost:   11
c ---[1805]---> BDD-cost:   11
c ---[1804]---> BDD-cost:   11
c ---[1803]---> BDD-cost:   10
c ---[1802]---> BDD-cost:   11
c ---[1801]---> BDD-cost:   10
c ---[1800]---> BDD-cost:   10
c ---[1799]---> BDD-cost:   10
c ---[1798]---> BDD-cost:   10
c ---[1797]---> BDD-cost:   10
c ---[1796]---> BDD-cost:   12
c ---[1795]---> BDD-cost:   11
c ---[1794]---> BDD-cost:   11
c ---[1793]---> BDD-cost:   11
c ---[1792]---> BDD-cost:   11
c ---[1791]---> BDD-cost:   11
c ---[1790]---> BDD-cost:   10
c ---[1789]---> BDD-cost:   11
c ---[1788]---> BDD-cost:   10
c ---[1787]---> BDD-cost:   10
c ---[1786]---> BDD-cost:   10
c ---[1785]---> BDD-cost:   10
c ---[1784]---> BDD-cost:   10
c ---[1783]---> BDD-cost:   12
c ---[1782]---> BDD-cost:   11
c ---[1781]---> BDD-cost:   11
c ---[1780]---> BDD-cost:   11
c ---[1779]---> BDD-cost:   11
c ---[1778]---> BDD-cost:   11
c ---[1777]---> BDD-cost:   10
c ---[1776]---> BDD-cost:   11
c ---[1775]---> BDD-cost:   10
c ---[1774]---> BDD-cost:   10
c ---[1773]---> BDD-cost:   10
c ---[1772]---> BDD-cost:   10
c ---[1771]---> BDD-cost:   10
c ---[1770]---> BDD-cost:   12
c ---[1769]---> BDD-cost:   11
c ---[1768]---> BDD-cost:   11
c ---[1767]---> BDD-cost:   11
c ---[1766]---> BDD-cost:   11
c ---[1765]---> BDD-cost:   11
c ---[1764]---> BDD-cost:   10
c ---[1763]---> BDD-cost:   11
c ---[1762]---> BDD-cost:   10
c ---[1761]---> BDD-cost:   10
c ---[1760]---> BDD-cost:   10
c ---[1759]---> BDD-cost:   10
c ---[1758]---> BDD-cost:   10
c ---[1757]---> BDD-cost:   12
c ---[1756]---> BDD-cost:   11
c ---[1755]---> BDD-cost:   11
c ---[1754]---> BDD-cost:   11
c ---[1753]---> BDD-cost:   11
c ---[1752]---> BDD-cost:   11
c ---[1751]---> BDD-cost:   10
c ---[1750]---> BDD-cost:   11
c ---[1749]---> BDD-cost:   10
c ---[1748]---> BDD-cost:   10
c ---[1747]---> BDD-cost:   10
c ---[1746]---> BDD-cost:   10
c ---[1745]---> BDD-cost:   10
c ---[1744]---> BDD-cost:   12
c ---[1743]---> BDD-cost:   11
c ---[1742]---> BDD-cost:   11
c ---[1741]---> BDD-cost:   11
c ---[1740]---> BDD-cost:   11
c ---[1739]---> BDD-cost:   11
c ---[1738]---> BDD-cost:   10
c ---[1737]---> BDD-cost:   11
c ---[1736]---> BDD-cost:   10
c ---[1735]---> BDD-cost:   10
c ---[1734]---> BDD-cost:   10
c ---[1733]---> BDD-cost:   10
c ---[1732]---> BDD-cost:   10
c ---[1731]---> BDD-cost:   12
c ---[1730]---> BDD-cost:   11
c ---[1729]---> BDD-cost:   11
c ---[1728]---> BDD-cost:   11
c ---[1727]---> BDD-cost:   11
c ---[1726]---> BDD-cost:   11
c ---[1725]---> BDD-cost:   10
c ---[1724]---> BDD-cost:   11
c ---[1723]---> BDD-cost:   10
c ---[1722]---> BDD-cost:   10
c ---[1721]---> BDD-cost:   10
c ---[1720]---> BDD-cost:   10
c ---[1719]---> BDD-cost:   10
c ---[1718]---> BDD-cost:   12
c ---[1717]---> BDD-cost:   11
c ---[1716]---> BDD-cost:   11
c ---[1715]---> BDD-cost:   11
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/22709/stat): 22709 (minisat+_script) R 22708 22709 2660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1851813797 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/22709/statm): 174 3 169 147 0 27 0
[pid=22709] 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=22710
New process pid=22711
New process pid=22712
execve syscall for /bin/sed executable
One traced child (pid=22711) 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=22712) exited with status: 0
One traced child (pid=22710) exited with status: 0
New process pid=22713
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-gesa2.opb
One traced child (pid=22713) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=22714
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-gesa2.opb

[startup+10.0034 s]
Raw data (loadavg): 0.90 0.95 0.73 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 937 18 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221218576 134696194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 9.57
Current children cumulated vsize (Kb) 15048

[startup+20.0041 s]
Raw data (loadavg): 0.92 0.96 0.73 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 1937 18 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221218736 134844731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 19.57
Current children cumulated vsize (Kb) 15048

[startup+30.0048 s]
Raw data (loadavg): 0.93 0.96 0.73 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 2938 18 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221218648 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 29.58
Current children cumulated vsize (Kb) 15048

[startup+40.0055 s]
Raw data (loadavg): 0.94 0.96 0.74 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 3938 18 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219500 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 39.58
Current children cumulated vsize (Kb) 15048

[startup+50.0072 s]
Raw data (loadavg): 0.95 0.96 0.74 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 4938 18 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219024 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 49.58
Current children cumulated vsize (Kb) 15048

[startup+60.0079 s]
Raw data (loadavg): 0.95 0.96 0.74 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 5938 18 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219348 134849060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 59.58
Current children cumulated vsize (Kb) 15048

[startup+70.0086 s]
Raw data (loadavg): 0.96 0.96 0.74 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 6938 18 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219104 134696239 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 69.58
Current children cumulated vsize (Kb) 15048

[startup+80.0094 s]
Raw data (loadavg): 0.97 0.96 0.74 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 7939 18 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221218832 134629069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 79.59
Current children cumulated vsize (Kb) 15048

[startup+90.0101 s]
Raw data (loadavg): 0.97 0.96 0.75 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 8939 18 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219528 134693553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 89.59
Current children cumulated vsize (Kb) 15048

[startup+100.01 s]
Raw data (loadavg): 0.98 0.96 0.75 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 9939 18 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219628 134723285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 99.59
Current children cumulated vsize (Kb) 15048

[startup+110.011 s]
Raw data (loadavg): 0.98 0.96 0.75 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 10939 18 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221218620 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 109.59
Current children cumulated vsize (Kb) 15048

[startup+120.011 s]
Raw data (loadavg): 0.98 0.97 0.75 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 11939 18 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219008 134630875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 119.59
Current children cumulated vsize (Kb) 15048

[startup+130.012 s]
Raw data (loadavg): 0.98 0.97 0.75 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 12939 19 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219808 134723288 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 129.6
Current children cumulated vsize (Kb) 15048

[startup+140.013 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 13940 19 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221218804 134849086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 139.61
Current children cumulated vsize (Kb) 15048

[startup+150.013 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 14940 19 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219088 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 149.61
Current children cumulated vsize (Kb) 15048

[startup+160.014 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 15939 20 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219668 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 159.61
Current children cumulated vsize (Kb) 15048

[startup+170.015 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 16939 20 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219504 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 169.61
Current children cumulated vsize (Kb) 15048

[startup+180.016 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 17939 21 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219484 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 179.62
Current children cumulated vsize (Kb) 15048

[startup+190.016 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 18939 21 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220208 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 189.62
Current children cumulated vsize (Kb) 15048

[startup+200.016 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 19939 21 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219504 134694539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 199.62
Current children cumulated vsize (Kb) 15048

[startup+210.017 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 20939 21 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220064 134631207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 209.62
Current children cumulated vsize (Kb) 15048

[startup+220.018 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 21939 21 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219856 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 219.62
Current children cumulated vsize (Kb) 15048

[startup+230.018 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 22939 21 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219200 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 229.62
Current children cumulated vsize (Kb) 15048

[startup+240.019 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 23939 22 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221218944 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 239.63
Current children cumulated vsize (Kb) 15048

[startup+250.019 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 24939 22 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220320 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 249.63
Current children cumulated vsize (Kb) 15048

[startup+260.019 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 25939 22 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219008 134629216 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 259.63
Current children cumulated vsize (Kb) 15048

[startup+270.02 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 26939 22 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219672 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 269.63
Current children cumulated vsize (Kb) 15048

[startup+280.021 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 27940 22 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219600 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 279.64
Current children cumulated vsize (Kb) 15048

[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 28940 22 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219600 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 289.64
Current children cumulated vsize (Kb) 15048

[startup+300.021 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 29940 22 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219248 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 299.64
Current children cumulated vsize (Kb) 15048

[startup+310.022 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 30940 22 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219968 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 309.64
Current children cumulated vsize (Kb) 15048

[startup+320.022 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 31940 22 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219632 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 319.64
Current children cumulated vsize (Kb) 15048

[startup+330.024 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 32940 22 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220180 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 329.64
Current children cumulated vsize (Kb) 15048

[startup+340.024 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 33940 23 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220576 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 339.65
Current children cumulated vsize (Kb) 15048

[startup+350.024 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 34940 23 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219660 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 349.65
Current children cumulated vsize (Kb) 15048

[startup+360.025 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 35941 23 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221218896 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 359.66
Current children cumulated vsize (Kb) 15048

[startup+370.026 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 36941 23 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220028 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 369.66
Current children cumulated vsize (Kb) 15048

[startup+380.026 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 37941 23 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219856 134694377 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 379.66
Current children cumulated vsize (Kb) 15048

[startup+390.027 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 38941 23 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219472 134695274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 389.66
Current children cumulated vsize (Kb) 15048

[startup+400.028 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 39941 23 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219504 134849108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 399.66
Current children cumulated vsize (Kb) 15048

[startup+410.029 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 40942 23 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219308 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 409.67
Current children cumulated vsize (Kb) 15048

[startup+420.029 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 41942 23 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219440 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 419.67
Current children cumulated vsize (Kb) 15048

[startup+430.031 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 42942 23 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219996 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 429.67
Current children cumulated vsize (Kb) 15048

[startup+440.032 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 43942 23 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219280 134696587 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 439.67
Current children cumulated vsize (Kb) 15048

[startup+450.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 44942 23 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219828 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 449.67
Current children cumulated vsize (Kb) 15048

[startup+460.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 45943 23 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220064 134629138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 459.68
Current children cumulated vsize (Kb) 15048

[startup+470.034 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 46943 23 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219824 134695302 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 469.68
Current children cumulated vsize (Kb) 15048

[startup+480.035 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 47943 23 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219580 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 479.68
Current children cumulated vsize (Kb) 15048

[startup+490.035 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 48943 23 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219640 134842997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 489.68
Current children cumulated vsize (Kb) 15048

[startup+500.035 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 49943 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219308 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 499.69
Current children cumulated vsize (Kb) 15048

[startup+510.036 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 50944 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219780 134844636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 509.7
Current children cumulated vsize (Kb) 15048

[startup+520.037 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 51944 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219440 134844700 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 519.7
Current children cumulated vsize (Kb) 15048

[startup+530.037 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 52944 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219968 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 529.7
Current children cumulated vsize (Kb) 15048

[startup+540.038 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 53944 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220096 134845913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 539.7
Current children cumulated vsize (Kb) 15048

[startup+550.038 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 54944 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220560 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 549.7
Current children cumulated vsize (Kb) 15048

[startup+560.039 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 55945 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219112 134693601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 559.71
Current children cumulated vsize (Kb) 15048

[startup+570.039 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 56945 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220532 134845938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 569.71
Current children cumulated vsize (Kb) 15048

[startup+580.04 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 57945 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219268 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 579.71
Current children cumulated vsize (Kb) 15048

[startup+590.041 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 58945 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220944 134630835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 589.71
Current children cumulated vsize (Kb) 15048

[startup+600.041 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 59945 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220384 134694495 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 599.71
Current children cumulated vsize (Kb) 15048

[startup+610.041 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 60945 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219456 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 609.71
Current children cumulated vsize (Kb) 15048

[startup+620.041 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 61946 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219828 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 619.72
Current children cumulated vsize (Kb) 15048

[startup+630.042 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 62946 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219836 134845940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 629.72
Current children cumulated vsize (Kb) 15048

[startup+640.043 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 63946 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219488 134722527 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 639.72
Current children cumulated vsize (Kb) 15048

[startup+650.042 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 64946 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219328 134694545 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 649.72
Current children cumulated vsize (Kb) 15048

[startup+660.043 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 65946 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220684 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 659.72
Current children cumulated vsize (Kb) 15048

[startup+670.044 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 66947 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221218956 134845940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 669.73
Current children cumulated vsize (Kb) 15048

[startup+680.044 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 67947 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220588 134693792 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 679.73
Current children cumulated vsize (Kb) 15048

[startup+690.045 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 68947 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220432 134844708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 689.73
Current children cumulated vsize (Kb) 15048

[startup+700.045 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 69947 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219840 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 699.73
Current children cumulated vsize (Kb) 15048

[startup+710.046 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 70947 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220368 134522355 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 709.73
Current children cumulated vsize (Kb) 15048

[startup+720.046 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 71948 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220532 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 719.74
Current children cumulated vsize (Kb) 15048

[startup+730.047 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 72948 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220208 134694528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 729.74
Current children cumulated vsize (Kb) 15048

[startup+740.048 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 73948 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219692 134722542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 739.74
Current children cumulated vsize (Kb) 15048

[startup+750.048 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 74948 24 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220588 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 749.74
Current children cumulated vsize (Kb) 15048

[startup+760.049 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 75947 26 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220060 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 759.75
Current children cumulated vsize (Kb) 15048

[startup+770.049 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 76947 26 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220224 134849179 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 769.75
Current children cumulated vsize (Kb) 15048

[startup+780.051 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 77947 26 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219132 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 779.75
Current children cumulated vsize (Kb) 15048

[startup+790.051 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 78947 27 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220776 134629265 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 789.76
Current children cumulated vsize (Kb) 15048

[startup+800.051 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 79947 27 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219968 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 799.76
Current children cumulated vsize (Kb) 15048

[startup+810.052 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 80947 27 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219152 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 809.76
Current children cumulated vsize (Kb) 15048

[startup+820.053 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 81947 27 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219888 134629069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 819.76
Current children cumulated vsize (Kb) 15048

[startup+830.053 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 82947 27 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219680 134849143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 829.76
Current children cumulated vsize (Kb) 15048

[startup+840.054 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 83947 28 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219492 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 839.77
Current children cumulated vsize (Kb) 15048

[startup+850.055 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 84947 28 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220336 134696629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 849.77
Current children cumulated vsize (Kb) 15048

[startup+860.055 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 85948 28 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219200 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 859.78
Current children cumulated vsize (Kb) 15048

[startup+870.056 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 86948 28 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219264 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 869.78
Current children cumulated vsize (Kb) 15048

[startup+880.057 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 87948 28 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221221264 134843160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 879.78
Current children cumulated vsize (Kb) 15048

[startup+890.058 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 88948 28 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220352 134695269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 889.78
Current children cumulated vsize (Kb) 15048

[startup+900.057 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 89948 28 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220224 134694329 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 899.78
Current children cumulated vsize (Kb) 15048

[startup+910.058 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 90948 28 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219472 134718497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 909.78
Current children cumulated vsize (Kb) 15048

[startup+920.059 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 91948 28 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220172 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 919.78
Current children cumulated vsize (Kb) 15048

[startup+930.059 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 92949 28 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219684 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 929.79
Current children cumulated vsize (Kb) 15048

[startup+940.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 93949 28 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219552 134630728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 939.79
Current children cumulated vsize (Kb) 15048

[startup+950.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 94949 28 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220340 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 949.79
Current children cumulated vsize (Kb) 15048

[startup+960.061 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 95949 28 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220320 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 959.79
Current children cumulated vsize (Kb) 15048

[startup+970.061 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 96949 28 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220176 134722539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 969.79
Current children cumulated vsize (Kb) 15048

[startup+980.062 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 97950 28 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220504 134693621 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 979.8
Current children cumulated vsize (Kb) 15048

[startup+990.063 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 98949 29 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219884 134522320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 989.8
Current children cumulated vsize (Kb) 15048

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 99950 29 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219792 134845906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 999.81
Current children cumulated vsize (Kb) 15048

[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 100950 29 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221218780 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1009.81
Current children cumulated vsize (Kb) 15048

[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 101950 29 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220556 134845940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1019.81
Current children cumulated vsize (Kb) 15048

[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 102950 29 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220568 134722513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1029.81
Current children cumulated vsize (Kb) 15048

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 103950 29 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219720 134629277 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1039.81
Current children cumulated vsize (Kb) 15048

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 104950 29 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220384 134694532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1049.81
Current children cumulated vsize (Kb) 15048

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 105951 29 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219100 134723251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1059.82
Current children cumulated vsize (Kb) 15048

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 106951 29 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219444 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1069.82
Current children cumulated vsize (Kb) 15048

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 107951 29 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219808 134696618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1079.82
Current children cumulated vsize (Kb) 15048

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 108951 29 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220548 134845938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1089.82
Current children cumulated vsize (Kb) 15048

[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 109951 29 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220012 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1099.82
Current children cumulated vsize (Kb) 15048

[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 110952 29 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220912 134843420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1109.83
Current children cumulated vsize (Kb) 15048

[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 111952 29 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219504 134849061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1119.83
Current children cumulated vsize (Kb) 15048

[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 112952 29 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220256 134844736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1129.83
Current children cumulated vsize (Kb) 15048

[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 113952 29 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220556 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1139.83
Current children cumulated vsize (Kb) 15048

[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 114953 29 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219616 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1149.84
Current children cumulated vsize (Kb) 15048

[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 115953 29 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219804 134723240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1159.84
Current children cumulated vsize (Kb) 15048

[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 116953 30 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220332 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1169.85
Current children cumulated vsize (Kb) 15048

[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 117953 30 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220912 134843012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1179.85
Current children cumulated vsize (Kb) 15048

[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 118953 30 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219708 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1189.85
Current children cumulated vsize (Kb) 15048

[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 119953 30 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221219996 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1199.85
Current children cumulated vsize (Kb) 15048

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 120954 30 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220504 134693640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1209.86
Current children cumulated vsize (Kb) 15048



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 22714
Raw data (/proc/22709/stat): 22709 (minisat+_script) S 22708 22709 2660 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1851813797 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22709/statm): 532 234 485 147 0 385 0
[pid=22709] vsize: 2128
Raw data (/proc/22714/stat): 22714 (minisat+_bignum) R 22709 22709 2660 0 -1 0 3695 0 3 0 120954 30 0 0 25 0 1 0 1851813804 13230080 2950 4294967295 134512640 135167914 3221224448 3221220592 134629290 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22714/statm): 3230 2950 162 162 0 3068 0
[pid=22714] vsize: 12920
Current children cumulated CPU time (s) 1209.86
Current children cumulated vsize (Kb) 15048

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

Child status: 0
Real time (s): 1210.09
CPU time (s): 1209.85
CPU user time (s): 1209.54
CPU system time (s): 0.308953
CPU usage (%): 99.9806
Max. virtual memory (cumulated for all children) (Kb): 15048

Verifier Data

ERROR: no interpretation found !