alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/wrap/python/tests/randaut.ipynb
Alexandre Duret-Lutz 2f42c1c9bf randaut: add option --acc-type=random 
Fixes #71.

* src/bin/randaut.cc: Implement option --acc-type.
* src/tgbaalgos/randomgraph.cc,
src/tgbaalgos/randomgraph.hh (random_acceptance): New function.
* src/tgbatest/randaut.test, wrap/python/tests/randaut.ipynb: Test it.
2015-03-31 13:50:56 +02:00

2056 lines
No EOL
190 KiB
Text
Raw Blame History

{
"metadata": {
"name": "",
"signature": "sha256:f4c7efdcb7b97c3b11c230a6b18c8e46c1708289918a5dd8df73fe6baae3c8f6"
},
"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.4,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 --acc-type=random -H -S5 -A4 -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=\"94pt\" viewBox=\"0.00 0.00 389.00 94.23\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.604037 0.604037) rotate(0) translate(4 152)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-152 640,-152 640,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"208.5\" y=\"-133.8\">(Fin(</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"236.5\" y=\"-133.8\">\u2777</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"252.5\" y=\"-133.8\">) &amp; Inf(</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"295.5\" y=\"-133.8\">\u2778</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"311.5\" y=\"-133.8\">)) | Inf(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"351.5\" y=\"-133.8\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"367.5\" y=\"-133.8\">) | Fin(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"407.5\" y=\"-133.8\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"423.5\" y=\"-133.8\">)</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
"<ellipse cx=\"56\" cy=\"-43\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-39.3\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
"<path d=\"M1.15491,-43C2.79388,-43 17.1543,-43 30.6317,-43\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"37.9419,-43 30.9419,-46.1501 34.4419,-43 30.9419,-43.0001 30.9419,-43.0001 30.9419,-43.0001 34.4419,-43 30.9418,-39.8501 37.9419,-43 37.9419,-43\" stroke=\"black\"/>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node3\"><title>4</title>\n",
"<ellipse cx=\"196.5\" cy=\"-107\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"196.5\" y=\"-103.3\">4</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>0-&gt;4</title>\n",
"<path d=\"M72.6185,-50.2172C97.2443,-61.5966 145.184,-83.7494 173.354,-96.7666\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"179.726,-99.711 172.05,-99.6341 176.549,-98.2428 173.372,-96.7746 173.372,-96.7746 173.372,-96.7746 176.549,-98.2428 174.693,-93.9151 179.726,-99.711 179.726,-99.711\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-89.8\">!p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node4\"><title>1</title>\n",
"<ellipse cx=\"337\" cy=\"-72\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"337\" y=\"-68.3\">1</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>4-&gt;1</title>\n",
"<path d=\"M214.812,-106.46C235.75,-105.365 271.815,-102.047 301,-92 305.802,-90.347 310.693,-88.0243 315.238,-85.5443\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"321.598,-81.8579 317.121,-88.0936 318.57,-83.6131 315.542,-85.3684 315.542,-85.3684 315.542,-85.3684 318.57,-83.6131 313.962,-82.6431 321.598,-81.8579 321.598,-81.8579\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242\" y=\"-107.8\">!p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;0</title>\n",
"<path d=\"M319.285,-68.5504C313.501,-67.385 306.972,-66.1011 301,-65 266.869,-58.7071 258.495,-55.8289 224,-52 173.507,-46.3953 114.022,-44.2477 81.4244,-43.4497\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"74.1216,-43.2827 81.1918,-40.2936 77.6206,-43.3627 81.1197,-43.4428 81.1197,-43.4428 81.1197,-43.4428 77.6206,-43.3627 81.0477,-46.592 74.1216,-43.2827 74.1216,-43.2827\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"169\" y=\"-69.8\">p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"180.5\" y=\"-55.8\">\u24ff</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"196.5\" y=\"-55.8\">\u2777</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>1-&gt;4</title>\n",
"<path d=\"M318.853,-70.2251C299.612,-68.8402 267.724,-68.385 242,-77 232.889,-80.0513 223.897,-85.5125 216.407,-90.9468\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"210.499,-95.4519 214.155,-88.7025 213.282,-93.3297 216.065,-91.2074 216.065,-91.2074 216.065,-91.2074 213.282,-93.3297 217.975,-93.7123 210.499,-95.4519 210.499,-95.4519\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"245.5\" y=\"-80.8\">p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node5\"><title>2</title>\n",
"<ellipse cx=\"479.5\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"479.5\" y=\"-14.3\">2</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>1-&gt;2</title>\n",
"<path d=\"M350.281,-59.4247C356.579,-53.6389 364.666,-47.153 373,-43 399.034,-30.0267 432.08,-23.6063 454.186,-20.5548\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"461.238,-19.6445 454.698,-23.6649 457.766,-20.0927 454.295,-20.5408 454.295,-20.5408 454.295,-20.5408 457.766,-20.0927 453.892,-17.4167 461.238,-19.6445 461.238,-19.6445\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"373\" y=\"-46.8\">!p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>2-&gt;0</title>\n",
"<path d=\"M461.316,-18.3012C440.43,-18.7105 404.117,-19.5614 373,-21 247.989,-26.7795 216.651,-27.8917 92,-39 88.5277,-39.3094 84.8665,-39.6794 81.2726,-40.0675\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"74.0725,-40.8764 80.6771,-36.9645 77.5506,-40.4856 81.0288,-40.0949 81.0288,-40.0949 81.0288,-40.0949 77.5506,-40.4856 81.3804,-43.2252 74.0725,-40.8764 74.0725,-40.8764\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242\" y=\"-30.8\">!p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node6\"><title>3</title>\n",
"<ellipse cx=\"618\" cy=\"-47\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"618\" y=\"-43.3\">3</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>2-&gt;3</title>\n",
"<path d=\"M497.788,-17.6378C518.321,-17.6745 553.392,-19.2203 582,-28 586.796,-29.4719 591.685,-31.636 596.23,-33.9814\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"602.589,-37.4882 594.939,-36.8667 599.525,-35.7982 596.46,-34.1082 596.46,-34.1082 596.46,-34.1082 599.525,-35.7982 597.981,-31.3497 602.589,-37.4882 602.589,-37.4882\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"527\" y=\"-46.8\">p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"546.5\" y=\"-31.8\">\u24ff</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>3-&gt;1</title>\n",
"<path d=\"M600.829,-52.9992C594.977,-54.9248 588.265,-56.854 582,-58 502.497,-72.5421 406.218,-73.1946 362.144,-72.5759\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"355.032,-72.4583 362.083,-69.4246 358.532,-72.5162 362.031,-72.5742 362.031,-72.5742 362.031,-72.5742 358.532,-72.5162 361.979,-75.7237 355.032,-72.4583 355.032,-72.4583\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"450\" y=\"-89.8\">!p0 &amp; !p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"471.5\" y=\"-74.8\">\u2776</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD><TD><svg height=\"95pt\" viewBox=\"0.00 0.00 389.00 95.44\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.604037 0.604037) rotate(0) translate(4 154)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-154 640,-154 640,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"269\" y=\"-135.8\">Inf(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"291\" y=\"-135.8\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"307\" y=\"-135.8\">) | Fin(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"347\" y=\"-135.8\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"363\" y=\"-135.8\">)</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
"<ellipse cx=\"56\" cy=\"-43\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-39.3\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
"<path d=\"M1.15491,-43C2.79388,-43 17.1543,-43 30.6317,-43\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"37.9419,-43 30.9419,-46.1501 34.4419,-43 30.9419,-43.0001 30.9419,-43.0001 30.9419,-43.0001 34.4419,-43 30.9418,-39.8501 37.9419,-43 37.9419,-43\" stroke=\"black\"/>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node3\"><title>4</title>\n",
"<ellipse cx=\"196.5\" cy=\"-109\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"196.5\" y=\"-105.3\">4</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>0-&gt;4</title>\n",
"<path d=\"M72.6185,-50.4427C97.2443,-62.1778 145.184,-85.0228 173.354,-98.4468\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"179.726,-101.483 172.052,-101.315 176.566,-99.9775 173.407,-98.4718 173.407,-98.4718 173.407,-98.4718 176.566,-99.9775 174.762,-95.6282 179.726,-101.483 179.726,-101.483\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-90.8\">!p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node4\"><title>1</title>\n",
"<ellipse cx=\"337\" cy=\"-72\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"337\" y=\"-68.3\">1</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>4-&gt;1</title>\n",
"<path d=\"M214.816,-108.038C235.757,-106.452 271.826,-102.352 301,-92 305.786,-90.3018 310.671,-87.9595 315.214,-85.4746\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"321.574,-81.7903 317.096,-88.0248 318.546,-83.5447 315.517,-85.299 315.517,-85.299 315.517,-85.299 318.546,-83.5447 313.938,-82.5733 321.574,-81.7903 321.574,-81.7903\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242\" y=\"-108.8\">!p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;0</title>\n",
"<path d=\"M319.285,-68.5504C313.501,-67.385 306.972,-66.1011 301,-65 266.869,-58.7071 258.495,-55.8289 224,-52 173.507,-46.3953 114.022,-44.2477 81.4244,-43.4497\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"74.1216,-43.2827 81.1918,-40.2936 77.6206,-43.3627 81.1197,-43.4428 81.1197,-43.4428 81.1197,-43.4428 77.6206,-43.3627 81.0477,-46.592 74.1216,-43.2827 74.1216,-43.2827\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"169\" y=\"-70.8\">p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"188.5\" y=\"-55.8\">\u24ff</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>1-&gt;4</title>\n",
"<path d=\"M318.804,-70.0811C299.518,-68.5673 267.591,-67.9968 242,-77 232.415,-80.3722 223.084,-86.4987 215.462,-92.4951\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"209.991,-97.0074 213.387,-90.1233 212.691,-94.7804 215.391,-92.5533 215.391,-92.5533 215.391,-92.5533 212.691,-94.7804 217.396,-94.9834 209.991,-97.0074 209.991,-97.0074\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"245.5\" y=\"-80.8\">p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node5\"><title>2</title>\n",
"<ellipse cx=\"479.5\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"479.5\" y=\"-14.3\">2</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>1-&gt;2</title>\n",
"<path d=\"M350.281,-59.4247C356.579,-53.6389 364.666,-47.153 373,-43 399.034,-30.0267 432.08,-23.6063 454.186,-20.5548\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"461.238,-19.6445 454.698,-23.6649 457.766,-20.0927 454.295,-20.5408 454.295,-20.5408 454.295,-20.5408 457.766,-20.0927 453.892,-17.4167 461.238,-19.6445 461.238,-19.6445\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"373\" y=\"-46.8\">!p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>2-&gt;0</title>\n",
"<path d=\"M461.316,-18.3012C440.43,-18.7105 404.117,-19.5614 373,-21 247.989,-26.7795 216.651,-27.8917 92,-39 88.5277,-39.3094 84.8665,-39.6794 81.2726,-40.0675\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"74.0725,-40.8764 80.6771,-36.9645 77.5506,-40.4856 81.0288,-40.0949 81.0288,-40.0949 81.0288,-40.0949 77.5506,-40.4856 81.3804,-43.2252 74.0725,-40.8764 74.0725,-40.8764\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242\" y=\"-30.8\">!p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node6\"><title>3</title>\n",
"<ellipse cx=\"618\" cy=\"-47\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"618\" y=\"-43.3\">3</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>2-&gt;3</title>\n",
"<path d=\"M497.788,-17.6378C518.321,-17.6745 553.392,-19.2203 582,-28 586.796,-29.4719 591.685,-31.636 596.23,-33.9814\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"602.589,-37.4882 594.939,-36.8667 599.525,-35.7982 596.46,-34.1082 596.46,-34.1082 596.46,-34.1082 599.525,-35.7982 597.981,-31.3497 602.589,-37.4882 602.589,-37.4882\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"527\" y=\"-46.8\">p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"546.5\" y=\"-31.8\">\u24ff</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>3-&gt;1</title>\n",
"<path d=\"M600.829,-52.9992C594.977,-54.9248 588.265,-56.854 582,-58 502.497,-72.5421 406.218,-73.1946 362.144,-72.5759\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"355.032,-72.4583 362.083,-69.4246 358.532,-72.5162 362.031,-72.5742 362.031,-72.5742 362.031,-72.5742 358.532,-72.5162 361.979,-75.7237 355.032,-72.4583 355.032,-72.4583\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"450\" y=\"-89.8\">!p0 &amp; !p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"471.5\" y=\"-74.8\">\u2776</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD></TR><TR><TD><svg height=\"161pt\" viewBox=\"0.00 0.00 389.00 161.12\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.593893 0.593893) rotate(0) translate(4 267.292)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-267.292 651,-267.292 651,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"211.5\" y=\"-249.092\">((Inf(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"240.5\" y=\"-249.092\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"256.5\" y=\"-249.092\">) | Inf(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"293.5\" y=\"-249.092\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"309.5\" y=\"-249.092\">)) &amp; Fin(</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"359.5\" y=\"-249.092\">\u2778</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"375.5\" y=\"-249.092\">)) | Inf(</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"415.5\" y=\"-249.092\">\u2777</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"431.5\" y=\"-249.092\">)</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
"<ellipse cx=\"56\" cy=\"-108.292\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-104.592\">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,-108.292C2.79388,-108.292 17.1543,-108.292 30.6317,-108.292\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"37.9419,-108.292 30.9419,-111.442 34.4419,-108.292 30.9419,-108.292 30.9419,-108.292 30.9419,-108.292 34.4419,-108.292 30.9418,-105.142 37.9419,-108.292 37.9419,-108.292\" stroke=\"black\"/>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node3\"><title>4</title>\n",
"<ellipse cx=\"192.5\" cy=\"-138.292\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"192.5\" y=\"-134.592\">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,-112.031C97.3214,-117.286 140.361,-126.886 167.364,-132.909\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"174.526,-134.506 167.008,-136.057 171.11,-133.744 167.694,-132.982 167.694,-132.982 167.694,-132.982 171.11,-133.744 168.38,-129.908 174.526,-134.506 174.526,-134.506\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-131.092\">p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
"<ellipse cx=\"629\" cy=\"-103.292\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"629\" y=\"-99.5923\">2</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
"<path d=\"M66.4664,-123.193C86.0309,-151.95 133.942,-212.292 191.5,-212.292 191.5,-212.292 191.5,-212.292 493.5,-212.292 548.728,-212.292 593.968,-156.136 615.105,-124.438\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"619.006,-118.448 617.825,-126.033 617.096,-121.381 615.185,-124.314 615.185,-124.314 615.185,-124.314 617.096,-121.381 612.546,-122.594 619.006,-118.448 619.006,-118.448\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"315\" y=\"-230.092\">!p0 &amp; !p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"328.5\" y=\"-216.092\">\u2776</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"344.5\" y=\"-216.092\">\u2777</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node5\"><title>1</title>\n",
"<ellipse cx=\"344.5\" cy=\"-103.292\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"344.5\" y=\"-99.5923\">1</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge11\"><title>4-&gt;1</title>\n",
"<path d=\"M210.126,-134.413C236.819,-128.185 289.33,-115.932 319.896,-108.8\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"326.8,-107.189 320.699,-111.847 323.391,-107.984 319.983,-108.78 319.983,-108.78 319.983,-108.78 323.391,-107.984 319.267,-105.712 326.8,-107.189 326.8,-107.189\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238\" y=\"-145.092\">!p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"259.5\" y=\"-130.092\">\u24ff</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>2-&gt;1</title>\n",
"<path d=\"M610.979,-103.292C562.875,-103.292 425.789,-103.292 369.784,-103.292\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"362.746,-103.292 369.746,-100.142 366.246,-103.292 369.746,-103.292 369.746,-103.292 369.746,-103.292 366.246,-103.292 369.746,-106.442 362.746,-103.292 362.746,-103.292\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"465\" y=\"-122.092\">!p0 &amp; p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"484.5\" y=\"-107.092\">\u24ff</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node6\"><title>3</title>\n",
"<ellipse cx=\"492.5\" cy=\"-37.2923\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"492.5\" y=\"-33.5923\">3</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>2-&gt;3</title>\n",
"<path d=\"M627.214,-85.2939C625.158,-62.9548 617.943,-25.6846 593,-8.2923 572.949,5.68914 561.432,-1.33095 538,-8.2923 528.884,-11.0005 519.891,-16.2327 512.402,-21.516\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"506.495,-25.9117 510.23,-19.2057 509.303,-23.8223 512.11,-21.7328 512.11,-21.7328 512.11,-21.7328 509.303,-23.8223 513.991,-24.26 506.495,-25.9117 506.495,-25.9117\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"539.5\" y=\"-27.0923\">p0 &amp; p1</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"557.5\" y=\"-12.0923\">\u2777</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>1-&gt;0</title>\n",
"<path d=\"M326.509,-101.558C294.766,-98.5543 224.3,-93.008 165,-96.2923 136.061,-97.8951 102.96,-101.896 81.1142,-104.839\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"74.1596,-105.792 80.6673,-101.721 77.6272,-105.317 81.0948,-104.842 81.0948,-104.842 81.0948,-104.842 77.6272,-105.317 81.5224,-107.963 74.1596,-105.792 74.1596,-105.792\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"165\" y=\"-100.092\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;2</title>\n",
"<path d=\"M361.826,-108.317C370.729,-111.029 381.953,-114.404 392,-117.292 447.338,-133.201 462.935,-144.968 520,-137.292 550.588,-133.178 584.28,-121.321 605.763,-112.767\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"612.29,-110.119 606.987,-115.67 609.047,-111.435 605.803,-112.751 605.803,-112.751 605.803,-112.751 609.047,-111.435 604.619,-109.832 612.29,-110.119 612.29,-110.119\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"465\" y=\"-143.092\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>1-&gt;3</title>\n",
"<path d=\"M356.656,-89.2868C365.276,-79.4166 378.058,-66.6876 392,-59.2923 415.767,-46.6856 446.408,-41.2932 467.369,-38.9927\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"474.353,-38.3012 467.697,-42.1257 470.87,-38.6461 467.387,-38.991 467.387,-38.991 467.387,-38.991 470.87,-38.6461 467.077,-35.8564 474.353,-38.3012 474.353,-38.3012\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"392\" y=\"-78.0923\">!p0 &amp; p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"411.5\" y=\"-63.0923\">\u2776</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge10\"><title>3-&gt;0</title>\n",
"<path d=\"M474.212,-37.0029C454.339,-36.818 420.759,-36.9578 392,-39.2923 256.968,-50.2535 221.005,-51.9217 92,-93.2923 87.7036,-94.6701 83.2103,-96.3794 78.9306,-98.1455\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"72.44,-100.928 77.6325,-95.2747 75.6569,-99.549 78.8737,-98.1699 78.8737,-98.1699 78.8737,-98.1699 75.6569,-99.549 80.115,-101.065 72.44,-100.928 72.44,-100.928\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"240\" y=\"-74.0923\">p0 &amp; !p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"259.5\" y=\"-59.0923\">\u2776</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>3-&gt;2</title>\n",
"<path d=\"M510.59,-38.1655C531.47,-39.9276 567.197,-45.2451 593,-61.2923 601.478,-66.5649 608.898,-74.5955 614.698,-82.2274\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"618.809,-87.9335 612.161,-84.0948 616.763,-85.0936 614.717,-82.2536 614.717,-82.2536 614.717,-82.2536 616.763,-85.0936 617.273,-80.4125 618.809,-87.9335 618.809,-87.9335\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"538\" y=\"-79.0923\">p0 &amp; !p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"549.5\" y=\"-65.0923\">\u2776</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"565.5\" y=\"-65.0923\">\u2777</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD><TD><svg height=\"161pt\" viewBox=\"0.00 0.00 389.00 161.12\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.593893 0.593893) rotate(0) translate(4 267.292)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-267.292 651,-267.292 651,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"249.5\" y=\"-249.092\">Inf(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"271.5\" y=\"-249.092\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"287.5\" y=\"-249.092\">) | Inf(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"324.5\" y=\"-249.092\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"340.5\" y=\"-249.092\">) | Inf(</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"377.5\" y=\"-249.092\">\u2777</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"393.5\" y=\"-249.092\">)</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
"<ellipse cx=\"56\" cy=\"-108.292\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-104.592\">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,-108.292C2.79388,-108.292 17.1543,-108.292 30.6317,-108.292\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"37.9419,-108.292 30.9419,-111.442 34.4419,-108.292 30.9419,-108.292 30.9419,-108.292 30.9419,-108.292 34.4419,-108.292 30.9418,-105.142 37.9419,-108.292 37.9419,-108.292\" stroke=\"black\"/>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node3\"><title>4</title>\n",
"<ellipse cx=\"192.5\" cy=\"-138.292\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"192.5\" y=\"-134.592\">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,-112.031C97.3214,-117.286 140.361,-126.886 167.364,-132.909\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"174.526,-134.506 167.008,-136.057 171.11,-133.744 167.694,-132.982 167.694,-132.982 167.694,-132.982 171.11,-133.744 168.38,-129.908 174.526,-134.506 174.526,-134.506\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-131.092\">p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
"<ellipse cx=\"629\" cy=\"-103.292\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"629\" y=\"-99.5923\">2</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
"<path d=\"M66.4664,-123.193C86.0309,-151.95 133.942,-212.292 191.5,-212.292 191.5,-212.292 191.5,-212.292 493.5,-212.292 548.728,-212.292 593.968,-156.136 615.105,-124.438\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"619.006,-118.448 617.825,-126.033 617.096,-121.381 615.185,-124.314 615.185,-124.314 615.185,-124.314 617.096,-121.381 612.546,-122.594 619.006,-118.448 619.006,-118.448\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"315\" y=\"-230.092\">!p0 &amp; !p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"328.5\" y=\"-216.092\">\u2776</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"344.5\" y=\"-216.092\">\u2777</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node5\"><title>1</title>\n",
"<ellipse cx=\"344.5\" cy=\"-103.292\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"344.5\" y=\"-99.5923\">1</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge11\"><title>4-&gt;1</title>\n",
"<path d=\"M210.126,-134.413C236.819,-128.185 289.33,-115.932 319.896,-108.8\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"326.8,-107.189 320.699,-111.847 323.391,-107.984 319.983,-108.78 319.983,-108.78 319.983,-108.78 323.391,-107.984 319.267,-105.712 326.8,-107.189 326.8,-107.189\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238\" y=\"-145.092\">!p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"259.5\" y=\"-130.092\">\u24ff</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>2-&gt;1</title>\n",
"<path d=\"M610.979,-103.292C562.875,-103.292 425.789,-103.292 369.784,-103.292\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"362.746,-103.292 369.746,-100.142 366.246,-103.292 369.746,-103.292 369.746,-103.292 369.746,-103.292 366.246,-103.292 369.746,-106.442 362.746,-103.292 362.746,-103.292\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"465\" y=\"-122.092\">!p0 &amp; p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"484.5\" y=\"-107.092\">\u24ff</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node6\"><title>3</title>\n",
"<ellipse cx=\"492.5\" cy=\"-37.2923\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"492.5\" y=\"-33.5923\">3</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>2-&gt;3</title>\n",
"<path d=\"M627.214,-85.2939C625.158,-62.9548 617.943,-25.6846 593,-8.2923 572.949,5.68914 561.432,-1.33095 538,-8.2923 528.884,-11.0005 519.891,-16.2327 512.402,-21.516\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"506.495,-25.9117 510.23,-19.2057 509.303,-23.8223 512.11,-21.7328 512.11,-21.7328 512.11,-21.7328 509.303,-23.8223 513.991,-24.26 506.495,-25.9117 506.495,-25.9117\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"539.5\" y=\"-27.0923\">p0 &amp; p1</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"557.5\" y=\"-12.0923\">\u2777</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>1-&gt;0</title>\n",
"<path d=\"M326.509,-101.558C294.766,-98.5543 224.3,-93.008 165,-96.2923 136.061,-97.8951 102.96,-101.896 81.1142,-104.839\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"74.1596,-105.792 80.6673,-101.721 77.6272,-105.317 81.0948,-104.842 81.0948,-104.842 81.0948,-104.842 77.6272,-105.317 81.5224,-107.963 74.1596,-105.792 74.1596,-105.792\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"165\" y=\"-100.092\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;2</title>\n",
"<path d=\"M361.826,-108.317C370.729,-111.029 381.953,-114.404 392,-117.292 447.338,-133.201 462.935,-144.968 520,-137.292 550.588,-133.178 584.28,-121.321 605.763,-112.767\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"612.29,-110.119 606.987,-115.67 609.047,-111.435 605.803,-112.751 605.803,-112.751 605.803,-112.751 609.047,-111.435 604.619,-109.832 612.29,-110.119 612.29,-110.119\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"465\" y=\"-143.092\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>1-&gt;3</title>\n",
"<path d=\"M356.656,-89.2868C365.276,-79.4166 378.058,-66.6876 392,-59.2923 415.767,-46.6856 446.408,-41.2932 467.369,-38.9927\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"474.353,-38.3012 467.697,-42.1257 470.87,-38.6461 467.387,-38.991 467.387,-38.991 467.387,-38.991 470.87,-38.6461 467.077,-35.8564 474.353,-38.3012 474.353,-38.3012\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"392\" y=\"-78.0923\">!p0 &amp; p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"411.5\" y=\"-63.0923\">\u2776</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge10\"><title>3-&gt;0</title>\n",
"<path d=\"M474.212,-37.0029C454.339,-36.818 420.759,-36.9578 392,-39.2923 256.968,-50.2535 221.005,-51.9217 92,-93.2923 87.7036,-94.6701 83.2103,-96.3794 78.9306,-98.1455\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"72.44,-100.928 77.6325,-95.2747 75.6569,-99.549 78.8737,-98.1699 78.8737,-98.1699 78.8737,-98.1699 75.6569,-99.549 80.115,-101.065 72.44,-100.928 72.44,-100.928\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"240\" y=\"-74.0923\">p0 &amp; !p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"259.5\" y=\"-59.0923\">\u2776</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>3-&gt;2</title>\n",
"<path d=\"M510.59,-38.1655C531.47,-39.9276 567.197,-45.2451 593,-61.2923 601.478,-66.5649 608.898,-74.5955 614.698,-82.2274\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"618.809,-87.9335 612.161,-84.0948 616.763,-85.0936 614.717,-82.2536 614.717,-82.2536 614.717,-82.2536 616.763,-85.0936 617.273,-80.4125 618.809,-87.9335 618.809,-87.9335\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"538\" y=\"-79.0923\">p0 &amp; !p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"549.5\" y=\"-65.0923\">\u2776</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"565.5\" y=\"-65.0923\">\u2777</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD></TR><TR><TD><svg height=\"94pt\" viewBox=\"0.00 0.00 389.00 94.38\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.637705 0.637705) rotate(0) translate(4 144)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-144 606,-144 606,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"191\" y=\"-125.8\">(Inf(</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"216\" y=\"-125.8\">\u2777</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"232\" y=\"-125.8\">) | Fin(</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"272\" y=\"-125.8\">\u2778</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"288\" y=\"-125.8\">) | Inf(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"325\" y=\"-125.8\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"341\" y=\"-125.8\">)) &amp; Fin(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"391\" y=\"-125.8\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"407\" y=\"-125.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",
"<!-- 0&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>0-&gt;0</title>\n",
"<path d=\"M49.6208,-36.0373C48.3189,-45.8579 50.4453,-55 56,-55 60.166,-55 62.4036,-49.8576 62.7128,-43.1433\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"62.3792,-36.0373 65.8541,-42.8818 62.5434,-39.5335 62.7076,-43.0296 62.7076,-43.0296 62.7076,-43.0296 62.5434,-39.5335 59.561,-43.1774 62.3792,-36.0373 62.3792,-36.0373\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"26.5\" y=\"-73.8\">!p0 &amp; !p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"48\" y=\"-58.8\">\u2776</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node3\"><title>2</title>\n",
"<ellipse cx=\"180\" cy=\"-46\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"180\" y=\"-42.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.7078,-22.6976C94.762,-27.3572 131.09,-35.3969 155.083,-40.7069\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"162.103,-42.2604 154.587,-43.8233 158.685,-41.5041 155.268,-40.7477 155.268,-40.7477 155.268,-40.7477 158.685,-41.5041 155.949,-37.6722 162.103,-42.2604 162.103,-42.2604\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-41.8\">p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>2-&gt;2</title>\n",
"<path d=\"M169.627,-60.7917C166.249,-71.4165 169.707,-82 180,-82 187.881,-82 191.754,-75.7961 191.622,-68.1197\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"190.373,-60.7917 194.654,-67.1632 190.961,-64.242 191.549,-67.6923 191.549,-67.6923 191.549,-67.6923 190.961,-64.242 188.444,-68.2213 190.373,-60.7917 190.373,-60.7917\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"154\" y=\"-100.8\">p0 &amp; p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"172\" y=\"-85.8\">\u2776</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node5\"><title>3</title>\n",
"<ellipse cx=\"318.5\" cy=\"-89\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"318.5\" y=\"-85.3\">3</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>2-&gt;3</title>\n",
"<path d=\"M197.465,-51.1868C221.549,-58.7736 266.503,-72.935 294.039,-81.6094\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"300.977,-83.7948 293.353,-84.6959 297.638,-82.7431 294.3,-81.6915 294.3,-81.6915 294.3,-81.6915 297.638,-82.7431 295.246,-78.687 300.977,-83.7948 300.977,-83.7948\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"216\" y=\"-91.8\">p0 &amp; !p1</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"235.5\" y=\"-76.8\">\u2777</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node4\"><title>1</title>\n",
"<ellipse cx=\"584\" cy=\"-43\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"584\" y=\"-39.3\">1</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>1-&gt;0</title>\n",
"<path d=\"M568.174,-34.2983C545.326,-21.7336 499.768,-0 458,-0 179,-0 179,-0 179,-0 144.616,-0 105.422,-7.45961 80.9461,-13.0306\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"73.8442,-14.6886 79.9447,-10.0296 77.2525,-13.8929 80.6609,-13.0972 80.6609,-13.0972 80.6609,-13.0972 77.2525,-13.8929 81.377,-16.1647 73.8442,-14.6886 73.8442,-14.6886\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"289\" y=\"-3.8\">!p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;2</title>\n",
"<path d=\"M565.754,-43.1287C501.945,-43.6049 279.115,-45.2678 205.103,-45.8201\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"198.017,-45.873 204.993,-42.6708 201.517,-45.8468 205.016,-45.8207 205.016,-45.8207 205.016,-45.8207 201.517,-45.8468 205.04,-48.9706 198.017,-45.873 198.017,-45.873\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"366\" y=\"-47.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node6\"><title>4</title>\n",
"<ellipse cx=\"457\" cy=\"-89\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"457\" y=\"-85.3\">4</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>3-&gt;4</title>\n",
"<path d=\"M336.512,-89C360.421,-89 404.1,-89 431.506,-89\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"438.774,-89 431.774,-92.1501 435.274,-89 431.774,-89.0001 431.774,-89.0001 431.774,-89.0001 435.274,-89 431.774,-85.8501 438.774,-89 438.774,-89\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"367.5\" y=\"-106.8\">p0 &amp; p1</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"377.5\" y=\"-92.8\">\u2777</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"393.5\" y=\"-92.8\">\u2778</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>4-&gt;1</title>\n",
"<path d=\"M474.328,-83.4085C492.413,-77.1655 522.402,-66.6662 548,-57 552.001,-55.4893 556.239,-53.8377 560.334,-52.2155\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"567.021,-49.5434 561.69,-55.066 563.771,-50.8421 560.521,-52.1409 560.521,-52.1409 560.521,-52.1409 563.771,-50.8421 559.352,-49.2157 567.021,-49.5434 567.021,-49.5434\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"493\" y=\"-79.8\">p0 &amp; !p1</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD><TD><svg height=\"94pt\" viewBox=\"0.00 0.00 389.00 94.38\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.637705 0.637705) rotate(0) translate(4 144)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-144 606,-144 606,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"225.5\" y=\"-125.8\">Inf(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"247.5\" y=\"-125.8\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"263.5\" y=\"-125.8\">) | Fin(</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"303.5\" y=\"-125.8\">\u2777</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"319.5\" y=\"-125.8\">) | Inf(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"356.5\" y=\"-125.8\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"372.5\" y=\"-125.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",
"<!-- 0&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>0-&gt;0</title>\n",
"<path d=\"M49.6208,-36.0373C48.3189,-45.8579 50.4453,-55 56,-55 60.166,-55 62.4036,-49.8576 62.7128,-43.1433\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"62.3792,-36.0373 65.8541,-42.8818 62.5434,-39.5335 62.7076,-43.0296 62.7076,-43.0296 62.7076,-43.0296 62.5434,-39.5335 59.561,-43.1774 62.3792,-36.0373 62.3792,-36.0373\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"26.5\" y=\"-73.8\">!p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"48\" y=\"-58.8\">\u24ff</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node3\"><title>2</title>\n",
"<ellipse cx=\"180\" cy=\"-46\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"180\" y=\"-42.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.7078,-22.6976C94.762,-27.3572 131.09,-35.3969 155.083,-40.7069\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"162.103,-42.2604 154.587,-43.8233 158.685,-41.5041 155.268,-40.7477 155.268,-40.7477 155.268,-40.7477 158.685,-41.5041 155.949,-37.6722 162.103,-42.2604 162.103,-42.2604\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-41.8\">p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>2-&gt;2</title>\n",
"<path d=\"M169.627,-60.7917C166.249,-71.4165 169.707,-82 180,-82 187.881,-82 191.754,-75.7961 191.622,-68.1197\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"190.373,-60.7917 194.654,-67.1632 190.961,-64.242 191.549,-67.6923 191.549,-67.6923 191.549,-67.6923 190.961,-64.242 188.444,-68.2213 190.373,-60.7917 190.373,-60.7917\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"154\" y=\"-100.8\">p0 &amp; p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"172\" y=\"-85.8\">\u24ff</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node5\"><title>3</title>\n",
"<ellipse cx=\"318.5\" cy=\"-89\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"318.5\" y=\"-85.3\">3</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>2-&gt;3</title>\n",
"<path d=\"M197.465,-51.1868C221.549,-58.7736 266.503,-72.935 294.039,-81.6094\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"300.977,-83.7948 293.353,-84.6959 297.638,-82.7431 294.3,-81.6915 294.3,-81.6915 294.3,-81.6915 297.638,-82.7431 295.246,-78.687 300.977,-83.7948 300.977,-83.7948\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"216\" y=\"-91.8\">p0 &amp; !p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"235.5\" y=\"-76.8\">\u2776</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node4\"><title>1</title>\n",
"<ellipse cx=\"584\" cy=\"-43\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"584\" y=\"-39.3\">1</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>1-&gt;0</title>\n",
"<path d=\"M568.174,-34.2983C545.326,-21.7336 499.768,-0 458,-0 179,-0 179,-0 179,-0 144.616,-0 105.422,-7.45961 80.9461,-13.0306\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"73.8442,-14.6886 79.9447,-10.0296 77.2525,-13.8929 80.6609,-13.0972 80.6609,-13.0972 80.6609,-13.0972 77.2525,-13.8929 81.377,-16.1647 73.8442,-14.6886 73.8442,-14.6886\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"289\" y=\"-3.8\">!p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;2</title>\n",
"<path d=\"M565.754,-43.1287C501.945,-43.6049 279.115,-45.2678 205.103,-45.8201\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"198.017,-45.873 204.993,-42.6708 201.517,-45.8468 205.016,-45.8207 205.016,-45.8207 205.016,-45.8207 201.517,-45.8468 205.04,-48.9706 198.017,-45.873 198.017,-45.873\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"366\" y=\"-47.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node6\"><title>4</title>\n",
"<ellipse cx=\"457\" cy=\"-89\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"457\" y=\"-85.3\">4</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>3-&gt;4</title>\n",
"<path d=\"M336.512,-89C360.421,-89 404.1,-89 431.506,-89\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"438.774,-89 431.774,-92.1501 435.274,-89 431.774,-89.0001 431.774,-89.0001 431.774,-89.0001 435.274,-89 431.774,-85.8501 438.774,-89 438.774,-89\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"367.5\" y=\"-106.8\">p0 &amp; p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"377.5\" y=\"-92.8\">\u2776</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"393.5\" y=\"-92.8\">\u2777</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>4-&gt;1</title>\n",
"<path d=\"M474.328,-83.4085C492.413,-77.1655 522.402,-66.6662 548,-57 552.001,-55.4893 556.239,-53.8377 560.334,-52.2155\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"567.021,-49.5434 561.69,-55.066 563.771,-50.8421 560.521,-52.1409 560.521,-52.1409 560.521,-52.1409 563.771,-50.8421 559.352,-49.2157 567.021,-49.5434 567.021,-49.5434\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"493\" y=\"-79.8\">p0 &amp; !p1</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD></TR><TR><TD><svg height=\"95pt\" viewBox=\"0.00 0.00 389.00 95.32\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.63355 0.63355) rotate(0) translate(4 146.457)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-146.457 610,-146.457 610,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"184.5\" y=\"-128.257\">Fin(</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"209.5\" y=\"-128.257\">\u2777</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"225.5\" y=\"-128.257\">) &amp; (Inf(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"272.5\" y=\"-128.257\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"288.5\" y=\"-128.257\">) | (Fin(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"331.5\" y=\"-128.257\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"347.5\" y=\"-128.257\">) &amp; Fin(</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"393.5\" y=\"-128.257\">\u2778</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"409.5\" y=\"-128.257\">)))</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
"<ellipse cx=\"56\" cy=\"-44.4574\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-40.7574\">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,-44.4574C2.79388,-44.4574 17.1543,-44.4574 30.6317,-44.4574\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"37.9419,-44.4574 30.9419,-47.6075 34.4419,-44.4575 30.9419,-44.4575 30.9419,-44.4575 30.9419,-44.4575 34.4419,-44.4575 30.9418,-41.3075 37.9419,-44.4574 37.9419,-44.4574\" stroke=\"black\"/>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>0-&gt;0</title>\n",
"<path d=\"M49.6208,-61.4948C48.3189,-71.3154 50.4453,-80.4574 56,-80.4574 60.166,-80.4574 62.4036,-75.315 62.7128,-68.6007\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"62.3792,-61.4948 65.8541,-68.3393 62.5434,-64.9909 62.7076,-68.4871 62.7076,-68.4871 62.7076,-68.4871 62.5434,-64.9909 59.561,-68.6348 62.3792,-61.4948 62.3792,-61.4948\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"26.5\" y=\"-84.2574\">!p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node3\"><title>2</title>\n",
"<ellipse cx=\"461\" cy=\"-66.4574\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"461\" y=\"-62.7574\">2</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>0-&gt;2</title>\n",
"<path d=\"M67.7291,-58.2601C73.9738,-65.1392 82.4828,-72.7625 92,-76.4574 229.967,-130.022 278.431,-96.9852 425,-76.4574 428.912,-75.9096 432.999,-75.0332 436.944,-74.0214\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"443.821,-72.0954 437.93,-77.0165 440.451,-73.0393 437.081,-73.9832 437.081,-73.9832 437.081,-73.9832 440.451,-73.0393 436.231,-70.9499 443.821,-72.0954 443.821,-72.0954\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242\" y=\"-108.257\">!p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node4\"><title>1</title>\n",
"<ellipse cx=\"196.5\" cy=\"-44.4574\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"196.5\" y=\"-40.7574\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
"<path d=\"M74.2611,-44.4574C98.7573,-44.4574 143.707,-44.4574 171.456,-44.4574\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"178.456,-44.4574 171.457,-47.6075 174.956,-44.4575 171.456,-44.4575 171.456,-44.4575 171.456,-44.4575 174.956,-44.4575 171.456,-41.3075 178.456,-44.4574 178.456,-44.4574\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-63.2574\">!p0 &amp; !p1</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"113.5\" y=\"-48.2574\">\u2778</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node6\"><title>4</title>\n",
"<ellipse cx=\"588\" cy=\"-66.4574\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"588\" y=\"-62.7574\">4</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>2-&gt;4</title>\n",
"<path d=\"M479.119,-66.4574C500.691,-66.4574 537.912,-66.4574 562.495,-66.4574\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"569.687,-66.4574 562.687,-69.6075 566.187,-66.4575 562.687,-66.4575 562.687,-66.4575 562.687,-66.4575 566.187,-66.4575 562.687,-63.3075 569.687,-66.4574 569.687,-66.4574\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"497\" y=\"-85.2574\">p0 &amp; !p1</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"516.5\" y=\"-70.2574\">\u2777</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node5\"><title>3</title>\n",
"<ellipse cx=\"337\" cy=\"-39.4574\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"337\" y=\"-35.7574\">3</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>1-&gt;3</title>\n",
"<path d=\"M214.807,-42.5817C223.034,-41.772 233.013,-40.9084 242,-40.4574 265.599,-39.2731 292.571,-39.1086 311.553,-39.1891\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"318.663,-39.2323 311.644,-42.3396 315.163,-39.211 311.663,-39.1897 311.663,-39.1897 311.663,-39.1897 315.163,-39.211 311.682,-36.0397 318.663,-39.2323 318.663,-39.2323\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242\" y=\"-58.2574\">!p0 &amp; !p1</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"255.5\" y=\"-44.2574\">\u2777</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"271.5\" y=\"-44.2574\">\u2778</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>3-&gt;0</title>\n",
"<path d=\"M320.425,-31.7687C290.988,-18.1834 225.102,7.71572 169,-2.45745 136.409,-8.36739 100.952,-23.2169 78.8524,-33.5722\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"72.4406,-36.6268 77.4053,-30.7723 75.6003,-35.1214 78.7601,-33.6161 78.7601,-33.6161 78.7601,-33.6161 75.6003,-35.1214 80.1149,-36.4599 72.4406,-36.6268 72.4406,-36.6268\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"169\" y=\"-6.25745\">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=\"M355.038,-39.3705C372.845,-39.7041 401.421,-41.4457 425,-48.4574 429.664,-49.8445 434.442,-51.8529 438.91,-54.0296\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"445.183,-57.2863 437.519,-56.8568 442.077,-55.6737 438.97,-54.0611 438.97,-54.0611 438.97,-54.0611 442.077,-55.6737 440.422,-51.2654 445.183,-57.2863 445.183,-57.2863\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"373\" y=\"-66.2574\">p0 &amp; p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"383\" y=\"-52.2574\">\u24ff</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"399\" y=\"-52.2574\">\u2777</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>4-&gt;2</title>\n",
"<path d=\"M572.689,-56.5917C566.598,-52.964 559.237,-49.2952 552,-47.4574 528.307,-41.4413 520.693,-41.4413 497,-47.4574 492.137,-48.6922 487.219,-50.7535 482.668,-53.0735\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"476.311,-56.5917 480.91,-50.4459 479.374,-54.8968 482.436,-53.202 482.436,-53.202 482.436,-53.202 479.374,-54.8968 483.961,-55.958 476.311,-56.5917 476.311,-56.5917\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"498.5\" y=\"-51.2574\">p0 &amp; p1</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD><TD><svg height=\"95pt\" viewBox=\"0.00 0.00 389.00 95.32\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.63355 0.63355) rotate(0) translate(4 146.457)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-146.457 610,-146.457 610,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"218.5\" y=\"-128.257\">Fin(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"243.5\" y=\"-128.257\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"259.5\" y=\"-128.257\">) &amp; Fin(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"305.5\" y=\"-128.257\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"321.5\" y=\"-128.257\">) &amp; Fin(</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"367.5\" y=\"-128.257\">\u2777</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"383.5\" y=\"-128.257\">)</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
"<ellipse cx=\"56\" cy=\"-44.4574\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-40.7574\">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,-44.4574C2.79388,-44.4574 17.1543,-44.4574 30.6317,-44.4574\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"37.9419,-44.4574 30.9419,-47.6075 34.4419,-44.4575 30.9419,-44.4575 30.9419,-44.4575 30.9419,-44.4575 34.4419,-44.4575 30.9418,-41.3075 37.9419,-44.4574 37.9419,-44.4574\" stroke=\"black\"/>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>0-&gt;0</title>\n",
"<path d=\"M49.6208,-61.4948C48.3189,-71.3154 50.4453,-80.4574 56,-80.4574 60.166,-80.4574 62.4036,-75.315 62.7128,-68.6007\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"62.3792,-61.4948 65.8541,-68.3393 62.5434,-64.9909 62.7076,-68.4871 62.7076,-68.4871 62.7076,-68.4871 62.5434,-64.9909 59.561,-68.6348 62.3792,-61.4948 62.3792,-61.4948\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"26.5\" y=\"-84.2574\">!p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node3\"><title>2</title>\n",
"<ellipse cx=\"461\" cy=\"-66.4574\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"461\" y=\"-62.7574\">2</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>0-&gt;2</title>\n",
"<path d=\"M67.7291,-58.2601C73.9738,-65.1392 82.4828,-72.7625 92,-76.4574 229.967,-130.022 278.431,-96.9852 425,-76.4574 428.912,-75.9096 432.999,-75.0332 436.944,-74.0214\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"443.821,-72.0954 437.93,-77.0165 440.451,-73.0393 437.081,-73.9832 437.081,-73.9832 437.081,-73.9832 440.451,-73.0393 436.231,-70.9499 443.821,-72.0954 443.821,-72.0954\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242\" y=\"-108.257\">!p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node4\"><title>1</title>\n",
"<ellipse cx=\"196.5\" cy=\"-44.4574\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"196.5\" y=\"-40.7574\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
"<path d=\"M74.2611,-44.4574C98.7573,-44.4574 143.707,-44.4574 171.456,-44.4574\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"178.456,-44.4574 171.457,-47.6075 174.956,-44.4575 171.456,-44.4575 171.456,-44.4575 171.456,-44.4575 174.956,-44.4575 171.456,-41.3075 178.456,-44.4574 178.456,-44.4574\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-63.2574\">!p0 &amp; !p1</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"113.5\" y=\"-48.2574\">\u2777</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node6\"><title>4</title>\n",
"<ellipse cx=\"588\" cy=\"-66.4574\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"588\" y=\"-62.7574\">4</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>2-&gt;4</title>\n",
"<path d=\"M479.119,-66.4574C500.691,-66.4574 537.912,-66.4574 562.495,-66.4574\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"569.687,-66.4574 562.687,-69.6075 566.187,-66.4575 562.687,-66.4575 562.687,-66.4575 562.687,-66.4575 566.187,-66.4575 562.687,-63.3075 569.687,-66.4574 569.687,-66.4574\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"497\" y=\"-85.2574\">p0 &amp; !p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"516.5\" y=\"-70.2574\">\u2776</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node5\"><title>3</title>\n",
"<ellipse cx=\"337\" cy=\"-39.4574\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"337\" y=\"-35.7574\">3</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>1-&gt;3</title>\n",
"<path d=\"M214.807,-42.5817C223.034,-41.772 233.013,-40.9084 242,-40.4574 265.599,-39.2731 292.571,-39.1086 311.553,-39.1891\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"318.663,-39.2323 311.644,-42.3396 315.163,-39.211 311.663,-39.1897 311.663,-39.1897 311.663,-39.1897 315.163,-39.211 311.682,-36.0397 318.663,-39.2323 318.663,-39.2323\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242\" y=\"-58.2574\">!p0 &amp; !p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"255.5\" y=\"-44.2574\">\u2776</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"271.5\" y=\"-44.2574\">\u2777</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>3-&gt;0</title>\n",
"<path d=\"M320.425,-31.7687C290.988,-18.1834 225.102,7.71572 169,-2.45745 136.409,-8.36739 100.952,-23.2169 78.8524,-33.5722\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"72.4406,-36.6268 77.4053,-30.7723 75.6003,-35.1214 78.7601,-33.6161 78.7601,-33.6161 78.7601,-33.6161 75.6003,-35.1214 80.1149,-36.4599 72.4406,-36.6268 72.4406,-36.6268\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"169\" y=\"-6.25745\">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=\"M355.038,-39.3705C372.845,-39.7041 401.421,-41.4457 425,-48.4574 429.664,-49.8445 434.442,-51.8529 438.91,-54.0296\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"445.183,-57.2863 437.519,-56.8568 442.077,-55.6737 438.97,-54.0611 438.97,-54.0611 438.97,-54.0611 442.077,-55.6737 440.422,-51.2654 445.183,-57.2863 445.183,-57.2863\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"373\" y=\"-66.2574\">p0 &amp; p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"383\" y=\"-52.2574\">\u24ff</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"399\" y=\"-52.2574\">\u2776</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>4-&gt;2</title>\n",
"<path d=\"M572.689,-56.5917C566.598,-52.964 559.237,-49.2952 552,-47.4574 528.307,-41.4413 520.693,-41.4413 497,-47.4574 492.137,-48.6922 487.219,-50.7535 482.668,-53.0735\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"476.311,-56.5917 480.91,-50.4459 479.374,-54.8968 482.436,-53.202 482.436,-53.202 482.436,-53.202 479.374,-54.8968 483.961,-55.958 476.311,-56.5917 476.311,-56.5917\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"498.5\" y=\"-51.2574\">p0 &amp; p1</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD></TR><TR><TD><svg height=\"178pt\" viewBox=\"0.00 0.00 389.00 178.49\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.800412 0.800412) rotate(0) translate(4 219)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-219 482,-219 482,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"136\" y=\"-200.8\">(Inf(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"161\" y=\"-200.8\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"177\" y=\"-200.8\">)&amp;Inf(</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"213\" y=\"-200.8\">\u2778</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"229\" y=\"-200.8\">)) | Inf(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"269\" y=\"-200.8\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"285\" y=\"-200.8\">) | Inf(</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"322\" y=\"-200.8\">\u2777</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"338\" y=\"-200.8\">)</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
"<ellipse cx=\"56\" cy=\"-75\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-71.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,-75C2.79388,-75 17.1543,-75 30.6317,-75\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"37.9419,-75 30.9419,-78.1501 34.4419,-75 30.9419,-75.0001 30.9419,-75.0001 30.9419,-75.0001 34.4419,-75 30.9418,-71.8501 37.9419,-75 37.9419,-75\" stroke=\"black\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
"<ellipse cx=\"194.5\" cy=\"-43\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"194.5\" y=\"-39.3\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
"<path d=\"M71.3705,-65.0479C77.4707,-61.2955 84.8216,-57.3662 92,-55 117.365,-46.6388 147.991,-43.9613 168.922,-43.1744\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"176.168,-42.963 169.263,-46.3159 172.669,-43.0651 169.171,-43.1673 169.171,-43.1673 169.171,-43.1673 172.669,-43.0651 169.079,-40.0186 176.168,-42.963 176.168,-42.963\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-72.8\">p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"103.5\" y=\"-58.8\">\u24ff</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"119.5\" y=\"-58.8\">\u2776</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node4\"><title>3</title>\n",
"<ellipse cx=\"460\" cy=\"-145\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"460\" y=\"-141.3\">3</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>0-&gt;3</title>\n",
"<path d=\"M70.7219,-85.8091C76.9544,-90.342 84.581,-95.3873 92,-99 122.584,-113.892 132.305,-112.609 165,-122 255.036,-147.861 276.079,-163.126 369,-175 393.247,-178.098 401.074,-183.481 424,-175 430.868,-172.459 437.298,-167.902 442.725,-163.095\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"447.797,-158.27 444.897,-165.377 445.262,-160.682 442.726,-163.094 442.726,-163.094 442.726,-163.094 445.262,-160.682 440.555,-160.812 447.797,-158.27 447.797,-158.27\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"243.5\" y=\"-180.8\">p0 &amp; p1</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"261.5\" y=\"-165.8\">\u2778</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node5\"><title>2</title>\n",
"<ellipse cx=\"333\" cy=\"-75\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"333\" y=\"-71.3\">2</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;2</title>\n",
"<path d=\"M212.526,-42.328C233.105,-42.0426 268.52,-43.2548 297,-53 302.135,-54.7572 307.291,-57.3961 312.007,-60.2424\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"318.122,-64.1889 310.532,-63.0396 315.181,-62.2909 312.24,-60.393 312.24,-60.393 312.24,-60.393 315.181,-62.2909 313.948,-57.7463 318.122,-64.1889 318.122,-64.1889\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242\" y=\"-71.8\">!p0 &amp; p1</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"261.5\" y=\"-56.8\">\u2777</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>3-&gt;2</title>\n",
"<path d=\"M452.579,-128.399C446.934,-116.091 437.498,-99.9565 424,-91 404.504,-78.0639 377.614,-74.721 358.313,-74.2123\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"351.063,-74.1437 358.092,-71.0602 354.562,-74.1769 358.062,-74.21 358.062,-74.21 358.062,-74.21 354.562,-74.1769 358.032,-77.3599 351.063,-74.1437 351.063,-74.1437\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"369\" y=\"-108.8\">p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"380.5\" y=\"-94.8\">\u24ff</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"396.5\" y=\"-94.8\">\u2778</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>2-&gt;0</title>\n",
"<path d=\"M315.397,-79.5979C309.622,-80.9822 303.07,-82.3151 297,-83 206.463,-93.2153 182.537,-93.2153 92,-83 88.3011,-82.5827 84.4234,-81.9247 80.6514,-81.1611\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"73.6032,-79.5979 81.1193,-78.0383 77.0202,-80.3557 80.4372,-81.1136 80.4372,-81.1136 80.4372,-81.1136 77.0202,-80.3557 79.7551,-84.1889 73.6032,-79.5979 73.6032,-79.5979\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"165\" y=\"-107.8\">!p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"170.5\" y=\"-93.8\">\u24ff</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"186.5\" y=\"-93.8\">\u2777</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"202.5\" y=\"-93.8\">\u2778</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>2-&gt;3</title>\n",
"<path d=\"M341.917,-91.1442C347.929,-101.749 357.176,-115.079 369,-123 388.67,-136.178 415.475,-141.475 434.706,-143.597\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"441.676,-144.265 434.407,-146.733 438.192,-143.931 434.708,-143.597 434.708,-143.597 434.708,-143.597 438.192,-143.931 435.008,-140.461 441.676,-144.265 441.676,-144.265\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"370.5\" y=\"-159.8\">p0 &amp; p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388.5\" y=\"-144.8\">\u24ff</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node6\"><title>4</title>\n",
"<ellipse cx=\"460\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"460\" y=\"-14.3\">4</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>2-&gt;4</title>\n",
"<path d=\"M339.532,-57.945C344.819,-44.7266 354.205,-27.3079 369,-19 389.176,-7.67056 416.124,-9.11345 435.26,-12.3433\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"442.18,-13.6458 434.718,-15.4467 438.741,-12.9984 435.301,-12.351 435.301,-12.351 435.301,-12.351 438.741,-12.9984 435.884,-9.25537 442.18,-13.6458 442.18,-13.6458\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"369\" y=\"-22.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>4-&gt;0</title>\n",
"<path d=\"M442.863,-11.8003C437.014,-9.85582 430.296,-7.96604 424,-7 399.838,-3.29256 393.439,-6.46118 369,-7 278.267,-9.00049 254.275,0.324783 165,-16 131.404,-22.1433 121.089,-22.1046 92,-40 85.0513,-44.2748 78.443,-50.1925 72.8781,-55.9466\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"68.0811,-61.1333 70.5215,-53.8554 70.4576,-58.5638 72.8341,-55.9943 72.8341,-55.9943 72.8341,-55.9943 70.4576,-58.5638 75.1467,-58.1331 68.0811,-61.1333 68.0811,-61.1333\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242\" y=\"-10.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=\"M443.368,-25.278C437.336,-28.052 430.366,-31.2148 424,-34 399.726,-44.6205 393.022,-45.8213 369,-57 364.588,-59.0531 359.922,-61.357 355.485,-63.6132\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"349.204,-66.8499 353.983,-60.8433 352.315,-65.2466 355.426,-63.6433 355.426,-63.6433 355.426,-63.6433 352.315,-65.2466 356.869,-66.4434 349.204,-66.8499 349.204,-66.8499\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"369\" y=\"-60.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD><TD><svg height=\"178pt\" viewBox=\"0.00 0.00 389.00 178.49\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.800412 0.800412) rotate(0) translate(4 219)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-219 482,-219 482,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"136\" y=\"-200.8\">(Inf(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"161\" y=\"-200.8\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"177\" y=\"-200.8\">)&amp;Inf(</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"213\" y=\"-200.8\">\u2778</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"229\" y=\"-200.8\">)) | Inf(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"269\" y=\"-200.8\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"285\" y=\"-200.8\">) | Inf(</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"322\" y=\"-200.8\">\u2777</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"338\" y=\"-200.8\">)</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
"<ellipse cx=\"56\" cy=\"-75\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-71.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,-75C2.79388,-75 17.1543,-75 30.6317,-75\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"37.9419,-75 30.9419,-78.1501 34.4419,-75 30.9419,-75.0001 30.9419,-75.0001 30.9419,-75.0001 34.4419,-75 30.9418,-71.8501 37.9419,-75 37.9419,-75\" stroke=\"black\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
"<ellipse cx=\"194.5\" cy=\"-43\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"194.5\" y=\"-39.3\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
"<path d=\"M71.3705,-65.0479C77.4707,-61.2955 84.8216,-57.3662 92,-55 117.365,-46.6388 147.991,-43.9613 168.922,-43.1744\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"176.168,-42.963 169.263,-46.3159 172.669,-43.0651 169.171,-43.1673 169.171,-43.1673 169.171,-43.1673 172.669,-43.0651 169.079,-40.0186 176.168,-42.963 176.168,-42.963\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-72.8\">p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"103.5\" y=\"-58.8\">\u24ff</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"119.5\" y=\"-58.8\">\u2776</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node4\"><title>3</title>\n",
"<ellipse cx=\"460\" cy=\"-145\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"460\" y=\"-141.3\">3</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>0-&gt;3</title>\n",
"<path d=\"M70.7219,-85.8091C76.9544,-90.342 84.581,-95.3873 92,-99 122.584,-113.892 132.305,-112.609 165,-122 255.036,-147.861 276.079,-163.126 369,-175 393.247,-178.098 401.074,-183.481 424,-175 430.868,-172.459 437.298,-167.902 442.725,-163.095\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"447.797,-158.27 444.897,-165.377 445.262,-160.682 442.726,-163.094 442.726,-163.094 442.726,-163.094 445.262,-160.682 440.555,-160.812 447.797,-158.27 447.797,-158.27\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"243.5\" y=\"-180.8\">p0 &amp; p1</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"261.5\" y=\"-165.8\">\u2778</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node5\"><title>2</title>\n",
"<ellipse cx=\"333\" cy=\"-75\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"333\" y=\"-71.3\">2</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;2</title>\n",
"<path d=\"M212.526,-42.328C233.105,-42.0426 268.52,-43.2548 297,-53 302.135,-54.7572 307.291,-57.3961 312.007,-60.2424\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"318.122,-64.1889 310.532,-63.0396 315.181,-62.2909 312.24,-60.393 312.24,-60.393 312.24,-60.393 315.181,-62.2909 313.948,-57.7463 318.122,-64.1889 318.122,-64.1889\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242\" y=\"-71.8\">!p0 &amp; p1</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"261.5\" y=\"-56.8\">\u2777</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>3-&gt;2</title>\n",
"<path d=\"M452.579,-128.399C446.934,-116.091 437.498,-99.9565 424,-91 404.504,-78.0639 377.614,-74.721 358.313,-74.2123\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"351.063,-74.1437 358.092,-71.0602 354.562,-74.1769 358.062,-74.21 358.062,-74.21 358.062,-74.21 354.562,-74.1769 358.032,-77.3599 351.063,-74.1437 351.063,-74.1437\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"369\" y=\"-108.8\">p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"380.5\" y=\"-94.8\">\u24ff</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"396.5\" y=\"-94.8\">\u2778</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>2-&gt;0</title>\n",
"<path d=\"M315.397,-79.5979C309.622,-80.9822 303.07,-82.3151 297,-83 206.463,-93.2153 182.537,-93.2153 92,-83 88.3011,-82.5827 84.4234,-81.9247 80.6514,-81.1611\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"73.6032,-79.5979 81.1193,-78.0383 77.0202,-80.3557 80.4372,-81.1136 80.4372,-81.1136 80.4372,-81.1136 77.0202,-80.3557 79.7551,-84.1889 73.6032,-79.5979 73.6032,-79.5979\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"165\" y=\"-107.8\">!p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"170.5\" y=\"-93.8\">\u24ff</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"186.5\" y=\"-93.8\">\u2777</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"202.5\" y=\"-93.8\">\u2778</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>2-&gt;3</title>\n",
"<path d=\"M341.917,-91.1442C347.929,-101.749 357.176,-115.079 369,-123 388.67,-136.178 415.475,-141.475 434.706,-143.597\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"441.676,-144.265 434.407,-146.733 438.192,-143.931 434.708,-143.597 434.708,-143.597 434.708,-143.597 438.192,-143.931 435.008,-140.461 441.676,-144.265 441.676,-144.265\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"370.5\" y=\"-159.8\">p0 &amp; p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388.5\" y=\"-144.8\">\u24ff</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node6\"><title>4</title>\n",
"<ellipse cx=\"460\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"460\" y=\"-14.3\">4</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>2-&gt;4</title>\n",
"<path d=\"M339.532,-57.945C344.819,-44.7266 354.205,-27.3079 369,-19 389.176,-7.67056 416.124,-9.11345 435.26,-12.3433\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"442.18,-13.6458 434.718,-15.4467 438.741,-12.9984 435.301,-12.351 435.301,-12.351 435.301,-12.351 438.741,-12.9984 435.884,-9.25537 442.18,-13.6458 442.18,-13.6458\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"369\" y=\"-22.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>4-&gt;0</title>\n",
"<path d=\"M442.863,-11.8003C437.014,-9.85582 430.296,-7.96604 424,-7 399.838,-3.29256 393.439,-6.46118 369,-7 278.267,-9.00049 254.275,0.324783 165,-16 131.404,-22.1433 121.089,-22.1046 92,-40 85.0513,-44.2748 78.443,-50.1925 72.8781,-55.9466\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"68.0811,-61.1333 70.5215,-53.8554 70.4576,-58.5638 72.8341,-55.9943 72.8341,-55.9943 72.8341,-55.9943 70.4576,-58.5638 75.1467,-58.1331 68.0811,-61.1333 68.0811,-61.1333\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242\" y=\"-10.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=\"M443.368,-25.278C437.336,-28.052 430.366,-31.2148 424,-34 399.726,-44.6205 393.022,-45.8213 369,-57 364.588,-59.0531 359.922,-61.357 355.485,-63.6132\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"349.204,-66.8499 353.983,-60.8433 352.315,-65.2466 355.426,-63.6433 355.426,-63.6433 355.426,-63.6433 352.315,-65.2466 356.869,-66.4434 349.204,-66.8499 349.204,-66.8499\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"369\" y=\"-60.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD></TR><TR><TD><svg height=\"82pt\" viewBox=\"0.00 0.00 389.00 81.93\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.606864 0.606864) rotate(0) translate(4 131)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-131 637,-131 637,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"203\" y=\"-112.8\">((Inf(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"232\" y=\"-112.8\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"248\" y=\"-112.8\">) | Fin(</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"288\" y=\"-112.8\">\u2777</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"304\" y=\"-112.8\">)) &amp; Inf(</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"351\" y=\"-112.8\">\u2778</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"367\" y=\"-112.8\">)) | Fin(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"410\" y=\"-112.8\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"426\" y=\"-112.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",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node3\"><title>3</title>\n",
"<ellipse cx=\"188\" cy=\"-61\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"188\" y=\"-57.3\">3</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>0-&gt;3</title>\n",
"<path d=\"M73.2017,-23.359C95.9724,-30.8909 137.572,-44.6506 163.672,-53.2838\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"170.594,-55.5734 162.959,-56.3658 167.271,-54.4743 163.948,-53.3751 163.948,-53.3751 163.948,-53.3751 167.271,-54.4743 164.937,-50.3845 170.594,-55.5734 170.594,-55.5734\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-48.8\">p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
"<ellipse cx=\"332.5\" cy=\"-28\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"332.5\" y=\"-24.3\">2</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
"<path d=\"M74.026,-15.0227C94.7379,-11.5648 130.805,-6.07052 162,-4 217.733,-0.300864 232.364,-5.39555 287,-17 293.746,-18.4328 301.024,-20.156 307.7,-21.8088\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"314.656,-23.5576 307.099,-24.9056 311.261,-22.7041 307.867,-21.8506 307.867,-21.8506 307.867,-21.8506 311.261,-22.7041 308.635,-18.7957 314.656,-23.5576 314.656,-23.5576\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"162\" y=\"-22.8\">p0 &amp; p1</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"180\" y=\"-7.8\">\u2778</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>3-&gt;2</title>\n",
"<path d=\"M206.126,-58.285C225.788,-55.0282 258.944,-49.1086 287,-42 293.919,-40.247 301.347,-38.0419 308.115,-35.9037\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"315.143,-33.6343 309.45,-38.7828 311.813,-34.7097 308.482,-35.7852 308.482,-35.7852 308.482,-35.7852 311.813,-34.7097 307.514,-32.7875 315.143,-33.6343 315.143,-33.6343\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"232\" y=\"-56.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>2-&gt;3</title>\n",
"<path d=\"M314.749,-24.4729C294.515,-20.9628 259.74,-17.358 232,-27 222.401,-30.3365 213.328,-36.805 206.013,-43.2123\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"200.782,-48.0472 203.785,-40.9826 203.352,-45.6715 205.923,-43.2959 205.923,-43.2959 205.923,-43.2959 203.352,-45.6715 208.061,-45.6092 200.782,-48.0472 200.782,-48.0472\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"232\" y=\"-30.8\">p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node5\"><title>1</title>\n",
"<ellipse cx=\"478.5\" cy=\"-86\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"478.5\" y=\"-82.3\">1</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>2-&gt;1</title>\n",
"<path d=\"M349.866,-33.6055C369.721,-40.516 404.124,-52.8433 433,-65 440.322,-68.0826 448.197,-71.697 455.257,-75.0499\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"461.994,-78.2863 454.321,-78.0946 458.84,-76.7708 455.685,-75.2552 455.685,-75.2552 455.685,-75.2552 458.84,-76.7708 457.049,-72.4158 461.994,-78.2863 461.994,-78.2863\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"378\" y=\"-68.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;3</title>\n",
"<path d=\"M460.416,-86.1573C420.292,-86.2811 317.008,-85.1699 232,-72 225.651,-71.0164 218.877,-69.5067 212.627,-67.9179\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"205.589,-66.0433 213.164,-64.8012 208.971,-66.9442 212.353,-67.8451 212.353,-67.8451 212.353,-67.8451 208.971,-66.9442 211.543,-70.8889 205.589,-66.0433 205.589,-66.0433\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"305\" y=\"-86.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node6\"><title>4</title>\n",
"<ellipse cx=\"615\" cy=\"-61\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"615\" y=\"-57.3\">4</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>1-&gt;4</title>\n",
"<path d=\"M493.591,-76.1081C501.997,-70.8108 513.122,-64.8108 524,-62 545.71,-56.3903 571.36,-56.7554 589.712,-58.1596\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"597.097,-58.8106 589.848,-61.3337 593.611,-58.5032 590.124,-58.1958 590.124,-58.1958 590.124,-58.1958 593.611,-58.5032 590.401,-55.058 597.097,-58.8106 597.097,-58.8106\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"525.5\" y=\"-65.8\">p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>4-&gt;2</title>\n",
"<path d=\"M597.336,-56.8259C591.556,-55.4754 585.017,-54.0556 579,-53 498.622,-38.8971 401.94,-31.9403 357.717,-29.3032\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"350.581,-28.8883 357.753,-26.15 354.076,-29.0915 357.57,-29.2947 357.57,-29.2947 357.57,-29.2947 354.076,-29.0915 357.387,-32.4394 350.581,-28.8883 350.581,-28.8883\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"451\" y=\"-45.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=\"M598.739,-69.338C592.751,-72.2422 585.716,-75.2171 579,-77 553.917,-83.6591 524.164,-85.6085 503.77,-86.0789\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"496.705,-86.1912 503.654,-82.9302 500.205,-86.1355 503.704,-86.0798 503.704,-86.0798 503.704,-86.0798 500.205,-86.1355 503.754,-89.2294 496.705,-86.1912 496.705,-86.1912\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"524\" y=\"-88.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD><TD><svg height=\"83pt\" viewBox=\"0.00 0.00 389.00 83.14\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.606864 0.606864) rotate(0) translate(4 133)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-133 637,-133 637,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"313.5\" y=\"-113.8\">t</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",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node3\"><title>3</title>\n",
"<ellipse cx=\"188\" cy=\"-56\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"188\" y=\"-52.3\">3</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>0-&gt;3</title>\n",
"<path d=\"M73.4646,-22.8127C96.1968,-29.4575 137.33,-41.481 163.348,-49.0865\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"170.258,-51.1063 162.656,-52.1658 166.899,-50.1243 163.54,-49.1423 163.54,-49.1423 163.54,-49.1423 166.899,-50.1243 164.423,-46.1188 170.258,-51.1063 170.258,-51.1063\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-45.8\">p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
"<ellipse cx=\"332.5\" cy=\"-30\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"332.5\" y=\"-26.3\">2</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
"<path d=\"M74.1567,-16.492C112.559,-13.4774 208.248,-7.9748 287,-20 293.783,-21.0358 301.073,-22.5161 307.749,-24.0215\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"314.7,-25.6448 307.167,-27.1202 311.292,-24.8488 307.883,-24.0527 307.883,-24.0527 307.883,-24.0527 311.292,-24.8488 308.6,-20.9853 314.7,-25.6448 314.7,-25.6448\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"162\" y=\"-17.8\">p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>3-&gt;2</title>\n",
"<path d=\"M206.154,-54.8547C225.843,-53.3204 259.023,-50.0602 287,-44 293.975,-42.489 301.422,-40.3593 308.188,-38.2159\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"315.209,-35.9133 309.539,-41.0879 311.883,-37.004 308.558,-38.0948 308.558,-38.0948 308.558,-38.0948 311.883,-37.004 307.576,-35.1016 315.209,-35.9133 315.209,-35.9133\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"232\" y=\"-55.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>2-&gt;3</title>\n",
"<path d=\"M314.556,-26.9332C294.432,-23.9454 260.055,-20.9221 232,-29 223.699,-31.3902 215.452,-35.9071 208.434,-40.5722\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"202.368,-44.8414 206.279,-38.2365 205.23,-42.8269 208.092,-40.8124 208.092,-40.8124 208.092,-40.8124 205.23,-42.8269 209.905,-43.3884 202.368,-44.8414 202.368,-44.8414\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"232\" y=\"-32.8\">p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node5\"><title>1</title>\n",
"<ellipse cx=\"478.5\" cy=\"-88\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"478.5\" y=\"-84.3\">1</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>2-&gt;1</title>\n",
"<path d=\"M349.866,-35.6055C369.721,-42.516 404.124,-54.8433 433,-67 440.322,-70.0826 448.197,-73.697 455.257,-77.0499\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"461.994,-80.2863 454.321,-80.0946 458.84,-78.7708 455.685,-77.2552 455.685,-77.2552 455.685,-77.2552 458.84,-78.7708 457.049,-74.4158 461.994,-80.2863 461.994,-80.2863\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"378\" y=\"-70.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;3</title>\n",
"<path d=\"M460.317,-88.4042C419.981,-89.0089 316.278,-88.5601 232,-71 225.293,-69.6025 218.199,-67.4323 211.749,-65.1727\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"205.052,-62.7181 212.709,-62.1695 208.338,-63.9226 211.625,-65.1271 211.625,-65.1271 211.625,-65.1271 208.338,-63.9226 210.541,-68.0847 205.052,-62.7181 205.052,-62.7181\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"305\" y=\"-89.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node6\"><title>4</title>\n",
"<ellipse cx=\"615\" cy=\"-63\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"615\" y=\"-59.3\">4</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>1-&gt;4</title>\n",
"<path d=\"M493.591,-78.1081C501.997,-72.8108 513.122,-66.8108 524,-64 545.71,-58.3903 571.36,-58.7554 589.712,-60.1596\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"597.097,-60.8106 589.848,-63.3337 593.611,-60.5032 590.124,-60.1958 590.124,-60.1958 590.124,-60.1958 593.611,-60.5032 590.401,-57.058 597.097,-60.8106 597.097,-60.8106\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"525.5\" y=\"-67.8\">p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>4-&gt;2</title>\n",
"<path d=\"M597.336,-58.8259C591.556,-57.4754 585.017,-56.0556 579,-55 498.622,-40.8971 401.94,-33.9403 357.717,-31.3032\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"350.581,-30.8883 357.753,-28.15 354.076,-31.0915 357.57,-31.2947 357.57,-31.2947 357.57,-31.2947 354.076,-31.0915 357.387,-34.4394 350.581,-30.8883 350.581,-30.8883\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"451\" y=\"-47.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=\"M598.739,-71.338C592.751,-74.2422 585.716,-77.2171 579,-79 553.917,-85.6591 524.164,-87.6085 503.77,-88.0789\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"496.705,-88.1912 503.654,-84.9302 500.205,-88.1355 503.704,-88.0798 503.704,-88.0798 503.704,-88.0798 500.205,-88.1355 503.754,-91.2294 496.705,-88.1912 496.705,-88.1912\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"524\" y=\"-90.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD></TR><TR><TD><svg height=\"104pt\" viewBox=\"0.00 0.00 389.00 104.32\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.628433 0.628433) rotate(0) translate(4 162)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-162 615,-162 615,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"196\" y=\"-143.8\">(Fin(</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"224\" y=\"-143.8\">\u2778</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"240\" y=\"-143.8\">) &amp; Inf(</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"283\" y=\"-143.8\">\u2777</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"299\" y=\"-143.8\">)) | Fin(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"342\" y=\"-143.8\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"358\" y=\"-143.8\">) | Inf(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"395\" y=\"-143.8\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"411\" y=\"-143.8\">)</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
"<ellipse cx=\"56\" cy=\"-33\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-29.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,-33C2.79388,-33 17.1543,-33 30.6317,-33\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"37.9419,-33 30.9419,-36.1501 34.4419,-33 30.9419,-33.0001 30.9419,-33.0001 30.9419,-33.0001 34.4419,-33 30.9418,-29.8501 37.9419,-33 37.9419,-33\" stroke=\"black\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
"<ellipse cx=\"180\" cy=\"-79\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"180\" y=\"-75.3\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
"<path d=\"M69.2107,-45.7202C75.4914,-51.5403 83.585,-58.0132 92,-62 111.836,-71.3978 136.574,-75.6007 154.595,-77.4802\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"161.873,-78.1518 154.613,-80.6451 158.387,-77.8301 154.902,-77.5085 154.902,-77.5085 154.902,-77.5085 158.387,-77.8301 155.192,-74.3718 161.873,-78.1518 161.873,-78.1518\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-78.8\">p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;0</title>\n",
"<path d=\"M172.212,-62.5446C166.525,-51.1261 157.2,-36.7928 144,-30 124.307,-19.8656 98.6507,-22.3171 80.3119,-26.266\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"73.4267,-27.8918 79.5154,-23.2174 76.833,-27.0874 80.2394,-26.2831 80.2394,-26.2831 80.2394,-26.2831 76.833,-27.0874 80.9633,-29.3487 73.4267,-27.8918 73.4267,-27.8918\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-47.8\">p0 &amp; p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"102\" y=\"-33.8\">\u2776</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"118\" y=\"-33.8\">\u2778</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
"<ellipse cx=\"316.5\" cy=\"-79\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"316.5\" y=\"-75.3\">2</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>1-&gt;2</title>\n",
"<path d=\"M198.035,-79C221.554,-79 264.11,-79 291.03,-79\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"298.179,-79 291.179,-82.1501 294.679,-79 291.179,-79.0001 291.179,-79.0001 291.179,-79.0001 294.679,-79 291.179,-75.8501 298.179,-79 298.179,-79\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"216\" y=\"-82.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node5\"><title>4</title>\n",
"<ellipse cx=\"458\" cy=\"-112\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"458\" y=\"-108.3\">4</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>2-&gt;4</title>\n",
"<path d=\"M333.36,-85.4367C341.763,-88.6593 352.323,-92.4143 362,-95 385.827,-101.367 413.661,-106.032 433.017,-108.848\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"439.994,-109.836 432.622,-111.973 436.529,-109.345 433.063,-108.855 433.063,-108.855 433.063,-108.855 436.529,-109.345 433.505,-105.736 439.994,-109.836 439.994,-109.836\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"362\" y=\"-123.8\">p0 &amp; p1</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"380\" y=\"-108.8\">\u2777</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>4-&gt;2</title>\n",
"<path d=\"M445.717,-98.666C437.803,-90.3994 426.445,-80.5218 414,-76 390.288,-67.3844 361.1,-69.937 341.073,-73.5033\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"334.135,-74.8443 340.41,-70.4229 337.572,-74.18 341.008,-73.5157 341.008,-73.5157 341.008,-73.5157 337.572,-74.18 341.606,-76.6084 334.135,-74.8443 334.135,-74.8443\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"362\" y=\"-79.8\">p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node6\"><title>3</title>\n",
"<ellipse cx=\"593\" cy=\"-46\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"593\" y=\"-42.3\">3</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>4-&gt;3</title>\n",
"<path d=\"M474.517,-104.3C498.143,-92.5758 543.224,-70.2046 570.151,-56.8423\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"576.582,-53.6512 571.712,-59.5845 573.447,-55.207 570.311,-56.7628 570.311,-56.7628 570.311,-56.7628 573.447,-55.207 568.911,-53.9412 576.582,-53.6512 576.582,-53.6512\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"502\" y=\"-93.8\">p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>3-&gt;0</title>\n",
"<path d=\"M577.024,-37.1307C552.995,-23.7637 503.955,-7.10543e-15 459,-0 179,-0 179,-0 179,-0 139.514,-2.41779e-15 129.67,-6.16328 92,-18 87.6956,-19.3526 83.1986,-21.0501 78.9177,-22.8125\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"72.4271,-25.5951 77.6195,-19.9417 75.644,-24.216 78.8608,-22.8368 78.8608,-22.8368 78.8608,-22.8368 75.644,-24.216 80.102,-25.732 72.4271,-25.5951 72.4271,-25.5951\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"289\" y=\"-3.8\">p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>3-&gt;2</title>\n",
"<path d=\"M574.738,-45.9421C536.125,-46.1497 440.034,-48.5463 362,-66 355.078,-67.5482 347.649,-69.571 340.881,-71.5582\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"333.853,-73.6764 339.646,-68.6404 337.204,-72.6664 340.555,-71.6564 340.555,-71.6564 340.555,-71.6564 337.204,-72.6664 341.464,-74.6724 333.853,-73.6764 333.853,-73.6764\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"432\" y=\"-72.8\">p0 &amp; p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"450\" y=\"-57.8\">\u2776</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD><TD><svg height=\"104pt\" viewBox=\"0.00 0.00 389.00 104.32\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.628433 0.628433) rotate(0) translate(4 162)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-162 615,-162 615,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"222.5\" y=\"-143.8\">(Fin(</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"250.5\" y=\"-143.8\">\u2777</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"266.5\" y=\"-143.8\">) &amp; Inf(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"309.5\" y=\"-143.8\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"325.5\" y=\"-143.8\">)) | Fin(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"368.5\" y=\"-143.8\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"384.5\" y=\"-143.8\">)</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
"<ellipse cx=\"56\" cy=\"-33\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-29.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,-33C2.79388,-33 17.1543,-33 30.6317,-33\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"37.9419,-33 30.9419,-36.1501 34.4419,-33 30.9419,-33.0001 30.9419,-33.0001 30.9419,-33.0001 34.4419,-33 30.9418,-29.8501 37.9419,-33 37.9419,-33\" stroke=\"black\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
"<ellipse cx=\"180\" cy=\"-79\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"180\" y=\"-75.3\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
"<path d=\"M69.2107,-45.7202C75.4914,-51.5403 83.585,-58.0132 92,-62 111.836,-71.3978 136.574,-75.6007 154.595,-77.4802\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"161.873,-78.1518 154.613,-80.6451 158.387,-77.8301 154.902,-77.5085 154.902,-77.5085 154.902,-77.5085 158.387,-77.8301 155.192,-74.3718 161.873,-78.1518 161.873,-78.1518\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-78.8\">p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;0</title>\n",
"<path d=\"M172.212,-62.5446C166.525,-51.1261 157.2,-36.7928 144,-30 124.307,-19.8656 98.6507,-22.3171 80.3119,-26.266\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"73.4267,-27.8918 79.5154,-23.2174 76.833,-27.0874 80.2394,-26.2831 80.2394,-26.2831 80.2394,-26.2831 76.833,-27.0874 80.9633,-29.3487 73.4267,-27.8918 73.4267,-27.8918\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-47.8\">p0 &amp; p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"102\" y=\"-33.8\">\u24ff</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"118\" y=\"-33.8\">\u2777</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
"<ellipse cx=\"316.5\" cy=\"-79\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"316.5\" y=\"-75.3\">2</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>1-&gt;2</title>\n",
"<path d=\"M198.035,-79C221.554,-79 264.11,-79 291.03,-79\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"298.179,-79 291.179,-82.1501 294.679,-79 291.179,-79.0001 291.179,-79.0001 291.179,-79.0001 294.679,-79 291.179,-75.8501 298.179,-79 298.179,-79\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"216\" y=\"-82.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node5\"><title>4</title>\n",
"<ellipse cx=\"458\" cy=\"-112\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"458\" y=\"-108.3\">4</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>2-&gt;4</title>\n",
"<path d=\"M333.36,-85.4367C341.763,-88.6593 352.323,-92.4143 362,-95 385.827,-101.367 413.661,-106.032 433.017,-108.848\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"439.994,-109.836 432.622,-111.973 436.529,-109.345 433.063,-108.855 433.063,-108.855 433.063,-108.855 436.529,-109.345 433.505,-105.736 439.994,-109.836 439.994,-109.836\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"362\" y=\"-123.8\">p0 &amp; p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"380\" y=\"-108.8\">\u2776</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>4-&gt;2</title>\n",
"<path d=\"M445.717,-98.666C437.803,-90.3994 426.445,-80.5218 414,-76 390.288,-67.3844 361.1,-69.937 341.073,-73.5033\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"334.135,-74.8443 340.41,-70.4229 337.572,-74.18 341.008,-73.5157 341.008,-73.5157 341.008,-73.5157 337.572,-74.18 341.606,-76.6084 334.135,-74.8443 334.135,-74.8443\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"362\" y=\"-79.8\">p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node6\"><title>3</title>\n",
"<ellipse cx=\"593\" cy=\"-46\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"593\" y=\"-42.3\">3</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>4-&gt;3</title>\n",
"<path d=\"M474.517,-104.3C498.143,-92.5758 543.224,-70.2046 570.151,-56.8423\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"576.582,-53.6512 571.712,-59.5845 573.447,-55.207 570.311,-56.7628 570.311,-56.7628 570.311,-56.7628 573.447,-55.207 568.911,-53.9412 576.582,-53.6512 576.582,-53.6512\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"502\" y=\"-93.8\">p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>3-&gt;0</title>\n",
"<path d=\"M577.024,-37.1307C552.995,-23.7637 503.955,-7.10543e-15 459,-0 179,-0 179,-0 179,-0 139.514,-2.41779e-15 129.67,-6.16328 92,-18 87.6956,-19.3526 83.1986,-21.0501 78.9177,-22.8125\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"72.4271,-25.5951 77.6195,-19.9417 75.644,-24.216 78.8608,-22.8368 78.8608,-22.8368 78.8608,-22.8368 75.644,-24.216 80.102,-25.732 72.4271,-25.5951 72.4271,-25.5951\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"289\" y=\"-3.8\">p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>3-&gt;2</title>\n",
"<path d=\"M574.738,-45.9421C536.125,-46.1497 440.034,-48.5463 362,-66 355.078,-67.5482 347.649,-69.571 340.881,-71.5582\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"333.853,-73.6764 339.646,-68.6404 337.204,-72.6664 340.555,-71.6564 340.555,-71.6564 340.555,-71.6564 337.204,-72.6664 341.464,-74.6724 333.853,-73.6764 333.853,-73.6764\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"432\" y=\"-72.8\">p0 &amp; p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"450\" y=\"-57.8\">\u24ff</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD></TR><TR><TD><svg height=\"93pt\" viewBox=\"0.00 0.00 389.00 93.08\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.641914 0.641914) rotate(0) translate(4 141)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-141 602,-141 602,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"189\" y=\"-122.8\">(Inf(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"214\" y=\"-122.8\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"230\" y=\"-122.8\">) | (Inf(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"270\" y=\"-122.8\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"286\" y=\"-122.8\">)&amp;Inf(</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"322\" y=\"-122.8\">\u2778</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"338\" y=\"-122.8\">))) &amp; Inf(</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"389\" y=\"-122.8\">\u2777</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"405\" y=\"-122.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",
"<!-- 0&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>0-&gt;0</title>\n",
"<path d=\"M49.6208,-36.0373C48.3189,-45.8579 50.4453,-55 56,-55 60.166,-55 62.4036,-49.8576 62.7128,-43.1433\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"62.3792,-36.0373 65.8541,-42.8818 62.5434,-39.5335 62.7076,-43.0296 62.7076,-43.0296 62.7076,-43.0296 62.5434,-39.5335 59.561,-43.1774 62.3792,-36.0373 62.3792,-36.0373\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"26.5\" y=\"-58.8\">!p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node3\"><title>4</title>\n",
"<ellipse cx=\"183\" cy=\"-48\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"183\" y=\"-44.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.599,-22.851C95.359,-27.8993 133.663,-36.7858 158.424,-42.5304\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"165.332,-44.1331 157.801,-45.6195 161.923,-43.3421 158.513,-42.551 158.513,-42.551 158.513,-42.551 161.923,-43.3421 159.225,-39.4825 165.332,-44.1331 165.332,-44.1331\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-42.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>4-&gt;4</title>\n",
"<path d=\"M172.627,-62.7917C169.249,-73.4165 172.707,-84 183,-84 190.881,-84 194.754,-77.7961 194.622,-70.1197\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"193.373,-62.7917 197.654,-69.1632 193.961,-66.242 194.549,-69.6923 194.549,-69.6923 194.549,-69.6923 193.961,-66.242 191.444,-70.2213 193.373,-62.7917 193.373,-62.7917\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"155.5\" y=\"-102.8\">!p0 &amp; p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"175\" y=\"-87.8\">\u2776</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node6\"><title>2</title>\n",
"<ellipse cx=\"319.5\" cy=\"-51\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"319.5\" y=\"-47.3\">2</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>4-&gt;2</title>\n",
"<path d=\"M201.035,-48.38C224.554,-48.9045 267.11,-49.8538 294.03,-50.4542\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"301.179,-50.6137 294.11,-53.6067 297.68,-50.5356 294.181,-50.4575 294.181,-50.4575 294.181,-50.4575 297.68,-50.5356 294.251,-47.3082 301.179,-50.6137 301.179,-50.6137\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"219\" y=\"-67.8\">!p0 &amp; p1</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238.5\" y=\"-52.8\">\u2778</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node4\"><title>1</title>\n",
"<ellipse cx=\"453\" cy=\"-47\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"453\" y=\"-43.3\">1</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node5\"><title>3</title>\n",
"<ellipse cx=\"580\" cy=\"-20\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"580\" y=\"-16.3\">3</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;3</title>\n",
"<path d=\"M470.858,-43.3587C492.572,-38.6685 530.446,-30.4876 555.118,-25.1586\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"562.01,-23.6699 555.833,-28.2269 558.589,-24.4089 555.168,-25.1479 555.168,-25.1479 555.168,-25.1479 558.589,-24.4089 554.503,-22.0689 562.01,-23.6699 562.01,-23.6699\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"489\" y=\"-57.8\">!p0 &amp; p1</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"508.5\" y=\"-42.8\">\u2777</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>3-&gt;0</title>\n",
"<path d=\"M562.153,-15.5614C538.271,-9.66919 493.12,-0 454,-0 182,-0 182,-0 182,-0 146.438,-0 105.825,-7.60932 80.7964,-13.1969\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"73.8598,-14.7833 79.9814,-10.1519 77.2717,-14.003 80.6837,-13.2226 80.6837,-13.2226 80.6837,-13.2226 77.2717,-14.003 81.3859,-16.2934 73.8598,-14.7833 73.8598,-14.7833\" 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",
"<!-- 2&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>2-&gt;1</title>\n",
"<path d=\"M337.691,-50.4771C360.629,-49.7793 401.381,-48.5397 427.522,-47.7446\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"434.804,-47.5231 427.904,-50.8845 431.306,-47.6295 427.808,-47.736 427.808,-47.736 427.808,-47.736 431.306,-47.6295 427.712,-44.5874 434.804,-47.5231 434.804,-47.5231\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"365\" y=\"-67.8\">p0 &amp; p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"383\" y=\"-52.8\">\u24ff</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD><TD><svg height=\"93pt\" viewBox=\"0.00 0.00 389.00 93.08\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.641914 0.641914) rotate(0) translate(4 141)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-141 602,-141 602,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"189\" y=\"-122.8\">(Inf(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"214\" y=\"-122.8\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"230\" y=\"-122.8\">) | (Inf(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"270\" y=\"-122.8\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"286\" y=\"-122.8\">)&amp;Inf(</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"322\" y=\"-122.8\">\u2778</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"338\" y=\"-122.8\">))) &amp; Inf(</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"389\" y=\"-122.8\">\u2777</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"405\" y=\"-122.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",
"<!-- 0&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>0-&gt;0</title>\n",
"<path d=\"M49.6208,-36.0373C48.3189,-45.8579 50.4453,-55 56,-55 60.166,-55 62.4036,-49.8576 62.7128,-43.1433\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"62.3792,-36.0373 65.8541,-42.8818 62.5434,-39.5335 62.7076,-43.0296 62.7076,-43.0296 62.7076,-43.0296 62.5434,-39.5335 59.561,-43.1774 62.3792,-36.0373 62.3792,-36.0373\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"26.5\" y=\"-58.8\">!p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node3\"><title>4</title>\n",
"<ellipse cx=\"183\" cy=\"-48\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"183\" y=\"-44.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.599,-22.851C95.359,-27.8993 133.663,-36.7858 158.424,-42.5304\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"165.332,-44.1331 157.801,-45.6195 161.923,-43.3421 158.513,-42.551 158.513,-42.551 158.513,-42.551 161.923,-43.3421 159.225,-39.4825 165.332,-44.1331 165.332,-44.1331\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-42.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>4-&gt;4</title>\n",
"<path d=\"M172.627,-62.7917C169.249,-73.4165 172.707,-84 183,-84 190.881,-84 194.754,-77.7961 194.622,-70.1197\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"193.373,-62.7917 197.654,-69.1632 193.961,-66.242 194.549,-69.6923 194.549,-69.6923 194.549,-69.6923 193.961,-66.242 191.444,-70.2213 193.373,-62.7917 193.373,-62.7917\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"155.5\" y=\"-102.8\">!p0 &amp; p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"175\" y=\"-87.8\">\u2776</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node6\"><title>2</title>\n",
"<ellipse cx=\"319.5\" cy=\"-51\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"319.5\" y=\"-47.3\">2</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>4-&gt;2</title>\n",
"<path d=\"M201.035,-48.38C224.554,-48.9045 267.11,-49.8538 294.03,-50.4542\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"301.179,-50.6137 294.11,-53.6067 297.68,-50.5356 294.181,-50.4575 294.181,-50.4575 294.181,-50.4575 297.68,-50.5356 294.251,-47.3082 301.179,-50.6137 301.179,-50.6137\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"219\" y=\"-67.8\">!p0 &amp; p1</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238.5\" y=\"-52.8\">\u2778</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node4\"><title>1</title>\n",
"<ellipse cx=\"453\" cy=\"-47\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"453\" y=\"-43.3\">1</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node5\"><title>3</title>\n",
"<ellipse cx=\"580\" cy=\"-20\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"580\" y=\"-16.3\">3</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;3</title>\n",
"<path d=\"M470.858,-43.3587C492.572,-38.6685 530.446,-30.4876 555.118,-25.1586\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"562.01,-23.6699 555.833,-28.2269 558.589,-24.4089 555.168,-25.1479 555.168,-25.1479 555.168,-25.1479 558.589,-24.4089 554.503,-22.0689 562.01,-23.6699 562.01,-23.6699\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"489\" y=\"-57.8\">!p0 &amp; p1</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"508.5\" y=\"-42.8\">\u2777</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>3-&gt;0</title>\n",
"<path d=\"M562.153,-15.5614C538.271,-9.66919 493.12,-0 454,-0 182,-0 182,-0 182,-0 146.438,-0 105.825,-7.60932 80.7964,-13.1969\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"73.8598,-14.7833 79.9814,-10.1519 77.2717,-14.003 80.6837,-13.2226 80.6837,-13.2226 80.6837,-13.2226 77.2717,-14.003 81.3859,-16.2934 73.8598,-14.7833 73.8598,-14.7833\" 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",
"<!-- 2&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>2-&gt;1</title>\n",
"<path d=\"M337.691,-50.4771C360.629,-49.7793 401.381,-48.5397 427.522,-47.7446\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"434.804,-47.5231 427.904,-50.8845 431.306,-47.6295 427.808,-47.736 427.808,-47.736 427.808,-47.736 431.306,-47.6295 427.712,-44.5874 434.804,-47.5231 434.804,-47.5231\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"365\" y=\"-67.8\">p0 &amp; p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"383\" y=\"-52.8\">\u24ff</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD></TR><TR><TD><svg height=\"76pt\" viewBox=\"0.00 0.00 389.00 75.95\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.660441 0.660441) rotate(0) translate(4 111)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-111 585,-111 585,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"174\" y=\"-92.8\">((Fin(</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"206\" y=\"-92.8\">\u2777</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"222\" y=\"-92.8\">) &amp; Inf(</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"265\" y=\"-92.8\">\u2778</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"281\" y=\"-92.8\">)) | Inf(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"321\" y=\"-92.8\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"337\" y=\"-92.8\">)) &amp; Fin(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"387\" y=\"-92.8\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"403\" y=\"-92.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",
"<!-- 0&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>0-&gt;0</title>\n",
"<path d=\"M49.6208,-35.0373C48.3189,-44.8579 50.4453,-54 56,-54 60.166,-54 62.4036,-48.8576 62.7128,-42.1433\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"62.3792,-35.0373 65.8541,-41.8818 62.5434,-38.5335 62.7076,-42.0296 62.7076,-42.0296 62.7076,-42.0296 62.5434,-38.5335 59.561,-42.1774 62.3792,-35.0373 62.3792,-35.0373\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"26.5\" y=\"-72.8\">!p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"48\" y=\"-57.8\">\u24ff</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
"<ellipse cx=\"180\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"180\" y=\"-14.3\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
"<path d=\"M74.2209,-18C95.2018,-18 130.787,-18 154.587,-18\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"161.867,-18 154.867,-21.1501 158.367,-18 154.867,-18.0001 154.867,-18.0001 154.867,-18.0001 158.367,-18 154.867,-14.8501 161.867,-18 161.867,-18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-35.8\">p0 &amp; p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"102\" y=\"-21.8\">\u2776</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"118\" y=\"-21.8\">\u2778</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node4\"><title>4</title>\n",
"<ellipse cx=\"307\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"307\" y=\"-14.3\">4</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;4</title>\n",
"<path d=\"M198.119,-18C219.691,-18 256.912,-18 281.495,-18\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"288.687,-18 281.687,-21.1501 285.187,-18 281.687,-18.0001 281.687,-18.0001 281.687,-18.0001 285.187,-18 281.687,-14.8501 288.687,-18 288.687,-18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"216\" y=\"-21.8\">p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node5\"><title>2</title>\n",
"<ellipse cx=\"431\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"431\" y=\"-14.3\">2</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>4-&gt;2</title>\n",
"<path d=\"M325.221,-18C346.202,-18 381.787,-18 405.587,-18\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"412.867,-18 405.867,-21.1501 409.367,-18 405.867,-18.0001 405.867,-18.0001 405.867,-18.0001 409.367,-18 405.867,-14.8501 412.867,-18 412.867,-18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"343\" y=\"-36.8\">p0 &amp; p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"361\" y=\"-21.8\">\u2776</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node6\"><title>3</title>\n",
"<ellipse cx=\"555\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"555\" y=\"-14.3\">3</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>2-&gt;3</title>\n",
"<path d=\"M449.221,-18C470.202,-18 505.787,-18 529.587,-18\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"536.867,-18 529.867,-21.1501 533.367,-18 529.867,-18.0001 529.867,-18.0001 529.867,-18.0001 533.367,-18 529.867,-14.8501 536.867,-18 536.867,-18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"467\" y=\"-21.8\">p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>3-&gt;3</title>\n",
"<path d=\"M544.627,-32.7917C541.249,-43.4165 544.707,-54 555,-54 562.881,-54 566.754,-47.7961 566.622,-40.1197\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"565.373,-32.7917 569.654,-39.1632 565.961,-36.242 566.549,-39.6923 566.549,-39.6923 566.549,-39.6923 565.961,-36.242 563.444,-40.2213 565.373,-32.7917 565.373,-32.7917\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"529\" y=\"-72.8\">p0 &amp; p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"547\" y=\"-57.8\">\u2776</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD><TD><svg height=\"76pt\" viewBox=\"0.00 0.00 389.00 75.95\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.660441 0.660441) rotate(0) translate(4 111)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-111 585,-111 585,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"208.5\" y=\"-92.8\">(Inf(</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"233.5\" y=\"-92.8\">\u2777</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"249.5\" y=\"-92.8\">) | Inf(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"286.5\" y=\"-92.8\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"302.5\" y=\"-92.8\">)) &amp; Fin(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"352.5\" y=\"-92.8\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"368.5\" y=\"-92.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",
"<!-- 0&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>0-&gt;0</title>\n",
"<path d=\"M49.6208,-35.0373C48.3189,-44.8579 50.4453,-54 56,-54 60.166,-54 62.4036,-48.8576 62.7128,-42.1433\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"62.3792,-35.0373 65.8541,-41.8818 62.5434,-38.5335 62.7076,-42.0296 62.7076,-42.0296 62.7076,-42.0296 62.5434,-38.5335 59.561,-42.1774 62.3792,-35.0373 62.3792,-35.0373\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"26.5\" y=\"-72.8\">!p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"48\" y=\"-57.8\">\u24ff</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
"<ellipse cx=\"180\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"180\" y=\"-14.3\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
"<path d=\"M74.2209,-18C95.2018,-18 130.787,-18 154.587,-18\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"161.867,-18 154.867,-21.1501 158.367,-18 154.867,-18.0001 154.867,-18.0001 154.867,-18.0001 158.367,-18 154.867,-14.8501 161.867,-18 161.867,-18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-35.8\">p0 &amp; p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"102\" y=\"-21.8\">\u2776</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"118\" y=\"-21.8\">\u2777</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node4\"><title>4</title>\n",
"<ellipse cx=\"307\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"307\" y=\"-14.3\">4</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;4</title>\n",
"<path d=\"M198.119,-18C219.691,-18 256.912,-18 281.495,-18\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"288.687,-18 281.687,-21.1501 285.187,-18 281.687,-18.0001 281.687,-18.0001 281.687,-18.0001 285.187,-18 281.687,-14.8501 288.687,-18 288.687,-18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"216\" y=\"-21.8\">p0 &amp; !p1</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node5\"><title>2</title>\n",
"<ellipse cx=\"431\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"431\" y=\"-14.3\">2</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>4-&gt;2</title>\n",
"<path d=\"M325.221,-18C346.202,-18 381.787,-18 405.587,-18\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"412.867,-18 405.867,-21.1501 409.367,-18 405.867,-18.0001 405.867,-18.0001 405.867,-18.0001 409.367,-18 405.867,-14.8501 412.867,-18 412.867,-18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"343\" y=\"-36.8\">p0 &amp; p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"361\" y=\"-21.8\">\u2776</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node6\"><title>3</title>\n",
"<ellipse cx=\"555\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"555\" y=\"-14.3\">3</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>2-&gt;3</title>\n",
"<path d=\"M449.221,-18C470.202,-18 505.787,-18 529.587,-18\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"536.867,-18 529.867,-21.1501 533.367,-18 529.867,-18.0001 529.867,-18.0001 529.867,-18.0001 533.367,-18 529.867,-14.8501 536.867,-18 536.867,-18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"467\" y=\"-21.8\">p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>3-&gt;3</title>\n",
"<path d=\"M544.627,-32.7917C541.249,-43.4165 544.707,-54 555,-54 562.881,-54 566.754,-47.7961 566.622,-40.1197\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"565.373,-32.7917 569.654,-39.1632 565.961,-36.242 566.549,-39.6923 566.549,-39.6923 566.549,-39.6923 565.961,-36.242 563.444,-40.2213 565.373,-32.7917 565.373,-32.7917\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"529\" y=\"-72.8\">p0 &amp; p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"547\" y=\"-57.8\">\u2776</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD></TR><TR><TD><svg height=\"131pt\" viewBox=\"0.00 0.00 389.00 131.14\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.590737 0.590737) rotate(0) translate(4 218)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-218 654.5,-218 654.5,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"212.25\" y=\"-199.8\">Fin(</text>\n",
"<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"237.25\" y=\"-199.8\">\u2778</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"253.25\" y=\"-199.8\">) &amp; Fin(</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"299.25\" y=\"-199.8\">\u2777</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"315.25\" y=\"-199.8\">) &amp; (Inf(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"362.25\" y=\"-199.8\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"378.25\" y=\"-199.8\">)&amp;Inf(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"414.25\" y=\"-199.8\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"430.25\" y=\"-199.8\">))</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
"<ellipse cx=\"56\" cy=\"-48\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-44.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,-48C2.79388,-48 17.1543,-48 30.6317,-48\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"37.9419,-48 30.9419,-51.1501 34.4419,-48 30.9419,-48.0001 30.9419,-48.0001 30.9419,-48.0001 34.4419,-48 30.9418,-44.8501 37.9419,-48 37.9419,-48\" stroke=\"black\"/>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node3\"><title>4</title>\n",
"<ellipse cx=\"192.5\" cy=\"-114\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"192.5\" y=\"-110.3\">4</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>0-&gt;4</title>\n",
"<path d=\"M72.4289,-55.571C96.2193,-67.2452 141.964,-89.6923 169.306,-103.109\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"175.837,-106.314 168.165,-106.058 172.695,-104.772 169.553,-103.23 169.553,-103.23 169.553,-103.23 172.695,-104.772 170.94,-100.402 175.837,-106.314 175.837,-106.314\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-107.8\">!p0 &amp; p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"103.5\" y=\"-93.8\">\u24ff</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"119.5\" y=\"-93.8\">\u2776</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node4\"><title>1</title>\n",
"<ellipse cx=\"337.5\" cy=\"-84\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"337.5\" y=\"-80.3\">1</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge11\"><title>4-&gt;1</title>\n",
"<path d=\"M210.184,-110.5C235.45,-105.199 283.539,-95.1107 312.542,-89.0261\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"319.479,-87.5708 313.275,-92.091 316.054,-88.2895 312.628,-89.0081 312.628,-89.0081 312.628,-89.0081 316.054,-88.2895 311.982,-85.9252 319.479,-87.5708 319.479,-87.5708\" 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",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node6\"><title>2</title>\n",
"<ellipse cx=\"623\" cy=\"-104\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"623\" y=\"-100.3\">2</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge10\"><title>4-&gt;2</title>\n",
"<path d=\"M208.11,-123.711C216.506,-128.812 227.451,-134.678 238,-138 355.52,-175.009 393.266,-188.573 514,-164 548.541,-156.97 556.89,-151.326 587,-133 592.841,-129.445 598.738,-124.973 603.984,-120.614\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"609.388,-115.975 606.128,-122.925 606.732,-118.255 604.076,-120.535 604.076,-120.535 604.076,-120.535 606.732,-118.255 602.024,-118.145 609.388,-115.975 609.388,-115.975\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"387\" y=\"-179.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;0</title>\n",
"<path d=\"M320.078,-79.247C297.674,-72.9814 256.176,-62.1514 220,-57 171.165,-50.0459 113.39,-48.3875 81.4045,-48.0385\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"74.2268,-47.9777 81.2532,-44.8872 77.7267,-48.0074 81.2265,-48.0371 81.2265,-48.0371 81.2265,-48.0371 77.7267,-48.0074 81.1998,-51.1869 74.2268,-47.9777 74.2268,-47.9777\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"165\" y=\"-75.8\">!p0 &amp; p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"184.5\" y=\"-60.8\">\u2776</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node5\"><title>3</title>\n",
"<ellipse cx=\"488\" cy=\"-75\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"488\" y=\"-71.3\">3</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>1-&gt;3</title>\n",
"<path d=\"M355.535,-82.9676C381.802,-81.3757 432.308,-78.3147 462.496,-76.4851\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"469.706,-76.0481 462.91,-79.6159 466.213,-76.2599 462.719,-76.4717 462.719,-76.4717 462.719,-76.4717 466.213,-76.2599 462.529,-73.3274 469.706,-76.0481 469.706,-76.0481\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"387\" y=\"-99.8\">p0 &amp; !p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"406.5\" y=\"-84.8\">\u2776</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>3-&gt;1</title>\n",
"<path d=\"M474.208,-62.9306C466.201,-56.2295 455.289,-48.5488 444,-45 418.985,-37.1361 409.642,-36.0343 385,-45 373.737,-49.0979 363.303,-57.254 355.184,-65.0529\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"349.952,-70.3408 352.636,-63.1494 352.413,-67.8529 354.875,-65.365 354.875,-65.365 354.875,-65.365 352.413,-67.8529 357.114,-67.5806 349.952,-70.3408 349.952,-70.3408\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"385\" y=\"-62.8\">!p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"398.5\" y=\"-48.8\">\u24ff</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"414.5\" y=\"-48.8\">\u2776</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>3-&gt;2</title>\n",
"<path d=\"M506.047,-74.7273C525.921,-74.8651 559.547,-76.5225 587,-85 591.794,-86.4803 596.682,-88.6479 601.226,-90.9943\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"607.586,-94.5007 599.935,-93.8796 604.521,-92.8109 601.456,-91.121 601.456,-91.121 601.456,-91.121 604.521,-92.8109 602.976,-88.3625 607.586,-94.5007 607.586,-94.5007\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"532\" y=\"-103.8\">!p0 &amp; p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"551.5\" y=\"-88.8\">\u24ff</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>2-&gt;0</title>\n",
"<path d=\"M612.68,-89.0993C593.408,-60.3424 546.157,-0 489,-0 191.5,-0 191.5,-0 191.5,-0 149.216,-0 103.577,-21.3034 77.8201,-35.5256\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"71.7141,-38.9716 76.2621,-32.7878 74.7622,-37.2513 77.8103,-35.5311 77.8103,-35.5311 77.8103,-35.5311 74.7622,-37.2513 79.3586,-38.2743 71.7141,-38.9716 71.7141,-38.9716\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"308\" y=\"-18.8\">!p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"329.5\" y=\"-3.8\">\u24ff</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>2-&gt;1</title>\n",
"<path d=\"M605.863,-110.2C600.014,-112.144 593.296,-114.034 587,-115 498.261,-128.616 470.926,-141.016 385,-115 375.084,-111.998 365.35,-106.107 357.371,-100.259\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"351.638,-95.844 359.106,-97.619 354.411,-97.9794 357.184,-100.115 357.184,-100.115 357.184,-100.115 354.411,-97.9794 355.263,-102.611 351.638,-95.844 351.638,-95.844\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"462\" y=\"-148.8\">p0 &amp; p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"480\" y=\"-133.8\">\u24ff</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>2-&gt;2</title>\n",
"<path d=\"M612.627,-118.792C609.249,-129.417 612.707,-140 623,-140 630.881,-140 634.754,-133.796 634.622,-126.12\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"633.373,-118.792 637.654,-125.163 633.961,-122.242 634.549,-125.692 634.549,-125.692 634.549,-125.692 633.961,-122.242 631.444,-126.221 633.373,-118.792 633.373,-118.792\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"595.5\" y=\"-143.8\">p0 &amp; !p1</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD><TD><svg height=\"131pt\" viewBox=\"0.00 0.00 389.00 131.14\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.590737 0.590737) rotate(0) translate(4 218)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-218 654.5,-218 654.5,4 -4,4\" stroke=\"none\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"243.25\" y=\"-199.8\">Fin(</text>\n",
"<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"268.25\" y=\"-199.8\">\u2777</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"284.25\" y=\"-199.8\">) &amp; (Inf(</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"331.25\" y=\"-199.8\">\u24ff</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"347.25\" y=\"-199.8\">)&amp;Inf(</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"383.25\" y=\"-199.8\">\u2776</text>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"399.25\" y=\"-199.8\">))</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
"<ellipse cx=\"56\" cy=\"-48\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-44.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,-48C2.79388,-48 17.1543,-48 30.6317,-48\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"37.9419,-48 30.9419,-51.1501 34.4419,-48 30.9419,-48.0001 30.9419,-48.0001 30.9419,-48.0001 34.4419,-48 30.9418,-44.8501 37.9419,-48 37.9419,-48\" stroke=\"black\"/>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node3\"><title>4</title>\n",
"<ellipse cx=\"192.5\" cy=\"-114\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"192.5\" y=\"-110.3\">4</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>0-&gt;4</title>\n",
"<path d=\"M72.4289,-55.571C96.2193,-67.2452 141.964,-89.6923 169.306,-103.109\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"175.837,-106.314 168.165,-106.058 172.695,-104.772 169.553,-103.23 169.553,-103.23 169.553,-103.23 172.695,-104.772 170.94,-100.402 175.837,-106.314 175.837,-106.314\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-107.8\">!p0 &amp; p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"103.5\" y=\"-93.8\">\u24ff</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"119.5\" y=\"-93.8\">\u2776</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node4\"><title>1</title>\n",
"<ellipse cx=\"337.5\" cy=\"-84\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"337.5\" y=\"-80.3\">1</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge11\"><title>4-&gt;1</title>\n",
"<path d=\"M210.184,-110.5C235.45,-105.199 283.539,-95.1107 312.542,-89.0261\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"319.479,-87.5708 313.275,-92.091 316.054,-88.2895 312.628,-89.0081 312.628,-89.0081 312.628,-89.0081 316.054,-88.2895 311.982,-85.9252 319.479,-87.5708 319.479,-87.5708\" 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",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node6\"><title>2</title>\n",
"<ellipse cx=\"623\" cy=\"-104\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"623\" y=\"-100.3\">2</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge10\"><title>4-&gt;2</title>\n",
"<path d=\"M208.11,-123.711C216.506,-128.812 227.451,-134.678 238,-138 355.52,-175.009 393.266,-188.573 514,-164 548.541,-156.97 556.89,-151.326 587,-133 592.841,-129.445 598.738,-124.973 603.984,-120.614\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"609.388,-115.975 606.128,-122.925 606.732,-118.255 604.076,-120.535 604.076,-120.535 604.076,-120.535 606.732,-118.255 602.024,-118.145 609.388,-115.975 609.388,-115.975\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"387\" y=\"-179.8\">!p0 &amp; p1</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>1-&gt;0</title>\n",
"<path d=\"M320.078,-79.247C297.674,-72.9814 256.176,-62.1514 220,-57 171.165,-50.0459 113.39,-48.3875 81.4045,-48.0385\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"74.2268,-47.9777 81.2532,-44.8872 77.7267,-48.0074 81.2265,-48.0371 81.2265,-48.0371 81.2265,-48.0371 77.7267,-48.0074 81.1998,-51.1869 74.2268,-47.9777 74.2268,-47.9777\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"165\" y=\"-75.8\">!p0 &amp; p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"184.5\" y=\"-60.8\">\u2776</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node5\"><title>3</title>\n",
"<ellipse cx=\"488\" cy=\"-75\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"488\" y=\"-71.3\">3</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>1-&gt;3</title>\n",
"<path d=\"M355.535,-82.9676C381.802,-81.3757 432.308,-78.3147 462.496,-76.4851\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"469.706,-76.0481 462.91,-79.6159 466.213,-76.2599 462.719,-76.4717 462.719,-76.4717 462.719,-76.4717 466.213,-76.2599 462.529,-73.3274 469.706,-76.0481 469.706,-76.0481\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"387\" y=\"-99.8\">p0 &amp; !p1</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"406.5\" y=\"-84.8\">\u2776</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>3-&gt;1</title>\n",
"<path d=\"M474.208,-62.9306C466.201,-56.2295 455.289,-48.5488 444,-45 418.985,-37.1361 409.642,-36.0343 385,-45 373.737,-49.0979 363.303,-57.254 355.184,-65.0529\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"349.952,-70.3408 352.636,-63.1494 352.413,-67.8529 354.875,-65.365 354.875,-65.365 354.875,-65.365 352.413,-67.8529 357.114,-67.5806 349.952,-70.3408 349.952,-70.3408\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"385\" y=\"-62.8\">!p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"398.5\" y=\"-48.8\">\u24ff</text>\n",
"<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"414.5\" y=\"-48.8\">\u2776</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>3-&gt;2</title>\n",
"<path d=\"M506.047,-74.7273C525.921,-74.8651 559.547,-76.5225 587,-85 591.794,-86.4803 596.682,-88.6479 601.226,-90.9943\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"607.586,-94.5007 599.935,-93.8796 604.521,-92.8109 601.456,-91.121 601.456,-91.121 601.456,-91.121 604.521,-92.8109 602.976,-88.3625 607.586,-94.5007 607.586,-94.5007\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"532\" y=\"-103.8\">!p0 &amp; p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"551.5\" y=\"-88.8\">\u24ff</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;0 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>2-&gt;0</title>\n",
"<path d=\"M612.68,-89.0993C593.408,-60.3424 546.157,-0 489,-0 191.5,-0 191.5,-0 191.5,-0 149.216,-0 103.577,-21.3034 77.8201,-35.5256\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"71.7141,-38.9716 76.2621,-32.7878 74.7622,-37.2513 77.8103,-35.5311 77.8103,-35.5311 77.8103,-35.5311 74.7622,-37.2513 79.3586,-38.2743 71.7141,-38.9716 71.7141,-38.9716\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"308\" y=\"-18.8\">!p0 &amp; !p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"329.5\" y=\"-3.8\">\u24ff</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>2-&gt;1</title>\n",
"<path d=\"M605.863,-110.2C600.014,-112.144 593.296,-114.034 587,-115 498.261,-128.616 470.926,-141.016 385,-115 375.084,-111.998 365.35,-106.107 357.371,-100.259\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"351.638,-95.844 359.106,-97.619 354.411,-97.9794 357.184,-100.115 357.184,-100.115 357.184,-100.115 354.411,-97.9794 355.263,-102.611 351.638,-95.844 351.638,-95.844\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"462\" y=\"-148.8\">p0 &amp; p1</text>\n",
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"480\" y=\"-133.8\">\u24ff</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>2-&gt;2</title>\n",
"<path d=\"M612.627,-118.792C609.249,-129.417 612.707,-140 623,-140 630.881,-140 634.754,-133.796 634.622,-126.12\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"633.373,-118.792 637.654,-125.163 633.961,-122.242 634.549,-125.692 634.549,-125.692 634.549,-125.692 633.961,-122.242 631.444,-126.221 633.373,-118.792 633.373,-118.792\" stroke=\"black\"/>\n",
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"595.5\" y=\"-143.8\">p0 &amp; !p1</text>\n",
"</g>\n",
"</g>\n",
"</svg></TD></TR></TABLE>"
],
"metadata": {},
"output_type": "pyout",
"prompt_number": 2,
"text": [
"<IPython.core.display.HTML at 0x7f5ca02a7b70>"
]
}
],
"prompt_number": 2
},
{
"cell_type": "code",
"collapsed": false,
"input": [],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 3
}
],
"metadata": {}
}
]
}
Reference in a new issue View git blame Copy permalink