Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-misc04.opb
MD5SUM8f93517b37e3e8e201991f7d854ddab3
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 21
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 2097151
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 42171551460515200
Number of bits of the biggest number in a constraint 56
Biggest sum of numbers in a constraint 130719213204604475
Number of bits of the biggest sum of numbers57
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables97606
Total number of constraints1755
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)45
Number of constraints which are nor clauses,nor cardinality constraints1710
Minimum length of a constraint1
Maximum length of a constraint3381

Trace number 6094

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        885772 kB
Buffers:         23148 kB
Cached:          99172 kB
SwapCached:        760 kB
Active:          27544 kB
Inactive:        97104 kB
HighTotal:      131008 kB
HighFree:        29008 kB
LowTotal:       903652 kB
LowFree:        856764 kB
SwapTotal:     2097136 kB
SwapFree:      2095596 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5584 kB
Slab:            18620 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 03:33:55 (client local time) WITH STATUS 0 IN 1207.2 SECONDS
stats: 3248 7 1207.2 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 6477] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 1985 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1999]---> Sorter-cost: 2431     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5
c ---[1998]---> Sorter-cost: 2431     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5
c ---[1997]---> Sorter-cost: 2431     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5
c ---[1996]---> Sorter-cost: 2431     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5
c ---[1995]---> Sorter-cost: 2029     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 5
c ---[1994]---> Sorter-cost: 2029     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 5
c ---[1993]---> Sorter-cost: 2029     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 5
c ---[1992]---> Sorter-cost: 2029     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 5
c ---[1991]---> Sorter-cost:  861     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[1990]---> Sorter-cost:  861     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[1989]---> Sorter-cost:  861     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[1988]---> Sorter-cost:  861     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[1987]---> Sorter-cost:  861     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[1986]---> Sorter-cost:  861     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[1985]---> Sorter-cost:  861     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[1984]---> Sorter-cost:  861     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[1983]---> Sorter-cost:  831     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[1982]---> Sorter-cost:  831     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[1981]---> Sorter-cost:  831     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[1980]---> Sorter-cost:  831     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[1979]---> Adder-cost: 494   maxlim: 151532   bits: 18/18
c ---[1978]---> Adder-cost: 494   maxlim: 151532   bits: 18/18
c ---[1977]---> Adder-cost: 494   maxlim: 151532   bits: 18/18
c ---[1976]---> Adder-cost: 494   maxlim: 151532   bits: 18/18
c ---[1975]---> Adder-cost: 494   maxlim: 151532   bits: 18/18
c ---[1974]---> Adder-cost: 494   maxlim: 151532   bits: 18/18
c ---[1973]---> Adder-cost: 494   maxlim: 151532   bits: 18/18
c ---[1972]---> Adder-cost: 494   maxlim: 151532   bits: 18/18
c ---[1971]---> Adder-cost: 456   maxlim: 75756   bits: 17/17
c ---[1970]---> Adder-cost: 456   maxlim: 75756   bits: 17/17
c ---[1969]---> Adder-cost: 456   maxlim: 75756   bits: 17/17
c ---[1968]---> Adder-cost: 456   maxlim: 75756   bits: 17/17
c ---[1967]---> Sorter-cost:18557     Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1966]---> Sorter-cost:18557     Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1965]---> Sorter-cost:18614     Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1964]---> Sorter-cost:18614     Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1963]---> Sorter-cost: 2994     Base: 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1962]---> Sorter-cost: 2994     Base: 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1961]---> Sorter-cost: 3009     Base: 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1960]---> Sorter-cost: 3009     Base: 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1959]---> Sorter-cost: 3739     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 11
c ---[1958]---> Sorter-cost: 3739     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 11
c ---[1957]---> Sorter-cost: 3592     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[1956]---> Sorter-cost: 3592     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[1955]---> Adder-cost: 506   maxlim: 46056   bits: 16/16
c ---[1954]---> Adder-cost: 506   maxlim: 46056   bits: 16/16
c ---[1953]---> Adder-cost: 506   maxlim: 46056   bits: 16/16
c ---[1952]---> Adder-cost: 506   maxlim: 46056   bits: 16/16
c ---[1951]---> Sorter-cost: 2987     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1950]---> Sorter-cost: 2987     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1949]---> Sorter-cost: 3008     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1948]---> Sorter-cost: 3008     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1947]---> Adder-cost: 598   maxlim: 184296   bits: 18/18
c ---[1946]---> Adder-cost: 598   maxlim: 184296   bits: 18/18
c ---[1945]---> Adder-cost: 644   maxlim: 368616   bits: 19/19
c ---[1944]---> Adder-cost: 644   maxlim: 368616   bits: 19/19
c ---[1942]---> Adder-cost: 644   maxlim: 376808   bits: 19/19
c ---[1941]---> Adder-cost: 690   maxlim: 753640   bits: 20/20
c ---[1940]---> Adder-cost: 736   maxlim: 1507304   bits: 21/21
c ---[1939]---> Sorter-cost: 4382     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1938]---> Sorter-cost: 6906     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1937]---> Sorter-cost: 6999     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1936]---> Sorter-cost: 7061     Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1935]---> Sorter-cost:20066     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1934]---> Sorter-cost:26004     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1933]---> Sorter-cost:26194     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1932]---> Sorter-cost:26298     Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1931]---> Adder-cost: 552   maxlim: 92136   bits: 17/17
c ---[1930]---> Adder-cost: 552   maxlim: 92136   bits: 17/17
c ---[1929]---> Adder-cost: 552   maxlim: 92136   bits: 17/17
c ---[1928]---> Adder-cost: 552   maxlim: 92136   bits: 17/17
c ---[1926]---> Adder-cost: 782   maxlim: 2949096   bits: 22/22
c ---[1925]---> Adder-cost: 782   maxlim: 2949096   bits: 22/22
c ---[1924]---> Adder-cost: 782   maxlim: 2949096   bits: 22/22
c ---[1922]---> Adder-cost: 690   maxlim: 737256   bits: 20/20
c ---[1921]---> Adder-cost: 736   maxlim: 1474536   bits: 21/21
c ---[1920]---> Adder-cost: 782   maxlim: 2949096   bits: 22/22
c ---[1919]---> Adder-cost: 644   maxlim: 368616   bits: 19/19
c ---[1918]---> Adder-cost: 644   maxlim: 368616   bits: 19/19
c ---[1917]---> Adder-cost: 644   maxlim: 368616   bits: 19/19
c ---[1916]---> Adder-cost: 644   maxlim: 368616   bits: 19/19
c ---[1914]---> Adder-cost: 736   maxlim: 1474536   bits: 21/21
c ---[1913]---> Adder-cost: 782   maxlim: 2949096   bits: 22/22
c ---[1912]---> Adder-cost: 782   maxlim: 2949096   bits: 22/22
c ---[1911]---> Sorter-cost:30538     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1910]---> Sorter-cost:35446     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1909]---> Sorter-cost:35555     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1908]---> Sorter-cost:35659     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1906]---> Sorter-cost:13893     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1905]---> Sorter-cost:14928     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1904]---> Sorter-cost:15851     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1902]---> Adder-cost: 736   maxlim: 1474536   bits: 21/21
c ---[1901]---> Adder-cost: 782   maxlim: 2949096   bits: 22/22
c ---[1900]---> Adder-cost: 782   maxlim: 2949096   bits: 22/22
c ---[1899]---> Adder-cost: 782   maxlim: 3014632   bits: 22/22
c ---[1898]---> Adder-cost: 782   maxlim: 3014632   bits: 22/22
c ---[1897]---> Adder-cost: 782   maxlim: 3014632   bits: 22/22
c ---[1896]---> Adder-cost: 782

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/32379/stat): 32379 (minisat+_script) R 32378 32379 9854 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1796978533 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/32379/statm): 174 3 169 147 0 27 0
[pid=32379] 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=32380
New process pid=32381
New process pid=32382
execve syscall for /bin/sed executable
One traced child (pid=32381) 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=32382) exited with status: 0
One traced child (pid=32380) exited with status: 0
New process pid=32383
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-misc04.opb
One traced child (pid=32383) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=32384
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-misc04.opb

