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-maros-r7.opb
MD5SUMebb49febffdfe5475bc23e4ef8d466db
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 188160
Biggest coefficient in the objective function 536870912
Number of bits for the biggest coefficient in the objective function 30
Sum of the numbers in the objective function 6734508713856
Number of bits of the sum of numbers in the objective function 43
Biggest number in a constraint 536870912000000
Number of bits of the biggest number in a constraint 49
Biggest sum of numbers in a constraint 4602477289606474
Number of bits of the biggest sum of numbers53
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables282240
Total number of constraints3136
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 constraints3136
Minimum length of a constraint150
Maximum length of a constraint720

Trace number 2664

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        812892 kB
Buffers:         38148 kB
Cached:         153316 kB
SwapCached:        908 kB
Active:         152852 kB
Inactive:        41440 kB
HighTotal:      131008 kB
HighFree:         3808 kB
LowTotal:       903652 kB
LowFree:        809084 kB
SwapTotal:     2097136 kB
SwapFree:      2095620 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5992 kB
Slab:            21680 kB
Committed_AS:    93132 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 20:50:09 (client local time) WITH STATUS 0 IN 1202.45 SECONDS
stats: 2787 7 1202.45 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 9413] 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/29218/stat): 29218 (minisat+_script) R 29217 29218 17733 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1729062449 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/29218/statm): 174 3 169 147 0 27 0
[pid=29218] 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=29219
New process pid=29220
New process pid=29221
execve syscall for /bin/sed executable
One traced child (pid=29220) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=29221) exited with status: 0
One traced child (pid=29219) exited with status: 0
New process pid=29222
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-maros-r7.opb
One traced child (pid=29222) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=29223
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-maros-r7.opb

[startup+10.0036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 9989 0 3 0 683 41 0 0 25 0 1 0 1729062680 42586112 8990 4294967295 134512640 135167914 3221224448 3221222448 134695274 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29223/statm): 10397 8990 162 162 0 10235 0
[pid=29223] vsize: 41588
Current children cumulated CPU time (s) 8.61
Current children cumulated vsize (Kb) 43716

[startup+20.0043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 11458 0 3 0 1666 50 0 0 25 0 1 0 1729062680 48050176 10459 4294967295 134512640 135167914 3221224448 3221222896 134590724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29223/statm): 11731 10459 162 162 0 11569 0
[pid=29223] vsize: 46924
Current children cumulated CPU time (s) 18.53
Current children cumulated vsize (Kb) 49052

[startup+30.0051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 13938 0 3 0 2633 65 0 0 25 0 1 0 1729062680 57880576 12939 4294967295 134512640 135167914 3221224448 3221223292 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29223/statm): 14131 12939 162 162 0 13969 0
[pid=29223] vsize: 56524
Current children cumulated CPU time (s) 28.35
Current children cumulated vsize (Kb) 58652

[startup+40.0059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 16406 0 3 0 3600 81 0 0 25 0 1 0 1729062680 67710976 15407 4294967295 134512640 135167914 3221224448 3221222840 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 16531 15407 162 162 0 16369 0
[pid=29223] vsize: 66124
Current children cumulated CPU time (s) 38.18
Current children cumulated vsize (Kb) 68252

[startup+50.0067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 18880 0 3 0 4573 92 0 0 25 0 1 0 1729062680 77549568 17881 4294967295 134512640 135167914 3221224448 3221221280 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 18933 17881 162 162 0 18771 0
[pid=29223] vsize: 75732
Current children cumulated CPU time (s) 48.02
Current children cumulated vsize (Kb) 77860

[startup+60.0075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 21337 0 3 0 5537 109 0 0 25 0 1 0 1729062680 87334912 20338 4294967295 134512640 135167914 3221224448 3221220640 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 21322 20338 162 162 0 21160 0
[pid=29223] vsize: 85288
Current children cumulated CPU time (s) 57.83
Current children cumulated vsize (Kb) 87416

[startup+70.0083 s]
Raw data (loadavg): 0.99 0.97 0.91 1/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) T 29218 29218 17733 0 -1 0 23783 0 3 0 6504 125 0 0 25 0 1 0 1729062680 97099776 22784 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/29223/statm): 23706 22784 162 162 0 23544 0
[pid=29223] vsize: 94824
Current children cumulated CPU time (s) 67.66
Current children cumulated vsize (Kb) 96952

[startup+80.009 s]
Raw data (loadavg): 0.99 0.97 0.91 1/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) T 29218 29218 17733 0 -1 0 26226 0 3 0 7471 142 0 0 25 0 1 0 1729062680 106897408 25227 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/29223/statm): 26098 25227 162 162 0 25936 0
[pid=29223] vsize: 104392
Current children cumulated CPU time (s) 77.5
Current children cumulated vsize (Kb) 106520

