Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-misc04.opb
MD5SUM7b42190d864979953c47e5a92736f365
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 31
Biggest coefficient in the objective function 1073741824
Number of bits for the biggest coefficient in the objective function 31
Sum of the numbers in the objective function 2147483647
Number of bits of the sum of numbers in the objective function 31
Biggest number in a constraint 43188899594881916928
Number of bits of the biggest number in a constraint 66
Biggest sum of numbers in a constraint 133861748414790074368
Number of bits of the biggest sum of numbers67
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables146276
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 constraint5071

Trace number 3868

Launcher Data

LAUNCH ON wulflinc21 THE 2005-09-19 03:08:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2864 boxname=wulflinc21 idbench=520 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7b42190d864979953c47e5a92736f365  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-misc04.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-misc04.opb
IDLAUNCH: 2864
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        892424 kB
Buffers:         30232 kB
Cached:          84352 kB
SwapCached:        812 kB
Active:          57848 kB
Inactive:        59376 kB
HighTotal:      131008 kB
HighFree:        43624 kB
LowTotal:       903652 kB
LowFree:        848800 kB
SwapTotal:     2097892 kB
SwapFree:      2096476 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5804 kB
Slab:            19320 kB
Committed_AS:    64368 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 03:28:49 (client local time) WITH STATUS 0 IN 1205.65 SECONDS
stats: 2864 7 1205.65 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: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1999]---> Sorter-cost: 2992     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5
c ---[1998]---> Sorter-cost: 2992     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5
c ---[1997]---> Sorter-cost: 2992     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5
c ---[1996]---> Sorter-cost: 2992     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5
c ---[1995]---> Sorter-cost: 2590     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5
c ---[1994]---> Sorter-cost: 2590     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5
c ---[1993]---> Sorter-cost: 2590     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5
c ---[1992]---> Sorter-cost: 2590     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5
c ---[1991]---> Sorter-cost: 1116     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[1990]---> Sorter-cost: 1116     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[1989]---> Sorter-cost: 1116     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[1988]---> Sorter-cost: 1116     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[1987]---> Sorter-cost: 1116     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[1986]---> Sorter-cost: 1116     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[1985]---> Sorter-cost: 1116     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[1984]---> Sorter-cost: 1116     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[1983]---> Sorter-cost: 1086     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[1982]---> Sorter-cost: 1086     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[1981]---> Sorter-cost: 1086     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[1980]---> Sorter-cost: 1086     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[1979]---> Adder-cost: 608   maxlim: 1212396   bits: 21/21
c ---[1978]---> Adder-cost: 608   maxlim: 1212396   bits: 21/21
c ---[1977]---> Adder-cost: 608   maxlim: 1212396   bits: 21/21
c ---[1976]---> Adder-cost: 608   maxlim: 1212396   bits: 21/21
c ---[1975]---> Adder-cost: 608   maxlim: 1212396   bits: 21/21
c ---[1974]---> Adder-cost: 608   maxlim: 1212396   bits: 21/21
c ---[1973]---> Adder-cost: 608   maxlim: 1212396   bits: 21/21
c ---[1972]---> Adder-cost: 608   maxlim: 1212396   bits: 21/21
c ---[1971]---> Adder-cost: 570   maxlim: 606188   bits: 20/20
c ---[1970]---> Adder-cost: 570   maxlim: 606188   bits: 20/20
c ---[1969]---> Adder-cost: 570   maxlim: 606188   bits: 20/20
c ---[1968]---> Adder-cost: 570   maxlim: 606188   bits: 20/20
c ---[1967]---> Sorter-cost:27397     Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1966]---> Sorter-cost:27397     Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1965]---> Sorter-cost:27454     Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1964]---> Sorter-cost:27454     Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1963]---> Sorter-cost: 4322     Base: 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1962]---> Sorter-cost: 4322     Base: 2 2 2 2 2 5

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/1766/stat): 1766 (minisat+_script) R 1765 1766 20602 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1723807946 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/1766/statm): 174 3 169 147 0 27 0
[pid=1766] 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=1767
New process pid=1768
New process pid=1769
execve syscall for /bin/sed executable
One traced child (pid=1768) 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=1769) exited with status: 0
One traced child (pid=1767) exited with status: 0
New process pid=1770
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-misc04.opb
One traced child (pid=1770) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=1771
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-misc04.opb

[startup+10.0026 s]
Raw data (loadavg): 0.99 1.13 1.10 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 3685 0 0 0 613 18 0 0 25 0 1 0 1723808300 18980864 3523 4294967295 134512640 135167914 3221224448 3221222912 134590353 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1771/statm): 4634 3523 162 162 0 4472 0
[pid=1771] vsize: 18536
Current children cumulated CPU time (s) 9.42
Current children cumulated vsize (Kb) 20664

[startup+20.0033 s]
Raw data (loadavg): 0.99 1.12 1.10 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 7226 0 0 0 1568 42 0 0 25 0 1 0 1723808300 30240768 6899 4294967295 134512640 135167914 3221224448 3221220944 134849143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1771/statm): 7383 6899 162 162 0 7221 0
[pid=1771] vsize: 29532
Current children cumulated CPU time (s) 19.21
Current children cumulated vsize (Kb) 31660

