notxia/unibo-ai-notes
1
0
Fork 0
mirror of https://github.com/NotXia/unibo-ai-notes.git synced 2025-12-14 18:51:52 +01:00
Code Issues Packages Projects Releases Wiki Activity

Add CDMO CDCL

Browse Source
This commit is contained in:
Tian Cheng (Riccardo) Xia
2024-03-15 17:03:33 +01:00
parent 79fd2b6fad
commit bf94726c3a
8 changed files with 815 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

BIN
src/combinatorial-decision-making-and-optimization/img/_cdcl_1uip.pdf Normal file
View File

Binary file not shown.

BIN
src/combinatorial-decision-making-and-optimization/img/_cdcl_cut.pdf Normal file
View File

Binary file not shown.

BIN
src/combinatorial-decision-making-and-optimization/img/_cdcl_example1.pdf Normal file
View File

Binary file not shown.

BIN
src/combinatorial-decision-making-and-optimization/img/_cdcl_example2.pdf Normal file
View File

Binary file not shown.

BIN
src/combinatorial-decision-making-and-optimization/img/_cdcl_example3.pdf Normal file
View File

Binary file not shown.

BIN
src/combinatorial-decision-making-and-optimization/img/_cdcl_example4.pdf Normal file
View File

Binary file not shown.

701
src/combinatorial-decision-making-and-optimization/img/cdcl_example.drawio Normal file
View File

