diff --git a/info4/kapitel-0/Logik.ipynb b/info4/kapitel-0/Logik.ipynb
index 9c5c870d67d5ef99122c151f240a9c2b8a19f7ce..8921439a3af9ebcf7a3ec184a4fa4d0c17b6870d 100644
--- a/info4/kapitel-0/Logik.ipynb
+++ b/info4/kapitel-0/Logik.ipynb
@@ -144,69 +144,27 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 1,
+   "execution_count": null,
    "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/markdown": [
-       "$\\mathit{TRUE}$"
-      ],
-      "text/plain": [
-       "TRUE"
-      ]
-     },
-     "execution_count": 1,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     "2>1"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 2,
+   "execution_count": null,
    "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/markdown": [
-       "$\\mathit{TRUE}$"
-      ],
-      "text/plain": [
-       "TRUE"
-      ]
-     },
-     "execution_count": 2,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     "1+1 = 2"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 3,
+   "execution_count": null,
    "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/markdown": [
-       "$\\mathit{FALSE}$"
-      ],
-      "text/plain": [
-       "FALSE"
-      ]
-     },
-     "execution_count": 3,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     "2<1"
    ]
@@ -225,46 +183,18 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 4,
+   "execution_count": null,
    "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/markdown": [
-       "$\\mathit{TRUE}$"
-      ],
-      "text/plain": [
-       "TRUE"
-      ]
-     },
-     "execution_count": 4,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     "¬(2<1)"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 6,
+   "execution_count": null,
    "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/markdown": [
-       "$\\mathit{FALSE}$"
-      ],
-      "text/plain": [
-       "FALSE"
-      ]
-     },
-     "execution_count": 6,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     "¬(1+1=2)"
    ]
@@ -285,46 +215,18 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 7,
+   "execution_count": null,
    "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/markdown": [
-       "$\\mathit{TRUE}$"
-      ],
-      "text/plain": [
-       "TRUE"
-      ]
-     },
-     "execution_count": 7,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     "2>1 ∧ 1>0"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 8,
+   "execution_count": null,
    "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/markdown": [
-       "$\\mathit{FALSE}$"
-      ],
-      "text/plain": [
-       "FALSE"
-      ]
-     },
-     "execution_count": 8,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     "2>1 ∧ 1>2"
    ]
@@ -338,46 +240,18 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 11,
+   "execution_count": null,
    "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/markdown": [
-       "$\\mathit{FALSE}$"
-      ],
-      "text/plain": [
-       "FALSE"
-      ]
-     },
-     "execution_count": 11,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     "1>1 ∨ 1>2"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 10,
+   "execution_count": null,
    "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/markdown": [
-       "$\\mathit{TRUE}$"
-      ],
-      "text/plain": [
-       "TRUE"
-      ]
-     },
-     "execution_count": 10,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     "2>1 ∨ 3>1"
    ]
@@ -391,69 +265,27 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 12,
+   "execution_count": null,
    "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/markdown": [
-       "$\\mathit{TRUE}$"
-      ],
-      "text/plain": [
-       "TRUE"
-      ]
-     },
-     "execution_count": 12,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     "2>1 ⇒ 3>1"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 13,
+   "execution_count": null,
    "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/markdown": [
-       "$\\mathit{TRUE}$"
-      ],
-      "text/plain": [
-       "TRUE"
-      ]
-     },
-     "execution_count": 13,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     "2<1 ⇒ 1+1 = 5"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 14,
+   "execution_count": null,
    "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/markdown": [
-       "$\\mathit{FALSE}$"
-      ],
-      "text/plain": [
-       "FALSE"
-      ]
-     },
-     "execution_count": 14,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     "2>1 ⇒ 1+1=5"
    ]
