diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb
index 2b73e6071..04b9c5699 100644
--- a/tests/python/highlighting.ipynb
+++ b/tests/python/highlighting.ipynb
@@ -15,10 +15,9 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.4.3+"
+   "version": "3.5.3rc1"
   },
-  "name": "",
-  "signature": "sha256:30e1abf38b76bd072ff688d2b48f94eb5945807bfa9583a8f457ad3bc4966c4e"
+  "name": ""
  },
  "nbformat": 3,
  "nbformat_minor": 0,
@@ -155,7 +154,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fc0d01ef400>"
+        "<IPython.core.display.SVG object>"
        ]
       }
      ],
@@ -255,7 +254,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d01be8a0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b0b5ab70> >"
        ]
       }
      ],
@@ -357,7 +356,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7fc0d0132f90> >"
+        "<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7fd9b0aeb270> >"
        ]
       }
      ],
@@ -572,7 +571,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b10f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b0aeb390> >"
        ]
       }
      ],
@@ -751,7 +750,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b10f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b0aeb390> >"
        ]
       }
      ],
@@ -831,7 +830,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b1090> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b0aeb660> >"
        ]
       },
       {
@@ -877,7 +876,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b1030> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b0aeb300> >"
        ]
       }
      ],
@@ -963,7 +962,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d0132fc0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b0aeb150> >"
        ]
       }
      ],
@@ -1088,7 +1087,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d0132fc0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b0aeb150> >"
        ]
       },
       {
@@ -1145,7 +1144,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b1090> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b0aeb660> >"
        ]
       },
       {
@@ -1191,7 +1190,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b1030> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b0aeb300> >"
        ]
       }
      ],
@@ -1398,7 +1397,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7fc0d57b1150> >"
+        "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7fd9b0aeb750> >"
        ]
       },
       {
@@ -1472,7 +1471,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b1120> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b0aeb630> >"
        ]
       },
       {
@@ -1556,7 +1555,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b1180> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b0aeb2d0> >"
        ]
       }
      ],
@@ -1702,7 +1701,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b1270> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b0aeb810> >"
        ]
       }
      ],
@@ -1847,7 +1846,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b1270> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b0aeb810> >"
        ]
       }
      ],
@@ -1990,7 +1989,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d57b1270> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b0aeb810> >"
        ]
       },
       {
@@ -2094,7 +2093,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fc0d00e1518>"
+        "<IPython.core.display.SVG object>"
        ]
       },
       {
@@ -2147,14 +2146,243 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fc0d00feb38>"
+        "<IPython.core.display.SVG object>"
        ]
       }
      ],
      "prompt_number": 19
