diff --git a/wrap/python/tests/automata.ipynb b/wrap/python/tests/automata.ipynb
index 8c6c82c6a..3cca8794b 100644
--- a/wrap/python/tests/automata.ipynb
+++ b/wrap/python/tests/automata.ipynb
@@ -1,7 +1,7 @@
 {
  "metadata": {
   "name": "",
-  "signature": "sha256:46e5472540261241876badd1678f26f98c6708247f2b22d92e76ec7d15136f5c"
+  "signature": "sha256:9b116e5c61ed241183bd5fb9cd5e35010cceb5043c2fab2be81473f829bc528e"
  },
  "nbformat": 3,
  "nbformat_minor": 0,
@@ -12,10 +12,14 @@
      "cell_type": "code",
      "collapsed": false,
      "input": [
-      "import spot\n",
       "import os\n",
-      "os.environ['SPOT_DOTEXTRA'] = 'node[style=filled,fillcolor=\"#ffffaa\"]'\n",
-      "os.environ['SPOT_DOTDEFAULT'] = 'rbc'"
+      "# Note that Spot (loaded by the kernel) will cache a \n",
+      "# pointer to the environment variable the first time it\n",
+      "# reads them.  The Kernel may crash if you attempt to\n",
+      "# modify the variables afterwards.  See issue #63.\n",
+      "os.environ['SPOT_DOTEXTRA'] = 'size=\"11,5\" node[style=filled,fillcolor=\"#ffffaa\"]'\n",
+      "os.environ['SPOT_DOTDEFAULT'] = 'rbcf(Lato)'\n",
+      "import spot"
      ],
      "language": "python",
      "metadata": {},
@@ -34,7 +38,7 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 3,
+       "prompt_number": 2,
        "svg": [
         "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
         "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
@@ -42,16 +46,16 @@
         "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
         " -->\n",
         "<!-- Title: G Pages: 1 -->\n",
-        "<svg width=\"417pt\" height=\"184pt\"\n",
-        " viewBox=\"0.00 0.00 417.00 184.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<svg width=\"419pt\" height=\"184pt\"\n",
+        " viewBox=\"0.00 0.00 419.00 184.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 180)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-180 413,-180 413,4 -4,4\"/>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-180 415,-180 415,4 -4,4\"/>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g id=\"node2\" class=\"node\"><title>0</title>\n",
         "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-69\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"56\" y=\"-65.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-65.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;0 -->\n",
         "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
@@ -62,104 +66,104 @@
         "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
         "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-86.0373C48.3189,-95.8579 50.4453,-105 56,-105 59.4717,-105 61.6042,-101.429 62.3975,-96.3529\"/>\n",
         "<polygon fill=\"black\" stroke=\"black\" points=\"65.8971,-96.031 62.3792,-86.0373 58.8971,-96.0435 65.8971,-96.031\"/>\n",
-        "<text text-anchor=\"start\" x=\"37.5\" y=\"-108.8\" font-family=\"Times,serif\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"37.5\" y=\"-108.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g id=\"node3\" class=\"node\"><title>1</title>\n",
         "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"173\" cy=\"-109\" rx=\"18\" ry=\"18\"/>\n",
         "<ellipse fill=\"none\" stroke=\"black\" cx=\"173\" cy=\"-109\" rx=\"22\" ry=\"22\"/>\n",
-        "<text text-anchor=\"middle\" x=\"173\" y=\"-105.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+        "<text text-anchor=\"middle\" x=\"173\" y=\"-105.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;1 -->\n",
         "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
         "<path fill=\"none\" stroke=\"black\" d=\"M73.4767,-74.731C91.4653,-80.9879 120.631,-91.1325 142.571,-98.7639\"/>\n",
         "<polygon fill=\"black\" stroke=\"black\" points=\"141.482,-102.091 152.077,-102.07 143.782,-95.4793 141.482,-102.091\"/>\n",
-        "<text text-anchor=\"start\" x=\"109\" y=\"-97.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text>\n",
+        "<text text-anchor=\"start\" x=\"108\" y=\"-97.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
         "</g>\n",
         "<!-- 4 -->\n",
         "<g id=\"node4\" class=\"node\"><title>4</title>\n",
         "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"173\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"173\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
+        "<text text-anchor=\"middle\" x=\"173\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;4 -->\n",
         "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;4</title>\n",
         "<path fill=\"none\" stroke=\"black\" d=\"M72.9903,-61.9087C92.1291,-53.421 124.406,-39.107 146.884,-29.1383\"/>\n",
         "<polygon fill=\"black\" stroke=\"black\" points=\"148.423,-32.2847 156.146,-25.0311 145.585,-25.8857 148.423,-32.2847\"/>\n",
-        "<text text-anchor=\"start\" x=\"92\" y=\"-55.8\" font-family=\"Times,serif\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"92\" y=\"-55.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;1 -->\n",
         "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
         "<path fill=\"none\" stroke=\"black\" d=\"M162.933,-128.757C161.223,-139.35 164.578,-149 173,-149 178.527,-149 181.872,-144.844 183.035,-138.993\"/>\n",
         "<polygon fill=\"black\" stroke=\"black\" points=\"186.536,-138.768 183.067,-128.757 179.536,-138.747 186.536,-138.768\"/>\n",
-        "<text text-anchor=\"start\" x=\"157\" y=\"-152.8\" font-family=\"Times,serif\" font-size=\"14.00\">c &amp; d</text>\n",
+        "<text text-anchor=\"start\" x=\"156\" y=\"-152.8\" font-family=\"Lato\" font-size=\"14.00\">c &amp; d</text>\n",
         "</g>\n",
         "<!-- 2 -->\n",
         "<g id=\"node5\" class=\"node\"><title>2</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"391\" cy=\"-99\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"391\" y=\"-95.3\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"393\" cy=\"-99\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"393\" y=\"-95.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;2 -->\n",
         "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M190.397,-123.162C214.143,-141.898 259.681,-171.208 300,-159 326.567,-150.956 352.459,-132.198 369.599,-117.781\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"372.017,-120.316 377.274,-111.117 367.428,-115.03 372.017,-120.316\"/>\n",
-        "<text text-anchor=\"start\" x=\"263\" y=\"-164.8\" font-family=\"Times,serif\" font-size=\"14.00\">!c &amp; d</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M190.278,-122.894C214.315,-141.67 260.899,-171.444 302,-159 328.567,-150.956 354.459,-132.198 371.599,-117.781\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"374.017,-120.316 379.274,-111.117 369.428,-115.03 374.017,-120.316\"/>\n",
+        "<text text-anchor=\"start\" x=\"265\" y=\"-164.8\" font-family=\"Lato\" font-size=\"14.00\">!c &amp; d</text>\n",
         "</g>\n",
         "<!-- 3 -->\n",
         "<g id=\"node6\" class=\"node\"><title>3</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"281.5\" cy=\"-99\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"281.5\" y=\"-95.3\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"283.5\" cy=\"-99\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"283.5\" y=\"-95.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;3 -->\n",
         "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M195.193,-108.948C209.342,-108.706 228.339,-107.983 245,-106 247.77,-105.67 250.647,-105.244 253.511,-104.766\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"254.424,-108.156 263.61,-102.877 253.137,-101.275 254.424,-108.156\"/>\n",
-        "<text text-anchor=\"start\" x=\"223\" y=\"-111.8\" font-family=\"Times,serif\" font-size=\"14.00\">!d</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M195.152,-108.988C209.762,-108.77 229.617,-108.059 247,-106 249.77,-105.672 252.647,-105.247 255.511,-104.769\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"256.424,-108.159 265.61,-102.881 255.137,-101.278 256.424,-108.159\"/>\n",
+        "<text text-anchor=\"start\" x=\"223.5\" y=\"-111.8\" font-family=\"Lato\" font-size=\"14.00\">!d</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;4 -->\n",
         "<g id=\"edge13\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
         "<path fill=\"none\" stroke=\"black\" d=\"M163.425,-33.5414C160.73,-43.9087 163.922,-54 173,-54 178.958,-54 182.38,-49.654 183.267,-43.7362\"/>\n",
         "<polygon fill=\"black\" stroke=\"black\" points=\"186.744,-43.2812 182.575,-33.5414 179.76,-43.7557 186.744,-43.2812\"/>\n",
-        "<text text-anchor=\"middle\" x=\"173\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+        "<text text-anchor=\"middle\" x=\"173\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;1 -->\n",
         "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M375.779,-88.9002C352.56,-73.6457 304.892,-47.4667 263,-57 239.225,-62.4104 215.547,-76.7915 198.597,-89.0618\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"196.279,-86.4254 190.382,-95.2273 200.481,-92.0241 196.279,-86.4254\"/>\n",
-        "<text text-anchor=\"start\" x=\"278\" y=\"-60.8\" font-family=\"Times,serif\" font-size=\"14.00\">c</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M377.812,-89.0507C354.64,-74.0075 307.035,-48.1189 265,-57 240.592,-62.157 216.227,-76.7048 198.86,-89.1057\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"196.405,-86.5688 190.453,-95.3338 200.571,-92.1936 196.405,-86.5688\"/>\n",
+        "<text text-anchor=\"start\" x=\"280\" y=\"-60.8\" font-family=\"Lato\" font-size=\"14.00\">c</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
         "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M381.767,-114.541C379.169,-124.909 382.246,-135 391,-135 396.745,-135 400.045,-130.654 400.9,-124.736\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"404.379,-124.291 400.233,-114.541 397.394,-124.749 404.379,-124.291\"/>\n",
-        "<text text-anchor=\"start\" x=\"385.5\" y=\"-138.8\" font-family=\"Times,serif\" font-size=\"14.00\">!c</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M383.767,-114.541C381.169,-124.909 384.246,-135 393,-135 398.745,-135 402.045,-130.654 402.9,-124.736\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"406.379,-124.291 402.233,-114.541 399.394,-124.749 406.379,-124.291\"/>\n",
+        "<text text-anchor=\"start\" x=\"387.5\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\">!c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;1 -->\n",
         "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M264.522,-92.2959C250.744,-87.4303 230.383,-82.4351 213,-87 208.771,-88.1106 204.517,-89.7954 200.454,-91.7483\"/>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M266.525,-92.366C260.514,-90.2005 253.548,-88.0768 247,-87 232.089,-84.548 227.616,-83.1619 213,-87 208.771,-88.1106 204.517,-89.7954 200.454,-91.7483\"/>\n",
         "<polygon fill=\"black\" stroke=\"black\" points=\"198.542,-88.8035 191.42,-96.6478 201.879,-94.9568 198.542,-88.8035\"/>\n",
-        "<text text-anchor=\"start\" x=\"213\" y=\"-90.8\" font-family=\"Times,serif\" font-size=\"14.00\">c &amp; d</text>\n",
+        "<text text-anchor=\"start\" x=\"213\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">c &amp; d</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;2 -->\n",
         "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M299.772,-99C316.698,-99 342.762,-99 362.533,-99\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"362.771,-102.5 372.771,-99 362.771,-95.5001 362.771,-102.5\"/>\n",
-        "<text text-anchor=\"start\" x=\"318\" y=\"-102.8\" font-family=\"Times,serif\" font-size=\"14.00\">!c &amp; d</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M301.772,-99C318.698,-99 344.762,-99 364.533,-99\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"364.771,-102.5 374.771,-99 364.771,-95.5001 364.771,-102.5\"/>\n",
+        "<text text-anchor=\"start\" x=\"320\" y=\"-102.8\" font-family=\"Lato\" font-size=\"14.00\">!c &amp; d</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;3 -->\n",
         "<g id=\"edge12\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M272.521,-114.916C270.179,-125.15 273.172,-135 281.5,-135 286.965,-135 290.133,-130.758 291.003,-124.949\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"294.496,-124.72 290.479,-114.916 287.505,-125.085 294.496,-124.72\"/>\n",
-        "<text text-anchor=\"start\" x=\"275.5\" y=\"-138.8\" font-family=\"Times,serif\" font-size=\"14.00\">!d</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M274.521,-114.916C272.179,-125.15 275.172,-135 283.5,-135 288.965,-135 292.133,-130.758 293.003,-124.949\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"296.496,-124.72 292.479,-114.916 289.505,-125.085 296.496,-124.72\"/>\n",
+        "<text text-anchor=\"start\" x=\"277\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\">!d</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f7be0d392d0> >"
+        "<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f17fc124150> >"
        ]
       }
      ],
