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/miplib3/normalized-mps-v2-20-10-modglob.opb
MD5SUM4a035426d91356eed5e979934e763294
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 4538

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        883856 kB
Buffers:         36080 kB
Cached:          87212 kB
SwapCached:        536 kB
Active:          73652 kB
Inactive:        52200 kB
HighTotal:      131008 kB
HighFree:        41804 kB
LowTotal:       903652 kB
LowFree:        842052 kB
SwapTotal:     2097892 kB
SwapFree:      2096832 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5868 kB
Slab:            19472 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 18:25:54 (client local time) WITH STATUS 0 IN 1203.1 SECONDS
stats: 2992 7 1203.1 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/7767/stat): 7767 (minisat+_script) R 7766 7767 21452 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1851921832 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/7767/statm): 174 3 169 147 0 27 0
[pid=7767] 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=7768
New process pid=7769
New process pid=7770
execve syscall for /bin/sed executable
One traced child (pid=7769) 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=7770) exited with status: 0
One traced child (pid=7768) exited with status: 0
New process pid=7771
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-modglob.opb
One traced child (pid=7771) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=7772
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-modglob.opb

[startup+10.0041 s]
Raw data (loadavg): 0.93 0.95 0.88 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 5262 0 0 0 946 22 0 0 25 0 1 0 1851921839 19447808 4570 4294967295 134512640 135167914 3221224448 3221197692 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7772/statm): 4748 4570 162 162 0 4586 0
[pid=7772] vsize: 18992
Current children cumulated CPU time (s) 9.71
Current children cumulated vsize (Kb) 21120

[startup+20.0048 s]
Raw data (loadavg): 0.94 0.96 0.88 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 10909 0 0 0 1897 46 0 0 25 0 1 0 1851921839 39878656 9558 4294967295 134512640 135167914 3221224448 3221196120 134845939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7772/statm): 9736 9558 162 162 0 9574 0
[pid=7772] vsize: 38944
Current children cumulated CPU time (s) 19.46
Current children cumulated vsize (Kb) 41072

[startup+30.0055 s]
Raw data (loadavg): 0.95 0.96 0.88 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 17652 0 0 0 2845 73 0 0 25 0 1 0 1851921839 62099456 14983 4294967295 134512640 135167914 3221224448 3221196572 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7772/statm): 15161 14983 162 162 0 14999 0
[pid=7772] vsize: 60644
Current children cumulated CPU time (s) 29.21
Current children cumulated vsize (Kb) 62772

[startup+40.0062 s]
Raw data (loadavg): 0.95 0.96 0.88 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 22165 0 0 0 3800 93 0 0 25 0 1 0 1851921839 80584704 19496 4294967295 134512640 135167914 3221224448 3221201024 134695622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7772/statm): 19674 19496 162 162 0 19512 0
[pid=7772] vsize: 78696
Current children cumulated CPU time (s) 38.96
Current children cumulated vsize (Kb) 80824

[startup+50.0079 s]
Raw data (loadavg): 0.96 0.96 0.88 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 30966 0 0 0 4749 121 0 0 25 0 1 0 1851921839 105832448 25660 4294967295 134512640 135167914 3221224448 3221196768 134695578 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 25838 25660 162 162 0 25676 0
[pid=7772] vsize: 103352
Current children cumulated CPU time (s) 48.73
Current children cumulated vsize (Kb) 105480

[startup+60.0086 s]
Raw data (loadavg): 0.97 0.96 0.88 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 35422 0 0 0 5699 143 0 0 25 0 1 0 1851921839 124084224 30116 4294967295 134512640 135167914 3221224448 3221196572 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7772/statm): 30294 30116 162 162 0 30132 0
[pid=7772] vsize: 121176
Current children cumulated CPU time (s) 58.45
Current children cumulated vsize (Kb) 123304

