diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i
index 41e1f79f7..dff3566f8 100644
--- a/wrap/python/spot_impl.i
+++ b/wrap/python/spot_impl.i
@@ -116,6 +116,7 @@ namespace std {
 #include "tgba/taatgba.hh"
 #include "tgba/tgbaproduct.hh"
 
+#include "tgbaalgos/cleanacc.hh"
 #include "tgbaalgos/dotty.hh"
 #include "tgbaalgos/degen.hh"
 #include "tgbaalgos/dupexp.hh"
@@ -260,6 +261,7 @@ namespace spot {
 
 // Should come after the definition of tgba_digraph
 
+%include "tgbaalgos/cleanacc.hh"
 %include "tgbaalgos/degen.hh"
 %include "tgbaalgos/dotty.hh"
 %include "tgbaalgos/dupexp.hh"
diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am
index c01f198c0..477fdc79d 100644
--- a/wrap/python/tests/Makefile.am
+++ b/wrap/python/tests/Makefile.am
@@ -45,5 +45,6 @@ TESTS = \
   optionmap.py \
   parsetgba.py \
   piperead.ipynb \
+  randaut.ipynb \
   randltl.ipynb \
   setxor.py
diff --git a/wrap/python/tests/randaut.ipynb b/wrap/python/tests/randaut.ipynb
new file mode 100644
index 000000000..724c79d81
--- /dev/null
+++ b/wrap/python/tests/randaut.ipynb
@@ -0,0 +1,1968 @@
+{
+ "metadata": {
+  "name": "",
+  "signature": "sha256:f26e5cfdf72ab87cc41a6613deb2e29a0cca8a92678f062cd01b7513940e0424"
+ },
+ "nbformat": 3,
+ "nbformat_minor": 0,
+ "worksheets": [
+  {
+   "cells": [
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "import os\n",
+      "from IPython.display import display, HTML\n",
+      "# Note that Spot (loaded by the kernel) will store a copy of\n",
+      "# the environment variables the first time it reads them, so\n",
+      "# if you change those variables, the new values will be ignored\n",
+      "# until you restart the kernel.\n",
+      "os.environ['SPOT_DOTEXTRA'] = 'size=\"5,5\" node[style=filled,fillcolor=\"#ffffaa\"] edge[arrowhead=vee, arrowsize=.7]'\n",
+      "os.environ['SPOT_DOTDEFAULT'] = 'rbcf(Lato)'\n",
+      "import spot"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [],
+     "prompt_number": 1
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "txt = \"<TABLE><TR><TH>before</TH><TH>after</TH>\"\n",
+      "for a in spot.automata('randaut -H -S5 -A 3 -n10 2|'):\n",
+      "    txt += \"<TR><TD>{0}</TD><TD>{1}</TD></TR>\".format(a.show('.a').data, spot.cleanup_acceptance(a).show('.a').data)\n",
+      "txt += (\"</TABLE>\")\n",
+      "HTML(txt)"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "html": [
+        "<TABLE><TR><TH>before</TH><TH>after</TH><TR><TD><svg height=\"83pt\" viewBox=\"0.00 0.00 360.00 83.44\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.552571 0.552571) rotate(0) translate(4 147)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-147 647.5,-147 647.5,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"248.75\" y=\"-128.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"270.75\" y=\"-128.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"286.75\" y=\"-128.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"322.75\" y=\"-128.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"338.75\" y=\"-128.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"374.75\" y=\"-128.8\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"390.75\" y=\"-128.8\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-52\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-48.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,-52C2.79388,-52 17.1543,-52 30.6317,-52\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-52 30.9419,-55.1501 34.4419,-52 30.9419,-52.0001 30.9419,-52.0001 30.9419,-52.0001 34.4419,-52 30.9418,-48.8501 37.9419,-52 37.9419,-52\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>3</title>\n",
+        "<ellipse cx=\"196.5\" cy=\"-47\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"196.5\" y=\"-43.3\">3</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;3</title>\n",
+        "<path d=\"M71.7168,-42.4577C77.7499,-39.083 84.9605,-35.7041 92,-34 117.486,-27.8305 125.042,-30.286 151,-34 158.021,-35.0046 165.482,-36.858 172.247,-38.8569\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"179.262,-41.0496 171.641,-41.9676 175.921,-40.0053 172.581,-38.9611 172.581,-38.9611 172.581,-38.9611 175.921,-40.0053 173.521,-35.9545 179.262,-41.0496 179.262,-41.0496\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-37.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;0</title>\n",
+        "<path d=\"M178.173,-47.8311C169.941,-48.2126 159.964,-48.6555 151,-49 127.378,-49.9077 100.409,-50.7483 81.4345,-51.3073\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"74.3274,-51.5145 81.2325,-48.1617 77.8259,-51.4125 81.3244,-51.3104 81.3244,-51.3104 81.3244,-51.3104 77.8259,-51.4125 81.4162,-54.4591 74.3274,-51.5145 74.3274,-51.5145\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"94\" y=\"-53.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>2</title>\n",
+        "<ellipse cx=\"342.5\" cy=\"-76\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"342.5\" y=\"-72.3\">2</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;2</title>\n",
+        "<path d=\"M214.3,-50.3834C239.88,-55.5349 288.69,-65.3647 317.844,-71.236\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"324.807,-72.6381 317.322,-74.3441 321.375,-71.9471 317.944,-71.2561 317.944,-71.2561 317.944,-71.2561 321.375,-71.9471 318.566,-68.1681 324.807,-72.6381 324.807,-72.6381\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242\" y=\"-69.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>1</title>\n",
+        "<ellipse cx=\"614\" cy=\"-33\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"614\" y=\"-29.3\">1</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;0</title>\n",
+        "<path d=\"M597.589,-25.5437C591.583,-22.8653 584.574,-20.0124 578,-18 537.326,-5.54962 526.537,-2.55351e-15 484,-0 195.5,-0 195.5,-0 195.5,-0 148.071,-2.88658e-15 134.861,-5.69019 92,-26 86.3951,-28.6559 80.7926,-32.2752 75.7651,-35.9691\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"70.1618,-40.2865 73.7842,-33.5188 72.9343,-38.1503 75.7068,-36.0141 75.7068,-36.0141 75.7068,-36.0141 72.9343,-38.1503 77.6293,-38.5093 70.1618,-40.2865 70.1618,-40.2865\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"315\" y=\"-18.8\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"334.5\" y=\"-3.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
+        "<path d=\"M603.292,-47.7917C599.806,-58.4165 603.375,-69 614,-69 622.135,-69 626.134,-62.7961 625.997,-55.1197\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"624.708,-47.7917 629.023,-54.1403 625.314,-51.2388 625.92,-54.6859 625.92,-54.6859 625.92,-54.6859 625.314,-51.2388 622.818,-55.2315 624.708,-47.7917 624.708,-47.7917\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"584.5\" y=\"-87.8\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"606\" y=\"-72.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>4</title>\n",
+        "<ellipse cx=\"483\" cy=\"-76\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"483\" y=\"-72.3\">4</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;4</title>\n",
+        "<path d=\"M601.683,-46.226C595.39,-52.6763 587.018,-59.9085 578,-64 555.814,-74.0655 527.843,-76.5015 508.202,-76.7666\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"501.112,-76.7733 508.109,-73.6166 504.612,-76.7699 508.112,-76.7666 508.112,-76.7666 508.112,-76.7666 504.612,-76.7699 508.115,-79.9166 501.112,-76.7733 501.112,-76.7733\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"521\" y=\"-94.8\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"540.5\" y=\"-79.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;1</title>\n",
+        "<path d=\"M491.545,-59.6099C497.391,-49.0368 506.592,-36.1502 519,-30 541.019,-19.0855 569.641,-22.0424 589.489,-26.3324\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"596.376,-27.95 588.841,-29.4159 592.969,-27.1496 589.561,-26.3493 589.561,-26.3493 589.561,-26.3493 592.969,-27.1496 590.282,-23.2828 596.376,-27.95 596.376,-27.95\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"519\" y=\"-48.8\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"540.5\" y=\"-33.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;0</title>\n",
+        "<path d=\"M324.716,-80.2186C316.432,-82.089 306.255,-84.0735 297,-85 206.066,-94.1034 179.849,-94.1862 92,-69 87.4829,-67.7049 82.8363,-65.8585 78.4642,-63.8559\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"71.8778,-60.6373 79.55,-60.8805 75.0224,-62.174 78.167,-63.7107 78.167,-63.7107 78.167,-63.7107 75.0224,-62.174 76.784,-66.5408 71.8778,-60.6373 71.8778,-60.6373\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"169\" y=\"-108.8\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"188.5\" y=\"-93.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;4</title>\n",
+        "<path d=\"M360.761,-76C385.257,-76 430.207,-76 457.956,-76\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"464.956,-76 457.957,-79.1501 461.456,-76 457.956,-76.0001 457.956,-76.0001 457.956,-76.0001 461.456,-76 457.956,-72.8501 464.956,-76 464.956,-76\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388\" y=\"-79.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD><TD><svg height=\"72pt\" viewBox=\"0.00 0.00 360.00 72.39\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.552571 0.552571) rotate(0) translate(4 127)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-127 647.5,-127 647.5,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"318.75\" y=\"-107.8\">f</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-52\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-48.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,-52C2.79388,-52 17.1543,-52 30.6317,-52\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-52 30.9419,-55.1501 34.4419,-52 30.9419,-52.0001 30.9419,-52.0001 30.9419,-52.0001 34.4419,-52 30.9418,-48.8501 37.9419,-52 37.9419,-52\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>3</title>\n",
+        "<ellipse cx=\"196.5\" cy=\"-47\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"196.5\" y=\"-43.3\">3</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;3</title>\n",
+        "<path d=\"M71.7168,-42.4577C77.7499,-39.083 84.9605,-35.7041 92,-34 117.486,-27.8305 125.042,-30.286 151,-34 158.021,-35.0046 165.482,-36.858 172.247,-38.8569\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"179.262,-41.0496 171.641,-41.9676 175.921,-40.0053 172.581,-38.9611 172.581,-38.9611 172.581,-38.9611 175.921,-40.0053 173.521,-35.9545 179.262,-41.0496 179.262,-41.0496\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-37.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;0</title>\n",
+        "<path d=\"M178.173,-47.8311C169.941,-48.2126 159.964,-48.6555 151,-49 127.378,-49.9077 100.409,-50.7483 81.4345,-51.3073\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"74.3274,-51.5145 81.2325,-48.1617 77.8259,-51.4125 81.3244,-51.3104 81.3244,-51.3104 81.3244,-51.3104 77.8259,-51.4125 81.4162,-54.4591 74.3274,-51.5145 74.3274,-51.5145\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"94\" y=\"-53.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>2</title>\n",
+        "<ellipse cx=\"342.5\" cy=\"-61\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"342.5\" y=\"-57.3\">2</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;2</title>\n",
+        "<path d=\"M214.584,-48.661C240.025,-51.1344 287.987,-55.7973 317.111,-58.6288\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"324.438,-59.3412 317.166,-61.799 320.954,-59.0025 317.471,-58.6638 317.471,-58.6638 317.471,-58.6638 320.954,-59.0025 317.776,-55.5285 324.438,-59.3412 324.438,-59.3412\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242\" y=\"-59.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>1</title>\n",
+        "<ellipse cx=\"614\" cy=\"-33\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"614\" y=\"-29.3\">1</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;0</title>\n",
+        "<path d=\"M597.045,-26.1624C573.003,-16.4965 525.842,-0 484,-0 195.5,-0 195.5,-0 195.5,-0 148.071,-2.88658e-15 134.861,-5.69019 92,-26 86.3951,-28.6559 80.7926,-32.2752 75.7651,-35.9691\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"70.1618,-40.2865 73.7842,-33.5188 72.9343,-38.1503 75.7068,-36.0141 75.7068,-36.0141 75.7068,-36.0141 72.9343,-38.1503 77.6293,-38.5093 70.1618,-40.2865 70.1618,-40.2865\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"315\" y=\"-3.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
+        "<path d=\"M603.292,-47.7917C599.806,-58.4165 603.375,-69 614,-69 622.135,-69 626.134,-62.7961 625.997,-55.1197\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"624.708,-47.7917 629.023,-54.1403 625.314,-51.2388 625.92,-54.6859 625.92,-54.6859 625.92,-54.6859 625.314,-51.2388 622.818,-55.2315 624.708,-47.7917 624.708,-47.7917\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"584.5\" y=\"-72.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>4</title>\n",
+        "<ellipse cx=\"483\" cy=\"-61\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"483\" y=\"-57.3\">4</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;4</title>\n",
+        "<path d=\"M597.703,-41.2078C591.711,-44.0959 584.682,-47.0939 578,-49 554.955,-55.5738 527.701,-58.5517 508.49,-59.8976\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"501.293,-60.3518 508.081,-56.767 504.786,-60.1313 508.279,-59.9108 508.279,-59.9108 508.279,-59.9108 504.786,-60.1313 508.478,-63.0545 501.293,-60.3518 501.293,-60.3518\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"521\" y=\"-61.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;1</title>\n",
+        "<path d=\"M495.119,-47.2969C501.357,-40.7161 509.74,-33.5111 519,-30 541.743,-21.3762 569.848,-23.8048 589.372,-27.343\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"596.406,-28.7326 588.929,-30.4661 592.973,-28.0542 589.539,-27.3758 589.539,-27.3758 589.539,-27.3758 592.973,-28.0542 590.15,-24.2855 596.406,-28.7326 596.406,-28.7326\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"519\" y=\"-33.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;0</title>\n",
+        "<path d=\"M325.3,-67.4062C316.984,-70.3562 306.606,-73.5246 297,-75 206.906,-88.8377 180.122,-92.3007 92,-69 87.457,-67.7988 82.7987,-65.9951 78.4231,-64.0052\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"71.8372,-60.7845 79.5094,-61.03 74.9814,-62.3221 78.1256,-63.8597 78.1256,-63.8597 78.1256,-63.8597 74.9814,-62.3221 76.7417,-66.6895 71.8372,-60.7845 71.8372,-60.7845\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"169\" y=\"-88.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;4</title>\n",
+        "<path d=\"M360.761,-61C385.257,-61 430.207,-61 457.956,-61\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"464.956,-61 457.957,-64.1501 461.456,-61 457.956,-61.0001 457.956,-61.0001 457.956,-61.0001 461.456,-61 457.956,-57.8501 464.956,-61 464.956,-61\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388\" y=\"-64.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD></TR><TR><TD><svg height=\"98pt\" viewBox=\"0.00 0.00 360.00 97.76\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.57508 0.57508) rotate(0) translate(4 166)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-166 622,-166 622,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"236\" y=\"-147.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"258\" y=\"-147.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"274\" y=\"-147.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"310\" y=\"-147.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"326\" y=\"-147.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"362\" y=\"-147.8\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"378\" y=\"-147.8\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-20\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-16.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,-20C2.79388,-20 17.1543,-20 30.6317,-20\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-20 30.9419,-23.1501 34.4419,-20 30.9419,-20.0001 30.9419,-20.0001 30.9419,-20.0001 34.4419,-20 30.9418,-16.8501 37.9419,-20 37.9419,-20\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
+        "<ellipse cx=\"180\" cy=\"-47\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"180\" y=\"-43.3\">1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
+        "<path d=\"M73.7078,-23.6976C94.762,-28.3572 131.09,-36.3969 155.083,-41.7069\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"162.103,-43.2604 154.587,-44.8233 158.685,-42.5041 155.268,-41.7477 155.268,-41.7477 155.268,-41.7477 158.685,-42.5041 155.949,-38.6722 162.103,-43.2604 162.103,-43.2604\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-43.8\">p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
+        "<ellipse cx=\"313.5\" cy=\"-51\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"313.5\" y=\"-47.3\">3</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;3</title>\n",
+        "<path d=\"M198.191,-47.5229C221.129,-48.2207 261.881,-49.4603 288.022,-50.2554\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"295.304,-50.4769 288.212,-53.4126 291.806,-50.3705 288.308,-50.264 288.308,-50.264 288.308,-50.264 291.806,-50.3705 288.404,-47.1155 295.304,-50.4769 295.304,-50.4769\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"216\" y=\"-68.8\">p0 &amp; p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"234\" y=\"-53.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
+        "<ellipse cx=\"461.5\" cy=\"-112\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"461.5\" y=\"-108.3\">2</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>3-&gt;2</title>\n",
+        "<path d=\"M330.402,-57.6442C356.402,-68.5072 408.094,-90.1042 437.896,-102.556\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"444.617,-105.364 436.944,-105.572 441.388,-104.015 438.158,-102.665 438.158,-102.665 438.158,-102.665 441.388,-104.015 439.373,-99.7588 444.617,-105.364 444.617,-105.364\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"359\" y=\"-95.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
+        "<ellipse cx=\"600\" cy=\"-62\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"600\" y=\"-58.3\">4</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>2-&gt;4</title>\n",
+        "<path d=\"M479.589,-112.117C500.541,-111.61 536.637,-108.59 564,-95 570.956,-91.5452 577.477,-86.2454 582.961,-80.8971\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"588.078,-75.5991 585.481,-82.8227 585.646,-78.1168 583.215,-80.6345 583.215,-80.6345 583.215,-80.6345 585.646,-78.1168 580.949,-78.4463 588.078,-75.5991 588.078,-75.5991\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"509\" y=\"-127.8\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"528.5\" y=\"-112.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>4-&gt;0</title>\n",
+        "<path d=\"M585.581,-51.2004C562.111,-33.437 511.432,-7.10543e-15 462.5,-0 179,-0 179,-0 179,-0 144.572,-0 105.389,-7.85222 80.9277,-13.7165\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.8303,-15.4617 79.8756,-10.7313 77.2291,-14.6259 80.6278,-13.7901 80.6278,-13.7901 80.6278,-13.7901 77.2291,-14.6259 81.38,-16.849 73.8303,-15.4617 73.8303,-15.4617\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"286\" y=\"-3.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>4-&gt;3</title>\n",
+        "<path d=\"M581.804,-60.6615C560.504,-59.0552 523.099,-56.4034 491,-55 436.626,-52.6228 372.764,-51.6189 338.738,-51.2269\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"331.546,-51.1481 338.58,-48.0751 335.046,-51.1865 338.546,-51.2249 338.546,-51.2249 338.546,-51.2249 335.046,-51.1865 338.511,-54.3747 331.546,-51.1481 331.546,-51.1481\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"432\" y=\"-73.8\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"453.5\" y=\"-58.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>4-&gt;2</title>\n",
+        "<path d=\"M581.713,-62.1513C563.056,-62.8833 532.819,-65.7446 509,-76 498.486,-80.5269 488.261,-87.9944 480.09,-94.9581\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"474.783,-99.6564 477.936,-92.6579 477.403,-97.3365 480.024,-95.0165 480.024,-95.0165 480.024,-95.0165 477.403,-97.3365 482.112,-97.3752 474.783,-99.6564 474.783,-99.6564\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"510.5\" y=\"-79.8\">p0 &amp; p1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD><TD><svg height=\"86pt\" viewBox=\"0.00 0.00 360.00 85.69\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.57508 0.57508) rotate(0) translate(4 145)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-145 622,-145 622,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"306\" y=\"-125.8\">f</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-20\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-16.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,-20C2.79388,-20 17.1543,-20 30.6317,-20\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-20 30.9419,-23.1501 34.4419,-20 30.9419,-20.0001 30.9419,-20.0001 30.9419,-20.0001 34.4419,-20 30.9418,-16.8501 37.9419,-20 37.9419,-20\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
+        "<ellipse cx=\"180\" cy=\"-47\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"180\" y=\"-43.3\">1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
+        "<path d=\"M73.7078,-23.6976C94.762,-28.3572 131.09,-36.3969 155.083,-41.7069\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"162.103,-43.2604 154.587,-44.8233 158.685,-42.5041 155.268,-41.7477 155.268,-41.7477 155.268,-41.7477 158.685,-42.5041 155.949,-38.6722 162.103,-43.2604 162.103,-43.2604\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-43.8\">p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
+        "<ellipse cx=\"313.5\" cy=\"-51\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"313.5\" y=\"-47.3\">3</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;3</title>\n",
+        "<path d=\"M198.191,-47.5229C221.129,-48.2207 261.881,-49.4603 288.022,-50.2554\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"295.304,-50.4769 288.212,-53.4126 291.806,-50.3705 288.308,-50.264 288.308,-50.264 288.308,-50.264 291.806,-50.3705 288.404,-47.1155 295.304,-50.4769 295.304,-50.4769\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"216\" y=\"-53.8\">p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
+        "<ellipse cx=\"461.5\" cy=\"-97\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"461.5\" y=\"-93.3\">2</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>3-&gt;2</title>\n",
+        "<path d=\"M330.964,-56.1874C356.924,-64.3663 407.459,-80.2886 437.155,-89.6448\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"443.872,-91.761 436.249,-92.6618 440.534,-90.7092 437.195,-89.6574 437.195,-89.6574 437.195,-89.6574 440.534,-90.7092 438.142,-86.653 443.872,-91.761 443.872,-91.761\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"359\" y=\"-85.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
+        "<ellipse cx=\"600\" cy=\"-62\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"600\" y=\"-58.3\">4</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>2-&gt;4</title>\n",
+        "<path d=\"M479.411,-100.255C500.185,-103.462 536.1,-106.398 564,-95 571.19,-92.0626 577.775,-86.9043 583.246,-81.5264\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"588.326,-76.1493 585.808,-83.4008 585.923,-78.6934 583.519,-81.2374 583.519,-81.2374 583.519,-81.2374 585.923,-78.6934 581.229,-79.0741 588.326,-76.1493 588.326,-76.1493\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"509\" y=\"-106.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>4-&gt;0</title>\n",
+        "<path d=\"M585.581,-51.2004C562.111,-33.437 511.432,-7.10543e-15 462.5,-0 179,-0 179,-0 179,-0 144.572,-0 105.389,-7.85222 80.9277,-13.7165\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.8303,-15.4617 79.8756,-10.7313 77.2291,-14.6259 80.6278,-13.7901 80.6278,-13.7901 80.6278,-13.7901 77.2291,-14.6259 81.38,-16.849 73.8303,-15.4617 73.8303,-15.4617\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"286\" y=\"-3.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>4-&gt;3</title>\n",
+        "<path d=\"M581.804,-60.6615C560.504,-59.0552 523.099,-56.4034 491,-55 436.626,-52.6228 372.764,-51.6189 338.738,-51.2269\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"331.546,-51.1481 338.58,-48.0751 335.046,-51.1865 338.546,-51.2249 338.546,-51.2249 338.546,-51.2249 335.046,-51.1865 338.511,-54.3747 331.546,-51.1481 331.546,-51.1481\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"432\" y=\"-58.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>4-&gt;2</title>\n",
+        "<path d=\"M581.778,-63.2896C563.436,-64.9825 533.704,-68.6479 509,-76 500.68,-78.4761 491.915,-82.1339 484.266,-85.7058\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"477.6,-88.9256 482.533,-83.0447 480.751,-87.4034 483.903,-85.8812 483.903,-85.8812 483.903,-85.8812 480.751,-87.4034 485.273,-88.7177 477.6,-88.9256 477.6,-88.9256\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"510.5\" y=\"-79.8\">p0 &amp; p1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD></TR><TR><TD><svg height=\"157pt\" viewBox=\"0.00 0.00 360.00 156.65\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.56962 0.56962) rotate(0) translate(4 271)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-271 628,-271 628,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"239\" y=\"-252.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"261\" y=\"-252.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"277\" y=\"-252.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"313\" y=\"-252.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"329\" y=\"-252.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"365\" y=\"-252.8\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"381\" y=\"-252.8\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-154\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-150.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,-154C2.79388,-154 17.1543,-154 30.6317,-154\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-154 30.9419,-157.15 34.4419,-154 30.9419,-154 30.9419,-154 30.9419,-154 34.4419,-154 30.9418,-150.85 37.9419,-154 37.9419,-154\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>2</title>\n",
+        "<ellipse cx=\"183\" cy=\"-112\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"183\" y=\"-108.3\">2</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;2</title>\n",
+        "<path d=\"M73.3416,-148.509C95.1454,-141.183 133.883,-128.167 158.732,-119.818\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"165.654,-117.492 160.022,-122.708 162.337,-118.607 159.019,-119.722 159.019,-119.722 159.019,-119.722 162.337,-118.607 158.016,-116.736 165.654,-117.492 165.654,-117.492\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-144.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>4</title>\n",
+        "<ellipse cx=\"606\" cy=\"-140\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"606\" y=\"-136.3\">4</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;4</title>\n",
+        "<path d=\"M67.4339,-168.08C73.8286,-175.94 82.5786,-185.44 92,-192 127.491,-216.714 138.752,-229 182,-229 182,-229 182,-229 466.5,-229 515.351,-229 531.434,-221.984 570,-192 580.103,-184.145 588.309,-172.535 594.23,-162.276\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"597.617,-156.109 597.008,-163.761 595.932,-159.177 594.247,-162.244 594.247,-162.244 594.247,-162.244 595.932,-159.177 591.486,-160.728 597.617,-156.109 597.617,-156.109\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"292\" y=\"-232.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>1</title>\n",
+        "<ellipse cx=\"319.5\" cy=\"-85\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"319.5\" y=\"-81.3\">1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;1</title>\n",
+        "<path d=\"M200.676,-107.448C206.457,-105.941 212.993,-104.314 219,-103 244.66,-97.3877 274.315,-92.1869 294.529,-88.8338\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"301.524,-87.6847 295.128,-91.9278 298.071,-88.2521 294.617,-88.8195 294.617,-88.8195 294.617,-88.8195 298.071,-88.2521 294.106,-85.7111 301.524,-87.6847 301.524,-87.6847\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"220.5\" y=\"-106.8\">p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge11\"><title>4-&gt;0</title>\n",
+        "<path d=\"M589.183,-147.327C563.856,-158.369 512.378,-178 466.5,-178 182,-178 182,-178 182,-178 145.999,-178 105.194,-168.28 80.281,-161.211\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.3876,-159.208 80.9887,-158.137 76.7485,-160.185 80.1094,-161.162 80.1094,-161.162 80.1094,-161.162 76.7485,-160.185 79.2301,-164.186 73.3876,-159.208 73.3876,-159.208\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"292\" y=\"-181.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;2</title>\n",
+        "<path d=\"M587.628,-139.708C533.128,-138.642 360.72,-134.134 219,-118 215.417,-117.592 211.643,-117.057 207.954,-116.475\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"201.035,-115.317 208.459,-113.366 204.487,-115.895 207.939,-116.472 207.939,-116.472 207.939,-116.472 204.487,-115.895 207.419,-119.579 201.035,-115.317 201.035,-115.317\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"365\" y=\"-151.8\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"384.5\" y=\"-136.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;4</title>\n",
+        "<path d=\"M337.861,-84.7526C369.216,-84.6482 437.215,-85.9934 493,-98 528.599,-105.662 535.98,-113.014 570,-126 573.995,-127.525 578.231,-129.184 582.325,-130.808\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"589.012,-133.481 581.343,-133.808 585.762,-132.182 582.512,-130.883 582.512,-130.883 582.512,-130.883 585.762,-132.182 583.681,-127.958 589.012,-133.481 589.012,-133.481\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"438\" y=\"-115.8\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"449.5\" y=\"-101.8\">\u2776</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"465.5\" y=\"-101.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>3</title>\n",
+        "<ellipse cx=\"465.5\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"465.5\" y=\"-14.3\">3</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;3</title>\n",
+        "<path d=\"M331.075,-71.023C339.273,-61.1669 351.487,-48.4432 365,-41 388.616,-27.9921 419.285,-22.3223 440.295,-19.8627\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"447.296,-19.1198 440.667,-22.9909 443.815,-19.4891 440.335,-19.8585 440.335,-19.8585 440.335,-19.8585 443.815,-19.4891 440.003,-16.7261 447.296,-19.1198 447.296,-19.1198\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"365\" y=\"-59.8\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"384.5\" y=\"-44.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;0</title>\n",
+        "<path d=\"M447.706,-14.0926C406.913,-5.41768 300.01,12.3875 219,-18 154.911,-42.0402 98.2656,-103.174 72.2011,-134.638\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"67.6953,-140.153 69.6853,-132.739 69.9099,-137.442 72.1245,-134.732 72.1245,-134.732 72.1245,-134.732 69.9099,-137.442 74.5638,-136.725 67.6953,-140.153 67.6953,-140.153\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"219\" y=\"-36.8\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238.5\" y=\"-21.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;2</title>\n",
+        "<path d=\"M447.47,-17.1655C427.552,-16.4998 393.657,-16.3334 365,-21 294.533,-32.4752 278.846,-49.0682 219,-88 214.136,-91.1639 208.953,-94.6523 204.107,-97.9662\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"198.198,-102.033 202.179,-95.4694 201.081,-100.049 203.965,-98.0642 203.965,-98.0642 203.965,-98.0642 201.081,-100.049 205.751,-100.659 198.198,-102.033 198.198,-102.033\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"292\" y=\"-45.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;4</title>\n",
+        "<path d=\"M483.77,-19.8461C506.343,-23.1245 545.835,-31.9514 570,-55 586.822,-71.0447 595.832,-96.3502 600.474,-115.183\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"602.1,-122.304 597.471,-116.181 601.321,-118.892 600.542,-115.48 600.542,-115.48 600.542,-115.48 601.321,-118.892 603.613,-114.778 602.1,-122.304 602.1,-122.304\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"511\" y=\"-58.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD><TD><svg height=\"157pt\" viewBox=\"0.00 0.00 360.00 156.65\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.56962 0.56962) rotate(0) translate(4 271)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-271 628,-271 628,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"239\" y=\"-252.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"261\" y=\"-252.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"277\" y=\"-252.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"313\" y=\"-252.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"329\" y=\"-252.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"365\" y=\"-252.8\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"381\" y=\"-252.8\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-154\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-150.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,-154C2.79388,-154 17.1543,-154 30.6317,-154\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-154 30.9419,-157.15 34.4419,-154 30.9419,-154 30.9419,-154 30.9419,-154 34.4419,-154 30.9418,-150.85 37.9419,-154 37.9419,-154\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>2</title>\n",
+        "<ellipse cx=\"183\" cy=\"-112\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"183\" y=\"-108.3\">2</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;2</title>\n",
+        "<path d=\"M73.3416,-148.509C95.1454,-141.183 133.883,-128.167 158.732,-119.818\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"165.654,-117.492 160.022,-122.708 162.337,-118.607 159.019,-119.722 159.019,-119.722 159.019,-119.722 162.337,-118.607 158.016,-116.736 165.654,-117.492 165.654,-117.492\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-144.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>4</title>\n",
+        "<ellipse cx=\"606\" cy=\"-140\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"606\" y=\"-136.3\">4</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;4</title>\n",
+        "<path d=\"M67.4339,-168.08C73.8286,-175.94 82.5786,-185.44 92,-192 127.491,-216.714 138.752,-229 182,-229 182,-229 182,-229 466.5,-229 515.351,-229 531.434,-221.984 570,-192 580.103,-184.145 588.309,-172.535 594.23,-162.276\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"597.617,-156.109 597.008,-163.761 595.932,-159.177 594.247,-162.244 594.247,-162.244 594.247,-162.244 595.932,-159.177 591.486,-160.728 597.617,-156.109 597.617,-156.109\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"292\" y=\"-232.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>1</title>\n",
+        "<ellipse cx=\"319.5\" cy=\"-85\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"319.5\" y=\"-81.3\">1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;1</title>\n",
+        "<path d=\"M200.676,-107.448C206.457,-105.941 212.993,-104.314 219,-103 244.66,-97.3877 274.315,-92.1869 294.529,-88.8338\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"301.524,-87.6847 295.128,-91.9278 298.071,-88.2521 294.617,-88.8195 294.617,-88.8195 294.617,-88.8195 298.071,-88.2521 294.106,-85.7111 301.524,-87.6847 301.524,-87.6847\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"220.5\" y=\"-106.8\">p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge11\"><title>4-&gt;0</title>\n",
+        "<path d=\"M589.183,-147.327C563.856,-158.369 512.378,-178 466.5,-178 182,-178 182,-178 182,-178 145.999,-178 105.194,-168.28 80.281,-161.211\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.3876,-159.208 80.9887,-158.137 76.7485,-160.185 80.1094,-161.162 80.1094,-161.162 80.1094,-161.162 76.7485,-160.185 79.2301,-164.186 73.3876,-159.208 73.3876,-159.208\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"292\" y=\"-181.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;2</title>\n",
+        "<path d=\"M587.628,-139.708C533.128,-138.642 360.72,-134.134 219,-118 215.417,-117.592 211.643,-117.057 207.954,-116.475\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"201.035,-115.317 208.459,-113.366 204.487,-115.895 207.939,-116.472 207.939,-116.472 207.939,-116.472 204.487,-115.895 207.419,-119.579 201.035,-115.317 201.035,-115.317\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"365\" y=\"-151.8\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"384.5\" y=\"-136.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;4</title>\n",
+        "<path d=\"M337.861,-84.7526C369.216,-84.6482 437.215,-85.9934 493,-98 528.599,-105.662 535.98,-113.014 570,-126 573.995,-127.525 578.231,-129.184 582.325,-130.808\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"589.012,-133.481 581.343,-133.808 585.762,-132.182 582.512,-130.883 582.512,-130.883 582.512,-130.883 585.762,-132.182 583.681,-127.958 589.012,-133.481 589.012,-133.481\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"438\" y=\"-115.8\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"449.5\" y=\"-101.8\">\u2776</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"465.5\" y=\"-101.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>3</title>\n",
+        "<ellipse cx=\"465.5\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"465.5\" y=\"-14.3\">3</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;3</title>\n",
+        "<path d=\"M331.075,-71.023C339.273,-61.1669 351.487,-48.4432 365,-41 388.616,-27.9921 419.285,-22.3223 440.295,-19.8627\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"447.296,-19.1198 440.667,-22.9909 443.815,-19.4891 440.335,-19.8585 440.335,-19.8585 440.335,-19.8585 443.815,-19.4891 440.003,-16.7261 447.296,-19.1198 447.296,-19.1198\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"365\" y=\"-59.8\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"384.5\" y=\"-44.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;0</title>\n",
+        "<path d=\"M447.706,-14.0926C406.913,-5.41768 300.01,12.3875 219,-18 154.911,-42.0402 98.2656,-103.174 72.2011,-134.638\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"67.6953,-140.153 69.6853,-132.739 69.9099,-137.442 72.1245,-134.732 72.1245,-134.732 72.1245,-134.732 69.9099,-137.442 74.5638,-136.725 67.6953,-140.153 67.6953,-140.153\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"219\" y=\"-36.8\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238.5\" y=\"-21.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;2</title>\n",
+        "<path d=\"M447.47,-17.1655C427.552,-16.4998 393.657,-16.3334 365,-21 294.533,-32.4752 278.846,-49.0682 219,-88 214.136,-91.1639 208.953,-94.6523 204.107,-97.9662\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"198.198,-102.033 202.179,-95.4694 201.081,-100.049 203.965,-98.0642 203.965,-98.0642 203.965,-98.0642 201.081,-100.049 205.751,-100.659 198.198,-102.033 198.198,-102.033\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"292\" y=\"-45.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;4</title>\n",
+        "<path d=\"M483.77,-19.8461C506.343,-23.1245 545.835,-31.9514 570,-55 586.822,-71.0447 595.832,-96.3502 600.474,-115.183\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"602.1,-122.304 597.471,-116.181 601.321,-118.892 600.542,-115.48 600.542,-115.48 600.542,-115.48 601.321,-118.892 603.613,-114.778 602.1,-122.304 602.1,-122.304\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"511\" y=\"-58.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD></TR><TR><TD><svg height=\"101pt\" viewBox=\"0.00 0.00 360.00 101.23\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.56872 0.56872) rotate(0) translate(4 174)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-174 629,-174 629,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"239.5\" y=\"-155.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"261.5\" y=\"-155.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"277.5\" y=\"-155.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"313.5\" y=\"-155.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"329.5\" y=\"-155.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"365.5\" y=\"-155.8\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"381.5\" y=\"-155.8\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-91\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-87.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,-91C2.79388,-91 17.1543,-91 30.6317,-91\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-91 30.9419,-94.1501 34.4419,-91 30.9419,-91.0001 30.9419,-91.0001 30.9419,-91.0001 34.4419,-91 30.9418,-87.8501 37.9419,-91 37.9419,-91\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>4</title>\n",
+        "<ellipse cx=\"192.5\" cy=\"-121\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"192.5\" y=\"-117.3\">4</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;4</title>\n",
+        "<path d=\"M73.7626,-94.7389C97.3214,-99.9936 140.361,-109.593 167.364,-115.617\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"174.526,-117.214 167.008,-118.765 171.11,-116.452 167.694,-115.69 167.694,-115.69 167.694,-115.69 171.11,-116.452 168.38,-112.616 174.526,-117.214 174.526,-117.214\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-128.8\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111.5\" y=\"-113.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>2</title>\n",
+        "<ellipse cx=\"326\" cy=\"-86\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"326\" y=\"-82.3\">2</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>4-&gt;2</title>\n",
+        "<path d=\"M209.353,-114.23C217.755,-110.825 228.316,-106.832 238,-104 258.985,-97.8641 283.405,-93.0045 301.021,-89.889\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"308.125,-88.662 301.763,-92.9576 304.676,-89.2578 301.227,-89.8536 301.227,-89.8536 301.227,-89.8536 304.676,-89.2578 300.691,-86.7495 308.125,-88.662 308.125,-88.662\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238\" y=\"-122.8\">p0 &amp; p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"256\" y=\"-107.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>1</title>\n",
+        "<ellipse cx=\"464.5\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"464.5\" y=\"-14.3\">1</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;1</title>\n",
+        "<path d=\"M452.576,-31.667C447.807,-42.6562 451.781,-54 464.5,-54 474.437,-54 479.036,-47.0763 478.299,-38.8071\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"476.424,-31.667 481.248,-37.6375 477.313,-35.0522 478.202,-38.4375 478.202,-38.4375 478.202,-38.4375 477.313,-35.0522 475.155,-39.2375 476.424,-31.667 476.424,-31.667\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"437\" y=\"-57.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
+        "<ellipse cx=\"607\" cy=\"-105\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"607\" y=\"-101.3\">3</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;3</title>\n",
+        "<path d=\"M481.058,-25.391C502.124,-35.6554 540.583,-55.3111 571,-76 576.654,-79.8458 582.491,-84.4109 587.739,-88.7677\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"593.165,-93.3696 585.789,-91.2447 590.496,-91.1059 587.827,-88.8422 587.827,-88.8422 587.827,-88.8422 590.496,-91.1059 589.864,-86.4397 593.165,-93.3696 593.165,-93.3696\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"512\" y=\"-79.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;4</title>\n",
+        "<path d=\"M589.825,-110.976C583.972,-112.899 577.262,-114.833 571,-116 447.973,-138.926 415.081,-129.998 290,-134 266.901,-134.739 260.878,-137.273 238,-134 230.979,-132.995 223.518,-131.142 216.753,-129.143\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"209.738,-126.95 217.359,-126.032 213.079,-127.995 216.419,-129.039 216.419,-129.039 216.419,-129.039 213.079,-127.995 215.479,-132.045 209.738,-126.95 209.738,-126.95\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"362\" y=\"-135.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;2</title>\n",
+        "<path d=\"M588.803,-104.513C548.883,-103.275 446.863,-99.4809 362,-91 358.519,-90.6521 354.852,-90.2112 351.256,-89.7361\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"344.055,-88.7313 351.423,-86.5789 347.521,-89.215 350.988,-89.6986 350.988,-89.6986 350.988,-89.6986 347.521,-89.215 350.552,-92.8184 344.055,-88.7313 344.055,-88.7313\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"435\" y=\"-103.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>2-&gt;0</title>\n",
+        "<path d=\"M307.922,-84.5108C287.159,-82.7813 251.041,-80.0336 220,-79 195.569,-78.1865 189.407,-77.6482 165,-79 136.061,-80.6028 102.96,-84.6037 81.1142,-87.5471\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"74.1596,-88.4997 80.6673,-84.4288 77.6272,-88.0247 81.0948,-87.5496 81.0948,-87.5496 81.0948,-87.5496 77.6272,-88.0247 81.5224,-90.6705 74.1596,-88.4997 74.1596,-88.4997\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"165\" y=\"-82.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;1</title>\n",
+        "<path d=\"M340.504,-75.2966C346.82,-70.5718 354.573,-65.1593 362,-61 387.803,-46.5503 419.439,-33.8771 440.464,-26.1008\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"447.164,-23.6559 441.668,-29.0148 443.876,-24.8558 440.588,-26.0557 440.588,-26.0557 440.588,-26.0557 443.876,-24.8558 439.508,-23.0966 447.164,-23.6559 447.164,-23.6559\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"363.5\" y=\"-79.8\">p0 &amp; p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"381.5\" y=\"-64.8\">\u24ff</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD><TD><svg height=\"105pt\" viewBox=\"0.00 0.00 360.00 105.21\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.56872 0.56872) rotate(0) translate(4 181)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-181 629,-181 629,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"309.5\" y=\"-161.8\">f</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-106\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-102.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,-106C2.79388,-106 17.1543,-106 30.6317,-106\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-106 30.9419,-109.15 34.4419,-106 30.9419,-106 30.9419,-106 30.9419,-106 34.4419,-106 30.9418,-102.85 37.9419,-106 37.9419,-106\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>4</title>\n",
+        "<ellipse cx=\"192.5\" cy=\"-136\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"192.5\" y=\"-132.3\">4</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;4</title>\n",
+        "<path d=\"M73.7626,-109.739C97.3214,-114.994 140.361,-124.593 167.364,-130.617\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"174.526,-132.214 167.008,-133.765 171.11,-131.452 167.694,-130.69 167.694,-130.69 167.694,-130.69 171.11,-131.452 168.38,-127.616 174.526,-132.214 174.526,-132.214\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-128.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>2</title>\n",
+        "<ellipse cx=\"326\" cy=\"-93\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"326\" y=\"-89.3\">2</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>4-&gt;2</title>\n",
+        "<path d=\"M209.461,-129.572C217.893,-126.26 228.447,-122.247 238,-119 259.288,-111.764 283.859,-104.521 301.449,-99.5241\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"308.529,-97.5268 302.647,-102.459 305.161,-98.477 301.792,-99.4272 301.792,-99.4272 301.792,-99.4272 305.161,-98.477 300.937,-96.3955 308.529,-97.5268 308.529,-97.5268\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238\" y=\"-122.8\">p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>1</title>\n",
+        "<ellipse cx=\"464.5\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"464.5\" y=\"-14.3\">1</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;1</title>\n",
+        "<path d=\"M452.576,-31.667C447.807,-42.6562 451.781,-54 464.5,-54 474.437,-54 479.036,-47.0763 478.299,-38.8071\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"476.424,-31.667 481.248,-37.6375 477.313,-35.0522 478.202,-38.4375 478.202,-38.4375 478.202,-38.4375 477.313,-35.0522 475.155,-39.2375 476.424,-31.667 476.424,-31.667\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"437\" y=\"-57.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
+        "<ellipse cx=\"607\" cy=\"-105\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"607\" y=\"-101.3\">3</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;3</title>\n",
+        "<path d=\"M481.058,-25.391C502.124,-35.6554 540.583,-55.3111 571,-76 576.654,-79.8458 582.491,-84.4109 587.739,-88.7677\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"593.165,-93.3696 585.789,-91.2447 590.496,-91.1059 587.827,-88.8422 587.827,-88.8422 587.827,-88.8422 590.496,-91.1059 589.864,-86.4397 593.165,-93.3696 593.165,-93.3696\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"512\" y=\"-79.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;4</title>\n",
+        "<path d=\"M589.825,-110.976C583.972,-112.899 577.262,-114.833 571,-116 447.973,-138.926 415.033,-128.702 290,-134 265.356,-135.044 237.149,-135.549 217.623,-135.789\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"210.59,-135.869 217.554,-132.64 214.09,-135.829 217.59,-135.789 217.59,-135.789 217.59,-135.789 214.09,-135.829 217.625,-138.939 210.59,-135.869 210.59,-135.869\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"362\" y=\"-135.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;2</title>\n",
+        "<path d=\"M588.836,-104.262C541.105,-102.209 406.679,-96.427 351.304,-94.0453\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"344.033,-93.7326 351.162,-90.8864 347.529,-93.883 351.026,-94.0335 351.026,-94.0335 351.026,-94.0335 347.529,-93.883 350.891,-97.1806 344.033,-93.7326 344.033,-93.7326\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"435\" y=\"-102.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>2-&gt;0</title>\n",
+        "<path d=\"M307.697,-92.5174C278.328,-91.8305 216.857,-90.9653 165,-94 136.066,-95.6932 102.964,-99.676 81.1167,-102.59\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"74.1615,-103.533 80.675,-99.4714 77.6298,-103.063 81.0981,-102.593 81.0981,-102.593 81.0981,-102.593 77.6298,-103.063 81.5211,-105.714 74.1615,-103.533 74.1615,-103.533\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"165\" y=\"-97.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;1</title>\n",
+        "<path d=\"M342.129,-84.6871C366.42,-71.3406 414.205,-45.0852 442.02,-29.802\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"448.303,-26.3501 443.685,-32.4817 445.235,-28.0356 442.168,-29.721 442.168,-29.721 442.168,-29.721 445.235,-28.0356 440.651,-26.9603 448.303,-26.3501 448.303,-26.3501\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"363.5\" y=\"-76.8\">p0 &amp; p1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD></TR><TR><TD><svg height=\"76pt\" viewBox=\"0.00 0.00 360.00 75.85\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.583468 0.583468) rotate(0) translate(4 126)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-126 613,-126 613,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"231.5\" y=\"-107.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"253.5\" y=\"-107.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"269.5\" y=\"-107.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"305.5\" y=\"-107.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"321.5\" y=\"-107.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"357.5\" y=\"-107.8\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"373.5\" y=\"-107.8\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-14.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,-18C2.79388,-18 17.1543,-18 30.6317,-18\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-18 30.9419,-21.1501 34.4419,-18 30.9419,-18.0001 30.9419,-18.0001 30.9419,-18.0001 34.4419,-18 30.9418,-14.8501 37.9419,-18 37.9419,-18\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>4</title>\n",
+        "<ellipse cx=\"187\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"187\" y=\"-14.3\">4</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;4</title>\n",
+        "<path d=\"M74.1302,-18C96.5865,-18 136.116,-18 161.67,-18\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"168.799,-18 161.799,-21.1501 165.299,-18 161.799,-18.0001 161.799,-18.0001 161.799,-18.0001 165.299,-18 161.799,-14.8501 168.799,-18 168.799,-18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-21.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>2</title>\n",
+        "<ellipse cx=\"314\" cy=\"-48\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"314\" y=\"-44.3\">2</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>4-&gt;2</title>\n",
+        "<path d=\"M204.599,-21.9838C226.359,-27.2062 264.663,-36.3991 289.424,-42.3418\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"296.332,-43.9998 288.79,-45.4291 292.929,-43.1829 289.526,-42.3661 289.526,-42.3661 289.526,-42.3661 292.929,-43.1829 290.261,-39.303 296.332,-43.9998 296.332,-43.9998\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"223\" y=\"-42.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>1</title>\n",
+        "<ellipse cx=\"454.5\" cy=\"-43\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"454.5\" y=\"-39.3\">1</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
+        "<ellipse cx=\"591\" cy=\"-43\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"591\" y=\"-39.3\">3</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;3</title>\n",
+        "<path d=\"M472.535,-43C496.054,-43 538.61,-43 565.53,-43\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"572.679,-43 565.679,-46.1501 569.179,-43 565.679,-43.0001 565.679,-43.0001 565.679,-43.0001 569.179,-43 565.679,-39.8501 572.679,-43 572.679,-43\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"500\" y=\"-46.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>3-&gt;4</title>\n",
+        "<path d=\"M573.729,-37.9001C552.76,-31.5673 515.061,-20.9919 482,-16 382.867,-1.03176 262.783,-10.2098 212.255,-15.2929\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"205.035,-16.0395 211.674,-12.186 208.517,-15.6794 211.998,-15.3193 211.998,-15.3193 211.998,-15.3193 208.517,-15.6794 212.322,-18.4526 205.035,-16.0395 205.035,-16.0395\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"352\" y=\"-25.8\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"363.5\" y=\"-11.8\">\u24ff</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"379.5\" y=\"-11.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;2</title>\n",
+        "<path d=\"M575.577,-52.4726C569.469,-56.0402 562.126,-59.7702 555,-62 523.851,-71.7466 514.59,-68.2196 482,-70 423.379,-73.2025 406.758,-80.0077 350,-65 345.457,-63.7988 340.799,-61.9951 336.423,-60.0052\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"329.837,-56.7845 337.509,-57.03 332.981,-58.3221 336.126,-59.8597 336.126,-59.8597 336.126,-59.8597 332.981,-58.3221 334.742,-62.6895 329.837,-56.7845 329.837,-56.7845\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"427\" y=\"-76.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>2-&gt;1</title>\n",
+        "<path d=\"M332.261,-47.3769C356.757,-46.4925 401.707,-44.8698 429.456,-43.868\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"436.456,-43.6153 429.575,-47.0159 432.959,-43.7416 429.461,-43.8679 429.461,-43.8679 429.461,-43.8679 432.959,-43.7416 429.347,-40.72 436.456,-43.6153 436.456,-43.6153\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"350\" y=\"-49.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>2-&gt;2</title>\n",
+        "<path d=\"M303.627,-62.7917C300.249,-73.4165 303.707,-84 314,-84 321.881,-84 325.754,-77.7961 325.622,-70.1197\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"324.373,-62.7917 328.654,-69.1632 324.961,-66.242 325.549,-69.6923 325.549,-69.6923 325.549,-69.6923 324.961,-66.242 322.444,-70.2213 324.373,-62.7917 324.373,-62.7917\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"284.5\" y=\"-87.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD><TD><svg height=\"74pt\" viewBox=\"0.00 0.00 360.00 74.10\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.583468 0.583468) rotate(0) translate(4 123)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-123 613,-123 613,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"301.5\" y=\"-103.8\">f</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-14.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,-18C2.79388,-18 17.1543,-18 30.6317,-18\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-18 30.9419,-21.1501 34.4419,-18 30.9419,-18.0001 30.9419,-18.0001 30.9419,-18.0001 34.4419,-18 30.9418,-14.8501 37.9419,-18 37.9419,-18\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>4</title>\n",
+        "<ellipse cx=\"187\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"187\" y=\"-14.3\">4</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;4</title>\n",
+        "<path d=\"M74.1302,-18C96.5865,-18 136.116,-18 161.67,-18\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"168.799,-18 161.799,-21.1501 165.299,-18 161.799,-18.0001 161.799,-18.0001 161.799,-18.0001 165.299,-18 161.799,-14.8501 168.799,-18 168.799,-18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-21.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>2</title>\n",
+        "<ellipse cx=\"314\" cy=\"-45\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"314\" y=\"-41.3\">2</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>4-&gt;2</title>\n",
+        "<path d=\"M204.858,-21.6413C226.572,-26.3315 264.446,-34.5124 289.118,-39.8414\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"296.01,-41.3301 288.503,-42.9311 292.589,-40.5911 289.168,-39.8521 289.168,-39.8521 289.168,-39.8521 292.589,-40.5911 289.833,-36.7731 296.01,-41.3301 296.01,-41.3301\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"223\" y=\"-40.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>1</title>\n",
+        "<ellipse cx=\"454.5\" cy=\"-45\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"454.5\" y=\"-41.3\">1</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
+        "<ellipse cx=\"591\" cy=\"-45\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"591\" y=\"-41.3\">3</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;3</title>\n",
+        "<path d=\"M472.535,-45C496.054,-45 538.61,-45 565.53,-45\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"572.679,-45 565.679,-48.1501 569.179,-45 565.679,-45.0001 565.679,-45.0001 565.679,-45.0001 569.179,-45 565.679,-41.8501 572.679,-45 572.679,-45\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"500\" y=\"-48.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>3-&gt;4</title>\n",
+        "<path d=\"M573.768,-39.6142C552.84,-32.9794 515.185,-22.0853 482,-18 382.497,-5.75058 262.61,-12.298 212.195,-16.0093\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"204.992,-16.5555 211.733,-12.8852 208.482,-16.2908 211.972,-16.0261 211.972,-16.0261 211.972,-16.0261 208.482,-16.2908 212.21,-19.1671 204.992,-16.5555 204.992,-16.5555\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"352\" y=\"-15.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;2</title>\n",
+        "<path d=\"M575.577,-54.4726C569.469,-58.0402 562.126,-61.7702 555,-64 523.851,-73.7466 514.59,-70.2196 482,-72 423.313,-75.2061 406.142,-81.3933 350,-64 345.208,-62.5153 340.32,-60.3458 335.776,-57.9989\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"329.416,-54.4927 337.067,-55.1136 332.481,-56.1825 335.547,-57.8722 335.547,-57.8722 335.547,-57.8722 332.481,-56.1825 334.026,-60.6308 329.416,-54.4927 329.416,-54.4927\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"427\" y=\"-78.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>2-&gt;1</title>\n",
+        "<path d=\"M332.261,-45C356.757,-45 401.707,-45 429.456,-45\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"436.456,-45 429.457,-48.1501 432.956,-45 429.456,-45.0001 429.456,-45.0001 429.456,-45.0001 432.956,-45 429.456,-41.8501 436.456,-45 436.456,-45\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"350\" y=\"-48.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>2-&gt;2</title>\n",
+        "<path d=\"M303.627,-59.7917C300.249,-70.4165 303.707,-81 314,-81 321.881,-81 325.754,-74.7961 325.622,-67.1197\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"324.373,-59.7917 328.654,-66.1632 324.961,-63.242 325.549,-66.6923 325.549,-66.6923 325.549,-66.6923 324.961,-63.242 322.444,-67.2213 324.373,-59.7917 324.373,-59.7917\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"284.5\" y=\"-84.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD></TR><TR><TD><svg height=\"81pt\" viewBox=\"0.00 0.00 360.00 81.14\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.571429 0.571429) rotate(0) translate(4 138)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-138 626,-138 626,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238\" y=\"-119.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"260\" y=\"-119.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"276\" y=\"-119.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"312\" y=\"-119.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"328\" y=\"-119.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"364\" y=\"-119.8\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"380\" y=\"-119.8\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-19\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-15.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,-19C2.79388,-19 17.1543,-19 30.6317,-19\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-19 30.9419,-22.1501 34.4419,-19 30.9419,-19.0001 30.9419,-19.0001 30.9419,-19.0001 34.4419,-19 30.9418,-15.8501 37.9419,-19 37.9419,-19\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
+        "<ellipse cx=\"187\" cy=\"-46\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"187\" y=\"-42.3\">1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
+        "<path d=\"M73.8645,-22.5298C96.3661,-27.2394 136.343,-35.6068 161.987,-40.974\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"169.131,-42.4694 161.634,-44.1184 165.706,-41.7523 162.28,-41.0352 162.28,-41.0352 162.28,-41.0352 165.706,-41.7523 162.925,-37.952 169.131,-42.4694 169.131,-42.4694\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-56.8\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"113.5\" y=\"-41.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
+        "<ellipse cx=\"604\" cy=\"-46\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"604\" y=\"-42.3\">3</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;3</title>\n",
+        "<path d=\"M73.5838,-14.9706C98.0306,-9.39331 145.253,-0 186,-0 186,-0 186,-0 471.5,-0 512.352,-0 556.542,-20.0249 581.881,-33.6502\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"588.206,-37.1307 580.555,-36.5159 585.14,-35.4434 582.073,-33.7561 582.073,-33.7561 582.073,-33.7561 585.14,-35.4434 583.592,-30.9963 588.206,-37.1307 588.206,-37.1307\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"300\" y=\"-18.8\">p0 &amp; p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"318\" y=\"-3.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
+        "<ellipse cx=\"326\" cy=\"-79\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"326\" y=\"-75.3\">2</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;2</title>\n",
+        "<path d=\"M201.062,-57.3423C207.289,-62.0935 215.094,-67.163 223,-70 248.445,-79.131 279.652,-80.5897 300.797,-80.2692\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"307.831,-80.0913 300.913,-83.4174 304.332,-80.1798 300.833,-80.2684 300.833,-80.2684 300.833,-80.2684 304.332,-80.1798 300.754,-77.1194 307.831,-80.0913 307.831,-80.0913\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"223\" y=\"-97.8\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"244.5\" y=\"-82.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;2</title>\n",
+        "<path d=\"M592.186,-59.5917C585.916,-66.4091 577.41,-74.0406 568,-78 493.84,-109.203 395.111,-94.094 350.567,-84.6419\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"343.645,-83.1248 351.157,-81.5465 347.064,-83.8741 350.483,-84.6235 350.483,-84.6235 350.483,-84.6235 347.064,-83.8741 349.809,-87.7004 343.645,-83.1248 343.645,-83.1248\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"443\" y=\"-99.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>2-&gt;1</title>\n",
+        "<path d=\"M315.253,-64.4263C307.566,-54.3397 295.85,-41.7371 282,-36 259.043,-26.4911 230.361,-31.7278 210.756,-37.5942\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"203.971,-39.7579 209.683,-34.63 207.305,-38.6945 210.64,-37.6311 210.64,-37.6311 210.64,-37.6311 207.305,-38.6945 211.597,-40.6322 203.971,-39.7579 203.971,-39.7579\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"225\" y=\"-54.8\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"244.5\" y=\"-39.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
+        "<ellipse cx=\"470.5\" cy=\"-46\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"470.5\" y=\"-42.3\">4</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;4</title>\n",
+        "<path d=\"M342.021,-70.1219C350.058,-65.7747 360.279,-60.8708 370,-58 394.968,-50.6263 424.74,-47.7728 445.171,-46.6745\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"452.249,-46.3441 445.404,-49.8171 448.753,-46.5074 445.257,-46.6706 445.257,-46.6706 445.257,-46.6706 448.753,-46.5074 445.11,-43.524 452.249,-46.3441 452.249,-46.3441\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"370\" y=\"-75.8\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"381.5\" y=\"-61.8\">\u24ff</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"397.5\" y=\"-61.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>4-&gt;3</title>\n",
+        "<path d=\"M488.691,-46C511.629,-46 552.381,-46 578.522,-46\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"585.804,-46 578.804,-49.1501 582.304,-46 578.804,-46.0001 578.804,-46.0001 578.804,-46.0001 582.304,-46 578.804,-42.8501 585.804,-46 585.804,-46\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"516\" y=\"-63.8\">p0 &amp; p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"526\" y=\"-49.8\">\u24ff</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"542\" y=\"-49.8\">\u2776</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD><TD><svg height=\"81pt\" viewBox=\"0.00 0.00 360.00 81.14\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.571429 0.571429) rotate(0) translate(4 138)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-138 626,-138 626,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238\" y=\"-119.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"260\" y=\"-119.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"276\" y=\"-119.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"312\" y=\"-119.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"328\" y=\"-119.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"364\" y=\"-119.8\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"380\" y=\"-119.8\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-19\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-15.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,-19C2.79388,-19 17.1543,-19 30.6317,-19\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-19 30.9419,-22.1501 34.4419,-19 30.9419,-19.0001 30.9419,-19.0001 30.9419,-19.0001 34.4419,-19 30.9418,-15.8501 37.9419,-19 37.9419,-19\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
+        "<ellipse cx=\"187\" cy=\"-46\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"187\" y=\"-42.3\">1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
+        "<path d=\"M73.8645,-22.5298C96.3661,-27.2394 136.343,-35.6068 161.987,-40.974\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"169.131,-42.4694 161.634,-44.1184 165.706,-41.7523 162.28,-41.0352 162.28,-41.0352 162.28,-41.0352 165.706,-41.7523 162.925,-37.952 169.131,-42.4694 169.131,-42.4694\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-56.8\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"113.5\" y=\"-41.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
+        "<ellipse cx=\"604\" cy=\"-46\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"604\" y=\"-42.3\">3</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;3</title>\n",
+        "<path d=\"M73.5838,-14.9706C98.0306,-9.39331 145.253,-0 186,-0 186,-0 186,-0 471.5,-0 512.352,-0 556.542,-20.0249 581.881,-33.6502\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"588.206,-37.1307 580.555,-36.5159 585.14,-35.4434 582.073,-33.7561 582.073,-33.7561 582.073,-33.7561 585.14,-35.4434 583.592,-30.9963 588.206,-37.1307 588.206,-37.1307\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"300\" y=\"-18.8\">p0 &amp; p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"318\" y=\"-3.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
+        "<ellipse cx=\"326\" cy=\"-79\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"326\" y=\"-75.3\">2</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;2</title>\n",
+        "<path d=\"M201.062,-57.3423C207.289,-62.0935 215.094,-67.163 223,-70 248.445,-79.131 279.652,-80.5897 300.797,-80.2692\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"307.831,-80.0913 300.913,-83.4174 304.332,-80.1798 300.833,-80.2684 300.833,-80.2684 300.833,-80.2684 304.332,-80.1798 300.754,-77.1194 307.831,-80.0913 307.831,-80.0913\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"223\" y=\"-97.8\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"244.5\" y=\"-82.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;2</title>\n",
+        "<path d=\"M592.186,-59.5917C585.916,-66.4091 577.41,-74.0406 568,-78 493.84,-109.203 395.111,-94.094 350.567,-84.6419\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"343.645,-83.1248 351.157,-81.5465 347.064,-83.8741 350.483,-84.6235 350.483,-84.6235 350.483,-84.6235 347.064,-83.8741 349.809,-87.7004 343.645,-83.1248 343.645,-83.1248\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"443\" y=\"-99.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>2-&gt;1</title>\n",
+        "<path d=\"M315.253,-64.4263C307.566,-54.3397 295.85,-41.7371 282,-36 259.043,-26.4911 230.361,-31.7278 210.756,-37.5942\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"203.971,-39.7579 209.683,-34.63 207.305,-38.6945 210.64,-37.6311 210.64,-37.6311 210.64,-37.6311 207.305,-38.6945 211.597,-40.6322 203.971,-39.7579 203.971,-39.7579\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"225\" y=\"-54.8\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"244.5\" y=\"-39.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
+        "<ellipse cx=\"470.5\" cy=\"-46\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"470.5\" y=\"-42.3\">4</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;4</title>\n",
+        "<path d=\"M342.021,-70.1219C350.058,-65.7747 360.279,-60.8708 370,-58 394.968,-50.6263 424.74,-47.7728 445.171,-46.6745\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"452.249,-46.3441 445.404,-49.8171 448.753,-46.5074 445.257,-46.6706 445.257,-46.6706 445.257,-46.6706 448.753,-46.5074 445.11,-43.524 452.249,-46.3441 452.249,-46.3441\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"370\" y=\"-75.8\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"381.5\" y=\"-61.8\">\u24ff</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"397.5\" y=\"-61.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>4-&gt;3</title>\n",
+        "<path d=\"M488.691,-46C511.629,-46 552.381,-46 578.522,-46\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"585.804,-46 578.804,-49.1501 582.304,-46 578.804,-46.0001 578.804,-46.0001 578.804,-46.0001 582.304,-46 578.804,-42.8501 585.804,-46 585.804,-46\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"516\" y=\"-63.8\">p0 &amp; p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"526\" y=\"-49.8\">\u24ff</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"542\" y=\"-49.8\">\u2776</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD></TR><TR><TD><svg height=\"128pt\" viewBox=\"0.00 0.00 360.00 128.47\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.570975 0.570975) rotate(0) translate(4 221)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-221 626.5,-221 626.5,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238.25\" y=\"-202.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"260.25\" y=\"-202.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"276.25\" y=\"-202.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"312.25\" y=\"-202.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"328.25\" y=\"-202.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"364.25\" y=\"-202.8\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"380.25\" y=\"-202.8\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-51\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-47.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,-51C2.79388,-51 17.1543,-51 30.6317,-51\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-51 30.9419,-54.1501 34.4419,-51 30.9419,-51.0001 30.9419,-51.0001 30.9419,-51.0001 34.4419,-51 30.9418,-47.8501 37.9419,-51 37.9419,-51\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>2</title>\n",
+        "<ellipse cx=\"183\" cy=\"-89\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"183\" y=\"-85.3\">2</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;2</title>\n",
+        "<path d=\"M72.4221,-58.8127C78.429,-61.6524 85.4361,-64.7204 92,-67 113.999,-74.6402 139.901,-80.6752 158.256,-84.4769\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"165.139,-85.8714 157.653,-87.5688 161.709,-85.1764 158.278,-84.4815 158.278,-84.4815 158.278,-84.4815 161.709,-85.1764 158.904,-81.3942 165.139,-85.8714 165.139,-85.8714\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"93.5\" y=\"-99.8\">p0 &amp; p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111.5\" y=\"-84.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>2-&gt;0</title>\n",
+        "<path d=\"M173.489,-73.5186C167.444,-64.2391 158.388,-53.2518 147,-48 126.07,-38.3479 99.3976,-40.808 80.5388,-44.6307\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.4734,-46.2 79.6239,-41.6071 76.8901,-45.4411 80.3069,-44.6822 80.3069,-44.6822 80.3069,-44.6822 76.8901,-45.4411 80.9899,-47.7572 73.4734,-46.2 73.4734,-46.2\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-51.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>4</title>\n",
+        "<ellipse cx=\"595\" cy=\"-63\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"595\" y=\"-59.3\">4</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;4</title>\n",
+        "<path d=\"M187.772,-106.613C192.311,-123.53 201.599,-148.585 219,-163 264.644,-200.811 292.447,-191.198 351,-182 446.946,-166.929 481.389,-173.389 559,-115 569.226,-107.307 577.442,-95.709 583.338,-85.4173\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"586.706,-79.2246 586.129,-86.879 585.034,-82.2993 583.361,-85.374 583.361,-85.374 583.361,-85.374 585.034,-82.2993 580.594,-83.869 586.706,-79.2246 586.706,-79.2246\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"372.5\" y=\"-182.8\">p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>3</title>\n",
+        "<ellipse cx=\"321.5\" cy=\"-155\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"321.5\" y=\"-151.3\">3</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;3</title>\n",
+        "<path d=\"M199.393,-96.4427C223.561,-108.128 270.512,-130.83 298.322,-144.276\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"304.954,-147.483 297.281,-147.272 301.803,-145.96 298.652,-144.436 298.652,-144.436 298.652,-144.436 301.803,-145.96 300.023,-141.6 304.954,-147.483 304.954,-147.483\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"219\" y=\"-148.8\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"230.5\" y=\"-134.8\">\u2776</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"246.5\" y=\"-134.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>1</title>\n",
+        "<ellipse cx=\"464\" cy=\"-89\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"464\" y=\"-85.3\">1</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;2</title>\n",
+        "<path d=\"M445.836,-89C398.105,-89 263.679,-89 208.304,-89\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"201.033,-89 208.033,-85.8501 204.533,-89 208.033,-89.0001 208.033,-89.0001 208.033,-89.0001 204.533,-89 208.033,-92.1501 201.033,-89 201.033,-89\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"294\" y=\"-107.8\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"313.5\" y=\"-92.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;4</title>\n",
+        "<path d=\"M481.864,-85.601C504.366,-81.0658 544.343,-73.0083 569.987,-67.8398\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"577.131,-66.3999 570.892,-70.8709 573.7,-67.0914 570.269,-67.783 570.269,-67.783 570.269,-67.783 573.7,-67.0914 569.647,-64.6951 577.131,-66.3999 577.131,-66.3999\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"500\" y=\"-99.8\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"521.5\" y=\"-84.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;0</title>\n",
+        "<path d=\"M580.738,-51.4448C558.451,-33.2573 511.359,-0 465,-0 182,-0 182,-0 182,-0 142.627,-0 101.102,-21.9608 77.2033,-37.0609\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"71.2329,-40.924 75.3986,-34.4766 74.1714,-39.0227 77.1099,-37.1213 77.1099,-37.1213 77.1099,-37.1213 74.1714,-39.0227 78.8211,-39.7659 71.2329,-40.924 71.2329,-40.924\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"292\" y=\"-3.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge11\"><title>4-&gt;2</title>\n",
+        "<path d=\"M576.563,-61.8829C546.333,-60.0082 482.228,-56.3059 428,-55 401.785,-54.3687 395.114,-52.6203 369,-55 310.402,-60.34 242.644,-75.0063 207.649,-83.2251\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"200.694,-84.8753 206.777,-80.1943 204.099,-84.0673 207.505,-83.2592 207.505,-83.2592 207.505,-83.2592 204.099,-84.0673 208.232,-86.3241 200.694,-84.8753 200.694,-84.8753\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"369\" y=\"-73.8\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"390.5\" y=\"-58.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>4-&gt;4</title>\n",
+        "<path d=\"M584.292,-77.7917C580.806,-88.4165 584.375,-99 595,-99 603.135,-99 607.134,-92.7961 606.997,-85.1197\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"605.708,-77.7917 610.023,-84.1403 606.314,-81.2388 606.92,-84.6859 606.92,-84.6859 606.92,-84.6859 606.314,-81.2388 603.818,-85.2315 605.708,-77.7917 605.708,-77.7917\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"567.5\" y=\"-102.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;1</title>\n",
+        "<path d=\"M338.073,-147.685C363.075,-135.94 412.26,-112.835 440.891,-99.3857\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"447.357,-96.3481 442.361,-102.175 444.19,-97.8362 441.022,-99.3244 441.022,-99.3244 441.022,-99.3244 444.19,-97.8362 439.682,-96.4733 447.357,-96.3481 447.357,-96.3481\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"371\" y=\"-134.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD><TD><svg height=\"128pt\" viewBox=\"0.00 0.00 360.00 128.47\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.570975 0.570975) rotate(0) translate(4 221)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-221 626.5,-221 626.5,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238.25\" y=\"-202.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"260.25\" y=\"-202.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"276.25\" y=\"-202.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"312.25\" y=\"-202.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"328.25\" y=\"-202.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"364.25\" y=\"-202.8\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"380.25\" y=\"-202.8\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-51\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-47.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,-51C2.79388,-51 17.1543,-51 30.6317,-51\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-51 30.9419,-54.1501 34.4419,-51 30.9419,-51.0001 30.9419,-51.0001 30.9419,-51.0001 34.4419,-51 30.9418,-47.8501 37.9419,-51 37.9419,-51\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>2</title>\n",
+        "<ellipse cx=\"183\" cy=\"-89\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"183\" y=\"-85.3\">2</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;2</title>\n",
+        "<path d=\"M72.4221,-58.8127C78.429,-61.6524 85.4361,-64.7204 92,-67 113.999,-74.6402 139.901,-80.6752 158.256,-84.4769\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"165.139,-85.8714 157.653,-87.5688 161.709,-85.1764 158.278,-84.4815 158.278,-84.4815 158.278,-84.4815 161.709,-85.1764 158.904,-81.3942 165.139,-85.8714 165.139,-85.8714\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"93.5\" y=\"-99.8\">p0 &amp; p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111.5\" y=\"-84.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>2-&gt;0</title>\n",
+        "<path d=\"M173.489,-73.5186C167.444,-64.2391 158.388,-53.2518 147,-48 126.07,-38.3479 99.3976,-40.808 80.5388,-44.6307\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.4734,-46.2 79.6239,-41.6071 76.8901,-45.4411 80.3069,-44.6822 80.3069,-44.6822 80.3069,-44.6822 76.8901,-45.4411 80.9899,-47.7572 73.4734,-46.2 73.4734,-46.2\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-51.8\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>4</title>\n",
+        "<ellipse cx=\"595\" cy=\"-63\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"595\" y=\"-59.3\">4</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;4</title>\n",
+        "<path d=\"M187.772,-106.613C192.311,-123.53 201.599,-148.585 219,-163 264.644,-200.811 292.447,-191.198 351,-182 446.946,-166.929 481.389,-173.389 559,-115 569.226,-107.307 577.442,-95.709 583.338,-85.4173\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"586.706,-79.2246 586.129,-86.879 585.034,-82.2993 583.361,-85.374 583.361,-85.374 583.361,-85.374 585.034,-82.2993 580.594,-83.869 586.706,-79.2246 586.706,-79.2246\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"372.5\" y=\"-182.8\">p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>3</title>\n",
+        "<ellipse cx=\"321.5\" cy=\"-155\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"321.5\" y=\"-151.3\">3</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;3</title>\n",
+        "<path d=\"M199.393,-96.4427C223.561,-108.128 270.512,-130.83 298.322,-144.276\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"304.954,-147.483 297.281,-147.272 301.803,-145.96 298.652,-144.436 298.652,-144.436 298.652,-144.436 301.803,-145.96 300.023,-141.6 304.954,-147.483 304.954,-147.483\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"219\" y=\"-148.8\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"230.5\" y=\"-134.8\">\u2776</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"246.5\" y=\"-134.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>1</title>\n",
+        "<ellipse cx=\"464\" cy=\"-89\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"464\" y=\"-85.3\">1</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;2</title>\n",
+        "<path d=\"M445.836,-89C398.105,-89 263.679,-89 208.304,-89\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"201.033,-89 208.033,-85.8501 204.533,-89 208.033,-89.0001 208.033,-89.0001 208.033,-89.0001 204.533,-89 208.033,-92.1501 201.033,-89 201.033,-89\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"294\" y=\"-107.8\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"313.5\" y=\"-92.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;4</title>\n",
+        "<path d=\"M481.864,-85.601C504.366,-81.0658 544.343,-73.0083 569.987,-67.8398\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"577.131,-66.3999 570.892,-70.8709 573.7,-67.0914 570.269,-67.783 570.269,-67.783 570.269,-67.783 573.7,-67.0914 569.647,-64.6951 577.131,-66.3999 577.131,-66.3999\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"500\" y=\"-99.8\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"521.5\" y=\"-84.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;0</title>\n",
+        "<path d=\"M580.738,-51.4448C558.451,-33.2573 511.359,-0 465,-0 182,-0 182,-0 182,-0 142.627,-0 101.102,-21.9608 77.2033,-37.0609\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"71.2329,-40.924 75.3986,-34.4766 74.1714,-39.0227 77.1099,-37.1213 77.1099,-37.1213 77.1099,-37.1213 74.1714,-39.0227 78.8211,-39.7659 71.2329,-40.924 71.2329,-40.924\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"292\" y=\"-3.8\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge11\"><title>4-&gt;2</title>\n",
+        "<path d=\"M576.563,-61.8829C546.333,-60.0082 482.228,-56.3059 428,-55 401.785,-54.3687 395.114,-52.6203 369,-55 310.402,-60.34 242.644,-75.0063 207.649,-83.2251\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"200.694,-84.8753 206.777,-80.1943 204.099,-84.0673 207.505,-83.2592 207.505,-83.2592 207.505,-83.2592 204.099,-84.0673 208.232,-86.3241 200.694,-84.8753 200.694,-84.8753\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"369\" y=\"-73.8\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"390.5\" y=\"-58.8\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>4-&gt;4</title>\n",
+        "<path d=\"M584.292,-77.7917C580.806,-88.4165 584.375,-99 595,-99 603.135,-99 607.134,-92.7961 606.997,-85.1197\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"605.708,-77.7917 610.023,-84.1403 606.314,-81.2388 606.92,-84.6859 606.92,-84.6859 606.92,-84.6859 606.314,-81.2388 603.818,-85.2315 605.708,-77.7917 605.708,-77.7917\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"567.5\" y=\"-102.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;1</title>\n",
+        "<path d=\"M338.073,-147.685C363.075,-135.94 412.26,-112.835 440.891,-99.3857\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"447.357,-96.3481 442.361,-102.175 444.19,-97.8362 441.022,-99.3244 441.022,-99.3244 441.022,-99.3244 444.19,-97.8362 439.682,-96.4733 447.357,-96.3481 447.357,-96.3481\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"371\" y=\"-134.8\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD></TR><TR><TD><svg height=\"150pt\" viewBox=\"0.00 0.00 360.00 149.80\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.745342 0.745342) rotate(0) translate(4 196.976)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-196.976 479,-196.976 479,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"164.5\" y=\"-178.776\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"186.5\" y=\"-178.776\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"202.5\" y=\"-178.776\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238.5\" y=\"-178.776\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"254.5\" y=\"-178.776\">)&amp;Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"290.5\" y=\"-178.776\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"306.5\" y=\"-178.776\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-46.9763\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-43.2763\">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,-46.9763C2.79388,-46.9763 17.1543,-46.9763 30.6317,-46.9763\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-46.9763 30.9419,-50.1264 34.4419,-46.9763 30.9419,-46.9764 30.9419,-46.9764 30.9419,-46.9764 34.4419,-46.9763 30.9418,-43.8264 37.9419,-46.9763 37.9419,-46.9763\" 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,-64.0136C48.3189,-73.8342 50.4453,-82.9763 56,-82.9763 60.166,-82.9763 62.4036,-77.8339 62.7128,-71.1196\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"62.3792,-64.0136 65.8541,-70.8581 62.5434,-67.5097 62.7076,-71.0059 62.7076,-71.0059 62.7076,-71.0059 62.5434,-67.5097 59.561,-71.1537 62.3792,-64.0136 62.3792,-64.0136\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"26.5\" y=\"-101.776\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"48\" y=\"-86.7763\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
+        "<ellipse cx=\"189.5\" cy=\"-89.9763\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"189.5\" y=\"-86.2763\">1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
+        "<path d=\"M73.3887,-52.3353C96.5205,-59.8993 138.861,-73.7446 165.24,-82.3705\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"171.905,-84.5497 164.272,-85.368 168.578,-83.4619 165.251,-82.374 165.251,-82.374 165.251,-82.374 168.578,-83.4619 166.231,-79.38 171.905,-84.5497 171.905,-84.5497\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-92.7763\">p0 &amp; p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"110\" y=\"-77.7763\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
+        "<ellipse cx=\"326\" cy=\"-103.976\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"326\" y=\"-100.276\">3</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;3</title>\n",
+        "<path d=\"M62.8051,-63.6491C68.3468,-77.3067 77.9479,-96.2306 92,-107.976 143.772,-151.251 168.511,-147.475 235,-158.976 259.087,-163.143 268.572,-170.739 290,-158.976 302.275,-152.238 310.86,-139.167 316.455,-127.458\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"319.408,-120.78 319.458,-128.456 317.993,-123.98 316.577,-127.181 316.577,-127.181 316.577,-127.181 317.993,-123.98 313.696,-125.907 319.408,-120.78 319.408,-120.78\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"162\" y=\"-158.776\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;3</title>\n",
+        "<path d=\"M203.361,-102.129C211.682,-109.128 223.142,-117.253 235,-120.976 258.322,-128.299 266.178,-126.456 290,-120.976 294.58,-119.923 299.255,-118.187 303.635,-116.217\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"310.22,-112.993 305.318,-118.9 307.077,-114.532 303.933,-116.071 303.933,-116.071 303.933,-116.071 307.077,-114.532 302.548,-113.242 310.22,-112.993 310.22,-112.993\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"235\" y=\"-143.776\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"254.5\" y=\"-128.776\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>4</title>\n",
+        "<ellipse cx=\"326\" cy=\"-41.9763\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"326\" y=\"-38.2763\">4</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;4</title>\n",
+        "<path d=\"M205.318,-80.8497C213.779,-75.9317 224.719,-70.054 235,-65.9763 256.763,-57.3441 282.696,-50.7995 301.122,-46.7421\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"308.035,-45.2588 301.852,-49.8073 304.613,-45.9931 301.191,-46.7273 301.191,-46.7273 301.191,-46.7273 304.613,-45.9931 300.53,-43.6474 308.035,-45.2588 308.035,-45.2588\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"235\" y=\"-69.7763\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>3-&gt;1</title>\n",
+        "<path d=\"M309.759,-95.8537C303.774,-93.0935 296.735,-90.3587 290,-88.9763 264.68,-83.7791 234.968,-84.9988 214.647,-86.9097\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"207.611,-87.6344 214.251,-83.7837 211.092,-87.2758 214.574,-86.9172 214.574,-86.9172 214.574,-86.9172 211.092,-87.2758 214.897,-90.0506 207.611,-87.6344 207.611,-87.6344\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"236.5\" y=\"-106.776\">p0 &amp; p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"246.5\" y=\"-92.7763\">\u24ff</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"262.5\" y=\"-92.7763\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>2</title>\n",
+        "<ellipse cx=\"457\" cy=\"-65.9763\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"457\" y=\"-62.2763\">2</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;2</title>\n",
+        "<path d=\"M335.511,-88.4949C341.556,-79.2153 350.612,-68.2281 362,-62.9763 384.317,-52.6847 412.886,-55.5321 432.641,-59.6259\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"439.492,-61.1686 431.971,-62.7039 436.077,-60.3997 432.663,-59.6309 432.663,-59.6309 432.663,-59.6309 436.077,-60.3997 433.355,-56.5578 439.492,-61.1686 439.492,-61.1686\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"362\" y=\"-66.7763\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge11\"><title>4-&gt;0</title>\n",
+        "<path d=\"M307.861,-39.6617C278.151,-35.9554 215.165,-29.4475 162,-32.9763 134.095,-34.8284 102.292,-39.4203 81.0681,-42.8433\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"74.026,-43.999 80.4235,-39.7569 77.4798,-43.4321 80.9336,-42.8653 80.9336,-42.8653 80.9336,-42.8653 77.4798,-43.4321 81.4438,-45.9737 74.026,-43.999 74.026,-43.999\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"162\" y=\"-51.7763\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"181.5\" y=\"-36.7763\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;0</title>\n",
+        "<path d=\"M441.122,-56.792C420.303,-44.5162 380.881,-23.3363 344,-14.9763 234.578,9.82701 199.773,1.22321 92,-29.9763 87.4862,-31.283 82.8412,-33.1348 78.4696,-35.1389\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"71.883,-38.3573 76.7894,-32.4539 75.0277,-36.8207 78.1724,-35.2841 78.1724,-35.2841 78.1724,-35.2841 75.0277,-36.8207 79.5553,-38.1143 71.883,-38.3573 71.883,-38.3573\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"235\" y=\"-7.77629\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;3</title>\n",
+        "<path d=\"M440.59,-73.8232C434.584,-76.667 427.575,-79.729 421,-81.9763 397.655,-89.9552 370.079,-96.032 350.856,-99.7561\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"343.923,-101.067 350.216,-96.6712 347.362,-100.417 350.801,-99.7663 350.801,-99.7663 350.801,-99.7663 347.362,-100.417 351.387,-102.861 343.923,-101.067 343.923,-101.067\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"364\" y=\"-115.776\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"383.5\" y=\"-100.776\">\u2776</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD><TD><svg height=\"150pt\" viewBox=\"0.00 0.00 360.00 149.80\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.745342 0.745342) rotate(0) translate(4 196.976)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-196.976 479,-196.976 479,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"164.5\" y=\"-178.776\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"186.5\" y=\"-178.776\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"202.5\" y=\"-178.776\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238.5\" y=\"-178.776\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"254.5\" y=\"-178.776\">)&amp;Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"290.5\" y=\"-178.776\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"306.5\" y=\"-178.776\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-46.9763\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-43.2763\">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,-46.9763C2.79388,-46.9763 17.1543,-46.9763 30.6317,-46.9763\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-46.9763 30.9419,-50.1264 34.4419,-46.9763 30.9419,-46.9764 30.9419,-46.9764 30.9419,-46.9764 34.4419,-46.9763 30.9418,-43.8264 37.9419,-46.9763 37.9419,-46.9763\" 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,-64.0136C48.3189,-73.8342 50.4453,-82.9763 56,-82.9763 60.166,-82.9763 62.4036,-77.8339 62.7128,-71.1196\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"62.3792,-64.0136 65.8541,-70.8581 62.5434,-67.5097 62.7076,-71.0059 62.7076,-71.0059 62.7076,-71.0059 62.5434,-67.5097 59.561,-71.1537 62.3792,-64.0136 62.3792,-64.0136\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"26.5\" y=\"-101.776\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"48\" y=\"-86.7763\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
+        "<ellipse cx=\"189.5\" cy=\"-89.9763\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"189.5\" y=\"-86.2763\">1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
+        "<path d=\"M73.3887,-52.3353C96.5205,-59.8993 138.861,-73.7446 165.24,-82.3705\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"171.905,-84.5497 164.272,-85.368 168.578,-83.4619 165.251,-82.374 165.251,-82.374 165.251,-82.374 168.578,-83.4619 166.231,-79.38 171.905,-84.5497 171.905,-84.5497\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-92.7763\">p0 &amp; p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"110\" y=\"-77.7763\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
+        "<ellipse cx=\"326\" cy=\"-103.976\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"326\" y=\"-100.276\">3</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;3</title>\n",
+        "<path d=\"M62.8051,-63.6491C68.3468,-77.3067 77.9479,-96.2306 92,-107.976 143.772,-151.251 168.511,-147.475 235,-158.976 259.087,-163.143 268.572,-170.739 290,-158.976 302.275,-152.238 310.86,-139.167 316.455,-127.458\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"319.408,-120.78 319.458,-128.456 317.993,-123.98 316.577,-127.181 316.577,-127.181 316.577,-127.181 317.993,-123.98 313.696,-125.907 319.408,-120.78 319.408,-120.78\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"162\" y=\"-158.776\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;3</title>\n",
+        "<path d=\"M203.361,-102.129C211.682,-109.128 223.142,-117.253 235,-120.976 258.322,-128.299 266.178,-126.456 290,-120.976 294.58,-119.923 299.255,-118.187 303.635,-116.217\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"310.22,-112.993 305.318,-118.9 307.077,-114.532 303.933,-116.071 303.933,-116.071 303.933,-116.071 307.077,-114.532 302.548,-113.242 310.22,-112.993 310.22,-112.993\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"235\" y=\"-143.776\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"254.5\" y=\"-128.776\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>4</title>\n",
+        "<ellipse cx=\"326\" cy=\"-41.9763\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"326\" y=\"-38.2763\">4</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;4</title>\n",
+        "<path d=\"M205.318,-80.8497C213.779,-75.9317 224.719,-70.054 235,-65.9763 256.763,-57.3441 282.696,-50.7995 301.122,-46.7421\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"308.035,-45.2588 301.852,-49.8073 304.613,-45.9931 301.191,-46.7273 301.191,-46.7273 301.191,-46.7273 304.613,-45.9931 300.53,-43.6474 308.035,-45.2588 308.035,-45.2588\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"235\" y=\"-69.7763\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>3-&gt;1</title>\n",
+        "<path d=\"M309.759,-95.8537C303.774,-93.0935 296.735,-90.3587 290,-88.9763 264.68,-83.7791 234.968,-84.9988 214.647,-86.9097\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"207.611,-87.6344 214.251,-83.7837 211.092,-87.2758 214.574,-86.9172 214.574,-86.9172 214.574,-86.9172 211.092,-87.2758 214.897,-90.0506 207.611,-87.6344 207.611,-87.6344\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"236.5\" y=\"-106.776\">p0 &amp; p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"246.5\" y=\"-92.7763\">\u24ff</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"262.5\" y=\"-92.7763\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>2</title>\n",
+        "<ellipse cx=\"457\" cy=\"-65.9763\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"457\" y=\"-62.2763\">2</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;2</title>\n",
+        "<path d=\"M335.511,-88.4949C341.556,-79.2153 350.612,-68.2281 362,-62.9763 384.317,-52.6847 412.886,-55.5321 432.641,-59.6259\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"439.492,-61.1686 431.971,-62.7039 436.077,-60.3997 432.663,-59.6309 432.663,-59.6309 432.663,-59.6309 436.077,-60.3997 433.355,-56.5578 439.492,-61.1686 439.492,-61.1686\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"362\" y=\"-66.7763\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge11\"><title>4-&gt;0</title>\n",
+        "<path d=\"M307.861,-39.6617C278.151,-35.9554 215.165,-29.4475 162,-32.9763 134.095,-34.8284 102.292,-39.4203 81.0681,-42.8433\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"74.026,-43.999 80.4235,-39.7569 77.4798,-43.4321 80.9336,-42.8653 80.9336,-42.8653 80.9336,-42.8653 77.4798,-43.4321 81.4438,-45.9737 74.026,-43.999 74.026,-43.999\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"162\" y=\"-51.7763\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"181.5\" y=\"-36.7763\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;0</title>\n",
+        "<path d=\"M441.122,-56.792C420.303,-44.5162 380.881,-23.3363 344,-14.9763 234.578,9.82701 199.773,1.22321 92,-29.9763 87.4862,-31.283 82.8412,-33.1348 78.4696,-35.1389\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"71.883,-38.3573 76.7894,-32.4539 75.0277,-36.8207 78.1724,-35.2841 78.1724,-35.2841 78.1724,-35.2841 75.0277,-36.8207 79.5553,-38.1143 71.883,-38.3573 71.883,-38.3573\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"235\" y=\"-7.77629\">p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;3</title>\n",
+        "<path d=\"M440.59,-73.8232C434.584,-76.667 427.575,-79.729 421,-81.9763 397.655,-89.9552 370.079,-96.032 350.856,-99.7561\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"343.923,-101.067 350.216,-96.6712 347.362,-100.417 350.801,-99.7663 350.801,-99.7663 350.801,-99.7663 347.362,-100.417 351.387,-102.861 343.923,-101.067 343.923,-101.067\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"364\" y=\"-115.776\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"383.5\" y=\"-100.776\">\u2776</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD></TR><TR><TD><svg height=\"72pt\" viewBox=\"0.00 0.00 360.00 71.66\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.593081 0.593081) rotate(0) translate(4 116.822)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-116.822 603,-116.822 603,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"226.5\" y=\"-98.622\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"248.5\" y=\"-98.622\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"264.5\" y=\"-98.622\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"300.5\" y=\"-98.622\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"316.5\" y=\"-98.622\">)&amp;Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"352.5\" y=\"-98.622\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"368.5\" y=\"-98.622\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-38.822\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-35.122\">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,-38.822C2.79388,-38.822 17.1543,-38.822 30.6317,-38.822\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-38.822 30.9419,-41.9721 34.4419,-38.822 30.9419,-38.8221 30.9419,-38.8221 30.9419,-38.8221 34.4419,-38.822 30.9418,-35.6721 37.9419,-38.822 37.9419,-38.822\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
+        "<ellipse cx=\"192.5\" cy=\"-71.822\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"192.5\" y=\"-68.122\">1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
+        "<path d=\"M72.3414,-46.8809C78.3384,-49.7508 85.3598,-52.7752 92,-54.822 117.058,-62.5458 146.814,-67.0482 167.217,-69.4564\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"174.285,-70.2509 166.977,-72.5991 170.807,-69.8599 167.329,-69.4688 167.329,-69.4688 167.329,-69.4688 170.807,-69.8599 167.681,-66.3386 174.285,-70.2509 174.285,-70.2509\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-69.622\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;0</title>\n",
+        "<path d=\"M179.732,-58.479C171.503,-50.2086 159.741,-40.3302 147,-35.822 125.532,-28.2255 99.3558,-30.2451 80.7802,-33.3971\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.8134,-34.6924 80.1197,-30.3159 77.2544,-34.0526 80.6955,-33.4128 80.6955,-33.4128 80.6955,-33.4128 77.2544,-34.0526 81.2713,-36.5097 73.8134,-34.6924 73.8134,-34.6924\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-39.622\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
+        "<ellipse cx=\"326\" cy=\"-29.822\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"326\" y=\"-26.122\">3</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;3</title>\n",
+        "<path d=\"M209.889,-66.5876C232.922,-59.2309 275.001,-45.7912 301.403,-37.3587\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"308.405,-35.1224 302.695,-40.2528 305.071,-36.1873 301.737,-37.2522 301.737,-37.2522 301.737,-37.2522 305.071,-36.1873 300.778,-34.2515 308.405,-35.1224 308.405,-35.1224\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238\" y=\"-75.622\">p0 &amp; p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"256\" y=\"-60.622\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>3-&gt;0</title>\n",
+        "<path d=\"M307.984,-26.6322C287.282,-22.9276 251.225,-17.0411 220,-14.822 163.045,-10.7743 147.287,-11.5519 92,-25.822 87.8988,-26.8805 83.611,-28.2457 79.4989,-29.6919\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"72.8087,-32.1626 78.2839,-26.7826 76.0919,-30.9501 79.3752,-29.7376 79.3752,-29.7376 79.3752,-29.7376 76.0919,-30.9501 80.4665,-32.6925 72.8087,-32.1626 72.8087,-32.1626\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"165\" y=\"-33.622\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"184.5\" y=\"-18.622\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
+        "<ellipse cx=\"450\" cy=\"-29.822\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"450\" y=\"-26.122\">4</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;4</title>\n",
+        "<path d=\"M344.221,-29.822C365.202,-29.822 400.787,-29.822 424.587,-29.822\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"431.867,-29.822 424.867,-32.9721 428.367,-29.822 424.867,-29.8221 424.867,-29.8221 424.867,-29.8221 428.367,-29.822 424.867,-26.6721 431.867,-29.822 431.867,-29.822\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"362\" y=\"-48.622\">p0 &amp; p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"380\" y=\"-33.622\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
+        "<ellipse cx=\"581\" cy=\"-29.822\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"581\" y=\"-26.122\">2</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>2-&gt;4</title>\n",
+        "<path d=\"M567.046,-18.1562C560.841,-13.3397 553.023,-8.30843 545,-5.82198 519.953,1.94066 511.047,1.94066 486,-5.82198 480.359,-7.57027 474.819,-10.5767 469.87,-13.8819\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"463.954,-18.1562 467.784,-11.5033 466.791,-16.1064 469.628,-14.0566 469.628,-14.0566 469.628,-14.0566 466.791,-16.1064 471.473,-16.6099 463.954,-18.1562 463.954,-18.1562\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"486\" y=\"-23.622\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"499.5\" y=\"-9.62198\">\u24ff</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"515.5\" y=\"-9.62198\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>4-&gt;2</title>\n",
+        "<path d=\"M468.056,-32.1651C473.751,-32.8421 480.138,-33.4881 486,-33.822 512.18,-35.3131 518.82,-35.3131 545,-33.822 548.48,-33.6237 552.146,-33.3155 555.742,-32.956\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"562.944,-32.1651 556.329,-36.0606 559.464,-32.5472 555.985,-32.9294 555.985,-32.9294 555.985,-32.9294 559.464,-32.5472 555.641,-29.7982 562.944,-32.1651 562.944,-32.1651\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"489.5\" y=\"-53.622\">p0 &amp; p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"507.5\" y=\"-38.622\">\u24ff</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD><TD><svg height=\"72pt\" viewBox=\"0.00 0.00 360.00 71.66\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.593081 0.593081) rotate(0) translate(4 116.822)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-116.822 603,-116.822 603,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"226.5\" y=\"-98.622\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"248.5\" y=\"-98.622\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"264.5\" y=\"-98.622\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"300.5\" y=\"-98.622\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"316.5\" y=\"-98.622\">)&amp;Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"352.5\" y=\"-98.622\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"368.5\" y=\"-98.622\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-38.822\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-35.122\">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,-38.822C2.79388,-38.822 17.1543,-38.822 30.6317,-38.822\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-38.822 30.9419,-41.9721 34.4419,-38.822 30.9419,-38.8221 30.9419,-38.8221 30.9419,-38.8221 34.4419,-38.822 30.9418,-35.6721 37.9419,-38.822 37.9419,-38.822\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
+        "<ellipse cx=\"192.5\" cy=\"-71.822\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"192.5\" y=\"-68.122\">1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
+        "<path d=\"M72.3414,-46.8809C78.3384,-49.7508 85.3598,-52.7752 92,-54.822 117.058,-62.5458 146.814,-67.0482 167.217,-69.4564\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"174.285,-70.2509 166.977,-72.5991 170.807,-69.8599 167.329,-69.4688 167.329,-69.4688 167.329,-69.4688 170.807,-69.8599 167.681,-66.3386 174.285,-70.2509 174.285,-70.2509\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-69.622\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;0</title>\n",
+        "<path d=\"M179.732,-58.479C171.503,-50.2086 159.741,-40.3302 147,-35.822 125.532,-28.2255 99.3558,-30.2451 80.7802,-33.3971\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.8134,-34.6924 80.1197,-30.3159 77.2544,-34.0526 80.6955,-33.4128 80.6955,-33.4128 80.6955,-33.4128 77.2544,-34.0526 81.2713,-36.5097 73.8134,-34.6924 73.8134,-34.6924\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-39.622\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
+        "<ellipse cx=\"326\" cy=\"-29.822\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"326\" y=\"-26.122\">3</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;3</title>\n",
+        "<path d=\"M209.889,-66.5876C232.922,-59.2309 275.001,-45.7912 301.403,-37.3587\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"308.405,-35.1224 302.695,-40.2528 305.071,-36.1873 301.737,-37.2522 301.737,-37.2522 301.737,-37.2522 305.071,-36.1873 300.778,-34.2515 308.405,-35.1224 308.405,-35.1224\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238\" y=\"-75.622\">p0 &amp; p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"256\" y=\"-60.622\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>3-&gt;0</title>\n",
+        "<path d=\"M307.984,-26.6322C287.282,-22.9276 251.225,-17.0411 220,-14.822 163.045,-10.7743 147.287,-11.5519 92,-25.822 87.8988,-26.8805 83.611,-28.2457 79.4989,-29.6919\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"72.8087,-32.1626 78.2839,-26.7826 76.0919,-30.9501 79.3752,-29.7376 79.3752,-29.7376 79.3752,-29.7376 76.0919,-30.9501 80.4665,-32.6925 72.8087,-32.1626 72.8087,-32.1626\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"165\" y=\"-33.622\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"184.5\" y=\"-18.622\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
+        "<ellipse cx=\"450\" cy=\"-29.822\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"450\" y=\"-26.122\">4</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;4</title>\n",
+        "<path d=\"M344.221,-29.822C365.202,-29.822 400.787,-29.822 424.587,-29.822\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"431.867,-29.822 424.867,-32.9721 428.367,-29.822 424.867,-29.8221 424.867,-29.8221 424.867,-29.8221 428.367,-29.822 424.867,-26.6721 431.867,-29.822 431.867,-29.822\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"362\" y=\"-48.622\">p0 &amp; p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"380\" y=\"-33.622\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
+        "<ellipse cx=\"581\" cy=\"-29.822\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"581\" y=\"-26.122\">2</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>2-&gt;4</title>\n",
+        "<path d=\"M567.046,-18.1562C560.841,-13.3397 553.023,-8.30843 545,-5.82198 519.953,1.94066 511.047,1.94066 486,-5.82198 480.359,-7.57027 474.819,-10.5767 469.87,-13.8819\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"463.954,-18.1562 467.784,-11.5033 466.791,-16.1064 469.628,-14.0566 469.628,-14.0566 469.628,-14.0566 466.791,-16.1064 471.473,-16.6099 463.954,-18.1562 463.954,-18.1562\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"486\" y=\"-23.622\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"499.5\" y=\"-9.62198\">\u24ff</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"515.5\" y=\"-9.62198\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>4-&gt;2</title>\n",
+        "<path d=\"M468.056,-32.1651C473.751,-32.8421 480.138,-33.4881 486,-33.822 512.18,-35.3131 518.82,-35.3131 545,-33.822 548.48,-33.6237 552.146,-33.3155 555.742,-32.956\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"562.944,-32.1651 556.329,-36.0606 559.464,-32.5472 555.985,-32.9294 555.985,-32.9294 555.985,-32.9294 559.464,-32.5472 555.641,-29.7982 562.944,-32.1651 562.944,-32.1651\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"489.5\" y=\"-53.622\">p0 &amp; p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"507.5\" y=\"-38.622\">\u24ff</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD></TR><TR><TD><svg height=\"78pt\" viewBox=\"0.00 0.00 360.00 78.33\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.601504 0.601504) rotate(0) translate(4 126.217)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-126.217 594.5,-126.217 594.5,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"222.25\" y=\"-108.017\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"244.25\" y=\"-108.017\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"260.25\" y=\"-108.017\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"296.25\" y=\"-108.017\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"312.25\" y=\"-108.017\">)&amp;Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"348.25\" y=\"-108.017\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"364.25\" y=\"-108.017\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-35.2168\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-31.5168\">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,-35.2168C2.79388,-35.2168 17.1543,-35.2168 30.6317,-35.2168\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-35.2168 30.9419,-38.3669 34.4419,-35.2169 30.9419,-35.2169 30.9419,-35.2169 30.9419,-35.2169 34.4419,-35.2169 30.9418,-32.0669 37.9419,-35.2168 37.9419,-35.2168\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>4</title>\n",
+        "<ellipse cx=\"183\" cy=\"-35.2168\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"183\" y=\"-31.5168\">4</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;4</title>\n",
+        "<path d=\"M74.0378,-38.1453C79.731,-38.9916 86.1223,-39.7991 92,-40.2168 116.383,-41.9497 122.617,-41.9497 147,-40.2168 150.49,-39.9688 154.161,-39.5834 157.759,-39.134\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"164.962,-38.1453 158.456,-42.218 161.495,-38.6213 158.027,-39.0973 158.027,-39.0973 158.027,-39.0973 161.495,-38.6213 157.599,-35.9765 164.962,-38.1453 164.962,-38.1453\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"93.5\" y=\"-60.0168\">p0 &amp; p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111.5\" y=\"-45.0168\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>4-&gt;0</title>\n",
+        "<path d=\"M170.404,-22.078C164.156,-16.0007 155.908,-9.42793 147,-6.21684 124.004,2.07228 114.996,2.07228 92,-6.21684 85.4579,-8.57499 79.2724,-12.7461 73.9732,-17.2026\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"68.596,-22.078 71.6659,-15.0425 71.1889,-19.7271 73.7818,-17.3761 73.7818,-17.3761 73.7818,-17.3761 71.1889,-19.7271 75.8976,-19.7097 68.596,-22.078 68.596,-22.078\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-25.0168\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111.5\" y=\"-10.0168\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>3</title>\n",
+        "<ellipse cx=\"310\" cy=\"-35.2168\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"310\" y=\"-31.5168\">3</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>4-&gt;3</title>\n",
+        "<path d=\"M201.119,-35.2168C222.691,-35.2168 259.912,-35.2168 284.495,-35.2168\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"291.687,-35.2168 284.687,-38.3669 288.187,-35.2169 284.687,-35.2169 284.687,-35.2169 284.687,-35.2169 288.187,-35.2169 284.687,-32.0669 291.687,-35.2168 291.687,-35.2168\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"219\" y=\"-54.0168\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238.5\" y=\"-39.0168\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>1</title>\n",
+        "<ellipse cx=\"434\" cy=\"-35.2168\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"434\" y=\"-31.5168\">1</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
+        "<ellipse cx=\"561\" cy=\"-35.2168\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"561\" y=\"-31.5168\">2</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;2</title>\n",
+        "<path d=\"M452.119,-35.2168C473.691,-35.2168 510.912,-35.2168 535.495,-35.2168\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"542.687,-35.2168 535.687,-38.3669 539.187,-35.2169 535.687,-35.2169 535.687,-35.2169 535.687,-35.2169 539.187,-35.2169 535.687,-32.0669 542.687,-35.2168 542.687,-35.2168\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"470\" y=\"-39.0168\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>2-&gt;2</title>\n",
+        "<path d=\"M550.627,-50.0085C547.249,-60.6333 550.707,-71.2168 561,-71.2168 568.881,-71.2168 572.754,-65.013 572.622,-57.3366\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"571.373,-50.0085 575.654,-56.3801 571.961,-53.4588 572.549,-56.9091 572.549,-56.9091 572.549,-56.9091 571.961,-53.4588 569.444,-57.4381 571.373,-50.0085 571.373,-50.0085\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"531.5\" y=\"-89.0168\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"545\" y=\"-75.0168\">\u24ff</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"561\" y=\"-75.0168\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>3-&gt;1</title>\n",
+        "<path d=\"M328.221,-35.2168C349.202,-35.2168 384.787,-35.2168 408.587,-35.2168\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"415.867,-35.2168 408.867,-38.3669 412.367,-35.2169 408.867,-35.2169 408.867,-35.2169 408.867,-35.2169 412.367,-35.2169 408.867,-32.0669 415.867,-35.2168 415.867,-35.2168\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"346\" y=\"-53.0168\">p0 &amp; p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"356\" y=\"-39.0168\">\u2776</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"372\" y=\"-39.0168\">\u2777</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD><TD><svg height=\"78pt\" viewBox=\"0.00 0.00 360.00 78.33\" width=\"360pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.601504 0.601504) rotate(0) translate(4 126.217)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-126.217 594.5,-126.217 594.5,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"222.25\" y=\"-108.017\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"244.25\" y=\"-108.017\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"260.25\" y=\"-108.017\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"296.25\" y=\"-108.017\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"312.25\" y=\"-108.017\">)&amp;Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"348.25\" y=\"-108.017\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"364.25\" y=\"-108.017\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-35.2168\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-31.5168\">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,-35.2168C2.79388,-35.2168 17.1543,-35.2168 30.6317,-35.2168\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-35.2168 30.9419,-38.3669 34.4419,-35.2169 30.9419,-35.2169 30.9419,-35.2169 30.9419,-35.2169 34.4419,-35.2169 30.9418,-32.0669 37.9419,-35.2168 37.9419,-35.2168\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>4</title>\n",
+        "<ellipse cx=\"183\" cy=\"-35.2168\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"183\" y=\"-31.5168\">4</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;4</title>\n",
+        "<path d=\"M74.0378,-38.1453C79.731,-38.9916 86.1223,-39.7991 92,-40.2168 116.383,-41.9497 122.617,-41.9497 147,-40.2168 150.49,-39.9688 154.161,-39.5834 157.759,-39.134\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"164.962,-38.1453 158.456,-42.218 161.495,-38.6213 158.027,-39.0973 158.027,-39.0973 158.027,-39.0973 161.495,-38.6213 157.599,-35.9765 164.962,-38.1453 164.962,-38.1453\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"93.5\" y=\"-60.0168\">p0 &amp; p1</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111.5\" y=\"-45.0168\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>4-&gt;0</title>\n",
+        "<path d=\"M170.404,-22.078C164.156,-16.0007 155.908,-9.42793 147,-6.21684 124.004,2.07228 114.996,2.07228 92,-6.21684 85.4579,-8.57499 79.2724,-12.7461 73.9732,-17.2026\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"68.596,-22.078 71.6659,-15.0425 71.1889,-19.7271 73.7818,-17.3761 73.7818,-17.3761 73.7818,-17.3761 71.1889,-19.7271 75.8976,-19.7097 68.596,-22.078 68.596,-22.078\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-25.0168\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111.5\" y=\"-10.0168\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>3</title>\n",
+        "<ellipse cx=\"310\" cy=\"-35.2168\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"310\" y=\"-31.5168\">3</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>4-&gt;3</title>\n",
+        "<path d=\"M201.119,-35.2168C222.691,-35.2168 259.912,-35.2168 284.495,-35.2168\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"291.687,-35.2168 284.687,-38.3669 288.187,-35.2169 284.687,-35.2169 284.687,-35.2169 284.687,-35.2169 288.187,-35.2169 284.687,-32.0669 291.687,-35.2168 291.687,-35.2168\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"219\" y=\"-54.0168\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238.5\" y=\"-39.0168\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>1</title>\n",
+        "<ellipse cx=\"434\" cy=\"-35.2168\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"434\" y=\"-31.5168\">1</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>2</title>\n",
+        "<ellipse cx=\"561\" cy=\"-35.2168\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"561\" y=\"-31.5168\">2</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;2</title>\n",
+        "<path d=\"M452.119,-35.2168C473.691,-35.2168 510.912,-35.2168 535.495,-35.2168\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"542.687,-35.2168 535.687,-38.3669 539.187,-35.2169 535.687,-35.2169 535.687,-35.2169 535.687,-35.2169 539.187,-35.2169 535.687,-32.0669 542.687,-35.2168 542.687,-35.2168\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"470\" y=\"-39.0168\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>2-&gt;2</title>\n",
+        "<path d=\"M550.627,-50.0085C547.249,-60.6333 550.707,-71.2168 561,-71.2168 568.881,-71.2168 572.754,-65.013 572.622,-57.3366\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"571.373,-50.0085 575.654,-56.3801 571.961,-53.4588 572.549,-56.9091 572.549,-56.9091 572.549,-56.9091 571.961,-53.4588 569.444,-57.4381 571.373,-50.0085 571.373,-50.0085\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"531.5\" y=\"-89.0168\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"545\" y=\"-75.0168\">\u24ff</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"561\" y=\"-75.0168\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>3-&gt;1</title>\n",
+        "<path d=\"M328.221,-35.2168C349.202,-35.2168 384.787,-35.2168 408.587,-35.2168\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"415.867,-35.2168 408.867,-38.3669 412.367,-35.2169 408.867,-35.2169 408.867,-35.2169 408.867,-35.2169 412.367,-35.2169 408.867,-32.0669 415.867,-35.2168 415.867,-35.2168\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"346\" y=\"-53.0168\">p0 &amp; p1</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"356\" y=\"-39.0168\">\u2776</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"372\" y=\"-39.0168\">\u2777</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg></TD></TR></TABLE>"
+       ],
+       "metadata": {},
+       "output_type": "pyout",
+       "prompt_number": 2,
+       "text": [
+        "<IPython.core.display.HTML at 0x7f56a8059ba8>"
+       ]
+      }
+     ],
+     "prompt_number": 2
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [],
+     "language": "python",
+     "metadata": {},
+     "outputs": []
+    }
+   ],
+   "metadata": {}
+  }
+ ]
+}
\ No newline at end of file