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-blend.opb
MD5SUMc063ddfef33c4e28cf3156e6931d679b
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 0
Optimality of the best value was proved NO
Number of terms in the objective function 660
Biggest coefficient in the objective function 14388140441600
Number of bits for the biggest coefficient in the objective function 44
Sum of the numbers in the objective function 203610440670021
Number of bits of the sum of numbers in the objective function 48
Biggest number in a constraint 78436840243200
Number of bits of the biggest number in a constraint 47
Biggest sum of numbers in a constraint 789015556311444
Number of bits of the biggest sum of numbers50
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1229
Number of variables2490
Total number of constraints74
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 constraints74
Minimum length of a constraint30
Maximum length of a constraint780

Trace number 2618

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        893108 kB
Buffers:         35220 kB
Cached:          78928 kB
SwapCached:        908 kB
Active:          79656 kB
Inactive:        37208 kB
HighTotal:      131008 kB
HighFree:        55888 kB
LowTotal:       903652 kB
LowFree:        837220 kB
SwapTotal:     2097892 kB
SwapFree:      2096472 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5804 kB
Slab:            19084 kB
Committed_AS:    64368 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 20:31:05 (client local time) WITH STATUS 0 IN 1209.86 SECONDS
stats: 2755 7 1209.86 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 122] 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/31754/stat): 31754 (minisat+_script) R 31753 31754 20602 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1721301208 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/31754/statm): 174 3 169 147 0 27 0
[pid=31754] 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=31755
New process pid=31756
New process pid=31757
One traced child (pid=31756) exited with status: 0
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=31757) exited with status: 0
One traced child (pid=31755) exited with status: 0
New process pid=31758
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-blend.opb
One traced child (pid=31758) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=31759
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-blend.opb

[startup+10.0028 s]
Raw data (loadavg): 0.92 0.95 0.90 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1567 0 0 0 973 5 0 0 25 0 1 0 1721301221 5287936 1180 4294967295 134512640 135167914 3221224448 3221219312 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31759/statm): 1291 1180 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 9.85
Current children cumulated vsize (Kb) 7292

[startup+20.0034 s]
Raw data (loadavg): 0.93 0.96 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1567 0 0 0 1972 5 0 0 25 0 1 0 1721301221 5287936 1180 4294967295 134512640 135167914 3221224448 3221219344 134849061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 1291 1180 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 19.84
Current children cumulated vsize (Kb) 7292

[startup+30.0041 s]
Raw data (loadavg): 0.94 0.96 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1567 0 0 0 2972 5 0 0 25 0 1 0 1721301221 5287936 1180 4294967295 134512640 135167914 3221224448 3221219856 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 1291 1180 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 29.84
Current children cumulated vsize (Kb) 7292

[startup+40.0038 s]
Raw data (loadavg): 0.95 0.96 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1567 0 0 0 3972 5 0 0 25 0 1 0 1721301221 5287936 1180 4294967295 134512640 135167914 3221224448 3221219872 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 1291 1180 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 39.84
Current children cumulated vsize (Kb) 7292

[startup+50.0045 s]
Raw data (loadavg): 0.96 0.96 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1567 0 0 0 4972 5 0 0 25 0 1 0 1721301221 5287936 1180 4294967295 134512640 135167914 3221224448 3221219920 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 1291 1180 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 49.84
Current children cumulated vsize (Kb) 7292

[startup+60.0041 s]
Raw data (loadavg): 0.96 0.96 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1567 0 0 0 5973 5 0 0 25 0 1 0 1721301221 5287936 1180 4294967295 134512640 135167914 3221224448 3221219616 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 1291 1180 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 59.85
Current children cumulated vsize (Kb) 7292

[startup+70.0048 s]
Raw data (loadavg): 0.97 0.96 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1567 0 0 0 6973 5 0 0 25 0 1 0 1721301221 5287936 1180 4294967295 134512640 135167914 3221224448 3221220412 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 1291 1180 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 69.85
Current children cumulated vsize (Kb) 7292

[startup+80.0055 s]
Raw data (loadavg): 0.97 0.96 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1567 0 0 0 7973 5 0 0 25 0 1 0 1721301221 5287936 1180 4294967295 134512640 135167914 3221224448 3221220736 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 1291 1180 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 79.85
Current children cumulated vsize (Kb) 7292

