diff --git a/NEWS b/NEWS
index 20c027cbb..e2a376583 100644
--- a/NEWS
+++ b/NEWS
@@ -57,6 +57,8 @@ New in spot 1.99.5a (not yet released)
 
   Bug fixes:
   * automaton parser was ignoring the "unambiguous" property.
+  * --dot=Bb should work like --dot=b, allowing us to disable
+    a B option set via an environment variable.
 
 New in spot 1.99.5 (2015-11-03)
 
diff --git a/src/twaalgos/dot.cc b/src/twaalgos/dot.cc
index 63bc09b47..3b7476c02 100644
--- a/src/twaalgos/dot.cc
+++ b/src/twaalgos/dot.cc
@@ -119,6 +119,7 @@ namespace spot
 	      break;
 	    case 'b':
 	      opt_bullet = true;
+	      opt_bullet_but_buchi = false;
 	      break;
 	    case 'B':
 	      opt_bullet = true;
diff --git a/wrap/python/tests/decompose.ipynb b/wrap/python/tests/decompose.ipynb
index 80d4b12e9..a153db058 100644
--- a/wrap/python/tests/decompose.ipynb
+++ b/wrap/python/tests/decompose.ipynb
@@ -18,7 +18,7 @@
    "version": "3.4.3+"
   },
   "name": "",
-  "signature": "sha256:80d55ee45e6262dfcb29a53e9df5940e6a49ea8584e10e97963faeee4ace738a"
+  "signature": "sha256:3d73c80c329ce7b32e9edaa2470fce5e27744462f43431affbbb771deb92aff2"
  },
  "nbformat": 3,
  "nbformat_minor": 0,
@@ -203,7 +203,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd4fcc39198>"
+        "<IPython.core.display.SVG at 0x7fe3f4c0c588>"
        ]
       }
      ],
@@ -314,7 +314,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd505085f60>"
+        "<IPython.core.display.SVG at 0x7fe3fc364da0>"
        ]
       }
      ],
@@ -449,7 +449,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd4fc0f2978>"
+        "<IPython.core.display.SVG at 0x7fe3fc38b860>"
        ]
       }
      ],
@@ -533,7 +533,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd4fc1329b0>"
+        "<IPython.core.display.SVG at 0x7fe3fc3a0518>"
        ]
       }
      ],
@@ -604,7 +604,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd4fcbe7720> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe3f46e3f00> >"
        ]
       }
      ],
@@ -713,7 +713,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd505047cf8>"
+        "<IPython.core.display.SVG at 0x7fe3fc367c50>"
        ]
       },
       {
@@ -830,7 +830,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd5050739e8>"
+        "<IPython.core.display.SVG at 0x7fe3fc3c3748>"
        ]
       },
       {
@@ -966,7 +966,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd504fe65f8>"
+        "<IPython.core.display.SVG at 0x7fe3fc346358>"
        ]
       }
      ],
@@ -1364,7 +1364,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd505047a58>"
+        "<IPython.core.display.SVG at 0x7fe3fc367978>"
        ]
       }
      ],
@@ -1384,7 +1384,7 @@
       "for (name, opt) in (('terminal', 't'), ('strictly weak', 'w'), ('strong', 's')):\n",
       "    a = spot.decompose_strength(aut, opt)\n",
       "    a.set_name(name)\n",
-      "    display(a.show('.asn'))"
+      "    display(a.show('.basn'))"
      ],
      "language": "python",
      "metadata": {},
@@ -1393,16 +1393,16 @@
        "metadata": {},
        "output_type": "display_data",
        "svg": [
-        "<svg height=\"360pt\" viewBox=\"0.00 0.00 543.00 360.00\" width=\"543pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<svg height=\"360pt\" viewBox=\"0.00 0.00 548.84 360.00\" width=\"549pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
         "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.6 0.6) rotate(0) translate(4 596)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-596 901,-596 901,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"422.5\" y=\"-577.8\">terminal</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"427.5\" y=\"-563.8\">Inf(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"449.5\" y=\"-563.8\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"465.5\" y=\"-563.8\">)</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-596 910.74,-596 910.74,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"427.37\" y=\"-577.8\">terminal</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"432.37\" y=\"-563.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"454.37\" y=\"-563.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"470.37\" y=\"-563.8\">)</text>\n",
         "<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
-        "<polygon fill=\"none\" points=\"829,-265 829,-358 889,-358 889,-265 829,-265\" stroke=\"green\"/>\n",
+        "<polygon fill=\"none\" points=\"829,-260 829,-363 898.74,-363 898.74,-260 829,-260\" stroke=\"green\"/>\n",
         "</g>\n",
         "<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
         "<polygon fill=\"none\" points=\"746,-212 746,-297 798,-297 798,-212 746,-212\" stroke=\"red\"/>\n",
@@ -1435,14 +1435,14 @@
         "</g>\n",
         "<!-- 4 -->\n",
         "<g class=\"node\" id=\"node3\"><title>4</title>\n",
-        "<ellipse cx=\"859\" cy=\"-295\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"859\" cy=\"-295\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"859\" y=\"-291.3\">4</text>\n",
+        "<ellipse cx=\"863.87\" cy=\"-295\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"859.37\" y=\"-298.8\">4</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"855.87\" y=\"-283.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge5\"><title>0-&gt;4</title>\n",
-        "<path d=\"M58.0785,-303.931C62.6265,-361.975 85.3776,-541 193,-541 193,-541 193,-541 773,-541 802.871,-541 805.349,-518.569 819,-492 847.2,-437.115 855.049,-363.961 857.207,-324.031\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"857.547,-316.974 860.356,-324.118 857.379,-320.47 857.21,-323.966 857.21,-323.966 857.21,-323.966 857.379,-320.47 854.064,-323.814 857.547,-316.974 857.547,-316.974\" stroke=\"black\"/>\n",
+        "<path d=\"M58.0785,-303.931C62.6265,-361.975 85.3776,-541 193,-541 193,-541 193,-541 773,-541 801.6,-541 805.147,-521.021 819,-496 848.54,-442.645 858.191,-371.045 861.343,-329.275\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"861.843,-322.084 864.5,-329.286 861.6,-325.575 861.357,-329.067 861.357,-329.067 861.357,-329.067 861.6,-325.575 858.215,-328.848 861.843,-322.084 861.843,-322.084\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"485.5\" y=\"-544.8\">c</text>\n",
         "</g>\n",
         "<!-- 3 -->\n",
@@ -1480,9 +1480,9 @@
         "</g>\n",
         "<!-- 4&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge20\"><title>4-&gt;4</title>\n",
-        "<path d=\"M850.994,-315.581C849.886,-325.845 852.555,-335 859,-335 863.834,-335 866.544,-329.85 867.129,-322.945\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"867.006,-315.581 870.273,-322.527 867.065,-319.08 867.123,-322.58 867.123,-322.58 867.123,-322.58 867.065,-319.08 863.973,-322.632 867.006,-315.581 867.006,-315.581\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"859\" y=\"-338.8\">1</text>\n",
+        "<path d=\"M854.577,-320.37C853.937,-330.924 857.034,-339.87 863.87,-339.87 869.104,-339.87 872.146,-334.626 872.997,-327.431\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"873.163,-320.37 876.148,-327.442 873.081,-323.869 872.999,-327.368 872.999,-327.368 872.999,-327.368 873.081,-323.869 869.849,-327.294 873.163,-320.37 873.163,-320.37\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"863.87\" y=\"-343.67\">1</text>\n",
         "</g>\n",
         "<!-- 7 -->\n",
         "<g class=\"node\" id=\"node4\"><title>7</title>\n",
@@ -1491,9 +1491,9 @@
         "</g>\n",
         "<!-- 7&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge32\"><title>7-&gt;4</title>\n",
-        "<path d=\"M787.419,-247.669C800.184,-256.229 819.066,-268.891 834.089,-278.966\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"840.262,-283.105 832.694,-281.823 837.355,-281.156 834.448,-279.206 834.448,-279.206 834.448,-279.206 837.355,-281.156 836.203,-276.59 840.262,-283.105 840.262,-283.105\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"808\" y=\"-272.8\">!a</text>\n",
+        "<path d=\"M787.84,-247.412C800.516,-255.452 819.104,-267.242 834.608,-277.075\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"840.597,-280.874 832.999,-279.784 837.642,-278.999 834.686,-277.124 834.686,-277.124 834.686,-277.124 837.642,-278.999 836.373,-274.464 840.597,-280.874 840.597,-280.874\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"808\" y=\"-270.8\">!a</text>\n",
         "</g>\n",
         "<!-- 7&#45;&gt;7 -->\n",
         "<g class=\"edge\" id=\"edge31\"><title>7-&gt;7</title>\n",
@@ -1508,8 +1508,8 @@
         "</g>\n",
         "<!-- 8&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge34\"><title>8-&gt;4</title>\n",
-        "<path d=\"M786.488,-44.8498C797.043,-54.1116 811.199,-68.3829 819,-84 848.838,-143.733 856.012,-223.256 857.632,-265.576\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"857.867,-272.784 854.49,-265.89 857.753,-269.286 857.638,-265.787 857.638,-265.787 857.638,-265.787 857.753,-269.286 860.787,-265.685 857.867,-272.784 857.867,-272.784\" stroke=\"black\"/>\n",
+        "<path d=\"M786.396,-44.8966C796.897,-54.1856 811.026,-68.4705 819,-84 848.566,-141.579 858.206,-217.69 861.349,-260.995\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"861.832,-268.172 858.219,-261.399 861.597,-264.679 861.362,-261.187 861.362,-261.187 861.362,-261.187 861.597,-264.679 864.505,-260.976 861.832,-268.172 861.832,-268.172\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"808\" y=\"-87.8\">!a</text>\n",
         "</g>\n",
         "<!-- 8&#45;&gt;7 -->\n",
@@ -1531,9 +1531,9 @@
         "</g>\n",
         "<!-- 5&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge24\"><title>5-&gt;4</title>\n",
-        "<path d=\"M340.203,-306.023C345.664,-320.87 355.753,-341.744 372,-353 403.111,-374.554 418.281,-363.878 456,-367 608.731,-379.64 649.312,-360.127 798,-323 807.418,-320.648 810.044,-320.744 819,-317 823.832,-314.98 828.823,-312.499 833.553,-309.94\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"839.802,-306.439 835.235,-312.608 836.749,-308.149 833.696,-309.86 833.696,-309.86 833.696,-309.86 836.749,-308.149 832.156,-307.112 839.802,-306.439 839.802,-306.439\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"620\" y=\"-368.8\">!a &amp; c</text>\n",
+        "<path d=\"M340.203,-306.023C345.664,-320.87 355.753,-341.744 372,-353 403.111,-374.554 418.281,-363.878 456,-367 618.488,-380.448 664.221,-365.253 819,-314 823.447,-312.527 828.065,-310.781 832.563,-308.952\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"839.033,-306.237 833.797,-311.851 835.806,-307.592 832.579,-308.946 832.579,-308.946 832.579,-308.946 835.806,-307.592 831.36,-306.041 839.033,-306.237 839.033,-306.237\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"620\" y=\"-371.8\">!a &amp; c</text>\n",
         "</g>\n",
         "<!-- 5&#45;&gt;7 -->\n",
         "<g class=\"edge\" id=\"edge22\"><title>5-&gt;7</title>\n",
@@ -1555,9 +1555,9 @@
         "</g>\n",
         "<!-- 3&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge18\"><title>3-&gt;4</title>\n",
-        "<path d=\"M505.785,-296.693C515.418,-300.955 528.126,-305.82 540,-308 645.842,-327.432 774.689,-309.774 830.281,-300.213\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"837.317,-298.978 830.967,-303.29 833.87,-299.583 830.422,-300.188 830.422,-300.188 830.422,-300.188 833.87,-299.583 829.878,-297.085 837.317,-298.978 837.317,-298.978\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"701.5\" y=\"-320.8\">c</text>\n",
+        "<path d=\"M505.785,-296.693C515.418,-300.955 528.126,-305.82 540,-308 573.477,-314.146 655.533,-310.125 798,-301 808.354,-300.337 819.617,-299.378 829.809,-298.422\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"837.012,-297.729 830.345,-301.535 833.528,-298.064 830.044,-298.399 830.044,-298.399 830.044,-298.399 833.528,-298.064 829.743,-295.264 837.012,-297.729 837.012,-297.729\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"701.5\" y=\"-312.8\">c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;5 -->\n",
         "<g class=\"edge\" id=\"edge16\"><title>3-&gt;5</title>\n",
@@ -1584,8 +1584,8 @@
         "</g>\n",
         "<!-- 6&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge28\"><title>6-&gt;4</title>\n",
-        "<path d=\"M642.992,-220.687C647.593,-205.147 656.835,-183.253 674,-173 697.657,-158.87 708.779,-168.718 736,-173 764.602,-177.499 775.406,-174.894 798,-193 822.369,-212.528 838.951,-244.824 848.404,-267.843\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"850.995,-274.367 845.483,-269.024 849.703,-271.114 848.411,-267.861 848.411,-267.861 848.411,-267.861 849.703,-271.114 851.338,-266.698 850.995,-274.367 850.995,-274.367\" stroke=\"black\"/>\n",
+        "<path d=\"M642.992,-220.687C647.593,-205.147 656.835,-183.253 674,-173 697.657,-158.87 708.779,-168.718 736,-173 764.602,-177.499 775.095,-175.289 798,-193 821.724,-211.343 839.174,-240.989 849.964,-263.604\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"852.964,-270.078 847.162,-265.051 851.492,-266.902 850.02,-263.726 850.02,-263.726 850.02,-263.726 851.492,-266.902 852.879,-262.402 852.964,-270.078 852.964,-270.078\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"754\" y=\"-196.8\">!a &amp; c</text>\n",
         "</g>\n",
         "<!-- 6&#45;&gt;7 -->\n",
@@ -1620,14 +1620,14 @@
         "</g>\n",
         "<!-- 1&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge9\"><title>1-&gt;4</title>\n",
-        "<path d=\"M201.25,-397.774C207.007,-411.366 216.678,-430.283 230,-443 267.092,-478.41 281.719,-495 333,-495 333,-495 333,-495 773,-495 846.297,-495 857.298,-379.815 858.342,-324.272\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"858.427,-317.168 861.493,-324.205 858.385,-320.667 858.343,-324.167 858.343,-324.167 858.343,-324.167 858.385,-320.667 855.193,-324.129 858.427,-317.168 858.427,-317.168\" stroke=\"black\"/>\n",
+        "<path d=\"M201.047,-397.796C206.737,-411.644 216.419,-431.047 230,-444 266.965,-479.255 281.918,-495 333,-495 333,-495 333,-495 773,-495 844.915,-495 859.631,-386.081 862.405,-329\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"862.699,-321.973 865.554,-329.098 862.553,-325.47 862.407,-328.967 862.407,-328.967 862.407,-328.967 862.553,-325.47 859.26,-328.835 862.699,-321.973 862.699,-321.973\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"553\" y=\"-498.8\">!a &amp; c</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;7 -->\n",
         "<g class=\"edge\" id=\"edge7\"><title>1-&gt;7</title>\n",
-        "<path d=\"M207.946,-393.044C231.127,-413.301 282.077,-452 333,-452 333,-452 333,-452 572,-452 661.279,-452 682.033,-407.122 736,-336 752.509,-314.242 761.726,-284.007 766.505,-262.894\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"768.015,-255.835 769.631,-263.339 767.283,-259.257 766.551,-262.68 766.551,-262.68 766.551,-262.68 767.283,-259.257 763.47,-262.021 768.015,-255.835 768.015,-255.835\" stroke=\"black\"/>\n",
+        "<path d=\"M207.946,-393.044C231.127,-413.301 282.077,-452 333,-452 333,-452 333,-452 572,-452 663.378,-452 682.342,-401.965 736,-328 750.403,-308.146 759.775,-281.589 765.162,-262.475\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"767.034,-255.544 768.25,-263.123 766.122,-258.923 765.209,-262.302 765.209,-262.302 765.209,-262.302 766.122,-258.923 762.168,-261.481 767.034,-255.544 767.034,-255.544\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"473\" y=\"-455.8\">a &amp; c</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;5 -->\n",
@@ -1644,8 +1644,8 @@
         "</g>\n",
         "<!-- 2&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge13\"><title>2-&gt;4</title>\n",
-        "<path d=\"M210.94,-147.15C278.195,-119.324 544.129,-20.1344 736,-104 803.247,-133.393 837.266,-221.348 850.779,-266.926\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"852.773,-273.861 847.811,-268.004 851.806,-270.497 850.839,-267.134 850.839,-267.134 850.839,-267.134 851.806,-270.497 853.866,-266.263 852.773,-273.861 852.773,-273.861\" stroke=\"black\"/>\n",
+        "<path d=\"M210.94,-147.15C278.195,-119.324 544.129,-20.1344 736,-104 801.747,-132.738 837.806,-215.694 853.388,-262.274\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"855.628,-269.147 850.464,-263.467 854.543,-265.819 853.459,-262.491 853.459,-262.491 853.459,-262.491 854.543,-265.819 856.454,-261.516 855.628,-269.147 855.628,-269.147\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"553\" y=\"-76.8\">!a &amp; c</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;7 -->\n",
@@ -1682,23 +1682,23 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd504fe6588>"
+        "<IPython.core.display.SVG at 0x7fe3fc3462e8>"
        ]
       },
       {
        "metadata": {},
        "output_type": "display_data",
        "svg": [
-        "<svg height=\"278pt\" viewBox=\"0.00 0.00 734.00 277.87\" 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.897311 0.897311) rotate(0) translate(4 305.672)\">\n",
+        "<svg height=\"275pt\" viewBox=\"0.00 0.00 734.00 274.60\" 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.886752 0.886752) rotate(0) translate(4 305.672)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-305.672 814,-305.672 814,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"365\" y=\"-287.472\">strictly weak</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"384\" y=\"-273.472\">Inf(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"406\" y=\"-273.472\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"422\" y=\"-273.472\">)</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-305.672 823.74,-305.672 823.74,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"369.87\" y=\"-287.472\">strictly weak</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388.87\" y=\"-273.472\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"410.87\" y=\"-273.472\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"426.87\" y=\"-273.472\">)</text>\n",
         "<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
-        "<polygon fill=\"none\" points=\"742,-150.672 742,-243.672 802,-243.672 802,-150.672 742,-150.672\" stroke=\"green\"/>\n",
+        "<polygon fill=\"none\" points=\"742,-144.672 742,-247.672 811.74,-247.672 811.74,-144.672 742,-144.672\" stroke=\"green\"/>\n",
         "</g>\n",
         "<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
         "<polygon fill=\"none\" points=\"308,-31.6719 308,-167.672 664,-167.672 664,-31.6719 308,-31.6719\" stroke=\"red\"/>\n",
@@ -1758,15 +1758,15 @@
         "</g>\n",
         "<!-- 6 -->\n",
         "<g class=\"node\" id=\"node3\"><title>6</title>\n",
-        "<ellipse cx=\"772\" cy=\"-180.672\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"772\" cy=\"-180.672\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"772\" y=\"-176.972\">6</text>\n",
+        "<ellipse cx=\"776.87\" cy=\"-179.672\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"772.37\" y=\"-183.472\">6</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"768.87\" y=\"-168.472\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 6&#45;&gt;6 -->\n",
         "<g class=\"edge\" id=\"edge20\"><title>6-&gt;6</title>\n",
-        "<path d=\"M760.047,-199.188C757.391,-210.255 761.375,-220.672 772,-220.672 780.301,-220.672 784.548,-214.314 784.743,-206.255\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"783.953,-199.188 787.861,-205.794 784.342,-202.666 784.731,-206.144 784.731,-206.144 784.731,-206.144 784.342,-202.666 781.6,-206.494 783.953,-199.188 783.953,-199.188\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"755\" y=\"-224.472\">a &amp; b</text>\n",
+        "<path d=\"M763.7,-203.218C762.074,-214.544 766.464,-224.542 776.87,-224.542 785,-224.542 789.458,-218.44 790.244,-210.369\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"790.04,-203.218 793.388,-210.126 790.14,-206.717 790.24,-210.216 790.24,-210.216 790.24,-210.216 790.14,-206.717 787.091,-210.305 790.04,-203.218 790.04,-203.218\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"759.87\" y=\"-228.342\">a &amp; b</text>\n",
         "</g>\n",
         "<!-- 4 -->\n",
         "<g class=\"node\" id=\"node4\"><title>4</title>\n",
@@ -1793,8 +1793,8 @@
         "</g>\n",
         "<!-- 3&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
-        "<path d=\"M476.162,-70.5904C470.307,-81.8067 474.586,-93.6719 489,-93.6719 500.486,-93.6719 505.537,-86.1374 504.151,-77.4008\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"501.838,-70.5904 507.072,-76.2049 502.963,-73.9043 504.089,-77.2183 504.089,-77.2183 504.089,-77.2183 502.963,-73.9043 501.107,-78.2316 501.838,-70.5904 501.838,-70.5904\" stroke=\"black\"/>\n",
+        "<path d=\"M476.289,-70.9645C470.857,-82.0689 475.094,-93.6719 489,-93.6719 500.082,-93.6719 505.023,-86.3039 503.825,-77.6915\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"501.711,-70.9645 506.814,-76.6985 502.76,-74.3036 503.809,-77.6427 503.809,-77.6427 503.809,-77.6427 502.76,-74.3036 500.804,-78.5868 501.711,-70.9645 501.711,-70.9645\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"469\" y=\"-97.4719\">!a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 5 -->\n",
@@ -1810,9 +1810,9 @@
         "</g>\n",
         "<!-- 5&#45;&gt;6 -->\n",
         "<g class=\"edge\" id=\"edge19\"><title>5-&gt;6</title>\n",
-        "<path d=\"M654.142,-116.931C676.586,-129.173 718.94,-152.275 746.022,-167.048\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"752.223,-170.43 744.57,-169.844 749.151,-168.754 746.078,-167.078 746.078,-167.078 746.078,-167.078 749.151,-168.754 747.587,-164.313 752.223,-170.43 752.223,-170.43\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"674\" y=\"-163.472\">a &amp; b &amp; c</text>\n",
+        "<path d=\"M654.435,-116.679C676.57,-128.161 717.767,-149.531 745.985,-164.17\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"752.505,-167.552 744.841,-167.125 749.398,-165.94 746.292,-164.328 746.292,-164.328 746.292,-164.328 749.398,-165.94 747.742,-161.532 752.505,-167.552 752.505,-167.552\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"674\" y=\"-161.472\">a &amp; b &amp; c</text>\n",
         "</g>\n",
         "<!-- 5&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge16\"><title>5-&gt;4</title>\n",
@@ -1846,8 +1846,8 @@
         "</g>\n",
         "<!-- 2&#45;&gt;6 -->\n",
         "<g class=\"edge\" id=\"edge10\"><title>2-&gt;6</title>\n",
-        "<path d=\"M205.963,-175.189C227.483,-200.087 277.978,-250.672 333,-250.672 333,-250.672 333,-250.672 639,-250.672 682.226,-250.672 725.108,-221.011 749.779,-200.305\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"755.352,-195.517 752.094,-202.468 752.697,-197.798 750.042,-200.079 750.042,-200.079 750.042,-200.079 752.697,-197.798 747.989,-197.689 755.352,-195.517 755.352,-195.517\" stroke=\"black\"/>\n",
+        "<path d=\"M205.963,-175.189C227.483,-200.087 277.978,-250.672 333,-250.672 333,-250.672 333,-250.672 639,-250.672 681.805,-250.672 724.538,-222.97 750.587,-202.173\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"756.204,-197.588 752.773,-204.455 753.492,-199.802 750.781,-202.015 750.781,-202.015 750.781,-202.015 753.492,-199.802 748.789,-199.575 756.204,-197.588 756.204,-197.588\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"460\" y=\"-254.472\">a &amp; b &amp; c</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;4 -->\n",
@@ -1872,7 +1872,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd4fd89fa20>"
+        "<IPython.core.display.SVG at 0x7fe3f4bf6c88>"
        ]
       },
       {
@@ -2045,7 +2045,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd504fe6588>"
+        "<IPython.core.display.SVG at 0x7fe3fc3462e8>"
        ]
       }
      ],
