diff --git a/info4/kapitel-0/Logik.ipynb b/info4/kapitel-0/Logik.ipynb
index 8921439a3af9ebcf7a3ec184a4fa4d0c17b6870d..7ac1ca5af7d43b983235bd1c4788fc28aba3b593 100644
--- a/info4/kapitel-0/Logik.ipynb
+++ b/info4/kapitel-0/Logik.ipynb
@@ -144,27 +144,69 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 1,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 1,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     "2>1"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 2,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 2,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     "1+1 = 2"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 3,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{FALSE}$"
+      ],
+      "text/plain": [
+       "FALSE"
+      ]
+     },
+     "execution_count": 3,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     "2<1"
    ]
@@ -183,18 +225,46 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 4,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 4,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     "¬(2<1)"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 5,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{FALSE}$"
+      ],
+      "text/plain": [
+       "FALSE"
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     "¬(1+1=2)"
    ]
@@ -215,18 +285,46 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 6,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 6,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     "2>1 ∧ 1>0"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 7,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{FALSE}$"
+      ],
+      "text/plain": [
+       "FALSE"
+      ]
+     },
+     "execution_count": 7,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     "2>1 ∧ 1>2"
    ]
@@ -240,18 +338,46 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 8,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{FALSE}$"
+      ],
+      "text/plain": [
+       "FALSE"
+      ]
+     },
+     "execution_count": 8,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     "1>1 ∨ 1>2"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 9,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 9,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     "2>1 ∨ 3>1"
    ]
@@ -265,27 +391,69 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 10,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 10,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     "2>1 ⇒ 3>1"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 11,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 11,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     "2<1 ⇒ 1+1 = 5"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 12,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{FALSE}$"
+      ],
+      "text/plain": [
+       "FALSE"
+      ]
+     },
+     "execution_count": 12,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     "2>1 ⇒ 1+1=5"
    ]
@@ -299,27 +467,69 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 13,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 13,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     "1=2 ⇔ 2=1"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 14,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 14,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     "1=3 ⇔ 1=1024"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 15,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{FALSE}$"
+      ],
+      "text/plain": [
+       "FALSE"
+      ]
+     },
+     "execution_count": 15,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     "1=1 ⇔ 2=3"
    ]
