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-5.opb
MD5SUM9b244c88702eddacf15d45f12fda5eb0
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 constraints13501
Number of constraints which are clauses13501
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 1543

Launcher Data

LAUNCH ON wulflinc27 THE 2005-09-18 15:33:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2542 boxname=wulflinc27 idbench=198 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9b244c88702eddacf15d45f12fda5eb0  /oldhome/oroussel/tmp/wulflinc27/normalized-par32-5.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-par32-5.opb
IDLAUNCH: 2542
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        915800 kB
Buffers:         35320 kB
Cached:          51364 kB
SwapCached:        764 kB
Active:          63520 kB
Inactive:        25784 kB
HighTotal:      131008 kB
HighFree:        77084 kB
LowTotal:       903652 kB
LowFree:        838716 kB
SwapTotal:     2097892 kB
SwapFree:      2096616 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5724 kB
Slab:            24148 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 15:53:54 (client local time) WITH STATUS 0 IN 1200.16 SECONDS
stats: 2542 7 1200.16 0

Solver Data

c Parsing PB file...
c Converting 13094 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
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 |    9827    24632 |    3275       0        0     nan |  0.000 % |
c |       101 |    9827    24632 |    3602     101     1262    12.5 | 24.906 % |
c |       251 |    9827    24632 |    3962     251     4441    17.7 | 24.906 % |
c |       477 |    9827    24632 |    4359     477     7614    16.0 | 24.906 % |
c |       815 |    9827    24632 |    4794     815    20329    24.9 | 24.906 % |
c |      1322 |    9827    24632 |    5274    1322    40427    30.6 | 24.906 % |
c |      2082 |    9827    24632 |    5801    2082    63698    30.6 | 24.906 % |
c |      3222 |    9827    24632 |    6382    3222    97933    30.4 | 24.906 % |
c |      4930 |    9817    24610 |    7020    4929   145871    29.6 | 24.969 % |
c |      7493 |    9817    24610 |    7722    7492   218722    29.2 | 24.969 % |
c |     11338 |    9817    24610 |    8494    6606   175949    26.6 | 24.969 % |
c |     17105 |    9817    24610 |    9343    7226   216638    30.0 | 24.969 % |
c |     25755 |    9817    24610 |   10278   10380   268045    25.8 | 24.969 % |
c |     38731 |    9817    24610 |   11306   11401   279773    24.5 | 24.969 % |
c |     58192 |    9817    24610 |   12436   11386   276094    24.2 | 24.969 % |
c |     87384 |    9817    24610 |   13680   12380   296703    24.0 | 24.969 % |
c |    131175 |    9817    24610 |   15048   10106   229761    22.7 | 24.969 % |
c |    196859 |    9817    24610 |   16553    8709   192780    22.1 | 24.969 % |
c |    295386 |    9817    24610 |   18208   16160   368525    22.8 | 24.969 % |
c |    443175 |    9817    24610 |   20029   14820   349214    23.6 | 24.969 % |

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/3166/stat): 3166 (minisat+_script) R 3165 3166 28974 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1842353448 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/3166/statm): 174 3 169 147 0 27 0
[pid=3166] 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=3167
New process pid=3168
New process pid=3169
execve syscall for /bin/sed executable
One traced child (pid=3168) 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=3169) exited with status: 0
One traced child (pid=3167) exited with status: 0
New process pid=3170
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-par32-5.opb

[startup+10.0044 s]
Raw data (loadavg): 0.93 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1321 0 0 0 986 4 0 0 25 0 1 0 1842353453 5627904 1270 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1374 1270 145 145 0 1229 0
[pid=3170] vsize: 5496
Current children cumulated CPU time (s) 9.9
Current children cumulated vsize (Kb) 7620

[startup+20.0053 s]
Raw data (loadavg): 0.94 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1324 0 0 0 1986 4 0 0 25 0 1 0 1842353453 5627904 1273 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3170/statm): 1374 1273 145 145 0 1229 0
[pid=3170] vsize: 5496
Current children cumulated CPU time (s) 19.9
Current children cumulated vsize (Kb) 7620

