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/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-scrs8.opb
MD5SUM5dc586d2135331b914090f6587c7f4ee
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 24750
Biggest coefficient in the objective function 284830543390965760000
Number of bits for the biggest coefficient in the objective function 68
Sum of the numbers in the objective function 7193462013935082274816
Number of bits of the sum of numbers in the objective function 73
Biggest number in a constraint 284830543390965760000
Number of bits of the biggest number in a constraint 68
Biggest sum of numbers in a constraint 7193462013935082274816
Number of bits of the biggest sum of numbers73
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables35070
Total number of constraints490
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints490
Minimum length of a constraint30
Maximum length of a constraint1110

Trace number 2668

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        900740 kB
Buffers:         34204 kB
Cached:          71316 kB
SwapCached:        696 kB
Active:          65512 kB
Inactive:        42560 kB
HighTotal:      131008 kB
HighFree:        56112 kB
LowTotal:       903652 kB
LowFree:        844628 kB
SwapTotal:     2097640 kB
SwapFree:      2096372 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5812 kB
Slab:            20252 kB
Committed_AS:    64128 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 20:51:44 (client local time) WITH STATUS 0 IN 1200 SECONDS
stats: 2806 7 1200 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 1173] 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/5091/stat): 5091 (minisat+_script) R 5090 5091 20115 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1844166837 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/5091/statm): 174 3 169 147 0 27 0
[pid=5091] 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=5092
New process pid=5093
New process pid=5094
execve syscall for /bin/sed executable
One traced child (pid=5093) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=5094) exited with status: 0
One traced child (pid=5092) exited with status: 0
New process pid=5095
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-scrs8.opb
One traced child (pid=5095) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=5096
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-scrs8.opb

[startup+10.0041 s]
Raw data (loadavg): 0.91 0.94 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3777 0 0 0 949 23 0 0 25 0 1 0 1844166844 17571840 3721 4294967295 134512640 135167914 3221224448 3221223272 134691388 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4290 3721 162 162 0 4128 0
[pid=5096] vsize: 17160
Current children cumulated CPU time (s) 9.74
Current children cumulated vsize (Kb) 19288

[startup+20.0048 s]
Raw data (loadavg): 0.92 0.94 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3793 0 0 0 1950 23 0 0 25 0 1 0 1844166844 16797696 3531 4294967295 134512640 135167914 3221224448 3221218220 134723236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4101 3531 162 162 0 3939 0
[pid=5096] vsize: 16404
Current children cumulated CPU time (s) 19.75
Current children cumulated vsize (Kb) 18532

[startup+30.0044 s]
Raw data (loadavg): 0.94 0.94 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3793 0 0 0 2950 23 0 0 25 0 1 0 1844166844 16797696 3531 4294967295 134512640 135167914 3221224448 3221218640 134522189 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4101 3531 162 162 0 3939 0
[pid=5096] vsize: 16404
Current children cumulated CPU time (s) 29.75
Current children cumulated vsize (Kb) 18532

[startup+40.0051 s]
Raw data (loadavg): 0.94 0.94 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3793 0 0 0 3950 23 0 0 25 0 1 0 1844166844 16797696 3531 4294967295 134512640 135167914 3221224448 3221219440 134843113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4101 3531 162 162 0 3939 0
[pid=5096] vsize: 16404
Current children cumulated CPU time (s) 39.75
Current children cumulated vsize (Kb) 18532

[startup+50.0058 s]
Raw data (loadavg): 0.95 0.94 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3793 0 0 0 4950 23 0 0 25 0 1 0 1844166844 16797696 3531 4294967295 134512640 135167914 3221224448 3221221268 134849086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4101 3531 162 162 0 3939 0
[pid=5096] vsize: 16404
Current children cumulated CPU time (s) 49.75
Current children cumulated vsize (Kb) 18532

[startup+60.0065 s]
Raw data (loadavg): 0.96 0.94 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3793 0 0 0 5950 23 0 0 25 0 1 0 1844166844 16797696 3531 4294967295 134512640 135167914 3221224448 3221219180 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4101 3531 162 162 0 3939 0
[pid=5096] vsize: 16404
Current children cumulated CPU time (s) 59.75
Current children cumulated vsize (Kb) 18532

[startup+70.0072 s]
Raw data (loadavg): 0.97 0.94 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3793 0 0 0 6951 23 0 0 25 0 1 0 1844166844 16797696 3531 4294967295 134512640 135167914 3221224448 3221219152 134694517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4101 3531 162 162 0 3939 0
[pid=5096] vsize: 16404
Current children cumulated CPU time (s) 69.76
Current children cumulated vsize (Kb) 18532

