Some explanations

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

General information on the benchmark

Namesubmitted/aloul/FPGA_SAT05/normalized-chnl50_60_pb.cnf.cr.opb
MD5SUM6968a43b42bba7df68b13fdfd3b616a1
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 61
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.207967
Number of variables6000
Total number of constraints220
Number of constraints which are clauses120
Number of constraints which are cardinality constraints (but not clauses)100
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint50
Maximum length of a constraint60

Trace number 872

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        941848 kB
Buffers:         34352 kB
Cached:          31596 kB
SwapCached:        896 kB
Active:          53528 kB
Inactive:        15048 kB
HighTotal:      131008 kB
HighFree:        98028 kB
LowTotal:       903652 kB
LowFree:        843820 kB
SwapTotal:     2097892 kB
SwapFree:      2096496 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            18652 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 12:50:20 (client local time) WITH STATUS 0 IN 1207.4 SECONDS
stats: 2363 7 1207.4 0

Solver Data

c Parsing PB file...
c Converting 220 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................
c ---[  99]---> BDD-cost:  117
c ---[  98]---> BDD-cost:  117
c ---[  97]---> BDD-cost:  117
c ---[  96]---> BDD-cost:  117
c ---[  95]---> BDD-cost:  117
c ---[  94]---> BDD-cost:  117
c ---[  93]---> BDD-cost:  117
c ---[  92]---> BDD-cost:  117
c ---[  91]---> BDD-cost:  117
c ---[  90]---> BDD-cost:  117
c ---[  89]---> BDD-cost:  117
c ---[  88]---> BDD-cost:  117
c ---[  87]---> BDD-cost:  117
c ---[  86]---> BDD-cost:  117
c ---[  85]---> BDD-cost:  117
c ---[  84]---> BDD-cost:  117
c ---[  83]---> BDD-cost:  117
c ---[  82]---> BDD-cost:  117
c ---[  81]---> BDD-cost:  117
c ---[  80]---> BDD-cost:  117
c ---[  79]---> BDD-cost:  117
c ---[  78]---> BDD-cost:  117
c ---[  77]---> BDD-cost:  117
c ---[  76]---> BDD-cost:  117
c ---[  75]---> BDD-cost:  117
c ---[  74]---> BDD-cost:  117
c ---[  73]---> BDD-cost:  117
c ---[  72]---> BDD-cost:  117
c ---[  71]---> BDD-cost:  117
c ---[  70]---> BDD-cost:  117
c ---[  69]---> BDD-cost:  117
c ---[  68]---> BDD-cost:  117
c ---[  67]---> BDD-cost:  117
c ---[  66]---> BDD-cost:  117
c ---[  65]---> BDD-cost:  117
c ---[  64]---> BDD-cost:  117
c ---[  63]---> BDD-cost:  117
c ---[  62]---> BDD-cost:  117
c ---[  61]---> BDD-cost:  117
c ---[  60]---> BDD-cost:  117
c ---[  59]---> BDD-cost:  117
c ---[  58]---> BDD-cost:  117
c ---[  57]---> BDD-cost:  117
c ---[  56]---> BDD-cost:  117
c ---[  55]---> BDD-cost:  117
c ---[  54]---> BDD-cost:  117
c ---[  53]---> BDD-cost:  117
c ---[  52]---> BDD-cost:  117
c ---[  51]---> BDD-cost:  117
c ---[  50]---> BDD-cost:  117
c ---[  49]---> BDD-cost:  117
c ---[  48]---> BDD-cost:  117
c ---[  47]---> BDD-cost:  117
c ---[  46]---> BDD-cost:  117
c ---[  45]---> BDD-cost:  117
c ---[  44]---> BDD-cost:  117
c ---[  43]---> BDD-cost:  117
c ---[  42]---> BDD-cost:  117
c ---[  41]---> BDD-cost:  117
c ---[  40]---> BDD-cost:  117
c ---[  39]---> BDD-cost:  117
c ---[  38]---> BDD-cost:  117
c ---[  37]---> BDD-cost:  117
c ---[  36]---> BDD-cost:  117
c ---[  35]---> BDD-cost:  117
c ---[  34]---> BDD-cost:  117
c ---[  33]---> BDD-cost:  117
c ---[  32]---> BDD-cost:  117
c ---[  31]---> BDD-cost:  117
c ---[  30]---> BDD-cost:  117
c ---[  29]---> BDD-cost:  117
c ---[  28]---> BDD-cost:  117
c ---[  27]---> BDD-cost:  117
c ---[  26]---> BDD-cost:  117
c ---[  25]---> BDD-cost:  117
c ---[  24]---> BDD-cost:  117
c ---[  23]---> BDD-cost:  117
c ---[  22]---> BDD-cost:  117
c ---[  21]---> BDD-cost:  117
c ---[  20]---> BDD-cost:  117
c ---[  19]---> BDD-cost:  117
c ---[  18]---> BDD-cost:  117
c ---[  17]---> BDD-cost:  117
c ---[  16]---> BDD-cost:  117
c ---[  15]---> BDD-cost:  117
c ---[  14]---> BDD-cost:  117
c ---[  13]---> BDD-cost:  117
c ---[  12]---> BDD-cost:  117
c ---[  11]---> BDD-cost:  117
c ---[  10]---> BDD-cost:  117
c ---[   9]---> BDD-cost:  117
c ---[   8]---> BDD-cost:  117
c ---[   7]---> BDD-cost:  117
c ---[   6]---> BDD-cost:  117
c ---[   5]---> BDD-cost:  117
c ---[   4]---> BDD-cost:  117
c ---[   3]---> BDD-cost:  117
c ---[   2]---> BDD-cost:  117
c ---[   1]---> BDD-cost:  117
c ---[   0]---> BDD-cost:  117
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   29220    81700 |    9740       0        0     nan |  0.000 % |
c |       104 |   29220    81700 |   10714     104    19328   185.8 |  0.565 % |
c |       256 |   29220    81700 |   11785     256    51373   200.7 |  0.565 % |
c |       482 |   29220    81700 |   12963     482   102298   212.2 |  0.565 % |
c |       824 |   29220    81700 |   14260     824   174285   211.5 |  0.565 % |
c |      1330 |   29220    81700 |   15686    1330   314613   236.6 |  0.565 % |
c |      2091 |   29220    81700 |   17255    2091   547467   261.8 |  0.565 % |
c |      3231 |   29220    81700 |   18980    3231   973163   301.2 |  0.565 % |
c |      4940 |   29220    81700 |   20878    4940  1825691   369.6 |  0.565 % |
c |      7502 |   29220    81700 |   22966    7502  3300948   440.0 |  0.565 % |
c |     11349 |   29220    81700 |   25263   11349  4927293   434.2 |  0.565 % |
c |     17116 |   29220    81700 |   27789   17116  7830885   457.5 |  0.565 % |
c |     25776 |   29220    81700 |   30568   25776 12693138   492.4 |  0.565 % |
c |     38750 |   29220    81700 |   33625   12745  7008530   549.9 |  0.565 % |
c |     58211 |   29220    81700 |   36987   32206 21026723   652.9 |  0.565 % |
c |     87408 |   29220    81700 |   40686   27744 13222109   476.6 |  0.565 % |
c |    131200 |   29220    81700 |   44755   36115 20717915   573.7 |  0.565 % |

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/6967/stat): 6967 (minisat+_script) R 6966 6967 4419 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841293566 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/6967/statm): 174 3 169 147 0 27 0
[pid=6967] 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=6968
New process pid=6969
New process pid=6970
execve syscall for /bin/sed executable
One traced child (pid=6969) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=6970) exited with status: 0
One traced child (pid=6968) exited with status: 0
New process pid=6971
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-chnl50_60_pb.cnf.cr.opb

