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/MIPLIB/miplib/normalized-mps-v2-20-10-modglob.opb
MD5SUM2de26b7af333f64c2208bd35d6d5a979
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 9818
Biggest coefficient in the objective function 22009559908352000000
Number of bits for the biggest coefficient in the objective function 65
Sum of the numbers in the objective function 1485172925553747165184
Number of bits of the sum of numbers in the objective function 71
Biggest number in a constraint 22009559908352000000
Number of bits of the biggest number in a constraint 65
Biggest sum of numbers in a constraint 1485172925553747165184
Number of bits of the biggest sum of numbers71
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables9818
Total number of constraints389
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)98
Number of constraints which are nor clauses,nor cardinality constraints291
Minimum length of a constraint1
Maximum length of a constraint270

Trace number 3875

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        904192 kB
Buffers:         35248 kB
Cached:          71140 kB
SwapCached:        780 kB
Active:          73904 kB
Inactive:        35256 kB
HighTotal:      131008 kB
HighFree:        56196 kB
LowTotal:       903652 kB
LowFree:        847996 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              64 kB
Writeback:           0 kB
Mapped:           5804 kB
Slab:            15736 kB
Committed_AS:    64300 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 03:38:20 (client local time) WITH STATUS 0 IN 1202.99 SECONDS
stats: 2871 7 1202.99 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 426] 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/16466/stat): 16466 (minisat+_script) R 16465 16466 824 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788372785 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/16466/statm): 174 3 169 147 0 27 0
[pid=16466] 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=16467
New process pid=16468
New process pid=16469
execve syscall for /bin/sed executable
One traced child (pid=16468) 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=16469) exited with status: 0
One traced child (pid=16467) exited with status: 0
New process pid=16470
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-modglob.opb
One traced child (pid=16470) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=16471
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-modglob.opb

[startup+10.0031 s]
Raw data (loadavg): 0.94 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 5232 0 0 0 945 22 0 0 25 0 1 0 1788372792 19324928 4540 4294967295 134512640 135167914 3221224448 3221198804 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16471/statm): 4718 4540 162 162 0 4556 0
[pid=16471] vsize: 18872
Current children cumulated CPU time (s) 9.68
Current children cumulated vsize (Kb) 21000

[startup+20.0049 s]
Raw data (loadavg): 0.95 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 10872 0 0 0 1897 44 0 0 25 0 1 0 1788372792 39727104 9521 4294967295 134512640 135167914 3221224448 3221198736 134624994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 9699 9521 162 162 0 9537 0
[pid=16471] vsize: 38796
Current children cumulated CPU time (s) 19.42
Current children cumulated vsize (Kb) 40924

[startup+30.0056 s]
Raw data (loadavg): 0.96 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 17548 0 0 0 2844 70 0 0 25 0 1 0 1788372792 61673472 14879 4294967295 134512640 135167914 3221224448 3221196384 134847159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 15057 14879 162 162 0 14895 0
[pid=16471] vsize: 60228
Current children cumulated CPU time (s) 29.15
Current children cumulated vsize (Kb) 62356

[startup+40.0064 s]
Raw data (loadavg): 0.97 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 22006 0 0 0 3799 90 0 0 25 0 1 0 1788372792 79933440 19337 4294967295 134512640 135167914 3221224448 3221197468 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 19515 19337 162 162 0 19353 0
[pid=16471] vsize: 78060
Current children cumulated CPU time (s) 38.9
Current children cumulated vsize (Kb) 80188

[startup+50.0071 s]
Raw data (loadavg): 0.97 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) T 16466 16466 824 0 -1 0 30778 0 0 0 4748 117 0 0 25 0 1 0 1788372792 105062400 25472 4294967295 134512640 135167914 3221224448 3221197212 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/16471/statm): 25650 25472 162 162 0 25488 0
[pid=16471] vsize: 102600
Current children cumulated CPU time (s) 48.66
Current children cumulated vsize (Kb) 104728

[startup+60.0068 s]
Raw data (loadavg): 0.97 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) T 16466 16466 824 0 -1 0 35207 0 0 0 5699 138 0 0 25 0 1 0 1788372792 123203584 29901 4294967295 134512640 135167914 3221224448 3221197708 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/16471/statm): 30079 29901 162 162 0 29917 0
[pid=16471] vsize: 120316
Current children cumulated CPU time (s) 58.38
Current children cumulated vsize (Kb) 122444

