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/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-rail507.opb
MD5SUM3525728b1c2480586834886de2d50400
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 284672000000000
Optimality of the best value was proved NO
Number of terms in the objective function 63309
Biggest coefficient in the objective function 53687091200000000000
Number of bits for the biggest coefficient in the objective function 66
Sum of the numbers in the objective function 215947469635884908544
Number of bits of the sum of numbers in the objective function 68
Biggest number in a constraint 53687091200000000000
Number of bits of the biggest number in a constraint 66
Biggest sum of numbers in a constraint 215947469635884908544
Number of bits of the biggest sum of numbers68
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1234.36
Number of variables63009
Total number of constraints63518
Number of constraints which are clauses507
Number of constraints which are cardinality constraints (but not clauses)63011
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint59416

Trace number 5933

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        902380 kB
Buffers:         33112 kB
Cached:          68192 kB
SwapCached:        492 kB
Active:          50192 kB
Inactive:        53660 kB
HighTotal:      131008 kB
HighFree:        60592 kB
LowTotal:       903652 kB
LowFree:        841788 kB
SwapTotal:     2097136 kB
SwapFree:      2096072 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5884 kB
Slab:            22600 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 02:30:03 (client local time) WITH STATUS 0 IN 1208.33 SECONDS
stats: 3111 7 1208.33 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 63023] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...

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/9553/stat): 9553 (minisat+_script) R 9552 9553 8263 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1796586986 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/9553/statm): 174 3 169 147 0 27 0
[pid=9553] 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=9554
New process pid=9555
New process pid=9556
execve syscall for /bin/sed executable
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
One traced child (pid=9555) exited with status: 0
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=9556) exited with status: 0
One traced child (pid=9554) exited with status: 0
New process pid=9557
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-rail507.opb
One traced child (pid=9557) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=9558
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-rail507.opb

[startup+10.0042 s]
Raw data (loadavg): 0.88 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 3403 0 0 0 865 24 0 0 25 0 1 0 1796587067 13893632 3202 4294967295 134512640 135167914 3221224448 3221219792 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 3392 3202 162 162 0 3230 0
[pid=9558] vsize: 13568
Current children cumulated CPU time (s) 9.52
Current children cumulated vsize (Kb) 15696

[startup+20.005 s]
Raw data (loadavg): 0.90 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 6777 0 0 0 1824 43 0 0 25 0 1 0 1796587067 23515136 5523 4294967295 134512640 135167914 3221224448 3221222848 134849187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9558/statm): 5741 5523 162 162 0 5579 0
[pid=9558] vsize: 22964
Current children cumulated CPU time (s) 19.3
Current children cumulated vsize (Kb) 25092

[startup+30.0049 s]
Raw data (loadavg): 0.91 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 11072 0 0 0 2777 67 0 0 25 0 1 0 1796587067 33783808 7985 4294967295 134512640 135167914 3221224448 3221222608 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 8248 7985 162 162 0 8086 0
[pid=9558] vsize: 32992
Current children cumulated CPU time (s) 29.07
Current children cumulated vsize (Kb) 35120

[startup+40.0057 s]
Raw data (loadavg): 0.93 0.97 0.99 3/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 16794 0 0 0 3725 92 0 0 25 0 1 0 1796587067 46080000 10992 4294967295 134512640 135167914 3221224448 3220103168 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 11251 10993 162 162 0 11089 0
[pid=9558] vsize: 45000
Current children cumulated CPU time (s) 38.8
Current children cumulated vsize (Kb) 47128

[startup+50.0075 s]
Raw data (loadavg): 0.94 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 21921 0 0 0 4695 110 0 0 25 0 1 0 1796587067 67084288 16119 4294967295 134512640 135167914 3221224448 3208656064 134843113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9558/statm): 16378 16119 162 162 0 16216 0
[pid=9558] vsize: 65512
Current children cumulated CPU time (s) 48.68
Current children cumulated vsize (Kb) 67640

[startup+60.0094 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 21940 0 0 0 5694 111 0 0 25 0 1 0 1796587067 67190784 16138 4294967295 134512640 135167914 3221224448 3208991984 134845930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9558/statm): 16404 16138 162 162 0 16242 0
[pid=9558] vsize: 65616
Current children cumulated CPU time (s) 58.68
Current children cumulated vsize (Kb) 67744