-     "prompt_number": 3
+     "prompt_number": 2
     },
     {
      "cell_type": "code",
@@ -173,7 +177,7 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 4,
+       "prompt_number": 3,
        "svg": [
         "<svg height=\"186pt\" viewBox=\"0.00 0.00 488.00 186.00\" width=\"488pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
         "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 182)\">\n",
@@ -287,11 +291,11 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f7be5375860>"
+        "<IPython.core.display.SVG at 0x7f17fff640f0>"
        ]
       }
      ],
-     "prompt_number": 4
+     "prompt_number": 3
     },
     {
      "cell_type": "code",
@@ -305,17 +309,17 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 5,
+       "prompt_number": 4,
        "svg": [
-        "<svg height=\"342pt\" viewBox=\"0.00 0.00 425.00 342.00\" width=\"425pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<svg height=\"342pt\" viewBox=\"0.00 0.00 427.00 342.00\" width=\"427pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
         "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 338)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-338 421,-338 421,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"190\" y=\"-319.8\">Inf(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"211\" y=\"-319.8\">\u24ff</text>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"222\" y=\"-319.8\">)</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-338 423,-338 423,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"188.5\" y=\"-319.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"210.5\" y=\"-319.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"226.5\" y=\"-319.8\">)</text>\n",
         "<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
-        "<polygon fill=\"none\" points=\"143,-101 143,-303 409,-303 409,-101 143,-101\" stroke=\"green\"/>\n",
+        "<polygon fill=\"none\" points=\"143,-101 143,-303 411,-303 411,-101 143,-101\" stroke=\"green\"/>\n",
         "</g>\n",
         "<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
         "<polygon fill=\"none\" points=\"143,-8 143,-93 195,-93 195,-8 143,-8\" stroke=\"grey\"/>\n",
@@ -327,7 +331,7 @@
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node2\"><title>0</title>\n",
         "<ellipse cx=\"56\" cy=\"-44\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-40.3\">0</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-40.3\">0</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
@@ -338,106 +342,106 @@
         "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
         "<path d=\"M49.6208,-61.0373C48.3189,-70.8579 50.4453,-80 56,-80 59.4717,-80 61.6042,-76.4289 62.3975,-71.3529\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"65.8971,-71.031 62.3792,-61.0373 58.8971,-71.0435 65.8971,-71.031\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"37.5\" y=\"-83.8\">a &amp; !b</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"37.5\" y=\"-83.8\">a &amp; !b</text>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g class=\"node\" id=\"node3\"><title>1</title>\n",
         "<ellipse cx=\"169\" cy=\"-151\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-147.3\">1</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-147.3\">1</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
         "<path d=\"M69.7331,-56.2743C88.8864,-74.7373 125.282,-109.821 148.001,-131.721\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"145.787,-134.449 155.415,-138.869 150.645,-129.409 145.787,-134.449\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"109\" y=\"-120.8\">b</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"108\" y=\"-120.8\">b</text>\n",
         "</g>\n",
         "<!-- 4 -->\n",
         "<g class=\"node\" id=\"node6\"><title>4</title>\n",
         "<ellipse cx=\"169\" cy=\"-34\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-30.3\">4</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-30.3\">4</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge4\"><title>0-&gt;4</title>\n",
         "<path d=\"M74.3438,-42.4375C92.1015,-40.8377 119.96,-38.3279 140.683,-36.461\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"141.132,-39.9348 150.778,-35.5515 140.504,-32.963 141.132,-39.9348\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-44.8\">!a &amp; !b</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-44.8\">!a &amp; !b</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
         "<path d=\"M160.021,-166.916C157.679,-177.15 160.672,-187 169,-187 174.465,-187 177.633,-182.758 178.503,-176.949\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"181.996,-176.72 177.979,-166.916 175.005,-177.085 181.996,-176.72\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"153\" y=\"-205.8\">c &amp; d</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"163.5\" y=\"-190.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"152\" y=\"-205.8\">c &amp; d</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"161\" y=\"-190.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 3 -->\n",
         "<g class=\"node\" id=\"node4\"><title>3</title>\n",
-        "<ellipse cx=\"273.5\" cy=\"-193\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"273.5\" y=\"-189.3\">3</text>\n",
+        "<ellipse cx=\"275.5\" cy=\"-193\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"275.5\" y=\"-189.3\">3</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge7\"><title>1-&gt;3</title>\n",
-        "<path d=\"M186.813,-147.582C200.899,-145.553 221.183,-144.63 237,-152 245.041,-155.747 251.972,-162.289 257.52,-169.062\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"255.04,-171.596 263.789,-177.571 260.676,-167.444 255.04,-171.596\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"215\" y=\"-170.8\">!d</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"215.5\" y=\"-155.8\">\u24ff</text>\n",
+        "<path d=\"M186.737,-147.555C201.262,-145.401 222.492,-144.312 239,-152 247.042,-155.745 253.973,-162.287 259.521,-169.06\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"257.041,-171.594 265.79,-177.569 262.677,-167.442 257.041,-171.594\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"215.5\" y=\"-170.8\">!d</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"214\" y=\"-155.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 2 -->\n",
         "<g class=\"node\" id=\"node5\"><title>2</title>\n",
-        "<ellipse cx=\"383\" cy=\"-193\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"383\" y=\"-189.3\">2</text>\n",
+        "<ellipse cx=\"385\" cy=\"-193\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"385\" y=\"-189.3\">2</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge6\"><title>1-&gt;2</title>\n",
-        "<path d=\"M186.119,-144.99C209.781,-137.063 255.108,-125.3 292,-136 318.017,-143.546 343.725,-161.116 360.96,-174.769\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"359.202,-177.854 369.158,-181.479 363.636,-172.437 359.202,-177.854\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"255\" y=\"-154.8\">!c &amp; d</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"268\" y=\"-139.8\">\u24ff</text>\n",
+        "<path d=\"M186.385,-144.944C210.438,-136.96 256.512,-125.127 294,-136 320.017,-143.546 345.725,-161.116 362.96,-174.769\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"361.202,-177.854 371.158,-181.479 365.636,-172.437 361.202,-177.854\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"257\" y=\"-154.8\">!c &amp; d</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"267.5\" y=\"-139.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge10\"><title>3-&gt;1</title>\n",
-        "<path d=\"M255.357,-192.817C241.226,-192.068 220.982,-189.587 205,-182 199.269,-179.279 193.775,-175.331 188.908,-171.157\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"191.066,-168.383 181.376,-164.098 186.279,-173.491 191.066,-168.383\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"205\" y=\"-194.8\">c &amp; d</text>\n",
+        "<path d=\"M257.435,-192.94C242.865,-192.285 221.682,-189.872 205,-182 199.263,-179.293 193.766,-175.349 188.899,-171.176\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"191.057,-168.402 181.368,-164.115 186.269,-173.508 191.057,-168.402\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"205\" y=\"-195.8\">c &amp; d</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
-        "<path d=\"M264.521,-208.916C262.179,-219.15 265.172,-229 273.5,-229 278.965,-229 282.133,-224.758 283.003,-218.949\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"286.496,-218.72 282.479,-208.916 279.505,-219.085 286.496,-218.72\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"267.5\" y=\"-232.8\">!d</text>\n",
+        "<path d=\"M266.521,-208.916C264.179,-219.15 267.172,-229 275.5,-229 280.965,-229 284.133,-224.758 285.003,-218.949\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"288.496,-218.72 284.479,-208.916 281.505,-219.085 288.496,-218.72\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"269\" y=\"-232.8\">!d</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge11\"><title>3-&gt;2</title>\n",
-        "<path d=\"M291.772,-193C308.698,-193 334.762,-193 354.533,-193\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"354.771,-196.5 364.771,-193 354.771,-189.5 354.771,-196.5\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"310\" y=\"-196.8\">!c &amp; d</text>\n",
+        "<path d=\"M293.772,-193C310.698,-193 336.762,-193 356.533,-193\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"356.771,-196.5 366.771,-193 356.771,-189.5 356.771,-196.5\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"312\" y=\"-196.8\">!c &amp; d</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge8\"><title>2-&gt;1</title>\n",
-        "<path d=\"M370.041,-205.772C347.871,-227.825 298.67,-269.195 255,-253 219.738,-239.923 194.897,-202.083 181.517,-176.357\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"184.535,-174.566 176.952,-167.167 178.266,-177.68 184.535,-174.566\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"270\" y=\"-259.8\">c</text>\n",
+        "<path d=\"M372.089,-205.642C349.996,-227.482 300.914,-268.52 257,-253 221.196,-240.347 195.691,-202.391 181.901,-176.524\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"184.85,-174.602 177.192,-167.28 178.613,-177.779 184.85,-174.602\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"272\" y=\"-259.8\">c</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge9\"><title>2-&gt;2</title>\n",
-        "<path d=\"M373.767,-208.541C371.169,-218.909 374.246,-229 383,-229 388.745,-229 392.045,-224.654 392.9,-218.736\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"396.379,-218.291 392.233,-208.541 389.394,-218.749 396.379,-218.291\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"377.5\" y=\"-232.8\">!c</text>\n",
+        "<path d=\"M375.767,-208.541C373.169,-218.909 376.246,-229 385,-229 390.745,-229 394.045,-224.654 394.9,-218.736\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"398.379,-218.291 394.233,-208.541 391.394,-218.749 398.379,-218.291\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"379.5\" y=\"-232.8\">!c</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge13\"><title>4-&gt;4</title>\n",
         "<path d=\"M160.021,-49.916C157.679,-60.1504 160.672,-70 169,-70 174.465,-70 177.633,-65.7581 178.503,-59.9494\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"181.996,-59.7198 177.979,-49.916 175.005,-60.0851 181.996,-59.7198\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-73.8\">1</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-73.8\">1</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f7be0058ef0>"
+        "<IPython.core.display.SVG at 0x7f17fc047f60>"
        ]
       }
      ],
