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

Namesubmitted/manquinho/primes-dimacs-cnf/normalized-par32-2.opb
MD5SUM48ed39004ec868a1cad026c865b17eb2
Bench Categoryoptimization, small integers (OPTSMALLINT)
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 6352
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 6352
Number of bits of the sum of numbers in the objective function 13
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 6352
Number of bits of the biggest sum of numbers13
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables6352
Total number of constraints13429
Number of constraints which are clauses13429
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint3

Trace number 1535

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        693352 kB
Buffers:         35712 kB
Cached:         274508 kB
SwapCached:       1016 kB
Active:         102588 kB
Inactive:       210440 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        693100 kB
SwapTotal:     2097892 kB
SwapFree:      2096404 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5768 kB
Slab:            22536 kB
Committed_AS:    64376 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 15:50:15 (client local time) WITH STATUS 0 IN 1200.15 SECONDS
stats: 2536 7 1200.15 0

Solver Data

c Parsing PB file...
c Converting 13025 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9776    24386 |    3258       0        0     nan |  0.000 % |
c |       101 |    9776    24386 |    3583     101     1054    10.4 | 24.686 % |
c |       251 |    9776    24386 |    3942     251     5083    20.3 | 24.685 % |
c |       477 |    9776    24386 |    4336     477     7978    16.7 | 24.685 % |
c |       815 |    9776    24386 |    4770     815    19982    24.5 | 24.685 % |
c |      1322 |    9776    24386 |    5247    1322    33851    25.6 | 24.685 % |
c |      2082 |    9776    24386 |    5771    2082    53893    25.9 | 24.685 % |
c |      3222 |    9776    24386 |    6348    3222    85157    26.4 | 24.685 % |
c |      4930 |    9776    24386 |    6983    4930   135935    27.6 | 24.685 % |
c |      7493 |    9776    24386 |    7682    7493   211186    28.2 | 24.685 % |
c |     11337 |    9766    24364 |    8450    6645   174908    26.3 | 24.748 % |
c |     17104 |    9766    24364 |    9295    7259   205059    28.2 | 24.748 % |
c |     25753 |    9766    24364 |   10224   10390   302144    29.1 | 24.748 % |
c |     38728 |    9766    24364 |   11247   11443   271075    23.7 | 24.748 % |
c |     58190 |    9766    24364 |   12372   11483   266509    23.2 | 24.748 % |
c |     87382 |    9766    24364 |   13609   12488   344337    27.6 | 24.748 % |
c |    131171 |    9766    24364 |   14970   10333   228609    22.1 | 24.748 % |
c |    196855 |    9766    24364 |   16467    9460   209327    22.1 | 24.748 % |
c |    295382 |    9766    24364 |   18114   17181   397699    23.1 | 24.748 % |
c |    443171 |    9766    24364 |   19925   16694   376985    22.6 | 24.748 % |

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/15138/stat): 15138 (minisat+_script) R 15137 15138 9102 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1842307292 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/15138/statm): 174 3 169 147 0 27 0
[pid=15138] 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=15139
New process pid=15140
New process pid=15141
execve syscall for /bin/sed executable
One traced child (pid=15140) 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=15141) exited with status: 0
One traced child (pid=15139) exited with status: 0
New process pid=15142
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-par32-2.opb

[startup+10.0047 s]
Raw data (loadavg): 0.67 0.88 0.91 2/58 15142
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1316 0 0 0 985 5 0 0 25 0 1 0 1842307297 5627904 1265 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1374 1265 145 145 0 1229 0
[pid=15142] vsize: 5496
Current children cumulated CPU time (s) 9.92
Current children cumulated vsize (Kb) 7620

[startup+20.0056 s]
Raw data (loadavg): 0.72 0.89 0.91 2/58 15144
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 1984 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223088 134562128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0
[pid=15142] vsize: 5496
Current children cumulated CPU time (s) 19.91
Current children cumulated vsize (Kb) 7620

[startup+30.0066 s]
Raw data (loadavg): 0.76 0.89 0.91 2/58 15144
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 2984 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0
[pid=15142] vsize: 5496
Current children cumulated CPU time (s) 29.91
Current children cumulated vsize (Kb) 7620

[startup+40.0075 s]
Raw data (loadavg): 0.80 0.89 0.91 2/58 15144
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 3984 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0
[pid=15142] vsize: 5496
Current children cumulated CPU time (s) 39.91
Current children cumulated vsize (Kb) 7620

[startup+50.0084 s]
Raw data (loadavg): 0.83 0.89 0.91 2/58 15144
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 4984 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223040 134557215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0
[pid=15142] vsize: 5496
Current children cumulated CPU time (s) 49.91
Current children cumulated vsize (Kb) 7620

[startup+60.0093 s]
Raw data (loadavg): 0.85 0.90 0.91 2/58 15144
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 5985 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0
[pid=15142] vsize: 5496
Current children cumulated CPU time (s) 59.92
Current children cumulated vsize (Kb) 7620

[startup+70.0103 s]
Raw data (loadavg): 0.88 0.90 0.91 2/58 15144
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 6985 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223072 134562161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0
[pid=15142] vsize: 5496
Current children cumulated CPU time (s) 69.92
Current children cumulated vsize (Kb) 7620