@@ -2373,7 +2373,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd504fe68d0>"
+        "<IPython.core.display.SVG at 0x7fe3fc346278>"
        ]
       }
      ],
@@ -2393,7 +2393,7 @@
       "for (name, opt) in (('terminal', 't'), ('strictly weak', 'w'), ('strong', 's')):\n",
       "    a = spot.decompose_strength(aut, opt).postprocess('deterministic', 'SBAcc')\n",
       "    a.set_name(name)\n",
-      "    display(a.show('.asn'))"
+      "    display(a.show('.basn'))"
      ],
      "language": "python",
      "metadata": {},
@@ -2402,227 +2402,227 @@
        "metadata": {},
        "output_type": "display_data",
        "svg": [
-        "<svg height=\"166pt\" viewBox=\"0.00 0.00 405.00 166.00\" width=\"405pt\" 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 162)\">\n",
+        "<svg height=\"171pt\" viewBox=\"0.00 0.00 414.74 171.00\" width=\"415pt\" 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 167)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-162 401,-162 401,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"172.5\" y=\"-143.8\">terminal</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"177.5\" y=\"-129.8\">Inf(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"199.5\" y=\"-129.8\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"215.5\" y=\"-129.8\">)</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-167 410.74,-167 410.74,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"177.37\" y=\"-148.8\">terminal</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"182.37\" y=\"-134.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"204.37\" y=\"-134.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"220.37\" y=\"-134.8\">)</text>\n",
         "<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
-        "<polygon fill=\"none\" points=\"329,-8 329,-101 389,-101 389,-8 329,-8\" stroke=\"green\"/>\n",
+        "<polygon fill=\"none\" points=\"329,-8 329,-111 398.74,-111 398.74,-8 329,-8\" stroke=\"green\"/>\n",
         "</g>\n",
         "<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
-        "<polygon fill=\"none\" points=\"246,-12 246,-97 298,-97 298,-12 246,-12\" stroke=\"red\"/>\n",
+        "<polygon fill=\"none\" points=\"246,-17 246,-102 298,-102 298,-17 246,-17\" stroke=\"red\"/>\n",
         "</g>\n",
         "<g class=\"cluster\" id=\"clust3\"><title>cluster_2</title>\n",
-        "<polygon fill=\"none\" points=\"30,-10 30,-97 194,-97 194,-10 30,-10\" stroke=\"red\"/>\n",
+        "<polygon fill=\"none\" points=\"30,-15 30,-102 194,-102 194,-15 30,-15\" stroke=\"red\"/>\n",
         "</g>\n",
         "<!-- I -->\n",
         "<!-- 2 -->\n",
         "<g class=\"node\" id=\"node2\"><title>2</title>\n",
-        "<ellipse cx=\"56\" cy=\"-36\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-32.3\">2</text>\n",
+        "<ellipse cx=\"56\" cy=\"-41\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-37.3\">2</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge1\"><title>I-&gt;2</title>\n",
-        "<path d=\"M1.15491,-36C2.79388,-36 17.1543,-36 30.6317,-36\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"37.9419,-36 30.9419,-39.1501 34.4419,-36 30.9419,-36.0001 30.9419,-36.0001 30.9419,-36.0001 34.4419,-36 30.9418,-32.8501 37.9419,-36 37.9419,-36\" stroke=\"black\"/>\n",
+        "<path d=\"M1.15491,-41C2.79388,-41 17.1543,-41 30.6317,-41\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-41 30.9419,-44.1501 34.4419,-41 30.9419,-41.0001 30.9419,-41.0001 30.9419,-41.0001 34.4419,-41 30.9418,-37.8501 37.9419,-41 37.9419,-41\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge6\"><title>2-&gt;2</title>\n",
-        "<path d=\"M49.6208,-53.0373C48.3189,-62.8579 50.4453,-72 56,-72 60.166,-72 62.4036,-66.8576 62.7128,-60.1433\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"62.3792,-53.0373 65.8541,-59.8818 62.5434,-56.5335 62.7076,-60.0296 62.7076,-60.0296 62.7076,-60.0296 62.5434,-56.5335 59.561,-60.1774 62.3792,-53.0373 62.3792,-53.0373\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"36\" y=\"-75.8\">!a &amp; !c</text>\n",
+        "<path d=\"M49.6208,-58.0373C48.3189,-67.8579 50.4453,-77 56,-77 60.166,-77 62.4036,-71.8576 62.7128,-65.1433\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"62.3792,-58.0373 65.8541,-64.8818 62.5434,-61.5335 62.7076,-65.0296 62.7076,-65.0296 62.7076,-65.0296 62.5434,-61.5335 59.561,-65.1774 62.3792,-58.0373 62.3792,-58.0373\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"36\" y=\"-80.8\">!a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node3\"><title>0</title>\n",
-        "<ellipse cx=\"359\" cy=\"-38\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"359\" cy=\"-38\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"359\" y=\"-34.3\">0</text>\n",
+        "<ellipse cx=\"363.87\" cy=\"-43\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"359.37\" y=\"-46.8\">0</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"355.87\" y=\"-31.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge5\"><title>2-&gt;0</title>\n",
-        "<path d=\"M73.3004,-30.2748C112.507,-17.3288 214.985,11.5971 298,-8 310.484,-10.9471 323.332,-16.9114 333.92,-22.7512\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"340.197,-26.3431 332.557,-25.6004 337.159,-24.6047 334.122,-22.8664 334.122,-22.8664 334.122,-22.8664 337.159,-24.6047 335.686,-20.1323 340.197,-26.3431 340.197,-26.3431\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"216.5\" y=\"-6.8\">c</text>\n",
+        "<path d=\"M73.2626,-35.4408C112.387,-22.8585 214.696,5.32983 298,-13 310.243,-15.694 322.926,-20.9341 333.795,-26.2911\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"340.308,-29.62 332.642,-29.239 337.192,-28.027 334.075,-26.4341 334.075,-26.4341 334.075,-26.4341 337.192,-28.027 335.509,-23.6292 340.308,-29.62 340.308,-29.62\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"216.5\" y=\"-12.8\">c</text>\n",
         "</g>\n",
         "<!-- 3 -->\n",
         "<g class=\"node\" id=\"node5\"><title>3</title>\n",
-        "<ellipse cx=\"168\" cy=\"-38\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"168\" y=\"-34.3\">3</text>\n",
+        "<ellipse cx=\"168\" cy=\"-43\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"168\" y=\"-39.3\">3</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge7\"><title>2-&gt;3</title>\n",
-        "<path d=\"M74.2788,-36.1557C89.4809,-36.3106 112.211,-36.5854 132,-37 135.464,-37.0726 139.121,-37.1624 142.713,-37.2582\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"149.911,-37.4597 142.826,-40.4125 146.413,-37.3617 142.914,-37.2638 142.914,-37.2638 142.914,-37.2638 146.413,-37.3617 143.002,-34.115 149.911,-37.4597 149.911,-37.4597\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"94\" y=\"-40.8\">a &amp; !c</text>\n",
+        "<path d=\"M74.2788,-41.1557C89.4809,-41.3106 112.211,-41.5854 132,-42 135.464,-42.0726 139.121,-42.1624 142.713,-42.2582\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"149.911,-42.4597 142.826,-45.4125 146.413,-42.3617 142.914,-42.2638 142.914,-42.2638 142.914,-42.2638 146.413,-42.3617 143.002,-39.115 149.911,-42.4597 149.911,-42.4597\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"94\" y=\"-45.8\">a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
-        "<path d=\"M350.994,-58.5808C349.886,-68.8447 352.555,-78 359,-78 363.834,-78 366.544,-72.8502 367.129,-65.9451\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"367.006,-58.5808 370.273,-65.5273 367.065,-62.0803 367.123,-65.5798 367.123,-65.5798 367.123,-65.5798 367.065,-62.0803 363.973,-65.6324 367.006,-58.5808 367.006,-58.5808\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"359\" y=\"-81.8\">1</text>\n",
+        "<path d=\"M354.577,-68.37C353.937,-78.9238 357.034,-87.8701 363.87,-87.8701 369.104,-87.8701 372.146,-82.6259 372.997,-75.4312\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"373.163,-68.37 376.148,-75.4419 373.081,-71.869 372.999,-75.3681 372.999,-75.3681 372.999,-75.3681 373.081,-71.869 369.849,-75.2943 373.163,-68.37 373.163,-68.37\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"363.87\" y=\"-91.6701\">1</text>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g class=\"node\" id=\"node4\"><title>1</title>\n",
-        "<ellipse cx=\"272\" cy=\"-38\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"272\" y=\"-34.3\">1</text>\n",
+        "<ellipse cx=\"272\" cy=\"-43\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"272\" y=\"-39.3\">1</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge3\"><title>1-&gt;0</title>\n",
-        "<path d=\"M290.201,-38C301.58,-38 316.762,-38 329.875,-38\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"336.91,-38 329.91,-41.1501 333.41,-38 329.91,-38.0001 329.91,-38.0001 329.91,-38.0001 333.41,-38 329.91,-34.8501 336.91,-38 336.91,-38\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"308\" y=\"-41.8\">!a</text>\n",
+        "<path d=\"M290.328,-43C301.431,-43 316.206,-43 329.524,-43\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"336.74,-43 329.74,-46.1501 333.24,-43 329.74,-43.0001 329.74,-43.0001 329.74,-43.0001 333.24,-43 329.74,-39.8501 336.74,-43 336.74,-43\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"308\" y=\"-46.8\">!a</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge4\"><title>1-&gt;1</title>\n",
-        "<path d=\"M264.969,-54.6641C263.406,-64.625 265.75,-74 272,-74 276.688,-74 279.178,-68.7266 279.471,-61.8876\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"279.031,-54.6641 282.601,-61.4598 279.244,-58.1576 279.456,-61.6511 279.456,-61.6511 279.456,-61.6511 279.244,-58.1576 276.312,-61.8425 279.031,-54.6641 279.031,-54.6641\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"268.5\" y=\"-77.8\">a</text>\n",
+        "<path d=\"M264.969,-59.6641C263.406,-69.625 265.75,-79 272,-79 276.688,-79 279.178,-73.7266 279.471,-66.8876\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"279.031,-59.6641 282.601,-66.4598 279.244,-63.1576 279.456,-66.6511 279.456,-66.6511 279.456,-66.6511 279.244,-63.1576 276.312,-66.8425 279.031,-59.6641 279.031,-59.6641\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"268.5\" y=\"-82.8\">a</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge10\"><title>3-&gt;2</title>\n",
-        "<path d=\"M151.358,-45.733C145.443,-48.2587 138.555,-50.7376 132,-52 114.543,-55.3619 109.371,-55.7822 92,-52 87.5445,-51.0299 82.977,-49.4398 78.6739,-47.6293\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"72.1836,-44.6602 79.8596,-44.7078 75.3664,-46.1162 78.5492,-47.5723 78.5492,-47.5723 78.5492,-47.5723 75.3664,-46.1162 77.2387,-50.4368 72.1836,-44.6602 72.1836,-44.6602\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-58.8\">!a &amp; !c</text>\n",
+        "<path d=\"M151.358,-50.733C145.443,-53.2587 138.555,-55.7376 132,-57 114.543,-60.3619 109.371,-60.7822 92,-57 87.5445,-56.0299 82.977,-54.4398 78.6739,-52.6293\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"72.1836,-49.6602 79.8596,-49.7078 75.3664,-51.1162 78.5492,-52.5723 78.5492,-52.5723 78.5492,-52.5723 75.3664,-51.1162 77.2387,-55.4368 72.1836,-49.6602 72.1836,-49.6602\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-63.8\">!a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge8\"><title>3-&gt;0</title>\n",
-        "<path d=\"M180.109,-51.4827C193.757,-66.8742 218.509,-91.1866 246,-101 267.766,-108.77 276.758,-110.104 298,-101 316.343,-93.1388 331.734,-76.6106 342.334,-62.4558\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"346.579,-56.5669 345.041,-64.0875 344.532,-59.4063 342.486,-62.2457 342.486,-62.2457 342.486,-62.2457 344.532,-59.4063 339.93,-60.4039 346.579,-56.5669 346.579,-56.5669\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"254\" y=\"-110.8\">!a &amp; c</text>\n",
+        "<path d=\"M180.109,-56.4827C193.757,-71.8742 218.509,-96.1866 246,-106 267.766,-113.77 276.584,-114.688 298,-106 315.948,-98.7189 331.663,-83.8234 343.129,-70.3439\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"347.777,-64.68 345.772,-72.0896 345.557,-67.3857 343.337,-70.0913 343.337,-70.0913 343.337,-70.0913 345.557,-67.3857 340.902,-68.093 347.777,-64.68 347.777,-64.68\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"254\" y=\"-115.8\">!a &amp; c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge9\"><title>3-&gt;1</title>\n",
-        "<path d=\"M186.303,-38C202.962,-38 228.303,-38 246.927,-38\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"253.953,-38 246.953,-41.1501 250.453,-38 246.953,-38.0001 246.953,-38.0001 246.953,-38.0001 250.453,-38 246.953,-34.8501 253.953,-38 253.953,-38\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"204\" y=\"-41.8\">a &amp; c</text>\n",
+        "<path d=\"M186.303,-43C202.962,-43 228.303,-43 246.927,-43\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"253.953,-43 246.953,-46.1501 250.453,-43 246.953,-43.0001 246.953,-43.0001 246.953,-43.0001 250.453,-43 246.953,-39.8501 253.953,-43 253.953,-43\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"204\" y=\"-46.8\">a &amp; c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge11\"><title>3-&gt;3</title>\n",
-        "<path d=\"M159.021,-53.916C156.679,-64.1504 159.672,-74 168,-74 174.376,-74 177.625,-68.2263 177.746,-60.9268\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"176.979,-53.916 180.872,-60.5315 177.36,-57.3952 177.741,-60.8744 177.741,-60.8744 177.741,-60.8744 177.36,-57.3952 174.61,-61.2174 176.979,-53.916 176.979,-53.916\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"150\" y=\"-77.8\">a &amp; !c</text>\n",
+        "<path d=\"M159.021,-58.916C156.679,-69.1504 159.672,-79 168,-79 174.376,-79 177.625,-73.2263 177.746,-65.9268\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"176.979,-58.916 180.872,-65.5315 177.36,-62.3952 177.741,-65.8744 177.741,-65.8744 177.741,-65.8744 177.36,-62.3952 174.61,-66.2174 176.979,-58.916 176.979,-58.916\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"150\" y=\"-82.8\">a &amp; !c</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd4fd89fa20>"
+        "<IPython.core.display.SVG at 0x7fe3f4bf6c88>"
        ]
       },
       {
        "metadata": {},
        "output_type": "display_data",
        "svg": [
-        "<svg height=\"348pt\" viewBox=\"0.00 0.00 408.00 348.00\" width=\"408pt\" 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 344)\">\n",
+        "<svg height=\"358pt\" viewBox=\"0.00 0.00 417.74 358.00\" width=\"418pt\" 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 354)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-344 404,-344 404,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"160\" y=\"-325.8\">strictly weak</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"179\" y=\"-311.8\">Inf(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"201\" y=\"-311.8\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"217\" y=\"-311.8\">)</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-354 413.74,-354 413.74,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"164.87\" y=\"-335.8\">strictly weak</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"183.87\" y=\"-321.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"205.87\" y=\"-321.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"221.87\" y=\"-321.8\">)</text>\n",
         "<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
-        "<polygon fill=\"none\" points=\"332,-8 332,-101 392,-101 392,-8 332,-8\" stroke=\"green\"/>\n",
+        "<polygon fill=\"none\" points=\"332,-8 332,-111 401.74,-111 401.74,-8 332,-8\" stroke=\"green\"/>\n",
         "</g>\n",
         "<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
-        "<polygon fill=\"none\" points=\"30,-109 30,-296 388,-296 388,-109 30,-109\" stroke=\"red\"/>\n",
+        "<polygon fill=\"none\" points=\"30,-119 30,-306 392.87,-306 392.87,-119 30,-119\" stroke=\"red\"/>\n",
         "</g>\n",
         "<!-- I -->\n",
         "<!-- 2 -->\n",
         "<g class=\"node\" id=\"node2\"><title>2</title>\n",
-        "<ellipse cx=\"56\" cy=\"-208\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-204.3\">2</text>\n",
+        "<ellipse cx=\"56\" cy=\"-218\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-214.3\">2</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge1\"><title>I-&gt;2</title>\n",
-        "<path d=\"M1.15491,-208C2.79388,-208 17.1543,-208 30.6317,-208\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"37.9419,-208 30.9419,-211.15 34.4419,-208 30.9419,-208 30.9419,-208 30.9419,-208 34.4419,-208 30.9418,-204.85 37.9419,-208 37.9419,-208\" stroke=\"black\"/>\n",
+        "<path d=\"M1.15491,-218C2.79388,-218 17.1543,-218 30.6317,-218\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-218 30.9419,-221.15 34.4419,-218 30.9419,-218 30.9419,-218 30.9419,-218 34.4419,-218 30.9418,-214.85 37.9419,-218 37.9419,-218\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge6\"><title>2-&gt;2</title>\n",
-        "<path d=\"M49.6208,-225.037C48.3189,-234.858 50.4453,-244 56,-244 60.166,-244 62.4036,-238.858 62.7128,-232.143\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"62.3792,-225.037 65.8541,-231.882 62.5434,-228.533 62.7076,-232.03 62.7076,-232.03 62.7076,-232.03 62.5434,-228.533 59.561,-232.177 62.3792,-225.037 62.3792,-225.037\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"36\" y=\"-247.8\">!a &amp; !c</text>\n",
+        "<path d=\"M49.6208,-235.037C48.3189,-244.858 50.4453,-254 56,-254 60.166,-254 62.4036,-248.858 62.7128,-242.143\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"62.3792,-235.037 65.8541,-241.882 62.5434,-238.533 62.7076,-242.03 62.7076,-242.03 62.7076,-242.03 62.5434,-238.533 59.561,-242.177 62.3792,-235.037 62.3792,-235.037\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"36\" y=\"-257.8\">!a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g class=\"node\" id=\"node4\"><title>1</title>\n",
-        "<ellipse cx=\"362\" cy=\"-222\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"362\" y=\"-218.3\">1</text>\n",
+        "<ellipse cx=\"366.87\" cy=\"-232\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"366.87\" y=\"-228.3\">1</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge5\"><title>2-&gt;1</title>\n",
-        "<path d=\"M73.5774,-213.106C79.3504,-214.659 85.9075,-216.172 92,-217 115.794,-220.235 274.938,-221.499 336.629,-221.871\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"343.654,-221.912 336.635,-225.021 340.154,-221.892 336.654,-221.871 336.654,-221.871 336.654,-221.871 340.154,-221.892 336.672,-218.721 343.654,-221.912 343.654,-221.912\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"172\" y=\"-224.8\">a &amp; !b &amp; !c</text>\n",
+        "<path d=\"M73.5772,-223.108C79.3503,-224.66 85.9073,-226.173 92,-227 116.282,-230.297 279.008,-231.526 341.497,-231.88\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"348.604,-231.919 341.587,-235.031 345.104,-231.9 341.604,-231.881 341.604,-231.881 341.604,-231.881 345.104,-231.9 341.622,-228.731 348.604,-231.919 348.604,-231.919\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"172\" y=\"-233.8\">a &amp; !b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 3 -->\n",
         "<g class=\"node\" id=\"node5\"><title>3</title>\n",
-        "<ellipse cx=\"205\" cy=\"-135\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"205\" y=\"-131.3\">3</text>\n",
+        "<ellipse cx=\"205\" cy=\"-145\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"205\" y=\"-141.3\">3</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge7\"><title>2-&gt;3</title>\n",
-        "<path d=\"M64.0604,-191.651C69.8835,-180.153 79.2587,-165.378 92,-157 118.559,-139.537 155.808,-135.32 179.922,-134.607\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"186.958,-134.487 180.013,-137.756 183.459,-134.547 179.959,-134.606 179.959,-134.606 179.959,-134.606 183.459,-134.547 179.905,-131.457 186.958,-134.487 186.958,-134.487\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-160.8\">a &amp; b &amp; !c</text>\n",
+        "<path d=\"M64.0604,-201.651C69.8835,-190.153 79.2587,-175.378 92,-167 118.559,-149.537 155.808,-145.32 179.922,-144.607\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"186.958,-144.487 180.013,-147.756 183.459,-144.547 179.959,-144.606 179.959,-144.606 179.959,-144.606 183.459,-144.547 179.905,-141.457 186.958,-144.487 186.958,-144.487\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-170.8\">a &amp; b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node3\"><title>0</title>\n",
-        "<ellipse cx=\"362\" cy=\"-38\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"362\" cy=\"-38\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"362\" y=\"-34.3\">0</text>\n",
+        "<ellipse cx=\"366.87\" cy=\"-43\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"362.37\" y=\"-46.8\">0</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"358.87\" y=\"-31.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
-        "<path d=\"M349.453,-56.1003C346.427,-67.3213 350.609,-78 362,-78 370.899,-78 375.398,-71.4822 375.498,-63.2801\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"374.547,-56.1003 378.589,-62.6261 375.007,-59.57 375.467,-63.0397 375.467,-63.0397 375.467,-63.0397 375.007,-59.57 372.344,-63.4533 374.547,-56.1003 374.547,-56.1003\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"345\" y=\"-81.8\">a &amp; b</text>\n",
+        "<path d=\"M353.041,-66.0865C351.128,-77.6001 355.737,-87.8701 366.87,-87.8701 375.568,-87.8701 380.284,-81.6018 381.018,-73.3693\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"380.699,-66.0865 384.153,-72.9418 380.852,-69.5832 381.006,-73.0798 381.006,-73.0798 381.006,-73.0798 380.852,-69.5832 377.859,-73.2178 380.699,-66.0865 380.699,-66.0865\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"349.87\" y=\"-91.6701\">a &amp; b</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge4\"><title>1-&gt;2</title>\n",
-        "<path d=\"M344.328,-225.777C311.412,-232.77 235.737,-246.535 172,-241 136.039,-237.877 126.086,-238.877 92,-227 87.2624,-225.349 82.3986,-223.108 77.8606,-220.743\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"71.4979,-217.245 79.1496,-217.857 74.565,-218.931 77.632,-220.617 77.632,-220.617 77.632,-220.617 74.565,-218.931 76.1143,-223.378 71.4979,-217.245 71.4979,-217.245\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"185\" y=\"-245.8\">!a &amp; !c</text>\n",
+        "<path d=\"M349.026,-235.748C315.396,-242.767 237.532,-256.691 172,-251 136.039,-247.877 126.086,-248.877 92,-237 87.2624,-235.349 82.3986,-233.108 77.8606,-230.743\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"71.4979,-227.245 79.1496,-227.857 74.565,-228.931 77.632,-230.617 77.632,-230.617 77.632,-230.617 74.565,-228.931 76.1143,-233.378 71.4979,-227.245 71.4979,-227.245\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"185\" y=\"-255.8\">!a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge3\"><title>1-&gt;1</title>\n",
-        "<path d=\"M350.244,-236.042C345.847,-246.913 349.766,-258 362,-258 371.558,-258 376.041,-251.233 375.448,-243.089\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"373.756,-236.042 378.453,-242.113 374.573,-239.445 375.391,-242.848 375.391,-242.848 375.391,-242.848 374.573,-239.445 372.328,-243.584 373.756,-236.042 373.756,-236.042\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"344\" y=\"-261.8\">a &amp; !c</text>\n",
+        "<path d=\"M354.624,-245.667C349.726,-256.656 353.808,-268 366.87,-268 377.075,-268 381.799,-261.076 381.042,-252.807\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"379.116,-245.667 383.98,-251.605 380.027,-249.046 380.939,-252.426 380.939,-252.426 380.939,-252.426 380.027,-249.046 377.897,-253.246 379.116,-245.667 379.116,-245.667\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"348.87\" y=\"-271.8\">a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge10\"><title>3-&gt;2</title>\n",
-        "<path d=\"M190.695,-146.472C181.002,-154.411 167.295,-164.802 154,-172 130.12,-184.929 100.617,-195.142 80.4603,-201.338\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"73.7447,-203.36 79.5393,-198.326 77.0961,-202.351 80.4475,-201.342 80.4475,-201.342 80.4475,-201.342 77.0961,-202.351 81.3557,-204.358 73.7447,-203.36 73.7447,-203.36\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"103\" y=\"-201.8\">!a &amp; !c</text>\n",
+        "<path d=\"M190.695,-156.472C181.002,-164.411 167.295,-174.802 154,-182 130.12,-194.929 100.617,-205.142 80.4603,-211.338\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.7447,-213.36 79.5393,-208.326 77.0961,-212.351 80.4475,-211.342 80.4475,-211.342 80.4475,-211.342 77.0961,-212.351 81.3557,-214.358 73.7447,-213.36 73.7447,-213.36\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"103\" y=\"-211.8\">!a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge8\"><title>3-&gt;0</title>\n",
-        "<path d=\"M220.582,-125.874C247.288,-109.162 304.294,-73.4871 336.862,-53.1057\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"343.034,-49.2434 338.771,-55.6271 340.067,-51.1001 337.1,-52.9569 337.1,-52.9569 337.1,-52.9569 340.067,-51.1001 335.429,-50.2867 343.034,-49.2434 343.034,-49.2434\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"260\" y=\"-107.8\">a &amp; b &amp; c</text>\n",
+        "<path d=\"M220.469,-135.768C246.88,-118.918 303.33,-82.9016 337.604,-61.0343\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"343.733,-57.1236 339.526,-63.5443 340.783,-59.0062 337.832,-60.8888 337.832,-60.8888 337.832,-60.8888 340.783,-59.0062 336.138,-58.2332 343.733,-57.1236 343.733,-57.1236\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"260\" y=\"-116.8\">a &amp; b &amp; c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge9\"><title>3-&gt;1</title>\n",
-        "<path d=\"M221.144,-143.5C248.88,-159.068 307.895,-192.193 339.675,-210.031\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"346.022,-213.593 338.376,-212.914 342.97,-211.88 339.918,-210.167 339.918,-210.167 339.918,-210.167 342.97,-211.88 341.46,-207.42 346.022,-213.593 346.022,-213.593\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"256\" y=\"-202.8\">a &amp; !b &amp; !c</text>\n",
+        "<path d=\"M221.04,-153.185C249.606,-168.73 311.78,-202.565 344.6,-220.425\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"350.753,-223.774 343.099,-223.194 347.679,-222.101 344.605,-220.428 344.605,-220.428 344.605,-220.428 347.679,-222.101 346.111,-217.661 350.753,-223.774 350.753,-223.774\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"256\" y=\"-210.8\">a &amp; !b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge11\"><title>3-&gt;3</title>\n",
-        "<path d=\"M192.162,-147.918C186.307,-159.135 190.586,-171 205,-171 216.486,-171 221.537,-163.465 220.151,-154.729\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"217.838,-147.918 223.072,-153.533 218.963,-151.232 220.089,-154.546 220.089,-154.546 220.089,-154.546 218.963,-151.232 217.107,-155.56 217.838,-147.918 217.838,-147.918\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"174\" y=\"-174.8\">a &amp; b &amp; !c</text>\n",
+        "<path d=\"M192.289,-158.293C186.857,-169.397 191.094,-181 205,-181 216.082,-181 221.023,-173.632 219.825,-165.02\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"217.711,-158.293 222.814,-164.027 218.76,-161.632 219.809,-164.971 219.809,-164.971 219.809,-164.971 218.76,-161.632 216.804,-165.915 217.711,-158.293 217.711,-158.293\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"174\" y=\"-184.8\">a &amp; b &amp; !c</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd4fd89fa20>"
+        "<IPython.core.display.SVG at 0x7fe3f4bf6c88>"
        ]
       },
       {
@@ -2795,7 +2795,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd4fd89fa20>"
+        "<IPython.core.display.SVG at 0x7fe3f4bf6c88>"
        ]
       }
      ],