[startup+70.0076 s]
Raw data (loadavg): 0.98 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 39550 0 0 0 6650 156 0 0 22 0 1 0 1788372792 140992512 34244 4294967295 134512640 135167914 3221224448 3221195908 134849086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16471/statm): 34422 34244 162 162 0 34260 0
[pid=16471] vsize: 137688
Current children cumulated CPU time (s) 68.07
Current children cumulated vsize (Kb) 139816

[startup+80.0083 s]
Raw data (loadavg): 0.98 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 54026 0 0 0 7582 197 0 0 25 0 1 0 1788372792 200286208 48720 4294967295 134512640 135167914 3221224448 3221198128 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 48898 48720 162 162 0 48736 0
[pid=16471] vsize: 195592
Current children cumulated CPU time (s) 77.8
Current children cumulated vsize (Kb) 197720

[startup+90.0091 s]
Raw data (loadavg): 0.98 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) T 16466 16466 824 0 -1 0 56879 0 0 0 8549 212 0 0 25 0 1 0 1788372792 190373888 46300 4294967295 134512640 135167914 3221224448 3221195740 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/16471/statm): 46478 46300 162 162 0 46316 0
[pid=16471] vsize: 185912
Current children cumulated CPU time (s) 87.62
Current children cumulated vsize (Kb) 188040

[startup+100.01 s]
Raw data (loadavg): 0.98 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 61184 0 0 0 9504 232 0 0 25 0 1 0 1788372792 208007168 50605 4294967295 134512640 135167914 3221224448 3221201024 134695563 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 50783 50605 162 162 0 50621 0
[pid=16471] vsize: 203132
Current children cumulated CPU time (s) 97.37
Current children cumulated vsize (Kb) 205260

[startup+110.011 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 65476 0 0 0 10453 252 0 0 25 0 1 0 1788372792 225587200 54897 4294967295 134512640 135167914 3221224448 3221196192 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16471/statm): 55075 54897 162 162 0 54913 0
[pid=16471] vsize: 220300
Current children cumulated CPU time (s) 107.06
Current children cumulated vsize (Kb) 222428