[startup+30.004 s]
Raw data (loadavg): 0.99 1.12 1.09 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 10313 0 0 0 2526 61 0 0 25 0 1 0 1723808300 50102272 9951 4294967295 134512640 135167914 3221224448 3221223184 134845927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1771/statm): 12232 9951 162 162 0 12070 0
[pid=1771] vsize: 48928
Current children cumulated CPU time (s) 28.98
Current children cumulated vsize (Kb) 51056

[startup+40.0046 s]
Raw data (loadavg): 0.99 1.12 1.09 1/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) T 1766 1766 20602 0 -1 0 14627 0 0 0 3482 83 0 0 20 0 1 0 1723808300 59383808 12248 4294967295 134512640 135167914 3221224448 3221222540 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/1771/statm): 14498 12248 162 162 0 14336 0
[pid=1771] vsize: 57992
Current children cumulated CPU time (s) 38.76
Current children cumulated vsize (Kb) 60120

[startup+50.0053 s]
Raw data (loadavg): 0.99 1.11 1.09 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 18766 0 0 0 4448 100 0 0 25 0 1 0 1723808300 71127040 15145 4294967295 134512640 135167914 3221224448 3221223296 134594196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1771/statm): 17365 15145 162 162 0 17203 0
[pid=1771] vsize: 69460
Current children cumulated CPU time (s) 48.59
Current children cumulated vsize (Kb) 71588

[startup+60.006 s]
Raw data (loadavg): 0.99 1.11 1.09 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 18766 0 0 0 5448 100 0 0 25 0 1 0 1723808300 71127040 15145 4294967295 134512640 135167914 3221224448 3221223296 134594248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1771/statm): 17365 15145 162 162 0 17203 0
[pid=1771] vsize: 69460
Current children cumulated CPU time (s) 58.59
Current children cumulated vsize (Kb) 71588

[startup+70.0057 s]
Raw data (loadavg): 0.99 1.10 1.09 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 18766 0 0 0 6447 100 0 0 25 0 1 0 1723808300 71127040 15145 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1771/statm): 17365 15145 162 162 0 17203 0
[pid=1771] vsize: 69460
Current children cumulated CPU time (s) 68.58
Current children cumulated vsize (Kb) 71588

[startup+80.0064 s]
Raw data (loadavg): 0.99 1.10 1.09 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 18766 0 0 0 7447 101 0 0 25 0 1 0 1723808300 71127040 15145 4294967295 134512640 135167914 3221224448 3221223204 134697161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1771/statm): 17365 15145 162 162 0 17203 0
[pid=1771] vsize: 69460
Current children cumulated CPU time (s) 78.59
Current children cumulated vsize (Kb) 71588

[startup+90.0071 s]
Raw data (loadavg): 0.99 1.10 1.09 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 18767 0 0 0 8446 101 0 0 25 0 1 0 1723808300 71127040 15146 4294967295 134512640 135167914 3221224448 3221223216 134691372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1771/statm): 17365 15146 162 162 0 17203 0
[pid=1771] vsize: 69460
Current children cumulated CPU time (s) 88.58
Current children cumulated vsize (Kb) 71588

[startup+100.008 s]
Raw data (loadavg): 0.99 1.09 1.08 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 18767 0 0 0 9446 102 0 0 25 0 1 0 1723808300 71127040 15146 4294967295 134512640 135167914 3221224448 3221223204 134697076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1771/statm): 17365 15146 162 162 0 17203 0
[pid=1771] vsize: 69460
Current children cumulated CPU time (s) 98.59
Current children cumulated vsize (Kb) 71588

[startup+110.008 s]
Raw data (loadavg): 0.99 1.09 1.08 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 18780 0 0 0 10446 102 0 0 25 0 1 0 1723808300 67616768 14301 4294967295 134512640 135167914 3221224448 3221220892 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1771/statm): 16508 14301 162 162 0 16346 0
[pid=1771] vsize: 66032
Current children cumulated CPU time (s) 108.59
Current children cumulated vsize (Kb) 68160

[startup+120.009 s]
Raw data (loadavg): 0.99 1.08 1.08 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 18780 0 0 0 11445 103 0 0 25 0 1 0 1723808300 67616768 14301 4294967295 134512640 135167914 3221224448 3221220832 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1771/statm): 16508 14301 162 162 0 16346 0
[pid=1771] vsize: 66032
Current children cumulated CPU time (s) 118.59
Current children cumulated vsize (Kb) 68160

[startup+130.01 s]
Raw data (loadavg): 0.99 1.08 1.08 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 19227 0 0 0 12444 104 0 0 25 0 1 0 1723808300 69234688 14665 4294967295 134512640 135167914 3221224448 3221060376 134845877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1771/statm): 16903 14665 162 162 0 16741 0
[pid=1771] vsize: 67612
Current children cumulated CPU time (s) 128.59
Current children cumulated vsize (Kb) 69740

[startup+140.01 s]
Raw data (loadavg): 0.99 1.08 1.08 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 19294 0 0 0 13443 105 0 0 25 0 1 0 1723808300 69509120 14732 4294967295 134512640 135167914 3221224448 3221222844 134845940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1771/statm): 16970 14732 162 162 0 16808 0
[pid=1771] vsize: 67880
Current children cumulated CPU time (s) 138.59
Current children cumulated vsize (Kb) 70008