@@ -3145,7 +3145,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd505029630>"
+        "<IPython.core.display.SVG at 0x7fe3fc399438>"
        ]
       }
      ],
@@ -3158,7 +3158,7 @@
       "for (name, opt) in (('terminal', 't'), ('strictly weak', 'w'), ('strong', 's')):\n",
       "    a = spot.decompose_strength(aut, opt)\n",
       "    a.set_name(name)\n",
-      "    display(a.show('.asn'))"
+      "    display(a.show('.basn'))"
      ],
      "language": "python",
      "metadata": {},
@@ -3167,413 +3167,413 @@
        "metadata": {},
        "output_type": "display_data",
        "svg": [
-        "<svg height=\"360pt\" viewBox=\"0.00 0.00 675.63 360.00\" width=\"676pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.715706 0.715706) rotate(0) translate(4 499)\">\n",
+        "<svg height=\"360pt\" viewBox=\"0.00 0.00 676.61 360.00\" width=\"677pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.688337 0.688337) rotate(0) translate(4 519)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-499 940,-499 940,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"442\" y=\"-480.8\">terminal</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"447\" y=\"-466.8\">Inf(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"469\" y=\"-466.8\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"485\" y=\"-466.8\">)</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-519 978.96,-519 978.96,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"461.48\" y=\"-500.8\">terminal</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"466.48\" y=\"-486.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"488.48\" y=\"-486.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"504.48\" y=\"-486.8\">)</text>\n",
         "<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
-        "<polygon fill=\"none\" points=\"868,-105 868,-198 928,-198 928,-105 868,-105\" stroke=\"green\"/>\n",
+        "<polygon fill=\"none\" points=\"897.22,-100 897.22,-203 966.96,-203 966.96,-100 897.22,-100\" stroke=\"green\"/>\n",
         "</g>\n",
         "<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
-        "<polygon fill=\"none\" points=\"777,-216 777,-309 837,-309 837,-216 777,-216\" stroke=\"red\"/>\n",
+        "<polygon fill=\"none\" points=\"796.48,-219 796.48,-322 866.22,-322 866.22,-219 796.48,-219\" stroke=\"red\"/>\n",
         "</g>\n",
         "<g class=\"cluster\" id=\"clust3\"><title>cluster_2</title>\n",
-        "<polygon fill=\"none\" points=\"651,-160 651,-253 711,-253 711,-160 651,-160\" stroke=\"red\"/>\n",
+        "<polygon fill=\"none\" points=\"665.61,-160 665.61,-263 735.35,-263 735.35,-160 665.61,-160\" stroke=\"red\"/>\n",
         "</g>\n",
         "<g class=\"cluster\" id=\"clust4\"><title>cluster_3</title>\n",
-        "<polygon fill=\"none\" points=\"651,-331 651,-424 711,-424 711,-331 651,-331\" stroke=\"red\"/>\n",
+        "<polygon fill=\"none\" points=\"665.61,-341 665.61,-444 735.35,-444 735.35,-341 665.61,-341\" stroke=\"red\"/>\n",
         "</g>\n",
         "<g class=\"cluster\" id=\"clust5\"><title>cluster_4</title>\n",
-        "<polygon fill=\"none\" points=\"30,-143 30,-358 555,-358 555,-143 30,-143\" stroke=\"red\"/>\n",
+        "<polygon fill=\"none\" points=\"30,-148 30,-373 579.35,-373 579.35,-148 30,-148\" stroke=\"red\"/>\n",
         "</g>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node2\"><title>0</title>\n",
-        "<ellipse cx=\"60\" cy=\"-215\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"60\" cy=\"-215\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"60\" y=\"-211.3\">0</text>\n",
+        "<ellipse cx=\"64.8701\" cy=\"-219\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"60.3701\" y=\"-222.8\">0</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"56.8701\" y=\"-207.8\">\u2777</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
-        "<path d=\"M1.16638,-215C2.84121,-215 16.884,-215 30.7112,-215\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"37.8555,-215 30.8556,-218.15 34.3555,-215 30.8555,-215 30.8555,-215 30.8555,-215 34.3555,-215 30.8555,-211.85 37.8555,-215 37.8555,-215\" stroke=\"black\"/>\n",
+        "<path d=\"M1.04557,-219C1.94668,-219 16.0699,-219 30.6965,-219\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.8616,-219 30.8617,-222.15 34.3616,-219 30.8616,-219 30.8616,-219 30.8616,-219 34.3616,-219 30.8616,-215.85 37.8616,-219 37.8616,-219\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge5\"><title>0-&gt;0</title>\n",
-        "<path d=\"M52.6831,-235.991C51.7798,-246.087 54.2188,-255 60,-255 64.3359,-255 66.7918,-249.987 67.3677,-243.22\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"67.3169,-235.991 70.5161,-242.968 67.3415,-239.491 67.3662,-242.991 67.3662,-242.991 67.3662,-242.991 67.3415,-239.491 64.2163,-243.013 67.3169,-235.991 67.3169,-235.991\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"40\" y=\"-258.8\">!a &amp; !c</text>\n",
+        "<path d=\"M56.6704,-244.821C56.2072,-255.178 58.9404,-263.87 64.8701,-263.87 69.3173,-263.87 71.9666,-258.981 72.8178,-252.167\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.0697,-244.821 75.9779,-251.925 72.9497,-248.319 72.8297,-251.817 72.8297,-251.817 72.8297,-251.817 72.9497,-248.319 69.6816,-251.709 73.0697,-244.821 73.0697,-244.821\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"44.8701\" y=\"-267.67\">!a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 2 -->\n",
         "<g class=\"node\" id=\"node3\"><title>2</title>\n",
-        "<ellipse cx=\"898\" cy=\"-135\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"898\" cy=\"-135\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"898\" y=\"-131.3\">2</text>\n",
+        "<ellipse cx=\"932.09\" cy=\"-135\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"927.59\" y=\"-138.8\">2</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"924.09\" y=\"-123.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
-        "<path d=\"M65.2774,-193.599C77.5204,-139.217 118.038,-0 212,-0 212,-0 212,-0 808,-0 858.477,-0 881.953,-66.6001 891.456,-106.243\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"893.071,-113.31 888.44,-107.188 892.291,-109.898 891.511,-106.486 891.511,-106.486 891.511,-106.486 892.291,-109.898 894.582,-105.784 893.071,-113.31 893.071,-113.31\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"521.5\" y=\"-3.8\">c</text>\n",
+        "<path d=\"M71.4782,-192.583C85.5575,-134.336 128.171,-0 221.74,-0 221.74,-0 221.74,-0 832.35,-0 882.649,-0 910.086,-61.8079 922.572,-101.781\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"924.731,-108.971 919.701,-103.173 923.724,-105.619 922.718,-102.266 922.718,-102.266 922.718,-102.266 923.724,-105.619 925.735,-101.36 924.731,-108.971 924.731,-108.971\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"540.98\" y=\"-3.8\">c</text>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g class=\"node\" id=\"node7\"><title>1</title>\n",
-        "<ellipse cx=\"370\" cy=\"-228\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"370\" cy=\"-228\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"370\" y=\"-224.3\">1</text>\n",
+        "<ellipse cx=\"384.61\" cy=\"-233\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"380.11\" y=\"-236.8\">1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"376.61\" y=\"-221.8\">\u2777</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
-        "<path d=\"M82.1701,-215.894C136.239,-218.176 279.455,-224.221 340.639,-226.803\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"347.682,-227.1 340.555,-229.952 344.185,-226.953 340.688,-226.805 340.688,-226.805 340.688,-226.805 344.185,-226.953 340.821,-223.658 347.682,-227.1 347.682,-227.1\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"180\" y=\"-226.8\">a &amp; !b &amp; !c</text>\n",
+        "<path d=\"M91.8721,-220.146C149.269,-222.675 286.739,-228.732 350.318,-231.533\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"357.695,-231.858 350.563,-234.697 354.198,-231.704 350.701,-231.55 350.701,-231.55 350.701,-231.55 354.198,-231.704 350.84,-228.403 357.695,-231.858 357.695,-231.858\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"189.74\" y=\"-231.8\">a &amp; !b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 3 -->\n",
         "<g class=\"node\" id=\"node9\"><title>3</title>\n",
-        "<ellipse cx=\"213\" cy=\"-295\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"213\" cy=\"-295\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"213\" y=\"-291.3\">3</text>\n",
+        "<ellipse cx=\"222.74\" cy=\"-305\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"218.24\" y=\"-308.8\">3</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"214.74\" y=\"-293.8\">\u2777</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge4\"><title>0-&gt;3</title>\n",
-        "<path d=\"M67.8974,-235.769C73.9503,-250.589 84.2768,-269.659 100,-280 124.807,-296.315 159.427,-298.582 183.587,-297.709\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"190.727,-297.349 183.894,-300.848 187.231,-297.525 183.736,-297.702 183.736,-297.702 183.736,-297.702 187.231,-297.525 183.577,-294.556 190.727,-297.349 190.727,-297.349\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"100\" y=\"-300.8\">a &amp; b &amp; !c</text>\n",
+        "<path d=\"M76.0877,-243.444C83.3639,-257.804 94.553,-275.04 109.74,-285 133.091,-300.313 164.809,-304.813 188.53,-305.772\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"195.617,-305.964 188.534,-308.923 192.118,-305.869 188.62,-305.774 188.62,-305.774 188.62,-305.774 192.118,-305.869 188.705,-302.625 195.617,-305.964 195.617,-305.964\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"109.74\" y=\"-307.8\">a &amp; b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge11\"><title>2-&gt;2</title>\n",
-        "<path d=\"M889.994,-155.581C888.886,-165.845 891.555,-175 898,-175 902.834,-175 905.544,-169.85 906.129,-162.945\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"906.006,-155.581 909.273,-162.527 906.065,-159.08 906.123,-162.58 906.123,-162.58 906.123,-162.58 906.065,-159.08 902.973,-162.632 906.006,-155.581 906.006,-155.581\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"898\" y=\"-178.8\">1</text>\n",
+        "<path d=\"M922.798,-160.37C922.157,-170.924 925.254,-179.87 932.09,-179.87 937.324,-179.87 940.367,-174.626 941.218,-167.431\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"941.383,-160.37 944.368,-167.442 941.301,-163.869 941.219,-167.368 941.219,-167.368 941.219,-167.368 941.301,-163.869 938.07,-167.294 941.383,-160.37 941.383,-160.37\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"932.09\" y=\"-183.67\">1</text>\n",
         "</g>\n",
         "<!-- 4 -->\n",
         "<g class=\"node\" id=\"node4\"><title>4</title>\n",
-        "<ellipse cx=\"807\" cy=\"-246\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"807\" cy=\"-246\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"807\" y=\"-242.3\">4</text>\n",
+        "<ellipse cx=\"831.35\" cy=\"-254\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"826.85\" y=\"-257.8\">4</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"823.35\" y=\"-242.8\">\u2777</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge19\"><title>4-&gt;2</title>\n",
-        "<path d=\"M821.517,-229.141C836.808,-210.071 861.787,-178.918 878.787,-157.715\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"883.356,-152.017 881.434,-159.449 881.166,-154.748 878.977,-157.478 878.977,-157.478 878.977,-157.478 881.166,-154.748 876.519,-155.508 883.356,-152.017 883.356,-152.017\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"847\" y=\"-201.8\">!a</text>\n",
+        "<path d=\"M849.1,-233.813C865.768,-213.726 891.414,-182.817 909.579,-160.925\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"914.258,-155.286 912.213,-162.684 912.023,-157.979 909.788,-160.673 909.788,-160.673 909.788,-160.673 912.023,-157.979 907.364,-158.661 914.258,-155.286 914.258,-155.286\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"876.22\" y=\"-202.8\">!a</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge18\"><title>4-&gt;4</title>\n",
-        "<path d=\"M798.994,-266.581C797.886,-276.845 800.555,-286 807,-286 811.834,-286 814.544,-280.85 815.129,-273.945\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"815.006,-266.581 818.273,-273.527 815.065,-270.08 815.123,-273.58 815.123,-273.58 815.123,-273.58 815.065,-270.08 811.973,-273.632 815.006,-266.581 815.006,-266.581\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"803.5\" y=\"-289.8\">a</text>\n",
+        "<path d=\"M822.058,-279.37C821.417,-289.924 824.514,-298.87 831.35,-298.87 836.584,-298.87 839.626,-293.626 840.477,-286.431\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"840.643,-279.37 843.628,-286.442 840.561,-282.869 840.479,-286.368 840.479,-286.368 840.479,-286.368 840.561,-282.869 837.33,-286.294 840.643,-279.37 840.643,-279.37\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"827.85\" y=\"-302.67\">a</text>\n",
         "</g>\n",
         "<!-- 7 -->\n",
         "<g class=\"node\" id=\"node5\"><title>7</title>\n",
-        "<ellipse cx=\"681\" cy=\"-190\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"681\" cy=\"-190\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"681\" y=\"-186.3\">7</text>\n",
+        "<ellipse cx=\"700.48\" cy=\"-195\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"695.98\" y=\"-198.8\">7</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"692.48\" y=\"-183.8\">\u2777</text>\n",
         "</g>\n",
         "<!-- 7&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge31\"><title>7-&gt;2</title>\n",
-        "<path d=\"M702.615,-184.726C741.543,-174.768 825.873,-153.195 869.546,-142.023\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"876.447,-140.258 870.446,-145.044 873.056,-141.125 869.666,-141.993 869.666,-141.993 869.666,-141.993 873.056,-141.125 868.885,-138.941 876.447,-140.258 876.447,-140.258\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"801.5\" y=\"-169.8\">!a</text>\n",
+        "<path d=\"M726.93,-188.35C769.022,-177.351 853.052,-155.392 899.097,-143.36\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"905.877,-141.589 899.901,-146.406 902.49,-142.474 899.104,-143.358 899.104,-143.358 899.104,-143.358 902.49,-142.474 898.308,-140.311 905.877,-141.589 905.877,-141.589\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"825.85\" y=\"-173.8\">!a</text>\n",
         "</g>\n",
         "<!-- 7&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge30\"><title>7-&gt;4</title>\n",
-        "<path d=\"M701.375,-198.75C722.577,-208.325 756.67,-223.722 780.143,-234.323\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"786.761,-237.311 779.085,-237.301 783.571,-235.871 780.381,-234.43 780.381,-234.43 780.381,-234.43 783.571,-235.871 781.678,-231.559 786.761,-237.311 786.761,-237.311\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"730\" y=\"-231.8\">a &amp; !b</text>\n",
+        "<path d=\"M725.117,-205.822C746.148,-215.45 777.03,-229.588 799.904,-240.061\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"806.427,-243.047 798.751,-242.997 803.245,-241.59 800.062,-240.133 800.062,-240.133 800.062,-240.133 803.245,-241.59 801.374,-237.269 806.427,-243.047 806.427,-243.047\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"749.48\" y=\"-237.8\">a &amp; !b</text>\n",
         "</g>\n",
         "<!-- 7&#45;&gt;7 -->\n",
         "<g class=\"edge\" id=\"edge29\"><title>7-&gt;7</title>\n",
-        "<path d=\"M669.305,-208.93C666.918,-219.842 670.816,-230 681,-230 688.797,-230 692.909,-224.046 693.338,-216.357\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"692.695,-208.93 696.437,-215.633 692.997,-212.417 693.299,-215.904 693.299,-215.904 693.299,-215.904 692.997,-212.417 690.16,-216.176 692.695,-208.93 692.695,-208.93\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"664\" y=\"-233.8\">a &amp; b</text>\n",
+        "<path d=\"M688.35,-219.005C687.027,-230.141 691.07,-239.87 700.48,-239.87 707.832,-239.87 711.908,-233.932 712.709,-226.024\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"712.611,-219.005 715.858,-225.96 712.659,-222.504 712.708,-226.004 712.708,-226.004 712.708,-226.004 712.659,-222.504 709.559,-226.048 712.611,-219.005 712.611,-219.005\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"683.48\" y=\"-243.67\">a &amp; b</text>\n",
         "</g>\n",
         "<!-- 5 -->\n",
         "<g class=\"node\" id=\"node6\"><title>5</title>\n",
-        "<ellipse cx=\"681\" cy=\"-361\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"681\" cy=\"-361\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"681\" y=\"-357.3\">5</text>\n",
+        "<ellipse cx=\"700.48\" cy=\"-376\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"695.98\" y=\"-379.8\">5</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"692.48\" y=\"-364.8\">\u2777</text>\n",
         "</g>\n",
         "<!-- 5&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge21\"><title>5-&gt;2</title>\n",
-        "<path d=\"M703.13,-364.044C720.653,-365.798 746.003,-366.53 767,-360 802.783,-348.871 814.253,-342.779 837,-313 871.519,-267.81 886.851,-201.596 893.118,-163.966\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"894.254,-156.836 896.264,-164.244 893.703,-160.292 893.153,-163.749 893.153,-163.749 893.153,-163.749 893.703,-160.292 890.042,-163.253 894.254,-156.836 894.254,-156.836\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"801.5\" y=\"-359.8\">!a</text>\n",
+        "<path d=\"M727.661,-377.039C744.737,-377.019 767.328,-375.66 786.48,-370 825.298,-358.528 840.237,-357.037 866.22,-326 904.71,-280.023 920.732,-210.108 927.123,-168.842\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"928.173,-161.73 930.267,-169.115 927.662,-165.192 927.151,-168.655 927.151,-168.655 927.151,-168.655 927.662,-165.192 924.034,-168.195 928.173,-161.73 928.173,-161.73\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"825.85\" y=\"-369.8\">!a</text>\n",
         "</g>\n",
         "<!-- 5&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge20\"><title>5-&gt;4</title>\n",
-        "<path d=\"M702.126,-353.535C724.018,-345.114 757.205,-331.373 767,-322 780.875,-308.722 790.693,-289.429 797.007,-273.605\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"799.5,-267.064 799.95,-274.726 798.253,-270.334 797.007,-273.605 797.007,-273.605 797.007,-273.605 798.253,-270.334 794.063,-272.483 799.5,-267.064 799.5,-267.064\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"730\" y=\"-344.8\">a &amp; !b</text>\n",
+        "<path d=\"M725.575,-365.415C747.254,-355.558 777.098,-341.062 786.48,-332 799.974,-318.966 810.498,-300.875 817.853,-285.396\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"820.81,-278.945 820.757,-286.621 819.351,-282.126 817.893,-285.308 817.893,-285.308 817.893,-285.308 819.351,-282.126 815.03,-283.995 820.81,-278.945 820.81,-278.945\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"749.48\" y=\"-356.8\">a &amp; !b</text>\n",
         "</g>\n",
         "<!-- 5&#45;&gt;5 -->\n",
         "<g class=\"edge\" id=\"edge22\"><title>5-&gt;5</title>\n",
-        "<path d=\"M669.305,-379.93C666.918,-390.842 670.816,-401 681,-401 688.797,-401 692.909,-395.046 693.338,-387.357\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"692.695,-379.93 696.437,-386.633 692.997,-383.417 693.299,-386.904 693.299,-386.904 693.299,-386.904 692.997,-383.417 690.16,-387.176 692.695,-379.93 692.695,-379.93\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"664\" y=\"-404.8\">a &amp; b</text>\n",
+        "<path d=\"M688.35,-400.005C687.027,-411.141 691.07,-420.87 700.48,-420.87 707.832,-420.87 711.908,-414.932 712.709,-407.024\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"712.611,-400.005 715.858,-406.96 712.659,-403.504 712.708,-407.004 712.708,-407.004 712.708,-407.004 712.659,-403.504 709.559,-407.048 712.611,-400.005 712.611,-400.005\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"683.48\" y=\"-424.67\">a &amp; b</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge10\"><title>1-&gt;0</title>\n",
-        "<path d=\"M348.318,-222.247C324.044,-215.818 282.469,-205.812 246,-202 190.542,-196.203 125.455,-204.198 89.1456,-209.978\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"81.8483,-211.172 88.2478,-206.933 85.3024,-210.607 88.7565,-210.042 88.7565,-210.042 88.7565,-210.042 85.3024,-210.607 89.2651,-213.151 81.8483,-211.172 81.8483,-211.172\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"193\" y=\"-205.8\">!a &amp; !c</text>\n",
+        "<path d=\"M358.384,-226.048C332.769,-219.375 291.846,-209.77 255.74,-206 200.748,-200.257 136.518,-207.578 98.6266,-213.336\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"91.41,-214.463 97.8403,-210.271 94.8681,-213.923 98.3262,-213.383 98.3262,-213.383 98.3262,-213.383 94.8681,-213.923 98.8121,-216.495 91.41,-214.463 91.41,-214.463\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"202.74\" y=\"-209.8\">!a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge9\"><title>1-&gt;2</title>\n",
-        "<path d=\"M377.421,-207.122C393.562,-159.317 440.617,-46 524,-46 524,-46 524,-46 808,-46 843.857,-46 870.313,-82.5674 884.688,-108.823\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"888.081,-115.248 882.026,-110.529 886.446,-112.153 884.812,-109.058 884.812,-109.058 884.812,-109.058 886.446,-112.153 887.597,-107.587 888.081,-115.248 888.081,-115.248\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"663\" y=\"-49.8\">!a &amp; c</text>\n",
+        "<path d=\"M393.7,-207.391C411.658,-156.176 459.992,-46 543.48,-46 543.48,-46 543.48,-46 832.35,-46 868.672,-46 897.653,-79.6376 914.591,-105.554\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"918.43,-111.616 912.024,-107.388 916.558,-108.659 914.685,-105.702 914.685,-105.702 914.685,-105.702 916.558,-108.659 917.347,-104.017 918.43,-111.616 918.43,-111.616\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"682.48\" y=\"-49.8\">!a &amp; c</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge8\"><title>1-&gt;4</title>\n",
-        "<path d=\"M390.025,-237.295C396.248,-239.928 403.289,-242.487 410,-244 541.058,-273.543 577.881,-264.821 712,-257 734.3,-255.7 759.426,-252.678 778.086,-250.13\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"785.154,-249.146 778.655,-253.231 781.687,-249.629 778.221,-250.112 778.221,-250.112 778.221,-250.112 781.687,-249.629 777.786,-246.992 785.154,-249.146 785.154,-249.146\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"587\" y=\"-268.8\">a &amp; c</text>\n",
+        "<path d=\"M409.904,-242.508C416.194,-244.636 423.018,-246.657 429.48,-248 562.836,-275.71 599.461,-276.255 735.35,-267 756.17,-265.582 779.38,-262.436 797.647,-259.593\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"804.642,-258.482 798.223,-262.691 801.186,-259.031 797.729,-259.58 797.729,-259.58 797.729,-259.58 801.186,-259.031 797.235,-256.469 804.642,-258.482 804.642,-258.482\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"606.48\" y=\"-276.8\">a &amp; c</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge7\"><title>1-&gt;1</title>\n",
-        "<path d=\"M357.453,-246.1C354.427,-257.321 358.609,-268 370,-268 378.899,-268 383.398,-261.482 383.498,-253.28\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"382.547,-246.1 386.589,-252.626 383.007,-249.57 383.467,-253.04 383.467,-253.04 383.467,-253.04 383.007,-249.57 380.344,-253.453 382.547,-246.1 382.547,-246.1\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"337\" y=\"-271.8\">a &amp; !b &amp; !c</text>\n",
+        "<path d=\"M370.781,-256.087C368.868,-267.6 373.477,-277.87 384.61,-277.87 393.308,-277.87 398.024,-271.602 398.758,-263.369\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"398.439,-256.087 401.893,-262.942 398.593,-259.583 398.746,-263.08 398.746,-263.08 398.746,-263.08 398.593,-259.583 395.599,-263.218 398.439,-256.087 398.439,-256.087\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"351.61\" y=\"-281.67\">a &amp; !b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 6 -->\n",
         "<g class=\"node\" id=\"node8\"><title>6</title>\n",
-        "<ellipse cx=\"525\" cy=\"-178\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"525\" cy=\"-178\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"525\" y=\"-174.3\">6</text>\n",
+        "<ellipse cx=\"544.48\" cy=\"-185\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"539.98\" y=\"-188.8\">6</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"536.48\" y=\"-173.8\">\u2777</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;6 -->\n",
         "<g class=\"edge\" id=\"edge6\"><title>1-&gt;6</title>\n",
-        "<path d=\"M392.187,-226.62C413.882,-224.648 448.26,-219.958 476,-209 484.65,-205.583 493.401,-200.511 501.021,-195.455\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"507.127,-191.248 503.15,-197.813 504.245,-193.234 501.363,-195.219 501.363,-195.219 501.363,-195.219 504.245,-193.234 499.575,-192.625 507.127,-191.248 507.127,-191.248\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"412\" y=\"-228.8\">a &amp; b &amp; !c</text>\n",
+        "<path d=\"M411.628,-231.237C434.35,-229.061 467.915,-224.292 495.48,-214 502.321,-211.446 509.273,-207.899 515.685,-204.161\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"521.892,-200.388 517.546,-206.716 518.901,-202.206 515.91,-204.024 515.91,-204.024 515.91,-204.024 518.901,-202.206 514.274,-201.332 521.892,-200.388 521.892,-200.388\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"431.48\" y=\"-232.8\">a &amp; b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 6&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge28\"><title>6-&gt;0</title>\n",
-        "<path d=\"M502.995,-175.869C494.608,-175.117 484.856,-174.368 476,-174 446.692,-172.781 439.311,-172.867 410,-174 271.913,-179.337 234.091,-164.593 100,-198 95.5788,-199.101 91.0238,-200.659 86.6562,-202.389\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"79.9932,-205.209 85.2119,-199.58 83.2165,-203.845 86.4397,-202.481 86.4397,-202.481 86.4397,-202.481 83.2165,-203.845 87.6674,-205.382 79.9932,-205.209 79.9932,-205.209\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"277\" y=\"-179.8\">!a &amp; !c</text>\n",
+        "<path d=\"M517.877,-181.201C510.652,-180.292 502.773,-179.454 495.48,-179 466.204,-177.177 458.795,-177.966 429.48,-179 287.095,-184.022 248.737,-170.718 109.74,-202 105.347,-202.989 100.812,-204.34 96.3996,-205.851\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"89.6047,-208.33 95.1014,-202.972 92.8928,-207.131 96.1809,-205.931 96.1809,-205.931 96.1809,-205.931 92.8928,-207.131 97.2604,-208.89 89.6047,-208.33 89.6047,-208.33\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"286.74\" y=\"-184.8\">!a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 6&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge27\"><title>6-&gt;2</title>\n",
-        "<path d=\"M539.033,-160.336C547.692,-150.091 560.017,-138.05 574,-132 675.428,-88.1145 812.108,-113.574 869.658,-127.62\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"876.599,-129.353 869.044,-130.714 873.203,-128.505 869.807,-127.657 869.807,-127.657 869.807,-127.657 873.203,-128.505 870.571,-124.601 876.599,-129.353 876.599,-129.353\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"730.5\" y=\"-114.8\">!a &amp; c</text>\n",
+        "<path d=\"M559.853,-162.77C568.242,-151.796 579.855,-139.536 593.48,-133 696.016,-83.8113 837.056,-110.332 899.337,-126.056\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"906.18,-127.821 898.615,-129.123 902.791,-126.947 899.402,-126.073 899.402,-126.073 899.402,-126.073 902.791,-126.947 900.189,-123.022 906.18,-127.821 906.18,-127.821\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"749.98\" y=\"-110.8\">!a &amp; c</text>\n",
         "</g>\n",
         "<!-- 6&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge26\"><title>6-&gt;4</title>\n",
-        "<path d=\"M544.51,-167.238C578.913,-148.74 654.438,-115.273 712,-141 748.242,-157.198 776.303,-195.041 791.995,-220.586\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"795.716,-226.795 789.416,-222.409 793.917,-223.792 792.118,-220.79 792.118,-220.79 792.118,-220.79 793.917,-223.792 794.82,-219.171 795.716,-226.795 795.716,-226.795\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"650\" y=\"-144.8\">a &amp; !b &amp; c</text>\n",
+        "<path d=\"M567.508,-170.97C603.918,-149.696 678.297,-114.429 735.35,-141 771.701,-157.93 799.104,-196.373 814.918,-223.71\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"818.497,-230.054 812.314,-225.505 816.777,-227.006 815.057,-223.957 815.057,-223.957 815.057,-223.957 816.777,-227.006 817.801,-222.41 818.497,-230.054 818.497,-230.054\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"669.48\" y=\"-144.8\">a &amp; !b &amp; c</text>\n",
         "</g>\n",
         "<!-- 6&#45;&gt;7 -->\n",
         "<g class=\"edge\" id=\"edge23\"><title>6-&gt;7</title>\n",
-        "<path d=\"M547.09,-179.643C574.125,-181.75 621.11,-185.411 651.362,-187.768\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"658.67,-188.338 651.447,-190.935 655.181,-188.066 651.692,-187.794 651.692,-187.794 651.692,-187.794 655.181,-188.066 651.936,-184.654 658.67,-188.338 658.67,-188.338\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"574\" y=\"-190.8\">a &amp; b &amp; c</text>\n",
+        "<path d=\"M571.604,-186.696C597.679,-188.39 637.841,-190.997 666.188,-192.838\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"673.486,-193.312 666.296,-196.002 669.993,-193.085 666.5,-192.858 666.5,-192.858 666.5,-192.858 669.993,-193.085 666.704,-189.715 673.486,-193.312 673.486,-193.312\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"593.48\" y=\"-195.8\">a &amp; b &amp; c</text>\n",
         "</g>\n",
         "<!-- 6&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge25\"><title>6-&gt;1</title>\n",
-        "<path d=\"M502.727,-176.204C478.963,-175.089 439.908,-175.969 410,-190 402.11,-193.701 394.845,-199.665 388.778,-205.781\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"383.977,-210.908 386.462,-203.646 386.369,-208.353 388.762,-205.799 388.762,-205.799 388.762,-205.799 386.369,-208.353 391.061,-207.952 383.977,-210.908 383.977,-210.908\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"410\" y=\"-193.8\">a &amp; !b &amp; !c</text>\n",
+        "<path d=\"M517.489,-182.833C493.646,-181.857 457.836,-182.989 429.48,-195 422.092,-198.129 415.056,-202.988 408.868,-208.198\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"403.437,-213.042 406.564,-206.031 406.049,-210.712 408.661,-208.382 408.661,-208.382 408.661,-208.382 406.049,-210.712 410.758,-210.733 403.437,-213.042 403.437,-213.042\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"429.48\" y=\"-198.8\">a &amp; !b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 6&#45;&gt;6 -->\n",
         "<g class=\"edge\" id=\"edge24\"><title>6-&gt;6</title>\n",
-        "<path d=\"M511.532,-195.684C508.018,-207.056 512.508,-218 525,-218 534.857,-218 539.732,-211.186 539.623,-202.725\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"538.468,-195.684 542.71,-202.082 539.035,-199.138 539.602,-202.592 539.602,-202.592 539.602,-202.592 539.035,-199.138 536.493,-203.102 538.468,-195.684 538.468,-195.684\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"494\" y=\"-221.8\">a &amp; b &amp; !c</text>\n",
+        "<path d=\"M530.287,-208.087C528.323,-219.6 533.054,-229.87 544.48,-229.87 553.407,-229.87 558.247,-223.602 559.001,-215.369\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"558.673,-208.087 562.135,-214.938 558.831,-211.583 558.988,-215.079 558.988,-215.079 558.988,-215.079 558.831,-211.583 555.841,-215.221 558.673,-208.087 558.673,-208.087\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"513.48\" y=\"-233.67\">a &amp; b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge17\"><title>3-&gt;0</title>\n",
-        "<path d=\"M195.189,-281.694C185.834,-274.783 173.736,-266.63 162,-261 136.015,-248.535 125.933,-254.574 100,-242 94.461,-239.314 88.8316,-235.895 83.6368,-232.4\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"77.7696,-228.301 85.312,-229.727 80.6388,-230.305 83.5079,-232.31 83.5079,-232.31 83.5079,-232.31 80.6388,-230.305 81.7038,-234.892 77.7696,-228.301 77.7696,-228.301\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111\" y=\"-264.8\">!a &amp; !c</text>\n",
+        "<path d=\"M202.459,-287.266C193.615,-279.869 182.677,-271.693 171.74,-266 146.175,-252.694 135.904,-259.086 109.74,-247 104.198,-244.44 98.5259,-241.281 93.178,-238.018\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"87.0763,-234.168 94.6773,-235.239 90.0364,-236.036 92.9966,-237.903 92.9966,-237.903 92.9966,-237.903 90.0364,-236.036 91.3158,-240.567 87.0763,-234.168 87.0763,-234.168\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"120.74\" y=\"-269.8\">!a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge14\"><title>3-&gt;2</title>\n",
-        "<path d=\"M223.034,-314.786C243.053,-355.317 295.28,-444 369,-444 369,-444 369,-444 808,-444 865.868,-444 888.377,-241.358 894.846,-164.279\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"895.423,-157.223 897.992,-164.456 895.138,-160.711 894.853,-164.199 894.853,-164.199 894.853,-164.199 895.138,-160.711 891.713,-163.943 895.423,-157.223 895.423,-157.223\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"585\" y=\"-447.8\">!a &amp; c</text>\n",
+        "<path d=\"M234.46,-329.495C255.831,-374.096 308.256,-464 383.61,-464 383.61,-464 383.61,-464 832.35,-464 893.483,-464 920.029,-252.978 928.176,-168.94\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"928.842,-161.923 931.317,-169.19 928.511,-165.408 928.181,-168.892 928.181,-168.892 928.181,-168.892 928.511,-165.408 925.045,-168.594 928.842,-161.923 928.842,-161.923\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"604.48\" y=\"-467.8\">!a &amp; c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge13\"><title>3-&gt;4</title>\n",
-        "<path d=\"M234.989,-298.551C264.72,-303.265 320.846,-311 369,-311 369,-311 369,-311 682,-311 721.661,-311 761.14,-284.593 784.556,-265.442\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"790.153,-260.75 786.812,-267.66 787.471,-262.998 784.789,-265.246 784.789,-265.246 784.789,-265.246 787.471,-262.998 782.765,-262.832 790.153,-260.75 790.153,-260.75\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"494\" y=\"-314.8\">a &amp; !b &amp; c</text>\n",
+        "<path d=\"M249.412,-309.162C280.928,-313.903 336.051,-321 383.61,-321 383.61,-321 383.61,-321 701.48,-321 741.166,-321 780.763,-295.677 805.38,-276.168\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"811.005,-271.603 807.554,-278.46 808.287,-273.809 805.569,-276.014 805.569,-276.014 805.569,-276.014 808.287,-273.809 803.584,-273.568 811.005,-271.603 811.005,-271.603\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"513.48\" y=\"-324.8\">a &amp; !b &amp; c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;5 -->\n",
         "<g class=\"edge\" id=\"edge15\"><title>3-&gt;5</title>\n",
-        "<path d=\"M231.099,-307.925C240.345,-314.201 252.251,-321.193 264,-325 404.061,-370.387 583.722,-366.417 651.993,-362.838\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"659.005,-362.451 652.189,-365.982 655.51,-362.644 652.015,-362.837 652.015,-362.837 652.015,-362.837 655.51,-362.644 651.842,-359.691 659.005,-362.451 659.005,-362.451\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"414\" y=\"-364.8\">a &amp; b &amp; c</text>\n",
+        "<path d=\"M245.113,-320.686C253.614,-326.137 263.741,-331.706 273.74,-335 413.861,-381.157 592.916,-380.365 666.077,-377.696\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"673.235,-377.417 666.363,-380.838 669.737,-377.553 666.24,-377.69 666.24,-377.69 666.24,-377.69 669.737,-377.553 666.117,-374.542 673.235,-377.417 673.235,-377.417\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"433.48\" y=\"-377.8\">a &amp; b &amp; c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge12\"><title>3-&gt;1</title>\n",
-        "<path d=\"M233.714,-286.531C256.803,-276.607 296.197,-259.653 330,-245 334.18,-243.188 338.611,-241.262 342.928,-239.382\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"349.566,-236.49 344.407,-242.174 346.358,-237.888 343.149,-239.286 343.149,-239.286 343.149,-239.286 346.358,-237.888 341.891,-236.398 349.566,-236.49 349.566,-236.49\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"264\" y=\"-276.8\">a &amp; !b &amp; !c</text>\n",
+        "<path d=\"M247.674,-294.221C275.775,-281.565 322.431,-260.553 353.104,-246.739\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"359.774,-243.735 354.685,-249.482 356.583,-245.172 353.391,-246.61 353.391,-246.61 353.391,-246.61 356.583,-245.172 352.098,-243.737 359.774,-243.735 359.774,-243.735\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"273.74\" y=\"-285.8\">a &amp; !b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge16\"><title>3-&gt;3</title>\n",
-        "<path d=\"M198.98,-312.268C195.034,-323.787 199.707,-335 213,-335 223.593,-335 228.712,-327.88 228.358,-319.158\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"227.02,-312.268 231.447,-318.539 227.687,-315.704 228.354,-319.14 228.354,-319.14 228.354,-319.14 227.687,-315.704 225.262,-319.74 227.02,-312.268 227.02,-312.268\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"182\" y=\"-338.8\">a &amp; b &amp; !c</text>\n",
+        "<path d=\"M207.906,-327.625C205.623,-339.324 210.568,-349.87 222.74,-349.87 232.344,-349.87 237.449,-343.304 238.054,-334.787\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"237.575,-327.625 241.185,-334.399 237.808,-331.118 238.042,-334.61 238.042,-334.61 238.042,-334.61 237.808,-331.118 234.899,-334.82 237.575,-327.625 237.575,-327.625\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"191.74\" y=\"-353.67\">a &amp; b &amp; !c</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd4fc077d30>"
+        "<IPython.core.display.SVG at 0x7fe3f409fb38>"
        ]
       },
       {
        "metadata": {},
        "output_type": "display_data",
        "svg": [
-        "<svg height=\"360pt\" viewBox=\"0.00 0.00 538.09 360.00\" width=\"538pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.957447 0.957447) rotate(0) translate(4 372)\">\n",
+        "<svg height=\"360pt\" viewBox=\"0.00 0.00 537.47 360.00\" width=\"537pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.909091 0.909091) rotate(0) translate(4 392)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-372 558,-372 558,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"237\" y=\"-353.8\">strictly weak</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"256\" y=\"-339.8\">Inf(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"278\" y=\"-339.8\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"294\" y=\"-339.8\">)</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-392 587.22,-392 587.22,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"251.61\" y=\"-373.8\">strictly weak</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"270.61\" y=\"-359.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"292.61\" y=\"-359.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"308.61\" y=\"-359.8\">)</text>\n",
         "<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
-        "<polygon fill=\"none\" points=\"340,-8 340,-101 400,-101 400,-8 340,-8\" stroke=\"green\"/>\n",
+        "<polygon fill=\"none\" points=\"349.74,-8 349.74,-111 419.48,-111 419.48,-8 349.74,-8\" stroke=\"green\"/>\n",
         "</g>\n",
         "<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
-        "<polygon fill=\"none\" points=\"30,-109 30,-324 546,-324 546,-109 30,-109\" stroke=\"red\"/>\n",
+        "<polygon fill=\"none\" points=\"30,-119 30,-344 575.22,-344 575.22,-119 30,-119\" stroke=\"red\"/>\n",
         "</g>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node2\"><title>0</title>\n",
-        "<ellipse cx=\"60\" cy=\"-230\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"60\" cy=\"-230\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"60\" y=\"-226.3\">0</text>\n",
+        "<ellipse cx=\"64.8701\" cy=\"-250\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"60.3701\" y=\"-253.8\">0</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"56.8701\" y=\"-238.8\">\u2777</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
-        "<path d=\"M1.16638,-230C2.84121,-230 16.884,-230 30.7112,-230\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"37.8555,-230 30.8556,-233.15 34.3555,-230 30.8555,-230 30.8555,-230 30.8555,-230 34.3555,-230 30.8555,-226.85 37.8555,-230 37.8555,-230\" stroke=\"black\"/>\n",
+        "<path d=\"M1.04557,-250C1.94668,-250 16.0699,-250 30.6965,-250\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.8616,-250 30.8617,-253.15 34.3616,-250 30.8616,-250 30.8616,-250 30.8616,-250 34.3616,-250 30.8616,-246.85 37.8616,-250 37.8616,-250\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge4\"><title>0-&gt;0</title>\n",
-        "<path d=\"M52.6831,-250.991C51.7798,-261.087 54.2188,-270 60,-270 64.3359,-270 66.7918,-264.987 67.3677,-258.22\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"67.3169,-250.991 70.5161,-257.968 67.3415,-254.491 67.3662,-257.991 67.3662,-257.991 67.3662,-257.991 67.3415,-254.491 64.2163,-258.013 67.3169,-250.991 67.3169,-250.991\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"40\" y=\"-273.8\">!a &amp; !c</text>\n",
+        "<path d=\"M56.6704,-275.821C56.2072,-286.178 58.9404,-294.87 64.8701,-294.87 69.3173,-294.87 71.9666,-289.981 72.8178,-283.167\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.0697,-275.821 75.9779,-282.925 72.9497,-279.319 72.8297,-282.817 72.8297,-282.817 72.8297,-282.817 72.9497,-279.319 69.6816,-282.709 73.0697,-275.821 73.0697,-275.821\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"44.8701\" y=\"-298.67\">!a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g class=\"node\" id=\"node4\"><title>1</title>\n",
-        "<ellipse cx=\"370\" cy=\"-227\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"370\" cy=\"-227\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"370\" y=\"-223.3\">1</text>\n",
+        "<ellipse cx=\"384.61\" cy=\"-242\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"380.11\" y=\"-245.8\">1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"376.61\" y=\"-230.8\">\u2777</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
-        "<path d=\"M81.9453,-234.375C105.621,-239.08 145.379,-246.254 180,-249 246.747,-254.295 264.171,-247.233 330,-235 333.644,-234.323 337.473,-233.578 341.249,-232.824\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"348.383,-231.378 342.148,-235.856 344.953,-232.074 341.523,-232.769 341.523,-232.769 341.523,-232.769 344.953,-232.074 340.897,-229.682 348.383,-231.378 348.383,-231.378\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"180\" y=\"-253.8\">a &amp; !b &amp; !c</text>\n",
+        "<path d=\"M91.3607,-255.072C116.313,-259.762 155.464,-266.387 189.74,-269 256.503,-274.09 274.496,-270.044 339.74,-255 343.707,-254.085 347.844,-253.016 351.924,-251.89\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"358.696,-249.96 352.827,-254.908 355.33,-250.92 351.964,-251.879 351.964,-251.879 351.964,-251.879 355.33,-250.92 351.1,-248.849 358.696,-249.96 358.696,-249.96\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"189.74\" y=\"-274.8\">a &amp; !b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 2 -->\n",
         "<g class=\"node\" id=\"node6\"><title>2</title>\n",
-        "<ellipse cx=\"213\" cy=\"-139\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"213\" cy=\"-139\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"213\" y=\"-135.3\">2</text>\n",
+        "<ellipse cx=\"222.74\" cy=\"-154\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"218.24\" y=\"-157.8\">2</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"214.74\" y=\"-142.8\">\u2777</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
-        "<path d=\"M79.2141,-219.023C106.31,-202.694 157.285,-171.974 187.585,-153.713\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"193.721,-150.016 189.352,-156.327 190.724,-151.822 187.726,-153.629 187.726,-153.629 187.726,-153.629 190.724,-151.822 186.1,-150.931 193.721,-150.016 193.721,-150.016\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"100\" y=\"-209.8\">a &amp; b &amp; !c</text>\n",
+        "<path d=\"M88.2024,-236.246C115.866,-219.208 163.031,-190.159 193.267,-171.536\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"199.449,-167.729 195.141,-174.082 196.469,-169.564 193.489,-171.4 193.489,-171.4 193.489,-171.4 196.469,-169.564 191.837,-168.718 199.449,-167.729 199.449,-167.729\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"109.74\" y=\"-224.8\">a &amp; b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 3 -->\n",
         "<g class=\"node\" id=\"node3\"><title>3</title>\n",
-        "<ellipse cx=\"370\" cy=\"-38\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"370\" cy=\"-38\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"370\" y=\"-34.3\">3</text>\n",
+        "<ellipse cx=\"384.61\" cy=\"-43\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"380.11\" y=\"-46.8\">3</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"376.61\" y=\"-31.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
-        "<path d=\"M357.453,-56.1003C354.427,-67.3213 358.609,-78 370,-78 378.899,-78 383.398,-71.4822 383.498,-63.2801\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"382.547,-56.1003 386.589,-62.6261 383.007,-59.57 383.467,-63.0397 383.467,-63.0397 383.467,-63.0397 383.007,-59.57 380.344,-63.4533 382.547,-56.1003 382.547,-56.1003\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"353\" y=\"-81.8\">a &amp; b</text>\n",
+        "<path d=\"M370.781,-66.0865C368.868,-77.6001 373.477,-87.8701 384.61,-87.8701 393.308,-87.8701 398.024,-81.6018 398.758,-73.3693\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"398.439,-66.0865 401.893,-72.9418 398.593,-69.5832 398.746,-73.0798 398.746,-73.0798 398.746,-73.0798 398.593,-69.5832 395.599,-73.2178 398.439,-66.0865 398.439,-66.0865\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"367.61\" y=\"-91.6701\">a &amp; b</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge7\"><title>1-&gt;0</title>\n",
-        "<path d=\"M347.682,-227.208C293.45,-227.736 150.228,-229.131 89.1943,-229.725\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"82.1701,-229.794 89.139,-226.576 85.6699,-229.76 89.1698,-229.726 89.1698,-229.726 89.1698,-229.726 85.6699,-229.76 89.2005,-232.875 82.1701,-229.794 82.1701,-229.794\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"193\" y=\"-231.8\">!a &amp; !c</text>\n",
+        "<path d=\"M357.695,-242.652C300.261,-244.099 162.352,-247.571 98.8711,-249.169\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"91.8721,-249.345 98.7905,-246.02 95.371,-249.257 98.8698,-249.169 98.8698,-249.169 98.8698,-249.169 95.371,-249.257 98.9492,-252.318 91.8721,-249.345 91.8721,-249.345\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"202.74\" y=\"-249.8\">!a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge6\"><title>1-&gt;1</title>\n",
-        "<path d=\"M357.453,-245.1C354.427,-256.321 358.609,-267 370,-267 378.899,-267 383.398,-260.482 383.498,-252.28\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"382.547,-245.1 386.589,-251.626 383.007,-248.57 383.467,-252.04 383.467,-252.04 383.467,-252.04 383.007,-248.57 380.344,-252.453 382.547,-245.1 382.547,-245.1\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"337\" y=\"-270.8\">a &amp; !b &amp; !c</text>\n",
+        "<path d=\"M370.781,-265.087C368.868,-276.6 373.477,-286.87 384.61,-286.87 393.308,-286.87 398.024,-280.602 398.758,-272.369\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"398.439,-265.087 401.893,-271.942 398.593,-268.583 398.746,-272.08 398.746,-272.08 398.746,-272.08 398.593,-268.583 395.599,-272.218 398.439,-265.087 398.439,-265.087\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"351.61\" y=\"-290.67\">a &amp; !b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 4 -->\n",
         "<g class=\"node\" id=\"node5\"><title>4</title>\n",
-        "<ellipse cx=\"516\" cy=\"-261\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"516\" cy=\"-261\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"516\" y=\"-257.3\">4</text>\n",
+        "<ellipse cx=\"540.35\" cy=\"-276\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"535.85\" y=\"-279.8\">4</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"532.35\" y=\"-264.8\">\u2777</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge5\"><title>1-&gt;4</title>\n",
-        "<path d=\"M390.649,-234.73C396.783,-236.959 403.615,-239.257 410,-241 435.622,-247.993 465.415,-253.418 486.706,-256.843\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"493.861,-257.97 486.456,-259.992 490.404,-257.425 486.947,-256.881 486.947,-256.881 486.947,-256.881 490.404,-257.425 487.437,-253.769 493.861,-257.97 493.861,-257.97\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"412\" y=\"-257.8\">a &amp; b &amp; !c</text>\n",
+        "<path d=\"M410.506,-250.558C416.663,-252.504 423.275,-254.452 429.48,-256 455.001,-262.367 484.328,-267.602 506.26,-271.117\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"513.398,-272.243 505.993,-274.264 509.941,-271.698 506.484,-271.153 506.484,-271.153 506.484,-271.153 509.941,-271.698 506.974,-268.041 513.398,-272.243 513.398,-272.243\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"431.48\" y=\"-272.8\">a &amp; b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge15\"><title>4-&gt;0</title>\n",
-        "<path d=\"M494.968,-268.043C472.275,-275.592 434.02,-287.026 400,-291 302.398,-302.4 276.257,-288.763 180,-269 143.878,-261.583 134.768,-259.288 100,-247 95.7041,-245.482 91.214,-243.708 86.8727,-241.89\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"80.2225,-239.028 87.8976,-238.902 83.4374,-240.412 86.6522,-241.795 86.6522,-241.795 86.6522,-241.795 83.4374,-240.412 85.4067,-244.689 80.2225,-239.028 80.2225,-239.028\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"277\" y=\"-298.8\">!a &amp; !c</text>\n",
+        "<path d=\"M515.008,-285.328C491.103,-293.955 453.389,-306.151 419.48,-311 317.98,-325.515 290.121,-310.895 189.74,-290 153.521,-282.461 144.801,-278.807 109.74,-267 105.574,-265.597 101.222,-264.033 96.9444,-262.437\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"90.323,-259.922 97.9854,-259.463 93.5949,-261.165 96.8669,-262.408 96.8669,-262.408 96.8669,-262.408 93.5949,-261.165 95.7484,-265.353 90.323,-259.922 90.323,-259.922\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"286.74\" y=\"-319.8\">!a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge14\"><title>4-&gt;1</title>\n",
-        "<path d=\"M502.662,-243.397C495.849,-235.241 486.616,-226.397 476,-222 451.157,-211.71 420.128,-214.921 398.263,-219.501\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"391.222,-221.089 397.357,-216.476 394.636,-220.319 398.05,-219.549 398.05,-219.549 398.05,-219.549 394.636,-220.319 398.744,-222.622 391.222,-221.089 391.222,-221.089\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"410\" y=\"-225.8\">a &amp; !b &amp; !c</text>\n",
+        "<path d=\"M522.215,-255.476C514.834,-248.186 505.577,-240.839 495.48,-237 470.679,-227.57 440.429,-229.851 417.954,-233.907\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"410.947,-235.274 417.215,-230.842 414.382,-234.604 417.818,-233.934 417.818,-233.934 417.818,-233.934 414.382,-234.604 418.421,-237.025 410.947,-235.274 410.947,-235.274\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"429.48\" y=\"-240.8\">a &amp; !b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge13\"><title>4-&gt;4</title>\n",
-        "<path d=\"M503.453,-279.1C500.427,-290.321 504.609,-301 516,-301 524.899,-301 529.398,-294.482 529.498,-286.28\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"528.547,-279.1 532.589,-285.626 529.007,-282.57 529.467,-286.04 529.467,-286.04 529.467,-286.04 529.007,-282.57 526.344,-286.453 528.547,-279.1 528.547,-279.1\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"485\" y=\"-304.8\">a &amp; b &amp; !c</text>\n",
+        "<path d=\"M526.521,-299.087C524.608,-310.6 529.217,-320.87 540.35,-320.87 549.048,-320.87 553.764,-314.602 554.499,-306.369\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"554.179,-299.087 557.633,-305.942 554.333,-302.583 554.486,-306.08 554.486,-306.08 554.486,-306.08 554.333,-302.583 551.339,-306.218 554.179,-299.087 554.179,-299.087\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"509.35\" y=\"-324.67\">a &amp; b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge11\"><title>2-&gt;0</title>\n",
-        "<path d=\"M190.94,-136.11C166.744,-133.946 126.924,-134.055 100,-153 83.7006,-164.469 73.8107,-184.804 68.0698,-201.697\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"65.8569,-208.691 64.9656,-201.067 66.9128,-205.354 67.9688,-202.017 67.9688,-202.017 67.9688,-202.017 66.9128,-205.354 70.972,-202.967 65.8569,-208.691 65.8569,-208.691\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111\" y=\"-156.8\">!a &amp; !c</text>\n",
+        "<path d=\"M195.825,-150.543C171.482,-148.688 135.104,-149.645 109.74,-167 92.6401,-178.7 81.7051,-199.248 75.029,-216.97\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"72.5911,-223.851 71.9597,-216.201 73.76,-220.552 74.9289,-217.253 74.9289,-217.253 74.9289,-217.253 73.76,-220.552 77.898,-218.305 72.5911,-223.851 72.5911,-223.851\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"120.74\" y=\"-170.8\">!a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge9\"><title>2-&gt;3</title>\n",
-        "<path d=\"M231.78,-127.414C259.662,-109.246 313.708,-74.029 345.007,-53.6339\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"350.949,-49.762 346.804,-56.2227 348.017,-51.6728 345.085,-53.5836 345.085,-53.5836 345.085,-53.5836 348.017,-51.6728 343.365,-50.9444 350.949,-49.762 350.949,-49.762\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"268\" y=\"-110.8\">a &amp; b &amp; c</text>\n",
+        "<path d=\"M245.301,-139.03C273.986,-119.114 324.723,-83.8859 356.126,-62.0828\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"362.136,-57.9096 358.183,-64.4894 359.261,-59.9058 356.386,-61.9019 356.386,-61.9019 356.386,-61.9019 359.261,-59.9058 354.59,-59.3144 362.136,-57.9096 362.136,-57.9096\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"277.74\" y=\"-122.8\">a &amp; b &amp; c</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge8\"><title>2-&gt;1</title>\n",
-        "<path d=\"M232.389,-149.44C260.09,-165.167 312.595,-194.976 343.826,-212.708\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"350.151,-216.299 342.509,-215.582 347.108,-214.571 344.064,-212.843 344.064,-212.843 344.064,-212.843 347.108,-214.571 345.619,-210.103 350.151,-216.299 350.151,-216.299\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"264\" y=\"-207.8\">a &amp; !b &amp; !c</text>\n",
+        "<path d=\"M246.646,-166.608C275.019,-182.226 323.394,-208.854 354.406,-225.925\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"360.747,-229.415 353.096,-228.799 357.681,-227.727 354.615,-226.04 354.615,-226.04 354.615,-226.04 357.681,-227.727 356.134,-223.28 360.747,-229.415 360.747,-229.415\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"273.74\" y=\"-219.8\">a &amp; !b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge10\"><title>2-&gt;2</title>\n",
-        "<path d=\"M198.98,-156.268C195.034,-167.787 199.707,-179 213,-179 223.593,-179 228.712,-171.88 228.358,-163.158\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"227.02,-156.268 231.447,-162.539 227.687,-159.704 228.354,-163.14 228.354,-163.14 228.354,-163.14 227.687,-159.704 225.262,-163.74 227.02,-156.268 227.02,-156.268\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"182\" y=\"-182.8\">a &amp; b &amp; !c</text>\n",
+        "<path d=\"M207.906,-176.625C205.623,-188.324 210.568,-198.87 222.74,-198.87 232.344,-198.87 237.449,-192.304 238.054,-183.787\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"237.575,-176.625 241.185,-183.399 237.808,-180.118 238.042,-183.61 238.042,-183.61 238.042,-183.61 237.808,-180.118 234.899,-183.82 237.575,-176.625 237.575,-176.625\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"191.74\" y=\"-202.67\">a &amp; b &amp; !c</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd4fd89fcf8>"
+        "<IPython.core.display.SVG at 0x7fe3fc383ef0>"
        ]
       },
       {
@@ -3703,7 +3703,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd4fc077d30>"
+        "<IPython.core.display.SVG at 0x7fe3f409fb38>"
        ]
       }
      ],