[startup+10.0039 s]
Raw data (loadavg): 0.82 0.93 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 3726 0 0 0 728 17 0 0 25 0 1 0 1796978769 15372288 3561 4294967295 134512640 135167914 3221224448 3221222784 134694425 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32384/statm): 3753 3561 162 162 0 3591 0
[pid=32384] vsize: 15012
Current children cumulated CPU time (s) 9.53
Current children cumulated vsize (Kb) 17140

[startup+20.0047 s]
Raw data (loadavg): 0.85 0.93 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) T 32379 32379 9854 0 -1 0 7457 0 0 0 1687 39 0 0 25 0 1 0 1796978769 32321536 7127 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/32384/statm): 7891 7127 162 162 0 7729 0
[pid=32384] vsize: 31564
Current children cumulated CPU time (s) 19.34
Current children cumulated vsize (Kb) 33692

[startup+30.0055 s]
Raw data (loadavg): 0.87 0.93 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 11127 0 0 0 2652 57 0 0 25 0 1 0 1796978769 45039616 10262 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 10996 10262 162 162 0 10834 0
[pid=32384] vsize: 43984
Current children cumulated CPU time (s) 29.17
Current children cumulated vsize (Kb) 46112

[startup+40.0062 s]
Raw data (loadavg): 0.89 0.93 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 11127 0 0 0 3652 57 0 0 25 0 1 0 1796978769 45039616 10262 4294967295 134512640 135167914 3221224448 3221223204 134697054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 10996 10262 162 162 0 10834 0
[pid=32384] vsize: 43984
Current children cumulated CPU time (s) 39.17
Current children cumulated vsize (Kb) 46112

[startup+50.007 s]
Raw data (loadavg): 0.91 0.93 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 11136 0 0 0 4652 57 0 0 25 0 1 0 1796978769 42708992 9699 4294967295 134512640 135167914 3221224448 3221221740 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 10427 9699 162 162 0 10265 0
[pid=32384] vsize: 41708
Current children cumulated CPU time (s) 49.17
Current children cumulated vsize (Kb) 43836

[startup+60.0078 s]
Raw data (loadavg): 0.92 0.93 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 11271 0 0 0 5652 58 0 0 25 0 1 0 1796978769 43401216 9834 4294967295 134512640 135167914 3221224448 3221222284 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 10596 9834 162 162 0 10434 0
[pid=32384] vsize: 42384
Current children cumulated CPU time (s) 59.18
Current children cumulated vsize (Kb) 44512

[startup+70.0086 s]
Raw data (loadavg): 0.93 0.94 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 11907 0 0 0 6649 59 0 0 25 0 1 0 1796978769 45400064 10345 4294967295 134512640 135167914 3221224448 3221222492 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 11084 10345 162 162 0 10922 0
[pid=32384] vsize: 44336
Current children cumulated CPU time (s) 69.16
Current children cumulated vsize (Kb) 46464

[startup+80.0094 s]
Raw data (loadavg): 0.94 0.94 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 12671 0 0 0 7644 62 0 0 25 0 1 0 1796978769 47964160 10944 4294967295 134512640 135167914 3221224448 3221220876 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32384/statm): 11710 10944 162 162 0 11548 0
[pid=32384] vsize: 46840
Current children cumulated CPU time (s) 79.14
Current children cumulated vsize (Kb) 48968

[startup+90.0102 s]
Raw data (loadavg): 0.95 0.94 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 12748 0 0 0 8643 63 0 0 25 0 1 0 1796978769 48160768 11021 4294967295 134512640 135167914 3221224448 3221221472 134630751 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 11758 11021 162 162 0 11596 0
[pid=32384] vsize: 47032
Current children cumulated CPU time (s) 89.14
Current children cumulated vsize (Kb) 49160

[startup+100.011 s]
Raw data (loadavg): 0.96 0.94 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 12809 0 0 0 9643 63 0 0 25 0 1 0 1796978769 48320512 11082 4294967295 134512640 135167914 3221224448 3221220368 134522341 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 11797 11082 162 162 0 11635 0
[pid=32384] vsize: 47188
Current children cumulated CPU time (s) 99.14
Current children cumulated vsize (Kb) 49316

[startup+110.012 s]
Raw data (loadavg): 0.96 0.94 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 12838 0 0 0 10643 63 0 0 25 0 1 0 1796978769 49967104 11111 4294967295 134512640 135167914 3221224448 3221221052 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 12199 11111 162 162 0 12037 0
[pid=32384] vsize: 48796
Current children cumulated CPU time (s) 109.14
Current children cumulated vsize (Kb) 50924

[startup+120.013 s]
Raw data (loadavg): 0.97 0.94 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 12926 0 0 0 11642 64 0 0 25 0 1 0 1796978769 50192384 11199 4294967295 134512640 135167914 3221224448 3221219936 134844672 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 12254 11199 162 162 0 12092 0
[pid=32384] vsize: 49016
Current children cumulated CPU time (s) 119.14
Current children cumulated vsize (Kb) 51144

