logical_formulas/propositional_logic_parser.ipynb

{
 "cells": [
  {
   "attachments": {},
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The language of propositional logic is somewhat simpler than the language of arithmetic."
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "```xml\n",
    "<expr> ::= { <term> \"imp\" } <term> | <term> { ( \"iff\" | \"xor\") <term> }\n",
    "<term> ::= <factor> { (\"and\" | \"or\") <factor> }\n",
    "<factor> ::= '(' <expr> ')' | { \"not\" } <atom>\n",
    "<atom> ::= [A-Z] { [A-Za-z0-9_] } | \"bot\"\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "I have added a new showOption called `bussproof`. This option does not generate a diagram \n",
    "but instead produces LaTeX code that can be seamlessly incorporated into a LaTeX document. \n",
    "\n",
    "To ensure correct compilation of the source .tex file, it is necessary to include the `\\usepackage{bussproofs}` \n",
    "command in the preamble."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This script works good only when the identifier for propositional letter is short.  This problem has been fixed in the next script `first_order_logic_parser.ipynb`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [],
   "source": [
    "# url = 'https://raw.githubusercontent.com/jhjeong314/Proofmood/main/logical_formulas'\n",
    "# import httpimport\n",
    "# with httpimport.remote_repo(url):\n",
    "#   from propositional_logic_parse import *\n",
    "\n",
    "# If you get SSLCertVerificationError then try the following. \n",
    "# Of course, you should have arith_parse.py available locally.\n",
    "import sys\n",
    "sys.path.append('../')\n",
    "from modules.propositional_logic_parse import *\n",
    "\n",
    "def testParser(input_text, showOption='polish', showOperType=False):\n",
    "  # showOption ::= 'polish' | 'RPN' | 'infix_latex' | 'tree' | 'bussproof'\n",
    "  # showOperType has effect only when showOption == 'polish' or 'RPN'\n",
    "  from IPython.display import display, Math\n",
    "\n",
    "  try:\n",
    "    ast = parse_ast(input_text)\n",
    "  except ValueError as e:\n",
    "    print(f\"ValueError: {e}\")\n",
    "  except SyntaxError as e:\n",
    "    print(f\"SyntaxError: {e}\")\n",
    "  else:\n",
    "    if showOption=='polish':\n",
    "      print(ast.build_polish_notation(showOperType))\n",
    "    elif showOption=='RPN':\n",
    "      print(ast.build_RPN(showOperType))\n",
    "    elif showOption=='infix_latex':\n",
    "      s = ast.build_infix_latex()\n",
    "      print(s) # latex source text\n",
    "      display(Math(f\"${s}$\"))\n",
    "    elif showOption=='tree':\n",
    "      ast.draw_tree()\n",
    "    elif showOption=='bussproof':\n",
    "      s = ast.build_bussproof() \n",
    "      print(s)\n",
    "    else:\n",
    "      raise ValueError(f\"Invalid showOption: {showOption}\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "imp or and A B not C D\n",
      "A B and C not or D imp\n"
     ]
    }
   ],
   "source": [
    "input_formula = \"A and B or not C imp D\"\n",
    "testParser(input_formula)\n",
    "testParser(input_formula, 'RPN')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(A_{1} \\wedge B_{ij} \\leftrightarrow \\neg (\\neg {\\rm Bob} \\wedge A) \\vee \\bot) \\rightarrow \\neg C\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle (A_{1} \\wedge B_{ij} \\leftrightarrow \\neg (\\neg {\\rm Bob} \\wedge A) \\vee \\bot) \\rightarrow \\neg C$"
      ],
      "text/plain": [
       "<IPython.core.display.Math object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\\begin{prooftree}\n",
      "\\AxiomC{$A_{1}$}\n",
      "\\AxiomC{$B_{ij}$}\n",
      "\\BinaryInfC{$\\wedge$}\n",
      "\\AxiomC{${\\rm Bob}$}\n",
      "\\UnaryInfC{$\\neg$}\n",
      "\\AxiomC{$A$}\n",
      "\\BinaryInfC{$\\wedge$}\n",
      "\\UnaryInfC{$\\neg$}\n",
      "\\AxiomC{$\\bot$}\n",
      "\\BinaryInfC{$\\vee$}\n",
      "\\BinaryInfC{$\\leftrightarrow$}\n",
      "\\AxiomC{$C$}\n",
      "\\UnaryInfC{$\\neg$}\n",
      "\\BinaryInfC{$\\rightarrow$}\n",
      "\\end{prooftree}\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAaQAAAEjCAYAAAB9+XVVAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjcuMSwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy/bCgiHAAAACXBIWXMAAC4jAAAuIwF4pT92AAAcRElEQVR4nO3deVTVdeL/8dcFKVxGVJJcEjMdNVxKc9xoCrdSsNIkxwkxJ9OaIUvUcskzdmZOxzKDUmgsk8w0OYRYamIJGZZWlMuEYdQoOKRgeFQ0EVnu/f3RkfnyY5H1ft4Xn49zPMn9vD+f+7oEvu77s12bw+FwCAAAi7lZHQAAAIlCAgAYgkICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUJCk+RwOJSfn6+CggKrowCoIQoJjSIjI0NDhw7VjTfeKJvNJpvNJg8PDw0fPlwBAQEKCAjQiBEjNGzYMA0dOlTLly/Xr7/+Wu/nTUxMVPv27eXh4aE2bdooLi6uAV4NAGewORwOh9Uh0HTZ7XYFBQVp586dmjFjht56660KY7Zs2aKQkBC1a9dOiYmJ6tevX72e89dff9WsWbO0adMmvf3225o+fXq9tgfAOZghoVG5ubnpxhtvlCS1atWq0jETJ07U4sWLdeLECQUFBdV7N1urVq00ZsyYem0DgPNRSDDCww8/LEnKzs7W1q1b6709m81W720AcC4KCUbo1KlT2d+PHz9uYRIAVqGQYIRDhw6V/d3Pz8+6IAAsQyHBcg6HQ0uXLpUkjR49WkFBQRXGpKamKjg4WIMHD9bdd9+tIUOGaNmyZTU6M++DDz7Q/fffr1GjRqlHjx6aMGGCUlNTG/x1AKgfCgmWysrK0tixY/Xpp5/qmWee0bZt2+TmVv7HctWqVbrnnns0ffp0paamKiUlRYmJiUpLS9PQoUP13//+t8rtr1q1SocPH1ZcXJySk5N15MgR3XrrrRo2bJjWrl3b2C8PQC00szoArh3x8fHlds0VFRUpMzNTkrRs2TLNnDlTnp6e5dbZuXOnnn76aUVHR2v8+PFlj7dr104bNmxQ37599dBDD2nv3r1q1qzij/OQIUO0ZMmSsq89PDy0bNkypaWl6YknntAdd9yh22+/vWFfKIA6YYYEpwkODtZnn31W9mffvn3KyclRSkqK4uLi5OvrqzVr1pRbZ9GiRXI4HAoODq6wPTc3Nz3wwANKTU1VQkJCpc95yy23VPr41KlTVVJSomXLltX/hQFoEBQSLNezZ0/t2LFD7u7umjVrlv71r39J+u0U8EOHDun6669X+/btK13X19dXkrR58+ZaPWePHj0k/XZnBwBmoJBghBtuuEEhISGSpAULFujChQv6+eefJUnXXXddlet5eHhI+q28aqNNmzaSpAsXLqiwsLAOiQE0NAoJxujTp4+k30oiIyNDPj4+kqSCggLZ7fZK18nLy5OkKmdQVcnPz5f027Go//+4FQBrUEgwxokTJ8r+ftNNN+mWW25Rjx49VFpaqqysrErXOXr0qCRp7NixtXquKydX3HfffXXKCqDhUUgwwvnz5/XOO+9I+u3khw4dOshms+kf//iHJOn999+vsE5paam2bdumXr166ZFHHql0u+np6RUeczgciomJUatWrbR48eIGfBUA6oNCQqOy2+3Kzc2VJF2+fLnSMZmZmQoMDFR2drbuuuuucncE//Of/6wXXnhBL7zwgnbt2lX2eElJiZ599lm1atVKH374oVq0aFFhu56enmrZsqVWrFih0tJSSVJhYaHmzJmjtLQ0xcbGqmfPng35cgHUAx8/gUaRkZGhRx55RJmZmfrll18kSddff70GDhxY7iSFc+fOKTc3V7fddptCQ0MVEhJS6Y1Rv/zyS0VERCgnJ0fXX3+9SkpKNHLkSM2ZM0deXl4Vxq9bt07ffvutoqKitGHDBm3YsEEFBQW6cOGChgwZomeeeUbdu3dvvG8AgFqjkAAARmCXHQDACBQSAMAIFBIAwAgUEgDACBQSAMAIFBIAwAh8HhKcJjo6WtHR0ZY9f1hYmMLCwix7fgDV4zokAIAR2GUHADAChQQ0ce+8845+/PFHq2MAV0UhAU3Ynj17NH36dCUnJ1sdBbgqCglookpKSspO4rhyx3XAZBQS0EStXLlSOTk5kigkuAYKCWiCcnJytGvXLs2aNavsa8B0FBLQBC1atEivvPKKOnXqJIkZElwDhQQ0Mbt371a3bt3k5+enjh07SqKQ4Bq4UwPQhBQXF+v111/Xxo0bJamskE6dOmVlLKBGmCEBTcjKlSsVHh5e9jHxVwqpqKhIZ86csTIacFUUEtBEnDhxQnl5eRo+fHjZY1cKSWK3HczHLjsYJzY2VqtXr67VOnl5eYqLi1OfPn0aKZX5IiIitHTp0nKPeXp6ysvLS/n5+crJyZGfn59F6YCro5BgnClTpmjKlCm1WicgIEB5eXmNlMh8SUlJ+uSTT7R///4Ky4qLiyUxQ4L5KCTAxRUXF2vr1q1KS0urdPmYMWOUlJREIcF4HEMCXFxkZKSmTZtW5XIfHx9JzJBgPgoJcGHZ2dk6cuSIBg0aVOWY9u3bS6KQYD522aFJsNlsstlsVsdwutmzZ+ull16qdgwzJLgKCglNwssvv3xNnUFWWFioBQsWlN2VoTp2u12S9PPPPzsjGlBnfIQ54EIKCws1evRopaWl6fz585J+mwHFxMQoKCio3Ni5c+fq448/1pEjR3Tl17x3797q0qWLduzYoWbNeD8Ks1BIAAAjcFIDAMAIFBIAwAgUEgDACBQSAMAIFBIAwAgUEgDACFyIAKeJjo5WdHS01TFwFWFhYQoLC7M6Bq5BXIcEADACu+wAAEagkAAARqCQAABGoJAAAEagkIB6uHTpkjZu3Gh1DKBJoJCAeli7dq1CQ0P1008/WR0FcHmc9g3Ukd1uV69eveTr66tbb71VUVFRVkcCXBozJKCOtm/fLm9vb61bt04bNmzQ2bNnrY4EuDQKCaijiIgIzZ07V126dNG4ceP05ptvWh0JcGnssgPq4ODBg5owYYKOHTsmd3d3paamatKkScrMzOSjwYE6YoYE1EFkZKRmz54td3d3SdLgwYPl6+uruLg4i5MBrosZElBLOTk56tu3r44dOyYvL6+yx+Pj4/XSSy/pm2++sTAd4LqYIQG1FBUVpalTp5YrI0maOHGiTp8+rc8//9yiZIBrY4YE1MKlS5fUtWtXffnll+revXuF5ZGRkfr888+VkJBgQTrAtTFDAmph/fr18vf3r7SMJGnGjBnavXu3jh075uRkgOtjhgTUkMPhkJ+fn9544w3dddddVY4LDw+X3W7Xa6+95sR0gOtjhgTUUGJiolq2bFltGUnS008/rfXr1ys/P99JyYCmgUICaigyMlLh4eFXHXfzzTdr1KhReuutt5yQCmg62GUH1MDhw4c1duxYZWZmysPD46rj9+7dq5CQEB09erTsWiUA1WOGBNTARx99pHnz5tWojCTJ399f3bp1U0ZGRiMnA5oOZkgAACMwQwIAGIFCAgAYgUICABiBQgIAGIFCAgAYgU8SwzUtOjpa0dHRlj1/WFiYwsLCLHt+wCSc9u2Cpk2bpoyMDH3//fe6ePGiWrRooYEDB5a7APPChQu6ePGiRowYocWLF6tLly4WJgaAq3PpQnrnnXc0bNgw9ezZ0+oolggJCdF7772nFStWaN68eRWW79y5U+PHj1fbtm21d+/ea/b7BMA1uOwxpD179mj69OlKTk62Oopl9u3bJ0kaNWpUpcvHjh1b9qFxS5YscWY0wBhr165VTk6O1TFQAy5ZSCUlJWX73XNzcy1OY43s7GxlZWWpdevW6t+/f5XjunXrJklKS0tzVjTAKO+++y63cHIRLllIK1euLHvHc60WUkpKiiRp2LBhcnOr+n/jlV9EX19fp+QCgLpyuULKycnRrl27NGvWrLKvr0VXCunOO++scszRo0e1Y8cOSdJTTz3llFwAUFcuV0iLFi3SK6+8ok6dOklihuTv71/p8vz8fE2ePFklJSV6/vnnFRQU5Mx4AFBrLlVIu3fvVrdu3eTn56eOHTtKujYLKTc3Vz/99JM8PDw0ZMiQcstKSkqUkJCggQMH6uLFi0pKStLSpUstSgoANecyF8YWFxfr9ddf18aNGyWprJBOnTplZSxLXJkdeXp6KjAwsOxxu92uEydO6OTJk5o8ebKWL1+uG2+80aqYAFArLjNDWrlypcLDw3XddddJ+l8hFRUV6cyZM1ZGc7orhfTEE0/os88+K/uzZ88eHT16VJmZmTp+/Lh69uyp999/v8L6a9asUa9evarc/nPPPacxY8Y0Wn4AqIxLFNKJEyeUl5en4cOHlz12pZCka2+33ZVCqur6ow4dOmj9+vW6cOGCpk2bph9++KHc8o4dO2rmzJlVbr979+4KDQ1tuMAAUAMuUUgRERFavHhxucc8PT3l5eUlqeoz7fbv36/BgwcrOzu70TM6y+nTp3XkyBF5eHjoj3/8Y5XjfH195ePjo8LCQm3btq3csvHjx2v+/PlVrvvoo49q2rRpDZYZAGrC+GNISUlJ+uSTT7R///4Ky4qLiyVVnCHFx8dr+/btstls+uabb1RaWuqUrM6wZ88eORwODR06VC1atKhy3OXLl3X69GlJUqtWrZwVr8mKjY3V6tWra7VOXl6e4uLi1KdPn0ZKBTQtRhdScXGxtm7dWuVdBsaMGaOkpKQKhRQcHKzg4GB99tlnWrdunROSOs/Vdtdd8e6776q0tFSenp66//77JUmbN29Wenq6vvjiC3344Yfy9PQsG3/p0iUtX75cknTgwAHFx8fLw8OjkV6F65kyZYqmTJlSq3UCAgKUl5fXSImApsfoQoqMjKx215GPj4+ka+sY0p49eyRJI0eOrHLMf/7zHz377LNyc3PT6tWr1blzZ+Xm5uro0aNatGiRWrdure+//1533HFH2Tp///vfNW/ePHXo0EHe3t46dOiQ/vCHPzT66wGAK4w9hpSdna0jR45o0KBBVY5p3769pGunkE6dOqXvvvtOzZs319ChQyssLykp0aZNmzR06FB5enpqy5YteuSRRyRJycnJmjp1qvbs2aNmzZrJz8+vbL0zZ86of//+6tChg44fP64zZ86oa9euTntdACAZPEOaPXu2XnrppWrHXCszpMmTJ5fNcOx2u4qKihQQEFBul9rly5d19uxZdezYUUuXLtWjjz6qli1bli0PCQmRJC1evFjBwcFq3rx52bJ27dqVnVWXnJysPn36lH1vAcBZjCukwsJCLViwoOyuDNWx2+2SpJ9//tkZ0SwTFxfXINspKCjQ5s2btXXr1irHJCcna8SIEQ3yfNc6m80mm81mdQzAZRhTSIWFhRo9erTS0tJ0/vx5SVKXLl0UExNT4T5sc+fO1ccff6wjR45Ikn744Qfdeuut6tKli3bs2KFmzYx5WUb54IMP1LZtWwUEBGjNmjV66KGH1KZNm3Jjdu/eraioKGsCNjEvv/xyuV2jaBzx8fHV/szm5uZq4cKF5U7i+b+8vLy0ZcuWau+aD+cw5l9uT09PffHFFzUaGxER0chpmqYvv/xS99xzj0pLS5WVlVWhjNLT05Wbm6u7777bmoBNTHXHP9FwrpxVC9fHW4JryJQpU3Tq1CktWbJEf/3rXyssT05OVv/+/eXt7W1BOgDXOmNmSI3hyjGmK/+91vn7+1e4a0NBQUHZBbY7d+7kHnYALNMkZ0hJSUl66KGHyk55Hjt2rP70pz/pwIEDFiczS1ZWlry9vbVr1y4dOHBA33zzDR/kB8AyNofD4bA6BKxx+vRp3X///QoICFBWVpaWLFnCQXgAlqGQAABGaJK77AAArsfSkxqio6MVHR1tZQRcRVhYmMLCwqyO0Wj4GcTVNPXfAZOwyw4AYAR22QEAjEAhAQCM0KQvjAUA/E9RUZH27t2rY8eO6fTp0/L19dXdd9+tTp06lY1544039Pjjj1uSjxkSADRx2dnZevzxx9WrVy9t2rRJ1113nQYMGKCSkhI9+uij+uc//ylJevHFFxUTE2NZTgqpAV26dEkbN260OgZwVV999ZV+/PHHWq2zbds2nTt3rnECoVE4HA698MIL6tWrly5duqQDBw7ozTffVGhoqO655x6FhoZq586dysnJ0bhx47Ro0SIFBARYlpdCakBr165VaGiofvrpJ6ujANX67rvvtHDhwhqPP3funKZPn67CwsJGTIWGVFBQoEmTJmnJkiVasWKF1q9fr7Zt21Y6dsWKFdq/f78kUUhNgd1u12uvvaYRI0botddeszoOUK3Q0NCyYwk1sWbNGo0fP14dOnRo5GRoCKWlpQoODtaWLVv0/PPP629/+1u141u0aKHAwEA1a9ZMd955p5NSVkQhNZDt27fL29tb69at04YNG3T27FmrIwFVat68uWbOnFmjN08lJSWKiorS3LlznZAMDWHhwoVKTEyUv7+/li5dWqN1evbsqYEDB+p3v/tdI6erGoXUQCIiIjR37lx16dJF48aN05tvvml1JKBaYWFh2rBhg/Lz86sdFx8fr+7du+u2225zUjLUx6FDhxQRESGbzaZVq1bVal0rd9dJFFKDOHjwoDIzMzVp0iRJUnh4uKKiolRSUmJxMqBqHTt2VFBQkN56661qx0VGRio8PNxJqVBfzzzzjOx2u0aMGKEBAwbUeL3bb79dISEhjZjs6iikBhAZGanZs2fL3d1dkjR48GD5+voqLi7O4mRA9cLDw7Vq1SqVlpZWunzfvn06e/asxo8f7+RkqIvjx48rKSlJkjRjxoxarRsYGKj+/fs3Rqwao5DqKScnRx999JFmzpxZ7vHw8HBFRkZalAqomQEDBqhbt25KSEiodHlERITmzJkjm83m5GSoi/j4eEmSzWbTvffea3Ga2qOQ6ikqKkpTp06Vl5dXuccnTpyo06dP6/PPP7coGVAzVb15ysrKUkpKStknL8N86enpkqRevXrJ29vb4jS1RyHVw6VLl7RmzZpKP/bb3d1dTz31FLMkGG/8+PHKy8vT119/Xe7xlStXasaMGWrZsqVFyVBbJ0+elCTdfPPNtVrv+PHjRlxjRiHVw/r16+Xv76/u3btXunzGjBnavXt3ja/1AKzg5uamp59+utybp/Pnz2v9+vV68sknLUyG2mrdurUkqV27drVa78knn5QJn0REIdWRw+HQq6++Wu3ZR61bt9b06dO5UBbG+8tf/qJPP/1U2dnZkn6768i9996rm266yeJkqI3f//73klSrWzz9+9//lq+vr5o3b95IqWqOD+irox07dujvf/+7vv3222rHZWVlacCAAcrKyqpwnAkwyYIFC+RwOLRs2TL16NFD77//vgYNGmR1LNTC4cOH1a9fP3Xo0EEnTpyQm1v1c46SkhI9+OCDiomJ0Q033OCklFVjhlRHNb024+abb9aoUaOueq0HYLUnn3yy7E4jN910E2Xkgvr27atJkyYpNzdXsbGx1Y51OBwKCwvT7NmzjSgjSZIDtZaWlubo3Lmzo6ioqEbjv/jiC0fXrl0dJSUljZwMqJ8pU6Y4PD09HZs3b7Y6Curo7Nmzjr59+zratm3r2Lt3b6VjTpw44Xj44Ycdu3btcnK66vEBfXXw0Ucfad68efLw8KjReH9/f3Xr1k0ZGRny8/Nr5HRA3c2fP1+HDx/WhAkTrI6COmrTpo2+/vprzZ8/X4GBgQoKCtLYsWPl4+OjnJwcffXVV3J3d9err76q9u3bWx23HI4hAUATlZ+fr08//VRZWVmSfjuEMHLkSGOPZ1NIAAAjcFIDAMAIFBIAwAgUEgDACBQSAMAInPb9f0RHRys6OtrqGIBLCwsLU1hYmNUxmqS6/Bt15Q7groCz7AAARmCXHQDACBQSAMAIFBIAwAgUEgDACBQSAMAIFBIAwAgUEgDACBQSjLZ9+3ZNnjy5RmODg4OVkJDQyIkANBYKCUZLSEjQXXfdVaOx/v7+iouLa+REABoLd2qAsTIzMzVs2DClp6erXbt2Vx3/yy+/qF+/fkpNTVXXrl2dkBBAQ2KGBGM9/vjjmjNnTo3KSJJ8fHz03HPP6bHHHhPvswDXwwwJxikpKdHMmTN18uRJJSYmys2t5u+b7Ha77rvvPnl7eysmJkbNmnH/YFx7YmNjtXr16lqtk5eXp7i4OPXp06eRUl0dhQSjfP3111q4cKG8vLy0adMmNW/evNbbKC4uVmhoqE6ePKkXX3xRw4cPb4SkQNMSEBCg559/XgEBAZZl4O0jjLFlyxYFBwfLbrdLklq0aFHvbd55552KjY2t8Zl6AKzDMSQYY+LEicrIyNDo0aP1wAMP6OLFi3I4HLX+c/HiRU2cOFEjRoxQeno6ZQS4CAoJRunRo4cSExPVtm1bTZo0qWy2VFN2u10PPvigOnbsqOTkZPXu3buRkgJoaBQSjNOsWTO9/fbbKi0t1csvv1yrdZcvXy53d3dFR0fLZrM1UkKg6bHZbJb/znBSA4x17Ngx+fv7Kz09XW3btr3q+DNnzqh37946ePCgOnfu7ISEQNPx7bffys/Pr0GO3dYVMyQY65ZbbtG4ceP03nvv1Wh8bGysAgMDKSOgDgYNGmRpGUkUEgw3adIkpaSk1GhsSkqKJkyY0LiBADQadtkBAIzADAkAYAQKCQBgBAoJAGAECgkAYAQKCQBgBG6uCqeaPHmyPvzwQ6tjANeMy5cvWx2hxjjtGwBgBHbZAQCMQCEBAIxAIQEAjEAhAQCMQCEBAIxAIQEAjEAhAQCMQCEBcIrg4GAlJCRYHQMGo5AAOIW/v7/i4uKsjgGDcacGAE7xyy+/qF+/fkpNTVXXrl2tjgMDMUMC4BQ+Pj567rnn9Nhjj4n3wagMMyQATmO323XffffJ29tbMTExataM+zvjf5ghAXAaNzc3ffDBByoqKtLIkSO1b98+qyPBIMyQANTIK6+8ovnz5zfoNm02m2JjYzV58uQG3S5cE4UEwKkKCgo0depUnTt3Tq+//rp69+5tdSQYgh24AJzGbrfrwQcfVPfu3bV582bZbDarI8EgFBIAp1m+fLnc3d0VHR1tdRQYiF12AJzizJkz6t27tw4ePKjOnTtbHQcG4iw7AE4RGxurwMBAyghVopAAOEVKSoomTJhgdQwYjF12AAAjMEMCABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGIFCAgAYgUICABiBQgIAGOH/Af9iBE/IzLasAAAAAElFTkSuQmCC",
      "text/plain": [
       "<Figure size 450x300 with 1 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "input_formula = \"A_1 and B_ij iff not (not Bob and A_) or bot imp (not C)\"\n",
    "testParser(input_formula, 'infix_latex')\n",
    "testParser(input_formula, 'bussproof')\n",
    "testParser(input_formula, 'tree')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "A \\wedge B \\wedge C\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle A \\wedge B \\wedge C$"
      ],
      "text/plain": [
       "<IPython.core.display.Math object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\\begin{prooftree}\n",
      "\\AxiomC{$A$}\n",
      "\\AxiomC{$B$}\n",
      "\\BinaryInfC{$\\wedge$}\n",
      "\\AxiomC{$C$}\n",
      "\\BinaryInfC{$\\wedge$}\n",
      "\\end{prooftree}\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAZYAAAEjCAYAAAAR/ydQAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjcuMSwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy/bCgiHAAAACXBIWXMAAC4jAAAuIwF4pT92AAAO30lEQVR4nO3db6zWdf3H8RccDkMoXZKkNk4wFxjDlqwpdcxCcoG2EjFuxJ+armwisIPlyrnJarVoxhkGLgyZnURbMV2lYsWiYFizmZUUIzrnyAgOrLOIGoJyPOd3o8Fv/OAg+vtcf87p8di84fX9XNv7Bvj0/T3X91xD+vr6+gIAhQyt9QAADC7CAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCAkBRwgJAUcICQFHCwv/bd7/73fzlL3+p9RhAnRhW6wEY2LZs2ZJPf/rTuf/++zNhwoRaj1PUggULsnPnzvzpT3/K4cOHM3LkyEyZMiUNDQ0nzvz73//O4cOHM23atNx1110ZO3ZsDSeG+iAsvGE9PT1ZuHBhkmT//v01nqa8tra2JMncuXPzyCOP5Mtf/nLuuOOOU849/fTT+ehHP5oNGzZk27Ztgy6w8Hq5FcYbdt9996WrqyvJ4AzLcc8880ySZPr06ae9PmPGjMyaNSvd3d25++67qzka1CVh4Q3p6urKz3/+83z2s5898e+D0Z49e/Liiy/m3HPPzbvf/e5+z40fPz5J8sILL1RrNKhbwsIb8qUvfSnf/OY3c/HFFycZvBvLr371qyTJ+973vgwd2v9fl507dyZJmpqaqjIX1DNh4XXbvHlzxo8fn0mTJuWiiy5KMvjDctVVV/V7pr29PU899VSSZPHixVWZC+qZH97zuhw7diz3339/1q9fnyQnwnLgwIFajlUxx8PS3Nx82uuHDh3KnDlz0tPTk2XLluX666+v5nhQl2wsvC733XdfWlpaMnz48CT/G5ZXXnkl//jHP2o5WnH79+/Prl270tjYmCuvvPKkaz09PXnssccyZcqUHD58OJs2bco999xTo0mhvthYOGt79+7N3//+97z//e8/8drxsCT/+Q/x+eefX4vRKuL4tjJixIhcd911J17v7e3N3r17s2/fvsyZMyff+MY38ra3va1WY0LdsbFw1lasWJG77rrrpNdGjBiR8847L8ng+2TY8bB87nOfyy9/+csT/2zZsiXt7e3p7OzM7t27M2HChPzwhz+s8bRQP2wsnJVNmzblZz/7WZ577rlTrh07dizJ4PsB/vGw9Pf8yoUXXpi2traMGzcuCxYsyGWXXZZLL720miNCXRIWXtOxY8fy4x//uN9nNK699tps2rRpUIWlu7s7O3bsSGNjYz7wgQ/0e66pqSljxozJgQMH8pOf/ERYIG6FcRZaW1uzYMGCfq+PGTMmyeDaWLZs2ZK+vr5MnTo1I0eO7Pfcyy+/nO7u7iTJm970pmqNB3VNWDijPXv2ZMeOHXnve9/b75kLLrggyeAKy2vdBjvue9/7Xl599dWMGDEiH/vYx6oxGtQ9t8I4o0WLFmX58uVnPDNYN5Ykueaaa/o989e//jV33nlnhg4dmm9/+9t5+9vfXq3xoK7ZWDito0ePZsmSJSeesj+T3t7eJMnf/va3aoxWcQcOHMgf//jHnHPOOZk6deop13t6evLoo49m6tSpGTFiRB5//PF86lOfqsGkUJ+G9PX19dV6COrH0aNH8+EPfzgvvPBC/vWvfyX5z0aybt26U54qX7p0aX76059mx44dOf7H6NJLL83YsWPz1FNPZdiwgbUQz5kzJ/v37097e3v27duXhoaGXHnllWlsbDxx5uWXX87Bgwdz0UUX5cYbb8zNN9+cUaNG1XBqqD/CAkBRboUBUJSwAFCUsABQlLAAUJSwAFCUsABQ1MB60IAiVq9endWrV9d6jP86CxcuzMKFC2s9BlSc51gAKMqtMACKcisMOKNXXnkl27ZtS0dHR7q7u9PU1JQPfvCDufjii0+cWbNmTW699dYaTkk9sbEAp7Vnz57ceuutmThxYh599NEMHz48l19+eXp6enLzzTfnK1/5SpLk61//etatW1fjaaknNhbgJH19ffna176Wr371q7npppvyu9/9Lm95y1tOOjN//vzcdtttmTlzZp5++unceeedNZqWemRjYcA4cuRI1q9fX+sxBrWXXnops2fPzt1335177703bW1tp0TluHvvvTfPPfdckuRDH/pQFaek3gkLA8aDDz6Y+fPnZ9euXbUeZVB69dVXc9NNN+Xxxx/PsmXLctttt53x/MiRI3Pddddl2LBhueqqq6o0JQOBsDAg9Pb2ZuXKlZk2bVpWrlxZ63EGpS9+8YvZuHFjmpubc88995zVeyZMmJApU6bkzW9+c4WnYyARFgaEJ554IqNHj85DDz2Uhx9+OAcPHqz1SIPK73//+6xYsSJDhgzJt771rdf1XrfB+L+EhQFhxYoVWbp0acaOHZuZM2fmgQceqPVIg8oXvvCF9Pb2Ztq0abn88svP+n3vec97Mnfu3ApOxkDkyXvq3vPPP58bbrghHR0daWhoyLPPPpvZs2ens7NzwH39cT3avXt3xo0blyRZv359PvnJT9Z2IAY8Gwt1r7W1NYsWLUpDQ0OS5IorrkhTU1N+8IMf1HiywWHDhg1JkiFDhuQjH/lIjadhMBAW6lpXV1eefPLJfOYznznp9ZaWlrS2ttZoqsHlz3/+c5Jk4sSJGT16dI2nYTAQFuraqlWrMm/evJx33nknvT5r1qx0d3dn69atNZps8Ni3b1+SnLgddrZ2796do0ePVmAiBjphoW4dOXIk3/nOd7J48eJTrjU0NGTx4sW2lgLOPffcJMn555//ut53++23x49oOR1hoW61tbWlubk5l1xyyWmv33LLLdm8eXM6OjqqPNng8s53vjNJ8s9//vOs3/OHP/whTU1NOeeccyo0FQOZT4VRl/r6+jJp0qSsWbMmV199db/nWlpaTjw8yRuzffv2XHbZZbnwwguzd+/eDB165v/f7OnpyY033ph169blrW99a5WmZCCxsVCXNm7cmFGjRp0xKkmyZMmStLW15dChQ1WabPCZPHlyZs+enf379+f73//+Gc/29fVl4cKFWbRokajQL2GhLrW2tqalpeU1z40bNy7Tp0/P2rVrqzDV4LV27dpMnjw5t99+e5555pnTntm3b1/mzZuXT3ziE7n22murPCEDiVth1J3t27dnxowZ6ezsTGNj42ue37ZtW+bOnZv29vYTz7rw+r300kv5/Oc/n0ceeSTXX399ZsyYkTFjxqSrqyu/+c1v0tDQkGXLluWCCy6o9ajUOWGh7ixfvjzDhw8/q43luGnTpmX16tWZNGlSBSf773Do0KH84he/yIsvvpjkP1vhNddcc8pHvqE/wgJAUX7GAkBRwgJAUcICQFHCAkBRvsyCqpozZ05+9KMf1XoMqujjH/+4rzj4L+NTYQAU5VYYAEUJCwBFCQsARQkLAEUJC1TBkSNHsn79+lqPAVUhLFAFDz74YObPn59du3bVehSoOB83hgrr7e3NxIkT09TUlHe9611ZtWpVrUeCirKxQIU98cQTGT16dB566KE8/PDDOXjwYK1HgooSFqiwFStWZOnSpRk7dmxmzpyZBx54oNYjQUW5FQYV9Pzzz+eGG25IR0dHGhoa8uyzz2b27Nnp7OzMsGF+oxKDk40FKqi1tTWLFi068ZXJV1xxRZqamvzuLAY1GwtUSFdXVyZPnpyOjo6TvtZ3w4YNWb58eX7729/WcDqoHBsLVMiqVasyb968U74rftasWenu7s7WrVtrNBlUlo0FKuDIkSN5xzvekV//+te55JJLTrne2tqarVu35rHHHqvBdFBZNhaogLa2tjQ3N582Kklyyy23ZPPmzeno6KjyZFB5NhYorK+vL5MmTcqaNWty9dVX93uupaUlvb29WblyZRWng8qzsUBhGzduzKhRo84YlSRZsmRJ2tracujQoSpNBtUhLFBYa2trWlpaXvPcuHHjMn369Kxdu7YKU0H1uBUGBW3fvj0zZsxIZ2dnGhsbX/P8tm3bMnfu3LS3t5941gUGOhsLFPTkk0/mjjvuOKuoJElzc3PGjx+fnTt3VngyqB4bCwBF2VgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKEpYAChKWAAoSlgAKOp/AD2LkH4KSyvGAAAAAElFTkSuQmCC",
      "text/plain": [
       "<Figure size 450x300 with 1 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "input_formula = \"A and B and C\" # associativity\n",
    "testParser(input_formula, 'infix_latex')\n",
    "testParser(input_formula, 'tree')\n",
    "testParser(input_formula, 'bussproof')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(A \\wedge B) \\vee C\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle (A \\wedge B) \\vee C$"
      ],
      "text/plain": [
       "<IPython.core.display.Math object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAZYAAAEjCAYAAAAR/ydQAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjcuMSwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy/bCgiHAAAACXBIWXMAAC4jAAAuIwF4pT92AAAO2UlEQVR4nO3dfazWdf3H8RccYQilS5PAhEEWOsIKsqSwGyQXCqsQ448QYrrSyY1hZebYZLVKm8EkcXkTKwpl6XRhqRXTomDWIm+LoXE34m6yFB2KcuT8/mjwmz8Fwd/7nOs6p8dj4w+u7+fa3n8ceJ7P57q++3Zra2trCwAU6d7oAQDoWoQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwsL/209/+tM8+eSTjR4DaBJHNXoAOrcVK1Zk2rRpufHGGzNkyJBGj1Nq6tSpWbt2bf7+979n9+7d6d27d0aMGJGWlpYDa55//vns3r07o0ePzlVXXZUBAwY0cGJoDsLCm9ba2prp06cnSbZv397gaeotXrw4STJ58uTcdttt+da3vpWvfvWrr1l3//33Z/z48bnzzjuzcuXKLhdYOFKOwnjTFixYkG3btiXpmmHZb9WqVUmSMWPGvO71sWPHZsKECdm5c2fmzJnTkaNBUxIW3pRt27bld7/7Xb785S8f+HtXtHnz5mzcuDHHHHNM3ve+9x103eDBg5Mkjz/+eEeNBk1LWHhTvvnNb+YHP/hBTjzxxCRdd8fyhz/8IUnykY98JN27H/yfy9q1a5MkAwcO7JC5oJkJC0fswQcfzODBgzN06ND0798/SdcPy5lnnnnQNevWrcu9996bJJk1a1aHzAXNzIf3HJG9e/fmxhtvzJIlS5LkQFh27NjRyLHazf6wjBo16nWv79q1K5MmTUpra2vmzp2bcePGdeR40JTsWDgiCxYsyOzZs9OzZ88k/xuWl19+Of/+978bOVq57du356mnnkqPHj1yxhlnvOpaa2tr7rrrrowYMSK7d+/O8uXLc/XVVzdoUmgudiwcti1btuTpp5/ORz/60QOv7Q9L8p//iI877rhGjNYu9u9WevXqlXPPPffA6/v27cuWLVuydevWTJo0Kd///vfzjne8o1FjQtOxY+GwzZs3L1ddddWrXuvVq1eOPfbYJF3vm2H7w3LJJZfk97///YE/K1asyLp167Jhw4Zs2rQpQ4YMyR133NHgaaF52LFwWJYvX57f/va3Wb169Wuu7d27N0nX+wB/f1gOdv9Kv379snjx4gwaNChTp07NaaedllNPPbUjR4SmJCy8ob1792bZsmUHvUfj7LPPzvLly7tUWHbu3Jk1a9akR48e+djHPnbQdQMHDkzfvn2zY8eO3HPPPcICcRTGYZg/f36mTp160Ot9+/ZN0rV2LCtWrEhbW1tGjhyZ3r17H3TdSy+9lJ07dyZJ3vKWt3TUeNDUhIVD2rx5c9asWZPTTz/9oGtOOOGEJF0rLG90DLbfz372s7zyyivp1atXPvOZz3TEaND0HIVxSDNnzsy11157yDVddceSJGedddZB1/zzn//MFVdcke7du+dHP/pR3vnOd3bUeNDU7Fh4XXv27Mlll1124C77Q9m3b1+S5F//+ldHjNbuduzYkcceeyxHH310Ro4c+Zrrra2tuf322zNy5Mj06tUrd999d774xS82YFJoTt3a2traGj0EzWPPnj351Kc+lccffzzPPfdckv/sSBYtWvSau8ovv/zy/OY3v8maNWuy/8fo1FNPzYABA3LvvffmqKM614Z40qRJ2b59e9atW5etW7empaUlZ5xxRnr06HFgzUsvvZRnnnkm/fv3z3nnnZcLL7wwffr0aeDU0HyEBYBSjsIAKCUsAJQSFgBKCQsApYQFgFLCAkCpznWjASUWLlyYhQsXNnqM/zrTp0/P9OnTGz0GtDv3sQBQylEYAKUchQGH9PLLL2flypVZv359du7cmYEDB+YTn/hETjzxxANrbrrpplx88cUNnJJmYscCvK7Nmzfn4osvzimnnJLbb789PXv2zPDhw9Pa2poLL7ww3/72t5Mk11xzTRYtWtTgaWkmdizAq7S1teW73/1uvvOd7+T888/P3/72t7ztbW971ZopU6bk0ksvzTnnnJP7778/V1xxRYOmpRnZsdBpvPjii1myZEmjx+jSXnjhhUycODFz5szJddddl8WLF78mKvtdd911Wb16dZLkk5/8ZAdOSbMTFjqNH//4x5kyZUqeeuqpRo/SJb3yyis5//zzc/fdd2fu3Lm59NJLD7m+d+/eOffcc3PUUUflzDPP7KAp6QyEhU5h3759uf766zN69Ohcf/31jR6nS7ryyitz3333ZdSoUbn66qsP6z1DhgzJiBEj8ta3vrWdp6MzERY6hV/96lc5/vjj85Of/CQ///nP88wzzzR6pC7lkUceybx589KtW7f88Ic/PKL3Ogbj/xIWOoV58+bl8ssvz4ABA3LOOefk5ptvbvRIXcrXv/717Nu3L6NHj87w4cMP+30f+MAHMnny5HacjM7Infc0vYcffjif+9znsn79+rS0tOQvf/lLJk6cmA0bNnS6xx83o02bNmXQoEFJkiVLluQLX/hCYwei07NjoenNnz8/M2fOTEtLS5Lkwx/+cAYOHJhf/OIXDZ6sa7jzzjuTJN26dcunP/3pBk9DVyAsNLVt27bl17/+db70pS+96vXZs2dn/vz5DZqqa/nHP/6RJDnllFNy/PHHN3gaugJhoandcMMNueCCC3Lssce+6vUJEyZk586d+eMf/9igybqOrVu3JsmB47DDtWnTpuzZs6cdJqKzExaa1osvvphbbrkls2bNes21lpaWzJo1y66lwDHHHJMkOe64447ofTNmzIiPaHk9wkLTWrx4cUaNGpWTTz75da9fdNFFefDBB7N+/foOnqxrec973pMkefbZZw/7PY8++mgGDhyYo48+up2mojPzrTCaUltbW4YOHZqbbropH//4xw+6bvbs2QdunuTNeeKJJ3LaaaelX79+2bJlS7p3P/Tvm62trTnvvPOyaNGivP3tb++gKelM7FhoSvfdd1/69OlzyKgkyWWXXZbFixdn165dHTRZ1zNs2LBMnDgx27dvz9KlSw+5tq2tLdOnT8/MmTNFhYMSFprS/PnzM3v27DdcN2jQoIwZMya33nprB0zVdd16660ZNmxYZsyYkVWrVr3umq1bt+aCCy7I5z//+Zx99tkdPCGdiaMwms4TTzyRsWPHZsOGDenRo8cbrl+5cmUmT56cdevWHbjXhSP3wgsv5Gtf+1puu+22jBs3LmPHjk3fvn2zbdu2PPTQQ2lpacncuXNzwgknNHpUmpyw0HSuvfba9OzZ87B2LPuNHj06CxcuzNChQ9txsv8Ou3btygMPPJCNGzcm+c+u8KyzznrNV77hYIQFgFI+YwGglLAAUEpYACglLACU8jALOtSkSZPyy1/+stFj0IE++9nPesTBfxnfCgOglKMwAEoJCwClhAWAUsICQClhgUIPPfRQnnzyySN6zz333HNED9mCZicsUOixxx7LlVdeedjrn3322UybNs2z4+lShAUKTZkyJStXrjzsxyXfcsstGT9+fPr169fOk0HHcR8LFJszZ06ef/75N3xccmtra04++eQsW7Ys73//+ztoOmh/wgLFtm3blmHDhmX9+vWHfIbJ0qVLc/PNN+eBBx7owOmg/TkKg2L9+/fPuHHj3vBxyYf7+GXobOxYoB08/PDDmTBhwkEfl7xq1apMmzYta9euTbdu3RowIbQfOxZoB8OHD8/gwYNz1113ve71efPm5Stf+Yqo0CXZsUA7WbZsWa655pqsWrXqVa9v3LgxH/rQh7Jx48b06dOnQdNB+7FjgXYyfvz4PP300/nzn//8qtcXLFiQiy66SFTosuxYoB3dcMMN+dOf/pSlS5cmSZ577rm8613vyiOPPJKTTjqpwdNB+xAWaEe7d+/O4MGDs3r16gwYMCDz58/PX//61yxZsqTRo0G7ERZoZ9/4xjfS1taW733ve3n3u9+dO+64I6effnqjx4J249HE0M5mzJiRD37wg3nve9+bk046SVTo8oQF2tmAAQMyZsyYXHLJJY7A+K/gKAw6wOrVqzNt2rQ8+uij6d7dlzHp2oQFgFJ+dQKglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEr9Dxm8oC5leKbbAAAAAElFTkSuQmCC",
      "text/plain": [
       "<Figure size 450x300 with 1 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "input_formula = \"A and B or C\" # works but not recommended\n",
    "testParser(input_formula, 'infix_latex')\n",
    "testParser(input_formula, 'tree')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(A \\wedge B) \\vee C\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle (A \\wedge B) \\vee C$"
      ],
      "text/plain": [
       "<IPython.core.display.Math object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAZYAAAEjCAYAAAAR/ydQAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjcuMSwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy/bCgiHAAAACXBIWXMAAC4jAAAuIwF4pT92AAAO2UlEQVR4nO3dfazWdf3H8RccYQilS5PAhEEWOsIKsqSwGyQXCqsQ448QYrrSyY1hZebYZLVKm8EkcXkTKwpl6XRhqRXTomDWIm+LoXE34m6yFB2KcuT8/mjwmz8Fwd/7nOs6p8dj4w+u7+fa3n8ceJ7P57q++3Zra2trCwAU6d7oAQDoWoQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwsL/209/+tM8+eSTjR4DaBJHNXoAOrcVK1Zk2rRpufHGGzNkyJBGj1Nq6tSpWbt2bf7+979n9+7d6d27d0aMGJGWlpYDa55//vns3r07o0ePzlVXXZUBAwY0cGJoDsLCm9ba2prp06cnSbZv397gaeotXrw4STJ58uTcdttt+da3vpWvfvWrr1l3//33Z/z48bnzzjuzcuXKLhdYOFKOwnjTFixYkG3btiXpmmHZb9WqVUmSMWPGvO71sWPHZsKECdm5c2fmzJnTkaNBUxIW3pRt27bld7/7Xb785S8f+HtXtHnz5mzcuDHHHHNM3ve+9x103eDBg5Mkjz/+eEeNBk1LWHhTvvnNb+YHP/hBTjzxxCRdd8fyhz/8IUnykY98JN27H/yfy9q1a5MkAwcO7JC5oJkJC0fswQcfzODBgzN06ND0798/SdcPy5lnnnnQNevWrcu9996bJJk1a1aHzAXNzIf3HJG9e/fmxhtvzJIlS5LkQFh27NjRyLHazf6wjBo16nWv79q1K5MmTUpra2vmzp2bcePGdeR40JTsWDgiCxYsyOzZs9OzZ88k/xuWl19+Of/+978bOVq57du356mnnkqPHj1yxhlnvOpaa2tr7rrrrowYMSK7d+/O8uXLc/XVVzdoUmgudiwcti1btuTpp5/ORz/60QOv7Q9L8p//iI877rhGjNYu9u9WevXqlXPPPffA6/v27cuWLVuydevWTJo0Kd///vfzjne8o1FjQtOxY+GwzZs3L1ddddWrXuvVq1eOPfbYJF3vm2H7w3LJJZfk97///YE/K1asyLp167Jhw4Zs2rQpQ4YMyR133NHgaaF52LFwWJYvX57f/va3Wb169Wuu7d27N0nX+wB/f1gOdv9Kv379snjx4gwaNChTp07NaaedllNPPbUjR4SmJCy8ob1792bZsmUHvUfj7LPPzvLly7tUWHbu3Jk1a9akR48e+djHPnbQdQMHDkzfvn2zY8eO3HPPPcICcRTGYZg/f36mTp160Ot9+/ZN0rV2LCtWrEhbW1tGjhyZ3r17H3TdSy+9lJ07dyZJ3vKWt3TUeNDUhIVD2rx5c9asWZPTTz/9oGtOOOGEJF0rLG90DLbfz372s7zyyivp1atXPvOZz3TEaND0HIVxSDNnzsy11157yDVddceSJGedddZB1/zzn//MFVdcke7du+dHP/pR3vnOd3bUeNDU7Fh4XXv27Mlll1124C77Q9m3b1+S5F//+ldHjNbuduzYkcceeyxHH310Ro4c+Zrrra2tuf322zNy5Mj06tUrd999d774xS82YFJoTt3a2traGj0EzWPPnj351Kc+lccffzzPPfdckv/sSBYtWvSau8ovv/zy/OY3v8maNWuy/8fo1FNPzYABA3LvvffmqKM614Z40qRJ2b59e9atW5etW7empaUlZ5xxRnr06HFgzUsvvZRnnnkm/fv3z3nnnZcLL7wwffr0aeDU0HyEBYBSjsIAKCUsAJQSFgBKCQsApYQFgFLCAkCpznWjASUWLlyYhQsXNnqM/zrTp0/P9OnTGz0GtDv3sQBQylEYAKUchQGH9PLLL2flypVZv359du7cmYEDB+YTn/hETjzxxANrbrrpplx88cUNnJJmYscCvK7Nmzfn4osvzimnnJLbb789PXv2zPDhw9Pa2poLL7ww3/72t5Mk11xzTRYtWtTgaWkmdizAq7S1teW73/1uvvOd7+T888/P3/72t7ztbW971ZopU6bk0ksvzTnnnJP7778/V1xxRYOmpRnZsdBpvPjii1myZEmjx+jSXnjhhUycODFz5szJddddl8WLF78mKvtdd911Wb16dZLkk5/8ZAdOSbMTFjqNH//4x5kyZUqeeuqpRo/SJb3yyis5//zzc/fdd2fu3Lm59NJLD7m+d+/eOffcc3PUUUflzDPP7KAp6QyEhU5h3759uf766zN69Ohcf/31jR6nS7ryyitz3333ZdSoUbn66qsP6z1DhgzJiBEj8ta3vrWdp6MzERY6hV/96lc5/vjj85Of/CQ///nP88wzzzR6pC7lkUceybx589KtW7f88Ic/PKL3Ogbj/xIWOoV58+bl8ssvz4ABA3LOOefk5ptvbvRIXcrXv/717Nu3L6NHj87w4cMP+30f+MAHMnny5HacjM7Infc0vYcffjif+9znsn79+rS0tOQvf/lLJk6cmA0bNnS6xx83o02bNmXQoEFJkiVLluQLX/hCYwei07NjoenNnz8/M2fOTEtLS5Lkwx/+cAYOHJhf/OIXDZ6sa7jzzjuTJN26dcunP/3pBk9DVyAsNLVt27bl17/+db70pS+96vXZs2dn/vz5DZqqa/nHP/6RJDnllFNy/PHHN3gaugJhoandcMMNueCCC3Lssce+6vUJEyZk586d+eMf/9igybqOrVu3JsmB47DDtWnTpuzZs6cdJqKzExaa1osvvphbbrkls2bNes21lpaWzJo1y66lwDHHHJMkOe64447ofTNmzIiPaHk9wkLTWrx4cUaNGpWTTz75da9fdNFFefDBB7N+/foOnqxrec973pMkefbZZw/7PY8++mgGDhyYo48+up2mojPzrTCaUltbW4YOHZqbbropH//4xw+6bvbs2QdunuTNeeKJJ3LaaaelX79+2bJlS7p3P/Tvm62trTnvvPOyaNGivP3tb++gKelM7FhoSvfdd1/69OlzyKgkyWWXXZbFixdn165dHTRZ1zNs2LBMnDgx27dvz9KlSw+5tq2tLdOnT8/MmTNFhYMSFprS/PnzM3v27DdcN2jQoIwZMya33nprB0zVdd16660ZNmxYZsyYkVWrVr3umq1bt+aCCy7I5z//+Zx99tkdPCGdiaMwms4TTzyRsWPHZsOGDenRo8cbrl+5cmUmT56cdevWHbjXhSP3wgsv5Gtf+1puu+22jBs3LmPHjk3fvn2zbdu2PPTQQ2lpacncuXNzwgknNHpUmpyw0HSuvfba9OzZ87B2LPuNHj06CxcuzNChQ9txsv8Ou3btygMPPJCNGzcm+c+u8KyzznrNV77hYIQFgFI+YwGglLAAUEpYACglLACU8jALOtSkSZPyy1/+stFj0IE++9nPesTBfxnfCgOglKMwAEoJCwClhAWAUsICQClhgUIPPfRQnnzyySN6zz333HNED9mCZicsUOixxx7LlVdeedjrn3322UybNs2z4+lShAUKTZkyJStXrjzsxyXfcsstGT9+fPr169fOk0HHcR8LFJszZ06ef/75N3xccmtra04++eQsW7Ys73//+ztoOmh/wgLFtm3blmHDhmX9+vWHfIbJ0qVLc/PNN+eBBx7owOmg/TkKg2L9+/fPuHHj3vBxyYf7+GXobOxYoB08/PDDmTBhwkEfl7xq1apMmzYta9euTbdu3RowIbQfOxZoB8OHD8/gwYNz1113ve71efPm5Stf+Yqo0CXZsUA7WbZsWa655pqsWrXqVa9v3LgxH/rQh7Jx48b06dOnQdNB+7FjgXYyfvz4PP300/nzn//8qtcXLFiQiy66SFTosuxYoB3dcMMN+dOf/pSlS5cmSZ577rm8613vyiOPPJKTTjqpwdNB+xAWaEe7d+/O4MGDs3r16gwYMCDz58/PX//61yxZsqTRo0G7ERZoZ9/4xjfS1taW733ve3n3u9+dO+64I6effnqjx4J249HE0M5mzJiRD37wg3nve9+bk046SVTo8oQF2tmAAQMyZsyYXHLJJY7A+K/gKAw6wOrVqzNt2rQ8+uij6d7dlzHp2oQFgFJ+dQKglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEr9Dxm8oC5leKbbAAAAAElFTkSuQmCC",
      "text/plain": [
       "<Figure size 450x300 with 1 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "input_formula = \"(A and B) or C\" # recommended\n",
    "testParser(input_formula, 'infix_latex')\n",
    "testParser(input_formula, 'tree')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "A \\wedge (B \\vee C)\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle A \\wedge (B \\vee C)$"
      ],
      "text/plain": [
       "<IPython.core.display.Math object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAZYAAAEjCAYAAAAR/ydQAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjcuMSwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy/bCgiHAAAACXBIWXMAAC4jAAAuIwF4pT92AAAOu0lEQVR4nO3db6zWdf3H8RcgBGK6pZAQnGAuSXMV2bIiyqFNElb5B2YWDHRlBkSHwmlbi1Y3zBVnIjQtdElSrZiVGqwynTjKamZGC6lAHPHHyYRjK1EO5+rGb9AP5a++z7ng8Hhs3OB8P2d73dA9+X6v6zqnV6PRaAQAivRu9gAAehZhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGg1AnNHgAc3V588cWsWrUq69evz7Zt29LS0pIPfOADGTp06N4zt912W6655pomruRo4o4F9mPq1Kk577zzctJJJ6VXr14ZOHBgxo4dm/PPP3/vn3PPPTdvfvObc+2112bjxo3Nnlxu48aNueaaazJq1Kj84Ac/SL9+/TJ69Oh0dHTkqquuyle/+tUkyY033pg77rijyWs5qjSAA7ryyisbSRrf+MY39nt9xYoVjT59+jROO+20xtq1a7t5Xdfo7OxsfO1rX2sMGDCgMWXKlMazzz6733PXXnttY/z48Y0kjeuuu66bV3I0ExY4iBEjRjSSNB577LEDnrn88ssbSRqTJk3qvmFd5N///nfjkksuaSRpLFq06JBnBw0a1EjSWL58eTct5FjgURgcwMaNG7Nhw4acfPLJeetb33rAcyNHjkySrF69urumdYndu3fn8ssvz09+8pPMmzcvn/nMZw56/sQTT8zFF1+cE044Ie973/u6aSXHAmGBA3jooYeSJO95z3vSu/eB/1dZu3ZtkqSlpaVbdnWV66+/PitWrMiYMWPy5S9/+bC+58wzz8w73vGOvPa1r+3idRxLhAUOYE9YDvav8XXr1mX58uVJks9+9rPdsqsr/OlPf8r8+fPTq1ev3HLLLUf0veeff37XjOKY5e3GcAB7wjJmzJj9Xm9vb8/kyZPT0dGRefPmZcKECd05r9TcuXPT2dmZcePGZfTo0Yf9fW9/+9szbNiwLlzGsahXo9FoNHsEHG22bt2aIUOGpG/fvtmxY0dOPPHEvdc6Ojpyzz33ZO7cuenbt28WLVqUCy64oIlrX52nnnoqI0aMSJIsXbo0V155ZXMHccxzxwL7sedupX///rn44ov3fr2zszObNm3K5s2bM3ny5Nx00015/etf36yZJZYtW5Yk6dWrVy666KImr6EnEBbYjz1h+fSnP52bbrrpZde3bt2aK664ImeeeWYWL16cSZMmdffEMn/961+TJKNGjcqpp57a5DX0BF68h/3YE5YDPeI6/fTTs2TJkvzrX//K1KlT88QTT3TnvFKbN29Okr2Pww7XU089lZ07d3bBIo51wgIvsW3btqxZsyZ9+/bN2LFjD3iupaUlgwcPzs6dO3Pvvfd248JaJ598cpLkda973RF938yZM+MlWvZHWOAlVq5cmUajkXe/+937vGj/Ui+88EK2bduWJDnppJO6a165N73pTUmSHTt2HPb3PP7442lpacmAAQO6aBXHMmGBlzjUY7A9vve972X37t3p379/PvzhD3fHtC5xxRVXJEn++Mc/prOz85DnOzo68qUvfSlf+cpXunoaxyhhgZdYuXJlkmTcuHEHPPOPf/wj1113XXr37p1bb701b3jDG7prXrlzzjknl112WbZu3Zof/vCHBz3baDQyY8aMzJo1K6eddlo3LeRY43Ms8P88/fTTGTp0aF7zmtekvb09ffv23ed6R0dHfvzjH2fWrFnp169fbr311mP6bmWPHTt2ZOzYsdm0aVPuu+++vPe9733Zmc2bN2fu3LmZPn16Lrzwwias5FghLJBk8uTJ2bp1a9atW5fNmzenT58+Oe+88/YJywsvvJDt27dnyJAhufTSS3PVVVdl4MCBTVxd6z//+U++8IUv5Pvf/34mTJiQ8ePHZ/DgwdmyZUseeeSR9OnTJ/PmzcugQYOaPZWjnLAA+2hvb88DDzyQDRs2JPm/tyGPGzcup5xySnOHccwQFgBKefEegFLCAkApYQGglLAAUEpYACjlx+Zz3Fi0aFEWLVrU7BnHnRkzZmTGjBnNnkE38nZjAEp5FMarduedd+Zvf/tbs2cARwlh4VVZuXJlpk2bll//+tfNngIcJYSFV6yjo2Pvs/OtW7c2eQ1wtBAWXrEFCxZky5YtSYQF+B9h4RXZsmVLfvWrX+VTn/rU3r/z6jzyyCNH/FrVvffee0S/+RG6g7Dwitxwww355je/maFDhyZxx1Lhz3/+c66//vrDPr9jx45MmzYtO3fu7MJVcOSEhSP24IMPZuTIkTn77LMzZMiQJMJSYcqUKVm1alXWr19/WOe/853vZOLEiTn99NO7eBkcGWHhiOzatSvf+ta3csMNNyTJ3rA8/fTTzZzVIwwYMCCf/OQnc/PNNx/ybEdHRxYuXJg5c+Z0wzI4MsLCEVmwYEFaW1vTr1+/JP8Ly4svvphnn322mdN6hBkzZuSuu+5Ke3v7Qc8tW7YsZ5xxRt72trd10zI4fMLCYdu0aVOeeeaZfX4f+p6wJB6HVRgyZEgmTJiQxYsXH/RcW1tbWltbu2kVHBlh4bDNnz8/X/ziF/f5Wv/+/ff+ylrvDKvR2tqaW265Jbt3797v9d/85jfZvn17Jk6c2M3L4PD4IZQclvvvvz+//OUv8+ijj77s2q5du5K4Y6kyevTojBw5MnfffXcmTZr0suvz58/P5z73ufTq1asJ6+DQhIVD2rVrV+65556sXr16v9c/+MEP5v777xeWQq2trbnxxhtfFpYNGzbkoYceyp133tmkZXBoHoVxSG1tbZk6deoBrw8ePDiJO5ZKEydOzDPPPJPf/e53+3x9wYIFufrqqzNw4MAmLYNDExYOauPGjVmzZk3e+c53HvDMoEGDkghLpd69e2f27Nlpa2vb+7XnnnsuS5YsycyZM5u4DA5NWDioWbNmHfLT4O5Yusb06dPzwAMPZOPGjUmS22+/PRdddFGGDRvW5GVwcMLCfu3cuTOzZ8/e+yn7g+ns7EyS/POf/+yOaceNgQMHZvr06XvfIbbnM0RwtPPiPfvYuXNnLrzwwqxevTrPPfdckmT48OG54447MmHChH3OzpkzJ7/4xS+yZs2aJMkTTzyRs846K8OHD8/y5ctzwgn+83q1Zs6cmXPPPTdvectbMmzYsIM+koSjhV9NDEe5j33sY/npT3+apUuX5tJLL232HDgkYYGj3KOPPppp06bl8ccfT+/enl5z9BMWAEr55w8ApYQFgFLCAkApYQGglA8aHIcmT56cn/3sZ82eQTf6yEc+kh/96EfNnsFxwrvCACjlURgApYQFgFLCAkApYQGglLBw3Hj++eezdOnSZs+AHk9YOG7cfvvtmTJlSv7+9783ewr0aN5uzHGhs7Mzo0aNSktLS84666wsXLiw2ZOgx3LHwnHhvvvuy6mnnprvfve7ueuuu7J9+/ZmT4IeS1g4LsyfPz9z5szJ8OHD86EPfSjf/va3mz0JeiyPwujxHnvssXz0ox/N+vXr06dPn/z+97/PZZddlieffNKvT4Yu4I6FHq+trS2zZs1Knz59kiTvete70tLS4mdnQRdxx0KPtmXLlpxzzjlZv359TjnllL1fX7ZsWb7+9a/nD3/4QxPXQc/kjoUebeHChfnEJz6xT1SS5JJLLsm2bdvy8MMPN2kZ9FzuWOixnn/++bzxjW/Mb3/725xxxhkvu97W1paHH344d999dxPWQc/ljoUea8mSJRkzZsx+o5IkV199dR588MGsX7++m5dBz+aOhR6p0Wjk7LPPzm233Zb3v//9BzzX2tqazs7O3Hzzzd24Dno2dyz0SCtWrMjAgQMPGpUkmT17dpYsWZL29vZuWgY9n7DQI7W1taW1tfWQ50aMGJELLrggixcv7oZVcHzwKIwe5y9/+UvGjx+fJ598Mn379j3k+VWrVuXjH/941q1bt/ezLsAr546FHufnP/95Pv/5zx9WVJJkzJgxGTlyZNauXdvFy+D44I4FgFLuWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFLCAkApYQGglLAAUEpYACglLACUEhYASgkLAKWEBYBSwgJAKWEBoJSwAFBKWAAoJSwAlBIWAEoJCwClhAWAUsICQClhAaCUsABQSlgAKCUsAJQSFgBKCQsApYQFgFL/BRgrvhdEtA0DAAAAAElFTkSuQmCC",
      "text/plain": [
       "<Figure size 450x300 with 1 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "input_formula = \"A and (B or C)\" # works as expected\n",
    "testParser(input_formula, 'infix_latex')\n",
    "testParser(input_formula, 'tree')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "imp not A imp B and not C D\n",
      "A not B C not D and imp imp\n",
      "\\neg A \\rightarrow B \\rightarrow \\neg C \\wedge D\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\neg A \\rightarrow B \\rightarrow \\neg C \\wedge D$"
      ],
      "text/plain": [
       "<IPython.core.display.Math object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\\begin{prooftree}\n",
      "\\AxiomC{$A$}\n",
      "\\UnaryInfC{$\\neg$}\n",
      "\\AxiomC{$B$}\n",
      "\\AxiomC{$C$}\n",
      "\\UnaryInfC{$\\neg$}\n",
      "\\AxiomC{$D$}\n",
      "\\BinaryInfC{$\\wedge$}\n",
      "\\BinaryInfC{$\\rightarrow$}\n",
      "\\BinaryInfC{$\\rightarrow$}\n",
      "\\end{prooftree}\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAZYAAAEjCAYAAAAR/ydQAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjcuMSwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy/bCgiHAAAACXBIWXMAAC4jAAAuIwF4pT92AAASEklEQVR4nO3deWyU5buH8e90gbIISKUKSAGJQFhUEGQpS9nCLgJNg7LIFjFUIKWALCYQjcoPAghaghobQZaKbCqyRCKLgRiIgoJtkK0UKEsRqEAppcycPzztORwowvHuvJ13rk9CIp1nyh0hveZ5lxmPz+fzCQAAIyFODwAAcBfCAgAwRVgAAKYICwDAFGEBAJgiLAAAU4QFAGCKsAAATBEWAIApwgIAMEVYAACmCAsAwBRhAQCYIiwAAFOEBQBgirAAAEwRFgCAKcICADBFWAAApggLAMAUYQEAmCIsAABThAUAYIqwAABMERYAgCnCAgAwRVgAAKYICwDAFGEBAJgiLAAAU4QFAGCKsAAATBEWAIApwgIAMEVYAACmCAsAwBRhAQCYIiwAAFOEBQBgirAAAEwRFgCAKcICADBFWAAApggLAMAUYQEAmCIsAABThAUAYIqwAABMERYAgCnCAgAwRVgAAKYICwDAFGEBAJgiLAAAU4QFAGCKsAAATBEWAIApwgIAMEVYAACmCAsAwBRhAQCYIiwAAFOEBQBgirAAAEwRFgCAKcICADBFWAAApggLAMAUYQEAmCIsAABThAUAYIqwAABMERYAgCnCAgAwRVgAAKYICwDAFGEBAJgiLAAAU4QFAGAqzOkBAJSs/Px87d69W8ePH9fFixcVHR2tjh07qkaNGkVrPv74Y40ZM8bBKeEm7FgAlzp16pTGjBmjBg0aaNWqVSpTpoyaNWumgoICjRw5Uu+8844kafbs2UpJSXF4WrgJOxbAZXw+n9577z29++67iouL0y+//KJHH330jjVDhw7V2LFj1bNnT23ZskVTpkxxaFq4kcfn8/mcHgKAjdzcXA0ZMkTr169XcnKyxo4de9+1derUUXZ2tjZt2qSePXv6cVK4GYfCAJe4ffu24uLitH79es2aNeu+UZGk8uXLq1evXgoLC1O7du38NCWCAWEBXGLq1KnavHmzYmJiNHPmzAd6Tv369dW8eXM98sgjJTwdgglhAVzgwIEDmj9/vjwejz788MOHem5sbGzJDIWgxcl7wAUmT54sr9erzp07q1mzZg/8vOeee05PPvlkCU6GYMTJeyDAnTx5UnXq1JEkrVixQq+88oqzAyHocSgMCHBr1qyRJHk8HnXv3t3haQDCAgS8tLQ0SVKDBg0UGRnp8DQAYQECXlZWliQVHQ57UCdPnlReXl4JTIRgR1iAAFepUiVJUtWqVR/qeW+88YY4xYqSQFiAAPf0009Lkq5cufLAz/n1118VHR2tcuXKldBUCGZcFQYEuEOHDqlp06Z64okndObMGYWE3P/1YkFBgQYMGKCUlBQ99thjfpoSwYQdCxDgmjRpooEDB+rcuXNKTU2971qfz6eEhASNGzeOqKDEsGMBXODKlStq3769zpw5o40bN6pt27Z3rcnKytLkyZM1YsQIde3a1YEpESwIC+ASubm5mjRpklauXKnevXurR48eioqK0tmzZ/XTTz8pNDRUs2bNUrVq1ZweFS5HWACXycnJ0Q8//KCMjAxJf1+G3LlzZ1WuXNnZwRA0CAsAwBQn7wEApggLAMAUYQEAmCIsAABTfNAXUMolJycrOTnZ0RkSEhKUkJDg6AwIHFwVBgAwxaEwAIApwgIAMMU5FgCuMWzYMB0+fFhpaWm6du2aypYtqxYtWigs7O8fdV6vV5cuXVJ+fr569uyppKQkRUdHOzy1+3COBYDrDB48WCtXrtSbb76p2bNn3/V4enq6Ro8erfT0dG3YsEEdOnRwYEr3IiwAXKdu3brKyMjQtm3b1KVLl3uuuXbtmp599lnl5OQoLS1NUVFRfp7SvTjHAsBVMjMzlZGRofDwcLVp06bYdRUrVlRiYqL+/PNPzZkzx48Tuh9hAeAqO3fulCS1bNlS5cuXv+/amJgYSdKXX35Z4nMFE8ICwFUKwxIbG/uPaytWrChJOn36tHJzc0tyrKBCWAC4SmFYOnbs+I9rL1++XPTfV69eLbGZgg1hAeAaWVlZOnr0qMLCwu758cz/V3p6uiQpLCyMT9Y0RFgAuEbhbuX5558vOsx1P/v27ZMkNWrUSCEh/Di0wg2SgEukpqZqyZIlD/Wc7OxsrV69Wo0bNy6hqfxrx44dkh7sMJgkbd26VZLUr1+/khopKBEWwCUGDRqkQYMGPdRzYmNjlZ2dXUIT+d/DnF/5+eefdfToUYWHh2vEiBElPVpQYe8HwBXOnz+vw4cPKzQ0VO3atfvH9YsXL5YkjRo1SnXr1i3p8YIKYQHgCoW7lWbNmqlSpUr3XZuenq6lS5fqqaee0vvvv++P8YIKYQHgCg96GCwvL09Dhw5VhQoVtGbNGlWpUsUP0wUXwgIEMY/HI4/H4/QYJh4kLJcvX1afPn2UmZmp7du3q1mzZv4aL6gQFiCIzZ07Vy1btnR6jH8tMzNTaWlpknTP8ys5OTlasmSJGjVqpCpVqujAgQNq3ry5v8cMGry7MYCAFRcXp5MnT+rIkSPKycmRJLVq1UoRERGSJJ/Pp7y8POXn56tt27YaPny4K0Ja2hEWAIApDoUBAEwRFgCAKcICADBFWAAApggLAMAUYQEAmOLdjYFSLjk5WcnJyU6PEbQSEhKUkJDg9BgBhftYAACmOBTmAkuXLtUff/zh9BgAIIlDYQFv165dGj58uBYvXqz69es7PU6pMWzYMB0+fFi///67rl+/rvLly6t58+YKDQ0tWnP16lVdv35dnTp10vTp01WrVi0HJwbcg7AEsIKCgqJjv+fOnXN4mtJl2bJlkqTBgwdr5cqVevvtt5WUlHTXui1btqhPnz5as2aNdu/eTZwBAxwKC2CLFi3S2bNnJRGW4uzZs0eS1KVLl3s+3qNHD/Xv318XL17UW2+95c/RANciLAHq7Nmz+v777/Xaa68V/R53OnXqlDIyMlSpUiU988wzxa4r/FjagwcP+mu0oHHjxg2tWLHC6THgZ4QlQE2bNk3z5s1TjRo1JLFjuZfCD35q06aNQkKK/6d++PBhSVJ0dLRf5gomn332mYYOHaojR444PQr8iLAEoO3bt6tu3bpq1KiRqlevLomw3EthWO71wU+Fjh07pk2bNkmSxo8f75e5goXX69XChQvVqVMnLVy40Olx4EeEJcDcunVLixcv1rRp0ySpKCznz593cqxSqTAsMTEx93w8JydH8fHxKigo0KxZs9S7d29/jud6GzduVGRkpD7//HMtX75cly9fdnok+AlhCTCLFi1SYmKiypQpI+l/wpKfn69Lly45OVqpcu7cOR05ckTh4eFq1arVHY8VFBRo3bp1at68ua5fv65t27Zp5syZDk3qXvPnz9fEiRNVq1Yt9ezZU5988onTI8FPuNw4gJw5c0bZ2dlq27Zt0dcKwyL9/cO0atWqToxW6hTuViIiItSrV6+ir3u9Xp05c0ZZWVmKj4/XnDlz9Pjjjzs1pmvt379fJ06c0MCBAyVJiYmJGjhwoJKSkhQWxo8dt2PHEkDmz5+v6dOn3/G1iIgIVa5cWRJXhv1vhWF5/fXXtWPHjqJfu3bt0rFjx3TixAmdPHlS9evX11dffeXwtO6zYMECjRs3ruiG1BdeeEHR0dFavXq1w5PBH3ivsACxbds2JSYmKjIy8q7H9u3bp9zcXC1fvlyDBw92YLrSp3HjxkpLS9OWLVvUvXv3e67JzMxUnTp1VLZsWe3fv18NGzb085TudPbsWTVp0kTHjx8vetEjSWvWrNF//vMf7du3z8Hp4A/sSQPArVu39M033xR7n0W3bt20bds2rgz7bxcvXlR6errCw8PVvn37YtdFR0crKipK58+f17fffktYjHz00UcaMmTIHVGRpP79+2vy5Mn68ccf7/v3gsDHobAAsGDBAg0bNqzYx6OioiRxyXGhXbt2yefzqXXr1ipfvnyx627evKmLFy9KkipWrOiv8Vztxo0b+vTTT+956XZoaKjGjx+vBQsWODAZ/ImwlHKnTp1Senq6WrRoUeyaatWqSSIshQrPrxT3Ni6FvvjiC92+fVsRERF68cUX/TGa6y1btkwxMTGqV6/ePR8fNWqUtm/fruPHj/t5MvgTYSnlxo0bp6lTp953DTuWO+3atUuS1Llz52LXHD16VFOmTFFISIiWLFmimjVr+ms81/L5fPrggw+UmJhY7JpKlSpp+PDh3DDpcoSllMrLy9OECROK7rK/H6/XK0k6ffq0P0Yr1c6fP6/ffvtN5cqVU+vWre96vKCgQKtWrVLr1q0VERGh9evX69VXX3VgUvfZvHmzKlSooA4dOtx33YQJE7Rs2TLl5OT4aTL4G1eFlTJ5eXnq2rWrDh48qL/++kvS3zuSlJSUu+4MnzhxorZu3ar09HQV/jU2bNhQtWrV0qZNm4LqfoH4+HidO3dOx44dU1ZWlkJDQ9WqVSuFh4cXrbl586YuX76s6tWra8CAARo5cqQqVKjg4NTu0q1bNw0fPvyBrkyMi4tTmzZt7vlRBgh8hAXAv3bo0CH16NFDJ06cuCPmxdm9e7cGDx6sY8eO3fHha3AHDoUB+Ne+++47JSUlPVBUpL/fv61u3bpF7ywNd2HHAgAwxY4FAGCKsAAATBEWAIApwgIAMBU8NzqUIsnJyUpOTnbsz09ISFBCQoJjf/7/l9P/3+CMQP33Gsy4KgwAYIpDYQAAU4QFAGCKsAAATBEWAIApwgIAMEVYAACmCAsAwBRhAQJcXFyc1q1b5/QYQBHCAgS4mJgYrV692ukxgCLceQ8EuAsXLqhp06bau3evateu7fQ4ADsWINBFRUVpxowZGj16tHidiNKAHQvgAl6vV3379lVkZKRSUlIUFsb7y8I5hKWUSk1N1ZIlSx7qOdnZ2Vq9erUaN25cQlOhNLt165aGDh2qrKwszZ49W23btnV6JAQpwuIisbGxmjVrlmJjY50eBQ9h3rx5mjRpkun39Hg8Sk1NVXx8vOn3BR4E51gAhyUlJcnn8/3rX9evX1f//v3VqVMnpaWlERU4hgOxgAt4vV4NGDBA9erV09q1a+XxeJweCUGMsAAuMGfOHIWGhvIJmygVCIuLeDweXqkGoUuXLmn+/Pnav3+/06MAkgiLq8ydO1eNGjVyegz4WWpqqnr16qWaNWs6PQogibC4SosWLZweAQ7YuXOnXn75ZafHAIpwuTEAwBSXGwMATBEWAIApwgIAMEVYAACmCAsAwBSXGzsgPj5eX3/9tdNjIIj069ePT5mE33C5MQDAFIfCAACmCAsAwBRhAQCYIiwAAFOEBQBgirAAAEwRFgCAKcIC14iLi9O6deucHgMIeoQFrhETE8Pd5UApwJ33cI0LFy6oadOm2rt3r2rXru30OEDQYscC14iKitKMGTM0evRo8XoJcA47FriK1+tV3759FRkZqZSUFIWF8T6rgL+xY4GrhISEaMOGDcrPz1fnzp21Z88ep0cCgg47FpQa8+bN06RJk0y/p8fjUWpqquLj402/L4DiERa4Tm5uroYMGaIrV65o8eLFatiwodMjAUGFA9BwFa/XqwEDBqhevXpau3atPB6P0yMBQYewwFXmzJmj0NBQJScnOz0KELQ4FAbXuHTpkho2bKj9+/erZs2aTo8DBC2uCoNrpKamqlevXkQFcBhhgWvs3LlTL730ktNjAEGPQ2EAAFPsWAAApggLAMAUYQEAmCIsAABThAUAYIqwAABMERYAgCnCAgAwRVgAAKYICwDAFGEBAJgiLAAAU4QFAGCKsAAATBEWAIApwgIAMEVYAACmCAsAwBRhAQCYIiwAAFOEBQBgirAAAEwRFgCAKcICADBFWAAApggLAMAUYQEAmCIsAABThAUAYIqwAABMERYAgCnCAgAwRVgAAKYICwDAFGEBAJgiLAAAU4QFAGCKsAAATBEWAIApwgIAMEVYAACmCAsAwBRhAQCYIiwAAFOEBQBgirAAAEwRFgCAKcICADBFWAAApggLAMAUYQEAmCIsAABThAUAYIqwAABMERYAgCnCAgAwRVgAAKYICwDAFGEBAJgiLAAAU4QFAGCKsAAATBEWAIApwgIAMEVYAACmCAsAwBRhAQCYIiwAAFOEBQBgirAAAEwRFgCAKcICADBFWAAApggLAMAUYQEAmCIsAABThAUAYIqwAABMERYAgCnCAgAwRVgAAKb+C/T59sIwPofGAAAAAElFTkSuQmCC",
      "text/plain": [
       "<Figure size 450x300 with 1 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "input_formula = \"not A imp B imp not C and D\"\n",
    "testParser(input_formula) # default: polish notation\n",
    "testParser(input_formula, 'RPN')\n",
    "testParser(input_formula, 'infix_latex')\n",
    "testParser(input_formula, 'tree')\n",
    "testParser(input_formula, 'bussproof')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "imp not A_Cat_ij xor Bob and not C_1 D_12\n",
      "A_Cat_ij not Bob C_1 not D_12 and xor imp\n",
      "\\neg {\\rm A\\_Cat}_{ij} \\rightarrow ({\\rm Bob} \\nleftrightarrow \\neg C_{1} \\wedge D_{12})\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\neg {\\rm A\\_Cat}_{ij} \\rightarrow ({\\rm Bob} \\nleftrightarrow \\neg C_{1} \\wedge D_{12})$"
      ],
      "text/plain": [
       "<IPython.core.display.Math object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\\begin{prooftree}\n",
      "\\AxiomC{${\\rm A\\_Cat}_{ij}$}\n",
      "\\UnaryInfC{$\\neg$}\n",
      "\\AxiomC{${\\rm Bob}$}\n",
      "\\AxiomC{$C_{1}$}\n",
      "\\UnaryInfC{$\\neg$}\n",
      "\\AxiomC{$D_{12}$}\n",
      "\\BinaryInfC{$\\wedge$}\n",
      "\\BinaryInfC{$\\nleftrightarrow$}\n",
      "\\BinaryInfC{$\\rightarrow$}\n",
      "\\end{prooftree}\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAZ0AAAEjCAYAAADpH9ynAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjcuMSwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy/bCgiHAAAACXBIWXMAAC4jAAAuIwF4pT92AAAcr0lEQVR4nO3deVTV1f7/8dcBvGJhmiOmYg44UXo1J7KlSGqgeb0FqQVOaZlhZWpa3dtXvaV54d6sFLW6YoMjaZpzLnPKHHLImyXXZcrggEYqSgwh53x+f/jl/C5fUFEO+wg8H2uxxHP2/uz3Weh5sfdnfz7HZlmWJQAADPBwdwEAgIqD0AEAGEPoAACMIXQAAMYQOgAAYwgdAIAxhA4AwBhCBwBgDKEDADCG0AEAGEPoAACMIXQAAMYQOgAAYwgdAIAxhA4AwBhCBwBgDKEDADCG0AEAGEPoAACMIXQAAMYQOgAAYwgdAIAxhA4AwBhCBwBgDKEDADCG0AEAGEPoAACMIXQAAMYQOgAAYwgdAIAxhA4AwBhCBwBgDKEDADCG0AEAGEPoAACMIXQAAMYQOgAAYwgdAIAxhA4AwBhCBwBgDKEDADCG0AEAGEPoAACMIXQAAMYQOgAAYwgdAIAxhA4AwBhCBwBgDKEDADCG0AEAGEPoAACMIXQAAMYQOgAAYwgdAIAxhA4AwBhCBwBgDKEDADCG0AEAGEPoAACMIXQAAMYQOgAAYwgdAIAxhA4AwBhCBwBgDKEDADCG0AEAGEPoAACMIXQAAMYQOgAAYwgdAIAxhA4AwBhCBwBgDKEDADCG0AEAGEPoAACMIXQAAMYQOgAAY7zcXQCAiic3N1fffvutTpw4oV9//VV+fn7q3r277rnnHmebDz74QKNGjXJjlSgNzHQAGHPy5EmNGjVKLVq00JIlS/SHP/xB7dq1U15enp5++mm9+eabkqQZM2YoLi7OzdWiNDDTAVDqLMvS9OnTNW3aNIWHh+vgwYO6++67C7QZPHiwnn/+eYWGhmrjxo2aOHGim6pFabJZlmW5uwgA5VdWVpYiIyO1cuVKxcbG6vnnn79u23vvvVdpaWlav369QkNDDVYKE1heA1Bq7Ha7wsPDtXLlSk2ZMuW6gSNJd9xxh/r06SMvLy899NBDhqqESYQOgFLz6quvasOGDeratasmT55crD7NmzdX+/btVbVq1VKuDu5A6AAoFYcOHdI777wjm82mWbNm3VTfoKCg0ikKbsdGAgCl4pVXXpHD4VBwcLDatWtX7H5//OMf1aBBg1KsDO7ERgIALpecnKx7771XkrRo0SI99dRT7i0Itw2W1wC43PLlyyVJNptNjzzyiJurwe2E0AHgckeOHJEktWjRQjVr1izRsQ4cOKBOnTrp5MmTrigNbsY5HQAud+bMGUlyLrEVV3JysurWrStvb28tX75ca9eulc1m0759+2S320uhUpjGTAeAy911112SpBo1atxUvzFjxij/NHN4eLg+/vhjDR061OX1wX0IHQAu5+/vL0lKT08vdp9///vf8vPzU5UqVUqpKtwOCB0ALjdo0CBJ0sGDB+VwOG7YPi8vT2+88YamTp1a2qXBzQgdAC533333KSwsTGfPntXSpUuv29ayLEVFRemFF15QrVq1DFUIdyF0AJSKf/3rX7rvvvs0ZswY7dq1q8g2Z86cUWRkpJ544gn16tXLcIVwB3avASgV1atX1969ezVhwgT16dNHffv2VUhIiOrUqaPU1FTt2bNHnp6eevfdd1W7dm13lwtDuCMBgFJ36dIlbdmyRUlJSZKubqUODg5WtWrVbth327Zt6tGjhxITE296CzZuP8x0AJS6atWq6bHHHnN3GbgNcE4HwG0tf/dbcXbB4fZH6AC4LW3evFlPPPGE8+LQkJAQDRw4UAcPHnRzZSgJzukAAIxhpgMAMIbQAQAYQ+gAAIxhyzSAEomNjVVsbKxba4iKilJUVJRba0DxsJEAAGAMMx0AMGzIkCE6evSojhw5ot9++02VK1dWhw4d5OV19S3Z4XDowoULys3NVWhoqMaPHy8/Pz83V+0azHQAwE0iIiK0ePFiTZo0STNmzCj0fEJCgkaOHKmEhAStWrVK3bp1c0OVrkXoAICbNG7cWElJSdq8ebMefvjhItv89ttvatu2rS5duqQjR46oTp06hqt0LXavAYAbpKSkKCkpSZUqVVJgYOA12/n4+Ojll1/W+fPnFR0dbbDC0kHoAIAbbN++XZLUsWNH3XHHHddt27VrV0nSsmXLSr2u0kboAIAb5IdOUFDQDdv6+PhIkk6dOqWsrKzSLKvUEToA4Ab5odO9e/cbtr148aLz+4yMjFKryQRCBwAMO3PmjH7++Wd5eXnpwQcfvGH7hIQESZKXl1eZ/5RVQgcADMuf5TzwwAPOpbPr2bdvnySpdevW8vAo22/bZbt6ACiDtm3bJql4S2uS9NVXX0mS+vfvX+DxAwcOqFOnTjp58mShPjk5OZo+fbrGjh2rRx99VA8//LB27dpVssJdgDsSAIBhN3M+58CBA/r5559VqVIlDR8+XJK0fPlyrV27VjabTfv27ZPdbi/U76233tLIkSN17733SpLmzp2rHj16aMeOHercubPrXsxN4uJQAEYsXbpU8+bNu6k+aWlpio+PV0BAQClVZd65c+fk6+srT09PXbhwQXfdddd1248YMUJxcXF67rnnNHfu3ALPbdu2TT169FBiYqIzXCTp8uXL8vX11cSJEzVlyhRJkmVZuueee9SxY0etXr3a1S+r2JjpADBi0KBBGjRo0E31CQoKUlpaWilV5B75s5x27drdMHASEhL0ySefqEmTJnr77beLPYanp6dq165dYHu1zWZTo0aNdOzYsVsr3EUIHQAwqLhLazk5ORo8eLDuvPNOLV++XNWrVy/2GHfeeaeSk5MLPZ6YmKiOHTveVL2uxkYCADCoOKFz8eJFPfroo0pJSdHWrVvVrl27Eo+7ceNGnT9/Xm+88UaJj1UShA4AGJKSkqIjR45Ikh566KFCz1+6dEnz5s1T69atVb16dR06dEjt27cv8bg5OTkaP368pk+f7tZNBBLLawBuYzabTTabzd1llFh4eLiSk5N17Ngx5e/dCg0Nlbe3t6SrJ/lzcnKUm5urBx98UKtXr3bpMlhUVJRGjBihcePGueyYt4rQAXDbiomJUevWrd1dRoktX77cbWNPmzZN3bt315AhQyRJJ06cUJMmTdxWD8trAG5bHTp0uOEdmHFtn376qfz9/Z2BI0lxcXFurIiZDgCUWQ6Ho8Cf/239+vX69NNP1bNnT+enktrtdqWnp5sssRAuDgWAMmbz5s364IMPtGfPHp06dUr+/v5q166dJk2apPbt2+v8+fNq1KiRMjMzC/X9+9//rokTJ7qh6qsIHQCAMZzTAQAYQ+gAAIwhdAAAxhA6AABj2DINoERiY2MVGxvr7jJwDfm33bldlJvda2lpaVq8eLFeeuklo+Omp6dr69atSklJUW5urpo3b65evXo5L2jLzMzUjh07FBoaarQuALgdlZvltQULFmjs2LE6fPiwkfFOnDihQYMGqWnTplqzZo1q1aqltm3b6ty5cxowYIDef/99SdLo0aO1bNkyIzXh9mZZli5dulTgM06AiqbchM6SJUsK/Fmali1bpoCAAP3666/64YcfFBcXp4iICPXu3VvPPvus1q5dq8zMTAUGBuqzzz5z2bj79+/XoUOHXHa8iubo0aPq0qWL6tat67yRZKVKlfTggw8qKChIQUFB6tGjhwIDA9WlSxdFR0frt99+K/G4GzZsUO3atVWpUiVVr15d8fHxLng1QBlllQMJCQmWJEuS1bhx41Ida9GiRZbNZrOCgoKsnJyc67Z98sknLUnW0KFDXTL2lClTrAULFrjkWBWZ3W63QkJCLEnWiBEjimzzxRdfWFWqVLHq169v/fDDDyUeMyMjw/nvgZ8hKrJyMdNZvHixwsLCJF39ZLzdu3eXyjhHjx7VM888oypVqujjjz9W5cqVr9t+5syZN2xzM3bu3OmyY1VkHh4eqlu3riTJx8enyDaPPfaYXn/9dZ0+fVp9+/Yt8ZKYj4+PevXqVaJjAOVBuQidpUuXKiYmRo0bN5Z0NYRKw1//+ldlZWUpLCxMjRo1umH7unXrauDAgS4ZOyEhQV9//bVLjoXieeqppyRJJ0+e1OrVq0t8vPLwuTAVRXZ2thYtWuTuMsqlMh86+/bt0913363GjRtrwIABkqTPP/9cdrvdpeOkpqZqxYoVkqQ//elPxe4XEhJSonHz8vK0Z88ehYWFOT/8CWbcc889zu+L+rx5lF/z58/X4MGDdezYMXeXUu6U+dBZsmSJM2zy/zx37py2bNni0nE2btzofNNv06ZNsft169bNWVe+/fv3a/z48Xr88ccVHBysNm3aaOTIkTpx4kSh/rGxsXr11VedyzszZsxwnvQePnx4CV4RbuS/N22Uhw8SQ/E4HA6999576tGjh9577z13l1P+uPukUknY7Xarfv36VkpKivOxZs2aWZKsYcOGuXSsiRMnOjcrXL58+ZaPc/r0acvb29tq27at9fvvv1uWZVmZmZlWWFiYVbVqVWvPnj1F9ps8eTInoV1o6NChliTrpZdeKvJ5h8Nh9e7d25Jk9ezZ07Lb7YXa7N271woLC7M6duxodevWzerUqZM1ffp0KyMjo8hjLliwwPkzXLlypdWvXz8rODjYatq0qdW/f39r7969rnyJuEVffvml1blzZyslJcWqVq2adeHCBXeXVK6U6ZnO9u3b5efnp4YNGzofyz+HsnLlSv3+++8uG+vixYvO70vySYY5OTmSpLNnz+rKlSvO43300Uf6/fff9eKLL5asUJRYUlKSQkJCtGXLFr3yyitas2aNPDwK/leZNWuWevfurWHDhum7777T9u3btWHDBh0+fFhdunRRSkrKNY8/a9Ys/fjjj4qPj9fXX3+thIQEtWrVSoGBgZo/f35pvzzcwDvvvKNx48apYcOGCg0N1YcffujuksoXd6deSYwcOdKaOXNmgcd++OEH54xkxYoVLhtr0qRJzuNe6zfZ4jp//nyRx/Dz87O8vLyK7HOzM50PP/zQat68+TWff/31162ePXsW61jlUf5Mp379+lb37t2dX4GBgZavr6/l6+trxcTEWOnp6YX6btiwwbLZbNacOXMKPWe3261WrVpZnTp1sq5cuVLgufyZzujRo4usqW/fvpaXl5f1/fffu+Q14uYdPHjQ8vPzs/Ly8izLujqbbdCgQaGfJW5dmZ3p5ObmauXKlXriiScKPH7//ferVatWklx7oWjLli2d3589e7bY/fLy8grd+6hGjRry8vLSqlWr9MILLyg4OFjdunXTuXPnlJeX55J669Wrp2eeeeaazzdt2lSDBw92yVhlWXh4uLZt2+b82rVrl1JTU7V9+3bFx8fLz89PH330UYE+r732mizLUnh4eKHjeXh4qH///vruu+/0xRdfFDlmkyZNinw8MjJSeXl5evvtt0v+wnBLZs6cqRdeeEGenp6SpE6dOsnPz48Lel2ozIbOV199JbvdroiICOeJ9fyv/CWsdevWKSMjwyXjhYSEOLe8/vjjj8Xud+TIEX3wwQcFHvvss8/k5+enyZMnq0uXLvr888+1Y8cO+fr6uqRWSXr00Uc1YcKEaz7/9NNPa8iQIS4br7xp3ry51q9fL09PTz377LOaO3eupKvbpw8dOqTKlSurdu3aRfb18/OTJOdux+Jq1qyZpKt3MIB5qampWrduXaFf1l5++WXNnDnTTVWVP2U2dBYvXqyZM2cW+C01/+ubb76Rh4eHsrOztXLlSpeM5+vr65xV3cw1Gz/++KNz5iVJ77//voYMGaLOnTtr3759ioiIUM2aNW+ppvfff1979+69pb64sVq1aikiIkKSNGnSJGVkZOjUqVOSpD/84Q/X7FepUiVJVwPqZlSvXl2SlJGR4fzFCebMnj1bkZGRqlatWoHHH3vsMf3666/65ptv3FRZ+VImQyczM1NbtmwpcnlDkurXr++8+tuVS2xvvfWW7rzzTsXHxxf7DSU+Pr7AdT3R0dGSpH/84x+F3rhyc3Od32/atEmbNm1y/j3/RLb1X9fqnD9/vtBmiRUrVujNN9/UI488UuiNKzs7W1OnTtXUqVPVv39/50YGXFtAQICkq0Fw9OhR1alTR5KUlZUlh8NRZJ+0tDRJuuZM6FouXbok6eryq7e3962WjFuQnZ2tjz76qMiNPJ6ennrxxReZ7bhImQydL7/8UqGhode8hYkkDRs2TJK0efNm55tASfn7+2v+/PnKysrS008/XSAkirJmzRq1atWqwEWGly9fliTnbVjyHTt2rMC5ojNnzig1NdX59/w7IPz3azl9+nSBY589e1bHjx/Xa6+9pm+++UY//fRTgTH+53/+R6NGjdLkyZO1c+dObh5aDKdPn3Z+36BBAzVp0kTNmjWT3W5XUlJSkX2OHz8u6eYvDM7/efTr1++WasWt+/TTT9W1a1c1bdq0yOdHjBihrVu3FnktHW5OmQud5ORkTZky5YZ3HMg/B5OXl6d58+a5bPyBAwcqPj5e3377rfr166czZ84U2W7jxo1asmSJ3nzzzQKP5y/XTJ061fmb8pkzZzRq1Cj17dtX0tX7xx0/fty5xi9dPUdTq1YtrVq1Sg6HQ+np6Tp16lSBNl9//bUiIyO1Y8cOeXl5Fbig8cKFC2rTpo18fX2VnJysCxcuFOtWPhXZ5cuX9cknn0i6uuHA19dXNptNf/vb3yRdvfPF/2W327VmzRq1aNFCQ4cOLfK4RX2olmVZiouLk4+Pj15//XUXvgrciGVZevfdd/Xyyy9fs81dd92lYcOGcbGoK7h381zxHTt2zGrbtq3l6enp3LrcsGFDa+vWrQXaZWVlWYGBgVatWrWc7SRZzZo1s/r27euyehITE61BgwZZNWvWtEaMGGEtXLjQ+uqrr6wFCxZYERER1rRp05zbLv+b3W63Zs+ebXXo0MFq3ry5FRwcbD3++OPW4cOHrVOnTlkdOnSwAgICCm0FtyzL+v77762goCCrTZs2Vu/eva2ffvqpyNqGDh1qDR8+/Jq1z58/3woICLjl117W2e1265FHHrEkWc8991yRbU6cOGF17drVkmR169at0NbpadOmWVWrVrU2bdrkfOzKlSvWuHHjrCZNmlj/+c9/Ch1zwYIFlre3tzVmzBgrJibG+e8jOzvbevHFF62qVataa9eudeErRXGsW7fOeuCBB27YLjEx0apevXqR2+hRfOXmk0NvxoEDBzRnzpzrzpY8PDw0evRodezY8brHSk9P15YtW5SSkqIrV66oWbNm6tWr13WX/kpTVlaW6tatq9WrV6tHjx5FtomIiFCNGjU0a9Ysw9W519GjRzV06FAlJibql19+kSRVrlxZ7du3L3B+LT09XWfPnlXbtm01ePBgRUREFHmzzt27d+udd95RamqqKleurLy8PAUHB2vs2LGFTkZL0scff6z9+/dr9uzZWrhwoRYuXKisrCxlZGSoc+fOeuWVV665vIPS06tXLw0bNsy5CnE94eHhCgwM1Pjx4w1UVk65O/XcITY21vLw8CgwE/q/Xx4eHtasWbPcXepNW7RokdWwYUPL4XBYH374oXXx4sVCberVq+fSC2eBsurw4cNW/fr1rdzc3GK137lzp9WoUaMiVzFQPGXunI4rPP/887Lb7bIs65pfdrtdY8aMcXepN2337t3q3bu380R3/jbcfEeOHNHZs2fVvXt39xQI3EbWrVun8ePHO7e530jXrl3VuHFjHT16tJQrK78q5PJaefbtt99qxowZCggI0JgxY9SgQYMCz8+aNUvz589n5xoAtyB0KoCsrCznTUr79u2r1q1bKyYmxs1VAaiICJ1yLikpSa1atdLq1atVs2ZNhYSE6MCBAwXuzA0Apni5uwCULh8fH7Vr105bt25VUlKStm3bRuAAcBtmOgAAY5jpFCE2NlaxsbFurSEqKkpRUVFuraGiuB1+3ih/+D9cNGY6AABjKuR1OgAA9yB0AADGEDoAAGMIHQCAMYQOAMAYQgcAYAyhAwAwhtABABhD6AAo0vWuGz937pyys7MlSQ6Hw1RJKAcIHQBFGj16tHbv3l3o8f3796tevXpKTk5WTk6OQkJCdPnyZTdUiLKI0AFQyKuvvipvb28FBgYWem727Nnq2bOnWrZsKW9vbz377LPq37+/MjMz3VApyhpu+AnAyeFwKCoqSr/88os+//zzQs+fP39ey5Yt07Jly5yPhYeH6/Tp0+rZs6fWrVunGjVqmCwZZQw3/CyBpUuXat68eTfVJy0tTfHx8QoICCilqoBbc/r0aUVGRmrbtm366aef1Lp160JtoqOjNXfuXB0/flweHv9/oSQrK0vNmjVT5cqVtWTJEnXp0sVk6ShDCB3DgoKCNGXKFAUFBbm7FMDprbfeUkxMjEvOzXh6emrYsGGKjo5m1oNCWF4DoFatWqlevXrO0KlVq5Zq1qxZoE16errS0tLk7+9fqH9ubq4SExMlXf20Wn9/f91xxx2lXzjKHEIHgMLCwtSnTx9NmDBBc+bM0c6dO9WiRYsCbZ588kllZ2dr1apVhfo7HA75+fmpSZMmWrhwofz8/AxVjrKG0AEgSapSpYpiY2PVunVrDR8+XJs2bZKPj48kKTU1VStWrNCGDRuK7Dt27FgFBwcrLi5OXl68reDa+NdhmM1mk81mc3cZwDVFRUWpatWqGjhwoNauXSubzaZ58+bJ399fDz/8cKH20dHRysvL0yeffMK/bdwQoWNYTExMkbuCgNvJkCFDlJ6erkOHDqlt27Zav369xo0bV6hdZmamTp06pdmzZxM4KBZ2rwEAjOGOBAAAYwgdAIAxhA4AwBhCBwBgDKEDADCG0AEAGMN1OkUYMGCAvvzyS3eXAZQ7/fv3V3x8vLvLgBtxnQ4AwBiW1wAAxhA6AABjCB0AgDGEDgDAGEIHAGAMoQMAMIbQAQAYQ+igXAsPD9cXX3zh7jIA/C9CB+Va165duQIeuI1wRwKUa7/88ovuv/9+fffdd2rUqJG7ywEqPGY6KNfq1Kmjv/zlLxo5cqT4/QpwP2Y6KPccDof69eunmjVrKi4uTl5e3OcWcBdmOij3PDw8tGrVKuXm5io4OFi7du1yd0lAhcVMB7e1f/7zn5owYYJLj2mz2bR06VINGDDApccFcGOEDiqErKwsRUZGKj09XXPmzFHLli3dXRJQIbG4jXLP4XDo8ccfV9OmTbVixQrZbDZ3lwRUWIQOyr3o6Gh5enoqNjbW3aUAFR7LayjXLly4oJYtW+r7779X/fr13V0OUOGxew3l2tKlS9WnTx8CB7hNEDoo17Zv364///nP7i4DwP9ieQ0AYAwzHQCAMYQOAMAYQgcAYAyhAwAwhtABABhD6AAAjCF0AADGEDoAAGMIHQCAMYQOAMAYQgcAYAyhAwAwhtABABhD6AAAjCF0AADGEDoAAGMIHQCAMYQOAMAYQgcAYAyhAwAwhtABABhD6AAAjCF0AADGEDoAAGMIHQCAMYQOAMAYQgcAYAyhAwAwhtABABhD6AAAjCF0AADGEDoAAGMIHQCAMYQOAMAYQgcAYAyhAwAwhtABABhD6AAAjCF0AADGEDoAAGMIHQCAMYQOAMAYQgcAYAyhAwAwhtABABhD6AAAjCF0AADGEDoAAGMIHQCAMYQOAMAYQgcAYAyhAwAwhtABABhD6AAAjCF0AADGEDoAAGMIHQCAMYQOAMAYQgcAYAyhAwAwhtABABhD6AAAjCF0AADGEDoAAGMIHQCAMYQOAMAYQgcAYAyhAwAwhtABABhD6AAAjCF0AADGEDoAAGMIHQCAMYQOAMAYQgcAYAyhAwAwhtABABhD6AAAjCF0AADGEDoAAGMIHQCAMf8PCXYpKWWd7scAAAAASUVORK5CYII=",
      "text/plain": [
       "<Figure size 450x300 with 1 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "input_formula = \"not A_Cat_ij imp Bob xor not C_1 and D_12\"\n",
    "testParser(input_formula)\n",
    "testParser(input_formula, 'RPN')\n",
    "testParser(input_formula, 'infix_latex')\n",
    "testParser(input_formula, 'tree')\n",
    "testParser(input_formula, 'bussproof')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{\\rm Cats\\_and\\_Dogs}_{12}\n",
      "{\\rm Cats\\_and\\_Dogs}\n",
      "{\\rm Cats\\_and}_{Dogs}\n",
      "{\\rm Cats}\n"
     ]
    }
   ],
   "source": [
    "instr_li = [\"Cats_and_Dogs_12\", \"Cats_and_Dogs_\", \"Cats_and_Dogs\", \"Cats\"]\n",
    "for instr in instr_li:\n",
    "  print(identifier_to_latex(instr))"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "mlenv",
   "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.11.2"
  },
  "orig_nbformat": 4
 },
 "nbformat": 4,
 "nbformat_minor": 2
}