[startup+10.0057 s]
Raw data (loadavg): 0.93 0.98 0.96 1/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) T 6967 6967 4419 0 -1 0 3358 0 2 0 949 14 0 0 25 0 1 0 1841293571 14512128 3264 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/6971/statm): 3543 3264 145 145 0 3398 0
[pid=6971] vsize: 14172
Current children cumulated CPU time (s) 9.63
Current children cumulated vsize (Kb) 16296

[startup+20.0063 s]
Raw data (loadavg): 0.94 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 4962 0 2 0 1929 23 0 0 25 0 1 0 1841293571 21069824 4868 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 5144 4868 145 145 0 4999 0
[pid=6971] vsize: 20576
Current children cumulated CPU time (s) 19.52
Current children cumulated vsize (Kb) 22700

[startup+30.0069 s]
Raw data (loadavg): 0.95 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 6556 0 2 0 2908 32 0 0 25 0 1 0 1841293571 27615232 6462 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 6742 6462 145 145 0 6597 0
[pid=6971] vsize: 26968
Current children cumulated CPU time (s) 29.4
Current children cumulated vsize (Kb) 29092

[startup+40.0075 s]
Raw data (loadavg): 0.96 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 8026 0 2 0 3888 40 0 0 25 0 1 0 1841293571 33624064 7932 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 8209 7932 145 145 0 8064 0
[pid=6971] vsize: 32836
Current children cumulated CPU time (s) 39.28
Current children cumulated vsize (Kb) 34960