+    },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "# Highlighting languages\n",
+      "\n",
+      "For deterministic automata, the function `spot.highlight_languages()` can be used to highlight states that recognize the same language.  This can be a great help in reading automata.  States with a colored border share their language, and states with a black border all have a language different from all other states."
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "aut = spot.translate('(b W Xa) & GF(c <-> Xb) | a', 'generic', 'det')\n",
+      "spot.highlight_languages(aut)\n",
+      "aut.show('.bas')"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "pyout",
+       "prompt_number": 20,
+       "svg": [
+        "<svg height=\"283pt\" viewBox=\"0.00 0.00 734.00 283.07\" width=\"734pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.993234 0.993234) rotate(0) translate(4 281)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-281 735,-281 735,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"313.5\" y=\"-262.8\">Fin(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"338.5\" y=\"-262.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"354.5\" y=\"-262.8\">) &amp; Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"397.5\" y=\"-262.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"413.5\" y=\"-262.8\">)</text>\n",
+        "<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
+        "<polygon fill=\"none\" points=\"139,-146 139,-246 191,-246 191,-146 139,-146\" stroke=\"green\"/>\n",
+        "</g>\n",
+        "<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
+        "<polygon fill=\"none\" points=\"470,-27 470,-229 723,-229 723,-27 470,-27\" stroke=\"green\"/>\n",
+        "</g>\n",
+        "<g class=\"cluster\" id=\"clust3\"><title>cluster_2</title>\n",
+        "<polygon fill=\"none\" points=\"391,-8 391,-60 443,-60 443,-8 391,-8\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<g class=\"cluster\" id=\"clust4\"><title>cluster_3</title>\n",
+        "<polygon fill=\"none\" points=\"139,-36 139,-138 327.5,-138 327.5,-36 139,-36\" stroke=\"green\"/>\n",
+        "</g>\n",
+        "<g class=\"cluster\" id=\"clust5\"><title>cluster_4</title>\n",
+        "<polygon fill=\"none\" points=\"30,-44 30,-96 82,-96 82,-44 30,-44\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- I -->\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>1</title>\n",
+        "<ellipse cx=\"56\" cy=\"-70\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-66.3\">1</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;1</title>\n",
+        "<path d=\"M1.15491,-70C2.79388,-70 17.1543,-70 30.6317,-70\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-70 30.9419,-73.1501 34.4419,-70 30.9419,-70.0001 30.9419,-70.0001 30.9419,-70.0001 34.4419,-70 30.9418,-66.8501 37.9419,-70 37.9419,-70\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>0</title>\n",
+        "<ellipse cx=\"165\" cy=\"-172\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"165\" y=\"-168.3\">0</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;0</title>\n",
+        "<path d=\"M69.6945,-82.1013C88.6787,-100.198 124.54,-134.384 146.153,-154.987\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"151.322,-159.914 144.082,-157.365 148.789,-157.499 146.255,-155.084 146.255,-155.084 146.255,-155.084 148.789,-157.499 148.429,-152.804 151.322,-159.914 151.322,-159.914\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"107\" y=\"-140.8\">a</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node7\"><title>2</title>\n",
+        "<ellipse cx=\"417\" cy=\"-34\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"417\" y=\"-30.3\">2</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;2</title>\n",
+        "<path d=\"M72.3408,-61.7789C88.538,-53.3659 115,-40.3728 139,-32 165.768,-22.6614 172.849,-20.3569 201,-17 270.302,-8.73591 352.668,-21.519 392.332,-29.0808\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"399.229,-30.4257 391.755,-32.1775 395.793,-29.7558 392.358,-29.0858 392.358,-29.0858 392.358,-29.0858 395.793,-29.7558 392.961,-25.994 399.229,-30.4257 399.229,-30.4257\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"211.5\" y=\"-20.8\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node8\"><title>3</title>\n",
+        "<ellipse cx=\"165\" cy=\"-70\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#5da5da\" stroke-width=\"2\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"165\" y=\"-66.3\">3</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;3</title>\n",
+        "<path d=\"M74.1914,-70C91.8968,-70 119.648,-70 139.616,-70\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"146.851,-70 139.851,-73.1501 143.351,-70 139.851,-70.0001 139.851,-70.0001 139.851,-70.0001 143.351,-70 139.851,-66.8501 146.851,-70 146.851,-70\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-73.8\">!a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
+        "<path d=\"M155.767,-187.541C153.169,-197.909 156.246,-208 165,-208 171.702,-208 175.077,-202.085 175.124,-194.659\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"174.233,-187.541 178.229,-194.095 174.668,-191.014 175.103,-194.487 175.103,-194.487 175.103,-194.487 174.668,-191.014 171.977,-194.879 174.233,-187.541 174.233,-187.541\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"160.5\" y=\"-226.8\">1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"157\" y=\"-211.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>4</title>\n",
+        "<ellipse cx=\"496\" cy=\"-92\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#f17cb0\" stroke-width=\"2\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"496\" y=\"-88.3\">4</text>\n",
+        "</g>\n",
+        "<!-- 6 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>6</title>\n",
+        "<ellipse cx=\"584\" cy=\"-104\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#f17cb0\" stroke-width=\"2\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"584\" y=\"-100.3\">6</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;6 -->\n",
+        "<g class=\"edge\" id=\"edge11\"><title>4-&gt;6</title>\n",
+        "<path d=\"M514.116,-90.6026C524.071,-90.1368 536.821,-90.1368 548,-92 552.14,-92.6901 556.447,-93.8097 560.566,-95.0946\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"567.258,-97.3664 559.617,-98.0987 563.943,-96.2412 560.629,-95.1159 560.629,-95.1159 560.629,-95.1159 563.943,-96.2412 561.642,-92.1331 567.258,-97.3664 567.258,-97.3664\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"534.5\" y=\"-95.8\">!c</text>\n",
+        "</g>\n",
+        "<!-- 7 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>7</title>\n",
+        "<ellipse cx=\"697\" cy=\"-109\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#f17cb0\" stroke-width=\"2\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"697\" y=\"-105.3\">7</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;7 -->\n",
+        "<g class=\"edge\" id=\"edge12\"><title>4-&gt;7</title>\n",
+        "<path d=\"M512.019,-83.315C525.609,-75.9906 546.433,-66.0696 566,-62 581.665,-58.7419 586.276,-59.0434 602,-62 629.66,-67.2007 636.12,-71.8443 661,-85 666.129,-87.7121 671.415,-91.0267 676.275,-94.3165\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"682.16,-98.4231 674.617,-97.0007 679.29,-96.4202 676.42,-94.4174 676.42,-94.4174 676.42,-94.4174 679.29,-96.4202 678.222,-91.8341 682.16,-98.4231 682.16,-98.4231\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"580.5\" y=\"-65.8\">c</text>\n",
+        "</g>\n",
+        "<!-- 6&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge16\"><title>6-&gt;4</title>\n",
+        "<path d=\"M565.841,-107.212C555.871,-108.533 543.121,-109.283 532,-107 527.58,-106.093 523.029,-104.603 518.732,-102.906\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"512.241,-100.123 519.916,-99.9868 515.458,-101.502 518.675,-102.882 518.675,-102.882 518.675,-102.882 515.458,-101.502 517.433,-105.777 512.241,-100.123 512.241,-100.123\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"533.5\" y=\"-127.8\">!b</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"532\" y=\"-112.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 6&#45;&gt;6 -->\n",
+        "<g class=\"edge\" id=\"edge17\"><title>6-&gt;6</title>\n",
+        "<path d=\"M576.332,-120.29C574.483,-130.389 577.039,-140 584,-140 589.221,-140 591.964,-134.594 592.229,-127.63\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"591.668,-120.29 595.342,-127.03 591.935,-123.78 592.201,-127.27 592.201,-127.27 592.201,-127.27 591.935,-123.78 589.06,-127.51 591.668,-120.29 591.668,-120.29\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"565.5\" y=\"-143.8\">b &amp; !c</text>\n",
+        "</g>\n",
+        "<!-- 6&#45;&gt;7 -->\n",
+        "<g class=\"edge\" id=\"edge18\"><title>6-&gt;7</title>\n",
+        "<path d=\"M600.694,-96.8164C606.614,-94.4708 613.493,-92.1695 620,-91 637.935,-87.7768 643.289,-86.7127 661,-91 665.73,-92.1449 670.537,-94.0459 675.012,-96.1937\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"681.283,-99.4577 673.62,-99.0202 678.178,-97.8418 675.074,-96.226 675.074,-96.226 675.074,-96.226 678.178,-97.8418 676.528,-93.4318 681.283,-99.4577 681.283,-99.4577\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"623.5\" y=\"-94.8\">b &amp; c</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge19\"><title>7-&gt;4</title>\n",
+        "<path d=\"M683.103,-120.93C660.18,-140.644 610.556,-176.651 566,-164 548.914,-159.149 544.858,-155.253 532,-143 523.072,-134.492 515.111,-123.354 509.045,-113.657\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"505.342,-107.536 511.661,-111.895 507.154,-110.531 508.966,-113.525 508.966,-113.525 508.966,-113.525 507.154,-110.531 506.27,-115.156 505.342,-107.536 505.342,-107.536\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"579.5\" y=\"-184.8\">b</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"576\" y=\"-169.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;6 -->\n",
+        "<g class=\"edge\" id=\"edge20\"><title>7-&gt;6</title>\n",
+        "<path d=\"M678.791,-108.407C663.385,-107.856 640.18,-106.975 620,-106 616.535,-105.833 612.878,-105.641 609.286,-105.443\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"602.087,-105.037 609.253,-102.287 605.581,-105.234 609.076,-105.431 609.076,-105.431 609.076,-105.431 605.581,-105.234 608.898,-108.576 602.087,-105.037 602.087,-105.037\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"620\" y=\"-111.8\">!b &amp; !c</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;7 -->\n",
+        "<g class=\"edge\" id=\"edge21\"><title>7-&gt;7</title>\n",
+        "<path d=\"M687.425,-124.541C684.73,-134.909 687.922,-145 697,-145 703.95,-145 707.45,-139.085 707.499,-131.659\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"706.575,-124.541 710.6,-131.077 707.026,-128.012 707.477,-131.483 707.477,-131.483 707.477,-131.483 707.026,-128.012 704.353,-131.889 706.575,-124.541 706.575,-124.541\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"678.5\" y=\"-148.8\">!b &amp; c</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;4</title>\n",
+        "<path d=\"M432.606,-43.6256C440.786,-49.1295 451.099,-56.26 460,-63 465.452,-67.1281 471.223,-71.7844 476.473,-76.1383\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"481.925,-80.7047 474.536,-78.625 479.242,-78.4574 476.558,-76.21 476.558,-76.21 476.558,-76.21 479.242,-78.4574 478.581,-73.7951 481.925,-80.7047 481.925,-80.7047\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"453\" y=\"-66.8\">a</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;4</title>\n",
+        "<path d=\"M172.788,-86.4554C178.475,-97.8739 187.8,-112.207 201,-119 292.409,-166.041 421.048,-122.799 472.473,-101.867\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"479.204,-99.0728 473.947,-104.666 475.972,-100.414 472.739,-101.756 472.739,-101.756 472.739,-101.756 475.972,-100.414 471.532,-98.8468 479.204,-99.0728 479.204,-99.0728\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"357\" y=\"-141.8\">a</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;2</title>\n",
+        "<path d=\"M181.764,-62.7925C187.692,-60.3237 194.557,-57.7464 201,-56 268.503,-37.7027 351.689,-34.3871 391.933,-33.9368\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"398.934,-33.8831 391.959,-37.0868 395.435,-33.91 391.935,-33.9369 391.935,-33.9369 391.935,-33.9369 395.435,-33.91 391.91,-30.787 398.934,-33.8831 398.934,-33.8831\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"281\" y=\"-44.8\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;3</title>\n",
+        "<path d=\"M155.767,-85.5414C153.169,-95.9087 156.246,-106 165,-106 171.702,-106 175.077,-100.085 175.124,-92.6591\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"174.233,-85.5414 178.229,-92.0955 174.668,-89.0143 175.103,-92.4871 175.103,-92.4871 175.103,-92.4871 174.668,-89.0143 171.977,-92.8788 174.233,-85.5414 174.233,-85.5414\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"132\" y=\"-109.8\">!a &amp; b &amp; !c</text>\n",
+        "</g>\n",
+        "<!-- 5 -->\n",
+        "<g class=\"node\" id=\"node9\"><title>5</title>\n",
+        "<ellipse cx=\"301.5\" cy=\"-86\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#5da5da\" stroke-width=\"2\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"301.5\" y=\"-82.3\">5</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;5 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>3-&gt;5</title>\n",
+        "<path d=\"M182.479,-65.4387C202.062,-60.7826 235.539,-55.2494 263,-63 269.128,-64.7296 275.242,-67.7722 280.702,-71.0891\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"286.771,-75.0467 279.187,-73.8619 283.839,-73.135 280.907,-71.2233 280.907,-71.2233 280.907,-71.2233 283.839,-73.135 282.628,-68.5846 286.771,-75.0467 286.771,-75.0467\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"201\" y=\"-66.8\">!a &amp; b &amp; c</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge15\"><title>5-&gt;4</title>\n",
+        "<path d=\"M319.583,-86.5325C353.83,-87.5999 430.982,-90.0046 470.564,-91.2383\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"477.955,-91.4687 470.86,-94.399 474.457,-91.3596 470.959,-91.2506 470.959,-91.2506 470.959,-91.2506 474.457,-91.3596 471.057,-88.1021 477.955,-91.4687 477.955,-91.4687\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"413.5\" y=\"-94.8\">a</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge13\"><title>5-&gt;2</title>\n",
+        "<path d=\"M316.747,-76.3975C323.606,-72.0012 332.051,-66.912 340,-63 357.251,-54.5098 377.649,-46.8478 392.967,-41.5345\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"399.618,-39.264 394.011,-44.5067 396.306,-40.3948 392.994,-41.5256 392.994,-41.5256 392.994,-41.5256 396.306,-40.3948 391.976,-38.5445 399.618,-39.264 399.618,-39.264\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"340\" y=\"-66.8\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge14\"><title>5-&gt;3</title>\n",
+        "<path d=\"M283.156,-85.3654C263.232,-84.4607 229.605,-82.3956 201,-78 197.321,-77.4347 193.454,-76.6977 189.686,-75.9\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"182.64,-74.3203 190.16,-72.7781 186.055,-75.086 189.471,-75.8518 189.471,-75.8518 189.471,-75.8518 186.055,-75.086 188.781,-78.9255 182.64,-74.3203 182.64,-74.3203\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"213.5\" y=\"-103.8\">!a &amp; b</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"224\" y=\"-88.8\">\u2776</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG object>"
+       ]
+      }
+     ],
+     "prompt_number": 20
     }
    ],
    "metadata": {}
   }
  ]
-}
\ No newline at end of file
+}