[startup+70.0094 s]
Raw data (loadavg): 0.97 0.96 0.88 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 39812 0 0 0 6654 161 0 0 25 0 1 0 1851921839 142065664 34506 4294967295 134512640 135167914 3221224448 3221197264 134849122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7772/statm): 34684 34506 162 162 0 34522 0
[pid=7772] vsize: 138736
Current children cumulated CPU time (s) 68.18
Current children cumulated vsize (Kb) 140864

[startup+80.0111 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 54026 0 0 0 7594 199 0 0 25 0 1 0 1851921839 200286208 48720 4294967295 134512640 135167914 3221224448 3221198144 134624959 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7772/statm): 48898 48720 162 162 0 48736 0
[pid=7772] vsize: 195592
Current children cumulated CPU time (s) 77.96
Current children cumulated vsize (Kb) 197720

[startup+90.0118 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 57214 0 0 0 8561 214 0 0 25 0 1 0 1851921839 191746048 46635 4294967295 134512640 135167914 3221224448 3221198224 134849148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7772/statm): 46813 46635 162 162 0 46651 0
[pid=7772] vsize: 187252
Current children cumulated CPU time (s) 87.78
Current children cumulated vsize (Kb) 189380

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 61572 0 0 0 9513 236 0 0 25 0 1 0 1851921839 209596416 50993 4294967295 134512640 135167914 3221224448 3221201132 134847144 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7772/statm): 51171 50993 162 162 0 51009 0
[pid=7772] vsize: 204684
Current children cumulated CPU time (s) 97.52
Current children cumulated vsize (Kb) 206812

[startup+110.013 s]
Raw data (loadavg): 0.98 0.96 0.89 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 65896 0 0 0 10468 253 0 0 25 0 1 0 1851921839 227307520 55317 4294967295 134512640 135167914 3221224448 3221198560 134696152 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7772/statm): 55495 55317 162 162 0 55333 0
[pid=7772] vsize: 221980
Current children cumulated CPU time (s) 107.24
Current children cumulated vsize (Kb) 224108

[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 70183 0 0 0 11424 272 0 0 25 0 1 0 1851921839 244867072 59604 4294967295 134512640 135167914 3221224448 3221196056 134694458 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7772/statm): 59782 59604 162 162 0 59620 0
[pid=7772] vsize: 239128
Current children cumulated CPU time (s) 116.99
Current children cumulated vsize (Kb) 241256

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.89 1/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) T 7767 7767 21452 0 -1 0 74366 0 0 0 12374 292 0 0 25 0 1 0 1851921839 262000640 63787 4294967295 134512640 135167914 3221224448 3221195580 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7772/statm): 63965 63787 162 162 0 63803 0
[pid=7772] vsize: 255860
Current children cumulated CPU time (s) 126.69
Current children cumulated vsize (Kb) 257988

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 78498 0 0 0 13328 309 0 0 25 0 1 0 1851921839 278925312 67919 4294967295 134512640 135167914 3221224448 3221197632 134844703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7772/statm): 68097 67919 162 162 0 67935 0
[pid=7772] vsize: 272388
Current children cumulated CPU time (s) 136.4
Current children cumulated vsize (Kb) 274516

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) T 7767 7767 21452 0 -1 0 82598 0 0 0 14282 329 0 0 25 0 1 0 1851921839 295718912 72019 4294967295 134512640 135167914 3221224448 3221196220 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7772/statm): 72197 72019 162 162 0 72035 0
[pid=7772] vsize: 288788
Current children cumulated CPU time (s) 146.14
Current children cumulated vsize (Kb) 290916

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 106930 0 0 0 15200 391 0 0 25 0 1 0 1851921839 395382784 96351 4294967295 134512640 135167914 3221224448 3221199916 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 96529 96351 162 162 0 96367 0
[pid=7772] vsize: 386116
Current children cumulated CPU time (s) 155.94
Current children cumulated vsize (Kb) 388244

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.89 1/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) T 7767 7767 21452 0 -1 0 108263 0 0 0 16183 400 0 0 25 0 1 0 1851921839 357646336 87138 4294967295 134512640 135167914 3221224448 3221197340 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7772/statm): 87316 87138 162 162 0 87154 0
[pid=7772] vsize: 349264
Current children cumulated CPU time (s) 165.86
Current children cumulated vsize (Kb) 351392

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 112281 0 0 0 17138 419 0 0 25 0 1 0 1851921839 374104064 91156 4294967295 134512640 135167914 3221224448 3221196368 134849092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7772/statm): 91334 91156 162 162 0 91172 0
[pid=7772] vsize: 365336
Current children cumulated CPU time (s) 175.6
Current children cumulated vsize (Kb) 367464

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 116259 0 0 0 18094 437 0 0 25 0 1 0 1851921839 390397952 95134 4294967295 134512640 135167914 3221224448 3221196080 134624032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7772/statm): 95312 95134 162 162 0 95150 0
[pid=7772] vsize: 381248
Current children cumulated CPU time (s) 185.34
Current children cumulated vsize (Kb) 383376

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 120241 0 0 0 19049 455 0 0 25 0 1 0 1851921839 406708224 99116 4294967295 134512640 135167914 3221224448 3221198556 134843002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7772/statm): 99294 99116 162 162 0 99132 0
[pid=7772] vsize: 397176
Current children cumulated CPU time (s) 195.07
Current children cumulated vsize (Kb) 399304