[startup+80.0078 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3793 0 0 0 7951 23 0 0 25 0 1 0 1844166844 16797696 3531 4294967295 134512640 135167914 3221224448 3221220672 134843074 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4101 3531 162 162 0 3939 0
[pid=5096] vsize: 16404
Current children cumulated CPU time (s) 79.76
Current children cumulated vsize (Kb) 18532

[startup+90.0085 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3793 0 0 0 8951 23 0 0 25 0 1 0 1844166844 16797696 3531 4294967295 134512640 135167914 3221224448 3221219644 134723291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4101 3531 162 162 0 3939 0
[pid=5096] vsize: 16404
Current children cumulated CPU time (s) 89.76
Current children cumulated vsize (Kb) 18532

[startup+100.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3793 0 0 0 9951 23 0 0 25 0 1 0 1844166844 16797696 3531 4294967295 134512640 135167914 3221224448 3221218836 134629267 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4101 3531 162 162 0 3939 0
[pid=5096] vsize: 16404
Current children cumulated CPU time (s) 99.76
Current children cumulated vsize (Kb) 18532

[startup+110.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3793 0 0 0 10951 23 0 0 25 0 1 0 1844166844 16797696 3531 4294967295 134512640 135167914 3221224448 3221220928 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4101 3531 162 162 0 3939 0
[pid=5096] vsize: 16404
Current children cumulated CPU time (s) 109.76
Current children cumulated vsize (Kb) 18532

[startup+120.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3793 0 0 0 11952 23 0 0 25 0 1 0 1844166844 16797696 3531 4294967295 134512640 135167914 3221224448 3221220416 134631247 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4101 3531 162 162 0 3939 0
[pid=5096] vsize: 16404
Current children cumulated CPU time (s) 119.77
Current children cumulated vsize (Kb) 18532

[startup+130.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3793 0 0 0 12952 23 0 0 25 0 1 0 1844166844 16797696 3531 4294967295 134512640 135167914 3221224448 3221219984 134696264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4101 3531 162 162 0 3939 0
[pid=5096] vsize: 16404
Current children cumulated CPU time (s) 129.77
Current children cumulated vsize (Kb) 18532

[startup+140.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3793 0 0 0 13952 23 0 0 25 0 1 0 1844166844 16797696 3531 4294967295 134512640 135167914 3221224448 3221220184 134844674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4101 3531 162 162 0 3939 0
[pid=5096] vsize: 16404
Current children cumulated CPU time (s) 139.77
Current children cumulated vsize (Kb) 18532

[startup+150.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3904 0 0 0 14952 23 0 0 25 0 1 0 1844166844 17059840 3600 4294967295 134512640 135167914 3221224448 3221218000 134844672 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4165 3600 162 162 0 4003 0
[pid=5096] vsize: 16660
Current children cumulated CPU time (s) 149.77
Current children cumulated vsize (Kb) 18788

[startup+160.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3904 0 0 0 15952 24 0 0 25 0 1 0 1844166844 17059840 3600 4294967295 134512640 135167914 3221224448 3221218048 134843068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4165 3600 162 162 0 4003 0
[pid=5096] vsize: 16660
Current children cumulated CPU time (s) 159.78
Current children cumulated vsize (Kb) 18788

[startup+170.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3904 0 0 0 16952 24 0 0 25 0 1 0 1844166844 17059840 3600 4294967295 134512640 135167914 3221224448 3221218608 134722539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4165 3600 162 162 0 4003 0
[pid=5096] vsize: 16660
Current children cumulated CPU time (s) 169.78
Current children cumulated vsize (Kb) 18788

[startup+180.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3904 0 0 0 17952 24 0 0 25 0 1 0 1844166844 17059840 3600 4294967295 134512640 135167914 3221224448 3221218384 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4165 3600 162 162 0 4003 0
[pid=5096] vsize: 16660
Current children cumulated CPU time (s) 179.78
Current children cumulated vsize (Kb) 18788

[startup+190.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3904 0 0 0 18952 24 0 0 25 0 1 0 1844166844 17059840 3600 4294967295 134512640 135167914 3221224448 3221219660 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4165 3600 162 162 0 4003 0
[pid=5096] vsize: 16660
Current children cumulated CPU time (s) 189.78
Current children cumulated vsize (Kb) 18788

[startup+200.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3904 0 0 0 19952 24 0 0 25 0 1 0 1844166844 17059840 3600 4294967295 134512640 135167914 3221224448 3221219484 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4165 3600 162 162 0 4003 0
[pid=5096] vsize: 16660
Current children cumulated CPU time (s) 199.78
Current children cumulated vsize (Kb) 18788

[startup+210.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3904 0 0 0 20953 24 0 0 25 0 1 0 1844166844 17059840 3600 4294967295 134512640 135167914 3221224448 3221220784 134629196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4165 3600 162 162 0 4003 0
[pid=5096] vsize: 16660
Current children cumulated CPU time (s) 209.79
Current children cumulated vsize (Kb) 18788

[startup+220.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3904 0 0 0 21953 24 0 0 25 0 1 0 1844166844 17059840 3600 4294967295 134512640 135167914 3221224448 3221220204 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4165 3600 162 162 0 4003 0
[pid=5096] vsize: 16660
Current children cumulated CPU time (s) 219.79
Current children cumulated vsize (Kb) 18788

[startup+230.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3904 0 0 0 22953 24 0 0 25 0 1 0 1844166844 17059840 3600 4294967295 134512640 135167914 3221224448 3221220028 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4165 3600 162 162 0 4003 0
[pid=5096] vsize: 16660
Current children cumulated CPU time (s) 229.79
Current children cumulated vsize (Kb) 18788

[startup+240.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3904 0 0 0 23953 24 0 0 25 0 1 0 1844166844 17059840 3600 4294967295 134512640 135167914 3221224448 3221221436 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4165 3600 162 162 0 4003 0
[pid=5096] vsize: 16660
Current children cumulated CPU time (s) 239.79
Current children cumulated vsize (Kb) 18788

[startup+250.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3904 0 0 0 24953 24 0 0 25 0 1 0 1844166844 17059840 3600 4294967295 134512640 135167914 3221224448 3221221904 134843010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4165 3600 162 162 0 4003 0
[pid=5096] vsize: 16660
Current children cumulated CPU time (s) 249.79
Current children cumulated vsize (Kb) 18788

[startup+260.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3904 0 0 0 25954 24 0 0 25 0 1 0 1844166844 17059840 3600 4294967295 134512640 135167914 3221224448 3221219616 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4165 3600 162 162 0 4003 0
[pid=5096] vsize: 16660
Current children cumulated CPU time (s) 259.8
Current children cumulated vsize (Kb) 18788

[startup+270.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3904 0 0 0 26954 24 0 0 25 0 1 0 1844166844 17059840 3600 4294967295 134512640 135167914 3221224448 3221219968 134844676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4165 3600 162 162 0 4003 0
[pid=5096] vsize: 16660
Current children cumulated CPU time (s) 269.8
Current children cumulated vsize (Kb) 18788

[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 3904 0 0 0 27954 24 0 0 25 0 1 0 1844166844 17059840 3600 4294967295 134512640 135167914 3221224448 3221220144 134844736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4165 3600 162 162 0 4003 0
[pid=5096] vsize: 16660
Current children cumulated CPU time (s) 279.8
Current children cumulated vsize (Kb) 18788

[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4006 0 0 0 28954 24 0 0 25 0 1 0 1844166844 17453056 3660 4294967295 134512640 135167914 3221224448 3221218112 134693576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4261 3660 162 162 0 4099 0
[pid=5096] vsize: 17044
Current children cumulated CPU time (s) 289.8
Current children cumulated vsize (Kb) 19172

[startup+300.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4006 0 0 0 29954 24 0 0 25 0 1 0 1844166844 17453056 3660 4294967295 134512640 135167914 3221224448 3221219552 134629488 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4261 3660 162 162 0 4099 0
[pid=5096] vsize: 17044
Current children cumulated CPU time (s) 299.8
Current children cumulated vsize (Kb) 19172

[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4006 0 0 0 30955 24 0 0 25 0 1 0 1844166844 17453056 3660 4294967295 134512640 135167914 3221224448 3221219680 134522732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4261 3660 162 162 0 4099 0
[pid=5096] vsize: 17044
Current children cumulated CPU time (s) 309.81
Current children cumulated vsize (Kb) 19172

[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4006 0 0 0 31955 24 0 0 25 0 1 0 1844166844 17453056 3660 4294967295 134512640 135167914 3221224448 3221219264 134844708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4261 3660 162 162 0 4099 0
[pid=5096] vsize: 17044
Current children cumulated CPU time (s) 319.81
Current children cumulated vsize (Kb) 19172

[startup+330.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4006 0 0 0 32955 24 0 0 25 0 1 0 1844166844 17453056 3660 4294967295 134512640 135167914 3221224448 3221220928 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4261 3660 162 162 0 4099 0
[pid=5096] vsize: 17044
Current children cumulated CPU time (s) 329.81
Current children cumulated vsize (Kb) 19172

[startup+340.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4006 0 0 0 33955 24 0 0 25 0 1 0 1844166844 17453056 3660 4294967295 134512640 135167914 3221224448 3221219504 134843402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4261 3660 162 162 0 4099 0
[pid=5096] vsize: 17044
Current children cumulated CPU time (s) 339.81
Current children cumulated vsize (Kb) 19172

[startup+350.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4006 0 0 0 34955 24 0 0 25 0 1 0 1844166844 17453056 3660 4294967295 134512640 135167914 3221224448 3221219984 134696590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4261 3660 162 162 0 4099 0
[pid=5096] vsize: 17044
Current children cumulated CPU time (s) 349.81
Current children cumulated vsize (Kb) 19172

[startup+360.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4006 0 0 0 35956 24 0 0 25 0 1 0 1844166844 17453056 3660 4294967295 134512640 135167914 3221224448 3221221440 134843074 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4261 3660 162 162 0 4099 0
[pid=5096] vsize: 17044
Current children cumulated CPU time (s) 359.82
Current children cumulated vsize (Kb) 19172

[startup+370.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4006 0 0 0 36956 24 0 0 25 0 1 0 1844166844 17453056 3660 4294967295 134512640 135167914 3221224448 3221220896 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4261 3660 162 162 0 4099 0
[pid=5096] vsize: 17044
Current children cumulated CPU time (s) 369.82
Current children cumulated vsize (Kb) 19172

[startup+380.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4006 0 0 0 37956 24 0 0 25 0 1 0 1844166844 17453056 3660 4294967295 134512640 135167914 3221224448 3221220256 134629328 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4261 3660 162 162 0 4099 0
[pid=5096] vsize: 17044
Current children cumulated CPU time (s) 379.82
Current children cumulated vsize (Kb) 19172

[startup+390.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4006 0 0 0 38956 24 0 0 25 0 1 0 1844166844 17453056 3660 4294967295 134512640 135167914 3221224448 3221220960 134631232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4261 3660 162 162 0 4099 0
[pid=5096] vsize: 17044
Current children cumulated CPU time (s) 389.82
Current children cumulated vsize (Kb) 19172

[startup+400.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4006 0 0 0 39957 24 0 0 25 0 1 0 1844166844 17453056 3660 4294967295 134512640 135167914 3221224448 3221220364 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4261 3660 162 162 0 4099 0
[pid=5096] vsize: 17044
Current children cumulated CPU time (s) 399.83
Current children cumulated vsize (Kb) 19172

[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4006 0 0 0 40957 24 0 0 25 0 1 0 1844166844 17453056 3660 4294967295 134512640 135167914 3221224448 3221222528 134630858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4261 3660 162 162 0 4099 0
[pid=5096] vsize: 17044
Current children cumulated CPU time (s) 409.83
Current children cumulated vsize (Kb) 19172

[startup+420.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4006 0 0 0 41957 24 0 0 25 0 1 0 1844166844 17453056 3660 4294967295 134512640 135167914 3221224448 3221219356 134522320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4261 3660 162 162 0 4099 0
[pid=5096] vsize: 17044
Current children cumulated CPU time (s) 419.83
Current children cumulated vsize (Kb) 19172

[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4199 0 0 0 42957 25 0 0 25 0 1 0 1844166844 17793024 3769 4294967295 134512640 135167914 3221224448 3221218208 134844668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4344 3769 162 162 0 4182 0
[pid=5096] vsize: 17376
Current children cumulated CPU time (s) 429.84
Current children cumulated vsize (Kb) 19504

[startup+440.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4199 0 0 0 43957 25 0 0 25 0 1 0 1844166844 17793024 3769 4294967295 134512640 135167914 3221224448 3221219504 134843404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4344 3769 162 162 0 4182 0
[pid=5096] vsize: 17376
Current children cumulated CPU time (s) 439.84
Current children cumulated vsize (Kb) 19504

[startup+450.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4199 0 0 0 44957 25 0 0 25 0 1 0 1844166844 17793024 3769 4294967295 134512640 135167914 3221224448 3221218976 134843400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4344 3769 162 162 0 4182 0
[pid=5096] vsize: 17376
Current children cumulated CPU time (s) 449.84
Current children cumulated vsize (Kb) 19504

[startup+460.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4199 0 0 0 45957 25 0 0 25 0 1 0 1844166844 17793024 3769 4294967295 134512640 135167914 3221224448 3221219684 134849086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4344 3769 162 162 0 4182 0
[pid=5096] vsize: 17376
Current children cumulated CPU time (s) 459.84
Current children cumulated vsize (Kb) 19504

[startup+470.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4199 0 0 0 46957 25 0 0 25 0 1 0 1844166844 17793024 3769 4294967295 134512640 135167914 3221224448 3221219728 134844720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4344 3769 162 162 0 4182 0
[pid=5096] vsize: 17376
Current children cumulated CPU time (s) 469.84
Current children cumulated vsize (Kb) 19504

[startup+480.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4199 0 0 0 47958 25 0 0 25 0 1 0 1844166844 17793024 3769 4294967295 134512640 135167914 3221224448 3221220752 134849163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4344 3769 162 162 0 4182 0
[pid=5096] vsize: 17376
Current children cumulated CPU time (s) 479.85
Current children cumulated vsize (Kb) 19504

[startup+490.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4199 0 0 0 48958 25 0 0 25 0 1 0 1844166844 17793024 3769 4294967295 134512640 135167914 3221224448 3221220856 134693626 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4344 3769 162 162 0 4182 0
[pid=5096] vsize: 17376
Current children cumulated CPU time (s) 489.85
Current children cumulated vsize (Kb) 19504

[startup+500.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4199 0 0 0 49958 25 0 0 25 0 1 0 1844166844 17793024 3769 4294967295 134512640 135167914 3221224448 3221220384 134849102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4344 3769 162 162 0 4182 0
[pid=5096] vsize: 17376
Current children cumulated CPU time (s) 499.85
Current children cumulated vsize (Kb) 19504

[startup+510.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4199 0 0 0 50958 25 0 0 25 0 1 0 1844166844 17793024 3769 4294967295 134512640 135167914 3221224448 3221220016 134522341 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4344 3769 162 162 0 4182 0
[pid=5096] vsize: 17376
Current children cumulated CPU time (s) 509.85
Current children cumulated vsize (Kb) 19504

[startup+520.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4199 0 0 0 51959 25 0 0 25 0 1 0 1844166844 17793024 3769 4294967295 134512640 135167914 3221224448 3221220556 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4344 3769 162 162 0 4182 0
[pid=5096] vsize: 17376
Current children cumulated CPU time (s) 519.86
Current children cumulated vsize (Kb) 19504

[startup+530.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4199 0 0 0 52959 25 0 0 25 0 1 0 1844166844 17793024 3769 4294967295 134512640 135167914 3221224448 3221220208 134694524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4344 3769 162 162 0 4182 0
[pid=5096] vsize: 17376
Current children cumulated CPU time (s) 529.86
Current children cumulated vsize (Kb) 19504

[startup+540.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4199 0 0 0 53959 25 0 0 25 0 1 0 1844166844 17793024 3769 4294967295 134512640 135167914 3221224448 3221218848 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4344 3769 162 162 0 4182 0
[pid=5096] vsize: 17376
Current children cumulated CPU time (s) 539.86
Current children cumulated vsize (Kb) 19504

[startup+550.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4199 0 0 0 54959 25 0 0 25 0 1 0 1844166844 17793024 3769 4294967295 134512640 135167914 3221224448 3221220928 134693566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4344 3769 162 162 0 4182 0
[pid=5096] vsize: 17376
Current children cumulated CPU time (s) 549.86
Current children cumulated vsize (Kb) 19504

[startup+560.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4199 0 0 0 55959 25 0 0 25 0 1 0 1844166844 17793024 3769 4294967295 134512640 135167914 3221224448 3221222320 134843107 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4344 3769 162 162 0 4182 0
[pid=5096] vsize: 17376
Current children cumulated CPU time (s) 559.86
Current children cumulated vsize (Kb) 19504

[startup+570.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4313 0 0 0 56959 25 0 0 25 0 1 0 1844166844 18370560 3841 4294967295 134512640 135167914 3221224448 3221218892 134844638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4485 3841 162 162 0 4323 0
[pid=5096] vsize: 17940
Current children cumulated CPU time (s) 569.86
Current children cumulated vsize (Kb) 20068

[startup+580.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4313 0 0 0 57959 25 0 0 25 0 1 0 1844166844 18370560 3841 4294967295 134512640 135167914 3221224448 3221218192 134845890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4485 3841 162 162 0 4323 0
[pid=5096] vsize: 17940
Current children cumulated CPU time (s) 579.86
Current children cumulated vsize (Kb) 20068

[startup+590.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4313 0 0 0 58960 25 0 0 25 0 1 0 1844166844 18370560 3841 4294967295 134512640 135167914 3221224448 3221219136 134843118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4485 3841 162 162 0 4323 0
[pid=5096] vsize: 17940
Current children cumulated CPU time (s) 589.87
Current children cumulated vsize (Kb) 20068

[startup+600.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4313 0 0 0 59960 25 0 0 25 0 1 0 1844166844 18370560 3841 4294967295 134512640 135167914 3221224448 3221219680 134694444 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4485 3841 162 162 0 4323 0
[pid=5096] vsize: 17940
Current children cumulated CPU time (s) 599.87
Current children cumulated vsize (Kb) 20068

[startup+610.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4313 0 0 0 60960 25 0 0 25 0 1 0 1844166844 18370560 3841 4294967295 134512640 135167914 3221224448 3221219004 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4485 3841 162 162 0 4323 0
[pid=5096] vsize: 17940
Current children cumulated CPU time (s) 609.87
Current children cumulated vsize (Kb) 20068

[startup+620.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4313 0 0 0 61960 25 0 0 25 0 1 0 1844166844 18370560 3841 4294967295 134512640 135167914 3221224448 3221221488 134844668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4485 3841 162 162 0 4323 0
[pid=5096] vsize: 17940
Current children cumulated CPU time (s) 619.87
Current children cumulated vsize (Kb) 20068

[startup+630.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4313 0 0 0 62961 25 0 0 25 0 1 0 1844166844 18370560 3841 4294967295 134512640 135167914 3221224448 3221219392 134844706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4485 3841 162 162 0 4323 0
[pid=5096] vsize: 17940
Current children cumulated CPU time (s) 629.88
Current children cumulated vsize (Kb) 20068

[startup+640.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4313 0 0 0 63961 25 0 0 25 0 1 0 1844166844 18370560 3841 4294967295 134512640 135167914 3221224448 3221219088 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4485 3841 162 162 0 4323 0
[pid=5096] vsize: 17940
Current children cumulated CPU time (s) 639.88
Current children cumulated vsize (Kb) 20068

[startup+650.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4313 0 0 0 64961 25 0 0 25 0 1 0 1844166844 18370560 3841 4294967295 134512640 135167914 3221224448 3221219872 134849066 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4485 3841 162 162 0 4323 0
[pid=5096] vsize: 17940
Current children cumulated CPU time (s) 649.88
Current children cumulated vsize (Kb) 20068

[startup+660.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4313 0 0 0 65961 25 0 0 25 0 1 0 1844166844 18370560 3841 4294967295 134512640 135167914 3221224448 3221220272 134844653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4485 3841 162 162 0 4323 0
[pid=5096] vsize: 17940
Current children cumulated CPU time (s) 659.88
Current children cumulated vsize (Kb) 20068

[startup+670.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4313 0 0 0 66962 25 0 0 25 0 1 0 1844166844 18370560 3841 4294967295 134512640 135167914 3221224448 3221220688 134696590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4485 3841 162 162 0 4323 0
[pid=5096] vsize: 17940
Current children cumulated CPU time (s) 669.89
Current children cumulated vsize (Kb) 20068

[startup+680.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4313 0 0 0 67962 25 0 0 25 0 1 0 1844166844 18370560 3841 4294967295 134512640 135167914 3221224448 3221221040 134696581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4485 3841 162 162 0 4323 0
[pid=5096] vsize: 17940
Current children cumulated CPU time (s) 679.89
Current children cumulated vsize (Kb) 20068

[startup+690.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4313 0 0 0 68962 25 0 0 25 0 1 0 1844166844 18370560 3841 4294967295 134512640 135167914 3221224448 3221220640 134844672 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4485 3841 162 162 0 4323 0
[pid=5096] vsize: 17940
Current children cumulated CPU time (s) 689.89
Current children cumulated vsize (Kb) 20068

[startup+700.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4313 0 0 0 69962 25 0 0 25 0 1 0 1844166844 18370560 3841 4294967295 134512640 135167914 3221224448 3221221304 134629265 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4485 3841 162 162 0 4323 0
[pid=5096] vsize: 17940
Current children cumulated CPU time (s) 699.89
Current children cumulated vsize (Kb) 20068

[startup+710.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4591 0 0 0 70961 26 0 0 25 0 1 0 1844166844 18890752 3994 4294967295 134512640 135167914 3221224448 3221218320 134844736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4612 3994 162 162 0 4450 0
[pid=5096] vsize: 18448
Current children cumulated CPU time (s) 709.89
Current children cumulated vsize (Kb) 20576

[startup+720.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4591 0 0 0 71962 26 0 0 25 0 1 0 1844166844 18890752 3994 4294967295 134512640 135167914 3221224448 3221218384 134845930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4612 3994 162 162 0 4450 0
[pid=5096] vsize: 18448
Current children cumulated CPU time (s) 719.9
Current children cumulated vsize (Kb) 20576

[startup+730.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4591 0 0 0 72962 26 0 0 25 0 1 0 1844166844 18890752 3994 4294967295 134512640 135167914 3221224448 3221220056 134842997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4612 3994 162 162 0 4450 0
[pid=5096] vsize: 18448
Current children cumulated CPU time (s) 729.9
Current children cumulated vsize (Kb) 20576

[startup+740.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4591 0 0 0 73962 26 0 0 25 0 1 0 1844166844 18890752 3994 4294967295 134512640 135167914 3221224448 3221219708 134693552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4612 3994 162 162 0 4450 0
[pid=5096] vsize: 18448
Current children cumulated CPU time (s) 739.9
Current children cumulated vsize (Kb) 20576

[startup+750.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4591 0 0 0 74962 26 0 0 25 0 1 0 1844166844 18890752 3994 4294967295 134512640 135167914 3221224448 3221220936 134843032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4612 3994 162 162 0 4450 0
[pid=5096] vsize: 18448
Current children cumulated CPU time (s) 749.9
Current children cumulated vsize (Kb) 20576

[startup+760.041 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4591 0 0 0 75962 26 0 0 25 0 1 0 1844166844 18890752 3994 4294967295 134512640 135167914 3221224448 3221219324 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4612 3994 162 162 0 4450 0
[pid=5096] vsize: 18448
Current children cumulated CPU time (s) 759.9
Current children cumulated vsize (Kb) 20576

[startup+770.042 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4591 0 0 0 76963 26 0 0 25 0 1 0 1844166844 18890752 3994 4294967295 134512640 135167914 3221224448 3221220164 134849060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4612 3994 162 162 0 4450 0
[pid=5096] vsize: 18448
Current children cumulated CPU time (s) 769.91
Current children cumulated vsize (Kb) 20576

[startup+780.042 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4591 0 0 0 77963 26 0 0 25 0 1 0 1844166844 18890752 3994 4294967295 134512640 135167914 3221224448 3221221408 134695307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4612 3994 162 162 0 4450 0
[pid=5096] vsize: 18448
Current children cumulated CPU time (s) 779.91
Current children cumulated vsize (Kb) 20576

[startup+790.042 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4591 0 0 0 78963 26 0 0 25 0 1 0 1844166844 18890752 3994 4294967295 134512640 135167914 3221224448 3221221632 134849187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4612 3994 162 162 0 4450 0
[pid=5096] vsize: 18448
Current children cumulated CPU time (s) 789.91
Current children cumulated vsize (Kb) 20576

[startup+800.042 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4591 0 0 0 79963 26 0 0 25 0 1 0 1844166844 18890752 3994 4294967295 134512640 135167914 3221224448 3221219472 134695274 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4612 3994 162 162 0 4450 0
[pid=5096] vsize: 18448
Current children cumulated CPU time (s) 799.91
Current children cumulated vsize (Kb) 20576

[startup+810.043 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4591 0 0 0 80963 26 0 0 25 0 1 0 1844166844 18890752 3994 4294967295 134512640 135167914 3221224448 3221220340 134723220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4612 3994 162 162 0 4450 0
[pid=5096] vsize: 18448
Current children cumulated CPU time (s) 809.91
Current children cumulated vsize (Kb) 20576

[startup+820.043 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4591 0 0 0 81964 26 0 0 25 0 1 0 1844166844 18890752 3994 4294967295 134512640 135167914 3221224448 3221221552 134844718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4612 3994 162 162 0 4450 0
[pid=5096] vsize: 18448
Current children cumulated CPU time (s) 819.92
Current children cumulated vsize (Kb) 20576

[startup+830.043 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4591 0 0 0 82964 26 0 0 25 0 1 0 1844166844 18890752 3994 4294967295 134512640 135167914 3221224448 3221221200 134845913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4612 3994 162 162 0 4450 0
[pid=5096] vsize: 18448
Current children cumulated CPU time (s) 829.92
Current children cumulated vsize (Kb) 20576

[startup+840.044 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4591 0 0 0 83964 26 0 0 25 0 1 0 1844166844 18890752 3994 4294967295 134512640 135167914 3221224448 3221220720 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4612 3994 162 162 0 4450 0
[pid=5096] vsize: 18448
Current children cumulated CPU time (s) 839.92
Current children cumulated vsize (Kb) 20576

[startup+850.044 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4711 0 0 0 84964 27 0 0 25 0 1 0 1844166844 19091456 4072 4294967295 134512640 135167914 3221224448 3221219152 134843015 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4661 4072 162 162 0 4499 0
[pid=5096] vsize: 18644
Current children cumulated CPU time (s) 849.93
Current children cumulated vsize (Kb) 20772

[startup+860.045 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4711 0 0 0 85964 27 0 0 25 0 1 0 1844166844 19091456 4072 4294967295 134512640 135167914 3221224448 3221220960 134630866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4661 4072 162 162 0 4499 0
[pid=5096] vsize: 18644
Current children cumulated CPU time (s) 859.93
Current children cumulated vsize (Kb) 20772

[startup+870.046 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4711 0 0 0 86964 27 0 0 25 0 1 0 1844166844 19091456 4072 4294967295 134512640 135167914 3221224448 3221219356 134694551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4661 4072 162 162 0 4499 0
[pid=5096] vsize: 18644
Current children cumulated CPU time (s) 869.93
Current children cumulated vsize (Kb) 20772

[startup+880.046 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4711 0 0 0 87964 27 0 0 25 0 1 0 1844166844 19091456 4072 4294967295 134512640 135167914 3221224448 3221220048 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4661 4072 162 162 0 4499 0
[pid=5096] vsize: 18644
Current children cumulated CPU time (s) 879.93
Current children cumulated vsize (Kb) 20772

[startup+890.047 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4711 0 0 0 88964 27 0 0 25 0 1 0 1844166844 19091456 4072 4294967295 134512640 135167914 3221224448 3221220740 134849060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4661 4072 162 162 0 4499 0
[pid=5096] vsize: 18644
Current children cumulated CPU time (s) 889.93
Current children cumulated vsize (Kb) 20772

[startup+900.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4711 0 0 0 89965 27 0 0 25 0 1 0 1844166844 19091456 4072 4294967295 134512640 135167914 3221224448 3221220532 134845880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4661 4072 162 162 0 4499 0
[pid=5096] vsize: 18644
Current children cumulated CPU time (s) 899.94
Current children cumulated vsize (Kb) 20772

[startup+910.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4711 0 0 0 90965 27 0 0 25 0 1 0 1844166844 19091456 4072 4294967295 134512640 135167914 3221224448 3221219688 134849057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4661 4072 162 162 0 4499 0
[pid=5096] vsize: 18644
Current children cumulated CPU time (s) 909.94
Current children cumulated vsize (Kb) 20772

[startup+920.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4711 0 0 0 91965 27 0 0 25 0 1 0 1844166844 19091456 4072 4294967295 134512640 135167914 3221224448 3221221744 134843001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4661 4072 162 162 0 4499 0
[pid=5096] vsize: 18644
Current children cumulated CPU time (s) 919.94
Current children cumulated vsize (Kb) 20772

[startup+930.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4711 0 0 0 92965 27 0 0 25 0 1 0 1844166844 19091456 4072 4294967295 134512640 135167914 3221224448 3221221072 134845881 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4661 4072 162 162 0 4499 0
[pid=5096] vsize: 18644
Current children cumulated CPU time (s) 929.94
Current children cumulated vsize (Kb) 20772

[startup+940.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4711 0 0 0 93966 27 0 0 25 0 1 0 1844166844 19091456 4072 4294967295 134512640 135167914 3221224448 3221222160 134522325 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4661 4072 162 162 0 4499 0
[pid=5096] vsize: 18644
Current children cumulated CPU time (s) 939.95
Current children cumulated vsize (Kb) 20772

[startup+950.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4711 0 0 0 94966 27 0 0 25 0 1 0 1844166844 19091456 4072 4294967295 134512640 135167914 3221224448 3221220720 134522834 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4661 4072 162 162 0 4499 0
[pid=5096] vsize: 18644
Current children cumulated CPU time (s) 949.95
Current children cumulated vsize (Kb) 20772

[startup+960.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4711 0 0 0 95966 27 0 0 25 0 1 0 1844166844 19091456 4072 4294967295 134512640 135167914 3221224448 3221220336 134696217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4661 4072 162 162 0 4499 0
[pid=5096] vsize: 18644
Current children cumulated CPU time (s) 959.95
Current children cumulated vsize (Kb) 20772

[startup+970.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4711 0 0 0 96966 27 0 0 25 0 1 0 1844166844 19091456 4072 4294967295 134512640 135167914 3221224448 3221220512 134843402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4661 4072 162 162 0 4499 0
[pid=5096] vsize: 18644
Current children cumulated CPU time (s) 969.95
Current children cumulated vsize (Kb) 20772

[startup+980.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4711 0 0 0 97966 27 0 0 25 0 1 0 1844166844 19091456 4072 4294967295 134512640 135167914 3221224448 3221220496 134844725 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4661 4072 162 162 0 4499 0
[pid=5096] vsize: 18644
Current children cumulated CPU time (s) 979.95
Current children cumulated vsize (Kb) 20772

[startup+990.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4824 0 0 0 98966 28 0 0 25 0 1 0 1844166844 20062208 4143 4294967295 134512640 135167914 3221224448 3221219280 134696264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4898 4143 162 162 0 4736 0
[pid=5096] vsize: 19592
Current children cumulated CPU time (s) 989.96
Current children cumulated vsize (Kb) 21720

[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4824 0 0 0 99966 28 0 0 25 0 1 0 1844166844 20062208 4143 4294967295 134512640 135167914 3221224448 3221219824 134693582 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4898 4143 162 162 0 4736 0
[pid=5096] vsize: 19592
Current children cumulated CPU time (s) 999.96
Current children cumulated vsize (Kb) 21720

[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4824 0 0 0 100966 28 0 0 25 0 1 0 1844166844 20062208 4143 4294967295 134512640 135167914 3221224448 3221219440 134845903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4898 4143 162 162 0 4736 0
[pid=5096] vsize: 19592
Current children cumulated CPU time (s) 1009.96
Current children cumulated vsize (Kb) 21720

[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4824 0 0 0 101967 28 0 0 25 0 1 0 1844166844 20062208 4143 4294967295 134512640 135167914 3221224448 3221219120 134720495 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4898 4143 162 162 0 4736 0
[pid=5096] vsize: 19592
Current children cumulated CPU time (s) 1019.97
Current children cumulated vsize (Kb) 21720

[startup+1030.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4824 0 0 0 102967 28 0 0 25 0 1 0 1844166844 20062208 4143 4294967295 134512640 135167914 3221224448 3221218464 134849163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4898 4143 162 162 0 4736 0
[pid=5096] vsize: 19592
Current children cumulated CPU time (s) 1029.97
Current children cumulated vsize (Kb) 21720

[startup+1040.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4824 0 0 0 103967 28 0 0 25 0 1 0 1844166844 20062208 4143 4294967295 134512640 135167914 3221224448 3221218828 134522235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4898 4143 162 162 0 4736 0
[pid=5096] vsize: 19592
Current children cumulated CPU time (s) 1039.97
Current children cumulated vsize (Kb) 21720

[startup+1050.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4824 0 0 0 104967 28 0 0 25 0 1 0 1844166844 20062208 4143 4294967295 134512640 135167914 3221224448 3221221012 134845880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4898 4143 162 162 0 4736 0
[pid=5096] vsize: 19592
Current children cumulated CPU time (s) 1049.97
Current children cumulated vsize (Kb) 21720

[startup+1060.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4824 0 0 0 105967 28 0 0 25 0 1 0 1844166844 20062208 4143 4294967295 134512640 135167914 3221224448 3221220320 134845906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4898 4143 162 162 0 4736 0
[pid=5096] vsize: 19592
Current children cumulated CPU time (s) 1059.97
Current children cumulated vsize (Kb) 21720

[startup+1070.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4824 0 0 0 106968 28 0 0 25 0 1 0 1844166844 20062208 4143 4294967295 134512640 135167914 3221224448 3221218736 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4898 4143 162 162 0 4736 0
[pid=5096] vsize: 19592
Current children cumulated CPU time (s) 1069.98
Current children cumulated vsize (Kb) 21720

[startup+1080.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4824 0 0 0 107968 28 0 0 25 0 1 0 1844166844 20062208 4143 4294967295 134512640 135167914 3221224448 3221220360 134844674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4898 4143 162 162 0 4736 0
[pid=5096] vsize: 19592
Current children cumulated CPU time (s) 1079.98
Current children cumulated vsize (Kb) 21720

[startup+1090.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4824 0 0 0 108968 28 0 0 25 0 1 0 1844166844 20062208 4143 4294967295 134512640 135167914 3221224448 3221221408 134844637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4898 4143 162 162 0 4736 0
[pid=5096] vsize: 19592
Current children cumulated CPU time (s) 1089.98
Current children cumulated vsize (Kb) 21720

[startup+1100.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4824 0 0 0 109968 28 0 0 25 0 1 0 1844166844 20062208 4143 4294967295 134512640 135167914 3221224448 3221221360 134845930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4898 4143 162 162 0 4736 0
[pid=5096] vsize: 19592
Current children cumulated CPU time (s) 1099.98
Current children cumulated vsize (Kb) 21720

[startup+1110.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4824 0 0 0 110969 28 0 0 25 0 1 0 1844166844 20062208 4143 4294967295 134512640 135167914 3221224448 3221220672 134844694 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4898 4143 162 162 0 4736 0
[pid=5096] vsize: 19592
Current children cumulated CPU time (s) 1109.99
Current children cumulated vsize (Kb) 21720

[startup+1120.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4879 0 0 0 111968 28 0 0 25 0 1 0 1844166844 20193280 4198 4294967295 134512640 135167914 3221224448 3221206332 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4930 4198 162 162 0 4768 0
[pid=5096] vsize: 19720
Current children cumulated CPU time (s) 1119.98
Current children cumulated vsize (Kb) 21848

[startup+1130.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4974 0 0 0 112968 28 0 0 25 0 1 0 1844166844 20246528 4215 4294967295 134512640 135167914 3221224448 3221219424 134845924 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4943 4215 162 162 0 4781 0
[pid=5096] vsize: 19772
Current children cumulated CPU time (s) 1129.98
Current children cumulated vsize (Kb) 21900

[startup+1140.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4974 0 0 0 113968 28 0 0 25 0 1 0 1844166844 20246528 4215 4294967295 134512640 135167914 3221224448 3221220588 134694480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4943 4215 162 162 0 4781 0
[pid=5096] vsize: 19772
Current children cumulated CPU time (s) 1139.98
Current children cumulated vsize (Kb) 21900

[startup+1150.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4974 0 0 0 114969 28 0 0 25 0 1 0 1844166844 20246528 4215 4294967295 134512640 135167914 3221224448 3221218896 134845930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4943 4215 162 162 0 4781 0
[pid=5096] vsize: 19772
Current children cumulated CPU time (s) 1149.99
Current children cumulated vsize (Kb) 21900

[startup+1160.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4974 0 0 0 115969 29 0 0 25 0 1 0 1844166844 20246528 4215 4294967295 134512640 135167914 3221224448 3221220172 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4943 4215 162 162 0 4781 0
[pid=5096] vsize: 19772
Current children cumulated CPU time (s) 1160
Current children cumulated vsize (Kb) 21900

[startup+1170.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4974 0 0 0 116969 29 0 0 25 0 1 0 1844166844 20246528 4215 4294967295 134512640 135167914 3221224448 3221220212 134849147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4943 4215 162 162 0 4781 0
[pid=5096] vsize: 19772
Current children cumulated CPU time (s) 1170
Current children cumulated vsize (Kb) 21900

[startup+1180.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4974 0 0 0 117969 29 0 0 25 0 1 0 1844166844 20246528 4215 4294967295 134512640 135167914 3221224448 3221219532 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4943 4215 162 162 0 4781 0
[pid=5096] vsize: 19772
Current children cumulated CPU time (s) 1180
Current children cumulated vsize (Kb) 21900

[startup+1190.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4974 0 0 0 118969 29 0 0 25 0 1 0 1844166844 20246528 4215 4294967295 134512640 135167914 3221224448 3221221100 134722656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4943 4215 162 162 0 4781 0
[pid=5096] vsize: 19772
Current children cumulated CPU time (s) 1190
Current children cumulated vsize (Kb) 21900

[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4974 0 0 0 119969 29 0 0 25 0 1 0 1844166844 20246528 4215 4294967295 134512640 135167914 3221224448 3221221012 134843117 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4943 4215 162 162 0 4781 0
[pid=5096] vsize: 19772
Current children cumulated CPU time (s) 1200
Current children cumulated vsize (Kb) 21900



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 5096
Raw data (/proc/5091/stat): 5091 (minisat+_script) S 5090 5091 20115 0 -1 0 314 331 0 0 0 1 0 1 16 0 1 0 1844166837 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5091/statm): 532 234 485 147 0 385 0
[pid=5091] vsize: 2128
Raw data (/proc/5096/stat): 5096 (minisat+_bignum) R 5091 5091 20115 0 -1 0 4974 0 0 0 119969 29 0 0 25 0 1 0 1844166844 20246528 4215 4294967295 134512640 135167914 3221224448 3221221024 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5096/statm): 4943 4215 162 162 0 4781 0
[pid=5096] vsize: 19772
Current children cumulated CPU time (s) 1200
Current children cumulated vsize (Kb) 21900

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

Child status: 0
Real time (s): 1200.08
CPU time (s): 1200
CPU user time (s): 1199.7
CPU system time (s): 0.300954
CPU usage (%): 99.9936
Max. virtual memory (cumulated for all children) (Kb): 21900

Verifier Data

ERROR: no interpretation found !