{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Handwritten Equation Decipherment (HED)\n",
    "\n",
    "This notebook shows an implementation of [Handwritten Equation Decipherment](https://proceedings.neurips.cc/paper_files/paper/2019/file/9c19a2aa1d84e04b0bd4bc888792bd1e-Paper.pdf). In this task, the handwritten equations are given, which consist of sequential pictures of characters. The equations are generated with unknown operation rules from images of symbols ('0', '1', '+' and '='), and each equation is associated with a label indicating whether the equation is correct (i.e., positive) or not (i.e., negative). Also, we are given a knowledge base which involves the structure of the equations and a recursive definition of bit-wise operations. The task is to learn from a training set of above mentioned equations and then to predict labels of unseen equations. \n",
    "\n",
    "Intuitively, we first use a machine learning model (learning part) to obtain the pseudo-labels ('0', '1', '+' and '=') for the observed pictures. We then use the knowledge base (reasoning part) to perform abductive reasoning so as to yield ground hypotheses as possible explanations to the observed facts, suggesting some pseudo-labels to be revised. This process enables us to further update the machine learning model."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# Import necessary libraries and modules\n",
    "import os.path as osp\n",
    "import torch\n",
    "import torch.nn as nn\n",
    "import matplotlib.pyplot as plt\n",
    "from examples.hed.datasets import get_dataset, split_equation\n",
    "from examples.models.nn import SymbolNet\n",
    "from abl.learning import ABLModel, BasicNN\n",
    "from examples.hed.reasoning import HedKB, HedReasoner\n",
    "from abl.data.evaluation import SymbolAccuracy\n",
    "from examples.hed.consistency_metric import ConsistencyMetric\n",
    "from abl.utils import ABLLogger, print_log\n",
    "from examples.hed.bridge import HedBridge"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Working with Data"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "First, we get the datasets of handwritten equations:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "total_train_data = get_dataset(train=True)\n",
    "train_data, val_data = split_equation(total_train_data, 3, 1)\n",
    "test_data = get_dataset(train=False)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The dataset are shown below:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Equations in the dataset is organized by equation length, from 5 to 26\n",
      "\n",
      "For each euqation length, there are 225 true equation and 225 false equation in the training set\n",
      "For each euqation length, there are 75 true equation and 75 false equation in the validation set\n",
      "For each euqation length, there are 300 true equation and 300 false equation in the test set\n"
     ]
    }
   ],
   "source": [
    "true_train_equation = train_data[1]\n",
    "false_train_equation = train_data[0]\n",
    "print(f\"Equations in the dataset is organized by equation length, \" +\n",
    "      f\"from {min(train_data[0].keys())} to {max(train_data[0].keys())}\")\n",
    "print()\n",
    "\n",
    "true_train_equation_with_length_5 = true_train_equation[5]\n",
    "false_train_equation_with_length_5 = false_train_equation[5]\n",
    "print(f\"For each euqation length, there are {len(true_train_equation_with_length_5)} \" +\n",
    "      f\"true equation and {len(false_train_equation_with_length_5)} false equation \" +\n",
    "      f\"in the training set\")\n",
    "\n",
    "true_val_equation = val_data[1]\n",
    "false_val_equation = val_data[0]\n",
    "true_val_equation_with_length_5 = true_val_equation[5]\n",
    "false_val_equation_with_length_5 = false_val_equation[5]\n",
    "print(f\"For each euqation length, there are {len(true_val_equation_with_length_5)} \" +\n",
    "      f\"true equation and {len(false_val_equation_with_length_5)} false equation \" +\n",
    "      f\"in the validation set\")\n",
    "\n",
    "true_test_equation = test_data[1]\n",
    "false_test_equation = test_data[0]\n",
    "true_test_equation_with_length_5 = true_test_equation[5]\n",
    "false_test_equation_with_length_5 = false_test_equation[5]\n",
    "print(f\"For each euqation length, there are {len(true_test_equation_with_length_5)} \" +\n",
    "      f\"true equation and {len(false_test_equation_with_length_5)} false equation \" +\n",
    "      f\"in the test set\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "As illustrations, we show four equations in the training dataset:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "First true equation with length 5 in the training dataset:\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAgQAAABpCAYAAABF9zs7AAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjcuMiwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy8pXeV/AAAACXBIWXMAAA9hAAAPYQGoP6dpAAANF0lEQVR4nO3de3CU1RnH8bO7WXIBJAki14BIQAQZURFBEcdOFW0VBisD6CgdqQwqIFClDjhjp3Z6wYpS0BGhilQ7WmuxUxURtQpeuIiGooJIuClgBCEQkizZ7Pv2H+d5ztLdXEj23dv389dvsyfZk2V3OTnPe87xua7rGgAAkNX8ye4AAABIPgYEAACAAQEAAGBAAAAADAMCAABgGBAAAADDgAAAABgGBAAAwBiT09SGV/vHJbIfWWuN81KLf8YLO4e0Qk9aV6G/RvKfJt0Ss829zz4vudIpSHifmmtC6cct+n7eM4nRGu+ZTXt7tUJPcKpLeu1t0ffznkmMpr5nmCEAAAAMCAAAAAMCAABgGBAAAADDgAAAABgGBAAAwDAgAAAAhgEBAAAwDAgAAIBhQAAAAAwDAgAAYJpxlgHQGgLVdcnuAn4QGHiu5O13FUru23+/5H1HiiT3HLfVk34B6axi+mWSN92/KGabIQ9Pl9zlsQ8T3qemYoYAAAAwIAAAAFlQMqgZe6nk3nO2SV7Ra63kUd0Ge9mlrJDnD0uO5AYku7+pklzj5nrap6zl1+c/cuUFkn+59K+Sr8oPaXPjk1zraonn2S/6Sv6qtrPk11dfIrnHO9o++NbmlvQaSBvHJw6TvHz2o5LDri9Wc2PcRPfo9DBDAAAAGBAAAIAsKBkcGKlTNuusMgFaX/eco5Jn/PFuyZ2/+U7y5JL3JNe5OpWNxLHLBKueW9qs7831BSVP6bBH8sqc45IfnrRB8ucT6yXPvWZidD++2tWsx06koM/x9PEC1hxxtasfuzWOls38HvepKRxX/2Zs79eyUp4vIjli4kyLZ5GaLvo89Qum7/PBDAEAAGBAAAAAsqBkAO/Y06L53+v0p69epxernTaS7ZUIaF11o4ZIfnbpY9Y9+ZIm7holuXaC/rscurqX5GO6sMC0/Vpzlxe3S35iWKnkt5ctkXxwVJeoPp2VQiWDd6r7e/p4JcEjkuf+/RbJfeZ/ro3y8zRH9D3jNV+O/rfgVNdI3r5QN7L67eUrJR+qby95cGK7hgRjhgAAADAgAAAADAgAAIDJgmsIysc/GfPrt+0dad06HrMNTp/rT9+lN5kgNFOXgHYN6HUDK6uLJdeMtpaOHT0guWi5leP8fLvCnbtqU8w2t059I+r26sVnNNRlT60aWOjxI+rj9c7R5yvi6HU39UP0go2TRfrR7MVqRHsFcMF+XV7o2/CZ5H6/+FTyCqck5s+ZnXorJz0xdMKWZHehVTBDAAAAGBAAAIAMLRnYBxoZUxazzQfrB0guNesT2yHAAwfu1XPYt17whOTycK3k5WOukRw5+lWr96HvK3dKfuEni6PuW20uObV50lTMuKzxRh4IhLRk8PN7Xpc8uYP+29S4iV+eW+TXstKUr7WcuuUvQyXX51MGtIWu1+dmaclTksNxdmCdtOfHkrss/DBxHWsBZggAAAADAgAAkKElg3WPL2m0TeksygRIf76g7jDYd7ROM0dcvdz7mnXTJZdu0yvFE6Hn6/q4A8ZE77ZX/TMt5bV9eYNJpvfmPJLUx4/lGz0XynwW1o/mgAnGaN26dlnrRn7VdbXkzg+uaeZPmtVKPUpNzpUXSp732DOSw24kZt5mVXv2Legnua1J7us/HmYIAAAAAwIAAJChJYN42IwoOVzrgBS0rn1z9BCjLX0WSS6r02nLkueT8zbP9UVPdde1078/2nrdmVOErZJKyNUr/Q9EciXbh3V5zevHth+vyglauXk/J3XWkSRGqFhLdCPyqq17Yq8sGP/PGZL7vJz6ZWpmCAAAAAMCAACQQSWDnY8Os26VxWxTMZwyQSIV+PWSWp+1R/vuxZ0lnxHQfdILfCe96VgjqhzdlCVi0mvzlboBtTG/Pm/3WMnxzhpIhFBh7KnTVHPT1JmSD5+vU+Rv3D1fckWkjckkdlmgwF8f977msksMmSgw8FzJox96K4k9STxmCAAAAAMCAACQQSWDeLJtZYE99Rf01TfQsnX0zNFjdsc/M1vyOe+XS758XoXkdcd1c47Ppw6U7LTxdqo5cELLFcE/6+8wrfvbnvajuQID+kXdXj1ikXVLSx+1C7pLzjP7E90tcXS0rijZFo7eg7/Tm7slJ/6V2bDcVZ9IPtO9SLJ9UX21m1klgyonT/LCm8dH3eev038RX6Tx8oHPan/dS7rJzkWxGqe5LyfrIeD/KNzWaPuP6/R10/uV1CiLNhUzBAAAgAEBAADIoJJB+fgnY349G445jt5URKcFt1b3kJzjb+YOIw046ejLpihHp4gLDsaeatw8SycSXb9exR9oE4nVHA2oXRg9BXl2ToFk+9javFc3etYn25dXrJC84MiAqPvqD37rdXfiCnTqKLlg817JUy8ak4zueC5w4suo2762+jpyzu6qX29C+SAT2SsLto9/3L4nZvugT7/+wOwpkvPXJed9eLqYIQAAAAwIAABAmpcMmrIZUbe1mT/lVRjQPbUX771KcpurdSo0UFRkWsKtt65CLtEpxcpBxZI77Tqh3xDQKbQrFmqpZkQ7naqMuKkxHrU3Jqp0ChpomXyuG71xkmOVi9btOUdyb/Nfz/pks49dfnXmVVH3Bc1mr7sTl3OkUnLgTH0NH7uit2RfBle0AnXRJcTDg3RzofXTFkiuiDS+HiTTNyayjzOOZ8yOGyS3+2iP5HR7CaXGJzIAAEgqBgQAACC9Swbx2JsRFazc0EDLzBBydcquX4fvJG+86zLJTq5pEb91cXvlkDrJu6/V1R2DFtwluWTZPsk1jm7UUW11xO430teJcZdat3TDnzaV0SsiUql4V3GHHht9vK9On9urlQ5Hqk22sI+A/iJsHwGdnX8z7h7XsfFGdvvD2r5nxdbW7o5nsvNfGwAARGFAAAAA0rtkkM2bEdnsafjRxZ9KvvO+dyW39Fhfe/OjSuuq/PKwrixwrT07Isf03Ih6h3FnpvEX6GqMC+eUSX65WlezBPYfjvqeZJ9fYHt37iOST1orIzae1PJWwGRnSaslRyGns+/vGC55ze3zrXsy60yLhvBJDQAAGBAAAIA0LBk0ZTOi0lmZXyaIxy4f7HDOSshjnBWoknzjp3dILlldKbn89/rvdEvblySH3bR7ySEGd2AfyY92Wy55+IPTJHc8+JGXXWqWnWF7T/qAlbJjuvzU37NHTuyCTsAqNX5r7bJTZa0QypTnLNxOf9dif/PKBJ2X5zXeKA0wQwAAABgQAACANCwZxFtZYG9GZMzxmG3QOtr7Q5JrtxVKdsp0injwYmujjuARyd9F2ie2cxnO54uenvW3cPVIc1RN0DLQmHlvx+xDx2WpWyawFfrrGm+UYYLWS2V9qHvUffdMHy/ZsRoGq7SU4Mz5XvKK/s9JPhTJjKvwt9z3hOSwG/uY47Uh/V0fmnG75NzXNiWuYx5ihgAAADAgAAAAaVgyiCfbNiNKJnuTIyeoU9i+oE6nHTuZH7M9WubrLV2jbp88T6d0Vw5bInnmiDsl+98vO+3Hqx0zVPJND7wpeURbPcb6R1PvlpxnNp72Y3lp2pgpye5CctVHH39csNM6LjuoKwicKl1RtHfKIG2SuJ4ljX3Mcbwjj5d+e6XkTCkT2JghAAAADAgAAECalAzYjCi1tDE63RjnYlwkSJ97o1/nI/rdKnnDxX/Trz+uU/f/uf9yybmrdJoz0LFY8uEbzpV8aJhOl7513QLJ5WE9p2DS8nsk9/z3h03/BZAacqL/FvT1LpG858ZOkl+bonv6V0Q2Sz6QISsLEI0ZAgAAwIAAAAAwIAAAACZNriGItzthnxenSmapYWLl+cKSN4Z6Sy44qGNKN6y7v9W7jDW90O7pDpJ/10uXhT1w5meSJy/R6wkORPTwqzyfXitwXnCNZHvnwUWV50t+/pHrJPd8Or2vG1j8r6eS3YWUFbIuDDri6LUCQV/spXjZZGP52ZL7miPxG6YpPrUBAAADAgAAkCYlAyRfx8AJybPW60EofRfodHT1jZdKvrDwE8khNxP3NUsN+a/o87+xrFRy6Vxdarjjp1py6xy1TFT/Hrh221jJh1/rIbnbsq2Si6vS4+Cipqh0WDaHaAPemyx5y8jYJaX+f9DPwUwsoDBDAAAAGBAAAIA0KRnctnek5BW91kpmd8Lk8Af0QCO3Xg/XqbxVD0KZ1PEDyeVh3fkMiVO/Z5/kflM0X28ubvR7c4y272JlJ1ZjIAOdc3OZ5LFmaJxWOzzpS7IwQwAAABgQAACANCkZVAw/LnmUGZy8juD/+XQTm1CtXrkdctPipQUA+AEzBAAAgAEBAABIk5IBki9gdGWBP8C15wCQaZghAAAADAgAAAAlA8RR6K+Juj3/m2sl9/l1rd5RXORVlwAACcQMAQAAYEAAAACM8bmu6zbeDAAAZDJmCAAAAAMCAADAgAAAABgGBAAAwDAgAAAAhgEBAAAwDAgAAIBhQAAAAAwDAgAAYIz5HxK9QIKCV9rsAAAAAElFTkSuQmCC",
      "text/plain": [
       "<Figure size 640x480 with 5 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "First true equation with length 8 in the training dataset:\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAgQAAABICAYAAACJB+2oAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjcuMiwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy8pXeV/AAAACXBIWXMAAA9hAAAPYQGoP6dpAAAtX0lEQVR4nO29eZAc133n+XnvZVbWXdXVdzf6QDeAxkmCIsH7ECnqsGyLS0vyWPZ4Vru2Z73eiB2PPBG7G+GdI8ITMxuj2ZFjx3LYCo89kmzdt2RKokQRIkUKIgmAxH0f3Y3uRnVXd91HZr63f1QDICkeINmNqgbyE4E/UJVV+cuuzPe+7/d+hzDGGAICAgICAgJuaGSrDQgICAgICAhoPYEgCAgICAgICAgEQUBAQEBAQEAgCAICAgICAgIIBEFAQEBAQEAAgSAICAgICAgIIBAEAQEBAQEBAQSCICAgICAgIACwrvbA98qPrqYdLeFx/ZWrOu6ps+Mrel5b+HTLOn9y7lFmPz1ObKZO6HQWbAtjKUS9AZ7P4n3D5NdL/tlvP87HUvuY9R1co1bEhvtGT131sTfyb38jX/vjZzavsiXXnveuP3r1x97Av31w7dcXV3vtgYeghVhS44UFvr38M1wqGikESIlvC7QNUmj8oJ5kQEBAQMAqEgiCFuEi6HLKlIYEtU67KQaMAa0xIRuTjFHtFtR7fRKyhotAm+DnCggICAhYHa56yyBg5dBGUjOKdc4itY018l6Y2HQ3VrGOLFbRcQcvHqIyoOkcWSStKriBGAgICAgIWEWCWaYFNFAs6TAPJw7y/Qf+P7Z88DhT74lS3JAE36feFSE/HuG+ew/xvZv/lo2hORZ0hAYrEz8QEBAQEBDwagJB0AbsSF5A7ChQ7lcgJUhx+b3gBwoICAgIuBYE800LUGgUGtcosn6EX0m+yFdu+wz5TT7GUhgBQkPVtylqg4+4/JmAgICAgIDVoO1jCFR3N6QTzD7ci5sQ9D9dxrpYQJ+dxHheq81bEbSRlLEQuukZEDdqRsGdN7GwPYa2wUhB/48u4h872WqrAgJWFZlIIJMJFh4cJr9B4uQgVDB0P34Ob/pCq81bFazBARpjvUjXR7g+8vxF/Gy21WZdO4RAbRqnMtZBfsym2rP8sobUKU1k3ifyzDH8QuGamtXegkAIzEAX5dEE9//+c3ww9SJ/ov+AzsMhIhfmrhtBUDM2Da0QfqstaS2zd8bZ8tGj9IULONLjZ7N3EAsEQcB1jkyncNd1oj+2wP6d/8Cnclt54uIE7vFuxHUqCNyRbi7cF8GqglUx9Lg+3CiCQAiEUhS2dzJzr+BjDz7Fn/UcAKCkazy4/59x/niGzUfTEAiCV9LojFLpUfSH8nSqMo0OQ7XTIqKCALvrDd+BkWiO9U6WhKrxRPIukukUfqEE+vpSS8KykPEY7s1jzN0WITGpSZwpI/MVRLmKXsiha7VWmxlwDTGm6SHcEp5mviPOPqfnugkjluEwcqCPxkCaxc0RlrYYbtp1grLrUPVsjt6ZQeXufM3PClcQnhc4i4auF4uohSLemXPX+ApWCKlQE2Pkd3Qyc7/hA3fs5+HEIXyjmfYrXPAiFMphVE1cqUtzDWl/QZC2qHYJuqwiCeniJjWNlEKoIPzhekPbMOwssNmZIS2ruAmBSCUR1Rqmfp0JglAIkUoyvz3C6IdOc3D/KF44TuxCCGfeQVSqEAiCG5Jxe4Fi7DzPh269bgSBiEWpD2dYnHAoPVTmA2PH+M8DT+Mbg4vP/GafJR16zc9m/QR/feF+Dk4PYNXiJM7byHNTa2+RsOwZqI6kmb0L7r31CH8+8DMANDDpRTlaH6BRsYlUBfjXPmasvQWBkCyNKerbq4yGsizpEF0vSDIv5tHlaqutC1hpDLhGEZV1BiyPWic0hjqx8wX8er3V1q0oYmiA2Xd3s3RbnX838FN+kZrm4M4BzufTFIpRur87QfrAEpyZRJfLrTY3YBXRS3lsrZmfWsfnx4cYtBdbbdKKIBwHmUzibl1HbjxM5VcLrO+c4dHefWxzprFQSGGwUXSpBinpvub39KoF/nDgSU509fHNnp2cPNHPSPxdRCaL6INXX4q6pQiB2rCe7L29LNyq+d37nuLB+BEA9jU0R+v9/Nsff5jUEcXIKRdnoYjOXfv7oK0FgVCKWpdh8+AsnbLCko6QOlWDgycwbqPV5gWsMGJZEISFT0qG8OKaemcI237tlcOaRQi8TIylCcPEyCwPRXI8FMlBFxxzJafcbv7Nid8hvJggMhuGQBBc1+hyBdNoYC+OsK80Qjj52hPjmkIIpONAKs7ihjBLWw1/tfOLjFl5hq0oINBccYlHRQgEuMZHo/GX31MIokLyYKTGveFTfDB2hP+UfJifHX0XkMA5rMDolrjX3xJC4vUkWdhp2L7jHH/a9dLltybdTvaWR+neI+l6/DQ6X8A0GmhtmmXsr+G1ta0guBR56w/UeX/3YbqUy5KOtNqsgFVENuBctYtiNAT4+BFNIyER1vXiOAUZjSKGBljYGKVzYp7bMudf8f6I5ZKR0yR2ZTmf7GTifCfML7TI2oBrgUrGEakkbpfH/amjpGWFrJ9stVnvCBEK4W8dZWlTjK2/f4h70ye5OVRoTvzAKa/Kc7Vhatq+3LDNR/IP53cxO59CzDkIT6DWl+hLF/nj9T9iyMoxYVt8vOsp+B147KXtDIVuJX4yj3/oWCsv941Z3irIrw/zLx9+jHdFzrzi7XE7Cwn46UfGOXzXMJEpi1ABOk64OAs1eOk45hp5SNtWEIhwGBOPEk9W2RqeIiQEDaPaXwkGvG0u1V5wjQX4IJvph8jrJ15EhGy8TIxah+DmzBzrnVdGVidkiKgw3Nx1gacrYXS0dd4RRfs+az7izQ9aI4hIBN2RwI43GLXnWfKjLPlRxFrtaCYVMhqlOBChOCT4P/p/wGbbASJ4+BR0jaONbn60uJW6b9HQTUHgacXs0R6i05LkWR/lauZLCc73RXmqcxM3x86zwZ5ko+XyJz0/4sKGFGfGxgkVYqhDrb3kN0IohUwlqHZK/qfUMRxhA1A3Lq7R2ELQbRV4ZOQAp7q72JMZJb8YRhibaFKROpvEFIvXJMi4bQWBHumlOBbnpp6j3BwqcLCR4MfFbciG33QRXUeEhUtU1lmhzsZrFj8Mm2JzZFQF30jCsxbp4yVMsdRq01YMEYtRHI1QWq/5F30/ols1aNfHMC3bO07HR+AaRdms7S2l6o51zN4e4p71Bxi1Gnxi5r384twIY4u1NpZkr4NUyB2bKI0m8P5gnt/oP866l93ez9YcPjn5IY6+MMLI91ykqxFeczwXxjCRX0BU65hyFYwm8VICnYjw7E9v57GNd5L/2Pe4OXKO20IN/nDwST7/0Tr7wlsZeSGJrtbacitZjo9y9jd7EDvzSCQV0yCvfb5V3MaP5zfTHS6Rtiu8J3mY30w9T7Y3SkU7nLq/h/3FYZ7eejPJ04aOL+1ddU9Be45EgJcIUc0Iep0CCRniUH2QA0sDyIbf3FtpAau1YmqgqPjRZh2Cyy2QQWKwBYTQ6LdYVNJH4CPXRnXDZZeaDkGvnScsfEAi66AKteum3gQAUuJFBDrqMWZ52KJtH0EWdLTVJrwpCoMt/NfsBLpWvAi1DovqsMt4NEtUKGYqSbxcGFHPrzlBIJSiOhCnMGzxm4MHeX/iAGFh4eGT8+s8V72ZQ6cGyRwThPYcxdTrr3i+fylvYH4BYYdIV9Yh/W4en99CrdPi5tBBxuwcj3bt5ZmBCRjqR87N47fT9poQqEQCty9BfaLKHX0XUEIw4/kcaPTx4/nNvHh6HdFkjWS0RpddQkY04/YiCbvM/eEiRyKn2D2xgbyI0dXXg1nMr2qxorYdjcp9IYpjMBTOUdQNPvnz9xM/HGI4exZ9jdNNLg06Gbny6tMW8N3SBF+avo3IjEQsp5oYAelQlV4VQVGlZq4u0EgDNaMoGwvfyDUhClQqCd2d1Ho87oucple17W15Q/GvTzzSahNeE20EShhidoNbM+f5eOZZAHxzRQBUjEXNWNSMjW8kSrTvM1Acljxy6/PcHz+KRFKsO6iyRPhrLK0OkLEI535dsG3rGR5N7mPEspBIXmr4/PvJR9m/b5wtf5GFxQJ+pXJVW8DGbaDPTpEqlimUh/lvt48x9jtZxu0sD0fn+O37nuHLXe+i56sbiH2tfQSB6syw+L6NLNwk+Ju7/ooRq4Akwqfn7+dbT95O117Y+swMJuJgQg4/6Lqfb3c8ROG3i7xn+Dif6H6SCdviC3d+hm9vvYUvqvtJH1tH+u9/sWopl+038kqFsC1qHRK/r0a3VUQD1kWb+LTGtCA3u4GirENMehkA/BVqRayExhYeTy9t5Oy5bjoXmw+H8A3SM5wvd7Cvocn6XdReJ0f31djCIyR8orJOWFwREdrIyysmv91aWFgWJhKCkCYlBa7RlI2HdAHXA92+g/k7Rbbbb/EyZk51t9qEX8Y0/xllIKSpejY3RSd/6bCwdLGFh43fvmJAKmTIxo3Dzth5umUFsPC1oF1NfiOE4yBiMZyuKrd2nKdTGRxhUTceZ90u9p0cIXVKos9MYjz3LcWDGbeBXsoTPTFPbKCPn5fGsRMeO0Ilboud4exIJ4d7tpBMJtGVSlt4FYXjUO6XuD0NtoaK2EhOunX25oZInJIkT5fxzpxD2CGEbRGZSxJOJ7h4rIsfeFsYdBbZEZ7iDmeRe2LH+eLGWym4cbpGhzD5Av5CbsVtbjtBoDpSkEmztNPlT3f9I3eHz1EzkDoJHc/NoQvXfj951ktxqLqOz+69ExpyZVtCSUP8aIiJJ4vIShGMwSo2iFiCEz8b5bfO/iHGE02XwRuhAS2wO2oMdS3xu+t+zkfi56kYn4Yx5LRFzajLEb3thLAs/LCNdHy6VIxf1F0O1IaIXjSY2Sy6cR2kYb0GtpAo8crf9VJuthQa0eKmFls+OdvS878uWmNsCxMLs7ijl//rno+CNKAM+M1nZWzDLDs7prgveZw+mW96CtpsC0F1pKCvm/pgg4/EzyOx0G3uzXtdhEAN9tMY6mBDzyy3x04RFQoPn3nd4HMzd7H1z+Yx8zn8t7nPr2s1OH2eTHeSrz17O8e29/KrG/6Re8NzbBx4jF/fPkH6zk1EDl1ofQ8IqTDJGMVtDXaMT+EIyZ5akv987v3M7R5k9EtHMeUKmqbYMW4DXasjsvNs/C95SCX40n3v4zMb4Mu/9SnuDhf5xzs/zV9vupdvhu6i86U+El/6+Yqb3XaCgEya6liGWFeFbc40eW0z6ycJlQyiVGlJQGHRj3C+miF63MGqgZFvPj9fNQKS5zRyqdxUzEIgay6hvCBxxqZWcK6qx4EwzSj9WmeM03mHr1q3Uu5xKPlhXKPYEr5AWpUJC7c9txCk4NJ4XTM2OT+GdA2m0bjugkgv4WOwX/WaxlyeFJqlbFsnChrDmZad+w3RYCyBF1Z4YYEqKayKwC6B8JvPwflkhg6nwq64jbR0K/+Mr09nB4UtaWKZEo6w0WjqWrO0FCM+JxC19guQeyPc/jTFIYeNsUX6VAHXaOZ8j0/P38+Lp9exee7oOy+ypX2sXJnE8RiH0/3sH/ZIS0Ov0ohkg2qXQzjirMwFvU2EZaHWDVAZSTM4sMBNqWkADtaGOHlgHd1ndbPWwKu3hLSP0eBnF5CVKqkzafyww0U/znq7wDrLYVtkii/3u9TP2yRWwfa2EwSlrV3M3KP4H0Zf4BZH85dLEzw5P0E45zULeLRgX23GTfNStp/Rz51D5xYRoVcP4+8AbRDRCCYebTZzshQyV0TMNOg55oHvNyfLN0JIUBJhWeieDhpdMWY2jvJf+9cjl4NSxz9wmg92H2BHeJLEKsRCrCRFHWbeTaAa5prl37YCbczlAiyXERrfmNcMkrvWnPvD9hZiQno0igY7a9N50Cf1+FGM64ExTIZ3csju531dEWLCoyZs/DbzjhW3dTH7G3V+a6xZpKZmPJa0JvpShMHvZ9Fza6fZj1CKuVuj5Le5fKhjH9tDggue5uvFm3nyr+5g7GRjxZ5l/8QZBiYvkMvdzL9b9yEe6dnPx5MXGOpdZG7TAKnjsRU5z9tFxmPMvWeQpc3w1YkvsN7WaGP4wtnbmPi3R9Dl6htvaWgfXSrh7D1Jlz/Gi7VhBq2DbLBhU2iOXZvO8NLkBF2rYHt7CQKpqCcVur8ZcVnRLl+fuoWp4z1sWiiB2xrXcUpVGUwWyN4/il0exKiVcQ9c8jI4Sx7ObGn5NUFlQyf1tEK55g33Eo1oroakawjP11CnZpClGrZSJCYldlmhGs3jDhweZmowxf+2cTfjoYsrYv+KoRTakgjZnBx9I9FG3BBtoF/tIlZtVL3+XcNX9ua1EegVc4u9kuYWyev/2JfO+/LzX/rMbDnJhXiSXD2O9Ddfzt2vDPmMpAvEZB3XyLYQWK/GjQqGuhdZF2ruBR9phHipPoSTM4jFAtpt/T741WD196E70xQ2+GzaMMOAlQcUeW0zXe8gMeXhzBTwV2oxp310tYpyDQ1fXY6JyoTLnM/4+GGrtZE5jkNxPVgjJTLKpW4Ez9R6yS3G6CyVry6+wRhMrY6dLfOXex/g2dEx/mb9t5DCJiR9jFydwbF9BMFygE2lV3DX+BnWOxeZ9SH3RD8Tj+Xg1GTLur+NOXP8Rm+V7/6vHg1tIVfI/yiFJqR8ntuzifGvhC+/fv4DittvO07DV284kEmhqXghsuUY2V90sX7ShnoDlXWJXsgS9X0QEqEksdkBSgMdPPZH23lf12EeWpErWCFsCy9moVR7ey5uNP7Dum8DzfCUhpG4qzTM2mhC4vUTa2vLz8Crz2+jyWuHi36CX2we5/n7h4GmWPhwaoZhJ0dalSkYp+3iBwAaScGH+w+yI9wUXt/O38L3J7eQnnTxZudabN3VU902yOKEw4fvfZY/7XmGqAjhGp9pP8XxQg+xAzN4k1Mre1JjmsGlLxOqmxNznBjqxk3EaOWmgYhG6L99ho+ue4GUVBxphPiL8w9inQtj3kLKvK7VEKfOsfnfD3H+vg1k/+/VXyG1jSBQmTSmr5vKgObhzGGW/BiPlbYTnjfI7BJ+CwPLwsIlo0rsSp9bsQwDAFt6hIXHntQYRjVXxEYAKZd70qeoGQtXv/ZPdClyuqZtsokET9wc4vzHRptvvmzsS532icw3kHWfSNal5DrU9QpueawAbn8H2Z0h1nfPAM0YgoIXRrSo3kRAk19/4X/BVj5d8TJjiXn+efdugBULTL1UK+OruV08NT2ONgLDldvX1xJb+Ty07jij4QV2RU5jC//y+aXQNFAooRl2FiBz5bnot5dIqwo2r12joB0wQqAwr6hvYoyANXbf58dDLN3SYEd0krCwkAhcfI7VBsiW4/R4q5M3Hyr6nJju4Wi6H1KT3Bk/SX3Y4tnk7a0RBFJhjQ5R2djFePIo46GL2ChOuT2c2T9IxyneejyUNoiGi6pD1o9gC58diWmeSU+genswpfKKNj9rG0FAZwf5bWniY3k+nrzI/7Owke9d2E5i2sObaW20c1i4xFSD0cSBFS1OZAtNWBj+quNeUKFmRpUQpDrKPJI4RM0I3DcZzJrV2iTvSx/gyMQg0BwoU6pKWDT4N7sfJXUwQv9TS4TzVfINh8pVpjBeK0rDEZx75/lAb7P+aNGPsNiIXlUwZcDq0f/nIdyoxfxYhlObB/jYB/cghWbJX5mCRRpJTdt854WdjHz7UkDgledL1X3cqMXXf/MWRtfNM7Z+joSsUdTh5rYSEolGCc14aI5tzhS28FEYasbCR74i3TZgFRCCxa2GP7rzJ9wTOYtF896oG82h0gC5xRjdemlVTu3M14gcSfBi/yD0wa9GSzwc+Tn3Zu5YlYC7N0PYFqVtPSxutPhY6jQT9gJKOOwvDzP0uE/kfB7/rZbeNxpcD+UaJt1OxkIXeTB+mL/tvRO9rhs1a11ngmC5Sl1lrIPZu+HBvqb7bPf8RqYP97JhqdJiA6/gGslK+imaA5WP1lcGLGEMvhHUjFhOE3xzQaCNJCbrrHeuxAbEZB2F4datZzjW08OxiQT4gg/37Lm8Z9kueBHBRCbLkN20a/fSJp47McqGpesv3dCUyqRP1Kh3RPg/d76H+1PHeSQ2/UvH3ZM6gRzRPLdrJ52xW7D2nkQXi9fWViFQdU3qrItVsfif9T8HYRD+Ck2wppkdkzkmCC1W0I5C2xLhGaSvUaUGsurRsSdO9tgg/3vvxzHqlecXy+m2fqdLprvAoyMv8WhyH+7ys9PuYkAuezQkgpLvUKmFyLR3LOdlrNFh3MEM4cESuyJnSEmBh8/uapRny9t56okddJwGU1nhEthCIEIhKv0RatuqvCvTnDMWdZU5XyJbEHohw2FkOsXs7Qo2ldjmTOEi+Nv8KD88v5mBqSIsLL3l7zW+jykUCec8vjl/C/ekT/FI4hDRcAM/EkHZKzuFt4EgkIhQiNI6iztvO8r7MwfwjebkbDcdhwVqofTL5SxbgI/ANyv753KNAckVQaBZ/r+kZhQVffW50zHRIGHPv+I1heFfDv4Qd8CisUOhkYSFe3kQahe8CNySOs+gtQgoDmb7myme+Vw7Jki+I3SxiH34HJn4OD88uI3yZueXBIESggcipxkLXeSHN+3AdyKsOxa99oJACmTDx5nOEz0JXS+s8HCx/OMKY0BrvEwMPyRRvka4GllpgOvRt7sGUr5mMK9wfUTdpbijh9yWLp6Jj/Gx1PMUWTuli6XQKGFT9hzcuoX018Zd31iXYWFHhJv6j3GbU8ERYerG5fHCdp6Y3sjIP1YJnZrFK6/sok6oZvOkSrfi3RsOc3fiJABZX3DK7WwWNLvGiEgEk0qQvGWB3xv7GRN2lawv+MbMLZTOpBDnD+OX3sZK3hj8QoFQtsq+qXXEVIPfS50gGa7jRxOY600QCNtCJhNUuwUf730aF8V3KknEyShd+0uQW2q1iWsCH9EskPAyLg0rUmhCy0e1lRgQAmHZaFuQkDXCwgMUixcTrDvqIxdL150gML6PLpWxKx6iEqLkOtjiyp68RCIRZJTCpYyIeXhRC9S1zz6Y/AMPd9Fh8InOZk2Id5BdI3QzCEx6TZepEaIpBAzokMC3BbN3C9IbcuSm09hLiu4XwoQXPHynWQzMiNcQBL5BNTSVHkUjbUiGaq8pBGKi0Tb3vkwkEP09VHthZ/g83bKObxR7LowQ3x/Gzs63xSLozchtjVB7T5H3Zg5jC4VEUNQeX913K/GjIULT0+h8YcXK7ArLQqaS6PUDTN+XpPSuKr/d/SxjVh6I8neLd/Pd09vomb3GLgIhoKuD+mCKm7qOcV/0JFFhk9MWx8/0kZiSzcyCt/N3EALpOHjxEP0dizjK4xvlfs5Nd7LlTA4W8yt6Ka0XBEpB2KGRNLwnUufHVYeflTYRmwZx9Cy62t4d19qJ11sRqeV91rZDSETIRluQUDXsZRvVkkX8TAFzjVfE1wTTrK0g6z6yLqj5r3wEJQIlJFFCpGUN2/Hww6YlLaA/edtX+P7STfzs+Luwqma5INdbEwXCXCrHvVw86+Vj4vKWgRcBLyq45bbjfGrkm/z54H08Nz9C7uIA2hJ4YcHrLfaF3xQZtYzAi/vEVOMVPQ3gSi+SdmnnLKIR3N4kjbRmxCqQlhKNoZyNMnzCQxRWbk94NakMCD4+sYddkbNYy0uOmoHYiRDdLzbQ8zl0ZYW8A1IhHAc6UhTXx6jfVeRX1h/n3WEXluMW9mRH8Q8lcRZK1/yX1skI9YzF5vgMm+xmO7oFP05oxiY6p5v1Md4mIuzgRRV9sQIh6bGnOIaaD2Fms5jaytZpabkgeDXPV8b4ztntpOY1plptSSGigGuDjEUR/T3Uug0PRM6Rlm13O64uy2lTLw80ksKgjY+mWaDIGBCrlP//Zvz19AMU6mGKO+sY//Un5dfFAFogbE1HZ5FUpMaWVDOdTiMuT9yO9LCFzwPJo9QNfCD1Ervip9nzO+MsuVEs6aNep06Bb5oxNGm7Qk+owI7wFEoYErJBFBeFoWws/iF3J9lGnM+PvIM/yAohQiFqXSFMzCOjFAqBa3wwollH4a0GnrWIRlrzaHI/vWqVxOqyB1F1ZZj7tfWUBwSRWxfYkDnJv+h5nnE7C1gUdI0lrTk33Un/IYNaKNLKCg55XeMvcrv43tQ2hp6oE5pcxPfe3j6GUAqRSFDLWHy0+3l8BI/lbkK6rMr82PIRWFgWxglxKZNpqt5BaS5OV0m3RYOKgNVDhGx0IowXNayz4vhG4xofocV13dAIaKYT+YKGVtSNhxQChUBfakBlTMvdxsdnehDSEEtVEcIsl1J+a3ieIuI0uG/gNJsjM3wkcRyFoPaq9CsfyGvFgnboVmUGVJG7u6cJCfGmkdlKCBrGUDfNTp/Fl6fVCk3N2OxfXMfFYvwt278aGMemkZCoaJ2wsHCNT8W4CFcgPd2sTroG0GHNJrtZFdBfqfLiUjUnQSVBKWQijj/QSW67Ib0+x2d2fI4B1aBHRfEQFHSNSV9y2u1BzYeIXahhVjhm4erslmglljNcDPuWhsjOpOg+OoU3l337Ik81eyI0EoKdzgUWtIOrFcJnVebHlgsCvXGIs48kGbipmVr40sIAqUMWztza6wUe8NYQto2bDmOc5mByyqtyuNFLZE4gJufQ5et3u0jlSmQOxTmb6uU7Q8Nscy4wYbeXCBr5dHPlZ95mO2phDMLVeNE4P9l+O491Gv7fjWWUMghx6d+V47UWGCNe872rwRh+SbQIYWjUbZJPRkjlNLSyo/Pyire6oYvih4o8sv4wALtraZ4sbCF1RBF+4QR+Cxq4tQVCwO3bqPSFKQ5Y1Dtg8KFJtqWP8QeJ4/RZS0zYGls0qwx8q9zFfzn1MLm9PfQ/7bHp3ALMZNFvJ3jvHdktKYzHWNwk6bXzaKDq2eBJjOe/oxgK1dXJmUc7aWypkpCChVUeIlorCKSi0RHG31DlpkyzO1Wx5hBeMshao+UrpIBVJuxQy1iISNOdVtQ2024Hqgq6VG62SL1OEeUq0Yse9qLFqXovfVYe7PaKmQhNL76zLzAGXA8rFiGe6ULVBYVoFA0ItzlxX5q+V038C5ANSJ9sELrY+r15YVvUU4q71p3lXfFzAJxtdLM3N0Qkp1elpW1bIwQIiYyEEZEwSyNRisOS8pCP7KrzH8e+xs7QlWmqbiR53eCsF+IHuR3Mneiif7/Geey5ls0XQgrqSUEjo0nI5iLGM5J3HBEtFSYapjrWYMvAHDaCmrFZakSQ7upsI7ZMEAg7hMykubjJ4e/u/K8MqAp1E8L1FPG6gTWSehPw9qmv72Lm113eu/kI0KyAV9EhpGcwb7NF6lrBz84TeaZCqn8bu2/dSNdgibvDx1pt1is4/K963vF3CCMwwoDyQRlk2EdNhhl42sPOu9gL5WZTr1UMmhTGQMNt+d68sGxkKkmlV/KJvsfpVhoI8eP5zUw+N8jITGtKs7cSlU4j0kkW7u4nPy7Z8vAJ/rjvF/RZeWKiwZaX7f4UdI3n6ik+Nflesp8bITbrsfnkPOSWWrt4FJLyOshsyDWF/UogFVZvN5WxDJ+443Eejh1BCsHe6ihH9o3QdeY662Ugwg6mN0O9E24JeWgs8rpBvWZjF31EC0sVB1wDhMCLKob7smyINgsqzfopjpb6Uddvg8PLGM/DLxSwK4ZyI0RthWtcrASDY/NvftBVYICGd+X65gs2bkwhXYNVspvpjKsoCAzgZ6Ir1pTsbSMFWBbahnUWREWzf0nRDWMXBbK+9n2iSoDvgBeVhJ0Qomo197qX0+dEIoHp7eRSWwo3FaGRslnaJPE2VPlQz4v8WjSLIyzAomTqlLTLpGdz1u3ju7mbOXJ6gImXiqj5Av7UhdYHnkuBH4JkuEZoJRKlpUKGHfyBTsp9NjdHzjFkSSY9zZFyP7EpSWR+debH1gmCgV7OPpJB3pJHCcE5V/NMdQOhExEiu/fjN67vFeINzfINX81YfGTgAHdETwHwxYu388JTE4yevfFWSu3In2385op8z6V02Gb6n8eBsSG+u/UmCvUwS/VmuppY5daWUtRX/RxvBfWylA2JwYjl2gwttGklCAtBfazGvBcmeq4P5Th4M3PIWBTGh5i5J83O3z1ASHrYQpO0qsRVnduipxm3F+lVFo5o3hN147G72skLlfV8ds/dhKdtBnfX2JItok+exff96zLwXGXS0NPJqY8kkeMlBlWJSU/yqYvv4Yd7d7Dl8ycxxdWp0dK6ZYml8GKGtNOc+IvGZqqRQdVYudzVNkcKjeKtB0+tdYRtITvSNBKCjc4cnbKKa0JMFtPEpgWq0LhhAkqFNtRci4p/pR2LRILQLW+EnJYrG9QpRbORz1joIrs6zlHRIYpeeMW6h64l/Jddc74eJpwzqEpjTRXiUkXFT2uw2S7TKSMA2AhGBhY463czf2uS8GKcyMVeGlFFccgmv9nnkc59hIWLLbxmnxjh0qtcMsoh69eZ1JpzXgfTbgdfmbmV87kOEsdsYjMa50wWUyhh6m3kRtQG6UG5EaKBxAb6owXOJjohnUBWKlffb0Aq9FAfleEYrC+zc3AaR8CkF+fZC6NEpi30Qm7VhFDb+ClnvRT7loawWx/3c02RmLZauVwLZCJOdUs/pWHDw5F5QDDvV7lwtovNu3OIC9kbJqDUqhpKC1EuDKaoGR9bKGyhcE0zna6VYnFBr0wTo5ejMISEz4OJw6g1Nf2tHnPTHWzZ3YyQX0ukj8Lv7/kf+Vc7H+f3ks32xkkZ5uubv8DSJs1379jGnJvkbKWTpF1jZ/w846E57g03PYDycjtri7z2uODV+UbxJg6UBnnyxc04cxYDP20wcrGMOHsQXa/jNRotjwV5LUIFQTaXoKjDJGyf3+/9KRHlcnTHduKxMLx07KqyDWTIZvL9KSpbanxm199zc6gACJ4ubyL03TTdp+urukXSNoLgXKObI7O9pAvt92OvFq5R5I3E81YgInUNIeIxljaG8PsaOMJmzq9yuNGBVVDNcsXVG2fLIHyxSuJIgr19Q0x1W6yzGjiqGUn1ljujrQF8LrX81W1TOfBaIeMx6uM91Dqb162XH3rRkIjFArqdVr1XQWzOp3QiynNj6/lg7DgZGcIRFkkZJip9dkVOs+RE2RBOEZV1xu0sGdnAIkrVNMjpOvvrPRysDjFV7+BiLc7+80PohRCpE4rIgiY8mYelQrMPwAqVQF5xjCY6a6inw5y9tZsdoQLdqsxN8Sl233YTpf40XfEdWKUGcqmEKZbwF3LIRKK5leKEMLaF15uikglR2VJj++gFBlSRmjH8zeLtfOvcDlKTLs7c6vb2aRtB8LOlcZw9cZLnrt/c81dT1g5ZP4lXsxG+h5GCt14Obu3h9aWpvafIB0ZOIhEcbnTw2Yv3EJ0WeJNTrTbv2vLcQQb2Ks5HbueJ0S08FDtCSvq4xsenuRi63u6IZqMw+80PvN7oyjD9QBhny9IrYwiqouUt3t8O8f3TRGY7eGJsE+9OH+WByDn6l2tWWCh2OaCpAM0tYEkzUBBg0tPsqY3xnw69F55PEZ0zhBc1E/tn8admwGiMNs2CR20ujI3v0/nsHPGpDnY/uImd4fNM2Jp/mjzC1n8yxU9Lm/ns83dhz0XIHE6SPFVFPJtDDPRSHuugnla4cUHu3jqbh6f4b8PfZ3uoiC0kT9e6+IfvPED6OISfehG/Wl3Vv0fbCAJtxHIr01ZbsvooDGHhsae2gb89cSfhkw6qVMY4Nr6j2v3+f8doS9KVKDLgLAFwrD7Ac5PDpBev8wt/LYzBeB5CXwm+u7RyVEBfR5HJ3jB+bxpVqeDnFtt+gAx4bYxt4SY1mUgNiWTKq3Oo0YNdvPZ9KlYCUyqhspLoi0P8a/MhNgxkGU0s8CsdBxiycvSqBqHlKpKnvTh/P38Xnm5GxhxY6Cd7voPESYuO4x6hJRerWMcsLq29lGNjYKmIY1s8vXcLZzd08slNX2ZIeYxaeWqxU5zY3MO5wQ4u9HeQ2xYlseMuqj2CWo+PiXqoiM+9Y6fYmZiiYRQvNpJ8eeF2np8bInPIkDhfw1yD7ZK2EQQ3ElJoUtLl6dw48S8niV+oIhcKmGQMoyJvq0TsWkKHFBtTWdY7WZSQ7C0OY+2PE59aWy7T1cYWgnt7TvE0UBrpIeH2IgqltTdgBgBgHIXudOmPFQDYXx/gv8/cTXhlsjuvOf5SHpbyDH9F4P8kycKOIab6hjn9cBd3dJ7lwcRhwsKlqCN8beE2nv3GzcjlW7fjhMeWp46hq7XLAYJreS3oZ7OIpTzjX4yxtKGP3X+ymV+LH2DMthm2yrxv9EdoNO52n9Me7K0NMxa6yKhVIiUV0eXMCtf4fKPcz57iGD/93i0kzxg6vncIv1C4JhtsrUs7zOXpfiHNnOriJxNxLpRSrTKlZUjxsg5yQuD2xCkMh+mIz6GvY1EgXc10JcUhZ5AnrUV+MT1M52EPZ6ZwwwQTvprkGc2nf/EgepdkS6ZZ0tYWknsSx/GRPN7Th7MUJaQkJijRsSbRIYtYqkpfuFmR8khtgAOnB+lf7Xq0q4zJF1GeT0YKEtMO2fIQX08M8eXEvRiaHS2dRUHP3jrSb05roblmrNA76QLYbhjfJzSVo0N38Jc/eZjPDd3OH236KRudWe4NN71CtoBuWWenM0lKuiSExF7OJ/paqYt9lRG+/Nwuwhdsel7wiMxVr2lsScsEgTeXJfWDCn5oK99/aAfzhRjOm3/susNI0YwdUJJKT4j8BsH2WOF1WxlfDwhfc7EU56AaAKB+Okn856cwxRu0hjuQPpxH6BRPjEzwx8uCQCF4ILxEt3qOb/fcTThnE1KtTkYMeLsYSzKYyjMUbpYnPlrqI3bMIXJxbXvG/MVFWFyEqWlsoPeHV/GZVbeqBWgf78w51Mwc43IL+fE0n/+tO7in9zR3OD/HERKJpEtF6FLw8unXNT5fvXgre08PM/YlTfjwafzs/DWvs9C6LQOj0dUamf2LPPXXu+jMaeLnilgXci1tXdkKjASUYmmjYvO7T/Fg5zFco65bUWCfy+J8YZhZJ8NUeD3DJxuYYqm5R3aDIi7Mk254TBUTrTYlYJUInbnI/N8N88XECP89816iFwwDR8rY0zfemHc9oxsuoTMX6cwnWPR6eDzey3e67n7T6ODYlGHdok/45Aw6X2hJBcYWCoJmvXr/0DG6Dl15+YZ8MKTAKEl10Oc/jHyDorFxzfW7EvSmL5D8woVXvLa2nabvHD+bhWyWcvEWasZDG3O5eE3NhME0Xa8Baxdvapr0Z6d/+fUW2BKwimgfb2oapiD10lv/eCvvhyCosJ3wBFkdDQq23MCM/p3kwWc+8Yr2f6oBIy/mUbkS/hrLVQ8ICFg7BIKgHdDN0V9oqGmbkPCxRbBuuBGxfvwC3T/+5dcNwUoyICBgdVmbCbABAQEBAQEBK0ogCAICAgICAgICQRAQEBAQEBAQCIKAgICAgIAAQBgTFEYPCAgICAi40Qk8BAEBAQEBAQGBIAgICAgICAgIBEFAQEBAQEAAgSAICAgICAgIIBAEAQEBAQEBAQSCICAgICAgIIBAEAQEBAQEBAQQCIKAgICAgIAAAkEQEBAQEBAQAPz/CdcmuBZR37MAAAAASUVORK5CYII=",
      "text/plain": [
       "<Figure size 640x480 with 8 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "First false equation with length 5 in the training dataset:\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAgQAAABpCAYAAABF9zs7AAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjcuMiwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy8pXeV/AAAACXBIWXMAAA9hAAAPYQGoP6dpAAAPzklEQVR4nO3deXTU5b3H8WdmEkJCAmE1LIFIIGwiIpUWuJQ1eqqWq2ilUtriRbGISlWqt1fusdjFVq+eVmtdClpjLUgXoOBy9VBoK0WiKBVkly1BDGsIAplMZn73j97z/T7DmZDJZOY3M8n79dcnyW8yD+E3yTPP91k8juM4BgAAtGreZDcAAAAkHx0CAABAhwAAANAhAAAAhg4BAAAwdAgAAIChQwAAAAwdAgAAYIzJiPbCUu/XEtmOVuvt0O+b/T3W7e8fh5Y0X1HG55Kn33uf5Pbr9uhFHTtI9Jw+I/ngjGLJb9z9qOS99bnxbmbUxhftbtbjec0kRjxeM5sPFsahJTjfZb0rmvV4XjOJEe1rhhECAABAhwAAADShZAA0ptbxSD4xwCfZE+onuX15pattAgBEhxECAABAhwAAAFAyQBx9FmwnecXsxyT7jJ6wPfWJ+yX3XGqtPgBcZN+TvazfgiFOg4+K16Plwcr6JDYEccUIAQAAoEMAAAAoGSBB7PJBO0+d5O/fsURyWdllbjYJEEGjQ97DV8yT7PgoGUTDE9Kf38+vfFny0GQ0BnHDCAEAAKBDAAAAWlDJIDR2uOS9t+vnd0xYFPH6SXPnSM5eUZ6wdiF8eLYi0Em/4IQkhjL10528bSTvTWjL0Bhfvp49UbO0s+QnBrwq+QdXT5cc3N688x/cMuPJeyUPWqJ3mXPunF7k4f1SQxy/X/Le8d2S2JLUc2TlQMkfXrFU8o2fTJZ8Zk4XyaGtO9xpWBS44wEAAB0CAACQhiUDewhzz7N9JJeN1NLA8CxrKLqB7/PMz38h+Ru99ajenssPSq6vYN/9RPK005UIvVedkHzZpbdJfmP005IPBZN3FHJr5b9cz6FYM/RZyV7rvURdQZ5k33Z32tVcvV7RTbFO/dvFkkc9qOXDY3Xcbw3Ts0quyKaw5xk+RPL6ES9KDjj6c1rS938lf7xKd3N6cOxUyfWVhxLVxKgwQgAAAOgQAACANCkZ2GWCU6U6g3PL2F9KtocwGyoT2EoydSb7xge0fPDv112nz3uzzp4NVh2Jtrm4AHsPeZOl/weeQ1WSQ58OkJypCxSQBAduDUq2X2Nek97/Mdes1dpG14yNkke31SHbaH6PwJjqUFr8GYk7Z/QwyfeU6WqCTI+WCW45MEny/hpdYbV26O8lV0zT0nf3xykZAACAJKNDAAAAUrhkYB2vaa8msMsEibBywArJs5aXSj465rwhUo5JjVqto7sOTc7dJnndiyWS6yafkdxKRyBTXsgaRH+2WlcftNmkM/aDJj1MzNkZ8fMnuPlwAZ4RuprgvrLfSZ6QXSv52/t1A6JTN2hZtH1na/e1tzQ+P/cpyQ89PiJeTY0JIwQAAIAOAQAAoEMAAABMqs0hsOYNnHqtWPKWYYtj/palW2+SPKFgl+QFXT5q9LGL+7wt+bZ/TAr72rEpWZKDR4/G3L7Wxl522Maru3XVJaMxiOj4rFGSd47TnSJD1vuHw3W6FDhYU+NOw+IowHshRMk3RJdBz331j5LteQOzK8ZLrr5G59oEq3U5ta+D7uh5MqSPHW4tv67+pr72jDEm/+UNMbY6NrwqAAAAHQIAAJBqJYMvDpX41yaWCZaf0V2gnrnra5JzN2iZ4P32RZJHTBsnuXT6u5J/UqC7ltkW914b9vGwZ74tufBGSgZoOa68c73kkFXisZcdfjB7mPWILW40C0iKHXfkS74yW5dH7wn4JR+e01uyU/1xxO8T3KnLc0f/fa7k7eP0b10wyyQVIwQAAIAOAQAASHLJIDR2eNjHsxataNLjB625XXL/XwYktyl/X3LYzmnWbGj7EIn3PhkpufIXf5PcK6Ph8ZvCjtVNaiuQyg4sHC15dTfdOS38ECN9/+C8l95lAnu1S5+MyAc1nQjpKpgTQd1lzuthl9KW7tx1+jdh3Vcfl1ypt4SZP+Ebkp19kcsEDSl+UstvlWPOSW57Y1X4hYua9G2bjRECAABAhwAAACS5ZJD5cPjwyPW5Rxp9zEa/Dt0VP2+dWF4e+xBm9opyyXfN042MlpesbPAxt/TSmdgvjrw2Lu2IVVHG564/Z6w6ePWs8M5ZOmP3dFCLO06m/r/2zsi1Hp0+/850M+Yq3ajLXk1gv2cY8AedGd3fvGvS2cd1BZJvek6Hfn3WDlldv1Ipec3gP0s+GTzb5Oc74+jP9Bjlh5RXMP8Tyd192ZKHvHyn5Iv3NWPToHf19bY70FGft134Jl+nY3+GmDBCAAAA6BAAAIAklAxqpn9J8t9Knj7vq5H7J1/dOUWyM1FXB3jN5ng2zRhjzJ6NffT7l2h7Mj2+sOtuyD0m+cxLeubBskEFxm3THpjv+nPGzJrQ3ea0DqPm9vxUcvEyncr7pfXf0YfaI9ku2PiKu8/nNvvMgtcLI59Z8NARXQnUf156lwlsVYF8yX0W7ZbsaaPD+bWbu0v+QtEcyd6wpUsNy6jVcsDhcXrz7piiP+tP6/0GqaHiQV1ps6xIVxasOZcvuf9z+nvKWnDQZN5LB0ouzPiH5J0rS8Ku62GOGTcxQgAAAOgQAACAJJQMRtzzoeTw2cwN8/9Mh+7amEMXuLL5+j70geRh/fS8gn+OeinsOrvtBZnVkn2Dvyw5uG2XcUOnjZ+58jzx5visjW5ydSZv1oHjVrYe4Im8gQxiE82ZBav2XyK5h9nmTsNc8MUc3Ve+x/qTkr+/6XrJ/f77hOSuVU3fZN7j6M8092BbyVetvkOy12/9DvSm//297s1kt6BpfBd1k/yTmWX6eau2eU/ZLMm99+nwfnMcv1xXFvTL1Hsrqzq5q04YIQAAAHQIAACASyWDkzN1NvN93R6zvtLwMFzpVt0gyD7COMoJvjFz/Drr91xN2wtcqfK8tZIDnXIku9XbuuutN1x6pvgq8OkmHNPKb5Nc9HUdzt2/VI/EfnXkryV/Fmyf4NYZY8xjjV+SZmpu1lU+C7vpbHf7zIJNfr1zezwSvrqmpWjr0d8kQ7MOS/7DqOckn36rjWT77INYdPXpfvWT3/6u5P4v6Fz1+txMA3ft/J+ekq/JOSV5yN9nS7744fiUCWxnp9Q0flESMEIAAADoEAAAAJdKBp8X6nBkjwscKRzmV10lBmv2xbtJDcoo7CV55oj4DxUlQo43PTc3yfPqkdU+nzXb2pqdbX/evr7GSc9/c7INnrdVckNnFszYcKvk4vIPTUtX60Qui+R56yJ+PhZnHP1V+/rkJyW3LXV5t62EeyDZDWhUaJxutvXOuKesr+hKp06rc0y8ZXTXTesWXrIq7t8/HhghAAAAdAgAAIBLJQPH2m/DG2UfJHtleeMXJYDnZZ19/F9d9Cjj888yCFiTjnf7dSjI+87mhLUNiIVdBnu+UI/xtc8sqArqLPiOa6JbXYPYBKyfe8DhPZnbDnxF7+8u1tHGl5d/U3Kv5fq7P15Fnb2z+0qe0u41ybsCWpq66M2DYY9pznkJseBuBAAAdAgAAIBLJQOPNbwe7fkFifbZPD3q8u7v/EnyxJx3JIesjZMC5+1LssGvJYTFC6+TnGdazhGxaBkOTO8tuaEzCyYs+Z7kvi9scKdhgAsyevUM+/hHU38X8brsFR0kh86cictz2ysaVv/Ho/azSZq58F7JnSqT+9pjhAAAANAhAAAASTj+OFr2zOj6isomPdY3ZIDk7fN0z/tB/fXo5Fu6vS55RvsK69HRbZz0433XSs5bSpkAqcU3uETyott18xX7zAL7/UDWifQ/eheIJNg1P+zj69udiHxhnDhjLpOc+YMqyVnWS6zkzdslD1z2keRkF9QZIQAAAHQIAABACpcMvrBazy8o2zTqAlf+P2spw8oJeqzrgMzI+5TbGyTFMkxz+DWdud3dNK2kASSavyBP8vAsvcNDYfd9sgcogZbBf/UVki99eLPkwrZanrjp/vmSS6wycyq9ChkhAAAAdAgAAEAKn2WwoIvOvFxw1UcXuPJf7LMGAk5mE6+PfM2sgxMkV42qCftad5MeRyOnsqA14z0YjHxfOA6z32Phv/+kZPs119Aqg55rT7vRLCDtZBRcJPnkuIslOzOPSn5ukK7kGZSpf39KVs3RnAar0RghAAAAdAgAAEALOssg0MTnWPZ5J8mLK8ZKrv5NoeTOb+6JT+MgOnv1mN0FFVMk95unG3g4/XRYLjfbLzloKB9c0MihEtcO/Y3k8NeDvgd4urpYP12+xcTb8Vnhq4M6L07NMxJ81vkOed7gBa78l9MhLTe2xHsy07pf2nlTaQ58bDzbPwn7eOBfbpW8Y+IiyaPvfk/yX64fJPnRS/Ssm0nZuqGd7ayj99CgJXP1uRZ+LDkdfpKMEAAAADoEAACADgEAADAuzSEo+uMxyT+9cZjk/+zyz4Q8X2W91p0frSqVvOUJfe68vdZ511b9NN/adbDxaiKaI2QtKQweOy5514Iiye8Oe0LyjkA7V9qVrg5N0N0JG1pWay87XH3nRMk+80FiG5di7HkDFfX5kn97ROc9ZFrzCfxB/VX53R5vSe6fEZAcMA2sX04DmdZ9sdHfUXJZ1WjJWb76Rr/PS70avcR1odrasI8HPKK/+w9+Wec0PVawUS+ycwNeOd1d8q8euUFy8Us6VyYd5g3YGCEAAAB0CAAAgEslg+C2XZI33nyJ5OFTx4ddd/nV2yQv7vN2k55j2DN3Sc47qEN3+WU6fJNnUn+nqFbLY/VNgzp8Weuk7zCs2zpv0yHdp072kTw7X5fPjt8yTXKHTfr5RJTHUnWZoTHGdLDKAT+sGiP55Bg9jMaX30EfYK0unPZjXVbWtY/uCBmoj3yQWjrIyaqTfOx93Zmv+Cl7yZ61A6xfy7Jhr12t/KUs++9R6V/vlrxz0q8jXr/2XFvJ97xwm+SiF/dK7ng4de/1pmCEAAAA0CEAAAAulQxs9nBNoZWNMebojzRPMVeYpijksCG0cm1XlUtevUpniq+2Xku5Roc5W/MqmrPWCpexHXdLfvzJqyU77fQnVLhK3zsNnL9Vv5EvfcsEYUI6H75D9in9vPXvOzS9n+Sawbq6wtSn726N/b+lq2uuNSMavb6X9Xem8TUX6YcRAgAAQIcAAAAkoWQAAMlW6+hQ+MScnZJnTNUyZq4nS/IdQ3Ulwvpv9ZWc6WvZhZc6a+XEA0OWSZ6Wd1jy2ZBVPjDfc6NZSBBGCAAAAB0CAABAyQBAKxew3hcdsKaOhxwdCn+wQDdKy+mus+rTba/6prLfMZ6w/rHb6/RPh9famKizC21C4jBCAAAA6BAAAABKBgAQkdej52hUh/RXZXUS2pJq7J8NWg5GCAAAAB0CAABgjMdxOF8WAIDWjhECAABAhwAAANAhAAAAhg4BAAAwdAgAAIChQwAAAAwdAgAAYOgQAAAAQ4cAAAAYY/4P1F7bW+utHi0AAAAASUVORK5CYII=",
      "text/plain": [
       "<Figure size 640x480 with 5 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "First false equation with length 8 in the training dataset:\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAgQAAABICAYAAACJB+2oAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjcuMiwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy8pXeV/AAAACXBIWXMAAA9hAAAPYQGoP6dpAAAliUlEQVR4nO3deZBcx33Y8W/3O+bNzM7sMXsDi8XiPikC4AWaokSRkkKZsixLSmSV40N2XBXJ5UoUO5VKqSpRVSopx0lVXHFJTipxbFmSJVmyTN0UJUoiJZMiSJAgQQJLXAtgd7Hn7OxcOzPvve78MbMACOJa7DGzi/6wUAR237zt2Zl579fdv+6f0FprDMMwDMO4rcl6N8AwDMMwjPozAYFhGIZhGCYgMAzDMAzDBASGYRiGYWACAsMwDMMwMAGBYRiGYRiYgMAwDMMwDExAYBiGYRgGYN/sge+WH1nOdtTFk+rvbuq42/m5AzwztHlJfqYjQrqtMl/IHOALX3mY5tOK1h+eYuQ3tvIbv/sE/e4UG50plJaEiCX5mdfy9o2nbuq42/m1v52fO8DhsxuWsSX1sb//3E0ddzu/9rfzczcjBIZhGIZhmIDAMAzDMIwFTBkYhmEYy08KjYVGorGEKTVjrBwTEBiGYTQQB4UrFM1S4IjqIK4yNeiMFWACAsMwjEWKiBBXqEWdY37+djyMklUeR0obmA1iOCJcfANrPrNuyU5lrEEmIDAMw1ikhFQkpIW1iNUxEeEgERwut/BSsZ8vHr4XK22jXM1SLbr5zN6lOY+xNpmAoAHY3V0EGzqZ2dlEdpPAmwZ3VtPxzAWC00P1bp5hrAhh29U//esJ2uKkd8eoNAv8OMgAkkOK2LiP8/SraL+y7O1plv4Nj7FqN+q/zb6Nl2Y3UAxcAi2RtzD378oAKTRHx3qYy3i0HHaJphWq9kOEBjSLCw4+uYjHGmueCQgaQLi+g7GDCdoeG+H53Y/zp+nNfPfCHgoTnURMQGDcJoTrImJRsntSZDda7PjgIB/oeJn3xs4xHko+9vLHmX69hc3PR1YkIGiRN16E5QiJRPLlMwfIv5zCKQikD/oWbtraAgTExzWpWUXyxfOoyWl0GILSS/Ocv7D4UxhrV8MFBHLPDnLbm0nvtJhbF4AA4QvW/RjiZ/OIY2dQxWK9m7nkhAatBaFW7PJGmGmP83Ssm0i9G2bUnZVMMvXB3ZTaBaWUxpsS9P39MHo2RzgzU+/mLZqIRJCRCJlHdzGzQ6J359jSOcWHO19ghzuOJyw6rJDf2vILvuwcwL9rK+7ILOEbN7e51K2655lP3LjtQoPQRF5oovNUiD2nkL6q9uQXqhZEWMUAWQrQxRIiFqV4cDOlVotCj0BLWGSqglFnVmsrdLQx8WAn03eFdP7cou2VDOLsKGFmtq5ta7iAoLAlydhBwYce/kf+pOtlACbCAg8U/oh2N0HLkAdrMCAAUFqg0Gx1prESgzzl3V/vJhn1Ji1EoomphyrsGRjhn3Uf4m8v3EPl2U4crWENBAQyEkEkE0zcJXjPOw/zu+1Pc4drAaCo/r9ZWHyydRApFJ/f/igtVgvOCQHLmH3f8U3vhsfMjwQ0n8xhXUijyxVQIdR69bfEsUEICAJEc5KJfTal9T5v3ztI0i6TDSIovca2kBFXDKms4VUVItnE3IYWso8UOPPg5xlwfg+nmKQ5nQMTEFRZLc3Q3sbUbpv99w3yUOIYoVYMBUWO++00nYXkiRx6rlTvphrGihC2jf/g25gecHnf7sM82nqEHc4UhxIDvNTeh1WIVy+kq/ziWfyl7YwdtNlzz2k+mnqOPtuHWiBwpT4nTWanRiiX9qck6KXLwL9S4nTh5g6UAlkoV2/kzU2EiQhD749TaQ+qEcNCX575e6MGbM3ebafZGJ/mHclBPFmhpNwFnrBxiQO7yexMMHUnOP0FyhMxnBnJ5r+ZJBw8We/mLbtQK7xkmUJPgmTsxgHocmuYgEDE4/hdzcytD/iNrmfZ7kyjiDIUNHOk2E9sQmGNTBFWln/ucMWJ6lCgJatjgaEWlLSD2ZPk9iZsm9nNLplt8MG2F3jQqwBRetxZno9LlOfUu4mLIwQIyeyAQ/d9o3y0+3kORkLg2hfGlJUn0lugNJ5ASIFexuFza3ZuAQdLVDxKkIpSSrnsfOA0v9b1IkV165N+vrZxRMDWyBgJWaJDli8mMa4JQlDsizN1J3zo4ef4T50v8heZTTw5tZO573cjB+vdwGVWGxFuipYptCTQDfB5bpiAYG5nD+f+icOBPSe5OzJBQtqUtc/vPf37tByK0HPkAuFMBh0E9W7qksv3x/AfyPJwV/UT8H+mH+CJszvpGr9xlrOxNlkdHdDRSvqBMu/YfoJN9iwQJa/K5EIPq6IRvrqlqepGYe3YQuZtKbIH5/jMwA/Y7U4A0es+ps/O8tFtL/JXs/eDWN5h85n/sZDfbogUAZ5dpNn2+Wj382x0phZVpCtEYqHwRICFpqgtpNaoZS78tRKs1lboTDF2n8XH3/MUu6IjvFiGPz/6DsTxJjZNjLN8Yz+NZWdqjJ9tSRAkvbrXEmiYgKDSYhMZyHFn8zDtVvWiUNQVoqcjdD2fRY9PocvlOrdyiQmBsB1KLZK71p1jpzcKwIl8J8WRJqyimR65LQkB7S2U1ifZvH6cx9qOEJeCoq5wNrA4N9eKVVIIP1y9AYEQ+Kk4mS2SLb2T3O9N4onq5UihCLVmPKzgI2iT4AkLR1g0S8EDTYN8tXUfMuqhtFq2TsJ/237zlREvZ6GJSR+HpRm+8Gu3CX8N5Q2IeIxyT5Kgt8zvtLzI6SDGKb+TYCRG6rRGFBYwOrPKrfcyNLcWCKNNJiC4nVmdHVR2rmdmt+ZT3U/SZflAlEwpip2TyEqwei/4xi0RjouMepz4nXa23n2Wf7vh+2xxshz3m3i2sJW/fPwREmeg88VT6Fx+VeYPyFgM2ZFiZH+Mu375KI+ljpCQLrJ2OTzt+5zw2/mjr/0W3qRgz4eO8XDbMT6cOENCutwVyXPfurMce3QPydMFOPTqsrTTE7cWaFi1T61f98t74yrc0cvZD8CjO1+lWbr8NL+TH4ztpOsX0Pr0GcKpdL2buGIOxIfIr4vwUnw/9Z40aIyAQFqEjiDuVWiyqr3ioq6QDkNEAMIPQa29tTbCdam02KhkwBZH44jqfGPMqRB6Gm2ZC8rtRnjVjHvZX+D31z/NLjdHRFic91O8lO2j7XVN4swcajq9OqfPpIVsbaG8qYPCOs17215jhzuOrF0KFYrD5T5+nt1K21FN00iZ04+k2JVoQWmNLSyapUNXJMtLbYLopLtsFzFrEeG4upWNCG4j5RaLvo3j7I6P4AiLs6U2hqda2DheIbgwVu/mLa9QYfmKMJAUdQVLKJqsMo0wAFT3gEBEIsiWZrIbJf9l23fY4U4CHt8r9PJ0djvJIYU4N4Zaa9MFAJYkdATCVkRFNXPYEpJ/v/E7vNC5ia8/9x6anq9zG40VpbdsIDvQxIH1b/BQdBJPuEyGZf7X0IOcP9XBrufGUGMTqFUYDIhIBKuzg6mH+uj7Fyf4QNsJ3hs7hycurSgo6YD/8K2P0PuMIvXCOXAdpv0ooZaEaBQatCI0ve9Vrdgh+cymJ9nuTAARnjm3mabnYrjjk2s+d0BNTeP4Ptb5zXwj388zmW0cz3TiFurf6a37p0oIgXAcVAS2OlO01Vo0HTYxWmzGLmn03Fx1t6616LL1t1YtSapDFtkUmUDVPVwzVloYr+aUtLlFYqI6jO5rmM7HcGYtdDa3KjfmEo6L1dZKcXcPs5sFH+x8iftjJ0hIF0dYqPn/tMablDQdT6NmMlDx39LbXt2plLc3YdtYySRBHDY5U7TUVlbNzXo0jYaI/G2SO6A0QkNYGxZolPGk+t9ypATbIoxoNjnOxXnE2SBGuhTDKilUae0n1833fABGwwSvz61D+ubCd7uptLoUuwUpN3/xaz6C4lSMxJSAsP69iIUSjou1vofMXd30/OEpPtB2ksfiwzjX2GvAm9aoU0PoIEC2tqxsY41lZXW0M7d3PcW+gF4rvJhIGjvlkvjuywSlNTgSfAXRFEf3tlNJhdwdHcKTPj3eLD+Jd1DvHSbqHxDME1wMBgAUglALrDV8T9TRCMUOiRev7q0w3/N5vbSe52YGcIqr7+JfLxYaeZU9XS8meGlrUUvAltv89r35XoviRp8N7jQAeVVmLIzjTtjExpYvo345CS9CeWOKXJ/FR9tOsD96hlhtikxdkYkfohEhF5+nDgKy03Feau2j1Po8zSvY7sgVZYctoQm1qF6bEA2RJzBfRMlC4whF2ABtui7bxo9b4IZ4wuJ8oDgfeDg5VuXI1y2xLLRrg62Ii4CSckj78YbYkrpxAoIrhFoSKrkqs6hvVqUrwey9JR7uO/Omr//d8H7GXuxm01jWDI7eJE8EV61ON7+RSzp0qCDx9dV7pfVmtacIe9qYfbDE5+79Em9zp1FEeN33+FFuN70/84kdOU9QWH0XTZlq5fwjEewds3w48RptVoSbnq2cK5F6zuHozADpfpuuFXz5Oi7rjVTLGgt8NAWlKGlJ+RojHCvNQRGXikRtyrGRF6PqiEMlIbGiZaLC5auze/jKif2khtfolPBVCNtGuRbCUTRLwZFCH88Mb6IjV/9gv2EDghczG5g4nWJLdu1OFyhXEk8UaXPfvEXq6HQzLadBZucaMsHmVrOvXRQOYAn1pkkzLarndEWIi6Ii4EYpt/OjAb62KKgIvyht4WfpzUih31R6NlDVUrQPtJ2kz0nTYWdxG/C3qlJJcgNxOtqm2OSkiUkLX4d8Z/YAT13YRku6jCoUWdat+ZaaEFgtLQSdzYQDc+zrvkBMWlTrAwpm1BzjoeS1SjfH5tYxXkkyUWoiNnnp9dFaY5VBVi71yOUKjfT84bnH3vTvQEvaIwV2x0fY6E6yo7bx0GL3B5gfubpyxOHy3v+VJBpLaHLKYTRs5nBxIy9n11ff/9f5fH553aKaumTmn6mvLYJAIm617sNqJATaFghL4wjJWClJfjpGd8kEBNf06rEN9H9P4ZybpP6/puURRiT9rTNsiEy/6evWqShdTw6jJqev8cj6cUSIJ27thuqgiEmLiPSpdbiqBMRkGU/4xGSAoyXhlcVOrnG+WS2ZDJP8vxP30fTVJFqClpclavoaLeEv/2kH7+4b5H0tR0jKxpunLPYnmTgg+dWu02xz4oRaMa3m+PKrdxF73SM1OkSQy9W7mQsiXBe1sZfMjiY+cccTPBAfxBP2xRv6cGDzZGEXnz9xL5WjzTQNQ2xSkTwycukzrxRWRWNVqjfd+cdaS7Tpz/Wc/uz2i3+XIVhlzfFNFk/du5Vf3vwaj3T/gpyqkFO3HmAqoKIlPtXA9WLQI3R1GgyNd5WxZEeAJwSjgcezhS18/tlfYv0PBKEjrp+MfPCWm7qkNLdxcqglCR2JZQXEhMuZTIrokIudK6zAu/r66h4QCNtGx6Mo+ypvDs2a3H/gRqyKQM9m0Q1St8ERIUUV4Y1KN0cL6/j+yZ0AWAtM8BBCE3ECMpNNdJzTeOkQEXGJjyr+5LlHsSIhbsRHL2AeVClBULFwT0aJjZdBgL5sw3erHKKlYKoYYa5WFEY2UJEIu7uLYGMXk3fYpO6Y4EB8CIBDZc2LpR1Ej3m0HQvQhZsstNNAZNRj4kCS2a2w3Rul2yoDERQaieCZ4jb+7+v3I44m6Dwa4k1XsDMl9NUCH13tSc8/diWWHcYvXJqCEkojyyEIjxknwTfG7uap/m0EShKGt9YWITRCwLs2vMHH2p5DCoWFxhMhIYJvZPdxptjOobE+ymUHy1JveqyUmrliBJVxaXndIjaaR9kSbcvq5+Amgmqj/pTm1splL4O6BwS4DkHSQ0Ua5DfSAGSFutfFvpwnQjLa4sVcPz8c3MHmzyqE1qjIwt8+Wri0BwF2vgiBQkcjtLw+S9P5SHUJplzYXl1aCLQlsAt5rOn8W74v5spgWwTFTvKBS6jlojacWWrBxi5G395E0/2T/MXOL9Jvh4Ta49vZO/nRhW30PFvCOTRIuAoTrkQ8zvT9Pm/bfJ797lQtd6BKoXlichdNTzaROpKD51+tff0qrni5Vqpn6Z2evKwNGoIQ54JN4jUXFYsQxr1FFSDTsjp0/K1fv5PH3vUynvSxUCSkD1ry9TN3MjvUwsbvBLjTc1cvZqUUspJHzhYhk8W2bbBtsORbSwobxg3UPyDoTDFxV5zYuuoN8EI4x/kghjtl4V3Iotf4MpT53upKzYsumUXM+S1VB11LQW59hIn7Q4SyEZXYWxb0igAQcGD7Se5MDOOKkFIDJBZaHR3429dx4ZdidL17mPf3vEKX5XOkkuRUpZMvPXM/rUclbecuEFb81ZVcKwR2fx/lgXY2bZjgwdQJvMsKEV0I5zhc7ub4SDf9pyrYU7mGnBY8/q960QKwNFZBErsgiI8pmo9mQF72Pl7oa1O7UVulAFH2aX+2lU/M/l71hAKUXf1r8qSkc0YRGcsj5iogJdoSb97BVIB2LHQsglQJits6yPfaZAfAb1MQCFM1tcGVKg5OsbYjb53VPSDwU3Fm9/oc7KoW9hkNohya24Q3LbAuTK3KntFCzc+Hzm9MtCpiA7nwRs4PYS7FyigtBFoICusEn37nN0nZeWLircGjqg0te8K/mIhY0nV/20NHK5P7Yuh7Zvnuzq/XltxG+Vquj+9N7Gb9DzWx775IEKyyYAAQlkWlL8XsQIQPdx3jvU2vERGXfuejQZTvzexFnvfwBs+isjfIjajT5+Hzv/JZHBHSIiscKm3gz06+i6lX2mk+fkXv+xZ64lqAKPvI6SydT+bofOoqPfogBK3RFR9hW4i4B1i8KZ4VAmUL8By0ZZHe4ZDd7fO79z7Db7a8wGToXvF+/zcLbquxvPyKjVfQ4Nc/LK7vlVEIwqhFLFVkXTQDVJePtVhFQhfwIgirkQZ4l8f8fGg4n0HeYE+4pC1cEXJP4gzRXT5PfGonWoNlLSzHQUpNPFJhYjJJ29PNNI0GxF4YIruvk9FHfexISMTzb/r+JwRsaL1At5PBE/41pgKqUfd8MLASyWg3Y64viXgkzQf7X8O+bPnas5lNHDvVy5a0j16FwQBUixe98RGX/p2jPNT0Oh2WwrosIPhS+j6e/+t9rB8so2Yy182VEVGPqTsF7rZZWmSFG5VHXkrzxY18LVlnz/CR/sO82raOQ1v6a3P4t1aeXNRWwhSPt9L78ySyorDK6k3JsABCa9AgyyGVFpfhRyzCloBEqoAAQiURte6/UgKlJAPtQzyUnOCO6DkKStZyEup/o7mWg00nyG+N8PO2u1fwlW0sfs4lPh5WpzfrrO5dpdCVdCQKdLpZoDqE7gm/mi3u2Gt+Hmw+q7iRM259beGIgB2RUfZ65/l46me3dB5PhAzYHp/PruNPh34NZ84iWiyS75F86p4fsjUyRr89c3HjlxtRWtSWfTX2pkNXU0rZ/MttT3PAG8KqbdITasWZbBvesIudy6BWYTCAEIh4jPvvGuQ/r/827dLFER5wqazxi1N99HztJDqXv+FmNMJxYGOBB/tOEVvhl/jSplaSNqvIY02v8oHEKzi9i3tdrNoKgd9u/gijoxuxCxqnqGuJgG893i5riu2S+w4e42DLKT7QdAwLKF2lGX5tQzcfSbk2lNBIXaorlxfucqaItxzmJ4l76tSiOqjlPc3P5ciihTdVQjfAjrz1CwiEQNgOc+0Wnx74AVudKSDCWJDglWIfkRmNHh1HzdX/l2Rc4msLtcB111IoXBRp5fFyuY3vTO4lPqoRCsoHd1Ds1cRqSwGL2q7tAnfzP2M1BQMyHkf0ryPfK9nsjtMmK4Ta5pmSzc8KO8g+3cXG72UQZy/Uu6kLJy1K7ztAZqvN+1serwUDl0Y/RoMyj+f3MDrcRjI3hrpefpAQWJ0dhOs72NEzwYPJQWKyei6JqMtIj49Eac2tjQtcIrWmJDS/2fssT//zNOXQvu5eBoGySDglHm19lRZZJKeqx6prvO8b+fOgcwWaT80xOekxo0rEpWCXm6uOCN8mSps6GH7I4UDfaQCcWYlzeoww99ak6JVW3xECKQii8I7oNLFa6d+ijjBZSWDPgVqFS61uBwu94ITawhKaknZ4udDPmZkU0Uy1uEdug0vQGhCvBQSrsbe/EMKLUO5JUGnRpGQRT1RHh46Xe/jxxDaazyjUy6/Xu5kLJwTSdchstsnu9NnkTlzMG5gf/Uorl3+c2YyddqrTBDdav9+coJzy2BafZpM7gYN1Mfk2RIKuDauvgEsjeUv03tSw3xvmXbHh6y6gtC4+X01aVUcrqoHJ6vyM6FIJeyqPXYgyHQo6LE2rjNIAeb4rptJiIwcKbG8aB8AqQTiVrk4R1lndpwyMtc9C0yIrjAQtfPXYfpzBGL3PnWf2rl7CX53h0Z6zbHXH13wwAKB7Ohn6ZYfuXeP02yGR2nTBXw0dpPLNDrqOZRoky2FhrM0b8de1IN+V5tPbfsJedwaIodCUtc9oGPLlmQc4/vfb6X0juGH1UuG6TD7QSWYb/EFykK22jyUcAkJKOiDjR3FzGmuucefHb6SkLaZvulhVdRoA3rqj4WqiCkXk+VHiw5381cz9PJx4jYeit9EosBBUmiSbO6cYiEze+PgVZgICY0VIwNc2YcalaQbU+CRC93Kga5g74ueJiYAiEDbCCoBlIhyXoMXD68/xttQoMeng65DxsJpoOfBGBTmdXZUBgUrEKKVcdnec4X3xk7RZkYsjA75WnA+SDOa6aD0REDufu25+hPQ8RHOS/HqB3lCkz5kmVtufoqh8TgQOZ/NtuHmFnPNX5e8Lqjf2RqmHsGJUiCoWcfOawWwXu6PDwG0SEAiBsCzCCGxsStNm5d9S3Kve1u7V12hMtkY51R6gFjBTiZJT3tINxTYoGYuhtw8wvSfKp3Z9nzu9c0gsHi9087kz7yD5gkfkpWOrdplt0BKh2C7p8WZplu6bKpeOhfC50Yd49fUN7Dp0FnW9TbeEoPSOPcxuctj5yAk+1HWYjXYFaoVhn5rr5o+f+HWaj1v0/Ow4ehUWezLAmwk5cno9m5sm+fXEeL2bsyKE6yKTSQq9gn/X9UMAxkOQDTTIZQKCBjE/N9rIqw2WxHwmtVXtGQVq4UmKq5FwHUpdMUopwe7ICB1WhRklOJQfYOR0O71jISqXu+FQeqOqJG1KKUGrXXxTIiFUE0UHpzqJTFqozCzqymxqaSEcG6u1BZ2Ik9nqkt2sONh2mv2R88QuO99Y0EzipEXzkE+YnlmVyzINEKGGskVZLWxn0tVMRj3obMNPKnqsKOeCOU75rcgKDVO0zAQEdVYtYnJpY6LbbADxtiESCcbucQh3FtjklJgOJY8XdvL4L/az88/SMD1DGDRQV2EhhGBqr03PO4e5P37iLd8+5Xcgf9pC9wkffZXnaHe2ozpbOffeNgp7Snx831P8SvJleq2QmHCwLlt6fKzQy/pvjaLGJlbnskwDAOUKZNwnbtd/7f1K0et7GHlvG4ktaQC+MnuAr5zeT2I4vOrnoh5MQNBgwgaJFI2lIyIRdCJGuSOkpzVHREjKWjJcacXOWjA+ueqX14ZRTU8sW1s+Wi1vrNDkVZnJIImb1VglhdXdBZasFjSLuQRNLvkOh7mUJL+rzL6B8zzYdJzdjotC4+uQ0aDMeBjlG7MHeOLETramz9xw/4KVshKFslZzEuG1hI4gGq/QbM3Vuykrx5YEUYg51Zv/WCVJdjpOa7FxrvkmIKiz6uY6sjpVoNXanzK4zQjbxurtptDfTP+OMd7ZeQIHi2kV5bXZHpycqNbrWKVTBfOUA+2RfK009vw6ecWgH2Gw2I1T0ISeJP1gH8UOSW5LSHx9jvdvfIE742c5EBkhJsATspZAWF1iWNYBX5y9i++M7CbxnxJsOzdFMJut63O93HyJ4uVwMa9GrL2goJKQ3Nt7ll3RkXo3pW4GZ7uInnZxM42zvN4EBA1kPhgotWvEvt3IXBFRqqBqpZB1+fYZXlsrtNIwV8IqK6RUeLXtbn1tky17WD7oUFWPW8VEALN+9C0b7CRkhe2xMb57l0D6NkGTgmSZ9T1p7mgb5cHEIJucNBvsN29cW9YBR33BiUoff3PsHvSZOG0jI6jp9IrlDTji2j23+SCgrC1Ktc20lrok8/x23J4IcYRaU4m3VkVzrtDKdHMT0DiVXVfSbNnDS2usYqVh1hqYgKAB9d4xxumgm8SZJLEpReJYGpGeRU2nG2auybhJKiQYG8ftaqNyWS8vE8aYzDbhFUH7C6sJ0YjsguBMNkWmIwpUUGgkki2OzUDyFB/76H+/eKwUAqeWLVPND7i0TZ1CUdIBORXy52Pv49BwPxs+a+GePEtwYfzGmxktoYS8/s+SQDrwOO+nKKgIJV1NkFvsLoq+tpFC0edMk5Ql2uwsjrhGaehVykuHnDzRw0vJfn47OVrv5tTFVKaJ/jcqyHSuYV7b+gYESuPmNH+b3cL+6BD73LWfbX45Jxfw+lAvXV4Omocufv3h7kF+tB+Ge1vJzLj055vx/ADSmbq11Vika/VqV/fAQJXWRKc0Z892MLKhFbxLy8gkEoQiJpw3f61mfh22QjEZlpkKHf5s/D28MtlD7rUU0TGBMzpWrYi4wvk1z5XWXfN7rghxRMAXxw9yeGQ95VkPUZLVyoyL7cir6jlSG2foS87wq50vkbLzlJS76I27Ni6yaUtGV/+oWq7J7SBIRJjb4LMpVuC1SoCaieBOzqIbJB8G6hkQaI0OfKJTIZ9940Ee60+xr/OlujWnHtzxHM2HOngu0Q99l77+6fajfLr9KEM7ihz32/n0Gx+nKx1HjNprojdprD3NpyooO8Ibd/fALa4rP+knOTy3kUP/sJeeZ+foeuU44cwM9cqu+ObUvmt+L2pVM+QP/XwH634cEB+cRI2OgWUhrFtfK6S1Bt8Hx2HqI3t4bSCFelCyIZ4m40cXvUT3o1sW9fAlF66x3IjrKbW7vH3vMTrcPE8WduGNWnDqPKqBpoLrPmUgK4piMUImiNW7KSsvPUvq9QTne5P86dZdPNA0yMFIyKsVn1N+B/9z6Nc4N5pi48kK1tgM4XXKxBoNSgis5iR+c5Su6DhdTnW+dDJIUp6Ikcyujd6RN5KlVTbzxPBOdkZHeXfsHK3Su+5j3vArPDc3wPem9nD0Qg/lqShOxmLdyz7uuTRqrr4Z6C99e1f1L7pamE6E1b8jqFZjldD1Rkj0fI6gPYHqbUE78i1ljG/W/L3RyVaQ5YDmM2ViEzZn0ps54W1emg1s7luCcxi3xCopTmQ6KCUcmuwyMgRd8Rtq75H6BgRaI31FmHfIVG6/atjh5DTOs1lSXXfyhe13o7YJDkZe4/nSAD9Jb2fqR71seMXHO3yaYGq63s01boGwLERLM5UWh77YDL32DJYQjPtJvFELL7M2ckL0mfN4k2nOntzKVxJ3s7d/hNYbdGZfLffypZF7GPnHdaz7aYXIcHU/BjWbI2iAkbD+/z1YneoJQ3TFv+pSR+G44DqU37mL2QGHMEK1UE9tSHwhtAUIiI67RLKK5p8PYY2N070UT2ben/zrpTybsQB2KeT8VBIpNP2xNCJovPyhuo8QuMNpun/cw7N6C093P83pcme9m7RytEJVfFqOTCPCNr7e8S6+lHoX7iw4eU3v8QLOhQwq3zjLUoyF0WGIzswSO9/E1356Hz/eupUn7vhr7oid4+/3Zcnkk/TGYtVVJKs4YVRVfGS+wIbvh4y9PMDHuj6FukFJWycP3pRm/fkykTOT6GwePTfXOD2mig+OjWhtQbUnyexoAkBcviJEgBaCiV8K6Ru4QIs3hyuDW1om6FohEs0r471MZaIUOzfhpQfQ1qXRg7XCna0QOx/n/I7WejdlxVhzAWI8xmgxxeOZJlrHG290sO4BgbowTtszAfl1/fzi4Bam/ThlZbEC+33Un9agQ8JjJ2g6Bk1XOWT13iIMALQmzOaxLkzR+XySqUo7ub2KdfYM7+w/yQ/f2FfduCgMYRUHBKgQVQpxv38IF1joZb4Rn7nWGiEtVHOc/IYYEwdDECCCy+7OtZGARw+8wic7fkyXVU2gvJWiNRHhIBH8Q0cLLxX7+SL3YqVtlKsXn6jYYKxChehEjKlivN5NWTFyzicyLVF5SThtE51uvHd9/QOCig/pGdY/meRbow8hQpChJnVkvG7JRIaxpFSIyszS9twYiTPNfPDkHyNCiOQ0A0N5VL7QOL1i46Jzf7AX5UKlVSE7S3zijmew0JQu239/fm+AfbEhANIKctzaunJZC4vW2ZpE0xxt9xTIhR6WUEu4+dEfLdF5FkdOzNB2LMKJg8284VewGmvkfFmIc2P0fV+CJdC2xB6ebrhAuO4BwXw5TI4cI3nk0pfN5XHtsa6z0ctap8tlgtNDiNPQ/uwV36tPk4wbkPdkiFghm5NZdjdf4JMtx4DqpkkXj6nVWUiHIUVtUdIWxUWO7zfLMh3WHPsjGRxR2/VxjdVtUPkCzkgae3odr5Z7kY2TaL9swpkZmJm5+O9GCwagEQIC47ZgCZAokGtv+NNYm/7j7m9jCYUnfGKyzHDoX+Wo6o3a19ai9wiY5yNRWlAJ9ZIH0aklPdutU4Ui+D5bvhDjc09/hN7XRhryBnm7MQGBsSIKSpIJY1CWyPnrqgkMjAb29ugFQq3xAV9DboVK9SotLm1TvLYGBi6p5ZzwynG8Vxqzt3w7MgGBsawSskJOufzXsffy/MgGNnwPomM5cB1Cx0QERuOaDC+tm1yq3r9hNDITEBjLyqp1cUYLzRRno3iTJeRMHiGEGSEwGtqVhZoMY60TWq+xbBXDMAzDMBbMhMCGYRiGYZiAwDAMwzAMExAYhmEYhoEJCAzDMAzDwAQEhmEYhmFgAgLDMAzDMDABgWEYhmEYmIDAMAzDMAxMQGAYhmEYBvD/AQE8MsqzGcUvAAAAAElFTkSuQmCC",
      "text/plain": [
       "<Figure size 640x480 with 8 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "true_train_equation_with_length_5 = true_train_equation[5]\n",
    "true_train_equation_with_length_8 = true_train_equation[8]\n",
    "print(f\"First true equation with length 5 in the training dataset:\")\n",
    "for i, x in enumerate(true_train_equation_with_length_5[0]):\n",
    "    plt.subplot(1, 5, i+1)\n",
    "    plt.axis('off') \n",
    "    plt.imshow(x.transpose(1, 2, 0))\n",
    "plt.show()\n",
    "print(f\"First true equation with length 8 in the training dataset:\")\n",
    "for i, x in enumerate(true_train_equation_with_length_8[0]):\n",
    "    plt.subplot(1, 8, i+1)\n",
    "    plt.axis('off') \n",
    "    plt.imshow(x.transpose(1, 2, 0))\n",
    "plt.show()\n",
    "\n",
    "false_train_equation_with_length_5 = false_train_equation[5]\n",
    "false_train_equation_with_length_8 = false_train_equation[8]\n",
    "print(f\"First false equation with length 5 in the training dataset:\")\n",
    "for i, x in enumerate(false_train_equation_with_length_5[0]):\n",
    "    plt.subplot(1, 5, i+1)\n",
    "    plt.axis('off') \n",
    "    plt.imshow(x.transpose(1, 2, 0))\n",
    "plt.show()\n",
    "print(f\"First false equation with length 8 in the training dataset:\")\n",
    "for i, x in enumerate(false_train_equation_with_length_8[0]):\n",
    "    plt.subplot(1, 8, i+1)\n",
    "    plt.axis('off') \n",
    "    plt.imshow(x.transpose(1, 2, 0))\n",
    "plt.show()"
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Building the Learning Part"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To build the learning part, we need to first build a machine learning base model. We use SymbolNet, and encapsulate it within a `BasicNN` object to create the base model. `BasicNN` is a class that encapsulates a PyTorch model, transforming it into a base model with an sklearn-style interface. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# class of symbol may be one of ['0', '1', '+', '='], total of 4 classes\n",
    "cls = SymbolNet(num_classes=4)\n",
    "loss_fn = nn.CrossEntropyLoss()\n",
    "optimizer = torch.optim.RMSprop(cls.parameters(), lr=0.001, weight_decay=1e-4)\n",
    "device = torch.device(\"cuda\" if torch.cuda.is_available() else \"cpu\")\n",
    "\n",
    "base_model = BasicNN(\n",
    "    cls,\n",
    "    loss_fn,\n",
    "    optimizer,\n",
    "    device=device,\n",
    "    batch_size=32,\n",
    "    num_epochs=1,\n",
    "    stop_loss=None,\n",
    ")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "However, the base model built above deals with instance-level data (i.e., individual images), and can not directly deal with example-level data (i.e., a list of images comprising the equation). Therefore, we wrap the base model into `ABLModel`, which enables the learning part to train, test, and predict on example-level data."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "model = ABLModel(base_model)"
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Building the Reasoning Part"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In the reasoning part, we first build a knowledge base. As mentioned before, the knowledge base in this task involves the structure of the equations and a recursive definition of bit-wise operations. The knowledge base is already defined in `HedKB`, which is derived from `PrologKB`, and is built upon Prolog file `reasoning/BK.pl` and `reasoning/learn_add.pl`.\n",
    "\n",
    "Specifically, the knowledge about the structure of equations (in `reasoning/BK.pl`) is a set of DCG (definite clause grammar) rules recursively define that a digit is a sequence of '0' and '1', and equations share the structure of X+Y=Z, though the length of X, Y and Z can be varied. The knowledge about bit-wise operations (in `reasoning/learn_add.pl`) is a recursive logic program, which reversely calculates X+Y, i.e., it operates on X and Y digit-by-digit and from the last digit to the first.\n",
    "\n",
    "Note: Please notice that, the specific rules for calculating the operations are undefined in the knowledge base, i.e., results of '0+0', '0+1' and '1+1' could be '0', '1', '00', '01' or even '10'. The missing calculation rules are required to be learned from the data. Therefore, `HedKB` incorporates methods for abducing rules from data. Users interested can refer to the specific implementation of `HedKB` in `reasoning/reasoning.py`"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "kb = HedKB()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Then, we create a reasoner. Due to the indeterminism of abductive reasoning, there could be multiple candidates compatible to the knowledge base. When this happens, reasoner can minimize inconsistencies between the knowledge base and pseudo-labels predicted by the learning part, and then return only one candidate that has the highest consistency. \n",
    "\n",
    "In this task, we create the reasoner by instantiating the class `HedReasoner`, which is a reasoner derived from `Reasoner` and tailored specifically for this task. `HedReasoner` leverages [ZOOpt library](https://github.com/polixir/ZOOpt) for acceleration, and has designed a specific strategy to better harness ZOOpt’s capabilities. Additionally, methods for abducing rules from data have been incorporated. Users interested can refer to the specific implementation of `HedReasoner` in `reasoning/reasoning.py`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "reasoner = HedReasoner(kb, dist_func=\"hamming\", use_zoopt=True, max_revision=10)"
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Building Evaluation Metrics"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Next, we set up evaluation metrics. These metrics will be used to evaluate the model performance during training and testing. Specifically, we use `SymbolAccuracy` and `ReasoningMetric`, which are used to evaluate the accuracy of the machine learning model’s predictions and the accuracy of the final reasoning results, respectively."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "metric_list = [ConsistencyMetric(kb=kb)]"
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Bridge Learning and Reasoning\n",
    "\n",
    "Now, the last step is to bridge the learning and reasoning part. We proceed this step by creating an instance of `HedBridge`, which is derived from `SimpleBridge` and tailored specific for this task."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "bridge = HedBridge(model, reasoner, metric_list)"
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Perform pretraining, training and testing by invoking the `pretrain`, `train` and `test` methods of `HedBridge`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "# Build logger\n",
    "print_log(\"Abductive Learning on the HED example.\", logger=\"current\")\n",
    "\n",
    "# Retrieve the directory of the Log file and define the directory for saving the model weights.\n",
    "log_dir = ABLLogger.get_current_instance().log_dir\n",
    "weights_dir = osp.join(log_dir, \"weights\")\n",
    "\n",
    "bridge.pretrain(weights_dir)\n",
    "bridge.train(train_data, val_data)\n",
    "bridge.test(test_data)"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "ABL",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.8.13"
  },
  "orig_nbformat": 4,
  "vscode": {
   "interpreter": {
    "hash": "fb6f4ceeabb9a733f366948eb80109f83aedf798cc984df1e68fb411adb27d58"
   }
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}