@@ -339,18 +549,204 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 16,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Preference changed: OPTIMIZE_AST = FALSE\n"
+      ]
+     },
+     "execution_count": 16,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     ":pref OPTIMIZE_AST=FALSE"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 17,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "image/svg+xml": [
+       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
+       " -->\n",
+       "<!-- Title: g Pages: 1 -->\n",
+       "<svg width=\"373pt\" height=\"320pt\"\n",
+       " viewBox=\"0.00 0.00 373.00 320.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 316)\">\n",
+       "<title>g</title>\n",
+       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-316 369,-316 369,4 -4,4\"/>\n",
+       "<!-- Noderoot -->\n",
+       "<g id=\"node1\" class=\"node\">\n",
+       "<title>Noderoot</title>\n",
+       "<path fill=\"#b3ee3a\" stroke=\"#000000\" d=\"M42,-133.5C42,-133.5 12,-133.5 12,-133.5 6,-133.5 0,-127.5 0,-121.5 0,-121.5 0,-107.5 0,-107.5 0,-101.5 6,-95.5 12,-95.5 12,-95.5 42,-95.5 42,-95.5 48,-95.5 54,-101.5 54,-107.5 54,-107.5 54,-121.5 54,-121.5 54,-127.5 48,-133.5 42,-133.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"27\" y=\"-118.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">⇔</text>\n",
+       "<text text-anchor=\"middle\" x=\"27\" y=\"-103.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">true</text>\n",
+       "</g>\n",
+       "<!-- Node1 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>Node1</title>\n",
+       "<path fill=\"#b3ee3a\" stroke=\"#000000\" d=\"M173,-188C173,-188 102,-188 102,-188 96,-188 90,-182 90,-176 90,-176 90,-147 90,-147 90,-141 96,-135 102,-135 102,-135 173,-135 173,-135 179,-135 185,-141 185,-147 185,-147 185,-176 185,-176 185,-182 179,-188 173,-188\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137.5\" y=\"-172.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">⇒</text>\n",
+       "<text text-anchor=\"middle\" x=\"137.5\" y=\"-157.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">true</text>\n",
+       "<text text-anchor=\"middle\" x=\"137.5\" y=\"-142.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2 &gt; 3 ⇒ 4 &gt; 1</text>\n",
+       "</g>\n",
+       "<!-- Node1&#45;&gt;Noderoot -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>Node1&#45;&gt;Noderoot</title>\n",
+       "<path fill=\"none\" stroke=\"#000000\" d=\"M89.9968,-141.295C81.0718,-137.4988 71.8716,-133.5857 63.3529,-129.9623\"/>\n",
+       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"64.6477,-126.7096 54.0755,-126.0163 61.9078,-133.1512 64.6477,-126.7096\"/>\n",
+       "</g>\n",
+       "<!-- Node2 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>Node2</title>\n",
+       "<path fill=\"#ff6347\" stroke=\"#000000\" d=\"M263,-265C263,-265 233,-265 233,-265 227,-265 221,-259 221,-253 221,-253 221,-224 221,-224 221,-218 227,-212 233,-212 233,-212 263,-212 263,-212 269,-212 275,-218 275,-224 275,-224 275,-253 275,-253 275,-259 269,-265 263,-265\"/>\n",
+       "<text text-anchor=\"middle\" x=\"248\" y=\"-249.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">&gt;</text>\n",
+       "<text text-anchor=\"middle\" x=\"248\" y=\"-234.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">false</text>\n",
+       "<text text-anchor=\"middle\" x=\"248\" y=\"-219.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2 &gt; 3</text>\n",
+       "</g>\n",
+       "<!-- Node2&#45;&gt;Node1 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>Node2&#45;&gt;Node1</title>\n",
+       "<path fill=\"none\" stroke=\"#000000\" d=\"M220.9687,-219.6637C209.963,-211.9946 196.9154,-202.9026 184.4453,-194.213\"/>\n",
+       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"186.1423,-191.1296 175.9367,-188.2839 182.1402,-196.8727 186.1423,-191.1296\"/>\n",
+       "</g>\n",
+       "<!-- Node3 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>Node3</title>\n",
+       "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"311,-275.5 311,-311.5 365,-311.5 365,-275.5 311,-275.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"338\" y=\"-289.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
+       "</g>\n",
+       "<!-- Node3&#45;&gt;Node2 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>Node3&#45;&gt;Node2</title>\n",
+       "<path fill=\"none\" stroke=\"#000000\" d=\"M310.997,-276.9982C302.5314,-271.8248 293.0484,-266.0296 284.0611,-260.5373\"/>\n",
+       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"285.6529,-257.4083 275.295,-255.1803 282.0027,-263.3813 285.6529,-257.4083\"/>\n",
+       "</g>\n",
+       "<!-- Node4 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>Node4</title>\n",
+       "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"311,-220.5 311,-256.5 365,-256.5 365,-220.5 311,-220.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"338\" y=\"-234.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
+       "</g>\n",
+       "<!-- Node4&#45;&gt;Node2 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>Node4&#45;&gt;Node2</title>\n",
+       "<path fill=\"none\" stroke=\"#000000\" d=\"M310.997,-238.5C302.9723,-238.5 294.0335,-238.5 285.4691,-238.5\"/>\n",
+       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"285.295,-235.0001 275.295,-238.5 285.2949,-242.0001 285.295,-235.0001\"/>\n",
+       "</g>\n",
+       "<!-- Node5 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>Node5</title>\n",
+       "<path fill=\"#b3ee3a\" stroke=\"#000000\" d=\"M263,-188C263,-188 233,-188 233,-188 227,-188 221,-182 221,-176 221,-176 221,-147 221,-147 221,-141 227,-135 233,-135 233,-135 263,-135 263,-135 269,-135 275,-141 275,-147 275,-147 275,-176 275,-176 275,-182 269,-188 263,-188\"/>\n",
+       "<text text-anchor=\"middle\" x=\"248\" y=\"-172.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">&gt;</text>\n",
+       "<text text-anchor=\"middle\" x=\"248\" y=\"-157.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">true</text>\n",
+       "<text text-anchor=\"middle\" x=\"248\" y=\"-142.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">4 &gt; 1</text>\n",
+       "</g>\n",
+       "<!-- Node5&#45;&gt;Node1 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>Node5&#45;&gt;Node1</title>\n",
+       "<path fill=\"none\" stroke=\"#000000\" d=\"M220.9687,-161.5C213.1697,-161.5 204.3453,-161.5 195.4276,-161.5\"/>\n",
+       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"195.3694,-158.0001 185.3694,-161.5 195.3694,-165.0001 195.3694,-158.0001\"/>\n",
+       "</g>\n",
+       "<!-- Node6 -->\n",
+       "<g id=\"node7\" class=\"node\">\n",
+       "<title>Node6</title>\n",
+       "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"311,-165.5 311,-201.5 365,-201.5 365,-165.5 311,-165.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"338\" y=\"-179.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">4</text>\n",
+       "</g>\n",
+       "<!-- Node6&#45;&gt;Node5 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>Node6&#45;&gt;Node5</title>\n",
+       "<path fill=\"none\" stroke=\"#000000\" d=\"M310.997,-176.8993C302.8842,-174.9161 293.8369,-172.7046 285.1869,-170.5901\"/>\n",
+       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"285.8401,-167.1468 275.295,-168.1721 284.1779,-173.9466 285.8401,-167.1468\"/>\n",
+       "</g>\n",
+       "<!-- Node7 -->\n",
+       "<g id=\"node8\" class=\"node\">\n",
+       "<title>Node7</title>\n",
+       "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"311,-110.5 311,-146.5 365,-146.5 365,-110.5 311,-110.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"338\" y=\"-124.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+       "</g>\n",
+       "<!-- Node7&#45;&gt;Node5 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>Node7&#45;&gt;Node5</title>\n",
+       "<path fill=\"none\" stroke=\"#000000\" d=\"M310.997,-138.4011C302.796,-141.4081 293.6401,-144.7653 284.905,-147.9682\"/>\n",
+       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"283.4788,-144.7632 275.295,-151.4918 285.8887,-151.3353 283.4788,-144.7632\"/>\n",
+       "</g>\n",
+       "<!-- Node8 -->\n",
+       "<g id=\"node9\" class=\"node\">\n",
+       "<title>Node8</title>\n",
+       "<path fill=\"#b3ee3a\" stroke=\"#000000\" d=\"M157,-106C157,-106 118,-106 118,-106 112,-106 106,-100 106,-94 106,-94 106,-65 106,-65 106,-59 112,-53 118,-53 118,-53 157,-53 157,-53 163,-53 169,-59 169,-65 169,-65 169,-94 169,-94 169,-100 163,-106 157,-106\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137.5\" y=\"-90.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">¬</text>\n",
+       "<text text-anchor=\"middle\" x=\"137.5\" y=\"-75.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">true</text>\n",
+       "<text text-anchor=\"middle\" x=\"137.5\" y=\"-60.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">¬(5 &lt; 1)</text>\n",
+       "</g>\n",
+       "<!-- Node8&#45;&gt;Noderoot -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>Node8&#45;&gt;Noderoot</title>\n",
+       "<path fill=\"none\" stroke=\"#000000\" d=\"M105.8351,-89.5296C92.6976,-93.6908 77.3698,-98.5458 63.7409,-102.8626\"/>\n",
+       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.6492,-99.5369 54.1729,-105.8932 64.763,-106.2102 62.6492,-99.5369\"/>\n",
+       "</g>\n",
+       "<!-- Node9 -->\n",
+       "<g id=\"node10\" class=\"node\">\n",
+       "<title>Node9</title>\n",
+       "<path fill=\"#ff6347\" stroke=\"#000000\" d=\"M263,-100C263,-100 233,-100 233,-100 227,-100 221,-94 221,-88 221,-88 221,-59 221,-59 221,-53 227,-47 233,-47 233,-47 263,-47 263,-47 269,-47 275,-53 275,-59 275,-59 275,-88 275,-88 275,-94 269,-100 263,-100\"/>\n",
+       "<text text-anchor=\"middle\" x=\"248\" y=\"-84.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">&lt;</text>\n",
+       "<text text-anchor=\"middle\" x=\"248\" y=\"-69.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">false</text>\n",
+       "<text text-anchor=\"middle\" x=\"248\" y=\"-54.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">5 &lt; 1</text>\n",
+       "</g>\n",
+       "<!-- Node9&#45;&gt;Node8 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>Node9&#45;&gt;Node8</title>\n",
+       "<path fill=\"none\" stroke=\"#000000\" d=\"M220.9687,-74.9678C208.5454,-75.6423 193.5202,-76.4582 179.6609,-77.2107\"/>\n",
+       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"179.1478,-73.7333 169.3523,-77.7705 179.5274,-80.723 179.1478,-73.7333\"/>\n",
+       "</g>\n",
+       "<!-- Node10 -->\n",
+       "<g id=\"node11\" class=\"node\">\n",
+       "<title>Node10</title>\n",
+       "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"311,-55.5 311,-91.5 365,-91.5 365,-55.5 311,-55.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"338\" y=\"-69.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">5</text>\n",
+       "</g>\n",
+       "<!-- Node10&#45;&gt;Node9 -->\n",
+       "<g id=\"edge10\" class=\"edge\">\n",
+       "<title>Node10&#45;&gt;Node9</title>\n",
+       "<path fill=\"none\" stroke=\"#000000\" d=\"M310.997,-73.5C302.9723,-73.5 294.0335,-73.5 285.4691,-73.5\"/>\n",
+       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"285.295,-70.0001 275.295,-73.5 285.2949,-77.0001 285.295,-70.0001\"/>\n",
+       "</g>\n",
+       "<!-- Node11 -->\n",
+       "<g id=\"node12\" class=\"node\">\n",
+       "<title>Node11</title>\n",
+       "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"311,-.5 311,-36.5 365,-36.5 365,-.5 311,-.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"338\" y=\"-14.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+       "</g>\n",
+       "<!-- Node11&#45;&gt;Node9 -->\n",
+       "<g id=\"edge11\" class=\"edge\">\n",
+       "<title>Node11&#45;&gt;Node9</title>\n",
+       "<path fill=\"none\" stroke=\"#000000\" d=\"M310.997,-35.0018C302.5314,-40.1752 293.0484,-45.9704 284.0611,-51.4627\"/>\n",
+       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"282.0027,-48.6187 275.295,-56.8197 285.6529,-54.5917 282.0027,-48.6187\"/>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>"
+      ],
+      "text/plain": [
+       "<Dot visualization: formula_tree [(2>3 => 4>1) <=> not(5<1)]>"
+      ]
+     },
+     "execution_count": 17,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     ":dot formula_tree (2>3 ⇒ 4>1) ⇔ ¬(5<1)"
    ]