[startup+90.0098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 28658 0 3 0 8437 159 0 0 25 0 1 0 1729062680 116645888 27659 4294967295 134512640 135167914 3221224448 3221221600 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 28478 27659 162 162 0 28316 0
[pid=29223] vsize: 113912
Current children cumulated CPU time (s) 87.33
Current children cumulated vsize (Kb) 116040

[startup+100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 31089 0 3 0 9405 173 0 0 25 0 1 0 1729062680 126394368 30090 4294967295 134512640 135167914 3221224448 3221222700 134694368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 30858 30090 162 162 0 30696 0
[pid=29223] vsize: 123432
Current children cumulated CPU time (s) 97.15
Current children cumulated vsize (Kb) 125560

[startup+110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 33500 0 3 0 10375 187 0 0 25 0 1 0 1729062680 136060928 32501 4294967295 134512640 135167914 3221224448 3221220716 134845940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 33218 32501 162 162 0 33056 0
[pid=29223] vsize: 132872
Current children cumulated CPU time (s) 106.99
Current children cumulated vsize (Kb) 135000

[startup+120.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 35941 0 3 0 11344 201 0 0 25 0 1 0 1729062680 145809408 34942 4294967295 134512640 135167914 3221224448 3221222864 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 35598 34942 162 162 0 35436 0
[pid=29223] vsize: 142392
Current children cumulated CPU time (s) 116.82
Current children cumulated vsize (Kb) 144520

[startup+130.012 s]
Raw data (loadavg): 0.99 0.97 0.91 1/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) T 29218 29218 17733 0 -1 0 38372 0 3 0 12313 215 0 0 25 0 1 0 1729062680 155574272 37373 4294967295 134512640 135167914 3221224448 3221222588 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/29223/statm): 37982 37373 162 162 0 37820 0
[pid=29223] vsize: 151928
Current children cumulated CPU time (s) 126.65
Current children cumulated vsize (Kb) 154056

[startup+140.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 40814 0 3 0 13284 227 0 0 25 0 1 0 1729062680 165359616 39815 4294967295 134512640 135167914 3221224448 3221221960 134581244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 40371 39815 162 162 0 40209 0
[pid=29223] vsize: 161484
Current children cumulated CPU time (s) 136.48
Current children cumulated vsize (Kb) 163612

[startup+150.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 43234 0 3 0 14252 242 0 0 25 0 1 0 1729062680 175063040 42235 4294967295 134512640 135167914 3221224448 3221221584 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29223/statm): 42740 42235 162 162 0 42578 0
[pid=29223] vsize: 170960
Current children cumulated CPU time (s) 146.31
Current children cumulated vsize (Kb) 173088

[startup+160.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 45678 0 3 0 15220 256 0 0 25 0 1 0 1729062680 184860672 44679 4294967295 134512640 135167914 3221224448 3221222896 134591595 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 45132 44679 162 162 0 44970 0
[pid=29223] vsize: 180528
Current children cumulated CPU time (s) 156.13
Current children cumulated vsize (Kb) 182656

[startup+170.015 s]
Raw data (loadavg): 0.99 0.97 0.91 1/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) T 29218 29218 17733 0 -1 0 48106 0 3 0 16189 270 0 0 25 0 1 0 1729062680 194609152 47107 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/29223/statm): 47512 47107 162 162 0 47350 0
[pid=29223] vsize: 190048
Current children cumulated CPU time (s) 165.96
Current children cumulated vsize (Kb) 192176

[startup+180.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) T 29218 29218 17733 0 -1 0 50529 0 3 0 17158 285 0 0 25 0 1 0 1729062680 204312576 49530 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/29223/statm): 49881 49530 162 162 0 49719 0
[pid=29223] vsize: 199524
Current children cumulated CPU time (s) 175.8
Current children cumulated vsize (Kb) 201652

[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 52972 0 3 0 18127 299 0 0 21 0 1 0 1729062680 232710144 51973 4294967295 134512640 135167914 3221224448 3221221304 134693626 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29223/statm): 56814 51973 162 162 0 56652 0
[pid=29223] vsize: 227256
Current children cumulated CPU time (s) 185.63
Current children cumulated vsize (Kb) 229384

[startup+200.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 55392 0 3 0 19094 314 0 0 25 0 1 0 1729062680 242409472 54393 4294967295 134512640 135167914 3221224448 3221222192 134843160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 59182 54393 162 162 0 59020 0
[pid=29223] vsize: 236728
Current children cumulated CPU time (s) 195.45
Current children cumulated vsize (Kb) 238856

[startup+210.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 57773 0 3 0 20062 329 0 0 25 0 1 0 1729062680 252051456 56774 4294967295 134512640 135167914 3221224448 3221222800 134516620 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 61536 56774 162 162 0 61374 0
[pid=29223] vsize: 246144
Current children cumulated CPU time (s) 205.28
Current children cumulated vsize (Kb) 248272

[startup+220.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 60152 0 3 0 21032 341 0 0 25 0 1 0 1729062680 261767168 59153 4294967295 134512640 135167914 3221224448 3221222720 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 63908 59153 162 162 0 63746 0
[pid=29223] vsize: 255632
Current children cumulated CPU time (s) 215.1
Current children cumulated vsize (Kb) 257760

[startup+230.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 62622 0 3 0 21999 356 0 0 25 0 1 0 1729062680 271745024 61623 4294967295 134512640 135167914 3221224448 3221222048 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 66344 61623 162 162 0 66182 0
[pid=29223] vsize: 265376
Current children cumulated CPU time (s) 224.92
Current children cumulated vsize (Kb) 267504

[startup+240.02 s]
Raw data (loadavg): 0.99 0.97 0.91 1/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) T 29218 29218 17733 0 -1 0 65063 0 3 0 22966 372 0 0 25 0 1 0 1729062680 281542656 64064 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/29223/statm): 68736 64064 162 162 0 68574 0
[pid=29223] vsize: 274944
Current children cumulated CPU time (s) 234.75
Current children cumulated vsize (Kb) 277072

[startup+250.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 67503 0 3 0 23933 386 0 0 25 0 1 0 1729062680 291332096 66504 4294967295 134512640 135167914 3221224448 3221222764 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 71126 66504 162 162 0 70964 0
[pid=29223] vsize: 284504
Current children cumulated CPU time (s) 244.56
Current children cumulated vsize (Kb) 286632

[startup+260.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 69953 0 3 0 24898 402 0 0 25 0 1 0 1729062680 301170688 68954 4294967295 134512640 135167914 3221224448 3221222080 134522331 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 73528 68954 162 162 0 73366 0
[pid=29223] vsize: 294112
Current children cumulated CPU time (s) 254.37
Current children cumulated vsize (Kb) 296240

[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 72373 0 3 0 25869 416 0 0 25 0 1 0 1729062680 310939648 71374 4294967295 134512640 135167914 3221224448 3221220588 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 75913 71374 162 162 0 75751 0
[pid=29223] vsize: 303652
Current children cumulated CPU time (s) 264.22
Current children cumulated vsize (Kb) 305780

[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 74743 0 3 0 26840 429 0 0 25 0 1 0 1729062680 320647168 73744 4294967295 134512640 135167914 3221224448 3221222800 134844731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29223/statm): 78283 73744 162 162 0 78121 0
[pid=29223] vsize: 313132
Current children cumulated CPU time (s) 274.06
Current children cumulated vsize (Kb) 315260

[startup+290.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 77101 0 3 0 27809 443 0 0 25 0 1 0 1729062680 330305536 76102 4294967295 134512640 135167914 3221224448 3221219760 134581189 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 80641 76102 162 162 0 80479 0
[pid=29223] vsize: 322564
Current children cumulated CPU time (s) 283.89
Current children cumulated vsize (Kb) 324692

[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 86359 0 3 0 28726 482 0 0 24 0 1 0 1729062680 368209920 85360 4294967295 134512640 135167914 3221224448 3221223376 134543320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29223/statm): 89895 85360 162 162 0 89733 0
[pid=29223] vsize: 359580
Current children cumulated CPU time (s) 293.45
Current children cumulated vsize (Kb) 361708

[startup+310.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 86394 0 3 0 29725 483 0 0 25 0 1 0 1729062680 361574400 83741 4294967295 134512640 135167914 3221224448 3221077440 134625368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29223/statm): 88275 83741 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 303.45
Current children cumulated vsize (Kb) 355228

[startup+320.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 30721 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221215552 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 313.45
Current children cumulated vsize (Kb) 355228

[startup+330.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 31721 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216032 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 323.45
Current children cumulated vsize (Kb) 355228

[startup+340.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 32722 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216080 134845903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 333.46
Current children cumulated vsize (Kb) 355228

[startup+350.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 33722 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216512 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 343.46
Current children cumulated vsize (Kb) 355228

[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 34722 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221215784 134844674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 353.46
Current children cumulated vsize (Kb) 355228

[startup+370.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 35722 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216332 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 363.46
Current children cumulated vsize (Kb) 355228

[startup+380.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 36723 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216828 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 373.47
Current children cumulated vsize (Kb) 355228

[startup+390.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 37723 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216708 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 383.47
Current children cumulated vsize (Kb) 355228

[startup+400.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 38723 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216512 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 393.47
Current children cumulated vsize (Kb) 355228

[startup+410.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 39723 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217024 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 403.47
Current children cumulated vsize (Kb) 355228

[startup+420.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 40723 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216636 134723267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 413.47
Current children cumulated vsize (Kb) 355228

[startup+430.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 41724 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216148 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 423.48
Current children cumulated vsize (Kb) 355228

[startup+440.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 42724 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217064 134693744 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 433.48
Current children cumulated vsize (Kb) 355228

[startup+450.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 43724 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217048 134722513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 443.48
Current children cumulated vsize (Kb) 355228

[startup+460.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 44724 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216400 134844720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 453.48
Current children cumulated vsize (Kb) 355228

[startup+470.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 45724 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217056 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 463.48
Current children cumulated vsize (Kb) 355228

[startup+480.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 46725 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217076 134629227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 473.49
Current children cumulated vsize (Kb) 355228

[startup+490.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 47725 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216528 134693563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 483.49
Current children cumulated vsize (Kb) 355228

[startup+500.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 48725 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217016 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 493.49
Current children cumulated vsize (Kb) 355228

[startup+510.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 49725 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216880 134693561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 503.49
Current children cumulated vsize (Kb) 355228

[startup+520.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 50726 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217152 134844725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 513.5
Current children cumulated vsize (Kb) 355228

[startup+530.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 51726 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217040 134694528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 523.5
Current children cumulated vsize (Kb) 355228

[startup+540.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 52726 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217056 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 533.5
Current children cumulated vsize (Kb) 355228

[startup+550.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 53726 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217424 134628649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 543.5
Current children cumulated vsize (Kb) 355228

[startup+560.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 54726 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217760 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 553.5
Current children cumulated vsize (Kb) 355228

[startup+570.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 55727 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217216 134694539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 563.51
Current children cumulated vsize (Kb) 355228

[startup+580.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 56727 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216656 134718203 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 573.51
Current children cumulated vsize (Kb) 355228

[startup+590.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 57727 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217504 134844736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 583.51
Current children cumulated vsize (Kb) 355228

[startup+600.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 58727 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216868 134849060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 593.51
Current children cumulated vsize (Kb) 355228

[startup+610.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 59728 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217056 134849071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 603.52
Current children cumulated vsize (Kb) 355228

[startup+620.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 60728 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217360 134695298 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 613.52
Current children cumulated vsize (Kb) 355228

[startup+630.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 61728 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217340 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 623.52
Current children cumulated vsize (Kb) 355228

[startup+640.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 62728 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217536 134522497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 633.52
Current children cumulated vsize (Kb) 355228

[startup+650.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 63729 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217352 134846929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 643.53
Current children cumulated vsize (Kb) 355228

[startup+660.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 64729 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217052 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 653.53
Current children cumulated vsize (Kb) 355228

[startup+670.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 65729 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217052 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 663.53
Current children cumulated vsize (Kb) 355228

[startup+680.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 66729 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217568 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 673.53
Current children cumulated vsize (Kb) 355228

[startup+690.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 67730 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216656 134718203 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 683.54
Current children cumulated vsize (Kb) 355228

[startup+700.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 68730 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216624 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 693.54
Current children cumulated vsize (Kb) 355228

[startup+710.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 69730 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217584 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 703.54
Current children cumulated vsize (Kb) 355228

[startup+720.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 70730 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217072 134629080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 713.54
Current children cumulated vsize (Kb) 355228

[startup+730.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 71730 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217396 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 723.54
Current children cumulated vsize (Kb) 355228

[startup+740.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 72731 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217936 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 733.55
Current children cumulated vsize (Kb) 355228

[startup+750.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 73731 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217884 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 743.55
Current children cumulated vsize (Kb) 355228

[startup+760.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 74731 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217132 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 753.55
Current children cumulated vsize (Kb) 355228

[startup+770.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 75731 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217744 134843113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 763.55
Current children cumulated vsize (Kb) 355228

[startup+780.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 76732 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217744 134849099 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 773.56
Current children cumulated vsize (Kb) 355228

[startup+790.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 77732 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217296 134844672 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 783.56
Current children cumulated vsize (Kb) 355228

[startup+800.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 78732 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217760 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 793.56
Current children cumulated vsize (Kb) 355228

[startup+810.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 79732 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217196 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 803.56
Current children cumulated vsize (Kb) 355228

[startup+820.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 80733 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217232 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 813.57
Current children cumulated vsize (Kb) 355228

[startup+830.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 81733 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216800 134844703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 823.57
Current children cumulated vsize (Kb) 355228

[startup+840.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 82733 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216876 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 833.57
Current children cumulated vsize (Kb) 355228

[startup+850.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 83733 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217328 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 843.57
Current children cumulated vsize (Kb) 355228

[startup+860.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 84734 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217424 134629259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 853.58
Current children cumulated vsize (Kb) 355228

[startup+870.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 85734 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221216800 134844731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 863.58
Current children cumulated vsize (Kb) 355228

[startup+880.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 86734 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217872 134843113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 873.58
Current children cumulated vsize (Kb) 355228

[startup+890.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 87734 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217184 134693570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 883.58
Current children cumulated vsize (Kb) 355228

[startup+900.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 88735 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217596 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 893.59
Current children cumulated vsize (Kb) 355228

[startup+910.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 89735 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217488 134845895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 903.59
Current children cumulated vsize (Kb) 355228

[startup+920.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 90735 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217936 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 913.59
Current children cumulated vsize (Kb) 355228

[startup+930.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 91735 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217872 134696578 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 923.59
Current children cumulated vsize (Kb) 355228

[startup+940.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 92736 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217340 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 933.6
Current children cumulated vsize (Kb) 355228

[startup+950.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 93736 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217668 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 943.6
Current children cumulated vsize (Kb) 355228

[startup+960.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 94736 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217568 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 953.6
Current children cumulated vsize (Kb) 355228

[startup+970.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 95736 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217328 134845933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 963.6
Current children cumulated vsize (Kb) 355228

[startup+980.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 96736 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217608 134629277 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 973.6
Current children cumulated vsize (Kb) 355228

[startup+990.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 97737 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217760 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 983.61
Current children cumulated vsize (Kb) 355228

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 98737 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217660 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 993.61
Current children cumulated vsize (Kb) 355228

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 99737 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221218980 134849086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1003.61
Current children cumulated vsize (Kb) 355228

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 100737 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217340 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1013.61
Current children cumulated vsize (Kb) 355228

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 101738 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217568 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1023.62
Current children cumulated vsize (Kb) 355228

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 102738 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217504 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1033.62
Current children cumulated vsize (Kb) 355228

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 103738 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217152 134843130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1043.62
Current children cumulated vsize (Kb) 355228

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 104738 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217136 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1053.62
Current children cumulated vsize (Kb) 355228

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 105738 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217728 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1063.62
Current children cumulated vsize (Kb) 355228

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 106739 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221218080 134849148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1073.63
Current children cumulated vsize (Kb) 355228

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 107739 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217400 134722657 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1083.63
Current children cumulated vsize (Kb) 355228

[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 108739 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217372 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1093.63
Current children cumulated vsize (Kb) 355228

[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 109740 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217936 134693566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1103.64
Current children cumulated vsize (Kb) 355228

[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 110740 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217728 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1113.64
Current children cumulated vsize (Kb) 355228

[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 111740 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221218240 134844672 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1123.64
Current children cumulated vsize (Kb) 355228

[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 112740 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217952 134629275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1133.64
Current children cumulated vsize (Kb) 355228

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 113741 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217364 134844636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1143.65
Current children cumulated vsize (Kb) 355228

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 114741 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217940 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1153.65
Current children cumulated vsize (Kb) 355228

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 115741 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217872 134696656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1163.65
Current children cumulated vsize (Kb) 355228

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 116741 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217308 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1173.65
Current children cumulated vsize (Kb) 355228

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 117741 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221218120 134693729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1183.65
Current children cumulated vsize (Kb) 355228

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 118742 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217504 134844725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1193.66
Current children cumulated vsize (Kb) 355228

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 119742 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217792 134844708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1203.66
Current children cumulated vsize (Kb) 355228



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29223
Raw data (/proc/29218/stat): 29218 (minisat+_script) S 29217 29218 17733 0 -1 0 314 7173 0 0 0 1 107 29 17 0 1 0 1729062449 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29218/statm): 532 234 485 147 0 385 0
[pid=29218] vsize: 2128
Raw data (/proc/29223/stat): 29223 (minisat+_bignum) R 29218 29218 17733 0 -1 0 87713 0 3 0 119742 487 0 0 25 0 1 0 1729062680 361574400 83742 4294967295 134512640 135167914 3221224448 3221217792 134844697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29223/statm): 88275 83742 162 162 0 88113 0
[pid=29223] vsize: 353100
Current children cumulated CPU time (s) 1203.66
Current children cumulated vsize (Kb) 355228

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

Child status: 0
Real time (s): 1210.24
CPU time (s): 1202.45
CPU user time (s): 1197.43
CPU system time (s): 5.02623
CPU usage (%): 99.3566
Max. virtual memory (cumulated for all children) (Kb): 361708

Verifier Data

ERROR: no interpretation found !