[startup+130.013 s]
Raw data (loadavg): 0.97 0.95 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 13089 0 0 0 12641 64 0 0 25 0 1 0 1796978769 50647040 11362 4294967295 134512640 135167914 3221224448 3221220224 134693570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 12365 11362 162 162 0 12203 0
[pid=32384] vsize: 49460
Current children cumulated CPU time (s) 129.13
Current children cumulated vsize (Kb) 51588

[startup+140.013 s]
Raw data (loadavg): 0.98 0.95 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 13845 0 0 0 13640 66 0 0 25 0 1 0 1796978769 52232192 11788 4294967295 134512640 135167914 3221224448 3221221152 134844703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 12752 11788 162 162 0 12590 0
[pid=32384] vsize: 51008
Current children cumulated CPU time (s) 139.14
Current children cumulated vsize (Kb) 53136

[startup+150.014 s]
Raw data (loadavg): 0.98 0.95 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 14070 0 0 0 14639 67 0 0 25 0 1 0 1796978769 52862976 11971 4294967295 134512640 135167914 3221224448 3221220400 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 12906 11971 162 162 0 12744 0
[pid=32384] vsize: 51624
Current children cumulated CPU time (s) 149.14
Current children cumulated vsize (Kb) 53752

[startup+160.015 s]
Raw data (loadavg): 0.98 0.95 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 14291 0 0 0 15638 67 0 0 25 0 1 0 1796978769 53346304 12150 4294967295 134512640 135167914 3221224448 3221219856 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 13024 12150 162 162 0 12862 0
[pid=32384] vsize: 52096
Current children cumulated CPU time (s) 159.13
Current children cumulated vsize (Kb) 54224

[startup+170.014 s]
Raw data (loadavg): 0.98 0.95 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 14291 0 0 0 16638 67 0 0 25 0 1 0 1796978769 53346304 12150 4294967295 134512640 135167914 3221224448 3221219628 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 13024 12150 162 162 0 12862 0
[pid=32384] vsize: 52096
Current children cumulated CPU time (s) 169.13
Current children cumulated vsize (Kb) 54224