-     "prompt_number": 5
+     "prompt_number": 4
     },
     {
      "cell_type": "code",
@@ -454,19 +458,89 @@
        ],
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 6,
+       "prompt_number": 5,
        "text": [
         "a U b"
        ]
       }
      ],
+     "prompt_number": 5
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "spot.translate(f)"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "pyout",
+       "prompt_number": 6,
+       "svg": [
+        "<?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.38.0 (20140413.2041)\n",
+        " -->\n",
+        "<!-- Title: G Pages: 1 -->\n",
+        "<svg width=\"171pt\" height=\"85pt\"\n",
+        " viewBox=\"0.00 0.00 171.00 85.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 81)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 167,-81 167,4 -4,4\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 1 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;1 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.67247,-22 15.0966,-22 27.6277,-22\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"27.9419,-25.5001 37.9419,-22 27.9418,-18.5001 27.9419,-25.5001\"/>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 59.4717,-58 61.6042,-54.4289 62.3975,-49.3529\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"65.8971,-49.031 62.3792,-39.0373 58.8971,-49.0435 65.8971,-49.031\"/>\n",
+        "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
+        "<ellipse fill=\"none\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
+        "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M74.1977,-22C84.1587,-22 97.0038,-22 108.697,-22\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"108.997,-25.5001 118.997,-22 108.997,-18.5001 108.997,-25.5001\"/>\n",
+        "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M132.994,-42.5808C131.886,-52.8447 134.555,-62 141,-62 145.129,-62 147.708,-58.2427 148.737,-52.8436\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"152.243,-52.6691 149.006,-42.5808 145.245,-52.4857 152.243,-52.6691\"/>\n",
+        "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>\n"
+       ],
+       "text": [
+        "<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f17fc0fb930> >"
+       ]
+      }
+     ],
      "prompt_number": 6
     },
     {
      "cell_type": "code",
      "collapsed": false,
      "input": [
-      "spot.translate(f)"
+      "f.translate()"
      ],
      "language": "python",
      "metadata": {},
@@ -482,16 +556,16 @@
         "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
         " -->\n",
         "<!-- Title: G Pages: 1 -->\n",
-        "<svg width=\"169pt\" height=\"85pt\"\n",
-        " viewBox=\"0.00 0.00 169.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<svg width=\"171pt\" height=\"85pt\"\n",
+        " viewBox=\"0.00 0.00 171.00 85.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 81)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 165,-81 165,4 -4,4\"/>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 167,-81 167,4 -4,4\"/>\n",
         "<!-- I -->\n",
         "<!-- 1 -->\n",
         "<g id=\"node2\" class=\"node\"><title>1</title>\n",
         "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;1 -->\n",
         "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
@@ -502,31 +576,31 @@
         "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
         "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 59.4717,-58 61.6042,-54.4289 62.3975,-49.3529\"/>\n",
         "<polygon fill=\"black\" stroke=\"black\" points=\"65.8971,-49.031 62.3792,-39.0373 58.8971,-49.0435 65.8971,-49.031\"/>\n",
-        "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Times,serif\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
         "</g>\n",
         "<!-- 0 -->\n",
         "<g id=\"node3\" class=\"node\"><title>0</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"139\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
-        "<ellipse fill=\"none\" stroke=\"black\" cx=\"139\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
-        "<text text-anchor=\"middle\" x=\"139\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
+        "<ellipse fill=\"none\" stroke=\"black\" cx=\"141\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
+        "<text text-anchor=\"middle\" x=\"141\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;0 -->\n",
         "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M74.178,-22C83.6095,-22 95.6007,-22 106.637,-22\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"106.811,-25.5001 116.811,-22 106.811,-18.5001 106.811,-25.5001\"/>\n",
-        "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M74.1977,-22C84.1587,-22 97.0038,-22 108.697,-22\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"108.997,-25.5001 118.997,-22 108.997,-18.5001 108.997,-25.5001\"/>\n",
+        "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
         "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M131.317,-42.9908C130.369,-53.0872 132.93,-62 139,-62 142.889,-62 145.337,-58.3422 146.346,-53.0587\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"149.846,-53.1023 146.683,-42.9908 142.85,-52.868 149.846,-53.1023\"/>\n",
-        "<text text-anchor=\"middle\" x=\"139\" y=\"-65.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M132.994,-42.5808C131.886,-52.8447 134.555,-62 141,-62 145.129,-62 147.708,-58.2427 148.737,-52.8436\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"152.243,-52.6691 149.006,-42.5808 145.245,-52.4857 152.243,-52.6691\"/>\n",
+        "<text text-anchor=\"middle\" x=\"141\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f7be0d10930> >"
+        "<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f17fc0fbb70> >"
        ]
       }
      ],
@@ -536,7 +610,7 @@
      "cell_type": "code",
      "collapsed": false,
      "input": [
-      "f.translate()"
+      "f.translate('mon')"
      ],
      "language": "python",
      "metadata": {},
@@ -552,86 +626,16 @@
         "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
         " -->\n",
         "<!-- Title: G Pages: 1 -->\n",
-        "<svg width=\"169pt\" height=\"85pt\"\n",
-        " viewBox=\"0.00 0.00 169.00 85.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 81)\">\n",
-        "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 165,-81 165,4 -4,4\"/>\n",
-        "<!-- I -->\n",
-        "<!-- 1 -->\n",
-        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
-        "</g>\n",
-        "<!-- I&#45;&gt;1 -->\n",
-        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.67247,-22 15.0966,-22 27.6277,-22\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"27.9419,-25.5001 37.9419,-22 27.9418,-18.5001 27.9419,-25.5001\"/>\n",
-        "</g>\n",
-        "<!-- 1&#45;&gt;1 -->\n",
-        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 59.4717,-58 61.6042,-54.4289 62.3975,-49.3529\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"65.8971,-49.031 62.3792,-39.0373 58.8971,-49.0435 65.8971,-49.031\"/>\n",
-        "<text text-anchor=\"start\" x=\"37.5\" y=\"-61.8\" font-family=\"Times,serif\" font-size=\"14.00\">a &amp; !b</text>\n",
-        "</g>\n",
-        "<!-- 0 -->\n",
-        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"139\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
-        "<ellipse fill=\"none\" stroke=\"black\" cx=\"139\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
-        "<text text-anchor=\"middle\" x=\"139\" y=\"-18.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
-        "</g>\n",
-        "<!-- 1&#45;&gt;0 -->\n",
-        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M74.178,-22C83.6095,-22 95.6007,-22 106.637,-22\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"106.811,-25.5001 116.811,-22 106.811,-18.5001 106.811,-25.5001\"/>\n",
-        "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text>\n",
-        "</g>\n",
-        "<!-- 0&#45;&gt;0 -->\n",
-        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M131.317,-42.9908C130.369,-53.0872 132.93,-62 139,-62 142.889,-62 145.337,-58.3422 146.346,-53.0587\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"149.846,-53.1023 146.683,-42.9908 142.85,-52.868 149.846,-53.1023\"/>\n",
-        "<text text-anchor=\"middle\" x=\"139\" y=\"-65.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
-        "</g>\n",
-        "</g>\n",
-        "</svg>\n"
-       ],
-       "text": [
-        "<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f7be0d10b70> >"
-       ]
-      }
-     ],
-     "prompt_number": 8
-    },
-    {
-     "cell_type": "code",
-     "collapsed": false,
-     "input": [
-      "f.translate('mon')"
-     ],
-     "language": "python",
-     "metadata": {},
-     "outputs": [
-      {
-       "metadata": {},
-       "output_type": "pyout",
-       "prompt_number": 9,
-       "svg": [
-        "<?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.38.0 (20140413.2041)\n",
-        " -->\n",
-        "<!-- Title: G Pages: 1 -->\n",
-        "<svg width=\"161pt\" height=\"77pt\"\n",
-        " viewBox=\"0.00 0.00 161.00 77.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<svg width=\"163pt\" height=\"77pt\"\n",
+        " viewBox=\"0.00 0.00 163.00 77.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 73)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-73 157,-73 157,4 -4,4\"/>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-73 159,-73 159,4 -4,4\"/>\n",
         "<!-- I -->\n",
         "<!-- 1 -->\n",
         "<g id=\"node2\" class=\"node\"><title>1</title>\n",
         "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;1 -->\n",
         "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
@@ -642,34 +646,34 @@
         "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
         "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-35.0373C48.3189,-44.8579 50.4453,-54 56,-54 59.4717,-54 61.6042,-50.4289 62.3975,-45.3529\"/>\n",
         "<polygon fill=\"black\" stroke=\"black\" points=\"65.8971,-45.031 62.3792,-35.0373 58.8971,-45.0435 65.8971,-45.031\"/>\n",
-        "<text text-anchor=\"start\" x=\"37.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"37.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
         "</g>\n",
         "<!-- 0 -->\n",
         "<g id=\"node3\" class=\"node\"><title>0</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"135\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"135\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"137\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;0 -->\n",
         "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M74.0888,-18C83.659,-18 95.8172,-18 106.677,-18\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"106.959,-21.5001 116.959,-18 106.959,-14.5001 106.959,-21.5001\"/>\n",
-        "<text text-anchor=\"start\" x=\"92\" y=\"-21.8\" font-family=\"Times,serif\" font-size=\"14.00\">b</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M74.1418,-18C84.2871,-18 97.3664,-18 108.883,-18\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"108.892,-21.5001 118.892,-18 108.892,-14.5001 108.892,-21.5001\"/>\n",
+        "<text text-anchor=\"start\" x=\"92\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
         "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M128.266,-35.0373C126.892,-44.8579 129.137,-54 135,-54 138.665,-54 140.916,-50.4289 141.753,-45.3529\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"145.252,-45.0307 141.734,-35.0373 138.252,-45.0439 145.252,-45.0307\"/>\n",
-        "<text text-anchor=\"middle\" x=\"135\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M129.969,-34.6641C128.406,-44.625 130.75,-54 137,-54 141.004,-54 143.405,-50.1525 144.202,-44.7682\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"147.7,-44.6033 144.031,-34.6641 140.701,-44.7219 147.7,-44.6033\"/>\n",
+        "<text text-anchor=\"middle\" x=\"137\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f7be0d10ae0> >"
+        "<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f17fc0fb990> >"
        ]
       }
      ],
-     "prompt_number": 9
+     "prompt_number": 8
     },
     {
      "cell_type": "code",
@@ -686,13 +690,13 @@
        ],
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 10,
+       "prompt_number": 9,
        "text": [
         "Ga | Gb | Gc"
        ]
       }
      ],
