3sat-v2.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "# Simple Quantum Implementation using Qiskit Aqua for Boolean satisfiability problems\n",
    "\n",
    "\n",
    "\n",
    "This Jupyter notebook demonstrates how easy it is to use quantum algorithms from [Qiskit Aqua](https://qiskit.org/aqua) to solve Boolean satisfiability problems [(SAT)](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem). \n",
    "\n",
    "It is based on the Qiskit tutorial [\n",
    "Using Grover search for boolean satisfiability](https://github.com/JavaFXpert/qiskit4devs-workshop-notebooks/blob/master/grover_search_party.ipynb) by [James Weaver](http://twitter.com/JavaFXpert).\n",
    "\n",
    "Implemented by [Jan-R. Lahmann](http://twitter.com/JanLahmann) using Qiskit, binder and RISE."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "## Boolean Satisfiabilty problems (SAT)\n",
    "\n",
    "The Boolean satisfiability problem [(SAT)](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem) considers a Boolean expression with N boolean variables involving negation (NOT, $\\neg$), conjunction (AND, $\\wedge$) and disjunction (OR, $\\vee$), as in the following (simple) example:  \n",
    "$$ f(x_1, x_2) = (x_1 \\vee x_2) \\wedge (x_1 \\vee \\neg x_2) . $$\n",
    "\n",
    "The problem is to determine whether there is any assignment of values (TRUE, FALSE) to the Boolean variables which makes the formula true. \n",
    "\n",
    "It's something like trying to flip a bunch of switches to find the setting that makes a light bulb turn on.  \n",
    "SAT is of central importance in many areas of computer science, including complexity theory, algorithmics, cryptography, artificial intelligence, circuit design, and automatic theorem proving."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "subslide"
    }
   },
   "source": [
    "SAT was the first problem proven to be NP-complete.  \n",
    "This means that all problems in the [complexity class NP](https://en.wikipedia.org/wiki/NP_(complexity)) are at most as difficult to solve as SAT. \n",
    "\n",
    "There is no known classical algorithm that efficiently solves each SAT problem, and it is generally believed that no such algorithm exists.  \n",
    "Whether Boolean satisfiability problems have a classical algorithm that is polynomial in time is equivalent to the [P vs. NP problem](https://en.wikipedia.org/wiki/P_versus_NP_problem).  \n",
    "\n",
    "\n",
    "While [Grover's quantum search algorithm](https://en.wikipedia.org/wiki/Grover's_algorithm) does not provide exponential speed-up to this problem, it may nevertheless provide some speed-up in contrast to classical black-box search strategies.\n",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "## Solving 3-SAT using Qiskit Aqua and Grover's search algorithm\n",
    "### Throwing a party while avoiding the drama\n",
    "\n",
    "Imagine you are inviting some friends to a party, some who are couples, and some who are not on speaking terms. \n",
    "\n",
    "Specifically, **Alice** and **Bob** are in a relationship, as are **Carol** and **David**. However, **Alice** and **David** had a bad breakup a while ago and haven't been civil with each other since. \n",
    "\n",
    "Armed with a quantum computer and Qiskit Aqua, how can you leverage Grover's quantum search algorithm to identify friendly combinations of people to invite?\n",
    "\n",
    "The constraints for our party planning problem may be formulated with the following boolean expression:\n",
    "\n",
    "        ((A and B) or (C and D)) and not (A and D)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "To apply a quantum algorithm from Qiskit Aqua to this problem, we simply need to import the Qiskit libraries and run the algorithm with the appropriate parameters."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "# Import the necessary functions from Qiskit\n",
    "from qiskit import qiskit\n",
    "from qiskit.visualization import plot_histogram\n",
    "from qiskit.utils import QuantumInstance\n",
    "from qiskit.algorithms import Grover\n",
    "from qiskit.circuit.library import PhaseOracle\n",
    "from qiskit import Aer\n",
    "from qiskit.algorithms import AmplificationProblem"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "Let's go ahead and use our expression in a Grover quantum search to find out compatible combinations of people to invite.\n",
    "\n",
    "Note: We'll represent and with \"&\", or with \"|\", not with \"~\" in our expression."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "pycharm": {
     "name": "#%%\n"
    },
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "# Define the formal logical expression corresponding to our \"party problem\"\n",
    "log_expr = \"((A & B) | (C & D)) & ~(A & D)\""
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "Let's run the algorithm on a quantum simulator and plot the result.\n",
    "\n",
    "Each basis state represents our four friends, with the least significant bit representing Alice. If a bit is 1, then the advice is to invite the person that the bit represents. If the bit is 0, then Grover advises not to send an invitation."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAoAAAAHTCAYAAAC3P6nnAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjUuMywgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy/NK7nSAAAACXBIWXMAAA9hAAAPYQGoP6dpAABXXElEQVR4nO3deVhV5f7+8XsDMsjsLKagOZUmaA6oieIAppWZs5VaHbV5PA1aOZyOU9lsOabRSVOPHk/lTAQ5kaRmmaXijAMK2gEhZNrr94c/9tcdoOAG97b9fl2X1yXPevZan8f1IDdrNBmGYQgAAABOw8XeBQAAAOD6IgACAAA4GQIgAACAkyEAAgAAOBkCIAAAgJMhAAIAADgZAiAAAICTcbN3AX9lZrNZp06dkq+vr0wmk73LAQAAf2GGYejChQsKCgqSi8uVj/ERACvRqVOnVL9+fXuXAQAAnEhKSopuuummK/YhAFYiX19fSZd2hJ+fn52rAQAAf2WZmZmqX7++JX9cCQGwEhWd9vXz8yMAAgCA66Isl51xEwgAAICTIQACAAA4GYcNgD/88IP69OmjgIAAeXt7Kzw8XMuXLy/z59etW6ehQ4eqefPmCggIUNWqVdW8eXM98sgjOnDgQLH+ycnJmjp1qiIiIhQUFCR3d3fVr19fI0aM0L59+ypyaAAAAHZlMgzDsHcRfxYfH6/o6Gh5enpq6NCh8vX11cqVK3Xs2DHNnDlTL7zwwlXX8dRTT+nrr79Whw4dFBQUpCpVqui3337TunXr5ObmprVr16p79+6W/kOHDtWyZcvUsmVL3XHHHfLz89OePXu0bt06eXl5af369YqIiCjXODIzM+Xv76+MjAyuAQQAAJWqPLnD4QJgQUGBmjdvrhMnTuj7779XWFiYJCkjI0Pt27fX0aNHdeDAAQUHB19xPRcvXpSnp2ex9ri4OPXs2VNt27bVDz/8YGn/9NNPFRoaqtatW1v1X7p0qYYNG6Zbb71Ve/fuLddYCIAAAOB6KU/ucLhTwN9++60OHTqk4cOHW8KfJPn7+2v8+PHKy8tTTEzMVddTUviTpB49eigwMFAHDx60ah81alSx8CddOjLYtGlT/frrr0pPTy/fYAAAAByQwwXAhIQESVJUVFSxZdHR0ZKk77777prXn5iYqN9//10tW7Ys82eqVKkiSXJz46k5AADgxudwiSY5OVmS1KRJk2LL6tSpIx8fH0ufsti4caO2bdum3NxcJScna/Xq1apRo4befffdMn0+KSlJe/fuVbt27RQQEHDFvrm5ucrNzbV8nZmZKUnKz89Xfn6+JMnFxUWurq4qLCyU2Wy29C1qLygo0OVn5V1dXeXi4lJqe9F6ixSF1IKCgjK1V6lSRWazWYWFhZY2k8kkNze3UttLq50xMSbGxJgYE2NiTPYbU3k4XADMyMiQdOmUb0n8/Pwsfcpi48aNevvtty1fN27cWEuXLtXtt99eplpGjhwpFxcXvfnmm1ftP23aNE2ePLnEGqpWrSpJatCggVq3bq2ff/5Zx48ft/Rp1qyZmjdvrqSkJKWlpVnaw8LCFBwcrE2bNunChQuW9o4dO6pWrVrauHGj1QSLjIyUl5eX1q5da1VDnz59lJOTo/j4eEubm5ub+vbtq/T0dCUmJlrafX191b17d6WkpGj37t2W9po1a6pTp05KTk7W/v37Le2MiTExJsbEmBgTY7L/mIKCglRWDncTSFRUlGJjY5WcnKzGjRsXW16vXj1lZWWVKwRKUlZWln799Vf94x//0DfffKOFCxdq+PDhpfbPyclR3759FR8frylTpmj8+PFX3UZJRwDr16+v9PR0y8WYzvbbCGNiTIyJMTEmxsSYrs+YsrOzb9y7gAcNGqQVK1Zox44dJR6l8/X1VWBgoFXqLY+CggK1bdtWBw8e1JEjR1SzZs1ifS5evKh77rlHsbGxGjdunKZOnXpN2+IuYAAAcL3c0HcBF137V9J1fqmpqcrKyirx+sCycnNzU2RkpLKzs7Vjx45iy3Nycizh76WXXrrm8AcAAOCoHC4Adu3aVdKl6+b+bMOGDVZ9rtWpU6ck/d/dvUVycnLUr18/xcbG6u9//7tmzJhh03YAAAAckcMFwB49eqhRo0ZasmSJ1cWQGRkZmjp1qtzd3TVixAhL++nTp7Vv375i1wSWdHRPuhQiV61apYCAAHXs2NHSfvHiRUv4e/755/XWW29V7MAAAAAchMPdBezm5qYFCxYoOjpaERERJb4KLiQkxNJ/3LhxiomJ0aJFizRq1ChLe7t27dSyZUu1atVKN910k7Kzs/Xzzz9r8+bNqlKlihYuXChvb29L/0cffVSxsbGqU6eOfH19NWnSpGK1jRo1ymrbAAAANyKHC4DSpduqt2zZookTJ2rZsmXKz8/XbbfdphkzZmjIkCFlWsfUqVMVHx+v7777TmlpaXJxcVGDBg00ZswYPfvss7rlllus+h89elTSpesMS3qUiyR169aNAAgAAG54DncX8F8JdwEDAIDr5Ya+CxgAAACViwAIAADgZAiAAAAAToYACAAA4GQIgAAAAE6GAAgAAOBkCIAAAABOhgAIAADgZAiAAAAAToYACAAA4GQIgAAAAE6GAAgAAOBkCIAAAABOhgAIAADgZAiAAAAAToYACAAA4GQIgLD46KOPFBISIk9PT3Xo0EFJSUml9p0/f766dOmiwMBABQYGqmfPnsX6m0ymEv+89dZbxdaXm5ursLAwmUwm7d69u6KHBgAALkMAhCRp2bJlev755zVx4kTt2rVLoaGhio6O1tmzZ0vsn5CQoGHDhik+Pl6JiYmqX7++oqKidPLkSUuf06dPW/1ZuHChTCaTBgwYUGx9L730koKCgiptfAAA4P+YDMMw7F3EX1VmZqb8/f2VkZEhPz8/e5dzRR06dFC7du00a9YsSZLZbFb9+vX11FNP6ZVXXrnq5wsLCxUYGKhZs2ZpxIgRJfa59957deHCBcXFxVm1r1u3Ts8//7xWrlypFi1a6Mcff1RYWJjNYwIAwJmUJ3dwBBDKy8vTzp071bNnT0ubi4uLevbsqcTExDKt448//lB+fr6qVatW4vIzZ85ozZo1euSRR4q1jx49Wv/6179UtWrVax8EAAAoMwIglJ6ersLCQtWuXduqvXbt2kpNTS3TOl5++WUFBQVZhcjLxcTEyNfXV/fdd5+lzTAMjRo1So8++qjatm177QMAAADl4mbvAnDjmz59upYuXaqEhAR5enqW2GfhwoW6//77rZZ/+OGHunDhgsaNG3e9SgUAAOIIICTVqFFDrq6uOnPmjFX7mTNnVKdOnSt+dubMmZo+fbo2btyoVq1aldhn8+bN2r9/v/72t79ZtX/77bdKTEyUh4eH3Nzc1LhxY0lS27ZtNXLkSBtGBAAAroQACLm7u+v222+3ujnDbDYrLi5OHTt2LPVzb775pt544w2tX7/+iqdwP/nkE91+++0KDQ21av/ggw/0008/affu3dq9e7fWrl0r6dIdyVOmTLFxVAAAoDScAoYk6fnnn9fIkSPVtm1btW/fXu+9956ys7P10EMPSZJGjBihevXqadq0aZKkGTNmaMKECVqyZIlCQkIs1wr6+PjIx8fHst7MzEz9+9//1ttvv11smw0aNLD6uuhzN998s2666aZKGScAACAA4v8bMmSI0tLSNGHCBKWmpiosLEzr16+33Bhy/Phxubj83wHj2bNnKy8vTwMHDrRaz8SJEzVp0iTL10uXLpVhGBo2bNh1GQcAALg6ngNYiW6k5wACAIAbG88BBAA4nIp+3aQk/fbbb7rnnnvk7+8vb29vtWvXTsePH7fqk5iYqO7du8vb21t+fn6KiIhQTk5OhY8PuJEQAAEAla4yXjd56NAh3XHHHWrevLkSEhL0888/6/XXX7d63FRiYqJ69+6tqKgoJSUl6YcfftCTTz5pdUkL4Iw4BVyJOAUMAJdUxusmhw4dqipVquhf//pXqZ8LDw9Xr1699MYbb1TMQAAHxilgAIDDqIzXTZrNZq1Zs0ZNmzZVdHS0atWqpQ4dOui///2v5TNnz57V9u3bVatWLXXq1Em1a9dW165dtWXLlgodH3AjIgACACpVZbxu8uzZs8rKytL06dPVu3dvbdy4Uf3799d9992n7777TpJ0+PBhSdKkSZM0evRorV+/Xm3atFGPHj2UnJxcgSMEbjw8BgYA4NBKet2k2WyWJPXr10/PPfecJCksLEzbtm3TnDlz1LVrV0ufsWPHWp5p2rp1a8XFxWnhwoWW55oCzogjgACASlUZr5usUaOG3NzcdOutt1r1v+WWWyx3AdetW1eSrtgHcFYEQABApaqM1026u7urXbt22r9/v1X7gQMHFBwcLEkKCQlRUFDQFfsAzopTwACASlcZr5t88cUXNWTIEEVERCgyMlLr16/X119/rYSEBEmSyWTSiy++qIkTJyo0NFRhYWGKiYnRvn37tGLFiuv/jwA4EAIgAKDSVcbrJvv37685c+Zo2rRpevrpp9WsWTOtXLlSd9xxh6X/s88+q4sXL+q5557T+fPnFRoaqtjYWN18882VP2jAgfEcwErEcwABAMD1wnMAAQAAUCoCIAAAgJMhAAIAADgZAiAAAICTIQACAAA4GQIgAACAkyEAAgAAOBkeBH2DG/2evStwXPOftXcFAAA4Jo4AAgAAOBkCIAAAgJMhAAIAADgZAiAAAICTIQACAAA4GQIgAACAkyEAAgAAOBkCIAAAgJMhAAIAADgZ3gQCALgi3jhUMt42hBsZRwABAACcDAEQAADAyRAAAQAAnAwBEMA1+eijjxQSEiJPT0916NBBSUlJpfadP3++unTposDAQAUGBqpnz57F+k+aNEnNmzeXt7e3pc/27dut+uzatUu9evVSQECAqlevrjFjxigrK6tSxgcAf2UEQADltmzZMj3//POaOHGidu3apdDQUEVHR+vs2bMl9k9ISNCwYcMUHx+vxMRE1a9fX1FRUTp58qSlT9OmTTVr1izt2bNHW7ZsUUhIiKKiopSWliZJOnXqlHr27KnGjRtr+/btWr9+vfbu3atRo0ZdjyEDwF+KyTAMw95F/FVlZmbK399fGRkZ8vPzq5RtcHde6bhDr/J06NBB7dq106xZsyRJZrNZ9evX11NPPaVXXnnlqp8vLCxUYGCgZs2apREjRpTYp+j755tvvlGPHj00b948vf766zp9+rRcXC797rpnzx61atVKycnJaty4ccUNEFb4f6Zk/B8DR1Oe3MERQADlkpeXp507d6pnz56WNhcXF/Xs2VOJiYllWscff/yh/Px8VatWrdRtzJs3T/7+/goNDZUk5ebmyt3d3RL+JMnLy0uStGXLlmsdDgA4JQIggHJJT09XYWGhateubdVeu3ZtpaamlmkdL7/8soKCgqxCpCStXr1aPj4+8vT01LvvvqvY2FjVqFFDktS9e3elpqbqrbfeUl5enn7//XfL0cbTp09XwMgAwHkQAAFcV9OnT9fSpUu1atUqeXp6Wi2LjIzU7t27tW3bNvXu3VuDBw+2XFfYokULxcTE6O2331bVqlVVp04dNWzYULVr17Y6KggAuDr+1wRQLjVq1JCrq6vOnDlj1X7mzBnVqVPnip+dOXOmpk+fro0bN6pVq1bFlnt7e6tx48YKDw/XJ598Ijc3N33yySeW5cOHD1dqaqpOnjypc+fOadKkSUpLS1OjRo0qZnAA4CQIgADKxd3dXbfffrvi4uIsbWazWXFxcerYsWOpn3vzzTf1xhtvaP369Wrbtm2ZtmU2m5Wbm1usvXbt2vLx8dGyZcvk6empXr16lX8gAODEeBcwgHJ7/vnnNXLkSLVt21bt27fXe++9p+zsbD300EOSpBEjRqhevXqaNm2aJGnGjBmaMGGClixZopCQEMu1gj4+PvLx8VF2dramTJmie+65R3Xr1lV6ero++ugjnTx5UoMGDbJsd9asWerUqZN8fHwUGxurF198UdOnT1dAQMB1/zcAgBsZARBAuQ0ZMkRpaWmaMGGCUlNTFRYWpvXr11tuDDl+/LjVdXmzZ89WXl6eBg4caLWeiRMnatKkSXJ1ddW+ffsUExOj9PR0Va9eXe3atdPmzZvVokULS/+kpCRNnDhRWVlZat68uebOnasHH3zw+gwaAP5CeA5gJeI5gPbFM7qAisH/MyXj/xg4Gp4DCAAAgFIRAAEAAJwMARAAAMDJEAABAACcDAEQAADAyRAAAQAAnAwBEAAAwMkQAAEAAJwMARAAAMDJOGwA/OGHH9SnTx8FBATI29tb4eHhWr58eZk+axiG1q1bp8cee0ytWrWSv7+/qlatqtDQUE2dOlUXL14s03oee+wxmUwmmUwmy7tLAQAAbnQO+S7g+Ph4RUdHy9PTU0OHDpWvr69WrlypIUOGKCUlRS+88MIVP5+bm6s+ffrIw8ND3bp1U3R0tC5evKgNGzbo1Vdf1X//+18lJCSoatWqpa4jNjZWc+bMkbe3t7Kzsyt6iAAAAHbjcAGwoKBAo0ePlouLizZt2qSwsDBJ0oQJE9S+fXuNHz9eAwcOVHBwcKnrcHV11T//+U89/vjjCgwMtLTn5+drwIAB+vrrr/XRRx/pxRdfLPHzGRkZevjhhzVw4EClpaXpu+++q9AxAgAA2JPDnQL+9ttvdejQIQ0fPtwS/iTJ399f48ePV15enmJiYq64jipVqujVV1+1Cn9F7ePGjZOkK4a6Z555Rjk5Ofroo4+ufSAAAMAmH330kUJCQuTp6akOHTooKSmp1L7z589Xly5dFBgYqMDAQPXs2dOqf35+vl5++WXddttt8vb2VlBQkEaMGKFTp05ZrWfKlCnq1KmTqlatqoCAgMoamt05XABMSEiQJEVFRRVbFh0dLenK4e1qqlSpIklycyv54OfXX3+tmJgYffjhh6pVq9Y1bwcAAFy7ZcuW6fnnn9fEiRO1a9cuhYaGKjo6WmfPni2xf0JCgoYNG6b4+HglJiaqfv36ioqK0smTJyVJf/zxh3bt2qXXX39du3bt0n/+8x/t379f99xzj9V68vLyNGjQID322GOVPkZ7crhTwMnJyZKkJk2aFFtWp04d+fj4WPpci4ULF0oqOWCeO3dOo0eP1r333qthw4aVe925ubnKzc21fJ2ZmSnp0m8d+fn5kiQXFxe5urqqsLBQZrPZ0reovaCgQIZhWNpdXV3l4uJSajtKV/RvLkkmk0lubm4ym80qLCws1l7a/qio/XR5LdL//QJSUFBQpvYqVaqUWjtjYkyVPSaUzpH2019t7r3zzjv629/+pgceeECS9OGHH2rNmjVauHChXnrppWJjWrx4sVXts2fP1sqVKxUXF6f7779fVatW1dq1a63G9N5776lTp046dOiQGjRoIFdXV02ePFkFBQWWs435+fk3zH4qD4cLgBkZGZIunfItiZ+fn6VPea1bt05z587VLbfcokceeaTY8scff1x5eXmaPXv2Na1/2rRpmjx5crH2jRs3Wm44adCggVq3bq2ff/5Zx48ft/Rp1qyZmjdvrqSkJKWlpVnaw8LCFBwcrE2bNunChQuW9o4dO3KE8iqKvtElydfXV927d1dKSop2795taa9Zs6Y6deqk5ORk7d+/39Je0ftp48aNVv8RREZGysvLy6pGSerTp49ycnIUHx9vaXNzc1Pfvn2Vnp6uxMRExsSYrvuYUDpH2k9/pblnGIZ27typxx57zKp/ixYtlJiYWKYx5eTkKC8vT9WqVbvimEwmk5KSkvTLL79Yjemnn35Sfn6+1q5de8Psp6CgIJWVybg8tjuAqKgoxcbGKjk5WY0bNy62vF69esrKyip3CPzhhx/Uo0cPubm5afPmzWrRooXV8mXLlmno0KH67LPP9OCDD1rau3Xrpu+++06nT59WnTp1rriNko4A1q9fX+np6fLz85NU8b9hjX6vXP8MTuXjJzgCWFLtzJnSXT5nJMf77d5ec485U7L5z3IEsLLGdOrUKYWEhGjLli1q3769pX3cuHHavHmzEhMTrzqmp556SrGxsdq7d6/l3+fyMeXn56tTp05q1qyZPvvss2JjiomJ0QsvvKC0tLQbZj9lZ2fL399fGRkZltxRGoc7Alh05K+0gJeZmVns5o6r2bFjh6KiouTi4qINGzYUC3/nz5/XE088ob59+1qFv/Ly8PCQh4dHsfYqVaoUO43i6uoqV1fXYn1LuzaxtHaUrqRTVy4uLiUeJi9tf1TUfirtNFp52kurvbxjQukcaT850txD6RxpP/2V5l7R311cXKzai8ZxtTFNnz5dy5cvV0JCgjw9PS3LiuTn52vw4MGSpLlz5xaryc3NzdK/pLpsGWtl76eycriLyIqu/SvpOr/U1FRlZWWVeH1gaXbs2KFevXrJbDZrw4YNateuXbE+x48f17lz57RmzRrLg5+L/hTdcFK3bl2ZTCarw7MAAKDi1ahRQ66urjpz5oxV+5kzZ656Nm7mzJmaPn26Nm7cqFatWhVbXhT+jh07ptjY2KseKfurcrjDSl27dtW0adO0ceNGDR061GrZhg0bLH3Koij8FRYWasOGDerQoUOJ/apXr17iNYGStGbNGqWmpmr48OHy8vJS9erVyzEaAABQXu7u7rr99tsVFxene++9V5JkNpsVFxenJ598stTPvfnmm5oyZYo2bNigtm3bFlteFP6Sk5MVHx/v1D/THS4A9ujRQ40aNdKSJUv09NNPW54FmJGRoalTp8rd3V0jRoyw9D99+rQyMjJUt25dqxtHdu7cqV69eqmgoEDr169Xx44dS91m/fr1tWDBghKXdevWTampqXr77bev+lsHAACoGM8//7xGjhyptm3bqn379nrvvfeUnZ2thx56SJI0YsQI1atXT9OmTZMkzZgxQxMmTNCSJUsUEhJieYWrj4+PfHx8lJ+fr4EDB2rXrl1avXq1CgsLLX2qVasmd3d3SZfOCp4/f17Hjx9XYWGh5cxf48aN5ePjc53/FSqPwwVANzc3LViwQNHR0YqIiLB6FdyxY8c0c+ZMhYSEWPqPGzdOMTExWrRokUaNGiXp0jV9vXr10v/+9z/17t1bsbGxio2NtdpOQECAnn322es3MAAAUGZDhgxRWlqaJkyYoNTUVIWFhWn9+vWqXbu2pEtB7fJr5mbPnq28vDwNHDjQaj0TJ07UpEmTdPLkSX311VeSZPWiCenSK2i7desm6dKbxy5/4UTr1q2L9fkrcLgAKF26rXrLli2aOHGili1bpvz8fN12222aMWOGhgwZctXPZ2Zm6vfff5ckrV+/XuvXry/WJzg4mAAIAIADe/LJJ0s95Vv04ogiR48eveK6QkJCVJYHn3z66af69NNPy1jhjcshA6AktW/fXuvWrbtqv5J2VFl3cln8eYIBAADc6BzuLmAAAABULgIgAACAkyEAAgAAOBkCIAAAgJMhAAIAADgZAiAAAICTIQACAAA4GQIgAACAkyEAAgAAOBkCIAAAgJMhAAIAADgZAiAAAICTIQACAAA4GTd7FwAAAP5aRr9n7woc0/xn7V3B/+EIIAAAgJMhAAIAADgZAiAAAICTIQACAAA4GQIgAACAkyEAAgAAOBkCIAAAgJMhAAIAADgZAiAAAICTqZQ3gRw9elSxsbHy9PRU//795ePjUxmbAQAAwDWw6Qjg1KlT1bBhQ/3++++WtoSEBLVs2VKPPvqoRo0apTZt2uj8+fM2FwoAAICKYVMA/O9//6uQkBAFBgZa2l5++WWZzWZNnjxZjz32mA4ePKj33nvP1joBAABQQWwKgEePHtWtt95q+frUqVP64Ycf9MQTT+i1117TrFmz1KNHD61atcrmQgEAAFAxbAqAmZmZCggIsHy9adMmmUwm3X333Za2Nm3a6Pjx47ZsBgAAABXIpgBYu3ZtHTt2zPJ1bGysPDw81KFDB0vbxYsXZTKZbNkMAAAAKpBNdwG3a9dOX375pVavXi1PT08tW7ZMkZGR8vDwsPQ5cuSIgoKCbC4UAAAAFcOmI4Djx49XQUGB+vXrp+joaF28eFHjx4+3LM/NzdWmTZusjggCAADAvmw6AtimTRt9//33+te//iVJGjx4sNq3b29Z/uOPPyoyMlLDhw+3rUoAAABUGJsfBB0aGqrQ0NASl4WHh3MHMAAAgIOpsDeBZGVl6cCBA8rOzlaXLl0qarUAAACoYDa/C/jo0aPq16+fAgMD1a5dO0VGRlqWbd26VbfeeqsSEhJs3QwAAAAqiE0B8Pjx4woPD9fatWvVr18/dezYUYZhWJZ36NBB6enp+uKLL2wuFAAAABXDpgA4ceJE/f777/ruu++0YsUK9erVy2q5m5ubunTpoq1bt9pUJAAAACqOTQFww4YN6t+/vzp16lRqn+DgYJ08edKWzQAAAKAC2RQAz58/r5CQkCv2MQxDubm5tmwGAAAAFcjmV8ElJydfsc+ePXvUoEEDWzYDAACACmRTAOzVq5dWr16tn3/+ucTlmzdv1rfffqs+ffrYshkAAABUIJsC4GuvvSYvLy9FRERoypQpOnjwoCRp3bp1ev3119W7d2/VqFFDL774YoUUCwAAANvZ9CDokJAQbdiwQUOHDtXrr78uk8kkwzB01113yTAMNWjQQCtWrFDdunUrql4AAADYyOY3gXTo0EHJycn6+uuvtX37dp0/f15+fn7q0KGD+vXrJ3d394qoEwAAABWkQl4F5+bmpv79+6t///4VsToAAABUIptfBQcAAIAbS7mOAH722WeSpP79+8vX19fydVmMGDGifJUBAACgUpQrAI4aNUomk0nh4eHy9fW1fH0lhmHIZDIRAAEAABxEuQLgwoULZTKZLHf1Llq0qFKKAgAAQOUp9xHAy40cObIiawEAAMB1YNNNIJs2bdLx48ev2CclJUWbNm2yZTMAAACoQDYFwMjISH366adX7PPZZ58pMjLSls0AAACgAtkUAA3DuGofs9l81RtFAAAAcP1U+nMAk5OT5e/vX9mbAQAAQBmV+00gDz/8sNXX//3vf3X06NFi/QoLCy3X/915553XXCAAAAAqVrkD4OXX/JlMJu3evVu7d+8usa/JZFK7du307rvvXmt9AAAAqGDlDoBHjhyRdOn6v0aNGunZZ5/VM888U6yfq6urAgMD5e3tbXuVAAAAqDDlDoDBwcGWvy9atEhhYWFWbQAAAHBs5Q6Al+NB0AAAADeecgXAogc6t2/fXp6enuV6wHNERET5KgMAAEClKFcA7Natm0wmk3777Tc1bdrU8nVZFBYWXlOBAAAAqFjlCoATJkyQyWRSjRo1rL4GAADAjaNcAXDSpElX/BoAAACOr9LfBAIAAADHQgAEAABwMuU6Bdy9e/dr2ojJZFJcXNw1fRYAAAAVq1wBMCEh4Zo2wo0iAAAAjqNcAdBsNldWHQAAALhOuAYQAADAyRAAAQAAnAyvggMAAHAyvAoOAADAyfAqOAAAACfDq+AAAACcDDeBAAAAOJlyHQEsTW5urtauXasff/xRGRkZ8vf3V+vWrdWnTx95eHhUxCYAAABQQWwOgF999ZXGjBmjtLQ0GYZhaTeZTKpVq5bmzZunu+++29bNAAAAoILYFADj4uI0YMAAubq66uGHH1aXLl1Uu3ZtnTlzRps2bdLnn3+u++67Txs2bLjm9wgDAACgYtl0DeDEiRPl5eWlHTt2aP78+RoxYoSio6M1YsQILViwQElJSfL09NTEiRPLve4ffvhBffr0UUBAgLy9vRUeHq7ly5eX+fOHDh3SpEmTdM8996hevXoymUwKCQm56ufMZrMWLlyoO+64QwEBAapataqaNm2qhx56SBcuXCj3OAAAAByNTUcAf/zxRw0fPlwtW7YscXmrVq00ePBgLV26tFzrjY+PV3R0tDw9PTV06FD5+vpq5cqVGjJkiFJSUvTCCy9cdR2bN2/W5MmT5erqqltuuUWpqalX/Uxubq4GDhyo1atXq1WrVho1apQ8PDx0/PhxrV27Vm+88YZ8fX3LNRYAAABHY1MArFq1qmrWrHnFPrVq1VLVqlXLvM6CggKNHj1aLi4u2rRpk8LCwiRdeuZg+/btNX78eA0cOFDBwcFXXE9ERIQSExMVGhoqLy8veXp6XnXbr7zyilavXq3p06fr5ZdftlpmNpvLPAYAAABHZtMp4J49e+qbb765Yp9vvvlGvXr1KvM6v/32Wx06dEjDhw+3hD9J8vf31/jx45WXl6eYmJirrqdRo0YKDw+Xl5dXmbZ78uRJzZo1S126dCkW/iTJxcVFLi48NQcAANz4bEo0M2fO1NmzZzVixAilpKRYLUtJSdGDDz6o9PR0zZw5s8zrTEhIkCRFRUUVWxYdHS1J+u6776696FKsWLFCBQUFGjRokC5cuKDFixdr2rRpWrhwoU6ePFnh2wMAALCXcp0CLulO3sDAQC1evFhLly5VgwYNLHcBHz9+XIWFhWrVqpUefPBBxcXFlWkbycnJkqQmTZoUW1anTh35+PhY+lSknTt3SpL+97//qVmzZjp9+rRlmbu7u6ZPn67nnnvuiuvIzc1Vbm6u5evMzExJUn5+vvLz8yVdOpLo6uqqwsJCq9PKRe0FBQVWj9NxdXWVi4tLqe0oXdG/uXTpsURubm4ym81W76Uuai9tf1TUfrq8Fklyc7v0rVdQUFCm9ipVqpRae3nHhNI50n5ypLmH0jnSfnKkucd7JkpXmfupPMoVAIuOzpWkoKBAhw8f1uHDh63af/rpp3K9LzgjI0PSpVO+JfHz87P0qUhnz56VJE2ePFm9evXSN998o/r162vTpk0aM2aMnn/+eTVv3lx33nlnqeuYNm2aJk+eXKx948aNlusgGzRooNatW+vnn3/W8ePHLX2aNWum5s2bKykpSWlpaZb2sLAwBQcHa9OmTVZ3IXfs2FG1atWyedx/ZWvXrrX83dfXV927d1dKSop2795taa9Zs6Y6deqk5ORk7d+/39Je0ftp48aNVv9hR0ZGysvLy6pGSerTp49ycnIUHx9vaXNzc1Pfvn2Vnp6uxMREm8eE0jnSfnKkuYfSOdJ+cqS5J/HzqTSVuZ+CgoLKXIfJuDy2O4CoqCjFxsYqOTlZjRs3Lra8Xr16ysrKKncI9PT0VJ06dXT06NErbrdu3bo6ePCg1Y0r69atU58+fdSjR48rXvNY0hHA+vXrKz09XX5+fpIq/rf70e+V65/BqXz8BEcAS6qdOVO6y+eMdOMfhamoucecKdn8ZzkCWNqYxn7AEcCSzH+2co8AZmdny9/fXxkZGZbcUZoKeRVcRSo68ldawMvMzFRgYGClbbdnz57F7lqOjo6Wh4eHduzYccV1eHh4lPjquypVqhQ7jeLq6lri6biib+6ytqN0JZ26Ku1mntL2R0Xtp9JOo5WnvbTayzsmlM6R9pMjzT2UzpH2k6PNPZSssvdTmeu45k9WkqJr/0q6zi81NVVZWVklXh9oq2bNmkmSAgICii1zcXGRr6+vcnJyKny7AAAA11uFxPYTJ04oPj5ep06dsjoFWsRkMun1118v07q6du2qadOmaePGjRo6dKjVsg0bNlj6VLTu3btrypQp+vXXX4stS0tLU3p6upo2bVrh2wUAALjebA6AL774ot5//32r89aGYVhu/Cj6e1kDYI8ePdSoUSMtWbJETz/9tOVZgBkZGZo6darc3d01YsQIS//Tp08rIyNDdevWLfXGkbLo2rWrbrnlFsXFxSk2Ntby7ELDMDR+/HhJ0uDBg695/QAAAI7CpgA4f/58vf322+rVq5ceffRRDRgwQKNGjVJ0dLQ2bdqkBQsW6N5779Xjjz9e9oLc3LRgwQJFR0crIiLC6lVwx44d08yZM63e6Ttu3DjFxMRo0aJFGjVqlKU9PT1df//73y1f5+fnKz093arPzJkzVaNGDUmXzqUvWrRI3bt3V58+fXTffffppptu0pYtW5SUlKQ2bdrolVdeueZ/KwAAAEdhUwCcN2+eQkJCtG7dOsuFiyEhIRoyZIiGDBmiwYMHq1evXho0aFC51hsZGaktW7Zo4sSJWrZsmfLz83XbbbdpxowZGjJkSJnWkZWVVeyNIdnZ2VZtkyZNsgRASerQoYOSkpI0ceJExcXFKTMzUw0aNNC4ceM0fvx4eXt7l2scAAAAjsimALhv3z49+OCDVnetXH5reteuXdW3b1/NnDlTAwcOLNe627dvr3Xr1l2136effqpPP/20WHtISIiu5Qk3LVq00IoVK8r9OQAAgBuFzXcBX37XrLe3t86dO2e1vFmzZtq7d6+tmwEAAEAFsSkA1qtXTydOnLB8ffPNN2v79u1WfX755RdOnQIAADgQmwJg586d9f3331u+7tevn3788UeNHTtWa9as0bhx47Ru3TpFRETYXCgAAAAqhk3XAD744IM6deqUjh07puDgYL344otavXq15s+frwULFsgwDIWEhOitt96qqHoBAABgI5sCYLdu3dStWzfL1z4+Pvr+++/15Zdf6tChQwoODtbdd9/NKWAAAAAHUuEv8KtSpUq57/gFAADA9VNhAfDcuXP66aeflJGRIX9/f4WGhqp69eoVtXoAAABUEJsD4NGjR/XMM89ozZo1Vs/dM5lMuuuuu/Tee+9ZvbkDAAAA9mVTADx06JA6d+6ss2fPqkmTJurcubNq166tM2fOaNu2bfrqq6/0/fffa9u2bWrUqFFF1QwAAAAb2BQAX375ZaWlpWnOnDkaPXq0TCaTZZlhGJo3b54ef/xxvfzyy/r3v/9tc7EAAACwnU0BMC4uTvfcc4/GjBlTbJnJZNLYsWO1du1affPNN7ZsBgAAABXIpgdBFxYWqkWLFlfs07JlSxUWFtqyGQAAAFQgmwJgmzZtrvqe371796pt27a2bAYAAAAVyKYAOGXKFK1bt04LFiwocfm8efO0YcMG/fOf/7RlMwAAAKhA5boG8B//+EextsjISI0dO1Zvv/221V3AW7du1YEDBxQdHa24uDh16tSpwooGAADAtStXAJw0aVKpy/bv36/9+/cXa1+/fr02bNig119/vdzFAQAAoOKVKwDGx8dXVh0AAAC4TsoVALt27VpZdQAAAOA6sekmEAAAANx4bH4XsCRt3bpVn376qXbv3q3MzEz5+fmpdevWGjFihO64446K2AQAAAAqiM0B8LnnntMHH3wgwzAkXXoDiGEY2rlzpz755BM988wzeuedd2wuFAAAABXDplPAMTExev/999WkSRMtXrxYp06dUkFBgU6fPq0lS5aoadOmev/99/XZZ59VVL0AAACwkU0BcPbs2brpppu0fft2DRs2THXq1JHJZFLt2rU1dOhQff/996pXr54+/vjjiqoXAAAANrIpAO7du1cDBgyQv79/icv9/f01YMCAq74uDgAAANdPpd8FbDKZKnsTAAAAKAebAmCLFi20cuVKZWVllbj8woULWrlypVq0aGHLZgAAAFCBbAqAY8eO1YkTJ9SxY0etXLlS6enpkqT09HStWLFCnTp10okTJ/TYY49VSLEAAACwnU2PgXnooYf0448/atasWRo8eLAkycXFRWazWZJkGIaeeuopjRw50vZKAQAAUCFsfg7gBx98oEGDBpX4IOiRI0eqS5cuFVEnAAAAKohNAXDTpk3y8/NTly5dCHoAAAA3CJuuAYyMjNS8efMqqhYAAABcBzYFwFq1asnT07OiagEAAMB1YFMA7NWrlxISEizvAQYAAIDjsykATp8+XefOndOYMWN0/vz5iqoJAAAAlcimm0AeeOABBQQEaOHChfr888/VsGFD1a5du9jbP0wmk+Li4mwqFAAAABXDpgCYkJBg+Xtubq727dunffv2FevH6+AAAAAch00BsOiBzwAAALhxXNM1gImJierevbt8fX3l7++vXr16KSkpqaJrAwAAQCUo9xHAPXv2qEePHrp48aKlLS4uTtu2bVNSUpJatGhRoQUCAACgYpX7COD06dN18eJFvfrqq0pNTVVqaqpef/115eTkaMaMGZVRIwAAACpQuY8Abt68WXfccYfeeOMNS9vkyZOVkJCg7777rkKLAwAAQMUr9xHAM2fOKDw8vFh7hw4ddObMmQopCgAAAJWn3AEwPz9fPj4+xdq9vb2Vn59fIUUBAACg8tj0JhAAAADceK7pOYCff/65vv/+e6u2gwcPSpL69OlTrL/JZNKaNWuuZVMAAACoYNcUAA8ePGgJfH+2fv36Ym28CQQAAMBxlDsAHjlypDLqAAAAwHVS7gAYHBxcGXUAAADgOuEmEAAAACdDAAQAAHAyBEAAAAAnQwAEAABwMgRAAAAAJ0MABAAAcDIEQAAAACdDAAQAAHAyBEAAAAAnQwAEAABwMgRAAAAAJ0MABAAAcDIEQAAAACdDAAQAAHAyBEAAAAAnQwAEAABwMgRAAAAAJ0MABAAAcDIEQAAAACdDAAQAAHAyBEAAAAAnQwAEAABwMgRAAAAAJ0MABAAAcDIEQAAAACdDAAQAAHAyBEAAAAAnQwAEAABwMgRAAAAAJ0MABAAAcDIEQAAAACfjsAHwhx9+UJ8+fRQQECBvb2+Fh4dr+fLl5VpHbm6u/vGPf6hJkyby9PRUUFCQxowZo7Nnz5bYPycnR++8847atGmjwMBABQQEKDQ0VFOmTFFGRkZFDAsAAMDu3OxdQEni4+MVHR0tT09PDR06VL6+vlq5cqWGDBmilJQUvfDCC1ddh9lsVr9+/bRhwwaFh4drwIABSk5O1oIFCxQXF6fvv/9eNWvWtPTPz89XZGSktm/frrCwMI0aNcpSy2uvvaYvvvhCSUlJqlq1amUNGwAA4LpwuABYUFCg0aNHy8XFRZs2bVJYWJgkacKECWrfvr3Gjx+vgQMHKjg4+IrriYmJ0YYNGzRs2DAtXrxYJpNJkjRnzhw99thjeu211zR37lxL/1WrVmn79u3q37+//vOf/1it695779WXX36pFStWaMSIERU7YAAAgOvM4U4Bf/vttzp06JCGDx9uCX+S5O/vr/HjxysvL08xMTFXXc/8+fMlSdOmTbOEP0kaO3asGjVqpMWLFysnJ8fSfvjwYUnSnXfeWWxdffv2lSSlpaVd05gAAAAcicMFwISEBElSVFRUsWXR0dGSpO++++6K67h48aK2b9+uZs2aFTtSaDKZ1KtXL2VnZ2vHjh2W9pYtW0qS1q1bV2x9a9askclkUmRkZLnGAgAA4Igc7hRwcnKyJKlJkybFltWpU0c+Pj6WPqU5dOiQzGZzieu4fN3Jycnq0qWLpEtH+e69916tWrVKrVu3Vrdu3SRdugbwyJEjmjdvntq0aXPF7ebm5io3N9fydWZmpqRL1xfm5+dLklxcXOTq6qrCwkKZzWZL36L2goICGYZhaXd1dZWLi0up7Shd0b+5dCn4u7m5yWw2q7CwsFh7afujovbT5bVIkpvbpW+9goKCMrVXqVKl1NrLOyaUzpH2kyPNPZTOkfaTI809Bzy+5DAqcz+Vh8MFwKK7bf39/Utc7ufnd9U7csuyjsv7SZf+oVeuXKnx48frzTff1O7duy3LRo4cqV69el219mnTpmny5MnF2jdu3Gi5eaRBgwZq3bq1fv75Zx0/ftzSp1mzZmrevLmSkpKsTjWHhYUpODhYmzZt0oULFyztHTt2VK1ata5akzNbu3at5e++vr7q3r27UlJSrPZtzZo11alTJyUnJ2v//v2W9oreTxs3brT6DzsyMlJeXl5WNUpSnz59lJOTo/j4eEubm5ub+vbtq/T0dCUmJto8JpTOkfaTI809lM6R9pMjzT2Jn0+lqcz9FBQUVOY6TMblsd0BREVFKTY2VsnJyWrcuHGx5fXq1VNWVtYVQ+C2bdvUuXNn3X///fr888+LLZ8/f77GjBmjd955R88995wk6Y8//tCwYcO0fft2vf/+++rZs6ck6ZtvvtEzzzwjwzC0fft2hYSElLrdko4A1q9fX+np6ZbQWdG/3Y9+r9RynN7HT3AEsKTamTOlu3zOSDf+UZiKmnvMmZLNf5YjgKWNaewHHAEsyfxnK/cIYHZ2tvz9/ZWRkWHJHaVxuCOARUftSgt4mZmZCgwMtHkdl/eTpKlTp+qrr77Sl19+qXvuucfSPmTIEHl6euree+/VlClTLDeXlMTDw0MeHh7F2qtUqVLsNIqrq2uJp+OKvrnL2o7SlXTqysXFpcTD5KXtj4raT6WdRitPe2m1l3dMKJ0j7SdHmnsonSPtJ0ebeyhZZe+nMtdxzZ+sJJdfn/dnqampysrKKvXaviKNGjWSi4tLqdcKlnSdYdHNHyXd6FHU9uOPP5ZhBAAAAI7N4QJg165dJV26FufPNmzYYNWnNF5eXmrfvr3279+vY8eOWS0zDEOxsbHy9vZW27ZtLe15eXmSSn7US1FbSUf3AAAAbjQOFwB79OihRo0aacmSJVYXQ2ZkZGjq1Klyd3e3ehjz6dOntW/fvmKne8eMGSNJGjdunNW1CXPnztXhw4d1//33y8vLy9LeuXNnSdLkyZOtzqkXFhZq4sSJkko+OggAAHCjcbgT925ublqwYIGio6MVERFh9Sq4Y8eOaebMmVY3YowbN04xMTFatGiR5fVt0qU7d5ctW6YvvvhCR44cUdeuXXXw4EH95z//UcOGDfXPf/7Tarvjx4/Xl19+qc8++0w7d+5U9+7dJUlxcXH69ddf1aRJkzK9gg4AAMDROdwRQOnSkbYtW7aoc+fOWrZsmWbPnq3atWtr6dKlZQ5hLi4u+vLLLzVp0iSlpaXp3Xff1datW/XII48oMTHR6j3A0qXbqnfu3Kknn3xSubm5mjt3rubNm6fCwkK9+OKL2r59+1VvPgEAALgRONxjYP5KMjMzy3w79rXi8Qylm/+svStwTMyZ0jFnSsacKRnzpXTMmZJV9pwpT+5wyCOAAAAAqDwEQAAAACdDAAQAAHAyBEAAAAAnQwAEAABwMgRAAAAAJ0MABAAAcDIEQAAAACdDAAQAAHAyBEAAAAAnQwAEAABwMgRAAAAAJ0MABAAAcDIEQAAAACdDAAQAAHAyBEAAAAAnQwAEAABwMgRAAAAAJ0MABAAAcDIEQAAAACdDAAQAAHAyBEAAAAAnQwAEAABwMgRAAAAAJ0MABAAAcDIEQAAAACdDAAQAAHAyBEAAAAAnQwAEAABwMgRAAAAAJ0MABAAAcDIEQAAAACdDAAQAAHAyBEAAAAAnQwAEAABwMgRAAAAAJ0MABAAAcDIEQAAAACdDAAQAAHAyBEAAAAAnQwAEAABwMgRAAAAAJ0MABAAAcDIEQAAAACdDAAQAAHAyBEAAAAAnQwAEAABwMgRAAAAAJ0MABAAAcDIEQAAAACdDAAQAAHAyBEAAAAAnQwAEAABwMgRAAAAAJ0MABAAAcDIEQAAAACdDAAQAAHAyBEAAAAAnQwAEAABwMgRAAAAAJ0MABAAAcDIEQAAAACdDAAQAAHAyBEAAAAAnQwAEAABwMgRAAAAAJ0MABAAAcDIEQAAAACdDAAQAAHAyBEAAAAAnQwAEAABwMgRAAAAAJ0MABAAAcDIEQAAAACdDAAQAAHAyBEAAAAAnQwAEAABwMgRAAAAAJ+OwAfCHH35Qnz59FBAQIG9vb4WHh2v58uXlWkdubq7+8Y9/qEmTJvL09FRQUJDGjBmjs2fPlvqZxYsXq3379vL29lZgYKDuuusu7dq1y9bhAAAAOAyHDIDx8fHq3LmztmzZosGDB+vRRx9VamqqhgwZorfffrtM6zCbzerXr58mTpyoGjVq6Nlnn1XHjh21YMECdezYUWlpacU+M2XKFD3wwAM6e/asHn30UQ0aNEibNm1Sp06dtHXr1ooeJgAAgF242buAPysoKNDo0aPl4uKiTZs2KSwsTJI0YcIEtW/fXuPHj9fAgQMVHBx8xfXExMRow4YNGjZsmBYvXiyTySRJmjNnjh577DG99tprmjt3rqV/cnKyJk2apKZNmyopKUn+/v6SpMcff1zh4eEaPXq0fvnlF7m4OGRmBgAAKDOHSzPffvutDh06pOHDh1vCnyT5+/tr/PjxysvLU0xMzFXXM3/+fEnStGnTLOFPksaOHatGjRpp8eLFysnJsbQvWrRIBQUFevXVVy3hT5LCwsI0bNgw/fbbb9qyZUsFjBAAAMC+HC4AJiQkSJKioqKKLYuOjpYkfffdd1dcx8WLF7V9+3Y1a9as2JFCk8mkXr16KTs7Wzt27KjQ7QIAANwIHO4UcHJysiSpSZMmxZbVqVNHPj4+lj6lOXTokMxmc4nruHzdycnJ6tKli+XvPj4+qlOnzhX7X0lubq5yc3MtX2dkZEiSzp8/r/z8fEmSi4uLXF1dVVhYKLPZbOlb1F5QUCDDMCztrq6ucnFxKbU97+IVS3Jq587lW/5uMpnk5uYms9mswsLCYu2l7Y+K2k9F+7+Im9ulb72CgoIytVepUqXU2ss7JuZM6S6fM5J995MjzT3mTMkyM+VQ+8mR5l7eRYc7vuQQMjNVqfspOztbkqz2R2kcLgAWhabLT8Nezs/Pz9LHlnVc3q/o77Vq1Spz/5JMmzZNkydPLtbesGHDK34OleOzcfauADca5gzKg/mC8rpec+bChQulZqAiDhcAb2Tjxo3T888/b/nabDbr/Pnzql69utV1iH9FmZmZql+/vlJSUiyBGbgS5gzKizmD8nK2OWMYhi5cuKCgoKCr9nW4AFiUWEs72paZmanAwECb13F5v6K/l6d/STw8POTh4WHVFhAQcMXP/NX4+fk5xTcZKg5zBuXFnEF5OdOcuVpWKeJwJ+mvdL1damqqsrKySr22r0ijRo3k4uJS6jV7JV1n2KRJE2VlZSk1NbVM/QEAAG5UDhcAu3btKknauHFjsWUbNmyw6lMaLy8vtW/fXvv379exY8eslhmGodjYWHl7e6tt27YVul0AAIAbgcMFwB49eqhRo0ZasmSJdu/ebWnPyMjQ1KlT5e7urhEjRljaT58+rX379hU7fTtmzBhJl67Lu/xumLlz5+rw4cO6//775eXlZWl/6KGH5ObmpilTplita/fu3friiy90yy236I477qjo4f5leHh4aOLEicVOgQOlYc6gvJgzKC/mTOlMRlnuFb7O4uPjFR0dLU9PTw0dOlS+vr5auXKljh07ppkzZ+qFF16w9B01apRiYmK0aNEijRo1ytJuNpvVp08fbdiwQeHh4eratasOHjyo//znPwoJCdH27dtVs2ZNq+1OmTJFr732moKDgzVgwABduHBBS5cuVV5enuLi4tS5c+fr9U8AAABQaRzuCKAkRUZGasuWLercubOWLVum2bNnq3bt2lq6dKlV+LsSFxcXffnll5o0aZLS0tL07rvvauvWrXrkkUeUmJhYLPxJ0quvvqrPP/9cNWvW1OzZs7V8+XJ16dJF27ZtI/wBAIC/DIc8AggAAIDK45BHAAEAAFB5CIAAAABOhgAIAADgZAiAAAAAToYACAAA4GQIgAAAAE6GAAgAuOGYzeYS/w78WUlPu2POEAAB2BmPIsW1cHFxUWZmpuXv0qW5xA92/JnJZJIk5eXl6ezZs5L+b85IzhsGeRA0bJafny9XV1erb6iyMAzD8o0J55KZmSk3NzdVrVq1XJ9jzjg3wzD0008/afHixTpy5Ijy8/Pl6+urdu3a6d5771VwcLBVX+YKCgoKtGXLFs2ZM0enT59WRkaGfHx8FBERoQEDBuj222+39HW2OUMAhM0mTJig4OBgRURE6KabbpKXl9dVP+Ns32iw9swzz8jPz0+RkZFq3ry5atWqJTc3tyt+xmw2l/uXDPy1zJs3T5MmTVJqaqoCAwPl4uKic+fOWZZ3795djz76qO666y55enrasVI4irfeektvvvmmzp07p6ZNmyonJ0cpKSmW5S1bttQTTzyhBx54QN7e3nas9PojAMImx44dU8OGDSVJDRo0UFRUlO6++261adNGtWrVUpUqVSx9i36AHzt2TF999ZXatGnDO5ad0OVzplq1aurYsaOioqLUvn17NW7cWNWrV7f0LfpF4eDBg1qwYIE6duyofv362at02NHx48cVGhqqkJAQzZ49WwEBAapdu7b279+vVatW6csvv9SBAwckSUOGDNE//vEPNWnSxM5Vw56OHTumli1bKiwsTHPnzlWdOnVUrVo17d27V7GxsVq/fr3i4uJUWFioDh06aMaMGYqIiLB32dePAdjg448/Nkwmk9G9e3ejffv2hru7u2EymYzbbrvNGD9+vLFp0yYjLS3NKCwstHxm1qxZhslkMr744gs7Vg57mTt3rmEymYz77rvPGDRokFG7dm3DZDIZDRo0MB588EHjs88+M/bs2WNkZmZaPjN79mzDZDIZMTExdqwc9jRhwgSjVq1axvr160vts2bNGqNbt26GyWQyunXrZhw6dOg6VghHM2nSJKNGjRpGbGysYRiG1c+hIlu2bDEGDRpkmEwmo1WrVsauXbsMwzAMs9l8XWu1BwIgbPLcc88ZJpPJ+P77741Tp04ZCxcuNEaNGmU0adLEMJlMhoeHh9GtWzdj5syZxp49e4zU1FTLN1tWVpa9y4cdvPTSS4bJZDK2bdtmZGVlGevWrTMmT55sdOvWzfD19TXc3NyMli1bGk8//bSxevVqY8+ePcaAAQOYM06ub9++xi233GKkpKQYhmEYBQUFhmFc+qFe9HfDMIz8/Hzj1VdfNUwmk/H888/bpVY4hkGDBhmNGjUyjh49ahiG9Zz5cxicP3++YTKZjIEDB173Ou2FAIhrlpmZadx7772GyWQyLl68aGm/ePGisWPHDuO9994z+vfvb9SpU8cwmUxGtWrVjB49ehju7u5G37597Vg57CU7O9t4+OGHDQ8PD+N///ufpT0/P984ePCgsXLlSuO5554zWrdubbi7uxtVq1Y12rRpY5hMJuOuu+6yY+Wwt5deeslwdXU1Tpw4UWqfoh/qZrPZ6N69u9GsWTPj5MmT16tEOJipU6caJpPJ2LlzZ6l9CgoKjPz8fMMwDGPgwIFGcHCwsW/fvutVol1d+apr4Aq8vb01cOBA+fv7KzMzUzVr1pTZbJaHh4duv/123X777Ro5cqR27dqlzZs3a/Pmzdq+fbvy8/P1xBNP2Lt82IGXl5f69++vwMBA5efnS7p0nZ+bm5tuvvlm3Xzzzerdu7cOHjyonTt3auvWrVq9erUk6fHHH7dn6bCzrl276q233tJDDz2k6dOnKzQ0VK6urlZ9TCaT5VrjsLAw7dixQ7///ruCgoLsVDXsqUuXLjKZTHrkkUf01ltvqXPnzsVuUrz8xrJbbrlFa9eu1R9//HG9S7ULbgJBpSjpjs09e/Zo+PDhSklJ0f/+9z/7FAaHZZRwZ3hycrKGDRumgwcPMmecXF5enh555BEtXrxYnTt31rPPPqvevXuXeOdmRkaGnn32Wa1Zs8by3Dc4p3HjxmnGjBlq2LChnnjiCfXt21fBwcHF7hLPzMzU008/rdWrVys9Pd1O1V5fHAGETQoLC4v9Fi5Z/1aVn5+vKlWqKC0tTYcPH9awYcOuZ4lwMKXNmcvDX0FBgdzc3HT06FH98ssveuCBB65niXBA7u7u+te//qUmTZroww8/1KBBg9S6dWsNGTJEPXr0UPXq1eXm5qYaNWpozpw5WrFihUaOHGnvsmFn06ZNU/PmzTVt2jT9/e9/15w5c3TnnXcqIiJCdevWVfXq1eXn56f33ntPK1as0N/+9jd7l3zdEABhk5J+kP9Z0aNgNm/erJycHI0dO7ayy4IDK8ucKXom4J49e1RQUMCcgeUXyaeeekqNGzfW8uXL9e233+qVV16Rq6urmjRpInd3d508eVLnzp1T79699cILL9i7bNhR0VmFBx54QCEhIVq1apU2bNigjz76SB999JFq1KihvLw85ebmKicnR4MHD3aqOcMpYFw3mzZt0vr16zV16lR7l4IbxI8//qitW7fqySeftHcpcDB5eXnaunWrEhIStHfvXp07d06nT59WQECAhgwZoocfflj+/v72LhMOpLCwUL/88ot++OEH7du3T6dPn9ahQ4fUoEED9enTRw888MBVH0j/V0IAxDUrLCyUi4sLb/RAmRiGYTn9y5xBWRUWFio5OVm///675V2/jRo1srqx48KFC8rKylLdunWVm5srDw8PO1YMR/Tna4zz8vLk4uIiNze3Ui9L+asjAKLcUlJSVL9+fcvXZrNZhmFc9Ruo6LouOJ9Dhw7p5ptvtnxtNptlNpuZD7ii/fv3a9y4cVq7dq3y8vLk4eGhwMBABQcHKzw8XFFRUbrjjjvk6+sridcF4ur+PEeKgmFJN6H91REAUS5Hjx5Vo0aNFBUVpWHDhumuu+6yenVXYWGhTCaTXFxcLN9QeXl5cnd3t2PVsKdDhw6pSZMmat68uR5++GE98MADqlOnjmV5YWGhpEvXBhbNmezsbGVlZVku7IfzOXXqlHr37q29e/fqwQcfVI0aNeTm5qa9e/dq8+bNyszMVEBAgPr3768xY8aoQ4cO9i4Zdvb777/r559/Vnh4OEeBy+K6PnUQN7yiB2sW/alRo4YxcuRIY82aNZaHaRbJzc01DMMw5syZY/To0cPYv3+/PUqGnc2YMcNqzhS9puvzzz838vLyrPpePmfat29veS0TnM9rr71mBAYGGgsWLLC05ebmGnl5ecbx48eNuXPnGp07dzZcXFyMW2+91Vi9erVhGM7xCi+U7O9//7thMpmMNm3aGG+88Ybxyy+/lNq3aJ4cOHDA2L17d7H/i5wBARDlctdddxm+vr7GggULjJEjRxpVq1a1/FBv3Lix8fe//91ISkqy+sx9993Ha7yc2IABAwwvLy9jyZIlxoQJE4xbb73VMmeqVKliDB061IiLi7P6DHMGoaGhRu/evY0zZ84YhlFysEtLSzM+/PBDo1q1aoavr6/x66+/Xu8y4UDCwsIMFxcXo1q1apb/YyIjI425c+eW+AaZrKwsY9iwYUZ4eDgBELiSs2fPGu3btzfq1atnacvJyTEWL15s9OjRw+oIT7t27YwPPvjAWL58uVG3bl3j7rvvtmPlsJe0tDSjU6dORp06dSxtubm5xrp164xHHnnEqFu3rmXO1KxZ03jllVeMzz//nDnj5NLT0422bdsa4eHhV+2bn59vLF261DCZTMbYsWOvQ3VwREeOHDGCgoKM8PBwY/fu3cYbb7xhREREGJ6enobJZDJ8fX2NwYMHG6tWrTLOnTtnGIZhJCUlGdWqVTMiIyPtXL19cA0gyiwlJUX333+//Pz8tHr16mLX9p0+fVpLlixRTEyMfvnlF0mSh4eHcnNztXr1avXp08depcNOzpw5o1GjRqmwsFBr166VYRiW50JKUnp6utatW6cVK1YoLi7O6hVMzBnnZPz/60DHjBmjBQsW6KuvvtKdd94pFxcXFRYWlnpN6B133KG8vDytX79e1apVu85Vw97i4+PVs2dPPfnkk3r//fclSVlZWdq2bZvWr1+vuLg47dmzR5IUFBSkQYMGKScnR/PmzdPXX3+tvn372rN8uyAAoszy8/O1ZcsWeXp6qkOHDpYbPcxms+XGjyIHDhzQBx98oI8//liBgYE6d+6cHSuHPR08eFC5ubm65ZZbrObMnx8hlJKSok8//VTTp0+Xh4eHzp8/b8eqYW/r1q1T3759LW/+iIqKsiwrunGoaA5lZGRo1KhR+vXXX7V//357lQw7+umnnzRo0CA99dRTeuqpp4o92iU1NVUJCQlav369Nm3apKNHj0qSAgICnPb/Gu6XR5lVqVJFkZGRlvAnXXp9l6urq+UHe0FBgQoLC9W0aVONHDlSXl5eGjhwoJ0rhz01btxYLVq0KDZnih69UFhYqMLCQtWvX1+9evWSJA0aNMieJcMB3Hnnnfr888+VkZGh3r17q3v37lq+fLmys7Pl6upq9cN969atSkpKUteuXe1YMewpNDRUO3futLw2smh+mM1mSVKdOnU0dOhQffrpp9qyZYueeOIJSXLqV5PyfAWU2eUP8S3pwZkmk8nq9Mxnn32mnJwcjRkz5nqXihtEURgs8vnnnzNnYDFgwABJ0jvvvKOEhAQlJCSoVq1a6tq1q3r16iUPDw/98ssv+uSTT+Th4aFnnnnGzhXDnoqeB3m5ol88i848uLq6KigoyHKZwMMPP3xda3QknAJGpcjMzNTYsWMVHx+v1NRUe5eDG0B2draeeOIJrV27VmfPnrV3OXAghmHo66+/1rx587Rx40YVFBRYLe/YsaNee+013XnnnXaqEDeSw4cP695779WFCxd05MgRe5djNwRAlMnZs2e1Z88eHThwQFlZWWrfvr2aN29u9aDePx8VzM3N1dmzZ63eGgLnca1vZcjMzJSfn18lVIQbjXHpSRVW8ygjI0MJCQk6fPiwgoKC5OPjo3bt2qlWrVp2rBQ3kiNHjmjs2LHq2rWrXn31VXuXYzcEQFzVunXr9M9//lOJiYlW7dWqVVPPnj01ZMgQ3X333byxAaUqSxgsKCgodkoYzqe097Je/pYh4HLX+i5fZ30HcBECIK4oJSVF3bp1U3Z2tkaNGqXIyEgdPnxYP/74o3766Sf9/PPPys3NVYsWLTRu3DgNHDhQ7u7uvJPTiZ05c0ZvvvmmoqKi1KFDBwUEBFiWFf1342zv3MTVlfSO1j8f/ftze9FNRPzy6ZzKOmf+jNeTXsJ3Da5o7ty5+v3337VgwQLdd999VstOnDihbdu26auvvtKSJUv0wAMP6MSJE3rppZcIf07s448/1rvvvqtVq1bp1ltvVbdu3dS1a1e1atXK6v2cZrNZhmHI1dVVCQkJunjxonr37m3HymFPc+fOVUJCgkaMGKGuXbvKx8fH8otC0Z2cRY99KWr/841ncC5lnTN/Rvi7hCOAuKLw8HB5eXnp3//+t2rUqFHqabr4+Hi98MIL+vXXX/Xxxx879Z1Vzq5169b69ddf1aZNG+3atUv5+fkKDg5W586dFRkZqc6dO6t58+aW/n/88YeGDRum1atXKzs7W56ennasHvbSsGFDHTt2TB4eHgoNDVVUVJT69OmjDh06WB0xLigokJubm/744w/NmzdPoaGhioyMtGPlsBfmjG0IgChVVlaW+vfvrxMnTmjnzp2qWrWq1SH3Px9u//HHH9WjRw916dJFX375peWJ/nAeKSkpioiIUPXq1ZWYmKidO3dq7dq1+uqrr/Tzzz/LxcVFLVq0UEREhCIiIhQdHa39+/frnnvuUbt27fTVV1/Zewiwg7179+q2227T7bffrsDAQH3zzTeSJG9vb3Xu3Fl9+vRRVFSU1S8OW7ZsUUREhDp16qQtW7bYq3TYCXOmAlTme+Zw43v55ZcNk8lkfPLJJ8WWXf5y9sLCQsMwDKNfv35G06ZNjaNHj163GuE4tm/fblSrVs0YOXKkYRiGUVBQYBQWFhpnzpwx1q1bZzz66KNGcHCwYTKZjKpVqxoRERGW90h//fXX9i0edvPFF18YJpPJeOeddwzDMIz9+/cbM2bMMMLCwizviq5bt64xbNgw47PPPjPOnz9vvP3224bJZDJWr15t5+phD8wZ2xEAcUUnTpwwbrvtNsNkMhlPPfWUsXPnTiMnJ8eqT35+vmEYhpGRkWEMGjTIaNCggT1KhQNITk427rvvPmPx4sUlLs/LyzOOHj1q/Otf/zIGDx5sVKtWzTCZTEZgYOB1rhSOZO7cuYbJZDLWrl1bbFlSUpLx3HPPGfXr17f8YG/atKlRp04dw9/f//oXC4fAnLEdARBXtWrVKqNhw4aGyWQy2rZta7zxxhtGfHy8cfToUasw+Pnnnxs1a9Y0xo4da8dqYW//+9//jPT09Cv2KTpiPGfOHMNkMhmPP/749SgNDshsNhuJiYnGc889Zxw8eNCq/XI5OTnG6tWrjZEjRxr+/v6GyWQynnzyyetdLhwAc6ZicA0gSmT86fq98+fPa9q0aVq+fLlSUlJUs2ZNtWzZUkFBQapatapycnK0fPlyNWzYUP/973/VrFkzO1YPe/jznJGu/uy2l156STNnztSOHTvUpk2b61EmHFRWVpbc3d1LvEPzz3PrySef1Mcff6xdu3YpLCzsOlYJR8KcsQ0BEKUq+gY6ceKEgoKC5OLiol9++UWrV69WQkKCfvvtN6WkpEiSAgMDFRYWpg8++EAtWrSwc+Wwl6I5k5qaqlq1alkFv8LCQstjPKRLjxHq27evTp06pbS0NHuVjBtE0dw6dOiQhgwZooyMDCUnJ9u7LDgw5syV8QAlFFNQUKCtW7dq4cKFOnDggEwmk6pWrap27dpp8ODBeuWVV/Tyyy8rJSVFOTk5Onz4sJo3b6769evLzc2Nu3+d0J/njIuLi7y8vBQaGqoBAwaoU6dOxR4d5OnpqVGjRikoKMhOVeNGUvR/ym+//aZdu3bpxRdftHNFcHTMmSvjCCCKmTlzpt544w1duHBBjRs3lqurq/bv329Zfuutt+rxxx/XwIEDef8mJF19zjRv3lyjR4/WsGHDVKdOHUt7Xl6e3NzceHA4yvyL45kzZ7R+/Xrdfffdqlat2nWoDI6KOWMbAiCsHDlyRLfddpvatGmjmJgYubu7q3bt2kpNTdXXX3+tf//730pISJAkRUZGasaMGWrbtq19i4ZdlWfOdO/eXW+++SbX+0E5OTk6fvy4GjRoIC8vr3J91tnf4eqsmDMViwAIKxMmTNDcuXO1ZMkS9ejRQ1Lx37L27NmjmTNnavny5QoODtbixYt1++2326tk2Jktc4bLBZzX9OnTtXLlSt13330KDw9Xs2bNVLt27Sv+kE5LS1NgYCCvf3NSzJmKRQCElQEDBmj37t2Kj49XgwYNLK/QMQxDZrPZ6hvt/fff13PPPaeRI0dq0aJFdqwa9sScwbW46aabdOrUKbm6usrf31+dOnVSVFSUOnTooEaNGql69epW/bOzszVp0iSdO3dO8+fP52iOE2LOVCwiMay0bt1aq1atUlZWliRZfmu6/P2/RUdtnnnmGW3evFnffvutDh8+rEaNGtmtbtgPcwbldeDAAWVkZKhjx44aPny4YmNjlZiYqNWrV6tBgwbq1q2bevbsqdatW6tevXoKCAjQL7/8ovnz56tbt278IHdCzJmKRwCElaIXZN9///16++23dccdd5T4jKWi6ymaNWumdevWWX74w/kwZ1BeBw4c0MWLFxUVFaUnnnhCd911l/bv36/ExER9++23WrlypRYvXqxbb71V3bt3V+/evRUXF6fMzEyNHj3a3uXDDpgzleB6PG0aN46CggLjhRdeMEwmk3HLLbcYs2bNMlJTU0vse/78eWPEiBFGzZo1r3OVcCTMGZTXv//9b8NkMhnLli2zas/LyzOSk5ONFStWGM8884wRGhpquLu7G97e3kbVqlV5ZaATY85UPK4BRInmzp2rt956S4cPH1ZQUJD69++vO++8U/Xr15erq6sCAgL04Ycf6r333tPjjz+ut99+294lw86YMygrwzC0b98+eXp6qmHDhiXeDJSdna0DBw5o//79WrRokWJjY/Xkk0/qgw8+sFPVsCfmTMUjAKJEhmHo4MGDmj9/vpYuXaoTJ05IkmrVqqUqVaro9OnTMpvNGjZsmGbMmKGbbrrJzhXD3pgzqAgl/WB/+umnNWvWLO3cuVOtW7e2U2VwVMyZa0MAxFVlZ2crKSlJX331lU6dOqWzZ8/Kz89PgwcP1oABA+Tp6WnvEuFgmDOwldlslouLi44ePap+/frp999/1/Hjx+1dFhwYc6Z8uAkEV+Xt7a3IyEhFRkYqPz9fVapUsXdJcHDMGdiq6O0wJ0+eVH5+vh5//HE7VwRHx5wpH44AAgAclmEYOnHihKpVqyZvb297l4MbAHOmbAiAAAAAToY3sAMAADgZAiAAAICTIQACAAA4GQIgAACAkyEAAgAAOBkCIAAAgJMhAAIAADgZAiAAAICTIQACAAA4mf8Hk3XEQRKuXpAAAAAASUVORK5CYII=\n",
      "text/plain": [
       "<Figure size 700x500 with 1 Axes>"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Run the algorithm on a simulator, and print a histogram of the result\n",
    "# The logical expression can automatically be transformed into a form suitable for Grover's algorithm\n",
    "oracle = PhaseOracle(log_expr)\n",
    "backend = Aer.get_backend('qasm_simulator')\n",
    "grover = Grover(quantum_instance=backend)\n",
    "problem = AmplificationProblem(oracle)\n",
    "result = grover.amplify(problem)\n",
    "plot_histogram(result.circuit_results)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "source": [
    "The result shows that the assignments 0011, 0111, 1100, 1110 for David-Carol-Bob-Alice are potential solutions to the problem.  \n",
    "Whether or not these are correct solutions to the problem can be verified efficiently, as 3-SAT is in NP.  \n",
    "Note that the variables in the histogram are in reverse order: David-Carol-Bob-Alice instead of Alice-Bob-Carol-David.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "slideshow": {
     "slide_type": "slide"
    }
   },
   "source": [
    "### Now it's your turn to play!\n",
    "\n",
    "Create and implement your own scenario that can be modeled as a boolean satisfiability problem using Grover search. Have fun with it, and carry on with your quantum computing journey!"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "pycharm": {
     "name": "#%%\n"
    },
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [],
   "source": [
    "# Define the formal logical expression corresponding to our \"party problem\"\n",
    "log_expr = '((A & C) | (B & D)) & ~(A & D)'"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "pycharm": {
     "name": "#%%\n"
    },
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAoAAAAHUCAYAAACqOplfAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjUuMywgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy/NK7nSAAAACXBIWXMAAA9hAAAPYQGoP6dpAABWcElEQVR4nO3deVyU9f7//+ewCAgIuIcp6HFNU9y3XHAB08rM3Tpq9U3bFzsd08qljlvZaTlWbql00rT0eDIXFAnc09Q8mqXiCi4oqIEQss31+8Mf83ECFJzBGZvH/XbzdmPe13uu63U5b+DJtb1NhmEYAgAAgMtwc3QBAAAAuL0IgAAAAC6GAAgAAOBiCIAAAAAuhgAIAADgYgiAAAAALoYACAAA4GIIgAAAAC7Gw9EF/JmZzWadPXtW/v7+MplMji4HAAD8iRmGoStXrig4OFhubjc+xkcALENnz55VzZo1HV0GAABwIUlJSbr77rtv2MdpA+CPP/6oiRMnavv27crNzdW9996rMWPGaNCgQSV6/7p16xQVFaV9+/YpOTlZOTk5qlWrljp27KixY8eqfv36Vv0TEhL0zTffKDo6WkePHlVqaqqqVaum8PBwjR8/Xg0bNiz1Pvj7+0u69kFUqFCh1O8HAAAoqfT0dNWsWdOSP27E5IxzAcfFxSkyMlLe3t4aMmSI/P39tWLFCp06dUozZ87Uq6++etN1vPDCC/ruu+/Utm1bBQcHy9PTU7/++qvWrVsnDw8PrV27Vt26dbP0HzJkiJYtW6YmTZrovvvuU4UKFXTgwAGtW7dOPj4+io6OVufOnUu1H+np6QoICFBaWhoBEAAAlKnS5A6nC4B5eXlq2LChTp8+rR9++EFhYWGSpLS0NLVp00YnT57UkSNHFBIScsP1XL16Vd7e3oXaY2Nj1aNHD7Vq1Uo//vijpX3RokVq1qyZmjdvbtV/6dKlGjp0qO655x4dPHiwVPtCAAQAALdLaXKH090F/P333+vYsWMaNmyYJfxJUkBAgMaPH6+cnBxFRUXddD1FhT9J6t69u4KCgnT06FGr9pEjRxYKf9K1I4P169fXL7/8otTU1NLtDAAAgBNyugAYHx8vSYqIiCi0LDIyUpK0adOmW17/jh07dPnyZTVp0qTE7/H09JQkeXg47SWTAAAAJeZ0iSYhIUGSVK9evULLqlevLj8/P0ufktiwYYO2b9+u7OxsJSQkaPXq1apcubI++OCDEr1/165dOnjwoFq3bq3AwMAb9s3OzlZ2drbldXp6uiQpNzdXubm5kiQ3Nze5u7srPz9fZrPZ0regPS8vT9eflXd3d5ebm1ux7QXrLVAQUvPy8krU7unpKbPZrPz8fEubyWSSh4dHse3F1c4+sU/sE/vEPrFP7JPj9qk0nC4ApqWlSbp2yrcoFSpUsPQpiQ0bNuj999+3vK5bt66WLl2qli1blqiWESNGyM3NTe++++5N+0+bNk2TJ08usoby5ctLkmrVqqXmzZtr//79SkxMtPRp0KCBGjZsqF27diklJcXSHhYWppCQEG3evFlXrlyxtLdv315Vq1bVhg0brAZYeHi4fHx8tHbtWqsaevfuraysLMXFxVnaPDw81KdPH6WmpmrHjh2Wdn9/f3Xr1k1JSUnat2+fpb1KlSrq0KGDEhISdPjwYUs7+8Q+sU/sE/vEPrFPjt+n4OBglZTT3QQSERGhmJgYJSQkqG7duoWW16hRQxkZGaUKgZKUkZGhX375RW+//bY2btyoBQsWaNiwYcX2z8rKUp8+fRQXF6cpU6Zo/PjxN91GUUcAa9asqdTUVMvFmK721wj7xD6xT+wT+8Q+sU+3Z58yMzPv3LuABw4cqOXLl2v37t1FHqXz9/dXUFCQVeotjby8PLVq1UpHjx7ViRMnVKVKlUJ9rl69qoceekgxMTEaN26cpk6dekvb4i5gAABwu9zRdwEXXPtX1HV+ycnJysjIKPL6wJLy8PBQeHi4MjMztXv37kLLs7KyLOHv73//+y2HPwAAAGfldAGwS5cukq5dN/dH69evt+pzq86ePSvp/+7uLZCVlaW+ffsqJiZGf/vb3zRjxgybtgMAAOCMnC4Adu/eXXXq1NGSJUusLoZMS0vT1KlTVa5cOQ0fPtzSfu7cOR06dKjQNYFFHd2TroXIlStXKjAwUO3bt7e0X7161RL+xowZo/fee8++OwYAAOAknO4uYA8PD82fP1+RkZHq3LlzkVPBhYaGWvqPGzdOUVFRWrhwoUaOHGlpb926tZo0aaKmTZvq7rvvVmZmpvbv368tW7bI09NTCxYskK+vr6X/008/rZiYGFWvXl3+/v6aNGlSodpGjhxptW0AAIA7kdMFQOnabdVbt27VxIkTtWzZMuXm5uree+/VjBkzNHjw4BKtY+rUqYqLi9OmTZuUkpIiNzc31apVS6NGjdLLL7+sRo0aWfU/efKkpGvXGRb1KBdJ6tq1KwEQAADc8ZzuLuA/E+4CBgAAt8sdfRcwAAAAyhYBEAAAwMUQAAEAAFwMARAAAMDFEAABAABcDAEQAADAxRAAAQAAXAwBEAAAwMUQAAEAAFwMARAAAMDFEAABAABcDAEQAADAxRAAAQAAXAwBEAAAwMUQAAEAAFwMARAAAMDFEAABAABcDAEQAADAxRAAAQAAXAwBEAAAwMUQAAEAt8Unn3yi0NBQeXt7q23bttq1a1exfefNm6dOnTopKChIQUFB6tGjR6H+JpOpyH/vvfeepc+UKVPUoUMHlS9fXoGBgWW1a8AdhwAIAChzy5Yt05gxYzRx4kTt3btXzZo1U2RkpC5cuFBk//j4eA0dOlRxcXHasWOHatasqYiICJ05c8bS59y5c1b/FixYIJPJpP79+1v65OTkaODAgXrmmWfKfB+BO4nJMAzD0UX8WaWnpysgIEBpaWmqUKGCo8sBAIdp27atWrdurVmzZkmSzGazatasqRdeeEGvv/76Td+fn5+voKAgzZo1S8OHDy+yz8MPP6wrV64oNja20LJFixbp5Zdf1m+//WbTfgDOrDS5gyOAAIAylZOToz179qhHjx6WNjc3N/Xo0UM7duwo0Tp+//135ebmqmLFikUuP3/+vNasWaMnn3zSLjUDf3YEQABAmUpNTVV+fr6qVatm1V6tWjUlJyeXaB1jx45VcHCwVYi8XlRUlPz9/fXII4/YXC/gCjwcXQAAADcyffp0LV26VPHx8fL29i6yz4IFC/Too48WuxyANQIgAKBMVa5cWe7u7jp//rxV+/nz51W9evUbvnfmzJmaPn26Nm7cqKZNmxbZZ8uWLTp8+LCWLVtmt5qBPztOAQMAylS5cuXUsmVLq5szzGazYmNj1b59+2Lf9+677+qdd95RdHS0WrVqVWy/zz//XC1btlSzZs3sWjfwZ8YRQABAmRszZoxGjBihVq1aqU2bNvrwww+VmZmpxx9/XJI0fPhw1ahRQ9OmTZMkzZgxQxMmTNCSJUsUGhpquVbQz89Pfn5+lvWmp6frm2++0fvvv1/kdhMTE3Xp0iUlJiYqPz9f+/btkyTVrVvXaj2AqyEAAgDK3ODBg5WSkqIJEyYoOTlZYWFhio6OttwYkpiYKDe3/zsp9dlnnyknJ0cDBgywWs/EiRM1adIky+ulS5fKMAwNHTq0yO1OmDBBUVFRltfNmzeXJMXFxalr16522jvgzsNzAMsQzwEEAAC3C88BBAAAQLEIgAAAAC6GAAgAAOBiCICw+OSTTxQaGipvb2+1bdtWu3btKrbvvHnz1KlTJwUFBSkoKEg9evQosv+vv/6qhx56SAEBAfL19VXr1q2VmJhoWX716lU999xzqlSpkvz8/NS/f/9CzwoDAAD2RQCEJGnZsmUaM2aMJk6cqL1796pZs2aKjIzUhQsXiuwfHx+voUOHKi4uTjt27FDNmjUVERGhM2fOWPocO3ZM9913nxo2bKj4+Hjt379fb731ltWT+l955RV99913+uabb7Rp0yadPXuWqZwAAChj3AVchu6ku4Dbtm2r1q1ba9asWZKuPaS1Zs2aeuGFF/T666/f9P35+fkKCgrSrFmzNHz4cEnSkCFD5OnpqX//+99FvictLU1VqlTRkiVLLI96OHTokBo1aqQdO3aoXbt2dto7AAD+/LgLGKWSk5OjPXv2WE2y7ubmph49emjHjh0lWsfvv/+u3NxcVaxYUdK1ALlmzRrVr19fkZGRqlq1qtq2bav//ve/lvfs2bNHubm5Vttt2LChatWqVeLtAgCA0iMAQqmpqcrPz7c8kLVAtWrVLE/fv5mxY8cqODjYEuYuXLigjIwMTZ8+Xb169dKGDRvUr18/PfLII9q0aZMkKTk5WeXKlVNgYOAtbxcAAJQeM4HAZtOnT9fSpUsVHx9vub7PbDZLkvr27atXXnlFkhQWFqbt27dr9uzZ6tKli8PqBQDA1XEEEKpcubLc3d0L3X17/vx5Va9e/YbvnTlzpqZPn64NGzaoadOmVuv08PDQPffcY9W/UaNGlruAq1evrpycHP3222+l3i4AALh1BECoXLlyatmypWJjYy1tZrNZsbGxat++fbHve/fdd/XOO+8oOjparVq1KrTO1q1b6/Dhw1btR44cUUhIiCSpZcuW8vT0tNru4cOHlZiYeMPtAgAA23AKGJKkMWPGaMSIEWrVqpXatGmjDz/8UJmZmXr88cclScOHD1eNGjU0bdo0SdKMGTM0YcIELVmyRKGhoZZr9vz8/OTn5ydJeu211zR48GB17txZ4eHhio6O1nfffaf4+HhJUkBAgJ588kmNGTNGFStWVIUKFfTCCy+offv23AEMAEAZIgBCkjR48GClpKRowoQJSk5OVlhYmKKjoy03hiQmJsrN7f8OGH/22WfKycmxPL6lwMSJEzVp0iRJUr9+/TR79mxNmzZNL774oho0aKAVK1bovvvus/T/4IMP5Obmpv79+ys7O1uRkZH69NNPy36HAQBwYTwHsAzdSc8BBAAAdzaeAwgAAIBiEQABAABcDAEQAADAxRAAAQAAXAx3AQMAbuipDx1dgXOa97KjKwBuHUcAAQAAXAwBEAAAwMUQAAEAAFwMARAAAMDFEAABAABcDAEQAADAxRAAAQAAXAwBEAAAwMUQAAEAAFwMARAAAMDFEAAB3JJPPvlEoaGh8vb2Vtu2bbVr165i+86bN0+dOnVSUFCQgoKC1KNHj0L9J02apIYNG8rX19fSZ+fOnVZ99u7dq549eyowMFCVKlXSqFGjlJGRUSb7BwB/ZgRAAKW2bNkyjRkzRhMnTtTevXvVrFkzRUZG6sKFC0X2j4+P19ChQxUXF6cdO3aoZs2aioiI0JkzZyx96tevr1mzZunAgQPaunWrQkNDFRERoZSUFEnS2bNn1aNHD9WtW1c7d+5UdHS0Dh48qJEjR96OXQaAPxWTYRiGo4v4s0pPT1dAQIDS0tJUoUKFMtkGk7QXj4nay07btm3VunVrzZo1S5JkNptVs2ZNvfDCC3r99ddv+v78/HwFBQVp1qxZGj58eJF9Cr5/Nm7cqO7du2vu3Ll66623dO7cObm5Xfvb9cCBA2ratKkSEhJUt25d++0grPBzpmj8jIGzKU3u4AgggFLJycnRnj171KNHD0ubm5ubevTooR07dpRoHb///rtyc3NVsWLFYrcxd+5cBQQEqFmzZpKk7OxslStXzhL+JMnHx0eStHXr1lvdHQBwSQRAAKWSmpqq/Px8VatWzaq9WrVqSk5OLtE6xo4dq+DgYKsQKUmrV6+Wn5+fvL299cEHHygmJkaVK1eWJHXr1k3Jycl67733lJOTo8uXL1uONp47d84OewYAroMACOC2mj59upYuXaqVK1fK29vball4eLj27dun7du3q1evXho0aJDlusLGjRsrKipK77//vsqXL6/q1aurdu3aqlatmtVRQQDAzfFTE0CpVK5cWe7u7jp//rxV+/nz51W9evUbvnfmzJmaPn26NmzYoKZNmxZa7uvrq7p166pdu3b6/PPP5eHhoc8//9yyfNiwYUpOTtaZM2d08eJFTZo0SSkpKapTp459dg4AXAQBEECplCtXTi1btlRsbKylzWw2KzY2Vu3bty/2fe+++67eeecdRUdHq1WrViXaltlsVnZ2dqH2atWqyc/PT8uWLZO3t7d69uxZ+h0BABfm4egCANx5xowZoxEjRqhVq1Zq06aNPvzwQ2VmZurxxx+XJA0fPlw1atTQtGnTJEkzZszQhAkTtGTJEoWGhlquFfTz85Ofn58yMzM1ZcoUPfTQQ7rrrruUmpqqTz75RGfOnNHAgQMt2501a5Y6dOggPz8/xcTE6LXXXtP06dMVGBh42/8PAOBORgAEUGqDBw9WSkqKJkyYoOTkZIWFhSk6OtpyY0hiYqLVdXmfffaZcnJyNGDAAKv1TJw4UZMmTZK7u7sOHTqkqKgopaamqlKlSmrdurW2bNmixo0bW/rv2rVLEydOVEZGhho2bKg5c+bor3/96+3ZaQD4E+E5gGWI5wA6Fs/oAuyDnzNF42cMnA3PAQQAAECxCIAAAMAp2XPO8dzcXI0dO1b33nuvfH19FRwcrOHDh+vs2bNW63GVOccJgAAAwOnYe87x33//XXv37tVbb72lvXv36j//+Y8OHz6shx56yLIOV5pznGsAyxDXADoW1+cA9sHPmaLxM6Zs3Y45x3/88Ue1adNGp06dUq1ate74Oce5BhAAANyxbsec45KUlpYmk8lkeZSUK805TgAEAABOpSznHC9w9epVjR07VkOHDrUcLXOlOccJgAAA4E/lRnOOS9duCBk0aJAMw9Bnn31maXelOcf/XHsDAADueGU553hB+Dt16pRiYmIKXSvnKnOOEwABAIBTKas5xwvCX0JCgjZu3KhKlSoVu64/+5zjThsAf/zxR/Xu3VuBgYHy9fVVu3bt9PXXX5fovYZhaN26dXrmmWfUtGlTBQQEqHz58mrWrJmmTp2qq1evlmg9zzzzjEwmk0wmU4mvOQAAALYbM2aM5s2bp6ioKP3666965plnCs05Pm7cOEv/GTNm6K233tKCBQssc44nJydbnuGXm5urAQMGaPfu3Vq8eLHy8/MtfXJycizrmTVrlvbu3asjR47ok08+0fPPP69p06b96eYcd8q5gOPi4hQZGSlvb28NGTJE/v7+WrFihQYPHqykpCS9+uqrN3x/dna2evfuLS8vL3Xt2lWRkZG6evWq1q9frzfeeEP//e9/FR8fr/Llyxe7jpiYGM2ePVu+vr7KzMy09y4CAIAbsPec42fOnNGqVaskSWFhYVZ94uLi1LVrV0muM+e40z0HMC8vTw0bNtTp06f1ww8/WD6ktLQ0tWnTRidPntSRI0cUEhJS7Dpyc3P17rvv6tlnn1VQUJBVe//+/fXdd9/p3Xff1WuvvVbk+9PS0tSkSRO1a9dOKSkp2rRpk86dO3fT6w7+iOcAOhbP6ALsg58zReNnDJzNHf0cwO+//17Hjh3TsGHDrBJ6QECAxo8fr5ycHEVFRd1wHZ6ennrjjTeswl9Be8Hh4k2bNhX7/pdeeklZWVn65JNPbn1HAAAAnJTTnQKOj4+XJEVERBRaFhkZKenG4e1mPD09JUkeHkXv+nfffaeoqCgtWbJEVatWveXtAAAAOCunC4AJCQmSpHr16hVaVr16dfn5+Vn63IoFCxZIKjpgXrx4UU899ZQefvhhDR06tNTrzs7OVnZ2tuV1enq6pGunnnNzcyVde5K5u7u78vPzZTabLX0L2vPy8nT9WXl3d3e5ubkV247iFfyfS5LJZJKHh4fMZrPy8/MLtRf3edjrc7q+Fun//gDJy8srUbunp2extbNP7FNZ7xOK50yf059x7LFPpdun0nC6AJiWlibp2infolSoUMHSp7TWrVunOXPmqFGjRnryyScLLX/22WeVk5Nj9VDI0pg2bZomT55cqH3Dhg2WG05q1aql5s2ba//+/UpMTLT0adCggRo2bKhdu3YpJSXF0h4WFqaQkBBt3rxZV65csbS3b9+eI5Q3sXbtWsvX/v7+6tatm5KSkrRv3z5Le5UqVdShQwclJCTo8OHDlnZ7f04bNmyw+kEQHh4uHx8fqxolqXfv3srKylJcXJylzcPDQ3369FFqaqrVFEjsE/t0u/YJxXOmz+nPOPbYp9LtU3BwsErK6W4CiYiIUExMTLGTLteoUUMZGRmlDoE//vijunfvLg8PD23ZskWNGze2Wr5s2TINGTJEX3zxhdXdPl27di3xTSBFHQGsWbOmUlNTLRdj2vuvES7OLt6nz3EEsKjaGTPFu37MSM73172jxh5jpmjzXuYIIPvkXPuUmZlZ4ptAnO4IYMGRv+ICXnp6eqGbO25m9+7dioiIkJubm9avX18o/F26dEnPPfec+vTpY9Ot3l5eXvLy8irU7unpWeg0iru7u9zd3Qv1Le7axOLaUbyiTl25ubkVeZi8uM/DXp9TcafRStNeXO2l3ScUz5k+J2caeyieM31Of8axxz6Vfp9KyukuIiu49q+o6/wKHuhY1PWBxdm9e7d69uwps9ms9evXq3Xr1oX6JCYm6uLFi1qzZo3lwc8F/wpuOLnrrrtkMpmsDs8CAADciZzusFKXLl00bdo0bdiwQUOGDLFatn79ekufkigIf/n5+Vq/fr3atm1bZL9KlSoVeU2gJK1Zs0bJyckaNmyYfHx8bjhtDAAAwJ3A6QJg9+7dVadOHS1ZskQvvvii1YOgp06dqnLlymn48OGW/ufOnVNaWpruuusuqxtH9uzZo549eyovL0/R0dE3nDuwZs2amj9/fpHLunbtquTkZL3//vulfhA0AACAM3K6AOjh4aH58+crMjJSnTt3tpoK7tSpU5o5c6ZCQ0Mt/ceNG6eoqCgtXLhQI0eOlHTtmr6ePXvqt99+U69evRQTE6OYmBir7QQGBurll1++fTsGAADgJJwuAErXbqveunWrJk6cqGXLlik3N1f33nuvZsyYocGDB9/0/enp6bp8+bIkKTo6WtHR0YX6hISEEAABAIBLcsoAKElt2rTRunXrbtpv0aJFWrRokVVbaGio7PV0m4KZSQAAAP4snO4uYAAAAJQtAiAAAICLIQACAAC4GKe9BhAAANyZmD6waPNednQF/4cjgAAAAC6GAAgAAOBiCIAAAAAuhgAIAADgYgiAAAAALoYACAAA4GIIgAAAAC6GAAgAAOBiCIAAAAAuhgAIAADgYgiAAAAALoYACAAA4GIIgAAAAC6GAAgAAOBiCIAAAAAuhgAIAADgYgiAAAAALoYACAAA4GIIgAAAAC6GAAgAAOBiCIAAAAAuhgAIAADgYjzKYqUnT55UTEyMvL291a9fP/n5+ZXFZgAAAHALbDoCOHXqVNWuXVuXL1+2tMXHx6tJkyZ6+umnNXLkSLVo0UKXLl2yuVAAAADYh00B8L///a9CQ0MVFBRkaRs7dqzMZrMmT56sZ555RkePHtWHH35oa50AAACwE5sC4MmTJ3XPPfdYXp89e1Y//vijnnvuOb355puaNWuWunfvrpUrV9pcKAAAAOzDpgCYnp6uwMBAy+vNmzfLZDLpwQcftLS1aNFCiYmJtmwGAAAAdmRTAKxWrZpOnTpleR0TEyMvLy+1bdvW0nb16lWZTCZbNgMAAAA7suku4NatW+vbb7/V6tWr5e3trWXLlik8PFxeXl6WPidOnFBwcLDNhQIAAMA+bDoCOH78eOXl5alv376KjIzU1atXNX78eMvy7Oxsbd682eqIIAAAABzLpiOALVq00A8//KB///vfkqRBgwapTZs2luU//fSTwsPDNWzYMNuqBAAAgN3Y/CDoZs2aqVmzZkUua9euHXcAAwAAOBm7zQSSkZGhI0eOKDMzU506dbLXagEAAGBnNs8FfPLkSfXt21dBQUFq3bq1wsPDLcu2bdume+65R/Hx8bZuBgAAAHZiUwBMTExUu3bttHbtWvXt21ft27eXYRiW5W3btlVqaqq++uormwsFAACAfdgUACdOnKjLly9r06ZNWr58uXr27Gm13MPDQ506ddK2bdtsKhIAAAD2Y1MAXL9+vfr166cOHToU2yckJERnzpyxZTMAAACwI5sC4KVLlxQaGnrDPoZhKDs725bNAAAAwI5sngouISHhhn0OHDigWrVq2bIZAAAA2JFNAbBnz55avXq19u/fX+TyLVu26Pvvv1fv3r1t2QwAAADsyKYA+Oabb8rHx0edO3fWlClTdPToUUnSunXr9NZbb6lXr16qXLmyXnvtNbsUCwAAANvZ9CDo0NBQrV+/XkOGDNFbb70lk8kkwzD0wAMPyDAM1apVS8uXL9ddd91lr3oBAABgI5tnAmnbtq0SEhL03XffaefOnbp06ZIqVKigtm3bqm/fvipXrpw96gQAAICd2GUqOA8PD/Xr10/9+vWzx+oAAABQhmyeCg4AAAB3llIdAfziiy8kSf369ZO/v7/ldUkMHz68dJUBAACgTJQqAI4cOVImk0nt2rWTv7+/5fWNGIYhk8lEAAQAAHASpQqACxYskMlkstzVu3DhwjIpCgAAAGWn1EcArzdixAh71gIAAIDbwKabQDZv3qzExMQb9klKStLmzZtt2QwAAADsyKYAGB4erkWLFt2wzxdffKHw8HBbNgMAAAA7sikAGoZx0z5ms/mmN4oAAADg9inz5wAmJCQoICCgrDcDAACAEir1TCBPPPGE1ev//ve/OnnyZKF++fn5luv/7r///lsuEAAAAPZV6gB4/TV/JpNJ+/bt0759+4rsazKZ1Lp1a33wwQe3Wh8AAADsrNQB8MSJE5KuXf9Xp04dvfzyy3rppZcK9XN3d1dQUJB8fX1trxIAAAB2U+oAGBISYvl64cKFCgsLs2oDAACAcyt1ALweD4IGAAC485QqABY80LlNmzby9vYu1QOeO3fuXLrKAAAAUCZKFQC7du0qk8mkX3/9VfXr17e8Lon8/PxbKhAAAAD2VaoAOGHCBJlMJlWuXNnqNQAAAO4cpQqAkyZNuuFrAAAAOL8ynwkEAAAAzoUACAAA4GJKdQq4W7dut7QRk8mk2NjYW3ovAAAA7KtUATA+Pv6WNsKNIgAAAM6jVAHQbDaXVR0AAAC4TbgGEAAAwMUQAAEAAFwMU8EBAAC4GKaCAwAAcDFMBQcAAOBimAoOAADAxXATCAAAgIsp1RHA4mRnZ2vt2rX66aeflJaWpoCAADVv3ly9e/eWl5eXPTYBAAAAO7E5AK5atUqjRo1SSkqKDMOwtJtMJlWtWlVz587Vgw8+WOr1/vjjj5o4caK2b9+u3Nxc3XvvvRozZowGDRpUovcfO3ZM//73v7V3717t2bNHZ8+eVUhIiE6ePHnD95nNZi1atEgLFizQzz//rJycHN19993q2LGjPv74Y/n7+5d6XwAAAJyJTQEwNjZW/fv3l7u7u5544gl16tRJ1apV0/nz57V582Z9+eWXeuSRR7R+/fpSzSMcFxenyMhIeXt7a8iQIfL399eKFSs0ePBgJSUl6dVXX73pOrZs2aLJkyfL3d1djRo1UnJy8k3fk52drQEDBmj16tVq2rSpRo4cKS8vLyUmJmrt2rV65513CIAAAOCOZ1MAnDhxonx8fLR9+3Y1adLEatnw4cP14osvqmPHjpo4cWKJA2BeXp6eeuopubm5afPmzQoLC5N07Y7jNm3aaPz48RowYIBCQkJuuJ7OnTtrx44datasmXx8fOTt7X3Tbb/++utavXq1pk+frrFjx1otYxo8AADwZ2HTTSA//fSTBg8eXCj8FWjatKkGDRqkvXv3lnid33//vY4dO6Zhw4ZZwp8kBQQEaPz48crJyVFUVNRN11OnTh21a9dOPj4+JdrumTNnNGvWLHXq1KlQ+JMkNzc3ublxzwwAALjz2XQEsHz58qpSpcoN+1StWlXly5cv8Trj4+MlSREREYWWRUZGSpI2bdpU8iJLaPny5crLy9PAgQN15coVrVq1SomJiapWrZoiIyNVo0YNu28TAADAEWwKgD169NDGjRs1derUYvts3LhRPXv2LPE6ExISJEn16tUrtKx69ery8/Oz9LGnPXv2SJJ+++03NWjQQOfOnbMsK1eunKZPn65XXnnlhuvIzs5Wdna25XV6erokKTc3V7m5uZKuHUl0d3dXfn6+1Wnlgva8vDyrm2nc3d3l5uZWbDuKV/B/Ll27KcnDw0Nms9lqVpqC9uI+D3t9TtfXIkkeHte+9fLy8krU7unpWWztpd0nFM+ZPidnGnsonjN9Ts409njKXPHK8nMqDZsC4MyZM9WxY0cNHz5cU6ZMUc2aNS3LkpKSNH78eKWmpurbb78t8TrT0tIkXTvlW5QKFSpY+tjThQsXJEmTJ09Wz549tXHjRtWsWVObN2/WqFGjNGbMGDVs2FD3339/seuYNm2aJk+eXKh9w4YNlqOgtWrVUvPmzbV//34lJiZa+jRo0EANGzbUrl27lJKSYmkPCwtTSEiINm/erCtXrlja27dvr6pVq9q8339ma9eutXzt7++vbt26KSkpSfv27bO0V6lSRR06dFBCQoIOHz5sabf357RhwwarH9jh4eHy8fGxqlGSevfuraysLMXFxVnaPDw81KdPH6WmpmrHjh027xOK50yfkzONPRTPmT4nZxp7Er+filOWn1NwcHCJ6zAZ18f2myjqRo7Lly9r//79cnd3V61atSx3AScmJio/P19NmzZVxYoVFRsbW6JtREREKCYmRgkJCapbt26h5TVq1FBGRkapQ6C3t7eqV69e7GNgCrZ711136ejRo1anrdetW6fevXure/fu2rhxY7HbKOoIYM2aNZWamqoKFSpIsv9f9099WKr/Bpfy6XMcASyqdsZM8a4fM9KdfxTGXmOPMVO0eS9zBLC4fRr9MUcAizLv5bI9ApiZmamAgAClpaVZckdxSnUEsOD6vKLk5eXp+PHjOn78uFX7//73v1LNF1xw5K+4gJeenq6goKASr6+02+3Ro0ehaxYjIyPl5eWl3bt333AdXl5eRT742tPTs9BpFHd39yJPxxV8c5e0HcUr6tRVcTfzFPd52OtzKu40Wmnai6u9tPuE4jnT5+RMYw/Fc6bPydnGHopW1p9TiesoTWez2XxL/65PtDdTcO1fUdf5JScnKyMjo8jrA23VoEEDSVJgYGChZW5ubvL391dWVpbdtwsAAHC7Od0x2i5duki6di3OH61fv96qjz0VnN7+5ZdfCi1LSUlRamqqQkND7b5dAACA283pAmD37t1Vp04dLVmyxOpiyLS0NE2dOlXlypXT8OHDLe3nzp3ToUOHbL4xpEuXLmrUqJFiY2MVExNjaTcMQ+PHj5ekEk9DBwAA4MzscuL+9OnTiouL09mzZ61ugihgMpn01ltvlawgDw/Nnz9fkZGR6ty5s9VUcKdOndLMmTOtjsSNGzdOUVFRWrhwoUaOHGlpT01N1d/+9jfL69zcXKWmplr1mTlzpipXrizp2rn0hQsXqlu3burdu7ceeeQR3X333dq6dat27dqlFi1a6PXXXy/dfwwAAIATsjkAvvbaa/roo4+srvMzDMNy40fB1yUNgNK129+3bt2qiRMnatmyZcrNzdW9996rGTNmaPDgwSVaR0ZGRqEZQzIzM63aJk2aZAmAktS2bVvt2rVLEydOVGxsrNLT01WrVi2NGzdO48ePl6+vb4n3AQAAwFnZFADnzZun999/Xz179tTTTz+t/v37a+TIkYqMjNTmzZs1f/58Pfzww3r22WdLve42bdpo3bp1N+23aNEiLVq0qFB7aGioSvGEG4vGjRtr+fLlpX4fAADAncKmADh37lyFhoZq3bp1lluXQ0NDNXjwYA0ePFiDBg1Sz549NXDgQLsUCwAAANvZdBPIoUOH1KtXL6vn1lz/cMouXbqoT58+mjlzpi2bAQAAgB3ZfBfw9c/N8/X11cWLF62WN2jQQAcPHrR1MwAAALATmwJgjRo1dPr0acvrv/zlL9q5c6dVn59//pmbJwAAAJyITQGwY8eO+uGHHyyv+/btq59++kmjR4/WmjVrNG7cOK1bt06dO3e2uVAAAADYh003gfz1r3/V2bNnderUKYWEhOi1117T6tWrNW/ePM2fP1+GYSg0NFTvvfeeveoFAACAjWwKgF27dlXXrl0tr/38/PTDDz/o22+/1bFjxxQSEqIHH3yQU8AAAABOxC4zgVzP09NTAwYMsPdqAQAAYCd2C4AXL17U//73P6WlpSkgIEDNmjVTpUqV7LV6AAAA2InNAfDkyZN66aWXtGbNGquZN0wmkx544AF9+OGHVnP3AgAAwLFsCoDHjh1Tx44ddeHCBdWrV08dO3ZUtWrVdP78eW3fvl2rVq3SDz/8oO3bt6tOnTr2qhkAAAA2sCkAjh07VikpKZo9e7aeeuopmUwmyzLDMDR37lw9++yzGjt2rL755hubiwUAAIDtbAqAsbGxeuihhzRq1KhCy0wmk0aPHq21a9dq48aNtmwGAAAAdmTTg6Dz8/PVuHHjG/Zp0qSJ8vPzbdkMAAAA7MimANiiRYubzvN78OBBtWrVypbNAAAAwI5sCoBTpkzRunXrNH/+/CKXz507V+vXr9c//vEPWzYDAAAAOyrVNYBvv/12obbw8HCNHj1a77//vtVdwNu2bdORI0cUGRmp2NhYdejQwW5FAwAA4NaVKgBOmjSp2GWHDx/W4cOHC7VHR0dr/fr1euutt0pdHAAAAOyvVAEwLi6urOoAAADAbVKqANilS5eyqgMAAAC3iU03gQAAAODOY/NcwJK0bds2LVq0SPv27VN6eroqVKig5s2ba/jw4brvvvvssQkAAADYic0B8JVXXtHHH38swzAkXZsBxDAM7dmzR59//rleeukl/fOf/7S5UAAAANiHTaeAo6Ki9NFHH6levXpavHixzp49q7y8PJ07d05LlixR/fr19dFHH+mLL76wV70AAACwkU0B8LPPPtPdd9+tnTt3aujQoapevbpMJpOqVaumIUOG6IcfflCNGjX06aef2qteAAAA2MimAHjw4EH1799fAQEBRS4PCAhQ//79bzpdHAAAAG6fMr8L2GQylfUmAAAAUAo2BcDGjRtrxYoVysjIKHL5lStXtGLFCjVu3NiWzQAAAMCObAqAo0eP1unTp9W+fXutWLFCqampkqTU1FQtX75cHTp00OnTp/XMM8/YpVgAAADYzqbHwDz++OP66aefNGvWLA0aNEiS5ObmJrPZLEkyDEMvvPCCRowYYXulAAAAsAubnwP48ccfa+DAgUU+CHrEiBHq1KmTPeoEAACAndgUADdv3qwKFSqoU6dOBD0AAIA7hE3XAIaHh2vu3Ln2qgUAAAC3gU0BsGrVqvL29rZXLQAAALgNbAqAPXv2VHx8vGUeYAAAADg/mwLg9OnTdfHiRY0aNUqXLl2yV00AAAAoQzbdBPLYY48pMDBQCxYs0JdffqnatWurWrVqhWb/MJlMio2NtalQAAAA2IdNATA+Pt7ydXZ2tg4dOqRDhw4V6sd0cAAAAM7DpgBY8MBnAAAA3Dlu6RrAHTt2qFu3bvL391dAQIB69uypXbt22bs2AAAAlIFSHwE8cOCAunfvrqtXr1raYmNjtX37du3atUuNGze2a4EAAACwr1IfAZw+fbquXr2qN954Q8nJyUpOTtZbb72lrKwszZgxoyxqBAAAgB2V+gjgli1bdN999+mdd96xtE2ePFnx8fHatGmTXYsDAACA/ZX6COD58+fVrl27Qu1t27bV+fPn7VIUAAAAyk6pA2Bubq78/PwKtfv6+io3N9cuRQEAAKDs2DQTCAAAAO48t/QcwC+//FI//PCDVdvRo0clSb179y7U32Qyac2aNbeyKQAAANjZLQXAo0ePWgLfH0VHRxdqYyYQAAAA51HqAHjixImyqAMAAAC3SakDYEhISFnUAQAAgNuEm0AAAABcDAEQAADAxRAAAQAAXAwBEAAAwMUQAAEAAFwMARAAAMDFEAABAABcDAEQAADAxRAAAQAAXAwBEAAAwMUQAAEAAFwMARAAAMDFEAABAABcDAEQAADAxRAAAQAAXAwBEAAAwMUQAAEAAFwMARAAAMDFEAABAABcDAEQAADAxRAAAQAAXAwBEAAAwMUQAAEAAFwMARAAAMDFEAABAABcDAEQAADAxRAAAQAAXAwBEAAAwMUQAAEAAFwMARAAAMDFOG0A/PHHH9W7d28FBgbK19dX7dq109dff12qdWRnZ+vtt99WvXr15O3treDgYI0aNUoXLlwosn9WVpb++c9/qkWLFgoKClJgYKCaNWumKVOmKC0tzR67BQAA4HAeji6gKHFxcYqMjJS3t7eGDBkif39/rVixQoMHD1ZSUpJeffXVm67DbDarb9++Wr9+vdq1a6f+/fsrISFB8+fPV2xsrH744QdVqVLF0j83N1fh4eHauXOnwsLCNHLkSEstb775pr766ivt2rVL5cuXL6vdBgAAuC2cLgDm5eXpqaeekpubmzZv3qywsDBJ0oQJE9SmTRuNHz9eAwYMUEhIyA3XExUVpfXr12vo0KFavHixTCaTJGn27Nl65pln9Oabb2rOnDmW/itXrtTOnTvVr18//ec//7Fa18MPP6xvv/1Wy5cv1/Dhw+27wwAAALeZ050C/v7773Xs2DENGzbMEv4kKSAgQOPHj1dOTo6ioqJuup558+ZJkqZNm2YJf5I0evRo1alTR4sXL1ZWVpal/fjx45Kk+++/v9C6+vTpI0lKSUm5pX0CAABwJk4XAOPj4yVJERERhZZFRkZKkjZt2nTDdVy9elU7d+5UgwYNCh0pNJlM6tmzpzIzM7V7925Le5MmTSRJ69atK7S+NWvWyGQyKTw8vFT7AgAA4Iyc7hRwQkKCJKlevXqFllWvXl1+fn6WPsU5duyYzGZzkeu4ft0JCQnq1KmTpGtH+R5++GGtXLlSzZs3V9euXSVduwbwxIkTmjt3rlq0aHHD7WZnZys7O9vyOj09XdK16wtzc3MlSW5ubnJ3d1d+fr7MZrOlb0F7Xl6eDMOwtLu7u8vNza3YdhSv4P9cuhb8PTw8ZDablZ+fX6i9uM/DXp/T9bVIkofHtW+9vLy8ErV7enoWW3tp9wnFc6bPyZnGHornTJ+TM409Jzy+5DTK8nMqDacLgAV32wYEBBS5vEKFCje9I7ck67i+n3TtP3rFihUaP3683n33Xe3bt8+ybMSIEerZs+dNa582bZomT55cqH3Dhg2Wm0dq1aql5s2ba//+/UpMTLT0adCggRo2bKhdu3ZZnWoOCwtTSEiINm/erCtXrlja27dvr6pVq960Jle2du1ay9f+/v7q1q2bkpKSrD7bKlWqqEOHDkpISNDhw4ct7fb+nDZs2GD1Azs8PFw+Pj5WNUpS7969lZWVpbi4OEubh4eH+vTpo9TUVO3YscPmfULxnOlzcqaxh+I50+fkTGNP4vdTccrycwoODi5xHSbj+tjuBCIiIhQTE6OEhATVrVu30PIaNWooIyPjhiFw+/bt6tixox599FF9+eWXhZbPmzdPo0aN0j//+U+98sorkqTff/9dQ4cO1c6dO/XRRx+pR48ekqSNGzfqpZdekmEY2rlzp0JDQ4vdblFHAGvWrKnU1FRL6LT3X/dPfVhsOS7v0+c4AlhU7YyZ4l0/ZqQ7/yiMvcYeY6Zo817mCGBx+zT6Y44AFmXey2V7BDAzM1MBAQFKS0uz5I7iON0RwIKjdsUFvPT0dAUFBdm8juv7SdLUqVO1atUqffvtt3rooYcs7YMHD5a3t7cefvhhTZkyxXJzSVG8vLzk5eVVqN3T07PQaRR3d/ciT8cVfHOXtB3FK+rUlZubW5GHyYv7POz1ORV3Gq007cXVXtp9QvGc6XNyprGH4jnT5+RsYw9FK+vPqcR13PI7y8j11+f9UXJysjIyMoq9tq9AnTp15ObmVuy1gkVdZ1hw80dRN3oUtP30008l2AMAAADn5nQBsEuXLpKuXYvzR+vXr7fqUxwfHx+1adNGhw8f1qlTp6yWGYahmJgY+fr6qlWrVpb2nJwcSUU/6qWgraijewAAAHcapwuA3bt3V506dbRkyRKriyHT0tI0depUlStXzuphzOfOndOhQ4cKne4dNWqUJGncuHFW1ybMmTNHx48f16OPPiofHx9Le8eOHSVJkydPtjqnnp+fr4kTJ0oq+uggAADAncbpTtx7eHho/vz5ioyMVOfOna2mgjt16pRmzpxpdSPGuHHjFBUVpYULF1qmb5Ou3bm7bNkyffXVVzpx4oS6dOmio0eP6j//+Y9q166tf/zjH1bbHT9+vL799lt98cUX2rNnj7p16yZJio2N1S+//KJ69eqVaAo6AAAAZ+d0RwCla0fatm7dqo4dO2rZsmX67LPPVK1aNS1durTEIczNzU3ffvutJk2apJSUFH3wwQfatm2bnnzySe3YscNqHmDp2m3Ve/bs0fPPP6/s7GzNmTNHc+fOVX5+vl577TXt3LnzpjefAAAA3Amc7jEwfybp6eklvh37VvF4huLNe9nRFTgnxkzxGDNFY8wUjfFSPMZM0cp6zJQmdzjlEUAAAACUHQIgAACAiyEAAgAAuBgCIAAAgIshAAIAALgYAiAAAICLIQACAAC4GAIgAACAiyEAAgAAuBgCIAAAgIshAAIAALgYAiAAAICLIQACAAC4GAIgAACAiyEAAgAAuBgCIAAAgIshAAIAALgYAiAAAICLIQACAAC4GAIgAACAiyEAAgAAuBgCIAAAgIshAAIAALgYAiAAAICLIQACAAC4GAIgAACAiyEAAgAAuBgCIAAAgIshAAIAALgYAiAAAICLIQACAAC4GAIgAACAiyEAAgAAuBgCIAAAgIshAAIAALgYAiAAAICLIQACAAC4GAIgAACAiyEAAgAAuBgCIAAAgIshAAIAALgYAiAAAICLIQACAAC4GAIgAACAiyEAAgAAuBgCIAAAgIshAAIAALgYAiAAAICLIQACAAC4GAIgAACAiyEAAgAAuBgCIAAAgIshAAIAALgYAiAAAICLIQACAAC4GAIgAACAiyEAAgAAuBgCIAAAgIshAAIAALgYAiAAAICLIQACAAC4GAIgAACAiyEAAgAAuBgCIAAAgIshAAIAALgYAiAAAICLIQACAAC4GAIgAACAiyEAAgAAuBgCIAAAgIshAAIAALgYAiAAAICLIQACAAC4GAIgAACAiyEAAgAAuBgCIAAAgIshAAIAALgYAiAAAICLIQACAAC4GKcNgD/++KN69+6twMBA+fr6ql27dvr6669LtY7s7Gy9/fbbqlevnry9vRUcHKxRo0bpwoULxb5n8eLFatOmjXx9fRUUFKQHHnhAe/futXV3AAAAnIZTBsC4uDh17NhRW7du1aBBg/T0008rOTlZgwcP1vvvv1+idZjNZvXt21cTJ05U5cqV9fLLL6t9+/aaP3++2rdvr5SUlELvmTJlih577DFduHBBTz/9tAYOHKjNmzerQ4cO2rZtm713EwAAwCE8HF3AH+Xl5empp56Sm5ubNm/erLCwMEnShAkT1KZNG40fP14DBgxQSEjIDdcTFRWl9evXa+jQoVq8eLFMJpMkafbs2XrmmWf05ptvas6cOZb+CQkJmjRpkurXr69du3YpICBAkvTss8+qXbt2euqpp/Tzzz/Lzc0pMzMAAECJOV2a+f7773Xs2DENGzbMEv4kKSAgQOPHj1dOTo6ioqJuup558+ZJkqZNm2YJf5I0evRo1alTR4sXL1ZWVpalfeHChcrLy9Mbb7xhCX+SFBYWpqFDh+rXX3/V1q1b7bCHAAAAjuV0ATA+Pl6SFBERUWhZZGSkJGnTpk03XMfVq1e1c+dONWjQoNCRQpPJpJ49eyozM1O7d++263YBAADuBE53CjghIUGSVK9evULLqlevLj8/P0uf4hw7dkxms7nIdVy/7oSEBHXq1MnytZ+fn6pXr37D/jeSnZ2t7Oxsy+u0tDRJ0qVLl5SbmytJcnNzk7u7u/Lz82U2my19C9rz8vJkGIal3d3dXW5ubsW251y9YUku7eLFXMvXJpNJHh4eMpvNys/PL9Re3Odhr8+p4PMv4OFx7VsvLy+vRO2enp7F1l7afWLMFO/6MSM59nNyprHHmClaerqc6nNyprGXc9Xpji85hfR0lennlJmZKUlWn0dxnC4AFoSm60/DXq9ChQqWPras4/p+BV9XrVq1xP2LMm3aNE2ePLlQe+3atW/4PpSNL8Y5ugLcaRgzKA3GC0rrdo2ZK1euFJuBCjhdALyTjRs3TmPGjLG8NpvNunTpkipVqmR1HeKfUXp6umrWrKmkpCRLYAZuhDGD0mLMoLRcbcwYhqErV64oODj4pn2dLgAWJNbijralp6crKCjI5nVc36/g69L0L4qXl5e8vLys2gIDA2/4nj+bChUquMQ3GeyHMYPSYsygtFxpzNwsqxRwupP0N7reLjk5WRkZGcVe21egTp06cnNzK/aavaKuM6xXr54yMjKUnJxcov4AAAB3KqcLgF26dJEkbdiwodCy9evXW/Upjo+Pj9q0aaPDhw/r1KlTVssMw1BMTIx8fX3VqlUru24XAADgTuB0AbB79+6qU6eOlixZon379lna09LSNHXqVJUrV07Dhw+3tJ87d06HDh0qdPp21KhRkq5dl3f93TBz5szR8ePH9eijj8rHx8fS/vjjj8vDw0NTpkyxWte+ffv01VdfqVGjRrrvvvvsvbt/Gl5eXpo4cWKhU+BAcRgzKC3GDEqLMVM8k1GSe4Vvs7i4OEVGRsrb21tDhgyRv7+/VqxYoVOnTmnmzJl69dVXLX1HjhypqKgoLVy4UCNHjrS0m81m9e7dW+vXr1e7du3UpUsXHT16VP/5z38UGhqqnTt3qkqVKlbbnTJlit58802FhISof//+unLlipYuXaqcnBzFxsaqY8eOt+u/AAAAoMw43RFASQoPD9fWrVvVsWNHLVu2TJ999pmqVaumpUuXWoW/G3Fzc9O3336rSZMmKSUlRR988IG2bdumJ598Ujt27CgU/iTpjTfe0JdffqkqVaros88+09dff61OnTpp+/bthD8AAPCn4ZRHAAEAAFB2nPIIIAAAAMoOARAAAMDFEAABAABcDAEQAADAxRAAAQAAXAwBEAAAwMUQAAEAdxyz2Vzk18AfFfW0O8YMARCAg/EoUtwKNzc3paenW76Wro0lfrHjj0wmkyQpJydHFy5ckPR/Y0Zy3TDIg6Bhs9zcXLm7u1t9Q5WEYRiWb0y4lvT0dHl4eKh8+fKleh9jxrUZhqH//e9/Wrx4sU6cOKHc3Fz5+/urdevWevjhhxUSEmLVl7GCvLw8bd26VbNnz9a5c+eUlpYmPz8/de7cWf3791fLli0tfV1tzBAAYbMJEyYoJCREnTt31t133y0fH5+bvsfVvtFg7aWXXlKFChUUHh6uhg0bqmrVqvLw8Ljhe8xmc6n/yMCfy9y5czVp0iQlJycrKChIbm5uunjxomV5t27d9PTTT+uBBx6Qt7e3AyuFs3jvvff07rvv6uLFi6pfv76ysrKUlJRkWd6kSRM999xzeuyxx+Tr6+vASm8/AiBscurUKdWuXVuSVKtWLUVEROjBBx9UixYtVLVqVXl6elr6FvwCP3XqlFatWqUWLVowx7ILun7MVKxYUe3bt1dERITatGmjunXrqlKlSpa+BX8oHD16VPPnz1f79u3Vt29fR5UOB0pMTFSzZs0UGhqqzz77TIGBgapWrZoOHz6slStX6ttvv9WRI0ckSYMHD9bbb7+tevXqObhqONKpU6fUpEkThYWFac6cOapevboqVqyogwcPKiYmRtHR0YqNjVV+fr7atm2rGTNmqHPnzo4u+/YxABt8+umnhslkMrp162a0adPGKFeunGEymYx7773XGD9+vLF582YjJSXFyM/Pt7xn1qxZhslkMr766isHVg5HmTNnjmEymYxHHnnEGDhwoFGtWjXDZDIZtWrVMv76178aX3zxhXHgwAEjPT3d8p7PPvvMMJlMRlRUlAMrhyNNmDDBqFq1qhEdHV1snzVr1hhdu3Y1TCaT0bVrV+PYsWO3sUI4m0mTJhmVK1c2YmJiDMMwrH4PFdi6dasxcOBAw2QyGU2bNjX27t1rGIZhmM3m21qrIxAAYZNXXnnFMJlMxg8//GCcPXvWWLBggTFy5EijXr16hslkMry8vIyuXbsaM2fONA4cOGAkJydbvtkyMjIcXT4c4O9//7thMpmM7du3GxkZGca6deuMyZMnG127djX8/f0NDw8Po0mTJsaLL75orF692jhw4IDRv39/xoyL69Onj9GoUSMjKSnJMAzDyMvLMwzj2i/1gq8NwzByc3ONN954wzCZTMaYMWMcUiucw8CBA406deoYJ0+eNAzDesz8MQzOmzfPMJlMxoABA257nY5CAMQtS09PNx5++GHDZDIZV69etbRfvXrV2L17t/Hhhx8a/fr1M6pXr26YTCajYsWKRvfu3Y1y5coZffr0cWDlcJTMzEzjiSeeMLy8vIzffvvN0p6bm2scPXrUWLFihfHKK68YzZs3N8qVK2eUL1/eaNGihWEymYwHHnjAgZXD0f7+978b7u7uxunTp4vtU/BL3Ww2G926dTMaNGhgnDlz5naVCCczdepUw2QyGXv27Cm2T15enpGbm2sYhmEMGDDACAkJMQ4dOnS7SnSoG191DdyAr6+vBgwYoICAAKWnp6tKlSoym83y8vJSy5Yt1bJlS40YMUJ79+7Vli1btGXLFu3cuVO5ubl67rnnHF0+HMDHx0f9+vVTUFCQcnNzJV27zs/Dw0N/+ctf9Je//EW9evXS0aNHtWfPHm3btk2rV6+WJD377LOOLB0O1qVLF7333nt6/PHHNX36dDVr1kzu7u5WfUwmk+Va47CwMO3evVuXL19WcHCwg6qGI3Xq1Ekmk0lPPvmk3nvvPXXs2LHQTYrX31jWqFEjrV27Vr///vvtLtUhuAkEZaKoOzYPHDigYcOGKSkpSb/99ptjCoPTMoq4MzwhIUFDhw7V0aNHGTMuLicnR08++aQWL16sjh076uWXX1avXr2KvHMzLS1NL7/8stasWWN57htc07hx4zRjxgzVrl1bzz33nPr06aOQkJBCd4mnp6frxRdf1OrVq5Wamuqgam8vjgDCJvn5+YX+Cpes/6rKzc2Vp6enUlJSdPz4cQ0dOvR2lggnU9yYuT785eXlycPDQydPntTPP/+sxx577HaWCCdUrlw5/fvf/1a9evX0r3/9SwMHDlTz5s01ePBgde/eXZUqVZKHh4cqV66s2bNna/ny5RoxYoSjy4aDTZs2TQ0bNtS0adP0t7/9TbNnz9b999+vzp0766677lKlSpVUoUIFffjhh1q+fLn+3//7f44u+bYhAMImRf0i/6OCR8Fs2bJFWVlZGj16dFmXBSdWkjFT8EzAAwcOKC8vjzEDyx+SL7zwgurWrauvv/5a33//vV5//XW5u7urXr16KleunM6cOaOLFy+qV69eevXVVx1dNhyo4KzCY489ptDQUK1cuVLr16/XJ598ok8++USVK1dWTk6OsrOzlZWVpUGDBrnUmOEUMG6bzZs3Kzo6WlOnTnV0KbhD/PTTT9q2bZuef/55R5cCJ5OTk6Nt27YpPj5eBw8e1MWLF3Xu3DkFBgZq8ODBeuKJJxQQEODoMuFE8vPz9fPPP+vHH3/UoUOHdO7cOR07dky1atVS79699dhjj930gfR/JgRA3LL8/Hy5ubkxowdKxDAMy+lfxgxKKj8/XwkJCbp8+bJlrt86depY3dhx5coVZWRk6K677lJ2dra8vLwcWDGc0R+vMc7JyZGbm5s8PDyKvSzlz44AiFJLSkpSzZo1La/NZrMMw7jpN1DBdV1wPceOHdNf/vIXy2uz2Syz2cx4wA0dPnxY48aN09q1a5WTkyMvLy8FBQUpJCRE7dq1U0REhO677z75+/tLYrpA3Nwfx0hBMCzqJrQ/OwIgSuXkyZOqU6eOIiIiNHToUD3wwANWU3fl5+fLZDLJzc3N8g2Vk5OjcuXKObBqONKxY8dUr149NWzYUE888YQee+wxVa9e3bI8Pz9f0rVrAwvGTGZmpjIyMiwX9sP1nD17Vr169dLBgwf117/+VZUrV5aHh4cOHjyoLVu2KD09XYGBgerXr59GjRqltm3bOrpkONjly5e1f/9+tWvXjqPAJXFbnzqIO17BgzUL/lWuXNkYMWKEsWbNGsvDNAtkZ2cbhmEYs2fPNrp3724cPnzYESXDwWbMmGE1Zgqm6fryyy+NnJwcq77Xj5k2bdpYpmWC63nzzTeNoKAgY/78+Za27OxsIycnx0hMTDTmzJljdOzY0XBzczPuueceY/Xq1YZhuMYUXija3/72N8NkMhktWrQw3nnnHePnn38utm/BODly5Iixb9++Qj+LXAEBEKXywAMPGP7+/sb8+fONESNGGOXLl7f8Uq9bt67xt7/9zdi1a5fVex555BGm8XJh/fv3N3x8fIwlS5YYEyZMMO655x7LmPH09DSGDBlixMbGWr2HMYNmzZoZvXr1Ms6fP28YRtHBLiUlxfjXv/5lVKxY0fD39zd++eWX210mnEhYWJjh5uZmVKxY0fIzJjw83JgzZ06RM8hkZGQYQ4cONdq1a0cABG7kwoULRps2bYwaNWpY2rKysozFixcb3bt3tzrC07p1a+Pjjz82vv76a+Ouu+4yHnzwQQdWDkdJSUkxOnToYFSvXt3Slp2dbaxbt8548sknjbvuussyZqpUqWK8/vrrxpdffsmYcXGpqalGq1atjHbt2t20b25urrF06VLDZDIZo0ePvg3VwRmdOHHCCA4ONtq1a2fs27fPeOedd4zOnTsb3t7ehslkMvz9/Y1BgwYZK1euNC5evGgYhmHs2rXLqFixohEeHu7g6h2DawBRYklJSXr00UdVoUIFrV69utC1fefOndOSJUsUFRWln3/+WZLk5eWl7OxsrV69Wr1793ZU6XCQ8+fPa+TIkcrPz9fatWtlGIbluZCSlJqaqnXr1mn58uWKjY21moKJMeOajP//OtBRo0Zp/vz5WrVqle6//365ubkpPz+/2GtC77vvPuXk5Cg6OloVK1a8zVXD0eLi4tSjRw89//zz+uijjyRJGRkZ2r59u6KjoxUbG6sDBw5IkoKDgzVw4EBlZWVp7ty5+u6779SnTx9Hlu8QBECUWG5urrZu3Spvb2+1bdvWcqOH2Wy23PhR4MiRI/r444/16aefKigoSBcvXnRg5XCko0ePKjs7W40aNbIaM398hFBSUpIWLVqk6dOny8vLS5cuXXJg1XC0devWqU+fPpaZPyIiIizLCm4cKhhDaWlpGjlypH755RcdPnzYUSXDgf73v/9p4MCBeuGFF/TCCy8UerRLcnKy4uPjFR0drc2bN+vkyZOSpMDAQJf9WcP98igxT09PhYeHW8KfdG36Lnd3d8sv9ry8POXn56t+/foaMWKEfHx8NGDAAAdXDkeqW7euGjduXGjMFDx6IT8/X/n5+apZs6Z69uwpSRo4cKAjS4YTuP/++/Xll18qLS1NvXr1Urdu3fT1118rMzNT7u7uVr/ct23bpl27dqlLly4OrBiO1KxZM+3Zs8cybWTB+DCbzZKk6tWra8iQIVq0aJG2bt2q5557TpJcempSnq+AErv+Ib5FPTjTZDJZnZ754osvlJWVpVGjRt3uUnGHKAiDBb788kvGDCz69+8vSfrnP/+p+Ph4xcfHq2rVqurSpYt69uwpLy8v/fzzz/r888/l5eWll156ycEVw5EKngd5vYI/PAvOPLi7uys4ONhymcATTzxxW2t0JpwCRplIT0/X6NGjFRcXp+TkZEeXgztAZmamnnvuOa1du1YXLlxwdDlwIoZh6LvvvtPcuXO1YcMG5eXlWS1v37693nzzTd1///0OqhB3kuPHj+vhhx/WlStXdOLECUeX4zAEQJTIhQsXdODAAR05ckQZGRlq06aNGjZsaPWg3j8eFczOztaFCxesZg2B67jVWRnS09NVoUKFMqgIdxrj2pMqrMZRWlqa4uPjdfz4cQUHB8vPz0+tW7dW1apVHVgp7iQnTpzQ6NGj1aVLF73xxhuOLsdhCIC4qXXr1ukf//iHduzYYdVesWJF9ejRQ4MHD9aDDz7IjA0oVknCYF5eXqFTwnA9xc3Lev0sQ8D1bnUuX1edA7gAARA3lJSUpK5duyozM1MjR45UeHi4jh8/rp9++kn/+9//tH//fmVnZ6tx48YaN26cBgwYoHLlyjEnpws7f/683n33XUVERKht27YKDAy0LCv4ceNqc27i5oqao/WPR//+2F5wExF/fLqmko6ZP2J60mv4rsENzZkzR5cvX9b8+fP1yCOPWC07ffq0tm/frlWrVmnJkiV67LHHdPr0af39738n/LmwTz/9VB988IFWrlype+65R127dlWXLl3UtGlTq/k5zWazDMOQu7u74uPjdfXqVfXq1cuBlcOR5syZo/j4eA0fPlxdunSRn5+f5Q+Fgjs5Cx77UtD+xxvP4FpKOmb+iPB3DUcAcUPt2rWTj4+PvvnmG1WuXLnY03RxcXF69dVX9csvv+jTTz916TurXF3z5s31yy+/qEWLFtq7d69yc3MVEhKijh07Kjw8XB07dlTDhg0t/X///XcNHTpUq1evVmZmpry9vR1YPRyldu3aOnXqlLy8vNSsWTNFRESod+/eatu2rdUR47y8PHl4eOj333/X3Llz1axZM4WHhzuwcjgKY8Y2BEAUKyMjQ/369dPp06e1Z88elS9f3uqQ+x8Pt//000/q3r27OnXqpG+//dbyRH+4jqSkJHXu3FmVKlXSjh07tGfPHq1du1arVq3S/v375ebmpsaNG6tz587q3LmzIiMjdfjwYT300ENq3bq1Vq1a5ehdgAMcPHhQ9957r1q2bKmgoCBt3LhRkuTr66uOHTuqd+/eioiIsPrDYevWrercubM6dOigrVu3Oqp0OAhjxg7Kcp453PnGjh1rmEwm4/PPPy+07PrJ2fPz8w3DMIy+ffsa9evXN06ePHnbaoTz2Llzp1GxYkVjxIgRhmEYRl5enpGfn2+cP3/eWLdunfH0008bISEhhslkMsqXL2907tzZMo/0d99959ji4TBfffWVYTKZjH/+85+GYRjG4cOHjRkzZhhhYWGWuaLvuusuY+jQocYXX3xhXLp0yXj//fcNk8lkrF692sHVwxEYM7YjAOKGTp8+bdx7772GyWQyXnjhBWPPnj1GVlaWVZ/c3FzDMAwjLS3NGDhwoFGrVi1HlAonkJCQYDzyyCPG4sWLi1yek5NjnDx50vj3v/9tDBo0yKhYsaJhMpmMoKCg21wpnMmcOXMMk8lkrF27ttCyXbt2Ga+88opRs2ZNyy/2+vXrG9WrVzcCAgJuf7FwCowZ2xEAcVMrV640ateubZhMJqNVq1bGO++8Y8TFxRknT560CoNffvmlUaVKFWP06NEOrBaO9ttvvxmpqak37FNwxHj27NmGyWQynn322dtRGpyQ2Ww2duzYYbzyyivG0aNHrdqvl5WVZaxevdoYMWKEERAQYJhMJuP555+/3eXCCTBm7INrAFEk4w/X7126dEnTpk3T119/raSkJFWpUkVNmjRRcHCwypcvr6ysLH399deqXbu2/vvf/6pBgwYOrB6O8McxI9382W1///vfNXPmTO3evVstWrS4HWXCSWVkZKhcuXJF3qH5x7H1/PPP69NPP9XevXsVFhZ2G6uEM2HM2IYAiGIVfAOdPn1awcHBcnNz088//6zVq1crPj5ev/76q5KSkiRJQUFBCgsL08cff6zGjRs7uHI4SsGYSU5OVtWqVa2CX35+vuUxHtK1xwj16dNHZ8+eVUpKiqNKxh2iYGwdO3ZMgwcPVlpamhISEhxdFpwYY+bGeIASCsnLy9O2bdu0YMECHTlyRCaTSeXLl1fr1q01aNAgvf766xo7dqySkpKUlZWl48ePq2HDhqpZs6Y8PDy4+9cF/XHMuLm5ycfHR82aNVP//v3VoUOHQo8O8vb21siRIxUcHOygqnEnKfiZ8uuvv2rv3r167bXXHFwRnB1j5sY4AohCZs6cqXfeeUdXrlxR3bp15e7ursOHD1uW33PPPXr22Wc1YMAA5t+EpJuPmYYNG+qpp57S0KFDVb16dUt7Tk6OPDw8eHA4SvyH4/nz5xUdHa0HH3xQFStWvA2VwVkxZmxDAISVEydO6N5771WLFi0UFRWlcuXKqVq1akpOTtZ3332nb775RvHx8ZKk8PBwzZgxQ61atXJs0XCo0oyZbt266d133+V6PygrK0uJiYmqVauWfHx8SvVeV5/D1VUxZuyLAAgrEyZM0Jw5c7RkyRJ1795dUuG/sg4cOKCZM2fq66+/VkhIiBYvXqyWLVs6qmQ4mC1jhssFXNf06dO1YsUKPfLII2rXrp0aNGigatWq3fCXdEpKioKCgpj+zUUxZuyLAAgr/fv31759+xQXF6datWpZptAxDENms9nqG+2jjz7SK6+8ohEjRmjhwoUOrBqOxJjBrbj77rt19uxZubu7KyAgQB06dFBERITatm2rOnXqqFKlSlb9MzMzNWnSJF28eFHz5s3jaI4LYszYF5EYVpo3b66VK1cqIyNDkix/NV0//2/BUZuXXnpJW7Zs0ffff6/jx4+rTp06DqsbjsOYQWkdOXJEaWlpat++vYYNG6aYmBjt2LFDq1evVq1atdS1a1f16NFDzZs3V40aNRQYGKiff/5Z8+bNU9euXflF7oIYM/ZHAISVggmyH330Ub3//vu67777inzGUsH1FA0aNNC6dessv/zhehgzKK0jR47o6tWrioiI0HPPPacHHnhAhw8f1o4dO/T9999rxYoVWrx4se655x5169ZNvXr1UmxsrNLT0/XUU085unw4AGOmDNyOp03jzpGXl2e8+uqrhslkMho1amTMmjXLSE5OLrLvpUuXjOHDhxtVqlS5zVXCmTBmUFrffPONYTKZjGXLllm15+TkGAkJCcby5cuNl156yWjWrJlRrlw5w9fX1yhfvjxTBrowxoz9cQ0gijRnzhy99957On78uIKDg9WvXz/df//9qlmzptzd3RUYGKh//etf+vDDD/Xss8/q/fffd3TJcDDGDErKMAwdOnRI3t7eql27dpE3A2VmZurIkSM6fPiwFi5cqJiYGD3//PP6+OOPHVQ1HIkxY38EQBTJMAwdPXpU8+bN09KlS3X69GlJUtWqVeXp6alz587JbDZr6NChmjFjhu6++24HVwxHY8zAHor6xf7iiy9q1qxZ2rNnj5o3b+6gyuCsGDO3hgCIm8rMzNSuXbu0atUqnT17VhcuXFCFChU0aNAg9e/fX97e3o4uEU6GMQNbmc1mubm56eTJk+rbt68uX76sxMRER5cFJ8aYKR1uAsFN+fr6Kjw8XOHh4crNzZWnp6ejS4KTY8zAVgWzw5w5c0a5ubl69tlnHVwRnB1jpnQ4AggAcFqGYej06dOqWLGifH19HV0O7gCMmZIhAAIAALgYZmAHAABwMQRAAAAAF0MABAAAcDEEQAAAABdDAAQAAHAxBEAAAAAXQwAEAABwMQRAAAAAF0MABAAAcDH/H0DAekE0WOOjAAAAAElFTkSuQmCC\n",
      "text/plain": [
       "<Figure size 700x500 with 1 Axes>"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Run the algorithm \n",
    "oracle = PhaseOracle(log_expr)\n",
    "backend = Aer.get_backend('aer_simulator')\n",
    "quantum_instance = QuantumInstance(backend, shots=200)\n",
    "grover = Grover(quantum_instance=backend)\n",
    "problem = AmplificationProblem(oracle)\n",
    "result = grover.amplify(problem)\n",
    "plot_histogram(result.circuit_results)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "pycharm": {
     "name": "#%%\n"
    },
    "slideshow": {
     "slide_type": "fragment"
    }
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'qiskit-terra': '0.21.2', 'qiskit-aer': '0.10.4', 'qiskit-ignis': None, 'qiskit-ibmq-provider': '0.19.2', 'qiskit': '0.37.2', 'qiskit-nature': None, 'qiskit-finance': None, 'qiskit-optimization': None, 'qiskit-machine-learning': None}"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Print Qiskit version \n",
    "qiskit.__qiskit_version__"
   ]
  }
 ],
 "metadata": {
  "anaconda-cloud": {},
  "celltoolbar": "Slideshow",
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.9.13"
  },
  "latex_envs": {
   "bibliofile": "biblio.bib",
   "cite_by": "apalike",
   "current_citInitial": 1,
   "eqLabelWithNumbers": true,
   "eqNumInitial": 0
  },
  "livereveal": {
   "autolaunch": true
  },
  "nav_menu": {},
  "toc": {
   "navigate_menu": true,
   "number_sections": true,
   "sideBar": true,
   "threshold": 6,
   "toc_cell": false,
   "toc_section_display": "block",
   "toc_window_display": false
  }
 },
 "nbformat": 4,
 "nbformat_minor": 1
}