diff --git a/NEWS b/NEWS
index 1a309583c..92a77acb6 100644
--- a/NEWS
+++ b/NEWS
@@ -49,10 +49,13 @@ New in spot 1.99.4a (not yet released)
   * The Debian package is now compiled for all Python3 versions
     supported by Debian, not just the default one.
   * Automata now have get_name()/set_name() methods.
+  * spot.postprocess(aut, *options), or aut.postprocess(*options)
+    simplify the use of the spot.postprocessor object.  (Just like we
+    have spot.translate() on top of spot.translator().)
 
   Bugs fixed:
 
-  * Work around some strange weird exception raised when using the
+  * Work around some weird exception raised when using the
     randltlgenerator under Python 3.5.
   * Recognize "nullptr" formulas as None in Python.
   * Fix compilation of bench/stutter/
@@ -61,7 +64,7 @@ New in spot 1.99.4a (not yet released)
   * "randaut -Q0 1" used to segfault.
   * "ltlgrind -F FILENAME/COL" did not preserve other CSV columns.
   * "ltlgrind --help" did not document FORMAT.
-  * unabbreviate could easily use forbidden operators
+  * unabbreviate could easily use forbidden operators.
 
 New in spot 1.99.4 (2015-10-01)
 
diff --git a/wrap/python/spot.py b/wrap/python/spot.py
index 2641c6bf7..e7a8be5c5 100644
--- a/wrap/python/spot.py
+++ b/wrap/python/spot.py
@@ -373,25 +373,7 @@ def automaton(filename):
         raise RuntimeError("Failed to read automaton from {}".format(filename))
 
 
-def translate(formula, *args):
-    """Translate a formula into an automaton.
-
-    Keep in mind that pref expresses just a preference that may not be
-    satisfied.
-
-    The optional arguments should be strings among the following:
-    - at most one in 'TGBA', 'BA', or 'Monitor'
-      (type of automaton to build)
-    - at most one in 'Small', 'Deterministic', 'Any'
-      (preferred characteristics of the produced automaton)
-    - at most one in 'Low', 'Medium', 'High'
-      (optimization level)
-    - any combination of 'Complete', 'Unambiguous', and
-      'StateBasedAcceptance' (or 'SBAcc' for short)
-
-    The default corresponds to 'tgba', 'small' and 'high'.
-    """
-
+def _postproc_translate_options(obj, default_type, *args):
     type_ = None
     pref_ = None
     optm_ = None
@@ -404,6 +386,8 @@ def translate(formula, *args):
         if type_ is not None and type_ != val:
             raise ValueError("type cannot be both {} and {}"
                              .format(type_, val))
+        elif val == 'generic':
+            type_ = postprocessor.Generic
         elif val == 'tgba':
             type_ = postprocessor.TGBA
         elif val == 'ba':
@@ -452,6 +436,7 @@ def translate(formula, *args):
         'tgba': type_set,
         'ba': type_set,
         'monitor': type_set,
+        'generic': type_set,
         'small': pref_set,
         'deterministic': pref_set,
         'any': pref_set,
@@ -488,26 +473,77 @@ def translate(formula, *args):
                                  .format(arg, str(compat)))
 
     if type_ is None:
-        type_ = postprocessor.TGBA
+        type_ = default_type
     if pref_ is None:
         pref_ = postprocessor.Small
     if optm_ is None:
         optm_ = postprocessor.High
 
+    obj.set_type(type_)
+    obj.set_pref(pref_ | comp_ | unam_ | sbac_)
+    obj.set_level(optm_)
+
+
+def translate(formula, *args):
+    """Translate a formula into an automaton.
+
+    Keep in mind that 'Deterministic' expresses just a preference that
+    may not be satisfied.
+
+    The optional arguments should be strings among the following:
+    - at most one in 'TGBA', 'BA', or 'Monitor'
+      (type of automaton to build)
+    - at most one in 'Small', 'Deterministic', 'Any'
+      (preferred characteristics of the produced automaton)
+    - at most one in 'Low', 'Medium', 'High'
+      (optimization level)
+    - any combination of 'Complete', 'Unambiguous', and
+      'StateBasedAcceptance' (or 'SBAcc' for short)
+
+    The default corresponds to 'tgba', 'small' and 'high'.
+    """
+    a = translator(_bdd_dict)
+    _postproc_translate_options(a, postprocessor.TGBA, *args)
     if type(formula) == str:
         formula = parse_formula(formula)
-
-    a = translator(_bdd_dict)
-    a.set_type(type_)
-    a.set_pref(pref_ | comp_ | unam_ | sbac_)
-    a.set_level(optm_)
-
     return a.run(formula)
 
 
 formula.translate = translate
 
 
+def postprocess(automaton, *args):
+    """Post process an automaton.
+
+    This applies a number of simlification algorithms, depending on
+    the options supplied. Keep in mind that 'Deterministic' expresses
+    just a preference that may not be satisfied if the input is
+    not already 'Deterministic'.
+
+    The optional arguments should be strings among the following:
+    - at most one in 'Generic', 'TGBA', 'BA', or 'Monitor'
+      (type of automaton to build)
+    - at most one in 'Small', 'Deterministic', 'Any'
+      (preferred characteristics of the produced automaton)
+    - at most one in 'Low', 'Medium', 'High'
+      (optimization level)
+    - any combination of 'Complete' and 'StateBasedAcceptance'
+      (or 'SBAcc' for short)
+
+    The default corresponds to 'generic', 'small' and 'high'.
+    """
+    p = postprocessor()
+    if type(automaton) == str:
+        automaton = globals()['automaton'](automaton)
+    _postproc_translate_options(p, postprocessor.Generic, *args)
+    return p.run(automaton)
+
+
+twa.postprocess = postprocess
+twa.scc_filter = scc_filter
+twa.scc_filter_states = scc_filter_states
+
+
 # Wrapper around a formula iterator to which we add some methods of formula
 # (using _addfilter and _addmap), so that we can write things like
 # formulas.simplify().is_X_free().
diff --git a/wrap/python/tests/automata.ipynb b/wrap/python/tests/automata.ipynb
index 4617f3847..80d4f1167 100644
--- a/wrap/python/tests/automata.ipynb
+++ b/wrap/python/tests/automata.ipynb
@@ -17,7 +17,8 @@
    "pygments_lexer": "ipython3",
    "version": "3.4.3+"
   },
-  "name": ""
+  "name": "",
+  "signature": "sha256:d67ef646828999fe2beb805f3bb74087bbb30e12354c11fdfbe0f28c23bd7e5f"
  },
  "nbformat": 3,
  "nbformat_minor": 0,