[startup+80.0112 s]
Raw data (loadavg): 0.89 0.90 0.91 2/58 15146
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 7985 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0
[pid=15142] vsize: 5496
Current children cumulated CPU time (s) 79.92
Current children cumulated vsize (Kb) 7620

[startup+90.0121 s]
Raw data (loadavg): 0.91 0.91 0.91 2/58 15146
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 8985 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0
[pid=15142] vsize: 5496
Current children cumulated CPU time (s) 89.92
Current children cumulated vsize (Kb) 7620

[startup+100.013 s]
Raw data (loadavg): 0.92 0.91 0.91 2/58 15146
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 9986 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223120 134555585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0
[pid=15142] vsize: 5496
Current children cumulated CPU time (s) 99.93
Current children cumulated vsize (Kb) 7620

[startup+110.015 s]
Raw data (loadavg): 0.93 0.91 0.91 2/58 15146
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 10986 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0
[pid=15142] vsize: 5496
Current children cumulated CPU time (s) 109.93
Current children cumulated vsize (Kb) 7620

[startup+120.016 s]
Raw data (loadavg): 0.94 0.91 0.91 2/58 15146
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1323 0 0 0 11986 5 0 0 25 0 1 0 1842307297 5627904 1272 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1374 1272 145 145 0 1229 0
[pid=15142] vsize: 5496
Current children cumulated CPU time (s) 119.93
Current children cumulated vsize (Kb) 7620

[startup+130.016 s]
Raw data (loadavg): 0.95 0.92 0.91 2/58 15146
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1324 0 0 0 12986 5 0 0 25 0 1 0 1842307297 5627904 1273 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1374 1273 145 145 0 1229 0
[pid=15142] vsize: 5496
Current children cumulated CPU time (s) 129.93
Current children cumulated vsize (Kb) 7620

[startup+140.017 s]
Raw data (loadavg): 0.96 0.92 0.91 2/58 15148
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1324 0 0 0 13987 5 0 0 25 0 1 0 1842307297 5627904 1273 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1374 1273 145 145 0 1229 0
[pid=15142] vsize: 5496
Current children cumulated CPU time (s) 139.94
Current children cumulated vsize (Kb) 7620

[startup+150.018 s]
Raw data (loadavg): 0.97 0.92 0.91 2/58 15148
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1338 0 0 0 14986 6 0 0 25 0 1 0 1842307297 5685248 1287 4294967295 134512640 135094434 3221224448 3221223120 134555323 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1388 1287 145 145 0 1243 0
[pid=15142] vsize: 5552
Current children cumulated CPU time (s) 149.94
Current children cumulated vsize (Kb) 7676

[startup+160.019 s]
Raw data (loadavg): 0.97 0.92 0.91 2/58 15148
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1352 0 0 0 15987 6 0 0 25 0 1 0 1842307297 5758976 1301 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1406 1301 145 145 0 1261 0
[pid=15142] vsize: 5624
Current children cumulated CPU time (s) 159.95
Current children cumulated vsize (Kb) 7748

[startup+170.02 s]
Raw data (loadavg): 0.97 0.92 0.91 2/58 15148
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1364 0 0 0 16987 6 0 0 25 0 1 0 1842307297 5824512 1313 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15142/statm): 1422 1313 145 145 0 1277 0
[pid=15142] vsize: 5688
Current children cumulated CPU time (s) 169.95
Current children cumulated vsize (Kb) 7812

[startup+180.021 s]
Raw data (loadavg): 0.98 0.93 0.91 2/58 15148
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1391 0 0 0 17985 7 0 0 25 0 1 0 1842307297 5935104 1340 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15142/statm): 1449 1340 145 145 0 1304 0
[pid=15142] vsize: 5796
Current children cumulated CPU time (s) 179.94
Current children cumulated vsize (Kb) 7920

[startup+190.022 s]
Raw data (loadavg): 0.98 0.93 0.91 2/58 15148
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1400 0 0 0 18984 7 0 0 25 0 1 0 1842307297 6000640 1349 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1465 1349 145 145 0 1320 0
[pid=15142] vsize: 5860
Current children cumulated CPU time (s) 189.93
Current children cumulated vsize (Kb) 7984

[startup+200.023 s]
Raw data (loadavg): 0.98 0.93 0.91 2/58 15150
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1405 0 0 0 19984 7 0 0 25 0 1 0 1842307297 6033408 1354 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1473 1354 145 145 0 1328 0
[pid=15142] vsize: 5892
Current children cumulated CPU time (s) 199.93
Current children cumulated vsize (Kb) 8016

[startup+210.024 s]
Raw data (loadavg): 0.98 0.93 0.91 2/58 15150
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1405 0 0 0 20985 7 0 0 25 0 1 0 1842307297 6033408 1354 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1473 1354 145 145 0 1328 0
[pid=15142] vsize: 5892
Current children cumulated CPU time (s) 209.94
Current children cumulated vsize (Kb) 8016