@@ -467,69 +299,27 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 15,
+   "execution_count": null,
    "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/markdown": [
-       "$\\mathit{TRUE}$"
-      ],
-      "text/plain": [
-       "TRUE"
-      ]
-     },
-     "execution_count": 15,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     "1=2 ⇔ 2=1"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 16,
+   "execution_count": null,
    "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/markdown": [
-       "$\\mathit{TRUE}$"
-      ],
-      "text/plain": [
-       "TRUE"
-      ]
-     },
-     "execution_count": 16,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     "1=3 ⇔ 1=1024"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 17,
+   "execution_count": null,
    "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/markdown": [
-       "$\\mathit{FALSE}$"
-      ],
-      "text/plain": [
-       "FALSE"
-      ]
-     },
-     "execution_count": 17,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     "1=1 ⇔ 2=3"
    ]
@@ -549,253 +339,18 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 18,
+   "execution_count": null,
    "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "Preference changed: OPTIMIZE_AST = FALSE\n"
-      ]
-     },
-     "execution_count": 18,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     ":pref OPTIMIZE_AST=FALSE"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 19,
+   "execution_count": null,
    "metadata": {},
-   "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.28.0 (20110509.1545)\n",
-       " -->\n",
-       "<!-- Title: g Pages: 1 -->\n",
-       "<svg width=\"370pt\" height=\"319pt\"\n",
-       " viewBox=\"0.00 0.00 370.00 319.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-       "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 315)\">\n",
-       "<title>g</title>\n",
-       "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-315 367,-315 367,5 -4,5\"/>\n",
-       "<!-- Noderoot -->\n",
-       "<g id=\"node1\" class=\"node\"><title>Noderoot</title>\n",
-       "<polygon fill=\"#b3ee3a\" stroke=\"#b3ee3a\" points=\"42,-137.602 12,-137.602 0,-125.602 0,-108.398 12,-96.3981 42,-96.3981 54,-108.398 54,-125.602 42,-137.602\"/>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M12,-137.602C6,-137.602 0,-131.602 0,-125.602\"/>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M0,-108.398C0,-102.398 6,-96.3981 12,-96.3981\"/>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M42,-96.3981C48,-96.3981 54,-102.398 54,-108.398\"/>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M54,-125.602C54,-131.602 48,-137.602 42,-137.602\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"42,-137.602 12,-137.602 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M12,-137.602C6,-137.602 0,-131.602 0,-125.602\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"0,-125.602 0,-108.398 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M0,-108.398C0,-102.398 6,-96.3981 12,-96.3981\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"12,-96.3981 42,-96.3981 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M42,-96.3981C48,-96.3981 54,-102.398 54,-108.398\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"54,-108.398 54,-125.602 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M54,-125.602C54,-131.602 48,-137.602 42,-137.602\"/>\n",
-       "<text text-anchor=\"middle\" x=\"27\" y=\"-121.2\" font-family=\"Times,serif\" font-size=\"14.00\">⇔</text>\n",
-       "<text text-anchor=\"middle\" x=\"27\" y=\"-104.4\" font-family=\"Times,serif\" font-size=\"14.00\">true</text>\n",
-       "</g>\n",
-       "<!-- Node1 -->\n",
-       "<g id=\"node2\" class=\"node\"><title>Node1</title>\n",
-       "<polygon fill=\"#b3ee3a\" stroke=\"#b3ee3a\" points=\"169.79,-187.401 102.21,-187.401 90.2103,-175.401 90.2103,-140.599 102.21,-128.599 169.79,-128.599 181.79,-140.599 181.79,-175.401 169.79,-187.401\"/>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M102.21,-187.401C96.2103,-187.401 90.2103,-181.401 90.2103,-175.401\"/>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M90.2103,-140.599C90.2103,-134.599 96.2103,-128.599 102.21,-128.599\"/>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M169.79,-128.599C175.79,-128.599 181.79,-134.599 181.79,-140.599\"/>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M181.79,-175.401C181.79,-181.401 175.79,-187.401 169.79,-187.401\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"169.79,-187.401 102.21,-187.401 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M102.21,-187.401C96.2103,-187.401 90.2103,-181.401 90.2103,-175.401\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"90.2103,-175.401 90.2103,-140.599 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M90.2103,-140.599C90.2103,-134.599 96.2103,-128.599 102.21,-128.599\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"102.21,-128.599 169.79,-128.599 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M169.79,-128.599C175.79,-128.599 181.79,-134.599 181.79,-140.599\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"181.79,-140.599 181.79,-175.401 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M181.79,-175.401C181.79,-181.401 175.79,-187.401 169.79,-187.401\"/>\n",
-       "<text text-anchor=\"middle\" x=\"136\" y=\"-170.6\" font-family=\"Times,serif\" font-size=\"14.00\">⇒</text>\n",
-       "<text text-anchor=\"middle\" x=\"136\" y=\"-153.8\" font-family=\"Times,serif\" font-size=\"14.00\">true</text>\n",
-       "<text text-anchor=\"middle\" x=\"136\" y=\"-137\" font-family=\"Times,serif\" font-size=\"14.00\">2 &gt; 3 ⇒ 4 &gt; 1</text>\n",
-       "</g>\n",
-       "<!-- Node1&#45;&gt;Noderoot -->\n",
-       "<g id=\"edge2\" class=\"edge\"><title>Node1&#45;&gt;Noderoot</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M90.2423,-140.85C81.4339,-137.475 72.3006,-133.975 63.8324,-130.73\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"64.8468,-127.371 54.2565,-127.061 62.3421,-133.907 64.8468,-127.371\"/>\n",
-       "</g>\n",
-       "<!-- Node2 -->\n",
-       "<g id=\"node4\" class=\"node\"><title>Node2</title>\n",
-       "<polygon fill=\"tomato\" stroke=\"tomato\" points=\"260,-267.401 230,-267.401 218,-255.401 218,-220.599 230,-208.599 260,-208.599 272,-220.599 272,-255.401 260,-267.401\"/>\n",
-       "<path fill=\"tomato\" stroke=\"tomato\" d=\"M230,-267.401C224,-267.401 218,-261.401 218,-255.401\"/>\n",
-       "<path fill=\"tomato\" stroke=\"tomato\" d=\"M218,-220.599C218,-214.599 224,-208.599 230,-208.599\"/>\n",
-       "<path fill=\"tomato\" stroke=\"tomato\" d=\"M260,-208.599C266,-208.599 272,-214.599 272,-220.599\"/>\n",
-       "<path fill=\"tomato\" stroke=\"tomato\" d=\"M272,-255.401C272,-261.401 266,-267.401 260,-267.401\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"260,-267.401 230,-267.401 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M230,-267.401C224,-267.401 218,-261.401 218,-255.401\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"218,-255.401 218,-220.599 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M218,-220.599C218,-214.599 224,-208.599 230,-208.599\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"230,-208.599 260,-208.599 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M260,-208.599C266,-208.599 272,-214.599 272,-220.599\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"272,-220.599 272,-255.401 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M272,-255.401C272,-261.401 266,-267.401 260,-267.401\"/>\n",
-       "<text text-anchor=\"middle\" x=\"245\" y=\"-250.6\" font-family=\"Times,serif\" font-size=\"14.00\">&gt;</text>\n",
-       "<text text-anchor=\"middle\" x=\"245\" y=\"-233.8\" font-family=\"Times,serif\" font-size=\"14.00\">false</text>\n",
-       "<text text-anchor=\"middle\" x=\"245\" y=\"-217\" font-family=\"Times,serif\" font-size=\"14.00\">2 &gt; 3</text>\n",
-       "</g>\n",
-       "<!-- Node2&#45;&gt;Node1 -->\n",
-       "<g id=\"edge4\" class=\"edge\"><title>Node2&#45;&gt;Node1</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M217.825,-218.43C207.768,-210.911 195.951,-202.075 184.504,-193.517\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"186.37,-190.542 176.265,-187.357 182.178,-196.148 186.37,-190.542\"/>\n",
-       "</g>\n",
-       "<!-- Node3 -->\n",
-       "<g id=\"node6\" class=\"node\"><title>Node3</title>\n",
-       "<polygon fill=\"white\" stroke=\"black\" points=\"308,-275 308,-311 362,-311 362,-275 308,-275\"/>\n",
-       "<text text-anchor=\"middle\" x=\"335\" y=\"-288.9\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
-       "</g>\n",
-       "<!-- Node3&#45;&gt;Node2 -->\n",
-       "<g id=\"edge6\" class=\"edge\"><title>Node3&#45;&gt;Node2</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M307.597,-276.498C299.168,-271.23 289.707,-265.317 280.776,-259.735\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"282.416,-256.633 272.081,-254.301 278.706,-262.569 282.416,-256.633\"/>\n",
-       "</g>\n",
-       "<!-- Node4 -->\n",
-       "<g id=\"node8\" class=\"node\"><title>Node4</title>\n",
-       "<polygon fill=\"white\" stroke=\"black\" points=\"308,-220 308,-256 362,-256 362,-220 308,-220\"/>\n",
-       "<text text-anchor=\"middle\" x=\"335\" y=\"-233.9\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
-       "</g>\n",
-       "<!-- Node4&#45;&gt;Node2 -->\n",
-       "<g id=\"edge8\" class=\"edge\"><title>Node4&#45;&gt;Node2</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M307.597,-238C299.607,-238 290.689,-238 282.176,-238\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"282.081,-234.5 272.081,-238 282.081,-241.5 282.081,-234.5\"/>\n",
-       "</g>\n",
-       "<!-- Node5 -->\n",
-       "<g id=\"node10\" class=\"node\"><title>Node5</title>\n",
-       "<polygon fill=\"#b3ee3a\" stroke=\"#b3ee3a\" points=\"260,-187.401 230,-187.401 218,-175.401 218,-140.599 230,-128.599 260,-128.599 272,-140.599 272,-175.401 260,-187.401\"/>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M230,-187.401C224,-187.401 218,-181.401 218,-175.401\"/>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M218,-140.599C218,-134.599 224,-128.599 230,-128.599\"/>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M260,-128.599C266,-128.599 272,-134.599 272,-140.599\"/>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M272,-175.401C272,-181.401 266,-187.401 260,-187.401\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"260,-187.401 230,-187.401 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M230,-187.401C224,-187.401 218,-181.401 218,-175.401\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"218,-175.401 218,-140.599 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M218,-140.599C218,-134.599 224,-128.599 230,-128.599\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"230,-128.599 260,-128.599 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M260,-128.599C266,-128.599 272,-134.599 272,-140.599\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"272,-140.599 272,-175.401 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M272,-175.401C272,-181.401 266,-187.401 260,-187.401\"/>\n",
-       "<text text-anchor=\"middle\" x=\"245\" y=\"-170.6\" font-family=\"Times,serif\" font-size=\"14.00\">&gt;</text>\n",
-       "<text text-anchor=\"middle\" x=\"245\" y=\"-153.8\" font-family=\"Times,serif\" font-size=\"14.00\">true</text>\n",
-       "<text text-anchor=\"middle\" x=\"245\" y=\"-137\" font-family=\"Times,serif\" font-size=\"14.00\">4 &gt; 1</text>\n",
-       "</g>\n",
-       "<!-- Node5&#45;&gt;Node1 -->\n",
-       "<g id=\"edge10\" class=\"edge\"><title>Node5&#45;&gt;Node1</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M217.825,-158C209.913,-158 200.912,-158 191.859,-158\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"191.671,-154.5 181.671,-158 191.671,-161.5 191.671,-154.5\"/>\n",
-       "</g>\n",
-       "<!-- Node6 -->\n",
-       "<g id=\"node12\" class=\"node\"><title>Node6</title>\n",
-       "<polygon fill=\"white\" stroke=\"black\" points=\"308,-165 308,-201 362,-201 362,-165 308,-165\"/>\n",
-       "<text text-anchor=\"middle\" x=\"335\" y=\"-178.9\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
-       "</g>\n",
-       "<!-- Node6&#45;&gt;Node5 -->\n",
-       "<g id=\"edge12\" class=\"edge\"><title>Node6&#45;&gt;Node5</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M307.597,-175.499C299.519,-173.204 290.493,-170.64 281.895,-168.198\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"282.657,-164.775 272.081,-165.409 280.744,-171.509 282.657,-164.775\"/>\n",
-       "</g>\n",
-       "<!-- Node7 -->\n",
-       "<g id=\"node14\" class=\"node\"><title>Node7</title>\n",
-       "<polygon fill=\"white\" stroke=\"black\" points=\"308,-110 308,-146 362,-146 362,-110 308,-110\"/>\n",
-       "<text text-anchor=\"middle\" x=\"335\" y=\"-123.9\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
-       "</g>\n",
-       "<!-- Node7&#45;&gt;Node5 -->\n",
-       "<g id=\"edge14\" class=\"edge\"><title>Node7&#45;&gt;Node5</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M307.597,-137.001C299.431,-139.785 290.297,-142.899 281.615,-145.858\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"280.417,-142.569 272.081,-149.109 282.676,-149.195 280.417,-142.569\"/>\n",
-       "</g>\n",
-       "<!-- Node8 -->\n",
-       "<g id=\"node16\" class=\"node\"><title>Node8</title>\n",
-       "<polygon fill=\"#b3ee3a\" stroke=\"#b3ee3a\" points=\"155.539,-105.401 116.461,-105.401 104.461,-93.4014 104.461,-58.5986 116.461,-46.5986 155.539,-46.5986 167.539,-58.5986 167.539,-93.4014 155.539,-105.401\"/>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M116.461,-105.401C110.461,-105.401 104.461,-99.4014 104.461,-93.4014\"/>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M104.461,-58.5986C104.461,-52.5986 110.461,-46.5986 116.461,-46.5986\"/>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M155.539,-46.5986C161.539,-46.5986 167.539,-52.5986 167.539,-58.5986\"/>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M167.539,-93.4014C167.539,-99.4014 161.539,-105.401 155.539,-105.401\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"155.539,-105.401 116.461,-105.401 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M116.461,-105.401C110.461,-105.401 104.461,-99.4014 104.461,-93.4014\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"104.461,-93.4014 104.461,-58.5986 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M104.461,-58.5986C104.461,-52.5986 110.461,-46.5986 116.461,-46.5986\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"116.461,-46.5986 155.539,-46.5986 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M155.539,-46.5986C161.539,-46.5986 167.539,-52.5986 167.539,-58.5986\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"167.539,-58.5986 167.539,-93.4014 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M167.539,-93.4014C167.539,-99.4014 161.539,-105.401 155.539,-105.401\"/>\n",
-       "<text text-anchor=\"middle\" x=\"136\" y=\"-88.6\" font-family=\"Times,serif\" font-size=\"14.00\">¬</text>\n",
-       "<text text-anchor=\"middle\" x=\"136\" y=\"-71.8\" font-family=\"Times,serif\" font-size=\"14.00\">true</text>\n",
-       "<text text-anchor=\"middle\" x=\"136\" y=\"-55\" font-family=\"Times,serif\" font-size=\"14.00\">¬(5 &lt; 1)</text>\n",
-       "</g>\n",
-       "<!-- Node8&#45;&gt;Noderoot -->\n",
-       "<g id=\"edge16\" class=\"edge\"><title>Node8&#45;&gt;Noderoot</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M104.338,-87.749C91.7402,-92.5762 77.0624,-98.2004 63.962,-103.22\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"62.3978,-100.071 54.3122,-106.918 64.9025,-106.608 62.3978,-100.071\"/>\n",
-       "</g>\n",
-       "<!-- Node9 -->\n",
-       "<g id=\"node18\" class=\"node\"><title>Node9</title>\n",
-       "<polygon fill=\"tomato\" stroke=\"tomato\" points=\"260,-102.401 230,-102.401 218,-90.4014 218,-55.5986 230,-43.5986 260,-43.5986 272,-55.5986 272,-90.4014 260,-102.401\"/>\n",
-       "<path fill=\"tomato\" stroke=\"tomato\" d=\"M230,-102.401C224,-102.401 218,-96.4014 218,-90.4014\"/>\n",
-       "<path fill=\"tomato\" stroke=\"tomato\" d=\"M218,-55.5986C218,-49.5986 224,-43.5986 230,-43.5986\"/>\n",
-       "<path fill=\"tomato\" stroke=\"tomato\" d=\"M260,-43.5986C266,-43.5986 272,-49.5986 272,-55.5986\"/>\n",
-       "<path fill=\"tomato\" stroke=\"tomato\" d=\"M272,-90.4014C272,-96.4014 266,-102.401 260,-102.401\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"260,-102.401 230,-102.401 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M230,-102.401C224,-102.401 218,-96.4014 218,-90.4014\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"218,-90.4014 218,-55.5986 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M218,-55.5986C218,-49.5986 224,-43.5986 230,-43.5986\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"230,-43.5986 260,-43.5986 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M260,-43.5986C266,-43.5986 272,-49.5986 272,-55.5986\"/>\n",
-       "<polyline fill=\"none\" stroke=\"black\" points=\"272,-55.5986 272,-90.4014 \"/>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M272,-90.4014C272,-96.4014 266,-102.401 260,-102.401\"/>\n",
-       "<text text-anchor=\"middle\" x=\"245\" y=\"-85.6\" font-family=\"Times,serif\" font-size=\"14.00\">&lt;</text>\n",
-       "<text text-anchor=\"middle\" x=\"245\" y=\"-68.8\" font-family=\"Times,serif\" font-size=\"14.00\">false</text>\n",
-       "<text text-anchor=\"middle\" x=\"245\" y=\"-52\" font-family=\"Times,serif\" font-size=\"14.00\">5 &lt; 1</text>\n",
-       "</g>\n",
-       "<!-- Node9&#45;&gt;Node8 -->\n",
-       "<g id=\"edge18\" class=\"edge\"><title>Node9&#45;&gt;Node8</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M217.825,-73.7339C205.913,-74.0679 191.531,-74.4711 178.221,-74.8443\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"177.741,-71.3562 167.843,-75.1352 177.938,-78.3535 177.741,-71.3562\"/>\n",
-       "</g>\n",
-       "<!-- Node10 -->\n",
-       "<g id=\"node20\" class=\"node\"><title>Node10</title>\n",
-       "<polygon fill=\"white\" stroke=\"black\" points=\"308,-55 308,-91 362,-91 362,-55 308,-55\"/>\n",
-       "<text text-anchor=\"middle\" x=\"335\" y=\"-68.9\" font-family=\"Times,serif\" font-size=\"14.00\">5</text>\n",
-       "</g>\n",
-       "<!-- Node10&#45;&gt;Node9 -->\n",
-       "<g id=\"edge20\" class=\"edge\"><title>Node10&#45;&gt;Node9</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M307.597,-73C299.607,-73 290.689,-73 282.176,-73\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"282.081,-69.5001 272.081,-73 282.081,-76.5001 282.081,-69.5001\"/>\n",
-       "</g>\n",
-       "<!-- Node11 -->\n",
-       "<g id=\"node22\" class=\"node\"><title>Node11</title>\n",
-       "<polygon fill=\"white\" stroke=\"black\" points=\"308,-0 308,-36 362,-36 362,-0 308,-0\"/>\n",
-       "<text text-anchor=\"middle\" x=\"335\" y=\"-13.9\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
-       "</g>\n",
-       "<!-- Node11&#45;&gt;Node9 -->\n",
-       "<g id=\"edge22\" class=\"edge\"><title>Node11&#45;&gt;Node9</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M307.597,-34.5018C299.168,-39.7702 289.707,-45.6833 280.776,-51.2647\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"278.706,-48.4313 272.081,-56.6994 282.416,-54.3673 278.706,-48.4313\"/>\n",
-       "</g>\n",
-       "</g>\n",
-       "</svg>"
-      ],
-      "text/plain": [
-       "<Dot visualization: formula_tree [(2>3 => 4>1) <=> not(5<1)]>"
-      ]
-     },
-     "execution_count": 19,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     ":dot formula_tree (2>3 ⇒ 4>1) ⇔ ¬(5<1)"
    ]