[startup+150.012 s]
Raw data (loadavg): 0.99 1.08 1.08 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 19502 0 0 0 14441 106 0 0 25 0 1 0 1723808300 70832128 14940 4294967295 134512640 135167914 3221224448 3221221816 134849057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1771/statm): 17293 14940 162 162 0 17131 0
[pid=1771] vsize: 69172
Current children cumulated CPU time (s) 148.58
Current children cumulated vsize (Kb) 71300

[startup+160.013 s]
Raw data (loadavg): 0.99 1.07 1.08 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 20056 0 0 0 15439 108 0 0 25 0 1 0 1723808300 72097792 15329 4294967295 134512640 135167914 3221224448 3221219648 134695307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1771/statm): 17602 15329 162 162 0 17440 0
[pid=1771] vsize: 70408
Current children cumulated CPU time (s) 158.58
Current children cumulated vsize (Kb) 72536

[startup+170.014 s]
Raw data (loadavg): 0.99 1.07 1.08 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 20279 0 0 0 16438 108 0 0 25 0 1 0 1723808300 74252288 15552 4294967295 134512640 135167914 3221224448 3221222464 134695269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1771/statm): 18128 15552 162 162 0 17966 0
[pid=1771] vsize: 72512
Current children cumulated CPU time (s) 168.57
Current children cumulated vsize (Kb) 74640

[startup+180.014 s]
Raw data (loadavg): 0.99 1.07 1.08 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 20494 0 0 0 17436 110 0 0 25 0 1 0 1723808300 74743808 15767 4294967295 134512640 135167914 3221224448 3221222256 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1771/statm): 18248 15767 162 162 0 18086 0
[pid=1771] vsize: 72992
Current children cumulated CPU time (s) 178.57
Current children cumulated vsize (Kb) 75120

[startup+190.015 s]
Raw data (loadavg): 0.99 1.06 1.08 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21229 0 0 0 18435 111 0 0 25 0 1 0 1723808300 76279808 16172 4294967295 134512640 135167914 3221224448 3221219804 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18623 16172 162 162 0 18461 0
[pid=1771] vsize: 74492
Current children cumulated CPU time (s) 188.57
Current children cumulated vsize (Kb) 76620

[startup+200.016 s]
Raw data (loadavg): 0.99 1.06 1.08 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21229 0 0 0 19435 111 0 0 25 0 1 0 1723808300 76279808 16172 4294967295 134512640 135167914 3221224448 3221220496 134844691 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18623 16172 162 162 0 18461 0
[pid=1771] vsize: 74492
Current children cumulated CPU time (s) 198.57
Current children cumulated vsize (Kb) 76620

[startup+210.016 s]
Raw data (loadavg): 0.99 1.06 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21229 0 0 0 20435 111 0 0 25 0 1 0 1723808300 76279808 16172 4294967295 134512640 135167914 3221224448 3221220528 134522502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18623 16172 162 162 0 18461 0
[pid=1771] vsize: 74492
Current children cumulated CPU time (s) 208.57
Current children cumulated vsize (Kb) 76620

[startup+220.017 s]
Raw data (loadavg): 0.99 1.06 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21276 0 0 0 21435 111 0 0 25 0 1 0 1723808300 76402688 16219 4294967295 134512640 135167914 3221224448 3221218988 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18653 16219 162 162 0 18491 0
[pid=1771] vsize: 74612
Current children cumulated CPU time (s) 218.57
Current children cumulated vsize (Kb) 76740

[startup+230.018 s]
Raw data (loadavg): 0.99 1.05 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21276 0 0 0 22435 111 0 0 25 0 1 0 1723808300 76402688 16219 4294967295 134512640 135167914 3221224448 3221220744 134722657 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18653 16219 162 162 0 18491 0
[pid=1771] vsize: 74612
Current children cumulated CPU time (s) 228.57
Current children cumulated vsize (Kb) 76740

[startup+240.018 s]
Raw data (loadavg): 0.99 1.05 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21276 0 0 0 23436 111 0 0 25 0 1 0 1723808300 76402688 16219 4294967295 134512640 135167914 3221224448 3221222120 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18653 16219 162 162 0 18491 0
[pid=1771] vsize: 74612
Current children cumulated CPU time (s) 238.58
Current children cumulated vsize (Kb) 76740

[startup+250.019 s]
Raw data (loadavg): 0.99 1.05 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21324 0 0 0 24436 112 0 0 25 0 1 0 1723808300 76525568 16267 4294967295 134512640 135167914 3221224448 3221218944 134522502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18683 16267 162 162 0 18521 0
[pid=1771] vsize: 74732
Current children cumulated CPU time (s) 248.59
Current children cumulated vsize (Kb) 76860

[startup+260.02 s]
Raw data (loadavg): 0.99 1.05 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21324 0 0 0 25436 112 0 0 25 0 1 0 1723808300 76525568 16267 4294967295 134512640 135167914 3221224448 3221220576 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18683 16267 162 162 0 18521 0
[pid=1771] vsize: 74732
Current children cumulated CPU time (s) 258.59
Current children cumulated vsize (Kb) 76860