@@ -28,6 +29,7 @@
      "cell_type": "code",
      "collapsed": false,
      "input": [
+      "from IPython.display import display\n",
       "import spot\n",
       "spot.setup()"
      ],
@@ -176,7 +178,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2e58013ea0> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d053f5d0> >"
        ]
       }
      ],
@@ -315,7 +317,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG object>"
+        "<IPython.core.display.SVG at 0x7f48d04f8470>"
        ]
       }
      ],
@@ -468,7 +470,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG object>"
+        "<IPython.core.display.SVG at 0x7f48d005f518>"
        ]
       }
      ],
@@ -568,7 +570,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2e4afe6720> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d05238d0> >"
        ]
       }
      ],
@@ -638,7 +640,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2e4afe6870> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d05237e0> >"
        ]
       }
      ],
@@ -714,7 +716,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2e4afe6600> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d0523750> >"
        ]
       }
      ],
@@ -837,7 +839,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG object>"
+        "<IPython.core.display.SVG at 0x7f48d005f5c0>"
        ]
       }
      ],
@@ -1027,7 +1029,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG object>"
+        "<IPython.core.display.SVG at 0x7f48d0027710>"
        ]
       }
      ],
@@ -1174,7 +1176,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2e4afe6180> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d0523ab0> >"
        ]
       }
      ],
@@ -1275,7 +1277,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2e4afe6330> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d0523870> >"
        ]
       }
      ],
@@ -1393,7 +1395,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2e4afe66c0> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d05237b0> >"
        ]
       }
      ],
@@ -1492,7 +1494,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2e4afe6de0> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d04c2120> >"
        ]
       }
      ],
@@ -1962,7 +1964,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2e4afe6d20> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d0523f30> >"
        ]
       }
      ],
