dfa_from_rnn.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# RNN extraction\n",
    "\n",
    "### Welcome!\n",
    "\n",
    "This is a notebook to let you play around with the extraction method described in our ICML 2018 paper, [Extracting Automata from Recurrent Neural Networks Using Queries and Counterexamples](https://arxiv.org/abs/1711.09576).\n",
    "\n",
    "In this notebook you can train and extract an LSTM or GRU network on any language you like, after which it will draw a neat little DFA for the language.\n",
    "\n",
    "#### Quick Start\n",
    "The easiest way to start is to just \"run all\". This notebook will train and extract an LSTM network on the 3rd Tomita grammar (it tends to learn that one pretty easily, and it's more interesting than the first or second grammars). But you can also do your own thing: we import implementations of all the Tomita grammars here, and you can ask it to learn any one of those instead. (Tomitas 1-4 and 7 generally train pretty easily. Tomitas 5 and 6 are more difficult...)\n",
    "\n",
    "You can also define any other language you like, including over other alphabets. For that, just set the `target` and `alphabet` variables. \n",
    "\n",
    "Other than that, the different things going on in this notebok are explained if you browse through it. \n",
    "\n",
    "\n",
    "#### Extracting from a Pretrained Network\n",
    "In addition to training a new network here, you can also plug in a pretrained network. For that the network must implement this simple API:\n",
    ">1. `.classify_word(word)`       returns a True or False classification for a word over the input alphabet\n",
    ">2. `.get_first_RState()`        returns a continuous vector representation of the network's initial state (an RState, as a list of floats)\n",
    ">3. `.get_next_RState(state,char)`    given an RState, returns the next RState the network goes to on input character char\n",
    "\n",
    "The provided `RNNClassifier` class implements these functions.\n",
    "One example of a continuous vector representation of all of a GRU's hidden values would be the concatenation of the $h$ vectors of each of its layers. For an LSTM, the $c$ vectors are also necessary. The mapping from hidden state to continuous vector must be consistent, or the abstraction won't make sense (i.e, the vectors should always be concatenated in the same order).\n",
    "\n",
    "Given a network `rnn` with this API, a DFA can be extracted using `extract(rnn)`. `extract` also has the optional parameters `time_limit` (default: 50 seconds) and `initial_split_depth` (default: 10)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Code starts here!"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 1. Imports"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Implementations of LSTM and GRU classifiers, the Tomita grammars, and our main extraction method."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "from LSTM import LSTMNetwork\n",
    "from GRU import GRUNetwork\n",
    "from RNNClassifier import RNNClassifier\n",
    "from Training_Functions import make_train_set_for_target,mixed_curriculum_train\n",
    "from Tomita_Grammars import tomita_1, tomita_2, tomita_3, tomita_4, tomita_5, tomita_6, tomita_7\n",
    "from Extraction import extract"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 2. Training"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 2.1. Define a Language\n",
    "Define a target language for your network. \n",
    "\n",
    "A language is defined as a function that takes a word over a fixed alphabet and either accepts or rejects it.\n",
    "\n",
    "You can pick any one of the Tomita grammars we have imported, they are defined over the alphabet $\\{0,1\\}$.\n",
    "\n",
    "You can also define your own target language. For instance, the language of all words starting and ending with the same character, over the alphabet $\\{a,b,c\\}$:\n",
    "\n",
    "```\n",
    "def target(w):             \n",
    "   if len(w)==0:          \n",
    "       return True         \n",
    "   return w[0]==w[-1] \n",
    "\n",
    "alphabet = \"abc\"    \n",
    "```"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "target = tomita_3\n",
    "alphabet = \"01\""
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The tomita_3 language is the complement of `((0|1)*0)*1(11)*(0(0|1)*1)*0(00)*(1(0|1)*)*` (i.e., the language of all words where there is no odd number of consecutive zeros after an odd number of consecutive ones),\n",
    "as verified below."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "False\n"
     ]
    }
   ],
   "source": [
    "print(target(\"00011000\"))\n",
    "print(target(\"10011000\"))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 2.2. Create a Train Set\n",
    "`make_train_set_for_target` returns for the target function a dictionary of words of different lengths, each mapped to its classification by the target. It tries to return a train set with an even split between positive and negative samples for each sample length. Its optional parameters are:\n",
    ">1. `max_train_samples_per_length` (default 300): the maximum number of words of each length in the train set\n",
    ">2. `search_size_per_length` (default 1000): the maximum number of words to be sampled from each length while generating the train set\n",
    ">3. `provided_examples` (default `None`): hand-crafted samples to add to the train set (helpful if random sampling is unlikely to find one of the classes)\n",
    ">4. `lengths` (a list of integers, default $0-15,20,25,30$): the lengths that will appear in the train set\n",
    "\n",
    "If the target is such that the positive or negative class is relatively rare, `make_train_set_for_target` is unlikely to create an evenly split test set without some help. In this case it is best to help it with some provided examples, e.g.: for the language of all words containing the sequence `0123` over the alphabet $\\{0,1,2,3\\}$, you may want to run:\n",
    "```\n",
    "short_strings = [\"\",\"0\",\"1\",\"2\",\"3\"]\n",
    "positive_examples = [a+\"0123\"+b for a,b in itertools.product(short_strings,short_strings)]\n",
    "make_train_set_for_target(target,alphabet,provided_examples=positive_examples)\n",
    "```\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "made train set of size: 2717 , of which positive examples: 1306\n"
     ]
    }
   ],
   "source": [
    "train_set = make_train_set_for_target(target,alphabet)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "2717\n",
      "[('', True), ('1', True), ('0', True), ('11', True), ('01', True), ('00', True), ('10', False), ('111', True), ('000', True), ('011', True)]\n"
     ]
    }
   ],
   "source": [
    "print(len(train_set))\n",
    "print(list(train_set.items())[:10])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "#### 2.3. Create and Train a Network"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "\n",
    "`RNNClassifier` generates an RNN-Classifier for a given alphabet.\n",
    "Its optional parameters are:\n",
    ">1. `num_layers` (default value 2): the number of hidden layers\n",
    ">2. `hidden_dim` (default value 5): the size of the hidden layers\n",
    ">3. `input_dim` (default value 3): the size of the input vectors (these networks use embedding, not one-hot encoding)\n",
    ">4. `RNNClass` (default value `LSTMNetwork`): the RNN architecture (possible values `LSTMNetwork`, `GRUNetwork`)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [],
   "source": [
    "rnn = RNNClassifier(alphabet,num_layers=1,hidden_dim=10,RNNClass = LSTMNetwork)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The function `mixed_curriculum_train(rnn,train_set)` trains the network `rnn` with the given dictionary of labeled examples, `train_set`. Its optional parameters are: \n",
    ">1. `stop_threshold` (default $0.001$): the threshold for the average loss of the network on the train set under which training is cut short\n",
    ">2. `learning_rate` (defualt 0.001): learning rate for optimiser\n",
    ">2. `length_epochs` (default $5$): explained below\n",
    ">3. `random_batch_epochs` (default $100$): below\n",
    ">4. `random_batch_size` (default $20$): below\n",
    ">5. `single_batch_epochs` (default $100$): below\n",
    ">6. `outer_loops` (default $3$): below\n",
    "\n",
    "`mixed_curriculum_train` splits the input dictionary first into batches by length, training for `length_epochs` iterations each of these batches, by order of increasing length. Then for `random_batch_epochs` iterations it will, at each iteration, split the dictionary into random batches of size `random_batch_size` and train each batch for one iteration. After that it will train the dictionary as one big batch for `single_batch_epochs` iterations. It does all of this `outer_loops` times.\n",
    "\n",
    "This will print some scatter plots of the average loss on the train set. The plots will come in pairs: each time one for the most recent iterations of training where the whole dictionary was trained as one batch, and another for all the iterations the rnn has been trained since its initialisation.\n",
    "\n",
    "`mixed_curriculum_train` should work for most simple targets without any tinkering. If the network doesn't drop under the stop threshold, you may want to call it again."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {
    "scrolled": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "current average loss is:  0.0055616439525183\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAXcAAAD8CAYAAACMwORRAAAABHNCSVQICAgIfAhkiAAAAAlwSFlz\nAAALEgAACxIB0t1+/AAAADl0RVh0U29mdHdhcmUAbWF0cGxvdGxpYiB2ZXJzaW9uIDIuMS4wLCBo\ndHRwOi8vbWF0cGxvdGxpYi5vcmcvpW3flQAAIABJREFUeJzt3Xt4VPW97/H31xhqVCpWqHJV9CA2\nkAASoMiRgFBAqYBIW/DyCE8ttaL2ckwFr2yslQ3u7a6VlmoP3isoR5GzpQd3i4i30xIUy+2gEVGS\nqERqqEJQEr7njxnSIUwyK8kkM7PyeT1PHmat+c2abxaTz1rzW+u3lrk7IiISLsekugAREUk+hbuI\nSAgp3EVEQkjhLiISQgp3EZEQUriLiISQwl1EJIQU7iIiIaRwFxEJoWNT9cYdO3b0M844I1VvLyKS\nkTZs2PCJu3dK1C5l4X7GGWdQXFycqrcXEclIZvZ+kHbqlhERCSGFu4hICCncRURCKGV97hJuBw8e\npLS0lAMHDqS6FJGMdNxxx9GtWzeys7Ob9PpA4W5m44BfAVnA7919fp3n7wVGRiePB77u7h2aVJGE\nQmlpKe3bt+eMM87AzFJdjkhGcXf27NlDaWkpPXv2bNIyEoa7mWUBi4BvAaXAejNb6e5bYwr5aUz7\n64EBTapGQuPAgQMKdpEmMjNOOeUUKioqmryMIH3ug4ESd9/h7l8CS4GJDbSfBjzZ5IokNBTsIk3X\n3L+fIOHeFdgVM10anRevmNOBnsCaZlUlIiLNEiTc420+6rvx6lRgubvXxF2Q2UwzKzaz4uZ83RBp\nqrlz53LPPfckbXnnnXde7eOioiL69OlDUVERixcv5tFHH2308iorK/nNb35TO11eXs6UKVOSUuuI\nESNabODgtGnTyM/P5957723S69euXctrr71WOz19+nSWL1+erPJSqiXXe0OCHFAtBbrHTHcDyutp\nOxWYVd+C3P0B4AGAgoKCRt+Ze8WbZSxcvZ3yyiq6dMihaGxvJg2I+yVCpFXEBtLvfvc7Kioq+MpX\nvtLk5R0O92uvvRaALl26pH3IffTRR7z22mu8/36ggZMAVFdXc+yx/4yftWvXcuKJJx6xsZTmCbLn\nvh7oZWY9zawdkQBfWbeRmfUGTgZeT26JESveLGPOM5soq6zCgbLKKuY8s4kVb5a1xNtJK1vxZhnD\n5q+h5+znGTZ/TVL+Xx999FHy8/Pp168fV1555VHPP/jggwwaNIh+/fpx6aWXsn//fgCefvpp+vbt\nS79+/Rg+fDgAW7ZsYfDgwfTv35/8/HzeeecdAE488UQAJkyYwL59+xgyZAjLli074htCSUkJo0eP\npl+/fpx77rm8++67fP7554waNYpzzz2XvLw8nnvuOQBmz57Nu+++S//+/SkqKmLnzp307dsXiByk\nnjFjBnl5eQwYMIAXX3wRgIcffpjJkyczbtw4evXqxc9//vOE6+bJJ58kLy+Pvn37ctNNNwFQU1PD\n9OnT6du3L3l5ebV74ffddx+5ubnk5+czderUo5Y1ZswYdu/eTf/+/Xn55ZfZuHEj3/zmN8nPz+eS\nSy7h008/BSJ7sDfffDOFhYX86le/qn39zp07Wbx4Mffee2/tMgDWrVvHeeedx5lnnnnEBm7hwoUM\nGjSI/Px87rjjDgD27dvH+PHj6devH3379mXZsmUAbNiwgcLCQgYOHMjYsWP58MMPj6q/oqKCSy+9\nlEGDBjFo0CBeffVVIPIt78orr+SCCy6gV69ePPjgg0DkTJaioqLa9XT4vQAWLFhAXl4e/fr1Y/bs\n2bXzn376aQYPHszZZ59d+/vV95lKGndP+ANcBLwNvAvcEp03D5gQ02YuMD/I8tydgQMHemOcd/ef\n/fSb/vOon/Pu/nOjliOtY+vWrYHbPvtGqZ9z6x+P+H8959Y/+rNvlDb5/Tdv3uxnn322V1RUuLv7\nnj173N39jjvu8IULF7q7+yeffFLb/pZbbvH77rvP3d379u3rpaWR9/7000/d3f26667zxx9/3N3d\nv/jiC9+/f7+7u59wwgm1y4h9HPs+gwcP9meeecbd3auqqnzfvn1+8OBB37t3r7u7V1RU+FlnneWH\nDh3y9957z/v06VO7nNjpe+65x6dPn+7u7tu2bfPu3bt7VVWVP/TQQ96zZ0+vrKz0qqoq79Gjh3/w\nwQdHrZPCwkJfv369l5WVeffu3X337t1+8OBBHzlypD/77LNeXFzso0ePrm1/+Hfv3LmzHzhw4Ih5\nserWnJeX52vXrnV399tuu81//OMf177/j370o6NeX3d9ubtfddVVPmXKFK+pqfEtW7b4WWed5e7u\nq1ev9h/84Ad+6NAhr6mp8fHjx/tLL73ky5cv96uvvrr29ZWVlf7ll1/60KFDfffu3e7uvnTpUp8x\nY8ZR7z1t2jR/+eWX3d39/fff93POOae2pvz8fN+/f79XVFR4t27dvKyszJcvX+6jR4/26upq/+ij\nj7x79+5eXl7uq1at8qFDh/q+ffvc/Z+fucLCQv/Zz37m7u7PP/+8jxo1yt3r/0zFivd3BBR7gIwN\ndJ67u68CVtWZd3ud6bnN2sokUF5ZFWi+um4yz8LV26k6eORhmqqDNSxcvb3J/3dr1qxhypQpdOzY\nEYCvfe1rR7XZvHkzt956K5WVlXz++eeMHTsWgGHDhjF9+nS++93vMnnyZACGDh3KXXfdRWlpKZMn\nT6ZXr16B6vjss88oKyvjkksuASIDUyAyyOvmm29m3bp1HHPMMZSVlfHxxx83uKxXXnmF66+/HoBz\nzjmH008/nbfffhuAUaNGcdJJJwGQm5vL+++/T/fu3eMuZ/369YwYMYJOnSIXFrz88stZt24dt912\nGzt27OD6669n/PjxjBkzBoD8/Hwuv/xyJk2axKRJkxqsce/evVRWVlJYWAjAVVddxXe+853a57/3\nve81+PpYkyZN4phjjiE3N7d23bzwwgu88MILDBgQOdv6888/55133uH888/nxhtv5KabbuLb3/42\n559/Pps3b2bz5s1861vfAiLfTDp37nzU+/zpT39i69baM7v5xz/+wWeffQbAxIkTycnJIScnh5Ej\nR/LXv/6VV155hWnTppGVlcWpp55KYWEh69ev56WXXmLGjBkcf/zxwJGfucOfo4EDB7Jz506g6Z+p\noDLm8gNdOuQknK+um8wUdMPdGO6e8FSy6dOnc//997Np0ybuuOOO2tG0ixcv5he/+AW7du2if//+\n7Nmzh8suu4yVK1eSk5PD2LFjWbMm2AlhkR2toz3xxBNUVFSwYcMGNm7cyKmnnppwNG99ywKO6OfP\nysqiurq60cs5+eSTeeuttxgxYgSLFi3i6quvBuD5559n1qxZbNiwgYEDBza47EROOOGEwG1jf6fD\nNbs7c+bMYePGjWzcuJGSkhK+//3vc/bZZ7Nhwwby8vKYM2cO8+bNw93p06dPbdtNmzbxwgsvHPU+\nhw4d4vXXX69tV1ZWRvv27YGjT0c0s3rXX0OfucO/S+z/TVM/U0FlTLgXje1NTnbWEfNysrMoGtu7\ndrqhPUBJX0E23I01atQonnrqKfbs2QPA3//+96PafPbZZ3Tu3JmDBw/yxBNP1M5/9913GTJkCPPm\nzaNjx47s2rWLHTt2cOaZZ3LDDTcwYcIE/va3vwWq46tf/SrdunVjxYoVAHzxxRfs37+fvXv38vWv\nf53s7GxefPHF2oOR7du3r91rrGv48OG1db799tt88MEH9O7dO27bhgwZMoSXXnqJTz75hJqaGp58\n8kkKCwv55JNPOHToEJdeeil33nknb7zxBocOHWLXrl2MHDmSBQsW1H7Lqc9JJ53EySefXNuv/Nhj\nj9XuxTekod871tixY1myZEltDWVlZezevZvy8nKOP/54rrjiCm688UbeeOMNevfuTUVFBa+/HjkM\nePDgQbZs2XLUMseMGcP9999fO71x48bax8899xwHDhxgz549rF27lkGDBjF8+HCWLVtGTU0NFRUV\nrFu3jsGDBzNmzBiWLFlSe+wm3mcuVlM/U0FlzLVlDn89b6jLpSX2AKXlFY3tzZxnNh2xYa674W6s\nPn36cMstt1BYWEhWVhYDBgzg4YcfPqLNnXfeyZAhQzj99NPJy8urDZeioiLeeecd3J1Ro0bRr18/\n5s+fz+OPP052djannXYat99+e5x3je+xxx7jhz/8IbfffjvZ2dk8/fTTXH755Vx88cUUFBTQv39/\nzjnnHABOOeUUhg0bRt++fbnwwguZNeufJ59de+21XHPNNeTl5XHsscfy8MMPN+nMnM6dO3P33Xcz\ncuRI3J2LLrqIiRMn8tZbbzFjxgwOHToEwN13301NTQ1XXHEFe/fuxd356U9/SocODV9Z5JFHHuGa\na65h//79nHnmmTz00EMJa7r44ouZMmUKzz33HL/+9a/rbTdmzBi2bdvG0KFDgcgB7ccff5ySkhKK\nioo45phjyM7O5re//S3t2rVj+fLl3HDDDezdu5fq6mp+8pOf0KdPnyOWed999zFr1izy8/Oprq5m\n+PDhLF68GIDBgwczfvx4PvjgA2677Ta6dOnCJZdcwuuvv06/fv0wMxYsWMBpp53GuHHj2LhxIwUF\nBbRr146LLrqIX/7yl/X+LsuWLWvyZyoIa+irXksqKCjwZJ/7OWz+GsriBHnXDjm8OvuCpL6XNGzb\ntm184xvfCNxex0ok3cydO5cTTzyRG2+8MWU1xPs7MrMN7l6Q6LUZs+ceREvsAUrrmDSgq8JcJIlC\nFe5Bum60hygiQcydOzfVJTRLqMIdGt4DPHw2zeE9+8Nn0xx+nSRXkDNWRCS+5naZZ8zZMsmgs2la\nz3HHHceePXua/QEVaYs8ej33w+MimiJ0e+4N0dk0radbt26UlpY263rUIm3Z4TsxNVWbCvcuHXLi\nnk3TnPOpJb7s7Owm30FGRJqvTXXLBBkIJSISBm1qzz3I2TQiImHQpsIddD61iLQNbapbRkSkrVC4\ni4iEUJvrlglCo1hFJNMp3OvQKFYRCQN1y9ShUawiEgYK9zo0ilVEwiBQuJvZODPbbmYlZja7njbf\nNbOtZrbFzP6Q3DJbT0vcFUhEpLUlDHczywIWARcCucA0M8ut06YXMAcY5u59gJ+0QK2tQqNYRSQM\nghxQHQyUuPsOADNbCkwEtsa0+QGwyN0/BXD33ckutLVoFKuIhEGQcO8K7IqZLgWG1GlzNoCZvQpk\nAXPd/f8kpcIU0ChWEcl0QcI93t0W6l6k+1igFzAC6Aa8bGZ93b3yiAWZzQRmAvTo0aPRxYqISDBB\nDqiWAt1jprsB5XHaPOfuB939PWA7kbA/grs/4O4F7l7QqVOnptYsIiIJBNlzXw/0MrOeQBkwFbis\nTpsVwDTgYTPrSKSbZkcyC00nGsEqIukuYbi7e7WZXQesJtKfvsTdt5jZPKDY3VdGnxtjZluBGqDI\n3fe0ZOGpohGsIpIJLFX3uCwoKPDi4uKUvHdzDJu/Ju7dnLp2yOHV2RekoCIRaUvMbIO7FyRqpxGq\njaQRrCKSCRTujaQRrCKSCRTujaQRrCKSCXTJ30bSCFYRyQQK9ybQCFYRSXfqlhERCSHtubcQDXQS\nkVRSuLcADXQSkVRTt0wL0K36RCTVFO4tQAOdRCTVFO4tQAOdRCTVFO4tQAOdRCTVdEC1BWigk4ik\nmsK9hWigk4ikkrplRERCSHvuKaJBTiLSkhTuKaBBTiLS0tQtkwIa5CQiLU3hngIa5CQiLS1QuJvZ\nODPbbmYlZjY7zvPTzazCzDZGf65OfqnhoUFOItLSEoa7mWUBi4ALgVxgmpnlxmm6zN37R39+n+Q6\nQ0WDnESkpQU5oDoYKHH3HQBmthSYCGxtycLCTIOcRKSlBQn3rsCumOlSYEicdpea2XDgbeCn7r6r\nbgMzmwnMBOjRo0fjqw0RDXISkZYUpM/d4szzOtP/GzjD3fOBPwGPxFuQuz/g7gXuXtCpU6fGVSoi\nIoEFCfdSoHvMdDegPLaBu+9x9y+ikw8CA5NTnoiINEWQcF8P9DKznmbWDpgKrIxtYGadYyYnANuS\nV6KIiDRWwj53d682s+uA1UAWsMTdt5jZPKDY3VcCN5jZBKAa+DswvQVrFhGRBMy9bvd56ygoKPDi\n4uKUvLeISKYysw3uXpConUaoioiEkMJdRCSEdFXINKbLAotIUync05QuCywizaFumTSlywKLSHMo\n3NOULgssIs2hcE9TuiywiDSHwj1N6bLAItIcOqCapnRZYBFpDoV7GtNlgUWkqdQtIyISQgp3EZEQ\nUriLiISQwl1EJIQU7iIiIaRwFxEJIYW7iEgIKdxFREIoULib2Tgz225mJWY2u4F2U8zMzSzhLaBE\nRKTlJAx3M8sCFgEXArnANDPLjdOuPXAD8JdkFykiIo0TZM99MFDi7jvc/UtgKTAxTrs7gQXAgSTW\nJyIiTRAk3LsCu2KmS6PzapnZAKC7u/9nEmsTEZEmChLuFmee1z5pdgxwL/A/Ei7IbKaZFZtZcUVF\nRfAqRUSkUYJcFbIU6B4z3Q0oj5luD/QF1poZwGnASjOb4O7FsQty9weABwAKCgocaRbdQFtE6hMk\n3NcDvcysJ1AGTAUuO/yku+8FOh6eNrO1wI11g12SSzfQFpGGJOyWcfdq4DpgNbANeMrdt5jZPDOb\n0NIFSny6gbaINCTQzTrcfRWwqs682+tpO6L5ZUkiuoG2iDREI1QzlG6gLSINUbhnKN1AW0Qaonuo\nZijdQFtEGqJwz2C6gbaI1EfdMiIiIaRwFxEJIYW7iEgIKdxFREJI4S4iEkIKdxGREFK4i4iEkMJd\nRCSEFO4iIiGkcBcRCSGFu4hICCncRURCSOEuIhJCCncRkRBSuIuIhFCgcDezcWa23cxKzGx2nOev\nMbNNZrbRzF4xs9zklyoiIkElDHczywIWARcCucC0OOH9B3fPc/f+wALg35NeqYiIBBZkz30wUOLu\nO9z9S2ApMDG2gbv/I2byBMCTV6KIiDRWkNvsdQV2xUyXAkPqNjKzWcDPgHbABUmpTkREmiTInrvF\nmXfUnrm7L3L3s4CbgFvjLshsppkVm1lxRUVF4yoVEZHAgoR7KdA9ZrobUN5A+6XApHhPuPsD7l7g\n7gWdOnUKXqWIiDRKkG6Z9UAvM+sJlAFTgctiG5hZL3d/Jzo5HngHSbkVb5axcPV2yiur6NIhh6Kx\nvZk0oGuqyxKRVpAw3N292syuA1YDWcASd99iZvOAYndfCVxnZqOBg8CnwFUtWbQktuLNMuY8s4mq\ngzUAlFVWMeeZTQAKeJE2wNxTc2JLQUGBFxcXp+S924Jh89dQVll11PyuHXJ4dbaOd4tkKjPb4O4F\nidpphGpIlccJ9obmi0i4KNxDqkuHnEbNF5FwUbiHVNHY3uRkZx0xLyc7i6KxvVNUkYi0piBny0gG\nOnzQVGfLiLRNCvcQmzSgq8JcpI1St4yISAgp3EVEQkjhLiISQgp3EZEQUriLiISQwl1EJIQU7iIi\nIaRwFxEJIYW7iEgIKdxFREJI4S4iEkIKdxGREFK4i4iEkMJdRCSEAoW7mY0zs+1mVmJms+M8/zMz\n22pmfzOzP5vZ6ckvVUREgkoY7maWBSwCLgRygWlmllun2ZtAgbvnA8uBBckuVEREgguy5z4YKHH3\nHe7+JbAUmBjbwN1fdPf90cn/C3RLbpkiItIYQcK9K7ArZro0Oq8+3wf+2JyiRESkeYLcZs/izPO4\nDc2uAAqAwnqenwnMBOjRo0fAEkVEpLGC7LmXAt1jprsB5XUbmdlo4BZggrt/EW9B7v6Auxe4e0Gn\nTp2aUq+IiAQQJNzXA73MrKeZtQOmAitjG5jZAOB3RIJ9d/LLFBGRxkjYLePu1WZ2HbAayAKWuPsW\nM5sHFLv7SmAhcCLwtJkBfODuE1qwbkmSFW+WsXD1dsorq+jSIYeisb2ZNKChQyoikgmC9Lnj7quA\nVXXm3R7zeHSS65JWsOLNMuY8s4mqgzUAlFVWMeeZTQAKeJEMpxGqbdjC1dtrg/2wqoM1LFy9PUUV\niUiyKNzbsPLKqkbNF5HMoXBvw7p0yGnUfBHJHAr3NqxobG9ysrOOmJeTnUXR2N4pqkhEkiXQAVUJ\np8MHTXW2jEj4KNzbuEkDuirMRUJI3TIiIiGkcBcRCSGFu4hICCncRURCSOEuIhJCCncRkRBSuIuI\nhJDCXUQkhBTuIiIhpBGq0iDdzEMkMyncpV66mYdI5lK3jNRLN/MQyVwKd6mXbuYhkrkChbuZjTOz\n7WZWYmaz4zw/3MzeMLNqM5uS/DIlFXQzD5HMlTDczSwLWARcCOQC08wst06zD4DpwB+SXaCkjm7m\nIZK5ghxQHQyUuPsOADNbCkwEth5u4O47o88daoEaJUV0Mw+RzBUk3LsCu2KmS4EhTXkzM5sJzATo\n0aNHUxYhrUw38xDJTEH63C3OPG/Km7n7A+5e4O4FnTp1asoiREQkgCDhXgp0j5nuBpS3TDkiIpIM\nQcJ9PdDLzHqaWTtgKrCyZcsSEZHmSNjn7u7VZnYdsBrIApa4+xYzmwcUu/tKMxsEPAucDFxsZv/i\n7n1atHJJG7pEgUj6CXT5AXdfBayqM+/2mMfriXTXSBujSxSIpCeNUJVm0SUKRNKTwl2aRZcoEElP\nCndpFl2iQCQ9KdylWXSJApH0pOu5S7PoEgUi6UnhLs2mSxSIpB91y4iIhJD23KXFaZCTSOtTuEuL\n0iAnkdRQt4y0KA1yEkkNhbu0KA1yEkkNdctIi+rSIYeyOEFed5CT+uVFkkt77tKiggxyOtwvX1ZZ\nhfPPfvkVb5a1crUi4aFwlxY1aUBX7p6cR9cOORjQtUMOd0/OO2KvXP3yIsmnbhlpcYkGOQXpl1e3\njUjjaM9dUi7RxcfUbSPSeAp3SblE/fJBu21WvFnGsPlr6Dn7eYbNX6PwlzZN3TKScokuPha02ybR\nYKlEXTvq+pEwUbhLWmioXz7I6ZQN7d1PGtA1YfgHHUmbjA1EumxktDELt0DhbmbjgF8RuUH27919\nfp3nvwI8CgwE9gDfc/edyS1V2qqisb2PCF44+nTKRHv3icI/0fOQ+NtB0G8P6bCRScY3nWTV0Rob\nw0xZRjIl7HM3syxgEXAhkAtMM7PcOs2+D3zq7v8NuBf412QXKm1XkNMpEx2UTRT+Qbp+EvX9Bzk2\nkIxlJDrAHOQAdKL3CbKM5tbRGu+RSctItiAHVAcDJe6+w92/BJYCE+u0mQg8En28HBhlZpa8MqWt\nmzSgK6/OvoD35o/n1dkXHLW3k+igbKLwD3K7wGRsINJlI9OcbzrJqqO1NoaZsoxkCxLuXYFdMdOl\n0Xlx27h7NbAXOKXugsxsppkVm1lxRUVF0yoWiSPR3n2i8A8ykjYZG4h02cg095tOMuporY1hpiwj\n2YKEe7w9cG9CG9z9AXcvcPeCTp06BalPJLCG9u4ThX+Qrp9kbCDSZSPT3G86yaijtTaGmbKMZAsS\n7qVA95jpbkB5fW3M7FjgJODvyShQJFkSde0Eeb65G4h02cg095tOMuporY1hpiwj2cz9qB3sIxtE\nwvptYBRQBqwHLnP3LTFtZgF57n6NmU0FJrv7dxtabkFBgRcXFze3fpE2qTVOp9TZMul5toyZbXD3\ngoTtEoV7dGEXAf9B5FTIJe5+l5nNA4rdfaWZHQc8Bgwgssc+1d13NLRMhbuISOMFDfdA57m7+ypg\nVZ15t8c8PgB8p7FFiohIy9C1ZUREQkjhLiISQgp3EZEQUriLiISQwl1EJIQU7iIiIaRwFxEJIYW7\niEgIBRqh2iJvbFYBvN/El3cEPkliOS0pU2pVncmVKXVC5tSqOiNOd/eEV15MWbg3h5kVBxl+mw4y\npVbVmVyZUidkTq2qs3HULSMiEkIKdxGREMrUcH8g1QU0QqbUqjqTK1PqhMypVXU2Qkb2uYuISMMy\ndc9dREQakHHhbmbjzGy7mZWY2exU11MfM9tpZpvMbKOZpdVdScxsiZntNrPNMfO+Zmb/ZWbvRP89\nOZU1RmuKV+dcMyuLrteN0RvJpJSZdTezF81sm5ltMbMfR+en1TptoM60WqdmdpyZ/dXM3orW+S/R\n+T3N7C/R9bnMzNqlss4EtT5sZu/FrNP+rV6cu2fMD5E7Qb0LnAm0A94CclNdVz217gQ6prqOemob\nDpwLbI6ZtwCYHX08G/jXNK1zLnBjqmurU2dn4Nzo4/ZEbkuZm27rtIE602qdAgacGH2cDfwF+Cbw\nFJG7vAEsBn6UxrU+DExJZW2Ztuc+GChx9x3u/iWwFJiY4poyjruv4+gbmE8EHok+fgSY1KpFxVFP\nnWnH3T909zeijz8DtgFdSbN12kCdacUjPo9OZkd/HLgAWB6dn/L1CQ3WmnKZFu5dgV0x06Wk4Ycz\nyoEXzGyDmc1MdTEBnOruH0IkBICvp7iehlxnZn+LdtukvPsolpmdQeRewn8hjddpnTohzdapmWWZ\n2UZgN/BfRL6xV7p7dbRJ2vzt163V3Q+v07ui6/ReM/tKa9eVaeFucealxVYyjmHufi5wITDLzIan\nuqCQ+C1wFtAf+BD4t9SW809mdiLwv4CfuPs/Ul1PfeLUmXbr1N1r3L0/0I3IN/ZvxGvWulXFV7dW\nM+sLzAHOAQYBXwNuau26Mi3cS4HuMdPdgPIU1dIgdy+P/rsbeJbIBzSdfWxmnQGi/+5OcT1xufvH\n0T+mQ8CDpMl6NbNsIoH5hLs/E52ddus0Xp3puk4B3L0SWEukH7uDmR0bfSrt/vZjah0X7QJzd/8C\neIgUrNNMC/f1QK/oUfN2wFRgZYprOoqZnWBm7Q8/BsYAmxt+VcqtBK6KPr4KeC6FtdTrcFhGXUIa\nrFczM+B/Atvc/d9jnkqrdVpfnem2Ts2sk5l1iD7OAUYTOT7wIjAl2izl6xPqrfX/xWzUjcixgVZf\npxk3iCl6mtZ/EDlzZom735Xiko5iZmcS2VsHOBb4QzrVaWZPAiOIXL3uY+AOYAWRsxF6AB8A33H3\nlB7MrKfOEUS6D5zIGUk/PNyvnSpm9t+Bl4FNwKHo7JuJ9GenzTptoM5ppNE6NbN8IgdMs4jsgD7l\n7vOif1dLiXRzvAlcEd0zTplHKFW8AAAAS0lEQVQGal0DdCLSlbwRuCbmwGvr1JZp4S4iIollWreM\niIgEoHAXEQkhhbuISAgp3EVEQkjhLiISQgp3EZEQUriLiISQwl1EJIT+PzipLCSR3UzzAAAAAElF\nTkSuQmCC\n",
      "text/plain": [
       "<matplotlib.figure.Figure at 0x10a5439b0>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAXcAAAD8CAYAAACMwORRAAAABHNCSVQICAgIfAhkiAAAAAlwSFlz\nAAALEgAACxIB0t1+/AAAADl0RVh0U29mdHdhcmUAbWF0cGxvdGxpYiB2ZXJzaW9uIDIuMS4wLCBo\ndHRwOi8vbWF0cGxvdGxpYi5vcmcvpW3flQAAH8RJREFUeJzt3X10VPW97/H3lxAlqBgrtAsTEOyl\nUswjRrByq1hQ7MMFqtwDlj7QWy9dq9UebZsW61kHL3YJLZ6rtbU+9bQWZSm2Vymr2uJZhT6uY0uQ\nqDwUi4CS0NZACQdNwCF87x8zE4dkkux5ysxsPq+1WGT27Oz57ezkM3t++7e/P3N3REQkXIbkuwEi\nIpJ9CncRkRBSuIuIhJDCXUQkhBTuIiIhpHAXEQkhhbuISAgp3EVEQkjhLiISQkPz9cIjR470cePG\n5evlRUSK0ubNmw+4+6iB1stbuI8bN46mpqZ8vbyISFEys9eCrKduGRGREFK4i4iEkMJdRCSE8tbn\nLgIQiURoaWnh6NGj+W6KSEEZNmwYlZWVlJaWpvX9CnfJq5aWFs466yzGjRuHmeW7OSIFwd05ePAg\nLS0tjB8/Pq1tqFtG8uro0aOce+65CnaRBGbGueeem9EnWoW75J2CXaS3TP8uFO4iIiFUVOG+dksr\n01ZsYPySZ5i2YgNrt7Tmu0kSUrfffjt33XVX1rZ32WWXdX/d2NjIRRddRGNjIw888ACrVq1KeXvt\n7e18//vf7368f/9+5s2bl5W2Tp8+fVBvMEz82eRr+zfccAPbt28H4M4770zp+3N5LDJh+Zogu6Gh\nwVP5BVq7pZVbn3qZzkhX9zIDHKgoL6Nx1oXMra/IfkMlp3bs2MH73//+fDejl9tvv50zzzyTr371\nq1nf9ogRI2hra+P0009Pext79+7lYx/7GFu3bs1iy6KmT5/OXXfdRUNDQ9a3XQzOPPNM3nzzzcDr\n5/JYJPv7MLPN7j7gwSmaM/eV63eeFOwQDXaA1vZObl7TTP2y53Q2H3K5+PS2atUqampqqK2t5VOf\n+lSv5x9++GEuueQSamtrue666+jo6ADgJz/5CVVVVdTW1nL55ZcDsG3bNqZMmUJdXR01NTX85S9/\nAaKBATB79mzeeustpk6dypo1a076hLBr1y5mzpxJbW0tkydP5tVXX+XNN99kxowZTJ48merqan72\ns58BsGTJEl599VXq6upobGxk7969VFVVAdGL1J/97Geprq6mvr6ejRs3AvDII49w7bXXcs011zBh\nwgS+9rWvDfizefzxx6murqaqqoqvf/3rAHR1dbFo0SKqqqqorq7m7rvvBuDee+9l0qRJ1NTUsGDB\ngl7bGuhn8+tf/5rp06czb948Jk6cyMKFC4mffG7atInLLruM2tpapkyZwpEjR+jq6qKxsZFLLrmE\nmpoaHnzwwaT7EGT78U8rS5YsobOzk7q6OhYuXHjS9+f7WKTM3fPy7+KLL/ZUjPv6z/38AP8m/ssv\n/OkXWlLatuTP9u3bA6/79AstPvFffpHV471161Z/3/ve521tbe7ufvDgQXd3X7p0qa9cudLd3Q8c\nONC9/m233eb33nuvu7tXVVV5S0v0tQ8dOuTu7jfeeKM/9thj7u5+7Ngx7+jocHf3M844o3sbiV8n\nvs6UKVP8qaeecnf3zs5Of+uttzwSifjhw4fd3b2trc3f+973+okTJ3zPnj1+0UUXdW8n8fFdd93l\nixYtcnf3HTt2+JgxY7yzs9N/9KMf+fjx4729vd07Ozt97Nix/vrrr/f6mVxxxRW+adMmb21t9TFj\nxvgbb7zhkUjEr7zySn/66ae9qanJZ86c2b1+fN9Hjx7tR48ePWlZooF+Nhs3bvQRI0b4vn37vKur\nyy+99FL/3e9+58eOHfPx48f7n/70J3d3P3z4sEciEX/wwQf9jjvucHf3o0eP+sUXX+y7d+/u9boD\nbT9xn3sen8TH+TgWyf4+gCYPkLFFc+Z+XnlZoPU6I13cvKZZffIhlOzTW2eki5Xrd6a9zQ0bNjBv\n3jxGjhwJwLve9a5e62zdupUPfvCDVFdXs3r1arZt2wbAtGnTWLRoEQ8//DBdXdF2feADH+DOO+/k\nW9/6Fq+99hplZcF+b48cOUJraysf//jHgegNLMOHD8fd+cY3vkFNTQ0zZ86ktbWVv//97/1u6/e/\n/333J5CJEydy/vnn88orrwAwY8YMzj77bIYNG8akSZN47bW+a1Bt2rSJ6dOnM2rUKIYOHcrChQv5\n7W9/ywUXXMDu3bu56aab+OUvf8mIESMAqKmpYeHChTz22GMMHdr7FpogP5spU6ZQWVnJkCFDqKur\nY+/evezcuZPRo0dzySWXANFuraFDh/Lcc8+xatUq6urqmDp1KgcPHuz+NNCXZNsPKp/HIh1FE+6N\nsy6krLQk8Prqqgmf/e2dKS0Pwt0HHHK2aNEivve97/Hyyy+zdOnS7rHHDzzwAN/85jfZt28fdXV1\nHDx4kE984hOsW7eOsrIyZs2axYYNGwK3I5nVq1fT1tbG5s2baW5u5j3vec+AY5/72hZwUj9/SUkJ\nx48fT3k755xzDi+++CLTp0/nvvvu44YbbgDgmWee4Ytf/CKbN2/m4osv7rXtID+bZO3r6xi5O9/9\n7ndpbm6mubmZPXv2cPXVV/e5P6nuf0/5PBbpKJpwn1tfwfJrq6mIncEHHQF6qCPCrU+9rIAPgb4+\nvQX9VJfMjBkzePLJJzl48CAA//jHP3qtc+TIEUaPHk0kEmH16tXdy1999VWmTp3KsmXLGDlyJPv2\n7WP37t1ccMEFfOlLX2L27Nm89NJLgdoxYsQIKisrWbt2LQDHjh2jo6ODw4cP8+53v5vS0lI2btzY\nfXZ31llnceTIkaTbuvzyy7vb+corr/D6669z4YUXBv+hxEydOpXf/OY3HDhwgK6uLh5//HGuuOIK\nDhw4wIkTJ7juuuu44447eOGFFzhx4gT79u3jyiuv5Nvf/jbt7e29Lkqm+7OZOHEi+/fvZ9OmTUD0\neBw/fpxZs2Zx//33E4lEuvf1rbfeSnk/eyotLe3eZqJ8Hot0DBjuZvZDM3vDzJJeCraoe81sl5m9\nZGaTs9/MqLn1FfxhyYfYu+Kj3D2/jvKyYDUXMv3oLoUh2ae3stISGmel/8dy0UUXcdttt3HFFVdQ\nW1vLl7/85V7r3HHHHUydOpWrrrqKiRMnvtOexsbui42XX345tbW1rFmzhqqqKurq6vjzn//Mpz/9\n6cBtefTRR7n33nupqanhsssu429/+xsLFy6kqamJhoYGVq9e3f365557LtOmTaOqqorGxsaTtvOF\nL3yBrq4uqqurmT9/Po888khaI3NGjx7N8uXLufLKK7sv8s6ZM4fW1lamT59OXV0dixYtYvny5XR1\ndfHJT36y+8LhLbfcQnl5+UnbS/dnc9ppp7FmzRpuuukmamtrueqqqzh69Cg33HADkyZNYvLkyVRV\nVfH5z38+K2e/ixcv7u5iSpTPY5GOAYdCmtnlwJvAKnevSvL8R4CbgI8AU4HvuPvUgV441aGQfVm7\npZWV63fSOsBHcwP2rPhoxq8n2ZXqUMj48d7f3sl5GgIrIZfJUMgBC4e5+2/NbFw/q8whGvwOPG9m\n5WY22t3/OtC2s2FufQVz6yuSjoNPlMlHdykc8eMtIv3LRp97BbAv4XFLbNmgivfJJ+uqyfSju4hI\nsclGuCe7tpm0r8fMFptZk5k1tbW1ZeGlTza3voLmpVdzz/w6KsrLMKJ3ry6/tlpnewVsoK5BkVNR\npn8X2ajn3gKMSXhcCexPtqK7PwQ8BNE+9yy8dlL66F48hg0bxsGDB1X2VySBx+q5Dxs2LO1tZCPc\n1wE3mtkTRC+oHh6s/nYpfpWVlbS0tJCLT3IixSw+E1O6Bgx3M3scmA6MNLMWYClQCuDuDwDPEh0p\nswvoAD6bdmvklFNaWpr2TDMi0rcgo2WuH+B5B76YtRZlmYbOicipqGjuUE1HfHhka3snjkoSiMip\nI9ThnqzQFKgkgYiEX6jDvb+CUqoeKSJhFupwD3JXqrpqRCSMQh3uqZQJPtQR4ZY1zYzT/KwiEgKh\nDvf+ShIkkzhtn/rkRaSYhTrcoXdJgqBUJlhEilnowz0uXgv+nvl1gbtqMpnhR0Qkn06ZcI9LpatG\nZYJFpFidcuEOybtqepasUplgESlm2SgcVrQSq0eqTIGIhMkpHe6JVCZYRMLklOyWEREJO4W7iEgI\nKdxFREJI4S4iEkIKdxGREFK4i4iEkMJdRCSEFO4iIiGkcBcRCSGFu4hICCncRURCSOEuIhJCCncR\nkRBSuIuIhJDCXUQkhBTuIiIhFGiyDjO7BvgOUAL8wN1X9Hh+LPBjoDy2zhJ3fzbLbR0UiTMynV1W\nihm0d0Q0O5OIFBVz9/5XMCsBXgGuAlqATcD17r49YZ2HgC3ufr+ZTQKedfdx/W23oaHBm5qaMmx+\ndq3d0sqtT71MZ6Srz3XOGV7K0v9xkUJeRPLCzDa7e8NA6wXplpkC7HL33e7+NvAEMKfHOg6MiH19\nNrA/lcYWipXrd/Yb7ACHOiLcsqaZcUueYdqKDazd0jpIrRMRCS5IuFcA+xIet8SWJbod+KSZtQDP\nAjdlpXWDbH97Z6D14p91Wts7FfQiUpCChLslWdazL+d64BF3rwQ+AjxqZr22bWaLzazJzJra2tpS\nb22OnVdelvL3JAb9rU+9rIAXkYIQJNxbgDEJjyvp3e3yOeBJAHf/T2AYMLLnhtz9IXdvcPeGUaNG\npdfiHGqcdSFlpSVpf39npIuV63dmsUUiIukJEu6bgAlmNt7MTgMWAOt6rPM6MAPAzN5PNNwL79R8\nAHPrK1h+bTUV5WUYUF5WyvDS1EaLBu3aERHJpQGHQrr7cTO7EVhPdJjjD919m5ktA5rcfR3wFeBh\nM7uFaE/FIh9oGE6Bmltf0WskTHx4ZGt7J0bvPqlE6XTtiIhk24BDIXOlEIdCBtFf0JeVlrD82moN\nkxSRnAk6FDLQTUzyjsQz+8QbnnSTk4gUEoV7BpJ14YiIFALVlhERCSGduWeB6tGISKHRBdUMBalH\nM7x0CKeXlijwRSRj2awtI/0IUo+mI3KCQx0RnOidrDevaaZ+2XO6m1VEckbhnqF0b1o61BFRuQIR\nyRmFe4YyuWlJ5QpEJFcU7hnKtB6NyhWISC5otEyG4hdGE0fLvH28i47IiUDfr3IFIpILCvcs6K8e\nTX+BX1ZaQuOsCwezqSJyitBQyEGk8fAikqmgQyEV7nnQ19j4+Hj4Qx0RSszocqd8EN8Ekr35JGtL\n4rKKFNvU1xtcf69XqG+Aqi0k+aBwL2DTVmygNc0LqalUnkysYDlQYAa5Gasv8eqY/b0JlKd4LaIv\n/b0BDvayZOWf8/0GnQ69SRUXhXsBG7/kmX5rwg/EgPLhpf2eQacS1sNLh3D0+AlOFGUF/uJTSKWh\nk/2eFFL7pDeFewHL5My9Pz3PoKVwJXuDzka3V6r6+13M9WtLelR+oIBlOja+L/E4V7AXPica4vDO\n8WrvjPRaluuJ1/u7z0KTvhc3hXsexOdqLS8rzXdTpAjk8k7mge6z0F3UxUvhnidz6ytoXno198yv\nO2lC7nOGRwO/xAxiy4bY4LfPIGlbei7LpGnDS4dwzvDSfvc91QnKwypXdzIH+RSpu6iLk25iyrMg\nszllMpIlLpVRK9kakZOtESPpDNEcjGXxPmlgwPb919FIRhesc3Unc+Id1n31vQ8xY+2WVvW9Fxld\nUC0SAwVcsmF50HdQ64aqwZXNoaa5utDZXxs1gqZwaLTMKSbZGbRGOxSWdD6B9PWmnavAX7ulla88\n+WLSi/IV5WX8YcmHMtq+ZE7hLlLkUh0yGw/8TIO+r/swDNiz4qNpbVOyR0MhRYpcqhcy44Gc6RDG\nvvr3VcG0uCjcRQpUviaCSTaCRhVMi4/CXaRA5WsimPh9GPEhuhXlZbqYWoQ0FFKkQPUcpjjQRdae\nMjnzTxyiG78QfMuaZo2mKiIKd5EC1t9EMP0Ffra6UXoOj4z358fbJoUrULib2TXAd4AS4AfuviLJ\nOv8E3E70d+xFd/9EFtspIjEDzfyVzbPrlet39hr3Hu/PV7gXtgHD3cxKgPuAq4AWYJOZrXP37Qnr\nTABuBaa5+yEze3euGiwivQW50zkdffXbqyRB4QtyQXUKsMvdd7v728ATwJwe6/xv4D53PwTg7m9k\nt5kikg8aFlm8goR7BbAv4XFLbFmi9wHvM7M/mNnzsW4cEcmDtVtambZiA+OXPMO0FRsyKtmrYZHF\nK0ife7LCfz0v1g8FJgDTgUrgd2ZW5e7tJ23IbDGwGGDs2LEpN1ZE+pftC6DJRuwkjqFXv3vhCnLm\n3gKMSXhcCexPss7P3D3i7nuAnUTD/iTu/pC7N7h7w6hRo9Jts4j0oa8LoF958sW0z+Dn1ld0n8EP\n1iQikrkg4b4JmGBm483sNGABsK7HOmuBKwHMbCTRbprd2WyoiAysrwudXe7csqaZcWl21fQ3akYK\n04Dh7u7HgRuB9cAO4El332Zmy8xsdmy19cBBM9sObAQa3f1grhotIsn1d6EzsfbMzWuaqV/2XOCQ\n16iZ4qOqkCIhkmrd+KCVJPuqUKkywINPVSFFTkHxujDxqQoHErSSpEbNFB+Fu0jIzK2v4N/+qTbl\nomP99aGrmFjxUW0ZkRDqOYQxaLGx/vrQVUysuCjcRUKqZxjfvm4b7Z2Rfr8nyJ2nKiZWHNQtI3IK\nmFtfQfPSq7lnfh0VsQDv2SsftA9dwyKLg87cRU4hybpWUq0kqWGRxUHhLnKKSreS5HnlZUmHRaqY\nWGFRt4yIpKSv6f863j6ucgQFROEuIimJD4ssLys9afmhjojqzRQQhbuIpGxufQVnnN67V1cXVguH\nwl1E0qILq4VN4S4iadEsTYVN4S4iaVG9mcKmoZAikpbEEgepjpWX3FO4i0ja0h0rL7mnbhkRkRBS\nuIuIhJC6ZUQkK9KtVSO5oXAXkYypDHDhUbeMiGRMZYALj8JdRDKmu1ULj8JdRDKmu1ULj8JdRDKm\nu1ULjy6oikjGdLdq4VG4i0hW6G7VwqJuGRGREFK4i4iEkMJdRCSEAoW7mV1jZjvNbJeZLelnvXlm\n5mbWkL0miohIqgYMdzMrAe4DPgxMAq43s0lJ1jsL+BLwx2w3UkREUhPkzH0KsMvdd7v728ATwJwk\n690BfBs4msX2iYhIGoKEewWwL+FxS2xZNzOrB8a4+8+z2DYREUlTkHHulmSZdz9pNgS4G1g04IbM\nFgOLAcaOHRushSJSVFT6tzAEOXNvAcYkPK4E9ic8PguoAn5tZnuBS4F1yS6quvtD7t7g7g2jRo1K\nv9UiUpDipX9b2ztx3in9u3ZLa76bdsoJEu6bgAlmNt7MTgMWAOviT7r7YXcf6e7j3H0c8Dww292b\nctJiESlYKv1bOAYMd3c/DtwIrAd2AE+6+zYzW2Zms3PdQBEpHir9WzgC1ZZx92eBZ3ss+9c+1p2e\nebNEpBidV15Ga5IgV+nfwac7VEUka1T6t3CoKqSIZI1K/xYOhbuIZJVK/xYGdcuIiISQwl1EJIQU\n7iIiIaRwFxEJIYW7iEgIKdxFREJI4S4iEkIKdxGREFK4i4iEkMJdRCSEFO4iIiGk2jIikjOaci9/\nFO4ikhPxKffiMzPFp9wDFPCDQN0yIpITmnIvvxTuIpITmnIvvxTuIpITfU2tpyn3BofCXURyQlPu\n5ZcuqIpITmjKvfxSuItIzmjKvfxRt4yISAgp3EVEQkjhLiISQgp3EZEQUriLiISQwl1EJIQChbuZ\nXWNmO81sl5ktSfL8l81su5m9ZGa/MrPzs99UEREJasBwN7MS4D7gw8Ak4Hozm9RjtS1Ag7vXAD8F\nvp3thoqISHBBztynALvcfbe7vw08AcxJXMHdN7p7R+zh80BldpspIiKpCBLuFcC+hMctsWV9+Rzw\ni0waJSIimQlSfsCSLPOkK5p9EmgArujj+cXAYoCxY8cGbKKIFDvNyDT4gpy5twBjEh5XAvt7rmRm\nM4HbgNnufizZhtz9IXdvcPeGUaNGpdNeESky8RmZWts7cd6ZkWntltZ8Ny3UgoT7JmCCmY03s9OA\nBcC6xBXMrB54kGiwv5H9ZopIsdKMTPkxYLi7+3HgRmA9sAN40t23mdkyM5sdW20lcCbwEzNrNrN1\nfWxORE4xmpEpPwKV/HX3Z4Fneyz714SvZ2a5XSISEueVl9GaJMg1I1Nu6Q5VEckpzciUH5qsQ0Ry\nSjMy5YfCXURyTjMyDT51y4iIhJDCXUQkhBTuIiIhpHAXEQkhXVAVkUGlOjODQ+EuIoMmXmcmXo4g\nXmcGUMBnmbplRGTQqM7M4FG4i8igUZ2ZwaNwF5FB01c9GdWZyT6Fu4gMGtWZGTy6oCoig0Z1ZgaP\nuSedMS/nGhoavKmpKS+vLSL5pyGR6TGzze7eMNB6OnMXkUGnIZG5pz53ERl0GhKZewp3ERl0GhKZ\newp3ERl0GhKZewp3ERl0GhKZewp3ERl0c+srWH5tNRXlZRhQXlbKsNIh3LKmmWkrNrB2S2u+m1j0\nFO4ikhdz6yv4w5IPcff8Oo4dP8GhjgjOOyNnFPCZUbiLSF5p5ExuKNxFJK/6GiHT2t6ps/cMKNxF\nJK/6GyGj7pn0KdxFJK+SjZyJ64x0cbMusqZF4S4ieRUfOdOf1vZObl7TTP2y5xTyAalwmIgUhGkr\nNtAa4A5VAxwoMaPLnfKyUsygvSNyShQgC1o4LFC4m9k1wHeAEuAH7r6ix/OnA6uAi4GDwHx339vf\nNhXuIpKoZzGxTAwvHcLppSUc6oj0ehMIuqy9I8LZKX5PKttO940oa1UhzawEuA+4CmgBNpnZOnff\nnrDa54BD7v7fzGwB8C1gfkotFpFTWmKt9yBn8P3piJygI3ICgK7YCWx7Z6T7+aDL0vmeoMtyXQkz\nSJ/7FGCXu+9297eBJ4A5PdaZA/w49vVPgRlmZtlrpoicCuI3Nt0zv67Pi6xhksvx/EHCvQLYl/C4\nJbYs6Trufhw4DJzbc0NmttjMmsysqa2tLb0Wi0joxS+ylpeV5rspOZerSphBwj3ZGXjPjvog6+Du\nD7l7g7s3jBo1Kkj7ROQUNbe+gualV3PP/DoqYmPhw9gdkKtKmEFmYmoBxiQ8rgT297FOi5kNBc4G\n/pGVForIKW1ufUV3n3R8ar7W9s6TLlK+fbyru4+9mOSyEmaQcN8ETDCz8UArsAD4RI911gGfAf4T\nmAds8HyNsRSR0EoM+p4S52TNxiiXQh0tE9SA4e7ux83sRmA90aGQP3T3bWa2DGhy93XAvwOPmtku\nomfsC3LSWhGRPvQX/KeiQBNku/uzwLM9lv1rwtdHgf+Z3aaJiEi6VH5ARCSEFO4iIiGkcBcRCSGF\nu4hICCncRURCSOEuIhJCCncRkRDK22QdZtYGvJbmt48EDmSxOfkUln3RfhSesOyL9uNk57v7gMW5\n8hbumTCzpiDF6otBWPZF+1F4wrIv2o/0qFtGRCSEFO4iIiFUrOH+UL4bkEVh2RftR+EJy75oP9JQ\nlH3uIiLSv2I9cxcRkX4UXbib2TVmttPMdpnZkny3JygzG2NmG81sh5ltM7N/ji1/l5n9h5n9Jfb/\nOfluaxBmVmJmW8zs57HH483sj7H9WGNmp+W7jUGYWbmZ/dTM/hw7Nh8oxmNiZrfEfq+2mtnjZjas\nWI6Jmf3QzN4ws60Jy5IeA4u6N/b3/5KZTc5fy0/Wx36sjP1uvWRmT5tZecJzt8b2Y6eZzcp2e4oq\n3M2sBLgP+DAwCbjezCblt1WBHQe+4u7vBy4Fvhhr+xLgV+4+AfhV7HEx+GdgR8LjbwF3x/bjEPC5\nvLQqdd8BfunuE4FaovtUVMfEzCqALwEN7l5FdFKdBRTPMXkEuKbHsr6OwYeBCbF/i4H7B6mNQTxC\n7/34D6DK3WuAV4BbAWJ/+wuAi2Lf8/1YvmVNUYU7MAXY5e673f1t4AlgTp7bFIi7/9XdX4h9fYRo\niFQQbf+PY6v9GJibnxYGZ2aVwEeBH8QeG/Ah4KexVYplP0YAlxOdSQx3f9vd2ynCY0J04p2y2BzG\nw4G/UiTHxN1/S+85l/s6BnOAVR71PFBuZqMHp6X9S7Yf7v6cux+PPXye6BzUEN2PJ9z9mLvvAXYR\nzbesKbZwrwD2JTxuiS0rKmY2DqgH/gi8x93/CtE3AODd+WtZYPcAXwPiMxKfC7Qn/BIXy3G5AGgD\nfhTrYvqBmZ1BkR0Td28F7gJeJxrqh4HNFOcxievrGBRzBvwv4Bexr3O+H8UW7pZkWVEN9zGzM4H/\nB9zs7v+V7/akysw+Brzh7psTFydZtRiOy1BgMnC/u9cDb1HgXTDJxPqj5wDjgfOAM4h2X/RUDMdk\nIEX5u2ZmtxHtml0dX5RktazuR7GFewswJuFxJbA/T21JmZmVEg321e7+VGzx3+MfK2P/v5Gv9gU0\nDZhtZnuJdot9iOiZfHmsSwCK57i0AC3u/sfY458SDftiOyYzgT3u3ubuEeAp4DKK85jE9XUMii4D\nzOwzwMeAhf7O2POc70exhfsmYEJsFMBpRC9IrMtzmwKJ9Uv/O7DD3f9vwlPrgM/Evv4M8LPBblsq\n3P1Wd69093FEf/4b3H0hsBGYF1ut4PcDwN3/Buwzswtji2YA2ymyY0K0O+ZSMxse+z2L70fRHZME\nfR2DdcCnY6NmLgUOx7tvCpGZXQN8HZjt7h0JT60DFpjZ6WY2nugF4j9l9cXdvaj+AR8hetX5VeC2\nfLcnhXb/d6Ifu14CmmP/PkK0v/pXwF9i/78r321NYZ+mAz+PfX1B7JdzF/AT4PR8ty/gPtQBTbHj\nshY4pxiPCfB/gD8DW4FHgdOL5ZgAjxO9VhAhekb7ub6OAdHujPtif/8vEx0hlPd96Gc/dhHtW4//\nzT+QsP5tsf3YCXw42+3RHaoiIiFUbN0yIiISgMJdRCSEFO4iIiGkcBcRCSGFu4hICCncRURCSOEu\nIhJCCncRkRD6/6QosYyPjKxNAAAAAElFTkSuQmCC\n",
      "text/plain": [
       "<matplotlib.figure.Figure at 0x10b994400>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "classification loss on last batch was: 0.0004617909239663479\n"
     ]
    }
   ],
   "source": [
    "mixed_curriculum_train(rnn,train_set,stop_threshold = 0.0005)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 3. Extraction"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 3.1. Initial Examples\n",
    "\n",
    "In Section 7.3 of the paper we note that the process sometimes needs one positive and one negative initial sample to get started. We take these from the training set, using the shortest sample from each class.\n",
    "\n",
    "If extracting from a network you no longer have the train set for, you can also make such a list manually. \n",
    "Of course, there is nothing to stop you from having more than one initial sample from each class, or not using any, and so on."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "['', '10']\n"
     ]
    }
   ],
   "source": [
    "all_words = sorted(list(train_set.keys()),key=lambda x:len(x))\n",
    "pos = next((w for w in all_words if rnn.classify_word(w)==True),None)\n",
    "neg = next((w for w in all_words if rnn.classify_word(w)==False),None)\n",
    "starting_examples = [w for w in [pos,neg] if not None == w]\n",
    "print(starting_examples)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 3.2. Clear the Computation Graph\n",
    "If you're using our network classes, and just running one network at a time, you don't need this. Still, it's good practice. `renew` function resets the DyNet computation graph and refreshes the calling network's initial vectors."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [],
   "source": [
    "rnn.renew()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 3.3. Extract\n",
    "It is generally necessary to give the extraction some `starting_examples` to work with, so it doesn't get stuck on a single state automaton (Section 7.3. in the paper). We made those in Section 3.1. of this notebook.\n",
    "\n",
    "You can set a `time_limit` on the extraction (default $50$ seconds) and the `initial_split_depth` (default $10$) for the initial aggressive refinement (which is described in Section 7.3.1. of our extraction paper).\n",
    "\n",
    "\n",
    "During extraction, the method will report the counterexamples it finds, how long it took to find each one, and how long it took to refine the observation table (i.e. how long it took to update the $L^*$ automaton) between each two equivalence queries. Every time it starts a new equivalence query, if the proposed DFA has less than $30$ states, it will also display it."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "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": "iVBORw0KGgoAAAANSUhEUgAAAIgAAAA7CAYAAACg5MKJAAAAAXNSR0IArs4c6QAADDlJREFUeAHtXQeQFNcRbQ440pFMECIIKCTBiWAEhjI5Y4LIiFAYjC2EESBARUYUIISFVJRBRSySrgQIDEiHEAWUSkTbZIFJhYhCwNWRc/Yd137vy7ua20t7u7Now7xXezPz58+f+T09/bv7z+7lUNU14sCRQAYSyAEF0Qz2OcWOBCTKkYEjgcwk4ChIZtJx9jkWxNGBzCUQUAuSIinSDswRxFwiSzKXUITvzRXI/r8v78s2cBFYBAw27JAdMgSsCtYDHaSVQMCimDWyRnqCn4F/BoMRKiodwYPg92Bp0EFqCQREQY7KUakP/gWcDQYz7sk9qQvSwu0E84AOfpGA7QpyU25KHbA8+B2YCwx2nJJTRkm6S3dZCjr4RQK2OqnP5JkZVrjkEBMKykFRVAa/AOPAuaADiwSYSbUL7+l7mg88BIYipuk0zQXuBB38LAGxSxDLdBl9Pv0CDFWkaIp2A0uAF0AHqrb4IIwCGoJDwRlgKOOBPDAhb7REy7/BfGAkw28FuSbX5HdgLLgJzAmGOs7JOeNoM8m3Aoxk+OWkJkkS/P7ueNai5R9gOCgHlaESyP6QfwcjGv6Ms+/oOxoDHgPDETN0huYEvwMjFT47qYt1MRyYHPolGM7orb31N+A5MBLhkw+yR/ZIU3AM+CEYzngsj6UBmAyy3wXASEK2FSRREo1TWltqy3owKgLeGLggF0yf+VCsBSMJ2VKQp/LUWI7bclv2g4XASAFnfluBsb1iJeZijNy+fVvu3r0rjx8/lidPnsjTp085XEuOHHi5AZ+8efNKgQKwN/gUK1ZMSpQoISVLlpQKFSpIxYoVpXLlylK9enWJiYkJahFmS0HekrfkS5DKwfR0pGGOzJFhY4ZJp6ROUqtoLSlcuLDky5fPKEOePL9M8qWkpBjFefTokdy/f19u3rwpN27ckMTERLlw4YJcvHjRKBUVqVKlStKwYUNp0qSJtGvXzihRUMnVW8drrs41TukG3eDtIWFZr7/218LgKdBXPHv2TE+fPq3x8fE6btw4bdy4sUZHR2tUVJQ2atRI4+LiFJbJ1+ZtPc6rKIZzE5yj+BCMdDzRJ1oXrALeBe0CLI1RmO7duxtlKV68uM6aNUsxdKU5BYY0/fbbb/WTTz7RXbt2KRUuO7h8+bJu377dq0OyVJCLetHMTXTVrpipSPGq0XCvlKAJWgrsCAZCJlevXtUxY8Yohi+tUaOGnjhxwi1S7oMPo4sXL9br16/r6NGjtX379l4pybVr13TkyJGm3WHDhrnbzGwlUwV5pI+0FlgNvA8+L7Ajmzdvtu10n3/+uW1tuRrapbs0GpwEBgpnz57VevXqaZEiRfTAgQNGCeCvaMeOHd2nTE5O1vLly+vYsWPdZRmt7N+/X48cOcLvQaktCtJH+2hR8Cz4vMAOt2zZUhcsWGDLKbdt26ZlypSxpS3PRhbqQuOXxWu85y7btumLtGnTRkuXLq3ffPONubkbNqT2AydNmqSIlvTBgwdZnpdDVnYUJMPXvWbKTDMXwQk4zk3YCfRCdu7cKYcPH5acOXNKlSpVpFWrViZU7NOnj2zZssV48/Ty8bTIiy++aKKCHTt2yKFDh8wxffv2Fdx492Ux7Fy1apUMHjxYYH3k6NGjUrt2benatasJOxcuXCgQsnTo0MF9jL8rA2Wg/AfsB+4F+fKz3WC4vHLlSiOjqVOnmuYZHltRrVo1efjwoWzatEnefPNN6y6/16PSa2GLbDFZ0ukyXVqDdmPixIkC8ykjRowQmFDhNsF8Ap4Ws86bz1wBw0g8GfLKK6+YdXj9AisjDRo0MErDyhhCpGzZsjJ8+HCZO3eujB8/Xljv1q1bgjFcGIKyrXLlypm27fzDd25rgp1B5ocCgaJFi0r//v0Fvohpng+MFcyvEIiMrMX2rHvaJPoaxcDmYCCAHIHSQ7d60dOmTXOfClbFmMClS5e6y1asWGFCwCtXrpgyVx2OqS7A8pjjGDoSP/zwg1l27txZoRhmPVB/EjVR84B/BAOFZcuWKSyqwuKmOQXlAG3QIUOGpNnnWZDdISaNBYmRGPkruAvcB9oNDht8mnv27Cnr1683zY8aNSrNaVjPhd69e8vx48flhRdeMFaGwxNx5swZVxUzfHCjU6dOpozDlgvWtlxldi75Hitfp+N3bAIFJts4HKcHhLmmuFSpUunt9qssjYKwNU7AtQC7gpdBu8FhoFChQoKnW+CQyp07d9KcwnpTkUAyygFnTGbOnCmxsbGmPjOWLrAO4Vq6yrm0tmUtt2P9K/kKA/F0mQ/+HgwUVq9ebXwxKgPT+lYwW0u89tpr1mJb1tNVEE7ArQRpTbqB/wXtRM2aNY2zSYeSjmetWrWMv2A9h/Wmnj9/Xl5//XWpW7euTJgwQRDWWatmuW5tK8vK2ahwTI7Jn8DBIKchMgJ9Jn58xezZswXDiEnFs41Lly6laoppfOK5KQhPVhj8GjwO2mk6qf3Lly+XggULyrx582Tjxo2CzJ7Ad+Bp3U+7y2yybMqUKZKUlCRvvPEGN8VqOUxBJn+oHNa2MqmarV235JZxTDmrPQv0BK+Ryj9o0CBj/TgH4wtoMenMT5482ciBDjeyp6maOnjwoPChe/XVV1OV27Lh6cR4bq/X9SbWn6/zPXf5tM24vn79+kpnleASM526bt06s80kGTqmAwYMMPuY2OnWrZspgzKZ7OG7775rtplqRnhrjhs6dKgpw9Nktl1/YKU0d+7ceu7cOWXiyZtcgevYjJbJmqytwHLgVdAF9mX37t0mCYUZXHM9dCrZnx9//NFVzaslHfHmzZsbp3T69OnuY5gJrVq1qlt+lCcUQ6Ek7jpc4XXUqVNHFy1alKqcjj6vZ+DAganKM9rINJPqOugD/UBzg/8E/QU7hDBNe/XqpWvXrtUZM2YoEz1WtGjRwnSiWbNmiifPdJbZQjw92qVLF8VsqCLHoQj/zMTWkiVLTDKMHe/Ro4fu27fP3RyjpVy5cplsJEy1u9yflZE6UvOC34MEbw5T3uwXr4EKyaX189NPP2V5Ss6xMApjYgyWTzH06p49e1IdRyVk1hTWVNkfhPTKCMcTLOP5mYVl8pFAnkQRHJhyhMYmXc95mczglYJwvqEzWBK8BPoLDBdmEoo3Pz1QCAkJCal2YZhI9fSzDkM2bwAnWO/du+dN1Szr8Hs/DFk+OvaRIn+jL730khF4ekphVRAqtScoB1oKDLWKhJ5i2DXhPDPJiPDcVsLzOG7zprvC/vT2s4zWGENcRru9Kvf6fZD7ct946fklv/wLzAtGGtadXic9VveQmOUxcufMHYFSGN/IGznExcWZuvRFMNzIyZMnBbkaE7bTH8M0v7Rt29ZEdkz62QGmEeh/MZvsK7xWEJ7gLMgvZncAl4GRhFWbVkm/kf0k+aTv0QhDe1gc9xtl8CXMdACjj4xyHL7KGBbTRIpNmzb1tYmfj/PKzlgqbdbNGgXOAiMFSZqkTcCK4NbvtyqiCnU5ofRvIMksP9l1UoNFtl75IJ4X+7F+bL4vslW3eu4Ky+2hOlQLgEdAF+gD8KUdpvgxoeZOg2ekLHyPIxThk4Kwoz1BztmcB8MZn+lnxildo2sy7CZmUhUzrtq6dWvjZDK0ZRRiVRa+3BOK8FlBHupD/e3/yfVwxF7daybhxut4r7vHyGHOnDkmRKWC8D1TLjGX4nUbwVTRZwVhJ2g9aEV6gOGGy3pZS4PtwGegL8BkoiILrC+//LI7oedLO7/mMdmKYvAkpAF/xfAPICf4xoHhAM49NQOvgwdATjtELOzQzk/1UxPZMMIJB7ytb2tB8AQY6fBriLEKr5/20yLgaTCUwTknfin9a9CBTb8wRPP7BGwEPgL5fmZBMNTAXxRqDvIHgCeDDjC7zqfELkEkSIL5kjN/tTge5E9whwpC+doDKeN0Xxjy9YRlpaz57u5G2ShTwVABrV8XsBjIKYRQUuyAyzgQ4+wCXRBS47jLfzqjZwIhjpBu0zYn1VMKoRIJcE6Jc0vhEoF53gd/t231QazmzppL4M9FBON/e2AOh9/7+Rs4FnSQVgIBUxCe6grIdzb5q0TBCv5HCv6aoYP0JRBQBeEpT4NHwGBFe2mPV6DyB+vl/erXFXAF+dV76FyAXxKwNcz160qcg4NSAo6CBOVtCZ6LchQkeO5FUF7J/wBmJZL2/HeXKAAAAABJRU5ErkJggg==\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.014844000000003632\n",
      "obs table refinement took 0.002\n",
      "guided starting equivalence query for DFA of size 4\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAIUAAAGTCAYAAAAGItEOAAAAAXNSR0IArs4c6QAANBRJREFUeAHtfQn8TdX6/mueM0USqURoRpOIyr9bSDJcTeLWrSvVrVQab/O/SKorKs0JkakyllJEptBFSshMgyFj5vV7nsU+zvd8z3z2eM56n8/3e/bZwxre/Zw1vutdBZRSH4kRo4EwDRQAKVTYd3NoNCAFjQ6MBiI1YEgRqRHz3ZQUhgP5NeBoSXFQDkoLoICP8Za8lV8rOX6msJP5f0QekcnAG0A5wG/ytXwttwOnAhcARg5rgL0PJ2SYGqYEeAfwqxxUB1Ur4FhgHWDkkAYc6ZIukAXSCLgJ6Av4WbbJNjkXYEk2BSgG5LrYTopNsknOAWoAk4DCgN9liSzRxGgv7eVtINfF1obmATkgHQF+fgQEgRAkwCnAYOBdoB+Q82JnPXqPukeVAOYBQZRn1DOqMDAFyGURuzI/UA3UDcvBarBdQboeDhue7YBKwCogV8WWNsVcmSuNgTuA3kCQZYfs0N3TolJUpgElgFyTjEnxu/wuDYG6wHigEBB0WS7LdWOZA2+DgFyTjBqa+2Qf2uvt8ZsqKkOBbCAECVATYH6IPkDOSSb15m3qNlUaWAhko/RWvVUhYBKQS5J2Q/NN9aYqAIwAslmuVdeqCsByIFckrTbFDJkhzYAewNNANstf8pdcCOwHPt/+uWxdv1V+//13+eOPP2Tbtm2yY8cO2blzp+zZs0erAcSRQoUKScmSJfVf2bJlpXLlynLMMcdI9erVhd/9LimTYr2s1w3LBtJAPgEK5sDs+ypZpfNcvnt5WfrS0tA75YsvXbq0lCpVSooWLSoFChSQggULyr59+2TXrl3y119/yZ9//ikHDx4MPXP00UdLrVq15KyzzpIGDRrIBRdcIPXq1Qtd98NBSqTYI3t0CbFFtshs4CggV4Qzqs1XN5duf3aThyo9JJUqVZLChRMP4ZMQmzdvlt9++01WrFghv/zyi/z0008yf/58WbBggSZPtWrV5PLLL5drr71WmjVrponlqV5TqSdvUjepo4CfgFyUvqqvKgiMA+yQvXv3qunTp6snn3xSnXnmmbSVVahiVJ8+fdT27dvtiCKtMJJuaPZT/XTDcowak1ZE2fJQF9VFlQWWAHbLjz/+qO68806FKkmhHaIGDhxodxRJhZcUKTgXwDmBp4Fcl91qtzoXqANsBZwQNGRV165dFdonqn379gqN2TzR7N69W3322WeqV69euqQ5cOBAnuuZfklIitVqtZ4LaKvaYmbgYKbxZcXza9VaVQVoDTipk88//1yhYaoaNWqk0HDVukPbRJ144onqzTffVOgBqfvvv1+1bNlS2UmMuKTYpXap+sBpwHbALeEvZcKECbZF9/7779sWlhXQdDVdFQUeA5yUhQsXqgoVKqhOnTrpF9+4cWPVunXrUJT79+9XNWrUUA888EDoXKYHcUlxvbpelQeWAW4JM9m8eXP12muv2RLl5MmT1XHHHWdLWJGBDFADdDtrlBoVecnW7yNHjtSN0L59++rPMWPytusee+wxhW5xvmom3UTEJEUf1UcP8X6mPks37JjPoZumvvrqK/XSSy8pZpTFJIV1Zbt27XTGr7vuOvX666+r9evX62ssPsePH6+eeeYZ9dxzz6m1a9fq89Y/dPtU//799Vfe17NnTzVp0iRVpkwZddRRR+mwPv30U+t22z67qq56qH+RWmRbmNECatiwoapTp47WzcqVK/Pc8tFHH+nz/LRDopKCY/0c838ecEIefvhhXScy7Dlz5qhzzz1XR4OBHn2eXTPWlSTOli1bdPeMv3Z+Z0ny9NNP6yLTqmffe+89hYEkhXED9corr4S6d8OGDVMXXnihwpiCfhZjA7ZnZ6/aqxoDJwObAaeEP4bixYvrl4/R0zzRfP311/o877FD8pGCbYeKwCWAE8JSgo0nvmBLwjPz/fff6wy+/fbb1mU1aNAg3RL/9ddf9TnrntmzZ4fuuf766/Vzo0YdKsrZvaO0adNG9/1DNzpwsF6tV8WAGwCn5IMPPlAYMVUYQs8XBfXAH9Ltt9+e71o6JwpGjpyVltLyL2A6MAuwWzgUfMopp0jHjh3lk08+0cHfd999+aLhfZZwpG/RokV6/gBVjEyZMkVfWrr0yJBz1apV9bmrrrpKf6KotR7Xw8+hLw4c0K6TZmdcQ+KUYDAr5kgneh462ipVqtgSfT5SMFROcl0KtAU2AHZLv379BPW84FcsaFTq+YHIOMJJwfkETiihQSUvvvii1K1bV98ePqfAeyjWp/5y+F94WOHn7TgeKSPlOeBV4HzAKfnmm2+kYsWKQgJYk29WXCQMxa45lKik4CTXEIClRjtgL2CncDJo3rx50q1bN0F9KPXr19fzA+FxhL9IzhmcffbZgraHoD0i6IKF35rwODyshDencMNCWSidgW7AzYBTsmrVKkG1KOeff4h0a9asyRPVxo0b9XdHScEYygIfA4sAO4tFshz1o6BXIOgtyLhx42TDhg0604zXeoFWkchzTzzxhJ55bNWqFb/mmXXUJ+L8Y3jhYcW5NaVLm2WztAE4W/wS4JRwxrVz58562h09NSlWrJhgviRPdHPnztWzrrVr185zPt0vUUsKKzDaXdJGkQtkXgPsEDR8BF1NNnB1cJdddplwOpl/lGOPPVZ/zpgxQ9/DmUTaK5A46GoKfxWvvvqqvgfd1VDVw3somzZt0p/WP4aHBqqenVy+fLkOy7qW7ifXtVwD0BxxOFAEiCboKQm6xYKBuGiXE55jntq2bSvfffedoLupS8g77oBxdO/eIf2xjYVxC0HDPGrVmTCSaDck0zp9Uj2pigBTgUwFNgYKL0pdc801avjw4QoZVBx8CZdLL71Ut6YvvvhihaJTffvtt7oLil+Juvrqq9Xq1asVbBFU+fLl1bvvvqveeustPUCF/Km///3vatasWaHg2MthV7VcuXJ6TCR0IYODe9W9qjjwHRApnPnkaOxNN2FGGeMjTFM6o43Tpk1TaJArtCMUjy1h743hodTU+XnooYdsnzjL1yW1Ig//5Ph+G6AysAbIVFAkKva1+cKjCTMeOTiFKiDPiB3vieyvRwuL5zj+ASupWJdTOs91LexqfABYwnSgGlQo5vUMJ4lQpEgRTQh+Pvroo9atCT/ZvUTpoJ/lyG4sHXG8xuqiJww0xRuSIgXD3AbUAxoCfwG5KHPVXL0CrrvqrkdfOUJ6ww036CFmEoElEj/D/2CRpe0l4ukLRjd6xhMNcP0sGtXq448/jveIo9cSmw4hh5QyAM3vuHj4VmAgkEvyh/whbXa3kVoTa8n6j9ZLhU8qaKspWl+x7UCxPiP1wnsoeJO6fbN48WLBRJegVBBUDcLeBCa9dPsBI7KCSa/IINz9nirlJqgJ2vroJfVSqo8G9v4Va1aoytdXVgVKFtC/ZPRo8pQGfN+x/lh9cKobPQNVokSJ0H0ceocJnnrqqae0TQSrA79I0iWFRdXL5XJ5FrgPOAO4BMh26VOtj2x/frvcdcZdMvbNsbJs2TLBy9bd5GTyztHWv/3tb7pbedJJJ+kRXQ7G+VbSZWdH1VHPkaxQK9INIhDP0RMPG5YfAZZwEg9dQwVzff3L53wEXnDUP5YUnKQLkiTd0IzM1E61U515GDzORpmpZuqJrofUQ1Gzx+7n6NGj1ZVXXqknqkiOyKqFjU+aAARJ0iYFM8lSgjOqfweyTTaoDaoq0AI4ACQSDKrlmbZnCcHSA3Mxehwl0fN+up4RKZiRLwEa9T4HZIvsUXtUI6AW8CeQqvzwww+qR48e2o6DxHDCHDDVNKVyf8akYGQvA1wPwZ5JNsgt6hZVBlgMZCIccKPVtRPGPZmkK9GztpCCkdwIlAN+BoIsr6pXtd3lx8q7wSOv9ZfSssF4XajdsluaALuAmQAHu4Im9FzDLjadwj4O5KrYRgoqcC1Arzb0XjsKoPvloEiQ0263juNOnacaWTWpJiOAccBTQFCEpdzVQEWAw/dBIrMjOnai/npNvRaoetlqDy1VS51QR+DCtK2hGZlzu1rwkeHa/Z1zONnUc7JDP46RIryvv0VtsSOtOgyu8bBLOMbC9S09ASNHNGBrQzOyfvtVftU2jPR+E1f+wlVa+7fBX/E4d87FtQ74+yXOPSleottoesEzckQDKc+SHnk08VEVqSJfAf8D4snsibOlz/V9ZMC6AVKuSux9QQYOGShjV4yVZ2Y8I7UvsMdItaW0jJe0nLzmaEmRrEZhvSSwu5SpU6fGfIRrPLjYhQ7I4NhDaNlsxBkN2NolTSeJmGmUsWPHChYWx32chCEhKIMHD3bEbD9uAnLoouek+OKLL7TrQZqyxxMSgYYtFDoWg4uBeLebaxlowHNSwPeCnHPOOdoqKVY+uCAGK8hDlk60ecSi41i3m/MZasBTUtDQlYuME1UdEydOFGu9JPPL50gmrjYzYr8GPCUFV4FxRRcW+MTNGUsFyyLaupGrp7jk0Ij9GvCUFFxOV7NmTe2BNlbW+PJZmkSaz8P0Ta9JjfWcOZ++BjwnRYsWLeKmnoRgDyVSYMCiSwr6xzZirwY8IwUXDMMjjVxxxRVxc8SqI5rPCT5EYsBwNu7z5mLqGvCMFKw64MNJmjVrFjPV7HrCSVrcMQm6NTBirwY8JQUJgVVTMXM0YsQITtjFvM5RTo5XcKsFI/ZpwBNS8EXzZXLVVDyBFXRcUvBZhkXfDUbs04AnpKBTM1YNTZs2jZkTOiThAlx6omGbgn88Dv9unYefi5jhmAupa8ATUnAeg47QsJ1BzBRz/SVHMtmYtP5YIrBksL5bn5a3vJiBmQspacAzUnC5faxeRUo5MDfbrgFPSEH3fxdddJHtmTEB2qMB10lBh6gco2jSpIk9OTCh2K4B10nBxiM3YYMDctszYwK0RwOuk4IbqtEJKIlhxJ8a8IQU9J5rxL8acJ0UnO8wpPAvIZgyV0lB41wOWhlSGFKENMBSgiOS8QatQjebA8804GpJQd/YNNOns3Yj/tWAq6Tgls50GWjE3xpwlRTctwOORvNohB72uedHupLp8+nGm83PuUoKznxys3cKF/ZwmyiWHOlYT2X6fDa/1Ezz5iop2POgD2rKypUr5cYbbxRs9ZBWHjJ9Pq1Ic+QhRxcYR+oQ20kK9ujQp7kAKJpBbuQzsb5n+nyscM15F8cpaPtAy2uLFEb5/tWAa9UHDWYo3APLiL814BopWFJQuIjHiL814DopjLWVvwnB1LlGCksVHOY24m8NuEYKbFCvNYFN6/2tEZM690oKrhqn0xFr/1Cje/9qwLWSgipgaRFeUnDcgsINV9ORTJ9PJ85ceMZVUmB7pdCOw1xLetddd2kdY7tFwYazeie+ZJWe6fPJxpOL97nqHY8b2NO0/4UXXkhL11xb2qFDh4RLCdMK3DwU0oCrJQV32Pvtt99CkZsDf2rAkMKf78XTVLlKiurVq2snqp7m2ESeUAOukoK2E5zypl8JI/7VgKukoNMzujlct26dfzViUube4BV1bdln0oDXiH814GpJQUvucuXKyeLFi/2rEZMyd0sK6vv000+XBQsWGNX7WAOulhTUwxlnnCELFy70sUpM0lwnBUsKkiKe1zvzWrzVgOukaNCggXa+vmTJEm9zbmKPqQHXScF1pHSqOnPmzJiJMhe81YDrpKBNRf369WXWrFk65xs3btR7d3Ts2FH69evnrTZM7FoDrq77sHTO8QruCMS1G3PncgvBQ05SGzVqZN1iPj3UgCukoLUVScC9wuiVn0v+WGIsW7YslHVaeZvV6CF1eHrgOCm4o0/t2rW1AQ2JYK3/sD6t3HMJAB2uGvFeA463Kfjr79+/v85pJBEis29KikiNePPdcVIwW9xJ8Oabb8635VNklg0pIjXizXdXSMGscXPZGjVqxF0hZkjhDQkiY3WNFLTkTuRt35Ai8vV48901UjB79IrXq1cv7QwtWnYNKaJpxf1zrpKC2evevbtwR6DILSV5zZCCWvBeXCcF15IOGTJESpcunafEIEmMa2bvCcEUuE4KRkpjG24IFz5Taq015XUj3mrAE1Iwy61atZJu3bqFeiOlSpXyVhMm9pAGHB/RDMUU5aBPnz56+Pvnn3/O1544KAfld2ADsBP4C5gDUMYBJQ6jnJSTqkBZwIg9GnB12WC0JM9dOFfOb3C+VD2zqrSa00oWAb8AvwL7gTzCr1yLXDrPWf2lpJSU44A6wGmHcbacLXUBI6lpwHVSKFEyGxgPTAFmAbtf2S2FxxWW8yaep19nbamtf/0sAY4FygAsGYoDRYDdh8HSYzOw/jDWylpZDPwALAH2ApWBi4BmQGugOmAkvgZcIwVf/mBgNMCXdyJwMcAXRkx5b4p06dIlfmpTuLpP9sl8YOphkIDbgXOAdkAngIQzEkUD6AE4JjvUDjUAOAtAAaFOBR4H/ge4LXvUHjUe+CdQESgMtAMmAUbyaoDdQtuFZHgeqASUADoD3wJ+kd1qtxoENAFI1obAWMDIIQ3YSoqD6qAuGUiG0sCDwB+An+U79Z1qDZAc5wGzgVwX20gxX83XSmWxfA+wEQiSzFPzVFOgIHAbsAXIVcmYFCwdXgCKACyOFwJBFlYrVYDjAT9VeW7qNCNS8NfUAmDp0BMgQbJBWOW1BJgvto1yTdImxVq1Vp0GVAVmAtkoLAFZnXQFDgC5ImkNcy+X5XIJUBqYCWTrgNC9cq/UBK4D/gCGAoWBbJeUB69+k9/kQoBzDV8CnHvIdvlGvpHLgY7AO0C2S0qzpBxebgEUBCYAuUAIEqAJMAIYBDwGZL2kUk92U91UWWA5kIvyunpdFQC+BLJZkq4+OF3dCmC9ymI0V6WDdJAZwEKgPJCNkhQpOLlUD2gAkBS5LFtkC+Zwa0tn4AUgGyWpNsUAGSBrgJ5ArgtLB7Yr+gGrgGyUhKTgpEAf4F/ACYDXwgXK6Xr9tyvtXaWrHAP0BbJREpJiskyWlQBJ4aWMGzdOGjZsKG3atEl7L1O70k9Dn5sB9kZYtWabJCTFh/KhnAuwTeGVrF69WnvV4+p1v0gX6aJtSDlWk22SkBTTZJo0B7yU448/Xvh3wgkneJmMPHEjRbrBSf1km8QlxSbZpG0dOYJpJL8GqBd2T7NN4pJitazW+WUXzEh+DVAvbG9lm8QlBUsKytGAkfwaqCgVoaFDOsp/Nbhn4pKCi3AopQAj+TVAvVg6yn81uGfiksIaxuXaCiP5NcDRTUtH+a8G90xcUrB4pNCWwEh+DXBZYzZWrXFJcbKcLMWAeYCR/BrgYqNTgWyTuKQgITgJNh3wg/hpc1oO/38LNAKyTeKSgpm9FOC0+QHAK+G2lS+//LKMGjVKJ+HBBx+USZMmeZUcHS9/KOx5UD/ZJgmnzmmPWQsYA7QEjBzSAIe5FwDZWLUmLClouNoUeBkwckgD9JnxEfBPIBslYUnBTNNwlSvDaZdJA9ZcF5JhEvAzwHZXtklSpGCm6duBVclcgH4iclXoTed84D2A7gyyUZImBa2MzgSuB/oDuSj0b0HvOKxSJwIFgGyUhG0KK9M1pAaM8gbIq0Au2mmyC0rDmm3A+0C2EoLvO6XlTrTipmsiGq1ytPP/Abki/5Z/y6cAS4gqQFZLqusXuIj4OoD+JyYDuSA9VA+9pnS4Gp4L2UWhmIbsVXvVtUBRYAiQrcJ8dgLoZuEDIFckLVJQOSwxugNcMUWPNfuAbJI1ao32t8EScSKQS5I2KSwlvaPeUSUBugZaBmSDjFQjVQWgHhB0JyzpvI+kex+xGlb/kH/IdwB9Wp4OPA3sAYIoK2Fa1wagS8WrAY5J0FFrzkk6TIr2DKsPen0pBdQE6CZoPxAEoX+uhwF68qsDZPsC4kTvJOPqIzKC1Wq1dpFYSBVStYF3gb8APwq98bA9xHYDPfr1BuhvM9fFdlJYCl2qlmpysOXO+pke834AvBaWaHSyehVA4h4D9ALo+9PIIQ04RgpLwb+qX9X/B04AMCio6gKPAHMAt/xI8YV/CnQB6G2X6WgGDAVMyWC9qSOfSc99ZNrY4lYNNEwZdRhcU0IXSY0BeoqpD7BRl8hf9o4dO/SuQrHSQ2OgpQCdttMfF31z0+aB588D2Igk6BvcSHQNuEaKyOi5hQOdqBNcerdhwQZB50UqFKigjXq4TUOkF/9CewrJsPuGybWvXKv9+Efz4s/pbPZ+CgHc1oFT/rQHIbhS3EhiDXhGivCkbdiwQaoeV1WeHfOslGlZRu/3sU7W6Q0buO/HDoAE2Dl6p+zvtF+K/1FcSpYoqbd7sDaBIYHC9/sgIXJ5ij9cvykfH6lJvDvq16+fwkZz6q+/4vdSsBOyQgbV0KFDvUtsDsSc8eBVyiyM8sCIESP0nmLFi8c23tm+fbuMGTNGPz1o0KAooZhTdmnAc1L8/vvv8s0330j79u3j5mn06NFy4MAhi/KJEyfKn3/+Gfd+czF9DXhOio8//liKFSsmV1xxRdxcDBw4MHT94MGDMnLkyNB3c2CvBjxvaF522WVy1FFHCauQWPLHH3/ovUxJBkrBggWlcePGMmXKlFiPmPMZaMDTkmLr1q3y1VdfSbt27eJm4aOPPsqz2zHJwSqHvRYj9mvAU1JwlRca83L55fGXDbDqsEoJSwUsLYYNG2Z9NZ82asBTUowfP17OP/98KV8+tufaVatWyezZszV5wvNNkrz//vvhp8yxTRrwjBQsIdiLaNGiRdysfPjhh1K4cH77Yj7//fffy/Lly+M+by6mrgHPSMEXyjZBol4HS4P9+yN2Mj6cT5JlyJAhqefaPBFXA56RglXHscceK2eddVbMBP7www/y008/xbxOspgqJKZ60r7gGSlYdbCBWaBA7FVWrDqKFCkSN3OsPljqGLFPA56QAnMcuvF4ySWXxM0JS4F9+xK7OSZ5jNingfwtOPvCjhnSzJkzZe/evdK0adOY96xfv16aNGmS5/qmTZvk559/lgsuuCDPefPFZg14Men3xBNPKLhUTjnq4cOH61nSlB80D6SkAU+qj6lTp8pFF11kM71NcHZpwHVSsI0wY8YMQwq73qAD4bhOirlz5+r9OkxJ4cDbtClIT0hRrlw5qVWrlk1ZMMHYrQHXSTF//vy4A1Z2Z9CEl7oGPCHF2WefnXpKzROuacBVUrCRyaFrQwrX3m9aEblKisWLF8uePXsMKdJ6Ve495CopFi1aJEWLFpU6deq4l0MTU8oacJUUv/zyi94gLpp9RMopNw84pgFXSbFixQo56aSTHMuMCdgeDbg6IbZy5Uqx9hZl24LW2Jz2pmU2zfJod5msZPp8svHk4n3JvwUbtMOFP8ccc4zws27dusJNaG+66Sbh2o/WrVvnM86NFWWmz8cK15w/rIGUps8yvLlq1aqqT58+CiWDAglCocGCStWoUUM98MADoXPRDqxZ0nSfjxamOZdfA66WFJs3bxYu7Jk2bZrccsstoR9moUKFpHPnzoKFxrJz56EdDkMXoxxk+nyUIM2pMA24RgoOXO3evVsWLlyooz/9dDijCJPTTjtNE4K2m8lIps8nE0eu3uMaKSyL7F9//VXrmka74VK5cmX9lZZVyUimzycTR67e4xoprBXjXC3O6oKDWOFSsmRJ/TWZpYCZPh8erznOrwHXSVGiRIn8qcAZizRVqqTnIT/T56MmKkdPukYKaxTz6KOP1gTgOEO40CkJpV69euGnox6TAJk8HzVQczKkAddIYZUQVkmwZs2aUCJ4sHHjRv09GVLwxkyf15GZf1E14BopOFpJ90U0z6eTkunTp+dJEM30uFrMGvHMczHiS6bPRwRnvkZowDVSMN5SpUrpFV933HGH9O7dO7SSnF1V+rN6++23kxrqzvT5CB2YrxEacHXuo2LFirqaICHYxuDQNj3ZsMfx6KOPSv369SOSF/1rps9HD9WctTTgKik478Etqrl+tGfPnrrBybYEz6cimT6fSly5eK+r1YdFCkvRHG9IlRDWs/zM9PnwsMzxEQ24TgprRPNIEsyR3zTgKimwflRoaGPE3xpwlRQ1a9YUriZnb8OIfzXgKiloiofZe1Na+JcPOmWukoIlBWXZsmX60/zzpwZcJQU89QssrEI2Ff5UiUmVq6SgumkcYxnaGPX7UwOuk+KMM84wpPAnF0Kp8oQUS5YsMT2Q0Cvw34HrpDjnnHO0s9R58+b5TxsmRVoDrpOC3dJKlSoJPeSFC8cu1q1bF37KHHukAddJwXxyNRhJsXbtWhkwYIC0bNlS6N3mgw8+8EgNJtpwDbg6S0rP+1YJ8fXXX0v16tX1pBYHtCjcDMaI9xpwnBT0rstlgTSiGTdunGzbtk0b2liedC2DW1pmlSlTxnuNmBSI46Sgb+2XX35Zu1229G0RwvrOT5YihhThGvHu2PE2BS2s6DvbMtyNl1VDinjace+a46RgVtjjeOONNxLmypAioYpcucEVUjAnN9xwg3Ts2DHqLj9WTg0pLE14++kaKZhNlhZc90EzumhiSBFNK+6fc5UU7HJyO8nInQOtbBtSWJrw9tNVUjCrXAyErR2iru8wpPCWDFbsrpOCET/yyCNy7rnn5mlfcNVXKj6vrAyYT/s14Akp2KYYOnSoXkZoZclyRWB9N5/eacATUjC7tMB66623QjmnVZYRf2jA8RHNeNlkF5XujLhttTXvQc933EGQVt/845LCHTt2aPsL7mbM3kuXLl30YBgXLHMi7bjjjhM4WdOf3DLClDrxtJ74WgH6Rkt8mzN3kACfffaZ3H777XopIdsVdJRG4dJATrHTjREboBwR5R9HSOmbgnMqnG7nZnMkDudUKGyXnHjiiUIfWlybys1mOCtLAhlJTgOukoL841ZRo0aN0pNj3IiW7Qv+uvmC7777bv0y6Y6AZLAcnSSTFXrVo8+KH3/8UegDnH+zZs0Sli4kG4lx1VVXSdu2bXXVlUyYOXsPSwqnBc7N1L333qvoRxOKVnjpqkePHmrChAkKv3AdPbZ8cCQZIIWCnYbq1KmTQlWj42/YsKHq37+/2rp1qyNxBj1QLs5xTMaOHasuvfRShapAHX/88QrjEwq/YMfiSxQw9kJVqK4U2iQK7Q4Ffxnq1ltvVUuXLk30aE5dd4QUsJtQsMXUv8oWLVoofofdhK8UCy996pVXXlGouhSqMAXnroYch9+QraSAlbZq3ry5JgPdLMNlka+IEC0xdAHN6uWUU05RsP3QrqDRPol2a86cs4UUMJpRjz/+uIJvTAW/VQr+rAKnQJKDJQfbHazq2N7JVcmYFGzINWrUSKG7qGBhpajcIAs87ahrrrlGt4Puv/9+xXZIrklGpIDxrSpfvrzCmICnDUgnXtq7776rG6IkPFwwORGFb8NMmxTcZgH9f9W+fXu1a9cu32Ywk4RhIzwFRyu6vQFnK5kEFahn0yLF4MGDFUYO1V133eW7XoXd2sdoqcKWmQpD6WrlypV2B+/L8FImBfv5bKV3797dlxlyIlFbtmxRWBitSwwMwzsRha/CTIkU7HJiNlPdeOONCtZTvsqI04lhiQEDZNWkSZPAN6YT6SppUrAV3qBBA4VJJoUJqUThZuV1bIKn21FPPfVUVubPylTSpHjsscd0KcF5jFyWvn37KkzUqfnz52etGpKaJeXU9MknnywghmDzt5ydPGTGwQQ577zztB3H559/np26SIbuXbt21aN8sGFI5vasvwf7qeqh/C+++CIr85qwpODmLLRteO655+TOO+/07JcxefJkbaXFtGDEUVtZeZYYRNy0aVPhhjYjR470MhnOxJ2I6rCjVLBaUtg+MtGtjl2Hc3c9asppbpjj6TESTst7KTAh1F1zWI95mQxH4k7Y0LzyyivV1Vdf7UjkyQQKe00Fy+/QrSi5VNmyZfVsbOikBwecSeUEIMmRbZLQmpvmc+ibO1NMJREq3RbQwNcSWn2DpCFDX+u82580DkYXXb799lu3o3Y8vrikwLCu3rSF9o1eCewc8kTNJYe09saIap7zXnzharc5c+Z4EbWjccYlhbUNQ7Vq1RxNRLKB01EabC310sMLL7ww2cccu49LC7ipTbZJ3HUfNJ+ncJsnrwXdP+HeYfTBSSFBBg0a5Gmy2PuwdORpQmyOPG5JYXNcGQUHMz/hkgDuF8JdCTFTq5cJZBSoeTiqBuKSwioh/PRr4EYyJATF8rQXNWcunOT+Z5aOXIjOtSjiksLaWJb+Lv0k3NCWywSt9HmVNlZhmeyB5lW6E8UblxT8VbLe9PoXGZkJLi2Eib7evjLympvf2V2nW+lsk7ikYGbZ7Zo6dapn+Z44caJegAyTv1AauKltr1699HLD0EmXD5ge7roMG06XY3YhukSjcV4Pc8NPlp6yx6p0vZrrySefVJyQ8lpyepibaz25vI52BF4JV5dhzMRX1l5Yza6wWNkrlTgab8K5D8Zups7zvoOcnzpnDWaMbI7U46CHMbKxfiNcFkijXWOOl/3meElVHySGMdxVyhjuWkVE2Kcx8Tcm/mF0OHJoFgOZxUBH2BB2ZJYNhikjCw+TblNE5h0+ts0C40ilZMn3tEnB/BtXBFnCgohsZEQKhmWclkRoNAu+ZkwK6sC4N8oCJoRlwRZSWOGFO0KDI9PAOEKDWZ9xhGa9RHzaSgor3CC6TKR7BeNP89AbdIQUFjmC4lw114furfdlfTpKCiuSZNwwW/fa/WncMKeu0YQLjI/MD2Z+hORFddhO62x63Kfn/VNPPVWMw/bMdZ1JCK6SIjKh3NqBpn7Tpk2TBQsWaM/7kVs70ECXWztwa4ZoWztg4bPeF8Rs7RCp3fS/e0qKaMmOtwnM6tWrNXG4BsQiCTeBIXH4xxVbLGXMJjDRNJv8Od+RIl7SR4wYIR06dGA7KN5t5lqGGkhozZ1h+ObxAGrAkCKAL83pJBtSOK3hAIZvSBHAl+Z0kg0pnNZwAMM3pAjgS3M6yYYUTms4gOEbUgTwpTmdZEMKpzUcwPANKQL40pxOsiGF0xoOYPiGFAF8aU4n2ZDCaQ0HMHxDigC+NKeTbEjhtIYDGL4hRQBfmtNJNqRwWsMBDN+QIoAvzekkG1I4reEAhm9IEcCX5nSSDSmc1nAAwzekCOBLczrJhhROaziA4RtSBPClOZ3kwJOC+5zBzZLTesqp8ANLCq45ve++++Skk06S0aNH59RLczqzgSUFt8eEoxHB/utO6yjnwo+726CftcEdeeAa2s9JDGzaAltSBFbjAUi4IUUAXpLbSTSkcFvjAYjPkCIAL8ntJBpSuK3xAMRnSBGAl+R2Eg0p3NZ4AOILNCm2bNmiVbx79+4AqDo4SQwsKSZMmCB33XWX1vTHH38s2FRXOA9iJHMNGO94mesw60IIbEmRdW/CRxkypPDRy/BLUgwp/PImfJQOQwofvQy/JMWQwi9vwkfpMKTw0cvwS1IMKfzyJnyUDkMKH70MvyTFkMIvb8JH6TCk8NHL8EtSDCn88iZ8lA5DCh+9DL8kxbcTYhs2bJBHH300j564v9jChQvl0ksvzXOe+4c9/fTTec6ZL+lrwLek4D5h1apVE5KjYMHYBdqBAwfk3nvvlRdeeCF9LZgn82ggtrbz3Ob+lwIFCugVYIULFxa++Fh/TNl1113nfgKzOEbflhTUOauKM844I676TzjhBFmxYkXce8zF1DTg25KC2Tj99NOlVq1aMXNUpEgR6dKlS8zr5kJ6GvA1KZglvnRWIdFk3759cu2110a7ZM5loAFfVx/M1y+//CI1a9aMmkWWJNwO24i9GvB9SUH/Ew0aNBA2PMOFpUfnzp3DT5ljmzTge1Iwn/RDEdktZW/kmmuusUkNJphwDfi++mBif/vtNzn22GNDe5yTIBdccIFMmzYtPC/m2CYNBKKkOOaYY6RZs2Z5SguWHkac0UAgSMGsd+rUKaQBti/at28f+m4O7NVAYEjRtm3bUElx2WWXSYUKFezVhAktpIHAkKJs2bLSokULnfDwUiOUE3NgmwZ809DcuHGjLFq0SP9xbGL9+vX6jxNiO3bs0F7wdu7cKfv375cSJUqE/sqVKyecJeXfcccdJ3Xq1JHTTjtN6tatK8WLF7dNUbkUkGekIAGmTJmi/9iL4MunsFrg0DZfMHscfNllypTRL7hQoUIyZMgQ3b7gSnO6S9y8eXOIQGvXrpWff/5Z9uzZI7yXxLjoooukadOm+o8NViOJNeAaKQ4ePCjffvutjBw5UkaNGiWrV68WVgkXXnihfnH169fXv3ASIZ5s27ZNjjrqqJi3cPxi6dKlusSZNWuWTJ06VebNm6dnWc8//3xh26Rdu3Zy4oknxgwj5y/AbsFRgXsA9eyzzyrMZiooW+HXqx555BE1Z84chRfoaNxW4Nu3b1effvqpwjyKqlixok4Hurhq6NChCqWKdZv5PKwBDgg5Ivi1KgxDK8xkKlQJ6p577lE//PCDI3GlEigm0dT48ePVVVddpVDFKFQpqlevXgrtllSCyep7bScFqgVNBiq8du3a6t1331Wo+32pRLRB1AMPPKBKly6tKlWqpHr37m1KDrwp20jBX+Dzzz+vSpUqpTCrqQYNGqTQU/AlGSIThZ6PevjhhxV6NQq9F/Xll19G3pJT320hxeLFixUspLRSn3zySYWeQSCVCAsuXa2w7XPzzTcrdIEDmY9ME50xKd555x1VsmRJdd5556lly5Zlmh5fPI8ekm4H1atXT8Ek0BdpcjMRaZMCXUzVvXt3hXkI9eCDDypWH9kkbBs1adJEtzcmTpyYTVlLmJe0SIEtFRTM4FTRokUVBpMSRhLUG5hPDKnrHtQHH3wQ1GyknO6UScESAib1+hc0efLklCMM4gM9evRQsOFQw4cPD2LyU05zyqRglcES4vPPP085siA/cMcdd6hixYqpr776KsjZSCrtKQ1zDxs2TJvAffjhhzlnCgdtSseOHfUmdk888YSexudEHedZOITPP/xY9BwNGt6CkVPB2Ieev+HaFF4LiiRNilWrVsmZZ54p119/vfTv3z8o+bM1nRgul7PPPlvP22DAS0/UofTQBKGJILev4kQdZ3O3bt3KUljHz2tcAknrcz7fqFEjady4sX7e1gTaFFjSpGjdurUsX75c5s6dm9NT0pizEU6svffee3mswSLfB6f4N23aJJy55SZ4nL3lcgTqjxN2tEZH70Y6dOigSyBfGQ0lU8lgplFPIsEfdjK3Z/09HNg6/vjj0x6kg5mAGjx4sAIh9AgwR1JvueUWBfL4QndJNTQ5o9i8eXNfJNgPiYABkB69RTWacXJQzah+/frpWWQ2ZOF+QbEr7KUkJAVHKTlANXbsWC/TqaZPn64ef/xx9cwzzyjYSXiaFkbeGTPAaB/Ylg5O4cOdgibbueeeq7CsIU/YnDr47LPP9IwudZGq2QFLp2R7TglJ8Z///EfBCsrTya1///vfCgY5ushG3a1JyuluL+Wbb77RVer//vc/W5PBeSQYAKlTTjlFoU2iwyZBeO7NN99U2LlZ3X///aply5ZJEQOOXhT8d2iyUY/JSEJSoKWsbr311mTCcuQezkPcfffdmpQcOPviiy/0vAQaagoNX0fiTCZQpoUGOy+++GIyt6d0D6f0YYaoWrVqpV88eioKDf1QGJx9rlGjhp72D52McTB79mxF4vLHZAspWGSxnhs4cGCMKJ0/jf3M85VSt912m84kLae8lCuvvFJh/YkjSSD5+SJZpfBzzJgxeeJ57LHHdCM1GeMgVk2pkCKuiT/aE3pwhn1rrwRDzNoINzx+/IL01/Lly4efdv2YeoE1mSPx0q8XxzLeeOMNHT7HOMKFFuscD4EVWfhpW47jkoL9bApH5rySaHGvWbNGSAiOF3gplStXFi5NcErQbtADZQw/0qCZcVM4/mG3xCWFtXGbrwZWoAEOt6MnEteq225FRQuPxLR0FO16pueqV6+uR0i5XCFymJxD6RRraUSmcYU/H5cUMK3T97KY8ot88skn+ldjbSrnZbqoF0tHTqSDcyskRDThUgZKlSpVol3O6FxcUnBSh+JkEZlK6jk8DEsv/ZfKc07dy+rV0pETcXCdDEtpEoATb+HCeRgKrMPCT9tyHJcUGMrVkThRb6Wa+j///FM4O4mekHASyg9CvXAG1AmhTw4unDrnnHN08GxHhYv1Q3WdFPwVYBBFMIIWnh7Xj3ft2iXshfz3v//Vq8qsBLA+9ZKw1AudpyQjnFpPVtD3lH/961+6Mf3KK6/oH0HkO+DE2llnnSVYRpFssEnfF7ekYCjsFqHPnHSAdt9ID3j0RXH00UcLxiUE8wT676mnntKzlF4t/+OyRxKS+oknXDOLhVBJ95RYVXTt2lV3NWECKPT5BQMfwZoUDjTqqDg9j3ELefvtt0PuGXhhxowZgiFywchnniRZjWE+l5TkGRGJ8sUaRPFqdRf8WumBF2Qm3yfN5LwSVGUK3cKok1dcpsghaayP1Wnm3BFHPxMJSKY4+YjV8grrbUO3c/SUi5Y4wtm3b1/10EMPRR1Q5CAj9YSV+KEBP66Gg3GQPs/0Ml2cB4knCYe5mSCuA73zzjvjhZNT1ziLyalzmiaGCxqG6h//+Id+qbTpJBksMnMVWixBe0GHRTNHLitA1RD1Vg5vc21uPOFcB0qaeLckvJaQFAwB9Zoe7l6BxTJGlP61cvif9g+coOrTp486+eSTNQG4dtYiQvgnz4cLinSF8ZbQmlYMTul5FA5JZyLY911xvigTSYoU/GUw0yyGcl3gD0NXBXBpoK6++mq9SJnrZsMJEOuYhjWcy+EEFyf0+HfJJZdocthhQ0HbjGSnx+O9x6RIwQBoT8HMej0JFS8zTl+Dnap2pcCqgbrgS41FgGjneT96DOqf//ynJgK62U4nOa3wkyYFQ+/WrZu2a/ByyjqtXNr0EBt7fNkYRUyLFLTYCoKkRAq6FGCLGu6H8lkGBSGzmaSRrXi2CzhlTfnpp5/Uc889p+AiWhOEpYdVgkQrJXhu3bp1mSTBtWdTIgVTxdYvXQ2QHGws5YLQcJmLqNmziCbs4r3++uvajpVVBHsd0aqWoCzATpkUVAozxy4Zu09ciJvNMnr0aG3KBj9ZSS2ihk8u3V5go5y+OlhCWA3RoKxgT4sUJAFNxmDooc3GZs6cmZW8YFeTVQL7/akaylIh7FFweSXbYuxy0jQuCJI2KZg5Vh9weKqLyp49eyoOdGWDcOyBhrGsAuidxw6hbuzodtqRlkRhZEQKBs7M0o6QjTD6cwhKERlLMXTLxN4Fq0ea0ueiZEwKS2nz58/X3mz466InPPqRCpLA16Zq2rSpri5oGJwrjeho78g2UjBwlhoDBgzQnuY41k8PNyyK/SzfffedNp9ng5AumoJS7zupU1tJYSWUZuesi+mGkOsk6dQU07rWZc8/uXSBQ85w0ax7Bw0bNvR8BZznSglLgCOksMInOdh/59Auf4mnnnqqXvpn96oqK754n5xo4gAUh5g5jc1qjt3MSZMmxXssJ68l7YoALzUjoZ9s/DoF/X69PJ/GMRdffLH2y02n6nYby9AVANo52je35Riedo00b6Nvbm4PEWk2n1EGs+hh10hh6Qw/PUG9rS2L+LJIFloEcYsGlCTaaTtNzKztGvji6MWf2zlwqwb0crQRKz34h3vxp2ke7RixFlMv0FmyZIl2IsL1EfQDQQLSxwbN5o3E14DrpIhMDq2U0djTDj2s/T7oHIWGq/y1JytcB8HtIGhTytVT/OPOANzewUhqGvCcFLGSi56MwIpIL3bh+gqrZCBRaM1tlRxckMNShdtEGLFHA74lhT3ZM6Gko4GE1tzpBGqeCbYGDCmC/f4cSb0hhSNqDXag/wevXqUI/glxgAAAAABJRU5ErkJggg==\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.0820760000000007\n",
      "obs table refinement took 0.003\n",
      "guided starting equivalence query for DFA of size 5\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAQMAAAGTCAYAAAAst3eIAAAAAXNSR0IArs4c6QAAQABJREFUeAHtXQm8VeP6fkuDJiVDJbNEKjQoyRASN0qKQlSSi7jGkITQ/VPGq3KFuFRoMEQTlYpCKUMSSpqLSlFpkPr+z/Npbfucs88+e1h77zW87/Pb5+y9hm+t9Xxrvesb3qGYMWakqCgDykDoGSgGZWBCz4ISoAwoA1JcOVAGlAFlgAyoMtD7QBlQBiwDqgz0RlAGlIFwKoPdsltaAsU8jBfkBb09lYGsM1Ai60fM8QF7SS/5AHgOqAR4TabKVLkBqA00AVSUgWwxEKrZhJEyUjoALwFdAC8KWy4XAnOBOcBBgIoykA0GQqMM5sk8+6btJt3kP4CX5Tf5TRoD+wLTgNKAijKQaQZCoQx+kV/kJOAwYBJQAvC6fCffWYVwsVwsQwAVZSDTDAR+NmGX7LJdAza/RwF+UASs9GOB4QC7NIMAFWUg0wwEXhn0kB7yMfAWsD/gJ7lALpAHgVuBDwEVZSCTDAS6mzBUhkon4FXgMsCPYsSgo3CxzAA4oHgIoKIMZIKBwCoDPjinAf8C+gN+li2yxQ5+lpJSVimUkTJ+vhw9d48yEEhlsFbWSkOgFjAe2AvwuyyWxXYQlAZTwwAVZcBtBgI3ZrBTdtpmNd+irwNBUASs9KMAXg/xBKCiDLjNQOCUwc1ys3wBvA1wnj5I0kJayMPAncBkQEUZcJOBQHUTaNP/T2A00BYIqlwul8t7AMdFjgBUlAE3GAiMMvhEPpFmAN+aDwFBlm2yTZoCfwLvb35ffl31q6xbt85+Nm3aJFu2bJHff/9dduzYYWlg/Jq99tpLypYtaz8VK1aUAw88UKpUqSKHHHKI8LeKMhAIZbBaVtsBwwbSQN4B6JEYdFkmy+w173vrvrLoqUWRy+UDX758eSlXrpyUKlVKihUrJsWLF5edO3fK1q1b7ee3336T3bt3R/bZf//95eijj5YTTzxRGjZsKE2aNJFatWpF1uuXcDDge2WwQ3bIGcCvwGxgHyAsQr+F5subS/dfu0uvA3sJH+oSJYo2taYi2LBhg/z888+yZMkS+fHHH+W7776TL774QubNm2cVxsEHHyznnXeeXHbZZdKsWTOrUMLCa1iv0/fK4Gq52o4RUBEcA4RNBsgAuQV4F+C0Y7rCFsTs2bNlypQp8uabb8pXX31luxK33HKL/POf/7StjnSPoft7lAEGRPWrDDADTDHgXSDM0sV0MRWB7wG35dtvvzU33nijQdfDYJzBDB061O1DaHkeYUA8ch5Jn8Y0M82UAB4Cwi7bzXbTCKgFbAIyIWvXrjXXXXedwfiDufjiiw0GKPMcZvv27ea9994z/fr1MzNnzjS7du3Ks15/eJ8BX9oZLJflcgnAICD3AGEXxjt4E9gIXAHQn8FtOeCAA+S///2vTJw4UaZNmybnnHOObNu2zR4GisIOOC5fvly6du0qb7/9trRu3TrPIKXb56PlZYAB7+urvGe41Ww19YE6wGYgW8I344QJE1w73Msvv+xaWU5BM8wMUwq4D8ikYJDRVK5c2Vx55ZW2BXDqqacaPPyRQ/7555/msMMOM3fddVdkmX7xPgO+6yZ0NB3NvsAPQLaEN3fz5s0N3oyuHPKDDz4w1atXd6Ws/IUMNoPtOMpb5q38q1z9PXr0aDY/zNNPP23/v/tu3nGb++67z2B608DmwdXjamGZY6DoeagMtEZSLfJxedza5tP5iLb6bgoolunTp8uXX35pDXSOPfZY2xSm4U7Hjh1l8uTJ1lCH8/ZsAlerVs02k9lk/vzzz+0+eFMKHvLIaW3cuFFee+016d69u6BVYaftGjRoIG3btrXz/4MHD5aDDjpIWrVqFdkn3S+0wPwcuBKYBRwHZELatWtnbRKeeeYZW3zdunXzHKZOnTrW8Gn8+PFyySWX5FmnP7zJgG/GDGiLfxfwCEAbfbeld+/e8sMPPwin0Gh0w98UDIzZ+XZ+54N+zDHHSJkyZayVHw11+L1nz56C1oM0bdo00o9GN0A4V3/zzTfLwIED5e6777bbcX7/+OOPl9KlS9uyaAHotnC68QSAYyq0v8iUtGnTRpYuXWqLp3KMFlo4UhYuXBi9WL97mYHMNTrcK5ljA/sBZwGZEBjhGBjsmKlTp0aK79u3b+Q7Wgu2KTxkyJDIsmHDhtmR9Z9++skuc7bBHH1kG7Qo7H6Yr7fLOE1HwUNkoATs90z9WWVWmdLAFUCmhNOMaCkZmDoXOAR5wH1vbrjhhgLrdIE3GfBFy6C8lLcOSDNlpm36uq1c2fTnG79Dhw4yZswYW3yPHj0KHIbbOULLvPnz51v7frYe2MWgLFr0t2kwuwCUCy+80P5n18OR6LKcZW7+d+ImMgdDpmTz5s2FWiZiatEetmrVqpk6vJbrMgO+UAa85r7A2QC9EX8C3BY25ffZZx9h0xeDhfLrrwWb19EPMO396eiDgTJ54oknIrb80Tb/3Ibi/I8+5+iyope78Z1em/8HUCGcDGRKPvroI9lvv/2ED77jFOUci4qCctxxmRmzcI6j/91jwDfKoDhyxDJacDmgHfAH4KbQSYcDgRzs46Bg/fr1rf1+9DGiH2Da9NerV08aNWokvXr1EkylRW9a5PfosorcOIkNvpavkR6mi83KRFPtTMmyZcusufLJJ/+lbFasWJHnUOvXr7e/VRnkocXTP3yjDMgi06GNAXjD3wi4JXyrof8rFSpUkEGDBsm4ceNkzZo19mbnMZwH12n6clmfPn2sJ+AFF1zAn0kZ2LC86LJsAS782SAbpA1A780ngUzJH3/8IZ06dZJDDz1UMLVoB0NhdZjncHPnzrVekDVr1syzXH94lwFfKQPSyLiGjHrMQCb/BdwQDOfIs88+S5sLW1yLFi2sByC9ACnOSPknn3xit6FnH+MFUGFw6oxvQWeKbfXq1ZEuBreh/PLLL/a/84flYeDRegsuXrzYluWsS/U/80NcCjDsG/NDlARiCWc9Jk2aZKc6Y60vahmvidOKfNhHjBhhW0TwXZBHH300wh/HUGB3IBhwjdlFKuoYuj5HDHhzXLPos3rAPGBKAh8B6QrMag0eUHPppZeaUaNGGdzYhkYz0XL22Wfb0fEzzzzToIlsPv74Y2tlhylCc9FFFxmY4hrYEJh9993XvPTSS+aFF16whkWoVtO+fXsza9asSHGctYCrsalUqZI12omsSOPL7eZ2UwaYC+QXvMmt9SRMhQ3GRex1YDo0/2ZF/p4xY4bBQKvBOIHhd0c4G0NrQ7SS7PVgGtW88sorzmr97xMGfGeB6PC62+w2bYAqwAogXYHrrkF3wT7oscriDb9y5co8q9DUz2Nhx21YRiKCAUqDqESJbFrkNsPMMLoj4O+wyLY8j7Fjx5rOnTtbj0MqpZIlS1pFQEV07733RrYt6gsVGQyl7L7wSbCKL9Y+tNR0plpjrddl3mbAt8qAtNJD7zigIbANCKOwJcAWwW0APQffeecdQ/sGmgJHKwB+dz6IgGQeeOCBuHQh2In1QMTAqt0Pg6UGDkhx99GV/mbAV+bIuJnzSAWpYKMgN5JGci3wMhAmQdRDabO9jRw98WhZPXK1VB5T2UYpYrQjjg1QGKwklqCVYBfj9rXjFwsWLJCvv/7aBjZBF0A4OwBnJGs6PWDAAIEzUqxidFmAGPB9pCPWxUTgfIC+C4z6EwZZunKpNO7ZWNa9tU7gyGlnPPhgJyJUBDSV5n8+9I4rMt2U6TtxyimnCMZIpHHjxtbnIpEydRv/M+DrloFD/3lynjWyuUPukOOBs4Cgy2MHPyab+2+Wm4+/WcY+P9b6VfDhLqwlkJ8PWkeee+65NqTZkUceaS0waUSlEmIG/N3LyXv27U1768OwxCzJuyJgv4aYIXbAcKQZGbmyzz77zIYnQ9hz28envwBu65gfKA2Dpn9kX/2iDJAB39kZxNPbL8lLcjBAwxsEBY+3qW/X0S25O9ALYLQnRxjinH175k946623pGXLlraJD6UQMZpytkW92y6C81v/KwNkIFDKAClC7IDiSlkpXYGgyRpZY30z6KNRWKIYdhXoX4FZBRsK/amnnhIn1gDXUeg/4XwPGkd6PakzEChlQBoOB0YCdNbpBwRF6ItBnwx6cL4K0FejKKETEa0DGe78m2++kVtvvVU4SEhlwBkHFWUgmoFAzCZEX5Dz/Sl5Sm4HxgEcYPS7XCPXyAiA3QSaZKcqVASM2sTBwhNOOCHVYnS/ADIQWGXAuuoEMLnIZ0ANwK9CHwzGJWBm6daAijKQCQYCrQy2y3Y5DeBg4qcAjZT8Jh/JRzaOQ2/pLfcBKspAphgItDIgaRxMpEvvKQBzC/gpKaufzz1TN6yWmzkGih6Fytyxs1Iypxo5mMixg8JG4LNyIkkehK2ai4D9gVcAPymxJC9VN/cIA4FXBuSZXYX/AH0Apmz3gzDk+Q8Ag7n4sXvjB471HPMyEJr5pevlevkCYPqxdEfk81Lo/i/OhAwH2Jrx88Cn+8xoiZlkIBQtA4fAgTJQ6gC0UPwNcEuYI8Et+UA+kB4AA5oGYUrULV60nMwzEPgBxPwU0oqvIbAaiCvMKcqo6W3w2TvOlnOwrj0+P8bZJslVHaSDzRyV5G66uTKQFgOh6SY4LFWTanj3fiDzgHgye+Jsebzj4zJ49WCptHelQjd9+dWXZdyScdL3075S82R3gn/SHVtFGcg2A6FrGSRK8BVXXGF9/Z3kKLH2ozUfLfkYEPVf//qXjRQcaztdpgz4gYFQjRkkWiEMBc7ovowCHE+oKJz8AMOHD89I+PN4x9d1yoCbDKgyiMEmQ4kzIxCzJceTV199NeL9x4SqSLUeb3Ndpwx4mgFVBjGq54033rCZkhgarDBh6+H111+PRBaiFyBbByrKgF8ZUGWQr+YYSJSxAIrqIrz33ns2LbuzO/cbPXp0gZyDznr9rwx4nQFVBvlqCMlRbAYkBgiJJ0jJXiAmALMNMTWbijLgRwZUGeSrtQkTJkiNGjXk6KOPzrfm75986Jm63QlH7qxhV4FKQkUZ8CMDqgzy1RqVwT/+8Y98S/P+pCLgmEF+oXJAFiM7+Jh/nf5WBrzOgCqDqBpi0lSGCCtKGTBjc/HisaljdmUGJFVRBvzGQOw72m9X4dL5Tpw4UcqUKSPNmjUrtERmVObUY7yU6kg6Wuj+ukIZ8CoDqgyiaoZdBCoCKoTChDMG8YRWiciybEOWx9tO1ykDXmNAlcGeGmEugSlTpkiLFi3i1hHf+vFaBdyZCmHkyJFxy9GVyoDXGFBlsKdGmHR048aNcsYZZxRaR6tWrbKJSTle4HyKFUMMInyc385/VQaF0qgrPMqAKoM9FfPRRx8JUpPFDR9evXp1a3HIloHzGTFiBNPaR347y+M5OHn0XtDTCjkDqgz23AAffvihNG3atNBZgpDfJ3r5IWBAlUGUMjj99NNDUOV6icpAbAZUGYCXRYsWyU8//SSqDGLfJLo0HAyoMkA9z5o1S0qVKiUNGjQIR63rVSoDMRhQZQBSvvzyS6ldu7ZVCDE40kXKQCgYUGWAav7iiy+kXr16oahwvUhloDAGVBmAGVUGhd0eujxMDIReGSxbtswaG5144olhqne9VmWgAAOhVwb0UqQFoSqDAveGLggZA6FXBj/88INUq1ZNypcvH7Kq18tVBvIyEHplsGTJEjniiCPysqK/lIEQMqDKIIYyoAHStGnTUr4d0t0/5QPrjspAGgyEXhnQE9EJib5u3Trp0aOHHHnkkSlFK0p3/zTqUXdVBtJmIPTKgG7LlStXtkQuXbpUOnXqJNu2Metq8pLu/skfUfdQBtxjIHSJV/NTx0xIjjI46aSTYgY6zb9PYb/T3b+wcnW5MpANBkLdMmDsAaZRq1Sp8CzL2agEPYYy4AUGQq0Mdu7caeugdOnSXqgLPQdlIKcMhFoZsGVA2WuvvXJaCXpwZcALDKgyQC2oMvDCrajnkGsGQq0Mck2+Hl8Z8BIDoVYGTn6ErVu3eqlO9FyUgZwwEGplULJkSeFHlUFO7j09qMcYCLUyYF2ULVtWmFXZERohUbZv3+4sSup/uvsndTDdWBlwkYHQKwPmSvj1118tpUyvdvPNN9vvb7/9trzwwgs2UGqifKe7f6LH0e2UgUwwUAwJQEwmCvZLmY0aNbJRkR977LGUTnnUqFHSvn17m0glpQJ0J2XAIwyEvmVQpUoVWbt2rUeqQ09DGcgdA6oMoAzocqyiDISdgdArA7ovL1++POz3gV6/MiChVwZHHXWU0PWYadRVlIEwMxB6ZcBAJjt27BAGOVFRBsLMQOiVAVsGlMWLF4f5PtBrVwa0m1C1alUbz2DBggV6OygDoWYg9C0D1n7dunXl66+/DvWNoBevDKgy2KMM5s2bp3eDMhBqBlQZ7FEG8+fPVyvCUD8KevGqDHAPNGjQQDZt2iQLFy7UO0IZCC0DqgxQ9cyzuPfee8unn34a2htBL1wZUGWAe4AxDerXrx9RBuvXr5ehQ4dKhw4dZODAgXqXKAOhYCD0eROcWma+xcmTJwtzH8ydO9cupkNn06ZNnU30vzIQaAZCqwwY0IQP/9ixY2XMmDHC1GhsITArsyMMlFqhQgXnp/5XBgLNQCiVAROn1KxZ03orUgE4+ROc/06NM5S6KgOHDf0fdAZCOWbAB3zQoEG2bvMrgPwVrsogPyP6O6gMhFIZsDLbtm0rV199tZQoEb9xpMogqLe+Xld+BkKrDEjE008/LYceemjcJCqqDPLfMvo7qAyEWhkwMvLo0aPj1q0qg7j06MoAMRBqZcB6rFevnvTr10+KFSsWs1pVGcSkRRcGkIHQKwPW6W233SbNmjWLOX6gyiCAd71eUkwGVBmAFrYKhg8fLuXKlcvTQuDgYqlSpWISpwuVgaAxoMpgT41Wq1bNmiBHp5HgmIKKMhAWBlQZRNV0q1at5Prrr4/MLpQvXz5qrX5VBoLNQPxJ9mBfe8yre/zxx2XKlCnWnTn/eMFu2S1rgTXA78A2YA5AGQeU2YNKUkkOAioCKsqAXxgIfXq1WBU19+u50rh+Yzm43sFy/uzzZT6wGPgZ+BPII/zJHK0xGhFlpaxUB44F6uxBfalvf+cpQ38oAx5gQJUBKsEAswG+3T8EPgV2PL1DSkwoIY0nNLaPcU2pad/2fONXAyoAbAnsDSCxO/TBX2BrYQOweg9WykpZAFChLAT+AA4ETgeaAa2BQwAVZSDXDIRaGcySWTIceAvgQ3sEcCbAB5WY/r/p0qVLF9fqaKfslC8AKhxiOrAZOAloB1wJUNGoKAO5YCB0yoB9/WHAs8CXQG3gYqAtcDyQTWErYTJAZUT8BlwIXAc0B1SUgWwyEBplQCUwCHgM2AJ0AK4FTga8IDtkh4wGBgMfAQ2BPsD5gIoykA0GAq8MOB7wPNAbYH/+RuB2YH/AqzJX5sqDwDtAY2AAwK6EijKQSQYCbWfA/nkT4AbgCmAp8DDgZUXAym4AjAE+B0oDbL10B34FVJSBTDEQSGXA1gC7A3yrlgKoFJ4A9gP8JPWknh1kfEVekTeBE4FPABVlIBMMBE4Z8O15AXA38BDAEXvO8ftZOkpH+RrgdXCW41FARRlwm4FAjRmsklVyHsB5fr5J2TIImjwuj8udAAc/BwLFNXdu0Ko4Z9cTGHNkWgjSRmAfgEZDQTXk4eDnkQBbCzSNfh0oAagoA+kyEIiWAc2EmwL0BZgC0Dcg6MLpR7aCOEX6IqCiDKTLgO/HDDhd2BJgc3kiEAZFwEo/DRgFDAXuB1SUgXQZ8L0y6CE9rBMRFcEBQJiESpA2CH2BDwAVZSAdBnzdTaBjEWcORgDtgbAKzak5TsIZh30BFWUgFQZ8qwzo9HMcQLPd14Awy0bZCJ/KmtIF0GnHMN8J6V27b7sJtOFfATwChF3YGrgPYJdhOaCiDKTCgC+VgWNhyLn2w4BcCxO3bt/OCCe5E3o6VgGeBlSUgVQY8KUy4GDZMoDKIJcybtw4adiwobRp00a2bduWy1OxAVa6Slc7u8AulIoykCwDvlQGr8qr1rqQYwa5kuXLl0vdunVtNudcnUP+414lV1lDJJ1ZyM+M/k6EAV8qgxkyI+fBP5ijkZ/DDz88EZ6zsg3OSI4GaJCkogwky4DvlMEv8ouNJUiLQ5WCDJAX9WwsyIsuKZoB3ykDjhVQOJWmUpAB8uJwVHCtLlEGCmfAd8qALQOK32ITFF4F7q5h4Jb1gIoykCwDvlMGjGVIKQeoFGSAvGwFVJSBZBnwnTKoLJXtNdLqTqUgA4zloCbJBXnRJUUz4Dtl4HQP6MuvUpCBdbJOu1AFadElCTDgO2VQQ2rYIKGMa6hSkAHy4vcwbwWvSpdkgwHfKQNGC2a+wpmAF2Tjxr+6K7k2RyYXNNP+GDgFUFEGkmXAd8qAF3g2MBbYBeRKfv75Z3nqqafkzTfftKfQs2dPmTRpUq5Oxx6XxlicbSE/KspAsgz40oX5B/nBWtpRIWjGob+rnC7MjGnAJCwqykCyDPiyZcBxg2bAU4DKXwww6/NI4GpARRlIhQFftgx4ocxifAbAcGfnAmEXKgEmcWXad46rqCgDyTLgW2XAC20NMEQ6m8V7A2GV2TLbppH7n/zPpnUPKw963ekx4GtlQBv8EwDmEGCG5TDKZtmMJGz15CiAraRigIoykAoDvhwzcC6UUY6eBZ4BmEwkbMKpRAY02QS8DKgiCNsd4O71+j4Vz6VyKRrJs6UzQCed5kBY5Ca5Sd4F2CKoCqgoA+kw4OtugnPhfEMy5fo7e8A0a0GXu+Qum2maYeIZKl1FGUiXAV93E5yLZ/OYg2etAKYcC3LodMY37AQ8CbBroIrAuQv0f7oM+L6b4BBQEiFBhwNsLnNAcR7AlOxBSkrK0PCXA18CNLhqAagoA24xEIiWgUMGWwhPAEMAhgw/FfgRCIIwxfyJAF2UGdZMFUEQatVb1xAoZeBQyyjBcwAmZaUHH1sIOwA/ylJZKm2AdkBb4DNAvRL9WJPeP+dAKgPSXgugQngA6AfUBtiNyKVzUzK3Ax2OegEMB/89wPDnzwNlARVlIBMMBFYZkCyOI9wBfAuwy8DpRz5cHGzcDnhRVskq6QkcDrwAsFXzFRCGGRIv1keYzikQU4uJVhi9HflwcbahAkDl0A3IZTIWnvufwCSA+SM5MEh7iduAGwCN9Zho7ep26TIQKmXgkPWz/GwHGdnsZp+cyuAigH1zBk4pDmRatsgWmQpwYJD2ERwYpCcmcyZybICtGhVlIJsMhFIZOATvlt02YhIfSIIZjCsC7FKcBlAxcLCuGpCOcJxiETAfmAXQ4/JzgMtPBvjwc4DwCEBFGcgVA6FWBvlJ58M6fQ8YNWgNQGFEZiYnOWgPqBzYzSgD0FuSb3GOQRCcweBbnvEFiJUA3Yo5m7EXwIHN0wG6XxPMnKyiDHiBAVUGcWqByUioIAjaK3Bwjw/4TwCb+Xzwt63YJjtn7JQyl/2lGKggKgGO4qgu1eVYgC0MKoIwu1rHoVpXeYABVQZpVsKoUaOkffv2YoxJsyTdXRnILQOZHynL7fXp0ZUBZSBBBlQZJEiUbqYMBJ0BVQZBr2G9PmUgQQZUGSRIlG6mDASdAVUGQa9hvT5lIEEGVBkkSJRupgwEnQFVBkGvYb0+ZSBBBlQZJEiUbqYMBJ0BVQZBr2G9PmUgQQZUGSRIlG6mDASdAVUGQa9hvT5lIEEGVBkkSJRupgwEnQFVBkGvYb0+ZSBBBlQZJEiUbqYMBJ0BVQZBr2G9PmUgQQZUGSRIlG6mDASdAVUGQa9hvT5lIEEGVBkkSJRupgwEnQFVBkGvYb0+ZSBBBlQZJEiUbqYMBJ0BVQZBr2G9PmUgQQZUGSRIlG6mDASdAVUGQa9hvT5lIEEGVBkkSJRupgwEnQFVBkGvYb0+ZSBBBkokuJ1ulgADO3bskOnTp8uXX34pp556qpx88slSvLjq2wSo0008wIDeqS5Vwtq1a6VWrVqyfPly6dq1q7z99tvSunVr2b17t0tH0GKUgcwyoMrAJX7btWsndevWlW7dusn+++8vDz/8sMyfP1969erl0hG0GGUgswyoMnCJ3xkzZsg111wTKW2vvfaSzp07y8CBA+X333+PLNcvyoBXGVBl4GLNsGUQLXXq1LGKYPz48dGL9bsy4EkGVBm4WC3VqlXLU9qBBx5ofy9cuDDPcv2hDHiRAVUGLtUKuwWlSpXKU1rZsmXt7zVr1uRZrj+UAS8yoMogg7Wya9cuW3rVqlUzeBQtWhlwhwFVBu7wKHzwaWcQLZs3b7Y/jzvuuOjF+l0Z8CQDqgxcrJYVK1bkKW39+vX2tyqDPLToD48yoMrApYopXbq0zJw5M09pc+fOlRNPPFFq1qyZZ7n+UAa8yIAqA5dq5cYbb5RHH31UjDG2xO3bt8u7774rQ4YMUZNklzjWYjLLgPomuMQvFUGJEiWsCXKLFi2EMwi9e/eW+vXru3QELUYZyCwDqgxc4rdYsWLyyCOP2IFEjhVUqVLFpZK1GGUgOwxoN8FlnmlvoIrAZVK1uKwwoMogKzTrQZQB7zOgysD7daRnqAxkhQFVBlmhWQ+iDHifAVUG3q8jPUNlICsMqDLICs16EGXA+wyoMvB+HekZKgNZYUCVQVZo1oMoA95nQJWB9+tIz1AZyAoDqgyyQrMeRBnwPgOqDLxfR3qGykBWGFDfhCRo/vXXX+XTTz/NswcTplAmTpyYZ/nee+8tzZo1y7NMfygDXmagGFxu//K59fJZeuTcGPL8gAMOkG3bthV5RpdccomMHDmyyO10A2XAKwxoNyGJmihXrpxceOGF1lW5qN0uv/zyojbR9cqApxhQZZBkdXTs2FH+/PPPuHtRafzjH/+Iu42uVAa8xoAqgyRr5Nxzz5UKFSoUulfJkiWlffv2wjBoKsqAnxhQZZBkbfFhv/TSS4X/Y8nOnTuFrQcVZcBvDOgAYgo1xrTrhc0U7LfffsKMzJqKPQVidZecMqAtgxToP/300+2sQv5d2Vq44oorVBHkJ0Z/+4IBVQYpVBPjHXbq1KlAV4FdBJ1FSIFQ3cUTDGg3IcVq+Pzzz6VBgwZ59j7kkENk+fLleZbpD2XALwxoyyDFmmII9MMPPzyyN7sInTt3jvzWL8qA3xhQZZBGjXXp0iVigMQuwmWXXZZGabqrMpBbBrSbkAb/CxculGOOOcaWUKtWLVmwYEEapemuykBuGdCWQRr8M4di3bp1bQnaRUiDSN3VEwyo12IC1UC7gcWLF8vq1avth6nTtmzZIsyn6BgfffbZZ3L99dcLvRUrVaok1atXl4MOOsj+P/roo6Vs2bIJHEk3UQZyx4Aqg3zc88H/8MMPZcaMGTJv3jyZP3++rFu3zm7FKUV6LfIhp0kyH3waGfFDxcBuA///8ssvNtfipk2b7H40QDriiCOkTp06NvfiGWecIY0bN7b75zu8/lQGcsZA6McM6MH9ySefyBtvvCHjx4+X7777TpgijanUOWNQu3Zt+xCzS1CtWrXIgGF0jTGmAbfPL3R5XrFihXz77bdWqVCxzJo1S5YtW2Z9F04++WTrBdm2bVs57LDD8u+uv5WBrDIQWmWwaNEiGTx4sLz66qv2Lc6HvU2bNnLmmWdK06ZN4zojpVtDtEWgSfP7778vY8eOFQZNadiwoVx11VXWgnGfffZJ9xC6vzKQNAOhUwbjxo2TJ598Uj744AM59NBD7QN48cUX2xZA0uy5sAOnJKdOnSqvvfaaDYbCLgWtGO+44w6pUaOGC0fQIpSBBBlgpKMwCN7A5qSTTmJUJ9OyZUsDpWB27drlqUtHC8EMGDDAYMDRoKtiMENh0ILx1DnqyQSXAQnupf11Zd9//71p3ry5VQKIUmTmzp3r+UtG8BQzdOhQAxsGg9kKc9dddxmMP3j+vPUE/c1AYJUBmt/mvvvuM6VKlTIY3DMzZ870XU1RKbClgKlKgy6NQdBV312DnrB/GAikMsBovTnllFNMmTJlzH/+8x/Dh8rP8vPPPxsEVDGY2jQYSzB//PGHny9Hz92jDARuAHHatGnCqToa/bz++us5GxhMcMgmqc3+97//yY033ignnHCCvPPOO9a+IakCdGNlIA4DgVIGo0aNkiuvvFJatWolr7zyiqBlEOfS/bmKNgsMtkqDJ+ZqiPac9OcV6Vl7hYHA+CYMHz7cxia87rrrZMSIEYFUBLxp6BBFIymaN5966qnWgMkrN5Oeh78ZCETLgMY7F1xwgdx0003y2GOP+btGEjx7GirRrHnHjh2CwVHtMiTIm25WOAO+Vwb0B2DEoXbt2slLL70k9B8Ii9BhitaSjLBEIyqaUasoA6ky4GtlQOu9Jk2a2Gv/+OOPBdOIqfLg2/3oF0Efh3vuuUfuvfde316HnnjuGfD1mEHfvn0FRkXWlDeMioC3Dx2k+vfvLw8++KA4SWBzf1vpGfiRAd+2DBhbgHEC7r//frnzzjv9yL1r54xpa+sSzTgKHD9RUQZSYcC3yoCzBpxao8sxp9nCLozBwAHFyZMny9lnnx12OvT6U2DAl8pg8+bNUrVqVenXr581wknhul3ZheMUfBMz2tE555wjjRo1cqXcVAtxkrswNoOKMpA0Ax61jIx7Ws8//7xBa8Bs2LAh7naZXIlpTFOxYkXrMwDSrakwlFMmD1lk2S+//LJ1bEJkpiK31Q2UgfwM+HIAkaa4tMLbd999k1Z+buzw5ptv2hRqDG+2dOlS2zTnuXBE/8cff3TjECmVwbgMnFqdMGFCSvvrTuFmwJfKgBZ4p512Ws5qjsencRPn9fnwsY/eoUMHgUOUMDBqroRWibS5YPdFRRlIlgHfKYMlS5bI+vXrI/YFyV6wG9tz9iK/gQ8tICm5aq0410Wbgzlz5jg/9b8ykDADvlMGcOe1F0evxFwJIyTnFwY+pSLgw5hLOfjgg+Wnn37K5SnosX3KgO+UAfvplP33399TlNM5ijYPuQ5myrDtDkeeIkhPxvMM+E4ZeJHRMWPG2DDqN998sxdPT89JGUiIAd8pA775KBw38IIw5PqLL75oP144H7YKHI68cD56Dv5hwHfKoEqVKpbdVatW5ZxluhH36dPHBlIpXbp0zs+HJ7By5UprkOWJk9GT8BUDvlMGTFPG8QJO7+VStm7dan0iEGNRYHwUORW6FdOtOlfy6aef2oQsuTq+Hte/DPjSHLl169Y2zRmNf3IhdJ1G2HXrMci8i47AItLmaaTRj5OQ1VmXjf9UUJzReOGFF2z4t2wcU48RHAZ8mXiVyuBf//qXbNy4MSfz+p06dbJWfrEs/WiDkAtFwFty9OjRjHZtrTODc4vqlWSLAV+2DLziqJStSkr0OOqolChTul0sBnw3ZsCLYDp0RkGmSTBToKuI7Z589NFHcsMNNygdykBKDPiyZcAr1eAmf9c3uwaNGzcWDW7yNyf6LXkGfNky4GVy4K5Hjx7y0EMPCef6wyxIwSZffPGFDX8WZh702tNjwLctA162BkQVG/dQA6Km9xDo3n8x4GtlwEvQUOkaKl0fZncY8G03wbn8mjVrCsN8vfrqq4KkpM7iwP+n9eN5551nw8PT3iK/S3XgCdALdJ0BX9oZ5GehRYsWNoEK5/8ZYOSJJ56wkYjybxeU33RRbtmypfVO1GxKQanV3F9HIJQBaezYsaN9S3LKkX4LYUi8OmPGDDnssMNyfxfpGQSCAd93E6Jr4ZJLLrHh06dMmWIjFX/zzTfRq33/nSnZTzrpJJtuni2Cww8/3PfXpBfgHQYCpQxIa7NmzewIO4OM8MF5+umnZdeuXd5hPIUzWbt2rVx22WXStWtX6d69u0ybNk3dlFPgUXcpgoH84ZKD8hvTjua+++4zSLtmkILM4E3qu0vD+IeBDYGBMZENyQ5fCN9dg56wfxigY0ugBbkYTfPmzQ10ooGnoZk7d67nr5dKYOjQoeaYY46xeRDuuusu8/vvv3v+vPUE/c1A4LoJ+RtCnHqcNGmSjB071g4sMpT4+eefL+PHj5fdu3fn3zynv3/77TcZOHCg1KpVS7p06WKDqy5YsEAeeeQRYRh0FWUgkwz43ugoWXJeeuklueWWW2TTpk12JP6qq64SJh+pXbt2skW5sj2tKKdOnWozSY8cOdLmYeDMCG0matSo4coxtBBlIBEGQqUMduzYYZOvbNu2TdAMl2HDhlljJUYnYguiTZs2cuaZZ0rTpk2tZ6RDIFsQxYu714havny5TJ8+3eZpZIuFBkSM3oTugPzzn//MeYRl57r1f7gYCJUy4IPGty+zHjGdOwW9PBtCjVaM7DowqzOt+TDoKPXr15djjz1W5s2bZx2iqlWrZiMsJXqLoJ8vzKfw7bffyvz58+1n1qxZsmzZMmHMRPoUMGIS4xDwf7169YSp45ilSUUZyDYDoVEG7B5cffXV8tZbb9kHrzCiOY3Htzbn8akEmKqMLQoKH1ImUKHHJGMqMBV8mTJlrILgNmxxML4Cw5/RxZpdEQpbFYzdWKdOHatg+PBTEUSnkmdMR6ZUxwyI9O7d2+6nf5SBbDIQCmXAN3PDhg1t+namcU9UkO3ZNtv5kD788MP2AedDzm7Fli1b7INPBcB+Px9sRzkwrgAVBrM+8cNWSCIDgBw8ZO4FhlOjibWKMpBNBgKvDPimZuAPvsFpvluiRGIW2IwyfOqpp1qDpXPOOcf277NRMVdccYW1ovz888/l0EMPzcYh9RjKgGXAvVExjxJ622232T7666+/nrAioCMQg65yPIHi/M/GJT733HM2O1O7du0i3ZNsHFePoQwEWhmMGzdO/vvf/wqb+4na8bPJf9FFF9nIy7mwQ2B3gi7JjNPACNAqykC2GAisMmCasW7dutnAqXRgSlRog8DZBrpC50o4xvDyyy/b/Acc+FRRBrLBQGCVAR16OD5AR6VEhV6BzzzzjCccm2jzQLsDXgfjG6ooA5lmIJDKgLYE/AwZMsRGDE6ExDlz5tiZg1jbZnPMIPr4ffv2tQZQHD9gwhgVZSCTDAROGfChuemmm+Saa65JeHpu3bp10qpVK8/5KtD46bXXXrNTlzRRzpVSyuQNqGV7h4HAKQOmN6NxUP/+/RNimWMDbdu2tSnevRj3gEZOTJvGgC0PPvhgQtekGykDqTAQKGXAjELsGjAzMg1/EhHmXqCVYS4HDIs6T9pJPPXUU1YZxMrvWNT+ul4ZSISBwBgd8a1OfwIa6nBKMREZPny40MinKDnrrLPsm7mo7TK9ngFfeW2IyZDwVGmmz0nLDw4DgWkZDB482M7N8w2aqDCYKP0Vypcvb3dJ1Dox0fLd3o7XePDBBwsHFDXHpNvsanmBUAYcNKSDDwcOHW/ERKqW5sYvvPCCDTk+ZswYm8qcCoFjDl7MQ0CTahok/fjjj5pgNZEK1m2SYiAQyuCBBx6wD++9996b1MU7GyNOojU/pjchWwk0+KGjkBcVwlFHHWXDwNMYiYpMRRlwjQFMV/laECjEIDaAGTRoUNrXgfgFBlaLkXJgxWjgK2ADq0YWeuTLPffcY68b9hEeOSM9Db8z4PsBRNoTTJ482Y4XlCxZMmUlicCpNpAJp/A4YOh1od8E06vRh4EDivvtt5/XT1nPz+MM+LqbwFTsNCHu06ePpKMIWEc07mEkI+Zd8IMwYArzS+JtZLNJ5cKpyg886TkmzoCvlQGjBh955JEJTQ8WRQmVQYcOHVyNdVjUMdNdz7iJNEhiUhUqRBVlIC0G/NrPQcQhmyAF7slpXwJzKYBEg/iEaZeViwIw5WgwA2IQXDUXh9djBoQB37YMaE9QuXJl66KcljbEzmxuc5S+UaNG6RaVk/0Z6LVz5862hcRpRxVlIBUGfKkMGHWYBjiMF8gow+kIlLqMGDFCLr300nSKyfm+DOLCoKs0SGJcRhVlIFkGfKkMGMKMFnicSUhX6M+wcuVKufzyy9MtKqf7Mxgrw70zDPv111+f03PRg/uTAV8qA8YJpKehG9Np7CIcf/zxctxxx/mzBqPOmi0DJoZ55ZVXbMspapV+VQaKZMB3yoC5DGbPnl1oIJIirzhqA8Y75Gg8050HRVq2bCm0xKRpNnlSUQYSZcB3RkeMV8Dm8OLFixO9xkK3YwalCy64QJYsWWLzLha6oc9W0OaAyWW/+eYbYch1TkGqKANFMeCrlgEH+xjOjPYAbghtC5o0aRIoRUBeaJBE92z6VrDVowZJbtwtwS/DV8qAiU04QOYoA6Y0e//9921UIwYoSeam54j722+/HekipFOWF28TTruyC8TEMak6cNGTU12lvVi7mTknXykDPrx0UT7hhBOEORFr1aolzGjctWtX+2Az8UmiCuHdd9+1U3Dt27dPu6zMVE36pTZo0ECYso2p4ZjQNVFhABWmo2OEZp2mTJS1AGznJ+Op2rVrG+Q1MIhqZBCLwODhj5w+wpYZBCsxCC8eWRbvC250AzdlV8qKdxwvrEMAF1OxYkUDX44iTwctL8MPuhfWKhNJZIvcRzcIBgN0dPGFLF261N6ckyZNMlOnTrXf8XbPc+4IcGLKlStnkBQ1z/L8PxAMxbr/IiZA2mXlL9uLv/F2N2glGEyhGhhsJXSKd999tyqDhJgKzka+6SZMnDjRBh5hABKmVafUrVs3T9uMKc9pnchZgnjCaEEU2iqkW1a843hlHQ2SOH5A46prr73WK6el5+ExBnyjDOiZ17RpU2FUIrouU+hyHC0HHnig/Ukf/3jCWQROve2zzz5plxXvOF5ax1yTnGGgkRWzRqkoA/kZ8I0ymD59eiTWwM8//2ynzagYooVJSylr1qyJXpznOzMso5sRmUVIp6w8BfvgB4Oh3H///XLrrbcKZ2ZUlIFoBnyhDPim5wN+xhln2HN3ohlHXwi/O0lQqlatmn9V5DftFKg0aGxESaesSKE++sJpxubNmwuT0TKTlIoy4DDgC2XAtxi9EzndRTnkkEPsg0/bgGjZvHmz/RnPz4BdBKZcZz+akk5ZtgCf/WHkZ/ovMDIUPTUdBeqzy9DTzQADvlAGTJHOBClOaDPaF1BWrFiRh5L169fb34UpA5odU7FE+yKkWlaeA/vsx7777mtNummohcCqPjt7Pd1MMeAbZXDSSSdFOGDiE7YUZs6cGVnGLwwMSqVRs2bNPMudH2wVMHchm8mOpFqWs79f/9erV08YA4E5KWnMpaIMeN7OAJ6F1iYAgU/zTOjefvvthkZIsDi0yzmXDiVgGMKsMMHUo+nevXuB1amUVaAQny5AlCSDWRWDcZk8V3DddddZOwOGl1MJBwOe91r89ttvbawBet/xbeYIqkdgGGM985jwhAOMbPJfeeWVziZ5/s+fP9/aJTCYCTMpRUuyZUXv6/fvHHc57bTTrNkxu1Aw2LKRomnCTJNv5ndkPspzzjnH75eq518EA55XBjSW4UAXb1Jn0C/6mjgAxrGCKlWqRC8u8L1Xr152nh2WjDZ9WoENsCDRsmLt6+dl9O9AAhk599xzLUd+vhY999QZ8PyYAd/oDFYaSxHwsummW5Qi4HYMlUZvR46mFyaJllXY/n5dzszVHE8hRwMGDPDrZeh5p8mA55WB001I5zrZ/OVMgt/jHKbDQVH7shvw4IMPCsZPhLMMKuFjwPPKgBGN2DJIR2iCe+yxx9qZhnTKCfq+7ErRSpEGSbTMVAkXA4FXBhwHoNVhtG1BuKo48atlF4rBVJn6nV0qNUhKnLsgbOlpZQBfevn111+lRo0aKXNNPwS+5VQZJEZhpUqVrEESg6n27NkzsZ10q0Aw4GllwBBnlMPhcZeqsItAM2ZGSFJJjAFGkmKSmscee8wqhsT20q38zoCnlQH97ynVq1dPiWfOoTN2gbYKkqeP9hpMxnLVVVcJ09WrBJ8BTyuDVatWCZutjmtystUxYcIEofOSE0A12f3Dvj3zWdLPg0FgaOehEmwGPK8MDj744JRrgHPnjIyUassi5QMHZEfGi6DRF12du3XrFpCr0ssojAFPKwMO/MWLTVDYRXE532SMgKxdhHgsFb2OyphKlUqBLQWV4DLgaWVAM+NUswHREw8Rk+Xiiy8Obu1l6crOPvts6du3r9xxxx02D0OWDquHyTIDgVUGfJvR1p7JRFTSZwAh6G3cSOaZYOg4leAx4BlHpWeffdaOWrOf6nw4vcWIx61atYos4zp6HTJCUWHyyy+/2O7Fyy+/rCbIhZGUwvLffvtNGFeCXbcPPvhASpQokUIpuotnGfCKp/bjjz9u/efxsJv8H0Q4MrjxDCzk7AdTjnFPG0E7DGYgisyfELcQXRmTAWTBttwiqGrM9brQvwx4ppvQrl07qzD/+OMPyf9h6nT2/2kue9ZZZxU5O8AuAlOtIaGKZ5WwX0+MuSqee+45efLJJ62Zd6zrQJKaWIt1mccZ8IwyQGq0AklR8nMHnVvkFBcNlRjARGcR8rPn3u+OHTvKjTfeKAwZR6/SaGFSmmOOOUY2bdoUvVi/+4ABzygDcsUHOF4/lMZHTAYaT+iTT0Mlet+pZI6BJ554wipvGiTRsItOTXfeeac1UKJdAjM4q/iLAU8pA3YV2B2IJYyMzPBbhQU5cfZhF4HlcKBRJXMMsD5GjRoldCZjnIgzzzxTMO5jD8ggMawHFZ8x4LXhDgY1BYUxP7NmzYp7ut99953db8qUKXG305XuMTBo0CBToUIFO8AbXW8c8GWCWxX/MOCplgH1KLsKTn4E/naEAU4aNWrk/Iz5n28j5l9s1qxZzPW60F0GoAjkpptusslu87foELVaQ7C7S3fGS/OcMmATn7MH0cJxBIT0jl4U8zuVAZ2Sihf33GXFPF+/Lty6das4g4gcK+CDH0voPq7iHwY8Y3QUTRnjFzixDLicU4r0YMyfdTl6H4ZSb9CggaArUWQLIno//Z4cA2j0WsvOSZMmFbkjxw4Ybl2tQIukyhMbePIVytDoTleBNxSDdcZTBGSSb6FEuhKeYN3HJ0HFPGLECJtPgZcRrxVGxcGpRhV/MOBJZRDdVWATtCj3Wd50vEGpRFQyzwBzNdLUm62Dgw46yIarL+yo2lUojBnvLfdkN4E0sSVAhxiMVFt/euZWLEw+/PBDm679m2++scE4CttOl7vPAMcPevfubd2b2UrIH0SVy9hV2G+//dw/uJboKgOebBnwCp23PMNvxVME3JZvn+OPP14VAcnIstAQjAZIHKthwttY3QaGnlPxPgM5bRmsl/Uyfw9+lB9l9R6skTWyYcYG2XDaBik5p6TsarBL9t6DMlJGKgEH7UF1qS5DTxwqbS5tI/179rdbeZ/2YJ4hZ4H69esnDzzwgL1ATjdSOTCX47Rp02Je9Pbt261JMzNnwU7EDhQj2avww8jYSKgr3IYfjiPR6Iyh3MuXL29bj+ym8HPkkUdaD1d6uaYaAyPmCYZoYVaVAR/86XswQ2bgkV9jqa4sleVogA82H/JqQLnd5WTweYOl1/u9pCSA28Fim2wTqImI4lgpK+X73d9b56a99t5LagGnA2fsQRWJn4MxRHWdtUvlQ925c2f57LPPmOXbzgYxatUBBxxgw9ZPn467AB927+jbwK4FW39sWTCykvOAcxaCDz4VAD9UNo5yoAk0k+1SaXCmadGiRdYakhfJLibd3M84A3cBPlQQKkUzkFFlsFt2y0zgzT1YLsulInAqcBpQH6gD8OGPJazkROIX7pJdsgigspkFfAh8DnD5yUBboB1wBKCSHQaoBOBKLj169LAPMH0Y+PAy1R1niJjolfEpGzdubB9WhrLn8nSE5bOFwWlmOqvNmDFDGIOBuSR5fH6aNm0asyuTznEDsy8qzXX5yfxk/g0cBsCw2BwH3AN8BuwCsiGbzWbzDtAFqAzwPJoBrwN/ACqZZQBu6AZOY+bkk0+2JuI0T+7SpYt55513DN7qmT34ntLR4jBonZh77rnHIMqzPY/DDz/c/Pvf/zYYnM7KOfjpIGzGuSaLzCLTGSgJ8AG8FfgGyLXsNDvNeOBCYC+gCtAP2AKouMsAAtEajBsYZMY2eNObCy+80IwfP95gkNdg5sHdgyVZGmabDIOyoPthMP5g0JUx6F4kWUpwN3dFGSw3y60S4INWE3gJ2AZ4UVaaleYuoDxwAPAYsANQSY8BJKwxyMBkMC5gMLhnEDPRFBWRKr0jpr43xh3MSy+9ZOgUR4VFpbB8+fLUCwzInmkpA75x+wPlgKOAYcCfgB9kvVlv7gbKAMcCHwAqqTGAeIgGWa4NBvvM3XffbRDVOrWCsrwXZjvMsGHDDCxXDaJimf79+xsMUmb5LLxzuJSVwQKzwBwP8GF6ENgO+FGWmCWmNcAxhW7A74BKYgz8/vvvBtGObF8cYebMkiVLEtvRY1th2tI8+OCDVpnBXsUsWLDAY2eYndNJSRm8aF40ZYHGwGIgCPKGecOOc3Cw82tAJT4DX3/9tR2UY//7jTfeiL+xT9YuXrzYYHbDBnx98cUXfXLW7p1mUspgt9ltBwURo9j0BNhNCJJw7ONUgOMJ7wEqsRmYOHGiHRfAXH7g+trsJiAVvY3CzcFG+MbEJiGASxNWBpyOuwxAIHPzKhBU4XVeCXBGZCigkpeBoUOH2pF4mIkbTh8GVTj7wZD9CLYT6OuMrr+ElAFbBJcDfGOGZaDtTnOnKQ6MAlT+YgAxDw3Miw0Cn4aCEg6McmYEMR5D0UJISBnQXoAtgklAmORGc6MpDUwFwi5Tp041MBk2CJEeKirgpm1bCGFIGlOkOfLr8rpcBrwGXAqESTjF0B6gP0WfV/tI8U3FbXZnzKnbUF+MtcAozLSbp/ce3XRpf0/beFi6BSZCM13J6RVKO/+RI0daX4Mw3QcMv8/YnH369LG+E/SLoOs2658fOmM5DlQM08974MADD5QjjjhCKlas6Buq4iqDZbJMTgA6AoOAMMpm2Sz1gOX7Lxd0k6RC+QrWqYY3AD/M/kSPOkyzWTt4vDYtTVxHpxtmIKpXr56ccsop1nuP3nZ+El4Pc1BgpF2++OILG1/CT+fv1rnecMMN8vzzz9u632effazypy8F65mOVrwH6ETFbFLRwWEZCAam0PYeYJ7KZs2aWV8Jt87LzXLiKoPW0loWA3MBuhCHVWbLbGkC/A+4EihMeBMw6SuzOi1dulQWLlwoX331lXWcoVcdA7vSnfeSSy6xgVv9EBsQA4YCnwLrYMSbOazCh50xNhlaD/4VhdJA5UnnKDpN8R748ccfBdOw8uWXX1plypcHvTMvvvhim2+idu3ahZaV9RWFdQCnm+nWEGeimVjYJqFafrW52hwKpGpchZvDDB8+3EAR2HlsWutdc801BjeMZ3mkMQ48/qxhkWdPMosnxilVPKAG7tcpHZW+Gczpccstt1heWRZaCua997wxjV3oACI9/M4BVP5iYJVZZa0tB5lBaVOCN4cZOHCgQX5JOyiHsGGenL5ighQqLbiSp33NQSmgefPm9gFO93roUTlhwgSDYL9WwZx77rk5t9mIqQzofUjz3LFALoVa9Pbbb7cOMF5weqFHZn3ALXGce/jAIUGMQQCQmEWzVcHR/GwLYg6YznDi8YrQ5+H//u//cno6Y8eOtQ+vm96OnMKk0xQGH837779f4PrQ1TDPPPOMda4q7B4psFPUgrffftvQOasoiakMepvepjqQS6ejRx55xCBCjUHyFFO1alU7v82KyKV8aD60SnKemefqadC1ln72yF5sMOYQKRuBRK0ypLJA5qLI8mx8mTdvnr3pESQkG4dL6BhIumtdoxPaOEMb0bkJAXfMvffe6+oR2IVgF5KGTtHdBj4H7Ep8//33hnVRq1YtgwhRCR2bzwvGOWw9IidmkfvEVAZNTBNzLZAroY04A2M4wmAYmKIxbKLlUmh8tR/wJOC2sOWDcF/mggsuiBQ9e/ZsgxQMj5EAAAv9SURBVAFIW5nZVgZPPvmkwVSpZ4xtnnvuOYNoSDlXBqyca6+91jRp0iRST259oekzFQL9PXg/sBuB2QqDyE2RQ2BGw9bLihUrIstifUESIsMPLSg5NpGIMigQHXmH7LAhw5pK06wPZjoHZKw7pklzhNNxF110kXBKJ5dSTIrJKcDHgNvC8G7MRQBtLpMnT7bFc/QersFuHyqh8j7++GM7HcqkKbkWzspwWhOKMtenYo/P0GkMrUZ7EzeFXCPOgp22hBeloFVgpyQ5Ne0IM5EjgIwMGTLEWRTzP0O98YMWZ8z1sRYWUAY/yA9QBzvs3HqsHbKxDM3lPIehYQfnuW+77bY8y3PxgzYHjLWYCUHLx8bog8dcJopPqkzGEoy+CZPa2cWN+WJgXgZGXfaKkBcqgh9++MH1U0JcBRs3EjNPNmAs7VSihcZNnN6k8ZfbUkAZMHw55UDAC8KgqMydgGaZfVByfU4HyAHyC5ApOf/8820gz0yVn2i5tJegJV2uhW9ITMV5ytiJ1oUUcpQJYQuIRmxo/ltr1vzH4PGpiLjeTSmRv7CNstEu2lf2zb8q67/ZXIYtvGDwxB6bigGRabJ+HtEHZFh3h6Po5W59P+SQQ2w4cbfKS7UcWtLl2iiK4dRpqEXrTS8JrQop5CgTwnvAEQweO18j/2n6TuMlKiM3c0QUaBmUk3L2oL/L75GD5+oLm82MwY8IOnLiiScKm07jxo3L1elEeHE4ysSJsD8Y6wbIxLHilckbjm+nXAkTqMAWQxDZOFenUOhxHV7IUSaE94AjscZsnDwTjlJytk33f4GWwX7yV048NoWZucgLwkEQKgKabjLuPpvSuRJ2oxyOMnEOn3zyifVnyETZyZTJNw7m9ZPZxdVt4SUoHECNNv2lSTfNgpmujQ5BZ511lqvHTLQwh5dM5Y/k4K0jjuJxfvM/HaVo0pxunonoMvm9gDI4TA6z2yyUhXIU4BWhswcz7cDmIKenRF4cjtw+EWYdGj16tDz88MNuF510ebCOtL4VSe/o0g7r1q2zWZ6ji6PNP70FMc1qXwy5Ugac3aCQo0wILD/tGBlsPQRTiAUOQWWUicHdAsqAb72aANOf/QPwivDmYNOxRYsWOT0lZojqACQijntrIttyMAjz17afjiCjieyS0W04YJuJEetET5pTrPkFQVXklVdesY5g+ddl8/fMmTPtmznRlkEy9wEdw+ADYRXhu+++a7vF0ftv2rTJppLLxAujwJgBSWX6sylAroRksNL5FnCE86qcXmIarlwJ08MxjRv5iSeclmMzlw9UIsI+4HXXXSdINiK8GTi95IgzSMXmcTaF3pVsliOfQDYP64tjcWCb/MQTGPnI008/beNA0HM1EWGXCM5rcvPNNwvHyziVzvpHwNnI7iNGjBBYYtpUcZGF+AJLXWnZsmWBweek7p9Y1kuTzWRrdpurbEi0NmO4KRgZWXNkZPVN2VMs1vWluqyP6WMOBGKlZ4PGNrQOoz0/6sYG1ES/u8hDoclpzU0xf2zQF86zPTMRwfjKlofpJFs+/RSyIRitNjwmAnpk43AJHeOOO+7IuQUiTcdZv1AIBc4Zb3C7vH379obp5Gg9yG3RkiiwbfQCjAvYIKzcvlu3boZOTI7gxWIQVMYmpXniiSesx2Ose4C5H3isxx9/3O7K9HG0ImUdcnmnTp1i+j04x+H/mObINLs9DLgJyJWQEF4QCfaCUAHQhfl2IFow2GOuuuoq633IysToryWfFUCFVpjQnBSa3wYXZR7AuXPnFrZpzpbTSYwuzFQMKn8xQLNweptG35c0HX7ooYeszwLrnYqA/51PLMXB0ug8hBavQRAcm8QFiWoLpRnd5Lj1QHdztBrMmDFjCi2jqBUxlQF3GgAw/t9SQMWYpwHyAYtvw4qhBq5Ro4atcObtcyo++j+XRwuabLbCmH+Qab0QHs1Q29N70YvCWAuMe4jmrhdPL+vn5PAxYMAAm3mJLTm6HvMFkF8BRN8H6PtHzpWh2OloxJgG9EEgv127djVF+RpECijkC93iWSbLT1UKVQZ8E9YALgXCLhvMBlN5V2XTbmI7Ax8J+yDzYY6u8MK+M6AJ0pIb5hjgDcPP2WefbZWCH964bB2wu5OIo0vQ7xN22dhSYouODzLrPJH7oFevXjbzM+8duilzP3qoMhs0PVPdEAZupedjOlKoMmChjGfAuAZMYx5WoedXrftrmeJV/+r/xXsDxFII3B4GU7YvyGYcZkR8RSWVAF12EabLV+ft5smyT3/99ddHlH8y94DTbWTXom3btuapp57ybObnuMqAhHYHKgJBSaOW7E1y16y7jNwlpuoRVe3NkMyNQOUQa7An2XPI9fYMMsPxkHh92lyfYyaPz3EhDvCyW0ce+EmkRcD65/3C7NR+kCKVwVaz1Ub3OdocbdYCYZJxZpxBw97cB1C+/fZbg/ndyIyBc2PEahE4y4ISMuy+++6zNzbMwcN0C9hmPOMocJaIzXC2lDDtbTjuw/4+67mwMSNnHVsDfpAilQEv4ieAKdcZ8msjEAZhVCMml70KiCWrV682zz77rA24Qu1f2CASvMti7e7LZZw1gT1+wpF2fHmRUSfNAV8qAU7bcWYrv3A2gIODHACEn0BMxcDIRXyB+EESUga8kB+AQ4DaABOUBlneNG/a4KftTLuEksvSxoDjARxggsGQvSmcZiSzFQdFOFLdrl07GyQ1v01EUK7RuQ4YWxn4whh4EJpEFDqnwmfMmGEHiznIyFaB85Jgq8oPkrAy4MWsBOoABwGfAkGUx8xjNsfi9eZ6swtIVjhDwKCW3bt3t33Mzz77LNkiPL09b3oOprGL5Je+cLKEwhnOhqBjDM5UA/HSWKhv374GPgS+yU2ZlDIgqewmtATYl34EoIFSEITjIecDvK7+gBtCwxQ/TB+mcq39+/e3bz54kLo2PZbKebi5D+uLAUj5Rodpr2E3wQ3xqh1J/mtLWhmwACqARwGmLT8N+Brwswwzw0wVgBaGHwMqiTHAUXY2iatUqWIQdCaxnTy6Fbtz8Dewg4GPPvpoHgtDj56y66eVkjJwzuJz87lpDPBtykzN6wE/Cc//dICp19ktCMvgqJt1xLen022gDX10JF83j5OpspiLgRmW2Rpo3Lix787fTV7SUgY8EfarBwMHAEhManoC6wAvyxwzx7QGaFBFZTYbUEmPAYZ158PEgbPWrVubOXPmpFdghvemSXnPnj2t/whiPZrBgweHsjUQTXPaysApbIvZYvoBVAplgC7AJ4BXhDkS2R1gt4ZKoCGQ64xRXuHGzfNg4o6GDRtapcBmN7sPdKLxiiCSlEEiWTsjQiUAt3iDMGNeOb2cnodrysC5CiqFZ4ETAT50nIq8H/gKyLbsMDvMeKAbUBlgd4bThZMAlcwyQFt5TkOy+c1kLHTNpUt2LgbTmIjm/vvvt1OFbLnQPJw2IqoE8t4DcVOyg7i0ZJbMkuHAW8BK4AjgTOD0PeBvN+VP+dMmgPlQ/sJ0mS6bgZOAdgDTqVcDVLLHAMyxbcAWBujANKsNeY6xBTn9dNwF+MCox0ZAdvOMliCALjwD7Wfq1Kk2oC7chG0ino4dOwq6M24eLjBlZVQZOCyxiTAbGAfwMf0UYKIWBlytDdQBGGrtoD3gA1sBKAPsDZQEuP22PdggG2Q1sAZYASwAvgG+B/4AmPPhNICKpzVwCKCSewYYz4/RfPiAIm+gwGNPYKEnTJrDYLeMc8kw4fABsPEuGaqdkaL5gemvMKEKIz7B8s8GBaWigSWo/TAuISNMIfiIDY/HZCN86Kl4GAEIiW0FVqK5J8HDZ5AVZZD/+vlgzwHmAcxORCwGfgb4dk9UykpZqQ4cA9QFqFSY8agWoOJ9BuDrYdOm8SHG1J7Nj8HcGNHh7oq6CnRDBFObNssQjISEn+OPP14wbmEVSFH76/q/GciJMvj78Hm/7ZbdshbgG595G5yWABVEacBpKTDBC1sRFQGV4DHAKMh842PaMtISYDozPvhOS4FxItmCYHYhWEMGj4QcXJGnlEEOrl8PqQwoA3sYUJWqt4IyoAxYBlQZ6I2gDCgDqgz0HlAGlIG/Gfh/zm2ghkDCIq8AAAAASUVORK5CYII=\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.023385999999995022\n",
      "overall guided extraction time took: 0.1330209999999994\n",
      "generated counterexamples were: (format: (counterexample, counterexample generation time))\n",
      "('10', 0.014844000000003632)\n",
      "('10010', 0.0820760000000007)\n"
     ]
    }
   ],
   "source": [
    "dfa = extract(rnn,time_limit = 50,initial_split_depth = 10,starting_examples=starting_examples)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 3.4. Get stats\n",
    "Display the extracted DFA by using the `draw_nicely` function, which has optional parameters `maximum` (default $60$) and `force` (default `False`), and will only draw the DFA if it has less than `maximum` states or `force` is set to `True`.\n",
    "\n",
    "Print some statistics you might find interesting about the network, such as the trained RNN's accuracy against its target, the extracted DFA's accuracy against the RNN, and the extracted DFA's accuracy against the original RNN's target."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAQMAAAGTCAYAAAAst3eIAAAAAXNSR0IArs4c6QAAQABJREFUeAHtXQm8VeP6fkuDJiVDJbNEKjQoyRASN0qKQlSSi7jGkITQ/VPGq3KFuFRoMEQTlYpCKUMSSpqLSlFpkPr+z/Npbfucs88+e1h77zW87/Pb5+y9hm+t9Xxrvesb3qGYMWakqCgDykDoGSgGZWBCz4ISoAwoA1JcOVAGlAFlgAyoMtD7QBlQBiwDqgz0RlAGlIFwKoPdsltaAsU8jBfkBb09lYGsM1Ai60fM8QF7SS/5AHgOqAR4TabKVLkBqA00AVSUgWwxEKrZhJEyUjoALwFdAC8KWy4XAnOBOcBBgIoykA0GQqMM5sk8+6btJt3kP4CX5Tf5TRoD+wLTgNKAijKQaQZCoQx+kV/kJOAwYBJQAvC6fCffWYVwsVwsQwAVZSDTDAR+NmGX7LJdAza/RwF+UASs9GOB4QC7NIMAFWUg0wwEXhn0kB7yMfAWsD/gJ7lALpAHgVuBDwEVZSCTDAS6mzBUhkon4FXgMsCPYsSgo3CxzAA4oHgIoKIMZIKBwCoDPjinAf8C+gN+li2yxQ5+lpJSVimUkTJ+vhw9d48yEEhlsFbWSkOgFjAe2AvwuyyWxXYQlAZTwwAVZcBtBgI3ZrBTdtpmNd+irwNBUASs9KMAXg/xBKCiDLjNQOCUwc1ys3wBvA1wnj5I0kJayMPAncBkQEUZcJOBQHUTaNP/T2A00BYIqlwul8t7AMdFjgBUlAE3GAiMMvhEPpFmAN+aDwFBlm2yTZoCfwLvb35ffl31q6xbt85+Nm3aJFu2bJHff/9dduzYYWlg/Jq99tpLypYtaz8VK1aUAw88UKpUqSKHHHKI8LeKMhAIZbBaVtsBwwbSQN4B6JEYdFkmy+w173vrvrLoqUWRy+UDX758eSlXrpyUKlVKihUrJsWLF5edO3fK1q1b7ee3336T3bt3R/bZf//95eijj5YTTzxRGjZsKE2aNJFatWpF1uuXcDDge2WwQ3bIGcCvwGxgHyAsQr+F5subS/dfu0uvA3sJH+oSJYo2taYi2LBhg/z888+yZMkS+fHHH+W7776TL774QubNm2cVxsEHHyznnXeeXHbZZdKsWTOrUMLCa1iv0/fK4Gq52o4RUBEcA4RNBsgAuQV4F+C0Y7rCFsTs2bNlypQp8uabb8pXX31luxK33HKL/POf/7StjnSPoft7lAEGRPWrDDADTDHgXSDM0sV0MRWB7wG35dtvvzU33nijQdfDYJzBDB061O1DaHkeYUA8ch5Jn8Y0M82UAB4Cwi7bzXbTCKgFbAIyIWvXrjXXXXedwfiDufjiiw0GKPMcZvv27ea9994z/fr1MzNnzjS7du3Ks15/eJ8BX9oZLJflcgnAICD3AGEXxjt4E9gIXAHQn8FtOeCAA+S///2vTJw4UaZNmybnnHOObNu2zR4GisIOOC5fvly6du0qb7/9trRu3TrPIKXb56PlZYAB7+urvGe41Ww19YE6wGYgW8I344QJE1w73Msvv+xaWU5BM8wMUwq4D8ikYJDRVK5c2Vx55ZW2BXDqqacaPPyRQ/7555/msMMOM3fddVdkmX7xPgO+6yZ0NB3NvsAPQLaEN3fz5s0N3oyuHPKDDz4w1atXd6Ws/IUMNoPtOMpb5q38q1z9PXr0aDY/zNNPP23/v/tu3nGb++67z2B608DmwdXjamGZY6DoeagMtEZSLfJxedza5tP5iLb6bgoolunTp8uXX35pDXSOPfZY2xSm4U7Hjh1l8uTJ1lCH8/ZsAlerVs02k9lk/vzzz+0+eFMKHvLIaW3cuFFee+016d69u6BVYaftGjRoIG3btrXz/4MHD5aDDjpIWrVqFdkn3S+0wPwcuBKYBRwHZELatWtnbRKeeeYZW3zdunXzHKZOnTrW8Gn8+PFyySWX5FmnP7zJgG/GDGiLfxfwCEAbfbeld+/e8sMPPwin0Gh0w98UDIzZ+XZ+54N+zDHHSJkyZayVHw11+L1nz56C1oM0bdo00o9GN0A4V3/zzTfLwIED5e6777bbcX7/+OOPl9KlS9uyaAHotnC68QSAYyq0v8iUtGnTRpYuXWqLp3KMFlo4UhYuXBi9WL97mYHMNTrcK5ljA/sBZwGZEBjhGBjsmKlTp0aK79u3b+Q7Wgu2KTxkyJDIsmHDhtmR9Z9++skuc7bBHH1kG7Qo7H6Yr7fLOE1HwUNkoATs90z9WWVWmdLAFUCmhNOMaCkZmDoXOAR5wH1vbrjhhgLrdIE3GfBFy6C8lLcOSDNlpm36uq1c2fTnG79Dhw4yZswYW3yPHj0KHIbbOULLvPnz51v7frYe2MWgLFr0t2kwuwCUCy+80P5n18OR6LKcZW7+d+ImMgdDpmTz5s2FWiZiatEetmrVqpk6vJbrMgO+UAa85r7A2QC9EX8C3BY25ffZZx9h0xeDhfLrrwWb19EPMO396eiDgTJ54oknIrb80Tb/3Ibi/I8+5+iyope78Z1em/8HUCGcDGRKPvroI9lvv/2ED77jFOUci4qCctxxmRmzcI6j/91jwDfKoDhyxDJacDmgHfAH4KbQSYcDgRzs46Bg/fr1rf1+9DGiH2Da9NerV08aNWokvXr1EkylRW9a5PfosorcOIkNvpavkR6mi83KRFPtTMmyZcusufLJJ/+lbFasWJHnUOvXr7e/VRnkocXTP3yjDMgi06GNAXjD3wi4JXyrof8rFSpUkEGDBsm4ceNkzZo19mbnMZwH12n6clmfPn2sJ+AFF1zAn0kZ2LC86LJsAS782SAbpA1A780ngUzJH3/8IZ06dZJDDz1UMLVoB0NhdZjncHPnzrVekDVr1syzXH94lwFfKQPSyLiGjHrMQCb/BdwQDOfIs88+S5sLW1yLFi2sByC9ACnOSPknn3xit6FnH+MFUGFw6oxvQWeKbfXq1ZEuBreh/PLLL/a/84flYeDRegsuXrzYluWsS/U/80NcCjDsG/NDlARiCWc9Jk2aZKc6Y60vahmvidOKfNhHjBhhW0TwXZBHH300wh/HUGB3IBhwjdlFKuoYuj5HDHhzXLPos3rAPGBKAh8B6QrMag0eUHPppZeaUaNGGdzYhkYz0XL22Wfb0fEzzzzToIlsPv74Y2tlhylCc9FFFxmY4hrYEJh9993XvPTSS+aFF16whkWoVtO+fXsza9asSHGctYCrsalUqZI12omsSOPL7eZ2UwaYC+QXvMmt9SRMhQ3GRex1YDo0/2ZF/p4xY4bBQKvBOIHhd0c4G0NrQ7SS7PVgGtW88sorzmr97xMGfGeB6PC62+w2bYAqwAogXYHrrkF3wT7oscriDb9y5co8q9DUz2Nhx21YRiKCAUqDqESJbFrkNsPMMLoj4O+wyLY8j7Fjx5rOnTtbj0MqpZIlS1pFQEV07733RrYt6gsVGQyl7L7wSbCKL9Y+tNR0plpjrddl3mbAt8qAtNJD7zigIbANCKOwJcAWwW0APQffeecdQ/sGmgJHKwB+dz6IgGQeeOCBuHQh2In1QMTAqt0Pg6UGDkhx99GV/mbAV+bIuJnzSAWpYKMgN5JGci3wMhAmQdRDabO9jRw98WhZPXK1VB5T2UYpYrQjjg1QGKwklqCVYBfj9rXjFwsWLJCvv/7aBjZBF0A4OwBnJGs6PWDAAIEzUqxidFmAGPB9pCPWxUTgfIC+C4z6EwZZunKpNO7ZWNa9tU7gyGlnPPhgJyJUBDSV5n8+9I4rMt2U6TtxyimnCMZIpHHjxtbnIpEydRv/M+DrloFD/3lynjWyuUPukOOBs4Cgy2MHPyab+2+Wm4+/WcY+P9b6VfDhLqwlkJ8PWkeee+65NqTZkUceaS0waUSlEmIG/N3LyXv27U1768OwxCzJuyJgv4aYIXbAcKQZGbmyzz77zIYnQ9hz28envwBu65gfKA2Dpn9kX/2iDJAB39kZxNPbL8lLcjBAwxsEBY+3qW/X0S25O9ALYLQnRxjinH175k946623pGXLlraJD6UQMZpytkW92y6C81v/KwNkIFDKAClC7IDiSlkpXYGgyRpZY30z6KNRWKIYdhXoX4FZBRsK/amnnhIn1gDXUeg/4XwPGkd6PakzEChlQBoOB0YCdNbpBwRF6ItBnwx6cL4K0FejKKETEa0DGe78m2++kVtvvVU4SEhlwBkHFWUgmoFAzCZEX5Dz/Sl5Sm4HxgEcYPS7XCPXyAiA3QSaZKcqVASM2sTBwhNOOCHVYnS/ADIQWGXAuuoEMLnIZ0ANwK9CHwzGJWBm6daAijKQCQYCrQy2y3Y5DeBg4qcAjZT8Jh/JRzaOQ2/pLfcBKspAphgItDIgaRxMpEvvKQBzC/gpKaufzz1TN6yWmzkGih6Fytyxs1Iypxo5mMixg8JG4LNyIkkehK2ai4D9gVcAPymxJC9VN/cIA4FXBuSZXYX/AH0Apmz3gzDk+Q8Ag7n4sXvjB471HPMyEJr5pevlevkCYPqxdEfk81Lo/i/OhAwH2Jrx88Cn+8xoiZlkIBQtA4fAgTJQ6gC0UPwNcEuYI8Et+UA+kB4AA5oGYUrULV60nMwzEPgBxPwU0oqvIbAaiCvMKcqo6W3w2TvOlnOwrj0+P8bZJslVHaSDzRyV5G66uTKQFgOh6SY4LFWTanj3fiDzgHgye+Jsebzj4zJ49WCptHelQjd9+dWXZdyScdL3075S82R3gn/SHVtFGcg2A6FrGSRK8BVXXGF9/Z3kKLH2ozUfLfkYEPVf//qXjRQcaztdpgz4gYFQjRkkWiEMBc7ovowCHE+oKJz8AMOHD89I+PN4x9d1yoCbDKgyiMEmQ4kzIxCzJceTV199NeL9x4SqSLUeb3Ndpwx4mgFVBjGq54033rCZkhgarDBh6+H111+PRBaiFyBbByrKgF8ZUGWQr+YYSJSxAIrqIrz33ns2LbuzO/cbPXp0gZyDznr9rwx4nQFVBvlqCMlRbAYkBgiJJ0jJXiAmALMNMTWbijLgRwZUGeSrtQkTJkiNGjXk6KOPzrfm75986Jm63QlH7qxhV4FKQkUZ8CMDqgzy1RqVwT/+8Y98S/P+pCLgmEF+oXJAFiM7+Jh/nf5WBrzOgCqDqBpi0lSGCCtKGTBjc/HisaljdmUGJFVRBvzGQOw72m9X4dL5Tpw4UcqUKSPNmjUrtERmVObUY7yU6kg6Wuj+ukIZ8CoDqgyiaoZdBCoCKoTChDMG8YRWiciybEOWx9tO1ykDXmNAlcGeGmEugSlTpkiLFi3i1hHf+vFaBdyZCmHkyJFxy9GVyoDXGFBlsKdGmHR048aNcsYZZxRaR6tWrbKJSTle4HyKFUMMInyc385/VQaF0qgrPMqAKoM9FfPRRx8JUpPFDR9evXp1a3HIloHzGTFiBNPaR347y+M5OHn0XtDTCjkDqgz23AAffvihNG3atNBZgpDfJ3r5IWBAlUGUMjj99NNDUOV6icpAbAZUGYCXRYsWyU8//SSqDGLfJLo0HAyoMkA9z5o1S0qVKiUNGjQIR63rVSoDMRhQZQBSvvzyS6ldu7ZVCDE40kXKQCgYUGWAav7iiy+kXr16oahwvUhloDAGVBmAGVUGhd0eujxMDIReGSxbtswaG5144olhqne9VmWgAAOhVwb0UqQFoSqDAveGLggZA6FXBj/88INUq1ZNypcvH7Kq18tVBvIyEHplsGTJEjniiCPysqK/lIEQMqDKIIYyoAHStGnTUr4d0t0/5QPrjspAGgyEXhnQE9EJib5u3Trp0aOHHHnkkSlFK0p3/zTqUXdVBtJmIPTKgG7LlStXtkQuXbpUOnXqJNu2Metq8pLu/skfUfdQBtxjIHSJV/NTx0xIjjI46aSTYgY6zb9PYb/T3b+wcnW5MpANBkLdMmDsAaZRq1Sp8CzL2agEPYYy4AUGQq0Mdu7caeugdOnSXqgLPQdlIKcMhFoZsGVA2WuvvXJaCXpwZcALDKgyQC2oMvDCrajnkGsGQq0Mck2+Hl8Z8BIDoVYGTn6ErVu3eqlO9FyUgZwwEGplULJkSeFHlUFO7j09qMcYCLUyYF2ULVtWmFXZERohUbZv3+4sSup/uvsndTDdWBlwkYHQKwPmSvj1118tpUyvdvPNN9vvb7/9trzwwgs2UGqifKe7f6LH0e2UgUwwUAwJQEwmCvZLmY0aNbJRkR977LGUTnnUqFHSvn17m0glpQJ0J2XAIwyEvmVQpUoVWbt2rUeqQ09DGcgdA6oMoAzocqyiDISdgdArA7ovL1++POz3gV6/MiChVwZHHXWU0PWYadRVlIEwMxB6ZcBAJjt27BAGOVFRBsLMQOiVAVsGlMWLF4f5PtBrVwa0m1C1alUbz2DBggV6OygDoWYg9C0D1n7dunXl66+/DvWNoBevDKgy2KMM5s2bp3eDMhBqBlQZ7FEG8+fPVyvCUD8KevGqDHAPNGjQQDZt2iQLFy7UO0IZCC0DqgxQ9cyzuPfee8unn34a2htBL1wZUGWAe4AxDerXrx9RBuvXr5ehQ4dKhw4dZODAgXqXKAOhYCD0eROcWma+xcmTJwtzH8ydO9cupkNn06ZNnU30vzIQaAZCqwwY0IQP/9ixY2XMmDHC1GhsITArsyMMlFqhQgXnp/5XBgLNQCiVAROn1KxZ03orUgE4+ROc/06NM5S6KgOHDf0fdAZCOWbAB3zQoEG2bvMrgPwVrsogPyP6O6gMhFIZsDLbtm0rV199tZQoEb9xpMogqLe+Xld+BkKrDEjE008/LYceemjcJCqqDPLfMvo7qAyEWhkwMvLo0aPj1q0qg7j06MoAMRBqZcB6rFevnvTr10+KFSsWs1pVGcSkRRcGkIHQKwPW6W233SbNmjWLOX6gyiCAd71eUkwGVBmAFrYKhg8fLuXKlcvTQuDgYqlSpWISpwuVgaAxoMpgT41Wq1bNmiBHp5HgmIKKMhAWBlQZRNV0q1at5Prrr4/MLpQvXz5qrX5VBoLNQPxJ9mBfe8yre/zxx2XKlCnWnTn/eMFu2S1rgTXA78A2YA5AGQeU2YNKUkkOAioCKsqAXxgIfXq1WBU19+u50rh+Yzm43sFy/uzzZT6wGPgZ+BPII/zJHK0xGhFlpaxUB44F6uxBfalvf+cpQ38oAx5gQJUBKsEAswG+3T8EPgV2PL1DSkwoIY0nNLaPcU2pad/2fONXAyoAbAnsDSCxO/TBX2BrYQOweg9WykpZAFChLAT+AA4ETgeaAa2BQwAVZSDXDIRaGcySWTIceAvgQ3sEcCbAB5WY/r/p0qVLF9fqaKfslC8AKhxiOrAZOAloB1wJUNGoKAO5YCB0yoB9/WHAs8CXQG3gYqAtcDyQTWErYTJAZUT8BlwIXAc0B1SUgWwyEBplQCUwCHgM2AJ0AK4FTga8IDtkh4wGBgMfAQ2BPsD5gIoykA0GAq8MOB7wPNAbYH/+RuB2YH/AqzJX5sqDwDtAY2AAwK6EijKQSQYCbWfA/nkT4AbgCmAp8DDgZUXAym4AjAE+B0oDbL10B34FVJSBTDEQSGXA1gC7A3yrlgKoFJ4A9gP8JPWknh1kfEVekTeBE4FPABVlIBMMBE4Z8O15AXA38BDAEXvO8ftZOkpH+RrgdXCW41FARRlwm4FAjRmsklVyHsB5fr5J2TIImjwuj8udAAc/BwLFNXdu0Ko4Z9cTGHNkWgjSRmAfgEZDQTXk4eDnkQBbCzSNfh0oAagoA+kyEIiWAc2EmwL0BZgC0Dcg6MLpR7aCOEX6IqCiDKTLgO/HDDhd2BJgc3kiEAZFwEo/DRgFDAXuB1SUgXQZ8L0y6CE9rBMRFcEBQJiESpA2CH2BDwAVZSAdBnzdTaBjEWcORgDtgbAKzak5TsIZh30BFWUgFQZ8qwzo9HMcQLPd14Awy0bZCJ/KmtIF0GnHMN8J6V27b7sJtOFfATwChF3YGrgPYJdhOaCiDKTCgC+VgWNhyLn2w4BcCxO3bt/OCCe5E3o6VgGeBlSUgVQY8KUy4GDZMoDKIJcybtw4adiwobRp00a2bduWy1OxAVa6Slc7u8AulIoykCwDvlQGr8qr1rqQYwa5kuXLl0vdunVtNudcnUP+414lV1lDJJ1ZyM+M/k6EAV8qgxkyI+fBP5ijkZ/DDz88EZ6zsg3OSI4GaJCkogwky4DvlMEv8ouNJUiLQ5WCDJAX9WwsyIsuKZoB3ykDjhVQOJWmUpAB8uJwVHCtLlEGCmfAd8qALQOK32ITFF4F7q5h4Jb1gIoykCwDvlMGjGVIKQeoFGSAvGwFVJSBZBnwnTKoLJXtNdLqTqUgA4zloCbJBXnRJUUz4Dtl4HQP6MuvUpCBdbJOu1AFadElCTDgO2VQQ2rYIKGMa6hSkAHy4vcwbwWvSpdkgwHfKQNGC2a+wpmAF2Tjxr+6K7k2RyYXNNP+GDgFUFEGkmXAd8qAF3g2MBbYBeRKfv75Z3nqqafkzTfftKfQs2dPmTRpUq5Oxx6XxlicbSE/KspAsgz40oX5B/nBWtpRIWjGob+rnC7MjGnAJCwqykCyDPiyZcBxg2bAU4DKXwww6/NI4GpARRlIhQFftgx4ocxifAbAcGfnAmEXKgEmcWXad46rqCgDyTLgW2XAC20NMEQ6m8V7A2GV2TLbppH7n/zPpnUPKw963ekx4GtlQBv8EwDmEGCG5TDKZtmMJGz15CiAraRigIoykAoDvhwzcC6UUY6eBZ4BmEwkbMKpRAY02QS8DKgiCNsd4O71+j4Vz6VyKRrJs6UzQCed5kBY5Ca5Sd4F2CKoCqgoA+kw4OtugnPhfEMy5fo7e8A0a0GXu+Qum2maYeIZKl1FGUiXAV93E5yLZ/OYg2etAKYcC3LodMY37AQ8CbBroIrAuQv0f7oM+L6b4BBQEiFBhwNsLnNAcR7AlOxBSkrK0PCXA18CNLhqAagoA24xEIiWgUMGWwhPAEMAhgw/FfgRCIIwxfyJAF2UGdZMFUEQatVb1xAoZeBQyyjBcwAmZaUHH1sIOwA/ylJZKm2AdkBb4DNAvRL9WJPeP+dAKgPSXgugQngA6AfUBtiNyKVzUzK3Ax2OegEMB/89wPDnzwNlARVlIBMMBFYZkCyOI9wBfAuwy8DpRz5cHGzcDnhRVskq6QkcDrwAsFXzFRCGGRIv1keYzikQU4uJVhi9HflwcbahAkDl0A3IZTIWnvufwCSA+SM5MEh7iduAGwCN9Zho7ep26TIQKmXgkPWz/GwHGdnsZp+cyuAigH1zBk4pDmRatsgWmQpwYJD2ERwYpCcmcyZybICtGhVlIJsMhFIZOATvlt02YhIfSIIZjCsC7FKcBlAxcLCuGpCOcJxiETAfmAXQ4/JzgMtPBvjwc4DwCEBFGcgVA6FWBvlJ58M6fQ8YNWgNQGFEZiYnOWgPqBzYzSgD0FuSb3GOQRCcweBbnvEFiJUA3Yo5m7EXwIHN0wG6XxPMnKyiDHiBAVUGcWqByUioIAjaK3Bwjw/4TwCb+Xzwt63YJjtn7JQyl/2lGKggKgGO4qgu1eVYgC0MKoIwu1rHoVpXeYABVQZpVsKoUaOkffv2YoxJsyTdXRnILQOZHynL7fXp0ZUBZSBBBlQZJEiUbqYMBJ0BVQZBr2G9PmUgQQZUGSRIlG6mDASdAVUGQa9hvT5lIEEGVBkkSJRupgwEnQFVBkGvYb0+ZSBBBlQZJEiUbqYMBJ0BVQZBr2G9PmUgQQZUGSRIlG6mDASdAVUGQa9hvT5lIEEGVBkkSJRupgwEnQFVBkGvYb0+ZSBBBlQZJEiUbqYMBJ0BVQZBr2G9PmUgQQZUGSRIlG6mDASdAVUGQa9hvT5lIEEGVBkkSJRupgwEnQFVBkGvYb0+ZSBBBlQZJEiUbqYMBJ0BVQZBr2G9PmUgQQZUGSRIlG6mDASdAVUGQa9hvT5lIEEGVBkkSJRupgwEnQFVBkGvYb0+ZSBBBkokuJ1ulgADO3bskOnTp8uXX34pp556qpx88slSvLjq2wSo0008wIDeqS5Vwtq1a6VWrVqyfPly6dq1q7z99tvSunVr2b17t0tH0GKUgcwyoMrAJX7btWsndevWlW7dusn+++8vDz/8sMyfP1969erl0hG0GGUgswyoMnCJ3xkzZsg111wTKW2vvfaSzp07y8CBA+X333+PLNcvyoBXGVBl4GLNsGUQLXXq1LGKYPz48dGL9bsy4EkGVBm4WC3VqlXLU9qBBx5ofy9cuDDPcv2hDHiRAVUGLtUKuwWlSpXKU1rZsmXt7zVr1uRZrj+UAS8yoMogg7Wya9cuW3rVqlUzeBQtWhlwhwFVBu7wKHzwaWcQLZs3b7Y/jzvuuOjF+l0Z8CQDqgxcrJYVK1bkKW39+vX2tyqDPLToD48yoMrApYopXbq0zJw5M09pc+fOlRNPPFFq1qyZZ7n+UAa8yIAqA5dq5cYbb5RHH31UjDG2xO3bt8u7774rQ4YMUZNklzjWYjLLgPomuMQvFUGJEiWsCXKLFi2EMwi9e/eW+vXru3QELUYZyCwDqgxc4rdYsWLyyCOP2IFEjhVUqVLFpZK1GGUgOwxoN8FlnmlvoIrAZVK1uKwwoMogKzTrQZQB7zOgysD7daRnqAxkhQFVBlmhWQ+iDHifAVUG3q8jPUNlICsMqDLICs16EGXA+wyoMvB+HekZKgNZYUCVQVZo1oMoA95nQJWB9+tIz1AZyAoDqgyyQrMeRBnwPgOqDLxfR3qGykBWGFDfhCRo/vXXX+XTTz/NswcTplAmTpyYZ/nee+8tzZo1y7NMfygDXmagGFxu//K59fJZeuTcGPL8gAMOkG3bthV5RpdccomMHDmyyO10A2XAKwxoNyGJmihXrpxceOGF1lW5qN0uv/zyojbR9cqApxhQZZBkdXTs2FH+/PPPuHtRafzjH/+Iu42uVAa8xoAqgyRr5Nxzz5UKFSoUulfJkiWlffv2wjBoKsqAnxhQZZBkbfFhv/TSS4X/Y8nOnTuFrQcVZcBvDOgAYgo1xrTrhc0U7LfffsKMzJqKPQVidZecMqAtgxToP/300+2sQv5d2Vq44oorVBHkJ0Z/+4IBVQYpVBPjHXbq1KlAV4FdBJ1FSIFQ3cUTDGg3IcVq+Pzzz6VBgwZ59j7kkENk+fLleZbpD2XALwxoyyDFmmII9MMPPzyyN7sInTt3jvzWL8qA3xhQZZBGjXXp0iVigMQuwmWXXZZGabqrMpBbBrSbkAb/CxculGOOOcaWUKtWLVmwYEEapemuykBuGdCWQRr8M4di3bp1bQnaRUiDSN3VEwyo12IC1UC7gcWLF8vq1avth6nTtmzZIsyn6BgfffbZZ3L99dcLvRUrVaok1atXl4MOOsj+P/roo6Vs2bIJHEk3UQZyx4Aqg3zc88H/8MMPZcaMGTJv3jyZP3++rFu3zm7FKUV6LfIhp0kyH3waGfFDxcBuA///8ssvNtfipk2b7H40QDriiCOkTp06NvfiGWecIY0bN7b75zu8/lQGcsZA6McM6MH9ySefyBtvvCHjx4+X7777TpgijanUOWNQu3Zt+xCzS1CtWrXIgGF0jTGmAbfPL3R5XrFihXz77bdWqVCxzJo1S5YtW2Z9F04++WTrBdm2bVs57LDD8u+uv5WBrDIQWmWwaNEiGTx4sLz66qv2Lc6HvU2bNnLmmWdK06ZN4zojpVtDtEWgSfP7778vY8eOFQZNadiwoVx11VXWgnGfffZJ9xC6vzKQNAOhUwbjxo2TJ598Uj744AM59NBD7QN48cUX2xZA0uy5sAOnJKdOnSqvvfaaDYbCLgWtGO+44w6pUaOGC0fQIpSBBBlgpKMwCN7A5qSTTmJUJ9OyZUsDpWB27drlqUtHC8EMGDDAYMDRoKtiMENh0ILx1DnqyQSXAQnupf11Zd9//71p3ry5VQKIUmTmzp3r+UtG8BQzdOhQAxsGg9kKc9dddxmMP3j+vPUE/c1AYJUBmt/mvvvuM6VKlTIY3DMzZ870XU1RKbClgKlKgy6NQdBV312DnrB/GAikMsBovTnllFNMmTJlzH/+8x/Dh8rP8vPPPxsEVDGY2jQYSzB//PGHny9Hz92jDARuAHHatGnCqToa/bz++us5GxhMcMgmqc3+97//yY033ignnHCCvPPOO9a+IakCdGNlIA4DgVIGo0aNkiuvvFJatWolr7zyiqBlEOfS/bmKNgsMtkqDJ+ZqiPac9OcV6Vl7hYHA+CYMHz7cxia87rrrZMSIEYFUBLxp6BBFIymaN5966qnWgMkrN5Oeh78ZCETLgMY7F1xwgdx0003y2GOP+btGEjx7GirRrHnHjh2CwVHtMiTIm25WOAO+Vwb0B2DEoXbt2slLL70k9B8Ii9BhitaSjLBEIyqaUasoA6ky4GtlQOu9Jk2a2Gv/+OOPBdOIqfLg2/3oF0Efh3vuuUfuvfde316HnnjuGfD1mEHfvn0FRkXWlDeMioC3Dx2k+vfvLw8++KA4SWBzf1vpGfiRAd+2DBhbgHEC7r//frnzzjv9yL1r54xpa+sSzTgKHD9RUQZSYcC3yoCzBpxao8sxp9nCLozBwAHFyZMny9lnnx12OvT6U2DAl8pg8+bNUrVqVenXr581wknhul3ZheMUfBMz2tE555wjjRo1cqXcVAtxkrswNoOKMpA0Ax61jIx7Ws8//7xBa8Bs2LAh7naZXIlpTFOxYkXrMwDSrakwlFMmD1lk2S+//LJ1bEJkpiK31Q2UgfwM+HIAkaa4tMLbd999k1Z+buzw5ptv2hRqDG+2dOlS2zTnuXBE/8cff3TjECmVwbgMnFqdMGFCSvvrTuFmwJfKgBZ4p512Ws5qjsencRPn9fnwsY/eoUMHgUOUMDBqroRWibS5YPdFRRlIlgHfKYMlS5bI+vXrI/YFyV6wG9tz9iK/gQ8tICm5aq0410Wbgzlz5jg/9b8ykDADvlMGcOe1F0evxFwJIyTnFwY+pSLgw5hLOfjgg+Wnn37K5SnosX3KgO+UAfvplP33399TlNM5ijYPuQ5myrDtDkeeIkhPxvMM+E4ZeJHRMWPG2DDqN998sxdPT89JGUiIAd8pA775KBw38IIw5PqLL75oP144H7YKHI68cD56Dv5hwHfKoEqVKpbdVatW5ZxluhH36dPHBlIpXbp0zs+HJ7By5UprkOWJk9GT8BUDvlMGTFPG8QJO7+VStm7dan0iEGNRYHwUORW6FdOtOlfy6aef2oQsuTq+Hte/DPjSHLl169Y2zRmNf3IhdJ1G2HXrMci8i47AItLmaaTRj5OQ1VmXjf9UUJzReOGFF2z4t2wcU48RHAZ8mXiVyuBf//qXbNy4MSfz+p06dbJWfrEs/WiDkAtFwFty9OjRjHZtrTODc4vqlWSLAV+2DLziqJStSkr0OOqolChTul0sBnw3ZsCLYDp0RkGmSTBToKuI7Z589NFHcsMNNygdykBKDPiyZcAr1eAmf9c3uwaNGzcWDW7yNyf6LXkGfNky4GVy4K5Hjx7y0EMPCef6wyxIwSZffPGFDX8WZh702tNjwLctA162BkQVG/dQA6Km9xDo3n8x4GtlwEvQUOkaKl0fZncY8G03wbn8mjVrCsN8vfrqq4KkpM7iwP+n9eN5551nw8PT3iK/S3XgCdALdJ0BX9oZ5GehRYsWNoEK5/8ZYOSJJ56wkYjybxeU33RRbtmypfVO1GxKQanV3F9HIJQBaezYsaN9S3LKkX4LYUi8OmPGDDnssMNyfxfpGQSCAd93E6Jr4ZJLLrHh06dMmWIjFX/zzTfRq33/nSnZTzrpJJtuni2Cww8/3PfXpBfgHQYCpQxIa7NmzewIO4OM8MF5+umnZdeuXd5hPIUzWbt2rVx22WXStWtX6d69u0ybNk3dlFPgUXcpgoH84ZKD8hvTjua+++4zSLtmkILM4E3qu0vD+IeBDYGBMZENyQ5fCN9dg56wfxigY0ugBbkYTfPmzQ10ooGnoZk7d67nr5dKYOjQoeaYY46xeRDuuusu8/vvv3v+vPUE/c1A4LoJ+RtCnHqcNGmSjB071g4sMpT4+eefL+PHj5fdu3fn3zynv3/77TcZOHCg1KpVS7p06WKDqy5YsEAeeeQRYRh0FWUgkwz43ugoWXJeeuklueWWW2TTpk12JP6qq64SJh+pXbt2skW5sj2tKKdOnWozSY8cOdLmYeDMCG0matSo4coxtBBlIBEGQqUMduzYYZOvbNu2TdAMl2HDhlljJUYnYguiTZs2cuaZZ0rTpk2tZ6RDIFsQxYu714havny5TJ8+3eZpZIuFBkSM3oTugPzzn//MeYRl57r1f7gYCJUy4IPGty+zHjGdOwW9PBtCjVaM7DowqzOt+TDoKPXr15djjz1W5s2bZx2iqlWrZiMsJXqLoJ8vzKfw7bffyvz58+1n1qxZsmzZMmHMRPoUMGIS4xDwf7169YSp45ilSUUZyDYDoVEG7B5cffXV8tZbb9kHrzCiOY3Htzbn8akEmKqMLQoKH1ImUKHHJGMqMBV8mTJlrILgNmxxML4Cw5/RxZpdEQpbFYzdWKdOHatg+PBTEUSnkmdMR6ZUxwyI9O7d2+6nf5SBbDIQCmXAN3PDhg1t+namcU9UkO3ZNtv5kD788MP2AedDzm7Fli1b7INPBcB+Px9sRzkwrgAVBrM+8cNWSCIDgBw8ZO4FhlOjibWKMpBNBgKvDPimZuAPvsFpvluiRGIW2IwyfOqpp1qDpXPOOcf277NRMVdccYW1ovz888/l0EMPzcYh9RjKgGXAvVExjxJ622232T7666+/nrAioCMQg65yPIHi/M/GJT733HM2O1O7du0i3ZNsHFePoQwEWhmMGzdO/vvf/wqb+4na8bPJf9FFF9nIy7mwQ2B3gi7JjNPACNAqykC2GAisMmCasW7dutnAqXRgSlRog8DZBrpC50o4xvDyyy/b/Acc+FRRBrLBQGCVAR16OD5AR6VEhV6BzzzzjCccm2jzQLsDXgfjG6ooA5lmIJDKgLYE/AwZMsRGDE6ExDlz5tiZg1jbZnPMIPr4ffv2tQZQHD9gwhgVZSCTDAROGfChuemmm+Saa65JeHpu3bp10qpVK8/5KtD46bXXXrNTlzRRzpVSyuQNqGV7h4HAKQOmN6NxUP/+/RNimWMDbdu2tSnevRj3gEZOTJvGgC0PPvhgQtekGykDqTAQKGXAjELsGjAzMg1/EhHmXqCVYS4HDIs6T9pJPPXUU1YZxMrvWNT+ul4ZSISBwBgd8a1OfwIa6nBKMREZPny40MinKDnrrLPsm7mo7TK9ngFfeW2IyZDwVGmmz0nLDw4DgWkZDB482M7N8w2aqDCYKP0Vypcvb3dJ1Dox0fLd3o7XePDBBwsHFDXHpNvsanmBUAYcNKSDDwcOHW/ERKqW5sYvvPCCDTk+ZswYm8qcCoFjDl7MQ0CTahok/fjjj5pgNZEK1m2SYiAQyuCBBx6wD++9996b1MU7GyNOojU/pjchWwk0+KGjkBcVwlFHHWXDwNMYiYpMRRlwjQFMV/laECjEIDaAGTRoUNrXgfgFBlaLkXJgxWjgK2ADq0YWeuTLPffcY68b9hEeOSM9Db8z4PsBRNoTTJ482Y4XlCxZMmUlicCpNpAJp/A4YOh1od8E06vRh4EDivvtt5/XT1nPz+MM+LqbwFTsNCHu06ePpKMIWEc07mEkI+Zd8IMwYArzS+JtZLNJ5cKpyg886TkmzoCvlQGjBh955JEJTQ8WRQmVQYcOHVyNdVjUMdNdz7iJNEhiUhUqRBVlIC0G/NrPQcQhmyAF7slpXwJzKYBEg/iEaZeViwIw5WgwA2IQXDUXh9djBoQB37YMaE9QuXJl66KcljbEzmxuc5S+UaNG6RaVk/0Z6LVz5862hcRpRxVlIBUGfKkMGHWYBjiMF8gow+kIlLqMGDFCLr300nSKyfm+DOLCoKs0SGJcRhVlIFkGfKkMGMKMFnicSUhX6M+wcuVKufzyy9MtKqf7Mxgrw70zDPv111+f03PRg/uTAV8qA8YJpKehG9Np7CIcf/zxctxxx/mzBqPOmi0DJoZ55ZVXbMspapV+VQaKZMB3yoC5DGbPnl1oIJIirzhqA8Y75Gg8050HRVq2bCm0xKRpNnlSUQYSZcB3RkeMV8Dm8OLFixO9xkK3YwalCy64QJYsWWLzLha6oc9W0OaAyWW/+eYbYch1TkGqKANFMeCrlgEH+xjOjPYAbghtC5o0aRIoRUBeaJBE92z6VrDVowZJbtwtwS/DV8qAiU04QOYoA6Y0e//9921UIwYoSeam54j722+/HekipFOWF28TTruyC8TEMak6cNGTU12lvVi7mTknXykDPrx0UT7hhBOEORFr1aolzGjctWtX+2Az8UmiCuHdd9+1U3Dt27dPu6zMVE36pTZo0ECYso2p4ZjQNVFhABWmo2OEZp2mTJS1AGznJ+Op2rVrG+Q1MIhqZBCLwODhj5w+wpYZBCsxCC8eWRbvC250AzdlV8qKdxwvrEMAF1OxYkUDX44iTwctL8MPuhfWKhNJZIvcRzcIBgN0dPGFLF261N6ckyZNMlOnTrXf8XbPc+4IcGLKlStnkBQ1z/L8PxAMxbr/IiZA2mXlL9uLv/F2N2glGEyhGhhsJXSKd999tyqDhJgKzka+6SZMnDjRBh5hABKmVafUrVs3T9uMKc9pnchZgnjCaEEU2iqkW1a843hlHQ2SOH5A46prr73WK6el5+ExBnyjDOiZ17RpU2FUIrouU+hyHC0HHnig/Ukf/3jCWQROve2zzz5plxXvOF5ax1yTnGGgkRWzRqkoA/kZ8I0ymD59eiTWwM8//2ynzagYooVJSylr1qyJXpznOzMso5sRmUVIp6w8BfvgB4Oh3H///XLrrbcKZ2ZUlIFoBnyhDPim5wN+xhln2HN3ohlHXwi/O0lQqlatmn9V5DftFKg0aGxESaesSKE++sJpxubNmwuT0TKTlIoy4DDgC2XAtxi9EzndRTnkkEPsg0/bgGjZvHmz/RnPz4BdBKZcZz+akk5ZtgCf/WHkZ/ovMDIUPTUdBeqzy9DTzQADvlAGTJHOBClOaDPaF1BWrFiRh5L169fb34UpA5odU7FE+yKkWlaeA/vsx7777mtNummohcCqPjt7Pd1MMeAbZXDSSSdFOGDiE7YUZs6cGVnGLwwMSqVRs2bNPMudH2wVMHchm8mOpFqWs79f/9erV08YA4E5KWnMpaIMeN7OAJ6F1iYAgU/zTOjefvvthkZIsDi0yzmXDiVgGMKsMMHUo+nevXuB1amUVaAQny5AlCSDWRWDcZk8V3DddddZOwOGl1MJBwOe91r89ttvbawBet/xbeYIqkdgGGM985jwhAOMbPJfeeWVziZ5/s+fP9/aJTCYCTMpRUuyZUXv6/fvHHc57bTTrNkxu1Aw2LKRomnCTJNv5ndkPspzzjnH75eq518EA55XBjSW4UAXb1Jn0C/6mjgAxrGCKlWqRC8u8L1Xr152nh2WjDZ9WoENsCDRsmLt6+dl9O9AAhk599xzLUd+vhY999QZ8PyYAd/oDFYaSxHwsummW5Qi4HYMlUZvR46mFyaJllXY/n5dzszVHE8hRwMGDPDrZeh5p8mA55WB001I5zrZ/OVMgt/jHKbDQVH7shvw4IMPCsZPhLMMKuFjwPPKgBGN2DJIR2iCe+yxx9qZhnTKCfq+7ErRSpEGSbTMVAkXA4FXBhwHoNVhtG1BuKo48atlF4rBVJn6nV0qNUhKnLsgbOlpZQBfevn111+lRo0aKXNNPwS+5VQZJEZhpUqVrEESg6n27NkzsZ10q0Aw4GllwBBnlMPhcZeqsItAM2ZGSFJJjAFGkmKSmscee8wqhsT20q38zoCnlQH97ynVq1dPiWfOoTN2gbYKkqeP9hpMxnLVVVcJ09WrBJ8BTyuDVatWCZutjmtystUxYcIEofOSE0A12f3Dvj3zWdLPg0FgaOehEmwGPK8MDj744JRrgHPnjIyUassi5QMHZEfGi6DRF12du3XrFpCr0ssojAFPKwMO/MWLTVDYRXE532SMgKxdhHgsFb2OyphKlUqBLQWV4DLgaWVAM+NUswHREw8Rk+Xiiy8Obu1l6crOPvts6du3r9xxxx02D0OWDquHyTIDgVUGfJvR1p7JRFTSZwAh6G3cSOaZYOg4leAx4BlHpWeffdaOWrOf6nw4vcWIx61atYos4zp6HTJCUWHyyy+/2O7Fyy+/rCbIhZGUwvLffvtNGFeCXbcPPvhASpQokUIpuotnGfCKp/bjjz9u/efxsJv8H0Q4MrjxDCzk7AdTjnFPG0E7DGYgisyfELcQXRmTAWTBttwiqGrM9brQvwx4ppvQrl07qzD/+OMPyf9h6nT2/2kue9ZZZxU5O8AuAlOtIaGKZ5WwX0+MuSqee+45efLJJ62Zd6zrQJKaWIt1mccZ8IwyQGq0AklR8nMHnVvkFBcNlRjARGcR8rPn3u+OHTvKjTfeKAwZR6/SaGFSmmOOOUY2bdoUvVi/+4ABzygDcsUHOF4/lMZHTAYaT+iTT0Mlet+pZI6BJ554wipvGiTRsItOTXfeeac1UKJdAjM4q/iLAU8pA3YV2B2IJYyMzPBbhQU5cfZhF4HlcKBRJXMMsD5GjRoldCZjnIgzzzxTMO5jD8ggMawHFZ8x4LXhDgY1BYUxP7NmzYp7ut99953db8qUKXG305XuMTBo0CBToUIFO8AbXW8c8GWCWxX/MOCplgH1KLsKTn4E/naEAU4aNWrk/Iz5n28j5l9s1qxZzPW60F0GoAjkpptusslu87foELVaQ7C7S3fGS/OcMmATn7MH0cJxBIT0jl4U8zuVAZ2Sihf33GXFPF+/Lty6das4g4gcK+CDH0voPq7iHwY8Y3QUTRnjFzixDLicU4r0YMyfdTl6H4ZSb9CggaArUWQLIno//Z4cA2j0WsvOSZMmFbkjxw4Ybl2tQIukyhMbePIVytDoTleBNxSDdcZTBGSSb6FEuhKeYN3HJ0HFPGLECJtPgZcRrxVGxcGpRhV/MOBJZRDdVWATtCj3Wd50vEGpRFQyzwBzNdLUm62Dgw46yIarL+yo2lUojBnvLfdkN4E0sSVAhxiMVFt/euZWLEw+/PBDm679m2++scE4CttOl7vPAMcPevfubd2b2UrIH0SVy9hV2G+//dw/uJboKgOebBnwCp23PMNvxVME3JZvn+OPP14VAcnIstAQjAZIHKthwttY3QaGnlPxPgM5bRmsl/Uyfw9+lB9l9R6skTWyYcYG2XDaBik5p6TsarBL9t6DMlJGKgEH7UF1qS5DTxwqbS5tI/179rdbeZ/2YJ4hZ4H69esnDzzwgL1ATjdSOTCX47Rp02Je9Pbt261JMzNnwU7EDhQj2avww8jYSKgr3IYfjiPR6Iyh3MuXL29bj+ym8HPkkUdaD1d6uaYaAyPmCYZoYVaVAR/86XswQ2bgkV9jqa4sleVogA82H/JqQLnd5WTweYOl1/u9pCSA28Fim2wTqImI4lgpK+X73d9b56a99t5LagGnA2fsQRWJn4MxRHWdtUvlQ925c2f57LPPmOXbzgYxatUBBxxgw9ZPn467AB927+jbwK4FW39sWTCykvOAcxaCDz4VAD9UNo5yoAk0k+1SaXCmadGiRdYakhfJLibd3M84A3cBPlQQKkUzkFFlsFt2y0zgzT1YLsulInAqcBpQH6gD8OGPJazkROIX7pJdsgigspkFfAh8DnD5yUBboB1wBKCSHQaoBOBKLj169LAPMH0Y+PAy1R1niJjolfEpGzdubB9WhrLn8nSE5bOFwWlmOqvNmDFDGIOBuSR5fH6aNm0asyuTznEDsy8qzXX5yfxk/g0cBsCw2BwH3AN8BuwCsiGbzWbzDtAFqAzwPJoBrwN/ACqZZQBu6AZOY+bkk0+2JuI0T+7SpYt55513DN7qmT34ntLR4jBonZh77rnHIMqzPY/DDz/c/Pvf/zYYnM7KOfjpIGzGuSaLzCLTGSgJ8AG8FfgGyLXsNDvNeOBCYC+gCtAP2AKouMsAAtEajBsYZMY2eNObCy+80IwfP95gkNdg5sHdgyVZGmabDIOyoPthMP5g0JUx6F4kWUpwN3dFGSw3y60S4INWE3gJ2AZ4UVaaleYuoDxwAPAYsANQSY8BJKwxyMBkMC5gMLhnEDPRFBWRKr0jpr43xh3MSy+9ZOgUR4VFpbB8+fLUCwzInmkpA75x+wPlgKOAYcCfgB9kvVlv7gbKAMcCHwAqqTGAeIgGWa4NBvvM3XffbRDVOrWCsrwXZjvMsGHDDCxXDaJimf79+xsMUmb5LLxzuJSVwQKzwBwP8GF6ENgO+FGWmCWmNcAxhW7A74BKYgz8/vvvBtGObF8cYebMkiVLEtvRY1th2tI8+OCDVpnBXsUsWLDAY2eYndNJSRm8aF40ZYHGwGIgCPKGecOOc3Cw82tAJT4DX3/9tR2UY//7jTfeiL+xT9YuXrzYYHbDBnx98cUXfXLW7p1mUspgt9ltBwURo9j0BNhNCJJw7ONUgOMJ7wEqsRmYOHGiHRfAXH7g+trsJiAVvY3CzcFG+MbEJiGASxNWBpyOuwxAIHPzKhBU4XVeCXBGZCigkpeBoUOH2pF4mIkbTh8GVTj7wZD9CLYT6OuMrr+ElAFbBJcDfGOGZaDtTnOnKQ6MAlT+YgAxDw3Miw0Cn4aCEg6McmYEMR5D0UJISBnQXoAtgklAmORGc6MpDUwFwi5Tp041MBk2CJEeKirgpm1bCGFIGlOkOfLr8rpcBrwGXAqESTjF0B6gP0WfV/tI8U3FbXZnzKnbUF+MtcAozLSbp/ce3XRpf0/beFi6BSZCM13J6RVKO/+RI0daX4Mw3QcMv8/YnH369LG+E/SLoOs2658fOmM5DlQM08974MADD5QjjjhCKlas6Buq4iqDZbJMTgA6AoOAMMpm2Sz1gOX7Lxd0k6RC+QrWqYY3AD/M/kSPOkyzWTt4vDYtTVxHpxtmIKpXr56ccsop1nuP3nZ+El4Pc1BgpF2++OILG1/CT+fv1rnecMMN8vzzz9u632effazypy8F65mOVrwH6ETFbFLRwWEZCAam0PYeYJ7KZs2aWV8Jt87LzXLiKoPW0loWA3MBuhCHVWbLbGkC/A+4EihMeBMw6SuzOi1dulQWLlwoX331lXWcoVcdA7vSnfeSSy6xgVv9EBsQA4YCnwLrYMSbOazCh50xNhlaD/4VhdJA5UnnKDpN8R748ccfBdOw8uWXX1plypcHvTMvvvhim2+idu3ahZaV9RWFdQCnm+nWEGeimVjYJqFafrW52hwKpGpchZvDDB8+3EAR2HlsWutdc801BjeMZ3mkMQ48/qxhkWdPMosnxilVPKAG7tcpHZW+Gczpccstt1heWRZaCua997wxjV3oACI9/M4BVP5iYJVZZa0tB5lBaVOCN4cZOHCgQX5JOyiHsGGenL5ighQqLbiSp33NQSmgefPm9gFO93roUTlhwgSDYL9WwZx77rk5t9mIqQzofUjz3LFALoVa9Pbbb7cOMF5weqFHZn3ALXGce/jAIUGMQQCQmEWzVcHR/GwLYg6YznDi8YrQ5+H//u//cno6Y8eOtQ+vm96OnMKk0xQGH837779f4PrQ1TDPPPOMda4q7B4psFPUgrffftvQOasoiakMepvepjqQS6ejRx55xCBCjUHyFFO1alU7v82KyKV8aD60SnKemefqadC1ln72yF5sMOYQKRuBRK0ypLJA5qLI8mx8mTdvnr3pESQkG4dL6BhIumtdoxPaOEMb0bkJAXfMvffe6+oR2IVgF5KGTtHdBj4H7Ep8//33hnVRq1YtgwhRCR2bzwvGOWw9IidmkfvEVAZNTBNzLZAroY04A2M4wmAYmKIxbKLlUmh8tR/wJOC2sOWDcF/mggsuiBQ9e/ZsgxQMj5EAAAv9SURBVAFIW5nZVgZPPvmkwVSpZ4xtnnvuOYNoSDlXBqyca6+91jRp0iRST259oekzFQL9PXg/sBuB2QqDyE2RQ2BGw9bLihUrIstifUESIsMPLSg5NpGIMigQHXmH7LAhw5pK06wPZjoHZKw7pklzhNNxF110kXBKJ5dSTIrJKcDHgNvC8G7MRQBtLpMnT7bFc/QersFuHyqh8j7++GM7HcqkKbkWzspwWhOKMtenYo/P0GkMrUZ7EzeFXCPOgp22hBeloFVgpyQ5Ne0IM5EjgIwMGTLEWRTzP0O98YMWZ8z1sRYWUAY/yA9QBzvs3HqsHbKxDM3lPIehYQfnuW+77bY8y3PxgzYHjLWYCUHLx8bog8dcJopPqkzGEoy+CZPa2cWN+WJgXgZGXfaKkBcqgh9++MH1U0JcBRs3EjNPNmAs7VSihcZNnN6k8ZfbUkAZMHw55UDAC8KgqMydgGaZfVByfU4HyAHyC5ApOf/8820gz0yVn2i5tJegJV2uhW9ITMV5ytiJ1oUUcpQJYQuIRmxo/ltr1vzH4PGpiLjeTSmRv7CNstEu2lf2zb8q67/ZXIYtvGDwxB6bigGRabJ+HtEHZFh3h6Po5W59P+SQQ2w4cbfKS7UcWtLl2iiK4dRpqEXrTS8JrQop5CgTwnvAEQweO18j/2n6TuMlKiM3c0QUaBmUk3L2oL/L75GD5+oLm82MwY8IOnLiiScKm07jxo3L1elEeHE4ysSJsD8Y6wbIxLHilckbjm+nXAkTqMAWQxDZOFenUOhxHV7IUSaE94AjscZsnDwTjlJytk33f4GWwX7yV048NoWZucgLwkEQKgKabjLuPpvSuRJ2oxyOMnEOn3zyifVnyETZyZTJNw7m9ZPZxdVt4SUoHECNNv2lSTfNgpmujQ5BZ511lqvHTLQwh5dM5Y/k4K0jjuJxfvM/HaVo0pxunonoMvm9gDI4TA6z2yyUhXIU4BWhswcz7cDmIKenRF4cjtw+EWYdGj16tDz88MNuF510ebCOtL4VSe/o0g7r1q2zWZ6ji6PNP70FMc1qXwy5Ugac3aCQo0wILD/tGBlsPQRTiAUOQWWUicHdAsqAb72aANOf/QPwivDmYNOxRYsWOT0lZojqACQijntrIttyMAjz17afjiCjieyS0W04YJuJEetET5pTrPkFQVXklVdesY5g+ddl8/fMmTPtmznRlkEy9wEdw+ADYRXhu+++a7vF0ftv2rTJppLLxAujwJgBSWX6sylAroRksNL5FnCE86qcXmIarlwJ08MxjRv5iSeclmMzlw9UIsI+4HXXXSdINiK8GTi95IgzSMXmcTaF3pVsliOfQDYP64tjcWCb/MQTGPnI008/beNA0HM1EWGXCM5rcvPNNwvHyziVzvpHwNnI7iNGjBBYYtpUcZGF+AJLXWnZsmWBweek7p9Y1kuTzWRrdpurbEi0NmO4KRgZWXNkZPVN2VMs1vWluqyP6WMOBGKlZ4PGNrQOoz0/6sYG1ES/u8hDoclpzU0xf2zQF86zPTMRwfjKlofpJFs+/RSyIRitNjwmAnpk43AJHeOOO+7IuQUiTcdZv1AIBc4Zb3C7vH379obp5Gg9yG3RkiiwbfQCjAvYIKzcvlu3boZOTI7gxWIQVMYmpXniiSesx2Ose4C5H3isxx9/3O7K9HG0ImUdcnmnTp1i+j04x+H/mObINLs9DLgJyJWQEF4QCfaCUAHQhfl2IFow2GOuuuoq633IysToryWfFUCFVpjQnBSa3wYXZR7AuXPnFrZpzpbTSYwuzFQMKn8xQLNweptG35c0HX7ooYeszwLrnYqA/51PLMXB0ug8hBavQRAcm8QFiWoLpRnd5Lj1QHdztBrMmDFjCi2jqBUxlQF3GgAw/t9SQMWYpwHyAYtvw4qhBq5Ro4atcObtcyo++j+XRwuabLbCmH+Qab0QHs1Q29N70YvCWAuMe4jmrhdPL+vn5PAxYMAAm3mJLTm6HvMFkF8BRN8H6PtHzpWh2OloxJgG9EEgv127djVF+RpECijkC93iWSbLT1UKVQZ8E9YALgXCLhvMBlN5V2XTbmI7Ax8J+yDzYY6u8MK+M6AJ0pIb5hjgDcPP2WefbZWCH964bB2wu5OIo0vQ7xN22dhSYouODzLrPJH7oFevXjbzM+8duilzP3qoMhs0PVPdEAZupedjOlKoMmChjGfAuAZMYx5WoedXrftrmeJV/+r/xXsDxFII3B4GU7YvyGYcZkR8RSWVAF12EabLV+ft5smyT3/99ddHlH8y94DTbWTXom3btuapp57ybObnuMqAhHYHKgJBSaOW7E1y16y7jNwlpuoRVe3NkMyNQOUQa7An2XPI9fYMMsPxkHh92lyfYyaPz3EhDvCyW0ce+EmkRcD65/3C7NR+kCKVwVaz1Ub3OdocbdYCYZJxZpxBw97cB1C+/fZbg/ndyIyBc2PEahE4y4ISMuy+++6zNzbMwcN0C9hmPOMocJaIzXC2lDDtbTjuw/4+67mwMSNnHVsDfpAilQEv4ieAKdcZ8msjEAZhVCMml70KiCWrV682zz77rA24Qu1f2CASvMti7e7LZZw1gT1+wpF2fHmRUSfNAV8qAU7bcWYrv3A2gIODHACEn0BMxcDIRXyB+EESUga8kB+AQ4DaABOUBlneNG/a4KftTLuEksvSxoDjARxggsGQvSmcZiSzFQdFOFLdrl07GyQ1v01EUK7RuQ4YWxn4whh4EJpEFDqnwmfMmGEHiznIyFaB85Jgq8oPkrAy4MWsBOoABwGfAkGUx8xjNsfi9eZ6swtIVjhDwKCW3bt3t33Mzz77LNkiPL09b3oOprGL5Je+cLKEwhnOhqBjDM5UA/HSWKhv374GPgS+yU2ZlDIgqewmtATYl34EoIFSEITjIecDvK7+gBtCwxQ/TB+mcq39+/e3bz54kLo2PZbKebi5D+uLAUj5Rodpr2E3wQ3xqh1J/mtLWhmwACqARwGmLT8N+Brwswwzw0wVgBaGHwMqiTHAUXY2iatUqWIQdCaxnTy6Fbtz8Dewg4GPPvpoHgtDj56y66eVkjJwzuJz87lpDPBtykzN6wE/Cc//dICp19ktCMvgqJt1xLen022gDX10JF83j5OpspiLgRmW2Rpo3Lix787fTV7SUgY8EfarBwMHAEhManoC6wAvyxwzx7QGaFBFZTYbUEmPAYZ158PEgbPWrVubOXPmpFdghvemSXnPnj2t/whiPZrBgweHsjUQTXPaysApbIvZYvoBVAplgC7AJ4BXhDkS2R1gt4ZKoCGQ64xRXuHGzfNg4o6GDRtapcBmN7sPdKLxiiCSlEEiWTsjQiUAt3iDMGNeOb2cnodrysC5CiqFZ4ETAT50nIq8H/gKyLbsMDvMeKAbUBlgd4bThZMAlcwyQFt5TkOy+c1kLHTNpUt2LgbTmIjm/vvvt1OFbLnQPJw2IqoE8t4DcVOyg7i0ZJbMkuHAW8BK4AjgTOD0PeBvN+VP+dMmgPlQ/sJ0mS6bgZOAdgDTqVcDVLLHAMyxbcAWBujANKsNeY6xBTn9dNwF+MCox0ZAdvOMliCALjwD7Wfq1Kk2oC7chG0ino4dOwq6M24eLjBlZVQZOCyxiTAbGAfwMf0UYKIWBlytDdQBGGrtoD3gA1sBKAPsDZQEuP22PdggG2Q1sAZYASwAvgG+B/4AmPPhNICKpzVwCKCSewYYz4/RfPiAIm+gwGNPYKEnTJrDYLeMc8kw4fABsPEuGaqdkaL5gemvMKEKIz7B8s8GBaWigSWo/TAuISNMIfiIDY/HZCN86Kl4GAEIiW0FVqK5J8HDZ5AVZZD/+vlgzwHmAcxORCwGfgb4dk9UykpZqQ4cA9QFqFSY8agWoOJ9BuDrYdOm8SHG1J7Nj8HcGNHh7oq6CnRDBFObNssQjISEn+OPP14wbmEVSFH76/q/GciJMvj78Hm/7ZbdshbgG595G5yWABVEacBpKTDBC1sRFQGV4DHAKMh842PaMtISYDozPvhOS4FxItmCYHYhWEMGj4QcXJGnlEEOrl8PqQwoA3sYUJWqt4IyoAxYBlQZ6I2gDCgDqgz0HlAGlIG/Gfh/zm2ghkDCIq8AAAAASUVORK5CYII=\n",
      "text/plain": [
       "<IPython.core.display.Image object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "testing on train set, i.e. test set is train set\n",
      "test set size: 2717\n",
      "of which positive: 1306 (48.06%)\n",
      "rnn score against target on test set: 2717 (100.0%)\n",
      "extracted dfa score against rnn on test set: 2717 (100.0%)\n",
      "extracted dfa score against target on rnn's test set: 2717 (100.0%)\n"
     ]
    }
   ],
   "source": [
    "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",
    "test_set = train_set \n",
    "print(\"testing on train set, i.e. test set is train set\")\n",
    "# we're printing stats on the train set for now, but you can define other test sets by using\n",
    "# make_train_set_for_target\n",
    "\n",
    "n = len(test_set)\n",
    "print(\"test set size:\", n)\n",
    "pos = len([w for w in test_set if target(w)])\n",
    "print(\"of which positive:\",pos,\"(\"+percent(pos/n)+\")\")\n",
    "rnn_target = len([w for w in test_set if rnn.classify_word(w)==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 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)==target(w)])\n",
    "print(\"extracted dfa score against target on rnn's test set:\",dfa_target,\"(\"+percent(dfa_target/n)+\")\")"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 2",
   "language": "python",
   "name": "python2"
  },
  "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
}