diff --git a/logic_programming/3_PropositionalLogic.ipynb b/logic_programming/3_PropositionalLogic.ipynb
index 99e5067f770bf6fb288c4ec9b397450def4a4647..8d09732394206de1baa519f4f21930130f9ccab0 100644
--- a/logic_programming/3_PropositionalLogic.ipynb
+++ b/logic_programming/3_PropositionalLogic.ipynb
@@ -42,7 +42,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 23,
+   "execution_count": 11,
    "id": "964ebd52",
    "metadata": {
     "vscode": {
@@ -50,66 +50,10 @@
     }
    },
    "outputs": [
-    {
-     "data": {
-      "text/html": [
-       "\n",
-       "            <style>\n",
-       "            details  {\n",
-       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
-       "            }\n",
-       "\n",
-       "            details > summary {\n",
-       "              cursor: pointer;\n",
-       "            }\n",
-       "            </style>\n",
-       "            <details><summary>Previously defined clauses of user:wff/2 were retracted (click to expand)</summary><pre>:- dynamic wff/2.\n",
-       "\n",
-       "wff(A, B) :-\n",
-       "    A=[112|B].\n",
-       "wff(A, B) :-\n",
-       "    A=[113|B].\n",
-       "wff(A, B) :-\n",
-       "    A=[40, 172|C],\n",
-       "    wff(C, D),\n",
-       "    D=[41|B].\n",
-       "wff(A, B) :-\n",
-       "    A=[40|C],\n",
-       "    wff(C, D),\n",
-       "    D=[8743|E],\n",
-       "    wff(E, F),\n",
-       "    F=[41|B].\n",
-       "</pre></details>"
-      ],
-      "text/plain": [
-       "Previously defined clauses of user:wff/2 were retracted:\n",
-       ":- dynamic wff/2.\n",
-       "\n",
-       "wff(A, B) :-\n",
-       "    A=[112|B].\n",
-       "wff(A, B) :-\n",
-       "    A=[113|B].\n",
-       "wff(A, B) :-\n",
-       "    A=[40, 172|C],\n",
-       "    wff(C, D),\n",
-       "    D=[41|B].\n",
-       "wff(A, B) :-\n",
-       "    A=[40|C],\n",
-       "    wff(C, D),\n",
-       "    D=[8743|E],\n",
-       "    wff(E, F),\n",
-       "    F=[41|B].\n"
-      ]
-     },
-     "metadata": {
-      "application/json": {}
-     },
-     "output_type": "display_data"
-    },
     {
      "data": {
       "text/plain": [
-       "% Asserting clauses for user:wff/2\n"
+       "\u001b[1;31m% The Prolog server was restarted"
       ]
      },
      "metadata": {},
@@ -129,7 +73,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 17,
+   "execution_count": 12,
    "id": "fc6823ad",
    "metadata": {
     "vscode": {
@@ -153,7 +97,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 18,
+   "execution_count": 13,
    "id": "152289b6",
    "metadata": {
     "vscode": {
@@ -177,7 +121,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 29,
+   "execution_count": 14,
    "id": "2c3dd1bf",
    "metadata": {
     "vscode": {
@@ -200,6 +144,27 @@
     "%comment."
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "38b0a282",
+   "metadata": {},
+   "source": [
+    "This grammar does not talk about whitespace and requires parentheses for every connective used.\n",
+    "In practice, one typically uses operator precedences to avoid having to write too many parentheses:\n",
+    "- negation binds strongest\n",
+    "- then come conjunction and disjunction\n",
+    "- then come implication and equivalence.\n",
+    "\n",
+    "So instead of\n",
+    "- (((¬ p) ∧ (¬ q)) ⇒ ((¬ p) ∨ (¬ q)))\n",
+    "we can write\n",
+    "- ¬ p ∧ ¬ q ⇒ ¬ p ∨ ¬ q\n",
+    "\n",
+    "We will try not not mix conjunction/disjunction and implication/equivalence without parentheses.\n",
+    "We will also not try to improve our Prolog parser here to accomodate these precedences.\n",
+    "This is the subject of another course (on compiler construction)."
+   ]
+  },
   {
    "cell_type": "markdown",
    "id": "92b6dc2d",
@@ -211,78 +176,14 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 24,
+   "execution_count": 15,
    "id": "78163b60",
    "metadata": {
     "vscode": {
      "languageId": "prolog"
     }
    },
-   "outputs": [
-    {
-     "data": {
-      "text/html": [
-       "\n",
-       "            <style>\n",
-       "            details  {\n",
-       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
-       "            }\n",
-       "\n",
-       "            details > summary {\n",
-       "              cursor: pointer;\n",
-       "            }\n",
-       "            </style>\n",
-       "            <details><summary>Previously defined clauses of user:wff/3 were retracted (click to expand)</summary><pre>:- dynamic wff/3.\n",
-       "\n",
-       "wff(p, [112|A], A).\n",
-       "wff(q, A, B) :-\n",
-       "    A=[113|B].\n",
-       "wff(not(A), B, C) :-\n",
-       "    B=[40, 172|D],\n",
-       "    wff(A, D, E),\n",
-       "    E=[41|C].\n",
-       "wff(and(A, B), C, D) :-\n",
-       "    C=[40|E],\n",
-       "    wff(A, E, F),\n",
-       "    F=[8743|G],\n",
-       "    wff(B, G, H),\n",
-       "    H=[41|D].\n",
-       "</pre></details>"
-      ],
-      "text/plain": [
-       "Previously defined clauses of user:wff/3 were retracted:\n",
-       ":- dynamic wff/3.\n",
-       "\n",
-       "wff(p, [112|A], A).\n",
-       "wff(q, A, B) :-\n",
-       "    A=[113|B].\n",
-       "wff(not(A), B, C) :-\n",
-       "    B=[40, 172|D],\n",
-       "    wff(A, D, E),\n",
-       "    E=[41|C].\n",
-       "wff(and(A, B), C, D) :-\n",
-       "    C=[40|E],\n",
-       "    wff(A, E, F),\n",
-       "    F=[8743|G],\n",
-       "    wff(B, G, H),\n",
-       "    H=[41|D].\n"
-      ]
-     },
-     "metadata": {
-      "application/json": {}
-     },
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/plain": [
-       "% Asserting clauses for user:wff/3\n"
-      ]
-     },
-     "metadata": {},
-     "output_type": "display_data"
-    }
-   ],
+   "outputs": [],
    "source": [
     " :- set_prolog_flag(double_quotes, codes).\n",
     "wff(p) --> \"p\". % atomic proposition\n",
@@ -296,7 +197,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 25,
+   "execution_count": 16,
    "id": "8ddb568d",
    "metadata": {
     "vscode": {
@@ -320,7 +221,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 26,
+   "execution_count": 17,
    "id": "075dc3b2",
    "metadata": {
     "vscode": {
@@ -344,7 +245,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 28,
+   "execution_count": 18,
    "id": "338cb7dd",
    "metadata": {
     "vscode": {
@@ -378,160 +279,14 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 8,
+   "execution_count": 19,
    "id": "f6116612",
    "metadata": {
     "vscode": {
      "languageId": "prolog"
     }
    },
-   "outputs": [
-    {
-     "data": {
-      "text/html": [
-       "\n",
-       "            <style>\n",
-       "            details  {\n",
-       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
-       "            }\n",
-       "\n",
-       "            details > summary {\n",
-       "              cursor: pointer;\n",
-       "            }\n",
-       "            </style>\n",
-       "            <details><summary>Previously defined clauses of user:subtree/3 were retracted (click to expand)</summary><pre>:- dynamic subtree/3.\n",
-       "\n",
-       "subtree(A, B, C) :-\n",
-       "    A=..[_|D],\n",
-       "    nth1(B, D, C).\n",
-       "</pre></details>"
-      ],
-      "text/plain": [
-       "Previously defined clauses of user:subtree/3 were retracted:\n",
-       ":- dynamic subtree/3.\n",
-       "\n",
-       "subtree(A, B, C) :-\n",
-       "    A=..[_|D],\n",
-       "    nth1(B, D, C).\n"
-      ]
-     },
-     "metadata": {
-      "application/json": {}
-     },
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/plain": [
-       "% Asserting clauses for user:subtree/3\n"
-      ]
-     },
-     "metadata": {},
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/html": [
-       "\n",
-       "            <style>\n",
-       "            details  {\n",
-       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
-       "            }\n",
-       "\n",
-       "            details > summary {\n",
-       "              cursor: pointer;\n",
-       "            }\n",
-       "            </style>\n",
-       "            <details><summary>Previously defined clauses of user:rec_subtree/2 were retracted (click to expand)</summary><pre>:- dynamic rec_subtree/2.\n",
-       "\n",
-       "rec_subtree(A, B) :-\n",
-       "    A=B.\n",
-       "rec_subtree(A, B) :-\n",
-       "    subtree(A, _, C),\n",
-       "    rec_subtree(C, B).\n",
-       "</pre></details>"
-      ],
-      "text/plain": [
-       "Previously defined clauses of user:rec_subtree/2 were retracted:\n",
-       ":- dynamic rec_subtree/2.\n",
-       "\n",
-       "rec_subtree(A, B) :-\n",
-       "    A=B.\n",
-       "rec_subtree(A, B) :-\n",
-       "    subtree(A, _, C),\n",
-       "    rec_subtree(C, B).\n"
-      ]
-     },
-     "metadata": {
-      "application/json": {}
-     },
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/plain": [
-       "% Asserting clauses for user:rec_subtree/2\n"
-      ]
-     },
-     "metadata": {},
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/html": [
-       "\n",
-       "            <style>\n",
-       "            details  {\n",
-       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
-       "            }\n",
-       "\n",
-       "            details > summary {\n",
-       "              cursor: pointer;\n",
-       "            }\n",
-       "            </style>\n",
-       "            <details><summary>Previously defined clauses of user:subnode/3 were retracted (click to expand)</summary><pre>:- dynamic subnode/3.\n",
-       "\n",
-       "subnode(A, [shape/B, label/C], D) :-\n",
-       "    rec_subtree(D, A),\n",
-       "    functor(A, C, _),\n",
-       "    (   atom(A)\n",
-       "    ->  B=egg\n",
-       "    ;   number(A)\n",
-       "    ->  B=oval\n",
-       "    ;   B=rect\n",
-       "    ).\n",
-       "</pre></details>"
-      ],
-      "text/plain": [
-       "Previously defined clauses of user:subnode/3 were retracted:\n",
-       ":- dynamic subnode/3.\n",
-       "\n",
-       "subnode(A, [shape/B, label/C], D) :-\n",
-       "    rec_subtree(D, A),\n",
-       "    functor(A, C, _),\n",
-       "    (   atom(A)\n",
-       "    ->  B=egg\n",
-       "    ;   number(A)\n",
-       "    ->  B=oval\n",
-       "    ;   B=rect\n",
-       "    ).\n"
-      ]
-     },
-     "metadata": {
-      "application/json": {}
-     },
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/plain": [
-       "% Asserting clauses for user:subnode/3\n"
-      ]
-     },
-     "metadata": {},
-     "output_type": "display_data"
-    }
-   ],
+   "outputs": [],
    "source": [
     "subtree(Term,Nr,SubTerm) :- \n",
     "   Term =.. [_|ArgList], %obtain arguments of the term\n",
@@ -548,7 +303,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 9,
+   "execution_count": 20,
    "id": "d7e68593",
    "metadata": {
     "vscode": {
@@ -598,7 +353,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 7,
+   "execution_count": 21,
    "id": "3646e3ee",
    "metadata": {
     "vscode": {
@@ -656,320 +411,14 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 21,
+   "execution_count": 22,
    "id": "350b9756",
    "metadata": {
     "vscode": {
      "languageId": "prolog"
     }
    },
-   "outputs": [
-    {
-     "data": {
-      "text/html": [
-       "\n",
-       "            <style>\n",
-       "            details  {\n",
-       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
-       "            }\n",
-       "\n",
-       "            details > summary {\n",
-       "              cursor: pointer;\n",
-       "            }\n",
-       "            </style>\n",
-       "            <details><summary>Previously defined clauses of user:not/2 were retracted (click to expand)</summary><pre>:- dynamic not/2.\n",
-       "\n",
-       "not(true, false).\n",
-       "not(false, true).\n",
-       "</pre></details>"
-      ],
-      "text/plain": [
-       "Previously defined clauses of user:not/2 were retracted:\n",
-       ":- dynamic not/2.\n",
-       "\n",
-       "not(true, false).\n",
-       "not(false, true).\n"
-      ]
-     },
-     "metadata": {
-      "application/json": {}
-     },
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/plain": [
-       "% Asserting clauses for user:not/2\n"
-      ]
-     },
-     "metadata": {},
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/html": [
-       "\n",
-       "            <style>\n",
-       "            details  {\n",
-       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
-       "            }\n",
-       "\n",
-       "            details > summary {\n",
-       "              cursor: pointer;\n",
-       "            }\n",
-       "            </style>\n",
-       "            <details><summary>Previously defined clauses of user:and/3 were retracted (click to expand)</summary><pre>:- dynamic and/3.\n",
-       "\n",
-       "and(true, A, A).\n",
-       "and(false, _, false).\n",
-       "</pre></details>"
-      ],
-      "text/plain": [
-       "Previously defined clauses of user:and/3 were retracted:\n",
-       ":- dynamic and/3.\n",
-       "\n",
-       "and(true, A, A).\n",
-       "and(false, _, false).\n"
-      ]
-     },
-     "metadata": {
-      "application/json": {}
-     },
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/plain": [
-       "% Asserting clauses for user:and/3\n"
-      ]
-     },
-     "metadata": {},
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/html": [
-       "\n",
-       "            <style>\n",
-       "            details  {\n",
-       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
-       "            }\n",
-       "\n",
-       "            details > summary {\n",
-       "              cursor: pointer;\n",
-       "            }\n",
-       "            </style>\n",
-       "            <details><summary>Previously defined clauses of user:or/3 were retracted (click to expand)</summary><pre>:- dynamic or/3.\n",
-       "\n",
-       "or(true, _, true).\n",
-       "or(false, A, A).\n",
-       "</pre></details>"
-      ],
-      "text/plain": [
-       "Previously defined clauses of user:or/3 were retracted:\n",
-       ":- dynamic or/3.\n",
-       "\n",
-       "or(true, _, true).\n",
-       "or(false, A, A).\n"
-      ]
-     },
-     "metadata": {
-      "application/json": {}
-     },
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/plain": [
-       "% Asserting clauses for user:or/3\n"
-      ]
-     },
-     "metadata": {},
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/html": [
-       "\n",
-       "            <style>\n",
-       "            details  {\n",
-       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
-       "            }\n",
-       "\n",
-       "            details > summary {\n",
-       "              cursor: pointer;\n",
-       "            }\n",
-       "            </style>\n",
-       "            <details><summary>Previously defined clauses of user:implies/3 were retracted (click to expand)</summary><pre>:- dynamic implies/3.\n",
-       "\n",
-       "implies(A, B, C) :-\n",
-       "    not(A, D),\n",
-       "    or(D, B, C).\n",
-       "</pre></details>"
-      ],
-      "text/plain": [
-       "Previously defined clauses of user:implies/3 were retracted:\n",
-       ":- dynamic implies/3.\n",
-       "\n",
-       "implies(A, B, C) :-\n",
-       "    not(A, D),\n",
-       "    or(D, B, C).\n"
-      ]
-     },
-     "metadata": {
-      "application/json": {}
-     },
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/plain": [
-       "% Asserting clauses for user:implies/3\n"
-      ]
-     },
-     "metadata": {},
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/html": [
-       "\n",
-       "            <style>\n",
-       "            details  {\n",
-       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
-       "            }\n",
-       "\n",
-       "            details > summary {\n",
-       "              cursor: pointer;\n",
-       "            }\n",
-       "            </style>\n",
-       "            <details><summary>Previously defined clauses of user:equiv/3 were retracted (click to expand)</summary><pre>:- dynamic equiv/3.\n",
-       "\n",
-       "equiv(A, B, C) :-\n",
-       "    implies(A, B, D),\n",
-       "    implies(B, A, E),\n",
-       "    and(D, E, C).\n",
-       "</pre></details>"
-      ],
-      "text/plain": [
-       "Previously defined clauses of user:equiv/3 were retracted:\n",
-       ":- dynamic equiv/3.\n",
-       "\n",
-       "equiv(A, B, C) :-\n",
-       "    implies(A, B, D),\n",
-       "    implies(B, A, E),\n",
-       "    and(D, E, C).\n"
-      ]
-     },
-     "metadata": {
-      "application/json": {}
-     },
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/plain": [
-       "% Asserting clauses for user:equiv/3\n"
-      ]
-     },
-     "metadata": {},
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/html": [
-       "\n",
-       "            <style>\n",
-       "            details  {\n",
-       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
-       "            }\n",
-       "\n",
-       "            details > summary {\n",
-       "              cursor: pointer;\n",
-       "            }\n",
-       "            </style>\n",
-       "            <details><summary>Previously defined clauses of user:truth_value/1 were retracted (click to expand)</summary><pre>:- dynamic truth_value/1.\n",
-       "\n",
-       "truth_value(true).\n",
-       "truth_value(false).\n",
-       "</pre></details>"
-      ],
-      "text/plain": [
-       "Previously defined clauses of user:truth_value/1 were retracted:\n",
-       ":- dynamic truth_value/1.\n",
-       "\n",
-       "truth_value(true).\n",
-       "truth_value(false).\n"
-      ]
-     },
-     "metadata": {
-      "application/json": {}
-     },
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/plain": [
-       "% Asserting clauses for user:truth_value/1\n"
-      ]
-     },
-     "metadata": {},
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/html": [
-       "\n",
-       "            <style>\n",
-       "            details  {\n",
-       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
-       "            }\n",
-       "\n",
-       "            details > summary {\n",
-       "              cursor: pointer;\n",
-       "            }\n",
-       "            </style>\n",
-       "            <details><summary>Previously defined clauses of user:truth_table/7 were retracted (click to expand)</summary><pre>:- dynamic truth_table/7.\n",
-       "\n",
-       "truth_table(A, B, C, D, E, F, G) :-\n",
-       "    truth_value(A),\n",
-       "    truth_value(B),\n",
-       "    not(A, C),\n",
-       "    and(A, B, D),\n",
-       "    or(A, B, E),\n",
-       "    implies(A, B, F),\n",
-       "    equiv(A, B, G).\n",
-       "</pre></details>"
-      ],
-      "text/plain": [
-       "Previously defined clauses of user:truth_table/7 were retracted:\n",
-       ":- dynamic truth_table/7.\n",
-       "\n",
-       "truth_table(A, B, C, D, E, F, G) :-\n",
-       "    truth_value(A),\n",
-       "    truth_value(B),\n",
-       "    not(A, C),\n",
-       "    and(A, B, D),\n",
-       "    or(A, B, E),\n",
-       "    implies(A, B, F),\n",
-       "    equiv(A, B, G).\n"
-      ]
-     },
-     "metadata": {
-      "application/json": {}
-     },
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/plain": [
-       "% Asserting clauses for user:truth_table/7\n"
-      ]
-     },
-     "metadata": {},
-     "output_type": "display_data"
-    }
-   ],
+   "outputs": [],
    "source": [
     "not(true,false).\n",
     "not(false,true).\n",
@@ -994,7 +443,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 22,
+   "execution_count": 23,
    "id": "54b57ff8",
    "metadata": {
     "vscode": {
@@ -1040,92 +489,14 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 23,
+   "execution_count": 24,
    "id": "175c00d0",
    "metadata": {
     "vscode": {
      "languageId": "prolog"
     }
    },
-   "outputs": [
-    {
-     "data": {
-      "text/html": [
-       "\n",
-       "            <style>\n",
-       "            details  {\n",
-       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
-       "            }\n",
-       "\n",
-       "            details > summary {\n",
-       "              cursor: pointer;\n",
-       "            }\n",
-       "            </style>\n",
-       "            <details><summary>Previously defined clauses of user:value/3 were retracted (click to expand)</summary><pre>:- dynamic value/3.\n",
-       "\n",
-       "value(A, B, C) :-\n",
-       "    atomic(A),\n",
-       "    member(A/C, B).\n",
-       "value(and(A, B), C, D) :-\n",
-       "    value(A, C, E),\n",
-       "    value(B, C, F),\n",
-       "    and(E, F, D).\n",
-       "value(or(A, B), C, D) :-\n",
-       "    value(A, C, E),\n",
-       "    value(B, C, F),\n",
-       "    or(E, F, D).\n",
-       "value(not(A), B, C) :-\n",
-       "    value(A, B, D),\n",
-       "    not(D, C).\n",
-       "value(implies(A, B), C, D) :-\n",
-       "    value(or(not(A), B), C, D).\n",
-       "value(equiv(A, B), C, D) :-\n",
-       "    value(and(implies(A, B), implies(B, A)),\n",
-       "          C,\n",
-       "          D).\n",
-       "</pre></details>"
-      ],
-      "text/plain": [
-       "Previously defined clauses of user:value/3 were retracted:\n",
-       ":- dynamic value/3.\n",
-       "\n",
-       "value(A, B, C) :-\n",
-       "    atomic(A),\n",
-       "    member(A/C, B).\n",
-       "value(and(A, B), C, D) :-\n",
-       "    value(A, C, E),\n",
-       "    value(B, C, F),\n",
-       "    and(E, F, D).\n",
-       "value(or(A, B), C, D) :-\n",
-       "    value(A, C, E),\n",
-       "    value(B, C, F),\n",
-       "    or(E, F, D).\n",
-       "value(not(A), B, C) :-\n",
-       "    value(A, B, D),\n",
-       "    not(D, C).\n",
-       "value(implies(A, B), C, D) :-\n",
-       "    value(or(not(A), B), C, D).\n",
-       "value(equiv(A, B), C, D) :-\n",
-       "    value(and(implies(A, B), implies(B, A)),\n",
-       "          C,\n",
-       "          D).\n"
-      ]
-     },
-     "metadata": {
-      "application/json": {}
-     },
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/plain": [
-       "% Asserting clauses for user:value/3\n"
-      ]
-     },
-     "metadata": {},
-     "output_type": "display_data"
-    }
-   ],
+   "outputs": [],
    "source": [
     "value(X,Interpretation,Value) :- \n",
     "   atomic(X), % we could also use: proposition(X),\n",
@@ -1143,7 +514,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 24,
+   "execution_count": 25,
    "id": "eee17774",
    "metadata": {
     "vscode": {
@@ -1213,78 +584,14 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 35,
+   "execution_count": 27,
    "id": "2ee60c15",
    "metadata": {
     "vscode": {
      "languageId": "prolog"
     }
    },
-   "outputs": [
-    {
-     "data": {
-      "text/html": [
-       "\n",
-       "            <style>\n",
-       "            details  {\n",
-       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
-       "            }\n",
-       "\n",
-       "            details > summary {\n",
-       "              cursor: pointer;\n",
-       "            }\n",
-       "            </style>\n",
-       "            <details><summary>Previously defined clauses of user:subnode_val/4 were retracted (click to expand)</summary><pre>:- dynamic subnode_val/4.\n",
-       "\n",
-       "subnode_val(A, [shape/B, label/C, style/filled, fillcolor/D], E, F) :-\n",
-       "    rec_subtree(E, A),\n",
-       "    functor(A, C, _),\n",
-       "    (   atom(A)\n",
-       "    ->  B=egg\n",
-       "    ;   number(A)\n",
-       "    ->  B=oval\n",
-       "    ;   B=rect\n",
-       "    ),\n",
-       "    (   value(A, F, true)\n",
-       "    ->  D=olive\n",
-       "    ;   D=salmon1\n",
-       "    ).\n",
-       "</pre></details>"
-      ],
-      "text/plain": [
-       "Previously defined clauses of user:subnode_val/4 were retracted:\n",
-       ":- dynamic subnode_val/4.\n",
-       "\n",
-       "subnode_val(A, [shape/B, label/C, style/filled, fillcolor/D], E, F) :-\n",
-       "    rec_subtree(E, A),\n",
-       "    functor(A, C, _),\n",
-       "    (   atom(A)\n",
-       "    ->  B=egg\n",
-       "    ;   number(A)\n",
-       "    ->  B=oval\n",
-       "    ;   B=rect\n",
-       "    ),\n",
-       "    (   value(A, F, true)\n",
-       "    ->  D=olive\n",
-       "    ;   D=salmon1\n",
-       "    ).\n"
-      ]
-     },
-     "metadata": {
-      "application/json": {}
-     },
-     "output_type": "display_data"
-    },
-    {
-     "data": {
-      "text/plain": [
-       "% Asserting clauses for user:subnode_val/4\n"
-      ]
-     },
-     "metadata": {},
-     "output_type": "display_data"
-    }
-   ],
+   "outputs": [],
    "source": [
     "\n",
     "subnode_val(Sub,[shape/S, label/F, style/filled, fillcolor/C],Formula,Interpretation) :- \n",
@@ -1295,7 +602,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 39,
+   "execution_count": 28,
    "id": "2b497dad",
    "metadata": {
     "vscode": {
@@ -1340,7 +647,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 38,
+   "execution_count": 29,
    "id": "0fd23f05",
    "metadata": {
     "vscode": {
@@ -1385,13 +692,37 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 30,
    "id": "23775624",
    "metadata": {
     "vscode": {
      "languageId": "prolog"
     }
    },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- use_module(library(clpfd))."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "7a6e29ed",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
    "outputs": [],
    "source": []
   }