multiagent.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "3b359025",
   "metadata": {},
   "source": [
    "# Trajectory planning for multi-agent systems"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "07cd83c6",
   "metadata": {},
   "source": [
    "Multi-agent path finding (MAPF) is a problem that has been studied for a large number of years for applications including robotics, aviation, video games, and more [[Dresner and Stone 2008](https://www.jair.org/index.php/jair/article/download/10542/25241),\n",
    "[Ma et al. 2017](https://ojs.aaai.org/index.php/AIIDE/article/download/12919/12767),\n",
    "[Pallottino et al. 2007](https://ieeexplore.ieee.org/iel5/8860/4399947/04392815.pdf?casa_token=HP6WWjHKswQAAAAA:ua93qnZ1EBG34GM6r84yNkR5h7uZqYqh3HjF8xB0_zhIMlWwmuI8RMIJ6h-QWElqXOZlSg),\n",
    "[Silver 2005](https://ojs.aaai.org/index.php/AIIDE/article/download/18726/18503),\n",
    "[Wurman et al. 2008](http://www.dcsc.tudelft.nl/~sc4081/2018/assign/pap/robert_kiva_paper.pdf)]. It raises the question of how multiple agents can reach their goal position without colliding with each other.\n",
    "\n",
    "In this case study we are using contracts defined in pacti to ensure that the resulting path is conflict-free. We are focusing on vertex conflicts, where two or more agents cannot share a grid cell, and swapping conflicts, preventing two agents from swapping positions in two adjacent cells. For a detailed survey on objective functions and conflict types, see [[Stern et al. 2019](https://arxiv.org/abs/1906.08291)].\n",
    "\n",
    "In the following section we will explain the problem setup and illustrate our approach of using contracts to find a safe strategy for the robots. The benefit of using contracts for this application is how modularly we can add/remove robots or additional contraints to the problem.\n",
    "\n",
    "In the video below you can see the implementation of the resulting strategy for five robots on the\n",
    "[Robotarium](https://www.robotarium.gatech.edu) [[Wilson et al. 2020](https://ieeexplore.ieee.org/iel7/5488303/8960558/08960572.pdf?casa_token=5GsOySsxPm4AAAAA:gVhO3ngOXJzZ-gnupam3LFl5EDInm50sLy4BTUP8zqxuDvAMRyMKNAp_bPOvBPKmcYbjZg)].\n",
    "\n",
    "![Robotarium Implementation](https://github.com/pacti-org/media/blob/main/case_studies/multiagent_coordination/robotarium.gif?raw=true)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5cf987f5",
   "metadata": {},
   "source": [
    "This case study shows how Pacti can be used to formalize a multiagent navigation problem and synthesize a strategy for the robots to reach their respective goal position without crashing into each other.\n",
    "\n",
    "We will start by importing the relevant packages."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "eb50b037",
   "metadata": {},
   "outputs": [],
   "source": [
    "%matplotlib inline\n",
    "import numpy as np\n",
    "from utils.multiagent_utils import (\n",
    "    Coord,\n",
    "    Robot,\n",
    "    distance,\n",
    "    find_random_move,\n",
    "    get_collision_contract,\n",
    "    get_swapping_contract,\n",
    "    check_move\n",
    ")\n",
    "from utils.plotting_utils import (\n",
    "    Snapshot,\n",
    "    animate,\n",
    "    plot_grid_world,\n",
    "    save_trace\n",
    ")\n",
    "from utils.swapping_contract import get_swapping_contracts_list\n",
    "from utils.collision_contract import get_collision_contracts_list\n",
    "from utils.stay_at_goal_contract import robots_stay_at_goal\n",
    "from utils.dynamics_contract import get_dynamics_contract\n",
    "\n",
    "from utils.optimize_utils import optimize_contract\n",
    "from utils.behavior_utils import ntl_contains_behavior, tl_contains_behavior, extend_var_dict\n",
    "\n",
    "from pacti.iocontract import Var\n",
    "from pacti.contracts import PolyhedralIoContract, PolyhedralIoContractCompound\n",
    "from typing import List\n",
    "from itertools import combinations\n",
    "import random"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5b4d753e",
   "metadata": {},
   "source": [
    "### Create gridworld and robots"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "104e7504",
   "metadata": {},
   "source": [
    "First we will create the grid world with the dimensions $grid_{n} \\times grid_{m}$ for our robots to move in. Each robot starts at their respective initial condition, with the task to reach its goal position on the grid. \n",
    "To initialize the robots and set up the grid world, we will call the functions that we imported from multiagent_utils."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "97ad2a36",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAgMAAAEiCAYAAABkw9FZAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjcuNCwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy8WgzjOAAAACXBIWXMAAA9hAAAPYQGoP6dpAAAgBUlEQVR4nO3de3BV9d3v8c/aa2cn2bkDARIIAcpFBYvUCxioD1QehXAEz5n6jFUfRTtYHS+jf7TTdqYzenpOferUcVqtWn2qzuCx5+mxN4faVkVtJyAKQWtrNZRbCASQALkSkuy11/njZwIYk6xA9l5h/96vGSaXvbN+v734Juuzf+u3fsvxfd8XAACwViTsDgAAgHARBgAAsBxhAAAAyxEGAACwHGEAAADLEQYAALAcYQAAAMsRBgAAsBxhAAAAyxEGgHPEmjVrNHXq1CGft2fPHjmOo+effz7lfTpbS5Ys0ZIlS4Z83ltvvSXHcfTWW2+lvE+AjQgDQIrt3r1bd999t2bNmqV4PK54PK4LLrhAd911lz744INQ+vTuu+/KcRw9+uij/R5bvXq1HMfRc8891++xK664QpMmTUpHFwGkEWEASKH169dr7ty5WrdunZYtW6ZHH31UP/7xj7VixQq98soruuiii1RfXx9oW88884zq6upGpF9f+tKXFI/HVVNT0++xTZs2KRqNauPGjad9v7u7W1u2bNGiRYtGpA8ARo9o2B0AMtXOnTt1/fXXq7KyUhs2bFBZWdlpj//whz/UE088oUhk8Eze0dGhvLw8ZWVljVjfotGoFixY0O+AX1dXp6amJt1www39gkJtba1OnDihxYsXn3X7x48fVzweP+vtABgZjAwAKfLwww+ro6NDzz33XL8gIJkD8r333quKioq+761Zs0b5+fnauXOnqqurVVBQoBtvvLHvsc/OGWhubtaaNWtUVFSk4uJi3XLLLWpubg7Uv8WLF+vQoUPasWNH3/c2btyowsJC3X777X3B4NTHen+u1xNPPKE5c+YoOztb5eXluuuuu/q1v2TJEs2dO1e1tbW64oorFI/H9d3vfnfAfu3bt0/XXnut8vLyNH78eN1///3q6uoK9JoAnBlGBoAUWb9+vWbMmKEFCxYM6+cSiYSuvvpqLV68WD/60Y8GfAft+75Wr16tmpoa3XHHHTr//PP1m9/8RrfcckugdnoP6jU1NZoxY4Ykc8BfuHChFixYoKysLG3atEmrVq3qe6ygoEDz5s2TJD3wwAN68MEHtWzZMt15552qq6vTk08+qS1btmjjxo2njWQcOXJEK1as0PXXX6+bbrpJEyZM+Nw+dXZ26sorr9TevXt17733qry8XOvWrdMbb7wRbOcBOCOEASAFWltb1djYqGuvvbbfY83NzUokEn1f5+XlKTc3t+/rrq4uXXfddXrooYcGbePll1/WX/7yFz388MP65je/KUm68847tXTp0kB9vPzyy+W6rmpqarRmzRpJ5oB/ww03KCcnR/Pnz1dNTc1pYWDhwoVyXVeHDx/WQw89pKuuukp/+MMf+k51nHfeebr77rv1wgsv6NZbb+1r6+DBg3rqqaf0jW98Y9A+Pf3009q+fbt++ctf6rrrrpMkrV27ti+AAEgNThMAKdDa2ipJys/P7/fYkiVLVFpa2vfvpz/9ab/n3HnnnUO28corrygajZ72XNd1dc899wTqY0FBgb74xS/2zQ1oampSXV2dqqqqJEmLFi3qOzWwfft2HT58uG804fXXX1d3d7fuu+++0+Y8rF27VoWFhfr9739/WlvZ2dmnhYPBXlNZWZm++tWv9n0vHo/r9ttvD/SaAJwZwgCQAgUFBZKk9vb2fo/97Gc/02uvvaYXXnjhc382Go1q8uTJQ7ZRX1+vsrKyfoFj9uzZgfu5ePHivrkBmzZtkuu6WrhwoSSpqqpKtbW16urq6jdfoPcKiM+2FYvFNH369H5XSEyaNEmxWCzQa5oxY4Ycxznj1wRg+AgDQAoUFRWprKxMf//73/s9tmDBAi1btmzAS/Sys7OHvMJgpPQe3Ddu3KiNGzfqwgsv7AsXVVVV6urq0pYtW1RTU6NoNNoXFIbr1NMgAEYfwgCQIitXrtSOHTv07rvvpmT7lZWVOnDgQL/Rh+GsRXDqJMKNGzeeFlDKy8tVWVnZFxTmz5/fN5mxsrLyc9vq7u7W7t27+x4/k9e0c+dO+b5/xq8JwPARBoAU+da3vqV4PK7bbrtNhw4d6vf4Zw94w1VdXa1EIqEnn3yy73ue5+mxxx4LvI3y8nJNmzZNGzZs0NatW/vmC/SqqqrSb3/7W9XV1Z12SeGyZcsUi8X0k5/85LTX8fOf/1wtLS1auXLlGb+mxsZGvfTSS33fO378uJ5++ukz2h6AYLiaAEiRmTNn6sUXX9TXvvY1zZ49WzfeeKPmzZsn3/e1e/duvfjii4pEIoHmB3yea665RosWLdK3v/1t7dmzRxdccIF+/etfq6WlZVjbWbx4sdatWydJ/U5dVFVV6Re/+EXf83qVlpbqO9/5jh588EEtX75cq1atUl1dnZ544gldeumluummm87oNa1du1aPP/64br75ZtXW1qqsrEzr1q1jgSIgxQgDQAqtXr1af/vb3/TII4/o1Vdf1bPPPivHcVRZWamVK1fqjjvuOOPL5iKRiF5++WXdd999euGFF+Q4jlatWqVHHnlE8+fPD7yd3jAwadKkfsP7p4aDz648+MADD6i0tFSPP/647r//fo0ZM0a33367fvCDH5zxaonxeFwbNmzQPffco8cee0zxeFw33nijVqxYoeXLl5/RNgEMzfHPdqwSAACc05gzAACA5QgDAABYjjAAAIDlCAMAAFiOMAAAgOUIAwAAWC7QOgPJZFKNjY0qKCjodwMRAAAwOvm+r7a2NpWXlw96z5NAYaCxsVEVFRUj1jkAAJA+DQ0Ng652GigM9N6OtaGhQYWFhSPTMwAAkFKtra2qqKjoO44PJFAY6D01UFhYSBgAAOAcM9QpfiYQAgBgOcIAAACWIwwAAGA5wgAAAJYjDAAAYDnCAAAAlgt0aWEqdXd3S5Jc1w25J6Of53mS2FdBsK+CY18Fx74Kjn0VXO++isViofUh1DDQ3d2t73//+5Kf0MWXzJc7yFKJtvOSSdVu3SbJ0cWXLOAXbBCe56m2tpa6CoC6Co66Co66Cq6vriR973vfCy0QhD4yID8hJQ9L3j7J55drQMmklGz69IuEJH65BkVdBUNdDQ91FQx1dc4JNQy4rquLL75I8varenkV6XEQnudJvvm8esUyudHBl5a0mdlXXdRVANRVcNRVcNRVcL2nCKRwT6mEPjJgXnxEruvyyzUE1418+pF9NRTqKjjqKjjqKjjqKrjRsH8Y5wIAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHLRsDswGjQ0ZGnnrmztqY9p585stbdH5CUd5eYmNW1qt6ZN7VLllG7NmtWlCPEJAM4Nvi8dOSI1N0vHjpnPe3okx5FycqRx46TiYmnMGKmwMOzehsraMNDTI23Zmqc/vVagrbV5am115ftSVlZSWVFfciTPc7RxU54kKZ7ra/bsE1pxdasWL2pXYWEy5FcAAPhcXV3S3r1SXZ35ePy4CQCxmOS65jmJxMlgkJ8vzZghzZwplZeffI5FrAwDdXXZeuqZcXr//bgSnjRhfI/Ky7oHfNfv+1J7e0R//zBH77+fq2nTSvT1W4/oii+3y3HS23cAwAB8X6qvlzZvlhobpWhUKi2VJk/WgH+sk0mppUV6/33pgw9MIFiwwIwaWMSqMJBISL98qUS/+K8SHTvmatrULsXj/pA/5zhSQUFSBQVd6umR9uzJ1vf/90RdfVWr1n79iIqLvTT0HgAwoBMnpC1bzEHd96Vp00wYGEokIpWUmH+dndJHH0kHDkiXXSbNnStbzg3b8SplRoN+8vh4PfX0OMmXLjj/RKAg8FlZWdLMmV0aMyah3/yuWP/zf01UU5N9Q0oAMGocPy5t2CC9/bY5qAcNAp+VmyvNmmXCxOuvmxEGz443e1aEAc+TnniqVL/5XbHKJvaovLznrIf3S0o8zZxxQpvfzdMP/mOiWlqs2JUAMLqcOCG9+ab04YfS9OlSUdHZbc9xpIkTpQkTTLjYssWcSshwVhzB/vinQv325WKVTewe0SH9nBy/LxA88+w4+cMfaAAAnI3a2pNBIDt75LZbWGgCwebN0o4dI7fdUSrjw8C+fVl6ft1YxWJJlZSM/HBPTo6vSZO69cc/FapmY96Ibx8AMID6eum998wVACMZBHoVFZntvvOO1No68tsfRTI6DPi+9OzzY7V/f5amVHSnrJ0xJZ6SnvSfz45TW1tG71IAGB26u81BOpk8+1MDgykvlw4elLZtS10bo0BGH7l2745p8zt5mlQ+8GWDI2Xq1C7t2h3TprcZHQCAlNu7V9q3z1w2mEqRiDldUFdnFi7KUBkdBt78c75aWtyUnB74rKwsyXV9/fHVQuYOAEAq+b708cfmQJ2Vlfr2iovNaYLdu1PfVkgyNgwkEtKGNwpVWOSlbWGgsok9+uijHO3aFUtPgwBgo2PHpIYGafz49LTnOGZC4ccfZ+yVBRkbBvbvj+noMVfFRYm0tZmfn1RHR0R76lMwkQUAYDQ3Sx0dZhnhdCksNKMDbW3pazONMjYM7G3IUkdHRPn56UtxkYjkS9pTz8gAAKRMc7P5mM714HNzzeJGLS3pazONMjYMHDxoziOleyXJrCxf9fVpOIcFALY6etTcdCidXNfMVWBk4NzS3e1ISv9dhFxX6uxkeWIASJnu7vDuLJihyxNnbBgwo0chTOv3pUiEywkAIGXCvHlQht6qNmPDQDyeDCUL9PQ4KizKzOQIAKNCbq65+1wY0nEpYwgyNgxMntwjN9p7uiB9vKSj6VNTt9ohAFhvzJj0D9f39Jg7IRYWprfdNMnYMFA5pVv5+Z7aO9L3EhMJc4qgspIwAAApU1xshuvTGQg6OqS8PNN2BsrYMDBuXEJTKnp09MgZ3NP6DB09FlVxkacZX+hKW5sAYJ0xY8w79N5LDNOhuVkqLZXi8fS1mUYZGwYcR1p+Vau6uh0l0rTu0OHDUVVVdWj8+PQtdAQA1snLk2bNko4cSU97nmeuYDjvvPS0F4KMDQOS9OXF7ZowIaFDh1I/4aO9PaLsmK9lX8nMa1ABYFSZMcOsNdDRkfq2Dh+Wxo2TKitT31ZIMjoMlJR4umZli441R9XVlbqJhL5vVh289NLjumje8ZS1AwD41MSJZnRg3z6l9O5wXV1m1cF586ScnNS1E7KMDgOS9G9fPab5845r566clNVLw76YJoxP6I61TYqmb4oCANgrEpEWLDDv2A8cSF07e/ea0DFnTuraGAUyPgzE477uuL1JJcUJ7dkz8stXHjniqrMzon+/8aimckkhAKRPcbEJBJ2d5k6GI62hQSoqkhYuzNj1BXplfBiQpLlzT+jeuw8rGpV2746N2AhBU1NUnxzO0r999ZhWr8rMm1cAwKh23nlSVZWZTHj06Mhtt6HBLHm8dGn6bpUcImsGtZdd2SbHkX78eKk++ihH06d3KSfnzFKB50m792TL96Wbbjiq29YcCXV1TACwluNIl1xiPr79trmR0OTJZ37vgq4uqb7ejDosXSpNnz6i3R2trAkDknTlV9o0cUKPnnpmnN57L66i4oQmTugJfJ4/mZSOHI3q4MEsTa3s1tdvPaKvLG3L1KWqAeDcEImYQDB2rPTOO9I//2nWBCgpCX4fg0TCXDXQ2irNnm1ODZSWprbfo4hVYUCS5sw5oYcf2q//96sSvby+SNv/mausaFJjxiSUn59ULOafdnBPJKT2dlfNLa7a212NKUno2lXNWnPzUdYTAIDRwnHMu/gJE6Rt26S6Omn7dik/3yxQFI+r3zu/7m5zaWJzs1luuLRUuuwyM1kww+cIfJZ1YUCScnN93XzTUa2+plk1G/P1x1cLVV8f0969WerpMTXly5F8XxFXys9Pqmxij/512VEtuaJdkyaFdIMMAMDg8vKkL3/ZXApYXy999JE52B8+3H/54qws8/zp081oQEVFRl8+OBgrw0CvoqKkVla3qnpFq5qbXe3dG1PDvix1dkbk+1Is5qusrEeVU7o1fnyCeQEAcK4oLJQuvFCaO/fku//29pOBICvLPKe42NoAcCqrw0AvxzELFJWUdGrevM6wuwMAGCmOY04V5OeH3ZNRjfe6AABYjjAAAIDlCAMAAFiOMAAAgOUIAwAAWI4wAACA5QgDAABYjjAAAIDlCAMAAFiOMAAAgOUIAwAAWI4wAACA5QgDAABYjjAAAIDlCAMAAFiOMAAAgOUIAwAAWI4wAACA5aJhd8DzPMlLmo8YkOd58rxk3+dy2F8DMfuKugqCugqOugqOugqur65CFmoY8DxPtbXvSckmyZHcCAMVA/GSSdVu+4f5wl0v180Jt0OjmJdMqnbrFslvpq6GQF0FR10FR10FZ+pqmyRH1dXVcl03lH6EPjIgOWF34NyT/ESc4RlEMmn+YGN4qKvBUVdnhroaXDJp3hBLkt8tKRZKN0INA67r6uJLFkh+j6qr/zW0RHQuMENt66XkJ6peXsW+GoTneZJvPq9eeYPcaF64HRrFqKvgqKvgqKvgTq0r1/VD60foIwOmSFy50QIKZjCOJzeaI3kRua7LvhqC65p3Im40T260IOTejGLU1bBQVwFRV8PSW1dhCr8HAAAgVIQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHLRsDvged5pH/H5PM8z+8hLsq+GYPZVsu9zOeyvgVBXwVFXwVFXwZ1aV2EKNQx4nqfa2lrJT0jqlhthoGIgXjKp2q1bJL9ZcsS+GoSXTKp22z/MF+56uW5OuB0axair4Kir4Kir4E6tq+prPLkhHZVDHxmQn5CShyVvn+RTMANKJs0vFoYn+Yk4GzYI6urMUFeDo67OUHiH5FDDgOu6uvjiiyRvv6qXV8l13TC7M6p5nif55vPqlTfIjeaF26FRzAzhrpeSn1BXQ6CugqOugqOugvM8T4r8SVJEbjQ3tH6EPjJgfqEicl2XX64huK55J+JG8+RGC0LuzSjmeHKjOZJHXQVBXQVEXQ0LdRWQ48mNxsPuBeNcAADYjjAAAIDlCAMAAFiOMAAAgOUIAwAAWI4wAACA5QgDAABYjjAAAIDlCAMAAFiOMAAAgOUIAwAAWI4wAACA5QgDAABYjjAAAIDlCAMAAFiOMAAAgOUIAwAAWI4wAACA5aJhd2BU8H2puU2qPyDtPyR1dpnvxbKksnFSxURpwlgpQnYCgHOJ70sdHVJzs9TeLnme+X5WllRYKBUVSbm5oXZxVLA7DLS0STXvSa9tNkGg/bjUk5AcR5Iv+ZJcR8qLS6Ul0pULpCsuliZPCLvnAIBBtLZKe/ZIH39sgsDx4yeDQK+sLCkvT5owQZo1S5oyRcrJCaO34bMzDHSekH71urT+L9KhI1I0Ko0plKZMNKMBjnPyuYmE1N4pHWySfvaS9MtXpcXzpZuvkcaPCe81AAD66eiQtm2T6uqkY8ek/HwzAlBaav7Un6q72zx/1y7z/NJS6YtflObMMUHBJvaFgQ93Ss/8SnrvY6m4QJpZKUXdgZ8fjZrnFRdISV862iy9/Kb01zrp1mulpZeeHh4AAGnn+9Lu3dLmzdK+fSff7Q92djcWM/9KSsz7vqYm6fXXpYYGaeFCEw5sYVcYeONd6fFfSEdbpS9USDmx4f18xJHGlUglhdKeA9J//Fza1SCtWd0/cgIA0iKZlGprpbffllzXhAB3kPd4nycalSZONMFg+3bpk0+kpUul6dNT0+fRxp4ZcRvekR5dZyYHnj9t+EHgVK4rfWGyGS148Q/Sf/7aVCMAIK18X9q6VaqpMZMBp0wZfhA4VXa2CRNdXdJrr5lTCDawIwz8fYf0+P+VEp40bdLIDeuPKzETC196XXr5zyOzTQBAYB9/LG3aJI0dK40ZwWlcFRVmwuGbb5pRgkyX+WHgeKf09EtSc6s0tXzktz+2WMrNlv7PemlP48hvHwDwuY4dk955x1waWFIy8tuvqJBaWsw8hJ6ekd/+aJL5YeCl16W/bpemT07dRL/JE6RPjknPvGRmoQAAUiqZlN5910z6KytLXTtTppg5BB9+mLo2RoPMDgPHWqX1fzbn9rPPYo7AUBxHqiyTtnxoggcAIKUOHjQH6ckpfJ8nmTkERUXSX/8qnTiRunbCltlhoOY96ZOjZvXAVMuPS9090hvvpL4tALDcjh1mnYC8vNS3VVpqRiDq61PfVlgyNwz4vvTqJnMR6WDrCIyk0hJp0wcmgAAAUqKjw4wKjE3D+zzJXJ0Qi5nJipkqc8NAU7PUcFAaW5S+NkuKzBLHOxvS1yYAWOboUbPccHFx+tosLpYOHzbLGmeizA0Dez+910BeGu9AEXXNKoX1B9LXJgBYprnZDP6ezXoCw5WXd/KGR5koc8PAvkNSImnuNZBOEUfasz+9bQKARY4eTW8QkMy9ChIJMyKRiTI3DBw/IYVxy4CsLKmlPYSGAcAOnZ3h3UgoU9cbyNww4PvhtOvInCoAAKREmKu/h3VoSbXMDQPpPj3Qy0uaFQkBACkRi5mlgsOQ7tMT6ZK5YWDiOPMx3RGyp8csQAQASIkxY8waA+nkeWZxo4KC9LabLpkbBiommisJ2jvT12bSl+RIlSm4BwIAQNLJSwrTOWTf2SnF42Y1wkyUuWFgUqlUUmiu+0+X9g4pL4eRAQBIoeJic6lfexrnare2SoWFjAyce6JR6SuXmZn96YqPB49I5083N0UCAKRESYm5o2C6bi3s+yYMnHeeFMnQo2aGvqxP/cslUlGBuWFRqnX3mJNKV12e2rtmAIDlHMccmJPJ9Fzq19xsRgWmTUt9W2HJ7DAwbZK0YK7UeDj1EwnrD5j2Lp+X2nYAAJoyxdyxcN++1LaTTEqHDkmzZ5sRiUyV2WHAcaQ1q6VJ4819ClLlWKvkRqTb/rtUkIZbaAGA5WIxacECM2zf0pK6dhobpbIy6UtfSl0bo0FmhwFJmjxB+vf/ZobxU3G64ESXtP+QdHWVtOiikd8+AOBzVVZK8+ebA3ZX18hvv6XFbPeyy8xpgkyW+WFAMgfqVUukg01S8wheXXCiS9qxV7rsQum2a5krAABpdvHF0pw50q5dIxsIWlrM6YGFC6UZM0Zuu6NVNOwOpIXrSndcZ07+/O4t6XinVFZ6dgfvY63S/k9MEPj2bWaiIgAgrXJypKVLzecffiiVl5/dWgC+b0JAW5t0+eXSpZdm7hUEp7IjDEjmrhZ3XS9NGCv915+kj3ZJUydJ8ZzhbacnIe1pNHcnXL1E+vr/kIoJAgAQlnhcuvJKEwLef9/c1bCiwlxhPhydndLevWYdg2XLpLlz7QgCkk1hQDKVcf0Kaf750jO/kt7/2NxLYPxYqaRg4P9135faj5vTDD2euWrgtmulxfM5NQAAo0BOjrR4sQkBmzdLu3ebP/mlpWaBooH+VCeT5pRAU5M5BJx/vpmYOG5cevsfNrvCQK/ZU6WH7pW2/kN6bbNU+6FUd8Qc9LOipoIcmaDQ9ekC2PEcac4MafkiqWqeVJgf5isAAHyOykpp4kTzDr+uznxsbDR/3rOzT95oKJEwaxQ4jpSfL110kTRzpjnNkKk3IxqMnWFAMqcNLp9n/u07JO1skPYekHbuk9o6zH0GcrPNKEBlmbnfwMwp9owZAcA5KjvbHNhnzJCOHDGLBjU3m3f/PT3mz3h2thk1KCoyNz7K9KsFhmJvGDjV5AnmHwAgYziOGe63bcj/TPA2FwAAyxEGAACwHGEAAADLEQYAALAcYQAAAMsRBgAAsBxhAAAAyxEGAACwHGEAAADLEQYAALAcYQAAAMsRBgAAsBxhAAAAyxEGAACwHGEAAADLEQYAALAcYQAAAMsRBgAAsBxhAAAAy0XD7oDneZKXNB8xIM/z5HnJvs/lsL8GYvYVdRUEdRUcdRUcdRVcX12FLNQw4Hmeamvfk5JNkiO5EQYqBuIlk6rd9g/zRfRVuW5uuB0axair4Kir4Kir4Kir4Exd1UqSqqur5bpuKP0YBdXshN2Bc9Ao+G8b9air4aOuhkZdDR91dS5wfN/3h3pSa2urioqK1NLSosLCwhHtQHd3t+R3y3WH7Ib1zFBSVG6UlD0Uz/Ooq4Coq+Coq+Coq+B6TxPEYrER33bQ43focwbMix/5HZCJ3ND/t84dZqiNugqCugqOugqOugourFMDp2L8BgAAyxEGAACwHGEAAADLEQYAALAcYQAAAMsRBgAAsBxhAAAAywW6ErR3XaLW1taUdgYAAIyc3uP2UOsLBgoDbW1tkqSKioqz7BYAAEi3trY2FRUVDfh4oOWIk8mkGhsbVVBQIMdhbW4AAM4Fvu+rra1N5eXligxyc61AYQAAAGQuJhACAGA5wgAAAJYjDAAAYDnCAAAAliMMAABgOcIAAACWIwwAAGC5/w/VP82ipvHQAwAAAABJRU5ErkJggg==",
      "text/plain": [
       "<Figure size 640x480 with 1 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "# Define the grid world dimensions n x m\n",
    "grid_n = 6\n",
    "grid_m = 3\n",
    "\n",
    "# Initialize the robots\n",
    "r1 = Robot(\"A\", (0, 0), (5, 2))\n",
    "r2 = Robot(\"B\", (0, 2), (5, 0))\n",
    "robots = [r1, r2]\n",
    "\n",
    "plot_grid_world(grid_n, grid_m, robots)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2bc27790",
   "metadata": {},
   "source": [
    "### Define dynamics contracts for each robot per timestep"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ec5c6a4e",
   "metadata": {},
   "source": [
    "We will break up the execution into individual timesteps as our planning horizon to reduce the complexity of the planning problem. This horizon length can be increased depending on the problem to be solved, but for the purpose of this case study we will do our planning in increments of single time steps.\n",
    "\n",
    "The figure below will give an overview of the process per timestep, on the right we will see the resulting traces of the robots when following a strategy found using Pacti.\n",
    "\n",
    "![Overview Figure](https://github.com/pacti-org/media/blob/main/case_studies/multiagent_coordination/multiagent_overview.png?raw=true)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "73d7a2f9",
   "metadata": {},
   "source": [
    "This figure shows how we will use the contracts for each time step to place constraints on the movement of the robots. The contracts that we will take into account are $\\mathcal{C}_{\\text{dyn}}$, which describes the dynamics of each robot,  $\\mathcal{C}_{\\text{collision}}$, which will ensure that no two robots will occupy the same grid cell, and  $\\mathcal{C}_{\\text{swapping}}$, which ensure that two robots cannot swap positions (they would collide during the transition). For each time step we will repeat this process and update the positions of the robots according to the chosen move. Applying this strategy will result in a trajectory as shown on the right side of the figure."
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "id": "3d3a1093",
   "metadata": {},
   "source": [
    "Now we define the contracts for the robots' dynamics, the input variables are the current position of each robot in $x$ and $y$ coordinates and the current timestep $t=i$. The output variables are the next position of the robots $(x_{i+1},y_{i+1})$ and the next timestep $i+1$. \n",
    "\n",
    "In the assumptions we define the initial positions and time step as the current position of the robot and the current timestep:\n",
    "\n",
    "$$\n",
    "\\begin{align*}\n",
    "t_i &= t \\\\\n",
    "x_i &= x \\\\\n",
    "y_i &= y\n",
    "\\end{align*}\n",
    "$$\n",
    "\n",
    "The guarantees of the contract are defining the dynamics and ensure that the time step increases by 1.\n",
    "\n",
    "$$\n",
    "t_{i+1} - t_i = 1\n",
    "$$\n",
    "\n",
    "The dynamics allow any single cell vertical or horizontal transitions to an adjacent cell on the grid (but not diagonal) and are specified as\n",
    "\n",
    "$$\n",
    "|x_i - x_{i+1}| + |y_i - y_{i+1}| \\leq 1.\n",
    "$$\n",
    "\n",
    "We will break this constraint up into four separate constraints:\n",
    "\n",
    "$$\n",
    "\\begin{align*}\n",
    "& x_{i+1} - x_i + y_{i+1} - y_i \\leq 1 \\\\\n",
    "& x_{i+1} - x_i - y_{i+1} + y_i \\leq 1 \\\\\n",
    "& -x_{i+1} + x_i + y_{i+1} - y_i \\leq 1 \\\\\n",
    "& -x_{i+1} + x_i - y_{i+1} + y_i \\leq 1\n",
    "\\end{align*}\n",
    "$$\n",
    "\n",
    "We also ensure that the robot has to remain within the grid, specified as:\n",
    "\n",
    "$$\n",
    "\\begin{align*}\n",
    "&x_{i+1} < grid_n \\\\\n",
    "&y_{i+1} < grid_m\n",
    "\\end{align*}\n",
    "$$\n",
    "\n",
    "Note that we need one dynamics contract for each robot, as the contract can only describe the dynamics for the robot whose behavior it describes. We are extending the input and output variables to include the variables for the other robots and the other contracts that we will use later, but each robot's dynamics contract only specifies the guarantees for its respecive robot's coordinates for the next timestep. In the code the subscript $0$ corresponds to timestep $i$ and the subscript $1$ corresponds to timestep $i+1$.\n",
    "\n",
    "This contract implementing the constraints explained above is defined in the following function:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "8c4afdae",
   "metadata": {},
   "outputs": [],
   "source": [
    "def get_dynamics_contract_robot(name: str, init_pos: Coord, timestep: int) -> PolyhedralIoContract:  # noqa: WPS210\n",
    "    \"\"\"\n",
    "    Function to set up the contract encoding the dynamics for a single robot for the next timestep.\n",
    "\n",
    "    Args:\n",
    "        name: name of the robot\n",
    "        init_pos: current coordinates of the robot\n",
    "        timestep: current timestep\n",
    "\n",
    "    Returns:\n",
    "        Resulting contract compound that encodes the dynamics for the robot.\n",
    "    \"\"\"\n",
    "    x_str_0 = 'x_{0}_0'.format(name)\n",
    "    y_str_0 = 'y_{0}_0'.format(name)\n",
    "    x_str_1 = 'x_{0}_1'.format(name)\n",
    "    y_str_1 = 'y_{0}_1'.format(name)\n",
    "    t_0 = 't_0'\n",
    "    t_1 = 't_1'\n",
    "\n",
    "    contract = PolyhedralIoContract.from_strings(\n",
    "        input_vars=[x_str_0, y_str_0, t_0],\n",
    "        output_vars=[x_str_1, y_str_1, t_1],\n",
    "        assumptions=[\n",
    "                \"{0} = {1}\".format(x_str_0, init_pos.x),\n",
    "                \"{0} = {1}\".format(y_str_0, init_pos.y),\n",
    "                \"{0} = {1}\".format(t_0, timestep),\n",
    "        ],\n",
    "        guarantees=[\n",
    "                \"{0} - {1} = 1\".format(t_1, t_0),\n",
    "                \"{0} - {1} + {2} - {3} <= 1\".format(x_str_1, x_str_0, y_str_1, y_str_0),\n",
    "                \"{0} - {1} - {2} + {3} <= 1\".format(x_str_1, x_str_0, y_str_1, y_str_0),\n",
    "                \"-{0} + {1} + {2} - {3} <= 1\".format(x_str_1, x_str_0, y_str_1, y_str_0),\n",
    "                \"-{0} + {1} - {2} + {3} <= 1\".format(x_str_1, x_str_0, y_str_1, y_str_0),\n",
    "                \"{0} <= {1}\".format(x_str_1, grid_n - 1),\n",
    "                \"{0} <= {1}\".format(y_str_1, grid_m - 1),\n",
    "                \"-{0} <= 0\".format(x_str_1),\n",
    "                \"-{0} <= 0\".format(y_str_1),\n",
    "        ],\n",
    "    )\n",
    "    return contract"
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "id": "8d532a64",
   "metadata": {},
   "source": [
    "### Collision Conflict Contract\n",
    "Next we describe the contracts that will ensure that our robots do not collide. For this we will place constraints on the distance between a pair of robots, and ensure that is will always be larger or equal to one cell - meaning two robots will never share the same cell (i.e. collide).\n",
    "\n",
    "To describe the this requirement in linear inequalities, we need to break up the collision requirement into four inequalities. Each inequality will place constraints on both robots for a specific configuration with regards to each other (for example robot A is to the top right of robot B). \n",
    "\n",
    "As the guarantees of these contracts are mutually exclusive (robots can only be in one configuration at a time - Robot A cannot be to the right and to the left of robot B at the same time), we need to consider each of these collision quadrants separately in our analysis. To achieve this, we are using a `PolyhedralIoContractCompound` which allows for disjoint guarantees (and disjoint assumptions if desired).\n",
    "\n",
    "The linear inequalities ensuring no collision for two robots $A$ and $B$ are defined as follows.\n",
    "\n",
    "We assume that the two robots do not collide:\n",
    "\n",
    "$$\n",
    "\\text{distance}(A,B) \\geq 1\n",
    "$$\n",
    "\n",
    "The guarantees are that at least one of these inequalities is satisfied:\n",
    "\n",
    "$$\n",
    "\\begin{align*}\n",
    "&x^A_1 - x^B_1 + y^A_1 - y^B_1 \\leq -1 \\\\\n",
    "&x^A_1 - x^B_1 - y^A_1 + y^B_1 \\leq -1 \\\\\n",
    "&x^A_1 + x^B_1 + y^A_1 - y^B_1 \\leq -1 \\\\\n",
    "&x^A_1 + x^B_1 - y^A_1 + y^B_1 \\leq -1\n",
    "\\end{align*}\n",
    "$$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "67252004",
   "metadata": {},
   "outputs": [],
   "source": [
    "def collision_contract(robot_1: Robot, robot_2: Robot) -> PolyhedralIoContractCompound:\n",
    "    \"\"\"\n",
    "    Function to ensure no collisions between two robots.\n",
    "\n",
    "    Returns:\n",
    "        Resulting contract compound that ensures no collisions.\n",
    "    \"\"\"\n",
    "    outputvars = [\n",
    "        \"x_\" + str(robot_1.name) + \"_1\",\n",
    "        \"y_\" + str(robot_1.name) + \"_1\",\n",
    "        \"x_\" + str(robot_2.name) + \"_1\",\n",
    "        \"y_\" + str(robot_2.name) + \"_1\",\n",
    "    ]\n",
    "\n",
    "    contract = PolyhedralIoContractCompound.from_strings(\n",
    "        input_vars=[\"current_distance\"],\n",
    "        output_vars= outputvars,\n",
    "        assumptions=[[\"-current_distance <= -1\"]],\n",
    "        guarantees=[\n",
    "            [\"x_\"+robot_1.name+ \"_1 - x_\" +robot_2.name+ \"_1 + y_\" +robot_1.name+ \"_1 - y_\" +robot_2.name+ \"_1 >= 1\"],\n",
    "            [\"-x_\"+robot_1.name+ \"_1 + x_\" +robot_2.name+ \"_1 - y_\" +robot_1.name+ \"_1 + y_\" +robot_2.name+ \"_1 >= 1\"],\n",
    "            [\"x_\"+robot_1.name+ \"_1 - x_\" +robot_2.name+ \"_1 - y_\" +robot_1.name+ \"_1 + y_\" +robot_2.name+ \"_1 >= 1\"],\n",
    "            [\"-x_\"+robot_1.name+ \"_1 + x_\" +robot_2.name+ \"_1 + y_\" +robot_1.name+ \"_1 - y_\" +robot_2.name+ \"_1 >= 1\"],\n",
    "            \n",
    "        ],\n",
    "    )\n",
    "    return contract"
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "id": "f2313ece",
   "metadata": {},
   "source": [
    "### Swapping Contract\n",
    "Next we define the contract that determines that the robots will also stay collision free during their transition to another cell, meaning that two robots cannot swap places in the grid, as they would collide while traversing the same edge in opposite directions. We do this by defining another contract with a disjoint guarantee sets.\n",
    "What we want to enforce is that the two robots cannot swap positions, given as:\n",
    "$$\n",
    "\\begin{align*}\n",
    "\\vert x_{i}^{A}-x_{i+1}^{B}\\vert+\\vert y_{i}^{A}-y_{i+1}^{B}\\vert \\neq 0 \\quad \\text{ or }\\quad \\vert x_{i}^{B}-x_{i+1}^{A}\\vert +\\vert y_{i}^{B}-y_{i+1}^{A}\\vert \\neq 0.\n",
    "\\end{align*}\n",
    "$$\n",
    "We encode this constraint in the following four constraints:\n",
    "$$\n",
    "\\begin{align*}\n",
    "&(x_{i}^{A}-x_{i+1}^{B})+(y_{i}^{A}-y_{i+1}^{B}) \\geq 1\\\\\n",
    "&(x_{i}^{A}-x_{i+1}^{B})+(y_{i}^{A}-y_{i+1}^{B}) \\geq -1\\\\\n",
    "&(x_{i}^{B}-x_{i+1}^{A})+(y_{i}^{B}-y_{i+1}^{A}) \\geq 1\\\\\n",
    "&(x_{i}^{B}-x_{i+1}^{A})+(y_{i}^{B}-y_{i+1}^{A}) \\geq -1\n",
    "\\end{align*}\n",
    "$$\n",
    " \n",
    "Where we need at least one of these inequalities to be satisfied. This contract does not state a specific assumption on the agent's positions."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "6eacd3c9",
   "metadata": {},
   "outputs": [],
   "source": [
    "def swapping_contract(robot_1: Robot, robot_2: Robot) -> PolyhedralIoContractCompound:\n",
    "    \"\"\"\n",
    "    Contract ensuring no swapping for a pair of robots.\n",
    "\n",
    "    Args:\n",
    "        robot_1: Name of robot 1.\n",
    "        robot_2: Name of robot 2.\n",
    "\n",
    "    Returns:\n",
    "        The compound contract that ensures no collision.\n",
    "    \"\"\"\n",
    "    inputvars = [\n",
    "        \"x_\" + str(robot_1.name) + \"_0\",\n",
    "        \"y_\" + str(robot_1.name) + \"_0\",\n",
    "        \"x_\" + str(robot_2.name) + \"_0\",\n",
    "        \"y_\" + str(robot_2.name) + \"_0\",\n",
    "    ]\n",
    "    outputvars = [\n",
    "        \"x_\" + str(robot_1.name) + \"_1\",\n",
    "        \"y_\" + str(robot_1.name) + \"_1\",\n",
    "        \"x_\" + str(robot_2.name) + \"_1\",\n",
    "        \"y_\" + str(robot_2.name) + \"_1\",\n",
    "    ]\n",
    "\n",
    "    contract = PolyhedralIoContractCompound.from_strings(\n",
    "        input_vars=inputvars,\n",
    "        output_vars=outputvars,\n",
    "        assumptions=[[]],\n",
    "        guarantees=[\n",
    "            [\"x_\"+robot_1.name+ \"_1 - x_\" +robot_2.name+ \"_0 + y_\" +robot_1.name+ \"_1 - y_\" +robot_2.name+ \"_0 >= 1\"],\n",
    "            [\"x_\"+robot_1.name+ \"_1 - x_\" +robot_2.name+ \"_0 + y_\" +robot_1.name+ \"_1 - y_\" +robot_2.name+ \"_0 <= -1\"],\n",
    "            [\"x_\"+robot_2.name+ \"_1 - x_\" +robot_1.name+ \"_0 + y_\" +robot_2.name+ \"_1 - y_\" +robot_1.name+ \"_0 >= 1\"],\n",
    "            [\"x_\"+robot_2.name+ \"_1 - x_\" +robot_1.name+ \"_0 + y_\" +robot_2.name+ \"_1 - y_\" +robot_1.name+ \"_0 <= -1\"],\n",
    "            ]\n",
    "        )\n",
    "    return contract"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bef50d2d",
   "metadata": {},
   "source": [
    "Now we use Pacti to create the contracts from the functions and display them to confirm we set them up as desired."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "9fc1936c",
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Dynamics Contract Robot A:\n",
      " InVars: [x_A_0, y_A_0, t_0]\n",
      "OutVars:[x_A_1, y_A_1, t_1]\n",
      "A: [\n",
      "  x_A_0 = -0\n",
      "  y_A_0 = -0\n",
      "  t_0 = -0\n",
      "]\n",
      "G: [\n",
      "  -t_0 + t_1 = 1\n",
      "  -x_A_0 + x_A_1 - y_A_0 + y_A_1 <= 1\n",
      "  -x_A_1 <= 0\n",
      "  -y_A_1 <= 0\n",
      "] \n",
      "\n",
      "Dynamics Contract Robot B:\n",
      " InVars: [x_B_0, y_B_0, t_0]\n",
      "OutVars:[x_B_1, y_B_1, t_1]\n",
      "A: [\n",
      "  x_B_0 = -0\n",
      "  y_B_0 = 2\n",
      "  t_0 = -0\n",
      "]\n",
      "G: [\n",
      "  -t_0 + t_1 = 1\n",
      "  -x_B_0 + x_B_1 + y_B_0 - y_B_1 <= 1\n",
      "  y_B_1 <= 2\n",
      "  -x_B_1 <= 0\n",
      "] \n",
      "\n",
      "Collision Contract:\n",
      " InVars: [current_distance]\n",
      "OutVars:[x_A_1, y_A_1, x_B_1, y_B_1]\n",
      "A: [\n",
      "  -current_distance <= -1\n",
      "]\n",
      "G: [\n",
      "  -x_A_1 + x_B_1 - y_A_1 + y_B_1 <= -1\n",
      "]\n",
      "or \n",
      "[\n",
      "  x_A_1 - x_B_1 + y_A_1 - y_B_1 <= -1\n",
      "]\n",
      "or \n",
      "[\n",
      "  -x_A_1 + x_B_1 + y_A_1 - y_B_1 <= -1\n",
      "]\n",
      "or \n",
      "[\n",
      "  x_A_1 - x_B_1 - y_A_1 + y_B_1 <= -1\n",
      "] \n",
      "\n",
      "Swapping Contract:\n",
      " InVars: [x_A_0, y_A_0, x_B_0, y_B_0]\n",
      "OutVars:[x_A_1, y_A_1, x_B_1, y_B_1]\n",
      "A: [\n",
      "  \n",
      "]\n",
      "G: [\n",
      "  -x_A_1 + x_B_0 - y_A_1 + y_B_0 <= -1\n",
      "]\n",
      "or \n",
      "[\n",
      "  x_A_1 - x_B_0 + y_A_1 - y_B_0 <= -1\n",
      "]\n",
      "or \n",
      "[\n",
      "  x_A_0 - x_B_1 + y_A_0 - y_B_1 <= -1\n",
      "]\n",
      "or \n",
      "[\n",
      "  -x_A_0 + x_B_1 - y_A_0 + y_B_1 <= -1\n",
      "]\n"
     ]
    }
   ],
   "source": [
    "c_dyn_a = get_dynamics_contract_robot(r1.name, r1.pos, 0)\n",
    "c_dyn_b = get_dynamics_contract_robot(r2.name, r2.pos, 0)\n",
    "c_collision = collision_contract(r1, r2)\n",
    "c_swapping = swapping_contract(r1, r2)\n",
    "\n",
    "print(\"Dynamics Contract Robot A:\\n {0} \\n\".format(c_dyn_a))\n",
    "print(\"Dynamics Contract Robot B:\\n {0} \\n\".format(c_dyn_b))\n",
    "print(\"Collision Contract:\\n {0} \\n\".format(c_collision))\n",
    "print(\"Swapping Contract:\\n {0}\".format(c_swapping))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fa5b6aaa",
   "metadata": {},
   "source": [
    "### Merging the dynamics contracts\n",
    "We are ready to start merging the contracts. We start by merging the dynamics contracts for each of the robots. This contract now holds all the information for possible steps that both robots can take, but it does not ensure no collisions yet. Now let's take a look at the contract describing the dynamics for both robots."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "93dbefec",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "InVars: [x_A_0, y_A_0, t_0, x_B_0, y_B_0]\n",
      "OutVars:[x_A_1, y_A_1, t_1, x_B_1, y_B_1]\n",
      "A: [\n",
      "  x_A_0 = -0\n",
      "  y_A_0 = -0\n",
      "  t_0 = -0\n",
      "  x_B_0 = -0\n",
      "  y_B_0 = 2\n",
      "]\n",
      "G: [\n",
      "  -t_0 + t_1 = 1\n",
      "  -x_A_0 + x_A_1 - y_A_0 + y_A_1 <= 1\n",
      "  -x_A_1 <= 0\n",
      "  -y_A_1 <= 0\n",
      "  -x_B_0 + x_B_1 + y_B_0 - y_B_1 <= 1\n",
      "  y_B_1 <= 2\n",
      "  -x_B_1 <= 0\n",
      "]\n"
     ]
    }
   ],
   "source": [
    "c_combined_dynamics = c_dyn_a.merge(c_dyn_b)\n",
    "print(c_combined_dynamics)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e2667a0f",
   "metadata": {},
   "source": [
    "Next we can use the dynamics contract to find a possible next move for the robots that minimizes an objective. Our objective is minimizing the distance to the goal for the two robots A and B:\n",
    "$$\n",
    "\\vert x_{i+1}^{A}-x_{\\text{goal}}^{A}\\vert +\\vert y_{i+1}^{A}-y_{\\text{goal}}^{A}\\vert + \\vert x_{i+1}^{B}-x_{\\text{goal}}^{B}\\vert +\\vert y_{i+1}^{B}-y_{\\text{goal}}^{B}\\vert\n",
    "$$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "8f293135-a64a-4586-b60d-dac2d853ac1a",
   "metadata": {},
   "outputs": [],
   "source": [
    "# set objective (cumulative distance to the goal)\n",
    "def objective_expr(robots: List[Robot]) -> str:\n",
    "    '''\n",
    "    Function returning a string describing the cumulative euclidian distance for the robots to their goals.\n",
    "    Args:\n",
    "        robots: List of robots.\n",
    "\n",
    "    Returns:\n",
    "        The string that describes the objective.\n",
    "    '''\n",
    "    expr = ''\n",
    "    for robot in robots:\n",
    "        sgn_x = np.sign((robot.goal.x - robot.pos.x))\n",
    "        sgn_y = np.sign((robot.goal.y - robot.pos.y))\n",
    "\n",
    "        if sgn_x < 0:\n",
    "            expr += \"(-\"+ str(robot.goal.x) + \" + x_\"+ str(robot.name) + \"_1) + \"\n",
    "        elif sgn_x > 0:\n",
    "            expr += \"(\"+ str(robot.goal.x) + \" - x_\"+ str(robot.name) + \"_1) + \"\n",
    "        else:\n",
    "            expr += \"(-\"+ str(robot.goal.x) + \" + x_\"+ str(robot.name) + \"_1) + \"\n",
    "            expr += \"(\"+ str(robot.goal.x) + \" - x_\"+ str(robot.name) + \"_1) + \"\n",
    "\n",
    "        if sgn_y < 0:\n",
    "            expr += \"( y_\"+ str(robot.name) + \"_1 -\"+ str(robot.goal.y) + \") + \"\n",
    "        if sgn_y > 0:\n",
    "            expr += \"(\"+ str(robot.goal.y) + \" - y_\"+ str(robot.name) + \"_1) + \"\n",
    "        else:\n",
    "            expr += \"( y_\"+ str(robot.name) + \"_1 -\"+ str(robot.goal.y) + \") + \"\n",
    "            expr += \"(\"+ str(robot.goal.y) + \" - y_\"+ str(robot.name) + \"_1) + \"\n",
    "\n",
    "    expr = expr[:-2]\n",
    "\n",
    "    return expr"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5d12fecb-1681-4b18-88ba-900934c7b94c",
   "metadata": {},
   "source": [
    "We can now use the objective and the dynamics contract to find the next best move to take."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "46cc0397-b301-49f6-b093-93740f90b782",
   "metadata": {},
   "outputs": [],
   "source": [
    "fun_val, var_dict = optimize_contract(contract=c_combined_dynamics, expr=objective_expr(robots), maximize=False)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c3f5c00b-7404-442b-8471-7000e37b5686",
   "metadata": {},
   "source": [
    "We need to extend the result of the optimization in the form of a 'variable dictionary' with the current distance between the robots to be able to evaluate the other contracts for this proposed solution."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "9c69d4c6-75be-40a9-b449-66f86c175bd1",
   "metadata": {},
   "outputs": [],
   "source": [
    "vars = {}\n",
    "for key in var_dict.keys():\n",
    "    vars.update({key.name: var_dict[key]})\n",
    "    \n",
    "robotcombis = combinations(robots, 2)\n",
    "cur_dist = np.inf\n",
    "for combi in list(robotcombis):\n",
    "    distance_btw_robots = np.abs(combi[0].pos.x - combi[1].pos.x) + np.abs(combi[0].pos.y - combi[1].pos.y)\n",
    "    cur_dist = min(cur_dist, distance_btw_robots)\n",
    "\n",
    "var_dict.update({Var(\"current_distance\"): cur_dist})"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "558d1d60-3282-44a7-aff5-05fa15961ae5",
   "metadata": {},
   "source": [
    "We can now use this dictionary to check whether the move satisfies the swapping and the collision contract. If it does we can apply it to the robots, otherwise we will take a random move."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "ecd00c9b-de48-4479-b6f0-1738a00114fc",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "The robots can take the optimal move [(1.0, -0.0), (1.0, 2.0)]\n"
     ]
    }
   ],
   "source": [
    "move_ok = True\n",
    "if not c_swapping.g.contains_behavior(var_dict):\n",
    "    move_ok = False\n",
    "if not c_collision.a.contains_behavior(var_dict) or not c_collision.g.contains_behavior(var_dict):\n",
    "    move_ok = False\n",
    "\n",
    "if move_ok:\n",
    "    move = [(var_dict[Var(\"x_\"+robot.name+\"_1\")], var_dict[Var(\"y_\"+robot.name+\"_1\")]) for robot in robots]\n",
    "    print('The robots can take the optimal move {}'.format(move))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d9af8f40",
   "metadata": {},
   "source": [
    "We also introduce another move type, a random move, where the robots have to satisfy all their contracts, but do not need to reduce their cumulative distance to the goal.\n",
    "To do this we find the possible next positions and choose a random element, then we check whether it satisfies all contracts. If not we remove that move from the possible options and try a different move."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "4b710a44",
   "metadata": {},
   "outputs": [],
   "source": [
    "if not move_ok:\n",
    "    move = find_random_move(grid_n, grid_m, robots, t_0, multiagent_contract, [collision_contract], [swapping_contract])\n",
    "    print('The robots will take a random move {}'.format(move))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9bdac913",
   "metadata": {},
   "source": [
    "Now we can put everything together and run the simulation of our two robots navigating the grid together.\n",
    "\n",
    "Note: If you do not have `ffmpeg` install, you will need to install it to create the animation (https://www.ffmpeg.org)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "cfcb8c47",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "The robots will take a random move [(0, 1), (1, 3)]\n",
      "The robots can take the optimal move [(-0.0, 2.0), (2.0, 3.0)]\n",
      "The robots can take the optimal move [(-0.0, 3.0), (3.0, 3.0)]\n",
      "The robots can take the optimal move [(1.0, 3.0), (4.0, 3.0)]\n",
      "The robots can take the optimal move [(2.0, 3.0), (4.0, 2.0)]\n",
      "The robots can take the optimal move [(3.0, 3.0), (4.0, 1.0)]\n",
      "The robots can take the optimal move [(3.0, 3.0), (4.0, 1.0)]\n",
      "The robots can take the optimal move [(4.0, 3.0), (4.0, 1.0)]\n",
      "The robots can take the optimal move [(4.0, 3.0), (4.0, 1.0)]\n",
      "Rendering 8 frames...\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "<video width=\"640\" height=\"480\" controls autoplay loop>\n",
       "  <source type=\"video/mp4\" src=\"data:video/mp4;base64,AAAAIGZ0eXBNNFYgAAACAE00ViBpc29taXNvMmF2YzEAAAAIZnJlZQAAN4RtZGF0AAACrgYF//+q\n",
       "3EXpvebZSLeWLNgg2SPu73gyNjQgLSBjb3JlIDE2NCByMzA5NSBiYWVlNDAwIC0gSC4yNjQvTVBF\n",
       "Ry00IEFWQyBjb2RlYyAtIENvcHlsZWZ0IDIwMDMtMjAyMiAtIGh0dHA6Ly93d3cudmlkZW9sYW4u\n",
       "b3JnL3gyNjQuaHRtbCAtIG9wdGlvbnM6IGNhYmFjPTEgcmVmPTMgZGVibG9jaz0xOjA6MCBhbmFs\n",
       "eXNlPTB4MzoweDExMyBtZT1oZXggc3VibWU9NyBwc3k9MSBwc3lfcmQ9MS4wMDowLjAwIG1peGVk\n",
       "X3JlZj0xIG1lX3JhbmdlPTE2IGNocm9tYV9tZT0xIHRyZWxsaXM9MSA4eDhkY3Q9MSBjcW09MCBk\n",
       "ZWFkem9uZT0yMSwxMSBmYXN0X3Bza2lwPTEgY2hyb21hX3FwX29mZnNldD0tMiB0aHJlYWRzPTEy\n",
       "IGxvb2thaGVhZF90aHJlYWRzPTIgc2xpY2VkX3RocmVhZHM9MCBucj0wIGRlY2ltYXRlPTEgaW50\n",
       "ZXJsYWNlZD0wIGJsdXJheV9jb21wYXQ9MCBjb25zdHJhaW5lZF9pbnRyYT0wIGJmcmFtZXM9MyBi\n",
       "X3B5cmFtaWQ9MiBiX2FkYXB0PTEgYl9iaWFzPTAgZGlyZWN0PTEgd2VpZ2h0Yj0xIG9wZW5fZ29w\n",
       "PTAgd2VpZ2h0cD0yIGtleWludD0yNTAga2V5aW50X21pbj0xIHNjZW5lY3V0PTQwIGludHJhX3Jl\n",
       "ZnJlc2g9MCByY19sb29rYWhlYWQ9NDAgcmM9Y3JmIG1idHJlZT0xIGNyZj0yMy4wIHFjb21wPTAu\n",
       "NjAgcXBtaW49MCBxcG1heD02OSBxcHN0ZXA9NCBpcF9yYXRpbz0xLjQwIGFxPTE6MS4wMACAAAAP\n",
       "32WIhAAX//731LfMsu1Tb7YLqPeiniZfQ3UlAZuWxO06gAAAAwAAAwAAHrwXOAJfiQrzrwAAAwDK\n",
       "gBeoSf8KY4+IA3IlyY2Pz8lWsaCSfUerAIsiYhIrAiduhs4F6f6wTX6ivvniNZxlCmDHq3WVYCIa\n",
       "+QQMxbN/jBMEcRlgOJjEM9xWbZc99ZopYFi84u7gJ5dFPSpYv6/4Upwk+r6jjkqwNLpj4bqhjpZT\n",
       "6KwiU5vSQ7dH45z9dULcAlLCdMnSVwLmsGDBkuCV7fztHqZADgPolz0bpoDXWW195PsbUsLHgOCg\n",
       "gnmF8RTDYDwFnPeibLMbnhxyE/xXSMYV04AEFOdK7DqLhIeoFTlLbHAYgplNWGYMjRwCzEpicPB+\n",
       "fakU+EhaJo7wwKSPXjRvhBO9FmnHroRDK/HaADQrh+h5nyF54+qJYW8/mQm7PMM3dKBx0Zp2Oack\n",
       "/Dq6XP4uyAE9j2aVowwcquZFQbi45AxPZCm9OWp7ThJ3q/S3TTpTKZbmXye1+YyMQ5q9DrNTK5Rc\n",
       "Xqey6bYLTQFP4WfedcUeDGOLYrCAVPJc+7cxRp0L204F5S7/KCCKdrNpZiihf+XCrsWqGAYAa+aY\n",
       "/GhiZPrcsPp45eYr6xTo90hbLp0wqzaAdPs9E1v6E1ElB+V8Eb4mufVUXiGy9uRhuzM3F1j3+fck\n",
       "djwdmYsnEyZwbwHU/q7MbdB+MdQikdApM0y+PQigKHxpRlumUi+pN9/0EqN1E2fvs8WT8RSuiQ0S\n",
       "Vf/e91dRP/BWsuJrZAQ92VfDq31oWPy6UV/FOdAFjpIvcd1h7VDOXunbw/++r5IXtKS6Qxt+Rafr\n",
       "KbS8boXiZ/ZjOGPikCBIoBV1j9UMQnN8OW0g3EV23WzToxCUcZTXVBqTaQNuTDlLaYFQ/gxOl++9\n",
       "5W6J6j99tTDUb/GuzhnI7ENDM28hTrs01P6IWYgKfAq/WX+Oq8FNuJlUMlCrIozGf2wEnJzCm8AH\n",
       "4loKLX+5gsmDHu5sTjGAyF+C9854CRX10Dg5A/BqTi//zOQbI5DTvgzvgJy3UGGBI8pY1OPqYBku\n",
       "x9kkVyFFRna6R5NrjghHjpTDV5AfazpMXrsU5810HWGipU8moxrPozPAz1ujaFzJcC33bkpWSCsF\n",
       "WQ3WMSFdwS+G/iFHP80ffFLd6mBki8Ylj43dfVSe/pqQ4EU71tsrNbvKPc0jF+bZYy/a6p/+bkpN\n",
       "DkH63gVGQHZnCxK2wqAA2yBkNaThaC7d/hYSP6iI7CTXRcZKtKen9kRjyW0Xql5QjUjFLVe53jHl\n",
       "YBYR8sitWBJsTgdru2mtJpUubwUGRZdWBKxkjs8J+vtXDh+XvGhhcffzj0te9kMzGrYTOfdXbQ9E\n",
       "aM8GygSoDgKozWhRK5BC4iMOohkNFrWQf1ORlTsBPFZuLhEvstq43YJNDEI0SV6OmDn/XYwGnjEB\n",
       "YAvL3v0QqB8278bioiXgfs3h6VrLD53IrFHb+a8tqA4bjtJGbmvyx5988xgYfn5F4OLR83VcrM9H\n",
       "vZJR52aFO7XCMydiSo0PD93ZI+77Lku3RAUvMDwFIyeWDytiIH23TZPPUw5KIB9Vz8b3odflIz2B\n",
       "omj2OTtmOB7PziZrDC6WknvUuIAVyK7Ck1+4V7uMrtSh8Sk+GUi8KAZCUznfQDcMj8hhdqFRsNop\n",
       "RdTr/vJPhJmdsNtZFGzevn1hRyVS3kzv7Gqq1/9dheZq3zcQ4qkl66prVLmKZjPKN7SkfbrNgFK5\n",
       "kCB4hn9j/l8m/3MBaZIx7M+WNKW23wGDY+tMfkZgGbqrEhACFw1JDKMqBOqInaRxi5pe5t+FnL95\n",
       "VIROIJ55hHw1hGzjL25VCQvrqZ9eYYCFt+VKHhCAQKNcJyf+5mFRjZZzNbspa+ETSuEvGtNvb1bj\n",
       "Tjx4FugmOh/BbGi4ycIh0RPdD6ZR6RJlWfDNGTpg4i6AHE0sVhuSq5Zbercs3s5oVIceBd5B26QT\n",
       "zVZzUPBz9KnIrCx/0x3Pk2q3BQwEiJa0s1gDAjsiajc4ENIcD4iGT0IOOAUSbi4F6h2bIVvDPuXU\n",
       "DcBfm3TIxwp2fRrl29xQua4VkwMZdQSKWHsp/2V8yiMPCRHV3qbd4qETd6+kmJo/lFAhPoAN4KVS\n",
       "HLJU8WLeBp3Cc/HlQO3rRc6fhemp5IsLv2ZNF9/qp8WPmZqnVO0KPjyP+AVcbGTqi3TgEp24pfHS\n",
       "Zpl4sCLSraiHpPrhgACNfHcYURC565pNlGkEwduACFW9Fex+pDTgNk3efOtxX/62D7upvR+mCHFI\n",
       "sb9kEDg78ftBw3Gf5BrLoISGgAQ9YMuXcdOVd8Fc3xfQxF4njmve8qiQjCrmZ4nyEH/cs5KOOvR1\n",
       "KmNof3UP0g8KG1L7B1OitABcsUEwtxdAqKhB7ZRNDhMRVo4/uxFlVgLRiRh4VDP2HAzkIsB5lh6o\n",
       "w79dq79PPQDPU6Oxg6rTKcLMU6TGKletuybn75w2Kq33JaSUcqzz5v0lB95qfG8yYLH40dSm4W9P\n",
       "VhDc1tYqlEv1xFAWUf2RXma9cXsyHkq7bZo5Y+Gy2Wv7pfNuDlKh4G7EpGGvA0rWM1RqYneWiq2u\n",
       "zLaI0MJ6AkT5l1bEAMkPaB+RruO124KAV3DtXT0HUq5py8Hm4HM12QO4uWu4LpZUt7670IZ0KgmD\n",
       "3aYoGtc/aZYGKjXcVw0hJJHS6oSXr/gIwNsr9EU4QkCEj9kaU+JRPlpbzxXsP7/XUYgl64Zenxw0\n",
       "59UUJrAI8Ghna1g99JHEELmojI8dGixtpc9sbaFSnUYn07QIIi6dSdFjKDMANwNP+XZuuuxJA6AD\n",
       "J1hoM8+kFNWUcp1wK95HDOEQICe+YDnSyWp7E6iGxl78iTI3cYJwnqgv19eaT25BPhcX1rB8vg5m\n",
       "X0hKOTeh0pfRoeRZ/8QddKN/x1BC5uKf8fojveV44ZeSUfrELJdCaAPiS7esmP2S2rA+UGxfilWG\n",
       "efnvsRx7tykWVwr/hRJYt3X2yxsPHUHUTFEr2V3QxF7UY75O9kNK1PjlkIcsUqBxbJYnIDr20jGb\n",
       "5n4Rc49zRHkGznSUrENMH/bs7ghITpOJEsbmGN1dtAjGQReBfJQjTFL6+2u9he9HynxYuGutdCnF\n",
       "xnP4/vRoWrJMJd9JyaGTMrEcrbkskRZb7beC4n65Kw/6uLq/HwraxaMCSmjsYjErTxWkwAE7NnMS\n",
       "N7YMLWqw5Qwx06rh3SL/dB2TIJJMmEl5HKGaVgewN1jdn27YF2RLUQzZOOwrFgxMC6nKOQTg1583\n",
       "CHbmgae9mAAHmq3Y3qZqxjuSHqvZhnq36c0ijI27uIKXJodg7bLl/PzNbPVyDXtPls/llMgX1WV6\n",
       "at5CjVcrfuQaaTibYDQeBlWO4gMZeWBtdi6n0dfbff/FPv9HsoinkJgNKp3VshXnuBDH5Jd/IVs8\n",
       "Myx+PO6quv+K4wR8KwmOyhf/eC+WbO0aYU0w7PuY5PEkYexgzYlgq9dgUbbeA1zX5Tg78BJOg+aj\n",
       "IIfp66w8T76g7pT1cH5rdz7v9fSCi4tCTFhudXuFBes8qt64K8MzHpRZwwnnz0wANBnPT0pg1+RO\n",
       "7T/iG8YsZDeMJRVLdAolO4hyss9UvOtqFq+FWAVrHghHy/fXswvYkIzWEszOP/NLUgXaAUi8rYY1\n",
       "MV2B6w/JOHPAgvveyPfUZ/0V6FRCEdRmS8VZfoTvqwqMmgpOQPpIqvTGGebI3icLIYfCiBxl4PX1\n",
       "c4F8j6Zsw5VKJ9VvChUjbNwHPdKyRYC5fQOtrTm2T6mQ/4gMg9Pd80TAgFkcFiU4qMSOIqGPDcbJ\n",
       "nNwCnXmg48n8AXbJ49lhdnT32pIp0qDzYgtHVj7FypnMzV7rLYwGgNSILoSxkzDiSQ3LnHTP0s82\n",
       "59a4rwyfY0o8EKQQF2nfpENOWe/BCGJzgnLGRCPBDehOrvq2S4GNg2KUTlNNyoZsqackTR7uFceI\n",
       "4vtROyLWLM9wzQioB/U9Xj4Gu5qbqZ4u0aRnAygOGLwVJAGyADQ+1T5uhneoS2Ld5/JJ7cBuhKIu\n",
       "MB9viKH/3M9OleGLxKtCm5+bY4tiBC6BiAGvKamqBtgBs05pnawQ1Qjlqt5IxiTqh+E2pl+5YgRG\n",
       "60WPojQ1fYwcVMglu6QFK0N5CjU/lolFHsPsd2Vx2Jf14OfbBJWBL95/+Q4n/L1HbHFzcfPX+Ca7\n",
       "ZhWrfB7sOyGFftVfAsNX5894P+BcoF9/3p4NEvQPtZsncIwDYlm2TQMPc8vkAXMFgxGTwnMMP6Xk\n",
       "Tmk+688v5Zo3UAVjnhfraUhC/6nEoK4Cw0GbC4aFZKsFOvp/mWK6r1PDu7ByTXEH/uow522De1n/\n",
       "IKJumV89C9At5WGbultE6QPBmMixDW8GkubfB0POOqI0TZaTNOXGVRQB8mNpvk+4b5Sa2jTI1w1J\n",
       "jUt0ngIZAeXTuI70ddvvKg2DFuv4zjh3IOeiKyEhcvWuxB3KZR7+XQ74tb4YJKCFpigReBj2qZtg\n",
       "TwFwcFtEV3vh81Xo/HxCCl5FxWV5FzMnxDYG0Stg9AtVxW1GODrMhpRSakD6/n2Vl6vK6oSr2xV3\n",
       "4UZvQ9SoGTnetqrLmS8IaVIVONYwt9oRcmWmJ3V237I8UYo5BxJ288Fqi7GYZhBhxZQ3C3zB5OYj\n",
       "v9OOTf8FzFTTYYAauyx4nlSGR30hK8MGaItzGel0KK0p8dO9iYNYaXvouqK7AOJLRhOjEsXjajIZ\n",
       "ZG7hNPF0eaDZjCrHR4kUsBz4QABZbSAP1Cm9C+h4UDb6Gn14py/aVkEfv0/9Bg//tZJeE/ZTYGzd\n",
       "hGEDYL0mFauCf76Hj/Llm3D5NdmvEDo5NyaoAg9r+fW2zw3j1UCxz0PwQFKkCBVvLWIbr6bNx6or\n",
       "XWURqD33Mn9wqLcZ5olx0YrP+4XN7Pk7d1PH4AXSS1Ltdf1JhJMKqF+powfU56RleQwrFdKVg3sK\n",
       "RcieeN9PTZ39OtcII9yC3/fJIYJ9o17GGKRfCpck+EYGBGVYB0sq3tmfac5CADjRUSxOfq1ocJb1\n",
       "JnWhVS2lrU9lpnbAq+NmFizgbO9i/QsYOBnY37KBr/ttiuvMji9r9vl3waFoRT1RBTv49lLj5yc/\n",
       "fnCBcRnCfdluUAyXNNpednqMm9L2+eGyhtVlGJiupiK3d+R8IZGDBASsTOW5UkW7ZL2LNCjEW8yU\n",
       "q4HmHNbP1Xzdccl7f59tKUxfQ6DAA57/+6bTQt8yKJweTqsU/WGGnozRW+xcYChQrTozrmXO9q7N\n",
       "LOZ87PvLbdMQ7Nz0qU7eqYDlZIbShYLvQ157yIPtC4lVt2pXaEOMubebH1tS47fmqJzXpvmA3VBm\n",
       "1Ye9D3ypD1MxqT1WK7zaDi5V6lvylCKpLZPhRYXHgLgko20IP4sSXg28uk1A56udEuMzTtslINuw\n",
       "AYErgSYg1wkhDD0AAAMAA2MAAAM+QZohbEF//tqmWACUO0poAQMNWKCOOdjE7HabFvej5RLia2F9\n",
       "uD32cSrjylcmNBT5230fsFqYqmqhc7AnclMXqaeJ5JseGmSdJHoEZbSj6adNsLFFL81hBMR5mc30\n",
       "VAiqjnLDLU9g6MMWQPvVSSgyh5RA9Q/8bAyjRDj4dqeOeIXIQPP1fCnitEDH//93+oGd0GmRYjdI\n",
       "UAw5paOGDtz+nQSsigSlv19Y3xsGFy7Vr7YUVR6AYiMlLkJb92gNBKBgKHCWu5qXdla8I1jRPj+n\n",
       "BaNcNZ5NdlyrqqP/TGEZaZLvSbK56rR0EFh3G5t640Z+yGzMDKzKE8shYh3Hs52Lp2xfaYsH4htx\n",
       "jQfBOR7bqzKljhEpQIB5VNu0OzwgxJ4gLITLcRA0wRyy+OMCOmWxmrGSffk/rt31nEiWYRzsMvx4\n",
       "/B8C6EB42KeKw3aBaM2e9dMDiw2K1Cxm0ksOx5Kz/pDDeoCQ6q6mz3VllA+/ASe0mNCu18rSLYKh\n",
       "sfz2K7hkSMFAlG/jXkEpsWHfzmgzTrfPWsPJZqlHKTq7+DlwB9a3c9nLkefhYe04ZI1i1f4a6gYg\n",
       "+bv24bwDTlqLmgBSmrWBhUE5fw6kG7c0YD/U/jcmeUGEwA5/Y89wGvEfdYhkvipLA1EucjCQY2iu\n",
       "x0vOowth0/xbCtgqtmCDd1zMCuE8ZcanG/Lcw3PtwijfK/IjWlbERZvBg655b+4uoEB9wHbLkide\n",
       "orohn91/dIFVcrWpP4YFTynzaGfvEuDV3nls9I8QyrkeW/3GIYeCKHJ8/06asjZGpEBm45iGtIrn\n",
       "SRAnSmudjSTzs5kB1NBQADSJfjNVojNIO53GFz5uv/L8pf/0dImcMQwJYfpAh94LoZY+FWtDsKiK\n",
       "pi69DU9B+Q5D5Wtsc6MCjPZKzRaUOYxnrbd/sRE+kYx+gZNbga66SEMFAcgdhR0At81GEc/kJPaY\n",
       "MOAU3ZHMAxTYxwHICltipwMqOBuKSHCWvjj7Ovl7Tv3FH+TzqTTc6RQiK9LkTHyKfuDsrHR1s710\n",
       "nRUg+I6pvCpAGpewi//xPomilnF2UqhIrb2CSpheqV7/OcnJcd2KgqaioJ5kIHN2BTi0UyoAAAbE\n",
       "QZpCPCGTKYQX//7aplgAlDzCgAG1Nc48JcmJcg+GgVvmFsL6Krbutrh1QCivNwvI6ON1ZLahv0hs\n",
       "wO9mtF4ONgExWi3msaAULtAZ75Racvu0NGw+dPGvcBtUZoVoYc3D8S26tD8xCwHjewATD30zAf5x\n",
       "M/nbb5FMfc44Q6LfgH36YrHW2gPg08kb/4oHjrfawPcEaE1m9dsLgCqQ7hIJuufQJi0WDip5XgRw\n",
       "XVI3Iuws4m+b7iXVbYOCv1D59h477TUq6ouzT4i9o9bIdPPaOMFvxYHQ8OA8czFx3qhTnNpoO0t3\n",
       "PbDPUBfRt9t+HX/jKLtoPEMwhLSKtecX/xbljizvhhHMhSB/6WxNGTdHafbqIZUtZhoHE3lqwQhO\n",
       "DODIHn4O5a0n6YvhB05vW83qH9PEP441MLoe3hyo92QQa3Qq9rqtNsZmttDSnPMMmFUOH7yHf48e\n",
       "/V3sNgjBfd0v/FlVzhvG+/kGDn/v/hqd9Ui7z6lHlladNYXAUyMXmNsL8804HjdVAk3ViTGbG5tB\n",
       "eCH+5wvfeVTWij2vDgA5KwxlTqfZDgBLYl7mIfEBEgZPrI1y+ijYmEk0AatSPnoXX1K2D7IWGFnY\n",
       "FJPFjE/J5rYSkb/sp+3TgSnRs7qcULQEXdcrPZPsN/8lvRShOjUKPTNdQjf7GOAcl64aK5bpVBH9\n",
       "U5W/WUME9O8Gt+rF1q+H8g2Yb2376KtwhJYOrO+QtGwVXUzxgCICSMt0/98oifS6qFnl9Hbegk1v\n",
       "mM3RQ2USh5aQ08v8u/4HkvKzGYYpwJF+eb5fV+cRSzpz/aIaE2Mb01JOEeA/JYzNkWbfKT3zsGfr\n",
       "mM3LFix7zsRGv3VD9NoMbUv6fXWEd5tJXzPkFFRLtgsLSrN++648wkCXgvKOGsBRdyf5EWguvCxi\n",
       "kWwuxq56b0DiVqxnewn3Jz3+Hm66OFTYo3tmSXGL5mf+drxNjic3TJUgg+l3LV+cpk4YoFaLzWy8\n",
       "473Dwx6PMV2P98C2Lz1cvN2wRCKDZCPkh4QHx1tL4c5yBrnKwi3Wlr3uEJq8W1hNtTJSf2VkMK8w\n",
       "J3YxVoafA9sQD4WzpM1s2ivy3jaPlqn6eBn1cwE2ypJhyVuqpMau6vvUal0hnziLltt15ZxmoNEY\n",
       "vyrf8YZ1nMial0Ae4T9LCM5Nl/ePSsTo78lXwl3ehei/XO3gPknguY9v51UG1hm/9jLScIsi5NnQ\n",
       "7Fpu2fEb+hhFREyaFL7htjMiWELVSOY0ZKFfKtcz+usvhTYHDbXNIrioR3IvXJv1tQQ0dwVxq2o8\n",
       "fLTtasFbvH+fZwhRrEND+ZN21GEDADAccUDdOaK+JpHzb5XB2u71uMzObV5KN/0C8ipejMafARrf\n",
       "RoY0NI/nWKowRnEPRZhdkSygNEEwmm/t6yF+k0hkEu9yZWMzfIh6SLJJkWw96rdncX7PEnDqOI92\n",
       "L28LwW06oAfURY/fRS4dWm9ER5hKk3Zdm6HcRD/84eJ4axalAX7n98I3y8Io5gkDVUMy5GkOOk4x\n",
       "q6Qs/4w43YV5hJLYjhuBm0xq+RFOe7SB/p4S0dNPqkPbHDVRvzvXA7BRYF8ILuT2AEw8xleqSw3X\n",
       "zekQStBGh40jy4NeRp4H1WuNO6aqEGIKZQ//MQ/i/mhvpS/r+QicW5Zg1ThM68EIec+9UjAnvKZA\n",
       "vIMkSi3cyLsY+mWZu0nbEgLG8tpkbyTAnd0yIqLm/PfzeL67Hj/Dw1Zyl0kIFl5BDTfk3k21vYjW\n",
       "7oCC3ReI8E/oB/pJX94HJN8BtI+ZSTRfczAcbkLL2UWp3HhQgknUfROYsInWNiYngsbU7t66nzs2\n",
       "B6iTN82Q6C6D8ranNKLjsuNM/aCaLAiEBlGbOQzH4O/SUWD8x3KhHYacaG+mUBKdNQDRXdWL6WcJ\n",
       "pqfEZapk2MvN89db7K7TkBdNB4H7iERXAH4tPWTygJRAr35ITypR2Ah2iURgH4f2bcb7Ah8nmOz8\n",
       "T+MtNf7m29b619sK4Ug3HhuHPzAPD3FlZ+KquKx/AZgWIQme5j18M5E9q4jySi1Q8oC0i2ZbQ9ui\n",
       "/7tYXO0wNZZrNgksVKwc4quuCyhibi5jb0O7SGtL0szhcFl4c4tPm2YYFLYEWcKVZYihCC5M7Meg\n",
       "zQqVqpxOuIL/mGSphDDpNjmFsndMSh9VqKQgey0JUSTNTCuyXDnHuzAfBQrXuok30WwHPJvS/tCp\n",
       "WLrA3cfkDqo0i8jEr1aVuZj+8HIhmpQL3Z0srd23/NWUuqUKFXUyCA+83ED1fUw/GA+BvAEPefWB\n",
       "hCDPt156wfQ+TqOTe6y+wpGTmr+i6wAABglBmmNJ4Q8mUwIL//7aplgAhDzCgAEor2DkqNPWsyJT\n",
       "dhGmVwopTef44q0Xvpp0Dr2KGok/6FOvohtExdDFLqDPEjMQDh172ECBsiCs+D1NvtVHXgNugMNG\n",
       "o8XDiOzbL9lIUNvdLubtBX6iBL9VHggcUJGhQR7z34ysIQBxcxp8SLDqNFPc/E4En/pvH6yYWy64\n",
       "fblh5UWZPi4fVmBRC6Qj95pgzQiZPu04B8dz8Hv3Bc8kAXEtfDyzkIF8hBCr2UrNeFcukplrQW4u\n",
       "RItY6oj8zwSiZUDnSTmBgm77qdTZ1w3idaYpSAo3qnHXgbBwPCGnsrPSFlV0FyFvAU5eYSeixfcT\n",
       "asNowCfufYeX7t/GWTYmiFmWN6+fW26YrIuFcf0r8P0yNr7WWJWGEiH52DNmQ2e9z3dnLKZv9CaL\n",
       "cmGgvyY/5bzElas1wR44a6K73MogPPSwxL88GOzqxTjf39Pe82dohNJl5PFctk0gIGzINW/MAPiH\n",
       "eCiyOZyR2LMwmQ9i85K8l/Cs8uiImjnZ6iZEXRPh36+k+FRlyiAX6ujpDrDJlPbaTr/ZwUcbEUiS\n",
       "emrXmGLtTIvPgsIhWT7sTOKOBT6azkBQOOv4yzmnAx2cPLq7Xb0AImLLOccmBzcn/16OmSeAFvi1\n",
       "LzlIu9H1G9nodqrj95+LmeAk2QCLZG3sFLAG4x+NE1WY28tXGNgGpdhp8vRc/2yfJQiMGTneBlGS\n",
       "xjblmAxdO092xebV4P6WIlfD+NGCJyEHh2+8sHvaJ4rGi/IGl3dNGlqz3Wrdvi8TZ8TSliEoKUWM\n",
       "Jr1vTNY50I+E/2d82MEG4jJUqtPKlDMDfk/N0gmy2+oInwKTyS7meZCW48d5CP2u2jOphez3qlSm\n",
       "ojOI1O0DrnlsqtzjYy2LZasT/y+z3kQr1jEY1GG7F6PsPK3Cc1bOAp1ht4a2pbkbGf4LNksUz3m3\n",
       "6fnTVhRQ6Ikhw7rfjX1sRaXqtmv9D6BIBNw88DRVr1EaPKlnRQOVJqzf3QLwNdFyvujEJMEV9nz0\n",
       "Kg0N7fL4cNw0msbwqdWQmWtJ+8vBmZkk0mG7v5B3pgimztkMvBlm9rL2KUeZqsL2YnhuJzVgJuKW\n",
       "UgSkBJL9mvtrPghkh5Zzj5yw3/MNNpRaSSwwaVYBijj8Kzs+1psI5O9+8pE7MAF8/0QwasV8Tbx3\n",
       "3Fv1yg5Zqlf4sovNynLyjAoQ9+5mQHFTETf1Y5AaVFHETSbKOKOvflaHuwUEFpccZBGV615qlDNL\n",
       "V8rJqNU7OiASq+DycN7+p0m2JXTG+vFeMuqswfxPLSnEaD6tFJB8pdyR89HJLMe/iBDdVwzUdLvL\n",
       "xZaqZoyqGdRe/ztJi+ceVWyB92d3lAAI1G8ioIMohLxibkescNcI3D5oOo/5zeXqlO7pj4geqzw3\n",
       "+3ZHb0eLnrjQroZS5zRutiddG7nBVFYm0ERxjGu0h/Gk+oU4TQnbfX1Pa5umIdmcN+zlzN/L7wNc\n",
       "x+NQRI99G3igy4rNXbMs7mnsKep3xt4pNNWFQVGge6HJxDViTl6Qrn7yLeBI34FewmDyjrbTQG+c\n",
       "/HUgGONwx/AfsbtK8vEAmiWWkCvfueJ1CLgOFkpl5FAco+LtfF20slOoO/XEQL1L8g88oa4927sm\n",
       "U/lmhHeSCREXwbeewFBM2FdvpfXmLirEVJpPf3UbfZjrVwSHGPLeqg8oTLSXx4E2A5TpyfZjxSoo\n",
       "ddasHjpjLqgQjBUDzQgScr0XWJ0NgVeuqCC5/ePXtI92ZX/nd6coFS2W/oVlRSBFCvfqCAk4OW0j\n",
       "KhntHU5MBv7aTB3cZPSOoropmJG1Q3uVi7NIO3BjPpuYpIW1UScsSRC/QkdcX5wg69oGZPuk0Hx6\n",
       "dSNcn9k7/HKBdMuZZyAsPgyBLOb1n7pH9tPETVo/23Oyl8yiSW8LhhygTNCwC/DbyxmXDcdCqiLN\n",
       "gDl4HiwDDdFtB7hjXt1cBSe+2Avk30MfyahNexngwDGvgU9PYKEjjx8aWUUo7LhU3b8POv15G2CI\n",
       "0iilXugSnBN6R0POxUbzvx6yeYlKu03hpRnF9IQGGpwAAAeoQZqFSeEPJlMFETwV//7WpVAAlDwE\n",
       "oAIgVT1tVNZZVRd05dqCyJdSyZsZfuz+w9GKgx62A7f8yPU0/K8+eqH+Wu7eHnfEgiHZH1RyYyW6\n",
       "sGNocsBizy00Us0YPzh/to0/o1nIMPjES1eOM5J6AwCv5wiz6K7UBL9CdQQusOEW1I4LCBb2QgbB\n",
       "j+IoM8BTBt+1M2zGfcLRdCF70TfBa554HN5lYKPB82XUiCdutdAz2lo+DRzI8ymkNRB3mwJFkl0y\n",
       "UU3pkdout0aakF7Fg6Nh308Nth6Mkkha5IYd6KrViVcWKzyMElo+BIPwdUPpPlNKWFQWSQtHj0qn\n",
       "UedksHG4NLCyyt8cs44IE0qCPBvfxHvnVjxhslEZczp+iVumTQ0uR72scxb/G7Gp9rzNPptzxXG2\n",
       "zPEa5j3QAcoTabtuCV9TaPDiTZPagIeguvrAzXkd++LsfnDqK65lRBtqQWDS3nkycSmJxgI8TTo1\n",
       "RlEsbzuAtTo1H/hAXzea+tBuUtFztrPuUznhgij3c6L9whScgKLXTBMq6scp7yfg6oA8UT4fFyCz\n",
       "jVv+P/+Py1mfLtsnvqpmeyPUF7q7cP8hOjCWpE3QnBp51D5/5dyOlpGhSBV6pACUsA1Bd+L8dKRz\n",
       "u/wfXDeKJuoZPt6wcOT14jPpB6/xk1e1WNvUSqTRBhLvblcuZHCCub/vdqAppbmfMC6bIpkbltg3\n",
       "iShI6SMfJHCcW4C0GNMr2fitAbh3fJy+h+BCk6NUY/7/PQgrAoXJ1JqauD+5lJC8Hzfik649uKwe\n",
       "GcFFKlEDhYn7Qno9dzPXJBux4vvgqHJa45dOSqJiTusEbwPr7xJLwFZAAjmoycLBvMDawHosldod\n",
       "IC6j47m59xK5Ai+EfWWHWC7B0uE5WjnUHtPV3SD88USkbnRpdiC+V23C2oEvQocYS/lJrVJaT1yV\n",
       "ECRbtmuUV18lu60xEslEHsnXPFszWAE+cKeEUxCWVc1h4vQDS4J+NDji5W3uIJTafwTkcr72IYm0\n",
       "reo8xwKD/kwj7C+vYvT3f3uxHHUhmOpd51ytBhPOG0uXQudLs3pqiFB4gpzfQ9i4QdgZ+AsHWz+G\n",
       "6bqNOVKQsH5V8KrG+RjtuGqi+WOse8purriyoMKGvPOULMa6oEDilyp3gBKhso8TBKa911nUaL/6\n",
       "FNaT83GXBEwrZ2+zuQ+QLBw56+nZK/EewGmamc5jAJCzngFLzI5BS7nHHZDxqIbCqf+UMfByNDdK\n",
       "UoLEqri0afRdxQ9QLChqvFIhSBoNGKGP5NJK1F+GsSSAVJrRPJQD1PJqYplMApsSUe18Z83D8eLm\n",
       "OVmlH0YLN7GjDw4fWOUfC0NArtKqrhF/rsEx9cXbajEQQ27dfwq+mQ8Dh+FprMbKzL1K4szS8G54\n",
       "GqBjW4AsjLbqP+mpSySUkAjhItQHbb+D2R/eZcGWvPxOguNR7IbUHGRI7W+Ca8PGtCdWUvhGMR/V\n",
       "sn+8c/xegVJaSTYSnxL4CgAF1rP614NadXSLUCtP7lPhK9VAYX+xs49nPdKg1p/w03c/7QEIq7s4\n",
       "NUH0TsY05B8lfWCyOtT+YPSUDz6d3/Ly5rusKu6hGK18rRhRjvucjz/6uiKcvIMwUr6cydhHxri/\n",
       "HcgLVL+jdDQvv/8tUl58yTy7fKv7Dy4qG8CGL2uFsN9PkXgL33Dv+/p7LnadqxlkEU5Z22NEacWI\n",
       "4KTfsKMwDyVBE9jRWTaS4PLGidEbGcm8m4gNI8tuf0dpPAAoq2ngUjbVAFczcZinoBOFkE8H43ZB\n",
       "tkAssB2NJR9CI7NmPbxFBKkLu1vXRR/0AOSJ3n3+eF6BWJjEyYz2eM1lwNB46CEeJE7KfEKL9VE7\n",
       "KB4yCtfE2dosJFzFCM9HD+IgSG2RAQi25xtzJ6iWJJNteMwEPKfkbz/Lm0c71fq3MV7Q+vXi+AIl\n",
       "yiLZre/rxZ2Ak6lUloVF5Q6BaoxxvfpzyepJiOfO8uD+NrrqJ6idi8Tjy1V9KHMuhaF51Hw8CU7l\n",
       "giwdxVk1IxTtYAbMmF57rx5XYAPegy0817Bp0rGejKbpkWimldVwAzHNjU4LoHERcNkX+FFynoBX\n",
       "DtDdyQMsf8hX5U8y7dR07KJIxfh0g3qcBD37Sdl+N6DWGazL3fOeWX4GlgmNskXd+5nbw+5lnfWa\n",
       "21sF7jEcueoo7nTP77r8CNUXkZEbrFcf2p6JpavC8T2GL5SMXxp9g0pwL9EPcgZARDo9ZOf9ELT8\n",
       "UOheSD8dLnAAFABNQoQr/Al425IsPI8KtrkumubByuCAADxz+4afvey/cUGI5DECNhhb6oNXvjeB\n",
       "w+gqlWmk7y9ELExjofRx9NZ3K0s7chThvB2yAJeDlxJin7cqPIT0z72uqVyCMNkW/0AJgnNERLn6\n",
       "ORdlxLP1Bnr79BHUGwE5tJs3zEqssASIfcWZRxRWQppNvd/XKeK8C9gyn9gASCPHEfUqyKLIeCen\n",
       "SzcCfGsohD5YFBDkEVCxO3FjlKTlvfqSty1dO3LA6cC7RlxnzwOfW5TaoFvRhyuh/tCr9k1IyiIT\n",
       "D0L5TmAZRmF8w7XgwBt/CE0KuWekP+9mk5sgaWqm2Fq/yP9H50dPoR6hxMDRekUuSxsWTShWqeEE\n",
       "XQAAA+ABnqRqQV8AAGQpxLgrupBFY+7swKxQTbJIBV20EhE79Pq/dv7kYkhOwTZ2J3XiqhPV1MJD\n",
       "/5OCMfIyADZY9E6lOODvm/1s5YocYcNbaWQfTOVMZpnan/UyupIdoSuw5MzsphfP/hLVMMibuiqw\n",
       "/Cebhpb4TlFw16ZNun0oQ1fwk05ZOA/JX2q3fVErN5bmSfzb+MG/oO4w6rbVvBmF5EVJtcu+uWI6\n",
       "mJct4Jb4icD5R21hFBwgM6MPT110hH3gvE6cV2qwMFK3wpt97JYBWb6oxQu+UcZQGvUMAtc9eFzg\n",
       "drFI1axj5l26yUsSSvo+h2EtlGsxcHll5hxXvbxDm4LWGo7442zdd6RMuI0tYDHgIN2I+Ou8/Fpw\n",
       "s+LT+QuFzWm2WewV8CcL396OkpgXXTOYqKoWbUin5XvrTgylPAILhn8RMpgEt1aQ5V5DoCH3Noe6\n",
       "JaC468M8zBlkyuqwPnajnDq3A7KlZ5paIN2RN9NAudC74oDlFNTx774YjvBmWf4k9Nz4MOzgS1AY\n",
       "uhwCHauB4s8BrtUjS7YaUOcmVOT8yMhmD9WwY0oMQNpDyLlOcq8wBT+i6z2FsKvsUg3kzWhwrM+z\n",
       "omef5yMKuM9UIdRPYB/yPegCi1CUlO5jMWLqTWL9BOTyGHI9Tl96EEeFmwj8cgZmNqu8Hmpztj72\n",
       "ZG7lojz/2mUXXZ7jXgh+ThLMChK8J5HcFjiaVRgXOXSLwu8FZuBdQoH7RUVXMdX7npHTQxDZIMo1\n",
       "bRhnlcP1PbWQ2CwW1jkLR4baMHLyU+N9nDDPhdhHbxpLKI4vP+y6jJyNtcmLfyH+BrLQAjBHvMxN\n",
       "VM9dCA9+Os2g9I/jVak02mKlp2HWeRqIf6BD7D+HDTD0e30ARBXC67eqiWQ4dVCSh7ihA58z53//\n",
       "qz3yR19SOh34yrMnkj0crjZYIaH8xM7uE7xKQ52YgnJhSOKLt3HnbzLs9DX8FO7x1mtotBZVfXOJ\n",
       "CxaAE/SrMFlgC+0ud1EOeViSLHMhTUwpv//tstyRACdZoeTOFfFjOVjHIkJpKbp0BXJSPNyoVGWb\n",
       "jRrdZ8RmzYqTeoc1KNEojDLXDLhXxJebPzBhFAvQVE0dgME96gmZbqptNGu+5tRJkUJrytD2D5Q+\n",
       "jZHFwlNpPiy9Ys6vjto/O6HTmEWY6EAhbkthv0g5TXnFhrKMhsaKyoGnBZ3VQ6PawAAaMU3sQgaX\n",
       "ZGxIWAmP+TJW8sd7vKoDqUGNziXd9ZY03JFsKgmxaS5CzbpVdJmdOZOis+yBt8BhMttu1ERX+97+\n",
       "vZnSMVNLQj6AOP30biKgli45kAhcT9TbiIiGzQAABUJBmqZJ4Q8mUwILf/7WpVAAai38phBXV4J7\n",
       "/hER8AAdYqFmPdHaM/QO7qQQKa2kSJmHJYK/RmCXDyEC7pJoyUtwyUmadF9OF/Spdn6IRP/n8gag\n",
       "X8BoerOGJuRn0AOH0IBAYDpZPfNL/Cst5/BjSVtpCcr/6MH1FrmtaAwB28kYkALWUeaBvT526ONr\n",
       "ANmuDBQAM+b48/IU4RA+OaK4684rW2W5mAZHVb86gPY9/sMiMu7mc23zqIUSsElec19zTwwfX3m4\n",
       "LA+8bhZA29kAkZ67bOJbNxE0SCdUeyuYZkeDW+Ji8/jUVGrrwvlC23dI+aO66bY4S36VRhsj0pMc\n",
       "TsYcgCzyUbU3wZnZcNm2oN/+veqtC1NfO3DhmXDjFbswyiZ/wFsRuGN23fY6JMUaQ2DljlFeb/3i\n",
       "64ADBs3eAoGyTgAIFgKjuWvFb8CuOeyBj5Q64//TI58W0I1bHlI4uEUHCKx2TE4AcYBBKikv8lhO\n",
       "Fs4+FpgYvsqmicURif9KLxO9Ij+W5KGlsVKP0E+40oENqsGhXl+nZ7TSgVuZi6WZkwjkE0KnpSO1\n",
       "G1KgQf2KmCuE+N/xSrk+1zMgfTU2UP5qQ/ODbByV5s6+x+/2lo8Em36PfTEuFkp5gTJ0wEj7Zxl8\n",
       "WVCJdEdr8kVJqdcuTG5AlAD4wrxuXXKVyxG5hMCKdCPxwa6LoCmrBxMwXZKGQqUu3P0lzXtktH87\n",
       "sgrPJsjOpdxbgc4spPBbmePfIIIj8IUz8QmhXpaI2vBaPWYwiBRpo1TgPnMH8MVTvBIiLsMbbNtS\n",
       "tMqXtOsmGSSiKmEYo7RUGASmtBG+PYAtrehjZoObUhxJqzajPAC6kJiTXaYxeNx51MW3r2QdygmA\n",
       "AIHNIVx5r+IMvZC4xddsgCuKXc+I5f3fJCt39DFdXNSIqKGwX6ytQ9OZ7uRyD+yziQ8zYDMAPq7W\n",
       "bzXwxBXbZsA6Olr91ELrL3tDLkU4IvZ2jj/iUlAygvN6NDyf7j4u2GvN8tQkM2hQDxbcnJ9rToXh\n",
       "JHKoSepQSBhDLR1ke2miCFGItGooqS7z8B5oAawqXXH7j65uoUaXIYllFfJPh+FYF4b1Kn4dk1uh\n",
       "RKYhvQXWq1/W6RyeofUCRq8HBOnTNgA9FJY4GlOwKBtG8MoTzbxFvWe25b8ZoujSBfRM6r/Kn00O\n",
       "Oo7BHHaUm3pz4PsFiOKdJrlbY+A6iaV69m78cxhi2ZlLJ4shZAktpOmrb+GakRM+0gczYevySgEQ\n",
       "PNZqmQ3QPptFzckACnTYuKVdIcS283ixrNiFyGwrB9MnkATikSdwNQbHyNPX73JrVkeRY5RUA/jv\n",
       "eYwwgE8Q+A94POyMC4H50gvD8oyufnvBQgNdT7/IC14W0gFZOGSxg9V9keBn1cmwoa6f5+V+tRUs\n",
       "VU/y6WOcec7zmqbiQ+6/FfHa0FRkl/x9E7pSB/JlTtv9Dk3SirDnjSqrulw/+JDyd3Pb9cQqeQdx\n",
       "eoK7wEJHfOhVehnz3+PfGF/cEj3cc66WWb8tM44NP1/5V24V/qRqkEKxOjRY+jn/SZ1IgSojHOPS\n",
       "7HonRLjpPrFXT4MsLonenp9EAXzSC3SbKkLsipCk3PLnaKHzqE9M+iLPQL51+BQ2zW+ac0hAZir/\n",
       "bMirRrTUlMrwewKK/gKIV8gHazAfvML9QOkoKcBXoEkBP8qFyNMZZXL0fUgVswnC9VHtcABgUlM7\n",
       "yHzShFHn5WNQFucVyqu1gPJxr0UwU5FLy5UTq4M8FjFG3JHNebAWPt1h4hGHwR7jLfQMj6AYrxBb\n",
       "I27hVoOricIT/wAAA/ZBmsdJ4Q8mUwIK//7WpVAAlDwEoAEOSu12aQurYpvmKfGAlAsjn4lPNI/g\n",
       "taGhwu8AiUEwijm1YjahPkaRA9+nU4jbDp/td3O/48S/wvjrOZs4LbPae3nXbha7M0YxpCid9OQc\n",
       "sF+nX0TTa1RRhPlnx7t6v3J31VDlzAcBEAtE0ohrHTXblVwM/pNxyrQR1nP9I2Qjn1ucKx/ckiX4\n",
       "Uej+Bp5V2iL8Bf4FcJQOYQZSCqE1stIZpRDGx8HGbTYVk8WAQbEyeJQ9Dc2duhi7jXuNMix/fE1D\n",
       "Y2eNBVTB0MAl8jYsxk7ZdB+VyxuDEFN53hDZLkkH2nzNkJlujKM0w2RJoPIezR5X7En2WCb7610q\n",
       "frQMRRJf1bHRYTT6wPI7pbQfGD5f+B2zg+jLVgKN5iNBzD3zBYL1v55AvemIDlnnANGxq0JC+nUl\n",
       "Is4UXtWBkqmflra8CPqeW52EXqPjiGLrewUkLfzypFcEimvJJc3fQIwYHqC1RB7daE/A++qc0jVu\n",
       "NiJFxDFqY/Z/SBQE4x7gMP8nBFMo9h0Kubk0ybXh148DI4FF+6pJj6rKrAXOrsuYwRrNlWA79m9O\n",
       "ReS351hL8wOjooX7DTrwZh2pS2h8mxiuMkYNGUxTADXDr38gyL4bjt5izQBiu9ShAUWwq4JymQOc\n",
       "k7Gxqyu8qkk+xRZRwBeaBLtY/KtQ1Dkdrj5Zt9qIn/J/ytddd/cXdlFgIvuHwCR+zt6IEyY5wQ2l\n",
       "o1WBVkclOQYJG2XszdvHHbVoqqixy3aHmeNE9BTVCI4Npt6kxa5l/da83pgG75U/aUO4JwriGbYA\n",
       "UBUB4So0iqdK5T61IpI6Qnto8nZv4P30yB1O9DcgVAdkxqQvZ8gT2mQjDxKNhiTZZa8V15+I+vwD\n",
       "xoNVeoyNY6z499jtnCO5p8Otz8Yt+XwZMbRzt7vIdvijYVwEXcgkWy2NxSV2owzSQ+y0xTix/KA3\n",
       "YMox1ffWuCwA24Amt0fPgjrSIJM31NptE2R6tsQMhY8rBbk/dVjSWiGNDU0CqrLbMV/ov5wA66/B\n",
       "egmpIHPD1lT21p+eXO+c9fMS1r/Pj1Jl6gJBmxU1pf4h48px1NrgSg7XMyH0rFMsC2kf+ZZGv5/s\n",
       "42NNQevTn1aXqh834S1XOK4hrwSdVG6cRTXMjCla/I57evcJvuw2NLEagT6tJrp34ebGWOOlXM+H\n",
       "ihcSpw8PlaJAxP+rMTF+N7KUHv0ZV3joyHXf5tN9toygoeQdUm1nIwxG/cT55JhiJ7tcIy+tbNdT\n",
       "AKwO/YgP0JFNRsCC4TDmnhoYahFYN2JqD3PjhSw6R8u+vwgTirhQHS214sN29MOTHbeWLl1V8PSq\n",
       "HHEAAANxbW9vdgAAAGxtdmhkAAAAAAAAAAAAAAAAAAAD6AAAH0AAAQAAAQAAAAAAAAAAAAAAAAEA\n",
       "AAAAAAAAAAAAAAAAAAABAAAAAAAAAAAAAAAAAABAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA\n",
       "AAAAAgAAApx0cmFrAAAAXHRraGQAAAADAAAAAAAAAAAAAAABAAAAAAAAH0AAAAAAAAAAAAAAAAAA\n",
       "AAAAAAEAAAAAAAAAAAAAAAAAAAABAAAAAAAAAAAAAAAAAABAAAAAAoAAAAHgAAAAAAAkZWR0cwAA\n",
       "ABxlbHN0AAAAAAAAAAEAAB9AAACAAAABAAAAAAIUbWRpYQAAACBtZGhkAAAAAAAAAAAAAAAAAABA\n",
       "AAACAABVxAAAAAAALWhkbHIAAAAAAAAAAHZpZGUAAAAAAAAAAAAAAABWaWRlb0hhbmRsZXIAAAAB\n",
       "v21pbmYAAAAUdm1oZAAAAAEAAAAAAAAAAAAAACRkaW5mAAAAHGRyZWYAAAAAAAAAAQAAAAx1cmwg\n",
       "AAAAAQAAAX9zdGJsAAAAt3N0c2QAAAAAAAAAAQAAAKdhdmMxAAAAAAAAAAEAAAAAAAAAAAAAAAAA\n",
       "AAAAAoAB4ABIAAAASAAAAAAAAAABAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAGP//\n",
       "AAAANWF2Y0MBZAAW/+EAGGdkABas2UCgPaEAAAMAAQAAAwACDxYtlgEABmjr48siwP34+AAAAAAc\n",
       "dXVpZGtoQPJfJE/FujmlG88DI/MAAAAAAAAAGHN0dHMAAAAAAAAAAQAAAAgAAEAAAAAAFHN0c3MA\n",
       "AAAAAAAAAQAAAAEAAAAwY3R0cwAAAAAAAAAEAAAABAAAgAAAAAABAADAAAAAAAEAAEAAAAAAAgAA\n",
       "gAAAAAAcc3RzYwAAAAAAAAABAAAAAQAAAAgAAAABAAAANHN0c3oAAAAAAAAAAAAAAAgAABKVAAAD\n",
       "QgAABsgAAAYNAAAHrAAAA+QAAAVGAAAD+gAAABRzdGNvAAAAAAAAAAEAAAAwAAAAYXVkdGEAAABZ\n",
       "bWV0YQAAAAAAAAAhaGRscgAAAAAAAAAAbWRpcmFwcGwAAAAAAAAAAAAAAAAsaWxzdAAAACSpdG9v\n",
       "AAAAHGRhdGEAAAABAAAAAExhdmY2MC4zLjEwMA==\n",
       "\">\n",
       "  Your browser does not support the video tag.\n",
       "</video>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "grid_n = 5\n",
    "grid_m = 5\n",
    "\n",
    "r1 = Robot(\"A\", (0, 1), (4, 3))\n",
    "r2 = Robot(\"B\", (0, 3), (4, 1))\n",
    "trace: List[Snapshot] = []\n",
    "robots = [r1, r2]\n",
    "num_iter = grid_n * len(robots) * 3\n",
    "\n",
    "t_0 = 0\n",
    "trace = save_trace(\n",
    "    trace, [(r1.pos.x, r1.pos.y), (r2.pos.x, r2.pos.y)], [(r1.goal.x, r1.goal.y), (r2.goal.x, r2.goal.y)]\n",
    ")\n",
    "\n",
    "# Create the contracts ensuring no conflicts\n",
    "c_collision = collision_contract(r1, r2)\n",
    "c_swapping = swapping_contract(r1, r2)\n",
    "\n",
    "c_collision_list = [c_collision]\n",
    "c_swapping_list = [c_swapping]\n",
    "\n",
    "random_move_nrs = 0\n",
    "\n",
    "for _i in range(0, num_iter):  # noqa: WPS122\n",
    "    # find the current distance to the goal\n",
    "    to_goal = distance([[robot.pos.x, robot.pos.y] for robot in robots], [robot.goal for robot in robots])\n",
    "    \n",
    "    # set up the dynamics contracts\n",
    "    c_dyn1 = get_dynamics_contract_robot(r1.name, r1.pos, t_0)\n",
    "    c_dyn2 = get_dynamics_contract_robot(r2.name, r2.pos, t_0)\n",
    "    multiagent_contract = c_dyn1.merge(c_dyn2)\n",
    "\n",
    "    # add stay at goal\n",
    "    goal_contract = robots_stay_at_goal(robots, t_0)\n",
    "    multiagent_contract = multiagent_contract.merge(goal_contract)\n",
    "    \n",
    "    # set the objective\n",
    "    expr = objective_expr(robots)\n",
    "    \n",
    "    # optimize over the contract by minimizing the objective\n",
    "    fun_val, var_dict = optimize_contract(contract=multiagent_contract, expr=expr, maximize=False)\n",
    "    var_dict = extend_var_dict(var_dict, robots)\n",
    "\n",
    "    move = [(var_dict[Var(\"x_\"+robot.name+\"_1\")], var_dict[Var(\"y_\"+robot.name+\"_1\")]) for robot in robots]\n",
    "    \n",
    "    move_ok = check_move(var_dict, c_collision_list, c_swapping_list)\n",
    "    \n",
    "    if to_goal <= 3: # if the robots are close to the goal take the optimal move or take 3 random moves if that is not possible\n",
    "        if move_ok and random_move_nrs == 0:\n",
    "            print('The robots can take the optimal move {}'.format(move))\n",
    "        elif not move_ok:\n",
    "            random_move_nrs += 3\n",
    "            print('Proposed optimal move: {}'.format(move))\n",
    "    # if the robots are not close to the goal choose a random move with a probabiity that decreases as the ditance to the goal formation decreases\n",
    "    elif random.random() < 0.5*to_goal/(len(robots)*grid_n):\n",
    "        random_move_nrs += 1\n",
    "        \n",
    "    if not move_ok or random_move_nrs > 0:\n",
    "        move, t_1 = find_random_move(grid_n, grid_m, robots, t_0, multiagent_contract, c_collision_list, c_swapping_list)\n",
    "        print('The robots will take a random move {}'.format(move))\n",
    "        random_move_nrs= max(random_move_nrs-1,0)\n",
    "    else:\n",
    "        move = [(var_dict[Var(\"x_\"+robot.name+\"_1\")], var_dict[Var(\"y_\"+robot.name+\"_1\")]) for robot in robots]\n",
    "        print('The robots can take the optimal move {}'.format(move))\n",
    "\n",
    "\n",
    "    for i,robot in enumerate(robots):\n",
    "        robot.move(move[i])\n",
    "\n",
    "    dist = distance([[r1.pos.x, r1.pos.y], [r2.pos.x, r2.pos.y]], [r1.goal, r2.goal])\n",
    "\n",
    "    trace = save_trace(\n",
    "        trace, [(r1.pos.x, r1.pos.y), (r2.pos.x, r2.pos.y)], [(r1.goal.x, r1.goal.y), (r2.goal.x, r2.goal.y)]\n",
    "    )\n",
    "\n",
    "    if dist == 0:\n",
    "        break\n",
    "\n",
    "animate(trace, grid_n, grid_m, \"2_robots\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e75c3433",
   "metadata": {},
   "source": [
    "This is how to set up a multi-agent navigation problem in Pacti with a horizon of a single timestep, if desired this horizon can be extended by composing multiple timesteps to ensure that the robots will not get stuck depending on the obstacle placement and the actions that the robots are taking. For this case study we will continue using a horizon length of one but we will increase the number of robots in our grid world."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "959e8914",
   "metadata": {},
   "source": [
    "### Extension to three robots"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "id": "f82c9beb",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "All robots reached their goal [(4.0, 4.0), (4.0, 2.0), (4.0, -0.0)]\n",
      "Rendering 23 frames...\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "<video width=\"640\" height=\"480\" controls autoplay loop>\n",
       "  <source type=\"video/mp4\" src=\"data:video/mp4;base64,AAAAIGZ0eXBNNFYgAAACAE00ViBpc29taXNvMmF2YzEAAAAIZnJlZQAAhyltZGF0AAACrgYF//+q\n",
       "3EXpvebZSLeWLNgg2SPu73gyNjQgLSBjb3JlIDE2NCByMzA5NSBiYWVlNDAwIC0gSC4yNjQvTVBF\n",
       "Ry00IEFWQyBjb2RlYyAtIENvcHlsZWZ0IDIwMDMtMjAyMiAtIGh0dHA6Ly93d3cudmlkZW9sYW4u\n",
       "b3JnL3gyNjQuaHRtbCAtIG9wdGlvbnM6IGNhYmFjPTEgcmVmPTMgZGVibG9jaz0xOjA6MCBhbmFs\n",
       "eXNlPTB4MzoweDExMyBtZT1oZXggc3VibWU9NyBwc3k9MSBwc3lfcmQ9MS4wMDowLjAwIG1peGVk\n",
       "X3JlZj0xIG1lX3JhbmdlPTE2IGNocm9tYV9tZT0xIHRyZWxsaXM9MSA4eDhkY3Q9MSBjcW09MCBk\n",
       "ZWFkem9uZT0yMSwxMSBmYXN0X3Bza2lwPTEgY2hyb21hX3FwX29mZnNldD0tMiB0aHJlYWRzPTEy\n",
       "IGxvb2thaGVhZF90aHJlYWRzPTIgc2xpY2VkX3RocmVhZHM9MCBucj0wIGRlY2ltYXRlPTEgaW50\n",
       "ZXJsYWNlZD0wIGJsdXJheV9jb21wYXQ9MCBjb25zdHJhaW5lZF9pbnRyYT0wIGJmcmFtZXM9MyBi\n",
       "X3B5cmFtaWQ9MiBiX2FkYXB0PTEgYl9iaWFzPTAgZGlyZWN0PTEgd2VpZ2h0Yj0xIG9wZW5fZ29w\n",
       "PTAgd2VpZ2h0cD0yIGtleWludD0yNTAga2V5aW50X21pbj0xIHNjZW5lY3V0PTQwIGludHJhX3Jl\n",
       "ZnJlc2g9MCByY19sb29rYWhlYWQ9NDAgcmM9Y3JmIG1idHJlZT0xIGNyZj0yMy4wIHFjb21wPTAu\n",
       "NjAgcXBtaW49MCBxcG1heD02OSBxcHN0ZXA9NCBpcF9yYXRpbz0xLjQwIGFxPTE6MS4wMACAAAAV\n",
       "P2WIhAAX//731LfMsu1Tb7YLqPeiniZfQ3UlAZuWxO06gAAAAwAAAwAAHrwXOAJfiQrzrwAAAwDK\n",
       "gBeoSf8KY4+ICYCMCPmOK6uxPufUdvSXd0d0Rrth78IMaM+ncQ+cQt/2oJ4Sx7t4ktF5W2b8HeK8\n",
       "hSQ3Nf2QAAeV7EVOPMAv9cOoIQ0tQC8ZvW/pF3FR+6qsRGqJ7EqHEu6JOujfMZ8nO3CltbMrnkR4\n",
       "Z05d2Ikt5htR9ESc3SHvs6FRmzVCsz9nWrdqrHnRafThkkEFrlWlqNrNl37hG4ujmBoojN+ZhhGJ\n",
       "KEHmPRCqHf8yEJOaNqoUB4q10SdKTPof0+SNeKU+PfO2cuusQ/DE20c66qMbRKY6ZJ7JJtEoCTde\n",
       "16WNiI5oqIdhp04up/mSd5AmaoVmfs61btVaEfWv3LmhY0rvvV1fwfvZ1gzg1I5pMzDu2U9JYxCE\n",
       "DHb58cJhf/mArXWr8kBvJGvFKhrRlUXHKV4FJUp6Y+H4Ew15N6UHgiOt5xfeECPFx58Uguoj8B5n\n",
       "DcJPuwTnlzBmftZRjPWDhtxgCmoKu4W7i4HmMiM8SRT27Tqx8wsKH9iU1MQfITPWEEBoWGRUvf86\n",
       "2PACCAZMubaH2SpRK7jnuLfaszFxlEn5Eey/UBDdCoIzpFfQbRWRypzhyOu2/u35uR8y2NvNiHeq\n",
       "7nYC4bLzb7cxylr5ln5Ts3Y3x4ccAhDA3Gq9+TgAMFQZWzcCvt6Bm1HMO8zVT+V0/6cz+k7xOq6z\n",
       "TZrJ5DqQ6bYSTqmJJ8l1occUUPGoiaxk0pbLUL+hjNxSRWy0r3RGWEiZOeaCY8FgTmCLYMtqGEds\n",
       "VGqz1Mp1E/G991MsgJ8oesNcK/zYqbDMjSXxbpy+tdGAd18KwYXQrSrayB/B6HmdaoigVw3NysKB\n",
       "86ZL70l1upCg6+sXscyHS5ALGjV64BhSg5j44PabeNpE0FJyv0u2XAGaGAfSnRap8jfRoZ5TIVZH\n",
       "9r2VpqKC5rRqjjmAieXX0rs5uZcTrBpNduhqJLPkiXcgKV56uXMvyFTXPOgPdbKUauZKu5NJFBTR\n",
       "0Fw++NHug4tdabtptXKx+Z+MkYjcWf6whU274Gx8JHE/ADW5HN8GoslvCfhz4ssIS7H3y8/gnllb\n",
       "QGDE8LXiyFPn22RgVxoGGgjBsQDJcs5D/ivfQosakdUyfka3TPKNAwBKpBvQESNRjNauQGA+kWaV\n",
       "PShnQdNFO2OyBI3UlIQBiNnYn9Aat0XQ9cFoJGbed+0rvUlPM0y4CRgeO3FrPFq62/0YOQKEP3L+\n",
       "9A0JHcKoKkgvf92bosb8+yGnjgiFPEMU1x+QM/QpwCf82mXGefDX7vUsQWpII1Z0T/tVGpMU2l6V\n",
       "od170u/MRadh+yk4wuvuyyaAqiAPNE8xMLtqM4c9p5PFR/s/seRvZcvTFMV/qmFm+JLOaRi06SfD\n",
       "TV8sPiRbe/0TLtzgU4MEqdX2kTH66OmT7UC7Iw17Yr/o+iVmHRmP6ekG/yzTCd0+b0cUb+ULsPiJ\n",
       "ZUAq56Yu4o3F67LZ9D+sUPOjGp4WqpeMF+FWwFt6fkzMJz/q0KcqL77IikXuKJl7cK4aFHwHD2eu\n",
       "eXSmaIaiCMA+AAtCoUXQr7Nzni70oWv0di/wyHQ6csYhegwy7JuQcXJSGzusT4foLopi0ghyfCCs\n",
       "F3RZGbg/0TSx0ziBlVZVXpxgzg3GoKjZVCdCSJ/R7gQJuat7QJVR9XRNqzD5ywNYD7opZfZWa3aA\n",
       "HehXcOOMgbNjdB19vuLDcTOIkihXzUbInbiiRVjnDrdPDp2utkmsPddfJaPZrkiZlaSlkY6yWyPk\n",
       "Th0VjVcnv9AcJq+uVwqN8gLJ6CRmai4NwdIXO83c+a5ae7T9BhPP1yB506s+wg7Ku0NYJHrxoKS0\n",
       "FvC5ukD7XzO760zYXCgvrDcOSwBbbWznL24LdYSmakSIUkWTH+3+OOnfc1/8Ao627nqTVtuxwpC1\n",
       "nS77+/nAFA5Vr2fGdDBNbE6OvolEn/uXRPGYfW3UIgYOptCacczDN8MA7iyy+aA+Xq8p0Btp0ZJl\n",
       "tJN7n2wDiFIqW7TSRZd6RXJceMq/eoPnhDIKOUULr01oPbLMmPFsDU22PhPfkszVwth4QIk71vrm\n",
       "OTAKOqGrVc1F/1dCBnL1OVUw3+GFnrx4fodcMzhAsBCEZrUwsOfC/fu67/AfQnUYrcFIHFMsZpxW\n",
       "TWvCTBaad6ISnpKAG2soyMewwl6VYWBDc8HD/zrDRgy/gF7iVmMMmC3F/21WmePhpI/ipPHXPqM9\n",
       "9SUL55gucdGvPA2E20sboVCBh4BtP0k+iJKVEGdOCyQqObetTr0N4yrYIw0AI1HC1fuN6jArgzSh\n",
       "TyeVcXVbQtBJKYxnIW64Mha0FY24m7eaGqqds1S3q19duTnd/tDITKiP7VeR8aaDpHEAFzKmDMeB\n",
       "Lfg7jgam2q5SEPFffuZpJmZhvR5SnIsp/Kf9Nt2EhZBKmGNSC/TGM22kMMtYvKPklz7goh5M6Pqi\n",
       "fUcPkZ54SgKj/acix0gaRDvyaRYMiAlugDuQ2xeeOdY01pnb2ah8eKa0W2IMBSOQShUc3F1Gj5rl\n",
       "pya5hffRHu/yXcg8saICkfxu0WNBNHo/dYELdPIHVGNWEz2dAXF2LHx+8uhSCuqOVMQWjd2b5oPD\n",
       "DVZjaVtmlNp0bcGDwMJtR1sgl3pZkUHjmLNDxUPBXGdPJ3ZbX3KY3uVKiZipUZZEpCG/unm22tOE\n",
       "Fuk/IjgvMxMXDin/RaTEoBg/d2B/OQuyymhy9Kcou3RlaSIS1Bm7uZyJcXZtuQ47VfhzP6rg3CHp\n",
       "ncD95A7XB4i86IpegXymUegBXh7bIKIR0eXY4wgZpnKDkqY0wanumhq4WSpx66FIEE7NdR3fGmBm\n",
       "0qg7Edsa4MLuO2hbcHRBz6rWylmKFGcbl1Wd8HE9JnLYIg7nee6d/tf0dwvNfXY3ra2gs7tm/JRx\n",
       "Ki/XG7nb0ndrNehAaaEqwQ5AOPNRsUhDukgjrFuV4iDgwr/3bJdKfeo6l6yC0kSTv/Xv9OIhpUex\n",
       "8WrRBsXDE7uZS3gzGIIiZ05tLI1gdZsqPGH2v7vjjL5vb+BrW3Hf/rP33T5CCURiOp3+KGLifrfR\n",
       "ffoaguG90O0wYlMNqieb+mGHVAB0B0VE16WIqZYQRqfSQXaaIJbWmh1XBPVcvAB/Jel0P++GtnvS\n",
       "VkNH7Xqwddw+vn8R4R/1ZN+L2wkXXz1a9Cm92GxZF0cd5zGoQ7//8hZBJ3sH4oWPtE4lubf8clmW\n",
       "G8UzBXWpU5+DzZWPx562e2n+OJSZtW1whBBlTP96Zpt+tMsCEiNQHnfu3cfdDXQ8AmI88/gcAX+T\n",
       "zUs8r+M2x0n2NcMdJVBbc9ilhZTYWvFTD+fzhgure6AT3wAL95ksppNp9PZiq0M8e77VnmYqTvHg\n",
       "d5jZ+BosUgB+u6gIE1xGT6bpv2zngP/EaAifHcOR4o4t31x7tsANgwV4koqslFi7XydFRv8u/Rm/\n",
       "uCkjHkgIxqwxECemvZMLddiQspVT5Rle7XXBL0A4pf+89AVdmgs0U+qSUYqZQaMMRuPEq8yM0mBe\n",
       "spVaETBjPBUM+VSWcArMMLALQGBYaPYtVdr1fRm6goCFTD+fxqTEwPgYCMM3PJiT9gPm9g7/5pkH\n",
       "OnvpN+mdM91vhMXj+PO7u9jTnBk1NNzaNYwwl25nJBByCwgDPsu8W30dTaYKBMmjLI4g2KjfSAnN\n",
       "bWQnQCqnMEXFzDhEW+AXLoeJfw8XrMQAuUXJsBlpOy/4cOE3ukWKphu0oTtuJWaEbaK3LjZlqK9B\n",
       "QHn78bdMJIU6n0/LkoD9BP0ReOtOqxOFbj0c1K8DmSFS/r8LE+26JGMP8F+FGgQtL7PmFWskKqMS\n",
       "+S5A2PS1FjQI8ikFh71Cs75tZlqSfgfbHlbyFIvcVUBpQuNmWfP0lvJwWqqJJ68DZqmB+xdMEs1c\n",
       "vJS2CN8yD4C56wIFl8gEApMaqGd5BJm5Hr0X+TKzGHtUtrBoydRsM26/wu+n4lVOUpY4Uzjg+ZxV\n",
       "IJUQh4v1+50FmZHyZO8fWcbfpc6nXZUiPfQiMkvdnGMwdUd2+VjYk+ivGNtWNx7H7A/sd1UYomAW\n",
       "GWp+1QzgCU1xWrSANEhzAdRnD3P/8D8kS8qQsj32fmh3S7ZC7AByi51DDEFTgan5oAALMMxqmSuF\n",
       "ziSgKkbqcRfqem5XgBQFj7tmvD4fcocOEI+jHwV8azsszTMl+ZYU8iGymSvgHWi6j6moYSF4eJMJ\n",
       "hz//U1oHSA3apATamIFl/R+NhC0oTBG8k2cgImGxFGo+HKx7ypIZlXis51KIEUYlurYo0J9Nh7J7\n",
       "ZdM3Flu68QmJIoz54y+D/zVJA59J0mGYOI3jSFZCkhp8VZuPteBxPneY86Apy58YkTP8eSgaYhqz\n",
       "AhWQ2WWvnV3sn+QfgU4w284HNsV7WBBqmuLJxvBt+pyRBWZoS/+0liU7MI5fqc6onfs5bWVYt0bp\n",
       "uXtG70annviRex37FZt07ypcOa8kFSiMV1yLsem49l3b5JPFqB3fFy5fJJaqaaB8eV4oR5WSG4Mz\n",
       "AXhrm915dl7Q72w7ocTFb8ZZ1rwn0mK51La257rW8fAYlYCNDAKNs1ybaKC5QYQSkc86zG0d5AZ1\n",
       "t4p9xrT0mEFJ4GfR6Ob5udD7RFQjZ0IxYQKIrhktcUm1GxX6cuqlHfQ1QGEv6wyf5VgsQBp1GFzi\n",
       "FMYzedqGamNFR/6xsCb2ytbMsiTH6tcGumSabEQAi80RyXciA9zHleb4XrFsUKLVR28efWgc04m6\n",
       "ZMz7NYO7unlywQljs/NYEkNIGCHafLFcJqrASj7BHlCJJiLcLNMf49zZDDnDkkvE70AKd0nxMhxh\n",
       "H3D6QjstDYj2nuJW9bJZ4gYGlj01dDnUayQRAKGuF4r97349oadRsxXb/p9f09xVd+8bnOgN5asA\n",
       "AVqUTBccvYyVj7St+hC69HSLwq2sB/ZtxlqvgSKbLEEXqNyyiBgJGDsPI/54E1pzhvyArT1hmBOt\n",
       "XBj0YNSehhjg8PANrWUebI1Hw166TohCdhtaTS0uNNMVNjZzwnxa61821dGs01RbUAYziIvtIPiE\n",
       "smbh4o8fYbyaS2lBeJdgfixHpwMf+ErPqoee5prUTsSzpNC5orw8aBbnNc9DraDr2pOO+gC2yis+\n",
       "KKGy/tpuFVISYILp/IxLVFiBE/kjLY6fL8YAAIb4JehdKFwv2flNSGf5WdnHPdFz1QEn0tIL6FbZ\n",
       "bEjil9YTbNZkv5bCmWi8GtN22Npv2i7JtLhGBrJgeUM/AG3vUjLn9SIq9qpljdM0/NqL8/ayuAcx\n",
       "iu/g1d+PAVq9ua9lbVxmRAjMpwYGxNdNUXQLVJRubFPF8BG5kXdXldXIoZzkTuTO4z3Vxh5i3r7c\n",
       "YRO0y+wAZEP1jS6i2ypZKqiLLuiBBPSWT3bcGHBXYuoX2w3J5qcM6VpyjofQfSu0mP1B272oj0kH\n",
       "NlnNd7PAuMyIEZk6vbTPRsRBEXLmQY52xS01zQ80Ox42AaEc8lPd53oErK7S+gCIs7c6/xbUAdWW\n",
       "j+2uFTwsoWN3y05tf1/i9gpD1cp3xtVnfV+w68eOCcl940X/yql9ob326U7ThxoJ+R6K7I37Al54\n",
       "ApsCmUQihRGWjxqQCOEkpuHQtCJUswvj2Z3ZPMm7jSHYi341hJFoCjJ8IFeUlfJgSd/IgG3bUZ1j\n",
       "ZuuJhH4di/JJjVVpx3C99by7gvMm1NULaQgsn2uExhrjJohxns8z7Iaw+2CWY2VKmUg7e2tFZxBg\n",
       "XvShazSzv3bP3joXA8fdkexZ0n6SuwoCBezmB3lbgVCge25rJcxxiB0JDfzupiuGS1Z9bK0AnnBu\n",
       "cZBYD++LykbozDF4u3M96d14b71tfN/sQgHBLgOhbsBwm/iTlu6b6+cQMdihatmRPMYNGJILp8ei\n",
       "b6/2DhObr0T20HT8PF08LUzZQUdQZVbidsDequx0r6FEcQOX+aOgnlfusTVQxlEi+bBzGQB2hV3y\n",
       "FWz+kV+bXdj7t4uuD1ZLmEYPTxNjOyzQFzvDzjF53Lt8HbIV6BVDUDzBGlabJTsmnxDC7ZLtMtiu\n",
       "z0FQ6mcxXp1QLgArrd4dL3KOgla74PO8m+LQxbdGyW1zwtjPJzfbhZB2m1aavvtIkLa/qfBe1Q5d\n",
       "8CZCC7gto2tPMBeZvLAWI3yqJq4KK+pCS+2FVp3/r2q8tI+2gqwIiNuLQZ+TdEGPvaEi9tLzk7sz\n",
       "dc8PO6jb/WBSJX7sVjHiNgFvg+K27DsSe946l0/oI6ieygwFr2AweNgUOfF3cPswcIkIIEvbFpg/\n",
       "XpbMOpjMDBfJu/p3fxfj6tSdeeSmmVCoIPgMSnrpkh52sHq8TloRa9/qxYMlIDcRTK+fjrSk6iEb\n",
       "0PKF2rAQ9DEnl+wsuZevicI2V8MP9KAMlylA0oJKj7fMsOtiwSItaZw9wGWIoR3i4b9v1baiEFNA\n",
       "BynhPQhmcXnt0CCdz6ZmHr1BqkOFREnfVdHcFxV7dmY/qsJ3yc6U26xwCstRrIrHQ8APkB+kl7/R\n",
       "aQrWTz8D8NjkdlVXlmori3YUFJPbSJNMDoCkKG6RZuiDA5a8rcKV1G0Dymag+GkaZZG0Bn+ub4h1\n",
       "46yepkg7vumVaiowyMJBIhigRI+nbcdESnB0uEuyF6vRvIDfDJNuQbvm5dvXmd7mYKLYtR/r+/4y\n",
       "uTvuE800m9imEEURtywo3xnl/H8VLMq4YwmSI6fSpmT8qILPqXmWkS+vx4U6ZnPs5fXgAEaWU3qF\n",
       "KRD6jIdVJYLRGmx32RPLqBiXj6d2pSKwjD1UP2/Ba/HmQVH3YDiH58UTKRQLuZzoOhgKG6s+bUob\n",
       "0PnxKoUPKU/RxnnmeaQ2nIJ+dZcQqeOw2n/Eo0U5pEtFuM4HC8KTYV6lXazpFgMgf4CYi2np3YtL\n",
       "6BpfY0xamFGLDs4ySNm8tdY3pUgNuIUbi4YiWLYTwBQ+7SaTq2zS0Xz6L7NpKMasSSD1hKn7Lkv1\n",
       "9GAMZzQr5xTvWRpqhmQnX+mqVN5AOWxPQxJgjDm+Pi+m4gmhvZrBrEBKV3JwR55FESLi46F1UGiu\n",
       "Aff8/hz7tQLG7x0pNbXFCVSarWtt6fkE0iFbnFmDXA1x7kdlB8nlKUh4BoxuRB7hffxCJx0SgKSa\n",
       "TqD7uiswxlcWGm5qCxNLvZOb3kF4AfmtSXBU/fGVIiUQYKjz/I+e+15WO/QKzY2IA61lzbXYOI6R\n",
       "2BBz+Ia16kdm3wBCXJ9KVhZcuAAAAwDXgQAAB8VBmiFsQX/+2qZYAJQ7EMAH0Gs7s47NOh+XopDi\n",
       "6xLC2ATapPJd3uxEIt6laLcqET/2D+wq4n2eE6cOJ6jYoX9v+tkPH6lAuQZd+WiNiaumaxEiYWc1\n",
       "Vbnv/o8G5b4QWiMUe8kQJDQ7x/ogduv/jpSQ0PV80YMAOAOcJF/iMlOoVTDEGeRYolnNmLgl3MrB\n",
       "ydAyqwd5mKjLKNnrDr9mEEay6AQjTbyZjcOqdd3MC9lqyYB/5t9sB/4PP/TuGeYeNL1QDgWAUeyM\n",
       "9m5qVurajcAIDdkteBGQX2Zh+Zct21J/GDYJ7gtZwUEI4EDZrlR9A54DyV/hK/ifEhkZe9MkpVKz\n",
       "kN899GQbuXU2zSnzDm4K7u/4O9K0lolTnazo9fw0oiEXGa2vh2+TxgS+ds8zPZVPfUe0y8QvT1Qj\n",
       "OHVijDWoGL+Ekqg5dUfqpjhgrkkabIVefP/63tQOyqzijBXv8s0HJCU+IYi789OKM48Evq0ZlxuL\n",
       "3Jby/BzORH8M6aRhuxp8ht0wTCCg6ngJ0tEKAgNnPjyZXFIhHh296fkXXvQ0OmNqdHboh0n0FRfD\n",
       "3f2HGu8NE1kUeVnUQWr/9fdoJD/DgLT2VVdtjiXVYr4VZxWgZK9xoXOlCDNh3cb9E2hBiN7H+EwW\n",
       "Wxq1ey4i7RzkqSJpnyhKh0lnc2ZWNl/XurHMDL422Cu8r+frDO1vWtdQw/rsVlVqxGrZ4lojXhk5\n",
       "MKAEj8gWwbywQ0dS3SU8PQBtmAtooAjrL5lVkbrPSa+dAlSRNSFeOU0j514wD7pohs1QDMG69eEG\n",
       "bdbKHzL3F4zsj24FSSii2fKhLfTq5ywO6Lpk36lX2c5M4X5ftNJ3Zuupl2Vnf3W2lSPKhJ/MAKnr\n",
       "VkNuTeyoEz2fc/VdQKFzkEBVVQ6Dk+fmufFsTR/vu3KnsBSKeo45PBd7hz0WxKgjdCHypuOAiKsf\n",
       "qvjIDKQ9UsPlwhRTEoH4RNVzGhxxjhqIkvGRtWMWhTvohe95Z0ZCAgsQuE7X+/Q5Bi6sYM4uzFqh\n",
       "jYpzDEYlolIcDRgwbCJNydfS7pI8fMtSMzjBulut+99wImbqq+rIXMvjNSNya2d1vmlcHrGVV1d0\n",
       "wxQeAmVliPHm1qo0y5pFjSFALw0flLJqu/f3WejKcuqHFWQxhNQFAQYsF2iS2l9OIVQExtfPtbPm\n",
       "0XR/Bqk0Ut6zhm6tmQe9BrVMNgy4oxh9T4UeCUTX2z+tMJ16oAVIrcc3VxHBiKlJ1GFX4C5LwfQo\n",
       "lUHGdxAOOGmJkYat56EKyyvClHk6b3xZ+XFDyNVF0bPYOCm5VBicBSqqlVtSCiYhKwQvccUm/JPa\n",
       "iJx/8bAwI67LEzD4DLsLgH1MMdhpgwN0wG538GjYd0BDqGe1V0sbTJxMk1QKYgB1CiCa3qHCxlM4\n",
       "YrIjhtx+BLYgRy77Yl2lOvlokZzzcR3k+oIQsBaHtn9xEuBSs+VYLuVHuWFMFKYYhVANFVzKVA+c\n",
       "sCD7sBRqDFEzyf6TW6ZdDrpM3kZHoxlFWIbAim51p38ajQpHZC2dxhHmIXs5qpwQJ2oK+/USBHwh\n",
       "at/fbopPr3hJ9Aua0woF9KUP2y8pD+HVvP900XjJ8tuWX6zVqsVxpevtaQUKpvduX052hGHm9KvJ\n",
       "GJrlP5SOQXgwuuqwO7+85CwW9AQTc4vdJPHk3Ip7I5wALcJGk1t7v9YF80Toa2x5QXOnDEoQ7/0K\n",
       "O0EthJOvQeM+7PGItfU//fRIhWdfyuyT4/2PIT41ax7GF549Zd58mcy9WrjByHxCSWXvoM84v9yv\n",
       "cHXVZzuPAL2qhowmJfLK7j6HJudOY1eCs7pfTZJ6i7CG0Z4F9gUC4OlSEc7M3MNRaDfkAhMw+2Ln\n",
       "YEhN9SxYVn26sx+oyvdhhgXGNQc7376ZZvKEwvL22pMWpjEkMq4NZm2Xoya6ujzW22R9q7XEx7kC\n",
       "O15OY2tsHO9Hn2aC+Q3vxKdSTEuPV7nIcX/OY40TWjseqKEXgiXEfhjOzPDS6y+J5obLLhW6diuW\n",
       "Zqh+2MpxCU1yuFIXHB9lENhDEULiQ5YbUt9tBeVdA17LHRhUUMRxB0WxoCydmDvMRFAl9X0nSFIk\n",
       "9MWVvw4xa2aId58ZAVfrnm1GnBXYtp/WOBfBIfwTBUvPc7PqOWilredAWmvs8Btfl/EQWSwPJlVP\n",
       "+GouAqSSS1By1c4rqLNpwI4xlYNae/n9n9a76HcVXAEG4fZ/GKC3S3qNF/R/TlYVEmby0UuliSJ4\n",
       "8FlkCZ+CpRDir7dDqXbSiOv8Ft/x9S87ocIiFmlbNcHlD4/JyAl9nxSKzyyEvXWHKU/kUxsrl9z8\n",
       "3NPM09PyXkS6HSa+Azrc0rXywhNQj10wlYlD2StxxvgrBKoHSsP9tyvke6it9J637GCH3rZnEhq/\n",
       "n0zeMFpFL3NpI8eYMLizpF/zrtkclL9+GDSQvcbu+B3ArXIUZf0EkGzxtYgk7Az7P6Jioyaf4279\n",
       "RSczyFcCEiP+KMVKpdrvK/8NdbOTagXCA4N2ivWtmLL7cFi2lIAPa9zuIaz1jQ3fR0ixRqRJxgWb\n",
       "po1b9LRKwkVw8yf3d5z/Kij0OAHDHsKQYzIXuVEtJZ5SyTeO1R3Bzon5Wntodo1FPjEMm6RORCiZ\n",
       "jJt1CaD4RVBqpAhxJvRApbDZXMcQZxwAAAcgQZpCPCGTKYQX//7aplgAlDzCgAPiFBrng9wcoGx+\n",
       "QDLKDfbQfOY+2cANYu/PZT9IaBX9H/hLN5rSUpwPmh41RBpn22zgtEHeh1/O/nxhk65uTYnvbosx\n",
       "w48tCmGDC8+R+8lghcVZJjoizDSpGlr7k3/5NGvP4Z32m8zSxvcJaGg5s3fFB642SeCkWTY/jcdW\n",
       "fYbJTfWrMZcw4REq1o3n/HjDlZFUTilnJu5bOS85akIguCRHiNvy1cvGJ5fELu8w31B4d2IWcIhu\n",
       "/B10HL+RuZri1vo1pWQZKllg/0XK8U2e8qzvL21MmwZ+LWelIy+I3fWbRpeAZbLrb+U72yFmLm0d\n",
       "F0h0mBDIwLjJ48/tx9fDUiRV4LWB8lThFsQoh/wmZBf8mRN04EVMIUAL6Fcb5gZ11XH3zNWqiDZR\n",
       "+g68bAYTi/KVt7rjJazC+h7Gzr0/OlYoeQEgq9XsPaYMzOc7pVv8vvRK7k3kCjNsg9PQl+UdQvAI\n",
       "L9TvK3HbDyITiQG5mVbf7DUBHej5csrz81bWsh9tsw3TJc6kMKbxUU+ZzGef/PGQ+W6QfQmtqJSu\n",
       "Ruw+c9qgeJgmsaKmwn9q3EGWki7y4RORygrln+nZDFzSrNX78DxrDRrXkHI85sAh46a+i2pgmoyk\n",
       "Xezqq/t5D5OMHbU5WZqy4YDGFggS0/qKsqWbBnQELRHOyOJ0X4/Lht971joh6RzIp525oWNI7TyX\n",
       "na+zsYUpp64A2tFDoIh+mR2exuyVFFhb8XCpBW5ecG+tfOrQLEMFwXULgpXesbA4GFc0uyECqMf1\n",
       "DjTD09jcrO1+u5dK2rjiARNtDlchda2eiu0sxRLhI9NEjSOiXrF8unop+D33jFAG9l33Q5znqGqY\n",
       "JYL4NYQy+8Sr/v0mtAM5qndYUpLCjNsm5ozjND8DE8Uc99u4meI/Qcnt3OlyBU3mOdNuwANW9dbb\n",
       "cOocHIgCRZyqVbf2TSrtFanls02D0b/riAQXFqjuSGmVN2THbL3tQ+KhgSxBGntJechPJFb3RueX\n",
       "+8N0LmtK2H1Lq84TlHb4WrzMfi94N27yKITzvEGxjOmY8XugeN9W8n2QTIXSzNH7fapJn+xjS9hI\n",
       "wAbCBSqT6DG6asOen08a5EqVvucbzcWL2BOclLa7kKRJ+q7F5c60WEOhSjOVdtDxeKtg92wrgfNs\n",
       "7cK3IdxV+k9l5tIFZiFsswbodn2GxyaemkIl7gFCqLktCO6ATXWxzZe6pe19RQnRyXJOkas20VH0\n",
       "pnEp06fQny64B6qsPGTNgD2XtpliW//0c01hXYjreYVzUFhW2h//HGZDcNCzpq8/iso4XvoHropc\n",
       "gItPJEWtliEri+axGYCFbxcszU/Khik1yM09fKH2MQDgYTivOQ4ujOWcBYan98NzC92aYMS8qsxJ\n",
       "dF7p+H5mukYDh75OlCopCHnpDrM8UI1fS3oFXdJojwN6WPpAcKGW/+A16AaVh9euSzkFhLtF+SKE\n",
       "vCFzDxEPVxQnBuMXk5v/rzbFUV2XVWjlEUK5nO61PnHeickz3NOIu71hzYMogYr0c3MOaJ/pOGOg\n",
       "jZ6soSgCVUWJWRM9R2pZZKQBbuGR1EO/9ZCfMnBWTppqey4VW9rHaDDPJLJDdHYW6EoHm2doiwPz\n",
       "ZSuq3iOks2Ql47+hXgQdqLO75oWLxMLgUg2DPh0MMP2SOk7YE7wrLAHjX3b6tRvLY9boAykw4QQG\n",
       "1JrObivMdDwAChDgQ8Ep1enjPgz+1xMv/JqkIgPtLPAikMvNH9yk0hTRo6mPqPwoJGFtX5+LpbH5\n",
       "FDt51XkFQzOB0iHzBI3B0+bKiP09s8y2SqPGDz9tdkbid+FIG9ccCgl4cPJn+bqBDWiLZoCl4cPu\n",
       "QMQvqfqTWjbOD7GA2aIyLoohoEN/+ypX+Khdeyid9UrYwTBGhP2nD0BqHbSGlLB4eMWn0/H2OkXk\n",
       "kp6rv6ASGaQxnSi1TpzQHiI2lZ73FW3a8Q1yEt8Vq6+GyDnk2yQug7r4Sfs7vVX2Z2wkN1zYwul1\n",
       "nLYreMnza/E1/znpTDsFeX62/nJRGkEswckBhIunucWB07ZZibEhlUuNorn09PztAcDYwL+R2WoC\n",
       "7k2OZjQv4N0meffCmkYUqJ3DoF8BjjkhLDvvJ4HzBun+RfRXQZLZDqhUy3Ul0rQuJk/azlwqOMH2\n",
       "QyYguyHcMiNilctMAZbLHOTVvLLoJ9c4K0SK+ZrEmUvIs98jjJCS9Ql1K01Bt5P9y/EMf8vYaVQf\n",
       "1MpZ3MRP81Q9nU+flwsIUkGhguZhR3YuGShqHZRTB4w/fd3y7lZtiqjPm6WtFSqiP4qVcFNiYTQe\n",
       "wjlhQD7fKpJomoexpqp0Lq0M7Q1UY59aPasl7eCbteNMDNAEFfXhpxjd/uaMcs529zSTNA3mspXo\n",
       "z4f46/ISXbqdDAhukBscDtcxQUpYEesBVMUlAAAHJEGaY0nhDyZTAgv//tqmWACUPMKABBNJAbZ5\n",
       "YIDdra2rTR0bhpnfYeXJ8/W09MI17vFvK07w5JEi1V5CEowjHj/+F0CBzd84lYL3YfNTfIAAI606\n",
       "AbMpRdvCsqLY/cuLlnAqRb6XerMYZJS1CfE+v+AhieEZAPquUQq5g5dAN+DOmAOEKxpZWAjm/a/F\n",
       "Lpt2lR53w/f3sVZB5DKGR/SZTt+L9tk3j4bHlJvM+Q39GqReq+zou6r9uUeecPXPTHul/CKLwBNS\n",
       "gGnmjF9T5qU1LwI0o+Aqitnkliqh/YKt7SRJ3efZL1xdkanGCPHtygyqSk2xXqDSCpnTfpd+6uBu\n",
       "o15QXHmiRRrvzH35VdDEnXteot3aldlUDVw8pIvARf/xblTeZ2hRZ3HWiXcQQyVfLsLN9r1L4BWe\n",
       "jVTkZmlANKSnNI2KRgOc0yv/2s5s/ZVlDlZwlo8Rpyg/kp7fEsQeNksU/XKHsWMs10KS7+VJEU04\n",
       "t0brTxRbAXkMO//jygIAFBF7WsGZQz+Qi2b5Z7WjOem7qT7O2UZb/ijkrIxzruf2AnuZzEJnPxaj\n",
       "nyrG++8plBFhY33Jl4h2v9JoiL8KueYFGSkrV2qbVAXdB0OsGyvitEChsTZsDx/0xgqZQobjiZm2\n",
       "M8MB6cE2/Al/t4Wc+Ojdna44BxZ/6rQbCksesCCVEGVrirTqjJ/J9jWraMJ6K0RDm56ZjSPyVmnD\n",
       "dceEAL7CJXuJGu+8mb0KZATZ31n5SmpbprHyxoJaFxX7OdAccV3gawDPam56oF4TDqkVt19sYZVc\n",
       "UQxjctDeNeB2T6eTJjer4vRursy6EUdRjClqR6NlEAho7DNWdQSVzrd4dB28rnnG2oopEttYgrf2\n",
       "rA4kNKdqvHQNhnNdy/anlOl/Z5ubXN899DH7Y2nUfzMwFcnEKS8RG+NtGPKIjk1Eg9WnaEDlC/ab\n",
       "tJd5MuLyBifFhKHGXey/enTQ+5iOgp2kNVWtkmzd6s6W2qvsA4iDmocQl0HBgM6qYH8vrdCHq0Qi\n",
       "i0KXlPOFYV9PUqH9rSbPfQxrcNgkc3wbew0RAHOnJIEPqTdnAVffZqLIr5LiXZFAZH5XmUyCXWFT\n",
       "i1n4q63hqn0cDIxx77TCeR6oeUVDUo29kJyODvggcEE/K3gk/G4e4XgbnCH84CI7OgW4q1lQJADy\n",
       "cAU00t/6RAzt2o9r3+anP9hs3xH+KylqNagpJBw87nM0paoTJvi4/IgFESk53J82YkTriX/dUd0O\n",
       "mNDnzBWkvQpCmR2sArzn5jFw9PXaupcn8sebWJTX9m4nmP3bdp/HRtARIalbW2JYE5p0r5LpwkrN\n",
       "Xc9MYpwCNV77fyrke/NZCJua80W3A7VLHo6FGhzNSsMaKRO05Y/A1bVC+wTpYpHbqc0io4g7EwCs\n",
       "W+30AsVQHaasToMpocICpHd+ZWcoZZhzV4+gvgx9FC/QKhJKTLsnnsMxXi1dzLmCl4//pVSjKkuD\n",
       "wSt+/hSB1kVTAkZUO+cIpYrfCE6bvampoJXxTFZyFn0rpudlIddtUMcRgEzymCaHQjjF0ahplJ3b\n",
       "96AZwRrhVHl2FVGavmyvNRk1bcsB0Ya0meiIgk8lFzh7Gjh/AED6ir5+Vtaazdl7M2O+PDFw6CL4\n",
       "HRPybyynm64kC/N7xTht6s9XfyL5wy1rJeCPu5pFirSYujYab9u8TuvzLNrd2aVS/YqfLHRidtdx\n",
       "kRx8srNEQ+Jg+mpPNGa+0R8k0EeADcbvMEpJcsXLyiROkJhthbuyi9d1YsqjFm0MZi7KimmSJ347\n",
       "y/wtlPh3CcaWZmjK2y1+DvS1HQ4JwSV+AH6OXyWw8w/A86MK5lMre9UMwddUPYmXnn6xEmJ4FIkC\n",
       "8AFvPZdVxIbMbbxjOjjz5onwfoz93AyOkVVvqI5SwgZ7obMPueqJhxQ0DAyjRNgvtPjbhoDjIHhQ\n",
       "UIxtdu9C6RRiEVSF8lGJDMR0csunRCwwyP2gh+1xwXp8+oYPQHjupSB+ice0tv9CqVRcBW4Y79N8\n",
       "/2teTcMX6eLb0uDguaMLe2d9O7xo5iBn4Xq7rzVnganYvPNdCt9wAHVz34+oZsnB11GOnjAmXvq2\n",
       "ADzapTUXhC9XZ4SDJazmgVazUzO2R6M6vngkKyJZ4J5JPjX9KOelBWF8FnIPK36Fz30gn2ITgpcM\n",
       "CqiQuT79dszGW/Defm9FOeD4EovvpNcHEn2KLGOnKYww6MdmQBeLXdxNH2A4gf8NNgZEppMDqji5\n",
       "P6LDTr1FvFfGy9fEna5Y60msmKQ7mlEHnqpGb/KqXwZzQb32eFqorjutCDEIV7fGB79z4+Qf75yz\n",
       "yEhSA5WjI+QUBZdETpapZ3bM1rxq/zstBnfS2o6SOYwLc0F3eGpOBU3JM/c5EJ6BYoot0ypmqBPp\n",
       "lRSPMCVgda0JAKvoawU0/4IEoBjbGdNoDWr/EupTf2vSQsoAAAeHQZqESeEPJlMCC//+2qZYAJQ8\n",
       "yB4AScNfNaNAt3g24Uwko33LXst/0Cjq5PDThhdw/wrl5OteAAnC+vS1vsJ4gfDdNDNEDRLYqiPo\n",
       "9eLzMhkZ5RRZD8oiOAuAumQDX6IN/BBkv6liB/X5f2lS7oj0z0Xv3cMq97B118zAgLcwnGH+zV9m\n",
       "XykgoLqdFSDDo867TO3ra15/0tHYNwDaLomrwvHvK3zfEXicM0DAV2WJakrhLBhpg8orRkBRKd6s\n",
       "0eBf/k4IlaPLcgXUooqbHXjY7SOuDHD85uPF2pQDUmCSEPaRzjd+HoSoMmux0TJr7N87W7mpd2Vr\n",
       "wjWNE+P6cFo1w1nk12XKuqo/9MYRl+0oclq4jhvf8SEtkK3IRIhvbDUETao/VJ5ibDCcNMYdi6ds\n",
       "X2mLB+IbcY0HwTke26sypY4RKUB/OPhXQ/tDkivllFfSJb2ameLtUIyMefLPfSM+72rCtF4neiyA\n",
       "AsgzLgFDMf4zpGPcd08k+NOObtKdN5O3spZMRWeqh2PBkQs6/7R0EYx5dJgfJy83mBGt7X7sOvcS\n",
       "KNGiP6nSXO7TXmJv5E4mad42ciDSgD3+CjjwblgKjvFILFN0a/STT0gyG1ciHza4uBEg89Y59h7V\n",
       "0MTSl5s4RA/rYp52BSLtzGGY9i/tR7C0b7wf0hEFfI6rXxkBmVoNiCrryJRR5lu59mKGSlTiszJe\n",
       "Azy4/h9rkey5825I7yIEwCLW9naZDYk18UHzPs5l3dOFfy2oty5Q40OgbjB/qAtMfBQmsSUluw2x\n",
       "aWgSDb1hAQZgcoPaG7AmsuELb+dRZXfB9RtaZin3SEX438h1G5PUCN86DocYhkyt8jyiqsFCkLqs\n",
       "8xsWyBup1B2g2E6m6hX0vYWNfGQn1PWetXLmMNBILpVy6p1P7fsTL0ty5oUtJ/DpT42nxnI0n7Rz\n",
       "vGHWjriD0uxBZaJxucttEp8+8jKG3Tlp190uBIq2LVxpnzSJ+ZsKmxLjJy9RR+fFzazi89zHpttF\n",
       "EtrALw+aBPogmBR2tpYjaiFvxpk5MUO+40yGIMXUwWEyk4Ib1/iLo2PtdB/slquFRRaQg1X9+3y3\n",
       "Lck7pbdyyprzx7lvsm15xFtocXvrgMw7REKIku9mXbH0DRDH22jLXEIQftlu5bFA2giMh6JinBUB\n",
       "EPQoSAsyO01M5pcgknmOaaB3TgGen8peDqgWsmnBFkYX9d//NGckQoe/bZ9dtSgLDox9fDik118Y\n",
       "+TY02tI9SCkEptO05YX2sew3MgdQtXiiMPwBasHVEVcetanH1CMyvkWZM+4ZhKI+ykbv+EtH/9z2\n",
       "XwR21KPbKFq7P3okhz4Oayz79UhmNhGFyWudzd09yNVkp+IavWZRd78yVPI1Mkz5BsM0QElzYTsB\n",
       "P44QFkEj769OXF/XUpzG8+hkH8ZBIvqzr6sLac/lJb0oYJxUIpMfczOVsT5+3YmjgJDP9IVzJwfr\n",
       "06EqR6Cn690eRLbpW3u3M3g5t5iqF6i7lcyCB13kDHjp/WL91xSQs0AmPMYFg/o9AGJSIRbuil7P\n",
       "3StVTrSE/ONtV/AnaPQWaf72a+v0DGRId5arBDqh5VlxWtMUQiAflvmas2u3h3/Q9L8pmAoPGEGi\n",
       "dKLN94QT1kL8pqbeDFsLPisl5/iOgWBevziJxzBsW8BwYAqzlB1uCJyEblcyKy/L3D4JePXd+imU\n",
       "ngdUlylI3zIBGbdQDCwOfnW7zb6sv3V8ZJ2NnjyHEYnvk8rNdk2ZG09wtYXT1D1Rgaxt3cmnQmLa\n",
       "5YdobOM5jRk8xKJ83lZmJlBVT+19zvMuEKS5wJjdvEJ5S4LwN5CVYSC/De1udmpkepxSzgoGUCO8\n",
       "y2DiK6dE/qrQqqWuQaFZkg/7A34DFN+uxItfIsyB701FS/b6XTBt13yVrWZ8ToDwA4wNvRFAoPgR\n",
       "hweFID1JHGfN//l7GCTp6auQuU7QCUvzGZUTZAX8dYZcZBctbdIY1wG93064Ug2KPJK7FxgSVwPr\n",
       "JTGok5aM7kcqdrRhDwKlh6gAqZGzdNpMgONks+Mweta6d6+2t2Z03EafUsRi94lgZRcSDzJeCIT3\n",
       "4Uxy89czjN56RKC4RI/Dx8JoPMpIGvTmEiyho4Gme4u/D47p7VDG38rqjYa2rO8VndYMF9tSf61G\n",
       "t0fM+M8FqKtiecjymQRVVpoKyf5XewF6H2ruMzIQAEviaNcul4ww9SLGnD4ULZUdDe99btliDOcI\n",
       "R1kAoQlY2dRCCqhJ8XKz23AySF/usH8JmFTXPiMtz+tmFmdRoBOSNg4B0GgkhOYYK41wgxGaylGi\n",
       "YvLazzt/SqDHrNlJKo4hmOrtxVmcgWKKcqjeowLGaMTLGzH7DeXRdePjAUhPvyojBDFGC/zNMXRi\n",
       "Lzlt24QDAmSIb9Np5VhzUTiizT5ac8feP+18RCgba3UHeMGVy9zRjzo2S+iZTf8/YEmJAk59ZUv8\n",
       "p0T77UEgX889djwm7aXKsQyigdtQgz4EnQOBlMBfxiI6i9T3xXtkNgey86ru70PHsZmhDb1zGfbn\n",
       "WdPfGxtzvSlHheNJzM8rU+EwehvgcAaz4+DugQAACsdBmqdJ4Q8mUwIL//7aplgAlNlvTABXTgn5\n",
       "fX+r3mU0iHLbGOaEe17Wrc4T0Ph5hJdxZb2MhOVdjgVdtmxVPkILZP+h8Kk8hFf64MnkWbjgPpk7\n",
       "s3iZzfCqr0ze6/qGqazij9f6KaophO3cHL7mb/8bQ1+sZkOskJW45wUj+pbm/weKngy4RsBO/auJ\n",
       "YtqalvIJm8YByIZvoerTOvWHNaqcd7oPiGvY087LNWuVPql5G68s9A9EMxUKOxnGMMHLHfvbwP0Y\n",
       "wkwF0e/xXN5uFi07vPAiDvqf5gxjZSjW4OMqgCI16G6ue32UJCYBjSMttfGkqBQgank6FdjWiTDE\n",
       "U5aVcDj5OD0RCPRd9K8/hCJDJMSrlvxfOTMdio4exqnhvb8uStEL3GjIsbNqZB79Bw8zWbUELIET\n",
       "8gUBTb+zXOiYiA3EGVVCrUJ1fNAF769xzK9NSZj6JYxeP+43Mm0zxOmuj3uuJQI7k5jIdF7TY0V8\n",
       "EYYGVUpJ7rhM8ms4GrOZIMwjaWvRBAVDm52TQIvRf/50d2FQe9VAHG4mtElknTPOv0Lieq59yq3z\n",
       "bQqmugQchOishr0QHQt12EZIJuQwfy3yKQtfZkuLxqQmbjLcWzG/tK/hgW5oEGrF8YuhClr/Bl/D\n",
       "yYoFd/CosIGlSjwY4FKz3/np9N/XKW3oqLIOqmflE67PejMxMvCSbgxeRNLFTm4Sc5btvoG9oUsU\n",
       "bTqhl8IcnysMBdZeuNaLerBb8BcLty32dYfM4529OMdWTsvwe1xJOkyKOSpQcPRJHRPOK7ThaQdV\n",
       "agVBm9akHWC5uScBQNae0c5GMNFGOBbMPaVrgrWq1o6JDqMRup4udJUCafBkX9ok7sNhGfJcAER2\n",
       "vI+cOLn1lFrbl+6j/gC1WvLQpHKf++y3AcHSFN/iifuAuLph0d7F6rCj+juvbWOgGQMVTbAAYh5S\n",
       "Nisf5khWQxmZrohFjb+tWttTM2VidQrUNeH7YtUaJ/0uOhSxVdL9uzG0YpkHF5MZDYBVRrMHdBwq\n",
       "sZegqpSxoA7kunxgOwEw5AcZJ+nDwMBK6haMhByHBteLDX1G8cnZB9Re8RkLAm30LgSry5IgjTaK\n",
       "IjZVV3DeqvjIDc0asE/m6/kA/17EMY+RPZv/0otGb9JWcTMkLOSiCSB96zrXSauzvXrni2oKkcmJ\n",
       "fEjbWSMXJzu1u2XHu42EVIV5TTczpMwplFNhECsXYiSvg3835Wm55lcSfYLa/hDXXVZWF/ORUwGR\n",
       "6mqvmPy0K/RhAdMSWWon/XOOAwMQaTC52u04GDapX0dN5o+q+OEFL4xO8ac3vR/zB2MiRIj85dzk\n",
       "xetUet8weWIg1WIgUgWsjRK7W2TUbDiaNrKSdj6Np6GsyL6EDGzdxQdF4GopeniD+QaWuUikOIOs\n",
       "zjPpeL++yHeEbq7d1hXzUeWtKgTkH9QrpMW6qzMSthF09NBv5/oqDaZY/he/JZsh9uok9BqGXn8C\n",
       "rSyLiteCFF1VuQgp/SvbsvOBNy9LKoHAMtNUfaeqVIuNUoMhLkCZo6+iK2TVbh59KkQycaI9ptPm\n",
       "0S/JbKw22i3IHjWKDaJ+zwIBbotCFcvEr0Ym3EnMaA9aQ10Kes7FLp280AVh5+MAf1vkRXsb1oGP\n",
       "60w0qTeXwCPRUVozSlap6SOZIPWidEx0G4a3kILT0jLsWI6QXJSum+HGZXsLg+wgLQiIIsVTs2wu\n",
       "SkuXvA4h/MOsgJAubnysAutMi7b5tetz6paAFnNj4UcJOrBBlrHaXF6HKEQiVZeTngtPbi1xJYXQ\n",
       "dXlnmXlBry7DtVH4HY4n9s7PLmlrftVKsaWA6RETVI27R6sGf5VfpoicN89CcSE11pc2/sstSDxv\n",
       "MU+aSGnQ87eRQRfWr2AftDV2em4yPOn90MpHiKc8+QzMdo+DfF53O+sfAc8Ydzj2uyFHzOmR0bVz\n",
       "Phwn1/y7YBoNdqYGiKPXfytxPShTC7FpxBLMexZW4pqGVPWwlDzbNb5wbx4BzdDkUdnZBRTUZ5Kt\n",
       "reE3btlR3lfFqqUyBcRcjjmyUC0v8zdzROYDDTEIA1i1Yy1PvZUnz+ILx/6hFzaqBR2PZ8MFIdex\n",
       "TmO3iS8rvU41PmIBLx2w4+HVKfDf4oBCJpCHmoKzyv+GGVts7nWHp4L0uMEmXNUALcDa+fb1q/6r\n",
       "GT96kunFJTnPh4nyr+6EhBo+HTGe3m0wP7M2Debq6qDZ9LmBAa/aO9rKnuGYMkGI/4adVHPCbQ6Y\n",
       "/li3p4g0akPjGxBYGOVKwxjRd0s15yoRky3KK/bdz7S7cCwaZx5IGajTU6HVjjL/hvpDyRHvtMMr\n",
       "zFPFr0fw+JdQB+an/kdR3Li4/wjnMBRgNF3/ejkXa4kWeiXabS4plb2QrI0RTle/Bsz6x5QAE3zx\n",
       "hklaf6mPra+6is5pp9O6AN0Gp/pDhBtdYWk9Cxrr7oQpj13OnYzRyjStRLBaCfqwaiSWUO5xIFmJ\n",
       "TWMaizzeQvsv3IcQZJhc+eP1SBrOkjenDxbRf0yZaA3RSTiYYBkvai1sFemp/y1mJ26gKb5ekzj7\n",
       "YWiY+s6Zk6R0BOzbjJSKIcik8UX0mK8ub6WCIJ5EezWR5dmy6cHn7sGNFDIRmYUWxClhqRRof5Ws\n",
       "KrL+PoWVxVI+XGG44C+vQoV6YdT0rLik6ccBmZxRumRWwMyjdKikJUbR3rgsFmDWEgO2aB8ARDlT\n",
       "M9fgPTvw5ZK6AD3mMzfa8Vv/CphikimsUCED8/tRnOnlU22OH23XcUNsVvxkNuFXocuhy/De5gMX\n",
       "JVGk6oB9kXCSY+YMWBf87FI0MerNVWVUCMF8yhWsjn5OUWlEYoNI9CP9dQhm8l2UOD5URXZ76kBY\n",
       "cO+rojlwtVr+Ssdk1e3ntYhhG2A/umLySrpZegVfJSdK/QtcvMEdPLxvJ94SxRF8CjZF18Fb0itC\n",
       "shEr7CNxK0CYzuzN22fk6Q4T0s3WcyPyThzXiwfDmi/ybgw+ZHp7nhDcWBEcg390qsV6LqXzvYia\n",
       "146eNaZ7ZJ3fyXyC2bwWtMctvrD1nkGONaKER2l3Tk2L7ochT7ACozYhjKgCdDRa0H4WfEcIE/ry\n",
       "6yKgAA3afxY28abIoyW+bmmPBOGT2xlhm4FwRRw0ZLiaJnFnJG04lczG5Ie2MuRUZZlT81AXJZEu\n",
       "+1tOaoTy7rgO90m04n1SVXqNkgXHZQlP4l8O4c3RcAiiokJwSjrmWlFlGDKbCFms8RHGOVf5ROs5\n",
       "dPpHz2FyjdPMqyfDPf7OZuVLD2qrs4Ol8jCaM9W7FoD3LlAisLlJ5lHqeZx/yIDauCAIhUCs+4l8\n",
       "zB8uFYyLDNJBdkKGwzArcS3MbOPzuJifMAd0bGfAJwwxpENA3xkc4598maD3vKlYwGhsbUhlLmsS\n",
       "jF/woMC0H3dEvK1yRZqB3iFX7cMeDibvfoqYlJ+dv77jzsiBB4xuXNmK+BWeCRHoOCnlqEMAjVy6\n",
       "e+vrA9k2DO0KgXuUJSluKBygPAoifuA5Pnlb8coh9uR1QZcOnSCcBAoEtJMpGkV3sQpkX9W0s757\n",
       "+u2SO6NyKi8RqpU110fSB+VD03K3ZIf4iZvizsi6sKNTLx2ownyP0GEpO7dIfycTPbMJgZBFyZqK\n",
       "ifMY6Jd6NQ+I6P+IpohyjYb/Ah885DzVEXcclld1xJa3Y0BwUmEqWrPLxabMgg6CBJhUQKoG9QAA\n",
       "AlFBnsVFETwV/wAATJHKK3lEqFSCJpSNho72r3RteOpHoQgCvRI/R+MgTi/t50H3puYRJ4F7UyCU\n",
       "8x5G7kFZskPFDRw9RWsz5CLC+YE+uJEhfsau5nRLEqEgOg7bZU1zsvZwxoCo1L5PcP352GyYKcmF\n",
       "wKoEQ5DP58xW+C2mhA+sRi/vztYrOFuH8625HC5TGOZOryEiXibl3nwZaFBzmp2JRxy3rdaZP6ji\n",
       "f9/jd472K2WGUh0PVI2n8kbfSEaF0iBENaNDqiCUG5j8YpgeCvjXKwBvuwCfWoGeOQjDaIu+MoU1\n",
       "GrcAYCSTnV6nTCRbuPhARM7xRn45nQURXifYgDkh1nVSkFZ6dbk4V5TrxtlXoO2Xv9Q4I2TqGzy3\n",
       "XjDlBj6NjEjrhn/+CcE4H1l73BvYYPGg0TXvbJwXrCB5nboTrLJoHJ03JWvG/Qfx3P6TntFWq3Ei\n",
       "rmmEZTof7XLKv9oPO0L6NMPDPFRuzRbEOxh7mRnaTttWSsu0ZdGNQzq2zLzbkth5YuZN3MNlqzZc\n",
       "qqu+DjWPB7J94/M/POF/WcZvpjEIKoddJRKxhBIy0G7fUlFhsbpAoa6J3IS53Rrti7LIx2baY4Hr\n",
       "v+6YVVQICqjNKNKGJtdxSzG5pjl8mL/KbMV+NMjCs3yB5CoDrCHRr35Crv67qANHhefAJhIdro/B\n",
       "fovys5GZcUOIW1fGALGNSaFAmu9A3h1+jXtq3HdrX1Iub9QlN8LQm/hUmNQwA/EF0RMQBkbsebjq\n",
       "i40lWh0nr5ouOYmGQ4y9c8IAuobASNRZQQAAAegBnuZqQV8AABWCkVwgDXvW2E9zke58PH+dU25p\n",
       "4tG+Q7ZTU2vaA30rfPX6N3DtxyPxiHchbSOOacpYM1P60f33GrpJLr126TO+CRu9AZ8Sjulk0+DZ\n",
       "OYs+/8cqx5N+ZTlZ5mQ/DTe/OAiF/HDTCTq5V4SEVHdV/BBsBOCDWrXoH9xP9Qvgfdw6EPSrMRU9\n",
       "4ff27/lnjALnfuAYoPAfuZeYUZXHWbAX3fIGr1Wr41rIJ8UqcmLZ0DXH1rZaxvWX+LlHcwKTAXws\n",
       "ySF349s7u8ks91UeGcMi05Dw38FWMvR8sy4aaAUIEq3yq8ayruYJ/qMfmzaFuwfa7M7mr6CJ49QM\n",
       "vWr268sDmR0POh+Dw55pxZbYF6gpJDHxXOlvE6NFC0H0rA4brxAT4Hwrg6/6aUIL3srRjKQfoePC\n",
       "ivBC8+y5tQEnAm4iWs/YfC43oiOKUMAQK1oraJquYVlfKTzVk++0pq94s7+mDRyENzkGn/OENGUv\n",
       "mVkJ42wSOwPGmcB+D6uecg3hPfFapFvdpQHksfSYTUEqaff3NSfm5b2Gd5ttBUaxWazQEXA2/Dtd\n",
       "koEXspJmi24j7IJc1xO+kLvg/DhD7RJZbIQuV1CDulEwPtt9vF45FSWqJGKJX7wPRxBDZUdeafbE\n",
       "rzwwIQAABYRBmulJqEFomUwU8Ff//talUACU1pIGAYiFNHBy3lup7MEqs4+E1Q8mSWlDhZQD6lOY\n",
       "tXmZ5Jk1BrsYwga9TQxT6I0uXtsAUI5uEnd9Fu31JVFniaJKCNIv/g7GZX3p7SmIaHWezuZ0r2lG\n",
       "dc8p/ff+DjIX7N07vULKVeVTvkgq/IcloZKkYqOewh/mS7pFvX3k6gUPCVA5caTFGFVApLKb6jlN\n",
       "gVT3uHIck3lkdRy5yEiTnb9uNX8bFzD37h7RaN5FLUtRdlSQoKsQZ6WT0bcwnBeQxTpki0vhkBJ0\n",
       "CzEHxyFrMg1FQg6W8bqhy7DagorOiLKRKxypOzex23Ku1q2X2STG7bmEYhq7XI07y6EYekNQsZK0\n",
       "VZwCWKe7P26Ny/vwNhbFTeKnNW4Xpt4uPvQIPUj8ZGiXn91poRNwTY0duQzghYXbkuSQywVN8hVL\n",
       "F7LEDF5M6GqHeUKUzEQqdfD0NLj1CPRchzy4qywkK7cw87fv3HqofTiQe0tLcBOIcFMSq8Rntl0P\n",
       "0C/3qg9fwBb5gjxXeXwzj0mtH8NBCtoAABQHfua3JaoT/wMgFPj0Gw1Qc4HuJs0WS9eWVEYUwRuZ\n",
       "ugtKkUkAPSKo5DbOf+vUEd86lex+ZJMJ7dDVDkvuOlw4GqgCQ7Hg6YFlaJhqEKBpNJqEvcabKJvF\n",
       "bUrnr//q7farvkMNeaSCvUovOe/sglkwF/or4Fy4EeOGBsLDMAwk5SPTBvbdIr1ytu2dLb5OVQ1l\n",
       "fsP4sEOmqY0JM5nC/7Cl8N1fo2Z4bvjbIiJapqWAi/2HTYDfyB+IWTTV83/l5XOkbMMN72Wbw58N\n",
       "r1acZm2EXU4P4bojy6buTH+AK/OssUZfJhBdO4QRROr+Kdet+JszwV+YIs03NtzrfkFmAlXIoKZy\n",
       "VXnuFc5SBB0UP16AJVjGPAOLHFBxNp4C0W+KTebJW4xUUqRpXX8lYvIs4XkhbbhYyGnM8C7IBB+5\n",
       "T4odHRagi2P1uSJoUr7S47gC5Pjawh8/Bxeh9qnAlfgb71/On7fy11DPYiJGvmMrWOkvRxP5yyv8\n",
       "+VgsgaGNOelj33gJ6ENs9VYR8J+O6pRjj8KocctqYNY61/sdC63cnthk6hAIEG0MRmCHWZD65nRx\n",
       "Eej/e5JPyOFAyJXMvge8w6S9qJxpnZcUi+YinHwx5OzYU0l39dmPQT0yWZG8h1cp1w8eOTwnajL1\n",
       "kJwpM4cqmi7Rjcyn4n6qY4tAHxZQsO+yCglJtlLBi+YZwRfxxOOLJeXnMoi4D79bej5Db9Xgvh0U\n",
       "i46kiXe+RTcQtUDtZEYr1JjYozH9R6kwPKdVG0lccR9NXGkxWrCZM/YlYMiRgSwcrTeL0nF7ujHE\n",
       "L3yi+73Ct/lNNWodJiVHVyIDL0tcTwOJ2zqzDhs8LBJjnyIh55Qhvsdbzv+6QB0AhdpYCL86DC/r\n",
       "UUW4HHfoAGfOeRZ4JLg1fUgxUJwomldsPhTKWDwoZIPeqT40tEy7V19MADbM0y5QnbQsWA1bFH4H\n",
       "Mu/q5W7hsM2AXZGlyAbAmqMjUU6ysRPAv7IlicEM03cC7+KC6WNbUYqmjmpV+nsmJPSEZSPpsPcp\n",
       "Tf7mikqazJ/DB+YVcF+A98AIEvNSIU+OEMzNxVc7M6L6FUKDjKI5POIP8Kl8IkIVpmvFx9k3i29p\n",
       "vYSCAQjHaUZkqDBeycHW8tSboXH9fksxE5A/oVjLGTed88NsmkxKGsqTjoT3HletsLxwv9LgItXK\n",
       "UvgFbUkHxRDG8Jbx5cRKybgs0gcRrZIzNBcl76oSvlw2y5QwsNEY9JiI2qF2Mfh9b8AyVMhA1Bn9\n",
       "0CssafWRARdQjIuoM2FmX7UavqZEPXSX0R4Pk2NSWTBBTKAeUsJ58D82HKECiXNM6hA/wAAAA2IB\n",
       "nwhqQV8AABhraKmKUt6N0AWR62wnucj3Ph4/zqm3NPFo3yHbKam17QG+lb5wbCkons5G8rRIeYrq\n",
       "iAW0jjmnKWDNT+tH99xq6SS69dukzvgkbvQGfEo7pZNPg2TmLPv/HKseTfmU5WeZkPw03vzgGeu7\n",
       "63BJ1cq8JCKjuq/gg2AnBBrVr0D+4n+oXwPu4dCHpVmIqe8Pv7d/yzxgFzv3AMUHgP3MvMKMrjrN\n",
       "gL7uwLaZMZa4g3S3OeWztY6Brj61stY3rL/FyjuYFJgL4WZJC78e2d3eSWe6qPDOGRach4b+CrGX\n",
       "o+WZcNNAKECVb5VeNZV3ME/1F2+2WoxL9iwIy4v1Ldn1LDcnTRh6HMqfW+FRppF9mxKNQblzBa7Y\n",
       "92iJa2gwsp6dGihaD6VgcN14gJ8D4Vwdf9NKEF72VoxlIP0PHhRXghefZc2oCTgTcRLWfsPhcb0R\n",
       "HFKGAIFa0VtE1XMKyvlJ4nmd00XLvIhfdmDRyENzkGn/OENGUvmVkJ42wSOwPGmcB+D6uecg3hPf\n",
       "FapFvdpQHksfSYTUEqaff3NR7MtKXOCiqvYfULcjVM2zam/Nqj0W2/rVFQ/2UGRCbHWoZCm760OV\n",
       "gtuBd1WjPnf1jHKJOCxONolJNtAk8VyV/2/8bIaPsmBXRDy0n8KFcbI98wVPhYhrrpio/vPlBUvd\n",
       "6rJR91VVgcbLvcVxiMJp0zTupI+PWIoJH4OZLlaDgZdYHQs95R6LVi2GL8WodjiAQSP/Cm6rMJsq\n",
       "3pAgjEcf3Lj3DGDB/KJOoijONGEmh9VJEGuDPgFd3rw4MLhGkLYy+ZnWlo2T5Ok84ow9cRWUIMIW\n",
       "bMZB3lUCwuYt2aPfjJLjTwNahMBwZcMzVLK7onPhteLEeRez8lXroyx3/jeNLyLpP3RmmnLMdYJ4\n",
       "LHlG1k5xI6kR7T9jXjmQWFGfrUjDmoX7wQx32wxnJE3KJTWfMaR68MQLIbOOStkZLGJXgU4xeRH3\n",
       "LAGv/SbEtIfd3j8+l0vkBgKcIPUzpBYF4utrnPD9Hd5Hqyv3/dsGbYSbLM/uW1agTfxhT8vM9jk5\n",
       "tAaco6JwCqvt7hMg/2G9+gcEyetfimhELAKwkx/AAVED59BpZxDl8ZSachmloH8bG0QJ04mPNwwA\n",
       "rBXLUd1eRhug4AAABgJBmwtJ4QpSZTBSwW/+1qVQAJQ8hdADbKJT+Oj7tdjFCICoZrXDLHQMbdZS\n",
       "OA6YMGwqzIhgTOOnydtdNSeGi7sYJ00C59Bul5WfteIVAfFbqodYtKYmJvKLCjw0fefpk399HQr/\n",
       "XpXNsmiFdEHgfiKYNqBe7TmnApwoavuY1G1fFzw1nkhsV18isQnie3pia8Dpb4uLfUN22+qt19IE\n",
       "qb8go5CEPYHsSLtvSxkLVx0fK24v1hKBrxI9bIesZE4CUZdgY7Ko8Yqhq0mALQpvuEGMRfR2NCXH\n",
       "oB0oJh6iMouhR8yW7+ze3itOl7HXD2PVqs7L2bK5RhS6EwA2jXgl9+c5G5wzKTxEASAaOp0AZe73\n",
       "kMuzCQf4SLQWaAiLf5l3eAV943rSbMcGztF8uq7SnDDJM5OGGaJK0qjqVgU1G7nhZGLX/jljZDX0\n",
       "V4GjXVA6I1F7fTBd5XQgp+zeL9YO8TDXSeBaYODcxEX4FuaVjnQQ3EDrIk0k7i4ceiUtR000x5PR\n",
       "VLdOr0pevR1DsLGSXAr81Cle/MsNCyS3dOZtgHB2mKVMZQOwer8aDVupz7MqBTDXffO6ygVxECym\n",
       "IKwz1hMjzYxm2OacJugXfClZakDBy+rRUimx7cNd24yO2hejw1no9RLa7qpEsUtDOYdwB5BcqqzF\n",
       "eySWtfuErjtX2HPZ3/8W6akGh6k7tik2n5vfUPbXem4pf6WYZNtAqCrxAUVQHfdyNmmI6zdLN82c\n",
       "3xp+IeBKEHhpcHaEctX187FhMbN9Sk5BzyOG4uNKAPvHrLpw8SfRPVXC76mKT52FboVXgg6eSXxk\n",
       "oLRXcCDl91GBvBi721O7EEHm9Mn25OZkd4lv+Bd9q7FrEWPkFXC2wFp0OmH885ZjMcyjh/Vk3RP0\n",
       "dw3ytHhBLR0Vw9Y8LGQnDzQfFMQDQey5k8s44+EXsR6OQ9Y09Q4LfISR2JpzdIesJKozHML9CL8t\n",
       "kmHN3W8j+f/su/rWjPG+Dv/dEqs9SvSay15Tz6Znt9qZEWkfmP5XR7QwaCVpjickLRPTk5cdft5F\n",
       "phDEee+FBfWS/HCY9NnWJUecjR4eOIeN7/fZ7PtF6NghVA+xPvwGnVbuLzl+l3lBrsS44jJyTFbW\n",
       "b5KpTnoRMQJug5FX9iD+s24qOtGjcIUq5iP3TidRZ+CEir3hxWpZQ5lhXhZ8Wewxa2ZRVVH0OYLP\n",
       "TqrLJEoV4aqrESu1w6xhTtkn8c0D8TTOSlZj6lkss6eeDDvMxSbH95AAhgE3DNhjdWBwViNppadv\n",
       "/L+EiqaF+6VHOdWBeEg5tt+rkrewlanvQ/lGAql9/ILjxU0wZFdfXTtyLTbIvgezj5jg0vYPgB0j\n",
       "xmjSMOegefChtE4Wk9giUgw928tVOG+M8TyzALvYMTBFtvv+9HQjWSI98lU3wIv0A3JuXt0/PGno\n",
       "zWqDDW2Qlb8UjIAHQskZHRskJDUGB1RQGXJb37zNZ6I7wIMD5JHSJBTnGPQYK3wQWLxXNZlOJXjd\n",
       "Ruq45Y6/vuDoCaFJDN/Omhx31OtBnWl+P0PasgtksS6j9nfQ0HiuuBRI8TekSC9rerE0c4fS/7NF\n",
       "g5rTiszxAlVsSH4NAg0v647rd/8ORXhu/diz0Y5oZApaafnE0AuE6Oph6zgSMEzjJZ7YTESaWyfz\n",
       "kVt6C+NeRnJKYLRY4FCRsUL/czedqw8b6UiVsVTLSdnbMdCl8OEkJAKxCab7ND9Vcr9xa4IQSZyS\n",
       "Es0hkYpFQ0s83yAwZtNUN4W1bl7QlMYXsWLWV5yTqPkptzQwXJT3vP+ti2viC+5K2zEEwPQx2g9I\n",
       "UJQK7b2DRFRirpZtkItT0j9gNMB4eZ07/PTXegxLv9V5C+WJq/bqlHhCmQZrV8kk8GfAQRKY8I2G\n",
       "3hDHvFbd9dQzWAKmt4AWQm7DoAlcE0k9wcTbFJuRuZoCqNlSqqfSKLemHVWTLXTXJm0leE7UzqgB\n",
       "jma9fPHVr99k3D1yP9uFV5RqLHwQ1VKaG/nRuNuCcv6VInM1GWOhNmGE0XR/WP2jHoBfsyGLfexg\n",
       "6+cSWmu6aS2xWiAS8QAABWIBnypqQV8AACOSLEcMHv3aYT9nHXQADavW2E9zke58PH+dU25p4tG+\n",
       "Q7ZTU2vaA30rfNMoR4duOQjyzZPhTyAjjiWl4f53gpYM1P60f33GrpJLr126TO+CRu9AZ8Sjulk0\n",
       "+DZOYs+/8cqx5N+ZTlZ5mQ/DTe/OAD8kvrcEnVyrwkIqO6r+CDYCcEGtWvQP7if6hfA+7h0IelWY\n",
       "ip7w+/t3/LPGAXO/cAxQeA/cy8woyuOs2AvvBrXlJjLXEG6W5zy2drHQNcfWtlrG9Zf4uUdzApMB\n",
       "fCzJIXfj2zu7ySz3VR4ZwyLTkPDfwVYy9HyzLhpoBQgSrfKrxrKu5gn+oB/5tu0YAvrCsCMuL9S3\n",
       "Z9Sw3J00YehzKn1vhUaaRfZsSjUG5cwWu2PdoiXhGKAm8To0ULQfSsDhuvEBPgfCuDr/ppQgveyt\n",
       "GMpB+h48KK8ELz7Lm1AScCbiJaz9h8LjeiI4pQwBArWitomq5hWV8pOzYHumi5d5EL7swaOQhucg\n",
       "0/5whoyl8yshPG2CR2B40zgPwfVzzkG8J74rVIt7tKA8lj6TCaglTT7+5nvV9brBAKkWFdzJMaBs\n",
       "6kVk//i3PIiFbRcH8Dq9SJobk55cygKpu3Tzf8nOE/Cc/wkCJsc1QyD8hDowfdqLZ/+Eh4hw2QmI\n",
       "Y+j70MpQiqWY6lGIlQwzJ2coaiwulLkkL+BnbFoetUalzIlcpOSepBVUblw+8wkZYi59NXO1HVPN\n",
       "Ivbi3v/rHHkcp8M0I+kOWJSyjgr9eDyzty2M0vosiXTX8mObg4RF4fqq3JgVW8fawrSGiZaSpeDV\n",
       "zR1SSJKFbO7T4h92xozkk8IIQDejl8cMNm1QseFDxD8/MiNkMXeD3fvyLBY4CEEip9tmRmj+09Mj\n",
       "vsJswYwzAj3FpNLUgb8uQkwRdGwNJqT42XCCIL0gu2csN4jSMJY/fOnl1F4KEt9cmLg28VOHZhrX\n",
       "7jIny6PUuA7F+liZDHH+5t09g/UaMsfHfGqcRXy6gYN3SP52Mx+9NUzMsqQGWnVKuceWzb45yxCv\n",
       "c0q2hkxqTpr5Oi33WmklNudOK3pU/VqW79ANp+OkU0Crc+HNAuSzUr8s+GzZv19mnY+7m8Mp1rH3\n",
       "jGLdn8ZmnS5J2LIISIu1M1faHlK/MRPfoJQMpF8DMzVvLM31Z+k3CMe4THOW48KMCNdt+vgu3AvE\n",
       "iuZ4WFOyVnAgdaq4NDGMPXNwOmbO8KJ7p2ZksOt0rV50ivVH9pxezoH7kIYjSa/7Q09JJ6KUYkeP\n",
       "r0LvlIQGuKJfac22rxn1JzCFPoVEIYpL1ZRsFCh3hgWvasBAl3BoAhav3tFH6pHpqBCZojg/yCSm\n",
       "y5sDJfDEpy/1Eupf6jbZQykAFjCTpFCfAF6ddn6A06tpiXm9JY0VFMoYAtJipYRdOwx350CX3j1H\n",
       "TfB0MLqzaT1WupPHfP2IKWmGPIwHeGOAEfAlqfbdtpD5J+6pi4NT1wavFOsa64Nv+4V6pI77yP4f\n",
       "XSJ6HxQbKJPnpmzDz1oz/ah3wj60JFUw/qtIqMX8GdkyQa660hupwDd0LEX7X02GaBmBDSMuMARq\n",
       "A0XpVkNkTq1MX+p7mMCRM9P0mco27fl4W5IPeYm/z26oATwptIgtqjdiwC9CJ4h0jsv3XySOadVH\n",
       "HifJXnV+7nO68wbC9ZZQcCSWx84ypqXyDF3X+hIPt8Sr5SOXO20iecyHC9SI9ozAHuMU2FvD9VC3\n",
       "ZEScctrEDdmvdn6NOu433Z7So8afBrDFY/nQ0I12aEeBkxnwcq1Tfb2Ja2YfQz0GWwl5vEGXxkG7\n",
       "rhEyyuhTsjNGwH6kKOd1tpbXZxAQjkaPzpf8AAAIEkGbLknhDomUwIL//tqmWACUPMKAAiZ9Q6Bx\n",
       "eGwHOa96Kip0RC0Pu/ZJdEpU1uzlyeWJueUJrWxPWO5kvJjs6L9BF+98ko0SZnXfOq0HSMskMdyO\n",
       "3zXea5qP2jEoYcC1SWUrphM8Kass3Fawth2lJU13ogqwhNw5ZHqDd+5vQgLhjavMUEMqMWSfmmbY\n",
       "kCTYh/4+tRd3hHk2mgwR//w7OAeg8gZRtgk0axQrnL+CFxINhuPaGG25f1crjCfr8iHSf5FB81tk\n",
       "8yjyGc6WTZ8YC5mOCBD4wb1wZByCPFUOa1Gexvq8Zex8OJI0OEEM4A/akv8DHh1uYRdIEJ53Ishf\n",
       "q5yCH5g5DwfIK/r0WrspjCUhuaJjSr0CJ1qbJgi5TefGcB9we5vWB9SBQdt4rexsO3IKlGH0b1GX\n",
       "9rMcT1iiPRkRw0TwtyLm1m3kw7OS0XF1wvc9609OhAuP4YBflGd1RqJn044HIglBEIAbABpdtdyI\n",
       "I5j0qvFvV1wtX4IIfiQgyUGh7Gf7yC1pO/1memJ1r5h1xQI/4mrdY6kBzYG9oux3JIkGcj4lA8W7\n",
       "Dvtn62mqPiWm+wBo0QE9PZ2AYv1TckzTLrvOmtTt+244bdUogm4Wp4wjKu18veLw1WLOzHHwdQbo\n",
       "KZNpzZQgYYH8ndrS83/XGsQ2OHdXL/ZZISXKOgOY9e+K37dE9mjBCj+hBg/TpdnVGpZE1GtzEl3q\n",
       "sMItjURD+vrWJCDSS5+q47mmM13MqQcPRI64ABzr2V5O+48iIqBt3V8zSbX17pC1G26kBeY+m2Zt\n",
       "elFB51MS9VFku7GdG+h3bl9wIpc387V2oSVgh8xEBvGFTp9ozUV3IX2yAX1vLuhLdfZV8w0klcyh\n",
       "LWkINLwU+yzUDX7g5KQ1EZX3B1ymaM4vhheVxecLpjR53PcS/ZrwUpdntJ+aIZDsBV4QQVBmLu72\n",
       "6Ta3ajpACqL2r1kuIn5do3CZ1DXWykCDxfDxg5rTOrJN1tMOu6SPwmzM0XNAXiRPMK3fgrOTZ8fE\n",
       "TGRMCQ9rE3eIp6n1XgiTEDs98MyLSAzcUtAqLeRwZaIiiybG8uuP+RkBvB2p/Y/iNXjdMtPLK7uk\n",
       "F3dHem4LAGoirGBaNkhZfXtRNEO5zXHDx5DwVx4OW14SNzAuirm4PgXfF4ESI6Fa6XCAJJA93e+j\n",
       "IUng9xb3FsyGjEn5vMcuSOhP0NxAxFThyClAXS5wVleCjX2HAVSF8o/a/bd8nTmesqSjBh8vdYGF\n",
       "d7VaHFPeqwa/w97QrhSJGSICw2ml/Ezi/CnnmZJuetmLq/+X5bpyz7dWOYn1vaQRG95zRZXd2vv7\n",
       "O1ssyZs/7ippJ1Jgul/3WZszhjZUO0YgUbYk/P6mALTcussGHHwcKwr2cnpR8XKBVoll8nd9LV3R\n",
       "jB2dHWzAeGCdGJIAXm6BTjqT5LGO4ykva5RTvQ8jliI1BDoWoVvQ2p+pq2qJ48ssp7Q4m9frTpMh\n",
       "8k8lTMhcf3kiunSoIxqneYw8ABP3sGGlcxGe9eoQpOi22ORMclyaGpS4N06KoOh1y6meSqomG3E2\n",
       "o4nytBeydrnCoi1pbgtjMUZrSjoMcMi8Pg6Nq/NImqJTJLwV0Cmw8lI3HD86VVpJPQwCtWdU5/qB\n",
       "6jj0PWd0iAGXKxWnAChFJe5l1gcO42ughUd8yefSlMQrCAO0VTJkUFELHau8iCdQ9WFtKn9e0e+8\n",
       "ewMhyaThzcl2jkhazfLLUpbK6vUFGxRbBLvGuKp+6zDdqisdE/suF4OSrkiwhiI12DP6Ep+vwh7N\n",
       "mpqeFHupgIRM7omXBR2kqFVXZ91qmRjwP9mGZYceJdp2Oa4IHAlrKEpNS8EfmgUbNDygVIDxPcHC\n",
       "B7hauQG4VUAYH2wnbqgk1l6SH9/Qk296LjGC8Wjkyrbla2xuMgr/psL9hZKKws1tKGUP8MM5UPcw\n",
       "MVKRdfbEc9EvhGSHzFLJeh/x9UPweK30nhnW47u99z7bwpbAOVEAu++d3UOXqp5YBP924vaEiywL\n",
       "1Fu0NSiOzDJ+YHnWH1fHZBLLnoNUskXVExrsrzltoSaMbA/Q37Fssyjige2WeXNTRUmpfjjobdhK\n",
       "ZXFfBtbuOAmF2FI71zK6LVH2QTaZyx0T8nNcq12YYa9h1jEGOJVPO6HZtqkbqpwyL3tUNgzM1AYz\n",
       "ivZbSgpxdwn/rwPJ9Jh8CUyDtxyvwMFQQr1gf5jkig9P9bzGLBd2P6iGp7M+qrYwUB/uKrKpbr10\n",
       "Qk7m417V/TgJPj44lu13urLZKSRMDc3w/G/A22QMabC0xeBPwlrVa4Q83ojki9sDGjnOalOk3TdQ\n",
       "KA3hWBUuonlOIM+i39U/8E60j+XvMAEnUmnAlM3CBk+H7iBCuc7qeJz35wku6c11lcuiIipI+xKh\n",
       "4WqD2RrbyKh83jC0VY3P9vTndWwoJNGhWCAu/WpVV4q2nImVMnIRdZyX96oGnTsQE1f7DeYz+kxS\n",
       "Sl00mj+XsEXLlnzw4Yx3gs0Wd5kwWuKq6k0VRq4qKfUVRxTCOj/0EqpmITfefMcDWLI0OkETY8kh\n",
       "UCiTn2FUvepBg7pmigPlmEYq/Hp6yNjebglEV4GcdOwtgrQBZUh+B3f9S4xsPTdofW3X3rx5P/Cg\n",
       "DhkqRZgdJFJzk9YgqT0QT6fHXDtmMdWc7j9GJIslhyoww2fJ1EADXBx4SXQv/4uXsn6jUWDBMjhK\n",
       "fodQuBQPrC3ZYIr74HMbTqedRFkYLexIFIPU3gfAoFpFsgLNHLiS0yYQZCE3AAAAgkGfTEUVPBX/\n",
       "AAAZqXn8I01vzMO54ABC37VrgPuF2Ok982EXz05O9R+F88bRPUYgsfGp22H/a6mUN7XV8hBsqfNc\n",
       "2RoFQ2Ur4T+k9lJQAlyELGB5s4Vni8omoeaIcdxOP2dueARMO7kqNgQVrbsTpUgPQBHw8qPyU8I3\n",
       "VAORgM7Eh6UAAAPKAZ9takFfAAA/VFkzi43HjTBZjr3hkxRJAFketsJ7nI9z4eP86ptzTxaN8h2y\n",
       "mpte0BvpW+Zg7Eons5FQBuSYWEG+dqAIlpeH+d4KWDNT+tH99xq6SS69dukzvgkbvQGfEo7pZNPg\n",
       "2TmLPv/HKseTfmU5WeZkPw03vzgFqjMlQTsFcq8JCKjuq/gg2AnBBrVr0D+4n+oXwPu4dCHpVmIq\n",
       "e8Pv7d/yzxgFzv3AMUHgP3MvMKMrjrNgL7v/sGUmMtcQbpbnPLZ2sdA1x9a2Wsb1l/i5R3MCkwF8\n",
       "LMkhd+PbO7vJLPdVHhnDItOQ8N/BVjL0fLMuGmgFCBKt8qvGsq7mCf6iNVri/kP2bQt2D7XZnc1f\n",
       "QRPHqBl61e3XlgcyOh50PweHPNOLLbAvUFJIZH1qpMmSo0ULQfSsDhuvEBPgfCuDr/ppQgveytGM\n",
       "pB+h48KK8ELz7Lm1AScCbiJaz9h8LjeiI4pQwBArWitomq5hWV8pO3UOlpouXeRC+7MGjkIbnINP\n",
       "+cIaMpfMrITxtgkdgeNM4D8H1c85BvCe+K1SLe7SgPJY+kwmoJU0+/uaP4YVuKQRc7jHPYmhfdbf\n",
       "2YfzJiIjbGsI6Y7KVfZfIlXUpoRiuuObylvv1rLrT8wUpkJv8HZmsd+KhHh0Lcrz7rms7gyWTgcK\n",
       "/VRs+erW4c6/cc0S07l+uuAEamBSrgMX8LvmGNft2tp6RC39zpdVAdZzF/sFYWBDGp9lhhWEZTfI\n",
       "tnDZPXB7C9fzxzLX+uRk/Ru9XVU64Zs/NgCTRSe1pgBL4340ky5qkc3/FzRBPPNTwCRB3zVIi+WJ\n",
       "am47XcXg89AMyuNt1ZQjjZurhDch7aIDWxes/ZQ7FV+NsuxS9G4HMo9wdukSYxMxrp+5xo6tr/lT\n",
       "glqei901eg4WUbR1AWD+AUFTnTM5jGkB8qxae+lN/YazauXHwwwhMuHNjl5OYkj53+K90A1jgTdv\n",
       "iBU2K63ZQKybaefy/JUrhb9gRFrAXssBJAaLAUBCL9WxZKmYn5iQm+JPmRKSeX0qZWIsMDhpHO95\n",
       "T3xsNmzWBce3dYlKCYhXojwXA8DwMTjuanIN8uYOKQjELZIuKZ9SxN8P7dZpipzm0LBSIsRVDfFQ\n",
       "TlralYUHwP0B8+a1ZxXoQkIHUi0LYL2KtjER1/+oy7+5BGlED3MXtK/3fJZsIeDJH7QmVAcBVc00\n",
       "Vsm9UyBWc+blRjdFcD9hFPHXIKej4NKtrKJ1hmvsAVC30Pb6+NFuv6/e4nmTLQfgF0MVjkk72nVT\n",
       "EwBYOher0s08S/RpwQAABoxBm29JqEFomUwIL//+2qZYAJQ8woABwl/QyUi9N6J3w+2F9FSBUoDR\n",
       "MBDCQuxLtS17+8EjWH+7Yv+Xppm9Qykhjz1vd9SfXeFYz0fVniB9hwR+31ShShYrALxwRWev9een\n",
       "QqafqFsy/LMoeV4nJT5M6QEhiZ4Nx7OHB7J6ZSWLbhJMEbEOC7M+DdnFBFFup3WK4Bwrm9Dw32C0\n",
       "FO0IlwiYrRGLMF3fjUXRVdnKixX+NICL7w+U7AmwYm5gFMNxzc5x85H9+646C6I9aqYEdoi/I77v\n",
       "et/hstRTm0Ns/FcMnLhutUZpv1HwAb284PrmZoIC5k+Yu6VCEfLCnfwMXwWxwgZuHPqVjPqROKbx\n",
       "zaxDM4H///KyxL6q9hNH0hQ/TJLVeH/c2BaukK+yjP/7pj72XpLXzWtsOLMJpl1zDUS1UCsXPujK\n",
       "Hfs2vgrzuPqLicGMfWlrWBzkMdw+Lwm3m+qlDk5Mtgxqy0mNg0l1qLRM3Zflba3S3enU8ZDC2kyZ\n",
       "ACXDRINAqsTpU6HsD2evEdXSdI8LCWW+yYrq50bNFboWGOwfx4uUBklvAEpS76scsUkUrcveNL+O\n",
       "czq2+eLsX4PZVe/HTpON9cNvYx0Sbst1eyc2iEkSw8zNbjWIM9ybet7sXPQQkt88Lox+BDunnOT5\n",
       "7W938Op0coLIdii+U3QdiFhWQ5GJfmFo/p/Qa4KM5A8Y5N73vLdeX9lOBhqdhpnEev50BjifioSQ\n",
       "KAz3iOuM71NdfVH9/ngJwN/UpopAH7mL1orP5UCC+FhhSB6zCCkYO0O2Sb15yUpFz+DXiaXCYNVL\n",
       "IbpUDDZyitvBcoUM9qjqRsJAxbgA6Ni4Ols6NB0ZSAoa/ZLlJgYpQD7SJbyisKiEzdU8wNyd6E12\n",
       "JNt8VyphBqpQuhWYIA1oiVGxpQ4tRdQxYA0U8LRgrXPJACgLHSkssHv5HU+tI0RKICnVYjDJCN8k\n",
       "+rZr1rRRWIIgCDj7a6gkCUuw+lw3MRIaX9fPa753/UcFXGR5bkmTk+I6UK+MIV2qfvkP/FM1cL6J\n",
       "4SqzmctNES8Mo+MezAlh86Eu51/9ydTkgRlTofrug0yI2Jisnrt5E/7HDivPbTF8LIkyIOfiqEnI\n",
       "OGJAHtpyJw+Dx+YaCgAiPoMz54M6I+wHKeBYWQOtuBh+kMSBBxa+j1RhtkZ66oaf40vbnAWAGkB5\n",
       "hVvJDXnWmxZxyJ5tfsA2VNOR7PTdaDIYNt2wvjRdejYwtUwMhT5uYECHkCiu6Cu0XqboNg9BsQM1\n",
       "pJt1RiGUFV7zj8A9dCIN1p4XkhzW6lW70b+tgIkr5+ojgIjimBB2Gq7j7RxhaEuf2Hv+go67KRv7\n",
       "N/6LF7PsHALb6opQUbXbIwdGdDRjwZnpMnChm9PabmIlfr3YoRRzJsbrLp/ctOBZdAmNEjKUPpqu\n",
       "e0z/HdA2QZRMuovaBsPz4s9Mm1CnqRFJQw3ObIcFWtjDmSy6tAh+i2DmOUklkv8AqfPQqclAriBJ\n",
       "+CJmsM8WLKz5bOhpEZoQlG+mJ6TtbCrwo0KAZI+LlVNriyHzEHIPeZGGNLj1UivhCFRDjAvgnr2u\n",
       "2hVLycwyLT8yWHXvWrKsXSTOf/ozx+XTv9oNMG7m6Jq5MiD7UlN3z/XjENQJ6xUsQ5mUtB1y59VQ\n",
       "JYOQ3kuloMN2dFJIPDjCwvaeIpQnlfhQqis9oS/A07zfh8dt+Gww7cNLCRyItmS2O6UEXTXf/Ni6\n",
       "pDYpTE4QyDfm2UiG5HpVfK1Hjogiwt1OOmPHRCXtpO77IvmA3UUnQL0BsC5GUfh0Q3UmZNAw/hFt\n",
       "sCaDcqr1NYzujNUdAoXGasHnCRZSwjgLbky3ifnbT/j48O71r5TGgJWwu1dpeE1Qi2z2KQWTsUKx\n",
       "agYKntfanZXG/VI7vdKYDqd47ifpQom+MWH9CiUCzUpAMHf4kxfNjmPUMpiUEr7EGHJwq6e5YzXm\n",
       "+sBMXOJwpanRokFEX12vUkRJ3cyXdTGu/2a0dt0i1j65gCvt25+lN5KN27HpMd5y6vIsYSUVMTRA\n",
       "W5mNa90VZ0ltAIIY59ymDtDLqh9OtZbpDhdrCuqZNqIIoQ6KOINgyqFDmNJk/jReuEfY1Aib175I\n",
       "wbtKvMjNc84OXUq+X5yrsEf5yOVwk4ZFsdPN2O4xspEabBQrYECBBRCvN7jZR3N6xTdRS3ZANY0p\n",
       "Z+sm+W6XhXiWNB8cWNUIvsCDODSbGWttaKXhiks1XHo1WPc5IGehJwAABGFBm5BJ4QpSZTAgv//+\n",
       "2qZYAJQ8yB4AIPf0MEVoWioqteDKXpuaH3CwqX10mYim40IMTyOrCyQHGLpWJv4GpJ7uOAQvtCmQ\n",
       "1EtMBwDdzKS3u8s06u9By19qozvmUNLD/4c+f1PlNe3LVD8Fe0CIOmL27XPixecSjEPMQqEwOVWi\n",
       "QBw3IxwH0aPwuSCMSUXxl8SwP988i70KH3m+TK38BC9ptqa/V+akLNbt8GgBLhSz+nxFCI2lDmlL\n",
       "EZ8mSoFxfc0xy/TJpeO4uNeIWgS+2KlgQfVlXlktRZ2gn/CX4osFmr4SiJMhP+O+EwlXf/OjO8PL\n",
       "BHrrgbXzzvfpgC1L+bWXAbYOGHsL8QQde9iZMeDDaQWz5vsY5PFsHHwFOj6CBX1z4Wp4zJB5wIu4\n",
       "spL/0FFCThwsBD0EcSVNp90c6xQ6p8HQPBjJXJrXn/JfO6iw1xX1GQNTGwJ7qPwl4EAf6iJVxrqr\n",
       "GpTYoQxWqhP3RWg3T1Pr8t3mVZMceEbhSfk6fZUTtR/ITuonb8mRhH7H+nP9RLuRBYctHmn9WNti\n",
       "CPPMfb62ShibaGWr/6Zj6yHQczk/uyEuhM7ySzNNJilrJj6Ez9EL57Dq6by7QwHimrp+7rv32eZg\n",
       "VWilrCXdsIkCptwkIhqjdhRVn/oir+P2g59bkbKlPs3TWR/U/mZsSWhq/95PRMoeEIMKwQ4F8pVc\n",
       "WDSfFFYSiNmyNF9zuUIxIVOyBr2FvzDqqua9+XJZxb5wP7SKLlYaXmOx9Cj8GS/+MK774iWD2Qd+\n",
       "ODLgtph9TZuCbMuQ7ZbXT5s2k0JDepBEZSQqhBovtqeTCMW4oiH+YwtDJiWsbr1K/xEm2a9+mty8\n",
       "mKWdizNI82L8jWqt4FXr679Rh6OJkADJrHKwR3DkZq/XHCrSMHKHxoLs4IxvUN25oMVsPvSW83sT\n",
       "E+I5bFjKYsjm7j9rwua8m3fS7+PxwR2sfbtsAoJ1j2cNYVLlNq0TxaHhSspg6QyTYb/u9+TsFEH1\n",
       "By+vXvLmsQD08sWWNVibjyHfWR0LcB2k6RAjDDJ26mnx1TczQ9etH9dvtiql5EFiHmC3SjPQ0mlE\n",
       "T738t2LHNIztDXqeJs1Wz8/ZlvB1Uw8ESrdjAfcleHnOU/mbUGSJulskVb2q9cdEqoDaXWm5E+jK\n",
       "nQiA9lUnrMMpR5pWR76yFX7JkUdK7jBuhsq4Z91rhIR2TA2wf1E3Tpc/LAwkiCJp9s3wsRewQQOk\n",
       "SLYGCcZWBSOeeycevgdXLEWUZUHkZBzhCS7utvcDwps+KgByl+9rsdSNyqYSSLztMziAh2jKpJTp\n",
       "HgmFdeuXWGbpjnnetnXkc9LW30rhycfLGdfGsPninS0yto4CzMeGkDxTSXDFCltsaFUh4GEdBll+\n",
       "iBWS253mIMmpW8ftti2NrXwdO6Ekd7pY5i0qvsI0azSuQy+f7i8FZ3P1PlU1+wUeKKhw0wEAGCJj\n",
       "acEP/lcRCV5ZvM2aWRS27rartlt5Uk4JeAAACeVBm7NJ4Q6JlMCC//7aplgAlNlvTAAjthpexaVs\n",
       "sZfUJb4m3ldCet9EMnuc38Yl1JM3lem6oxwmEV0V/MIztfSJ9udFtd+uB0NvgOAslcX2WZND/usn\n",
       "INr2/ndT/PXmdORNN3V1Iu2sZVNLugIPdEhVNNSmoqPmyNb78biyccHFdjLauigZMMSjN72UVF0F\n",
       "Drr8BfQLHfnYn112I7yJxStX6f7IxKbFCewLI9Sz4iDPrMkAgb0nIHNTBNutztV6J7q7XuQTiNwj\n",
       "0Snj+BHmRJGhNRKqTC/CRBO29aiMwf0mSnb5WYhe42+1OyYEW/V0WEn54nyeHZ+h29vKMwjLbdGW\n",
       "qC5CzJAgPi3EQDBxASN/yCaJihtDcRQOYGBLw4qhiR0HGPzNFWFaR7ZDrJMHUX8lMfVq9m98JIkk\n",
       "UD1UEXSvPs5Ep39WS3xpk5Qz0SHTMmKeX8UMcByNfETEuYK+hnoeGRfyZC3BGmYkN9yuS/vf7GZy\n",
       "MrhE4o1KAwtf/tq0cREKd+hMIKf5LhRGPTvbRmT0v/nI70QqTJgmtL3g9Ktwo2ItrXXmRUXr9rBQ\n",
       "Z+T5kQQlltThBl5cD2GsoI8Ec8giME1zFYUryKgaJEYdFpxDRTW4r4Tf4X4xpoM8gfQfra/bxtbA\n",
       "ZWPFm6huQ8dOyjVQPdOvengCay2bGq7dCYzhoMWhgBb1AQvdbqptCHQOBWrjMvsZQZg1OMdu9jAH\n",
       "40DjxDXcxh71R8Ntwbe8TSqP0GQUpWMQxpQxORLNYULexRk9XtZCIM9tCy1IxdP9QW28tHYlOC2U\n",
       "8i/qZAvV6hwENJrSipOkmCq40jji50qkbFudrVZEuAcQBnO9i3uh45b7UEMX1F1Tfy17pRD6S37p\n",
       "HSQMsPaF9F9p6IxjLSQkBQMLMzeo3Ffqtd3aCo/dBwoX4WH8+c+NX7y5quX8sHmKs+GVSO+ktX0G\n",
       "Q/RfyWzkMJKhXVZaHPb81YcS5UNr3xwE/lHUNlES+LIYsfNeRksQJgMrsKU5yMMXAxmkmVxdIy9i\n",
       "ziEl670UnICOZAk1WxARkh3QqBRrl45kAL0wAyTysvWUfPLXf1oX9dwEpVAIM2fAiy8kVOPSZ6Q3\n",
       "Q3jR36brwrEm59eopEiNkryy5SKPnRrGcJXPmKS7edyg9JpcsYAyqHpgl2mCIJs+NxusGeg5gE+o\n",
       "DY3/EBD2/YTZ1hFdeCCHTYXHeCx4kz18SyXlFAefs7qecq+Z9Yw3f/8Dn1Tt+Fkjcf3Wh9eZgbMd\n",
       "MzBwPKGGSm5mObnwtrfu9XRprlGp+uYdSkGeZDxIDkYhVipMrU2oZ5KDHDqRuE/idCNPmVkWvgn6\n",
       "t0dK1oRXasoZNsXC6Dznufj/IjYEf/EVj2CrDF6G5pzk2lTQbHu2Skw+QDL5I5K/wIxqPAqg3K25\n",
       "IbpYXjUDXUUadjrJYxwBSfuLTi2aJc1jlIJF8BN7DX87hGYCiVtdJeyHWcPpb1d608Opywsalkq2\n",
       "AMbBBV3FfD55IHtfUBpE76JdjzuHlh14X923M+JrRn7dB8C7QG3VAxTWEiny3nn3J4lGnhsLwDH8\n",
       "cDbI5pMMr0vgjlPhVjh2LBqw6oGM1AJzZZeGWUEOEyzcGx24ZQknnh0uqRGvhbshS+HCq/QRQ4cg\n",
       "kFcwuLKI3ZU5SCF3vaTPo1IFjuLa7/mSfWwtxr/1V4zshmJdUacywrsluxAIknWEVSdHXzBJHn3N\n",
       "ZsPkgmHfMeNyqd6Ptpq/4CeKR2A44VNWZVRczsZchw6CB0BqkADeAp8Vrwpf4kPqRE50ujjikqRL\n",
       "+vi1xOPqhgdgcXn77Qa85i3SyIUopiMKE1FKB/dUaxIfCONWKnGfAvG9DaXRPlM+BDPhDbS8ktL+\n",
       "cp9r3Y3FbSNmiDL/VZCL9IVW/bi8rkHnRLzFKzb5eplVw/XTt107U2UTv5zPxOB3Flutun6DfdTv\n",
       "nwu33TzKvTMXqAipfgcj6o7u9aEm03Pa323N/rebB7Qp1kfxAJioZ5U/yAZs2WN8fG4BFmJ7IrgU\n",
       "jvrH8xhQdpmS4o9LADZgqrDfBZz+YR9k+otTFebzP/cN3GLbMlYYkGgGK0BIw+qHZgxZaRZrPVB9\n",
       "YOmdA7gPOZ+QxysewZ1F4HgQVOXponuRekA+QXDsoKNmE0yHO5K2xNUhJa2gAdEIlq3kcQPp/C7Q\n",
       "xOgrat1FhuVTIW2/FS+mDs96VkquY/sLj7YePHHrRt2ek1HQRcx9IQOaltOOcJHfGpNqufdAppSs\n",
       "93K2vBxmDfMHo9IWAnU6i4UadbFnv1GRjRYjhPhnc7yq4LstTcPPp8cWsHLWcAiV2Tph+dMjgkhF\n",
       "+6+rUcEBj9++FtmptEkic+DqLNMPsfbSJ9Ak/ZS74htR4Rat83ebbhNeZAQWbVjFXUESy8XBjMNe\n",
       "2G3tIC6IgfazuEoPr2Gbr2XJ1gWaqq9b2rHYv8k4hM/X56cI8uzzlrpk5sxp1UHfD8HyabucQd1I\n",
       "8kSMfZ7+CeqGwp+rYx1pM1ta5EiZe94WvBKTS11AKXrB2TXw35U4nlUohvXJBaaEoGiVm/gyiBsR\n",
       "kAMSwNuN/oP5nWVXeif/EP6cqBFV01p1QdwC3nsiEdDeZaNwMK4iYu74498AGHgy9e9c9M6kJWrm\n",
       "YHEfw0R49oF6XindNxO+MuqXQMtcmIxoZ9Md8hTsYCfjxRiv2Sxv9amle3bQX43nV7CLxd90Zu8G\n",
       "Rmsm62DD7r8Wt8hwqx9X9KrfMLmSCiTAa69+R+vo7upSSBqf017yEG1Pl2DaKo1EXhB6sSG2QD8O\n",
       "nwMWeooxqDaBsTa/N/D4Ug7Gmj7pIrMEpLwwXkOC4wF2DboiQ+ydgHlC2goSSrpWylPfvQF5kB38\n",
       "ip2sHr7dcHQBLsPlahfu17tLLyD3/nG1TRwBSA98W/nVSTKmJbUXFCASjGIMfwWrbtmw4T2m/FpN\n",
       "m4QmVfJub32cCBO+3bxwipJo4wSIgbrSfTR5BTuDKpMNADeycll2jWw09rJ7x/7Yy/1ISnRk0+gw\n",
       "Fcwh04LBPLM5DyUCZBWL6Jy+FUnKwESw6TVf1sity11PgGJuonAFgn45MgKWf+ePHoqcW+QFq+rP\n",
       "teoaV6Y57gCqDW7vkKTfMImAt0fj9wSaTmGAcz4WShEP0KcXdSplju7+YhvPl1UyRBZLlRPdS5lu\n",
       "QhHBjpY5XjhVNbn9u0UDm6HAaJCwjLtErqKWX0fLW8fidEtUx2xmZbAmZNP6Fx1QlB3oEpvObQWr\n",
       "pPnM64kyD59hEYVVPSWKir6Mf1N99r68btO+fAHlvK/Kx+Mnb/0oddw68DIEYUBmd+3B6Ml3kp7P\n",
       "zEylURZ5sKyO5c7v6dKATMKoO8dt4lEgtHk6ZoWu1xglMFYoNAMtL7zRuiKX4FLqp4WZn0jAAAAB\n",
       "9kGf0UURPBX/AABYTMS4K7qPIoGryf5hPr5f/OjQ6AD5LPpKSOZiFWWXvbyRLRFXxpR78MHzSRNo\n",
       "2SkAdTVYQl4ZQbD54e1WmirYvTKpjjs6utS35cRfi7FyhwQuWka98vYFpnAHrmSdN8JVvg5RmuF+\n",
       "eHbwmeFr61z7pU8TwJnwNutLpbem0B7ECGINBpRHIa0Mf1fGoUNXnqH1mgh7KUc1oyZ+/SXGCjmg\n",
       "ImCgjPy+kAcVB0EEnK//ATNjRLH+pORgjxxuPcJXoVHmQ9ndtz25uL4ZxlEgYcSzBih4Qhj/5RFu\n",
       "vf98nou8z3HpJHMm6ZtsZ0xIKI5+aAvokMgCX/V6moExtkqqEn6RlFPZmGNkeSae9wYjenxrXpQM\n",
       "84xqWSu2xH7/JIf9XQN7c+uOqzv2J+SnorWumPZVtlmU3K2myYIkQWrOms1JmR9zG1iIsA++lk2p\n",
       "aVGDGjQyLflM7Mivl89SsG0Kqy8fVQl6LSIFNXREkInQsYEVbG+zDmj1mezzv+3eN6FZ/z78B7Fj\n",
       "eO8JGtosuxR0pvOnISuJSPTrHETnZFGZJDvpZNiX77nNNkTiAc66umdXpy5jQmCaanKpy9dDB/fa\n",
       "12+B1LqjKybWzsfbqT30gcztY1rYhQWiOPh9sWgTaqkUPU5uUa+0s4Y70snqFJEAAAIpAZ/yakFf\n",
       "AAAVgzEuEAKoxRCZFKVAFxzf1ICnCT+I8lydqIAkuz6GAazeDvtURi1kCamJe2ahqx2zRID+Ay6l\n",
       "n9lBkR3d3J9pgVEux1ie96yoIGWELxh2SzVs5tbWcBrmHOdC9dkDa5Ban8JtPH9o6hwJppxuTxDS\n",
       "rzzFnH6WipPbcF58H9PLxy4P6/ifyeK5txuqqsGUQ/sBoxGFmSdo25opqKsb9AN0SPu5bWEe88Ve\n",
       "JZkswZVUXg97cDJlTnGNQoWFWmf7Gs0M27cmMBJbbitOP9zU5lPYD84Xj2wVtOhmkO//8kS0pByN\n",
       "EXVJ10boaYIqskoUj1xzIz7iMLC3hvxdSvCZtgN/C2Vr2MoAf8ZmF9pfkSSpgQ6dhcxdtNjKB/Z8\n",
       "Iyu87YKZ8oprkmqiaOSfIBzlEd1l842qkkt8vSYSxRFa5Unj7i5KHTkvtMdUUDOy53B74In3MNSF\n",
       "I9y8LcwXE42q4UsMX95Sc2P4EXjmT6P7xWuHM4dyCogI3Qa1G6WuTCn/1SPP3gRBqifS6mt3rBZw\n",
       "wXWoDSMqBHsImaCG/tIOFiXHAEKU/QdXsLrH+LPnfLcK7taOG3e6TxYovB7l9FYiL/HnE7C7cf+t\n",
       "epHSQKb5y50JUeUkDrdVECYjpAABHlxYA8uZ3iZ3mbaH9dLVQEiSCNzUIFQtg0FkYQhwXU7TKDTE\n",
       "MLEK6h6S5bxKgv3xBb6C8o/3jRocbvbvii2SPeIWMfxnwAAAA/RBm/VJqEFomUwU8Fv//talUACU\n",
       "PIgwACWhmSlmTp0zrF3GagAAAwM0MX+k8ezg/wx2UgAGXzjKmsfoUA+LxnbcA6N0ntW+H51wf6s0\n",
       "5iUtryn65AvElG9/YXYmCAYdIJerMMbghXuRQn5Rtv/XdHptpJhPBV9UNn9oYSqK6GyQh39e4BMf\n",
       "fFF7+Vh3oZ0WPsdBD1S24VrIQK++MyMlM4avtftoXDHseuOGoi7OFsMeF9yZAd/CtWWFabqVQ4H/\n",
       "/7P0yRTaLCqPwuLUDOUDhYmvoe7XWJflpLHGovfXHayswcDAAKvUXf1bdyCk23C87nRCqB7MiGMT\n",
       "BkKV7pFek2uo8YNicEN3MGPX55+B7QTy8QJVNc1p5H4XywvJ0p2KJt8PfE+tNaaXzXukA65nntgV\n",
       "HprwhknUo3sOFOAZUtHb1K64gxh11JZdHSy2IeV9etQiXrRdXMATfCBiqqbv2sEuMZqMGPKo/3bB\n",
       "RTfxIeQlmbL8ETGFhjjD7KfSG/QYVj+W7qzZPqK1pBxawcvcPGEYgk30/m1Q2GLh11OReHlSEq04\n",
       "/P4nw6jwD7QBkdqmYaXXTNrWaemK1FT90n+iiQiTRDVL7uc2xDsoktonGVXsIQdvMM56FDTzYu35\n",
       "fYBHHC3RPm2+UA5ySqw6tOQ4IvHCAxINMhxG/wRiUOIb5agEvf2l3hs8amYdvOXAooN9kUMbryyy\n",
       "a2aB6WiJBX95xFrm2xEDXba2oLSUSWC/j98HsKs2k5iWn14Qhg7x63r/MBF+c1eF0vfYm2NancXO\n",
       "DabFh6qKqhsSFXdG2Z1vyILN/k/JJTNLmazbGGvONrAnUA2fJCwMJ67HOoNDW8v00vxErU6VMFow\n",
       "hZGRND7j+kYyeqhV71qix+Z9liWy2d33yBdemCFsbXp8rvhW1iun/vIlzk83i7h67PAtyhN7lETJ\n",
       "lqbefKPMinaqlGV/OB0GsfXjluV/5Jfa9w7I5peYL0QpjyInKKe0fKnlL6vQBFx3pWeOwY9WYQrx\n",
       "nwiTstmmRHKWpd44mt7N+2ujkZjxHIM3wbH2C3Bn5YOjwTVakzD9uaBKV1UqY+hyR2QfTFWuIQVD\n",
       "qcPyRtL4SiEoFR+ldCbkxG1nh70gzPcP17orLOTCbUG3s9DMqAwLNpLVKQTtqXC6/ieQ5LwXhoCB\n",
       "UAfTr8OEN/rDtDZ1Wdk4WCEwBjI1BYbEq9ov4qaloGqR0N0nozIP4kTz5tctr1N5gDS3m/4UZc9I\n",
       "atjDrJyiUPBelzzQz2mCJlBE+hm9/iXU0prJeyq4Q8oTD6sv/OdFhrgGvsmYKxJCjImOz3wEkeJq\n",
       "KtQRGqyPVCe2xDPzAPogexUmRh0xwAf4AAACMgGeFGpBXwAAGGtoqM6YGPJgo8Z+w5NdlsK22O3u\n",
       "Tl1rtCcmKAknouWQXs8pEAIJPVKwu/oVkVYMKeQH/VAv1nMkrHNpABpAEeGzalIXBiUGXgOp4xOu\n",
       "lb+rfi3TCbGfmSlH/D62+YQSrdonGpNgIZSTR2/ngWl8wDUU8ijgR1c/ifuWBxPOJela+7ALO6tM\n",
       "s/5IZUCeOJWcrbZTddsCNg4mkPARs+vsbD56Q54hYsRZ5L+x8QCjzEPQzrWBN0T6mjaVjB7DXe5P\n",
       "cASqGEb82t8EJY2zlWlWLtpuBmPI/CF/zRFLI9ITlNRmNWE9tPTXeaX+2o2aCqHpmQNI/7dVubwF\n",
       "wFzF7uUiewX5/nhuNYwvRf3H6hoalmI1h1tnSjMPZOfvGyPKMsG4bui7gvBd/Z7nxoy/a+a0JwEW\n",
       "coaAPIbyoGCdp2z0MYE6yt1iqdfUbrD+7YQcnWEzdvQTdRM9XbZCGlN8XeYLUJsbysExuY34ISv7\n",
       "Zs5rTSy7r2WQh2YwgNAW3dSKLCu6OA8vIFKraOjIkyMBxQgRtyOyW9KHfffSvUkFTjmoXpq81n95\n",
       "HkIGihyeba4aTraaw72zb7YRDMh34bcpBxvIKiNP5l5pAmeG4BrqcTNayxKls8SA5fgtzRPAoSYE\n",
       "5PkWtOrwXqqm/sM86oh6slSuNnX713OJmLixACbtz/zNrWQEf7mCDIr39pIvSwcuLEFXn8UOqetY\n",
       "Bj8l8OtxaFR34TY4ZyNmBXmYCgkAAAKFQZoWSeEKUmUwIK///talUAB0k6YBYtI3+3tMNFcQAbN2\n",
       "kXt44QXFwDsZNhIODVVOeJprAtWiySKp0fQj2gbfOl9KlQiVOmdHV3/OM6NUu83W8XB7LO50kv17\n",
       "pC/eD6xho6codPFP6TQ5ACZ2dr23bIzu2743suwze89zwu96P264+VrLZE1vY4XHm3E9FtmWZ0vG\n",
       "jO19B/WxIB68rHOcoKwuwNHl2PhEMklOlNiWPZ4dU3owh913KTF8upZuADilzKPqnLOww+xWVYhj\n",
       "z6YT8MapLN+agaTWun1cLiCbPWrlxT8ub5Sb7Ksn3nTZ3LcHiCqpaAHG1loQFYugz5XOATL2snVa\n",
       "CSBwe50l582GMolt2LdpKQfFUef2rAtffDuXwa0lZuT9thPWQdsL0kCtw3btuxEV0IV6nZIWT2mq\n",
       "FahjhPgNaHN3ppTpY4NELIfGjy5T/8I0t3LMkjmtP590l31EZ0GSIAVX7qizq1+DBAZM09u8QG5n\n",
       "XcL49/AjjUxcX9JtboHQBBuGH0fBCqvW6hAidl+9IF7Hl2R68c91m0Hk99YSSPe9fekWL24j6yLE\n",
       "zyVL4W8HEOA8J2g/QXMjOy10DqA5/FXnibKBY/UjdKe7Kf3ria7vY8GlKcuU7Yhq2DL7U3uvV2+r\n",
       "DkAxAyOrqBttUN8n4d0JyA38Nu7nF38KpU6P5FcgXaEgvyYai+sDSSLCyGRGDHQm5nVGpCFnFB0C\n",
       "rooTQ7jMFl6PfIOClpdeTTYmT0OCv4DQw6ndscvQdPYCN3hS8NzB/bPpiynhNofelouj/Y+Mwe7b\n",
       "s7kRxNOXqByRuM/mmcVkyUSm9nyO/4MiXlIskPtbdoi/LF8Wvl/1KmBAAAAEBW1vb3YAAABsbXZo\n",
       "ZAAAAAAAAAAAAAAAAAAAA+gAAFnYAAEAAAEAAAAAAAAAAAAAAAABAAAAAAAAAAAAAAAAAAAAAQAA\n",
       "AAAAAAAAAAAAAAAAQAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAIAAAMwdHJhawAAAFx0\n",
       "a2hkAAAAAwAAAAAAAAAAAAAAAQAAAAAAAFnYAAAAAAAAAAAAAAAAAAAAAAABAAAAAAAAAAAAAAAA\n",
       "AAAAAQAAAAAAAAAAAAAAAAAAQAAAAAKAAAAB4AAAAAAAJGVkdHMAAAAcZWxzdAAAAAAAAAABAABZ\n",
       "2AAAgAAAAQAAAAACqG1kaWEAAAAgbWRoZAAAAAAAAAAAAAAAAAAAQAAABcAAVcQAAAAAAC1oZGxy\n",
       "AAAAAAAAAAB2aWRlAAAAAAAAAAAAAAAAVmlkZW9IYW5kbGVyAAAAAlNtaW5mAAAAFHZtaGQAAAAB\n",
       "AAAAAAAAAAAAAAAkZGluZgAAABxkcmVmAAAAAAAAAAEAAAAMdXJsIAAAAAEAAAITc3RibAAAALdz\n",
       "dHNkAAAAAAAAAAEAAACnYXZjMQAAAAAAAAABAAAAAAAAAAAAAAAAAAAAAAKAAeAASAAAAEgAAAAA\n",
       "AAAAAQAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABj//wAAADVhdmNDAWQAFv/hABhn\n",
       "ZAAWrNlAoD2hAAADAAEAAAMAAg8WLZYBAAZo6+PLIsD9+PgAAAAAHHV1aWRraEDyXyRPxbo5pRvP\n",
       "AyPzAAAAAAAAABhzdHRzAAAAAAAAAAEAAAAXAABAAAAAABRzdHNzAAAAAAAAAAEAAAABAAAAiGN0\n",
       "dHMAAAAAAAAADwAAAAUAAIAAAAAAAQABAAAAAAACAABAAAAAAAEAAMAAAAAAAQAAQAAAAAABAADA\n",
       "AAAAAAEAAEAAAAAAAQABAAAAAAACAABAAAAAAAIAAIAAAAAAAQABAAAAAAACAABAAAAAAAEAAMAA\n",
       "AAAAAQAAQAAAAAABAACAAAAAABxzdHNjAAAAAAAAAAEAAAABAAAAFwAAAAEAAABwc3RzegAAAAAA\n",
       "AAAAAAAAFwAAF/UAAAfJAAAHJAAABygAAAeLAAAKywAAAlUAAAHsAAAFiAAAA2YAAAYGAAAFZgAA\n",
       "CBYAAACGAAADzgAABpAAAARlAAAJ6QAAAfoAAAItAAAD+AAAAjYAAAKJAAAAFHN0Y28AAAAAAAAA\n",
       "AQAAADAAAABhdWR0YQAAAFltZXRhAAAAAAAAACFoZGxyAAAAAAAAAABtZGlyYXBwbAAAAAAAAAAA\n",
       "AAAAACxpbHN0AAAAJKl0b28AAAAcZGF0YQAAAAEAAAAATGF2ZjYwLjMuMTAw\n",
       "\">\n",
       "  Your browser does not support the video tag.\n",
       "</video>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "# set grid world dimensions n x m\n",
    "grid_n = 5\n",
    "grid_m = 5\n",
    "\n",
    "# Intitialize the robots\n",
    "r1 = Robot(\"A\", (0, 0), (4, 4))\n",
    "r2 = Robot(\"B\", (0, 2), (4, 2))\n",
    "r3 = Robot(\"C\", (0, 4), (4, 0))\n",
    "robots = [r1, r2, r3]\n",
    "num_iter = grid_n * len(robots) * 3\n",
    "t_0 = 0\n",
    "\n",
    "# Get the contracts ensuring no conflicts\n",
    "collision_contract_list = get_collision_contracts_list(robots)\n",
    "swapping_contracts_list = get_swapping_contracts_list(robots)\n",
    "\n",
    "# save the initial step\n",
    "trace = []\n",
    "trace = save_trace(trace,\n",
    "    [(robot.pos.x,robot.pos.y) for robot in robots],\n",
    "    [(robot.goal.x,robot.goal.y) for robot in robots])\n",
    "\n",
    "random_move_nrs = 0\n",
    "\n",
    "for _j in range(0, num_iter):  # noqa: WPS122\n",
    "    to_goal = distance([[robot.pos.x, robot.pos.y] for robot in robots], [robot.goal for robot in robots])\n",
    "\n",
    "    # merge the dynamics contracts\n",
    "    dynamics_contract = get_dynamics_contract(robots[0].name, robots[0].pos, t_0, grid_n, grid_m)\n",
    "    for robot in robots[1:]:\n",
    "        contract = get_dynamics_contract(robot.name, robot.pos, t_0, grid_n, grid_m)\n",
    "        dynamics_contract = dynamics_contract.merge(contract)\n",
    "\n",
    "    # keep robots that are at the goal there most of the time\n",
    "    if random.random() < 0.9:\n",
    "        goal_contract = robots_stay_at_goal(robots, t_0)\n",
    "        multiagent_contract = dynamics_contract.merge(goal_contract)\n",
    "    else:\n",
    "        multiagent_contract = dynamics_contract\n",
    "\n",
    "    # set the objective\n",
    "    expr = objective_expr(robots)\n",
    "    \n",
    "    # optimize over the contract by minimizing the objective\n",
    "    fun_val, var_dict = optimize_contract(contract=multiagent_contract, expr=expr, maximize=False)\n",
    "    var_dict = extend_var_dict(var_dict, robots)\n",
    "    \n",
    "    move_ok = check_move(var_dict, collision_contract_list, swapping_contracts_list)\n",
    "    move = [(var_dict[Var(\"x_\"+robot.name+\"_1\")], var_dict[Var(\"y_\"+robot.name+\"_1\")]) for robot in robots]\n",
    "\n",
    "    if to_goal <= 5: # if the robots are close to the goal take the optimal move or take 3 random moves if that is not possible\n",
    "        if not move_ok:\n",
    "            random_move_nrs += 3\n",
    "    # if the robots are not close to the goal choose a random move with decreasing probability\n",
    "    elif random.random() < 0.4*to_goal/(len(robots)*grid_n):\n",
    "        random_move_nrs += 1\n",
    "\n",
    "    if not move_ok or random_move_nrs > 0:\n",
    "        move, t_1 = find_random_move(grid_n, grid_m, robots, t_0, multiagent_contract, collision_contract_list, swapping_contracts_list)\n",
    "        random_move_nrs= max(random_move_nrs-1,0)\n",
    "\n",
    "    # take the move\n",
    "    for i,robot in enumerate(robots):\n",
    "        robot.move(move[i])\n",
    "        t_0 +=1\n",
    "\n",
    "    trace = save_trace(trace,\n",
    "    [(robot.pos.x,robot.pos.y) for robot in robots],\n",
    "    [(robot.goal.x,robot.goal.y) for robot in robots])\n",
    "\n",
    "    if distance([[robot.pos.x, robot.pos.y] for robot in robots], [robot.goal for robot in robots]) == 0:\n",
    "        print('All robots reached their goal {}'.format(move))\n",
    "        break\n",
    "\n",
    "animate(trace, grid_n, grid_m, \"3_robots\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b5ff1335",
   "metadata": {},
   "source": [
    "This analysis can be extended by adding obstacles (by adding a contract that ensures no collision with obstacles) and adding more robots to the grid as desired. \n",
    "We showed how to set up our contracts to describe the viewpoint for a single timestep, and how to modularly add contracts describing the dynamics of individual robots and conflicts.\n",
    "\n",
    "Depending on the obstacle geometry and the number of robots, it can be necessary to consider a longer horizon to reach the goal more efficiently - prevent situations where the robots get stuck. For this we could compose the contracts for multiple timesteps and pick the strategy on the possible action set resulting from this analysis, which we leave to future work."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e8819c27",
   "metadata": {},
   "source": [
    "## References\n",
    "\n",
    "[**Dresner and Stone 2008**](https://www.jair.org/index.php/jair/article/download/10542/25241)\n",
    "\n",
    "Dresner, K. and Stone, P., 2008. A multiagent approach to autonomous intersection management. Journal of artificial intelligence research, 31, pp.591-656.\n",
    "\n",
    "[**Ma et al. 2017**](https://ojs.aaai.org/index.php/AIIDE/article/download/12919/12767)\n",
    "\n",
    "Ma, H., Yang, J., Cohen, L., Kumar, T.S. and Koenig, S., 2017, September. Feasibility study: Moving non-homogeneous teams in congested video game environments. In Thirteenth Artificial Intelligence and Interactive Digital Entertainment Conference.\n",
    "\n",
    "[**Pallottino et al. 2007**](https://ieeexplore.ieee.org/iel5/8860/4399947/04392815.pdf?casa_token=HP6WWjHKswQAAAAA:ua93qnZ1EBG34GM6r84yNkR5h7uZqYqh3HjF8xB0_zhIMlWwmuI8RMIJ6h-QWElqXOZlSg)\n",
    "\n",
    "Pallottino, L., Scordio, V.G., Bicchi, A. and Frazzoli, E., 2007. Decentralized cooperative policy for conflict resolution in multivehicle systems. IEEE Transactions on Robotics, 23(6), pp.1170-1183.\n",
    "\n",
    "[**Silver 2005**](https://ojs.aaai.org/index.php/AIIDE/article/download/18726/18503)\n",
    "\n",
    "Silver, D., 2005. Cooperative pathfinding. In Proceedings of the aaai conference on artificial intelligence and interactive digital entertainment (Vol. 1, No. 1, pp. 117-122).\n",
    "\n",
    "[**Stern et al. 2019**](https://arxiv.org/abs/1906.08291)\n",
    "\n",
    "Stern, R., Sturtevant, N.R., Felner, A., Koenig, S., Ma, H., Walker, T.T., Li, J., Atzmon, D., Cohen, L., Kumar, T.S. and Barták, R., 2019, July. _Multi-agent pathfinding: Definitions, variants, and benchmarks._ In Twelfth Annual Symposium on Combinatorial Search.\n",
    "\n",
    "[**Wilson et al. 2020**](https://ieeexplore.ieee.org/iel7/5488303/8960558/08960572.pdf?casa_token=5GsOySsxPm4AAAAA:gVhO3ngOXJzZ-gnupam3LFl5EDInm50sLy4BTUP8zqxuDvAMRyMKNAp_bPOvBPKmcYbjZg)\n",
    "\n",
    "Wilson, S., Glotfelter, P., Wang, L., Mayya, S., Notomista, G., Mote, M. and Egerstedt, M., 2020. The robotarium: Globally impactful opportunities, challenges, and lessons learned in remote-access, distributed control of multirobot systems. IEEE Control Systems Magazine, 40(1), pp.26-44.\n",
    "\n",
    "[**Wurman et al. 2008**](http://www.dcsc.tudelft.nl/~sc4081/2018/assign/pap/robert_kiva_paper.pdf)\n",
    "\n",
    "Wurman, P.R., D'Andrea, R. and Mountz, M., 2008. Coordinating hundreds of cooperative, autonomous vehicles in warehouses. AI magazine, 29(1), pp.9-9.\n",
    "\n"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.10.13"
  },
  "vscode": {
   "interpreter": {
    "hash": "b282b3e35ff361393169c4f355db145ffcb63e574f57c9818c827b7c99ca9fc3"
   }
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}