tutorial_mnist_polytope_repair.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Provable *Polytope* Repair of MNIST DNNs\n",
    "========================================"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "# !pip install -r requirements.txt --index-url https://download.pytorch.org/whl/cu113\n",
    "import warnings; warnings.filterwarnings(\"ignore\")\n",
    "import os, sys; sys.path.insert(0, os.getcwd())\n",
    "import torch\n",
    "\n",
    "device = torch.device('cuda:0') if torch.cuda.is_available() else torch.device('cpu')\n",
    "dtype = torch.float64"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Load a MNIST pytorch model"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "from experiments import mnist\n",
    "model = mnist.model('9x100').to(device,dtype).eval()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Construct repair set from the MNIST-C dataset."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "image_polytopes (1, 7, 784): 1 polytope(s) of 7 vertices.\n",
      "Expected labels: tensor([8, 8, 8, 8, 8, 8, 8])\n",
      "Misclassified as: tensor([5, 5, 5, 5, 5, 8, 8])\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAABa0AAAESCAYAAAD+E/kVAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjkuMCwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy80BEi2AAAACXBIWXMAAA9hAAAPYQGoP6dpAABGbUlEQVR4nO3deYxdZ33/8efO3Nn3GY9ntYfEwXEWIJsViEmcRMGUBhGSFCiRmkBLm0pQUQSVEK1ArVQVgppu6qJWBVS1apxSqBIoKWkIbmIHHLKRhaQO8dgejz2eGc/m2efe8/sjxD+oz+c793597vXx+P2SkMLz9fec55zzbOfxTU4miqIoAAAAAAAAAACQAhVnugIAAAAAAAAAALyBTWsAAAAAAAAAQGqwaQ0AAAAAAAAASA02rQEAAAAAAAAAqcGmNQAAAAAAAAAgNdi0BgAAAAAAAACkBpvWAAAAAAAAAIDUYNMaAAAAAAAAAJAa2UL+UD6fD8PDw6GpqSlkMplS1wkAAAAAAAAAsMZEURRmZmZCb29vqKjQv6cuaNN6eHg4bNiwIbHKAQAAAAAAAADOTYcOHQr9/f0yXtB/HqSpqSmxCgEAAAAAAAAAzl2r7TcXtGnNfxIEAAAAAAAAAJCE1fab+RAjAAAAAAAAACA12LQGAAAAAAAAAKQGm9YAAAAAAAAAgNRg0xoAAAAAAAAAkBpsWgMAAAAAAAAAUoNNawAAAAAAAABAarBpDQAAAAAAAABIDTatAQAAAAAAAACpwaY1AAAAAAAAACA12LQGAAAAAAAAAKRG9kxX4GxVX18fW/6hD31I5rz3ve+VsSiKTrtOhR4vn88nWg/vuTzH/Id/+AeZs2vXLte5cGa87W1vk7Ft27bJ2HXXXSdjVVVVseVJ9y9LLpeTMasemUym6DzreFZscXFRxn7jN35Dxrz9Gf9fU1NTbPnGjRtljhXbsGGDK0/FGhoaZI7VRsvZNjxzmLfvWdQxh4aGZM5nPvMZ17k8HnnkERlbXl52HVPde8/45T2XxRp/reN5zmXlWPfDilVWVsaWW9fl7ZcVFfG/W1lZWZE53jlHxVQdQrCvy8r7lV/5FRlL2t/8zd/Elg8MDMics2Ee9azrve8WVmxubi62/ODBgzLn0KFDrtiBAweKPtfMzIyMoTBWX/7nf/5nGaurq5MxNXYkPdevxnO+pN+p5+fnZWz37t2u2HPPPVd0PXDm3HDDDTL227/927HlVr9U65QQfGufcvYvK887Nz/wwAMytnPnzthyNbdB45fWAAAAAAAAAIDUYNMaAAAAAAAAAJAabFoDAAAAAAAAAFKDTWsAAAAAAAAAQGqwaQ0AAAAAAAAASI3sma5Amr3nPe+RsQ9+8IOx5S0tLTLH+2VtT473S6zevKSperz//e+XOY8//riM5XK5063SOe9Nb3qTjG3btk3Grrnmmtjy9evXu+phfS1Y9bFSfJk4DX3We7yqqioZe/vb3y5je/bsKaxiZ4j1RWur/Q4MDCSWE0IIGzdulLG2trbYcmt+8M4dnjbl/Xq2RdXD+jp50ufyfmXcc3/7+/tljtVGk56nlpaWXHmeay7FmkPFrDaa9D309i8rZrX7lZWVwipW4Lk8c1gp+oq6Zu+5SjFOKVaf7e3tjS33PMcQ/GuOpNfunjmnFGNAbW1tbPnmzZtlzpYtW2TM296UsbExGTt48KCMHThwoOg863iHDh2SsbS//6h3hBDstarVRpNeW5Tz/T1pNTU1MnbDDTe4YqOjo7Hl1jvC7t27ZWz//v0yhsJY89Ttt98uY573Zu/6RsW8/Svp8dxinevmm2+Wseuuuy62fOfOnTLnoYceKrxi5xB+aQ0AAAAAAAAASA02rQEAAAAAAAAAqcGmNQAAAAAAAAAgNdi0BgAAAAAAAACkBpvWAAAAAAAAAIDUYNMaAAAAAAAAAJAa2TNdgXK44oorZOwDH/iAjF1wwQVFnyuXy8lYFEWJxqycTCaTeD08rOPl8/mi81pbW2XO+973Phn75je/KWNrVXt7e2z5tddeK3O2bdsmY1Z/8DxLKydp3nbt7WPlknR/DSGEq6++Wsb27NmT+PmK9Xd/93cytnHjRtcxPffRar9WbGVlpehzWZIez8vZL61zeftX0vOl535Y59qwYYOMDQ4OFn0ubz28c3PS5/Ic07vO8rS3UswdVv2TnlcqKvRvUzzn8vbZpO9vOVnzinqW3vvuvR/quXjH86THAO81e9pNKeYVpaOjQ8bWrVsnY29729tkzDOHWbHDhw/L2Gc+8xkZK5d3vOMdMmaNldZzVv0v6XXFavXwtN+k+4qXda7Ozs7Y8ltvvVXmWLF9+/bJ2OOPPx5bvnv3bpkzMTEhY2uVdX+tvZOk3xO8ax/P8bxt3tMvrTnd0tjYGFv+67/+6zLn+uuvl7H7779fxp5++umC63U24pfWAAAAAAAAAIDUYNMaAAAAAAAAAJAabFoDAAAAAAAAAFKDTWsAAAAAAAAAQGqwaQ0AAAAAAAAASA02rQEAAAAAAAAAqZE90xUoVl9fn4x96EMfii2/5pprZE4URTKWz+cLr1gBxytFTMlkMkXnWOfy1CEE+x56rjmXy8mcX/qlX5KxPXv2yNjIyIiMlUtFhf77o+3bt8vYddddJ2Nbt26NLbfu+/Lysox524Anz9sfPH3Wy9PHrLp7+6zivRdve9vbZKy1tTW2fHJy0nUuj40bN8pY0mOst61Z45RnbLPaRjmv2TsGeNq2NSZ66+E5XtLjV39/v4wNDg4WfS6LNZ5725TK8871njzv2Jb0cy7FfKPqYT0vK2bVUeUlPReFkPx4Y40PSduwYYOMqXG7nGNlCPo5W/NK0kqxvkm6j3n6kbfvJT1PWax6WO23nNT68fLLL5c5Sa9vSvG8yvmcLaUYt5Wk++UFF1xQdOyjH/2ozNm7d6+M7d69W8asvYJyvl8q3d3dMnbzzTfLmPf9QklLX/G2ec9YX87nv2nTJhn7gz/4Axl7/PHHY8t37twpcw4fPlx4xc4wfmkNAAAAAAAAAEgNNq0BAAAAAAAAAKnBpjUAAAAAAAAAIDXYtAYAAAAAAAAApAab1gAAAAAAAACA1GDTGgAAAAAAAACQGtkzduKsPvUdd9whY7fddpuM5fP52PIoimSOFbOoPFWH06lHW1tbbPnCwoLreJ4863iZTEbGrPvhuVfe+3vzzTfL2Fe+8hUZK5evf/3rMlZTU+M6prpXuVxO5lj30MqzeJ6l9zlXVlbGlre0tMgcq/1OT0/L2MrKiowpSY9FpRhvrOe8devW2PKHH35Y5iQt6XYYgm/usO69p495n5e3jipmzc319fUypvpeCCEsLi7Gli8tLckcb9tWrH6eNKt+fX19ZauHNUZVVOjfLFgx1bat+2v1B09/LkVfUfUvxRhr3SuVZz0Ti3Uu1WfLec3WuSzePI/+/v6i62HVz3omnrZhxbz3yftulLRyjvUqz/uOY/VZz7Ms5xxWCldffXVsuTVPWesKz3PxPkuLd6xPMqcUPOOU915YfcVzriuvvFLGrrjiChn72Mc+JmMf+chHZKxc3ve+98mY991I5XmeyWr1UH2sFOsbT8x7PIsnz/uOfs0118SWb9u2Teb8+7//u4zt3LnTVY9S4ZfWAAAAAAAAAIDUYNMaAAAAAAAAAJAabFoDAAAAAAAAAFKDTWsAAAAAAAAAQGqwaQ0AAAAAAAAASI1sqU/w7ne/O7b8jjvukDnt7e0yZn1l2PMVb4vn653Wubq7u2Wsp6dHxtSXR62vrc7OzsrY//7v/8qYur/WvbCu2fsVepXn/XK99SXhH/zgB7HlL730ksxJWk1NjYwlfe89X/ZdrR6emFWP1tZWGVu/fr2MdXZ2xpYvLS3JHKvui4uLMrZ///7Y8pmZGZmT9Jfmk+5fIdjPRfWjhx9+WOYkzTueWzxtNOlxz9u/LG1tbTK2YcOG2PLGxkaZY90Pq6+o+WhsbEzmHD9+XMaS5u0rnuP19fUVfTwvbxtN+mvn3nFKtTerft7rUueqrKyUOZdffrmM1dXVueoxPz8fWz4+Pi5zDh06JGOe5+Kdpyyecc9zvFLo7++XMXWvStFGk14zWzx5Vt2rqqpkrKurS8bWrVsXW26t6aw12PT0tIzNzc3FllvzntUfSvHumYbjeW3dujW23Lq/Fuveq7boXfta9zDp+dK6Lk9MrfVCsPuDtQbz7Et47pN1TO/xLLW1tYkf0+PSSy+NLb/qqqtcx/OMRd5+6Rlvku5fq+V52lR1dbWMWfORp6+UYg2m3HbbbTJ2/fXXy9h9990XW/69733vdKsk8UtrAAAAAAAAAEBqsGkNAAAAAAAAAEgNNq0BAAAAAAAAAKnBpjUAAAAAAAAAIDXYtAYAAAAAAAAApAab1gAAAAAAAACA1MiW+gSf/OQnY8vz+bzMyeVyMmblRVFUVPlqMetcVVVVseXnn3++zGlvb3fVY25uLrZ8eXlZ5jQ2NsqYVcfh4eHY8snJSZnjvb/lZNXjPe95T2z5Sy+9VKrqnMJqa0nHvH3P21dUXiaTkTm9vb0y1tLSUnQ9FhYWZI51zXV1dTKm6njw4EGZMzs766qHJ6cU497GjRtjy/v7+2XO0NCQjHl4xxTPNZeir6iYdS5LTU2NjLW2tsqYatvWdVn9yKp/U1NTbHllZaXMmZiYkLGVlRUZU+OKNd54+4rnWfb09MhY0jzjcgj2vUq6Ht5YkjkhhJDNxi+HzzvvPJlj9T3vGKuOuWHDBplTX18vY9Y6xvOcrbon3W689Uia1WfVeFlRoX8T5B2LrLHZs36weOZZqz90d3fL2Pr164s+ZkNDg8xpbm6Wsba2NhlT7z/WXFSK9x/VPkqx9kmaNU696U1vii33jimee+8dl7318KxHrHWR1X67urpiy63+0NfXJ2PWHoPqK2NjYzJnaWlJxjzP0hpjvfNDOecwy3vf+97Y8lJcl+eYSY8p1rP05qk1XQghVFdXx5Z3dHTIHO8e3uHDh2PLp6enZY53vFH3w7sescabu+++O7b8e9/7nsw5XfzSGgAAAAAAAACQGmxaAwAAAAAAAABSg01rAAAAAAAAAEBqsGkNAAAAAAAAAEgNNq0BAAAAAAAAAKnBpjUAAAAAAAAAIDWypT5BPp8vqrwUMSsniiLXuVReXV2dzFlZWZGxkZERGRsbGyuqDqvV44ILLpCxiYmJ2PLp6WmZs7i4KGNemUym6BzrflixjRs3xpZfe+21Muexxx4rvGIFsOrnzcvlcrHl5ewPVqylpUXmZLN6aLLa2/DwcGy5atch2G2tqalJxjZt2hRbrvprCHY/su6vh7c/eI55xRVXyJyhoSHXuRRrHLV47kcp5inPuaw2WlNTI2Otra0ypu7jwYMHZc7U1JSMVVVVyVhbW1tseV9fX9E5IYRw7NgxGVP317qH3rFNsdpoc3OzjDU0NMjY7Oxs0fXwXpd1r1Sed+5Q85RVj1KMbered3Z2yhzrug4cOCBjk5OTMlZfXx9b3tPTI3Pa29tlrLKyUsaWl5dlzHM875ioePusR2Njo4x5xlFrDWMpRT/ynMtSURH/eyerr3R1dcmYda/Uu9HCwoLMscZR61n29/fHls/Nzckcqx7l5H2WSbvqqqtkTLVf1Z5CsOdSz/jgnTs876RWnnXN1li/bt06GVPv/fPz8zLHGs9ra2tlrLu7O7bcuodHjx6VMY9SrG/K6frrr5exgYGB2HLPO3+5WfdXxTzrwBDs9mv1I7X/YL3zW+84Vn9W67PDhw/LHOu9OennbN3DtMwrb+CX1gAAAAAAAACA1GDTGgAAAAAAAACQGmxaAwAAAAAAAABSg01rAAAAAAAAAEBqsGkNAAAAAAAAAEgNNq0BAAAAAAAAAKmRLfUJcrlcbHk+ny86J4QQoigqOmady3O8EEJobGyUMWV5eVnGRkZGZGxqaiq23KpfbW2tjDU3N8tYW1tbbPn4+LjMmZ2dlbGKCv33IplMRsY8zzLp2I4dO2TOk08+KWMLCwsyVmwdVpN0f/D2FavPqjZgPf+6ujoZs9rbkSNHYssXFxdljmVpaUnG1q1bF1teX18vc6qqqmRsbm6u8Ir9jHUPLd5xT8Uuv/xymfPAAw8UXrECWG3NknRfWVlZSbQe1rms59ze3i5j2aye4icnJ2PLh4aGZI63jqofrV+/XuZUVlbKmPUsvWOp53iqHt769fb2yti+fftkTLHaqPW8rHnbc7ykn5f3GVvXtWXLlqLPNTY2JmMHDhwovGI/Z3p6OrbcmovUui2EEDo6OmRMzZcW7/rBw/su4NHX1+eqh2r33vmhFGtcxTsGtLS0xJZv3LhR5ljPy3r/ee2112RMsdaP1nNR46+V42kbq8XOZldeeaWMqTaadF+2zmUpxTOpqamJLe/u7pY51lhkXZd6Tx8eHnYdz5pXenp6YsutNZ3aywjBfv9RfawUzyvptmjtxdx8882J1iPp9zrv+JX0+rGpqUnGVDtcLaZYewXWPpj1rtXZ2Rlbbq3NrH0ka770vJOU4p26VPilNQAAAAAAAAAgNdi0BgAAAAAAAACkBpvWAAAAAAAAAIDUYNMaAAAAAAAAAJAabFoDAAAAAAAAAFKDTWsAAAAAAAAAQGpkz9SJoyiSsXw+n2jMOlcul5Mxy+LiYmx5RYX+e4D5+XkZW15eljHPdan6hRDC3NycjPX09MSWW9dlPROrjpZMJlN0jlUPj/r6ehnbsWOHjD3wwANFn8tqh0n3laT7lzfW2trqOt7ExISMqX5k3UPv+DA7OxtbXlNTI3NWVlZcMdX/rH5p8fZZldfe3i5zLrzwQhl75ZVXZKzYOqzGMxZZzz/pe2jlWG2qubnZVY+DBw/Gllvt0BqXrfuh7qM1F2Wzenli1UPV38rxzDcW75jd29srY/v27Su6Ht71TWVlZaLn8saS1t3dLWPqmq3n9fzzz8uYNTZb7U21nYWFBZljrR+tmKeveMc9FbPO5V0XeVh9z7pmVX/vPFWK9bRHdXW1jHV0dMSWW/Wz1m0vvfSSjKn76203k5OTMtbZ2Rlb3tTUJHOsfmndD2uM9azdyzm/XXTRRTKm2kYI+n6Uoq8o1r3wrqctan1mrZmtMfvo0aMyNjQ0FFvuXdNZeer9WPWhEOw9EG/bTjInhOTH2JtvvlnGrD0GVQ/vu2zSc3PSMWu9b63brPFmaWlJxoaHh2PLp6enZY71vmK9o6m9gv7+fpnT1tYmY0nvgVisvKTnlULwS2sAAAAAAAAAQGqwaQ0AAAAAAAAASA02rQEAAAAAAAAAqcGmNQAAAAAAAAAgNdi0BgAAAAAAAACkhv5cZ0KS/hKrdTz1xWgrx/ulbvVlbevrw9bxpqamZEwd0/pCtvcLyerLo+oLyCGEMDY2JmPW/fV8qbkUX0BVdbRytm3bJmMPPPBA4RX7GetZer8IrI5pfRG6FH1FfRXY236teqivBXuPZ12X+vKz9RVk66vgnjbg/eJ20s/Zyrnssstk7JVXXpExxdtuLJ7rsurh+aq9p62tVg/ra+1Jz5fWva+trZUxxRqnFhcXZUxdlzXfeL+EnvQX3q2vpHtYbcPimWetc3nrkTSrHao6jo6Oypyk5+YQdHurq6tzHc/qs6qPedePnnnWew89Y6ylt7fXdS7PnONdc1gxVQ/vnNjQ0CBjjY2NseUnTpyQOUePHpWxpO+vtQazYrOzs7HlCwsLMse7Hinnu3HS57rqqqsSPVc5xwBvf6isrJSxqqoqGevr64stt9Z0x44dk7HDhw/LmFoXedc31hpMtXtrDFD7JiHovheCrqNnD2E1SfeV7du3y1g510WePmblWPfe6pdqXunv75c57e3tMma9C1hrtwMHDsSWW9dlxay+UlNTE1tuzSsW65pVX/GsHVaLJd1XCsEvrQEAAAAAAAAAqcGmNQAAAAAAAAAgNdi0BgAAAAAAAACkBpvWAAAAAAAAAIDUYNMaAAAAAAAAAJAabFoDAAAAAAAAAFIjW+oT5HK52PJ8Pi9zko5FUeQ6npU3NzcXW76ysiJzKir03xG0tbXJ2PHjx2PLrfpVV1fLWEdHh4ypOqrnGEIItbW1MjY/Py9jVv09vMdTedaztNqNh3V/k75PFm/fs+qoYsvLyzLHuvfWuTKZTGy5dX+tftnZ2Sljqo/NzMwUnRNCCAsLCzKm7r1Vd88z8casnMsuu0zGdu7cKWOK9SzV81+Nur/eMcDTZ7393KrH4uKijKn7aN1fS0NDg4yp+c1qv9Z1LS0tFV6xAnjbjac/WNfV3d3tqofnXNY1e+Yj65q9fdbzXKyc1tZWGVP1Hx0dLTonBHvssNTX18eW9/X1yRzr/o6NjcmYqmM2q18NvHOpR9JjrKWnp8d1Ls9asBTXpdq99Uys9Yj1TqLyRkZGZM7k5KSMee6h1UYbGxtlrLm5WcbUe501j3rf+bxzjkfS7ytXXnmljCW9fvTGkj5eXV2djFljh8qbnp6WOcPDwzI2OzsrY542ZbXRmpoaGWtqaootHx8flznWus3zXpf0uGydqxTK2baTzrPur/UusH79+tjyrq4umWONsYODgzI2NTUlY+qavXOzNR+p+lt7Z0NDQzJmUfUvRbsuZ195A7+0BgAAAAAAAACkBpvWAAAAAAAAAIDUYNMaAAAAAAAAAJAabFoDAAAAAAAAAFKDTWsAAAAAAAAAQGqwaQ0AAAAAAAAASI1sqU+Qy+Viy6Mokjn5fL7o41l53nN58iYnJ2VOQ0ODjFVWVspYsXVY7Xjz8/MyVldXF1ve0dHhOtdPf/pTGauo0H9nou699UysmNVuVMzbNjysc2UyGVc91DGte7GysiJjXouLi7Hl3udl1VG1KSsnm9XDYE1NjYx52qjVVzxtysrxthuLZ4y17q+H9Syta7ao+nvmm9V46mjd36qqKhlbWFiQMTUPWOeyxuzW1lYZa2triy1fXl6WOdPT0zLmab/eMdZzTO/c0d3d7aqHUoo26plXvOONqoc1jqo1zGoxNU9NTEzIHO/a0loLXnbZZbHl1jh64sQJV0yxnmXSc5i3r1h19Ojt7XXVQ7GuqxRrS9VXrOM1NjbKWHNzs4ypY46Pj8scay6y7kd1dXVsuTVWrlu3TsasMWBwcDC2POm5KITk1wHemIc1BnjadtLrUYt3zWyNv2p9E4Ku47Fjx2TOzMyMjHnqb73HWGNAT0+PjClWX7HmoqTnFetZluLdqFy89fOMD96+YvVLNa9YOUeOHJExa87x7GdY12W9a1lrOjVXWf3c6iuetY9nj3E13veL08EvrQEAAAAAAAAAqcGmNQAAAAAAAAAgNdi0BgAAAAAAAACkBpvWAAAAAAAAAIDUYNMaAAAAAAAAAJAabFoDAAAAAAAAAFIjW+oT5PP5ospXk8lkZCyKotjylZWVonNWMzk5GVve09MjcyorK2WstrZWxioq4v9uwbou61zV1dUytri4GFtu1a+7u1vGrLyxsTEZGxkZiS232o03ptqAJ8crl8vJmKfNh6Dbh3WupK8rBF3/hYUFVz1qampkzDPeZLN6GKyvry/6XA0NDTJn48aNMjY/Py9jql9avM/S0+6tNuUd6z3H8/YVzxiQ9HVZ7dC6Lmusr6qqkjH1zLx9pb29XcbU/VVzm5WzGpWX9PG8x7TurzU3e3iv2erPine+9PRZ61wtLS0y5uEd26zYwMCAjKn7YR1v//79MmZJeu2TdH8u51rFWqt6xgDvuJF0zOpf1juENXcopVifq/eL3t5emWONo9PT0zI2OjoaW760tCRzrPnXYvUVD6ttJL1WSbqNlnNu9s5F1hq8nH3FGhPVGqyvr0/mNDY2yph1P44cORJbPj4+LnO87dAztpVznrJYdUx67VOK93fPuaz3BM87pLce1r1S7d5aP1r7AW1tbTLW1NQUW37gwAGZMzU1JWPWvVJtO+k5wDpXKfFLawAAAAAAAABAarBpDQAAAAAAAABIDTatAQAAAAAAAACpwaY1AAAAAAAAACA12LQGAAAAAAAAAKSG/sRnQjxfrPR+DVTFvF86tqivvk5OTsoc9WXfEELo6uqSsePHj8eWW1/utL5kan2xdmFhIbZ8eHhY5lhfVN2wYYOM1dXVydj8/Hxs+cTEhMxJ+mvM5fxKr/UVd+8Xkj39oRRfmFVfV7e+xu1t2x0dHbHlVruxvqxtfYV+dnY2tty6h7W1tTK2adMmGTt69GhsufdL3d42oPqK1X6T7iulaKPqmNZXmq16WH1WsfqDdTxve+vt7Y0tt8Z6q41aX6FX84rVv8477zwZm5mZkTE1d1iSXiN4+145+4qnjVrH9F5X0vOs9dV1a5xSc875558vc1599VUZ27Jli4xZc5gac6zn5V0jlLO9Jd1uyll3Tz1K0R8sKs9qG2oNs1pMrd2t9xhrftu4caOMtbS0xJardWUI9rx96NAhGfPMHaVYj6hnlvS7cSkk3S+TVor6TU9Py5hqv9YcYLVD9Y4TQgjNzc2x5da7tvWuNTo6KmOqH3nf6zySfjdeLS9pnvpb97Cc12XV3Rp/l5aWYsutNtrU1CRj69atkzFrb0q9r1jvMdms3jK11pYHDhyILVfv9SHY/cia+xTr+XvXluWcV97AL60BAAAAAAAAAKnBpjUAAAAAAAAAIDXYtAYAAAAAAAAApAab1gAAAAAAAACA1GDTGgAAAAAAAACQGmxaAwAAAAAAAABSI1vqE+RyudjyTCYjc/L5fNHHs/Ks41miKJIxVf+5uTmZMz8/L2O1tbUytnnz5tjyxcVFmdPS0iJj1v2YmJiILR8bG5M5VVVVrlhnZ6eMdXV1xZYfO3ZM5ljPyxsrl1K0UXVMqw9ZMa+VlZXYcqv9Tk1NyVhjY6OM9ff3x5b39PTInIaGBhlbWlqSMdUWrb5itfkNGzbIWEVF/N8vWueynqW3P6g25cnxssbYuro6Vz1U/T05q8U89/D48eOuWHNzs4ytX78+tlyNvSHY47mnr1RWVsqc9vZ2Gdu4caOMHT58OLb8xIkTMsfieZZWu/HGPKx1VtLzZSnGAE+eNSZaMdXerHb4jne8o/CK/RxPX7fmji1btsjY0aNHZUy1D++ayPO8vO0m6XVb0mN9KdaVSa9jl5eXZWx8fFzGuru7Y8vb2tpkTkdHh4xZdVfrmIWFBZljzStWLOlnVs62bR3Pevf0sOYVz/0txbubqqNVdytmva9Y91e9r1hrs9bWVhnzrB+sHGtdNDw8LGOeNmXdX49SzFNJjwHea/bMzd62rY7pPZ5F7QdYrHf0Cy64QMas5+wZH6y+Mjo6KmMHDhyILVfv9SH45ynPGsy6ZquOZ2LvjF9aAwAAAAAAAABSg01rAAAAAAAAAEBqsGkNAAAAAAAAAEgNNq0BAAAAAAAAAKnBpjUAAAAAAAAAIDXYtAYAAAAAAAAApEa21CfI5XKx5VEUuY6Xz+cTzbHq4anjzMyMjA0NDclYX1+fjFVXV8eWV1VVyRx130MI4cSJEzJ29OjR2PLl5WWZY93f4eFhGWttbZWx2tra2PKWlhaZc/z4cRlL+jl726+ysLAgY+r5r0Y9l1L0B09sYmJC5mQyGRnr7++Xsbq6uthyb1+x6njs2LHY8vn5eZljXdf69etlTF1Xc3OzzBkbG5Mx63lZ7WNlZaXonKT7yuHDh2Vs06ZNrmMmPQZ47q+VMz09LWPWvNLT0yNjTU1NseUVFfrvstXzDyGEkZERGTty5EjR56qsrJQxa+5Qc7B1Dz3rCivPGlOsWNK8/dyT572Hnn5k5VjtZnBwUMZqampiy9XYG4L9LK37YfXZQ4cOxZZb67aBgQFXzKpHuXj7Q9LzSlpYawSLNZYqS0tLMjY1NSVjah3e0NAgc6y5Y25uTsbUOsa6Xmvea2trkzE1T1nPpBTvsp5xz2KtmZLmbb9Jn8tzr7zH86z5reNZfcXql6ofdXV1yRxrvrTGZlV/7z1Mel3kXZ8vLi6WrR6ee1WKdy1PG7W8+c1vljG1t2Ody1r7WPfQmt8Ua34YHR2VMev9RynnfovFalPlfLcvBL+0BgAAAAAAAACkBpvWAAAAAAAAAIDUYNMaAAAAAAAAAJAabFoDAAAAAAAAAFKDTWsAAAAAAAAAQGqwaQ0AAAAAAAAASI1sqU+Qy+Viy6Moch0vn88nei7reBZ1ruXlZZkzPz8vY3NzczLW0tISW97c3CxzGhoaZKyyslLGVlZWZExR9yKEEBYXF2VsdHRUxtQ1W/fQ+yxVXinajbJ3714Zu+aaa2TMU0crpxQxVY+FhQWZc/ToURmz8np7e2PLW1tbZU42q4dBq41abVGxxofx8XEZW7duXWx5fX29zLH6ZSmec7kMDw/L2Pnnny9jnusq533y3tvjx4+7jqn6ihp7QwhhbGxMxg4cOCBjS0tLseXV1dUy58SJEzLW0dEhY6pPeNYOq1HHtI5n1SPp/nW2jwEVFfG/q/DWYWpqSsbUuGKNKZannnpKxmZnZ2VMXbM1PwwMDMiYmjtC0H3Wur+ZTEbGPO0m6XVbKahnEoJv7rB4r0udz/u8ampqZEzdD+v9YWhoSMasdZY6Zl1dncyx3o2qqqpkTK0Tp6enZY4l6THWezxrzZR2Vvv15HmP19XVJWP9/f0yptb81lxkraUs1vuFYtXdsx/gvb8WVY+k56IQQnjyyScLr9hp8qwTyznvWWOl1W6s8VftCVnvFoODgzLm1d7eHlve1NQkc6w50bMfUIr2m/S7ZznfVwrBL60BAAAAAAAAAKnBpjUAAAAAAAAAIDXYtAYAAAAAAAAApAab1gAAAAAAAACA1GDTGgAAAAAAAACQGmxaAwAAAAAAAABSI1vqE/zXf/1XbPm73vUumRNFUaKxpI9nxfL5vMyxYqOjozI2MTERW97Z2SlzBgYGZGxhYUHGMplMbLn3PlnXXFdXV3Seqt9qrDp6jmkdz+PJJ5+UsXe84x2uY3quy8qxnmU5++XU1JSMVVZWxpY3NDTInOXlZRnL5XIy5mmjS0tLMjYzMyNjXV1dseUrKysyx/u8PHneZ+lx+PBh17mSvi6L1QbUMSsqfH+HbLWBubk5Gctm46d/63izs7MyZrVtxVt367mo+2j1cy9Vf2vcsCTdV7w89fC0eW9e0vN5CCFs3Lix6Jxjx47JmNVXvHVUrPuh5kSrHla/9NZDjb9WX/H083JL+ll6j6eeszXvWaz3i5qamtjykZERmWPFFhcXC6/Yz1RVVcmY1earq6tlzPNeVwrqfN511vDw8GnX6ed5x3pPjncd6+lHVptSa/DVzjU0NBRbfvz4cZljrX0sqm1b99Dqey0tLTI2Pz9feMV+xvucPcfzevrppxM/pmLVX82L1n3yzh2q3bS3t8ucDRs2yJh1XS+//HJsudXmrfWIdc3WPKDeB6zjWXW01iPqfnifl3dM9LCO98gjjyR6rkKkY9UHAAAAAAAAAEBg0xoAAAAAAAAAkCJsWgMAAAAAAAAAUoNNawAAAAAAAABAarBpDQAAAAAAAABIjWypT/Dggw/Gll999dUyp6GhQcbK+dXMcn4x2jqX+srpwsKCzLG+mlpfX1/0ubxfrLW+Pmx9xXt6ejq2fGlpyVUPi2o3SX+Z2vKTn/xExsbGxmSso6NDxjzXVYo2r+5V0s8rBP0lbPW1+xB0mw8hhGPHjsmYqr9VP6vNW31F1XFqakrmeMdKT6yc4/Lw8LCMWfXw1LEUXyf3tBtvPazxUs0D1pe6X3vtNRmz+rOKqS+kh+BvU2oMsFj1sCT9xftStDfF+9V1xVt3zz206mcdz/rCe1VVVWy51TZeeOEF17ks6j56+4rVH6w1pGK1G6sNqPp71xzWOOXhXY948rx9Jek1aW1trYw1NjbKmHpmL7/8ctF1CMHXV6zrtdZ7VntT/cE7P1iSngesnCNHjhR9PO+5LOree8c2DzXOhxBCZ2enjFnvzdYYOzg4GFtutV/v3JHNxm/pWO8WFmv9qJ5L0u/GIfjW51ZsfHxcxrxjmGLNU1bbVn3Ce83Wc6mrq4stt/qD1WdHR0dlbGJiIrbc8/6wGut9W+2dePe6LOV850u6/83MzMjYt7/97UTPVQh+aQ0AAAAAAAAASA02rQEAAAAAAAAAqcGmNQAAAAAAAAAgNdi0BgAAAAAAAACkBpvWAAAAAAAAAIDUYNMaAAAAAAAAAJAa2VKfYH5+Prb8wQcflDkf+tCHZCyTyZx2nQplnSuKoqJzLOp4luPHj8vY5OSkjLW2tsrYwMBAbPm+fftkTjarm1FjY6OM5XI5GRsbG4stz+fzMse6h56Y91xJ+9GPfiRjO3bskDFV/1LU3dPuvfWw8mZnZ2PL1TgUQgh1dXUytm7dOhlTbdS6F+3t7TJm9RV1LnW9q9XD4nkuVo7Vzz2Gh4dd9fDw3kMrzxpXlIoK/ffL3nFqeXk5ttwaz62+YvUxxeoPPT09MqbqHkIIhw4dii1fWVmROUnPHeWcHyxWPaw2Ws51ltW21djhrZ/Vfj3PzLNGXC2mjllfX+863vT0tIx5xiKL1cfUubz3MGnlbPPWffeO5yrPGs+t8deqx4kTJ2LLveONda7KysrY8traWpljjSkzMzMyZvUVxdturGv2rJmsaz569GjRxysFz7uWdS88Y0dDQ4PMaWlpcdVjZGRExhRPXw7B7s+qT1jXvLCwIGMTExMy5pmbk+4r3vnhmWeeceV5JN3PS9FuVMxqN9a5Dh48KGOevTPrmquqqmTMqr96t7feLcbHx2XMepZqbC7F2ifpNd13vvMdGbPGjlLhl9YAAAAAAAAAgNRg0xoAAAAAAAAAkBpsWgMAAAAAAAAAUoNNawAAAAAAAABAarBpDQAAAAAAAABIDTatAQAAAAAAAACpkT1TJ/7+978vY1dffbWMDQwMyFg+n48tj6JI5lgxSyaTceUleTwrZ2RkRMZaW1tlrLu7O7Z8bGxM5lRWVspYS0uLjM3Pz8vY9PR0bPny8rLMUc9/NZ524z2Xx1NPPSVjN910k4yp+nvbvMVqiyrmrYeVp9ri1NSUzKmtrZWxjo4OGTt+/HjRx2tra5Mxq22Pjo4WnVMKnjaVdF+ZnZ2VscnJSRmzxr2KiuL//tbbftW5SjGmVFdXy9jCwkJseX19vcypq6uTMWs8V3mdnZ0yx+pHBw8elDHVPrzrAE/bLsW5PKx27a2Hp69YbduKqXp4j9fY2Fh0nvdc1pxo3cOLL744ttyai1RfDiGEF198UcaSHnOsdqPuh+f5h2CvOz28/cFzXVYsl8vJmEXV0WprNTU1rnpYc7Bi3cOGhgYZ6+rqii23+vLc3JyMWe9G5ewPnnZvjSlqPRqCfT88vG1U5VnH8z4TdQ+tc1lrDivPuvee+dJ6T7DWZ+p921qbHTlyRMasfq6uy2qjSb/zedc3zzzzjKseHt75Len395WVFRlTbXtxcdF1LqsfKdms3o60+oN1P6z3C9Unjh49KnPUvtRq9fDw9iNPPaz3qf/5n/8p+nilxC+tAQAAAAAAAACpwaY1AAAAAAAAACA12LQGAAAAAAAAAKQGm9YAAAAAAAAAgNRg0xoAAAAAAAAAkBpsWgMAAAAAAAAAUiN7pisQ51vf+paMffzjH5exKIqKKj8dmUymqPJS1COXy8nYwsKCjI2NjclYS0tLbPmmTZtkTlVVlYwtLS3J2NGjR2Vsfn4+tjyfz8sc6/5aecr09LSM7dq1q+jjeQ0NDcnY4OCgjA0MDMSWW23UUlGR7N9xWc/E+5xVn5idnXWdq6OjQ8ZU+2hra5M5zc3NMnbw4EEZm5ycjC23xgCLt6+omHW8Uoy/yvDwsIy1trYWfTxvX/Fcs/ceevuKmiPq6upkTlNTk4wtLy/LWGdnZ9HnGh8flzFrDlN9opzP0ju2lZN3PE/6flhjWNLnWllZKboeVh1qampkzGpv5513noypNdiJEydkznPPPSdjnrHDqrv1vDzrX2+/TLofWffJW0elFGsfFbPavGctZeVZ84M11qv5IYQQGhoaYssXFxdlzoEDB2Ts8OHDMpb0WsX7LD2OHDmS6PG8PG3b6l/esUix+oP1npDN6u2Snp4eGauvr48tt/qKFbPet5XXXntNxo4fPy5jSb9Te9e4nrnDem+23hOSdv/998vYTTfdJGONjY2x5aV4n5qZmYktt/qXNZ5feOGFMqb2dqz1qNX3rJi1D6b2n6y5w7ofVv09z8y7l+hZqzz00ENF55wp/NIaAAAAAAAAAJAabFoDAAAAAAAAAFKDTWsAAAAAAAAAQGqwaQ0AAAAAAAAASA02rQEAAAAAAAAAqcGmNQAAAAAAAAAgNbJnugJxXnzxRRl78sknZezyyy9PtB4VFcXv6WcyGde5crmcjOXz+djyKIpkzvT0tKseVVVVseXWvbDqMTQ0JGNHjhyRMXXNqvx0PP7447Hl3//+92VOKerh8fTTT8vYwMBAbLmnXZ8Oq314cqzY0tJSbPnU1JTMmZiYkLHGxkYZU/fX6stWm7dii4uLseVWO/TeQyvm6Zeq7qVg3cNLLrkk0XNZY33S99BzvBBCWFhYkDHVJ6w239PTI2O9vb0ytry8HFs+Pj4uc6xneeLECRnzzJcWz3OxcqyYd/2QtHLOb9ZzUWOpd/yy1kWqr6g1UQghXHHFFTLmnWfHxsZiywcHB2WO1c8tqo7eNmrNfR7WsyznOsbTH7zjedLHtOZfa+3T3NwsY21tbbHl7e3tMscyNzcnY6Ojo0WVh2Cv95J+Lt5n6RnDrL43MjLiqoeHNd5Y46VnvvTeX8Wqu7UesfqDtWZqaGiILbeuy1rfzM/Py5haM83Ozsoc71ivYt5nmfTa59lnn030eF7WnpX1/n7jjTfGll933XUyJ+l10Q9+8AOZo95/Q7D7imof1nyu3utDsOcwa+6z+oRi1dHTj7x9xaqHiln94Sc/+YmMpQ2/tAYAAAAAAAAApAab1gAAAAAAAACA1GDTGgAAAAAAAACQGmxaAwAAAAAAAABSg01rAAAAAAAAAEBqZM90BYr1n//5nzJ2+eWXx5Z7voC7WszD+6VQFbNyvF9bVV9UrampkTnWl449X2gNwfeV6RdffFHGdu3aJWPWF6PT7qmnnpKxW2+9Nbbc+wVnb39I+ovhVp6Kqa8jhxDC4OCgjLW1tcmY+mL4sWPHZI71hffl5WUZ83xB3bpPXvv27Ystf+GFF2TOSy+9lHg9FPX19BCSH8+T/qq9dbxcLufKW1hYkDHVFq3j9fX1yZj1pe6xsbGi6hCCPXdY98PDO94kPbYlzfu1c++Xyz3H84znnvVSCPZa5eWXX44tv/jii2WOdS9mZmZkbGhoSMbUesSaH7zUmOi9v97n7JH243nvk8Uzh1nXZa19s1n9etjS0lJ0jvXeYfWV+fn52HLrHce6Zuseet61vO0m6bW2NZcm7XOf+5yMXXbZZTL21re+Nbb8wgsvlDnetY+ysrIiY/v375ex4eFhGevo6JAxNUdYazPrmq11lsorxXhezvWviln95Mc//vFp16nUrOf88MMPx5Y/88wzMufGG2+UsUsuuaTwiv2MVT/rvbmqqkrGrDlCSXr9aMU884M35p0DrOuqrKyMLf/ud78rc84m/NIaAAAAAAAAAJAabFoDAAAAAAAAAFKDTWsAAAAAAAAAQGqwaQ0AAAAAAAAASA02rQEAAAAAAAAAqcGmNQAAAAAAAAAgNbJnugLFGhkZkbHvfve7seU7duyQOZlMxlUPT573XFEUxZbn8/mic0IIYXl5uejYzMyMzMnlcq56WLHDhw/Hlu/atUvmvPrqqzK2Vk1PT8vYiy++GFt+6aWXJl4P61l6WG3b0+6tNj8xMSFjk5OTMra0tCRjHt6+oqg+FIJuGyGE8MILL8jYiRMniq5HOQ0PDyd6PKutWeO5Z6z3Pn9vbHZ2Nrb84MGDMmdwcFDGrP6Q9P3w5HmP5xmLrBzL6OioK0+x5maL9bzUMb3t0DpXRUX87yq899eqx9jYWGz597//fde5kl5beq/ZUw/vuaw81W48z3+1c3kcOXJExrq7u2XMsz63eNf1nr4+Pz8vY/v37y/6eNazrKysLPp4Ifjuo3du9swdSbdDi1V36904adY1P/3000XHmpqaZM5b3vIWV6yvr0/GFOs5LywsyJi17lTPzOoPSa87k957WC2W9LlU/V955RWZY+1ZnM3UOiWEEO6//34Ze/Ob3yxj27dvjy3v7e2VOVYbtd4FrHdxxVoHJP0eVs7x3Lsutqj1atLvFmcKv7QGAAAAAAAAAKQGm9YAAAAAAAAAgNRg0xoAAAAAAAAAkBpsWgMAAAAAAAAAUoNNawAAAAAAAABAarBpDQAAAAAAAABIjeyZrkCSvvOd78SWb926Vea0t7cnWocoilx5mUwm0Xp4j5fP52PLreuyzjU/Py9jjz76qIzt3btXxlCYp556Krb8LW95i+t4Sbftiork/87M0+5Vmw8hhFwuV/TxrPtkxSYmJmTsxRdfLKo8hBBGRkZkbK0aHh6WMatteNq2tz+oPKt+lZWVMma1UU9bXFxcTPR4q8WSzLFMT0/L2LFjx2TM6kcqNjo6KnOsmDUWeVjHs2JWW1SxpPtDCL77YeV4zuVt1941mGd8SLqveNuhZyyyrssz/3p96UtfkjFrrdLT0xNb3t3dLXO6urpkbP369TLW2dkpY83NzbHlSbcN65hJzwFeSfc9i3e8sXjqb81haTczMyNje/bsccVU/7v00ktlziWXXCJjLS0tMmbx9BWLZ262ckox1iueuluef/75onPOVfv27Ss6Zu2dbd++Xcbq6upkTM2l3jZq5VnzdtJjvaf9eteP1rvMI488UnQ9zib80hoAAAAAAAAAkBpsWgMAAAAAAAAAUoNNawAAAAAAAABAarBpDQAAAAAAAABIDTatAQAAAAAAAACpwaY1AAAAAAAAACA1sme6AknK5XKx5Q899JDMueOOO2Qsk8mcdp0KPV5Fhf77AxWLokjm5PN5GbPyFKvuTzzxhIx973vfk7HFxcWi64HCPf3007HlH/7wh2VOTU2NjFntxtNXrONZ/cHKUzFPzmrUePPjH/9Y5jz//PMy9tprr7nqgf/PGvcOHz4sYz09PUWfqxRtSvGO556Yd95bWFiQsZGRkdjyY8eOyZykY/Pz8zJnrVJj1GqsNmC1RSXpucN7XRY153j7nuc+Wcf0zonW/fXMl9a991yzleO9h0nzzCvWfFMK9fX1seXr16+XOV1dXTLW2dlZdMw6V3V1tYxZbVTFkp5jvcf0tl+rPyvWvJeWvpIWR48eLao8hBD++7//W8bOP/98GbvkkkuKjln9wUv1Fe+aLun5zVsPNee88MILruOhME8++aSMWe+527dvl7G3v/3tseXeNUw516pJ19HbHx599FEZW+vzAL+0BgAAAAAAAACkBpvWAAAAAAAAAIDUYNMaAAAAAAAAAJAabFoDAAAAAAAAAFKDTWsAAAAAAAAAQGpkogI+lzw9PR1aWlrKUR8AAAAAAAAAwBo2NTUVmpubZZxfWgMAAAAAAAAAUoNNawAAAAAAAABAarBpDQAAAAAAAABIDTatAQAAAAAAAACpwaY1AAAAAAAAACA12LQGAAAAAAAAAKQGm9YAAAAAAAAAgNRg0xoAAAAAAAAAkBpsWgMAAAAAAAAAUoNNawAAAAAAAABAarBpDQAAAAAAAABIDTatAQAAAAAAAACpUdCmdRRFpa4HAAAAAAAAAOAcsNp+c0Gb1jMzM4lUBgAAAAAAAABwblttvzkTFfAz6nw+H4aHh0NTU1PIZDKJVQ7lMT09HTZs2BAOHToUmpubz3R1gFSinwCFoa8AhaGvAIWhrwCFoa8AhaGvpF8URWFmZib09vaGigr9e+psIQerqKgI/f39iVUOZ0ZzczMdFlgF/QQoDH0FKAx9BSgMfQUoDH0FKAx9Jd1aWlpW/TN8iBEAAAAAAAAAkBpsWgMAAAAAAAAAUoNN63NATU1N+MIXvhBqamrOdFWA1KKfAIWhrwCFoa8AhaGvAIWhrwCFoa+sHQV9iBEAAAAAAAAAgHLgl9YAAAAAAAAAgNRg0xoAAAAAAAAAkBpsWgMAAAAAAAAAUoNNawAAAAAAAABAarBpnQLT09PhvvvuC5/+9KfD9u3bwwUXXBBaWlpCdXV1WL9+fbj++uvDPffcE8bHxws63oEDB8KnP/3psGXLltDQ0BDa29vD1q1bw5e//OUwNzeXaN2TPlcUReGee+4JAwMDobOzM9x9991hZmYm0Trj7PajH/0o/NEf/VHYsWNH6O/vDzU1NaGxsTFs3rw5fPSjHw2PP/54wceir2AtO3bsWPjWt74VPv/5z4f3vOc9Yd26dSGTyYRMJhM+8pGPFHUs+grWsnK1b9o20oi5gr6EwvAOQl+BjX2t19FPEhbhjHv44YejEMKq/1u3bl300EMPmcd64IEHoubmZnmMzZs3R/v27Uuk3qU411//9V9HnZ2d0de//vVo165d0RVXXBF9+MMfTqS+OPtde+21BfWVO++8M1pcXDSPRV/BWmf1kbvuuqvg49BXsJaVq33TtpFWzBX0JayOd5DX0VdgYV/rdfSTZLFpnQIPP/xwtGHDhujOO++M/uIv/iL6xje+ET3xxBPR7t27o507d0Yf+MAHosrKyiiEEFVXV0fPPvts7HGefvrpqK6uLgohRI2NjdEf//EfR3v27IkeeeSR6Dd/8zd/odNNT0+fVp1Lda63v/3t0b333nvy/z/11FNRZWVlNDc3d1r1xdqwadOmKIQQ9fb2Rp/85Cejr3/969HevXujJ554Irr33nujvr6+k23PmhjoKzgX/Pxia+PGjdGOHTuK3oigr2AtK1f7pm0jzZgr6EtYHe8gr6OvwMK+1uvoJ8li0zoFVlZWVv0z3/zmN092mFtvvTX2z7zxN8DZbDbas2fPKfF77rnn5DG+8IUvnFadS3WurVu3Rn/5l3958v8/99xzUUVFRXTixInTqi/WhptvvjnauXOn7DOjo6PR5s2bT7a9Xbt2xf45+grOBZ///OejBx98MDp69GgURVG0f//+ojci6CtYy8rVvmnbSDPmCvoSVsc7yOvoK7Cwr/U6+kmy2LQ+i1x44YUn/3WK/+uHP/zhyc509913x+bncrnooosuikIIUWtra7S0tOSqRynP9eUvfznq7u6OvvnNb0aPPfZYdPXVV0e33Xabq544Nz344IMn2+fv/M7vnBKnr+BcVexGBH0Fa1m52jdtG2ebc3GuoC8hCefCOwh9BUlY6/ta9JNk8SHGs0hTU1MIIYSFhYVTYv/xH/9x8p8/+tGPxuZXVFSEO++8M4QQwuTkZHj00Udd9SjluT71qU+F3/qt3wqf+MQnwi233BIuvvji8I//+I+ueuLcdMMNN5z855/+9KenxOkrQGHoK1jLytW+adtY69bCXEFfQhLOhXcQ+gqSsNb3tegnyWLT+izxyiuvhGeffTaEEMKWLVtOib/xteKGhoZw5ZVXyuNs37795D/v3r3bVZdSnquysjL84R/+YRgaGgrj4+PhK1/5SmhtbXXVE+emxcXFk/9cWVl5Spy+AhSGvoK1rFztm7aNtW4tzBX0JSThXHgHoa/gdJ0L+1r0k2SxaZ1ic3NzYd++feHee+8N27dvDysrKyGEEH73d3/3lD/7k5/8JIQQwgUXXBCy2aw85s8PDG/kFKuc5wKKtWvXrpP/fNFFF50Sp68AhaGvYC0rV5ujbWOtY64AXsc7CBCPfS2cDv1kcEZ87Wtfk/9qQgghfPaznw133HHHL5QtLCyEsbGxEEII/f395vHb2tpCQ0NDmJ2dDYcOHSq6fuU8F1CsfD4fvvjFL578/x/84Ad/IU5fAQpDX8FaVq42R9vGWsdcAbyOdxDgF7GvhaTwS+uzxGWXXRb27t0b/uRP/iRkMplfiM3MzJz858bGxlWP1dDQEEII4cSJE0XXo5znAor1Z3/2Z2Hv3r0hhBBuu+22U/41H/oKUBj6CtaycrU52jbWOuYK4HW8gwCFYV8LxWLTOmXe//73h+effz48//zzYe/eveFf//Vfw6233hqeffbZ8OEPfzh861vfOiXn5/8D9tXV1aueo6amJoQQwvz8fNH1K+e5gGLs2rUrfPaznw0hhLB+/frwt3/7t6f8GfoKUBj6CtaycrU52jbWOuYKgHcQIA77WkgKm9ZFyGQyp/2/r33ta+Y5Wltbw6WXXhouvfTSsHXr1vCrv/qr4Rvf+Eb4p3/6p/Daa6+FW2655ZRj1NbWnvznpaWlVa/jjY9E1NXVFX0PynkunL3K0Vd+3osvvhhuvfXWsLKyEmpra8O//du/hfXr15/y5+grSJty95VC0VewlpWrzdG2sdYxV+BcxzsIEI99LSSFTeuzxK/92q+FD3zgAyGfz4dPfOIT4fjx4ydjTU1NJ/+5kH9dYXZ2NoRQ2L8G8X+V81xAIfbv3x927NgRJiYmQmVlZbjvvvvCddddF/tn6StAYegrWMvK1eZo21jrmCtwLuMdBCge+1ooFh9iLEISXwrt6elx595yyy3h/vvvD7Ozs+Ghhx46+R+ur62tDR0dHWF8fDwMDQ2Zx5iYmDjZ4TZs2FB0Hcp5Lpy9ytVXhoeHw0033RSGh4dDJpMJX/nKV8Itt9wi/zx9BWlzpucVhb6CtaxcbY62jbWOuQLnKt5BAD/2tVAMNq2LsGXLljN6/s7OzpP/fODAgV+IXXzxxeGxxx4Lr776alhZWQnZbPyjffnll0/+80UXXeSqRznPhbNTOfrK2NhYeNe73hVee+21EEIIf/VXfxXuvPPOVfPoK0iTMz2vWOgrWMvK1eZo21jrmCtwruEdBDg97GuhGPznQc4ihw8fPvnP//dfS3jnO98ZQnj9X1t46qmn5DF27dp18p+3bdvmqkc5zwXEmZqaCu9+97vDSy+9FEII4Ytf/GL4+Mc/XlAufQUoDH0Fa1m52hxtG2sdcwXOJbyDAKePfS0UJcJZ45d/+ZejEEIUQogeffTRX4j98Ic/PBm7++67Y/NzuVx00UUXRSGEqLW1NVpaWnLVo5znAv6v2dnZaNu2bSfb4O///u8XlU9fwblq//79J9vjXXfdteqfp69gLStXm6Nt42zDXAHE4x0ESAb7WigGm9Yp8NWvfjWan583/8y99957skOdd9550crKyil/5tprr41CCFE2m4327NlzSvyee+45eYwvfOEL8lxv/JmBgQH5Z5I6F1CMxcXFaMeOHSfb1ic/+UnXcegrOBcVuxERRfQVrG1JtDnaNtYa5grgVLyDAKtjXwulkImiKAo4o970pjeFmZmZcPvtt4d3vvOdYdOmTaGxsTHMzMyE559/PvzLv/xL2L17dwghhOrq6vDtb3873HTTTacc55lnngnbtm0L8/PzobGxMXzuc58LN9xwQ5ifnw/33Xdf+Pu///sQQgibN28OP/rRj37hi6k/L5PJhBBCGBgYCIODg7F/JqlzAcW4/fbbwze+8Y0QQgg33nhj+PM///OT7TVOdXV12Lx58ynl9BWcCx5//PHw6quvnvz/Y2Nj4fd+7/dCCK//q20f+9jHfuHPf+QjHznlGPQVrGVJtDnaNs52zBXA6ngHAVbHvhZK4kzvmiOKBgYGTv7tjfW//v7+6Lvf/a55rAceeCBqbm6Wx9i8eXO0b98+8xihgL+RSupcQDEK6Sc//z+rDdNXsNbdddddRfUXhb6Ctex02xxtG2c75gpgdbyDAKtjXwulwKZ1Crz88svRn/7pn0a33XZb9Na3vjXq6uqKstls1NTUFG3atCm6/fbbo69+9avR7OxsQccbHByMPvWpT0WbN2+O6uvro9bW1uiqq66KvvSlLxV0jEI7dxLnAoqR5IIxiugrWNuS2oiIIvoK1rbTaXO0bZztmCuA1fEOAqyOfS2UAv95EAAAAAAAAABAalSc6QoAAAAAAAAAAPAGNq0BAAAAAAAAAKnBpjUAAAAAAAAAIDXYtAYAAAAAAAAApAab1gAAAAAAAACA1GDTGgAAAAAAAACQGmxaAwAAAAAAAABSg01rAAAAAAAAAEBqsGkNAAAAAAAAAEgNNq0BAAAAAAAAAKnBpjUAAAAAAAAAIDXYtAYAAAAAAAAApAab1gAAAAAAAACA1GDTGgAAAAAAAACQGmxaAwAAAAAAAABS4/8BOU2+tt0OD4UAAAAASUVORK5CYII=",
      "text/plain": [
       "<Figure size 1850x1050 with 1 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "from experiments import mnist\n",
    "import numpy as np\n",
    "\n",
    "# Load the MNIST-C dataset.\n",
    "mnist_c = mnist.datasets.MNIST_C(corruption='fog', split='test').reshape(784).to(device,dtype)\n",
    "\n",
    "# Find all misclassified images from MNIST-C with label `8`.\n",
    "_, misclassified_dataset = mnist_c.filter_label(8).misclassified(model)\n",
    "\n",
    "# Construct the polytope repair set by rotate each misclassified image with [-30, -20, -10, 0, 10, 20, 30] degrees.\n",
    "# An input polytope is represented as its seven vertices of the rotated images.\n",
    "rotation_dataset = misclassified_dataset.rotate(degs=np.linspace(-30., 30., 7), scale=1.).to(device,dtype)\n",
    "\n",
    "# Check an input polytope.\n",
    "image_polytopes, labels = rotation_dataset.load(1)\n",
    "print(f\"image_polytopes {tuple(image_polytopes.shape)}: {image_polytopes.shape[0]} polytope(s) of {image_polytopes.shape[1]} vertices.\")\n",
    "print(\"Expected labels:\", labels.flatten().long())\n",
    "print(\"Misclassified as:\", model(image_polytopes[0].to(device,dtype)).argmax(-1).cpu())\n",
    "mnist.imshow(image_polytopes, degs=rotation_dataset.degs)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "##"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Set parameter Username\n",
      "Academic license - for non-commercial use only - expires 2025-02-28\n",
      "Set parameter Crossover to value 0\n",
      "Set parameter Method to value 2\n",
      "Set parameter Threads to value 32\n",
      "Set parameter Presolve to value 1\n"
     ]
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "                                                 \r"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Gurobi Optimizer version 11.0.0 build v11.0.0rc2 (linux64 - \"Ubuntu 22.04.2 LTS\")\n",
      "\n",
      "CPU model: Intel(R) Core(TM) i9-9960X CPU @ 3.10GHz, instruction set [SSE2|AVX|AVX2|AVX512]\n",
      "Thread count: 16 physical cores, 32 logical processors, using up to 32 threads\n",
      "\n",
      "Optimize a model with 339725 rows, 249114 columns and 2144040 nonzeros\n",
      "Model fingerprint: 0x8348704d\n",
      "Coefficient statistics:\n",
      "  Matrix range     [6e-06, 4e+00]\n",
      "  Objective range  [1e+00, 1e+00]\n",
      "  Bounds range     [0e+00, 0e+00]\n",
      "  RHS range        [1e-06, 6e-01]\n",
      "Presolve removed 241042 rows and 86352 columns\n",
      "Presolve time: 0.93s\n",
      "Presolved: 98683 rows, 162762 columns, 1657406 nonzeros\n",
      "Ordering time: 1.28s\n",
      "\n",
      "Barrier statistics:\n",
      " Dense cols : 1\n",
      " Free vars  : 8701\n",
      " AA' NZ     : 1.695e+06\n",
      " Factor NZ  : 1.004e+07 (roughly 200 MB of memory)\n",
      " Factor Ops : 9.618e+09 (less than 1 second per iteration)\n",
      " Threads    : 32\n",
      "\n",
      "                  Objective                Residual\n",
      "Iter       Primal          Dual         Primal    Dual     Compl     Time\n",
      "   0   1.99968235e+01 -1.91539082e-03  2.98e+02 3.20e+01  4.86e+00     3s\n",
      "   1   1.38858943e+03  3.66963888e-03  6.69e+01 1.94e+01  3.57e+00     3s\n",
      "   2   2.13503632e+03  1.61209493e-03  3.93e-01 2.48e-01  2.22e+00     3s\n",
      "   3   1.14424518e+01  9.54284452e-04  4.10e-04 6.99e-02  1.72e-02     3s\n",
      "   4   6.08634875e+00  7.50152394e-04  1.85e-04 4.05e-02  8.38e-03     3s\n",
      "   5   5.55791628e+00  6.93594131e-04  1.66e-04 3.18e-02  7.27e-03     3s\n",
      "   6   3.48546422e+00  4.31511625e-04  1.01e-04 1.61e-02  4.15e-03     4s\n",
      "   7   2.18069993e+00  8.35132908e-05  5.95e-05 8.68e-03  2.46e-03     4s\n",
      "   8   1.57533039e+00 -1.29738852e-04  4.16e-05 5.87e-03  1.74e-03     4s\n",
      "   9   1.14962475e+00 -5.66253645e-04  2.94e-05 2.81e-03  1.23e-03     4s\n",
      "  10   6.58847301e-01 -1.23838067e-03  1.58e-05 1.04e-03  6.92e-04     4s\n",
      "  11   3.58124227e-01 -1.41170909e-03  8.12e-06 2.69e-04  3.73e-04     4s\n",
      "  12   1.64831789e-01 -8.91854132e-04  3.71e-06 9.34e-05  1.71e-04     4s\n",
      "  13   1.24018083e-01 -4.68643717e-04  2.77e-06 5.50e-05  1.28e-04     4s\n",
      "  14   9.05108462e-02  4.78055550e-05  7.41e-06 3.52e-05  9.33e-05     4s\n",
      "  15   6.90907925e-02  8.63939402e-04  5.49e-06 2.03e-05  7.04e-05     5s\n",
      "  16   4.92256588e-02  1.73630512e-03  4.09e-06 1.58e-05  4.90e-05     5s\n",
      "  17   4.30794155e-02  3.25591940e-03  3.52e-06 9.73e-06  4.11e-05     5s\n",
      "  18   3.57789442e-02  4.44241728e-03  2.41e-05 7.72e-06  3.23e-05     5s\n",
      "  19   3.17295511e-02  6.08025098e-03  1.99e-05 6.32e-06  2.64e-05     5s\n",
      "  20   2.86019049e-02  8.04115540e-03  1.63e-05 4.93e-06  2.12e-05     6s\n",
      "  21   2.74941491e-02  8.81320375e-03  1.50e-05 4.40e-06  1.93e-05     6s\n",
      "  22   2.52332186e-02  1.08566500e-02  1.22e-05 3.04e-06  1.48e-05     6s\n",
      "  23   2.24192464e-02  1.21253351e-02  8.70e-06 2.13e-06  1.06e-05     6s\n",
      "  24   2.17342526e-02  1.26361668e-02  1.79e-05 1.72e-06  9.38e-06     6s\n",
      "  25   2.05471405e-02  1.32868197e-02  1.48e-05 1.19e-06  7.48e-06     6s\n",
      "  26   1.84200761e-02  1.36465522e-02  9.22e-06 8.27e-07  4.92e-06     7s\n",
      "  27   1.72785277e-02  1.40001536e-02  6.50e-06 5.17e-07  3.38e-06     7s\n",
      "  28   1.65094158e-02  1.41914964e-02  4.91e-06 3.41e-07  2.39e-06     7s\n",
      "  29   1.59859440e-02  1.43238565e-02  3.41e-06 2.15e-07  1.71e-06     7s\n",
      "  30   1.56903480e-02  1.43984240e-02  2.87e-06 1.40e-07  1.33e-06     7s\n",
      "  31   1.53763205e-02  1.44390608e-02  2.08e-06 1.00e-07  9.66e-07     7s\n",
      "  32   1.52247249e-02  1.44591770e-02  1.58e-06 7.66e-08  7.89e-07     8s\n",
      "  33   1.50936247e-02  1.44981424e-02  1.62e-06 7.63e-08  6.14e-07     8s\n",
      "  34   1.48052307e-02  1.45204305e-02  7.61e-07 7.88e-08  2.93e-07     8s\n",
      "  35   1.46833833e-02  1.45353107e-02  4.24e-07 5.78e-08  1.53e-07     8s\n",
      "  36   1.46535518e-02  1.45437617e-02  5.28e-07 5.23e-08  1.13e-07     8s\n",
      "  37   1.46203746e-02  1.45457794e-02  3.68e-07 6.97e-08  7.69e-08     8s\n",
      "  38   1.46024052e-02  1.45465918e-02  3.66e-07 3.98e-08  5.75e-08     8s\n",
      "  39   1.45772213e-02  1.45470707e-02  2.07e-07 3.95e-08  3.11e-08     8s\n",
      "  40   1.45744545e-02  1.45474383e-02  1.73e-07 3.30e-08  2.78e-08     9s\n",
      "  41   1.45700244e-02  1.45477575e-02  1.65e-07 2.64e-08  2.29e-08     9s\n",
      "  42   1.45600843e-02  1.45479650e-02  3.52e-07 2.72e-08  1.25e-08     9s\n",
      "  43   1.45574177e-02  1.45485487e-02  2.63e-07 1.60e-08  9.14e-09     9s\n",
      "  44   1.45529889e-02  1.45486347e-02  1.30e-07 1.40e-08  4.49e-09     9s\n",
      "  45   1.45504257e-02  1.45486825e-02  4.61e-08 7.65e-09  1.80e-09     9s\n",
      "  46   1.45494621e-02  1.45486987e-02  3.27e-08 4.16e-09  7.86e-10     9s\n",
      "  47   1.45487465e-02  1.45486987e-02  1.62e-07 1.44e-09  4.92e-11     9s\n",
      "  48   1.45487130e-02  1.45487117e-02  2.05e-09 1.30e-09  1.30e-12    10s\n",
      "\n",
      "Barrier solved model in 48 iterations and 9.59 seconds (10.26 work units)\n",
      "Optimal objective 1.45487130e-02\n",
      "\n"
     ]
    }
   ],
   "source": [
    "import sytorch as st\n",
    "\n",
    "image_polytopes = image_polytopes.to(device,dtype)\n",
    "\n",
    "# We use an the Gurobi LP solver as the optimizer.\n",
    "optimizer = st.GurobiSolver().verbose_()\n",
    "\n",
    "# Attach the model to the optimizer\n",
    "model.to(optimizer)\n",
    "\n",
    "# Make the first layer weight and all-layer bias editable.\n",
    "model.requires_symbolic_weight_and_bias()\n",
    "\n",
    "# Toggle the symbolic-execution mode.\n",
    "model.repair()\n",
    "\n",
    "# Encode the symbolic output vpolytope, such that all vertices are in the same linear region.\n",
    "symbolic_output_vpolytopes = model.v(image_polytopes)\n",
    "\n",
    "# Prepare objectives: parameter detla.\n",
    "param_delta = model.parameter_deltas()\n",
    "\n",
    "# Prepare objectives: output delta.\n",
    "with st.no_symbolic():\n",
    "    original_output_vpolytopes = model.v(image_polytopes)\n",
    "output_delta = (symbolic_output_vpolytopes - original_output_vpolytopes).reshape(-1)\n",
    "\n",
    "delta = param_delta.norm_ub('linf+l1_normalized') + output_delta.norm_ub('linf+l1_normalized')\n",
    "\n",
    "# Find optimal parameters that satisfies the repair specification.\n",
    "assert optimizer.solve(\n",
    "    # Add the output constraint.\n",
    "    symbolic_output_vpolytopes.argmax(-1) == labels, \n",
    "    \n",
    "    # Specify the minimization objective.\n",
    "    minimize=delta\n",
    ")\n",
    "\n",
    "# Update the model with the optimal parameters that satisfies the repair specification.\n",
    "repaired_model = model.update_().eval()\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Evaluate efficacy of the  repaired model"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "image_polytopes (1, 7, 784): 1 polytope(s) of 7 vertices.\n",
      "Expected labels: tensor([8, 8, 8, 8, 8, 8, 8])\n",
      "Prediction after repair: tensor([8, 8, 8, 8, 8, 8, 8])\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAABa0AAAESCAYAAAD+E/kVAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjkuMCwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy80BEi2AAAACXBIWXMAAA9hAAAPYQGoP6dpAABGbUlEQVR4nO3deYxdZ33/8efO3Nn3GY9ntYfEwXEWIJsViEmcRMGUBhGSFCiRmkBLm0pQUQSVEK1ArVQVgppu6qJWBVS1apxSqBIoKWkIbmIHHLKRhaQO8dgejz2eGc/m2efe8/sjxD+oz+c793597vXx+P2SkMLz9fec55zzbOfxTU4miqIoAAAAAAAAAACQAhVnugIAAAAAAAAAALyBTWsAAAAAAAAAQGqwaQ0AAAAAAAAASA02rQEAAAAAAAAAqcGmNQAAAAAAAAAgNdi0BgAAAAAAAACkBpvWAAAAAAAAAIDUYNMaAAAAAAAAAJAa2UL+UD6fD8PDw6GpqSlkMplS1wkAAAAAAAAAsMZEURRmZmZCb29vqKjQv6cuaNN6eHg4bNiwIbHKAQAAAAAAAADOTYcOHQr9/f0yXtB/HqSpqSmxCgEAAAAAAAAAzl2r7TcXtGnNfxIEAAAAAAAAAJCE1fab+RAjAAAAAAAAACA12LQGAAAAAAAAAKQGm9YAAAAAAAAAgNRg0xoAAAAAAAAAkBpsWgMAAAAAAAAAUoNNawAAAAAAAABAarBpDQAAAAAAAABIDTatAQAAAAAAAACpwaY1AAAAAAAAACA12LQGAAAAAAAAAKRG9kxX4GxVX18fW/6hD31I5rz3ve+VsSiKTrtOhR4vn88nWg/vuTzH/Id/+AeZs2vXLte5cGa87W1vk7Ft27bJ2HXXXSdjVVVVseVJ9y9LLpeTMasemUym6DzreFZscXFRxn7jN35Dxrz9Gf9fU1NTbPnGjRtljhXbsGGDK0/FGhoaZI7VRsvZNjxzmLfvWdQxh4aGZM5nPvMZ17k8HnnkERlbXl52HVPde8/45T2XxRp/reN5zmXlWPfDilVWVsaWW9fl7ZcVFfG/W1lZWZE53jlHxVQdQrCvy8r7lV/5FRlL2t/8zd/Elg8MDMics2Ee9azrve8WVmxubi62/ODBgzLn0KFDrtiBAweKPtfMzIyMoTBWX/7nf/5nGaurq5MxNXYkPdevxnO+pN+p5+fnZWz37t2u2HPPPVd0PXDm3HDDDTL227/927HlVr9U65QQfGufcvYvK887Nz/wwAMytnPnzthyNbdB45fWAAAAAAAAAIDUYNMaAAAAAAAAAJAabFoDAAAAAAAAAFKDTWsAAAAAAAAAQGqwaQ0AAAAAAAAASI3sma5Amr3nPe+RsQ9+8IOx5S0tLTLH+2VtT473S6zevKSperz//e+XOY8//riM5XK5063SOe9Nb3qTjG3btk3Grrnmmtjy9evXu+phfS1Y9bFSfJk4DX3We7yqqioZe/vb3y5je/bsKaxiZ4j1RWur/Q4MDCSWE0IIGzdulLG2trbYcmt+8M4dnjbl/Xq2RdXD+jp50ufyfmXcc3/7+/tljtVGk56nlpaWXHmeay7FmkPFrDaa9D309i8rZrX7lZWVwipW4Lk8c1gp+oq6Zu+5SjFOKVaf7e3tjS33PMcQ/GuOpNfunjmnFGNAbW1tbPnmzZtlzpYtW2TM296UsbExGTt48KCMHThwoOg863iHDh2SsbS//6h3hBDstarVRpNeW5Tz/T1pNTU1MnbDDTe4YqOjo7Hl1jvC7t27ZWz//v0yhsJY89Ttt98uY573Zu/6RsW8/Svp8dxinevmm2+Wseuuuy62fOfOnTLnoYceKrxi5xB+aQ0AAAAAAAAASA02rQEAAAAAAAAAqcGmNQAAAAAAAAAgNdi0BgAAAAAAAACkBpvWAAAAAAAAAIDUYNMaAAAAAAAAAJAa2TNdgXK44oorZOwDH/iAjF1wwQVFnyuXy8lYFEWJxqycTCaTeD08rOPl8/mi81pbW2XO+973Phn75je/KWNrVXt7e2z5tddeK3O2bdsmY1Z/8DxLKydp3nbt7WPlknR/DSGEq6++Wsb27NmT+PmK9Xd/93cytnHjRtcxPffRar9WbGVlpehzWZIez8vZL61zeftX0vOl535Y59qwYYOMDQ4OFn0ubz28c3PS5/Ic07vO8rS3UswdVv2TnlcqKvRvUzzn8vbZpO9vOVnzinqW3vvuvR/quXjH86THAO81e9pNKeYVpaOjQ8bWrVsnY29729tkzDOHWbHDhw/L2Gc+8xkZK5d3vOMdMmaNldZzVv0v6XXFavXwtN+k+4qXda7Ozs7Y8ltvvVXmWLF9+/bJ2OOPPx5bvnv3bpkzMTEhY2uVdX+tvZOk3xO8ax/P8bxt3tMvrTnd0tjYGFv+67/+6zLn+uuvl7H7779fxp5++umC63U24pfWAAAAAAAAAIDUYNMaAAAAAAAAAJAabFoDAAAAAAAAAFKDTWsAAAAAAAAAQGqwaQ0AAAAAAAAASA02rQEAAAAAAAAAqZE90xUoVl9fn4x96EMfii2/5pprZE4URTKWz+cLr1gBxytFTMlkMkXnWOfy1CEE+x56rjmXy8mcX/qlX5KxPXv2yNjIyIiMlUtFhf77o+3bt8vYddddJ2Nbt26NLbfu+/Lysox524Anz9sfPH3Wy9PHrLp7+6zivRdve9vbZKy1tTW2fHJy0nUuj40bN8pY0mOst61Z45RnbLPaRjmv2TsGeNq2NSZ66+E5XtLjV39/v4wNDg4WfS6LNZ5725TK8871njzv2Jb0cy7FfKPqYT0vK2bVUeUlPReFkPx4Y40PSduwYYOMqXG7nGNlCPo5W/NK0kqxvkm6j3n6kbfvJT1PWax6WO23nNT68fLLL5c5Sa9vSvG8yvmcLaUYt5Wk++UFF1xQdOyjH/2ozNm7d6+M7d69W8asvYJyvl8q3d3dMnbzzTfLmPf9QklLX/G2ec9YX87nv2nTJhn7gz/4Axl7/PHHY8t37twpcw4fPlx4xc4wfmkNAAAAAAAAAEgNNq0BAAAAAAAAAKnBpjUAAAAAAAAAIDXYtAYAAAAAAAAApAab1gAAAAAAAACA1GDTGgAAAAAAAACQGtkzduKsPvUdd9whY7fddpuM5fP52PIoimSOFbOoPFWH06lHW1tbbPnCwoLreJ4863iZTEbGrPvhuVfe+3vzzTfL2Fe+8hUZK5evf/3rMlZTU+M6prpXuVxO5lj30MqzeJ6l9zlXVlbGlre0tMgcq/1OT0/L2MrKiowpSY9FpRhvrOe8devW2PKHH35Y5iQt6XYYgm/usO69p495n5e3jipmzc319fUypvpeCCEsLi7Gli8tLckcb9tWrH6eNKt+fX19ZauHNUZVVOjfLFgx1bat+2v1B09/LkVfUfUvxRhr3SuVZz0Ti3Uu1WfLec3WuSzePI/+/v6i62HVz3omnrZhxbz3yftulLRyjvUqz/uOY/VZz7Ms5xxWCldffXVsuTVPWesKz3PxPkuLd6xPMqcUPOOU915YfcVzriuvvFLGrrjiChn72Mc+JmMf+chHZKxc3ve+98mY991I5XmeyWr1UH2sFOsbT8x7PIsnz/uOfs0118SWb9u2Teb8+7//u4zt3LnTVY9S4ZfWAAAAAAAAAIDUYNMaAAAAAAAAAJAabFoDAAAAAAAAAFKDTWsAAAAAAAAAQGqwaQ0AAAAAAAAASI1sqU/w7ne/O7b8jjvukDnt7e0yZn1l2PMVb4vn653Wubq7u2Wsp6dHxtSXR62vrc7OzsrY//7v/8qYur/WvbCu2fsVepXn/XK99SXhH/zgB7HlL730ksxJWk1NjYwlfe89X/ZdrR6emFWP1tZWGVu/fr2MdXZ2xpYvLS3JHKvui4uLMrZ///7Y8pmZGZmT9Jfmk+5fIdjPRfWjhx9+WOYkzTueWzxtNOlxz9u/LG1tbTK2YcOG2PLGxkaZY90Pq6+o+WhsbEzmHD9+XMaS5u0rnuP19fUVfTwvbxtN+mvn3nFKtTerft7rUueqrKyUOZdffrmM1dXVueoxPz8fWz4+Pi5zDh06JGOe5+Kdpyyecc9zvFLo7++XMXWvStFGk14zWzx5Vt2rqqpkrKurS8bWrVsXW26t6aw12PT0tIzNzc3FllvzntUfSvHumYbjeW3dujW23Lq/Fuveq7boXfta9zDp+dK6Lk9MrfVCsPuDtQbz7Et47pN1TO/xLLW1tYkf0+PSSy+NLb/qqqtcx/OMRd5+6Rlvku5fq+V52lR1dbWMWfORp6+UYg2m3HbbbTJ2/fXXy9h9990XW/69733vdKsk8UtrAAAAAAAAAEBqsGkNAAAAAAAAAEgNNq0BAAAAAAAAAKnBpjUAAAAAAAAAIDXYtAYAAAAAAAAApAab1gAAAAAAAACA1MiW+gSf/OQnY8vz+bzMyeVyMmblRVFUVPlqMetcVVVVseXnn3++zGlvb3fVY25uLrZ8eXlZ5jQ2NsqYVcfh4eHY8snJSZnjvb/lZNXjPe95T2z5Sy+9VKrqnMJqa0nHvH3P21dUXiaTkTm9vb0y1tLSUnQ9FhYWZI51zXV1dTKm6njw4EGZMzs766qHJ6cU497GjRtjy/v7+2XO0NCQjHl4xxTPNZeir6iYdS5LTU2NjLW2tsqYatvWdVn9yKp/U1NTbHllZaXMmZiYkLGVlRUZU+OKNd54+4rnWfb09MhY0jzjcgj2vUq6Ht5YkjkhhJDNxi+HzzvvPJlj9T3vGKuOuWHDBplTX18vY9Y6xvOcrbon3W689Uia1WfVeFlRoX8T5B2LrLHZs36weOZZqz90d3fL2Pr164s+ZkNDg8xpbm6Wsba2NhlT7z/WXFSK9x/VPkqx9kmaNU696U1vii33jimee+8dl7318KxHrHWR1X67urpiy63+0NfXJ2PWHoPqK2NjYzJnaWlJxjzP0hpjvfNDOecwy3vf+97Y8lJcl+eYSY8p1rP05qk1XQghVFdXx5Z3dHTIHO8e3uHDh2PLp6enZY53vFH3w7sescabu+++O7b8e9/7nsw5XfzSGgAAAAAAAACQGmxaAwAAAAAAAABSg01rAAAAAAAAAEBqsGkNAAAAAAAAAEgNNq0BAAAAAAAAAKnBpjUAAAAAAAAAIDWypT5BPp8vqrwUMSsniiLXuVReXV2dzFlZWZGxkZERGRsbGyuqDqvV44ILLpCxiYmJ2PLp6WmZs7i4KGNemUym6BzrflixjRs3xpZfe+21Muexxx4rvGIFsOrnzcvlcrHl5ewPVqylpUXmZLN6aLLa2/DwcGy5atch2G2tqalJxjZt2hRbrvprCHY/su6vh7c/eI55xRVXyJyhoSHXuRRrHLV47kcp5inPuaw2WlNTI2Otra0ypu7jwYMHZc7U1JSMVVVVyVhbW1tseV9fX9E5IYRw7NgxGVP317qH3rFNsdpoc3OzjDU0NMjY7Oxs0fXwXpd1r1Sed+5Q85RVj1KMbered3Z2yhzrug4cOCBjk5OTMlZfXx9b3tPTI3Pa29tlrLKyUsaWl5dlzHM875ioePusR2Njo4x5xlFrDWMpRT/ynMtSURH/eyerr3R1dcmYda/Uu9HCwoLMscZR61n29/fHls/Nzckcqx7l5H2WSbvqqqtkTLVf1Z5CsOdSz/jgnTs876RWnnXN1li/bt06GVPv/fPz8zLHGs9ra2tlrLu7O7bcuodHjx6VMY9SrG/K6frrr5exgYGB2HLPO3+5WfdXxTzrwBDs9mv1I7X/YL3zW+84Vn9W67PDhw/LHOu9OennbN3DtMwrb+CX1gAAAAAAAACA1GDTGgAAAAAAAACQGmxaAwAAAAAAAABSg01rAAAAAAAAAEBqsGkNAAAAAAAAAEgNNq0BAAAAAAAAAKmRLfUJcrlcbHk+ny86J4QQoigqOmady3O8EEJobGyUMWV5eVnGRkZGZGxqaiq23KpfbW2tjDU3N8tYW1tbbPn4+LjMmZ2dlbGKCv33IplMRsY8zzLp2I4dO2TOk08+KWMLCwsyVmwdVpN0f/D2FavPqjZgPf+6ujoZs9rbkSNHYssXFxdljmVpaUnG1q1bF1teX18vc6qqqmRsbm6u8Ir9jHUPLd5xT8Uuv/xymfPAAw8UXrECWG3NknRfWVlZSbQe1rms59ze3i5j2aye4icnJ2PLh4aGZI63jqofrV+/XuZUVlbKmPUsvWOp53iqHt769fb2yti+fftkTLHaqPW8rHnbc7ykn5f3GVvXtWXLlqLPNTY2JmMHDhwovGI/Z3p6OrbcmovUui2EEDo6OmRMzZcW7/rBw/su4NHX1+eqh2r33vmhFGtcxTsGtLS0xJZv3LhR5ljPy3r/ee2112RMsdaP1nNR46+V42kbq8XOZldeeaWMqTaadF+2zmUpxTOpqamJLe/u7pY51lhkXZd6Tx8eHnYdz5pXenp6YsutNZ3aywjBfv9RfawUzyvptmjtxdx8882J1iPp9zrv+JX0+rGpqUnGVDtcLaZYewXWPpj1rtXZ2Rlbbq3NrH0ka770vJOU4p26VPilNQAAAAAAAAAgNdi0BgAAAAAAAACkBpvWAAAAAAAAAIDUYNMaAAAAAAAAAJAabFoDAAAAAAAAAFKDTWsAAAAAAAAAQGpkz9SJoyiSsXw+n2jMOlcul5Mxy+LiYmx5RYX+e4D5+XkZW15eljHPdan6hRDC3NycjPX09MSWW9dlPROrjpZMJlN0jlUPj/r6ehnbsWOHjD3wwANFn8tqh0n3laT7lzfW2trqOt7ExISMqX5k3UPv+DA7OxtbXlNTI3NWVlZcMdX/rH5p8fZZldfe3i5zLrzwQhl75ZVXZKzYOqzGMxZZzz/pe2jlWG2qubnZVY+DBw/Gllvt0BqXrfuh7qM1F2Wzenli1UPV38rxzDcW75jd29srY/v27Su6Ht71TWVlZaLn8saS1t3dLWPqmq3n9fzzz8uYNTZb7U21nYWFBZljrR+tmKeveMc9FbPO5V0XeVh9z7pmVX/vPFWK9bRHdXW1jHV0dMSWW/Wz1m0vvfSSjKn76203k5OTMtbZ2Rlb3tTUJHOsfmndD2uM9azdyzm/XXTRRTKm2kYI+n6Uoq8o1r3wrqctan1mrZmtMfvo0aMyNjQ0FFvuXdNZeer9WPWhEOw9EG/bTjInhOTH2JtvvlnGrD0GVQ/vu2zSc3PSMWu9b63brPFmaWlJxoaHh2PLp6enZY71vmK9o6m9gv7+fpnT1tYmY0nvgVisvKTnlULwS2sAAAAAAAAAQGqwaQ0AAAAAAAAASA02rQEAAAAAAAAAqcGmNQAAAAAAAAAgNdi0BgAAAAAAAACkhv5cZ0KS/hKrdTz1xWgrx/ulbvVlbevrw9bxpqamZEwd0/pCtvcLyerLo+oLyCGEMDY2JmPW/fV8qbkUX0BVdbRytm3bJmMPPPBA4RX7GetZer8IrI5pfRG6FH1FfRXY236teqivBXuPZ12X+vKz9RVk66vgnjbg/eJ20s/Zyrnssstk7JVXXpExxdtuLJ7rsurh+aq9p62tVg/ra+1Jz5fWva+trZUxxRqnFhcXZUxdlzXfeL+EnvQX3q2vpHtYbcPimWetc3nrkTSrHao6jo6Oypyk5+YQdHurq6tzHc/qs6qPedePnnnWew89Y6ylt7fXdS7PnONdc1gxVQ/vnNjQ0CBjjY2NseUnTpyQOUePHpWxpO+vtQazYrOzs7HlCwsLMse7Hinnu3HS57rqqqsSPVc5xwBvf6isrJSxqqoqGevr64stt9Z0x44dk7HDhw/LmFoXedc31hpMtXtrDFD7JiHovheCrqNnD2E1SfeV7du3y1g510WePmblWPfe6pdqXunv75c57e3tMma9C1hrtwMHDsSWW9dlxay+UlNTE1tuzSsW65pVX/GsHVaLJd1XCsEvrQEAAAAAAAAAqcGmNQAAAAAAAAAgNdi0BgAAAAAAAACkBpvWAAAAAAAAAIDUYNMaAAAAAAAAAJAabFoDAAAAAAAAAFIjW+oT5HK52PJ8Pi9zko5FUeQ6npU3NzcXW76ysiJzKir03xG0tbXJ2PHjx2PLrfpVV1fLWEdHh4ypOqrnGEIItbW1MjY/Py9jVv09vMdTedaztNqNh3V/k75PFm/fs+qoYsvLyzLHuvfWuTKZTGy5dX+tftnZ2Sljqo/NzMwUnRNCCAsLCzKm7r1Vd88z8casnMsuu0zGdu7cKWOK9SzV81+Nur/eMcDTZ7393KrH4uKijKn7aN1fS0NDg4yp+c1qv9Z1LS0tFV6xAnjbjac/WNfV3d3tqofnXNY1e+Yj65q9fdbzXKyc1tZWGVP1Hx0dLTonBHvssNTX18eW9/X1yRzr/o6NjcmYqmM2q18NvHOpR9JjrKWnp8d1Ls9asBTXpdq99Uys9Yj1TqLyRkZGZM7k5KSMee6h1UYbGxtlrLm5WcbUe501j3rf+bxzjkfS7ytXXnmljCW9fvTGkj5eXV2djFljh8qbnp6WOcPDwzI2OzsrY542ZbXRmpoaGWtqaootHx8flznWus3zXpf0uGydqxTK2baTzrPur/UusH79+tjyrq4umWONsYODgzI2NTUlY+qavXOzNR+p+lt7Z0NDQzJmUfUvRbsuZ195A7+0BgAAAAAAAACkBpvWAAAAAAAAAIDUYNMaAAAAAAAAAJAabFoDAAAAAAAAAFKDTWsAAAAAAAAAQGqwaQ0AAAAAAAAASI1sqU+Qy+Viy6Mokjn5fL7o41l53nN58iYnJ2VOQ0ODjFVWVspYsXVY7Xjz8/MyVldXF1ve0dHhOtdPf/pTGauo0H9nou699UysmNVuVMzbNjysc2UyGVc91DGte7GysiJjXouLi7Hl3udl1VG1KSsnm9XDYE1NjYx52qjVVzxtysrxthuLZ4y17q+H9Syta7ao+nvmm9V46mjd36qqKhlbWFiQMTUPWOeyxuzW1lYZa2triy1fXl6WOdPT0zLmab/eMdZzTO/c0d3d7aqHUoo26plXvOONqoc1jqo1zGoxNU9NTEzIHO/a0loLXnbZZbHl1jh64sQJV0yxnmXSc5i3r1h19Ojt7XXVQ7GuqxRrS9VXrOM1NjbKWHNzs4ypY46Pj8scay6y7kd1dXVsuTVWrlu3TsasMWBwcDC2POm5KITk1wHemIc1BnjadtLrUYt3zWyNv2p9E4Ku47Fjx2TOzMyMjHnqb73HWGNAT0+PjClWX7HmoqTnFetZluLdqFy89fOMD96+YvVLNa9YOUeOHJExa87x7GdY12W9a1lrOjVXWf3c6iuetY9nj3E13veL08EvrQEAAAAAAAAAqcGmNQAAAAAAAAAgNdi0BgAAAAAAAACkBpvWAAAAAAAAAIDUYNMaAAAAAAAAAJAabFoDAAAAAAAAAFIjW+oT5PP5ospXk8lkZCyKotjylZWVonNWMzk5GVve09MjcyorK2WstrZWxioq4v9uwbou61zV1dUytri4GFtu1a+7u1vGrLyxsTEZGxkZiS232o03ptqAJ8crl8vJmKfNh6Dbh3WupK8rBF3/hYUFVz1qampkzDPeZLN6GKyvry/6XA0NDTJn48aNMjY/Py9jql9avM/S0+6tNuUd6z3H8/YVzxiQ9HVZ7dC6Lmusr6qqkjH1zLx9pb29XcbU/VVzm5WzGpWX9PG8x7TurzU3e3iv2erPine+9PRZ61wtLS0y5uEd26zYwMCAjKn7YR1v//79MmZJeu2TdH8u51rFWqt6xgDvuJF0zOpf1juENXcopVifq/eL3t5emWONo9PT0zI2OjoaW760tCRzrPnXYvUVD6ttJL1WSbqNlnNu9s5F1hq8nH3FGhPVGqyvr0/mNDY2yph1P44cORJbPj4+LnO87dAztpVznrJYdUx67VOK93fPuaz3BM87pLce1r1S7d5aP1r7AW1tbTLW1NQUW37gwAGZMzU1JWPWvVJtO+k5wDpXKfFLawAAAAAAAABAarBpDQAAAAAAAABIDTatAQAAAAAAAACpwaY1AAAAAAAAACA12LQGAAAAAAAAAKSG/sRnQjxfrPR+DVTFvF86tqivvk5OTsoc9WXfEELo6uqSsePHj8eWW1/utL5kan2xdmFhIbZ8eHhY5lhfVN2wYYOM1dXVydj8/Hxs+cTEhMxJ+mvM5fxKr/UVd+8Xkj39oRRfmFVfV7e+xu1t2x0dHbHlVruxvqxtfYV+dnY2tty6h7W1tTK2adMmGTt69GhsufdL3d42oPqK1X6T7iulaKPqmNZXmq16WH1WsfqDdTxve+vt7Y0tt8Z6q41aX6FX84rVv8477zwZm5mZkTE1d1iSXiN4+145+4qnjVrH9F5X0vOs9dV1a5xSc875558vc1599VUZ27Jli4xZc5gac6zn5V0jlLO9Jd1uyll3Tz1K0R8sKs9qG2oNs1pMrd2t9xhrftu4caOMtbS0xJardWUI9rx96NAhGfPMHaVYj6hnlvS7cSkk3S+TVor6TU9Py5hqv9YcYLVD9Y4TQgjNzc2x5da7tvWuNTo6KmOqH3nf6zySfjdeLS9pnvpb97Cc12XV3Rp/l5aWYsutNtrU1CRj69atkzFrb0q9r1jvMdms3jK11pYHDhyILVfv9SHY/cia+xTr+XvXluWcV97AL60BAAAAAAAAAKnBpjUAAAAAAAAAIDXYtAYAAAAAAAAApAab1gAAAAAAAACA1GDTGgAAAAAAAACQGmxaAwAAAAAAAABSI1vqE+RyudjyTCYjc/L5fNHHs/Ks41miKJIxVf+5uTmZMz8/L2O1tbUytnnz5tjyxcVFmdPS0iJj1v2YmJiILR8bG5M5VVVVrlhnZ6eMdXV1xZYfO3ZM5ljPyxsrl1K0UXVMqw9ZMa+VlZXYcqv9Tk1NyVhjY6OM9ff3x5b39PTInIaGBhlbWlqSMdUWrb5itfkNGzbIWEVF/N8vWueynqW3P6g25cnxssbYuro6Vz1U/T05q8U89/D48eOuWHNzs4ytX78+tlyNvSHY47mnr1RWVsqc9vZ2Gdu4caOMHT58OLb8xIkTMsfieZZWu/HGPKx1VtLzZSnGAE+eNSZaMdXerHb4jne8o/CK/RxPX7fmji1btsjY0aNHZUy1D++ayPO8vO0m6XVb0mN9KdaVSa9jl5eXZWx8fFzGuru7Y8vb2tpkTkdHh4xZdVfrmIWFBZljzStWLOlnVs62bR3Pevf0sOYVz/0txbubqqNVdytmva9Y91e9r1hrs9bWVhnzrB+sHGtdNDw8LGOeNmXdX49SzFNJjwHea/bMzd62rY7pPZ5F7QdYrHf0Cy64QMas5+wZH6y+Mjo6KmMHDhyILVfv9SH45ynPGsy6ZquOZ2LvjF9aAwAAAAAAAABSg01rAAAAAAAAAEBqsGkNAAAAAAAAAEgNNq0BAAAAAAAAAKnBpjUAAAAAAAAAIDXYtAYAAAAAAAAApEa21CfI5XKx5VEUuY6Xz+cTzbHq4anjzMyMjA0NDclYX1+fjFVXV8eWV1VVyRx130MI4cSJEzJ29OjR2PLl5WWZY93f4eFhGWttbZWx2tra2PKWlhaZc/z4cRlL+jl726+ysLAgY+r5r0Y9l1L0B09sYmJC5mQyGRnr7++Xsbq6uthyb1+x6njs2LHY8vn5eZljXdf69etlTF1Xc3OzzBkbG5Mx63lZ7WNlZaXonKT7yuHDh2Vs06ZNrmMmPQZ47q+VMz09LWPWvNLT0yNjTU1NseUVFfrvstXzDyGEkZERGTty5EjR56qsrJQxa+5Qc7B1Dz3rCivPGlOsWNK8/dyT572Hnn5k5VjtZnBwUMZqampiy9XYG4L9LK37YfXZQ4cOxZZb67aBgQFXzKpHuXj7Q9LzSlpYawSLNZYqS0tLMjY1NSVjah3e0NAgc6y5Y25uTsbUOsa6Xmvea2trkzE1T1nPpBTvsp5xz2KtmZLmbb9Jn8tzr7zH86z5reNZfcXql6ofdXV1yRxrvrTGZlV/7z1Mel3kXZ8vLi6WrR6ee1WKdy1PG7W8+c1vljG1t2Ody1r7WPfQmt8Ua34YHR2VMev9RynnfovFalPlfLcvBL+0BgAAAAAAAACkBpvWAAAAAAAAAIDUYNMaAAAAAAAAAJAabFoDAAAAAAAAAFKDTWsAAAAAAAAAQGqwaQ0AAAAAAAAASI1sqU+Qy+Viy6Moch0vn88nei7reBZ1ruXlZZkzPz8vY3NzczLW0tISW97c3CxzGhoaZKyyslLGVlZWZExR9yKEEBYXF2VsdHRUxtQ1W/fQ+yxVXinajbJ3714Zu+aaa2TMU0crpxQxVY+FhQWZc/ToURmz8np7e2PLW1tbZU42q4dBq41abVGxxofx8XEZW7duXWx5fX29zLH6ZSmec7kMDw/L2Pnnny9jnusq533y3tvjx4+7jqn6ihp7QwhhbGxMxg4cOCBjS0tLseXV1dUy58SJEzLW0dEhY6pPeNYOq1HHtI5n1SPp/nW2jwEVFfG/q/DWYWpqSsbUuGKNKZannnpKxmZnZ2VMXbM1PwwMDMiYmjtC0H3Wur+ZTEbGPO0m6XVbKahnEoJv7rB4r0udz/u8ampqZEzdD+v9YWhoSMasdZY6Zl1dncyx3o2qqqpkTK0Tp6enZY4l6THWezxrzZR2Vvv15HmP19XVJWP9/f0yptb81lxkraUs1vuFYtXdsx/gvb8WVY+k56IQQnjyyScLr9hp8qwTyznvWWOl1W6s8VftCVnvFoODgzLm1d7eHlve1NQkc6w50bMfUIr2m/S7ZznfVwrBL60BAAAAAAAAAKnBpjUAAAAAAAAAIDXYtAYAAAAAAAAApAab1gAAAAAAAACA1GDTGgAAAAAAAACQGmxaAwAAAAAAAABSI1vqE/zXf/1XbPm73vUumRNFUaKxpI9nxfL5vMyxYqOjozI2MTERW97Z2SlzBgYGZGxhYUHGMplMbLn3PlnXXFdXV3Seqt9qrDp6jmkdz+PJJ5+UsXe84x2uY3quy8qxnmU5++XU1JSMVVZWxpY3NDTInOXlZRnL5XIy5mmjS0tLMjYzMyNjXV1dseUrKysyx/u8PHneZ+lx+PBh17mSvi6L1QbUMSsqfH+HbLWBubk5Gctm46d/63izs7MyZrVtxVt367mo+2j1cy9Vf2vcsCTdV7w89fC0eW9e0vN5CCFs3Lix6Jxjx47JmNVXvHVUrPuh5kSrHla/9NZDjb9WX/H083JL+ll6j6eeszXvWaz3i5qamtjykZERmWPFFhcXC6/Yz1RVVcmY1earq6tlzPNeVwrqfN511vDw8GnX6ed5x3pPjncd6+lHVptSa/DVzjU0NBRbfvz4cZljrX0sqm1b99Dqey0tLTI2Pz9feMV+xvucPcfzevrppxM/pmLVX82L1n3yzh2q3bS3t8ucDRs2yJh1XS+//HJsudXmrfWIdc3WPKDeB6zjWXW01iPqfnifl3dM9LCO98gjjyR6rkKkY9UHAAAAAAAAAEBg0xoAAAAAAAAAkCJsWgMAAAAAAAAAUoNNawAAAAAAAABAarBpDQAAAAAAAABIjWypT/Dggw/Gll999dUyp6GhQcbK+dXMcn4x2jqX+srpwsKCzLG+mlpfX1/0ubxfrLW+Pmx9xXt6ejq2fGlpyVUPi2o3SX+Z2vKTn/xExsbGxmSso6NDxjzXVYo2r+5V0s8rBP0lbPW1+xB0mw8hhGPHjsmYqr9VP6vNW31F1XFqakrmeMdKT6yc4/Lw8LCMWfXw1LEUXyf3tBtvPazxUs0D1pe6X3vtNRmz+rOKqS+kh+BvU2oMsFj1sCT9xftStDfF+9V1xVt3zz206mcdz/rCe1VVVWy51TZeeOEF17ks6j56+4rVH6w1pGK1G6sNqPp71xzWOOXhXY948rx9Jek1aW1trYw1NjbKmHpmL7/8ctF1CMHXV6zrtdZ7VntT/cE7P1iSngesnCNHjhR9PO+5LOree8c2DzXOhxBCZ2enjFnvzdYYOzg4GFtutV/v3JHNxm/pWO8WFmv9qJ5L0u/GIfjW51ZsfHxcxrxjmGLNU1bbVn3Ce83Wc6mrq4stt/qD1WdHR0dlbGJiIrbc8/6wGut9W+2dePe6LOV850u6/83MzMjYt7/97UTPVQh+aQ0AAAAAAAAASA02rQEAAAAAAAAAqcGmNQAAAAAAAAAgNdi0BgAAAAAAAACkBpvWAAAAAAAAAIDUYNMaAAAAAAAAAJAa2VKfYH5+Prb8wQcflDkf+tCHZCyTyZx2nQplnSuKoqJzLOp4luPHj8vY5OSkjLW2tsrYwMBAbPm+fftkTjarm1FjY6OM5XI5GRsbG4stz+fzMse6h56Y91xJ+9GPfiRjO3bskDFV/1LU3dPuvfWw8mZnZ2PL1TgUQgh1dXUytm7dOhlTbdS6F+3t7TJm9RV1LnW9q9XD4nkuVo7Vzz2Gh4dd9fDw3kMrzxpXlIoK/ffL3nFqeXk5ttwaz62+YvUxxeoPPT09MqbqHkIIhw4dii1fWVmROUnPHeWcHyxWPaw2Ws51ltW21djhrZ/Vfj3PzLNGXC2mjllfX+863vT0tIx5xiKL1cfUubz3MGnlbPPWffeO5yrPGs+t8deqx4kTJ2LLveONda7KysrY8traWpljjSkzMzMyZvUVxdturGv2rJmsaz569GjRxysFz7uWdS88Y0dDQ4PMaWlpcdVjZGRExhRPXw7B7s+qT1jXvLCwIGMTExMy5pmbk+4r3vnhmWeeceV5JN3PS9FuVMxqN9a5Dh48KGOevTPrmquqqmTMqr96t7feLcbHx2XMepZqbC7F2ifpNd13vvMdGbPGjlLhl9YAAAAAAAAAgNRg0xoAAAAAAAAAkBpsWgMAAAAAAAAAUoNNawAAAAAAAABAarBpDQAAAAAAAABIDTatAQAAAAAAAACpkT1TJ/7+978vY1dffbWMDQwMyFg+n48tj6JI5lgxSyaTceUleTwrZ2RkRMZaW1tlrLu7O7Z8bGxM5lRWVspYS0uLjM3Pz8vY9PR0bPny8rLMUc9/NZ524z2Xx1NPPSVjN910k4yp+nvbvMVqiyrmrYeVp9ri1NSUzKmtrZWxjo4OGTt+/HjRx2tra5Mxq22Pjo4WnVMKnjaVdF+ZnZ2VscnJSRmzxr2KiuL//tbbftW5SjGmVFdXy9jCwkJseX19vcypq6uTMWs8V3mdnZ0yx+pHBw8elDHVPrzrAE/bLsW5PKx27a2Hp69YbduKqXp4j9fY2Fh0nvdc1pxo3cOLL744ttyai1RfDiGEF198UcaSHnOsdqPuh+f5h2CvOz28/cFzXVYsl8vJmEXV0WprNTU1rnpYc7Bi3cOGhgYZ6+rqii23+vLc3JyMWe9G5ewPnnZvjSlqPRqCfT88vG1U5VnH8z4TdQ+tc1lrDivPuvee+dJ6T7DWZ+p921qbHTlyRMasfq6uy2qjSb/zedc3zzzzjKseHt75Len395WVFRlTbXtxcdF1LqsfKdms3o60+oN1P6z3C9Unjh49KnPUvtRq9fDw9iNPPaz3qf/5n/8p+nilxC+tAQAAAAAAAACpwaY1AAAAAAAAACA12LQGAAAAAAAAAKQGm9YAAAAAAAAAgNRg0xoAAAAAAAAAkBpsWgMAAAAAAAAAUiN7pisQ51vf+paMffzjH5exKIqKKj8dmUymqPJS1COXy8nYwsKCjI2NjclYS0tLbPmmTZtkTlVVlYwtLS3J2NGjR2Vsfn4+tjyfz8sc6/5aecr09LSM7dq1q+jjeQ0NDcnY4OCgjA0MDMSWW23UUlGR7N9xWc/E+5xVn5idnXWdq6OjQ8ZU+2hra5M5zc3NMnbw4EEZm5ycjC23xgCLt6+omHW8Uoy/yvDwsIy1trYWfTxvX/Fcs/ceevuKmiPq6upkTlNTk4wtLy/LWGdnZ9HnGh8flzFrDlN9opzP0ju2lZN3PE/6flhjWNLnWllZKboeVh1qampkzGpv5513noypNdiJEydkznPPPSdjnrHDqrv1vDzrX2+/TLofWffJW0elFGsfFbPavGctZeVZ84M11qv5IYQQGhoaYssXFxdlzoEDB2Ts8OHDMpb0WsX7LD2OHDmS6PG8PG3b6l/esUix+oP1npDN6u2Snp4eGauvr48tt/qKFbPet5XXXntNxo4fPy5jSb9Te9e4nrnDem+23hOSdv/998vYTTfdJGONjY2x5aV4n5qZmYktt/qXNZ5feOGFMqb2dqz1qNX3rJi1D6b2n6y5w7ofVv09z8y7l+hZqzz00ENF55wp/NIaAAAAAAAAAJAabFoDAAAAAAAAAFKDTWsAAAAAAAAAQGqwaQ0AAAAAAAAASA02rQEAAAAAAAAAqcGmNQAAAAAAAAAgNbJnugJxXnzxRRl78sknZezyyy9PtB4VFcXv6WcyGde5crmcjOXz+djyKIpkzvT0tKseVVVVseXWvbDqMTQ0JGNHjhyRMXXNqvx0PP7447Hl3//+92VOKerh8fTTT8vYwMBAbLmnXZ8Oq314cqzY0tJSbPnU1JTMmZiYkLHGxkYZU/fX6stWm7dii4uLseVWO/TeQyvm6Zeq7qVg3cNLLrkk0XNZY33S99BzvBBCWFhYkDHVJ6w239PTI2O9vb0ytry8HFs+Pj4uc6xneeLECRnzzJcWz3OxcqyYd/2QtHLOb9ZzUWOpd/yy1kWqr6g1UQghXHHFFTLmnWfHxsZiywcHB2WO1c8tqo7eNmrNfR7WsyznOsbTH7zjedLHtOZfa+3T3NwsY21tbbHl7e3tMscyNzcnY6Ojo0WVh2Cv95J+Lt5n6RnDrL43MjLiqoeHNd5Y46VnvvTeX8Wqu7UesfqDtWZqaGiILbeuy1rfzM/Py5haM83Ozsoc71ivYt5nmfTa59lnn030eF7WnpX1/n7jjTfGll933XUyJ+l10Q9+8AOZo95/Q7D7imof1nyu3utDsOcwa+6z+oRi1dHTj7x9xaqHiln94Sc/+YmMpQ2/tAYAAAAAAAAApAab1gAAAAAAAACA1GDTGgAAAAAAAACQGmxaAwAAAAAAAABSg01rAAAAAAAAAEBqZM90BYr1n//5nzJ2+eWXx5Z7voC7WszD+6VQFbNyvF9bVV9UrampkTnWl449X2gNwfeV6RdffFHGdu3aJWPWF6PT7qmnnpKxW2+9Nbbc+wVnb39I+ovhVp6Kqa8jhxDC4OCgjLW1tcmY+mL4sWPHZI71hffl5WUZ83xB3bpPXvv27Ystf+GFF2TOSy+9lHg9FPX19BCSH8+T/qq9dbxcLufKW1hYkDHVFq3j9fX1yZj1pe6xsbGi6hCCPXdY98PDO94kPbYlzfu1c++Xyz3H84znnvVSCPZa5eWXX44tv/jii2WOdS9mZmZkbGhoSMbUesSaH7zUmOi9v97n7JH243nvk8Uzh1nXZa19s1n9etjS0lJ0jvXeYfWV+fn52HLrHce6Zuseet61vO0m6bW2NZcm7XOf+5yMXXbZZTL21re+Nbb8wgsvlDnetY+ysrIiY/v375ex4eFhGevo6JAxNUdYazPrmq11lsorxXhezvWviln95Mc//vFp16nUrOf88MMPx5Y/88wzMufGG2+UsUsuuaTwiv2MVT/rvbmqqkrGrDlCSXr9aMU884M35p0DrOuqrKyMLf/ud78rc84m/NIaAAAAAAAAAJAabFoDAAAAAAAAAFKDTWsAAAAAAAAAQGqwaQ0AAAAAAAAASA02rQEAAAAAAAAAqcGmNQAAAAAAAAAgNbJnugLFGhkZkbHvfve7seU7duyQOZlMxlUPT573XFEUxZbn8/mic0IIYXl5uejYzMyMzMnlcq56WLHDhw/Hlu/atUvmvPrqqzK2Vk1PT8vYiy++GFt+6aWXJl4P61l6WG3b0+6tNj8xMSFjk5OTMra0tCRjHt6+oqg+FIJuGyGE8MILL8jYiRMniq5HOQ0PDyd6PKutWeO5Z6z3Pn9vbHZ2Nrb84MGDMmdwcFDGrP6Q9P3w5HmP5xmLrBzL6OioK0+x5maL9bzUMb3t0DpXRUX87yq899eqx9jYWGz597//fde5kl5beq/ZUw/vuaw81W48z3+1c3kcOXJExrq7u2XMsz63eNf1nr4+Pz8vY/v37y/6eNazrKysLPp4Ifjuo3du9swdSbdDi1V36904adY1P/3000XHmpqaZM5b3vIWV6yvr0/GFOs5LywsyJi17lTPzOoPSa87k957WC2W9LlU/V955RWZY+1ZnM3UOiWEEO6//34Ze/Ob3yxj27dvjy3v7e2VOVYbtd4FrHdxxVoHJP0eVs7x3Lsutqj1atLvFmcKv7QGAAAAAAAAAKQGm9YAAAAAAAAAgNRg0xoAAAAAAAAAkBpsWgMAAAAAAAAAUoNNawAAAAAAAABAarBpDQAAAAAAAABIjeyZrkCSvvOd78SWb926Vea0t7cnWocoilx5mUwm0Xp4j5fP52PLreuyzjU/Py9jjz76qIzt3btXxlCYp556Krb8LW95i+t4Sbftiork/87M0+5Vmw8hhFwuV/TxrPtkxSYmJmTsxRdfLKo8hBBGRkZkbK0aHh6WMatteNq2tz+oPKt+lZWVMma1UU9bXFxcTPR4q8WSzLFMT0/L2LFjx2TM6kcqNjo6KnOsmDUWeVjHs2JWW1SxpPtDCL77YeV4zuVt1941mGd8SLqveNuhZyyyrssz/3p96UtfkjFrrdLT0xNb3t3dLXO6urpkbP369TLW2dkpY83NzbHlSbcN65hJzwFeSfc9i3e8sXjqb81haTczMyNje/bsccVU/7v00ktlziWXXCJjLS0tMmbx9BWLZ262ckox1iueuluef/75onPOVfv27Ss6Zu2dbd++Xcbq6upkTM2l3jZq5VnzdtJjvaf9eteP1rvMI488UnQ9zib80hoAAAAAAAAAkBpsWgMAAAAAAAAAUoNNawAAAAAAAABAarBpDQAAAAAAAABIDTatAQAAAAAAAACpwaY1AAAAAAAAACA1sme6AknK5XKx5Q899JDMueOOO2Qsk8mcdp0KPV5Fhf77AxWLokjm5PN5GbPyFKvuTzzxhIx973vfk7HFxcWi64HCPf3007HlH/7wh2VOTU2NjFntxtNXrONZ/cHKUzFPzmrUePPjH/9Y5jz//PMy9tprr7nqgf/PGvcOHz4sYz09PUWfqxRtSvGO556Yd95bWFiQsZGRkdjyY8eOyZykY/Pz8zJnrVJj1GqsNmC1RSXpucN7XRY153j7nuc+Wcf0zonW/fXMl9a991yzleO9h0nzzCvWfFMK9fX1seXr16+XOV1dXTLW2dlZdMw6V3V1tYxZbVTFkp5jvcf0tl+rPyvWvJeWvpIWR48eLao8hBD++7//W8bOP/98GbvkkkuKjln9wUv1Fe+aLun5zVsPNee88MILruOhME8++aSMWe+527dvl7G3v/3tseXeNUw516pJ19HbHx599FEZW+vzAL+0BgAAAAAAAACkBpvWAAAAAAAAAIDUYNMaAAAAAAAAAJAabFoDAAAAAAAAAFKDTWsAAAAAAAAAQGpkogI+lzw9PR1aWlrKUR8AAAAAAAAAwBo2NTUVmpubZZxfWgMAAAAAAAAAUoNNawAAAAAAAABAarBpDQAAAAAAAABIDTatAQAAAAAAAACpwaY1AAAAAAAAACA12LQGAAAAAAAAAKQGm9YAAAAAAAAAgNRg0xoAAAAAAAAAkBpsWgMAAAAAAAAAUoNNawAAAAAAAABAarBpDQAAAAAAAABIDTatAQAAAAAAAACpUdCmdRRFpa4HAAAAAAAAAOAcsNp+c0Gb1jMzM4lUBgAAAAAAAABwblttvzkTFfAz6nw+H4aHh0NTU1PIZDKJVQ7lMT09HTZs2BAOHToUmpubz3R1gFSinwCFoa8AhaGvAIWhrwCFoa8AhaGvpF8URWFmZib09vaGigr9e+psIQerqKgI/f39iVUOZ0ZzczMdFlgF/QQoDH0FKAx9BSgMfQUoDH0FKAx9Jd1aWlpW/TN8iBEAAAAAAAAAkBpsWgMAAAAAAAAAUoNN63NATU1N+MIXvhBqamrOdFWA1KKfAIWhrwCFoa8AhaGvAIWhrwCFoa+sHQV9iBEAAAAAAAAAgHLgl9YAAAAAAAAAgNRg0xoAAAAAAAAAkBpsWgMAAAAAAAAAUoNNawAAAAAAAABAarBpnQLT09PhvvvuC5/+9KfD9u3bwwUXXBBaWlpCdXV1WL9+fbj++uvDPffcE8bHxws63oEDB8KnP/3psGXLltDQ0BDa29vD1q1bw5e//OUwNzeXaN2TPlcUReGee+4JAwMDobOzM9x9991hZmYm0Trj7PajH/0o/NEf/VHYsWNH6O/vDzU1NaGxsTFs3rw5fPSjHw2PP/54wceir2AtO3bsWPjWt74VPv/5z4f3vOc9Yd26dSGTyYRMJhM+8pGPFHUs+grWsnK1b9o20oi5gr6EwvAOQl+BjX2t19FPEhbhjHv44YejEMKq/1u3bl300EMPmcd64IEHoubmZnmMzZs3R/v27Uuk3qU411//9V9HnZ2d0de//vVo165d0RVXXBF9+MMfTqS+OPtde+21BfWVO++8M1pcXDSPRV/BWmf1kbvuuqvg49BXsJaVq33TtpFWzBX0JayOd5DX0VdgYV/rdfSTZLFpnQIPP/xwtGHDhujOO++M/uIv/iL6xje+ET3xxBPR7t27o507d0Yf+MAHosrKyiiEEFVXV0fPPvts7HGefvrpqK6uLgohRI2NjdEf//EfR3v27IkeeeSR6Dd/8zd/odNNT0+fVp1Lda63v/3t0b333nvy/z/11FNRZWVlNDc3d1r1xdqwadOmKIQQ9fb2Rp/85Cejr3/969HevXujJ554Irr33nujvr6+k23PmhjoKzgX/Pxia+PGjdGOHTuK3oigr2AtK1f7pm0jzZgr6EtYHe8gr6OvwMK+1uvoJ8li0zoFVlZWVv0z3/zmN092mFtvvTX2z7zxN8DZbDbas2fPKfF77rnn5DG+8IUvnFadS3WurVu3Rn/5l3958v8/99xzUUVFRXTixInTqi/WhptvvjnauXOn7DOjo6PR5s2bT7a9Xbt2xf45+grOBZ///OejBx98MDp69GgURVG0f//+ojci6CtYy8rVvmnbSDPmCvoSVsc7yOvoK7Cwr/U6+kmy2LQ+i1x44YUn/3WK/+uHP/zhyc509913x+bncrnooosuikIIUWtra7S0tOSqRynP9eUvfznq7u6OvvnNb0aPPfZYdPXVV0e33Xabq544Nz344IMn2+fv/M7vnBKnr+BcVexGBH0Fa1m52jdtG2ebc3GuoC8hCefCOwh9BUlY6/ta9JNk8SHGs0hTU1MIIYSFhYVTYv/xH/9x8p8/+tGPxuZXVFSEO++8M4QQwuTkZHj00Udd9SjluT71qU+F3/qt3wqf+MQnwi233BIuvvji8I//+I+ueuLcdMMNN5z855/+9KenxOkrQGHoK1jLytW+adtY69bCXEFfQhLOhXcQ+gqSsNb3tegnyWLT+izxyiuvhGeffTaEEMKWLVtOib/xteKGhoZw5ZVXyuNs37795D/v3r3bVZdSnquysjL84R/+YRgaGgrj4+PhK1/5SmhtbXXVE+emxcXFk/9cWVl5Spy+AhSGvoK1rFztm7aNtW4tzBX0JSThXHgHoa/gdJ0L+1r0k2SxaZ1ic3NzYd++feHee+8N27dvDysrKyGEEH73d3/3lD/7k5/8JIQQwgUXXBCy2aw85s8PDG/kFKuc5wKKtWvXrpP/fNFFF50Sp68AhaGvYC0rV5ujbWOtY64AXsc7CBCPfS2cDv1kcEZ87Wtfk/9qQgghfPaznw133HHHL5QtLCyEsbGxEEII/f395vHb2tpCQ0NDmJ2dDYcOHSq6fuU8F1CsfD4fvvjFL578/x/84Ad/IU5fAQpDX8FaVq42R9vGWsdcAbyOdxDgF7GvhaTwS+uzxGWXXRb27t0b/uRP/iRkMplfiM3MzJz858bGxlWP1dDQEEII4cSJE0XXo5znAor1Z3/2Z2Hv3r0hhBBuu+22U/41H/oKUBj6CtaycrU52jbWOuYK4HW8gwCFYV8LxWLTOmXe//73h+effz48//zzYe/eveFf//Vfw6233hqeffbZ8OEPfzh861vfOiXn5/8D9tXV1aueo6amJoQQwvz8fNH1K+e5gGLs2rUrfPaznw0hhLB+/frwt3/7t6f8GfoKUBj6CtaycrU52jbWOuYKgHcQIA77WkgKm9ZFyGQyp/2/r33ta+Y5Wltbw6WXXhouvfTSsHXr1vCrv/qr4Rvf+Eb4p3/6p/Daa6+FW2655ZRj1NbWnvznpaWlVa/jjY9E1NXVFX0PynkunL3K0Vd+3osvvhhuvfXWsLKyEmpra8O//du/hfXr15/y5+grSJty95VC0VewlpWrzdG2sdYxV+BcxzsIEI99LSSFTeuzxK/92q+FD3zgAyGfz4dPfOIT4fjx4ydjTU1NJ/+5kH9dYXZ2NoRQ2L8G8X+V81xAIfbv3x927NgRJiYmQmVlZbjvvvvCddddF/tn6StAYegrWMvK1eZo21jrmCtwLuMdBCge+1ooFh9iLEISXwrt6elx595yyy3h/vvvD7Ozs+Ghhx46+R+ur62tDR0dHWF8fDwMDQ2Zx5iYmDjZ4TZs2FB0Hcp5Lpy9ytVXhoeHw0033RSGh4dDJpMJX/nKV8Itt9wi/zx9BWlzpucVhb6CtaxcbY62jbWOuQLnKt5BAD/2tVAMNq2LsGXLljN6/s7OzpP/fODAgV+IXXzxxeGxxx4Lr776alhZWQnZbPyjffnll0/+80UXXeSqRznPhbNTOfrK2NhYeNe73hVee+21EEIIf/VXfxXuvPPOVfPoK0iTMz2vWOgrWMvK1eZo21jrmCtwruEdBDg97GuhGPznQc4ihw8fPvnP//dfS3jnO98ZQnj9X1t46qmn5DF27dp18p+3bdvmqkc5zwXEmZqaCu9+97vDSy+9FEII4Ytf/GL4+Mc/XlAufQUoDH0Fa1m52hxtG2sdcwXOJbyDAKePfS0UJcJZ45d/+ZejEEIUQogeffTRX4j98Ic/PBm7++67Y/NzuVx00UUXRSGEqLW1NVpaWnLVo5znAv6v2dnZaNu2bSfb4O///u8XlU9fwblq//79J9vjXXfdteqfp69gLStXm6Nt42zDXAHE4x0ESAb7WigGm9Yp8NWvfjWan583/8y99957skOdd9550crKyil/5tprr41CCFE2m4327NlzSvyee+45eYwvfOEL8lxv/JmBgQH5Z5I6F1CMxcXFaMeOHSfb1ic/+UnXcegrOBcVuxERRfQVrG1JtDnaNtYa5grgVLyDAKtjXwulkImiKAo4o970pjeFmZmZcPvtt4d3vvOdYdOmTaGxsTHMzMyE559/PvzLv/xL2L17dwghhOrq6vDtb3873HTTTacc55lnngnbtm0L8/PzobGxMXzuc58LN9xwQ5ifnw/33Xdf+Pu///sQQgibN28OP/rRj37hi6k/L5PJhBBCGBgYCIODg7F/JqlzAcW4/fbbwze+8Y0QQgg33nhj+PM///OT7TVOdXV12Lx58ynl9BWcCx5//PHw6quvnvz/Y2Nj4fd+7/dCCK//q20f+9jHfuHPf+QjHznlGPQVrGVJtDnaNs52zBXA6ngHAVbHvhZK4kzvmiOKBgYGTv7tjfW//v7+6Lvf/a55rAceeCBqbm6Wx9i8eXO0b98+8xihgL+RSupcQDEK6Sc//z+rDdNXsNbdddddRfUXhb6Ctex02xxtG2c75gpgdbyDAKtjXwulwKZ1Crz88svRn/7pn0a33XZb9Na3vjXq6uqKstls1NTUFG3atCm6/fbbo69+9avR7OxsQccbHByMPvWpT0WbN2+O6uvro9bW1uiqq66KvvSlLxV0jEI7dxLnAoqR5IIxiugrWNuS2oiIIvoK1rbTaXO0bZztmCuA1fEOAqyOfS2UAv95EAAAAAAAAABAalSc6QoAAAAAAAAAAPAGNq0BAAAAAAAAAKnBpjUAAAAAAAAAIDXYtAYAAAAAAAAApAab1gAAAAAAAACA1GDTGgAAAAAAAACQGmxaAwAAAAAAAABSg01rAAAAAAAAAEBqsGkNAAAAAAAAAEgNNq0BAAAAAAAAAKnBpjUAAAAAAAAAIDXYtAYAAAAAAAAApAab1gAAAAAAAACA1GDTGgAAAAAAAACQGmxaAwAAAAAAAABS4/8BOU2+tt0OD4UAAAAASUVORK5CYII=",
      "text/plain": [
       "<Figure size 1850x1050 with 1 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "image_polytopes, labels = rotation_dataset.load(1)\n",
    "print(f\"image_polytopes {tuple(image_polytopes.shape)}: {image_polytopes.shape[0]} polytope(s) of {image_polytopes.shape[1]} vertices.\")\n",
    "print(\"Expected labels:\", labels.flatten().long())\n",
    "print(\"Prediction after repair:\", repaired_model(image_polytopes[0].to(device,dtype)).argmax(-1).cpu())\n",
    "mnist.imshow(image_polytopes, degs=rotation_dataset.degs)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Evaluate accuracy of the  repaired model"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "                                                                 "
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "APRNN Drawdown: 95.08% -> 95.23% (-0.15%).\n"
     ]
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "\r"
     ]
    }
   ],
   "source": [
    "testset = mnist.datasets.Dataset('identity', 'test').reshape(784).to(device,dtype)\n",
    "\n",
    "original_model = mnist.model('9x100').to(device,dtype).eval()\n",
    "acc0 = testset.accuracy(original_model)\n",
    "acc1 = testset.accuracy(repaired_model)\n",
    "drawdown = acc0 - acc1\n",
    "print(f\"APRNN Drawdown: {acc0:.2%} -> {acc1:.2%} ({'+' if drawdown > 0 else ''}{drawdown:.2%}).\")\n"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "pldi24-tutorial",
   "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.9.18"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}