Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-fast0507.opb
MD5SUM38504d32a17a57a658eee171614b901e
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 324
Optimality of the best value was proved NO
Number of terms in the objective function 63009
Biggest coefficient in the objective function 2
Number of bits for the biggest coefficient in the objective function 2
Sum of the numbers in the objective function 122425
Number of bits of the sum of numbers in the objective function 17
Biggest number in a constraint 2
Number of bits of the biggest number in a constraint 2
Biggest sum of numbers in a constraint 122425
Number of bits of the biggest sum of numbers17
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.29
Number of variables63009
Total number of constraints63516
Number of constraints which are clauses507
Number of constraints which are cardinality constraints (but not clauses)63009
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint7753

Trace number 6129

Launcher Data

LAUNCH ON wulflinc4 THE 2005-09-20 03:35:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3292 boxname=wulflinc4 idbench=948 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  38504d32a17a57a658eee171614b901e  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-fast0507.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-fast0507.opb
IDLAUNCH: 3292
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
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:        868044 kB
Buffers:         33540 kB
Cached:         106020 kB
SwapCached:        860 kB
Active:          49476 kB
Inactive:        92684 kB
HighTotal:      131008 kB
HighFree:        26432 kB
LowTotal:       903652 kB
LowFree:        841612 kB
SwapTotal:     2097136 kB
SwapFree:      2095644 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5520 kB
Slab:            18776 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 03:55:57 (client local time) WITH STATUS 10 IN 1207.21 SECONDS
stats: 3292 7 1207.21 10

Solver Data

c Parsing PB file...
c Converting 494 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ==
c   -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     487   407371 |     162       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 343
c ---[   0]---> Adder-cost: 125984   maxlim: 122082   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  882303  3556733 |  294101       0        0     nan |  0.000 % |
c |       100 |  882255  3556553 |  323511      96      289     3.0 |  0.016 % |
c |       250 |  881309  3553217 |  355862     114      351     3.1 |  0.101 % |
c |       475 |  880776  3551348 |  391448     259      864     3.3 |  0.151 % |
c |       812 |  880279  3549615 |  430593     523     1870     3.6 |  0.196 % |
c |      1318 |  879889  3548279 |  473652     977     4292     4.4 |  0.232 % |
c |      2077 |  879700  3547656 |  521017    1709    10871     6.4 |  0.251 % |
c |      3216 |  879644  3547470 |  573119    2839    17243     6.1 |  0.256 % |
c |      4924 |  879509  3547011 |  630431    4532    25034     5.5 |  0.270 % |
c |      7486 |  879420  3546722 |  693474    7079    43284     6.1 |  0.279 % |
c |     11330 |  879361  3546531 |  762822   10915    68960     6.3 |  0.286 % |
c |     17096 |  879361  3546531 |  839104   16681   104664     6.3 |  0.286 % |
c |     25745 |  879361  3546531 |  923014   25330   246101     9.7 |  0.286 % |
c |     38719 |  879284  3546264 | 1015316   38293   536469    14.0 |  0.293 % |
c 
c *** TERMINATED ***
s SATISFIABLE

#### TRACE IS TOO LONG. SEE FILE pb05-wulflinc4-3292-948-3-0-8861.out.gz TO GET THE COMPLETE TRACE
#### TAIL OF TRACE ####
...c Parsing PB file...
c Converting 494 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ==
c   -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     487   407371 |     162       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 343
c ---[   0]---> Adder-cost: 125984   maxlim: 122082   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  882303  3556733 |  294101       0        0     nan |  0.000 % |
c |       100 |  882255  3556553 |  323511      96      289     3.0 |  0.016 % |
c |       250 |  881309  3553217 |  355862     114      351     3.1 |  0.101 % |
c |       475 |  880776  3551348 |  391448     259      864     3.3 |  0.151 % |
c |       812 |  880279  3549615 |  430593     523     1870     3.6 |  0.196 % |
c |      1318 |  879889  3548279 |  473652     977     4292     4.4 |  0.232 % |
c |      2077 |  879700  3547656 |  521017    1709    10871     6.4 |  0.251 % |
c |      3216 |  879644  3547470 |  573119    2839    17243     6.1 |  0.256 % |
c |      4924 |  879509  3547011 |  630431    4532    25034     5.5 |  0.270 % |
c |      7486 |  879420  3546722 |  693474    7079    43284     6.1 |  0.279 % |
c |     11330 |  879361  3546531 |  762822   10915    68960     6.3 |  0.286 % |
c |     17096 |  879361  3546531 |  839104   16681   104664     6.3 |  0.286 % |
c |     25745 |  879361  3546531 |  923014   25330   246101     9.7 |  0.286 % |
c |     38719 |  879284  3546264 | 1015316   38293   536469    14.0 |  0.293 % |
c 
c *** TERMINATED ***
s SATISFIABLE

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/8898/stat): 8898 (minisat+_script) R 8897 8898 6847 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797100190 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/8898/statm): 174 3 169 147 0 27 0
[pid=8898] 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=8899
New process pid=8900
New process pid=8901
One traced child (pid=8900) exited with status: 0
execve syscall for /bin/sed executable
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=8901) exited with status: 0
One traced child (pid=8899) exited with status: 0
New process pid=8902
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-fast0507.opb

[startup+10.0045 s]
Raw data (loadavg): 0.96 0.97 0.89 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 15408 0 0 0 887 63 0 0 25 0 1 0 1797100195 50012160 10879 4294967295 134512640 135094434 3221224432 3221222160 134519159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 12210 10880 145 145 0 12065 0
[pid=8902] vsize: 48840
Current children cumulated CPU time (s) 9.51
Current children cumulated vsize (Kb) 50964