[startup+180.015 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 14539 0 0 0 17638 67 0 0 25 0 1 0 1796978769 53874688 12356 4294967295 134512640 135167914 3221224448 3221220540 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 13153 12356 162 162 0 12991 0
[pid=32384] vsize: 52612
Current children cumulated CPU time (s) 179.13
Current children cumulated vsize (Kb) 54740

[startup+190.016 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 14539 0 0 0 18638 67 0 0 25 0 1 0 1796978769 53874688 12356 4294967295 134512640 135167914 3221224448 3221221296 134629340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 13153 12356 162 162 0 12991 0
[pid=32384] vsize: 52612
Current children cumulated CPU time (s) 189.13
Current children cumulated vsize (Kb) 54740

[startup+200.017 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 14788 0 0 0 19636 68 0 0 25 0 1 0 1796978769 54411264 12563 4294967295 134512640 135167914 3221224448 3221220124 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 13284 12563 162 162 0 13122 0
[pid=32384] vsize: 53136
Current children cumulated CPU time (s) 199.12
Current children cumulated vsize (Kb) 55264

[startup+210.018 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 14901 0 0 0 20636 69 0 0 25 0 1 0 1796978769 57761792 12676 4294967295 134512640 135167914 3221224448 3221222832 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 14102 12676 162 162 0 13940 0
[pid=32384] vsize: 56408
Current children cumulated CPU time (s) 209.13
Current children cumulated vsize (Kb) 58536

[startup+220.018 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 15412 0 0 0 21633 70 0 0 25 0 1 0 1796978769 59052032 13062 4294967295 134512640 135167914 3221224448 3221219808 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 14417 13062 162 162 0 14255 0
[pid=32384] vsize: 57668
Current children cumulated CPU time (s) 219.11
Current children cumulated vsize (Kb) 59796

[startup+230.019 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 15412 0 0 0 22633 70 0 0 25 0 1 0 1796978769 59052032 13062 4294967295 134512640 135167914 3221224448 3221220576 134522268 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 14417 13062 162 162 0 14255 0
[pid=32384] vsize: 57668
Current children cumulated CPU time (s) 229.11
Current children cumulated vsize (Kb) 59796

[startup+240.019 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 15412 0 0 0 23633 70 0 0 25 0 1 0 1796978769 59052032 13062 4294967295 134512640 135167914 3221224448 3221219952 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 14417 13062 162 162 0 14255 0
[pid=32384] vsize: 57668
Current children cumulated CPU time (s) 239.11
Current children cumulated vsize (Kb) 59796

[startup+250.02 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 15412 0 0 0 24633 70 0 0 25 0 1 0 1796978769 59052032 13062 4294967295 134512640 135167914 3221224448 3221220384 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 14417 13062 162 162 0 14255 0
[pid=32384] vsize: 57668
Current children cumulated CPU time (s) 249.11
Current children cumulated vsize (Kb) 59796

[startup+260.021 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 15412 0 0 0 25633 70 0 0 25 0 1 0 1796978769 59052032 13062 4294967295 134512640 135167914 3221224448 3221220564 134849086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 14417 13062 162 162 0 14255 0
[pid=32384] vsize: 57668
Current children cumulated CPU time (s) 259.11
Current children cumulated vsize (Kb) 59796

[startup+270.02 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 15412 0 0 0 26634 70 0 0 25 0 1 0 1796978769 59052032 13062 4294967295 134512640 135167914 3221224448 3221219472 134720491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 14417 13062 162 162 0 14255 0
[pid=32384] vsize: 57668
Current children cumulated CPU time (s) 269.12
Current children cumulated vsize (Kb) 59796

[startup+280.021 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 15412 0 0 0 27634 70 0 0 25 0 1 0 1796978769 59052032 13062 4294967295 134512640 135167914 3221224448 3221220340 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 14417 13062 162 162 0 14255 0
[pid=32384] vsize: 57668
Current children cumulated CPU time (s) 279.12
Current children cumulated vsize (Kb) 59796

[startup+290.022 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 15412 0 0 0 28634 70 0 0 25 0 1 0 1796978769 59052032 13062 4294967295 134512640 135167914 3221224448 3221219980 134723260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 14417 13062 162 162 0 14255 0
[pid=32384] vsize: 57668
Current children cumulated CPU time (s) 289.12
Current children cumulated vsize (Kb) 59796

[startup+300.023 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17117 0 0 0 29628 75 0 0 25 0 1 0 1796978769 62443520 13983 4294967295 134512640 135167914 3221224448 3221219088 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15245 13983 162 162 0 15083 0
[pid=32384] vsize: 60980
Current children cumulated CPU time (s) 299.11
Current children cumulated vsize (Kb) 63108

[startup+310.024 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17117 0 0 0 30629 75 0 0 25 0 1 0 1796978769 62443520 13983 4294967295 134512640 135167914 3221224448 3221220912 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15245 13983 162 162 0 15083 0
[pid=32384] vsize: 60980
Current children cumulated CPU time (s) 309.12
Current children cumulated vsize (Kb) 63108

[startup+320.023 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17117 0 0 0 31629 75 0 0 25 0 1 0 1796978769 62443520 13983 4294967295 134512640 135167914 3221224448 3221220048 134849122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15245 13983 162 162 0 15083 0
[pid=32384] vsize: 60980
Current children cumulated CPU time (s) 319.12
Current children cumulated vsize (Kb) 63108

[startup+330.024 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17117 0 0 0 32629 75 0 0 25 0 1 0 1796978769 62443520 13983 4294967295 134512640 135167914 3221224448 3221220572 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15245 13983 162 162 0 15083 0
[pid=32384] vsize: 60980
Current children cumulated CPU time (s) 329.12
Current children cumulated vsize (Kb) 63108

[startup+340.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17117 0 0 0 33629 75 0 0 25 0 1 0 1796978769 62443520 13983 4294967295 134512640 135167914 3221224448 3221220908 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15245 13983 162 162 0 15083 0
[pid=32384] vsize: 60980
Current children cumulated CPU time (s) 339.12
Current children cumulated vsize (Kb) 63108

[startup+350.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17117 0 0 0 34630 75 0 0 25 0 1 0 1796978769 62443520 13983 4294967295 134512640 135167914 3221224448 3221221228 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15245 13983 162 162 0 15083 0
[pid=32384] vsize: 60980
Current children cumulated CPU time (s) 349.13
Current children cumulated vsize (Kb) 63108

[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17117 0 0 0 35630 75 0 0 25 0 1 0 1796978769 62443520 13983 4294967295 134512640 135167914 3221224448 3221221104 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15245 13983 162 162 0 15083 0
[pid=32384] vsize: 60980
Current children cumulated CPU time (s) 359.13
Current children cumulated vsize (Kb) 63108

[startup+370.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17117 0 0 0 36630 75 0 0 25 0 1 0 1796978769 62443520 13983 4294967295 134512640 135167914 3221224448 3221220352 134720472 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15245 13983 162 162 0 15083 0
[pid=32384] vsize: 60980
Current children cumulated CPU time (s) 369.13
Current children cumulated vsize (Kb) 63108

[startup+380.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17523 0 0 0 37628 76 0 0 25 0 1 0 1796978769 63168512 14264 4294967295 134512640 135167914 3221224448 3221219440 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15422 14264 162 162 0 15260 0
[pid=32384] vsize: 61688
Current children cumulated CPU time (s) 379.12
Current children cumulated vsize (Kb) 63816

[startup+390.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17523 0 0 0 38629 76 0 0 25 0 1 0 1796978769 63168512 14264 4294967295 134512640 135167914 3221224448 3221220064 134630917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15422 14264 162 162 0 15260 0
[pid=32384] vsize: 61688
Current children cumulated CPU time (s) 389.13
Current children cumulated vsize (Kb) 63816

[startup+400.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17523 0 0 0 39629 76 0 0 25 0 1 0 1796978769 63168512 14264 4294967295 134512640 135167914 3221224448 3221220156 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15422 14264 162 162 0 15260 0
[pid=32384] vsize: 61688
Current children cumulated CPU time (s) 399.13
Current children cumulated vsize (Kb) 63816

[startup+410.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17523 0 0 0 40629 76 0 0 25 0 1 0 1796978769 63168512 14264 4294967295 134512640 135167914 3221224448 3221221136 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15422 14264 162 162 0 15260 0
[pid=32384] vsize: 61688
Current children cumulated CPU time (s) 409.13
Current children cumulated vsize (Kb) 63816

[startup+420.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17523 0 0 0 41629 76 0 0 25 0 1 0 1796978769 63168512 14264 4294967295 134512640 135167914 3221224448 3221221104 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15422 14264 162 162 0 15260 0
[pid=32384] vsize: 61688
Current children cumulated CPU time (s) 419.13
Current children cumulated vsize (Kb) 63816

[startup+430.032 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17523 0 0 0 42629 76 0 0 25 0 1 0 1796978769 63168512 14264 4294967295 134512640 135167914 3221224448 3221220560 134694398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15422 14264 162 162 0 15260 0
[pid=32384] vsize: 61688
Current children cumulated CPU time (s) 429.13
Current children cumulated vsize (Kb) 63816

[startup+440.032 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17523 0 0 0 43630 76 0 0 25 0 1 0 1796978769 63168512 14264 4294967295 134512640 135167914 3221224448 3221219996 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15422 14264 162 162 0 15260 0
[pid=32384] vsize: 61688
Current children cumulated CPU time (s) 439.14
Current children cumulated vsize (Kb) 63816

[startup+450.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17523 0 0 0 44630 76 0 0 25 0 1 0 1796978769 63168512 14264 4294967295 134512640 135167914 3221224448 3221221996 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15422 14264 162 162 0 15260 0
[pid=32384] vsize: 61688
Current children cumulated CPU time (s) 449.14
Current children cumulated vsize (Kb) 63816

[startup+460.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17966 0 0 0 45627 78 0 0 25 0 1 0 1796978769 63893504 14546 4294967295 134512640 135167914 3221224448 3221219552 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15599 14546 162 162 0 15437 0
[pid=32384] vsize: 62396
Current children cumulated CPU time (s) 459.13
Current children cumulated vsize (Kb) 64524

[startup+470.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17966 0 0 0 46627 78 0 0 25 0 1 0 1796978769 63893504 14546 4294967295 134512640 135167914 3221224448 3221219324 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15599 14546 162 162 0 15437 0
[pid=32384] vsize: 62396
Current children cumulated CPU time (s) 469.13
Current children cumulated vsize (Kb) 64524

[startup+480.034 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17966 0 0 0 47627 78 0 0 25 0 1 0 1796978769 63893504 14546 4294967295 134512640 135167914 3221224448 3221219536 134629143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15599 14546 162 162 0 15437 0
[pid=32384] vsize: 62396
Current children cumulated CPU time (s) 479.13
Current children cumulated vsize (Kb) 64524

[startup+490.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17966 0 0 0 48628 78 0 0 25 0 1 0 1796978769 63893504 14546 4294967295 134512640 135167914 3221224448 3221220648 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15599 14546 162 162 0 15437 0
[pid=32384] vsize: 62396
Current children cumulated CPU time (s) 489.14
Current children cumulated vsize (Kb) 64524

[startup+500.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17966 0 0 0 49628 78 0 0 25 0 1 0 1796978769 63893504 14546 4294967295 134512640 135167914 3221224448 3221221824 134629358 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15599 14546 162 162 0 15437 0
[pid=32384] vsize: 62396
Current children cumulated CPU time (s) 499.14
Current children cumulated vsize (Kb) 64524

[startup+510.036 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17966 0 0 0 50628 78 0 0 25 0 1 0 1796978769 63893504 14546 4294967295 134512640 135167914 3221224448 3221221428 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15599 14546 162 162 0 15437 0
[pid=32384] vsize: 62396
Current children cumulated CPU time (s) 509.14
Current children cumulated vsize (Kb) 64524

[startup+520.037 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17966 0 0 0 51628 78 0 0 25 0 1 0 1796978769 63893504 14546 4294967295 134512640 135167914 3221224448 3221221616 134843400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15599 14546 162 162 0 15437 0
[pid=32384] vsize: 62396
Current children cumulated CPU time (s) 519.14
Current children cumulated vsize (Kb) 64524

[startup+530.038 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17966 0 0 0 52628 78 0 0 25 0 1 0 1796978769 63893504 14546 4294967295 134512640 135167914 3221224448 3221220080 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15599 14546 162 162 0 15437 0
[pid=32384] vsize: 62396
Current children cumulated CPU time (s) 529.14
Current children cumulated vsize (Kb) 64524

[startup+540.039 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 17966 0 0 0 53629 78 0 0 25 0 1 0 1796978769 63893504 14546 4294967295 134512640 135167914 3221224448 3221219680 134849122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15599 14546 162 162 0 15437 0
[pid=32384] vsize: 62396
Current children cumulated CPU time (s) 539.15
Current children cumulated vsize (Kb) 64524

[startup+550.039 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18093 0 0 0 54629 78 0 0 25 0 1 0 1796978769 63934464 14637 4294967295 134512640 135167914 3221224448 3221221632 134849061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15609 14637 162 162 0 15447 0
[pid=32384] vsize: 62436
Current children cumulated CPU time (s) 549.15
Current children cumulated vsize (Kb) 64564

[startup+560.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18093 0 0 0 55629 78 0 0 25 0 1 0 1796978769 63934464 14637 4294967295 134512640 135167914 3221224448 3221221440 134843074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15609 14637 162 162 0 15447 0
[pid=32384] vsize: 62436
Current children cumulated CPU time (s) 559.15
Current children cumulated vsize (Kb) 64564

[startup+570.041 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18093 0 0 0 56629 78 0 0 25 0 1 0 1796978769 63934464 14637 4294967295 134512640 135167914 3221224448 3221221584 134695269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15609 14637 162 162 0 15447 0
[pid=32384] vsize: 62436
Current children cumulated CPU time (s) 569.15
Current children cumulated vsize (Kb) 64564

[startup+580.042 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18093 0 0 0 57629 78 0 0 25 0 1 0 1796978769 63934464 14637 4294967295 134512640 135167914 3221224448 3221221296 134629275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15609 14637 162 162 0 15447 0
[pid=32384] vsize: 62436
Current children cumulated CPU time (s) 579.15
Current children cumulated vsize (Kb) 64564

[startup+590.043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18219 0 0 0 58629 78 0 0 25 0 1 0 1796978769 64282624 14763 4294967295 134512640 135167914 3221224448 3221219088 134844689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15694 14763 162 162 0 15532 0
[pid=32384] vsize: 62776
Current children cumulated CPU time (s) 589.15
Current children cumulated vsize (Kb) 64904

[startup+600.043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18219 0 0 0 59629 78 0 0 25 0 1 0 1796978769 64282624 14763 4294967295 134512640 135167914 3221224448 3221220048 134849122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15694 14763 162 162 0 15532 0
[pid=32384] vsize: 62776
Current children cumulated CPU time (s) 599.15
Current children cumulated vsize (Kb) 64904

[startup+610.044 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18219 0 0 0 60629 78 0 0 25 0 1 0 1796978769 64282624 14763 4294967295 134512640 135167914 3221224448 3221221208 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15694 14763 162 162 0 15532 0
[pid=32384] vsize: 62776
Current children cumulated CPU time (s) 609.15
Current children cumulated vsize (Kb) 64904

[startup+620.044 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18219 0 0 0 61630 78 0 0 25 0 1 0 1796978769 64282624 14763 4294967295 134512640 135167914 3221224448 3221220832 134845906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15694 14763 162 162 0 15532 0
[pid=32384] vsize: 62776
Current children cumulated CPU time (s) 619.16
Current children cumulated vsize (Kb) 64904

[startup+630.045 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18338 0 0 0 62629 79 0 0 25 0 1 0 1796978769 64589824 14882 4294967295 134512640 135167914 3221224448 3221219328 134694539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15769 14882 162 162 0 15607 0
[pid=32384] vsize: 63076
Current children cumulated CPU time (s) 629.16
Current children cumulated vsize (Kb) 65204

[startup+640.045 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18338 0 0 0 63629 79 0 0 25 0 1 0 1796978769 64589824 14882 4294967295 134512640 135167914 3221224448 3221220384 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15769 14882 162 162 0 15607 0
[pid=32384] vsize: 63076
Current children cumulated CPU time (s) 639.16
Current children cumulated vsize (Kb) 65204

[startup+650.046 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18338 0 0 0 64630 79 0 0 25 0 1 0 1796978769 64589824 14882 4294967295 134512640 135167914 3221224448 3221220752 134693566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15769 14882 162 162 0 15607 0
[pid=32384] vsize: 63076
Current children cumulated CPU time (s) 649.17
Current children cumulated vsize (Kb) 65204

[startup+660.047 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18338 0 0 0 65630 79 0 0 25 0 1 0 1796978769 64589824 14882 4294967295 134512640 135167914 3221224448 3221221552 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15769 14882 162 162 0 15607 0
[pid=32384] vsize: 63076
Current children cumulated CPU time (s) 659.17
Current children cumulated vsize (Kb) 65204

[startup+670.048 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18338 0 0 0 66630 79 0 0 25 0 1 0 1796978769 64589824 14882 4294967295 134512640 135167914 3221224448 3221221420 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15769 14882 162 162 0 15607 0
[pid=32384] vsize: 63076
Current children cumulated CPU time (s) 669.17
Current children cumulated vsize (Kb) 65204

[startup+680.049 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18519 0 0 0 67629 79 0 0 25 0 1 0 1796978769 65024000 15063 4294967295 134512640 135167914 3221224448 3221143264 134523819 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15875 15063 162 162 0 15713 0
[pid=32384] vsize: 63500
Current children cumulated CPU time (s) 679.16
Current children cumulated vsize (Kb) 65628

[startup+690.049 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18566 0 0 0 68628 80 0 0 25 0 1 0 1796978769 65040384 15070 4294967295 134512640 135167914 3221224448 3221221808 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15879 15070 162 162 0 15717 0
[pid=32384] vsize: 63516
Current children cumulated CPU time (s) 689.16
Current children cumulated vsize (Kb) 65644

[startup+700.05 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18689 0 0 0 69628 80 0 0 25 0 1 0 1796978769 65392640 15193 4294967295 134512640 135167914 3221224448 3221221736 134693626 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 15965 15193 162 162 0 15803 0
[pid=32384] vsize: 63860
Current children cumulated CPU time (s) 699.16
Current children cumulated vsize (Kb) 65988

[startup+710.051 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18819 0 0 0 70627 81 0 0 25 0 1 0 1796978769 65732608 15323 4294967295 134512640 135167914 3221224448 3221220548 134845938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 16048 15323 162 162 0 15886 0
[pid=32384] vsize: 64192
Current children cumulated CPU time (s) 709.16
Current children cumulated vsize (Kb) 66320

[startup+720.051 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18949 0 0 0 71626 82 0 0 25 0 1 0 1796978769 72359936 15453 4294967295 134512640 135167914 3221224448 3221220672 134845895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 17666 15453 162 162 0 17504 0
[pid=32384] vsize: 70664
Current children cumulated CPU time (s) 719.16
Current children cumulated vsize (Kb) 72792

[startup+730.052 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 18949 0 0 0 72626 82 0 0 25 0 1 0 1796978769 72359936 15453 4294967295 134512640 135167914 3221224448 3221222320 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 17666 15453 162 162 0 17504 0
[pid=32384] vsize: 70664
Current children cumulated CPU time (s) 729.16
Current children cumulated vsize (Kb) 72792

[startup+740.052 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 19082 0 0 0 73626 82 0 0 25 0 1 0 1796978769 72712192 15586 4294967295 134512640 135167914 3221224448 3221220844 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 17752 15586 162 162 0 17590 0
[pid=32384] vsize: 71008
Current children cumulated CPU time (s) 739.16
Current children cumulated vsize (Kb) 73136

[startup+750.053 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 19212 0 0 0 74626 83 0 0 25 0 1 0 1796978769 73048064 15716 4294967295 134512640 135167914 3221224448 3221220120 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 17834 15716 162 162 0 17672 0
[pid=32384] vsize: 71336
Current children cumulated CPU time (s) 749.17
Current children cumulated vsize (Kb) 73464

[startup+760.054 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 19212 0 0 0 75626 83 0 0 25 0 1 0 1796978769 73048064 15716 4294967295 134512640 135167914 3221224448 3221221456 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 17834 15716 162 162 0 17672 0
[pid=32384] vsize: 71336
Current children cumulated CPU time (s) 759.17
Current children cumulated vsize (Kb) 73464

[startup+770.054 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 19341 0 0 0 76626 83 0 0 25 0 1 0 1796978769 73383936 15845 4294967295 134512640 135167914 3221224448 3221221116 134522235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 17916 15845 162 162 0 17754 0
[pid=32384] vsize: 71664
Current children cumulated CPU time (s) 769.17
Current children cumulated vsize (Kb) 73792

[startup+780.054 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 19471 0 0 0 77625 83 0 0 25 0 1 0 1796978769 73723904 15975 4294967295 134512640 135167914 3221224448 3221219328 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 17999 15975 162 162 0 17837 0
[pid=32384] vsize: 71996
Current children cumulated CPU time (s) 779.16
Current children cumulated vsize (Kb) 74124

[startup+790.055 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 19471 0 0 0 78626 83 0 0 25 0 1 0 1796978769 73723904 15975 4294967295 134512640 135167914 3221224448 3221222576 134844637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 17999 15975 162 162 0 17837 0
[pid=32384] vsize: 71996
Current children cumulated CPU time (s) 789.17
Current children cumulated vsize (Kb) 74124

[startup+800.056 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 19779 0 0 0 79624 84 0 0 25 0 1 0 1796978769 74276864 16202 4294967295 134512640 135167914 3221224448 3221220592 134630751 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 18134 16202 162 162 0 17972 0
[pid=32384] vsize: 72536
Current children cumulated CPU time (s) 799.16
Current children cumulated vsize (Kb) 74664

[startup+810.057 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 19779 0 0 0 80624 84 0 0 25 0 1 0 1796978769 74276864 16202 4294967295 134512640 135167914 3221224448 3221219968 134696386 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 18134 16202 162 162 0 17972 0
[pid=32384] vsize: 72536
Current children cumulated CPU time (s) 809.16
Current children cumulated vsize (Kb) 74664

[startup+820.058 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 19779 0 0 0 81624 84 0 0 25 0 1 0 1796978769 74276864 16202 4294967295 134512640 135167914 3221224448 3221221052 134722231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 18134 16202 162 162 0 17972 0
[pid=32384] vsize: 72536
Current children cumulated CPU time (s) 819.16
Current children cumulated vsize (Kb) 74664

[startup+830.058 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 19779 0 0 0 82625 84 0 0 25 0 1 0 1796978769 74276864 16202 4294967295 134512640 135167914 3221224448 3221220940 134693792 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 18134 16202 162 162 0 17972 0
[pid=32384] vsize: 72536
Current children cumulated CPU time (s) 829.17
Current children cumulated vsize (Kb) 74664

[startup+840.059 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 19779 0 0 0 83625 84 0 0 25 0 1 0 1796978769 74276864 16202 4294967295 134512640 135167914 3221224448 3221221404 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 18134 16202 162 162 0 17972 0
[pid=32384] vsize: 72536
Current children cumulated CPU time (s) 839.17
Current children cumulated vsize (Kb) 74664

[startup+850.061 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 19779 0 0 0 84625 84 0 0 25 0 1 0 1796978769 74276864 16202 4294967295 134512640 135167914 3221224448 3221221376 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 18134 16202 162 162 0 17972 0
[pid=32384] vsize: 72536
Current children cumulated CPU time (s) 849.17
Current children cumulated vsize (Kb) 74664

[startup+860.062 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 20041 0 0 0 85624 86 0 0 25 0 1 0 1796978769 74862592 16422 4294967295 134512640 135167914 3221224448 3221219356 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 18277 16422 162 162 0 18115 0
[pid=32384] vsize: 73108
Current children cumulated CPU time (s) 859.18
Current children cumulated vsize (Kb) 75236

[startup+870.063 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 20041 0 0 0 86624 86 0 0 25 0 1 0 1796978769 74862592 16422 4294967295 134512640 135167914 3221224448 3221220352 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 18277 16422 162 162 0 18115 0
[pid=32384] vsize: 73108
Current children cumulated CPU time (s) 869.18
Current children cumulated vsize (Kb) 75236

[startup+880.064 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 20041 0 0 0 87624 86 0 0 25 0 1 0 1796978769 74862592 16422 4294967295 134512640 135167914 3221224448 3221220940 134694320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 18277 16422 162 162 0 18115 0
[pid=32384] vsize: 73108
Current children cumulated CPU time (s) 879.18
Current children cumulated vsize (Kb) 75236

[startup+890.065 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 20041 0 0 0 88625 86 0 0 25 0 1 0 1796978769 74862592 16422 4294967295 134512640 135167914 3221224448 3221220048 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 18277 16422 162 162 0 18115 0
[pid=32384] vsize: 73108
Current children cumulated CPU time (s) 889.19
Current children cumulated vsize (Kb) 75236

[startup+900.066 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 20041 0 0 0 89625 86 0 0 25 0 1 0 1796978769 74862592 16422 4294967295 134512640 135167914 3221224448 3221220028 134722542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 18277 16422 162 162 0 18115 0
[pid=32384] vsize: 73108
Current children cumulated CPU time (s) 899.19
Current children cumulated vsize (Kb) 75236

[startup+910.067 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 20041 0 0 0 90625 86 0 0 25 0 1 0 1796978769 74862592 16422 4294967295 134512640 135167914 3221224448 3221221792 134522828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 18277 16422 162 162 0 18115 0
[pid=32384] vsize: 73108
Current children cumulated CPU time (s) 909.19
Current children cumulated vsize (Kb) 75236

[startup+920.067 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 20041 0 0 0 91625 86 0 0 25 0 1 0 1796978769 74862592 16422 4294967295 134512640 135167914 3221224448 3221221004 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 18277 16422 162 162 0 18115 0
[pid=32384] vsize: 73108
Current children cumulated CPU time (s) 919.19
Current children cumulated vsize (Kb) 75236

[startup+930.068 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 22943 0 0 0 92618 92 0 0 25 0 1 0 1796978769 80842752 17964 4294967295 134512640 135167914 3221224448 3221218716 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 19737 17964 162 162 0 19575 0
[pid=32384] vsize: 78948
Current children cumulated CPU time (s) 929.18
Current children cumulated vsize (Kb) 81076

[startup+940.069 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 22943 0 0 0 93619 92 0 0 25 0 1 0 1796978769 80842752 17964 4294967295 134512640 135167914 3221224448 3221220208 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 19737 17964 162 162 0 19575 0
[pid=32384] vsize: 78948
Current children cumulated CPU time (s) 939.19
Current children cumulated vsize (Kb) 81076

[startup+950.071 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 22943 0 0 0 94619 92 0 0 25 0 1 0 1796978769 80842752 17964 4294967295 134512640 135167914 3221224448 3221220760 134849057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 19737 17964 162 162 0 19575 0
[pid=32384] vsize: 78948
Current children cumulated CPU time (s) 949.19
Current children cumulated vsize (Kb) 81076

[startup+960.072 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 22943 0 0 0 95619 92 0 0 25 0 1 0 1796978769 80842752 17964 4294967295 134512640 135167914 3221224448 3221219872 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 19737 17964 162 162 0 19575 0
[pid=32384] vsize: 78948
Current children cumulated CPU time (s) 959.19
Current children cumulated vsize (Kb) 81076

[startup+970.072 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 22943 0 0 0 96620 92 0 0 25 0 1 0 1796978769 80842752 17964 4294967295 134512640 135167914 3221224448 3221220360 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 19737 17964 162 162 0 19575 0
[pid=32384] vsize: 78948
Current children cumulated CPU time (s) 969.2
Current children cumulated vsize (Kb) 81076

[startup+980.073 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 22943 0 0 0 97620 92 0 0 25 0 1 0 1796978769 80842752 17964 4294967295 134512640 135167914 3221224448 3221220720 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 19737 17964 162 162 0 19575 0
[pid=32384] vsize: 78948
Current children cumulated CPU time (s) 979.2
Current children cumulated vsize (Kb) 81076

[startup+990.074 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 22943 0 0 0 98620 92 0 0 25 0 1 0 1796978769 80842752 17964 4294967295 134512640 135167914 3221224448 3221221120 134630935 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 19737 17964 162 162 0 19575 0
[pid=32384] vsize: 78948
Current children cumulated CPU time (s) 989.2
Current children cumulated vsize (Kb) 81076

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23209 0 0 0 99619 93 0 0 25 0 1 0 1796978769 81424384 18188 4294967295 134512640 135167914 3221224448 3221219656 134845939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 19879 18188 162 162 0 19717 0
[pid=32384] vsize: 79516
Current children cumulated CPU time (s) 999.2
Current children cumulated vsize (Kb) 81644

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23209 0 0 0 100619 93 0 0 25 0 1 0 1796978769 81424384 18188 4294967295 134512640 135167914 3221224448 3221219904 134629448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 19879 18188 162 162 0 19717 0
[pid=32384] vsize: 79516
Current children cumulated CPU time (s) 1009.2
Current children cumulated vsize (Kb) 81644

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23209 0 0 0 101619 93 0 0 25 0 1 0 1796978769 81424384 18188 4294967295 134512640 135167914 3221224448 3221221108 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 19879 18188 162 162 0 19717 0
[pid=32384] vsize: 79516
Current children cumulated CPU time (s) 1019.2
Current children cumulated vsize (Kb) 81644

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23209 0 0 0 102620 93 0 0 25 0 1 0 1796978769 81424384 18188 4294967295 134512640 135167914 3221224448 3221220508 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 19879 18188 162 162 0 19717 0
[pid=32384] vsize: 79516
Current children cumulated CPU time (s) 1029.21
Current children cumulated vsize (Kb) 81644

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23209 0 0 0 103620 93 0 0 25 0 1 0 1796978769 81424384 18188 4294967295 134512640 135167914 3221224448 3221220920 134722657 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 19879 18188 162 162 0 19717 0
[pid=32384] vsize: 79516
Current children cumulated CPU time (s) 1039.21
Current children cumulated vsize (Kb) 81644

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23209 0 0 0 104620 93 0 0 25 0 1 0 1796978769 81424384 18188 4294967295 134512640 135167914 3221224448 3221221264 134694545 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 19879 18188 162 162 0 19717 0
[pid=32384] vsize: 79516
Current children cumulated CPU time (s) 1049.21
Current children cumulated vsize (Kb) 81644

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23209 0 0 0 105620 93 0 0 25 0 1 0 1796978769 81424384 18188 4294967295 134512640 135167914 3221224448 3221220560 134843015 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 19879 18188 162 162 0 19717 0
[pid=32384] vsize: 79516
Current children cumulated CPU time (s) 1059.21
Current children cumulated vsize (Kb) 81644

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23429 0 0 0 106618 95 0 0 25 0 1 0 1796978769 82006016 18408 4294967295 134512640 135167914 3221224448 3221218736 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 20021 18408 162 162 0 19859 0
[pid=32384] vsize: 80084
Current children cumulated CPU time (s) 1069.21
Current children cumulated vsize (Kb) 82212

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23429 0 0 0 107619 95 0 0 25 0 1 0 1796978769 82006016 18408 4294967295 134512640 135167914 3221224448 3221219792 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 20021 18408 162 162 0 19859 0
[pid=32384] vsize: 80084
Current children cumulated CPU time (s) 1079.22
Current children cumulated vsize (Kb) 82212

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23429 0 0 0 108619 95 0 0 25 0 1 0 1796978769 82006016 18408 4294967295 134512640 135167914 3221224448 3221221104 134693570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 20021 18408 162 162 0 19859 0
[pid=32384] vsize: 80084
Current children cumulated CPU time (s) 1089.22
Current children cumulated vsize (Kb) 82212

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23429 0 0 0 109619 95 0 0 25 0 1 0 1796978769 82006016 18408 4294967295 134512640 135167914 3221224448 3221221616 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 20021 18408 162 162 0 19859 0
[pid=32384] vsize: 80084
Current children cumulated CPU time (s) 1099.22
Current children cumulated vsize (Kb) 82212

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23429 0 0 0 110620 95 0 0 25 0 1 0 1796978769 82006016 18408 4294967295 134512640 135167914 3221224448 3221221804 134696182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 20021 18408 162 162 0 19859 0
[pid=32384] vsize: 80084
Current children cumulated CPU time (s) 1109.23
Current children cumulated vsize (Kb) 82212

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23429 0 0 0 111620 95 0 0 25 0 1 0 1796978769 82006016 18408 4294967295 134512640 135167914 3221224448 3221220928 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 20021 18408 162 162 0 19859 0
[pid=32384] vsize: 80084
Current children cumulated CPU time (s) 1119.23
Current children cumulated vsize (Kb) 82212

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23581 0 0 0 112619 95 0 0 25 0 1 0 1796978769 82288640 18518 4294967295 134512640 135167914 3221224448 3221219520 134694345 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 20090 18518 162 162 0 19928 0
[pid=32384] vsize: 80360
Current children cumulated CPU time (s) 1129.22
Current children cumulated vsize (Kb) 82488

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23581 0 0 0 113619 95 0 0 25 0 1 0 1796978769 82288640 18518 4294967295 134512640 135167914 3221224448 3221220348 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 20090 18518 162 162 0 19928 0
[pid=32384] vsize: 80360
Current children cumulated CPU time (s) 1139.22
Current children cumulated vsize (Kb) 82488

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23581 0 0 0 114619 95 0 0 25 0 1 0 1796978769 82288640 18518 4294967295 134512640 135167914 3221224448 3221219840 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 20090 18518 162 162 0 19928 0
[pid=32384] vsize: 80360
Current children cumulated CPU time (s) 1149.22
Current children cumulated vsize (Kb) 82488

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23581 0 0 0 115620 95 0 0 25 0 1 0 1796978769 82288640 18518 4294967295 134512640 135167914 3221224448 3221221024 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 20090 18518 162 162 0 19928 0
[pid=32384] vsize: 80360
Current children cumulated CPU time (s) 1159.23
Current children cumulated vsize (Kb) 82488

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23581 0 0 0 116620 95 0 0 25 0 1 0 1796978769 82288640 18518 4294967295 134512640 135167914 3221224448 3221221804 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 20090 18518 162 162 0 19928 0
[pid=32384] vsize: 80360
Current children cumulated CPU time (s) 1169.23
Current children cumulated vsize (Kb) 82488

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23581 0 0 0 117620 95 0 0 25 0 1 0 1796978769 82288640 18518 4294967295 134512640 135167914 3221224448 3221219984 134696656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 20090 18518 162 162 0 19928 0
[pid=32384] vsize: 80360
Current children cumulated CPU time (s) 1179.23
Current children cumulated vsize (Kb) 82488

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23581 0 0 0 118620 95 0 0 25 0 1 0 1796978769 82288640 18518 4294967295 134512640 135167914 3221224448 3221219728 134844715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 20090 18518 162 162 0 19928 0
[pid=32384] vsize: 80360
Current children cumulated CPU time (s) 1189.23
Current children cumulated vsize (Kb) 82488

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23581 0 0 0 119621 95 0 0 25 0 1 0 1796978769 82288640 18518 4294967295 134512640 135167914 3221224448 3221220960 134844703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 20090 18518 162 162 0 19928 0
[pid=32384] vsize: 80360
Current children cumulated CPU time (s) 1199.24
Current children cumulated vsize (Kb) 82488

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23822 0 0 0 120619 96 0 0 25 0 1 0 1796978769 82800640 18717 4294967295 134512640 135167914 3221224448 3221221056 134695307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 20215 18717 162 162 0 20053 0
[pid=32384] vsize: 80860
Current children cumulated CPU time (s) 1209.23
Current children cumulated vsize (Kb) 82988



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 32384
Raw data (/proc/32379/stat): 32379 (minisat+_script) S 32378 32379 9854 0 -1 0 314 6098 0 0 0 0 180 28 18 0 1 0 1796978533 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32379/statm): 532 234 485 147 0 385 0
[pid=32379] vsize: 2128
Raw data (/proc/32384/stat): 32384 (minisat+_bignum) R 32379 32379 9854 0 -1 0 23822 0 0 0 120619 96 0 0 25 0 1 0 1796978769 82800640 18717 4294967295 134512640 135167914 3221224448 3221221112 134693737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32384/statm): 20215 18717 162 162 0 20053 0
[pid=32384] vsize: 80860
Current children cumulated CPU time (s) 1209.23
Current children cumulated vsize (Kb) 82988

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

Child status: 0
Real time (s): 1210.13
CPU time (s): 1207.2
CPU user time (s): 1206.2
CPU system time (s): 1.00585
CPU usage (%): 99.758
Max. virtual memory (cumulated for all children) (Kb): 82988

Verifier Data

ERROR: no interpretation found !