@ -0,0 +1,701 @@
<mxfile host="Electron" modified="2024-03-15T16:02:44.844Z" agent="Mozilla/5.0 (Windows NT 10.0; Win64; x64) AppleWebKit/537.36 (KHTML, like Gecko) draw.io/23.1.5 Chrome/120.0.6099.109 Electron/28.1.0 Safari/537.36" etag="xqsC8_HsGit7oY8XCL57" version="23.1.5" type="device">
<diagram name="Pagina-1" id="TPm98Ap4iW5uKvmGSb2f">
<mxGraphModel dx="1103" dy="1812" grid="1" gridSize="10" guides="1" tooltips="1" connect="1" arrows="1" fold="1" page="1" pageScale="1" pageWidth="827" pageHeight="1169" math="0" shadow="0">
<root>
<mxCell id="0" />
<mxCell id="1" parent="0" />
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-1" value="&lt;font style=&quot;font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i&gt;c&lt;sub style=&quot;&quot;&gt;1&lt;/sub&gt;:&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;1&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨ &lt;i&gt;x&lt;sub&gt;2&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;¬x&lt;sub&gt;4&lt;/sub&gt;&amp;nbsp;&lt;br&gt;c&lt;sub&gt;2&lt;/sub&gt;:&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;1&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;¬x&lt;sub&gt;2&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub&gt;3&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;¬x&lt;sub&gt;4&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub style=&quot;&quot;&gt;5&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub&gt;6&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;sub&gt;5&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;span style=&quot;font-style: italic;&quot;&gt;&lt;sub&gt;6&lt;/sub&gt;&lt;/span&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;6&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;8&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;/font&gt;&lt;font face=&quot;Computer modern&quot;&gt;&lt;br&gt;&lt;/font&gt;" style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="150" y="220" width="200" height="180" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-4" value="&lt;font style=&quot;font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i&gt;c&lt;sub style=&quot;&quot;&gt;1&lt;/sub&gt;:&amp;nbsp;¬x&lt;sub&gt;1&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨ &lt;i&gt;x&lt;sub&gt;2&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;¬x&lt;sub&gt;4&lt;/sub&gt;&amp;nbsp;&lt;br&gt;c&lt;sub&gt;2&lt;/sub&gt;:&amp;nbsp;¬x&lt;sub&gt;1&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;¬x&lt;sub&gt;2&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub&gt;3&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;¬x&lt;sub&gt;4&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub&gt;5&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub&gt;6&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;sub&gt;5&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;span style=&quot;font-style: italic;&quot;&gt;&lt;sub&gt;6&lt;/sub&gt;&lt;/span&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;6&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;x&lt;sub&gt;7&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;¬x&lt;sub&gt;8&lt;/sub&gt;&lt;/i&gt;&lt;/font&gt;&lt;font face=&quot;Computer modern&quot;&gt;&lt;br&gt;&lt;/font&gt;" style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="60" y="-90" width="230" height="180" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-5" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;1&lt;/sub&gt;@1&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="570" y="210" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-6" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;8&lt;/sub&gt;@2&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="400" y="250" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-7" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;7&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="400" y="360" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-8" value="&lt;font style=&quot;font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i&gt;c&lt;sub style=&quot;&quot;&gt;1&lt;/sub&gt;:&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;1&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨ &lt;i&gt;x&lt;sub&gt;2&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;¬x&lt;sub&gt;4&lt;/sub&gt;&amp;nbsp;&lt;br&gt;c&lt;sub&gt;2&lt;/sub&gt;:&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;1&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;¬x&lt;sub&gt;2&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub&gt;3&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;¬x&lt;sub&gt;4&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub style=&quot;&quot;&gt;5&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;6&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;¬x&lt;sub&gt;5&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;span style=&quot;font-style: italic;&quot;&gt;&lt;sub&gt;6&lt;/sub&gt;&lt;/span&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;¬x&lt;/font&gt;&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;&lt;font color=&quot;#009900&quot;&gt;6&lt;/font&gt;&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;8&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;/font&gt;&lt;font face=&quot;Computer modern&quot;&gt;&lt;br&gt;&lt;/font&gt;" style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="150" y="480" width="200" height="180" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-9" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;1&lt;/sub&gt;@1&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="570" y="470" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-10" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;8&lt;/sub&gt;@2&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="400" y="510" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-11" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;7&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="400" y="620" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-14" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;6&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="500" y="530" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-15" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="500" y="610" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-16" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-10" target="mCqeTS5OQJ7wAlwwDYhK-14">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="440" y="610" as="sourcePoint" />
<mxPoint x="490" y="560" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-20" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-16">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-17" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-11" target="mCqeTS5OQJ7wAlwwDYhK-15">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="470" y="546" as="sourcePoint" />
<mxPoint x="530" y="565" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-19" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;5&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-17">
<mxGeometry x="0.035" y="-2" relative="1" as="geometry">
<mxPoint y="3" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-21" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-11" target="mCqeTS5OQJ7wAlwwDYhK-14">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="470" y="546" as="sourcePoint" />
<mxPoint x="530" y="565" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-22" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-21">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-11" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-36" value="&lt;font style=&quot;font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i&gt;c&lt;sub style=&quot;&quot;&gt;1&lt;/sub&gt;:&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;1&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨ &lt;i&gt;&lt;font color=&quot;#009900&quot;&gt;x&lt;sub&gt;2&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;4&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;br&gt;c&lt;sub&gt;2&lt;/sub&gt;:&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;1&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;2&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;3&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;¬x&lt;/font&gt;&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;&lt;font color=&quot;#009900&quot;&gt;3&lt;/font&gt;&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;4&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;x&lt;/font&gt;&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;&lt;font color=&quot;#009900&quot;&gt;4&lt;/font&gt;&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub style=&quot;&quot;&gt;5&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;6&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;¬x&lt;sub&gt;5&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;span style=&quot;font-style: italic;&quot;&gt;&lt;sub&gt;6&lt;/sub&gt;&lt;/span&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;¬x&lt;/font&gt;&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;&lt;font color=&quot;#009900&quot;&gt;6&lt;/font&gt;&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;8&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;/font&gt;&lt;font face=&quot;Computer modern&quot;&gt;&lt;br&gt;&lt;/font&gt;" style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="150" y="760" width="200" height="180" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-37" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;1&lt;/sub&gt;@1&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="570" y="750" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-38" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;8&lt;/sub&gt;@2&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="400" y="790" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-39" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;7&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="400" y="900" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-40" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;6&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="500" y="810" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-41" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="500" y="890" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-42" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-38" target="mCqeTS5OQJ7wAlwwDYhK-40">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="440" y="890" as="sourcePoint" />
<mxPoint x="490" y="840" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-43" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-42">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-44" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-39" target="mCqeTS5OQJ7wAlwwDYhK-41">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="470" y="826" as="sourcePoint" />
<mxPoint x="530" y="845" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-45" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;5&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-44">
<mxGeometry x="0.035" y="-2" relative="1" as="geometry">
<mxPoint y="3" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-46" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-39" target="mCqeTS5OQJ7wAlwwDYhK-40">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="470" y="826" as="sourcePoint" />
<mxPoint x="530" y="845" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-47" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-46">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-11" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-48" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="590" y="850" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-49" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-40" target="mCqeTS5OQJ7wAlwwDYhK-48">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="470" y="826" as="sourcePoint" />
<mxPoint x="510" y="835" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-50" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;4&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-49">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-51" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-41" target="mCqeTS5OQJ7wAlwwDYhK-48">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="570" y="846" as="sourcePoint" />
<mxPoint x="610" y="864" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-52" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;4&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-51">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="4" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-53" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;2&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="680" y="810" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-54" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="680" y="890" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-55" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-48" target="mCqeTS5OQJ7wAlwwDYhK-53">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="570" y="846" as="sourcePoint" />
<mxPoint x="610" y="864" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-56" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;1&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-55">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-10" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-57" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-48" target="mCqeTS5OQJ7wAlwwDYhK-54">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="660" y="864" as="sourcePoint" />
<mxPoint x="700" y="846" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-58" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;3&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-57">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-3" y="3" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-59" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0.106;entryY=0.126;entryDx=0;entryDy=0;entryPerimeter=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-37" target="mCqeTS5OQJ7wAlwwDYhK-53">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="660" y="864" as="sourcePoint" />
<mxPoint x="700" y="846" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-60" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;1&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-59">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-61" value="&lt;font style=&quot;font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i&gt;c&lt;sub style=&quot;&quot;&gt;1&lt;/sub&gt;:&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;1&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨ &lt;i&gt;&lt;font color=&quot;#009900&quot;&gt;x&lt;sub&gt;2&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;4&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;br&gt;c&lt;sub&gt;2&lt;/sub&gt;:&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;1&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;2&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;3&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;¬x&lt;/font&gt;&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;&lt;font color=&quot;#009900&quot;&gt;3&lt;/font&gt;&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;4&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;x&lt;/font&gt;&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;&lt;font color=&quot;#009900&quot;&gt;4&lt;/font&gt;&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub style=&quot;&quot;&gt;5&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;6&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;¬x&lt;sub&gt;5&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;span style=&quot;font-style: italic;&quot;&gt;&lt;sub&gt;6&lt;/sub&gt;&lt;/span&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;¬x&lt;/font&gt;&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;&lt;font color=&quot;#009900&quot;&gt;6&lt;/font&gt;&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;8&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;/font&gt;&lt;font face=&quot;Computer modern&quot;&gt;&lt;br&gt;&lt;/font&gt;" style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="160" y="1020" width="200" height="180" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-62" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;1&lt;/sub&gt;@1&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="580" y="1010" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-63" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;8&lt;/sub&gt;@2&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="410" y="1050" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-64" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;7&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="410" y="1160" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-65" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;6&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="510" y="1070" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-66" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="510" y="1150" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-67" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-63" target="mCqeTS5OQJ7wAlwwDYhK-65">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="450" y="1150" as="sourcePoint" />
<mxPoint x="500" y="1100" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-68" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-67">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-69" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-64" target="mCqeTS5OQJ7wAlwwDYhK-66">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="480" y="1086" as="sourcePoint" />
<mxPoint x="540" y="1105" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-70" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;5&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-69">
<mxGeometry x="0.035" y="-2" relative="1" as="geometry">
<mxPoint y="3" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-71" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-64" target="mCqeTS5OQJ7wAlwwDYhK-65">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="480" y="1086" as="sourcePoint" />
<mxPoint x="540" y="1105" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-72" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-71">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-11" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-73" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="600" y="1110" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-74" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-65" target="mCqeTS5OQJ7wAlwwDYhK-73">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="480" y="1086" as="sourcePoint" />
<mxPoint x="520" y="1095" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-75" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;4&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-74">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-76" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-66" target="mCqeTS5OQJ7wAlwwDYhK-73">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="580" y="1106" as="sourcePoint" />
<mxPoint x="620" y="1124" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-77" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;4&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-76">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="4" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-78" value="&lt;font style=&quot;font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i style=&quot;border-color: var(--border-color);&quot;&gt;x&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-style: italic;&quot;&gt;2&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="690" y="1070" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-79" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font style=&quot;border-color: var(--border-color); font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i style=&quot;border-color: var(--border-color);&quot;&gt;x&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-style: italic;&quot;&gt;3&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="690" y="1150" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-80" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-73" target="mCqeTS5OQJ7wAlwwDYhK-78">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="580" y="1106" as="sourcePoint" />
<mxPoint x="620" y="1124" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-81" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;1&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-80">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-10" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-82" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-73" target="mCqeTS5OQJ7wAlwwDYhK-79">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="670" y="1124" as="sourcePoint" />
<mxPoint x="710" y="1106" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-83" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;3&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-82">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-3" y="3" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-84" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0.106;entryY=0.126;entryDx=0;entryDy=0;entryPerimeter=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-62" target="mCqeTS5OQJ7wAlwwDYhK-78">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="670" y="1124" as="sourcePoint" />
<mxPoint x="710" y="1106" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-85" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;1&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-84">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-88" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;κ&lt;/i&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#FFCCCC;verticalAlign=middle;labelPosition=center;verticalLabelPosition=middle;align=center;" vertex="1" parent="1">
<mxGeometry x="790" y="1110" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-89" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-78" target="mCqeTS5OQJ7wAlwwDYhK-88">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="790" y="1040" as="sourcePoint" />
<mxPoint x="847" y="1078" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-90" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left;&quot;&gt;&lt;font size=&quot;1&quot;&gt;2&lt;/font&gt;&lt;/i&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-89">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-91" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-79" target="mCqeTS5OQJ7wAlwwDYhK-88">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="760" y="1106" as="sourcePoint" />
<mxPoint x="810" y="1124" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-92" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left;&quot;&gt;&lt;font size=&quot;1&quot;&gt;2&lt;/font&gt;&lt;/i&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-91">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="4" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-93" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;entryX=0.5;entryY=0;entryDx=0;entryDy=0;curved=1;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-62" target="mCqeTS5OQJ7wAlwwDYhK-88">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="760" y="1106" as="sourcePoint" />
<mxPoint x="810" y="1124" as="targetPoint" />
<Array as="points">
<mxPoint x="770" y="1020" />
</Array>
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-94" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left;&quot;&gt;&lt;font size=&quot;1&quot;&gt;2&lt;/font&gt;&lt;/i&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-93">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="1" y="9" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-96" value="&lt;font color=&quot;#ffffff&quot;&gt;Text&lt;/font&gt;" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="840" y="790" width="20" height="80" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-97" value="&lt;font color=&quot;#ffffff&quot;&gt;Text&lt;/font&gt;" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="840" y="510" width="20" height="80" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-98" value="&lt;font color=&quot;#ffffff&quot;&gt;Text&lt;/font&gt;" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="840" y="290" width="20" height="80" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-99" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;1&lt;/sub&gt;@1&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="500" y="1370" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-100" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;8&lt;/sub&gt;@2&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="330" y="1410" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-101" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;7&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="330" y="1520" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-102" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;6&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="430" y="1430" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-103" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="430" y="1510" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-104" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-100" target="mCqeTS5OQJ7wAlwwDYhK-102">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="370" y="1510" as="sourcePoint" />
<mxPoint x="420" y="1460" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-105" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-104">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-106" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-101" target="mCqeTS5OQJ7wAlwwDYhK-103">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="400" y="1446" as="sourcePoint" />
<mxPoint x="460" y="1465" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-107" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;5&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-106">
<mxGeometry x="0.035" y="-2" relative="1" as="geometry">
<mxPoint y="3" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-108" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-101" target="mCqeTS5OQJ7wAlwwDYhK-102">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="400" y="1446" as="sourcePoint" />
<mxPoint x="460" y="1465" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-109" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-108">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-11" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-110" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="520" y="1470" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-111" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-102" target="mCqeTS5OQJ7wAlwwDYhK-110">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="400" y="1446" as="sourcePoint" />
<mxPoint x="440" y="1455" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-112" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;4&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-111">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-113" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-103" target="mCqeTS5OQJ7wAlwwDYhK-110">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="500" y="1466" as="sourcePoint" />
<mxPoint x="540" y="1484" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-114" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;4&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-113">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="4" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-115" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i style=&quot;border-color: var(--border-color);&quot;&gt;x&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-style: italic;&quot;&gt;2&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="610" y="1430" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-116" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font style=&quot;border-color: var(--border-color); font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i style=&quot;border-color: var(--border-color);&quot;&gt;x&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-style: italic;&quot;&gt;3&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="610" y="1510" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-117" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-110" target="mCqeTS5OQJ7wAlwwDYhK-115">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="500" y="1466" as="sourcePoint" />
<mxPoint x="540" y="1484" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-118" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;1&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-117">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-10" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-119" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-110" target="mCqeTS5OQJ7wAlwwDYhK-116">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="590" y="1484" as="sourcePoint" />
<mxPoint x="630" y="1466" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-120" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;3&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-119">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-3" y="3" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-121" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0.106;entryY=0.126;entryDx=0;entryDy=0;entryPerimeter=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-99" target="mCqeTS5OQJ7wAlwwDYhK-115">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="590" y="1484" as="sourcePoint" />
<mxPoint x="630" y="1466" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-122" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;1&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-121">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-123" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;κ&lt;/i&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#FFCCCC;verticalAlign=middle;labelPosition=center;verticalLabelPosition=middle;align=center;" vertex="1" parent="1">
<mxGeometry x="710" y="1470" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-124" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-115" target="mCqeTS5OQJ7wAlwwDYhK-123">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="710" y="1400" as="sourcePoint" />
<mxPoint x="767" y="1438" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-125" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left;&quot;&gt;&lt;font size=&quot;1&quot;&gt;2&lt;/font&gt;&lt;/i&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-124">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-126" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-116" target="mCqeTS5OQJ7wAlwwDYhK-123">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="680" y="1466" as="sourcePoint" />
<mxPoint x="730" y="1484" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-127" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left;&quot;&gt;&lt;font size=&quot;1&quot;&gt;2&lt;/font&gt;&lt;/i&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-126">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="4" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-128" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;entryX=0.5;entryY=0;entryDx=0;entryDy=0;curved=1;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-99" target="mCqeTS5OQJ7wAlwwDYhK-123">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="680" y="1466" as="sourcePoint" />
<mxPoint x="730" y="1484" as="targetPoint" />
<Array as="points">
<mxPoint x="690" y="1380" />
</Array>
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-129" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left;&quot;&gt;&lt;font size=&quot;1&quot;&gt;2&lt;/font&gt;&lt;/i&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-128">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="1" y="9" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-131" value="" style="endArrow=none;dashed=1;html=1;rounded=0;curved=1;strokeColor=#3399FF;strokeWidth=2;entryX=0.75;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" target="mCqeTS5OQJ7wAlwwDYhK-133">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="420" y="1560" as="sourcePoint" />
<mxPoint x="590" y="1350" as="targetPoint" />
<Array as="points">
<mxPoint x="380" y="1360" />
<mxPoint x="600" y="1470" />
</Array>
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-133" value="&lt;font color=&quot;#3399ff&quot;&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬x&lt;sub&gt;1&amp;nbsp;&lt;/sub&gt;&lt;/i&gt;&lt;span style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;∨&lt;/span&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt; x&lt;sub&gt;7&amp;nbsp;&lt;/sub&gt;&lt;/i&gt;&lt;span style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;∨&lt;/span&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;&amp;nbsp;&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬x&lt;sub&gt;8&lt;/sub&gt;&lt;/i&gt;&lt;/font&gt;" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="500" y="1320" width="130" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-135" value="" style="endArrow=none;dashed=1;html=1;rounded=0;strokeWidth=2;curved=1;strokeColor=#CC0000;entryX=0.25;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" target="mCqeTS5OQJ7wAlwwDYhK-137">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="610" y="1560" as="sourcePoint" />
<mxPoint x="670" y="1360" as="targetPoint" />
<Array as="points">
<mxPoint x="590" y="1450" />
<mxPoint x="620" y="1400" />
</Array>
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-137" value="&lt;font color=&quot;#cc0000&quot;&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬x&lt;sub style=&quot;&quot;&gt;1&amp;nbsp;&lt;/sub&gt;&lt;/i&gt;&lt;span style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;∨&lt;/span&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt; &lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬x&lt;sub style=&quot;&quot;&gt;4&lt;/sub&gt;&lt;/i&gt;&lt;/font&gt;" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="640" y="1340" width="130" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-138" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;1&lt;/sub&gt;@1&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="660" y="1700" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-139" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;8&lt;/sub&gt;@2&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="490" y="1740" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-140" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;7&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="490" y="1850" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-141" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;6&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="590" y="1760" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-142" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="590" y="1840" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-143" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-139" target="mCqeTS5OQJ7wAlwwDYhK-141">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="530" y="1840" as="sourcePoint" />
<mxPoint x="580" y="1790" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-144" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-143">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-145" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-140" target="mCqeTS5OQJ7wAlwwDYhK-142">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="560" y="1776" as="sourcePoint" />
<mxPoint x="620" y="1795" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-146" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;5&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-145">
<mxGeometry x="0.035" y="-2" relative="1" as="geometry">
<mxPoint y="3" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-147" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-140" target="mCqeTS5OQJ7wAlwwDYhK-141">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="560" y="1776" as="sourcePoint" />
<mxPoint x="620" y="1795" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-148" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-147">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-11" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-149" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="680" y="1800" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-150" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-141" target="mCqeTS5OQJ7wAlwwDYhK-149">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="560" y="1776" as="sourcePoint" />
<mxPoint x="600" y="1785" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-151" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;4&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-150">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-152" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-142" target="mCqeTS5OQJ7wAlwwDYhK-149">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="660" y="1796" as="sourcePoint" />
<mxPoint x="700" y="1814" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-153" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;4&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-152">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="4" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-154" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;2&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="770" y="1760" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-155" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font style=&quot;border-color: var(--border-color); font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i style=&quot;border-color: var(--border-color);&quot;&gt;x&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-style: italic;&quot;&gt;3&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="770" y="1840" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-156" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-149" target="mCqeTS5OQJ7wAlwwDYhK-154">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="660" y="1796" as="sourcePoint" />
<mxPoint x="700" y="1814" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-157" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;1&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-156">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-10" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-158" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-149" target="mCqeTS5OQJ7wAlwwDYhK-155">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="750" y="1814" as="sourcePoint" />
<mxPoint x="790" y="1796" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-159" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;3&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-158">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-3" y="3" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-160" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0.106;entryY=0.126;entryDx=0;entryDy=0;entryPerimeter=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-138" target="mCqeTS5OQJ7wAlwwDYhK-154">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="750" y="1814" as="sourcePoint" />
<mxPoint x="790" y="1796" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-161" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;1&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-160">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-162" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;κ&lt;/i&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#FFCCCC;verticalAlign=middle;labelPosition=center;verticalLabelPosition=middle;align=center;" vertex="1" parent="1">
<mxGeometry x="870" y="1800" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-163" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-154" target="mCqeTS5OQJ7wAlwwDYhK-162">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="870" y="1730" as="sourcePoint" />
<mxPoint x="927" y="1768" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-164" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left;&quot;&gt;&lt;font size=&quot;1&quot;&gt;2&lt;/font&gt;&lt;/i&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-163">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-165" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-155" target="mCqeTS5OQJ7wAlwwDYhK-162">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="840" y="1796" as="sourcePoint" />
<mxPoint x="890" y="1814" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-166" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left;&quot;&gt;&lt;font size=&quot;1&quot;&gt;2&lt;/font&gt;&lt;/i&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-165">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="4" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-167" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;entryX=0.5;entryY=0;entryDx=0;entryDy=0;curved=1;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-138" target="mCqeTS5OQJ7wAlwwDYhK-162">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="840" y="1796" as="sourcePoint" />
<mxPoint x="890" y="1814" as="targetPoint" />
<Array as="points">
<mxPoint x="850" y="1710" />
</Array>
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-168" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left;&quot;&gt;&lt;font size=&quot;1&quot;&gt;2&lt;/font&gt;&lt;/i&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-167">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="1" y="9" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-171" value="" style="endArrow=none;dashed=1;html=1;rounded=0;strokeWidth=2;curved=1;strokeColor=#CC0000;entryX=0.25;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" target="mCqeTS5OQJ7wAlwwDYhK-172">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="770" y="1890" as="sourcePoint" />
<mxPoint x="830" y="1690" as="targetPoint" />
<Array as="points">
<mxPoint x="750" y="1780" />
<mxPoint x="780" y="1730" />
</Array>
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-172" value="&lt;font color=&quot;#cc0000&quot;&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬x&lt;sub style=&quot;&quot;&gt;1&amp;nbsp;&lt;/sub&gt;&lt;/i&gt;&lt;span style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;∨&lt;/span&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt; &lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬x&lt;sub style=&quot;&quot;&gt;4&lt;/sub&gt;&lt;/i&gt;&lt;/font&gt;" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="800" y="1670" width="130" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-173" value="&lt;font style=&quot;font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i&gt;c&lt;sub style=&quot;&quot;&gt;1&lt;/sub&gt;:&amp;nbsp;¬x&lt;sub&gt;1&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨ &lt;i&gt;x&lt;sub&gt;2&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;¬x&lt;sub&gt;4&lt;/sub&gt;&amp;nbsp;&lt;br&gt;c&lt;sub&gt;2&lt;/sub&gt;:&amp;nbsp;¬x&lt;sub&gt;1&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;¬x&lt;sub&gt;2&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub&gt;3&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;¬x&lt;sub&gt;4&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub style=&quot;&quot;&gt;5&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub&gt;6&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;sub&gt;5&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;span style=&quot;font-style: italic;&quot;&gt;&lt;sub&gt;6&lt;/sub&gt;&lt;/span&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;6&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;x&lt;sub&gt;7&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;¬x&lt;sub style=&quot;&quot;&gt;8&lt;br&gt;&lt;/sub&gt;&lt;/i&gt;&lt;/font&gt;&lt;b&gt;&lt;u&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px;&quot;&gt;:&amp;nbsp;&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px;&quot;&gt;¬x&lt;sub style=&quot;border-color: var(--border-color);&quot;&gt;1&amp;nbsp;&lt;/sub&gt;&lt;/i&gt;&lt;span style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px;&quot;&gt;∨&lt;/span&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px;&quot;&gt;&amp;nbsp;&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px;&quot;&gt;¬x&lt;sub style=&quot;border-color: var(--border-color);&quot;&gt;4&lt;/sub&gt;&lt;/i&gt;&lt;/u&gt;&lt;/b&gt;&lt;font face=&quot;Computer modern&quot;&gt;&lt;br&gt;&lt;/font&gt;" style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="260" y="1680" width="200" height="210" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-174" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 18px;&quot;&gt;(1UIP)&lt;/font&gt;" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="685" y="1830" width="60" height="30" as="geometry" />
</mxCell>
</root>
</mxGraphModel>
</diagram>
</mxfile>

