diff --git a/.gitignore b/.gitignore
index 688cb4c32cebf7e1fb9fe6cced2ec94facfcece8..1d347b39534bbf753ee9c0c4b9db689df57a6b56 100644
--- a/.gitignore
+++ b/.gitignore
@@ -10,6 +10,8 @@ rank_zero_case.*
 !rank_zero_case.ipynb
 other_P_choice.*
 !other_P_choice.ipynb
+benchmark.*
+!benchmark.ipynb
 filtered_sage.txt
 _minted-main/*
 sage-plots-for-main.tex
diff --git a/benchmark-results.tsv b/benchmark-results.tsv
new file mode 100644
index 0000000000000000000000000000000000000000..f8b7e2e8ab367e5ec4207fac5fa904449691156c
--- /dev/null
+++ b/benchmark-results.tsv
@@ -0,0 +1,4 @@
+theorem number	ns/iter
+#5.1	2,172,454,393
+#6.1	179,422,048
+#6.2	108,542,166
diff --git a/benchmark.ipynb b/benchmark.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..38fce5443c119f1b6c13d717f7c4aef9a5d28f0f
--- /dev/null
+++ b/benchmark.ipynb
@@ -0,0 +1,135 @@
+{
+ "cells": [
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "id": "6cefb60b",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "import pandas\n",
+    "import matplotlib.pyplot as plt"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 2,
+   "id": "d256aa1d",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "<div>\n",
+       "<style scoped>\n",
+       "    .dataframe tbody tr th:only-of-type {\n",
+       "        vertical-align: middle;\n",
+       "    }\n",
+       "\n",
+       "    .dataframe tbody tr th {\n",
+       "        vertical-align: top;\n",
+       "    }\n",
+       "\n",
+       "    .dataframe thead th {\n",
+       "        text-align: right;\n",
+       "    }\n",
+       "</style>\n",
+       "<table border=\"1\" class=\"dataframe\">\n",
+       "  <thead>\n",
+       "    <tr style=\"text-align: right;\">\n",
+       "      <th></th>\n",
+       "      <th>theorem number</th>\n",
+       "      <th>ns/iter</th>\n",
+       "    </tr>\n",
+       "  </thead>\n",
+       "  <tbody>\n",
+       "    <tr>\n",
+       "      <th>0</th>\n",
+       "      <td>#5.1</td>\n",
+       "      <td>2172454393</td>\n",
+       "    </tr>\n",
+       "    <tr>\n",
+       "      <th>1</th>\n",
+       "      <td>#6.1</td>\n",
+       "      <td>179422048</td>\n",
+       "    </tr>\n",
+       "    <tr>\n",
+       "      <th>2</th>\n",
+       "      <td>#6.2</td>\n",
+       "      <td>108542166</td>\n",
+       "    </tr>\n",
+       "  </tbody>\n",
+       "</table>\n",
+       "</div>"
+      ],
+      "text/plain": [
+       "  theorem number     ns/iter\n",
+       "0           #5.1  2172454393\n",
+       "1           #6.1   179422048\n",
+       "2           #6.2   108542166"
+      ]
+     },
+     "execution_count": 2,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "bench_results = pandas.read_csv(\"benchmark-results.tsv\", delimiter=\"\\t\")\n",
+    "\n",
+    "# parse second column as integers (removing commas)\n",
+    "bench_results[\"ns/iter\"] = bench_results[\"ns/iter\"].map(lambda s: int(s.replace(\",\",\"\")))\n",
+    "bench_results"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "id": "131e92cb",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "image/png": "iVBORw0KGgoAAAANSUhEUgAAArMAAAGbCAYAAADX8BjdAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjguMiwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy8g+/7EAAAACXBIWXMAAA9hAAAPYQGoP6dpAABUxUlEQVR4nO3dd3QUZd/G8WshIYU0ElJpAQSkSZVeBSmRLiC9qzyCggGECBqaIEUEleaRog9VpTyISJESQBHp0qQZIEBiKEoIJXXePzjZ1yWFJAY2C9/POXt0771n5jebHXJl9p57TIZhGAIAAABsUB5rFwAAAABkF2EWAAAANoswCwAAAJtFmAUAAIDNIswCAADAZhFmAQAAYLMIswAAALBZhFkAAADYLMIsAAAAbBZhFk+kxYsXy2QymR92dnYqXLiw+vbtq8uXL1u7vFynUaNGFu+Xvb29AgMD1b9/f124cMHa5UmS+vTpIxcXF2uXkWmNGjVShQoVrF2G+Vg4f/68tUsxGzt2rEwmk0VbYGCg+vTpY9F26NAhNWzYUO7u7jKZTJo5c6YkaevWrapevbry588vk8mktWvXPp7Cs2HSpEmZru/OnTsaO3asduzYkeq1lPfs2rVrOVsg8ASws3YBwKO0aNEiPfvss7p796527typyZMnKywsTEePHlX+/PmtXV6uUqJECS1dulSSFB8fr2PHjmncuHHasmWLfv/9dzk7O1u5QmTHSy+9pD179sjf39/apWRozZo1cnNzs2jr16+fbt++rRUrVqhAgQIKDAyUYRjq3LmzSpcurXXr1il//vwqU6aMlap+uEmTJqljx45q167dQ/veuXNH48aNk3T/jyEAmUOYxROtQoUKql69uiSpcePGSkpK0oQJE7R27Vp17949zWXu3Lnz2ILb49zWwzg5OalWrVrm5w0aNJCjo6P69++v3bt3q1mzZlasznbkpp+pJHl7e8vb29vaZTxUlSpVUrUdO3ZMr776qlq2bGluu3z5sm7cuKH27durSZMmObLthIQE8zc4yJzc9jnH041hBniqpIS1lK/OU766Pnr0qJo1ayZXV1fzL8gbN27ojTfeUKFChZQvXz6VKFFCo0ePVlxcnMU6//77b/Xv31+enp5ycXHRSy+9pD/++EMmk0ljx44190v5mvDgwYPq2LGjChQooJIlS0qS9u/fry5duigwMFBOTk4KDAxU165dU33Fn/KV8bZt2/Tqq6/Ky8tLbm5u6tWrl27fvq2oqCh17txZHh4e8vf31/Dhw5WQkJDt98vd3V2SZG9vb9F+5swZdevWTT4+PnJwcFDZsmU1e/Zsiz47duyQyWTS8uXLNXr0aAUEBMjNzU1NmzbVqVOnUm1r48aNatKkidzd3eXs7KyyZctq8uTJqfqdPXtWQUFBcnFxUZEiRTRs2DCLn8n58+dlMpk0bdo0TZkyxfyeNmrUSKdPn1ZCQoJGjRqlgIAAubu7q3379oqOjrbYxsqVK9WsWTP5+/vLyclJZcuW1ahRo3T79m2Lfhl9ftKyZs0aOTs7a8CAAUpMTEy3X1pfuUv3z9b984xdcnKyJk6cqDJlysjJyUkeHh567rnnNGvWLHOftIYZpAyB2Ldvn+rXry9nZ2eVKFFCH374oZKTky22efz4cTVr1kzOzs7y9vbWoEGD9P3338tkMqX5dfiDvv/+e1WuXFkODg4qXry4pk+f/tB9Tqk5MTFRc+fONQ9/GTt2rAoXLixJGjlypEwmkwIDA83ryMrn8r///a+GDRumQoUKycHBQWfPnpUk/fjjj2rSpInc3Nzk7OysunXrauvWrRbrSDmWjx8/rq5du8rd3V2+vr7q16+fbt68ae5nMpl0+/Ztffnll+Z9SO+M6/nz581/dIwbN87c/8HPwZ9//pnhNiXJMAzNmTNHlStXlpOTkwoUKKCOHTvqjz/+SLXdhQsXqlKlSnJ0dJSnp6fat2+vkydPWvTJ6HMeHx+viRMn6tlnn5WDg4O8vb3Vt29fXb161WIdgYGBatWqldavX68qVaqYj6v169dLuv8zL1u2rPLnz68aNWpo//79Fsv/8ccf6tKliwICAuTg4CBfX181adJEhw8fTvP9xNOFP0PxVEn5hfXPM1Xx8fFq06aNXn/9dY0aNUqJiYm6d++eGjdurHPnzmncuHF67rnntGvXLk2ePFmHDx/W999/L+l+mGjdurX279+vsWPHqmrVqtqzZ49atGiRbg0dOnRQly5dNHDgQHM4On/+vMqUKaMuXbrI09NTkZGRmjt3rp5//nmdOHFCBQsWtFjHgAED1KFDB61YsUKHDh3Su+++q8TERJ06dUodOnTQa6+9ph9//FFTpkxRQECAgoODM/X+pASslGEG48ePV4kSJVSnTh1znxMnTqhOnToqWrSoPvroI/n5+WnTpk166623dO3aNYWGhlqs891331XdunX1xRdfKCYmRiNHjlTr1q118uRJ5c2bV5K0YMECvfrqq2rYsKHmzZsnHx8fnT59WseOHbNYV0JCgtq0aaP+/ftr2LBh2rlzpyZMmCB3d3e9//77Fn1nz56t5557TrNnz9bff/+tYcOGqXXr1qpZs6bs7e21cOFCXbhwQcOHD9eAAQO0bt0687JnzpxRUFCQhg4dqvz58+v333/XlClT9Ouvv2rbtm0W20nr85OWjz/+WCNGjNDYsWM1ZsyYTP08Hmbq1Knm9TVo0EAJCQn6/fff9ffffz902aioKHXv3l3Dhg1TaGio1qxZo5CQEAUEBKhXr16SpMjISDVs2FD58+fX3Llz5ePjo+XLl2vw4MGZqm/r1q1q27atateurRUrVigpKUlTp07Vn3/+meFyKUMjateurY4dO2rYsGGSpMKFC6tSpUrq0KGD3nzzTXXr1k0ODg6Ssv65DAkJUe3atTVv3jzlyZNHPj4+WrJkiXr16qW2bdvqyy+/lL29vebPn6/mzZtr06ZNqf5Qefnll/XKK6+of//+Onr0qEJCQiTdD4iStGfPHr3wwgtq3Lix3nvvPUlKNZQihb+/vzZu3KgWLVqof//+GjBggCSlOqv+sG1K0uuvv67Fixfrrbfe0pQpU3Tjxg2NHz9ederU0ZEjR+Tr6ytJmjx5st5991117dpVkydP1vXr1zV27FjVrl1b+/btU6lSpczrTOtznpycrLZt22rXrl165513VKdOHV24cEGhoaFq1KiR9u/fLycnJ/M6jhw5opCQEI0ePVru7u4aN26cOnTooJCQEG3dulWTJk2SyWTSyJEj1apVK4WHh5uXDwoKMn9+ihYtqmvXrunnn3/O1GcdTwEDeAItWrTIkGT88ssvRkJCgnHr1i1j/fr1hre3t+Hq6mpERUUZhmEYvXv3NiQZCxcutFh+3rx5hiTj66+/tmifMmWKIcnYvHmzYRiG8f333xuSjLlz51r0mzx5siHJCA0NNbeFhoYakoz333//ofUnJiYasbGxRv78+Y1Zs2al2q8333zTon+7du0MScaMGTMs2itXrmxUrVr1odtr2LChISnVo3Tp0sbJkyct+jZv3twoXLiwcfPmTYv2wYMHG46OjsaNGzcMwzCM7du3G5KMoKAgi35ff/21IcnYs2ePYRiGcevWLcPNzc2oV6+ekZycnG6NKT+rB38mQUFBRpkyZczPw8PDDUlGpUqVjKSkJHP7zJkzDUlGmzZtLJYfOnSoISnV/qRITk42EhISjLCwMEOSceTIkVQ1Pfj5MYz772n58uWNpKQkY/DgwUa+fPmMJUuWpLt//1SsWDGjd+/eaa6zYcOG5uetWrUyKleunOG6Uj4z4eHhFuuRZOzdu9eib7ly5YzmzZubn48YMcIwmUzG8ePHLfo1b97ckGRs3749w23XrFnTCAgIMO7evWtui4mJMTw9PY0Hf/2ktc+SjEGDBlm0pfx8p02blqqmrHwuGzRoYNHv9u3bhqenp9G6dWuL9qSkJKNSpUpGjRo1zG0px/LUqVMt+r7xxhuGo6Ojxec4f/78af4s03L16tVU/25kdZt79uwxJBkfffSRRb+IiAjDycnJeOeddwzDMIy//vrLcHJySnV8Xrx40XBwcDC6detmbkvvc758+XJDkrFq1SqL9n379hmSjDlz5pjbihUrZjg5ORmXLl0ytx0+fNiQZPj7+xu3b982t69du9aQZKxbt84wDMO4du2aIcmYOXNm2m8cnnpP9TCDnTt3qnXr1goICMj2FbFff/21KleuLGdnZxUrVkzTpk3L+UKRbbVq1ZK9vb1cXV3VqlUr+fn56YcffjCfmUjx8ssvWzzftm2b8ufPr44dO1q0p3zll/K1Y1hYmCSpc+fOFv26du2abk0PbkuSYmNjNXLkSD3zzDOys7OTnZ2dXFxcdPv27VRf+UlSq1atLJ6XLVtW0v0zWg+2Z3Y2gpIlS2rfvn3at2+f9uzZo2XLlsnJyUlNmjTRmTNnJEn37t3T1q1b1b59ezk7OysxMdH8CAoK0r179/TLL79YrLdNmzYWz5977jlJ/z/U4+eff1ZMTIzeeOONVFe4P8hkMql169ap1pfWPgYFBSlPnv//Jy6j90iSLl68aG77448/1K1bN/n5+Slv3ryyt7dXw4YNJSnNn0daP1Pp/vvVrl07LV26VJs3b053nHZ21ahRQ0eOHNEbb7yhTZs2KSYmJtPL+vn5qUaNGhZtD76XYWFhqlChgsqVK2fRL6PPd4rbt29r37596tChgxwdHc3trq6uqX6G/1Z2PpcP/sx+/vln3bhxQ71797ZYPjk5WS1atNC+fftSDTNJ67N97969VMNWctLDtrl+/XqZTCb16NHDYj/8/PxUqVIl89CQPXv26O7du6mGMRQpUkQvvPBCqqEVUur3bP369fLw8FDr1q0ttlW5cmX5+fmlGoZSuXJlFSpUyPw85dhr1KiRxfjblPaUz6Knp6dKliypadOmacaMGTp06FCq4TB4uj3Vwwxu376tSpUqqW/fvun+MsrIDz/8oO7du+vTTz9Vs2bNdPLkSQ0YMEBOTk6Z/hoOj9ZXX32lsmXLys7OTr6+vmle0e3s7Jzqq7/r16/Lz88vVbjy8fGRnZ2drl+/bu5nZ2cnT09Pi34PhuV/SquGbt26aevWrXrvvff0/PPPy83NTSaTSUFBQbp7926q/g9uL1++fOm237t3L91a/snR0dF8sZx0/w+BRo0aqVChQnr//fe1fPlyXb9+XYmJifr000/16aefprmeB6cO8vLysnie8rVwyn6ljK1LGQuZEWdnZ4tglLK+tPYxK++RJPM6YmNjVb9+fTk6OmrixIkqXbq0nJ2dFRERoQ4dOqT6eaT1+UkRHR2tiIgINW3a1GKoRk4JCQlR/vz5tWTJEs2bN0958+ZVgwYNNGXKFIufZVoe/LlI99/Lf+7f9evXVbx48VT9Mvp8p/jrr7+UnJwsPz+/VK+l1fZvZOdz+eBxmDL04cE/YP/pxo0bFrOgPOyz/Sg8bJt//vmnDMNI92dUokQJSTL/G5bWv0cBAQHasmWLRVtan/M///xTf//9t/kYetCD73l2j0mTyaStW7dq/Pjxmjp1qoYNGyZPT091795dH3zwgVxdXdPcPp4eT3WYbdmypcVVsg+Kj4/XmDFjtHTpUv3999+qUKGCpkyZYh7A/9///lft2rXTwIEDJd3/R2LkyJGaMmWKBg0a9NCzTHj0ypYt+9Bf6mn9nLy8vLR3714ZhmHxenR0tBITE81jWL28vJSYmKgbN25Y/IMcFRWV6e3dvHlT69evV2hoqEaNGmVuj4uL040bNzLewUfM399fBQsW1JEjRyRJBQoUUN68edWzZ08NGjQozWXSCj8ZSRkTeOnSpX9XbA7Ztm2brly5oh07dpjPxkpKd2xeRsd50aJFNWPGDLVv314dOnTQN998kyqMp8XR0THVhYbS/XDwz/HTdnZ2Cg4OVnBwsP7++2/9+OOPevfdd9W8eXNFRET866vNvby80hzfmtHnO0WBAgVkMpnS7JuZ5bMiO5/LB39uKe/rp59+ajGrxz9lJsRbW8GCBWUymbRr1y5z0P2nlLaUUBwZGZmqz5UrV1KN00/rc16wYEF5eXlp48aNadaSkyGzWLFiWrBggSTp9OnT+vrrrzV27FjFx8dr3rx5ObYd2KanepjBw/Tt21c//fSTVqxYod9++02dOnVSixYtzF+5xsXFpfrF5OTkpEuXLuWaieaRPU2aNFFsbGyqoSdfffWV+XVJ5rCzcuVKi34rVqzI9LZMJpMMw0j1i+eLL75QUlJSVkvPUZcuXdK1a9fk4+Mj6f7ZmcaNG+vQoUN67rnnVL169VSPtM74ZaROnTpyd3fXvHnzZBjGo9iNLEn5pf3gz2P+/PnZWl+zZs20adMm7dy5U61atUr1VXVaAgMD9dtvv1m0nT59Os1ZIFJ4eHioY8eOGjRokG7cuJEjN0lo2LChjh07phMnTli0Z+bznXJV+urVqy3OnN+6dUvffffdv67tn3Lic1m3bl15eHjoxIkTaS5fvXr1dM9AZuTBs90P6yv9uzO7rVq1kmEYunz5cpr7ULFiRUlS7dq15eTkpCVLllgsf+nSJW3bti1T0561atVK169fV1JSUprbelTz/5YuXVpjxoxRxYoVdfDgwUeyDdiWp/rMbEbOnTun5cuX69KlSwoICJAkDR8+XBs3btSiRYs0adIkNW/eXG+//bb69Omjxo0b6+zZs+Y71ERGRlpMGQPb0qtXL82ePVu9e/fW+fPnVbFiRe3evVuTJk1SUFCQmjZtKklq0aKF6tatq2HDhikmJkbVqlXTnj17zKH3n2M20+Pm5qYGDRpo2rRpKliwoAIDAxUWFqYFCxbIw8PjUe6mhbt375rHFSYlJSk8PFxTp06VJA0dOtTcb9asWapXr57q16+v//znPwoMDNStW7d09uxZfffdd6mu9n8YFxcXffTRRxowYICaNm2qV199Vb6+vjp79qyOHDmizz77LMf2MTPq1KmjAgUKaODAgQoNDZW9vb2WLl1qPjudHfXq1dPWrVvVokULNWvWTBs2bDBPe5aWnj17qkePHnrjjTf08ssv68KFC5o6dWqqK9tbt25tnkvZ29tbFy5c0MyZM1WsWDGLK9Gza+jQoVq4cKFatmyp8ePHy9fXV8uWLdPvv/8u6eGf7wkTJqhFixZ68cUXNWzYMCUlJWnKlCnKnz9/jn/r8G8/ly4uLvr000/Vu3dv3bhxQx07dpSPj4+uXr2qI0eO6OrVq5o7d26W66pYsaJ27Nih7777Tv7+/nJ1dU035Lm6uqpYsWL63//+pyZNmsjT09P8b0Jm1a1bV6+99pr69u2r/fv3q0GDBsqfP78iIyO1e/duVaxYUf/5z3/k4eGh9957T++++6569eqlrl276vr16xo3bpwcHR1Tzf6Qli5dumjp0qUKCgrSkCFDVKNGDdnb2+vSpUvavn272rZtq/bt22e69vT89ttvGjx4sDp16qRSpUopX7582rZtm3777TeLb7Pw9CLMpuPgwYMyDEOlS5e2aI+LizP/hf/qq6/q3LlzatWqlRISEuTm5qYhQ4Zo7Nix5imHYJscHR21fft2jR49WtOmTdPVq1dVqFAhDR8+3OIf+Tx58ui7777TsGHD9OGHHyo+Pl5169bVkiVLVKtWrUyH0WXLlmnIkCF65513lJiYqLp162rLli2pLlZ6lP744w/Vrl1b0v39Srlg5NNPP7X4ur1cuXI6ePCgJkyYoDFjxig6OloeHh4qVaqUgoKCsrXt/v37KyAgQFOmTNGAAQNkGIYCAwPVu3fvHNm3rPDy8tL333+vYcOGqUePHsqfP7/atm2rlStXqmrVqtleb/Xq1RUWFqamTZvqhRde0KZNm1J9lZuiW7duunLliubNm6dFixapQoUKmjt3rvnuUCkaN26sVatWmac98/Pz04svvqj33nsv1dzA2REQEKCwsDANHTpUAwcOlLOzs9q3b6/x48erd+/eD/18v/jii1q7dq3GjBmjV155RX5+fnrjjTd09+7dVPvyb+XE57JHjx4qWrSopk6dqtdff123bt2Sj4+PKleunOa8v5kxa9YsDRo0SF26dNGdO3fUsGHDDOfnXbBggUaMGKE2bdooLi5OvXv31uLFi7O0zfnz56tWrVqaP3++5syZo+TkZAUEBKhu3boWF/2FhITIx8dHn3zyiVauXGmej3nSpEmZ+mMob968WrdunWbNmqX//ve/mjx5svnW4Q0bNjSfBf63/Pz8VLJkSc2ZM0cREREymUwqUaKEPvroI7355ps5sg3YNpORG77XywVMJpPWrFljvuXgypUr1b17dx0/fjxVMHVxcbG4gCEpKUlRUVHy9vbW1q1bFRQUpD///NP81SyePsuWLVP37t31008/PZILfwBreu2118wXBGbnq3cAyEmcmU1HlSpVlJSUpOjoaNWvXz/Dvnnz5jVPN7J8+XLVrl2bIPsUWb58uS5fvqyKFSsqT548+uWXXzRt2jQ1aNCAIAubN378eAUEBKhEiRKKjY3V+vXr9cUXX2jMmDEEWQC5wlMdZmNjY813hJKk8PBwHT58WJ6enipdurS6d++uXr166aOPPlKVKlV07do1bdu2TRUrVlRQUJCuXbumb7/9Vo0aNdK9e/e0aNEiffPNN+a5R/F0cHV11YoVKzRx4kTdvn1b/v7+6tOnjyZOnGjt0oB/zd7eXtOmTdOlS5eUmJioUqVKacaMGRoyZIi1SwMASU/5MIMdO3aocePGqdpTxiglJCRo4sSJ+uqrr3T58mV5eXmpdu3aGjdunCpWrKhr166pdevWOnr0qAzDUO3atfXBBx+oZs2aVtgbAACAp89THWYBAABg25hnFgAAADaLMAsAAACb9dRdAJacnKwrV67I1dWV280CAADkQoZh6NatWwoICHjoDVqeujB75coVFSlSxNplAAAA4CEiIiJUuHDhDPs8dWHW1dVV0v03x83NzcrVAAAA4EExMTEqUqSIObdlyHjK3Lx505Bk3Lx509qlPFKTJk0yqlevbri4uBje3t5G27Ztjd9//z3DZa5cuWJ07drVKF26tGEymYwhQ4ak6tOwYUNDUqpHUFBQtrf92muvGZKMjz/++KHbeuWVV7L0PmRVcnKyERoaavj7+xuOjo5Gw4YNjWPHjln0OXv2rNGuXTujYMGChqurq9GpUycjKirqkdYFAMDTJCt5jQvAnlBhYWEaNGiQfvnlF23ZskWJiYlq1qyZbt++ne4ycXFx8vb21ujRo1WpUqU0+6xevVqRkZHmx7Fjx5Q3b1516tQpW9teu3at9u7dq4CAgDS39+qrr1psb/78+Vl8Jyz16dNHY8eOTff1qVOnasaMGfrss8+0b98+873ub926JUm6ffu2mjVrJpPJpG3btumnn35SfHy8WrdureTk5H9VGwAAyIbHEK5zlaflzOyDoqOjDUlGWFhYpvo3bNgwzTOzD/r4448NV1dXIzY2NsvbvnTpklGoUCHj2LFjRrFixdI8M/uwGi5dumR07tzZ8PDwMDw9PY02bdoY4eHh6fbv3bu3ERoamuZrycnJhp+fn/Hhhx+a2+7du2e4u7sb8+bNMwzDMDZt2mTkyZPH4vNz48YNQ5KxZcuWDGsFAACZw5lZpHLz5k1JkqenZ46ud8GCBerSpYvy58+fpW0nJyerZ8+eGjFihMqXL5/uskuXLlXBggVVvnx5DR8+3HyGVJLu3Lmjxo0by8XFRTt37tTu3bvl4uKiFi1aKD4+Psv7Eh4erqioKDVr1szc5uDgoIYNG+rnn3+WdP/stclkkoODg7mPo6Oj8uTJo927d2d5mwAA4N956i4AexoZhqHg4GDVq1dPFSpUyLH1/vrrrzp27JgWLFiQ5W1PmTJFdnZ2euutt9Jdtnv37ipevLj8/Px07NgxhYSE6MiRI9qyZYskacWKFcqTJ4+++OIL8zRrixYtkoeHh3bs2GERSjMjKipKkuTr62vR7uvrqwsXLkiSatWqpfz582vkyJGaNGmSDMPQyJEjlZycrMjIyCxtDwAA/HuE2afA4MGD9dtvv+X4mcMFCxaoQoUKqlGjRpa2feDAAc2aNUsHDx7McK7fV1991fz/FSpUUKlSpVS9enUdPHhQVatW1YEDB3T27NlUVzreu3dP586dk3T/zO7rr79ufi3lzOr06dPNbfPnz1f37t3Nzx+syTAMc5u3t7e++eYb/ec//9Enn3yiPHnyqGvXrqpatary5s2b7r4AAIBHgzD7hHvzzTe1bt067dy586HztGXFnTt3tGLFCo0fPz7L2961a5eio6NVtGhRc1tSUpKGDRummTNn6vz582mur2rVqrK3t9eZM2dUtWpVJScnq1q1alq6dGmqvt7e3pKkNm3aqGbNmub2kSNHqlChQhZnhFPOxPr5+Um6f4bW39/f/Hp0dLTF2dpmzZrp3Llzunbtmuzs7OTh4SE/Pz8VL1483fcCAAA8GoTZJ5RhGHrzzTe1Zs0a7dixI8eD1tdff624uDj16NEjy9vu2bOnmjZtatHWvHlz9ezZU3379k13m8ePH1dCQoI5aFatWlUrV66Uj49PunMGu7q6Wpy5dXV1laenp5555plUfVOGNGzZskVVqlSRJMXHxyssLExTpkxJ1b9gwYKSpG3btik6Olpt2rRJt3YAAPBoEGafUIMGDdKyZcv0v//9T66urubxoO7u7nJycpIkhYSE6PLly/rqq6/Myx0+fFiSFBsbq6tXr+rw4cPKly+fypUrZ7H+BQsWqF27dvLy8srytr28vFItZ29vLz8/P5UpU0aSdO7cOS1dulRBQUEqWLCgTpw4oWHDhqlKlSqqW7eupPtjaqdNm6a2bdtq/PjxKly4sC5evKjVq1drxIgRWT4TbTKZNHToUE2aNEmlSpVSqVKlNGnSJDk7O6tbt27mfosWLVLZsmXl7e2tPXv2aMiQIXr77bfNtQMAgMeHMPuEmjt3riSpUaNGFu2LFi1Snz59JEmRkZG6ePGixespZySl+2Nbly1bpmLFill89X/69Gnt3r1bmzdvzva2HyZfvnzaunWrZs2apdjYWBUpUkQvvfSSQkNDzWNTnZ2dtXPnTo0cOVIdOnTQrVu3VKhQITVp0iTbd3d75513dPfuXb3xxhv666+/VLNmTW3evNni7O6pU6cUEhKiGzduKDAwUKNHj9bbb7+dre0BAIB/x2QYhmHtIh6nmJgYubu76+bNm9zOFgAAIBfKSl5jnlkAAADYLMIsAAAAbBZjZp8AgaO+t3YJSMf5D1+ydgkAADzRODMLAAAAm0WYBQAAgM0izAIAAMBmEWYBAABgswizAAAAsFmEWQAAANgswiwAAABsFmEWAAAANoswCwAAAJtFmAUAAIDNIswCAADAZhFmAQAAYLMIswAAALBZhFkAAADYLMIsAAAAbBZhFgAAADaLMAsAAACbRZgFAACAzbJqmJ08ebKef/55ubq6ysfHR+3atdOpU6ceulxYWJiqVasmR0dHlShRQvPmzXsM1QIAACC3sWqYDQsL06BBg/TLL79oy5YtSkxMVLNmzXT79u10lwkPD1dQUJDq16+vQ4cO6d1339Vbb72lVatWPcbKAQAAkBvYWXPjGzdutHi+aNEi+fj46MCBA2rQoEGay8ybN09FixbVzJkzJUlly5bV/v37NX36dL388suPumQAAADkIrlqzOzNmzclSZ6enun22bNnj5o1a2bR1rx5c+3fv18JCQmp+sfFxSkmJsbiAQAAgCdDrgmzhmEoODhY9erVU4UKFdLtFxUVJV9fX4s2X19fJSYm6tq1a6n6T548We7u7uZHkSJFcrx2AAAAWEeuCbODBw/Wb7/9puXLlz+0r8lksnhuGEaa7ZIUEhKimzdvmh8RERE5UzAAAACszqpjZlO8+eabWrdunXbu3KnChQtn2NfPz09RUVEWbdHR0bKzs5OXl1eq/g4ODnJwcMjRegEAAJA7WPXMrGEYGjx4sFavXq1t27apePHiD12mdu3a2rJli0Xb5s2bVb16ddnb2z+qUgEAAJALWTXMDho0SEuWLNGyZcvk6uqqqKgoRUVF6e7du+Y+ISEh6tWrl/n5wIEDdeHCBQUHB+vkyZNauHChFixYoOHDh1tjFwAAAGBFVg2zc+fO1c2bN9WoUSP5+/ubHytXrjT3iYyM1MWLF83Pixcvrg0bNmjHjh2qXLmyJkyYoE8++YRpuQAAAJ5CVh0zm3LhVkYWL16cqq1hw4Y6ePDgI6gIAAAAtiTXzGYAAAAAZBVhFgAAADaLMAsAAACbRZgFAACAzSLMAgAAwGYRZgEAAGCzCLMAAACwWYRZAAAA2CzCLAAAAGwWYRYAAAA2izALAAAAm0WYBQAAgM0izAIAAMBmEWYBAABgswizAAAAsFmEWQAAANgswiwAAABsFmEWAAAANoswCwAAAJtFmAUAAIDNIswCAADAZhFmAQAAYLMIswAAALBZhFkAAADYLMIsAAAAbBZhFgAAADaLMAsAAACbRZgFAACAzSLMAgAAwGYRZgEAAGCzCLMAAACwWYRZAAAA2CzCLAAAAGwWYRYAAAA2izALAAAAm0WYBQAAgM0izAIAAMBmEWYBAABgswizAAAAsFmEWQAAANgswiwAAABsFmEWAAAANoswCwAAAJtFmAUAAIDNIswCAADAZhFmAQAAYLMIswAAALBZhFkAAADYLMIsAAAAbBZhFgAAADaLMAsAAACbRZgFAACAzSLMAgAAwGYRZgEAAGCzCLMAAACwWYRZAAAA2CyrhtmdO3eqdevWCggIkMlk0tq1azPsv2PHDplMplSP33///fEUDAAAgFzFzpobv337tipVqqS+ffvq5ZdfzvRyp06dkpubm/m5t7f3oygPAAAAuZxVw2zLli3VsmXLLC/n4+MjDw+PnC8IAAAANsUmx8xWqVJF/v7+atKkibZv355h37i4OMXExFg8AAAA8GSwqTDr7++vzz//XKtWrdLq1atVpkwZNWnSRDt37kx3mcmTJ8vd3d38KFKkyGOsGAAAAI+SyTAMw9pFSJLJZNKaNWvUrl27LC3XunVrmUwmrVu3Ls3X4+LiFBcXZ34eExOjIkWK6ObNmxbjbm1Z4KjvrV0C0nH+w5esXQIAADYnJiZG7u7umcprNnVmNi21atXSmTNn0n3dwcFBbm5uFg8AAAA8GWw+zB46dEj+/v7WLgMAAABWkO3ZDCIiInT+/HnduXNH3t7eKl++vBwcHLK0jtjYWJ09e9b8PDw8XIcPH5anp6eKFi2qkJAQXb58WV999ZUkaebMmQoMDFT58uUVHx+vJUuWaNWqVVq1alV2dwMAAAA2LEth9sKFC5o3b56WL1+uiIgI/XO4bb58+VS/fn299tprevnll5Unz8NP+u7fv1+NGzc2Pw8ODpYk9e7dW4sXL1ZkZKQuXrxofj0+Pl7Dhw/X5cuX5eTkpPLly+v7779XUFBQVnYDAAAAT4hMXwA2ZMgQLVq0SM2aNVObNm1Uo0YNFSpUSE5OTrpx44aOHTumXbt2afny5bKzs9OiRYv0/PPPP+r6sywrA4ptBReA5V5cAAYAQNZlJa9l+sxsvnz5dO7cuTTvtuXj46MXXnhBL7zwgkJDQ7VhwwZduHAhV4ZZAAAAPDkyHWanTZtm/v8LFy7Ix8dHTk5Oafbla38AAAA8DlmezSA5OVmlSpXSpUuXHkU9AAAAQKZlOczmyZNHpUqV0vXr1x9FPQAAAECmZWue2alTp2rEiBE6duxYTtcDAAAAZFq25pnt0aOH7ty5o0qVKilfvnypxs7euHEjR4oDAAAAMpKtMDtz5swcLgMAAADIumyF2d69e+d0HQAAAECWZWvMrCSdO3dOY8aMUdeuXRUdHS1J2rhxo44fP55jxQEAAAAZyVaYDQsLU8WKFbV3716tXr1asbGxkqTffvtNoaGhOVogAAAAkJ5shdlRo0Zp4sSJ2rJli/Lly2dub9y4sfbs2ZNjxQEAAAAZyVaYPXr0qNq3b5+q3dvbm/lnAQAA8NhkK8x6eHgoMjIyVfuhQ4dUqFChf10UAAAAkBnZCrPdunXTyJEjFRUVJZPJpOTkZP30008aPny4evXqldM1AgAAAGnKVpj94IMPVLRoURUqVEixsbEqV66cGjRooDp16mjMmDE5XSMAAACQpmzNM2tvb6+lS5dqwoQJOnjwoJKTk1WlShWVKlUqp+sDAAAA0pWtM7Pjx4/XnTt3VKJECXXs2FGdO3dWqVKldPfuXY0fPz6nawQAAADSlK0wO27cOPPcsv90584djRs37l8XBQAAAGRGtsKsYRgymUyp2o8cOSJPT89/XRQAAACQGVkaM1ugQAGZTCaZTCaVLl3aItAmJSUpNjZWAwcOzPEiAQAAgLRkKczOnDlThmGoX79+GjdunNzd3c2v5cuXT4GBgapdu3aOFwkAAACkJUthtnfv3pKk4sWLq06dOrK3t38kRQEAAACZkekwGxMTIzc3N0lSlSpVdPfuXd29ezfNvin9AAAAgEcp02G2QIECioyMlI+Pjzw8PNK8ACzlwrCkpKQcLRIAAABIS6bD7LZt28wzFWzbti3NMAsAAAA8TpkOsw0bNtTnn3+uNm3aqFGjRo+wJAAAACBzsjTP7PLlyxUYGKiaNWtq0qRJOn78+KOqCwAAAHioLIXZ7du3KzIyUm+++aYOHz6sOnXqqGTJkgoODtaOHTuUnJz8qOoEAAAAUsnyHcAKFCigHj166Ouvv9bVq1c1e/Zs3bt3Tz179pS3t7d69eqlb7/9Vrdv334U9QIAAABm2bqdbYp8+fKpRYsWmjNnjiIiIrRp0yYFBgZqwoQJmjFjRk7VCAAAAKQpSzdNSE9SUpKOHj2qkiVLavz48Ro/frwSEhJyYtUAAABAurJ1Znbo0KFasGCBpPtBtkGDBqpataqKFCmiHTt2SBJ3BwMAAMAjl60w++2336pSpUqSpO+++07nz5/X77//rqFDh2r06NE5WiAAAACQnmyF2WvXrsnPz0+StGHDBnXq1EmlS5dW//79dfTo0RwtEAAAAEhPtsKsr6+vTpw4oaSkJG3cuFFNmzaVJN25c0d58+bN0QIBAACA9GTrArC+ffuqc+fO8vf3l8lk0osvvihJ2rt3r5599tkcLRAAAABIT7bC7NixY1WhQgVFRESoU6dOcnBwkCTlzZtXo0aNytECAQAAgPRke2qujh07pmrr3bv3vyoGAAAAyIpsh9mtW7dq69atio6OTnUb24ULF/7rwgAAAICHyVaYHTdunMaPH6/q1aubx80CAAAAj1u2wuy8efO0ePFi9ezZM6frAQAAADItW1NzxcfHq06dOjldCwAAAJAl2QqzAwYM0LJly3K6FgAAACBLsjXM4N69e/r888/1448/6rnnnpO9vb3F6zNmzMiR4gAAAICMZCvM/vbbb6pcubIk6dixYxavcTEYAAAAHpdshdnt27fndB0AAABAlmVrzCwAAACQG2Q6zA4cOFARERGZ6rty5UotXbo020UBAAAAmZHpYQbe3t6qUKGC6tSpozZt2qh69eoKCAiQo6Oj/vrrL504cUK7d+/WihUrVKhQIX3++eePsm4AAAAg82F2woQJevPNN7VgwQLNmzcv1YVfrq6uatq0qb744gs1a9YsxwsFAAAAHpSlC8B8fHwUEhKikJAQ/f3337pw4YLu3r2rggULqmTJksxkAAAAgMcqW7MZSJKHh4c8PDxysBQAAAAga5jNAAAAADaLMAsAAACbRZgFAACAzSLMAgAAwGZlO8wmJibqxx9/1Pz583Xr1i1J0pUrVxQbG5tjxQEAAAAZyVaYvXDhgipWrKi2bdtq0KBBunr1qiRp6tSpGj58eKbXs3PnTrVu3VoBAQEymUxau3btQ5cJCwtTtWrV5OjoqBIlSmjevHnZ2QUAAAA8AbIVZocMGaLq1avrr7/+kpOTk7m9ffv22rp1a6bXc/v2bVWqVEmfffZZpvqHh4crKChI9evX16FDh/Tuu+/qrbfe0qpVq7K8DwAAALB92Zpndvfu3frpp5+UL18+i/ZixYrp8uXLmV5Py5Yt1bJly0z3nzdvnooWLaqZM2dKksqWLav9+/dr+vTpevnllzO9HgAAADwZsnVmNjk5WUlJSanaL126JFdX139dVHr27NmT6la5zZs31/79+5WQkJDmMnFxcYqJibF4AAAA4MmQrTD74osvms+OSpLJZFJsbKxCQ0MVFBSUU7WlEhUVJV9fX4s2X19fJSYm6tq1a2kuM3nyZLm7u5sfRYoUeWT1AQAA4PHKVpj9+OOPFRYWpnLlyunevXvq1q2bAgMDdfnyZU2ZMiWna7RgMpksnhuGkWZ7ipCQEN28edP8iIiIeKT1AQAA4PHJ1pjZgIAAHT58WMuXL9fBgweVnJys/v37q3v37hYXhOU0Pz8/RUVFWbRFR0fLzs5OXl5eaS7j4OAgBweHR1YTAAAArCdbYVaSnJyc1K9fP/Xr1y8n68lQ7dq19d1331m0bd68WdWrV5e9vf1jqwMAAAC5Q7bD7OXLl/XTTz8pOjpaycnJFq+99dZbmVpHbGyszp49a34eHh6uw4cPy9PTU0WLFlVISIguX76sr776SpI0cOBAffbZZwoODtarr76qPXv2aMGCBVq+fHl2dwMAAAA2LFthdtGiRRo4cKDy5csnLy8vi/GqJpMp02F2//79aty4sfl5cHCwJKl3795avHixIiMjdfHiRfPrxYsX14YNG/T2229r9uzZCggI0CeffMK0XAAAAE8pk5FyBVUWFClSRAMHDlRISIjy5Mn2HXGtIiYmRu7u7rp586bc3NysXU6OCBz1vbVLQDrOf/iStUsAAMDmZCWvZSuJ3rlzR126dLG5IAsAAIAnS7bSaP/+/fXNN9/kdC0AAABAlmRrzOzkyZPVqlUrbdy4URUrVkw1k8CMGTNypDgAAAAgI9kKs5MmTdKmTZtUpkwZSUp1ARgAAADwOGQrzM6YMUMLFy5Unz59crgcAAAAIPOyNWbWwcFBdevWzelaAAAAgCzJVpgdMmSIPv3005yuBQAAAMiSbA0z+PXXX7Vt2zatX79e5cuXT3UB2OrVq3OkOAAAACAj2QqzHh4e6tChQ07XAgAAAGRJtm9nCwAAAFgbt/ACAACAzcr0mdmqVatq69atKlCggKpUqZLhfLIHDx7MkeIAAACAjGQ6zLZt21YODg6SpHbt2j2qegAAAIBMy3SYDQ0NVb9+/TRr1iyFhoY+ypoAAACATMnSmNkvv/xSd+/efVS1AAAAAFmSpTBrGMajqgMAAADIsizPZpDRhV8AAADA45TleWZLly790EB748aNbBcEAAAAZFaWw+y4cePk7u7+KGoBAAAAsiTLYbZLly7y8fF5FLUAAAAAWZKlMbOMlwUAAEBuwmwGAAAAsFlZGmaQnJz8qOoAAAAAsizLU3MBAAAAuQVhFgAAADaLMAsAAACbRZgFAACAzSLMAgAAwGYRZgEAAGCzCLMAAACwWYRZAAAA2CzCLAAAAGwWYRYAAAA2izALAAAAm0WYBQAAgM0izAIAAMBmEWYBAABgswizAAAAsFmEWQAAANgswiwAAABsFmEWAAAANoswCwAAAJtFmAUAAIDNIswCAADAZhFmAQAAYLMIswAAALBZhFkAAADYLMIsAAAAbBZhFgAAADaLMAsAAACbRZgFAACAzSLMAgAAwGYRZgEAAGCzCLMAAACwWYRZAAAA2CzCLAAAAGyW1cPsnDlzVLx4cTk6OqpatWratWtXun137Nghk8mU6vH7778/xooBAACQW1g1zK5cuVJDhw7V6NGjdejQIdWvX18tW7bUxYsXM1zu1KlTioyMND9KlSr1mCoGAABAbmLVMDtjxgz1799fAwYMUNmyZTVz5kwVKVJEc+fOzXA5Hx8f+fn5mR958+Z9TBUDAAAgN7FamI2Pj9eBAwfUrFkzi/ZmzZrp559/znDZKlWqyN/fX02aNNH27dsz7BsXF6eYmBiLBwAAAJ4MVguz165dU1JSknx9fS3afX19FRUVleYy/v7++vzzz7Vq1SqtXr1aZcqUUZMmTbRz5850tzN58mS5u7ubH0WKFMnR/QAAAID12Fm7AJPJZPHcMIxUbSnKlCmjMmXKmJ/Xrl1bERERmj59uho0aJDmMiEhIQoODjY/j4mJIdACAAA8Iax2ZrZgwYLKmzdvqrOw0dHRqc7WZqRWrVo6c+ZMuq87ODjIzc3N4gEAAIAng9XCbL58+VStWjVt2bLFon3Lli2qU6dOptdz6NAh+fv753R5AAAAsAFWHWYQHBysnj17qnr16qpdu7Y+//xzXbx4UQMHDpR0f4jA5cuX9dVXX0mSZs6cqcDAQJUvX17x8fFasmSJVq1apVWrVllzNwAAAGAlVg2zr7zyiq5fv67x48crMjJSFSpU0IYNG1SsWDFJUmRkpMWcs/Hx8Ro+fLguX74sJycnlS9fXt9//72CgoKstQsAAACwIpNhGIa1i3icYmJi5O7urps3bz4x42cDR31v7RKQjvMfvmTtEgAAsDlZyWtWv50tAAAAkF2EWQAAANgswiwAAABsFmEWAAAANoswCwAAAJtFmAUAAIDNIswCAADAZhFmAQAAYLMIswAAALBZhFkAAADYLMIsAAAAbBZhFgAAADaLMAsAAACbRZgFAACAzSLMAgAAwGYRZgEAAGCzCLMAAACwWYRZAAAA2CzCLAAAAGwWYRYAAAA2izALAAAAm0WYBQAAgM0izAIAAMBmEWYBAABgswizAPAPO3fuVOvWrRUQECCTyaS1a9dm2L9Pnz4ymUypHuXLlzf3SUhI0Pjx41WyZEk5OjqqUqVK2rhxY7rrnDx5skwmk4YOHWqxjpEjR6pixYrKnz+/AgIC1KtXL125csXc58aNG3rzzTdVpkwZOTs7q2jRonrrrbd08+bNbL8fmWEYhsaOHauAgAA5OTmpUaNGOn78uEWfqKgo9ezZU35+fsqfP7+qVq2qb7/99pHWBeDpQJgFgH+4ffu2KlWqpM8++yxT/WfNmqXIyEjzIyIiQp6enurUqZO5z5gxYzR//nx9+umnOnHihAYOHKj27dvr0KFDqda3b98+ff7553ruuecs2u/cuaODBw/qvffe08GDB7V69WqdPn1abdq0Mfe5cuWKrly5ounTp+vo0aNavHixNm7cqP79+2fz3bivT58+Gjt2bLqvT506VTNmzNBnn32mffv2yc/PTy+++KJu3bpl7tOzZ0+dOnVK69at09GjR9WhQwe98sorab4HAJAVJsMwDGsX8TjFxMTI3d1dN2/elJubm7XLyRGBo763dglIx/kPX7J2CfgXTCaT1qxZo3bt2mV6mbVr16pDhw4KDw9XsWLFJEkBAQEaPXq0Bg0aZO7Xrl07ubi4aMmSJea22NhYVa1aVXPmzNHEiRNVuXJlzZw5M91t7du3TzVq1NCFCxdUtGjRNPt888036tGjh27fvi07OztJ0uXLlxUcHKzNmzcrT548qlevnmbNmqXAwMA019GnTx8FBgamGWgNw1BAQICGDh2qkSNHSpLi4uLk6+urKVOm6PXXX5ckubi4aO7cuerZs6d5WS8vL02dOvVfh20AT56s5DXOzAJADlqwYIGaNm1qDrLS/XDn6Oho0c/JyUm7d++2aBs0aJBeeuklNW3aNFPbunnzpkwmkzw8PDLs4+bmZg6yd+7cUePGjeXi4qKdO3dq9+7dcnFxUYsWLRQfH5/Jvfx/4eHhioqKUrNmzcxtDg4OatiwoX7++WdzW7169bRy5UrduHFDycnJWrFiheLi4tSoUaMsbxMA/snO2gUAwJMiMjJSP/zwg5YtW2bR3rx5c82YMUMNGjRQyZIltXXrVv3vf/9TUlKSuc+KFSt08OBB7du3L1PbunfvnkaNGqVu3bqle9bi+vXrmjBhgvnsaMp28uTJoy+++EImk0mStGjRInl4eGjHjh0WoTQzoqKiJEm+vr4W7b6+vrpw4YL5+cqVK/XKK6/Iy8tLdnZ2cnZ21po1a1SyZMksbQ8AHsSZWQDIIYsXL5aHh0eqYQmzZs1SqVKl9OyzzypfvnwaPHiw+vbtq7x580qSIiIiNGTIEC1ZsiTVGdy0JCQkqEuXLkpOTtacOXPS7BMTE6OXXnpJ5cqVU2hoqLn9wIEDOnv2rFxdXeXi4iIXFxd5enrq3r17OnfunCRp6dKl5tdcXFy0dOlSTZo0KVXbP6UE4xSGYVi0jRkzRn/99Zd+/PFH7d+/X8HBwerUqZOOHj360P0FgIxwZhYAcoBhGFq4cKF69uypfPnyWbzm7e2ttWvX6t69e7p+/boCAgI0atQoFS9eXNL9gBkdHa1q1aqZl0lKStLOnTv12WefKS4uzhx8ExIS1LlzZ4WHh2vbtm1pnpW9deuWWrRoIRcXF61Zs0b29vbm15KTk1WtWrVUYTSlTklq06aNatasaW4fOXKkChUqpLfeesvclnIm1s/PT9L9M7T+/v7m16Ojo819zp07p88++0zHjh0zz/JQqVIl7dq1S7Nnz9a8efMe+v4CQHoIswCQA8LCwnT27NkML2ZydHRUoUKFlJCQoFWrVqlz586SpCZNmqQ6Q9m3b189++yzGjlyZKoge+bMGW3fvl1eXl6pthETE6PmzZvLwcFB69atS3Wmt2rVqlq5cqV8fHzSHZ7g6uoqV1dXi+eenp565plnUvUtXry4/Pz8tGXLFlWpUkWSFB8fr7CwME2ZMkXS/XG6kpQnj+WXgXnz5lVycnK67xcAZAZhFgD+ITY2VmfPnjU/Dw8P1+HDh+Xp6amiRYsqJCREly9f1ldffWWx3IIFC1SzZk1VqFAh1Tr37t2ry5cvq3Llyrp8+bLGjh2r5ORkvfPOO5Luh8UHl8ufP7+8vLzM7YmJierYsaMOHjyo9evXKykpyTxe1dPTU/ny5dOtW7fUrFkz3blzR0uWLFFMTIxiYmIk3T/rmjdvXnXv3l3Tpk1T27ZtNX78eBUuXFgXL17U6tWrNWLECBUuXDhL71fKfLiTJk1SqVKlVKpUKU2aNEnOzs7q1q2bJOnZZ5/VM888o9dff13Tp0+Xl5eX1q5dqy1btmj9+vVZ2h4APIgwCwD/sH//fjVu3Nj8PDg4WJLUu3dvLV68WJGRkbp48aLFMjdv3tSqVas0a9asNNd57949jRkzRn/88YdcXFwUFBSk//73vxnOQvCgS5cuad26dZKkypUrW7y2fft2NWrUSAcOHNDevXslKdVZ1PDwcAUGBsrZ2Vk7d+7UyJEj1aFDB926dUuFChVSkyZNsj1d4TvvvKO7d+/qjTfe0F9//aWaNWtq8+bN5rO79vb22rBhg0aNGqXWrVsrNjZWzzzzjL788ksFBQVla5sAkIJ5Zp8AzDObezHPLICnxc6dOzVt2jQdOHBAkZGRmZqjOSwsTMHBwTp+/LgCAgL0zjvvaODAgRZ9Zs6cqblz5+rixYsqWLCgOnbsqMmTJ5uH0IwdO1bjxo2zWMbX19f8zcWDXn/9dX3++ef6+OOPzXfZu3HjhkJDQ7V582ZFRESoYMGCateunSZMmCB3d/fsvSGZYBiGxo0bp88//9z8h+Ds2bMt7iAYFRWlESNGaMuWLbp165bKlCmjd999Vx07dnxkdeUGzDMLAAAeq6zePS88PFxBQUGqX7++Dh06pHfffVdvvfWWVq1aZe6zdOlSjRo1SqGhoTp58qQWLFiglStXKiQkxGJd5cuXt7gTX3qzZKxdu1Z79+5VQECARTt3z7NtDDMAAAD/WsuWLdWyZctM9583b56KFi1qvstd2bJltX//fk2fPl0vv/yyJGnPnj2qW7euefx1YGCgunbtql9//dViXXZ2duaZNdJz+fJlDR48WJs2bdJLL1l+a1ahQgWLEF2yZEl98MEH6tGjhxITE7N997yMGIahmTNnavTo0erQoYMk6csvv5Svr6+WLVtmnh96z549mjt3rmrUqCHp/jR3H3/8sQ4ePGi+6PJpR5gF8NRiiE7uxRCdJ9+ePXtS3aSjefPmWrBggRISEmRvb6969eppyZIl+vXXX1WjRg398ccf2rBhg3r37m2x3JkzZxQQECAHBwfVrFlTkyZNUokSJcyvJycnq2fPnhoxYoTFV/gZSe/uefXr19fOnTtlZ2eniRMnqkWLFvrtt99STcn3MA+7e15KmE25e95LL70kDw8Pff3119w97wGEWQAA8NhFRUWleee4xMREXbt2Tf7+/urSpYuuXr2qevXqyTAMJSYm6j//+Y9GjRplXqZmzZr66quvVLp0af3555+aOHGi6tSpo+PHj5unr5syZYrs7Ows5krOCHfPsy2EWQAAYBVp3Tnun+07duzQBx98oDlz5qhmzZo6e/ashgwZIn9/f7333nuSZDG0oWLFiqpdu7ZKliypL7/8UsHBwTpw4IBmzZqlgwcPptpeWjJz97x/evDuef8MwHFxcTKZTJo+fbq5bf78+erevXuG70F6d88rWLCg1q5dq06dOmnXrl2qWLHiQ/fnaUCYBQAAj52fn1+qGQeio6NlZ2dnPqP63nvvqWfPnhowYICk+2H19u3beu211zR69OhUN+KQ7s/RXLFiRZ05c0aStGvXLkVHR6to0aLmPklJSRo2bJhmzpyp8+fPm9u5e55tIswCAIDHrnbt2vruu+8s2jZv3qzq1aubQ+SdO3fSvHOcYRhKb2bRuLg4nTx5UvXr15d0fzaApk2bWvRp3ry5evbsqb59+5rbuHue7WJqLgAA8K/Fxsbq8OHDOnz4sKT/v3teyk1GQkJC1KtXL3P/gQMH6sKFCwoODtbJkye1cOFCLViwQMOHDzf3ad26tebOnasVK1YoPDxcW7Zs0Xvvvac2bdqYb/M8fPhwhYWFKTw8XHv37lXHjh0VExNjvkgs5U56/3zY29vLz89PZcqUkSTz3fNu376tBQsWKCYmRlFRUYqKilJSUpIkqXv37ipYsKDatm2rXbt2KTw8XGFhYRoyZIguXbqU5ffrn3fPW7NmjY4dO6Y+ffqke/e8X3/9VefOndNHH32kLVu2PHQO36cJZ2YBAMC/ltW75xUvXlwbNmzQ22+/rdmzZysgIECffPKJeVou6f54UZPJpDFjxujy5cvy9vZW69at9cEHH5j7XLp0SV27dtW1a9fk7e2tWrVq6ZdfflGxYsUyXTt3z7Nt3AHsCcD0QrkX0wvlbhw7uRfHDvB04w5gAAAAeCowzAAAAGQa32jkbk/jtxqcmQUAAIDNIswCAADAZhFmAQAAYLMIswAAALBZhFkAAADYLMIsAAAAbBZhFgAAADaLMAsAAACbRZgFAACAzSLMAgAAwGZZPczOmTNHxYsXl6Ojo6pVq6Zdu3Zl2D8sLEzVqlWTo6OjSpQooXnz5j2mSgEAAJDbWDXMrly5UkOHDtXo0aN16NAh1a9fXy1bttTFixfT7B8eHq6goCDVr19fhw4d0rvvvqu33npLq1atesyVAwAAIDewapidMWOG+vfvrwEDBqhs2bKaOXOmihQporlz56bZf968eSpatKhmzpypsmXLasCAAerXr5+mT5/+mCsHAABAbmBnrQ3Hx8frwIEDGjVqlEV7s2bN9PPPP6e5zJ49e9SsWTOLtubNm2vBggVKSEiQvb19qmXi4uIUFxdnfn7z5k1JUkxMzL/dhVwjOe6OtUtAOp6kz9mTiGMn9+LYyb04bnK3J+XYSdkPwzAe2tdqYfbatWtKSkqSr6+vRbuvr6+ioqLSXCYqKirN/omJibp27Zr8/f1TLTN58mSNGzcuVXuRIkX+RfVA5rjPtHYFgG3i2AGy50k7dm7duiV3d/cM+1gtzKYwmUwWzw3DSNX2sP5ptacICQlRcHCw+XlycrJu3LghLy+vDLcD64iJiVGRIkUUEREhNzc3a5cD2ASOGyB7OHZyL8MwdOvWLQUEBDy0r9XCbMGCBZU3b95UZ2Gjo6NTnX1N4efnl2Z/Ozs7eXl5pbmMg4ODHBwcLNo8PDyyXzgeCzc3N/5hAbKI4wbIHo6d3OlhZ2RTWO0CsHz58qlatWrasmWLRfuWLVtUp06dNJepXbt2qv6bN29W9erV0xwvCwAAgCebVWczCA4O1hdffKGFCxfq5MmTevvtt3Xx4kUNHDhQ0v0hAr169TL3HzhwoC5cuKDg4GCdPHlSCxcu1IIFCzR8+HBr7QIAAACsyKpjZl955RVdv35d48ePV2RkpCpUqKANGzaoWLFikqTIyEiLOWeLFy+uDRs26O2339bs2bMVEBCgTz75RC+//LK1dgE5zMHBQaGhoamGhgBIH8cNkD0cO08Gk5GZOQ8AAACAXMjqt7MFAAAAsoswCwAAAJtFmAUAAIDNIswCAADAZhFmAQAAYLMIswAAALBZhFkAAADYLMIscq2IiAj169fP2mUANodjB0jb3bt3tXv3bp04cSLVa/fu3dNXX31lharwb3HTBORaR44cUdWqVZWUlGTtUgCbwrEDpHb69Gk1a9ZMFy9elMlkUv369bV8+XL5+/tLkv78808FBARw3Nggq97OFk+3devWZfj6H3/88ZgqAWwLxw6QdSNHjlTFihW1f/9+/f333woODlbdunW1Y8cOFS1a1Nrl4V/gzCysJk+ePDKZTMroI2gymfgrGXgAxw6Qdb6+vvrxxx9VsWJFc9ugQYO0fv16bd++Xfnz5+fMrI1izCysxt/fX6tWrVJycnKaj4MHD1q7RCBX4tgBsu7u3buys7P8Qnr27Nlq06aNGjZsqNOnT1upMvxbhFlYTbVq1TL8pfuwM0/A04pjB8i6Z599Vvv370/V/umnn6pt27Zq06aNFapCTiDMwmpGjBihOnXqpPv6M888o+3btz/GigDbwLEDZF379u21fPnyNF/77LPP1LVrV/4ItFGMmQUAAIDN4swsAAAAbBZhFrnWnDlzNH78eGuXAdgcjh0g6zhubBfDDJBrNWnSROHh4cyZCWQRxw6QdRw3toswCwAAAJvFMAMAAADYLG5ni1zl8OHDOnPmjPz9/VW3bl2ZTCZrlwTkOnFxccqTJ4/s7e0lSefOndPChQt18eJFFStWTP3791fx4sWtXCWQu3DcPLk4Mwur6datm27duiVJio2NVfPmzVW1alX16NFDDRo0UI0aNfT3339bt0ggF2rZsqW+++47SdJPP/2k8uXLa/369UpISNCGDRtUoUIF7dmzx8pVArkLx82TizGzsJq8efMqMjJSPj4+GjFihFatWqVvv/1WVatW1bFjx9S5c2e1aNFCM2bMsHapQK5SoEAB7d+/XyVLllSjRo1UtWpVi+Pkvffe0/bt27V7924rVgnkLhw3Ty7OzMJq/vl31A8//KAPP/xQVatWlSRVqFBB06dP1/r1661VHpBrJSQkKCEhQZL0+++/q3fv3hav9+nTR0eOHLFGaUCuxXHz5CLMwqpSxsT++eefqlChgsVr5cuXV0REhDXKAnK1mjVrmr8uLVmyZKpfwIcPH5anp6c1SgNyLY6bJxcXgMGq3nvvPTk7OytPnjyKiopSuXLlzK9du3ZNLi4uVqwOyJ0mTpyoli1b6vbt2+ratauGDRumM2fOqGzZsjp16pQ++eQThYSEWLtMIFfhuHlyMWYWVtOoUSOL2Qp69Oih/v37m59PmDBBW7du1Y4dO6xQHZC77dmzR8HBwdq7d69Fe0BAgEaMGKEhQ4ZYqTIg9+K4eTIRZpFr/fHHH8qXL58KFy5s7VKAXOvq1av6448/lJycLH9/fwUGBlq7JCDX47h5sjBmFrnC4MGDdePGDYu2EiVKEGSBhxg3bpxKlSql2rVr8wsZyCSOmycLYRZWc+nSJfP/L1u2TLGxsZKkihUrcuEXkAGOHSDrOG6eXFwABqt59tln5eXlpbp16+revXuKiIhQ0aJFdf78efP0KQBS49gBso7j5snFmVlYzc2bN/XNN9+oWrVqSk5OVlBQkEqXLq24uDht2rRJUVFR1i4RyJU4doCs47h5cnEBGKzm3r17cnR0lHT/ziwHDhxQZGSkmjZtqgoVKujEiRMqXLiwTp06ZeVKgdyFYwfIOo6bJxfDDGA1bm5uqlKliurWrav4+HjduXNHdevWlZ2dnVauXKnChQvr119/tXaZQK7DsQNkHcfNk4thBrCaK1euaMyYMXJwcFBiYqKqV6+u+vXrKz4+XgcPHpTJZFK9evWsXSaQ63DsAFnHcfPkYpgBcoUCBQpo586dOnnypHr16iU/Pz/9+eefqlGjhsLCwqxdHpBrcewAWcdx82ThzCxyDXd3d3Xu3Fn29vbatm2bwsPD9cYbb1i7LCDX49gBso7j5snBmVnkChERESpUqJDy5MmjChUq6IcfflCRIkWsXRaQ63HsAFnHcfNkIcwCAADAZjHMAAAAADaLMAsAAACbRZgFAACAzSLMAngq7dixQyaTSX///be1S3li9enTR+3atbN2GQCecIRZAE+8Ro0aaejQodYuAwDwCBBmAeAxSkhIsHYJNs0wDCUmJlq7DAC5CGEWwBOtT58+CgsL06xZs2QymWQymXT+/Hnz6wcOHFD16tXl7OysOnXq6NSpUxbLf/fdd6pWrZocHR1VokQJjRs3ziJMXbx4UW3btpWLi4vc3NzUuXNn/fnnn+bXx44dq8qVK2vhwoUqUaKEHBwcZBiGbt68qddee00+Pj5yc3PTCy+8oCNHjqS5XNGiReXi4qL//Oc/SkpK0tSpU+Xn5ycfHx998MEHD93/du3aafr06fL395eXl5cGDRpkEapNJpPWrl1rsZyHh4cWL14sSTp//rxMJpO+/vpr1a9fX05OTnr++ed1+vRp7du3T9WrV5eLi4tatGihq1evpqph3Lhx5v18/fXXFR8fb37NMAxNnTpVJUqUkJOTkypVqqRvv/3W/HrKcJBNmzapevXqcnBw0K5duzLcZwBPFztrFwAAj9KsWbN0+vRpVahQQePHj5ckeXt7mwPt6NGj9dFHH8nb21sDBw5Uv3799NNPP0mSNm3apB49euiTTz5R/fr1de7cOb322muSpNDQUBmGoXbt2il//vwKCwtTYmKi3njjDb3yyivasWOHuYazZ8/q66+/1qpVq5Q3b15J0ksvvSRPT09t2LBB7u7umj9/vpo0aaLTp0/L09NTknTu3Dn98MMP2rhxo86dO6eOHTsqPDxcpUuXVlhYmH7++Wf169dPTZo0Ua1atdJ9D7Zv3y5/f39t375dZ8+e1SuvvKLKlSvr1VdfzdJ7GRoaqpkzZ6po0aLq16+funbtKjc3N82aNUvOzs7q3Lmz3n//fc2dO9e8zNatW+Xo6Kjt27fr/Pnz6tu3rwoWLGgO4WPGjNHq1as1d+5clSpVSjt37lSPHj3k7e2thg0bmtfzzjvvaPr06SpRooQ8PDyyVDeAJ5wBAE+4hg0bGkOGDLFo2759uyHJ+PHHH81t33//vSHJuHv3rmEYhlG/fn1j0qRJFsv997//Nfz9/Q3DMIzNmzcbefPmNS5evGh+/fjx44Yk49dffzUMwzBCQ0MNe3t7Izo62txn69athpubm3Hv3j2LdZcsWdKYP3++eTlnZ2cjJibG/Hrz5s2NwMBAIykpydxWpkwZY/Lkyenue+/evY1ixYoZiYmJ5rZOnToZr7zyivm5JGPNmjUWy7m7uxuLFi0yDMMwwsPDDUnGF198YX59+fLlhiRj69at5rbJkycbZcqUsdi2p6encfv2bXPb3LlzDRcXFyMpKcmIjY01HB0djZ9//tli2/379ze6du1qGMb//5zWrl2b7j4CeLpxZhbAU+25554z/7+/v78kKTo6WkWLFtWBAwe0b98+i6/yk5KSdO/ePd25c0cnT55UkSJFLG6DWa5cOXl4eOjkyZN6/vnnJUnFihWTt7e3uc+BAwcUGxsrLy8vi1ru3r2rc+fOmZ8HBgbK1dXV/NzX11d58+ZVnjx5LNqio6Mz3Mfy5cubzwin7OfRo0czfmPS8M/3ytfXV5JUsWLFDGupVKmSnJ2dzc9r166t2NhYRUREKDo6Wvfu3dOLL75osUx8fLyqVKli0Va9evUs1wvg6UCYBfBUs7e3N/+/yWSSJCUnJ5v/O27cOHXo0CHVco6OjjIMw7zMPz3Ynj9/fovXk5OT5e/vbzEUIcU/v0L/Z20p9aXVllJveh62jMlkkvHAnc3TulAtrffqwbaH1ZJW3++//16FChWyeN3BwcHi+YPvIQCkIMwCeOLly5dPSUlJWV6uatWqOnXqlJ555pk0Xy9XrpwuXryoiIgI89nZEydO6ObNmypbtmyG642KipKdnZ0CAwOzXFdO8/b2VmRkpPn5mTNndOfOnRxZ95EjR3T37l05OTlJkn755Re5uLiocOHCKlCggBwcHHTx4kWL8bEAkBWEWQBPvMDAQO3du1fnz5+Xi4uL+QKrh3n//ffVqlUrFSlSRJ06dVKePHn022+/6ejRo5o4caKaNm2q5557Tt27d9fMmTPNF4A1bNgww6/FmzZtqtq1a6tdu3aaMmWKypQpoytXrmjDhg1q167dY/9K/YUXXtBnn32mWrVqKTk5WSNHjkx1Nje74uPj1b9/f40ZM0YXLlxQaGioBg8erDx58sjV1VXDhw/X22+/reTkZNWrV08xMTH6+eef5eLiot69e+dIDQCebEzNBeCJN3z4cOXNm1flypWTt7e3Ll68mKnlmjdvrvXr12vLli16/vnnVatWLc2YMUPFihWT9P9TWhUoUEANGjRQ06ZNVaJECa1cuTLD9ZpMJm3YsEENGjRQv379VLp0aXXp0kXnz583j0V9nD766CMVKVJEDRo0ULdu3TR8+HCLca7/RpMmTVSqVCk1aNBAnTt3VuvWrTV27Fjz6xMmTND777+vyZMnq2zZsmrevLm+++47FS9ePEe2D+DJZzIeHCgFAAAA2AjOzAIAAMBmEWYBAABgswizAAAAsFmEWQAAANgswiwAAABsFmEWAAAANoswCwAAAJtFmAUAAIDNIswCAADAZhFmAQAAYLMIswAAALBZhFkAAADYrP8DeKTQSJTte8kAAAAASUVORK5CYII=",
+      "text/plain": [
+       "<Figure size 800x400 with 1 Axes>"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "#plt.figure(figsize=(8, 7))\n",
+    "ax = bench_results.plot.bar(y='ns/iter', x='theorem number', figsize=(8,4))\n",
+    "ax.bar_label(ax.containers[0]) # add numeric values on bars\n",
+    "plt.title('Program Benchmark using different theorems')\n",
+    "plt.ylabel('Time (ns/iter)')\n",
+    "plt.legend().remove()\n",
+    "plt.savefig('figures/benchmark.png', bbox_inches='tight')\n",
+    "plt.show()"
+   ]
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "SageMath 10.1",
+   "language": "sage",
+   "name": "sagemath"
+  },
+  "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.11.7"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}
diff --git a/content.tex b/content.tex
index b74c618ca1d2f616133f6240168bc328fac600b4..4903ea8e18ca7d4371d8813a04134b136b500834 100644
--- a/content.tex
+++ b/content.tex
@@ -866,6 +866,7 @@ Here are some benchmarks to illustrate the performance benefits of the
 alternative algorithm which will later be described in this article [ref].
 
 \begin{center}
+\label{table:bench-schmidt-vs-nay}
 \begin{tabular}{ |r|l|l| }
  \hline
  Choice of $v$ on $\mathbb{P}^2$
@@ -2002,18 +2003,79 @@ given by theorems
 \ref{thm:rmax_with_uniform_eps}
 \ref{thm:rmax_with_eps1}, have been shown in passing to be tighter than the
 previous one.
-However, in principle, it could be possible that this does not translate to an
+However, in principle, it could be possible that this does not translate to a
 decrease in computational time to find the solutions to the problem.
 This could be due to a range of potential reasons:
 \begin{itemize}
 	\item Unexpected optimisations from the compiler for a certain form of the
 		program.
-	\item Increased complexity to computing the tighter bounds.
+	\item Increased complexity to computing the formulae for the tighter bounds.
 	\item Modern CPU architecture such as branch predictors
 		\cite{BranchPredictor2024} may offset the overhead of considering ranks that
 		turn out to be too large to have any solutions.
 \end{itemize}
 
+For relatively small Chern characters (as those appearing in examples so far),
+the difference in performance between the program \cite{NaylorRust2023} when
+patched with the results of the different theorems above, do not show any
+significant difference in performance. The earlier, weaker theorems occasionally
+producing the results marginally faster.
+
+Note that this program patched with theorem \ref{thm:loose-bound-on-r} will be
+using the same bound as was used in the previously existing program
+\cite{SchmidtGithub2020}. However the difference of performance can be of
+several orders of magnitude as illustrated in the table in section
+\ref{table:bench-schmidt-vs-nay}.
+This will be attributed to the difference in programming language and algorithm,
+the latter having already been discussed in that same section.
+
+In order to see a difference between the different patches, we use the Chern
+character $v=(45,54\ell,-41\frac{\ell^2}{2})$ for a smooth projective surface $X$
+with a generator $\ell$ for $NS(X)$ such that $\ell^2=1$ or 2 (such as a
+principally polarised surface or $\mathbb{P}^2$).
+This example was chosen for the large rank $\chern_0(v)=45$,
+but also the large Bogomolov discriminant $\Delta(v)=4761\ell^2$, which are both
+indicators to the size of the bounds on the pseudo-semistabiliser ranks.
+
+\begin{figure}
+	\includegraphics[width=\linewidth]{figures/benchmark.png}
+	\caption{
+		Comparing the performance of program \cite{NaylorRust2023}
+		with different patches corresponding to the results of theorems
+		\ref{thm:loose-bound-on-r}
+		\ref{thm:rmax_with_uniform_eps}
+		\ref{thm:rmax_with_eps1}
+		when computing solutions to problem \ref{problem:problem-statement-2}
+		for $(45,54\ell,-41\frac{\ell^2}{2})$
+	}
+	\label{fig:benchmark}
+\end{figure}
+
+As shown in figure \ref{fig:benchmark}, there can be a significant improvement
+by using theorems \ref{thm:rmax_with_uniform_eps} \ref{thm:rmax_with_eps1}
+which specialise to different values of $\chern_1^{\beta_{-}(v)}(u)$
+of solutions $u$ of problem \ref{problem:problem-statement-2}.
+the program to eliminate.
+
+As for the difference between theorems \ref{thm:rmax_with_uniform_eps}
+and \ref{thm:rmax_with_eps1}, the biggest indicator is the `$n$'-value, that is,
+the denominator of $\beta_{-}(v)$. For this example, it is 15.
+The bound from theorem \ref{thm:rmax_with_eps1} is roughly $1/{k_{v,q}}$ times
+that of theorem \ref{thm:rmax_with_uniform_eps}.
+Note that $k_{v,q}$ iterates through all its possible values
+$\{1, 2, \ldots, n\}$ cyclically.
+So we could expect the average tighter bound to be approximately that of the
+average looser times the mean average of $1/{k_{v,q}}$:
+\begin{equation*}
+	\frac{1}{n} \sum_{i=1}^n \frac{1}{i}
+\end{equation*}
+This certainly tends to 0 for large $n$. But in the current example, with
+$n=15$, this gives us approximately 0.2 for the ratio of the average tighter bound
+versus the average looser.
+However, the actual ratio in the benchmark shown in figure \ref{fig:benchmark}
+between the two instances of the program patched with the two corresponding
+bounds is around 0.6 instead.
+Not as good as the improvement on the bound, however still not an insignificant
+for examples with larger `$n$'-value, where the execution time will
+potentially be in the order of minutes, or even hours.
 
-However these don't end up being significant overheads when using the ``better''
-theorems, as verified here.
diff --git a/figures/benchmark.png b/figures/benchmark.png
new file mode 100644
index 0000000000000000000000000000000000000000..7e2b4b681d66d6c09c1b57c0651b4976a68fada0
Binary files /dev/null and b/figures/benchmark.png differ