[startup+270.019 s]
Raw data (loadavg): 0.99 1.05 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21371 0 0 0 26436 112 0 0 25 0 1 0 1723808300 76648448 16314 4294967295 134512640 135167914 3221224448 3221218384 134844736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18713 16314 162 162 0 18551 0
[pid=1771] vsize: 74852
Current children cumulated CPU time (s) 268.59
Current children cumulated vsize (Kb) 76980

[startup+280.02 s]
Raw data (loadavg): 0.99 1.04 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21371 0 0 0 27436 112 0 0 25 0 1 0 1723808300 76648448 16314 4294967295 134512640 135167914 3221224448 3221219680 134843400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18713 16314 162 162 0 18551 0
[pid=1771] vsize: 74852
Current children cumulated CPU time (s) 278.59
Current children cumulated vsize (Kb) 76980

[startup+290.021 s]
Raw data (loadavg): 0.99 1.04 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21371 0 0 0 28436 112 0 0 25 0 1 0 1723808300 76648448 16314 4294967295 134512640 135167914 3221224448 3221220236 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18713 16314 162 162 0 18551 0
[pid=1771] vsize: 74852
Current children cumulated CPU time (s) 288.59
Current children cumulated vsize (Kb) 76980

[startup+300.021 s]
Raw data (loadavg): 1.07 1.06 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21473 0 0 0 29436 112 0 0 25 0 1 0 1723808300 76910592 16416 4294967295 134512640 135167914 3221224448 3221218780 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18777 16416 162 162 0 18615 0
[pid=1771] vsize: 75108
Current children cumulated CPU time (s) 298.59
Current children cumulated vsize (Kb) 77236

[startup+310.022 s]
Raw data (loadavg): 1.14 1.07 1.08 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21473 0 0 0 30436 112 0 0 25 0 1 0 1723808300 76910592 16416 4294967295 134512640 135167914 3221224448 3221218632 134722657 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18777 16416 162 162 0 18615 0
[pid=1771] vsize: 75108
Current children cumulated CPU time (s) 308.59
Current children cumulated vsize (Kb) 77236

[startup+320.022 s]
Raw data (loadavg): 1.11 1.07 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21473 0 0 0 31436 112 0 0 25 0 1 0 1723808300 76910592 16416 4294967295 134512640 135167914 3221224448 3221221856 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18777 16416 162 162 0 18615 0
[pid=1771] vsize: 75108
Current children cumulated CPU time (s) 318.59
Current children cumulated vsize (Kb) 77236

[startup+330.022 s]
Raw data (loadavg): 1.10 1.07 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21503 0 0 0 32436 112 0 0 25 0 1 0 1723808300 76984320 16446 4294967295 134512640 135167914 3221224448 3221222460 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18795 16446 162 162 0 18633 0
[pid=1771] vsize: 75180
Current children cumulated CPU time (s) 328.59
Current children cumulated vsize (Kb) 77308

[startup+340.022 s]
Raw data (loadavg): 1.08 1.06 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21540 0 0 0 33437 112 0 0 25 0 1 0 1723808300 77078528 16483 4294967295 134512640 135167914 3221224448 3221221088 134843064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18818 16483 162 162 0 18656 0
[pid=1771] vsize: 75272
Current children cumulated CPU time (s) 338.6
Current children cumulated vsize (Kb) 77400

[startup+350.023 s]
Raw data (loadavg): 1.07 1.06 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21710 0 0 0 34436 113 0 0 25 0 1 0 1723808300 77545472 16653 4294967295 134512640 135167914 3221224448 3221221120 134630751 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18932 16653 162 162 0 18770 0
[pid=1771] vsize: 75728
Current children cumulated CPU time (s) 348.6
Current children cumulated vsize (Kb) 77856

[startup+360.024 s]
Raw data (loadavg): 1.06 1.06 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21714 0 0 0 35436 113 0 0 25 0 1 0 1723808300 77545472 16657 4294967295 134512640 135167914 3221224448 3221221816 134849057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18932 16657 162 162 0 18770 0
[pid=1771] vsize: 75728
Current children cumulated CPU time (s) 358.6
Current children cumulated vsize (Kb) 77856

[startup+370.023 s]
Raw data (loadavg): 1.05 1.06 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21788 0 0 0 36436 113 0 0 25 0 1 0 1723808300 77729792 16731 4294967295 134512640 135167914 3221224448 3221218064 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18977 16731 162 162 0 18815 0
[pid=1771] vsize: 75908
Current children cumulated CPU time (s) 368.6
Current children cumulated vsize (Kb) 78036

[startup+380.024 s]
Raw data (loadavg): 1.04 1.05 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21788 0 0 0 37436 113 0 0 25 0 1 0 1723808300 77729792 16731 4294967295 134512640 135167914 3221224448 3221221756 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 18977 16731 162 162 0 18815 0
[pid=1771] vsize: 75908
Current children cumulated CPU time (s) 378.6
Current children cumulated vsize (Kb) 78036

[startup+390.024 s]
Raw data (loadavg): 1.03 1.05 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 21869 0 0 0 38436 113 0 0 25 0 1 0 1723808300 77938688 16812 4294967295 134512640 135167914 3221224448 3221221824 134629248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 19028 16812 162 162 0 18866 0
[pid=1771] vsize: 76112
Current children cumulated CPU time (s) 388.6
Current children cumulated vsize (Kb) 78240