[startup+70.0102 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 21984 0 0 0 6693 111 0 0 25 0 1 0 1796587067 67358720 16182 4294967295 134512640 135167914 3221224448 3209242940 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16445 16182 162 162 0 16283 0
[pid=9558] vsize: 65780
Current children cumulated CPU time (s) 68.67
Current children cumulated vsize (Kb) 67908

[startup+80.011 s]
Raw data (loadavg): 0.96 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 21987 0 0 0 7694 111 0 0 25 0 1 0 1796587067 67358720 16185 4294967295 134512640 135167914 3221224448 3209452032 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16445 16185 162 162 0 16283 0
[pid=9558] vsize: 65780
Current children cumulated CPU time (s) 78.68
Current children cumulated vsize (Kb) 67908

[startup+90.0119 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 21989 0 0 0 8693 111 0 0 25 0 1 0 1796587067 67358720 16187 4294967295 134512640 135167914 3221224448 3209634656 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16445 16187 162 162 0 16283 0
[pid=9558] vsize: 65780
Current children cumulated CPU time (s) 88.67
Current children cumulated vsize (Kb) 67908

[startup+100.012 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22018 0 0 0 9694 111 0 0 25 0 1 0 1796587067 67571712 16216 4294967295 134512640 135167914 3221224448 3209798684 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16497 16216 162 162 0 16335 0
[pid=9558] vsize: 65988
Current children cumulated CPU time (s) 98.68
Current children cumulated vsize (Kb) 68116

[startup+110.013 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22020 0 0 0 10694 111 0 0 25 0 1 0 1796587067 67571712 16218 4294967295 134512640 135167914 3221224448 3209949244 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16497 16218 162 162 0 16335 0
[pid=9558] vsize: 65988
Current children cumulated CPU time (s) 108.68
Current children cumulated vsize (Kb) 68116

[startup+120.013 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22022 0 0 0 11694 111 0 0 25 0 1 0 1796587067 67571712 16220 4294967295 134512640 135167914 3221224448 3210088528 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16497 16220 162 162 0 16335 0
[pid=9558] vsize: 65988
Current children cumulated CPU time (s) 118.68
Current children cumulated vsize (Kb) 68116

[startup+130.013 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22024 0 0 0 12694 111 0 0 25 0 1 0 1796587067 67571712 16222 4294967295 134512640 135167914 3221224448 3210219132 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16497 16222 162 162 0 16335 0
[pid=9558] vsize: 65988
Current children cumulated CPU time (s) 128.68
Current children cumulated vsize (Kb) 68116

[startup+140.014 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22109 0 0 0 13694 112 0 0 25 0 1 0 1796587067 67915776 16307 4294967295 134512640 135167914 3221224448 3210342112 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16581 16307 162 162 0 16419 0
[pid=9558] vsize: 66324
Current children cumulated CPU time (s) 138.69
Current children cumulated vsize (Kb) 68452

[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22111 0 0 0 14694 112 0 0 25 0 1 0 1796587067 67915776 16309 4294967295 134512640 135167914 3221224448 3210459200 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16581 16309 162 162 0 16419 0
[pid=9558] vsize: 66324
Current children cumulated CPU time (s) 148.69
Current children cumulated vsize (Kb) 68452

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22112 0 0 0 15694 112 0 0 25 0 1 0 1796587067 67915776 16310 4294967295 134512640 135167914 3221224448 3210570816 134694444 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16581 16310 162 162 0 16419 0
[pid=9558] vsize: 66324
Current children cumulated CPU time (s) 158.69
Current children cumulated vsize (Kb) 68452

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22114 0 0 0 16695 112 0 0 25 0 1 0 1796587067 67915776 16312 4294967295 134512640 135167914 3221224448 3210677888 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16581 16312 162 162 0 16419 0
[pid=9558] vsize: 66324
Current children cumulated CPU time (s) 168.7
Current children cumulated vsize (Kb) 68452

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22115 0 0 0 17695 112 0 0 25 0 1 0 1796587067 67915776 16313 4294967295 134512640 135167914 3221224448 3210780928 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16581 16313 162 162 0 16419 0
[pid=9558] vsize: 66324
Current children cumulated CPU time (s) 178.7
Current children cumulated vsize (Kb) 68452

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22116 0 0 0 18695 112 0 0 25 0 1 0 1796587067 67915776 16314 4294967295 134512640 135167914 3221224448 3210880208 134624640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16581 16314 162 162 0 16419 0
[pid=9558] vsize: 66324
Current children cumulated CPU time (s) 188.7
Current children cumulated vsize (Kb) 68452

[startup+200.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22118 0 0 0 19695 112 0 0 25 0 1 0 1796587067 67915776 16316 4294967295 134512640 135167914 3221224448 3210976032 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16581 16316 162 162 0 16419 0
[pid=9558] vsize: 66324
Current children cumulated CPU time (s) 198.7
Current children cumulated vsize (Kb) 68452

[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22119 0 0 0 20695 112 0 0 25 0 1 0 1796587067 67915776 16317 4294967295 134512640 135167914 3221224448 3211069216 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16581 16317 162 162 0 16419 0
[pid=9558] vsize: 66324
Current children cumulated CPU time (s) 208.7
Current children cumulated vsize (Kb) 68452

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22120 0 0 0 21695 112 0 0 25 0 1 0 1796587067 67915776 16318 4294967295 134512640 135167914 3221224448 3211159472 134849148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16581 16318 162 162 0 16419 0
[pid=9558] vsize: 66324
Current children cumulated CPU time (s) 218.7
Current children cumulated vsize (Kb) 68452

[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22121 0 0 0 22696 112 0 0 25 0 1 0 1796587067 67915776 16319 4294967295 134512640 135167914 3221224448 3211247292 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16581 16319 162 162 0 16419 0
[pid=9558] vsize: 66324
Current children cumulated CPU time (s) 228.71
Current children cumulated vsize (Kb) 68452

[startup+240.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22122 0 0 0 23696 112 0 0 25 0 1 0 1796587067 67915776 16320 4294967295 134512640 135167914 3221224448 3211332860 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16581 16320 162 162 0 16419 0
[pid=9558] vsize: 66324
Current children cumulated CPU time (s) 238.71
Current children cumulated vsize (Kb) 68452

[startup+250.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22125 0 0 0 24696 113 0 0 25 0 1 0 1796587067 67923968 16323 4294967295 134512640 135167914 3221224448 3211416192 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16583 16323 162 162 0 16421 0
[pid=9558] vsize: 66332
Current children cumulated CPU time (s) 248.72
Current children cumulated vsize (Kb) 68460

[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22129 0 0 0 25696 113 0 0 25 0 1 0 1796587067 67936256 16327 4294967295 134512640 135167914 3221224448 3211497724 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16586 16327 162 162 0 16424 0
[pid=9558] vsize: 66344
Current children cumulated CPU time (s) 258.72
Current children cumulated vsize (Kb) 68472

[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22134 0 0 0 26696 113 0 0 25 0 1 0 1796587067 67952640 16332 4294967295 134512640 135167914 3221224448 3211577248 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16590 16332 162 162 0 16428 0
[pid=9558] vsize: 66360
Current children cumulated CPU time (s) 268.72
Current children cumulated vsize (Kb) 68488

[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22138 0 0 0 27696 113 0 0 25 0 1 0 1796587067 68161536 16336 4294967295 134512640 135167914 3221224448 3211655188 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16641 16336 162 162 0 16479 0
[pid=9558] vsize: 66564
Current children cumulated CPU time (s) 278.72
Current children cumulated vsize (Kb) 68692

[startup+290.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22142 0 0 0 28696 113 0 0 25 0 1 0 1796587067 68173824 16340 4294967295 134512640 135167914 3221224448 3211731380 134849086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16644 16340 162 162 0 16482 0
[pid=9558] vsize: 66576
Current children cumulated CPU time (s) 288.72
Current children cumulated vsize (Kb) 68704

[startup+300.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22146 0 0 0 29696 113 0 0 25 0 1 0 1796587067 68186112 16344 4294967295 134512640 135167914 3221224448 3211806112 134844715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16647 16344 162 162 0 16485 0
[pid=9558] vsize: 66588
Current children cumulated CPU time (s) 298.72
Current children cumulated vsize (Kb) 68716

[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22149 0 0 0 30697 113 0 0 25 0 1 0 1796587067 68194304 16347 4294967295 134512640 135167914 3221224448 3211879420 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16649 16347 162 162 0 16487 0
[pid=9558] vsize: 66596
Current children cumulated CPU time (s) 308.73
Current children cumulated vsize (Kb) 68724

[startup+320.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22153 0 0 0 31697 113 0 0 25 0 1 0 1796587067 68206592 16351 4294967295 134512640 135167914 3221224448 3211951264 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16652 16351 162 162 0 16490 0
[pid=9558] vsize: 66608
Current children cumulated CPU time (s) 318.73
Current children cumulated vsize (Kb) 68736

[startup+330.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22158 0 0 0 32697 113 0 0 25 0 1 0 1796587067 68222976 16356 4294967295 134512640 135167914 3221224448 3212021984 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16656 16356 162 162 0 16494 0
[pid=9558] vsize: 66624
Current children cumulated CPU time (s) 328.73
Current children cumulated vsize (Kb) 68752

[startup+340.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22161 0 0 0 33697 113 0 0 25 0 1 0 1796587067 68231168 16359 4294967295 134512640 135167914 3221224448 3212091488 134844697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16658 16359 162 162 0 16496 0
[pid=9558] vsize: 66632
Current children cumulated CPU time (s) 338.73
Current children cumulated vsize (Kb) 68760

[startup+350.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22165 0 0 0 34697 113 0 0 25 0 1 0 1796587067 68243456 16363 4294967295 134512640 135167914 3221224448 3212160096 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16661 16363 162 162 0 16499 0
[pid=9558] vsize: 66644
Current children cumulated CPU time (s) 348.73
Current children cumulated vsize (Kb) 68772

[startup+360.028 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22169 0 0 0 35697 113 0 0 25 0 1 0 1796587067 68255744 16367 4294967295 134512640 135167914 3221224448 3212227296 134694383 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16664 16367 162 162 0 16502 0
[pid=9558] vsize: 66656
Current children cumulated CPU time (s) 358.73
Current children cumulated vsize (Kb) 68784

[startup+370.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22172 0 0 0 36697 113 0 0 25 0 1 0 1796587067 68263936 16370 4294967295 134512640 135167914 3221224448 3212293632 134624644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16666 16370 162 162 0 16504 0
[pid=9558] vsize: 66664
Current children cumulated CPU time (s) 368.73
Current children cumulated vsize (Kb) 68792

[startup+380.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22176 0 0 0 37697 113 0 0 25 0 1 0 1796587067 68276224 16374 4294967295 134512640 135167914 3221224448 3212358736 134843001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16669 16374 162 162 0 16507 0
[pid=9558] vsize: 66676
Current children cumulated CPU time (s) 378.73
Current children cumulated vsize (Kb) 68804

[startup+390.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22178 0 0 0 38697 114 0 0 25 0 1 0 1796587067 68284416 16376 4294967295 134512640 135167914 3221224448 3212423056 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16671 16376 162 162 0 16509 0
[pid=9558] vsize: 66684
Current children cumulated CPU time (s) 388.74
Current children cumulated vsize (Kb) 68812

[startup+400.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22182 0 0 0 39697 114 0 0 25 0 1 0 1796587067 68296704 16380 4294967295 134512640 135167914 3221224448 3212486464 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16674 16380 162 162 0 16512 0
[pid=9558] vsize: 66696
Current children cumulated CPU time (s) 398.74
Current children cumulated vsize (Kb) 68824

[startup+410.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22185 0 0 0 40698 114 0 0 25 0 1 0 1796587067 68304896 16383 4294967295 134512640 135167914 3221224448 3212548956 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16676 16383 162 162 0 16514 0
[pid=9558] vsize: 66704
Current children cumulated CPU time (s) 408.75
Current children cumulated vsize (Kb) 68832

[startup+420.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22189 0 0 0 41698 114 0 0 25 0 1 0 1796587067 68317184 16387 4294967295 134512640 135167914 3221224448 3212610560 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16679 16387 162 162 0 16517 0
[pid=9558] vsize: 66716
Current children cumulated CPU time (s) 418.75
Current children cumulated vsize (Kb) 68844

[startup+430.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22358 0 0 0 42698 114 0 0 25 0 1 0 1796587067 68661248 16472 4294967295 134512640 135167914 3221224448 3212671276 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16763 16472 162 162 0 16601 0
[pid=9558] vsize: 67052
Current children cumulated CPU time (s) 428.75
Current children cumulated vsize (Kb) 69180

[startup+440.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22361 0 0 0 43698 114 0 0 25 0 1 0 1796587067 68673536 16475 4294967295 134512640 135167914 3221224448 3212731216 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16766 16475 162 162 0 16604 0
[pid=9558] vsize: 67064
Current children cumulated CPU time (s) 438.75
Current children cumulated vsize (Kb) 69192

[startup+450.034 s]
Raw data (loadavg): 0.99 0.97 0.99 3/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22364 0 0 0 44698 114 0 0 25 0 1 0 1796587067 68681728 16478 4294967295 134512640 135167914 3221224448 3212790704 134624604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16768 16478 162 162 0 16606 0
[pid=9558] vsize: 67072
Current children cumulated CPU time (s) 448.75
Current children cumulated vsize (Kb) 69200

[startup+460.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22367 0 0 0 45698 114 0 0 25 0 1 0 1796587067 68689920 16481 4294967295 134512640 135167914 3221224448 3212849312 134722532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16770 16481 162 162 0 16608 0
[pid=9558] vsize: 67080
Current children cumulated CPU time (s) 458.75
Current children cumulated vsize (Kb) 69208

[startup+470.036 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22371 0 0 0 46698 114 0 0 25 0 1 0 1796587067 68702208 16485 4294967295 134512640 135167914 3221224448 3212907372 134722660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16773 16485 162 162 0 16611 0
[pid=9558] vsize: 67092
Current children cumulated CPU time (s) 468.75
Current children cumulated vsize (Kb) 69220

[startup+480.036 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22374 0 0 0 47698 115 0 0 25 0 1 0 1796587067 68710400 16488 4294967295 134512640 135167914 3221224448 3212964480 134694407 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16775 16488 162 162 0 16613 0
[pid=9558] vsize: 67100
Current children cumulated CPU time (s) 478.76
Current children cumulated vsize (Kb) 69228

[startup+490.037 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22376 0 0 0 48699 115 0 0 25 0 1 0 1796587067 68718592 16490 4294967295 134512640 135167914 3221224448 3213021024 134844641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16777 16490 162 162 0 16615 0
[pid=9558] vsize: 67108
Current children cumulated CPU time (s) 488.77
Current children cumulated vsize (Kb) 69236

[startup+500.038 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22379 0 0 0 49699 115 0 0 25 0 1 0 1796587067 68726784 16493 4294967295 134512640 135167914 3221224448 3213077024 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16779 16493 162 162 0 16617 0
[pid=9558] vsize: 67116
Current children cumulated CPU time (s) 498.77
Current children cumulated vsize (Kb) 69244

[startup+510.039 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22383 0 0 0 50698 116 0 0 25 0 1 0 1796587067 68739072 16497 4294967295 134512640 135167914 3221224448 3213132444 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16782 16497 162 162 0 16620 0
[pid=9558] vsize: 67128
Current children cumulated CPU time (s) 508.77
Current children cumulated vsize (Kb) 69256

[startup+520.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22384 0 0 0 51697 117 0 0 25 0 1 0 1796587067 68743168 16498 4294967295 134512640 135167914 3221224448 3213187152 134849143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16783 16498 162 162 0 16621 0
[pid=9558] vsize: 67132
Current children cumulated CPU time (s) 518.77
Current children cumulated vsize (Kb) 69260

[startup+530.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22388 0 0 0 52697 117 0 0 25 0 1 0 1796587067 68755456 16502 4294967295 134512640 135167914 3221224448 3213241056 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16786 16502 162 162 0 16624 0
[pid=9558] vsize: 67144
Current children cumulated CPU time (s) 528.77
Current children cumulated vsize (Kb) 69272

[startup+540.041 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22391 0 0 0 53697 117 0 0 25 0 1 0 1796587067 68763648 16505 4294967295 134512640 135167914 3221224448 3213294880 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16788 16505 162 162 0 16626 0
[pid=9558] vsize: 67152
Current children cumulated CPU time (s) 538.77
Current children cumulated vsize (Kb) 69280

[startup+550.041 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22394 0 0 0 54696 117 0 0 25 0 1 0 1796587067 68771840 16508 4294967295 134512640 135167914 3221224448 3213347904 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16790 16508 162 162 0 16628 0
[pid=9558] vsize: 67160
Current children cumulated CPU time (s) 548.76
Current children cumulated vsize (Kb) 69288

[startup+560.042 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22396 0 0 0 55697 117 0 0 25 0 1 0 1796587067 68780032 16510 4294967295 134512640 135167914 3221224448 3213400588 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16792 16510 162 162 0 16630 0
[pid=9558] vsize: 67168
Current children cumulated CPU time (s) 558.77
Current children cumulated vsize (Kb) 69296

[startup+570.043 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22399 0 0 0 56697 117 0 0 25 0 1 0 1796587067 68788224 16513 4294967295 134512640 135167914 3221224448 3213452624 134624657 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16794 16513 162 162 0 16632 0
[pid=9558] vsize: 67176
Current children cumulated CPU time (s) 568.77
Current children cumulated vsize (Kb) 69304

[startup+580.044 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22403 0 0 0 57697 117 0 0 25 0 1 0 1796587067 68800512 16517 4294967295 134512640 135167914 3221224448 3213504076 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16797 16517 162 162 0 16635 0
[pid=9558] vsize: 67188
Current children cumulated CPU time (s) 578.77
Current children cumulated vsize (Kb) 69316

[startup+590.045 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22404 0 0 0 58697 118 0 0 25 0 1 0 1796587067 68804608 16518 4294967295 134512640 135167914 3221224448 3213555392 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16798 16518 162 162 0 16636 0
[pid=9558] vsize: 67192
Current children cumulated CPU time (s) 588.78
Current children cumulated vsize (Kb) 69320

[startup+600.045 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22407 0 0 0 59697 118 0 0 25 0 1 0 1796587067 68812800 16521 4294967295 134512640 135167914 3221224448 3213605996 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16800 16521 162 162 0 16638 0
[pid=9558] vsize: 67200
Current children cumulated CPU time (s) 598.78
Current children cumulated vsize (Kb) 69328

[startup+610.046 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22410 0 0 0 60697 118 0 0 25 0 1 0 1796587067 68820992 16524 4294967295 134512640 135167914 3221224448 3213656112 134845895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16802 16524 162 162 0 16640 0
[pid=9558] vsize: 67208
Current children cumulated CPU time (s) 608.78
Current children cumulated vsize (Kb) 69336

[startup+620.047 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22413 0 0 0 61697 118 0 0 25 0 1 0 1796587067 68833280 16527 4294967295 134512640 135167914 3221224448 3213705892 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16805 16527 162 162 0 16643 0
[pid=9558] vsize: 67220
Current children cumulated CPU time (s) 618.78
Current children cumulated vsize (Kb) 69348

[startup+630.047 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22415 0 0 0 62698 118 0 0 25 0 1 0 1796587067 68837376 16529 4294967295 134512640 135167914 3221224448 3213755408 134849148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16806 16529 162 162 0 16644 0
[pid=9558] vsize: 67224
Current children cumulated CPU time (s) 628.79
Current children cumulated vsize (Kb) 69352

[startup+640.048 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22418 0 0 0 63698 118 0 0 25 0 1 0 1796587067 68845568 16532 4294967295 134512640 135167914 3221224448 3213804256 134694398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16808 16532 162 162 0 16646 0
[pid=9558] vsize: 67232
Current children cumulated CPU time (s) 638.79
Current children cumulated vsize (Kb) 69360

[startup+650.048 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22420 0 0 0 64698 118 0 0 25 0 1 0 1796587067 68853760 16534 4294967295 134512640 135167914 3221224448 3213852912 134624426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16810 16534 162 162 0 16648 0
[pid=9558] vsize: 67240
Current children cumulated CPU time (s) 648.79
Current children cumulated vsize (Kb) 69368

[startup+660.048 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22423 0 0 0 65698 118 0 0 25 0 1 0 1796587067 68861952 16537 4294967295 134512640 135167914 3221224448 3213900896 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16812 16537 162 162 0 16650 0
[pid=9558] vsize: 67248
Current children cumulated CPU time (s) 658.79
Current children cumulated vsize (Kb) 69376

[startup+670.049 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22425 0 0 0 66698 118 0 0 25 0 1 0 1796587067 68870144 16539 4294967295 134512640 135167914 3221224448 3213948752 134693563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16814 16539 162 162 0 16652 0
[pid=9558] vsize: 67256
Current children cumulated CPU time (s) 668.79
Current children cumulated vsize (Kb) 69384

[startup+680.049 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22428 0 0 0 67698 118 0 0 25 0 1 0 1796587067 68878336 16542 4294967295 134512640 135167914 3221224448 3213995904 134844672 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16816 16542 162 162 0 16654 0
[pid=9558] vsize: 67264
Current children cumulated CPU time (s) 678.79
Current children cumulated vsize (Kb) 69392

[startup+690.05 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22431 0 0 0 68698 119 0 0 25 0 1 0 1796587067 68886528 16545 4294967295 134512640 135167914 3221224448 3214043028 134845938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16818 16545 162 162 0 16656 0
[pid=9558] vsize: 67272
Current children cumulated CPU time (s) 688.8
Current children cumulated vsize (Kb) 69400

[startup+700.051 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22433 0 0 0 69698 119 0 0 25 0 1 0 1796587067 68894720 16547 4294967295 134512640 135167914 3221224448 3214089656 134694369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16820 16547 162 162 0 16658 0
[pid=9558] vsize: 67280
Current children cumulated CPU time (s) 698.8
Current children cumulated vsize (Kb) 69408

[startup+710.052 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22435 0 0 0 70698 119 0 0 25 0 1 0 1796587067 68898816 16549 4294967295 134512640 135167914 3221224448 3214135936 134843074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16821 16549 162 162 0 16659 0
[pid=9558] vsize: 67284
Current children cumulated CPU time (s) 708.8
Current children cumulated vsize (Kb) 69412

[startup+720.052 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22437 0 0 0 71698 119 0 0 25 0 1 0 1796587067 68907008 16551 4294967295 134512640 135167914 3221224448 3214181920 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16823 16551 162 162 0 16661 0
[pid=9558] vsize: 67292
Current children cumulated CPU time (s) 718.8
Current children cumulated vsize (Kb) 69420

[startup+730.052 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22440 0 0 0 72699 119 0 0 25 0 1 0 1796587067 68915200 16554 4294967295 134512640 135167914 3221224448 3214227616 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16825 16554 162 162 0 16663 0
[pid=9558] vsize: 67300
Current children cumulated CPU time (s) 728.81
Current children cumulated vsize (Kb) 69428

[startup+740.053 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22443 0 0 0 73698 119 0 0 25 0 1 0 1796587067 68923392 16557 4294967295 134512640 135167914 3221224448 3214272896 134624608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16827 16557 162 162 0 16665 0
[pid=9558] vsize: 67308
Current children cumulated CPU time (s) 738.8
Current children cumulated vsize (Kb) 69436

[startup+750.054 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22444 0 0 0 74699 119 0 0 25 0 1 0 1796587067 68927488 16558 4294967295 134512640 135167914 3221224448 3214317664 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16828 16558 162 162 0 16666 0
[pid=9558] vsize: 67312
Current children cumulated CPU time (s) 748.81
Current children cumulated vsize (Kb) 69440

[startup+760.055 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22447 0 0 0 75699 119 0 0 25 0 1 0 1796587067 68935680 16561 4294967295 134512640 135167914 3221224448 3214362176 134844725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16830 16561 162 162 0 16668 0
[pid=9558] vsize: 67320
Current children cumulated CPU time (s) 758.81
Current children cumulated vsize (Kb) 69448

[startup+770.056 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22449 0 0 0 76699 119 0 0 25 0 1 0 1796587067 68943872 16563 4294967295 134512640 135167914 3221224448 3214406564 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16832 16563 162 162 0 16670 0
[pid=9558] vsize: 67328
Current children cumulated CPU time (s) 768.81
Current children cumulated vsize (Kb) 69456

[startup+780.056 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22452 0 0 0 77699 119 0 0 25 0 1 0 1796587067 68952064 16566 4294967295 134512640 135167914 3221224448 3214450644 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16834 16566 162 162 0 16672 0
[pid=9558] vsize: 67336
Current children cumulated CPU time (s) 778.81
Current children cumulated vsize (Kb) 69464

[startup+790.057 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22455 0 0 0 78699 120 0 0 25 0 1 0 1796587067 68960256 16569 4294967295 134512640 135167914 3221224448 3214494420 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16836 16569 162 162 0 16674 0
[pid=9558] vsize: 67344
Current children cumulated CPU time (s) 788.82
Current children cumulated vsize (Kb) 69472

[startup+800.057 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22456 0 0 0 79699 120 0 0 25 0 1 0 1796587067 68964352 16570 4294967295 134512640 135167914 3221224448 3214537648 134693563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16837 16570 162 162 0 16675 0
[pid=9558] vsize: 67348
Current children cumulated CPU time (s) 798.82
Current children cumulated vsize (Kb) 69476

[startup+810.059 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22459 0 0 0 80700 120 0 0 25 0 1 0 1796587067 68972544 16573 4294967295 134512640 135167914 3221224448 3214580736 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16839 16573 162 162 0 16677 0
[pid=9558] vsize: 67356
Current children cumulated CPU time (s) 808.83
Current children cumulated vsize (Kb) 69484

[startup+820.06 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22461 0 0 0 81700 120 0 0 25 0 1 0 1796587067 68980736 16575 4294967295 134512640 135167914 3221224448 3214623648 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16841 16575 162 162 0 16679 0
[pid=9558] vsize: 67364
Current children cumulated CPU time (s) 818.83
Current children cumulated vsize (Kb) 69492

[startup+830.06 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22464 0 0 0 82700 120 0 0 25 0 1 0 1796587067 68988928 16578 4294967295 134512640 135167914 3221224448 3214666256 134624724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16843 16578 162 162 0 16681 0
[pid=9558] vsize: 67372
Current children cumulated CPU time (s) 828.83
Current children cumulated vsize (Kb) 69500

[startup+840.06 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22465 0 0 0 83700 120 0 0 25 0 1 0 1796587067 68993024 16579 4294967295 134512640 135167914 3221224448 3214708544 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16844 16579 162 162 0 16682 0
[pid=9558] vsize: 67376
Current children cumulated CPU time (s) 838.83
Current children cumulated vsize (Kb) 69504

[startup+850.061 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22468 0 0 0 84700 120 0 0 25 0 1 0 1796587067 69001216 16582 4294967295 134512640 135167914 3221224448 3214750656 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16846 16582 162 162 0 16684 0
[pid=9558] vsize: 67384
Current children cumulated CPU time (s) 848.83
Current children cumulated vsize (Kb) 69512

[startup+860.062 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22470 0 0 0 85701 120 0 0 25 0 1 0 1796587067 69009408 16584 4294967295 134512640 135167914 3221224448 3214792352 134624782 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16848 16584 162 162 0 16686 0
[pid=9558] vsize: 67392
Current children cumulated CPU time (s) 858.84
Current children cumulated vsize (Kb) 69520

[startup+870.063 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22472 0 0 0 86701 120 0 0 25 0 1 0 1796587067 69013504 16586 4294967295 134512640 135167914 3221224448 3214833980 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16849 16586 162 162 0 16687 0
[pid=9558] vsize: 67396
Current children cumulated CPU time (s) 868.84
Current children cumulated vsize (Kb) 69524

[startup+880.064 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22475 0 0 0 87701 120 0 0 25 0 1 0 1796587067 69021696 16589 4294967295 134512640 135167914 3221224448 3214875196 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16851 16589 162 162 0 16689 0
[pid=9558] vsize: 67404
Current children cumulated CPU time (s) 878.84
Current children cumulated vsize (Kb) 69532

[startup+890.065 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22476 0 0 0 88701 120 0 0 25 0 1 0 1796587067 69025792 16590 4294967295 134512640 135167914 3221224448 3214916064 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16852 16590 162 162 0 16690 0
[pid=9558] vsize: 67408
Current children cumulated CPU time (s) 888.84
Current children cumulated vsize (Kb) 69536

[startup+900.065 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22479 0 0 0 89701 120 0 0 25 0 1 0 1796587067 69033984 16593 4294967295 134512640 135167914 3221224448 3214956860 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16854 16593 162 162 0 16692 0
[pid=9558] vsize: 67416
Current children cumulated CPU time (s) 898.84
Current children cumulated vsize (Kb) 69544

[startup+910.066 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22481 0 0 0 90702 120 0 0 25 0 1 0 1796587067 69042176 16595 4294967295 134512640 135167914 3221224448 3214997440 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16856 16595 162 162 0 16694 0
[pid=9558] vsize: 67424
Current children cumulated CPU time (s) 908.85
Current children cumulated vsize (Kb) 69552

[startup+920.067 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22484 0 0 0 91702 120 0 0 25 0 1 0 1796587067 69050368 16598 4294967295 134512640 135167914 3221224448 3215037872 134624420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16858 16598 162 162 0 16696 0
[pid=9558] vsize: 67432
Current children cumulated CPU time (s) 918.85
Current children cumulated vsize (Kb) 69560

[startup+930.068 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22485 0 0 0 92702 120 0 0 25 0 1 0 1796587067 69054464 16599 4294967295 134512640 135167914 3221224448 3215077856 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16859 16599 162 162 0 16697 0
[pid=9558] vsize: 67436
Current children cumulated CPU time (s) 928.85
Current children cumulated vsize (Kb) 69564

[startup+940.069 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22487 0 0 0 93702 120 0 0 25 0 1 0 1796587067 69058560 16601 4294967295 134512640 135167914 3221224448 3215117832 134624744 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16860 16601 162 162 0 16698 0
[pid=9558] vsize: 67440
Current children cumulated CPU time (s) 938.85
Current children cumulated vsize (Kb) 69568

[startup+950.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22489 0 0 0 94703 120 0 0 25 0 1 0 1796587067 69066752 16603 4294967295 134512640 135167914 3221224448 3215157404 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16862 16603 162 162 0 16700 0
[pid=9558] vsize: 67448
Current children cumulated CPU time (s) 948.86
Current children cumulated vsize (Kb) 69576

[startup+960.071 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22492 0 0 0 95703 120 0 0 25 0 1 0 1796587067 69074944 16606 4294967295 134512640 135167914 3221224448 3215196864 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16864 16606 162 162 0 16702 0
[pid=9558] vsize: 67456
Current children cumulated CPU time (s) 958.86
Current children cumulated vsize (Kb) 69584

[startup+970.072 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22494 0 0 0 96703 120 0 0 25 0 1 0 1796587067 69083136 16608 4294967295 134512640 135167914 3221224448 3215236080 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16866 16608 162 162 0 16704 0
[pid=9558] vsize: 67464
Current children cumulated CPU time (s) 968.86
Current children cumulated vsize (Kb) 69592

[startup+980.073 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22495 0 0 0 97703 120 0 0 25 0 1 0 1796587067 69476352 16609 4294967295 134512640 135167914 3221224448 3215274988 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16962 16609 162 162 0 16800 0
[pid=9558] vsize: 67848
Current children cumulated CPU time (s) 978.86
Current children cumulated vsize (Kb) 69976

[startup+990.074 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22497 0 0 0 98703 121 0 0 25 0 1 0 1796587067 69484544 16611 4294967295 134512640 135167914 3221224448 3215313788 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16964 16611 162 162 0 16802 0
[pid=9558] vsize: 67856
Current children cumulated CPU time (s) 988.87
Current children cumulated vsize (Kb) 69984

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22500 0 0 0 99703 121 0 0 25 0 1 0 1796587067 69492736 16614 4294967295 134512640 135167914 3221224448 3215352368 134624410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16966 16614 162 162 0 16804 0
[pid=9558] vsize: 67864
Current children cumulated CPU time (s) 998.87
Current children cumulated vsize (Kb) 69992

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22502 0 0 0 100703 121 0 0 25 0 1 0 1796587067 69500928 16616 4294967295 134512640 135167914 3221224448 3215390848 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16968 16616 162 162 0 16806 0
[pid=9558] vsize: 67872
Current children cumulated CPU time (s) 1008.87
Current children cumulated vsize (Kb) 70000

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22504 0 0 0 101704 121 0 0 25 0 1 0 1796587067 69505024 16618 4294967295 134512640 135167914 3221224448 3215428928 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16969 16618 162 162 0 16807 0
[pid=9558] vsize: 67876
Current children cumulated CPU time (s) 1018.88
Current children cumulated vsize (Kb) 70004

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22505 0 0 0 102704 121 0 0 25 0 1 0 1796587067 69509120 16619 4294967295 134512640 135167914 3221224448 3215466944 134844725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16970 16619 162 162 0 16808 0
[pid=9558] vsize: 67880
Current children cumulated CPU time (s) 1028.88
Current children cumulated vsize (Kb) 70008

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22508 0 0 0 103704 121 0 0 25 0 1 0 1796587067 69517312 16622 4294967295 134512640 135167914 3221224448 3215504640 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16972 16622 162 162 0 16810 0
[pid=9558] vsize: 67888
Current children cumulated CPU time (s) 1038.88
Current children cumulated vsize (Kb) 70016

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22509 0 0 0 104704 121 0 0 25 0 1 0 1796587067 69521408 16623 4294967295 134512640 135167914 3221224448 3215542288 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16973 16623 162 162 0 16811 0
[pid=9558] vsize: 67892
Current children cumulated CPU time (s) 1048.88
Current children cumulated vsize (Kb) 70020

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22512 0 0 0 105704 121 0 0 25 0 1 0 1796587067 69529600 16626 4294967295 134512640 135167914 3221224448 3215579616 134843074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16975 16626 162 162 0 16813 0
[pid=9558] vsize: 67900
Current children cumulated CPU time (s) 1058.88
Current children cumulated vsize (Kb) 70028

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22514 0 0 0 106705 121 0 0 25 0 1 0 1796587067 69537792 16628 4294967295 134512640 135167914 3221224448 3215616736 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16977 16628 162 162 0 16815 0
[pid=9558] vsize: 67908
Current children cumulated CPU time (s) 1068.89
Current children cumulated vsize (Kb) 70036

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22515 0 0 0 107705 121 0 0 25 0 1 0 1796587067 69537792 16629 4294967295 134512640 135167914 3221224448 3215654096 134624420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16977 16629 162 162 0 16815 0
[pid=9558] vsize: 67908
Current children cumulated CPU time (s) 1078.89
Current children cumulated vsize (Kb) 70036

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22517 0 0 0 108705 121 0 0 25 0 1 0 1796587067 69545984 16631 4294967295 134512640 135167914 3221224448 3215690796 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16979 16631 162 162 0 16817 0
[pid=9558] vsize: 67916
Current children cumulated CPU time (s) 1088.89
Current children cumulated vsize (Kb) 70044

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22520 0 0 0 109705 121 0 0 25 0 1 0 1796587067 69554176 16634 4294967295 134512640 135167914 3221224448 3215727516 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16981 16634 162 162 0 16819 0
[pid=9558] vsize: 67924
Current children cumulated CPU time (s) 1098.89
Current children cumulated vsize (Kb) 70052

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22521 0 0 0 110704 122 0 0 25 0 1 0 1796587067 69558272 16635 4294967295 134512640 135167914 3221224448 3215764016 134849148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16982 16635 162 162 0 16820 0
[pid=9558] vsize: 67928
Current children cumulated CPU time (s) 1108.89
Current children cumulated vsize (Kb) 70056

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22524 0 0 0 111704 123 0 0 25 0 1 0 1796587067 69566464 16638 4294967295 134512640 135167914 3221224448 3215800220 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16984 16638 162 162 0 16822 0
[pid=9558] vsize: 67936
Current children cumulated CPU time (s) 1118.9
Current children cumulated vsize (Kb) 70064

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22525 0 0 0 112704 123 0 0 25 0 1 0 1796587067 69570560 16639 4294967295 134512640 135167914 3221224448 3215836392 134722657 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16985 16639 162 162 0 16823 0
[pid=9558] vsize: 67940
Current children cumulated CPU time (s) 1128.9
Current children cumulated vsize (Kb) 70068

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22527 0 0 0 113704 123 0 0 25 0 1 0 1796587067 69574656 16641 4294967295 134512640 135167914 3221224448 3215872496 134624420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16986 16641 162 162 0 16824 0
[pid=9558] vsize: 67944
Current children cumulated CPU time (s) 1138.9
Current children cumulated vsize (Kb) 70072

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22529 0 0 0 114704 124 0 0 25 0 1 0 1796587067 69582848 16643 4294967295 134512640 135167914 3221224448 3215908236 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16988 16643 162 162 0 16826 0
[pid=9558] vsize: 67952
Current children cumulated CPU time (s) 1148.91
Current children cumulated vsize (Kb) 70080

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22532 0 0 0 115704 124 0 0 25 0 1 0 1796587067 69591040 16646 4294967295 134512640 135167914 3221224448 3215943904 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16990 16646 162 162 0 16828 0
[pid=9558] vsize: 67960
Current children cumulated CPU time (s) 1158.91
Current children cumulated vsize (Kb) 70088

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22533 0 0 0 116704 124 0 0 25 0 1 0 1796587067 69595136 16647 4294967295 134512640 135167914 3221224448 3215979520 134694444 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16991 16647 162 162 0 16829 0
[pid=9558] vsize: 67964
Current children cumulated CPU time (s) 1168.91
Current children cumulated vsize (Kb) 70092

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22534 0 0 0 117704 124 0 0 25 0 1 0 1796587067 69599232 16648 4294967295 134512640 135167914 3221224448 3216014928 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16992 16648 162 162 0 16830 0
[pid=9558] vsize: 67968
Current children cumulated CPU time (s) 1178.91
Current children cumulated vsize (Kb) 70096

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22536 0 0 0 118704 124 0 0 25 0 1 0 1796587067 69603328 16650 4294967295 134512640 135167914 3221224448 3216050108 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16993 16650 162 162 0 16831 0
[pid=9558] vsize: 67972
Current children cumulated CPU time (s) 1188.91
Current children cumulated vsize (Kb) 70100

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22538 0 0 0 119704 124 0 0 25 0 1 0 1796587067 69611520 16652 4294967295 134512640 135167914 3221224448 3216084960 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16995 16652 162 162 0 16833 0
[pid=9558] vsize: 67980
Current children cumulated CPU time (s) 1198.91
Current children cumulated vsize (Kb) 70108

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22540 0 0 0 120704 124 0 0 25 0 1 0 1796587067 69615616 16654 4294967295 134512640 135167914 3221224448 3216120000 134624613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16996 16654 162 162 0 16834 0
[pid=9558] vsize: 67984
Current children cumulated CPU time (s) 1208.91
Current children cumulated vsize (Kb) 70112



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 9558
Raw data (/proc/9553/stat): 9553 (minisat+_script) S 9552 9553 8263 0 -1 0 314 2351 0 0 0 0 47 16 20 0 1 0 1796586986 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9553/statm): 532 234 485 147 0 385 0
[pid=9553] vsize: 2128
Raw data (/proc/9558/stat): 9558 (minisat+_bignum) R 9553 9553 8263 0 -1 0 22540 0 0 0 120705 124 0 0 25 0 1 0 1796587067 69615616 16654 4294967295 134512640 135167914 3221224448 3216119964 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9558/statm): 16996 16654 162 162 0 16834 0
[pid=9558] vsize: 67984
Current children cumulated CPU time (s) 1208.92
Current children cumulated vsize (Kb) 70112

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

Child status: 0
Real time (s): 1210.12
CPU time (s): 1208.33
CPU user time (s): 1207.05
CPU system time (s): 1.27981
CPU usage (%): 99.8517
Max. virtual memory (cumulated for all children) (Kb): 70112

Verifier Data

ERROR: no interpretation found !