[startup+30.0061 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1324 0 0 0 2985 4 0 0 25 0 1 0 1842353453 5627904 1273 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1374 1273 145 145 0 1229 0
[pid=3170] vsize: 5496
Current children cumulated CPU time (s) 29.89
Current children cumulated vsize (Kb) 7620

[startup+40.0069 s]
Raw data (loadavg): 0.96 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1324 0 0 0 3985 4 0 0 25 0 1 0 1842353453 5627904 1273 4294967295 134512640 135094434 3221224448 3221223104 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1374 1273 145 145 0 1229 0
[pid=3170] vsize: 5496
Current children cumulated CPU time (s) 39.89
Current children cumulated vsize (Kb) 7620

[startup+50.0077 s]
Raw data (loadavg): 0.96 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1324 0 0 0 4985 5 0 0 25 0 1 0 1842353453 5627904 1273 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1374 1273 145 145 0 1229 0
[pid=3170] vsize: 5496
Current children cumulated CPU time (s) 49.9
Current children cumulated vsize (Kb) 7620

[startup+60.0085 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1324 0 0 0 5985 5 0 0 25 0 1 0 1842353453 5627904 1273 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1374 1273 145 145 0 1229 0
[pid=3170] vsize: 5496
Current children cumulated CPU time (s) 59.9
Current children cumulated vsize (Kb) 7620

[startup+70.0093 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1324 0 0 0 6985 5 0 0 25 0 1 0 1842353453 5627904 1273 4294967295 134512640 135094434 3221224448 3221222912 134781535 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1374 1273 145 145 0 1229 0
[pid=3170] vsize: 5496
Current children cumulated CPU time (s) 69.9
Current children cumulated vsize (Kb) 7620

[startup+80.0101 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1324 0 0 0 7985 5 0 0 25 0 1 0 1842353453 5627904 1273 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1374 1273 145 145 0 1229 0
[pid=3170] vsize: 5496
Current children cumulated CPU time (s) 79.9
Current children cumulated vsize (Kb) 7620

[startup+90.011 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1324 0 0 0 8986 5 0 0 25 0 1 0 1842353453 5627904 1273 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1374 1273 145 145 0 1229 0
[pid=3170] vsize: 5496
Current children cumulated CPU time (s) 89.91
Current children cumulated vsize (Kb) 7620

[startup+100.012 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1324 0 0 0 9986 5 0 0 25 0 1 0 1842353453 5627904 1273 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1374 1273 145 145 0 1229 0
[pid=3170] vsize: 5496
Current children cumulated CPU time (s) 99.91
Current children cumulated vsize (Kb) 7620

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1324 0 0 0 10986 5 0 0 25 0 1 0 1842353453 5627904 1273 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1374 1273 145 145 0 1229 0
[pid=3170] vsize: 5496
Current children cumulated CPU time (s) 109.91
Current children cumulated vsize (Kb) 7620

[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1324 0 0 0 11986 5 0 0 25 0 1 0 1842353453 5627904 1273 4294967295 134512640 135094434 3221224448 3221223104 134558398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1374 1273 145 145 0 1229 0
[pid=3170] vsize: 5496
Current children cumulated CPU time (s) 119.91
Current children cumulated vsize (Kb) 7620

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1324 0 0 0 12986 5 0 0 25 0 1 0 1842353453 5627904 1273 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1374 1273 145 145 0 1229 0
[pid=3170] vsize: 5496
Current children cumulated CPU time (s) 129.91
Current children cumulated vsize (Kb) 7620

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1324 0 0 0 13986 6 0 0 25 0 1 0 1842353453 5627904 1273 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1374 1273 145 145 0 1229 0
[pid=3170] vsize: 5496
Current children cumulated CPU time (s) 139.92
Current children cumulated vsize (Kb) 7620

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1329 0 0 0 14987 6 0 0 25 0 1 0 1842353453 5660672 1278 4294967295 134512640 135094434 3221224448 3221223120 134556285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1382 1278 145 145 0 1237 0
[pid=3170] vsize: 5528
Current children cumulated CPU time (s) 149.93
Current children cumulated vsize (Kb) 7652

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1335 0 0 0 15987 6 0 0 25 0 1 0 1842353453 5693440 1284 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1390 1284 145 145 0 1245 0
[pid=3170] vsize: 5560
Current children cumulated CPU time (s) 159.93
Current children cumulated vsize (Kb) 7684

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1352 0 0 0 16986 6 0 0 25 0 1 0 1842353453 5763072 1301 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1407 1301 145 145 0 1262 0
[pid=3170] vsize: 5628
Current children cumulated CPU time (s) 169.92
Current children cumulated vsize (Kb) 7752

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1357 0 0 0 17986 6 0 0 25 0 1 0 1842353453 5795840 1306 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1415 1306 145 145 0 1270 0
[pid=3170] vsize: 5660
Current children cumulated CPU time (s) 179.92
Current children cumulated vsize (Kb) 7784

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1360 0 0 0 18986 6 0 0 25 0 1 0 1842353453 5808128 1309 4294967295 134512640 135094434 3221224448 3221223060 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1418 1309 145 145 0 1273 0
[pid=3170] vsize: 5672
Current children cumulated CPU time (s) 189.92
Current children cumulated vsize (Kb) 7796

[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1361 0 0 0 19986 6 0 0 25 0 1 0 1842353453 5812224 1310 4294967295 134512640 135094434 3221224448 3221223040 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1419 1310 145 145 0 1274 0
[pid=3170] vsize: 5676
Current children cumulated CPU time (s) 199.92
Current children cumulated vsize (Kb) 7800

[startup+210.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1368 0 0 0 20986 6 0 0 25 0 1 0 1842353453 5844992 1317 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1427 1317 145 145 0 1282 0
[pid=3170] vsize: 5708
Current children cumulated CPU time (s) 209.92
Current children cumulated vsize (Kb) 7832

[startup+220.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1368 0 0 0 21986 6 0 0 25 0 1 0 1842353453 5844992 1317 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1427 1317 145 145 0 1282 0
[pid=3170] vsize: 5708
Current children cumulated CPU time (s) 219.92
Current children cumulated vsize (Kb) 7832

[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1368 0 0 0 22987 6 0 0 25 0 1 0 1842353453 5844992 1317 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1427 1317 145 145 0 1282 0
[pid=3170] vsize: 5708
Current children cumulated CPU time (s) 229.93
Current children cumulated vsize (Kb) 7832

[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1375 0 0 0 23987 7 0 0 25 0 1 0 1842353453 5877760 1324 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1435 1324 145 145 0 1290 0
[pid=3170] vsize: 5740
Current children cumulated CPU time (s) 239.94
Current children cumulated vsize (Kb) 7864

[startup+250.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1376 0 0 0 24987 7 0 0 25 0 1 0 1842353453 5877760 1325 4294967295 134512640 135094434 3221224448 3221223104 134558298 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1435 1325 145 145 0 1290 0
[pid=3170] vsize: 5740
Current children cumulated CPU time (s) 249.94
Current children cumulated vsize (Kb) 7864

[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1401 0 0 0 25987 7 0 0 25 0 1 0 1842353453 5980160 1350 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1460 1350 145 145 0 1315 0
[pid=3170] vsize: 5840
Current children cumulated CPU time (s) 259.94
Current children cumulated vsize (Kb) 7964

[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1428 0 0 0 26987 7 0 0 25 0 1 0 1842353453 6172672 1377 4294967295 134512640 135094434 3221224448 3221223072 134562149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3170/statm): 1507 1377 145 145 0 1362 0
[pid=3170] vsize: 6028
Current children cumulated CPU time (s) 269.94
Current children cumulated vsize (Kb) 8152

[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1429 0 0 0 27986 8 0 0 25 0 1 0 1842353453 6172672 1378 4294967295 134512640 135094434 3221224448 3221223016 134782985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1507 1378 145 145 0 1362 0
[pid=3170] vsize: 6028
Current children cumulated CPU time (s) 279.94
Current children cumulated vsize (Kb) 8152

[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1436 0 0 0 28986 8 0 0 25 0 1 0 1842353453 6205440 1385 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1515 1385 145 145 0 1370 0
[pid=3170] vsize: 6060
Current children cumulated CPU time (s) 289.94
Current children cumulated vsize (Kb) 8184

[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1437 0 0 0 29986 8 0 0 25 0 1 0 1842353453 6205440 1386 4294967295 134512640 135094434 3221224448 3221223104 134557987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1515 1386 145 145 0 1370 0
[pid=3170] vsize: 6060
Current children cumulated CPU time (s) 299.94
Current children cumulated vsize (Kb) 8184

[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1448 0 0 0 30987 8 0 0 25 0 1 0 1842353453 6254592 1397 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1527 1397 145 145 0 1382 0
[pid=3170] vsize: 6108
Current children cumulated CPU time (s) 309.95
Current children cumulated vsize (Kb) 8232

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1448 0 0 0 31987 8 0 0 25 0 1 0 1842353453 6254592 1397 4294967295 134512640 135094434 3221224448 3221223104 134557818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1527 1397 145 145 0 1382 0
[pid=3170] vsize: 6108
Current children cumulated CPU time (s) 319.95
Current children cumulated vsize (Kb) 8232

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1477 0 0 0 32986 8 0 0 25 0 1 0 1842353453 6385664 1426 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1559 1426 145 145 0 1414 0
[pid=3170] vsize: 6236
Current children cumulated CPU time (s) 329.94
Current children cumulated vsize (Kb) 8360

[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1484 0 0 0 33987 8 0 0 25 0 1 0 1842353453 6434816 1433 4294967295 134512640 135094434 3221224448 3221223104 134558147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1571 1433 145 145 0 1426 0
[pid=3170] vsize: 6284
Current children cumulated CPU time (s) 339.95
Current children cumulated vsize (Kb) 8408

[startup+350.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1489 0 0 0 34987 8 0 0 25 0 1 0 1842353453 6443008 1438 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1573 1438 145 145 0 1428 0
[pid=3170] vsize: 6292
Current children cumulated CPU time (s) 349.95
Current children cumulated vsize (Kb) 8416

[startup+360.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1489 0 0 0 35987 8 0 0 25 0 1 0 1842353453 6443008 1438 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1573 1438 145 145 0 1428 0
[pid=3170] vsize: 6292
Current children cumulated CPU time (s) 359.95
Current children cumulated vsize (Kb) 8416

[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1497 0 0 0 36987 9 0 0 25 0 1 0 1842353453 6492160 1446 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1585 1446 145 145 0 1440 0
[pid=3170] vsize: 6340
Current children cumulated CPU time (s) 369.96
Current children cumulated vsize (Kb) 8464

[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1500 0 0 0 37987 9 0 0 25 0 1 0 1842353453 6524928 1449 4294967295 134512640 135094434 3221224448 3221223104 134558238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3170/statm): 1593 1449 145 145 0 1448 0
[pid=3170] vsize: 6372
Current children cumulated CPU time (s) 379.96
Current children cumulated vsize (Kb) 8496

[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1500 0 0 0 38987 9 0 0 25 0 1 0 1842353453 6524928 1449 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1593 1449 145 145 0 1448 0
[pid=3170] vsize: 6372
Current children cumulated CPU time (s) 389.96
Current children cumulated vsize (Kb) 8496

[startup+400.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1532 0 0 0 39986 9 0 0 25 0 1 0 1842353453 6651904 1481 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1624 1481 145 145 0 1479 0
[pid=3170] vsize: 6496
Current children cumulated CPU time (s) 399.95
Current children cumulated vsize (Kb) 8620

[startup+410.036 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1532 0 0 0 40987 9 0 0 25 0 1 0 1842353453 6651904 1481 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1624 1481 145 145 0 1479 0
[pid=3170] vsize: 6496
Current children cumulated CPU time (s) 409.96
Current children cumulated vsize (Kb) 8620

[startup+420.037 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1541 0 0 0 41987 9 0 0 25 0 1 0 1842353453 6692864 1490 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1634 1490 145 145 0 1489 0
[pid=3170] vsize: 6536
Current children cumulated CPU time (s) 419.96
Current children cumulated vsize (Kb) 8660

[startup+430.038 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1541 0 0 0 42987 9 0 0 25 0 1 0 1842353453 6692864 1490 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1634 1490 145 145 0 1489 0
[pid=3170] vsize: 6536
Current children cumulated CPU time (s) 429.96
Current children cumulated vsize (Kb) 8660

[startup+440.039 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1541 0 0 0 43987 9 0 0 25 0 1 0 1842353453 6692864 1490 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1634 1490 145 145 0 1489 0
[pid=3170] vsize: 6536
Current children cumulated CPU time (s) 439.96
Current children cumulated vsize (Kb) 8660

[startup+450.039 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1547 0 0 0 44987 10 0 0 25 0 1 0 1842353453 6717440 1496 4294967295 134512640 135094434 3221224448 3221223104 134556043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1640 1496 145 145 0 1495 0
[pid=3170] vsize: 6560
Current children cumulated CPU time (s) 449.97
Current children cumulated vsize (Kb) 8684

[startup+460.041 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1547 0 0 0 45987 10 0 0 25 0 1 0 1842353453 6717440 1496 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1640 1496 145 145 0 1495 0
[pid=3170] vsize: 6560
Current children cumulated CPU time (s) 459.97
Current children cumulated vsize (Kb) 8684

[startup+470.042 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1548 0 0 0 46988 10 0 0 25 0 1 0 1842353453 6717440 1497 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1640 1497 145 145 0 1495 0
[pid=3170] vsize: 6560
Current children cumulated CPU time (s) 469.98
Current children cumulated vsize (Kb) 8684

[startup+480.043 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1548 0 0 0 47988 10 0 0 25 0 1 0 1842353453 6717440 1497 4294967295 134512640 135094434 3221224448 3221223120 134556543 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1640 1497 145 145 0 1495 0
[pid=3170] vsize: 6560
Current children cumulated CPU time (s) 479.98
Current children cumulated vsize (Kb) 8684

[startup+490.044 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1548 0 0 0 48988 10 0 0 25 0 1 0 1842353453 6717440 1497 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1640 1497 145 145 0 1495 0
[pid=3170] vsize: 6560
Current children cumulated CPU time (s) 489.98
Current children cumulated vsize (Kb) 8684

[startup+500.044 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1548 0 0 0 49988 10 0 0 25 0 1 0 1842353453 6717440 1497 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1640 1497 145 145 0 1495 0
[pid=3170] vsize: 6560
Current children cumulated CPU time (s) 499.98
Current children cumulated vsize (Kb) 8684

[startup+510.044 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1548 0 0 0 50989 10 0 0 25 0 1 0 1842353453 6717440 1497 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1640 1497 145 145 0 1495 0
[pid=3170] vsize: 6560
Current children cumulated CPU time (s) 509.99
Current children cumulated vsize (Kb) 8684

[startup+520.045 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1554 0 0 0 51989 10 0 0 25 0 1 0 1842353453 6750208 1503 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1648 1503 145 145 0 1503 0
[pid=3170] vsize: 6592
Current children cumulated CPU time (s) 519.99
Current children cumulated vsize (Kb) 8716

[startup+530.046 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1554 0 0 0 52989 10 0 0 25 0 1 0 1842353453 6750208 1503 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1648 1503 145 145 0 1503 0
[pid=3170] vsize: 6592
Current children cumulated CPU time (s) 529.99
Current children cumulated vsize (Kb) 8716

[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1556 0 0 0 53989 10 0 0 25 0 1 0 1842353453 6750208 1505 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1648 1505 145 145 0 1503 0
[pid=3170] vsize: 6592
Current children cumulated CPU time (s) 539.99
Current children cumulated vsize (Kb) 8716

[startup+550.048 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1556 0 0 0 54989 10 0 0 25 0 1 0 1842353453 6750208 1505 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1648 1505 145 145 0 1503 0
[pid=3170] vsize: 6592
Current children cumulated CPU time (s) 549.99
Current children cumulated vsize (Kb) 8716

[startup+560.049 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1556 0 0 0 55988 11 0 0 25 0 1 0 1842353453 6750208 1505 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1648 1505 145 145 0 1503 0
[pid=3170] vsize: 6592
Current children cumulated CPU time (s) 559.99
Current children cumulated vsize (Kb) 8716

[startup+570.05 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1557 0 0 0 56988 12 0 0 25 0 1 0 1842353453 6750208 1506 4294967295 134512640 135094434 3221224448 3221223040 134551469 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1648 1506 145 145 0 1503 0
[pid=3170] vsize: 6592
Current children cumulated CPU time (s) 570
Current children cumulated vsize (Kb) 8716

[startup+580.051 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1557 0 0 0 57988 12 0 0 25 0 1 0 1842353453 6750208 1506 4294967295 134512640 135094434 3221224448 3221223120 134555274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1648 1506 145 145 0 1503 0
[pid=3170] vsize: 6592
Current children cumulated CPU time (s) 580
Current children cumulated vsize (Kb) 8716

[startup+590.052 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1563 0 0 0 58988 12 0 0 25 0 1 0 1842353453 6774784 1512 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1654 1512 145 145 0 1509 0
[pid=3170] vsize: 6616
Current children cumulated CPU time (s) 590
Current children cumulated vsize (Kb) 8740

[startup+600.053 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1597 0 0 0 59987 13 0 0 25 0 1 0 1842353453 6909952 1546 4294967295 134512640 135094434 3221224448 3221223104 134558284 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1687 1546 145 145 0 1542 0
[pid=3170] vsize: 6748
Current children cumulated CPU time (s) 600
Current children cumulated vsize (Kb) 8872

[startup+610.054 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1600 0 0 0 60987 13 0 0 25 0 1 0 1842353453 6926336 1549 4294967295 134512640 135094434 3221224448 3221223104 134557978 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1691 1549 145 145 0 1546 0
[pid=3170] vsize: 6764
Current children cumulated CPU time (s) 610
Current children cumulated vsize (Kb) 8888

[startup+620.054 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1607 0 0 0 61987 13 0 0 25 0 1 0 1842353453 6955008 1556 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1698 1556 145 145 0 1553 0
[pid=3170] vsize: 6792
Current children cumulated CPU time (s) 620
Current children cumulated vsize (Kb) 8916

[startup+630.055 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1614 0 0 0 62988 13 0 0 25 0 1 0 1842353453 6987776 1563 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1706 1563 145 145 0 1561 0
[pid=3170] vsize: 6824
Current children cumulated CPU time (s) 630.01
Current children cumulated vsize (Kb) 8948

[startup+640.056 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1618 0 0 0 63987 13 0 0 25 0 1 0 1842353453 7053312 1567 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1722 1567 145 145 0 1577 0
[pid=3170] vsize: 6888
Current children cumulated CPU time (s) 640
Current children cumulated vsize (Kb) 9012

[startup+650.057 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1624 0 0 0 64988 13 0 0 25 0 1 0 1842353453 7053312 1573 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1722 1573 145 145 0 1577 0
[pid=3170] vsize: 6888
Current children cumulated CPU time (s) 650.01
Current children cumulated vsize (Kb) 9012

[startup+660.058 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1625 0 0 0 65988 13 0 0 25 0 1 0 1842353453 7053312 1574 4294967295 134512640 135094434 3221224448 3221223040 134557016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1722 1574 145 145 0 1577 0
[pid=3170] vsize: 6888
Current children cumulated CPU time (s) 660.01
Current children cumulated vsize (Kb) 9012

[startup+670.059 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1625 0 0 0 66988 14 0 0 25 0 1 0 1842353453 7053312 1574 4294967295 134512640 135094434 3221224448 3221223104 134556043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1722 1574 145 145 0 1577 0
[pid=3170] vsize: 6888
Current children cumulated CPU time (s) 670.02
Current children cumulated vsize (Kb) 9012

[startup+680.059 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1626 0 0 0 67988 14 0 0 25 0 1 0 1842353453 7053312 1575 4294967295 134512640 135094434 3221224448 3221223136 134554788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1722 1575 145 145 0 1577 0
[pid=3170] vsize: 6888
Current children cumulated CPU time (s) 680.02
Current children cumulated vsize (Kb) 9012

[startup+690.06 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1626 0 0 0 68988 14 0 0 25 0 1 0 1842353453 7053312 1575 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1722 1575 145 145 0 1577 0
[pid=3170] vsize: 6888
Current children cumulated CPU time (s) 690.02
Current children cumulated vsize (Kb) 9012

[startup+700.061 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1636 0 0 0 69988 14 0 0 25 0 1 0 1842353453 7118848 1585 4294967295 134512640 135094434 3221224448 3221223136 134554682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1738 1585 145 145 0 1593 0
[pid=3170] vsize: 6952
Current children cumulated CPU time (s) 700.02
Current children cumulated vsize (Kb) 9076

[startup+710.063 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1636 0 0 0 70989 14 0 0 25 0 1 0 1842353453 7118848 1585 4294967295 134512640 135094434 3221224448 3221223104 134557843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1738 1585 145 145 0 1593 0
[pid=3170] vsize: 6952
Current children cumulated CPU time (s) 710.03
Current children cumulated vsize (Kb) 9076

[startup+720.064 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1636 0 0 0 71989 14 0 0 25 0 1 0 1842353453 7118848 1585 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1738 1585 145 145 0 1593 0
[pid=3170] vsize: 6952
Current children cumulated CPU time (s) 720.03
Current children cumulated vsize (Kb) 9076

[startup+730.064 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1636 0 0 0 72989 14 0 0 25 0 1 0 1842353453 7118848 1585 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1738 1585 145 145 0 1593 0
[pid=3170] vsize: 6952
Current children cumulated CPU time (s) 730.03
Current children cumulated vsize (Kb) 9076

[startup+740.066 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1638 0 0 0 73989 14 0 0 25 0 1 0 1842353453 7118848 1587 4294967295 134512640 135094434 3221224448 3221223088 134562041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1738 1587 145 145 0 1593 0
[pid=3170] vsize: 6952
Current children cumulated CPU time (s) 740.03
Current children cumulated vsize (Kb) 9076

[startup+750.067 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1638 0 0 0 74989 14 0 0 25 0 1 0 1842353453 7118848 1587 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1738 1587 145 145 0 1593 0
[pid=3170] vsize: 6952
Current children cumulated CPU time (s) 750.03
Current children cumulated vsize (Kb) 9076

[startup+760.068 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1638 0 0 0 75990 14 0 0 25 0 1 0 1842353453 7118848 1587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1738 1587 145 145 0 1593 0
[pid=3170] vsize: 6952
Current children cumulated CPU time (s) 760.04
Current children cumulated vsize (Kb) 9076

[startup+770.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1638 0 0 0 76990 14 0 0 25 0 1 0 1842353453 7118848 1587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1738 1587 145 145 0 1593 0
[pid=3170] vsize: 6952
Current children cumulated CPU time (s) 770.04
Current children cumulated vsize (Kb) 9076

[startup+780.071 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1638 0 0 0 77990 14 0 0 25 0 1 0 1842353453 7118848 1587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1738 1587 145 145 0 1593 0
[pid=3170] vsize: 6952
Current children cumulated CPU time (s) 780.04
Current children cumulated vsize (Kb) 9076

[startup+790.071 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1638 0 0 0 78990 15 0 0 25 0 1 0 1842353453 7118848 1587 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1738 1587 145 145 0 1593 0
[pid=3170] vsize: 6952
Current children cumulated CPU time (s) 790.05
Current children cumulated vsize (Kb) 9076

[startup+800.072 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1638 0 0 0 79990 15 0 0 25 0 1 0 1842353453 7118848 1587 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1738 1587 145 145 0 1593 0
[pid=3170] vsize: 6952
Current children cumulated CPU time (s) 800.05
Current children cumulated vsize (Kb) 9076

[startup+810.073 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1639 0 0 0 80991 15 0 0 25 0 1 0 1842353453 7118848 1588 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1738 1588 145 145 0 1593 0
[pid=3170] vsize: 6952
Current children cumulated CPU time (s) 810.06
Current children cumulated vsize (Kb) 9076

[startup+820.074 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1639 0 0 0 81991 15 0 0 25 0 1 0 1842353453 7118848 1588 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1738 1588 145 145 0 1593 0
[pid=3170] vsize: 6952
Current children cumulated CPU time (s) 820.06
Current children cumulated vsize (Kb) 9076

[startup+830.075 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1649 0 0 0 82991 15 0 0 25 0 1 0 1842353453 7184384 1598 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1754 1598 145 145 0 1609 0
[pid=3170] vsize: 7016
Current children cumulated CPU time (s) 830.06
Current children cumulated vsize (Kb) 9140

[startup+840.077 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1649 0 0 0 83991 15 0 0 25 0 1 0 1842353453 7184384 1598 4294967295 134512640 135094434 3221224448 3221223120 134555609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1754 1598 145 145 0 1609 0
[pid=3170] vsize: 7016
Current children cumulated CPU time (s) 840.06
Current children cumulated vsize (Kb) 9140

[startup+850.077 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1649 0 0 0 84991 15 0 0 25 0 1 0 1842353453 7184384 1598 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1754 1598 145 145 0 1609 0
[pid=3170] vsize: 7016
Current children cumulated CPU time (s) 850.06
Current children cumulated vsize (Kb) 9140

[startup+860.078 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1650 0 0 0 85992 15 0 0 25 0 1 0 1842353453 7184384 1599 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1754 1599 145 145 0 1609 0
[pid=3170] vsize: 7016
Current children cumulated CPU time (s) 860.07
Current children cumulated vsize (Kb) 9140

[startup+870.079 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1650 0 0 0 86992 15 0 0 25 0 1 0 1842353453 7184384 1599 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1754 1599 145 145 0 1609 0
[pid=3170] vsize: 7016
Current children cumulated CPU time (s) 870.07
Current children cumulated vsize (Kb) 9140

[startup+880.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1650 0 0 0 87992 15 0 0 25 0 1 0 1842353453 7184384 1599 4294967295 134512640 135094434 3221224448 3221223072 134557574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1754 1599 145 145 0 1609 0
[pid=3170] vsize: 7016
Current children cumulated CPU time (s) 880.07
Current children cumulated vsize (Kb) 9140

[startup+890.081 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1650 0 0 0 88992 15 0 0 25 0 1 0 1842353453 7184384 1599 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1754 1599 145 145 0 1609 0
[pid=3170] vsize: 7016
Current children cumulated CPU time (s) 890.07
Current children cumulated vsize (Kb) 9140

[startup+900.081 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1653 0 0 0 89992 15 0 0 25 0 1 0 1842353453 7184384 1602 4294967295 134512640 135094434 3221224448 3221223080 134557638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1754 1602 145 145 0 1609 0
[pid=3170] vsize: 7016
Current children cumulated CPU time (s) 900.07
Current children cumulated vsize (Kb) 9140

[startup+910.082 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1716 0 0 0 90991 16 0 0 25 0 1 0 1842353453 7446528 1665 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1818 1665 145 145 0 1673 0
[pid=3170] vsize: 7272
Current children cumulated CPU time (s) 910.07
Current children cumulated vsize (Kb) 9396

[startup+920.083 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1716 0 0 0 91991 16 0 0 25 0 1 0 1842353453 7446528 1665 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1818 1665 145 145 0 1673 0
[pid=3170] vsize: 7272
Current children cumulated CPU time (s) 920.07
Current children cumulated vsize (Kb) 9396

[startup+930.084 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1716 0 0 0 92992 16 0 0 25 0 1 0 1842353453 7446528 1665 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1818 1665 145 145 0 1673 0
[pid=3170] vsize: 7272
Current children cumulated CPU time (s) 930.08
Current children cumulated vsize (Kb) 9396

[startup+940.086 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1716 0 0 0 93992 16 0 0 25 0 1 0 1842353453 7446528 1665 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1818 1665 145 145 0 1673 0
[pid=3170] vsize: 7272
Current children cumulated CPU time (s) 940.08
Current children cumulated vsize (Kb) 9396

[startup+950.087 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1716 0 0 0 94992 16 0 0 25 0 1 0 1842353453 7446528 1665 4294967295 134512640 135094434 3221224448 3221223040 134556870 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1818 1665 145 145 0 1673 0
[pid=3170] vsize: 7272
Current children cumulated CPU time (s) 950.08
Current children cumulated vsize (Kb) 9396

[startup+960.087 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1718 0 0 0 95993 16 0 0 25 0 1 0 1842353453 7446528 1667 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1818 1667 145 145 0 1673 0
[pid=3170] vsize: 7272
Current children cumulated CPU time (s) 960.09
Current children cumulated vsize (Kb) 9396

[startup+970.088 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1723 0 0 0 96992 16 0 0 25 0 1 0 1842353453 7479296 1672 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3170/statm): 1826 1672 145 145 0 1681 0
[pid=3170] vsize: 7304
Current children cumulated CPU time (s) 970.08
Current children cumulated vsize (Kb) 9428

[startup+980.089 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1726 0 0 0 97992 16 0 0 25 0 1 0 1842353453 7479296 1675 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1826 1675 145 145 0 1681 0
[pid=3170] vsize: 7304
Current children cumulated CPU time (s) 980.08
Current children cumulated vsize (Kb) 9428

[startup+990.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1726 0 0 0 98992 16 0 0 25 0 1 0 1842353453 7479296 1675 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1826 1675 145 145 0 1681 0
[pid=3170] vsize: 7304
Current children cumulated CPU time (s) 990.08
Current children cumulated vsize (Kb) 9428

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1735 0 0 0 99993 16 0 0 25 0 1 0 1842353453 7544832 1684 4294967295 134512640 135094434 3221224448 3221223104 134557829 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1842 1684 145 145 0 1697 0
[pid=3170] vsize: 7368
Current children cumulated CPU time (s) 1000.09
Current children cumulated vsize (Kb) 9492

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1735 0 0 0 100993 16 0 0 25 0 1 0 1842353453 7544832 1684 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1842 1684 145 145 0 1697 0
[pid=3170] vsize: 7368
Current children cumulated CPU time (s) 1010.09
Current children cumulated vsize (Kb) 9492

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1744 0 0 0 101993 16 0 0 25 0 1 0 1842353453 7610368 1693 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1858 1693 145 145 0 1713 0
[pid=3170] vsize: 7432
Current children cumulated CPU time (s) 1020.09
Current children cumulated vsize (Kb) 9556

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1745 0 0 0 102993 16 0 0 25 0 1 0 1842353453 7610368 1694 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1858 1694 145 145 0 1713 0
[pid=3170] vsize: 7432
Current children cumulated CPU time (s) 1030.09
Current children cumulated vsize (Kb) 9556

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1745 0 0 0 103993 17 0 0 25 0 1 0 1842353453 7610368 1694 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1858 1694 145 145 0 1713 0
[pid=3170] vsize: 7432
Current children cumulated CPU time (s) 1040.1
Current children cumulated vsize (Kb) 9556

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1745 0 0 0 104994 17 0 0 25 0 1 0 1842353453 7610368 1694 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1858 1694 145 145 0 1713 0
[pid=3170] vsize: 7432
Current children cumulated CPU time (s) 1050.11
Current children cumulated vsize (Kb) 9556

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1745 0 0 0 105994 17 0 0 25 0 1 0 1842353453 7610368 1694 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1858 1694 145 145 0 1713 0
[pid=3170] vsize: 7432
Current children cumulated CPU time (s) 1060.11
Current children cumulated vsize (Kb) 9556

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1745 0 0 0 106994 17 0 0 25 0 1 0 1842353453 7610368 1694 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1858 1694 145 145 0 1713 0
[pid=3170] vsize: 7432
Current children cumulated CPU time (s) 1070.11
Current children cumulated vsize (Kb) 9556

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1745 0 0 0 107995 17 0 0 25 0 1 0 1842353453 7610368 1694 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1858 1694 145 145 0 1713 0
[pid=3170] vsize: 7432
Current children cumulated CPU time (s) 1080.12
Current children cumulated vsize (Kb) 9556

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1745 0 0 0 108995 17 0 0 25 0 1 0 1842353453 7610368 1694 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1858 1694 145 145 0 1713 0
[pid=3170] vsize: 7432
Current children cumulated CPU time (s) 1090.12
Current children cumulated vsize (Kb) 9556

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1745 0 0 0 109995 17 0 0 25 0 1 0 1842353453 7610368 1694 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1858 1694 145 145 0 1713 0
[pid=3170] vsize: 7432
Current children cumulated CPU time (s) 1100.12
Current children cumulated vsize (Kb) 9556

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1746 0 0 0 110995 17 0 0 25 0 1 0 1842353453 7610368 1695 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1858 1695 145 145 0 1713 0
[pid=3170] vsize: 7432
Current children cumulated CPU time (s) 1110.12
Current children cumulated vsize (Kb) 9556

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1756 0 0 0 111996 17 0 0 25 0 1 0 1842353453 7675904 1705 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1874 1705 145 145 0 1729 0
[pid=3170] vsize: 7496
Current children cumulated CPU time (s) 1120.13
Current children cumulated vsize (Kb) 9620

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1756 0 0 0 112996 17 0 0 25 0 1 0 1842353453 7675904 1705 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1874 1705 145 145 0 1729 0
[pid=3170] vsize: 7496
Current children cumulated CPU time (s) 1130.13
Current children cumulated vsize (Kb) 9620

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1756 0 0 0 113996 17 0 0 25 0 1 0 1842353453 7675904 1705 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1874 1705 145 145 0 1729 0
[pid=3170] vsize: 7496
Current children cumulated CPU time (s) 1140.13
Current children cumulated vsize (Kb) 9620

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1756 0 0 0 114996 17 0 0 25 0 1 0 1842353453 7675904 1705 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1874 1705 145 145 0 1729 0
[pid=3170] vsize: 7496
Current children cumulated CPU time (s) 1150.13
Current children cumulated vsize (Kb) 9620

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1756 0 0 0 115995 18 0 0 25 0 1 0 1842353453 7675904 1705 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1874 1705 145 145 0 1729 0
[pid=3170] vsize: 7496
Current children cumulated CPU time (s) 1160.13
Current children cumulated vsize (Kb) 9620

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1756 0 0 0 116995 19 0 0 25 0 1 0 1842353453 7675904 1705 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1874 1705 145 145 0 1729 0
[pid=3170] vsize: 7496
Current children cumulated CPU time (s) 1170.14
Current children cumulated vsize (Kb) 9620

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1756 0 0 0 117995 19 0 0 25 0 1 0 1842353453 7675904 1705 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1874 1705 145 145 0 1729 0
[pid=3170] vsize: 7496
Current children cumulated CPU time (s) 1180.14
Current children cumulated vsize (Kb) 9620

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1756 0 0 0 118995 19 0 0 25 0 1 0 1842353453 7675904 1705 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1874 1705 145 145 0 1729 0
[pid=3170] vsize: 7496
Current children cumulated CPU time (s) 1190.14
Current children cumulated vsize (Kb) 9620

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1756 0 0 0 119995 19 0 0 25 0 1 0 1842353453 7675904 1705 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1874 1705 145 145 0 1729 0
[pid=3170] vsize: 7496
Current children cumulated CPU time (s) 1200.14
Current children cumulated vsize (Kb) 9620



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3170
Raw data (/proc/3166/stat): 3166 (minisat+_script) S 3165 3166 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842353448 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3166/statm): 531 226 485 147 0 384 0
[pid=3166] vsize: 2124
Raw data (/proc/3170/stat): 3170 (minisat+_64-bit) R 3166 3166 28974 0 -1 0 1756 0 0 0 119995 19 0 0 25 0 1 0 1842353453 7675904 1705 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3170/statm): 1874 1705 145 145 0 1729 0
[pid=3170] vsize: 7496
Current children cumulated CPU time (s) 1200.14
Current children cumulated vsize (Kb) 9620

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

Child status: 0
Real time (s): 1200.12
CPU time (s): 1200.16
CPU user time (s): 1199.96
CPU system time (s): 0.201969
CPU usage (%): 100.003
Max. virtual memory (cumulated for all children) (Kb): 9620

Verifier Data

ERROR: no interpretation found !