-     "prompt_number": 10
+     "prompt_number": 9
     },
     {
      "cell_type": "code",
@@ -706,7 +710,7 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 11,
+       "prompt_number": 10,
        "svg": [
         "<svg height=\"177pt\" viewBox=\"0.00 0.00 305.00 177.00\" width=\"305pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
         "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 173)\">\n",
@@ -781,11 +785,11 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f7bcacc95c0>"
+        "<IPython.core.display.SVG at 0x7f17ed8c7b38>"
        ]
       }
      ],
-     "prompt_number": 11
+     "prompt_number": 10
     },
     {
      "cell_type": "code",
@@ -799,179 +803,272 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 12,
+       "prompt_number": 11,
        "svg": [
-        "<svg height=\"280pt\" viewBox=\"0.00 0.00 591.82 280.00\" width=\"592pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<svg height=\"280pt\" viewBox=\"0.00 0.00 596.84 280.00\" width=\"597pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
         "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 276)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-276 587.821,-276 587.821,4 -4,4\" stroke=\"none\"/>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-276 592.84,-276 592.84,4 -4,4\" stroke=\"none\"/>\n",
         "<!-- I -->\n",
         "<!-- 6 -->\n",
         "<g class=\"node\" id=\"node2\"><title>6</title>\n",
-        "<ellipse cx=\"277.821\" cy=\"-212\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"277.821\" cy=\"-212\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"277.821\" y=\"-208.3\">6</text>\n",
+        "<ellipse cx=\"279.84\" cy=\"-212\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<ellipse cx=\"279.84\" cy=\"-212\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"279.84\" y=\"-208.3\">6</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;6 -->\n",
         "<g class=\"edge\" id=\"edge1\"><title>I-&gt;6</title>\n",
-        "<path d=\"M277.821,-270.834C277.821,-269.282 277.821,-257.111 277.821,-244.332\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"281.321,-244.144 277.821,-234.144 274.321,-244.144 281.321,-244.144\" stroke=\"black\"/>\n",
+        "<path d=\"M279.84,-270.834C279.84,-269.282 279.84,-257.111 279.84,-244.332\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"283.34,-244.144 279.84,-234.144 276.34,-244.144 283.34,-244.144\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 6&#45;&gt;6 -->\n",
         "<g class=\"edge\" id=\"edge20\"><title>6-&gt;6</title>\n",
-        "<path d=\"M298.811,-219.317C308.908,-220.22 317.821,-217.781 317.821,-212 317.821,-208.296 314.163,-205.964 308.879,-205.004\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"308.918,-201.504 298.811,-204.683 308.695,-208.5 308.918,-201.504\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"317.821\" y=\"-208.3\">a &amp; b &amp; c</text>\n",
+        "<path d=\"M300.831,-219.317C310.927,-220.22 319.84,-217.781 319.84,-212 319.84,-208.296 316.182,-205.964 310.899,-205.004\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"310.937,-201.504 300.831,-204.683 310.714,-208.5 310.937,-201.504\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"319.84\" y=\"-208.3\">a &amp; b &amp; c</text>\n",
         "</g>\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node3\"><title>0</title>\n",
-        "<ellipse cx=\"96.8206\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"96.8206\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"96.8206\" y=\"-18.3\">0</text>\n",
+        "<ellipse cx=\"98.8401\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<ellipse cx=\"98.8401\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"98.8401\" y=\"-18.3\">0</text>\n",
         "</g>\n",
         "<!-- 6&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge14\"><title>6-&gt;0</title>\n",
-        "<path d=\"M255.721,-208.524C196.826,-201.426 38.4848,-178.913 7.82057,-139 -19.6942,-103.186 34.0271,-61.1222 69.3557,-38.795\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"71.1909,-41.7753 77.8807,-33.5596 67.5277,-35.8104 71.1909,-41.7753\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"7.82057\" y=\"-113.3\">!a &amp; !b &amp; c</text>\n",
+        "<path d=\"M258.007,-208.601C199.023,-201.628 38.8277,-179.258 7.8401,-139 -20.0104,-102.818 35.1362,-60.7371 71.1365,-38.5459\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.0339,-41.4892 79.8144,-33.3483 69.437,-35.484 73.0339,-41.4892\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"7.8401\" y=\"-113.3\">!a &amp; !b &amp; c</text>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g class=\"node\" id=\"node4\"><title>1</title>\n",
-        "<ellipse cx=\"323.821\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"323.821\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"323.821\" y=\"-18.3\">1</text>\n",
+        "<ellipse cx=\"326.84\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<ellipse cx=\"326.84\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"326.84\" y=\"-18.3\">1</text>\n",
         "</g>\n",
         "<!-- 6&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge15\"><title>6-&gt;1</title>\n",
-        "<path d=\"M293.596,-196.107C299.73,-189.363 306.154,-180.909 309.821,-172 325.565,-133.743 327.14,-85.434 326.081,-54.3777\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"329.567,-53.9873 325.615,-44.1569 322.574,-54.3058 329.567,-53.9873\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"324.821\" y=\"-113.3\">!a &amp; b &amp; !c</text>\n",
+        "<path d=\"M295.763,-196.555C302.193,-189.767 308.99,-181.157 312.84,-172 328.873,-133.863 330.378,-85.5249 329.224,-54.4292\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"332.708,-54.0118 328.725,-44.1943 325.716,-54.353 332.708,-54.0118\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"327.84\" y=\"-113.3\">!a &amp; b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 2 -->\n",
         "<g class=\"node\" id=\"node5\"><title>2</title>\n",
-        "<ellipse cx=\"475.821\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"475.821\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"475.821\" y=\"-18.3\">2</text>\n",
+        "<ellipse cx=\"478.84\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<ellipse cx=\"478.84\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"478.84\" y=\"-18.3\">2</text>\n",
         "</g>\n",
         "<!-- 6&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge16\"><title>6-&gt;2</title>\n",
-        "<path d=\"M299.754,-207.718C353.012,-199.238 486.572,-174.735 510.821,-139 529.65,-111.25 511.455,-73.0765 495.046,-48.2235\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"497.724,-45.9426 489.153,-39.7138 491.969,-49.9277 497.724,-45.9426\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"517.821\" y=\"-113.3\">a &amp; !b &amp; !c</text>\n",
+        "<path d=\"M301.646,-207.819C355.288,-199.487 491.1,-175.144 515.84,-139 534.958,-111.069 515.686,-72.6972 498.568,-47.8724\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"501.358,-45.7581 492.669,-39.6958 495.681,-49.8535 501.358,-45.7581\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"522.84\" y=\"-113.3\">a &amp; !b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 3 -->\n",
         "<g class=\"node\" id=\"node6\"><title>3</title>\n",
-        "<ellipse cx=\"104.821\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"104.821\" cy=\"-117\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"104.821\" y=\"-113.3\">3</text>\n",
+        "<ellipse cx=\"104.84\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<ellipse cx=\"104.84\" cy=\"-117\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"104.84\" y=\"-113.3\">3</text>\n",
         "</g>\n",
         "<!-- 6&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge17\"><title>6-&gt;3</title>\n",
-        "<path d=\"M256.67,-205.151C235.049,-198.702 200.895,-187.194 173.821,-172 157.607,-162.901 141.147,-150.181 128.371,-139.372\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"130.4,-136.498 120.548,-132.602 125.819,-141.792 130.4,-136.498\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"173.821\" y=\"-160.8\">!a &amp; b &amp; c</text>\n",
+        "<path d=\"M258.504,-205.147C236.691,-198.695 202.22,-187.184 174.84,-172 158.434,-162.901 141.737,-150.181 128.767,-139.372\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"130.704,-136.424 120.822,-132.602 126.164,-141.752 130.704,-136.424\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"174.84\" y=\"-160.8\">!a &amp; b &amp; c</text>\n",
         "</g>\n",
         "<!-- 4 -->\n",
         "<g class=\"node\" id=\"node7\"><title>4</title>\n",
-        "<ellipse cx=\"429.821\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"429.821\" cy=\"-117\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"429.821\" y=\"-113.3\">4</text>\n",
+        "<ellipse cx=\"432.84\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<ellipse cx=\"432.84\" cy=\"-117\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"432.84\" y=\"-113.3\">4</text>\n",
         "</g>\n",
         "<!-- 6&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge18\"><title>6-&gt;4</title>\n",
-        "<path d=\"M296.155,-199.782C322.631,-183.583 371.758,-153.525 402.512,-134.709\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"404.717,-137.462 411.421,-129.258 401.064,-131.491 404.717,-137.462\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"362.821\" y=\"-160.8\">a &amp; b &amp; !c</text>\n",
+        "<path d=\"M298.295,-199.782C325.061,-183.513 374.823,-153.266 405.751,-134.466\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"407.592,-137.443 414.319,-129.258 403.956,-131.461 407.592,-137.443\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"364.84\" y=\"-160.8\">a &amp; b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 5 -->\n",
         "<g class=\"node\" id=\"node8\"><title>5</title>\n",
-        "<ellipse cx=\"216.821\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"216.821\" cy=\"-117\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"216.821\" y=\"-113.3\">5</text>\n",
+        "<ellipse cx=\"218.84\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<ellipse cx=\"218.84\" cy=\"-117\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"218.84\" y=\"-113.3\">5</text>\n",
         "</g>\n",
         "<!-- 6&#45;&gt;5 -->\n",
         "<g class=\"edge\" id=\"edge19\"><title>6-&gt;5</title>\n",
-        "<path d=\"M264.723,-194.191C259.599,-187.412 253.776,-179.446 248.821,-172 243.19,-163.539 237.415,-154.075 232.347,-145.463\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"235.215,-143.431 227.167,-136.54 229.161,-146.945 235.215,-143.431\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"248.821\" y=\"-160.8\">a &amp; !b &amp; c</text>\n",
+        "<path d=\"M266.742,-194.191C261.619,-187.412 255.795,-179.446 250.84,-172 245.209,-163.539 239.434,-154.075 234.367,-145.463\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"237.234,-143.431 229.187,-136.54 231.18,-146.945 237.234,-143.431\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"250.84\" y=\"-160.8\">a &amp; !b &amp; c</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
-        "<path d=\"M117.401,-30.3702C127.665,-31.5284 136.821,-28.7383 136.821,-22 136.821,-17.6833 133.063,-14.9869 127.664,-13.9109\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"127.493,-10.405 117.401,-13.6298 127.302,-17.4024 127.493,-10.405\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"136.821\" y=\"-18.3\">c</text>\n",
+        "<path d=\"M119.421,-30.3702C129.685,-31.5284 138.84,-28.7383 138.84,-22 138.84,-17.6833 135.083,-14.9869 129.684,-13.9109\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"129.513,-10.405 119.421,-13.6298 129.321,-17.4024 129.513,-10.405\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"138.84\" y=\"-18.3\">c</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge3\"><title>1-&gt;1</title>\n",
-        "<path d=\"M344.401,-30.3702C354.665,-31.5284 363.821,-28.7383 363.821,-22 363.821,-17.6833 360.063,-14.9869 354.664,-13.9109\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"354.493,-10.405 344.401,-13.6298 354.302,-17.4024 354.493,-10.405\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"363.821\" y=\"-18.3\">b</text>\n",
+        "<path d=\"M347.421,-30.3702C357.685,-31.5284 366.84,-28.7383 366.84,-22 366.84,-17.6833 363.083,-14.9869 357.684,-13.9109\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"357.513,-10.405 347.421,-13.6298 357.321,-17.4024 357.513,-10.405\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"366.84\" y=\"-18.3\">b</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge4\"><title>2-&gt;2</title>\n",
-        "<path d=\"M496.401,-30.3702C506.665,-31.5284 515.821,-28.7383 515.821,-22 515.821,-17.6833 512.063,-14.9869 506.664,-13.9109\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"506.493,-10.405 496.401,-13.6298 506.302,-17.4024 506.493,-10.405\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"515.821\" y=\"-18.3\">a</text>\n",
+        "<path d=\"M499.421,-30.3702C509.685,-31.5284 518.84,-28.7383 518.84,-22 518.84,-17.6833 515.083,-14.9869 509.684,-13.9109\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"509.513,-10.405 499.421,-13.6298 509.321,-17.4024 509.513,-10.405\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"518.84\" y=\"-18.3\">a</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge5\"><title>3-&gt;0</title>\n",
-        "<path d=\"M100.426,-95.0356C99.3798,-89.2207 98.3997,-82.8875 97.8206,-77 97.0968,-69.6426 96.724,-61.6951 96.5546,-54.2187\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"100.053,-54.0318 96.4353,-44.0737 93.0533,-54.1142 100.053,-54.0318\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"97.8206\" y=\"-65.8\">!b &amp; c</text>\n",
+        "<path d=\"M101.72,-94.9925C100.973,-89.1774 100.268,-82.8549 99.8401,-77 99.3008,-69.6268 98.9988,-61.6732 98.8392,-54.196\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"102.337,-54.0032 98.6983,-44.0528 95.3376,-54.1005 102.337,-54.0032\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"99.8401\" y=\"-65.8\">!b &amp; c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge6\"><title>3-&gt;1</title>\n",
-        "<path d=\"M118.176,-99.186C129.593,-85.226 145.463,-66.8933 153.821,-62 197.157,-36.6256 255.69,-27.7601 291.543,-24.6629\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"292.194,-28.1235 301.899,-23.8749 291.662,-21.1437 292.194,-28.1235\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"153.821\" y=\"-65.8\">b &amp; !c</text>\n",
+        "<path d=\"M118.571,-99.4594C130.514,-85.4667 147.219,-66.9259 155.84,-62 199.687,-36.9475 258.489,-27.9869 294.467,-24.7826\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"295.165,-28.2385 304.859,-23.9616 294.614,-21.2602 295.165,-28.2385\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"155.84\" y=\"-65.8\">b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge7\"><title>3-&gt;3</title>\n",
-        "<path d=\"M125.401,-125.37C135.665,-126.528 144.821,-123.738 144.821,-117 144.821,-112.683 141.063,-109.987 135.664,-108.911\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"135.493,-105.405 125.401,-108.63 135.302,-112.402 135.493,-105.405\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"144.821\" y=\"-113.3\">b &amp; c</text>\n",
+        "<path d=\"M125.421,-125.37C135.685,-126.528 144.84,-123.738 144.84,-117 144.84,-112.683 141.083,-109.987 135.684,-108.911\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"135.513,-105.405 125.421,-108.63 135.321,-112.402 135.513,-105.405\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"144.84\" y=\"-113.3\">b &amp; c</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge8\"><title>4-&gt;1</title>\n",
-        "<path d=\"M420.21,-97.1109C413.838,-85.9186 404.665,-72.013 393.821,-62 382.059,-51.1404 366.728,-42.1637 353.413,-35.5713\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"354.69,-32.3041 344.153,-31.1996 351.702,-38.634 354.69,-32.3041\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"405.821\" y=\"-65.8\">!a &amp; b</text>\n",
+        "<path d=\"M423.229,-97.1109C416.857,-85.9186 407.685,-72.013 396.84,-62 385.079,-51.1404 369.748,-42.1637 356.432,-35.5713\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"357.71,-32.3041 347.173,-31.1996 354.721,-38.634 357.71,-32.3041\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"408.84\" y=\"-65.8\">!a &amp; b</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge9\"><title>4-&gt;2</title>\n",
-        "<path d=\"M441.69,-98.1028C445.777,-91.5928 450.225,-84.0908 453.821,-77 457.791,-69.1689 461.597,-60.4456 464.893,-52.3336\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"468.223,-53.4297 468.639,-42.843 461.712,-50.86 468.223,-53.4297\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"459.821\" y=\"-65.8\">a &amp; !b</text>\n",
+        "<path d=\"M444.71,-98.1028C448.796,-91.5928 453.245,-84.0908 456.84,-77 460.811,-69.1689 464.616,-60.4456 467.913,-52.3336\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"471.243,-53.4297 471.658,-42.843 464.731,-50.86 471.243,-53.4297\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"462.84\" y=\"-65.8\">a &amp; !b</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge10\"><title>4-&gt;4</title>\n",
-        "<path d=\"M450.401,-125.37C460.665,-126.528 469.821,-123.738 469.821,-117 469.821,-112.683 466.063,-109.987 460.664,-108.911\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"460.493,-105.405 450.401,-108.63 460.302,-112.402 460.493,-105.405\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"469.821\" y=\"-113.3\">a &amp; b</text>\n",
+        "<path d=\"M453.421,-125.37C463.685,-126.528 472.84,-123.738 472.84,-117 472.84,-112.683 469.083,-109.987 463.684,-108.911\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"463.513,-105.405 453.421,-108.63 463.321,-112.402 463.513,-105.405\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"472.84\" y=\"-113.3\">a &amp; b</text>\n",
         "</g>\n",
         "<!-- 5&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge11\"><title>5-&gt;0</title>\n",
-        "<path d=\"M212.569,-95.3163C209.347,-84.2043 203.876,-70.9826 194.821,-62 176.833,-44.1578 149.662,-34.2098 128.489,-28.8346\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"129.176,-25.401 118.644,-26.5487 127.593,-32.2197 129.176,-25.401\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"204.821\" y=\"-65.8\">!a &amp; c</text>\n",
+        "<path d=\"M214.588,-95.3163C211.367,-84.2043 205.896,-70.9826 196.84,-62 178.852,-44.1578 151.682,-34.2098 130.509,-28.8346\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"131.196,-25.401 120.663,-26.5487 129.613,-32.2197 131.196,-25.401\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"206.84\" y=\"-65.8\">!a &amp; c</text>\n",
         "</g>\n",
         "<!-- 5&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge12\"><title>5-&gt;2</title>\n",
-        "<path d=\"M237.087,-107.526C263.687,-96.5156 311.919,-76.937 353.821,-62 384.748,-50.9751 420.585,-39.6937 445.38,-32.1195\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"446.406,-35.4656 454.958,-29.2102 444.372,-28.7677 446.406,-35.4656\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"353.821\" y=\"-65.8\">a &amp; !c</text>\n",
+        "<path d=\"M238.802,-107.727C265.504,-96.7677 314.413,-77.0653 356.84,-62 387.781,-51.0134 423.616,-39.7261 448.407,-32.14\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"449.435,-35.4856 457.983,-29.2257 447.397,-28.7889 449.435,-35.4856\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"356.84\" y=\"-65.8\">a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 5&#45;&gt;5 -->\n",
         "<g class=\"edge\" id=\"edge13\"><title>5-&gt;5</title>\n",
-        "<path d=\"M237.401,-125.37C247.665,-126.528 256.821,-123.738 256.821,-117 256.821,-112.683 253.063,-109.987 247.664,-108.911\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"247.493,-105.405 237.401,-108.63 247.302,-112.402 247.493,-105.405\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"start\" x=\"256.821\" y=\"-113.3\">a &amp; c</text>\n",
+        "<path d=\"M239.421,-125.37C249.685,-126.528 258.84,-123.738 258.84,-117 258.84,-112.683 255.083,-109.987 249.684,-108.911\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"249.513,-105.405 239.421,-108.63 249.321,-112.402 249.513,-105.405\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"258.84\" y=\"-113.3\">a &amp; c</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f7bcacdebe0>"
+        "<IPython.core.display.SVG at 0x7f17ed8c7a58>"
+       ]
+      }
+     ],
+     "prompt_number": 11
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "a = spot.translate('F(a & X(!a &Xb))', pref=\"any\"); a"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "pyout",
+       "prompt_number": 12,
+       "svg": [
+        "<?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.38.0 (20140413.2041)\n",
+        " -->\n",
+        "<!-- Title: G Pages: 1 -->\n",
+        "<svg width=\"332pt\" height=\"92pt\"\n",
+        " viewBox=\"0.00 0.00 332.00 92.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 88)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-88 328,-88 328,4 -4,4\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-18C2.67247,-18 15.0966,-18 27.6277,-18\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"27.9419,-21.5001 37.9419,-18 27.9418,-14.5001 27.9419,-21.5001\"/>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-35.0373C48.3189,-44.8579 50.4453,-54 56,-54 59.4717,-54 61.6042,-50.4289 62.3975,-45.3529\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"65.8971,-45.031 62.3792,-35.0373 58.8971,-45.0435 65.8971,-45.031\"/>\n",
+        "<text text-anchor=\"start\" x=\"51.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"135\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"start\" x=\"130.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M74.0888,-18C83.659,-18 95.8172,-18 106.677,-18\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"106.959,-21.5001 116.959,-18 106.959,-14.5001 106.959,-21.5001\"/>\n",
+        "<text text-anchor=\"start\" x=\"92\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"218\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"218\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M153.178,-18C163.81,-18 177.694,-18 189.796,-18\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"189.847,-21.5001 199.847,-18 189.847,-14.5001 189.847,-21.5001\"/>\n",
+        "<text text-anchor=\"start\" x=\"171\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"306\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"306\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;3 -->\n",
+        "<g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M236.403,-18C248.254,-18 264.183,-18 277.708,-18\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"277.916,-21.5001 287.916,-18 277.916,-14.5001 277.916,-21.5001\"/>\n",
+        "<text text-anchor=\"start\" x=\"257.5\" y=\"-36.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
+        "<text text-anchor=\"start\" x=\"254\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g id=\"edge6\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M298.332,-34.2903C296.483,-44.3892 299.039,-54 306,-54 310.459,-54 313.111,-50.0557 313.955,-44.5656\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"317.446,-44.1887 313.668,-34.2903 310.448,-44.384 317.446,-44.1887\"/>\n",
+        "<text text-anchor=\"start\" x=\"301.5\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "<text text-anchor=\"start\" x=\"298\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>\n"
+       ],
+       "text": [
+        "<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f17fc0fbb40> >"
        ]
       }
      ],
