diff --git a/logic_programming/5_SLD.ipynb b/logic_programming/5_SLD.ipynb
index 42e2e280c0209ccd718c2ec53bbe6a580f84292e..87a08d339b950ea6ea535c835082757cbe66eb30 100644
--- a/logic_programming/5_SLD.ipynb
+++ b/logic_programming/5_SLD.ipynb
@@ -60,9 +60,9 @@
     ":- discontiguous program/3.\n",
     ":- dynamic program/3.\n",
     "program(1,'weather',\n",
-    "   [ [pos(wet),neg(rains),neg(outside)],\n",
-    "     [pos(rains)],\n",
-    "     [pos(outside)] ]).\n",
+    "   [ [pos(wet),neg(rains),neg(outside)],      % wet :- rains, outside.\n",
+    "     [pos(rains)],                            % rains.\n",
+    "     [pos(outside)] ]).                       % outside.\n",
     "negate(pos(A),neg(A)).\n",
     "negate(neg(A),pos(A))."
    ]
@@ -74,7 +74,7 @@
    "source": [
     "For simplicity we will assume that the positive literal is always the first literal in a clause.\n",
     "\n",
-    "Let us now perform resolution with a negative literal:"
+    "Let us now perform resolution with a negative literal by searching for a clause with a matching positive literal (in first position):"
    ]
   },
   {
@@ -135,7 +135,7 @@
    "id": "68fd6059",
    "metadata": {},
    "source": [
-    "Here we find a contradiction:"
+    "Here we find a contradiction, by obtaining the empty clause for the logical variable ```Resolvent```:"
    ]
   },
   {
@@ -168,7 +168,7 @@
    "id": "07785e91",
    "metadata": {},
    "source": [
-    "We can extend this code to work with a complete denial, rather than single negative literal:"
+    "We can extend this code to work with longer denials (aka queries), rather than just single negative literal:"
    ]
   },
   {
@@ -183,9 +183,9 @@
    "outputs": [],
    "source": [
     "resolve_query(Query,Clauses,Resolvent) :-\n",
-    "     selection_rule(Query,SelectedLiteral,RestQuery),\n",
-    "     resolve_literal(SelectedLiteral,Clauses,Body),\n",
-    "     append(Body,RestQuery,Resolvent).\n",
+    "     selection_rule(Query,SelectedLiteral,RestQuery),  % select literal\n",
+    "     resolve_literal(SelectedLiteral,Clauses,Body),    % resolve literal\n",
+    "     append(Body,RestQuery,Resolvent).                 % merge body with rest of denial/query\n",
     "\n",
     "selection_rule([LeftmostLiteral|Rest],LeftmostLiteral,Rest)."
    ]
@@ -644,7 +644,91 @@
    "outputs": [
     {
      "data": {
-      "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 7.0.0 (20221023.0053)\n -->\n<!-- Pages: 1 -->\n<svg width=\"282pt\" height=\"392pt\"\n viewBox=\"0.00 0.00 282.19 392.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 388)\">\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-388 278.19,-388 278.19,4 -4,4\"/>\n<!-- [] -->\n<g id=\"node1\" class=\"node\">\n<title>[]</title>\n<polygon fill=\"none\" stroke=\"green\" points=\"93.45,-36 39.45,-36 39.45,0 93.45,0 93.45,-36\"/>\n<text text-anchor=\"middle\" x=\"66.45\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">[]</text>\n</g>\n<!-- [neg(p)] -->\n<g id=\"node2\" class=\"node\">\n<title>[neg(p)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"143.37,-348.05 145.97,-348.15 148.55,-348.3 151.08,-348.49 153.57,-348.74 156,-349.03 158.37,-349.36 160.65,-349.75 162.86,-350.18 164.96,-350.65 166.97,-351.16 168.87,-351.71 170.66,-352.31 172.32,-352.94 173.86,-353.61 175.28,-354.31 176.55,-355.04 177.7,-355.8 178.71,-356.59 179.57,-357.41 180.3,-358.25 180.89,-359.11 181.35,-359.99 181.66,-360.89 181.84,-361.8 181.89,-362.72 181.81,-363.65 181.6,-364.59 181.28,-365.53 180.83,-366.47 180.28,-367.41 179.62,-368.35 178.86,-369.28 178,-370.2 177.05,-371.11 176.02,-372.01 174.91,-372.89 173.73,-373.75 172.48,-374.59 171.17,-375.41 169.8,-376.2 168.38,-376.96 166.92,-377.69 165.41,-378.39 163.87,-379.06 162.3,-379.69 160.7,-380.29 159.07,-380.84 157.43,-381.35 155.76,-381.82 154.08,-382.25 152.38,-382.64 150.68,-382.97 148.96,-383.26 147.24,-383.51 145.52,-383.7 143.78,-383.85 142.05,-383.95 140.31,-384 138.58,-384 136.84,-383.95 135.11,-383.85 133.38,-383.7 131.65,-383.51 129.93,-383.26 128.21,-382.97 126.51,-382.64 124.81,-382.25 123.13,-381.82 121.47,-381.35 119.82,-380.84 118.19,-380.29 116.59,-379.69 115.02,-379.06 113.48,-378.39 111.97,-377.69 110.51,-376.96 109.09,-376.2 107.72,-375.41 106.41,-374.59 105.16,-373.75 103.98,-372.89 102.87,-372.01 101.84,-371.11 100.89,-370.2 100.03,-369.28 99.27,-368.35 98.61,-367.41 98.06,-366.47 97.61,-365.53 97.29,-364.59 97.08,-363.65 97,-362.72 97.05,-361.8 97.23,-360.89 97.55,-359.99 98,-359.11 98.59,-358.25 99.32,-357.41 100.19,-356.59 101.19,-355.8 102.34,-355.04 103.62,-354.31 105.03,-353.61 106.57,-352.94 108.24,-352.31 110.02,-351.71 111.92,-351.16 113.93,-350.65 116.04,-350.18 118.24,-349.75 120.53,-349.36 122.89,-349.03 125.32,-348.74 127.81,-348.49 130.34,-348.3 132.92,-348.15 135.52,-348.05 138.14,-348 140.76,-348 143.37,-348.05\"/>\n<text text-anchor=\"middle\" x=\"139.45\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(p)]</text>\n</g>\n<!-- [neg(q),neg(r)] -->\n<g id=\"node3\" class=\"node\">\n<title>[neg(q),neg(r)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"145.71,-261.05 149.85,-261.15 153.96,-261.3 158,-261.49 161.97,-261.74 165.84,-262.03 169.61,-262.36 173.25,-262.75 176.76,-263.18 180.13,-263.65 183.33,-264.16 186.35,-264.71 189.2,-265.31 191.86,-265.94 194.31,-266.61 196.56,-267.31 198.6,-268.04 200.43,-268.8 202.03,-269.59 203.42,-270.41 204.58,-271.25 205.52,-272.11 206.24,-272.99 206.74,-273.89 207.03,-274.8 207.11,-275.72 206.98,-276.65 206.65,-277.59 206.13,-278.53 205.43,-279.47 204.54,-280.41 203.49,-281.35 202.27,-282.28 200.91,-283.2 199.4,-284.11 197.75,-285.01 195.98,-285.89 194.1,-286.75 192.11,-287.59 190.02,-288.41 187.84,-289.2 185.58,-289.96 183.24,-290.69 180.84,-291.39 178.39,-292.06 175.88,-292.69 173.33,-293.29 170.73,-293.84 168.11,-294.35 165.45,-294.82 162.77,-295.25 160.07,-295.64 157.35,-295.97 154.62,-296.26 151.88,-296.51 149.12,-296.7 146.36,-296.85 143.6,-296.95 140.83,-297 138.06,-297 135.29,-296.95 132.53,-296.85 129.77,-296.7 127.02,-296.51 124.27,-296.26 121.54,-295.97 118.82,-295.64 116.12,-295.25 113.44,-294.82 110.78,-294.35 108.16,-293.84 105.57,-293.29 103.01,-292.69 100.5,-292.06 98.05,-291.39 95.65,-290.69 93.32,-289.96 91.06,-289.2 88.88,-288.41 86.79,-287.59 84.8,-286.75 82.91,-285.89 81.14,-285.01 79.5,-284.11 77.99,-283.2 76.62,-282.28 75.4,-281.35 74.35,-280.41 73.47,-279.47 72.76,-278.53 72.24,-277.59 71.91,-276.65 71.78,-275.72 71.86,-274.8 72.15,-273.89 72.65,-272.99 73.37,-272.11 74.31,-271.25 75.48,-270.41 76.86,-269.59 78.46,-268.8 80.29,-268.04 82.33,-267.31 84.58,-266.61 87.04,-265.94 89.69,-265.31 92.54,-264.71 95.57,-264.16 98.77,-263.65 102.13,-263.18 105.64,-262.75 109.28,-262.36 113.05,-262.03 116.93,-261.74 120.89,-261.49 124.94,-261.3 129.04,-261.15 133.19,-261.05 137.36,-261 141.54,-261 145.71,-261.05\"/>\n<text text-anchor=\"middle\" x=\"139.45\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(q),neg(r)]</text>\n</g>\n<!-- [neg(p)]&#45;&gt;[neg(q),neg(r)] -->\n<g id=\"edge1\" class=\"edge\">\n<title>[neg(p)]&#45;&gt;[neg(q),neg(r)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M139.45,-347.8C139.45,-336.58 139.45,-321.67 139.45,-308.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"142.95,-308.98 139.45,-298.98 135.95,-308.98 142.95,-308.98\"/>\n<text text-anchor=\"middle\" x=\"142.95\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">p</text>\n</g>\n<!-- [neg(s),neg(r)] -->\n<g id=\"node5\" class=\"node\">\n<title>[neg(s),neg(r)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"72.59,-174.05 76.66,-174.15 80.68,-174.3 84.65,-174.49 88.54,-174.74 92.35,-175.03 96.04,-175.36 99.62,-175.75 103.06,-176.18 106.36,-176.65 109.5,-177.16 112.48,-177.71 115.27,-178.31 117.87,-178.94 120.28,-179.61 122.49,-180.31 124.49,-181.04 126.28,-181.8 127.86,-182.59 129.22,-183.41 130.36,-184.25 131.28,-185.11 131.99,-185.99 132.48,-186.89 132.76,-187.8 132.84,-188.72 132.71,-189.65 132.39,-190.59 131.88,-191.53 131.19,-192.47 130.32,-193.41 129.29,-194.35 128.1,-195.28 126.75,-196.2 125.27,-197.11 123.66,-198.01 121.92,-198.89 120.07,-199.75 118.12,-200.59 116.07,-201.41 113.93,-202.2 111.71,-202.96 109.42,-203.69 107.07,-204.39 104.66,-205.06 102.2,-205.69 99.69,-206.29 97.15,-206.84 94.57,-207.35 91.97,-207.82 89.33,-208.25 86.68,-208.64 84.02,-208.97 81.33,-209.26 78.64,-209.51 75.94,-209.7 73.23,-209.85 70.52,-209.95 67.8,-210 65.09,-210 62.37,-209.95 59.66,-209.85 56.95,-209.7 54.25,-209.51 51.56,-209.26 48.88,-208.97 46.21,-208.64 43.56,-208.25 40.93,-207.82 38.32,-207.35 35.74,-206.84 33.2,-206.29 30.7,-205.69 28.23,-205.06 25.82,-204.39 23.47,-203.69 21.18,-202.96 18.96,-202.2 16.83,-201.41 14.77,-200.59 12.82,-199.75 10.97,-198.89 9.23,-198.01 7.62,-197.11 6.14,-196.2 4.8,-195.28 3.6,-194.35 2.57,-193.41 1.7,-192.47 1.01,-191.53 0.5,-190.59 0.18,-189.65 0.05,-188.72 0.13,-187.8 0.41,-186.89 0.91,-185.99 1.61,-185.11 2.54,-184.25 3.68,-183.41 5.03,-182.59 6.61,-181.8 8.4,-181.04 10.4,-180.31 12.61,-179.61 15.02,-178.94 17.62,-178.31 20.42,-177.71 23.39,-177.16 26.53,-176.65 29.83,-176.18 33.27,-175.75 36.85,-175.36 40.55,-175.03 44.35,-174.74 48.24,-174.49 52.21,-174.3 56.23,-174.15 60.3,-174.05 64.4,-174 68.5,-174 72.59,-174.05\"/>\n<text text-anchor=\"middle\" x=\"66.45\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(s),neg(r)]</text>\n</g>\n<!-- [neg(q),neg(r)]&#45;&gt;[neg(s),neg(r)] -->\n<g id=\"edge3\" class=\"edge\">\n<title>[neg(q),neg(r)]&#45;&gt;[neg(s),neg(r)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M125.02,-261.21C114.53,-248.98 100.12,-232.21 88.23,-218.36\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"91,-216.21 81.82,-210.91 85.68,-220.77 91,-216.21\"/>\n<text text-anchor=\"middle\" x=\"110.95\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">q</text>\n</g>\n<!-- [neg(t),neg(r)] -->\n<g id=\"node6\" class=\"node\">\n<title>[neg(t),neg(r)]</title>\n<ellipse fill=\"none\" stroke=\"red\" cx=\"212.45\" cy=\"-192\" rx=\"61.99\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"212.45\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(t),neg(r)]</text>\n</g>\n<!-- [neg(q),neg(r)]&#45;&gt;[neg(t),neg(r)] -->\n<g id=\"edge2\" class=\"edge\">\n<title>[neg(q),neg(r)]&#45;&gt;[neg(t),neg(r)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M153.87,-261.21C164.37,-248.98 178.77,-232.21 190.66,-218.36\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"193.21,-220.77 197.07,-210.91 187.9,-216.21 193.21,-220.77\"/>\n<text text-anchor=\"middle\" x=\"182.95\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">q</text>\n</g>\n<!-- [neg(r)] -->\n<g id=\"node4\" class=\"node\">\n<title>[neg(r)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"70.21,-87.05 72.7,-87.15 75.17,-87.3 77.6,-87.49 79.98,-87.74 82.31,-88.03 84.58,-88.36 86.77,-88.75 88.88,-89.18 90.9,-89.65 92.82,-90.16 94.64,-90.71 96.36,-91.31 97.95,-91.94 99.43,-92.61 100.78,-93.31 102.01,-94.04 103.1,-94.8 104.07,-95.59 104.9,-96.41 105.6,-97.25 106.17,-98.11 106.6,-98.99 106.9,-99.89 107.07,-100.8 107.12,-101.72 107.04,-102.65 106.85,-103.59 106.53,-104.53 106.11,-105.47 105.58,-106.41 104.94,-107.35 104.21,-108.28 103.39,-109.2 102.48,-110.11 101.5,-111.01 100.43,-111.89 99.3,-112.75 98.1,-113.59 96.85,-114.41 95.54,-115.2 94.18,-115.96 92.77,-116.69 91.33,-117.39 89.86,-118.06 88.35,-118.69 86.81,-119.29 85.26,-119.84 83.68,-120.35 82.08,-120.82 80.47,-121.25 78.84,-121.64 77.21,-121.97 75.57,-122.26 73.92,-122.51 72.26,-122.7 70.6,-122.85 68.94,-122.95 67.28,-123 65.61,-123 63.95,-122.95 62.29,-122.85 60.63,-122.7 58.97,-122.51 57.32,-122.26 55.68,-121.97 54.05,-121.64 52.42,-121.25 50.81,-120.82 49.22,-120.35 47.64,-119.84 46.08,-119.29 44.54,-118.69 43.04,-118.06 41.56,-117.39 40.12,-116.69 38.72,-115.96 37.36,-115.2 36.05,-114.41 34.79,-113.59 33.59,-112.75 32.46,-111.89 31.4,-111.01 30.41,-110.11 29.5,-109.2 28.68,-108.28 27.95,-107.35 27.31,-106.41 26.78,-105.47 26.36,-104.53 26.05,-103.59 25.85,-102.65 25.77,-101.72 25.82,-100.8 25.99,-99.89 26.29,-98.99 26.73,-98.11 27.29,-97.25 27.99,-96.41 28.82,-95.59 29.79,-94.8 30.88,-94.04 32.11,-93.31 33.46,-92.61 34.94,-91.94 36.54,-91.31 38.25,-90.71 40.07,-90.16 41.99,-89.65 44.01,-89.18 46.12,-88.75 48.31,-88.36 50.58,-88.03 52.91,-87.74 55.29,-87.49 57.72,-87.3 60.19,-87.15 62.68,-87.05 65.19,-87 67.7,-87 70.21,-87.05\"/>\n<text text-anchor=\"middle\" x=\"66.45\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(r)]</text>\n</g>\n<!-- [neg(r)]&#45;&gt;[] -->\n<g id=\"edge4\" class=\"edge\">\n<title>[neg(r)]&#45;&gt;[]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M66.45,-86.8C66.45,-75.58 66.45,-60.67 66.45,-47.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"69.95,-47.98 66.45,-37.98 62.95,-47.98 69.95,-47.98\"/>\n<text text-anchor=\"middle\" x=\"68.95\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">r</text>\n</g>\n<!-- [neg(s),neg(r)]&#45;&gt;[neg(r)] -->\n<g id=\"edge5\" class=\"edge\">\n<title>[neg(s),neg(r)]&#45;&gt;[neg(r)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M66.45,-173.8C66.45,-162.58 66.45,-147.67 66.45,-134.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"69.95,-134.98 66.45,-124.98 62.95,-134.98 69.95,-134.98\"/>\n<text text-anchor=\"middle\" x=\"69.45\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">s</text>\n</g>\n</g>\n</svg>\n",
+      "image/svg+xml": [
+       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 10.0.1 (20240210.2158)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"294pt\" height=\"398pt\"\n",
+       " viewBox=\"0.00 0.00 293.55 398.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 394)\">\n",
+       "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-394 289.55,-394 289.55,4 -4,4\"/>\n",
+       "<!-- [] -->\n",
+       "<g id=\"node1\" class=\"node\">\n",
+       "<title>[]</title>\n",
+       "<polygon fill=\"none\" stroke=\"green\" points=\"96.4,-36 42.4,-36 42.4,0 96.4,0 96.4,-36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"69.4\" y=\"-12.95\" font-family=\"Times,serif\" font-size=\"14.00\">[]</text>\n",
+       "</g>\n",
+       "<!-- [neg(p)] -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>[neg(p)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"149.45,-354.05 152.14,-354.15 154.79,-354.3 157.41,-354.49 159.97,-354.74 162.48,-355.03 164.92,-355.36 167.28,-355.75 169.55,-356.18 171.73,-356.65 173.8,-357.16 175.76,-357.71 177.6,-358.31 179.32,-358.94 180.91,-359.61 182.36,-360.31 183.68,-361.04 184.86,-361.8 185.9,-362.59 186.8,-363.41 187.55,-364.25 188.16,-365.11 188.63,-365.99 188.95,-366.89 189.14,-367.8 189.19,-368.72 189.1,-369.65 188.89,-370.59 188.56,-371.53 188.1,-372.47 187.53,-373.41 186.85,-374.35 186.06,-375.28 185.17,-376.2 184.2,-377.11 183.13,-378.01 181.99,-378.89 180.77,-379.75 179.48,-380.59 178.13,-381.41 176.72,-382.2 175.25,-382.96 173.74,-383.69 172.19,-384.39 170.6,-385.06 168.98,-385.69 167.33,-386.29 165.65,-386.84 163.95,-387.35 162.23,-387.82 160.5,-388.25 158.75,-388.64 156.99,-388.97 155.22,-389.26 153.45,-389.51 151.66,-389.7 149.88,-389.85 148.09,-389.95 146.3,-390 144.51,-390 142.72,-389.95 140.93,-389.85 139.14,-389.7 137.36,-389.51 135.58,-389.26 133.81,-388.97 132.06,-388.64 130.31,-388.25 128.57,-387.82 126.85,-387.35 125.15,-386.84 123.48,-386.29 121.82,-385.69 120.2,-385.06 118.61,-384.39 117.06,-383.69 115.55,-382.96 114.09,-382.2 112.68,-381.41 111.33,-380.59 110.04,-379.75 108.82,-378.89 107.67,-378.01 106.61,-377.11 105.63,-376.2 104.74,-375.28 103.96,-374.35 103.28,-373.41 102.7,-372.47 102.25,-371.53 101.91,-370.59 101.7,-369.65 101.62,-368.72 101.67,-367.8 101.85,-366.89 102.18,-365.99 102.64,-365.11 103.25,-364.25 104.01,-363.41 104.9,-362.59 105.94,-361.8 107.12,-361.04 108.44,-360.31 109.9,-359.61 111.49,-358.94 113.2,-358.31 115.05,-357.71 117.01,-357.16 119.08,-356.65 121.25,-356.18 123.52,-355.75 125.88,-355.36 128.32,-355.03 130.83,-354.74 133.4,-354.49 136.01,-354.3 138.67,-354.15 141.35,-354.05 144.05,-354 146.75,-354 149.45,-354.05\"/>\n",
+       "<text text-anchor=\"middle\" x=\"145.4\" y=\"-366.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(p)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(q),neg(r)] -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>[neg(q),neg(r)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"151.93,-265.55 156.24,-265.65 160.52,-265.8 164.73,-265.99 168.86,-266.24 172.9,-266.53 176.83,-266.86 180.62,-267.25 184.28,-267.68 187.78,-268.15 191.12,-268.66 194.27,-269.21 197.24,-269.81 200.01,-270.44 202.56,-271.11 204.91,-271.81 207.03,-272.54 208.93,-273.3 210.61,-274.09 212.05,-274.91 213.26,-275.75 214.24,-276.61 214.99,-277.49 215.51,-278.39 215.81,-279.3 215.89,-280.22 215.76,-281.15 215.42,-282.09 214.88,-283.03 214.14,-283.97 213.22,-284.91 212.12,-285.85 210.86,-286.78 209.43,-287.7 207.86,-288.61 206.15,-289.51 204.3,-290.39 202.34,-291.25 200.26,-292.09 198.09,-292.91 195.82,-293.7 193.46,-294.46 191.03,-295.19 188.53,-295.89 185.97,-296.56 183.36,-297.19 180.7,-297.79 178,-298.34 175.26,-298.85 172.5,-299.32 169.7,-299.75 166.89,-300.14 164.06,-300.47 161.21,-300.76 158.35,-301.01 155.48,-301.2 152.61,-301.35 149.73,-301.45 146.84,-301.5 143.96,-301.5 141.08,-301.45 138.2,-301.35 135.32,-301.2 132.45,-301.01 129.59,-300.76 126.75,-300.47 123.91,-300.14 121.1,-299.75 118.31,-299.32 115.54,-298.85 112.8,-298.34 110.1,-297.79 107.44,-297.19 104.83,-296.56 102.27,-295.89 99.77,-295.19 97.34,-294.46 94.99,-293.7 92.72,-292.91 90.54,-292.09 88.46,-291.25 86.5,-290.39 84.66,-289.51 82.94,-288.61 81.37,-287.7 79.95,-286.78 78.68,-285.85 77.58,-284.91 76.66,-283.97 75.93,-283.03 75.38,-282.09 75.04,-281.15 74.91,-280.22 74.99,-279.3 75.29,-278.39 75.81,-277.49 76.56,-276.61 77.54,-275.75 78.76,-274.91 80.2,-274.09 81.87,-273.3 83.77,-272.54 85.89,-271.81 88.24,-271.11 90.8,-270.44 93.57,-269.81 96.53,-269.21 99.69,-268.66 103.02,-268.15 106.52,-267.68 110.18,-267.25 113.98,-266.86 117.9,-266.53 121.94,-266.24 126.07,-265.99 130.29,-265.8 134.56,-265.65 138.88,-265.55 143.22,-265.5 147.58,-265.5 151.93,-265.55\"/>\n",
+       "<text text-anchor=\"middle\" x=\"145.4\" y=\"-278.45\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(q),neg(r)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(p)]&#45;&gt;[neg(q),neg(r)] -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>[neg(p)]&#45;&gt;[neg(q),neg(r)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M145.4,-353.91C145.4,-342.26 145.4,-326.55 145.4,-313.02\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"148.9,-313.36 145.4,-303.36 141.9,-313.36 148.9,-313.36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"148.78\" y=\"-322.7\" font-family=\"Times,serif\" font-size=\"14.00\">p</text>\n",
+       "</g>\n",
+       "<!-- [neg(s),neg(r)] -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>[neg(s),neg(r)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"75.82,-177.05 80.08,-177.15 84.28,-177.3 88.43,-177.49 92.5,-177.74 96.48,-178.03 100.34,-178.36 104.08,-178.75 107.68,-179.18 111.13,-179.65 114.41,-180.16 117.52,-180.71 120.44,-181.31 123.16,-181.94 125.68,-182.61 127.99,-183.31 130.08,-184.04 131.95,-184.8 133.6,-185.59 135.02,-186.41 136.21,-187.25 137.18,-188.11 137.91,-188.99 138.43,-189.89 138.72,-190.8 138.8,-191.72 138.67,-192.65 138.34,-193.59 137.8,-194.53 137.08,-195.47 136.17,-196.41 135.09,-197.35 133.85,-198.28 132.44,-199.2 130.9,-200.11 129.21,-201.01 127.39,-201.89 125.46,-202.75 123.42,-203.59 121.27,-204.41 119.04,-205.2 116.72,-205.96 114.33,-206.69 111.87,-207.39 109.35,-208.06 106.77,-208.69 104.15,-209.29 101.5,-209.84 98.8,-210.35 96.08,-210.82 93.33,-211.25 90.56,-211.64 87.77,-211.97 84.97,-212.26 82.15,-212.51 79.33,-212.7 76.5,-212.85 73.66,-212.95 70.82,-213 67.98,-213 65.14,-212.95 62.31,-212.85 59.48,-212.7 56.65,-212.51 53.84,-212.26 51.04,-211.97 48.25,-211.64 45.48,-211.25 42.73,-210.82 40,-210.35 37.31,-209.84 34.65,-209.29 32.03,-208.69 29.46,-208.06 26.94,-207.39 24.48,-206.69 22.09,-205.96 19.77,-205.2 17.53,-204.41 15.39,-203.59 13.35,-202.75 11.41,-201.89 9.6,-201.01 7.91,-200.11 6.36,-199.2 4.96,-198.28 3.71,-197.35 2.63,-196.41 1.72,-195.47 1,-194.53 0.47,-193.59 0.13,-192.65 0,-191.72 0.08,-190.8 0.37,-189.89 0.89,-188.99 1.63,-188.11 2.59,-187.25 3.79,-186.41 5.21,-185.59 6.85,-184.8 8.72,-184.04 10.81,-183.31 13.12,-182.61 15.64,-181.94 18.37,-181.31 21.29,-180.71 24.39,-180.16 27.68,-179.65 31.12,-179.18 34.72,-178.75 38.46,-178.36 42.33,-178.03 46.3,-177.74 50.37,-177.49 54.52,-177.3 58.73,-177.15 62.98,-177.05 67.26,-177 71.55,-177 75.82,-177.05\"/>\n",
+       "<text text-anchor=\"middle\" x=\"69.4\" y=\"-189.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(s),neg(r)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(q),neg(r)]&#45;&gt;[neg(s),neg(r)] -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>[neg(q),neg(r)]&#45;&gt;[neg(s),neg(r)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M130.39,-265.41C119.28,-252.77 103.98,-235.36 91.48,-221.13\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"94.36,-219.1 85.13,-213.9 89.1,-223.72 94.36,-219.1\"/>\n",
+       "<text text-anchor=\"middle\" x=\"117.78\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">q</text>\n",
+       "</g>\n",
+       "<!-- [neg(t),neg(r)] -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>[neg(t),neg(r)]</title>\n",
+       "<ellipse fill=\"none\" stroke=\"red\" cx=\"221.4\" cy=\"-195\" rx=\"64.15\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"221.4\" y=\"-189.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(t),neg(r)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(q),neg(r)]&#45;&gt;[neg(t),neg(r)] -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>[neg(q),neg(r)]&#45;&gt;[neg(t),neg(r)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M160.42,-265.41C171.52,-252.77 186.82,-235.36 199.32,-221.13\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"201.71,-223.72 205.68,-213.9 196.45,-219.1 201.71,-223.72\"/>\n",
+       "<text text-anchor=\"middle\" x=\"192.78\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">q</text>\n",
+       "</g>\n",
+       "<!-- [neg(r)] -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>[neg(r)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"73.3,-88.55 75.88,-88.65 78.44,-88.8 80.96,-88.99 83.43,-89.24 85.84,-89.53 88.19,-89.86 90.46,-90.25 92.65,-90.68 94.74,-91.15 96.74,-91.66 98.62,-92.21 100.4,-92.81 102.05,-93.44 103.58,-94.11 104.98,-94.81 106.25,-95.54 107.39,-96.3 108.39,-97.09 109.25,-97.91 109.98,-98.75 110.56,-99.61 111.01,-100.49 111.32,-101.39 111.5,-102.3 111.55,-103.22 111.47,-104.15 111.27,-105.09 110.94,-106.03 110.5,-106.97 109.95,-107.91 109.3,-108.85 108.54,-109.78 107.69,-110.7 106.75,-111.61 105.72,-112.51 104.62,-113.39 103.45,-114.25 102.21,-115.09 100.9,-115.91 99.55,-116.7 98.14,-117.46 96.69,-118.19 95.19,-118.89 93.66,-119.56 92.1,-120.19 90.51,-120.79 88.89,-121.34 87.26,-121.85 85.6,-122.32 83.93,-122.75 82.25,-123.14 80.56,-123.47 78.85,-123.76 77.14,-124.01 75.43,-124.2 73.71,-124.35 71.99,-124.45 70.26,-124.5 68.54,-124.5 66.82,-124.45 65.09,-124.35 63.37,-124.2 61.66,-124.01 59.95,-123.76 58.25,-123.47 56.55,-123.14 54.87,-122.75 53.2,-122.32 51.55,-121.85 49.91,-121.34 48.3,-120.79 46.71,-120.19 45.14,-119.56 43.61,-118.89 42.12,-118.19 40.67,-117.46 39.26,-116.7 37.9,-115.91 36.6,-115.09 35.36,-114.25 34.18,-113.39 33.08,-112.51 32.06,-111.61 31.11,-110.7 30.26,-109.78 29.51,-108.85 28.85,-107.91 28.3,-106.97 27.86,-106.03 27.54,-105.09 27.33,-104.15 27.25,-103.22 27.3,-102.3 27.48,-101.39 27.79,-100.49 28.24,-99.61 28.83,-98.75 29.55,-97.91 30.41,-97.09 31.41,-96.3 32.55,-95.54 33.82,-94.81 35.22,-94.11 36.75,-93.44 38.41,-92.81 40.18,-92.21 42.07,-91.66 44.06,-91.15 46.15,-90.68 48.34,-90.25 50.61,-89.86 52.96,-89.53 55.37,-89.24 57.85,-88.99 60.36,-88.8 62.92,-88.65 65.5,-88.55 68.1,-88.5 70.7,-88.5 73.3,-88.55\"/>\n",
+       "<text text-anchor=\"middle\" x=\"69.4\" y=\"-101.45\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(r)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(r)]&#45;&gt;[] -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>[neg(r)]&#45;&gt;[]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M69.4,-88.41C69.4,-76.76 69.4,-61.05 69.4,-47.52\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"72.9,-47.86 69.4,-37.86 65.9,-47.86 72.9,-47.86\"/>\n",
+       "<text text-anchor=\"middle\" x=\"71.65\" y=\"-57.2\" font-family=\"Times,serif\" font-size=\"14.00\">r</text>\n",
+       "</g>\n",
+       "<!-- [neg(s),neg(r)]&#45;&gt;[neg(r)] -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>[neg(s),neg(r)]&#45;&gt;[neg(r)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M69.4,-176.91C69.4,-165.26 69.4,-149.55 69.4,-136.02\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"72.9,-136.36 69.4,-126.36 65.9,-136.36 72.9,-136.36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"72.03\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">s</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n"
+      ],
       "text/plain": [
        "digraph {\n",
        "\"[]\" [shape=\"rect\", color=\"green\"]\n",
@@ -819,7 +903,429 @@
    "outputs": [
     {
      "data": {
-      "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 7.0.0 (20221023.0053)\n -->\n<!-- Pages: 1 -->\n<svg width=\"1101pt\" height=\"1175pt\"\n viewBox=\"0.00 0.00 1101.41 1175.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 1171)\">\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-1171 1097.41,-1171 1097.41,4 -4,4\"/>\n<!-- [] -->\n<g id=\"node1\" class=\"node\">\n<title>[]</title>\n<polygon fill=\"none\" stroke=\"green\" points=\"512.36,-123 458.36,-123 458.36,-87 512.36,-87 512.36,-123\"/>\n<text text-anchor=\"middle\" x=\"485.36\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[]</text>\n</g>\n<!-- [neg(a),neg(b),neg(and2)] -->\n<g id=\"node2\" class=\"node\">\n<title>[neg(a),neg(b),neg(and2)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"119.47,-87.05 126.16,-87.15 132.78,-87.3 139.31,-87.49 145.71,-87.74 151.96,-88.03 158.05,-88.36 163.93,-88.75 169.6,-89.18 175.02,-89.65 180.19,-90.16 185.08,-90.71 189.67,-91.31 193.96,-91.94 197.93,-92.61 201.56,-93.31 204.85,-94.04 207.8,-94.8 210.39,-95.59 212.62,-96.41 214.5,-97.25 216.01,-98.11 217.18,-98.99 217.99,-99.89 218.45,-100.8 218.58,-101.72 218.37,-102.65 217.84,-103.59 217,-104.53 215.86,-105.47 214.44,-106.41 212.74,-107.35 210.78,-108.28 208.57,-109.2 206.13,-110.11 203.48,-111.01 200.62,-111.89 197.58,-112.75 194.36,-113.59 190.99,-114.41 187.47,-115.2 183.82,-115.96 180.06,-116.69 176.18,-117.39 172.22,-118.06 168.17,-118.69 164.05,-119.29 159.87,-119.84 155.63,-120.35 151.34,-120.82 147.01,-121.25 142.65,-121.64 138.26,-121.97 133.85,-122.26 129.42,-122.51 124.98,-122.7 120.52,-122.85 116.06,-122.95 111.59,-123 107.13,-123 102.66,-122.95 98.2,-122.85 93.74,-122.7 89.3,-122.51 84.87,-122.26 80.46,-121.97 76.07,-121.64 71.71,-121.25 67.38,-120.82 63.09,-120.35 58.85,-119.84 54.67,-119.29 50.55,-118.69 46.5,-118.06 42.53,-117.39 38.66,-116.69 34.9,-115.96 31.25,-115.2 27.73,-114.41 24.36,-113.59 21.14,-112.75 18.1,-111.89 15.24,-111.01 12.59,-110.11 10.15,-109.2 7.94,-108.28 5.98,-107.35 4.28,-106.41 2.85,-105.47 1.71,-104.53 0.88,-103.59 0.35,-102.65 0.14,-101.72 0.27,-100.8 0.73,-99.89 1.54,-98.99 2.7,-98.11 4.22,-97.25 6.1,-96.41 8.33,-95.59 10.92,-94.8 13.87,-94.04 17.16,-93.31 20.79,-92.61 24.76,-91.94 29.04,-91.31 33.64,-90.71 38.53,-90.16 43.69,-89.65 49.12,-89.18 54.79,-88.75 60.67,-88.36 66.75,-88.03 73.01,-87.74 79.41,-87.49 85.94,-87.3 92.56,-87.15 99.25,-87.05 105.99,-87 112.73,-87 119.47,-87.05\"/>\n<text text-anchor=\"middle\" x=\"109.36\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(a),neg(b),neg(and2)]</text>\n</g>\n<!-- [neg(b),neg(and2)] -->\n<g id=\"node9\" class=\"node\">\n<title>[neg(b),neg(and2)]</title>\n<ellipse fill=\"none\" stroke=\"red\" cx=\"109.36\" cy=\"-18\" rx=\"77.19\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"109.36\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(b),neg(and2)]</text>\n</g>\n<!-- [neg(a),neg(b),neg(and2)]&#45;&gt;[neg(b),neg(and2)] -->\n<g id=\"edge1\" class=\"edge\">\n<title>[neg(a),neg(b),neg(and2)]&#45;&gt;[neg(b),neg(and2)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M109.36,-86.8C109.36,-75.58 109.36,-60.67 109.36,-47.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"112.86,-47.98 109.36,-37.98 105.86,-47.98 112.86,-47.98\"/>\n<text text-anchor=\"middle\" x=\"112.86\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">a</text>\n</g>\n<!-- [neg(and11),neg(and2)] -->\n<g id=\"node3\" class=\"node\">\n<title>[neg(and11),neg(and2)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"122.72,-174.05 128.91,-174.15 135.04,-174.3 141.08,-174.49 147.01,-174.74 152.8,-175.03 158.43,-175.36 163.88,-175.75 169.12,-176.18 174.15,-176.65 178.93,-177.16 183.46,-177.71 187.71,-178.31 191.68,-178.94 195.35,-179.61 198.71,-180.31 201.76,-181.04 204.48,-181.8 206.88,-182.59 208.95,-183.41 210.69,-184.25 212.09,-185.11 213.17,-185.99 213.92,-186.89 214.35,-187.8 214.47,-188.72 214.28,-189.65 213.79,-190.59 213.01,-191.53 211.95,-192.47 210.63,-193.41 209.06,-194.35 207.24,-195.28 205.2,-196.2 202.94,-197.11 200.49,-198.01 197.84,-198.89 195.02,-199.75 192.05,-200.59 188.93,-201.41 185.67,-202.2 182.29,-202.96 178.81,-203.69 175.22,-204.39 171.55,-205.06 167.8,-205.69 163.99,-206.29 160.11,-206.84 156.19,-207.35 152.22,-207.82 148.22,-208.25 144.18,-208.64 140.12,-208.97 136.03,-209.26 131.93,-209.51 127.82,-209.7 123.69,-209.85 119.56,-209.95 115.43,-210 111.29,-210 107.16,-209.95 103.02,-209.85 98.9,-209.7 94.79,-209.51 90.69,-209.26 86.6,-208.97 82.54,-208.64 78.5,-208.25 74.5,-207.82 70.53,-207.35 66.6,-206.84 62.73,-206.29 58.92,-205.69 55.17,-205.06 51.5,-204.39 47.91,-203.69 44.43,-202.96 41.05,-202.2 37.79,-201.41 34.67,-200.59 31.69,-199.75 28.88,-198.89 26.23,-198.01 23.77,-197.11 21.52,-196.2 19.47,-195.28 17.66,-194.35 16.09,-193.41 14.76,-192.47 13.71,-191.53 12.93,-190.59 12.44,-189.65 12.25,-188.72 12.37,-187.8 12.8,-186.89 13.55,-185.99 14.63,-185.11 16.03,-184.25 17.77,-183.41 19.84,-182.59 22.23,-181.8 24.96,-181.04 28.01,-180.31 31.37,-179.61 35.04,-178.94 39.01,-178.31 43.26,-177.71 47.79,-177.16 52.57,-176.65 57.59,-176.18 62.84,-175.75 68.29,-175.36 73.92,-175.03 79.71,-174.74 85.64,-174.49 91.68,-174.3 97.81,-174.15 104,-174.05 110.24,-174 116.48,-174 122.72,-174.05\"/>\n<text text-anchor=\"middle\" x=\"113.36\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(and11),neg(and2)]</text>\n</g>\n<!-- [neg(and11),neg(and2)]&#45;&gt;[neg(a),neg(b),neg(and2)] -->\n<g id=\"edge2\" class=\"edge\">\n<title>[neg(and11),neg(and2)]&#45;&gt;[neg(a),neg(b),neg(and2)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M112.55,-173.8C112.02,-162.58 111.32,-147.67 110.71,-134.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"114.22,-134.8 110.25,-124.98 107.23,-135.13 114.22,-134.8\"/>\n<text text-anchor=\"middle\" x=\"129.36\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">and11</text>\n</g>\n<!-- [neg(and12)] -->\n<g id=\"node4\" class=\"node\">\n<title>[neg(and12)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"612.95,-174.05 616.65,-174.15 620.32,-174.3 623.93,-174.49 627.47,-174.74 630.93,-175.03 634.3,-175.36 637.56,-175.75 640.69,-176.18 643.69,-176.65 646.55,-177.16 649.26,-177.71 651.8,-178.31 654.17,-178.94 656.37,-179.61 658.38,-180.31 660.2,-181.04 661.83,-181.8 663.26,-182.59 664.5,-183.41 665.54,-184.25 666.38,-185.11 667.02,-185.99 667.47,-186.89 667.72,-187.8 667.79,-188.72 667.68,-189.65 667.39,-190.59 666.92,-191.53 666.29,-192.47 665.5,-193.41 664.56,-194.35 663.48,-195.28 662.26,-196.2 660.91,-197.11 659.44,-198.01 657.86,-198.89 656.17,-199.75 654.39,-200.59 652.53,-201.41 650.58,-202.2 648.56,-202.96 646.48,-203.69 644.34,-204.39 642.14,-205.06 639.9,-205.69 637.62,-206.29 635.31,-206.84 632.96,-207.35 630.59,-207.82 628.19,-208.25 625.78,-208.64 623.35,-208.97 620.91,-209.26 618.46,-209.51 616,-209.7 613.54,-209.85 611.07,-209.95 608.6,-210 606.12,-210 603.65,-209.95 601.18,-209.85 598.72,-209.7 596.26,-209.51 593.81,-209.26 591.37,-208.97 588.94,-208.64 586.52,-208.25 584.13,-207.82 581.76,-207.35 579.41,-206.84 577.1,-206.29 574.82,-205.69 572.58,-205.06 570.38,-204.39 568.24,-203.69 566.16,-202.96 564.14,-202.2 562.19,-201.41 560.32,-200.59 558.55,-199.75 556.86,-198.89 555.28,-198.01 553.81,-197.11 552.46,-196.2 551.24,-195.28 550.16,-194.35 549.22,-193.41 548.43,-192.47 547.8,-191.53 547.33,-190.59 547.04,-189.65 546.92,-188.72 546.99,-187.8 547.25,-186.89 547.7,-185.99 548.34,-185.11 549.18,-184.25 550.22,-183.41 551.46,-182.59 552.89,-181.8 554.52,-181.04 556.34,-180.31 558.35,-179.61 560.55,-178.94 562.92,-178.31 565.46,-177.71 568.17,-177.16 571.02,-176.65 574.03,-176.18 577.16,-175.75 580.42,-175.36 583.78,-175.03 587.25,-174.74 590.79,-174.49 594.4,-174.3 598.06,-174.15 601.77,-174.05 605.49,-174 609.23,-174 612.95,-174.05\"/>\n<text text-anchor=\"middle\" x=\"607.36\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(and12)]</text>\n</g>\n<!-- [neg(c),neg(d)] -->\n<g id=\"node10\" class=\"node\">\n<title>[neg(c),neg(d)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"607.7,-87.05 611.9,-87.15 616.06,-87.3 620.15,-87.49 624.17,-87.74 628.1,-88.03 631.92,-88.36 635.61,-88.75 639.16,-89.18 642.57,-89.65 645.81,-90.16 648.88,-90.71 651.76,-91.31 654.45,-91.94 656.94,-92.61 659.22,-93.31 661.29,-94.04 663.14,-94.8 664.76,-95.59 666.17,-96.41 667.34,-97.25 668.3,-98.11 669.03,-98.99 669.53,-99.89 669.83,-100.8 669.9,-101.72 669.78,-102.65 669.44,-103.59 668.92,-104.53 668.2,-105.47 667.31,-106.41 666.24,-107.35 665.01,-108.28 663.62,-109.2 662.09,-110.11 660.43,-111.01 658.63,-111.89 656.72,-112.75 654.71,-113.59 652.59,-114.41 650.38,-115.2 648.09,-115.96 645.73,-116.69 643.3,-117.39 640.81,-118.06 638.27,-118.69 635.68,-119.29 633.06,-119.84 630.4,-120.35 627.71,-120.82 624.99,-121.25 622.25,-121.64 619.5,-121.97 616.73,-122.26 613.95,-122.51 611.16,-122.7 608.37,-122.85 605.56,-122.95 602.76,-123 599.96,-123 597.15,-122.95 594.35,-122.85 591.56,-122.7 588.77,-122.51 585.99,-122.26 583.22,-121.97 580.47,-121.64 577.73,-121.25 575.01,-120.82 572.32,-120.35 569.66,-119.84 567.04,-119.29 564.45,-118.69 561.91,-118.06 559.42,-117.39 556.99,-116.69 554.63,-115.96 552.34,-115.2 550.13,-114.41 548.01,-113.59 545.99,-112.75 544.08,-111.89 542.29,-111.01 540.63,-110.11 539.1,-109.2 537.71,-108.28 536.48,-107.35 535.41,-106.41 534.52,-105.47 533.8,-104.53 533.28,-103.59 532.94,-102.65 532.81,-101.72 532.89,-100.8 533.18,-99.89 533.69,-98.99 534.42,-98.11 535.38,-97.25 536.55,-96.41 537.96,-95.59 539.58,-94.8 541.43,-94.04 543.5,-93.31 545.78,-92.61 548.26,-91.94 550.95,-91.31 553.84,-90.71 556.91,-90.16 560.15,-89.65 563.55,-89.18 567.11,-88.75 570.8,-88.36 574.62,-88.03 578.55,-87.74 582.56,-87.49 586.66,-87.3 590.82,-87.15 595.02,-87.05 599.24,-87 603.48,-87 607.7,-87.05\"/>\n<text text-anchor=\"middle\" x=\"601.36\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(c),neg(d)]</text>\n</g>\n<!-- [neg(and12)]&#45;&gt;[neg(c),neg(d)] -->\n<g id=\"edge3\" class=\"edge\">\n<title>[neg(and12)]&#45;&gt;[neg(c),neg(d)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M606.15,-173.8C605.35,-162.58 604.3,-147.67 603.38,-134.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"606.89,-134.71 602.7,-124.98 599.91,-135.2 606.89,-134.71\"/>\n<text text-anchor=\"middle\" x=\"622.36\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">and12</text>\n</g>\n<!-- [neg(and12),neg(not2),neg(or4)] -->\n<g id=\"node5\" class=\"node\">\n<title>[neg(and12),neg(not2),neg(or4)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"695.76,-696.05 703.98,-696.15 712.11,-696.3 720.12,-696.49 727.97,-696.74 735.65,-697.03 743.12,-697.36 750.34,-697.75 757.3,-698.18 763.96,-698.65 770.3,-699.16 776.3,-699.71 781.94,-700.31 787.2,-700.94 792.06,-701.61 796.52,-702.31 800.56,-703.04 804.18,-703.8 807.36,-704.59 810.1,-705.41 812.4,-706.25 814.27,-707.11 815.69,-707.99 816.69,-708.89 817.26,-709.8 817.41,-710.72 817.16,-711.65 816.51,-712.59 815.48,-713.53 814.08,-714.47 812.33,-715.41 810.24,-716.35 807.84,-717.28 805.13,-718.2 802.14,-719.11 798.88,-720.01 795.37,-720.89 791.64,-721.75 787.69,-722.59 783.55,-723.41 779.23,-724.2 774.75,-724.96 770.13,-725.69 765.38,-726.39 760.51,-727.06 755.54,-727.69 750.49,-728.29 745.35,-728.84 740.15,-729.35 734.88,-729.82 729.57,-730.25 724.22,-730.64 718.84,-730.97 713.42,-731.26 707.98,-731.51 702.53,-731.7 697.06,-731.85 691.58,-731.95 686.1,-732 680.62,-732 675.13,-731.95 669.66,-731.85 664.19,-731.7 658.73,-731.51 653.3,-731.26 647.88,-730.97 642.5,-730.64 637.14,-730.25 631.83,-729.82 626.57,-729.35 621.37,-728.84 616.23,-728.29 611.17,-727.69 606.21,-727.06 601.34,-726.39 596.59,-725.69 591.96,-724.96 587.49,-724.2 583.17,-723.41 579.03,-722.59 575.08,-721.75 571.35,-720.89 567.84,-720.01 564.58,-719.11 561.59,-718.2 558.88,-717.28 556.48,-716.35 554.39,-715.41 552.64,-714.47 551.24,-713.53 550.21,-712.59 549.56,-711.65 549.31,-710.72 549.46,-709.8 550.03,-708.89 551.02,-707.99 552.45,-707.11 554.32,-706.25 556.62,-705.41 559.36,-704.59 562.54,-703.8 566.15,-703.04 570.19,-702.31 574.65,-701.61 579.52,-700.94 584.78,-700.31 590.42,-699.71 596.42,-699.16 602.76,-698.65 609.42,-698.18 616.38,-697.75 623.6,-697.36 631.07,-697.03 638.74,-696.74 646.6,-696.49 654.61,-696.3 662.74,-696.15 670.95,-696.05 679.22,-696 687.5,-696 695.76,-696.05\"/>\n<text text-anchor=\"middle\" x=\"683.36\" y=\"-710.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(and12),neg(not2),neg(or4)]</text>\n</g>\n<!-- [neg(c),neg(d),neg(not2),neg(or4)] -->\n<g id=\"node11\" class=\"node\">\n<title>[neg(c),neg(d),neg(not2),neg(or4)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"694.56,-609.05 703.3,-609.15 711.95,-609.3 720.48,-609.49 728.84,-609.74 737.01,-610.03 744.96,-610.36 752.64,-610.75 760.04,-611.18 767.13,-611.65 773.88,-612.16 780.27,-612.71 786.27,-613.31 791.87,-613.94 797.05,-614.61 801.79,-615.31 806.09,-616.04 809.94,-616.8 813.32,-617.59 816.24,-618.41 818.69,-619.25 820.68,-620.11 822.19,-620.99 823.25,-621.89 823.86,-622.8 824.02,-623.72 823.75,-624.65 823.06,-625.59 821.97,-626.53 820.48,-627.47 818.62,-628.41 816.39,-629.35 813.83,-630.28 810.95,-631.2 807.77,-632.11 804.3,-633.01 800.57,-633.89 796.59,-634.75 792.39,-635.59 787.98,-636.41 783.39,-637.2 778.62,-637.96 773.71,-638.69 768.65,-639.39 763.47,-640.06 758.18,-640.69 752.8,-641.29 747.33,-641.84 741.79,-642.35 736.19,-642.82 730.54,-643.25 724.85,-643.64 719.11,-643.97 713.35,-644.26 707.57,-644.51 701.76,-644.7 695.94,-644.85 690.11,-644.95 684.28,-645 678.44,-645 672.61,-644.95 666.78,-644.85 660.96,-644.7 655.15,-644.51 649.37,-644.26 643.6,-643.97 637.87,-643.64 632.18,-643.25 626.52,-642.82 620.92,-642.35 615.39,-641.84 609.92,-641.29 604.54,-640.69 599.25,-640.06 594.07,-639.39 589.01,-638.69 584.09,-637.96 579.33,-637.2 574.73,-636.41 570.33,-635.59 566.13,-634.75 562.15,-633.89 558.42,-633.01 554.95,-632.11 551.77,-631.2 548.89,-630.28 546.32,-629.35 544.1,-628.41 542.24,-627.47 540.75,-626.53 539.65,-625.59 538.96,-624.65 538.69,-623.72 538.86,-622.8 539.46,-621.89 540.52,-620.99 542.04,-620.11 544.03,-619.25 546.48,-618.41 549.4,-617.59 552.78,-616.8 556.63,-616.04 560.93,-615.31 565.67,-614.61 570.85,-613.94 576.45,-613.31 582.45,-612.71 588.84,-612.16 595.59,-611.65 602.67,-611.18 610.08,-610.75 617.76,-610.36 625.71,-610.03 633.88,-609.74 642.24,-609.49 650.77,-609.3 659.42,-609.15 668.16,-609.05 676.95,-609 685.77,-609 694.56,-609.05\"/>\n<text text-anchor=\"middle\" x=\"681.36\" y=\"-623.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(c),neg(d),neg(not2),neg(or4)]</text>\n</g>\n<!-- [neg(and12),neg(not2),neg(or4)]&#45;&gt;[neg(c),neg(d),neg(not2),neg(or4)] -->\n<g id=\"edge4\" class=\"edge\">\n<title>[neg(and12),neg(not2),neg(or4)]&#45;&gt;[neg(c),neg(d),neg(not2),neg(or4)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M682.95,-695.8C682.69,-684.58 682.34,-669.67 682.03,-656.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"685.54,-656.9 681.81,-646.98 678.54,-657.06 685.54,-656.9\"/>\n<text text-anchor=\"middle\" x=\"699.36\" y=\"-666.8\" font-family=\"Times,serif\" font-size=\"14.00\">and12</text>\n</g>\n<!-- [neg(and3)] -->\n<g id=\"node6\" class=\"node\">\n<title>[neg(and3)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"356.47,-348.05 359.86,-348.15 363.21,-348.3 366.51,-348.49 369.75,-348.74 372.91,-349.03 375.99,-349.36 378.96,-349.75 381.83,-350.18 384.57,-350.65 387.19,-351.16 389.66,-351.71 391.98,-352.31 394.15,-352.94 396.16,-353.61 397.99,-354.31 399.66,-355.04 401.15,-355.8 402.46,-356.59 403.59,-357.41 404.54,-358.25 405.31,-359.11 405.89,-359.99 406.3,-360.89 406.54,-361.8 406.6,-362.72 406.5,-363.65 406.23,-364.59 405.81,-365.53 405.23,-366.47 404.51,-367.41 403.65,-368.35 402.66,-369.28 401.54,-370.2 400.31,-371.11 398.96,-372.01 397.52,-372.89 395.98,-373.75 394.35,-374.59 392.65,-375.41 390.87,-376.2 389.02,-376.96 387.12,-377.69 385.16,-378.39 383.15,-379.06 381.11,-379.69 379.02,-380.29 376.91,-380.84 374.76,-381.35 372.59,-381.82 370.4,-382.25 368.2,-382.64 365.98,-382.97 363.75,-383.26 361.51,-383.51 359.26,-383.7 357.01,-383.85 354.75,-383.95 352.49,-384 350.23,-384 347.97,-383.95 345.71,-383.85 343.46,-383.7 341.21,-383.51 338.97,-383.26 336.74,-382.97 334.52,-382.64 332.31,-382.25 330.13,-381.82 327.96,-381.35 325.81,-380.84 323.7,-380.29 321.61,-379.69 319.56,-379.06 317.56,-378.39 315.6,-377.69 313.7,-376.96 311.85,-376.2 310.07,-375.41 308.36,-374.59 306.74,-373.75 305.2,-372.89 303.75,-372.01 302.41,-371.11 301.18,-370.2 300.06,-369.28 299.07,-368.35 298.21,-367.41 297.49,-366.47 296.91,-365.53 296.49,-364.59 296.22,-363.65 296.12,-362.72 296.18,-361.8 296.41,-360.89 296.82,-359.99 297.41,-359.11 298.18,-358.25 299.13,-357.41 300.26,-356.59 301.57,-355.8 303.06,-355.04 304.72,-354.31 306.56,-353.61 308.57,-352.94 310.74,-352.31 313.06,-351.71 315.53,-351.16 318.15,-350.65 320.89,-350.18 323.76,-349.75 326.73,-349.36 329.81,-349.03 332.97,-348.74 336.21,-348.49 339.51,-348.3 342.86,-348.15 346.25,-348.05 349.65,-348 353.07,-348 356.47,-348.05\"/>\n<text text-anchor=\"middle\" x=\"351.36\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(and3)]</text>\n</g>\n<!-- [neg(or21),neg(and2)] -->\n<g id=\"node26\" class=\"node\">\n<title>[neg(or21),neg(and2)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"327.12,-261.05 332.92,-261.15 338.66,-261.3 344.31,-261.49 349.86,-261.74 355.28,-262.03 360.55,-262.36 365.65,-262.75 370.56,-263.18 375.26,-263.65 379.74,-264.16 383.98,-264.71 387.96,-265.31 391.67,-265.94 395.11,-266.61 398.26,-267.31 401.11,-268.04 403.66,-268.8 405.91,-269.59 407.84,-270.41 409.47,-271.25 410.79,-272.11 411.79,-272.99 412.5,-273.89 412.9,-274.8 413.01,-275.72 412.83,-276.65 412.37,-277.59 411.64,-278.53 410.66,-279.47 409.42,-280.41 407.95,-281.35 406.25,-282.28 404.33,-283.2 402.22,-284.11 399.92,-285.01 397.45,-285.89 394.81,-286.75 392.02,-287.59 389.1,-288.41 386.05,-289.2 382.89,-289.96 379.62,-290.69 376.27,-291.39 372.83,-292.06 369.33,-292.69 365.75,-293.29 362.13,-293.84 358.45,-294.35 354.74,-294.82 350.99,-295.25 347.21,-295.64 343.41,-295.97 339.58,-296.26 335.75,-296.51 331.89,-296.7 328.03,-296.85 324.17,-296.95 320.3,-297 316.42,-297 312.55,-296.95 308.69,-296.85 304.82,-296.7 300.97,-296.51 297.13,-296.26 293.31,-295.97 289.51,-295.64 285.73,-295.25 281.98,-294.82 278.26,-294.35 274.59,-293.84 270.96,-293.29 267.39,-292.69 263.88,-292.06 260.45,-291.39 257.09,-290.69 253.83,-289.96 250.67,-289.2 247.62,-288.41 244.7,-287.59 241.91,-286.75 239.27,-285.89 236.8,-285.01 234.5,-284.11 232.38,-283.2 230.47,-282.28 228.77,-281.35 227.3,-280.41 226.06,-279.47 225.07,-278.53 224.35,-277.59 223.89,-276.65 223.71,-275.72 223.82,-274.8 224.22,-273.89 224.92,-272.99 225.93,-272.11 227.25,-271.25 228.87,-270.41 230.81,-269.59 233.06,-268.8 235.61,-268.04 238.46,-267.31 241.61,-266.61 245.04,-265.94 248.76,-265.31 252.74,-264.71 256.98,-264.16 261.45,-263.65 266.16,-263.18 271.07,-262.75 276.17,-262.36 281.44,-262.03 286.86,-261.74 292.41,-261.49 298.06,-261.3 303.8,-261.15 309.6,-261.05 315.44,-261 321.28,-261 327.12,-261.05\"/>\n<text text-anchor=\"middle\" x=\"318.36\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(or21),neg(and2)]</text>\n</g>\n<!-- [neg(and3)]&#45;&gt;[neg(or21),neg(and2)] -->\n<g id=\"edge5\" class=\"edge\">\n<title>[neg(and3)]&#45;&gt;[neg(or21),neg(and2)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M344.68,-347.8C340.21,-336.28 334.22,-320.86 329.09,-307.63\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"332.46,-306.64 325.58,-298.59 325.93,-309.18 332.46,-306.64\"/>\n<text text-anchor=\"middle\" x=\"350.86\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">and3</text>\n</g>\n<!-- [neg(and4),neg(or4)] -->\n<g id=\"node7\" class=\"node\">\n<title>[neg(and4),neg(or4)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"557.77,-957.05 563.33,-957.15 568.84,-957.3 574.27,-957.49 579.59,-957.74 584.8,-958.03 589.85,-958.36 594.75,-958.75 599.46,-959.18 603.98,-959.65 608.27,-960.16 612.34,-960.71 616.16,-961.31 619.73,-961.94 623.02,-962.61 626.05,-963.31 628.78,-964.04 631.23,-964.8 633.39,-965.59 635.25,-966.41 636.81,-967.25 638.07,-968.11 639.04,-968.99 639.71,-969.89 640.1,-970.8 640.2,-971.72 640.03,-972.65 639.59,-973.59 638.89,-974.53 637.95,-975.47 636.76,-976.41 635.34,-977.35 633.71,-978.28 631.88,-979.2 629.85,-980.11 627.64,-981.01 625.27,-981.89 622.73,-982.75 620.06,-983.59 617.25,-984.41 614.33,-985.2 611.29,-985.96 608.16,-986.69 604.94,-987.39 601.64,-988.06 598.28,-988.69 594.85,-989.29 591.37,-989.84 587.84,-990.35 584.28,-990.82 580.68,-991.25 577.05,-991.64 573.4,-991.97 569.73,-992.26 566.05,-992.51 562.35,-992.7 558.64,-992.85 554.93,-992.95 551.22,-993 547.5,-993 543.79,-992.95 540.07,-992.85 536.37,-992.7 532.67,-992.51 528.99,-992.26 525.32,-991.97 521.67,-991.64 518.04,-991.25 514.44,-990.82 510.88,-990.35 507.35,-989.84 503.87,-989.29 500.44,-988.69 497.08,-988.06 493.78,-987.39 490.56,-986.69 487.42,-985.96 484.39,-985.2 481.46,-984.41 478.66,-983.59 475.98,-982.75 473.45,-981.89 471.08,-981.01 468.87,-980.11 466.84,-979.2 465.01,-978.28 463.37,-977.35 461.96,-976.41 460.77,-975.47 459.83,-974.53 459.13,-973.59 458.69,-972.65 458.52,-971.72 458.62,-970.8 459.01,-969.89 459.68,-968.99 460.65,-968.11 461.91,-967.25 463.47,-966.41 465.33,-965.59 467.49,-964.8 469.93,-964.04 472.67,-963.31 475.69,-962.61 478.99,-961.94 482.56,-961.31 486.38,-960.71 490.45,-960.16 494.74,-959.65 499.26,-959.18 503.97,-958.75 508.86,-958.36 513.92,-958.03 519.13,-957.74 524.45,-957.49 529.88,-957.3 535.39,-957.15 540.95,-957.05 546.55,-957 552.17,-957 557.77,-957.05\"/>\n<text text-anchor=\"middle\" x=\"549.36\" y=\"-971.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(and4),neg(or4)]</text>\n</g>\n<!-- [neg(or3),neg(not2),neg(or4)] -->\n<g id=\"node30\" class=\"node\">\n<title>[neg(or3),neg(not2),neg(or4)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"560.81,-870.05 568.4,-870.15 575.9,-870.3 583.3,-870.49 590.56,-870.74 597.65,-871.03 604.54,-871.36 611.21,-871.75 617.63,-872.18 623.78,-872.65 629.64,-873.16 635.18,-873.71 640.39,-874.31 645.25,-874.94 649.74,-875.61 653.86,-876.31 657.59,-877.04 660.93,-877.8 663.86,-878.59 666.4,-879.41 668.52,-880.25 670.24,-881.11 671.56,-881.99 672.48,-882.89 673.01,-883.8 673.15,-884.72 672.91,-885.65 672.32,-886.59 671.36,-887.53 670.07,-888.47 668.46,-889.41 666.53,-890.35 664.31,-891.28 661.8,-892.2 659.04,-893.11 656.03,-894.01 652.79,-894.89 649.35,-895.75 645.7,-896.59 641.88,-897.41 637.89,-898.2 633.76,-898.96 629.49,-899.69 625.1,-900.39 620.61,-901.06 616.02,-901.69 611.35,-902.29 606.6,-902.84 601.8,-903.35 596.94,-903.82 592.04,-904.25 587.09,-904.64 582.12,-904.97 577.12,-905.26 572.1,-905.51 567.06,-905.7 562.01,-905.85 556.95,-905.95 551.89,-906 546.83,-906 541.76,-905.95 536.71,-905.85 531.66,-905.7 526.62,-905.51 521.6,-905.26 516.6,-904.97 511.63,-904.64 506.68,-904.25 501.78,-903.82 496.92,-903.35 492.12,-902.84 487.37,-902.29 482.7,-901.69 478.11,-901.06 473.62,-900.39 469.23,-899.69 464.96,-898.96 460.83,-898.2 456.84,-897.41 453.02,-896.59 449.37,-895.75 445.92,-894.89 442.69,-894.01 439.68,-893.11 436.91,-892.2 434.41,-891.28 432.19,-890.35 430.26,-889.41 428.65,-888.47 427.35,-887.53 426.4,-886.59 425.8,-885.65 425.57,-884.72 425.71,-883.8 426.24,-882.89 427.16,-881.99 428.48,-881.11 430.2,-880.25 432.32,-879.41 434.86,-878.59 437.79,-877.8 441.13,-877.04 444.86,-876.31 448.98,-875.61 453.47,-874.94 458.33,-874.31 463.54,-873.71 469.08,-873.16 474.93,-872.65 481.08,-872.18 487.51,-871.75 494.18,-871.36 501.07,-871.03 508.16,-870.74 515.42,-870.49 522.81,-870.3 530.32,-870.15 537.9,-870.05 545.54,-870 553.18,-870 560.81,-870.05\"/>\n<text text-anchor=\"middle\" x=\"549.36\" y=\"-884.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(or3),neg(not2),neg(or4)]</text>\n</g>\n<!-- [neg(and4),neg(or4)]&#45;&gt;[neg(or3),neg(not2),neg(or4)] -->\n<g id=\"edge6\" class=\"edge\">\n<title>[neg(and4),neg(or4)]&#45;&gt;[neg(or3),neg(not2),neg(or4)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M549.36,-956.8C549.36,-945.58 549.36,-930.67 549.36,-917.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"552.86,-917.98 549.36,-907.98 545.86,-917.98 552.86,-917.98\"/>\n<text text-anchor=\"middle\" x=\"562.86\" y=\"-927.8\" font-family=\"Times,serif\" font-size=\"14.00\">and4</text>\n</g>\n<!-- [neg(and5)] -->\n<g id=\"node8\" class=\"node\">\n<title>[neg(and5)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"554.47,-1044.05 557.86,-1044.15 561.21,-1044.3 564.51,-1044.49 567.75,-1044.74 570.91,-1045.03 573.99,-1045.36 576.96,-1045.75 579.83,-1046.18 582.57,-1046.65 585.19,-1047.16 587.66,-1047.71 589.98,-1048.31 592.15,-1048.94 594.16,-1049.61 595.99,-1050.31 597.66,-1051.04 599.15,-1051.8 600.46,-1052.59 601.59,-1053.41 602.54,-1054.25 603.31,-1055.11 603.89,-1055.99 604.3,-1056.89 604.54,-1057.8 604.6,-1058.72 604.5,-1059.65 604.23,-1060.59 603.81,-1061.53 603.23,-1062.47 602.51,-1063.41 601.65,-1064.35 600.66,-1065.28 599.54,-1066.2 598.31,-1067.11 596.96,-1068.01 595.52,-1068.89 593.98,-1069.75 592.35,-1070.59 590.65,-1071.41 588.87,-1072.2 587.02,-1072.96 585.12,-1073.69 583.16,-1074.39 581.15,-1075.06 579.11,-1075.69 577.02,-1076.29 574.91,-1076.84 572.76,-1077.35 570.59,-1077.82 568.4,-1078.25 566.2,-1078.64 563.98,-1078.97 561.75,-1079.26 559.51,-1079.51 557.26,-1079.7 555.01,-1079.85 552.75,-1079.95 550.49,-1080 548.23,-1080 545.97,-1079.95 543.71,-1079.85 541.46,-1079.7 539.21,-1079.51 536.97,-1079.26 534.74,-1078.97 532.52,-1078.64 530.31,-1078.25 528.13,-1077.82 525.96,-1077.35 523.81,-1076.84 521.7,-1076.29 519.61,-1075.69 517.56,-1075.06 515.56,-1074.39 513.6,-1073.69 511.7,-1072.96 509.85,-1072.2 508.07,-1071.41 506.36,-1070.59 504.74,-1069.75 503.2,-1068.89 501.75,-1068.01 500.41,-1067.11 499.18,-1066.2 498.06,-1065.28 497.07,-1064.35 496.21,-1063.41 495.49,-1062.47 494.91,-1061.53 494.49,-1060.59 494.22,-1059.65 494.12,-1058.72 494.18,-1057.8 494.41,-1056.89 494.82,-1055.99 495.41,-1055.11 496.18,-1054.25 497.13,-1053.41 498.26,-1052.59 499.57,-1051.8 501.06,-1051.04 502.72,-1050.31 504.56,-1049.61 506.57,-1048.94 508.74,-1048.31 511.06,-1047.71 513.53,-1047.16 516.15,-1046.65 518.89,-1046.18 521.76,-1045.75 524.73,-1045.36 527.81,-1045.03 530.97,-1044.74 534.21,-1044.49 537.51,-1044.3 540.86,-1044.15 544.25,-1044.05 547.65,-1044 551.07,-1044 554.47,-1044.05\"/>\n<text text-anchor=\"middle\" x=\"549.36\" y=\"-1058.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(and5)]</text>\n</g>\n<!-- [neg(and5)]&#45;&gt;[neg(and4),neg(or4)] -->\n<g id=\"edge7\" class=\"edge\">\n<title>[neg(and5)]&#45;&gt;[neg(and4),neg(or4)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M549.36,-1043.8C549.36,-1032.58 549.36,-1017.67 549.36,-1004.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"552.86,-1004.98 549.36,-994.98 545.86,-1004.98 552.86,-1004.98\"/>\n<text text-anchor=\"middle\" x=\"562.86\" y=\"-1014.8\" font-family=\"Times,serif\" font-size=\"14.00\">and5</text>\n</g>\n<!-- [neg(d)] -->\n<g id=\"node12\" class=\"node\">\n<title>[neg(d)]</title>\n<ellipse fill=\"none\" stroke=\"red\" cx=\"601.36\" cy=\"-18\" rx=\"39.79\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"601.36\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(d)]</text>\n</g>\n<!-- [neg(c),neg(d)]&#45;&gt;[neg(d)] -->\n<g id=\"edge8\" class=\"edge\">\n<title>[neg(c),neg(d)]&#45;&gt;[neg(d)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M601.36,-86.8C601.36,-75.58 601.36,-60.67 601.36,-47.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"604.86,-47.98 601.36,-37.98 597.86,-47.98 604.86,-47.98\"/>\n<text text-anchor=\"middle\" x=\"604.86\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">c</text>\n</g>\n<!-- [neg(d),neg(not2),neg(or4)] -->\n<g id=\"node13\" class=\"node\">\n<title>[neg(d),neg(not2),neg(or4)]</title>\n<ellipse fill=\"none\" stroke=\"red\" cx=\"681.36\" cy=\"-540\" rx=\"108.58\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"681.36\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(d),neg(not2),neg(or4)]</text>\n</g>\n<!-- [neg(c),neg(d),neg(not2),neg(or4)]&#45;&gt;[neg(d),neg(not2),neg(or4)] -->\n<g id=\"edge9\" class=\"edge\">\n<title>[neg(c),neg(d),neg(not2),neg(or4)]&#45;&gt;[neg(d),neg(not2),neg(or4)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M681.36,-608.8C681.36,-597.58 681.36,-582.67 681.36,-569.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"684.86,-569.98 681.36,-559.98 677.86,-569.98 684.86,-569.98\"/>\n<text text-anchor=\"middle\" x=\"684.86\" y=\"-579.8\" font-family=\"Times,serif\" font-size=\"14.00\">c</text>\n</g>\n<!-- [neg(e)] -->\n<g id=\"node14\" class=\"node\">\n<title>[neg(e)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"489.2,-174.05 491.75,-174.15 494.27,-174.3 496.75,-174.49 499.19,-174.74 501.57,-175.03 503.88,-175.36 506.12,-175.75 508.28,-176.18 510.34,-176.65 512.31,-177.16 514.17,-177.71 515.92,-178.31 517.55,-178.94 519.06,-179.61 520.44,-180.31 521.69,-181.04 522.81,-181.8 523.8,-182.59 524.65,-183.41 525.36,-184.25 525.94,-185.11 526.38,-185.99 526.69,-186.89 526.87,-187.8 526.92,-188.72 526.84,-189.65 526.64,-190.59 526.32,-191.53 525.88,-192.47 525.34,-193.41 524.69,-194.35 523.95,-195.28 523.11,-196.2 522.18,-197.11 521.17,-198.01 520.08,-198.89 518.93,-199.75 517.7,-200.59 516.42,-201.41 515.08,-202.2 513.69,-202.96 512.26,-203.69 510.79,-204.39 509.28,-205.06 507.74,-205.69 506.17,-206.29 504.58,-206.84 502.96,-207.35 501.33,-207.82 499.69,-208.25 498.03,-208.64 496.36,-208.97 494.68,-209.26 492.99,-209.51 491.3,-209.7 489.61,-209.85 487.91,-209.95 486.21,-210 484.51,-210 482.81,-209.95 481.11,-209.85 479.42,-209.7 477.73,-209.51 476.04,-209.26 474.36,-208.97 472.69,-208.64 471.03,-208.25 469.39,-207.82 467.75,-207.35 466.14,-206.84 464.55,-206.29 462.98,-205.69 461.44,-205.06 459.93,-204.39 458.46,-203.69 457.03,-202.96 455.64,-202.2 454.3,-201.41 453.02,-200.59 451.79,-199.75 450.63,-198.89 449.55,-198.01 448.54,-197.11 447.61,-196.2 446.77,-195.28 446.02,-194.35 445.38,-193.41 444.83,-192.47 444.4,-191.53 444.08,-190.59 443.88,-189.65 443.8,-188.72 443.85,-187.8 444.03,-186.89 444.33,-185.99 444.78,-185.11 445.35,-184.25 446.07,-183.41 446.92,-182.59 447.9,-181.8 449.02,-181.04 450.28,-180.31 451.66,-179.61 453.17,-178.94 454.8,-178.31 456.55,-177.71 458.41,-177.16 460.37,-176.65 462.44,-176.18 464.59,-175.75 466.83,-175.36 469.15,-175.03 471.53,-174.74 473.96,-174.49 476.45,-174.3 478.97,-174.15 481.51,-174.05 484.08,-174 486.64,-174 489.2,-174.05\"/>\n<text text-anchor=\"middle\" x=\"485.36\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(e)]</text>\n</g>\n<!-- [neg(e)]&#45;&gt;[] -->\n<g id=\"edge10\" class=\"edge\">\n<title>[neg(e)]&#45;&gt;[]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M485.36,-173.8C485.36,-162.58 485.36,-147.67 485.36,-134.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"488.86,-134.98 485.36,-124.98 481.86,-134.98 488.86,-134.98\"/>\n<text text-anchor=\"middle\" x=\"488.86\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">e</text>\n</g>\n<!-- [neg(e),neg(not2),neg(or4)] -->\n<g id=\"node15\" class=\"node\">\n<title>[neg(e),neg(not2),neg(or4)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"423.06,-696.05 430.15,-696.15 437.16,-696.3 444.08,-696.49 450.86,-696.74 457.48,-697.03 463.93,-697.36 470.16,-697.75 476.16,-698.18 481.91,-698.65 487.38,-699.16 492.56,-699.71 497.42,-700.31 501.96,-700.94 506.16,-701.61 510.01,-702.31 513.5,-703.04 516.62,-703.8 519.36,-704.59 521.73,-705.41 523.71,-706.25 525.32,-707.11 526.55,-707.99 527.41,-708.89 527.9,-709.8 528.04,-710.72 527.82,-711.65 527.26,-712.59 526.37,-713.53 525.16,-714.47 523.65,-715.41 521.85,-716.35 519.77,-717.28 517.44,-718.2 514.85,-719.11 512.04,-720.01 509.02,-720.89 505.79,-721.75 502.39,-722.59 498.81,-723.41 495.09,-724.2 491.23,-724.96 487.24,-725.69 483.14,-726.39 478.94,-727.06 474.65,-727.69 470.28,-728.29 465.85,-728.84 461.36,-729.35 456.82,-729.82 452.24,-730.25 447.62,-730.64 442.97,-730.97 438.3,-731.26 433.61,-731.51 428.9,-731.7 424.18,-731.85 419.46,-731.95 414.73,-732 409.99,-732 405.26,-731.95 400.54,-731.85 395.82,-731.7 391.11,-731.51 386.42,-731.26 381.75,-730.97 377.1,-730.64 372.48,-730.25 367.9,-729.82 363.36,-729.35 358.87,-728.84 354.43,-728.29 350.07,-727.69 345.78,-727.06 341.58,-726.39 337.48,-725.69 333.49,-724.96 329.63,-724.2 325.9,-723.41 322.33,-722.59 318.93,-721.75 315.7,-720.89 312.68,-720.01 309.86,-719.11 307.28,-718.2 304.95,-717.28 302.87,-716.35 301.07,-715.41 299.56,-714.47 298.35,-713.53 297.46,-712.59 296.9,-711.65 296.68,-710.72 296.81,-709.8 297.31,-708.89 298.17,-707.99 299.4,-707.11 301.01,-706.25 302.99,-705.41 305.36,-704.59 308.1,-703.8 311.22,-703.04 314.71,-702.31 318.56,-701.61 322.76,-700.94 327.3,-700.31 332.16,-699.71 337.34,-699.16 342.81,-698.65 348.56,-698.18 354.56,-697.75 360.79,-697.36 367.23,-697.03 373.86,-696.74 380.64,-696.49 387.55,-696.3 394.57,-696.15 401.65,-696.05 408.79,-696 415.93,-696 423.06,-696.05\"/>\n<text text-anchor=\"middle\" x=\"412.36\" y=\"-710.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(e),neg(not2),neg(or4)]</text>\n</g>\n<!-- [neg(not2),neg(or4)] -->\n<g id=\"node22\" class=\"node\">\n<title>[neg(not2),neg(or4)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"420.57,-609.05 426,-609.15 431.38,-609.3 436.68,-609.49 441.88,-609.74 446.96,-610.03 451.89,-610.36 456.67,-610.75 461.28,-611.18 465.68,-611.65 469.88,-612.16 473.85,-612.71 477.58,-613.31 481.06,-613.94 484.28,-614.61 487.23,-615.31 489.9,-616.04 492.29,-616.8 494.4,-617.59 496.21,-618.41 497.73,-619.25 498.97,-620.11 499.91,-620.99 500.57,-621.89 500.95,-622.8 501.05,-623.72 500.88,-624.65 500.45,-625.59 499.77,-626.53 498.85,-627.47 497.69,-628.41 496.31,-629.35 494.71,-630.28 492.92,-631.2 490.94,-632.11 488.79,-633.01 486.47,-633.89 484,-634.75 481.38,-635.59 478.64,-636.41 475.79,-637.2 472.83,-637.96 469.77,-638.69 466.62,-639.39 463.4,-640.06 460.12,-640.69 456.77,-641.29 453.37,-641.84 449.93,-642.35 446.45,-642.82 442.94,-643.25 439.39,-643.64 435.83,-643.97 432.25,-644.26 428.65,-644.51 425.04,-644.7 421.42,-644.85 417.8,-644.95 414.17,-645 410.55,-645 406.92,-644.95 403.29,-644.85 399.68,-644.7 396.07,-644.51 392.47,-644.26 388.89,-643.97 385.32,-643.64 381.78,-643.25 378.27,-642.82 374.79,-642.35 371.35,-641.84 367.95,-641.29 364.6,-640.69 361.31,-640.06 358.09,-639.39 354.95,-638.69 351.89,-637.96 348.93,-637.2 346.07,-636.41 343.33,-635.59 340.72,-634.75 338.25,-633.89 335.93,-633.01 333.78,-632.11 331.8,-631.2 330,-630.28 328.41,-629.35 327.03,-628.41 325.87,-627.47 324.95,-626.53 324.27,-625.59 323.84,-624.65 323.67,-623.72 323.77,-622.8 324.15,-621.89 324.81,-620.99 325.75,-620.11 326.98,-619.25 328.51,-618.41 330.32,-617.59 332.43,-616.8 334.82,-616.04 337.49,-615.31 340.44,-614.61 343.66,-613.94 347.14,-613.31 350.87,-612.71 354.84,-612.16 359.04,-611.65 363.44,-611.18 368.04,-610.75 372.82,-610.36 377.76,-610.03 382.84,-609.74 388.04,-609.49 393.34,-609.3 398.72,-609.15 404.15,-609.05 409.62,-609 415.1,-609 420.57,-609.05\"/>\n<text text-anchor=\"middle\" x=\"412.36\" y=\"-623.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(not2),neg(or4)]</text>\n</g>\n<!-- [neg(e),neg(not2),neg(or4)]&#45;&gt;[neg(not2),neg(or4)] -->\n<g id=\"edge11\" class=\"edge\">\n<title>[neg(e),neg(not2),neg(or4)]&#45;&gt;[neg(not2),neg(or4)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M412.36,-695.8C412.36,-684.58 412.36,-669.67 412.36,-656.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"415.86,-656.98 412.36,-646.98 408.86,-656.98 415.86,-656.98\"/>\n<text text-anchor=\"middle\" x=\"415.86\" y=\"-666.8\" font-family=\"Times,serif\" font-size=\"14.00\">e</text>\n</g>\n<!-- [neg(e),neg(or4)] -->\n<g id=\"node16\" class=\"node\">\n<title>[neg(e),neg(or4)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"419.42,-522.05 424.09,-522.15 428.71,-522.3 433.27,-522.49 437.74,-522.74 442.11,-523.03 446.36,-523.36 450.47,-523.75 454.43,-524.18 458.22,-524.65 461.82,-525.16 465.24,-525.71 468.45,-526.31 471.44,-526.94 474.21,-527.61 476.75,-528.31 479.05,-529.04 481.1,-529.8 482.91,-530.59 484.47,-531.41 485.78,-532.25 486.84,-533.11 487.65,-533.99 488.22,-534.89 488.54,-535.8 488.63,-536.72 488.49,-537.65 488.12,-538.59 487.53,-539.53 486.74,-540.47 485.74,-541.41 484.55,-542.35 483.18,-543.28 481.64,-544.2 479.94,-545.11 478.09,-546.01 476.09,-546.89 473.97,-547.75 471.72,-548.59 469.36,-549.41 466.91,-550.2 464.36,-550.96 461.73,-551.69 459.03,-552.39 456.26,-553.06 453.43,-553.69 450.55,-554.29 447.63,-554.84 444.67,-555.35 441.68,-555.82 438.65,-556.25 435.61,-556.64 432.54,-556.97 429.46,-557.26 426.37,-557.51 423.27,-557.7 420.16,-557.85 417.04,-557.95 413.92,-558 410.8,-558 407.68,-557.95 404.56,-557.85 401.45,-557.7 398.35,-557.51 395.25,-557.26 392.17,-556.97 389.11,-556.64 386.06,-556.25 383.04,-555.82 380.05,-555.35 377.09,-554.84 374.17,-554.29 371.29,-553.69 368.46,-553.06 365.69,-552.39 362.99,-551.69 360.36,-550.96 357.81,-550.2 355.35,-549.41 353,-548.59 350.75,-547.75 348.63,-546.89 346.63,-546.01 344.78,-545.11 343.08,-544.2 341.54,-543.28 340.17,-542.35 338.98,-541.41 337.98,-540.47 337.19,-539.53 336.6,-538.59 336.23,-537.65 336.09,-536.72 336.17,-535.8 336.5,-534.89 337.06,-533.99 337.88,-533.11 338.94,-532.25 340.25,-531.41 341.81,-530.59 343.62,-529.8 345.67,-529.04 347.97,-528.31 350.51,-527.61 353.28,-526.94 356.27,-526.31 359.48,-525.71 362.89,-525.16 366.5,-524.65 370.29,-524.18 374.25,-523.75 378.36,-523.36 382.61,-523.03 386.97,-522.74 391.45,-522.49 396,-522.3 400.63,-522.15 405.3,-522.05 410,-522 414.72,-522 419.42,-522.05\"/>\n<text text-anchor=\"middle\" x=\"412.36\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(e),neg(or4)]</text>\n</g>\n<!-- [neg(or4)] -->\n<g id=\"node31\" class=\"node\">\n<title>[neg(or4)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"416.96,-435.05 420,-435.15 423.01,-435.3 425.98,-435.49 428.89,-435.74 431.73,-436.03 434.5,-436.36 437.18,-436.75 439.75,-437.18 442.22,-437.65 444.57,-438.16 446.79,-438.71 448.88,-439.31 450.83,-439.94 452.64,-440.61 454.29,-441.31 455.79,-442.04 457.13,-442.8 458.3,-443.59 459.32,-444.41 460.17,-445.25 460.86,-446.11 461.39,-446.99 461.76,-447.89 461.97,-448.8 462.03,-449.72 461.94,-450.65 461.69,-451.59 461.31,-452.53 460.79,-453.47 460.15,-454.41 459.37,-455.35 458.48,-456.28 457.48,-457.2 456.37,-458.11 455.16,-459.01 453.86,-459.89 452.48,-460.75 451.02,-461.59 449.48,-462.41 447.88,-463.2 446.22,-463.96 444.51,-464.69 442.75,-465.39 440.95,-466.06 439.11,-466.69 437.23,-467.29 435.33,-467.84 433.4,-468.35 431.45,-468.82 429.48,-469.25 427.5,-469.64 425.5,-469.97 423.5,-470.26 421.48,-470.51 419.46,-470.7 417.44,-470.85 415.41,-470.95 413.38,-471 411.34,-471 409.31,-470.95 407.28,-470.85 405.26,-470.7 403.24,-470.51 401.22,-470.26 399.21,-469.97 397.22,-469.64 395.24,-469.25 393.27,-468.82 391.32,-468.35 389.39,-467.84 387.49,-467.29 385.61,-466.69 383.77,-466.06 381.97,-465.39 380.21,-464.69 378.5,-463.96 376.84,-463.2 375.24,-462.41 373.7,-461.59 372.24,-460.75 370.86,-459.89 369.56,-459.01 368.35,-458.11 367.24,-457.2 366.24,-456.28 365.35,-455.35 364.57,-454.41 363.92,-453.47 363.41,-452.53 363.02,-451.59 362.78,-450.65 362.69,-449.72 362.75,-448.8 362.96,-447.89 363.33,-446.99 363.86,-446.11 364.55,-445.25 365.4,-444.41 366.42,-443.59 367.59,-442.8 368.93,-442.04 370.43,-441.31 372.08,-440.61 373.88,-439.94 375.83,-439.31 377.92,-438.71 380.15,-438.16 382.5,-437.65 384.96,-437.18 387.54,-436.75 390.22,-436.36 392.98,-436.03 395.83,-435.74 398.74,-435.49 401.71,-435.3 404.72,-435.15 407.76,-435.05 410.83,-435 413.89,-435 416.96,-435.05\"/>\n<text text-anchor=\"middle\" x=\"412.36\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(or4)]</text>\n</g>\n<!-- [neg(e),neg(or4)]&#45;&gt;[neg(or4)] -->\n<g id=\"edge12\" class=\"edge\">\n<title>[neg(e),neg(or4)]&#45;&gt;[neg(or4)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M412.36,-521.8C412.36,-510.58 412.36,-495.67 412.36,-482.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"415.86,-482.98 412.36,-472.98 408.86,-482.98 415.86,-482.98\"/>\n<text text-anchor=\"middle\" x=\"415.86\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">e</text>\n</g>\n<!-- [neg(not1)] -->\n<g id=\"node17\" class=\"node\">\n<title>[neg(not1)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"746.35,-174.05 749.66,-174.15 752.93,-174.3 756.16,-174.49 759.32,-174.74 762.41,-175.03 765.42,-175.36 768.33,-175.75 771.13,-176.18 773.81,-176.65 776.36,-177.16 778.78,-177.71 781.05,-178.31 783.17,-178.94 785.13,-179.61 786.92,-180.31 788.55,-181.04 790.01,-181.8 791.29,-182.59 792.39,-183.41 793.32,-184.25 794.07,-185.11 794.64,-185.99 795.04,-186.89 795.27,-187.8 795.33,-188.72 795.23,-189.65 794.97,-190.59 794.56,-191.53 793.99,-192.47 793.29,-193.41 792.45,-194.35 791.48,-195.28 790.39,-196.2 789.18,-197.11 787.87,-198.01 786.46,-198.89 784.96,-199.75 783.37,-200.59 781.7,-201.41 779.96,-202.2 778.16,-202.96 776.3,-203.69 774.38,-204.39 772.42,-205.06 770.42,-205.69 768.39,-206.29 766.32,-206.84 764.22,-207.35 762.11,-207.82 759.97,-208.25 757.81,-208.64 755.64,-208.97 753.46,-209.26 751.27,-209.51 749.08,-209.7 746.88,-209.85 744.67,-209.95 742.46,-210 740.26,-210 738.05,-209.95 735.84,-209.85 733.64,-209.7 731.44,-209.51 729.26,-209.26 727.08,-208.97 724.91,-208.64 722.75,-208.25 720.61,-207.82 718.49,-207.35 716.4,-206.84 714.33,-206.29 712.3,-205.69 710.29,-205.06 708.33,-204.39 706.42,-203.69 704.56,-202.96 702.76,-202.2 701.02,-201.41 699.35,-200.59 697.76,-199.75 696.26,-198.89 694.85,-198.01 693.54,-197.11 692.33,-196.2 691.24,-195.28 690.27,-194.35 689.43,-193.41 688.73,-192.47 688.16,-191.53 687.75,-190.59 687.49,-189.65 687.38,-188.72 687.45,-187.8 687.68,-186.89 688.08,-185.99 688.65,-185.11 689.4,-184.25 690.33,-183.41 691.43,-182.59 692.71,-181.8 694.17,-181.04 695.8,-180.31 697.59,-179.61 699.55,-178.94 701.67,-178.31 703.94,-177.71 706.36,-177.16 708.91,-176.65 711.59,-176.18 714.39,-175.75 717.3,-175.36 720.3,-175.03 723.4,-174.74 726.56,-174.49 729.79,-174.3 733.06,-174.15 736.36,-174.05 739.69,-174 743.03,-174 746.35,-174.05\"/>\n<text text-anchor=\"middle\" x=\"741.36\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(not1)]</text>\n</g>\n<!-- [neg(not_e)] -->\n<g id=\"node23\" class=\"node\">\n<title>[neg(not_e)]</title>\n<ellipse fill=\"none\" stroke=\"red\" cx=\"742.36\" cy=\"-105\" rx=\"54.69\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"742.36\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(not_e)]</text>\n</g>\n<!-- [neg(not1)]&#45;&gt;[neg(not_e)] -->\n<g id=\"edge13\" class=\"edge\">\n<title>[neg(not1)]&#45;&gt;[neg(not_e)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M741.56,-173.8C741.69,-162.58 741.87,-147.67 742.02,-134.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"745.52,-135.02 742.14,-124.98 738.52,-134.94 745.52,-135.02\"/>\n<text text-anchor=\"middle\" x=\"753.86\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">not1</text>\n</g>\n<!-- [neg(not1),neg(and2)] -->\n<g id=\"node18\" class=\"node\">\n<title>[neg(not1),neg(and2)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"337.12,-174.05 342.92,-174.15 348.66,-174.3 354.31,-174.49 359.86,-174.74 365.28,-175.03 370.55,-175.36 375.65,-175.75 380.56,-176.18 385.26,-176.65 389.74,-177.16 393.98,-177.71 397.96,-178.31 401.67,-178.94 405.11,-179.61 408.26,-180.31 411.11,-181.04 413.66,-181.8 415.91,-182.59 417.84,-183.41 419.47,-184.25 420.79,-185.11 421.79,-185.99 422.5,-186.89 422.9,-187.8 423.01,-188.72 422.83,-189.65 422.37,-190.59 421.64,-191.53 420.66,-192.47 419.42,-193.41 417.95,-194.35 416.25,-195.28 414.33,-196.2 412.22,-197.11 409.92,-198.01 407.45,-198.89 404.81,-199.75 402.02,-200.59 399.1,-201.41 396.05,-202.2 392.89,-202.96 389.62,-203.69 386.27,-204.39 382.83,-205.06 379.33,-205.69 375.75,-206.29 372.13,-206.84 368.45,-207.35 364.74,-207.82 360.99,-208.25 357.21,-208.64 353.41,-208.97 349.58,-209.26 345.75,-209.51 341.89,-209.7 338.03,-209.85 334.17,-209.95 330.3,-210 326.42,-210 322.55,-209.95 318.69,-209.85 314.82,-209.7 310.97,-209.51 307.13,-209.26 303.31,-208.97 299.51,-208.64 295.73,-208.25 291.98,-207.82 288.26,-207.35 284.59,-206.84 280.96,-206.29 277.39,-205.69 273.88,-205.06 270.45,-204.39 267.09,-203.69 263.83,-202.96 260.67,-202.2 257.62,-201.41 254.7,-200.59 251.91,-199.75 249.27,-198.89 246.8,-198.01 244.5,-197.11 242.38,-196.2 240.47,-195.28 238.77,-194.35 237.3,-193.41 236.06,-192.47 235.07,-191.53 234.35,-190.59 233.89,-189.65 233.71,-188.72 233.82,-187.8 234.22,-186.89 234.92,-185.99 235.93,-185.11 237.25,-184.25 238.87,-183.41 240.81,-182.59 243.06,-181.8 245.61,-181.04 248.46,-180.31 251.61,-179.61 255.04,-178.94 258.76,-178.31 262.74,-177.71 266.98,-177.16 271.45,-176.65 276.16,-176.18 281.07,-175.75 286.17,-175.36 291.44,-175.03 296.86,-174.74 302.41,-174.49 308.06,-174.3 313.8,-174.15 319.6,-174.05 325.44,-174 331.28,-174 337.12,-174.05\"/>\n<text text-anchor=\"middle\" x=\"328.36\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(not1),neg(and2)]</text>\n</g>\n<!-- [neg(not_e),neg(and2)] -->\n<g id=\"node24\" class=\"node\">\n<title>[neg(not_e),neg(and2)]</title>\n<ellipse fill=\"none\" stroke=\"red\" cx=\"329.36\" cy=\"-105\" rx=\"92.88\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"329.36\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(not_e),neg(and2)]</text>\n</g>\n<!-- [neg(not1),neg(and2)]&#45;&gt;[neg(not_e),neg(and2)] -->\n<g id=\"edge14\" class=\"edge\">\n<title>[neg(not1),neg(and2)]&#45;&gt;[neg(not_e),neg(and2)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M328.56,-173.8C328.69,-162.58 328.87,-147.67 329.02,-134.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"332.52,-135.02 329.14,-124.98 325.52,-134.94 332.52,-135.02\"/>\n<text text-anchor=\"middle\" x=\"341.86\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">not1</text>\n</g>\n<!-- [neg(not1),neg(not2),neg(or4)] -->\n<g id=\"node19\" class=\"node\">\n<title>[neg(not1),neg(not2),neg(or4)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"977.21,-696.05 985.06,-696.15 992.83,-696.3 1000.48,-696.49 1007.99,-696.74 1015.33,-697.03 1022.46,-697.36 1029.36,-697.75 1036.01,-698.18 1042.37,-698.65 1048.43,-699.16 1054.17,-699.71 1059.55,-700.31 1064.58,-700.94 1069.23,-701.61 1073.49,-702.31 1077.35,-703.04 1080.81,-703.8 1083.85,-704.59 1086.47,-705.41 1088.67,-706.25 1090.45,-707.11 1091.81,-707.99 1092.76,-708.89 1093.31,-709.8 1093.45,-710.72 1093.21,-711.65 1092.59,-712.59 1091.61,-713.53 1090.27,-714.47 1088.6,-715.41 1086.6,-716.35 1084.3,-717.28 1081.72,-718.2 1078.86,-719.11 1075.74,-720.01 1072.39,-720.89 1068.82,-721.75 1065.05,-722.59 1061.1,-723.41 1056.97,-724.2 1052.69,-724.96 1048.27,-725.69 1043.73,-726.39 1039.08,-727.06 1034.34,-727.69 1029.5,-728.29 1024.59,-728.84 1019.62,-729.35 1014.59,-729.82 1009.52,-730.25 1004.41,-730.64 999.26,-730.97 994.08,-731.26 988.89,-731.51 983.68,-731.7 978.45,-731.85 973.22,-731.95 967.98,-732 962.74,-732 957.5,-731.95 952.27,-731.85 947.04,-731.7 941.83,-731.51 936.63,-731.26 931.46,-730.97 926.31,-730.64 921.2,-730.25 916.12,-729.82 911.1,-729.35 906.12,-728.84 901.22,-728.29 896.38,-727.69 891.64,-727.06 886.98,-726.39 882.44,-725.69 878.03,-724.96 873.75,-724.2 869.62,-723.41 865.67,-722.59 861.9,-721.75 858.33,-720.89 854.98,-720.01 851.86,-719.11 849,-718.2 846.42,-717.28 844.12,-716.35 842.12,-715.41 840.45,-714.47 839.11,-713.53 838.13,-712.59 837.51,-711.65 837.26,-710.72 837.41,-709.8 837.96,-708.89 838.91,-707.99 840.27,-707.11 842.05,-706.25 844.25,-705.41 846.87,-704.59 849.91,-703.8 853.36,-703.04 857.23,-702.31 861.49,-701.61 866.14,-700.94 871.16,-700.31 876.55,-699.71 882.29,-699.16 888.35,-698.65 894.71,-698.18 901.36,-697.75 908.26,-697.36 915.39,-697.03 922.73,-696.74 930.24,-696.49 937.89,-696.3 945.66,-696.15 953.51,-696.05 961.4,-696 969.32,-696 977.21,-696.05\"/>\n<text text-anchor=\"middle\" x=\"965.36\" y=\"-710.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(not1),neg(not2),neg(or4)]</text>\n</g>\n<!-- [neg(not_e),neg(not2),neg(or4)] -->\n<g id=\"node25\" class=\"node\">\n<title>[neg(not_e),neg(not2),neg(or4)]</title>\n<ellipse fill=\"none\" stroke=\"red\" cx=\"966.36\" cy=\"-627\" rx=\"124.28\" ry=\"18\"/>\n<text text-anchor=\"middle\" x=\"966.36\" y=\"-623.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(not_e),neg(not2),neg(or4)]</text>\n</g>\n<!-- [neg(not1),neg(not2),neg(or4)]&#45;&gt;[neg(not_e),neg(not2),neg(or4)] -->\n<g id=\"edge15\" class=\"edge\">\n<title>[neg(not1),neg(not2),neg(or4)]&#45;&gt;[neg(not_e),neg(not2),neg(or4)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M965.56,-695.8C965.69,-684.58 965.87,-669.67 966.02,-656.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"969.52,-657.02 966.14,-646.98 962.52,-656.94 969.52,-657.02\"/>\n<text text-anchor=\"middle\" x=\"977.86\" y=\"-666.8\" font-family=\"Times,serif\" font-size=\"14.00\">not1</text>\n</g>\n<!-- [neg(not2)] -->\n<g id=\"node20\" class=\"node\">\n<title>[neg(not2)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"490.35,-261.05 493.66,-261.15 496.93,-261.3 500.16,-261.49 503.32,-261.74 506.41,-262.03 509.42,-262.36 512.33,-262.75 515.13,-263.18 517.81,-263.65 520.36,-264.16 522.78,-264.71 525.05,-265.31 527.17,-265.94 529.13,-266.61 530.92,-267.31 532.55,-268.04 534.01,-268.8 535.29,-269.59 536.39,-270.41 537.32,-271.25 538.07,-272.11 538.64,-272.99 539.04,-273.89 539.27,-274.8 539.33,-275.72 539.23,-276.65 538.97,-277.59 538.56,-278.53 537.99,-279.47 537.29,-280.41 536.45,-281.35 535.48,-282.28 534.39,-283.2 533.18,-284.11 531.87,-285.01 530.46,-285.89 528.96,-286.75 527.37,-287.59 525.7,-288.41 523.96,-289.2 522.16,-289.96 520.3,-290.69 518.38,-291.39 516.42,-292.06 514.42,-292.69 512.39,-293.29 510.32,-293.84 508.22,-294.35 506.11,-294.82 503.97,-295.25 501.81,-295.64 499.64,-295.97 497.46,-296.26 495.27,-296.51 493.08,-296.7 490.88,-296.85 488.67,-296.95 486.46,-297 484.26,-297 482.05,-296.95 479.84,-296.85 477.64,-296.7 475.44,-296.51 473.26,-296.26 471.08,-295.97 468.91,-295.64 466.75,-295.25 464.61,-294.82 462.49,-294.35 460.4,-293.84 458.33,-293.29 456.3,-292.69 454.29,-292.06 452.33,-291.39 450.42,-290.69 448.56,-289.96 446.76,-289.2 445.02,-288.41 443.35,-287.59 441.76,-286.75 440.26,-285.89 438.85,-285.01 437.54,-284.11 436.33,-283.2 435.24,-282.28 434.27,-281.35 433.43,-280.41 432.73,-279.47 432.16,-278.53 431.75,-277.59 431.49,-276.65 431.38,-275.72 431.45,-274.8 431.68,-273.89 432.08,-272.99 432.65,-272.11 433.4,-271.25 434.33,-270.41 435.43,-269.59 436.71,-268.8 438.17,-268.04 439.8,-267.31 441.59,-266.61 443.55,-265.94 445.67,-265.31 447.94,-264.71 450.36,-264.16 452.91,-263.65 455.59,-263.18 458.39,-262.75 461.3,-262.36 464.3,-262.03 467.4,-261.74 470.56,-261.49 473.79,-261.3 477.06,-261.15 480.36,-261.05 483.69,-261 487.03,-261 490.35,-261.05\"/>\n<text text-anchor=\"middle\" x=\"485.36\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(not2)]</text>\n</g>\n<!-- [neg(not2)]&#45;&gt;[neg(e)] -->\n<g id=\"edge16\" class=\"edge\">\n<title>[neg(not2)]&#45;&gt;[neg(e)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M485.36,-260.8C485.36,-249.58 485.36,-234.67 485.36,-221.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"488.86,-221.98 485.36,-211.98 481.86,-221.98 488.86,-221.98\"/>\n<text text-anchor=\"middle\" x=\"497.86\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">not2</text>\n</g>\n<!-- [neg(not2),neg(not2),neg(or4)] -->\n<g id=\"node21\" class=\"node\">\n<title>[neg(not2),neg(not2),neg(or4)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"424.21,-783.05 432.06,-783.15 439.83,-783.3 447.48,-783.49 454.99,-783.74 462.33,-784.03 469.46,-784.36 476.36,-784.75 483.01,-785.18 489.37,-785.65 495.43,-786.16 501.17,-786.71 506.55,-787.31 511.58,-787.94 516.23,-788.61 520.49,-789.31 524.35,-790.04 527.81,-790.8 530.85,-791.59 533.47,-792.41 535.67,-793.25 537.45,-794.11 538.81,-794.99 539.76,-795.89 540.31,-796.8 540.45,-797.72 540.21,-798.65 539.59,-799.59 538.61,-800.53 537.27,-801.47 535.6,-802.41 533.6,-803.35 531.3,-804.28 528.72,-805.2 525.86,-806.11 522.74,-807.01 519.39,-807.89 515.82,-808.75 512.05,-809.59 508.1,-810.41 503.97,-811.2 499.69,-811.96 495.27,-812.69 490.73,-813.39 486.08,-814.06 481.34,-814.69 476.5,-815.29 471.59,-815.84 466.62,-816.35 461.59,-816.82 456.52,-817.25 451.41,-817.64 446.26,-817.97 441.08,-818.26 435.89,-818.51 430.68,-818.7 425.45,-818.85 420.22,-818.95 414.98,-819 409.74,-819 404.5,-818.95 399.27,-818.85 394.04,-818.7 388.83,-818.51 383.63,-818.26 378.46,-817.97 373.31,-817.64 368.2,-817.25 363.12,-816.82 358.1,-816.35 353.12,-815.84 348.22,-815.29 343.38,-814.69 338.64,-814.06 333.98,-813.39 329.44,-812.69 325.03,-811.96 320.75,-811.2 316.62,-810.41 312.67,-809.59 308.9,-808.75 305.33,-807.89 301.98,-807.01 298.86,-806.11 296,-805.2 293.42,-804.28 291.12,-803.35 289.12,-802.41 287.45,-801.47 286.11,-800.53 285.13,-799.59 284.51,-798.65 284.26,-797.72 284.41,-796.8 284.96,-795.89 285.91,-794.99 287.27,-794.11 289.05,-793.25 291.25,-792.41 293.87,-791.59 296.91,-790.8 300.36,-790.04 304.23,-789.31 308.49,-788.61 313.14,-787.94 318.16,-787.31 323.55,-786.71 329.29,-786.16 335.35,-785.65 341.71,-785.18 348.36,-784.75 355.26,-784.36 362.39,-784.03 369.73,-783.74 377.24,-783.49 384.89,-783.3 392.66,-783.15 400.51,-783.05 408.4,-783 416.32,-783 424.21,-783.05\"/>\n<text text-anchor=\"middle\" x=\"412.36\" y=\"-797.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(not2),neg(not2),neg(or4)]</text>\n</g>\n<!-- [neg(not2),neg(not2),neg(or4)]&#45;&gt;[neg(e),neg(not2),neg(or4)] -->\n<g id=\"edge17\" class=\"edge\">\n<title>[neg(not2),neg(not2),neg(or4)]&#45;&gt;[neg(e),neg(not2),neg(or4)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M412.36,-782.8C412.36,-771.58 412.36,-756.67 412.36,-743.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"415.86,-743.98 412.36,-733.98 408.86,-743.98 415.86,-743.98\"/>\n<text text-anchor=\"middle\" x=\"424.86\" y=\"-753.8\" font-family=\"Times,serif\" font-size=\"14.00\">not2</text>\n</g>\n<!-- [neg(not2),neg(or4)]&#45;&gt;[neg(e),neg(or4)] -->\n<g id=\"edge18\" class=\"edge\">\n<title>[neg(not2),neg(or4)]&#45;&gt;[neg(e),neg(or4)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M412.36,-608.8C412.36,-597.58 412.36,-582.67 412.36,-569.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"415.86,-569.98 412.36,-559.98 408.86,-569.98 415.86,-569.98\"/>\n<text text-anchor=\"middle\" x=\"424.86\" y=\"-579.8\" font-family=\"Times,serif\" font-size=\"14.00\">not2</text>\n</g>\n<!-- [neg(or21),neg(and2)]&#45;&gt;[neg(and11),neg(and2)] -->\n<g id=\"edge19\" class=\"edge\">\n<title>[neg(or21),neg(and2)]&#45;&gt;[neg(and11),neg(and2)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M279.32,-261.81C245.59,-247.83 196.75,-227.58 160.78,-212.66\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"162.5,-209.59 151.93,-208.99 159.82,-216.05 162.5,-209.59\"/>\n<text text-anchor=\"middle\" x=\"240.86\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">or21</text>\n</g>\n<!-- [neg(or21),neg(and2)]&#45;&gt;[neg(not1),neg(and2)] -->\n<g id=\"edge20\" class=\"edge\">\n<title>[neg(or21),neg(and2)]&#45;&gt;[neg(not1),neg(and2)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M320.38,-260.8C321.7,-249.58 323.46,-234.67 324.98,-221.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"328.44,-222.31 326.13,-211.97 321.48,-221.49 328.44,-222.31\"/>\n<text text-anchor=\"middle\" x=\"336.86\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">or21</text>\n</g>\n<!-- [neg(or22)] -->\n<g id=\"node27\" class=\"node\">\n<title>[neg(or22)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"617.44,-261.05 620.8,-261.15 624.12,-261.3 627.4,-261.49 630.62,-261.74 633.76,-262.03 636.81,-262.36 639.77,-262.75 642.62,-263.18 645.34,-263.65 647.94,-264.16 650.39,-264.71 652.7,-265.31 654.85,-265.94 656.85,-266.61 658.67,-267.31 660.32,-268.04 661.8,-268.8 663.1,-269.59 664.23,-270.41 665.17,-271.25 665.93,-272.11 666.52,-272.99 666.92,-273.89 667.16,-274.8 667.22,-275.72 667.12,-276.65 666.85,-277.59 666.43,-278.53 665.86,-279.47 665.14,-280.41 664.29,-281.35 663.3,-282.28 662.19,-283.2 660.97,-284.11 659.63,-285.01 658.2,-285.89 656.67,-286.75 655.06,-287.59 653.36,-288.41 651.59,-289.2 649.76,-289.96 647.87,-290.69 645.93,-291.39 643.93,-292.06 641.9,-292.69 639.83,-293.29 637.73,-293.84 635.6,-294.35 633.45,-294.82 631.27,-295.25 629.08,-295.64 626.88,-295.97 624.66,-296.26 622.44,-296.51 620.2,-296.7 617.97,-296.85 615.73,-296.95 613.48,-297 611.24,-297 608.99,-296.95 606.75,-296.85 604.51,-296.7 602.28,-296.51 600.06,-296.26 597.84,-295.97 595.64,-295.64 593.45,-295.25 591.27,-294.82 589.12,-294.35 586.99,-293.84 584.89,-293.29 582.82,-292.69 580.79,-292.06 578.79,-291.39 576.85,-290.69 574.96,-289.96 573.12,-289.2 571.36,-288.41 569.66,-287.59 568.05,-286.75 566.52,-285.89 565.08,-285.01 563.75,-284.11 562.53,-283.2 561.42,-282.28 560.43,-281.35 559.58,-280.41 558.86,-279.47 558.29,-278.53 557.87,-277.59 557.6,-276.65 557.5,-275.72 557.56,-274.8 557.8,-273.89 558.2,-272.99 558.79,-272.11 559.55,-271.25 560.49,-270.41 561.61,-269.59 562.92,-268.8 564.39,-268.04 566.05,-267.31 567.87,-266.61 569.86,-265.94 572.02,-265.31 574.33,-264.71 576.78,-264.16 579.38,-263.65 582.1,-263.18 584.95,-262.75 587.9,-262.36 590.96,-262.03 594.1,-261.74 597.32,-261.49 600.6,-261.3 603.92,-261.15 607.28,-261.05 610.66,-261 614.05,-261 617.44,-261.05\"/>\n<text text-anchor=\"middle\" x=\"612.36\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(or22)]</text>\n</g>\n<!-- [neg(or22)]&#45;&gt;[neg(and12)] -->\n<g id=\"edge21\" class=\"edge\">\n<title>[neg(or22)]&#45;&gt;[neg(and12)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M611.35,-260.8C610.69,-249.58 609.81,-234.67 609.05,-221.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"612.56,-221.76 608.48,-211.98 605.57,-222.17 612.56,-221.76\"/>\n<text text-anchor=\"middle\" x=\"622.86\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">or22</text>\n</g>\n<!-- [neg(or22)]&#45;&gt;[neg(not1)] -->\n<g id=\"edge22\" class=\"edge\">\n<title>[neg(or22)]&#45;&gt;[neg(not1)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M636.62,-262.01C657.22,-248.44 686.94,-228.86 709.46,-214.02\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"711.24,-217.04 717.67,-208.61 707.39,-211.19 711.24,-217.04\"/>\n<text text-anchor=\"middle\" x=\"696.86\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">or22</text>\n</g>\n<!-- [neg(or22),neg(not2),neg(or4)] -->\n<g id=\"node28\" class=\"node\">\n<title>[neg(or22),neg(not2),neg(or4)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"698.21,-783.05 706.06,-783.15 713.83,-783.3 721.48,-783.49 728.99,-783.74 736.33,-784.03 743.46,-784.36 750.36,-784.75 757.01,-785.18 763.37,-785.65 769.43,-786.16 775.17,-786.71 780.55,-787.31 785.58,-787.94 790.23,-788.61 794.49,-789.31 798.35,-790.04 801.81,-790.8 804.85,-791.59 807.47,-792.41 809.67,-793.25 811.45,-794.11 812.81,-794.99 813.76,-795.89 814.31,-796.8 814.45,-797.72 814.21,-798.65 813.59,-799.59 812.61,-800.53 811.27,-801.47 809.6,-802.41 807.6,-803.35 805.3,-804.28 802.72,-805.2 799.86,-806.11 796.74,-807.01 793.39,-807.89 789.82,-808.75 786.05,-809.59 782.1,-810.41 777.97,-811.2 773.69,-811.96 769.27,-812.69 764.73,-813.39 760.08,-814.06 755.34,-814.69 750.5,-815.29 745.59,-815.84 740.62,-816.35 735.59,-816.82 730.52,-817.25 725.41,-817.64 720.26,-817.97 715.08,-818.26 709.89,-818.51 704.68,-818.7 699.45,-818.85 694.22,-818.95 688.98,-819 683.74,-819 678.5,-818.95 673.27,-818.85 668.04,-818.7 662.83,-818.51 657.63,-818.26 652.46,-817.97 647.31,-817.64 642.2,-817.25 637.12,-816.82 632.1,-816.35 627.12,-815.84 622.22,-815.29 617.38,-814.69 612.64,-814.06 607.98,-813.39 603.44,-812.69 599.03,-811.96 594.75,-811.2 590.62,-810.41 586.67,-809.59 582.9,-808.75 579.33,-807.89 575.98,-807.01 572.86,-806.11 570,-805.2 567.42,-804.28 565.12,-803.35 563.12,-802.41 561.45,-801.47 560.11,-800.53 559.13,-799.59 558.51,-798.65 558.26,-797.72 558.41,-796.8 558.96,-795.89 559.91,-794.99 561.27,-794.11 563.05,-793.25 565.25,-792.41 567.87,-791.59 570.91,-790.8 574.36,-790.04 578.23,-789.31 582.49,-788.61 587.14,-787.94 592.16,-787.31 597.55,-786.71 603.29,-786.16 609.35,-785.65 615.71,-785.18 622.36,-784.75 629.26,-784.36 636.39,-784.03 643.73,-783.74 651.24,-783.49 658.89,-783.3 666.66,-783.15 674.51,-783.05 682.4,-783 690.32,-783 698.21,-783.05\"/>\n<text text-anchor=\"middle\" x=\"686.36\" y=\"-797.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(or22),neg(not2),neg(or4)]</text>\n</g>\n<!-- [neg(or22),neg(not2),neg(or4)]&#45;&gt;[neg(and12),neg(not2),neg(or4)] -->\n<g id=\"edge23\" class=\"edge\">\n<title>[neg(or22),neg(not2),neg(or4)]&#45;&gt;[neg(and12),neg(not2),neg(or4)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M685.75,-782.8C685.36,-771.58 684.83,-756.67 684.37,-743.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"687.88,-743.85 684.03,-733.98 680.88,-744.1 687.88,-743.85\"/>\n<text text-anchor=\"middle\" x=\"696.86\" y=\"-753.8\" font-family=\"Times,serif\" font-size=\"14.00\">or22</text>\n</g>\n<!-- [neg(or22),neg(not2),neg(or4)]&#45;&gt;[neg(not1),neg(not2),neg(or4)] -->\n<g id=\"edge24\" class=\"edge\">\n<title>[neg(or22),neg(not2),neg(or4)]&#45;&gt;[neg(not1),neg(not2),neg(or4)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M739.82,-783.71C786.9,-769.37 855.41,-748.5 904.56,-733.52\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"905.37,-736.94 913.91,-730.67 903.33,-730.24 905.37,-736.94\"/>\n<text text-anchor=\"middle\" x=\"854.86\" y=\"-753.8\" font-family=\"Times,serif\" font-size=\"14.00\">or22</text>\n</g>\n<!-- [neg(or3)] -->\n<g id=\"node29\" class=\"node\">\n<title>[neg(or3)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"489.96,-348.05 493,-348.15 496.01,-348.3 498.98,-348.49 501.89,-348.74 504.73,-349.03 507.5,-349.36 510.18,-349.75 512.75,-350.18 515.22,-350.65 517.57,-351.16 519.79,-351.71 521.88,-352.31 523.83,-352.94 525.64,-353.61 527.29,-354.31 528.79,-355.04 530.13,-355.8 531.3,-356.59 532.32,-357.41 533.17,-358.25 533.86,-359.11 534.39,-359.99 534.76,-360.89 534.97,-361.8 535.03,-362.72 534.94,-363.65 534.69,-364.59 534.31,-365.53 533.79,-366.47 533.15,-367.41 532.37,-368.35 531.48,-369.28 530.48,-370.2 529.37,-371.11 528.16,-372.01 526.86,-372.89 525.48,-373.75 524.02,-374.59 522.48,-375.41 520.88,-376.2 519.22,-376.96 517.51,-377.69 515.75,-378.39 513.95,-379.06 512.11,-379.69 510.23,-380.29 508.33,-380.84 506.4,-381.35 504.45,-381.82 502.48,-382.25 500.5,-382.64 498.5,-382.97 496.5,-383.26 494.48,-383.51 492.46,-383.7 490.44,-383.85 488.41,-383.95 486.38,-384 484.34,-384 482.31,-383.95 480.28,-383.85 478.26,-383.7 476.24,-383.51 474.22,-383.26 472.21,-382.97 470.22,-382.64 468.24,-382.25 466.27,-381.82 464.32,-381.35 462.39,-380.84 460.49,-380.29 458.61,-379.69 456.77,-379.06 454.97,-378.39 453.21,-377.69 451.5,-376.96 449.84,-376.2 448.24,-375.41 446.7,-374.59 445.24,-373.75 443.86,-372.89 442.56,-372.01 441.35,-371.11 440.24,-370.2 439.24,-369.28 438.35,-368.35 437.57,-367.41 436.92,-366.47 436.41,-365.53 436.02,-364.59 435.78,-363.65 435.69,-362.72 435.75,-361.8 435.96,-360.89 436.33,-359.99 436.86,-359.11 437.55,-358.25 438.4,-357.41 439.42,-356.59 440.59,-355.8 441.93,-355.04 443.43,-354.31 445.08,-353.61 446.88,-352.94 448.83,-352.31 450.92,-351.71 453.15,-351.16 455.5,-350.65 457.96,-350.18 460.54,-349.75 463.22,-349.36 465.98,-349.03 468.83,-348.74 471.74,-348.49 474.71,-348.3 477.72,-348.15 480.76,-348.05 483.83,-348 486.89,-348 489.96,-348.05\"/>\n<text text-anchor=\"middle\" x=\"485.36\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(or3)]</text>\n</g>\n<!-- [neg(or3)]&#45;&gt;[neg(not2)] -->\n<g id=\"edge26\" class=\"edge\">\n<title>[neg(or3)]&#45;&gt;[neg(not2)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M485.36,-347.8C485.36,-336.58 485.36,-321.67 485.36,-308.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"488.86,-308.98 485.36,-298.98 481.86,-308.98 488.86,-308.98\"/>\n<text text-anchor=\"middle\" x=\"494.86\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">or3</text>\n</g>\n<!-- [neg(or3)]&#45;&gt;[neg(or22)] -->\n<g id=\"edge25\" class=\"edge\">\n<title>[neg(or3)]&#45;&gt;[neg(or22)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M508.95,-349.21C529.2,-335.66 558.54,-316.02 580.81,-301.12\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"582.55,-304.16 588.91,-295.69 578.66,-298.35 582.55,-304.16\"/>\n<text text-anchor=\"middle\" x=\"566.86\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">or3</text>\n</g>\n<!-- [neg(or3),neg(not2),neg(or4)]&#45;&gt;[neg(not2),neg(not2),neg(or4)] -->\n<g id=\"edge28\" class=\"edge\">\n<title>[neg(or3),neg(not2),neg(or4)]&#45;&gt;[neg(not2),neg(not2),neg(or4)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M521.96,-870C501.01,-857 471.92,-838.96 448.98,-824.72\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"450.87,-821.77 440.53,-819.48 447.18,-827.72 450.87,-821.77\"/>\n<text text-anchor=\"middle\" x=\"498.86\" y=\"-840.8\" font-family=\"Times,serif\" font-size=\"14.00\">or3</text>\n</g>\n<!-- [neg(or3),neg(not2),neg(or4)]&#45;&gt;[neg(or22),neg(not2),neg(or4)] -->\n<g id=\"edge27\" class=\"edge\">\n<title>[neg(or3),neg(not2),neg(or4)]&#45;&gt;[neg(or22),neg(not2),neg(or4)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M576.75,-870C597.7,-857 626.79,-838.96 649.74,-824.72\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"651.54,-827.72 658.19,-819.48 647.85,-821.77 651.54,-827.72\"/>\n<text text-anchor=\"middle\" x=\"635.86\" y=\"-840.8\" font-family=\"Times,serif\" font-size=\"14.00\">or3</text>\n</g>\n<!-- [neg(or4)]&#45;&gt;[neg(and3)] -->\n<g id=\"edge29\" class=\"edge\">\n<title>[neg(or4)]&#45;&gt;[neg(and3)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M400.31,-435.21C391.62,-423.1 379.73,-406.53 369.85,-392.76\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"372.94,-391.07 364.27,-384.99 367.26,-395.15 372.94,-391.07\"/>\n<text text-anchor=\"middle\" x=\"395.86\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\">or4</text>\n</g>\n<!-- [neg(or4)]&#45;&gt;[neg(or3)] -->\n<g id=\"edge30\" class=\"edge\">\n<title>[neg(or4)]&#45;&gt;[neg(or3)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M426.78,-435.21C437.42,-422.82 452.06,-405.78 464.04,-391.82\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"466.62,-394.2 470.48,-384.33 461.31,-389.64 466.62,-394.2\"/>\n<text text-anchor=\"middle\" x=\"462.86\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\">or4</text>\n</g>\n<!-- [neg(output)] -->\n<g id=\"node32\" class=\"node\">\n<title>[neg(output)]</title>\n<polygon fill=\"none\" stroke=\"blue\" points=\"555.07,-1131.05 558.85,-1131.15 562.59,-1131.3 566.28,-1131.49 569.89,-1131.74 573.43,-1132.03 576.86,-1132.36 580.19,-1132.75 583.39,-1133.18 586.46,-1133.65 589.37,-1134.16 592.14,-1134.71 594.73,-1135.31 597.15,-1135.94 599.39,-1136.61 601.45,-1137.31 603.31,-1138.04 604.97,-1138.8 606.43,-1139.59 607.7,-1140.41 608.76,-1141.25 609.61,-1142.11 610.27,-1142.99 610.73,-1143.89 610.99,-1144.8 611.06,-1145.72 610.95,-1146.65 610.65,-1147.59 610.17,-1148.53 609.53,-1149.47 608.72,-1150.41 607.76,-1151.35 606.65,-1152.28 605.41,-1153.2 604.03,-1154.11 602.53,-1155.01 600.92,-1155.89 599.2,-1156.75 597.38,-1157.59 595.47,-1158.41 593.49,-1159.2 591.43,-1159.96 589.3,-1160.69 587.11,-1161.39 584.87,-1162.06 582.58,-1162.69 580.26,-1163.29 577.89,-1163.84 575.5,-1164.35 573.08,-1164.82 570.63,-1165.25 568.17,-1165.64 565.69,-1165.97 563.2,-1166.26 560.69,-1166.51 558.18,-1166.7 555.67,-1166.85 553.14,-1166.95 550.62,-1167 548.1,-1167 545.57,-1166.95 543.05,-1166.85 540.54,-1166.7 538.02,-1166.51 535.52,-1166.26 533.03,-1165.97 530.55,-1165.64 528.09,-1165.25 525.64,-1164.82 523.22,-1164.35 520.83,-1163.84 518.46,-1163.29 516.13,-1162.69 513.85,-1162.06 511.61,-1161.39 509.42,-1160.69 507.29,-1159.96 505.23,-1159.2 503.24,-1158.41 501.34,-1157.59 499.52,-1156.75 497.8,-1155.89 496.19,-1155.01 494.69,-1154.11 493.31,-1153.2 492.06,-1152.28 490.96,-1151.35 490,-1150.41 489.19,-1149.47 488.55,-1148.53 488.07,-1147.59 487.77,-1146.65 487.66,-1145.72 487.73,-1144.8 487.99,-1143.89 488.45,-1142.99 489.11,-1142.11 489.96,-1141.25 491.02,-1140.41 492.29,-1139.59 493.75,-1138.8 495.41,-1138.04 497.27,-1137.31 499.32,-1136.61 501.56,-1135.94 503.99,-1135.31 506.58,-1134.71 509.34,-1134.16 512.26,-1133.65 515.33,-1133.18 518.53,-1132.75 521.85,-1132.36 525.29,-1132.03 528.82,-1131.74 532.44,-1131.49 536.13,-1131.3 539.87,-1131.15 543.65,-1131.05 547.45,-1131 551.27,-1131 555.07,-1131.05\"/>\n<text text-anchor=\"middle\" x=\"549.36\" y=\"-1145.3\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(output)]</text>\n</g>\n<!-- [neg(output)]&#45;&gt;[neg(and5)] -->\n<g id=\"edge31\" class=\"edge\">\n<title>[neg(output)]&#45;&gt;[neg(and5)]</title>\n<path fill=\"none\" stroke=\"black\" d=\"M549.36,-1130.8C549.36,-1119.58 549.36,-1104.67 549.36,-1091.69\"/>\n<polygon fill=\"black\" stroke=\"black\" points=\"552.86,-1091.98 549.36,-1081.98 545.86,-1091.98 552.86,-1091.98\"/>\n<text text-anchor=\"middle\" x=\"566.86\" y=\"-1101.8\" font-family=\"Times,serif\" font-size=\"14.00\">output</text>\n</g>\n</g>\n</svg>\n",
+      "image/svg+xml": [
+       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 10.0.1 (20240210.2158)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"1147pt\" height=\"1195pt\"\n",
+       " viewBox=\"0.00 0.00 1146.81 1194.50\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 1190.5)\">\n",
+       "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-1190.5 1142.81,-1190.5 1142.81,4 -4,4\"/>\n",
+       "<!-- [] -->\n",
+       "<g id=\"node1\" class=\"node\">\n",
+       "<title>[]</title>\n",
+       "<polygon fill=\"none\" stroke=\"green\" points=\"532.1,-124.5 478.1,-124.5 478.1,-88.5 532.1,-88.5 532.1,-124.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"505.1\" y=\"-101.45\" font-family=\"Times,serif\" font-size=\"14.00\">[]</text>\n",
+       "</g>\n",
+       "<!-- [neg(a),neg(b),neg(and2)] -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>[neg(a),neg(b),neg(and2)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"124.65,-88.55 131.64,-88.65 138.56,-88.8 145.38,-88.99 152.07,-89.24 158.6,-89.53 164.96,-89.86 171.1,-90.25 177.02,-90.68 182.69,-91.15 188.09,-91.66 193.2,-92.21 198,-92.81 202.47,-93.44 206.62,-94.11 210.41,-94.81 213.85,-95.54 216.93,-96.3 219.63,-97.09 221.97,-97.91 223.93,-98.75 225.51,-99.61 226.73,-100.49 227.58,-101.39 228.06,-102.3 228.19,-103.22 227.98,-104.15 227.42,-105.09 226.55,-106.03 225.36,-106.97 223.87,-107.91 222.09,-108.85 220.04,-109.78 217.74,-110.7 215.19,-111.61 212.42,-112.51 209.43,-113.39 206.25,-114.25 202.89,-115.09 199.37,-115.91 195.69,-116.7 191.88,-117.46 187.95,-118.19 183.9,-118.89 179.76,-119.56 175.53,-120.19 171.23,-120.79 166.86,-121.34 162.43,-121.85 157.95,-122.32 153.43,-122.75 148.87,-123.14 144.29,-123.47 139.68,-123.76 135.05,-124.01 130.41,-124.2 125.76,-124.35 121.1,-124.45 116.43,-124.5 111.76,-124.5 107.1,-124.45 102.43,-124.35 97.78,-124.2 93.14,-124.01 88.51,-123.76 83.9,-123.47 79.32,-123.14 74.76,-122.75 70.24,-122.32 65.76,-121.85 61.33,-121.34 56.96,-120.79 52.66,-120.19 48.43,-119.56 44.29,-118.89 40.24,-118.19 36.31,-117.46 32.5,-116.7 28.82,-115.91 25.3,-115.09 21.94,-114.25 18.76,-113.39 15.78,-112.51 13,-111.61 10.46,-110.7 8.15,-109.78 6.1,-108.85 4.33,-107.91 2.84,-106.97 1.64,-106.03 0.77,-105.09 0.22,-104.15 0,-103.22 0.13,-102.3 0.62,-101.39 1.46,-100.49 2.68,-99.61 4.26,-98.75 6.22,-97.91 8.56,-97.09 11.26,-96.3 14.34,-95.54 17.78,-94.81 21.57,-94.11 25.72,-93.44 30.19,-92.81 34.99,-92.21 40.1,-91.66 45.5,-91.15 51.17,-90.68 57.09,-90.25 63.23,-89.86 69.59,-89.53 76.12,-89.24 82.81,-88.99 89.63,-88.8 96.55,-88.65 103.54,-88.55 110.57,-88.5 117.62,-88.5 124.65,-88.55\"/>\n",
+       "<text text-anchor=\"middle\" x=\"114.1\" y=\"-101.45\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(a),neg(b),neg(and2)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(b),neg(and2)] -->\n",
+       "<g id=\"node9\" class=\"node\">\n",
+       "<title>[neg(b),neg(and2)]</title>\n",
+       "<ellipse fill=\"none\" stroke=\"red\" cx=\"114.1\" cy=\"-18\" rx=\"81.04\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"114.1\" y=\"-12.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(b),neg(and2)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(a),neg(b),neg(and2)]&#45;&gt;[neg(b),neg(and2)] -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>[neg(a),neg(b),neg(and2)]&#45;&gt;[neg(b),neg(and2)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M114.1,-88.41C114.1,-76.76 114.1,-61.05 114.1,-47.52\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"117.6,-47.86 114.1,-37.86 110.6,-47.86 117.6,-47.86\"/>\n",
+       "<text text-anchor=\"middle\" x=\"117.1\" y=\"-57.2\" font-family=\"Times,serif\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- [neg(and11),neg(and2)] -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>[neg(and11),neg(and2)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"128.85,-177.05 135.3,-177.15 141.69,-177.3 147.99,-177.49 154.17,-177.74 160.2,-178.03 166.07,-178.36 171.75,-178.75 177.21,-179.18 182.45,-179.65 187.43,-180.16 192.15,-180.71 196.58,-181.31 200.72,-181.94 204.55,-182.61 208.05,-183.31 211.23,-184.04 214.07,-184.8 216.57,-185.59 218.72,-186.41 220.53,-187.25 222,-188.11 223.12,-188.99 223.9,-189.89 224.35,-190.8 224.47,-191.72 224.27,-192.65 223.76,-193.59 222.95,-194.53 221.85,-195.47 220.48,-196.41 218.84,-197.35 216.94,-198.28 214.81,-199.2 212.46,-200.11 209.9,-201.01 207.14,-201.89 204.21,-202.75 201.11,-203.59 197.85,-204.41 194.46,-205.2 190.94,-205.96 187.3,-206.69 183.57,-207.39 179.74,-208.06 175.84,-208.69 171.86,-209.29 167.82,-209.84 163.73,-210.35 159.6,-210.82 155.42,-211.25 151.22,-211.64 146.98,-211.97 142.73,-212.26 138.45,-212.51 134.16,-212.7 129.87,-212.85 125.56,-212.95 121.25,-213 116.94,-213 112.63,-212.95 108.33,-212.85 104.03,-212.7 99.74,-212.51 95.47,-212.26 91.21,-211.97 86.97,-211.64 82.77,-211.25 78.59,-210.82 74.46,-210.35 70.37,-209.84 66.33,-209.29 62.35,-208.69 58.45,-208.06 54.62,-207.39 50.89,-206.69 47.25,-205.96 43.73,-205.2 40.34,-204.41 37.09,-203.59 33.98,-202.75 31.05,-201.89 28.29,-201.01 25.73,-200.11 23.38,-199.2 21.25,-198.28 19.36,-197.35 17.72,-196.41 16.34,-195.47 15.24,-194.53 14.43,-193.59 13.92,-192.65 13.72,-191.72 13.84,-190.8 14.29,-189.89 15.07,-188.99 16.19,-188.11 17.66,-187.25 19.47,-186.41 21.62,-185.59 24.12,-184.8 26.96,-184.04 30.14,-183.31 33.65,-182.61 37.47,-181.94 41.61,-181.31 46.04,-180.71 50.76,-180.16 55.74,-179.65 60.98,-179.18 66.44,-178.75 72.12,-178.36 77.99,-178.03 84.03,-177.74 90.2,-177.49 96.5,-177.3 102.89,-177.15 109.34,-177.05 115.84,-177 122.35,-177 128.85,-177.05\"/>\n",
+       "<text text-anchor=\"middle\" x=\"119.1\" y=\"-189.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(and11),neg(and2)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(and11),neg(and2)]&#45;&gt;[neg(a),neg(b),neg(and2)] -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>[neg(and11),neg(and2)]&#45;&gt;[neg(a),neg(b),neg(and2)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M118.11,-176.91C117.43,-165.26 116.53,-149.55 115.74,-136.02\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"119.26,-136.14 115.19,-126.36 112.27,-136.55 119.26,-136.14\"/>\n",
+       "<text text-anchor=\"middle\" x=\"133.6\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">and11</text>\n",
+       "</g>\n",
+       "<!-- [neg(and12)] -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>[neg(and12)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"636.91,-177.05 640.76,-177.15 644.58,-177.3 648.33,-177.49 652.02,-177.74 655.62,-178.03 659.12,-178.36 662.51,-178.75 665.77,-179.18 668.89,-179.65 671.86,-180.16 674.68,-180.71 677.32,-181.31 679.79,-181.94 682.07,-182.61 684.16,-183.31 686.06,-184.04 687.75,-184.8 689.24,-185.59 690.53,-186.41 691.61,-187.25 692.48,-188.11 693.15,-188.99 693.62,-189.89 693.89,-190.8 693.96,-191.72 693.84,-192.65 693.53,-193.59 693.05,-194.53 692.4,-195.47 691.57,-196.41 690.6,-197.35 689.47,-198.28 688.2,-199.2 686.79,-200.11 685.27,-201.01 683.62,-201.89 681.87,-202.75 680.02,-203.59 678.08,-204.41 676.05,-205.2 673.95,-205.96 671.79,-206.69 669.56,-207.39 667.28,-208.06 664.95,-208.69 662.57,-209.29 660.16,-209.84 657.72,-210.35 655.26,-210.82 652.77,-211.25 650.26,-211.64 647.73,-211.97 645.19,-212.26 642.64,-212.51 640.09,-212.7 637.52,-212.85 634.95,-212.95 632.38,-213 629.81,-213 627.24,-212.95 624.67,-212.85 622.11,-212.7 619.55,-212.51 617,-212.26 614.46,-211.97 611.93,-211.64 609.42,-211.25 606.93,-210.82 604.47,-210.35 602.03,-209.84 599.62,-209.29 597.25,-208.69 594.92,-208.06 592.63,-207.39 590.41,-206.69 588.24,-205.96 586.14,-205.2 584.11,-204.41 582.17,-203.59 580.32,-202.75 578.57,-201.89 576.93,-201.01 575.4,-200.11 573.99,-199.2 572.72,-198.28 571.6,-197.35 570.62,-196.41 569.8,-195.47 569.14,-194.53 568.66,-193.59 568.35,-192.65 568.23,-191.72 568.31,-190.8 568.57,-189.89 569.04,-188.99 569.71,-188.11 570.58,-187.25 571.66,-186.41 572.95,-185.59 574.44,-184.8 576.13,-184.04 578.03,-183.31 580.12,-182.61 582.4,-181.94 584.87,-181.31 587.51,-180.71 590.33,-180.16 593.3,-179.65 596.43,-179.18 599.69,-178.75 603.07,-178.36 606.57,-178.03 610.17,-177.74 613.86,-177.49 617.62,-177.3 621.43,-177.15 625.28,-177.05 629.15,-177 633.04,-177 636.91,-177.05\"/>\n",
+       "<text text-anchor=\"middle\" x=\"631.1\" y=\"-189.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(and12)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(c),neg(d)] -->\n",
+       "<g id=\"node10\" class=\"node\">\n",
+       "<title>[neg(c),neg(d)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"630.72,-88.55 635.11,-88.65 639.45,-88.8 643.72,-88.99 647.92,-89.24 652.02,-89.53 656.01,-89.86 659.86,-90.25 663.58,-90.68 667.13,-91.15 670.52,-91.66 673.72,-92.21 676.73,-92.81 679.54,-93.44 682.14,-94.11 684.52,-94.81 686.68,-95.54 688.61,-96.3 690.31,-97.09 691.77,-97.91 693,-98.75 694,-99.61 694.76,-100.49 695.29,-101.39 695.6,-102.3 695.68,-103.22 695.54,-104.15 695.2,-105.09 694.65,-106.03 693.9,-106.97 692.96,-107.91 691.85,-108.85 690.56,-109.78 689.12,-110.7 687.52,-111.61 685.78,-112.51 683.91,-113.39 681.91,-114.25 679.81,-115.09 677.6,-115.91 675.29,-116.7 672.9,-117.46 670.43,-118.19 667.89,-118.89 665.29,-119.56 662.64,-120.19 659.94,-120.79 657.2,-121.34 654.42,-121.85 651.61,-122.32 648.77,-122.75 645.92,-123.14 643.04,-123.47 640.15,-123.76 637.24,-124.01 634.33,-124.2 631.41,-124.35 628.49,-124.45 625.56,-124.5 622.63,-124.5 619.7,-124.45 616.78,-124.35 613.86,-124.2 610.95,-124.01 608.04,-123.76 605.15,-123.47 602.28,-123.14 599.42,-122.75 596.58,-122.32 593.77,-121.85 590.99,-121.34 588.25,-120.79 585.55,-120.19 582.9,-119.56 580.3,-118.89 577.76,-118.19 575.29,-117.46 572.9,-116.7 570.6,-115.91 568.39,-115.09 566.28,-114.25 564.28,-113.39 562.41,-112.51 560.67,-111.61 559.07,-110.7 557.63,-109.78 556.34,-108.85 555.23,-107.91 554.29,-106.97 553.55,-106.03 552.99,-105.09 552.65,-104.15 552.51,-103.22 552.6,-102.3 552.9,-101.39 553.43,-100.49 554.19,-99.61 555.19,-98.75 556.42,-97.91 557.88,-97.09 559.58,-96.3 561.51,-95.54 563.67,-94.81 566.05,-94.11 568.65,-93.44 571.46,-92.81 574.47,-92.21 577.67,-91.66 581.06,-91.15 584.62,-90.68 588.33,-90.25 592.19,-89.86 596.17,-89.53 600.27,-89.24 604.47,-88.99 608.75,-88.8 613.09,-88.65 617.47,-88.55 621.88,-88.5 626.31,-88.5 630.72,-88.55\"/>\n",
+       "<text text-anchor=\"middle\" x=\"624.1\" y=\"-101.45\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(c),neg(d)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(and12)]&#45;&gt;[neg(c),neg(d)] -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>[neg(and12)]&#45;&gt;[neg(c),neg(d)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M629.71,-176.91C628.77,-165.26 627.5,-149.55 626.4,-136.02\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"629.92,-136.04 625.62,-126.36 622.94,-136.61 629.92,-136.04\"/>\n",
+       "<text text-anchor=\"middle\" x=\"645.6\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">and12</text>\n",
+       "</g>\n",
+       "<!-- [neg(and12),neg(not2),neg(or4)] -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>[neg(and12),neg(not2),neg(or4)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"724.07,-708.05 732.67,-708.15 741.17,-708.3 749.55,-708.49 757.78,-708.74 765.81,-709.03 773.62,-709.36 781.18,-709.75 788.45,-710.18 795.42,-710.65 802.06,-711.16 808.33,-711.71 814.24,-712.31 819.74,-712.94 824.83,-713.61 829.5,-714.31 833.73,-715.04 837.51,-715.8 840.83,-716.59 843.7,-717.41 846.11,-718.25 848.06,-719.11 849.55,-719.99 850.6,-720.89 851.19,-721.8 851.35,-722.72 851.09,-723.65 850.41,-724.59 849.33,-725.53 847.87,-726.47 846.04,-727.41 843.85,-728.35 841.33,-729.28 838.5,-730.2 835.37,-731.11 831.96,-732.01 828.29,-732.89 824.38,-733.75 820.25,-734.59 815.92,-735.41 811.4,-736.2 806.72,-736.96 801.88,-737.69 796.91,-738.39 791.82,-739.06 786.62,-739.69 781.33,-740.29 775.96,-740.84 770.51,-741.35 765.01,-741.82 759.45,-742.25 753.85,-742.64 748.21,-742.97 742.55,-743.26 736.86,-743.51 731.15,-743.7 725.43,-743.85 719.7,-743.95 713.96,-744 708.23,-744 702.49,-743.95 696.76,-743.85 691.04,-743.7 685.33,-743.51 679.64,-743.26 673.98,-742.97 668.34,-742.64 662.74,-742.25 657.19,-741.82 651.68,-741.35 646.24,-740.84 640.86,-740.29 635.57,-739.69 630.37,-739.06 625.28,-738.39 620.31,-737.69 615.47,-736.96 610.79,-736.2 606.27,-735.41 601.94,-734.59 597.81,-733.75 593.9,-732.89 590.23,-732.01 586.82,-731.11 583.69,-730.2 580.86,-729.28 578.34,-728.35 576.16,-727.41 574.32,-726.47 572.86,-725.53 571.78,-724.59 571.1,-723.65 570.84,-722.72 571,-721.8 571.6,-720.89 572.64,-719.99 574.13,-719.11 576.08,-718.25 578.49,-717.41 581.36,-716.59 584.69,-715.8 588.47,-715.04 592.69,-714.31 597.36,-713.61 602.45,-712.94 607.96,-712.31 613.86,-711.71 620.14,-711.16 626.77,-710.65 633.74,-710.18 641.01,-709.75 648.57,-709.36 656.38,-709.03 664.42,-708.74 672.64,-708.49 681.02,-708.3 689.52,-708.15 698.12,-708.05 706.76,-708 715.43,-708 724.07,-708.05\"/>\n",
+       "<text text-anchor=\"middle\" x=\"711.1\" y=\"-720.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(and12),neg(not2),neg(or4)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(c),neg(d),neg(not2),neg(or4)] -->\n",
+       "<g id=\"node11\" class=\"node\">\n",
+       "<title>[neg(c),neg(d),neg(not2),neg(or4)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"722.88,-619.55 732.01,-619.65 741.04,-619.8 749.94,-619.99 758.68,-620.24 767.21,-620.53 775.51,-620.86 783.53,-621.25 791.26,-621.68 798.66,-622.15 805.71,-622.66 812.38,-623.21 818.65,-623.81 824.49,-624.44 829.9,-625.11 834.86,-625.81 839.35,-626.54 843.37,-627.3 846.9,-628.09 849.95,-628.91 852.51,-629.75 854.58,-630.61 856.16,-631.49 857.27,-632.39 857.9,-633.3 858.07,-634.22 857.79,-635.15 857.07,-636.09 855.93,-637.03 854.37,-637.97 852.43,-638.91 850.11,-639.85 847.43,-640.78 844.42,-641.7 841.1,-642.61 837.48,-643.51 833.58,-644.39 829.43,-645.25 825.04,-646.09 820.44,-646.91 815.64,-647.7 810.67,-648.46 805.53,-649.19 800.25,-649.89 794.84,-650.56 789.32,-651.19 783.7,-651.79 777.99,-652.34 772.2,-652.85 766.36,-653.32 760.46,-653.75 754.51,-654.14 748.52,-654.47 742.5,-654.76 736.46,-655.01 730.4,-655.2 724.32,-655.35 718.24,-655.45 712.14,-655.5 706.05,-655.5 699.96,-655.45 693.87,-655.35 687.79,-655.2 681.73,-655.01 675.69,-654.76 669.67,-654.47 663.68,-654.14 657.74,-653.75 651.83,-653.32 645.99,-652.85 640.2,-652.34 634.5,-651.79 628.87,-651.19 623.35,-650.56 617.94,-649.89 612.66,-649.19 607.53,-648.46 602.55,-647.7 597.75,-646.91 593.15,-646.09 588.76,-645.25 584.61,-644.39 580.72,-643.51 577.1,-642.61 573.77,-641.7 570.76,-640.78 568.08,-639.85 565.76,-638.91 563.82,-637.97 562.26,-637.03 561.12,-636.09 560.4,-635.15 560.12,-634.22 560.29,-633.3 560.92,-632.39 562.03,-631.49 563.61,-630.61 565.69,-629.75 568.24,-628.91 571.29,-628.09 574.83,-627.3 578.84,-626.54 583.33,-625.81 588.29,-625.11 593.7,-624.44 599.54,-623.81 605.81,-623.21 612.48,-622.66 619.53,-622.15 626.93,-621.68 634.66,-621.25 642.68,-620.86 650.98,-620.53 659.51,-620.24 668.25,-619.99 677.15,-619.8 686.18,-619.65 695.31,-619.55 704.49,-619.5 713.7,-619.5 722.88,-619.55\"/>\n",
+       "<text text-anchor=\"middle\" x=\"709.1\" y=\"-632.45\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(c),neg(d),neg(not2),neg(or4)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(and12),neg(not2),neg(or4)]&#45;&gt;[neg(c),neg(d),neg(not2),neg(or4)] -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>[neg(and12),neg(not2),neg(or4)]&#45;&gt;[neg(c),neg(d),neg(not2),neg(or4)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M710.7,-707.91C710.43,-696.26 710.07,-680.55 709.76,-667.02\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"713.26,-667.28 709.53,-657.36 706.26,-667.44 713.26,-667.28\"/>\n",
+       "<text text-anchor=\"middle\" x=\"726.6\" y=\"-676.7\" font-family=\"Times,serif\" font-size=\"14.00\">and12</text>\n",
+       "</g>\n",
+       "<!-- [neg(and3)] -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>[neg(and3)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"371.46,-354.05 375.01,-354.15 378.52,-354.3 381.99,-354.49 385.38,-354.74 388.7,-355.03 391.93,-355.36 395.05,-355.75 398.06,-356.18 400.94,-356.65 403.68,-357.16 406.28,-357.71 408.71,-358.31 410.99,-358.94 413.09,-359.61 415.02,-360.31 416.77,-361.04 418.33,-361.8 419.7,-362.59 420.89,-363.41 421.89,-364.25 422.69,-365.11 423.31,-365.99 423.74,-366.89 423.99,-367.8 424.05,-368.72 423.94,-369.65 423.66,-370.59 423.22,-371.53 422.61,-372.47 421.85,-373.41 420.95,-374.35 419.91,-375.28 418.74,-376.2 417.45,-377.11 416.04,-378.01 414.52,-378.89 412.91,-379.75 411.2,-380.59 409.41,-381.41 407.54,-382.2 405.61,-382.96 403.61,-383.69 401.56,-384.39 399.45,-385.06 397.3,-385.69 395.12,-386.29 392.9,-386.84 390.65,-387.35 388.37,-387.82 386.08,-388.25 383.76,-388.64 381.43,-388.97 379.09,-389.26 376.74,-389.51 374.38,-389.7 372.02,-389.85 369.65,-389.95 367.28,-390 364.91,-390 362.54,-389.95 360.17,-389.85 357.81,-389.7 355.45,-389.51 353.1,-389.26 350.76,-388.97 348.43,-388.64 346.12,-388.25 343.82,-387.82 341.54,-387.35 339.29,-386.84 337.07,-386.29 334.89,-385.69 332.74,-385.06 330.64,-384.39 328.58,-383.69 326.58,-382.96 324.65,-382.2 322.78,-381.41 320.99,-380.59 319.28,-379.75 317.67,-378.89 316.15,-378.01 314.74,-377.11 313.45,-376.2 312.28,-375.28 311.24,-374.35 310.34,-373.41 309.58,-372.47 308.97,-371.53 308.53,-370.59 308.25,-369.65 308.14,-368.72 308.21,-367.8 308.45,-366.89 308.88,-365.99 309.5,-365.11 310.31,-364.25 311.3,-363.41 312.49,-362.59 313.86,-361.8 315.42,-361.04 317.17,-360.31 319.1,-359.61 321.2,-358.94 323.48,-358.31 325.92,-357.71 328.51,-357.16 331.25,-356.65 334.13,-356.18 337.14,-355.75 340.26,-355.36 343.49,-355.03 346.81,-354.74 350.2,-354.49 353.67,-354.3 357.18,-354.15 360.73,-354.05 364.31,-354 367.89,-354 371.46,-354.05\"/>\n",
+       "<text text-anchor=\"middle\" x=\"366.1\" y=\"-366.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(and3)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(or21),neg(and2)] -->\n",
+       "<g id=\"node26\" class=\"node\">\n",
+       "<title>[neg(or21),neg(and2)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"340.29,-265.55 346.38,-265.65 352.41,-265.8 358.34,-265.99 364.17,-266.24 369.86,-266.53 375.4,-266.86 380.75,-267.25 385.91,-267.68 390.84,-268.15 395.55,-268.66 399.99,-269.21 404.18,-269.81 408.08,-270.44 411.68,-271.11 414.99,-271.81 417.98,-272.54 420.66,-273.3 423.02,-274.09 425.05,-274.91 426.76,-275.75 428.14,-276.61 429.2,-277.49 429.94,-278.39 430.36,-279.3 430.48,-280.22 430.29,-281.15 429.81,-282.09 429.04,-283.03 428.01,-283.97 426.71,-284.91 425.16,-285.85 423.38,-286.78 421.37,-287.7 419.15,-288.61 416.73,-289.51 414.14,-290.39 411.37,-291.25 408.44,-292.09 405.37,-292.91 402.17,-293.7 398.85,-294.46 395.42,-295.19 391.9,-295.89 388.29,-296.56 384.61,-297.19 380.86,-297.79 377.05,-298.34 373.19,-298.85 369.29,-299.32 365.36,-299.75 361.39,-300.14 357.4,-300.47 353.38,-300.76 349.35,-301.01 345.31,-301.2 341.25,-301.35 337.19,-301.45 333.13,-301.5 329.06,-301.5 325,-301.45 320.94,-301.35 316.88,-301.2 312.84,-301.01 308.81,-300.76 304.8,-300.47 300.8,-300.14 296.83,-299.75 292.9,-299.32 289,-298.85 285.14,-298.34 281.33,-297.79 277.58,-297.19 273.9,-296.56 270.29,-295.89 266.77,-295.19 263.34,-294.46 260.02,-293.7 256.82,-292.91 253.75,-292.09 250.83,-291.25 248.06,-290.39 245.46,-289.51 243.04,-288.61 240.82,-287.7 238.82,-286.78 237.03,-285.85 235.48,-284.91 234.19,-283.97 233.15,-283.03 232.38,-282.09 231.9,-281.15 231.72,-280.22 231.83,-279.3 232.25,-278.39 232.99,-277.49 234.05,-276.61 235.43,-275.75 237.14,-274.91 239.17,-274.09 241.53,-273.3 244.21,-272.54 247.2,-271.81 250.51,-271.11 254.12,-270.44 258.02,-269.81 262.2,-269.21 266.65,-268.66 271.35,-268.15 276.28,-267.68 281.44,-267.25 286.79,-266.86 292.33,-266.53 298.02,-266.24 303.85,-265.99 309.79,-265.8 315.81,-265.65 321.9,-265.55 328.03,-265.5 334.17,-265.5 340.29,-265.55\"/>\n",
+       "<text text-anchor=\"middle\" x=\"331.1\" y=\"-278.45\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(or21),neg(and2)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(and3)]&#45;&gt;[neg(or21),neg(and2)] -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>[neg(and3)]&#45;&gt;[neg(or21),neg(and2)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M359.18,-353.91C354.37,-342.02 347.85,-325.91 342.3,-312.2\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"345.68,-311.21 338.68,-303.25 339.19,-313.84 345.68,-311.21\"/>\n",
+       "<text text-anchor=\"middle\" x=\"365.22\" y=\"-322.7\" font-family=\"Times,serif\" font-size=\"14.00\">and3</text>\n",
+       "</g>\n",
+       "<!-- [neg(and4),neg(or4)] -->\n",
+       "<g id=\"node7\" class=\"node\">\n",
+       "<title>[neg(and4),neg(or4)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"579.84,-973.55 585.63,-973.65 591.35,-973.8 597,-973.99 602.54,-974.24 607.95,-974.53 613.21,-974.86 618.3,-975.25 623.2,-975.68 627.9,-976.15 632.36,-976.66 636.59,-977.21 640.57,-977.81 644.28,-978.44 647.71,-979.11 650.85,-979.81 653.7,-980.54 656.24,-981.3 658.48,-982.09 660.42,-982.91 662.04,-983.75 663.35,-984.61 664.36,-985.49 665.06,-986.39 665.46,-987.3 665.57,-988.22 665.39,-989.15 664.93,-990.09 664.21,-991.03 663.22,-991.97 661.99,-992.91 660.52,-993.85 658.82,-994.78 656.91,-995.7 654.8,-996.61 652.51,-997.51 650.04,-998.39 647.4,-999.25 644.62,-1000.09 641.7,-1000.91 638.66,-1001.7 635.51,-1002.46 632.25,-1003.19 628.9,-1003.89 625.47,-1004.56 621.97,-1005.19 618.4,-1005.79 614.78,-1006.34 611.12,-1006.85 607.41,-1007.32 603.67,-1007.75 599.89,-1008.14 596.1,-1008.47 592.28,-1008.76 588.45,-1009.01 584.61,-1009.2 580.75,-1009.35 576.89,-1009.45 573.03,-1009.5 569.16,-1009.5 565.3,-1009.45 561.44,-1009.35 557.59,-1009.2 553.74,-1009.01 549.91,-1008.76 546.09,-1008.47 542.3,-1008.14 538.53,-1007.75 534.78,-1007.32 531.08,-1006.85 527.41,-1006.34 523.79,-1005.79 520.22,-1005.19 516.72,-1004.56 513.29,-1003.89 509.94,-1003.19 506.69,-1002.46 503.53,-1001.7 500.49,-1000.91 497.57,-1000.09 494.79,-999.25 492.16,-998.39 489.68,-997.51 487.39,-996.61 485.28,-995.7 483.37,-994.78 481.67,-993.85 480.2,-992.91 478.97,-991.97 477.98,-991.03 477.26,-990.09 476.8,-989.15 476.62,-988.22 476.73,-987.3 477.13,-986.39 477.83,-985.49 478.84,-984.61 480.15,-983.75 481.78,-982.91 483.71,-982.09 485.95,-981.3 488.5,-980.54 491.34,-979.81 494.49,-979.11 497.92,-978.44 501.62,-977.81 505.6,-977.21 509.83,-976.66 514.3,-976.15 518.99,-975.68 523.89,-975.25 528.98,-974.86 534.24,-974.53 539.65,-974.24 545.19,-973.99 550.84,-973.8 556.57,-973.65 562.35,-973.55 568.18,-973.5 574.01,-973.5 579.84,-973.55\"/>\n",
+       "<text text-anchor=\"middle\" x=\"571.1\" y=\"-986.45\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(and4),neg(or4)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(or3),neg(not2),neg(or4)] -->\n",
+       "<g id=\"node30\" class=\"node\">\n",
+       "<title>[neg(or3),neg(not2),neg(or4)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"583.07,-885.05 590.99,-885.15 598.83,-885.3 606.56,-885.49 614.15,-885.74 621.56,-886.03 628.76,-886.36 635.73,-886.75 642.44,-887.18 648.87,-887.65 654.99,-888.16 660.78,-888.71 666.22,-889.31 671.3,-889.94 675.99,-890.61 680.3,-891.31 684.19,-892.04 687.68,-892.8 690.75,-893.59 693.4,-894.41 695.62,-895.25 697.42,-896.11 698.79,-896.99 699.75,-897.89 700.3,-898.8 700.45,-899.72 700.21,-900.65 699.58,-901.59 698.59,-902.53 697.24,-903.47 695.55,-904.41 693.53,-905.35 691.21,-906.28 688.6,-907.2 685.71,-908.11 682.57,-909.01 679.18,-909.89 675.58,-910.75 671.77,-911.59 667.78,-912.41 663.61,-913.2 659.29,-913.96 654.83,-914.69 650.24,-915.39 645.55,-916.06 640.75,-916.69 635.87,-917.29 630.91,-917.84 625.89,-918.35 620.82,-918.82 615.69,-919.25 610.53,-919.64 605.33,-919.97 600.1,-920.26 594.86,-920.51 589.59,-920.7 584.32,-920.85 579.03,-920.95 573.74,-921 568.45,-921 563.16,-920.95 557.87,-920.85 552.6,-920.7 547.33,-920.51 542.09,-920.26 536.86,-919.97 531.66,-919.64 526.5,-919.25 521.38,-918.82 516.3,-918.35 511.28,-917.84 506.32,-917.29 501.44,-916.69 496.65,-916.06 491.95,-915.39 487.36,-914.69 482.9,-913.96 478.58,-913.2 474.42,-912.41 470.42,-911.59 466.61,-910.75 463.01,-909.89 459.62,-909.01 456.48,-908.11 453.59,-907.2 450.98,-906.28 448.66,-905.35 446.64,-904.41 444.95,-903.47 443.6,-902.53 442.61,-901.59 441.98,-900.65 441.74,-899.72 441.89,-898.8 442.44,-897.89 443.4,-896.99 444.78,-896.11 446.57,-895.25 448.8,-894.41 451.44,-893.59 454.51,-892.8 458,-892.04 461.9,-891.31 466.2,-890.61 470.9,-889.94 475.97,-889.31 481.41,-888.71 487.2,-888.16 493.32,-887.65 499.75,-887.18 506.46,-886.75 513.43,-886.36 520.64,-886.03 528.04,-885.74 535.63,-885.49 543.36,-885.3 551.2,-885.15 559.13,-885.05 567.1,-885 575.09,-885 583.07,-885.05\"/>\n",
+       "<text text-anchor=\"middle\" x=\"571.1\" y=\"-897.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(or3),neg(not2),neg(or4)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(and4),neg(or4)]&#45;&gt;[neg(or3),neg(not2),neg(or4)] -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>[neg(and4),neg(or4)]&#45;&gt;[neg(or3),neg(not2),neg(or4)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M571.1,-973.41C571.1,-961.76 571.1,-946.05 571.1,-932.52\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"574.6,-932.86 571.1,-922.86 567.6,-932.86 574.6,-932.86\"/>\n",
+       "<text text-anchor=\"middle\" x=\"584.22\" y=\"-942.2\" font-family=\"Times,serif\" font-size=\"14.00\">and4</text>\n",
+       "</g>\n",
+       "<!-- [neg(and5)] -->\n",
+       "<g id=\"node8\" class=\"node\">\n",
+       "<title>[neg(and5)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"576.46,-1062.05 580.01,-1062.15 583.52,-1062.3 586.99,-1062.49 590.38,-1062.74 593.7,-1063.03 596.93,-1063.36 600.05,-1063.75 603.06,-1064.18 605.94,-1064.65 608.68,-1065.16 611.28,-1065.71 613.71,-1066.31 615.99,-1066.94 618.09,-1067.61 620.02,-1068.31 621.77,-1069.04 623.33,-1069.8 624.7,-1070.59 625.89,-1071.41 626.89,-1072.25 627.69,-1073.11 628.31,-1073.99 628.74,-1074.89 628.99,-1075.8 629.05,-1076.72 628.94,-1077.65 628.66,-1078.59 628.22,-1079.53 627.61,-1080.47 626.85,-1081.41 625.95,-1082.35 624.91,-1083.28 623.74,-1084.2 622.45,-1085.11 621.04,-1086.01 619.52,-1086.89 617.91,-1087.75 616.2,-1088.59 614.41,-1089.41 612.54,-1090.2 610.61,-1090.96 608.61,-1091.69 606.56,-1092.39 604.45,-1093.06 602.3,-1093.69 600.12,-1094.29 597.9,-1094.84 595.65,-1095.35 593.37,-1095.82 591.08,-1096.25 588.76,-1096.64 586.43,-1096.97 584.09,-1097.26 581.74,-1097.51 579.38,-1097.7 577.02,-1097.85 574.65,-1097.95 572.28,-1098 569.91,-1098 567.54,-1097.95 565.17,-1097.85 562.81,-1097.7 560.45,-1097.51 558.1,-1097.26 555.76,-1096.97 553.43,-1096.64 551.12,-1096.25 548.82,-1095.82 546.54,-1095.35 544.29,-1094.84 542.07,-1094.29 539.89,-1093.69 537.74,-1093.06 535.64,-1092.39 533.58,-1091.69 531.58,-1090.96 529.65,-1090.2 527.78,-1089.41 525.99,-1088.59 524.28,-1087.75 522.67,-1086.89 521.15,-1086.01 519.74,-1085.11 518.45,-1084.2 517.28,-1083.28 516.24,-1082.35 515.34,-1081.41 514.58,-1080.47 513.97,-1079.53 513.53,-1078.59 513.25,-1077.65 513.14,-1076.72 513.21,-1075.8 513.45,-1074.89 513.88,-1073.99 514.5,-1073.11 515.31,-1072.25 516.3,-1071.41 517.49,-1070.59 518.86,-1069.8 520.42,-1069.04 522.17,-1068.31 524.1,-1067.61 526.2,-1066.94 528.48,-1066.31 530.92,-1065.71 533.51,-1065.16 536.25,-1064.65 539.13,-1064.18 542.14,-1063.75 545.26,-1063.36 548.49,-1063.03 551.81,-1062.74 555.2,-1062.49 558.67,-1062.3 562.18,-1062.15 565.73,-1062.05 569.31,-1062 572.89,-1062 576.46,-1062.05\"/>\n",
+       "<text text-anchor=\"middle\" x=\"571.1\" y=\"-1074.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(and5)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(and5)]&#45;&gt;[neg(and4),neg(or4)] -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>[neg(and5)]&#45;&gt;[neg(and4),neg(or4)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M571.1,-1061.91C571.1,-1050.26 571.1,-1034.55 571.1,-1021.02\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"574.6,-1021.36 571.1,-1011.36 567.6,-1021.36 574.6,-1021.36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"584.22\" y=\"-1030.7\" font-family=\"Times,serif\" font-size=\"14.00\">and5</text>\n",
+       "</g>\n",
+       "<!-- [neg(d)] -->\n",
+       "<g id=\"node12\" class=\"node\">\n",
+       "<title>[neg(d)]</title>\n",
+       "<ellipse fill=\"none\" stroke=\"red\" cx=\"624.1\" cy=\"-18\" rx=\"41.12\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"624.1\" y=\"-12.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(d)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(c),neg(d)]&#45;&gt;[neg(d)] -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>[neg(c),neg(d)]&#45;&gt;[neg(d)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M624.1,-88.41C624.1,-76.76 624.1,-61.05 624.1,-47.52\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"627.6,-47.86 624.1,-37.86 620.6,-47.86 627.6,-47.86\"/>\n",
+       "<text text-anchor=\"middle\" x=\"627.1\" y=\"-57.2\" font-family=\"Times,serif\" font-size=\"14.00\">c</text>\n",
+       "</g>\n",
+       "<!-- [neg(d),neg(not2),neg(or4)] -->\n",
+       "<g id=\"node13\" class=\"node\">\n",
+       "<title>[neg(d),neg(not2),neg(or4)]</title>\n",
+       "<ellipse fill=\"none\" stroke=\"red\" cx=\"709.1\" cy=\"-549\" rx=\"113.79\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"709.1\" y=\"-543.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(d),neg(not2),neg(or4)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(c),neg(d),neg(not2),neg(or4)]&#45;&gt;[neg(d),neg(not2),neg(or4)] -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>[neg(c),neg(d),neg(not2),neg(or4)]&#45;&gt;[neg(d),neg(not2),neg(or4)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M709.1,-619.41C709.1,-607.76 709.1,-592.05 709.1,-578.52\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"712.6,-578.86 709.1,-568.86 705.6,-578.86 712.6,-578.86\"/>\n",
+       "<text text-anchor=\"middle\" x=\"712.1\" y=\"-588.2\" font-family=\"Times,serif\" font-size=\"14.00\">c</text>\n",
+       "</g>\n",
+       "<!-- [neg(e)] -->\n",
+       "<g id=\"node14\" class=\"node\">\n",
+       "<title>[neg(e)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"509.1,-177.05 511.75,-177.15 514.37,-177.3 516.95,-177.49 519.49,-177.74 521.96,-178.03 524.37,-178.36 526.7,-178.75 528.94,-179.18 531.09,-179.65 533.14,-180.16 535.07,-180.71 536.89,-181.31 538.59,-181.94 540.16,-182.61 541.6,-183.31 542.9,-184.04 544.07,-184.8 545.09,-185.59 545.98,-186.41 546.72,-187.25 547.32,-188.11 547.78,-188.99 548.1,-189.89 548.29,-190.8 548.34,-191.72 548.25,-192.65 548.04,-193.59 547.71,-194.53 547.26,-195.47 546.7,-196.41 546.02,-197.35 545.25,-198.28 544.37,-199.2 543.41,-200.11 542.36,-201.01 541.23,-201.89 540.02,-202.75 538.75,-203.59 537.41,-204.41 536.02,-205.2 534.58,-205.96 533.08,-206.69 531.55,-207.39 529.98,-208.06 528.38,-208.69 526.75,-209.29 525.09,-209.84 523.41,-210.35 521.72,-210.82 520,-211.25 518.28,-211.64 516.54,-211.97 514.79,-212.26 513.04,-212.51 511.28,-212.7 509.52,-212.85 507.75,-212.95 505.98,-213 504.21,-213 502.44,-212.95 500.68,-212.85 498.91,-212.7 497.15,-212.51 495.4,-212.26 493.65,-211.97 491.92,-211.64 490.19,-211.25 488.48,-210.82 486.78,-210.35 485.1,-209.84 483.44,-209.29 481.81,-208.69 480.21,-208.06 478.64,-207.39 477.11,-206.69 475.62,-205.96 474.17,-205.2 472.78,-204.41 471.44,-203.59 470.17,-202.75 468.97,-201.89 467.83,-201.01 466.78,-200.11 465.82,-199.2 464.94,-198.28 464.17,-197.35 463.49,-196.41 462.93,-195.47 462.48,-194.53 462.15,-193.59 461.94,-192.65 461.86,-191.72 461.91,-190.8 462.09,-189.89 462.41,-188.99 462.87,-188.11 463.47,-187.25 464.21,-186.41 465.1,-185.59 466.12,-184.8 467.29,-184.04 468.59,-183.31 470.03,-182.61 471.6,-181.94 473.3,-181.31 475.12,-180.71 477.05,-180.16 479.1,-179.65 481.25,-179.18 483.49,-178.75 485.82,-178.36 488.23,-178.03 490.7,-177.74 493.24,-177.49 495.82,-177.3 498.45,-177.15 501.09,-177.05 503.76,-177 506.43,-177 509.1,-177.05\"/>\n",
+       "<text text-anchor=\"middle\" x=\"505.1\" y=\"-189.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(e)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(e)]&#45;&gt;[] -->\n",
+       "<g id=\"edge10\" class=\"edge\">\n",
+       "<title>[neg(e)]&#45;&gt;[]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M505.1,-176.91C505.1,-165.26 505.1,-149.55 505.1,-136.02\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"508.6,-136.36 505.1,-126.36 501.6,-136.36 508.6,-136.36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"508.1\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">e</text>\n",
+       "</g>\n",
+       "<!-- [neg(e),neg(not2),neg(or4)] -->\n",
+       "<g id=\"node15\" class=\"node\">\n",
+       "<title>[neg(e),neg(not2),neg(or4)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"440.26,-708.05 447.65,-708.15 454.96,-708.3 462.17,-708.49 469.25,-708.74 476.15,-709.03 482.87,-709.36 489.37,-709.75 495.63,-710.18 501.62,-710.65 507.33,-711.16 512.73,-711.71 517.81,-712.31 522.54,-712.94 526.92,-713.61 530.93,-714.31 534.57,-715.04 537.82,-715.8 540.68,-716.59 543.15,-717.41 545.22,-718.25 546.9,-719.11 548.18,-719.99 549.08,-720.89 549.59,-721.8 549.73,-722.72 549.5,-723.65 548.92,-724.59 547.99,-725.53 546.73,-726.47 545.16,-727.41 543.28,-728.35 541.11,-729.28 538.68,-730.2 535.98,-731.11 533.05,-732.01 529.9,-732.89 526.54,-733.75 522.98,-734.59 519.26,-735.41 515.37,-736.2 511.34,-736.96 507.18,-737.69 502.91,-738.39 498.53,-739.06 494.06,-739.69 489.5,-740.29 484.88,-740.84 480.2,-741.35 475.46,-741.82 470.68,-742.25 465.87,-742.64 461.02,-742.97 456.15,-743.26 451.26,-743.51 446.35,-743.7 441.43,-743.85 436.5,-743.95 431.56,-744 426.63,-744 421.69,-743.95 416.77,-743.85 411.84,-743.7 406.94,-743.51 402.04,-743.26 397.17,-742.97 392.32,-742.64 387.51,-742.25 382.73,-741.82 377.99,-741.35 373.31,-740.84 368.69,-740.29 364.14,-739.69 359.66,-739.06 355.28,-738.39 351.01,-737.69 346.85,-736.96 342.82,-736.2 338.93,-735.41 335.21,-734.59 331.66,-733.75 328.29,-732.89 325.14,-732.01 322.21,-731.11 319.51,-730.2 317.08,-729.28 314.91,-728.35 313.03,-727.41 311.46,-726.47 310.2,-725.53 309.27,-724.59 308.69,-723.65 308.46,-722.72 308.6,-721.8 309.11,-720.89 310.01,-719.99 311.29,-719.11 312.97,-718.25 315.04,-717.41 317.51,-716.59 320.37,-715.8 323.62,-715.04 327.26,-714.31 331.27,-713.61 335.65,-712.94 340.39,-712.31 345.46,-711.71 350.86,-711.16 356.57,-710.65 362.56,-710.18 368.82,-709.75 375.32,-709.36 382.04,-709.03 388.95,-708.74 396.02,-708.49 403.23,-708.3 410.54,-708.15 417.93,-708.05 425.37,-708 432.82,-708 440.26,-708.05\"/>\n",
+       "<text text-anchor=\"middle\" x=\"429.1\" y=\"-720.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(e),neg(not2),neg(or4)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(not2),neg(or4)] -->\n",
+       "<g id=\"node22\" class=\"node\">\n",
+       "<title>[neg(not2),neg(or4)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"437.69,-619.55 443.37,-619.65 449,-619.8 454.55,-619.99 459.99,-620.24 465.31,-620.53 470.48,-620.86 475.48,-621.25 480.3,-621.68 484.91,-622.15 489.3,-622.66 493.46,-623.21 497.37,-623.81 501.01,-624.44 504.38,-625.11 507.47,-625.81 510.27,-626.54 512.77,-627.3 514.97,-628.09 516.87,-628.91 518.46,-629.75 519.76,-630.61 520.74,-631.49 521.43,-632.39 521.83,-633.3 521.93,-634.22 521.76,-635.15 521.31,-636.09 520.6,-637.03 519.63,-637.97 518.42,-638.91 516.97,-639.85 515.3,-640.78 513.43,-641.7 511.35,-642.61 509.1,-643.51 506.67,-644.39 504.08,-645.25 501.35,-646.09 498.48,-646.91 495.49,-647.7 492.39,-648.46 489.19,-649.19 485.9,-649.89 482.53,-650.56 479.09,-651.19 475.58,-651.79 472.03,-652.34 468.42,-652.85 464.78,-653.32 461.1,-653.75 457.4,-654.14 453.67,-654.47 449.92,-654.76 446.15,-655.01 442.37,-655.2 438.59,-655.35 434.79,-655.45 430.99,-655.5 427.2,-655.5 423.4,-655.45 419.61,-655.35 415.82,-655.2 412.04,-655.01 408.28,-654.76 404.53,-654.47 400.8,-654.14 397.09,-653.75 393.41,-653.32 389.77,-652.85 386.16,-652.34 382.61,-651.79 379.1,-651.19 375.66,-650.56 372.29,-649.89 369,-649.19 365.8,-648.46 362.7,-647.7 359.71,-646.91 356.84,-646.09 354.11,-645.25 351.52,-644.39 349.09,-643.51 346.84,-642.61 344.76,-641.7 342.89,-640.78 341.22,-639.85 339.78,-638.91 338.56,-637.97 337.59,-637.03 336.88,-636.09 336.43,-635.15 336.26,-634.22 336.36,-633.3 336.76,-632.39 337.45,-631.49 338.44,-630.61 339.73,-629.75 341.32,-628.91 343.22,-628.09 345.42,-627.3 347.93,-626.54 350.72,-625.81 353.81,-625.11 357.18,-624.44 360.83,-623.81 364.73,-623.21 368.89,-622.66 373.28,-622.15 377.89,-621.68 382.71,-621.25 387.71,-620.86 392.88,-620.53 398.2,-620.24 403.64,-619.99 409.19,-619.8 414.82,-619.65 420.5,-619.55 426.23,-619.5 431.96,-619.5 437.69,-619.55\"/>\n",
+       "<text text-anchor=\"middle\" x=\"429.1\" y=\"-632.45\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(not2),neg(or4)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(e),neg(not2),neg(or4)]&#45;&gt;[neg(not2),neg(or4)] -->\n",
+       "<g id=\"edge11\" class=\"edge\">\n",
+       "<title>[neg(e),neg(not2),neg(or4)]&#45;&gt;[neg(not2),neg(or4)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M429.1,-707.91C429.1,-696.26 429.1,-680.55 429.1,-667.02\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"432.6,-667.36 429.1,-657.36 425.6,-667.36 432.6,-667.36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"432.1\" y=\"-676.7\" font-family=\"Times,serif\" font-size=\"14.00\">e</text>\n",
+       "</g>\n",
+       "<!-- [neg(e),neg(or4)] -->\n",
+       "<g id=\"node16\" class=\"node\">\n",
+       "<title>[neg(e),neg(or4)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"436.48,-531.05 441.36,-531.15 446.2,-531.3 450.96,-531.49 455.64,-531.74 460.21,-532.03 464.65,-532.36 468.95,-532.75 473.09,-533.18 477.05,-533.65 480.82,-534.16 484.39,-534.71 487.75,-535.31 490.88,-535.94 493.77,-536.61 496.43,-537.31 498.83,-538.04 500.98,-538.8 502.87,-539.59 504.5,-540.41 505.87,-541.25 506.98,-542.11 507.83,-542.99 508.42,-543.89 508.76,-544.8 508.85,-545.72 508.7,-546.65 508.32,-547.59 507.7,-548.53 506.87,-549.47 505.83,-550.41 504.59,-551.35 503.16,-552.28 501.54,-553.2 499.76,-554.11 497.83,-555.01 495.74,-555.89 493.52,-556.75 491.17,-557.59 488.71,-558.41 486.14,-559.2 483.47,-559.96 480.72,-560.69 477.9,-561.39 475,-562.06 472.04,-562.69 469.03,-563.29 465.98,-563.84 462.88,-564.35 459.75,-564.82 456.59,-565.25 453.41,-565.64 450.2,-565.97 446.98,-566.26 443.75,-566.51 440.5,-566.7 437.25,-566.85 433.99,-566.95 430.73,-567 427.46,-567 424.2,-566.95 420.94,-566.85 417.69,-566.7 414.44,-566.51 411.21,-566.26 407.99,-565.97 404.78,-565.64 401.6,-565.25 398.44,-564.82 395.31,-564.35 392.21,-563.84 389.16,-563.29 386.15,-562.69 383.19,-562.06 380.3,-561.39 377.47,-560.69 374.72,-559.96 372.05,-559.2 369.49,-558.41 367.02,-557.59 364.67,-556.75 362.45,-555.89 360.37,-555.01 358.43,-554.11 356.65,-553.2 355.04,-552.28 353.6,-551.35 352.36,-550.41 351.32,-549.47 350.49,-548.53 349.87,-547.59 349.49,-546.65 349.34,-545.72 349.43,-544.8 349.77,-543.89 350.36,-542.99 351.21,-542.11 352.32,-541.25 353.69,-540.41 355.32,-539.59 357.21,-538.8 359.36,-538.04 361.77,-537.31 364.42,-536.61 367.31,-535.94 370.45,-535.31 373.8,-534.71 377.37,-534.16 381.14,-533.65 385.11,-533.18 389.24,-532.75 393.54,-532.36 397.98,-532.03 402.55,-531.74 407.23,-531.49 411.99,-531.3 416.83,-531.15 421.72,-531.05 426.63,-531 431.56,-531 436.48,-531.05\"/>\n",
+       "<text text-anchor=\"middle\" x=\"429.1\" y=\"-543.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(e),neg(or4)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(or4)] -->\n",
+       "<g id=\"node31\" class=\"node\">\n",
+       "<title>[neg(or4)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"433.9,-442.55 437.09,-442.65 440.24,-442.8 443.34,-442.99 446.39,-443.24 449.37,-443.53 452.26,-443.86 455.06,-444.25 457.75,-444.68 460.34,-445.15 462.79,-445.66 465.12,-446.21 467.31,-446.81 469.34,-447.44 471.23,-448.11 472.96,-448.81 474.53,-449.54 475.93,-450.3 477.16,-451.09 478.22,-451.91 479.11,-452.75 479.84,-453.61 480.39,-454.49 480.78,-455.39 481,-456.3 481.06,-457.22 480.96,-458.15 480.71,-459.09 480.31,-460.03 479.77,-460.97 479.09,-461.91 478.28,-462.85 477.34,-463.78 476.29,-464.7 475.13,-465.61 473.87,-466.51 472.51,-467.39 471.07,-468.25 469.54,-469.09 467.93,-469.91 466.26,-470.7 464.52,-471.46 462.73,-472.19 460.89,-472.89 459,-473.56 457.08,-474.19 455.11,-474.79 453.12,-475.34 451.11,-475.85 449.07,-476.32 447.01,-476.75 444.93,-477.14 442.85,-477.47 440.75,-477.76 438.64,-478.01 436.53,-478.2 434.41,-478.35 432.28,-478.45 430.16,-478.5 428.03,-478.5 425.91,-478.45 423.78,-478.35 421.67,-478.2 419.55,-478.01 417.44,-477.76 415.34,-477.47 413.26,-477.14 411.18,-476.75 409.12,-476.32 407.08,-475.85 405.07,-475.34 403.08,-474.79 401.12,-474.19 399.19,-473.56 397.3,-472.89 395.46,-472.19 393.67,-471.46 391.93,-470.7 390.26,-469.91 388.66,-469.09 387.13,-468.25 385.68,-467.39 384.32,-466.51 383.06,-465.61 381.9,-464.7 380.85,-463.78 379.91,-462.85 379.1,-461.91 378.43,-460.97 377.88,-460.03 377.48,-459.09 377.23,-458.15 377.13,-457.22 377.19,-456.3 377.42,-455.39 377.8,-454.49 378.35,-453.61 379.08,-452.75 379.97,-451.91 381.03,-451.09 382.26,-450.3 383.67,-449.54 385.23,-448.81 386.96,-448.11 388.85,-447.44 390.89,-446.81 393.07,-446.21 395.4,-445.66 397.86,-445.15 400.44,-444.68 403.13,-444.25 405.93,-443.86 408.83,-443.53 411.8,-443.24 414.85,-442.99 417.95,-442.8 421.1,-442.65 424.29,-442.55 427.49,-442.5 430.7,-442.5 433.9,-442.55\"/>\n",
+       "<text text-anchor=\"middle\" x=\"429.1\" y=\"-455.45\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(or4)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(e),neg(or4)]&#45;&gt;[neg(or4)] -->\n",
+       "<g id=\"edge12\" class=\"edge\">\n",
+       "<title>[neg(e),neg(or4)]&#45;&gt;[neg(or4)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M429.1,-530.91C429.1,-519.26 429.1,-503.55 429.1,-490.02\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"432.6,-490.36 429.1,-480.36 425.6,-490.36 432.6,-490.36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"432.1\" y=\"-499.7\" font-family=\"Times,serif\" font-size=\"14.00\">e</text>\n",
+       "</g>\n",
+       "<!-- [neg(not1)] -->\n",
+       "<g id=\"node17\" class=\"node\">\n",
+       "<title>[neg(not1)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"775.31,-177.05 778.76,-177.15 782.17,-177.3 785.54,-177.49 788.84,-177.74 792.07,-178.03 795.2,-178.36 798.24,-178.75 801.16,-179.18 803.96,-179.65 806.62,-180.16 809.14,-180.71 811.51,-181.31 813.72,-181.94 815.77,-182.61 817.64,-183.31 819.34,-184.04 820.86,-184.8 822.19,-185.59 823.34,-186.41 824.31,-187.25 825.09,-188.11 825.69,-188.99 826.11,-189.89 826.35,-190.8 826.42,-191.72 826.31,-192.65 826.04,-193.59 825.6,-194.53 825.02,-195.47 824.28,-196.41 823.4,-197.35 822.39,-198.28 821.26,-199.2 820,-200.11 818.63,-201.01 817.16,-201.89 815.59,-202.75 813.93,-203.59 812.19,-204.41 810.38,-205.2 808.49,-205.96 806.55,-206.69 804.56,-207.39 802.51,-208.06 800.42,-208.69 798.3,-209.29 796.14,-209.84 793.95,-210.35 791.74,-210.82 789.51,-211.25 787.26,-211.64 785,-211.97 782.73,-212.26 780.44,-212.51 778.15,-212.7 775.85,-212.85 773.55,-212.95 771.25,-213 768.94,-213 766.64,-212.95 764.34,-212.85 762.04,-212.7 759.75,-212.51 757.47,-212.26 755.19,-211.97 752.93,-211.64 750.68,-211.25 748.45,-210.82 746.24,-210.35 744.05,-209.84 741.89,-209.29 739.77,-208.69 737.68,-208.06 735.64,-207.39 733.64,-206.69 731.7,-205.96 729.82,-205.2 728,-204.41 726.26,-203.59 724.6,-202.75 723.04,-201.89 721.56,-201.01 720.19,-200.11 718.94,-199.2 717.8,-198.28 716.79,-197.35 715.91,-196.41 715.17,-195.47 714.59,-194.53 714.15,-193.59 713.88,-192.65 713.77,-191.72 713.84,-190.8 714.08,-189.89 714.5,-188.99 715.1,-188.11 715.88,-187.25 716.85,-186.41 718,-185.59 719.34,-184.8 720.85,-184.04 722.55,-183.31 724.42,-182.61 726.47,-181.94 728.68,-181.31 731.05,-180.71 733.57,-180.16 736.23,-179.65 739.03,-179.18 741.95,-178.75 744.99,-178.36 748.13,-178.03 751.35,-177.74 754.65,-177.49 758.02,-177.3 761.43,-177.15 764.88,-177.05 768.36,-177 771.84,-177 775.31,-177.05\"/>\n",
+       "<text text-anchor=\"middle\" x=\"770.1\" y=\"-189.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(not1)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(not_e)] -->\n",
+       "<g id=\"node23\" class=\"node\">\n",
+       "<title>[neg(not_e)]</title>\n",
+       "<ellipse fill=\"none\" stroke=\"red\" cx=\"771.1\" cy=\"-106.5\" rx=\"56.98\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"771.1\" y=\"-101.45\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(not_e)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(not1)]&#45;&gt;[neg(not_e)] -->\n",
+       "<g id=\"edge13\" class=\"edge\">\n",
+       "<title>[neg(not1)]&#45;&gt;[neg(not_e)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M770.29,-176.91C770.43,-165.26 770.61,-149.55 770.77,-136.02\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"774.26,-136.4 770.88,-126.36 767.26,-136.32 774.26,-136.4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"782.1\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">not1</text>\n",
+       "</g>\n",
+       "<!-- [neg(not1),neg(and2)] -->\n",
+       "<g id=\"node18\" class=\"node\">\n",
+       "<title>[neg(not1),neg(and2)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"351.24,-177.05 357.3,-177.15 363.29,-177.3 369.2,-177.49 374.99,-177.74 380.65,-178.03 386.15,-178.36 391.48,-178.75 396.61,-179.18 401.52,-179.65 406.19,-180.16 410.62,-180.71 414.77,-181.31 418.65,-181.94 422.24,-182.61 425.53,-183.31 428.51,-184.04 431.17,-184.8 433.52,-185.59 435.54,-186.41 437.24,-187.25 438.61,-188.11 439.66,-188.99 440.4,-189.89 440.82,-190.8 440.93,-191.72 440.74,-192.65 440.27,-193.59 439.51,-194.53 438.47,-195.47 437.18,-196.41 435.64,-197.35 433.87,-198.28 431.87,-199.2 429.67,-200.11 427.26,-201.01 424.68,-201.89 421.93,-202.75 419.02,-203.59 415.96,-204.41 412.78,-205.2 409.48,-205.96 406.07,-206.69 402.57,-207.39 398.98,-208.06 395.32,-208.69 391.59,-209.29 387.8,-209.84 383.96,-210.35 380.08,-210.82 376.17,-211.25 372.22,-211.64 368.25,-211.97 364.26,-212.26 360.25,-212.51 356.23,-212.7 352.2,-212.85 348.16,-212.95 344.12,-213 340.07,-213 336.03,-212.95 331.99,-212.85 327.96,-212.7 323.94,-212.51 319.93,-212.26 315.94,-211.97 311.97,-211.64 308.02,-211.25 304.11,-210.82 300.23,-210.35 296.39,-209.84 292.6,-209.29 288.88,-208.69 285.21,-208.06 281.62,-207.39 278.12,-206.69 274.71,-205.96 271.41,-205.2 268.23,-204.41 265.18,-203.59 262.27,-202.75 259.51,-201.89 256.93,-201.01 254.52,-200.11 252.32,-199.2 250.32,-198.28 248.55,-197.35 247.01,-196.41 245.72,-195.47 244.69,-194.53 243.93,-193.59 243.45,-192.65 243.26,-191.72 243.37,-190.8 243.79,-189.89 244.53,-188.99 245.58,-188.11 246.96,-187.25 248.65,-186.41 250.67,-185.59 253.02,-184.8 255.68,-184.04 258.66,-183.31 261.95,-182.61 265.54,-181.94 269.42,-181.31 273.58,-180.71 278,-180.16 282.67,-179.65 287.58,-179.18 292.71,-178.75 298.04,-178.36 303.54,-178.03 309.2,-177.74 315,-177.49 320.9,-177.3 326.89,-177.15 332.95,-177.05 339.04,-177 345.15,-177 351.24,-177.05\"/>\n",
+       "<text text-anchor=\"middle\" x=\"342.1\" y=\"-189.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(not1),neg(and2)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(not_e),neg(and2)] -->\n",
+       "<g id=\"node24\" class=\"node\">\n",
+       "<title>[neg(not_e),neg(and2)]</title>\n",
+       "<ellipse fill=\"none\" stroke=\"red\" cx=\"343.1\" cy=\"-106.5\" rx=\"96.9\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"343.1\" y=\"-101.45\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(not_e),neg(and2)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(not1),neg(and2)]&#45;&gt;[neg(not_e),neg(and2)] -->\n",
+       "<g id=\"edge14\" class=\"edge\">\n",
+       "<title>[neg(not1),neg(and2)]&#45;&gt;[neg(not_e),neg(and2)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M342.29,-176.91C342.43,-165.26 342.61,-149.55 342.77,-136.02\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"346.26,-136.4 342.88,-126.36 339.26,-136.32 346.26,-136.4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"355.1\" y=\"-145.7\" font-family=\"Times,serif\" font-size=\"14.00\">not1</text>\n",
+       "</g>\n",
+       "<!-- [neg(not1),neg(not2),neg(or4)] -->\n",
+       "<g id=\"node19\" class=\"node\">\n",
+       "<title>[neg(not1),neg(not2),neg(or4)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"1017.47,-708.05 1025.66,-708.15 1033.77,-708.3 1041.76,-708.49 1049.6,-708.74 1057.26,-709.03 1064.7,-709.36 1071.91,-709.75 1078.85,-710.18 1085.49,-710.65 1091.81,-711.16 1097.8,-711.71 1103.43,-712.31 1108.67,-712.94 1113.53,-713.61 1117.98,-714.31 1122.01,-715.04 1125.61,-715.8 1128.78,-716.59 1131.52,-717.41 1133.82,-718.25 1135.67,-719.11 1137.1,-719.99 1138.09,-720.89 1138.66,-721.8 1138.81,-722.72 1138.56,-723.65 1137.91,-724.59 1136.89,-725.53 1135.49,-726.47 1133.74,-727.41 1131.66,-728.35 1129.26,-729.28 1126.56,-730.2 1123.57,-731.11 1120.32,-732.01 1116.83,-732.89 1113.1,-733.75 1109.16,-734.59 1105.03,-735.41 1100.73,-736.2 1096.26,-736.96 1091.65,-737.69 1086.91,-738.39 1082.06,-739.06 1077.1,-739.69 1072.05,-740.29 1066.93,-740.84 1061.74,-741.35 1056.49,-741.82 1051.19,-742.25 1045.86,-742.64 1040.48,-742.97 1035.08,-743.26 1029.66,-743.51 1024.22,-743.7 1018.76,-743.85 1013.3,-743.95 1007.83,-744 1002.36,-744 996.89,-743.95 991.43,-743.85 985.97,-743.7 980.53,-743.51 975.11,-743.26 969.71,-742.97 964.34,-742.64 959,-742.25 953.7,-741.82 948.45,-741.35 943.26,-740.84 938.14,-740.29 933.09,-739.69 928.14,-739.06 923.28,-738.39 918.54,-737.69 913.93,-736.96 909.46,-736.2 905.16,-735.41 901.03,-734.59 897.09,-733.75 893.36,-732.89 889.87,-732.01 886.62,-731.11 883.63,-730.2 880.93,-729.28 878.53,-728.35 876.45,-727.41 874.7,-726.47 873.31,-725.53 872.28,-724.59 871.63,-723.65 871.38,-722.72 871.53,-721.8 872.1,-720.89 873.09,-719.99 874.52,-719.11 876.38,-718.25 878.67,-717.41 881.41,-716.59 884.58,-715.8 888.18,-715.04 892.22,-714.31 896.66,-713.61 901.52,-712.94 906.77,-712.31 912.39,-711.71 918.38,-711.16 924.7,-710.65 931.35,-710.18 938.28,-709.75 945.49,-709.36 952.93,-709.03 960.59,-708.74 968.43,-708.49 976.42,-708.3 984.53,-708.15 992.72,-708.05 1000.97,-708 1009.23,-708 1017.47,-708.05\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1005.1\" y=\"-720.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(not1),neg(not2),neg(or4)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(not_e),neg(not2),neg(or4)] -->\n",
+       "<g id=\"node25\" class=\"node\">\n",
+       "<title>[neg(not_e),neg(not2),neg(or4)]</title>\n",
+       "<ellipse fill=\"none\" stroke=\"red\" cx=\"1006.1\" cy=\"-637.5\" rx=\"129.66\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1006.1\" y=\"-632.45\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(not_e),neg(not2),neg(or4)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(not1),neg(not2),neg(or4)]&#45;&gt;[neg(not_e),neg(not2),neg(or4)] -->\n",
+       "<g id=\"edge15\" class=\"edge\">\n",
+       "<title>[neg(not1),neg(not2),neg(or4)]&#45;&gt;[neg(not_e),neg(not2),neg(or4)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1005.29,-707.91C1005.43,-696.26 1005.61,-680.55 1005.77,-667.02\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"1009.26,-667.4 1005.88,-657.36 1002.26,-667.32 1009.26,-667.4\"/>\n",
+       "<text text-anchor=\"middle\" x=\"1017.1\" y=\"-676.7\" font-family=\"Times,serif\" font-size=\"14.00\">not1</text>\n",
+       "</g>\n",
+       "<!-- [neg(not2)] -->\n",
+       "<g id=\"node20\" class=\"node\">\n",
+       "<title>[neg(not2)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"510.31,-265.55 513.76,-265.65 517.17,-265.8 520.54,-265.99 523.84,-266.24 527.07,-266.53 530.2,-266.86 533.24,-267.25 536.16,-267.68 538.96,-268.15 541.62,-268.66 544.14,-269.21 546.51,-269.81 548.72,-270.44 550.77,-271.11 552.64,-271.81 554.34,-272.54 555.86,-273.3 557.19,-274.09 558.34,-274.91 559.31,-275.75 560.09,-276.61 560.69,-277.49 561.11,-278.39 561.35,-279.3 561.42,-280.22 561.31,-281.15 561.04,-282.09 560.6,-283.03 560.02,-283.97 559.28,-284.91 558.4,-285.85 557.39,-286.78 556.26,-287.7 555,-288.61 553.63,-289.51 552.16,-290.39 550.59,-291.25 548.93,-292.09 547.19,-292.91 545.38,-293.7 543.49,-294.46 541.55,-295.19 539.56,-295.89 537.51,-296.56 535.42,-297.19 533.3,-297.79 531.14,-298.34 528.95,-298.85 526.74,-299.32 524.51,-299.75 522.26,-300.14 520,-300.47 517.73,-300.76 515.44,-301.01 513.15,-301.2 510.85,-301.35 508.55,-301.45 506.25,-301.5 503.94,-301.5 501.64,-301.45 499.34,-301.35 497.04,-301.2 494.75,-301.01 492.47,-300.76 490.19,-300.47 487.93,-300.14 485.68,-299.75 483.45,-299.32 481.24,-298.85 479.05,-298.34 476.89,-297.79 474.77,-297.19 472.68,-296.56 470.64,-295.89 468.64,-295.19 466.7,-294.46 464.82,-293.7 463,-292.91 461.26,-292.09 459.6,-291.25 458.04,-290.39 456.56,-289.51 455.19,-288.61 453.94,-287.7 452.8,-286.78 451.79,-285.85 450.91,-284.91 450.17,-283.97 449.59,-283.03 449.15,-282.09 448.88,-281.15 448.77,-280.22 448.84,-279.3 449.08,-278.39 449.5,-277.49 450.1,-276.61 450.88,-275.75 451.85,-274.91 453,-274.09 454.34,-273.3 455.85,-272.54 457.55,-271.81 459.42,-271.11 461.47,-270.44 463.68,-269.81 466.05,-269.21 468.57,-268.66 471.23,-268.15 474.03,-267.68 476.95,-267.25 479.99,-266.86 483.13,-266.53 486.35,-266.24 489.65,-265.99 493.02,-265.8 496.43,-265.65 499.88,-265.55 503.36,-265.5 506.84,-265.5 510.31,-265.55\"/>\n",
+       "<text text-anchor=\"middle\" x=\"505.1\" y=\"-278.45\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(not2)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(not2)]&#45;&gt;[neg(e)] -->\n",
+       "<g id=\"edge16\" class=\"edge\">\n",
+       "<title>[neg(not2)]&#45;&gt;[neg(e)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M505.1,-265.41C505.1,-253.76 505.1,-238.05 505.1,-224.52\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"508.6,-224.86 505.1,-214.86 501.6,-224.86 508.6,-224.86\"/>\n",
+       "<text text-anchor=\"middle\" x=\"517.1\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">not2</text>\n",
+       "</g>\n",
+       "<!-- [neg(not2),neg(not2),neg(or4)] -->\n",
+       "<g id=\"node21\" class=\"node\">\n",
+       "<title>[neg(not2),neg(not2),neg(or4)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"441.47,-796.55 449.66,-796.65 457.77,-796.8 465.76,-796.99 473.6,-797.24 481.26,-797.53 488.7,-797.86 495.91,-798.25 502.85,-798.68 509.49,-799.15 515.81,-799.66 521.8,-800.21 527.43,-800.81 532.67,-801.44 537.53,-802.11 541.98,-802.81 546.01,-803.54 549.61,-804.3 552.78,-805.09 555.52,-805.91 557.82,-806.75 559.67,-807.61 561.1,-808.49 562.09,-809.39 562.66,-810.3 562.81,-811.22 562.56,-812.15 561.91,-813.09 560.89,-814.03 559.49,-814.97 557.74,-815.91 555.66,-816.85 553.26,-817.78 550.56,-818.7 547.57,-819.61 544.32,-820.51 540.83,-821.39 537.1,-822.25 533.16,-823.09 529.03,-823.91 524.73,-824.7 520.26,-825.46 515.65,-826.19 510.91,-826.89 506.06,-827.56 501.1,-828.19 496.05,-828.79 490.93,-829.34 485.74,-829.85 480.49,-830.32 475.19,-830.75 469.86,-831.14 464.48,-831.47 459.08,-831.76 453.66,-832.01 448.22,-832.2 442.76,-832.35 437.3,-832.45 431.83,-832.5 426.36,-832.5 420.89,-832.45 415.43,-832.35 409.97,-832.2 404.53,-832.01 399.11,-831.76 393.71,-831.47 388.34,-831.14 383,-830.75 377.7,-830.32 372.45,-829.85 367.26,-829.34 362.14,-828.79 357.09,-828.19 352.14,-827.56 347.28,-826.89 342.54,-826.19 337.93,-825.46 333.46,-824.7 329.16,-823.91 325.03,-823.09 321.09,-822.25 317.36,-821.39 313.87,-820.51 310.62,-819.61 307.63,-818.7 304.93,-817.78 302.53,-816.85 300.45,-815.91 298.7,-814.97 297.31,-814.03 296.28,-813.09 295.63,-812.15 295.38,-811.22 295.53,-810.3 296.1,-809.39 297.09,-808.49 298.52,-807.61 300.38,-806.75 302.67,-805.91 305.41,-805.09 308.58,-804.3 312.18,-803.54 316.22,-802.81 320.66,-802.11 325.52,-801.44 330.77,-800.81 336.39,-800.21 342.38,-799.66 348.7,-799.15 355.35,-798.68 362.28,-798.25 369.49,-797.86 376.93,-797.53 384.59,-797.24 392.43,-796.99 400.42,-796.8 408.53,-796.65 416.72,-796.55 424.97,-796.5 433.23,-796.5 441.47,-796.55\"/>\n",
+       "<text text-anchor=\"middle\" x=\"429.1\" y=\"-809.45\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(not2),neg(not2),neg(or4)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(not2),neg(not2),neg(or4)]&#45;&gt;[neg(e),neg(not2),neg(or4)] -->\n",
+       "<g id=\"edge17\" class=\"edge\">\n",
+       "<title>[neg(not2),neg(not2),neg(or4)]&#45;&gt;[neg(e),neg(not2),neg(or4)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M429.1,-796.41C429.1,-784.76 429.1,-769.05 429.1,-755.52\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"432.6,-755.86 429.1,-745.86 425.6,-755.86 432.6,-755.86\"/>\n",
+       "<text text-anchor=\"middle\" x=\"441.1\" y=\"-765.2\" font-family=\"Times,serif\" font-size=\"14.00\">not2</text>\n",
+       "</g>\n",
+       "<!-- [neg(not2),neg(or4)]&#45;&gt;[neg(e),neg(or4)] -->\n",
+       "<g id=\"edge18\" class=\"edge\">\n",
+       "<title>[neg(not2),neg(or4)]&#45;&gt;[neg(e),neg(or4)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M429.1,-619.41C429.1,-607.76 429.1,-592.05 429.1,-578.52\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"432.6,-578.86 429.1,-568.86 425.6,-578.86 432.6,-578.86\"/>\n",
+       "<text text-anchor=\"middle\" x=\"441.1\" y=\"-588.2\" font-family=\"Times,serif\" font-size=\"14.00\">not2</text>\n",
+       "</g>\n",
+       "<!-- [neg(or21),neg(and2)]&#45;&gt;[neg(and11),neg(and2)] -->\n",
+       "<g id=\"edge19\" class=\"edge\">\n",
+       "<title>[neg(or21),neg(and2)]&#45;&gt;[neg(and11),neg(and2)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M291.22,-266.23C256.18,-251.93 205.08,-231.08 167.66,-215.82\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"168.99,-212.58 158.41,-212.04 166.35,-219.06 168.99,-212.58\"/>\n",
+       "<text text-anchor=\"middle\" x=\"256.47\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">or21</text>\n",
+       "</g>\n",
+       "<!-- [neg(or21),neg(and2)]&#45;&gt;[neg(not1),neg(and2)] -->\n",
+       "<g id=\"edge20\" class=\"edge\">\n",
+       "<title>[neg(or21),neg(and2)]&#45;&gt;[neg(not1),neg(and2)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M333.27,-265.41C334.75,-253.76 336.75,-238.05 338.47,-224.52\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"341.91,-225.21 339.7,-214.85 334.96,-224.33 341.91,-225.21\"/>\n",
+       "<text text-anchor=\"middle\" x=\"350.47\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">or21</text>\n",
+       "</g>\n",
+       "<!-- [neg(or22)] -->\n",
+       "<g id=\"node27\" class=\"node\">\n",
+       "<title>[neg(or22)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"641.36,-265.55 644.84,-265.65 648.29,-265.8 651.69,-265.99 655.02,-266.24 658.28,-266.53 661.45,-266.86 664.51,-267.25 667.46,-267.68 670.28,-268.15 672.97,-268.66 675.52,-269.21 677.91,-269.81 680.14,-270.44 682.21,-271.11 684.1,-271.81 685.81,-272.54 687.35,-273.3 688.7,-274.09 689.86,-274.91 690.84,-275.75 691.63,-276.61 692.23,-277.49 692.65,-278.39 692.9,-279.3 692.96,-280.22 692.85,-281.15 692.58,-282.09 692.14,-283.03 691.55,-283.97 690.81,-284.91 689.92,-285.85 688.9,-286.78 687.75,-287.7 686.48,-288.61 685.1,-289.51 683.61,-290.39 682.03,-291.25 680.35,-292.09 678.6,-292.91 676.77,-293.7 674.87,-294.46 672.9,-295.19 670.89,-295.89 668.82,-296.56 666.72,-297.19 664.57,-297.79 662.39,-298.34 660.18,-298.85 657.95,-299.32 655.7,-299.75 653.43,-300.14 651.15,-300.47 648.85,-300.76 646.54,-301.01 644.23,-301.2 641.91,-301.35 639.58,-301.45 637.26,-301.5 634.93,-301.5 632.61,-301.45 630.28,-301.35 627.96,-301.2 625.65,-301.01 623.34,-300.76 621.05,-300.47 618.76,-300.14 616.49,-299.75 614.24,-299.32 612.01,-298.85 609.8,-298.34 607.62,-297.79 605.47,-297.19 603.37,-296.56 601.3,-295.89 599.29,-295.19 597.33,-294.46 595.43,-293.7 593.59,-292.91 591.84,-292.09 590.16,-291.25 588.58,-290.39 587.09,-289.51 585.71,-288.61 584.44,-287.7 583.29,-286.78 582.27,-285.85 581.39,-284.91 580.64,-283.97 580.05,-283.03 579.61,-282.09 579.34,-281.15 579.23,-280.22 579.29,-279.3 579.54,-278.39 579.96,-277.49 580.56,-276.61 581.35,-275.75 582.33,-274.91 583.49,-274.09 584.84,-273.3 586.38,-272.54 588.09,-271.81 589.98,-271.11 592.05,-270.44 594.28,-269.81 596.67,-269.21 599.22,-268.66 601.91,-268.15 604.73,-267.68 607.68,-267.25 610.75,-266.86 613.91,-266.53 617.17,-266.24 620.5,-265.99 623.9,-265.8 627.35,-265.65 630.83,-265.55 634.34,-265.5 637.85,-265.5 641.36,-265.55\"/>\n",
+       "<text text-anchor=\"middle\" x=\"636.1\" y=\"-278.45\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(or22)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(or22)]&#45;&gt;[neg(and12)] -->\n",
+       "<g id=\"edge21\" class=\"edge\">\n",
+       "<title>[neg(or22)]&#45;&gt;[neg(and12)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M635.11,-265.41C634.43,-253.76 633.53,-238.05 632.74,-224.52\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"636.26,-224.64 632.19,-214.86 629.27,-225.05 636.26,-224.64\"/>\n",
+       "<text text-anchor=\"middle\" x=\"646.47\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">or22</text>\n",
+       "</g>\n",
+       "<!-- [neg(or22)]&#45;&gt;[neg(not1)] -->\n",
+       "<g id=\"edge22\" class=\"edge\">\n",
+       "<title>[neg(or22)]&#45;&gt;[neg(not1)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M660.99,-266.43C682.58,-252.5 713.98,-232.23 737.55,-217.01\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"739.35,-220.01 745.86,-211.65 735.56,-214.13 739.35,-220.01\"/>\n",
+       "<text text-anchor=\"middle\" x=\"727.47\" y=\"-234.2\" font-family=\"Times,serif\" font-size=\"14.00\">or22</text>\n",
+       "</g>\n",
+       "<!-- [neg(or22),neg(not2),neg(or4)] -->\n",
+       "<g id=\"node28\" class=\"node\">\n",
+       "<title>[neg(or22),neg(not2),neg(or4)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"727.52,-796.55 735.75,-796.65 743.89,-796.8 751.91,-796.99 759.78,-797.24 767.47,-797.53 774.95,-797.86 782.18,-798.25 789.15,-798.68 795.82,-799.15 802.17,-799.66 808.18,-800.21 813.83,-800.81 819.1,-801.44 823.97,-802.11 828.44,-802.81 832.48,-803.54 836.1,-804.3 839.29,-805.09 842.03,-805.91 844.34,-806.75 846.21,-807.61 847.64,-808.49 848.63,-809.39 849.2,-810.3 849.36,-811.22 849.1,-812.15 848.45,-813.09 847.42,-814.03 846.02,-814.97 844.27,-815.91 842.18,-816.85 839.77,-817.78 837.05,-818.7 834.06,-819.61 830.79,-820.51 827.28,-821.39 823.54,-822.25 819.59,-823.09 815.44,-823.91 811.12,-824.7 806.63,-825.46 802,-826.19 797.24,-826.89 792.37,-827.56 787.39,-828.19 782.33,-828.79 777.18,-829.34 771.97,-829.85 766.7,-830.32 761.38,-830.75 756.02,-831.14 750.63,-831.47 745.2,-831.76 739.76,-832.01 734.3,-832.2 728.82,-832.35 723.33,-832.45 717.84,-832.5 712.35,-832.5 706.86,-832.45 701.37,-832.35 695.9,-832.2 690.43,-832.01 684.99,-831.76 679.56,-831.47 674.17,-831.14 668.81,-830.75 663.49,-830.32 658.22,-829.85 653.01,-829.34 647.86,-828.79 642.8,-828.19 637.82,-827.56 632.95,-826.89 628.19,-826.19 623.56,-825.46 619.07,-824.7 614.75,-823.91 610.6,-823.09 606.65,-822.25 602.91,-821.39 599.4,-820.51 596.13,-819.61 593.14,-818.7 590.42,-817.78 588.01,-816.85 585.92,-815.91 584.17,-814.97 582.77,-814.03 581.74,-813.09 581.09,-812.15 580.83,-811.22 580.99,-810.3 581.56,-809.39 582.56,-808.49 583.98,-807.61 585.85,-806.75 588.16,-805.91 590.9,-805.09 594.09,-804.3 597.71,-803.54 601.76,-802.81 606.22,-802.11 611.1,-801.44 616.37,-800.81 622.01,-800.21 628.02,-799.66 634.37,-799.15 641.04,-798.68 648.01,-798.25 655.25,-797.86 662.72,-797.53 670.41,-797.24 678.28,-796.99 686.3,-796.8 694.45,-796.65 702.67,-796.55 710.95,-796.5 719.24,-796.5 727.52,-796.55\"/>\n",
+       "<text text-anchor=\"middle\" x=\"715.1\" y=\"-809.45\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(or22),neg(not2),neg(or4)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(or22),neg(not2),neg(or4)]&#45;&gt;[neg(and12),neg(not2),neg(or4)] -->\n",
+       "<g id=\"edge23\" class=\"edge\">\n",
+       "<title>[neg(or22),neg(not2),neg(or4)]&#45;&gt;[neg(and12),neg(not2),neg(or4)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M714.31,-796.41C713.77,-784.76 713.04,-769.05 712.41,-755.52\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"715.93,-755.69 711.97,-745.86 708.93,-756.01 715.93,-755.69\"/>\n",
+       "<text text-anchor=\"middle\" x=\"725.47\" y=\"-765.2\" font-family=\"Times,serif\" font-size=\"14.00\">or22</text>\n",
+       "</g>\n",
+       "<!-- [neg(or22),neg(not2),neg(or4)]&#45;&gt;[neg(not1),neg(not2),neg(or4)] -->\n",
+       "<g id=\"edge24\" class=\"edge\">\n",
+       "<title>[neg(or22),neg(not2),neg(or4)]&#45;&gt;[neg(not1),neg(not2),neg(or4)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M769.64,-797.23C818.86,-782.55 891.24,-760.96 942.73,-745.6\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"943.68,-748.97 952.26,-742.76 941.68,-742.26 943.68,-748.97\"/>\n",
+       "<text text-anchor=\"middle\" x=\"897.47\" y=\"-765.2\" font-family=\"Times,serif\" font-size=\"14.00\">or22</text>\n",
+       "</g>\n",
+       "<!-- [neg(or3)] -->\n",
+       "<g id=\"node29\" class=\"node\">\n",
+       "<title>[neg(or3)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"509.9,-354.05 513.09,-354.15 516.24,-354.3 519.34,-354.49 522.39,-354.74 525.37,-355.03 528.26,-355.36 531.06,-355.75 533.75,-356.18 536.34,-356.65 538.79,-357.16 541.12,-357.71 543.31,-358.31 545.34,-358.94 547.23,-359.61 548.96,-360.31 550.53,-361.04 551.93,-361.8 553.16,-362.59 554.22,-363.41 555.11,-364.25 555.84,-365.11 556.39,-365.99 556.78,-366.89 557,-367.8 557.06,-368.72 556.96,-369.65 556.71,-370.59 556.31,-371.53 555.77,-372.47 555.09,-373.41 554.28,-374.35 553.34,-375.28 552.29,-376.2 551.13,-377.11 549.87,-378.01 548.51,-378.89 547.07,-379.75 545.54,-380.59 543.93,-381.41 542.26,-382.2 540.52,-382.96 538.73,-383.69 536.89,-384.39 535,-385.06 533.08,-385.69 531.11,-386.29 529.12,-386.84 527.11,-387.35 525.07,-387.82 523.01,-388.25 520.93,-388.64 518.85,-388.97 516.75,-389.26 514.64,-389.51 512.53,-389.7 510.41,-389.85 508.28,-389.95 506.16,-390 504.03,-390 501.91,-389.95 499.78,-389.85 497.67,-389.7 495.55,-389.51 493.44,-389.26 491.34,-388.97 489.26,-388.64 487.18,-388.25 485.12,-387.82 483.08,-387.35 481.07,-386.84 479.08,-386.29 477.12,-385.69 475.19,-385.06 473.3,-384.39 471.46,-383.69 469.67,-382.96 467.93,-382.2 466.26,-381.41 464.66,-380.59 463.13,-379.75 461.68,-378.89 460.32,-378.01 459.06,-377.11 457.9,-376.2 456.85,-375.28 455.91,-374.35 455.1,-373.41 454.43,-372.47 453.88,-371.53 453.48,-370.59 453.23,-369.65 453.13,-368.72 453.19,-367.8 453.42,-366.89 453.8,-365.99 454.35,-365.11 455.08,-364.25 455.97,-363.41 457.03,-362.59 458.26,-361.8 459.67,-361.04 461.23,-360.31 462.96,-359.61 464.85,-358.94 466.89,-358.31 469.07,-357.71 471.4,-357.16 473.86,-356.65 476.44,-356.18 479.13,-355.75 481.93,-355.36 484.83,-355.03 487.8,-354.74 490.85,-354.49 493.95,-354.3 497.1,-354.15 500.29,-354.05 503.49,-354 506.7,-354 509.9,-354.05\"/>\n",
+       "<text text-anchor=\"middle\" x=\"505.1\" y=\"-366.95\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(or3)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(or3)]&#45;&gt;[neg(not2)] -->\n",
+       "<g id=\"edge26\" class=\"edge\">\n",
+       "<title>[neg(or3)]&#45;&gt;[neg(not2)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M505.1,-353.91C505.1,-342.26 505.1,-326.55 505.1,-313.02\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"508.6,-313.36 505.1,-303.36 501.6,-313.36 508.6,-313.36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"514.1\" y=\"-322.7\" font-family=\"Times,serif\" font-size=\"14.00\">or3</text>\n",
+       "</g>\n",
+       "<!-- [neg(or3)]&#45;&gt;[neg(or22)] -->\n",
+       "<g id=\"edge25\" class=\"edge\">\n",
+       "<title>[neg(or3)]&#45;&gt;[neg(or22)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M529.12,-355.13C550.19,-341.22 580.99,-320.89 604.13,-305.6\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"605.85,-308.66 612.27,-300.23 602,-302.82 605.85,-308.66\"/>\n",
+       "<text text-anchor=\"middle\" x=\"592.1\" y=\"-322.7\" font-family=\"Times,serif\" font-size=\"14.00\">or3</text>\n",
+       "</g>\n",
+       "<!-- [neg(or3),neg(not2),neg(or4)]&#45;&gt;[neg(not2),neg(not2),neg(or4)] -->\n",
+       "<g id=\"edge28\" class=\"edge\">\n",
+       "<title>[neg(or3),neg(not2),neg(or4)]&#45;&gt;[neg(not2),neg(not2),neg(or4)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M543.04,-884.91C521.12,-871.56 490.44,-852.87 466.44,-838.25\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"468.26,-835.26 457.9,-833.05 464.62,-841.24 468.26,-835.26\"/>\n",
+       "<text text-anchor=\"middle\" x=\"522.1\" y=\"-853.7\" font-family=\"Times,serif\" font-size=\"14.00\">or3</text>\n",
+       "</g>\n",
+       "<!-- [neg(or3),neg(not2),neg(or4)]&#45;&gt;[neg(or22),neg(not2),neg(or4)] -->\n",
+       "<g id=\"edge27\" class=\"edge\">\n",
+       "<title>[neg(or3),neg(not2),neg(or4)]&#45;&gt;[neg(or22),neg(not2),neg(or4)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M599.55,-884.91C621.88,-871.5 653.16,-852.7 677.55,-838.05\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"679.13,-841.19 685.9,-833.04 675.52,-835.19 679.13,-841.19\"/>\n",
+       "<text text-anchor=\"middle\" x=\"664.1\" y=\"-853.7\" font-family=\"Times,serif\" font-size=\"14.00\">or3</text>\n",
+       "</g>\n",
+       "<!-- [neg(or4)]&#45;&gt;[neg(and3)] -->\n",
+       "<g id=\"edge29\" class=\"edge\">\n",
+       "<title>[neg(or4)]&#45;&gt;[neg(and3)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M416.65,-442.41C407.62,-430.01 395.24,-413.01 384.99,-398.94\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"387.91,-397.01 379.19,-390.98 382.25,-401.13 387.91,-397.01\"/>\n",
+       "<text text-anchor=\"middle\" x=\"413.1\" y=\"-411.2\" font-family=\"Times,serif\" font-size=\"14.00\">or4</text>\n",
+       "</g>\n",
+       "<!-- [neg(or4)]&#45;&gt;[neg(or3)] -->\n",
+       "<g id=\"edge30\" class=\"edge\">\n",
+       "<title>[neg(or4)]&#45;&gt;[neg(or3)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M443.75,-442.82C454.97,-430.06 470.61,-412.25 483.3,-397.81\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"485.77,-400.29 489.75,-390.47 480.52,-395.67 485.77,-400.29\"/>\n",
+       "<text text-anchor=\"middle\" x=\"483.1\" y=\"-411.2\" font-family=\"Times,serif\" font-size=\"14.00\">or4</text>\n",
+       "</g>\n",
+       "<!-- [neg(output)] -->\n",
+       "<g id=\"node32\" class=\"node\">\n",
+       "<title>[neg(output)]</title>\n",
+       "<polygon fill=\"none\" stroke=\"blue\" points=\"577.01,-1150.55 580.93,-1150.65 584.81,-1150.8 588.63,-1150.99 592.38,-1151.24 596.04,-1151.53 599.6,-1151.86 603.05,-1152.25 606.37,-1152.68 609.54,-1153.15 612.57,-1153.66 615.43,-1154.21 618.12,-1154.81 620.63,-1155.44 622.95,-1156.11 625.08,-1156.81 627.01,-1157.54 628.73,-1158.3 630.25,-1159.09 631.56,-1159.91 632.66,-1160.75 633.55,-1161.61 634.23,-1162.49 634.7,-1163.39 634.97,-1164.3 635.05,-1165.22 634.93,-1166.15 634.62,-1167.09 634.13,-1168.03 633.46,-1168.97 632.62,-1169.91 631.63,-1170.85 630.48,-1171.78 629.19,-1172.7 627.76,-1173.61 626.2,-1174.51 624.53,-1175.39 622.75,-1176.25 620.87,-1177.09 618.89,-1177.91 616.83,-1178.7 614.7,-1179.46 612.49,-1180.19 610.22,-1180.89 607.9,-1181.56 605.53,-1182.19 603.12,-1182.79 600.67,-1183.34 598.19,-1183.85 595.68,-1184.32 593.14,-1184.75 590.59,-1185.14 588.02,-1185.47 585.44,-1185.76 582.84,-1186.01 580.24,-1186.2 577.63,-1186.35 575.02,-1186.45 572.4,-1186.5 569.79,-1186.5 567.17,-1186.45 564.56,-1186.35 561.95,-1186.2 559.35,-1186.01 556.75,-1185.76 554.17,-1185.47 551.6,-1185.14 549.05,-1184.75 546.51,-1184.32 544,-1183.85 541.52,-1183.34 539.07,-1182.79 536.66,-1182.19 534.29,-1181.56 531.97,-1180.89 529.7,-1180.19 527.5,-1179.46 525.36,-1178.7 523.3,-1177.91 521.32,-1177.09 519.44,-1176.25 517.66,-1175.39 515.99,-1174.51 514.43,-1173.61 513,-1172.7 511.71,-1171.78 510.56,-1170.85 509.57,-1169.91 508.73,-1168.97 508.07,-1168.03 507.57,-1167.09 507.26,-1166.15 507.14,-1165.22 507.22,-1164.3 507.49,-1163.39 507.96,-1162.49 508.65,-1161.61 509.53,-1160.75 510.63,-1159.91 511.94,-1159.09 513.46,-1158.3 515.18,-1157.54 517.11,-1156.81 519.24,-1156.11 521.56,-1155.44 524.07,-1154.81 526.76,-1154.21 529.62,-1153.66 532.65,-1153.15 535.82,-1152.68 539.14,-1152.25 542.59,-1151.86 546.15,-1151.53 549.81,-1151.24 553.56,-1150.99 557.38,-1150.8 561.26,-1150.65 565.18,-1150.55 569.12,-1150.5 573.07,-1150.5 577.01,-1150.55\"/>\n",
+       "<text text-anchor=\"middle\" x=\"571.1\" y=\"-1163.45\" font-family=\"Times,serif\" font-size=\"14.00\">[neg(output)]</text>\n",
+       "</g>\n",
+       "<!-- [neg(output)]&#45;&gt;[neg(and5)] -->\n",
+       "<g id=\"edge31\" class=\"edge\">\n",
+       "<title>[neg(output)]&#45;&gt;[neg(and5)]</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M571.1,-1150.41C571.1,-1138.76 571.1,-1123.05 571.1,-1109.52\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"574.6,-1109.86 571.1,-1099.86 567.6,-1109.86 574.6,-1109.86\"/>\n",
+       "<text text-anchor=\"middle\" x=\"588.35\" y=\"-1119.2\" font-family=\"Times,serif\" font-size=\"14.00\">output</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n"
+      ],
       "text/plain": [
        "digraph {\n",
        "\"[]\" [shape=\"rect\", color=\"green\"]\n",