[startup+90.0052 s]
Raw data (loadavg): 0.98 0.96 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1567 0 0 0 8973 5 0 0 25 0 1 0 1721301221 5287936 1180 4294967295 134512640 135167914 3221224448 3221220756 134696180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 1291 1180 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 89.85
Current children cumulated vsize (Kb) 7292

[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1567 0 0 0 9973 5 0 0 25 0 1 0 1721301221 5287936 1180 4294967295 134512640 135167914 3221224448 3221219340 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 1291 1180 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 99.85
Current children cumulated vsize (Kb) 7292

[startup+110.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1567 0 0 0 10974 5 0 0 25 0 1 0 1721301221 5287936 1180 4294967295 134512640 135167914 3221224448 3221219004 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 1291 1180 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 109.86
Current children cumulated vsize (Kb) 7292

[startup+120.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1567 0 0 0 11974 5 0 0 25 0 1 0 1721301221 5287936 1180 4294967295 134512640 135167914 3221224448 3221218120 134693761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 1291 1180 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 119.86
Current children cumulated vsize (Kb) 7292

[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1567 0 0 0 12974 5 0 0 25 0 1 0 1721301221 5287936 1180 4294967295 134512640 135167914 3221224448 3221219712 134630940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 1291 1180 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 129.86
Current children cumulated vsize (Kb) 7292

[startup+140.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1567 0 0 0 13974 5 0 0 25 0 1 0 1721301221 5287936 1180 4294967295 134512640 135167914 3221224448 3221220068 134629227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 1291 1180 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 139.86
Current children cumulated vsize (Kb) 7292

[startup+150.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1567 0 0 0 14975 5 0 0 25 0 1 0 1721301221 5287936 1180 4294967295 134512640 135167914 3221224448 3221218480 134630830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 1291 1180 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 149.87
Current children cumulated vsize (Kb) 7292

[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1612 0 0 0 15975 5 0 0 25 0 1 0 1721301221 5287936 1183 4294967295 134512640 135167914 3221224448 3221220960 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 1291 1183 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 159.87
Current children cumulated vsize (Kb) 7292

[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1612 0 0 0 16975 5 0 0 25 0 1 0 1721301221 5287936 1183 4294967295 134512640 135167914 3221224448 3221220876 134722660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 1291 1183 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 169.87
Current children cumulated vsize (Kb) 7292

[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1612 0 0 0 17975 5 0 0 25 0 1 0 1721301221 5287936 1183 4294967295 134512640 135167914 3221224448 3221221296 134630853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 1291 1183 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 179.87
Current children cumulated vsize (Kb) 7292

[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 1612 0 0 0 18975 5 0 0 25 0 1 0 1721301221 5287936 1183 4294967295 134512640 135167914 3221224448 3221221648 134630853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 1291 1183 162 162 0 1129 0
[pid=31759] vsize: 5164
Current children cumulated CPU time (s) 189.87
Current children cumulated vsize (Kb) 7292

[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5059 0 0 0 19949 17 0 0 25 0 1 0 1721301221 14438400 3393 4294967295 134512640 135167914 3221224448 3221219696 134849163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31759/statm): 3525 3393 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 199.73
Current children cumulated vsize (Kb) 16228

[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5059 0 0 0 20949 17 0 0 25 0 1 0 1721301221 14438400 3393 4294967295 134512640 135167914 3221224448 3221220608 134629328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3393 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 209.73
Current children cumulated vsize (Kb) 16228

[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5059 0 0 0 21949 17 0 0 25 0 1 0 1721301221 14438400 3393 4294967295 134512640 135167914 3221224448 3221220560 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3393 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 219.73
Current children cumulated vsize (Kb) 16228

[startup+230.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5059 0 0 0 22949 17 0 0 25 0 1 0 1721301221 14438400 3393 4294967295 134512640 135167914 3221224448 3221221088 134843113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3393 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 229.73
Current children cumulated vsize (Kb) 16228

[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5059 0 0 0 23949 17 0 0 25 0 1 0 1721301221 14438400 3393 4294967295 134512640 135167914 3221224448 3221221664 134629451 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3393 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 239.73
Current children cumulated vsize (Kb) 16228

[startup+250.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5059 0 0 0 24950 17 0 0 25 0 1 0 1721301221 14438400 3393 4294967295 134512640 135167914 3221224448 3221221616 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3393 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 249.74
Current children cumulated vsize (Kb) 16228

[startup+260.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5059 0 0 0 25950 17 0 0 25 0 1 0 1721301221 14438400 3393 4294967295 134512640 135167914 3221224448 3221221648 134629080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3393 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 259.74
Current children cumulated vsize (Kb) 16228

[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5059 0 0 0 26950 17 0 0 25 0 1 0 1721301221 14438400 3393 4294967295 134512640 135167914 3221224448 3221221312 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3393 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 269.74
Current children cumulated vsize (Kb) 16228

[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5059 0 0 0 27950 17 0 0 25 0 1 0 1721301221 14438400 3393 4294967295 134512640 135167914 3221224448 3221221188 134718180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3393 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 279.74
Current children cumulated vsize (Kb) 16228

[startup+290.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5095 0 0 0 28950 17 0 0 25 0 1 0 1721301221 14438400 3429 4294967295 134512640 135167914 3221224448 3221217548 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3429 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 289.74
Current children cumulated vsize (Kb) 16228

[startup+300.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5095 0 0 0 29951 17 0 0 25 0 1 0 1721301221 14438400 3429 4294967295 134512640 135167914 3221224448 3221219104 134849061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3429 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 299.75
Current children cumulated vsize (Kb) 16228

[startup+310.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5095 0 0 0 30951 17 0 0 25 0 1 0 1721301221 14438400 3429 4294967295 134512640 135167914 3221224448 3221220560 134843074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3429 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 309.75
Current children cumulated vsize (Kb) 16228

[startup+320.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5095 0 0 0 31951 17 0 0 25 0 1 0 1721301221 14438400 3429 4294967295 134512640 135167914 3221224448 3221220208 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3429 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 319.75
Current children cumulated vsize (Kb) 16228

[startup+330.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5095 0 0 0 32951 17 0 0 25 0 1 0 1721301221 14438400 3429 4294967295 134512640 135167914 3221224448 3221220208 134843113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3429 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 329.75
Current children cumulated vsize (Kb) 16228

[startup+340.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5095 0 0 0 33951 17 0 0 25 0 1 0 1721301221 14438400 3429 4294967295 134512640 135167914 3221224448 3221217736 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3429 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 339.75
Current children cumulated vsize (Kb) 16228

[startup+350.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5095 0 0 0 34952 17 0 0 25 0 1 0 1721301221 14438400 3429 4294967295 134512640 135167914 3221224448 3221219504 134843064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3429 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 349.76
Current children cumulated vsize (Kb) 16228

[startup+360.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5095 0 0 0 35952 17 0 0 25 0 1 0 1721301221 14438400 3429 4294967295 134512640 135167914 3221224448 3221220032 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3429 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 359.76
Current children cumulated vsize (Kb) 16228

[startup+370.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5095 0 0 0 36952 17 0 0 25 0 1 0 1721301221 14438400 3429 4294967295 134512640 135167914 3221224448 3221221680 134844715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3429 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 369.76
Current children cumulated vsize (Kb) 16228

[startup+380.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5095 0 0 0 37953 17 0 0 25 0 1 0 1721301221 14438400 3429 4294967295 134512640 135167914 3221224448 3221220016 134522331 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3429 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 379.77
Current children cumulated vsize (Kb) 16228

[startup+390.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5095 0 0 0 38953 17 0 0 25 0 1 0 1721301221 14438400 3429 4294967295 134512640 135167914 3221224448 3221221436 134722542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3429 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 389.77
Current children cumulated vsize (Kb) 16228

[startup+400.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5095 0 0 0 39953 17 0 0 25 0 1 0 1721301221 14438400 3429 4294967295 134512640 135167914 3221224448 3221220412 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3429 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 399.77
Current children cumulated vsize (Kb) 16228

[startup+410.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5095 0 0 0 40953 17 0 0 25 0 1 0 1721301221 14438400 3429 4294967295 134512640 135167914 3221224448 3221221968 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3525 3429 162 162 0 3363 0
[pid=31759] vsize: 14100
Current children cumulated CPU time (s) 409.77
Current children cumulated vsize (Kb) 16228

[startup+420.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5124 0 0 0 41953 18 0 0 25 0 1 0 1721301221 14491648 3375 4294967295 134512640 135167914 3221224448 3221220736 134849071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3538 3375 162 162 0 3376 0
[pid=31759] vsize: 14152
Current children cumulated CPU time (s) 419.78
Current children cumulated vsize (Kb) 16280

[startup+430.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5784 0 0 0 42952 19 0 0 25 0 1 0 1721301221 15843328 3705 4294967295 134512640 135167914 3221224448 3221211504 134624954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3868 3705 162 162 0 3706 0
[pid=31759] vsize: 15472
Current children cumulated CPU time (s) 429.78
Current children cumulated vsize (Kb) 17600

[startup+440.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5784 0 0 0 43952 19 0 0 25 0 1 0 1721301221 14491648 3375 4294967295 134512640 135167914 3221224448 3221220672 134696759 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3538 3375 162 162 0 3376 0
[pid=31759] vsize: 14152
Current children cumulated CPU time (s) 439.78
Current children cumulated vsize (Kb) 16280

[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5784 0 0 0 44952 19 0 0 25 0 1 0 1721301221 14491648 3375 4294967295 134512640 135167914 3221224448 3221221552 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3538 3375 162 162 0 3376 0
[pid=31759] vsize: 14152
Current children cumulated CPU time (s) 449.78
Current children cumulated vsize (Kb) 16280

[startup+460.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5784 0 0 0 45952 19 0 0 25 0 1 0 1721301221 14491648 3375 4294967295 134512640 135167914 3221224448 3221221292 134694480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3538 3375 162 162 0 3376 0
[pid=31759] vsize: 14152
Current children cumulated CPU time (s) 459.78
Current children cumulated vsize (Kb) 16280

[startup+470.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 5784 0 0 0 46952 19 0 0 25 0 1 0 1721301221 14491648 3375 4294967295 134512640 135167914 3221224448 3221221744 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 3538 3375 162 162 0 3376 0
[pid=31759] vsize: 14152
Current children cumulated CPU time (s) 469.78
Current children cumulated vsize (Kb) 16280

[startup+480.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7549 0 0 0 47941 26 0 0 25 0 1 0 1721301221 20361216 4810 4294967295 134512640 135167914 3221224448 3221209664 134849473 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4971 4810 162 162 0 4809 0
[pid=31759] vsize: 19884
Current children cumulated CPU time (s) 479.74
Current children cumulated vsize (Kb) 22012

[startup+490.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7581 0 0 0 48941 26 0 0 25 0 1 0 1721301221 17793024 4183 4294967295 134512640 135167914 3221224448 3221220784 134844720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4183 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 489.74
Current children cumulated vsize (Kb) 19504

[startup+500.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7581 0 0 0 49941 26 0 0 25 0 1 0 1721301221 17793024 4183 4294967295 134512640 135167914 3221224448 3221220560 134849108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4183 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 499.74
Current children cumulated vsize (Kb) 19504

[startup+510.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7581 0 0 0 50942 26 0 0 25 0 1 0 1721301221 17793024 4183 4294967295 134512640 135167914 3221224448 3221221456 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4183 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 509.75
Current children cumulated vsize (Kb) 19504

[startup+520.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7581 0 0 0 51942 26 0 0 25 0 1 0 1721301221 17793024 4183 4294967295 134512640 135167914 3221224448 3221220576 134693570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4183 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 519.75
Current children cumulated vsize (Kb) 19504

[startup+530.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7581 0 0 0 52942 26 0 0 25 0 1 0 1721301221 17793024 4183 4294967295 134512640 135167914 3221224448 3221221264 134849179 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4183 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 529.75
Current children cumulated vsize (Kb) 19504

[startup+540.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7581 0 0 0 53942 26 0 0 25 0 1 0 1721301221 17793024 4183 4294967295 134512640 135167914 3221224448 3221221740 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4183 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 539.75
Current children cumulated vsize (Kb) 19504

[startup+550.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7581 0 0 0 54943 26 0 0 25 0 1 0 1721301221 17793024 4183 4294967295 134512640 135167914 3221224448 3221220596 134629364 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4183 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 549.76
Current children cumulated vsize (Kb) 19504

[startup+560.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7590 0 0 0 55943 26 0 0 25 0 1 0 1721301221 17793024 4192 4294967295 134512640 135167914 3221224448 3221221252 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4192 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 559.76
Current children cumulated vsize (Kb) 19504

[startup+570.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7618 0 0 0 56943 26 0 0 25 0 1 0 1721301221 17793024 4220 4294967295 134512640 135167914 3221224448 3221213628 134694368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4220 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 569.76
Current children cumulated vsize (Kb) 19504

[startup+580.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7618 0 0 0 57943 26 0 0 25 0 1 0 1721301221 17793024 4220 4294967295 134512640 135167914 3221224448 3221221312 134845890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4220 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 579.76
Current children cumulated vsize (Kb) 19504

[startup+590.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7618 0 0 0 58944 26 0 0 25 0 1 0 1721301221 17793024 4220 4294967295 134512640 135167914 3221224448 3221203888 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4220 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 589.77
Current children cumulated vsize (Kb) 19504

[startup+600.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7948 0 0 0 59943 27 0 0 25 0 1 0 1721301221 17793024 4220 4294967295 134512640 135167914 3221224448 3221219956 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4220 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 599.77
Current children cumulated vsize (Kb) 19504

[startup+610.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7948 0 0 0 60943 27 0 0 25 0 1 0 1721301221 17793024 4220 4294967295 134512640 135167914 3221224448 3221221568 134723229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4220 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 609.77
Current children cumulated vsize (Kb) 19504

[startup+620.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7948 0 0 0 61943 27 0 0 25 0 1 0 1721301221 17793024 4220 4294967295 134512640 135167914 3221224448 3221220320 134696316 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4220 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 619.77
Current children cumulated vsize (Kb) 19504

[startup+630.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7948 0 0 0 62944 27 0 0 25 0 1 0 1721301221 17793024 4220 4294967295 134512640 135167914 3221224448 3221221968 134843026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4220 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 629.78
Current children cumulated vsize (Kb) 19504

[startup+640.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7948 0 0 0 63944 27 0 0 25 0 1 0 1721301221 17793024 4220 4294967295 134512640 135167914 3221224448 3221220864 134723229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4220 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 639.78
Current children cumulated vsize (Kb) 19504

[startup+650.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7948 0 0 0 64944 27 0 0 25 0 1 0 1721301221 17793024 4220 4294967295 134512640 135167914 3221224448 3221221024 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4220 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 649.78
Current children cumulated vsize (Kb) 19504

[startup+660.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7948 0 0 0 65944 27 0 0 25 0 1 0 1721301221 17793024 4220 4294967295 134512640 135167914 3221224448 3221221772 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4220 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 659.78
Current children cumulated vsize (Kb) 19504

[startup+670.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7948 0 0 0 66944 27 0 0 25 0 1 0 1721301221 17793024 4220 4294967295 134512640 135167914 3221224448 3221222144 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4220 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 669.78
Current children cumulated vsize (Kb) 19504

[startup+680.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7948 0 0 0 67945 27 0 0 25 0 1 0 1721301221 17793024 4220 4294967295 134512640 135167914 3221224448 3221221664 134629161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4220 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 679.79
Current children cumulated vsize (Kb) 19504

[startup+690.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7948 0 0 0 68945 27 0 0 25 0 1 0 1721301221 17793024 4220 4294967295 134512640 135167914 3221224448 3221221968 134694407 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4220 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 689.79
Current children cumulated vsize (Kb) 19504

[startup+700.035 s]
Raw data (loadavg): 0.99 0.97 0.91 3/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 7948 0 0 0 69945 27 0 0 25 0 1 0 1721301221 17793024 4220 4294967295 134512640 135167914 3221224448 3221220960 134629448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4220 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 699.79
Current children cumulated vsize (Kb) 19504

[startup+710.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8284 0 0 0 70944 28 0 0 25 0 1 0 1721301221 17793024 4226 4294967295 134512640 135167914 3221224448 3221220560 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4226 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 709.79
Current children cumulated vsize (Kb) 19504

[startup+720.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8284 0 0 0 71944 28 0 0 25 0 1 0 1721301221 17793024 4226 4294967295 134512640 135167914 3221224448 3221220828 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4226 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 719.79
Current children cumulated vsize (Kb) 19504

[startup+730.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8284 0 0 0 72945 28 0 0 25 0 1 0 1721301221 17793024 4226 4294967295 134512640 135167914 3221224448 3221220560 134694504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4226 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 729.8
Current children cumulated vsize (Kb) 19504

[startup+740.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8284 0 0 0 73945 28 0 0 25 0 1 0 1721301221 17793024 4226 4294967295 134512640 135167914 3221224448 3221220944 134629224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4226 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 739.8
Current children cumulated vsize (Kb) 19504

[startup+750.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8284 0 0 0 74945 28 0 0 25 0 1 0 1721301221 17793024 4226 4294967295 134512640 135167914 3221224448 3221221200 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4226 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 749.8
Current children cumulated vsize (Kb) 19504

[startup+760.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8284 0 0 0 75945 28 0 0 25 0 1 0 1721301221 17793024 4226 4294967295 134512640 135167914 3221224448 3221222464 134844637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4226 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 759.8
Current children cumulated vsize (Kb) 19504

[startup+770.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8284 0 0 0 76946 28 0 0 25 0 1 0 1721301221 17793024 4226 4294967295 134512640 135167914 3221224448 3221221816 134849087 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4226 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 769.81
Current children cumulated vsize (Kb) 19504

[startup+780.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 77946 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221219088 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 779.81
Current children cumulated vsize (Kb) 19504

[startup+790.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 78946 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221220056 134693801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 789.81
Current children cumulated vsize (Kb) 19504

[startup+800.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 79946 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221220880 134718188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 799.81
Current children cumulated vsize (Kb) 19504

[startup+810.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 80946 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221220496 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 809.81
Current children cumulated vsize (Kb) 19504

[startup+820.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 81947 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221220960 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 819.82
Current children cumulated vsize (Kb) 19504

[startup+830.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 82947 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221221120 134629345 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 829.82
Current children cumulated vsize (Kb) 19504

[startup+840.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 83947 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221220560 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 839.82
Current children cumulated vsize (Kb) 19504

[startup+850.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 84947 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221220560 134694396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 849.82
Current children cumulated vsize (Kb) 19504

[startup+860.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 85948 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221221648 134629248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 859.83
Current children cumulated vsize (Kb) 19504

[startup+870.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 86948 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221220752 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 869.83
Current children cumulated vsize (Kb) 19504

[startup+880.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 87948 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221221404 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 879.83
Current children cumulated vsize (Kb) 19504

[startup+890.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 88948 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221221180 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 889.83
Current children cumulated vsize (Kb) 19504

[startup+900.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 89949 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221221184 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 899.84
Current children cumulated vsize (Kb) 19504

[startup+910.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 90949 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221220412 134693585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 909.84
Current children cumulated vsize (Kb) 19504

[startup+920.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 91949 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221221008 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 919.84
Current children cumulated vsize (Kb) 19504

[startup+930.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 92949 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221221792 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 929.84
Current children cumulated vsize (Kb) 19504

[startup+940.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 93950 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221220572 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 939.85
Current children cumulated vsize (Kb) 19504

[startup+950.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 94950 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221221228 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 949.85
Current children cumulated vsize (Kb) 19504

[startup+960.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 95950 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221221280 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 959.85
Current children cumulated vsize (Kb) 19504

[startup+970.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 96950 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221221104 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 969.85
Current children cumulated vsize (Kb) 19504

[startup+980.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 97951 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221222172 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 979.86
Current children cumulated vsize (Kb) 19504

[startup+990.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 98951 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221221360 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 989.86
Current children cumulated vsize (Kb) 19504

[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8288 0 0 0 99951 28 0 0 25 0 1 0 1721301221 17793024 4230 4294967295 134512640 135167914 3221224448 3221221184 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4344 4230 162 162 0 4182 0
[pid=31759] vsize: 17376
Current children cumulated CPU time (s) 999.86
Current children cumulated vsize (Kb) 19504

[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8325 0 0 0 100951 28 0 0 25 0 1 0 1721301221 18579456 4267 4294967295 134512640 135167914 3221224448 3221221280 134694351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4536 4267 162 162 0 4374 0
[pid=31759] vsize: 18144
Current children cumulated CPU time (s) 1009.86
Current children cumulated vsize (Kb) 20272

[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8326 0 0 0 101951 28 0 0 25 0 1 0 1721301221 18583552 4268 4294967295 134512640 135167914 3221224448 3221218912 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4537 4268 162 162 0 4375 0
[pid=31759] vsize: 18148
Current children cumulated CPU time (s) 1019.86
Current children cumulated vsize (Kb) 20276

[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8326 0 0 0 102952 28 0 0 25 0 1 0 1721301221 18583552 4268 4294967295 134512640 135167914 3221224448 3221220052 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4537 4268 162 162 0 4375 0
[pid=31759] vsize: 18148
Current children cumulated CPU time (s) 1029.87
Current children cumulated vsize (Kb) 20276

[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8326 0 0 0 103952 28 0 0 25 0 1 0 1721301221 18583552 4268 4294967295 134512640 135167914 3221224448 3221220912 134522296 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4537 4268 162 162 0 4375 0
[pid=31759] vsize: 18148
Current children cumulated CPU time (s) 1039.87
Current children cumulated vsize (Kb) 20276

[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8326 0 0 0 104952 28 0 0 25 0 1 0 1721301221 18583552 4268 4294967295 134512640 135167914 3221224448 3221220912 134849143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4537 4268 162 162 0 4375 0
[pid=31759] vsize: 18148
Current children cumulated CPU time (s) 1049.87
Current children cumulated vsize (Kb) 20276

[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8326 0 0 0 105952 28 0 0 25 0 1 0 1721301221 18583552 4268 4294967295 134512640 135167914 3221224448 3221221488 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4537 4268 162 162 0 4375 0
[pid=31759] vsize: 18148
Current children cumulated CPU time (s) 1059.87
Current children cumulated vsize (Kb) 20276

[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8326 0 0 0 106953 28 0 0 25 0 1 0 1721301221 18583552 4268 4294967295 134512640 135167914 3221224448 3221221712 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4537 4268 162 162 0 4375 0
[pid=31759] vsize: 18148
Current children cumulated CPU time (s) 1069.88
Current children cumulated vsize (Kb) 20276

[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 8326 0 0 0 107953 28 0 0 25 0 1 0 1721301221 18583552 4268 4294967295 134512640 135167914 3221224448 3221220672 134843113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4537 4268 162 162 0 4375 0
[pid=31759] vsize: 18148
Current children cumulated CPU time (s) 1079.88
Current children cumulated vsize (Kb) 20276

[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 9048 0 0 0 108951 30 0 0 25 0 1 0 1721301221 19972096 4660 4294967295 134512640 135167914 3221224448 3221216636 134723236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4876 4660 162 162 0 4714 0
[pid=31759] vsize: 19504
Current children cumulated CPU time (s) 1089.88
Current children cumulated vsize (Kb) 21632

[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 9048 0 0 0 109951 30 0 0 25 0 1 0 1721301221 19972096 4660 4294967295 134512640 135167914 3221224448 3221217868 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4876 4660 162 162 0 4714 0
[pid=31759] vsize: 19504
Current children cumulated CPU time (s) 1099.88
Current children cumulated vsize (Kb) 21632

[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 9048 0 0 0 110952 30 0 0 25 0 1 0 1721301221 19972096 4660 4294967295 134512640 135167914 3221224448 3221217556 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4876 4660 162 162 0 4714 0
[pid=31759] vsize: 19504
Current children cumulated CPU time (s) 1109.89
Current children cumulated vsize (Kb) 21632

[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 9048 0 0 0 111952 30 0 0 25 0 1 0 1721301221 19972096 4660 4294967295 134512640 135167914 3221224448 3221218640 134694351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4876 4660 162 162 0 4714 0
[pid=31759] vsize: 19504
Current children cumulated CPU time (s) 1119.89
Current children cumulated vsize (Kb) 21632

[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 9048 0 0 0 112952 30 0 0 25 0 1 0 1721301221 19972096 4660 4294967295 134512640 135167914 3221224448 3221218208 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4876 4660 162 162 0 4714 0
[pid=31759] vsize: 19504
Current children cumulated CPU time (s) 1129.89
Current children cumulated vsize (Kb) 21632

[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 9048 0 0 0 113952 30 0 0 25 0 1 0 1721301221 19972096 4660 4294967295 134512640 135167914 3221224448 3221218272 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4876 4660 162 162 0 4714 0
[pid=31759] vsize: 19504
Current children cumulated CPU time (s) 1139.89
Current children cumulated vsize (Kb) 21632

[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 9048 0 0 0 114953 30 0 0 25 0 1 0 1721301221 19972096 4660 4294967295 134512640 135167914 3221224448 3221217708 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4876 4660 162 162 0 4714 0
[pid=31759] vsize: 19504
Current children cumulated CPU time (s) 1149.9
Current children cumulated vsize (Kb) 21632

[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 9048 0 0 0 115953 30 0 0 25 0 1 0 1721301221 19972096 4660 4294967295 134512640 135167914 3221224448 3221218428 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4876 4660 162 162 0 4714 0
[pid=31759] vsize: 19504
Current children cumulated CPU time (s) 1159.9
Current children cumulated vsize (Kb) 21632

[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 9048 0 0 0 116953 30 0 0 25 0 1 0 1721301221 19972096 4660 4294967295 134512640 135167914 3221224448 3221217856 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4876 4660 162 162 0 4714 0
[pid=31759] vsize: 19504
Current children cumulated CPU time (s) 1169.9
Current children cumulated vsize (Kb) 21632

[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 9048 0 0 0 117953 30 0 0 25 0 1 0 1721301221 19972096 4660 4294967295 134512640 135167914 3221224448 3221218060 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4876 4660 162 162 0 4714 0
[pid=31759] vsize: 19504
Current children cumulated CPU time (s) 1179.9
Current children cumulated vsize (Kb) 21632

[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 9048 0 0 0 118953 30 0 0 25 0 1 0 1721301221 19972096 4660 4294967295 134512640 135167914 3221224448 3221217772 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4876 4660 162 162 0 4714 0
[pid=31759] vsize: 19504
Current children cumulated CPU time (s) 1189.9
Current children cumulated vsize (Kb) 21632

[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 9048 0 0 0 119954 30 0 0 25 0 1 0 1721301221 19972096 4660 4294967295 134512640 135167914 3221224448 3221218032 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4876 4660 162 162 0 4714 0
[pid=31759] vsize: 19504
Current children cumulated CPU time (s) 1199.91
Current children cumulated vsize (Kb) 21632

[startup+1210.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 9048 0 0 0 120954 30 0 0 25 0 1 0 1721301221 19972096 4660 4294967295 134512640 135167914 3221224448 3221219468 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4876 4660 162 162 0 4714 0
[pid=31759] vsize: 19504
Current children cumulated CPU time (s) 1209.91
Current children cumulated vsize (Kb) 21632



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31759
Raw data (/proc/31754/stat): 31754 (minisat+_script) S 31753 31754 20602 0 -1 0 314 516 0 0 0 0 5 2 18 0 1 0 1721301208 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31754/statm): 532 234 485 147 0 385 0
[pid=31754] vsize: 2128
Raw data (/proc/31759/stat): 31759 (minisat+_bignum) R 31754 31754 20602 0 -1 0 9048 0 0 0 120954 30 0 0 25 0 1 0 1721301221 19972096 4660 4294967295 134512640 135167914 3221224448 3221219616 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31759/statm): 4876 4660 162 162 0 4714 0
[pid=31759] vsize: 19504
Current children cumulated CPU time (s) 1209.91
Current children cumulated vsize (Kb) 21632

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

Child status: 0
Real time (s): 1210.07
CPU time (s): 1209.86
CPU user time (s): 1209.55
CPU system time (s): 0.310952
CPU usage (%): 99.982
Max. virtual memory (cumulated for all children) (Kb): 22012

Verifier Data

ERROR: no interpretation found !