@@ -980,10 +1077,476 @@
     {
      "cell_type": "code",
      "collapsed": false,
-     "input": [],
+     "input": [
+      "spot.sl(a)"
+     ],
      "language": "python",
      "metadata": {},
-     "outputs": []
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "pyout",
+       "prompt_number": 15,
+       "svg": [
+        "<?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.38.0 (20140413.2041)\n",
+        " -->\n",
+        "<!-- Title: G Pages: 1 -->\n",
+        "<svg width=\"790pt\" height=\"360pt\"\n",
+        " viewBox=\"0.00 0.00 789.73 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.647482 0.647482) rotate(0) translate(4 552)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-552 1215.69,-552 1215.69,4 -4,4\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-282\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-278.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-282C2.67247,-282 15.0966,-282 27.6277,-282\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"27.9419,-285.5 37.9419,-282 27.9418,-278.5 27.9419,-285.5\"/>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"162.5\" cy=\"-225\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"162.5\" y=\"-221.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M72.4193,-273.589C89.5736,-264.233 117.504,-248.998 137.518,-238.081\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"139.254,-241.121 146.357,-233.26 135.902,-234.976 139.254,-241.121\"/>\n",
+        "<text text-anchor=\"start\" x=\"92\" y=\"-264.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"274.5\" cy=\"-282\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"274.5\" y=\"-278.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M73.874,-285.312C105.727,-291.062 176.828,-301.499 236,-293 239.782,-292.457 243.714,-291.62 247.548,-290.646\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"248.648,-293.972 257.296,-287.851 246.718,-287.243 248.648,-293.972\"/>\n",
+        "<text text-anchor=\"start\" x=\"144\" y=\"-299.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"392.5\" cy=\"-182\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"392.5\" y=\"-178.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;3 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M66.4817,-266.974C86.5703,-236.695 136.724,-168.943 199,-142 262.31,-114.61 292.001,-103.76 354,-134 364.122,-138.937 372.313,-148.074 378.427,-157.061\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"375.613,-159.166 383.843,-165.838 381.57,-155.49 375.613,-159.166\"/>\n",
+        "<text text-anchor=\"start\" x=\"199\" y=\"-145.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g id=\"node6\" class=\"node\"><title>4</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"508.5\" cy=\"-283\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"508.5\" y=\"-279.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;4 -->\n",
+        "<g id=\"edge5\" class=\"edge\"><title>0&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M57.7109,-300.095C60.7583,-350.7 76.8361,-490 161.5,-490 161.5,-490 161.5,-490 334.5,-490 409.803,-490 436.423,-457.369 472,-391 485.846,-365.171 495.573,-332.971 501.301,-310.48\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"504.744,-311.134 503.722,-300.589 497.945,-309.47 504.744,-311.134\"/>\n",
+        "<text text-anchor=\"start\" x=\"254\" y=\"-493.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 5 -->\n",
+        "<g id=\"node7\" class=\"node\"><title>5</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"618\" cy=\"-159\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"618\" y=\"-155.3\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;5 -->\n",
+        "<g id=\"edge6\" class=\"edge\"><title>0&#45;&gt;5</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M59.5927,-264.36C69.1541,-202.623 104.85,-0 161.5,-0 161.5,-0 161.5,-0 509.5,-0 572.254,-0 600.855,-86.0511 611.591,-131.544\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"608.191,-132.378 613.783,-141.377 615.024,-130.855 608.191,-132.378\"/>\n",
+        "<text text-anchor=\"start\" x=\"316.5\" y=\"-3.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 6 -->\n",
+        "<g id=\"node8\" class=\"node\"><title>6</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"618\" cy=\"-283\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"618\" y=\"-279.3\" font-family=\"Lato\" font-size=\"14.00\">6</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;6 -->\n",
+        "<g id=\"edge7\" class=\"edge\"><title>0&#45;&gt;6</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M56.3587,-300.051C55.3315,-357.603 60.4873,-533 161.5,-533 161.5,-533 161.5,-533 509.5,-533 605.049,-533 616.721,-376.973 617.41,-311.443\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"620.91,-311.392 617.435,-301.383 613.91,-311.374 620.91,-311.392\"/>\n",
+        "<text text-anchor=\"start\" x=\"315\" y=\"-536.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g id=\"edge8\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M153.521,-240.916C151.179,-251.15 154.172,-261 162.5,-261 167.965,-261 171.133,-256.758 172.003,-250.949\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"175.496,-250.72 171.479,-240.916 168.505,-251.085 175.496,-250.72\"/>\n",
+        "<text text-anchor=\"start\" x=\"145.5\" y=\"-264.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g id=\"edge9\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M174.399,-238.625C180.859,-245.896 189.606,-254.461 199,-260 213.583,-268.598 231.778,-274.054 246.536,-277.382\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"246.074,-280.86 256.574,-279.443 247.482,-274.003 246.074,-280.86\"/>\n",
+        "<text text-anchor=\"start\" x=\"199\" y=\"-277.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g id=\"edge10\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M180.265,-221.838C219.465,-214.445 317.374,-195.98 364.851,-187.026\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"365.532,-190.459 374.71,-185.167 364.235,-183.581 365.532,-190.459\"/>\n",
+        "<text text-anchor=\"start\" x=\"256\" y=\"-210.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;4 -->\n",
+        "<g id=\"edge11\" class=\"edge\"><title>1&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M172.479,-209.649C178.749,-200.27 187.958,-188.807 199,-182 280.605,-131.693 320.87,-128.502 413,-155 442.746,-163.556 452.659,-167.835 472,-192 487.02,-210.766 481.177,-220.641 490,-243 491.85,-247.689 493.92,-252.641 495.971,-257.403\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"492.855,-259.013 500.076,-266.765 499.266,-256.202 492.855,-259.013\"/>\n",
+        "<text text-anchor=\"start\" x=\"313\" y=\"-144.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;5 -->\n",
+        "<g id=\"edge12\" class=\"edge\"><title>1&#45;&gt;5</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M168.516,-208.006C173.818,-192.756 183.579,-170.722 199,-157 218.547,-139.606 228.567,-142.149 254,-136 371.942,-107.483 406.242,-121.118 527,-133 551.471,-135.408 558.612,-131.407 582,-139 585.932,-140.276 589.912,-142.028 593.709,-143.968\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"592.212,-147.143 602.64,-149.015 595.656,-141.048 592.212,-147.143\"/>\n",
+        "<text text-anchor=\"start\" x=\"375.5\" y=\"-123.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;6 -->\n",
+        "<g id=\"edge13\" class=\"edge\"><title>1&#45;&gt;6</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M168.227,-242.485C175.273,-267.677 188.792,-312.631 199,-326 234.13,-372.011 256.369,-376.996 313,-389 382.136,-403.654 403.101,-406.733 472,-391 524.906,-378.919 541.436,-374.049 582,-338 591.327,-329.711 599.112,-318.361 604.953,-308.123\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"608.121,-309.621 609.76,-299.154 601.951,-306.315 608.121,-309.621\"/>\n",
+        "<text text-anchor=\"start\" x=\"374\" y=\"-404.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g id=\"edge14\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M263.695,-267.344C256.944,-258.393 247.194,-247.463 236,-241 222.301,-233.091 205.076,-229.088 190.853,-227.064\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"191.009,-223.558 180.67,-225.869 190.194,-230.51 191.009,-223.558\"/>\n",
+        "<text text-anchor=\"start\" x=\"200.5\" y=\"-244.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g id=\"edge15\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M264.925,-297.541C262.23,-307.909 265.422,-318 274.5,-318 280.458,-318 283.88,-313.654 284.767,-307.736\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"288.244,-307.281 284.075,-297.541 281.26,-307.756 288.244,-307.281\"/>\n",
+        "<text text-anchor=\"start\" x=\"256\" y=\"-321.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;3 -->\n",
+        "<g id=\"edge16\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M283.767,-266.383C290.49,-254.757 300.835,-239.052 313,-228 328.464,-213.95 335.98,-215.575 354,-205 358.576,-202.315 363.43,-199.393 368.074,-196.561\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"369.929,-199.529 376.617,-191.312 366.265,-193.565 369.929,-199.529\"/>\n",
+        "<text text-anchor=\"start\" x=\"315\" y=\"-231.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g id=\"edge17\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M292.56,-282.074C332.447,-282.245 432.073,-282.675 480.383,-282.883\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"480.4,-286.383 490.415,-282.926 480.431,-279.383 480.4,-286.383\"/>\n",
+        "<text text-anchor=\"start\" x=\"372\" y=\"-285.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;5 -->\n",
+        "<g id=\"edge18\" class=\"edge\"><title>2&#45;&gt;5</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M280.75,-264.887C286.653,-247.539 297.486,-220.539 313,-201 333.676,-174.96 341.248,-167.646 372,-155 446.278,-124.454 544.248,-141.138 590.568,-152.002\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"589.871,-155.435 600.416,-154.41 591.533,-148.635 589.871,-155.435\"/>\n",
+        "<text text-anchor=\"start\" x=\"434.5\" y=\"-143.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;6 -->\n",
+        "<g id=\"edge19\" class=\"edge\"><title>2&#45;&gt;6</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M287.591,-294.625C294.456,-301.07 303.549,-308.484 313,-313 399.658,-354.404 435.08,-370.831 527,-343 553.567,-334.956 579.459,-316.198 596.599,-301.781\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"599.017,-304.316 604.274,-295.117 594.428,-299.03 599.017,-304.316\"/>\n",
+        "<text text-anchor=\"start\" x=\"433\" y=\"-359.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;1 -->\n",
+        "<g id=\"edge20\" class=\"edge\"><title>3&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M374.301,-179.412C348.005,-176.004 296.393,-171.485 254,-181 229.693,-186.456 204.386,-199.485 186.735,-209.958\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"184.47,-207.241 177.771,-215.449 188.126,-213.21 184.47,-207.241\"/>\n",
+        "<text text-anchor=\"start\" x=\"257.5\" y=\"-184.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g id=\"edge21\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M384.617,-198.245C378.275,-211.641 367.766,-230.422 354,-243 345.639,-250.64 320.461,-262.581 300.85,-271.238\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"299.268,-268.109 291.494,-275.308 302.06,-274.528 299.268,-268.109\"/>\n",
+        "<text text-anchor=\"start\" x=\"315\" y=\"-268.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g id=\"edge22\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M382.687,-197.167C379.713,-207.664 382.984,-218 392.5,-218 398.745,-218 402.3,-213.549 403.166,-207.522\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"406.622,-206.846 402.313,-197.167 399.646,-207.42 406.622,-206.846\"/>\n",
+        "<text text-anchor=\"start\" x=\"374\" y=\"-221.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;4 -->\n",
+        "<g id=\"edge23\" class=\"edge\"><title>3&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M402.231,-197.183C409.049,-208.102 419.309,-222.663 431,-233 446.653,-246.84 454.532,-244.537 472,-256 476.576,-259.003 481.332,-262.406 485.819,-265.76\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"483.933,-268.724 493.999,-272.029 488.191,-263.168 483.933,-268.724\"/>\n",
+        "<text text-anchor=\"start\" x=\"431\" y=\"-259.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;5 -->\n",
+        "<g id=\"edge24\" class=\"edge\"><title>3&#45;&gt;5</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M410.186,-177.389C416.642,-175.765 424.121,-174.077 431,-173 486.958,-164.237 553.277,-160.913 589.677,-159.687\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"590.082,-163.176 599.969,-159.37 589.866,-156.179 590.082,-163.176\"/>\n",
+        "<text text-anchor=\"start\" x=\"491.5\" y=\"-168.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;6 -->\n",
+        "<g id=\"edge25\" class=\"edge\"><title>3&#45;&gt;6</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M410.49,-183.825C426.702,-185.943 451.607,-190.192 472,-198 518.274,-215.716 566.956,-247.327 594.493,-266.606\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"592.806,-269.7 602.986,-272.633 596.857,-263.991 592.806,-269.7\"/>\n",
+        "<text text-anchor=\"start\" x=\"490\" y=\"-227.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;1 -->\n",
+        "<g id=\"edge26\" class=\"edge\"><title>4&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M506.342,-301.215C503.871,-322.954 496.141,-358.439 472,-375 456.974,-385.308 449.145,-376.677 431,-375 351.317,-367.635 325.844,-377.242 254,-342 224.607,-327.582 219.126,-318.821 199,-293 188.92,-280.068 180.325,-263.847 174.118,-250.492\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"177.311,-249.06 170.033,-241.361 170.922,-251.919 177.311,-249.06\"/>\n",
+        "<text text-anchor=\"start\" x=\"316.5\" y=\"-373.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;2 -->\n",
+        "<g id=\"edge27\" class=\"edge\"><title>4&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M491.55,-290.063C485.542,-292.396 478.571,-294.719 472,-296 402.638,-309.517 382.319,-309.734 313,-296 308.974,-295.202 304.809,-294.027 300.785,-292.692\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"301.82,-289.343 291.227,-289.165 299.397,-295.911 301.82,-289.343\"/>\n",
+        "<text text-anchor=\"start\" x=\"374\" y=\"-309.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;3 -->\n",
+        "<g id=\"edge28\" class=\"edge\"><title>4&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M502.475,-265.839C497.166,-250.421 487.401,-228.101 472,-214 467.83,-210.182 440.383,-199.418 419.105,-191.422\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"420.169,-188.084 409.576,-187.87 417.724,-194.643 420.169,-188.084\"/>\n",
+        "<text text-anchor=\"start\" x=\"433\" y=\"-217.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;4 -->\n",
+        "<g id=\"edge29\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M499.267,-298.541C496.669,-308.909 499.746,-319 508.5,-319 514.245,-319 517.545,-314.654 518.4,-308.736\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"521.879,-308.291 517.733,-298.541 514.894,-308.749 521.879,-308.291\"/>\n",
+        "<text text-anchor=\"start\" x=\"488\" y=\"-322.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;5 -->\n",
+        "<g id=\"edge30\" class=\"edge\"><title>4&#45;&gt;5</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M521.004,-269.73C539.675,-248.194 576.715,-205.468 598.929,-179.845\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"601.672,-182.023 605.578,-172.175 596.383,-177.438 601.672,-182.023\"/>\n",
+        "<text text-anchor=\"start\" x=\"546.5\" y=\"-242.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;6 -->\n",
+        "<g id=\"edge31\" class=\"edge\"><title>4&#45;&gt;6</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M526.772,-283C543.698,-283 569.762,-283 589.533,-283\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"589.771,-286.5 599.771,-283 589.771,-279.5 589.771,-286.5\"/>\n",
+        "<text text-anchor=\"start\" x=\"545\" y=\"-286.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;5 -->\n",
+        "<g id=\"edge32\" class=\"edge\"><title>5&#45;&gt;5</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M608.767,-174.541C606.169,-184.909 609.246,-195 618,-195 623.745,-195 627.045,-190.654 627.9,-184.736\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"631.379,-184.291 627.233,-174.541 624.394,-184.749 631.379,-184.291\"/>\n",
+        "<text text-anchor=\"start\" x=\"601\" y=\"-198.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 7 -->\n",
+        "<g id=\"node9\" class=\"node\"><title>7</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"731\" cy=\"-176\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"731\" y=\"-172.3\" font-family=\"Lato\" font-size=\"14.00\">7</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;7 -->\n",
+        "<g id=\"edge33\" class=\"edge\"><title>5&#45;&gt;7</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M636.072,-158.841C651.587,-158.999 675.034,-159.994 695,-164 698.051,-164.612 701.2,-165.422 704.301,-166.333\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"703.273,-169.679 713.866,-169.47 705.454,-163.028 703.273,-169.679\"/>\n",
+        "<text text-anchor=\"start\" x=\"656\" y=\"-167.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 8 -->\n",
+        "<g id=\"node10\" class=\"node\"><title>8</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"731\" cy=\"-270\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"731\" y=\"-266.3\" font-family=\"Lato\" font-size=\"14.00\">8</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;8 -->\n",
+        "<g id=\"edge34\" class=\"edge\"><title>5&#45;&gt;8</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M626.246,-175.292C632.397,-187.908 642.108,-205.314 654,-218 668.989,-233.991 689.72,-247.767 705.744,-257.116\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"704.127,-260.222 714.556,-262.091 707.569,-254.127 704.127,-260.222\"/>\n",
+        "<text text-anchor=\"start\" x=\"654\" y=\"-253.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 6&#45;&gt;6 -->\n",
+        "<g id=\"edge35\" class=\"edge\"><title>6&#45;&gt;6</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M608.767,-298.541C606.169,-308.909 609.246,-319 618,-319 623.745,-319 627.045,-314.654 627.9,-308.736\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"631.379,-308.291 627.233,-298.541 624.394,-308.749 631.379,-308.291\"/>\n",
+        "<text text-anchor=\"start\" x=\"599.5\" y=\"-322.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 6&#45;&gt;7 -->\n",
+        "<g id=\"edge36\" class=\"edge\"><title>6&#45;&gt;7</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M622.422,-265.333C626.786,-247.328 636.028,-219.738 654,-203 667.449,-190.475 687.084,-183.695 703.028,-180.063\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"703.747,-183.488 712.87,-178.101 702.378,-176.623 703.747,-183.488\"/>\n",
+        "<text text-anchor=\"start\" x=\"656\" y=\"-206.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 6&#45;&gt;8 -->\n",
+        "<g id=\"edge37\" class=\"edge\"><title>6&#45;&gt;8</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M636.344,-280.969C654.102,-278.889 681.96,-275.626 702.683,-273.199\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"703.253,-276.657 712.778,-272.017 702.439,-269.704 703.253,-276.657\"/>\n",
+        "<text text-anchor=\"start\" x=\"654\" y=\"-281.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;7 -->\n",
+        "<g id=\"edge38\" class=\"edge\"><title>7&#45;&gt;7</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M722.021,-191.916C719.679,-202.15 722.672,-212 731,-212 736.465,-212 739.633,-207.758 740.503,-201.949\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"743.996,-201.72 739.979,-191.916 737.005,-202.085 743.996,-201.72\"/>\n",
+        "<text text-anchor=\"start\" x=\"712.5\" y=\"-215.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 9 -->\n",
+        "<g id=\"node11\" class=\"node\"><title>9</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"837.5\" cy=\"-321\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"837.5\" y=\"-317.3\" font-family=\"Lato\" font-size=\"14.00\">9</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;9 -->\n",
+        "<g id=\"edge39\" class=\"edge\"><title>7&#45;&gt;9</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M744.505,-187.995C759.187,-202.494 783.724,-228.064 801,-253 810.187,-266.259 818.627,-282.194 824.971,-295.305\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"821.964,-297.134 829.391,-304.689 828.296,-294.151 821.964,-297.134\"/>\n",
+        "<text text-anchor=\"start\" x=\"767\" y=\"-271.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "<text text-anchor=\"start\" x=\"776\" y=\"-256.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 10 -->\n",
+        "<g id=\"node12\" class=\"node\"><title>10</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"950.448\" cy=\"-226\" rx=\"21.3963\" ry=\"21.3963\"/>\n",
+        "<text text-anchor=\"middle\" x=\"950.448\" y=\"-222.3\" font-family=\"Lato\" font-size=\"14.00\">10</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;10 -->\n",
+        "<g id=\"edge40\" class=\"edge\"><title>7&#45;&gt;10</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M749.167,-173.628C773.4,-170.841 818.828,-167.686 856,-177 880.513,-183.142 905.744,-196.894 923.8,-208.27\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"922.253,-211.439 932.546,-213.95 926.066,-205.568 922.253,-211.439\"/>\n",
+        "<text text-anchor=\"start\" x=\"819\" y=\"-195.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "<text text-anchor=\"start\" x=\"829.5\" y=\"-180.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;8 -->\n",
+        "<g id=\"edge41\" class=\"edge\"><title>8&#45;&gt;8</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M722.021,-285.916C719.679,-296.15 722.672,-306 731,-306 736.465,-306 739.633,-301.758 740.503,-295.949\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"743.996,-295.72 739.979,-285.916 737.005,-296.085 743.996,-295.72\"/>\n",
+        "<text text-anchor=\"start\" x=\"710.5\" y=\"-309.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;9 -->\n",
+        "<g id=\"edge42\" class=\"edge\"><title>8&#45;&gt;9</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M747.419,-277.525C764.398,-285.812 791.935,-299.251 811.903,-308.995\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"810.495,-312.203 821.017,-313.444 813.566,-305.913 810.495,-312.203\"/>\n",
+        "<text text-anchor=\"start\" x=\"767\" y=\"-321.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "<text text-anchor=\"start\" x=\"776\" y=\"-306.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;10 -->\n",
+        "<g id=\"edge43\" class=\"edge\"><title>8&#45;&gt;10</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M740.078,-254.24C746.053,-244.436 755.193,-232.653 767,-227 816.356,-203.368 882.185,-211.176 919.777,-218.753\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"919.082,-222.183 929.594,-220.857 920.55,-215.339 919.082,-222.183\"/>\n",
+        "<text text-anchor=\"start\" x=\"819\" y=\"-230.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "<text text-anchor=\"start\" x=\"829.5\" y=\"-215.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 9&#45;&gt;9 -->\n",
+        "<g id=\"edge44\" class=\"edge\"><title>9&#45;&gt;9</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M828.521,-336.916C826.179,-347.15 829.172,-357 837.5,-357 842.965,-357 846.133,-352.758 847.003,-346.949\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"850.496,-346.72 846.479,-336.916 843.505,-347.085 850.496,-346.72\"/>\n",
+        "<text text-anchor=\"start\" x=\"820.5\" y=\"-375.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "<text text-anchor=\"start\" x=\"829.5\" y=\"-360.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 9&#45;&gt;10 -->\n",
+        "<g id=\"edge45\" class=\"edge\"><title>9&#45;&gt;10</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M842.449,-303.446C847.146,-286.574 856.635,-261.552 874,-247 886.411,-236.6 903.603,-231.331 918.442,-228.671\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"919.344,-232.076 928.729,-227.158 918.326,-225.15 919.344,-232.076\"/>\n",
+        "<text text-anchor=\"start\" x=\"874\" y=\"-265.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "<text text-anchor=\"start\" x=\"884.5\" y=\"-250.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 11 -->\n",
+        "<g id=\"node13\" class=\"node\"><title>11</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1190.24\" cy=\"-320\" rx=\"21.3963\" ry=\"21.3963\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1190.24\" y=\"-316.3\" font-family=\"Lato\" font-size=\"14.00\">11</text>\n",
+        "</g>\n",
+        "<!-- 9&#45;&gt;11 -->\n",
+        "<g id=\"edge46\" class=\"edge\"><title>9&#45;&gt;11</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M839.947,-339.074C843.366,-376.939 853.261,-462.691 874,-482 925.334,-529.795 960.93,-503.936 1030.9,-499 1084.58,-495.213 1111.02,-518.263 1150.79,-482 1169.75,-464.718 1180.9,-393.55 1185.96,-351.508\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1189.44,-351.833 1187.11,-341.497 1182.49,-351.03 1189.44,-351.833\"/>\n",
+        "<text text-anchor=\"start\" x=\"991.896\" y=\"-522.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"1002.4\" y=\"-507.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 12 -->\n",
+        "<g id=\"node14\" class=\"node\"><title>12</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1070.34\" cy=\"-321\" rx=\"21.3963\" ry=\"21.3963\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1070.34\" y=\"-317.3\" font-family=\"Lato\" font-size=\"14.00\">12</text>\n",
+        "</g>\n",
+        "<!-- 9&#45;&gt;12 -->\n",
+        "<g id=\"edge47\" class=\"edge\"><title>9&#45;&gt;12</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M854.953,-326.076C860.894,-327.667 867.691,-329.213 874,-330 943.195,-338.635 961.625,-337.999 1030.9,-330 1033.77,-329.668 1036.74,-329.201 1039.7,-328.653\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1040.49,-332.062 1049.54,-326.552 1039.03,-325.216 1040.49,-332.062\"/>\n",
+        "<text text-anchor=\"start\" x=\"929.948\" y=\"-354.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"942.448\" y=\"-339.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 10&#45;&gt;9 -->\n",
+        "<g id=\"edge48\" class=\"edge\"><title>10&#45;&gt;9</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M938.445,-243.876C931.44,-254.332 921.692,-267.332 911,-277 908.881,-278.916 882.676,-294.686 862.373,-306.804\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"860.366,-303.926 853.568,-312.052 863.95,-309.939 860.366,-303.926\"/>\n",
+        "<text text-anchor=\"start\" x=\"875.5\" y=\"-316.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "<text text-anchor=\"start\" x=\"884.5\" y=\"-301.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 10&#45;&gt;10 -->\n",
+        "<g id=\"edge49\" class=\"edge\"><title>10&#45;&gt;10</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M940.451,-245.077C938.584,-255.682 941.917,-265.448 950.448,-265.448 956.047,-265.448 959.406,-261.242 960.527,-255.354\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"964.025,-255.049 960.446,-245.077 957.025,-255.105 964.025,-255.049\"/>\n",
+        "<text text-anchor=\"start\" x=\"931.948\" y=\"-284.248\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "<text text-anchor=\"start\" x=\"942.448\" y=\"-269.248\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 10&#45;&gt;11 -->\n",
+        "<g id=\"edge50\" class=\"edge\"><title>10&#45;&gt;11</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M968.572,-213.756C975.193,-209.079 982.858,-203.735 989.896,-199 1030,-172.02 1045.42,-147.36 1091.79,-161 1121.71,-169.802 1131.84,-174.229 1150.79,-199 1170.92,-225.309 1180.67,-262.432 1185.28,-288.603\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1181.87,-289.422 1186.91,-298.74 1188.78,-288.311 1181.87,-289.422\"/>\n",
+        "<text text-anchor=\"start\" x=\"1051.84\" y=\"-179.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"1062.34\" y=\"-164.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 10&#45;&gt;12 -->\n",
+        "<g id=\"edge51\" class=\"edge\"><title>10&#45;&gt;12</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M962.313,-244.032C969.27,-254.542 979.014,-267.546 989.896,-277 991.047,-278 1019.81,-293.856 1042.4,-306.25\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1040.85,-309.39 1051.3,-311.128 1044.22,-303.252 1040.85,-309.39\"/>\n",
+        "<text text-anchor=\"start\" x=\"989.896\" y=\"-317.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"1002.4\" y=\"-302.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 11&#45;&gt;9 -->\n",
+        "<g id=\"edge52\" class=\"edge\"><title>11&#45;&gt;9</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1175.79,-336.339C1158.66,-355.709 1127.01,-386.889 1091.79,-399 1047.72,-414.154 960.01,-416.671 929,-407 896.265,-396.791 869.427,-366.357 853.7,-344.593\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"856.425,-342.383 847.845,-336.167 850.677,-346.377 856.425,-342.383\"/>\n",
+        "<text text-anchor=\"start\" x=\"993.396\" y=\"-430.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "<text text-anchor=\"start\" x=\"1002.4\" y=\"-415.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 11&#45;&gt;10 -->\n",
+        "<g id=\"edge53\" class=\"edge\"><title>11&#45;&gt;10</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1174.22,-305.599C1167.38,-299.452 1159,-292.454 1150.79,-287 1101.17,-254.014 1088.8,-241.065 1030.9,-227 1015.15,-223.175 997.122,-222.65 982.225,-223.202\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"981.801,-219.72 972.008,-223.762 982.185,-226.709 981.801,-219.72\"/>\n",
+        "<text text-anchor=\"start\" x=\"1051.84\" y=\"-266.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "<text text-anchor=\"start\" x=\"1062.34\" y=\"-251.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 11&#45;&gt;11 -->\n",
+        "<g id=\"edge54\" class=\"edge\"><title>11&#45;&gt;11</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1179.89,-339.077C1177.95,-349.682 1181.4,-359.448 1190.24,-359.448 1196.04,-359.448 1199.52,-355.242 1200.68,-349.354\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1204.18,-349.048 1200.6,-339.077 1197.18,-349.106 1204.18,-349.048\"/>\n",
+        "<text text-anchor=\"start\" x=\"1171.74\" y=\"-378.248\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"1182.24\" y=\"-363.248\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 11&#45;&gt;12 -->\n",
+        "<g id=\"edge55\" class=\"edge\"><title>11&#45;&gt;12</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1173.07,-306.515C1166.57,-301.921 1158.73,-297.354 1150.79,-295 1133.32,-289.82 1127.22,-289.662 1109.79,-295 1104.94,-296.486 1100.15,-298.812 1095.69,-301.477\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1093.42,-298.783 1087.06,-307.259 1097.32,-304.598 1093.42,-298.783\"/>\n",
+        "<text text-anchor=\"start\" x=\"1109.79\" y=\"-313.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"1122.29\" y=\"-298.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 12&#45;&gt;9 -->\n",
+        "<g id=\"edge56\" class=\"edge\"><title>12&#45;&gt;9</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1052.16,-333.174C1045.66,-337.507 1038.09,-342.239 1030.9,-346 989.658,-367.544 974.545,-379.504 929,-370 903.68,-364.716 878.057,-349.739 860.569,-337.721\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"862.388,-334.72 852.211,-331.773 858.33,-340.423 862.388,-334.72\"/>\n",
+        "<text text-anchor=\"start\" x=\"933.448\" y=\"-391.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "<text text-anchor=\"start\" x=\"942.448\" y=\"-376.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 12&#45;&gt;10 -->\n",
+        "<g id=\"edge57\" class=\"edge\"><title>12&#45;&gt;10</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1064.53,-300.174C1059.29,-282.284 1049.12,-257.195 1030.9,-243 1017.11,-232.263 998.068,-227.936 982.08,-226.33\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"982.322,-222.839 972.101,-225.628 981.83,-229.821 982.322,-222.839\"/>\n",
+        "<text text-anchor=\"start\" x=\"991.896\" y=\"-261.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "<text text-anchor=\"start\" x=\"1002.4\" y=\"-246.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 12&#45;&gt;11 -->\n",
+        "<g id=\"edge58\" class=\"edge\"><title>12&#45;&gt;11</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1091.67,-323.512C1097.51,-324.126 1103.89,-324.694 1109.79,-325 1127.99,-325.944 1132.61,-326.177 1150.79,-325 1153.38,-324.833 1156.06,-324.602 1158.74,-324.332\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1159.41,-327.778 1168.94,-323.139 1158.6,-320.825 1159.41,-327.778\"/>\n",
+        "<text text-anchor=\"start\" x=\"1111.79\" y=\"-343.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"1122.29\" y=\"-328.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 12&#45;&gt;12 -->\n",
+        "<g id=\"edge59\" class=\"edge\"><title>12&#45;&gt;12</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1059.99,-340.077C1058.06,-350.682 1061.51,-360.448 1070.34,-360.448 1076.14,-360.448 1079.62,-356.242 1080.78,-350.354\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1084.28,-350.048 1080.7,-340.077 1077.28,-350.106 1084.28,-350.048\"/>\n",
+        "<text text-anchor=\"start\" x=\"1049.84\" y=\"-379.248\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"1062.34\" y=\"-364.248\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>\n"
+       ],
+       "text": [
+        "<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f17fc0fb9c0> >"
+       ]
+      }
+     ],
+     "prompt_number": 15
     }
    ],
    "metadata": {}