@@ -878,32 +433,9 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 20,
+   "execution_count": null,
    "metadata": {},
-   "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": 20,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     ":table {p,q,F1,F2| p:BOOL & q:BOOL & \n",
     "                   F1=bool(p=TRUE ∨ (¬(p=TRUE) ∧ q=TRUE)) & // p ∨ (¬p ∧ q)\n",
@@ -946,32 +478,9 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 21,
+   "execution_count": null,
    "metadata": {},
-   "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": 21,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "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",
@@ -993,32 +502,9 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 22,
+   "execution_count": null,
    "metadata": {},
-   "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": 22,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "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",
@@ -1048,32 +534,9 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 24,
+   "execution_count": null,
    "metadata": {},
-   "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": 24,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     ":table {p,q,F1,F2| p:BOOL & q:BOOL & F1=bool(p=TRUE ⇔ q=TRUE) & F2=bool(p=TRUE ⇒ q=TRUE)}"
    ]
@@ -1141,32 +604,9 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 25,
+   "execution_count": null,
    "metadata": {},
-   "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": 25,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     ":table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL & \n",
     "                   S1=bool(x=TRUE ⇔ y=TRUE) &\n",
@@ -1191,32 +631,9 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 27,
+   "execution_count": null,
    "metadata": {},
-   "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": 27,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     ":table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL & \n",
     "                   S1=bool(x=TRUE ⇒ y=TRUE) &\n",