[startup+400.024 s]
Raw data (loadavg): 1.03 1.05 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 22157 0 0 0 39433 115 0 0 25 0 1 0 1723808300 81915904 17058 4294967295 134512640 135167914 3221224448 3221219132 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 19999 17058 162 162 0 19837 0
[pid=1771] vsize: 79996
Current children cumulated CPU time (s) 398.59
Current children cumulated vsize (Kb) 82124

[startup+410.025 s]
Raw data (loadavg): 1.02 1.05 1.07 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 22157 0 0 0 40433 115 0 0 25 0 1 0 1723808300 81915904 17058 4294967295 134512640 135167914 3221224448 3221219984 134696194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 19999 17058 162 162 0 19837 0
[pid=1771] vsize: 79996
Current children cumulated CPU time (s) 408.59
Current children cumulated vsize (Kb) 82124

[startup+420.025 s]
Raw data (loadavg): 1.02 1.05 1.06 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 22157 0 0 0 41433 115 0 0 25 0 1 0 1723808300 81915904 17058 4294967295 134512640 135167914 3221224448 3221219632 134723229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 19999 17058 162 162 0 19837 0
[pid=1771] vsize: 79996
Current children cumulated CPU time (s) 418.59
Current children cumulated vsize (Kb) 82124

[startup+430.025 s]
Raw data (loadavg): 1.02 1.04 1.06 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 22157 0 0 0 42434 115 0 0 25 0 1 0 1723808300 81915904 17058 4294967295 134512640 135167914 3221224448 3221219888 134629123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 19999 17058 162 162 0 19837 0
[pid=1771] vsize: 79996
Current children cumulated CPU time (s) 428.6
Current children cumulated vsize (Kb) 82124

[startup+440.026 s]
Raw data (loadavg): 1.01 1.04 1.06 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 22157 0 0 0 43434 115 0 0 25 0 1 0 1723808300 81915904 17058 4294967295 134512640 135167914 3221224448 3221219680 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 19999 17058 162 162 0 19837 0
[pid=1771] vsize: 79996
Current children cumulated CPU time (s) 438.6
Current children cumulated vsize (Kb) 82124

[startup+450.027 s]
Raw data (loadavg): 1.01 1.04 1.06 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 22157 0 0 0 44434 115 0 0 25 0 1 0 1723808300 81915904 17058 4294967295 134512640 135167914 3221224448 3221222360 134629265 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 19999 17058 162 162 0 19837 0
[pid=1771] vsize: 79996
Current children cumulated CPU time (s) 448.6
Current children cumulated vsize (Kb) 82124

[startup+460.027 s]
Raw data (loadavg): 1.01 1.04 1.06 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 22477 0 0 0 45432 116 0 0 25 0 1 0 1723808300 82685952 17336 4294967295 134512640 135167914 3221224448 3221219792 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 20187 17336 162 162 0 20025 0
[pid=1771] vsize: 80748
Current children cumulated CPU time (s) 458.59
Current children cumulated vsize (Kb) 82876

[startup+470.028 s]
Raw data (loadavg): 1.01 1.04 1.06 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 22477 0 0 0 46433 116 0 0 25 0 1 0 1723808300 82685952 17336 4294967295 134512640 135167914 3221224448 3221221388 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 20187 17336 162 162 0 20025 0
[pid=1771] vsize: 80748
Current children cumulated CPU time (s) 468.6
Current children cumulated vsize (Kb) 82876

[startup+480.029 s]
Raw data (loadavg): 1.00 1.03 1.06 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 22477 0 0 0 47433 116 0 0 25 0 1 0 1723808300 82685952 17336 4294967295 134512640 135167914 3221224448 3221220768 134630875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 20187 17336 162 162 0 20025 0
[pid=1771] vsize: 80748
Current children cumulated CPU time (s) 478.6
Current children cumulated vsize (Kb) 82876

[startup+490.028 s]
Raw data (loadavg): 1.00 1.03 1.06 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 22477 0 0 0 48433 116 0 0 25 0 1 0 1723808300 82685952 17336 4294967295 134512640 135167914 3221224448 3221220144 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 20187 17336 162 162 0 20025 0
[pid=1771] vsize: 80748
Current children cumulated CPU time (s) 488.6
Current children cumulated vsize (Kb) 82876

[startup+500.03 s]
Raw data (loadavg): 1.00 1.03 1.06 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 22477 0 0 0 49433 116 0 0 25 0 1 0 1723808300 82685952 17336 4294967295 134512640 135167914 3221224448 3221221780 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 20187 17336 162 162 0 20025 0
[pid=1771] vsize: 80748
Current children cumulated CPU time (s) 498.6
Current children cumulated vsize (Kb) 82876

[startup+510.031 s]
Raw data (loadavg): 1.00 1.03 1.06 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 24133 0 0 0 50429 120 0 0 25 0 1 0 1723808300 86151168 18291 4294967295 134512640 135167914 3221224448 3221218752 134849061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21033 18291 162 162 0 20871 0
[pid=1771] vsize: 84132
Current children cumulated CPU time (s) 508.6
Current children cumulated vsize (Kb) 86260

