Left Termination proof of /tmp/tmpge5Xrc/delete-bfb.pl

Left Termination of the query pattern delete_in_3(g, a, g) w.r.t. the given Prolog program could successfully be proven:

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇐)

↳2 TRIPLES

↳3 TriplesToPiDPProof (⇐)

↳4 PiDP

↳5 DependencyGraphProof (⇔)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇔)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇐)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔)

        ↳20 YES

    ↳21 PiDP

        ↳22 PiDPToQDPProof (⇐)

        ↳23 QDP

        ↳24 QDPSizeChangeProof (⇔)

        ↳25 YES

(0) Obligation:

Clauses:

delete(X, tree(X, void, Right), Right).
delete(X, tree(X, Left, void), Left).
delete(X, tree(X, Left, Right), tree(Y, Left, Right1)) :- delmin(Right, Y, Right1).
delete(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), delete(X, Left, Left1)).
delete(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), delete(X, Right, Right1)).
delmin(tree(Y, void, Right), Y, Right).
delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1).
less(0, s(X3)).
less(s(X), s(Y)) :- less(X, Y).

Queries:

delete(g,a,g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: delete(T1, T2, T3)\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | delete(T6, T2, T7), SCOPE: 1, CLAUSE: 1 | delete(T6, T2, T7), SCOPE: 1, CLAUSE: 2 | delete(T6, T2, T7), SCOPE: 1, CLAUSE: 3 | delete(T6, T2, T7), SCOPE: 1, CLAUSE: 4\n\nT6 is ground\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT3 is ground\ndelete(T1, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: delete(T6, T2, T7), SCOPE: 1, CLAUSE: 1 | delete(T6, T2, T7), SCOPE: 1, CLAUSE: 2 | delete(T6, T2, T7), SCOPE: 1, CLAUSE: 3 | delete(T6, T2, T7), SCOPE: 1, CLAUSE: 4\n\nT6 is ground\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: true | delete(T10, T2, T11), SCOPE: 1, CLAUSE: 2 | delete(T10, T2, T11), SCOPE: 1, CLAUSE: 3 | delete(T10, T2, T11), SCOPE: 1, CLAUSE: 4\n\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: delete(T6, T2, T7), SCOPE: 1, CLAUSE: 2 | delete(T6, T2, T7), SCOPE: 1, CLAUSE: 3 | delete(T6, T2, T7), SCOPE: 1, CLAUSE: 4\n\nT6 is ground\nT7 is ground\ndelete(T6, T2, T7) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: delete(T10, T2, T11), SCOPE: 1, CLAUSE: 2 | delete(T10, T2, T11), SCOPE: 1, CLAUSE: 3 | delete(T10, T2, T11), SCOPE: 1, CLAUSE: 4\n\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: delmin(T22, T20, T21) | delete(T17, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 3 | delete(T17, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 4\n\nT17 is ground\nT20 is ground\nT18 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: delete(T10, T2, T11), SCOPE: 1, CLAUSE: 3 | delete(T10, T2, T11), SCOPE: 1, CLAUSE: 4\n\nT10 is ground\nT11 is ground\ndelete(T10, T2, T11) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: delmin(T22, T20, T21), SCOPE: 2, CLAUSE: 5 | delmin(T22, T20, T21), SCOPE: 2, CLAUSE: 6 | ?_2 | delete(T17, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 3 | delete(T17, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 4\n\nT17 is ground\nT20 is ground\nT18 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: delmin(T22, T20, T21), SCOPE: 2, CLAUSE: 5\n\nT20 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: delmin(T22, T20, T21), SCOPE: 2, CLAUSE: 6 | ?_2 | delete(T17, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 3 | delete(T17, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 4\n\nT17 is ground\nT20 is ground\nT18 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: delmin(T22, T20, T21), SCOPE: 2, CLAUSE: 6\n\nT20 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ?_2 | delete(T17, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 3 | delete(T17, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 4\n\nT17 is ground\nT20 is ground\nT18 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: delmin(T63, T60, T61)\n\nT60 is ground\nT61 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: delmin(T63, T60, T61), SCOPE: 3, CLAUSE: 5 | delmin(T63, T60, T61), SCOPE: 3, CLAUSE: 6\n\nT60 is ground\nT61 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: delmin(T63, T60, T61), SCOPE: 3, CLAUSE: 5\n\nT60 is ground\nT61 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: delmin(T63, T60, T61), SCOPE: 3, CLAUSE: 6\n\nT60 is ground\nT61 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: delmin(T96, T93, T94)\n\nT93 is ground\nT94 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: delete(T17, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 3 | delete(T17, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 4\n\nT17 is ground\nT20 is ground\nT18 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: delete(T17, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 3\n\nT17 is ground\nT20 is ground\nT18 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: delete(T17, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 4\n\nT17 is ground\nT20 is ground\nT18 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(less(T121, T122), delete(T121, T126, T125))\n\nT121 is ground\nT122 is ground\nT125 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: less(T121, T122)\n\nT121 is ground\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: delete(T121, T126, T125)\n\nT121 is ground\nT125 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: less(T121, T122), SCOPE: 4, CLAUSE: 7 | less(T121, T122), SCOPE: 4, CLAUSE: 8\n\nT121 is ground\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: less(T121, T122), SCOPE: 4, CLAUSE: 7\n\nT121 is ground\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: less(T121, T122), SCOPE: 4, CLAUSE: 8\n\nT121 is ground\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: less(T140, T141)\n\nT140 is ground\nT141 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(less(T159, T158), delete(T158, T163, T162))\n\nT158 is ground\nT159 is ground\nT162 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: less(T159, T158)\n\nT158 is ground\nT159 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: delete(T158, T163, T162)\n\nT158 is ground\nT162 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(less(T177, T178), delete(T177, T182, T181)) | delete(T177, T2, tree(T178, T181, T180)), SCOPE: 1, CLAUSE: 4\n\nT177 is ground\nT178 is ground\nT181 is ground\nT180 is ground\ndelete(T177, T2, tree(T178, T181, T180)) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: delete(T10, T2, T11), SCOPE: 1, CLAUSE: 4\n\nT10 is ground\nT11 is ground\ndelete(T10, T2, T11) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))\ndelete(T10, T2, T11) !=? delete(X210, tree(X211, X212, X213), tree(X211, X214, X213))", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(less(T177, T178), delete(T177, T182, T181)), SCOPE: 5, CLAUSE: 7 | ','(less(T177, T178), delete(T177, T182, T181)), SCOPE: 5, CLAUSE: 8 | ?_5 | delete(T177, T2, tree(T178, T181, T180)), SCOPE: 1, CLAUSE: 4\n\nT177 is ground\nT178 is ground\nT181 is ground\nT180 is ground\ndelete(T177, T2, tree(T178, T181, T180)) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(less(T177, T178), delete(T177, T182, T181)), SCOPE: 5, CLAUSE: 7\n\nT177 is ground\nT178 is ground\nT181 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ','(less(T177, T178), delete(T177, T182, T181)), SCOPE: 5, CLAUSE: 8 | ?_5 | delete(T177, T2, tree(T178, T181, T180)), SCOPE: 1, CLAUSE: 4\n\nT177 is ground\nT178 is ground\nT181 is ground\nT180 is ground\ndelete(T177, T2, tree(T178, T181, T180)) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: delete(0, T182, T181)\n\nT181 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(less(T177, T178), delete(T177, T182, T181)), SCOPE: 5, CLAUSE: 8\n\nT177 is ground\nT178 is ground\nT181 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ?_5 | delete(T177, T2, tree(T178, T181, T180)), SCOPE: 1, CLAUSE: 4\n\nT177 is ground\nT178 is ground\nT181 is ground\nT180 is ground\ndelete(T177, T2, tree(T178, T181, T180)) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(less(T198, T199), delete(s(T198), T182, T181))\n\nT181 is ground\nT198 is ground\nT199 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: less(T198, T199)\n\nT198 is ground\nT199 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: delete(s(T198), T182, T181)\n\nT181 is ground\nT198 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: delete(T177, T2, tree(T178, T181, T180)), SCOPE: 1, CLAUSE: 4\n\nT177 is ground\nT178 is ground\nT181 is ground\nT180 is ground\ndelete(T177, T2, tree(T178, T181, T180)) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(less(T219, T218), delete(T218, T223, T222))\n\nT218 is ground\nT219 is ground\nT222 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(less(T232, T231), delete(T231, T236, T235))\n\nT231 is ground\nT232 is ground\nT235 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(less(T232, T231), delete(T231, T236, T235)), SCOPE: 6, CLAUSE: 7 | ','(less(T232, T231), delete(T231, T236, T235)), SCOPE: 6, CLAUSE: 8\n\nT231 is ground\nT232 is ground\nT235 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(less(T232, T231), delete(T231, T236, T235)), SCOPE: 6, CLAUSE: 7\n\nT231 is ground\nT232 is ground\nT235 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(less(T232, T231), delete(T231, T236, T235)), SCOPE: 6, CLAUSE: 8\n\nT231 is ground\nT232 is ground\nT235 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: delete(s(T241), T236, T235)\n\nT235 is ground\nT241 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(less(T250, T251), delete(s(T251), T236, T235))\n\nT235 is ground\nT250 is ground\nT251 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: less(T250, T251)\n\nT250 is ground\nT251 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: delete(s(T251), T236, T235)\n\nT235 is ground\nT251 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: delmin(T270, T268, T269) | delete(T265, T2, tree(T268, T266, T269)), SCOPE: 1, CLAUSE: 3 | delete(T265, T2, tree(T268, T266, T269)), SCOPE: 1, CLAUSE: 4\n\nT265 is ground\nT268 is ground\nT266 is ground\nT269 is ground\ndelete(T265, T2, tree(T268, T266, T269)) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: delete(T6, T2, T7), SCOPE: 1, CLAUSE: 3 | delete(T6, T2, T7), SCOPE: 1, CLAUSE: 4\n\nT6 is ground\nT7 is ground\ndelete(T6, T2, T7) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T6, T2, T7) !=? delete(X318, tree(X318, X319, X320), tree(X321, X319, X322))", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: delmin(T270, T268, T269), SCOPE: 7, CLAUSE: 5 | delmin(T270, T268, T269), SCOPE: 7, CLAUSE: 6 | ?_7 | delete(T265, T2, tree(T268, T266, T269)), SCOPE: 1, CLAUSE: 3 | delete(T265, T2, tree(T268, T266, T269)), SCOPE: 1, CLAUSE: 4\n\nT265 is ground\nT268 is ground\nT266 is ground\nT269 is ground\ndelete(T265, T2, tree(T268, T266, T269)) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: delmin(T270, T268, T269), SCOPE: 7, CLAUSE: 5\n\nT268 is ground\nT269 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: delmin(T270, T268, T269), SCOPE: 7, CLAUSE: 6 | ?_7 | delete(T265, T2, tree(T268, T266, T269)), SCOPE: 1, CLAUSE: 3 | delete(T265, T2, tree(T268, T266, T269)), SCOPE: 1, CLAUSE: 4\n\nT265 is ground\nT268 is ground\nT266 is ground\nT269 is ground\ndelete(T265, T2, tree(T268, T266, T269)) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: delmin(T270, T268, T269), SCOPE: 7, CLAUSE: 6\n\nT268 is ground\nT269 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ?_7 | delete(T265, T2, tree(T268, T266, T269)), SCOPE: 1, CLAUSE: 3 | delete(T265, T2, tree(T268, T266, T269)), SCOPE: 1, CLAUSE: 4\n\nT265 is ground\nT268 is ground\nT266 is ground\nT269 is ground\ndelete(T265, T2, tree(T268, T266, T269)) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: delmin(T311, T308, T309)\n\nT308 is ground\nT309 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: delete(T265, T2, tree(T268, T266, T269)), SCOPE: 1, CLAUSE: 3 | delete(T265, T2, tree(T268, T266, T269)), SCOPE: 1, CLAUSE: 4\n\nT265 is ground\nT268 is ground\nT266 is ground\nT269 is ground\ndelete(T265, T2, tree(T268, T266, T269)) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: delete(T265, T2, tree(T268, T266, T269)), SCOPE: 1, CLAUSE: 3\n\nT265 is ground\nT268 is ground\nT266 is ground\nT269 is ground\ndelete(T265, T2, tree(T268, T266, T269)) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: delete(T265, T2, tree(T268, T266, T269)), SCOPE: 1, CLAUSE: 4\n\nT265 is ground\nT268 is ground\nT266 is ground\nT269 is ground\ndelete(T265, T2, tree(T268, T266, T269)) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(less(T336, T337), delete(T336, T341, T340))\n\nT336 is ground\nT337 is ground\nT340 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(less(T355, T354), delete(T354, T359, T358))\n\nT354 is ground\nT355 is ground\nT358 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(less(T367, T368), delete(T367, T372, T371)) | delete(T367, T2, tree(T368, T371, T370)), SCOPE: 1, CLAUSE: 4\n\nT367 is ground\nT368 is ground\nT371 is ground\nT370 is ground\ndelete(T367, T2, tree(T368, T371, T370)) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T367, T2, tree(T368, T371, T370)) !=? delete(X318, tree(X318, X319, X320), tree(X321, X319, X322))", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: delete(T6, T2, T7), SCOPE: 1, CLAUSE: 4\n\nT6 is ground\nT7 is ground\ndelete(T6, T2, T7) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T6, T2, T7) !=? delete(X318, tree(X318, X319, X320), tree(X321, X319, X322))\ndelete(T6, T2, T7) !=? delete(X439, tree(X440, X441, X442), tree(X440, X443, X442))", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(less(T367, T368), delete(T367, T372, T371)), SCOPE: 8, CLAUSE: 7 | ','(less(T367, T368), delete(T367, T372, T371)), SCOPE: 8, CLAUSE: 8 | ?_8 | delete(T367, T2, tree(T368, T371, T370)), SCOPE: 1, CLAUSE: 4\n\nT367 is ground\nT368 is ground\nT371 is ground\nT370 is ground\ndelete(T367, T2, tree(T368, T371, T370)) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T367, T2, tree(T368, T371, T370)) !=? delete(X318, tree(X318, X319, X320), tree(X321, X319, X322))", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(less(T367, T368), delete(T367, T372, T371)), SCOPE: 8, CLAUSE: 7\n\nT367 is ground\nT368 is ground\nT371 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(less(T367, T368), delete(T367, T372, T371)), SCOPE: 8, CLAUSE: 8 | ?_8 | delete(T367, T2, tree(T368, T371, T370)), SCOPE: 1, CLAUSE: 4\n\nT367 is ground\nT368 is ground\nT371 is ground\nT370 is ground\ndelete(T367, T2, tree(T368, T371, T370)) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T367, T2, tree(T368, T371, T370)) !=? delete(X318, tree(X318, X319, X320), tree(X321, X319, X322))", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: delete(0, T372, T371)\n\nT371 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(less(T367, T368), delete(T367, T372, T371)), SCOPE: 8, CLAUSE: 8\n\nT367 is ground\nT368 is ground\nT371 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ?_8 | delete(T367, T2, tree(T368, T371, T370)), SCOPE: 1, CLAUSE: 4\n\nT367 is ground\nT368 is ground\nT371 is ground\nT370 is ground\ndelete(T367, T2, tree(T368, T371, T370)) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T367, T2, tree(T368, T371, T370)) !=? delete(X318, tree(X318, X319, X320), tree(X321, X319, X322))", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ','(less(T388, T389), delete(s(T388), T372, T371))\n\nT371 is ground\nT388 is ground\nT389 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: delete(T367, T2, tree(T368, T371, T370)), SCOPE: 1, CLAUSE: 4\n\nT367 is ground\nT368 is ground\nT371 is ground\nT370 is ground\ndelete(T367, T2, tree(T368, T371, T370)) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T367, T2, tree(T368, T371, T370)) !=? delete(X318, tree(X318, X319, X320), tree(X321, X319, X322))", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(less(T403, T402), delete(T402, T407, T406))\n\nT402 is ground\nT403 is ground\nT406 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(less(T416, T415), delete(T415, T420, T419))\n\nT415 is ground\nT416 is ground\nT419 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(less(T416, T415), delete(T415, T420, T419)), SCOPE: 9, CLAUSE: 7 | ','(less(T416, T415), delete(T415, T420, T419)), SCOPE: 9, CLAUSE: 8\n\nT415 is ground\nT416 is ground\nT419 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(less(T416, T415), delete(T415, T420, T419)), SCOPE: 9, CLAUSE: 7\n\nT415 is ground\nT416 is ground\nT419 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(less(T416, T415), delete(T415, T420, T419)), SCOPE: 9, CLAUSE: 8\n\nT415 is ground\nT416 is ground\nT419 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: delete(s(T425), T420, T419)\n\nT419 is ground\nT425 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(less(T434, T435), delete(s(T435), T420, T419))\n\nT419 is ground\nT434 is ground\nT435 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: true | delete(T440, T2, T441), SCOPE: 1, CLAUSE: 2 | delete(T440, T2, T441), SCOPE: 1, CLAUSE: 3 | delete(T440, T2, T441), SCOPE: 1, CLAUSE: 4\n\nT440 is ground\nT441 is ground\ndelete(T440, T2, T441) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT3 is ground\ndelete(T1, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, T3) !=? delete(X532, tree(X532, X533, void), X533)", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: delete(T440, T2, T441), SCOPE: 1, CLAUSE: 2 | delete(T440, T2, T441), SCOPE: 1, CLAUSE: 3 | delete(T440, T2, T441), SCOPE: 1, CLAUSE: 4\n\nT440 is ground\nT441 is ground\ndelete(T440, T2, T441) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: delmin(T452, T450, T451) | delete(T447, T2, tree(T450, T448, T451)), SCOPE: 1, CLAUSE: 3 | delete(T447, T2, tree(T450, T448, T451)), SCOPE: 1, CLAUSE: 4\n\nT447 is ground\nT450 is ground\nT448 is ground\nT451 is ground\ndelete(T447, T2, tree(T450, T448, T451)) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: delete(T440, T2, T441), SCOPE: 1, CLAUSE: 3 | delete(T440, T2, T441), SCOPE: 1, CLAUSE: 4\n\nT440 is ground\nT441 is ground\ndelete(T440, T2, T441) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T440, T2, T441) !=? delete(X541, tree(X541, X542, X543), tree(X544, X542, X545))", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: delmin(T452, T450, T451), SCOPE: 10, CLAUSE: 5 | delmin(T452, T450, T451), SCOPE: 10, CLAUSE: 6 | ?_10 | delete(T447, T2, tree(T450, T448, T451)), SCOPE: 1, CLAUSE: 3 | delete(T447, T2, tree(T450, T448, T451)), SCOPE: 1, CLAUSE: 4\n\nT447 is ground\nT450 is ground\nT448 is ground\nT451 is ground\ndelete(T447, T2, tree(T450, T448, T451)) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: delmin(T452, T450, T451), SCOPE: 10, CLAUSE: 5\n\nT450 is ground\nT451 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: delmin(T452, T450, T451), SCOPE: 10, CLAUSE: 6 | ?_10 | delete(T447, T2, tree(T450, T448, T451)), SCOPE: 1, CLAUSE: 3 | delete(T447, T2, tree(T450, T448, T451)), SCOPE: 1, CLAUSE: 4\n\nT447 is ground\nT450 is ground\nT448 is ground\nT451 is ground\ndelete(T447, T2, tree(T450, T448, T451)) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: delmin(T452, T450, T451), SCOPE: 10, CLAUSE: 6\n\nT450 is ground\nT451 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ?_10 | delete(T447, T2, tree(T450, T448, T451)), SCOPE: 1, CLAUSE: 3 | delete(T447, T2, tree(T450, T448, T451)), SCOPE: 1, CLAUSE: 4\n\nT447 is ground\nT450 is ground\nT448 is ground\nT451 is ground\ndelete(T447, T2, tree(T450, T448, T451)) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: delmin(T493, T490, T491)\n\nT490 is ground\nT491 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: delete(T447, T2, tree(T450, T448, T451)), SCOPE: 1, CLAUSE: 3 | delete(T447, T2, tree(T450, T448, T451)), SCOPE: 1, CLAUSE: 4\n\nT447 is ground\nT450 is ground\nT448 is ground\nT451 is ground\ndelete(T447, T2, tree(T450, T448, T451)) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: delete(T447, T2, tree(T450, T448, T451)), SCOPE: 1, CLAUSE: 3\n\nT447 is ground\nT450 is ground\nT448 is ground\nT451 is ground\ndelete(T447, T2, tree(T450, T448, T451)) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: delete(T447, T2, tree(T450, T448, T451)), SCOPE: 1, CLAUSE: 4\n\nT447 is ground\nT450 is ground\nT448 is ground\nT451 is ground\ndelete(T447, T2, tree(T450, T448, T451)) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ','(less(T518, T519), delete(T518, T523, T522))\n\nT518 is ground\nT519 is ground\nT522 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ','(less(T537, T536), delete(T536, T541, T540))\n\nT536 is ground\nT537 is ground\nT540 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: ','(less(T549, T550), delete(T549, T554, T553)) | delete(T549, T2, tree(T550, T553, T552)), SCOPE: 1, CLAUSE: 4\n\nT549 is ground\nT550 is ground\nT553 is ground\nT552 is ground\ndelete(T549, T2, tree(T550, T553, T552)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T549, T2, tree(T550, T553, T552)) !=? delete(X541, tree(X541, X542, X543), tree(X544, X542, X545))", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: delete(T440, T2, T441), SCOPE: 1, CLAUSE: 4\n\nT440 is ground\nT441 is ground\ndelete(T440, T2, T441) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T440, T2, T441) !=? delete(X541, tree(X541, X542, X543), tree(X544, X542, X545))\ndelete(T440, T2, T441) !=? delete(X662, tree(X663, X664, X665), tree(X663, X666, X665))", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: ','(less(T549, T550), delete(T549, T554, T553)), SCOPE: 11, CLAUSE: 7 | ','(less(T549, T550), delete(T549, T554, T553)), SCOPE: 11, CLAUSE: 8 | ?_11 | delete(T549, T2, tree(T550, T553, T552)), SCOPE: 1, CLAUSE: 4\n\nT549 is ground\nT550 is ground\nT553 is ground\nT552 is ground\ndelete(T549, T2, tree(T550, T553, T552)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T549, T2, tree(T550, T553, T552)) !=? delete(X541, tree(X541, X542, X543), tree(X544, X542, X545))", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: ','(less(T549, T550), delete(T549, T554, T553)), SCOPE: 11, CLAUSE: 7\n\nT549 is ground\nT550 is ground\nT553 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ','(less(T549, T550), delete(T549, T554, T553)), SCOPE: 11, CLAUSE: 8 | ?_11 | delete(T549, T2, tree(T550, T553, T552)), SCOPE: 1, CLAUSE: 4\n\nT549 is ground\nT550 is ground\nT553 is ground\nT552 is ground\ndelete(T549, T2, tree(T550, T553, T552)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T549, T2, tree(T550, T553, T552)) !=? delete(X541, tree(X541, X542, X543), tree(X544, X542, X545))", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: delete(0, T554, T553)\n\nT553 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: ','(less(T549, T550), delete(T549, T554, T553)), SCOPE: 11, CLAUSE: 8\n\nT549 is ground\nT550 is ground\nT553 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: ?_11 | delete(T549, T2, tree(T550, T553, T552)), SCOPE: 1, CLAUSE: 4\n\nT549 is ground\nT550 is ground\nT553 is ground\nT552 is ground\ndelete(T549, T2, tree(T550, T553, T552)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T549, T2, tree(T550, T553, T552)) !=? delete(X541, tree(X541, X542, X543), tree(X544, X542, X545))", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: ','(less(T570, T571), delete(s(T570), T554, T553))\n\nT553 is ground\nT570 is ground\nT571 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: delete(T549, T2, tree(T550, T553, T552)), SCOPE: 1, CLAUSE: 4\n\nT549 is ground\nT550 is ground\nT553 is ground\nT552 is ground\ndelete(T549, T2, tree(T550, T553, T552)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T549, T2, tree(T550, T553, T552)) !=? delete(X541, tree(X541, X542, X543), tree(X544, X542, X545))", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: ','(less(T585, T584), delete(T584, T589, T588))\n\nT584 is ground\nT585 is ground\nT588 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: ','(less(T598, T597), delete(T597, T602, T601))\n\nT597 is ground\nT598 is ground\nT601 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: ','(less(T598, T597), delete(T597, T602, T601)), SCOPE: 12, CLAUSE: 7 | ','(less(T598, T597), delete(T597, T602, T601)), SCOPE: 12, CLAUSE: 8\n\nT597 is ground\nT598 is ground\nT601 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: ','(less(T598, T597), delete(T597, T602, T601)), SCOPE: 12, CLAUSE: 7\n\nT597 is ground\nT598 is ground\nT601 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: ','(less(T598, T597), delete(T597, T602, T601)), SCOPE: 12, CLAUSE: 8\n\nT597 is ground\nT598 is ground\nT601 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: delete(s(T607), T602, T601)\n\nT601 is ground\nT607 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: ','(less(T616, T617), delete(s(T617), T602, T601))\n\nT601 is ground\nT616 is ground\nT617 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: delmin(T630, T628, T629) | delete(T625, T2, tree(T628, T626, T629)), SCOPE: 1, CLAUSE: 3 | delete(T625, T2, tree(T628, T626, T629)), SCOPE: 1, CLAUSE: 4\n\nT625 is ground\nT628 is ground\nT626 is ground\nT629 is ground\ndelete(T625, T2, tree(T628, T626, T629)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T625, T2, tree(T628, T626, T629)) !=? delete(X532, tree(X532, X533, void), X533)", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT3 is ground\ndelete(T1, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, T3) !=? delete(X532, tree(X532, X533, void), X533)\ndelete(T1, T2, T3) !=? delete(X758, tree(X758, X759, X760), tree(X761, X759, X762))", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: delmin(T630, T628, T629), SCOPE: 13, CLAUSE: 5 | delmin(T630, T628, T629), SCOPE: 13, CLAUSE: 6 | ?_13 | delete(T625, T2, tree(T628, T626, T629)), SCOPE: 1, CLAUSE: 3 | delete(T625, T2, tree(T628, T626, T629)), SCOPE: 1, CLAUSE: 4\n\nT625 is ground\nT628 is ground\nT626 is ground\nT629 is ground\ndelete(T625, T2, tree(T628, T626, T629)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T625, T2, tree(T628, T626, T629)) !=? delete(X532, tree(X532, X533, void), X533)", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: delmin(T630, T628, T629), SCOPE: 13, CLAUSE: 5\n\nT628 is ground\nT629 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: delmin(T630, T628, T629), SCOPE: 13, CLAUSE: 6 | ?_13 | delete(T625, T2, tree(T628, T626, T629)), SCOPE: 1, CLAUSE: 3 | delete(T625, T2, tree(T628, T626, T629)), SCOPE: 1, CLAUSE: 4\n\nT625 is ground\nT628 is ground\nT626 is ground\nT629 is ground\ndelete(T625, T2, tree(T628, T626, T629)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T625, T2, tree(T628, T626, T629)) !=? delete(X532, tree(X532, X533, void), X533)", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: delmin(T630, T628, T629), SCOPE: 13, CLAUSE: 6\n\nT628 is ground\nT629 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: ?_13 | delete(T625, T2, tree(T628, T626, T629)), SCOPE: 1, CLAUSE: 3 | delete(T625, T2, tree(T628, T626, T629)), SCOPE: 1, CLAUSE: 4\n\nT625 is ground\nT628 is ground\nT626 is ground\nT629 is ground\ndelete(T625, T2, tree(T628, T626, T629)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T625, T2, tree(T628, T626, T629)) !=? delete(X532, tree(X532, X533, void), X533)", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: delmin(T671, T668, T669)\n\nT668 is ground\nT669 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: delete(T625, T2, tree(T628, T626, T629)), SCOPE: 1, CLAUSE: 3 | delete(T625, T2, tree(T628, T626, T629)), SCOPE: 1, CLAUSE: 4\n\nT625 is ground\nT628 is ground\nT626 is ground\nT629 is ground\ndelete(T625, T2, tree(T628, T626, T629)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T625, T2, tree(T628, T626, T629)) !=? delete(X532, tree(X532, X533, void), X533)", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: delete(T625, T2, tree(T628, T626, T629)), SCOPE: 1, CLAUSE: 3\n\nT625 is ground\nT628 is ground\nT626 is ground\nT629 is ground\ndelete(T625, T2, tree(T628, T626, T629)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T625, T2, tree(T628, T626, T629)) !=? delete(X532, tree(X532, X533, void), X533)", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: delete(T625, T2, tree(T628, T626, T629)), SCOPE: 1, CLAUSE: 4\n\nT625 is ground\nT628 is ground\nT626 is ground\nT629 is ground\ndelete(T625, T2, tree(T628, T626, T629)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T625, T2, tree(T628, T626, T629)) !=? delete(X532, tree(X532, X533, void), X533)", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: ','(less(T696, T697), delete(T696, T701, T700))\n\nT696 is ground\nT697 is ground\nT700 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: ','(less(T715, T714), delete(T714, T719, T718))\n\nT714 is ground\nT715 is ground\nT718 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: ','(less(T727, T728), delete(T727, T732, T731)) | delete(T727, T2, tree(T728, T731, T730)), SCOPE: 1, CLAUSE: 4\n\nT727 is ground\nT728 is ground\nT731 is ground\nT730 is ground\ndelete(T727, T2, tree(T728, T731, T730)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T727, T2, tree(T728, T731, T730)) !=? delete(X532, tree(X532, X533, void), X533)\ndelete(T727, T2, tree(T728, T731, T730)) !=? delete(X758, tree(X758, X759, X760), tree(X761, X759, X762))", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT3 is ground\ndelete(T1, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, T3) !=? delete(X532, tree(X532, X533, void), X533)\ndelete(T1, T2, T3) !=? delete(X758, tree(X758, X759, X760), tree(X761, X759, X762))\ndelete(T1, T2, T3) !=? delete(X879, tree(X880, X881, X882), tree(X880, X883, X882))", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: ','(less(T727, T728), delete(T727, T732, T731)), SCOPE: 14, CLAUSE: 7 | ','(less(T727, T728), delete(T727, T732, T731)), SCOPE: 14, CLAUSE: 8 | ?_14 | delete(T727, T2, tree(T728, T731, T730)), SCOPE: 1, CLAUSE: 4\n\nT727 is ground\nT728 is ground\nT731 is ground\nT730 is ground\ndelete(T727, T2, tree(T728, T731, T730)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T727, T2, tree(T728, T731, T730)) !=? delete(X532, tree(X532, X533, void), X533)\ndelete(T727, T2, tree(T728, T731, T730)) !=? delete(X758, tree(X758, X759, X760), tree(X761, X759, X762))", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: ','(less(T727, T728), delete(T727, T732, T731)), SCOPE: 14, CLAUSE: 7\n\nT727 is ground\nT728 is ground\nT731 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: ','(less(T727, T728), delete(T727, T732, T731)), SCOPE: 14, CLAUSE: 8 | ?_14 | delete(T727, T2, tree(T728, T731, T730)), SCOPE: 1, CLAUSE: 4\n\nT727 is ground\nT728 is ground\nT731 is ground\nT730 is ground\ndelete(T727, T2, tree(T728, T731, T730)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T727, T2, tree(T728, T731, T730)) !=? delete(X532, tree(X532, X533, void), X533)\ndelete(T727, T2, tree(T728, T731, T730)) !=? delete(X758, tree(X758, X759, X760), tree(X761, X759, X762))", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: delete(0, T732, T731)\n\nT731 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: ','(less(T727, T728), delete(T727, T732, T731)), SCOPE: 14, CLAUSE: 8\n\nT727 is ground\nT728 is ground\nT731 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: ?_14 | delete(T727, T2, tree(T728, T731, T730)), SCOPE: 1, CLAUSE: 4\n\nT727 is ground\nT728 is ground\nT731 is ground\nT730 is ground\ndelete(T727, T2, tree(T728, T731, T730)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T727, T2, tree(T728, T731, T730)) !=? delete(X532, tree(X532, X533, void), X533)\ndelete(T727, T2, tree(T728, T731, T730)) !=? delete(X758, tree(X758, X759, X760), tree(X761, X759, X762))", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: ','(less(T748, T749), delete(s(T748), T732, T731))\n\nT731 is ground\nT748 is ground\nT749 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: delete(T727, T2, tree(T728, T731, T730)), SCOPE: 1, CLAUSE: 4\n\nT727 is ground\nT728 is ground\nT731 is ground\nT730 is ground\ndelete(T727, T2, tree(T728, T731, T730)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T727, T2, tree(T728, T731, T730)) !=? delete(X532, tree(X532, X533, void), X533)\ndelete(T727, T2, tree(T728, T731, T730)) !=? delete(X758, tree(X758, X759, X760), tree(X761, X759, X762))", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(less(T763, T762), delete(T762, T767, T766))\n\nT762 is ground\nT763 is ground\nT766 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: ','(less(T776, T775), delete(T775, T780, T779))\n\nT775 is ground\nT776 is ground\nT779 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: ','(less(T776, T775), delete(T775, T780, T779)), SCOPE: 15, CLAUSE: 7 | ','(less(T776, T775), delete(T775, T780, T779)), SCOPE: 15, CLAUSE: 8\n\nT775 is ground\nT776 is ground\nT779 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: ','(less(T776, T775), delete(T775, T780, T779)), SCOPE: 15, CLAUSE: 7\n\nT775 is ground\nT776 is ground\nT779 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: ','(less(T776, T775), delete(T775, T780, T779)), SCOPE: 15, CLAUSE: 8\n\nT775 is ground\nT776 is ground\nT779 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: delete(s(T785), T780, T779)\n\nT779 is ground\nT785 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: ','(less(T794, T795), delete(s(T795), T780, T779))\n\nT779 is ground\nT794 is ground\nT795 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 204 [arrowhead = none ];
204 -> 2;

205 [label="EVAL with clause\ndelete(X6, tree(X6, void, X7), X7).\nand substitution\nT1 -> T6\nX6 -> T6\nX7 -> T7\nT2 -> tree(T6, void, T7)\nT3 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 205 [arrowhead = none ];
205 -> 3;

206 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 206 [arrowhead = none ];
206 -> 4;

207 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 207 [arrowhead = none ];
207 -> 5;

208 [label="EVAL with clause\ndelete(X532, tree(X532, X533, void), X533).\nand substitution\nT1 -> T440\nX532 -> T440\nX533 -> T441\nT2 -> tree(T440, T441, void)\nT3 -> T441", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 208 [arrowhead = none ];
208 -> 117;

209 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 209 [arrowhead = none ];
209 -> 118;

210 [label="EVAL with clause\ndelete(X12, tree(X12, X13, void), X13).\nand substitution\nT6 -> T10\nX12 -> T10\nX13 -> T11\nT2 -> tree(T10, T11, void)\nT7 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 210 [arrowhead = none ];
210 -> 6;

211 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 211 [arrowhead = none ];
211 -> 7;

212 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 212 [arrowhead = none ];
212 -> 8;

213 [label="EVAL with clause\ndelete(X318, tree(X318, X319, X320), tree(X321, X319, X322)) :- delmin(X320, X321, X322).\nand substitution\nT6 -> T265\nX318 -> T265\nX319 -> T266\nX320 -> T270\nT2 -> tree(T265, T266, T270)\nX321 -> T268\nX322 -> T269\nT7 -> tree(T268, T266, T269)\nT267 -> T270", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 213 [arrowhead = none ];
213 -> 75;

214 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 214 [arrowhead = none ];
214 -> 76;

215 [label="EVAL with clause\ndelete(X21, tree(X21, X22, X23), tree(X24, X22, X25)) :- delmin(X23, X24, X25).\nand substitution\nT10 -> T17\nX21 -> T17\nX22 -> T18\nX23 -> T22\nT2 -> tree(T17, T18, T22)\nX24 -> T20\nX25 -> T21\nT11 -> tree(T20, T18, T21)\nT19 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 215 [arrowhead = none ];
215 -> 9;

216 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 216 [arrowhead = none ];
216 -> 10;

217 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
9 -> 217 [arrowhead = none ];
217 -> 11;

218 [label="EVAL with clause\ndelete(X210, tree(X211, X212, X213), tree(X211, X214, X213)) :- ','(less(X210, X211), delete(X210, X212, X214)).\nand substitution\nT10 -> T177\nX210 -> T177\nX211 -> T178\nX212 -> T182\nX213 -> T180\nT2 -> tree(T178, T182, T180)\nX214 -> T181\nT11 -> tree(T178, T181, T180)\nT179 -> T182", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 218 [arrowhead = none ];
218 -> 48;

219 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 219 [arrowhead = none ];
219 -> 49;

220 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
11 -> 220 [arrowhead = none ];
220 -> 12;

221 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
11 -> 221 [arrowhead = none ];
221 -> 13;

222 [label="EVAL with clause\ndelmin(tree(X39, void, X40), X39, X40).\nand substitution\nX39 -> T31\nX40 -> T32\nT22 -> tree(T31, void, T32)\nT20 -> T31\nT21 -> T32", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 222 [arrowhead = none ];
222 -> 14;

223 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 223 [arrowhead = none ];
223 -> 15;

224 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
13 -> 224 [arrowhead = none ];
224 -> 17;

225 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
13 -> 225 [arrowhead = none ];
225 -> 18;

226 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
14 -> 226 [arrowhead = none ];
226 -> 16;

227 [label="EVAL with clause\ndelmin(tree(X67, X68, X69), X70, tree(X67, X71, X72)) :- delmin(X68, X70, X71).\nand substitution\nX67 -> T57\nX68 -> T63\nX69 -> T59\nT22 -> tree(T57, T63, T59)\nT20 -> T60\nX70 -> T60\nX71 -> T61\nX72 -> T62\nT21 -> tree(T57, T61, T62)\nT58 -> T63", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 227 [arrowhead = none ];
227 -> 19;

228 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 228 [arrowhead = none ];
228 -> 20;

229 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 229 [arrowhead = none ];
229 -> 29;

230 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
19 -> 230 [arrowhead = none ];
230 -> 21;

231 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
21 -> 231 [arrowhead = none ];
231 -> 22;

232 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
21 -> 232 [arrowhead = none ];
232 -> 23;

233 [label="EVAL with clause\ndelmin(tree(X91, void, X92), X91, X92).\nand substitution\nX91 -> T76\nX92 -> T77\nT63 -> tree(T76, void, T77)\nT60 -> T76\nT61 -> T77", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 233 [arrowhead = none ];
233 -> 24;

234 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 234 [arrowhead = none ];
234 -> 25;

235 [label="EVAL with clause\ndelmin(tree(X107, X108, X109), X110, tree(X107, X111, X112)) :- delmin(X108, X110, X111).\nand substitution\nX107 -> T90\nX108 -> T96\nX109 -> T92\nT63 -> tree(T90, T96, T92)\nT60 -> T93\nX110 -> T93\nX111 -> T94\nX112 -> T95\nT61 -> tree(T90, T94, T95)\nT91 -> T96", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 235 [arrowhead = none ];
235 -> 27;

236 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 236 [arrowhead = none ];
236 -> 28;

237 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 237 [arrowhead = none ];
237 -> 26;

238 [label="INSTANCE with matching:\nT63 -> T96\nT60 -> T93\nT61 -> T94", fontsize=14, style = filled, fillcolor = lightgrey];
27 -> 238 [arrowhead = none , style=dashed];
238 -> 19[style=dashed];

239 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
29 -> 239 [arrowhead = none ];
239 -> 30;

240 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
29 -> 240 [arrowhead = none ];
240 -> 31;

241 [label="EVAL with clause\ndelete(X143, tree(X144, X145, X146), tree(X144, X147, X146)) :- ','(less(X143, X144), delete(X143, X145, X147)).\nand substitution\nT17 -> T121\nX143 -> T121\nX144 -> T122\nX145 -> T126\nX146 -> T124\nT2 -> tree(T122, T126, T124)\nT20 -> T122\nT18 -> T125\nX147 -> T125\nT21 -> T124\nT123 -> T126", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 241 [arrowhead = none ];
241 -> 32;

242 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 242 [arrowhead = none ];
242 -> 33;

243 [label="EVAL with clause\ndelete(X187, tree(X188, X189, X190), tree(X188, X189, X191)) :- ','(less(X188, X187), delete(X187, X190, X191)).\nand substitution\nT17 -> T158\nX187 -> T158\nX188 -> T159\nX189 -> T160\nX190 -> T163\nT2 -> tree(T159, T160, T163)\nT20 -> T159\nT18 -> T160\nT21 -> T162\nX191 -> T162\nT161 -> T163", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 243 [arrowhead = none ];
243 -> 44;

244 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 244 [arrowhead = none ];
244 -> 45;

245 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
32 -> 245 [arrowhead = none ];
245 -> 34;

246 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
32 -> 246 [arrowhead = none ];
246 -> 35;

247 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
34 -> 247 [arrowhead = none ];
247 -> 36;

248 [label="INSTANCE with matching:\nT1 -> T121\nT2 -> T126\nT3 -> T125", fontsize=14, style = filled, fillcolor = lightgrey];
35 -> 248 [arrowhead = none , style=dashed];
248 -> 1[style=dashed];

249 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
36 -> 249 [arrowhead = none ];
249 -> 37;

250 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
36 -> 250 [arrowhead = none ];
250 -> 38;

251 [label="EVAL with clause\nless(0, s(X161)).\nand substitution\nT121 -> 0\nX161 -> T135\nT122 -> s(T135)", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 251 [arrowhead = none ];
251 -> 39;

252 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 252 [arrowhead = none ];
252 -> 40;

253 [label="EVAL with clause\nless(s(X167), s(X168)) :- less(X167, X168).\nand substitution\nX167 -> T140\nT121 -> s(T140)\nX168 -> T141\nT122 -> s(T141)", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 253 [arrowhead = none ];
253 -> 42;

254 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 254 [arrowhead = none ];
254 -> 43;

255 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 255 [arrowhead = none ];
255 -> 41;

256 [label="INSTANCE with matching:\nT121 -> T140\nT122 -> T141", fontsize=14, style = filled, fillcolor = lightgrey];
42 -> 256 [arrowhead = none , style=dashed];
256 -> 34[style=dashed];

257 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
44 -> 257 [arrowhead = none ];
257 -> 46;

258 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
44 -> 258 [arrowhead = none ];
258 -> 47;

259 [label="INSTANCE with matching:\nT121 -> T159\nT122 -> T158", fontsize=14, style = filled, fillcolor = lightgrey];
46 -> 259 [arrowhead = none , style=dashed];
259 -> 34[style=dashed];

260 [label="INSTANCE with matching:\nT1 -> T158\nT2 -> T163\nT3 -> T162", fontsize=14, style = filled, fillcolor = lightgrey];
47 -> 260 [arrowhead = none , style=dashed];
260 -> 1[style=dashed];

261 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
48 -> 261 [arrowhead = none ];
261 -> 50;

262 [label="EVAL with clause\ndelete(X277, tree(X278, X279, X280), tree(X278, X279, X281)) :- ','(less(X278, X277), delete(X277, X280, X281)).\nand substitution\nT10 -> T231\nX277 -> T231\nX278 -> T232\nX279 -> T233\nX280 -> T236\nT2 -> tree(T232, T233, T236)\nX281 -> T235\nT11 -> tree(T232, T233, T235)\nT234 -> T236", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 262 [arrowhead = none ];
262 -> 64;

263 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 263 [arrowhead = none ];
263 -> 65;

264 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
50 -> 264 [arrowhead = none ];
264 -> 51;

265 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
50 -> 265 [arrowhead = none ];
265 -> 52;

266 [label="EVAL with clause\nless(0, s(X224)).\nand substitution\nT177 -> 0\nX224 -> T187\nT178 -> s(T187)", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 266 [arrowhead = none ];
266 -> 53;

267 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 267 [arrowhead = none ];
267 -> 54;

268 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
52 -> 268 [arrowhead = none ];
268 -> 55;

269 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
52 -> 269 [arrowhead = none ];
269 -> 56;

270 [label="INSTANCE with matching:\nT1 -> 0\nT2 -> T182\nT3 -> T181", fontsize=14, style = filled, fillcolor = lightgrey];
53 -> 270 [arrowhead = none , style=dashed];
270 -> 1[style=dashed];

271 [label="EVAL with clause\nless(s(X238), s(X239)) :- less(X238, X239).\nand substitution\nX238 -> T198\nT177 -> s(T198)\nX239 -> T199\nT178 -> s(T199)", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 271 [arrowhead = none ];
271 -> 57;

272 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 272 [arrowhead = none ];
272 -> 58;

273 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
56 -> 273 [arrowhead = none ];
273 -> 61;

274 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
57 -> 274 [arrowhead = none ];
274 -> 59;

275 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
57 -> 275 [arrowhead = none ];
275 -> 60;

276 [label="INSTANCE with matching:\nT121 -> T198\nT122 -> T199", fontsize=14, style = filled, fillcolor = lightgrey];
59 -> 276 [arrowhead = none , style=dashed];
276 -> 34[style=dashed];

277 [label="INSTANCE with matching:\nT1 -> s(T198)\nT2 -> T182\nT3 -> T181", fontsize=14, style = filled, fillcolor = lightgrey];
60 -> 277 [arrowhead = none , style=dashed];
277 -> 1[style=dashed];

278 [label="EVAL with clause\ndelete(X260, tree(X261, X262, X263), tree(X261, X262, X264)) :- ','(less(X261, X260), delete(X260, X263, X264)).\nand substitution\nT177 -> T218\nX260 -> T218\nX261 -> T219\nX262 -> T220\nX263 -> T223\nT2 -> tree(T219, T220, T223)\nT178 -> T219\nT181 -> T220\nT180 -> T222\nX264 -> T222\nT221 -> T223", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 278 [arrowhead = none ];
278 -> 62;

279 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 279 [arrowhead = none ];
279 -> 63;

280 [label="INSTANCE with matching:\nT159 -> T219\nT158 -> T218\nT163 -> T223\nT162 -> T222", fontsize=14, style = filled, fillcolor = lightgrey];
62 -> 280 [arrowhead = none , style=dashed];
280 -> 44[style=dashed];

281 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
64 -> 281 [arrowhead = none ];
281 -> 66;

282 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
66 -> 282 [arrowhead = none ];
282 -> 67;

283 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
66 -> 283 [arrowhead = none ];
283 -> 68;

284 [label="EVAL with clause\nless(0, s(X291)).\nand substitution\nT232 -> 0\nX291 -> T241\nT231 -> s(T241)", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 284 [arrowhead = none ];
284 -> 69;

285 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 285 [arrowhead = none ];
285 -> 70;

286 [label="EVAL with clause\nless(s(X301), s(X302)) :- less(X301, X302).\nand substitution\nX301 -> T250\nT232 -> s(T250)\nX302 -> T251\nT231 -> s(T251)", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 286 [arrowhead = none ];
286 -> 71;

287 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 287 [arrowhead = none ];
287 -> 72;

288 [label="INSTANCE with matching:\nT1 -> s(T241)\nT2 -> T236\nT3 -> T235", fontsize=14, style = filled, fillcolor = lightgrey];
69 -> 288 [arrowhead = none , style=dashed];
288 -> 1[style=dashed];

289 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
71 -> 289 [arrowhead = none ];
289 -> 73;

290 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
71 -> 290 [arrowhead = none ];
290 -> 74;

291 [label="INSTANCE with matching:\nT198 -> T250\nT199 -> T251", fontsize=14, style = filled, fillcolor = lightgrey];
73 -> 291 [arrowhead = none , style=dashed];
291 -> 59[style=dashed];

292 [label="INSTANCE with matching:\nT1 -> s(T251)\nT2 -> T236\nT3 -> T235", fontsize=14, style = filled, fillcolor = lightgrey];
74 -> 292 [arrowhead = none , style=dashed];
292 -> 1[style=dashed];

293 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
75 -> 293 [arrowhead = none ];
293 -> 77;

294 [label="EVAL with clause\ndelete(X439, tree(X440, X441, X442), tree(X440, X443, X442)) :- ','(less(X439, X440), delete(X439, X441, X443)).\nand substitution\nT6 -> T367\nX439 -> T367\nX440 -> T368\nX441 -> T372\nX442 -> T370\nT2 -> tree(T368, T372, T370)\nX443 -> T371\nT7 -> tree(T368, T371, T370)\nT369 -> T372", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 294 [arrowhead = none ];
294 -> 94;

295 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 295 [arrowhead = none ];
295 -> 95;

296 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
77 -> 296 [arrowhead = none ];
296 -> 78;

297 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
77 -> 297 [arrowhead = none ];
297 -> 79;

298 [label="EVAL with clause\ndelmin(tree(X336, void, X337), X336, X337).\nand substitution\nX336 -> T279\nX337 -> T280\nT270 -> tree(T279, void, T280)\nT268 -> T279\nT269 -> T280", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 298 [arrowhead = none ];
298 -> 80;

299 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 299 [arrowhead = none ];
299 -> 81;

300 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
79 -> 300 [arrowhead = none ];
300 -> 83;

301 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
79 -> 301 [arrowhead = none ];
301 -> 84;

302 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 302 [arrowhead = none ];
302 -> 82;

303 [label="EVAL with clause\ndelmin(tree(X364, X365, X366), X367, tree(X364, X368, X369)) :- delmin(X365, X367, X368).\nand substitution\nX364 -> T305\nX365 -> T311\nX366 -> T307\nT270 -> tree(T305, T311, T307)\nT268 -> T308\nX367 -> T308\nX368 -> T309\nX369 -> T310\nT269 -> tree(T305, T309, T310)\nT306 -> T311", fontsize=14, style = filled, fillcolor = lightblue];
83 -> 303 [arrowhead = none ];
303 -> 85;

304 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
83 -> 304 [arrowhead = none ];
304 -> 86;

305 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
84 -> 305 [arrowhead = none ];
305 -> 87;

306 [label="INSTANCE with matching:\nT63 -> T311\nT60 -> T308\nT61 -> T309", fontsize=14, style = filled, fillcolor = lightgrey];
85 -> 306 [arrowhead = none , style=dashed];
306 -> 19[style=dashed];

307 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
87 -> 307 [arrowhead = none ];
307 -> 88;

308 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
87 -> 308 [arrowhead = none ];
308 -> 89;

309 [label="EVAL with clause\ndelete(X400, tree(X401, X402, X403), tree(X401, X404, X403)) :- ','(less(X400, X401), delete(X400, X402, X404)).\nand substitution\nT265 -> T336\nX400 -> T336\nX401 -> T337\nX402 -> T341\nX403 -> T339\nT2 -> tree(T337, T341, T339)\nT268 -> T337\nT266 -> T340\nX404 -> T340\nT269 -> T339\nT338 -> T341", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 309 [arrowhead = none ];
309 -> 90;

310 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 310 [arrowhead = none ];
310 -> 91;

311 [label="EVAL with clause\ndelete(X422, tree(X423, X424, X425), tree(X423, X424, X426)) :- ','(less(X423, X422), delete(X422, X425, X426)).\nand substitution\nT265 -> T354\nX422 -> T354\nX423 -> T355\nX424 -> T356\nX425 -> T359\nT2 -> tree(T355, T356, T359)\nT268 -> T355\nT266 -> T356\nT269 -> T358\nX426 -> T358\nT357 -> T359", fontsize=14, style = filled, fillcolor = lightblue];
89 -> 311 [arrowhead = none ];
311 -> 92;

312 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
89 -> 312 [arrowhead = none ];
312 -> 93;

313 [label="INSTANCE with matching:\nT121 -> T336\nT122 -> T337\nT126 -> T341\nT125 -> T340", fontsize=14, style = filled, fillcolor = lightgrey];
90 -> 313 [arrowhead = none , style=dashed];
313 -> 32[style=dashed];

314 [label="INSTANCE with matching:\nT232 -> T355\nT231 -> T354\nT236 -> T359\nT235 -> T358", fontsize=14, style = filled, fillcolor = lightgrey];
92 -> 314 [arrowhead = none , style=dashed];
314 -> 64[style=dashed];

315 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
94 -> 315 [arrowhead = none ];
315 -> 96;

316 [label="EVAL with clause\ndelete(X500, tree(X501, X502, X503), tree(X501, X502, X504)) :- ','(less(X501, X500), delete(X500, X503, X504)).\nand substitution\nT6 -> T415\nX500 -> T415\nX501 -> T416\nX502 -> T417\nX503 -> T420\nT2 -> tree(T416, T417, T420)\nX504 -> T419\nT7 -> tree(T416, T417, T419)\nT418 -> T420", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 316 [arrowhead = none ];
316 -> 108;

317 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 317 [arrowhead = none ];
317 -> 109;

318 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
96 -> 318 [arrowhead = none ];
318 -> 97;

319 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
96 -> 319 [arrowhead = none ];
319 -> 98;

320 [label="EVAL with clause\nless(0, s(X453)).\nand substitution\nT367 -> 0\nX453 -> T377\nT368 -> s(T377)", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 320 [arrowhead = none ];
320 -> 99;

321 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 321 [arrowhead = none ];
321 -> 100;

322 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
98 -> 322 [arrowhead = none ];
322 -> 101;

323 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
98 -> 323 [arrowhead = none ];
323 -> 102;

324 [label="INSTANCE with matching:\nT1 -> 0\nT2 -> T372\nT3 -> T371", fontsize=14, style = filled, fillcolor = lightgrey];
99 -> 324 [arrowhead = none , style=dashed];
324 -> 1[style=dashed];

325 [label="EVAL with clause\nless(s(X467), s(X468)) :- less(X467, X468).\nand substitution\nX467 -> T388\nT367 -> s(T388)\nX468 -> T389\nT368 -> s(T389)", fontsize=14, style = filled, fillcolor = lightblue];
101 -> 325 [arrowhead = none ];
325 -> 103;

326 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
101 -> 326 [arrowhead = none ];
326 -> 104;

327 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 327 [arrowhead = none ];
327 -> 105;

328 [label="INSTANCE with matching:\nT198 -> T388\nT199 -> T389\nT182 -> T372\nT181 -> T371", fontsize=14, style = filled, fillcolor = lightgrey];
103 -> 328 [arrowhead = none , style=dashed];
328 -> 57[style=dashed];

329 [label="EVAL with clause\ndelete(X483, tree(X484, X485, X486), tree(X484, X485, X487)) :- ','(less(X484, X483), delete(X483, X486, X487)).\nand substitution\nT367 -> T402\nX483 -> T402\nX484 -> T403\nX485 -> T404\nX486 -> T407\nT2 -> tree(T403, T404, T407)\nT368 -> T403\nT371 -> T404\nT370 -> T406\nX487 -> T406\nT405 -> T407", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 329 [arrowhead = none ];
329 -> 106;

330 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 330 [arrowhead = none ];
330 -> 107;

331 [label="INSTANCE with matching:\nT232 -> T403\nT231 -> T402\nT236 -> T407\nT235 -> T406", fontsize=14, style = filled, fillcolor = lightgrey];
106 -> 331 [arrowhead = none , style=dashed];
331 -> 64[style=dashed];

332 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
108 -> 332 [arrowhead = none ];
332 -> 110;

333 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
110 -> 333 [arrowhead = none ];
333 -> 111;

334 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
110 -> 334 [arrowhead = none ];
334 -> 112;

335 [label="EVAL with clause\nless(0, s(X514)).\nand substitution\nT416 -> 0\nX514 -> T425\nT415 -> s(T425)", fontsize=14, style = filled, fillcolor = lightblue];
111 -> 335 [arrowhead = none ];
335 -> 113;

336 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
111 -> 336 [arrowhead = none ];
336 -> 114;

337 [label="EVAL with clause\nless(s(X524), s(X525)) :- less(X524, X525).\nand substitution\nX524 -> T434\nT416 -> s(T434)\nX525 -> T435\nT415 -> s(T435)", fontsize=14, style = filled, fillcolor = lightblue];
112 -> 337 [arrowhead = none ];
337 -> 115;

338 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
112 -> 338 [arrowhead = none ];
338 -> 116;

339 [label="INSTANCE with matching:\nT1 -> s(T425)\nT2 -> T420\nT3 -> T419", fontsize=14, style = filled, fillcolor = lightgrey];
113 -> 339 [arrowhead = none , style=dashed];
339 -> 1[style=dashed];

340 [label="INSTANCE with matching:\nT250 -> T434\nT251 -> T435\nT236 -> T420\nT235 -> T419", fontsize=14, style = filled, fillcolor = lightgrey];
115 -> 340 [arrowhead = none , style=dashed];
340 -> 71[style=dashed];

341 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
117 -> 341 [arrowhead = none ];
341 -> 119;

342 [label="EVAL with clause\ndelete(X758, tree(X758, X759, X760), tree(X761, X759, X762)) :- delmin(X760, X761, X762).\nand substitution\nT1 -> T625\nX758 -> T625\nX759 -> T626\nX760 -> T630\nT2 -> tree(T625, T626, T630)\nX761 -> T628\nX762 -> T629\nT3 -> tree(T628, T626, T629)\nT627 -> T630", fontsize=14, style = filled, fillcolor = lightblue];
118 -> 342 [arrowhead = none ];
342 -> 162;

343 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
118 -> 343 [arrowhead = none ];
343 -> 163;

344 [label="EVAL with clause\ndelete(X541, tree(X541, X542, X543), tree(X544, X542, X545)) :- delmin(X543, X544, X545).\nand substitution\nT440 -> T447\nX541 -> T447\nX542 -> T448\nX543 -> T452\nT2 -> tree(T447, T448, T452)\nX544 -> T450\nX545 -> T451\nT441 -> tree(T450, T448, T451)\nT449 -> T452", fontsize=14, style = filled, fillcolor = lightblue];
119 -> 344 [arrowhead = none ];
344 -> 120;

345 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
119 -> 345 [arrowhead = none ];
345 -> 121;

346 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
120 -> 346 [arrowhead = none ];
346 -> 122;

347 [label="EVAL with clause\ndelete(X662, tree(X663, X664, X665), tree(X663, X666, X665)) :- ','(less(X662, X663), delete(X662, X664, X666)).\nand substitution\nT440 -> T549\nX662 -> T549\nX663 -> T550\nX664 -> T554\nX665 -> T552\nT2 -> tree(T550, T554, T552)\nX666 -> T553\nT441 -> tree(T550, T553, T552)\nT551 -> T554", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 347 [arrowhead = none ];
347 -> 139;

348 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 348 [arrowhead = none ];
348 -> 140;

349 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
122 -> 349 [arrowhead = none ];
349 -> 123;

350 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
122 -> 350 [arrowhead = none ];
350 -> 124;

351 [label="EVAL with clause\ndelmin(tree(X559, void, X560), X559, X560).\nand substitution\nX559 -> T461\nX560 -> T462\nT452 -> tree(T461, void, T462)\nT450 -> T461\nT451 -> T462", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 351 [arrowhead = none ];
351 -> 125;

352 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 352 [arrowhead = none ];
352 -> 126;

353 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
124 -> 353 [arrowhead = none ];
353 -> 128;

354 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
124 -> 354 [arrowhead = none ];
354 -> 129;

355 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
125 -> 355 [arrowhead = none ];
355 -> 127;

356 [label="EVAL with clause\ndelmin(tree(X587, X588, X589), X590, tree(X587, X591, X592)) :- delmin(X588, X590, X591).\nand substitution\nX587 -> T487\nX588 -> T493\nX589 -> T489\nT452 -> tree(T487, T493, T489)\nT450 -> T490\nX590 -> T490\nX591 -> T491\nX592 -> T492\nT451 -> tree(T487, T491, T492)\nT488 -> T493", fontsize=14, style = filled, fillcolor = lightblue];
128 -> 356 [arrowhead = none ];
356 -> 130;

357 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
128 -> 357 [arrowhead = none ];
357 -> 131;

358 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
129 -> 358 [arrowhead = none ];
358 -> 132;

359 [label="INSTANCE with matching:\nT311 -> T493\nT308 -> T490\nT309 -> T491", fontsize=14, style = filled, fillcolor = lightgrey];
130 -> 359 [arrowhead = none , style=dashed];
359 -> 85[style=dashed];

360 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
132 -> 360 [arrowhead = none ];
360 -> 133;

361 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
132 -> 361 [arrowhead = none ];
361 -> 134;

362 [label="EVAL with clause\ndelete(X623, tree(X624, X625, X626), tree(X624, X627, X626)) :- ','(less(X623, X624), delete(X623, X625, X627)).\nand substitution\nT447 -> T518\nX623 -> T518\nX624 -> T519\nX625 -> T523\nX626 -> T521\nT2 -> tree(T519, T523, T521)\nT450 -> T519\nT448 -> T522\nX627 -> T522\nT451 -> T521\nT520 -> T523", fontsize=14, style = filled, fillcolor = lightblue];
133 -> 362 [arrowhead = none ];
362 -> 135;

363 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
133 -> 363 [arrowhead = none ];
363 -> 136;

364 [label="EVAL with clause\ndelete(X645, tree(X646, X647, X648), tree(X646, X647, X649)) :- ','(less(X646, X645), delete(X645, X648, X649)).\nand substitution\nT447 -> T536\nX645 -> T536\nX646 -> T537\nX647 -> T538\nX648 -> T541\nT2 -> tree(T537, T538, T541)\nT450 -> T537\nT448 -> T538\nT451 -> T540\nX649 -> T540\nT539 -> T541", fontsize=14, style = filled, fillcolor = lightblue];
134 -> 364 [arrowhead = none ];
364 -> 137;

365 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
134 -> 365 [arrowhead = none ];
365 -> 138;

366 [label="INSTANCE with matching:\nT336 -> T518\nT337 -> T519\nT341 -> T523\nT340 -> T522", fontsize=14, style = filled, fillcolor = lightgrey];
135 -> 366 [arrowhead = none , style=dashed];
366 -> 90[style=dashed];

367 [label="INSTANCE with matching:\nT416 -> T537\nT415 -> T536\nT420 -> T541\nT419 -> T540", fontsize=14, style = filled, fillcolor = lightgrey];
137 -> 367 [arrowhead = none , style=dashed];
367 -> 108[style=dashed];

368 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
139 -> 368 [arrowhead = none ];
368 -> 141;

369 [label="EVAL with clause\ndelete(X723, tree(X724, X725, X726), tree(X724, X725, X727)) :- ','(less(X724, X723), delete(X723, X726, X727)).\nand substitution\nT440 -> T597\nX723 -> T597\nX724 -> T598\nX725 -> T599\nX726 -> T602\nT2 -> tree(T598, T599, T602)\nX727 -> T601\nT441 -> tree(T598, T599, T601)\nT600 -> T602", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 369 [arrowhead = none ];
369 -> 153;

370 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 370 [arrowhead = none ];
370 -> 154;

371 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
141 -> 371 [arrowhead = none ];
371 -> 142;

372 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
141 -> 372 [arrowhead = none ];
372 -> 143;

373 [label="EVAL with clause\nless(0, s(X676)).\nand substitution\nT549 -> 0\nX676 -> T559\nT550 -> s(T559)", fontsize=14, style = filled, fillcolor = lightblue];
142 -> 373 [arrowhead = none ];
373 -> 144;

374 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
142 -> 374 [arrowhead = none ];
374 -> 145;

375 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
143 -> 375 [arrowhead = none ];
375 -> 146;

376 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
143 -> 376 [arrowhead = none ];
376 -> 147;

377 [label="INSTANCE with matching:\nT1 -> 0\nT2 -> T554\nT3 -> T553", fontsize=14, style = filled, fillcolor = lightgrey];
144 -> 377 [arrowhead = none , style=dashed];
377 -> 1[style=dashed];

378 [label="EVAL with clause\nless(s(X690), s(X691)) :- less(X690, X691).\nand substitution\nX690 -> T570\nT549 -> s(T570)\nX691 -> T571\nT550 -> s(T571)", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 378 [arrowhead = none ];
378 -> 148;

379 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 379 [arrowhead = none ];
379 -> 149;

380 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
147 -> 380 [arrowhead = none ];
380 -> 150;

381 [label="INSTANCE with matching:\nT388 -> T570\nT389 -> T571\nT372 -> T554\nT371 -> T553", fontsize=14, style = filled, fillcolor = lightgrey];
148 -> 381 [arrowhead = none , style=dashed];
381 -> 103[style=dashed];

382 [label="EVAL with clause\ndelete(X706, tree(X707, X708, X709), tree(X707, X708, X710)) :- ','(less(X707, X706), delete(X706, X709, X710)).\nand substitution\nT549 -> T584\nX706 -> T584\nX707 -> T585\nX708 -> T586\nX709 -> T589\nT2 -> tree(T585, T586, T589)\nT550 -> T585\nT553 -> T586\nT552 -> T588\nX710 -> T588\nT587 -> T589", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 382 [arrowhead = none ];
382 -> 151;

383 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 383 [arrowhead = none ];
383 -> 152;

384 [label="INSTANCE with matching:\nT416 -> T585\nT415 -> T584\nT420 -> T589\nT419 -> T588", fontsize=14, style = filled, fillcolor = lightgrey];
151 -> 384 [arrowhead = none , style=dashed];
384 -> 108[style=dashed];

385 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
153 -> 385 [arrowhead = none ];
385 -> 155;

386 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
155 -> 386 [arrowhead = none ];
386 -> 156;

387 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
155 -> 387 [arrowhead = none ];
387 -> 157;

388 [label="EVAL with clause\nless(0, s(X737)).\nand substitution\nT598 -> 0\nX737 -> T607\nT597 -> s(T607)", fontsize=14, style = filled, fillcolor = lightblue];
156 -> 388 [arrowhead = none ];
388 -> 158;

389 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
156 -> 389 [arrowhead = none ];
389 -> 159;

390 [label="EVAL with clause\nless(s(X747), s(X748)) :- less(X747, X748).\nand substitution\nX747 -> T616\nT598 -> s(T616)\nX748 -> T617\nT597 -> s(T617)", fontsize=14, style = filled, fillcolor = lightblue];
157 -> 390 [arrowhead = none ];
390 -> 160;

391 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
157 -> 391 [arrowhead = none ];
391 -> 161;

392 [label="INSTANCE with matching:\nT1 -> s(T607)\nT2 -> T602\nT3 -> T601", fontsize=14, style = filled, fillcolor = lightgrey];
158 -> 392 [arrowhead = none , style=dashed];
392 -> 1[style=dashed];

393 [label="INSTANCE with matching:\nT434 -> T616\nT435 -> T617\nT420 -> T602\nT419 -> T601", fontsize=14, style = filled, fillcolor = lightgrey];
160 -> 393 [arrowhead = none , style=dashed];
393 -> 115[style=dashed];

394 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
162 -> 394 [arrowhead = none ];
394 -> 164;

395 [label="EVAL with clause\ndelete(X879, tree(X880, X881, X882), tree(X880, X883, X882)) :- ','(less(X879, X880), delete(X879, X881, X883)).\nand substitution\nT1 -> T727\nX879 -> T727\nX880 -> T728\nX881 -> T732\nX882 -> T730\nT2 -> tree(T728, T732, T730)\nX883 -> T731\nT3 -> tree(T728, T731, T730)\nT729 -> T732", fontsize=14, style = filled, fillcolor = lightblue];
163 -> 395 [arrowhead = none ];
395 -> 181;

396 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
163 -> 396 [arrowhead = none ];
396 -> 182;

397 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
164 -> 397 [arrowhead = none ];
397 -> 165;

398 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
164 -> 398 [arrowhead = none ];
398 -> 166;

399 [label="EVAL with clause\ndelmin(tree(X776, void, X777), X776, X777).\nand substitution\nX776 -> T639\nX777 -> T640\nT630 -> tree(T639, void, T640)\nT628 -> T639\nT629 -> T640", fontsize=14, style = filled, fillcolor = lightblue];
165 -> 399 [arrowhead = none ];
399 -> 167;

400 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
165 -> 400 [arrowhead = none ];
400 -> 168;

401 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
166 -> 401 [arrowhead = none ];
401 -> 170;

402 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
166 -> 402 [arrowhead = none ];
402 -> 171;

403 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
167 -> 403 [arrowhead = none ];
403 -> 169;

404 [label="EVAL with clause\ndelmin(tree(X804, X805, X806), X807, tree(X804, X808, X809)) :- delmin(X805, X807, X808).\nand substitution\nX804 -> T665\nX805 -> T671\nX806 -> T667\nT630 -> tree(T665, T671, T667)\nT628 -> T668\nX807 -> T668\nX808 -> T669\nX809 -> T670\nT629 -> tree(T665, T669, T670)\nT666 -> T671", fontsize=14, style = filled, fillcolor = lightblue];
170 -> 404 [arrowhead = none ];
404 -> 172;

405 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
170 -> 405 [arrowhead = none ];
405 -> 173;

406 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
171 -> 406 [arrowhead = none ];
406 -> 174;

407 [label="INSTANCE with matching:\nT311 -> T671\nT308 -> T668\nT309 -> T669", fontsize=14, style = filled, fillcolor = lightgrey];
172 -> 407 [arrowhead = none , style=dashed];
407 -> 85[style=dashed];

408 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
174 -> 408 [arrowhead = none ];
408 -> 175;

409 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
174 -> 409 [arrowhead = none ];
409 -> 176;

410 [label="EVAL with clause\ndelete(X840, tree(X841, X842, X843), tree(X841, X844, X843)) :- ','(less(X840, X841), delete(X840, X842, X844)).\nand substitution\nT625 -> T696\nX840 -> T696\nX841 -> T697\nX842 -> T701\nX843 -> T699\nT2 -> tree(T697, T701, T699)\nT628 -> T697\nT626 -> T700\nX844 -> T700\nT629 -> T699\nT698 -> T701", fontsize=14, style = filled, fillcolor = lightblue];
175 -> 410 [arrowhead = none ];
410 -> 177;

411 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
175 -> 411 [arrowhead = none ];
411 -> 178;

412 [label="EVAL with clause\ndelete(X862, tree(X863, X864, X865), tree(X863, X864, X866)) :- ','(less(X863, X862), delete(X862, X865, X866)).\nand substitution\nT625 -> T714\nX862 -> T714\nX863 -> T715\nX864 -> T716\nX865 -> T719\nT2 -> tree(T715, T716, T719)\nT628 -> T715\nT626 -> T716\nT629 -> T718\nX866 -> T718\nT717 -> T719", fontsize=14, style = filled, fillcolor = lightblue];
176 -> 412 [arrowhead = none ];
412 -> 179;

413 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
176 -> 413 [arrowhead = none ];
413 -> 180;

414 [label="INSTANCE with matching:\nT336 -> T696\nT337 -> T697\nT341 -> T701\nT340 -> T700", fontsize=14, style = filled, fillcolor = lightgrey];
177 -> 414 [arrowhead = none , style=dashed];
414 -> 90[style=dashed];

415 [label="INSTANCE with matching:\nT416 -> T715\nT415 -> T714\nT420 -> T719\nT419 -> T718", fontsize=14, style = filled, fillcolor = lightgrey];
179 -> 415 [arrowhead = none , style=dashed];
415 -> 108[style=dashed];

416 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
181 -> 416 [arrowhead = none ];
416 -> 183;

417 [label="EVAL with clause\ndelete(X940, tree(X941, X942, X943), tree(X941, X942, X944)) :- ','(less(X941, X940), delete(X940, X943, X944)).\nand substitution\nT1 -> T775\nX940 -> T775\nX941 -> T776\nX942 -> T777\nX943 -> T780\nT2 -> tree(T776, T777, T780)\nX944 -> T779\nT3 -> tree(T776, T777, T779)\nT778 -> T780", fontsize=14, style = filled, fillcolor = lightblue];
182 -> 417 [arrowhead = none ];
417 -> 195;

418 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
182 -> 418 [arrowhead = none ];
418 -> 196;

419 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
183 -> 419 [arrowhead = none ];
419 -> 184;

420 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
183 -> 420 [arrowhead = none ];
420 -> 185;

421 [label="EVAL with clause\nless(0, s(X893)).\nand substitution\nT727 -> 0\nX893 -> T737\nT728 -> s(T737)", fontsize=14, style = filled, fillcolor = lightblue];
184 -> 421 [arrowhead = none ];
421 -> 186;

422 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
184 -> 422 [arrowhead = none ];
422 -> 187;

423 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
185 -> 423 [arrowhead = none ];
423 -> 188;

424 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
185 -> 424 [arrowhead = none ];
424 -> 189;

425 [label="INSTANCE with matching:\nT1 -> 0\nT2 -> T732\nT3 -> T731", fontsize=14, style = filled, fillcolor = lightgrey];
186 -> 425 [arrowhead = none , style=dashed];
425 -> 1[style=dashed];

426 [label="EVAL with clause\nless(s(X907), s(X908)) :- less(X907, X908).\nand substitution\nX907 -> T748\nT727 -> s(T748)\nX908 -> T749\nT728 -> s(T749)", fontsize=14, style = filled, fillcolor = lightblue];
188 -> 426 [arrowhead = none ];
426 -> 190;

427 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
188 -> 427 [arrowhead = none ];
427 -> 191;

428 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
189 -> 428 [arrowhead = none ];
428 -> 192;

429 [label="INSTANCE with matching:\nT388 -> T748\nT389 -> T749\nT372 -> T732\nT371 -> T731", fontsize=14, style = filled, fillcolor = lightgrey];
190 -> 429 [arrowhead = none , style=dashed];
429 -> 103[style=dashed];

430 [label="EVAL with clause\ndelete(X923, tree(X924, X925, X926), tree(X924, X925, X927)) :- ','(less(X924, X923), delete(X923, X926, X927)).\nand substitution\nT727 -> T762\nX923 -> T762\nX924 -> T763\nX925 -> T764\nX926 -> T767\nT2 -> tree(T763, T764, T767)\nT728 -> T763\nT731 -> T764\nT730 -> T766\nX927 -> T766\nT765 -> T767", fontsize=14, style = filled, fillcolor = lightblue];
192 -> 430 [arrowhead = none ];
430 -> 193;

431 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
192 -> 431 [arrowhead = none ];
431 -> 194;

432 [label="INSTANCE with matching:\nT416 -> T763\nT415 -> T762\nT420 -> T767\nT419 -> T766", fontsize=14, style = filled, fillcolor = lightgrey];
193 -> 432 [arrowhead = none , style=dashed];
432 -> 108[style=dashed];

433 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
195 -> 433 [arrowhead = none ];
433 -> 197;

434 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
197 -> 434 [arrowhead = none ];
434 -> 198;

435 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
197 -> 435 [arrowhead = none ];
435 -> 199;

436 [label="EVAL with clause\nless(0, s(X954)).\nand substitution\nT776 -> 0\nX954 -> T785\nT775 -> s(T785)", fontsize=14, style = filled, fillcolor = lightblue];
198 -> 436 [arrowhead = none ];
436 -> 200;

437 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
198 -> 437 [arrowhead = none ];
437 -> 201;

438 [label="EVAL with clause\nless(s(X964), s(X965)) :- less(X964, X965).\nand substitution\nX964 -> T794\nT776 -> s(T794)\nX965 -> T795\nT775 -> s(T795)", fontsize=14, style = filled, fillcolor = lightblue];
199 -> 438 [arrowhead = none ];
438 -> 202;

439 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
199 -> 439 [arrowhead = none ];
439 -> 203;

440 [label="INSTANCE with matching:\nT1 -> s(T785)\nT2 -> T780\nT3 -> T779", fontsize=14, style = filled, fillcolor = lightgrey];
200 -> 440 [arrowhead = none , style=dashed];
440 -> 1[style=dashed];

441 [label="INSTANCE with matching:\nT434 -> T794\nT435 -> T795\nT420 -> T780\nT419 -> T779", fontsize=14, style = filled, fillcolor = lightgrey];
202 -> 441 [arrowhead = none , style=dashed];
441 -> 115[style=dashed];

}

(2) Obligation:

Triples:

delmin19(tree(T90, T96, T92), T93, tree(T90, T94, T95)) :- delmin19(T96, T93, T94).
less34(s(T140), s(T141)) :- less34(T140, T141).
p44(T159, T158, T163, T162) :- less34(T159, T158).
p44(T159, T158, T163, T162) :- ','(lessc34(T159, T158), delete1(T158, T163, T162)).
p32(T121, T122, T126, T125) :- less34(T121, T122).
p32(T121, T122, T126, T125) :- ','(lessc34(T121, T122), delete1(T121, T126, T125)).
p64(0, s(T241), T236, T235) :- delete1(s(T241), T236, T235).
p64(s(T250), s(T251), T236, T235) :- p71(T250, T251, T236, T235).
p57(T198, T199, T182, T181) :- less34(T198, T199).
p57(T198, T199, T182, T181) :- ','(lessc34(T198, T199), delete1(s(T198), T182, T181)).
p71(T250, T251, T236, T235) :- less34(T250, T251).
p71(T250, T251, T236, T235) :- ','(lessc34(T250, T251), delete1(s(T251), T236, T235)).
p108(0, s(T425), T420, T419) :- delete1(s(T425), T420, T419).
p108(s(T434), s(T435), T420, T419) :- p71(T434, T435, T420, T419).
delete1(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) :- delmin19(T63, T60, T61).
delete1(T121, tree(T122, T126, T124), tree(T122, T125, T124)) :- p32(T121, T122, T126, T125).
delete1(T158, tree(T159, T160, T163), tree(T159, T160, T162)) :- p44(T159, T158, T163, T162).
delete1(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) :- delete1(0, T182, T181).
delete1(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) :- p57(T198, T199, T182, T181).
delete1(T218, tree(T219, T220, T223), tree(T219, T220, T222)) :- p44(T219, T218, T223, T222).
delete1(T231, tree(T232, T233, T236), tree(T232, T233, T235)) :- p64(T232, T231, T236, T235).
delete1(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) :- delmin19(T311, T308, T309).
delete1(T336, tree(T337, T341, T339), tree(T337, T340, T339)) :- p32(T336, T337, T341, T340).
delete1(T354, tree(T355, T356, T359), tree(T355, T356, T358)) :- p64(T355, T354, T359, T358).
delete1(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) :- delete1(0, T372, T371).
delete1(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) :- p57(T388, T389, T372, T371).
delete1(T402, tree(T403, T404, T407), tree(T403, T404, T406)) :- p64(T403, T402, T407, T406).
delete1(T415, tree(T416, T417, T420), tree(T416, T417, T419)) :- p108(T416, T415, T420, T419).
delete1(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) :- delmin19(T493, T490, T491).
delete1(T518, tree(T519, T523, T521), tree(T519, T522, T521)) :- p32(T518, T519, T523, T522).
delete1(T536, tree(T537, T538, T541), tree(T537, T538, T540)) :- p108(T537, T536, T541, T540).
delete1(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) :- delete1(0, T554, T553).
delete1(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) :- p57(T570, T571, T554, T553).
delete1(T584, tree(T585, T586, T589), tree(T585, T586, T588)) :- p108(T585, T584, T589, T588).
delete1(s(T607), tree(0, T599, T602), tree(0, T599, T601)) :- delete1(s(T607), T602, T601).
delete1(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) :- p71(T616, T617, T602, T601).
delete1(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) :- delmin19(T671, T668, T669).
delete1(T696, tree(T697, T701, T699), tree(T697, T700, T699)) :- p32(T696, T697, T701, T700).
delete1(T714, tree(T715, T716, T719), tree(T715, T716, T718)) :- p108(T715, T714, T719, T718).
delete1(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) :- delete1(0, T732, T731).
delete1(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) :- p57(T748, T749, T732, T731).
delete1(T762, tree(T763, T764, T767), tree(T763, T764, T766)) :- p108(T763, T762, T767, T766).
delete1(s(T785), tree(0, T777, T780), tree(0, T777, T779)) :- delete1(s(T785), T780, T779).
delete1(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) :- p71(T794, T795, T780, T779).

Clauses:

delminc19(tree(T76, void, T77), T76, T77).
delminc19(tree(T90, T96, T92), T93, tree(T90, T94, T95)) :- delminc19(T96, T93, T94).
deletec1(T6, tree(T6, void, T7), T7).
deletec1(T10, tree(T10, T11, void), T11).
deletec1(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32)).
deletec1(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) :- delminc19(T63, T60, T61).
deletec1(T121, tree(T122, T126, T124), tree(T122, T125, T124)) :- qc32(T121, T122, T126, T125).
deletec1(T158, tree(T159, T160, T163), tree(T159, T160, T162)) :- qc44(T159, T158, T163, T162).
deletec1(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) :- deletec1(0, T182, T181).
deletec1(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) :- qc57(T198, T199, T182, T181).
deletec1(T218, tree(T219, T220, T223), tree(T219, T220, T222)) :- qc44(T219, T218, T223, T222).
deletec1(T231, tree(T232, T233, T236), tree(T232, T233, T235)) :- qc64(T232, T231, T236, T235).
deletec1(T265, tree(T265, T266, tree(T279, void, T280)), tree(T279, T266, T280)).
deletec1(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) :- delminc19(T311, T308, T309).
deletec1(T336, tree(T337, T341, T339), tree(T337, T340, T339)) :- qc32(T336, T337, T341, T340).
deletec1(T354, tree(T355, T356, T359), tree(T355, T356, T358)) :- qc64(T355, T354, T359, T358).
deletec1(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) :- deletec1(0, T372, T371).
deletec1(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) :- qc57(T388, T389, T372, T371).
deletec1(T402, tree(T403, T404, T407), tree(T403, T404, T406)) :- qc64(T403, T402, T407, T406).
deletec1(T415, tree(T416, T417, T420), tree(T416, T417, T419)) :- qc108(T416, T415, T420, T419).
deletec1(T440, tree(T440, T441, void), T441).
deletec1(T447, tree(T447, T448, tree(T461, void, T462)), tree(T461, T448, T462)).
deletec1(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) :- delminc19(T493, T490, T491).
deletec1(T518, tree(T519, T523, T521), tree(T519, T522, T521)) :- qc32(T518, T519, T523, T522).
deletec1(T536, tree(T537, T538, T541), tree(T537, T538, T540)) :- qc108(T537, T536, T541, T540).
deletec1(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) :- deletec1(0, T554, T553).
deletec1(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) :- qc57(T570, T571, T554, T553).
deletec1(T584, tree(T585, T586, T589), tree(T585, T586, T588)) :- qc108(T585, T584, T589, T588).
deletec1(s(T607), tree(0, T599, T602), tree(0, T599, T601)) :- deletec1(s(T607), T602, T601).
deletec1(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) :- qc71(T616, T617, T602, T601).
deletec1(T625, tree(T625, T626, tree(T639, void, T640)), tree(T639, T626, T640)).
deletec1(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) :- delminc19(T671, T668, T669).
deletec1(T696, tree(T697, T701, T699), tree(T697, T700, T699)) :- qc32(T696, T697, T701, T700).
deletec1(T714, tree(T715, T716, T719), tree(T715, T716, T718)) :- qc108(T715, T714, T719, T718).
deletec1(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) :- deletec1(0, T732, T731).
deletec1(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) :- qc57(T748, T749, T732, T731).
deletec1(T762, tree(T763, T764, T767), tree(T763, T764, T766)) :- qc108(T763, T762, T767, T766).
deletec1(s(T785), tree(0, T777, T780), tree(0, T777, T779)) :- deletec1(s(T785), T780, T779).
deletec1(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) :- qc71(T794, T795, T780, T779).
lessc34(0, s(T135)).
lessc34(s(T140), s(T141)) :- lessc34(T140, T141).
qc44(T159, T158, T163, T162) :- ','(lessc34(T159, T158), deletec1(T158, T163, T162)).
qc32(T121, T122, T126, T125) :- ','(lessc34(T121, T122), deletec1(T121, T126, T125)).
qc64(0, s(T241), T236, T235) :- deletec1(s(T241), T236, T235).
qc64(s(T250), s(T251), T236, T235) :- qc71(T250, T251, T236, T235).
qc57(T198, T199, T182, T181) :- ','(lessc34(T198, T199), deletec1(s(T198), T182, T181)).
qc71(T250, T251, T236, T235) :- ','(lessc34(T250, T251), deletec1(s(T251), T236, T235)).
qc108(0, s(T425), T420, T419) :- deletec1(s(T425), T420, T419).
qc108(s(T434), s(T435), T420, T419) :- qc71(T434, T435, T420, T419).

Afs:

delete1(x1, x2, x3) = delete1(x1, x3)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
delete1_in: (b,f,b)
delmin19_in: (f,b,b)
p32_in: (b,b,f,b)
less34_in: (b,b)
lessc34_in: (b,b)
p44_in: (b,b,f,b)
p57_in: (b,b,f,b)
p64_in: (b,b,f,b)
p71_in: (b,b,f,b)
p108_in: (b,b,f,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

DELETE1_IN_GAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U19_GAG(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_in_agg(T63, T60, T61))
DELETE1_IN_GAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → DELMIN19_IN_AGG(T63, T60, T61)
DELMIN19_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_AGG(T90, T96, T92, T93, T94, T95, delmin19_in_agg(T96, T93, T94))
DELMIN19_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → DELMIN19_IN_AGG(T96, T93, T94)
DELETE1_IN_GAG(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U20_GAG(T121, T122, T126, T124, T125, p32_in_ggag(T121, T122, T126, T125))
DELETE1_IN_GAG(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → P32_IN_GGAG(T121, T122, T126, T125)
P32_IN_GGAG(T121, T122, T126, T125) → U6_GGAG(T121, T122, T126, T125, less34_in_gg(T121, T122))
P32_IN_GGAG(T121, T122, T126, T125) → LESS34_IN_GG(T121, T122)
LESS34_IN_GG(s(T140), s(T141)) → U2_GG(T140, T141, less34_in_gg(T140, T141))
LESS34_IN_GG(s(T140), s(T141)) → LESS34_IN_GG(T140, T141)
P32_IN_GGAG(T121, T122, T126, T125) → U7_GGAG(T121, T122, T126, T125, lessc34_in_gg(T121, T122))
U7_GGAG(T121, T122, T126, T125, lessc34_out_gg(T121, T122)) → U8_GGAG(T121, T122, T126, T125, delete1_in_gag(T121, T126, T125))
U7_GGAG(T121, T122, T126, T125, lessc34_out_gg(T121, T122)) → DELETE1_IN_GAG(T121, T126, T125)
DELETE1_IN_GAG(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U21_GAG(T158, T159, T160, T163, T162, p44_in_ggag(T159, T158, T163, T162))
DELETE1_IN_GAG(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → P44_IN_GGAG(T159, T158, T163, T162)
P44_IN_GGAG(T159, T158, T163, T162) → U3_GGAG(T159, T158, T163, T162, less34_in_gg(T159, T158))
P44_IN_GGAG(T159, T158, T163, T162) → LESS34_IN_GG(T159, T158)
P44_IN_GGAG(T159, T158, T163, T162) → U4_GGAG(T159, T158, T163, T162, lessc34_in_gg(T159, T158))
U4_GGAG(T159, T158, T163, T162, lessc34_out_gg(T159, T158)) → U5_GGAG(T159, T158, T163, T162, delete1_in_gag(T158, T163, T162))
U4_GGAG(T159, T158, T163, T162, lessc34_out_gg(T159, T158)) → DELETE1_IN_GAG(T158, T163, T162)
DELETE1_IN_GAG(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U22_GAG(T187, T182, T180, T181, delete1_in_gag(0, T182, T181))
DELETE1_IN_GAG(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → DELETE1_IN_GAG(0, T182, T181)
DELETE1_IN_GAG(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U23_GAG(T198, T199, T182, T180, T181, p57_in_ggag(T198, T199, T182, T181))
DELETE1_IN_GAG(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → P57_IN_GGAG(T198, T199, T182, T181)
P57_IN_GGAG(T198, T199, T182, T181) → U11_GGAG(T198, T199, T182, T181, less34_in_gg(T198, T199))
P57_IN_GGAG(T198, T199, T182, T181) → LESS34_IN_GG(T198, T199)
P57_IN_GGAG(T198, T199, T182, T181) → U12_GGAG(T198, T199, T182, T181, lessc34_in_gg(T198, T199))
U12_GGAG(T198, T199, T182, T181, lessc34_out_gg(T198, T199)) → U13_GGAG(T198, T199, T182, T181, delete1_in_gag(s(T198), T182, T181))
U12_GGAG(T198, T199, T182, T181, lessc34_out_gg(T198, T199)) → DELETE1_IN_GAG(s(T198), T182, T181)
DELETE1_IN_GAG(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U24_GAG(T218, T219, T220, T223, T222, p44_in_ggag(T219, T218, T223, T222))
DELETE1_IN_GAG(T231, tree(T232, T233, T236), tree(T232, T233, T235)) → U25_GAG(T231, T232, T233, T236, T235, p64_in_ggag(T232, T231, T236, T235))
DELETE1_IN_GAG(T231, tree(T232, T233, T236), tree(T232, T233, T235)) → P64_IN_GGAG(T232, T231, T236, T235)
P64_IN_GGAG(0, s(T241), T236, T235) → U9_GGAG(T241, T236, T235, delete1_in_gag(s(T241), T236, T235))
P64_IN_GGAG(0, s(T241), T236, T235) → DELETE1_IN_GAG(s(T241), T236, T235)
DELETE1_IN_GAG(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U26_GAG(T265, T266, T305, T311, T307, T308, T309, T310, delmin19_in_agg(T311, T308, T309))
DELETE1_IN_GAG(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U27_GAG(T336, T337, T341, T339, T340, p32_in_ggag(T336, T337, T341, T340))
DELETE1_IN_GAG(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U28_GAG(T354, T355, T356, T359, T358, p64_in_ggag(T355, T354, T359, T358))
P64_IN_GGAG(s(T250), s(T251), T236, T235) → U10_GGAG(T250, T251, T236, T235, p71_in_ggag(T250, T251, T236, T235))
P64_IN_GGAG(s(T250), s(T251), T236, T235) → P71_IN_GGAG(T250, T251, T236, T235)
P71_IN_GGAG(T250, T251, T236, T235) → U14_GGAG(T250, T251, T236, T235, less34_in_gg(T250, T251))
P71_IN_GGAG(T250, T251, T236, T235) → LESS34_IN_GG(T250, T251)
P71_IN_GGAG(T250, T251, T236, T235) → U15_GGAG(T250, T251, T236, T235, lessc34_in_gg(T250, T251))
U15_GGAG(T250, T251, T236, T235, lessc34_out_gg(T250, T251)) → U16_GGAG(T250, T251, T236, T235, delete1_in_gag(s(T251), T236, T235))
U15_GGAG(T250, T251, T236, T235, lessc34_out_gg(T250, T251)) → DELETE1_IN_GAG(s(T251), T236, T235)
DELETE1_IN_GAG(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U29_GAG(T377, T372, T370, T371, delete1_in_gag(0, T372, T371))
DELETE1_IN_GAG(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U30_GAG(T388, T389, T372, T370, T371, p57_in_ggag(T388, T389, T372, T371))
DELETE1_IN_GAG(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U31_GAG(T402, T403, T404, T407, T406, p64_in_ggag(T403, T402, T407, T406))
DELETE1_IN_GAG(T415, tree(T416, T417, T420), tree(T416, T417, T419)) → U32_GAG(T415, T416, T417, T420, T419, p108_in_ggag(T416, T415, T420, T419))
DELETE1_IN_GAG(T415, tree(T416, T417, T420), tree(T416, T417, T419)) → P108_IN_GGAG(T416, T415, T420, T419)
P108_IN_GGAG(0, s(T425), T420, T419) → U17_GGAG(T425, T420, T419, delete1_in_gag(s(T425), T420, T419))
P108_IN_GGAG(0, s(T425), T420, T419) → DELETE1_IN_GAG(s(T425), T420, T419)
DELETE1_IN_GAG(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U33_GAG(T447, T448, T487, T493, T489, T490, T491, T492, delmin19_in_agg(T493, T490, T491))
DELETE1_IN_GAG(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U34_GAG(T518, T519, T523, T521, T522, p32_in_ggag(T518, T519, T523, T522))
DELETE1_IN_GAG(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U35_GAG(T536, T537, T538, T541, T540, p108_in_ggag(T537, T536, T541, T540))
P108_IN_GGAG(s(T434), s(T435), T420, T419) → U18_GGAG(T434, T435, T420, T419, p71_in_ggag(T434, T435, T420, T419))
P108_IN_GGAG(s(T434), s(T435), T420, T419) → P71_IN_GGAG(T434, T435, T420, T419)
DELETE1_IN_GAG(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U36_GAG(T559, T554, T552, T553, delete1_in_gag(0, T554, T553))
DELETE1_IN_GAG(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U37_GAG(T570, T571, T554, T552, T553, p57_in_ggag(T570, T571, T554, T553))
DELETE1_IN_GAG(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U38_GAG(T584, T585, T586, T589, T588, p108_in_ggag(T585, T584, T589, T588))
DELETE1_IN_GAG(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U39_GAG(T607, T599, T602, T601, delete1_in_gag(s(T607), T602, T601))
DELETE1_IN_GAG(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → DELETE1_IN_GAG(s(T607), T602, T601)
DELETE1_IN_GAG(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U40_GAG(T617, T616, T599, T602, T601, p71_in_ggag(T616, T617, T602, T601))
DELETE1_IN_GAG(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → P71_IN_GGAG(T616, T617, T602, T601)
DELETE1_IN_GAG(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U41_GAG(T625, T626, T665, T671, T667, T668, T669, T670, delmin19_in_agg(T671, T668, T669))
DELETE1_IN_GAG(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U42_GAG(T696, T697, T701, T699, T700, p32_in_ggag(T696, T697, T701, T700))
DELETE1_IN_GAG(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U43_GAG(T714, T715, T716, T719, T718, p108_in_ggag(T715, T714, T719, T718))
DELETE1_IN_GAG(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U44_GAG(T737, T732, T730, T731, delete1_in_gag(0, T732, T731))
DELETE1_IN_GAG(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U45_GAG(T748, T749, T732, T730, T731, p57_in_ggag(T748, T749, T732, T731))
DELETE1_IN_GAG(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U46_GAG(T762, T763, T764, T767, T766, p108_in_ggag(T763, T762, T767, T766))
DELETE1_IN_GAG(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U47_GAG(T785, T777, T780, T779, delete1_in_gag(s(T785), T780, T779))
DELETE1_IN_GAG(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U48_GAG(T795, T794, T777, T780, T779, p71_in_ggag(T794, T795, T780, T779))

The TRS R consists of the following rules:

lessc34_in_gg(0, s(T135)) → lessc34_out_gg(0, s(T135))
lessc34_in_gg(s(T140), s(T141)) → U81_gg(T140, T141, lessc34_in_gg(T140, T141))
U81_gg(T140, T141, lessc34_out_gg(T140, T141)) → lessc34_out_gg(s(T140), s(T141))

The argument filtering Pi contains the following mapping:
delete1_in_gag(x1, x2, x3) = delete1_in_gag(x1, x3)
tree(x1, x2, x3) = tree(x1, x2, x3)
delmin19_in_agg(x1, x2, x3) = delmin19_in_agg(x2, x3)
p32_in_ggag(x1, x2, x3, x4) = p32_in_ggag(x1, x2, x4)
less34_in_gg(x1, x2) = less34_in_gg(x1, x2)
s(x1) = s(x1)
lessc34_in_gg(x1, x2) = lessc34_in_gg(x1, x2)
0 = 0
lessc34_out_gg(x1, x2) = lessc34_out_gg(x1, x2)
U81_gg(x1, x2, x3) = U81_gg(x1, x2, x3)
p44_in_ggag(x1, x2, x3, x4) = p44_in_ggag(x1, x2, x4)
p57_in_ggag(x1, x2, x3, x4) = p57_in_ggag(x1, x2, x4)
p64_in_ggag(x1, x2, x3, x4) = p64_in_ggag(x1, x2, x4)
p71_in_ggag(x1, x2, x3, x4) = p71_in_ggag(x1, x2, x4)
p108_in_ggag(x1, x2, x3, x4) = p108_in_ggag(x1, x2, x4)
DELETE1_IN_GAG(x1, x2, x3) = DELETE1_IN_GAG(x1, x3)
U19_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U19_GAG(x1, x2, x3, x6, x7, x8, x9)
DELMIN19_IN_AGG(x1, x2, x3) = DELMIN19_IN_AGG(x2, x3)
U1_AGG(x1, x2, x3, x4, x5, x6, x7) = U1_AGG(x1, x4, x5, x6, x7)
U20_GAG(x1, x2, x3, x4, x5, x6) = U20_GAG(x1, x2, x4, x5, x6)
P32_IN_GGAG(x1, x2, x3, x4) = P32_IN_GGAG(x1, x2, x4)
U6_GGAG(x1, x2, x3, x4, x5) = U6_GGAG(x1, x2, x4, x5)
LESS34_IN_GG(x1, x2) = LESS34_IN_GG(x1, x2)
U2_GG(x1, x2, x3) = U2_GG(x1, x2, x3)
U7_GGAG(x1, x2, x3, x4, x5) = U7_GGAG(x1, x2, x4, x5)
U8_GGAG(x1, x2, x3, x4, x5) = U8_GGAG(x1, x2, x4, x5)
U21_GAG(x1, x2, x3, x4, x5, x6) = U21_GAG(x1, x2, x3, x5, x6)
P44_IN_GGAG(x1, x2, x3, x4) = P44_IN_GGAG(x1, x2, x4)
U3_GGAG(x1, x2, x3, x4, x5) = U3_GGAG(x1, x2, x4, x5)
U4_GGAG(x1, x2, x3, x4, x5) = U4_GGAG(x1, x2, x4, x5)
U5_GGAG(x1, x2, x3, x4, x5) = U5_GGAG(x1, x2, x4, x5)
U22_GAG(x1, x2, x3, x4, x5) = U22_GAG(x1, x3, x4, x5)
U23_GAG(x1, x2, x3, x4, x5, x6) = U23_GAG(x1, x2, x4, x5, x6)
P57_IN_GGAG(x1, x2, x3, x4) = P57_IN_GGAG(x1, x2, x4)
U11_GGAG(x1, x2, x3, x4, x5) = U11_GGAG(x1, x2, x4, x5)
U12_GGAG(x1, x2, x3, x4, x5) = U12_GGAG(x1, x2, x4, x5)
U13_GGAG(x1, x2, x3, x4, x5) = U13_GGAG(x1, x2, x4, x5)
U24_GAG(x1, x2, x3, x4, x5, x6) = U24_GAG(x1, x2, x3, x5, x6)
U25_GAG(x1, x2, x3, x4, x5, x6) = U25_GAG(x1, x2, x3, x5, x6)
P64_IN_GGAG(x1, x2, x3, x4) = P64_IN_GGAG(x1, x2, x4)
U9_GGAG(x1, x2, x3, x4) = U9_GGAG(x1, x3, x4)
U26_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U26_GAG(x1, x2, x3, x6, x7, x8, x9)
U27_GAG(x1, x2, x3, x4, x5, x6) = U27_GAG(x1, x2, x4, x5, x6)
U28_GAG(x1, x2, x3, x4, x5, x6) = U28_GAG(x1, x2, x3, x5, x6)
U10_GGAG(x1, x2, x3, x4, x5) = U10_GGAG(x1, x2, x4, x5)
P71_IN_GGAG(x1, x2, x3, x4) = P71_IN_GGAG(x1, x2, x4)
U14_GGAG(x1, x2, x3, x4, x5) = U14_GGAG(x1, x2, x4, x5)
U15_GGAG(x1, x2, x3, x4, x5) = U15_GGAG(x1, x2, x4, x5)
U16_GGAG(x1, x2, x3, x4, x5) = U16_GGAG(x1, x2, x4, x5)
U29_GAG(x1, x2, x3, x4, x5) = U29_GAG(x1, x3, x4, x5)
U30_GAG(x1, x2, x3, x4, x5, x6) = U30_GAG(x1, x2, x4, x5, x6)
U31_GAG(x1, x2, x3, x4, x5, x6) = U31_GAG(x1, x2, x3, x5, x6)
U32_GAG(x1, x2, x3, x4, x5, x6) = U32_GAG(x1, x2, x3, x5, x6)
P108_IN_GGAG(x1, x2, x3, x4) = P108_IN_GGAG(x1, x2, x4)
U17_GGAG(x1, x2, x3, x4) = U17_GGAG(x1, x3, x4)
U33_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U33_GAG(x1, x2, x3, x6, x7, x8, x9)
U34_GAG(x1, x2, x3, x4, x5, x6) = U34_GAG(x1, x2, x4, x5, x6)
U35_GAG(x1, x2, x3, x4, x5, x6) = U35_GAG(x1, x2, x3, x5, x6)
U18_GGAG(x1, x2, x3, x4, x5) = U18_GGAG(x1, x2, x4, x5)
U36_GAG(x1, x2, x3, x4, x5) = U36_GAG(x1, x3, x4, x5)
U37_GAG(x1, x2, x3, x4, x5, x6) = U37_GAG(x1, x2, x4, x5, x6)
U38_GAG(x1, x2, x3, x4, x5, x6) = U38_GAG(x1, x2, x3, x5, x6)
U39_GAG(x1, x2, x3, x4, x5) = U39_GAG(x1, x2, x4, x5)
U40_GAG(x1, x2, x3, x4, x5, x6) = U40_GAG(x1, x2, x3, x5, x6)
U41_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U41_GAG(x1, x2, x3, x6, x7, x8, x9)
U42_GAG(x1, x2, x3, x4, x5, x6) = U42_GAG(x1, x2, x4, x5, x6)
U43_GAG(x1, x2, x3, x4, x5, x6) = U43_GAG(x1, x2, x3, x5, x6)
U44_GAG(x1, x2, x3, x4, x5) = U44_GAG(x1, x3, x4, x5)
U45_GAG(x1, x2, x3, x4, x5, x6) = U45_GAG(x1, x2, x4, x5, x6)
U46_GAG(x1, x2, x3, x4, x5, x6) = U46_GAG(x1, x2, x3, x5, x6)
U47_GAG(x1, x2, x3, x4, x5) = U47_GAG(x1, x2, x4, x5)
U48_GAG(x1, x2, x3, x4, x5, x6) = U48_GAG(x1, x2, x3, x5, x6)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETE1_IN_GAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U19_GAG(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_in_agg(T63, T60, T61))
DELETE1_IN_GAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → DELMIN19_IN_AGG(T63, T60, T61)
DELMIN19_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_AGG(T90, T96, T92, T93, T94, T95, delmin19_in_agg(T96, T93, T94))
DELMIN19_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → DELMIN19_IN_AGG(T96, T93, T94)
DELETE1_IN_GAG(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U20_GAG(T121, T122, T126, T124, T125, p32_in_ggag(T121, T122, T126, T125))
DELETE1_IN_GAG(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → P32_IN_GGAG(T121, T122, T126, T125)
P32_IN_GGAG(T121, T122, T126, T125) → U6_GGAG(T121, T122, T126, T125, less34_in_gg(T121, T122))
P32_IN_GGAG(T121, T122, T126, T125) → LESS34_IN_GG(T121, T122)
LESS34_IN_GG(s(T140), s(T141)) → U2_GG(T140, T141, less34_in_gg(T140, T141))
LESS34_IN_GG(s(T140), s(T141)) → LESS34_IN_GG(T140, T141)
P32_IN_GGAG(T121, T122, T126, T125) → U7_GGAG(T121, T122, T126, T125, lessc34_in_gg(T121, T122))
U7_GGAG(T121, T122, T126, T125, lessc34_out_gg(T121, T122)) → U8_GGAG(T121, T122, T126, T125, delete1_in_gag(T121, T126, T125))
U7_GGAG(T121, T122, T126, T125, lessc34_out_gg(T121, T122)) → DELETE1_IN_GAG(T121, T126, T125)
DELETE1_IN_GAG(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U21_GAG(T158, T159, T160, T163, T162, p44_in_ggag(T159, T158, T163, T162))
DELETE1_IN_GAG(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → P44_IN_GGAG(T159, T158, T163, T162)
P44_IN_GGAG(T159, T158, T163, T162) → U3_GGAG(T159, T158, T163, T162, less34_in_gg(T159, T158))
P44_IN_GGAG(T159, T158, T163, T162) → LESS34_IN_GG(T159, T158)
P44_IN_GGAG(T159, T158, T163, T162) → U4_GGAG(T159, T158, T163, T162, lessc34_in_gg(T159, T158))
U4_GGAG(T159, T158, T163, T162, lessc34_out_gg(T159, T158)) → U5_GGAG(T159, T158, T163, T162, delete1_in_gag(T158, T163, T162))
U4_GGAG(T159, T158, T163, T162, lessc34_out_gg(T159, T158)) → DELETE1_IN_GAG(T158, T163, T162)
DELETE1_IN_GAG(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U22_GAG(T187, T182, T180, T181, delete1_in_gag(0, T182, T181))
DELETE1_IN_GAG(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → DELETE1_IN_GAG(0, T182, T181)
DELETE1_IN_GAG(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U23_GAG(T198, T199, T182, T180, T181, p57_in_ggag(T198, T199, T182, T181))
DELETE1_IN_GAG(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → P57_IN_GGAG(T198, T199, T182, T181)
P57_IN_GGAG(T198, T199, T182, T181) → U11_GGAG(T198, T199, T182, T181, less34_in_gg(T198, T199))
P57_IN_GGAG(T198, T199, T182, T181) → LESS34_IN_GG(T198, T199)
P57_IN_GGAG(T198, T199, T182, T181) → U12_GGAG(T198, T199, T182, T181, lessc34_in_gg(T198, T199))
U12_GGAG(T198, T199, T182, T181, lessc34_out_gg(T198, T199)) → U13_GGAG(T198, T199, T182, T181, delete1_in_gag(s(T198), T182, T181))
U12_GGAG(T198, T199, T182, T181, lessc34_out_gg(T198, T199)) → DELETE1_IN_GAG(s(T198), T182, T181)
DELETE1_IN_GAG(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U24_GAG(T218, T219, T220, T223, T222, p44_in_ggag(T219, T218, T223, T222))
DELETE1_IN_GAG(T231, tree(T232, T233, T236), tree(T232, T233, T235)) → U25_GAG(T231, T232, T233, T236, T235, p64_in_ggag(T232, T231, T236, T235))
DELETE1_IN_GAG(T231, tree(T232, T233, T236), tree(T232, T233, T235)) → P64_IN_GGAG(T232, T231, T236, T235)
P64_IN_GGAG(0, s(T241), T236, T235) → U9_GGAG(T241, T236, T235, delete1_in_gag(s(T241), T236, T235))
P64_IN_GGAG(0, s(T241), T236, T235) → DELETE1_IN_GAG(s(T241), T236, T235)
DELETE1_IN_GAG(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U26_GAG(T265, T266, T305, T311, T307, T308, T309, T310, delmin19_in_agg(T311, T308, T309))
DELETE1_IN_GAG(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U27_GAG(T336, T337, T341, T339, T340, p32_in_ggag(T336, T337, T341, T340))
DELETE1_IN_GAG(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U28_GAG(T354, T355, T356, T359, T358, p64_in_ggag(T355, T354, T359, T358))
P64_IN_GGAG(s(T250), s(T251), T236, T235) → U10_GGAG(T250, T251, T236, T235, p71_in_ggag(T250, T251, T236, T235))
P64_IN_GGAG(s(T250), s(T251), T236, T235) → P71_IN_GGAG(T250, T251, T236, T235)
P71_IN_GGAG(T250, T251, T236, T235) → U14_GGAG(T250, T251, T236, T235, less34_in_gg(T250, T251))
P71_IN_GGAG(T250, T251, T236, T235) → LESS34_IN_GG(T250, T251)
P71_IN_GGAG(T250, T251, T236, T235) → U15_GGAG(T250, T251, T236, T235, lessc34_in_gg(T250, T251))
U15_GGAG(T250, T251, T236, T235, lessc34_out_gg(T250, T251)) → U16_GGAG(T250, T251, T236, T235, delete1_in_gag(s(T251), T236, T235))
U15_GGAG(T250, T251, T236, T235, lessc34_out_gg(T250, T251)) → DELETE1_IN_GAG(s(T251), T236, T235)
DELETE1_IN_GAG(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U29_GAG(T377, T372, T370, T371, delete1_in_gag(0, T372, T371))
DELETE1_IN_GAG(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U30_GAG(T388, T389, T372, T370, T371, p57_in_ggag(T388, T389, T372, T371))
DELETE1_IN_GAG(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U31_GAG(T402, T403, T404, T407, T406, p64_in_ggag(T403, T402, T407, T406))
DELETE1_IN_GAG(T415, tree(T416, T417, T420), tree(T416, T417, T419)) → U32_GAG(T415, T416, T417, T420, T419, p108_in_ggag(T416, T415, T420, T419))
DELETE1_IN_GAG(T415, tree(T416, T417, T420), tree(T416, T417, T419)) → P108_IN_GGAG(T416, T415, T420, T419)
P108_IN_GGAG(0, s(T425), T420, T419) → U17_GGAG(T425, T420, T419, delete1_in_gag(s(T425), T420, T419))
P108_IN_GGAG(0, s(T425), T420, T419) → DELETE1_IN_GAG(s(T425), T420, T419)
DELETE1_IN_GAG(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U33_GAG(T447, T448, T487, T493, T489, T490, T491, T492, delmin19_in_agg(T493, T490, T491))
DELETE1_IN_GAG(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U34_GAG(T518, T519, T523, T521, T522, p32_in_ggag(T518, T519, T523, T522))
DELETE1_IN_GAG(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U35_GAG(T536, T537, T538, T541, T540, p108_in_ggag(T537, T536, T541, T540))
P108_IN_GGAG(s(T434), s(T435), T420, T419) → U18_GGAG(T434, T435, T420, T419, p71_in_ggag(T434, T435, T420, T419))
P108_IN_GGAG(s(T434), s(T435), T420, T419) → P71_IN_GGAG(T434, T435, T420, T419)
DELETE1_IN_GAG(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U36_GAG(T559, T554, T552, T553, delete1_in_gag(0, T554, T553))
DELETE1_IN_GAG(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U37_GAG(T570, T571, T554, T552, T553, p57_in_ggag(T570, T571, T554, T553))
DELETE1_IN_GAG(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U38_GAG(T584, T585, T586, T589, T588, p108_in_ggag(T585, T584, T589, T588))
DELETE1_IN_GAG(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U39_GAG(T607, T599, T602, T601, delete1_in_gag(s(T607), T602, T601))
DELETE1_IN_GAG(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → DELETE1_IN_GAG(s(T607), T602, T601)
DELETE1_IN_GAG(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U40_GAG(T617, T616, T599, T602, T601, p71_in_ggag(T616, T617, T602, T601))
DELETE1_IN_GAG(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → P71_IN_GGAG(T616, T617, T602, T601)
DELETE1_IN_GAG(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U41_GAG(T625, T626, T665, T671, T667, T668, T669, T670, delmin19_in_agg(T671, T668, T669))
DELETE1_IN_GAG(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U42_GAG(T696, T697, T701, T699, T700, p32_in_ggag(T696, T697, T701, T700))
DELETE1_IN_GAG(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U43_GAG(T714, T715, T716, T719, T718, p108_in_ggag(T715, T714, T719, T718))
DELETE1_IN_GAG(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U44_GAG(T737, T732, T730, T731, delete1_in_gag(0, T732, T731))
DELETE1_IN_GAG(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U45_GAG(T748, T749, T732, T730, T731, p57_in_ggag(T748, T749, T732, T731))
DELETE1_IN_GAG(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U46_GAG(T762, T763, T764, T767, T766, p108_in_ggag(T763, T762, T767, T766))
DELETE1_IN_GAG(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U47_GAG(T785, T777, T780, T779, delete1_in_gag(s(T785), T780, T779))
DELETE1_IN_GAG(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U48_GAG(T795, T794, T777, T780, T779, p71_in_ggag(T794, T795, T780, T779))

The TRS R consists of the following rules:

lessc34_in_gg(0, s(T135)) → lessc34_out_gg(0, s(T135))
lessc34_in_gg(s(T140), s(T141)) → U81_gg(T140, T141, lessc34_in_gg(T140, T141))
U81_gg(T140, T141, lessc34_out_gg(T140, T141)) → lessc34_out_gg(s(T140), s(T141))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 49 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESS34_IN_GG(s(T140), s(T141)) → LESS34_IN_GG(T140, T141)

The TRS R consists of the following rules:

lessc34_in_gg(0, s(T135)) → lessc34_out_gg(0, s(T135))
lessc34_in_gg(s(T140), s(T141)) → U81_gg(T140, T141, lessc34_in_gg(T140, T141))
U81_gg(T140, T141, lessc34_out_gg(T140, T141)) → lessc34_out_gg(s(T140), s(T141))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESS34_IN_GG(s(T140), s(T141)) → LESS34_IN_GG(T140, T141)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESS34_IN_GG(s(T140), s(T141)) → LESS34_IN_GG(T140, T141)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

LESS34_IN_GG(s(T140), s(T141)) → LESS34_IN_GG(T140, T141)
The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELMIN19_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → DELMIN19_IN_AGG(T96, T93, T94)

The TRS R consists of the following rules:

lessc34_in_gg(0, s(T135)) → lessc34_out_gg(0, s(T135))
lessc34_in_gg(s(T140), s(T141)) → U81_gg(T140, T141, lessc34_in_gg(T140, T141))
U81_gg(T140, T141, lessc34_out_gg(T140, T141)) → lessc34_out_gg(s(T140), s(T141))

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELMIN19_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → DELMIN19_IN_AGG(T96, T93, T94)

R is empty.
The argument filtering Pi contains the following mapping:
tree(x1, x2, x3) = tree(x1, x2, x3)
DELMIN19_IN_AGG(x1, x2, x3) = DELMIN19_IN_AGG(x2, x3)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELMIN19_IN_AGG(T93, tree(T90, T94, T95)) → DELMIN19_IN_AGG(T93, T94)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

DELMIN19_IN_AGG(T93, tree(T90, T94, T95)) → DELMIN19_IN_AGG(T93, T94)
The graph contains the following edges 1 >= 1, 2 > 2

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETE1_IN_GAG(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → P32_IN_GGAG(T121, T122, T126, T125)
P32_IN_GGAG(T121, T122, T126, T125) → U7_GGAG(T121, T122, T126, T125, lessc34_in_gg(T121, T122))
U7_GGAG(T121, T122, T126, T125, lessc34_out_gg(T121, T122)) → DELETE1_IN_GAG(T121, T126, T125)
DELETE1_IN_GAG(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → P44_IN_GGAG(T159, T158, T163, T162)
P44_IN_GGAG(T159, T158, T163, T162) → U4_GGAG(T159, T158, T163, T162, lessc34_in_gg(T159, T158))
U4_GGAG(T159, T158, T163, T162, lessc34_out_gg(T159, T158)) → DELETE1_IN_GAG(T158, T163, T162)
DELETE1_IN_GAG(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → DELETE1_IN_GAG(0, T182, T181)
DELETE1_IN_GAG(T231, tree(T232, T233, T236), tree(T232, T233, T235)) → P64_IN_GGAG(T232, T231, T236, T235)
P64_IN_GGAG(0, s(T241), T236, T235) → DELETE1_IN_GAG(s(T241), T236, T235)
DELETE1_IN_GAG(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → P57_IN_GGAG(T198, T199, T182, T181)
P57_IN_GGAG(T198, T199, T182, T181) → U12_GGAG(T198, T199, T182, T181, lessc34_in_gg(T198, T199))
U12_GGAG(T198, T199, T182, T181, lessc34_out_gg(T198, T199)) → DELETE1_IN_GAG(s(T198), T182, T181)
DELETE1_IN_GAG(T415, tree(T416, T417, T420), tree(T416, T417, T419)) → P108_IN_GGAG(T416, T415, T420, T419)
P108_IN_GGAG(0, s(T425), T420, T419) → DELETE1_IN_GAG(s(T425), T420, T419)
DELETE1_IN_GAG(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → DELETE1_IN_GAG(s(T607), T602, T601)
DELETE1_IN_GAG(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → P71_IN_GGAG(T616, T617, T602, T601)
P71_IN_GGAG(T250, T251, T236, T235) → U15_GGAG(T250, T251, T236, T235, lessc34_in_gg(T250, T251))
U15_GGAG(T250, T251, T236, T235, lessc34_out_gg(T250, T251)) → DELETE1_IN_GAG(s(T251), T236, T235)
P108_IN_GGAG(s(T434), s(T435), T420, T419) → P71_IN_GGAG(T434, T435, T420, T419)
P64_IN_GGAG(s(T250), s(T251), T236, T235) → P71_IN_GGAG(T250, T251, T236, T235)

The TRS R consists of the following rules:

lessc34_in_gg(0, s(T135)) → lessc34_out_gg(0, s(T135))
lessc34_in_gg(s(T140), s(T141)) → U81_gg(T140, T141, lessc34_in_gg(T140, T141))
U81_gg(T140, T141, lessc34_out_gg(T140, T141)) → lessc34_out_gg(s(T140), s(T141))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3) = tree(x1, x2, x3)
s(x1) = s(x1)
lessc34_in_gg(x1, x2) = lessc34_in_gg(x1, x2)
0 = 0
lessc34_out_gg(x1, x2) = lessc34_out_gg(x1, x2)
U81_gg(x1, x2, x3) = U81_gg(x1, x2, x3)
DELETE1_IN_GAG(x1, x2, x3) = DELETE1_IN_GAG(x1, x3)
P32_IN_GGAG(x1, x2, x3, x4) = P32_IN_GGAG(x1, x2, x4)
U7_GGAG(x1, x2, x3, x4, x5) = U7_GGAG(x1, x2, x4, x5)
P44_IN_GGAG(x1, x2, x3, x4) = P44_IN_GGAG(x1, x2, x4)
U4_GGAG(x1, x2, x3, x4, x5) = U4_GGAG(x1, x2, x4, x5)
P57_IN_GGAG(x1, x2, x3, x4) = P57_IN_GGAG(x1, x2, x4)
U12_GGAG(x1, x2, x3, x4, x5) = U12_GGAG(x1, x2, x4, x5)
P64_IN_GGAG(x1, x2, x3, x4) = P64_IN_GGAG(x1, x2, x4)
P71_IN_GGAG(x1, x2, x3, x4) = P71_IN_GGAG(x1, x2, x4)
U15_GGAG(x1, x2, x3, x4, x5) = U15_GGAG(x1, x2, x4, x5)
P108_IN_GGAG(x1, x2, x3, x4) = P108_IN_GGAG(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(22) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(23) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELETE1_IN_GAG(T121, tree(T122, T125, T124)) → P32_IN_GGAG(T121, T122, T125)
P32_IN_GGAG(T121, T122, T125) → U7_GGAG(T121, T122, T125, lessc34_in_gg(T121, T122))
U7_GGAG(T121, T122, T125, lessc34_out_gg(T121, T122)) → DELETE1_IN_GAG(T121, T125)
DELETE1_IN_GAG(T158, tree(T159, T160, T162)) → P44_IN_GGAG(T159, T158, T162)
P44_IN_GGAG(T159, T158, T162) → U4_GGAG(T159, T158, T162, lessc34_in_gg(T159, T158))
U4_GGAG(T159, T158, T162, lessc34_out_gg(T159, T158)) → DELETE1_IN_GAG(T158, T162)
DELETE1_IN_GAG(0, tree(s(T187), T181, T180)) → DELETE1_IN_GAG(0, T181)
DELETE1_IN_GAG(T231, tree(T232, T233, T235)) → P64_IN_GGAG(T232, T231, T235)
P64_IN_GGAG(0, s(T241), T235) → DELETE1_IN_GAG(s(T241), T235)
DELETE1_IN_GAG(s(T198), tree(s(T199), T181, T180)) → P57_IN_GGAG(T198, T199, T181)
P57_IN_GGAG(T198, T199, T181) → U12_GGAG(T198, T199, T181, lessc34_in_gg(T198, T199))
U12_GGAG(T198, T199, T181, lessc34_out_gg(T198, T199)) → DELETE1_IN_GAG(s(T198), T181)
DELETE1_IN_GAG(T415, tree(T416, T417, T419)) → P108_IN_GGAG(T416, T415, T419)
P108_IN_GGAG(0, s(T425), T419) → DELETE1_IN_GAG(s(T425), T419)
DELETE1_IN_GAG(s(T607), tree(0, T599, T601)) → DELETE1_IN_GAG(s(T607), T601)
DELETE1_IN_GAG(s(T617), tree(s(T616), T599, T601)) → P71_IN_GGAG(T616, T617, T601)
P71_IN_GGAG(T250, T251, T235) → U15_GGAG(T250, T251, T235, lessc34_in_gg(T250, T251))
U15_GGAG(T250, T251, T235, lessc34_out_gg(T250, T251)) → DELETE1_IN_GAG(s(T251), T235)
P108_IN_GGAG(s(T434), s(T435), T419) → P71_IN_GGAG(T434, T435, T419)
P64_IN_GGAG(s(T250), s(T251), T235) → P71_IN_GGAG(T250, T251, T235)

The TRS R consists of the following rules:

lessc34_in_gg(0, s(T135)) → lessc34_out_gg(0, s(T135))
lessc34_in_gg(s(T140), s(T141)) → U81_gg(T140, T141, lessc34_in_gg(T140, T141))
U81_gg(T140, T141, lessc34_out_gg(T140, T141)) → lessc34_out_gg(s(T140), s(T141))

The set Q consists of the following terms:

lessc34_in_gg(x0, x1)
U81_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(24) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

P32_IN_GGAG(T121, T122, T125) → U7_GGAG(T121, T122, T125, lessc34_in_gg(T121, T122))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
U7_GGAG(T121, T122, T125, lessc34_out_gg(T121, T122)) → DELETE1_IN_GAG(T121, T125)
The graph contains the following edges 1 >= 1, 4 > 1, 3 >= 2
DELETE1_IN_GAG(T121, tree(T122, T125, T124)) → P32_IN_GGAG(T121, T122, T125)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
P44_IN_GGAG(T159, T158, T162) → U4_GGAG(T159, T158, T162, lessc34_in_gg(T159, T158))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
U4_GGAG(T159, T158, T162, lessc34_out_gg(T159, T158)) → DELETE1_IN_GAG(T158, T162)
The graph contains the following edges 2 >= 1, 4 > 1, 3 >= 2
DELETE1_IN_GAG(T158, tree(T159, T160, T162)) → P44_IN_GGAG(T159, T158, T162)
The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3
DELETE1_IN_GAG(0, tree(s(T187), T181, T180)) → DELETE1_IN_GAG(0, T181)
The graph contains the following edges 1 >= 1, 2 > 2
DELETE1_IN_GAG(s(T607), tree(0, T599, T601)) → DELETE1_IN_GAG(s(T607), T601)
The graph contains the following edges 1 >= 1, 2 > 2
P64_IN_GGAG(0, s(T241), T235) → DELETE1_IN_GAG(s(T241), T235)
The graph contains the following edges 2 >= 1, 3 >= 2
P64_IN_GGAG(s(T250), s(T251), T235) → P71_IN_GGAG(T250, T251, T235)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
DELETE1_IN_GAG(T231, tree(T232, T233, T235)) → P64_IN_GGAG(T232, T231, T235)
The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3
DELETE1_IN_GAG(T415, tree(T416, T417, T419)) → P108_IN_GGAG(T416, T415, T419)
The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3
P57_IN_GGAG(T198, T199, T181) → U12_GGAG(T198, T199, T181, lessc34_in_gg(T198, T199))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
U12_GGAG(T198, T199, T181, lessc34_out_gg(T198, T199)) → DELETE1_IN_GAG(s(T198), T181)
The graph contains the following edges 3 >= 2
DELETE1_IN_GAG(s(T198), tree(s(T199), T181, T180)) → P57_IN_GGAG(T198, T199, T181)
The graph contains the following edges 1 > 1, 2 > 2, 2 > 3
DELETE1_IN_GAG(s(T617), tree(s(T616), T599, T601)) → P71_IN_GGAG(T616, T617, T601)
The graph contains the following edges 2 > 1, 1 > 2, 2 > 3
P108_IN_GGAG(0, s(T425), T419) → DELETE1_IN_GAG(s(T425), T419)
The graph contains the following edges 2 >= 1, 3 >= 2
U15_GGAG(T250, T251, T235, lessc34_out_gg(T250, T251)) → DELETE1_IN_GAG(s(T251), T235)
The graph contains the following edges 3 >= 2
P108_IN_GGAG(s(T434), s(T435), T419) → P71_IN_GGAG(T434, T435, T419)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
P71_IN_GGAG(T250, T251, T235) → U15_GGAG(T250, T251, T235, lessc34_in_gg(T250, T251))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

(0) Obligation:

(1) PrologToDTProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) TriplesToPiDPProof (SOUND transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (EQUIVALENT transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) PiDPToQDPProof (SOUND transformation)

(23) Obligation:

(24) QDPSizeChangeProof (EQUIVALENT transformation)

(25) YES