@@ -1264,32 +681,9 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 28,
+   "execution_count": null,
    "metadata": {},
-   "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": 28,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     ":table {x,y,S1,S2,Puzzle,WS | x:BOOL & y:BOOL & \n",
     "                   S1=bool(x=TRUE ⇔ y=TRUE) &\n",
@@ -1423,7 +817,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 29,
+   "execution_count": 1,
    "metadata": {},
    "outputs": [
     {
@@ -1448,7 +842,7 @@
        "2\t3\tTRUE\n"
       ]
      },
-     "execution_count": 29,
+     "execution_count": 1,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1496,25 +890,19 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 30,
+   "execution_count": 2,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/markdown": [
-       "$\\mathit{TRUE}$\n",
-       "\n",
-       "**Solution:**\n",
-       "* $\\mathit{x} = 0$"
+       "$\\mathit{TRUE}$"
       ],
       "text/plain": [
-       "TRUE\n",
-       "\n",
-       "Solution:\n",
-       "\tx = 0"
+       "TRUE"
       ]
      },
-     "execution_count": 30,
+     "execution_count": 2,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1532,7 +920,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 31,
+   "execution_count": 3,
    "metadata": {},
    "outputs": [
     {
@@ -1550,7 +938,7 @@
        "\tx = 0"
       ]
      },
