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-boeing2.opb
MD5SUM9d4981de84e8fd488c4493c292301fa3
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 3114
Biggest coefficient in the objective function 40265318400000
Number of bits for the biggest coefficient in the objective function 46
Sum of the numbers in the objective function 2533036563346675
Number of bits of the sum of numbers in the objective function 52
Biggest number in a constraint 431563682611200
Number of bits of the biggest number in a constraint 49
Biggest sum of numbers in a constraint 17042207919312540
Number of bits of the biggest sum of numbers54
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables3371
Total number of constraints213
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 constraints213
Minimum length of a constraint12
Maximum length of a constraint2370

Trace number 2679

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        925096 kB
Buffers:         34504 kB
Cached:          48756 kB
SwapCached:        856 kB
Active:          64304 kB
Inactive:        21612 kB
HighTotal:      131008 kB
HighFree:        80724 kB
LowTotal:       903652 kB
LowFree:        844372 kB
SwapTotal:     2097136 kB
SwapFree:      2095712 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5720 kB
Slab:            18028 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 21:00:02 (client local time) WITH STATUS 0 IN 1205.28 SECONDS
stats: 2832 7 1205.28 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 258] 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/20941/stat): 20941 (minisat+_script) R 20940 20941 31915 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785965617 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/20941/statm): 174 3 169 147 0 27 0
[pid=20941] 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=20942
New process pid=20943
New process pid=20944
execve syscall for /bin/sed executable
One traced child (pid=20943) 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=20944) exited with status: 0
One traced child (pid=20942) exited with status: 0
New process pid=20945
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-boeing2.opb
One traced child (pid=20945) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=20946
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-boeing2.opb

[startup+10.0034 s]
Raw data (loadavg): 0.97 0.96 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 4700 0 0 0 944 20 0 0 25 0 1 0 1785965633 16670720 3902 4294967295 134512640 135167914 3221224448 3221199712 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 4070 3902 162 162 0 3908 0
[pid=20946] vsize: 16280
Current children cumulated CPU time (s) 9.75
Current children cumulated vsize (Kb) 18408

[startup+20.0053 s]
Raw data (loadavg): 0.97 0.96 0.93 1/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) T 20941 20941 31915 0 -1 0 10317 0 0 0 1889 46 0 0 25 0 1 0 1785965633 36978688 8860 4294967295 134512640 135167914 3221224448 3221199804 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/20946/statm): 9028 8860 162 162 0 8866 0
[pid=20946] vsize: 36112
Current children cumulated CPU time (s) 19.46
Current children cumulated vsize (Kb) 38240

[startup+30.0061 s]
Raw data (loadavg): 0.98 0.96 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 16842 0 0 0 2839 70 0 0 25 0 1 0 1785965633 58306560 14067 4294967295 134512640 135167914 3221224448 3221199740 134694368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 14235 14067 162 162 0 14073 0
[pid=20946] vsize: 56940
Current children cumulated CPU time (s) 29.2
Current children cumulated vsize (Kb) 59068

[startup+40.0059 s]
Raw data (loadavg): 0.98 0.96 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 21008 0 0 0 3795 90 0 0 25 0 1 0 1785965633 75370496 18233 4294967295 134512640 135167914 3221224448 3221200636 134624320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 18401 18233 162 162 0 18239 0
[pid=20946] vsize: 73604
Current children cumulated CPU time (s) 38.96
Current children cumulated vsize (Kb) 75732

[startup+50.0068 s]
Raw data (loadavg): 0.98 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 29492 0 0 0 4750 115 0 0 25 0 1 0 1785965633 99315712 24080 4294967295 134512640 135167914 3221224448 3221199328 134845130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 24247 24080 162 162 0 24085 0
[pid=20946] vsize: 96988
Current children cumulated CPU time (s) 48.76
Current children cumulated vsize (Kb) 99116

[startup+60.0076 s]
Raw data (loadavg): 0.98 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 33507 0 0 0 5703 133 0 0 25 0 1 0 1785965633 115757056 28095 4294967295 134512640 135167914 3221224448 3221199908 134844636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 28261 28095 162 162 0 28099 0
[pid=20946] vsize: 113044
Current children cumulated CPU time (s) 58.47
Current children cumulated vsize (Kb) 115172

