dfa_from_rnn_notebook_for_several_rnns.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Welcome!\n",
    "\n",
    "This is another notebook demonstration the extraction method from our [ICML 2018 paper](https://arxiv.org/abs/1711.09576), only with a little extra functionality to help you keep track of multiple networks, and without documentation."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "from LSTM import LSTMNetwork\n",
    "from GRU import GRUNetwork\n",
    "from RNNClassifier import RNNClassifier\n",
    "from Training_Functions import mixed_curriculum_train\n",
    "from Tomita_Grammars import tomita_1, tomita_2, tomita_3, tomita_4, tomita_5, tomita_6, tomita_7\n",
    "from Training_Functions import make_train_set_for_target\n",
    "from Extraction import extract"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "try:\n",
    "    None == all_my_rnns\n",
    "except NameError:\n",
    "    all_my_rnns = []\n",
    "    \n",
    "class Wrapper:\n",
    "    def __init__(self,rnn,alphabet,target,name,train_set):\n",
    "        self.rnn = rnn\n",
    "        self.alphabet = alphabet\n",
    "        self.target = target\n",
    "        self.name = name\n",
    "        words = sorted(list(train_set.keys()),key=lambda x:len(x))\n",
    "        short_pos = next((w for w in words if target(w)==True),None)\n",
    "        short_neg = next((w for w in words if target(w)==False),None)\n",
    "        self.starting_examples = [w for w in [short_pos,short_neg] if not None==w]\n",
    "        self.train_set = train_set\n",
    "        self.dfas = []\n",
    "    def __repr__(self):\n",
    "        return self.name"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "made train set of size: 2731 , of which positive examples: 1308\n"
     ]
    }
   ],
   "source": [
    "alphabet = \"01\"\n",
    "target = tomita_3\n",
    "name = \"my Tomita 3 RNN\"\n",
    "\n",
    "# alternative option (example):\n",
    "# def target(w):\n",
    "#     if len(w)==0:\n",
    "#         return True\n",
    "#     return w[0]==w[-1]\n",
    "# alphabet = \"abc\"\n",
    "# name = \"start and end same over abc\"\n",
    "\n",
    "\n",
    "rnn = RNNClassifier(alphabet,num_layers=1,hidden_dim=10,RNNClass = LSTMNetwork)\n",
    "\n",
    "\n",
    "train_set = make_train_set_for_target(target,alphabet)\n",
    "wrapper = Wrapper(rnn,alphabet,target,name,train_set)\n",
    "all_my_rnns.append(wrapper)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "scrolled": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "current average loss is:  0.0054309656350380875\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAXcAAAD8CAYAAACMwORRAAAABHNCSVQICAgIfAhkiAAAAAlwSFlz\nAAALEgAACxIB0t1+/AAAIABJREFUeJzt3Xt0FfXd7/H31xhqvCyxmlaugh4KBZKABCjyKCIIKFUu\nXgpVl7CeFm94OW1TwfuxtaL41NYuW4o9iLeKwkGkB7rwaRFRq5ZwUW4HjYiSjUpAQ0WCJuF7/tg7\n6U4I2ZNkh7338HmtlcWemV9mfzPsfGbym9/MmLsjIiLhclSqCxARkeRTuIuIhJDCXUQkhBTuIiIh\npHAXEQkhhbuISAgp3EVEQkjhLiISQgp3EZEQOjpVb3zKKad4ly5dUvX2IiIZafXq1bvcPTdRu5SF\ne5cuXSguLk7V24uIZCQz+zBIO3XLiIiEkMJdRCSEFO4iIiGUsj53CbfKykpKS0vZv39/qksRyUjH\nHHMMHTt2JDs7u1nfr3CXVlFaWsoJJ5xAly5dMLNUlyOSUdyd3bt3U1paSteuXZu1jkDdMmY2ysy2\nmFmJmU1rYPnDZrYu9vWumZU3qxoJjf3793PyyScr2EWawcw4+eSTW/SXb8IjdzPLAh4FzgdKgVVm\nttjdN9W0cff/Gdf+RqBvsyuS0FCwizRfS39/ghy5DwBK3H2ru38NzAPGNNJ+IvBsi6oSEZEWCRLu\nHYDtcdOlsXkHMbPTgK7A8paXJpJ899xzDw899FDS1nfWWWfVvi4qKqJXr14UFRUxa9YsnnzyySav\nr7y8nN///ve10zt27ODSSy9NSq3nnntuq104OHHiRPLz83n44Yeb9f0rVqzgH//4R+30pEmTWLBg\nQbLKS6nW3O6NSfYJ1QnAAnevbmihmU0BpgB07ty5yStftDbCzGVb2FFeQfu2ORSN7M7Yvg3uZ0QO\ni/hAmj17Np999hlZWVnNXl9NuF9//fUAtG/fPu1D7pNPPmHVqlWUlJQE/p6qqiqOPvrf8bNixQqO\nP/74OjtLaZkgR+4RoFPcdMfYvIZMoJEuGXef7e6F7l6Ym5vw1gh1LFobYfrC9UTKK3AgUl7B9IXr\nWbT2UKVIJlm0NsLgGcvpOm0Jg2csT8r/65NPPkl+fj4FBQVcddVVBy1/7LHH6N+/PwUFBVxyySXs\n27cPgPnz59O7d28KCgo455xzANi4cSMDBgygT58+5Ofn89577wFw/PHHA3DxxRezd+9e+vXrx3PP\nPVfnL4SSkhKGDx9OQUEBZ555Ju+//z579+5l2LBhnHnmmeTl5fHiiy8CMG3aNN5//3369OlDUVER\n27Zto3fv3kD0JPXkyZPJy8ujb9++vPzyywDMnTuX8ePHM2rUKLp168bPf/7zhNvm2WefJS8vj969\ne3PrrbcCUF1dzaRJk+jduzd5eXm1R+GPPPIIPXv2JD8/nwkTJhy0rhEjRhCJROjTpw+vvvoq69at\n43vf+x75+fmMGzeOzz//HIgewd5yyy0UFhby29/+tvb7t23bxqxZs3j44Ydr1wGwcuVKzjrrLE4/\n/fQ6O7iZM2fSv39/8vPzufvuuwH48ssvGT16NAUFBfTu3ZvnnnsOgNWrVzNkyBD69evHyJEj+fjj\njw+qv6ysjEsuuYT+/fvTv39/Xn/9dSD6V95VV13FoEGD6NatG4899hgQHclSVFRUu51q3gvggQce\nIC8vj4KCAqZN+/fYk/nz5zNgwAC+853v1P58h/pMJY27N/pF9Oh+K9HuljbA20CvBtr1ALYBlmid\n7k6/fv28Kc66/+9+2q3/96Cvs+7/e5PWI4fHpk2bArd9YU2p97jjr3X+X3vc8Vd/YU1ps99/w4YN\n3q1bNy8rK3N39927d7u7+9133+0zZ850d/ddu3bVtr/99tv9kUcecXf33r17e2lp9L0///xzd3ef\nOnWqP/300+7u/tVXX/m+ffvc3f24446rXUf86/j3GTBggC9cuNDd3SsqKvzLL7/0yspK37Nnj7u7\nl5WV+RlnnOEHDhzwDz74wHv16lW7nvjphx56yCdPnuzu7ps3b/ZOnTp5RUWFP/744961a1cvLy/3\niooK79y5s3/00UcHbZMhQ4b4qlWrPBKJeKdOnXznzp1eWVnpQ4cO9RdeeMGLi4t9+PDhte1rfvZ2\n7dr5/v3768yLV7/mvLw8X7Fihbu733nnnX7zzTfXvv9111130PfX317u7ldffbVfeumlXl1d7Rs3\nbvQzzjjD3d2XLVvmP/7xj/3AgQNeXV3to0eP9ldeecUXLFjgP/rRj2q/v7y83L/++msfNGiQ79y5\n093d582bV7v94k2cONFfffVVd3f/8MMPvUePHrU15efn+759+7ysrMw7duzokUjEFyxY4MOHD/eq\nqir/5JNPvFOnTr5jxw5funSpDxo0yL/88kt3//dnbsiQIf6Tn/zE3d2XLFniw4YNc/dDf6biNfR7\nBBR7gIxN2C3j7lVmNhVYBmQBc9x9o5ndG3uTxbGmE4B5sTdPuh3lFYHmq+sm88xctoWKyro9eRWV\n1cxctqXZ/3fLly/nsssu45RTTgHgm9/85kFtNmzYwB133EF5eTl79+5l5MiRAAwePJhJkyZx+eWX\nM378eAAGDRrEfffdR2lpKePHj6dbt26B6vjiiy+IRCKMGzcOiF6YAtGLvG677TZWrlzJUUcdRSQS\n4dNPP210Xa+99ho33ngjAD169OC0007j3XffBWDYsGGceOKJAPTs2ZMPP/yQTp06NbieVatWce65\n51Lz1/MVV1zBypUrufPOO9m6dSs33ngjo0ePZsSIEQDk5+dzxRVXMHbsWMaOHdtojXv27KG8vJwh\nQ4YAcPXVV3PZZZfVLv/BD37Q6PfHGzt2LEcddRQ9e/as3TYvvfQSL730En37Rgfk7d27l/fee4+z\nzz6bn/70p9x66618//vf5+yzz2bDhg1s2LCB888/H4j+ZdKuXbuD3udvf/sbmzbVDv7jX//6F3v3\n7gVgzJgx5OTkkJOTw9ChQ/nnP//Ja6+9xsSJE8nKyuLb3/42Q4YMYdWqVbzyyitMnjyZY489Fqj7\nmav5HPXr149t27YBzf9MBRWoz93dlwJL6827q970Pckr62Dt2+YQaSDg27fNqX1d03VTExQ1XTeA\nAj6NBd1xJ9ukSZNYtGgRBQUFzJ07lxUrVgAwa9Ys3nrrLZYsWUK/fv1YvXo1P/zhDxk4cCBLlizh\nwgsv5I9//CPnnXdes9/7mWeeoaysjNWrV5OdnU2XLl1aNKb5G9/4Ru3rrKwsqqqqmryOk046ibff\nfptly5Yxa9Ysnn/+eebMmcOSJUtYuXIlf/nLX7jvvvtYv359nf7ypjjuuOMCt43/mWqOGd2d6dOn\nc8011xzUfs2aNSxdupQ77riDYcOGMW7cOHr16sUbb7zR6PscOHCAN998s3bHG6/+cMTmDk+s+Vni\n/2+S/ZmqL2PuLVM0sjs52XVPVOVkZ1E0snvtdGNHgJK+4nfQQeYHcd555zF//nx2794NwGeffXZQ\nmy+++IJ27dpRWVnJM888Uzv//fffZ+DAgdx7773k5uayfft2tm7dyumnn85NN93EmDFjeOeddwLV\nccIJJ9CxY0cWLVoEwFdffcW+ffvYs2cP3/rWt8jOzubll1/mww8/rG3/xRdfNLius88+u7bOd999\nl48++oju3bs32LYxAwYM4JVXXmHXrl1UV1fz7LPPMmTIEHbt2sWBAwe45JJL+OUvf8maNWs4cOAA\n27dvZ+jQoTzwwAPs2bOn9qi2ISeeeCInnXRSbb/yU089VXsU35jGfu54I0eOZM6cObU1RCIRdu7c\nyY4dOzj22GO58sorKSoqYs2aNXTv3p2ysrLacK+srGTjxo0HrXPEiBH87ne/q51et25d7esXX3yR\n/fv3s3v3blasWEH//v05++yzee6556iurqasrIyVK1cyYMAAzj//fB5//PHaczcNfebiNfczFVTG\n3H6g5si7sS6XVB0BSssUjexe5y8uOHjH3VS9evXi9ttvZ8iQIWRlZdG3b1/mzp1bp80vfvELBg4c\nSG5uLgMHDqwNl6KiIt577z3cnWHDhlFQUMADDzzAU089RXZ2Nqeeeiq33XZb4FqeeuoprrnmGu66\n6y6ys7OZP38+V1xxBRdddBF5eXkUFhbSo0cPAE4++WQGDx5M7969ueCCC7jhhhtq13P99ddz3XXX\nkZeXx9FHH83cuXPrHN0G1a5dO2bMmMHQoUNxd0aPHs2YMWN4++23mTx5MgcOHADg/vvvp7q6miuv\nvJI9e/bg7tx00020bdu20fU/8cQTXHvttezbt4/TTz+dxx9/PGFNF110EZdeeikvvvhinaCtb8SI\nEWzevJlBgwYB0RPaTz/9NCUlJRQVFXHUUUeRnZ3NH/7wB9q0acOCBQu46aab2LNnD1VVVdxyyy30\n6tWrzjofeeQRbrjhBvLz86mqquKcc85h1qxZQLRLaujQoezatYs777yT9u3bM27cON544w0KCgow\nMx588EFOPfVURo0axbp16ygsLKRNmzZceOGF/OpXvzrkz/L88883+zMVhLVSF3lChYWFnuyxn4Nn\nLG+w66ZD2xxen5a8P3cksc2bN/Pd7343cHudK5F0c88993D88cfzs5/9LGU1NPR7ZGar3b0w0fdm\nzJF7EEGOABUi6Wls3w76fxBJolCFe6KuG51wFZGg7rnnnlSX0CKhCndo/AiwNYbcyaG5u24eJtJM\nLe0yz5jRMsmgE66HzzHHHMPu3btb/AEVORJ57H7uDQ3PDCp0R+6NCTJWXpKjY8eOlJaWUlZWlupS\nRDJSzZOYmuuICvfWGHInDcvOzm72E2REpOWOqHAPMlZeRCQMjqhwBw25E5EjwxF1QlVE5EihcBcR\nCSGFu4hICCncRURCSOEuIhJCCncRkRBSuIuIhJDCXUQkhAKFu5mNMrMtZlZiZtMO0eZyM9tkZhvN\n7M/JLfPwWbQ2wuAZy+k6bQmDZyxn0dpIqksSEWmyhFeomlkW8ChwPlAKrDKzxe6+Ka5NN2A6MNjd\nPzezb7VWwa1J93sXkbAIcuQ+AChx963u/jUwDxhTr82PgUfd/XMAd9+Z3DIPDz1gW0TCIki4dwC2\nx02XxubF+w7wHTN73czeNLNRDa3IzKaYWbGZFafjrWB1v3cRCYtknVA9GugGnAtMBB4zs4Meke7u\ns9290N0Lc3Nzk/TWyXOo+7rrfu8ikmmChHsE6BQ33TE2L14psNjdK939A+BdomGfUYpGdicnO6vO\nPN3vXUQyUZBwXwV0M7OuZtYGmAAsrtdmEdGjdszsFKLdNFuTWOdhMbZvB+4fn0eHtjkY0KFtDveP\nz9PJVBHJOAlHy7h7lZlNBZYBWcAcd99oZvcCxe6+OLZshJltAqqBInff3ZqFtxbd711EwsBS9QDj\nwsJCLy4uTsl7i4hkKjNb7e6FidrpClURkRBSuIuIhJDCXUQkhBTuIiIhpHAXEQkhhbuISAgp3EVE\nQkjhLiISQgp3EZEQUriLiISQwl1EJIQU7iIiIaRwFxEJIYW7iEgIKdxFREJI4S4iEkIKdxGREFK4\ni4iEUKBwN7NRZrbFzErMbFoDyyeZWZmZrYt9/Sj5pYqISFAJH5BtZlnAo8D5QCmwyswWu/umek2f\nc/eprVCjiIg0UZAj9wFAibtvdfevgXnAmNYtS0REWiJIuHcAtsdNl8bm1XeJmb1jZgvMrFNSqhMR\nkWZJ2C0T0F+AZ939KzO7BngCOK9+IzObAkwB6Ny5c5Le+vBatDbCzGVb2FFeQfu2ORSN7M7Yvg3t\n60REUifIkXsEiD8S7xibV8vdd7v7V7HJPwH9GlqRu89290J3L8zNzW1OvSm1aG2E6QvXEymvwIFI\neQXTF65n0dpIwu8VETmcgoT7KqCbmXU1szbABGBxfAMzaxc3eTGwOXklpo+Zy7ZQUVldZ15FZTUz\nl21JUUUiIg1L2C3j7lVmNhVYBmQBc9x9o5ndCxS7+2LgJjO7GKgCPgMmtWLNKbOjvKJJ80VEUiVQ\nn7u7LwWW1pt3V9zr6cD05JaWftq3zSHSQJC3b5uTgmpERA5NV6g2QdHI7uRkZ9WZl5OdRdHI7imq\nSESkYckaLXNEqBkVo9EyIpLuFO5NNLZvB4W5iKQ9dcuIiISQwl1EJIQU7iIiIaRwFxEJIYW7iEgI\nKdxFREJI4S4iEkIKdxGREFK4i4iEkMJdRCSEFO4iIiGkcBcRCSGFu4hICCncRURCSOEuIhJCCncR\nkRAKFO5mNsrMtphZiZlNa6TdJWbmZlaYvBJFRKSpEoa7mWUBjwIXAD2BiWbWs4F2JwA3A28lu0gR\nEWmaIEfuA4ASd9/q7l8D84AxDbT7BfAAsD+J9YmISDMECfcOwPa46dLYvFpmdibQyd2XJLE2ERFp\nphafUDWzo4BfAz8N0HaKmRWbWXFZWVlL31pERA4hSLhHgE5x0x1j82qcAPQGVpjZNuB7wOKGTqq6\n+2x3L3T3wtzc3OZXLSIijQoS7quAbmbW1czaABOAxTUL3X2Pu5/i7l3cvQvwJnCxuxe3SsUiIpJQ\nwnB39ypgKrAM2Aw87+4bzexeM7u4tQsUEZGmOzpII3dfCiytN++uQ7Q9t+VliYhIS+gKVRGREFK4\ni4iEkMJdRCSEFO4iIiGkcBcRCSGFu4hICCncRURCSOEuIhJCgS5ikuAWrY0wc9kWdpRX0L5tDkUj\nuzO2b4fE3ygikkQK9yRatDbC9IXrqaisBiBSXsH0hesBFPAiclipWyaJZi7bUhvsNSoqq5m5bEuK\nKhKRI5XCPYl2lFc0ab6ISGtRuCdR+7Y5TZovItJaFO5JVDSyOznZWXXm5WRnUTSye4oqEpEjlU6o\nJlHNSVONlhGRVFO4J9nYvh0U5iKScuqWEREJIYW7iEgIKdxFREIoULib2Sgz22JmJWY2rYHl15rZ\nejNbZ2avmVnP5JcqIiJBJQx3M8sCHgUuAHoCExsI7z+7e5679wEeBH6d9EpFRCSwIEfuA4ASd9/q\n7l8D84Ax8Q3c/V9xk8cBnrwSRUSkqYIMhewAbI+bLgUG1m9kZjcAPwHaAOc1tCIzmwJMAejcuXNT\naxURkYCSdkLV3R919zOAW4E7DtFmtrsXunthbm5ust5aRETqCRLuEaBT3HTH2LxDmQeMbUlRIiLS\nMkHCfRXQzcy6mlkbYAKwOL6BmXWLmxwNvJe8EkVEpKkS9rm7e5WZTQWWAVnAHHffaGb3AsXuvhiY\nambDgUrgc+Dq1ixaREQaF+jeMu6+FFhab95dca9vTnJdIiLSArpCVUQkhBTuIiIhpHAXEQkhhbuI\nSAgp3EVEQkhPYkqBRWsjehSfiLQqhfthtmhthOkL11NRWQ1ApLyC6QvXAyjgRSRp1C1zmM1ctqU2\n2GtUVFYzc9mWFFUkImGkcD/MdpRXNGm+iEhzKNwPs/Ztc5o0X0SkORTuh1nRyO7kZGfVmZeTnUXR\nyO4pqkhEwkgnVA+zmpOmGi0jIq1J4Z4CY/t2UJiLSKtSt4yISAgp3EVEQkjhLiISQgp3EZEQUriL\niIRQoHA3s1FmtsXMSsxsWgPLf2Jmm8zsHTP7u5mdlvxSRUQkqIThbmZZwKPABUBPYKKZ9azXbC1Q\n6O75wALgwWQXKiIiwQU5ch8AlLj7Vnf/GpgHjIlv4O4vu/u+2OSbQMfklikiIk0RJNw7ANvjpktj\n8w7lP4G/tqQoERFpmaReoWpmVwKFwJBDLJ8CTAHo3LlzMt9aRETiBDlyjwCd4qY7xubVYWbDgduB\ni939q4ZW5O6z3b3Q3Qtzc3ObU6+IiAQQ5Mh9FdDNzLoSDfUJwA/jG5hZX+CPwCh335n0Ko8wegyf\niLRUwnB39yozmwosA7KAOe6+0czuBYrdfTEwEzgemG9mAB+5+8WtWHdo6TF8IpIMgfrc3X0psLTe\nvLviXg9Pcl1HrMYew6dwF5GgdIVqmtFj+EQkGRTuaUaP4RORZFC4pxk9hk9EkkFPYkozegyfiCSD\nwj0N6TF8ItJS6pYREQkhhbuISAgp3EVEQkjhLiISQgp3EZEQUriLiISQwl1EJIQ0zj0D6ZbAIpKI\nwj3D6JbAIhKEumUyTGO3BBYRqaFwzzC6JbCIBKFwzzC6JbCIBKFwzzC6JbCIBKETqhlGtwQWkSAC\nhbuZjQJ+S/QB2X9y9xn1lp8D/AbIBya4+4JkFyr/plsCi0giCbtlzCwLeBS4AOgJTDSznvWafQRM\nAv6c7AJFRKTpghy5DwBK3H0rgJnNA8YAm2oauPu22LIDrVCjiIg0UZBw7wBsj5suBQa2TjmSDLqC\nVUQO6wlVM5sCTAHo3Lnz4XzrI4auYBURCDYUMgJ0ipvuGJvXZO4+290L3b0wNze3OauQBHQFq4hA\nsHBfBXQzs65m1gaYACxu3bKkuXQFq4hAgHB39ypgKrAM2Aw87+4bzexeM7sYwMz6m1kpcBnwRzPb\n2JpFy6HpClYRgYB97u6+FFhab95dca9XEe2ukRQrGtm9Tp876ApWkSORrlANGV3BKiKgcA+lIFew\narikSLgp3I9AGi4pEn66K+QRSMMlRcJP4X4E0nBJkfBTuB+BNFxSJPwU7kcgPfBDJPx0QvUIFGS4\npEbTiGQ2hfsRqrHhkhpNI5L51C0jB9FoGpHMp3CXg2g0jUjmU7eMHKR92xwiDQR5/Gga9cmLpDcd\nuctBEo2mqemTj5RX4Py7T37R2mbd5l9EWoGO3OUgiUbTNNYnX9NGR/YiqaVwlwY1NpomUZ+8RtuI\npJ66ZaTJEl3hGmS0zaK1EQbPWE7XaUsYPGO5unREkkxH7tJkiR4Ikqwj+0RdO+r6ETk0hbs0WaI+\n+USjbYL22Te2Awiyg9DOQY5kCndplsb65Ft6ZA+JdwCJlidj5wAt30G09nKRQwkU7mY2CvgtkAX8\nyd1n1Fv+DeBJoB+wG/iBu29LbqmSKVp6ZA+JdwCJlrd05wAt/+uhtZfXSIcdTKpryIQag7ZJloQn\nVM0sC3gUuADoCUw0s571mv0n8Lm7/w/gYeCBZBcqmWVs3w68Pu08PpgxmtennVfnAxzkrpSJTtom\nWt7SnQMkPjGc6uWQ+JqD1l6eDjVkQo1B2yRTkNEyA4ASd9/q7l8D84Ax9dqMAZ6IvV4ADDMzS16Z\nEiZj+3bg/vF5dGibgwEd2uZw//i8Ju0AEi1v6c4BWr6DaO3lkB47mFTXkAk1Bm2TTEHCvQOwPW66\nNDavwTbuXgXsAU6uvyIzm2JmxWZWXFZW1ryKJRQaO7KvWd7YDiDR8pbuHKDlO4jWXg7psYNJdQ2Z\nUGPQNsl0WMe5u/tsdy9098Lc3NzD+daSgYLsAA61vKU7B2j5DqK1l0N67GBSXUMm1Bi0TTIFCfcI\n0CluumNsXoNtzOxo4ESiJ1ZFUqYlO4ea5S3ZQbT2ckiPHUyqa8iEGoO2SSZz98YbRMP6XWAY0RBf\nBfzQ3TfGtbkByHP3a81sAjDe3S9vbL2FhYVeXFzc0vpFjniZMAok1cszpYYgzGy1uxcmbJco3GMr\nuxD4DdGhkHPc/T4zuxcodvfFZnYM8BTQF/gMmODuWxtbp8JdRKTpgoZ7oHHu7r4UWFpv3l1xr/cD\nlzW1SBERaR26cZiISAgp3EVEQkjhLiISQgp3EZEQUriLiISQwl1EJIQU7iIiIaRwFxEJoUBXqLbK\nG5uVAR8289tPAXYlsZzWkAk1QmbUqRqTQzUmR6prPM3dE955MWXh3hJmVhzk8ttUyoQaITPqVI3J\noRqTIxNqBHXLiIiEksJdRCSEMjXcZ6e6gAAyoUbIjDpVY3KoxuTIhBozs89dREQal6lH7iIi0oiM\nC3czG2VmW8ysxMympbqehpjZNjNbb2brzCwtnkhiZnPMbKeZbYib900z+28zey/270lpWOM9ZhaJ\nbct1sQfHpLLGTmb2spltMrONZnZzbH7abMtGaky3bXmMmf3TzN6O1fm/YvO7mtlbsd/x58ysTRrW\nONfMPojbln1SVeMhuXvGfBF9EtT7wOlAG+BtoGeq62qgzm3AKamuo15N5wBnAhvi5j0ITIu9ngY8\nkIY13gP8LNXbL66edsCZsdcnEH0EZc902paN1Jhu29KA42Ovs4G3gO8BzxN9mhvALOC6NKxxLnBp\nqrdhY1+ZduQ+AChx963u/jUwDxiT4poygruvJPoIxHhjgCdir58Axh7Wouo5RI1pxd0/dvc1sddf\nAJuBDqTRtmykxrTiUXtjk9mxLwfOAxbE5qd6Wx6qxrSXaeHeAdgeN11KGn5oif7nv2Rmq81sSqqL\nacS33f3j2OtPgG+nsphGTDWzd2LdNintOopnZl2IPjf4LdJ0W9arEdJsW5pZlpmtA3YC/030L/Ny\nd6+KNUn573j9Gt29ZlveF9uWD5vZN1JYYoMyLdwzxX+4+5nABcANZnZOqgtKxKN/d6bjEckfgDOA\nPsDHwH+ltpwoMzse+D/ALe7+r/hl6bItG6gx7balu1e7ex+gI9G/zHukuKSD1K/RzHoD04nW2h/4\nJnBrCktsUKaFewToFDfdMTYvrbh7JPbvTuAFoh/adPSpmbUDiP27M8X1HMTdP439ch0AHiMNtqWZ\nZRMNzWfcfWFsdlpty4ZqTMdtWcPdy4GXgUFAWzM7OrYobX7H42ocFev6cnf/CnicNNqWNTIt3FcB\n3WJn09sAE4DFKa6pDjM7zsxOqHkNjAA2NP5dKbMYuDr2+mrgxRTW0qCawIwZR4q3pZkZ8L+Bze7+\n67hFabMtD1VjGm7LXDNrG3udA5xP9PzAy8ClsWap3pYN1fj/4nbkRvScQNr9jmfcRUyx4Vu/ITpy\nZo6735fikuows9OJHq0DHA38OR1qNLNngXOJ3tHuU+BuYBHRkQmdid6h83J3T9kJzUPUeC7RbgQn\nOgrpmri+7cPOzP4DeBVYDxyIzb6NaJ92WmzLRmqcSHpty3yiJ0yziB5oPu/u98Z+h+YR7e5YC1wZ\nO0JOpxqXA7lER9OsA66NO/GaFjIu3EVEJLFM65YREZEAFO4iIiGkcBcRCSGFu4hICCncRURCSOEu\nIhJCCne9ZP+XAAAAD0lEQVQRkRBSuIuIhND/B0odaJkXKFNVAAAAAElFTkSuQmCC\n",
      "text/plain": [
       "<matplotlib.figure.Figure at 0x1311137b8>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAXcAAAD8CAYAAACMwORRAAAABHNCSVQICAgIfAhkiAAAAAlwSFlz\nAAALEgAACxIB0t1+/AAAHqxJREFUeJzt3X10VPW97/H31xAhKoIi7cIAgr0cKOQRAlq5lqgo1HqF\nqj2i0BZvvfSuVq19SIv1rKNVl+LFddraB596WotyFe1Byq22eG6hj+u0JQpVHg4WECXRVkDCRRMw\nhO/9Y2biECbJnqfM7J3Pay0WmZ2dPb89O/nMb377t7/b3B0REYmWEwrdABERyT2Fu4hIBCncRUQi\nSOEuIhJBCncRkQhSuIuIRJDCXUQkghTuIiIRpHAXEYmgAYV64jPOOMPHjBlTqKcXEQmlF154Ya+7\nD+9tvYKF+5gxY2hsbCzU04uIhJKZvRZkPQ3LiIhEkMJdRCSCFO4iIhFUsDF3EYD29naampo4dOhQ\noZsiUlQGDRrEyJEjKS0tzejnFe5SUE1NTQwePJgxY8ZgZoVujkhRcHf27dtHU1MTY8eOzWgbGpaR\ngjp06BDDhg1TsIskMTOGDRuW1SdahbsUnIJd5HjZ/l0o3EVEIkjhHhKrNjQzfclaxi5+lulL1rJq\nQ3OhmxRpt99+O/fdd1/Otnfeeed1ft3Q0MCkSZNoaGjgwQcfZNmyZWlvr6WlhR/84Aedj9944w2u\nuuqqnLS1vr6+Ty8wTH5tCrX966+/ni1btgBw9913p/Xz+TwW2bBC3SC7rq7OdYVqMKs2NHPLypdp\na+84ZvlpJ5Vy23+bxNza8gK1LHtbt27lwx/+cKGbcZzbb7+dU045ha9+9as53/aQIUN4++23KSkp\nyXgbu3bt4rLLLmPTpk05bFlMfX099913H3V1dTnfdhiccsopvPPOO4HXz+exSPX3YWYvuHuvB0c9\n9xBYumbbccEOsL+1nS+t2MiYftSbz8cnmGXLllFVVUV1dTWf+tSnjvv+I488wtSpU6murubKK6+k\ntbUVgKeffpqKigqqq6v56Ec/CsDmzZuZNm0aNTU1VFVV8de//hWIBQbA5ZdfzjvvvMOUKVNYsWLF\nMZ8Qtm/fzsyZM6murmby5Mns2LGDd955h4suuojJkydTWVnJz372MwAWL17Mjh07qKmpoaGhgV27\ndlFRUQHETlJfd911VFZWUltby7p16wB49NFHueKKK5g9ezbjxo3ja1/7Wq+vzRNPPEFlZSUVFRV8\n/etfB6Cjo4OFCxdSUVFBZWUl3/rWtwC4//77mThxIlVVVcybN++4bfX22vz617+mvr6eq666igkT\nJjB//nwSnc/169dz3nnnUV1dzbRp0zh48CAdHR00NDQwdepUqqqqeOihh1LuQ5DtJz6tLF68mLa2\nNmpqapg/f/4xP1/oY5E2dy/IvylTprgEM+brP/ezAv6r+eYaf+bFpkI3ObAtW7YEXveZF5t8wj/9\n4pj9nfBPv8hqfzdt2uTjxo3zPXv2uLv7vn373N39tttu86VLl7q7+969ezvXv/XWW/3+++93d/eK\nigpvaoo99/79+93d/YYbbvDHH3/c3d0PHz7sra2t7u5+8sknd24j+evk55k2bZqvXLnS3d3b2tr8\n3Xff9fb2dj9w4IC7u+/Zs8c/9KEP+dGjR/3VV1/1SZMmdW4n+fF9993n1113nbu7b9261UeNGuVt\nbW3+4x//2MeOHestLS3e1tbmo0eP9tdff/2412TGjBm+fv16b25u9lGjRvlbb73l7e3tfsEFF/gz\nzzzjjY2NPnPmzM71E/s+YsQIP3To0DHLkvX22qxbt85PPfVU3717t3d0dPi5557rv/vd7/zw4cM+\nduxY//Of/+zu7gcOHPD29nZ/6KGH/M4773R390OHDvmUKVN8586dxz1vb9tP3ueuxyf5cSGORaq/\nD6DRA2Sseu4hcObQssDrRrk3n+oTTFt7B0vXbMt4m2vXruWTn/wkZ5xxBgCnn376cets2rSJ888/\nn8rKSpYvX87mzZsBmD59OgsXLuSRRx6hoyPWro985CPcfffd3Hvvvbz22muUlQU7dgcPHqS5uZlP\nfOITQOwClpNOOgl35xvf+AZVVVXMnDmT5uZm/v73v/e4rd///vcsWLAAgAkTJnDWWWfxyiuvAHDR\nRRcxZMgQBg0axMSJE3ntte5rUK1fv576+nqGDx/OgAEDmD9/Pr/97W85++yz2blzJzfeeCO//OUv\nOfXUUwGoqqpi/vz5PP744wwYcPwlNEFem2nTpjFy5EhOOOEEampq2LVrF9u2bWPEiBFMnToVgFNP\nPZUBAwbw/PPPs2zZMmpqajjnnHPYt29f56eB7qTaflCFPBaZULiHQMOs8ZSVBh+fTZxFaW5p45aV\nL0cm4N9oaUtrea4sXLiQ733ve7z88svcdtttnXOPH3zwQe666y52797NlClT2LdvH9deey2rV6+m\nrKyMSy+9lLVr12b13MuXL2fPnj288MILbNy4kQ9+8INZzX0eOHBg59clJSUcOXIk7W2cdtpp/OUv\nf6G+vp4HH3yQ66+/HoBnn32WL3zhC7z44otMnTr1uG0HeW3SaZ+7893vfpeNGzeyceNGXn31VS65\n5JIe257N/hfjseiJwj0E5taWc88VlQwtS/8y5Gx7tsWku08w6Xyy6erCCy/k6aefZt++fQC8/fbb\nx61z8OBBRowYQXt7O8uXL+9cvmPHDs455xzuuOMOhg8fzu7du9m5cydnn302N910E3PmzOGll14K\n1I7BgwczcuRIVq1aBcDhw4dpbW3lwIEDfOADH6C0tJR169Z19u4GDx7MwYMHU27r/PPP72znK6+8\nwuuvv8748eODvyhx06ZN4ze/+Q179+6lo6ODJ554ghkzZrB3716OHj3KlVdeyV133cWLL77I0aNH\n2b17NxdccAH33nsvBw4cOO6kZKavzfjx43nzzTdZv349EDseR44cYdasWTzwwAO0t7d37uu7776b\n9n52VVpa2rnNZIU8FplQuIfE3NpyNt52Cd++uobyeJgFvcQh3z3bvpLqE0xZaQkNszL/Y5k0aRK3\n3norM2bMoLq6mi9/+cvHrXPnnXdyzjnnMH36dCZMmPB+exoaOk82Jk72PfXUU1RUVFBTU8OmTZv4\n9Kc/Hbgtjz32GPfffz9VVVWcd955/O1vf2P+/Pk0NjZSWVnJsmXLOp9/2LBhTJ8+nYqKChoaGo7Z\nzuc//3mOHj1KZWUlV199NY8++ugxvcSgRowYwZIlS7jggguorq5mypQpzJkzh+bmZurr66mpqWHB\nggXcc889dHR0sGDBgs4ThzfddBNDhw49ZnuZvjYnnngiK1as4MYbb6S6upqLL76YQ4cOcf311zNx\n4kQmT55MRUUFn/vc53LS+120aFHnEFOyQh6LTGgqZIit2tDM7as309J2fC8jWfnQMv6w+MI+alV6\n0p0KuWpDM0vXbOONljbOHFpGw6zxoZ4KKtKTbKZCqnBYAeQqoObWljO3trxze80tbRjvj7lD9j3b\nYpPYZxHpmcK9j3W9IKm5pY0vrdjIzSs2Up5h0CcHnnq2IgIK9z6Xajpf8uyWm1ds5Jv/Z3PGV56G\nsWfr7ioeJtJFtkPmCvc+FuTkZmKueja9+bD04AcNGsS+fftU9lckicfruQ8aNCjjbeiEah+bvmQt\nzRnMXkmnjkyqWjSJsfhM3yzyRXdiEkmtuzsxBT2hGijczWw28B2gBPihuy/p8v3RwE+AofF1Frv7\ncz1ts7+Ge3dFwIIoKy3hnisqew3mIG8gUSg6JtIf5SzczawEeAW4GGgC1gPXuPuWpHUeBja4+wNm\nNhF4zt3H9LTd/hruQI+zW3oTZFrj2MXPBtpm4rlLzOhwL7pevYgcL5dTIacB2919Z3zDTwJzgC1J\n6zhwavzrIcAb6TW3f+k6uyXIXPWEIGP2Zw4tCzT0k3gD6Ii/wSfKFSTaKCLhFeQK1XJgd9Ljpviy\nZLcDC8ysCXgOuDHVhsxskZk1mlnjnj17Mmhu9KR75WmQS+3TrUWTLErlCkT6s1yVH7gGeNTdRwKX\nAo+Z2XHbdveH3b3O3euGDx+eo6eOhrm15fxh8YXsWvJxvnV1Tco6MkEvSErUokm3TEFCVMoViPRn\nQYZlmoFRSY9Hxpcl+ywwG8Dd/8PMBgFnAG/lopH9TdcrTzOZzpjN0E82hbhEpDgECff1wDgzG0ss\n1OcB13ZZ53XgIuBRM/swMAjQuEuWcnVBUpAyBQlRK1cg0l/1Gu7ufsTMbgDWEJvm+CN332xmdxC7\nI8hq4CvAI2b2JWKZsdALNYFeupWqTEFzS5tmy4hEkC5ikk5huapVpD/TDbIlLYmLq5pb2nDer3NT\ne8fzkbmTk0h/op57DkRhiKOnq1p1sZNI8chp+YF8iEq491ROIEyhGPSq1oRirVUjEnUK9z6SbiGw\nYg3FTAuaJZxUegIDS0toaW3XeL1IHinc+0i6Pd5kQQuB9YVsCpp1R4Evkns6odpHsrngp5gu9U9c\n1ZrqythMtbYfZX9ru07QihSAwj1L2dRxgeK61D/dOjeZSNyIZMziZ5m+ZK2CXiRPNCyTA6lmywQt\n5RukhG8hZbNvQWn4RiQ4jbkXWJBQLKYx93SkW6smEwp8kdQU7kUoaleAJu/PkLJS3jvSQWv70bw9\nnwJfROEuBRLGwC/GN91ibJMUB4W7FI1sbiuYiWxvJg7vv2nsb23v84vQerrBeRguiJP8UrhLUeqL\n8XoIHoaZXoSWz5AN2qZivSBO8kvhLkWtr4dvEroO42RzVW5CkMBPp/5QphfGpfOJRcJL4S6hU6jA\nz4eugd/dcFSqN4bW946wvzWzTzZhnYElwSncM6QTWcUlSoHfV4r92gnJjsI9AzqRFQ4K/J4Z8OqS\nj/e6njoy4aRwz0C6J7IU+MUjVzNyyoeWdb5pmHHMbJm+mOmTytCyUk4eOCDwVcJBeu6pOjIa0gkH\nhXsGolLhsb/LNOh7C8W+KMWQSqqeeHezjoL+HvbUkVFnpbgFDfdeb5Ddn2QzeyJR4VF/EIWXfCNw\nCDaMU1ZaQsOs8WltN3nbQQI/6EnWrlJVHk20JdOhlZ4K1jW3tHHLypc7n0fCST33JNnWNA861imF\nl8/x5qDTHnNdfyidfQoyBKkTs8VJwzIZymbsVn8Mkq1M33TSHUMP0pFRZ6U4aVgmQ8kfvdP5yB3k\nY71Ib1IN/QSxdM2244K6rb2Drzz1l87tdn2exM9114PP5kY0UnjquacpnSsNRfpKT5MBeitT0F0v\nXle8FicNy4j0I+nUyEkV2tnOvpG+o3uoivQj6dzucX9rO7esfPmYWxzOrS3n5IHHj9IW031+JT0K\nd5EISNzgvMSC3fW2rb2Dm1dsPOY+tt1Njyym+/xKcDqhKhIRiaGTdKbzJs9p7+46D51YDSf13EUi\nJNGDL48HcpB+fGLoJdXQjmaBhZd67iIR03U6b5Cbo7zR0nbM9EgVEws/hbtIhHUtU9DbnPZM59lL\n8dGwjEg/MLe2nD8svpBvX12joZd+Qj13kX5EQy/9h8JdpJ/R0Ev/oGEZEZEIChTuZjbbzLaZ2XYz\nW9zNOv9oZlvMbLOZ/e/cNlNERNLR67CMmZUA3wcuBpqA9Wa22t23JK0zDrgFmO7u+83sA/lqsIj0\nDd1jNdyC9NynAdvdfae7vwc8Cczpss7/AL7v7vsB3P2t3DZTRPpSolJkc0sbzvtXsibXo5HiFiTc\ny4HdSY+b4suS/QPwD2b2BzP7o5nNzlUDRaTvdVcfXkXEwiNXs2UGAOOAemAk8Fszq3T3luSVzGwR\nsAhg9OjROXpqEck1FRELvyA992ZgVNLjkfFlyZqA1e7e7u6vAq8QC/tjuPvD7l7n7nXDhw/PtM0i\nkmfdFQtTEbHwCBLu64FxZjbWzE4E5gGru6yzilivHTM7g9gwzc4ctlNE+pCKiIVfr8My7n7EzG4A\n1gAlwI/cfbOZ3QE0uvvq+PcuMbMtQAfQ4O778tlwEckfXckafrrNnohIiAS9zV7kyw+kuqH10LJS\nzGK3G+u6rKW1Xb0UEQm9SId717u6d8Q/pSTXtk61LPnuNAp4EQmjSNeWSTVXNyjN6RWRMIt0uGc7\nJ1dzekUkrCId7tnOydWcXhEJq1CNuScXMhoS4ARow6zxad0JPpnm9IpImIVmKmTXk6OpnFR6AgNL\nS1LOggm6TLNlRKSYRW4qZJCTo63tR2ltPwocOwumrLSEb19do7AWkX4jNGPu2Zzc1MwXEelvQhPu\n2Z7c1MwXEelPQhPuqQoZpUMzX0SkPwnNmHvXQkZDykp570hH5xh7TzTzRUT6m9CEO8QCvutJ0VTT\nI5NnwZRr5ouI9EOhCvdUUgW+iEh/F5oxdxERCU7hLiISQQp3EZEICv2Yu4jkV/KkBZXmCA+Fu4h0\nq2tNJ93IJjw0LCMi3UpV00nlPMJB4S4i3equbIfKeRQ/hbuIdKu7sh0q51H8FO4i0q1UNZ1UziMc\ndEJVRLrVtaaTZsuEh8JdRHqkEh/hpGEZEZEIUriLiESQwl1EJIIU7iIiEaRwFxGJIIW7iEgEKdxF\nRCJI4S4iEkEKdxGRCFK4i4hEkMJdRCSCAoW7mc02s21mtt3MFvew3pVm5mZWl7smiohIunoNdzMr\nAb4PfAyYCFxjZhNTrDcY+CLwp1w3UkRE0hOk5z4N2O7uO939PeBJYE6K9e4E7gUO5bB9IiKSgSDh\nXg7sTnrcFF/WycwmA6Pc/dmeNmRmi8ys0cwa9+zZk3ZjRUQkmKxPqJrZCcC/AF/pbV13f9jd69y9\nbvjw4dk+tYiIdCNIuDcDo5Iej4wvSxgMVAC/NrNdwLnAap1UFREpnCDhvh4YZ2ZjzexEYB6wOvFN\ndz/g7me4+xh3HwP8Ebjc3Rvz0mIREelVr+Hu7keAG4A1wFbgKXffbGZ3mNnl+W6giIikL9A9VN39\nOeC5Lsv+uZt167NvloiIZENXqIqIRJDCXUQkghTuIiIRpHAXEYkghbuISAQFmi0jIgKwakMzS9ds\n442WNs4cWkbDrPHMrS3v/QelzyncRSSQVRuauWXly7S1dwDQ3NLGLStfBlDAFyENy4hIIEvXbOsM\n9oS29g6WrtlWoBZJTxTuIhLIGy1taS2XwlK4i0ggZw4tS2u5FJbCXUQCaZg1nrLSkmOWlZWW0DBr\nfIFaJD3RCVURCSRx0lSzZcJB4S4igc2tLVeYh4SGZUREIkjhLiISQQp3EZEIUriLiESQwl1EJIIU\n7iIiEaRwFxGJIIW7iEgEKdxFRCJI4S4iEkEKdxGRCFJtGRFJm263V/wU7iKSFt1uLxw0LCMiadHt\n9sJB4S4iadHt9sJB4S4iadHt9sJB4S4iadHt9sJBJ1RFJC263V44KNxFJG263V7x07CMiEgEKdxF\nRCJI4S4iEkGBwt3MZpvZNjPbbmaLU3z/y2a2xcxeMrNfmdlZuW+qiIgE1Wu4m1kJ8H3gY8BE4Boz\nm9hltQ1AnbtXAT8F/leuGyoiIsEF6blPA7a7+053fw94EpiTvIK7r3P31vjDPwIjc9tMERFJR5Bw\nLwd2Jz1uii/rzmeBX2TTKBERyU5O57mb2QKgDpjRzfcXAYsARo8encunFhGRJEHCvRkYlfR4ZHzZ\nMcxsJnArMMPdD6fakLs/DDwMUFdX52m3VkSKjmq7F6cg4b4eGGdmY4mF+jzg2uQVzKwWeAiY7e5v\n5byVIlKUVNu9ePU65u7uR4AbgDXAVuApd99sZneY2eXx1ZYCpwBPm9lGM1udtxaLSNFQbffiFWjM\n3d2fA57rsuyfk76emeN2iUgIqLZ78dIVqiKSMdV2L14KdxHJmGq7Fy+V/BWRjKm2e/FSuItIVlTb\nvThpWEZEJIIU7iIiEaRwFxGJII25i0hOqAxBcVG4i0jWVIag+GhYRkSypjIExUfhLiJZUxmC4qNw\nF5GsqQxB8VG4i0jWVIag+OiEqohkTWUIio/CXURyQmUIiovCXURyTnPeC0/hLiI5pTnvxUEnVEUk\npzTnvTgo3EUkpzTnvTgo3EUkpzTnvTgo3EUkpzTnvTjohKqI5JTmvBcHc/eCPHFdXZ03NjYW5LlF\npG9oSmTumdkL7l7X23rquYtIXmhKZGFpzF1E8kJTIgtL4S4ieaEpkYWlcBeRvOhu6qMD05esZdWG\n5r5tUD+jcBeRvEg1JTIhMf6ugM8fhbuI5MXc2nLuuaKS8m568Bp/zy+Fu4jkzdzacv6w+EKsm+83\nt7Sp954nCncRybueSg9oeCY/FO4iknc9jb+3tXdw84qNOsmaYwp3Ecm7xPh7T5pb2rh5xUZq73he\nIZ8DCncR6RNza8u7PbmabH9rO19asZExi59Vbz4Lqi0jIn2ma0mCoE4qPYGBpSW0tLb3+xo1QWvL\nBAp3M5sNfAcoAX7o7ku6fH8gsAyYAuwDrnb3XT1tU+Eu0j8liok1Z3mlaiLw97e2U2JGhztDy0ox\no9dl5SF+g8hZuJtZCfAKcDHQBKwHrnH3LUnrfB6ocvf/aWbzgE+4+9U9bVfhLtK/ZdqLzxUjdrVs\num8MuViWzSeQXFaFnAZsd/ed8Q0/CcwBtiStMwe4Pf71T4HvmZl5ocZ8RKToJULt9tWbaWlr7/Pn\nT4RTRzymktvQF8vyXSUzyAnVcmB30uOm+LKU67j7EeAAMCwXDRSR6JpbW87G2y7h21fXdJ5s7e6C\npyjK51W6fVrP3cwWAYsARo8e3ZdPLSJFbG5teWfvddWG5oL15gshX1Uyg/Tcm4FRSY9HxpelXMfM\nBgBDiJ1YPYa7P+zude5eN3z48MxaLCKR1rU3b8DQslJOKo3mzO183Tg8SM99PTDOzMYSC/F5wLVd\n1lkNfAb4D+AqYK3G20UkG8m9+YTk2/YNyeLEZuJkaqHl88bhvYa7ux8xsxuANcSmQv7I3Teb2R1A\no7uvBv4VeMzMtgNvE3sDEBHJqVSBn4nk6Zhhmy0TlC5iEhEJkaBTIaM5iCUi0s8p3EVEIkjhLiIS\nQQp3EZEIUriLiESQwl1EJIIU7iIiEaRwFxGJoIJdxGRme4DXMvzxM4C9OWxOoWg/iov2o7hoP1I7\ny917Lc5VsHDPhpk1BrlCq9hpP4qL9qO4aD+yo2EZEZEIUriLiERQWMP94UI3IEe0H8VF+1FctB9Z\nCOWYu4iI9CysPXcREelB6MLdzGab2TYz225miwvdnqDMbJSZrTOzLWa22cy+GF9+upn9u5n9Nf7/\naYVua2/MrMTMNpjZz+OPx5rZn+LHZIWZnVjoNvbGzIaa2U/N7D/NbKuZfSSkx+JL8d+nTWb2hJkN\nCsPxMLMfmdlbZrYpaVnK199i7o/vz0tmNrlwLT9WN/uxNP579ZKZPWNmQ5O+d0t8P7aZ2ax8ti1U\n4W5mJcD3gY8BE4FrzGxiYVsV2BHgK+4+ETgX+EK87YuBX7n7OOBX8cfF7ovA1qTH9wLfcvf/AuwH\nPluQVqXnO8Av3X0CUE1sf0J1LMysHLgJqHP3CmJ3SptHOI7Ho8DsLsu6e/0/BoyL/1sEPNBHbQzi\nUY7fj38HKty9CngFuAUg/vc+D5gU/5kfxDMtL0IV7sA0YLu773T394AngTkFblMg7v6mu78Y//og\nsTApJ9b+n8RX+wkwtzAtDMbMRgIfB34Yf2zAhcBP46uEYR+GAB8ldntI3P09d28hZMcibgBQFr8x\n/UnAm4TgeLj7b4ndkjNZd6//HGCZx/wRGGpmI/qmpT1LtR/u/ry7H4k//CMwMv71HOBJdz/s7q8C\n24llWl6ELdzLgd1Jj5viy0LFzMYAtcCfgA+6+5vxb/0N+GCBmhXUt4GvAUfjj4cBLUm/zGE4JmOB\nPcCP48NLPzSzkwnZsXD3ZuA+4HVioX4AeIHwHY+E7l7/MP/d/3fgF/Gv+3Q/whbuoWdmpwD/Btzs\n7v8v+Xsem7pUtNOXzOwy4C13f6HQbcnSAGAy8IC71wLv0mUIptiPBUB8THoOsTerM4GTOX6IIJTC\n8Pr3xsxuJTYcu7wQzx+2cG8GRiU9HhlfFgpmVkos2Je7+8r44r8nPmLG/3+rUO0LYDpwuZntIjYk\ndiGxseuh8WEBCMcxaQKa3P1P8cc/JRb2YToWADOBV919j7u3AyuJHaOwHY+E7l7/0P3dm9lC4DJg\nvr8/37xP9yNs4b4eGBefDXAisZMTqwvcpkDiY9P/Cmx1939J+tZq4DPxrz8D/Kyv2xaUu9/i7iPd\nfQyx136tu88H1gFXxVcr6n0AcPe/AbvNbHx80UXAFkJ0LOJeB841s5Piv1+J/QjV8UjS3eu/Gvh0\nfNbMucCBpOGbomNms4kNXV7u7q1J31oNzDOzgWY2ltgJ4j/nrSHuHqp/wKXEzkDvAG4tdHvSaPd/\nJfYx8yVgY/zfpcTGrH8F/BX4v8DphW5rwP2pB34e//rs+C/pduBpYGCh2xeg/TVAY/x4rAJOC+Ox\nAL4J/CewCXgMGBiG4wE8Qew8QTuxT1Kf7e71B4zYLLkdwMvEZgcVfB962I/txMbWE3/nDyatf2t8\nP7YBH8tn23SFqohIBIVtWEZERAJQuIuIRJDCXUQkghTuIiIRpHAXEYkghbuISAQp3EVEIkjhLiIS\nQf8fmGp3BNujtIkAAAAASUVORK5CYII=\n",
      "text/plain": [
       "<matplotlib.figure.Figure at 0x13259bdd8>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "classification loss on last batch was: 0.0004836621741852622\n"
     ]
    }
   ],
   "source": [
    "mixed_curriculum_train(wrapper.rnn,wrapper.train_set,stop_threshold = 0.0005)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "wrapper.rnn.renew()  \n",
    "# you only really need this if you start messing about and doing weird stuff. \n",
    "# It cleans the computation graph, but doesn't reset the weights so don't worry"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "scrolled": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "provided counterexamples are: ['', '10']\n",
      "obs table refinement took 0.0\n",
      "guided starting equivalence query for DFA of size 1\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAIgAAAA7CAYAAACg5MKJAAAAAXNSR0IArs4c6QAADDlJREFUeAHt\nXQeQFNcRbQ440pFMECIIKCTBiWAEhjI5Y4LIiFAYjC2EESBARUYUIISFVJRBRSySrgQIDEiHEAWU\nSkTbZIFJhYhCwNWRc/Yd137vy7ua20t7u7Now7xXezPz58+f+T09/bv7z+7lUNU14sCRQAYSyAEF\n0Qz2OcWOBCTKkYEjgcwk4ChIZtJx9jkWxNGBzCUQUAuSIinSDswRxFwiSzKXUITvzRXI/r8v78s2\ncBFYBAw27JAdMgSsCtYDHaSVQMCimDWyRnqCn4F/BoMRKiodwYPg92Bp0EFqCQREQY7KUakP/gWc\nDQYz7sk9qQvSwu0E84AOfpGA7QpyU25KHbA8+B2YCwx2nJJTRkm6S3dZCjr4RQK2OqnP5JkZVrjk\nEBMKykFRVAa/AOPAuaADiwSYSbUL7+l7mg88BIYipuk0zQXuBB38LAGxSxDLdBl9Pv0CDFWkaIp2\nA0uAF0AHqrb4IIwCGoJDwRlgKOOBPDAhb7REy7/BfGAkw28FuSbX5HdgLLgJzAmGOs7JOeNoM8m3\nAoxk+OWkJkkS/P7ueNai5R9gOCgHlaESyP6QfwcjGv6Ms+/oOxoDHgPDETN0huYEvwMjFT47qYt1\nMRyYHPolGM7orb31N+A5MBLhkw+yR/ZIU3AM+CEYzngsj6UBmAyy3wXASEK2FSRREo1TWltqy3ow\nKgLeGLggF0yf+VCsBSMJ2VKQp/LUWI7bclv2g4XASAFnfluBsb1iJeZijNy+fVvu3r0rjx8/lidP\nnsjTp085XEuOHHi5AZ+8efNKgQKwN/gUK1ZMSpQoISVLlpQKFSpIxYoVpXLlylK9enWJiYkJahFm\nS0HekrfkS5DKwfR0pGGOzJFhY4ZJp6ROUqtoLSlcuLDky5fPKEOePL9M8qWkpBjFefTokdy/f19u\n3rwpN27ckMTERLlw4YJcvHjRKBUVqVKlStKwYUNp0qSJtGvXzihRUMnVW8drrs41TukG3eDtIWFZ\nr7/218LgKdBXPHv2TE+fPq3x8fE6btw4bdy4sUZHR2tUVJQ2atRI4+LiFJbJ1+ZtPc6rKIZzE5yj\n+BCMdDzRJ1oXrALeBe0CLI1RmO7duxtlKV68uM6aNUsxdKU5BYY0/fbbb/WTTz7RXbt2KRUuO7h8\n+bJu377dq0OyVJCLetHMTXTVrpipSPGq0XCvlKAJWgrsCAZCJlevXtUxY8Yohi+tUaOGnjhxwi1S\n7oMPo4sXL9br16/r6NGjtX379l4pybVr13TkyJGm3WHDhrnbzGwlUwV5pI+0FlgNvA8+L7Ajmzdv\ntu10n3/+uW1tuRrapbs0GpwEBgpnz57VevXqaZEiRfTAgQNGCeCvaMeOHd2nTE5O1vLly+vYsWPd\nZRmt7N+/X48cOcLvQaktCtJH+2hR8Cz4vMAOt2zZUhcsWGDLKbdt26ZlypSxpS3PRhbqQuOXxWu8\n5y7btumLtGnTRkuXLq3ffPONubkbNqT2AydNmqSIlvTBgwdZnpdDVnYUJMPXvWbKTDMXwQk4zk3Y\nCfRCdu7cKYcPH5acOXNKlSpVpFWrViZU7NOnj2zZssV48/Ty8bTIiy++aKKCHTt2yKFDh8wxffv2\nFdx492Ux7Fy1apUMHjxYYH3k6NGjUrt2benatasJOxcuXCgQsnTo0MF9jL8rA2Wg/AfsB+4F+fKz\n3WC4vHLlSiOjqVOnmuYZHltRrVo1efjwoWzatEnefPNN6y6/16PSa2GLbDFZ0ukyXVqDdmPixIkC\n8ykjRowQmFDhNsF8Ap4Ws86bz1wBw0g8GfLKK6+YdXj9AisjDRo0MErDyhhCpGzZsjJ8+HCZO3eu\njB8/Xljv1q1bgjFcGIKyrXLlypm27fzDd25rgp1B5ocCgaJFi0r//v0Fvohpng+MFcyvEIiMrMX2\nrHvaJPoaxcDmYCCAHIHSQ7d60dOmTXOfClbFmMClS5e6y1asWGFCwCtXrpgyVx2OqS7A8pjjGDoS\nP/zwg1l27txZoRhmPVB/EjVR84B/BAOFZcuWKSyqwuKmOQXlAG3QIUOGpNnnWZDdISaNBYmRGPkr\nuAvcB9oNDht8mnv27Cnr1683zY8aNSrNaVjPhd69e8vx48flhRdeMFaGwxNx5swZVxUzfHCjU6dO\npozDlgvWtlxldi75Hitfp+N3bAIFJts4HKcHhLmmuFSpUunt9qssjYKwNU7AtQC7gpdBu8FhoFCh\nQoKnW+CQyp07d9KcwnpTkUAyygFnTGbOnCmxsbGmPjOWLrAO4Vq6yrm0tmUtt2P9K/kKA/F0mQ/+\nHgwUVq9ebXwxKgPT+lYwW0u89tpr1mJb1tNVEE7ArQRpTbqB/wXtRM2aNY2zSYeSjmetWrWMv2A9\nh/Wmnj9/Xl5//XWpW7euTJgwQRDWWatmuW5tK8vK2ahwTI7Jn8DBIKchMgJ9Jn58xezZswXDiEnF\ns41Lly6laoppfOK5KQhPVhj8GjwO2mk6qf3Lly+XggULyrx582Tjxo2CzJ7Ad+Bp3U+7y2yybMqU\nKZKUlCRvvPEGN8VqOUxBJn+oHNa2MqmarV235JZxTDmrPQv0BK+Ryj9o0CBj/TgH4wtoMenMT548\n2ciBDjeyp6maOnjwoPChe/XVV1OV27Lh6cR4bq/X9SbWn6/zPXf5tM24vn79+kpnleASM526bt06\ns80kGTqmAwYMMPuY2OnWrZspgzKZ7OG7775rtplqRnhrjhs6dKgpw9Nktl1/YKU0d+7ceu7cOWXi\nyZtcgevYjJbJmqytwHLgVdAF9mX37t0mCYUZXHM9dCrZnx9//NFVzaslHfHmzZsbp3T69OnuY5gJ\nrVq1qlt+lCcUQ6Ek7jpc4XXUqVNHFy1alKqcjj6vZ+DAganKM9rINJPqOugD/UBzg/8E/QU7hDBN\ne/XqpWvXrtUZM2YoEz1WtGjRwnSiWbNmiifPdJbZQjw92qVLF8VsqCLHoQj/zMTWkiVLTDKMHe/R\no4fu27fP3RyjpVy5cplsJEy1u9yflZE6UvOC34MEbw5T3uwXr4EKyaX189NPP2V5Ss6xMApjYgyW\nTzH06p49e1IdRyVk1hTWVNkfhPTKCMcTLOP5mYVl8pFAnkQRHJhyhMYmXc95mczglYJwvqEzWBK8\nBPoLDBdmEoo3Pz1QCAkJCal2YZhI9fSzDkM2bwAnWO/du+dN1Szr8Hs/DFk+OvaRIn+jL730khF4\nekphVRAqtScoB1oKDLWKhJ5i2DXhPDPJiPDcVsLzOG7zprvC/vT2s4zWGENcRru9Kvf6fZD7ct94\n6fklv/wLzAtGGtadXic9VveQmOUxcufMHYFSGN/IGznExcWZuvRFMNzIyZMnBbkaE7bTH8M0v7Rt\n29ZEdkz62QGmEeh/MZvsK7xWEJ7gLMgvZncAl4GRhFWbVkm/kf0k+aTv0QhDe1gc9xtl8CXMdACj\nj4xyHL7KGBbTRIpNmzb1tYmfj/PKzlgqbdbNGgXOAiMFSZqkTcCK4NbvtyqiCnU5ofRvIMksP9l1\nUoNFtl75IJ4X+7F+bL4vslW3eu4Ky+2hOlQLgEdAF+gD8KUdpvgxoeZOg2ekLHyPIxThk4Kwoz1B\nztmcB8MZn+lnxildo2sy7CZmUhUzrtq6dWvjZDK0ZRRiVRa+3BOK8FlBHupD/e3/yfVwxF7daybh\nxut4r7vHyGHOnDkmRKWC8D1TLjGX4nUbwVTRZwVhJ2g9aEV6gOGGy3pZS4PtwGegL8BkoiILrC+/\n/LI7oedLO7/mMdmKYvAkpAF/xfAPICf4xoHhAM49NQOvgwdATjtELOzQzk/1UxPZMMIJB7ytb2tB\n8AQY6fBriLEKr5/20yLgaTCUwTknfin9a9CBTb8wRPP7BGwEPgL5fmZBMNTAXxRqDvIHgCeDDjC7\nzqfELkEkSIL5kjN/tTge5E9whwpC+doDKeN0Xxjy9YRlpaz57u5G2ShTwVABrV8XsBjIKYRQUuyA\nyzgQ4+wCXRBS47jLfzqjZwIhjpBu0zYn1VMKoRIJcE6Jc0vhEoF53gd/t231QazmzppL4M9FBON/\ne2AOh9/7+Rs4FnSQVgIBUxCe6grIdzb5q0TBCv5HCv6aoYP0JRBQBeEpT4NHwGBFe2mPV6DyB+vl\n/erXFXAF+dV76FyAXxKwNcz160qcg4NSAo6CBOVtCZ6LchQkeO5FUF7J/wBmJZL2/HeXKAAAAABJ\nRU5ErkJggg==\n",
      "text/plain": [
       "<IPython.core.display.Image object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "storing provided counterexample of length 2\n",
      "returning counterexample of length 2:\t\t10, this counterexample is rejected by the given RNN.\n",
      "equivalence checking took: 0.017189000000001897\n",
      "obs table refinement took 0.002\n",
      "guided starting equivalence query for DFA of size 4\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAIUAAAGTCAYAAAAGItEOAAAAAXNSR0IArs4c6QAANGtJREFUeAHt\nfQncTdX6/yMyKxEhUYlIRagQUdx+JaEQDaK6daVZpfEW1f+mpO4VDVejUAgNSDTJPHdNJSRzypQh\nFNb/+13s03nPe+azx3PW83ze95yzh7XXetZ3r+kZVgGl1EgxZCQQJoECAIUK+22+GgnIUUYGRgKR\nEjCgiJSI+W1aCoOB/BJwtKU4JIekFbiAj/l1eT2/VHL8SCEny/+oPCpfgv8LLg32G30tX8vt4Nrg\nRmBDRyTA2YcTNEKNUAJ+E+xXOqQOqdbgiuANYEOHJeDIlHSRLJLG4JvAA8B+pp2yU84DsyWbAi4C\nznWyHRRbZaucC64KngwuBPY7LZflGhgdpIO8Ac51snWgeVAOSicwP0eCgwAIAuB08DDwW+CB4Jwn\nO/vRe9W9qhh4ATiI9LR6WhUCTwHnMoldhR+ihuiB5TA1zK4kXU+HA8/24HLgNeBcJVvGFPNlvjQB\n3wHuBw4y7ZbdenpaWArLNHAxcK5RxqD4RX6RBuBa4AngguCg0ypZpQfLXHgbCs41ymig+af8ifF6\nB7xTheV9cDYAggCoBmZ5yP3BOUeZ9Ju3qdtUSfBicDZSP9VPFQRPBucSpT3QHKwGqwLgD8DZTNeo\na1QZ8CpwrlBaY4qZMlOag3uBnwJnM+2VvXIB+AB40q5J8tvG3+SXX36RX3/9VXbu3Cm7d++WPXv2\nyP79+7UYABwpWLCgFC9eXP8de+yxUr58eTnhhBPkpJNOEv72O6UMio2yUQ8s60t9+Qh8VA5o39fI\nGl3m43oeJyteXBGqU1Z8yZIlpUSJElK4cGEpUKCAHHXUUfLnn3/K77//Lnv37pUdO3bIoUOHQvcc\nf/zxUr16dalbt67Ur19fGjVqJGeccUbovB++pASK/bJftxDbZbvMAR8DzhWiRrXl2pbSY0cPebjc\nw1KuXDkpVCjxEj4BsW3bNtm8ebOsXr1afvzxR/n+++9l4cKFsmjRIg2eypUry6WXXirXXHONNG/e\nXAPLU7mm0k/epG5Sx4C/B+ciDVAD1FHg8WA76I8//lDTp09Xffr0UXXq1KGtrEIXo/r376927dpl\nxyPSSiPpgeZANVAPLD9Rn6T1oGy5qZvqpo4FLwfbTd9995268847FbokhXGIGjJkiN2PSCq9pEBB\nXQB1Ak+Bc532qX3qPHBN8G9gJwgDWdW9e3eF8Ynq0KGDwmA2z2P27dunPvvsM/Xss8/qlubgwYN5\nzmf6IyEo1qq1WhdwlboKmoFDmT4vK+5fr9arCuA2YCdlMmnSJIWBqWrcuLHCwFXLDmMTdcopp6jB\ngwcrzIDUAw88oC6//HJlJzDiguJ39buqBz4TvAvsFvFN+fTTT2173DvvvGNbWlZC09V0VRj8ONhJ\nWrx4sSpTpozq0qWLrvgmTZqoNm3ahB554MABVbVqVfXggw+GjmX6JS4orlPXqePAK8FuEQvZsmVL\n9corr9jyyC+//FKdeOKJtqQVmchr6jU9zhqjxkSesvX36NGj9SB0wIAB+vOTT/KO6x5//HGFaXG+\nbibdTMQERX/VXy/xfqY+SzftmPdhmqa++uor9eKLLyoWlM0kiX1l+/btdcGvvfZa9eqrr6qNGzfq\nc2w+J0yYoJ5++mn1zDPPqPXr1+vj1j9M+9SgQYP0T17Xt29fNXnyZFWqVCl1zDHH6LQ+/vhj63Lb\nPrur7nqpf4laYlua0RJq0KCBqlmzppbNTz/9lOeSkSNH6uP8tIOigoJr/Vzzfw7sBD3yyCO6T2Ta\nc+fOVeedd55+DBZ69HFOzdhXEjjbt2/X0zO+7fzNluSpp57STabVz7799tsKC0kK6wbqpZdeCk3v\nRowYoS644AKFNQV9L9YGbC/OH+oP1QR8Gngb2Cniy1C0aFFd+Vg9zfOYr7/+Wh/nNXZQPlBw7FAW\nfDHYCWIrwcETK9ii8MJ8++23uoBvvPGGdVoNHTpUj8R//vlnfcy6Zs6cOaFrrrvuOn3fmDGHm3JO\n70jt2rXTc//QhQ582ag2qiLg68FO0bvvvquwYqqwhJ7vEZQDX6Tbb78937l0DhwVuXJWUkrKP8DT\nwbPBdhOXgk8//XTp1KmTfPTRRzr5+++/P99jeJ1FXOlbsmSJ1h+gi5EpU6boUytW/LXkXKlSJX2s\nbdu2+hNNrXW7Xn4O/XDgC+06aXZGHxKnCItZMVc6MfPQj61QoYItj88HCqZKJVcL8FXgTWC7aeDA\ngYJ+XvAWCwaVWj8Q+YxwUFCfQIUSBlTywgsvSK1atfTl4ToFXkOyPvWPI//C0wo/bsf30TJangG/\nDG4IdoqmTp0qZcuWFQLAUr5ZzyJgSHbpUKKCgkqu4WC2Gu3Bf4DtJCqDFixYID169BD0h1KvXj2t\nHwh/RnhFUmdwzjnnCMYegvGIYAoWfmnC7+FpJbw4hQsWy2LpCu4BvhnsFK1Zs0bQLUrDhodBt27d\nujyP2rJli/7tKCj4hGPBH4KXgO1sFoly9I+CWYFgtiDjx4+XTZs26ULzuVYFWk0ij/Xu3VtrHlu3\nbs2febSO+kCcf0wvPK04l6Z0aptsk3ZgaotfBDtF1Lh27dpVq90xU5MiRYoI9CV5Hjd//nytda1R\no0ae4+n+iNpSWInR7pI2inSQeQVsB2HgI5hqcoCrk7vkkkuE6mT+kSpWrKg/Z86cqa+hJpH2CgQO\npprCt+Lll1/W12C6Gup6eA1p69at+tP6x/QwQNXayVWrVum0rHPpftKvpTOY5oijwEeDoxFmSoJp\nsWAhLtrphMdYpquuukrmzZsnmG7qFvKOO2Ac3a9fSH4cY2HdQjAwj9p1JnxItAuSGZ32UX3U0eBv\nwJkSbAwUKkp17txZjRo1SqGAiosv4dSiRQs9mr7ooosUmk41Y8YMPQXFW6KuvPJKtXbtWgVbBHXc\nccept956S73++ut6gQrlU1dffbWaPXt2KDnOcjhVLV26tF4TCZ3I4Mt96j5VFDwPHEnUfHI19qab\noFHG+gjzlM5q47Rp0xQG5ArjCMXvFnH2xvTQauryPPzww7YrzvJNSa2Hh39yfb8duDx4HThTQpOo\nONdmhUcjFjxycQpdQJ4VO14TOV+PlhaPcf0DVlKxTqd0nH4tnGq8C7aI+UA3qNDMaw0ngXD00Udr\nQPDzsccesy5N+MnpJVoHfS9XdmPJiOs11hQ9YaIpXpAUKJjmTvAZ4AbgveBcpPlqvvaA66l66tVX\nrpBef/31eomZQGCLxM/wP1hkaXuJePKC0Y3WeGIAru/FoFp9+OGH8W5x9Fxi0yGUkFQKTPM7Og/f\nCh4CziX6VX6VdvvaSfWJ1WXjyI1S5qMy2mqK1lccO5Csz0i58BoSalKPb5YtWyZQdAlaBUHXIJxN\nQOmlxw9YkRUovSKTcPd3qpD7VH2qrY9eVC+memtgr1+9brUqf115VaB4Af0mY0aTpzVgfcf6Y/dB\nVTdmBqpYsWKh67j0DhM89eSTT2qbCHYHfqGkWwoLqpfKpfIv8P3gs8EXg7Od+lfuL7ue2yV3n323\njBs8TlauXCmobD1NTqbsXG39v//7Pz2tPPXUU/WKLhfjfEvporOT6qR1JKvV6nSTCMR9jMTDgeVI\nsEVU4mFqqGCur9986iNQwVH/2FJQSRckSnqgGVmoPWqPqnOE+T0baZaapRVdD6uHoxaP08+xY8eq\nK664QiuqCI7IroWDT5oABInSBgULyVaCGtWrwdlGm9QmVQncCnwQnIiwqJZHbc8Wgq0HdDF6HSXR\n/X46nxEoWJAvwDTqfQacLbRf7VeNwdXBO8Cp0tKlS1WvXr20HQeB4YQ5YKp5SuX6jEHBh/0bTH8I\nzkyygW5Rt6hS4GXgTIgLbrS6dsK4J5N8JbrXFlDwITeAS4N/AAeZXlYva7vLD5V3i0deyy8lt8F4\nU6h9sk+agn8HzwJzsStoxMg1nGIzKOwT4Fwl20BBAa4HM6oNo9eOATP8clAoyHm3W8ZxVeepPqyy\nVJYPwOPBT4KDQmzlrgSXBXP5PkhgdkTGTvRfr6hXAtUvW+OhFWqFE+IIXJq2DTQjS27XCD4yXbt/\nU4eTTTMnO+TjGCjC5/rb1XY78qrToI+HXcQ1Fvq39AUb+ksCtg40I/u3n+VnbcPI6DdxaS/O0tq/\nHf6KxrlyPs51xN+Pca5J8RTDRjMKnqG/JJCylvSvWxN/qyAV5Cvw/8DxaM7EOdL/uv7y2obXpHSF\n2PuCDBk+RMatHidPz3xaajSyx0j1crk8XtZy8pyjLUWyEoX1ksDuUr755puYt9DHg84uDECGwB5C\ny2ZDzkjA1ilpOlmEplHGjRsncCyOezsBQ0CQhg0b5ojZftwM5NBJz0Hx+eef69CDNGWPRwQCDVtI\nDCyGEAPxLjfnMpCA56BA7AU599xztVVSrHLQIQYe5CFLJ9o8wuk41uXmeIYS8BQUNHSlk3GirmPi\nxIli+UuyvLyPYKK3mSH7JeApKOgFRo8uOPjELRlbBcsi2rqQ3lN0OTRkvwQ8BQXd6apVq6Yj0MYq\nGiufrUmk+TxM37RPaqz7zPH0JeA5KFq1ahU39wQEZyiRBAMW3VIwPrYheyXgGSjoMIyINHLZZZfF\nLRG7jmgxJ3gTgQHD2bj3m5OpS8AzULDrQAwnad68ecxcc+qJIGlx1yQY1sCQvRLwFBQEBLymYpbo\ngw8+oMIu5nmucnK9glstGLJPAp6AghXNyqTXVDyCFXRcUPBepsXYDYbsk4AnoGBQM3YNzZo1i1kS\nBiShAy4j0XBMwT9+D/9tHUeci5jpmBOpS8ATUFCPwUBo2M4gZo7pf8mVTA4mrT+2CGwZrN/WpxUt\nL2Zi5kRKEvAMFHS3jzWrSKkE5mLbJeAJKBj+78ILL7S9MCZBeyTgOigYEJVrFE2bNrWnBCYV2yXg\nOig4eOQmbAhAbnthTIL2SMB1UHBDNQYBJTAM+VMCnoCC0XMN+VcCroOC+g4DCv8CgjlzFRQ0zuWi\nlQGFAUVIAmwluCIZb9EqdLH54pkEXG0pGBubZvoM1m7IvxJwFRTc0pkhAw35WwKugoL7diDQaB6J\nMMI+9/xIlzK9P93nZvN9roKCmk9u9k6iYw+3iWLLkY71VKb3Z3OlZlo2V0HBmQdjUJN++uknueGG\nGwRbPaRVhkzvT+uhOXKTow7GkTLEdpKCPTr0YToARTPIjbwn1u9M74+Vrjnu4joFbR9oeW2Bwgjf\nvxJwrfugwQyJe2AZ8rcEXAMFWwoSnXgM+VsCroPCWFv5GxDMnWugsETBZW5D/paAa6DABvVaEti0\n3t8SMblzr6Wg1ziDjlj7hxrZ+1cCrrUUFAFbi/CWgusWJG64mg5len86z8yFe1wFBbZXCu04TF/S\nu+++W8sY2y0KNpzVO/ElK/RM70/2Obl4navR8biBPU37n3/++bRkTd/Sjh07JnQlTCtxc1NIAq62\nFNxhb/PmzaGHmy/+lIABhT/rxdNcuQqKk046SQdR9bTE5uEJJeAqKGg7QZU340oY8q8EXAUFg54x\nzOGGDRv8KxGTM/cWryhryz6TBryG/CsBV1sKWnKXLl1ali1b5l+JmJy521JQ3meddZYsWrTIiN7H\nEnC1paAczj77bFm8eLGPRWKy5joo2FIQFPGi3plq8VYCroOifv36Ovj68uXLvS25eXpMCbgOCvqR\nMqjqrFmzYmbKnPBWAq6DgjYV9erVk9mzZ+uSb9myRe/d0alTJxk4cKC30jBP1xJw1e/DkjnXK7gj\nEH035s/nFoKHg6Q2btzYusR8eigBV0BBayuCgHuFMSo/Xf7YYqxcuTJUdFp5G2/0kDg8/eI4KLij\nT40aNbQBDYFg+X9Yn1bp6QLAgKuGvJeA42MKvv2DBg3SJY0EQmTxTUsRKRFvfjsOChaLOwnefPPN\n+bZ8iiyyAUWkRLz57QooWDRuLlu1atW4HmIGFN6AIPKproGCltyJou0bUERWjze/XQMFi8eoeM8+\n+6wOhhatuAYU0aTi/jFXQcHi9ezZU7gjUOSWkjxnQEEpeE+ug4K+pMOHD5eSJUvmaTEIEhOa2XtA\nMAeug4IPpbENN4QL15RavqY8b8hbCXgCCha5devW0qNHj9BspESJEt5Kwjw9JAHHVzRDT4rypX//\n/nr5+4cffsg3njgkh+QX8CbwHvBe8FwwaTy42BEuLaWlEvhYsCF7JOCq22C0LM9fPF8a1m8olepU\nktZzW8sS8I/gn8EHwHmIP+mLXDLPUf2juBSXE8E1wWce4XPkHKkFNpSaBFwHhRIlc8ATwFPAs8H7\nXtonhcYXkvMnnq+rs4bU0G8/W4CK4FJgtgxFwUeD9x1hth7bwBuP8HpZL8vAS8HLwX+Ay4MvBDcH\ntwGfBDYUXwKugYKVPww8FszKOwV8EZgVRp7y9hTp1q1b/NymcPZP+VMWgr85wgTgLvC54PbgLmAC\nzlAUCWAG4BjtVrvVa+C6YDQQqjb4CfD/wG7TfrVfTQD/HVwWXAjcHjwZbCivBDgttJ0IhufA5cDF\nwF3BM8B+oX1qnxoKbgomWBuAx4ENHZaAraA4pA7ploFgKAl+CPwr2M80T81TbcAEx/ngOeBcJ9tA\nsVAt1EJls3wveAs4SLRALVDNwEeBbwNvB+cqZQwKtg7Pg48GszleDA4ysVupAK4C9lOX56ZMMwIF\n36ZWYLYOfcEESDYQu7zLwSwXx0a5RmmDYr1ar84EVwLPAmcjsQVkd9IdfBCcK5TWMvcqWSUXg0uC\nZ4GzdUHoPrlPqoGvBf8Kfh9cCJztlPLi1WbZLBeAqWv4AkzdQ7bTVJkql4I7gd8EZzulpCXl8nIr\n8FHgT8G5AAgCoCn4A/BQ8OPgrKdU+skeqoc6FrwKnIv0qnpVFQB/Ac5mSrr7oLq6NZj9KpvRXKWO\n0lFmgheDjwNnIyUFCiqXzgDXBxMUuUzbZTt0uDWkK/h5cDZSUmOK1+Q1WQfuC851YuvAccVA8Bpw\nNlLCloJKgVPBtEX4D9grmjFjhkyaNEk7Jv/tb38Txvn2ithyngbuAO4PzjpKNGD6XH2ulUVL1dJE\nlzp2/q677lLYAUBVqVJFoQIULMIV/Ecce14yCfdRfVR58B/gbKOE3cd78p6cB+aYwgsaM2aMcN+x\nrVu36mi9DGnAbSwfffRR4d7pXlE36aZtSLlWk22UEBTTZJq0BHtFM2fO1FtBMH4FfUZatGghjHpz\n4MABmTv3sCGvF3mrIlX0gJPyyTaKC4qtslXbOnIF0yvq1atXyA3AygPdA0heb3xLuXB6mm0UFxRr\nZa0uL6dgXlG5cuXyPXrdunUaEA0bNsx3zs0DlMtP4GyjuKBgS0E6HuwnGjFihDzxxBOeR74pK2Uh\nocMy8pN8Ms1LXFDQCYdUAuwXYsysihUrhvYf8zJflIslIy/zYfez44LCWsalb4UfaMWKFfLmm9BT\n4s8PxNVNS0Z+yI9deYgLCjaPJNoSeE07duyQ3r17y5AhQ6RIkSJeZ0c/n26Nfuta7RBMXFBw1a4I\neAHYS+JeppyF/Oc//xFuY2nRpk2bhH6oXhGdjWqDs40SLnNz2kXfTOo/vCBG1Gvbtq3UrVtXKlWq\nFMrCtm3b5JtvvhHuT8pQjG4Tl3nLgR8F3wvOKkq0RPtP9U91IvgA2Avq3LmzXtqG0PN9ovXwIkv6\nmVPVVL3874W3m9OFTthS0B6zOvgT8OVgQ4clwGXuRWCvu1Yn6iPumIIPpOFqM/C/wYYOS4AxM0aC\n/w7ORkrYUrDQNFylZzjtMmnAmutEMEwG/wDmQDzbKClQsNC0p2BXMh/MOBG5Soym0xD8NpjhDLKR\nkgYFrYzqgK8DDwLnIjG+BaPjsEudCC4AzkZKOKawCl1Vqupp6cvyck7aaXKqcTN4J/gdcLYCgvVd\nyKr0ZD5pxc3QRDRa5Wrn38C5QnfJXfIxmC1EBXBWU6pzXjoRXwtm/IkvwblAvVQv7VM6So3KheKi\nUUyDaJd4DbgweDg4W4nl7AJmmIV3wblCaYGCwmGL0RNMjylGrPkTnE20Tq3T8TbYIk4E5xKlDQpL\nSG+qN1VxMEMDrQRnA41Wo1UZ8BngoAdhSac+kp59xBpY3Sg3yjwwY1qeBX4KvB8cRPoJpnXtwAyp\neCWYaxJUBuYcpYOkaPew+2DUlxLgamCGCfJKiRYtf/GOMT7XI2BG8qsJznYH4niy4LmMu4/IB6xV\na3WIxIKqoKoBfgu8F+xHYjQejoc4bmBEv35gxtvMdbIdFJZAV6gVGhwcubN/ZsQ8L73MrHyxRWOQ\n1bZgAvcE8LNgxv40dFgCjoHCEvDP6mf1/8Ang7EoqGqBHwXPBbsVR4oV/jG4G5jRdpmP5uD3waZl\nsGrqr8+kdR+ZDra4VcN08JgjTJ8ShkhqAmakmHpgDuoSxcvevXu33lUoVn4OykFZAWbQdsbjYmxu\n2jzw+PlgDiLJjA1uKLoEXANF5OO5hQODqJPperfpwCZaCEuZimW0UQ+3aYiM4l9wf0EZcf8Iueal\na3Qc/2hR/KnO5uynIJjbOlDlT3sQ8glgQ4kl4BkoIrM25osx0v5v7eXp9U/L1kpbZQOYWzZw34/d\nYAJgz9g9cqDLASn6a1EpXqy43u7B2gSGAArf74OAyGUVf6R8U/r9V0/i7bd77rlH1a5dO24msBOy\nttN8//33415nTmYmgYwXr1JCYJyLP/nkE7niiitiXrFr1y7hNaShQ4fGvM6cyFwCvgDFd999J6tW\nrYoLirFjx8rBgwd1iSdOnCh0DjLkjAR8AQq2AMcff7zE8yKnZ5hFhw4dktGjR1s/zafNEvAFKMaN\nGyetWiFoKyLWRKNff/1VvvrqKyEYLAoHiXXMfNojgei1YE/aSaXCboBBzqxAJNFuGjlyZJ7djgmO\nqVOnCt0GDdkvAc9BwRYAY2UdtihW8dgqhLcSvI6tCuNUGLJfAp6D4osvvpBzzjlHypQpE7V0a9as\nkTlz5mjghF9AkLzzzjvhh8x3myTgOSgY7a5ly5Yxi/Pee+9JoUL57YvZunz77bd61hLzZnMiLQl4\nCor169fL8uXL44KCrQEj4UUjgmX48OHRTpljGUjAU1Cw62AAkgsuiB59b+nSpfL999/HLB7BYrqQ\nmOJJ+4TnoCAgihUrFrUA7DoSxZ7gohe7EUP2ScBTUHAq2rRp05ilYSvAoCWJiOAxZJ8E8o/g7Es7\nbkq//PKLHiQ2atQo6nUbN27MBxiGYmY4o1j3RE3IHExdApnp09K/+8MPP9SB17dvT35T2FGjRmkt\nafpPNXcmIwHPug/G3K5Vq5aULp39G9Ol/qp6e4enoGjcuLG3pTdPjyoBT0BBFTgj8MfTikbNrTno\nigQ8AQUj5+7du1cvb7tSSvOQlCTgCSgWL16st2s44wxvNpZJSUI5eLFnoDjttNOkaNHcjZ3lZ6x5\nBoqzzz7bz3LJ6bx5BoqzzjorpwXv58K7Dor9+/frDeHMeMK/sHAdFNzqCatqcvLJJ/tXKjmeM9dB\nQUsqUtWqVXNc9P4tvusKsbVr10rx4sW1ST/Fsnr1aqEfB9XntOguX758UtJiNzRlyhStNm/SpIle\nCItlDZ5UguaikARcbymo6aSPBwm7EMtNN92kjXY5RW3evLm20g7lLsYXalipNyHAeD+Ua9KmTZt8\nxr0xbjeHE0kgGa2Znddg52FVp04dhc1bFN5stWDBglDygwcPVmXLllUYd4SOhX+xtKRoGRRAEDoF\nCyyF7kg9+OCDoWPmS/oScL2lgKpca0b79u2rl7lpyW3R9ddfL4w/8cYbb1iHon5OmzZNbrnlltA5\n7m7ctWtXGThwoOzZc3iHxNBJ8yVlCbgOCjoK0y6TzjyRaxVc4axWrZrQ+ScRRd575plnakBMmDAh\n0a3mfAIJuA4Kakg5SKTfBvcXjSQONFeuXJnPzyPyush7rQGqlxvNReYxqL89AcUff/yh5RXNYJcz\nE57ngDQWsbsoXLhwntO8j2RcCfOIJa0fnoDCqtACBQrkyzRbEnYvqW5ub4UpqFAhyyPs55OY/Qdc\nBwUdeFjppGiDQo45atSooVXrsYprdUHh53kfySyfh0slve+ug8LqMkqUKCFc8o6kLVu2JFWxkffy\nPpIBRaREU//tOijY9+/bt09uvvlmmTVrVp4Fp507dwqtsq6++uq4JWFLM3369DzXzJ8/X29oy1bG\nUGYS8AQU3Ka6Z8+ewjWL8Ig0DC3Qrl07QcCzuKW64447pF+/fqEZCkHGaDhc3zBL3XFFl9RJ13Uf\nHEByS2oqxLgt9e233y58y0844QS9bP3yyy8nzDgBwbEJl7YvueQSPeN47LHHpF69egnvNRckloDr\noChXrpwwXBEJIRLl66+/Fo4HuLF9Ir9RqzictXBFlANO3ktAGbJPAq53HwQFZwpcwLKICrJkAWHd\nw0+uVxhAhEvEnu+ug8JaeaSm05A/JeA6KKpUqaIlQbW3IX9KwHVQUGfBruKnn37yp0RMrsR1UHDK\nyNbCgMK/6HMdFBQFjXZphmfInxLwBBQ1a9YUxuM25E8JeAIK6icMKPwJCObKE1DQ6JZL3D///LN/\nJZPDOfMEFFzJJC1ZsiSHRe/fonsCCi5gVapUSWDJ7V/J5HDOPAEF5V2/fn2tCAuXPXUZZqoaLhFv\nvnsOCtpPUDNKjSeVYtR2GvJWAq5rSanVZPjlefPmaZW3ZXoH1xUtCTgDeSsR83RxBRTsFh5//HH5\n+OOP9eCSqm/aQ1jRdHmeRINeAwrvUelK90EVNyvemm2wVbAAES4CHjegCJeIN99dAQWL9uSTTwpX\nMgmQWESgGFDEko57x10DBbuGZAKrG1C4V/mxnuQaKJiBunXrSp8+feIa18baNipWAcxx+yXgKiiY\n/YceekiDgwPNaGRaimhScfeY66DgmIJbPMUyxTegcBcA0Z7mOiiYidNPP137bUT6khIwpUqVipZP\nc8xFCXgCCpbvzjvvFMaqCu9GuKJpyHsJeAYKthLvvvtunpACZpDpPSCYA89AwYfTS4whiSyyAqRZ\nv82nNxKIPgVwMS833nijIMCZIDCaduyx9hbjHmL8YxASxsGivyhjcDL+RLdu3XSIRYZD4s5CJ554\nolbF87N69eo6JKOLRci6RxVgDDWvSkUA0J/0s88+k7feekub/rPySexe6E1GlwAOPhnCgH8cg9C7\njPuF8FpGvCFw6LFO4qzmlFNOEcbAom/phRdeqGNsmh0DtHiS+ucqKIg/7h02ZswYGT9+vN6IljMO\nLmrxjef5Rx55RActIRjCB6GJSsMAKIxZQdtP6lj4N3v2bN26MHQBdyFq27at9mhnt2UojgTYUjhN\nCE6m7rvvPgVrK7ZKCupy1atXLx1LE2946PGo0NB3u76gy1EY0KouXbooAE8/v0GDBmrQoEHqt99+\ns+sxWZUO307HaNy4capFixZ6q0k4AKnevXsrvMGOPS9RwgiwptBVKYxJFIKnKETTUbfeequCoU+i\nW3PqvCOgQNegzj33XP1WIt624m+ozn0l2B07dqiXXnpJYWCq0IUpBGc14DhSQ7aCYvny5aply5Ya\nDAyTjGAkvgJCtMwwhDO7F6yyKvi46lDOGJ9EuzRnjtkCCthBqCeeeEJBPa4waFSIRxU4ARIcbDk4\n7mBXx9jhuUoZg4IDOWw6qzBdVP/+978VhRtk2rx5s+rcubMeBz3wwAOK45Bco4xAgdBECjGsFNYE\nPB1AOlFpWDfRA1ECHsbGTjzCt2mmDQpus4D5v+rQoYNCtDvfFjCTjC1btkzBQ16PN+Aln0lSgbo3\nLVAMGzZM79Vx9913+25WYbf0sVqqsP2EwhK6gqOS3cn7Mr2UQcF5PkfpiIPpywI5kSk4Qyvso6pb\nDET2c+IRvkozJVBwylmyZEl1ww03KGzN4KuCOJ0Zthinnnqqatq0aeAH04lklTQoOAqH/6eCkklB\nIZUo3aw8/+233+pxFNwVsrJ8VqGSBgU8vHQrQT1GLtOAAQMUFHVq4cKFWSuGpLSkVE1zN0C6/mHz\ntjjqtew/BSTI+eefr7W6kyZNys4CJwP37t2761U+2DAkc3nWX4P9UPVS/ueff56VZU3YfVC1TW0i\nm00/EPYgVX4AJ4x3FHYb8INIbM9DQlC8/vrrClZLCpH3bX94KglSDc+BLu0xvM4L8z1kyBA9NYf1\nWCrFCMS1CQ13P/roI7nssstS3tPLzs6WIZu55aSfNnhp3769NhnkltzZRglBQfM5zM09LTcj9PIP\nS86e5iP84dzhiCGaZsyYEX44K77HBQXjTzHyDO0bDeWXQKNGjWTu3Ln5TwT8SFxQWHEuK1euHPBi\nOpN9uhRA1e5M4h6mGhcU1oaxxuk3eg3RecmSUfQrgnk0LiiCWSST60wlEBcUVguRjW9DpoLj/Rxv\nWTKyIz2/pBEXFNYW0evXr/dLfn2Vjw0bNmTlHmZxQcEpIPtNbiprKL8EOF2HK0P+EwE/EhcULBun\nXfT39AMx8j/J8jf1Mk/ccJf7qcKG08tsOPLshKCg/yVX7awKcSQXCRLltA+W4toHlZcybtbkyZMT\n3OXsae68jDVrufTSS519kAepJ1Sdcw9ROvs+88wzOvqMB3n05SObNWumu9bwbbl9mdF0MpWMhsao\nzvNKKdtV5wlbCgLNGNn89bqxyzBGNkdeEroF0mjXmONlvzleQnsKq+E0hrtKGcNdCw1hn8bE35j4\nh8Hhr6/GGcg4A/2FhrBvxm0wTBhZ+DXpMUVk2UeOHGkcjCOFkiW/0wYFy29CEWQJCiKKkREomJYJ\nWhIh0Sz4mTEoKAMT3igLkBBWBFtAYaUXHggNirTABEIbOnSoCYRmVSI+bQWFlW4QQyYyvIKJp3m4\nBh0BhQWOoARXzfWle6u+rE9HQWE9JNkwzNb1dn6aMMypSzMpLelfOsLMviF7MQO2M+I+I+/Xrl3b\nBGzPTMwZ3+0qKCJza23tMG3aNFm0aJGOvI+YUvoya2sHBHnXWztwa4ZoWzvA2VjvC2K2doiUbvq/\nPQVFtGzH2wSGjsbcsgGhnsUCCbeEIHD4R48tOiHTz9NQ+hLwHSjiFeWDDz6Qjh07chwU7zJzLkMJ\nJDTczTB9c3sAJWBAEcBKczrLBhROSziA6RtQBLDSnM6yAYXTEg5g+gYUAaw0p7NsQOG0hAOYvgFF\nACvN6SwbUDgt4QCmb0ARwEpzOssGFE5LOIDpG1AEsNKczrIBhdMSDmD6BhQBrDSns2xA4bSEA5i+\nAUUAK83pLBtQOC3hAKZvQBHASnM6ywYUTks4gOkbUASw0pzOsgGF0xIOYPoGFAGsNKezbEDhtIQD\nmL4BRQArzeksBx4U3OcMYZacllNOpR9YUNDn9P7775dTTz1Vxo4dm1OV5nRhAwsKbo+JQCOCLa6d\nllHOpV8oqCXmjjwIDR3U7Ps634FtKXwt1YBnzoAi4BXoRPYNKJyQasDTNKAIeAU6kX0DCiekGvA0\nDSgCXoFOZN+AwgmpBjzNQIPC2ivVD5vXBhwHebIfWFB8+umncvfdd+vCfPjhh/L6668L9SCGMpeA\niY6XuQyzLoXAthRZVxM+KpABhY8qwy9ZMaDwS034KB8GFD6qDL9kxYDCLzXho3wYUPioMvySFQMK\nv9SEj/JhQOGjyvBLVgwo/FITPsqHAYWPKsMvWTGg8EtN+CgfBhQ+qgy/ZMW3CrFNmzbJY489lkdO\n3F9s8eLF0qJFizzHuX/YU089leeY+ZG+BHwLCu4TVrlyZSE4jjoqdoN28OBBue++++T5559PXwrm\nzjwSiC3tPJe5/4NbUNIDrFChQsKKj/XHnF177bXuZzCLn+jbloIyZ1dx9tlnxxX/ySefLKtXr457\njTmZmgR821KwGGeddZZUr149ZomOPvpo6datW8zz5kR6EvA1KFgkVjq7kGj0559/yjXXXBPtlDmW\ngQR83X2wXD/++KNUq1YtahHZknA7bEP2SsD3LQXjT9SvX1848Awnth5du3YNP2S+2yQB34OC5eQs\nJHJaytlI586dbRKDSSZcAr7vPpjZzZs3S8WKFUN7nBMgjRo1kmnTpoWXxXy3SQKBaClOOOEEad68\neZ7Wgq2HIWckEAhQsOhdunQJSYDjiw4dOoR+my/2SiAwoLjqqqtCLcUll1wiZcqUsVcSJrWQBAID\nimOPPVZatWqlMx7eaoRKYr7YJgHfDDS3bNkiS5Ys0X9cm9i4caP+o0Js9+7dOgrenj175MCBA1Ks\nWLHQX+nSpYVaUv6deOKJUrNmTTnzzDOlVq1aUrRoUdsElUsJeQYKAmDKlCn6j7MIVj6J3QKXtlnB\nnHGwskuVKqUruGDBgjJ8+HA9vqCnOcMlbtu2LQSg9evXyw8//CD79+8XXktgXHjhhdKsWTP9xwGr\nocQScA0Uhw4dkhkzZsjo0aNlzJgxsnbtWmGXcMEFF+iKq1evnn7DCYR4tHPnTjnmmGNiXsL1ixUr\nVugWZ/bs2fLNN9/IggULtJa1YcOGwrFJ+/bt5ZRTTomZRs6fgN2Co4TwAOpf//qXgjZTQdgKb696\n9NFH1dy5cxUq0NFnW4nv2rVLffzxxwp6FFW2bFmdD0xx1fvvv6/QqliXmc8jEuCCkCOEt1VhGVpB\nk6nQJah7771XLV261JFnpZIolGhqwoQJqm3btgpdjEKXop599lmFcUsqyWT1tbaDAt2CBgMFXqNG\nDfXWW28p9P2+FCLGIOrBBx9UJUuWVOXKlVP9+vUzLQdqyjZQ8A187rnnVIkSJRS0mmro0KEKMwVf\ngiEyU5j5qEceeURhVqMwe1FffPFF5CU59dsWUCxbtkzBQkoLtU+fPgozg0AKERZculvh2Ofmm29W\nmAIHshyZZjpjULz55puqePHi6vzzz1crV67MND++uB8zJD0OOuOMMxRMAn2RJzczkTYoMMVUPXv2\nVNBDqIceekix+8gm4tioadOmerwxceLEbCpawrKkBQpsqaBgBqcKFy6ssJiU8CFBvYDlxJK6nkG9\n++67QS1GyvlOGRRsIWBSr9+gL7/8MuUHBvGGXr16KdhwqFGjRgUx+ynnOWVQsMtgCzFp0qSUHxbk\nG+644w5VpEgR9dVXXwW5GEnlPaVl7hEjRmgTuPfeey/nTOEgTenUqZPexK53795ajU9FHfUsXMLn\nH14WraPBwFuwcipY+9D6G/qm8FxQKGlQrFmzRurUqSPXXXedDBo0KCjlszWfWC6Xc845R+ttsOCl\nFXVoPTRAaCLI7auoqKM297fffmMrrJ/Pc3SBpPU572/cuLE0adJE329rBm1KLGlQtGnTRlatWiXz\n58/PaZU0dDZCxdrbb7+dxxossj6o4t+6datQc8tN8Ki9pTsC5UeFHa3RMbuRjh076hbIV0ZDyXQy\n0DRqJRLiYSdzedZfw4WtKlWqpL1IBzMBNWzYMAVA6BVgrqTecsstCuDxheySGmhSo9iyZUtfZNgP\nmYABkF69RTeacXbQzaiBAwdqLTIHsgi/oDgV9pISgoKrlFygGjdunJf51PoIhBxQCDmgqMjymrpC\nA4zxgW3ZoAqfZWOrcd555ym4NeRJm6qDzz77TGt0p0+fnrLZAVunZGdOCUHxz3/+U8EKylPlVt++\nfRVM7NStt96qKlSooNcMvAbp1KlTdZf6v//9L0/lZfqDeiQYAKnTTz9dYUyikyNAeGzw4MEKOzer\nBx54QF1++eVJAQOBXhRfJoLtrrvuSip7CUGBkbKujKRSc+AiDG61MYyVNA1mYLHleXfGRTwa7Lzw\nwgtW1mz7ZEsIM0TVunVrXfGYqSgM9EPpU/tctWpVrfYPHYzxZc6cOYrAxUDYHlCwyWI/N2TIkBiP\ndP7w999/n+8htKCCWV2+424fuOKKKxT8Txx57Oeff64rkl0KK/STTz7J85zHH39cD1KTMQ5i15QK\nKOKa+GM8oRdnOLf2itCM5nk0F4k4NcbKap7jXvygXGBN5sijGdeLaxn//e9/dfpc4wgnWqxzPQRW\nZOGHbfkeFxScZ5O4MucH2rBhg14boB8pDX69pvLlywtdE5wijBv0QhnTjzRo5rNJXP+wm6JHAzny\nFGvjNj8srKA5FegfZPny5Tp3BAisu+yWR0rpHXfccWLJKKUbk7z4pJNO0iukdFeIXCbnUjrJco1I\nMsmkLovbUsC0TifCZsprwjqJYHyh41vVrVtXsPgj48eP9zRblIslIycyQt0KARGN6MpAwmws2umM\njsUFBZU6JCebyFRzT+USAUGaNWtWqrfbej27V0tGtiZ8JDH6ybCVJgCoeAsn6mFIsA4LP2zL97ig\nwFKufogT/VYmuacg6DnmxFuSSr4oF4LUCWJMDjpOnXvuuTr5devW5XmM9aK6Dgq+BRz9YwUtT4a8\n/oEFHNmxY4fQ+9xLolw46E2GOGtKljD3lH/84x/CMctLL70k1MRG1gEVa+xG4UaRbLLJX5dn8hvl\nB5U/XHb1iqiEe+edd/JYVj/zzDMKwvIqS/q5MCXQc/9ESkIa/t5zzz0Kb3xS+eXCFFdu6URlLUtz\nRbJ27dqKC2Yk+tHQpwbAyJMmuhv9HExj8xynlx4QkfQiZMIVTWsRxSvvLhaQzjrwH9WFogsBHJPz\nFNqLHzC0UZgWRlVecdWVS9Lwj9WVQd0RVz8TEbojReUjvOUV/G1DlxMMdFriCueAAQPUww8/HHVB\nkYuMrHx44ofUEvSGg3GQPs78Ml/Ug8SjhKBghtBvqjvvvDNeOo6eo88p0W69KY4+LInEqcWk6pym\nieHEN/XGG2/UlUqbToKBlcQ/AjsWYbyg06KZI90KIlsA6z62IpRDPKKuo3v37vEuSXguISiYAptq\nLnevhrOMIaXfVsqD9g9UUPXv31+ddtppuvLZ7FtACP/k8XDC+oaCeWPIpxWLU1qPwiXpTAj7viv6\nrWRCSYGCbwYLzWYo1wnxMHRXQN3LlVdeqZ2U6TcbDoBY32lYc//99ysquGB5pf8uvvhiDQ47bCho\nm2GNQzKpp6RAwQdQVc3C0n0/V4mDS4ZSYNdAWbBiYwEg2nFejxmD+vvf/66BgBmUL0WZNCiY+x49\nemi1NdXZuUgc7LGyadORDihosRUESgkUnApxRI3wQ/ksg4JQ2EzyyFE8xwVUWZOo0ufUGCGiNUDY\nelgtSLRWgsegr8kkC67dmxIomCuOfhlqgODgYCkXiIbLdKLmzCIacYr36quvasMfdhGcdUTrWoLi\ngJ0yKCgUFo5TMk6f6IibzTR27FhtyoY4WUk5USMmlx4vcFDOWB1sIayBaFA82NMCBUFAkzHaTdJs\nDIqprMQFp5rsEjjvTyc+F2cUdK/kWIxTTprGBYHSBgULx+4DAU91U0njWr8sLmUqeK490DCWXQCj\n89hBlI0d00478pIojYxAwcRZWNoRchDGeA5BaSJjCYZhmTi7YPdIU/pcpIxBYQlt4cKFOpoN3y5G\nwmMcqSARYm2qZs2a6e7itttuy5lBdLQ6sg0UTJytxmuvvaYjzXGtnxFu2BT7mebNm6fN5zkgZIim\noPT7TsrUVlBYGaXZOftihiGkEwpN8mfOnGmd9vyTrgtcckaIZj07aNCggececJ4LJSwDjoDCSp/g\n4PydS7t8E2kT8MQTT2jnFOsatz6paOICFJeYqcZmN8dp5uTJk93KQmCek3QoAlRqRsQ42bStxLxf\nu+czNvZFF12k43IzqLrdsbIZCgDjHB2b2woMT7tGmrcxNje3h4g0m8+ogFl0s2ugsGSG10XQb2sn\nFlYWwcJAH9yiAS2JDtpOEzPaYPKPFcco/uiGdFwMzHK0ESsj+PPPiuJPU3faMcIXUzvo0BUAU0Ch\nfwTjQBCAjLFBs3lD8SXgOigis0MrZQz2dEAPa78PeoDRcJVve7JEPwhuB0GbUnpP8Y87A3B7B0Op\nScBzUMTKLmYyAisi7exC/wqrZSBQaMhqtRw0bmWLwm0iDNkjAd+Cwp7imVTSkUBcv490EjT3BF8C\nBhTBr0PbS2BAYbtIg5/g/wckxmwWCbfEBgAAAABJRU5ErkJggg==\n",
      "text/plain": [
       "<IPython.core.display.Image object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "split wasn't perfect: gotta start over\n",
      "returning counterexample of length 5:\t\t10010, this counterexample is rejected by the given RNN.\n",
      "equivalence checking took: 0.08149300000000892\n",
      "obs table refinement took 0.003\n",
      "guided starting equivalence query for DFA of size 5\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAQMAAAGTCAYAAAAst3eIAAAAAXNSR0IArs4c6QAAQABJREFUeAHt\nfQm8VeP6/1MaNEpoNjdIoVGSIVdClBQVUUkuEhkyJYR+fyJj5QrdrgakjI00U2iSm4SSZlFJlAap\n9//9vlrn7nPOPufsYe291/A8388+Z++113rXu77vWs9+h2coZIx5S1SUAWUg9AwUgjIwoWdBCVAG\nlAEprBwoA8qAMkAGVBnofaAMKAOWAVUGeiMoA8pAOJXBATkgrYBCHsar8qrenspA2hkokvYzZviE\nfaWvzAReBsoBXpNZMktuAeoATQEVZSBdDIRqNeEteUs6AiOAboAXhT2Xy4DFwCKgCqCiDKSDgdAo\ng6Wy1P7S9pAe8jzgZflNfpMmwOHAbKA4oKIMpJqBUCiDX+QXaQwcC0wDigBel2/lW6sQrpArZDig\nogykmoHArybsl/12aMDu9zjAD4qAjX4SMAbgkGYooKIMpJqBwCuDPtJHPgXeBY4E/CSXyqXyKHAH\n8DGgogykkoFADxNGySjpArwOXAX4UYwYDBSukLkAJxSPBlSUgVQwEFhlwAfnbOBW4EnAz7JTdtrJ\nz2JSzCqFElLCz5ejdfcoA4FUBptlszQCagOTgUMAv8sqWWUnQWkwNRpQUQbcZiBwcwb7ZJ/tVvNX\n9E0gCIqAjX4iwOshngFUlAG3GQicMugtvWUJ8B7AdfogSUtpKY8D9wDTARVlwE0GAjVMoE3/P4Hx\nQDsgqHK1XC0fApwXOR5QUQbcYCAwyuAz+UyaA/zVfAwIsuyW3dIM+Av4aMdHsn3jdtmyZYt9/f77\n77Jz5075448/ZO/evZYGxq855JBDpGTJkvZ12GGHSYUKFaRixYpy9NFHCz+rKAOBUAY/yo92wrCh\nNJQPAHokBl3Wylp7zYffcbisfG5l1uXygS9durSUKlVKihUrJoUKFZLChQvLvn37ZNeuXfb122+/\nyYEDB7KOOfLII6VGjRpSr149adSokTRt2lRq166d9b2+CQcDvlcGe2WvnAtsBxYAZYGwCP0WWqxr\nIT2395S+FfoKH+oiRQo2taYi2LZtm/z888+yevVq+eGHH+Tbb7+VJUuWyNKlS63CqFatmlx00UVy\n1VVXSfPmza1CCQuvYb1O3yuD6+V6O0dARVALCJsMlsFyOzAB4LJjssIexIIFC2TGjBnyzjvvyH//\n+187lLj99tvln//8p+11JHsOPd6jDDAgql9lsBlsCgETgDBLN9PNHAZ8B7gt33zzjenVq5fB0MNg\nnsGMGjXK7VNoeR5hQDxSj7irMdvMNkWAx4Cwyx6zx5wO1AZ+B1IhmzdvNjfddJPB/IO54oorDCYo\ns51mz5495sMPPzQDBw408+bNM/v378/2vX7wPgO+tDNYJ+vkSoBBQB4Awi6Md/AO8CtwDUB/Brfl\nqKOOkn/9618ydepUmT17tlxwwQWye/duexooCjvhuG7dOunevbu899570qZNm2yTlG7XR8tLAQPe\n11fZa7jL7DINgLrADiBdwl/GKVOmuHa61157zbWynILmmrmmGPAQkErBJKMpX768ufbaa20P4Kyz\nzjJ4+LNO+ddff5ljjz3W3HvvvVnb9I33GfDdMKGz6WwOB74H0iW8uVu0aGHwy+jKKWfOnGmqVq3q\nSlk5Cxlmhtl5lHfNuzm/cvXz+PHj2f0wL7zwgv0/YUL2eZuHHnrIYHnTwObB1fNqYaljoOB1qBT0\nRhIt8ml52trm0/mItvpuCiiWOXPmyJdffmkNdE466STbFabhTufOnWX69OnWUIfr9uwCV65c2XaT\n2WX+4osv7DH4pRQ85FnV+vXXX+WNN96Qnj17CnoVdtmuYcOG0q5dO7v+P2zYMKlSpYq0bt0665hk\n39AC8wvgWmA+cDKQCmnfvr21SXjxxRdt8aecckq209StW9caPk2ePFmuvPLKbN/pB28y4Js5A9ri\n3ws8AdBG323p16+ffP/998IlNBrd8DMFE2N2vZ3v+aDXqlVLSpQoYa38aKjD9/fdd5+g9yDNmjXL\nGkdjGCBcq+/du7cMGTJE7r//frsf1/dPPfVUKV68uC2LFoBuC5cbTwM4p0L7i1RJ27ZtZc2aNbZ4\nKsdIoYUjZcWKFZGb9b2XGUhdp8O9kjk3cATwDyAVAiMcA4MdM2vWrKziBwwYkPUevQXbFR4+fHjW\nttGjR9uZ9Z9++sluc/bBGn3WPuhR2OOwXm+3cZmOgofIQAnY96n6s9FsNMWBa4BUCZcZ0VMyMHXO\ndQrygPve3HLLLbm+0w3eZMAXPYPSUto6IM2Tebbr67ZyZdefv/gdO3aU999/3xbfp0+fXKfhfo7Q\nMm/ZsmXWvp+9Bw4xKCtX/s80mEMAymWXXWb/c+jhSGRZzjY3/ztxE5mDIVWyY8eOPC0TsbRoT1up\nUqVUnV7LdZkBXygDXvMA4HyA3og/AW4Lu/Jly5YVdn0xWSjbt+fuXkc+wLT3p6MPJsrkmWeeybLl\nj7T55z4U539knSPLitzuxnt6bf4/gArhDCBV8sknn8gRRxwhfPAdpyjnXFQUlJNPTs2chXMe/e8e\nA75RBoWRI5bRgksB7YE/ATeFTjqcCORkHycFGzRoYO33I88R+QDTpr9+/fpy+umnS9++fQVLaZG7\nFvg+sqwCd45jh6/kK6SH6WazMtFUO1Wydu1aa658xhl/K5v169dnO9XWrVvtZ1UG2Wjx9AffKAOy\nyHRo7wO84XsBbgl/1TD+lTJlysjQoUNl0qRJsmnTJnuz8xzOg+t0fbmtf//+1hPw0ksv5ce4DGxY\nXmRZtgAX/myTbdIWoPfms0Cq5M8//5QuXbrIMcccI1hatJOhsDrMdrrFixdbL8iaNWtm264fvMuA\nr5QBaWRcQ0Y9ZiCTfwFuCKZz5KWXXqLNhS2uZcuW1gOQXoAUZ6b8s88+s/vQs4/xAqgwuHTGX0Fn\nie3HH3/MGmJwH8ovv/xi/zt/WB4mHq234KpVq2xZzneJ/md+iE4Aw74xP0RRIJpw1WPatGl2qTPa\n9wVt4zVxWZEP+9ixY22PCL4L8tRTT2XxxzkU2B0IJlyjDpEKOod+nyEGvDmvWXCtHjGPmKLAJ0Cy\nArNagwfUdOrUyYwbN87gxjY0momU888/386On3feeQZdZPPpp59aKzssEZrLL7/cwBTXwIbAHH74\n4WbEiBHm1VdftYZFaFbToUMHM3/+/KziuGoBV2NTrlw5a7ST9UUSb+4yd5kSwGIgp+CX3FpPwlTY\nYF7EXgeWQ3PuVuDnuXPnGky0GswTGL53hKsxtDZEL8leD5ZRzciRI52v9b9PGPCdBaLD6wFzwLQF\nKgLrgWQFrrsGwwX7oEcrizf8hg0bsn2Frn42CzvuwzJiEUxQGkQlimXXAvcZbUbTHQF/R2fty3pM\nnDjRdO3a1XocUikVLVrUKgIqogcffDBr34LeUJHBUMoeC58Eq/iiHUNLTWepNdr3us3bDPhWGZBW\neuidDDQCdgNhFPYE2CO4E6Dn4AcffGBo30BT4EgFwPfOCxGQzCOPPJIvXQh2Yj0QMbFqj8NkqYED\nUr7H6Jf+ZsBX5si4mbNJGSljoyCfLqfLjcBrQJgEUQ+l7Z62UmNqDfnxrR+l/PvlbZQiRjvi3ACF\nwUqiCXoJdjNuXzt/sXz5cvnqq69sYBMMAYSrA3BGsqbTgwcPFjgjRStGtwWIAd9HOmJbTAUuAei7\nwKg/YZA1G9ZIk/uayJZ3twgcOe2KBx/sWISKgKbS/M+H3nFFppsyfSfOPPNMwRyJNGnSxPpcxFKm\n7uN/BnzdM3Dov0guskY2d8vdcirwDyDoMqjaINnx5A7pfWpvmfjKROtXwYc7r55ATj5oHXnhhRfa\nkGYnnHCCtcCkEZVKiBnw9ygne+07mA7Wh2G1WZ39i4B9Gm6G2wnDt8xbWVe2cOFCG54MYc/tGJ/+\nArito76gNAy6/lnH6htlgAz4zs4gP709QkZINYCGNwgKnt+uvv2Obsk9gb4Aoz05whDnHNszf8K7\n774rrVq1sl18KIUsoylnX7S7HSI4n/W/MkAGAqUMkCLETihukA3SHQiabJJN1jeDPhp5JYrhUIH+\nFVhVsKHQn3vuOXFiDfA7Cv0nnPdB40ivJ3EGAqUMSMNxwFsAnXUGAkER+mLQJ4MenK8D9NUoSOhE\nROtAhjv/+uuv5Y477hBOElIZcMVBRRmIZCAQqwmRF+S8f06ek7uASQAnGP0uN8gNMhbgMIEm2YkK\nFQGjNnGy8LTTTku0GD0ugAwEVhmwrboATC6yEKgO+FXog8G4BMws3QZQUQZSwUCglcEe2SNnA5xM\n/BygkZLf5BP5xMZx6Cf95CFARRlIFQOBVgYkjZOJdOk9E2BuAT8lZfVz3VN1w2q5qWOg4Fmo1J07\nLSVzqZGTiZw7yGsGPi0VifMk7NVcDhwJjAT8pMTivFTd3SMMBF4ZkGcOFZ4H+gNM2e4HYcjz7wEG\nc/Hj8MYPHGsdszMQmvWlm+VmWQIw/ViyM/LZKXT/E1dCxgDszfh54tN9ZrTEVDIQip6BQ+AQGSJ1\nAVoo/ga4JcyR4JbMlJnSB2BA0yAsibrFi5aTegYCP4GYk0Ja8TUCfgTyFeYUZdT0tngdms+ei/Bd\nB7x+yGefOL/qKB1t5qg4D9PdlYGkGAjNMMFhqbJUxm/vTFkK5CcLpi6Qpzs/LcN+HCblDi2X566v\nvf6aTFo9SQZ8PkBqnuFO8E+6Y6soA+lmIHQ9g1gJvuaaa6yvv5McJdpxtOajJR8Dot566602UnC0\n/XSbMuAHBkI1ZxBrgzAUOKP7MgpwfkJF4eQHGDNmTErCn+d3fv1OGXCTAVUGUdhkKHFmBGK25Pzk\n9ddfz/L+Y0JVpFrPb3f9ThnwNAOqDKI0z9tvv20zJTE0WF7C3sObb76ZFVmIXoDsHagoA35lQJVB\njpZjIFHGAihoiPDhhx/atOzO4Txu/PjxuXIOOt/rf2XA6wyoMsjRQkiOYjMgMUBIfoKU7LliAjDb\nEFOzqSgDfmRAlUGOVpsyZYpUr15datSokeOb/33kQ8/U7U44cucbDhWoJFSUAT8yoMogR6tRGVx8\n8cU5tmb/SEXAOYOcQuWALEZ28jHnd/pZGfA6A6oMIlqISVMZIqwgZcCMzYULR6eO2ZUZkFRFGfAb\nA9HvaL9dhUv1nTp1qpQoUUKaN2+eZ4nMqMylx/xSqiPpaJ7H6xfKgFcZUGUQ0TIcIlARUCHkJVwx\nyE9olYgsyzZkeX776XfKgNcYUGVwsEWYS2DGjBnSsmXLfNuIv/r59Qp4MBXCW2+9lW85+qUy4DUG\nVBkcbBEmHf3111/l3HPPzbONNm7caBOTcr7AeRUqhBhEeDmfnf+qDPKkUb/wKAOqDA42zCeffCJI\nTZZv+PCqVatai0P2DJzX2LFjmdY+67OzPT8HJ4/eC1qtkDOgyuDgDfDxxx9Ls2bN8lwlCPl9opcf\nAgZUGUQog3POOScETa6XqAxEZ0CVAXhZuXKl/PTTT6LKIPpNolvDwYAqA7Tz/PnzpVixYtKwYcNw\ntLpepTIQhQFVBiDlyy+/lDp16liFEIUj3aQMhIIBVQZo5iVLlkj9+vVD0eB6kcpAXgyoMgAzqgzy\nuj10e5gYCL0yWLt2rTU2qlevXpjaXa9VGcjFQOiVAb0UaUGoyiDXvaEbQsZA6JXB999/L5UrV5bS\npUuHrOn1cpWB7AyEXhmsXr1ajj/++Oys6CdlIIQMqDKIogxogDR79uyEb4dkj0/4xHqgMpAEA6FX\nBvREdEKib9myRfr06SMnnHBCQtGKkj0+iXbUQ5WBpBkIvTKg23L58uUtkWvWrJEuXbrI7t3Muhq/\nJHt8/GfUI5QB9xgIXeLVnNQxE5KjDBo3bhw10GnOY/L6nOzxeZWr25WBdDAQ6p4BYw8wjVq5cnln\nWU5HI+g5lAEvMBBqZbBv3z7bBsWLF/dCW2gdlIGMMhBqZcCeAeWQQw7JaCPoyZUBLzCgygCtoMrA\nC7ei1iHTDIRaGWSafD2/MuAlBkKtDJz8CLt27fJSm2hdlIGMMBBqZVC0aFHhS5VBRu49PanHGAi1\nMmBblCxZUphV2REaIVH27NnjbIrrf7LHx3Uy3VkZcJGB0CsD5krYvn27pZTp1Xr37m3fv/fee/Lq\nq6/aQKmx8p3s8bGeR/dTBlLBQCEkADGpKNgvZZ5++uk2KvKgQYMSqvK4ceOkQ4cONpFKQgXoQcqA\nRxgIfc+gYsWKsnnzZo80h1ZDGcgcA6oMoAzocqyiDISdgdArA7ovr1u3Luz3gV6/MiChVwYnnnii\n0PWYadRVlIEwMxB6ZcBAJnv37hUGOVFRBsLMQOiVAXsGlFWrVoX5PtBrVwZ0mFCpUiUbz2D58uV6\nOygDoWYg9D0Dtv4pp5wiX331VahvBL14ZUCVwUFlsHTpUr0blIFQM6DK4KAyWLZsmVoRhvpR0ItX\nZYB7oGHDhvL777/LihUr9I5QBkLLgCoDND3zLB566KHy+eefh/ZG0AtXBlQZ4B5gTIMGDRpkKYOt\nW7fKqFGjpGPHjjJkyBC9S5SBUDAQ+rwJTisz3+L06dOFuQ8WL15sN9Ohs1mzZs4u+l8ZCDQDoVUG\nDGjCh3/ixIny/vvvC1OjsYfArMyOMFBqmTJlnI/6XxkINAOhVAZMnFKzZk3rrUgF4ORPcP47Lc5Q\n6qoMHDb0f9AZCOWcAR/woUOH2rbNqQByNrgqg5yM6OegMhBKZcDGbNeunVx//fVSpEj+nSNVBkG9\n9fW6cjIQWmVAIl544QU55phj8k2iosog5y2jn4PKQKiVASMjjx8/Pt+2VWWQLz36ZYAYCLUyYDvW\nr19fBg4cKIUKFYrarKoMotKiGwPIQOiVAdv0zjvvlObNm0edP1BlEMC7Xi8pKgOqDEALewVjxoyR\nUqVKZeshcHKxWLFiUYnTjcpA0BhQZXCwRStXrmxNkCPTSHBOQUUZCAsDqgwiWrp169Zy8803Z60u\nlC5dOuJbfasMBJuB/BfZg33tUa/u6aeflhkzZlh35pzzBQfkgGwGNgF/ALuBRQBlElDiIMpJOakC\nHAaoKAN+YSD06dWiNdTirxZLkwZNpFr9anLJgktkGbAK+Bn4C8gm/MgcrVE6ESWlpFQFTgLqHkQD\naWA/ZytDPygDHmBAlQEawQALAP66fwx8Dux9Ya8UmVJEmkxpYh/jmlLT/trzF78yUAZgT+BQAInd\noQ/+BnsL24AfD2KDbJDlABXKCuBPoAJwDtAcaAMcDagoA5lmINTKYL7MlzHAuwAf2uOB8wA+qMSc\n/8yRbt26udZG+2SfLAGocIg5wA6gMdAeuBagolFRBjLBQOiUAcf6o4GXgC+BOsAVQDvgVCCdwl7C\ndIDKiPgNuAy4CWgBqCgD6WQgNMqASmAoMAjYCXQEbgTOALwge2WvjAeGAZ8AjYD+wCWAijKQDgYC\nrww4H/AK0A/geL4XcBdwJOBVWSyL5VHgA6AJMBjgUEJFGUglA4G2M+D4vClwC3ANsAZ4HPCyImBj\nNwTeB74AigPsvfQEtgMqykCqGAikMmBvgMMB/qoWA6gUngGOAPwk9aW+nWQcKSPlHaAe8Bmgogyk\ngoHAKQP+el4K3A88BnDGnmv8fpbO0lm+AngdXOV4ClBRBtxmIFBzBhtlo1wEcJ2fv6TsGQRNnpan\n5R6Ak59DgMKaOzdoTZyx6wmMOTItBGkjUBag0VBQDXk4+XkCwN4CTaPfBIoAKspAsgwEomdAM+Fm\nAH0BZgD0DQi6cPmRvSAukf4bUFEGkmXA93MGXC5sBbC7PBUIgyJgo58NjANGAQ8DKspAsgz4Xhn0\nkT7WiYiK4CggTEIlSBuEAcBMQEUZSIYBXw8T6FjElYOxQAcgrEJzas6TcMXhcEBFGUiEAd8qAzr9\nnAzQbPcNIMzyq/wKn8qa0g3QZccw3wnJXbtvhwm04V8PPAGEXdgbeAjgkGEdoKIMJMKAL3sGtDCk\nuzE9/J4HMiUzZ86UyZMnC+MndurUSapWrZqpqqCftE+qA1cCtL5UUQbiZcCXPQNOlq0FaHiTKWGu\nhd69ewuTuA4aNMhmZpo0aVKmqmMDrHSX7nZ1gYpBRRmIlwFf9gyul+vla4CTZpmQH374QRYuXCgd\nO3a0p9+5c6dUq1ZNGjduLNOmTctElew5OUQ4FuDKyoWAijIQDwO+7BnMlbkZDf7BzM2OIiDZjKJ8\n+eWXS9myZePh3vV9j5FjpAZAgyQVZSBeBnynDH6RX2wsQVocZkpq1aqV7dQHDhyQVatW2cxM2b7I\nwAfyop6NGSA+AKf0nTLgXAGFS2lekI0bN8q1114rTZs2lWbNMqegHC7Ii8ORs03/KwOxMOA7Dxf2\nDCheiE0wffp06dWrl3z33Xe2TlQMo0ePtu8z9YeBW7YCKspAvAz4rmfAWIaUUkCmpUWLFvLtt9/K\n6tWrpV69ejZfYyZXFBxedsmuTFOj5/chA75TBuWlvKWZVndekeOOO84qAtbn888zs8LhcMFYDmqS\n7LCh/+NhwHfKwBke0JffS3LyySdLlSpVpFKlShmt1hbZ4okhVEZJ0JMnxIDvlAGt7BgklHENvSRb\ntmyR7du3S8uWLTNaLfLi9zBvGSUwxCf3nTKgImC+wnlApmTq1KkycuRI2bXrf2Pz4cOHC60Sa9So\nkalqwUjbyKfAmYCKMhAvA75bTeAFng+MAPYDhwDplvXr11ubgltvvTXLJ6F58+ZyzjnnpLsq2c5H\nYyyutpAfFWUgXgZ8aY78vXxvLe0mysSMZRyioRGHBhUqVJBChQrFy3tK9qcLM2MaMAmLijIQLwO+\nVAa8SAY/ZSDQaYCK2JzPnE+hxyITrqgoA/Ey4FtlwCzG5wLqlPN3k9N5i0lcmfad8yoqykC8DPhW\nGfBC2wAMkc5u8aFAWGWBLLBp5P4j/7Fp3cPKg153cgz4WhnQBv80gDkEmGE5jLJDdiAJW305EWAv\nqRCgogwkwoDvlhYjL5K++y8BLwJMJhI24VIiA5r8DrwGqCII2x3g7vX6cmkxkoJO0gmd5AXSFaCT\nTgsgLHKb3CYTAPYIKgEqykAyDPh6mOBcOH8hmXL9g4PgSkPQ5V65164cMEw8Q6WrKAPJMuDrYYJz\n8ewec/KsNcCUY0EOnc74hl2AZwEODVQROHeB/k+WAd8PExwCiiIk6BiA3WVOKC4FmJI9SElJGRr+\nauBLgAZXLQEVZcAtBgLRM3DIYA/hGWA48AJwFvADEARhivl6AF2UGdZMFUEQWtVb1xAoZeBQe51c\nJ4sAJmWlBx97CHsBP8oaWSNtgfZAO2AhoF6JfmxJ79c5kMqAtNcGqBAeAQYCdQAOI+jc5Aehw1Ff\ngCnkvgOYK+IVoCSgogykgoHAKgOSxXmEu4FvAA4ZuPzIh4uTjXsAL8pG2Sj3AccBrwLs1fwXCMMK\niRfbI0x1CsTSYqwNRm9HPlxcbSgDUDn0AKggMil/yV/W4Yr5IzkxSHuJO4FbAC/EeswkN3ru9DEQ\nKmXg0Pqz/GwnGdnt5picyuBygGNzBk4pDKRadspOmQVwYpD2EZwYbA7cBHBugL0aFWUgnQyEUhk4\nBB+QAzZiEh9IgunJDgM4pDgboGLgZF1lIBnhPMVKYBkwH6DH5RcAt58B8OHnBCGTyaooA5liINTK\nICfpfFjnHASjBm0CKIzIzOQkVQ6CyoHDjBIAvSX5K845CIIrGPyV//EgNsgG61bM1QxGZeLE5jkA\n3a+JioCKMuAFBlQZ5NMKTEZCBUHQXoGTe3zIfwLYzeeDv3v9btk3d5+UuOpvxUAFUQ5wFEdVqSon\nAexhUBGE2dU6H6r1Kw8woMogyUYYN26cdOjQQYwxSZakhysDmWUg9TNlmb0+PbsyoAzEyIAqgxiJ\n0t2UgaAzoMog6C2s16cMxMiAKoMYidLdlIGgM6DKIOgtrNenDMTIgCqDGInS3ZSBoDOgyiDoLazX\npwzEyIAqgxiJ0t2UgaAzoMog6C2s16cMxMiAKoMYidLdlIGgM6DKIOgtrNenDMTIgCqDGInS3ZSB\noDOgyiDoLazXpwzEyIAqgxiJ0t2UgaAzoMog6C2s16cMxMiAKoMYidLdlIGgM6DKIOgtrNenDMTI\ngCqDGInS3ZSBoDOgyiDoLazXpwzEyIAqgxiJ0t2UgaAzoMog6C2s16cMxMiAKoMYidLdlIGgM6DK\nIOgtrNenDMTIgCqDGInS3ZSBoDOgyiDoLazXpwzEyECRGPfT3WJgYO/evTJnzhz58ssv5ayzzpIz\nzjhDChdWfRsDdbqLBxjQO9WlRti8ebPUrl1b1q1bJ927d5f33ntP2rRpIwcOHHDpDFqMMpBaBlQZ\nuMRv+/bt5ZRTTpEePXrIkUceKY8//rgsW7ZM+vbt69IZtBhlILUMqDJwid+5c+fKDTfckFXaIYcc\nIl27dpUhQ4bIH3/8kbVd3ygDXmVAlYGLLcOeQaTUrVvXKoLJkydHbtb3yoAnGVBl4GKzVK5cOVtp\nFSpUsJ9XrFiRbbt+UAa8yIAqA5dahcOCYsWKZSutZMmS9vOmTZuybdcPyoAXGVBlkMJW2b9/vy29\nUqVKKTyLFq0MuMOAKgN3eBQ++LQziJQdO3bYjyeffHLkZn2vDHiSAVUGLjbL+vXrs5W2detW+1mV\nQTZa9INHGVBl4FLDFC9eXObNm5ettMWLF0u9evWkZs2a2bbrB2XAiwyoMnCpVXr16iVPPfWUGGNs\niXv27JEJEybI8OHD1STZJY61mNQyoL4JLvFLRVCkSBFrgtyyZUvhCkK/fv2kQYMGLp1Bi1EGUsuA\nKgOX+C1UqJA88cQTdiKRcwUVK1Z0qWQtRhlIDwM6THCZZ9obqCJwmVQtLi0MqDJIC816EmXA+wyo\nMvB+G2kNlYG0MKDKIC0060mUAe8zoMrA+22kNVQG0sKAKoO00KwnUQa8z4AqA++3kdZQGUgLA6oM\n0kKznkQZ8D4Dqgy830ZaQ2UgLQyoMkgLzXoSZcD7DKgy8H4baQ2VgbQwoL4JcdC8fft2+fzzz7Md\nwYQplKlTp2bbfuihh0rz5s2zbdMPyoCXGSgEl9u/fW69XEuP1I0hz4866ijZvXt3gTW68sor5a23\n3ipwP91BGfAKAzpMiKMlSpUqJZdddpl1VS7osKuvvrqgXfR7ZcBTDKgyiLM5OnfuLH/99Ve+R1Fp\nXHzxxfnuo18qA15jQJVBnC1y4YUXSpkyZfI8qmjRotKhQwdhGDQVZcBPDKgyiLO1+LB36tRJ+D+a\n7Nu3T9h7UFEG/MaATiAm0GJMu57XSsERRxwhzMisqdgTIFYPySgD2jNIgP5zzjnHrirkPJS9hWuu\nuUYVQU5i9LMvGFBlkEAzMd5hly5dcg0VOETQVYQECNVDPMGADhMSbIYvvvhCGjZsmO3oo48+Wtat\nW5dtm35QBvzCgPYMEmwphkA/7rjjso7mEKFr165Zn/WNMuA3BlQZJNFi3bp1yzJA4hDhqquuSqI0\nPVQZyCwDOkxIgv8VK1ZIrVq1bAm1a9eW5cuXJ1GaHqoMZJYB7RkkwT9zKJ5yyim2BB0iJEGkHuoJ\nBtRrMYZmoN3AqlWr5Mcff7Qvpk7buXOnMJ+iY3y0cOFCufnmm4XeiuXKlZOqVatKlSpV7P8aNWpI\nyZIlYziT7qIMZI4BVQY5uOeD//HHH8vcuXNl6dKlsmzZMtmyZYvdi0uK9FrkQ06TZD74NDLii4qB\nwwb+/+WXX2yuxd9//90eRwOk448/XurWrWtzL5577rnSpEkTe3yO0+tHZSBjDIR+zoAe3J999pm8\n/fbbMnnyZPn222+FKdKYSp0rBnXq1LEPMYcElStXzpowjGwxxjTg/jmFLs/r16+Xb775xioVKpb5\n8+fL2rVrre/CGWecYb0g27VrJ8cee2zOw/WzMpBWBkKrDFauXCnDhg2T119/3f6K82Fv27atnHfe\nedKsWbN8nZGSbSHaItCk+aOPPpKJEycKg6Y0atRIrrvuOmvBWLZs2WRPoccrA3EzEDplMGnSJHn2\n2Wdl5syZcswxx9gH8IorrrA9gLjZc+EALknOmjVL3njjDRsMhUMKWjHefffdUr16dRfOoEUoAzEy\nwEhHYRD8ApvGjRszqpNp1aqVgVIw+/fv99Slo4dgBg8ebDDhaDBUMVihMOjBeKqOWpngMiDBvbS/\nr+y7774zLVq0sEoAUYrM4sWLPX/JCJ5iRo0aZWDDYLBaYe69916D+QfP11sr6G8GAqsM0P02Dz30\nkClWrJjB5J6ZN2+e71qKSoE9BSxVGgxpDIKu+u4atML+YSCQygCz9ebMM880JUqUMM8//7zhQ+Vn\n+fnnnw0CqhgsbRrMJZg///zTz5ejdfcoA4GbQJw9e7ZwqY5GP2+++WbGJgZjnLKJa7f//Oc/0qtX\nLznttNPkgw8+sPYNcRWgOysD+TAQKGUwbtw4ufbaa6V169YycuRIQc8gn0v351e0WWCwVRo8MVdD\npOekP69Ia+0VBgLjmzBmzBgbm/Cmm26SsWPHBlIR8KahQxSNpGjefNZZZ1kDJq/cTFoPfzMQiJ4B\njXcuvfRSue2222TQoEH+bpEYa09DJZo17927VzA5qkOGGHnT3fJmwPfKgP4AjDjUvn17GTFihNB/\nICxChylaSzLCEo2oaEatogwkyoCvlQGt95o2bWqv/dNPPxUsIybKg2+Po18EfRweeOABefDBB317\nHVrxzDPg6zmDAQMGCIyKrClvGBUBbx86SD355JPy6KOPipMENvO3ldbAjwz4tmfA2AKME/Dwww/L\nPffc40fuXaszlq2tSzTjKHD+REUZSIQB3yoDrhpwaY0ux1xmC7swBgMnFKdPny7nn39+2OnQ60+A\nAV8OE3bs2CGw3Zc+ffp4RhEw/fqCBQsSaAJ3DmFil7PPPltefPFFdwrUUkLHgC+VAe0IDhw44Jmc\nhosWLbJxCJhLIZPSo0cPmTBhgmzdujWT1dBz+5QBXyoDmuLSCu/www/POO2MZtS/f3/hykamhXEZ\nuLQ6ZcqUTFdFz+9DBnypDGiBxy6xF+T++++3y3peqAutEmlzwWVWFWUgXgZ8pwxWr15tu8GOfUG8\nF+zm/u+++64wXBrjJHpFaHPAYYuKMhAvA76Ljgx3XnuN9ErMpHBp85133rETmU4U5EzWxzl3tWrV\n5KeffnI+6n9lIGYGfKcMGIaccuSRR8Z8kW7vyHV9rmQwlqLXhGHbHY68Vjetj7cZ8N0wwQt0Ugkw\nr2LFihW9UB2tgzLgCgO+Uwb85aNkavmMjlHjx4+3qwccJvDF1Q3KkiVL7Gc6EGVK2CtwOMpUHfS8\n/mTAd8ME59d448aN1lsv3bRv2LBBmPeA7tKOcNhAoeERQ7EPHz7cJlxxvk/nf9avUqVK6Tylnisg\nDPhOGTBNGecLuLzImfN0yz/+8Q/hAxcpu3btklKlSsnjjz8uNJPOpHz++ec2IUsm66Dn9icDvhsm\nkGYuK37yySf+ZDyFtaZSQih4QTDYFJ5Fiw4qA75UBm3atLFWdr/++mtQ2yWh6+JcBocstM5UUQbi\nZcCXXot0VOK4eODAgTZacLwXHdT96azELNFMIquiDMTLgC97BkyHzijIjHfIFOgqYtPIc+h0yy23\nKB3KQEIM+LJnwCvV4Cb/a28NbvI/LvRd4gz4smfAy61SpYq1AnzssceE6dXDLEjBZm0cGP5MRRlI\nlAHf9gx4wRoQVWzcQw2Imujtr8dFMuBrZcAL0VDpGio98obW94kz4NthgnPJdCHm7Pnrr78uSErq\nbA78fyZRueiii2x4eJpEa86EwDd5yi/QdxaI0Rhp2bKlTaDSpUsXQcZleeaZZ6RwYd/ruWiXarfR\nRblVq1bWO1GzKeVJk34RJwOBUAa85s6dO9tfSS450m8hDIlX586dK8cee2ycTa67KwPRGQjUz+eV\nV15pw6fPmDFDTj/9dPn666+jX7VPtzIle+PGjW26efYINAOzTxvSo9UOlDIgx82bN7cz7GXLlrUP\nzgsvvCD79+/3KP2xVWvz5s02fkL37t2lZ8+eMnv2bHVTjo063SseBmCwEkjBsqN56KGHDNKuGaQg\nM/gl9d11Yv7DwIbAIFOSOeaYYwyiHvvuGrTC/mGAji2BFuRiNC1atGDAAXPZZZcZePV5/nqpBJAk\nxtSqVcsULVrU3HvvvQYh2T1fb62gvxkI3DAhZ6+IS4/Tpk2TiRMn2olFhhK/5JJLZPLkyTYRS879\nM/n5t99+kyFDhkjt2rWlW7duNl7D8uXL5YknnhCGQVdRBlLJgO+NjuIlZ8SIEXL77bcLIxpzJv66\n664TJh/JVLhzWlHOmjXLZpJmpCQmQeHKCG0mqlevHu/l6f7KQMIMhEoZ7N271yZf2b17tw1xPnr0\naGusxJiF7EG0bdtWzjvvPGnWrJnQM9IRpnJz026BYdPmzJljMyazx0IDIkZvwnBA/vnPfwonP1WU\ngXQzECplwAeNv74LFy606dxJNkZ5NoQarRg5dGBWZ1rzYdJRGjRoICeddJIsXbpU6BBVuXJlKVIk\ndtMMpl5bv369fPPNN7Js2TL7mj9/vqxdu1aKFy9uhwGYxxDGIeD/+vXr2+Cq7B2oKAPpZiA0yoDD\ng+uvv16YBYkPXl7CZTz+anMdn0qAqcrYo6DwIWXwEHpMsufAVPAlSpSwCoL7sMfB+Arbtm2zLtZO\nchX2Khi7sW7dulbB8OGnc1FkKnnGdGRKdayASL9+/fKqnm5XBlLGQCiUAX+ZGzVqZKMiMTpSrPLK\nK6/YbjsfUgY7ZQwFvjis2Llzp33wqQA47ueD7SgHLAVahcGsT3zVqFEjpglATh727t3bhnSjibWK\nMpBOBgKvDPhL3aRJE/sLTvPdWLv5jDJ81llnWYOlCy64wI7v09Ew11xzjbWiZHp32Bak45R6DmXA\nMhD4pcU777zTjtHffPPNmBUBHYEYdJXzCRTnv/2Q4j8vv/yynZto37591vAkxafU4pUBy0CglQET\nmvzrX/8SdvePO+64mJqcXf7LL79cGHmZqwjpFtoT0CWZcRpuvfXWdJ9ezxdiBgKrDJhmrEePHjZw\nKh2YYhXaIHC1ga7QmRLOMbz22mvy6quvWtfsTNVDzxsuBgKrDOjQw/kBOirFKvQKfPHFFz3h2ESb\nB9od8DqYw1FFGUg1A4FUBrQl4Is5DzmzH4ssWrTIrhxE2zedcwaR5x8wYIA1gOL8gSaMiWRG36eC\ngcApAz40TIp6ww03SKzLc1u2bJHWrVtnZI4gv0al8dMbb7xhly5popwppZRfHfW74DAQOGVwzz33\nWOOgWMOGc26gXbt2NsW7F+Me0MiJadMYsOXRRx8Nzp2nV+I5BgKlDJhRiEOD559/PubhQZ8+fayV\nYSYnDAu6K2gn8dxzz1llgJgGBe2u3ysDCTEQGKMj/qrTn4CGOlxSjEXGjBkjNPIpSJiGnb/MmRYG\nfOW1MdNyrEulma6znt8/DASmZzBs2DC7Ns9f0FiFLsz0VyhdurQ9JFbrxFjLd3s/XmO1atWEE4qa\nY9JtdrW8QCgDThrSwYcTh1yjj1Vobsy1fNokvP/++zaVORUCHZK8mIeATlE0SPrhhx80wWqsjaz7\nxcxAIJTBI488Yh/eBx98MOYLj9wRcRKt+TG9CdlLoMEPVyK8qBBOPPFEGwaeXphUZCrKgGsMYLnK\n14JAIQaxAczQoUOTvg7ELzCwWswqBz0GA18BG1g1a6NH3jzwwAP2umEf4ZEaaTX8zoDvJxBpTzB9\n+nQ7X4DgoQkrSQROtYFMOFHICUOvC/0mmF6NPgycUDziiCO8XmWtn8cZ8PUwganYaULcv39/SUYR\nsI1o3MNIRsy74AdhwBTml8SvkY2ZmAmnKj/wpHWMnQFfKwNGDT7hhBNiWh4siBIqg44dO7oa67Cg\ncyb7PeMm0iCJSVWoEFWUgaQY8Os4BxGHbIIUuCcnfQnMpQASDeITJl1WJgrAkqPBCohBcNVMnF7P\nGRAGfNszoD1B+fLlrYtyUtoQB7O7zVl65mf0ozDQa9euXW0PicuOKspAIgz4Uhkw6jANcBgvkFGG\nkxEodRk7dqx06tQpmWIyfiyDuDDoKg2SGJdRRRmIlwFfKgOGMKMFHlcSkhX6M2zYsEGuvvrqZIvK\n6PEMxspw7wzDfvPNN2e0LnpyfzLgS2XAOIH0NHRjOY1DhFNPPVVOPvlkf7ZgRK3ZM2BimJEjR9qe\nU8RX+lYZKJAB3ykD5jJYsGBBnoFICrziiB0Y75Cz8VdddVXEVn+/bdWqldASk6bZ5ElFGYiVAd8Z\nHTFeAbvDq1ativUa89yPGZQuvfRSWb16tc27mOeOPvuCNgdMLvv1118LQ65zCVJFGSiIAV/1DDjZ\nx3BmtAdwQ2hb0LRp00ApAvJCgyS6Z9O3gr0eNUhy424Jfhm+UgZMbMIJMkcZMKXZRx99JIxqxDRo\n8dz0nHF/7733soYIyZTlxduEy64cAjFxTKIOXPTkVFdpL7ZuaurkK2XAh5cuyqeddpowJ2Lt2rWF\nGY27d+9uH2wmPolVIUyYMMEuwXXo0CHpslLTNMmX2rBhQ2HKNqaG++CDD2IukAFUmI6OEZp1mTJm\n2vy/o5+Mp+rUqWOQ18AgqpFBLAKDhz+r+ghbZhCsxCC8eNa2/N7gRjdwU3alrPzO44XvEMDFHHbY\nYQa+HAVWBz0vwxeGF9YqE0lkCzxGdwgGA3R08YWsWbPG3pzTpk0zs2bNsu/x656t7ghwYkqVKmWQ\nFDXb9pwfEAzFuv8iJkDSZeUs24uf8etu0EswWEI1MNiKqYr333+/KoOYmArOTr4ZJkydOtUGHmEA\nEqZVp5xyyinZumZMeU7rRK4S5CeMFkShrUKyZeV3Hq98R4Mkzh/QuOrGG2/0SrW0Hh5jwDfKgJ55\nzZo1E0YlousyhS7HkVKhQgX7kT7++QlXEbj0VrZs2aTLyu88XvqOAVS5wkAjK2aNUlEGcjLgG2Uw\nZ86crFgDP//8s102o2KIFCYtpWzatClyc7b3zLCMYUbWKkIyZWUr2AcfGAzl4YcfljvuuEO4MqOi\nDEQy4AtlwF96PuDnnnuurbsTzTjyQvjeSYJSqVKlnF9lfaadApUGjY0oyZSVVaiP3nCZsUWLFsJk\ntMwkpaIMOAz4QhnwV4zeiVzuohx99NH2wadtQKTs2LHDfszPz4BDBKZc5ziakkxZtgCf/WHkZ/ov\nMDIUPTUdBeqzy9DqpoABXygDpkhnghQntBntCyjr16/PRsnWrVvt57yUAc2OqVgifRESLSvbiX32\n4fDDD7cm3TTUQmBVn9Veq5sqBnyjDBo3bpzFAROfsKcwb968rG18w8CgVBo1a9bMtt35wF4Bcxey\nm+xIomU5x/v1f/369YUxEGi9SWMuFWXA83YG8Cy0NgEIfJptQfeuu+4yNEKCxaHdzrV0KAHDEGZ5\nCZYeTc+ePXN9nUhZuQrx6QZESTJYVTGYl8l2BTfddJO1M2B4OZVwMOB5r8VvvvnGxhqg9x1/zRxB\n8wgMY6xnHhOecIKRXf5rr73W2SXb/2XLllm7BAYzYSalSIm3rMhj/f6e8y5nn322NTvmEAoGWzZS\nNE2YafLN/I7MR3nBBRf4/VK1/gUw4HllQGMZTnTxJnUm/SKviRNgnCuoWLFi5OZc7/v27WvX2WHJ\naNOn5doBG2ItK9qxft5G/w4kkJELL7zQcuTna9G6J86A5+cM+IvOYKXRFAEvm266BSkC7sdQafR2\n5Gx6XhJrWXkd79ftzFzN+RRyNHjwYL9ehtY7SQY8rwycYUIy18nuL1cS/B7nMBkOCjqWw4BHH31U\nMH9i3cEL2l+/Dx4DnlcGjGjEnkEyQhPck046ya40JFNO0I/lUIpWijRIomWmSrgYCLwy4DwArQ4j\nbQvC1cSxXy2HUAymytTvHFKpQVLs3AVhT08rA/jSy/bt26V69eoJc00/BP7KqTKIjcJy5cpZgyQG\nU73vvvtiO0j3CgQDnlYGDHFGOQ4ed4kKhwg0Y2aEJJXYGGAkKSapGTRokFUMsR2le/mdAU8rA/rf\nU6pWrZoQz1xDZ+wC7RXETx/tNZiM5brrrhOmq1cJPgOeVgYbN24Udlsd1+R4m2PKlClC5yUngGq8\nx4d9f+azpJ8Hg8DQzkMl2Ax4XhlUq1Yt4Rbg2jkjIyXas0j4xAE5kPEiaPRFV+cePXoE5Kr0MvJi\nwNPKgBN/+cUmyOuiuJ2/ZIyArEOE/Fgq+DsqYypVKgX2FFSCy4CnlQHNjBPNBkRPPERMliuuuCK4\nrZemKzv//PNlwIABcvfdd9s8DGk6rZ4mzQwEVhnw14y29kwmopI8AwhBb+NGMs8EQ8epBI8Bzzgq\nvfTSS3bWmuNU58XlLUY8bt26ddY2fkevQ0Yoykt++eUXO7x47bXX1AQ5L5IS2P7bb78J40pw6DZz\n5kwpUqRIAqXoIZ5lwCue2k8//bT1n8fDbnK+EOHI4MYzsJCzLyw55lttBO0wWIEoMH9CvoXol1EZ\nQBZsyy2Cqkb9Xjf6lwHPDBPat29vFeaff/4pOV9Mnc7xP81l//GPfxS4OsAhAlOtIaGKZ5WwXyvG\nXBUvv/yyPPvss9bMO9p1IElNtM26zeMMeEYZIDVarqQoObmDzi1wiYuGSgxgoqsIOdlz73Pnzp2l\nV69ewpBx9CqNFCalqVWrlvz++++Rm/W9DxjwjDIgV3yA8xuH0viIyUDzE/rk01CJ3ncqqWPgmWee\nscqbBkk07KJT0z333GMNlGiXwAzOKv5iwFPKgEMFDgeiCSMjM/xWXkFOnGM4RGA5nGhUSR0DbI9x\n48YJnckYJ+K8884TzPvYEzJIDNtBxWcMeG26g0FNQWHU1/z58/Ot7rfffmuPmzFjRr776ZfuMTB0\n6FBTpkwZO8Eb2W6c8GWCWxX/MOCpngH1KIcKTn4EfnaEAU5OP/1052PU//w1Yv7F5s2bR/1eN7rL\nABSB3HbbbTbZbc4eHaJWawh2d+lOeWmeUwbs4nP1IFI4j4CQ3pGbor6nMqBTUuHCnrusqPX168Zd\nu3aJM4nIuQI++NGE7uMq/mHAM0ZHkZQxfoETy4DbuaRID8acWZcjj2Eo9YYNGwqGEgX2ICKP0/fx\nMYBOr7XsnDZtWoEHcu6A4dbVCrRAqjyxgyd/Qhka3Rkq8IZisM78FAGZ5K9QLEMJT7Du40pQMY8d\nO9bmU+Bl5NcLo+LgUqOKPxjwpDKIHCqwC1qQ+yxvOt6gVCIqqWeAuRpp6s3eQZUqVWy4+rzOqkOF\nvJjx3nZPDhNIE3sCdIjBTLX1p2duxbzk448/tunav/76axuMI6/9dLv7DHD+oF+/fta9mb2EnEFU\nuY1DhSOOOML9k2uJrjLgyZ4Br9D5lWf4rfwUAfflr8+pp56qioBkpFloCEYDJM7VMOFttGEDQ8+p\neJ+BjPYMtspWWXYQP8gP8uNBbJJNsm3uNtl29jYpuqio7G+4Xw49iBJSQsoBVQ6iqlSVUfVGSdtO\nbeXJ+560e3mf9mDWkKtAAwcOlEceecReIJcbqRyYy3H27NlRL3rPnj3WpJmZs2AnYieKkexV+GJk\nbCTUFe7DF+eRaHTGUO6lS5e2vUcOU/g64YQTrIcrvVwTjYERtYIh2phWZcAHf85BzJW5eOQ3WarL\nS3mpAfDB5kNeGSh1oJQMu2iY9P2orxQFcDtY7JbdAjWRpTg2yAb57sB31rnpkEMPkdrAOcC5B1FR\n8s/BGKK2Ttul8qHu2rWrLFy4kFm+7WoQo1YdddRRNmz9nDm4C/Di8I6+DRxasPfHngUjKzkPOFch\n+OBTAfBFZeMoB5pAM9kulQZXmlauXGmtIXmRHGLSzf3cc3EX4EUFoVIwAylVBgfkgMwD3jmIdbJO\nDgPOAs4GGgB1AT780YSNHEv8wv2yX1YCVDbzgY+BLwBuPwNoB7QHjgdU0sMAlQBcyaVPnz72AaYP\nAx9eprrjChETvTI+ZZMmTezDylD23J6MsHz2MLjMTGe1uXPnCmMwMJckz89Xs2bNog5lkjlvYI5F\no7kuP5mfzP8BxwIwLDYnAw8AC4H9QDpkh9lhPgC6AeUB1qM58CbwJ6CSWgbghm7gNGbOOOMMayJO\n8+Ru3bqZDz74wOBXPbUnP1g6ehwGvRPzwAMPGER5tvU47rjjzP/93/8ZTE6npQ5+Ogm7ca7JSrPS\ndAWKAnwA7wC+BjIt+8w+Mxm4DDgEqAgMBHYCKu4ygEC0BvMGBpmxDX7pzWWXXWYmT55sMMlrsPLg\n7sniLA2rTYZBWTD8MJh/MBjKGAwv4iwluLu7ogzWmXVWCfBBqwmMAHYDXpQNZoO5FygNHAUMAvYC\nKskxgIQ1BhmYDOYFDCb3DGImmoIiUiV3xsSPxryDGTFihKFTHBUWlcK6desSLzAgRyalDPiL+yRQ\nCjgRGA38BfhBtpqt5n6gBHASMBNQSYwBxEM0yHJtMNln7r//foOo1okVlOajsNphRo8ebWC5ahAV\nyzz55JMGk5RproV3TpewMlhulptTAT5MjwJ7AD/KarPatAE4p9AD+ANQiY2BP/74wyDakR2LI8yc\nWb16dWwHemwvLFuaRx991Coz2KuY5cuXe6yG6alOQsrg3+bfpiTQBFgFBEHeNm/beQ5Odn4FqOTP\nwFdffWUn5Tj+fvvtt/Pf2Sffrlq1ymB1wwZ8/fe//+2TWrtXzbiUwQFzwE4KIkaxuQ/gMCFIwrmP\nswDOJ3wIqERnYOrUqXZeAGv5gRtrc5iAVPQ2CjcnG+EbE52EAG6NWRlwOe4qAIHMzetAUIXXeS3A\nFZFRgEp2BkaNGmVn4mEmbrh8GFTh6gdD9iPYTqCvM7L9YlIG7BFcDfAXMywTbfeYe0xhYByg8jcD\niHloYF5sEPg0FJRwYpQrI4jxGIoeQkzKgPYC7BFMA8IkvUwvUxyYBYRdZs2aZWAybBAiPVRUwE3b\n9hDCkDSmQHPkN+VNuQp4A+gEhEm4xNABoD9F/9f7S+HfC9vszlhTt6G+GGuBUZhpN0/vPbrp0v6e\ntvGwdAtMhGa6ktMrlHb+b731lvU1CNN9wPD7jM3Zv39/6ztBvwi6brP9+aIzluNAxTD9vAcqVKgg\nxx9/vBx22GG+oSpfZbBW1sppQGdgKBBG2SE7pD6w7sh1gmGSlCldxjrV8Abgi9mf6FGHZTZrB4+f\nTUsTv6PTDTMQ1a9fX84880zrvUdvOz8Jr4c5KDDTLkuWLLHxJfxUf7fqesstt8grr7xi275s2bJW\n+dOXgu1MRyveA3SiYjapyOCwDAQDU2h7DzBPZfPmza2vhFv1crOcfJVBG2kjq4DFAF2IwyoLZIE0\nBf4DXAvkJbwJmPSVWZ3WrFkjK1askP/+97/WcYZedQzsSnfeK6+80gZu9UNsQEwYCnwKrIMRb+aw\nCh92xthkaD34V+RJA5UnnaPoNMV74IcffhAsw8qXX35plSl/POidecUVV9h8E3Xq1MmzrLR/kdcA\ncI6ZYw1xppqpee0Squ3Xm+vNMUCixlW4OcyYMWMMFIFdx6a13g033GBww3iWRxrjwOPPGhZ5tpJp\nrBiXVPGAGrhfJ3RW+mYwp8ftt99ueWVZ6CmYDz/0xjJ2nhOI9PC7AFD5m4GNZqO1thxqhiZNCX45\nzJAhQwzyS9pJOYQN8+TyFROkUGnBlTzpaw5KAS1atLAPcLLXQ4/KKVOmGAT7tQrmwgsvzLjNRlRl\nQO9DmudOBLwg7733nqFzSaaFHpkNALfEce7hA4cEMQYBQKIWzV4FZ/PTLYg5YLrCiSeTggSu5qWX\nXrKOTxizG5pAZ1ImTpxoH143vR25hEmnKUw+mo8++ijX5WGoYV588UXrXJXXPZLroIgNsT4/UZVB\nP9PPVAUy7XRE4jFOs+Qjp1/E5WXm7cfmY6skl5qlrlaArrX0s0f2YoM5h6yyEUjU3HXXXfbXGZmL\nsran483SpUst7wgSko7TRT0H0+VVqonPh8sAAAvXSURBVFTJIPCJXd5jt5pORVSOmRI6NyHgjnnw\nwQddrQKHEBxC0tApctjwxBNP2J7Id999Z9gWtWvXNogQFdO5431+oiqDpqapuRHIpCCJiuGLFmC8\nCbygDGh8dQTwLOC20N0X4b7MpZdemlX0ggULDCYg7fWnWxk8++yzBkulGTW2ufjii+31kxAqRoTM\nt1x07949i6NMvLnxxhtN06ZNXT81TZ+pEOjvwfuBwwisVhhEbso6F3tHbJf169dnbYv2JpHnJ5cy\n4AQZDW1GAl4QusR6RRmQj9bAlUAqhAYuvFb+d4RDCW5LtzLgTdm6dWunGmn/v2jRIuteHHlixDu0\nDwfdpTMpI0eOtHM9nGB1WxgcBkvSBukEDew6bM848hwcLtP4CzYPkZvzfB/P85MrVPr38r3sBbi2\nrpKbAfLCWIupEExO2Rh98JhLRfFxlclYgrSPyJTQaIup3iOFxlxc3uPafSaFvNDw7Pvvv3e9Goir\nYONGYuXJBoylnUqk0LiJy5s0/nJbcikDhi+nVABUcjNwlBwlvwCpkksuucQG8kxV+bGWS3sJWtJl\nSmjNyVRuOQXdY8HwIefmtH6mdSGFHKVCMFS0Rmz4ubfWrDnPwfNTEfF7NyWXMvhVfrXlHy6Z1b5u\nXqSbZTGsu8ORm+U6ZR199NE2nLjzOVP/aUnnNaMohlan4Rb8BDJFiz2v0zMhR6kQ3gOOYKXJeZv1\nn6bvNF5yWxnlUgalpJQ96R/yR9bJ9c3/GCAvDkf/2+reO4wZba4A90pMrCTecDSx9orQ5Pehhx6y\n1n+ZNul2eCFHqRDeA45E6x2RC+aZcJSSs2+y/3MpgyPk75x4qewKJ1vpTB7PYZTDUSrq8dlnn1l/\nhlSUHU+ZzEqEWIbxHJLSfZl/4c4778zoPIZzgQ4vHMqkQj799NOsYh3Fk7UBb+goRZPmZPNMRJbJ\n97mUwbFyrN1nhazIua9+BgPkxeHIbUKYdWj8+PHWd8HtsuMtD9aR1rci3uNSsf/LL79slQDiLKai\n+LjLpM8JhRylQmD5KVi6FE4mco4kp1AZ0fnJbcmlDPirVxNg+jOV3AwwQ9SZQCxC99ZYhZNBWL+2\n43QEGY31sJTtx5tx3rx5KSs/1oLfffddO1HWpUuXbIcwPVumhLzwlznWnkE89wEdw+ADIQjQKrwP\nmIEq8nhYZNpUch06dHD98nMpA56B6c9mAF4QZ5KGXmOZFqaHYxo38pOfcFmOk1x8oGIRjgFvuukm\nQbIR4c3AXwRHMnX99K6kpyXyCThVSfv/6dOn20SuzLEIXw77ev75563ShIVk2uvjnJD1Ij/5CYzk\n5IUXXrBxIOi5GovQGxLOa9K7d2/hMjOHRWx/BJzNOnzs2LHStm1bmyouayPewC5BWrVqlWvyOa77\nJ5q1wnQz3ZrdZjIbEtNf0QoOyyjW6Aa/DFHttqPVP1Xb+pv+pgIQLT0bbehpHUZ7frSNDaiJcXeB\nVUGX05qbYv3YIHV5tv2Ziahjx462PPLA8tNliovZast9rMYt2SruwofFixfbXAbkMueLXEWabbtw\nupiLoOk46wOFkOsYWhByO361DdPJ0XqQ+6InkWvfyA30t2AQVu5PK0s6MTmCHxZrfMSkNM8884z1\neIx2D9BMm+d6+umn7aGJPD+5LBBZEs1ujwVuA1T+ZoAKgC7MdwGRgskec91111mrMDYmZn+zbl7G\nz8tLaE4KzW+DizIPIG9+rwn9IujCTMWg8jcDtATFXEE2M22aDj/22GPWZ4EPJBUB/zuvaIqDpdGa\ncPjw4dbikElckKg2T5q3bNmSbzvQGhK9BvP+++/nWUZBX0RVBjxoMECz5DWAijEvAOQDHhOGDUMN\nXL16ddvgzNvnNHzkf26PFHTZbIMx/yDTesGizmp7mhx7URhrgaav6O56sXppr5PDx+DBg23mJfbk\n6HrMH4CcCiDyPpgwYUJWXRmKnY5GjGlAHwTyS1+LgnwNsgrI4w3d4llmMhmh8lQG/CWsDnQCwi7b\nzDZTfn95035qe3P55ZfbB5kPc2SD5/WeAU2wLGaYY4A3DF/nn3++VQp++MVl74DDHS84imX6PuSQ\njT0l9uj4ILPNY7kP+vbtazM/896hmzKPo4cqs0HTAcsNoT9Lsolt81QGrCDjGTCuAdOYh1Xo/VX7\n4dqmcKW/x3/5/QJEUwjcv169enYsyG7c9u3bfUUllQBddhGmy1f1drOyHNPffPPNWco/nnvAGTZy\naNGuXTvz3HPPeTbzc77KgIT2BA4DgpJGLd6b5N759xq5V0yl4yvZmyGeG4HKIdpkT7x1yPT+DNXF\n+ZD8xrSZrmMqz895IU5aclhHHviKpUfA9uf9wuzUfpAClcEus8tG96lhapjNQJhkkplk0LE3DwGU\nb775xjz++ONZKwbOjRGtR+BsC0rIMJgC2xt70qRJYboFbDeewVW4SsRuOHtKdGHmvA/H+2znvOaM\nnO/YG/CDFKgMeBE/AUy5zpBfvwJhEEY1YnLZ64BoQt96huNiTDxq/7wmkeBdFu1wX27jqgns8WOO\ntOPLi4yoNCd8qQS4bMelupzC1QBODnICEH4CURUDIxfxB8QPEpMy4IV8DxwN1AGYoDTI8o55xwY/\nbW/ax5RcljYGnA/gBBOXiPiL4HQjma04KMKZ6vbt29swbDltIoJyjc51wNjKIIy5gQehiUWh0zZg\n7ty5drKYk4y8B5wfCfaq/CAxKwNezAagLlAF+BwIogwyg2yOxZvNzWY/EK9whYBBLXv27GnHmAsX\nLoy3CE/vz5uek2kcIvllLBwvoTABtiHo6tata8OPxXs896ex0IABAwwCofgmN2VcyoAXyWFCK4Bj\n6ScAGigFQTgfcgnA63oScENokeaH5cNErvXJJ5+0v3wIxuLa8lgi9XDzGLYXA5DyFx2mvYbDBDfE\nq3YkOa8tbmXAAqgAngKYtvxs4CvAzzLajDYVAVoYfgqoxMYAZ9nZJa5YsWKueIWxleCdvTicg7+B\nnQx86qmnslkYeqeWqa1JQsrAqdIX5gvTBOCvKTM1bwX8JKz/OQBTr3NYEJbJUTfbiL+ezrCBATwj\nI/m6eZ5UlQV3YMMMy+wNNGnSxHf1d5OXpJQBK8Jx9TDgKACJSc19wBbAy7LILDJtABpUUZktAFSS\nY4Bh3fkwceIMcQcMoxt7WWhSTucg+o8g1qMZNmxYKHsDkW2UtDJwCttpdpqBAJVCCaAb8BngFWEI\neA4HOKyhEmgEeCVjlFc4cqMeTNzRqFEjqxTY7R49erRJRUjxROuKSFIGiWTtigiVwMCBAw3Dk6sg\noIbbJFApvATUA/jQcSnyYeC/QLplr9lrJgM9gPIAhzNcLpwGqKSWAdrKcxmS3W8m/aBrLl2yMzGZ\nxkQ0Dz/8sF0qZM+F5uG0EVElkP0eyDclO4hLSubLfBkDvAtsAI4HzgPOOQh+dlP+kr/kC+Djg5gj\nc2QH0BhoDzCdemVAJX0MwBzbBmxhgA4ss0qZMmUEcwtyzjm4C/CCUY+NeOxmjVavXm1zDjCaMnJU\nCj8jMYnAUUg6d+4sGM64ebrAlJVSZeCwxC7CAmASwAf1c4CJWsoBdYC6AEOtVTkIPrBlgBLAoUBR\ngPvvPohtsk1+BDYB64HlwNfAd8CfAHM+nA1Q8bQBjgZUMs8A4/kxmg8fUOQNFHjsCSz0BB58AgMf\nG9ePYcKZLAWp5mwIOIYK5wumv8KIR4x4Bcs/GxSUigaWoPbFuISMMIXgIwJnMGGyET70VDyMAITE\ntlHzMGSeFe/UIC3KIOfl8sFeBCwFmJ2IWAX8DPDXPVYpKSWlKlALOAWgUmHGo9qAivcZgK+HLFmy\nxD7EWNoTJBcV+HIIfABirjyGIYKlTZtlCEZCwtepp54qmLewCiTmgnRHyYgyyIv3A3JANgP8xWd+\nAqcnQAVRHHB6Ckzwwl7EYYBK8BhAoA77a49ly6yeANOZ8cF3egqME8keBLMLwRoyeCRk4Io8pQwy\ncP16SmVAGTjIgKpUvRWUAWXAMqDKQG8EZUAZUGWg94AyoAz8j4H/DyXjXBPYfCluAAAAAElFTkSu\nQmCC\n",
      "text/plain": [
       "<IPython.core.display.Image object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "lstar successful: unrolling seems equivalent to proposed automaton\n",
      "equivalence checking took: 0.017006999999992445\n",
      "overall guided extraction time took: 0.12463400000000036\n",
      "generated counterexamples were: (format: (counterexample, counterexample generation time))\n",
      "('10', 0.017189000000001897)\n",
      "('10010', 0.08149300000000892)\n"
     ]
    }
   ],
   "source": [
    "wrapper.dfas.append(\n",
    "    extract(wrapper.rnn,time_limit=50,initial_split_depth=10,starting_examples=wrapper.starting_examples))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "testing on train set, i.e. test set is train set\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAQMAAAGTCAYAAAAst3eIAAAAAXNSR0IArs4c6QAAQABJREFUeAHt\nfQm8VeP6/1MaNEpoNjdIoVGSIVdClBQVUUkuEhkyJYR+fyJj5QrdrgakjI00U2iSm4SSZlFJlAap\n9//9vlrn7nPOPufsYe291/A8388+Z++113rXu77vWs9+h2coZIx5S1SUAWUg9AwUgjIwoWdBCVAG\nlAEprBwoA8qAMkAGVBnofaAMKAOWAVUGeiMoA8pAOJXBATkgrYBCHsar8qrenspA2hkokvYzZviE\nfaWvzAReBsoBXpNZMktuAeoATQEVZSBdDIRqNeEteUs6AiOAboAXhT2Xy4DFwCKgCqCiDKSDgdAo\ng6Wy1P7S9pAe8jzgZflNfpMmwOHAbKA4oKIMpJqBUCiDX+QXaQwcC0wDigBel2/lW6sQrpArZDig\nogykmoHArybsl/12aMDu9zjAD4qAjX4SMAbgkGYooKIMpJqBwCuDPtJHPgXeBY4E/CSXyqXyKHAH\n8DGgogykkoFADxNGySjpArwOXAX4UYwYDBSukLkAJxSPBlSUgVQwEFhlwAfnbOBW4EnAz7JTdtrJ\nz2JSzCqFElLCz5ejdfcoA4FUBptlszQCagOTgUMAv8sqWWUnQWkwNRpQUQbcZiBwcwb7ZJ/tVvNX\n9E0gCIqAjX4iwOshngFUlAG3GQicMugtvWUJ8B7AdfogSUtpKY8D9wDTARVlwE0GAjVMoE3/P4Hx\nQDsgqHK1XC0fApwXOR5QUQbcYCAwyuAz+UyaA/zVfAwIsuyW3dIM+Av4aMdHsn3jdtmyZYt9/f77\n77Jz5075448/ZO/evZYGxq855JBDpGTJkvZ12GGHSYUKFaRixYpy9NFHCz+rKAOBUAY/yo92wrCh\nNJQPAHokBl3Wylp7zYffcbisfG5l1uXygS9durSUKlVKihUrJoUKFZLChQvLvn37ZNeuXfb122+/\nyYEDB7KOOfLII6VGjRpSr149adSokTRt2lRq166d9b2+CQcDvlcGe2WvnAtsBxYAZYGwCP0WWqxr\nIT2395S+FfoKH+oiRQo2taYi2LZtm/z888+yevVq+eGHH+Tbb7+VJUuWyNKlS63CqFatmlx00UVy\n1VVXSfPmza1CCQuvYb1O3yuD6+V6O0dARVALCJsMlsFyOzAB4LJjssIexIIFC2TGjBnyzjvvyH//\n+187lLj99tvln//8p+11JHsOPd6jDDAgql9lsBlsCgETgDBLN9PNHAZ8B7gt33zzjenVq5fB0MNg\nnsGMGjXK7VNoeR5hQDxSj7irMdvMNkWAx4Cwyx6zx5wO1AZ+B1IhmzdvNjfddJPB/IO54oorDCYo\ns51mz5495sMPPzQDBw408+bNM/v378/2vX7wPgO+tDNYJ+vkSoBBQB4Awi6Md/AO8CtwDUB/Brfl\nqKOOkn/9618ydepUmT17tlxwwQWye/duexooCjvhuG7dOunevbu899570qZNm2yTlG7XR8tLAQPe\n11fZa7jL7DINgLrADiBdwl/GKVOmuHa61157zbWynILmmrmmGPAQkErBJKMpX768ufbaa20P4Kyz\nzjJ4+LNO+ddff5ljjz3W3HvvvVnb9I33GfDdMKGz6WwOB74H0iW8uVu0aGHwy+jKKWfOnGmqVq3q\nSlk5Cxlmhtl5lHfNuzm/cvXz+PHj2f0wL7zwgv0/YUL2eZuHHnrIYHnTwObB1fNqYaljoOB1qBT0\nRhIt8ml52trm0/mItvpuCiiWOXPmyJdffmkNdE466STbFabhTufOnWX69OnWUIfr9uwCV65c2XaT\n2WX+4osv7DH4pRQ85FnV+vXXX+WNN96Qnj17CnoVdtmuYcOG0q5dO7v+P2zYMKlSpYq0bt0665hk\n39AC8wvgWmA+cDKQCmnfvr21SXjxxRdt8aecckq209StW9caPk2ePFmuvPLKbN/pB28y4Js5A9ri\n3ws8AdBG323p16+ffP/998IlNBrd8DMFE2N2vZ3v+aDXqlVLSpQoYa38aKjD9/fdd5+g9yDNmjXL\nGkdjGCBcq+/du7cMGTJE7r//frsf1/dPPfVUKV68uC2LFoBuC5cbTwM4p0L7i1RJ27ZtZc2aNbZ4\nKsdIoYUjZcWKFZGb9b2XGUhdp8O9kjk3cATwDyAVAiMcA4MdM2vWrKziBwwYkPUevQXbFR4+fHjW\nttGjR9uZ9Z9++sluc/bBGn3WPuhR2OOwXm+3cZmOgofIQAnY96n6s9FsNMWBa4BUCZcZ0VMyMHXO\ndQrygPve3HLLLbm+0w3eZMAXPYPSUto6IM2Tebbr67ZyZdefv/gdO3aU999/3xbfp0+fXKfhfo7Q\nMm/ZsmXWvp+9Bw4xKCtX/s80mEMAymWXXWb/c+jhSGRZzjY3/ztxE5mDIVWyY8eOPC0TsbRoT1up\nUqVUnV7LdZkBXygDXvMA4HyA3og/AW4Lu/Jly5YVdn0xWSjbt+fuXkc+wLT3p6MPJsrkmWeeybLl\nj7T55z4U539knSPLitzuxnt6bf4/gArhDCBV8sknn8gRRxwhfPAdpyjnXFQUlJNPTs2chXMe/e8e\nA75RBoWRI5bRgksB7YE/ATeFTjqcCORkHycFGzRoYO33I88R+QDTpr9+/fpy+umnS9++fQVLaZG7\nFvg+sqwCd45jh6/kK6SH6WazMtFUO1Wydu1aa658xhl/K5v169dnO9XWrVvtZ1UG2Wjx9AffKAOy\nyHRo7wO84XsBbgl/1TD+lTJlysjQoUNl0qRJsmnTJnuz8xzOg+t0fbmtf//+1hPw0ksv5ce4DGxY\nXmRZtgAX/myTbdIWoPfms0Cq5M8//5QuXbrIMcccI1hatJOhsDrMdrrFixdbL8iaNWtm264fvMuA\nr5QBaWRcQ0Y9ZiCTfwFuCKZz5KWXXqLNhS2uZcuW1gOQXoAUZ6b8s88+s/vQs4/xAqgwuHTGX0Fn\nie3HH3/MGmJwH8ovv/xi/zt/WB4mHq234KpVq2xZzneJ/md+iE4Aw74xP0RRIJpw1WPatGl2qTPa\n9wVt4zVxWZEP+9ixY22PCL4L8tRTT2XxxzkU2B0IJlyjDpEKOod+nyEGvDmvWXCtHjGPmKLAJ0Cy\nArNagwfUdOrUyYwbN87gxjY0momU888/386On3feeQZdZPPpp59aKzssEZrLL7/cwBTXwIbAHH74\n4WbEiBHm1VdftYZFaFbToUMHM3/+/KziuGoBV2NTrlw5a7ST9UUSb+4yd5kSwGIgp+CX3FpPwlTY\nYF7EXgeWQ3PuVuDnuXPnGky0GswTGL53hKsxtDZEL8leD5ZRzciRI52v9b9PGPCdBaLD6wFzwLQF\nKgLrgWQFrrsGwwX7oEcrizf8hg0bsn2Frn42CzvuwzJiEUxQGkQlimXXAvcZbUbTHQF/R2fty3pM\nnDjRdO3a1XocUikVLVrUKgIqogcffDBr34LeUJHBUMoeC58Eq/iiHUNLTWepNdr3us3bDPhWGZBW\neuidDDQCdgNhFPYE2CO4E6Dn4AcffGBo30BT4EgFwPfOCxGQzCOPPJIvXQh2Yj0QMbFqj8NkqYED\nUr7H6Jf+ZsBX5si4mbNJGSljoyCfLqfLjcBrQJgEUQ+l7Z62UmNqDfnxrR+l/PvlbZQiRjvi3ACF\nwUqiCXoJdjNuXzt/sXz5cvnqq69sYBMMAYSrA3BGsqbTgwcPFjgjRStGtwWIAd9HOmJbTAUuAei7\nwKg/YZA1G9ZIk/uayJZ3twgcOe2KBx/sWISKgKbS/M+H3nFFppsyfSfOPPNMwRyJNGnSxPpcxFKm\n7uN/BnzdM3Dov0guskY2d8vdcirwDyDoMqjaINnx5A7pfWpvmfjKROtXwYc7r55ATj5oHXnhhRfa\nkGYnnHCCtcCkEZVKiBnw9ygne+07mA7Wh2G1WZ39i4B9Gm6G2wnDt8xbWVe2cOFCG54MYc/tGJ/+\nArito76gNAy6/lnH6htlgAz4zs4gP709QkZINYCGNwgKnt+uvv2Obsk9gb4Aoz05whDnHNszf8K7\n774rrVq1sl18KIUsoylnX7S7HSI4n/W/MkAGAqUMkCLETihukA3SHQiabJJN1jeDPhp5JYrhUIH+\nFVhVsKHQn3vuOXFiDfA7Cv0nnPdB40ivJ3EGAqUMSMNxwFsAnXUGAkER+mLQJ4MenK8D9NUoSOhE\nROtAhjv/+uuv5Y477hBOElIZcMVBRRmIZCAQqwmRF+S8f06ek7uASQAnGP0uN8gNMhbgMIEm2YkK\nFQGjNnGy8LTTTku0GD0ugAwEVhmwrboATC6yEKgO+FXog8G4BMws3QZQUQZSwUCglcEe2SNnA5xM\n/BygkZLf5BP5xMZx6Cf95CFARRlIFQOBVgYkjZOJdOk9E2BuAT8lZfVz3VN1w2q5qWOg4Fmo1J07\nLSVzqZGTiZw7yGsGPi0VifMk7NVcDhwJjAT8pMTivFTd3SMMBF4ZkGcOFZ4H+gNM2e4HYcjz7wEG\nc/Hj8MYPHGsdszMQmvWlm+VmWQIw/ViyM/LZKXT/E1dCxgDszfh54tN9ZrTEVDIQip6BQ+AQGSJ1\nAVoo/ga4JcyR4JbMlJnSB2BA0yAsibrFi5aTegYCP4GYk0Ja8TUCfgTyFeYUZdT0tngdms+ei/Bd\nB7x+yGefOL/qKB1t5qg4D9PdlYGkGAjNMMFhqbJUxm/vTFkK5CcLpi6Qpzs/LcN+HCblDi2X566v\nvf6aTFo9SQZ8PkBqnuFO8E+6Y6soA+lmIHQ9g1gJvuaaa6yvv5McJdpxtOajJR8Dot566602UnC0\n/XSbMuAHBkI1ZxBrgzAUOKP7MgpwfkJF4eQHGDNmTErCn+d3fv1OGXCTAVUGUdhkKHFmBGK25Pzk\n9ddfz/L+Y0JVpFrPb3f9ThnwNAOqDKI0z9tvv20zJTE0WF7C3sObb76ZFVmIXoDsHagoA35lQJVB\njpZjIFHGAihoiPDhhx/atOzO4Txu/PjxuXIOOt/rf2XA6wyoMsjRQkiOYjMgMUBIfoKU7LliAjDb\nEFOzqSgDfmRAlUGOVpsyZYpUr15datSokeOb/33kQ8/U7U44cucbDhWoJFSUAT8yoMogR6tRGVx8\n8cU5tmb/SEXAOYOcQuWALEZ28jHnd/pZGfA6A6oMIlqISVMZIqwgZcCMzYULR6eO2ZUZkFRFGfAb\nA9HvaL9dhUv1nTp1qpQoUUKaN2+eZ4nMqMylx/xSqiPpaJ7H6xfKgFcZUGUQ0TIcIlARUCHkJVwx\nyE9olYgsyzZkeX776XfKgNcYUGVwsEWYS2DGjBnSsmXLfNuIv/r59Qp4MBXCW2+9lW85+qUy4DUG\nVBkcbBEmHf3111/l3HPPzbONNm7caBOTcr7AeRUqhBhEeDmfnf+qDPKkUb/wKAOqDA42zCeffCJI\nTZZv+PCqVatai0P2DJzX2LFjmdY+67OzPT8HJ4/eC1qtkDOgyuDgDfDxxx9Ls2bN8lwlCPl9opcf\nAgZUGUQog3POOScETa6XqAxEZ0CVAXhZuXKl/PTTT6LKIPpNolvDwYAqA7Tz/PnzpVixYtKwYcNw\ntLpepTIQhQFVBiDlyy+/lDp16liFEIUj3aQMhIIBVQZo5iVLlkj9+vVD0eB6kcpAXgyoMgAzqgzy\nuj10e5gYCL0yWLt2rTU2qlevXpjaXa9VGcjFQOiVAb0UaUGoyiDXvaEbQsZA6JXB999/L5UrV5bS\npUuHrOn1cpWB7AyEXhmsXr1ajj/++Oys6CdlIIQMqDKIogxogDR79uyEb4dkj0/4xHqgMpAEA6FX\nBvREdEKib9myRfr06SMnnHBCQtGKkj0+iXbUQ5WBpBkIvTKg23L58uUtkWvWrJEuXbrI7t3Muhq/\nJHt8/GfUI5QB9xgIXeLVnNQxE5KjDBo3bhw10GnOY/L6nOzxeZWr25WBdDAQ6p4BYw8wjVq5cnln\nWU5HI+g5lAEvMBBqZbBv3z7bBsWLF/dCW2gdlIGMMhBqZcCeAeWQQw7JaCPoyZUBLzCgygCtoMrA\nC7ei1iHTDIRaGWSafD2/MuAlBkKtDJz8CLt27fJSm2hdlIGMMBBqZVC0aFHhS5VBRu49PanHGAi1\nMmBblCxZUphV2REaIVH27NnjbIrrf7LHx3Uy3VkZcJGB0CsD5krYvn27pZTp1Xr37m3fv/fee/Lq\nq6/aQKmx8p3s8bGeR/dTBlLBQCEkADGpKNgvZZ5++uk2KvKgQYMSqvK4ceOkQ4cONpFKQgXoQcqA\nRxgIfc+gYsWKsnnzZo80h1ZDGcgcA6oMoAzocqyiDISdgdArA7ovr1u3Luz3gV6/MiChVwYnnnii\n0PWYadRVlIEwMxB6ZcBAJnv37hUGOVFRBsLMQOiVAXsGlFWrVoX5PtBrVwZ0mFCpUiUbz2D58uV6\nOygDoWYg9D0Dtv4pp5wiX331VahvBL14ZUCVwUFlsHTpUr0blIFQM6DK4KAyWLZsmVoRhvpR0ItX\nZYB7oGHDhvL777/LihUr9I5QBkLLgCoDND3zLB566KHy+eefh/ZG0AtXBlQZ4B5gTIMGDRpkKYOt\nW7fKqFGjpGPHjjJkyBC9S5SBUDAQ+rwJTisz3+L06dOFuQ8WL15sN9Ohs1mzZs4u+l8ZCDQDoVUG\nDGjCh3/ixIny/vvvC1OjsYfArMyOMFBqmTJlnI/6XxkINAOhVAZMnFKzZk3rrUgF4ORPcP47Lc5Q\n6qoMHDb0f9AZCOWcAR/woUOH2rbNqQByNrgqg5yM6OegMhBKZcDGbNeunVx//fVSpEj+nSNVBkG9\n9fW6cjIQWmVAIl544QU55phj8k2iosog5y2jn4PKQKiVASMjjx8/Pt+2VWWQLz36ZYAYCLUyYDvW\nr19fBg4cKIUKFYrarKoMotKiGwPIQOiVAdv0zjvvlObNm0edP1BlEMC7Xi8pKgOqDEALewVjxoyR\nUqVKZeshcHKxWLFiUYnTjcpA0BhQZXCwRStXrmxNkCPTSHBOQUUZCAsDqgwiWrp169Zy8803Z60u\nlC5dOuJbfasMBJuB/BfZg33tUa/u6aeflhkzZlh35pzzBQfkgGwGNgF/ALuBRQBlElDiIMpJOakC\nHAaoKAN+YSD06dWiNdTirxZLkwZNpFr9anLJgktkGbAK+Bn4C8gm/MgcrVE6ESWlpFQFTgLqHkQD\naWA/ZytDPygDHmBAlQEawQALAP66fwx8Dux9Ya8UmVJEmkxpYh/jmlLT/trzF78yUAZgT+BQAInd\noQ/+BnsL24AfD2KDbJDlABXKCuBPoAJwDtAcaAMcDagoA5lmINTKYL7MlzHAuwAf2uOB8wA+qMSc\n/8yRbt26udZG+2SfLAGocIg5wA6gMdAeuBagolFRBjLBQOiUAcf6o4GXgC+BOsAVQDvgVCCdwl7C\ndIDKiPgNuAy4CWgBqCgD6WQgNMqASmAoMAjYCXQEbgTOALwge2WvjAeGAZ8AjYD+wCWAijKQDgYC\nrww4H/AK0A/geL4XcBdwJOBVWSyL5VHgA6AJMBjgUEJFGUglA4G2M+D4vClwC3ANsAZ4HPCyImBj\nNwTeB74AigPsvfQEtgMqykCqGAikMmBvgMMB/qoWA6gUngGOAPwk9aW+nWQcKSPlHaAe8Bmgogyk\ngoHAKQP+el4K3A88BnDGnmv8fpbO0lm+AngdXOV4ClBRBtxmIFBzBhtlo1wEcJ2fv6TsGQRNnpan\n5R6Ak59DgMKaOzdoTZyx6wmMOTItBGkjUBag0VBQDXk4+XkCwN4CTaPfBIoAKspAsgwEomdAM+Fm\nAH0BZgD0DQi6cPmRvSAukf4bUFEGkmXA93MGXC5sBbC7PBUIgyJgo58NjANGAQ8DKspAsgz4Xhn0\nkT7WiYiK4CggTEIlSBuEAcBMQEUZSIYBXw8T6FjElYOxQAcgrEJzas6TcMXhcEBFGUiEAd8qAzr9\nnAzQbPcNIMzyq/wKn8qa0g3QZccw3wnJXbtvhwm04V8PPAGEXdgbeAjgkGEdoKIMJMKAL3sGtDCk\nuzE9/J4HMiUzZ86UyZMnC+MndurUSapWrZqpqqCftE+qA1cCtL5UUQbiZcCXPQNOlq0FaHiTKWGu\nhd69ewuTuA4aNMhmZpo0aVKmqmMDrHSX7nZ1gYpBRRmIlwFf9gyul+vla4CTZpmQH374QRYuXCgd\nO3a0p9+5c6dUq1ZNGjduLNOmTctElew5OUQ4FuDKyoWAijIQDwO+7BnMlbkZDf7BzM2OIiDZjKJ8\n+eWXS9myZePh3vV9j5FjpAZAgyQVZSBeBnynDH6RX2wsQVocZkpq1aqV7dQHDhyQVatW2cxM2b7I\nwAfyop6NGSA+AKf0nTLgXAGFS2lekI0bN8q1114rTZs2lWbNMqegHC7Ii8ORs03/KwOxMOA7Dxf2\nDCheiE0wffp06dWrl3z33Xe2TlQMo0ePtu8z9YeBW7YCKspAvAz4rmfAWIaUUkCmpUWLFvLtt9/K\n6tWrpV69ejZfYyZXFBxedsmuTFOj5/chA75TBuWlvKWZVndekeOOO84qAtbn888zs8LhcMFYDmqS\n7LCh/+NhwHfKwBke0JffS3LyySdLlSpVpFKlShmt1hbZ4okhVEZJ0JMnxIDvlAGt7BgklHENvSRb\ntmyR7du3S8uWLTNaLfLi9zBvGSUwxCf3nTKgImC+wnlApmTq1KkycuRI2bXrf2Pz4cOHC60Sa9So\nkalqwUjbyKfAmYCKMhAvA75bTeAFng+MAPYDhwDplvXr11ubgltvvTXLJ6F58+ZyzjnnpLsq2c5H\nYyyutpAfFWUgXgZ8aY78vXxvLe0mysSMZRyioRGHBhUqVJBChQrFy3tK9qcLM2MaMAmLijIQLwO+\nVAa8SAY/ZSDQaYCK2JzPnE+hxyITrqgoA/Ey4FtlwCzG5wLqlPN3k9N5i0lcmfad8yoqykC8DPhW\nGfBC2wAMkc5u8aFAWGWBLLBp5P4j/7Fp3cPKg153cgz4WhnQBv80gDkEmGE5jLJDdiAJW305EWAv\nqRCgogwkwoDvlhYjL5K++y8BLwJMJhI24VIiA5r8DrwGqCII2x3g7vX6cmkxkoJO0gmd5AXSFaCT\nTgsgLHKb3CYTAPYIKgEqykAyDPh6mOBcOH8hmXL9g4PgSkPQ5V65164cMEw8Q6WrKAPJMuDrYYJz\n8ewec/KsNcCUY0EOnc74hl2AZwEODVQROHeB/k+WAd8PExwCiiIk6BiA3WVOKC4FmJI9SElJGRr+\nauBLgAZXLQEVZcAtBgLRM3DIYA/hGWA48AJwFvADEARhivl6AF2UGdZMFUEQWtVb1xAoZeBQe51c\nJ4sAJmWlBx97CHsBP8oaWSNtgfZAO2AhoF6JfmxJ79c5kMqAtNcGqBAeAQYCdQAOI+jc5Aehw1Ff\ngCnkvgOYK+IVoCSgogykgoHAKgOSxXmEu4FvAA4ZuPzIh4uTjXsAL8pG2Sj3AccBrwLs1fwXCMMK\niRfbI0x1CsTSYqwNRm9HPlxcbSgDUDn0AKggMil/yV/W4Yr5IzkxSHuJO4FbAC/EeswkN3ru9DEQ\nKmXg0Pqz/GwnGdnt5picyuBygGNzBk4pDKRadspOmQVwYpD2EZwYbA7cBHBugL0aFWUgnQyEUhk4\nBB+QAzZiEh9IgunJDgM4pDgboGLgZF1lIBnhPMVKYBkwH6DH5RcAt58B8OHnBCGTyaooA5liINTK\nICfpfFjnHASjBm0CKIzIzOQkVQ6CyoHDjBIAvSX5K845CIIrGPyV//EgNsgG61bM1QxGZeLE5jkA\n3a+JioCKMuAFBlQZ5NMKTEZCBUHQXoGTe3zIfwLYzeeDv3v9btk3d5+UuOpvxUAFUQ5wFEdVqSon\nAexhUBGE2dU6H6r1Kw8woMogyUYYN26cdOjQQYwxSZakhysDmWUg9TNlmb0+PbsyoAzEyIAqgxiJ\n0t2UgaAzoMog6C2s16cMxMiAKoMYidLdlIGgM6DKIOgtrNenDMTIgCqDGInS3ZSBoDOgyiDoLazX\npwzEyIAqgxiJ0t2UgaAzoMog6C2s16cMxMiAKoMYidLdlIGgM6DKIOgtrNenDMTIgCqDGInS3ZSB\noDOgyiDoLazXpwzEyIAqgxiJ0t2UgaAzoMog6C2s16cMxMiAKoMYidLdlIGgM6DKIOgtrNenDMTI\ngCqDGInS3ZSBoDOgyiDoLazXpwzEyIAqgxiJ0t2UgaAzoMog6C2s16cMxMiAKoMYidLdlIGgM6DK\nIOgtrNenDMTIgCqDGInS3ZSBoDOgyiDoLazXpwzEyECRGPfT3WJgYO/evTJnzhz58ssv5ayzzpIz\nzjhDChdWfRsDdbqLBxjQO9WlRti8ebPUrl1b1q1bJ927d5f33ntP2rRpIwcOHHDpDFqMMpBaBlQZ\nuMRv+/bt5ZRTTpEePXrIkUceKY8//rgsW7ZM+vbt69IZtBhlILUMqDJwid+5c+fKDTfckFXaIYcc\nIl27dpUhQ4bIH3/8kbVd3ygDXmVAlYGLLcOeQaTUrVvXKoLJkydHbtb3yoAnGVBl4GKzVK5cOVtp\nFSpUsJ9XrFiRbbt+UAa8yIAqA5dahcOCYsWKZSutZMmS9vOmTZuybdcPyoAXGVBlkMJW2b9/vy29\nUqVKKTyLFq0MuMOAKgN3eBQ++LQziJQdO3bYjyeffHLkZn2vDHiSAVUGLjbL+vXrs5W2detW+1mV\nQTZa9INHGVBl4FLDFC9eXObNm5ettMWLF0u9evWkZs2a2bbrB2XAiwyoMnCpVXr16iVPPfWUGGNs\niXv27JEJEybI8OHD1STZJY61mNQyoL4JLvFLRVCkSBFrgtyyZUvhCkK/fv2kQYMGLp1Bi1EGUsuA\nKgOX+C1UqJA88cQTdiKRcwUVK1Z0qWQtRhlIDwM6THCZZ9obqCJwmVQtLi0MqDJIC816EmXA+wyo\nMvB+G2kNlYG0MKDKIC0060mUAe8zoMrA+22kNVQG0sKAKoO00KwnUQa8z4AqA++3kdZQGUgLA6oM\n0kKznkQZ8D4Dqgy830ZaQ2UgLQyoMkgLzXoSZcD7DKgy8H4baQ2VgbQwoL4JcdC8fft2+fzzz7Md\nwYQplKlTp2bbfuihh0rz5s2zbdMPyoCXGSgEl9u/fW69XEuP1I0hz4866ijZvXt3gTW68sor5a23\n3ipwP91BGfAKAzpMiKMlSpUqJZdddpl1VS7osKuvvrqgXfR7ZcBTDKgyiLM5OnfuLH/99Ve+R1Fp\nXHzxxfnuo18qA15jQJVBnC1y4YUXSpkyZfI8qmjRotKhQwdhGDQVZcBPDKgyiLO1+LB36tRJ+D+a\n7Nu3T9h7UFEG/MaATiAm0GJMu57XSsERRxwhzMisqdgTIFYPySgD2jNIgP5zzjnHrirkPJS9hWuu\nuUYVQU5i9LMvGFBlkEAzMd5hly5dcg0VOETQVYQECNVDPMGADhMSbIYvvvhCGjZsmO3oo48+Wtat\nW5dtm35QBvzCgPYMEmwphkA/7rjjso7mEKFr165Zn/WNMuA3BlQZJNFi3bp1yzJA4hDhqquuSqI0\nPVQZyCwDOkxIgv8VK1ZIrVq1bAm1a9eW5cuXJ1GaHqoMZJYB7RkkwT9zKJ5yyim2BB0iJEGkHuoJ\nBtRrMYZmoN3AqlWr5Mcff7Qvpk7buXOnMJ+iY3y0cOFCufnmm4XeiuXKlZOqVatKlSpV7P8aNWpI\nyZIlYziT7qIMZI4BVQY5uOeD//HHH8vcuXNl6dKlsmzZMtmyZYvdi0uK9FrkQ06TZD74NDLii4qB\nwwb+/+WXX2yuxd9//90eRwOk448/XurWrWtzL5577rnSpEkTe3yO0+tHZSBjDIR+zoAe3J999pm8\n/fbbMnnyZPn222+FKdKYSp0rBnXq1LEPMYcElStXzpowjGwxxjTg/jmFLs/r16+Xb775xioVKpb5\n8+fL2rVrre/CGWecYb0g27VrJ8cee2zOw/WzMpBWBkKrDFauXCnDhg2T119/3f6K82Fv27atnHfe\nedKsWbN8nZGSbSHaItCk+aOPPpKJEycKg6Y0atRIrrvuOmvBWLZs2WRPoccrA3EzEDplMGnSJHn2\n2Wdl5syZcswxx9gH8IorrrA9gLjZc+EALknOmjVL3njjDRsMhUMKWjHefffdUr16dRfOoEUoAzEy\nwEhHYRD8ApvGjRszqpNp1aqVgVIw+/fv99Slo4dgBg8ebDDhaDBUMVihMOjBeKqOWpngMiDBvbS/\nr+y7774zLVq0sEoAUYrM4sWLPX/JCJ5iRo0aZWDDYLBaYe69916D+QfP11sr6G8GAqsM0P02Dz30\nkClWrJjB5J6ZN2+e71qKSoE9BSxVGgxpDIKu+u4atML+YSCQygCz9ebMM880JUqUMM8//7zhQ+Vn\n+fnnnw0CqhgsbRrMJZg///zTz5ejdfcoA4GbQJw9e7ZwqY5GP2+++WbGJgZjnLKJa7f//Oc/0qtX\nLznttNPkgw8+sPYNcRWgOysD+TAQKGUwbtw4ufbaa6V169YycuRIQc8gn0v351e0WWCwVRo8MVdD\npOekP69Ia+0VBgLjmzBmzBgbm/Cmm26SsWPHBlIR8KahQxSNpGjefNZZZ1kDJq/cTFoPfzMQiJ4B\njXcuvfRSue2222TQoEH+bpEYa09DJZo17927VzA5qkOGGHnT3fJmwPfKgP4AjDjUvn17GTFihNB/\nICxChylaSzLCEo2oaEatogwkyoCvlQGt95o2bWqv/dNPPxUsIybKg2+Po18EfRweeOABefDBB317\nHVrxzDPg6zmDAQMGCIyKrClvGBUBbx86SD355JPy6KOPipMENvO3ldbAjwz4tmfA2AKME/Dwww/L\nPffc40fuXaszlq2tSzTjKHD+REUZSIQB3yoDrhpwaY0ux1xmC7swBgMnFKdPny7nn39+2OnQ60+A\nAV8OE3bs2CGw3Zc+ffp4RhEw/fqCBQsSaAJ3DmFil7PPPltefPFFdwrUUkLHgC+VAe0IDhw44Jmc\nhosWLbJxCJhLIZPSo0cPmTBhgmzdujWT1dBz+5QBXyoDmuLSCu/www/POO2MZtS/f3/hykamhXEZ\nuLQ6ZcqUTFdFz+9DBnypDGiBxy6xF+T++++3y3peqAutEmlzwWVWFWUgXgZ8pwxWr15tu8GOfUG8\nF+zm/u+++64wXBrjJHpFaHPAYYuKMhAvA76Ljgx3XnuN9ErMpHBp85133rETmU4U5EzWxzl3tWrV\n5KeffnI+6n9lIGYGfKcMGIaccuSRR8Z8kW7vyHV9rmQwlqLXhGHbHY68Vjetj7cZ8N0wwQt0Ugkw\nr2LFihW9UB2tgzLgCgO+Uwb85aNkavmMjlHjx4+3qwccJvDF1Q3KkiVL7Gc6EGVK2CtwOMpUHfS8\n/mTAd8ME59d448aN1lsv3bRv2LBBmPeA7tKOcNhAoeERQ7EPHz7cJlxxvk/nf9avUqVK6Tylnisg\nDPhOGTBNGecLuLzImfN0yz/+8Q/hAxcpu3btklKlSsnjjz8uNJPOpHz++ec2IUsm66Dn9icDvhsm\nkGYuK37yySf+ZDyFtaZSQih4QTDYFJ5Fiw4qA75UBm3atLFWdr/++mtQ2yWh6+JcBocstM5UUQbi\nZcCXXot0VOK4eODAgTZacLwXHdT96azELNFMIquiDMTLgC97BkyHzijIjHfIFOgqYtPIc+h0yy23\nKB3KQEIM+LJnwCvV4Cb/a28NbvI/LvRd4gz4smfAy61SpYq1AnzssceE6dXDLEjBZm0cGP5MRRlI\nlAHf9gx4wRoQVWzcQw2Imujtr8dFMuBrZcAL0VDpGio98obW94kz4NthgnPJdCHm7Pnrr78uSErq\nbA78fyZRueiii2x4eJpEa86EwDd5yi/QdxaI0Rhp2bKlTaDSpUsXQcZleeaZZ6RwYd/ruWiXarfR\nRblVq1bWO1GzKeVJk34RJwOBUAa85s6dO9tfSS450m8hDIlX586dK8cee2ycTa67KwPRGQjUz+eV\nV15pw6fPmDFDTj/9dPn666+jX7VPtzIle+PGjW26efYINAOzTxvSo9UOlDIgx82bN7cz7GXLlrUP\nzgsvvCD79+/3KP2xVWvz5s02fkL37t2lZ8+eMnv2bHVTjo063SseBmCwEkjBsqN56KGHDNKuGaQg\nM/gl9d11Yv7DwIbAIFOSOeaYYwyiHvvuGrTC/mGAji2BFuRiNC1atGDAAXPZZZcZePV5/nqpBJAk\nxtSqVcsULVrU3HvvvQYh2T1fb62gvxkI3DAhZ6+IS4/Tpk2TiRMn2olFhhK/5JJLZPLkyTYRS879\nM/n5t99+kyFDhkjt2rWlW7duNl7D8uXL5YknnhCGQVdRBlLJgO+NjuIlZ8SIEXL77bcLIxpzJv66\n664TJh/JVLhzWlHOmjXLZpJmpCQmQeHKCG0mqlevHu/l6f7KQMIMhEoZ7N271yZf2b17tw1xPnr0\naGusxJiF7EG0bdtWzjvvPGnWrJnQM9IRpnJz026BYdPmzJljMyazx0IDIkZvwnBA/vnPfwonP1WU\ngXQzECplwAeNv74LFy606dxJNkZ5NoQarRg5dGBWZ1rzYdJRGjRoICeddJIsXbpU6BBVuXJlKVIk\ndtMMpl5bv369fPPNN7Js2TL7mj9/vqxdu1aKFy9uhwGYxxDGIeD/+vXr2+Cq7B2oKAPpZiA0yoDD\ng+uvv16YBYkPXl7CZTz+anMdn0qAqcrYo6DwIWXwEHpMsufAVPAlSpSwCoL7sMfB+Arbtm2zLtZO\nchX2Khi7sW7dulbB8OGnc1FkKnnGdGRKdayASL9+/fKqnm5XBlLGQCiUAX+ZGzVqZKMiMTpSrPLK\nK6/YbjsfUgY7ZQwFvjis2Llzp33wqQA47ueD7SgHLAVahcGsT3zVqFEjpglATh727t3bhnSjibWK\nMpBOBgKvDPhL3aRJE/sLTvPdWLv5jDJ81llnWYOlCy64wI7v09Ew11xzjbWiZHp32Bak45R6DmXA\nMhD4pcU777zTjtHffPPNmBUBHYEYdJXzCRTnv/2Q4j8vv/yynZto37591vAkxafU4pUBy0CglQET\nmvzrX/8SdvePO+64mJqcXf7LL79cGHmZqwjpFtoT0CWZcRpuvfXWdJ9ezxdiBgKrDJhmrEePHjZw\nKh2YYhXaIHC1ga7QmRLOMbz22mvy6quvWtfsTNVDzxsuBgKrDOjQw/kBOirFKvQKfPHFFz3h2ESb\nB9od8DqYw1FFGUg1A4FUBrQl4Is5DzmzH4ssWrTIrhxE2zedcwaR5x8wYIA1gOL8gSaMiWRG36eC\ngcApAz40TIp6ww03SKzLc1u2bJHWrVtnZI4gv0al8dMbb7xhly5popwppZRfHfW74DAQOGVwzz33\nWOOgWMOGc26gXbt2NsW7F+Me0MiJadMYsOXRRx8Nzp2nV+I5BgKlDJhRiEOD559/PubhQZ8+fayV\nYSYnDAu6K2gn8dxzz1llgJgGBe2u3ysDCTEQGKMj/qrTn4CGOlxSjEXGjBkjNPIpSJiGnb/MmRYG\nfOW1MdNyrEulma6znt8/DASmZzBs2DC7Ns9f0FiFLsz0VyhdurQ9JFbrxFjLd3s/XmO1atWEE4qa\nY9JtdrW8QCgDThrSwYcTh1yjj1Vobsy1fNokvP/++zaVORUCHZK8mIeATlE0SPrhhx80wWqsjaz7\nxcxAIJTBI488Yh/eBx98MOYLj9wRcRKt+TG9CdlLoMEPVyK8qBBOPPFEGwaeXphUZCrKgGsMYLnK\n14JAIQaxAczQoUOTvg7ELzCwWswqBz0GA18BG1g1a6NH3jzwwAP2umEf4ZEaaTX8zoDvJxBpTzB9\n+nQ7X4DgoQkrSQROtYFMOFHICUOvC/0mmF6NPgycUDziiCO8XmWtn8cZ8PUwganYaULcv39/SUYR\nsI1o3MNIRsy74AdhwBTml8SvkY2ZmAmnKj/wpHWMnQFfKwNGDT7hhBNiWh4siBIqg44dO7oa67Cg\ncyb7PeMm0iCJSVWoEFWUgaQY8Os4BxGHbIIUuCcnfQnMpQASDeITJl1WJgrAkqPBCohBcNVMnF7P\nGRAGfNszoD1B+fLlrYtyUtoQB7O7zVl65mf0ozDQa9euXW0PicuOKspAIgz4Uhkw6jANcBgvkFGG\nkxEodRk7dqx06tQpmWIyfiyDuDDoKg2SGJdRRRmIlwFfKgOGMKMFHlcSkhX6M2zYsEGuvvrqZIvK\n6PEMxspw7wzDfvPNN2e0LnpyfzLgS2XAOIH0NHRjOY1DhFNPPVVOPvlkf7ZgRK3ZM2BimJEjR9qe\nU8RX+lYZKJAB3ykD5jJYsGBBnoFICrziiB0Y75Cz8VdddVXEVn+/bdWqldASk6bZ5ElFGYiVAd8Z\nHTFeAbvDq1ativUa89yPGZQuvfRSWb16tc27mOeOPvuCNgdMLvv1118LQ65zCVJFGSiIAV/1DDjZ\nx3BmtAdwQ2hb0LRp00ApAvJCgyS6Z9O3gr0eNUhy424Jfhm+UgZMbMIJMkcZMKXZRx99JIxqxDRo\n8dz0nHF/7733soYIyZTlxduEy64cAjFxTKIOXPTkVFdpL7ZuaurkK2XAh5cuyqeddpowJ2Lt2rWF\nGY27d+9uH2wmPolVIUyYMMEuwXXo0CHpslLTNMmX2rBhQ2HKNqaG++CDD2IukAFUmI6OEZp1mTJm\n2vy/o5+Mp+rUqWOQ18AgqpFBLAKDhz+r+ghbZhCsxCC8eNa2/N7gRjdwU3alrPzO44XvEMDFHHbY\nYQa+HAVWBz0vwxeGF9YqE0lkCzxGdwgGA3R08YWsWbPG3pzTpk0zs2bNsu/x656t7ghwYkqVKmWQ\nFDXb9pwfEAzFuv8iJkDSZeUs24uf8etu0EswWEI1MNiKqYr333+/KoOYmArOTr4ZJkydOtUGHmEA\nEqZVp5xyyinZumZMeU7rRK4S5CeMFkShrUKyZeV3Hq98R4Mkzh/QuOrGG2/0SrW0Hh5jwDfKgJ55\nzZo1E0YlousyhS7HkVKhQgX7kT7++QlXEbj0VrZs2aTLyu88XvqOAVS5wkAjK2aNUlEGcjLgG2Uw\nZ86crFgDP//8s102o2KIFCYtpWzatClyc7b3zLCMYUbWKkIyZWUr2AcfGAzl4YcfljvuuEO4MqOi\nDEQy4AtlwF96PuDnnnuurbsTzTjyQvjeSYJSqVKlnF9lfaadApUGjY0oyZSVVaiP3nCZsUWLFsJk\ntMwkpaIMOAz4QhnwV4zeiVzuohx99NH2wadtQKTs2LHDfszPz4BDBKZc5ziakkxZtgCf/WHkZ/ov\nMDIUPTUdBeqzy9DqpoABXygDpkhnghQntBntCyjr16/PRsnWrVvt57yUAc2OqVgifRESLSvbiX32\n4fDDD7cm3TTUQmBVn9Veq5sqBnyjDBo3bpzFAROfsKcwb968rG18w8CgVBo1a9bMtt35wF4Bcxey\nm+xIomU5x/v1f/369YUxEGi9SWMuFWXA83YG8Cy0NgEIfJptQfeuu+4yNEKCxaHdzrV0KAHDEGZ5\nCZYeTc+ePXN9nUhZuQrx6QZESTJYVTGYl8l2BTfddJO1M2B4OZVwMOB5r8VvvvnGxhqg9x1/zRxB\n8wgMY6xnHhOecIKRXf5rr73W2SXb/2XLllm7BAYzYSalSIm3rMhj/f6e8y5nn322NTvmEAoGWzZS\nNE2YafLN/I7MR3nBBRf4/VK1/gUw4HllQGMZTnTxJnUm/SKviRNgnCuoWLFi5OZc7/v27WvX2WHJ\naNOn5doBG2ItK9qxft5G/w4kkJELL7zQcuTna9G6J86A5+cM+IvOYKXRFAEvm266BSkC7sdQafR2\n5Gx6XhJrWXkd79ftzFzN+RRyNHjwYL9ehtY7SQY8rwycYUIy18nuL1cS/B7nMBkOCjqWw4BHH31U\nMH9i3cEL2l+/Dx4DnlcGjGjEnkEyQhPck046ya40JFNO0I/lUIpWijRIomWmSrgYCLwy4DwArQ4j\nbQvC1cSxXy2HUAymytTvHFKpQVLs3AVhT08rA/jSy/bt26V69eoJc00/BP7KqTKIjcJy5cpZgyQG\nU73vvvtiO0j3CgQDnlYGDHFGOQ4ed4kKhwg0Y2aEJJXYGGAkKSapGTRokFUMsR2le/mdAU8rA/rf\nU6pWrZoQz1xDZ+wC7RXETx/tNZiM5brrrhOmq1cJPgOeVgYbN24Udlsd1+R4m2PKlClC5yUngGq8\nx4d9f+azpJ8Hg8DQzkMl2Ax4XhlUq1Yt4Rbg2jkjIyXas0j4xAE5kPEiaPRFV+cePXoE5Kr0MvJi\nwNPKgBN/+cUmyOuiuJ2/ZIyArEOE/Fgq+DsqYypVKgX2FFSCy4CnlQHNjBPNBkRPPERMliuuuCK4\nrZemKzv//PNlwIABcvfdd9s8DGk6rZ4mzQwEVhnw14y29kwmopI8AwhBb+NGMs8EQ8epBI8Bzzgq\nvfTSS3bWmuNU58XlLUY8bt26ddY2fkevQ0Yoykt++eUXO7x47bXX1AQ5L5IS2P7bb78J40pw6DZz\n5kwpUqRIAqXoIZ5lwCue2k8//bT1n8fDbnK+EOHI4MYzsJCzLyw55lttBO0wWIEoMH9CvoXol1EZ\nQBZsyy2Cqkb9Xjf6lwHPDBPat29vFeaff/4pOV9Mnc7xP81l//GPfxS4OsAhAlOtIaGKZ5WwXyvG\nXBUvv/yyPPvss9bMO9p1IElNtM26zeMMeEYZIDVarqQoObmDzi1wiYuGSgxgoqsIOdlz73Pnzp2l\nV69ewpBx9CqNFCalqVWrlvz++++Rm/W9DxjwjDIgV3yA8xuH0viIyUDzE/rk01CJ3ncqqWPgmWee\nscqbBkk07KJT0z333GMNlGiXwAzOKv5iwFPKgEMFDgeiCSMjM/xWXkFOnGM4RGA5nGhUSR0DbI9x\n48YJnckYJ+K8884TzPvYEzJIDNtBxWcMeG26g0FNQWHU1/z58/Ot7rfffmuPmzFjRr776ZfuMTB0\n6FBTpkwZO8Eb2W6c8GWCWxX/MOCpngH1KIcKTn4EfnaEAU5OP/1052PU//w1Yv7F5s2bR/1eN7rL\nABSB3HbbbTbZbc4eHaJWawh2d+lOeWmeUwbs4nP1IFI4j4CQ3pGbor6nMqBTUuHCnrusqPX168Zd\nu3aJM4nIuQI++NGE7uMq/mHAM0ZHkZQxfoETy4DbuaRID8acWZcjj2Eo9YYNGwqGEgX2ICKP0/fx\nMYBOr7XsnDZtWoEHcu6A4dbVCrRAqjyxgyd/Qhka3Rkq8IZisM78FAGZ5K9QLEMJT7Du40pQMY8d\nO9bmU+Bl5NcLo+LgUqOKPxjwpDKIHCqwC1qQ+yxvOt6gVCIqqWeAuRpp6s3eQZUqVWy4+rzOqkOF\nvJjx3nZPDhNIE3sCdIjBTLX1p2duxbzk448/tunav/76axuMI6/9dLv7DHD+oF+/fta9mb2EnEFU\nuY1DhSOOOML9k2uJrjLgyZ4Br9D5lWf4rfwUAfflr8+pp56qioBkpFloCEYDJM7VMOFttGEDQ8+p\neJ+BjPYMtspWWXYQP8gP8uNBbJJNsm3uNtl29jYpuqio7G+4Xw49iBJSQsoBVQ6iqlSVUfVGSdtO\nbeXJ+560e3mf9mDWkKtAAwcOlEceecReIJcbqRyYy3H27NlRL3rPnj3WpJmZs2AnYieKkexV+GJk\nbCTUFe7DF+eRaHTGUO6lS5e2vUcOU/g64YQTrIcrvVwTjYERtYIh2phWZcAHf85BzJW5eOQ3WarL\nS3mpAfDB5kNeGSh1oJQMu2iY9P2orxQFcDtY7JbdAjWRpTg2yAb57sB31rnpkEMPkdrAOcC5B1FR\n8s/BGKK2Ttul8qHu2rWrLFy4kFm+7WoQo1YdddRRNmz9nDm4C/Di8I6+DRxasPfHngUjKzkPOFch\n+OBTAfBFZeMoB5pAM9kulQZXmlauXGmtIXmRHGLSzf3cc3EX4EUFoVIwAylVBgfkgMwD3jmIdbJO\nDgPOAs4GGgB1AT780YSNHEv8wv2yX1YCVDbzgY+BLwBuPwNoB7QHjgdU0sMAlQBcyaVPnz72AaYP\nAx9eprrjChETvTI+ZZMmTezDylD23J6MsHz2MLjMTGe1uXPnCmMwMJckz89Xs2bNog5lkjlvYI5F\no7kuP5mfzP8BxwIwLDYnAw8AC4H9QDpkh9lhPgC6AeUB1qM58CbwJ6CSWgbghm7gNGbOOOMMayJO\n8+Ru3bqZDz74wOBXPbUnP1g6ehwGvRPzwAMPGER5tvU47rjjzP/93/8ZTE6npQ5+Ogm7ca7JSrPS\ndAWKAnwA7wC+BjIt+8w+Mxm4DDgEqAgMBHYCKu4ygEC0BvMGBpmxDX7pzWWXXWYmT55sMMlrsPLg\n7sniLA2rTYZBWTD8MJh/MBjKGAwv4iwluLu7ogzWmXVWCfBBqwmMAHYDXpQNZoO5FygNHAUMAvYC\nKskxgIQ1BhmYDOYFDCb3DGImmoIiUiV3xsSPxryDGTFihKFTHBUWlcK6desSLzAgRyalDPiL+yRQ\nCjgRGA38BfhBtpqt5n6gBHASMBNQSYwBxEM0yHJtMNln7r//foOo1okVlOajsNphRo8ebWC5ahAV\nyzz55JMGk5RproV3TpewMlhulptTAT5MjwJ7AD/KarPatAE4p9AD+ANQiY2BP/74wyDakR2LI8yc\nWb16dWwHemwvLFuaRx991Coz2KuY5cuXe6yG6alOQsrg3+bfpiTQBFgFBEHeNm/beQ5Odn4FqOTP\nwFdffWUn5Tj+fvvtt/Pf2Sffrlq1ymB1wwZ8/fe//+2TWrtXzbiUwQFzwE4KIkaxuQ/gMCFIwrmP\nswDOJ3wIqERnYOrUqXZeAGv5gRtrc5iAVPQ2CjcnG+EbE52EAG6NWRlwOe4qAIHMzetAUIXXeS3A\nFZFRgEp2BkaNGmVn4mEmbrh8GFTh6gdD9iPYTqCvM7L9YlIG7BFcDfAXMywTbfeYe0xhYByg8jcD\niHloYF5sEPg0FJRwYpQrI4jxGIoeQkzKgPYC7BFMA8IkvUwvUxyYBYRdZs2aZWAybBAiPVRUwE3b\n9hDCkDSmQHPkN+VNuQp4A+gEhEm4xNABoD9F/9f7S+HfC9vszlhTt6G+GGuBUZhpN0/vPbrp0v6e\ntvGwdAtMhGa6ktMrlHb+b731lvU1CNN9wPD7jM3Zv39/6ztBvwi6brP9+aIzluNAxTD9vAcqVKgg\nxx9/vBx22GG+oSpfZbBW1sppQGdgKBBG2SE7pD6w7sh1gmGSlCldxjrV8Abgi9mf6FGHZTZrB4+f\nTUsTv6PTDTMQ1a9fX84880zrvUdvOz8Jr4c5KDDTLkuWLLHxJfxUf7fqesstt8grr7xi275s2bJW\n+dOXgu1MRyveA3SiYjapyOCwDAQDU2h7DzBPZfPmza2vhFv1crOcfJVBG2kjq4DFAF2IwyoLZIE0\nBf4DXAvkJbwJmPSVWZ3WrFkjK1askP/+97/WcYZedQzsSnfeK6+80gZu9UNsQEwYCnwKrIMRb+aw\nCh92xthkaD34V+RJA5UnnaPoNMV74IcffhAsw8qXX35plSl/POidecUVV9h8E3Xq1MmzrLR/kdcA\ncI6ZYw1xppqpee0Squ3Xm+vNMUCixlW4OcyYMWMMFIFdx6a13g033GBww3iWRxrjwOPPGhZ5tpJp\nrBiXVPGAGrhfJ3RW+mYwp8ftt99ueWVZ6CmYDz/0xjJ2nhOI9PC7AFD5m4GNZqO1thxqhiZNCX45\nzJAhQwzyS9pJOYQN8+TyFROkUGnBlTzpaw5KAS1atLAPcLLXQ4/KKVOmGAT7tQrmwgsvzLjNRlRl\nQO9DmudOBLwg7733nqFzSaaFHpkNALfEce7hA4cEMQYBQKIWzV4FZ/PTLYg5YLrCiSeTggSu5qWX\nXrKOTxizG5pAZ1ImTpxoH143vR25hEmnKUw+mo8++ijX5WGoYV588UXrXJXXPZLroIgNsT4/UZVB\nP9PPVAUy7XRE4jFOs+Qjp1/E5WXm7cfmY6skl5qlrlaArrX0s0f2YoM5h6yyEUjU3HXXXfbXGZmL\nsran483SpUst7wgSko7TRT0H0+VVqonPh8sAAAvXSURBVFTJIPCJXd5jt5pORVSOmRI6NyHgjnnw\nwQddrQKHEBxC0tApctjwxBNP2J7Id999Z9gWtWvXNogQFdO5431+oiqDpqapuRHIpCCJiuGLFmC8\nCbygDGh8dQTwLOC20N0X4b7MpZdemlX0ggULDCYg7fWnWxk8++yzBkulGTW2ufjii+31kxAqRoTM\nt1x07949i6NMvLnxxhtN06ZNXT81TZ+pEOjvwfuBwwisVhhEbso6F3tHbJf169dnbYv2JpHnJ5cy\n4AQZDW1GAl4QusR6RRmQj9bAlUAqhAYuvFb+d4RDCW5LtzLgTdm6dWunGmn/v2jRIuteHHlixDu0\nDwfdpTMpI0eOtHM9nGB1WxgcBkvSBukEDew6bM848hwcLtP4CzYPkZvzfB/P85MrVPr38r3sBbi2\nrpKbAfLCWIupEExO2Rh98JhLRfFxlclYgrSPyJTQaIup3iOFxlxc3uPafSaFvNDw7Pvvv3e9Goir\nYONGYuXJBoylnUqk0LiJy5s0/nJbcikDhi+nVABUcjNwlBwlvwCpkksuucQG8kxV+bGWS3sJWtJl\nSmjNyVRuOQXdY8HwIefmtH6mdSGFHKVCMFS0Rmz4ubfWrDnPwfNTEfF7NyWXMvhVfrXlHy6Z1b5u\nXqSbZTGsu8ORm+U6ZR199NE2nLjzOVP/aUnnNaMohlan4Rb8BDJFiz2v0zMhR6kQ3gOOYKXJeZv1\nn6bvNF5yWxnlUgalpJQ96R/yR9bJ9c3/GCAvDkf/2+reO4wZba4A90pMrCTecDSx9orQ5Pehhx6y\n1n+ZNul2eCFHqRDeA45E6x2RC+aZcJSSs2+y/3MpgyPk75x4qewKJ1vpTB7PYZTDUSrq8dlnn1l/\nhlSUHU+ZzEqEWIbxHJLSfZl/4c4778zoPIZzgQ4vHMqkQj799NOsYh3Fk7UBb+goRZPmZPNMRJbJ\n97mUwbFyrN1nhazIua9+BgPkxeHIbUKYdWj8+PHWd8HtsuMtD9aR1rci3uNSsf/LL79slQDiLKai\n+LjLpM8JhRylQmD5KVi6FE4mco4kp1AZ0fnJbcmlDPirVxNg+jOV3AwwQ9SZQCxC99ZYhZNBWL+2\n43QEGY31sJTtx5tx3rx5KSs/1oLfffddO1HWpUuXbIcwPVumhLzwlznWnkE89wEdw+ADIQjQKrwP\nmIEq8nhYZNpUch06dHD98nMpA56B6c9mAF4QZ5KGXmOZFqaHYxo38pOfcFmOk1x8oGIRjgFvuukm\nQbIR4c3AXwRHMnX99K6kpyXyCThVSfv/6dOn20SuzLEIXw77ev75563ShIVk2uvjnJD1Ij/5CYzk\n5IUXXrBxIOi5GovQGxLOa9K7d2/hMjOHRWx/BJzNOnzs2LHStm1bmyouayPewC5BWrVqlWvyOa77\nJ5q1wnQz3ZrdZjIbEtNf0QoOyyjW6Aa/DFHttqPVP1Xb+pv+pgIQLT0bbehpHUZ7frSNDaiJcXeB\nVUGX05qbYv3YIHV5tv2Ziahjx462PPLA8tNliovZast9rMYt2SruwofFixfbXAbkMueLXEWabbtw\nupiLoOk46wOFkOsYWhByO361DdPJ0XqQ+6InkWvfyA30t2AQVu5PK0s6MTmCHxZrfMSkNM8884z1\neIx2D9BMm+d6+umn7aGJPD+5LBBZEs1ujwVuA1T+ZoAKgC7MdwGRgskec91111mrMDYmZn+zbl7G\nz8tLaE4KzW+DizIPIG9+rwn9IujCTMWg8jcDtATFXEE2M22aDj/22GPWZ4EPJBUB/zuvaIqDpdGa\ncPjw4dbikElckKg2T5q3bNmSbzvQGhK9BvP+++/nWUZBX0RVBjxoMECz5DWAijEvAOQDHhOGDUMN\nXL16ddvgzNvnNHzkf26PFHTZbIMx/yDTesGizmp7mhx7URhrgaav6O56sXppr5PDx+DBg23mJfbk\n6HrMH4CcCiDyPpgwYUJWXRmKnY5GjGlAHwTyS1+LgnwNsgrI4w3d4llmMhmh8lQG/CWsDnQCwi7b\nzDZTfn95035qe3P55ZfbB5kPc2SD5/WeAU2wLGaYY4A3DF/nn3++VQp++MVl74DDHS84imX6PuSQ\njT0l9uj4ILPNY7kP+vbtazM/896hmzKPo4cqs0HTAcsNoT9Lsolt81QGrCDjGTCuAdOYh1Xo/VX7\n4dqmcKW/x3/5/QJEUwjcv169enYsyG7c9u3bfUUllQBddhGmy1f1drOyHNPffPPNWco/nnvAGTZy\naNGuXTvz3HPPeTbzc77KgIT2BA4DgpJGLd6b5N759xq5V0yl4yvZmyGeG4HKIdpkT7x1yPT+DNXF\n+ZD8xrSZrmMqz895IU5aclhHHviKpUfA9uf9wuzUfpAClcEus8tG96lhapjNQJhkkplk0LE3DwGU\nb775xjz++ONZKwbOjRGtR+BsC0rIMJgC2xt70qRJYboFbDeewVW4SsRuOHtKdGHmvA/H+2znvOaM\nnO/YG/CDFKgMeBE/AUy5zpBfvwJhEEY1YnLZ64BoQt96huNiTDxq/7wmkeBdFu1wX27jqgns8WOO\ntOPLi4yoNCd8qQS4bMelupzC1QBODnICEH4CURUDIxfxB8QPEpMy4IV8DxwN1AGYoDTI8o55xwY/\nbW/ax5RcljYGnA/gBBOXiPiL4HQjma04KMKZ6vbt29swbDltIoJyjc51wNjKIIy5gQehiUWh0zZg\n7ty5drKYk4y8B5wfCfaq/CAxKwNezAagLlAF+BwIogwyg2yOxZvNzWY/EK9whYBBLXv27GnHmAsX\nLoy3CE/vz5uek2kcIvllLBwvoTABtiHo6tata8OPxXs896ex0IABAwwCofgmN2VcyoAXyWFCK4Bj\n6ScAGigFQTgfcgnA63oScENokeaH5cNErvXJJ5+0v3wIxuLa8lgi9XDzGLYXA5DyFx2mvYbDBDfE\nq3YkOa8tbmXAAqgAngKYtvxs4CvAzzLajDYVAVoYfgqoxMYAZ9nZJa5YsWKueIWxleCdvTicg7+B\nnQx86qmnslkYeqeWqa1JQsrAqdIX5gvTBOCvKTM1bwX8JKz/OQBTr3NYEJbJUTfbiL+ezrCBATwj\nI/m6eZ5UlQV3YMMMy+wNNGnSxHf1d5OXpJQBK8Jx9TDgKACJSc19wBbAy7LILDJtABpUUZktAFSS\nY4Bh3fkwceIMcQcMoxt7WWhSTucg+o8g1qMZNmxYKHsDkW2UtDJwCttpdpqBAJVCCaAb8BngFWEI\neA4HOKyhEmgEeCVjlFc4cqMeTNzRqFEjqxTY7R49erRJRUjxROuKSFIGiWTtigiVwMCBAw3Dk6sg\noIbbJFApvATUA/jQcSnyYeC/QLplr9lrJgM9gPIAhzNcLpwGqKSWAdrKcxmS3W8m/aBrLl2yMzGZ\nxkQ0Dz/8sF0qZM+F5uG0EVElkP0eyDclO4hLSubLfBkDvAtsAI4HzgPOOQh+dlP+kr/kC+Djg5gj\nc2QH0BhoDzCdemVAJX0MwBzbBmxhgA4ss0qZMmUEcwtyzjm4C/CCUY+NeOxmjVavXm1zDjCaMnJU\nCj8jMYnAUUg6d+4sGM64ebrAlJVSZeCwxC7CAmASwAf1c4CJWsoBdYC6AEOtVTkIPrBlgBLAoUBR\ngPvvPohtsk1+BDYB64HlwNfAd8CfAHM+nA1Q8bQBjgZUMs8A4/kxmg8fUOQNFHjsCSz0BB58AgMf\nG9ePYcKZLAWp5mwIOIYK5wumv8KIR4x4Bcs/GxSUigaWoPbFuISMMIXgIwJnMGGyET70VDyMAITE\ntlHzMGSeFe/UIC3KIOfl8sFeBCwFmJ2IWAX8DPDXPVYpKSWlKlALOAWgUmHGo9qAivcZgK+HLFmy\nxD7EWNoTJBcV+HIIfABirjyGIYKlTZtlCEZCwtepp54qmLewCiTmgnRHyYgyyIv3A3JANgP8xWd+\nAqcnQAVRHHB6Ckzwwl7EYYBK8BhAoA77a49ly6yeANOZ8cF3egqME8keBLMLwRoyeCRk4Io8pQwy\ncP16SmVAGTjIgKpUvRWUAWXAMqDKQG8EZUAZUGWg94AyoAz8j4H/DyXjXBPYfCluAAAAAElFTkSu\nQmCC\n",
      "text/plain": [
       "<IPython.core.display.Image object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "current test set size: 2731\n",
      "of which positive: 1308 (47.89%)\n",
      "rnn score against target on test set: 2731 (100.0%)\n",
      "extracted dfa score against rnn on test set: 2731 (100.0%)\n",
      "extracted dfa score against target on test set: 2731 (100.0%)\n"
     ]
    }
   ],
   "source": [
    "wrapper = all_my_rnns[-1]\n",
    "wrapper.rnn.renew()\n",
    "dfa_index = -1 # if you want to check the DFA from the last time you extracted something for this network\n",
    "dfa = wrapper.dfas[-1]\n",
    "test_set = wrapper.train_set \n",
    "print(\"testing on train set, i.e. test set is train set\")\n",
    "# here we're printing things on the train set, but you can also try other sets if you like\n",
    "# for instance you could also make one by running make_train_set_for_target(wrapper.target,wrapper.alphabet)\n",
    "\n",
    "\n",
    "from math import pow\n",
    "def percent(num,digits=2):\n",
    "    tens = pow(10,digits)\n",
    "    return str(int(100*num*tens)/tens)+\"%\"\n",
    "\n",
    "dfa.draw_nicely(maximum=30) #max size willing to draw\n",
    "n = len(test_set)\n",
    "print(\"current test set size:\", n)\n",
    "pos = len([w for w in test_set if wrapper.target(w)])\n",
    "print(\"of which positive:\",pos,\"(\"+percent(pos/n)+\")\")\n",
    "rnn_target = len([w for w in test_set if wrapper.rnn.classify_word(w)==wrapper.target(w)])\n",
    "print(\"rnn score against target on test set:\",rnn_target,\"(\"+percent(rnn_target/n)+\")\")\n",
    "dfa_rnn = len([w for w in test_set if wrapper.rnn.classify_word(w)==dfa.classify_word(w)])\n",
    "print(\"extracted dfa score against rnn on test set:\",dfa_rnn,\"(\"+percent(dfa_rnn/n)+\")\")\n",
    "dfa_target = len([w for w in test_set if dfa.classify_word(w)==wrapper.target(w)])\n",
    "print(\"extracted dfa score against target on test set:\",dfa_target,\"(\"+percent(dfa_target/n)+\")\")"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "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.6.3"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}