notebooks/certification_deepz.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "cac5c830",
   "metadata": {},
   "source": [
    "# Certification of Robustness using Zonotopes with DeepZ"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e03d16f6",
   "metadata": {},
   "source": [
    "In this notebook we will demonstrate the usage of certification using zonotopes within ART. With deterministic certification methods such as DeepZ we can have a guarantee if a datapoint could have its class changed under a given bound. This method was originally proposed in: https://papers.nips.cc/paper/2018/file/f2f446980d8e971ef3da97af089481c3-Paper.pdf\n",
    "\n",
    "The zonotopes abstraction used here is defined by:\n",
    "\\begin{equation}\n",
    "    \\hat{x} = \\eta_0 + \\sum_{i=1}^{i=N} \\eta_i \\epsilon_i \n",
    "\\end{equation}\n",
    "\n",
    "where $\\eta_0$ is the central vector, $\\epsilon_i$ are noise symbols, $\\eta_i$ are coefficients representing deviations around $\\eta_0$.\n",
    "\n",
    "We can illustrate a 2D toy example of this below in which the initial datapoint has two features, with a central vector of [0.25, 0.25] and these features both have noise terms of [0.25, 0.25]. We push this zonotope through the neural network and show it's intermediate shapes:\n"
   ]
  },
  {
   "attachments": {
    "zonotope_picture.png.png": {
     "image/png": "iVBORw0KGgoAAAANSUhEUgAAAfwAAAEuCAYAAABrpKA3AAAABHNCSVQICAgIfAhkiAAAAAlwSFlzAAAOxAAADsQBlSsOGwAAABl0RVh0U29mdHdhcmUAd3d3Lmlua3NjYXBlLm9yZ5vuPBoAACAASURBVHic7N13YFV1nv//523JTe+kQAiEFkJJICGkERDpVUHEMuuIjiLCON8dZ/e7v93Z0XV3dua7rlMExYpYwS4ERFTAUENJ6B0SEtJDeu7N7ef3BxMGFeQSbnJvwvvxX8i55/O54d7zOp96VHggRVF+Dbzg7noIIYTwSIkqleqkuyvR3ajdXQEhhBBCdD4JfCGEEOI2IIEvhBBC3Aa07q6A6DqKotDW1kZZWRklJSWUlJTQ0tKC3W5Ho9Hg7+9PbGwscXFxxMbG4ufnh0qlcne1RSey2WzU1NRw4cIFSkpKqK2txWq1AuDt7U1UVBRxcXHExcURFhaGRqNxc41FZ3I4HLS0tFy5PpSXl2M0GnE4HGi1WoKDg698Hnr37o2Xl5dcI7oRj/yfkkl7rmW1WikpKWHHjh0cPHgQh8OBTqejV69eBAUFodVqsdvtNDc3U11djcViAWDEiBGMHz+e+Ph4vLy83PwuhKs4HA4aGxvZu3cvO3fupKGhAZ1OR2BgIL169cLLywtFUTCbzVRVVWEwGLBarURHRzN+/HhSUlLkZrCHMZvNnDhxgry8PM6cOYNGo0Gv1xMZGYmfnx9qtRqbzUZ9fT11dXVYrVa8vb1JS0sjOzub6Ojorr4ZlEl7HeCR31gJfNdwOBwUFxfzxRdfcOHCBUJCQkhNTWXAgAFERUVdM8QtFgs1NTUUFxdz4MABqqur6dOnD/PmzWPQoEGo1TIK1J01NzezefNmdu/ejVqtJjExkZEjRxIdHU1QUNCPjlcUhYaGBioqKigsLOTs2bPodDomTpzIhAkT8PHxccO7EK5is9k4dOgQubm51NfX07t3b8aMGUPfvn0JDw9Hq/1xJ3BbWxuVlZWcPn2agwcP0trayrBhw5gzZw7R0dFddSMogd8BEvg9lNFoZNu2bXz77bf06tWLnJwcEhISbqqlbrPZOHv2LHl5eZSWljJhwgSmTp2Kv79/J9ZcdAa73c6pU6f47LPPaGpqIisri5SUFEJCQm7qPFVVVezbt4/9+/cTGxvLvHnz6Nevn7T2u6G6ujpyc3MpKChgyJAhjBs3jn79+t3UTb3RaOTYsWPk5eVhMpmYNWsW6enpXdEjKIHfAR75LZXAvzXNzc288847nD9/nszMTHJycvD19e3w+axWKzt27CAvL4+YmBgWLVpEWFiYC2ssOpPdbue7774jNzeX2NhYZs6cSe/evTt8PkVROHfuHF9++SVNTU0sXLiQlJQUCf1upLS0lNWrV2M0Gpk8eTIpKSm31CXf1NTEN998w6FDhxgzZgzz58/v7N4fCfwO8MhvqAR+x7W0tLBq1SrKy8u55557SEhIcNmFuLi4mDVr1hAaGsqiRYsIDw93yXndTXFYOb5/BzsPnKT3kFQm5qTi59UzJqfZ7Xa2bdvGhg0bSEtLY/Lkyej1epecu6WlhdzcXM6cOcP999/vsaGv2K2cOVbAmQvVqHXeeHt7ERgSwZCEIQT5XrslarMYOXbwAKVVDQSExjAqJZlgXx0ADkcbxw4UUFxZh39IJMmjkwnz96L83AkOnyomoFc/MlKGodV45vBXaWkpq1atQqvVsnDhQqKiolxyXrvdTkFBARs2bCA5OZmFCxe67LN2DRL4HeCZn0jRIVarlVWrVlFWVsbChQsZOnSoSy/A/fv358EHH6ShoYG3336blpYWl53bfRSObP2E9zbsoraqiGee+jn/+84WHO6ulgsoisLu3bvJzc0lPT2dadOmufQCHBAQwF133cXgwYNZs2YNx48fd9m5XUqlRmNv5d+WLSbvXD2Bvho2vfMCCx/5v1S2mK/5ErVai63hAk8+soTjdRa8tH+/VKrQ4q2u59ePPEL++Wb0Wg2gwjdAz8dvraYVL9QeeOMDUF1dzVtvvYVOp+OBBx5wWdgDaDQaxowZw5w5czh48CCffPIJDkdP+Cb1HBL4Pcg333zD2bNnWbhwIYMHD+6UMuLi4rjvvvuoqKhg8+bN3f4LrdhtlBv9efbZ3/Lvz/0P//XUbL7Z+A2G7v22AKisrGTdunUkJyczZcoUdDqdy8vw9fXl7rvvJjY2lk8++YTGxkaXl3GrVGoNMX3iCQnwo/+QRNIyxvPU4oc4uXUN20/UXTlOcdgxGk0AqLVexPUbSEBgIAMHxuF7VY+PSq2jT//BBAf4MCA+Hj+9DlAREhnP6NRRjBjYF7Xa8wLfYrGwbt06rFYrCxcuJCIiwuVlqFQqUlJSmDlzJvn5+RQUFLi8DNFxEvg9xIULF9i8eTM5OTkMGTKkU8vq168fEyZMYOfOnZw82b171VQaLZOnT0evUYFKQ0BgEHHx8eg973p9U2w2G2vXrsXPz49p06Z1Sti38/HxYebMmRiNRnJzc7Hb7Z1Wlms4OH3iKHZ9FP0iL89tObPva1a9/R7/+8z/4VfPvYnBpvxtwFPFT418qn7wO41a85PHu9PevXs5duwY06ZNIzIystPKUalUjBkzhmHDhvHRRx955E3g7UoCvwdQFIVPP/2U0NBQJk2a1OnlqVQqMjIyiI2NZePGjbS1tXV6mZ1HhU53eemRw9zEzkOXWPyLeeg885rttP3791NUVMScOXO6ZFVFVFQUkyZNYu/evRQXF3d6eR2hUsxs/egN7p09lRdyi1j10VpS44JQrFX89rnX6du/Pylpo9n81vPsOl7t7uq6VHNzMxs3biQpKYnhw4d3enkajYbZs2cDkJub2+nlCedI4PcARUVFXLhwgUmTJnVqS+5q3t7e5OTkUFpa6rEX+Jui2Nm/bSODpy1i3NDOa/10la1btzJgwAAGDRrUZWWmpqYSFhZGXl4eiqJ0WbnOUlTe5My9l4zBIZwuaSBhSBwalQrT+UJOGvyJ6RVO/2FZfLz+U1IHBN/gbCpUKnD84H0qiuKR7fvCwkLMZjPjxo3rsg1ygoKCyMrKoqCggKampi4pU/y02z7w7dY2zp48Rmll3Y0PdkmBJs6ePEFRWa3LTrlz504CAgIYOnSoy87pjPj4eKKjo9mxY0c36Mb9CYqDk3u/oco7kXkTk3CY22g2XnsyV3dw7tw5ysrKyMzM7NJZ8zqdjrS0NA4dOkRDQ0OXlXsztN6BLH3mz4z2OsrjT/8vzSYbKi8d9aVFBPQdTGLiMAb3701TY/PfXvGDGxfFxnfbdqLxCiIsUEfN1UHmaMNk1+Dt5Vk7llssFnbt2sXAgQOJjo7u0rLHjh2L3W5n9+7dXVquuLbbPvCbqk/z6ptrKa+5PM5kNRupLL9IVU09NsdPt1JudKzDdnnXuuaWVpqbGqlvbMFhN1F89hB/fXmtS+rf3NzMiRMnGDNmTJe17tt5eXmRkpLCiRMnaG5uvvELPJLCiZ2f8E+/f4PCvC/4j2ef4Z//7T8prml1d8U6LD8/n9DQUBISErq87FGjRqHVaj1rspai0NR4iVaDkUs19eAbxfMrltOw83X+5U9rsUSOYkrcJRY9/BTvvv8+y19ZjVnlTX1dDW1GIxXlFVRXV3Ox+DSrX/gXvjnRgt4vjJ/dO4VPVr3O0fPlXKqtYstna/AbmE6In2cFfnl5ORUVFYwZM6bLy/b392fEiBHs27fPI3t9bjee9cl0CxXxI9LJSBqAtbWa11a+zZDMidgrD3HePpAn7p3AtSbcWlureXXl2wzNmoi1/BBFjkE8ce/47x1rqD7PP8xbQIt3BBERvXnk179lTlYCU2ZPZ9/RNS6pfXV1NUaj8Sa6bhUMLU2YbGpCAn1oampB7xeIj3fHPgp9+/YFoKKi4qZ3bfMEisNBg1HDvLtnXPm3oKiBDIntvhsLFRcXM2DAAKd3TLNZ2mhqNuIfFITNZMCqaAkK9OtQ13RAQABRUVEUFRV14NWdw2G3Un2piV8++3v8AizUtZiIHpTNu2veYfexckqq7fx1zXrWfvgZdU0W5tz/c/qHqdl3Us0zf3gWKo6zufokdrsNJXQYP582DtQ6HvinF+i9aR3r17yF3j+IhOQMFmWnoPGwPv3i4mL0ej2xsbFOHa8odlqamlC0Pvh6QUuriYCgIHQd3Fdg0KBBnDx5koaGBkJDQzt0DuEaEvhXObz1I87b41iSlYraMZh/mLOIqdMyGRD04805Dm1ZS7HSnyczLx/74KyHmT4jk/4BV7eyNcxf8lvSkhPp3X8gEUEd3+3ueioqKtBoNE7vfFd59jDHK4xUHd1Ba/BgIh0XOdTcl/9YdleHyg8LC8PX15eSkhKGDRvWoXO4k0qtIWvqfLLcXREXMRgMXLp0ibFjxzp1vMPcxNYtu/HztZO39xzJif3Z9t0elv3bc8SFdmx71NjYWI9ak6/WepGcOZnkzO//++CUCQxOaf8pksef+qfv/T5r0pyf/FxovPyZOPdBJs51ZW1dS1EUSktLCQkJcW7ypuLgdOFuqk0qjufvJLh/EvUnviMs42Huv7NjQ4axsbFYLBYqKiok8N3stu/S/zuFQ/l70YdGXf6jqP0JVoopOH2tySYKh/bsxSc08vvHnvpxt7aPXwD+vt7UVpZjsLhmnNtqtbJ161bsdjsXL1688oQzJ17JubJmsrMyiNI3ca7Jl8zMHKbmJKMoDpobajl88CAtJucXofv6+hIaGkp5eXm3X5PfnR04cICamhoqKyux2Wz06dPHqdeVnTxC3Jg7SBrWj4LdR0jOGseMmdMJ89fS2lDNiaOH2V9wiOY2q9N1iYmJoaGhgdbW7jss0t21trayfft2FEWhrKzM6a2UreZmqo0+5GSkYKw8D2H9mDB5BikJ0TgMl9i9Zz9Hjx7m8Anne3BCQkLw9vamsrKyo29HuIgE/hV26uubryzRAvDSQUPdtQLfTl1DC9qrxsy9dAoN9d8/VuOlR2Uzo9X7UnFoM//vlU+x2G99HEur1VJfX8/GjRtpamrCz8/PyZm3WjJzstBr4cD+E0wcP5bIgclkjuyHYjVTeuE4b7+5mpqWm7sxCQwMvPLMbOEeISEhvPvuu1duvAIDA516Xe8RGQyJ0FN75giBQzOIDg3ljonj8dfZ+Hj1KhpVgVQf2sArn+7+4fS16woICAAuP1hFuIevry/79++nsLAQg8Hg9OdB6x1EduZobK0NlNTbGTWkP8PHjmdw72Csl87x/tpPWPfld9h1zu+Tr1ar8fPzw2AwdPTtCBeRLv0rVGi0GhxXTb5zOByorxmkKrQaNcr3jlV+dKx3cBT3zJuN3ltHlCqdf7v3d/zD/TMZdJ0t6G02G++++65Td8IGg4Fvv/2WrKws+vfv79RsbMXWxrmiKuJj9ew5r+WRwUG01p7jYmsoQ/uHMjxpJMG+G294nh9Sq9VUVFTw/PPPy8QcN9qyZQunT59GrVY7vfSqtuw82tA49u7eR1Laz8DaSsHREkaNTmT2Aw/jQOHLRjMD0mKcHtPXaDQoisLq1aux2Wwdf0PiltTU1PCrX/2KtLQ0pz8PtrZGiquMBFjO0KiKITbCm6JTRwiMHkwAKjImzyO5rxd+/jf3YByNRiOfBQ8ggX+Fmri+UZQ1N6EAKuw0tWroc83JW2r69o1i7w+P7XP1+JSDL17+d3bZ0njh6flotBoshhYM1ut/6LVaLYsWLbphaCqKwjvvvMPkyZM5efIkZrPZqaBtvHCYZ//wEQ/fnUlwbC+qik5SdraE9MlTbvjan2K324mJiWHp0qVdtsZXfN+xY8cIDAwkJSWFd955x8mLq4M3//CvRE9bSl2TDX1bA3t370EXORQ1KsJ7hVN08igtFg0hasffPus3ZrPZUKlU/PznP6dXr163+M5ER9jtdv77v/+b1atXs2rVKqeXzZ7Pz+X36ytYkBpAcLgfRccLqKi1MGGgN1pVX0YMtBATruWPz/6ef/7T/xDu5dxtoN1uR6uVuHE3+R+4QkXalFlsee80bbYZ6AxFtEZkkB7vR83JPP77nQKe+89/JFB7eavN9Cmz2LbmFG32aehaijD0yiQ93o/qE9/xh/cO8/v/eoq+g5MIiExFBVw4e5K40ePoH+oP/PQSthu11m02G8OHDyclJYWKigqKioqw2+03DNvg/qk8/0wkWv8wssffQWVdKzmT78Rff2sh3djYSHh4OGq12iOflnY70Gg0/OxnP6O+vh61Wk1jYyPBwTfaPEbNL3//Epda7URP/R8uVVehCwilV2gwdmMd677azZ0zZnDfjCp+/qf3mJ7+HF5OTEFvX6IZEBAgnwc3MZvNzJkzhwEDBhAQEOD09rYDs+/huX5VBIVFMm5KE00mGDw0Er1Wxa6tG7ENmkNSeASaxtOUNNgJj7xxhNjtdlpaWq4M9Qj3kcC/SuzIKfzDZBPrv1iHtamWf/7P3xLiraHJP4Rwajlfa2dU9OU/WWzyNH5Ws471n6/H0lTDv/z+3wnyUkNAKIMHxKJVqUieMINvN23ivZM7aGww8sIf/4UgveZHe3ncLJ1OR2pqKnB5WVx+fj4Wi+WGE/dUGh19+sVf+Xlg0N/HFhSricK9uzh34QI7du4malomfj43Xtff2tpKY2Mjo0aNcnoZmHC9xMREAPR6PVqtlrKyMvr163fD1wWGRRH4t06s2Ks+Gw6VQlXJec6cPUfRzgNMuHMCWicfCFNeXn5l9YZwDz8/P5KTk1EUhdjYWKeXSWq9fOkf3/458OPqhba9+vTnRPkZDrceRBk4lWERzsVHXV0dVquVmJiYm3sTwuUk8K+iUuvInDqfdIcDVKorj7gMih3OtEkTiAn9/hOzsqbdc3mi2veOHcmTj468fJBPMNPvvg+HoqBSqTqltdO+c1ZNTc0t7Zmu0ukZlTmDVenTUanUaJxcc1tXV4fRaCQuLq7DZQvX0ev1REZGcvHixVs6j9onnCd++SSV5WXELPglCyJCrrkfxbVcvHjRqZsN0flUKhVxcXEcOnSI5uZmpyfvXcug1IlEN9RSZ4Tf/24Kzi7Lv3jxIt7e3l2+y5/4MWmSAZY2A4a2v2+lqlarv/c8a6uhBpN/XyK9f3zF++GxP6JSfb+rW7HT3Nh8w138nBUVFYWfnx+nTp265QlzarUGrVbrdNjD5U09tFqtfJk9yMCBAzl//vwtT5JSa73oHRdP717Oh319fT3V1dUMGDDglsoWrtO/f39MJhMXLly4xTOp8A/pRVzvXmhu4vG/p06dIiwszIkhJtHZbvvA9w2KIkJbz/aCM9c9RucXRfZY1+xTr5gb2Pj514xId25jlBtp77prfzhGVzKZTBQWFjJy5EgZn/Mg6enptLS0cOzYsS4vu6CgAJVKxejRo7u8bHFtUVFR9OvXj3379nX50tmGhgZOnjxJZmbmjQ8Wne62D3x9QCQP/mIJ07NHdEl5Kn049z/yGPMnp7rsnBkZGZhMpi6/wJ89e5a6ujoyMzNl/N6D9O3bl/j4ePbs2dOlF/i2tjYKCwtJSUmRG0APotPpyM7OpqSkhLKysi4tOz8/H71e75Z9/MWPyVW6B4iNjWXw4MFs2bKlyzY7MRgM5OXlER8fL+P3HmjixImUlpZy9OjRLilPURT27NlDc3MzOTk5Mjvfw4wYMYLAwEDy8vKwWp3fNfFW1NbWkp+fT3p6+i3NLxKuI4HfA6hUKu6++27a2trYtGlTp29+43A42LFjB5cuXWLWrFl4e3t3anni5iUlJTF8+HA2bdrUJY+qvXjxItu3b2f8+PFOP6RFdB1/f3/mzJnD6dOnu+RJhlarlXXr1uHr68v06dM7vTzhHAn8HiImJobZs2ezf/9+Dh482GnlKIrCqVOn2L17NxMnTiQ+Pv7GLxJdTqPRMH/+fOx2Oxs3buzU+R0tLS1s2LCBsLAwpkyZIsM7Hio5OZnU1FS+/fZbSktLO62c9gZBUVER9913n7TuPYh8M3uQcePGMWrUKD7//HMOHz7cKWWcOXOGTz75hEGDBnHHHXfIxd2DhYeHs2DBAs6cOcO6des6JfRbWlr48MMPqa+v595775Wxew+m1WqZOXMmISEhrF27tlPG89vDfsuWLdx5551X9ocQnkGu1j1I+25rw4cP59NPP6WgoMBl3fuKonDixAnWrFmDWq0mIyNDNlbxYG1tbaxatYrjx4+jKApHjx7l888/d+kcj4aGBtauXUtlZSUPP/ywLMXrBkJDQ3nkkUfw9fXl/fffp6SkxGXnttls5OXl8fXXXzN+/HhmzpwpDQIP45Ebnz/77LMZwFR316M70mq1JCYmUlNTw5YtW2hoaCAuLs7Jx+dem9lsZuPGjWzatIlBgwbx85//nM8++4yoqCh5vrWH0mq1REREsGnTJurr63n44YfZtm0bx48fp1evXoSEhHR4Yl37DcQHH3yAwWBg0aJFJCQkyES9bsLPz4+EhASOHz/O9u3bgcsTf28lnOvq6vj444/Zt28fEydOZPbs2eh0N96p8xa89B//8R+XOrOAnsgjv6GKovwaeMHd9ejObDYbe/bs4fPPP8fHx4fx48czatQo9Hq90+ewWq0cOXKErVu30tjYyOzZs5kwYQI6nY6mpiZWrFjB/fffL+P4HsjhcLBy5UoGDBjAsWPHePrppykrK2PNmjVcvHiR1NRUxo0bR0RExE2d9+LFi+Tl5XHs2DGGDRvGvffeS3j4dR7/KDxaW1sbGzduZNu2bfTu3ZuJEycydOjQmwr+1tZW9u3bx44dO/Dy8mLhwoWMGDGiK1r2iSqV6mRnF9LTSOD3cDU1NXz++eccP34crVbL6NGjGTJkCL1798bHx+fKlr+KoqAoCiaTicrKSs6cOcOBAwdoa2tj8ODBLFy4kKioqO+du6Wlhb/85S88+OCDEvoexOFw8PLLLzNy5EhycnI4cOAAo0ePRq1WY7Va2bp1K1u3bqWlpYWBAwcyevRoYmNjCQ4O/tEDmGw2G3V1dZSUlHDgwAEuXrxIeHg406dPJyMjQ1r1PcDZs2f57LPPKC0tJSgoiLS0NOLj44mMjMTLy+t71wiHw4HBYKCsrIzjx49z5MgR1Go1qampzJkz55a27r1JEvgd4JHfVgl816uqqmLXrl0cOHAAg8GAzWYjLCyMgIAAtFotNpuN1tZW6urq0Gg0+Pr6kpycTHZ2Nn369LnueZubm3nxxRd54IEHJPQ9gM1m47XXXmP48OHk5ORc97j2XRK3b99OdXU1FosFvV5PeHg4Xl5eKIqC2WymtrYWq9WKl5cXcXFxjB8/nhEjRsijTnugc+fOsWPHDo4fP35lgmd4eDi+vr5oNBqsViuNjY00NTWh0+kICgoiIyOD9PR0QkJCbnB2l5PA7wAJ/NuMxWKhurqayspKysrKaGlpwWazodFo8Pf3p0+fPkRHRxMVFeX0+vrm5maWL1/OfffdJxO33MhisfDmm28ybNiwnwz7qymKQn19PZWVlZSXl1NbW4vFYgHA29ubqKgoevfuTVRUlOyFfpswGo1UVVVRUVFBeXk5bW1tV55nHxwcTGxsLNHR0fTq1euGj+TuRBL4HSCBL1yivaV/3333MXDgQHdX57ZjNptZvXo1Q4cOZdy4cdLVLno6CfwOkDUTwiUCAwP51a9+xYcffsi5c+fcXZ3bitls5u233yYhIUHCXghxXRL4wmUCAgJ46qmn+Oijjzhz5vpPHxSuYzabeeeddxgyZIjsYS+E+EkS+MKlAgICWLp0KZ9//jmnT592d3V6tPaW/eDBgyXshRA3JIEvXC4oKIjFixezfv16Cf1OYrFYeOutt0hISJCwF0I4RQJfdIrg4GAee+wx1q1bJ937Lma1Wq/MxpcxeyGEsyTwRacJDg5m8eLFfPrpp5w9e9bd1ekR7HY7r776KsOHDyc7O1vCXgjhNAl80amCgoJYtmwZH330kczev0V2u52XXnqJ5ORkadkLIW6aBL7odFfP3peWfsfYbDZeeuklUlNTyc7Odnd1hBDdkAS+6BIBAQH88pe/5OOPP5bQv0lWq5VXXnmFlJQUMjMz3V0dIUQ3JYEvukx76H/yyScykc9JZrOZ119/neTkZLKystxdHSFENyaBL7pUQEAAy5Yt49NPP72l0FccNkpPH+J4UY0La+dZzGYzb731FiNHjpSwF0LcMgl80eXaW/qffvppx9bpO6ycKszj6ccX8VFez+wpMJlMrF69muHDh5OVlSUT9IQQt0wCX7iFv78/v/zlL/niiy84derUzb1YrWNoSgaJ/XqhdE713MpkMvH222+TmJgoYS+EcBkJfOE2/v7+LFmyhNzcXE6evNkHX6noiTnY3o0/bNgwWWcvhHApCXzhVoGBgTz++ONs2LChA6Hfs7Q/z759zF7CXgjhShL4wu3a997Pzc29+e79HsJqtfLaa6+RlJREZmamhL0QwuUk8IVHCAwM5Mknn7wtn7Jns9l4+eWXSUlJkZa9EKLTSOALj+Hv789TTz3FZ599dsOWvs3SRnOrEbPJhM3u6KIaup7NZmPFihWMHTuWjIwMd1dHCNGDSeALj+Ln53fj2fuKnfLiCyRP/xlJvaxU1rV0bSVdxGq1smLFCtLT00lPT3d3dYQQPZxH9h0qivJr4AV310O4T2trKytWrGDu3LkMHTrU3dVxOYvFwquvvkpqaqq07IW4eYkqler2nuXbAdLCFx7J39+fZcuWsX79+h43e799u1wJeyFEV5LAFx7L39+fpUuXsm7duh4ze99kMvHmm28yatQo6cYXQnQpCXzh0a7eka+7t/Tb2tp46623SE5OJiMjQ2bjCyG6lAS+8Hh+fn4sW7aM3Nxcjh8/7u7qdIjJZOKtt94iKSlJwl4I4RYS+KJb8Pf358knn2TTpk0cO3bM3dW5KSaTiTfeeIPRo0dL2Ash3EYCX3Qb/v7+LF68mK+++qrbtPTbJ+iNGTOGsWPHStgLIdxGAl90KwEBATzxxBNs3LiREydOuLs6P8lqtbJy5UrS0tIk7IUQbieBL7qd9tn769ev99jQb99UJzMzk7FjAoQQrAAAIABJREFUx7q7OkIIIYEvuqf2Hflyc3M9LvStVivLly8nKyuLtLQ0d1dHCCEACXzRjfn5+bF06VI2bNjgMaFvsVhYsWIF2dnZEvZCCI8igS+6tfbZ+xs2bHD7RD6z2czKlSulZS+E8EgS+KLbaw/9jRs3ui30TSYTr732Gunp6RL2QgiPJIEveoT2iXzuaOm3tbXxxhtvMGbMGAl7IYTHksAXPUb7RL6NGzdy9OjRLimzPexl6Z0QwtNJ4IsexdfXl6VLl7J582aOHDnSqWW1h316ejpjxoyRsBdCeDQJfNHj+Pn5sWTJEr755ptOC32TycTrr79Oeno6qampEvZCCI8ngS96JD8/P5544gm+/vprl3fvm81mXnnlFTIyMiTshRDdhgS+6LHaW/qufOCOxWLhpZdeIjs7W7rxhRDdigS+6NHaH6375Zdf3nLoWywWli9fzvjx40lNTXVRDYUQomtI4Isez9fXl2XLll1p6SuKctPnuDrsU1JSOqGWQgjRuSTwxW3B19eXJ598kq+++uqmQ99sNrNixQomTJggLXshRLclgS9uG+1j+l9//bXT3fsmk4mVK1eSk5MjLXshRLcmgS9uK1eH/o2W7BmNRl599VWys7OlZS+E6PYk8MVtx9fXlyVLlvzk5jxGo5E33niDrKwsadkLIXoECXxxW2qfyLd582YOHz78vd+1h31mZiYpKSmy9E4I0SNI4Ivblo+PD0uXLuXbb7/l0KFDwOXtcl9//fUrLXsJeyFET6F1dwWEcKf27v1XXnkFk8lEfn4+48aNY/To0RL2QogeRVr44rbn6+vLokWLeOaZZ4iKipKWvRCiR5LAF7c9s9nMm2++ybPPPsvFixd/NKYvhBA9gXTpi9ua2Wxm+fLl3HnnnYwaNYrk5GReeuklAEaOHCktfSFEjyEtfHHbMpvNvPjii1fCHi5P5HvyySfZsmULhw4d6tA2vEII4Ykk8EW3pTjsWKz2Dr22ra2N5cuXM3ny5Cth387X15cnnniC7777TkJfCNFjSOCL7kdxcKn8HC8+9xve3Xzzz7o3Go2sXLmSO++8k+Tk5Gse4+vry+LFi6+EvhBCdHcS+KIbUnAoNk4cyKektvWmXmkwGHjttde44447ftSy/6H2lv62bds4ePDgrVRYCCHcTgJfdD8qDb16xxEdHnhTL2sP+5ycnOu27H/Ix8eHJUuWsHXrVmnpCyG6NQl8cVswGo289tprTJgwgVGjRt3U7Pv2Hfm2bNlCYWFhJ9ZSCCE6jwS+6PGMRiOvvPIKEyZMIDk5uUNL7fR6PU8++SR5eXkS+kKIbkkCX/RobW1trFy5kokTJ950y/6HfHx8eOKJJ8jLy5MxfSFEtyOBL7qtG62WM5lMrFixgkmTJjk9Zn8j7aEvY/pCiO5GAl90P4qN80f3cexCNUXHD1Bc2fCjQ9ra2njxxReZOnUqSUlJLi2+fUx/69atFBYWyjp9IUS34JH7hiqK8mvgBXfXQ3RPbW1trFixgilTprg87H9YzquvvkpOTs4tDxcIIW5KokqlOunuSnQ30sIXPYrJZGL58uWd0rL/IR8fHxYvXsz27dulpS+E8HgS+KLHMBqNLF++nGnTpjFy5MguKbM99Hfu3CmhL4TwaBL4okcwGAysXLmSqVOndlnYt/Px8eHxxx+/EvpCCOGJJPBFt2cwGHjllVeYNGlSl4d9u/bQ37FjBwUFBW6pgxBC/BQJfNGtGQwGXn31VSZPnuy2sG939Tp9CX0hhKeRwBfd1tUt+xEjRnjELHm9Xs/SpUvZvn07Bw4ccHd1hBDiCgl80S21P+K2vWXvCWHfztvbmyVLlrBz504JfSGEx5DAF91OW1tbl8/Gv1l6vZ4nnniCHTt2SOgLITyCBL7oVoxGIy+++CKzZs1i+PDh7q7OT2p/4I6EvhDCE0jgi27DaDSyYsUKZs6cybBhw9xdHadc3b2/f/9+WacvhHAbCXzRLbSH/YwZMzy+Zf9D7d37e/bskdAXQriNBL7weO076HXHsG+n1+t57LHH2Lt3r4S+EMItJPCFRzMYDKxYsaJbjNnfiI+PD7/4xS8k9IUQbiGBLzxWa2srK1euZMaMGd1mzP5GfHx8eOyxx8jPz2f//v3uro4Q4jYigS88UmtrK6+88gpTp07t9i37H9Lr9Tz++ONXxvSFEKIrSOALj9Pesp8+fTojRoxwd3U6hV6vZ8mSJezevZu9e/e6uzpCiNuABL7wKD2xG/96vLy8WLJkCfn5+RL6QohOJ4EvPIbBYOCll17qVuvsb5WXlxdPPPGEhL4QotNJ4AuP0L70bvbs2SQmJrq7Ol2qfXOe/Px89u3b5+7qCCF6KAl84XYGg4EXX3yROXPm3HZh3+6H3fuyZE8I4WoS+MKt2tfZ385h387Ly4vFixezb98+CX0hhMtJ4Au3MRgMt203/vV4e3vz2GOPUVBQIKEvhHApCXzhFu1hP3fuXAn7H9Dr9Tz66KMS+kIIl5LAF12utbWVFStWMHfuXIYOHeru6ngkCX0hhKtJ4Isu1dLSwksvvcScOXMk7G9Ar9fzi1/8ggMHDpCfn+/u6gghujkJfNFlWlpaWLlypbTsb0L7mP6BAwfYs2ePu6sjhOjGJPBFl2gP+9mzZ5OQkODu6nQr3t7eLF68WEJfCHFLJPBFp2ttbeXll1+Wbvxb0L5kT0JfCNFREviiU109G19a9remPfT3798voS+EuGkS+KLTtLa28uKLLzJv3jwJexdp35FPWvpCiJslgS86RUtLCytWrODuu+9myJAh7q5Oj6LT6Vi8eDEFBQXs3r1bluwJIZwigS9crqWlhZdffpm77rpLWvadxMvLi8cee4xDhw5J6AshnCKBL1yqfW98GbPvfN7e3jz66KMcOXJEQl8IcUMS+MJlWlpa+Otf/8r8+fMl7LuIt7c3jzzyCEePHmXXrl0S+kKI65LAFy7R3NzMihUrmD9/PoMHD3Z3dW4r3t7eLFq0SEJfCPGTtO6ugOhaJpOJS5cuUVNTQ2lpKS0tLdjtdjQaDf7+/vTp04fIyEgiIiLw8fFx6pzNzc28/PLLEvZu1N7Sf/PNNwHIzs526nUOh4P6+npqamqoqKigpqYGq9V65ZxRUVFER0cTERFBSEgIKpWq096D8Aytra3U1tZSVVVFeXk5RqMRh8OBVqslJCSEPn360KtXL8LDw9HpdO6urrgJHvntVRTl18AL7q5HT6EoClVVVezbt4/CwkKam5uxWq2Ehobi5+eHRqPBbrdjNBqpr69Ho9EQEBBAUlIS6enp9O7d+7oX+vawnzdvnoS9B7BYLLz++uskJyeTlZV13eOMRiNHjx5l586dVFVV0dbWhq+vLyEhIWi12ivnqqurw2q14uvrS2xsLOPGjSMxMVEu9D2MoigUFRWxe/duTp48icFgACA0NBQfHx/UajU2m42WlhYaGxvR6/WEhISQlpZGamoqoaGhXV3lRJVKdbKrC+3uJPB7uJqaGnJzczl+/DgqlYqRI0cyZMgQoqOj8fHxQavVolKpUBQFm82GyWSiqqqKs2fPcvjwYSwWC4MGDWLevHlER0d/79wS9p7JarXy6quvkpycTHZ2NgcPHiQpKQm1Wo3FYmH79u189913NDY20r9/f5KSkoiNjSUwMBAvL68rN3cOhwOLxUJDQwOlpaUcOnSIsrIyIiMjmTJlCmlpaajVMirY3Z09e5bc3FwuXLhAQEAAo0aNIj4+nl69euHt7Y1Go0GlUuFwOLDZbBgMBsrLyzl58iTHjx/Hy8uLlJQUZsyYQWBgYFdVWwK/AyTweyiHw0F+fj7r1q1DpVIxfvx4kpKS8Pf3d6pbVlEU2traOHr0KNu2baOtrY3Zs2eTk5ODRqO5ss5euvE9U3voJyQkcPjwYZ5++mkqKipYu3YtRUVFjB49mqysLCIjI9FoNE6fs6ysjO3bt3Py5EmSk5O55557CAkJ6eR3IzqD2Wxm06ZNbN26lYiICCZOnMiQIUPw9vZ26vUOh4Ompib279/Prl278Pf3595772XYsGFdMfQjgd8BEvg9kNVq5f3332f//v0kJSUxc+bMW7rzNplMbNy4kX379jFixAjuueceXn/9dRYsWMCgQYNcWHPhSjU1NSxfvpzq6moWL17M+++/j5+fH/PmzWPAgAEdvig7HA6OHDlCbm4uGo2GRx99lIEDB7q49qIz1dfX88Ybb3Dx4kXuuOMOJkyYcEvDNLW1tXzxxRecP3+eadOmMX369CtDQ51EAr8DJPB7GIvFwrvvvsuRI0eYO3cuqampLrnbVhSFEydO8OGHH6LT6XjwwQdJSkpyQY09i6I4aKytQfENItTfuUmLnshoNLJq1Sr0ej0HDx5Eq9UydOhQ5s2b5/RkzBtpbGxk7dq11NbW8thjj3nszZ/icNBwqYoWowXUanRe3vj5+ePn64NWc+0hCYfdyqWaGoxmK1qdnvBeEeh1l3tCFMVGbVU1RrMVjc6b8IgIfLw0NDdcoqHZiNbbl+jIcNQeOsGxrq6O1157jebmZh588EHi4uJccl673c62bdvYsmULkyZNYtasWZ0Z+hL4HSADcD2I3W6/Evbz589nzJgxLutaU6lUDBs2jAceeAC73c6ePXtoa2tzybk9hd3axt6vP2TWpBl8c7zc3dW5Jb6+vixbtoyUlBR0Oh3Dhw/nnnvucVnYAwQHB/Pggw8SGRnJ66+/TlFRkcvO7UqKYuf8oW1MShvNvy9/j283fsY/PvYgy373Ms0m2zVf47BZKPj2A9JGpvBq7m7aLPa/n89h5UzBBrJGJvHCe99iMFsBhcaqsyx96CE27T2Nw+GZSyMbGxt5/fXXaW1t5aGHHnJZ2ANoNBruvPNOpkyZwpYtW/jyyy9xOBwuO7+4dRL4PciuXbsoLCzk7rvvZtSoUZ1SRkJCAgsWLODUqVN89913PWrNt0bnQ1p2DjEhvvSEd3Xp0iU++ugjBg0axN133+302OzNCAgI4P777yckJIQPP/yQ1tZWl5dxq9QaHcOS04kJDyFj0gweenQJf/zXJ9j4+h/YcqLu7wcqDqy2yzcAWm8/UsZkEhoaQWZ2GiF+Xledz4dRGeOJCg0gPT2D8AAfQE3foelMnnInU7NTrttz4E42m40NGzZQX1/PAw88QJ8+fVxehkqlYsKECUycOJGvv/6aU6dOubwM0XGe96kUHVJZWcn69etJSUlh9OjRnVrW0KFDycjI4Ntvv/XYVl2HqVQ9Yq253W7ns88+A2DWrFmdEvbtAgICmDVrFrW1tXzzzTce2qq7+v9UoaH+EorWF3+fy930NReOsfaDd/mf537LK2u3YHFcDi+VSoXqJ0Y+f/g7nVbnsZ+fw4cPs3//fiZNmkTfvn07rZz2ScL9+/dnzZo1V5b4CfeTwO8BFEXhiy++wMvLi5kzZ3b6BUetVpOTk0NYWBgbNmzAbDZ3anni5h09epQjR44wffr0LlkjHRcXx7hx4/juu+8oKyvr9PI6QqVYKfxuI8/9f7/mmZVf8ps/vkjOoFCwN/Lc716gf1IGE7MTefF3v2H/uXp3V9elWltbyc3NZdCgQaSmpnZ6eTqdjrlz52IwGPjqq686vTzhHAn8HqCsrIxTp05x55134uvr2yVl+vv7M378eM6fP09paWmXlOlqezat5cUXX2TFy69ytrzZ3dVxqS1bthAbG9tlEytVKhWZmZn4+/uzY8cOzxzqUWmIHTCQ+qLD1On687P5k/DWqjGXHmBHkZHmqlJaieR3z/0r0YE3mmymQqUC5QeDPz/82VMcO3aMhoaGW56NfzMiIyNJS0tjz549HjnUczu67QPf1FLF+2+8yjd7TnRJeYq5jo/ffYuPN+9z2Tn37NmDt7c3I0aMcNk5nTFo0CDCwsLYvXu3h3bj/rSAkHCio6OJiopE7+XcWvTu4OLFixQVFZGent6lG+P4+voyevRoDhw44JEXeAU1EbFD+N3//C+a05/z2z+twWxTcFisNDQaSMm5k8lTprJg3mwCvK4X3ArHjx5HrfUnwEdDo8F41e+sWGwqdFrP+ixZrVZ27txJXFwcsbGxXVp2RkYGbW1tHDhwoEvLFdd22we+samaCqMPKYmXZ6vWlp5i65atfLNlO41t1p98bc2VY3fQ2Pbj2b6W1no2rvuC/P0F5O/cyq7CMyi6QHLuzODI3v0uqb/BYODQoUOMHj0avV7vknM6y8fHh+TkZI4cOUJLS0uXlu0Kw9MnsWDBAu6ZdxexEX4AKHY7FqvVM1uoTsrPz8fPz4/hw4d3edkpKSk4HA4OHjzY5WX/FLvdisViwWSyERo3ir/86Xd898YzLP9kJ179RjGUI/zTsyvI37uH9999h/JGG1arGavFgtly+TpgM7WyK/cN1mw9jd4vjBl3JLP+0y+oN1hBsXNy11fYI4YS4u9Z2w5XV1dz4cIFt+yMGBoaSkJCAnv27OnScsW13faBD+AXFEpokB8tFcf482vrGJyUQmJvB8/9cRXW6yyvaa44yl9eW8+Q5FQSY2z8xx/fxPaDY81N1ax++Xme/vXTvPXFHiKieqFW64iMjsRb45px9urqalpbW0lISHDLZKH4+HisVitVVVVdXrarOWxmjh4+xojscRhKzlDd2D2XHZ47d44BAwbg5eV144NdLCwsjF69enHu3LkuL/t6HDYzBwsLGDfnHqwXj1NS20pC9gJW/un/o/ZoHvvPW3ltzbv41x3k/Y+/JG70JBKiNBQePcPcBXMo3Pg+zz//PM+/8Bc27DjDtMnjUGn1PPlfLzN3qINn/vX/8u/P/he7Lqh59MEZeHnYVbW4uBgvLy/69evnlvITEhKora2lqanJLeWLv5On5V1l71drsYSOpXd4EKrwTOr3/CeHax4iNerHa5f3frkGW3gWMWGBqMKyqNv9HEdqH2Z05NWzoTXc88s/cNfksWh1XmjUrg/k9qDt1auXU8e31hSRd+A0lUVn6J0wgtaKM1RrB7PsgYkdKj88PBwfHx9KSkoYMmRIh87hKdRab5Kzp5OcPd3dVekwk8lEdXX1TYzd29j5zSYaDK1catMTqbdx+FQpDz/5FNFBHWup9unTx6NWb6i13uTMfICcmQ9879/vmP84d8xv/ymWv6wch6JSXdkwZ9b9i5l1//XP6xfSm8W/eQa7zQ4qldNbFHclRVEoKSkhMDDQyd02FSrOHqLgTBlV5dXE9u1LyYkD9M26j+lj4ztUh9jYWCwWC5WVlQQFBXXoHMI1POxe1J0cnDx6Cp+gkL8ttNESoq/n+KlrzdZ1cOKHx3rXc/z0j4+tryxi184dfPH5Oi7WuWZ5itVqpbCw8MqXOSIiwsllV1Z27j3JhMlTGRLUyLqCBkYP7U94eDB2Syu7tmziow/e4YMvtmC0Ojcm7+/vT0hICKWlpd1yHL+nOHnyJM3NzVRUVGC1Wp0eqy0t2IZ+8B1MHJfChnc/ZPDYTKIjI/DW/e3SoFj55J3VVLSYnK5LbGwstbW13W5jJpVa3YHd8VRotFqPC/vW1laOHTuGoiiUlpYSGxvrVA+gta2RwrNNzJoxBeO5vVwkgsH9+hAU4AOKg9OFO/l261a++DKPa29Z9GPh4eFoNBrKy7v3ZlY9gbTwr3BgMFpQX9UKV6tVtBmN1zzW2HaNYw3fP9YrIJSRSaPJSBtJ6d5P+c2/vcAbf/0tAT/R0+pMaKrVagoKCjAYDDQ2NhIQEODkBUfLxKlT8NKpOXTwKJPuW8KAMb0YABTtX8/BSn+WPbiQF55eyqaoeOan93finJd3XDMYDNhsts7eP1tch9ls5u233yYtLQ2Hw0FwcLBTr4seMZ5YLy8qC4+hH5jBgJjeDHzkob/9VqHo6D7Wf/kdSbMWOF2X9pZkU1NTp67/F9fn7e3N2rVrefTRR2ltbXW6902rD2Tq5GwcbfWUNNj4eeIgkvpe3sSr/MhXfLKnjX96fBYfr36XNsd4ApxoMmo0GgIDA7vlPJ+eRq7OV6jx8/Wi2fb3LTRtNgf6a25FqsbXxxuDzfb9Y32/f2ybqY0+sX1QA737xnMu/0WK6/8PI6OuXQObzcZ7773n1Hh4W1sbq1atIj09nfj4eOfG7x12jMY2tOpWdh6z8fyIcEyt1dS06IlOyGBWNCh2Gza1N/6+zo//arVaiouL+fOf/9ytJ7t1d3l5eRw6dAidTuf0jZfVbMCGmsL8AoaNnQF2M+cuVDFgQBwtVUWUmwIY1Cfspuqh1WpRFIV3330Xu91+4xeITmE2m3nwwQcZO3as0z0Qit2Goc2Gra6YS9Zw4qL9qK64gD4omm25n2MLncL+PXkExSfhexOdIRqNBpvN2T4B0Vkk8K9QM2TYYM5eqkUBVIqJS63+DBkYimI309BiITQ44MqxCcMGUVR31bGGAIYMDMVhN9PYbCE0xJeNb/w/Cnwm8cI/3oXNakWl88ZLowaufRHUarU8/PDDN6xp+0Y7SUlJVFZWYrPZnAraxpJCnvrDJ/zqH3IwBPZCa7jE/oL9xI2dgk9AEHG+FvZtWU9k+jzGJ0Y7+4fDZrMRHR3NsmXLpIXvJsXFxajVasaOHcvatWudDFqFl3/7JH3m/DPnz5QQNUlP0cnDlJuC6GdqZOe+EwxNScViNtHY2IIS4ocz95V2ux2VSsVDDz1EZGTkLb83cfMcDgd//etf+fOf/8wXX3zh9I3X+d2f8ceNNfxsjBavsF6YLl3k8JHzZNwRi6G5mdDhg8nKGc5/PvkzeieuZlS0c/M87Ha7xw173I5kDP8qaVPvxavuOKWXWig9soPgsQsYHeNDWcFG7v3Z/6Hc+Pfu9rHTF6K7dJyLl1ooObKd0PSFJEd7U3ZgAw889juaHBrSp81nYnIf6uvr2Lb1O8bP+xn9Qv1uuZ42mw0/Pz/mzp1LUFAQBoPBqaGAgOgElj48F23EMFb+9zJKikqJS86mb7AXit3C3q0bKTaFMLa/P2fK6m54vnYtLS34+vp2+ZIf8Xe1tbU89NBDxMTEoFarnew+VTHvsafpHwyP/Mv/MCzUjFEbRsboIdjMVgKCA6ksOU95VQ0lJeVO9960r8H387v1z7roGKPRSFJSEqmpqfj5+Tndnd5n5AQenjWG3ilz+aef30FpRT0pWZkEemsYNGwoPn/btEetWDFbnJuz43A4MBgM8nnwANIcu0pwbBL/+ISWkwfzcai8+d2/Po63RkVkYg6/ub+BuhYHvX3Vfzs2mX9crPvbsXqe+dfH8VariEoczx+fGYm/GgKTsrAeLSB/Tz76/uN55r4U9FoVt7oZl06nY8qUKcDlGdEFBQVYLJYb7qCl0QcyNjPrys9XT+uqv3iUjz7/CptOz07Fj8f/+TdO1aWtrY36+noSExMl8N0oLS0NuDyJUqvVUlZW5tTDUeKHp9I+9zo6KubvvwiKYFzOeIqP5dO7X3/sFovTH9vy8nKCg4Px9/e/uTchXMbf35+JEyeiKAq9e/d2esKcT3A048a19+59//OTNecRqjbuZtf2i0RmPcTovs7Nz2hoaMBsNhMTE3Pjg0WnksD/HhW9Bwyn94Dvb1ii8w3EO7QP8eHaGx7rFRBO8ojwyz9ovEhIziAhufNqHBMTg81m49KlS7d0Bx3WL4U/vfzqTb+urq4Oo9Ho0sdsio7z9/cnLCyMixcvkp6efsvn6z88nf98/ubOc/HiRfk8eAiVSkXfvn05fvw4ra2tt3QT5h3ch/vuuxuD0UJmjt9PPFLo+8rKyvDy8iI62vlhQtE5pEmGQtGRfHYfOn/dI+zmFmKHjsbfBUNQiqWRzblfUmNwzWSmqKgofH193bbRSfs++nL37jni4+MpKipyy4S5lpYWqqqq6N/fuRUeovPFx8fT1tbmkocaqTU6AgKcD3uAs2fPEhwc3CUPcRI/7bYP/KCoBJYueYh+Mdefiaz1CWNgvwiXlKfS+DBkWBq/+eUDNz7YCYGBgQwdOpQDBw5gtf70VsCuZrFYKCwsZOjQoU5u6iG6QlpaGvX19Zw5c6bLyz58+DA2m42UlJQuL1tcW0xMDNHR0W7Zz95gMHD06FHGjBnjsY8Nvp3c9oGv0erpP3AwMb2cW7d86wV602/AIPpG39xSp5+SlZVFU1MTp0+fdtk5nXHhwgUqKirIzs6W2fkeZNCgQcTExHT5/uVWq5W9e/cycuRIac15EG9vbzIzMzl79izV1dVdWva+ffuuPElRuN9tH/g9wcCBA+nbty9ff/11l611tVgsbN++nZiYGAYMGNAlZQrnqFQq7rjjDs6ePdulQz2FhYXU1tYyYcIEac15mJSUFHQ6HTt27OiyHTFbWlrYuXMno0ePdnojKNG5JPB7AJVKxT333MOlS5f49ttvO708RVHIz8+nuLiY2bNn43PNzYmEO40dO5Z+/fqxbt06DAbXbOn8U2pqati8eTNpaWnEx3dsz3XReYKCgpg5cyYHDx7k2LFjnV6ew+Fg/fr1OBwO5s6d2+nlCedI4PcQ/fv3Z+rUqeTl5XV6q660tJStW7eSnZ1NYmJip5YlOkar1XL//ffT3NzM5s2bO7Xnx2QysXHjRnx8fJgzZ45ssOKh0tPTSUxMZNOmTVy6dKnTylEUhYKCAo4dO8aCBQukde9BJPB7kKlTpxIfH88HH3zA+fPXX3VwK8rKylizZg2RkZFMmzZN1t57sJiYGObMmUNhYSHffPNNp4S+yWRi3bp1XLhwgfnz5xMSEuLyMoRreHl5cdddd6FWq1mzZg11dc5vruUsRVE4dOgQ69evZ8yYMYwZM8blZYiOk6t1D6LT6fjFL35BdHQ0H3zwAWfOnHHp3vYlJSW89957BAYGsmjRIpmZ7+FUKhXjxo1jxowZ7Nq1i6+//hqz2eyy87e2trJu3TpOnDjBwoULGTlypMvOLTpHVFQUjzzyCCaTiQ8++ICAnJsXAAAgAElEQVSamhqXndtut1NYWMjnn3/OyJEjWbhwoTQIPIxHzqxRFOXXwAvurkd31dTUxOrVqykpKSE7O5vs7OxbGme3WCzk5+ezdetWIiMjWbRoERERrlmmKDqf3W5ny5YtfPnll/Tv359p06YRHR3d4Yl1iqJQXFzMl19+SV1dHQsWLCAtLU0m6nUjxcXFvP3221gsFqZOnUpSUtItDcU0NTWxbds2CgoKGDVqFPfee29nz+1JVKlUJzuzgJ7II7+hEvi3rrW1lS1btpCXl0dUVBQ5OTkMHDjwph5XarVaKS4uZvv27RQXF5Odnc20adOkZd8N2e12jh07xrp162htbWXcuHEkJSXddBd8dXU1BQUF5OfnExMTw913382AAQMk7LuhmpoacnNzOXz4MImJiWRnZxMbG3tTrXKj0cipU6fIy8ujtbWVadOmkZWV1RWPRZbA7wCP/JZK4LuGw+HgzJkzbNiwgdLSUiIiIkhJSaFfv36Eh4df8w7cZDJRV1dHSUkJBQUFVFZWEh0dzZw5c2S//B6goaGBzZs3s2/fPrRaLYmJiYwcOZKIiAiCgoJ+FNx2u53Gxkaqq6s5ePAgZ8+eRaPRkJOTwx133CEPROnmrFYrBw4cYPPmzdTX19O3b19SU1Pp3bs3YWFh13w+h8FgoLa2lrNnz3Lw4EGamppISEhg9uzZ9OnTp6tu/iTwO0AC/zZgNpu5cOECO3fu5OjRozgcDvR6PeHh4QQFBaHRaLDb7TQ3N3Pp0iVMpv+fvTuPj6q6Gz/+uTOTzGRPJvu+ErIIhACyIypgZBExFAUFRURRQUSFWvvYurTK00dxwdLWWluLID5FUXaQXbYQQoCwmz1kJfsy+8z9/cEv80BFS0L2nPfr5etF4szcb2bunO89557zPQZkWSYhIYHRo0cTFRUllt71IFarlaqqKo4dO0ZaWhrV1dVoNBrc3Nzw9fVFrVYjyzIGg4GKigqampowGAwEBQUxYsQIkpOTb3hxIHRfTU1NnD9/noMHD5KdnY1KpcLJyQk/Pz9cXFxQKBRYLBaqq6upqanBYDDg6OjIoEGDGDFiBMHBwf9x8642JhJ+K3TJb6xI+O3DarXS1NREcXExBQUFFBUV0djYaN+r2sXFheDgYCIiIggODsbNzU0sserhDAYDV65coaCggIKCAqqqquwlmh0dHfHz8yM8PJzw8HC0Wm1HDNUKnchisVBXV0dRUREFBQWUlJSg1+ux2WyoVCrc3d0JCwsjIiLCvo9HJ436iYTfCiLh92KyLF9XdUuSJDFk34vJsmz/D8T5IFy9LXjt+dD8XxcgEn4riALovZgkSaIHL9h1ocZc6CLEBV/PIj5NQRAEQegFumoPPw14q7ODEARBELqk9qsNLAiCIAiCIAiCIAiCIAiCIAiCIAiCIAiCIAiCIAiCIAiCIAiCIAiCIAiCIAiCIAiCIAiCIAhCzyDJslzb2UEIgiAIgtC+JLl5KyRBEARBEHossXmOIAiCIPQCvS7hX7vn97V7f7f2tdrSv8d08uRJjEZjmx5DEARB6J266m557ebgwYMcOnQIWZY5evQoffv2Zfny5UiShCzL9j3Bm5OuLMv2PaGbk3HzY3bs2EFcXBzh4eHXPad5T/FrLwiu/d21r9EsKyuLTz/9FH9/f9RqNQsWLGDfvn2Eh4fj4ODwkzFcG+e1r/nvsQhdm81mQ6fTXfc7FxeXVn1+VqsVSZLaZC9zq9WKwWAAQK1Wo9fryczMZMyYMbf82kL3Z7Va0ev1wNU2R6lU4uzs3KrXslgsqFRtk5JMJhMmkwmFQoFGoyEvLw+lUklERESbvH531esS/ujRoxk9ejTFxcWUlpaydOlSmpqaWLNmDXq9nqCgIFJTU/nss8+wWCw0NjYyatQoBg0axIYNGygqKsLV1ZWZM2eyadMm9u7dy6RJkwgJCeGrr75CpVIxfvx4goKC+PTTT3F3d6euro7Zs2fj6enJ6tWrMZlM+Pj4kJqaaj/BT5w4wd13382ECRNwcHBAkiTMZjOfffYZAIMGDWLYsGFs3ryZ0tJSHB0dmTVrFufOnWP//v1oNBpcXFyYPXs2BQUFbN68GYARI0YwePDgTnu/hZvT2NjI5s2bMZvNXLx4kbNnz7J69WpcXV0xmUyoVCpUKhUWiwVZlrFarTg6OqJQKLDZbNc95ssvvyQxMZGEhARUKhUmkwlJknB0dMRms2G1WrFarfbHw9UGUpZlHB0dr7vIePfdd9FoNLi6upKYmEhYWBgHDhxg6NChKBQKHBwc7MeXJAm1Wg2A2WzGZrPZj9v8u2vjFrq/yspKtm/fjizL7N27F29vb/7whz8AVxN482dtNpuBqxe2zeeYxWLBYrHY27uVK1cyf/58nJyckCTpunPaarXaz93m15Rl+bpzu1ldXR2/+c1vGDBgALIsc88995CXl4dCoSAgIAAHBweUSqX9+Dc6RvNjmo8B2M/t7qzXJXy4ekK8++67zJkzB19fX3tyfPrpp/ntb3/LoEGDSE9PZ9GiRXh4ePDHP/4RDw8Pjh49yu9+9zv++c9/8t133zF8+HCSk5OJj4/nhRde4JlnnkGlUvHhhx+yePFizp07x/vvv8/x48f58ssvCQ8PR6/Xc+edd/L3v/+dhIQE+vXrB8CYMWNYuXIl27dvJykpiUceeQSTycT48eMJDg7m7bffZtiwYYwaNYrq6mo+/vhjMjIyqKmpwWQysWjRIpYvX87p06dZu3YtKSkpODs7s3r1ahISElp91S10DHd3d2bNmkVDQwNvv/02v/vd73B1dWXVqlU0NjZSX1/Pyy+/zLZt2zh79iwajYbIyEh+8YtfsHr1asrKyuznwaFDh8jIyOD+++/HZrOxd+9eZFnm/vvvx8PDg48++ojQ0FDKy8v57W9/S2FhIevXr0epVJKYmMjkyZPto0fZ2dksW7aMwMBAnJ2dKS0t5dixY/zpT3+ivr6e5557joKCAvbv309lZSVTpkwhISGBl19+mYiICOrr63niiSdQKBSsXbsWSZIICgpixowZbdabEzqPv78/jz76KIWFhZw7d46lS5diMpl455130Gg09tHKd955B0dHRxoaGpgyZQpxcXF88MEHKJVK1Go18+fPZ8uWLSiVSlJSUjh8+DDFxcXIssyTTz7J8ePHOXLkCG5ubnh6ejJv3jy2bNnChQsXMJvNpKamEhcXB1y9CFGr1UyePBlPT08cHR05e/Ys3377Lenp6QQEBPDII4/wzTffUFxcTF1dHc8//zzHjh1j+/bt+Pn54eLiwvz58zlw4ADHjx/HaDQybdo0+vfv38nv+K3pdZfZFouFjz/+mDFjxth7vrW1tYSFhaHRaPDz86Ourg5XV1dCQ0Px8PBAr9dTX1+Pr68vTk5OhIaGUllZiUqlsvdUdDodAQEBaLVa+9Wrj48Prq6uBAcHU1dXR0VFBSUlJWRlZTF06FD8/f3tcUVERLBixQreeOMNjhw5wqlTp3BxcSEiIgK1Wo0kSVRUVPD2229z5MgRampqqK6utj/X0dGR4OBgSktLKSsrIzs7m7y8PO655x7RsHYTBoOBv/zlLwwdOpR+/fpRVFREQUEBy5YtY+jQoWzatImKigpGjBjBwoULOXv2LBcuXCA3N5cXX3yRgQMHsnXrVgYOHMhjjz3GkCFD2LhxI08//TRz5sxh/fr1NDQ04OzszOLFi0lKSmLXrl2sXr2aoKAgoqOj2bx5M42NjcDV20Hz5s3js88+45e//CXbtm0DICoqisWLFxMYGMi5c+cIDw9n2LBhREREsHr1aqxWK/X19SxatIgJEyawZcsWvvjiCwDi4+PZu3cvVVVVnfY+C22rpqaGjz76iFmzZuHr68uePXsIDQ3lpZdeQqfTcenSJaqrq3nwwQd58MEH2bdvH3v37iU4OJhf/epXlJWVUVZWxtixY3n22WftCfrll18mPj6erVu3cuXKFUaPHs3SpUvJzc2luLiYf/zjH8THx+Pp6cmmTZvstzEjIiJISkriD3/4A8uWLSMvLw9ZlrnzzjtZvHgx2dnZNDQ02L9nVVVVHD16lNraWqKjo3nxxRepr68nMzOTtWvX0qdPH6Kjo1m/fj1Wq7WT3+1b0+sywbfffsu+fftISkpi//79eHl50b9/f1avXo3ZbKaoqIjIyMgfPS8iIoKysjI2bNjAkSNHeOSRR7h8+TI7duxAoVAwZMgQPvvsMzQaDeHh4Wg0GnJzc9m8eTOnTp1iyJAhREREUFFRgb+/PzabDXd3d/vrnz59mqKiIhwcHADw8/P7UQwmkwmbzUZQUBA2m81+3/67777Dy8uLkydPMnXqVMrLy2lsbCQgIABZlkXC7wZsNhtbtmzBwcGBiRMnAlcvTpsv9pycnKiqqsLBwQGtVmsf1jQYDPZ/Nz+m+YKzeUjdwcHBfl7JsoxGo0GSJDQaDQaDAYvFgqenJ0FBQTzzzDM4OTnZ4xo8eDC33347+fn5/OpXv6Jfv374+vraYzKZTPztb38jIiICrVZrv5/bHJNarbbfT9Vqtfj4+LBgwQI8PT07/k0W2pzJZOKf//wnI0aMYMCAAcDV87b5HGv+/F1cXHBzc8NkMmEwGDCbzWg0GgA0Go19yL/5dlPzML9Go6G6uhpHR0f7nBYHBwf7LSitVoufnx/+/v72W1GSJDFz5kwefPBBvvjiCzZt2kRCQgJarRaFQoEkSVRVVfHpp58yYcIEXFxc7Odt8+0EBwcH+9wVLy8vQkJCGDZsWLe/FaV87bXXXuvsIDqSQqEgKSkJjUaDUqnEycmJ+Ph4oqOjkSSJSZMm4evrS2RkJH5+fjg4OBAdHU1YWBhJSUlYLBbGjBlDXFwcwcHBaDQanJ2dGTNmDGq1Gn9/f+69916MRiPZ2dmMGjWKvn372nv04eHhGAwGfHx88Pf3t59AzSe9SqUiJSWFiIgIgoKC8PHxsccQERFBTEwMkiRxxx13EB8fz+XLl/H19SUsLIx77rmHwMBAEhMTcXFxQaFQEBoaipeXVye/68J/UlhYyDvvvEN8fDwFBQXk5OTQt29f0tLSyMnJIS0tjTlz5lBcXExgYCC+vr6cPn2asWPHkpWVxblz58jMzGTGjBnIssyePXvQarU4Ozuze/duTp06xYgRI/D09GT9+vXodDoOHz7M3Llz8fPz4/jx41itVpqamoiPj7cP6f/tb3/j4sWLHD9+nD59+nDbbbeRk5PD7bffTk5ODp6enuh0OmpraykvL8dsNjN27Fj+/ve/YzAYSE9Ptw/hHj9+HFmWqaysJD4+3n4RInRfBw8e5JtvviEyMpJLly5RXFxMcnIyGzZs4PLly5SXlzN16lTOnDnDoEGDMJlMFBQUkJKSwsaNG8nLy+PKlSukpqaSk5PD+fPnCQsLIz8/335ep6amcvnyZfbs2cPly5fR6/VMmjQJk8nE5cuXaWhowNfXF19fXwAqKir4/PPPycvLIzMzkwkTJqBQKHB0dCQoKIhTp06RlJTEqVOnkCSJS5cu0b9/fwwGAzt37qS6upra2lpSU1MxGo3k5uZiMBiQZZmIiIhuPRFaFN5pJ5WVlXz77bfMmzevXY9z4MABJEli9OjR7XocoX0ZjUbKy8vtw5IKhYLAwEAsFguVlZW4ubnh4eFBQ0MDjo6OODo6UldXh7u7O2azmcrKSlxdXfHw8MBqtVJWVoaTkxMeHh5cuXIFhUKBj48P58+fZ9++fUybNg0XFxc8PDyQZZmamhp0Oh0eHh64ubnZ46qvr6e+vh6lUmnv2Tc2NuLh4UFTUxNKpRKFQsGVK1fsIwMqlYo333yTF198EQcHB7y9vYGrc2caGhpwcXHB09OzWzecwlUNDQ32W4sADg4OBAQE2OedeHt7o9Fo7OeqzWajqanJfi7X1dXh7e2Nk5MTBoOByspKtFotSqXyunN6zZo19O/fHy8vL3x9fVGr1VitVioqKpBlGR8fH/vEPZvNRnV1NXq9HmdnZ7y9va9badIcS2Njo/18dHR0ZNu2bVgsFkaNGoWXlxfOzs5YrVYqKyuxWCxotdrrRr+6o3ZJ+OXl5Zw7dw4XF5e2fuluQ5ZlzGbzdbNH24PFYgHolsP2VquV4OBgwsLCOjuUXqOoqIiLFy8ybty4djuGXq/n66+/ZtasWSKpC23i4MGDxMbG3vBWZ1tJS0tDqVT26FVN7ZLws7Oz0ev1xMbGtvVLCz1ITU0NhYWF3H777R12zD179lBTU9MtL5DaSvPcj+5+jLbW2NhIXFwcgwYN6uxQfmTHjh3odLpufw+5tTrqnIXuV7uktLSUBQsW3NRj26XVa14X2RPWLQrtpzPODycnJ0aMGGGfMCQIzUpLS7l8+XJnh3FDHh4e3H333b36QlW4sW+++eamH9vis8dsNrNv3z7UajWjRo3izJkzWCwW4uPjb+r+hpgy0Dt1t6tmQehIzSsqJEnCZrMB9NrevNB+Wpzwy8vL8fb2pqysDJ1OR1VVFdXV1URHR+Pk5MSVK1c4cuTIDe+D/PWvf2Xr1q1i1ngvU1xczMcff0x4eHhnhyK0I1mWKS4utk+qEm5OdXU1X375JWFhYaSkpLB+/Xqio6NJSkpCpVJhs9nsFwFC25JlGaPRSGlpKWFhYSiVys4OqV21OOGrVCp0Op29xOfIkSMpLy9n//793Hffffj6+jJ8+HD7ZLJ/f+6SJUtEHe5e5re//a3o4fdgNpvNXqMiIyODqKgoXnrpJXHb5CaVl5dzxx13kJubiyRJhIeHU1NTQ2NjI56enlRWVlJcXNzZYfYYsiyj1+vJz8/n+++/59y5c+h0OgYOHMjDDz+Mh4dHZ4fYblqc8H19fSkpKbH30uvr66mrq2PEiBFtHpwgCF2X2WymoKCA7777jpycHCZOnMjjjz/Ohg0beO+991i4cOF1S/yEG/Px8eHQoUOo1WosFgtxcXGcPn2apqYmPD098fPzIzQ0tLPD7Naaqz/m5eWRkZHBxYsX0Wq1jB49mocffhi1Ws22bdt4/fXXSU1N5fbbb++RdSJanPCVSiXJycn2n93c3PDx8WnToARB6LosFgs//PADu3btorKyktGjRzN37lx7j/7BBx9k/fr1rFy5koULF15XUVL4MR8fH4YPH46rq6t9A5f4+HjRrt4iWZapra3l3LlznDx5krKyMrRaLcnJycyYMeNHPfkpU6aQlJTE2rVrycjIYPr06QQGBvao0Ukx5VMQhJtisVjIyclh48aNNDU1MW7cOJKTk3+0MZNSqSQ1NZWNGzeycuVKnnnmGTFv52dIknTdvhrdvbhLZ2ruyV+8eJHDhw9TVlZGZGQkgwYNom/fvnh4ePzkZEhJkggLC2PJkiXs3buXDz74gJSUFEaOHNnu9VQ6ikj4giD8LLPZzJkzZ/juu+/Q6XRMnDiRgQMH/uyQp0qlYurUqahUKlauXMmzzz5rr7gnCG3JarVy5coVzp49y+nTp6msrCQwMJCxY8cSHx9vr+t/s9RqNSkpKSQlJbFmzRoyMjL4xS9+QVhYWLfv7YuELwjCDdlsNjIzM9myZQuOjo6MGzeOfv363fQMfKVSycSJE1EqlXz00UcsXLhQJH2hTciyTFVVFenp6WRkZGAymYiKimLs2LFER0fj5uZ2y8k5ICDAvt30n/70J0aNGsU999zTre/ti4Qv9ChWqxVJkuzDdlartccvtWlrRqORrKwsNm7ciLOzM6mpqfTp06dVw5rNm0GpVCo++OADnn322euGrwXhZlmtVqqqqsjIyCAtLQ2dTkf//v2ZMWMGQUFBODs7t3ntAkdHR8aOHUv//v1Zt24db775JvPmzeu2S4xFwhd6DIPBwJo1awgJCWHChAnU1dXxySefMH/+/B691KatmEwmjh8/ztatW3F3d2fmzJnExsbe8gWTUqlk/PjxKJVK3n//fV544QX7zmaC8HNkWaa0tJS0tDROnTqFXq+nX79+PPLII4SGhnZIvQdJkvD29mbBggVkZmbywQcfMGLECKZMmdLt6k2IhC/0GBUVFfTr14+amhosFgvnz5+nT58+9uqOpaWlZGdnM3DgwE6OtGuRZZm0tDRWr15NVFQUjz/+OGFhYW1axlWhUHD33Xej0Wh46623+PWvfy1moQs/qb6+nh07drBv3z5cXFwYOnQojz76KMHBwTg4OHTKvfTmjXViY2P58ssvWbZsGUuXLiUkJKTDY2ktkfCFHkOr1XLgwAE8PDywWCxYLBZOnz5NQkICnp6eBAYGEhMT09lhdhkGg4EjR46wYcMGQkJCeP311/H29m63xlSSJEaNGoWjoyOvv/46v/71rwkICGiXY3UnZrOZXbt2ERMTQ58+fTAYDBw8eJCxY8f2mtr5ZrPZ3pM/evQoer2eCRMm8NZbb+Hu7t6lJsu5u7vzxBNPkJOTw/LlyxkxYgT33Xcfrq6unR3af9Q7ziahV3B1dSUlJQUnJyckSWL06NEMGTKkxyypaStNTU0cPHiQnTt3EhERwS9/+UuCg4M77Pi33347CoWC3//+97zyyisEBgZ22LG7osLCQry9vblw4QIxMTFkZ2dz8eJFRo4ciUqlwmQyYTabOzvMNmcymbh8+TJHjx7lxIkTaDQaBg8ezNKlS/H39+9SSf7fSZJETEwM//3f/8369et58803mTNnDvHx8V16DwSR8IUe5d+HiUV516tkWaa+vp6jR4+yfft24uLieOmllwgICOiUhnXw4MGoVCrefvttXnzxxW47CaotNG/9KkkSOp2OY8eOUVJSQnV1NcHBwZSWllJSUtLZYd4ym82GwWCgpKSEY8eOceLECZycnBg2bBgvv/wyXl5e3W6CrYuLC7NnzyY7O5u///3v9O3bl/vvvx9PT8/ODu2GRMIXhB6sefnSwYMHSUtLIzIykldeeaVLTJpLSkpi3rx5vP/++yxcuJDo6OjODqlThIWFkZeXR0REBLIs8/jjj3Px4kX8/PwACA8Pp7S0tJOjbB1ZlmlsbCQnJ4dTp06RnZ2NSqVi8ODBvPLKK2i12s4O8ZYpFApiY2P57W9/yzfffMMf/vAH7r//fpKTk7vcLZmuFY0gCG2iuazojh07OHXqFImJiSxevLjLDZUOGDCAefPmsWrVKubPn09cXFxnh9ThHB0dGT9+/HW/69u3bydF0zZ0Oh2XLl3i0KFDFBcX4+PjQ79+/bjnnnvw8/Pr0sPeraXRaHjwwQdJTk7myy+/JC0tjTlz5nSpFUItTviyLJOfn49arSYoKAiAvLw8AgMDxfCpIHQyWZYpLy9nz549nDp1isGDB/PSSy+h1Wq7VKK/VmJiIo8//jiffvopc+bM4bbbbuvskIQWstls1NXVkZ2dTUZGBnl5efj6+jJy5EhmzZqFu7t7txuubw1JkoiNjWXZsmXs3r2bN954g2nTpjF06NAuUbCnxQm/urqas2fPotfrmTJlCmazmX/+85/MmzePkJAQLBYLDQ0Noh60IHSw0tJStm/fTnZ2NsnJySxbtqxbVLaTJImEhATmzp3LZ599xqxZs+jXr1+XvUAR/k9NTQ1nzpzhxIkTVFVV4evry8CBA5kxYwZeXl699jNUq9VMnDiRxMRE1q1bR3p6OjNnzuz0VSktTvhNTU2EhoZSUlKC2Wxm69ateHt7U1FRQUhICFarFb1eL3r7gtABmnv0GzduJDs7mzFjxtgnDXWnxlaSJOLi4nj88cf55JNPmDlzJklJSd3qb+gNmu/Jnzp1ioMHD1JTU0NUVBQjR44kKioKDw+PXtGTv1nh4eEsXryYgwcP8s4775CSktKpyy1bfFStVsuxY8eQJInGxkbGjx9PZmamfQtMtVqNn58fFoulzYMVBOEqm81GcXEx3377LYWFhYwbN46HH34YFxeXzg6t1ZqHQxcsWMCqVauw2WwkJyeLpN/Jmid+njx5kuPHj1NRUUFcXBxTpkwhMjLSvgxWuDGNRsPdd99N//79Wbt2LceOHWP27NmEhIR0+PvW4oTv6urK5MmTUSgUKBQKVCoVY8eO7ZGTMAShKyouLmbt2rVUVlaSkpLC3Llzu3Wi/3dRUVEsXryYFStWYLPZGDx4sEgonaCxsZGDBw9y4MABLBYLCQkJTJkyhaioqBbvQNfbSZKEn58fzz77LEePHmXFihXcfffd3HvvvR06ItKqcYV/H64XQziC0L5sNhtFRUV8+eWXFBcXM2vWLJKSkrpdLe+bFRoayrJly1i+fDk2m43bb79dJJh2ZrVaqaurIyMjgz179lBbW8vIkSNZsGAB/v7+ODo6is/gFjk4ODBq1Cj69+/PP//5T1599VWefvrpDuvti2V5gtCFWa1WcnJy+Prrr6mqqiI1NZUhQ4b0iovswMBAXn31Vd544w2sVivDhw/vkQnHaDSya9cuIiIiSEhIoLi4mKKiIvr379/uIzcWi4WKigoyMjLsJW0HDBjAM8880ylDzr2BJEl4eHiwcOFCMjMz+Z//+R/uuOMOJk2a1O5z30TCF4QuyGw2k5+fz7p169DpdDzwwAMkJSV1iaU9HcnHx4fXXnuN119/HavVyqhRo3pcEiosLCQoKIi8vDwSEhJwcXHhwoUL9OnTx/7vS5cuMXjw4Fs+lizLWCwWqqqqSEtL49ChQ0iSxMCBA3nqqacICgrqcsVieipJkkhOTiY2NpY1a9bwm9/8hgULFhAZGdlu57j4ZIUepaSkBBcXFzw8PKirq8NoNKLVartNI2YwGDh//jzbt2+nsbGRGTNm0K9fv149R0ar1fLGG2/w5ptvYjQaueuuu3rU++Hg4EBjYyNw9daNs7MzsbGx6HQ6AOLi4qitrW3168uyjF6vp7i4mKysLPs2s801Gnx9fXvcRVR34urqypNPPsn58+f54x//yJAhQ7j33nvbpWBP92gFBeEm1NfXs3fvXtzd3Zk0aWmF59cAACAASURBVBI6nY7MzEzi4+OJjIzs7PB+lslk4sSJE+zevRulUklKSgr9+vXrNhcq7c3Dw4NXXnmFFStWYDabueeee3pM0g8JCaGsrIzExESMRiN1dXV4eXnZS+u2lsFgID8/n/T0dHJycnB0dLQvfQwJCekVt4W6i+ZaFK+//jpfffUV77zzDtOnT2/zi33Rmgg9Rn19PdHR0dTV1QHg5uaGzWazF5/JycnhzJkzDBw4sDPDvI5er+fUqVPs2LEDZ2dnpk6dSmxsrNjh7wa0Wi0vvPACH330ERaLhYkTJ/aIpKVSqRg2bJj9Z2dn51btICjLMjqdjqKiItLT0zl37hwuLi7cfvvt3HXXXfj5+fW6W0LdjaurK7Nnz+bixYt88cUXnDhxgqlTp7bZngMi4Qs9hq+vL4cOHcLPzw+9Xs/Ro0dxdXW1T4SJjo6moqKik6O8SqfTkZaWxoEDB3Bzc2PGjBn07du3x/Ra24tWq2XRokWsWrUKi8XClClTev0oSENDAz/88AMnT54kPz8fJycnBg4cyJIlS8RwfTekUCiIj4/n5ZdfZvPmzaxYsYLJkyfbd5i8Fb37myL0KGq1mvvvvx+lUokkSYwePRqbzdalEoLJZGL//v3s3LmTyMhIZs2aRWRkZJeKsavz8vLi2Wef5S9/+QtfffUVqampvfL9k2WZNWvWcPLkScLCwujfvz+TJk3C29u7V74fPY2zszPTp08nOTmZdevWkZaWxrPPPntLn604K4Qe5dp16V1puLexsZHvv/+eXbt20adPH5YsWYK/v3+XirE78fT05Omnn+bjjz9m3bp1PPTQQ70uyUmSRHl5OQ888ABDhw4V51IPpFAoiImJYfbs2fztb3/DZrPd2uu1UVyCINyATqfjm2++4fXXX6ekpIQXXniBJ598kqCgINFA3yJ3d3cWLFhARUUFa9euxWw2d3ZIHc7R0RFXV1dxLvVwDg4ObVL4SCR8QWgHer2eb7/9lhdeeIH6+npefPFF5s6dS3BwsLhP34ZcXV1ZsGABV65c4fPPPxd7eAjCz2hVy1NTU0N9fT1wtWG7cuWK+KIJvZ4sy9TW1rJ+/XpeeOEFampqeOedd5gzZw4BAQEi0bcTZ2dnFi1aRG1tLZ9++mm36+k3nzdGoxG4uiNpfX09six3cmRCT9PiFqi6uprvv/+eHTt2YDAYsFgs/PDDD6SlpQFXS4E2F4wQhN6gucFeu3Ytr776KkajkeXLl/PYY4/h6ura2eH1Co6OjixatAij0cjHH3/crZJ+RUUF27dvZ9euXciybG9jm1eUGI1GTCZTJ0cp9AQtTviNjY2Eh4fj6uqK2WzGycmJK1eu2Nd31tfXc+nSJXF1KvR4NpuNsrIye6LXaDS8/fbbPPzww+1SJUv4eSqVigULFqBUKvnTn/5k7zF3ddXV1fTr18/eZnp6emKxWOxbjhcVFVFcXNyZIQo9RIsTvpeXF0VFRVgsFmw2G7W1tURFRdmH9L28vEhKShJrP4Uey2azUVhYyGeffcYHH3yARqPhrbfeIjU1VfToO5mDgwNPPPEEzs7O/PnPf6apqamzQ/qPAgMDOXv2LE5OTuj1evbs2YOvr6+9ExUTE9PlK0UK3UOL17G4ublx9913o1AoUCgUyLKMRqPpUftxC8KN2Gw2Ll++zNatWyksLGTUqFFMmzYNT0/Pzg5NuIZKpeKxxx5jzZo1/PnPf2bBggVdun3y9PRk6tSp9voRKSkpyLIsZt4Lba5VC1ednJyu+1mUARV6MqvVSm5uLt999x3FxcWMHTuWOXPm4Ozs3NmhCT9BpVIxa9Ys/vWvf7Fq1Sqeeuop+xB5V9RV60cIPUvvqlQhdGuyLGOz2TqsQZRlmZycHDZs2IBOp2P06NE8+uijXbq3KPwfBwcHfvGLX7BhwwZWrVrFggULOmU0xmazIUmSuM0pdLobJnyj0ciWLVuIjIwkNjaWyspKwsPDOzo2QQAgKyuL/Px8Ghsbqa+v59FHH7XXx28PVquV7OxsNmzYQGNjI/fddx+33Xab6NF3Qw4ODkybNo2NGzfyxz/+kYULF3bYhMoTJ04QEBDA119/jVarZfr06WI0VOhUN0z4GRkZJCYmkp2dTW5uLu7u7iLhC52msbGRCxcuEBcXR1NT08+WUK2rq0OtVqPRaDAajej1ejw8PG6qd2W1Wjl79iybN2/GaDQyefJkBgwYIBrpbs7BwYH777+fLVu28P777/Pcc8/h5eXV7sfNycmhsbGR4cOHU1VVRVNTkziXhE51w5bTw8MDjUZDSkoKO3bs6HU1qoWuZdiwYfTp04edO3fSp0+fnzwfdTodmzZtQqvVkpKSwtGjRzEYDPTp04eoqKiffH1Zljl9+jRffPEFLi4uTJo0icTExOvuqwrdm1KpZPLkySgUCpYvX87SpUvx8fFp12OOGzeOr776iqKiIu68884uPYdA6B2uazmtVisXL14kPj4euLo5w7333ivW1AudQqfTcerUKYYPH46Pjw/Tp0//2YvPyspKYmNjqa2txWazYTQaCQ0NpbGxEbja4zpz5gwDBw780XMLCwtpbGxk2bJlbbb3tNB1WCwWLl68yOHDhzEYDO1ayKaxsZGzZ88ydOhQ5s2bh8lkEhePQpdwXespSRK7d++muLiY8PBw/vd//5clS5aISUpCp9BoNJw/f54rV65gMpk4c+YMr7322k8+3tfXlx07dhAQEIBer8fR0ZELFy6QnJwMQHR0tL162bUkSWLy5Mmo1Wreffddnn/+eXx9fdvrzxI6kNls5uTJk3z77beoVCpmz55NXFxcu06gc3Z25uTJk1RWVtr3qn/11Vd/8vHNdR28vLzw8PCgoqICWZbx9/dvtxiF3um6hK9QKJg0aRKLFi3CYDDwxz/+USR7oVP5+fnxhz/8gYSEBN59992ffayTkxOPPfYYCoUCSZIYM2YMFovFXsDk50iSxLhx45Blmffff58lS5a0+5Cv0H6MRiNZWVmsX78ed3d35syZQ3R0dIet8PD19WX58uUMHjyYt95662cfW1ZWRlZWFgCTJ0+mtraWS5cuMXnyZODqfiV6vb7dYxZ6vusq7VksFj7//HPeeOMNZs2axdGjR295/11BaC29Xk9lZSWbN2/mrrvu4ssvv/yPz3FwcECpVNoLQ7VkS0mFQsGECRMYP348K1asoKSk5Fb/BKGDNTY2sn//fn7/+9+za9cuFixYwK9+9StiY2M7LNnrdDoaGhrYunUrgwYN4quvvvrZx9fX1xMREWE/T/38/K7raFVUVFBZWdmuMQu9w3U9fJVKxa9//WuUSiVJSUls2bIFg8EgliMJncLFxYXHHnsMgNTUVI4dO9bux5QkibFjxyJJEh9++CHPPfccQUFB7X5c4dY0NTVx+PBh9u3bR2BgoL1H3xlr311dXXn00UcBeOihh+wbi/2U4OBgNm7cSEhICA0NDVRUVFBQUIDRaEStVhMeHk5paWlHhC70cD+aAdV8FaxUKpkyZYooFiF0CUqlkuHDh3fY8caMGYOjoyPvvvsuL774okj6XZAsy9TV1ZGWlsa+ffuIiIjgqaeeIiQkpMtsRaxSqRg5cuTPPsbNzY2ZM2fa21o3NzdiYmK6zN8g9Bw/u95OJHuht5IkieHDh+Po6Mg777zDokWLxAYmXUhtbS179uwhMzOTsLAwnn32WYKDg7ttm/Xvyb27/h1C19biBfYGg4HNmzfj5ORESkoKOTk5ZGZmMmTIkJ9d6ywI3VFycrJ9eH/x4sVERER0dki9WkNDA9u2beP48eMMGDCAp556isDAQFF/XhBuQosTfmVlJZGRkZSVlaHX64mJicFoNFJVVUVUVBR6vZ7CwkICAwPbI15B6FCSJDFw4EA0Gg3vv/8+zzzzDLGxsZ0dVq9TVVXFd999R1paGsOGDWPZsmV4e3uLnrAgtECLbxIplUr0ej1msxlJkqisrCQ7O9tezESj0RAUFCS+iEKPIUkSCQkJPPnkk/z5z3/mwoULnR1Sr1FbW8s//vEPfv/736NUKvmv//ovZsyYgY+Pj2hjBKGFWpzwm4tBREREUFtbS0lJCVar1V7QRJIkUYpX6JHi4+N58sknWbVqFZcuXerscHosWZapra3l008/5Ve/+hVarZbXXnuN6dOni169INyCFmdmhULBqFGj7D8HBweTlJTUpkEJQlckSRJxcXG88MILvPfeezz++OP0799fJKA2IssyZWVlbNq0idOnT5OSksL777/fK8rSXruFrizLyLIsZukLbU50xQWhhSIiInjuuedYtWoVs2fPZsCAASLp3wKbzUZZWRlff/01eXl5TJgwgYcffrjXVPlsampi27ZthIaGMmTIEDIyMqirq2PIkCH/cStfm80m9jrp4WRZxmq1tkkRPJHwBaEVoqOjWbx4MR988AEWi4Xk5GTRI2shi8VCQUEB27dvJycnhylTpjB//vxe0aO/VlFREXFxceTn52O1WmlsbMTT05OioiI8PDz44YcfyM7OZvDgwdc9rznZ79q1i8DAQHx9fcWFZw8hyzJ6vZ7S0lJOnz5NWloarq6ut/y6IuELPUZxcTF6vZ6oqChkWaaoqAhZlq8rW9qWwsLCWLJkCR9++CFms5lhw4aJBvcmWK1WsrOz2b59O5WVldx5553Mnz+/1+4V7+rqSlZWFjabDYvFgtVqpa6uzr5rY58+faiqqvrR8xQKBc888wxbt27lvffeIyUlhZEjR4o5VN2YXq8nPz+fzMxMLl26hFKpJCEhwV5n4lY7FeLMELq1a4czMzIy8Pf3x8PDA29vb9zd3dm/fz8BAQE4OTkhy3Kb7w0REhLCokWL+OCDDwBE0v8ZZrOZ3NxcNm7cSH19PSkpKQwaNAiNRtPZoXWqwMBAqqur8fPzQ5ZlEhMTqa+vJyws7D8+19HRkalTpzJw4EC++OILMjMzeeihh/D39xfnYTcgyzIGg4HCwkLS09M5e/YsLi4uJCcnM3/+fPz8/G5q86+bJRK+0Gna4t5jaWkpZWVlaDQarFYrPj4+9iWjV65cwcfHxz5EXF5eTn5+PoMGDbrl414rNDSUl19+meXLl2M0GhkzZowY3r9G89bGu3fvpqmpiYkTJ5KcnCx6ov+fUqmkf//+9p+dnZ1bVMdEkiTCw8N56aWX2LNnD++++y4TJkzgjjvu6LWjJl2ZLMs0NDSQk5PDyZMnyc3NRaPRMGjQIF544YV23ZpbfOOEbi0oKMhe576qqorCwkIGDx5MTU0N6enpDBgwwH5hERAQ0G7VIH18fFi2bBnvvfceZrOZ8ePHt8txuhOr1UpmZibbtm1DrVZz55130q9fv17fo28vKpWKCRMm0K9fP9atW0daWhpz584lODi4s0MTuFql9uzZsxw6dIiKigp8fX257bbbSElJwc/Pr0OqRYqEL/QYzctFm5c2zZo1C/hxnfL24ufnx0svvcSKFSuw2WyMHz++V/b0jUYjp0+fZtOmTbi4uDBt2jRiY2NFb7ODBAYGsnDhQtLT03n33Xe56667GDdunLjQ6mDNPflLly5x9OhRcnNzCQ0NZeTIkURHR+Ph4dHho1wi4Qs9xrX3LJvXNHc0b29vli5dyooVKzCZTEyaNKnXJH2z2Ux6ejqbN2/Gy8uLmTNn0qdPHzF03wkcHBwYMWIEcXFxfPHFF7z99ts8+uijYr+TDtDQ0MDp06c5evQo5eXlhISEcPvttzN79mzc3d07dW6F+CYKQhvz9PTk+eef58MPP8Rms3Hffff16AlUNpuNI0eOsG7dOiIiIpg/fz6hoaEi0XcBWq2Wp556iqysLFauXMnw4cO5//77xWhLGzObzRw/fpxt27ZRXV1NYmIid911FzExMbi4uHSZi37xjRSEdqDVaq/r6U+bNq3HJUC9Xs+RI0f45ptvCA8P59VXXxVrwbsglUrFwIED6du3L2vXruWVV17hqaeeIiYmRnxWrWSz2airqyMrK4sDBw5QUFDAgAEDePTRRwkPD0epVHbJ97ZVLVDzJKjme6XN/xYE4f+4uLiwZMkSVq5cyfr165k+fXqPSPpNTU0cPHiQnTt3EhUVxS9/+UuxYdYtKCkpwWg02rdezs3Nxc/PDzc3tzY9jrOzM/PmzeP8+fP85S9/oX///kyfPh1nZ+c2PU5P1ZzkMzIyOHDgAE1NTcTGxpKamkpMTEybLp9rLy1ufUwmE99//z1qtZoRI0ZQXl7OoUOHmD59envEJwjdmqurK4sWLeKjjz5i/fr1pKamdouG4d/Jskx9fT1Hjx5l27ZtJCQksHTpUrHeu5Wa6+VLksSRI0fw9fXF19cXFxcXysrKMBqNJCQkAFdnd+t0ujY5bvPOj2+88QZff/01r776KvPmzaNv374dMku8O5FlGbPZTHV1NWfPnuXgwYNUVVWRnJzMY489RnBwcLerCtnihF9RUYGnpydlZWXodDoCAgKuuz9RW1vL6dOniY+Pb9NABaG7cnV1tff0165dy0MPPdRtGgpZlqmpqWH//v0cPXqUqKgoXn31Vby9vTs7tG6tvLyc2tpaNBoNNpsNrVaL1WpFkiR8fHyuq1FRXV1NXV1dmx7f2dmZRx55hGHDhvHJJ5/Qp08fHnjgAby8vNr0ON2R0WiktLSUrKwssrKyaGxsJCYmhkceeYTIyMgucz++NVqc8FUqFTqdDovFYv+d2WzGarWiVCrx9PSkX79+WK3WNg1UELoztVrN008/zV//+lc+//xzHn300S49vN+8Re3OnTvJyMigf//+vPjii+IefRsJCAggICAAgHPnzlFYWEh4eDgNDQ0UFBRgNpvp06cPSqWSoKCgFhXiaYmYmBh+85vfsG3bNt5++21SU1MZPHhwr+vtWywWiouLSU9P58yZM8DV7bB/8YtfEBYW1m0u0P+TFrc4vr6+lJaWotVqsdlsNDU14e3tTUNDA56enoC4ny8IN+Li4mJP+p988glz587tcg1J8851+/bt49SpUwwaNIiXX34ZLy8v8b1uJ/feey/wf+1mc9Gmjnq/nZ2deeCBB0hOTmbNmjVkZGSQmpqKn59fj/3MmzenuXz5MqdPn+b06dMAJCcn8/jjjxMYGNgtb739Jy1O+EqlkoEDB173u3HjxrVZQILQk6nVap566ik++eQT/vrXv3aZ3eFkWaakpISdO3eSm5tLUlISS5cuxcfHp7ND6/H+Pal2RpKVJInIyEheeukldu3axYcffsi4ceMYPXp0lx6Jaimj0Uhubi5paWkUFBSgVquJi4tj3rx5hISE9PiRjZ7zSQpCN+Hg4MDjjz/O6tWrWbVqFc8880ynJX2bzUZFRQWbNm0iJyeH0aNHM3XqVNGj76U0Gg0TJ06kX79+/Otf/+LEiRM88sgj3ba3L8syRqOR/Px8jhw5wvnz5/Hy8mLIkCGMGzcOX1/fLnHB3VFEwheETqBWq3nsscf44osv+PDDD3nmmWdwcXHpsOPLsszly5fZsGEDly9fZty4ccyaNatDYxC6JoVCQXh4OM8//zwHDhzgf/7nfxg3bhx33313txnm1ul0/PDDDxw9epTs7Gy0Wi1Dhw7lvvvuw9PTs8f35H+KSPhCj1FZWUl1dTWxsbHA1SWk5eXlhIaGdnJkN6ZSqXjwwQf517/+xcqVK3n++ec7pN55cXExn3/+OVVVVUyePJl58+aJRC/8iEql4s477yQxMZF169Zx+PBhFi5ciJ+fX2eHdkNWq5WsrCx2795NcXExQUFBDB06lOnTp/fqJH8tkfCFHuPQoUP4+flRVVWFVqslMzOTEydOsGDBAiRJwmazYTKZOjvM6zg6OvLggw/y9ddf884777BkyZJ2Sb42m43CwkK+/PJLSktLmTlzJklJSb1qOFNoOUmS8Pf3Z+HChWRmZvLrX/+aadOmMX78+E7v7TfvJX/p0iV2797N+fPniY2NZdy4cV2upG1XIRK+0K1VVlZSU1ODo6MjkiQRGBiIwWCwl71sLp7h6OhIdXU1FRUVnR3yj6hUKqZPn87XX3/Ne++9x6JFi/Dw8GiT17ZarWRnZ7Nhwwaqq6t77bIr4dYolUoGDx5MQkICf/3rXzl06BBPPPEEERERHXpvX5ZlmpqaOHPmDAcOHKC4uJjg4GDGjRvHwoULxR4B/4FI+EK35uPjY59JfvLkSQ4fPkxKSgo2m43U1FT27t1rT24+Pj6EhIR0Zrg/SaFQMG3aNL755hs++OADlixZckulVS0WC/n5+axZswaj0cgDDzzAgAEDOr1XJvzY+fPnaWhoYMiQIZhMJo4fP46npyeJiYmdHdqPODs7s2jRIk6ePMn777/PHXfcwb333ouTk1O7HdNqtaLT6bhw4QK7du2iqKiI+Ph47rnnHntPXrg5IuELPcbUqVN/9LsHHnigEyJpHaVSyQMPPICjoyMrVqzg2WefbfGyOKPRyLlz59i2bRuNjY3MnDmTxMREMbTZxVitVntlvQsXLhAYGEhjYyMuLi4MGjSIDRs2EBcXh1KpRKfTtXmlvVuhUChITk4mPj6e1atX89Zbb/HQQw/Z420LZrOZqqoqLl68yPHjxykqKiIiIoKpU6cSFxcnzudWEglfELoQSZKYNGkSkiSxcuVKnnvuuZsqY2symcjMzGTHjh04ODgwceJEbrvtth61hronqauro6GhAUdHRywWCy4uLthsNiRJ4vz588TExNiTp9Vqva7Ublfh5OTEE088QVZWFuvWrSM2Npb77ruv1bejbDYb5eXlnDx5ktOnT9PY2EhYWBjjxo2jb9++HTKhtacTrYEgdDEKhYKJEyfae/rPP/88vr6+N3ysTqfj9OnTbN++HWdnZ1JTU+nbt69I9F2cVqtFq9UC4OXlZS+te/nyZdLS0uzlyZVKJW5ubvYqpl2NQqFgwIABREZGsmnTJpYvX86sWbNISEi4qd6+yWTiypUrnDlzhvT0dJqamkhMTOS+++4jPDwcJyenbrn+v6sSrYIgdEEKhYIJEybg4ODAu+++y/PPP2+vvQ5Xt6g9duwYBw4cwM3NjQcffJC4uDjROHZD11YqdXd3Z8GCBZ0YTeu4u7sza9YsfvjhBz7//HNCQ0OZPn36DTfjMZlMFBcXc+LECS5evIjRaCQmJoYZM2YQFRUlLlbbkXhnBaELGzt2LA4ODixfvpz/+q//ws3Njf3797Nnzx7Cw8OZNWsWkZGRopEUOp0kScTGxvLLX/6S7777jjfffJOHHnqIIUOG2As9ff/995w9exYnJyduu+02ZsyYQXBwcLtO+hP+T6taiR9++AEnJydCQkJoamri3LlzDBgwQCyJEIQ2JkkSI0eOxNnZmaVLl+Ll5UVcXByLFi0iICBALK8TuhwXFxemTp3K4MGD+fTTT/n222+xWCyo1WqGDRvGokWL8Pb2xsHBQYxIdbAWJ/zKykry8vJoaGjA29ub9PR0AgIC2LdvHxMmTMBms2E0Gm/YEBkMBr777juKioraJHihe7hw4QI2m62zw+i2JEli4MCBPP/883h4eBAWFiZmKQtdmiRJhISEsGzZMo4dO0Z0dDR+fn5iWWgna3HC1+l0+Pv7Y7VasVgsmEwmQkND7XsIGwwGysvLb7h/8913301ubq4Yfuxl5s6d+5OTzoSbI0kSAwYM6OwwBKFFNBoNY8aM6ewwhP+vxZlXq9Wye/duHBwcqK2txd3dna+//pqEhATgamGGsLAwLBbLj54bGxtrr3MuCIIgCELHaXHCd3V1Ze7cufafQ0NDGTZsWJsGJQjtxWazodPpsFqtP/p/sizf0j3Fzn6+iOHWnq/T6Vp9zPZmtVppamq64ehod32/2+r5XSWGW9XaGG7Uuf4p7TK2LssyDQ0N1NbWtsfLCz1EfX19hxcU8fX15ejRoz/6YjU0NGAwGG7p1sOZM2e47bbbWv38uro6JEnC3d29Vc/X6/WYTKZbqsOfn59PeHj4LTV+586ds4/4tZQsyxQXF99SCeTq6mpcXFxavDGQLMsMHDiw1cdtT56enhw+fPhHv6+srMRisVy3ZLMlbDYbJSUlt/R+l5SUEBAQ0Op5JWfOnCExMbHV55zVaqWqquqWdvHLy8u7pX0BmvfouJUYysrKWvU5tqTNkuR2aHGrqqrIysr60ax9s9lMcXExERERbX1IO6PRSHV19Q3nELSlzMzMdm8ccnNziYqKatdjFBQUEBQU1K6TaQoKCnBzc7MXGmkmyzIxMTH4+/u327FvVm1tLQaDodUNJ8Dx48cZPHhwq59fU1ODJEmtLrKi0+kwmUy3VKTlhx9+ICYm5pYS/smTJ0lKSmrVc2VZpqCg4JbaiMrKStzc3HrFToBlZWVYLJZWJ+zmXRRv5f0uKioiODi41Qk/IyOD5OTkW0r4FRUVt9TmX7p0iT59+rQ6hpKSEvvmXa1VUlJCUFBQq59/M9ol4f8Uq9VKfn4+0dHR7XYMo9FIbW1tuyeRw4cPM2LEiHY9Rl5eHpGRke16jPz8fEJDQ9t1eVd2djYeHh5dfuJe81ehtV/65tKorX3+rQwrttWQZPPrdGYsrf0c2iL27uZWztlr36/Wvsa1r9NaNpsNhULRqtdpq8+8s87ZtozhZihfe+2119r1CNdQKBR4eHi065IipVKJs7Nzu79xgYGB7b40ysPDo93/Dnd393Zfy+3h4dEhn0lLmc1mtm/fTkFBAZGRkVy4cIHDhw/j6emJq6vrTb1Gbm4uO3fuxNXVFU9PT/bv38/Zs2dvenKqzWZj//79nDx5kqioKBQKBd988w1qtfqGVcpu5Pjx43z//ff2ofitW7fi4OBw08/X6/Vs3ryZ6upqQkNDOXToEMePHycgIOCmC6Js3boVAG9vb/Lz89m5cydqtfqm9gEASE9Pp6ioiJCQEKqrqzl06BD19fU33WMym838/e9/JzY2FrVajV6vvFkD9QAACONJREFU5x//+EeP3E9Ar9ezceNGampqCA0NJSMjg2PHjuHv73/Tn9eZM2fYvXs3QUFBKBQKvv/+e0pKSggLC7up5xsMBrZv305JSQnh4eEYjUa++OILwsPDb6rmvSzLbNmyhby8PKKioqisrOT777/H1dX1pneJLC4utp/rbm5u7N69m7y8PMLCwm6qTdPpdKxevZq+ffvi6OjI7t27OXv2LJGRkTddFnjDhg34+fnh4uJCVlYWR44cISgo6KZHl3Jycjh8+DCxsbFIksTJkyc5e/Zsu43sdshi3vPnz7Np0yb7ZKk9e/Zw4sSJNj1GYWEh27dvp6ysDJvNxp49e8jNzW3TY1RVVbF582by8vJQKpVkZGSwd+/eFk2a+E90Oh27du0iIyMDhUJBfn4+e/fupb6+vs2OYbPZ2LVrl/1ettVqZdeuXW26V3x9fT2bN2/m0qVLKBQKDh06RHp6epu+V7eqqakJV1dXVCoVjY2N5OTkMGDAgBbVicjPz2f48OHk5eUBMGLEiBbtbGY0GrFarQQHB1NSUkJBQQFNTU0Yjcaber7NZqO2tpbExEQKCgooKiqipqYGs9l80zE03/80Go322uY1NTUtmsQWHx+PyWQCrl4E3XHHHeTn59/0868d9dNqtSQmJlJZWXnTz3dwcCAwMNBe7+HEiRMolcobTs7s7qqqqvD29sZoNGI2mykqKiIqKory8vKbfo3S0lKGDh3KuXPnUKvVDBkypEXf/7q6Ory9vbHZbOj1ei5cuNCi97uxsRGlUolarcZgMJCeno5CoWhRvY7CwkKGDRtGQUEBVquV6upqysvLbzoGJycnfHx87JsT1dTU0LdvX4qLi2/q+Q4ODkRHR2MwGABITExErVbf9HcXsF9gybKMTqcjLy/P/nrtod0TvizLFBYWEhUVxZkzZ6iursbDw4MzZ860aTGWkydPMmDAAC5evIhSqcTf37/NJw3m5OQQHh5OTk4OAP369aOurq5Nk1hBQQHh4eHk5uZitVoJCAigqqqqTf+W+vp6jEYjTU1N6HQ6CgsLKSgooKGhoc2OUVBQQGBgIIWFhfZdsLpaT0upVP6/9u7ntYmtDeD4N8lMGmtjGpgkVYONoIZoW2pt0BpdCHbhWvdCl9Kd4MK9K/8CEVyIIAoiuNKCra0rQakUWoixacSalEyjaZofJjPJ3MUlc+W+KBPfNo2357PpajonyWSek+c85xlKpRKVSgW73Y4sy3z79q2ljIfdbmd9fd085sWLFy3VdtjtdqrVKoVCAVmWzc9ieXnZUkFjc8KWy+VwOp3IsozP52NxcdHy90uSJDY3N82ArWka4XC4peuh0WhQq9UwDANZllFVtaUMmGEYVKtVDMOgUCgwNzfHqVOnLB8P/zxy1jAM1tbW+PTp05ZOYjuFLMsUi0Xz83I4HBQKhZYzdaqq4nK50HWdZ8+eMTY2ZvlYh8NBsVikWq1is9n4+PEjKysrZDIZS8dLkkS5XKZSqQB/b+f2+/0sLCxYHoMkSaiqisPhoFqt0tfXh8fjsRwwbTYbmqbRaDQwDANd19nY2LD869xms6HrOrquYxgGCwsLOJ3O/6lV+hXDMNA0zSx0V1WVpaWlbWtU1pY78I83rmZa9/9Z6/zZOX5cB3K5XC3NtKz6cczJZBJFUba0OKj5XjX/yrJMKBTa0mD873N9+PABm83G2traltdXNM8xPj7O3NwcoVDIcqp5u/X09JgP6zAMg2g0yurqKkePHrX8P0ZGRkgkEhw/fpxKpUJvb29Lgc7pdBKJRCiVSrjdbs6fP8/g4CCSJFn6fthsNoaGhshkMmZqcWNjo6WlM5/PRzAYxO12o2kap0+fJp/P09/fb/l1NG9aqqoyPDxMPB5vKWBXKhW6urpQVRWA/v5+M6BZ0Wg06OvrMwPA5cuXicViHV838jsURaG/v599+/ZRrVaJRqOoqmo5HQ9w8uRJUqkUhw8fplar/bR3ys94vV4OHjyIy+WiXq9z5coVc3eEFc1e+na7HU3TGB0dJZlMEo1GLY8hEokQj8cZGBhAlmVzp4DVJQFN0zhw4IA5YT9z5gzFYtFy4W7zaYblcpl8Po8kSXi9XnRdtzz52tzcRFEUstksiqIwMTHR8mS5FW0p2ovH4ywtLTE2Nobb7ebNmzd4PJ6WZ/C/srq6yvz8PENDQyiKwvz8PKVSiYsXL27ZGvXXr195/fo1kUiEQCDA1NQUfr+fc+fObdk5KpUKs7Oz+Hw+QqEQuVyOdDrNyMjIb2/X+rdGo8HLly/p6ekhHA7j8XjIZDLIsrxlxY6FQoGZmRmOHTvG/v37+fz5M6qqEovFdkX1tCAIQqdpa5W+IAiCIAg7QzyBQxB2mUajYa4RdlIRpSD8SvNaNQzjP1mM2Q4i4AvCLvP27VseP35MIpHg7t274uYp/BHu3bvH4uIiU1NTzM7O7vRw/kgi4G+jVCrF06dPKZfLPHr0aEu31gnC7xoeHubVq1fcvn2bq1evous6X758IZvNtr3VsSBYdenSJa5fv04ymeTChQtks1nS6XRHPwOh04iAv418Ph/v3r3j1q1b+P1+3G43hULB3IoiCDshnU5Tq9UIBoN0d3ejaRorKyvcv3+/pf37gtAuhmGQSCRwOBycOHECgOfPn7O8vCwyVC0QAX8bybKMLMtks1nOnj1LvV5nZmbG7EomCO2Wz+d58OABN2/epFarkcvl6O7uxuv1EggEOq4boiDA350B379/z507d5iensYwDEZHRymXy0xPT+/08P4YIuBvE03TePjwIYcOHSIQCJBMJpEkiVgsRrFY3OnhCbtUV1cXk5OTHDlyhBs3brB3717W19dpNBrU63VRxCd0pGAwyLVr1wgGg0xOTmKz2XC73fT29oqUfgs6q/XZf4imaQwODjIwMEA2mzVTpc2uToKwE/bs2WP2W2/2dfj+/Tsul4vx8XFLfdAFod1+bNalKAqA2dUuHA7v1LD+OGIffhvV63WePHlCKpViYmLCvHAFQRAEYbuJgC8IgiAIu8Bf6RuHZCq5Zy0AAAAASUVORK5CYII="
    }
   },
   "cell_type": "markdown",
   "id": "57e95744",
   "metadata": {},
   "source": [
    "![zonotope_picture.png.png](attachment:zonotope_picture.png.png)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "748cfc6a",
   "metadata": {},
   "source": [
    "We can see that the zonotope changes shape as it is passed through the neural network. When passing though a ReLU it gains another term (going from 2 sets of parallel lines to 3). We can then check if the final zonotope crosses any desicion boundaries and say if a point is certified.\n",
    "\n",
    "Let's see how to use this method in ART!"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "785902b1",
   "metadata": {},
   "outputs": [],
   "source": [
    "import torch\n",
    "import torch.optim as optim\n",
    "import numpy as np\n",
    "\n",
    "from torch import nn\n",
    "from sklearn.utils import shuffle\n",
    "\n",
    "from art.estimators.certification import deep_z\n",
    "from art.utils import load_mnist, preprocess, to_categorical\n",
    "\n",
    "device = torch.device(\"cuda:0\" if torch.cuda.is_available() else \"cpu\")\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "5df9e108",
   "metadata": {},
   "outputs": [],
   "source": [
    "# We make an example pytorch classifier\n",
    "\n",
    "class MNISTModel(nn.Module):\n",
    "    def __init__(self):\n",
    "        super(MNISTModel, self).__init__()\n",
    "        self.conv1 = nn.Conv2d(in_channels=1,\n",
    "                               out_channels=32,\n",
    "                               kernel_size=(4, 4),\n",
    "                               stride=(2, 2),\n",
    "                               dilation=(1, 1),\n",
    "                               padding=(0, 0))\n",
    "        self.conv2 = nn.Conv2d(in_channels=32,\n",
    "                               out_channels=32,\n",
    "                               kernel_size=(4, 4),\n",
    "                               stride=(2, 2),\n",
    "                               dilation=(1, 1),\n",
    "                               padding=(0, 0))\n",
    "        self.fc1 = nn.Linear(in_features=800,\n",
    "                             out_features=10)\n",
    "        self.relu = nn.ReLU()\n",
    "\n",
    "    def forward(self, x):\n",
    "        if isinstance(x, np.ndarray):\n",
    "            x = torch.from_numpy(x).float().to(device)\n",
    "        x = self.relu(self.conv1(x))\n",
    "        x = self.relu(self.conv2(x))\n",
    "        x = torch.flatten(x, 1)\n",
    "        x = self.fc1(x)\n",
    "        return x"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "148604f2",
   "metadata": {},
   "outputs": [],
   "source": [
    "model = MNISTModel()\n",
    "opt = optim.Adam(model.parameters(), lr=1e-4)\n",
    "criterion = nn.CrossEntropyLoss()\n",
    "(x_train, y_train), (x_test, y_test), min_, max_ = load_mnist()\n",
    "\n",
    "x_test = np.squeeze(x_test)\n",
    "x_test = np.expand_dims(x_test, axis=1)\n",
    "y_test = np.argmax(y_test, axis=1)\n",
    "\n",
    "x_train = np.squeeze(x_train)\n",
    "x_train = np.expand_dims(x_train, axis=1)\n",
    "y_train = np.argmax(y_train, axis=1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "1e240be5",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "End of epoch 0 loss 0.5815373063087463\n",
      "End of epoch 1 loss 0.2648811340332031\n",
      "End of epoch 2 loss 0.18593080341815948\n",
      "End of epoch 3 loss 0.1360677033662796\n",
      "End of epoch 4 loss 0.10795646160840988\n"
     ]
    }
   ],
   "source": [
    "# train the model normally\n",
    "\n",
    "def standard_train(model, opt, criterion, x, y, bsize=32, epochs=5):\n",
    "    num_of_batches = int(len(x) / bsize)\n",
    "    for epoch in range(epochs):\n",
    "        x, y = shuffle(x, y)\n",
    "        loss_list = []\n",
    "        for bnum in range(num_of_batches):\n",
    "            x_batch = np.copy(x[bnum * bsize:(bnum + 1) * bsize])\n",
    "            y_batch = np.copy(y[bnum * bsize:(bnum + 1) * bsize])\n",
    "\n",
    "            x_batch = torch.from_numpy(x_batch).float().to(device)\n",
    "            y_batch = torch.from_numpy(y_batch).type(torch.LongTensor).to(device)\n",
    "\n",
    "            # zero the parameter gradients\n",
    "            opt.zero_grad()\n",
    "            outputs = model(x_batch)\n",
    "            loss = criterion(outputs, y_batch)\n",
    "            loss_list.append(loss.data)\n",
    "            loss.backward()\n",
    "            opt.step()\n",
    "        print('End of epoch {} loss {}'.format(epoch, np.mean(loss_list)))\n",
    "    return model\n",
    "\n",
    "model = standard_train(model=model,\n",
    "                       opt=opt,\n",
    "                       criterion=criterion,\n",
    "                       x=x_train,\n",
    "                       y=y_train)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "f358bef6",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Test acc:  97.46000000000001\n"
     ]
    }
   ],
   "source": [
    "# lets now get the predicions for the MNIST test set and see how well our model is doing.\n",
    "with torch.no_grad():\n",
    "    test_preds = model(torch.from_numpy(x_test).float().to(device))\n",
    "\n",
    "test_preds = np.argmax(test_preds.cpu().detach().numpy(), axis=1)\n",
    "print('Test acc: ', np.mean(test_preds == y_test) * 100)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "430edde4",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "registered <class 'torch.nn.modules.conv.Conv2d'>\n",
      "registered <class 'torch.nn.modules.activation.ReLU'>\n",
      "registered <class 'torch.nn.modules.conv.Conv2d'>\n",
      "registered <class 'torch.nn.modules.activation.ReLU'>\n",
      "registered <class 'torch.nn.modules.linear.Linear'>\n",
      "Inferred reshape on op num 4\n"
     ]
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "/home/giulio/Documents/Projects/AI2_for_ART/adversarial-robustness-toolbox/art/estimators/certification/deep_z/pytorch.py:90: UserWarning: \n",
      "This estimator does not support networks which have dense layers before convolutional. We currently infer a reshape when a neural network goes from convolutional layers to dense layers. If your use case does not fall into this pattern then consider directly building a certifier network with the custom layers found in art.estimators.certification.deepz.deep_z.py\n",
      "\n",
      "  \"\\nThis estimator does not support networks which have dense layers before convolutional. \"\n"
     ]
    }
   ],
   "source": [
    "# But how robust are these predictions? \n",
    "# We can now examine this neural network's certified robustness. \n",
    "# We pass it into PytorchDeepZ. We will get a print out showing which \n",
    "# neural network layers have been registered. There will also be a \n",
    "# warning to tell us that PytorchDeepZ currently infers a reshape when \n",
    "# a neural network goes from using convolutional to dense layers. \n",
    "# This will cover the majority of use cases, however, if not then the \n",
    "# certification layers in art.estimators.certification.deepz.deep_z.py \n",
    "# can be used to directly build a certified model structure.\n",
    "\n",
    "zonotope_model = deep_z.PytorchDeepZ(model=model, \n",
    "                                     clip_values=(0, 1), \n",
    "                                     loss=nn.CrossEntropyLoss(), \n",
    "                                     input_shape=(1, 28, 28), \n",
    "                                     nb_classes=10)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "f5749a48",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Classified Correct 1/1 and also certified 1/1\n",
      "Classified Correct 2/2 and also certified 2/2\n",
      "Classified Correct 3/3 and also certified 2/3\n",
      "Classified Correct 4/4 and also certified 3/4\n",
      "Classified Correct 5/5 and also certified 4/5\n",
      "Classified Correct 6/6 and also certified 4/6\n",
      "Classified Correct 7/7 and also certified 4/7\n",
      "Classified Correct 8/8 and also certified 4/8\n",
      "Classified Correct 9/9 and also certified 4/9\n",
      "Classified Correct 10/10 and also certified 4/10\n",
      "Classified Correct 11/11 and also certified 5/11\n",
      "Classified Correct 12/12 and also certified 6/12\n",
      "Classified Correct 13/13 and also certified 7/13\n",
      "Classified Correct 14/14 and also certified 8/14\n",
      "Classified Correct 15/15 and also certified 9/15\n",
      "Classified Correct 16/16 and also certified 10/16\n",
      "Classified Correct 17/17 and also certified 11/17\n",
      "Classified Correct 18/18 and also certified 12/18\n",
      "Classified Correct 19/19 and also certified 12/19\n",
      "Classified Correct 20/20 and also certified 13/20\n",
      "Classified Correct 21/21 and also certified 14/21\n",
      "Classified Correct 22/22 and also certified 14/22\n",
      "Classified Correct 23/23 and also certified 15/23\n",
      "Classified Correct 24/24 and also certified 16/24\n",
      "Classified Correct 25/25 and also certified 16/25\n",
      "Classified Correct 26/26 and also certified 17/26\n",
      "Classified Correct 27/27 and also certified 18/27\n",
      "Classified Correct 28/28 and also certified 19/28\n",
      "Classified Correct 29/29 and also certified 20/29\n",
      "Classified Correct 30/30 and also certified 20/30\n",
      "Classified Correct 31/31 and also certified 21/31\n",
      "Classified Correct 32/32 and also certified 21/32\n",
      "Classified Correct 33/33 and also certified 22/33\n",
      "Classified Correct 34/34 and also certified 22/34\n",
      "Classified Correct 35/35 and also certified 23/35\n",
      "Classified Correct 36/36 and also certified 24/36\n",
      "Classified Correct 37/37 and also certified 25/37\n",
      "Classified Correct 38/38 and also certified 25/38\n",
      "Classified Correct 39/39 and also certified 26/39\n",
      "Classified Correct 40/40 and also certified 26/40\n",
      "Classified Correct 41/41 and also certified 26/41\n",
      "Classified Correct 42/42 and also certified 26/42\n",
      "Classified Correct 43/43 and also certified 27/43\n",
      "Classified Correct 44/44 and also certified 27/44\n",
      "Classified Correct 45/45 and also certified 28/45\n",
      "Classified Correct 46/46 and also certified 28/46\n",
      "Classified Correct 47/47 and also certified 28/47\n",
      "Classified Correct 48/48 and also certified 29/48\n",
      "Classified Correct 49/49 and also certified 30/49\n",
      "Classified Correct 50/50 and also certified 31/50\n"
     ]
    }
   ],
   "source": [
    "# Lets now see how robust our model is!\n",
    "# First we need to define what bound we need to check. \n",
    "# Here let's check for L infinity robustness with small bound of 0.05\n",
    "\n",
    "bound = 0.05\n",
    "num_certified = 0\n",
    "num_correct = 0\n",
    "\n",
    "# lets now loop over the data to check its certified robustness:\n",
    "# we need to consider a single sample at a time as due to memory and compute footprints batching is not supported.\n",
    "# In this demo we will look at the first 50 samples of the MNIST test data.\n",
    "original_x = np.copy(x_test)\n",
    "for i, (sample, pred, label) in enumerate(zip(x_test[:50], test_preds[:50], y_test[:50])):\n",
    "    \n",
    "    # we make the matrix representing the allowable perturbations. \n",
    "    # we have 28*28 features and each one can be manipulated independently requiring a different row.\n",
    "    # hence a 784*784 matrix.\n",
    "    eps_bound = np.eye(784) * bound\n",
    "    \n",
    "    # we then need to adjust the raw data with the eps bounds to take into account\n",
    "    # the allowable range of 0 - 1 for pixel data.\n",
    "    # We provide a simple function to do this preprocessing for image data.\n",
    "    # However if your use case is not supported then a custom pre-processor function will need to be written.\n",
    "    sample, eps_bound = zonotope_model.pre_process(cent=sample, \n",
    "                                                   eps=eps_bound)\n",
    "    sample = np.expand_dims(sample, axis=0)\n",
    "\n",
    "    # We pass the data sample and the eps bound to the certifier along with the prediction that was made\n",
    "    # for the datapoint. \n",
    "    # A boolean is returned signifying if it can have its class changed under the given bound.\n",
    "    is_certified = zonotope_model.certify(cent=sample,\n",
    "                                          eps=eps_bound,\n",
    "                                          prediction=pred)\n",
    "    \n",
    "    if pred == label:\n",
    "        num_correct +=1\n",
    "        if is_certified:\n",
    "            num_certified +=1 \n",
    "    \n",
    "    print('Classified Correct {}/{} and also certified {}/{}'.format(num_correct, i+1, num_certified, i+1))\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "b858fc2a",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Test acc:  92.0\n"
     ]
    }
   ],
   "source": [
    "# we can then compare this to the empirical PGD performance\n",
    "\n",
    "from art.estimators.classification import PyTorchClassifier\n",
    "from art.attacks.evasion.projected_gradient_descent.projected_gradient_descent import ProjectedGradientDescent\n",
    "\n",
    "classifier = PyTorchClassifier(\n",
    "    model=model,\n",
    "    clip_values=(0.0, 1.0),\n",
    "    loss=criterion,\n",
    "    optimizer=opt,\n",
    "    input_shape=(1, 28, 28),\n",
    "    nb_classes=10,\n",
    ")\n",
    "\n",
    "attack = ProjectedGradientDescent(classifier, eps=0.05, eps_step=0.01, verbose=False)\n",
    "x_train_adv = attack.generate(x_test[:50].astype('float32'))\n",
    "y_adv_pred = classifier.predict(torch.from_numpy(x_train_adv).float().to(device))\n",
    "y_adv_pred = np.argmax(y_adv_pred, axis=1)\n",
    "print('Test acc: ', np.mean(y_adv_pred == y_test[:50]) * 100)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1f60d178",
   "metadata": {},
   "source": [
    "we can see that the empirical test accuracy is much higher than the certifiable performance. This is because with certifiable techniques we will be providing a lower bound on the performance: there may well be datapoints that the certifier says are unsafe, but in fact cannot have their class changed."
   ]
  }
 ],
 "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.7.11"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}