[startup+70.0094 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 37353 0 0 0 6658 152 0 0 25 0 1 0 1785965633 131510272 31941 4294967295 134512640 135167914 3221224448 3221200752 134845933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 32107 31941 162 162 0 31945 0
[pid=20946] vsize: 128428
Current children cumulated CPU time (s) 68.21
Current children cumulated vsize (Kb) 130556

[startup+80.0103 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 41060 0 0 0 7619 167 0 0 25 0 1 0 1785965633 146690048 35648 4294967295 134512640 135167914 3221224448 3221200752 134624952 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 35813 35648 162 162 0 35651 0
[pid=20946] vsize: 143252
Current children cumulated CPU time (s) 77.97
Current children cumulated vsize (Kb) 145380

[startup+90.0101 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 53970 0 0 0 8572 200 0 0 25 0 1 0 1785965633 199569408 48558 4294967295 134512640 135167914 3221224448 3221201936 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 48723 48558 162 162 0 48561 0
[pid=20946] vsize: 194892
Current children cumulated CPU time (s) 87.83
Current children cumulated vsize (Kb) 197020

[startup+100.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 57141 0 0 0 9534 216 0 0 25 0 1 0 1785965633 190959616 46456 4294967295 134512640 135167914 3221224448 3221202536 134844674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 46621 46456 162 162 0 46459 0
[pid=20946] vsize: 186484
Current children cumulated CPU time (s) 97.61
Current children cumulated vsize (Kb) 188612

[startup+110.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 60738 0 0 0 10495 233 0 0 25 0 1 0 1785965633 205692928 50053 4294967295 134512640 135167914 3221224448 3221199680 134696152 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 50218 50053 162 162 0 50056 0
[pid=20946] vsize: 200872
Current children cumulated CPU time (s) 107.39
Current children cumulated vsize (Kb) 203000

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 64342 0 0 0 11459 247 0 0 25 0 1 0 1785965633 220454912 53657 4294967295 134512640 135167914 3221224448 3221200044 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 53822 53657 162 162 0 53660 0
[pid=20946] vsize: 215288
Current children cumulated CPU time (s) 117.17
Current children cumulated vsize (Kb) 217416

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 68012 0 0 0 12419 261 0 0 25 0 1 0 1785965633 235487232 57327 4294967295 134512640 135167914 3221224448 3221201280 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 57492 57327 162 162 0 57330 0
[pid=20946] vsize: 229968
Current children cumulated CPU time (s) 126.91
Current children cumulated vsize (Kb) 232096

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 71576 0 0 0 13382 274 0 0 25 0 1 0 1785965633 250081280 60891 4294967295 134512640 135167914 3221224448 3221200848 134849066 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 61055 60891 162 162 0 60893 0
[pid=20946] vsize: 244220
Current children cumulated CPU time (s) 136.67
Current children cumulated vsize (Kb) 246348

[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 75024 0 0 0 14346 289 0 0 25 0 1 0 1785965633 264204288 64339 4294967295 134512640 135167914 3221224448 3221201344 134844715 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 64503 64339 162 162 0 64341 0
[pid=20946] vsize: 258012
Current children cumulated CPU time (s) 146.46
Current children cumulated vsize (Kb) 260140

[startup+160.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 78461 0 0 0 15311 304 0 0 25 0 1 0 1785965633 278282240 67776 4294967295 134512640 135167914 3221224448 3221200088 134842997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 67940 67776 162 162 0 67778 0
[pid=20946] vsize: 271760
Current children cumulated CPU time (s) 156.26
Current children cumulated vsize (Kb) 273888

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 81932 0 0 0 16271 321 0 0 25 0 1 0 1785965633 292499456 71247 4294967295 134512640 135167914 3221224448 3221201056 134694407 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 71411 71247 162 162 0 71249 0
[pid=20946] vsize: 285644
Current children cumulated CPU time (s) 166.03
Current children cumulated vsize (Kb) 287772

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.93 1/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) T 20941 20941 31915 0 -1 0 85356 0 0 0 17235 336 0 0 25 0 1 0 1785965633 306520064 74671 4294967295 134512640 135167914 3221224448 3221199276 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/20946/statm): 74834 74671 162 162 0 74672 0
[pid=20946] vsize: 299336
Current children cumulated CPU time (s) 175.82
Current children cumulated vsize (Kb) 301464

[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 106868 0 0 0 18183 385 0 0 25 0 1 0 1785965633 351436800 85637 4294967295 134512640 135167914 3221224448 3221200064 134843426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 85800 85637 162 162 0 85638 0
[pid=20946] vsize: 343200
Current children cumulated CPU time (s) 185.79
Current children cumulated vsize (Kb) 345328

[startup+200.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) T 20941 20941 31915 0 -1 0 110143 0 0 0 19149 399 0 0 25 0 1 0 1785965633 364851200 88912 4294967295 134512640 135167914 3221224448 3221199708 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/20946/statm): 89075 88912 162 162 0 88913 0
[pid=20946] vsize: 356300
Current children cumulated CPU time (s) 195.59
Current children cumulated vsize (Kb) 358428

[startup+210.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 113555 0 0 0 20115 413 0 0 25 0 1 0 1785965633 378822656 92324 4294967295 134512640 135167914 3221224448 3221200000 134843107 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 92486 92324 162 162 0 92324 0
[pid=20946] vsize: 369944
Current children cumulated CPU time (s) 205.39
Current children cumulated vsize (Kb) 372072

[startup+220.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 116814 0 0 0 21081 426 0 0 25 0 1 0 1785965633 392167424 95583 4294967295 134512640 135167914 3221224448 3221200820 134849147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 95744 95583 162 162 0 95582 0
[pid=20946] vsize: 382976
Current children cumulated CPU time (s) 215.18
Current children cumulated vsize (Kb) 385104

[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 22060 433 0 0 25 0 1 0 1785965633 400191488 97542 4294967295 134512640 135167914 3221224448 3221223200 134693563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 97703 97542 162 162 0 97541 0
[pid=20946] vsize: 390812
Current children cumulated CPU time (s) 225.04
Current children cumulated vsize (Kb) 392940

[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 23056 437 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221218656 134629049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 235.04
Current children cumulated vsize (Kb) 308576

[startup+250.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 24056 437 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219164 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 245.04
Current children cumulated vsize (Kb) 308576

[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 25056 438 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219280 134696200 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 255.05
Current children cumulated vsize (Kb) 308576

[startup+270.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 26056 438 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219344 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 265.05
Current children cumulated vsize (Kb) 308576

[startup+280.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 27056 438 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221218908 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 275.05
Current children cumulated vsize (Kb) 308576

[startup+290.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 28055 439 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219668 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 285.05
Current children cumulated vsize (Kb) 308576

[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 29055 439 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221218988 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 295.05
Current children cumulated vsize (Kb) 308576

[startup+310.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 30055 439 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219100 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 305.05
Current children cumulated vsize (Kb) 308576

[startup+320.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 31055 440 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220352 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 315.06
Current children cumulated vsize (Kb) 308576

[startup+330.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 32055 440 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220000 134693563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 325.06
Current children cumulated vsize (Kb) 308576

[startup+340.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 33055 440 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219484 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 335.06
Current children cumulated vsize (Kb) 308576

[startup+350.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 34054 440 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220032 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 345.05
Current children cumulated vsize (Kb) 308576

[startup+360.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 35054 441 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219284 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 355.06
Current children cumulated vsize (Kb) 308576

[startup+370.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 36054 441 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219856 134694545 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 365.06
Current children cumulated vsize (Kb) 308576

[startup+380.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 37054 441 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220384 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 375.06
Current children cumulated vsize (Kb) 308576

[startup+390.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 38054 441 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220720 134522355 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 385.06
Current children cumulated vsize (Kb) 308576

[startup+400.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 39054 441 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220032 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 395.06
Current children cumulated vsize (Kb) 308576

[startup+410.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 40054 441 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220012 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 405.06
Current children cumulated vsize (Kb) 308576

[startup+420.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 41054 442 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219552 134844708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 415.07
Current children cumulated vsize (Kb) 308576

[startup+430.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 42053 442 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219120 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 425.06
Current children cumulated vsize (Kb) 308576

[startup+440.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 43053 442 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220672 134843074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 435.06
Current children cumulated vsize (Kb) 308576

[startup+450.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 44053 442 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220608 134629448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 445.06
Current children cumulated vsize (Kb) 308576

[startup+460.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 45053 443 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219540 134630869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 455.07
Current children cumulated vsize (Kb) 308576

[startup+470.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 46053 443 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219792 134843012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 465.07
Current children cumulated vsize (Kb) 308576

[startup+480.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 47053 443 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219984 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 475.07
Current children cumulated vsize (Kb) 308576

[startup+490.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 48053 443 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220504 134693686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 485.07
Current children cumulated vsize (Kb) 308576

[startup+500.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 49053 443 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219696 134696407 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 495.07
Current children cumulated vsize (Kb) 308576

[startup+510.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 50052 444 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220560 134849099 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 505.07
Current children cumulated vsize (Kb) 308576

[startup+520.039 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 51052 444 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220432 134629448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 515.07
Current children cumulated vsize (Kb) 308576

[startup+530.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 52052 444 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220496 134696781 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 525.07
Current children cumulated vsize (Kb) 308576

[startup+540.041 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 53051 446 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220236 134522361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 535.08
Current children cumulated vsize (Kb) 308576

[startup+550.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 54050 447 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219324 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 545.08
Current children cumulated vsize (Kb) 308576

[startup+560.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 55050 447 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220320 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 555.08
Current children cumulated vsize (Kb) 308576

[startup+570.044 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 56049 447 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220160 134843001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 565.07
Current children cumulated vsize (Kb) 308576

[startup+580.045 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 57049 448 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220400 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 575.08
Current children cumulated vsize (Kb) 308576

[startup+590.045 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 58048 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220320 134844715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 585.08
Current children cumulated vsize (Kb) 308576

[startup+600.046 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 59048 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220176 134849061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 595.08
Current children cumulated vsize (Kb) 308576

[startup+610.047 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 60048 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219264 134844736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 605.08
Current children cumulated vsize (Kb) 308576

[startup+620.047 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 61048 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220420 134629088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 615.08
Current children cumulated vsize (Kb) 308576

[startup+630.048 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 62048 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220760 134522185 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 625.08
Current children cumulated vsize (Kb) 308576

[startup+640.049 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 63049 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219504 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 635.09
Current children cumulated vsize (Kb) 308576

[startup+650.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 64049 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219528 134693815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 645.09
Current children cumulated vsize (Kb) 308576

[startup+660.051 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 65049 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219352 134693744 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 655.09
Current children cumulated vsize (Kb) 308576

[startup+670.052 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 66049 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219116 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 665.09
Current children cumulated vsize (Kb) 308576

[startup+680.052 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 67050 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220484 134843117 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 675.1
Current children cumulated vsize (Kb) 308576

[startup+690.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 68050 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219540 134630852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 685.1
Current children cumulated vsize (Kb) 308576

[startup+700.054 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 69050 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220784 134844725 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 695.1
Current children cumulated vsize (Kb) 308576

[startup+710.055 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 70050 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220496 134844691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 705.1
Current children cumulated vsize (Kb) 308576

[startup+720.056 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 71050 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221221424 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 715.1
Current children cumulated vsize (Kb) 308576

[startup+730.057 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 72051 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219616 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 725.11
Current children cumulated vsize (Kb) 308576

[startup+740.057 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 73051 449 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220304 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 735.11
Current children cumulated vsize (Kb) 308576

[startup+750.058 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 74051 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220592 134629224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 745.12
Current children cumulated vsize (Kb) 308576

[startup+760.059 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 75051 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220672 134844668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 755.12
Current children cumulated vsize (Kb) 308576

[startup+770.06 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 76052 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220672 134844725 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 765.13
Current children cumulated vsize (Kb) 308576

[startup+780.061 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 77052 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220672 134844725 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 775.13
Current children cumulated vsize (Kb) 308576

[startup+790.061 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 78052 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220040 134722513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 785.13
Current children cumulated vsize (Kb) 308576

[startup+800.061 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 79052 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219824 134844672 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 795.13
Current children cumulated vsize (Kb) 308576

[startup+810.062 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 80053 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220384 134849092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 805.14
Current children cumulated vsize (Kb) 308576

[startup+820.064 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 81053 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220304 134845930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 815.14
Current children cumulated vsize (Kb) 308576

[startup+830.065 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 82054 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220360 134844633 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 825.15
Current children cumulated vsize (Kb) 308576

[startup+840.074 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 83054 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220236 134694320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 835.15
Current children cumulated vsize (Kb) 308576

[startup+850.075 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 84055 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220760 134693815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 845.16
Current children cumulated vsize (Kb) 308576

[startup+860.075 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 85055 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220768 134629290 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 855.16
Current children cumulated vsize (Kb) 308576

[startup+870.076 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 86055 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220560 134843074 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 865.16
Current children cumulated vsize (Kb) 308576

[startup+880.077 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 87055 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220508 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 875.16
Current children cumulated vsize (Kb) 308576

[startup+890.078 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 88056 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220672 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 885.17
Current children cumulated vsize (Kb) 308576

[startup+900.079 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 89056 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220412 134694320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 895.17
Current children cumulated vsize (Kb) 308576

[startup+910.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 90056 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220608 134629024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 905.17
Current children cumulated vsize (Kb) 308576

[startup+920.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 91056 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219756 134844638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 915.17
Current children cumulated vsize (Kb) 308576

[startup+930.081 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 92057 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219296 134844637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 925.18
Current children cumulated vsize (Kb) 308576

[startup+940.082 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 93057 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220208 134694524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 935.18
Current children cumulated vsize (Kb) 308576

[startup+950.083 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 94057 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219888 134629345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 945.18
Current children cumulated vsize (Kb) 308576

[startup+960.084 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 95057 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221221136 134629382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 955.18
Current children cumulated vsize (Kb) 308576

[startup+970.085 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 96057 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220948 134630852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 965.18
Current children cumulated vsize (Kb) 308576

[startup+980.085 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 97058 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221221632 134849187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 975.19
Current children cumulated vsize (Kb) 308576

[startup+990.086 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 98058 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219968 134843107 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 985.19
Current children cumulated vsize (Kb) 308576

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 99058 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220144 134696353 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 995.19
Current children cumulated vsize (Kb) 308576

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 100058 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219980 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1005.19
Current children cumulated vsize (Kb) 308576

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 101059 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220320 134844736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1015.2
Current children cumulated vsize (Kb) 308576

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 102059 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220496 134843064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1025.2
Current children cumulated vsize (Kb) 308576

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 103059 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220432 134630728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1035.2
Current children cumulated vsize (Kb) 308576

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 104059 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219440 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1045.2
Current children cumulated vsize (Kb) 308576

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 105060 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220412 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1055.21
Current children cumulated vsize (Kb) 308576

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 106060 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220480 134845895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1065.21
Current children cumulated vsize (Kb) 308576

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 107060 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219680 134849092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1075.21
Current children cumulated vsize (Kb) 308576

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 108060 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220672 134843139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1085.21
Current children cumulated vsize (Kb) 308576

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 109060 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219872 134693570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1095.21
Current children cumulated vsize (Kb) 308576

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 110060 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220764 134696560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1105.21
Current children cumulated vsize (Kb) 308576

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 111061 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220928 134849066 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1115.22
Current children cumulated vsize (Kb) 308576

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 112061 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219984 134696578 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1125.22
Current children cumulated vsize (Kb) 308576

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 113061 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220144 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1135.22
Current children cumulated vsize (Kb) 308576

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 114061 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220848 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1145.22
Current children cumulated vsize (Kb) 308576

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 115062 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220692 134843000 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1155.23
Current children cumulated vsize (Kb) 308576

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 116062 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220080 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1165.23
Current children cumulated vsize (Kb) 308576

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 117062 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221219072 134845903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1175.23
Current children cumulated vsize (Kb) 308576

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 118063 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221221024 134843010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1185.24
Current children cumulated vsize (Kb) 308576

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.93 3/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 119063 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220864 134696653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1195.24
Current children cumulated vsize (Kb) 308576

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 120063 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220948 134628664 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1205.24
Current children cumulated vsize (Kb) 308576



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 20946
Raw data (/proc/20941/stat): 20941 (minisat+_script) S 20940 20941 31915 0 -1 0 314 532 0 0 0 1 8 2 17 0 1 0 1785965617 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20941/statm): 532 234 485 147 0 385 0
[pid=20941] vsize: 2128
Raw data (/proc/20946/stat): 20946 (minisat+_bignum) R 20941 20941 31915 0 -1 0 118773 0 0 0 120063 450 0 0 25 0 1 0 1785965633 313802752 76451 4294967295 134512640 135167914 3221224448 3221220888 134845939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20946/statm): 76612 76451 162 162 0 76450 0
[pid=20946] vsize: 306448
Current children cumulated CPU time (s) 1205.24
Current children cumulated vsize (Kb) 308576

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

Child status: 0
Real time (s): 1210.25
CPU time (s): 1205.28
CPU user time (s): 1200.64
CPU system time (s): 4.64129
CPU usage (%): 99.5891
Max. virtual memory (cumulated for all children) (Kb): 392940

Verifier Data

ERROR: no interpretation found !