[startup+520.03 s]
Raw data (loadavg): 1.00 1.03 1.05 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 24133 0 0 0 51429 120 0 0 25 0 1 0 1723808300 86151168 18291 4294967295 134512640 135167914 3221224448 3221220160 134696611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21033 18291 162 162 0 20871 0
[pid=1771] vsize: 84132
Current children cumulated CPU time (s) 518.6
Current children cumulated vsize (Kb) 86260

[startup+530.031 s]
Raw data (loadavg): 1.00 1.03 1.05 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 24133 0 0 0 52429 120 0 0 25 0 1 0 1723808300 86151168 18291 4294967295 134512640 135167914 3221224448 3221219524 134849060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21033 18291 162 162 0 20871 0
[pid=1771] vsize: 84132
Current children cumulated CPU time (s) 528.6
Current children cumulated vsize (Kb) 86260

[startup+540.032 s]
Raw data (loadavg): 1.00 1.03 1.05 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 24133 0 0 0 53429 120 0 0 25 0 1 0 1723808300 86151168 18291 4294967295 134512640 135167914 3221224448 3221221084 134845940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21033 18291 162 162 0 20871 0
[pid=1771] vsize: 84132
Current children cumulated CPU time (s) 538.6
Current children cumulated vsize (Kb) 86260

[startup+550.033 s]
Raw data (loadavg): 1.00 1.02 1.05 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 24133 0 0 0 54430 120 0 0 25 0 1 0 1723808300 86151168 18291 4294967295 134512640 135167914 3221224448 3221221820 134694480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21033 18291 162 162 0 20871 0
[pid=1771] vsize: 84132
Current children cumulated CPU time (s) 548.61
Current children cumulated vsize (Kb) 86260

[startup+560.033 s]
Raw data (loadavg): 1.00 1.02 1.05 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 24133 0 0 0 55430 120 0 0 25 0 1 0 1723808300 86151168 18291 4294967295 134512640 135167914 3221224448 3221220144 134843130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21033 18291 162 162 0 20871 0
[pid=1771] vsize: 84132
Current children cumulated CPU time (s) 558.61
Current children cumulated vsize (Kb) 86260

[startup+570.034 s]
Raw data (loadavg): 1.00 1.02 1.05 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 24510 0 0 0 56428 121 0 0 25 0 1 0 1723808300 86913024 18587 4294967295 134512640 135167914 3221224448 3221218800 134849122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21219 18587 162 162 0 21057 0
[pid=1771] vsize: 84876
Current children cumulated CPU time (s) 568.6
Current children cumulated vsize (Kb) 87004

[startup+580.034 s]
Raw data (loadavg): 1.00 1.02 1.05 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 24510 0 0 0 57428 121 0 0 25 0 1 0 1723808300 86913024 18587 4294967295 134512640 135167914 3221224448 3221220688 134696578 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21219 18587 162 162 0 21057 0
[pid=1771] vsize: 84876
Current children cumulated CPU time (s) 578.6
Current children cumulated vsize (Kb) 87004

[startup+590.035 s]
Raw data (loadavg): 1.00 1.02 1.05 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 24510 0 0 0 58428 121 0 0 25 0 1 0 1723808300 86913024 18587 4294967295 134512640 135167914 3221224448 3221220784 134629196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21219 18587 162 162 0 21057 0
[pid=1771] vsize: 84876
Current children cumulated CPU time (s) 588.6
Current children cumulated vsize (Kb) 87004

[startup+600.037 s]
Raw data (loadavg): 1.00 1.02 1.05 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 24510 0 0 0 59429 121 0 0 25 0 1 0 1723808300 86913024 18587 4294967295 134512640 135167914 3221224448 3221220496 134843074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21219 18587 162 162 0 21057 0
[pid=1771] vsize: 84876
Current children cumulated CPU time (s) 598.61
Current children cumulated vsize (Kb) 87004

[startup+610.038 s]
Raw data (loadavg): 1.00 1.02 1.05 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 24510 0 0 0 60429 121 0 0 25 0 1 0 1723808300 86913024 18587 4294967295 134512640 135167914 3221224448 3221222192 134630843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21219 18587 162 162 0 21057 0
[pid=1771] vsize: 84876
Current children cumulated CPU time (s) 608.61
Current children cumulated vsize (Kb) 87004

[startup+620.039 s]
Raw data (loadavg): 1.00 1.02 1.04 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 24510 0 0 0 61429 121 0 0 25 0 1 0 1723808300 86913024 18587 4294967295 134512640 135167914 3221224448 3221219184 134629373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21219 18587 162 162 0 21057 0
[pid=1771] vsize: 84876
Current children cumulated CPU time (s) 618.61
Current children cumulated vsize (Kb) 87004

[startup+630.04 s]
Raw data (loadavg): 1.00 1.02 1.04 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 24826 0 0 0 62429 121 0 0 25 0 1 0 1723808300 87605248 18903 4294967295 134512640 135167914 3221224448 3221220848 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21388 18903 162 162 0 21226 0
[pid=1771] vsize: 85552
Current children cumulated CPU time (s) 628.61
Current children cumulated vsize (Kb) 87680