@@ -2039,15 +2041,399 @@
      "collapsed": false,
      "input": [
       "a = spot.automaton('example1.aut')\n",
-      "spot.remove_fin(a)"
+      "display(a.show('.a'))\n",
+      "display(spot.remove_fin(a).show('.a'))\n",
+      "display(a.postprocess('TGBA', 'complete').show('.a'))\n",
+      "display(a.postprocess('BA'))"
      ],
      "language": "python",
      "metadata": {},
      "outputs": [
       {
        "metadata": {},
-       "output_type": "pyout",
-       "prompt_number": 19,
+       "output_type": "display_data",
+       "svg": [
+        "<svg height=\"178pt\" viewBox=\"0.00 0.00 361.00 178.46\" width=\"361pt\" 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 174.462)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-174.462 357,-174.462 357,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"8\" y=\"-156.262\">(Fin(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"36\" y=\"-156.262\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"52\" y=\"-156.262\">) &amp; Fin(</text>\n",
+        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"98\" y=\"-156.262\">\u2778</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"114\" y=\"-156.262\">) &amp; Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"157\" y=\"-156.262\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"173\" y=\"-156.262\">)) | (Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"217\" y=\"-156.262\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"233\" y=\"-156.262\">)&amp;Inf(</text>\n",
+        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"269\" y=\"-156.262\">\u2778</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"285\" y=\"-156.262\">)) | Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"325\" y=\"-156.262\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"341\" y=\"-156.262\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"87.75\" cy=\"-24.4625\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"87.75\" y=\"-20.7625\">0</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
+        "<path d=\"M32.9049,-24.4625C34.5439,-24.4625 48.9043,-24.4625 62.3817,-24.4625\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"69.6919,-24.4625 62.6919,-27.6126 66.1919,-24.4625 62.6919,-24.4626 62.6919,-24.4626 62.6919,-24.4626 66.1919,-24.4625 62.6918,-21.3126 69.6919,-24.4625 69.6919,-24.4625\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
+        "<path d=\"M81.3708,-41.4998C80.0689,-51.3204 82.1953,-60.4625 87.75,-60.4625 91.916,-60.4625 94.1536,-55.32 94.4628,-48.6058\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"94.1292,-41.4998 97.6041,-48.3443 94.2934,-44.9959 94.4576,-48.4921 94.4576,-48.4921 94.4576,-48.4921 94.2934,-44.9959 91.311,-48.6398 94.1292,-41.4998 94.1292,-41.4998\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"83.25\" y=\"-79.2625\">1</text>\n",
+        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"79.75\" y=\"-64.2625\">\u2778</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
+        "<ellipse cx=\"191.75\" cy=\"-83.4625\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"191.75\" y=\"-79.7625\">1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
+        "<path d=\"M96.2222,-40.4354C102.139,-51.2481 111.454,-64.894 123.75,-72.4625 136.455,-80.2825 152.974,-83.0589 166.43,-83.8673\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"173.547,-84.1335 166.434,-87.0196 170.049,-84.0026 166.551,-83.8718 166.551,-83.8718 166.551,-83.8718 170.049,-84.0026 166.669,-80.724 173.547,-84.1335 173.547,-84.1335\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"136.25\" y=\"-100.262\">a</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"123.75\" y=\"-86.2625\">\u2776</text>\n",
+        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"139.75\" y=\"-86.2625\">\u2778</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
+        "<ellipse cx=\"300.75\" cy=\"-24.4625\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"300.75\" y=\"-20.7625\">2</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;2</title>\n",
+        "<path d=\"M105.831,-23.2907C111.528,-22.9521 117.91,-22.6292 123.75,-22.4625 186.391,-20.6742 202.109,-20.6742 264.75,-22.4625 268.218,-22.5615 271.876,-22.7155 275.469,-22.8952\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"282.669,-23.2907 275.506,-26.0519 279.174,-23.0987 275.679,-22.9067 275.679,-22.9067 275.679,-22.9067 279.174,-23.0987 275.852,-19.7614 282.669,-23.2907 282.669,-23.2907\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"186.25\" y=\"-38.2625\">!a</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"175.75\" y=\"-24.2625\">\u24ff</text>\n",
+        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"191.75\" y=\"-24.2625\">\u2778</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;0</title>\n",
+        "<path d=\"M182.416,-67.7662C176.334,-57.843 167.17,-45.5882 155.75,-38.4625 142.991,-30.5007 126.471,-26.9895 113.029,-25.4742\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"105.92,-24.8221 113.179,-22.3249 109.406,-25.1419 112.891,-25.4617 112.891,-25.4617 112.891,-25.4617 109.406,-25.1419 112.603,-28.5985 105.92,-24.8221 105.92,-24.8221\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"135.25\" y=\"-57.2625\">b</text>\n",
+        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"131.75\" y=\"-42.2625\">\u2778</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;1</title>\n",
+        "<path d=\"M182.771,-99.3785C180.429,-109.613 183.422,-119.462 191.75,-119.462 198.126,-119.462 201.375,-113.689 201.496,-106.389\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"200.729,-99.3785 204.622,-105.994 201.11,-102.858 201.491,-106.337 201.491,-106.337 201.491,-106.337 201.11,-102.858 198.36,-106.68 200.729,-99.3785 200.729,-99.3785\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"174.75\" y=\"-137.262\">a &amp; b</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"175.75\" y=\"-123.262\">\u24ff</text>\n",
+        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"191.75\" y=\"-123.262\">\u2778</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>1-&gt;2</title>\n",
+        "<path d=\"M210.007,-84.4326C225.435,-84.5035 248.11,-82.5775 264.75,-72.4625 274.871,-66.3102 282.955,-56.0178 288.793,-46.5381\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"292.304,-40.4776 291.521,-48.1137 290.549,-43.5062 288.795,-46.5348 288.795,-46.5348 288.795,-46.5348 290.549,-43.5062 286.069,-44.9558 292.304,-40.4776 292.304,-40.4776\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"227.75\" y=\"-100.262\">!a &amp; b</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"230.25\" y=\"-86.2625\">\u2777</text>\n",
+        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"246.25\" y=\"-86.2625\">\u2778</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;0</title>\n",
+        "<path d=\"M283.519,-18.1905C259.601,-9.70234 213.427,3.81075 173.75,-1.46246 152.401,-4.2998 128.809,-10.9793 111.907,-16.4132\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"105.099,-18.6508 110.765,-13.4725 108.424,-17.5579 111.749,-16.465 111.749,-16.465 111.749,-16.465 108.424,-17.5579 112.732,-19.4575 105.099,-18.6508 105.099,-18.6508\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"185.25\" y=\"-5.26246\">!b</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>2-&gt;1</title>\n",
+        "<path d=\"M282.526,-24.4701C267.12,-25.2161 244.459,-28.1972 227.75,-38.4625 218.611,-44.0772 210.937,-53.0028 205.126,-61.4297\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"201.051,-67.7136 202.217,-60.1264 202.955,-64.7769 204.86,-61.8401 204.86,-61.8401 204.86,-61.8401 202.955,-64.7769 207.503,-63.5538 201.051,-67.7136 201.051,-67.7136\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"227.75\" y=\"-57.2625\">a &amp; !b</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238.25\" y=\"-42.2625\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>2-&gt;2</title>\n",
+        "<path d=\"M291.517,-40.0039C288.919,-50.3712 291.996,-60.4625 300.75,-60.4625 307.452,-60.4625 310.827,-54.5471 310.874,-47.1215\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"309.983,-40.0039 313.979,-46.5579 310.418,-43.4768 310.853,-46.9496 310.853,-46.9496 310.853,-46.9496 310.418,-43.4768 307.727,-47.3413 309.983,-40.0039 309.983,-40.0039\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"280.25\" y=\"-79.2625\">!a &amp; !b</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"292.75\" y=\"-64.2625\">\u24ff</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG at 0x7f48d00277b8>"
+       ]
+      },
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<svg height=\"176pt\" viewBox=\"0.00 0.00 410.50 175.53\" width=\"411pt\" 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 171.526)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-171.526 406.5,-171.526 406.5,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"97.75\" y=\"-153.326\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"119.75\" y=\"-153.326\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"135.75\" y=\"-153.326\">) | Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"172.75\" y=\"-153.326\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"188.75\" y=\"-153.326\">) | (Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"228.75\" y=\"-153.326\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"244.75\" y=\"-153.326\">)&amp;Inf(</text>\n",
+        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"280.75\" y=\"-153.326\">\u2778</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"296.75\" y=\"-153.326\">))</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-25.5257\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-21.8257\">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,-25.5257C2.79388,-25.5257 17.1543,-25.5257 30.6317,-25.5257\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-25.5257 30.9419,-28.6758 34.4419,-25.5258 30.9419,-25.5258 30.9419,-25.5258 30.9419,-25.5258 34.4419,-25.5258 30.9418,-22.3758 37.9419,-25.5257 37.9419,-25.5257\" 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,-42.5631C48.3189,-52.3837 50.4453,-61.5257 56,-61.5257 60.166,-61.5257 62.4036,-56.3833 62.7128,-49.669\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"62.3792,-42.5631 65.8541,-49.4076 62.5434,-46.0592 62.7076,-49.5554 62.7076,-49.5554 62.7076,-49.5554 62.5434,-46.0592 59.561,-49.7031 62.3792,-42.5631 62.3792,-42.5631\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"51.5\" y=\"-80.3257\">1</text>\n",
+        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"48\" y=\"-65.3257\">\u2778</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
+        "<ellipse cx=\"160\" cy=\"-78.5257\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"160\" y=\"-74.8257\">1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
+        "<path d=\"M64.2739,-41.8373C70.0973,-52.8095 79.3819,-66.507 92,-73.5257 104.901,-80.7019 121.422,-82.0046 134.83,-81.4873\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"141.916,-81.0385 135.129,-84.6248 138.423,-81.2598 134.93,-81.4811 134.93,-81.4811 134.93,-81.4811 138.423,-81.2598 134.731,-78.3374 141.916,-81.0385 141.916,-81.0385\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"104.5\" y=\"-98.3257\">a</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-84.3257\">\u2776</text>\n",
+        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"108\" y=\"-84.3257\">\u2778</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
+        "<ellipse cx=\"269\" cy=\"-25.5257\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"269\" y=\"-21.8257\">2</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;2</title>\n",
+        "<path d=\"M74.248,-24.476C91.4149,-23.4873 118.517,-22.078 142,-21.5257 182.443,-20.5747 192.59,-21.6366 233,-23.5257 236.465,-23.6877 240.123,-23.8768 243.715,-24.0727\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"250.914,-24.4783 243.748,-27.2295 247.419,-24.2814 243.925,-24.0845 243.925,-24.0845 243.925,-24.0845 247.419,-24.2814 244.102,-20.9395 250.914,-24.4783 250.914,-24.4783\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"154.5\" y=\"-40.3257\">!a</text>\n",
+        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"152\" y=\"-25.3257\">\u2778</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;0</title>\n",
+        "<path d=\"M149.358,-63.7736C143.113,-55.3948 134.248,-45.4299 124,-39.5257 110.969,-32.0177 94.4463,-28.5115 81.0699,-26.8854\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"74.0044,-26.162 81.2889,-23.7415 77.4862,-26.5185 80.968,-26.8751 80.968,-26.8751 80.968,-26.8751 77.4862,-26.5185 80.6471,-30.0087 74.0044,-26.162 74.0044,-26.162\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"103.5\" y=\"-58.3257\">b</text>\n",
+        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"100\" y=\"-43.3257\">\u2778</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;1</title>\n",
+        "<path d=\"M151.021,-94.4418C148.679,-104.676 151.672,-114.526 160,-114.526 166.376,-114.526 169.625,-108.752 169.746,-101.453\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"168.979,-94.4418 172.872,-101.057 169.36,-97.921 169.741,-101.4 169.741,-101.4 169.741,-101.4 169.36,-97.921 166.61,-101.743 168.979,-94.4418 168.979,-94.4418\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"143\" y=\"-133.326\">a &amp; b</text>\n",
+        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"152\" y=\"-118.326\">\u2778</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>1-&gt;2</title>\n",
+        "<path d=\"M177.894,-76.2046C193.077,-73.5836 215.598,-68.3394 233,-58.5257 239.656,-54.7722 246.025,-49.4861 251.463,-44.2425\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"256.565,-39.0714 253.891,-46.2665 254.107,-41.5627 251.649,-44.054 251.649,-44.054 251.649,-44.054 254.107,-41.5627 249.406,-41.8416 256.565,-39.0714 256.565,-39.0714\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"196\" y=\"-89.3257\">!a &amp; b</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"198.5\" y=\"-75.3257\">\u2777</text>\n",
+        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"214.5\" y=\"-75.3257\">\u2778</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;0</title>\n",
+        "<path d=\"M252.173,-19.1294C228.38,-10.2839 181.925,4.00261 142,-1.52575 120.47,-4.50705 96.7218,-11.5451 79.8133,-17.2333\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.012,-19.5727 78.6068,-14.3171 76.3217,-18.4343 79.6314,-17.2958 79.6314,-17.2958 79.6314,-17.2958 76.3217,-18.4343 80.6559,-20.2745 73.012,-19.5727 73.012,-19.5727\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"153.5\" y=\"-5.32575\">!b</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>2-&gt;1</title>\n",
+        "<path d=\"M250.943,-25.8163C235.65,-26.7527 213.06,-29.8545 196,-39.5257 187.962,-44.0825 180.793,-51.162 175.069,-58.0454\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"170.613,-63.7216 172.457,-56.2704 172.774,-60.9685 174.935,-58.2155 174.935,-58.2155 174.935,-58.2155 172.774,-60.9685 177.413,-60.1606 170.613,-63.7216 170.613,-63.7216\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"196\" y=\"-43.3257\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>2-&gt;2</title>\n",
+        "<path d=\"M259.767,-41.0672C257.169,-51.4344 260.246,-61.5257 269,-61.5257 275.702,-61.5257 279.077,-55.6104 279.124,-48.1848\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"278.233,-41.0672 282.229,-47.6212 278.668,-44.54 279.103,-48.0129 279.103,-48.0129 279.103,-48.0129 278.668,-44.54 275.977,-48.4046 278.233,-41.0672 278.233,-41.0672\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"248.5\" y=\"-65.3257\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
+        "<ellipse cx=\"382\" cy=\"-25.5257\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"382\" y=\"-21.8257\">3</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge11\"><title>2-&gt;3</title>\n",
+        "<path d=\"M287.344,-25.5257C305.998,-25.5257 335.797,-25.5257 356.763,-25.5257\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"363.778,-25.5257 356.778,-28.6758 360.278,-25.5258 356.778,-25.5258 356.778,-25.5258 356.778,-25.5258 360.278,-25.5258 356.778,-22.3758 363.778,-25.5257 363.778,-25.5257\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"305\" y=\"-29.3257\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
+        "<path d=\"M372.425,-41.0672C369.73,-51.4344 372.922,-61.5257 382,-61.5257 388.95,-61.5257 392.45,-55.6104 392.499,-48.1848\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"391.575,-41.0672 395.6,-47.6029 392.026,-44.538 392.477,-48.0088 392.477,-48.0088 392.477,-48.0088 392.026,-44.538 389.353,-48.4148 391.575,-41.0672 391.575,-41.0672\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"361.5\" y=\"-80.3257\">!a &amp; !b</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"374\" y=\"-65.3257\">\u24ff</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG at 0x7f48c1bcb668>"
+       ]
+      },
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<svg height=\"193pt\" viewBox=\"0.00 0.00 491.00 193.31\" width=\"491pt\" 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 189.31)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-189.31 487,-189.31 487,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"220.5\" y=\"-171.11\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242.5\" y=\"-171.11\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"258.5\" y=\"-171.11\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>1</title>\n",
+        "<ellipse cx=\"56\" cy=\"-39.31\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-35.61\">1</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;1</title>\n",
+        "<path d=\"M1.15491,-39.31C2.79388,-39.31 17.1543,-39.31 30.6317,-39.31\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-39.31 30.9419,-42.4601 34.4419,-39.31 30.9419,-39.3101 30.9419,-39.3101 30.9419,-39.3101 34.4419,-39.31 30.9418,-36.1601 37.9419,-39.31 37.9419,-39.31\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;1</title>\n",
+        "<path d=\"M49.6208,-56.3473C48.3189,-66.1679 50.4453,-75.31 56,-75.31 60.166,-75.31 62.4036,-70.1675 62.7128,-63.4533\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"62.3792,-56.3473 65.8541,-63.1918 62.5434,-59.8434 62.7076,-63.3396 62.7076,-63.3396 62.7076,-63.3396 62.5434,-59.8434 59.561,-63.4873 62.3792,-56.3473 62.3792,-56.3473\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-79.11\">1</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
+        "<ellipse cx=\"144\" cy=\"-94.31\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"144\" y=\"-90.61\">2</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;2</title>\n",
+        "<path d=\"M68.7319,-52.3683C75.1386,-58.9554 83.4866,-66.7125 92,-72.31 100.604,-77.9668 110.903,-82.7322 119.987,-86.3656\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"126.648,-88.9195 118.984,-89.3547 123.38,-87.6665 120.112,-86.4135 120.112,-86.4135 120.112,-86.4135 123.38,-87.6665 121.239,-83.4723 126.648,-88.9195 126.648,-88.9195\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"96.5\" y=\"-99.11\">a</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-84.11\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>3</title>\n",
+        "<ellipse cx=\"253\" cy=\"-29.31\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"253\" y=\"-25.61\">3</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;3</title>\n",
+        "<path d=\"M74.3049,-38.4225C109.084,-36.639 187.544,-32.6154 227.548,-30.5639\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"235.012,-30.1811 228.183,-33.6856 231.517,-30.3604 228.021,-30.5397 228.021,-30.5397 228.021,-30.5397 231.517,-30.3604 227.86,-27.3939 235.012,-30.1811 235.012,-30.1811\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"138.5\" y=\"-39.11\">!a</text>\n",
+        "</g>\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>0</title>\n",
+        "<ellipse cx=\"366\" cy=\"-45.31\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"366\" y=\"-41.61\">0</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
+        "<path d=\"M357.635,-61.6002C355.618,-71.6991 358.406,-81.31 366,-81.31 371.695,-81.31 374.688,-75.9039 374.977,-68.9403\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"374.365,-61.6002 378.086,-68.3144 374.656,-65.0881 374.947,-68.576 374.947,-68.576 374.947,-68.576 374.656,-65.0881 371.807,-68.8377 374.365,-61.6002 374.365,-61.6002\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"345.5\" y=\"-100.11\">!a &amp; !b</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"358\" y=\"-85.11\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>4</title>\n",
+        "<ellipse cx=\"465\" cy=\"-45.31\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"465\" y=\"-41.61\">4</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;4</title>\n",
+        "<path d=\"M384.342,-45.31C399.791,-45.31 422.554,-45.31 439.795,-45.31\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"446.808,-45.31 439.809,-48.4601 443.308,-45.31 439.808,-45.3101 439.808,-45.3101 439.808,-45.3101 443.308,-45.31 439.808,-42.1601 446.808,-45.31 446.808,-45.31\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"402\" y=\"-49.11\">a | b</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge16\"><title>4-&gt;4</title>\n",
+        "<path d=\"M456.635,-61.6002C454.618,-71.6991 457.406,-81.31 465,-81.31 470.695,-81.31 473.688,-75.9039 473.977,-68.9403\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"473.365,-61.6002 477.086,-68.3144 473.656,-65.0881 473.947,-68.576 473.947,-68.576 473.947,-68.576 473.656,-65.0881 470.807,-68.8377 473.365,-61.6002 473.365,-61.6002\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"465\" y=\"-85.11\">1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;1</title>\n",
+        "<path d=\"M133.659,-79.4339C127.406,-70.6289 118.427,-59.9353 108,-53.31 99.9283,-48.1812 89.9824,-44.9083 81.0235,-42.8301\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"74.105,-41.407 81.5961,-39.732 77.5332,-42.1122 80.9614,-42.8174 80.9614,-42.8174 80.9614,-42.8174 77.5332,-42.1122 80.3267,-45.9028 74.105,-41.407 74.105,-41.407\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"95.5\" y=\"-57.11\">b</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>2-&gt;4</title>\n",
+        "<path d=\"M157.074,-106.842C163.323,-112.423 171.429,-118.388 180,-121.31 218.487,-134.43 239.141,-178.096 384,-120.31 411.643,-109.283 435.358,-83.7555 449.633,-65.5495\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"454.105,-59.6875 452.364,-67.1636 451.982,-62.4703 449.859,-65.2531 449.859,-65.2531 449.859,-65.2531 451.982,-62.4703 447.355,-63.3427 454.105,-59.6875 454.105,-59.6875\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"303\" y=\"-151.11\">!b</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;2</title>\n",
+        "<path d=\"M136.332,-110.6C134.483,-120.699 137.039,-130.31 144,-130.31 149.221,-130.31 151.964,-124.904 152.229,-117.94\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"151.668,-110.6 155.342,-117.34 151.935,-114.09 152.201,-117.58 152.201,-117.58 152.201,-117.58 151.935,-114.09 149.06,-117.82 151.668,-110.6 151.668,-110.6\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"127\" y=\"-134.11\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>2-&gt;3</title>\n",
+        "<path d=\"M161.928,-92.0185C177.341,-89.2964 200.189,-83.6164 217,-72.31 225.529,-66.5738 233.032,-58.1415 238.882,-50.2604\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"243.022,-44.3948 241.559,-51.9302 241.003,-47.2543 238.985,-50.1137 238.985,-50.1137 238.985,-50.1137 241.003,-47.2543 236.412,-48.2972 243.022,-44.3948 243.022,-44.3948\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"180\" y=\"-106.11\">!a &amp; b</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"190.5\" y=\"-91.11\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge12\"><title>3-&gt;1</title>\n",
+        "<path d=\"M235.605,-24.3158C211.482,-17.6543 165.056,-7.45277 126,-14.31 109.757,-17.1619 92.2994,-23.521 79.0084,-29.1117\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"72.4663,-31.9426 77.6396,-26.2716 75.6785,-30.5526 78.8906,-29.1626 78.8906,-29.1626 78.8906,-29.1626 75.6785,-30.5526 80.1416,-32.0535 72.4663,-31.9426 72.4663,-31.9426\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"137.5\" y=\"-18.11\">!b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge11\"><title>3-&gt;0</title>\n",
+        "<path d=\"M270.859,-31.74C289.521,-34.4301 319.756,-38.7883 340.912,-41.8378\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"347.983,-42.857 340.605,-44.976 344.519,-42.3577 341.054,-41.8583 341.054,-41.8583 341.054,-41.8583 344.519,-42.3577 341.504,-38.7405 347.983,-42.857 347.983,-42.857\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"289\" y=\"-43.11\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge15\"><title>3-&gt;4</title>\n",
+        "<path d=\"M269.708,-21.7136C294.247,-10.8458 343.105,6.77258 384,-3.30996 405.723,-8.66554 428.072,-21.0901 443.607,-31.0447\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"449.826,-35.1319 442.247,-33.9197 446.901,-33.2096 443.977,-31.2873 443.977,-31.2873 443.977,-31.2873 446.901,-33.2096 445.707,-28.6549 449.826,-35.1319 449.826,-35.1319\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"361.5\" y=\"-7.10996\">b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge13\"><title>3-&gt;2</title>\n",
+        "<path d=\"M235.13,-32.24C219.759,-35.5063 196.937,-41.8971 180,-53.31 171.996,-58.7034 164.761,-66.4047 158.974,-73.6794\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"154.469,-79.6297 156.183,-72.1474 156.582,-76.8393 158.695,-74.049 158.695,-74.049 158.695,-74.049 156.582,-76.8393 161.206,-75.9505 154.469,-79.6297 154.469,-79.6297\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"180\" y=\"-57.11\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge14\"><title>3-&gt;3</title>\n",
+        "<path d=\"M243.767,-44.8514C241.169,-55.2187 244.246,-65.31 253,-65.31 259.702,-65.31 263.077,-59.3946 263.124,-51.969\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"262.233,-44.8514 266.229,-51.4054 262.668,-48.3243 263.103,-51.7971 263.103,-51.7971 263.103,-51.7971 262.668,-48.3243 259.977,-52.1888 262.233,-44.8514 262.233,-44.8514\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"232.5\" y=\"-69.11\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG at 0x7f48d002b8d0>"
+       ]
+      },
+      {
+       "metadata": {},
+       "output_type": "display_data",
        "svg": [
         "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
         "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
@@ -2055,117 +2441,145 @@
         "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
         " -->\n",
         "<!-- Title: G Pages: 1 -->\n",
-        "<svg width=\"411pt\" height=\"153pt\"\n",
-        " viewBox=\"0.00 0.00 410.50 152.53\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 148.526)\">\n",
+        "<svg width=\"527pt\" height=\"185pt\"\n",
+        " viewBox=\"0.00 0.00 527.00 185.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 181)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-148.526 406.5,-148.526 406.5,4 -4,4\"/>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-181 523,-181 523,4 -4,4\"/>\n",
         "<!-- I -->\n",
-        "<!-- 0 -->\n",
-        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-25.5257\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"56\" y=\"-21.8257\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
-        "</g>\n",
-        "<!-- I&#45;&gt;0 -->\n",
-        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-25.5257C2.79388,-25.5257 17.1543,-25.5257 30.6317,-25.5257\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-25.5257 30.9419,-28.6758 34.4419,-25.5258 30.9419,-25.5258 30.9419,-25.5258 30.9419,-25.5258 34.4419,-25.5258 30.9418,-22.3758 37.9419,-25.5257 37.9419,-25.5257\"/>\n",
-        "</g>\n",
-        "<!-- 0&#45;&gt;0 -->\n",
-        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-42.5631C48.3189,-52.3837 50.4453,-61.5257 56,-61.5257 60.166,-61.5257 62.4036,-56.3833 62.7128,-49.669\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-42.5631 65.8541,-49.4076 62.5434,-46.0592 62.7076,-49.5554 62.7076,-49.5554 62.7076,-49.5554 62.5434,-46.0592 59.561,-49.7031 62.3792,-42.5631 62.3792,-42.5631\"/>\n",
-        "<text text-anchor=\"start\" x=\"51.5\" y=\"-80.3257\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
-        "<text text-anchor=\"start\" x=\"48\" y=\"-65.3257\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#b276b2\">\u2778</text>\n",
-        "</g>\n",
-        "<!-- 1 -->\n",
-        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"160\" cy=\"-78.5257\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"160\" y=\"-74.8257\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
-        "</g>\n",
-        "<!-- 0&#45;&gt;1 -->\n",
-        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M64.2739,-41.8373C70.0973,-52.8095 79.3819,-66.507 92,-73.5257 104.901,-80.7019 121.422,-82.0046 134.83,-81.4873\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"141.916,-81.0385 135.129,-84.6248 138.423,-81.2598 134.93,-81.4811 134.93,-81.4811 134.93,-81.4811 138.423,-81.2598 134.731,-78.3374 141.916,-81.0385 141.916,-81.0385\"/>\n",
-        "<text text-anchor=\"start\" x=\"104.5\" y=\"-98.3257\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
-        "<text text-anchor=\"start\" x=\"92\" y=\"-84.3257\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
-        "<text text-anchor=\"start\" x=\"108\" y=\"-84.3257\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#b276b2\">\u2778</text>\n",
-        "</g>\n",
         "<!-- 2 -->\n",
-        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"269\" cy=\"-25.5257\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"269\" y=\"-21.8257\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+        "<g id=\"node2\" class=\"node\"><title>2</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-108\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-104.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
         "</g>\n",
-        "<!-- 0&#45;&gt;2 -->\n",
-        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M74.248,-24.476C91.4149,-23.4873 118.517,-22.078 142,-21.5257 182.443,-20.5747 192.59,-21.6366 233,-23.5257 236.465,-23.6877 240.123,-23.8768 243.715,-24.0727\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"250.914,-24.4783 243.748,-27.2295 247.419,-24.2814 243.925,-24.0845 243.925,-24.0845 243.925,-24.0845 247.419,-24.2814 244.102,-20.9395 250.914,-24.4783 250.914,-24.4783\"/>\n",
-        "<text text-anchor=\"start\" x=\"154.5\" y=\"-40.3257\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
-        "<text text-anchor=\"start\" x=\"152\" y=\"-25.3257\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#b276b2\">\u2778</text>\n",
-        "</g>\n",
-        "<!-- 1&#45;&gt;0 -->\n",
-        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M149.358,-63.7736C143.113,-55.3948 134.248,-45.4299 124,-39.5257 110.969,-32.0177 94.4463,-28.5115 81.0699,-26.8854\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"74.0044,-26.162 81.2889,-23.7415 77.4862,-26.5185 80.968,-26.8751 80.968,-26.8751 80.968,-26.8751 77.4862,-26.5185 80.6471,-30.0087 74.0044,-26.162 74.0044,-26.162\"/>\n",
-        "<text text-anchor=\"start\" x=\"103.5\" y=\"-58.3257\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
-        "<text text-anchor=\"start\" x=\"100\" y=\"-43.3257\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#b276b2\">\u2778</text>\n",
-        "</g>\n",
-        "<!-- 1&#45;&gt;1 -->\n",
-        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M151.021,-94.4418C148.679,-104.676 151.672,-114.526 160,-114.526 166.376,-114.526 169.625,-108.752 169.746,-101.453\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"168.979,-94.4418 172.872,-101.057 169.36,-97.921 169.741,-101.4 169.741,-101.4 169.741,-101.4 169.36,-97.921 166.61,-101.743 168.979,-94.4418 168.979,-94.4418\"/>\n",
-        "<text text-anchor=\"start\" x=\"143\" y=\"-133.326\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
-        "<text text-anchor=\"start\" x=\"152\" y=\"-118.326\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#b276b2\">\u2778</text>\n",
-        "</g>\n",
-        "<!-- 1&#45;&gt;2 -->\n",
-        "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M177.894,-76.2046C193.077,-73.5836 215.598,-68.3394 233,-58.5257 239.656,-54.7722 246.025,-49.4861 251.463,-44.2425\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"256.565,-39.0714 253.891,-46.2665 254.107,-41.5627 251.649,-44.054 251.649,-44.054 251.649,-44.054 254.107,-41.5627 249.406,-41.8416 256.565,-39.0714 256.565,-39.0714\"/>\n",
-        "<text text-anchor=\"start\" x=\"196\" y=\"-89.3257\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
-        "<text text-anchor=\"start\" x=\"198.5\" y=\"-75.3257\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#faa43a\">\u2777</text>\n",
-        "<text text-anchor=\"start\" x=\"214.5\" y=\"-75.3257\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#b276b2\">\u2778</text>\n",
-        "</g>\n",
-        "<!-- 2&#45;&gt;0 -->\n",
-        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M252.173,-19.1294C228.38,-10.2839 181.925,4.00261 142,-1.52575 120.47,-4.50705 96.7218,-11.5451 79.8133,-17.2333\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"73.012,-19.5727 78.6068,-14.3171 76.3217,-18.4343 79.6314,-17.2958 79.6314,-17.2958 79.6314,-17.2958 76.3217,-18.4343 80.6559,-20.2745 73.012,-19.5727 73.012,-19.5727\"/>\n",
-        "<text text-anchor=\"start\" x=\"153.5\" y=\"-5.32575\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
-        "</g>\n",
-        "<!-- 2&#45;&gt;1 -->\n",
-        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M250.943,-25.8163C235.65,-26.7527 213.06,-29.8545 196,-39.5257 187.962,-44.0825 180.793,-51.162 175.069,-58.0454\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"170.613,-63.7216 172.457,-56.2704 172.774,-60.9685 174.935,-58.2155 174.935,-58.2155 174.935,-58.2155 172.774,-60.9685 177.413,-60.1606 170.613,-63.7216 170.613,-63.7216\"/>\n",
-        "<text text-anchor=\"start\" x=\"196\" y=\"-43.3257\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "<!-- I&#45;&gt;2 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-108C2.79388,-108 17.1543,-108 30.6317,-108\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-108 30.9419,-111.15 34.4419,-108 30.9419,-108 30.9419,-108 30.9419,-108 34.4419,-108 30.9418,-104.85 37.9419,-108 37.9419,-108\"/>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
-        "<g id=\"edge10\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M259.767,-41.0672C257.169,-51.4344 260.246,-61.5257 269,-61.5257 275.702,-61.5257 279.077,-55.6104 279.124,-48.1848\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"278.233,-41.0672 282.229,-47.6212 278.668,-44.54 279.103,-48.0129 279.103,-48.0129 279.103,-48.0129 278.668,-44.54 275.977,-48.4046 278.233,-41.0672 278.233,-41.0672\"/>\n",
-        "<text text-anchor=\"start\" x=\"248.5\" y=\"-65.3257\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-125.037C48.3189,-134.858 50.4453,-144 56,-144 60.166,-144 62.4036,-138.858 62.7128,-132.143\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-125.037 65.8541,-131.882 62.5434,-128.533 62.7076,-132.03 62.7076,-132.03 62.7076,-132.03 62.5434,-128.533 59.561,-132.177 62.3792,-125.037 62.3792,-125.037\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-147.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"141\" cy=\"-155\" rx=\"18\" ry=\"18\"/>\n",
+        "<ellipse fill=\"none\" stroke=\"black\" cx=\"141\" cy=\"-155\" rx=\"22\" ry=\"22\"/>\n",
+        "<text text-anchor=\"middle\" x=\"141\" y=\"-151.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;0 -->\n",
+        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M68.4614,-121.499C74.7941,-128.206 83.1575,-135.938 92,-141 98.0857,-144.484 105.11,-147.163 111.875,-149.198\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"119.057,-151.162 111.474,-152.354 115.681,-150.239 112.305,-149.316 112.305,-149.316 112.305,-149.316 115.681,-150.239 113.136,-146.277 119.057,-151.162 119.057,-151.162\"/>\n",
+        "<text text-anchor=\"start\" x=\"93\" y=\"-148.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
         "</g>\n",
         "<!-- 3 -->\n",
-        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"382\" cy=\"-25.5257\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"382\" y=\"-21.8257\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
+        "<g id=\"node7\" class=\"node\"><title>3</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"377.5\" cy=\"-53\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"377.5\" y=\"-49.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;3 -->\n",
-        "<g id=\"edge11\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M287.344,-25.5257C305.998,-25.5257 335.797,-25.5257 356.763,-25.5257\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"363.778,-25.5257 356.778,-28.6758 360.278,-25.5258 356.778,-25.5258 356.778,-25.5258 356.778,-25.5258 360.278,-25.5258 356.778,-22.3758 363.778,-25.5257 363.778,-25.5257\"/>\n",
-        "<text text-anchor=\"start\" x=\"305\" y=\"-29.3257\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M73.5012,-103.661C112.314,-93.6736 212.566,-69.1368 298,-59 316.08,-56.8548 336.598,-55.3176 352.122,-54.3364\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"359.309,-53.8992 352.513,-57.4685 355.815,-54.1118 352.322,-54.3244 352.322,-54.3244 352.322,-54.3244 355.815,-54.1118 352.13,-51.1802 359.309,-53.8992 359.309,-53.8992\"/>\n",
+        "<text text-anchor=\"start\" x=\"194\" y=\"-81.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
         "</g>\n",
-        "<!-- 3&#45;&gt;3 -->\n",
-        "<g id=\"edge12\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M372.425,-41.0672C369.73,-51.4344 372.922,-61.5257 382,-61.5257 388.95,-61.5257 392.45,-55.6104 392.499,-48.1848\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"391.575,-41.0672 395.6,-47.6029 392.026,-44.538 392.477,-48.0088 392.477,-48.0088 392.477,-48.0088 392.026,-44.538 389.353,-48.4148 391.575,-41.0672 391.575,-41.0672\"/>\n",
-        "<text text-anchor=\"start\" x=\"361.5\" y=\"-80.3257\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
-        "<text text-anchor=\"start\" x=\"374\" y=\"-65.3257\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M123.544,-141.326C116.814,-136.124 108.789,-130.396 101,-126 94.4234,-122.288 86.9271,-118.93 80.0086,-116.147\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"73.3382,-113.564 81.0033,-113.154 76.602,-114.828 79.8659,-116.092 79.8659,-116.092 79.8659,-116.092 76.602,-114.828 78.7284,-119.029 73.3382,-113.564 73.3382,-113.564\"/>\n",
+        "<text text-anchor=\"start\" x=\"92\" y=\"-129.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g id=\"node4\" class=\"node\"><title>4</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"497\" cy=\"-120\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"497\" y=\"-116.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;4 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M163.293,-156.093C207.254,-158.09 311.209,-161.474 398,-154 424.498,-151.718 432.107,-153.364 457,-144 463.448,-141.575 470,-138.041 475.846,-134.428\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"481.874,-130.524 477.711,-136.973 478.936,-132.427 475.998,-134.329 475.998,-134.329 475.998,-134.329 478.936,-132.427 474.286,-131.685 481.874,-130.524 481.874,-130.524\"/>\n",
+        "<text text-anchor=\"start\" x=\"301.5\" y=\"-161.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 5 -->\n",
+        "<g id=\"node5\" class=\"node\"><title>5</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"258\" cy=\"-100\" rx=\"18\" ry=\"18\"/>\n",
+        "<ellipse fill=\"none\" stroke=\"black\" cx=\"258\" cy=\"-100\" rx=\"22\" ry=\"22\"/>\n",
+        "<text text-anchor=\"middle\" x=\"258\" y=\"-96.3\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;5 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;5</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M161.248,-145.794C180.404,-136.633 209.924,-122.514 231.122,-112.376\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"237.689,-109.236 232.733,-115.098 234.531,-110.746 231.374,-112.256 231.374,-112.256 231.374,-112.256 234.531,-110.746 230.015,-109.414 237.689,-109.236 237.689,-109.236\"/>\n",
+        "<text text-anchor=\"start\" x=\"181\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;4 -->\n",
+        "<g id=\"edge11\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M486.849,-135.167C483.772,-145.664 487.156,-156 497,-156 504.537,-156 508.287,-149.941 508.25,-142.39\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"507.151,-135.167 511.318,-141.614 507.678,-138.627 508.204,-142.087 508.204,-142.087 508.204,-142.087 507.678,-138.627 505.09,-142.561 507.151,-135.167 507.151,-135.167\"/>\n",
+        "<text text-anchor=\"start\" x=\"480\" y=\"-159.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;5 -->\n",
+        "<g id=\"edge12\" class=\"edge\"><title>4&#45;&gt;5</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M478.921,-118.559C438.561,-115.153 336.959,-106.579 287.26,-102.385\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"280.032,-101.775 287.272,-99.2247 283.52,-102.069 287.007,-102.364 287.007,-102.364 287.007,-102.364 283.52,-102.069 286.742,-105.502 280.032,-101.775 280.032,-101.775\"/>\n",
+        "<text text-anchor=\"start\" x=\"359\" y=\"-114.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;2 -->\n",
+        "<g id=\"edge14\" class=\"edge\"><title>5&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M235.839,-100.846C198.473,-102.341 121.02,-105.439 81.4399,-107.022\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"74.0519,-107.318 80.9204,-103.891 77.5491,-107.178 81.0463,-107.038 81.0463,-107.038 81.0463,-107.038 77.5491,-107.178 81.1722,-110.186 74.0519,-107.318 74.0519,-107.318\"/>\n",
+        "<text text-anchor=\"start\" x=\"134.5\" y=\"-108.8\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;4 -->\n",
+        "<g id=\"edge16\" class=\"edge\"><title>5&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M277.614,-110.332C283.933,-113.495 291.134,-116.734 298,-119 365.213,-141.186 386.713,-136.34 457,-128 461.98,-127.409 467.271,-126.51 472.295,-125.526\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"479.4,-124.048 473.188,-128.558 475.973,-124.761 472.546,-125.474 472.546,-125.474 472.546,-125.474 475.973,-124.761 471.905,-122.39 479.4,-124.048 479.4,-124.048\"/>\n",
+        "<text text-anchor=\"start\" x=\"359\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g id=\"node6\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"497\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
+        "<ellipse fill=\"none\" stroke=\"black\" cx=\"497\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
+        "<text text-anchor=\"middle\" x=\"497\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;1 -->\n",
+        "<g id=\"edge13\" class=\"edge\"><title>5&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M271.41,-82.1989C287.952,-60.2785 319.535,-24.315 357,-11 394.219,2.22762 440.463,-5.876 469.106,-13.4921\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"475.993,-15.4047 468.405,-16.5667 472.621,-14.4681 469.248,-13.5315 469.248,-13.5315 469.248,-13.5315 472.621,-14.4681 470.091,-10.4964 475.993,-15.4047 475.993,-15.4047\"/>\n",
+        "<text text-anchor=\"start\" x=\"357\" y=\"-14.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;3 -->\n",
+        "<g id=\"edge15\" class=\"edge\"><title>5&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M277.249,-88.6816C283.664,-84.9808 291.016,-81.0435 298,-78 315.966,-70.1711 337.187,-63.5611 353.033,-59.1079\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"359.904,-57.2169 353.991,-62.1114 356.53,-58.1456 353.155,-59.0743 353.155,-59.0743 353.155,-59.0743 356.53,-58.1456 352.319,-56.0372 359.904,-57.2169 359.904,-57.2169\"/>\n",
+        "<text text-anchor=\"start\" x=\"298\" y=\"-81.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M486.288,-41.3443C484.289,-52.0977 487.859,-62 497,-62 503.998,-62 507.732,-56.1954 508.2,-48.6485\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"507.712,-41.3443 511.321,-48.1187 507.945,-44.8365 508.178,-48.3288 508.178,-48.3288 508.178,-48.3288 507.945,-44.8365 505.035,-48.5388 507.712,-41.3443 507.712,-41.3443\"/>\n",
+        "<text text-anchor=\"start\" x=\"476.5\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;4 -->\n",
+        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M395.499,-55.8003C412.166,-59.1234 437.797,-65.8167 457,-78 466.106,-83.7772 474.491,-92.1901 481.135,-99.9716\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"485.858,-105.745 478.988,-102.322 483.642,-103.036 481.426,-100.327 481.426,-100.327 481.426,-100.327 483.642,-103.036 483.864,-98.3326 485.858,-105.745 485.858,-105.745\"/>\n",
+        "<text text-anchor=\"start\" x=\"418\" y=\"-81.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;1 -->\n",
+        "<g id=\"edge9\" class=\"edge\"><title>3&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M394.383,-46.4766C400.994,-43.9178 408.794,-41.0983 416,-39 432.988,-34.0535 452.392,-29.8946 467.836,-26.9286\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"475.071,-25.5702 468.773,-29.9579 471.631,-26.2161 468.191,-26.862 468.191,-26.862 468.191,-26.862 471.631,-26.2161 467.61,-23.766 475.071,-25.5702 475.071,-25.5702\"/>\n",
+        "<text text-anchor=\"start\" x=\"416\" y=\"-42.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2e4afe66f0> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d0523780> >"
        ]
       }
      ],
@@ -2321,7 +2735,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2e4afe6e70> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d05236f0> >"
        ]
       }
      ],
@@ -2391,7 +2805,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2e4afe6660> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d0523510> >"
        ]
       }
      ],