[startup+220.025 s]
Raw data (loadavg): 0.99 0.93 0.91 2/58 15150
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1410 0 0 0 21985 7 0 0 25 0 1 0 1842307297 6066176 1359 4294967295 134512640 135094434 3221224448 3221223120 134556450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1481 1359 145 145 0 1336 0
[pid=15142] vsize: 5924
Current children cumulated CPU time (s) 219.94
Current children cumulated vsize (Kb) 8048

[startup+230.026 s]
Raw data (loadavg): 0.99 0.94 0.91 2/58 15150
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1412 0 0 0 22985 7 0 0 25 0 1 0 1842307297 6066176 1361 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1481 1361 145 145 0 1336 0
[pid=15142] vsize: 5924
Current children cumulated CPU time (s) 229.94
Current children cumulated vsize (Kb) 8048

[startup+240.027 s]
Raw data (loadavg): 0.99 0.94 0.91 2/58 15150
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1412 0 0 0 23985 7 0 0 25 0 1 0 1842307297 6066176 1361 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1481 1361 145 145 0 1336 0
[pid=15142] vsize: 5924
Current children cumulated CPU time (s) 239.94
Current children cumulated vsize (Kb) 8048

[startup+250.028 s]
Raw data (loadavg): 0.99 0.94 0.91 2/58 15150
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1417 0 0 0 24986 7 0 0 25 0 1 0 1842307297 6098944 1366 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1489 1366 145 145 0 1344 0
[pid=15142] vsize: 5956
Current children cumulated CPU time (s) 249.95
Current children cumulated vsize (Kb) 8080

[startup+260.029 s]
Raw data (loadavg): 0.99 0.94 0.91 2/58 15152
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1417 0 0 0 25986 7 0 0 25 0 1 0 1842307297 6098944 1366 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1489 1366 145 145 0 1344 0
[pid=15142] vsize: 5956
Current children cumulated CPU time (s) 259.95
Current children cumulated vsize (Kb) 8080

[startup+270.03 s]
Raw data (loadavg): 0.99 0.94 0.91 2/58 15152
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1439 0 0 0 26986 7 0 0 25 0 1 0 1842307297 6262784 1388 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1529 1388 145 145 0 1384 0
[pid=15142] vsize: 6116
Current children cumulated CPU time (s) 269.95
Current children cumulated vsize (Kb) 8240

[startup+280.03 s]
Raw data (loadavg): 0.99 0.94 0.91 2/58 15152
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1441 0 0 0 27986 7 0 0 25 0 1 0 1842307297 6262784 1390 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1529 1390 145 145 0 1384 0
[pid=15142] vsize: 6116
Current children cumulated CPU time (s) 279.95
Current children cumulated vsize (Kb) 8240

[startup+290.032 s]
Raw data (loadavg): 0.99 0.94 0.91 2/58 15152
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1441 0 0 0 28986 7 0 0 25 0 1 0 1842307297 6262784 1390 4294967295 134512640 135094434 3221224448 3221223104 134558176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1529 1390 145 145 0 1384 0
[pid=15142] vsize: 6116
Current children cumulated CPU time (s) 289.95
Current children cumulated vsize (Kb) 8240