[startup+120.012 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 69752 0 0 0 11405 271 0 0 25 0 1 0 1788372792 243101696 59173 4294967295 134512640 135167914 3221224448 3221196316 134845882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 59351 59173 162 162 0 59189 0
[pid=16471] vsize: 237404
Current children cumulated CPU time (s) 116.77
Current children cumulated vsize (Kb) 239532

[startup+130.013 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 73905 0 0 0 12363 289 0 0 25 0 1 0 1788372792 260112384 63326 4294967295 134512640 135167914 3221224448 3221196088 134697257 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 63504 63326 162 162 0 63342 0
[pid=16471] vsize: 254016
Current children cumulated CPU time (s) 126.53
Current children cumulated vsize (Kb) 256144

[startup+140.014 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 78024 0 0 0 13321 308 0 0 25 0 1 0 1788372792 276983808 67445 4294967295 134512640 135167914 3221224448 3221197876 134697380 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16471/statm): 67623 67445 162 162 0 67461 0
[pid=16471] vsize: 270492
Current children cumulated CPU time (s) 136.3
Current children cumulated vsize (Kb) 272620

[startup+150.015 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 82099 0 0 0 14277 327 0 0 25 0 1 0 1788372792 293675008 71520 4294967295 134512640 135167914 3221224448 3221196800 134694517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 71698 71520 162 162 0 71536 0
[pid=16471] vsize: 286792
Current children cumulated CPU time (s) 146.05
Current children cumulated vsize (Kb) 288920

[startup+160.014 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 106930 0 0 0 15195 386 0 0 25 0 1 0 1788372792 395382784 96351 4294967295 134512640 135167914 3221224448 3221199916 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 96529 96351 162 162 0 96367 0
[pid=16471] vsize: 386116
Current children cumulated CPU time (s) 155.82
Current children cumulated vsize (Kb) 388244

[startup+170.015 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 107765 0 0 0 16185 391 0 0 25 0 1 0 1788372792 355606528 86640 4294967295 134512640 135167914 3221224448 3221197276 134695741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 86818 86640 162 162 0 86656 0
[pid=16471] vsize: 347272
Current children cumulated CPU time (s) 165.77
Current children cumulated vsize (Kb) 349400

[startup+180.015 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) T 16466 16466 824 0 -1 0 111798 0 0 0 17143 408 0 0 25 0 1 0 1788372792 372125696 90673 4294967295 134512640 135167914 3221224448 3221195740 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/16471/statm): 90851 90673 162 162 0 90689 0
[pid=16471] vsize: 363404
Current children cumulated CPU time (s) 175.52
Current children cumulated vsize (Kb) 365532

[startup+190.017 s]
Raw data (loadavg): 0.99 1.00 0.98 1/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) T 16466 16466 824 0 -1 0 115757 0 0 0 18100 425 0 0 25 0 1 0 1788372792 388341760 94632 4294967295 134512640 135167914 3221224448 3221197436 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/16471/statm): 94810 94632 162 162 0 94648 0
[pid=16471] vsize: 379240
Current children cumulated CPU time (s) 185.26
Current children cumulated vsize (Kb) 381368

[startup+200.017 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 119696 0 0 0 19056 443 0 0 25 0 1 0 1788372792 404475904 98571 4294967295 134512640 135167914 3221224448 3221207788 134843002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 98749 98571 162 162 0 98587 0
[pid=16471] vsize: 394996
Current children cumulated CPU time (s) 195
Current children cumulated vsize (Kb) 397124

[startup+210.017 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 123633 0 0 0 20015 460 0 0 25 0 1 0 1788372792 420601856 102508 4294967295 134512640 135167914 3221224448 3221198080 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16471/statm): 102686 102508 162 162 0 102524 0
[pid=16471] vsize: 410744
Current children cumulated CPU time (s) 204.76
Current children cumulated vsize (Kb) 412872

[startup+220.019 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 127570 0 0 0 20973 477 0 0 25 0 1 0 1788372792 436727808 106445 4294967295 134512640 135167914 3221224448 3221196264 134846853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16471/statm): 106623 106445 162 162 0 106461 0
[pid=16471] vsize: 426492
Current children cumulated CPU time (s) 214.51
Current children cumulated vsize (Kb) 428620

[startup+230.02 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 131454 0 0 0 21932 494 0 0 25 0 1 0 1788372792 452636672 110329 4294967295 134512640 135167914 3221224448 3221196480 134843160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16471/statm): 110507 110329 162 162 0 110345 0
[pid=16471] vsize: 442028
Current children cumulated CPU time (s) 224.27
Current children cumulated vsize (Kb) 444156

[startup+240.019 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 135317 0 0 0 22890 510 0 0 25 0 1 0 1788372792 468459520 114192 4294967295 134512640 135167914 3221224448 3221199932 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16471/statm): 114370 114192 162 162 0 114208 0
[pid=16471] vsize: 457480
Current children cumulated CPU time (s) 234.01
Current children cumulated vsize (Kb) 459608

[startup+250.02 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 139118 0 0 0 23846 527 0 0 25 0 1 0 1788372792 484028416 117993 4294967295 134512640 135167914 3221224448 3221195648 134696103 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16471/statm): 118171 117993 162 162 0 118009 0
[pid=16471] vsize: 472684
Current children cumulated CPU time (s) 243.74
Current children cumulated vsize (Kb) 474812

[startup+260.021 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 142883 0 0 0 24804 545 0 0 25 0 1 0 1788372792 499449856 121758 4294967295 134512640 135167914 3221224448 3221198064 134849066 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 121936 121758 162 162 0 121774 0
[pid=16471] vsize: 487744
Current children cumulated CPU time (s) 253.5
Current children cumulated vsize (Kb) 489872

[startup+270.021 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 146549 0 0 0 25767 560 0 0 25 0 1 0 1788372792 514465792 125424 4294967295 134512640 135167914 3221224448 3221197152 134843406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 125602 125424 162 162 0 125440 0
[pid=16471] vsize: 502408
Current children cumulated CPU time (s) 263.28
Current children cumulated vsize (Kb) 504536

[startup+280.022 s]
Raw data (loadavg): 0.99 1.00 0.98 1/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) T 16466 16466 824 0 -1 0 150192 0 0 0 26728 577 0 0 25 0 1 0 1788372792 529387520 129067 4294967295 134512640 135167914 3221224448 3221196364 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/16471/statm): 129245 129067 162 162 0 129083 0
[pid=16471] vsize: 516980
Current children cumulated CPU time (s) 273.06
Current children cumulated vsize (Kb) 519108

[startup+290.022 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 153868 0 0 0 27686 595 0 0 25 0 1 0 1788372792 544444416 132743 4294967295 134512640 135167914 3221224448 3221196288 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16471/statm): 132921 132743 162 162 0 132759 0
[pid=16471] vsize: 531684
Current children cumulated CPU time (s) 282.82
Current children cumulated vsize (Kb) 533812

[startup+300.023 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157525 0 0 0 28649 608 0 0 25 0 1 0 1788372792 559435776 136400 4294967295 134512640 135167914 3221224448 3221195744 134843130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16471/statm): 136581 136400 162 162 0 136419 0
[pid=16471] vsize: 546324
Current children cumulated CPU time (s) 292.58
Current children cumulated vsize (Kb) 548452

[startup+310.023 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157884 0 0 0 29642 613 0 0 25 0 1 0 1788372792 474517504 115668 4294967295 134512640 135167914 3221224448 3221223236 134623425 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115668 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 302.56
Current children cumulated vsize (Kb) 465524

[startup+320.024 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 30642 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217056 134693582 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 312.56
Current children cumulated vsize (Kb) 465524

[startup+330.025 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 31642 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217596 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 322.56
Current children cumulated vsize (Kb) 465524

[startup+340.025 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 32643 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217768 134693553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 332.57
Current children cumulated vsize (Kb) 465524

[startup+350.025 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 33643 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218128 134629138 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 342.57
Current children cumulated vsize (Kb) 465524

[startup+360.026 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 34643 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217488 134845909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 352.57
Current children cumulated vsize (Kb) 465524

[startup+370.027 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 35643 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217592 134694321 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 362.57
Current children cumulated vsize (Kb) 465524

[startup+380.028 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 36644 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218620 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 372.58
Current children cumulated vsize (Kb) 465524

[startup+390.028 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 37644 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217756 134849088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 382.58
Current children cumulated vsize (Kb) 465524

[startup+400.029 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 38644 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218112 134849099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 392.58
Current children cumulated vsize (Kb) 465524

[startup+410.03 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 39644 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218944 134522502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 402.58
Current children cumulated vsize (Kb) 465524

[startup+420.031 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 40645 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218936 134843032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 412.59
Current children cumulated vsize (Kb) 465524

[startup+430.031 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 41645 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219264 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 422.59
Current children cumulated vsize (Kb) 465524

[startup+440.032 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 42645 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218496 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 432.59
Current children cumulated vsize (Kb) 465524

[startup+450.033 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 43645 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217856 134844706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 442.59
Current children cumulated vsize (Kb) 465524

[startup+460.034 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 44646 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218736 134843400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 452.6
Current children cumulated vsize (Kb) 465524

[startup+470.034 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 45646 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219328 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 462.6
Current children cumulated vsize (Kb) 465524

[startup+480.035 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 46646 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218624 134843404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 472.6
Current children cumulated vsize (Kb) 465524

[startup+490.036 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 47646 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219352 134842997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 482.6
Current children cumulated vsize (Kb) 465524

[startup+500.037 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 48647 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218048 134723225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 492.61
Current children cumulated vsize (Kb) 465524

[startup+510.037 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 49647 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218816 134849143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 502.61
Current children cumulated vsize (Kb) 465524

[startup+520.038 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 50647 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218912 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 512.61
Current children cumulated vsize (Kb) 465524

[startup+530.039 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 51647 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218080 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 522.61
Current children cumulated vsize (Kb) 465524

[startup+540.039 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 52647 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219532 134693552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 532.61
Current children cumulated vsize (Kb) 465524

[startup+550.039 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 53648 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218588 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 542.62
Current children cumulated vsize (Kb) 465524

[startup+560.04 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 54648 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218560 134844706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 552.62
Current children cumulated vsize (Kb) 465524

[startup+570.041 s]
Raw data (loadavg): 0.99 1.00 0.98 3/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 55648 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219504 134843160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 562.62
Current children cumulated vsize (Kb) 465524

[startup+580.042 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 56648 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218412 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 572.62
Current children cumulated vsize (Kb) 465524

[startup+590.042 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 57649 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218288 134849061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 582.63
Current children cumulated vsize (Kb) 465524

[startup+600.043 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 58649 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219684 134849060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 592.63
Current children cumulated vsize (Kb) 465524

[startup+610.044 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 59649 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218476 134522184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 602.63
Current children cumulated vsize (Kb) 465524

[startup+620.045 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 60649 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218992 134849099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 612.63
Current children cumulated vsize (Kb) 465524

[startup+630.045 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 61650 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218272 134694545 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 622.64
Current children cumulated vsize (Kb) 465524

[startup+640.045 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 62650 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219888 134629080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 632.64
Current children cumulated vsize (Kb) 465524

[startup+650.046 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 63650 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217760 134849092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 642.64
Current children cumulated vsize (Kb) 465524

[startup+660.047 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 64650 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218256 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 652.64
Current children cumulated vsize (Kb) 465524

[startup+670.048 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 65651 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218032 134843113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 662.65
Current children cumulated vsize (Kb) 465524

[startup+680.049 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 66651 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221220192 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 672.65
Current children cumulated vsize (Kb) 465524

[startup+690.05 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 67651 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218208 134696745 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 682.65
Current children cumulated vsize (Kb) 465524

[startup+700.051 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 68651 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219104 134723225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 692.65
Current children cumulated vsize (Kb) 465524

[startup+710.051 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 69652 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218648 134694321 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 702.66
Current children cumulated vsize (Kb) 465524

[startup+720.052 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 70652 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219856 134843113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 712.66
Current children cumulated vsize (Kb) 465524

[startup+730.053 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 71652 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218988 134722656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 722.66
Current children cumulated vsize (Kb) 465524

[startup+740.053 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 72652 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218368 134845890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 732.66
Current children cumulated vsize (Kb) 465524

[startup+750.053 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 73653 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218368 134845888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 742.67
Current children cumulated vsize (Kb) 465524

[startup+760.054 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 74653 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219856 134849099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 752.67
Current children cumulated vsize (Kb) 465524

[startup+770.055 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 75653 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218560 134696745 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 762.67
Current children cumulated vsize (Kb) 465524

[startup+780.056 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 76653 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218640 134849092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 772.67
Current children cumulated vsize (Kb) 465524

[startup+790.055 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 77653 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219296 134720472 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 782.67
Current children cumulated vsize (Kb) 465524

[startup+800.056 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 78654 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219644 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 792.68
Current children cumulated vsize (Kb) 465524

[startup+810.057 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 79654 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218480 134629167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 802.68
Current children cumulated vsize (Kb) 465524

[startup+820.057 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 80654 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218472 134693744 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 812.68
Current children cumulated vsize (Kb) 465524

[startup+830.058 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 81654 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218624 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 822.68
Current children cumulated vsize (Kb) 465524

[startup+840.058 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 82655 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219184 134630940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 832.69
Current children cumulated vsize (Kb) 465524

[startup+850.059 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 83655 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219100 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 842.69
Current children cumulated vsize (Kb) 465524

[startup+860.059 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 84655 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221220048 134849187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 852.69
Current children cumulated vsize (Kb) 465524

[startup+870.061 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 85655 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218824 134843032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 862.69
Current children cumulated vsize (Kb) 465524

[startup+880.062 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 86656 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219088 134843026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 872.7
Current children cumulated vsize (Kb) 465524

[startup+890.062 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 87656 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218192 134845888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 882.7
Current children cumulated vsize (Kb) 465524

[startup+900.062 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 88656 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218468 134843031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 892.7
Current children cumulated vsize (Kb) 465524

[startup+910.063 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 89656 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219868 134722656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 902.7
Current children cumulated vsize (Kb) 465524

[startup+920.064 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 90657 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219000 134693808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 912.71
Current children cumulated vsize (Kb) 465524

[startup+930.065 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 91657 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219328 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 922.71
Current children cumulated vsize (Kb) 465524

[startup+940.065 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 92657 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218080 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 932.71
Current children cumulated vsize (Kb) 465524

[startup+950.066 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 93657 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219280 134843153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 942.71
Current children cumulated vsize (Kb) 465524

[startup+960.067 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 94658 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221220576 134693582 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 952.72
Current children cumulated vsize (Kb) 465524

[startup+970.069 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 95658 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219472 134845881 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 962.72
Current children cumulated vsize (Kb) 465524

[startup+980.069 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 96658 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219352 134696177 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 972.72
Current children cumulated vsize (Kb) 465524

[startup+990.069 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 97658 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219124 134845880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 982.72
Current children cumulated vsize (Kb) 465524

[startup+1000.07 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 98659 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219440 134844682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 992.73
Current children cumulated vsize (Kb) 465524

[startup+1010.07 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 99659 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221220144 134844731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1002.73
Current children cumulated vsize (Kb) 465524

[startup+1020.07 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 100659 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219008 134629216 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1012.73
Current children cumulated vsize (Kb) 465524

[startup+1030.07 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 101659 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217948 134693728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1022.73
Current children cumulated vsize (Kb) 465524

[startup+1040.07 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 102659 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218440 134845939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1032.73
Current children cumulated vsize (Kb) 465524

[startup+1050.07 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 103660 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217884 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1042.74
Current children cumulated vsize (Kb) 465524

[startup+1060.07 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 104660 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219520 134849099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1052.74
Current children cumulated vsize (Kb) 465524

[startup+1070.07 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 105660 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218956 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1062.74
Current children cumulated vsize (Kb) 465524

[startup+1080.07 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 106660 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218720 134718181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1072.74
Current children cumulated vsize (Kb) 465524

[startup+1090.08 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 107661 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218284 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1082.75
Current children cumulated vsize (Kb) 465524

[startup+1100.08 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 108661 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218384 134696342 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1092.75
Current children cumulated vsize (Kb) 465524

[startup+1110.08 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 109661 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218832 134629290 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1102.75
Current children cumulated vsize (Kb) 465524

[startup+1120.08 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 110661 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221217880 134723290 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1112.75
Current children cumulated vsize (Kb) 465524

[startup+1130.08 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 111662 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219884 134694480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1122.76
Current children cumulated vsize (Kb) 465524

[startup+1140.08 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 112662 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219168 134693561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1132.76
Current children cumulated vsize (Kb) 465524

[startup+1150.08 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 113662 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218208 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1142.76
Current children cumulated vsize (Kb) 465524

[startup+1160.08 s]
Raw data (loadavg): 1.07 1.02 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 114662 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218720 134844637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1152.76
Current children cumulated vsize (Kb) 465524

[startup+1170.08 s]
Raw data (loadavg): 1.06 1.02 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 115663 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219616 134844708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1162.77
Current children cumulated vsize (Kb) 465524

[startup+1180.08 s]
Raw data (loadavg): 1.05 1.01 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 116663 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221220144 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1172.77
Current children cumulated vsize (Kb) 465524

[startup+1190.08 s]
Raw data (loadavg): 1.04 1.01 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 117663 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218560 134843153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1182.77
Current children cumulated vsize (Kb) 465524

[startup+1200.08 s]
Raw data (loadavg): 1.03 1.01 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 118663 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218496 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1192.77
Current children cumulated vsize (Kb) 465524

[startup+1210.08 s]
Raw data (loadavg): 1.03 1.01 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 119664 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221219016 134629347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1202.78
Current children cumulated vsize (Kb) 465524



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.03 1.01 0.98 2/57 16471
Raw data (/proc/16466/stat): 16466 (minisat+_script) S 16465 16466 824 0 -1 0 314 332 0 0 0 1 0 0 22 0 1 0 1788372785 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16466/statm): 532 234 485 147 0 385 0
[pid=16466] vsize: 2128
Raw data (/proc/16471/stat): 16471 (minisat+_bignum) R 16466 16466 824 0 -1 0 157885 0 0 0 119664 613 0 0 25 0 1 0 1788372792 474517504 115669 4294967295 134512640 135167914 3221224448 3221218816 134522206 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16471/statm): 115849 115669 162 162 0 115687 0
[pid=16471] vsize: 463396
Current children cumulated CPU time (s) 1202.78
Current children cumulated vsize (Kb) 465524

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

Child status: 0
Real time (s): 1210.3
CPU time (s): 1202.99
CPU user time (s): 1196.64
CPU system time (s): 6.35203
CPU usage (%): 99.3961
Max. virtual memory (cumulated for all children) (Kb): 548452

Verifier Data

ERROR: no interpretation found !