doc/example_proof.svg

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
 "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
<!-- Generated by graphviz version 2.40.1 (20161225.0304)
 -->
<!-- Title: unsat_graph Pages: 1 -->
<svg width="648pt" height="479pt"
 viewBox="0.00 0.00 647.50 479.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 475)">
<title>unsat_graph</title>
<polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-475 643.5,-475 643.5,4 -4,4"/>
<!-- vertex_0 -->
<g id="node1" class="node">
<title>vertex_0</title>
<polygon fill="#ff0000" stroke="#ff0000" points="259,-471 205,-471 205,-435 259,-435 259,-471"/>
<text text-anchor="middle" x="232" y="-449.3" font-family="Times,serif" font-size="14.00" fill="#000000">[]</text>
</g>
<!-- vertex_1 -->
<g id="node2" class="node">
<title>vertex_1</title>
<polygon fill="#ff0000" stroke="#ff0000" points="259,-384 205,-384 205,-348 259,-348 259,-384"/>
<text text-anchor="middle" x="232" y="-362.3" font-family="Times,serif" font-size="14.00" fill="#000000">[]</text>
</g>
<!-- vertex_0&#45;&gt;vertex_1 -->
<g id="edge1" class="edge">
<title>vertex_0&#45;&gt;vertex_1</title>
<path fill="none" stroke="#000000" d="M232,-424.8156C232,-411.4102 232,-395.7801 232,-384.0034"/>
<polygon fill="#000000" stroke="#000000" points="228.5001,-424.9735 232,-434.9735 235.5001,-424.9736 228.5001,-424.9735"/>
<text text-anchor="middle" x="261" y="-405.8" font-family="Times,serif" font-size="14.00" fill="#000000">simplify</text>
</g>
<!-- vertex_2 -->
<g id="node3" class="node">
<title>vertex_2</title>
<polygon fill="#d3d3d3" stroke="#000000" points="255,-297 35,-297 35,-261 255,-261 255,-297"/>
<text text-anchor="middle" x="145" y="-275.3" font-family="Times,serif" font-size="14.00" fill="#000000">forall (X2:i). [¬p (f X2) X2]/2</text>
</g>
<!-- vertex_1&#45;&gt;vertex_2 -->
<g id="edge2" class="edge">
<title>vertex_1&#45;&gt;vertex_2</title>
<path fill="none" stroke="#000000" d="M206.5688,-340.5688C192.5952,-326.5952 175.5963,-309.5963 163.0034,-297.0034"/>
<polygon fill="#000000" stroke="#000000" points="204.4276,-343.3773 213.9735,-347.9735 209.3773,-338.4276 204.4276,-343.3773"/>
<text text-anchor="middle" x="217" y="-318.8" font-family="Times,serif" font-size="14.00" fill="#000000">s_sup&#45;</text>
</g>
<!-- vertex_5 -->
<g id="node6" class="node">
<title>vertex_5</title>
<polygon fill="#d3d3d3" stroke="#000000" points="370.5,-297 275.5,-297 275.5,-261 370.5,-261 370.5,-297"/>
<text text-anchor="middle" x="323" y="-275.3" font-family="Times,serif" font-size="14.00" fill="#000000">[p (f a) a]/4</text>
</g>
<!-- vertex_1&#45;&gt;vertex_5 -->
<g id="edge5" class="edge">
<title>vertex_1&#45;&gt;vertex_5</title>
<path fill="none" stroke="#000000" d="M258.1952,-340.9562C272.8868,-326.9104 290.875,-309.7129 304.1689,-297.0034"/>
<polygon fill="#000000" stroke="#000000" points="255.6648,-338.5332 250.8553,-347.9735 260.5021,-343.593 255.6648,-338.5332"/>
<text text-anchor="middle" x="306" y="-318.8" font-family="Times,serif" font-size="14.00" fill="#000000">s_sup&#45;</text>
</g>
<!-- vertex_3 -->
<g id="node4" class="node">
<title>vertex_3</title>
<polygon fill="#d3d3d3" stroke="#000000" points="242.5,-210 27.5,-210 27.5,-174 242.5,-174 242.5,-210"/>
<text text-anchor="middle" x="135" y="-188.3" font-family="Times,serif" font-size="14.00" fill="#000000">¬ (∃ x/13:i. (p (f x/13) x/13))</text>
</g>
<!-- vertex_2&#45;&gt;vertex_3 -->
<g id="edge3" class="edge">
<title>vertex_2&#45;&gt;vertex_3</title>
<path fill="none" stroke="#000000" d="M141.7604,-250.8156C140.2196,-237.4102 138.423,-221.7801 137.0694,-210.0034"/>
<polygon fill="#000000" stroke="#000000" points="138.3089,-251.4387 142.928,-260.9735 145.2631,-250.6393 138.3089,-251.4387"/>
<text text-anchor="middle" x="152.5" y="-231.8" font-family="Times,serif" font-size="14.00" fill="#000000">cnf</text>
</g>
<!-- vertex_4 -->
<g id="node5" class="node">
<title>vertex_4</title>
<polygon fill="#00ff00" stroke="#00ff00" points="188,-123 0,-123 0,-87 188,-87 188,-123"/>
<text text-anchor="middle" x="94" y="-101.3" font-family="Times,serif" font-size="14.00" fill="#000000">∃ x/13:i. (p (f x/13) x/13)</text>
</g>
<!-- vertex_3&#45;&gt;vertex_4 -->
<g id="edge4" class="edge">
<title>vertex_3&#45;&gt;vertex_4</title>
<path fill="none" stroke="#000000" d="M122.0918,-164.6093C115.6926,-151.0307 108.1442,-135.0133 102.4843,-123.0034"/>
<polygon fill="#000000" stroke="#000000" points="119.0757,-166.4198 126.5048,-173.9735 125.4078,-163.4356 119.0757,-166.4198"/>
<text text-anchor="middle" x="149" y="-144.8" font-family="Times,serif" font-size="14.00" fill="#000000">neg_goal</text>
</g>
<!-- vertex_6 -->
<g id="node7" class="node">
<title>vertex_6</title>
<polygon fill="#d3d3d3" stroke="#000000" points="430,-210 302,-210 302,-174 430,-174 430,-210"/>
<text text-anchor="middle" x="366" y="-188.3" font-family="Times,serif" font-size="14.00" fill="#000000">[p (f a) a ∨ ⊥]/3</text>
</g>
<!-- vertex_5&#45;&gt;vertex_6 -->
<g id="edge6" class="edge">
<title>vertex_5&#45;&gt;vertex_6</title>
<path fill="none" stroke="#000000" d="M336.3428,-252.0041C343.0953,-238.3421 351.1082,-222.1299 357.1018,-210.0034"/>
<polygon fill="#000000" stroke="#000000" points="333.2029,-250.4579 331.9096,-260.9735 339.4782,-253.5596 333.2029,-250.4579"/>
<text text-anchor="middle" x="377" y="-231.8" font-family="Times,serif" font-size="14.00" fill="#000000">simplify</text>
</g>
<!-- vertex_7 -->
<g id="node8" class="node">
<title>vertex_7</title>
<polygon fill="#d3d3d3" stroke="#000000" points="526,-123 206,-123 206,-87 526,-87 526,-123"/>
<text text-anchor="middle" x="366" y="-101.3" font-family="Times,serif" font-size="14.00" fill="#000000">forall (X0:i) (X1:i). [p X0 X1 ∨ ¬p X1 X0]/0</text>
</g>
<!-- vertex_6&#45;&gt;vertex_7 -->
<g id="edge7" class="edge">
<title>vertex_6&#45;&gt;vertex_7</title>
<path fill="none" stroke="#000000" d="M366,-163.8156C366,-150.4102 366,-134.7801 366,-123.0034"/>
<polygon fill="#000000" stroke="#000000" points="362.5001,-163.9735 366,-173.9735 369.5001,-163.9736 362.5001,-163.9735"/>
<text text-anchor="middle" x="389" y="-144.8" font-family="Times,serif" font-size="14.00" fill="#000000">s_sup&#45;</text>
</g>
<!-- vertex_9 -->
<g id="node10" class="node">
<title>vertex_9</title>
<polygon fill="#d3d3d3" stroke="#000000" points="639.5,-123 544.5,-123 544.5,-87 639.5,-87 639.5,-123"/>
<text text-anchor="middle" x="592" y="-101.3" font-family="Times,serif" font-size="14.00" fill="#000000">[p a (f a)]/1</text>
</g>
<!-- vertex_6&#45;&gt;vertex_9 -->
<g id="edge9" class="edge">
<title>vertex_6&#45;&gt;vertex_9</title>
<path fill="none" stroke="#000000" d="M422.1968,-170.3667C460.0863,-155.7809 509.491,-136.7623 545.2326,-123.0034"/>
<polygon fill="#000000" stroke="#000000" points="420.9023,-167.1146 412.8273,-173.9735 423.4172,-173.6473 420.9023,-167.1146"/>
<text text-anchor="middle" x="516" y="-144.8" font-family="Times,serif" font-size="14.00" fill="#000000">s_sup&#45;</text>
</g>
<!-- vertex_8 -->
<g id="node9" class="node">
<title>vertex_8</title>
<polygon fill="#ffff00" stroke="#ffff00" points="519.5,-36 212.5,-36 212.5,0 519.5,0 519.5,-36"/>
<text text-anchor="middle" x="366" y="-14.3" font-family="Times,serif" font-size="14.00" fill="#000000">∀ x/9:i y/11:i. ((p x/9 y/11) ⇒ (p y/11 x/9))</text>
</g>
<!-- vertex_7&#45;&gt;vertex_8 -->
<g id="edge8" class="edge">
<title>vertex_7&#45;&gt;vertex_8</title>
<path fill="none" stroke="#000000" d="M366,-76.8156C366,-63.4102 366,-47.7801 366,-36.0034"/>
<polygon fill="#000000" stroke="#000000" points="362.5001,-76.9735 366,-86.9735 369.5001,-76.9736 362.5001,-76.9735"/>
<text text-anchor="middle" x="377.5" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">cnf</text>
</g>
<!-- vertex_10 -->
<g id="node11" class="node">
<title>vertex_10</title>
<polygon fill="#ffff00" stroke="#ffff00" points="627.5,-36 556.5,-36 556.5,0 627.5,0 627.5,-36"/>
<text text-anchor="middle" x="592" y="-14.3" font-family="Times,serif" font-size="14.00" fill="#000000">p a (f a)</text>
</g>
<!-- vertex_9&#45;&gt;vertex_10 -->
<g id="edge10" class="edge">
<title>vertex_9&#45;&gt;vertex_10</title>
<path fill="none" stroke="#000000" d="M592,-76.8156C592,-63.4102 592,-47.7801 592,-36.0034"/>
<polygon fill="#000000" stroke="#000000" points="588.5001,-76.9735 592,-86.9735 595.5001,-76.9736 588.5001,-76.9735"/>
<text text-anchor="middle" x="603.5" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">cnf</text>
</g>
</g>
</svg>