[startup+20.0054 s]
Raw data (loadavg): 0.96 0.97 0.89 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 55972 0 0 0 1688 185 0 0 23 0 1 0 1797100195 185556992 41556 4294967295 134512640 135094434 3221224432 3221221872 134781858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8902/statm): 45302 41556 145 145 0 45157 0
[pid=8902] vsize: 181208
Current children cumulated CPU time (s) 18.74
Current children cumulated vsize (Kb) 183332

[startup+30.0062 s]
Raw data (loadavg): 0.97 0.97 0.89 1/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) T 8898 8898 6847 0 -1 0 97910 0 0 0 2492 304 0 0 24 0 1 0 1797100195 332865536 72948 4294967295 134512640 135094434 3221224432 3221220844 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8902/statm): 81266 72948 145 145 0 81121 0
[pid=8902] vsize: 325064
Current children cumulated CPU time (s) 27.97
Current children cumulated vsize (Kb) 327188

[startup+40.0071 s]
Raw data (loadavg): 0.97 0.97 0.90 1/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) T 8898 8898 6847 0 -1 0 114257 0 0 0 3385 358 0 0 25 0 1 0 1797100195 374099968 88387 4294967295 134512640 135094434 3221224432 3221216092 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8902/statm): 91333 88387 145 145 0 91188 0
[pid=8902] vsize: 365332
Current children cumulated CPU time (s) 37.44
Current children cumulated vsize (Kb) 367456

[startup+50.0089 s]
Raw data (loadavg): 0.98 0.97 0.90 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 126981 0 0 0 4273 414 0 0 25 0 1 0 1797100195 428355584 101111 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8902/statm): 104579 101111 145 145 0 104434 0
[pid=8902] vsize: 418316
Current children cumulated CPU time (s) 46.88
Current children cumulated vsize (Kb) 420440

[startup+60.0108 s]
Raw data (loadavg): 0.98 0.97 0.90 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 126990 0 0 0 5271 415 0 0 25 0 1 0 1797100195 428392448 101120 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 104588 101120 145 145 0 104443 0
[pid=8902] vsize: 418352
Current children cumulated CPU time (s) 56.87
Current children cumulated vsize (Kb) 420476

[startup+70.0116 s]
Raw data (loadavg): 0.98 0.97 0.90 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 127009 0 0 0 6270 415 0 0 25 0 1 0 1797100195 428470272 101139 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8902/statm): 104607 101139 145 145 0 104462 0
[pid=8902] vsize: 418428
Current children cumulated CPU time (s) 66.86
Current children cumulated vsize (Kb) 420552

[startup+80.0125 s]
Raw data (loadavg): 0.98 0.97 0.90 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 127063 0 0 0 7270 416 0 0 25 0 1 0 1797100195 428691456 101193 4294967295 134512640 135094434 3221224432 3221223044 134563052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 104661 101193 145 145 0 104516 0
[pid=8902] vsize: 418644
Current children cumulated CPU time (s) 76.87
Current children cumulated vsize (Kb) 420768