[startup+50.0081 s]
Raw data (loadavg): 0.96 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 9463 0 2 0 4868 50 0 0 25 0 1 0 1841293571 39571456 9369 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 9661 9369 145 145 0 9516 0
[pid=6971] vsize: 38644
Current children cumulated CPU time (s) 49.18
Current children cumulated vsize (Kb) 40768

[startup+60.0087 s]
Raw data (loadavg): 0.97 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 10820 0 2 0 5847 59 0 0 25 0 1 0 1841293571 45117440 10726 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 11015 10726 145 145 0 10870 0
[pid=6971] vsize: 44060
Current children cumulated CPU time (s) 59.06
Current children cumulated vsize (Kb) 46184

[startup+70.0093 s]
Raw data (loadavg): 0.97 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 12236 0 2 0 6829 66 0 0 25 0 1 0 1841293571 50909184 12142 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 12429 12142 145 145 0 12284 0
[pid=6971] vsize: 49716
Current children cumulated CPU time (s) 68.95
Current children cumulated vsize (Kb) 51840

[startup+80.0099 s]
Raw data (loadavg): 0.98 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 13497 0 2 0 7812 73 0 0 25 0 1 0 1841293571 56066048 13403 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 13688 13403 145 145 0 13543 0
[pid=6971] vsize: 54752
Current children cumulated CPU time (s) 78.85
Current children cumulated vsize (Kb) 56876

[startup+90.0105 s]
Raw data (loadavg): 0.98 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 14550 0 2 0 8796 81 0 0 25 0 1 0 1841293571 60375040 14456 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 14740 14456 145 145 0 14595 0
[pid=6971] vsize: 58960
Current children cumulated CPU time (s) 88.77
Current children cumulated vsize (Kb) 61084

[startup+100.011 s]
Raw data (loadavg): 0.98 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 16093 0 2 0 9775 90 0 0 25 0 1 0 1841293571 66686976 15999 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 16281 15999 145 145 0 16136 0
[pid=6971] vsize: 65124
Current children cumulated CPU time (s) 98.65
Current children cumulated vsize (Kb) 67248

[startup+110.012 s]
Raw data (loadavg): 0.98 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 17557 0 2 0 10754 99 0 0 25 0 1 0 1841293571 72671232 17463 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 17742 17463 145 145 0 17597 0
[pid=6971] vsize: 70968
Current children cumulated CPU time (s) 108.53
Current children cumulated vsize (Kb) 73092

[startup+120.012 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 18682 0 2 0 11736 105 0 0 25 0 1 0 1841293571 77402112 18588 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 18897 18588 145 145 0 18752 0
[pid=6971] vsize: 75588
Current children cumulated CPU time (s) 118.41
Current children cumulated vsize (Kb) 77712

[startup+130.012 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 19671 0 2 0 12720 112 0 0 25 0 1 0 1841293571 81453056 19577 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 19886 19577 145 145 0 19741 0
[pid=6971] vsize: 79544
Current children cumulated CPU time (s) 128.32
Current children cumulated vsize (Kb) 81668

[startup+140.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 20454 0 2 0 13708 117 0 0 25 0 1 0 1841293571 84656128 20360 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 20668 20360 145 145 0 20523 0
[pid=6971] vsize: 82672
Current children cumulated CPU time (s) 138.25
Current children cumulated vsize (Kb) 84796

[startup+150.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21085 0 2 0 14697 122 0 0 25 0 1 0 1841293571 87244800 20991 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 21300 20991 145 145 0 21155 0
[pid=6971] vsize: 85200
Current children cumulated CPU time (s) 148.19
Current children cumulated vsize (Kb) 87324

[startup+160.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21688 0 2 0 15688 125 0 0 25 0 1 0 1841293571 89731072 21594 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 21907 21594 145 145 0 21762 0
[pid=6971] vsize: 87628
Current children cumulated CPU time (s) 158.13
Current children cumulated vsize (Kb) 89752

[startup+170.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 16687 125 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0
[pid=6971] vsize: 87864
Current children cumulated CPU time (s) 168.12
Current children cumulated vsize (Kb) 89988

[startup+180.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 17686 126 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0
[pid=6971] vsize: 87864
Current children cumulated CPU time (s) 178.12
Current children cumulated vsize (Kb) 89988

[startup+190.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 18686 126 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0
[pid=6971] vsize: 87864
Current children cumulated CPU time (s) 188.12
Current children cumulated vsize (Kb) 89988

[startup+200.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 19686 126 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0
[pid=6971] vsize: 87864
Current children cumulated CPU time (s) 198.12
Current children cumulated vsize (Kb) 89988

[startup+210.019 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 20685 127 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0
[pid=6971] vsize: 87864
Current children cumulated CPU time (s) 208.12
Current children cumulated vsize (Kb) 89988

[startup+220.019 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 21685 127 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0
[pid=6971] vsize: 87864
Current children cumulated CPU time (s) 218.12
Current children cumulated vsize (Kb) 89988

[startup+230.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 22685 127 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0
[pid=6971] vsize: 87864
Current children cumulated CPU time (s) 228.12
Current children cumulated vsize (Kb) 89988

[startup+240.022 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 23684 128 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223104 134555673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0
[pid=6971] vsize: 87864
Current children cumulated CPU time (s) 238.12
Current children cumulated vsize (Kb) 89988

[startup+250.022 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 24684 128 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0
[pid=6971] vsize: 87864
Current children cumulated CPU time (s) 248.12
Current children cumulated vsize (Kb) 89988

[startup+260.024 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 25684 128 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0
[pid=6971] vsize: 87864
Current children cumulated CPU time (s) 258.12
Current children cumulated vsize (Kb) 89988

[startup+270.024 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21970 0 2 0 26680 131 0 0 25 0 1 0 1841293571 90873856 21876 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 22186 21876 145 145 0 22041 0
[pid=6971] vsize: 88744
Current children cumulated CPU time (s) 268.11
Current children cumulated vsize (Kb) 90868

[startup+280.025 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 23180 0 2 0 27664 137 0 0 25 0 1 0 1841293571 95854592 23086 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 23402 23086 145 145 0 23257 0
[pid=6971] vsize: 93608
Current children cumulated CPU time (s) 278.01
Current children cumulated vsize (Kb) 95732

[startup+290.027 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 24137 0 2 0 28652 143 0 0 25 0 1 0 1841293571 99835904 24043 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 24374 24043 145 145 0 24229 0
[pid=6971] vsize: 97496
Current children cumulated CPU time (s) 287.95
Current children cumulated vsize (Kb) 99620

[startup+300.027 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 25438 0 2 0 29632 151 0 0 25 0 1 0 1841293571 105168896 25344 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 25676 25344 145 145 0 25531 0
[pid=6971] vsize: 102704
Current children cumulated CPU time (s) 297.83
Current children cumulated vsize (Kb) 104828

[startup+310.028 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 26369 0 2 0 30617 157 0 0 25 0 1 0 1841293571 108990464 26275 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 26609 26275 145 145 0 26464 0
[pid=6971] vsize: 106436
Current children cumulated CPU time (s) 307.74
Current children cumulated vsize (Kb) 108560

[startup+320.029 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 27173 0 2 0 31605 162 0 0 25 0 1 0 1841293571 112291840 27079 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 27415 27079 145 145 0 27270 0
[pid=6971] vsize: 109660
Current children cumulated CPU time (s) 317.67
Current children cumulated vsize (Kb) 111784

[startup+330.03 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 28024 0 2 0 32591 167 0 0 25 0 1 0 1841293571 115781632 27930 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 28267 27930 145 145 0 28122 0
[pid=6971] vsize: 113068
Current children cumulated CPU time (s) 327.58
Current children cumulated vsize (Kb) 115192

[startup+340.031 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 28758 0 2 0 33579 172 0 0 25 0 1 0 1841293571 118800384 28664 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 29004 28664 145 145 0 28859 0
[pid=6971] vsize: 116016
Current children cumulated CPU time (s) 337.51
Current children cumulated vsize (Kb) 118140

[startup+350.031 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 29487 0 2 0 34570 175 0 0 25 0 1 0 1841293571 121790464 29393 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 29734 29393 145 145 0 29589 0
[pid=6971] vsize: 118936
Current children cumulated CPU time (s) 347.45
Current children cumulated vsize (Kb) 121060

[startup+360.033 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30024 0 2 0 35559 180 0 0 25 0 1 0 1841293571 123981824 29930 4294967295 134512640 135094434 3221224432 3221223024 134556966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29930 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 357.39
Current children cumulated vsize (Kb) 123200

[startup+370.033 s]
Raw data (loadavg): 0.99 0.98 0.96 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30024 0 2 0 36559 180 0 0 25 0 1 0 1841293571 123981824 29930 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29930 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 367.39
Current children cumulated vsize (Kb) 123200

[startup+380.034 s]
Raw data (loadavg): 1.07 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30025 0 2 0 37559 181 0 0 25 0 1 0 1841293571 123981824 29931 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29931 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 377.4
Current children cumulated vsize (Kb) 123200

[startup+390.036 s]
Raw data (loadavg): 1.06 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30025 0 2 0 38559 181 0 0 25 0 1 0 1841293571 123981824 29931 4294967295 134512640 135094434 3221224432 3221223024 134557196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29931 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 387.4
Current children cumulated vsize (Kb) 123200

[startup+400.036 s]
Raw data (loadavg): 1.05 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30025 0 2 0 39559 181 0 0 25 0 1 0 1841293571 123981824 29931 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29931 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 397.4
Current children cumulated vsize (Kb) 123200

[startup+410.037 s]
Raw data (loadavg): 1.04 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30025 0 2 0 40559 181 0 0 25 0 1 0 1841293571 123981824 29931 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29931 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 407.4
Current children cumulated vsize (Kb) 123200

[startup+420.038 s]
Raw data (loadavg): 1.04 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 41559 182 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 417.41
Current children cumulated vsize (Kb) 123200

[startup+430.038 s]
Raw data (loadavg): 1.03 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 42559 182 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 427.41
Current children cumulated vsize (Kb) 123200

[startup+440.039 s]
Raw data (loadavg): 1.03 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 43559 182 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 437.41
Current children cumulated vsize (Kb) 123200

[startup+450.039 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 44559 182 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 447.41
Current children cumulated vsize (Kb) 123200

[startup+460.04 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 45560 182 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 457.42
Current children cumulated vsize (Kb) 123200

[startup+470.04 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 46559 183 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 467.42
Current children cumulated vsize (Kb) 123200

[startup+480.041 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 47559 183 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 477.42
Current children cumulated vsize (Kb) 123200

[startup+490.042 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 48559 183 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 487.42
Current children cumulated vsize (Kb) 123200

[startup+500.042 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 49559 183 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 497.42
Current children cumulated vsize (Kb) 123200

[startup+510.042 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 50559 183 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 507.42
Current children cumulated vsize (Kb) 123200

[startup+520.042 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 51559 183 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 517.42
Current children cumulated vsize (Kb) 123200

[startup+530.043 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 52560 183 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 527.43
Current children cumulated vsize (Kb) 123200

[startup+540.044 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 53559 183 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 537.42
Current children cumulated vsize (Kb) 123200

[startup+550.044 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30028 0 2 0 54560 183 0 0 25 0 1 0 1841293571 123981824 29934 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29934 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 547.43
Current children cumulated vsize (Kb) 123200

[startup+560.045 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 55560 183 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223104 134555967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 557.43
Current children cumulated vsize (Kb) 123200

[startup+570.045 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 56560 183 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 567.43
Current children cumulated vsize (Kb) 123200

[startup+580.045 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 57560 183 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 577.43
Current children cumulated vsize (Kb) 123200

[startup+590.046 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 58560 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 587.44
Current children cumulated vsize (Kb) 123200

[startup+600.046 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 59560 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 597.44
Current children cumulated vsize (Kb) 123200

[startup+610.046 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 60561 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 607.45
Current children cumulated vsize (Kb) 123200

[startup+620.046 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 61561 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 617.45
Current children cumulated vsize (Kb) 123200

[startup+630.047 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 62561 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 627.45
Current children cumulated vsize (Kb) 123200

[startup+640.048 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 63561 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 637.45
Current children cumulated vsize (Kb) 123200

[startup+650.048 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 64561 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 647.45
Current children cumulated vsize (Kb) 123200

[startup+660.049 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 65562 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 657.46
Current children cumulated vsize (Kb) 123200

[startup+670.049 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 66562 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 667.46
Current children cumulated vsize (Kb) 123200

[startup+680.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 67562 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 677.46
Current children cumulated vsize (Kb) 123200

[startup+690.051 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 68562 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 687.46
Current children cumulated vsize (Kb) 123200

[startup+700.051 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 69562 185 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 697.47
Current children cumulated vsize (Kb) 123200

[startup+710.052 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 70562 185 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 707.47
Current children cumulated vsize (Kb) 123200

[startup+720.053 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 71562 185 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 717.47
Current children cumulated vsize (Kb) 123200

[startup+730.053 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 72562 185 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 727.47
Current children cumulated vsize (Kb) 123200

[startup+740.054 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 73562 185 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 737.47
Current children cumulated vsize (Kb) 123200

[startup+750.054 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 74562 185 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 747.47
Current children cumulated vsize (Kb) 123200

[startup+760.054 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 75563 185 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 757.48
Current children cumulated vsize (Kb) 123200

[startup+770.054 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 76563 185 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0
[pid=6971] vsize: 121076
Current children cumulated CPU time (s) 767.48
Current children cumulated vsize (Kb) 123200

[startup+780.055 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30498 0 2 0 77557 187 0 0 25 0 1 0 1841293571 125906944 30404 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 30739 30404 145 145 0 30594 0
[pid=6971] vsize: 122956
Current children cumulated CPU time (s) 777.44
Current children cumulated vsize (Kb) 125080

[startup+790.056 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 31241 0 2 0 78544 192 0 0 25 0 1 0 1841293571 128950272 31147 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 31482 31147 145 145 0 31337 0
[pid=6971] vsize: 125928
Current children cumulated CPU time (s) 787.36
Current children cumulated vsize (Kb) 128052

[startup+800.056 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 31906 0 2 0 79534 196 0 0 25 0 1 0 1841293571 131686400 31812 4294967295 134512640 135094434 3221224432 3221223168 134559697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32150 31812 145 145 0 32005 0
[pid=6971] vsize: 128600
Current children cumulated CPU time (s) 797.3
Current children cumulated vsize (Kb) 130724

[startup+810.056 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32550 0 2 0 80524 199 0 0 25 0 1 0 1841293571 134332416 32456 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32456 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 807.23
Current children cumulated vsize (Kb) 133308

[startup+820.057 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32550 0 2 0 81525 199 0 0 25 0 1 0 1841293571 134332416 32456 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32456 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 817.24
Current children cumulated vsize (Kb) 133308

[startup+830.057 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32550 0 2 0 82525 199 0 0 25 0 1 0 1841293571 134332416 32456 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32456 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 827.24
Current children cumulated vsize (Kb) 133308

[startup+840.059 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32550 0 2 0 83525 200 0 0 25 0 1 0 1841293571 134332416 32456 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32456 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 837.25
Current children cumulated vsize (Kb) 133308

[startup+850.059 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32550 0 2 0 84525 200 0 0 25 0 1 0 1841293571 134332416 32456 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32456 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 847.25
Current children cumulated vsize (Kb) 133308

[startup+860.059 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32552 0 2 0 85525 200 0 0 25 0 1 0 1841293571 134332416 32458 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32458 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 857.25
Current children cumulated vsize (Kb) 133308

[startup+870.059 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32552 0 2 0 86525 200 0 0 25 0 1 0 1841293571 134332416 32458 4294967295 134512640 135094434 3221224432 3221223024 134556757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32458 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 867.25
Current children cumulated vsize (Kb) 133308

[startup+880.059 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32552 0 2 0 87526 200 0 0 25 0 1 0 1841293571 134332416 32458 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32458 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 877.26
Current children cumulated vsize (Kb) 133308

[startup+890.06 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32552 0 2 0 88526 200 0 0 25 0 1 0 1841293571 134332416 32458 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32458 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 887.26
Current children cumulated vsize (Kb) 133308

[startup+900.06 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32552 0 2 0 89526 200 0 0 25 0 1 0 1841293571 134332416 32458 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32458 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 897.26
Current children cumulated vsize (Kb) 133308

[startup+910.061 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 90526 200 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 907.26
Current children cumulated vsize (Kb) 133308

[startup+920.062 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 91527 200 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 917.27
Current children cumulated vsize (Kb) 133308

[startup+930.062 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 92527 200 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223024 134557256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 927.27
Current children cumulated vsize (Kb) 133308

[startup+940.063 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 93527 200 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 937.27
Current children cumulated vsize (Kb) 133308

[startup+950.063 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 94527 200 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 947.27
Current children cumulated vsize (Kb) 133308

[startup+960.064 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 95525 202 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 957.27
Current children cumulated vsize (Kb) 133308

[startup+970.065 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 96525 202 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 967.27
Current children cumulated vsize (Kb) 133308

[startup+980.065 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 97525 202 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 977.27
Current children cumulated vsize (Kb) 133308

[startup+990.066 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 98525 203 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 987.28
Current children cumulated vsize (Kb) 133308

[startup+1000.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 99525 203 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 997.28
Current children cumulated vsize (Kb) 133308

[startup+1010.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32554 0 2 0 100525 203 0 0 25 0 1 0 1841293571 134332416 32460 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32460 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1007.28
Current children cumulated vsize (Kb) 133308

[startup+1020.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32554 0 2 0 101525 204 0 0 25 0 1 0 1841293571 134332416 32460 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32460 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1017.29
Current children cumulated vsize (Kb) 133308

[startup+1030.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32554 0 2 0 102525 204 0 0 25 0 1 0 1841293571 134332416 32460 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32460 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1027.29
Current children cumulated vsize (Kb) 133308

[startup+1040.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32554 0 2 0 103525 204 0 0 25 0 1 0 1841293571 134332416 32460 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32460 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1037.29
Current children cumulated vsize (Kb) 133308

[startup+1050.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32554 0 2 0 104525 204 0 0 25 0 1 0 1841293571 134332416 32460 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32460 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1047.29
Current children cumulated vsize (Kb) 133308

[startup+1060.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32554 0 2 0 105525 204 0 0 25 0 1 0 1841293571 134332416 32460 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32460 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1057.29
Current children cumulated vsize (Kb) 133308

[startup+1070.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32555 0 2 0 106525 204 0 0 25 0 1 0 1841293571 134332416 32461 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32461 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1067.29
Current children cumulated vsize (Kb) 133308

[startup+1080.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32555 0 2 0 107525 204 0 0 25 0 1 0 1841293571 134332416 32461 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32461 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1077.29
Current children cumulated vsize (Kb) 133308

[startup+1090.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32555 0 2 0 108526 204 0 0 25 0 1 0 1841293571 134332416 32461 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32461 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1087.3
Current children cumulated vsize (Kb) 133308

[startup+1100.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32555 0 2 0 109526 205 0 0 25 0 1 0 1841293571 134332416 32461 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32461 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1097.31
Current children cumulated vsize (Kb) 133308

[startup+1110.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32555 0 2 0 110526 205 0 0 25 0 1 0 1841293571 134332416 32461 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32461 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1107.31
Current children cumulated vsize (Kb) 133308

[startup+1120.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32555 0 2 0 111526 205 0 0 25 0 1 0 1841293571 134332416 32461 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32461 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1117.31
Current children cumulated vsize (Kb) 133308

[startup+1130.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32555 0 2 0 112526 205 0 0 25 0 1 0 1841293571 134332416 32461 4294967295 134512640 135094434 3221224432 3221223024 134557277 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32461 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1127.31
Current children cumulated vsize (Kb) 133308

[startup+1140.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32555 0 2 0 113526 205 0 0 25 0 1 0 1841293571 134332416 32461 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32461 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1137.31
Current children cumulated vsize (Kb) 133308

[startup+1150.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32555 0 2 0 114526 205 0 0 25 0 1 0 1841293571 134332416 32461 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32461 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1147.31
Current children cumulated vsize (Kb) 133308

[startup+1160.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32556 0 2 0 115527 205 0 0 25 0 1 0 1841293571 134332416 32462 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32462 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1157.32
Current children cumulated vsize (Kb) 133308

[startup+1170.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32556 0 2 0 116527 205 0 0 25 0 1 0 1841293571 134332416 32462 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32462 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1167.32
Current children cumulated vsize (Kb) 133308

[startup+1180.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32556 0 2 0 117527 205 0 0 25 0 1 0 1841293571 134332416 32462 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32462 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1177.32
Current children cumulated vsize (Kb) 133308

[startup+1190.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32556 0 2 0 118527 206 0 0 25 0 1 0 1841293571 134332416 32462 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32462 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1187.33
Current children cumulated vsize (Kb) 133308

[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32557 0 2 0 119527 206 0 0 25 0 1 0 1841293571 134332416 32463 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32463 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1197.33
Current children cumulated vsize (Kb) 133308

[startup+1210.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32557 0 2 0 120527 206 0 0 25 0 1 0 1841293571 134332416 32463 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32463 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1207.33
Current children cumulated vsize (Kb) 133308



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6971
Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6967/statm): 531 226 485 147 0 384 0
[pid=6967] vsize: 2124
Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32557 0 2 0 120527 206 0 0 25 0 1 0 1841293571 134332416 32463 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6971/statm): 32796 32463 145 145 0 32651 0
[pid=6971] vsize: 131184
Current children cumulated CPU time (s) 1207.33
Current children cumulated vsize (Kb) 133308

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

Child status: 0
Real time (s): 1210.14
CPU time (s): 1207.4
CPU user time (s): 1205.28
CPU system time (s): 2.12168
CPU usage (%): 99.7738
Max. virtual memory (cumulated for all children) (Kb): 133308

Verifier Data

ERROR: no interpretation found !