@@ -433,9 +829,32 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 18,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "|p|q|F1|F2|\n",
+       "|---|---|---|---|\n",
+       "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n",
+       "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
+       "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
+       "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n"
+      ],
+      "text/plain": [
+       "p\tq\tF1\tF2\n",
+       "FALSE\tFALSE\tFALSE\tFALSE\n",
+       "FALSE\tTRUE\tTRUE\tTRUE\n",
+       "TRUE\tFALSE\tTRUE\tTRUE\n",
+       "TRUE\tTRUE\tTRUE\tTRUE\n"
+      ]
+     },
+     "execution_count": 18,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     ":table {p,q,F1,F2| p:BOOL & q:BOOL & \n",
     "                   F1=bool(p=TRUE ∨ (¬(p=TRUE) ∧ q=TRUE)) & // p ∨ (¬p ∧ q)\n",
@@ -478,9 +897,32 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 19,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "|p|q|ODER|NODER|NUND|np|nq|\n",
+       "|---|---|---|---|---|---|---|\n",
+       "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
+       "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|\n",
+       "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|\n",
+       "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n"
+      ],
+      "text/plain": [
+       "p\tq\tODER\tNODER\tNUND\tnp\tnq\n",
+       "FALSE\tFALSE\tFALSE\tTRUE\tTRUE\tTRUE\tTRUE\n",
+       "FALSE\tTRUE\tTRUE\tFALSE\tFALSE\tTRUE\tFALSE\n",
+       "TRUE\tFALSE\tTRUE\tFALSE\tFALSE\tFALSE\tTRUE\n",
+       "TRUE\tTRUE\tTRUE\tFALSE\tFALSE\tFALSE\tFALSE\n"
+      ]
+     },
+     "execution_count": 19,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     ":table {p,q,ODER,NODER,NUND,np,nq| p:BOOL & q:BOOL & np = bool(¬(p=TRUE)) & nq = bool(¬(q=TRUE)) &\n",
     "                            ODER=bool(p=TRUE ∨ q=TRUE) &\n",
