Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 1007


Synopsis:        TCC generation changes the order of conjuncs
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Thu Nov  8 14:45:00 2007
Originator:      Hendrik Tews
Organization:    cs.ru.nl
Release:         PVS 4.0
Environment: 
 System:          
 Architecture: 

Description: 
  
  --oPi01Y3U7t
  Content-Type: text/plain; charset=us-ascii
  Content-Description: message body text
  Content-Transfer-Encoding: 7bit
  
  Hi,
  
  TCC generation changes the order of conjunkts. This is relatively
  harmless because PVS will never generate TCC's for a TCC.
  Nevertheless, conjunction and disjunction are not commutative in
  PVS. Further, when typechecking a TCC, one should only get TCCs
  that are already present and not additional (possibly unprovable)
  ones. Therefore IMHO TCC generation should not change the order of
  conjuncts.
  
  For theory Allocator (allocator.pvs) pvs 3.2 generates
  
  allocator?_TCC3: OBLIGATION
    FORALL (ac: Allocator, pm: (plain_memory?[State]), s: State):
      (pm`states(s) AND
        (FORALL (size: posnat):
           OK?(ac`alloc(pm)(size)(s)) AND
            NOT data(ac`alloc(pm)(size)(s)) = null_address
            IMPLIES
            disjoint?(ac`allocated(pm)(s),
                      address_block(data(ac`alloc(pm)(size)(s)), size))
             AND
             ac`allocated(pm)(state(ac`alloc(pm)(size)(s))) =
              union(ac`allocated(pm)(s),
                    address_block(data(ac`alloc(pm)(size)(s)), size))
              AND
              subset?(address_block(data(ac`alloc(pm)(size)(s)), size),
                      ac`memory_pool(pm)(s))
               AND
               ac`memory_pool(pm)(state(ac`alloc(pm)(size)(s))) =
                ac`memory_pool(pm)(s))
         AND
         (FORALL (addr: Address):
            OK?(ac`free(pm)(addr)(s)) IFF up?(ac`freed_size(pm)(addr)(s))))
       IMPLIES
       (FORALL (addr1: Address):
          OK?(ac`free(pm)(addr1)(s)) IMPLIES
           up?[posnat](ac`freed_size(pm)(addr1)(s)));
  
  
  which corresponds to the order in the source code.
  However, 4.1 (and 4.0 I believe) generate
  
  allocator?_TCC3: OBLIGATION
    FORALL (ac: Allocator, pm: (plain_memory?[State]), s: State):
      (FORALL (addr: Address):
         OK?(ac`free(pm)(addr)(s)) IFF up?(ac`freed_size(pm)(addr)(s)))
       AND
       (FORALL (size: posnat):
          OK?(ac`alloc(pm)(size)(s)) AND
           NOT data(ac`alloc(pm)(size)(s)) = null_address
           IMPLIES
           disjoint?(ac`allocated(pm)(s),
                     address_block(data(ac`alloc(pm)(size)(s)), size))
            AND
            ac`allocated(pm)(state(ac`alloc(pm)(size)(s))) =
             union(ac`allocated(pm)(s),
                   address_block(data(ac`alloc(pm)(size)(s)), size))
             AND
             subset?(address_block(data(ac`alloc(pm)(size)(s)), size),
                     ac`memory_pool(pm)(s))
              AND
              ac`memory_pool(pm)(state(ac`alloc(pm)(size)(s))) =
               ac`memory_pool(pm)(s))
        AND pm`states(s)
       IMPLIES
       (FORALL (addr1: Address):
          OK?(ac`free(pm)(addr1)(s)) IMPLIES
           up?[posnat](ac`freed_size(pm)(addr1)(s)));
  
  which has a differenct order.
  
  
  Bye,
  
  Hendrik
  
  
  
  --oPi01Y3U7t
  Content-Type: application/octet-stream
  Content-Disposition: attachment;
  	filename="bug.tar.gz"
  Content-Transfer-Encoding: base64
  
  H4sIAErsMkcAA+w8aXPbOLL5rF+B9ayryInsSPKRjDcel+/xmyR2WZ7NTLn8uBAJSYx5KDx8TCb/
  /XU3ABI8JHucZPe9eqNKLBJANxp9obsJapRPXjz7xp8efF5ubOD3y831Pnz3e/2XfWpXn2f93sv+
  +sbmZm9z8Ay6B/31Z2zjWxOGnzzNeMLYs0zcpovGpfHC7v+rnxHI/2bs89SNV2aJCHJPrM5uvu5S
  UcCb6+tz5N9/uQa6oeS/3ttYA/mv99ZfPmO9r0rFnM//c/kvLzM/ykSU+XHEdnY6nV8iP2Nb7IBn
  PLufic4yy6aC5diK98zi15ylIuQA4rJ4zG5i37M7e2LiRx0mB27R107nMPIY4ut0Om/jRDgH/o3v
  iRT6L6YiTu4VFIBF3RBa/wmSiHiGDctslsSAHaST5QCxYkOjuJtljlcgeSPCkLOjOOFBYHFomMUp
  gNtwxdmPrM92Yf6Ivd5mITsJZ4EPUICFMYXCQnwW77LI7jJ9Hdr23PkVnEN0TLI6CX6XfYA2SQJN
  9AEn94mOypyDLvNtnLegq979gbo7xEKTd8DKQ5ydJm5wkrEQwICRu+fESGBs746p+98TwQNommT9
  uy7+vZcdnxLiHPayP1iCnPs8lwWjOJs6qcmFvhMIYMTh27e7tOYQ1xyxk6MjyVM5XWhjs9EQzWcz
  IZ4FeUPGcjFyIV1aapXdhB4G0XTfG7fA6G2zlz0vmGtwE3j7Lg9HInHOknjWwlwQVpxkfjSpiKRb
  wzFnVZFEnYK8G5qDywIz7LKKFtOa7oByDouJQEMsoJ3bQHwiQovb1t18HpqzgYDSpr102ajLZl32
  scpDzl6zmVZLamFg8zDnCIiYUef3AIPiHcHdx/kkjGDm+fN/7LIE1LzLrqvzJ4BUG8G1XSfkoxar
  7H1eHQ73H2wkTQ1nQGjZ/WGBZQNDHU+MHeB9ndBRIZIuuytolY5Ej0mgIYw9a2TbWyScEQoHJJcQ
  ow7v/DRLLc3pLRLqiPgIK1hIFPxvk1yNJtAdzT/tSHBUnX1KbQoCicIHVUl7vcwPm27XNyhRwmwh
  xoe1fpDyBHYUrdRiOkcYQ3p+jf5xgXLDGGccxHHStguQIY0q2wEh5d0RLpjgLP5i9AD+VATjxZuM
  wsoRa38xMvRmTn+OJIlgt2H5mikuGX1VknJqtEqAxPkVLS7aBF2P4PoRNA2eTFNDu74aTWBJc+Xq
  Gvo2Ulbn2oVBPoVn7LFEtTCrlaw+/B88lbZ+hThsGTxMYehH30SWKy2yXKnL0qCgz/yUhbk7ZVOe
  eAIc/Ei4PE8Fgz0v9CfTjBHIYydgK30a74/JT7k2+C2IT3oMLF+iA7xRnGHguog/5LpU5Bhl38AQ
  v29ZB7T9Kaq+vvhKqooIYqEJ4oYDzZ6z1tgEtU7P2XXkptfHGQd666MWupEBC/boKAY6iEEPuE3J
  oflmN2pjjDZr3GBLkRSt9kJzMuJboiDI/qSyYPw0qmxq8wWEWvL6kXLBUfO3o4UkqS1ezcNcu2AK
  GRWwiaNhLeSLMnOKk2BdqT8KhHOxv4/cgS92Ogr8CccscrFEKwhaOFv37y3BhDRD5LCLOQVvY61a
  slyUUsbS3Re8cBcEGZSFDJxXBZE6jnyFCAcbm4sX2psfRxaxQ480Y5v1FqNqaKBfMEbigUCqj3j8
  xXhG/mQiGiGTyqEwKzIJlKYE6lnmztKOKLl6kOZEeLnbFHAzPJMip0avxZi+h1YZK7vtJjQqlNnt
  eg/qLwmV/jxBdwvgRXYYSUaWi5CliArtRO6c4gPb1snLyZHiP2ShEex5uv0wgP20gIbtMrSLLsA8
  los4UuHxHQxA7b9jL0DZsGt7zmcB7yhmns8yGVIbCm4ZiRJ8gYRULrtSZkedzvIy/FO8nefepCPo
  ulXdRDDW5teNqE66fz3JnshuhYgsiFOQ3SE3KLz47ewQAD/pcgL7A4KLSJYxdt8dkBQkyGdEN59N
  AEXBYv9PalcBpznQKXNLZp1BqxXFkQhn2f3OJRB4VQaVjL2LM3Zm9exqiQs/gNY6Q5bgxRsejjzO
  rLJkAlARbM24Ez/H/AWrIWb9o4MSehNPyjrI8rKshCBDJ1l/RFWkuwVVJMV8MhzpfZxsyiMnzIOG
  ERV+CCXzKWFNdGhQUvKk/VjXAcoHGBHeYYoBArdQxfp2ZeJJEt+mjh9Bfu9HfiaC+4Zrhkm3WlfA
  yjlVEm/w704XFwC+L0tKWqWDCKYVPIMFa8k9adJC7NanSOtmc9rP5sRWKRkk0tRqhbT50XW5UTei
  Oh0C0w5LF6+NfhY9h63ms7lQ4OscWdYE9icm0O5SE1xfF5imJAGVFnSUdHXPz26Em8VKfy/fSSqu
  2hX45O3Z6fnFybtjNrq5fHelVzQCFD1n7IPl6UVRE1YOoNEac3C/tjm63xzd16OzJNeDBVBao1DX
  xYciS1X98PJC+qMr+Prp8PT8t87e4fHJOz2fLuZegJHzIv7FllRklxfFKkJBdsy9MpOWTWA10Ih/
  bbs2OI/AR/VbxtvIqzcnh8OyjcbS7ms3UAyaKEYPoiDfuMwsnmfxSiJuEzBUJtvgs5TmI1igIz7m
  PFhiSwTryMZ+7X5tyYCTHYEYZ8WoBPPGpQJl6keTQGRxtNSYTXmsVrBKH+F/zKSP+sCOMG+jMNlQ
  2Ss4BUl6B5DDduS2OHfXqTBNVfBNUCmgEUbb85HMY0eFugo9bVQWUy0KyOdKZd5c7tPnktjJ9TaX
  IzFQJyClbATSkAdwmViKrR0D5ItiL+eWKCnW5gEcg+YHkFfYMAf76AnYFcvjMeRs47FIROQaJeBH
  yLYEk2kwBPmVlkWqVY6E2dMPMeQITqGnuqUyBekq/n9oQYXR1zcuzbLK0orRwCot7UVcK6hN78NQ
  ZInvVllW0s5VAli2jBaSX2AO4yhuhMt9gB0Y9Ue5JdRXI4fJBFq3SRBqq1M4kD3V3Mvo71Mx5xG8
  kJwvpbVIjWT5xOCSW6fAGF9VALLq4qmpsbPCZvufftj+v/CD5z/cOAKZRVn61U9+yM8D5z82Bht9
  ff5jrdfH8x+Dlxt/nf/4t3yW2UREAvwHK7SAcbAePOsBqSREZH7kBrmHD7154k4hLHOzPBHMEzOI
  aEWUMUhRUrC5Y4WnDLarAJiAaZCWuVoesleTUXqgnDozaBndZ6IoCHRUAl3vlXWHVw1AfFThhzkW
  aXbv/Disof1xu4mNpuB3Vcy6HFgZuagAtYeTzy0M7Enc71TC51zgYRsI6kQQ31p6chs5l3FYALBn
  fgUOn7erRLukel6CRumV8Zj8VbmLU/lJYYAEi7HdXy5OnfPD9+cnF4crRZdzw4OOTAOg5TZOPJNJ
  A6u/aVd6cXyZI2iQbba5sbG2SSPfSxzzmYEQNWaoZOY9TSBwy9VQcHfZ3yxyo+YiEFu3Qp7cQpRK
  w85xDsqZYjZ/gnQVh6O0zr4VoQPt8EUPog53f8Vb+NrBuz15tyfv9uXdvrw7kHcH8m54QnfDE9kn
  7w7k3fBM9p1JnPJuj+7g3/4Q7/eHeHtA1wdDCSah8PqIro/o+piuj+l6SNfDIdF+QohPzuRCjt7s
  ypHyihr3z3sOw8nOezt0O1C3A7w9O9g7RwD8lt3rqnt9ByjFGQ4uaAR+Eynq/ljdv1H3b9Q93iEG
  vENqfxsevrs4PHdwyUh3eb9jdiuGmffV/pNaP60ZxW4IG0S/63kJ2tNPIgArbzu8VnospTDdKgpQ
  OYmj1MnL78jrQWQNbcbgLovHYwhslAF9dyVtXMPvo99McqwgpFLtLHM8xvp66DazjDm2SUVL7Nv6
  6jtbSnQBJMrbhOxpoMFCoEE70PpCoPU2IFSlOVAwiBSuAUUmMR8IdKdlooMFEAetEIcLIA5bIY4W
  QBy1QhwvgDhuhRgugBi2QCCImIT4ELrQxYbK0kbxiRuY/6CyA7D5NKGrg+LqsLg6Kq6Oi6vhkM4X
  gkaCGTUnqs2BTtXi/1IrsAkUR+BhUT0KMzv/d8EqR0ifY3KAzVWz4Oy9n03ZpbIcG7nA/6U48pwA
  rlRMkaeWQUtXz/GprKjSUwIN/bk6kSrMLJhtxZgNa3WJWkCVM3O3eWIJgDm6XmYWKSyFUa7I1vzD
  pwHUoRvmYpc0Phq/WlKBvsLQh5cQ0pJhhv/KvYlAVQT5SVRaiD/xVAYCTfbInLaqFNj+mhXp7hYb
  xXHAUAH6BjP4oLjBpBP6FOGvsUte/4NQbX8Bru0SmWTFMA4FS5StsUkS5zLEPT7bsXyvsiUU0ymN
  wqgCxthoTRhTFNf7xvWBcQ3RhL5WyTOGFCWKM2OovK45BGxjC2mCrVfjOBga6IrLo/LyuLwcDovp
  YGfLkjh45HQQeWgcGHaU1+vFNcUfGvsFx+MKj8JNUUlBq3nzxry5KJG/HZ4/jNaMUorlm6FJs/Gk
  FMZygZpsgVQFtMfBG0s+y6wahd1KUM037fMUgnwYeDpWikFxLAVb1Y3Z95qhA85rw+7RVbAYTj0M
  25o1se/ZuomqDDu/AJUm60DHj0/B9Ypwabs5/gq4FKo3X4SqX2GXxPSluBSyenj9xcKsB+RfEeHJ
  lyGU7jRIhUIMPsjr6Kcwx8oki8/Kj19OesOt2k9F26/hrfnPJ+MtGUOnSTRL8BK9xYLyhh+pTfxP
  Hn6oQQ5aIYshc7ydEabVPS8eyDN9pW0Ek+2HV2rIHhHRKRy2arO4bV/JXLKWPUI+ebK7NphbJHtk
  iax4dN1Aj/yk97SAzVx2go/n9ERGt8Mic6zUyXdEMJEc5alz63uwLF24WRvoolfgR4InTiUvNfRH
  Q9qV4RW2YZrawDS/UtYY2qgXVUnaZuuDH9Z/2Hw5+GGTqlTGEDoAYoKXe5caYhuLWRvY6v0dFY6W
  HKTSExv89xoMG8cJy6ZxKtjtNGaREB7zs0ZC46wf13KaWsLzR5kIvG4ui/IcIINCYGd9YmEKfHZ+
  eHBpVYxBL8O+korbIMKwh3NLP1tKQx4EIs3YjE+EDNHVMSS816aA7zUMZGWv1Cpo928EEAxqGwEL
  4sRTI24Fc3nEeJDGzJ3yCDBlUz/Fw30xmM1IH35garzlj+WAlN+gkrKxuEX0g9ENqv8N6CaYf1oW
  D8NmbdHQv8qohs6EqshY0RWAeHu7qNbYVJdG1VGhcGYJ6IHly5OZkuXq+Apm2fI9wHcH8Pd1ixJS
  kahSlywW1jV0o9tuHEqmYES+ixblguSBzRaekpdisg3PMhZo//QkDQ9cpCyegbiBeJASvuvp3Uc8
  BER6HDQCvyexlCOMIMBCAXBaIR35e1CAGPTKzXBYCAAg1ES4yGGOeAS4OA7/P+aYTnIWxBkBoosj
  8oGnBInPryUEmuGMJzwUGP2ifo0AYYgzReMcH82iQwSf6hT0mlU2tZWBo5nep74LSiFNR7UjO2f4
  KMDCMoNNtNxwP8B8oQFS4LrxkyxvaYe8BAvNkNf70dQHfQevC275xkdpYAqN6yMu5iksJnkRk/3p
  Z5rLlGXjCXzcDpTZdlmBf5YKcGiZiNAsim6cdv1yHWcVEdE9xEkriCl+AeahxCYFOp61ozv75eTA
  glQXskhbrYfcAs+yxB/lmXyWc1cgv3izV+Xq8mzSpJQ1Ua8h6kkQj4CXRG/JfMCExU/aQ1G6fz27
  /TYffP4LNpMH2Td6+Pvsoee/g97aWs94/38Dn/8ONgd/Pf/9d3yW2d9PPHxnVatA94b1V9f6bADC
  etF79aK3BrnG1vraVq/PkEf4sjP7e2cZAq3dHKKgZIv9BBtL4l+zC+g2mt9CZAtB3T9jiE2N5osP
  PLmGrWKEr4dZrk0zsXPujeKcfi6A9v3snqY4J7rU02iMu/afP8eNH2MbjA2KnYNKhukqxn8Xpwen
  FF+zM/ApYw4IXhzeuWJGv3GQiABGe0ydBiYkFMK5geBRPoOYTkT4WpmPa5Ef7AIHjtuguONuFtxj
  rHML0TnumWHsiQA2Uiz5ZTDKd6csEDcisFcZOxPJlM9KVLCj3cPWlQce7GMAeiP3XV6cYsnw4Kig
  IGoVz4fKcI67uKdvsYPdi108HqpOhSLGc8E9mf3j1Q61vadyLbbRlWw8vBNuTlVcdbXTOYSApDJD
  hxiIMZmiB7iexCE6bggs/BsgDTYCWh3GdTI0KPf1OALWZLdAOQUDPE3zUMhB+2dvWJ+RvPByQOMj
  QJQw+gM7oreql1tO1brkYbmrbhk3cpm/4NbKVEEEbyrLLDDXWOvkmV85u4D3oIVsnEcuKQ5qX5VX
  LT8LUOUlCOdXp9JmZAQzDLMhZrysDLiCtKA42+R5lhIV1sD1ITQUs2132cz+jDM8YQJ1BhcRSTQy
  1TC4kcUO7tmpRakcpR1VLJhVXMqIAf9eqddWLIWa1K4LMgY6VVOxEgyi6VQGToAzVaa29KMGiXws
  Mneq7ux2UorK7ZhJWHxfRlf/xgqD0cZYhbF4o8it87gohJQ1IrZofFk38cf14tIjKJmHzpy9NqY5
  Y/kGUCO1XpY8b7DcAeNh9cOESZlLylF0mB+naMVhteqPRQnTNohcnclrmFwHY7wkiRNnH9woJV+L
  f3ijZsbdVpzgd48cQWhdREu5q5EWEKvAuYHjEB6e9XFu/DigalOheeZnWQbAtJfg+8bS5wtZLSyd
  VeWz1aRV1o+kndY/W3VLVlVn3OpwV2gMpwRTRsn0OyY1JtIPxahNT6+/dm6lwtgmPC67QJGqjS3k
  91gcwNc371nsunkitwHBrkUSwT6IDl4OBQevag1xnE1h+BT6gGmraAuc2Bjg0wkPNtViFkJJW4vC
  h/KTVS0qJVCZAJYRMBLvKu3zY0g641tcBSJM5RYONNF7cho1IZEU3/qAzKR6Sx25XzFX4sYzX+9/
  L5hO2opEB0en95FL2IAv9HSG1CTDBAbnw/jDIaWx6EBSUynJpRWjdgrxdtQEAf/9nqWyZgzZMvcQ
  rTplohNFqbTNxh3AoH/jxlQEelfmq30oTIOYMJGh2hZxMCnDtraoDWG+IgWdcvrLIcaCXdJ0ZfBX
  zRii9v5PESY6RwGfVOqrNROSYlGrO/1Zij7NXVVwoUCULEAN8YAMADn92aIuCFYkedguzREV4PRn
  9fMFaBLWPdaUwbtgHGzaBv7mAf5UV5LkM1k12RPAW0EML0dJI9OVEoC4ia8xxqwMCiHrgV7CUky1
  ynYzfXdPACcHF2hxWcIxJgcsVIqeUu3FU7EzilfiiXMsPhAjVUgNNgMkuFPhXhvAwAr3GsyKQ2ho
  EuLqw00YCLKS9Rb5QXGnvVhVJtKpSs4r/lYct+zx8gTdg3RMBkvRHZAbt03EO7rmWQpE+S5jH6Ah
  hoWrYt9szAsXrQ+O6K5isDMGRUuV7ZctNW+gDyzKCosfIYPQYYIrIMUD2ilhIJo8P6Hi6j2BAIBE
  gkagrw2E+tCv4ULkcAv8osvBcaZxKEaxd09pToqilCyQlW9b4fn1119ZOqV0Bkt2hiOfiIyKf6ma
  GJ+oFSTpS4OiRGR5EklvW6q57NvN1C/UbcldQFmXUh6gN6efAglD4fkcX/CELUZ1gwQVEuMDMDPI
  TcgskhiAWYw5jNIVUPcoBbUOQef/Jl0FEGdF4i5zKnqG4sKuneKt4Ns4gTmJf27C0ymzcvnaqcB0
  b8ohykjoEBjtYFvyWxk/7ojRCiw89CNZCQXhTMBKyvwWRIBPImBzE6AMOXKJlPcnHuFbuviFRxgh
  2yk94jfw9sMszB7y9mVO/rWdfTn745x9JcipbYQPe3Ma8i7OhE51/RRfIQv8a+l4l0pOr57+vFQ6
  sTgBNx/jIeoY5XYD+wLhWkLfvwTB0SRH9qxCzgThkI9jIBnDsgJZE0FkWHO/QcFzhoqBj1+Iy0u4
  5CWpNhmZKpsFHN/NUmENikCpT5eJ1ckqk3k6aA9EfvTsAh8QFtltF3YXiW4sy+wZlYrxqU0i+DW+
  IgIMzMWqbWxnph0Ue9gSASwZqirTG9TTPexqwlKzBtcz/U97X//ctrEkmF+Xf8VcvKpHbijFpGxn
  T7velJKX7EudE7+yk9va8rn4IBKU8EwRNEBa0aur+9tvunu+MQMMQFBSEqFSsQjMR093T09Pd0+P
  v4VvxddqI/KLbEfIE8K2r6k3WMBuiFZmppdmKiTbvMw5RVbJRbryN3kktNHiOlll/6DtBEczVtMT
  gm85V1yIgtgRmjTvl6iegRMfEmeQxnuTc36CWPw5tlWe4evJCZI3AZ23xMaFi22dojYN5gNtEeNr
  wRXf/6W4qKv3AyERNzlKVt7WLREd/XD/CQALkyCWnJ6wtxmc2brgS/dNUixK9vfd9abE7cAKDFDQ
  vSm+gKUINK0JyE63eDKeA5pdZyu+0QSk5vmmpL6gc5cqiHP+k08tzpVAGCglyVLyicuX9SHI3ZGH
  MmPalKR/4soS7+gDMDbIKXAMbqVLBFiP1//cmfD0ErQpNY+NGTgmJ1UihB/sTlZ8cHzVlJtLbI4c
  xkpQwiwGPpGWJT5nSTFB7YgGo2U+7YgEHWmVwZGg74sayn5NFwIszgif87LnK04J8tSubseGxBa2
  x23yIRWeN1r6sLYUSuzztwiFIVg/B+LQW5c4uNyphDRURq1pejjX7hLmUEeh7sM6vzENixnIUPLK
  S7EkqDK8woOEKIcXpEd9rrQCGOKaoYtZtJKv0U/5ZypZFSHig4D9p2hlfMx3aGSxNdbd+1dhH5RC
  ojlQmJjNXTvu6ilj0IJcpiraQCMU2UQ3Aybmn7WmBgtlUmQqYIa4Wqq55Xa3XPKF8NJU7mb5h6/H
  GIBDMntHjgHUAtCoLDpCGGjnaumGtu8BzspZX8UGjON+KyMgxNAsqJF78wtOCC6lb5JbMLKhnY0r
  JBDExf/Fn8nFmtaVLRglvBtPLH4uymEllPpbnDIpZA3CEt/k221+TZpcKrzFs++uL9IFnvLDwIcT
  rmdpFJCi5VWxhIEupBJoeKrf5YigFMGEVi34g1JHGxAMBDwz+jn7ZZutKlAFjYZWQwyYdqa1+SGF
  DFSG+14HzuD8pGhZKPxa5peVo4aSkOlDhuPZY3a/qrFiKhFptRXhdWrc5kjV6BWVAqpvEAN6GpmL
  wdjXVQU/YLhB0eIzsvixhFUqaELtqoIOLSSFfBwzL9qkiEKsyZdC0PgwGQw3BOBm0xlOxhmnZ+t4
  RV8D/rBFt2QELqt8KDD7w/cwo7CFEaUEk3ildyqclS95HgqKOjZrOjVTKRsEJsmT4DRWcvbBaezb
  hvnZAas0zhpjd+B+stV+96upyZMG75YwFRdSWNwSllJw7ywKCNuLRX0N+FnULRlB3yYWhRZcFsV3
  NSxq1HFY1K7pY1EtM5V8fAwXinwg/gfxfGyoJT2HAtXH/3w1fTqZqvifyQTuf3n2bPoY/3Mnj4j/
  8bIAhgI9/58UCjR5+uXpU/b0xdn02dnplH2CqJ67jQV6lS1RlwG1G8wieZlJC0vVcMsVWGN3MItU
  nyjjGmw0N4a/Sin6qOdbSj4q9hW1vjTiR1Z0UQcYQGB9Y7sNbfOrdYRvynQ/uVIN5DWjfG9vhXVS
  aBTwSijEXMcP6BfvhbyvlA8I+/euDkP6wrCsXQW8Sg+vM3KXGxLtDa151yfZmv/g6oeZCQIzLyeR
  GlRlQBClID82tW6CVGndO0DZeiPs9qoYHodHwfMOyVOuTf/BkXpWb++gPeVq+xfGDmvgqPy0rjEN
  5wALopaFcIujyewEVPWIj8S3hN7i8qjxujWaxtuGlMHhBunskhdMPjXyFza0CJVZBuR7vWD2SMja
  TlxpiRha8W7IzL817XU0tclCOzS9ACSfAhJVxp6Bniu2HnWSg5qf5R8Ux4lwK9vtoISJDdFIspJu
  SdQz22JOYyLnHP/haw6Sz0GQgtWqNNXY6QQ9MBLZ/c2G9zfWVFWVI1FizTin55Gea0jlRJ2i054z
  +PAOafc5MMDnAcJ+TgiB0kM4HqSrNTEE7XvP3373li30pvdCGn1wjyj3hrsNXGhxJtjnQuxyfvoz
  Vq9jJADHx0Y2pAJtu83Xw4Wa0HpYOJKXknfzm/VwIdFHNmJsS3pLDI8uuUvg4+dYpDQ8iexzkALk
  RuFPhI6Brq6cGTW8BZvawPo/kGtFOTKykg9vDO8kYGhs3gAmFmMyiur35Ydss4FAGPD/EFzghsjW
  mx2Zn/PdFv5ETlJ+BtDmkuv0RKo38doVL0/GRxJR3lLQKpJLiFteYRTenlvsVwaNlSSot+LgFjLd
  q7ffYQUPCyKlZ4tUOrZ/I0RHe9JY2Y7AxS1MRUGGIPNegCmgH/GanMvgAQAzvTArAQx8y0CW/EIu
  KkdmSAAbIlBfSpi+JHhGGGUFIO3EObwiRX8+tvn6f7nNQNDAL2W63K1UvIWmDp/LOlTTDMOCE5/k
  jyQnv+vb/1K4zNVEPxkxwxPqnQXYnHcmyHMYeGoi4fu5rREd9LXkaoOrDsXgfvOieKla0uV1g6LR
  Nd/KynapEfXGKEgTqDKv9FwK2jI7gqLa2Qsar+20I0SiLflK6kMtoPIII1sU4bKunZ+uBqe+SLUg
  /bXibY1T6EyT75iVlCkAlm7ZckwjuNaLw7nkB6fKMC56IVtbCwf6sJ73RS4ZYc2Wl2gK17cFWUMT
  ytw9Igv/+rJNbTBpUwoaIHhYaW5oRvKeoTg7+09LOaxRRr0bt4Dy7HRhEpWZCa5+wngPq0WHAUYV
  F0+wMUtrNUsJHUwYtQfqoH1ycQFLSSJD19/+zNRFJVHL63feCkHDkHDS+/ZkB4gg/NY2371VqiWu
  L9rf3nvwIEUeWNZDTpEEluYnT9gN3OPAF7KrNPmUwfmGT2kBQfcQkIzpDZJimy2zOcVL0U2ueGJe
  nd0zTxWibZDXK8ELn6zoMHsG98WWOwz2geOElxA+e3PM+YOPPF0cl+nHHQX4rsCFv005RLSci6ih
  62R9C7CqyAs6ODcwUDp7C6p+OlNorbxovc0OcYZ3h12jM1DYVEiBRmVuCwrIelEaUVOolgi/Wy5D
  gD/usiKV+h4ePBR5TaidCp2XGE+ndzFySyhU0Eid9TZLVxy25DLB5AaquS6toTVl0mq7gPaXVuZb
  kxycbTiu4CaC46Qs83mGAWJSX4TjNRgwAPtlEQbOS2cf5KCG5QSaKKcj+AfDBWdSecQin0QIHwcU
  Sw7LabUkGbFuMCgLyIvRgBKFCfv8WxUAWiQZqMMcFN4c5a8ASqsUFJsE5hwc8yn/Bwz1yRMyUE3G
  AlFNyxCKZrW5wvJYX9uwWs2qQcMshCmTLvaahTqIquoJaM9OqIG7PNV+Hzagk2IJDBcU/mxFJwd8
  TGLQyOg9mlCifDs6uXh36OR+Pqi0bN7vmwOd7EOWjuJCERLjaeFiQZjJ2ZKdnGD0N6egAaAx1aI2
  btZsM9qh6h5qNlKniZp9z7o7peBBZujQpCynKiMS48upj8T2TI2ms5ysncjcMGkFF2hVcQa9G79N
  oCb0z1STG2HsyavQygc7QbIuzRr4Gmo01Z2+l6Q0fNNAuRXd7UenCvW3kVgU4c2Y+qzd/E5t64pw
  XgXi+HDbhW3K7ZVlbakLmQp+c+OoLFu5EVMs3kgTE8X6GjgRu+yv48zpR+SMn4G2SG5B/F+TF651
  HV+N8CYRv3LiarLJi0E1dapuecM8Y5rD7O2nIpryT45MK039YwQOVh2fhkUHTDjeQpJBLLJw7a5I
  ubLA1b11fgNpBbfsA2cS3AQAyrimeoEBFTDdPvHtc7ac5R8s1ubj/PH82zevY+aRTFdhYzmoS4TF
  TKNYqrzZSzC1hM0vqqo6Yp2sghpVHSKIWZ+AMn4NOUEv0y2Yro3dmSmpJmPqMk5UURVTCg7lDR2T
  0ZloaSTsXN5pqSckgabmpfKQ6z40YNXJOAnMPy0tsbYjJ/eUlAFZ6ZOWsfIyQmK6kiyEuMr8b0Si
  XTpapMkmHauyVwZNAkIIh1PSnMJKxt+WmJZeaNx+ONeSGSTWZcDA5xl+U6fCv2v162mmcvGvhK8K
  R3OXMp6gdadqOfH0KmIMvO00QoStdQJJw+GHid75gWpeBypv4hRU7zak9TKgheK4wSjQXjU1Xdge
  1dSv9seppspa5mimZhxgoPnWmim6mX4rmmmk2mFsho54H2j0lB5jsiAzpdAgGdEEbb1y9D7bFh9m
  80i2ZSLPnQqklflWWAz3ouHQ4t8j1pqDsZH4KAzUWKCO4sY4ZjxyFi7BjjLNRJUhLY+0LNaRF2V1
  hxvla5Mf5btmjjxyVsQjFi0Eoy2g/SrD5kE2zRAh02gkQ2ilt63O64mZ0nguo2xHEx3uI7ZLwtgS
  tWEPh0MQh1qSzGCSvSSjrMt1LVsntUTcvzkmKCQIl0lw4huVjqG2LsI32gPEbQFMdFnxxTsdIvOX
  PMHD/5fZfIz5NjfgTbAyiYqjuJx5tyq9ETYzxPwZNqQjmSxbHImuMRSY2g0awUztptZgUFfT0rOZ
  FVzuRO4yg/qqDKqkkghqZ97Qp1chdRsJqqMuBM3d+ZXRxg6NFc7pUSmilTYaYQmooY3AaMXTB41Q
  QT3gxDqfmvTPikH14cteNBfbAthfOEImK4EjIxVntmeKfMum3FG9xwufmSCvGfzejhSRHqlWtGtN
  PHXNET1tuS9ueWvhG5nU+DT0Kj2bsnYLtevcoEZillpmLzf7erBM5MW4Qn5f1N+X9lpK7C0mTI6w
  BUALliAhoNpp7eiyhIH+alZ9Q9cwlq09mK2iGMbxfOCOJVy10YvbomrVM+hZdGK8tPvE3yRFixqn
  bWo8NN+x2dDp3k7o7+Ekye31Rb7K5ujI2YlkYTKhfuKPzsP4JRm0JO6uESp4kV1ebc8wy91ABCrV
  RSoJ868OW6fbTbeQMjiXDYj4JYpW8LaimrmgLKx6LDLzDwcdXcgL3CpRHhbK2zNBQLE23iV2amWH
  SxOI9uM7yTTDzfoK+R1OL6zz7djItv+vIkRLgI3pQRdpoRv/rixldrczSoos2CErRfrlJSbgAm+b
  oC+kN9waJc0ErVT8pHa/ImctkkpeHIucbPhTBHdjhBh1A8RCAFAtplJGMRF7YBRjHaCYBqEwo1Lg
  hcHxI+mmCMBjFu0A02ktTLM49JjxGUbZDuA8iwXHwVAzTHvi6bkNmCkkm9jIKdsPL72oh6eBoZpB
  2xNdXzWD5+UtP1wB/uqCt39tBVgc2upYjRmR7UGFakApxIVRs0nl8pi9uzrs/Yr0fUcXBZ3kKu5i
  JrtwbVDSsVCxQfniWZyXbkgKWqRkMuMa2mBCwdcfRBYzVq8d4zK5lfHfupYKp79Oi0uVBRBaqsRx
  wmm2T5BFX9WWoJhdzwSbzCw+MfOzDawUdd6uGnXxoIfIrtmAwfZ6u8uxjAkVVzKtsN3BK8KGeDc1
  X075y4+6bhOHzqY2e0MVajyGv2fI4IaDM1Tdr8DK6qiplaI+3kaDhcTUUWeO4NexfkLzSp+5/2hY
  V2VOga9thno/HH6E2eI79S4SjHyspgj46BznV8bLj0F7ZatuyYbp7dg04Ab6NW22td3AD7v9dJXK
  XMOkYCrTrD765Y6EvHG8l4/Q5kfKHVaZxyhRRCajM0j/mm7FVabiQkrhK1ju4MLJwY/JB2vqvpOZ
  cc9DU9/vDYXhXUNbHHwjMxDdR4zhbcm8yGsZ/VyFtr1Cx/sQU1tKJw6e9JcZKuTdtSX1aXT49ddq
  B+F+GnqzF56/19CJHZTviQH8KAB6Ia9kwMT9pbpaQGXwT8xkSlgWSlqwf+Tt1MHwyzrbvtdDEbc2
  +Idy3iRy+IDQT3xkEIMIaQ1MdUKZEmFu8IVJvcUTtvL8ISSez7aCkObrZDRWNYwbKTbLZFy5dAJP
  S7oja6yk2/feLDE2WvRc82B+du5SoAvWtQtblHM92+I15gY3R46JwWU+cM8XVVMmXTTHLjhK5j03
  Lq+gK1zWC0jxhffR4pFNLE9mAH3QGL80stZ5JF+1mi0Wb3VnqqQHjnLo1IZJnKoPgEMUf4CL2BXu
  uDYcHVknBFB3+xYSPROBQPejP6Tyx4wlAKrTMgB/4f+AUAAXZEJg+tjuE/rIMDmL4jDSV2T778ey
  0G7jFHkny6jiFCDDSz95rzuHJdA/HF3mCPNYy4Tzcw3tyclJDT4CSJF/nDZih9H/AyczPICyeTkR
  ypmB0woE72XhabCwhvK92TyUM8Y/hA7H2BAmZQj3eUphQ0Cq4RNB0Zdi9jI9fWcTaIe39zfMyMNb
  pz+4FqQozQS1/dWHOCjRKYl71iByoJfdhvcxhI75X2a3YAAdyTaejGIYx8s9sGi7ogzQc/7ezuOg
  8X/+vsJbQlHDIu9YlbE8KpfDUQYzVea2W8A/ugA3idpK45BJA2BWMs9UHHmVKRo3XbYYt1BUnwCW
  X6omyW5c4KLAnGVhDIZsIXXFg8vDEr+OxGfixdASIdYFrOr/ZtfX64X72OuHUUWtIJ4qht7B7PXC
  94g1xGzduwTJ0vhxaX62R6MWGrX4GJDBN4lJtQIJIPl8QsJY0qwqn+jLpb1rJtbyM1NFfhFjzvl0
  x7tUzDXDzzoG70iJwwyRwygRts3385JECu8E/pbSpEZ+mHNblwqVmE2983/MvmkjAoKyxdP0+5aE
  +cZdhAPkaaSP2VAdlTxkuuD1vxm1o9bFqAPBZlNdTgh983oOynZBPrLUuAwHi4p2qlvoJkrGSXRR
  ahlhZqItoFkLd8AZn/LmVjJqL05tGVLXt69FYVKOHNzJbUaGokbP0e4dGZKQhP9Sbgpc+S/VYxm4
  rIKLu+wHWFXCVyS6lI6+jaN2087hkjMS4tlSXPlXEe+ejoP7Cd/W2qwY3kno5YJKpqbchhf2jKly
  98BOTv2DvLrmXYDpq0Yj770dVmZqw0BpmDYrWZYbbJrCbpku4AoyTz5IO4M1FBbGOahDEY+lurbb
  07tr8ynCd7Eow5JzEYsbck/B9tCxEfEsC1VvZgkWVde0/Fzs1NVl1uUNHYYaOVB4qrfUaGOtCfRQ
  BBoBhMYlSEESmTcgqfJfiwGMrdL6Mg+Rz4yyjCq5Mma23cMzapWciymgR+z8pz9b/Qw/joC3X/2g
  MsB5kauNzMZIKcF6yL5OJxW9Qybkukb3bkMUULdCLUdCFGJ0OYcjCBtCxjnYsxjkIy3jiKMf8zWX
  a+tsTkepvUjzo+ua15w5Ikab3AXezO+glFi/p5oXmp8IyaURD1cephzT9d2buGxBqtlUHyl18dyu
  oYk8mLCWGalc6RlNDWzioZKjHU7ugSqIvSZuGYnljzw9qxXjLEZXPN4kt5j7VbXcjnZ8s7C9ssgV
  ABd65Z0KDDsCZBBsn1PeyxkifEKmUIyS3RUxbbsLmxANd1SuUi5weF0hrGzHXxuRSeQA2K3Rifxw
  mCbXImH+oWlZO/iqVsOilruWDwvv8qPVjEUvZzBI91hOX0tYHQJjFy932M6gW65GONrf7ToUxne0
  rKtpYhIOI/NiWO0JqoyFXyj1F/41VVqvo8JKdFRrRKAAjCP29G+NAhf18m4AnGOgIOM6EIuW38qS
  W8sEd8R6sQtsFcv3tHjZ4LdZtmrE5ABLD1yzmdrvh+wAs2koiE0awcTBVbr6HfJmQkiavGtqiaHi
  62PfHVOVm0G9AIybMqAdwNQgjnP1uFfzx4EddsNGB8NEuhnOPD1u3zwY6rL8t8LK3jpABR+1GgGW
  Nnb+Br56HqOPGOx8vRCffdYHZyieKLYA4YLzfzY9QG5tHLBpbTwTaX1L4zrovvNqVzqtmjK7JFu0
  A1MrncTFyGK138dRt9bxwPp3m6qVN33FIbc7VdqePDF1mw9gergueHRgjzjrStip/dl1Zdlf/ct2
  cxEQOd5U/4835v4hH7j/9zq95lplz5f+Gk/t/b+T6eTFixfy/t/TF8/g/t/p9KvTx/t/7+IR9/9q
  FqBLf5+pS38nEzZ5evb86dnpM+vS38H5YgGyDr2Pda7KH85P6W7KPXUMGZKeUL/sYpXPP5Ty9b4K
  jDT0go0X9lPUCQSa87/Yv79kCft3+vsLvjv8BzgERZkZAjLEb2dMYGWMhfjvdbJVTkHxTaUNMKPC
  6dPItA9AlqVZvsSW4bSC+m0qqoxDu+RAi1IcUPmblPFKMV7GriLGQ7gVthE4F0A3LwBOsvViR9e8
  XaSr/CZkL7HwMSPbjz6YIXX2WjwhtNJq5MHvF2xCNUZOuopq2TGbiKHVXL/qBXnq3WVqjnCoOWbN
  Q6oblCjPhzYaa77zbC3i0KJbgFHTJJktsvLvebYWtScusBOCduy1TUGNqVtjqlnbsKSbHDsZsS9f
  Wm+mI/a6kF0QHF+I7mF+YTev3wzsfr8Q3YkS4WRZzkjVH559IyMAx/6hTdwRSgoipP/BnsLsE0Xg
  l0snP8pV29in6EJnwIXHrmGTWNbXBDY+qubCjO5ip7y9vk63RTbvDT3ths3q0SVLUj01+EHT+LL1
  bJUUl1zhBTm+39D8s6H2CcqIGDlQJTFIAS3pwzUVXgM1W5FGW3sdvo6EIIg0eUnWPNWy1MfNCg/C
  5iWg3yRZcZOVqRrGkD5IVL9TpOS0I/Nv1ccH7c/EkGcV+s9E17MAc6vqVBhRbH2ayvr2Cv3T65/9
  NNBtSZB0A1X0Uw32UkIvxRC+o2pN86OCxBlvK7jc+de0MWtCvM12IcKZOBJm/WHudpv71lJFj5zW
  TyykrfteVNMIeFmzijK/+kV4FXJeeWg0N5K4aJa8VcwXXOX+lN4b8qPHTHAGh43WTXMvwF8NfsTt
  RCicEU/10I4D4ykgu8B1vpavkotyWySocPJy2RY+c7LiiXzIwomn89BgorL64T2B1gldSsaKPyHV
  jYi3kT3wBnh5dJ7stnithG7qS/Ki8BarexmItB1box17LCmM9bjdESDriwX72/EQlYxjZ3AUi+Tl
  uyeCMaj7GeLdes6Y5D0wuEcvlXU2+m9u0Us0trsmSvu7pjq9AUCB1ByA6uBnkFpplvIljKPKgmCV
  ldt3CPqYVpwYaOqg0A0GkGHBcnegUFNP3qscJUa6h821eGHxFIo/8UE3JfZd4r0AfsCklIOXXJgN
  5IHvv6roY7iOk0/ovEyV9Fhv02KZzHGiJ1u2yDGv1RwutE1F+KtoBlNdJ+BUOGHDMk1Zsipzdi5k
  zewN0PiXNdVc0KnQzTWRfidffy3FrjVK9yguGyI2rDLmodyq88q2ABhHYcE5trn+m8GHQ3GRrSoj
  /Wm6kuHW8tYFbQGEdI9CitgSSNynPcabTtmaCNDjbM1XK8ijDBLs22/Z64tVdolZIbq0Mg20AlOO
  iSm3LNIU+VmsQgPmb4+jfySWzYsVXZA93xVl9intU1zJzRSFxfP5li9F62sIWjwzEmqIMw70FdLF
  DS/GrFhZVqehORRzBJg2w4S7fsxklJgvCq5xyBgKFTzPYPFJyh3k5E7Xl9srKCRMUJvN6lYg1kS6
  SLNX8DW5hNvr+VJ/nfM9RYZ32ldgqeA+HpEhUWs1OWZLLkBSEynqyNUKWFHLOwu9zYwit7k9TU2U
  YHc5M1WH+0zMSiPt5iVUHzBvYwauadvQflrGrphCl/phSUsbGIu4BryuKhcKJmAnBYN1hO+WTqsY
  AA5rR6dtguyYbnq0xyYb55IBKwcZlh4tQ5TYEBXtu+NomvOJMXDrgTBSUiBbmiLAsD/j5DdpKpZt
  mbXLQ1QPQeMJZM34ej5RGGwzz13V0Z7pUogE50MFMI5PEpiWcQvUhJgx4OpPPGlF4QgZjEmYYtsZ
  CaODoHufIsvcc1iBZlxvo7xtRok/URrWfiSbacBTAWrSiFdxEpF+aUGIWihtUre6NYeSVoDU5tqy
  2tXHh0bE2NnHzNpEsn/3Kyd36bqjFGwVj9JHzgFWTFRFollHKPKLT1m+K0W6XRGsyIKh7iGEzUzu
  qPUtqaEZQwAZ65kAkdQJkmZYjwfoVeHCjHnvMHpe2xcKp4CUtkT6oUKzDUu0Orlgm3MrVauxerJG
  HLpmk5EZkBJZqc6LEcQKHajaBy3SbkaBy/EDtKdr/Bh1vZexOCLQgtTqV220jC+1QhiL9CqF9xWy
  pFx3l7J3LWa5LuBX8eipSOCQ4DW2bOOLHmRvFY8ziy1iTNeVkUUL40YqtpPG1f1sJ4nsw8kDEslN
  SPPL5MZafUsXU8O3pvZA5t+vKnqW1RMs+KF9en+CKHhYIeYARIM1dTAIbhJm1WN+LQVYa2HGepVm
  K2tfNGbzjfDGmj68gDd5bFiEQg7tet2zut8ig818E6la1JNiFuJJnwhoi5bWSHHdeJ1ZyrQsdMFs
  P6h9QKK0NQod2bofPaQeHBJyjzKis4wIGHbjhUQMMWahsg9KTHRgqyY50YjdntD7gCRFeyzWiYoO
  rUn1rLSUOKGWqH7q/cStFBe7o8md9TQ9bE8eRJsWQSfsNyhdK2TY00PfwkffRuq33eVGHrruKvTZ
  gaS+TY2qnA/uRexgAthG430GaHiAG8lyuORLXB0G/GPMWOGt0JEDdXwkT9c20s0eSWMWk/aoN87x
  NoWd1hLDvPo3iH7v+Vl0QdRXecl/ScrBKUArc0poaakljnxTu57Uz/9OaJcYjmMczSguHxjE+m0R
  sDWhAqs+O8yybyAikkYYwOunksKQjbHYhifhhrvyvL5lMSIVVYyQalhBXcgnxon7PefAxCDWnk1R
  CLxJpNYNChxVj3fFr4D26IwZBPEmUQ5oZ1TUxEQufHizAeqbKlp39i2OKBi0WxNgq7Bhx+56Amip
  q3H4bHIolFBb3rRR7vxNa6NcICtJhN/XG61iSCYCVs+YusiXX3z4OsO7UfH7MSSXS4qLjH/jqL4W
  SJPfLNdI6X9t4yLBaWaVMv0mtQNhV/lqUTIM2YAWRK/QtJUDj6tC2xPMzgYXM8kb1qzsMwIEN4Hb
  Kk0+kYKFueVLdOvwQpoqCrwBqwMVt0VyFppdOHYR88halwwwTelHPFzmBnnGpY+Dd677x1iaRdYS
  7ZR3AkGEF16Waihk5CwJ5aVxI0S8de1DbaEao5rTXHX8aCxhNTMsRieM6cOnEvZB9r2ZuEX22CgO
  elgMxGI5qD1ptbwySbs3PfbNamn5ILuybcgo1piTLmKVtOxVLdRtR9tuSAln8nWzfq7KdiHfbGo3
  N7C5tVOTE9vG11HCiWRndfItMv11cyfmFa7fv35z/uoVG5ZavjXZe876l2cRAq0mk5qkoS8TF2Pe
  /I+xiZhr14s+UkPae6tW6R/35tZeZ5MvqiO20boNZlRWSTcFgpfeoggow93pbe4a9nFE9DOH7OSe
  +zY23YeGdqOx9uiIADeg1PmapdcbvkoaNGSLnFMBrLXJbptfc0E55zS4xVuo4bhng8Qdw/0iya5M
  5eYGwkus2QyXkGAjtO0xPxqyeJitF+kG7o1c0x5rraAcnXRgMxqnyVz4RioSI/b6jXxjb1RsbWRf
  4dxFzbrLNK6x4zOzuprj8yV43R9n3ykTi7CsDFxTy+zUMraEs70WnKlgT8yW6Y1K8lrk1yLt67JN
  vlcHpN+WvQUdO/vuDT0tR7fbaj8YykJ6v5tCX4baP+AWsZmZItTwDqzUXu8OJrO9Y+Xbyzh7qOJV
  CTk7rYjIaZ09+i9pkYYN0HBEdLkr+PeClZt0niWr7B/pAu6r5W3wmniXR5lDAgpP7SGIVXHOnNJ3
  wi1tQ7Regh18nqxB4bjMZZq0TZFSlLWwkEudgnPIgMKwIRsW2yRFcp3CEVYU9wBeOsLhiHbANq96
  4f/xNhbgbebM9klem1eC6N9toWFWPSbGkiW0XzlrykuDJTiijj41Kq34HjO+otqY/ZgX6ewtV6Zn
  ryh7RuPCUr+yNCwQgx5DkYkzDBbSdJ+p8929nWz4GS6TyVer/AYWY8x+gnNVZihRcLXaMR2x+LB5
  eceZtVs7UsBpaDJx0iLbwtXoq91CeHvEYQI8pZ3zQeDdd3Q9G3QO40JlZUbglzOlqScnPqWRIA4M
  LmS3F2vvTeN5A/PEAZauhnNFIrqyj9H6ZP2BA+wWTmR4gr5Edh0qYumkVbNgtBruYJQu9Oh5t7qX
  eS6O5PruiUaKRTYoL0GZ5+s1xPs0tkNZh/zm3M7k8DZXb46OnCMBdDWYo2slh8WSrZBHuKuZXHJD
  DU5J5CYQgMZSbnkouyA63Ld3DvAtq+HN15WNl+b8rXxuYdqpp6cJiM8k7gWtWsuNdImqJOro7Gne
  ziqvDmXya1jWqnBE2Zs8Y2qSDJp1wDjURFBsawuqJeWjrGsvXq47BkhvJFRBkn7Mihvxx3VOw6yJ
  hWpNqXqqiK45LQQ0Zjxau7kgm/IEtMlx6UIKvGryxL15sX7EEpbIBJhk6XRJNTLa6fm8HWS6c3xG
  dE/QYTI33RRb/6ITYnVvYSdLjk9mV/U/N8DKum1b0KZtjFuUai0CK4UmZwRXqg2xxzzjkZpF9eqZ
  CkA1Jy+snB0CGICi1hjShP67Rz1vfGgMO/6kiRqyTK7S/sBrDSUVKbU0iokODLbYIvq7Ar4zcg9o
  NpdZMtHDZQ1MFWYomO11AWSwYKJBgT6RREpTkU2+Tznns+MY23kA4ktzYH3KPK+NsUN4YNw61TGe
  zTTv1NgIRHoKKbD22T+EW206sVDdydvGyRqbdWULDgkR2piogw10NFvXtAfx8OFAkdaxPoeJhFdY
  a8md4S1824bE1r0nQaF3mdKeelY1fR5WOLjdYaa7wBWHhbvWmhmhzWW2tYITIxDE6lWQ7KfM2dXV
  xgrDMG8NPEhvWhRI/qqo/LVZ0czmG/xEXkKhz4MW8n5yHDoNhvIdxjKS0dwdc1RPlG6+pra/Pr2O
  0yBfWe6saAbTSrx5WjEy916lMZF8T6wb2dLUr8Bwz+XI9ipd6+yf9DKahe5YDtF+uAdBEUo4FnGc
  OkoBh6eOk7qIxd/x4DtK6f0ldEQEbXDOQGVxiCZf2jMoW4shxcvimouLH2dTW8ZqsSj8fpEQP7tq
  V6rAKtV2lmHjLSaaitQ0ztWLTzj7yhyLrP+09SrkvHnpfRYxF/N8vcBjrCVLCj5l1yu4zGO1zFZ0
  gx3ceay8/OirFi5zMAxkaw7/ek4xdJur2xICR+VtiAxDTNaLIvtwRt7wDFLoYWQp3ZAX9AHW4Oqg
  okB5pC1HyO93LtQIhD8YKrxXyMdNenEhRO/JQ/XS+eQJ+3hwW1vFBLlfJvrm5lrs0WKaOw0097OR
  wFPbLfShBq+YjHEnWhDsIZZqODomvnsgZ2ZLD118ql7v/HWBNqPDjdldCa7osjOFp/vutNKxP6WH
  WSsqLFi81EG+AVHSZm8aH6Tb2R5Tw8c9zvEe53fN3G41TX+rU9Toes85W2vyueuV12ruENLjN6Wr
  tFPX2nhNbbnWxV/qy13q2U49AKm6v0QNSNPDaHeg2N2x2yQyN0TPul9UF/utF1Fd7LOONHbQcLgJ
  eCp8eS5TF4J3XSxayTcCwqvMdZG5sX7xSFXMgs4ToKuFjuHERvTGWHmiPM/Umrl62E+D+8IaQVX4
  1PYp1bee5M2akyJZsW1aXGdrdVDCc7qlR8GTLUVkXNU8bERFxfhUjKis/ENwo1UJpjLmnRNX1c0n
  13sIW9zm53CRc6HZUA0ACYXE1ecg8pHv7kln6ctdsdgU0di74twijq6Rn/6AqPgthBS2nH7BqdfT
  GhETz2Moq/0vGnsqenteZ9uxj/4V1moffWuszTHhhvwV+6CmUOVetNZeRJI2IyDoHdfdu1vs649A
  Ks1QDMZry+yk3lKDpnZbjbOsW/cjtFnRRR+JCg1wDj2zDz2rDzqj7382H0bJuG8VQytRfciXP44i
  dkix9+B0vLuSyPtLY1vh0zt0KxuxGbrVQTxVnC6mTAq7XDrIHsfK39IG5rGA3a1PxHaJDJxCd+j4
  EKktOmLBsPHFegYCjoHApOl2ALVZ0HjvQK/KVwO+FsqAtgv2vUGpa7mFAhPdbpzppvYIY1edosWM
  9i2U7pQKF63MtHZHraMFQXtAWh32CbdbXUYbrUb7ov+BbMBar8nezY/Rx55bJ7jBZd/ZfhgZcgD5
  cfeyo7tOUCtBatfVvlWFdluAgyr/Ebr/o5jdS8zuE6pSy7L3zKO9Hj3ovFd+QPPkQWxka+N5fpdb
  7MrOud1SXruMV9NwTgeDo6P/KpLNhgsT+iRCBCH+g/7ARfa///qdmZLziFJFHh3x/6rpIp2XPxsu
  UAo4nImWZQPzhC/DfCwic+RwDivqt/DSTCVpgASX8h0dVYmDmSjFEK2qUzQW/pjMi9z7fQI3YFKL
  QyvSiZ29JPAI4fNyxFH8N6MAn7QKEpMctRWxxEhWfDIiRAB9bGIMPuvtudhdfrlZJdlaLBonm09l
  f63T85Q/L549g3+/evFswv+dPJ18NcH3T58+e/ri+bPPJk+/mjx7/uL0xdMXnz2dnD57fvoZe9o3
  IL5nxwlRMPbZNr2pHXiZ946Xh/D8FWlPbPWO5hGjXLvMSkGOPCJtbXj3G10dCLldsuvrdJFBzd02
  W0GmSuGEbU4dO+3BCey4YqVLGEcmumN/VhAPenH4On3yBk1ESgy+ZO+eDIQE8Esgca0OrQcyRYf5
  ReQIc7N3iI83NR9zyCw8oyQ4qunGzOxP3lupe81RwQfRHXwSvQ2YNH/Cy3UCxla8Z8WUKqCAOolq
  jijzccVue5UtFul6bCQIgtL1GyeQn2MO9N+cJdtRxOgnL2ahJjYCkTpRbajkbfC3yN82qp40a6W9
  UhetDbL1MLlB8+00SIVaY4yDmG6xkNR4upEvAHMThNVTAhrGBrA8G7cKcEZP0IbVYKtRGg1ZjVQ2
  GJGMvSfv1vJJI1cE4rR+T3wvqBR1Y20taPW8Xn3Cux6AUqXVigJMg9ERCt8OR4JxiLW87/ZQN/jF
  0VPke++1PnTD6iF0Bq9J0lw3XYekJRq0amBYJ6urbtTNhDGs0ChfDDEb9jLFD+/mAQ7vpr/h5e4I
  +x7gvrpM2zFWV4r7omHkmhV2YfhHeChCVeyFtSoqlY5c8tuuqe2W1G5or7ZyZypDD8M7EGS2phE5
  97T+2pJH42JUwnp54FxvLd/2urm6SzXzvvZXjTusljziF9h3wzBe5Oy3kes2eveOiv1G33q/GAd1
  1K0VjdB23oweziYX0K/zNUM3jFLEe+28i6qG4DSgW224mqPD6idyKH1XswrR+/pfF9zXTR/sGZMV
  q0kXtHUQS3vjxZ9i3124yrviuT5wdxeL74HwXlmde0R8zxx6F9rnQdkbo6nuVKD2gfbIDVYYcQ0J
  ig+mrdZTs3qXiPnsP6UOQeyeJ1Tz+ZXupD3sLG0i7d1obuiUuD9NzYGEZhNa0xo4rpl3Qu4Wi8QH
  tqd5h/fQ1NEKoh6gIuoikqbmXXFJtAmy+1DuU8rW4yAOD71TuKJM34FYaL+kt54JhxMrFq4emIbW
  L9IfjPy5H/bsbIzsbagPVVjd/+5qj/n7EHdWdch+3FO1nEL3vpuKpuZvah/VsIk61B4q7Dy5v92U
  kwoSMRLrtu/GdM6KZjoVe/Et9SRXLIdId0xWojx6QGar7dtDxW+/vk1jRxQbF/UwubcvOVrxlOqE
  GabjjZJkZOtL1pnH79ss8bDYOly4kxQxV0BDovyecH73i/zBpZGfdI9E659u/U23qsZ5kPnWrH33
  upA8FDodYrU/4AT7g1KpYTb1ujsJboqcmKqHsDWyuOu+9MmYWLMeF8kD7oMf3i74PgndSo7cxwyt
  PVB0fzSrBSuwPwkSsyfDqEncNuknXKaJn88BpUzwDh7K6gGbh3Y4+lTWu8Ff1LG2A04tSO+He/Dy
  SwThHkNgTVYy7jpw8/CqFJdh4isK4J1I4mXt/BkSG9halnM1tKQIla29JM43LqJwzcDG7OIW4+Eh
  f1fXUeoxNQ0J4bHGRACIkUHWD/v0fY9ZP/QD+T84FvJ5ss2L8hDZP5ryf0ymp6fPVf6PZ/B9cjqZ
  POb/uJNncC6J/85M/mHl/ngLlycvs7m6e4c4mGm+YTd58QGsiPy7mSkE8vHwpWB+xZIS72vmyOZL
  iKqI6UPgfb6mK5gvV/lFsmKoAl2s0vJEpBDBpSEvttCHlbKEUlfoi1J10xlfMoplMk8ZXz3KrCRz
  5/aqSFHgwi3P26t8URIMNzk2scov8QZoDg/vG94wBolD9HqBaUSSFV9qaESqQ1Eaf6vS4isvSwgR
  hZYAhHrgl1VAlBKCYgNJMxiOTiB+WeTX7OYq43i1QNDdnfDiWcnKq3y3Wsj27OciZYus/HvO8UQN
  8sqUNIStsk9GqwoRsvUF1v9PXkgQNd3q/LL8TbJlV8knSN+Rro1KF7d4g7YXGNXZCful5GW3Obvk
  rULrEkhOEaTgPC8Kvj6vbv3D0v0ZTEQFN0X2KaE7nfivN+l2V6wB3rxUmC04t+VrMYhrLhvwqnKO
  KkPdrXQJjIt3g2tCcPhhSsDaxLfzq9sTg/CgqP0Dya9BSCmJCjJoSodhCIabjFOF948VOQr9YyaG
  4tMOW0quU8ooc8J+wmvKAZwi/bjLCk5WiUB/S4u/80Ffp5RA22Au3simSBcgBDhJdgVMROj0hKbe
  f6Us/XW+2i3oQvdNXpbZBZ2x533LNthTXFtLhplfhoizrBSuB7jeayv45DpZw/9wKq2yi4JTEnia
  97LcFciicjiIJBw9tnKdfODNJ+xTxvtfSbJJzHjGcsLe5hxdoi+SAbJDNuSUvOGSKyNO/PaLLwCv
  60VSLL4esUWOzHG5Swq+XUsNWMSMEzylL43HbzgMvKXeGoO4zV5gmNcxOW4IMgo6M7oQrc+TNfCH
  HlpyycUjV4PX6acUcLXC7KSIa2xL0Klk6fVmSzBxrK5FnqChlNYcZSA304JPGRAHl0lxkSwuBZ7n
  +WrFeYgLhxFygFpFfKmPlBA7Y++Glj41gkxEOieRlcXovchjpEfWqbo56Ts1YEzZQH1Rw25rlS23
  7/g8WCfb99jWQK4eZ6wBjO9+3ViZmcbsF17NRogflOB+R0DS1I8euzH4ELzeYQdhl8mlQir7EVvv
  VquZ3NfVJAfmnPntlzAXf/rl1SuYKTtYMTjLpkXBGZAzvJRfiClex2xZ5+GS8L+EF8OnYjfxhibl
  QojuLcgB2RSuhmdY7JiL1pvVrcGderarZRVm7ZyLl5IW2K1ewWE6nIiGflhqAQk1cEbyaTiHWR4S
  wbDaoKxO1fKezLlkB1/uiutdXDtYpW6PgPHbEuc1F2NbCcD3Rocl9DHPypSP7QauOzTYf5HLtfSY
  o4ncxlIV5HDDhsZ8BWvn+ljMP60gCGihMRRpQkSHBio1RGMYNTykyPR16/TSdtVWl+jYVVvcj+NW
  fda96nNvVV1GJYmTb95zxn+VXF8skmEyh0TW8oNMVy32x5gLzpn/3uTW1n7Y9ZcM5W6b5CiJI10X
  HtgbJ/O/Iciw0R6qu0dhd23Ktp8422CG1EDxl/aMd2GBR85R3SXwHbXjc424pvKa7pVF1qytL5MQ
  rVV6xXyg/hZHImeefsiYcj+g+017za2GIt95JUNJEONoxF6lSiv8NfRp9ic5V8QUiVXDy7ogK4cb
  00LFfvj+e7bbqK8kSe0yB+nWw/Jhlqs2UMXYIlsuuda+nqcd2Y4sXIv8Zl2LjO6EjxlFz3Rvb9Os
  JUWtsbM6mFBbHVHYqfdekOpaXo2eKvZUWApA/vNODdVedNoZ5bXG2LvCfCcgaggQ1B2UVjCDOTOz
  djjVmy78CgDqDEOtX4g7kLwXIcfqCHuKUTKaKz3mMAbz39mD+b8/lRfZ+suD9QFW/q+ePw/Y//GR
  9v8XT19MP3s6mTyfPP+MPT8YRMbzB7f/A/1/TD6kS75dPFQf9f6fp9Ovnk8l/Z+dnn4F9H/x4vmj
  /+cunidMUh/N2H/932+5plegaQ9E8+Dkr395/dN/n6FzYL5KkzXj0oL+WKQbXoB/OBv807bYpYMB
  /wQtlS//z+CfkotyWyTz7Qw2BuBXZPDS8jTCm4tsq/6eX/Hv6foyPV5l6zQpqu83V7d8BVLvhR2j
  PIa885W3xotPaVGCeVO92myO018Tvv6k1jteTjm65HuAf3u74WpGvkhVL4v0UzZPjUsT4CVYXG+3
  V9n6Ur35dQNrodk3jc2peZUnRSp/2J82ySVv8BjAOEYQSs8X9erqtgQHltO8e8OD+44rfRR9ID8W
  yXqRX89olOol2vXkL1zHj41AResDmODKyptjtx9ArPrxaZkl5Tw/5igDCzW8HgyAy475SDmTAefl
  64Qd83fHyLLHiAI0PaL6Mvl1wv55KNlwBHyZLhj8OL7K0iIp5le3JwuuPf5fBv8//nlTsv9wvh8n
  z044Y1u9VTp64e1oix7Tuq7cEv7O5isw7BWVXp/9OmXHK06acp5s0n4AEH0JQBDdXlTvi1bPMLdX
  4HPpYxQ1OOwTSYihgRSAZyQQBwP6xefHNTsulozUKfq5ZP9i/H1CIG7TX7fqM9/b8Cn1L3zWf+CC
  V1amNkm27tes+P3/AsowrP9vvjv/84/fHW6NaVj/ua5n6H/PUP97+tVj/MedPGAyvkzXnNExuIOM
  8eSRzosFnz/ocV//fbf+sJVRBejQXKFbcHXLrpLiGnyMg4t0nuzKFHUIdFujB1K2noJ1+k8lahkJ
  /A3OadNDSb2gG5INwOoPJlr5gq+O5CzIr693W/JIZmvo6oR9Ty7hMfkrBrCkzK/SOcajYE9jDC8R
  sRDoeYXYAv5B+Pmh8WQFdo9bcDyUKbluBtAh317itTHJim+B0avNq+/WfFP9CWILRhQpAsEZRcqH
  hqM0EUq9DhxHh4PaOUftYPA9hhGA5DHcqXqHDbN8BFKAnZ5MFVZJAzO9D2fs9TevfvjP859/eP0T
  31p///rN+atXvJ25YeIHO5W7pxehNGCtldt22rUP7UA3dYnZUDYNa5My6RvGmzqDvmoFnp9e/9zC
  nm9UdK9Na7Lr+804+1jH7YHsZ9YPG/X7t+nbYPds04+w6FcgOLRN3+hPMS6MVlt2+zPoy2hwkzut
  Tie+Xn19TkSnLp9zCGRwQQASqjn6N66wUKQYhv2Um5xrjxCTo8WQDBvKdwUGy3HNe/CX/AaE85g9
  O5lQ9Mmzk6fsB7iRKeMfRkr+3IH4aaBWH74XxRxNMi1WpHWVaBVCt5dn+wgGe1LuI8zayLI+BXCv
  gizGM+mIsX2lWG2XvDPLgv6gxAxJmasEwu+Us3BLMubk0RT/+Dw+j8/j8/g8Po/P4/P4PD6Pz+Pz
  +Dw+j8/jc0/P/wdiMahBAAgCAA==
  --oPi01Y3U7t--

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools