TP_3.ipynb

{
  "nbformat": 4,
  "nbformat_minor": 0,
  "metadata": {
    "colab": {
      "provenance": []
    },
    "kernelspec": {
      "name": "python3",
      "display_name": "Python 3"
    },
    "language_info": {
      "name": "python"
    }
  },
  "cells": [
    {
      "cell_type": "markdown",
      "source": [
        "#**Trabalho Prático 3**\n",
        "## Bárbara  Faria (A85774) , Bruna Araújo (A84408) e Tiago Lima (A85126)\n",
        "\n",
        ">O objetivo deste trabalho é o uso de SMT’s para modelar e verificar propriedades lógicas de sistemas dinâmicos. O trabalho foi executado em Z3."
      ],
      "metadata": {
        "id": "WVIkKsrEl9E-"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "#Enunciado\n",
        "\n",
        "No contexto do sistema de travagem ABS *(“Anti-Lock Breaking System”)*, pretende-se construir um autómato híbrido que descreva o sistema e que  possa ser usado para verificar as suas propriedades dinâmicas."
      ],
      "metadata": {
        "id": "KxTP9FuYmvV_"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "#Propriedades\n",
        "\n",
        "\n",
        "\n",
        "*   A componente discreta do autómato contém os modos:  Start,  Free,  Stopping, Blocked, e Stopped. No modo Free  não existe qualquer força de travagem; no modo Stopping aplica-se a força de travagem alta; no modo Blocked as rodas estão bloqueadas em relação ao corpo mas o veículo  desloca-se; no modo Stopped o veículo está imobilizado.\n",
        "\n",
        "*   A componente contínua  do autómato usa variáveis contínuas $\\,V, v\\,$ para descrever a  `velocidade do corpo`  do veículo em relação ao solo e a `velocidade linear das rodas` também em relação ao solo. Assume-se que o sistema de travagem exerce uma força de atrito  nos travões proporcional à diferença das duas velocidades.\n",
        "\n",
        "*   Os “switchs” (“jumps”) são a componente de projeto deste trabalho; cabe ao aluno definir quais devem ser estas  condições de modo a que o sistema tenha um comportamento desejável: imobilize-se depressa e não “derrape” muito."
      ],
      "metadata": {
        "id": "nRNWOvFXm8RM"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "#Exercícios\n",
        "\n",
        "**a.** Definir um autómato híbrido que descreva a dinâmica do sistema segundo as notas fornecidas e com os “switchs” escolhidos."
      ],
      "metadata": {
        "id": "7DtIzwIYn5gU"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "![265761633_1033390573898220_934360039585658853_n.png](data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAABOcAAAHSCAIAAAAojzhfAAABU2lDQ1BpY20AABiVY2BgPJGTnFvMJMDAkJtXUhTk7qQQERmlwP6IgZlBhIGTgY9BNjG5uMA32C2EgYGBoTixvDi5pCiHAQV8u8bACKIv62Yk5qXMnchg69CwwdahRKdx3lKlPgb8gDMltTiZgYHhAwMDQ3xyQVEJAwMjDwMDA095SQGILcHAwCBSFBEZxcDAqANip0PYDiB2EoQdAlYTEuTMwMCYwcDAkJCOxE5CYkPtAgHW0iB3J2SHlKRWlIBoZ2cDBlAYQEQ/h4D9xih2EiGWv4CBweITAwNzP0IsaRoDw/ZOBgaJWwgxlQUMDPytDAzbjiSXFpVBrdFiYGCoYfjBOIeplLmZ5SSbH4cQlwRPEt8XwfMi3ySyZPQUnFXWaGbp1Rm/ttxsf80t3NcspCxGPEU2p600rK63Q2eS2ZzVy3s23d4389Tx66lPyj/+/P8fAEeDZOWRl0f5AAAgAElEQVR4nOy9d1wUyfP43UuUsARJkpOCIKIiUVDEBGZMYMKMOXt3nuedeOeph1nPhNkTTzArElX0BEXFhCRFQKLkvGSQ54/6fubZ3+6yLLCwsNT7D15DT09PzW5vT1V3VTWtqamJIAiCIAiCIAiCIEiXRETQAiAIgiAIgiAIgiBIs6DViiAIgiAIgiAIgnRd0GpFEARBEARBEARBui5otSIIgiAIgiAIgiBdF7RaEQRBEARBEARBkK4LWq0IgiAIgiAIgiBI1wWtVgRBEARBEARBEKTrIiZoARAEQRAEQf6PxsbGkpKSsrKy6upqKJGVlZWQkOjdu3evXr0ELV1bWL58eUJCwujRo3///XdBy4IgCNJdoTU1NQlaBgRBEARBEFJdXf3u3bubN2+GhYUlJCRA4bBhw7S0tNatW+fg4EDVLCoqysrKEhUVNTMzE5y8PCEjI1NVVaWgoFBSUiJoWRCkhyJ802H8Ql5evry8/MSJE6tXrxa0LC2Aa60IgiAIgnQJQkJCFi1aVFlZqaOjY2FhQQipra3NycmJi4sbOnQos9Xq7++/Zs0aOTm5srIygYrcMtOnT09ISBg3bpygBUGQHopQTofxi/LyckIIg8EQtCAtI7RWa1NTU1lZWWRk5L17954+fZqcnEwIERcXt7KyMjAwWL16tZ2dHdRsbGzMzc3NyMiQkpIaPHhwx4lUU1MTExMjIiKir6+vrKzccTdCEARBkG5HWVnZ+vXry8vLhw4dumfPHjDzsrOz4+PjHzx40KdPH+bKoGOBvtXFuXLliqBFQJAejVBOh/VAhNZqra2tvX79+pYtW+rr6w0NDYcPH97U1FRdXV1QUJCZmWlnZ0dZrdXV1ZcuXfrtt9+MjY0TExM7TqTMzMzRo0fLysoeOnRo7ty5HXcjBOkJWFlZvXnzhuMpRUXF4uLiTpcIQZB28fDhw6ysLELIsWPHhg0bBoWampqampq4UIkgSNsQ1umwHojQWq0ZGRleXl51dXVOTk6//fabvb399+/fs7Oz4+Linj9/rqmpSdVsamqqqqpqamqqrKzsUJG+f/9eWVkpLS1dVVXVoTdCkJ5AcyYrIQSDxxCkO5KamgoH3H3zPn/+XFhYmJaWBv8+f/4cDhQVFU1NTZlr5ubmFhcXUwOCoqJi7969lZWVxcT+H+WnsrLyw4cPcHlDQ0N6enppaWlNTY2YmJiCgoKWlpaMjAxLsykpKXp6epqampWVlVlZWaWlpQ0NDb169VJQUNDV1WVpHwRWVlY2NjamCl+9etXQ0DB48GBJScm8vLzc3NyamhpCiLKyMvsdqfvm5eVxdORjaRxBEAqcDhMahNZq/e+//3Jzc5WUlPbu3TtkyBBCiIiIiLa2tra29vjx4wUtHYIg/GHVqlXsngt0Ol1A4iAI0nYUFRXh4M6dO3PnzhUXF+dYzcvLy9/fn/qX8u5zdnYOCQmB48rKyqSkpKtXr0ZERLx+/RoKra2thw8f7uLiYmdnx2wWfv782cHBwdnZ2d/fPyoqysfHJzo6Ojs7m06nW1lZLVq0aMqUKfLy8lT9W7durV271tvb28PDIyQkxNfXNzo6uqKiQlNT08rKas2aNY6OjszCb9++/datWzNmzLh58yZVOHbs2IqKimfPntXW1t66dSsgICA7O5sQMmrUqEWLFk2fPp3FcH3//v3Vq1cfPHjw+fNn9s/E3d3dz8+vlZ83gvQIhHU6DCgvL8/JyYGakGJKWVlZTU2NY+XCwsLs7GyY+ZKVldXR0aFG3W6B0FqtmZmZhBBRUVF9ff3m6tTX13/8+DE9PT0lJQXiToODg+GqPn36mJubQ9RrTk5OQUFBZWVlRUUFnFVRUVFTU9PQ0GBurbq6OjIyUlxcfOjQoXV1dcnJySUlJVJSUnp6elJSUm/fvoUXUl1dXVxcHNxISkrKwsJCTk6uUz4SBBFC9PT0mCNSEATpvowaNUpVVTU/P3/v3r3KysoDBw5UV1dnt10HDBjg5OSUkZEB724nJycoHzRoEBzU19c/ePDAy8srJSXF0NDQwcFBXFwcQoQOHjx47dq1ffv2ubm5US2DA1R5efnly5d37typrq6ur69vZGSUl5f37Nmz6OhoBoOxbNkyqj54ZmVkZOzfv//cuXP6+vqWlpb19fU5OTl37959/fq1n5/f8OHDKYFBR2RZIwWN4s6dO/7+/lJSUix3FBERmTdvHlU5IyNjzpw5nz9/NjY2hscpKyv78uVLRUVF7969Bw0aNGDAgI75ThCk2yOs02GEkLS0tMDAwNu3b0NNQoixsbGTk5O7u7u9vT1L5djY2Fu3bvn5+cHMl7Gx8ZIlS6ZPn97uD7gTaRJSjhw5QgiRk5O7fPlyXV0dxzpFRUVTpkxh/0x69erl4eHR1NRUX18fGxu7fv36YcOG6enpwVkJCQk7O7uffvrp/fv3zK2lpqZKS0tramqGhob+9ddfpqamIiIimpqau3btunfvHscPX1dX9+3bt531kSCIUAE/Im9vb0ELgiAI3/Dy8lJSUoJ1AE9Pz/v376elpXF8iXt7ezenxnz8+NHIyIgQMnLkyICAgLKysqampm/fvvn5+fXv358QoqGhkZSURNWPiIiAO4qLi48ZMyY8PBwuCQ8Pt7KyglPM9eHWsrKycnJynp6er169ggSQfn5+ampqhBBLS0uIPAKcnZ1B92UWktIEzMzM/Pz8qDuCd5iGhgZzC5s3byaEaGlpUY8TGxvr4eEB96qoqODHZ48gwklycrKqqirYaQ8ePEhPT+c4pPzxxx9OTk6Ghobww3T6Hz/99BNUqKur8/PzMzY2FhMTg/kjJycnW1tbuERDQ8PX15e5ZRhY7Ozsjh49CiuucImpqamYmBidTj958iRzfRhY1qxZs2nTJjqdbm5u7uTk5ODgQLX/7NkzZoGzs7NhbsvQ0NDW1hYqQ+PGxsYsldPT02E009TUBDEsLCzodDplB3ULbUporda3b9+qq6uLiooOHjz45s2bKSkp7H20oqJi9+7dkyZNgteblJSUq6urq6vrrFmzDh8+DBX27t0rLy9vYWExevRoV1fXKVOmjBw5sk+fPhISEuPHjy8oKKBagzTF8vLy8+bNk5eX79evn4ODg729/datW1+9euXq6jpmzBhCiKSk5JAhQ+BGnp6eycnJnf7ZIIgwwOM4e/r0aXCfg1cCzLlaWlqmpKRQdVJSUlatWkW9qwwNDVetWsVcgZlWVUYQpFWUlZX98ssv5ubm0tLSYBkuXbr0zp07GRkZLDW5WK3r1q2Daeu4uDiWU4GBgdDygQMHqEJQLgkhI0aMYPktBwYGwqmTJ0+y33rFihVgQ1L8+OOPcOrdu3dUIRer1cDA4MmTJ8zlPj4+cCohIYEqBC1l8+bNzDVhqRmC/Jv5OBEEaRLW6bAffviBENK/f38/P79v375B5fDw8JEjR7LMZ9XV1a1atYoQoqSkdPToUWrmy9PTU0tLC61WwcNgMHbs2KGiokKj0ZSUlJYuXerv7//ly5fa2lqWmuXl5b/88gshRFtbm+VUdXX13bt3f/zxx/Dw8MzMzKampoaGhuTk5K1bt4qLi6uqqt6/f5+qDFYrLMY6ODhcuXIlLi4uMjKSWk399OkTIURFReXs2bMd/wEgiJDD4zgLrwFnZ2cYsikiIiKgwrVr1zjGdSgqKn748IGltVZVRhCkbTx9+nTp0qWDBw8G9zlZWdm1a9eymKBclEt1dXVCyOTJkzk2Dvte2NjYUCWU1RoaGspeX0VFhRCycOFC9luzmKxNTU1xcXFw6sKFC1QhF6t1x44dzbVAjVFNTU1gae/evZu5JpUpPSoqiuOTIggCCN90WH5+vqysLCEkMDCQRRhqDHn69CmUpKSkQOXly5ezfCwHDx7sRlarCLv6JRxIS0uvWbNm9erVlpaWNTU1Fy5cWL169Z49e27fvk1FWrdIr169pk6dum/fPicnJ5iNgEDZxYsXa2ho1NbWxsbGslwiJiY2cODAnTt3zp8/f8CAAfb29vCCRBBEgISGhp46dcrQ0PDatWsRERHe3t4Qlx4TEzNnzpySkhJ3d3fK7AwMDLS0tCwpKXFycioqKqIaaVVlBEHajKOj47lz544ePbpkyRILC4va2trjx4//+OOPvOxoVVxcnJOTA+mOOFawtLQkhMTHx7OfAr2TBXiJ5+bmsp9iT0tBxZcWFBS0KCohhD1XMMcIVVtbW0LIhw8fwLkRHvP69evQAqzDIAjSHHJycrt37z527NicOXMGDx4sKip6/vx5Dw+Pffv2cRwKOALZ1BwdHdl/pBMmTIDl1hs3brBfuH37dgMDA5b6MB326tUr9vr79u1jGVsWLlwIBx8+fICD8PBwKlQ+6P8lPT0dyinzFYLzCSHLli1j+VhYSro4QpuNiUajqaqqbt++feTIkRCm/Pnz50uXLgUEBMyePRsmcdvWsoiIiLy8vK6ubn5+flJSEstZGRmZiRMnjh49mh8PgSAI31BUVHz16hX4CFFZFvbu3cuefnPChAk2Njb9+vUrKSm5efPmihUr2lAZQZB2MmLEiBEjRkRGRv7++++PHj0KDg4OCwubPXs296sSEhLgAJRCdsC9n+P+MV0WDw+P8PDwGzduKCsr29nZ0en0xMTECxcuiIuLT5kyhUvWSQRBKBwdHR0dHZ89e3b37t3//vsvNjb2+PHjKSkpvr6+vXv35n4tL9Nh7969a9V0WGhoaJunwxITE+Fg4sSJzcksIvJ/a5OUHQueydzv1ZURWqsVEBcXHzlypL29fVRUVGho6JMnT96+fXv27NmcnJzTp08rKyvz0khDQ8PXr1+zsrKKioqo3Yfz8vI4VhYTE6N8xBEE6Wi2bt26detWlkJvb++ffvqJpfDJkydgslIUFRVBwsC1a9eyVFZSUrK2toZBAwzRVlVGEIRfODg4eHt7Dx06lBASHBzcotVKbXzV3NbopaWlHBc5uzLfv3+HvE0BAQGnTp2illinTJmyZ88eQUuHIN0J4ZgOgx1oCSGurq7N1bG2tu4cYToNIbdaAXFx8REjRtjZ2Y0ePXr//v0hISGPHz9+8uTJrFmzuF/4/fv33Nzcx48fh4eHx8TEZGRkMHsASklJdbzsCIK0GuZU8hTUrhgU1FQl8x4VLICC29rKCILwESrQhheN0MDAQEJCoq6u7suXLxwrvHjxghDC0d+qvr6epaSurg4WQzgGtNfV1UlISDCXwGpMc6NQ2ygtLQXTdPfu3ampqVFRUYQQNTU1c3PzyZMno3swgrSB7j4dRm3HeufOnc65Y1egR1itANiuhJCQkJDa2tqIiIgWrdaqqipfX999+/bV1dWZm5u7uLhANHNVVdWjR49QQ0UQgcNxWZVHqKlKLsArrbWVEQRpAw8ePDA0NDQxMWEpp+aMBg4cSBVSWxHW1tZKSkpS5XQ63dTU9MOHD//9919paamCggJzU8nJyW/evIFcTewCwMYzzJfExMTExMQQQuzt7dnrBwQETJo0ifnu4JEhISHR5igkdqhd5U1NTadMmbJx40Z+tYwgPZluPR1mZmZGnYL8c1ygXJQLCwtZ/EwhTr670IOsVpiZgGhpXr6npqamwsLCs2fPVlVVTZkyZdWqVebm5tC9cnNz3d3do6OjO0VqBEE6hLKyMjiIiIigIl35UhlBkDawdOnSUaNGzZ49W1dXF/KlVVVVpaamnj17FlzxXVxcqMqUovb8+fNRo0YxGIyysjJNTU1oZ8uWLVFRUefOnZs5c6a6urqkpCSDwcjIyDhw4EBlZaWuru60adPYBTh8+LC8vPzMmTP19PRqa2szMjIOHToEG1qMGzeOvf6PP/74/ft3R0dHVVVVBoORkJBw4cIFcMzjmFSpbSgqKiopKRUVFe3Zs2fUqFFQKCEhoaysLCEhoaWlRe0njyAIO0I5HUZZrf7+/i3OZBkbG8PB/fv3lyxZQpXX1tY+ePCA+7VdCqG1Wq9evWpmZsbiE1hfX//x40cwX01NTaGQRqPBlEZTUxNzH21sbMzJyUlOTlZSUpoxY4ajoyOUw4445eXlrRUJbtTU1MQ+6YIgSOfTKrWSjzoogiAc0dbW9vPzCw8Pt7GxMTc3hwwokZGRsbGxSkpKnp6ekEoXsLCwAFtu9+7dmZmZBQUFNBpty5YtkDLt4cOHISEhO3fuTE1NHTBggKysbEFBQXR09PXr1zU0NDZs2AD7LrKgpaUFl9jY2DAYjDdv3vj5+dHpdE9PT471JSQktm7dOnfu3H79+hUUFAQHB8fGxmpoaGzbtg08s/iCjo6Om5vbqVOnLl68ePHiRSiUkZExMDCQlpa2sLCYOHEil4wsCNLDEcrpMEtLSzMzs7i4uAsXLpibmxsbG4OQtbW1hYWF2dnZaWlpbm5uUHnQoEFGRkZJSUlnz561tbU1NDSUlJTMzs5+8eIFe2aQrozQWq0//PCDvb395MmTjYyMdHR0mpqaSktLP3z4cPnyZREREW1tbSrNr6ioKPTRmpqaZ8+ejR49uqysjMFgaGhoiIuLS0pK1tfXJyYm5ubmqqmpVVZWJiUl3bp1i8rHxTvi4uLa2tq5ubnv3r0rLi6m0+k5OTmKioqUrzyCIJ0JvL0gpqXF5dNWVUYQpA3s2rXr4sWLSUlJUVFRAQEBhBBJSUkNDY2RI0eOGjVq06ZNzJWNjIxWrFhx+/bt58+fh4eH0+n0GTNmwCkVFZVdu3bBLso3btyA9EVUU5MnT/b09OQowLJly54/fx4SEgKX0Ol0S0tLBweHNWvWcKy/ffv2K1eu+Pj4FBYWEkKUlZWh/QkTJjBXg5lxFpc/SUnJ2tpalkLmU9SaT0VFhaqqKiGkf//+w4YNo6rl5eVlZWWdOnUqODi4b9++1HIKgiDMCOV0mKysrJeX16+//hobG7tx48axY8fCozEYjNTU1A8fPiQkJFBWq6qq6g8//LBt27aXL1/+/vvvI0aMkJWV/fjx4507d3r37l1bW/vt27cO+/j5idBarfr6+nfu3ImMjDQ3N+/bt29TU1NRUdG7d+++fv2qr6+/Zs0aarpCXFx88ODBKioqZWVlf/3119u3b8vKytTV1devX6+npzd27Njg4GBfX9/CwkJNTc2Kior4+PiHDx9yTGPNHTqdPmbMmDNnzgQGBiooKMjLy5eWlnp6euKbBkEEgoGBgaWl5Zs3b06dOrV582aWDMPtqYwgSBsYP368paVlZGRkQkICTA1LS0ubmpoOGTKEfcMGQsi2bdtMTU2jo6OrqqpUVFQgdQVgbm6+f/9+3psCbG1tZ8+eHRQUBM5+0Ka9vX1zC6ceHh6DBw++f/8+3EJXV3fcuHHs7U+aNKlPnz6wTyzFypUrq6qqOO7oDqdg5YQQEhkZuX//fhUVlV9//XXevHlUteTk5NjY2BUrVqSlpYWFhaEugSAcEdbpsJkzZ1ZXV/v7+yckJJw4caK2thYal5OT09XVZckvNWfOHBgogoODYatnfX19U1PTNWvWXLhw4ebNmxxn0LoatKamJkHL0CGEhYXdvHnz48ePX79+zc/Pp9Fo0tLSBgYGpqamLi4u7u7uzBmAKyoqjhw5cuPGjaSkpPr6+j59+ixYsGDv3r319fWvXr06fvz427dvk5OTaTSarKysmZnZ4MGDi4uLAwIC5s+f7+PjA42kpqaamprS6fQDBw5Q2wEzU1dXFx0d7e3t/fLly4KCAnFxcTs7Ox8fHyrUFkEQ3qHRaLxkY9q3bx84wHAc64KCgsCzztDQ8M8//xw7diyYo5GRkcHBwadOnXry5AkVaNCqygiCdBciIyMhNziPUevcRxW+s3z58rNnzzo4OERERLCcqqmpGTRoUFJSUnvy0iGI0FNQUMD7HBaDwbh37x7zdJizs3MbmmIeWPT09FqcDmMeWGJjY1ucDgOSk5PDw8MTEhIgubGKioqqquqQIUMsLCxY2mcwGM+fP3/27Bls+mppaTlq1Ki+fftevXr1v//+mz9/PvPEX9dEaNdax4wZM3jw4Pfv36ekpMDeqrKysn379jUxMWG3EmVlZdeuXWtmZpaYmFhfX6+iogKdQ1xc3NbWVk1N7fXr10lJSTQajU6nm5ubDxo06NOnT2ZmZsyzpIqKijt27BAVFeU4dQor/lZWVn/88cfz58/z8/PFxcUHDBhAuR0iCNL5TJgw4dq1a3PmzElJSZkzZw57BWYH/lZVRhAE4QvV1dWwZfT79++1tbUhBWhNTU1eXt6TJ08gvTnsFYkgCEdUVFSmTZvGMeiUHVlZ2Xnz5jH7NbS5KQotLa3ly5cvX76cx/oDBw5kzhHFhb59+/bt25eXmrKyss7OzswWOMDlYbsaQmu1ioiIqKqqsn83HKHRaIqKihx7oZiYWL9+/fr168dSrqqqyjInoaio+Msvv3C/EaT/4mNCfATpsSgqKpaUlLS4KSJU4JhcHpg9e7a1tfWBAwfCwsJgewlFRUVra+uhQ4cuXbrUwMCgzZURBEHaz9SpU8PCwhITE3fu3GliYkKlk0lLSwsODm5sbHRxcRk5cqSgxUQQBOlYhNZqRRBEuCkuLual2ooVK1asWMG9joGBwcmTJ3m8b6sqIwjS9aECuniM7IK9Bnr16tXBcv0f48eP37BhQ3h4eExMTFhYWE1NDZTr6urq6OhMnjx56dKlGGmPIIjQg1YrgiAIgiA9Fy0trR9++AEOeKlvY2Pzww8/MGfH6FBkZGQ2btw4atSo2NjYzMxMcBiGtDF9+/Y1NzdHkxVBuiBdfDqsOyK02ZgQBEEQBEEQBEE6n2/fvh0+fJgQsmnTJl6y2Lx8+fLWrVtSUlJ//PFHpwjY/UCrFUEQBEEQBEEQBOm6oIcwgiAIgiD8ISsrKyoqKioq6uXLl5mZmVAiaKEQzmhpadnZ2cFfOBC0RAjCCg4p3YiOHlJwrRVBkGbBt0U3AhVQRIBkZWXduHHj0KFDOER0X2b9D0ELgiA4pAgDfB9S+Gy1oo7bXUAFF+ECvi2EAFRAkc4hKytr8+bNN27cELQgCN+YNWvWoUOHUDFABAIOKcIHv4YU/litqON2d1DBRQB8WwgfqIAiHURzw4WdnZ2tre2sWbO0tbV5T8yLdD7USgNocSxnZ82adf36dQGJhvREcEjp7nT4kNLUPjIzM9HUESZmzZqVmZnZzl6BdEea+y3b2dlt2rTpxYsXmZmZ2De6MpmZmdevX9+0aRPH73HWrFmCFhARKq5fv86iO4JGImi5kLZz/fp19tEDv1Okc8AhRfjg+5DSdqsVddxuDSq4CDP4thA+UAFFOo5NmzaxDBf4uhca2IeOTZs2CVooRMjBIUWI4eOQ0karFXVcIQMV3J4Mvi2EGFRAEb7D3KO0tLTwTSGUsKh5OJeNdBw4pPQE+DKktMVqRR1XWEEFtweCb4ueACqgCL+ws7PDF0TPgVnfs7OzE7Q4iBCCQ0qPop1DSqutVtRxhR5UcHsO+LboUaACirQTZgUAR4weAvO4gfoAwl9wSOmBtGdIaZ3VijpuzwEVXKEH3xY9EFRAkTbD3HkOHTokaHGQzuPQoUP4skD4Dg4pPZY2DymtsFpRx+1poIIrxODboseCCijSBpi3K8Bu0wNhfmWgkx3SfnBI6eG0bUjh1WpFHbdnggquUIJvix4OKqBIa8ERA6HGDS0tLcxmgrQTHFKQNgwpNOau0xw3btxwc3OjuhezJYMIPZs3bz58+DAcc0w1jHQ7aDQaHODPucdC/a61tLSioqJw03aEC25ubrBfPOgWghYHERja2tpZWVnUthGCFgfpruCQggCtHVJEeGkUTdaezKFDh6jpkM2bN0P3Qrov1M9ZS0sLf849lkOHDoGlmpWVtXnzZkGLg3RdsrKyQL+EbtPO1ry9vcXFxceOHZuTk8MP6ZBOheoAN27cQGUAaRv8HVKQbk1rh5SWrVbUcRFUcIUGfFsgFKiAIrxAjfmzZs1qv6/N169fGxoaioqKCgsL+SEd0qkw9wFUBpC2wd8hBenWtHZIacFqRR0XAVDBFQ7wbYFQoAKK8AKlA/BlxNDX1xcTE1NSUlJWVm5/a0jng8oA0k74O6Qg3Z1WDSktWK2o4yIAKrjCAb4tEGZQAUW4wzxi8GXQ2Lp1a319/cOHD9XV1dvfWudTW1sLhnd8fLygZEhPT5eUlFRUVMzOzu78u2tpaVE9geoeCMIjfB9SkO5Oq4aUFqxW1HERClRwuzt8fFtgcJpwgAoowh3UAVjw9fVNS0szNTUdMGAAIaS6ujo/Pz8/P7+hoYHLVd+/fy8sLMzPz6+urm6/DLq6uuPHjy8tLT137lyrLjx9+jSNRlNQUGinAFRnQBc8pLXgkIKww/uQws1qxRkRhBlUcLs7fHxbYHCa0IAKKNIczCFCbRg01NXVaTSaq6vr9+/fuVTbuXMnjUbrFkuvDQ0Nf/75JyFky5YtUHLt2jU1NTU1NbW3b99yuTAvL69v375qamrXrl3jiySLFi0SERG5dOlSbW0t71eVl5cTQsrKytp5d6ozZGVl4RQ2wjvtHFIQYYX3IYVXq5Wv4iHdFVRwuy/8fVtgcJrQgAoo0hxRUVFw0LYRw9nZmRBy79693Nzc5urU19dfunSJEDJ+/Ph2SNpJREdHp6WlSUpKTpkyBUpsbW3FxMQIIf7+/lwuDA0NLSsrExcXt7W15Yskrq6uqqqqaWlpAQEBfGmwtdjZ2cEB1UkQpEXaOaQgQgyPQ0qzVivOiCDsoILbfeHv26K7B6cRQs6fP0+j0RYuXChAGTZv3kyj0Xbu3Ml9MaqjQQUU4QjVH9q2ne/06dNFRETAZmuuztu3b9PT00VERObPn98OSTsJ8MgdP368oqIilFCuwrdv366vr+d41ffv3+/cuUMIGTZsmKmpKb+EgUmBK1eu8KvBVkGZ3zhoILzTziEFEWJ4HFKatVpxRgThCNLZ71kAACAASURBVCq43RR8WzBTU1Pz559/ioiITJs2DUry8/Nzc3NLS0u5X1hZWZmbm5ufn88XMWbPni0qKnrkyJG8vLxWXaigoECj0U6fPs0XMVABRThCTU1Sw36rmDJlCsxq3blzp7l5GViiVFdXHzVqVPuE7XDq6+sfP35MCJk8eTJzOexnnp6e/ubNG44X5uTk3L9/nxCyePFiPsoD673379+vqanhY7M8QmmGL1++7Py7I92Udg4piBDD45DSstXa7XTcWbNmiYiI9O3bt7mJT0JIXV3dzZs3aTSampra58+fO1fA7g0quN2UNr8tLl68SKPRaDQa96Hk27dvYEpdvHixfZJ2Bn5+fmlpaerq6q6urlAyaNAgdXX1RYsWcV/23L9/v7q6+qBBg/gihrW19YABA8rKyoKCglp1IUSmQZRa+0EFFOEINci3WcV0d3cnhAQEBHBM21ZXVweLkFBNsNTW1hYXF2dlZWVkZGRlZRUWFrKEjL5//z49PZ0QMnDgQOZyJycnCQkJQsj169c5thwWFkYIkZCQcHJy4iIA3Lq5iTM4y/yTt7S0bHEpmwt1dXWFhYXp6enp6enZ2dnl5eWt8vjQ1taGg8zMzDbcHemZtH9IQYQVHocUbh7CcNDt+tbw4cObmpoKCgoePXrUXJ3q6urbt2+LiIhoaGgYGxt3kCSFhYV3795duHChiYkJ6P1ycnJjxow5ffo0xxw25eXld+/enT59upaWFtTX0tKaPn363bt3u07OG1RwuyltflvY2NjwHrglISFhY2PTPkk7nIaGBtCVV6xYQRUKKgZv48aNhJC///6byyxbR4MKKMIRSg1o8+T15MmTxcXFCSHBwcHsZ9+8eZOeni4uLs6yesnO15YAe7LNVFZWBgQEbNiwwczMTFdX18zMbPHixQEBAZWVlVSdV69eEUIkJSWtrKyYr9XR0XFwcIAlZfbcSN+/f799+zYhxMHBQUdHh4sMNjY2urq6O3bsYD9VXV0Ngl24cIH5vqqqqoSQmJiYNjzvo0ePFi9erKenp6enN2zYsD179iQmJgo2VAEReto/pCA9naZmoLpUZmZmc3W6Ju/fv5eQkOjVq9eGDRs4Vvj+/XtmZqacnBydTj948GDHSeLl5UWn09XV1S0sLIYPH25ra9u3b18wALy8vKqrq5krV1dX+/j40Ol0WVlZc3Pz4cOHDx8+fMCAAWJiYnQ6fdeuXSz1BQWl12ppaQlaFqQVtPiT58LgwYNhu4W6ujqOFRobG0HvdHR0bLekHU5iYiIhRERE5PXr11ThvXv3YOHiwoULzV344sULuPDx48f8EiY+Ph7GhJcvX/J+FXyV3t7efJEBf9QIR9ozaFCAY8KIESPYR4/169eDmwPvkjSHoqJimyWsrq4+evQoWKRaWloGBga6urq9e/eG6SSq2rJly8C2ZG/h7t27IEZwcDDLKerHdffuXe5iLF26lBAiLy9fWVnJcgqSjIiLiz958oS5fNKkSYSQkSNH8vik3t7eIMzRo0clJSX79OnD/LADBw789OkTj03xq3sgPQrsMwgXeOkezZ7rvn2rvLzczc2NRqMZGhpyVLKrq6thwrJPnz6tGqNbi5SUlIWFxeHDh5OTk5uamsrKyu7fv0/5FkZHRzNXfvr0KZ1OFxMTW7p06cePH6Hw5cuXI0aMIITQ6fTIyMiOE5V3UMHtprTnFw0LjISQFy9ecKxATaBeunSp3ZJ2OPDzV1NTYynX1NSE1aHGxkaOF8K6qKamJn/lgWwuXl5evF/CX6u1Ww/4SMfBl16xZ88eaCQ2Npa5vKamBtYe9+zZ02IjfVvCwsKizRKC5wUs+SYkJDQ1NZWUlPj4+GhqaqqqqlLVRo4cCdGk7C2UlJTIysoSQjw8PFhOQQInWVnZkpIS7mI8efIEJs5u3LjBcsrDw4Ojeb9u3TowdHl8UspqhTTIYAOXlJScOXMG5J84cWJzU5Ps4KCBtBbsMwgXeqjVWltbC1qpnJxcUFAQe4XS0tLZs2eLiYnxPkPZNhYsWMDynm5qavLx8YEP9vjx41RhXV0dLFUNGTKkrKyMuX5sbKycnBwhZOnSpR0qLe90377Rk2nPt5aeni4pKUkIac5/4fz586AJpaent1vSdtHY2FheXv7t2zfwG/z27VtpaSmLFQpZTKZOncpyLbUHI0cHk9raWl1dXdiqkYsA5eXl4K9YX1/f3NmvX78yF27YsIEQYm5uzvtjMlutpaWlWVlZ0Gx+fn5NTQ3v7bA0iD9qhBm+9IrExERwEmaZZImIiABbMTExsd2Stp26ujozMzMIE2UxLN+8eTNt2jTqX3l5eULIr7/+yrEdaqWUwWBQhQ0NDRMmTOD99Q1m/Pz585kLGQwG3JrdvKesUN6e9f+vP3XqVJaHpcIl4uPjeWwNBw2ktWCfQbjAS/fgtl9rN0VcXHz48OG9evWqq6sLDQ1lcS4CxTEoKEhKSmrq1Klc2mlsbMxvieLiYi4tXL58GV6HzBgZGcEBcwBMRkYG7Lq2atUqsFEpzMzMYLk1KCioqqqqNZ8EgvAH5sAt9nyVjY2NPAZulZaWprZEezIMNTY2JiYmHjt2zNnZWV9fX19f39nZee/evYmJiY2NjVCnvr7+v//+A7c6lssnTZrESwweeOU1x61bt/T19c3NzTmmefPx8dHX1+/fvz9zIfhffPz4sbW5QL9//56dnb13795hw4bB8y5evPjevXsMBqNV7SBIx9G/f39zc3PYo4U5eBtyF5mbm7P8HDqZlJSUuLg4Qsjq1asVFBSYTw0dOhRGNgBSoNHpdI7tTJkyRVRUlCWz2rdv34KCgkRFRan9Xbkze/ZsSAvMHE8bFBRUVlbWq1cvKuE5O9XV1by0T3Hp0iWWh/X09ISDt2/ftqopBEGQTkMIrVYajdanT5+FCxfW1tYGBASw7FFRW1v78OHD8vJyOp0+c+ZMLu1kZ2ercUVdXX3s2LGtFS8+Ph5M6759+1KFVMZ8e3t79ktgsjYnJyctLa21t0MQvgARaBkZGU+ePGE59e3bt8DAQKoOF86cOWPYEteuXWuzkJ8/f54zZ86vv/6am5urp6dnaGhYXFx85MiROXPmZGdnQ52vX7+C9smuK48cORJ2U2RRrwFIRmVqaspu7jJjY2MjKSnJMS1wfX39P//8AxnjmMtNTEzgAOJmeScjI2P8+PHnzp2j0Wh9+/bV1NR89OiRu7v7+fPn2bPCIIiggHXIuLi4T58+QUlNTQ3EgsIpAQJR7oQQcNRvMyNGjIBsIPfu3aMKIbuvlpYWTD23iJubm7i4eHl5OeyUA0CDDg4OXMz71pqaLCYrmOhwwDHbM4IgSFdACK1WSDE/btw4yOL79OlT5lO1tbVhYWESEhLW1tbck5iJior2aQklJSXepcrLy4uKigJfSnt7e+Yk+MnJyXDAcQtyQ0NDOODXLpEI0lpGjBgBiwz//vsvyynQzOh0eouamaKiYr+WAF+4NlBZWbly5crY2FhVVdVjx469f/8+OTn53r17Li4uGRkZ1OYQVAguJCBhAXbgiIiIYFkpra2tBSW7xS06TExMYO7pn3/+YTF9P3/+HBsbSwiBaDQKiKeFCq165FOnThUUFOzduzciIuLLly/37t0bM2YM5CWGfKcI0hWYPHmylJQULBtCSXR0dGZmppSUVIvZg4GEluD+2+nduzeNjdTUVELIly9foA7lBtU2FBQU3NzcYJsfcHagnFDc3NwoK9HHx4ddktWrV8PZoUOHgn/WlStXwD2EwWCAH9bChQu53F1aWhoOZs+ezd6+n59fex4NQRCkiyAmaAE6BAkJCUdHRzU1tZKSksDAQNjBlXIPDg4OlpaWBlccLmhqarZ/0jE1NfXdu3dw/P79+6CgoJycnDFjxuzcuZPZ0YhaCOII9ULisicHgnQooJOdP38evNdkZGSgvLGxEXKZMGtmzeHp6Un5ofGdwMDAiIgIUVHRY8eOUbbl0KFDL126dPToUQ0NDSihtFuOSuq0adO8vLzq6+uDgoKY3fujo6MzMjLExcW5OOlRLF68ODw8HFaWmLd2BJWd3bynNp6pqKho1SMrKSmdO3du4sSJ1MMeOHDg6dOnlZWV58+f53F5B0E6Gi0tLQcHh4cPH165cmXTpk0SEhLgueDg4MDjBhgtLoQqKipyCdgxMTFhDz2ATVYhKID6t0WoWAN2Jk2adOjQofLy8sDAQHd396ysrODgYFFRUeaYgt69e7PHDVGjEyFk7ty579+/Dw4OzsrK0tXVDQwMLC8vl5eX5+7iYWFhAQfa2trs7bd5KhBBEKRLIZxWKySGmTZt2qlTp4KDg/Pz8/v06UO5B1dUVMBLtBPEePjw4cqVK5lLBg0aNG3aNAMDA+ZCmPRtkYyMDH4LiCC8MnXq1EuXLoFOBqsKMOECgVvco8Q7gZCQEEKIqqoqy3KogoKCl5cX9S9lGXK0sSEG7+3bt6BeUxotKNk8xuA5OjrKyMhUVlYGBQVRVmt9ff2VK1cIIXPmzGnOvG9t4PqqVasok5WS39nZ+fbt2+yO3AgiQJYsWfLw4cP4+PhPnz4ZGRmBByz39UNmIDKWCyz5IFh4/vx5c6f09PTg4MWLF+Cq0ByysrIMBqOgoKC5CiNGjNDT00tJSbl//767uzv4d2hrazPPH82aNYva85wjs2fP3rFjR3V1dWho6PLly+GDcnNz42je19XVgV8YVbJ///79+/dzaR9obGxkvop5YOzVq1eLlyMIgggE4fQQhpHX1dVVTEysrq6OchKura0NDQ2VlJQcO3Ys5ZXXofTr12/+/5g4ceKQIUMSExN///33Q4cOYZAq0r0YPnw4aE7MMVdU4BZLrGbn8/r1a0KItbV1O9uBXRlZYvAgtAxOtYi2tjasrly5coVKsPTp06e4uDhRUdF58+Y1d+HLly9bJSrHxDA2NjaQBrlVTSFIh+Li4gKTNffv33/16lVmZqaCgoKjoyOPl8e0BGQkbgOmpqawyvry5UuWddSamhpqEACjlBDy4cMHLq0tX76cEPLgwYOioiJwD54/f36r5KHG0tu3b5eWlj548ABSPXGsDFoETMq3infv3rE8LLjMiIqKtjhBgCAIIiiE1moVExOzsrLq169fbW1tUFDQ9+/fYcfUkJAQKSkp7pOdQGNjY2ZL5OXlcW9k1KhRV/7HqVOn/vzzzxkzZpSWlh44cODIkSNUxpTm0hKyoKqqytvTIwj/UVBQgGXMgIAAmJinArfc3d1bdA+GOPO4luDi5sc9JAzynLVf5Zo0aRLE4EGKKbCHIQaPxdOvuUg5SlWNj48HW5pqjWXhhQXK7zomJoa9ceb8bULAlStX4LkgpXNzpKWlycvL02g0WKnuOlRXV3/58mXTpk0gHuTZ4h24iiO8vJ66HVTYp4+PD8TGN7d+2MkYGxtDIiIfH5+YmBhIxtvQ0JCfnx8YGMiccBHev1QcLEdcXV0lJSXLy8v//vtvmCKHrVZbBSxBh4aGXrx4sby8XFlZubk5waSkpLZN1S1atOjt27eQqbi2tjYzM/P06dMwzz5kyJDWtoYgCNI5CK2HMDgJu7q67t27Nzg4OC8vr3fv3uAerKura2dn1+Ll2dnZsD1jc4iIiAwePJj33H3a2tra2toDBw5MT09/8eLF2bNn161bB5mW9PX1eWlByNRWpNsxadKkgwcPgpPw7Nmzs7KyQkJCWAK3uHDhwoWtW7dyr3P69Glq50AWevfuzRwmClAhYRISEuAvxyPsPnIArHWEhYX5+vpu3rxZQkICtuiglpoBU1PT5iLlIGCvd+/excXF169fHzFiRF1dna+vLyGEy0IrtUwKriLsT0qFvwoHkGy5trbW39+fy5pbSEhIeXm5tLQ09eEIHDBpnj17tmvXroSEBChsbdIB6Dw6OjrsDpm8TAB1R6ZMmXLmzJmsrCxIDsTjZjCdwJYtW1auXJmVlbV27doNGzYYGRmVlZXdvXv34sWLzDnbLC0tL126lJWVxRzYz4KRkdHAgQPfvHlz+PBhQsjAgQPbkOTJ0dFRUVGxpKTk0KFD4OLBMTC1trY2JiYGBGtV+3JycgUFBYsXL96yZcvgwYOzs7P/+eefqKgoaWnpn3/+WciCYHV1dTMyMpydnQMDAzkO+MDWrVv37duno6OTnp7eofIUFRUFBAT4+flFRUXBIGBqajpu3Dh3d/dBgwbBhCmCIM0h5FbrxIkTDx48CE7CEydODAsLA89hXsZlMTGxFq3WNnjmaGtrjxs37sWLF1VVVQkJCWC1UqE1ubm57G1SK7ptuB2C8JHhw4fr6+snJyffv39/9uzZEEqqo6PDo3uwqqoq7E3KBS55ubmHhBkbG8fGxrLkDGeHUjdzc3ObCxNYvHhxWFhYfHx8YmJiczF4kZGRXO6ioKDg6enp7e19//79/fv3JyUlxcfHS0hILFiwgL0yZWxTSpWxsfHHjx+5P0hziWFKS0uZU7h1WYyMjCwtLZ8/fx4QEHDgwAGOAjc0NMBivqOjYztTvPKRjx8/Hj9+/MqVK3369OnXrx/3xTfu7Nq1i907QEVFpd0ydkUcHBzU1dVzcnLKy8vV1dU7J7UEL8yYMePLly9nzpyJj4+HNI2ioqK9e/dWV1c/duwYVc3e3l5UVLSxsTEiIsLFxaW51iCdUnl5uaio6Ny5c9sgj6am5pw5c06ePJmVlSUtLd3cnGBSUhKYPRw3zOMIjDAjR460s7O7cOHC+vXrYblVRkZGV1d3xIgRvEcadxfGjx/v4+MTGhqamZlJKVosVFdXw/o/S5oAvlNeXn7o0KE9e/YoKipqa2tLSko2NDSUlpYeOXLk5s2bJ0+e5DGlNoL0XJqaocUK3YKSkhJ7e3tJScl58+alpqbKyckpKSmFhYUJVqpdu3bBZ3v9+nUoAe2fEHLjxg32+pB2VVVVtdMl5Yxw9I2eBr++tX379lGz9bC/1G+//cYnGdsFRJSBYCynMjIyqEIqL0t4eHhzTZWWlioqKhJC/vjjDzCDFRUVs7KyWiUPJDQmhDx9+nT37t2wJMKxJhU7d+nSJR4bh/pLly4tLi5mLmcwGLB71pgxY1olrUB+1NTevI8fP+ZYISUlBSpcu3at48RITExMTU2tqanhsb67u7uampqTk9OVK1eoodvb27tVN4WrIiIi2iRyJ8H3XnHy5Elra2tra+uTJ0/yq01+ERoaum7dOisrKysrq1GjRv3111/v379nqQOzzFu3buXSTlZW1qhRo6CR1g4aFJGRkSDJggULmqtz8uRJ8EApLS3lsdlbt25ZWVn99ddfcIsFCxZQd7l161ZrhewWmkBoaKiYmBghhEuXCw8Ph4WKyMjIDhXm1KlTEB3wyy+/QN8oLS29desWePGYmJjw/lV2U7pFn0EEBS/dQ8it1urq6r///huy/23fvl1UVNTCwkLgIsHUqaSkZHx8PBRmZWXB8u+CBQuqq6uZ62dnZ4Nn4PLlywUkMivC0Td6Gvz61j5//iwpKQnGKnTjz58/80nGdvHgwQMQbMeOHQUFBfX19U1NTRUVFV++fJk5c+aJEyegGrXzzeXLl7m0Bl7KWlpaMGe0YsWKNogEqcJXrVoFluTBgwc5Vnv48CGIFB0dzWPL1Le5Z8+enJwceNjS0tJLly7Bisr58+dbJapAftTZ2dmysrJcBrcTJ07A6J2dnc2lnZcvX0ZGRqalpXE5y8V+mDhx4rRp065fv56cnMwy/HJkx44dBw4cAP2SSgKEVmtPYNu2bWBd8D7H0UHU19dDzO3KlSsFJUN36R4QWjVmzBgYJ9mB0b5v374dKkZJSQl49yxZsoTl1MWLF+GT9PX17VAZBE536TOIQECrtamhoeH9+/cSEhI0Go1Op8vIyOzcubNzbh0TE+Pr6xsTE8OsLaWmpvr4+EDogrOzc2VlJXUKlGMlJSUfH5/8/PympqaqqqrExMQtW7YQQtTU1NjnfQWFcPSNngYfvzUrKytqqwkrKyt+SMcHSktLx40bJyoqKicnt23btkePHkVHR589e9bOzk5GRobZigPJf/31Vy6tUamYoHJgYGAbRNqxYweYvuCD15zhBNFrMjIyvE+0g2y6urqioqLr1q2Dhz1y5AhIa2Fh0do5e0H9qF1dXcElkl3gurq6UaNGQYYb7o3A7MDixYvZTxUVFUGuu+PHjzd3+c6dO/v37w/BI9euXfvy5QsvtiuAVmuP4vnz5xCH/O7dO8FKAm4IYmJiAvQd6y7dY/v27SBncnIy+1kGgwHG5Pbt2ztUDMq1JCYmhuVUaWkpRLPPmTOnQ2UQON2lzyACAa3WJpjfglQfNBqtT58+z58/75z7Xrx4UUtLa/r06atWrfL+H0uWLAEV1tbW9smTJ8z1ExMTBw8eDDruxo0bvb29vby85s6dKyUl1adPn9aqRB2K0PSNHgUfv7XDhw+Dz5WYmNjhw4f5IR1/SEpKcnBwUFVVhUVXMAX19PTmzZvHbBRB6JqtrS2XpkpLS6k8TxoaGm1z3EpKSqLCaKdOndpcNQh+Gz16NO8tw+d/7do1R0dHVVVV6utQVVU1MzNrwygnqB817JxECLl58ybLKciPCslUuTeyYcMGyMReWFjIcgpS+0pJSb18+ZJLC48fP543b56xsbGYmNiUKVOuXr36+fPnqqqqFuVvp9V69OjR8P8RHR2dkpLCy007DRzq2Rk5ciQ4dAhWDAi4NTMzE6AM3aV7REVFwVzDkSNH2M+Cq0uvXr2ioqK4NFJaWvpfSyQkJHBpYf369RBswvHsjBkzYP6u9c/XnegufQYRCGi1NsGE/f379/v162diYsLumNFxxMTELF26dNiwYbAOAKirq1tYWCxdupSjHnb37l0PDw8TExMqq6S6urqLi8uBAweYV2UFTtfvG56envb29u1RLLKzs11cXOzt7W/fvs1X0QQGH7+1rKyssWPH2trajh07ts2BWx1EVlaWt7f39OnTbWxsbGxsFi1aBNseMteh5rxLSkq4NHXq1Clo5NSpU22WZ9GiRdBIc5ZkZWUlzPQfOHCA92bh88/KyiotLd23bx/1dezbty8pKakNcgrqR11WVqampkYImT59Ossp0MvV1NTKysq4N/Lq1StxcXGOXt/Tp08nhAwbNowXYQICAiZOnNi3b19xcfHJkyf/888/iYmJ3M3IdlqtzBgZGc2dO/fatWu5ubmtaqrj6PpDfefz8OFDWVlZTU1NBoMhKBmqq6ttbGzExMR4j4TvCLpR94BtI6ysrNh/zrALt52dHfcWeNkQ2N3dnUsL4Dni7OzM8Sw45kByvtY/X7ehG/UZpPPhpXvQOL4+YWWSurjF3yrCkdzc3Li4uJycnOTkZCjR0NDQ1NS0tLRsLhtwRkbGq1evkpOTa2pqoP7QoUNNTU27VEbQrt83ZGRkqqqqFBQUSkpK2tbCq1ev7O3tGxsb3dzc/P39qfL09HRw5uGeX7oL0vW/tU7j27dvxsbGDAbD19eX+1Y0nUB4ePjo0aN79er18ePHfv36CUoMAXaP9evX//3337KysqmpqVT6XAjb+++//9atW8ecx7U5TE1NExMTp02bBjmHgYKCAgMDAwaDcezYsXXr1vEiTHl5eWhoqK+v76dPn75+/ers7Dxz5kwrKyt9fX2Om1JERkZCAm1vb++ffvqJ96eGhLTUwF5SUlJYWJiamiorK7tu3brffvutK+yBgYMGRzw9PT9//nzhwgVB7UX37du32bNn0+n0a9euQVCAQOhG3ePYsWPgkREdHc28URCDwTA2Nv727dvRo0dhLbQ54uLiNm3axP0uI0eOpLyR2TE2Nk5KSnJ2dqZSuDGzb98+2BYuPT1dR0eHt8fqfnSjPoN0Pjx1j/aYvEjPpOv3jfnz51tYWPz8889tbiErK8vR0dHCwoLFcXHmzJmEkJkzZ/JDzE6l639rncnUqVNhKx1BC/J/qY9HjBghWDEE2D0ePnwIK6UXL16kCiGvsri4+MOHD3lpBBKzy8rKQlIAAHKcyMvLp6amtkqksrKyGzduuLq6gvo4ceLEoKAgjjXbvNaampqak5ND/RsXF3fp0iUzMzNojcen7mhw0EC40I26R0pKCswQsaQzAANSWlo6JSWlo2WAz6q5tVZvb2+o0MVj3dtJN+ozSOfDS/cQaZ0hjCDdgStXrrx9+3bv3r1tbkFTU/Pp06dv376FaBOKiooK6i/SfVm3bl2vXr1CQkIKCgoEKEZ5eXlgYKCYmBj3aX7hxsbGBvZivXv3LlUYHBwMTrM2Nja8NDJ9+nQZGRkGg3Hnzh2qEBocPXq0vr5+q0SSk5ObOXPmqVOnnJycIBfX5cuXW9VCi+jr6zN73AwYMGDhwoX79++HQGgfHx/+3g5BejIGBgbW1taEEH9//6qqKqocHKmsra2ZI7kQBOmyoNWKIEiPY/To0SNGjKioqLh+/boAxXj06FF2drapqSlsYtEzodPpbm5usGtrXl4eRHbdunWLEOLm5gYZgMGQo7GxevVqOGtqajp06FCYsaqrqyOE5OXlPX78mBAyf/781opUWVkZExNz7969jx8/goU5aNAgfj83B1xcXGBH0MjIyE64HYL0HJYsWUII+fLlS2xsLJSUl5fD7Bic6miozHzc6d27d8fLgiDdFTFBC4Ag/Ofz58+FhYXKysrGxsYshYaGhn369CksLMzOzmYwGOBVqKOjo6ioyNLIq1evGhoaoD71b2lpKSGktLT0+fPnUE1PTw+y6SDdiz/++KOurq6oqEiAMmRkZIwcOXLFihUCDE7rCkyaNGn37t0MBuPBgwdLly5NSUmJjIyUkJCAra0BfX19SK3EDORdB+bPn//s2bPIyMiUlBQTE5MHDx4wGAwtLa1hw4bxLkldXV1aWtqjR4/u378fGhpqYGDg4uIyffp0yDvdCairq3/8+LG44IHh7QAAIABJREFUuLhzbocgPYRx48YpKCiUlpbeu3cPPDgiIyNzc3MVFBTGjRvX4uVFRUUtJmTS0tJiDpplwdDQEGbBuAObeyMIwpn2uBcjPZOu3zfArXfGjBnshUePHv348aOXlxdl0BobG3t7ezOHwwEs2zyym7VAl9qUiAtd/1tDBIjAuwdoexMnTmxqajpw4AAhZNCgQa1qITc3F36kkI154sSJhJDNmzfzeHltbW1iYuI///wDCboMDQ0nTJhw9uxZ7hl92xzX2pwMsBmyiYlJ+1trPwLvFUhXptt1D0hLYWhoCPmfFyxYwHuWivbnEIZJt8GDB3M8+8MPP0DK9LY+XPeg2/UZpDPhpXvgWisihMAiKvxlKXz9+rWvr296erqBgYGTk1NZWdmXL1+2bt3KYDC2bdvGnLcTglcrKyvhXwcHBwaDERMTU1xc3Lt3b8pjUIjT/SFIp7Fs2bI3b948ffo0OTkZ3INBp+QdNTW1cePG+fv737p1a+bMmU+fPiWETJ48mZdr09PTnz59Ghoaev/+fQ0NjcmTJ7u6uk6aNElVVbWtD9QWYmJiEhISCCETJkzozPsiSE9g0aJFN2/eTElJ+fjxo4mJCWwWzWMaeWVlZQhk4IKtrS2XszBR/uHDB3AEYz5VV1cH28ZCID2CIM2BVivSs7h69aqWltb69euXLFmirq4eFxe3d+/ef//9d9euXdOnT2d2OGTh/v37EHgWGhpqZWXFMXk9giBtY/z48XQ6vaKi4sCBA1FRUXQ6HRZGWsXcuXP9/f2joqJOnz5dWVlpZGTExWGPIjIy0s/P79KlS5qammPGjHF1dZ0wYQK/7NWEhIR3795JSEhMmDBBVlYWCu/du6erq6uhoSEvLy8pKQk738THx584caKyslJDQ6MNz44gCHccHR11dHQyMjL8/f1Hjx6dl5eno6PDYwRB//79mffAawNUYrn79++zRNLGxMTExMQQQsaMGdOeWyCI0INWK9KzkJOT27p169q1a+FfMzOzX3755d9//4VJUC5WK4IgHYeOjo61tfXjx499fX0hq2cbvBjs7Oz09PTS0tIuXLhACFm4cCFlKHLh0KFDCQkJzs7OU6dOHT9+PLVnbHPExcW9ffsWjr98+QIHb9++pfIMT5kyhQooOHfu3OHDh2VkZF6+fEltbLN27dohQ4aYm5urq6uDhJmZmQ8ePHj16pWent6yZcu4L9ogCNIGZGVl3dzcDhw4cO3atezsbMj31mn+FHZ2dmZmZnFxcWfPnjUzMzM1NZWVlWUwGBkZGYcOHQJthEffEATpsaDVivQsBgwYQJmsVImKikpBQUF+fr7g5EKQno6Hh0dkZGRlZaWkpKSHh0cbWlBRUZk3b97u3bvz8/OVlZWZkzlxwcHBYdq0aS4uLi3aq0BQUNDWrVtZCq9fv07lo/7w4QNltcKo0tDQAJmNgdGjR8fHx797966wsLC2thYSKWtqak6cOHHSpEltSHqMIAgvTJ48+cCBA/n5+ZA9uDOtRFVV1Z9//nnDhg0vX77ctm0bTJAVFBRER0dfv37d2NjYy8urk0MSEKTbgVYr0rPgmKzVwsICQlwQBBEUEyZMWLlyZVVVlbS0dJsDO93d3cFQ1NXVNTc35+WSzZs3t+oWgwYN8vT05FJBSUmJOp4xY4a0tLS0tLS2tjZVuH///nfv3n369Onr16+we6SKioqpqamNjU3fvn1bJQxH8vPzL1++PHv2bOabIghiYWExaNCgmJiYysrKQYMGWVhYdObdp06dmpqaGh4e/vnz5/DwcCjU19cfOXLkkiVLMC4AQVoErVYEQRBE8KioqBw5cqSdjQwcOPDMmTN8kogzzs7Ozs7OPFaeNm3atGnTWApVVFRa1UhrUVVVLS4udnJyWrdu3aJFi+Tl5TvoRgjSvZCVlfXy8oKF1vHjx/MSQcDfu//2228uLi4vXryIj4+HQktLyyFDhkDycARBuINWK4IgCIIIFZs2bQoICNi8efONGzd+/vnnMWPG9OrVS9BCdV2+fPmSlpYGGeO1tLTMzc0lJCQ67nZhYWHOzs4DBw7kZQPPDiI8PNzFxcXMzOzhw4fM3gFCD8eJpM7Eysqq29mo6L6BdBFEBC0AgiAtcOzYsfT0dEFLgSBIt0FVVRXSMr948WL69OkbNmwoLi4WtFBdlPj4+F27di1YsADsmY0bN3779q3jbldZWQnZd6jg7devX9++ffvBgwfcLywqKrp9+/bt27fLysraL4aVlVX//v3fv38fFhbW/tYQ4YZy3zh69Chfuh+CtA20WhGkFcAEPCRQ6TQGDBgwduzYAwcOlJaWduZ9EQTpvvzwww8qKipNTU319fXnz5/X1NQ8e/ZsdXW1YKXy9vYWFxcfO3ZsTk6OYCUB6urqduzYceXKFWlp6cmTJ8+YMYMQ0qF6eWxsbGhoqKKi4qxZs6DkypUrM2bMmD17dm5uLpcLw8LCZsyYMWfOnJKSkvaLQafTwWy+fPkyc6owBOHIpk2bevXqtXnz5okTJz548KCmpkbQErUFX19fGo1Go9H+++8/LtXS0tLk5eVpNBrktO/K1NXVRUdHb9y4ccCAAfBo8vLyLi4uFy9e7CJjLH9BqxVBWoGWlhYhJD09PS0tDXZZ7ITMw6NHj9bS0tq+ffuwYcPu3r0rcL0TQZCuj5qa2qRJkyByr7GxsaamZs2aNZMnT37y5ElDQ4OgpPr69WtDQ0NRUVFhYaGgZGAmOzv79u3bhJBVq1ZdvXr15s2bf//9t4GBQcfdEXJNOzo66unpQcno0aNhDTYwMJDLhbBDm7m5OXVhO3Fzc5OQkAgNDU1MTORLg4gQIxzuG9bW1rBFNvfdd0NCQsrLy6Wlpa2trTtRurbw7NmzRYsWHT9+vLq6eujQoUOHDtXU1IyIiFiyZMmvv/4qfAvjaLUiSCtwdHSUkJD4+vXrvn37Ll++fOLEicjIyE6477Zt29TV1T99+uTm5jZ79uy8vLxOuGm3o6ys7PXr17du3bp161ZoaGhmZmaH3q6ystLFxYVGo925c6dDb8SdsWPH0mi0c+fOCVAGpGuydetWZWVl6t/6+vonT55MmDDBw8MDYjg7H319fTExMSUlJWbBBAjMPxJCZs2aRafTCSFDhgyBg46AwWCA8ckcWjls2DDYnZjLSJKTk/PkyRNCyNKlS/kljK6uromJCSHk5s2b/GoTEWK6pvtGqzAyMoKg4oCAAMjfzk5DQwPMZDk6OhoZGXW6jK2gqKho/fr1CQkJlpaWPj4+b968efPmzb1796ZNmyYmJnbhwgVqPzbhoakZWqyA9Fi6ft+ATdgmT57cYiHzqcOHDzMXwoQcS2F+fv7cuXP19fXhE1BWVj5z5kyHPcf/g4ODg6ioKCFERESkV69ePj4+VVVVvF/O32/tr7/+EhMTGzNmzLdv3/jSYPthMBhHjx4dNmwYPKaamtrevXs79I5BQUGEEG1t7dzc3KamppKSEti0MyUlhfuFz549u379elRUFF/EuHr1KmzHwmAw2txI1/9RI21j7dq10tLSLO99UVFROp3u5+fX0NDA5dqe0CvAhmzxGZOTk69du5acnNzO2z1//hxul5aWxly+ZcsWQoiMjExzI+rZs2chCS3Lhe1kx44dMHrU1NS09tqe0D0QFjZu3MiceFlcXHz06NHh4eH19fW8XN4V+oyfnx/I8PjxY44VkpOToYKfn1+nS9c6Dh48SAhRUFCIiYlhLi8tLYUJqf79+1dXVwtOwNbBS/fAtVZECJk0aZKnp+ekSZNaLGQ+xbJ128qVK9kLVVRUvL29f/75Z09PT09Pz40bN9ra2nbYc/w//Prrr2pqaoSQ79+/19TUrF271srKKiwsrL6+vnMEYKarufkRQqKion755Zc3b96MGjXK3d3d0tKyo523T5w4QQiZO3cufC9lZWXz5893c3Pz8fHhchWDwVi3bp2bmxulLreTMWPG6OjoxMTEREVF8aVBRJjYvn27goICS2FjY2NFRcXixYsdHBxevnzJrC70HJ4/f/7vv/8GBATAv//+D0pnZSY4OHjOnDmwYwoX0tPToVloOTo6msFgMFd49OgRIURdXV1XV5e5HF5MlZWVzeVkgmVYa2trlguZKSkpgVtzzCZFnS0oKKAKbWxsCCExMTEdmoAKERq6oPtGaxk+fDgY3pT5ykJISAjMEA0fPpxLO1FRUREREZSzBsezWVlZfJKaA/X19TCZ5ezszLI5uby8/JIlSwghnz59+vz5c8fJIADaY/Ii3CkpKQkJCVm2bJmpqSl8mHJycs7OzhcvXiwpKWGvz2AwQkJC3NzcqNzi2trabm5uISEhHOsLCuwbgsLa2hqWWwEajdarVy93d/eKiooWr+Xvt9YF11pXrlxJCDExMfn06VNTU1NeXh4cdBDp6ekyMjKEkHfv3lGFgwYNIoQYGBhw+UaoxZbAwEB+CbNu3TqIUmtzC/ijFmJWrVrV3LY3IiIisrKyixcv5nghX3rF+vXr4UdRXFzMcqqmpgZm/ebMmdPc5fn5+b4tERER0QbB3N3dOX4mp0+fZq/s7e0NqaS4NPj69eu1a9dS85hqampjxow5fvw484OPHTuW4/NWVFT069ePEDJhwgT2Zc/s7GwYbc6fP89FgPT0dMgXePz4cfaz9+7dA8E+fvzIfAkU3r59m0vLHMFBo2ciBO4b4J+voaFRWlrKcqqurs7JyQl8+Lk3YmhoSAhZtGgR+6mioiKIMuD4S6SIiYl50hJcdImMjAwuQ9bbt2/h7KVLl7g/SNeBl+6BVmsHsmfPHjk5ORUVFRMTEwsLC3Nzcx0dHbA69uzZw/JmqqmpuXTpkpycnLS0tJGRkYWFhYWFhaGhoaioqJyc3L59+9rgwNNBYN8QFMHBwSoqKhzfFocOHaqrq+NyrdB/ayNHjoSUKp1zu6NHj0JgGHMhuOvAMk5zF/74449wIS9zDTxy9+5dcC/Mz89vWwtC3z16Mt++fWMfN5gRFxdXUVEJCAhguZAvvYJan7x37x7LqdjYWDh14cKF5i6PiIjgIjng7u7eBsGOHz/u4eFBedN4/A+OfoMtWq1xcXGQVMnIyMjV1dXDw8PV1VVPT09GRsbX15eqpqqqSgjx8vJib2H37t3wK46NjWU5Be4bSkpKeXl53B8K1k5tbGzYFYa5c+eCeCwjD6jXW7du5d4yOzho9ExycnI0NDQ4/hKlpKRsbW2joqK+f//O8dou0mdCQ0NBjBs3brCcSkpKglOhoaHcG9m4cSPk4i4sLGQ5dfnyZfg0wJOlOZydnVsc3D58+NDc5RDoTgjhOG1H5WHavXs39wfpOvDSPdBq7UAkJSX79+//119/JSUlgaP5rVu3qHXX9+/fM1d+/vw5nU4XExObO3cudSoyMhIymNHp9FevXgnoOVjBviFAhgwZIiLCwbFfUlLSwsLi5s2bjY2NHC8U+m8Ngo25L4Y0NTX5+/v7+/u3/3bjx49nN5LT09NBBfzhhx84XlVRUQFyNlehbeTl5cF92/xoQt89ejjLly+HVTguyMnJOTg4BAUFUVfxpVdUVFRAztu5c+eynNq3b1+Lxtjnz58XtMSJEyfaLB6Yoy0+I3ertaamxs3NjRCip6d3+fJlmDzKz88/ceKEra3tggULoBqVc9XHx4e9kQ8fPsB3xH4XFxcX7ivSFGfOnIFbMC+owq3BYGZXYQcPHszLyhI7OGj0WATrvtF+ysrK+vTpw7Hbw3x0nz59ysrKuDfy6tUrcXFxjouZsJZrb2/PvYVt27aNawkuaTKoNMjNOZvA2bVr13IXo+vAS/cQ4/4a675AphNtbW3K25airq4Ols719PTU1dU7ToZJkyb99ttv4DQIjubTp0/Py8tbvXo1IeTFixfwtoCUZQcPHqyoqBgwYMDJkyfl5eWh3N7e/syZM/b29hUVFRcuXOj6ObiRjubPP//08PBgzzhfW1v74cOHhQsX3rx5899//6XRaAISsLMpKSmBSLCvX7+Cv+6VK1fAjAc9kgUI9uB4ioLBYCQnJ6elpVVUVIAfkaGhIfNuEyUlJc+ePSOEQDZCCh0dHWtr68ePH9+6dcvLy4s5awUQExMDcnKMr6aAaBklJaUJEyY0d1ZDQwPWdmBPAhMTk9evX4eHh3N/tBZp5+VI1wRW3rjXKS8vj4qK8vDwmDdvHqhufEFWVnbWrFn79+9/9OhRcXFx7969oby2thZS1zo7O4NBxREjIyNYuOjKJCUlQa7OZcuWLViwAApVVFRWr15tampKOfKlpKT8f+zdd1xTV9w/8BtWgCCIAgqEJSoCKqKCBBBRVByIA8G9R6u2tmDVamur1lbbWmjtUFu3rVVQ60ARUcRFwnKggANRSRRkONhD4PfHeZ77yxPgEkYIST7vP/q63JWTeu/N+d5zzveQBTqfnzgnJ6e+ffveunXrxIkTn3zyCUkHSFGUSCQiDc4zZsxosiRjxozp1KlTcXFxVFRUv3796PXXrl3Ly8vT0tKq/+Qhw/Iby6cKUN+GDRuOHz/e4JSttbW1JSUlf//9d2Rk5L59+5h/6eRFX18/KChox44dMTEx+fn5dFeU6urqEydOkN9BfX195pO4urr26tUrPT391KlT8+bNo9fn5+fHxMRQFDV9+nTmM3z33Xet+RaNDamV8Pjx49Z8SofTmpC3I7OystLW1l65cqXE+pqamoyMDD09PQMDg/379zd4bFVV1Z07d64yEggEpaWlLShYXFwc+R+7fft2eiWpyFIU9ccff9Q/hLxnNTc37yCpwBT92lB0ffv2bbC5ldDU1OzSpUv9d/mt/FejR0zt2LGj/lbSQ7X+C35xMTExB5pSf+Rbk+7cudPg/wdDQ8MG92/yf8Lr169/+eWXCRMm0DXpfv36LVu2TDzlLz1Bef3vu3//frIpNja2/slJplA7Ozvm7sGffPIJqdo2OBSQdAKUaLki78L69evHcFoGLfr1AOWkra1tY2ND3v4QLbuoaFevXiUx2H///UevTE1NJSe/cOFCK8/fGo21tf799997xQQGBpLZccRX0t0L//jjD3KS7Oxshs+iezs31jby448/kh3EHyy7du0iFQAp+/+TV12urq7inYRJxMvj8ervT7op9u3bV5qTi2urywMUkRy7b7SJmJgY0lIqPjzhwYMHpBIVExMjzUm2bNlCXsyJ9xbZt28faabKysqSTdn/B/3sYm5r9fX1lWkx2pA0l4fSRq1LlixhsVjW1tYS1b6ysrIdO3awWCwul5uSktLgsXl5ecOGDWO+G7lcbnp6egsKRjrwaGhoHD9+nF5JT6nUYKX/t99+I1szMjJa8IltTtGvDUV39uzZJqcT1NXVdXR0FM/30/p/NR6PV78yRJAqUZ8+fRiCsVYO4WhMdnb2ggULFixYQM4wePBg8ueKFSsa3J/5f0JFRcW2bds4HI6WltaoUaPIqcgkvcOHDy8sLCS70ZOj1v++eXl5JMXiwoULJTYVFRWRBtvvvvuO+UuRHIYStXyCrutL9EqinxJ0IZulyX8aUCmdO3emX0W1/lFfXFw8aNAgif5427ZtazJ1WTtoLGo1NDRs8v+Sra0t2Xnp0qVkIjTmz2oyan306BFp4dm2bRu9kjw5pe/mR/cbTE5OJmsKCwtJa9Jff/1Vf3/6ySzl+WltdXmAInr58mX95OT1qaurd+3alW5A6jjXTFFREemM4O/vT68MDQ0lL3+LioqkOUl6ejpJkyaeD8nf35+iqICAANkU/P/bsWMH8/OEbJ09e7asS9JWpLk8lLaHcEBAwP79+1+/fn3p0iXylpSorKyMjo7W1NR0dnaWmNSERrYyNGeR3ydysUqvsLBQJBKRRNWDBg0iuQQJugVfvEsPjaQWpCgqNze3T58+zfpQUD5+fn5mZmZksHRj+5SVlWVkZMyZM2fKlCnffPMNGcLRSgsXLuTz+YmJiQ8fPhRPs07uMoqi5s6dW79PLM3X15fL5TJ/BN17UHoWFhbk1SZp5AwMDFyzZk1zT0ITCASbN28uKyubOXPm2rVryddMTEz8448/zp07l5ubS0pIEjYYGRnV/77GxsajR48+cuRIZGSkeH9I0j342bNnbDZ7/PjxzMXw8PCwsbF5+vRpeHj4pEmTxDeRSWKNjIwkOg9bWlqShaysrBb8b6Qp4aTkQFHV1dXz58+XZpYsLS0tf3//zZs3kwyZbUJPT2/q1KkpKSnR0dFCodDCwqKyspL0xAsMDGR4aJBfPXpymsbY2tqOGDGisa1dunR58+aNxMonT5706NGD4Zxz584V7zR79+7dxMREV1dXesgPudnJAsnE2/pf5169eg0ZMiQmJubEiROffvopm80WCoUk1hXvuj99+nQ6NKX9+++/pEfi8OHDjY2N8/Pz//nnH/Ky4OrVq/n5+fr6+qTfVoOafDgzUJ0BKdBcNTU1hYWFf/7559mzZzdv3izv4vx/nTp1CgwMvHfv3uXLl3Nzc7t3715VVUU/lOiGgd27d5PpCcQtW7aMdK+wt7cfPHjw1atXDx8+vGDBAi0trdzc3MuXL1MUNWvWrCbLcOPGjVevXjHvM3LkSHrMoAT6R59Zg2GF4lLaqNXFxcXa2looFEZFRdFRa21tbW5ublxcnLa2Nnkd0qDOnTuHhYW1STFevHiRkZFBlhMTE//777+nT58OGTJk69at4p3mc3JyGE5CJxmX9fyTzeXu7i7vIqgoFovFYrGYm8hqa2tfv369b9++w4cP1x/d3QK+vr76+vpFRUVRUVHiUSupErHZbOYRLMHBwa0vg6zt2rWrrKysR48e27Zto/+nubq62tjY9OzZk66kktdMdnZ2DZ5kxowZR44cycvLu3r1KsnKQJw8eZL0xJOYWq0+MhTwhx9+qD8UkPys+vr6SmSFpZuGGhxrJD3xd3ygND755JPa2lrmfdTU1GxsbPbv3z948GA2m8383ra5xo8fv3Xr1qKionPnzn344YcPHz5MSkpis9kBAQHMB2ZmZpKWTAbTpk1jiFrnzZtXf9Bmk4PWfv75Z/E/f/jhh8TExICAgAZfipGz1Y+NG1NVVdXYpmnTpsXExCQlJZGXg+fOnSsrK7O1tRV/ye7j41O/Iku/ZTA2Np4wYcK+fftOnjy5ceNGfX19EuKOHDmSITR1dHSUsvAAzVVRUfHmzZsm+4i1Mz8/vy1btpBJkhcvXpyZmXnz5k2Jsd+2trb1cz2I34yzZ8++evXqzZs3MzMzHRwcIiMjS0tLLSwspKkeb9myhc5m3Jg7d+6IvykTR9/OhYWF9bcWFBSQha5duzZZEgWitFGrtrb2lClTfvzxxytXrtDVvsrKypiYmLKyMhsbG/GmTtmJjIyUeE8zaNCgZcuW9e3bV3yllKOlpRx73W74fL68iwBNqK2trayszMzMbP2pLCwsvLy8IiMjjx8//sknn9ApBEmVaPDgwR3wlV5GRkaDM2fQmTYJHx8fW1vbiooK8pZ07NixEnG+sbHxl19+Sf9JKsGNtRG5ublxuVyRSHTs2DE6ai0qKiJRK5l/okl+fn6//PJLfn6+eOhL6vqkIaixA5t8dwuqpqSkZNeuXTU1NY3twGKxLCwswsLCxo8fr6mp2bbxKtGvXz83N7eLFy+ePHnyww8/JF0G+vfvL5HPrL7u3bvXb+uQQFoUG9NW76AZkBdYaWlphYWFDHVEus/Ly5cvG9uHvJDKz88/f/58//79yUMjMDBQvG/XkiVLlixZwlCeBQsW7Nu37/nz53fu3HF0dIyNjaUT0dVHZsigkz8BtC1ZdN9oE87OzgMGDCDtSYsXLyYPJQcHB2dnZ3qfkSNHjhw5kuEk/v7+a9euff369fnz5x0cHP777z/SM4IkOWPm7e3dZMcohm7YFhYWWlpaVVVV165dmzhxosRWel6cJp+xCqY13Ys7surq6mvXrmlra3fq1Omff/4hK9+8eTNu3Dhtbe0G5wWWhfPnz4/7X56enn369NHU1DQ1Nd20adPLly/p3ZgHltDV7iZn9WgfcrpUoW205p8+IiKCnCQxMZGsKSgoII1+e/fubaPrq4VIwSTuEZLIpEn//vtvXV0dHds3OPpLHLlhGZIcrFy5ksS69ExuJIGTvr7+48ePpfk6JSUlgwcPpihq0qRJ9MqtW7eSt78lJSUS+7fyKdEmlwd0TMuXL2cIRLW1tadPny4SiepPsdi2VwXpya+rq/v48WMSZ4qP3pSXNpn55ty5c+Qk9Seeffz4sfjEjyQ4/PLLLxk+a86cOSQUv3//vq6uLpvNTkpKas53qispKenZsydpYyeJmk1MTPLz8xvcmTzAWzA9Bh4aqmzlypXq6urMP6xqamq2trbXrl0rKysjc/J1tGuGzITM4XAePXrk5uZGUVRoaGhzT0J65ru5uT19+pS8XYqLi5NNeSWRALtfv34SGXwqKiqmTp3a4PzMHZk0l4fStrVqaGj07du3X79+d+7ciYiICAwMVFdXz8nJuXr1qo6ODnOvpKqqqtTUVObePtra2gMHDmxyaOvYsWPJvI5kZo5bt27t27cvJibm66+/rqys/Prrr0kSNroPMDNp8kO0p/j4eHkXQRVVV1ePGjWKoY8ZTVNTc+jQoUuXLjU1NW0ywZg0vL296RFT5AUePWJq9OjRzMeeO3eOngGiMUFBQY21VDAPL2mMg4PDsmXLxNfs3LmTHCi+ktTw6I764pPctExgYOCOHTtIS+mUKVPo7sE8Ho98FhkpR899RbO1tSXBM4fDmTp1anJy8sWLF7Ozsy0tLSsqKkgFVKLhRUKbjGEGpfH27ds///yzfvdgFoulpaXVu3fv6Ohomc4ARxs9erSBgcG7d+9+//33lJQUAwODjjkrRgu4urr27NkzMzPz999/t7e3d3BwIIMpbt++ffDgwTdv3tCPRxsbmwcPHtCzBjQOqy7RAAAgAElEQVRo+vTphw8fTklJ2b59e1lZmaurK3mBJT3y9Ni2bdt///1HHmv+/v4kS5yEgoKC/Px8Mu9OM780qK6O0H2jTdAzRW3fvl0gEHTq1KnJMQv1zZw58+jRowKBYOfOnaWlpXZ2dsy9P9rQokWLQkJC7t2799dff82aNcvc3JyMTLxx40ZUVJSWltbKlSuZEwcoHKWNWklgGRAQkJSUdOPGDaFQaGpqGhMTU15ebmNjwzzx6bt37z777DN6cosGcbncixcv2tvbS18eGxsbGxubQYMGBQQE3Lp1a8eOHUuWLCH1Y+a0ELRmfVw7IElloZ0dOHCgySFq5Dfjp59+8vPzY7PZbZUtw8jIaOLEiXv27Pnvv/82b95Mj5gaPXp0k8k8fv311yaHcLi7uzcWtTo6Oq5YsUJi5dChQ5lPOHToUIl9SNTaYKxLh4Jv375lPi3BMILU2dmZ1GKPHTs2ZcqUoqIi0nFo2rRp9D5GRkb1v5F4zdLPz2/r1q3v3r2LjIxcvnz5gwcPUlJS2Gw2eYfaGCkfJqAi1q5d+/79e4mVWlpa1tbW5PnQbiUxNzcfPXp0RETE33//TX4+FGgsJXm/3NhUH0ZGRiEhIRs3bkxJSfn66695PF7Xrl0LCwsvX76clJS0fv16ek8PD48HDx7cunWL4bNcXV1NTEzy8vJIarQWVKMpipo6dWpYWFh2djYZzjB//vwGd7t//z5ZEO8VCcCswacKTVtbe9KkSdu3bzczM+vgmbosLS2HDBly6dIl8lAaMmSIlCmOxLm5uZHsiQcOHCAD6dstUAwKCjp//vz58+c3bdqUk5NDRmndu3fv1KlT79+/nzp1qvJNwK7MUStJD/Ptt99WVlbGxsZOnTr1woUL2traEydOZJjTnPwyubi40MP2GtRg+lBpWFtbT5gw4datWyUlJenp6SRqpdt2GhwVQ4+0VrJB1dACFRUVH3zwAcMPBom+fvjhhyVLlqirq7f5O8758+fv2bMnOzv79u3b9IgpeuIZBv7+/r1792bep8HWAMLT09PT07NFRZaWhYUFm82urKxMSEhgjgxJiM7QYMLhcGbNmrVp06bY2NiCgoK0tLTs7GwDAwPxFmlzc3N6upoGOTo68ni8Cxcu/Pfff8uXLyejbpycnBp8j1tSUkIWyBx0AOS3g2Stp2lqanbu3JnkRmr/ZvkFCxacOXOmoKCAzWaTfrByRzLENDmq08XFZeXKlQwjxObOnVtYWHjhwoU7d+5cvHiRTNjYq1evhQsXLlq0iN5t1KhRe/fuzcjIePnypZmZWYOnMjIyCgwM/P3338vKykxMTFr2ZmHQoEFDhgy5du1aQUHB4MGD63frIFJSUkj/YUxPAFLqON032sScOXOuX79eVlbW4oeSsbHxrFmztmzZkpeXZ2xs3J6vAo2NjUnGtdTU1H379hUVFZGBSCSt+qZNmySyNioBZY5a1dTUuFyup6fn5cuXz549S57gbDa7ya6MBgYG9GTfskBXK0kWBPHmkRs3btQfVE2mFTE0NOxoba3Q/v7+++/GuuWwWCz6HaepqamM3nEOGDCgV69ejx8/PnHiRH5+fkFBgYmJyZAhQ5o8cPny5bIoTxsyMjIaMGBAQkICCTXFQ+iKiorTp0/7+PiQlSSbWnZ29rt37xrLSh8UFLRt27aCgoLo6OiEhATSIk068Ehv2rRpFy5ciI+Pf/ToEcke3Fg4LRQKyUJrZrAAJbN69Wp6sJC6urqhoaG7u/vu3bvl1Y3c1dU1JCSkvLxcR0dHmgmc24Gbm9unn36qo6PDvJuHh4eHhwfDDhwOJzg42N3d/c6dO+Rm7Nq1q7Ozs5ubm/jr5qFDh5Ju0rGxsbNnz27sbMuXLyf1BAsLCwcHhxZ9M2rNmjUk2enIkSMbG1MQFRVFUdS4ceOaO5MfqKyO032jTYwbN+6jjz4qKyvT1dWVmE9OetOmTSPNS5aWlu2cltLFxeXXX3+9dOlSeno6yRtsZGQ0ePBgd3d3hmYABdaaQbEdX0VFxd69e0m2z9WrV6urqw8cOFC+Q5MrKipIk72Wltbdu3fJymfPnpGW26VLl1ZUVIjvn5eXR2LajjNTsHJcG4qoqKhIQ6OBN00sFktHR8fOzo6eVr6+NvxXIx3eLCwsSAS1dOnS1p+z9ci3azIXEfP/BLrn8JYtW54+fUpWPnz48LfffrOwsKBzUNFZqVJTUxk+i2R38PHxIRmJz58/39wv9eLFCxIVf/zxx+SFWlpaWoN7rlq1iqKobt26NfcjCNzUyic3N5f+Z9XT03NxcYmKimrWGXBVyAKpGQcEBMi7IHVZWVkkXG/uhUHg8lBBBQUFEi/ENTU1jY2N58+fn5OT0+ThuGaAgTSXhzK3tZLbyc3NrVu3bvn5+QcPHtTR0ZkxY0b79Dh//PhxZmZmz549DQwM6A7JL168iI+PJ/kGXV1d6SZWKyur8ePHHzt27NSpUyTRtqGhYWVlZU5Ozt9//52VldW1a9f6Q+BA1Wzfvr1+Q6uWlpahoeHevXvHjx/fPsWYOnVqaGioUChkHjHVMTH3/J84cWJkZOT58+d//vnn58+fk94Nt2/fjoqKMjMzo9tM6OnaMjIyGF6sBgQECAQCPp9fVlbWrVs35uH0DTIzMxszZsyxY8f+/fdfMu63sYYX0tNP1p2oQYGsXr2aoigdHR1zc3N/f/+ffvpJ3iUCiryAPn/+fFxcXH5+vnz77507d668vNzOzk7Z5sYAmelo3TdA5bQm5FUIxcXFJF8oi8WysbG5c+dO+3zuvn37bGxs5s+f/8UXXxz4XyEhITY2NiRR9blz58T3v3PnDpnzzcbG5ptvvjlw4MBvv/22bNkyDofTtWvXzz//vH2KLQ2luTYUy5s3byTecaqrq3fr1m3hwoXt/47T29ubnG3IkCGlpaVtcs5WItOa/fzzz8y7ffnll8zTTty+fXv69Ol2dnZ0fGtnZzd+/Pjjx4+L70bu1hUrVjCcKj09nZ60beXKlc38Qv8jKiqKlERbW/vIkSMN7vP27VsSUf/+++8t+xTc1EpGKBRqaGhYWlrOmDEjNze3ZSfBVSELhYWFZJTpwYMH5ViMsrKy4cOHt2b+IVweqgbdN0CmpLk8lLytlVT1pk2bJhKJ1NXV+/fv327p3R0dHZ2cnG7fvh0TE/PixQuy0sjIyMjIaNKkSXPmzJHoQO/k5PTFF18cO3YsPT19y5YtlZWVZH8nJydvb+9169a1T7GhwyJ9X8kyecdpa2t76tQpubzjXLt2LXk9P2LECCnnbZK1zz//vLCwsMkRtt988w3zDgMGDPjuu+/IUNLy8nJybzo6OkqkMwkMDNyyZculS5fIIL0GT2Vvb79+/XqRSERR1MKFC5v/nSjSKWPNmjXMQwFTUlIKCwu1tbVHjBjRsk8BJRMaGurl5bVu3bqRI0fKuyzwf3Tp0mXlypXLly/fv3//3Llz5VWM9PR0gUBgY2MjntgcgAG6b4DcscSj2/+z4X9bdRrbAZokEomSkpKys7PT0tLIGisrK2tr62HDhjWWMSUzMzM2NjY9PZ30vbSysho6dOjAgQM71IRLuDbaX2FhIT2wnsPh9OnT59tvv21WOhP8q7UtgUBAZn5KTk5ut8nZGrNixYo//vjD3d395s2bLTsDLg9lUltbu3bt2tbnFMRVISOvX78m+cO/+uoreZXh7t27R48eJVmOW3YGXB4qRSQS2djYmJmZeXh4hIWF0d2ImgXXDDCQ5vJA1ArNhmuj/a1evXr79u2amprW1ta+vr5ffvllc38z8K/WtsrKyjw9PW/fvr158+YNGzbIsSRv377t16+fSCTavXv30qVLW3YSXB5QH64KYIDLQ6WEhITcvXu3ld03cM0AA2kujzaeyxEA2tyrV69+/vlnKysrb2/vGzdu/Prrry17zQltSFdX95NPPqEo6vjx42/fvpVjSeLj40UiUY8ePSZMmCDHYgAAgFKqra1VV1e/fPkyRhyAfCFqBejodu3a5e3tvXfv3osXL9L5qEHuJkyY4OHhkZqaSvL3ysvhw4cpilqwYIECTewOAACKQk1NrfUjDgBaT/mzMQEotNra2jt37sTExMi7ICCpS5cuGzduvHbtmr6+vhyL4erq2qtXrzlz5sixDAAA0KT8/PyLFy+mp6fn5+dTFGVsbOzg4DB69Gj5zoEEoCgwrhWaDdeGIsK/GjDA5QH14aoABrg8muvx48fffvttQkLCixcviouLKYrq1KmTubn5kCFDli9f3oIJvRUOrhlggGxMIBO4NhQR/tWAAS4PqA9XBTDA5dEs+fn5y5YtO3v2rLm5+cyZM3v16kVRVGpq6u7du6urq318fA4ePKj0La64ZoCBNJcHeggDAAAAAMjKsWPHzp49q6mp+f333w8bNoykqHjx4oWhoeGGDRsuX74cGRm5YMECeRcToENDWys0G64NRYR/NWCAywPqw1UBDHB5SK+kpGTgwIGPHz+eN2/e7t272Ww2vSk/P9/NzS0rK2v48OGxsbFyLabM4ZoBBpj5BgAAAABU1/Pnz6dNmzZt2rTbt28zbH3w4IGMCnD//v3Hjx9TFDV58mTxkJUkZBo3bhxFUUlJSa9evZJRAQCUA3oIAwAAAIBy6ty587lz50pLS62srJydnSW2nj9/Pjw8nKKo77//vrEzTJ06lfkjOBzOwYMHG9t6584dsuDp6Vl/q4eHx2+//VZSUiIUCjEZOwADRK0AAAAAoJwMDAz8/f3//fffI0eObNiwoVOnTuJbjx49SlHUmDFjzMzMGjvDiRMnmD/C0NCQYWtubi5Z6Nq1a/2t3bt3JwuvX79m/hQAFYeoFQAAAOQmJyfn559/Jv0n3dzcGPbcu3fvo0eP+vfvP2vWrHYsoGyVlZUlJibeu3dPJBJRFKWjo9OrVy8PDw9ra+vmnionJ+f8+fOPHj3q0qXL2rVrZVNehTRnzpx///33xYsXiYmJPj4+9PqnT5+mpKRQFBUUFKSlpdXY4WfOnGE+v6amJsPWjIwMhq0aGv9TFX/y5AnzpwCoOEStAAAAIDcaGhq//vpreXk5yUzT2G6FhYVbtmx59uzZF1980b4FlKHCwsK//vorKirq0aNHpEVOW1ubdGSdO3fu2LFjpT/VlStXDhw4cO3atWfPnnXu3BlRqzgPDw9TU9OcnJwzZ86IR62k57Cenp6fnx/D4RMmTGjNp797906a3cgkrgDQGEStAAAAIDfGxsZubm5Xrlw5f/58YWFhg70oSbqaZ8+eURQ1fvz4di+jrPz22287d+4sKioKCAgYMGAAaS8NDw8/evTo06dPra2t7e3tmzzJ06dPjx49euHChWvXrpE1b9++lX3ZFYm+vv7UqVN//fXX8PDwb775Rl9fn6wn3YMnT56s9HOlAigB5BAGAAAAeVq4cCFFUa9evUpMTGxsn2PHjlEU5ezsXD+hjoK6ffv2zp07X716tWLFii+//HLVqlWrVq1au3btV199paurm5CQsHPnziZP8vLly88///z777/Py8v7+OOP+/Tp0y5lVzwzZ84kQ0wvX75M1jx58uTWrVsURc2ePVumH21qairNbo6OjjItBoCiQ1srALSf+Pj4iIgIiqJWr17NkPqitLT022+/LS8vDwwMdHd3b98yylB6enpycvKDBw/Ky8spirKwsHBzc1OmLwjQMr6+vkZGRgUFBeHh4Q12iy0sLIyKiqIoKiAgQFtbWx5lpLKysmJiYnr16jVixIg2OeGuXbtevXrVp0+f4OBg+nlobGw8e/bs06dPR0ZGhoeHf/311401PhP5+fmxsbHTpk0bO3asq6vro0ePZDeDi0JzcnKys7N7+PDh/v37J0+eTFFUZGRkeXm5mZlZkw/hJv/F9fT0GMa+2tjYSFNCAwMDaXYDUFnKH7VWVFScPHmyrq7Ozc3N1ta2fT60vLz88uXLx48f5/P5jx49oiiKzWY7OTkNGzZs4sSJLi4uDIP+AZRYcXExSbvi5OQ0f/78xna7e/duaGhoZWXlmDFj2reAslJaWrpz587r169nZGRkZ2dXVlZSFGViYuLo6Dhu3Lhly5ZxOBx5lxFAboyNjYcPHx4REdFYJ+HExEQymyWZ3LIxn3/+eXl5+ahRoxocpki2+vv7i49slEZWVlZ0dHRsbGxSUtKqVavaJGotLS09deoURVGjRo2SeIWnra09ffr0yMjIV69epaamDh8+nOE85ubm27dvHzZsWAuyN6kUHR2dxYsXr169Oi4u7uXLl2ZmZqR78MKFC/X09JiPvXLlCvMOzDmEraysyMK9e/f69esnsfX+/ftkof4mABCn/FFrcXHxkiVL1NXVw8LC2idqraysvHr16hdffPHo0aOBAwe6uLhoaGi8fv06LS1tx44dt2/f3rp16+DBg9uhJAAdzaBBg0iLyrFjxxii1sjIyMrKSktLy0GDBrVvAWXlypUrP/74Y0lJiaenJxmV9/Tp05iYmCtXrqSlpZmYmMydO1feZQSQp7lz50ZEROTl5cXFxQUEBEhsJQHG0KFDmcd5Xrt2jc/n3759u37UmpaW9vPPP1dWVjbr9/fJkyfR0dGXL19OTk7mcDhTpkyhQ9Y//viDOTcsiZPNzc0b3PTs2bO8vDyKory8vOpvHTJkCFl48OABc9RqZGQ0b948qb+QSps8efLq1auLi4uvX78+aNAgMo0qaXdlduPGDeYd6DzADbKzs6PPUz80PX36NEVRffr0QVsrADPlj1rr6urKysr09PQqKira4eNqa2uzs7O///77R48eeXt7r1271tXVlc1mC4XCkydP/vDDDwKBYM+ePf3790dzK6ggIyOjgICA3bt38/n8Fy9eNFifKy0tJb2IJ02aZGRkJI9itr2nT59aWFgEBgYOGzaMvHfPzc11dnbeuHFjXl7ejz/+iKgVVJyXl5elpWV2dvahQ4ckotaCgoILFy5QFDV9+nTm7sGBgYF8Pj8xMTEtLU1ilOC5c+cqKyuNjIwajBLre/LkyYULF2JjY5OTk8vKygIDA8eOHTt48GB6jOKZM2eio6OZT7J48eLGotacnByyQE/XKY7L5ZIFEtlCm7Cysho5cuSlS5cOHTr04sWLiooKe3t7aUaTenh4tOZz+/fvb25u/uLFi8OHD8+cOVM8Or179+7169cpilq6dGlrPgJAFSh/1NrOKioqrl27dvXqVSsrq1WrVnl7e5P11tbWs2fPTk1NPXjwYExMzLNnz3r37i3vwgLIwcyZM3fv3v3u3bvo6GiSgkXC7du3MzMzyQA2eRSQoigqOTn5zJkz8+bNa6sOGj4+Pn369BkyZAidu9LU1NTS0jI8PDw9Pf3+/fsikYiupwKoIH19/cmTJ//yyy9xcXESt0NCQkJeXp6uri7z9CTkofHll1+WlZVFRkZKRCPHjx8nAxTp7pqNefLkyfnz52NjY1NSUioqKvz9/UeMGOHp6WlpaSm+28cffzxx4kTmUzHc1CQfcmPo4Jw8DKFNaGhoTJky5dKlS1evXs3PzyexIpvNlvXn6urqfvnll8uWLbt169by5cs3btzYq1evd+/eJSQkbNiwobS01N7eHg3mAE1S5qg1Jyfn3LlzZP6r9+/fx8fHk2eTtra2r6+vjLKcFxcXnzt3TlNTs1evXhLj+w0MDCZPnnzw4MHS0lKBQICoFVTTgAEDrKysnj9/fuzYsQaj1sjISPJSnMwD0ZiQkJCysrKxY8c2WHEkWydPnuzr69us4iUlJZ05c4bP5yclJfn7+zfrWAYODg4ODg4SK7t27WphYZGenk6SzSBqBRU3ZcqUX375paio6OLFi+IPB5I92MPDQyJurM/S0tLDwyMmJubEiRPiE5bev38/NTWVoqhp06YxHJ6ZmRkVFXX58uVbt24VFhb6+voGBga6uLj07Nmz/s6tnIDn9evX0uxGgitoK9OnT//888+LiorI9TBp0qT2+dyZM2eSdCenTp26ffu2jo7O+/fvi4uLs7OzHRwc9u3b16VLl/YpCYDiUuao9eHDh0uWLCHLFRUVR44cOXLkCEVRXbp0iYqKajBqra6uvnv37u3btxlOq62t7e7u3lgLTHl5eWJiora29qBBg3R1dcU3sdlse3t7Q0PDioqKtLS01n05AEWlr68/c+bMrVu3CgSCzMxMiepgaWkpaRKZOXMm3SzZoMTExJs3b96/f79+1Hrv3r0//vijsrLS09NT+oIlJSWdPn1aIBAkJSU5OzuvXbuWTvz4yy+/kNiSwYYNG1oTdiJkBRgwYICjo2NaWpr4Ky26ezCZuaRJM2fOjImJSU1NFc98Q4bKW1lZDRs2jOHYDRs23Lhx4/Xr12PGjPHx8fHw8HBycmqLbwYdhaGh4YwZM3bv3l1ZWbl48WILC4v2+Vx9ff2wsLDx48cfPXqUz+cXFRWRt5nr1q3z9/cfOHBg+xQDQKEpc9RqZmb2wQcflJeXHzp0SFNT09XVtW/fvhRFcTgcExOTBg+pqKj477//vvvuO4bTGhkZ/fLLLw1GrXV1daWlpS9evDAyMmpwBzabbWNj8+DBA5ILEUA1TZ8+fevWrUVFRadPn161apX4plu3bj158oTsw3ySwMDAmzdvJicn18/KSAawGRsbM9dQaYmJiadOnRIIBCkpKRYWFsHBwaNGjerfv3+nTp3IDlFRUU0OYFu+fHlzI8+SkhLyAsva2pp5cgsAVaCvrz9t2rSvvvpKIBAIhUISUQgEgvz8fGNjY3pGHKFQuHnzZoljjY2NyW/32LFjjY2N8/Pzw8PD6ScDeRc2ZcoU5hstOjr6zZs3hoaG3t7eixYtkmnfUSnb1jD/apvbtWvXrl272v9zuVzu/PnzGdIQAgAzZY5ae/fuvWvXrry8vEOHDrHZ7BkzZqxYsYL5EBLcfvjhhwz7cDicXr16Nbjp/fv3ubm5DMeqqanp6upWV1e/ePFCui8BoITs7OxcXV0TExP//fdfiaiVdA92dXWlky42JiAgYP369WQAm0TUSmqoI0eObPI9emJi4smTJxMSElJSUqysrJYvXz58+PDBgwdLVChDQkKCgoKYT9WCd/aXLl0SiUQURc2aNau5xwIopYkTJ3711VdFRUXR0dGLFy+mswf7+Ph069aN7PP69es9e/ZIHGhra0ui1m7duvn4+Bw9evTIkSNr167V09O7d+8emVykyWyxH3/88cmTJx8/fnzs2LGXL19OnjzZ1dW1sZ3DwsKa7Db19ddfN/ZkkPKJwTCvNQCASlHmqLUFtLW1J06c2GR+hcbU1NRIMwSlurr65cuXLfsIACXAZrMDAgISExPv3buXmprav39/sr6kpIRkDw4ICGiylYPL5Xp5eV24cOH48ePr1q2j15OegRRFMceZCQkJJF69deuWjo7OokWLxo4d6+TkRNeMxY0ePbql37VR+fn5YWFhFEX17dt30aJFbX5+AEVEv9I6duzY4sWL8/PzSTcH8fGoTk5OdXV1DCeZN2/e0aNHs7Kybt265eXlRboHu7q6Mg+VJz0mPDw84uLizp49+/vvv/P5/CFDhsyaNYt+RomLjo5usgvGxx9/3Fh0SucWzszMrD+W4fHjx2ShwSG1AAAqCFErAMjB2LFjN2/eXFpaGhkZSdcIb9269fTpUw6HQ3cFZDZz5swLFy7cv3//7t279PCzyMjIqqoqGxsbhu7B2dnZa9asISkxZs+ePXLkyCFDhjQ2QYUslJSUfP/99wKBgMPhrFu3jh5AC6Di2Gz27NmzExMTExIShELhnTt3CgoKTExMpJyuhvDw8LCxsXn69GlkZKSXlxfpfBEQEED3+W9Mt27dRo8ePWDAgOHDh8fFxZ05c2bnzp23bt0aM2aMv7+/RDerVatWNTmQgaFB1crKisPhlJaWXr16tX6v0ZiYGLLQZKQNAKAiELW2JRaLpaOj0+Rumpqa9IRvAKqpd+/eXl5eUVFRx48fX79+PVl59uxZMm0jnWH7ypUrBw4ckDh2xIgRZJIAX19fExOTvLy8Y8eO0VErXUM1NDRs7NPfvHlz7do1iqJMTEwmTZoki6ZUZkeOHDlw4EBVVdWqVavaMFMxQBvicrmkB3s7T8s0ZcqUdevWFRcXnzhxIjExkTS0NivDaqdOnaZMmfLTTz9FRERMmTKFdA8eN26clIebmJiMGjXKycmJjl1DQ0MvXbrk4+Pj7+9PP51GjRrVou/3/wtJnoEXL17Mzs4WT49cUlJy+PBh8qxrz7dpAAAdWaNRq7x+ruSruro6JSUlOTmZYR8dHZ2hQ4c2OG+NhoaGNOGolpZWjx49WldSgObpaHc0m82ePHlyVFRUWloaaSmluwdPnjyZ7h786NGjQ4cOSRzL4XBI1Eoql//888+RI0fWr1+vp6d39+5dMtKMeT4DS0vLFStWRERE5OXl/fTTT3fu3Jk0aRLDZFQ//PAD6XXM4Ntvv21yWg7iwIEDP/30U2Fh4YoVK1asWKGnpyfNUQAqwtzcnIRzhw4dys7ObnK6mgZNnjz5p59+evbs2fbt26uqqnx8fBpLSNEYExOTkSNH9u/fn8Sup0+fDgsLu3Tp0saNG93c3JpbngYtX7782rVrL1++XL169fr168mrt7t37/7777+3bt3icDjBwcHiYyV+/PHHe/fu2djYbNq0qU0K0GLk1wTJz6FZOlo9BBQO2lr/j4qKirNnz0qTQ7jBCq66unrXrl07derUWFomMqJVU1Oze/fubVrw9oPfKmgr48ePJx3kIiMjnZyckpOTnz9/zuFwxGdB/OCDDz744AOGk8ybN++ff/55/vx5cnKyt7c36R7s5ubGPF+FoaHh6tWrfX19L168GBERce/ePdKQMmPGjAYjz9jY2CYHsH322WfSRK379+/funXr48ePP/roo88++6wjNKTgpoYGWVhYkGtDKBS287VBv5A3LtEAACAASURBVNKqqqrq0aNHC6afcXJycnNzEwgE9LDYliUENjEx8fHx6d+//4gRI+Li4k6dOpWSktJWUau3t/cHH3wQGhp66tSpvLw88jR48eJFamqqpqbmpk2bvL29xfcPCwvLycnp0qWLRNQ6e/ZseplMQyq+0s3N7aOPPmqTAtP4fD5Z4PF4bXtmAFBBUtZDGo1a5fhzJUdaWlo8Hm/lypUM+3A4HIbsplpaWj179kxPT09MTKysrBT/mayurs7KysrKyjI1NVXcKeDwW6WgOuAdbWZmNn78+PDw8IiIiC+++IJkD/b29m5Wzkwej9ejR4+srKzIyEhvb2/SWjt16tQmGzCtrKysrKycnJx8fX1jYmKOHTt27969uLi4wMBAPz8/icmx1q1b1+R0BVZWVk2Wdt++fVu3bs3MzFy5cuWqVaukbJuVNdzU0CA3NzdybURERLTztTF+/HhyX1MUtXTp0hb0R9DT05s9e7ZAICgpKenRo4f4u7AWMDY2Hj58eN++fYcPH95gwraW0dPTW7lypaWlZWRkJHn+kLG1Xl5eo0ePnjFjhsQXJ0OQOnfuLHGef/75p/7J6ZXv37+XXdTaQX5NQCF0wHoIdBDS1kPqGhEcHEx2CA4ObmwfhZCXl8dms/X09EJDQ9vh4woKCj788EMWi9W7d+87d+5IbPr000/V1NScnJwyMzPboTCyoDQXhqrpmP9wZCCrlpZWTEwMSVty4sSJ5p5kzZo1pNPvzZs3tbS0KIpKS0tr1hmeP38eGRm5cuXKbt269ezZc/z48Xv27Hn16lVzS8Jsz549JB3oypUrnz9/3rYnb42OeW2A3IWHh9PVCHmXBTqWwMBAcm2Eh4fLuyygMPBbA42R8tpQayyapYNdgUDQwsC5Y1BXV7e0tKyurk5OTi4sLKypqXn+/HlRUZGMPk5PT2/8+PFdu3bNycnZuXPngwcPKisra2pqhELh2bNnT58+ra+vP2HCBFtbWxkVQNboRnw0yyiWjnlHe3p6duvWraqq6ptvvhEKhd26dRsxYkRzT0KGsGZnZ//www9VVVWjR49u7lwRlpaW48eP/+yzz/bv3+/n55ecnLx169b58+e/evWquYVpzOnTp0kr6+jRo/38/MrKyh78X8+fP2+rz2ou3NTQIPp6oN+CAxCkVwseGtAsHbMeAh2BlPUQVmOTnolEIjpjO/PEaB1cSUnJF1988euvv3bp0mXRokVGRkYvXrz44IMP7O3tZfSJhYWFGzZs2Lt3L5vN9vf3d3Bw0NDQePbsWVxcnFAoDAwM/PLLLxU3GxOLxSIL6OChWDrsHT1v3rxDhw5paWlVVVXNnTv34MGDzT1DaWmpr6/vzZs3ySjZPXv2tGb6U6FQmJ6eHh0d/e+//549e3bw4MEtPpW4OXPm/P333xRF9ejRo8HJMDQ0NC5dutQmn9VcuKmhMXSPvvDwcLp5DVRcREQEmQ07MDCQbpAHaFKHrYeA3ElbD2Foh6UPU+geINXV1UlJSX5+fsbGxqTpdcCAAffu3ZPpJ6alpa1YscLNzc3IyIj8Y+jr67u4uKxYsSI9PV12Hy1r9O9TYGCgvMsCzdYx7+jY2FgydktPTy82NrZlJ9m5cyf5aj179szNzW19qYRCYXR0dEFBQetPRUyZMoX5ka2np9dWn9UsuKmBQWhoKC4PkIDuwdBiHbMeAvIlfT2k0bZWkq0uJCRECV6n1dTU3L9///Llyzk5Oerq6o6Ojn5+fgxzObZebW3t27dvk5KS7t+/n5uby2KxDAwMnJ2d+/fvr9BNGUFBQaRfEN67KyKluaOhDeGmBgbibSNoigfxhlY0l0ELoB4C9UlfD2GKWvFzBeLwW6XocEeDBNzU0CS6PoFaJuB6gFZCPQQkNKse0mg2JpLQnA55yasRUGV09gU0yCgo3NEgATc1NInuJBwREUFfMKCaxK8B+sIAkB7qISChWfUQprZWiZci6D+mysTfheD1mOLCHQ003NQgJbp5jcvlCoVCeRcH5IbOzoWGVmgx1EOA1tx6CFNbK16KAI3+1w8MDETtVnHhjgYabmqQUmhoKLlCRCIRnhsqKyQkhJ6dAiErtBjqIUBrbj1EfePGjcx78Hi8iIiIov/l6+vbRkUFhRESEnLx4kWynJaWJu/iQKvgjgbc1NAs+vr6FhYWpLlVIBDguaGCQkJCwsLCyHJ4eLijo6O8SwQKDPUQaFk9pOmoFT9XKg6/VUoGdzTgpobmcnR0LCoqEggE5LlhYGDAPBc8KJOwsLBNmzaR5eDgYLSPQSuhHgItrIdIOZdOcHAwfUhoaGhbTM8DCkA83UJwcLC8iwNtBne0ysJNDS0mPgINF4+KEP+xwLS90IZQD1FZLa6HSBu14udKBeG3SrnhjlZBuKmhlcSbWPHcUHriTwwejyfv4oCyQT1EBbWmHtKMqBU/VyoFv1WqAHe0SsFNDW1CvKLJ5XLDw8PlXSJoe+Hh4eLJUfCSC2QE9RCV0sp6SPOiVvxcqQL8VqkU3NGqADc1tC3xmgc9D4q8CwVtQygUSkxGglgCZAr1EFXQJvWQZket+LlSYvitUk24o5UYbmqQkfpzn+DRoejqT56JEALaB+ohSqwN6yEtiVrxc6V88Ful4nBHKx/c1NAOJK4x+ukRHBwcHh4uFArlXUBolFAoFAqF8fHxwcHBDWaEDgwMxL8gtBvUQ5RPm9dDWHV1dfUfVVIKCgoieaslLjIul8vj8Xg8Hmau75jIROFCoTAiIkIgEPD5fIkdAgMD6WnlQXXgjlZcuKlBXkQiUUhISP1HByguPC5AXlAPUVztUQ9pZRhdv9kXFBrerao43NHKBzc1tI/6r9VBsXC53NDQUDwuQL5QD1E+bVUPaVVbq7iI/9UmZ4N2xuVyQ0JCyNsseZcFOgTc0YoONzXIhUgk4vP5fD6fLJC379ABkSeDhYWFm5sbWrGgA0I9RNG1eT2kzaJWAj9XCgG/VSAl3NGKAjc1gMoSiUQ8Ho9+PoeGhkrktgFQXKiHKIp2qIe0cdQKAEBzdHRMT0+nKEpPT2/37t2Ojo7m5uZGRka1tbVqamryLh0AgMJDyAoAKgJRKwDIyrNnz2xsbMiyhoaGjo6On59f3759/f39ORxOp06djIyM5F1GAABFhZAVAFQHolYAkCGJfIDq6uo1NTUWFhYcDsff39/KysrR0bF37976+vocDqeuro7FYsm1vAAAioHP5wcFBdEha3x8fIMT2AAAKAdErQAgQxcvXlywYMHLly/rb9LS0mKxWL169WKz2T4+Pvb29i4uLra2tu/fv9fT05NHYQEAFAOfz3d3d6f/RMgKAEpPQ94FAABlZmJiUlJS0uCmqqoqiqLu379PUVRGRkZZWVnfvn1NTU0DAgKsra25XK6dnV1NTQ2bzW73UgMAdFwIWQFABaGtFQBkqLCwMDg4+MiRIzU1NVIeYmBgUF1d7eLiYm5uPnToUDs7ux49elhZWVVXV2tqasq4vAAAHVpERERQUBBZ5nK5fD4fCcMBQBWgrRUAZKhr165WVlbSh6wURb17946iqKtXr5IOxhUVFUOGDOnRo8fEiRNtbGw4HI6lpWVtba26urosCw4A0OGEhYWFhISQZYSsAKBS0NYKADJUWVl5+vTpzz77TCgUtuY8LBbL3NycoqiePXvyeDx3d3dnZ2eyBgBAFSBkBQBVhikTAUCG2Gz24MGDO3fu3Mrz1NXV5efn5+TkvH79+smTJw8ePCDDYgEAVIF4yMrj8RCyAoCqQQ9hAJAtfX390aNHp6enN6ufsDgjIyMbGxtzc3MfHx8bG5tRo0ZVVFTo6+u3dUkBADqikJCQsLAwsszj8eLj4+VdIgCA9oaoFQBky8jIyMzMrAUhK5fLZbPZ06dPNzU1HTNmjLa2tpmZGZnQVUtLSzaFBQDoWBCyAgAgagWA9jBo0KC+ffuSSW6YderUqbi42MfHx9raOjg4uLy83N7ensPhtEsxAQA6FvGQNTAwMDw8XN4lAgCQD0StACBzvXv31tbWZt5HV1fXzs4uICDAwcFh+PDhurq6aFAFAFXm7u7O5/PJcnBwcGhoqLxLBAAgN4haAUDm9PX1fXx80tPTy8rKGtunrKxMQ0Nj7dq1Ghp4LgGAqkPICgAgDjmEAUDmOByOra1tYyGrtbU1WUhKSvLy8mrfogEAdDgIWQEAJCBqBQCZq6urs7Oz69+/f/1NampqpqamGzduJH/y+Xx3d/d2LyAAQIcgEoksLCzokDU0NBQhKwAAolYAaA8sFsvV1dXKyqr+Jjab7ezs/Mknn9A1MwSuAKCaRCIRj8cTiUTkz9DQ0ODgYHkXCgCgQ0DUCgDtoaamxs/Pr3424PLychcXl86dO4v3gkPgCgCqBiErAAADRK0A0B44HI65uXlpaanEend3d09PT7KMwBUAVBOfzxcPWePj4xGyAgCIQ9QKAO2kR48e3t7eEiutra0tLCzoPxG4AoCqIc868ZCVx+PJu1AAAB0LolYAaCe9e/fmcrnia7p3775gwQI1tf/zIELgCgCqQ+Iph5AVAKBBiFoBoJ28f/9+6NChxsbG9BotLS1dXV1NTU2JPRG4AoAqiIiIoJ9vXC5XKBQiZAUAaBCiVgBoJ2w229bWtrKykl4zY8YMJyenBndG4AoAyi0sLCwoKIgsc7lcPp8v0RsFAABoiFoBoP2YmJi4urqyWCyKogwNDY2MjOpnFaYhcAUAZRUWFhYSEkKWEbICADQJUSsAtJ9+/fo5OjqS5T59+ixcuJB5fwSuAKB8QkJC6JCVx+MhZAUAaBKiVgBoP9XV1b6+vt27d2ez2UZGRtXV1U0egsAVAJRJSEhIWFgYWebxePHx8QhZAQCahKgVANqPpqamlZVVVVVVdXX13Llzu3XrJs1RCFwBQDnUD1nlXSIAAMWAqBUA2lWXLl1GjRrl7OxsaWkp/VEIXAFA0QUFBdEha3BwMEJWAADpIWoFgHbVvXt3e3t7a2vr/v37N+tABK4AoLjc3d0jIiLIsvjTDAAApIGoFQDaVU1NjYuLi4uLi/gUOFJC4AoAisjd3Z3P55NlhKwAAC3Aqqurk3cZAEC15ObmlpWV9ejRo2WHi88YgYFhANCRiUSioKAgOmQNDQ0NDg6Wd6EAABQPolYAUDwIXAGg4xOJRDweTyQSkT8RsgIAtBh6CAOA4kFXYQDo4BCyAgC0IbS1AoCiQosrAHRMEiFreHh4YGCgvAsFAKDAELUCgAJD4AoAHY1EB5D4+HgejyfXEgEAKDz0EAYABRYcHEx3ukNXYQCQO4SsAACygKgVABSb+GgxBK4AIEfijyAul4uQFQCgrSBqBQCFh8AVAOQuLCxMPGTl8/kIWQEA2gqiVgBQBhKBa1BQkLxLBAAqRHyMPQlZuVwu+RMJRAAAWk9948aN8i4DAEAb8PX1LSoqEggEFEWlp6cXFRX5+vrKu1AAoPwYQtaKioqioqLCwsLa2lodHR25FhMAQIFpyLsAAABthkziGhYWRv+XntYVAEAWQkJCyNOmfibz3Nzc48eP379/v6CgwMHBwc7Ozs/Pj8PhaGig9gUA0DyY+QYAlI14JTI4OBiBKwDICEPI+vjx40WLFuXm5r58+bKqqoqiKENDw4CAgGnTpvF4PC0tLfmVGgBA8aCHMAAoG/GuwgKBAF2FAUAWGELWtLQ0Pz+/wsJCe3v7wYMH29jYqKurZ2VlJScnv3nzpra21tHRUU0NuUUAAKSFqBUAlBACVwCQqaCgoL1795Ll4ODg8PBwetOTJ0/mzp377t27CRMmbN++feTIkTNnzrS2tu7evbtAIHj48OHr16/z8vI8PT3lV3wAAAWDqBUAlBMCVwCQEXd39+joaLIsMQzh3bt3e/bsSU5O5vF4f/31l76+fqdOnTQ1Ne3s7JycnLp37x4TE/P8+fOcnJzCwsJhw4bJ70sAACgSRK0AoLQQuAJAm3N3d+fz+WRZImStq6vLz88/cuTIvXv3Zs+e7ejoKD5+VU9Pj8fjcTicmJiY/Pz8kpISTU1NZ2dneXwJAAAFg6gVAJQZAlcAaCsikWjMmDF0yBoaGlq/EvXq1avIyMjs7OypU6f27dtXIl0wi8Xy8PBQV1e/cuXKy5cvORxOly5dbGxs2vFLAAAoJEStAKDkELgCQOuJRCIej5eenk7+DA0NDQ4OltiHxWJVV1cfOXJEKBR27tx54sSJDZ5q2LBhNTU1165du3fvHpfLdXBw0NPTk/03AABQYIhaAUD5IXAFgNYgIatIJCJ/Nhiy0t68eRMXF6ehodG9e/devXo1uI+3t/fbt28TEhISExM9PDx69uyJlMIAAAwQtQKASkDgCgAtw+fzx4wZQ4es4eHhixYtamxnLS2tgoKC2NjYtLQ0U1NTa2vrrl271t+trq6Oy+U+fPjw5cuXenp6rq6uHA5Hll8CAECxIWoFAFWBwBUAmovP57u7uxcVFZE/4+Pjm3xu2NjY5OTkCAQCPp9vampqamrapUsXiX1YLJampmZGRkZ6erqhoeHEiRN1dHRYLJbMvgcAgGJD1AoASis9Pb22tlZ8wBgCVwCQHglZ6T/j4+N5PF6TR7FYLCsrq1evXmVkZMTGxlpYWJiamhoaGkrspqWlVVRUFBUVpa+v7+Xl1a1bNxl8AwAAJYFBFACgnIqKiq5fv+7t7Z2Wlia+XnxAWlhYWEhIiJwKCAAdWkREBB2ycrlcKUNWiqLU1dWtra0XLlzo5eVFUdS6devOnDnz9OlTid1KS0uLiop0dXXRygoA0CS0tQKAcnr48OEnn3ySmZn57t27sWPHampq0pvQ4goAzMLCwhYvXkyWuVwun893dHSU/nBNTc2uXbuqqakVFBQIhcKrV69aWVkZGBgYGRnR+zx9+jQ6OvrZs2cjRowYPXo0YlcAAAaIWgFACb179+7kyZOXLl0yMjKaMWNGv3792Gy2+A4IXAGgMeK9MEjIyuVym3sSHR0dS0tLDofz5s2brKys69evv3//vry83Nzc/O3btw8fPoyNjd2/f7+lpaW/v3+/fv0kZnYFAABxiFoBQNnU1dUVFxdv27YtIyODy+WuXbvW3Ny8/m4IXAGgPvGQlcfjRUdHtyBkJTgcjqWlZZ8+fXJzcx89epSampqQkJCWlpaQkMDn8//++28TExN/f/+ZM2fq6uq26ZcAAFA2iFoBQNmwWKzt27dHRERoampu27Zt6NCh6urqDe6JwBUAxIWEhGzatIks83i8+Ph4fX195kNqa2sZevbq6uoaGxuPGjXq1atXb968EQqF9+/fT0tLy8vLs7e3nzRp0vLlyzHnDQBAk9AdBQCUzaNHj+7fv19eXu7r62tvby8+orW+0NBQ0rpC/5esAQBVExISQh4CdMja5CH5+fklJSU6Ojrdu3dvbJ9OnTrp6Oj8888/hw8ffvDgwYMHDzQ1NZ2cnPr27evr66ulpdWmXwIAQDkhagUApVJTU3PlypXTp09raWmNHj3a2dm5yUMQuAKAeMgaGBgYHh7e5CF5eXkpKSnr16//8MMPAwMD60/KSiNjVmfPnl1SUlJQUFBXV2dkZKSnp6emhqkcAACkgqgVAJTKvXv3/vvvv7q6ulGjRknf3ReBK4Aqc3d35/P5ZDk4OFia2z83NzcpKWn9+vUlJSVJSUmzZ89u8hAWi9WpU6dOnTq1RZEBAFQLXvIBgPIoKyt7+PBhamqqgYGBs7OzjY1NY+PNKisra2pqxNdgHlcA1dSCkDUnJyc+Pn716tWlpaW+vr7fffcdxqYCAMgUolYAUB6FhYV//vlnfn5+7969ly1b1uCAsdra2szMzOvXr69Zs6awsFB8EwJXAFXTgpD15cuXN27cWLNmzfv378eNG/fdd9+ZmJiQTfn5+UVFRTIuMgCAKkIPYQBQEhUVFVeuXBGJRMbGxrNmzZIIWevq6lgs1pMnT1JSUg4dOpSZmfn06dP79++fPn1aW1ub3g1dhQFUhEgk4vF4IpGI/Cn+0or5qOvXr69fv15DQ2PcuHGbN282MDAgTxiBQBAeHu7i4jJ27FhDQ0PZfwMAABWCqBUAlERFRcWFCxeysrLs7e15PF7nzp3pTaWlpRUVFeHh4SkpKXv37mWz2SYmJo6OjjNmzMjJybGxsRE/T2hoqEAgIM0vCFwBlFLLQlahUBgXF7d+/XpdXd0JEyZs3ryZzLNaW1srEAgOHDjwzz//CIXCoUOHImoFAGhbiFoBQEmcPHkyLi6upqbmo48+cnR0JCsrKipEIlF8fPzx48cTExPz8/P19PTGjh3r7e09bty4Ll26NDgZY3x8PN1vEIErgJJpWcianZ19+fLldevWde7ceeLEiZs3b2az2RRFvX//XiAQ7N+/Pzw83MvLa86cORYWFrL/EgAAqgVRKwAoA5FIdPfu3ZycnPHjxw8YMEBLS6u2tvbu3bsZGRm//fZbXl6eSCTS1NScO3fuwIEDp0+fzuFwSCNJYxC4AiglPp8fFBREh6zx8fE8Hq/Jo4qKipKSktasWWNkZDRlypTNmzerq6tTFFVVVSUQCPbu3Xvq1CkvL69ly5b5+fnJ/ksAAKgcRK0AoAxu3769Z88ebW1tDw+Pvn37ZmdnHz9+/MaNGxcvXqyqqurbt++ECRMWLlzYp08fGxsbMsa1yXMicAVQMnw+393dnf5TypCVoih9fX2hUOjh4eHk5LRp0yaysrKyUiAQ/Pnnn+fPnx86dOiKFSvGjh0rs7IDAKg0Vl1dnbzLAADQKllZWZ999ll0dLSzs/O2bdtu3rwZHx8fHR1dU1Pj7Ozs7Ow8a9asHj16mJqakuaRZhFPMSplT0IA6IBaHLLSrl+/PnToULJcXl4uEAh279598eJFT0/Pjz/+eNSoUW1dZAAA+B+IWgFAsVVXV6ekpCxZsuThw4fOzs4FBQUVFRWVlZW6urpLly4dPHjw8OHDWSxWg7PgSAmBK4Cii4iICAoKIstcLpfP53O53BafrbS0NCEh4Y8//oiLi/P09Pzkk0+GDx/edoUFAABJ6CEMAIpNU1MzNze3a9euNTU1ycnJXbp06dOnz4QJEzw8PPr379+pU6fWf4R4V2EyiSsCVwAFIj79cutD1qqqqtTU1B07dsTHx3t5eX366adeXl5tV1gAAGgAolYAUHgTJ07Mzs5WU1MzNjZ2cHBYvny5hoaG+MwTBQUFhYWFdnZ2Lf4IBK4ACqq5IWt1dTWLxdLQaLSCpKGhkZGR8erVq6FDh4aEhHh4eMig1AAA8H+ghzAAKIPa2tqUlBQDA4NevXpJZFqqrKy8du3a1q1bAwMDly1b1tgZqqqqmuxFjK7CAIpFPGTl8Xjh4eHMIWtRUZFIJMrNzXV1ddXT02tst5KSkoiICGdn5wEDBsig1AAAIAltrQCgDNTU1FxcXBrcxGaztbW11dXVP/vsMzU1tQ8++KD+PnFxcbq6unZ2dgYGBgyfghZXAAUSEhJCsn+TkDU+Pp55//fv3z969GjDhg1aWlrffvuto6NjY8nG9fT05syZw9AeCwAAbQsPXABQfmRSirq6uuDgYDU1tSVLlohvTU5O/uKLL3R1dX/++WcdHR3mFlcErgAKobkhK+n6W1RUFBcXx2Kxhg0b1rdvX+ad266wAADQBPWNGzfKuwwAADLXp08fPT293NzcP//808zMzNnZmawvKyu7efPm0aNHS0pKHBwcnJycmpzKddGiRRcvXhSJRBRFRUdHGxgYNHf+DACQKfGQNTAw8MKFC1IeqK6u/u7du5SUFDabbW9v3717d1kWEwAApKUm7wIAALSTKVOmfPjhh+7u7t9//71AICAri4uLd+3aVVBQYGFhMWbMGDU1qZ6K4jM9itePAUDu3N3d6VsyODg4PDxc+mMtLS0HDhxoZmZ248aN58+fV1VVyayYAADQDIhaAUCFTJ06ddWqVStWrCDjV8vLyyMiIp4+fWpmZrZs2TJdXV3pT4XAFaADEk+ZFhwcHBoa2twzzJ07t1+/fsXFxfv27Xv79q0MyggAAM2GqBUAVMu4cePmz59vb29P8oXeuHEjNzfX1tbW0dFRR0enWadC4ArQcYhEouaGrBUVFbW1tfXXz5w509TU9Pnz56mpqdXV1bIpLwAANAOiVgBQOfr6+mTh5MmTsbGxLBZr0aJFDg4O9fesqalhPhUCV4COQCQS8Xg88YmpmgxZ8/Ly7ty5c/jw4ZKSkvLycnq9rq5uv379unfvfv/+/XPnzqGTMABAR4CoFQBUVGZmZmJiYkFBgb+//4ABA9TV1cW3vnz58vr163fv3i0tLWU+DwJXAPkiIStJkCblXMrl5eW3bt1aunTpxo0bg4KCzp079/jxY/otVZ8+fUim8evXryckJMj+GwAAQBOQQxgAVFFdXV18fPymTZs0NTWnTZs2efJkkjq4srKyurr6yJEjx44dW7VqlUgkcnV17dy5M3OWJmQVBpAXiZA1PDx80aJFTR6lqal5586du3fvZmdnZ2RkpKSkxMfHm5iY1NTUdOnSRV1dvba2ViQSJSUl9evXz87OrrnDBwAAoG1htjEAUEXPnj3bt29fXV2dt7f33LlzWSzW+/fvRSLR7du3w8PDExISnj9/rqWl9f79+9zc3F69ejV5QszjCtD++Hy+u7s7/ad4x4cmTZ061czM7NGjR2FhYQUFBVeuXElKSvLz8/P09JwwYcKAAQMGDhwYFxe3Z8+eMWPGGBoayuxLAABA0xC1AoDKqaqqEgqFDx8+7Nq168iRIw0MDB48ePDkyZNff/01Ozs7KytLQ0NjzJgxnp6efn5+NjY2Ep2HG4PAFaA9NRmyZmVlVVdX29nZNXYGd3f3AQMGuLm5nT9//uLFiykpKceOHTtx4gSfz/f09Fy4cGFUVFROTs7ly5ctLCyalWMcAADaFquurk7eZQAAaFfl5eWLFi06pd2miQAAIABJREFUceJEz549Dxw4kJKScuPGjdOnT1dUVNja2pqZmS1evLh3796DBw+ura2VcgZXmngWU2nG1wFAC4iHrFwuNzw8XCJkjYyM/PDDD3fu3Dly5Mgm+/e+e/euoqLir7/+un379vnz52tqaqysrExNTblc7okTJwIDA3/66adu3brJ8gsBAAATRK0AoFrq6uouXbq0YcOG5OTk8ePH19bWXr9+vaSkpE+fPs7OztOnT3dwcDAzM2Oz2S3+CASuADIVFhZGujOQkJXP53O5XPEdiouLJ02adP369VGjRh05coTMzyyN9PT0uLi406dPJycnFxUVkX4Wrq6u33//PQarAwDIEXoIA4Bqef/+fXFxcXFxsbq6+qVLl9hstpaW1po1a1xcXEaNGqWurt76tCvoKgwgO02GrBRFsVisuXPnZmRkPH/+PDY21t/fn6Gf/7Vr1xwdHbt27UpRlIODg729vZubW3p6+u+///769WstLS0vLy9bW1sZfy0AAGCCHMIAoFrU1dU7d+789u3biooKS0vLmTNnhoSE+Pv7Dx48WEtLS1NTU5qTPHr0SENDQ1tbu7EdkFUYQBakCVkpitLS0qqurr5x40ZqaqqxsbGnp2djd+umTZv27NnTpUuXPn36kMiWxWKZmpr27Nlz1KhR9vb2AwcOnDNnDroHAwDIF3oIA4AqevXqVUJCgrOzs7a2tvH/a+/eo6K87v2P7+EucgkXibGDGFBDNUoUMA5e4iURRWNNKhe7qidGjTFNV35DkpplEhPtSdpoAj3LHC2JGM9pukRIrE0igVgvRwiDd0UFb6AIRJdcRi6CgDi/P3b7nDkDIigwD8z79YdrzzP7eZ49Oi78uL/P3gMGdOrczZs3Hzp06De/+c2IESPaT7mUCgNdyHw/ZJ1Ol5OT007npqamDRs2vPnmmwMHDty0adMvfvGL1n3eeeedTZs26XS61atXjxs3rnWHhoYGe3t7JyenrvsQAID70blVRgCgb3j44Yfnzp3r7+/f2cja0tJSVlZ29uzZs2fPNjc3t9/ZfFFT839wA+isTkVWOd06efLkyMjImpqavLy8iooKiw6/+93vkpKSJkyY8MYbb7QZWYUQ/fr1I7ICgBqQWgGgE5qamkaNGnXt2jW5WMs9y1UIrsCD62xklcaOHTty5EghxPbt26urq83/tur1+q1bt0ZERLz55ptTpkzptoEDALoGqRUAOqFfv35DhgwZNGjQ5cuXS0pKOvKQBcEVeBAxMTHK3xq9Xt/ByCqfUF2+fHlgYGBpaenWrVsbGxvl8T179hw4cGDChAlvvfXWpEmTum3gAIAuw2pMANA5JpOpsLBw586dEyZMGDJkSEf2yGFxJuD+REREZGZmyrZer09ISLDocPXqVXt7+zafMNdoNM3NzXV1dYcPH3ZxcRk7duyAAQM0Gs2dO3eCg4PnzZsXHh7eIx8CAPCgSK0A0Dmurq6nT58uKyvr169faGho//79NRrNPc+KjIxMS0urqakhuAIdZL6eWZuRde3atcnJydevXx8yZEib2dXNza25uTk9Pb2goGDo0KGhoaF2dnbe3t6PPvpom4sPAwDUidQKAJ1jMpns7e2zs7PLy8snTJjg4+PTzlaQCg8Pj5iYGIIr0BGlpaUzZ840X4K79T9X0tPTX3rppXPnzuXn5+/du9fPz6+5udnHx8fO7v88/eTj43Pjxo0ff/zR2dl51KhRfn5+QggHB/arB4DehNQKAG1raWmprKyUW7zKakN53M7OrqWlJSsrq6qqSqvVjhw5soP/Aia4Ah1RWlqq0+ny8/Ply7vtGlVTUzN8+PCioqLa2tqzZ88aDIajR486Ojra29sPGDDAZDLJv7MuLi4NDQ0FBQVnz56dMmVKQEBAR/6bCQCgKqRWAGhDU1PT+vXrT506VVRUVF1d7ejoePv2bScnJzs7O5PJ5OTkVFdX9/e//33w4MEjRozw8PDo4GUJrkD7ZGSVD4G3v9HxoEGDxowZM27cuFGjRhUXF1dVVZ0/f37nzp0VFRVlZWXBwcEmk0nWDAcEBGRnZx8+fNhoNM6ZM8fFxaVnPxMA4EGRWgGgDQaD4fjx47t27crIyLh06dKxY8caGhpqampu3brl4uLi6OhYUVFx6tSp8vLy8PDwhx9+2KIosR2tg2tkZKS/v383fyCgF7CIrKmpqUuWLGmnv6Oj4+DBg4OCgqKiouzs7FxdXUtKSk6cOJGdnX3u3LmbN28GBATIUgitVrt///76+vqgoKChQ4d2/C8sAEANSK0A0IbBgwd7eHgEBwd7e3tfvXr19OnTJ06c2LNnT2FhYXFxcVNTk5OTU05OzrVr18LDwwcPHuzk5NTxi1sE1+TkZIIrYDAYHn/8cfmXQm4ZFRkZ2ZET+/Xr5+vr++STT06ZMsXV1dXFxeXcuXMFBQX5+fn79+8fOHCgEMLd3f3ChQsGg2HgwIGTJk1qc81hAIBqaTqy2SAA2KampqZr167V1dVlZ2efPXv2+PHjRUVFrq6ucgWmK1euVFVVvfzyyytXrvTy8urISsLmLKaVzLd1BWyNwWCIiIhQXt7fX4c7d+7Y2dn9+OOPBw8e/OKLL8rLy+XD56GhobGxsYWFhatXrx4yZMh//Md/zJw5s6s/AQCgG5FaAeAe7ty509jY2NjYePz48UuXLu3fv7+srOzq1avFxcVCiN/+9re/+c1v7m+mlOAKWERWrVabmpr6gH8Rbt26dfz48ePHjycnJ5eUlNy8efPOnTtPP/30sWPH6uvr33nnncWLF3t7e3fR8AEA3Y7UCgCdUF9fX15eXlFRsX///kuXLrW0tEyfPn3+/PkdObe5udnOzs5i/VKCK2xcYmJifHy8bGu1WoPB0FU7qd64cePGjRt//etfDx48+I9//KOhoUEuqPbiiy+uWbPG19e3S+4CAOgBpFYA6LTbt2/b2dmVl5c3NDQMGTKknZ5y+43S0tIrV67Ip2F9fX2HDx9u3ofgCpvVfZFVUVtbW1NTk5ycnJOTYzAYpk2b9m//9m/z5s3r2rsAALoVqRUAusutW7eam5v/8z//U64K079/fxcXlxEjRsyfP/+5554z70lwhQ3qgcgqyeddDx48+NNPPzk5Oc2ePbs77gIA6D6kVgDoFpWVlRcvXvz973//448/3rx509nZOTAwUM781NbW/vGPf7TY0oPgCpsSHx+fmJgo2zqdLicnpwdu2tjY6Ozs3AM3AgB0LVIrAHS94uLi7OzsjRs35uTkuLu7R0VFTZ48edKkSRUVFUePHk1OTi4sLExOTl64cKH5WQRX2AirRFYAQO9FagWALnb58uWvvvpq69atZ86c8fb2Xrt2rU6nGzt2rMlkMplMdnZ2n3/++fr16zUazWefffbUU0+Zn0twRZ9HZAUAdJadtQcAAH3K1atX09PTZWQdMGDAxx9/PHfu3LFjxwohNBqNnZ2dEGLevHk6na62tjY3N7eiosL8dIun+yIiIgwGg5U+CtD1IiIilMiq1+uJrACAjiC1AkCXqampKSgoSE5OPnPmzMMPP7x+/fqnn3669Vauzs7Orq6uN27cOHHixO3bty3eJbiirzL/Muv1+oSEBGuPCADQO5BaAaBrtLS0VFdXv/fee8eOHRs4cOD69eunT5/eOrLKbSTPnDlz+/ZtR0dHNze31h0Iruh7iKwAgPtGagWArmEymd566y2DweDn5/fv//7v06ZNa3Mbj4aGhsOHD1dWVrq6uj722GOt51olgiv6jNLSUn9/f+ULnJCQQGQFAHQKqRUAuoDJZPr+++9PnTrl4uLy/PPPT5gw4Wc/+1mb3erq6rZt25afn29nZzdx4kRPT8+7XZPgij7AYoGxhIQEvV5v7UEBAHoZUisAdIFbt25duHDh3LlzXl5e06dPDw4ObrObRqNZuXLl119/bW9vv2rVqtGjR2s0mnYuS3BFr0ZkBQB0CVIrAHSBurq6n376SaPRhIaGjhkz5m7dlixZ8sUXX9jb2y9dunTy5MleXl73vDLBFb2UwWCw2MaJyAoAuD+kVgDoAi4uLg4ODn5+fi0tLc7Oznfu3Gnd54UXXtiyZYu9vf2sWbPmzp07bty4Dl6c4Ipex2AwREREsPMwAKBLkFoBoAs4OjqGh4f7+Pg0NzcfPXrUzs7OZDLJt5qamhobGxcuXPhf//VfDg4OoaGhzz//fFRUVKeuT3BFLyIjq/KSyAoAeECkVgDoAi4uLsOGDdPpdIcOHdqxY0dGRkZ5eXlVVVVhYeG+fftiY2O//PJLZ2fnqVOnvvLKK4sXL76PWxBc0SukpaUpkVWr1ZaUlBBZAQAPSKPMBgAAHtCePXv+/Oc///DDD0899dSQIUP8/PxycnKKi4vz8/P79++/bNmyqKioZ5555kFuYbG8DbNY6CYnTpx44oknOntWYmJifHy8bFv8PwsAAPeN1AoAXWn37t2pqakHDx5samoqKSm5c+eOl5eXm5vbW2+9NXbs2PuIAa0RXNEDPvzwQx8fn+XLl3f8FCIrAKCbkFoBoIsdP3787NmzOTk5dnZ2zs7OQUFBOp1uyJAhHh4eXXULgiu6VWFh4eTJk994442Or/prHll1Ol1qaiqRFQDQVUitAND16uvrb926ZWdn5+DgYGdn5+rq2uW3ILii++Tl5c2fP99kMn399dejR4++Z//4+PjExETZ1ul0OTk53T9GAIANYTUmAOh6rq6u3t7eDz30kJubW3dEVqUCU3nJ4kzoKiaTaf/+/UajsaGhobm5uaWlpf3+RFYAQHcjtQJAb6XVas0TAsEVXaKxsfHKlSsVFRVlZWWfffaZnV17/1Qwj6zR0dFEVgBAdyC1AkAvZjG1RXDFg6uqqiopKZHtK1euVFZW3q1nRESEEln1en1qampPjREAYFtIrQDQuxFc0bWMRmNWVpZs7969e8+ePW12M/+m6fX6hISEHhwjAMC2kFoBoNdrHVyVVZqATmlpaSkrK6upqZEvHR0djx07VlFRYdGNyAoA6EmkVgDoCyyCq/nywkDH2dvb79q16+bNm/LlrVu3vvvuu/r6eqVDaWmpv7+/ElkTEhKIrACA7kZqBYA+wjy4WuyLA3RQfX39uXPnzI/U1dXl5uY2Nze3/l4lJCR0fENXAADuG6kVAPoOgise0JkzZw4ePKjRaJQjV65cycrKcnR0JLICAKyF1AoAfQrBFQ+ioqLC0dHRZDKZHzx06FBSUpL5dyknJ4fICgDoMRqLn0wAgD7AYDBERETItlarNRgMWq3W2oOC2jU2Nr799ttJSUl1dXXmx+3s7O7cuaO8zMnJ0el01hggAMBGMdcKAH0QM664D83NzWVlZRaRVQhBZAUAWBepFQD6JoIrOuvo0aPHjx+/27uurq47duwIDAwUQlCoBQDoSVQIA0BfRqkwOm7Xrl3PPfecXC64NXd39+bm5hkzZuh0uqeffvrnP/+5o6Ojk5NTjw8TAGBzSK0A0McRXNERN27cWLt27aeffnq31CrJZ1yDg4MHDx4cFxf36KOPjh071sPDw2Qyma88DABAFyK1AkDf1yXBtbS01GAwGAyG3NzckpISeaQbBosuoNVqdTqd/FU27nnKnTt35syZ8/3333f8Lp6eni0tLdHR0UOHDn3xxRcdHBw8PT0dHR0fbOwAAFgitQKATbjv4FpaWpqWlpaQkEBG7b2i/6WdPnl5eQsXLszLy7uP62s0mjFjxgwYMODVV1/t37//uHHj+vfv/wDjBQDg/yC1AoCt6GxwLS0tjY+PT0tL66kBottFR0cnJCS0+ee+ffv2uLi4+76yq6urg4ODh4fHnDlzXnjhhSeffPLBRgoAwP8itQKADWknuJo/l3i3vKrT6caPHx8dHe3v7y+v0LPDR0cp5dxyqtzi3ejo6NTUVPMjLS0tW7Zsee211xoaGjp+F1dX1zt37jz22GMjRozw9PScNm2ar6/vmDFjPD09ecYVANCFSK0AYFvuOeOalpYWHx9vXg/ckfpSqFnav5gfTE1NVf5MKyoqJk+efO7cOfOtWVtzdnZ2cXGprq6eNWuWr69vSEhISEjIQw89FBYW1tTUxHrCAIBuQmoFAJvTTnCNj49PTExUerZTUIpep3V21ev1CQkJQgij0Thr1qyDBw+2PsvR0dHe3n7QoEEhISGenp5RUVHe3t6jRo3y8/Orr693dXXt2Q8BALBFpFYAsEVtBteYmBgl0mi12oSEBOZX+x6LuXRZLfzpp5+uXr3aaDQKIRwcHPr161dbW/vEE08MGTIkICBgxowZzs7O4eHhTk5OTk5OdnZ21v4QAADbQmoFABtlEVwff/zxjIwM+VKZgkNfZT6prtPpfvGLX6xZs8bX1zc4ONjDw2PatGnDhg0LCgp69NFHa2trPTw8rD1eAIBNI7UCgO0yD66enp7V1dVEVtthHlx9fX2Tk5Pd3NyGDh3q5+dnb2/PtqsAAPWgyAcAbJdOp8vJyZFtGVkTEhKIrDbC/M+6oqJi//7906ZNGzx4sIuLC5EVAKAqpFYAsGnmawXr9Xq9Xm/V4aBHmf+JJyYmsjcvAECdqBAGAJum7KtJYbDNUkqF29wJCQAAqyO1AoDtUhYN1mq1JSUl1h4OrMbf31/Ousslha09HAAA/g8qhAHARpWWlioVocyy2jjlC5CWlmZeNA4AgBqQWgHARsXHx8tGdHQ0+7LaOPPvgPLFAABAJagQBgAbpTzRmpqaSmpFaWmpv7+/bJeUlPB0KwBAPZhrBQBbpNQGM9EKSavVKt8EFhMGAKgKqRUAbJF5arX2WKAWypeB55wBAKpChTAA2BzzWlB+CsCcUjdOkTAAQD2YawUAm2MwGGSDiVZY0Ol0sqF8SQAAsDpSKwDYHCWQMJkGC+PHj5cNUisAQD1IrQBgc5QNOZWJNUBSpt9zc3OtPRYAAP6J1AoANkeZRiO1woL55jfWHgsAAP9EagUAm6PMtVIhDAAA1I81hAHA5ijrxPIjAK3x9QAAqA1zrQAAAAAA9SK1AgAAAADUi9QKAAAAAFAvUisAAAAAQL1IrQAAAAAA9SK1AgBUZ8GCBe7u7suWLbP2QAAAgPWRWgEAqlNcXHzz5s3i4mJrDwQAAFifg7UHAACApbCwsKqqqtDQUGsPBAAAWJ+GPcQBwNZoNBrZ4EcAWuPrAQBQGyqEAQAAAADqRWoFAKCj0tPTw8PDNRqNRqMJDw8/efJkO51Pnjwpe7bfDQAAtI/UCgCwJm9vb41GExcX1363devWaTQab2/vnhpXG9LT02fPnn3kyBH58siRI5mZme30r62ttWgAAID7QGoFAFjTjBkzhBDbt2+vrKxsp9tnn32mdLaW9957T64UVVhYaDKZTpw4ERkZacXxAABgI0itAABrmjdvnmzs3r37bn1OnjxZWFgohFi0aFEPDs2SnGVdunRpYGCgECIkJCQkJMSK4wEAwEaQWgEA1hQXF+fl5SWE2Llz5936pKamCiG8vLyioqJ6dnT/S5kKHjlypLXGAACAbSK1AgCsTD7U2k6R8Pbt25Vu1lJQUGDFuwMAYMtIrQAAK5szZ45stFkkrJQHK916WFJSkkajmTRpknw5adIkuTJwp1J0ZWXlK6+8Ipee8vb2fuWVV4qKirptyAAA9CmkVgCAlUVFRQUFBQkhtm7d2vpdWR4cFBR0z/Jgzb1YawniM2fODBs2bNOmTUajUQhhNBo3bdoUFhbGjjgAAHQEqRUAYH2xsbFCiMzMzNYzkLI8WHawiuXLl5tMpqysLPkyKyvLZDKZTKaUlJQOXuHll18WQmzbtq2iosJkMm3bts3Ly8toNP7yl79sf+VkAABAagUAqEJMTIxsWBQJK+XBSod2mO6lqqqq2z5Be7y8vPbt2xcXF+fj4yMf0P3DH/4ghCgsLGxn5WQAACCRWgEA1hcSEiKLhDdv3mx+XCkP7tV7zHz55ZcW41++fLlsHDhwwEqDAgCg1yC1AgBU4aWXXpJ7opoXCcvyYPlW7+Xh4dH6YGRkpBCCNZkAALgnUisAQBXmz58vG0rRrFIerLzVreLi4lov4NT+w6tyeWELr7zySg+MFgAA20FqBQCoQmBgYFhYmHmRsCwPDgsLCwwM7MgVVLuGMAAAeBCkVgCAWixdutS8SFiWB8uDPSAlJaX1Ak7tb8oqlxe2sHHjxp4ZMAAANoLUCgBQC/MiYaU8+Jlnnung6apdQ7impsbiSGVlZWZmphAiNDTUKkMCAKAXIbUCANTCx8dH7su6fv16WR4cGxvbwfJgNfv1r3998uRJ8yPJycmyMWvWLCsNCgCAXoPUCgBQkXnz5smNTDdt2qS87O2MRuPUqVPlwk6VlZVJSUkrV66UywhPnDjR2qMDAEDtSK0AABVR6oGNRmOnyoPVbNu2bUajccGCBRqNxtfX9+WXXxZCeHl58QQsAAAdQWoFAKiIj4/PqlWrZHvVqlU+Pj7WHtE/DRo0SDbc3d07eIrsGRQUFBcXd+LECVn8LI+sWrXqwoULfaD4GQCAHqAxmUzWHgMAoEdpNBrZ4EcAWuPrAQBQG+ZaAQAAAADqRWoFAAAAAKgXqRUAAAAAoF6kVgAAAACAepFaAQAAAADqRWoFAAAAAKgXqRUAAAAAoF6kVgAAAACAepFaAQAAAADqRWoFAAAAAKgXqRUAAAAAoF6kVgAAAACAepFaAQAAAADqRWoFAAAAAKgXqRUAAAAAoF6kVgAAAACAepFaAQAAAADqRWoFAPSokydPajQajUaTlJTUfs+ZM2dqNJq4uLieGlpPqKysXLduXXh4uPxN8Pb2jouLy87Otva4AABQL43JZLL2GAAAPUqj0ciGtX4EeHt7G43GsLCww4cP361PUVFRUFCQEOLPf/7z8uXLe3aA3aWoqCg2NvbIkSOt31q1atUHH3xgjUFZsvrXAwAAC8y1AgB6mpw+PXLkSFFR0d367N69Wzbmz5/fg0PrXjKyenl5bdu2zWQymUymEydOhIWFCSE+/PDD9PR0aw8QAAA1IrUCAHqaMneqRNPWNm/eLGOej49PDw6tG6WkpMhZ1m+++UYpew4JCcnIyPDy8hJCvPfee9YeIwAAakRqBQD0tJCQEFn9K6Npa0VFRTLgzZs3r/uGsW7dupkzZ/bYM6WffPKJECIyMnLixInmx318fFasWHHPyWcAAGwWqRUAYAWxsbHt5DRlDvaZZ55p5yLe3t4ajebtt99u591169bd7XRPT8/MzMxJkyb1QHatrKyUOXzatGmt3501a5ZsHDp0qFuHAQBAb0RqBQBYwZIlS2Tjq6++av2unINdsWJF++XBM2bMEEJs2rSp9Vvp6elGo1EI8fjjj9/t9OXLl2dlZUVGRnYku65bt05zL+2silxQUCAbERERrd/9+c9/LhtXrlxp5/MCAGCbSK0AACsIDAyUqxB99tlnFm8p5cFz5sxp/yKLFi0SQhiNxtbrGH333XdCiKCgoKioqHauMHHixIyMjKysrKCgoG6dd62pqWnnXSWcV1dXd/mtAQDo7UitAADrWLp0qRCisLDw5MmT5sdlebCXl1f7gVMIERUVJdcxkhnVXEpKilKHfE8TJ068ePHitm3b2smuv/vd70z30s4OPadPn+7ISI4ePdqRbgAA2BRSKwDAOpRnVlNTU82Py/JgZZXd9sluMqMqlPLgmJiYjo8nLi7untkVAAD0PFIrAMA6AgMDIyMjhRDbt29XDirlwb/61a86chHZzaJIWE69hoWFhYSEdHZUMrt+9NFHXl5emZmZc+fO7ewVAABA1yK1AgCs5oUXXrAoEpblwUFBQcr2MCdPnmy97tHQoUPluxMnTpSb6Pz3f/+3clk59SorkO9DZWVldXW1nK3tKoMHD+5ItzZXGAYAwMaRWgEAVtO6SFiWB3fweVRJdt6+fXtlZaV5eXD7u+a0qbKyct26dcOGDfvwww/l3qr79u2Tbz3gGsJarbazgwEAABKpFQBgNT4+PkrmNC8PNn8eNSQkpPW6RxcvXlQ6KJvoyHlaWR4cGxsbGBjYqcGkpKQMGzZs5cqVRqMxMjIyKysrIyPjPmqM2zRo0CDZyMnJaf2u8vRsm/viAABg40itAABrkrvXyCJhpTy4U1lR2URn586dSnnwvHnzOn6FlJSUoUOHLliwwDyvKiXK0gOuIRwYGCiXO967d2/rd7///nvZUDZuBQAAClIrAMCalN1rkpKSZHnwm2++2dmLyEdYt2/fnpKS0qny4Ozs7PDw8AULFhQWFt4tr3YVudxxZmamxU4/lZWVmzZtEkKsWLFC2bgVAAAoSK0AACtTdq+R5cH38Tyqcso777zT8fiXlJQ0adKkI0eOdHdeld544w2Zz6dOnaqseJyenj5z5kyj0ejl5fXGG290390BAOi9SK0AACubM2eO3L1GblfT2edRZf2tfD62sLBQueA9VVdX90xeVQa5ceNG+Ulnz54tF3CaPXv2kSNHvLy89u3bdx8fHAAAW6AxmUzWHgMAoEdpNBrZUM+PgPDwcDnRumvXrqioqPu4Qnp6+uzZs2XuPXz4cDeMsWsUFRV9/PHHP/zwgwzYQUFBsbGxS5YsUU9kVeHXAwBg40itAGBziCVoB18PAIDaUCEMAAAAAFAvUisAAAAAQL1IrQAAAAAA9SK1AgAAAADUi9QKAAAAAFAvUisAAAAAQL1IrQAAAAAA9SK1AgAAAADUi9QKAAAAAFAvUisAAAAAQL1IrQAAAAAA9SK1AgAAAADUi9QKAAAAAFAvUisA2BytVisbpaWl1h4LAADAPZBaAQDAPyn/kaH81wYAAFZHagUAm+Pv7y8bJSUl1h4L1MVgMMiGTqez9lgAAPgnUisA2Jzx48fLRlpamrXHAnVRUitzrQAA9SC1AoDNUabRcnNzrT0WqItSIcxcKwBAPTQmk8naYwAA9KjS0lKlSJhaJgdLAAAMlUlEQVSfAjCn0Whko6SkhOlWAIBKMNcKADZHq9UqgYQiYSiUL0N0dDSRFQCgHqRWALBF8fHxskFqhcI8tVp7LAAA/C8qhAHAFpkXCVMLChlZY2JiZJt/GwAAVIW5VgCwRVqtVplPU+ZdYcuYaAUAqBZzrQBgo8ynW1NTU8kqtsx8opW5dwCA2jDXCgA2iulWKJQvAOswAQBUiNQKALYrISFBRpTS0lKCq82Kj49XtmlNTU219nAAALBEagUA26XVahMSEmQ7MTGR4GqD4uPjExMTZZvICgBQJ/v333/f2mMAAFjNyJEja2pqcnNzhRC5ubmenp46nc7ag0IPSUxMXLNmjWzr9Xr+2wIAoE6sxgQAEDExMcoSsnq9XpmARR9mPssaHR3NRCsAQLVIrQAAIYSIiIgwGAyyTXDt88wjq06ny8nJsfaIAAC4K55rBQAIIUROTo6ypHBiYqK/v78y+4q+JC0tzd/f33yWlcgKAFA5UisA4J9SU1P1er1sl5aWxsTEmFcOo7dT/kyVFYP1ej2FwQAA9aNCGADwf6SlpcXExJgfif4X6w0KDyTtX5Qjcvlo/kwBAL0CqRUA0IY2Z1mjo6O1Wq1Op9PpdHKjV6iQnEotKSlJS0vLzc1VHldWREdHK1v1AgCgfqRWAEDbSktL4+PjqRDuS8irAIDeiNQKALiH1vWl6F20Wm18fLycKrf2WAAA6DRSKwCgQ0pLSw0Gg8FgkA1lRR+ojYym/v7+48ePp5wbANAHkFoBAAAAAOrFzjcAAAAAAPUitQIAAAAA1IvUCgAAAABQL1IrAAAAAEC9SK0AAGtqamoqKCg43crly5erqqraPMXT01Oj0WzcuLG7xxYdHa3RaKKjo7v7RkKIjRs3ajQaT0/PHrgXAAC9i4O1BwAAsGmXLl0aP358TU2NxfGIiIhp06YtWrQoMDDQ3t7e/C3Zua6urrvHVltbq/za3eTHaf37AAAASK0AAGsqLy+XUW348OFubm7yYENDQ0FBQU5Ozo4dO1JSUkaNGmXtYQIAAKuhQhgAoArJyclH/+Xvf//7ihUr+vfvn5+f/8EHH1h7aAAAwJpIrQAA1Rk2bNgHH3wwceJEIUR6erq1hwMAAKyJCmEAgEo99dRTmZmZnXqs9Nq1a1VVVUajUb708vLy9vb29fV1cGjj511NTU15eXlFRcXt27cdHBweeuihRx55xMPDo/1bVFRUFBYW3r59OygoaODAgebHr1+/bn5rPz8/X1/f1le4detWWVmZcl9fX9+AgICOf0YAAGwNqRUAoFKXLl0SQgwYMKAjnW/evHn+/Pm//vWvWVlZhw4dkgfHjRs3adKkmTNn6nS6/v37m/cvLy9PTU39xz/+sWfPntraWnd39/Dw8Oeffz4mJqadO1ZVVX366acJCQlCiC+++OKXv/ylEKK5ufns2bNff/31999/b37rWbNm/frXvx46dKjFFfbt2/fll18q950+ffry5ct7YHEpAAB6KVIrAEB16urqiouLd+3a5eDgsHjx4nv2b25u/u677957773CwsKgoKCJEyc6Ojo2NDSUl5d/8skn27ZtW7duXUxMjKOjo+xfXV29YcOG3//+9+7u7sHBwW5ubs3NzcXFxa+++mplZeXq1avvNqotW7asWbPG3d09JibmmWeekcePHDny2muvHT9+fPjw4ea3XrNmzfHjxzds2DB48GBlnFu2bFm7dm1DQ8Po0aM9PT2bm5tPnToVExMTFhbWdb9/AAD0LSYAAKwnKytL/jxKTEzc/S9JSUlTpkzp16/flClTLl68aHGK7P/RRx8pR/Ly8oYPHy6EmDJlyrfffltdXW0ymX766aeUlJTg4GAhxKBBg86fP6/0T05OFkL069dv2bJl8vrV1dUpKSlhYWGDBg1SukVGRgohIiMjTSZTbW1tcnKym5ubh4fHsmXL5C3k8SlTpgghnn766b1795rfWs6yrlixwnyccp3kKVOmnDp1yvy+SqLuzt9sAAB6JX46AgCsSUmtrT3yyCOffPJJUVGRxSmtU+tvf/tbIYSHh8fp06ctOu/atcvV1VUI8fHHH8sj9fX1MuJOnz5dCZ/S6dOnX331VeWlklrr6+s///xzGVmXL19uflZGRoYQwtfXt7Cw0OLWSUlJQgg3N7eamhp5RK/XtznO06dPjx49mtQKAECbqBAGAKjC+PHjvb29ZbupqenGjRsXLlx4/fXXT58+/f777ytFtm366quv5OpNI0eOtHgrKioqODj42LFjaWlpr7/+uhDiwoUL58+fF0IsXrzYYu2lkSNHbtiwweIKzc3N6enper3e3t7+V7/61R//+Efzs7799lshxODBg8+ePXv27FnzE+U+tHV1defPnw8NDRVCfPfdd22Oc+TIkfPmzcvLy+vk7xkAADaB1AoAUIX169fLrW6EELW1tefOndu6devWrVu/+OILX1/fdevW3e3Eqqqqq1evCiGUB00thIWFHTt27MyZM/JlQUGBbLSOuG2qrKx866236urqwsLCPvroI3d3d/N3T548KYQ4duzY7Nmz2zzd0dFRmR++cOGCEEL5mOYsFosCAAAKUisAQHXc3d3DwsIee+yxU6dOHThw4C9/+cvbb7/t6enZZuf8/HzZuNvav0FBQXLOU74sLi42P35PJpPpoYceEkLcuHGjpKRkxIgR5u/Kq/n5+UVERLR5ev/+/f39/TtyIwAA0CZSKwBApdzd3adOnXrgwIFr165dvHhRFtm22U026uvr2+xw48YN88lM+ZirrEPuyDAeeeSRd999d9GiRRcvXnz33Xf/9Kc/madQJycnIcSYMWP+9re/dfLzAQCADrGz9gAAALgrJWE2NzffrU9gYKCMjrL+trWcnBwhxBNPPKH0l42DBw92cBgTJkx4/fXXvby8duzYsWHDBhmDpZCQECHEtWvXOpKB5QLC169fb/1WOx8QAAAbR2oFAKhUY2NjYWGhDHuPPPLI3bq5u7vLqt3/+Z//Mc+T0sWLF48cOSKEePbZZ+WRkSNHyvT4ww8/NDY2mne+ceOGXDCptUWLFi1YsMDJyWnjxo1paWnKiWPGjJFPt8oHXNsnI+7u3bstxllcXCwHCQAAWiO1AgDUqKys7Jtvvtm5c6cQYurUqQEBAe10XrJkiZOTk8Fg2Lx58+XLl2WkrKury8/P//DDD2/evBkQEPDcc8/JzgEBAVOnThVCbNu2LTMz02g0yoScn5+/efPmJUuWtHkLNze3lStXTp069ebNm3/4wx/27t0rjz/77LM+Pj5CiISEhEOHDsmrybtfvnx579692dnZykXi4uKEEHl5edu3b5czrnKQ69evl58UAAC0xnOtAABVyMjIkDOrUl5e3t/+9rfr16+HhobKbU7bERsbu3v37oyMjPfff7+oqEjOppaXlx8+fDg1NXXQoEGvvfaa3KNV0uv158+fP3fu3DvvvBMTE+Pv719XV3fgwIFdu3bd7elZub3NmjVrfvrpp1OnTq1ZsyYoKGj48OEhISHLli37/PPPU1JSrl+/PnXqVPnUa3l5eVFRUXZ29pgxY5RFg2NjY9PS0g4cOPDRRx+VlJQMGzZMDnLPnj3jx4/Pzc3tit9IAAD6Go2yHD8AAD3v2LFjERERFpW6su73Zz/72ahRoxYvXjxr1izzt1xcXBobGxMTE//f//t/ysG8vLyEhIQTJ06UlZVVVFQIIZydnQcNGhQQEPDss8++9NJLsipY8Ze//GXLli0XLlwoKyuTnR999NGgoKDVq1ePGzdO9pk7d+6333777LPPfvPNN8qJO3bsWL58eUVFxdKlSz///HM5X5qYmLh3717lakIIX19fd3f3gICAF198ceHChcrphw4dWrt2bX5+/qVLl+THfOyxx2bMmDF+/Pi5c+c6OzvfunWrS3+DAQDo9ZhrBQBYk7+//8svv9x6+d8BAwaMGDFixowZrfezkf3Hjh1rfnD06NHr16/Pzs7Oz8+Xu9G4urqOGDFizJgx4eHhre+7cOHC4ODgnJwcuY+rq6treHj4k08+OXToUKXPnDlzBg4cGBYWZn7i888/X1BQUFxcrKwU5ebm9u67786cOVO5mqxDHjBgQOu7jxs37k9/+tPevXvlg6wDBgyYPHnyhAkTGhoali1bplwTAAAomGsFAAAAAKgXqzEBAAAAANSL1AoAAAAAUC9SKwAAAABAvUitAAAAAAD1IrUCAAAAANSL1AoAAAAAUC9SKwAAAABAvUitAAAAAAD1IrUCAAAAANSL1AoAAAAAUC9SKwAAAABAvf4/MfbhtxoofHgAAAAASUVORK5CYII=)"
      ],
      "metadata": {
        "id": "Ms-z7_08rywW"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        " \n",
        "\n",
        "**b.** Modele em lógica temporal linear LT  propriedades que caracterizam o comportamento desejável do sistema:\n",
        "\n",
        "> I.  O veículo imobiliza-se completamente em menos de $t$ segundos.\n",
        "\n",
        "$G(m = STOPPED \\rightarrow t \\le 12)$\n",
        "\n",
        "> II.  As velocidades $\\,V, v\\,$ diminuem sempre com o tempo.\n",
        "\n",
        "$G(t' > t \\rightarrow (V' < V \\wedge v' < v))$\n",
        "\n",
        "Para além destas propriedades, decidimos definir outras duas:\n",
        "\n",
        "> III. O veículo permanece no Modo FREE em menos de $t$ segundos.\n",
        "\n",
        "$F(m = FREE \\wedge c > 0 \\rightarrow m = STOPPING)$\n",
        "\n",
        "> IV. O veículo permanece no Modo BLOCKED em menos de $t$ segundos.\n",
        "\n",
        "$F(m = BLOCKED \\wedge c > 0 \\rightarrow m = FREE)$"
      ],
      "metadata": {
        "id": "LfiRQ5JGlM3T"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "**c.** Codificação (em SMT’s) do modelo que definimos em a:"
      ],
      "metadata": {
        "id": "qgx-etG1kmK6"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "!pip install z3-solver\n",
        "\n",
        "from z3 import *"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "ZeiEixo28_f9",
        "outputId": "cc72bb04-9e6e-446d-db1c-a5ae716eef7f"
      },
      "execution_count": null,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "Requirement already satisfied: z3-solver in /usr/local/lib/python3.7/dist-packages (4.8.13.0)\n"
          ]
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "Mode, (START,FREE,STOPPING,BLOCKED,STOPPED) = EnumSort('Mode', ('START','FREE','STOPPING','BLOCKED','STOPPED'))\n",
        "\n",
        "def declare(i):\n",
        "  s={}\n",
        "  s['m'] = Const('m'+str(i), Mode)\n",
        "  s['n'] = Const('n'+str(i), Mode)\n",
        "  s['t'] = Real('t'+str(i))\n",
        "  s['z'] = Real('z'+str(i))\n",
        "  s['c'] = Real('c'+str(i))\n",
        "  s['V'] = Real('V'+str(i))\n",
        "  s['v'] = Real('v'+str(i))\n",
        "  return s"
      ],
      "metadata": {
        "id": "y9uyf2zE9FKA"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "def init(s):\n",
        "  vzero = 30\n",
        "  return And(s['m']==START, s['n']==START, s['t']==0, s['z']==0, s['c']==1, s['V']==vzero, s['v']==vzero)"
      ],
      "metadata": {
        "id": "7T9pzsJg9Hqd"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "def trans(s, p):\n",
        "  #Constantes\n",
        "  a  = 0.008\n",
        "  P  = 1000\n",
        "  f  = a*P\n",
        "  cf = 1.6\n",
        "  cs = 3.2\n",
        "  b  = 0.8\n",
        "\n",
        "  #untimed\n",
        "  stf  = And(s['m']==START,    p['m']==FREE,     s['n']==START,    p['n']==FREE,     p['t']==s['t'], p['z']==s['z'],           p['c']==s['c'],            p['V']==s['V'],            p['v']==s['v'])\n",
        "  fsg  = And(s['m']==FREE,     p['m']==STOPPING, s['n']==FREE,     p['n']==STOPPING, p['t']==s['t'], p['z']==s['z'], s['c']>0, p['c']==s['c'],            p['V']==s['V'],            p['v']==s['v'], s['V']-s['v']>1.5)\n",
        "  sgb  = And(s['m']==STOPPING, p['m']==BLOCKED,  s['n']==STOPPING, p['n']==BLOCKED,  p['t']==s['t'], p['z']==s['z'],           p['c']==0.5,    s['V']>0,  p['V']==s['V'], s['v']>0,  p['v']==s['v'], s['V']-s['v']==0)\n",
        "  bf   = And(s['m']==BLOCKED,  p['m']==FREE,     s['n']==BLOCKED,  p['n']==FREE,     p['t']==s['t'], p['z']==s['z'], s['c']>0, p['c']==1,                 p['V']==s['V'],            p['v']==s['v'], s['V']-s['v']>0)\n",
        "  sgsd = And(s['m']==STOPPING, p['m']==STOPPED,  s['n']==STOPPING, p['n']==STOPPED,  p['t']==s['t'], p['z']==s['z'],           p['c']==s['c'], s['V']==0, p['V']==s['V'], s['v']==0, p['v']==s['v'])\n",
        "  sdsd = And(s['m']==STOPPED,  p['m']==STOPPED,  s['n']==STOPPED,  p['n']==STOPPED,  p['t']==s['t'], p['z']==s['z'],           p['c']==s['c'],            p['V']==s['V'],            p['v']==s['v'])\n",
        "\n",
        "  #timed\n",
        "  free     = And(s['m']==FREE,     p['m']==FREE,     s['n']==FREE,     p['n']==FREE,     p['t']>s['t'], p['z']>s['z'], p['t']-s['t']==p['z']-s['z'], s['c']>0, p['c']>0, p['c']==s['c']-p['z']+s['z'], s['V']>0,  p['V']>0,  p['V']<s['V'], p['V']-s['V']>=(-cf*2-b)*(p['t']-s['t']),   s['v']>0,  p['v']>0,  p['v']<s['v'], p['v']-s['v']>=(-f+(cf*2))*(p['t']-s['t']),   s['V']>=s['v'], p['V']>=p['v'], s['V']-s['v']<=2,   p['V']-p['v']<=2)\n",
        "  stopping = And(s['m']==STOPPING, p['m']==STOPPING, s['n']==STOPPING, p['n']==STOPPING, p['t']>s['t'], p['z']>s['z'], p['t']-s['t']==p['z']-s['z'],                     p['c']==s['c'],               s['V']>=0, p['V']>=0, p['V']<s['V'], p['V']-s['V']>=(-cs*0.1-b)*(p['t']-s['t']), s['v']>=0, p['v']>=0, p['v']<s['v'], p['v']-s['v']>=(-f+(cs*0.1))*(p['t']-s['t']), s['V']>=s['v'], p['V']>=p['v'], s['V']-s['v']<=0.1, p['V']-p['v']<=0.1)\n",
        "  blocked  = And(s['m']==BLOCKED,  p['m']==BLOCKED,  s['n']==BLOCKED,  p['n']==BLOCKED,  p['t']>s['t'], p['z']>s['z'], p['t']-s['t']==p['z']-s['z'], s['c']>0, p['c']>0, p['c']==s['c']-p['z']+s['z'], s['V']>0,  p['V']>0,  p['V']<s['V'], p['V']-s['V']<=(-f-b)*(p['t']-s['t']),      s['v']>0,  p['v']>0,  p['v']<s['v'],                                               s['V']>=s['v'], p['V']>=p['v'])\n",
        "\n",
        "  return Or(stf, fsg, sgb, bf, sgsd, sdsd, free, stopping, blocked)"
      ],
      "metadata": {
        "id": "tXW8mqSJ9Jzw"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [
        "def gera_traco(declare, init, trans, k):\n",
        "  s = Solver()\n",
        "  traco = [declare(i) for i in range(k)]\n",
        "\n",
        "  s.add(init(traco[0]))\n",
        "  for i in range(k-1):\n",
        "    s.add(trans(traco[i], traco[i+1]))\n",
        "\n",
        "  if s.check() == sat:\n",
        "    m = s.model()\n",
        "    for i in range(k):\n",
        "      print(\"Estado: \",i)\n",
        "      for v in traco[i]:\n",
        "        r = m[traco[i][v]]\n",
        "        if r.sort() != RealSort():\n",
        "          print(v, '=', r)\n",
        "        else:\n",
        "          print(v, '=', float(r.numerator_as_long())/float(r.denominator_as_long()))\n",
        "\n",
        "gera_traco(declare, init, trans, 5)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "5AzvRvTd9NCw",
        "outputId": "f75a8971-ec90-4f5f-a180-83655a33b6c5"
      },
      "execution_count": null,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "Estado:  0\n",
            "m = START\n",
            "n = START\n",
            "t = 0.0\n",
            "z = 0.0\n",
            "c = 1.0\n",
            "V = 30.0\n",
            "v = 30.0\n",
            "Estado:  1\n",
            "m = FREE\n",
            "n = FREE\n",
            "t = 0.0\n",
            "z = 0.0\n",
            "c = 1.0\n",
            "V = 30.0\n",
            "v = 30.0\n",
            "Estado:  2\n",
            "m = FREE\n",
            "n = FREE\n",
            "t = 0.6666666666666666\n",
            "z = 0.6666666666666666\n",
            "c = 0.3333333333333333\n",
            "V = 27.833333333333332\n",
            "v = 26.8\n",
            "Estado:  3\n",
            "m = FREE\n",
            "n = FREE\n",
            "t = 0.8333333333333334\n",
            "z = 0.8333333333333334\n",
            "c = 0.16666666666666666\n",
            "V = 27.666666666666668\n",
            "v = 26.0\n",
            "Estado:  4\n",
            "m = STOPPING\n",
            "n = STOPPING\n",
            "t = 0.8333333333333334\n",
            "z = 0.8333333333333334\n",
            "c = 0.16666666666666666\n",
            "V = 27.666666666666668\n",
            "v = 26.0\n"
          ]
        }
      ]
    },
    {
      "cell_type": "markdown",
      "source": [
        "**d.** Verificação das propriedades temporais que definimos em b:"
      ],
      "metadata": {
        "id": "NzXV_7fUeAI4"
      }
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "id": "xf0EmMD8o1qf"
      },
      "outputs": [],
      "source": [
        "def bmc_always(declare, init, trans, inv, K):\n",
        "    for k in range(1, K+1):\n",
        "        s = Solver()\n",
        "\n",
        "        traco = [declare(i) for i in range(k)]\n",
        "        s.add(init(traco[0]))\n",
        "        for i in range(k-1):\n",
        "            s.add(trans(traco[i], traco[i+1]))\n",
        "        s.add(Not(inv(traco[k-1])))\n",
        "\n",
        "        if s.check() == sat:\n",
        "            print(\"\\nA propriedade falha em traços de tamanho\",k)\n",
        "            n = s.model()\n",
        "            for i in range(k):\n",
        "                print(\"Estado:\", i)\n",
        "                for v in traco[i]:\n",
        "                    r = n[traco[i][v]]\n",
        "                    if r.sort() != RealSort():\n",
        "                        print(v, '=', r)\n",
        "                    else:\n",
        "                        print(v, '=', float(r.numerator_as_long())/float(r.denominator_as_long()))\n",
        "    print(\"A propriedade é válida em traços de tamanho até \"+str(k))\n",
        "\n",
        "def bmc_eventually(declare, init, trans, prop, K):\n",
        "    for k in range(1, K+1):\n",
        "        s = Solver()\n",
        "\n",
        "        traco = [declare(i) for i in range(k)]\n",
        "        s.add(init(traco[0]))\n",
        "        for i in range(k-1):\n",
        "          s.add(trans(traco[i],traco[i+1]))\n",
        "\n",
        "        #Forçar o loop\n",
        "        s.add(Or([trans(traco[k-1],traco[i]) for i in range(k)]))\n",
        "\n",
        "        #Testar que a propriedade nunca é válida\n",
        "        for i in range(k):\n",
        "          s.add(Not(prop(traco[i])))\n",
        "\n",
        "        if s.check() == sat:\n",
        "          print(\"A propriedade falha\")\n",
        "          n = s.model()\n",
        "          for i in range(k):\n",
        "              print(\"Estado:\", i)\n",
        "              for v in traco[i]:\n",
        "                  r = n[traco[i][v]]\n",
        "                  if r.sort() != RealSort():\n",
        "                      print(v, '=', r)\n",
        "                  else:\n",
        "                      print(v, '=', float(r.numerator_as_long())/float(r.denominator_as_long()))\n",
        "    print(\"A propriedade é válida em traços de tamanho até \"+str(k))"
      ]
    },
    {
      "cell_type": "markdown",
      "source": [
        "I.  O veículo imobiliza-se completamente em menos de $t$ segundos:"
      ],
      "metadata": {
        "id": "Pg8uur0RpoiI"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "def terminates_in_time(s):\n",
        "    return Implies(s['m'] == STOPPED, s['t']<=12)\n"
      ],
      "metadata": {
        "id": "0SUW6H8JoqCc"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "source": [
        "II.  As velocidades $V, v$ diminuem sempre com o tempo:\n"
      ],
      "metadata": {
        "id": "Z-lzfVPKpwtG"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "def vel_decreases(s):\n",
        "  p = declare(1)\n",
        "  return Implies(And(trans(s,p), p['t']>s['t']), And(p['V']<s['V'], p['v']<s['v']))"
      ],
      "metadata": {
        "id": "v1Z1maynoraG"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "source": [
        "III. O veículo permanece no Modo FREE em menos de $t$ segundos:\n"
      ],
      "metadata": {
        "id": "8DdGZL7IrL4w"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "def free_in_time(s):\n",
        "  p = declare(1)\n",
        "  return Implies(And(trans(s,p), s['m']==FREE, s['c']>0), p['m']==STOPPING)\n"
      ],
      "metadata": {
        "id": "RCMPD_vwpDvo"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "source": [
        "IV. O veículo permanece no Modo BLOCKED em menos de $t$ segundos:\n"
      ],
      "metadata": {
        "id": "VKBfi5zDrR8j"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "def blocked_in_time(s):\n",
        "  p = declare(1)\n",
        "  return Implies(And(trans(s,p), s['m']==BLOCKED, s['c']>0), p['m']==FREE)"
      ],
      "metadata": {
        "id": "_EJuLOC0rBhF"
      },
      "execution_count": null,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "source": [
        "Verificação:"
      ],
      "metadata": {
        "id": "7c-gzE7TgC6-"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "print(\"Verificar se o veículo se imobiliza completamente em menos de t segundos:\")\n",
        "bmc_always(declare, init, trans, terminates_in_time, 5)\n",
        "\n",
        "print(\"\\nVerificar se as velocidades V e v diminuem sempre com o tempo:\")\n",
        "bmc_always(declare, init, trans, vel_decreases, 5)\n",
        "\n",
        "print(\"\\nVerificar se permanecemos no modo FREE em menos de t segundos:\")\n",
        "bmc_eventually(declare, init, trans, free_in_time, 5)\n",
        "\n",
        "print(\"\\nVerificar se permanecemos no modo BLOCKED em menos de t segundos:\")\n",
        "bmc_eventually(declare, init, trans, blocked_in_time, 5)"
      ],
      "metadata": {
        "id": "GleWf38BrGKz",
        "outputId": "355a0c86-ea3d-491b-e5f7-1c92424be05d",
        "colab": {
          "base_uri": "https://localhost:8080/"
        }
      },
      "execution_count": null,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "Verificar se o veículo se imobiliza completamente em menos de t segundos:\n",
            "A propriedade é válida em traços de tamanho até 5\n",
            "\n",
            "Verificar se as velocidades V e v diminuem sempre com o tempo:\n",
            "A propriedade é válida em traços de tamanho até 5\n",
            "\n",
            "Verificar se permanecemos no modo FREE em menos de t segundos:\n",
            "A propriedade é válida em traços de tamanho até 5\n",
            "\n",
            "Verificar se permanecemos no modo BLOCKED em menos de t segundos:\n",
            "A propriedade é válida em traços de tamanho até 5\n"
          ]
        }
      ]
    }
  ]
}