[startup+300.033 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 15152
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1441 0 0 0 29987 7 0 0 25 0 1 0 1842307297 6262784 1390 4294967295 134512640 135094434 3221224448 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1529 1390 145 145 0 1384 0
[pid=15142] vsize: 6116
Current children cumulated CPU time (s) 299.96
Current children cumulated vsize (Kb) 8240

[startup+310.034 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 15152
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1441 0 0 0 30987 7 0 0 25 0 1 0 1842307297 6262784 1390 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1529 1390 145 145 0 1384 0
[pid=15142] vsize: 6116
Current children cumulated CPU time (s) 309.96
Current children cumulated vsize (Kb) 8240

[startup+320.035 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 15154
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1447 0 0 0 31987 8 0 0 25 0 1 0 1842307297 6295552 1396 4294967295 134512640 135094434 3221224448 3221223104 134556038 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1537 1396 145 145 0 1392 0
[pid=15142] vsize: 6148
Current children cumulated CPU time (s) 319.97
Current children cumulated vsize (Kb) 8272

[startup+330.034 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 15154
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1448 0 0 0 32987 8 0 0 25 0 1 0 1842307297 6295552 1397 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1537 1397 145 145 0 1392 0
[pid=15142] vsize: 6148
Current children cumulated CPU time (s) 329.97
Current children cumulated vsize (Kb) 8272

[startup+340.035 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 15154
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1454 0 0 0 33988 8 0 0 25 0 1 0 1842307297 6328320 1403 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1545 1403 145 145 0 1400 0
[pid=15142] vsize: 6180
Current children cumulated CPU time (s) 339.98
Current children cumulated vsize (Kb) 8304

[startup+350.036 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 15154
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1454 0 0 0 34988 8 0 0 25 0 1 0 1842307297 6328320 1403 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1545 1403 145 145 0 1400 0
[pid=15142] vsize: 6180
Current children cumulated CPU time (s) 349.98
Current children cumulated vsize (Kb) 8304

[startup+360.037 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 15154
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1460 0 0 0 35988 8 0 0 25 0 1 0 1842307297 6361088 1409 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1553 1409 145 145 0 1408 0
[pid=15142] vsize: 6212
Current children cumulated CPU time (s) 359.98
Current children cumulated vsize (Kb) 8336

[startup+370.038 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 15154
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1460 0 0 0 36988 8 0 0 25 0 1 0 1842307297 6361088 1409 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1553 1409 145 145 0 1408 0
[pid=15142] vsize: 6212
Current children cumulated CPU time (s) 369.98
Current children cumulated vsize (Kb) 8336

[startup+380.039 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 15156
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1460 0 0 0 37989 8 0 0 25 0 1 0 1842307297 6361088 1409 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1553 1409 145 145 0 1408 0
[pid=15142] vsize: 6212
Current children cumulated CPU time (s) 379.99
Current children cumulated vsize (Kb) 8336

[startup+390.04 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 15156
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1460 0 0 0 38988 8 0 0 25 0 1 0 1842307297 6361088 1409 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1553 1409 145 145 0 1408 0
[pid=15142] vsize: 6212
Current children cumulated CPU time (s) 389.98
Current children cumulated vsize (Kb) 8336

[startup+400.041 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 15156
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1486 0 0 0 39988 8 0 0 25 0 1 0 1842307297 6459392 1435 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1577 1435 145 145 0 1432 0
[pid=15142] vsize: 6308
Current children cumulated CPU time (s) 399.98
Current children cumulated vsize (Kb) 8432

[startup+410.043 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 15156
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1498 0 0 0 40988 8 0 0 25 0 1 0 1842307297 6516736 1447 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1591 1447 145 145 0 1446 0
[pid=15142] vsize: 6364
Current children cumulated CPU time (s) 409.98
Current children cumulated vsize (Kb) 8488

[startup+420.044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 15156
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1502 0 0 0 41988 8 0 0 25 0 1 0 1842307297 6516736 1451 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1591 1451 145 145 0 1446 0
[pid=15142] vsize: 6364
Current children cumulated CPU time (s) 419.98
Current children cumulated vsize (Kb) 8488

[startup+430.044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 15156
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1502 0 0 0 42988 8 0 0 25 0 1 0 1842307297 6516736 1451 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1591 1451 145 145 0 1446 0
[pid=15142] vsize: 6364
Current children cumulated CPU time (s) 429.98
Current children cumulated vsize (Kb) 8488

[startup+440.045 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 15158
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1503 0 0 0 43989 8 0 0 25 0 1 0 1842307297 6516736 1452 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1591 1452 145 145 0 1446 0
[pid=15142] vsize: 6364
Current children cumulated CPU time (s) 439.99
Current children cumulated vsize (Kb) 8488

[startup+450.046 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 15158
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1503 0 0 0 44989 8 0 0 25 0 1 0 1842307297 6516736 1452 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1591 1452 145 145 0 1446 0
[pid=15142] vsize: 6364
Current children cumulated CPU time (s) 449.99
Current children cumulated vsize (Kb) 8488

[startup+460.048 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 15158
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1510 0 0 0 45989 8 0 0 25 0 1 0 1842307297 6549504 1459 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1599 1459 145 145 0 1454 0
[pid=15142] vsize: 6396
Current children cumulated CPU time (s) 459.99
Current children cumulated vsize (Kb) 8520

[startup+470.048 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 15158
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1521 0 0 0 46989 8 0 0 25 0 1 0 1842307297 6647808 1470 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1623 1470 145 145 0 1478 0
[pid=15142] vsize: 6492
Current children cumulated CPU time (s) 469.99
Current children cumulated vsize (Kb) 8616

[startup+480.048 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 15158
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1525 0 0 0 47989 8 0 0 25 0 1 0 1842307297 6647808 1474 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1623 1474 145 145 0 1478 0
[pid=15142] vsize: 6492
Current children cumulated CPU time (s) 479.99
Current children cumulated vsize (Kb) 8616

[startup+490.049 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 15158
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1531 0 0 0 48990 9 0 0 25 0 1 0 1842307297 6680576 1480 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1631 1480 145 145 0 1486 0
[pid=15142] vsize: 6524
Current children cumulated CPU time (s) 490.01
Current children cumulated vsize (Kb) 8648

[startup+500.05 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 15160
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1539 0 0 0 49990 9 0 0 25 0 1 0 1842307297 6713344 1488 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1639 1488 145 145 0 1494 0
[pid=15142] vsize: 6556
Current children cumulated CPU time (s) 500.01
Current children cumulated vsize (Kb) 8680

[startup+510.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15160
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1542 0 0 0 50990 9 0 0 25 0 1 0 1842307297 6778880 1491 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1655 1491 145 145 0 1510 0
[pid=15142] vsize: 6620
Current children cumulated CPU time (s) 510.01
Current children cumulated vsize (Kb) 8744

[startup+520.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15160
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1542 0 0 0 51990 9 0 0 25 0 1 0 1842307297 6778880 1491 4294967295 134512640 135094434 3221224448 3221223104 134558164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1655 1491 145 145 0 1510 0
[pid=15142] vsize: 6620
Current children cumulated CPU time (s) 520.01
Current children cumulated vsize (Kb) 8744

[startup+530.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15160
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1542 0 0 0 52990 9 0 0 25 0 1 0 1842307297 6778880 1491 4294967295 134512640 135094434 3221224448 3221223040 134551876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1655 1491 145 145 0 1510 0
[pid=15142] vsize: 6620
Current children cumulated CPU time (s) 530.01
Current children cumulated vsize (Kb) 8744

[startup+540.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15160
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1544 0 0 0 53990 9 0 0 25 0 1 0 1842307297 6778880 1493 4294967295 134512640 135094434 3221224448 3221223120 134555437 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1655 1493 145 145 0 1510 0
[pid=15142] vsize: 6620
Current children cumulated CPU time (s) 540.01
Current children cumulated vsize (Kb) 8744

[startup+550.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15160
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1544 0 0 0 54991 9 0 0 25 0 1 0 1842307297 6778880 1493 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1655 1493 145 145 0 1510 0
[pid=15142] vsize: 6620
Current children cumulated CPU time (s) 550.02
Current children cumulated vsize (Kb) 8744

[startup+560.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15162
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1554 0 0 0 55991 9 0 0 25 0 1 0 1842307297 6791168 1503 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1658 1503 145 145 0 1513 0
[pid=15142] vsize: 6632
Current children cumulated CPU time (s) 560.02
Current children cumulated vsize (Kb) 8756

[startup+570.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15162
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1562 0 0 0 56991 9 0 0 25 0 1 0 1842307297 6828032 1511 4294967295 134512640 135094434 3221224448 3221223088 134562041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1667 1511 145 145 0 1522 0
[pid=15142] vsize: 6668
Current children cumulated CPU time (s) 570.02
Current children cumulated vsize (Kb) 8792

[startup+580.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15162
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1587 0 0 0 57990 9 0 0 25 0 1 0 1842307297 6914048 1536 4294967295 134512640 135094434 3221224448 3221223072 134562113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1688 1536 145 145 0 1543 0
[pid=15142] vsize: 6752
Current children cumulated CPU time (s) 580.01
Current children cumulated vsize (Kb) 8876

[startup+590.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15162
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1605 0 0 0 58991 9 0 0 25 0 1 0 1842307297 7016448 1554 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1713 1554 145 145 0 1568 0
[pid=15142] vsize: 6852
Current children cumulated CPU time (s) 590.02
Current children cumulated vsize (Kb) 8976

[startup+600.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15162
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1608 0 0 0 59991 9 0 0 25 0 1 0 1842307297 7016448 1557 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1713 1557 145 145 0 1568 0
[pid=15142] vsize: 6852
Current children cumulated CPU time (s) 600.02
Current children cumulated vsize (Kb) 8976

[startup+610.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15162
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1608 0 0 0 60991 9 0 0 25 0 1 0 1842307297 7016448 1557 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1713 1557 145 145 0 1568 0
[pid=15142] vsize: 6852
Current children cumulated CPU time (s) 610.02
Current children cumulated vsize (Kb) 8976

[startup+620.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15164
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1617 0 0 0 61991 9 0 0 25 0 1 0 1842307297 7081984 1566 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1729 1566 145 145 0 1584 0
[pid=15142] vsize: 6916
Current children cumulated CPU time (s) 620.02
Current children cumulated vsize (Kb) 9040

[startup+630.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15164
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1622 0 0 0 62992 9 0 0 25 0 1 0 1842307297 7114752 1571 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1737 1571 145 145 0 1592 0
[pid=15142] vsize: 6948
Current children cumulated CPU time (s) 630.03
Current children cumulated vsize (Kb) 9072

[startup+640.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15164
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1625 0 0 0 63992 9 0 0 25 0 1 0 1842307297 7114752 1574 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1737 1574 145 145 0 1592 0
[pid=15142] vsize: 6948
Current children cumulated CPU time (s) 640.03
Current children cumulated vsize (Kb) 9072

[startup+650.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15164
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1625 0 0 0 64992 9 0 0 25 0 1 0 1842307297 7114752 1574 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1737 1574 145 145 0 1592 0
[pid=15142] vsize: 6948
Current children cumulated CPU time (s) 650.03
Current children cumulated vsize (Kb) 9072

[startup+660.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15164
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1625 0 0 0 65992 9 0 0 25 0 1 0 1842307297 7114752 1574 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1737 1574 145 145 0 1592 0
[pid=15142] vsize: 6948
Current children cumulated CPU time (s) 660.03
Current children cumulated vsize (Kb) 9072

[startup+670.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15164
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1626 0 0 0 66993 9 0 0 25 0 1 0 1842307297 7114752 1575 4294967295 134512640 135094434 3221224448 3221223104 134558153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1737 1575 145 145 0 1592 0
[pid=15142] vsize: 6948
Current children cumulated CPU time (s) 670.04
Current children cumulated vsize (Kb) 9072

[startup+680.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15166
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1626 0 0 0 67993 9 0 0 25 0 1 0 1842307297 7114752 1575 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1737 1575 145 145 0 1592 0
[pid=15142] vsize: 6948
Current children cumulated CPU time (s) 680.04
Current children cumulated vsize (Kb) 9072

[startup+690.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15166
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1626 0 0 0 68993 9 0 0 25 0 1 0 1842307297 7114752 1575 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1737 1575 145 145 0 1592 0
[pid=15142] vsize: 6948
Current children cumulated CPU time (s) 690.04
Current children cumulated vsize (Kb) 9072

[startup+700.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15166
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1626 0 0 0 69993 9 0 0 25 0 1 0 1842307297 7114752 1575 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1737 1575 145 145 0 1592 0
[pid=15142] vsize: 6948
Current children cumulated CPU time (s) 700.04
Current children cumulated vsize (Kb) 9072

[startup+710.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15166
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1636 0 0 0 70994 9 0 0 25 0 1 0 1842307297 7180288 1585 4294967295 134512640 135094434 3221224448 3221223040 134556933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1753 1585 145 145 0 1608 0
[pid=15142] vsize: 7012
Current children cumulated CPU time (s) 710.05
Current children cumulated vsize (Kb) 9136

[startup+720.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15166
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1636 0 0 0 71994 9 0 0 25 0 1 0 1842307297 7180288 1585 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1753 1585 145 145 0 1608 0
[pid=15142] vsize: 7012
Current children cumulated CPU time (s) 720.05
Current children cumulated vsize (Kb) 9136

[startup+730.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15166
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1636 0 0 0 72994 9 0 0 25 0 1 0 1842307297 7180288 1585 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1753 1585 145 145 0 1608 0
[pid=15142] vsize: 7012
Current children cumulated CPU time (s) 730.05
Current children cumulated vsize (Kb) 9136

[startup+740.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15168
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1636 0 0 0 73994 9 0 0 25 0 1 0 1842307297 7180288 1585 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1753 1585 145 145 0 1608 0
[pid=15142] vsize: 7012
Current children cumulated CPU time (s) 740.05
Current children cumulated vsize (Kb) 9136

[startup+750.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15168
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1636 0 0 0 74995 9 0 0 25 0 1 0 1842307297 7180288 1585 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1753 1585 145 145 0 1608 0
[pid=15142] vsize: 7012
Current children cumulated CPU time (s) 750.06
Current children cumulated vsize (Kb) 9136

[startup+760.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15168
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1638 0 0 0 75995 9 0 0 25 0 1 0 1842307297 7180288 1587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1753 1587 145 145 0 1608 0
[pid=15142] vsize: 7012
Current children cumulated CPU time (s) 760.06
Current children cumulated vsize (Kb) 9136

[startup+770.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15168
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1639 0 0 0 76995 9 0 0 25 0 1 0 1842307297 7180288 1588 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1753 1588 145 145 0 1608 0
[pid=15142] vsize: 7012
Current children cumulated CPU time (s) 770.06
Current children cumulated vsize (Kb) 9136

[startup+780.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15168
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1639 0 0 0 77995 9 0 0 25 0 1 0 1842307297 7180288 1588 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1753 1588 145 145 0 1608 0
[pid=15142] vsize: 7012
Current children cumulated CPU time (s) 780.06
Current children cumulated vsize (Kb) 9136

[startup+790.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15168
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1639 0 0 0 78995 9 0 0 25 0 1 0 1842307297 7180288 1588 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1753 1588 145 145 0 1608 0
[pid=15142] vsize: 7012
Current children cumulated CPU time (s) 790.06
Current children cumulated vsize (Kb) 9136

[startup+800.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15170
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1639 0 0 0 79996 9 0 0 25 0 1 0 1842307297 7180288 1588 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1753 1588 145 145 0 1608 0
[pid=15142] vsize: 7012
Current children cumulated CPU time (s) 800.07
Current children cumulated vsize (Kb) 9136

[startup+810.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15170
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1639 0 0 0 80996 9 0 0 25 0 1 0 1842307297 7180288 1588 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1753 1588 145 145 0 1608 0
[pid=15142] vsize: 7012
Current children cumulated CPU time (s) 810.07
Current children cumulated vsize (Kb) 9136

[startup+820.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15170
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1639 0 0 0 81996 9 0 0 25 0 1 0 1842307297 7180288 1588 4294967295 134512640 135094434 3221224448 3221223072 134557705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1753 1588 145 145 0 1608 0
[pid=15142] vsize: 7012
Current children cumulated CPU time (s) 820.07
Current children cumulated vsize (Kb) 9136

[startup+830.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15170
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1639 0 0 0 82996 9 0 0 25 0 1 0 1842307297 7180288 1588 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1753 1588 145 145 0 1608 0
[pid=15142] vsize: 7012
Current children cumulated CPU time (s) 830.07
Current children cumulated vsize (Kb) 9136

[startup+840.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15170
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1639 0 0 0 83997 9 0 0 25 0 1 0 1842307297 7180288 1588 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1753 1588 145 145 0 1608 0
[pid=15142] vsize: 7012
Current children cumulated CPU time (s) 840.08
Current children cumulated vsize (Kb) 9136

[startup+850.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15170
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1646 0 0 0 84997 9 0 0 25 0 1 0 1842307297 7213056 1595 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1761 1595 145 145 0 1616 0
[pid=15142] vsize: 7044
Current children cumulated CPU time (s) 850.08
Current children cumulated vsize (Kb) 9168

[startup+860.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15172
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1652 0 0 0 85997 9 0 0 25 0 1 0 1842307297 7245824 1601 4294967295 134512640 135094434 3221224448 3221223120 134556291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1769 1601 145 145 0 1624 0
[pid=15142] vsize: 7076
Current children cumulated CPU time (s) 860.08
Current children cumulated vsize (Kb) 9200

[startup+870.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15172
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1653 0 0 0 86997 9 0 0 25 0 1 0 1842307297 7245824 1602 4294967295 134512640 135094434 3221224448 3221223120 134555274 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1769 1602 145 145 0 1624 0
[pid=15142] vsize: 7076
Current children cumulated CPU time (s) 870.08
Current children cumulated vsize (Kb) 9200

[startup+880.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15172
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1653 0 0 0 87998 9 0 0 25 0 1 0 1842307297 7245824 1602 4294967295 134512640 135094434 3221224448 3221223120 134555940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1769 1602 145 145 0 1624 0
[pid=15142] vsize: 7076
Current children cumulated CPU time (s) 880.09
Current children cumulated vsize (Kb) 9200

[startup+890.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15172
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1664 0 0 0 88997 10 0 0 25 0 1 0 1842307297 7311360 1613 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15142/statm): 1785 1613 145 145 0 1640 0
[pid=15142] vsize: 7140
Current children cumulated CPU time (s) 890.09
Current children cumulated vsize (Kb) 9264

[startup+900.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15172
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1726 0 0 0 89996 10 0 0 25 0 1 0 1842307297 7548928 1675 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1843 1675 145 145 0 1698 0
[pid=15142] vsize: 7372
Current children cumulated CPU time (s) 900.08
Current children cumulated vsize (Kb) 9496

[startup+910.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15172
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1726 0 0 0 90996 10 0 0 25 0 1 0 1842307297 7548928 1675 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1843 1675 145 145 0 1698 0
[pid=15142] vsize: 7372
Current children cumulated CPU time (s) 910.08
Current children cumulated vsize (Kb) 9496

[startup+920.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15174
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1733 0 0 0 91996 10 0 0 25 0 1 0 1842307297 7577600 1682 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1850 1682 145 145 0 1705 0
[pid=15142] vsize: 7400
Current children cumulated CPU time (s) 920.08
Current children cumulated vsize (Kb) 9524

[startup+930.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15174
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1734 0 0 0 92996 10 0 0 25 0 1 0 1842307297 7577600 1683 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1850 1683 145 145 0 1705 0
[pid=15142] vsize: 7400
Current children cumulated CPU time (s) 930.08
Current children cumulated vsize (Kb) 9524

[startup+940.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15174
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1744 0 0 0 93996 10 0 0 25 0 1 0 1842307297 7639040 1693 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1865 1693 145 145 0 1720 0
[pid=15142] vsize: 7460
Current children cumulated CPU time (s) 940.08
Current children cumulated vsize (Kb) 9584

[startup+950.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15174
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1744 0 0 0 94996 10 0 0 25 0 1 0 1842307297 7639040 1693 4294967295 134512640 135094434 3221224448 3221223088 134558264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1865 1693 145 145 0 1720 0
[pid=15142] vsize: 7460
Current children cumulated CPU time (s) 950.08
Current children cumulated vsize (Kb) 9584

[startup+960.097 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15174
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1758 0 0 0 95997 10 0 0 25 0 1 0 1842307297 7704576 1707 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1881 1707 145 145 0 1736 0
[pid=15142] vsize: 7524
Current children cumulated CPU time (s) 960.09
Current children cumulated vsize (Kb) 9648

[startup+970.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15174
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 96997 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0
[pid=15142] vsize: 7524
Current children cumulated CPU time (s) 970.1
Current children cumulated vsize (Kb) 9648

[startup+980.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15176
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 97997 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0
[pid=15142] vsize: 7524
Current children cumulated CPU time (s) 980.1
Current children cumulated vsize (Kb) 9648

[startup+990.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15176
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 98997 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0
[pid=15142] vsize: 7524
Current children cumulated CPU time (s) 990.1
Current children cumulated vsize (Kb) 9648

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15176
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 99997 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0
[pid=15142] vsize: 7524
Current children cumulated CPU time (s) 1000.1
Current children cumulated vsize (Kb) 9648

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15176
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 100998 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223072 134557705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0
[pid=15142] vsize: 7524
Current children cumulated CPU time (s) 1010.11
Current children cumulated vsize (Kb) 9648

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15176
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 101998 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223136 134554751 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0
[pid=15142] vsize: 7524
Current children cumulated CPU time (s) 1020.11
Current children cumulated vsize (Kb) 9648

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15176
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 102998 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0
[pid=15142] vsize: 7524
Current children cumulated CPU time (s) 1030.11
Current children cumulated vsize (Kb) 9648

[startup+1040.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15178
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 103998 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0
[pid=15142] vsize: 7524
Current children cumulated CPU time (s) 1040.11
Current children cumulated vsize (Kb) 9648

[startup+1050.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15178
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 104999 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0
[pid=15142] vsize: 7524
Current children cumulated CPU time (s) 1050.12
Current children cumulated vsize (Kb) 9648

[startup+1060.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15178
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 105999 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0
[pid=15142] vsize: 7524
Current children cumulated CPU time (s) 1060.12
Current children cumulated vsize (Kb) 9648

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15178
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 106999 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0
[pid=15142] vsize: 7524
Current children cumulated CPU time (s) 1070.12
Current children cumulated vsize (Kb) 9648

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15178
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1759 0 0 0 108000 11 0 0 25 0 1 0 1842307297 7704576 1708 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1881 1708 145 145 0 1736 0
[pid=15142] vsize: 7524
Current children cumulated CPU time (s) 1080.13
Current children cumulated vsize (Kb) 9648

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15178
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1761 0 0 0 109000 11 0 0 25 0 1 0 1842307297 7704576 1710 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1881 1710 145 145 0 1736 0
[pid=15142] vsize: 7524
Current children cumulated CPU time (s) 1090.13
Current children cumulated vsize (Kb) 9648

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15180
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1772 0 0 0 110000 11 0 0 25 0 1 0 1842307297 7770112 1721 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1897 1721 145 145 0 1752 0
[pid=15142] vsize: 7588
Current children cumulated CPU time (s) 1100.13
Current children cumulated vsize (Kb) 9712

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15180
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1772 0 0 0 111000 11 0 0 25 0 1 0 1842307297 7770112 1721 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1897 1721 145 145 0 1752 0
[pid=15142] vsize: 7588
Current children cumulated CPU time (s) 1110.13
Current children cumulated vsize (Kb) 9712

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15180
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1772 0 0 0 112000 11 0 0 25 0 1 0 1842307297 7770112 1721 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1897 1721 145 145 0 1752 0
[pid=15142] vsize: 7588
Current children cumulated CPU time (s) 1120.13
Current children cumulated vsize (Kb) 9712

[startup+1130.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15180
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1772 0 0 0 113001 11 0 0 25 0 1 0 1842307297 7770112 1721 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1897 1721 145 145 0 1752 0
[pid=15142] vsize: 7588
Current children cumulated CPU time (s) 1130.14
Current children cumulated vsize (Kb) 9712

[startup+1140.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15180
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1772 0 0 0 114001 11 0 0 25 0 1 0 1842307297 7770112 1721 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1897 1721 145 145 0 1752 0
[pid=15142] vsize: 7588
Current children cumulated CPU time (s) 1140.14
Current children cumulated vsize (Kb) 9712

[startup+1150.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15180
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1772 0 0 0 115001 11 0 0 25 0 1 0 1842307297 7770112 1721 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1897 1721 145 145 0 1752 0
[pid=15142] vsize: 7588
Current children cumulated CPU time (s) 1150.14
Current children cumulated vsize (Kb) 9712

[startup+1160.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15182
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1772 0 0 0 116001 11 0 0 25 0 1 0 1842307297 7770112 1721 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1897 1721 145 145 0 1752 0
[pid=15142] vsize: 7588
Current children cumulated CPU time (s) 1160.14
Current children cumulated vsize (Kb) 9712

[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15182
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1782 0 0 0 117002 11 0 0 25 0 1 0 1842307297 7835648 1731 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1913 1731 145 145 0 1768 0
[pid=15142] vsize: 7652
Current children cumulated CPU time (s) 1170.15
Current children cumulated vsize (Kb) 9776

[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15182
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1782 0 0 0 118002 11 0 0 25 0 1 0 1842307297 7835648 1731 4294967295 134512640 135094434 3221224448 3221223072 134562149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1913 1731 145 145 0 1768 0
[pid=15142] vsize: 7652
Current children cumulated CPU time (s) 1180.15
Current children cumulated vsize (Kb) 9776

[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15182
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1782 0 0 0 119002 11 0 0 25 0 1 0 1842307297 7835648 1731 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1913 1731 145 145 0 1768 0
[pid=15142] vsize: 7652
Current children cumulated CPU time (s) 1190.15
Current children cumulated vsize (Kb) 9776

[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15182
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1782 0 0 0 120003 11 0 0 25 0 1 0 1842307297 7835648 1731 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1913 1731 145 145 0 1768 0
[pid=15142] vsize: 7652
Current children cumulated CPU time (s) 1200.16
Current children cumulated vsize (Kb) 9776



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 15182
Raw data (/proc/15138/stat): 15138 (minisat+_script) S 15137 15138 9102 0 -1 0 288 239 0 0 0 1 0 1 21 0 1 0 1842307292 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15138/statm): 531 226 485 147 0 384 0
[pid=15138] vsize: 2124
Raw data (/proc/15142/stat): 15142 (minisat+_64-bit) R 15138 15138 9102 0 -1 0 1782 0 0 0 120003 11 0 0 25 0 1 0 1842307297 7835648 1731 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15142/statm): 1913 1731 145 145 0 1768 0
[pid=15142] vsize: 7652
Current children cumulated CPU time (s) 1200.16
Current children cumulated vsize (Kb) 9776

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

Child status: 0
Real time (s): 1200.13
CPU time (s): 1200.15
CPU user time (s): 1200.03
CPU system time (s): 0.119981
CPU usage (%): 100.002
Max. virtual memory (cumulated for all children) (Kb): 9776

Verifier Data

ERROR: no interpretation found !