[startup+640.041 s]
Raw data (loadavg): 1.00 1.02 1.04 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 63425 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221218804 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 638.59
Current children cumulated vsize (Kb) 89068

[startup+650.041 s]
Raw data (loadavg): 1.00 1.02 1.04 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 64425 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221218912 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 648.59
Current children cumulated vsize (Kb) 89068

[startup+660.042 s]
Raw data (loadavg): 1.00 1.01 1.04 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 65426 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221219308 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 658.6
Current children cumulated vsize (Kb) 89068

[startup+670.043 s]
Raw data (loadavg): 1.00 1.01 1.04 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 66426 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221220048 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 668.6
Current children cumulated vsize (Kb) 89068

[startup+680.043 s]
Raw data (loadavg): 1.00 1.01 1.04 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 67426 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221220032 134694444 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 678.6
Current children cumulated vsize (Kb) 89068

[startup+690.043 s]
Raw data (loadavg): 1.00 1.01 1.04 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 68426 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221221024 134844694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 688.6
Current children cumulated vsize (Kb) 89068

[startup+700.044 s]
Raw data (loadavg): 1.00 1.01 1.04 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 69426 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221220036 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 698.6
Current children cumulated vsize (Kb) 89068

[startup+710.044 s]
Raw data (loadavg): 1.00 1.01 1.04 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 70427 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221219104 134696578 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 708.61
Current children cumulated vsize (Kb) 89068

[startup+720.045 s]
Raw data (loadavg): 1.00 1.01 1.04 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 71427 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221219488 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 718.61
Current children cumulated vsize (Kb) 89068

[startup+730.046 s]
Raw data (loadavg): 1.00 1.01 1.03 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 72427 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221218820 134522188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 728.61
Current children cumulated vsize (Kb) 89068

[startup+740.046 s]
Raw data (loadavg): 1.00 1.01 1.03 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 73427 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221220700 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 738.61
Current children cumulated vsize (Kb) 89068

[startup+750.047 s]
Raw data (loadavg): 1.00 1.01 1.03 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 74428 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221219840 134522839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 748.62
Current children cumulated vsize (Kb) 89068

[startup+760.048 s]
Raw data (loadavg): 1.00 1.00 1.03 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 75428 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221220232 134693553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 758.62
Current children cumulated vsize (Kb) 89068

[startup+770.048 s]
Raw data (loadavg): 1.00 1.00 1.03 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 76428 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221218780 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 768.62
Current children cumulated vsize (Kb) 89068

[startup+780.049 s]
Raw data (loadavg): 1.00 1.00 1.03 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 77428 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221221120 134630940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 778.62
Current children cumulated vsize (Kb) 89068

[startup+790.049 s]
Raw data (loadavg): 1.00 1.00 1.03 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 78429 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221218464 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 788.63
Current children cumulated vsize (Kb) 89068

[startup+800.05 s]
Raw data (loadavg): 1.00 1.00 1.03 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 79429 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221220144 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 798.63
Current children cumulated vsize (Kb) 89068

[startup+810.05 s]
Raw data (loadavg): 1.00 1.00 1.03 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 80429 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221218812 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 808.63
Current children cumulated vsize (Kb) 89068

[startup+820.05 s]
Raw data (loadavg): 1.00 1.00 1.03 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 81429 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221220752 134693561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 818.63
Current children cumulated vsize (Kb) 89068

[startup+830.051 s]
Raw data (loadavg): 1.00 1.00 1.02 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 82429 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221218944 134718497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 828.63
Current children cumulated vsize (Kb) 89068

[startup+840.051 s]
Raw data (loadavg): 1.00 1.00 1.02 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 83430 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221220032 134843420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 838.64
Current children cumulated vsize (Kb) 89068

[startup+850.052 s]
Raw data (loadavg): 1.00 1.00 1.02 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 84430 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221219888 134630853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 848.64
Current children cumulated vsize (Kb) 89068

[startup+860.053 s]
Raw data (loadavg): 1.00 1.00 1.02 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 85430 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221221024 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 858.64
Current children cumulated vsize (Kb) 89068

[startup+870.052 s]
Raw data (loadavg): 1.00 1.00 1.02 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 86430 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221218208 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 868.64
Current children cumulated vsize (Kb) 89068

[startup+880.053 s]
Raw data (loadavg): 1.00 1.00 1.02 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 87431 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221220128 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 878.65
Current children cumulated vsize (Kb) 89068

[startup+890.053 s]
Raw data (loadavg): 1.00 1.00 1.02 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 88431 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221220496 134696665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 888.65
Current children cumulated vsize (Kb) 89068

[startup+900.053 s]
Raw data (loadavg): 1.00 1.00 1.02 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 89431 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221218240 134695319 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 898.65
Current children cumulated vsize (Kb) 89068

[startup+910.054 s]
Raw data (loadavg): 1.00 1.00 1.02 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 90431 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221220224 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 908.65
Current children cumulated vsize (Kb) 89068

[startup+920.055 s]
Raw data (loadavg): 1.00 1.00 1.02 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25373 0 0 0 91431 123 0 0 25 0 1 0 1723808300 89026560 19287 4294967295 134512640 135167914 3221224448 3221222144 134849122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21735 19287 162 162 0 21573 0
[pid=1771] vsize: 86940
Current children cumulated CPU time (s) 918.65
Current children cumulated vsize (Kb) 89068