-     "execution_count": 31,
+     "execution_count": 3,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1561,7 +949,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 32,
+   "execution_count": 4,
    "metadata": {},
    "outputs": [
     {
@@ -1579,7 +967,7 @@
        "\tx = 10"
       ]
      },
-     "execution_count": 32,
+     "execution_count": 4,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1590,7 +978,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 35,
+   "execution_count": 7,
    "metadata": {},
    "outputs": [
     {
@@ -1608,7 +996,7 @@
        "\tx = −100"
       ]
      },
-     "execution_count": 35,
+     "execution_count": 7,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1744,6 +1132,131 @@
     "* Nächste Vorlesung: Grundlagen der Mengentheorie"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Anhang mit Erläuterungen\n",
+    "\n",
+    "## Unterschied zwischen $\\equiv$ und $\\Leftrightarrow$\n",
+    "\n",
+    "* $\\Leftrightarrow$ is ein Junktor und wird verwendet um Formeln der Aussagenlogik zu erstellen\n",
+    " * wenn $\\phi$ und $\\psi$ Formeln der Aussagenlogik sind, dann ist $\\phi \\Leftrightarrow \\psi$  also auch eine Formel der Aussagenlogik\n",
+    "* $\\equiv$ is *kein* Junktor und kann *nicht* in Formeln der Aussagenlogik auftauchen\n",
+    "* Mit $\\equiv$ trifft man mathematische Aussagen über zwei Formeln.\n",
+    "\n",
+    "Es gilt aber folgendes Theorem:\n",
+    "Seien $\\phi$ und $\\psi$ beliebige Formeln der Aussagenlogik.\n",
+    "Dann gilt:\n",
+    "* $\\phi \\equiv \\psi$ gdw die Formel $\\phi \\Leftrightarrow \\psi$ eine Tautologie ist.\n"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Zum Beispiel haben wir $p \\vee \\neg q \\equiv q \\Rightarrow p$ und in der Tat is die Formel $(p \\vee \\neg q) \\Leftrightarrow (q \\Rightarrow p)$ eine Tautologie:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 2,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "|p|q|ODER|IMPL|EQUIV|\n",
+       "|---|---|---|---|---|\n",
+       "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
+       "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|\n",
+       "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
+       "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n"
+      ],
+      "text/plain": [
+       "p\tq\tODER\tIMPL\tEQUIV\n",
+       "FALSE\tFALSE\tTRUE\tTRUE\tTRUE\n",
+       "FALSE\tTRUE\tFALSE\tFALSE\tTRUE\n",
+       "TRUE\tFALSE\tTRUE\tTRUE\tTRUE\n",
+       "TRUE\tTRUE\tTRUE\tTRUE\tTRUE\n"
+      ]
+     },
+     "execution_count": 2,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":table {p,q,ODER,IMPL,EQUIV| p:BOOL & q:BOOL &\n",
+    "                            ODER=bool(p=TRUE ∨ ¬(q=TRUE)) & // 𝑝∨¬𝑞\n",
+    "                            IMPL = bool(q=TRUE ⇒ p=TRUE) &  // 𝑞⇒p\n",
+    "                            EQUIV=bool((ODER=TRUE) ⇔ (IMPL=TRUE))}"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Die Formel $(p \\vee q) \\Leftrightarrow (p \\wedge q)$ hingegen ist eine erfüllbare Formel, aber keine Tautologie.\n",
+    "Es gilt also $(p \\vee q) \\not\\equiv (p \\wedge q)$!"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 4,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "|p|q|ODER|UND|EQUIV|\n",
+       "|---|---|---|---|---|\n",
+       "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|\n",
+       "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n",
+       "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n",
+       "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n"
+      ],
+      "text/plain": [
+       "p\tq\tODER\tUND\tEQUIV\n",
+       "FALSE\tFALSE\tFALSE\tFALSE\tTRUE\n",
+       "FALSE\tTRUE\tTRUE\tFALSE\tFALSE\n",
+       "TRUE\tFALSE\tTRUE\tFALSE\tFALSE\n",
+       "TRUE\tTRUE\tTRUE\tTRUE\tTRUE\n"
+      ]
+     },
+     "execution_count": 4,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":table {p,q,ODER,UND,EQUIV| p:BOOL & q:BOOL &\n",
+    "                            ODER=bool(p=TRUE ∨ q=TRUE) & // 𝑝∨𝑞\n",
+    "                            UND = bool(p=TRUE & q=TRUE) &  // p&q\n",
+    "                            EQUIV=bool((ODER=TRUE) ⇔ (UND=TRUE))}"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "\n",
+    "## Unterschied zwischen $\\models$ und $\\Rightarrow$\n",
+    "\n",
+    "Das Gleiche gilt für diese beiden Symbole:\n",
+    "\n",
+    "* $\\Rightarrow$ is ein Junktor und wird verwendet um Formeln der Aussagenlogik zu erstellen\n",
+    " * wenn $\\phi$ und $\\psi$ Formeln der Aussagenlogik sind, dann ist $\\phi \\Rightarrow \\psi$  also auch eine Formel der Aussagenlogik\n",
+    "* $\\models$ is *kein* Junktor und kann *nicht* in Formeln der Aussagenlogik auftauchen\n",
+    "* Mit $\\models$ trifft man mathematische Aussagen über zwei Formeln.\n",
+    "\n",
+    "Es gilt aber folgendes Theorem:\n",
+    "Seien $\\phi$ und $\\psi$ beliebige Formeln der Aussagenlogik.\n",
+    "Dann gilt:\n",
+    "* $\\phi \\models \\psi$ gdw die Formel $\\phi \\Rightarrow \\psi$ eine Tautologie ist.\n",
+    "\n"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,