[startup+210.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 124192 0 0 0 20005 473 0 0 25 0 1 0 1851921839 422891520 103067 4294967295 134512640 135167914 3221224448 3221198432 134844720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7772/statm): 103245 103067 162 162 0 103083 0
[pid=7772] vsize: 412980
Current children cumulated CPU time (s) 204.81
Current children cumulated vsize (Kb) 415108

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) T 7767 7767 21452 0 -1 0 128118 0 0 0 20960 492 0 0 25 0 1 0 1851921839 438972416 106993 4294967295 134512640 135167914 3221224448 3221197340 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7772/statm): 107171 106993 162 162 0 107009 0
[pid=7772] vsize: 428684
Current children cumulated CPU time (s) 214.55
Current children cumulated vsize (Kb) 430812

[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 131943 0 0 0 21918 507 0 0 25 0 1 0 1851921839 454639616 110818 4294967295 134512640 135167914 3221224448 3221198976 134844725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 110996 110818 162 162 0 110834 0
[pid=7772] vsize: 443984
Current children cumulated CPU time (s) 224.28
Current children cumulated vsize (Kb) 446112

[startup+240.02 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 135744 0 0 0 22877 526 0 0 25 0 1 0 1851921839 470208512 114619 4294967295 134512640 135167914 3221224448 3221196320 134695569 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 114797 114619 162 162 0 114635 0
[pid=7772] vsize: 459188
Current children cumulated CPU time (s) 234.06
Current children cumulated vsize (Kb) 461316

[startup+250.021 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 139509 0 0 0 23837 543 0 0 25 0 1 0 1851921839 485629952 118384 4294967295 134512640 135167914 3221224448 3221199136 134849533 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 118562 118384 162 162 0 118400 0
[pid=7772] vsize: 474248
Current children cumulated CPU time (s) 243.83
Current children cumulated vsize (Kb) 476376

[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 143227 0 0 0 24797 559 0 0 25 0 1 0 1851921839 500858880 122102 4294967295 134512640 135167914 3221224448 3221196064 134695154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 122280 122102 162 162 0 122118 0
[pid=7772] vsize: 489120
Current children cumulated CPU time (s) 253.59
Current children cumulated vsize (Kb) 491248

[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 146896 0 0 0 25760 572 0 0 25 0 1 0 1851921839 515887104 125771 4294967295 134512640 135167914 3221224448 3221198172 134691200 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 125949 125771 162 162 0 125787 0
[pid=7772] vsize: 503796
Current children cumulated CPU time (s) 263.35
Current children cumulated vsize (Kb) 505924

[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 150566 0 0 0 26716 591 0 0 25 0 1 0 1851921839 530919424 129441 4294967295 134512640 135167914 3221224448 3221198180 134620491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7772/statm): 129619 129441 162 162 0 129457 0
[pid=7772] vsize: 518476
Current children cumulated CPU time (s) 273.1
Current children cumulated vsize (Kb) 520604

[startup+290.023 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) T 7767 7767 21452 0 -1 0 154213 0 0 0 27678 608 0 0 25 0 1 0 1851921839 545857536 133088 4294967295 134512640 135167914 3221224448 3221195468 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7772/statm): 133266 133088 162 162 0 133104 0
[pid=7772] vsize: 533064
Current children cumulated CPU time (s) 282.89
Current children cumulated vsize (Kb) 535192

[startup+300.024 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) T 7767 7767 21452 0 -1 0 157823 0 0 0 28641 625 0 0 25 0 1 0 1851921839 560656384 136698 4294967295 134512640 135167914 3221224448 3221198364 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7772/statm): 136879 136698 162 162 0 136717 0
[pid=7772] vsize: 547516
Current children cumulated CPU time (s) 292.69
Current children cumulated vsize (Kb) 549644

[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 29636 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221222984 134846944 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 302.68
Current children cumulated vsize (Kb) 465524

[startup+320.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 30637 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221217392 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 312.69
Current children cumulated vsize (Kb) 465524

[startup+330.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 31637 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221217368 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 322.69
Current children cumulated vsize (Kb) 465524

[startup+340.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 32637 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221217616 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 332.69
Current children cumulated vsize (Kb) 465524

[startup+350.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 33637 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221217604 134630852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 342.69
Current children cumulated vsize (Kb) 465524

[startup+360.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 34638 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218272 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 352.7
Current children cumulated vsize (Kb) 465524

[startup+370.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 35638 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218124 134694480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 362.7
Current children cumulated vsize (Kb) 465524

[startup+380.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 36638 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218096 134843064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 372.7
Current children cumulated vsize (Kb) 465524

[startup+390.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 37639 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221217968 134629307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 382.71
Current children cumulated vsize (Kb) 465524

[startup+400.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 38639 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218292 134696180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 392.71
Current children cumulated vsize (Kb) 465524

[startup+410.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 39639 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218368 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 402.71
Current children cumulated vsize (Kb) 465524

[startup+420.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 40639 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221217936 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 412.71
Current children cumulated vsize (Kb) 465524

[startup+430.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 41640 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219296 134695307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 422.72
Current children cumulated vsize (Kb) 465524

[startup+440.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 42640 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221217760 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 432.72
Current children cumulated vsize (Kb) 465524

[startup+450.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 43640 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218436 134845938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 442.72
Current children cumulated vsize (Kb) 465524

[startup+460.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 44640 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218672 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 452.72
Current children cumulated vsize (Kb) 465524

[startup+470.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 45641 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221217744 134694539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 462.73
Current children cumulated vsize (Kb) 465524

[startup+480.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 46641 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218912 134845895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 472.73
Current children cumulated vsize (Kb) 465524

[startup+490.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 47641 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218364 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 482.73
Current children cumulated vsize (Kb) 465524

[startup+500.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 48641 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219128 134844674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 492.73
Current children cumulated vsize (Kb) 465524

[startup+510.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 49642 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219328 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 502.74
Current children cumulated vsize (Kb) 465524

[startup+520.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 50642 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218464 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 512.74
Current children cumulated vsize (Kb) 465524

[startup+530.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 51642 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219536 134629290 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 522.74
Current children cumulated vsize (Kb) 465524

[startup+540.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 52642 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219024 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 532.74
Current children cumulated vsize (Kb) 465524

[startup+550.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 53642 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219136 134722539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 542.74
Current children cumulated vsize (Kb) 465524

[startup+560.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 54643 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219104 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 552.75
Current children cumulated vsize (Kb) 465524

[startup+570.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 55643 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218192 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 562.75
Current children cumulated vsize (Kb) 465524

[startup+580.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 56643 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219596 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 572.75
Current children cumulated vsize (Kb) 465524

[startup+590.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 57643 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219112 134723211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 582.75
Current children cumulated vsize (Kb) 465524

[startup+600.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 58644 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219704 134693754 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 592.76
Current children cumulated vsize (Kb) 465524

[startup+610.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 59644 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218972 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 602.76
Current children cumulated vsize (Kb) 465524

[startup+620.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 60644 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219252 134718502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 612.76
Current children cumulated vsize (Kb) 465524

[startup+630.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 61644 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218256 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 622.76
Current children cumulated vsize (Kb) 465524

[startup+640.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 62645 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218208 134845906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 632.77
Current children cumulated vsize (Kb) 465524

[startup+650.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 63645 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218160 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 642.77
Current children cumulated vsize (Kb) 465524

[startup+660.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 64645 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219356 134522184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 652.77
Current children cumulated vsize (Kb) 465524

[startup+670.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 65645 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219232 134847235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 662.77
Current children cumulated vsize (Kb) 465524

[startup+680.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 66646 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218624 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 672.78
Current children cumulated vsize (Kb) 465524

[startup+690.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 67646 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218552 134844674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 682.78
Current children cumulated vsize (Kb) 465524

[startup+700.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 68646 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218252 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 692.78
Current children cumulated vsize (Kb) 465524

[startup+710.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 69647 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218972 134845940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 702.79
Current children cumulated vsize (Kb) 465524

[startup+720.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 70647 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219120 134722527 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 712.79
Current children cumulated vsize (Kb) 465524

[startup+730.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 71647 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219520 134843030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 722.79
Current children cumulated vsize (Kb) 465524

[startup+740.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 72647 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218800 134843113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 732.79
Current children cumulated vsize (Kb) 465524

[startup+750.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 73648 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218560 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 742.8
Current children cumulated vsize (Kb) 465524

[startup+760.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 74648 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218736 134696366 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 752.8
Current children cumulated vsize (Kb) 465524

[startup+770.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 75648 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218976 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 762.8
Current children cumulated vsize (Kb) 465524

[startup+780.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 76648 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218640 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 772.8
Current children cumulated vsize (Kb) 465524

[startup+790.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 77648 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219216 134844682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 782.8
Current children cumulated vsize (Kb) 465524

[startup+800.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 78649 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219216 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 792.81
Current children cumulated vsize (Kb) 465524

[startup+810.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 79649 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219288 134849057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 802.81
Current children cumulated vsize (Kb) 465524

[startup+820.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 80649 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218160 134845933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 812.81
Current children cumulated vsize (Kb) 465524

[startup+830.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 81649 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218448 134694504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 822.81
Current children cumulated vsize (Kb) 465524

[startup+840.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 82650 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218976 134694532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 832.82
Current children cumulated vsize (Kb) 465524

[startup+850.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 83650 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219680 134843068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 842.82
Current children cumulated vsize (Kb) 465524

[startup+860.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 84650 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218992 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 852.82
Current children cumulated vsize (Kb) 465524

[startup+870.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 85650 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218896 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 862.82
Current children cumulated vsize (Kb) 465524

[startup+880.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 86651 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218896 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 872.83
Current children cumulated vsize (Kb) 465524

[startup+890.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 87651 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218648 134693553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 882.83
Current children cumulated vsize (Kb) 465524

[startup+900.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 88651 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219128 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 892.83
Current children cumulated vsize (Kb) 465524

[startup+910.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 89651 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218620 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 902.83
Current children cumulated vsize (Kb) 465524

[startup+920.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 90652 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218272 134843160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 912.84
Current children cumulated vsize (Kb) 465524

[startup+930.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 91652 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218224 134696202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 922.84
Current children cumulated vsize (Kb) 465524

[startup+940.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 92652 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219504 134694532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 932.84
Current children cumulated vsize (Kb) 465524

[startup+950.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 93652 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218644 134849086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 942.84
Current children cumulated vsize (Kb) 465524

[startup+960.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 94653 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221220700 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 952.85
Current children cumulated vsize (Kb) 465524

[startup+970.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 95653 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218992 134849179 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 962.85
Current children cumulated vsize (Kb) 465524

[startup+980.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 96653 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218944 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 972.85
Current children cumulated vsize (Kb) 465524

[startup+990.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 97653 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218108 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 982.85
Current children cumulated vsize (Kb) 465524

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 98654 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219728 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 992.86
Current children cumulated vsize (Kb) 465524

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 99654 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218280 134722513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1002.86
Current children cumulated vsize (Kb) 465524

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 100654 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218448 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1012.86
Current children cumulated vsize (Kb) 465524

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 101654 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218640 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1022.86
Current children cumulated vsize (Kb) 465524

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 102655 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218648 134693793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1032.87
Current children cumulated vsize (Kb) 465524

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 103655 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218928 134843030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1042.87
Current children cumulated vsize (Kb) 465524

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 104655 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219180 134693585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1052.87
Current children cumulated vsize (Kb) 465524

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 105655 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218196 134844636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1062.87
Current children cumulated vsize (Kb) 465524

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 106656 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218560 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1072.88
Current children cumulated vsize (Kb) 465524

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 107656 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218544 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1082.88
Current children cumulated vsize (Kb) 465524

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 108656 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219152 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1092.88
Current children cumulated vsize (Kb) 465524

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 109656 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221217424 134630912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1102.88
Current children cumulated vsize (Kb) 465524

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 110657 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218752 134723288 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1112.89
Current children cumulated vsize (Kb) 465524

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 111657 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218384 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1122.89
Current children cumulated vsize (Kb) 465524

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 112657 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218800 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1132.89
Current children cumulated vsize (Kb) 465524

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 113657 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218652 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1142.89
Current children cumulated vsize (Kb) 465524

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 114657 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218304 134628680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1152.89
Current children cumulated vsize (Kb) 465524

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 115658 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218400 134843001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1162.9
Current children cumulated vsize (Kb) 465524

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 116658 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221220176 134695257 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1172.9
Current children cumulated vsize (Kb) 465524

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 117658 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221218816 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1182.9
Current children cumulated vsize (Kb) 465524

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 118658 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221220176 134522502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1192.9
Current children cumulated vsize (Kb) 465524

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 119659 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219680 134694532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1202.91
Current children cumulated vsize (Kb) 465524



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 7772
Raw data (/proc/7767/stat): 7767 (minisat+_script) S 7766 7767 21452 0 -1 0 314 332 0 0 0 1 0 2 21 0 1 0 1851921832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7767/statm): 532 234 485 147 0 385 0
[pid=7767] vsize: 2128
Raw data (/proc/7772/stat): 7772 (minisat+_bignum) R 7767 7767 21452 0 -1 0 157885 0 0 0 119659 629 0 0 25 0 1 0 1851921839 474517504 115669 4294967295 134512640 135167914 3221224448 3221219636 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7772/statm): 115849 115669 162 162 0 115687 0
[pid=7772] vsize: 463396
Current children cumulated CPU time (s) 1202.91
Current children cumulated vsize (Kb) 465524

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

Child status: 0
Real time (s): 1210.3
CPU time (s): 1203.1
CPU user time (s): 1196.59
CPU system time (s): 6.51001
CPU usage (%): 99.4051
Max. virtual memory (cumulated for all children) (Kb): 549644

Verifier Data

ERROR: no interpretation found !