115
src/combinatorial-decision-making-and-optimization/sections/_sat.tex
View File

@ -117,7 +117,7 @@
\section{DPLL}
\section{DPLL algorithm}
\begin{description}
\item[DPLL] \marginnote{DPLL}
@ -203,4 +203,117 @@
\end{descriptionlist}
In the end, if the formula is SAT, $M$ contains an assignment of the variables.
\end{description}
\begin{remark}
Compared to resolution, DPLL is more memory efficient.
\end{remark}
\section{Conflict-driven clause learning (CDCL)}
DPLL with two improvements:
\begin{descriptionlist}
\item[Clause learning]
When a contradiction is found, augment the original CNF with a conflict clause
to prune the search space.
The conflict clause is obtained through resolution by combining two clauses that cause the contradiction.
\item[\texttt{Backjumping}]
Depending on the type of contradiction, skip decision literals that are not causing the conflict
and directly backtrack to an earlier relevant decision literal.
Given a clause $C$ of the CNF, if $Ml^\mathcal{D}N \models \lnot C$ and
there is a clause $(C' \vee l')$ derivable from the CNF such that $M \models \lnot C'$ and
$l'$ is undefined, then there is a transition:
\[ Ml^\mathcal{D}N \rightarrow Ml' \]
Note that $N$ might contain other decision literals and $(C' \vee l')$ is a conflict clause.
\begin{remark}
\texttt{Backjumping} can be seen as \texttt{UnitPropagate} applied on conflict clauses.
\end{remark}
\end{descriptionlist}
\begin{description}
\item[Implication graph]
DAG $G=(V, E)$ to record the history of decisions and unit resolutions.
\begin{descriptionlist}
\item[Vertex] Can be:
\begin{itemize}
\item A decision or derived literal (denoted as $l@d$, where $l$ is the literal and $d$ the decision level it originated from).
\item A marker to indicate a conflict (denoted as $\kappa@d$, where $d$ is the decision level it originated from).
\end{itemize}
\item[Edge]
Has form $v \xrightarrow{c_i} w$ and indicates that $w$ is obtained using the clause $c_i$ and the literal $v$.
\end{descriptionlist}
\begin{example}
Starting from the clauses $c_1, \dots, c_6$ of a CNF, one can build the implication graph while running DPLL/CDCL.
In this example, the decision literals (green nodes) are assigned following this order: $x_1 \rightarrow x_8 \rightarrow \lnot x_7$:
\begin{center}
\includegraphics[width=0.8\linewidth]{./img/_cdcl_example1.pdf}
\end{center}
\[ M \rightarrow M x_1^\mathcal{D} x_8^\mathcal{D} \lnot x_7^\mathcal{D} \]
Then, it is possible to derive implied variables using unit resolution starting from the decision literals:
\begin{center}
\includegraphics[width=0.8\linewidth]{./img/_cdcl_example2.pdf}
\end{center}
\[ M \rightarrow M \lnot x_6 \lnot x_5 \]
And so on:
\begin{center}
\includegraphics[width=0.8\linewidth]{./img/_cdcl_example3.pdf}
\end{center}
\[ M \rightarrow M x_4 x_2 \lnot x_3 \]
As $c_2$ is UNSAT, we reached a contradiction:
\begin{center}
\includegraphics[width=0.8\linewidth]{./img/_cdcl_example4.pdf}
\end{center}
\end{example}
\begin{remark}
Any cut that separates sources (decision literals) and the sink (contradiction node) is a valid conflict clause for backjumping.
\begin{example} \phantom{}
\begin{center}
\includegraphics[width=0.55\linewidth]{./img/_cdcl_cut.pdf}
\end{center}
\end{example}
\end{remark}
\item[Unit implication point (UIP)]
Given an implication graph where the latest decision node is $(l@d)$ and the conflict node is $(\kappa@d)$,
a node is a unit implication point iff it appears in all the paths from $(l@d)$ to $(\kappa@d)$.
The UIP closest to the conflict is denoted as 1UIP.
\begin{remark}
The decision node $(l@d)$ itself is a UIP.
\end{remark}
\item[1UIP-based backjumping]
In case of conflict, use the conflict clause obtained by cutting in front of the 1UIP.
\begin{remark}
This allows to:
\begin{itemize}
\item Reduce the size of the conflict clause.
\item Guarantee the highest backtrack jump.
\end{itemize}
\end{remark}
\begin{example}
\phantom{}
\begin{center}
\includegraphics[width=0.75\linewidth]{./img/_cdcl_1uip.pdf}
\end{center}
By adding the conflict clause $(\lnot x_1 \vee \lnot x_4)$, we can backjump up to $x_8^\mathcal{D}$
(not to $x_1^\mathcal{D}$ as it makes the conflict clause a unit).
\[ x_1^\mathcal{D} x_8^\mathcal{D} \lnot x_7^\mathcal{D} \lnot x_6 \lnot x_5 x_4 x_2 \lnot x_3 \rightarrow x_1^\mathcal{D} \lnot x_4\]
\end{example}
\end{description}