@@ -502,9 +944,32 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 20,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "|p|q|IMPL|KONT|np|nq|\n",
+       "|---|---|---|---|---|---|\n",
+       "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
+       "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|\n",
+       "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|\n",
+       "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n"
+      ],
+      "text/plain": [
+       "p\tq\tIMPL\tKONT\tnp\tnq\n",
+       "FALSE\tFALSE\tTRUE\tTRUE\tTRUE\tTRUE\n",
+       "FALSE\tTRUE\tTRUE\tTRUE\tTRUE\tFALSE\n",
+       "TRUE\tFALSE\tFALSE\tFALSE\tFALSE\tTRUE\n",
+       "TRUE\tTRUE\tTRUE\tTRUE\tFALSE\tFALSE\n"
+      ]
+     },
+     "execution_count": 20,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     ":table {p,q,IMPL,KONT,np,nq| p:BOOL & q:BOOL & np = bool(¬(p=TRUE)) & nq = bool(¬(q=TRUE)) &\n",
     "                            IMPL=bool(p=TRUE => q=TRUE) &\n",
@@ -534,9 +999,32 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 21,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "|p|q|F1|F2|\n",
+       "|---|---|---|---|\n",
+       "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
+       "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|\n",
+       "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n",
+       "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n"
+      ],
+      "text/plain": [
+       "p\tq\tF1\tF2\n",
+       "FALSE\tFALSE\tTRUE\tTRUE\n",
+       "FALSE\tTRUE\tFALSE\tTRUE\n",
+       "TRUE\tFALSE\tFALSE\tFALSE\n",
+       "TRUE\tTRUE\tTRUE\tTRUE\n"
+      ]
+     },
+     "execution_count": 21,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     ":table {p,q,F1,F2| p:BOOL & q:BOOL & F1=bool(p=TRUE ⇔ q=TRUE) & F2=bool(p=TRUE ⇒ q=TRUE)}"
    ]