@@ -3999,7 +3999,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd505029b70>"
+        "<IPython.core.display.SVG at 0x7fe3fc3999e8>"
        ]
       }
      ],
@@ -4105,7 +4105,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd4fc0d9748>"
+        "<IPython.core.display.SVG at 0x7fe3f4077550>"
        ]
       }
      ],
@@ -4128,7 +4128,7 @@
      "collapsed": false,
      "input": [
       "for opt in ('w', 't'):\n",
-      "    display(spot.decompose_strength(aut, opt).show('.as'))"
+      "    display(spot.decompose_strength(aut, opt).show('.bas'))"
      ],
      "language": "python",
      "metadata": {},
@@ -4137,119 +4137,119 @@
        "metadata": {},
        "output_type": "display_data",
        "svg": [
-        "<svg height=\"140pt\" viewBox=\"0.00 0.00 248.00 140.00\" width=\"248pt\" 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 136)\">\n",
+        "<svg height=\"150pt\" viewBox=\"0.00 0.00 267.48 150.00\" width=\"267pt\" 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 146)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-136 244,-136 244,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"99\" y=\"-117.8\">Inf(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"121\" y=\"-117.8\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"137\" y=\"-117.8\">)</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-146 263.48,-146 263.48,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"108.74\" y=\"-127.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"130.74\" y=\"-127.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"146.74\" y=\"-127.8\">)</text>\n",
         "<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
-        "<polygon fill=\"none\" points=\"172,-8 172,-101 232,-101 232,-8 172,-8\" stroke=\"green\"/>\n",
+        "<polygon fill=\"none\" points=\"181.74,-8 181.74,-111 251.48,-111 251.48,-8 181.74,-8\" stroke=\"green\"/>\n",
         "</g>\n",
         "<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
-        "<polygon fill=\"none\" points=\"30,-8 30,-101 90,-101 90,-8 30,-8\" stroke=\"green\"/>\n",
+        "<polygon fill=\"none\" points=\"30,-8 30,-111 99.7401,-111 99.7401,-8 30,-8\" stroke=\"green\"/>\n",
         "</g>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node2\"><title>0</title>\n",
-        "<ellipse cx=\"60\" cy=\"-38\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"60\" cy=\"-38\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"60\" y=\"-34.3\">0</text>\n",
+        "<ellipse cx=\"64.8701\" cy=\"-43\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"60.3701\" y=\"-46.8\">0</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"56.8701\" y=\"-31.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
-        "<path d=\"M1.16638,-38C2.84121,-38 16.884,-38 30.7112,-38\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"37.8555,-38 30.8556,-41.1501 34.3555,-38 30.8555,-38.0001 30.8555,-38.0001 30.8555,-38.0001 34.3555,-38 30.8555,-34.8501 37.8555,-38 37.8555,-38\" stroke=\"black\"/>\n",
+        "<path d=\"M1.04557,-43C1.94668,-43 16.0699,-43 30.6965,-43\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.8616,-43 30.8617,-46.1501 34.3616,-43 30.8616,-43.0001 30.8616,-43.0001 30.8616,-43.0001 34.3616,-43 30.8616,-39.8501 37.8616,-43 37.8616,-43\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
-        "<path d=\"M52.6831,-58.9908C51.7798,-69.0872 54.2188,-78 60,-78 64.3359,-78 66.7918,-72.9866 67.3677,-66.2204\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"67.3169,-58.9908 70.5161,-65.9684 67.3415,-62.4907 67.3662,-65.9906 67.3662,-65.9906 67.3662,-65.9906 67.3415,-62.4907 64.2163,-66.0128 67.3169,-58.9908 67.3169,-58.9908\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"42\" y=\"-81.8\">a &amp; !c</text>\n",
+        "<path d=\"M56.6704,-68.8213C56.2072,-79.1776 58.9404,-87.8701 64.8701,-87.8701 69.3173,-87.8701 71.9666,-82.9805 72.8178,-76.1667\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.0697,-68.8213 75.9779,-75.9252 72.9497,-72.3193 72.8297,-75.8172 72.8297,-75.8172 72.8297,-75.8172 72.9497,-72.3193 69.6816,-75.7092 73.0697,-68.8213 73.0697,-68.8213\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"46.8701\" y=\"-91.6701\">a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g class=\"node\" id=\"node3\"><title>1</title>\n",
-        "<ellipse cx=\"202\" cy=\"-38\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"202\" cy=\"-38\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"202\" y=\"-34.3\">1</text>\n",
+        "<ellipse cx=\"216.61\" cy=\"-43\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"212.11\" y=\"-46.8\">1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"208.61\" y=\"-31.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
-        "<path d=\"M82.263,-38C106.455,-38 146.065,-38 172.815,-38\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"179.996,-38 172.996,-41.1501 176.496,-38 172.996,-38.0001 172.996,-38.0001 172.996,-38.0001 176.496,-38 172.996,-34.8501 179.996,-38 179.996,-38\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"100\" y=\"-41.8\">a &amp; b &amp; !c</text>\n",
+        "<path d=\"M91.9528,-43C117.105,-43 155.269,-43 182.542,-43\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"189.576,-43 182.576,-46.1501 186.076,-43 182.576,-43.0001 182.576,-43.0001 182.576,-43.0001 186.076,-43 182.576,-39.8501 189.576,-43 189.576,-43\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"109.74\" y=\"-46.8\">a &amp; b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge4\"><title>1-&gt;1</title>\n",
-        "<path d=\"M189.695,-56.5156C186.961,-67.5833 191.062,-78 202,-78 210.545,-78 214.918,-71.6422 215.118,-63.5831\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"214.305,-56.5156 218.234,-63.1097 214.705,-59.9927 215.105,-63.4698 215.105,-63.4698 215.105,-63.4698 214.705,-59.9927 211.975,-63.8298 214.305,-56.5156 214.305,-56.5156\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"197.5\" y=\"-81.8\">b</text>\n",
+        "<path d=\"M203.074,-66.5464C201.403,-77.8722 205.915,-87.8701 216.61,-87.8701 224.966,-87.8701 229.548,-81.7678 230.355,-73.6976\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"230.146,-66.5464 233.5,-73.4513 230.249,-70.0449 230.351,-73.5434 230.351,-73.5434 230.351,-73.5434 230.249,-70.0449 227.202,-73.6355 230.146,-66.5464 230.146,-66.5464\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"212.11\" y=\"-91.6701\">b</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd4fc0bcd68>"
+        "<IPython.core.display.SVG at 0x7fe3f4079b38>"
        ]
       },
       {
        "metadata": {},
        "output_type": "display_data",
        "svg": [
-        "<svg height=\"140pt\" viewBox=\"0.00 0.00 210.00 140.00\" width=\"210pt\" 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 136)\">\n",
+        "<svg height=\"150pt\" viewBox=\"0.00 0.00 219.74 150.00\" width=\"220pt\" 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 146)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-136 206,-136 206,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"80\" y=\"-117.8\">Inf(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"102\" y=\"-117.8\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"118\" y=\"-117.8\">)</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-146 215.74,-146 215.74,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"84.8701\" y=\"-127.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"106.87\" y=\"-127.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"122.87\" y=\"-127.8\">)</text>\n",
         "<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
-        "<polygon fill=\"none\" points=\"134,-8 134,-101 194,-101 194,-8 134,-8\" stroke=\"green\"/>\n",
+        "<polygon fill=\"none\" points=\"134,-8 134,-111 203.74,-111 203.74,-8 134,-8\" stroke=\"green\"/>\n",
         "</g>\n",
         "<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
-        "<polygon fill=\"none\" points=\"30,-12 30,-97 82,-97 82,-12 30,-12\" stroke=\"red\"/>\n",
+        "<polygon fill=\"none\" points=\"30,-17 30,-102 82,-102 82,-17 30,-17\" stroke=\"red\"/>\n",
         "</g>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node2\"><title>0</title>\n",
-        "<ellipse cx=\"56\" cy=\"-38\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-34.3\">0</text>\n",
+        "<ellipse cx=\"56\" cy=\"-43\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-39.3\">0</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
-        "<path d=\"M1.15491,-38C2.79388,-38 17.1543,-38 30.6317,-38\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"37.9419,-38 30.9419,-41.1501 34.4419,-38 30.9419,-38.0001 30.9419,-38.0001 30.9419,-38.0001 34.4419,-38 30.9418,-34.8501 37.9419,-38 37.9419,-38\" stroke=\"black\"/>\n",
+        "<path d=\"M1.15491,-43C2.79388,-43 17.1543,-43 30.6317,-43\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-43 30.9419,-46.1501 34.4419,-43 30.9419,-43.0001 30.9419,-43.0001 30.9419,-43.0001 34.4419,-43 30.9418,-39.8501 37.9419,-43 37.9419,-43\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
-        "<path d=\"M49.6208,-55.0373C48.3189,-64.8579 50.4453,-74 56,-74 60.166,-74 62.4036,-68.8576 62.7128,-62.1433\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"62.3792,-55.0373 65.8541,-61.8818 62.5434,-58.5335 62.7076,-62.0296 62.7076,-62.0296 62.7076,-62.0296 62.5434,-58.5335 59.561,-62.1774 62.3792,-55.0373 62.3792,-55.0373\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"38\" y=\"-77.8\">a &amp; !c</text>\n",
+        "<path d=\"M49.6208,-60.0373C48.3189,-69.8579 50.4453,-79 56,-79 60.166,-79 62.4036,-73.8576 62.7128,-67.1433\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"62.3792,-60.0373 65.8541,-66.8818 62.5434,-63.5335 62.7076,-67.0296 62.7076,-67.0296 62.7076,-67.0296 62.5434,-63.5335 59.561,-67.1774 62.3792,-60.0373 62.3792,-60.0373\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"38\" y=\"-82.8\">a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g class=\"node\" id=\"node3\"><title>1</title>\n",
-        "<ellipse cx=\"164\" cy=\"-38\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"164\" cy=\"-38\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"164\" y=\"-34.3\">1</text>\n",
+        "<ellipse cx=\"168.87\" cy=\"-43\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"164.37\" y=\"-46.8\">1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"160.87\" y=\"-31.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
-        "<path d=\"M74.0307,-38C90.429,-38 115.526,-38 134.888,-38\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"141.998,-38 134.998,-41.1501 138.498,-38 134.998,-38.0001 134.998,-38.0001 134.998,-38.0001 138.498,-38 134.998,-34.8501 141.998,-38 141.998,-38\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-41.8\">a &amp; c</text>\n",
+        "<path d=\"M74.3234,-43C90.3789,-43 114.701,-43 134.521,-43\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"141.595,-43 134.595,-46.1501 138.095,-43 134.595,-43.0001 134.595,-43.0001 134.595,-43.0001 138.095,-43 134.595,-39.8501 141.595,-43 141.595,-43\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-46.8\">a &amp; c</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge4\"><title>1-&gt;1</title>\n",
-        "<path d=\"M153.933,-57.7575C152.223,-68.3499 155.578,-78 164,-78 170.448,-78 173.926,-72.3433 174.435,-64.9379\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"174.067,-57.7575 177.571,-64.5871 174.246,-61.2529 174.425,-64.7483 174.425,-64.7483 174.425,-64.7483 174.246,-61.2529 171.279,-64.9095 174.067,-57.7575 174.067,-57.7575\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"164\" y=\"-81.8\">1</text>\n",
+        "<path d=\"M157.755,-67.9167C156.845,-78.6664 160.55,-87.8701 168.87,-87.8701 175.24,-87.8701 178.905,-82.475 179.865,-75.1217\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"179.985,-67.9167 183.018,-74.9686 179.927,-71.4162 179.868,-74.9158 179.868,-74.9158 179.868,-74.9158 179.927,-71.4162 176.719,-74.863 179.985,-67.9167 179.985,-67.9167\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"168.87\" y=\"-91.6701\">1</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd4e6906710>"
+        "<IPython.core.display.SVG at 0x7fe3e5c70518>"
        ]
       }
      ],
