diff --git a/tests/python/formulas.ipynb b/tests/python/formulas.ipynb
index 20e96c17d..2882ac7ac 100644
--- a/tests/python/formulas.ipynb
+++ b/tests/python/formulas.ipynb
@@ -10,7 +10,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 10,
+   "execution_count": 1,
    "metadata": {},
    "outputs": [],
    "source": [
@@ -27,7 +27,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 11,
+   "execution_count": 2,
    "metadata": {},
    "outputs": [
     {
@@ -39,7 +39,7 @@
        "spot.formula(\"p1 U (p2 R (p3 & !p4))\")"
       ]
      },
-     "execution_count": 11,
+     "execution_count": 2,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -51,7 +51,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 12,
+   "execution_count": 3,
    "metadata": {},
    "outputs": [
     {
@@ -63,7 +63,7 @@
        "spot.formula(\"{a;first_match({b[*];c[+]}[:*3..5];b)}<>-> (c & GFb)\")"
       ]
      },
-     "execution_count": 12,
+     "execution_count": 3,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -81,7 +81,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 13,
+   "execution_count": 4,
    "metadata": {},
    "outputs": [
     {
@@ -93,7 +93,7 @@
        "spot.formula(\"c & (a | b)\")"
       ]
      },
-     "execution_count": 13,
+     "execution_count": 4,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -111,7 +111,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 14,
+   "execution_count": 5,
    "metadata": {},
    "outputs": [
     {
@@ -123,7 +123,7 @@
        "spot.formula(\"c & (a | b)\")"
       ]
      },
-     "execution_count": 14,
+     "execution_count": 5,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -142,7 +142,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 15,
+   "execution_count": 6,
    "metadata": {},
    "outputs": [
     {
@@ -151,7 +151,7 @@
        "'p1 U (p2 R (p3 & !p4))'"
       ]
      },
-     "execution_count": 15,
+     "execution_count": 6,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -169,7 +169,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 16,
+   "execution_count": 7,
    "metadata": {},
    "outputs": [
     {
@@ -201,7 +201,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 17,
+   "execution_count": 8,
    "metadata": {},
    "outputs": [
     {
@@ -237,7 +237,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 18,
+   "execution_count": 9,
    "metadata": {},
    "outputs": [
     {
@@ -299,7 +299,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 19,
+   "execution_count": 10,
    "metadata": {},
    "outputs": [
     {
@@ -308,7 +308,7 @@
        "True"
       ]
      },
-     "execution_count": 19,
+     "execution_count": 10,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -319,7 +319,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 20,
+   "execution_count": 11,
    "metadata": {},
    "outputs": [
     {
@@ -328,7 +328,7 @@
        "False"
       ]
      },
-     "execution_count": 20,
+     "execution_count": 11,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -346,7 +346,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 21,
+   "execution_count": 12,
    "metadata": {},
    "outputs": [
     {
@@ -355,7 +355,7 @@
        "True"
       ]
      },
-     "execution_count": 21,
+     "execution_count": 12,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -366,7 +366,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 22,
+   "execution_count": 13,
    "metadata": {},
    "outputs": [
     {
@@ -375,7 +375,7 @@
        "False"
       ]
      },
-     "execution_count": 22,
+     "execution_count": 13,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -386,7 +386,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 23,
+   "execution_count": 14,
    "metadata": {},
    "outputs": [
     {
@@ -395,7 +395,7 @@
        "True"
       ]
      },
-     "execution_count": 23,
+     "execution_count": 14,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -413,7 +413,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 24,
+   "execution_count": 15,
    "metadata": {},
    "outputs": [
     {
@@ -425,7 +425,7 @@
        "spot.formula(\"\\\"a > b\\\" & \\\"proc[2]@init\\\" & GF_foo_\")"
       ]
      },
-     "execution_count": 24,
+     "execution_count": 15,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -436,7 +436,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 25,
+   "execution_count": 16,
    "metadata": {},
    "outputs": [
     {
@@ -448,7 +448,7 @@
        "spot.formula(\"a & b & GFc\")"
       ]
      },
-     "execution_count": 25,
+     "execution_count": 16,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -459,7 +459,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 26,
+   "execution_count": 17,
    "metadata": {},
    "outputs": [
     {
@@ -471,7 +471,7 @@
        "spot.formula(\"p0 & p1 & GFp2\")"
       ]
      },
-     "execution_count": 26,
+     "execution_count": 17,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -489,7 +489,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 27,
+   "execution_count": 18,
    "metadata": {},
    "outputs": [
     {
@@ -710,7 +710,7 @@
        "<spot.jupyter.SVG object>"
       ]
      },
-     "execution_count": 27,
+     "execution_count": 18,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -728,7 +728,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 28,
+   "execution_count": 19,
    "metadata": {},
    "outputs": [
     {
@@ -764,7 +764,7 @@
        "<spot.jupyter.SVG object>"
       ]
      },
-     "execution_count": 28,
+     "execution_count": 19,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -775,7 +775,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 29,
+   "execution_count": 20,
    "metadata": {},
    "outputs": [
     {
@@ -784,7 +784,7 @@
        "'recurrence'"
       ]
      },
-     "execution_count": 29,
+     "execution_count": 20,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -795,7 +795,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 30,
+   "execution_count": 21,
    "metadata": {},
    "outputs": [
     {
@@ -807,7 +807,7 @@
        "spot.formula(\"F(a & X(!a & b))\")"
       ]
      },
-     "execution_count": 30,
+     "execution_count": 21,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -825,7 +825,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 31,
+   "execution_count": 22,
    "metadata": {},
    "outputs": [
     {
@@ -837,7 +837,7 @@
        "spot.formula(\"F(a & ((a & (a U (!a & b)) & ((!b U !a) | (b U !a))) | (!a & (!a U (a & !a & b)) & ((!b U a) | (b U a))) | (b & (b U (!a & b & !b)) & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b)) & ((!a U b) | (a U b))) | (!a & b & (G!a | Ga) & (G!b | Gb))))\")"
       ]
      },
-     "execution_count": 31,
+     "execution_count": 22,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -855,7 +855,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 32,
+   "execution_count": 23,
    "metadata": {},
    "outputs": [
     {
@@ -867,7 +867,7 @@
        "spot.formula(\"(0 R !(a <-> b)) -> (1 U (a <-> b))\")"
       ]
      },
-     "execution_count": 32,
+     "execution_count": 23,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -879,7 +879,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 33,
+   "execution_count": 24,
    "metadata": {},
    "outputs": [
     {
@@ -891,7 +891,7 @@
        "spot.formula(\"(1 U ((a & b) | (!a & !b))) | !(0 R ((!a & b) | (a & !b)))\")"
       ]
      },
-     "execution_count": 33,
+     "execution_count": 24,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -909,7 +909,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 34,
+   "execution_count": 25,
    "metadata": {},
    "outputs": [
     {
@@ -945,7 +945,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 35,
+   "execution_count": 26,
    "metadata": {},
    "outputs": [
     {
@@ -980,12 +980,12 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "Converting to Suffix Operator Normal Form:"
+    "Converting to [Suffix Operator Normal Form](https://doi.org/10.1109/TCAD.2008.2003303):"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 36,
+   "execution_count": 27,
    "metadata": {},
    "outputs": [
     {
@@ -1003,10 +1003,10 @@
     {
      "data": {
       "text/latex": [
-       "$\\mathsf{G} \\mathit{sonf\\_}_{0} \\land \\mathsf{G} (\\lnot \\mathit{sonf\\_}_{1} \\lor \\mathsf{F} a) \\land \\mathsf{G} (\\lnot \\mathit{sonf\\_}_{0} \\lor (\\{x^{\\star}\\}\\mathrel{\\Box\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} \\mathit{sonf\\_}_{1}))$"
+       "$\\mathsf{G} p_{0} \\land \\mathsf{G} (\\lnot p_{1} \\lor \\mathsf{F} a) \\land \\mathsf{G} (\\lnot p_{0} \\lor (\\{x^{\\star}\\}\\mathrel{\\Box\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} p_{1}))$"
       ],
       "text/plain": [
-       "spot.formula(\"Gsonf_0 & G(!sonf_1 | Fa) & G(!sonf_0 | ({x[*]}[]-> sonf_1))\")"
+       "spot.formula(\"Gp0 & G(!p1 | Fa) & G(!p0 | ({x[*]}[]-> p1))\")"
       ]
      },
      "metadata": {},
@@ -1015,7 +1015,7 @@
     {
      "data": {
       "text/plain": [
-       "('sonf_0', 'sonf_1')"
+       "('p0', 'p1')"
       ]
      },
      "metadata": {},
@@ -1027,10 +1027,17 @@
     "display(f)\n",
     "\n",
     "# In addition to the formula, returns a list of newly introduced APs\n",
-    "f, aps = spot.suffix_operator_normal_form(f, 'sonf_')\n",
+    "f, aps = spot.suffix_operator_normal_form(f, 'p')\n",
     "display(f)\n",
     "display(aps)"
    ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
   }
  ],
  "metadata": {