@@ -604,9 +1092,32 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 22,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "|x|y|S1|S2|Puzzle|\n",
+       "|---|---|---|---|---|\n",
+       "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
+       "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|\n",
+       "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n",
+       "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n"
+      ],
+      "text/plain": [
+       "x\ty\tS1\tS2\tPuzzle\n",
+       "FALSE\tFALSE\tTRUE\tTRUE\tTRUE\n",
+       "FALSE\tTRUE\tFALSE\tTRUE\tFALSE\n",
+       "TRUE\tFALSE\tFALSE\tFALSE\tFALSE\n",
+       "TRUE\tTRUE\tTRUE\tFALSE\tFALSE\n"
+      ]
+     },
+     "execution_count": 22,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     ":table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL & \n",
     "                   S1=bool(x=TRUE ⇔ y=TRUE) &\n",
@@ -631,9 +1142,32 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 23,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "|x|y|S1|S2|Puzzle|\n",
+       "|---|---|---|---|---|\n",
+       "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
+       "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
+       "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|\n",
+       "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n"
+      ],
+      "text/plain": [
+       "x\ty\tS1\tS2\tPuzzle\n",
+       "FALSE\tFALSE\tTRUE\tTRUE\tTRUE\n",
+       "FALSE\tTRUE\tTRUE\tTRUE\tTRUE\n",
+       "TRUE\tFALSE\tFALSE\tTRUE\tFALSE\n",
+       "TRUE\tTRUE\tTRUE\tFALSE\tFALSE\n"
+      ]
+     },
+     "execution_count": 23,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     ":table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL & \n",
     "                   S1=bool(x=TRUE ⇒ y=TRUE) &\n",