[startup+90.0133 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 127545 0 0 0 8263 419 0 0 25 0 1 0 1797100195 430665728 101675 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105143 101675 145 145 0 104998 0
[pid=8902] vsize: 420572
Current children cumulated CPU time (s) 86.83
Current children cumulated vsize (Kb) 422696

[startup+100.014 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 127744 0 0 0 9261 420 0 0 25 0 1 0 1797100195 431714304 101874 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105399 101874 145 145 0 105254 0
[pid=8902] vsize: 421596
Current children cumulated CPU time (s) 96.82
Current children cumulated vsize (Kb) 423720

[startup+110.016 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 127831 0 0 0 10259 420 0 0 25 0 1 0 1797100195 431996928 101961 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105468 101961 145 145 0 105323 0
[pid=8902] vsize: 421872
Current children cumulated CPU time (s) 106.8
Current children cumulated vsize (Kb) 423996

[startup+120.017 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 127887 0 0 0 11259 421 0 0 25 0 1 0 1797100195 432226304 102017 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105524 102017 145 145 0 105379 0
[pid=8902] vsize: 422096
Current children cumulated CPU time (s) 116.81
Current children cumulated vsize (Kb) 424220

[startup+130.017 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 127933 0 0 0 12258 421 0 0 25 0 1 0 1797100195 432410624 102063 4294967295 134512640 135094434 3221224432 3221223104 134555583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105569 102063 145 145 0 105424 0
[pid=8902] vsize: 422276
Current children cumulated CPU time (s) 126.8
Current children cumulated vsize (Kb) 424400

[startup+140.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 127976 0 0 0 13258 421 0 0 25 0 1 0 1797100195 432529408 102106 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105598 102106 145 145 0 105453 0
[pid=8902] vsize: 422392
Current children cumulated CPU time (s) 136.8
Current children cumulated vsize (Kb) 424516

[startup+150.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128005 0 0 0 14258 421 0 0 25 0 1 0 1797100195 432623616 102135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105621 102135 145 145 0 105476 0
[pid=8902] vsize: 422484
Current children cumulated CPU time (s) 146.8
Current children cumulated vsize (Kb) 424608

[startup+160.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128027 0 0 0 15258 421 0 0 25 0 1 0 1797100195 432697344 102157 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105639 102157 145 145 0 105494 0
[pid=8902] vsize: 422556
Current children cumulated CPU time (s) 156.8
Current children cumulated vsize (Kb) 424680

[startup+170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128042 0 0 0 16258 421 0 0 25 0 1 0 1797100195 432758784 102172 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105654 102172 145 145 0 105509 0
[pid=8902] vsize: 422616
Current children cumulated CPU time (s) 166.8
Current children cumulated vsize (Kb) 424740

[startup+180.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128055 0 0 0 17258 421 0 0 25 0 1 0 1797100195 432807936 102185 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105666 102185 145 145 0 105521 0
[pid=8902] vsize: 422664
Current children cumulated CPU time (s) 176.8
Current children cumulated vsize (Kb) 424788

[startup+190.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128063 0 0 0 18258 421 0 0 25 0 1 0 1797100195 432840704 102193 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105674 102193 145 145 0 105529 0
[pid=8902] vsize: 422696
Current children cumulated CPU time (s) 186.8
Current children cumulated vsize (Kb) 424820

[startup+200.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128081 0 0 0 19258 422 0 0 25 0 1 0 1797100195 432943104 102211 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105699 102211 145 145 0 105554 0
[pid=8902] vsize: 422796
Current children cumulated CPU time (s) 196.81
Current children cumulated vsize (Kb) 424920

[startup+210.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128081 0 0 0 20258 422 0 0 25 0 1 0 1797100195 432943104 102211 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105699 102211 145 145 0 105554 0
[pid=8902] vsize: 422796
Current children cumulated CPU time (s) 206.81
Current children cumulated vsize (Kb) 424920

[startup+220.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128087 0 0 0 21258 422 0 0 25 0 1 0 1797100195 432963584 102217 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105704 102217 145 145 0 105559 0
[pid=8902] vsize: 422816
Current children cumulated CPU time (s) 216.81
Current children cumulated vsize (Kb) 424940

[startup+230.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128096 0 0 0 22258 422 0 0 25 0 1 0 1797100195 432984064 102226 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105709 102226 145 145 0 105564 0
[pid=8902] vsize: 422836
Current children cumulated CPU time (s) 226.81
Current children cumulated vsize (Kb) 424960

[startup+240.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128101 0 0 0 23258 422 0 0 25 0 1 0 1797100195 433004544 102231 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105714 102231 145 145 0 105569 0
[pid=8902] vsize: 422856
Current children cumulated CPU time (s) 236.81
Current children cumulated vsize (Kb) 424980

[startup+250.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128109 0 0 0 24258 422 0 0 25 0 1 0 1797100195 433033216 102239 4294967295 134512640 135094434 3221224432 3221223072 134562068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105721 102239 145 145 0 105576 0
[pid=8902] vsize: 422884
Current children cumulated CPU time (s) 246.81
Current children cumulated vsize (Kb) 425008

[startup+260.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128113 0 0 0 25259 422 0 0 25 0 1 0 1797100195 433049600 102243 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105725 102243 145 145 0 105580 0
[pid=8902] vsize: 422900
Current children cumulated CPU time (s) 256.82
Current children cumulated vsize (Kb) 425024

[startup+270.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128121 0 0 0 26259 422 0 0 25 0 1 0 1797100195 433065984 102251 4294967295 134512640 135094434 3221224432 3221223044 134563064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105729 102251 145 145 0 105584 0
[pid=8902] vsize: 422916
Current children cumulated CPU time (s) 266.82
Current children cumulated vsize (Kb) 425040

[startup+280.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128129 0 0 0 27259 422 0 0 25 0 1 0 1797100195 433094656 102259 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105736 102259 145 145 0 105591 0
[pid=8902] vsize: 422944
Current children cumulated CPU time (s) 276.82
Current children cumulated vsize (Kb) 425068

[startup+290.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128132 0 0 0 28259 422 0 0 25 0 1 0 1797100195 433106944 102262 4294967295 134512640 135094434 3221224432 3221223088 134561463 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105739 102262 145 145 0 105594 0
[pid=8902] vsize: 422956
Current children cumulated CPU time (s) 286.82
Current children cumulated vsize (Kb) 425080

[startup+300.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128133 0 0 0 29259 422 0 0 25 0 1 0 1797100195 433111040 102263 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105740 102263 145 145 0 105595 0
[pid=8902] vsize: 422960
Current children cumulated CPU time (s) 296.82
Current children cumulated vsize (Kb) 425084

[startup+310.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128140 0 0 0 30259 422 0 0 25 0 1 0 1797100195 433131520 102270 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105745 102270 145 145 0 105600 0
[pid=8902] vsize: 422980
Current children cumulated CPU time (s) 306.82
Current children cumulated vsize (Kb) 425104

[startup+320.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128145 0 0 0 31259 422 0 0 25 0 1 0 1797100195 433143808 102275 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105748 102275 145 145 0 105603 0
[pid=8902] vsize: 422992
Current children cumulated CPU time (s) 316.82
Current children cumulated vsize (Kb) 425116

[startup+330.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128150 0 0 0 32259 422 0 0 25 0 1 0 1797100195 433164288 102280 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105753 102280 145 145 0 105608 0
[pid=8902] vsize: 423012
Current children cumulated CPU time (s) 326.82
Current children cumulated vsize (Kb) 425136

[startup+340.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128153 0 0 0 33260 422 0 0 25 0 1 0 1797100195 433172480 102283 4294967295 134512640 135094434 3221224432 3221223044 134563077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105755 102283 145 145 0 105610 0
[pid=8902] vsize: 423020
Current children cumulated CPU time (s) 336.83
Current children cumulated vsize (Kb) 425144

[startup+350.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128154 0 0 0 34260 422 0 0 25 0 1 0 1797100195 433176576 102284 4294967295 134512640 135094434 3221224432 3221223120 134554750 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105756 102284 145 145 0 105611 0
[pid=8902] vsize: 423024
Current children cumulated CPU time (s) 346.83
Current children cumulated vsize (Kb) 425148

[startup+360.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128157 0 0 0 35260 422 0 0 25 0 1 0 1797100195 433188864 102287 4294967295 134512640 135094434 3221224432 3221223052 134562986 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105759 102287 145 145 0 105614 0
[pid=8902] vsize: 423036
Current children cumulated CPU time (s) 356.83
Current children cumulated vsize (Kb) 425160

[startup+370.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128164 0 0 0 36260 422 0 0 25 0 1 0 1797100195 433213440 102294 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105765 102294 145 145 0 105620 0
[pid=8902] vsize: 423060
Current children cumulated CPU time (s) 366.83
Current children cumulated vsize (Kb) 425184

[startup+380.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128168 0 0 0 37260 422 0 0 25 0 1 0 1797100195 433229824 102298 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105769 102298 145 145 0 105624 0
[pid=8902] vsize: 423076
Current children cumulated CPU time (s) 376.83
Current children cumulated vsize (Kb) 425200

[startup+390.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128172 0 0 0 38261 422 0 0 25 0 1 0 1797100195 433233920 102302 4294967295 134512640 135094434 3221224432 3221223088 134561471 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105770 102302 145 145 0 105625 0
[pid=8902] vsize: 423080
Current children cumulated CPU time (s) 386.84
Current children cumulated vsize (Kb) 425204

[startup+400.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128174 0 0 0 39261 422 0 0 25 0 1 0 1797100195 433242112 102304 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105772 102304 145 145 0 105627 0
[pid=8902] vsize: 423088
Current children cumulated CPU time (s) 396.84
Current children cumulated vsize (Kb) 425212

[startup+410.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128176 0 0 0 40261 422 0 0 25 0 1 0 1797100195 433250304 102306 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105774 102306 145 145 0 105629 0
[pid=8902] vsize: 423096
Current children cumulated CPU time (s) 406.84
Current children cumulated vsize (Kb) 425220

[startup+420.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128179 0 0 0 41261 422 0 0 25 0 1 0 1797100195 433258496 102309 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105776 102309 145 145 0 105631 0
[pid=8902] vsize: 423104
Current children cumulated CPU time (s) 416.84
Current children cumulated vsize (Kb) 425228

[startup+430.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128181 0 0 0 42261 423 0 0 25 0 1 0 1797100195 433266688 102311 4294967295 134512640 135094434 3221224432 3221223088 134561514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105778 102311 145 145 0 105633 0
[pid=8902] vsize: 423112
Current children cumulated CPU time (s) 426.85
Current children cumulated vsize (Kb) 425236

[startup+440.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128185 0 0 0 43262 423 0 0 25 0 1 0 1797100195 433283072 102315 4294967295 134512640 135094434 3221224432 3221223088 134561698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105782 102315 145 145 0 105637 0
[pid=8902] vsize: 423128
Current children cumulated CPU time (s) 436.86
Current children cumulated vsize (Kb) 425252

[startup+450.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128190 0 0 0 44262 423 0 0 25 0 1 0 1797100195 433299456 102320 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105786 102320 145 145 0 105641 0
[pid=8902] vsize: 423144
Current children cumulated CPU time (s) 446.86
Current children cumulated vsize (Kb) 425268

[startup+460.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128211 0 0 0 45262 423 0 0 25 0 1 0 1797100195 433446912 102341 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105822 102341 145 145 0 105677 0
[pid=8902] vsize: 423288
Current children cumulated CPU time (s) 456.86
Current children cumulated vsize (Kb) 425412

[startup+470.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128216 0 0 0 46262 423 0 0 25 0 1 0 1797100195 433446912 102346 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8902/statm): 105822 102346 145 145 0 105677 0
[pid=8902] vsize: 423288
Current children cumulated CPU time (s) 466.86
Current children cumulated vsize (Kb) 425412

[startup+480.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128218 0 0 0 47262 423 0 0 25 0 1 0 1797100195 433455104 102348 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105824 102348 145 145 0 105679 0
[pid=8902] vsize: 423296
Current children cumulated CPU time (s) 476.86
Current children cumulated vsize (Kb) 425420

[startup+490.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128224 0 0 0 48262 423 0 0 25 0 1 0 1797100195 433475584 102354 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105829 102354 145 145 0 105684 0
[pid=8902] vsize: 423316
Current children cumulated CPU time (s) 486.86
Current children cumulated vsize (Kb) 425440

[startup+500.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128231 0 0 0 49262 423 0 0 25 0 1 0 1797100195 433504256 102361 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105836 102361 145 145 0 105691 0
[pid=8902] vsize: 423344
Current children cumulated CPU time (s) 496.86
Current children cumulated vsize (Kb) 425468

[startup+510.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128245 0 0 0 50262 423 0 0 25 0 1 0 1797100195 433557504 102375 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105849 102375 145 145 0 105704 0
[pid=8902] vsize: 423396
Current children cumulated CPU time (s) 506.86
Current children cumulated vsize (Kb) 425520

[startup+520.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128250 0 0 0 51262 423 0 0 25 0 1 0 1797100195 433577984 102380 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105854 102380 145 145 0 105709 0
[pid=8902] vsize: 423416
Current children cumulated CPU time (s) 516.86
Current children cumulated vsize (Kb) 425540

[startup+530.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128258 0 0 0 52263 423 0 0 25 0 1 0 1797100195 433610752 102388 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105862 102388 145 145 0 105717 0
[pid=8902] vsize: 423448
Current children cumulated CPU time (s) 526.87
Current children cumulated vsize (Kb) 425572

[startup+540.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128320 0 0 0 53261 424 0 0 25 0 1 0 1797100195 433819648 102450 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105913 102450 145 145 0 105768 0
[pid=8902] vsize: 423652
Current children cumulated CPU time (s) 536.86
Current children cumulated vsize (Kb) 425776

[startup+550.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128324 0 0 0 54261 424 0 0 25 0 1 0 1797100195 433836032 102454 4294967295 134512640 135094434 3221224432 3221223044 134563041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105917 102454 145 145 0 105772 0
[pid=8902] vsize: 423668
Current children cumulated CPU time (s) 546.86
Current children cumulated vsize (Kb) 425792

[startup+560.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128327 0 0 0 55262 424 0 0 25 0 1 0 1797100195 433848320 102457 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105920 102457 145 145 0 105775 0
[pid=8902] vsize: 423680
Current children cumulated CPU time (s) 556.87
Current children cumulated vsize (Kb) 425804

[startup+570.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128330 0 0 0 56262 424 0 0 25 0 1 0 1797100195 433860608 102460 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105923 102460 145 145 0 105778 0
[pid=8902] vsize: 423692
Current children cumulated CPU time (s) 566.87
Current children cumulated vsize (Kb) 425816

[startup+580.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128335 0 0 0 57262 424 0 0 25 0 1 0 1797100195 433876992 102465 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105927 102465 145 145 0 105782 0
[pid=8902] vsize: 423708
Current children cumulated CPU time (s) 576.87
Current children cumulated vsize (Kb) 425832

[startup+590.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128343 0 0 0 58262 424 0 0 25 0 1 0 1797100195 433909760 102473 4294967295 134512640 135094434 3221224432 3221223044 134563080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105935 102473 145 145 0 105790 0
[pid=8902] vsize: 423740
Current children cumulated CPU time (s) 586.87
Current children cumulated vsize (Kb) 425864

[startup+600.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128351 0 0 0 59262 424 0 0 25 0 1 0 1797100195 433942528 102481 4294967295 134512640 135094434 3221224432 3221223088 134561508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105943 102481 145 145 0 105798 0
[pid=8902] vsize: 423772
Current children cumulated CPU time (s) 596.87
Current children cumulated vsize (Kb) 425896

[startup+610.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128375 0 0 0 60262 424 0 0 25 0 1 0 1797100195 434032640 102505 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105965 102505 145 145 0 105820 0
[pid=8902] vsize: 423860
Current children cumulated CPU time (s) 606.87
Current children cumulated vsize (Kb) 425984

[startup+620.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128387 0 0 0 61262 424 0 0 25 0 1 0 1797100195 434081792 102517 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105977 102517 145 145 0 105832 0
[pid=8902] vsize: 423908
Current children cumulated CPU time (s) 616.87
Current children cumulated vsize (Kb) 426032

[startup+630.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128392 0 0 0 62262 424 0 0 25 0 1 0 1797100195 434098176 102522 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105981 102522 145 145 0 105836 0
[pid=8902] vsize: 423924
Current children cumulated CPU time (s) 626.87
Current children cumulated vsize (Kb) 426048

[startup+640.066 s]
Raw data (loadavg): 0.99 0.97 0.91 5/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128400 0 0 0 63262 424 0 0 25 0 1 0 1797100195 434130944 102530 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105989 102530 145 145 0 105844 0
[pid=8902] vsize: 423956
Current children cumulated CPU time (s) 636.87
Current children cumulated vsize (Kb) 426080

[startup+650.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128410 0 0 0 64262 424 0 0 25 0 1 0 1797100195 434171904 102540 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 105999 102540 145 145 0 105854 0
[pid=8902] vsize: 423996
Current children cumulated CPU time (s) 646.87
Current children cumulated vsize (Kb) 426120

[startup+660.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128422 0 0 0 65262 424 0 0 25 0 1 0 1797100195 434216960 102552 4294967295 134512640 135094434 3221224432 3221223072 134562090 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106010 102552 145 145 0 105865 0
[pid=8902] vsize: 424040
Current children cumulated CPU time (s) 656.87
Current children cumulated vsize (Kb) 426164

[startup+670.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128432 0 0 0 66262 425 0 0 25 0 1 0 1797100195 434257920 102562 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106020 102562 145 145 0 105875 0
[pid=8902] vsize: 424080
Current children cumulated CPU time (s) 666.88
Current children cumulated vsize (Kb) 426204

[startup+680.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128501 0 0 0 67261 425 0 0 25 0 1 0 1797100195 434532352 102631 4294967295 134512640 135094434 3221224432 3221223044 134563066 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106087 102631 145 145 0 105942 0
[pid=8902] vsize: 424348
Current children cumulated CPU time (s) 676.87
Current children cumulated vsize (Kb) 426472

[startup+690.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128506 0 0 0 68262 425 0 0 25 0 1 0 1797100195 434552832 102636 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106092 102636 145 145 0 105947 0
[pid=8902] vsize: 424368
Current children cumulated CPU time (s) 686.88
Current children cumulated vsize (Kb) 426492

[startup+700.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128514 0 0 0 69261 425 0 0 25 0 1 0 1797100195 434573312 102644 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106097 102644 145 145 0 105952 0
[pid=8902] vsize: 424388
Current children cumulated CPU time (s) 696.87
Current children cumulated vsize (Kb) 426512

[startup+710.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128518 0 0 0 70262 425 0 0 25 0 1 0 1797100195 434589696 102648 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106101 102648 145 145 0 105956 0
[pid=8902] vsize: 424404
Current children cumulated CPU time (s) 706.88
Current children cumulated vsize (Kb) 426528

[startup+720.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128519 0 0 0 71262 425 0 0 25 0 1 0 1797100195 434593792 102649 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106102 102649 145 145 0 105957 0
[pid=8902] vsize: 424408
Current children cumulated CPU time (s) 716.88
Current children cumulated vsize (Kb) 426532

[startup+730.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128523 0 0 0 72262 425 0 0 25 0 1 0 1797100195 434601984 102653 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106104 102653 145 145 0 105959 0
[pid=8902] vsize: 424416
Current children cumulated CPU time (s) 726.88
Current children cumulated vsize (Kb) 426540

[startup+740.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128528 0 0 0 73262 425 0 0 25 0 1 0 1797100195 434622464 102658 4294967295 134512640 135094434 3221224432 3221223088 134561737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106109 102658 145 145 0 105964 0
[pid=8902] vsize: 424436
Current children cumulated CPU time (s) 736.88
Current children cumulated vsize (Kb) 426560

[startup+750.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128534 0 0 0 74262 425 0 0 25 0 1 0 1797100195 434647040 102664 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106115 102664 145 145 0 105970 0
[pid=8902] vsize: 424460
Current children cumulated CPU time (s) 746.88
Current children cumulated vsize (Kb) 426584

[startup+760.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128537 0 0 0 75262 425 0 0 25 0 1 0 1797100195 434659328 102667 4294967295 134512640 135094434 3221224432 3221223088 134561476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106118 102667 145 145 0 105973 0
[pid=8902] vsize: 424472
Current children cumulated CPU time (s) 756.88
Current children cumulated vsize (Kb) 426596

[startup+770.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128540 0 0 0 76263 426 0 0 25 0 1 0 1797100195 434667520 102670 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106120 102670 145 145 0 105975 0
[pid=8902] vsize: 424480
Current children cumulated CPU time (s) 766.9
Current children cumulated vsize (Kb) 426604

[startup+780.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128546 0 0 0 77263 426 0 0 25 0 1 0 1797100195 434692096 102676 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106126 102676 145 145 0 105981 0
[pid=8902] vsize: 424504
Current children cumulated CPU time (s) 776.9
Current children cumulated vsize (Kb) 426628

[startup+790.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8902
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128647 0 0 0 78261 426 0 0 25 0 1 0 1797100195 435097600 102777 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106225 102777 145 145 0 106080 0
[pid=8902] vsize: 424900
Current children cumulated CPU time (s) 786.88
Current children cumulated vsize (Kb) 427024

[startup+800.082 s]
Raw data (loadavg): 0.99 0.97 0.91 3/61 8945
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128661 0 0 0 79260 427 0 0 17 0 1 0 1797100195 435154944 102791 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106239 102791 145 145 0 106094 0
[pid=8902] vsize: 424956
Current children cumulated CPU time (s) 796.88
Current children cumulated vsize (Kb) 427080

[startup+810.085 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 8953
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128669 0 0 0 80260 427 0 0 25 0 1 0 1797100195 435187712 102799 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106247 102799 145 145 0 106102 0
[pid=8902] vsize: 424988
Current children cumulated CPU time (s) 806.88
Current children cumulated vsize (Kb) 427112

[startup+820.086 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 8953
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128679 0 0 0 81260 427 0 0 25 0 1 0 1797100195 435228672 102809 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106257 102809 145 145 0 106112 0
[pid=8902] vsize: 425028
Current children cumulated CPU time (s) 816.88
Current children cumulated vsize (Kb) 427152

[startup+830.087 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 8953
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128717 0 0 0 82260 428 0 0 25 0 1 0 1797100195 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106326 102847 145 145 0 106181 0
[pid=8902] vsize: 425304
Current children cumulated CPU time (s) 826.89
Current children cumulated vsize (Kb) 427428

[startup+840.088 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 8953
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128717 0 0 0 83260 428 0 0 25 0 1 0 1797100195 435511296 102847 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106326 102847 145 145 0 106181 0
[pid=8902] vsize: 425304
Current children cumulated CPU time (s) 836.89
Current children cumulated vsize (Kb) 427428

[startup+850.089 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 8953
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128717 0 0 0 84260 428 0 0 25 0 1 0 1797100195 435511296 102847 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106326 102847 145 145 0 106181 0
[pid=8902] vsize: 425304
Current children cumulated CPU time (s) 846.89
Current children cumulated vsize (Kb) 427428

[startup+860.09 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 8953
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128718 0 0 0 85260 428 0 0 25 0 1 0 1797100195 435511296 102848 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106326 102848 145 145 0 106181 0
[pid=8902] vsize: 425304
Current children cumulated CPU time (s) 856.89
Current children cumulated vsize (Kb) 427428

[startup+870.092 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 8955
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128718 0 0 0 86261 428 0 0 25 0 1 0 1797100195 435511296 102848 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106326 102848 145 145 0 106181 0
[pid=8902] vsize: 425304
Current children cumulated CPU time (s) 866.9
Current children cumulated vsize (Kb) 427428

[startup+880.093 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128719 0 0 0 87261 428 0 0 25 0 1 0 1797100195 435511296 102849 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106326 102849 145 145 0 106181 0
[pid=8902] vsize: 425304
Current children cumulated CPU time (s) 876.9
Current children cumulated vsize (Kb) 427428

[startup+890.094 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128720 0 0 0 88261 428 0 0 25 0 1 0 1797100195 435511296 102850 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106326 102850 145 145 0 106181 0
[pid=8902] vsize: 425304
Current children cumulated CPU time (s) 886.9
Current children cumulated vsize (Kb) 427428

[startup+900.095 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128721 0 0 0 89261 428 0 0 25 0 1 0 1797100195 435515392 102851 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106327 102851 145 145 0 106182 0
[pid=8902] vsize: 425308
Current children cumulated CPU time (s) 896.9
Current children cumulated vsize (Kb) 427432

[startup+910.096 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128724 0 0 0 90262 428 0 0 25 0 1 0 1797100195 435527680 102854 4294967295 134512640 135094434 3221224432 3221223112 134554880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106330 102854 145 145 0 106185 0
[pid=8902] vsize: 425320
Current children cumulated CPU time (s) 906.91
Current children cumulated vsize (Kb) 427444

[startup+920.097 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128729 0 0 0 91262 428 0 0 25 0 1 0 1797100195 435548160 102859 4294967295 134512640 135094434 3221224432 3221223084 134561522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106335 102859 145 145 0 106190 0
[pid=8902] vsize: 425340
Current children cumulated CPU time (s) 916.91
Current children cumulated vsize (Kb) 427464

[startup+930.098 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128744 0 0 0 92262 428 0 0 25 0 1 0 1797100195 435605504 102874 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106349 102874 145 145 0 106204 0
[pid=8902] vsize: 425396
Current children cumulated CPU time (s) 926.91
Current children cumulated vsize (Kb) 427520

[startup+940.099 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128772 0 0 0 93261 428 0 0 25 0 1 0 1797100195 435720192 102902 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106377 102902 145 145 0 106232 0
[pid=8902] vsize: 425508
Current children cumulated CPU time (s) 936.9
Current children cumulated vsize (Kb) 427632

[startup+950.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128806 0 0 0 94261 428 0 0 25 0 1 0 1797100195 435855360 102936 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106410 102936 145 145 0 106265 0
[pid=8902] vsize: 425640
Current children cumulated CPU time (s) 946.9
Current children cumulated vsize (Kb) 427764

[startup+960.101 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128830 0 0 0 95261 428 0 0 25 0 1 0 1797100195 435949568 102960 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106433 102960 145 145 0 106288 0
[pid=8902] vsize: 425732
Current children cumulated CPU time (s) 956.9
Current children cumulated vsize (Kb) 427856

[startup+970.102 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128853 0 0 0 96260 429 0 0 25 0 1 0 1797100195 436043776 102983 4294967295 134512640 135094434 3221224432 3221223044 134563024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106456 102983 145 145 0 106311 0
[pid=8902] vsize: 425824
Current children cumulated CPU time (s) 966.9
Current children cumulated vsize (Kb) 427948

[startup+980.102 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128872 0 0 0 97260 429 0 0 25 0 1 0 1797100195 436117504 103002 4294967295 134512640 135094434 3221224432 3221223108 134554883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106474 103002 145 145 0 106329 0
[pid=8902] vsize: 425896
Current children cumulated CPU time (s) 976.9
Current children cumulated vsize (Kb) 428020

[startup+990.102 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 128963 0 0 0 98258 430 0 0 25 0 1 0 1797100195 436482048 103093 4294967295 134512640 135094434 3221224432 3221223024 134556815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106563 103093 145 145 0 106418 0
[pid=8902] vsize: 426252
Current children cumulated CPU time (s) 986.89
Current children cumulated vsize (Kb) 428376

[startup+1000.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129066 0 0 0 99256 430 0 0 25 0 1 0 1797100195 436895744 103196 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106664 103196 145 145 0 106519 0
[pid=8902] vsize: 426656
Current children cumulated CPU time (s) 996.87
Current children cumulated vsize (Kb) 428780

[startup+1010.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129083 0 0 0 100256 430 0 0 25 0 1 0 1797100195 436961280 103213 4294967295 134512640 135094434 3221224432 3221223088 134561741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106680 103213 145 145 0 106535 0
[pid=8902] vsize: 426720
Current children cumulated CPU time (s) 1006.87
Current children cumulated vsize (Kb) 428844

[startup+1020.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129088 0 0 0 101256 430 0 0 25 0 1 0 1797100195 436981760 103218 4294967295 134512640 135094434 3221224432 3221223072 134562045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106685 103218 145 145 0 106540 0
[pid=8902] vsize: 426740
Current children cumulated CPU time (s) 1016.87
Current children cumulated vsize (Kb) 428864

[startup+1030.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129106 0 0 0 102256 431 0 0 25 0 1 0 1797100195 437055488 103236 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106703 103236 145 145 0 106558 0
[pid=8902] vsize: 426812
Current children cumulated CPU time (s) 1026.88
Current children cumulated vsize (Kb) 428936

[startup+1040.11 s]
Raw data (loadavg): 1.08 1.00 0.92 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129115 0 0 0 103256 431 0 0 25 0 1 0 1797100195 437088256 103245 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106711 103245 145 145 0 106566 0
[pid=8902] vsize: 426844
Current children cumulated CPU time (s) 1036.88
Current children cumulated vsize (Kb) 428968

[startup+1050.11 s]
Raw data (loadavg): 1.07 1.00 0.92 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129132 0 0 0 104256 431 0 0 25 0 1 0 1797100195 437157888 103262 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106728 103262 145 145 0 106583 0
[pid=8902] vsize: 426912
Current children cumulated CPU time (s) 1046.88
Current children cumulated vsize (Kb) 429036

[startup+1060.11 s]
Raw data (loadavg): 1.06 1.00 0.92 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129169 0 0 0 105255 431 0 0 25 0 1 0 1797100195 437309440 103299 4294967295 134512640 135094434 3221224432 3221223088 134558026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106765 103299 145 145 0 106620 0
[pid=8902] vsize: 427060
Current children cumulated CPU time (s) 1056.87
Current children cumulated vsize (Kb) 429184

[startup+1070.11 s]
Raw data (loadavg): 1.05 1.00 0.92 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129196 0 0 0 106254 432 0 0 25 0 1 0 1797100195 437415936 103326 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106791 103326 145 145 0 106646 0
[pid=8902] vsize: 427164
Current children cumulated CPU time (s) 1066.87
Current children cumulated vsize (Kb) 429288

[startup+1080.11 s]
Raw data (loadavg): 1.04 1.00 0.92 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129220 0 0 0 107254 432 0 0 25 0 1 0 1797100195 437514240 103350 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106815 103350 145 145 0 106670 0
[pid=8902] vsize: 427260
Current children cumulated CPU time (s) 1076.87
Current children cumulated vsize (Kb) 429384

[startup+1090.11 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129235 0 0 0 108254 432 0 0 25 0 1 0 1797100195 437571584 103365 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106829 103365 145 145 0 106684 0
[pid=8902] vsize: 427316
Current children cumulated CPU time (s) 1086.87
Current children cumulated vsize (Kb) 429440

[startup+1100.11 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129249 0 0 0 109254 432 0 0 25 0 1 0 1797100195 437628928 103379 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106843 103379 145 145 0 106698 0
[pid=8902] vsize: 427372
Current children cumulated CPU time (s) 1096.87
Current children cumulated vsize (Kb) 429496

[startup+1110.11 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129265 0 0 0 110254 432 0 0 25 0 1 0 1797100195 437694464 103395 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106859 103395 145 145 0 106714 0
[pid=8902] vsize: 427436
Current children cumulated CPU time (s) 1106.87
Current children cumulated vsize (Kb) 429560

[startup+1120.11 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129279 0 0 0 111254 432 0 0 25 0 1 0 1797100195 437747712 103409 4294967295 134512640 135094434 3221224432 3221223120 134554854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106872 103409 145 145 0 106727 0
[pid=8902] vsize: 427488
Current children cumulated CPU time (s) 1116.87
Current children cumulated vsize (Kb) 429612

[startup+1130.11 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129299 0 0 0 112254 433 0 0 25 0 1 0 1797100195 437829632 103429 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106892 103429 145 145 0 106747 0
[pid=8902] vsize: 427568
Current children cumulated CPU time (s) 1126.88
Current children cumulated vsize (Kb) 429692

[startup+1140.12 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129317 0 0 0 113253 433 0 0 25 0 1 0 1797100195 437903360 103447 4294967295 134512640 135094434 3221224432 3221223088 134561505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106910 103447 145 145 0 106765 0
[pid=8902] vsize: 427640
Current children cumulated CPU time (s) 1136.87
Current children cumulated vsize (Kb) 429764

[startup+1150.12 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129326 0 0 0 114253 433 0 0 25 0 1 0 1797100195 437940224 103456 4294967295 134512640 135094434 3221224432 3221223072 134562128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106919 103456 145 145 0 106774 0
[pid=8902] vsize: 427676
Current children cumulated CPU time (s) 1146.87
Current children cumulated vsize (Kb) 429800

[startup+1160.12 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129337 0 0 0 115253 433 0 0 25 0 1 0 1797100195 437985280 103467 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106930 103467 145 145 0 106785 0
[pid=8902] vsize: 427720
Current children cumulated CPU time (s) 1156.87
Current children cumulated vsize (Kb) 429844

[startup+1170.12 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 8957
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129339 0 0 0 116254 433 0 0 25 0 1 0 1797100195 437993472 103469 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106932 103469 145 145 0 106787 0
[pid=8902] vsize: 427728
Current children cumulated CPU time (s) 1166.88
Current children cumulated vsize (Kb) 429852

[startup+1180.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 8959
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129343 0 0 0 117254 433 0 0 25 0 1 0 1797100195 438009856 103473 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106936 103473 145 145 0 106791 0
[pid=8902] vsize: 427744
Current children cumulated CPU time (s) 1176.88
Current children cumulated vsize (Kb) 429868

[startup+1190.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 8959
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129349 0 0 0 118254 433 0 0 25 0 1 0 1797100195 438034432 103479 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106942 103479 145 145 0 106797 0
[pid=8902] vsize: 427768
Current children cumulated CPU time (s) 1186.88
Current children cumulated vsize (Kb) 429892

[startup+1200.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 8959
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129355 0 0 0 119254 433 0 0 25 0 1 0 1797100195 438059008 103485 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106948 103485 145 145 0 106803 0
[pid=8902] vsize: 427792
Current children cumulated CPU time (s) 1196.88
Current children cumulated vsize (Kb) 429916

[startup+1210.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 8959
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129370 0 0 0 120254 433 0 0 25 0 1 0 1797100195 438116352 103500 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106962 103500 145 145 0 106817 0
[pid=8902] vsize: 427848
Current children cumulated CPU time (s) 1206.88
Current children cumulated vsize (Kb) 429972



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 8959
Raw data (/proc/8898/stat): 8898 (minisat+_script) S 8897 8898 6847 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797100190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8898/statm): 531 226 485 147 0 384 0
[pid=8898] vsize: 2124
Raw data (/proc/8902/stat): 8902 (minisat+_64-bit) R 8898 8898 6847 0 -1 0 129370 0 0 0 120254 433 0 0 25 0 1 0 1797100195 438116352 103500 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8902/statm): 106962 103500 145 145 0 106817 0
[pid=8902] vsize: 427848
Current children cumulated CPU time (s) 1206.88
Current children cumulated vsize (Kb) 429972

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

Child status: 10
Real time (s): 1210.51
CPU time (s): 1207.21
CPU user time (s): 1202.65
CPU system time (s): 4.56531
CPU usage (%): 99.7274
Max. virtual memory (cumulated for all children) (Kb): 429972

Verifier Data

ERROR: no interpretation found !