[startup+930.055 s]
Raw data (loadavg): 1.00 1.00 1.01 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25467 0 0 0 92431 123 0 0 25 0 1 0 1723808300 89034752 19381 4294967295 134512640 135167914 3221224448 3221023392 134695967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21737 19381 162 162 0 21575 0
[pid=1771] vsize: 86948
Current children cumulated CPU time (s) 928.65
Current children cumulated vsize (Kb) 89076

[startup+940.055 s]
Raw data (loadavg): 1.00 1.00 1.01 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 93429 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221218396 134723269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 938.65
Current children cumulated vsize (Kb) 90092

[startup+950.056 s]
Raw data (loadavg): 1.00 1.00 1.01 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 94429 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221218736 134696395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 948.65
Current children cumulated vsize (Kb) 90092

[startup+960.057 s]
Raw data (loadavg): 1.00 1.00 1.01 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 95429 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221219244 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 958.65
Current children cumulated vsize (Kb) 90092

[startup+970.056 s]
Raw data (loadavg): 1.00 1.00 1.01 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 96429 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221219792 134845918 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 968.65
Current children cumulated vsize (Kb) 90092

[startup+980.057 s]
Raw data (loadavg): 1.00 1.00 1.01 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 97430 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221218768 134695291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 978.66
Current children cumulated vsize (Kb) 90092

[startup+990.058 s]
Raw data (loadavg): 1.00 1.00 1.01 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 98430 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221219088 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 988.66
Current children cumulated vsize (Kb) 90092

[startup+1000.06 s]
Raw data (loadavg): 1.00 1.00 1.01 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 99430 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221218780 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 998.66
Current children cumulated vsize (Kb) 90092

[startup+1010.06 s]
Raw data (loadavg): 1.00 1.00 1.01 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 100430 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221218964 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1008.66
Current children cumulated vsize (Kb) 90092

[startup+1020.06 s]
Raw data (loadavg): 1.00 1.00 1.01 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 101431 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221219852 134845940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1018.67
Current children cumulated vsize (Kb) 90092

[startup+1030.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 102431 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221219200 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1028.67
Current children cumulated vsize (Kb) 90092

[startup+1040.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 103431 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221219880 134693737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1038.67
Current children cumulated vsize (Kb) 90092

[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 104431 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221220236 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1048.67
Current children cumulated vsize (Kb) 90092

[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 105432 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221220176 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1058.68
Current children cumulated vsize (Kb) 90092

[startup+1070.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 106432 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221217920 134843113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1068.68
Current children cumulated vsize (Kb) 90092

[startup+1080.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 107432 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221220496 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1078.68
Current children cumulated vsize (Kb) 90092

[startup+1090.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 108432 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221219316 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1088.68
Current children cumulated vsize (Kb) 90092

[startup+1100.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 109432 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221220684 134845940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1098.68
Current children cumulated vsize (Kb) 90092

[startup+1110.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 110433 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221218096 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1108.69
Current children cumulated vsize (Kb) 90092

[startup+1120.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 111433 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221220496 134696738 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1118.69
Current children cumulated vsize (Kb) 90092

[startup+1130.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 112433 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221221116 134693792 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1128.69
Current children cumulated vsize (Kb) 90092

[startup+1140.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 113433 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221219872 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1138.69
Current children cumulated vsize (Kb) 90092

[startup+1150.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 114434 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221219792 134844691 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1148.7
Current children cumulated vsize (Kb) 90092

[startup+1160.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 115434 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221219776 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1158.7
Current children cumulated vsize (Kb) 90092

[startup+1170.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 116434 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221220400 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1168.7
Current children cumulated vsize (Kb) 90092

[startup+1180.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 117434 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221220624 134844708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1178.7
Current children cumulated vsize (Kb) 90092

[startup+1190.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 118435 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221220144 134696298 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1188.71
Current children cumulated vsize (Kb) 90092

[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 119435 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221220348 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1198.71
Current children cumulated vsize (Kb) 90092

[startup+1210.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 120435 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221220672 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1208.71
Current children cumulated vsize (Kb) 90092



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/58 1771
Raw data (/proc/1766/stat): 1766 (minisat+_script) S 1765 1766 20602 0 -1 0 314 8607 0 0 0 0 265 46 18 0 1 0 1723807946 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1766/statm): 532 234 485 147 0 385 0
[pid=1766] vsize: 2128
Raw data (/proc/1771/stat): 1771 (minisat+_bignum) R 1766 1766 20602 0 -1 0 25888 0 0 0 120435 125 0 0 25 0 1 0 1723808300 90075136 19677 4294967295 134512640 135167914 3221224448 3221220744 134722657 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1771/statm): 21991 19677 162 162 0 21829 0
[pid=1771] vsize: 87964
Current children cumulated CPU time (s) 1208.71
Current children cumulated vsize (Kb) 90092

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

Child status: 0
Real time (s): 1210.11
CPU time (s): 1205.65
CPU user time (s): 1204.36
CPU system time (s): 1.2928
CPU usage (%): 99.6313
Max. virtual memory (cumulated for all children) (Kb): 90092

Verifier Data

ERROR: no interpretation found !