@@ -681,9 +1215,32 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 24,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "|x|y|S1|S2|Puzzle|WS|\n",
+       "|---|---|---|---|---|---|\n",
+       "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|\n",
+       "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n",
+       "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n",
+       "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n"
+      ],
+      "text/plain": [
+       "x\ty\tS1\tS2\tPuzzle\tWS\n",
+       "FALSE\tFALSE\tTRUE\tTRUE\tTRUE\tFALSE\n",
+       "FALSE\tTRUE\tFALSE\tTRUE\tFALSE\tFALSE\n",
+       "TRUE\tFALSE\tFALSE\tFALSE\tFALSE\tFALSE\n",
+       "TRUE\tTRUE\tTRUE\tFALSE\tFALSE\tFALSE\n"
+      ]
+     },
+     "execution_count": 24,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     ":table {x,y,S1,S2,Puzzle,WS | x:BOOL & y:BOOL & \n",
     "                   S1=bool(x=TRUE ⇔ y=TRUE) &\n",
@@ -817,7 +1374,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 1,
+   "execution_count": 25,
    "metadata": {},
    "outputs": [
     {
@@ -842,7 +1399,7 @@
        "2\t3\tTRUE\n"
       ]
      },
-     "execution_count": 1,
+     "execution_count": 25,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -890,19 +1447,25 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 2,
+   "execution_count": 26,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/markdown": [
-       "$\\mathit{TRUE}$"
+       "$\\mathit{TRUE}$\n",
+       "\n",
+       "**Solution:**\n",
+       "* $\\mathit{x} = 0$"
       ],
       "text/plain": [
-       "TRUE"
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tx = 0"
       ]
      },
-     "execution_count": 2,
+     "execution_count": 26,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -920,7 +1483,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 3,
+   "execution_count": 27,
    "metadata": {},
    "outputs": [
     {
@@ -938,7 +1501,7 @@
        "\tx = 0"
       ]
      },
-     "execution_count": 3,
+     "execution_count": 27,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -949,7 +1512,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 4,
+   "execution_count": 28,
    "metadata": {},
    "outputs": [
     {
@@ -967,7 +1530,7 @@
        "\tx = 10"
       ]
      },
-     "execution_count": 4,
+     "execution_count": 28,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -978,7 +1541,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 7,
+   "execution_count": 29,
    "metadata": {},
    "outputs": [
     {
@@ -996,7 +1559,7 @@
        "\tx = −100"
       ]
      },
-     "execution_count": 7,
+     "execution_count": 29,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1160,7 +1723,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 2,
+   "execution_count": 30,
    "metadata": {},
    "outputs": [
     {
@@ -1181,7 +1744,7 @@
        "TRUE\tTRUE\tTRUE\tTRUE\tTRUE\n"
       ]
      },
-     "execution_count": 2,
+     "execution_count": 30,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1203,7 +1766,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 4,
+   "execution_count": 31,
    "metadata": {},
    "outputs": [
     {
@@ -1224,7 +1787,7 @@
        "TRUE\tTRUE\tTRUE\tTRUE\tTRUE\n"
       ]
      },
-     "execution_count": 4,
+     "execution_count": 31,
      "metadata": {},
      "output_type": "execute_result"
     }