From 86446f5c3f3ec32b8aa2370276d3dde92bee855c Mon Sep 17 00:00:00 2001 From: Michael Leuschel <leuschel@uni-duesseldorf.de> Date: Tue, 15 Nov 2022 14:16:46 +0100 Subject: [PATCH] add SLD tree for circuit example Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de> --- logic_programming/5_SLD.ipynb | 366 ++++++++++++++++++++++++++++++++-- 1 file changed, 353 insertions(+), 13 deletions(-) diff --git a/logic_programming/5_SLD.ipynb b/logic_programming/5_SLD.ipynb index 2f8f702..a5fa19f 100644 --- a/logic_programming/5_SLD.ipynb +++ b/logic_programming/5_SLD.ipynb @@ -79,7 +79,7 @@ }, { "cell_type": "code", - "execution_count": 5, + "execution_count": 2, "id": "26e0221b", "metadata": { "vscode": { @@ -107,7 +107,7 @@ }, { "cell_type": "code", - "execution_count": 6, + "execution_count": 3, "id": "152289b6", "metadata": { "vscode": { @@ -140,7 +140,7 @@ }, { "cell_type": "code", - "execution_count": 7, + "execution_count": 4, "id": "2c3dd1bf", "metadata": { "vscode": { @@ -173,7 +173,7 @@ }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 5, "id": "33fc6271", "metadata": { "vscode": { @@ -200,7 +200,7 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 6, "id": "f2a8b4a4", "metadata": { "vscode": { @@ -234,7 +234,7 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 7, "id": "06aa608c", "metadata": { "vscode": { @@ -268,7 +268,7 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 8, "id": "a76d8b5d", "metadata": { "vscode": { @@ -310,7 +310,7 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 9, "id": "d7a0cc62", "metadata": { "vscode": { @@ -338,7 +338,7 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 10, "id": "78163b60", "metadata": { "vscode": { @@ -399,7 +399,7 @@ }, { "cell_type": "code", - "execution_count": 25, + "execution_count": 11, "id": "9d3fbd1a", "metadata": { "vscode": { @@ -418,7 +418,7 @@ }, { "cell_type": "code", - "execution_count": 26, + "execution_count": 12, "id": "a8ba5814", "metadata": { "vscode": { @@ -483,7 +483,7 @@ }, { "cell_type": "code", - "execution_count": 23, + "execution_count": 13, "id": "26924712", "metadata": { "vscode": { @@ -511,7 +511,7 @@ }, { "cell_type": "code", - "execution_count": 28, + "execution_count": 14, "id": "7d90c4ad", "metadata": { "vscode": { @@ -554,6 +554,346 @@ "source": [ "By putting the above queries into a tree we obtain a so-called ```SLD-tree``` for the program and top-level query under consideration." ] + }, + { + "cell_type": "markdown", + "id": "29e3d513", + "metadata": {}, + "source": [ + "Below is some code to display this SLD-tree graphically in Jupyter:" + ] + }, + { + "cell_type": "code", + "execution_count": 15, + "id": "cdfb419b", + "metadata": { + "vscode": { + "languageId": "prolog" + } + }, + "outputs": [], + "source": [ + "sld_node(Query,[shape/S,color/C],InitialQuery,ProgNr) :- sub_goal(InitialQuery,ProgNr,Query),\n", + " (Query=[] -> S=rect,C=green ; sld_edge(Query,_,ProgNr,_) -> S=egg, C=blue ; S=ellipse, C=red).\n", + "\n", + "sub_goal(Q,_,Q).\n", + "sub_goal(Q,ProgNr,SubG) :- sld_edge(Q,_,ProgNr,NewQuery),\n", + " sub_goal(NewQuery,ProgNr,SubG).\n", + "\n", + "sld_edge(Q,Lit,ProgNr,NewQuery) :- selection_rule(Q,neg(Lit),_),\n", + " program(ProgNr,_,Clauses), resolve_query(Q,Clauses,NewQuery).\n" + ] + }, + { + "cell_type": "code", + "execution_count": 16, + "id": "8f652455", + "metadata": { + "vscode": { + "languageId": "prolog" + } + }, + "outputs": [ + { + "data": { + "text/plain": [ + "\u001b[1mQ = [neg(p)],\n", + "L = [shape/egg,color/blue]" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "?- sld_node(Q,L,[neg(p)],2)." + ] + }, + { + "cell_type": "code", + "execution_count": 17, + "id": "bc5e2d49", + "metadata": { + "vscode": { + "languageId": "prolog" + } + }, + "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)]->[neg(q),neg(r)] -->\n<g id=\"edge1\" class=\"edge\">\n<title>[neg(p)]->[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)]->[neg(s),neg(r)] -->\n<g id=\"edge3\" class=\"edge\">\n<title>[neg(q),neg(r)]->[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)]->[neg(t),neg(r)] -->\n<g id=\"edge2\" class=\"edge\">\n<title>[neg(q),neg(r)]->[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)]->[] -->\n<g id=\"edge4\" class=\"edge\">\n<title>[neg(r)]->[]</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)]->[neg(r)] -->\n<g id=\"edge5\" class=\"edge\">\n<title>[neg(s),neg(r)]->[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", + "text/plain": [ + "digraph {\n", + "\"[]\" [shape=\"rect\", color=\"green\"]\n", + "\"[neg(p)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(q),neg(r)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(r)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(s),neg(r)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(t),neg(r)]\" [shape=\"ellipse\", color=\"red\"]\n", + " \"[neg(p)]\" -> \"[neg(q),neg(r)]\" [label=\"p\", color=\"black\", style=\"solid\"]\n", + " \"[neg(q),neg(r)]\" -> \"[neg(t),neg(r)]\" [label=\"q\", color=\"black\", style=\"solid\"]\n", + " \"[neg(q),neg(r)]\" -> \"[neg(s),neg(r)]\" [label=\"q\", color=\"black\", style=\"solid\"]\n", + " \"[neg(r)]\" -> \"[]\" [label=\"r\", color=\"black\", style=\"solid\"]\n", + " \"[neg(s),neg(r)]\" -> \"[neg(r)]\" [label=\"s\", color=\"black\", style=\"solid\"]\n", + "}" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/plain": [ + "\u001b[1mtrue" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "jupyter:show_graph(sld_node(_,_,[neg(p)],2),sld_edge(_,_,2,_))" + ] + }, + { + "cell_type": "code", + "execution_count": 18, + "id": "64f06b8f", + "metadata": { + "vscode": { + "languageId": "prolog" + } + }, + "outputs": [ + { + "data": { + "text/plain": [ + "\u001b[1;31mfalse" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "?-sld_edge([neg(p)],L,NQ,2)." + ] + }, + { + "cell_type": "code", + "execution_count": 19, + "id": "a847a9b7", + "metadata": { + "vscode": { + "languageId": "prolog" + } + }, + "outputs": [], + "source": [ + "program(3,'circuit', [\n", + " % Die Belegung von der Aufgabe:\n", + "[pos(a)], [pos(not_b)], [pos(c)],[pos(not_d)], [pos(e)],\n", + "% Schaltungen der ersten Ebene\n", + "[pos(and11) , neg(a),neg(b)],\n", + "[pos(or11) , neg(b)],\n", + "[pos(or11) , neg(c)],\n", + "[pos(and12) , neg(c),neg(d)],\n", + "[pos(not1) , neg(not_e)],\n", + "% Schaltungen der zweiten Ebene\n", + "[pos(or21) , neg(and11)],\n", + "[pos(or21) , neg(not1)],\n", + "[pos(and2) , neg(or11),neg(not1)],\n", + "[pos(or22) , neg(and12)],\n", + "[pos(or22) , neg(not1)],\n", + "[pos(not2) , neg(e)], % \\+ not1)],\n", + "% Schaltungen der dritten Ebene\n", + "[pos(and3) , neg(or21),neg(and2)],\n", + "[pos(or3) , neg(or22)],\n", + "[pos(or3) , neg(not2)],\n", + "% Schaltungen der vierten Ebene\n", + "[pos(or4) , neg(and3)],\n", + "[pos(or4) , neg(or3)],\n", + "[pos(and4) , neg(or3),neg(not2)],\n", + "% Letzte Ebene\n", + "[pos(and5) , neg(and4),neg(or4)],\n", + "[pos(output) , neg(and5)]\n", + "]) :- true." + ] + }, + { + "cell_type": "code", + "execution_count": 20, + "id": "e46506a9", + "metadata": { + "vscode": { + "languageId": "prolog" + } + }, + "outputs": [ + { + "data": { + "text/plain": [ + " 1: [neg(output)]\n", + " 2: [neg(and5)]\n", + " 3: [neg(and4),neg(or4)]\n", + " 4: [neg(or3),neg(not2),neg(or4)]\n", + " 5: [neg(or22),neg(not2),neg(or4)]\n", + " 6: [neg(and12),neg(not2),neg(or4)]\n", + " 7: [neg(c),neg(d),neg(not2),neg(or4)]\n", + " 8: [neg(d),neg(not2),neg(or4)]\n", + " 6: [neg(not1),neg(not2),neg(or4)]\n", + " 7: [neg(not_e),neg(not2),neg(or4)]\n", + " 5: [neg(not2),neg(not2),neg(or4)]\n", + " 6: [neg(e),neg(not2),neg(or4)]\n", + " 7: [neg(not2),neg(or4)]\n", + " 8: [neg(e),neg(or4)]\n", + " 9: [neg(or4)]\n", + " 10: [neg(and3)]\n", + " 11: [neg(or21),neg(and2)]\n", + " 12: [neg(and11),neg(and2)]\n", + " 13: [neg(a),neg(b),neg(and2)]\n", + " 14: [neg(b),neg(and2)]\n", + " 12: [neg(not1),neg(and2)]\n", + " 13: [neg(not_e),neg(and2)]\n", + " 10: [neg(or3)]\n", + " 11: [neg(or22)]\n", + " 12: [neg(and12)]\n", + " 13: [neg(c),neg(d)]\n", + " 14: [neg(d)]\n", + " 12: [neg(not1)]\n", + " 13: [neg(not_e)]\n", + " 11: [neg(not2)]\n", + " 12: [neg(e)]\n", + " 13: [] (contradiction)" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/plain": [ + "\u001b[1mClauses = [[pos(a)],[pos(not_b)],[pos(c)],[pos(not_d)],[pos(e)],[pos(and11),neg(a),neg(b)],[pos(or11),neg(b)],[pos(or11),neg(c)],[pos(and12),neg(c),neg(d)],[pos(not1),neg(not_e)],[pos(or21),neg(and11)],[pos(or21),neg(not1)],[pos(and2),neg(or11),neg(not1)],[pos(or22),neg(and12)],[pos(or22),neg(not1)],[pos(not2),neg(e)],[pos(and3),neg(or21),neg(and2)],[pos(or3),neg(or22)],[pos(or3),neg(not2)],[pos(or4),neg(and3)],[pos(or4),neg(or3)],[pos(and4),neg(or3),neg(not2)],[pos(and5),neg(and4),neg(or4)],[pos(output),neg(and5)]]" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "?- program(3,_,Clauses), trace_prove(output,Clauses)." + ] + }, + { + "cell_type": "code", + "execution_count": 21, + "id": "9d979ec6", + "metadata": { + "vscode": { + "languageId": "prolog" + } + }, + "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)]->[neg(b),neg(and2)] -->\n<g id=\"edge1\" class=\"edge\">\n<title>[neg(a),neg(b),neg(and2)]->[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)]->[neg(a),neg(b),neg(and2)] -->\n<g id=\"edge2\" class=\"edge\">\n<title>[neg(and11),neg(and2)]->[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)]->[neg(c),neg(d)] -->\n<g id=\"edge3\" class=\"edge\">\n<title>[neg(and12)]->[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)]->[neg(c),neg(d),neg(not2),neg(or4)] -->\n<g id=\"edge4\" class=\"edge\">\n<title>[neg(and12),neg(not2),neg(or4)]->[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)]->[neg(or21),neg(and2)] -->\n<g id=\"edge5\" class=\"edge\">\n<title>[neg(and3)]->[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)]->[neg(or3),neg(not2),neg(or4)] -->\n<g id=\"edge6\" class=\"edge\">\n<title>[neg(and4),neg(or4)]->[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)]->[neg(and4),neg(or4)] -->\n<g id=\"edge7\" class=\"edge\">\n<title>[neg(and5)]->[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)]->[neg(d)] -->\n<g id=\"edge8\" class=\"edge\">\n<title>[neg(c),neg(d)]->[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)]->[neg(d),neg(not2),neg(or4)] -->\n<g id=\"edge9\" class=\"edge\">\n<title>[neg(c),neg(d),neg(not2),neg(or4)]->[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)]->[] -->\n<g id=\"edge10\" class=\"edge\">\n<title>[neg(e)]->[]</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)]->[neg(not2),neg(or4)] -->\n<g id=\"edge11\" class=\"edge\">\n<title>[neg(e),neg(not2),neg(or4)]->[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)]->[neg(or4)] -->\n<g id=\"edge12\" class=\"edge\">\n<title>[neg(e),neg(or4)]->[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)]->[neg(not_e)] -->\n<g id=\"edge13\" class=\"edge\">\n<title>[neg(not1)]->[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)]->[neg(not_e),neg(and2)] -->\n<g id=\"edge14\" class=\"edge\">\n<title>[neg(not1),neg(and2)]->[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)]->[neg(not_e),neg(not2),neg(or4)] -->\n<g id=\"edge15\" class=\"edge\">\n<title>[neg(not1),neg(not2),neg(or4)]->[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)]->[neg(e)] -->\n<g id=\"edge16\" class=\"edge\">\n<title>[neg(not2)]->[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)]->[neg(e),neg(not2),neg(or4)] -->\n<g id=\"edge17\" class=\"edge\">\n<title>[neg(not2),neg(not2),neg(or4)]->[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)]->[neg(e),neg(or4)] -->\n<g id=\"edge18\" class=\"edge\">\n<title>[neg(not2),neg(or4)]->[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)]->[neg(and11),neg(and2)] -->\n<g id=\"edge19\" class=\"edge\">\n<title>[neg(or21),neg(and2)]->[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)]->[neg(not1),neg(and2)] -->\n<g id=\"edge20\" class=\"edge\">\n<title>[neg(or21),neg(and2)]->[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)]->[neg(and12)] -->\n<g id=\"edge21\" class=\"edge\">\n<title>[neg(or22)]->[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)]->[neg(not1)] -->\n<g id=\"edge22\" class=\"edge\">\n<title>[neg(or22)]->[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)]->[neg(and12),neg(not2),neg(or4)] -->\n<g id=\"edge23\" class=\"edge\">\n<title>[neg(or22),neg(not2),neg(or4)]->[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)]->[neg(not1),neg(not2),neg(or4)] -->\n<g id=\"edge24\" class=\"edge\">\n<title>[neg(or22),neg(not2),neg(or4)]->[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)]->[neg(not2)] -->\n<g id=\"edge26\" class=\"edge\">\n<title>[neg(or3)]->[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)]->[neg(or22)] -->\n<g id=\"edge25\" class=\"edge\">\n<title>[neg(or3)]->[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)]->[neg(not2),neg(not2),neg(or4)] -->\n<g id=\"edge28\" class=\"edge\">\n<title>[neg(or3),neg(not2),neg(or4)]->[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)]->[neg(or22),neg(not2),neg(or4)] -->\n<g id=\"edge27\" class=\"edge\">\n<title>[neg(or3),neg(not2),neg(or4)]->[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)]->[neg(and3)] -->\n<g id=\"edge29\" class=\"edge\">\n<title>[neg(or4)]->[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)]->[neg(or3)] -->\n<g id=\"edge30\" class=\"edge\">\n<title>[neg(or4)]->[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)]->[neg(and5)] -->\n<g id=\"edge31\" class=\"edge\">\n<title>[neg(output)]->[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", + "text/plain": [ + "digraph {\n", + "\"[]\" [shape=\"rect\", color=\"green\"]\n", + "\"[neg(a),neg(b),neg(and2)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(and11),neg(and2)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(and12)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(and12),neg(not2),neg(or4)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(and3)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(and4),neg(or4)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(and5)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(b),neg(and2)]\" [shape=\"ellipse\", color=\"red\"]\n", + "\"[neg(c),neg(d)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(c),neg(d),neg(not2),neg(or4)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(d)]\" [shape=\"ellipse\", color=\"red\"]\n", + "\"[neg(d),neg(not2),neg(or4)]\" [shape=\"ellipse\", color=\"red\"]\n", + "\"[neg(e)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(e),neg(not2),neg(or4)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(e),neg(or4)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(not1)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(not1),neg(and2)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(not1),neg(not2),neg(or4)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(not2)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(not2),neg(not2),neg(or4)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(not2),neg(or4)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(not_e)]\" [shape=\"ellipse\", color=\"red\"]\n", + "\"[neg(not_e),neg(and2)]\" [shape=\"ellipse\", color=\"red\"]\n", + "\"[neg(not_e),neg(not2),neg(or4)]\" [shape=\"ellipse\", color=\"red\"]\n", + "\"[neg(or21),neg(and2)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(or22)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(or22),neg(not2),neg(or4)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(or3)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(or3),neg(not2),neg(or4)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(or4)]\" [shape=\"egg\", color=\"blue\"]\n", + "\"[neg(output)]\" [shape=\"egg\", color=\"blue\"]\n", + " \"[neg(a),neg(b),neg(and2)]\" -> \"[neg(b),neg(and2)]\" [label=\"a\", color=\"black\", style=\"solid\"]\n", + " \"[neg(and11),neg(and2)]\" -> \"[neg(a),neg(b),neg(and2)]\" [label=\"and11\", color=\"black\", style=\"solid\"]\n", + " \"[neg(and12)]\" -> \"[neg(c),neg(d)]\" [label=\"and12\", color=\"black\", style=\"solid\"]\n", + " \"[neg(and12),neg(not2),neg(or4)]\" -> \"[neg(c),neg(d),neg(not2),neg(or4)]\" [label=\"and12\", color=\"black\", style=\"solid\"]\n", + " \"[neg(and3)]\" -> \"[neg(or21),neg(and2)]\" [label=\"and3\", color=\"black\", style=\"solid\"]\n", + " \"[neg(and4),neg(or4)]\" -> \"[neg(or3),neg(not2),neg(or4)]\" [label=\"and4\", color=\"black\", style=\"solid\"]\n", + " \"[neg(and5)]\" -> \"[neg(and4),neg(or4)]\" [label=\"and5\", color=\"black\", style=\"solid\"]\n", + " \"[neg(c),neg(d)]\" -> \"[neg(d)]\" [label=\"c\", color=\"black\", style=\"solid\"]\n", + " \"[neg(c),neg(d),neg(not2),neg(or4)]\" -> \"[neg(d),neg(not2),neg(or4)]\" [label=\"c\", color=\"black\", style=\"solid\"]\n", + " \"[neg(e)]\" -> \"[]\" [label=\"e\", color=\"black\", style=\"solid\"]\n", + " \"[neg(e),neg(not2),neg(or4)]\" -> \"[neg(not2),neg(or4)]\" [label=\"e\", color=\"black\", style=\"solid\"]\n", + " \"[neg(e),neg(or4)]\" -> \"[neg(or4)]\" [label=\"e\", color=\"black\", style=\"solid\"]\n", + " \"[neg(not1)]\" -> \"[neg(not_e)]\" [label=\"not1\", color=\"black\", style=\"solid\"]\n", + " \"[neg(not1),neg(and2)]\" -> \"[neg(not_e),neg(and2)]\" [label=\"not1\", color=\"black\", style=\"solid\"]\n", + " \"[neg(not1),neg(not2),neg(or4)]\" -> \"[neg(not_e),neg(not2),neg(or4)]\" [label=\"not1\", color=\"black\", style=\"solid\"]\n", + " \"[neg(not2)]\" -> \"[neg(e)]\" [label=\"not2\", color=\"black\", style=\"solid\"]\n", + " \"[neg(not2),neg(not2),neg(or4)]\" -> \"[neg(e),neg(not2),neg(or4)]\" [label=\"not2\", color=\"black\", style=\"solid\"]\n", + " \"[neg(not2),neg(or4)]\" -> \"[neg(e),neg(or4)]\" [label=\"not2\", color=\"black\", style=\"solid\"]\n", + " \"[neg(or21),neg(and2)]\" -> \"[neg(and11),neg(and2)]\" [label=\"or21\", color=\"black\", style=\"solid\"]\n", + " \"[neg(or21),neg(and2)]\" -> \"[neg(not1),neg(and2)]\" [label=\"or21\", color=\"black\", style=\"solid\"]\n", + " \"[neg(or22)]\" -> \"[neg(and12)]\" [label=\"or22\", color=\"black\", style=\"solid\"]\n", + " \"[neg(or22)]\" -> \"[neg(not1)]\" [label=\"or22\", color=\"black\", style=\"solid\"]\n", + " \"[neg(or22),neg(not2),neg(or4)]\" -> \"[neg(and12),neg(not2),neg(or4)]\" [label=\"or22\", color=\"black\", style=\"solid\"]\n", + " \"[neg(or22),neg(not2),neg(or4)]\" -> \"[neg(not1),neg(not2),neg(or4)]\" [label=\"or22\", color=\"black\", style=\"solid\"]\n", + " \"[neg(or3)]\" -> \"[neg(or22)]\" [label=\"or3\", color=\"black\", style=\"solid\"]\n", + " \"[neg(or3)]\" -> \"[neg(not2)]\" [label=\"or3\", color=\"black\", style=\"solid\"]\n", + " \"[neg(or3),neg(not2),neg(or4)]\" -> \"[neg(or22),neg(not2),neg(or4)]\" [label=\"or3\", color=\"black\", style=\"solid\"]\n", + " \"[neg(or3),neg(not2),neg(or4)]\" -> \"[neg(not2),neg(not2),neg(or4)]\" [label=\"or3\", color=\"black\", style=\"solid\"]\n", + " \"[neg(or4)]\" -> \"[neg(and3)]\" [label=\"or4\", color=\"black\", style=\"solid\"]\n", + " \"[neg(or4)]\" -> \"[neg(or3)]\" [label=\"or4\", color=\"black\", style=\"solid\"]\n", + " \"[neg(output)]\" -> \"[neg(and5)]\" [label=\"output\", color=\"black\", style=\"solid\"]\n", + "}" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/plain": [ + "\u001b[1mtrue" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "jupyter:show_graph(sld_node(_,_,[neg(output)],3),sld_edge(_,_,3,_))" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "fe797463", + "metadata": { + "vscode": { + "languageId": "prolog" + } + }, + "outputs": [], + "source": [] } ], "metadata": { -- GitLab