@@ -4266,7 +4266,7 @@
      "cell_type": "code",
      "collapsed": false,
      "input": [
-      "spot.decompose_strength(aut, 'st').show('.as')"
+      "spot.decompose_strength(aut, 'st').show('.bas')"
      ],
      "language": "python",
      "metadata": {},
@@ -4276,59 +4276,59 @@
        "output_type": "pyout",
        "prompt_number": 18,
        "svg": [
-        "<svg height=\"140pt\" viewBox=\"0.00 0.00 210.00 140.00\" width=\"210pt\" 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 136)\">\n",
+        "<svg height=\"150pt\" viewBox=\"0.00 0.00 219.74 150.00\" width=\"220pt\" 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 146)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-136 206,-136 206,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"80\" y=\"-117.8\">Inf(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"102\" y=\"-117.8\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"118\" y=\"-117.8\">)</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-146 215.74,-146 215.74,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"84.8701\" y=\"-127.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"106.87\" y=\"-127.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"122.87\" y=\"-127.8\">)</text>\n",
         "<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
-        "<polygon fill=\"none\" points=\"134,-8 134,-101 194,-101 194,-8 134,-8\" stroke=\"green\"/>\n",
+        "<polygon fill=\"none\" points=\"134,-8 134,-111 203.74,-111 203.74,-8 134,-8\" stroke=\"green\"/>\n",
         "</g>\n",
         "<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
-        "<polygon fill=\"none\" points=\"30,-12 30,-97 82,-97 82,-12 30,-12\" stroke=\"red\"/>\n",
+        "<polygon fill=\"none\" points=\"30,-17 30,-102 82,-102 82,-17 30,-17\" stroke=\"red\"/>\n",
         "</g>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node2\"><title>0</title>\n",
-        "<ellipse cx=\"56\" cy=\"-38\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-34.3\">0</text>\n",
+        "<ellipse cx=\"56\" cy=\"-43\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-39.3\">0</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
-        "<path d=\"M1.15491,-38C2.79388,-38 17.1543,-38 30.6317,-38\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"37.9419,-38 30.9419,-41.1501 34.4419,-38 30.9419,-38.0001 30.9419,-38.0001 30.9419,-38.0001 34.4419,-38 30.9418,-34.8501 37.9419,-38 37.9419,-38\" stroke=\"black\"/>\n",
+        "<path d=\"M1.15491,-43C2.79388,-43 17.1543,-43 30.6317,-43\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-43 30.9419,-46.1501 34.4419,-43 30.9419,-43.0001 30.9419,-43.0001 30.9419,-43.0001 34.4419,-43 30.9418,-39.8501 37.9419,-43 37.9419,-43\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
-        "<path d=\"M49.6208,-55.0373C48.3189,-64.8579 50.4453,-74 56,-74 60.166,-74 62.4036,-68.8576 62.7128,-62.1433\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"62.3792,-55.0373 65.8541,-61.8818 62.5434,-58.5335 62.7076,-62.0296 62.7076,-62.0296 62.7076,-62.0296 62.5434,-58.5335 59.561,-62.1774 62.3792,-55.0373 62.3792,-55.0373\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"38\" y=\"-77.8\">a &amp; !c</text>\n",
+        "<path d=\"M49.6208,-60.0373C48.3189,-69.8579 50.4453,-79 56,-79 60.166,-79 62.4036,-73.8576 62.7128,-67.1433\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"62.3792,-60.0373 65.8541,-66.8818 62.5434,-63.5335 62.7076,-67.0296 62.7076,-67.0296 62.7076,-67.0296 62.5434,-63.5335 59.561,-67.1774 62.3792,-60.0373 62.3792,-60.0373\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"38\" y=\"-82.8\">a &amp; !c</text>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g class=\"node\" id=\"node3\"><title>1</title>\n",
-        "<ellipse cx=\"164\" cy=\"-38\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"164\" cy=\"-38\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"164\" y=\"-34.3\">1</text>\n",
+        "<ellipse cx=\"168.87\" cy=\"-43\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"164.37\" y=\"-46.8\">1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"160.87\" y=\"-31.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
-        "<path d=\"M74.0307,-38C90.429,-38 115.526,-38 134.888,-38\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"141.998,-38 134.998,-41.1501 138.498,-38 134.998,-38.0001 134.998,-38.0001 134.998,-38.0001 138.498,-38 134.998,-34.8501 141.998,-38 141.998,-38\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-41.8\">a &amp; c</text>\n",
+        "<path d=\"M74.3234,-43C90.3789,-43 114.701,-43 134.521,-43\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"141.595,-43 134.595,-46.1501 138.095,-43 134.595,-43.0001 134.595,-43.0001 134.595,-43.0001 138.095,-43 134.595,-39.8501 141.595,-43 141.595,-43\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-46.8\">a &amp; c</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge4\"><title>1-&gt;1</title>\n",
-        "<path d=\"M153.933,-57.7575C152.223,-68.3499 155.578,-78 164,-78 170.448,-78 173.926,-72.3433 174.435,-64.9379\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"174.067,-57.7575 177.571,-64.5871 174.246,-61.2529 174.425,-64.7483 174.425,-64.7483 174.425,-64.7483 174.246,-61.2529 171.279,-64.9095 174.067,-57.7575 174.067,-57.7575\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"164\" y=\"-81.8\">1</text>\n",
+        "<path d=\"M157.755,-67.9167C156.845,-78.6664 160.55,-87.8701 168.87,-87.8701 175.24,-87.8701 178.905,-82.475 179.865,-75.1217\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"179.985,-67.9167 183.018,-74.9686 179.927,-71.4162 179.868,-74.9158 179.868,-74.9158 179.868,-74.9158 179.927,-71.4162 176.719,-74.863 179.985,-67.9167 179.985,-67.9167\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"168.87\" y=\"-91.6701\">1</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd4fc0bc978>"
+        "<IPython.core.display.SVG at 0x7fe3f40799e8>"
        ]
       }
      ],
@@ -4476,7 +4476,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd505081208>"
+        "<IPython.core.display.SVG at 0x7fe3f408bf28>"
        ]
       }
      ],
@@ -4601,7 +4601,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd50502ee10>"
+        "<IPython.core.display.SVG at 0x7fe3fc346208>"
        ]
       },
       {
@@ -4682,7 +4682,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd505029a20>"
+        "<IPython.core.display.SVG at 0x7fe3fc399748>"
        ]
       },
       {
@@ -4792,7 +4792,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fd4fc0dc470>"
+        "<IPython.core.display.SVG at 0x7fe3fc399748>"
        ]
       }
      ],