Left Termination proof of /tmp/tmpjGGKgj/delete-ffb.pl

Left Termination of the query pattern delete_in_3(a, 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 UsableRulesProof (⇔)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇔)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔)

        ↳27 YES

    ↳28 PiDP

        ↳29 UsableRulesProof (⇔)

        ↳30 PiDP

        ↳31 PiDPToQDPProof (⇐)

        ↳32 QDP

        ↳33 QDPSizeChangeProof (⇔)

        ↳34 YES

    ↳35 PiDP

        ↳36 UsableRulesProof (⇔)

        ↳37 PiDP

        ↳38 PiDPToQDPProof (⇐)

        ↳39 QDP

        ↳40 QDPSizeChangeProof (⇔)

        ↳41 YES

    ↳42 PiDP

        ↳43 UsableRulesProof (⇔)

        ↳44 PiDP

        ↳45 PiDPToQDPProof (⇐)

        ↳46 QDP

        ↳47 QDPSizeChangeProof (⇔)

        ↳48 YES

    ↳49 PiDP

        ↳50 UsableRulesProof (⇔)

        ↳51 PiDP

        ↳52 PiDPToQDPProof (⇐)

        ↳53 QDP

        ↳54 QDPSizeChangeProof (⇔)

        ↳55 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(a,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\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\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | delete(T1, T2, T7), SCOPE: 1, CLAUSE: 1 | delete(T1, T2, T7), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T7), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T7), SCOPE: 1, CLAUSE: 4\n\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\nT3 is ground\ndelete(T1, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: delete(T1, T2, T7), SCOPE: 1, CLAUSE: 1 | delete(T1, T2, T7), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T7), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T7), SCOPE: 1, CLAUSE: 4\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: true | delete(T1, T2, T11), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T11), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T11), SCOPE: 1, CLAUSE: 4\n\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: delete(T1, T2, T7), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T7), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T7), SCOPE: 1, CLAUSE: 4\n\nT7 is ground\ndelete(T1, T2, T7) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: delete(T1, T2, T11), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T11), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T11), SCOPE: 1, CLAUSE: 4\n\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: delmin(T22, T20, T21) | delete(T1, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 4\n\nT20 is ground\nT18 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: delete(T1, T2, T11), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T11), SCOPE: 1, CLAUSE: 4\n\nT11 is ground\ndelete(T1, 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(T1, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 4\n\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(T1, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 4\n\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(T1, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 4\n\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(T1, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 4\n\nT20 is ground\nT18 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: delete(T1, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 3\n\nT20 is ground\nT18 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: delete(T1, T2, tree(T20, T18, T21)), SCOPE: 1, CLAUSE: 4\n\nT20 is ground\nT18 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(less(T126, T122), delete(T126, T127, T125))\n\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(T126, T122)\n\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: delete(T130, T131, T125)\n\nT125 is ground\nT130 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: less(T126, T122), SCOPE: 4, CLAUSE: 7 | less(T126, T122), SCOPE: 4, CLAUSE: 8\n\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: less(T126, T122), SCOPE: 4, CLAUSE: 7\n\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: less(T126, T122), SCOPE: 4, CLAUSE: 8\n\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(T145, T144)\n\nT144 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(less(T163, T167), delete(T167, T168, T166))\n\nT163 is ground\nT166 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: less(T163, T167)\n\nT163 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: delete(T171, T172, T166)\n\nT166 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: less(T163, T167), SCOPE: 5, CLAUSE: 7 | less(T163, T167), SCOPE: 5, CLAUSE: 8\n\nT163 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: less(T163, T167), SCOPE: 5, CLAUSE: 7\n\nT163 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: less(T163, T167), SCOPE: 5, CLAUSE: 8\n\nT163 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: less(T184, T186)\n\nT184 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(less(T203, T199), delete(T203, T204, T202)) | delete(T1, T2, tree(T199, T202, T201)), SCOPE: 1, CLAUSE: 4\n\nT199 is ground\nT202 is ground\nT201 is ground\ndelete(T1, T2, tree(T199, T202, T201)) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: delete(T1, T2, T11), SCOPE: 1, CLAUSE: 4\n\nT11 is ground\ndelete(T1, T2, T11) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))\ndelete(T1, T2, T11) !=? delete(X226, tree(X227, X228, X229), tree(X227, X230, X229))", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(less(T203, T199), delete(T203, T204, T202)), SCOPE: 6, CLAUSE: 7 | ','(less(T203, T199), delete(T203, T204, T202)), SCOPE: 6, CLAUSE: 8 | ?_6 | delete(T1, T2, tree(T199, T202, T201)), SCOPE: 1, CLAUSE: 4\n\nT199 is ground\nT202 is ground\nT201 is ground\ndelete(T1, T2, tree(T199, T202, T201)) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(less(T203, T199), delete(T203, T204, T202)), SCOPE: 6, CLAUSE: 7\n\nT199 is ground\nT202 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(less(T203, T199), delete(T203, T204, T202)), SCOPE: 6, CLAUSE: 8 | ?_6 | delete(T1, T2, tree(T199, T202, T201)), SCOPE: 1, CLAUSE: 4\n\nT199 is ground\nT202 is ground\nT201 is ground\ndelete(T1, T2, tree(T199, T202, T201)) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: delete(0, T210, T202)\n\nT202 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(less(T203, T199), delete(T203, T204, T202)), SCOPE: 6, CLAUSE: 8\n\nT199 is ground\nT202 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ?_6 | delete(T1, T2, tree(T199, T202, T201)), SCOPE: 1, CLAUSE: 4\n\nT199 is ground\nT202 is ground\nT201 is ground\ndelete(T1, T2, tree(T199, T202, T201)) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(less(T223, T222), delete(s(T223), T224, T202))\n\nT202 is ground\nT222 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: less(T223, T222)\n\nT222 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: delete(s(T227), T228, T202)\n\nT202 is ground\nT227 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: delete(T1, T2, tree(T199, T202, T201)), SCOPE: 1, CLAUSE: 4\n\nT199 is ground\nT202 is ground\nT201 is ground\ndelete(T1, T2, tree(T199, T202, T201)) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(less(T246, T250), delete(T250, T251, T249))\n\nT246 is ground\nT249 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(less(T260, T264), delete(T264, T265, T263))\n\nT260 is ground\nT263 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(less(T260, T264), delete(T264, T265, T263)), SCOPE: 7, CLAUSE: 7 | ','(less(T260, T264), delete(T264, T265, T263)), SCOPE: 7, CLAUSE: 8\n\nT260 is ground\nT263 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(less(T260, T264), delete(T264, T265, T263)), SCOPE: 7, CLAUSE: 7\n\nT260 is ground\nT263 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(less(T260, T264), delete(T264, T265, T263)), SCOPE: 7, CLAUSE: 8\n\nT260 is ground\nT263 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: delete(s(T272), T271, T263)\n\nT263 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(less(T281, T283), delete(s(T283), T284, T263))\n\nT263 is ground\nT281 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: less(T281, T283)\n\nT281 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: delete(s(T287), T288, T263)\n\nT263 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: delmin(T305, T303, T304) | delete(T1, T2, tree(T303, T301, T304)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T303, T301, T304)), SCOPE: 1, CLAUSE: 4\n\nT303 is ground\nT301 is ground\nT304 is ground\ndelete(T1, T2, tree(T303, T301, T304)) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: delete(T1, T2, T7), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T7), SCOPE: 1, CLAUSE: 4\n\nT7 is ground\ndelete(T1, T2, T7) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T1, T2, T7) !=? delete(X334, tree(X334, X335, X336), tree(X337, X335, X338))", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: delmin(T305, T303, T304), SCOPE: 8, CLAUSE: 5 | delmin(T305, T303, T304), SCOPE: 8, CLAUSE: 6 | ?_8 | delete(T1, T2, tree(T303, T301, T304)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T303, T301, T304)), SCOPE: 1, CLAUSE: 4\n\nT303 is ground\nT301 is ground\nT304 is ground\ndelete(T1, T2, tree(T303, T301, T304)) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: delmin(T305, T303, T304), SCOPE: 8, CLAUSE: 5\n\nT303 is ground\nT304 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: delmin(T305, T303, T304), SCOPE: 8, CLAUSE: 6 | ?_8 | delete(T1, T2, tree(T303, T301, T304)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T303, T301, T304)), SCOPE: 1, CLAUSE: 4\n\nT303 is ground\nT301 is ground\nT304 is ground\ndelete(T1, T2, tree(T303, T301, T304)) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: delmin(T305, T303, T304), SCOPE: 8, CLAUSE: 6\n\nT303 is ground\nT304 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ?_8 | delete(T1, T2, tree(T303, T301, T304)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T303, T301, T304)), SCOPE: 1, CLAUSE: 4\n\nT303 is ground\nT301 is ground\nT304 is ground\ndelete(T1, T2, tree(T303, T301, T304)) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: delmin(T346, T343, T344)\n\nT343 is ground\nT344 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: delete(T1, T2, tree(T303, T301, T304)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T303, T301, T304)), SCOPE: 1, CLAUSE: 4\n\nT303 is ground\nT301 is ground\nT304 is ground\ndelete(T1, T2, tree(T303, T301, T304)) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: delete(T1, T2, tree(T303, T301, T304)), SCOPE: 1, CLAUSE: 3\n\nT303 is ground\nT301 is ground\nT304 is ground\ndelete(T1, T2, tree(T303, T301, T304)) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: delete(T1, T2, tree(T303, T301, T304)), SCOPE: 1, CLAUSE: 4\n\nT303 is ground\nT301 is ground\nT304 is ground\ndelete(T1, T2, tree(T303, T301, T304)) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(less(T376, T372), delete(T376, T377, T375))\n\nT372 is ground\nT375 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(less(T391, T395), delete(T395, T396, T394))\n\nT391 is ground\nT394 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ','(less(T409, T405), delete(T409, T410, T408)) | delete(T1, T2, tree(T405, T408, T407)), SCOPE: 1, CLAUSE: 4\n\nT405 is ground\nT408 is ground\nT407 is ground\ndelete(T1, T2, tree(T405, T408, T407)) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T1, T2, tree(T405, T408, T407)) !=? delete(X334, tree(X334, X335, X336), tree(X337, X335, X338))", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: delete(T1, T2, T7), SCOPE: 1, CLAUSE: 4\n\nT7 is ground\ndelete(T1, T2, T7) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T1, T2, T7) !=? delete(X334, tree(X334, X335, X336), tree(X337, X335, X338))\ndelete(T1, T2, T7) !=? delete(X455, tree(X456, X457, X458), tree(X456, X459, X458))", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(less(T409, T405), delete(T409, T410, T408)), SCOPE: 9, CLAUSE: 7 | ','(less(T409, T405), delete(T409, T410, T408)), SCOPE: 9, CLAUSE: 8 | ?_9 | delete(T1, T2, tree(T405, T408, T407)), SCOPE: 1, CLAUSE: 4\n\nT405 is ground\nT408 is ground\nT407 is ground\ndelete(T1, T2, tree(T405, T408, T407)) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T1, T2, tree(T405, T408, T407)) !=? delete(X334, tree(X334, X335, X336), tree(X337, X335, X338))", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(less(T409, T405), delete(T409, T410, T408)), SCOPE: 9, CLAUSE: 7\n\nT405 is ground\nT408 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(less(T409, T405), delete(T409, T410, T408)), SCOPE: 9, CLAUSE: 8 | ?_9 | delete(T1, T2, tree(T405, T408, T407)), SCOPE: 1, CLAUSE: 4\n\nT405 is ground\nT408 is ground\nT407 is ground\ndelete(T1, T2, tree(T405, T408, T407)) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T1, T2, tree(T405, T408, T407)) !=? delete(X334, tree(X334, X335, X336), tree(X337, X335, X338))", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: delete(0, T416, T408)\n\nT408 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(less(T409, T405), delete(T409, T410, T408)), SCOPE: 9, CLAUSE: 8\n\nT405 is ground\nT408 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ?_9 | delete(T1, T2, tree(T405, T408, T407)), SCOPE: 1, CLAUSE: 4\n\nT405 is ground\nT408 is ground\nT407 is ground\ndelete(T1, T2, tree(T405, T408, T407)) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T1, T2, tree(T405, T408, T407)) !=? delete(X334, tree(X334, X335, X336), tree(X337, X335, X338))", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(less(T429, T428), delete(s(T429), T430, T408))\n\nT408 is ground\nT428 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: delete(T1, T2, tree(T405, T408, T407)), SCOPE: 1, CLAUSE: 4\n\nT405 is ground\nT408 is ground\nT407 is ground\ndelete(T1, T2, tree(T405, T408, T407)) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T1, T2, tree(T405, T408, T407)) !=? delete(X334, tree(X334, X335, X336), tree(X337, X335, X338))", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: ','(less(T444, T448), delete(T448, T449, T447))\n\nT444 is ground\nT447 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ','(less(T458, T462), delete(T462, T463, T461))\n\nT458 is ground\nT461 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: ','(less(T458, T462), delete(T462, T463, T461)), SCOPE: 10, CLAUSE: 7 | ','(less(T458, T462), delete(T462, T463, T461)), SCOPE: 10, CLAUSE: 8\n\nT458 is ground\nT461 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(less(T458, T462), delete(T462, T463, T461)), SCOPE: 10, CLAUSE: 7\n\nT458 is ground\nT461 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(less(T458, T462), delete(T462, T463, T461)), SCOPE: 10, CLAUSE: 8\n\nT458 is ground\nT461 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: delete(s(T470), T469, T461)\n\nT461 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: ','(less(T479, T481), delete(s(T481), T482, T461))\n\nT461 is ground\nT479 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: true | delete(T1, T2, T488), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T488), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T488), SCOPE: 1, CLAUSE: 4\n\nT488 is ground\ndelete(T1, T2, T488) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: 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\nT3 is ground\ndelete(T1, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, T3) !=? delete(X548, tree(X548, X549, void), X549)", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: delete(T1, T2, T488), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T488), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T488), SCOPE: 1, CLAUSE: 4\n\nT488 is ground\ndelete(T1, T2, T488) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: delmin(T499, T497, T498) | delete(T1, T2, tree(T497, T495, T498)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T497, T495, T498)), SCOPE: 1, CLAUSE: 4\n\nT497 is ground\nT495 is ground\nT498 is ground\ndelete(T1, T2, tree(T497, T495, T498)) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: delete(T1, T2, T488), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T488), SCOPE: 1, CLAUSE: 4\n\nT488 is ground\ndelete(T1, T2, T488) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, T488) !=? delete(X557, tree(X557, X558, X559), tree(X560, X558, X561))", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: delmin(T499, T497, T498), SCOPE: 11, CLAUSE: 5 | delmin(T499, T497, T498), SCOPE: 11, CLAUSE: 6 | ?_11 | delete(T1, T2, tree(T497, T495, T498)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T497, T495, T498)), SCOPE: 1, CLAUSE: 4\n\nT497 is ground\nT495 is ground\nT498 is ground\ndelete(T1, T2, tree(T497, T495, T498)) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: delmin(T499, T497, T498), SCOPE: 11, CLAUSE: 5\n\nT497 is ground\nT498 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: delmin(T499, T497, T498), SCOPE: 11, CLAUSE: 6 | ?_11 | delete(T1, T2, tree(T497, T495, T498)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T497, T495, T498)), SCOPE: 1, CLAUSE: 4\n\nT497 is ground\nT495 is ground\nT498 is ground\ndelete(T1, T2, tree(T497, T495, T498)) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: delmin(T499, T497, T498), SCOPE: 11, CLAUSE: 6\n\nT497 is ground\nT498 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ?_11 | delete(T1, T2, tree(T497, T495, T498)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T497, T495, T498)), SCOPE: 1, CLAUSE: 4\n\nT497 is ground\nT495 is ground\nT498 is ground\ndelete(T1, T2, tree(T497, T495, T498)) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: delmin(T540, T537, T538)\n\nT537 is ground\nT538 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: delete(T1, T2, tree(T497, T495, T498)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T497, T495, T498)), SCOPE: 1, CLAUSE: 4\n\nT497 is ground\nT495 is ground\nT498 is ground\ndelete(T1, T2, tree(T497, T495, T498)) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: delete(T1, T2, tree(T497, T495, T498)), SCOPE: 1, CLAUSE: 3\n\nT497 is ground\nT495 is ground\nT498 is ground\ndelete(T1, T2, tree(T497, T495, T498)) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: delete(T1, T2, tree(T497, T495, T498)), SCOPE: 1, CLAUSE: 4\n\nT497 is ground\nT495 is ground\nT498 is ground\ndelete(T1, T2, tree(T497, T495, T498)) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ','(less(T570, T566), delete(T570, T571, T569))\n\nT566 is ground\nT569 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: ','(less(T585, T589), delete(T589, T590, T588))\n\nT585 is ground\nT588 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: ','(less(T603, T599), delete(T603, T604, T602)) | delete(T1, T2, tree(T599, T602, T601)), SCOPE: 1, CLAUSE: 4\n\nT599 is ground\nT602 is ground\nT601 is ground\ndelete(T1, T2, tree(T599, T602, T601)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, tree(T599, T602, T601)) !=? delete(X557, tree(X557, X558, X559), tree(X560, X558, X561))", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: delete(T1, T2, T488), SCOPE: 1, CLAUSE: 4\n\nT488 is ground\ndelete(T1, T2, T488) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, T488) !=? delete(X557, tree(X557, X558, X559), tree(X560, X558, X561))\ndelete(T1, T2, T488) !=? delete(X678, tree(X679, X680, X681), tree(X679, X682, X681))", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: ','(less(T603, T599), delete(T603, T604, T602)), SCOPE: 12, CLAUSE: 7 | ','(less(T603, T599), delete(T603, T604, T602)), SCOPE: 12, CLAUSE: 8 | ?_12 | delete(T1, T2, tree(T599, T602, T601)), SCOPE: 1, CLAUSE: 4\n\nT599 is ground\nT602 is ground\nT601 is ground\ndelete(T1, T2, tree(T599, T602, T601)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, tree(T599, T602, T601)) !=? delete(X557, tree(X557, X558, X559), tree(X560, X558, X561))", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: ','(less(T603, T599), delete(T603, T604, T602)), SCOPE: 12, CLAUSE: 7\n\nT599 is ground\nT602 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: ','(less(T603, T599), delete(T603, T604, T602)), SCOPE: 12, CLAUSE: 8 | ?_12 | delete(T1, T2, tree(T599, T602, T601)), SCOPE: 1, CLAUSE: 4\n\nT599 is ground\nT602 is ground\nT601 is ground\ndelete(T1, T2, tree(T599, T602, T601)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, tree(T599, T602, T601)) !=? delete(X557, tree(X557, X558, X559), tree(X560, X558, X561))", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: delete(0, T610, T602)\n\nT602 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: ','(less(T603, T599), delete(T603, T604, T602)), SCOPE: 12, CLAUSE: 8\n\nT599 is ground\nT602 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: ?_12 | delete(T1, T2, tree(T599, T602, T601)), SCOPE: 1, CLAUSE: 4\n\nT599 is ground\nT602 is ground\nT601 is ground\ndelete(T1, T2, tree(T599, T602, T601)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, tree(T599, T602, T601)) !=? delete(X557, tree(X557, X558, X559), tree(X560, X558, X561))", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: ','(less(T623, T622), delete(s(T623), T624, T602))\n\nT602 is ground\nT622 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: delete(T1, T2, tree(T599, T602, T601)), SCOPE: 1, CLAUSE: 4\n\nT599 is ground\nT602 is ground\nT601 is ground\ndelete(T1, T2, tree(T599, T602, T601)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, tree(T599, T602, T601)) !=? delete(X557, tree(X557, X558, X559), tree(X560, X558, X561))", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: ','(less(T638, T642), delete(T642, T643, T641))\n\nT638 is ground\nT641 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ','(less(T652, T656), delete(T656, T657, T655))\n\nT652 is ground\nT655 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: ','(less(T652, T656), delete(T656, T657, T655)), SCOPE: 13, CLAUSE: 7 | ','(less(T652, T656), delete(T656, T657, T655)), SCOPE: 13, CLAUSE: 8\n\nT652 is ground\nT655 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ','(less(T652, T656), delete(T656, T657, T655)), SCOPE: 13, CLAUSE: 7\n\nT652 is ground\nT655 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: ','(less(T652, T656), delete(T656, T657, T655)), SCOPE: 13, CLAUSE: 8\n\nT652 is ground\nT655 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: delete(s(T664), T663, T655)\n\nT655 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: ','(less(T673, T675), delete(s(T675), T676, T655))\n\nT655 is ground\nT673 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: delmin(T689, T687, T688) | delete(T1, T2, tree(T687, T685, T688)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T687, T685, T688)), SCOPE: 1, CLAUSE: 4\n\nT687 is ground\nT685 is ground\nT688 is ground\ndelete(T1, T2, tree(T687, T685, T688)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, tree(T687, T685, T688)) !=? delete(X548, tree(X548, X549, void), X549)", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT3 is ground\ndelete(T1, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, T3) !=? delete(X548, tree(X548, X549, void), X549)\ndelete(T1, T2, T3) !=? delete(X774, tree(X774, X775, X776), tree(X777, X775, X778))", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: delmin(T689, T687, T688), SCOPE: 14, CLAUSE: 5 | delmin(T689, T687, T688), SCOPE: 14, CLAUSE: 6 | ?_14 | delete(T1, T2, tree(T687, T685, T688)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T687, T685, T688)), SCOPE: 1, CLAUSE: 4\n\nT687 is ground\nT685 is ground\nT688 is ground\ndelete(T1, T2, tree(T687, T685, T688)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, tree(T687, T685, T688)) !=? delete(X548, tree(X548, X549, void), X549)", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: delmin(T689, T687, T688), SCOPE: 14, CLAUSE: 5\n\nT687 is ground\nT688 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: delmin(T689, T687, T688), SCOPE: 14, CLAUSE: 6 | ?_14 | delete(T1, T2, tree(T687, T685, T688)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T687, T685, T688)), SCOPE: 1, CLAUSE: 4\n\nT687 is ground\nT685 is ground\nT688 is ground\ndelete(T1, T2, tree(T687, T685, T688)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, tree(T687, T685, T688)) !=? delete(X548, tree(X548, X549, void), X549)", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: delmin(T689, T687, T688), SCOPE: 14, CLAUSE: 6\n\nT687 is ground\nT688 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: ?_14 | delete(T1, T2, tree(T687, T685, T688)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T687, T685, T688)), SCOPE: 1, CLAUSE: 4\n\nT687 is ground\nT685 is ground\nT688 is ground\ndelete(T1, T2, tree(T687, T685, T688)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, tree(T687, T685, T688)) !=? delete(X548, tree(X548, X549, void), X549)", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: delmin(T730, T727, T728)\n\nT727 is ground\nT728 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: delete(T1, T2, tree(T687, T685, T688)), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, tree(T687, T685, T688)), SCOPE: 1, CLAUSE: 4\n\nT687 is ground\nT685 is ground\nT688 is ground\ndelete(T1, T2, tree(T687, T685, T688)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, tree(T687, T685, T688)) !=? delete(X548, tree(X548, X549, void), X549)", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: delete(T1, T2, tree(T687, T685, T688)), SCOPE: 1, CLAUSE: 3\n\nT687 is ground\nT685 is ground\nT688 is ground\ndelete(T1, T2, tree(T687, T685, T688)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, tree(T687, T685, T688)) !=? delete(X548, tree(X548, X549, void), X549)", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: delete(T1, T2, tree(T687, T685, T688)), SCOPE: 1, CLAUSE: 4\n\nT687 is ground\nT685 is ground\nT688 is ground\ndelete(T1, T2, tree(T687, T685, T688)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, tree(T687, T685, T688)) !=? delete(X548, tree(X548, X549, void), X549)", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: ','(less(T760, T756), delete(T760, T761, T759))\n\nT756 is ground\nT759 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: ','(less(T775, T779), delete(T779, T780, T778))\n\nT775 is ground\nT778 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: ','(less(T793, T789), delete(T793, T794, T792)) | delete(T1, T2, tree(T789, T792, T791)), SCOPE: 1, CLAUSE: 4\n\nT789 is ground\nT792 is ground\nT791 is ground\ndelete(T1, T2, tree(T789, T792, T791)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, tree(T789, T792, T791)) !=? delete(X548, tree(X548, X549, void), X549)\ndelete(T1, T2, tree(T789, T792, T791)) !=? delete(X774, tree(X774, X775, X776), tree(X777, X775, X778))", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT3 is ground\ndelete(T1, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, T3) !=? delete(X548, tree(X548, X549, void), X549)\ndelete(T1, T2, T3) !=? delete(X774, tree(X774, X775, X776), tree(X777, X775, X778))\ndelete(T1, T2, T3) !=? delete(X895, tree(X896, X897, X898), tree(X896, X899, X898))", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: ','(less(T793, T789), delete(T793, T794, T792)), SCOPE: 15, CLAUSE: 7 | ','(less(T793, T789), delete(T793, T794, T792)), SCOPE: 15, CLAUSE: 8 | ?_15 | delete(T1, T2, tree(T789, T792, T791)), SCOPE: 1, CLAUSE: 4\n\nT789 is ground\nT792 is ground\nT791 is ground\ndelete(T1, T2, tree(T789, T792, T791)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, tree(T789, T792, T791)) !=? delete(X548, tree(X548, X549, void), X549)\ndelete(T1, T2, tree(T789, T792, T791)) !=? delete(X774, tree(X774, X775, X776), tree(X777, X775, X778))", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: ','(less(T793, T789), delete(T793, T794, T792)), SCOPE: 15, CLAUSE: 7\n\nT789 is ground\nT792 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(less(T793, T789), delete(T793, T794, T792)), SCOPE: 15, CLAUSE: 8 | ?_15 | delete(T1, T2, tree(T789, T792, T791)), SCOPE: 1, CLAUSE: 4\n\nT789 is ground\nT792 is ground\nT791 is ground\ndelete(T1, T2, tree(T789, T792, T791)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, tree(T789, T792, T791)) !=? delete(X548, tree(X548, X549, void), X549)\ndelete(T1, T2, tree(T789, T792, T791)) !=? delete(X774, tree(X774, X775, X776), tree(X777, X775, X778))", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: delete(0, T800, T792)\n\nT792 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ','(less(T793, T789), delete(T793, T794, T792)), SCOPE: 15, CLAUSE: 8\n\nT789 is ground\nT792 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: ?_15 | delete(T1, T2, tree(T789, T792, T791)), SCOPE: 1, CLAUSE: 4\n\nT789 is ground\nT792 is ground\nT791 is ground\ndelete(T1, T2, tree(T789, T792, T791)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, tree(T789, T792, T791)) !=? delete(X548, tree(X548, X549, void), X549)\ndelete(T1, T2, tree(T789, T792, T791)) !=? delete(X774, tree(X774, X775, X776), tree(X777, X775, X778))", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: ','(less(T813, T812), delete(s(T813), T814, T792))\n\nT792 is ground\nT812 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: delete(T1, T2, tree(T789, T792, T791)), SCOPE: 1, CLAUSE: 4\n\nT789 is ground\nT792 is ground\nT791 is ground\ndelete(T1, T2, tree(T789, T792, T791)) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, tree(T789, T792, T791)) !=? delete(X548, tree(X548, X549, void), X549)\ndelete(T1, T2, tree(T789, T792, T791)) !=? delete(X774, tree(X774, X775, X776), tree(X777, X775, X778))", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: ','(less(T828, T832), delete(T832, T833, T831))\n\nT828 is ground\nT831 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: ','(less(T842, T846), delete(T846, T847, T845))\n\nT842 is ground\nT845 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: ','(less(T842, T846), delete(T846, T847, T845)), SCOPE: 16, CLAUSE: 7 | ','(less(T842, T846), delete(T846, T847, T845)), SCOPE: 16, CLAUSE: 8\n\nT842 is ground\nT845 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: ','(less(T842, T846), delete(T846, T847, T845)), SCOPE: 16, CLAUSE: 7\n\nT842 is ground\nT845 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: ','(less(T842, T846), delete(T846, T847, T845)), SCOPE: 16, CLAUSE: 8\n\nT842 is ground\nT845 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: delete(s(T854), T853, T845)\n\nT845 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: ','(less(T863, T865), delete(s(T865), T866, T845))\n\nT845 is ground\nT863 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 212 [arrowhead = none ];
212 -> 2;

213 [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 -> 213 [arrowhead = none ];
213 -> 3;

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

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

216 [label="EVAL with clause\ndelete(X548, tree(X548, X549, void), X549).\nand substitution\nT1 -> T487\nX548 -> T487\nX549 -> T488\nT2 -> tree(T487, T488, void)\nT3 -> T488", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 216 [arrowhead = none ];
216 -> 125;

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

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

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

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

221 [label="EVAL with clause\ndelete(X334, tree(X334, X335, X336), tree(X337, X335, X338)) :- delmin(X336, X337, X338).\nand substitution\nT1 -> T300\nX334 -> T300\nX335 -> T301\nX336 -> T305\nT2 -> tree(T300, T301, T305)\nX337 -> T303\nX338 -> T304\nT7 -> tree(T303, T301, T304)\nT302 -> T305", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 221 [arrowhead = none ];
221 -> 83;

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

223 [label="EVAL with clause\ndelete(X21, tree(X21, X22, X23), tree(X24, X22, X25)) :- delmin(X23, X24, X25).\nand substitution\nT1 -> 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 -> 223 [arrowhead = none ];
223 -> 9;

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

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

226 [label="EVAL with clause\ndelete(X226, tree(X227, X228, X229), tree(X227, X230, X229)) :- ','(less(X226, X227), delete(X226, X228, X230)).\nand substitution\nT1 -> T203\nX226 -> T203\nX227 -> T199\nX228 -> T204\nX229 -> T201\nT2 -> tree(T199, T204, T201)\nX230 -> T202\nT11 -> tree(T199, T202, T201)\nT198 -> T203\nT200 -> T204", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 226 [arrowhead = none ];
226 -> 56;

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

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

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

230 [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 -> 230 [arrowhead = none ];
230 -> 14;

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

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

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

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

235 [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 -> 235 [arrowhead = none ];
235 -> 19;

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

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

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

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

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

241 [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 -> 241 [arrowhead = none ];
241 -> 24;

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

243 [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 -> 243 [arrowhead = none ];
243 -> 27;

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

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

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

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

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

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

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

251 [label="EVAL with clause\ndelete(X187, tree(X188, X189, X190), tree(X188, X189, X191)) :- ','(less(X188, X187), delete(X187, X190, X191)).\nand substitution\nT1 -> T167\nX187 -> T167\nX188 -> T163\nX189 -> T164\nX190 -> T168\nT2 -> tree(T163, T164, T168)\nT20 -> T163\nT18 -> T164\nT21 -> T166\nX191 -> T166\nT162 -> T167\nT165 -> T168", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 251 [arrowhead = none ];
251 -> 44;

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

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

254 [label="SPLIT 2\nnew knowledge:\nT130 is ground\nreplacements:\nT126 -> T130\nT127 -> T131", fontsize=14, style = filled, fillcolor = violet];
32 -> 254 [arrowhead = none ];
254 -> 35;

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

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

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

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

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

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

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

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

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

264 [label="INSTANCE with matching:\nT126 -> T145\nT122 -> T144", fontsize=14, style = filled, fillcolor = lightgrey];
42 -> 264 [arrowhead = none , style=dashed];
264 -> 34[style=dashed];

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

266 [label="SPLIT 2\nreplacements:\nT167 -> T171\nT168 -> T172", fontsize=14, style = filled, fillcolor = violet];
44 -> 266 [arrowhead = none ];
266 -> 47;

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

268 [label="INSTANCE with matching:\nT1 -> T171\nT2 -> T172\nT3 -> T166", fontsize=14, style = filled, fillcolor = lightgrey];
47 -> 268 [arrowhead = none , style=dashed];
268 -> 1[style=dashed];

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

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

271 [label="EVAL with clause\nless(0, s(X205)).\nand substitution\nT163 -> 0\nX205 -> T179\nT167 -> s(T179)", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 271 [arrowhead = none ];
271 -> 51;

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

273 [label="EVAL with clause\nless(s(X211), s(X212)) :- less(X211, X212).\nand substitution\nX211 -> T184\nT163 -> s(T184)\nX212 -> T186\nT167 -> s(T186)\nT185 -> T186", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 273 [arrowhead = none ];
273 -> 54;

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

275 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 275 [arrowhead = none ];
275 -> 53;

276 [label="INSTANCE with matching:\nT163 -> T184\nT167 -> T186", fontsize=14, style = filled, fillcolor = lightgrey];
54 -> 276 [arrowhead = none , style=dashed];
276 -> 46[style=dashed];

277 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
56 -> 277 [arrowhead = none ];
277 -> 58;

278 [label="EVAL with clause\ndelete(X293, tree(X294, X295, X296), tree(X294, X295, X297)) :- ','(less(X294, X293), delete(X293, X296, X297)).\nand substitution\nT1 -> T264\nX293 -> T264\nX294 -> T260\nX295 -> T261\nX296 -> T265\nT2 -> tree(T260, T261, T265)\nX297 -> T263\nT11 -> tree(T260, T261, T263)\nT259 -> T264\nT262 -> T265", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 278 [arrowhead = none ];
278 -> 72;

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

280 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
58 -> 280 [arrowhead = none ];
280 -> 59;

281 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
58 -> 281 [arrowhead = none ];
281 -> 60;

282 [label="EVAL with clause\nless(0, s(X240)).\nand substitution\nT203 -> 0\nX240 -> T209\nT199 -> s(T209)\nT204 -> T210", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 282 [arrowhead = none ];
282 -> 61;

283 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 283 [arrowhead = none ];
283 -> 62;

284 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
60 -> 284 [arrowhead = none ];
284 -> 63;

285 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
60 -> 285 [arrowhead = none ];
285 -> 64;

286 [label="INSTANCE with matching:\nT1 -> 0\nT2 -> T210\nT3 -> T202", fontsize=14, style = filled, fillcolor = lightgrey];
61 -> 286 [arrowhead = none , style=dashed];
286 -> 1[style=dashed];

287 [label="EVAL with clause\nless(s(X254), s(X255)) :- less(X254, X255).\nand substitution\nX254 -> T223\nT203 -> s(T223)\nX255 -> T222\nT199 -> s(T222)\nT221 -> T223\nT204 -> T224", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 287 [arrowhead = none ];
287 -> 65;

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

289 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 289 [arrowhead = none ];
289 -> 69;

290 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
65 -> 290 [arrowhead = none ];
290 -> 67;

291 [label="SPLIT 2\nnew knowledge:\nT227 is ground\nreplacements:\nT223 -> T227\nT224 -> T228", fontsize=14, style = filled, fillcolor = violet];
65 -> 291 [arrowhead = none ];
291 -> 68;

292 [label="INSTANCE with matching:\nT126 -> T223\nT122 -> T222", fontsize=14, style = filled, fillcolor = lightgrey];
67 -> 292 [arrowhead = none , style=dashed];
292 -> 34[style=dashed];

293 [label="INSTANCE with matching:\nT1 -> s(T227)\nT2 -> T228\nT3 -> T202", fontsize=14, style = filled, fillcolor = lightgrey];
68 -> 293 [arrowhead = none , style=dashed];
293 -> 1[style=dashed];

294 [label="EVAL with clause\ndelete(X276, tree(X277, X278, X279), tree(X277, X278, X280)) :- ','(less(X277, X276), delete(X276, X279, X280)).\nand substitution\nT1 -> T250\nX276 -> T250\nX277 -> T246\nX278 -> T247\nX279 -> T251\nT2 -> tree(T246, T247, T251)\nT199 -> T246\nT202 -> T247\nT201 -> T249\nX280 -> T249\nT245 -> T250\nT248 -> T251", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 294 [arrowhead = none ];
294 -> 70;

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

296 [label="INSTANCE with matching:\nT163 -> T246\nT167 -> T250\nT168 -> T251\nT166 -> T249", fontsize=14, style = filled, fillcolor = lightgrey];
70 -> 296 [arrowhead = none , style=dashed];
296 -> 44[style=dashed];

297 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
72 -> 297 [arrowhead = none ];
297 -> 74;

298 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
74 -> 298 [arrowhead = none ];
298 -> 75;

299 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
74 -> 299 [arrowhead = none ];
299 -> 76;

300 [label="EVAL with clause\nless(0, s(X307)).\nand substitution\nT260 -> 0\nX307 -> T272\nT264 -> s(T272)\nT265 -> T271\nT270 -> T272", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 300 [arrowhead = none ];
300 -> 77;

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

302 [label="EVAL with clause\nless(s(X317), s(X318)) :- less(X317, X318).\nand substitution\nX317 -> T281\nT260 -> s(T281)\nX318 -> T283\nT264 -> s(T283)\nT282 -> T283\nT265 -> T284", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 302 [arrowhead = none ];
302 -> 79;

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

304 [label="INSTANCE with matching:\nT1 -> s(T272)\nT2 -> T271\nT3 -> T263", fontsize=14, style = filled, fillcolor = lightgrey];
77 -> 304 [arrowhead = none , style=dashed];
304 -> 1[style=dashed];

305 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
79 -> 305 [arrowhead = none ];
305 -> 81;

306 [label="SPLIT 2\nreplacements:\nT283 -> T287\nT284 -> T288", fontsize=14, style = filled, fillcolor = violet];
79 -> 306 [arrowhead = none ];
306 -> 82;

307 [label="INSTANCE with matching:\nT163 -> T281\nT167 -> T283", fontsize=14, style = filled, fillcolor = lightgrey];
81 -> 307 [arrowhead = none , style=dashed];
307 -> 46[style=dashed];

308 [label="INSTANCE with matching:\nT1 -> s(T287)\nT2 -> T288\nT3 -> T263", fontsize=14, style = filled, fillcolor = lightgrey];
82 -> 308 [arrowhead = none , style=dashed];
308 -> 1[style=dashed];

309 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
83 -> 309 [arrowhead = none ];
309 -> 85;

310 [label="EVAL with clause\ndelete(X455, tree(X456, X457, X458), tree(X456, X459, X458)) :- ','(less(X455, X456), delete(X455, X457, X459)).\nand substitution\nT1 -> T409\nX455 -> T409\nX456 -> T405\nX457 -> T410\nX458 -> T407\nT2 -> tree(T405, T410, T407)\nX459 -> T408\nT7 -> tree(T405, T408, T407)\nT404 -> T409\nT406 -> T410", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 310 [arrowhead = none ];
310 -> 102;

311 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 311 [arrowhead = none ];
311 -> 103;

312 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
85 -> 312 [arrowhead = none ];
312 -> 86;

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

314 [label="EVAL with clause\ndelmin(tree(X352, void, X353), X352, X353).\nand substitution\nX352 -> T314\nX353 -> T315\nT305 -> tree(T314, void, T315)\nT303 -> T314\nT304 -> T315", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 314 [arrowhead = none ];
314 -> 88;

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

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

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

318 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 318 [arrowhead = none ];
318 -> 90;

319 [label="EVAL with clause\ndelmin(tree(X380, X381, X382), X383, tree(X380, X384, X385)) :- delmin(X381, X383, X384).\nand substitution\nX380 -> T340\nX381 -> T346\nX382 -> T342\nT305 -> tree(T340, T346, T342)\nT303 -> T343\nX383 -> T343\nX384 -> T344\nX385 -> T345\nT304 -> tree(T340, T344, T345)\nT341 -> T346", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 319 [arrowhead = none ];
319 -> 93;

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

321 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
92 -> 321 [arrowhead = none ];
321 -> 95;

322 [label="INSTANCE with matching:\nT63 -> T346\nT60 -> T343\nT61 -> T344", fontsize=14, style = filled, fillcolor = lightgrey];
93 -> 322 [arrowhead = none , style=dashed];
322 -> 19[style=dashed];

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

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

325 [label="EVAL with clause\ndelete(X416, tree(X417, X418, X419), tree(X417, X420, X419)) :- ','(less(X416, X417), delete(X416, X418, X420)).\nand substitution\nT1 -> T376\nX416 -> T376\nX417 -> T372\nX418 -> T377\nX419 -> T374\nT2 -> tree(T372, T377, T374)\nT303 -> T372\nT301 -> T375\nX420 -> T375\nT304 -> T374\nT371 -> T376\nT373 -> T377", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 325 [arrowhead = none ];
325 -> 98;

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

327 [label="EVAL with clause\ndelete(X438, tree(X439, X440, X441), tree(X439, X440, X442)) :- ','(less(X439, X438), delete(X438, X441, X442)).\nand substitution\nT1 -> T395\nX438 -> T395\nX439 -> T391\nX440 -> T392\nX441 -> T396\nT2 -> tree(T391, T392, T396)\nT303 -> T391\nT301 -> T392\nT304 -> T394\nX442 -> T394\nT390 -> T395\nT393 -> T396", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 327 [arrowhead = none ];
327 -> 100;

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

329 [label="INSTANCE with matching:\nT126 -> T376\nT122 -> T372\nT127 -> T377\nT125 -> T375", fontsize=14, style = filled, fillcolor = lightgrey];
98 -> 329 [arrowhead = none , style=dashed];
329 -> 32[style=dashed];

330 [label="INSTANCE with matching:\nT260 -> T391\nT264 -> T395\nT265 -> T396\nT263 -> T394", fontsize=14, style = filled, fillcolor = lightgrey];
100 -> 330 [arrowhead = none , style=dashed];
330 -> 72[style=dashed];

331 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
102 -> 331 [arrowhead = none ];
331 -> 104;

332 [label="EVAL with clause\ndelete(X516, tree(X517, X518, X519), tree(X517, X518, X520)) :- ','(less(X517, X516), delete(X516, X519, X520)).\nand substitution\nT1 -> T462\nX516 -> T462\nX517 -> T458\nX518 -> T459\nX519 -> T463\nT2 -> tree(T458, T459, T463)\nX520 -> T461\nT7 -> tree(T458, T459, T461)\nT457 -> T462\nT460 -> T463", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 332 [arrowhead = none ];
332 -> 116;

333 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 333 [arrowhead = none ];
333 -> 117;

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

335 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
104 -> 335 [arrowhead = none ];
335 -> 106;

336 [label="EVAL with clause\nless(0, s(X469)).\nand substitution\nT409 -> 0\nX469 -> T415\nT405 -> s(T415)\nT410 -> T416", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 336 [arrowhead = none ];
336 -> 107;

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

338 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
106 -> 338 [arrowhead = none ];
338 -> 109;

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

340 [label="INSTANCE with matching:\nT1 -> 0\nT2 -> T416\nT3 -> T408", fontsize=14, style = filled, fillcolor = lightgrey];
107 -> 340 [arrowhead = none , style=dashed];
340 -> 1[style=dashed];

341 [label="EVAL with clause\nless(s(X483), s(X484)) :- less(X483, X484).\nand substitution\nX483 -> T429\nT409 -> s(T429)\nX484 -> T428\nT405 -> s(T428)\nT427 -> T429\nT410 -> T430", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 341 [arrowhead = none ];
341 -> 111;

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

343 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
110 -> 343 [arrowhead = none ];
343 -> 113;

344 [label="INSTANCE with matching:\nT223 -> T429\nT222 -> T428\nT224 -> T430\nT202 -> T408", fontsize=14, style = filled, fillcolor = lightgrey];
111 -> 344 [arrowhead = none , style=dashed];
344 -> 65[style=dashed];

345 [label="EVAL with clause\ndelete(X499, tree(X500, X501, X502), tree(X500, X501, X503)) :- ','(less(X500, X499), delete(X499, X502, X503)).\nand substitution\nT1 -> T448\nX499 -> T448\nX500 -> T444\nX501 -> T445\nX502 -> T449\nT2 -> tree(T444, T445, T449)\nT405 -> T444\nT408 -> T445\nT407 -> T447\nX503 -> T447\nT443 -> T448\nT446 -> T449", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 345 [arrowhead = none ];
345 -> 114;

346 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 346 [arrowhead = none ];
346 -> 115;

347 [label="INSTANCE with matching:\nT260 -> T444\nT264 -> T448\nT265 -> T449\nT263 -> T447", fontsize=14, style = filled, fillcolor = lightgrey];
114 -> 347 [arrowhead = none , style=dashed];
347 -> 72[style=dashed];

348 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
116 -> 348 [arrowhead = none ];
348 -> 118;

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

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

351 [label="EVAL with clause\nless(0, s(X530)).\nand substitution\nT458 -> 0\nX530 -> T470\nT462 -> s(T470)\nT463 -> T469\nT468 -> T470", fontsize=14, style = filled, fillcolor = lightblue];
119 -> 351 [arrowhead = none ];
351 -> 121;

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

353 [label="EVAL with clause\nless(s(X540), s(X541)) :- less(X540, X541).\nand substitution\nX540 -> T479\nT458 -> s(T479)\nX541 -> T481\nT462 -> s(T481)\nT480 -> T481\nT463 -> T482", fontsize=14, style = filled, fillcolor = lightblue];
120 -> 353 [arrowhead = none ];
353 -> 123;

354 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
120 -> 354 [arrowhead = none ];
354 -> 124;

355 [label="INSTANCE with matching:\nT1 -> s(T470)\nT2 -> T469\nT3 -> T461", fontsize=14, style = filled, fillcolor = lightgrey];
121 -> 355 [arrowhead = none , style=dashed];
355 -> 1[style=dashed];

356 [label="INSTANCE with matching:\nT281 -> T479\nT283 -> T481\nT284 -> T482\nT263 -> T461", fontsize=14, style = filled, fillcolor = lightgrey];
123 -> 356 [arrowhead = none , style=dashed];
356 -> 79[style=dashed];

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

358 [label="EVAL with clause\ndelete(X774, tree(X774, X775, X776), tree(X777, X775, X778)) :- delmin(X776, X777, X778).\nand substitution\nT1 -> T684\nX774 -> T684\nX775 -> T685\nX776 -> T689\nT2 -> tree(T684, T685, T689)\nX777 -> T687\nX778 -> T688\nT3 -> tree(T687, T685, T688)\nT686 -> T689", fontsize=14, style = filled, fillcolor = lightblue];
126 -> 358 [arrowhead = none ];
358 -> 170;

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

360 [label="EVAL with clause\ndelete(X557, tree(X557, X558, X559), tree(X560, X558, X561)) :- delmin(X559, X560, X561).\nand substitution\nT1 -> T494\nX557 -> T494\nX558 -> T495\nX559 -> T499\nT2 -> tree(T494, T495, T499)\nX560 -> T497\nX561 -> T498\nT488 -> tree(T497, T495, T498)\nT496 -> T499", fontsize=14, style = filled, fillcolor = lightblue];
127 -> 360 [arrowhead = none ];
360 -> 128;

361 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
127 -> 361 [arrowhead = none ];
361 -> 129;

362 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
128 -> 362 [arrowhead = none ];
362 -> 130;

363 [label="EVAL with clause\ndelete(X678, tree(X679, X680, X681), tree(X679, X682, X681)) :- ','(less(X678, X679), delete(X678, X680, X682)).\nand substitution\nT1 -> T603\nX678 -> T603\nX679 -> T599\nX680 -> T604\nX681 -> T601\nT2 -> tree(T599, T604, T601)\nX682 -> T602\nT488 -> tree(T599, T602, T601)\nT598 -> T603\nT600 -> T604", fontsize=14, style = filled, fillcolor = lightblue];
129 -> 363 [arrowhead = none ];
363 -> 147;

364 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
129 -> 364 [arrowhead = none ];
364 -> 148;

365 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
130 -> 365 [arrowhead = none ];
365 -> 131;

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

367 [label="EVAL with clause\ndelmin(tree(X575, void, X576), X575, X576).\nand substitution\nX575 -> T508\nX576 -> T509\nT499 -> tree(T508, void, T509)\nT497 -> T508\nT498 -> T509", fontsize=14, style = filled, fillcolor = lightblue];
131 -> 367 [arrowhead = none ];
367 -> 133;

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

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

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

371 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
133 -> 371 [arrowhead = none ];
371 -> 135;

372 [label="EVAL with clause\ndelmin(tree(X603, X604, X605), X606, tree(X603, X607, X608)) :- delmin(X604, X606, X607).\nand substitution\nX603 -> T534\nX604 -> T540\nX605 -> T536\nT499 -> tree(T534, T540, T536)\nT497 -> T537\nX606 -> T537\nX607 -> T538\nX608 -> T539\nT498 -> tree(T534, T538, T539)\nT535 -> T540", fontsize=14, style = filled, fillcolor = lightblue];
136 -> 372 [arrowhead = none ];
372 -> 138;

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

374 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
137 -> 374 [arrowhead = none ];
374 -> 140;

375 [label="INSTANCE with matching:\nT346 -> T540\nT343 -> T537\nT344 -> T538", fontsize=14, style = filled, fillcolor = lightgrey];
138 -> 375 [arrowhead = none , style=dashed];
375 -> 93[style=dashed];

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

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

378 [label="EVAL with clause\ndelete(X639, tree(X640, X641, X642), tree(X640, X643, X642)) :- ','(less(X639, X640), delete(X639, X641, X643)).\nand substitution\nT1 -> T570\nX639 -> T570\nX640 -> T566\nX641 -> T571\nX642 -> T568\nT2 -> tree(T566, T571, T568)\nT497 -> T566\nT495 -> T569\nX643 -> T569\nT498 -> T568\nT565 -> T570\nT567 -> T571", fontsize=14, style = filled, fillcolor = lightblue];
141 -> 378 [arrowhead = none ];
378 -> 143;

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

380 [label="EVAL with clause\ndelete(X661, tree(X662, X663, X664), tree(X662, X663, X665)) :- ','(less(X662, X661), delete(X661, X664, X665)).\nand substitution\nT1 -> T589\nX661 -> T589\nX662 -> T585\nX663 -> T586\nX664 -> T590\nT2 -> tree(T585, T586, T590)\nT497 -> T585\nT495 -> T586\nT498 -> T588\nX665 -> T588\nT584 -> T589\nT587 -> T590", fontsize=14, style = filled, fillcolor = lightblue];
142 -> 380 [arrowhead = none ];
380 -> 145;

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

382 [label="INSTANCE with matching:\nT376 -> T570\nT372 -> T566\nT377 -> T571\nT375 -> T569", fontsize=14, style = filled, fillcolor = lightgrey];
143 -> 382 [arrowhead = none , style=dashed];
382 -> 98[style=dashed];

383 [label="INSTANCE with matching:\nT458 -> T585\nT462 -> T589\nT463 -> T590\nT461 -> T588", fontsize=14, style = filled, fillcolor = lightgrey];
145 -> 383 [arrowhead = none , style=dashed];
383 -> 116[style=dashed];

384 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
147 -> 384 [arrowhead = none ];
384 -> 149;

385 [label="EVAL with clause\ndelete(X739, tree(X740, X741, X742), tree(X740, X741, X743)) :- ','(less(X740, X739), delete(X739, X742, X743)).\nand substitution\nT1 -> T656\nX739 -> T656\nX740 -> T652\nX741 -> T653\nX742 -> T657\nT2 -> tree(T652, T653, T657)\nX743 -> T655\nT488 -> tree(T652, T653, T655)\nT651 -> T656\nT654 -> T657", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 385 [arrowhead = none ];
385 -> 161;

386 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 386 [arrowhead = none ];
386 -> 162;

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

388 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
149 -> 388 [arrowhead = none ];
388 -> 151;

389 [label="EVAL with clause\nless(0, s(X692)).\nand substitution\nT603 -> 0\nX692 -> T609\nT599 -> s(T609)\nT604 -> T610", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 389 [arrowhead = none ];
389 -> 152;

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

391 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
151 -> 391 [arrowhead = none ];
391 -> 154;

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

393 [label="INSTANCE with matching:\nT1 -> 0\nT2 -> T610\nT3 -> T602", fontsize=14, style = filled, fillcolor = lightgrey];
152 -> 393 [arrowhead = none , style=dashed];
393 -> 1[style=dashed];

394 [label="EVAL with clause\nless(s(X706), s(X707)) :- less(X706, X707).\nand substitution\nX706 -> T623\nT603 -> s(T623)\nX707 -> T622\nT599 -> s(T622)\nT621 -> T623\nT604 -> T624", fontsize=14, style = filled, fillcolor = lightblue];
154 -> 394 [arrowhead = none ];
394 -> 156;

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

396 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
155 -> 396 [arrowhead = none ];
396 -> 158;

397 [label="INSTANCE with matching:\nT429 -> T623\nT428 -> T622\nT430 -> T624\nT408 -> T602", fontsize=14, style = filled, fillcolor = lightgrey];
156 -> 397 [arrowhead = none , style=dashed];
397 -> 111[style=dashed];

398 [label="EVAL with clause\ndelete(X722, tree(X723, X724, X725), tree(X723, X724, X726)) :- ','(less(X723, X722), delete(X722, X725, X726)).\nand substitution\nT1 -> T642\nX722 -> T642\nX723 -> T638\nX724 -> T639\nX725 -> T643\nT2 -> tree(T638, T639, T643)\nT599 -> T638\nT602 -> T639\nT601 -> T641\nX726 -> T641\nT637 -> T642\nT640 -> T643", fontsize=14, style = filled, fillcolor = lightblue];
158 -> 398 [arrowhead = none ];
398 -> 159;

399 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
158 -> 399 [arrowhead = none ];
399 -> 160;

400 [label="INSTANCE with matching:\nT458 -> T638\nT462 -> T642\nT463 -> T643\nT461 -> T641", fontsize=14, style = filled, fillcolor = lightgrey];
159 -> 400 [arrowhead = none , style=dashed];
400 -> 116[style=dashed];

401 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
161 -> 401 [arrowhead = none ];
401 -> 163;

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

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

404 [label="EVAL with clause\nless(0, s(X753)).\nand substitution\nT652 -> 0\nX753 -> T664\nT656 -> s(T664)\nT657 -> T663\nT662 -> T664", fontsize=14, style = filled, fillcolor = lightblue];
164 -> 404 [arrowhead = none ];
404 -> 166;

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

406 [label="EVAL with clause\nless(s(X763), s(X764)) :- less(X763, X764).\nand substitution\nX763 -> T673\nT652 -> s(T673)\nX764 -> T675\nT656 -> s(T675)\nT674 -> T675\nT657 -> T676", fontsize=14, style = filled, fillcolor = lightblue];
165 -> 406 [arrowhead = none ];
406 -> 168;

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

408 [label="INSTANCE with matching:\nT1 -> s(T664)\nT2 -> T663\nT3 -> T655", fontsize=14, style = filled, fillcolor = lightgrey];
166 -> 408 [arrowhead = none , style=dashed];
408 -> 1[style=dashed];

409 [label="INSTANCE with matching:\nT479 -> T673\nT481 -> T675\nT482 -> T676\nT461 -> T655", fontsize=14, style = filled, fillcolor = lightgrey];
168 -> 409 [arrowhead = none , style=dashed];
409 -> 123[style=dashed];

410 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
170 -> 410 [arrowhead = none ];
410 -> 172;

411 [label="EVAL with clause\ndelete(X895, tree(X896, X897, X898), tree(X896, X899, X898)) :- ','(less(X895, X896), delete(X895, X897, X899)).\nand substitution\nT1 -> T793\nX895 -> T793\nX896 -> T789\nX897 -> T794\nX898 -> T791\nT2 -> tree(T789, T794, T791)\nX899 -> T792\nT3 -> tree(T789, T792, T791)\nT788 -> T793\nT790 -> T794", fontsize=14, style = filled, fillcolor = lightblue];
171 -> 411 [arrowhead = none ];
411 -> 189;

412 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
171 -> 412 [arrowhead = none ];
412 -> 190;

413 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
172 -> 413 [arrowhead = none ];
413 -> 173;

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

415 [label="EVAL with clause\ndelmin(tree(X792, void, X793), X792, X793).\nand substitution\nX792 -> T698\nX793 -> T699\nT689 -> tree(T698, void, T699)\nT687 -> T698\nT688 -> T699", fontsize=14, style = filled, fillcolor = lightblue];
173 -> 415 [arrowhead = none ];
415 -> 175;

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

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

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

419 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
175 -> 419 [arrowhead = none ];
419 -> 177;

420 [label="EVAL with clause\ndelmin(tree(X820, X821, X822), X823, tree(X820, X824, X825)) :- delmin(X821, X823, X824).\nand substitution\nX820 -> T724\nX821 -> T730\nX822 -> T726\nT689 -> tree(T724, T730, T726)\nT687 -> T727\nX823 -> T727\nX824 -> T728\nX825 -> T729\nT688 -> tree(T724, T728, T729)\nT725 -> T730", fontsize=14, style = filled, fillcolor = lightblue];
178 -> 420 [arrowhead = none ];
420 -> 180;

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

422 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
179 -> 422 [arrowhead = none ];
422 -> 182;

423 [label="INSTANCE with matching:\nT346 -> T730\nT343 -> T727\nT344 -> T728", fontsize=14, style = filled, fillcolor = lightgrey];
180 -> 423 [arrowhead = none , style=dashed];
423 -> 93[style=dashed];

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

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

426 [label="EVAL with clause\ndelete(X856, tree(X857, X858, X859), tree(X857, X860, X859)) :- ','(less(X856, X857), delete(X856, X858, X860)).\nand substitution\nT1 -> T760\nX856 -> T760\nX857 -> T756\nX858 -> T761\nX859 -> T758\nT2 -> tree(T756, T761, T758)\nT687 -> T756\nT685 -> T759\nX860 -> T759\nT688 -> T758\nT755 -> T760\nT757 -> T761", fontsize=14, style = filled, fillcolor = lightblue];
183 -> 426 [arrowhead = none ];
426 -> 185;

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

428 [label="EVAL with clause\ndelete(X878, tree(X879, X880, X881), tree(X879, X880, X882)) :- ','(less(X879, X878), delete(X878, X881, X882)).\nand substitution\nT1 -> T779\nX878 -> T779\nX879 -> T775\nX880 -> T776\nX881 -> T780\nT2 -> tree(T775, T776, T780)\nT687 -> T775\nT685 -> T776\nT688 -> T778\nX882 -> T778\nT774 -> T779\nT777 -> T780", fontsize=14, style = filled, fillcolor = lightblue];
184 -> 428 [arrowhead = none ];
428 -> 187;

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

430 [label="INSTANCE with matching:\nT376 -> T760\nT372 -> T756\nT377 -> T761\nT375 -> T759", fontsize=14, style = filled, fillcolor = lightgrey];
185 -> 430 [arrowhead = none , style=dashed];
430 -> 98[style=dashed];

431 [label="INSTANCE with matching:\nT458 -> T775\nT462 -> T779\nT463 -> T780\nT461 -> T778", fontsize=14, style = filled, fillcolor = lightgrey];
187 -> 431 [arrowhead = none , style=dashed];
431 -> 116[style=dashed];

432 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
189 -> 432 [arrowhead = none ];
432 -> 191;

433 [label="EVAL with clause\ndelete(X956, tree(X957, X958, X959), tree(X957, X958, X960)) :- ','(less(X957, X956), delete(X956, X959, X960)).\nand substitution\nT1 -> T846\nX956 -> T846\nX957 -> T842\nX958 -> T843\nX959 -> T847\nT2 -> tree(T842, T843, T847)\nX960 -> T845\nT3 -> tree(T842, T843, T845)\nT841 -> T846\nT844 -> T847", fontsize=14, style = filled, fillcolor = lightblue];
190 -> 433 [arrowhead = none ];
433 -> 203;

434 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
190 -> 434 [arrowhead = none ];
434 -> 204;

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

436 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
191 -> 436 [arrowhead = none ];
436 -> 193;

437 [label="EVAL with clause\nless(0, s(X909)).\nand substitution\nT793 -> 0\nX909 -> T799\nT789 -> s(T799)\nT794 -> T800", fontsize=14, style = filled, fillcolor = lightblue];
192 -> 437 [arrowhead = none ];
437 -> 194;

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

439 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
193 -> 439 [arrowhead = none ];
439 -> 196;

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

441 [label="INSTANCE with matching:\nT1 -> 0\nT2 -> T800\nT3 -> T792", fontsize=14, style = filled, fillcolor = lightgrey];
194 -> 441 [arrowhead = none , style=dashed];
441 -> 1[style=dashed];

442 [label="EVAL with clause\nless(s(X923), s(X924)) :- less(X923, X924).\nand substitution\nX923 -> T813\nT793 -> s(T813)\nX924 -> T812\nT789 -> s(T812)\nT811 -> T813\nT794 -> T814", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 442 [arrowhead = none ];
442 -> 198;

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

444 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
197 -> 444 [arrowhead = none ];
444 -> 200;

445 [label="INSTANCE with matching:\nT429 -> T813\nT428 -> T812\nT430 -> T814\nT408 -> T792", fontsize=14, style = filled, fillcolor = lightgrey];
198 -> 445 [arrowhead = none , style=dashed];
445 -> 111[style=dashed];

446 [label="EVAL with clause\ndelete(X939, tree(X940, X941, X942), tree(X940, X941, X943)) :- ','(less(X940, X939), delete(X939, X942, X943)).\nand substitution\nT1 -> T832\nX939 -> T832\nX940 -> T828\nX941 -> T829\nX942 -> T833\nT2 -> tree(T828, T829, T833)\nT789 -> T828\nT792 -> T829\nT791 -> T831\nX943 -> T831\nT827 -> T832\nT830 -> T833", fontsize=14, style = filled, fillcolor = lightblue];
200 -> 446 [arrowhead = none ];
446 -> 201;

447 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
200 -> 447 [arrowhead = none ];
447 -> 202;

448 [label="INSTANCE with matching:\nT458 -> T828\nT462 -> T832\nT463 -> T833\nT461 -> T831", fontsize=14, style = filled, fillcolor = lightgrey];
201 -> 448 [arrowhead = none , style=dashed];
448 -> 116[style=dashed];

449 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
203 -> 449 [arrowhead = none ];
449 -> 205;

450 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
205 -> 450 [arrowhead = none ];
450 -> 206;

451 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
205 -> 451 [arrowhead = none ];
451 -> 207;

452 [label="EVAL with clause\nless(0, s(X970)).\nand substitution\nT842 -> 0\nX970 -> T854\nT846 -> s(T854)\nT847 -> T853\nT852 -> T854", fontsize=14, style = filled, fillcolor = lightblue];
206 -> 452 [arrowhead = none ];
452 -> 208;

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

454 [label="EVAL with clause\nless(s(X980), s(X981)) :- less(X980, X981).\nand substitution\nX980 -> T863\nT842 -> s(T863)\nX981 -> T865\nT846 -> s(T865)\nT864 -> T865\nT847 -> T866", fontsize=14, style = filled, fillcolor = lightblue];
207 -> 454 [arrowhead = none ];
454 -> 210;

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

456 [label="INSTANCE with matching:\nT1 -> s(T854)\nT2 -> T853\nT3 -> T845", fontsize=14, style = filled, fillcolor = lightgrey];
208 -> 456 [arrowhead = none , style=dashed];
456 -> 1[style=dashed];

457 [label="INSTANCE with matching:\nT479 -> T863\nT481 -> T865\nT482 -> T866\nT461 -> T845", fontsize=14, style = filled, fillcolor = lightgrey];
210 -> 457 [arrowhead = none , style=dashed];
457 -> 123[style=dashed];

}

(2) Obligation:

Triples:

delmin19(tree(T90, T96, T92), T93, tree(T90, T94, T95)) :- delmin19(T96, T93, T94).
less34(s(T145), s(T144)) :- less34(T145, T144).
less46(s(T184), s(T186)) :- less46(T184, T186).
p44(T163, T167, T168, T166) :- less46(T163, T167).
p44(T163, T171, T172, T166) :- ','(lessc46(T163, T171), delete1(T171, T172, T166)).
p32(T126, T122, T127, T125) :- less34(T126, T122).
p32(T130, T122, T131, T125) :- ','(lessc34(T130, T122), delete1(T130, T131, T125)).
p72(0, s(T272), T271, T263) :- delete1(s(T272), T271, T263).
p72(s(T281), s(T283), T284, T263) :- p79(T281, T283, T284, T263).
p65(T223, T222, T224, T202) :- less34(T223, T222).
p65(T227, T222, T228, T202) :- ','(lessc34(T227, T222), delete1(s(T227), T228, T202)).
p79(T281, T283, T284, T263) :- less46(T281, T283).
p79(T281, T287, T288, T263) :- ','(lessc46(T281, T287), delete1(s(T287), T288, T263)).
p116(0, s(T470), T469, T461) :- delete1(s(T470), T469, T461).
p116(s(T479), s(T481), T482, T461) :- p79(T479, T481, T482, T461).
delete1(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) :- delmin19(T63, T60, T61).
delete1(T126, tree(T122, T127, T124), tree(T122, T125, T124)) :- p32(T126, T122, T127, T125).
delete1(T167, tree(T163, T164, T168), tree(T163, T164, T166)) :- p44(T163, T167, T168, T166).
delete1(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) :- delete1(0, T210, T202).
delete1(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) :- p65(T223, T222, T224, T202).
delete1(T250, tree(T246, T247, T251), tree(T246, T247, T249)) :- p44(T246, T250, T251, T249).
delete1(T264, tree(T260, T261, T265), tree(T260, T261, T263)) :- p72(T260, T264, T265, T263).
delete1(T300, tree(T300, T301, tree(T340, T346, T342)), tree(T343, T301, tree(T340, T344, T345))) :- delmin19(T346, T343, T344).
delete1(T376, tree(T372, T377, T374), tree(T372, T375, T374)) :- p32(T376, T372, T377, T375).
delete1(T395, tree(T391, T392, T396), tree(T391, T392, T394)) :- p72(T391, T395, T396, T394).
delete1(0, tree(s(T415), T416, T407), tree(s(T415), T408, T407)) :- delete1(0, T416, T408).
delete1(s(T429), tree(s(T428), T430, T407), tree(s(T428), T408, T407)) :- p65(T429, T428, T430, T408).
delete1(T448, tree(T444, T445, T449), tree(T444, T445, T447)) :- p72(T444, T448, T449, T447).
delete1(T462, tree(T458, T459, T463), tree(T458, T459, T461)) :- p116(T458, T462, T463, T461).
delete1(T494, tree(T494, T495, tree(T534, T540, T536)), tree(T537, T495, tree(T534, T538, T539))) :- delmin19(T540, T537, T538).
delete1(T570, tree(T566, T571, T568), tree(T566, T569, T568)) :- p32(T570, T566, T571, T569).
delete1(T589, tree(T585, T586, T590), tree(T585, T586, T588)) :- p116(T585, T589, T590, T588).
delete1(0, tree(s(T609), T610, T601), tree(s(T609), T602, T601)) :- delete1(0, T610, T602).
delete1(s(T623), tree(s(T622), T624, T601), tree(s(T622), T602, T601)) :- p65(T623, T622, T624, T602).
delete1(T642, tree(T638, T639, T643), tree(T638, T639, T641)) :- p116(T638, T642, T643, T641).
delete1(s(T664), tree(0, T653, T663), tree(0, T653, T655)) :- delete1(s(T664), T663, T655).
delete1(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) :- p79(T673, T675, T676, T655).
delete1(T684, tree(T684, T685, tree(T724, T730, T726)), tree(T727, T685, tree(T724, T728, T729))) :- delmin19(T730, T727, T728).
delete1(T760, tree(T756, T761, T758), tree(T756, T759, T758)) :- p32(T760, T756, T761, T759).
delete1(T779, tree(T775, T776, T780), tree(T775, T776, T778)) :- p116(T775, T779, T780, T778).
delete1(0, tree(s(T799), T800, T791), tree(s(T799), T792, T791)) :- delete1(0, T800, T792).
delete1(s(T813), tree(s(T812), T814, T791), tree(s(T812), T792, T791)) :- p65(T813, T812, T814, T792).
delete1(T832, tree(T828, T829, T833), tree(T828, T829, T831)) :- p116(T828, T832, T833, T831).
delete1(s(T854), tree(0, T843, T853), tree(0, T843, T845)) :- delete1(s(T854), T853, T845).
delete1(s(T865), tree(s(T863), T843, T866), tree(s(T863), T843, T845)) :- p79(T863, T865, T866, T845).

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(T126, tree(T122, T127, T124), tree(T122, T125, T124)) :- qc32(T126, T122, T127, T125).
deletec1(T167, tree(T163, T164, T168), tree(T163, T164, T166)) :- qc44(T163, T167, T168, T166).
deletec1(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) :- deletec1(0, T210, T202).
deletec1(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) :- qc65(T223, T222, T224, T202).
deletec1(T250, tree(T246, T247, T251), tree(T246, T247, T249)) :- qc44(T246, T250, T251, T249).
deletec1(T264, tree(T260, T261, T265), tree(T260, T261, T263)) :- qc72(T260, T264, T265, T263).
deletec1(T300, tree(T300, T301, tree(T314, void, T315)), tree(T314, T301, T315)).
deletec1(T300, tree(T300, T301, tree(T340, T346, T342)), tree(T343, T301, tree(T340, T344, T345))) :- delminc19(T346, T343, T344).
deletec1(T376, tree(T372, T377, T374), tree(T372, T375, T374)) :- qc32(T376, T372, T377, T375).
deletec1(T395, tree(T391, T392, T396), tree(T391, T392, T394)) :- qc72(T391, T395, T396, T394).
deletec1(0, tree(s(T415), T416, T407), tree(s(T415), T408, T407)) :- deletec1(0, T416, T408).
deletec1(s(T429), tree(s(T428), T430, T407), tree(s(T428), T408, T407)) :- qc65(T429, T428, T430, T408).
deletec1(T448, tree(T444, T445, T449), tree(T444, T445, T447)) :- qc72(T444, T448, T449, T447).
deletec1(T462, tree(T458, T459, T463), tree(T458, T459, T461)) :- qc116(T458, T462, T463, T461).
deletec1(T487, tree(T487, T488, void), T488).
deletec1(T494, tree(T494, T495, tree(T508, void, T509)), tree(T508, T495, T509)).
deletec1(T494, tree(T494, T495, tree(T534, T540, T536)), tree(T537, T495, tree(T534, T538, T539))) :- delminc19(T540, T537, T538).
deletec1(T570, tree(T566, T571, T568), tree(T566, T569, T568)) :- qc32(T570, T566, T571, T569).
deletec1(T589, tree(T585, T586, T590), tree(T585, T586, T588)) :- qc116(T585, T589, T590, T588).
deletec1(0, tree(s(T609), T610, T601), tree(s(T609), T602, T601)) :- deletec1(0, T610, T602).
deletec1(s(T623), tree(s(T622), T624, T601), tree(s(T622), T602, T601)) :- qc65(T623, T622, T624, T602).
deletec1(T642, tree(T638, T639, T643), tree(T638, T639, T641)) :- qc116(T638, T642, T643, T641).
deletec1(s(T664), tree(0, T653, T663), tree(0, T653, T655)) :- deletec1(s(T664), T663, T655).
deletec1(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) :- qc79(T673, T675, T676, T655).
deletec1(T684, tree(T684, T685, tree(T698, void, T699)), tree(T698, T685, T699)).
deletec1(T684, tree(T684, T685, tree(T724, T730, T726)), tree(T727, T685, tree(T724, T728, T729))) :- delminc19(T730, T727, T728).
deletec1(T760, tree(T756, T761, T758), tree(T756, T759, T758)) :- qc32(T760, T756, T761, T759).
deletec1(T779, tree(T775, T776, T780), tree(T775, T776, T778)) :- qc116(T775, T779, T780, T778).
deletec1(0, tree(s(T799), T800, T791), tree(s(T799), T792, T791)) :- deletec1(0, T800, T792).
deletec1(s(T813), tree(s(T812), T814, T791), tree(s(T812), T792, T791)) :- qc65(T813, T812, T814, T792).
deletec1(T832, tree(T828, T829, T833), tree(T828, T829, T831)) :- qc116(T828, T832, T833, T831).
deletec1(s(T854), tree(0, T843, T853), tree(0, T843, T845)) :- deletec1(s(T854), T853, T845).
deletec1(s(T865), tree(s(T863), T843, T866), tree(s(T863), T843, T845)) :- qc79(T863, T865, T866, T845).
lessc34(0, s(T138)).
lessc34(s(T145), s(T144)) :- lessc34(T145, T144).
lessc46(0, s(T179)).
lessc46(s(T184), s(T186)) :- lessc46(T184, T186).
qc44(T163, T171, T172, T166) :- ','(lessc46(T163, T171), deletec1(T171, T172, T166)).
qc32(T130, T122, T131, T125) :- ','(lessc34(T130, T122), deletec1(T130, T131, T125)).
qc72(0, s(T272), T271, T263) :- deletec1(s(T272), T271, T263).
qc72(s(T281), s(T283), T284, T263) :- qc79(T281, T283, T284, T263).
qc65(T227, T222, T228, T202) :- ','(lessc34(T227, T222), deletec1(s(T227), T228, T202)).
qc79(T281, T287, T288, T263) :- ','(lessc46(T281, T287), deletec1(s(T287), T288, T263)).
qc116(0, s(T470), T469, T461) :- deletec1(s(T470), T469, T461).
qc116(s(T479), s(T481), T482, T461) :- qc79(T479, T481, T482, T461).

Afs:

delete1(x1, x2, x3) = delete1(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: (f,f,b) (b,f,b)
delmin19_in: (f,b,b)
p32_in: (f,b,f,b) (b,b,f,b)
less34_in: (f,b) (b,b)
lessc34_in: (f,b) (b,b)
p44_in: (b,b,f,b) (b,f,f,b)
less46_in: (b,b) (b,f)
lessc46_in: (b,b) (b,f)
p65_in: (b,b,f,b) (f,b,f,b)
p72_in: (b,b,f,b) (b,f,f,b)
p79_in: (b,b,f,b) (b,f,f,b)
p116_in: (b,b,f,b) (b,f,f,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

DELETE1_IN_AAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U20_AAG(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_in_agg(T63, T60, T61))
DELETE1_IN_AAG(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_AAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → U21_AAG(T126, T122, T127, T124, T125, p32_in_agag(T126, T122, T127, T125))
DELETE1_IN_AAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → P32_IN_AGAG(T126, T122, T127, T125)
P32_IN_AGAG(T126, T122, T127, T125) → U7_AGAG(T126, T122, T127, T125, less34_in_ag(T126, T122))
P32_IN_AGAG(T126, T122, T127, T125) → LESS34_IN_AG(T126, T122)
LESS34_IN_AG(s(T145), s(T144)) → U2_AG(T145, T144, less34_in_ag(T145, T144))
LESS34_IN_AG(s(T145), s(T144)) → LESS34_IN_AG(T145, T144)
P32_IN_AGAG(T130, T122, T131, T125) → U8_AGAG(T130, T122, T131, T125, lessc34_in_ag(T130, T122))
U8_AGAG(T130, T122, T131, T125, lessc34_out_ag(T130, T122)) → U9_AGAG(T130, T122, T131, T125, delete1_in_gag(T130, T131, T125))
U8_AGAG(T130, T122, T131, T125, lessc34_out_ag(T130, T122)) → DELETE1_IN_GAG(T130, T131, T125)
DELETE1_IN_GAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U20_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)
DELETE1_IN_GAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → U21_GAG(T126, T122, T127, T124, T125, p32_in_ggag(T126, T122, T127, T125))
DELETE1_IN_GAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → P32_IN_GGAG(T126, T122, T127, T125)
P32_IN_GGAG(T126, T122, T127, T125) → U7_GGAG(T126, T122, T127, T125, less34_in_gg(T126, T122))
P32_IN_GGAG(T126, T122, T127, T125) → LESS34_IN_GG(T126, T122)
LESS34_IN_GG(s(T145), s(T144)) → U2_GG(T145, T144, less34_in_gg(T145, T144))
LESS34_IN_GG(s(T145), s(T144)) → LESS34_IN_GG(T145, T144)
P32_IN_GGAG(T130, T122, T131, T125) → U8_GGAG(T130, T122, T131, T125, lessc34_in_gg(T130, T122))
U8_GGAG(T130, T122, T131, T125, lessc34_out_gg(T130, T122)) → U9_GGAG(T130, T122, T131, T125, delete1_in_gag(T130, T131, T125))
U8_GGAG(T130, T122, T131, T125, lessc34_out_gg(T130, T122)) → DELETE1_IN_GAG(T130, T131, T125)
DELETE1_IN_GAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → U22_GAG(T167, T163, T164, T168, T166, p44_in_ggag(T163, T167, T168, T166))
DELETE1_IN_GAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → P44_IN_GGAG(T163, T167, T168, T166)
P44_IN_GGAG(T163, T167, T168, T166) → U4_GGAG(T163, T167, T168, T166, less46_in_gg(T163, T167))
P44_IN_GGAG(T163, T167, T168, T166) → LESS46_IN_GG(T163, T167)
LESS46_IN_GG(s(T184), s(T186)) → U3_GG(T184, T186, less46_in_gg(T184, T186))
LESS46_IN_GG(s(T184), s(T186)) → LESS46_IN_GG(T184, T186)
P44_IN_GGAG(T163, T171, T172, T166) → U5_GGAG(T163, T171, T172, T166, lessc46_in_gg(T163, T171))
U5_GGAG(T163, T171, T172, T166, lessc46_out_gg(T163, T171)) → U6_GGAG(T163, T171, T172, T166, delete1_in_gag(T171, T172, T166))
U5_GGAG(T163, T171, T172, T166, lessc46_out_gg(T163, T171)) → DELETE1_IN_GAG(T171, T172, T166)
DELETE1_IN_GAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → U23_GAG(T209, T210, T201, T202, delete1_in_gag(0, T210, T202))
DELETE1_IN_GAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → DELETE1_IN_GAG(0, T210, T202)
DELETE1_IN_GAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → U24_GAG(T223, T222, T224, T201, T202, p65_in_ggag(T223, T222, T224, T202))
DELETE1_IN_GAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → P65_IN_GGAG(T223, T222, T224, T202)
P65_IN_GGAG(T223, T222, T224, T202) → U12_GGAG(T223, T222, T224, T202, less34_in_gg(T223, T222))
P65_IN_GGAG(T223, T222, T224, T202) → LESS34_IN_GG(T223, T222)
P65_IN_GGAG(T227, T222, T228, T202) → U13_GGAG(T227, T222, T228, T202, lessc34_in_gg(T227, T222))
U13_GGAG(T227, T222, T228, T202, lessc34_out_gg(T227, T222)) → U14_GGAG(T227, T222, T228, T202, delete1_in_gag(s(T227), T228, T202))
U13_GGAG(T227, T222, T228, T202, lessc34_out_gg(T227, T222)) → DELETE1_IN_GAG(s(T227), T228, T202)
DELETE1_IN_GAG(T250, tree(T246, T247, T251), tree(T246, T247, T249)) → U25_GAG(T250, T246, T247, T251, T249, p44_in_ggag(T246, T250, T251, T249))
DELETE1_IN_GAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → U26_GAG(T264, T260, T261, T265, T263, p72_in_ggag(T260, T264, T265, T263))
DELETE1_IN_GAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → P72_IN_GGAG(T260, T264, T265, T263)
P72_IN_GGAG(0, s(T272), T271, T263) → U10_GGAG(T272, T271, T263, delete1_in_gag(s(T272), T271, T263))
P72_IN_GGAG(0, s(T272), T271, T263) → DELETE1_IN_GAG(s(T272), T271, T263)
DELETE1_IN_GAG(T300, tree(T300, T301, tree(T340, T346, T342)), tree(T343, T301, tree(T340, T344, T345))) → U27_GAG(T300, T301, T340, T346, T342, T343, T344, T345, delmin19_in_agg(T346, T343, T344))
DELETE1_IN_GAG(T376, tree(T372, T377, T374), tree(T372, T375, T374)) → U28_GAG(T376, T372, T377, T374, T375, p32_in_ggag(T376, T372, T377, T375))
DELETE1_IN_GAG(T395, tree(T391, T392, T396), tree(T391, T392, T394)) → U29_GAG(T395, T391, T392, T396, T394, p72_in_ggag(T391, T395, T396, T394))
P72_IN_GGAG(s(T281), s(T283), T284, T263) → U11_GGAG(T281, T283, T284, T263, p79_in_ggag(T281, T283, T284, T263))
P72_IN_GGAG(s(T281), s(T283), T284, T263) → P79_IN_GGAG(T281, T283, T284, T263)
P79_IN_GGAG(T281, T283, T284, T263) → U15_GGAG(T281, T283, T284, T263, less46_in_gg(T281, T283))
P79_IN_GGAG(T281, T283, T284, T263) → LESS46_IN_GG(T281, T283)
P79_IN_GGAG(T281, T287, T288, T263) → U16_GGAG(T281, T287, T288, T263, lessc46_in_gg(T281, T287))
U16_GGAG(T281, T287, T288, T263, lessc46_out_gg(T281, T287)) → U17_GGAG(T281, T287, T288, T263, delete1_in_gag(s(T287), T288, T263))
U16_GGAG(T281, T287, T288, T263, lessc46_out_gg(T281, T287)) → DELETE1_IN_GAG(s(T287), T288, T263)
DELETE1_IN_GAG(0, tree(s(T415), T416, T407), tree(s(T415), T408, T407)) → U30_GAG(T415, T416, T407, T408, delete1_in_gag(0, T416, T408))
DELETE1_IN_GAG(s(T429), tree(s(T428), T430, T407), tree(s(T428), T408, T407)) → U31_GAG(T429, T428, T430, T407, T408, p65_in_ggag(T429, T428, T430, T408))
DELETE1_IN_GAG(T448, tree(T444, T445, T449), tree(T444, T445, T447)) → U32_GAG(T448, T444, T445, T449, T447, p72_in_ggag(T444, T448, T449, T447))
DELETE1_IN_GAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → U33_GAG(T462, T458, T459, T463, T461, p116_in_ggag(T458, T462, T463, T461))
DELETE1_IN_GAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → P116_IN_GGAG(T458, T462, T463, T461)
P116_IN_GGAG(0, s(T470), T469, T461) → U18_GGAG(T470, T469, T461, delete1_in_gag(s(T470), T469, T461))
P116_IN_GGAG(0, s(T470), T469, T461) → DELETE1_IN_GAG(s(T470), T469, T461)
DELETE1_IN_GAG(T494, tree(T494, T495, tree(T534, T540, T536)), tree(T537, T495, tree(T534, T538, T539))) → U34_GAG(T494, T495, T534, T540, T536, T537, T538, T539, delmin19_in_agg(T540, T537, T538))
DELETE1_IN_GAG(T570, tree(T566, T571, T568), tree(T566, T569, T568)) → U35_GAG(T570, T566, T571, T568, T569, p32_in_ggag(T570, T566, T571, T569))
DELETE1_IN_GAG(T589, tree(T585, T586, T590), tree(T585, T586, T588)) → U36_GAG(T589, T585, T586, T590, T588, p116_in_ggag(T585, T589, T590, T588))
P116_IN_GGAG(s(T479), s(T481), T482, T461) → U19_GGAG(T479, T481, T482, T461, p79_in_ggag(T479, T481, T482, T461))
P116_IN_GGAG(s(T479), s(T481), T482, T461) → P79_IN_GGAG(T479, T481, T482, T461)
DELETE1_IN_GAG(0, tree(s(T609), T610, T601), tree(s(T609), T602, T601)) → U37_GAG(T609, T610, T601, T602, delete1_in_gag(0, T610, T602))
DELETE1_IN_GAG(s(T623), tree(s(T622), T624, T601), tree(s(T622), T602, T601)) → U38_GAG(T623, T622, T624, T601, T602, p65_in_ggag(T623, T622, T624, T602))
DELETE1_IN_GAG(T642, tree(T638, T639, T643), tree(T638, T639, T641)) → U39_GAG(T642, T638, T639, T643, T641, p116_in_ggag(T638, T642, T643, T641))
DELETE1_IN_GAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → U40_GAG(T664, T653, T663, T655, delete1_in_gag(s(T664), T663, T655))
DELETE1_IN_GAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → DELETE1_IN_GAG(s(T664), T663, T655)
DELETE1_IN_GAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → U41_GAG(T675, T673, T653, T676, T655, p79_in_ggag(T673, T675, T676, T655))
DELETE1_IN_GAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → P79_IN_GGAG(T673, T675, T676, T655)
DELETE1_IN_GAG(T684, tree(T684, T685, tree(T724, T730, T726)), tree(T727, T685, tree(T724, T728, T729))) → U42_GAG(T684, T685, T724, T730, T726, T727, T728, T729, delmin19_in_agg(T730, T727, T728))
DELETE1_IN_GAG(T760, tree(T756, T761, T758), tree(T756, T759, T758)) → U43_GAG(T760, T756, T761, T758, T759, p32_in_ggag(T760, T756, T761, T759))
DELETE1_IN_GAG(T779, tree(T775, T776, T780), tree(T775, T776, T778)) → U44_GAG(T779, T775, T776, T780, T778, p116_in_ggag(T775, T779, T780, T778))
DELETE1_IN_GAG(0, tree(s(T799), T800, T791), tree(s(T799), T792, T791)) → U45_GAG(T799, T800, T791, T792, delete1_in_gag(0, T800, T792))
DELETE1_IN_GAG(s(T813), tree(s(T812), T814, T791), tree(s(T812), T792, T791)) → U46_GAG(T813, T812, T814, T791, T792, p65_in_ggag(T813, T812, T814, T792))
DELETE1_IN_GAG(T832, tree(T828, T829, T833), tree(T828, T829, T831)) → U47_GAG(T832, T828, T829, T833, T831, p116_in_ggag(T828, T832, T833, T831))
DELETE1_IN_GAG(s(T854), tree(0, T843, T853), tree(0, T843, T845)) → U48_GAG(T854, T843, T853, T845, delete1_in_gag(s(T854), T853, T845))
DELETE1_IN_GAG(s(T865), tree(s(T863), T843, T866), tree(s(T863), T843, T845)) → U49_GAG(T865, T863, T843, T866, T845, p79_in_ggag(T863, T865, T866, T845))
DELETE1_IN_AAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → U22_AAG(T167, T163, T164, T168, T166, p44_in_gaag(T163, T167, T168, T166))
DELETE1_IN_AAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → P44_IN_GAAG(T163, T167, T168, T166)
P44_IN_GAAG(T163, T167, T168, T166) → U4_GAAG(T163, T167, T168, T166, less46_in_ga(T163, T167))
P44_IN_GAAG(T163, T167, T168, T166) → LESS46_IN_GA(T163, T167)
LESS46_IN_GA(s(T184), s(T186)) → U3_GA(T184, T186, less46_in_ga(T184, T186))
LESS46_IN_GA(s(T184), s(T186)) → LESS46_IN_GA(T184, T186)
P44_IN_GAAG(T163, T171, T172, T166) → U5_GAAG(T163, T171, T172, T166, lessc46_in_ga(T163, T171))
U5_GAAG(T163, T171, T172, T166, lessc46_out_ga(T163, T171)) → U6_GAAG(T163, T171, T172, T166, delete1_in_aag(T171, T172, T166))
U5_GAAG(T163, T171, T172, T166, lessc46_out_ga(T163, T171)) → DELETE1_IN_AAG(T171, T172, T166)
DELETE1_IN_AAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → U23_AAG(T209, T210, T201, T202, delete1_in_gag(0, T210, T202))
DELETE1_IN_AAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → DELETE1_IN_GAG(0, T210, T202)
DELETE1_IN_AAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → U24_AAG(T223, T222, T224, T201, T202, p65_in_agag(T223, T222, T224, T202))
DELETE1_IN_AAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → P65_IN_AGAG(T223, T222, T224, T202)
P65_IN_AGAG(T223, T222, T224, T202) → U12_AGAG(T223, T222, T224, T202, less34_in_ag(T223, T222))
P65_IN_AGAG(T223, T222, T224, T202) → LESS34_IN_AG(T223, T222)
P65_IN_AGAG(T227, T222, T228, T202) → U13_AGAG(T227, T222, T228, T202, lessc34_in_ag(T227, T222))
U13_AGAG(T227, T222, T228, T202, lessc34_out_ag(T227, T222)) → U14_AGAG(T227, T222, T228, T202, delete1_in_gag(s(T227), T228, T202))
U13_AGAG(T227, T222, T228, T202, lessc34_out_ag(T227, T222)) → DELETE1_IN_GAG(s(T227), T228, T202)
DELETE1_IN_AAG(T250, tree(T246, T247, T251), tree(T246, T247, T249)) → U25_AAG(T250, T246, T247, T251, T249, p44_in_gaag(T246, T250, T251, T249))
DELETE1_IN_AAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → U26_AAG(T264, T260, T261, T265, T263, p72_in_gaag(T260, T264, T265, T263))
DELETE1_IN_AAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → P72_IN_GAAG(T260, T264, T265, T263)
P72_IN_GAAG(0, s(T272), T271, T263) → U10_GAAG(T272, T271, T263, delete1_in_aag(s(T272), T271, T263))
P72_IN_GAAG(0, s(T272), T271, T263) → DELETE1_IN_AAG(s(T272), T271, T263)
DELETE1_IN_AAG(T300, tree(T300, T301, tree(T340, T346, T342)), tree(T343, T301, tree(T340, T344, T345))) → U27_AAG(T300, T301, T340, T346, T342, T343, T344, T345, delmin19_in_agg(T346, T343, T344))
DELETE1_IN_AAG(T376, tree(T372, T377, T374), tree(T372, T375, T374)) → U28_AAG(T376, T372, T377, T374, T375, p32_in_agag(T376, T372, T377, T375))
DELETE1_IN_AAG(T395, tree(T391, T392, T396), tree(T391, T392, T394)) → U29_AAG(T395, T391, T392, T396, T394, p72_in_gaag(T391, T395, T396, T394))
P72_IN_GAAG(s(T281), s(T283), T284, T263) → U11_GAAG(T281, T283, T284, T263, p79_in_gaag(T281, T283, T284, T263))
P72_IN_GAAG(s(T281), s(T283), T284, T263) → P79_IN_GAAG(T281, T283, T284, T263)
P79_IN_GAAG(T281, T283, T284, T263) → U15_GAAG(T281, T283, T284, T263, less46_in_ga(T281, T283))
P79_IN_GAAG(T281, T283, T284, T263) → LESS46_IN_GA(T281, T283)
P79_IN_GAAG(T281, T287, T288, T263) → U16_GAAG(T281, T287, T288, T263, lessc46_in_ga(T281, T287))
U16_GAAG(T281, T287, T288, T263, lessc46_out_ga(T281, T287)) → U17_GAAG(T281, T287, T288, T263, delete1_in_aag(s(T287), T288, T263))
U16_GAAG(T281, T287, T288, T263, lessc46_out_ga(T281, T287)) → DELETE1_IN_AAG(s(T287), T288, T263)
DELETE1_IN_AAG(0, tree(s(T415), T416, T407), tree(s(T415), T408, T407)) → U30_AAG(T415, T416, T407, T408, delete1_in_gag(0, T416, T408))
DELETE1_IN_AAG(s(T429), tree(s(T428), T430, T407), tree(s(T428), T408, T407)) → U31_AAG(T429, T428, T430, T407, T408, p65_in_agag(T429, T428, T430, T408))
DELETE1_IN_AAG(T448, tree(T444, T445, T449), tree(T444, T445, T447)) → U32_AAG(T448, T444, T445, T449, T447, p72_in_gaag(T444, T448, T449, T447))
DELETE1_IN_AAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → U33_AAG(T462, T458, T459, T463, T461, p116_in_gaag(T458, T462, T463, T461))
DELETE1_IN_AAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → P116_IN_GAAG(T458, T462, T463, T461)
P116_IN_GAAG(0, s(T470), T469, T461) → U18_GAAG(T470, T469, T461, delete1_in_aag(s(T470), T469, T461))
P116_IN_GAAG(0, s(T470), T469, T461) → DELETE1_IN_AAG(s(T470), T469, T461)
DELETE1_IN_AAG(T494, tree(T494, T495, tree(T534, T540, T536)), tree(T537, T495, tree(T534, T538, T539))) → U34_AAG(T494, T495, T534, T540, T536, T537, T538, T539, delmin19_in_agg(T540, T537, T538))
DELETE1_IN_AAG(T570, tree(T566, T571, T568), tree(T566, T569, T568)) → U35_AAG(T570, T566, T571, T568, T569, p32_in_agag(T570, T566, T571, T569))
DELETE1_IN_AAG(T589, tree(T585, T586, T590), tree(T585, T586, T588)) → U36_AAG(T589, T585, T586, T590, T588, p116_in_gaag(T585, T589, T590, T588))
P116_IN_GAAG(s(T479), s(T481), T482, T461) → U19_GAAG(T479, T481, T482, T461, p79_in_gaag(T479, T481, T482, T461))
P116_IN_GAAG(s(T479), s(T481), T482, T461) → P79_IN_GAAG(T479, T481, T482, T461)
DELETE1_IN_AAG(0, tree(s(T609), T610, T601), tree(s(T609), T602, T601)) → U37_AAG(T609, T610, T601, T602, delete1_in_gag(0, T610, T602))
DELETE1_IN_AAG(s(T623), tree(s(T622), T624, T601), tree(s(T622), T602, T601)) → U38_AAG(T623, T622, T624, T601, T602, p65_in_agag(T623, T622, T624, T602))
DELETE1_IN_AAG(T642, tree(T638, T639, T643), tree(T638, T639, T641)) → U39_AAG(T642, T638, T639, T643, T641, p116_in_gaag(T638, T642, T643, T641))
DELETE1_IN_AAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → U40_AAG(T664, T653, T663, T655, delete1_in_aag(s(T664), T663, T655))
DELETE1_IN_AAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → DELETE1_IN_AAG(s(T664), T663, T655)
DELETE1_IN_AAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → U41_AAG(T675, T673, T653, T676, T655, p79_in_gaag(T673, T675, T676, T655))
DELETE1_IN_AAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → P79_IN_GAAG(T673, T675, T676, T655)
DELETE1_IN_AAG(T684, tree(T684, T685, tree(T724, T730, T726)), tree(T727, T685, tree(T724, T728, T729))) → U42_AAG(T684, T685, T724, T730, T726, T727, T728, T729, delmin19_in_agg(T730, T727, T728))
DELETE1_IN_AAG(T760, tree(T756, T761, T758), tree(T756, T759, T758)) → U43_AAG(T760, T756, T761, T758, T759, p32_in_agag(T760, T756, T761, T759))
DELETE1_IN_AAG(T779, tree(T775, T776, T780), tree(T775, T776, T778)) → U44_AAG(T779, T775, T776, T780, T778, p116_in_gaag(T775, T779, T780, T778))
DELETE1_IN_AAG(0, tree(s(T799), T800, T791), tree(s(T799), T792, T791)) → U45_AAG(T799, T800, T791, T792, delete1_in_gag(0, T800, T792))
DELETE1_IN_AAG(s(T813), tree(s(T812), T814, T791), tree(s(T812), T792, T791)) → U46_AAG(T813, T812, T814, T791, T792, p65_in_agag(T813, T812, T814, T792))
DELETE1_IN_AAG(T832, tree(T828, T829, T833), tree(T828, T829, T831)) → U47_AAG(T832, T828, T829, T833, T831, p116_in_gaag(T828, T832, T833, T831))
DELETE1_IN_AAG(s(T854), tree(0, T843, T853), tree(0, T843, T845)) → U48_AAG(T854, T843, T853, T845, delete1_in_aag(s(T854), T853, T845))
DELETE1_IN_AAG(s(T865), tree(s(T863), T843, T866), tree(s(T863), T843, T845)) → U49_AAG(T865, T863, T843, T866, T845, p79_in_gaag(T863, T865, T866, T845))

The TRS R consists of the following rules:

lessc34_in_ag(0, s(T138)) → lessc34_out_ag(0, s(T138))
lessc34_in_ag(s(T145), s(T144)) → U82_ag(T145, T144, lessc34_in_ag(T145, T144))
U82_ag(T145, T144, lessc34_out_ag(T145, T144)) → lessc34_out_ag(s(T145), s(T144))
lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))
lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
delete1_in_aag(x1, x2, x3) = delete1_in_aag(x3)
tree(x1, x2, x3) = tree(x1, x2, x3)
delmin19_in_agg(x1, x2, x3) = delmin19_in_agg(x2, x3)
p32_in_agag(x1, x2, x3, x4) = p32_in_agag(x2, x4)
less34_in_ag(x1, x2) = less34_in_ag(x2)
s(x1) = s(x1)
lessc34_in_ag(x1, x2) = lessc34_in_ag(x2)
lessc34_out_ag(x1, x2) = lessc34_out_ag(x1, x2)
U82_ag(x1, x2, x3) = U82_ag(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)
less34_in_gg(x1, x2) = less34_in_gg(x1, x2)
lessc34_in_gg(x1, x2) = lessc34_in_gg(x1, x2)
0 = 0
lessc34_out_gg(x1, x2) = lessc34_out_gg(x1, x2)
U82_gg(x1, x2, x3) = U82_gg(x1, x2, x3)
p44_in_ggag(x1, x2, x3, x4) = p44_in_ggag(x1, x2, x4)
less46_in_gg(x1, x2) = less46_in_gg(x1, x2)
lessc46_in_gg(x1, x2) = lessc46_in_gg(x1, x2)
lessc46_out_gg(x1, x2) = lessc46_out_gg(x1, x2)
U83_gg(x1, x2, x3) = U83_gg(x1, x2, x3)
p65_in_ggag(x1, x2, x3, x4) = p65_in_ggag(x1, x2, x4)
p72_in_ggag(x1, x2, x3, x4) = p72_in_ggag(x1, x2, x4)
p79_in_ggag(x1, x2, x3, x4) = p79_in_ggag(x1, x2, x4)
p116_in_ggag(x1, x2, x3, x4) = p116_in_ggag(x1, x2, x4)
p44_in_gaag(x1, x2, x3, x4) = p44_in_gaag(x1, x4)
less46_in_ga(x1, x2) = less46_in_ga(x1)
lessc46_in_ga(x1, x2) = lessc46_in_ga(x1)
lessc46_out_ga(x1, x2) = lessc46_out_ga(x1)
U83_ga(x1, x2, x3) = U83_ga(x1, x3)
p65_in_agag(x1, x2, x3, x4) = p65_in_agag(x2, x4)
p72_in_gaag(x1, x2, x3, x4) = p72_in_gaag(x1, x4)
p79_in_gaag(x1, x2, x3, x4) = p79_in_gaag(x1, x4)
p116_in_gaag(x1, x2, x3, x4) = p116_in_gaag(x1, x4)
DELETE1_IN_AAG(x1, x2, x3) = DELETE1_IN_AAG(x3)
U20_AAG(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U20_AAG(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)
U21_AAG(x1, x2, x3, x4, x5, x6) = U21_AAG(x2, x4, x5, x6)
P32_IN_AGAG(x1, x2, x3, x4) = P32_IN_AGAG(x2, x4)
U7_AGAG(x1, x2, x3, x4, x5) = U7_AGAG(x2, x4, x5)
LESS34_IN_AG(x1, x2) = LESS34_IN_AG(x2)
U2_AG(x1, x2, x3) = U2_AG(x2, x3)
U8_AGAG(x1, x2, x3, x4, x5) = U8_AGAG(x2, x4, x5)
U9_AGAG(x1, x2, x3, x4, x5) = U9_AGAG(x1, x2, x4, x5)
DELETE1_IN_GAG(x1, x2, x3) = DELETE1_IN_GAG(x1, x3)
U20_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U20_GAG(x1, x2, x3, x6, x7, x8, x9)
U21_GAG(x1, x2, x3, x4, x5, x6) = U21_GAG(x1, x2, x4, x5, x6)
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)
LESS34_IN_GG(x1, x2) = LESS34_IN_GG(x1, x2)
U2_GG(x1, x2, x3) = U2_GG(x1, x2, x3)
U8_GGAG(x1, x2, x3, x4, x5) = U8_GGAG(x1, x2, x4, x5)
U9_GGAG(x1, x2, x3, x4, x5) = U9_GGAG(x1, x2, x4, x5)
U22_GAG(x1, x2, x3, x4, x5, x6) = U22_GAG(x1, x2, x3, x5, x6)
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)
LESS46_IN_GG(x1, x2) = LESS46_IN_GG(x1, x2)
U3_GG(x1, x2, x3) = U3_GG(x1, x2, x3)
U5_GGAG(x1, x2, x3, x4, x5) = U5_GGAG(x1, x2, x4, x5)
U6_GGAG(x1, x2, x3, x4, x5) = U6_GGAG(x1, x2, x4, x5)
U23_GAG(x1, x2, x3, x4, x5) = U23_GAG(x1, x3, x4, x5)
U24_GAG(x1, x2, x3, x4, x5, x6) = U24_GAG(x1, x2, x4, x5, x6)
P65_IN_GGAG(x1, x2, x3, x4) = P65_IN_GGAG(x1, x2, x4)
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)
U14_GGAG(x1, x2, x3, x4, x5) = U14_GGAG(x1, x2, x4, x5)
U25_GAG(x1, x2, x3, x4, x5, x6) = U25_GAG(x1, x2, x3, x5, x6)
U26_GAG(x1, x2, x3, x4, x5, x6) = U26_GAG(x1, x2, x3, x5, x6)
P72_IN_GGAG(x1, x2, x3, x4) = P72_IN_GGAG(x1, x2, x4)
U10_GGAG(x1, x2, x3, x4) = U10_GGAG(x1, x3, x4)
U27_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U27_GAG(x1, x2, x3, x6, x7, x8, x9)
U28_GAG(x1, x2, x3, x4, x5, x6) = U28_GAG(x1, x2, x4, x5, x6)
U29_GAG(x1, x2, x3, x4, x5, x6) = U29_GAG(x1, x2, x3, x5, x6)
U11_GGAG(x1, x2, x3, x4, x5) = U11_GGAG(x1, x2, x4, x5)
P79_IN_GGAG(x1, x2, x3, x4) = P79_IN_GGAG(x1, x2, x4)
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)
U17_GGAG(x1, x2, x3, x4, x5) = U17_GGAG(x1, x2, x4, x5)
U30_GAG(x1, x2, x3, x4, x5) = U30_GAG(x1, x3, x4, x5)
U31_GAG(x1, x2, x3, x4, x5, x6) = U31_GAG(x1, x2, x4, x5, x6)
U32_GAG(x1, x2, x3, x4, x5, x6) = U32_GAG(x1, x2, x3, x5, x6)
U33_GAG(x1, x2, x3, x4, x5, x6) = U33_GAG(x1, x2, x3, x5, x6)
P116_IN_GGAG(x1, x2, x3, x4) = P116_IN_GGAG(x1, x2, x4)
U18_GGAG(x1, x2, x3, x4) = U18_GGAG(x1, x3, x4)
U34_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U34_GAG(x1, x2, x3, x6, x7, x8, x9)
U35_GAG(x1, x2, x3, x4, x5, x6) = U35_GAG(x1, x2, x4, x5, x6)
U36_GAG(x1, x2, x3, x4, x5, x6) = U36_GAG(x1, x2, x3, x5, x6)
U19_GGAG(x1, x2, x3, x4, x5) = U19_GGAG(x1, x2, x4, x5)
U37_GAG(x1, x2, x3, x4, x5) = U37_GAG(x1, x3, x4, x5)
U38_GAG(x1, x2, x3, x4, x5, x6) = U38_GAG(x1, x2, x4, x5, x6)
U39_GAG(x1, x2, x3, x4, x5, x6) = U39_GAG(x1, x2, x3, x5, x6)
U40_GAG(x1, x2, x3, x4, x5) = U40_GAG(x1, x2, x4, x5)
U41_GAG(x1, x2, x3, x4, x5, x6) = U41_GAG(x1, x2, x3, x5, x6)
U42_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U42_GAG(x1, x2, x3, x6, x7, x8, x9)
U43_GAG(x1, x2, x3, x4, x5, x6) = U43_GAG(x1, x2, x4, x5, x6)
U44_GAG(x1, x2, x3, x4, x5, x6) = U44_GAG(x1, x2, x3, x5, x6)
U45_GAG(x1, x2, x3, x4, x5) = U45_GAG(x1, x3, x4, x5)
U46_GAG(x1, x2, x3, x4, x5, x6) = U46_GAG(x1, x2, x4, x5, x6)
U47_GAG(x1, x2, x3, x4, x5, x6) = U47_GAG(x1, x2, x3, x5, x6)
U48_GAG(x1, x2, x3, x4, x5) = U48_GAG(x1, x2, x4, x5)
U49_GAG(x1, x2, x3, x4, x5, x6) = U49_GAG(x1, x2, x3, x5, x6)
U22_AAG(x1, x2, x3, x4, x5, x6) = U22_AAG(x2, x3, x5, x6)
P44_IN_GAAG(x1, x2, x3, x4) = P44_IN_GAAG(x1, x4)
U4_GAAG(x1, x2, x3, x4, x5) = U4_GAAG(x1, x4, x5)
LESS46_IN_GA(x1, x2) = LESS46_IN_GA(x1)
U3_GA(x1, x2, x3) = U3_GA(x1, x3)
U5_GAAG(x1, x2, x3, x4, x5) = U5_GAAG(x1, x4, x5)
U6_GAAG(x1, x2, x3, x4, x5) = U6_GAAG(x1, x4, x5)
U23_AAG(x1, x2, x3, x4, x5) = U23_AAG(x1, x3, x4, x5)
U24_AAG(x1, x2, x3, x4, x5, x6) = U24_AAG(x2, x4, x5, x6)
P65_IN_AGAG(x1, x2, x3, x4) = P65_IN_AGAG(x2, x4)
U12_AGAG(x1, x2, x3, x4, x5) = U12_AGAG(x2, x4, x5)
U13_AGAG(x1, x2, x3, x4, x5) = U13_AGAG(x2, x4, x5)
U14_AGAG(x1, x2, x3, x4, x5) = U14_AGAG(x1, x2, x4, x5)
U25_AAG(x1, x2, x3, x4, x5, x6) = U25_AAG(x2, x3, x5, x6)
U26_AAG(x1, x2, x3, x4, x5, x6) = U26_AAG(x2, x3, x5, x6)
P72_IN_GAAG(x1, x2, x3, x4) = P72_IN_GAAG(x1, x4)
U10_GAAG(x1, x2, x3, x4) = U10_GAAG(x3, x4)
U27_AAG(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U27_AAG(x2, x3, x6, x7, x8, x9)
U28_AAG(x1, x2, x3, x4, x5, x6) = U28_AAG(x2, x4, x5, x6)
U29_AAG(x1, x2, x3, x4, x5, x6) = U29_AAG(x2, x3, x5, x6)
U11_GAAG(x1, x2, x3, x4, x5) = U11_GAAG(x1, x4, x5)
P79_IN_GAAG(x1, x2, x3, x4) = P79_IN_GAAG(x1, x4)
U15_GAAG(x1, x2, x3, x4, x5) = U15_GAAG(x1, x4, x5)
U16_GAAG(x1, x2, x3, x4, x5) = U16_GAAG(x1, x4, x5)
U17_GAAG(x1, x2, x3, x4, x5) = U17_GAAG(x1, x4, x5)
U30_AAG(x1, x2, x3, x4, x5) = U30_AAG(x1, x3, x4, x5)
U31_AAG(x1, x2, x3, x4, x5, x6) = U31_AAG(x2, x4, x5, x6)
U32_AAG(x1, x2, x3, x4, x5, x6) = U32_AAG(x2, x3, x5, x6)
U33_AAG(x1, x2, x3, x4, x5, x6) = U33_AAG(x2, x3, x5, x6)
P116_IN_GAAG(x1, x2, x3, x4) = P116_IN_GAAG(x1, x4)
U18_GAAG(x1, x2, x3, x4) = U18_GAAG(x3, x4)
U34_AAG(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U34_AAG(x2, x3, x6, x7, x8, x9)
U35_AAG(x1, x2, x3, x4, x5, x6) = U35_AAG(x2, x4, x5, x6)
U36_AAG(x1, x2, x3, x4, x5, x6) = U36_AAG(x2, x3, x5, x6)
U19_GAAG(x1, x2, x3, x4, x5) = U19_GAAG(x1, x4, x5)
U37_AAG(x1, x2, x3, x4, x5) = U37_AAG(x1, x3, x4, x5)
U38_AAG(x1, x2, x3, x4, x5, x6) = U38_AAG(x2, x4, x5, x6)
U39_AAG(x1, x2, x3, x4, x5, x6) = U39_AAG(x2, x3, x5, x6)
U40_AAG(x1, x2, x3, x4, x5) = U40_AAG(x2, x4, x5)
U41_AAG(x1, x2, x3, x4, x5, x6) = U41_AAG(x2, x3, x5, x6)
U42_AAG(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U42_AAG(x2, x3, x6, x7, x8, x9)
U43_AAG(x1, x2, x3, x4, x5, x6) = U43_AAG(x2, x4, x5, x6)
U44_AAG(x1, x2, x3, x4, x5, x6) = U44_AAG(x2, x3, x5, x6)
U45_AAG(x1, x2, x3, x4, x5) = U45_AAG(x1, x3, x4, x5)
U46_AAG(x1, x2, x3, x4, x5, x6) = U46_AAG(x2, x4, x5, x6)
U47_AAG(x1, x2, x3, x4, x5, x6) = U47_AAG(x2, x3, x5, x6)
U48_AAG(x1, x2, x3, x4, x5) = U48_AAG(x2, x4, x5)
U49_AAG(x1, x2, x3, x4, x5, x6) = U49_AAG(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_AAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U20_AAG(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_in_agg(T63, T60, T61))
DELETE1_IN_AAG(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_AAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → U21_AAG(T126, T122, T127, T124, T125, p32_in_agag(T126, T122, T127, T125))
DELETE1_IN_AAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → P32_IN_AGAG(T126, T122, T127, T125)
P32_IN_AGAG(T126, T122, T127, T125) → U7_AGAG(T126, T122, T127, T125, less34_in_ag(T126, T122))
P32_IN_AGAG(T126, T122, T127, T125) → LESS34_IN_AG(T126, T122)
LESS34_IN_AG(s(T145), s(T144)) → U2_AG(T145, T144, less34_in_ag(T145, T144))
LESS34_IN_AG(s(T145), s(T144)) → LESS34_IN_AG(T145, T144)
P32_IN_AGAG(T130, T122, T131, T125) → U8_AGAG(T130, T122, T131, T125, lessc34_in_ag(T130, T122))
U8_AGAG(T130, T122, T131, T125, lessc34_out_ag(T130, T122)) → U9_AGAG(T130, T122, T131, T125, delete1_in_gag(T130, T131, T125))
U8_AGAG(T130, T122, T131, T125, lessc34_out_ag(T130, T122)) → DELETE1_IN_GAG(T130, T131, T125)
DELETE1_IN_GAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U20_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)
DELETE1_IN_GAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → U21_GAG(T126, T122, T127, T124, T125, p32_in_ggag(T126, T122, T127, T125))
DELETE1_IN_GAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → P32_IN_GGAG(T126, T122, T127, T125)
P32_IN_GGAG(T126, T122, T127, T125) → U7_GGAG(T126, T122, T127, T125, less34_in_gg(T126, T122))
P32_IN_GGAG(T126, T122, T127, T125) → LESS34_IN_GG(T126, T122)
LESS34_IN_GG(s(T145), s(T144)) → U2_GG(T145, T144, less34_in_gg(T145, T144))
LESS34_IN_GG(s(T145), s(T144)) → LESS34_IN_GG(T145, T144)
P32_IN_GGAG(T130, T122, T131, T125) → U8_GGAG(T130, T122, T131, T125, lessc34_in_gg(T130, T122))
U8_GGAG(T130, T122, T131, T125, lessc34_out_gg(T130, T122)) → U9_GGAG(T130, T122, T131, T125, delete1_in_gag(T130, T131, T125))
U8_GGAG(T130, T122, T131, T125, lessc34_out_gg(T130, T122)) → DELETE1_IN_GAG(T130, T131, T125)
DELETE1_IN_GAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → U22_GAG(T167, T163, T164, T168, T166, p44_in_ggag(T163, T167, T168, T166))
DELETE1_IN_GAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → P44_IN_GGAG(T163, T167, T168, T166)
P44_IN_GGAG(T163, T167, T168, T166) → U4_GGAG(T163, T167, T168, T166, less46_in_gg(T163, T167))
P44_IN_GGAG(T163, T167, T168, T166) → LESS46_IN_GG(T163, T167)
LESS46_IN_GG(s(T184), s(T186)) → U3_GG(T184, T186, less46_in_gg(T184, T186))
LESS46_IN_GG(s(T184), s(T186)) → LESS46_IN_GG(T184, T186)
P44_IN_GGAG(T163, T171, T172, T166) → U5_GGAG(T163, T171, T172, T166, lessc46_in_gg(T163, T171))
U5_GGAG(T163, T171, T172, T166, lessc46_out_gg(T163, T171)) → U6_GGAG(T163, T171, T172, T166, delete1_in_gag(T171, T172, T166))
U5_GGAG(T163, T171, T172, T166, lessc46_out_gg(T163, T171)) → DELETE1_IN_GAG(T171, T172, T166)
DELETE1_IN_GAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → U23_GAG(T209, T210, T201, T202, delete1_in_gag(0, T210, T202))
DELETE1_IN_GAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → DELETE1_IN_GAG(0, T210, T202)
DELETE1_IN_GAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → U24_GAG(T223, T222, T224, T201, T202, p65_in_ggag(T223, T222, T224, T202))
DELETE1_IN_GAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → P65_IN_GGAG(T223, T222, T224, T202)
P65_IN_GGAG(T223, T222, T224, T202) → U12_GGAG(T223, T222, T224, T202, less34_in_gg(T223, T222))
P65_IN_GGAG(T223, T222, T224, T202) → LESS34_IN_GG(T223, T222)
P65_IN_GGAG(T227, T222, T228, T202) → U13_GGAG(T227, T222, T228, T202, lessc34_in_gg(T227, T222))
U13_GGAG(T227, T222, T228, T202, lessc34_out_gg(T227, T222)) → U14_GGAG(T227, T222, T228, T202, delete1_in_gag(s(T227), T228, T202))
U13_GGAG(T227, T222, T228, T202, lessc34_out_gg(T227, T222)) → DELETE1_IN_GAG(s(T227), T228, T202)
DELETE1_IN_GAG(T250, tree(T246, T247, T251), tree(T246, T247, T249)) → U25_GAG(T250, T246, T247, T251, T249, p44_in_ggag(T246, T250, T251, T249))
DELETE1_IN_GAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → U26_GAG(T264, T260, T261, T265, T263, p72_in_ggag(T260, T264, T265, T263))
DELETE1_IN_GAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → P72_IN_GGAG(T260, T264, T265, T263)
P72_IN_GGAG(0, s(T272), T271, T263) → U10_GGAG(T272, T271, T263, delete1_in_gag(s(T272), T271, T263))
P72_IN_GGAG(0, s(T272), T271, T263) → DELETE1_IN_GAG(s(T272), T271, T263)
DELETE1_IN_GAG(T300, tree(T300, T301, tree(T340, T346, T342)), tree(T343, T301, tree(T340, T344, T345))) → U27_GAG(T300, T301, T340, T346, T342, T343, T344, T345, delmin19_in_agg(T346, T343, T344))
DELETE1_IN_GAG(T376, tree(T372, T377, T374), tree(T372, T375, T374)) → U28_GAG(T376, T372, T377, T374, T375, p32_in_ggag(T376, T372, T377, T375))
DELETE1_IN_GAG(T395, tree(T391, T392, T396), tree(T391, T392, T394)) → U29_GAG(T395, T391, T392, T396, T394, p72_in_ggag(T391, T395, T396, T394))
P72_IN_GGAG(s(T281), s(T283), T284, T263) → U11_GGAG(T281, T283, T284, T263, p79_in_ggag(T281, T283, T284, T263))
P72_IN_GGAG(s(T281), s(T283), T284, T263) → P79_IN_GGAG(T281, T283, T284, T263)
P79_IN_GGAG(T281, T283, T284, T263) → U15_GGAG(T281, T283, T284, T263, less46_in_gg(T281, T283))
P79_IN_GGAG(T281, T283, T284, T263) → LESS46_IN_GG(T281, T283)
P79_IN_GGAG(T281, T287, T288, T263) → U16_GGAG(T281, T287, T288, T263, lessc46_in_gg(T281, T287))
U16_GGAG(T281, T287, T288, T263, lessc46_out_gg(T281, T287)) → U17_GGAG(T281, T287, T288, T263, delete1_in_gag(s(T287), T288, T263))
U16_GGAG(T281, T287, T288, T263, lessc46_out_gg(T281, T287)) → DELETE1_IN_GAG(s(T287), T288, T263)
DELETE1_IN_GAG(0, tree(s(T415), T416, T407), tree(s(T415), T408, T407)) → U30_GAG(T415, T416, T407, T408, delete1_in_gag(0, T416, T408))
DELETE1_IN_GAG(s(T429), tree(s(T428), T430, T407), tree(s(T428), T408, T407)) → U31_GAG(T429, T428, T430, T407, T408, p65_in_ggag(T429, T428, T430, T408))
DELETE1_IN_GAG(T448, tree(T444, T445, T449), tree(T444, T445, T447)) → U32_GAG(T448, T444, T445, T449, T447, p72_in_ggag(T444, T448, T449, T447))
DELETE1_IN_GAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → U33_GAG(T462, T458, T459, T463, T461, p116_in_ggag(T458, T462, T463, T461))
DELETE1_IN_GAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → P116_IN_GGAG(T458, T462, T463, T461)
P116_IN_GGAG(0, s(T470), T469, T461) → U18_GGAG(T470, T469, T461, delete1_in_gag(s(T470), T469, T461))
P116_IN_GGAG(0, s(T470), T469, T461) → DELETE1_IN_GAG(s(T470), T469, T461)
DELETE1_IN_GAG(T494, tree(T494, T495, tree(T534, T540, T536)), tree(T537, T495, tree(T534, T538, T539))) → U34_GAG(T494, T495, T534, T540, T536, T537, T538, T539, delmin19_in_agg(T540, T537, T538))
DELETE1_IN_GAG(T570, tree(T566, T571, T568), tree(T566, T569, T568)) → U35_GAG(T570, T566, T571, T568, T569, p32_in_ggag(T570, T566, T571, T569))
DELETE1_IN_GAG(T589, tree(T585, T586, T590), tree(T585, T586, T588)) → U36_GAG(T589, T585, T586, T590, T588, p116_in_ggag(T585, T589, T590, T588))
P116_IN_GGAG(s(T479), s(T481), T482, T461) → U19_GGAG(T479, T481, T482, T461, p79_in_ggag(T479, T481, T482, T461))
P116_IN_GGAG(s(T479), s(T481), T482, T461) → P79_IN_GGAG(T479, T481, T482, T461)
DELETE1_IN_GAG(0, tree(s(T609), T610, T601), tree(s(T609), T602, T601)) → U37_GAG(T609, T610, T601, T602, delete1_in_gag(0, T610, T602))
DELETE1_IN_GAG(s(T623), tree(s(T622), T624, T601), tree(s(T622), T602, T601)) → U38_GAG(T623, T622, T624, T601, T602, p65_in_ggag(T623, T622, T624, T602))
DELETE1_IN_GAG(T642, tree(T638, T639, T643), tree(T638, T639, T641)) → U39_GAG(T642, T638, T639, T643, T641, p116_in_ggag(T638, T642, T643, T641))
DELETE1_IN_GAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → U40_GAG(T664, T653, T663, T655, delete1_in_gag(s(T664), T663, T655))
DELETE1_IN_GAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → DELETE1_IN_GAG(s(T664), T663, T655)
DELETE1_IN_GAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → U41_GAG(T675, T673, T653, T676, T655, p79_in_ggag(T673, T675, T676, T655))
DELETE1_IN_GAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → P79_IN_GGAG(T673, T675, T676, T655)
DELETE1_IN_GAG(T684, tree(T684, T685, tree(T724, T730, T726)), tree(T727, T685, tree(T724, T728, T729))) → U42_GAG(T684, T685, T724, T730, T726, T727, T728, T729, delmin19_in_agg(T730, T727, T728))
DELETE1_IN_GAG(T760, tree(T756, T761, T758), tree(T756, T759, T758)) → U43_GAG(T760, T756, T761, T758, T759, p32_in_ggag(T760, T756, T761, T759))
DELETE1_IN_GAG(T779, tree(T775, T776, T780), tree(T775, T776, T778)) → U44_GAG(T779, T775, T776, T780, T778, p116_in_ggag(T775, T779, T780, T778))
DELETE1_IN_GAG(0, tree(s(T799), T800, T791), tree(s(T799), T792, T791)) → U45_GAG(T799, T800, T791, T792, delete1_in_gag(0, T800, T792))
DELETE1_IN_GAG(s(T813), tree(s(T812), T814, T791), tree(s(T812), T792, T791)) → U46_GAG(T813, T812, T814, T791, T792, p65_in_ggag(T813, T812, T814, T792))
DELETE1_IN_GAG(T832, tree(T828, T829, T833), tree(T828, T829, T831)) → U47_GAG(T832, T828, T829, T833, T831, p116_in_ggag(T828, T832, T833, T831))
DELETE1_IN_GAG(s(T854), tree(0, T843, T853), tree(0, T843, T845)) → U48_GAG(T854, T843, T853, T845, delete1_in_gag(s(T854), T853, T845))
DELETE1_IN_GAG(s(T865), tree(s(T863), T843, T866), tree(s(T863), T843, T845)) → U49_GAG(T865, T863, T843, T866, T845, p79_in_ggag(T863, T865, T866, T845))
DELETE1_IN_AAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → U22_AAG(T167, T163, T164, T168, T166, p44_in_gaag(T163, T167, T168, T166))
DELETE1_IN_AAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → P44_IN_GAAG(T163, T167, T168, T166)
P44_IN_GAAG(T163, T167, T168, T166) → U4_GAAG(T163, T167, T168, T166, less46_in_ga(T163, T167))
P44_IN_GAAG(T163, T167, T168, T166) → LESS46_IN_GA(T163, T167)
LESS46_IN_GA(s(T184), s(T186)) → U3_GA(T184, T186, less46_in_ga(T184, T186))
LESS46_IN_GA(s(T184), s(T186)) → LESS46_IN_GA(T184, T186)
P44_IN_GAAG(T163, T171, T172, T166) → U5_GAAG(T163, T171, T172, T166, lessc46_in_ga(T163, T171))
U5_GAAG(T163, T171, T172, T166, lessc46_out_ga(T163, T171)) → U6_GAAG(T163, T171, T172, T166, delete1_in_aag(T171, T172, T166))
U5_GAAG(T163, T171, T172, T166, lessc46_out_ga(T163, T171)) → DELETE1_IN_AAG(T171, T172, T166)
DELETE1_IN_AAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → U23_AAG(T209, T210, T201, T202, delete1_in_gag(0, T210, T202))
DELETE1_IN_AAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → DELETE1_IN_GAG(0, T210, T202)
DELETE1_IN_AAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → U24_AAG(T223, T222, T224, T201, T202, p65_in_agag(T223, T222, T224, T202))
DELETE1_IN_AAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → P65_IN_AGAG(T223, T222, T224, T202)
P65_IN_AGAG(T223, T222, T224, T202) → U12_AGAG(T223, T222, T224, T202, less34_in_ag(T223, T222))
P65_IN_AGAG(T223, T222, T224, T202) → LESS34_IN_AG(T223, T222)
P65_IN_AGAG(T227, T222, T228, T202) → U13_AGAG(T227, T222, T228, T202, lessc34_in_ag(T227, T222))
U13_AGAG(T227, T222, T228, T202, lessc34_out_ag(T227, T222)) → U14_AGAG(T227, T222, T228, T202, delete1_in_gag(s(T227), T228, T202))
U13_AGAG(T227, T222, T228, T202, lessc34_out_ag(T227, T222)) → DELETE1_IN_GAG(s(T227), T228, T202)
DELETE1_IN_AAG(T250, tree(T246, T247, T251), tree(T246, T247, T249)) → U25_AAG(T250, T246, T247, T251, T249, p44_in_gaag(T246, T250, T251, T249))
DELETE1_IN_AAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → U26_AAG(T264, T260, T261, T265, T263, p72_in_gaag(T260, T264, T265, T263))
DELETE1_IN_AAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → P72_IN_GAAG(T260, T264, T265, T263)
P72_IN_GAAG(0, s(T272), T271, T263) → U10_GAAG(T272, T271, T263, delete1_in_aag(s(T272), T271, T263))
P72_IN_GAAG(0, s(T272), T271, T263) → DELETE1_IN_AAG(s(T272), T271, T263)
DELETE1_IN_AAG(T300, tree(T300, T301, tree(T340, T346, T342)), tree(T343, T301, tree(T340, T344, T345))) → U27_AAG(T300, T301, T340, T346, T342, T343, T344, T345, delmin19_in_agg(T346, T343, T344))
DELETE1_IN_AAG(T376, tree(T372, T377, T374), tree(T372, T375, T374)) → U28_AAG(T376, T372, T377, T374, T375, p32_in_agag(T376, T372, T377, T375))
DELETE1_IN_AAG(T395, tree(T391, T392, T396), tree(T391, T392, T394)) → U29_AAG(T395, T391, T392, T396, T394, p72_in_gaag(T391, T395, T396, T394))
P72_IN_GAAG(s(T281), s(T283), T284, T263) → U11_GAAG(T281, T283, T284, T263, p79_in_gaag(T281, T283, T284, T263))
P72_IN_GAAG(s(T281), s(T283), T284, T263) → P79_IN_GAAG(T281, T283, T284, T263)
P79_IN_GAAG(T281, T283, T284, T263) → U15_GAAG(T281, T283, T284, T263, less46_in_ga(T281, T283))
P79_IN_GAAG(T281, T283, T284, T263) → LESS46_IN_GA(T281, T283)
P79_IN_GAAG(T281, T287, T288, T263) → U16_GAAG(T281, T287, T288, T263, lessc46_in_ga(T281, T287))
U16_GAAG(T281, T287, T288, T263, lessc46_out_ga(T281, T287)) → U17_GAAG(T281, T287, T288, T263, delete1_in_aag(s(T287), T288, T263))
U16_GAAG(T281, T287, T288, T263, lessc46_out_ga(T281, T287)) → DELETE1_IN_AAG(s(T287), T288, T263)
DELETE1_IN_AAG(0, tree(s(T415), T416, T407), tree(s(T415), T408, T407)) → U30_AAG(T415, T416, T407, T408, delete1_in_gag(0, T416, T408))
DELETE1_IN_AAG(s(T429), tree(s(T428), T430, T407), tree(s(T428), T408, T407)) → U31_AAG(T429, T428, T430, T407, T408, p65_in_agag(T429, T428, T430, T408))
DELETE1_IN_AAG(T448, tree(T444, T445, T449), tree(T444, T445, T447)) → U32_AAG(T448, T444, T445, T449, T447, p72_in_gaag(T444, T448, T449, T447))
DELETE1_IN_AAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → U33_AAG(T462, T458, T459, T463, T461, p116_in_gaag(T458, T462, T463, T461))
DELETE1_IN_AAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → P116_IN_GAAG(T458, T462, T463, T461)
P116_IN_GAAG(0, s(T470), T469, T461) → U18_GAAG(T470, T469, T461, delete1_in_aag(s(T470), T469, T461))
P116_IN_GAAG(0, s(T470), T469, T461) → DELETE1_IN_AAG(s(T470), T469, T461)
DELETE1_IN_AAG(T494, tree(T494, T495, tree(T534, T540, T536)), tree(T537, T495, tree(T534, T538, T539))) → U34_AAG(T494, T495, T534, T540, T536, T537, T538, T539, delmin19_in_agg(T540, T537, T538))
DELETE1_IN_AAG(T570, tree(T566, T571, T568), tree(T566, T569, T568)) → U35_AAG(T570, T566, T571, T568, T569, p32_in_agag(T570, T566, T571, T569))
DELETE1_IN_AAG(T589, tree(T585, T586, T590), tree(T585, T586, T588)) → U36_AAG(T589, T585, T586, T590, T588, p116_in_gaag(T585, T589, T590, T588))
P116_IN_GAAG(s(T479), s(T481), T482, T461) → U19_GAAG(T479, T481, T482, T461, p79_in_gaag(T479, T481, T482, T461))
P116_IN_GAAG(s(T479), s(T481), T482, T461) → P79_IN_GAAG(T479, T481, T482, T461)
DELETE1_IN_AAG(0, tree(s(T609), T610, T601), tree(s(T609), T602, T601)) → U37_AAG(T609, T610, T601, T602, delete1_in_gag(0, T610, T602))
DELETE1_IN_AAG(s(T623), tree(s(T622), T624, T601), tree(s(T622), T602, T601)) → U38_AAG(T623, T622, T624, T601, T602, p65_in_agag(T623, T622, T624, T602))
DELETE1_IN_AAG(T642, tree(T638, T639, T643), tree(T638, T639, T641)) → U39_AAG(T642, T638, T639, T643, T641, p116_in_gaag(T638, T642, T643, T641))
DELETE1_IN_AAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → U40_AAG(T664, T653, T663, T655, delete1_in_aag(s(T664), T663, T655))
DELETE1_IN_AAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → DELETE1_IN_AAG(s(T664), T663, T655)
DELETE1_IN_AAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → U41_AAG(T675, T673, T653, T676, T655, p79_in_gaag(T673, T675, T676, T655))
DELETE1_IN_AAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → P79_IN_GAAG(T673, T675, T676, T655)
DELETE1_IN_AAG(T684, tree(T684, T685, tree(T724, T730, T726)), tree(T727, T685, tree(T724, T728, T729))) → U42_AAG(T684, T685, T724, T730, T726, T727, T728, T729, delmin19_in_agg(T730, T727, T728))
DELETE1_IN_AAG(T760, tree(T756, T761, T758), tree(T756, T759, T758)) → U43_AAG(T760, T756, T761, T758, T759, p32_in_agag(T760, T756, T761, T759))
DELETE1_IN_AAG(T779, tree(T775, T776, T780), tree(T775, T776, T778)) → U44_AAG(T779, T775, T776, T780, T778, p116_in_gaag(T775, T779, T780, T778))
DELETE1_IN_AAG(0, tree(s(T799), T800, T791), tree(s(T799), T792, T791)) → U45_AAG(T799, T800, T791, T792, delete1_in_gag(0, T800, T792))
DELETE1_IN_AAG(s(T813), tree(s(T812), T814, T791), tree(s(T812), T792, T791)) → U46_AAG(T813, T812, T814, T791, T792, p65_in_agag(T813, T812, T814, T792))
DELETE1_IN_AAG(T832, tree(T828, T829, T833), tree(T828, T829, T831)) → U47_AAG(T832, T828, T829, T833, T831, p116_in_gaag(T828, T832, T833, T831))
DELETE1_IN_AAG(s(T854), tree(0, T843, T853), tree(0, T843, T845)) → U48_AAG(T854, T843, T853, T845, delete1_in_aag(s(T854), T853, T845))
DELETE1_IN_AAG(s(T865), tree(s(T863), T843, T866), tree(s(T863), T843, T845)) → U49_AAG(T865, T863, T843, T866, T845, p79_in_gaag(T863, T865, T866, T845))

The TRS R consists of the following rules:

lessc34_in_ag(0, s(T138)) → lessc34_out_ag(0, s(T138))
lessc34_in_ag(s(T145), s(T144)) → U82_ag(T145, T144, lessc34_in_ag(T145, T144))
U82_ag(T145, T144, lessc34_out_ag(T145, T144)) → lessc34_out_ag(s(T145), s(T144))
lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))
lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 7 SCCs with 106 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

LESS46_IN_GA(s(T184), s(T186)) → LESS46_IN_GA(T184, T186)

The TRS R consists of the following rules:

lessc34_in_ag(0, s(T138)) → lessc34_out_ag(0, s(T138))
lessc34_in_ag(s(T145), s(T144)) → U82_ag(T145, T144, lessc34_in_ag(T145, T144))
U82_ag(T145, T144, lessc34_out_ag(T145, T144)) → lessc34_out_ag(s(T145), s(T144))
lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))
lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
lessc34_in_ag(x1, x2) = lessc34_in_ag(x2)
lessc34_out_ag(x1, x2) = lessc34_out_ag(x1, x2)
U82_ag(x1, x2, x3) = U82_ag(x2, x3)
lessc34_in_gg(x1, x2) = lessc34_in_gg(x1, x2)
0 = 0
lessc34_out_gg(x1, x2) = lessc34_out_gg(x1, x2)
U82_gg(x1, x2, x3) = U82_gg(x1, x2, x3)
lessc46_in_gg(x1, x2) = lessc46_in_gg(x1, x2)
lessc46_out_gg(x1, x2) = lessc46_out_gg(x1, x2)
U83_gg(x1, x2, x3) = U83_gg(x1, x2, x3)
lessc46_in_ga(x1, x2) = lessc46_in_ga(x1)
lessc46_out_ga(x1, x2) = lessc46_out_ga(x1)
U83_ga(x1, x2, x3) = U83_ga(x1, x3)
LESS46_IN_GA(x1, x2) = LESS46_IN_GA(x1)

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:

LESS46_IN_GA(s(T184), s(T186)) → LESS46_IN_GA(T184, T186)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
LESS46_IN_GA(x1, x2) = LESS46_IN_GA(x1)

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

(10) PiDPToQDPProof (SOUND 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:

LESS46_IN_GA(s(T184)) → LESS46_IN_GA(T184)

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:

LESS46_IN_GA(s(T184)) → LESS46_IN_GA(T184)
The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

LESS46_IN_GG(s(T184), s(T186)) → LESS46_IN_GG(T184, T186)

The TRS R consists of the following rules:

lessc34_in_ag(0, s(T138)) → lessc34_out_ag(0, s(T138))
lessc34_in_ag(s(T145), s(T144)) → U82_ag(T145, T144, lessc34_in_ag(T145, T144))
U82_ag(T145, T144, lessc34_out_ag(T145, T144)) → lessc34_out_ag(s(T145), s(T144))
lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))
lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
lessc34_in_ag(x1, x2) = lessc34_in_ag(x2)
lessc34_out_ag(x1, x2) = lessc34_out_ag(x1, x2)
U82_ag(x1, x2, x3) = U82_ag(x2, x3)
lessc34_in_gg(x1, x2) = lessc34_in_gg(x1, x2)
0 = 0
lessc34_out_gg(x1, x2) = lessc34_out_gg(x1, x2)
U82_gg(x1, x2, x3) = U82_gg(x1, x2, x3)
lessc46_in_gg(x1, x2) = lessc46_in_gg(x1, x2)
lessc46_out_gg(x1, x2) = lessc46_out_gg(x1, x2)
U83_gg(x1, x2, x3) = U83_gg(x1, x2, x3)
lessc46_in_ga(x1, x2) = lessc46_in_ga(x1)
lessc46_out_ga(x1, x2) = lessc46_out_ga(x1)
U83_ga(x1, x2, x3) = U83_ga(x1, x3)
LESS46_IN_GG(x1, x2) = LESS46_IN_GG(x1, x2)

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

(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:

LESS46_IN_GG(s(T184), s(T186)) → LESS46_IN_GG(T184, T186)

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

(17) PiDPToQDPProof (EQUIVALENT 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:

LESS46_IN_GG(s(T184), s(T186)) → LESS46_IN_GG(T184, T186)

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:

LESS46_IN_GG(s(T184), s(T186)) → LESS46_IN_GG(T184, T186)
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:

LESS34_IN_GG(s(T145), s(T144)) → LESS34_IN_GG(T145, T144)

The TRS R consists of the following rules:

lessc34_in_ag(0, s(T138)) → lessc34_out_ag(0, s(T138))
lessc34_in_ag(s(T145), s(T144)) → U82_ag(T145, T144, lessc34_in_ag(T145, T144))
U82_ag(T145, T144, lessc34_out_ag(T145, T144)) → lessc34_out_ag(s(T145), s(T144))
lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))
lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
lessc34_in_ag(x1, x2) = lessc34_in_ag(x2)
lessc34_out_ag(x1, x2) = lessc34_out_ag(x1, x2)
U82_ag(x1, x2, x3) = U82_ag(x2, x3)
lessc34_in_gg(x1, x2) = lessc34_in_gg(x1, x2)
0 = 0
lessc34_out_gg(x1, x2) = lessc34_out_gg(x1, x2)
U82_gg(x1, x2, x3) = U82_gg(x1, x2, x3)
lessc46_in_gg(x1, x2) = lessc46_in_gg(x1, x2)
lessc46_out_gg(x1, x2) = lessc46_out_gg(x1, x2)
U83_gg(x1, x2, x3) = U83_gg(x1, x2, x3)
lessc46_in_ga(x1, x2) = lessc46_in_ga(x1)
lessc46_out_ga(x1, x2) = lessc46_out_ga(x1)
U83_ga(x1, x2, x3) = U83_ga(x1, x3)
LESS34_IN_GG(x1, x2) = LESS34_IN_GG(x1, x2)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

LESS34_IN_GG(s(T145), s(T144)) → LESS34_IN_GG(T145, T144)

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

(24) PiDPToQDPProof (EQUIVALENT transformation)

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

(25) Obligation:

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

LESS34_IN_GG(s(T145), s(T144)) → LESS34_IN_GG(T145, T144)

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

(26) 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(T145), s(T144)) → LESS34_IN_GG(T145, T144)
The graph contains the following edges 1 > 1, 2 > 2

(27) YES

(28) Obligation:

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

LESS34_IN_AG(s(T145), s(T144)) → LESS34_IN_AG(T145, T144)

The TRS R consists of the following rules:

lessc34_in_ag(0, s(T138)) → lessc34_out_ag(0, s(T138))
lessc34_in_ag(s(T145), s(T144)) → U82_ag(T145, T144, lessc34_in_ag(T145, T144))
U82_ag(T145, T144, lessc34_out_ag(T145, T144)) → lessc34_out_ag(s(T145), s(T144))
lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))
lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
lessc34_in_ag(x1, x2) = lessc34_in_ag(x2)
lessc34_out_ag(x1, x2) = lessc34_out_ag(x1, x2)
U82_ag(x1, x2, x3) = U82_ag(x2, x3)
lessc34_in_gg(x1, x2) = lessc34_in_gg(x1, x2)
0 = 0
lessc34_out_gg(x1, x2) = lessc34_out_gg(x1, x2)
U82_gg(x1, x2, x3) = U82_gg(x1, x2, x3)
lessc46_in_gg(x1, x2) = lessc46_in_gg(x1, x2)
lessc46_out_gg(x1, x2) = lessc46_out_gg(x1, x2)
U83_gg(x1, x2, x3) = U83_gg(x1, x2, x3)
lessc46_in_ga(x1, x2) = lessc46_in_ga(x1)
lessc46_out_ga(x1, x2) = lessc46_out_ga(x1)
U83_ga(x1, x2, x3) = U83_ga(x1, x3)
LESS34_IN_AG(x1, x2) = LESS34_IN_AG(x2)

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

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

LESS34_IN_AG(s(T145), s(T144)) → LESS34_IN_AG(T145, T144)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
LESS34_IN_AG(x1, x2) = LESS34_IN_AG(x2)

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

LESS34_IN_AG(s(T144)) → LESS34_IN_AG(T144)

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

(33) 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_AG(s(T144)) → LESS34_IN_AG(T144)
The graph contains the following edges 1 > 1

(34) YES

(35) 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_ag(0, s(T138)) → lessc34_out_ag(0, s(T138))
lessc34_in_ag(s(T145), s(T144)) → U82_ag(T145, T144, lessc34_in_ag(T145, T144))
U82_ag(T145, T144, lessc34_out_ag(T145, T144)) → lessc34_out_ag(s(T145), s(T144))
lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))
lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

(36) UsableRulesProof (EQUIVALENT transformation)

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

(37) 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

(38) PiDPToQDPProof (SOUND transformation)

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

(39) 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.

(40) 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

(41) YES

(42) Obligation:

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

DELETE1_IN_GAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → P32_IN_GGAG(T126, T122, T127, T125)
P32_IN_GGAG(T130, T122, T131, T125) → U8_GGAG(T130, T122, T131, T125, lessc34_in_gg(T130, T122))
U8_GGAG(T130, T122, T131, T125, lessc34_out_gg(T130, T122)) → DELETE1_IN_GAG(T130, T131, T125)
DELETE1_IN_GAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → P44_IN_GGAG(T163, T167, T168, T166)
P44_IN_GGAG(T163, T171, T172, T166) → U5_GGAG(T163, T171, T172, T166, lessc46_in_gg(T163, T171))
U5_GGAG(T163, T171, T172, T166, lessc46_out_gg(T163, T171)) → DELETE1_IN_GAG(T171, T172, T166)
DELETE1_IN_GAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → DELETE1_IN_GAG(0, T210, T202)
DELETE1_IN_GAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → P72_IN_GGAG(T260, T264, T265, T263)
P72_IN_GGAG(0, s(T272), T271, T263) → DELETE1_IN_GAG(s(T272), T271, T263)
DELETE1_IN_GAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → P65_IN_GGAG(T223, T222, T224, T202)
P65_IN_GGAG(T227, T222, T228, T202) → U13_GGAG(T227, T222, T228, T202, lessc34_in_gg(T227, T222))
U13_GGAG(T227, T222, T228, T202, lessc34_out_gg(T227, T222)) → DELETE1_IN_GAG(s(T227), T228, T202)
DELETE1_IN_GAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → P116_IN_GGAG(T458, T462, T463, T461)
P116_IN_GGAG(0, s(T470), T469, T461) → DELETE1_IN_GAG(s(T470), T469, T461)
DELETE1_IN_GAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → DELETE1_IN_GAG(s(T664), T663, T655)
DELETE1_IN_GAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → P79_IN_GGAG(T673, T675, T676, T655)
P79_IN_GGAG(T281, T287, T288, T263) → U16_GGAG(T281, T287, T288, T263, lessc46_in_gg(T281, T287))
U16_GGAG(T281, T287, T288, T263, lessc46_out_gg(T281, T287)) → DELETE1_IN_GAG(s(T287), T288, T263)
P116_IN_GGAG(s(T479), s(T481), T482, T461) → P79_IN_GGAG(T479, T481, T482, T461)
P72_IN_GGAG(s(T281), s(T283), T284, T263) → P79_IN_GGAG(T281, T283, T284, T263)

The TRS R consists of the following rules:

lessc34_in_ag(0, s(T138)) → lessc34_out_ag(0, s(T138))
lessc34_in_ag(s(T145), s(T144)) → U82_ag(T145, T144, lessc34_in_ag(T145, T144))
U82_ag(T145, T144, lessc34_out_ag(T145, T144)) → lessc34_out_ag(s(T145), s(T144))
lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))
lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3) = tree(x1, x2, x3)
s(x1) = s(x1)
lessc34_in_ag(x1, x2) = lessc34_in_ag(x2)
lessc34_out_ag(x1, x2) = lessc34_out_ag(x1, x2)
U82_ag(x1, x2, x3) = U82_ag(x2, x3)
lessc34_in_gg(x1, x2) = lessc34_in_gg(x1, x2)
0 = 0
lessc34_out_gg(x1, x2) = lessc34_out_gg(x1, x2)
U82_gg(x1, x2, x3) = U82_gg(x1, x2, x3)
lessc46_in_gg(x1, x2) = lessc46_in_gg(x1, x2)
lessc46_out_gg(x1, x2) = lessc46_out_gg(x1, x2)
U83_gg(x1, x2, x3) = U83_gg(x1, x2, x3)
lessc46_in_ga(x1, x2) = lessc46_in_ga(x1)
lessc46_out_ga(x1, x2) = lessc46_out_ga(x1)
U83_ga(x1, x2, x3) = U83_ga(x1, 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)
U8_GGAG(x1, x2, x3, x4, x5) = U8_GGAG(x1, x2, x4, x5)
P44_IN_GGAG(x1, x2, x3, x4) = P44_IN_GGAG(x1, x2, x4)
U5_GGAG(x1, x2, x3, x4, x5) = U5_GGAG(x1, x2, x4, x5)
P65_IN_GGAG(x1, x2, x3, x4) = P65_IN_GGAG(x1, x2, x4)
U13_GGAG(x1, x2, x3, x4, x5) = U13_GGAG(x1, x2, x4, x5)
P72_IN_GGAG(x1, x2, x3, x4) = P72_IN_GGAG(x1, x2, x4)
P79_IN_GGAG(x1, x2, x3, x4) = P79_IN_GGAG(x1, x2, x4)
U16_GGAG(x1, x2, x3, x4, x5) = U16_GGAG(x1, x2, x4, x5)
P116_IN_GGAG(x1, x2, x3, x4) = P116_IN_GGAG(x1, x2, x4)

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

(43) UsableRulesProof (EQUIVALENT transformation)

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

(44) Obligation:

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

DELETE1_IN_GAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → P32_IN_GGAG(T126, T122, T127, T125)
P32_IN_GGAG(T130, T122, T131, T125) → U8_GGAG(T130, T122, T131, T125, lessc34_in_gg(T130, T122))
U8_GGAG(T130, T122, T131, T125, lessc34_out_gg(T130, T122)) → DELETE1_IN_GAG(T130, T131, T125)
DELETE1_IN_GAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → P44_IN_GGAG(T163, T167, T168, T166)
P44_IN_GGAG(T163, T171, T172, T166) → U5_GGAG(T163, T171, T172, T166, lessc46_in_gg(T163, T171))
U5_GGAG(T163, T171, T172, T166, lessc46_out_gg(T163, T171)) → DELETE1_IN_GAG(T171, T172, T166)
DELETE1_IN_GAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → DELETE1_IN_GAG(0, T210, T202)
DELETE1_IN_GAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → P72_IN_GGAG(T260, T264, T265, T263)
P72_IN_GGAG(0, s(T272), T271, T263) → DELETE1_IN_GAG(s(T272), T271, T263)
DELETE1_IN_GAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → P65_IN_GGAG(T223, T222, T224, T202)
P65_IN_GGAG(T227, T222, T228, T202) → U13_GGAG(T227, T222, T228, T202, lessc34_in_gg(T227, T222))
U13_GGAG(T227, T222, T228, T202, lessc34_out_gg(T227, T222)) → DELETE1_IN_GAG(s(T227), T228, T202)
DELETE1_IN_GAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → P116_IN_GGAG(T458, T462, T463, T461)
P116_IN_GGAG(0, s(T470), T469, T461) → DELETE1_IN_GAG(s(T470), T469, T461)
DELETE1_IN_GAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → DELETE1_IN_GAG(s(T664), T663, T655)
DELETE1_IN_GAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → P79_IN_GGAG(T673, T675, T676, T655)
P79_IN_GGAG(T281, T287, T288, T263) → U16_GGAG(T281, T287, T288, T263, lessc46_in_gg(T281, T287))
U16_GGAG(T281, T287, T288, T263, lessc46_out_gg(T281, T287)) → DELETE1_IN_GAG(s(T287), T288, T263)
P116_IN_GGAG(s(T479), s(T481), T482, T461) → P79_IN_GGAG(T479, T481, T482, T461)
P72_IN_GGAG(s(T281), s(T283), T284, T263) → P79_IN_GGAG(T281, T283, T284, T263)

The TRS R consists of the following rules:

lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))

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)
U82_gg(x1, x2, x3) = U82_gg(x1, x2, x3)
lessc46_in_gg(x1, x2) = lessc46_in_gg(x1, x2)
lessc46_out_gg(x1, x2) = lessc46_out_gg(x1, x2)
U83_gg(x1, x2, x3) = U83_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)
U8_GGAG(x1, x2, x3, x4, x5) = U8_GGAG(x1, x2, x4, x5)
P44_IN_GGAG(x1, x2, x3, x4) = P44_IN_GGAG(x1, x2, x4)
U5_GGAG(x1, x2, x3, x4, x5) = U5_GGAG(x1, x2, x4, x5)
P65_IN_GGAG(x1, x2, x3, x4) = P65_IN_GGAG(x1, x2, x4)
U13_GGAG(x1, x2, x3, x4, x5) = U13_GGAG(x1, x2, x4, x5)
P72_IN_GGAG(x1, x2, x3, x4) = P72_IN_GGAG(x1, x2, x4)
P79_IN_GGAG(x1, x2, x3, x4) = P79_IN_GGAG(x1, x2, x4)
U16_GGAG(x1, x2, x3, x4, x5) = U16_GGAG(x1, x2, x4, x5)
P116_IN_GGAG(x1, x2, x3, x4) = P116_IN_GGAG(x1, x2, x4)

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

(45) PiDPToQDPProof (SOUND transformation)

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

(46) Obligation:

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

DELETE1_IN_GAG(T126, tree(T122, T125, T124)) → P32_IN_GGAG(T126, T122, T125)
P32_IN_GGAG(T130, T122, T125) → U8_GGAG(T130, T122, T125, lessc34_in_gg(T130, T122))
U8_GGAG(T130, T122, T125, lessc34_out_gg(T130, T122)) → DELETE1_IN_GAG(T130, T125)
DELETE1_IN_GAG(T167, tree(T163, T164, T166)) → P44_IN_GGAG(T163, T167, T166)
P44_IN_GGAG(T163, T171, T166) → U5_GGAG(T163, T171, T166, lessc46_in_gg(T163, T171))
U5_GGAG(T163, T171, T166, lessc46_out_gg(T163, T171)) → DELETE1_IN_GAG(T171, T166)
DELETE1_IN_GAG(0, tree(s(T209), T202, T201)) → DELETE1_IN_GAG(0, T202)
DELETE1_IN_GAG(T264, tree(T260, T261, T263)) → P72_IN_GGAG(T260, T264, T263)
P72_IN_GGAG(0, s(T272), T263) → DELETE1_IN_GAG(s(T272), T263)
DELETE1_IN_GAG(s(T223), tree(s(T222), T202, T201)) → P65_IN_GGAG(T223, T222, T202)
P65_IN_GGAG(T227, T222, T202) → U13_GGAG(T227, T222, T202, lessc34_in_gg(T227, T222))
U13_GGAG(T227, T222, T202, lessc34_out_gg(T227, T222)) → DELETE1_IN_GAG(s(T227), T202)
DELETE1_IN_GAG(T462, tree(T458, T459, T461)) → P116_IN_GGAG(T458, T462, T461)
P116_IN_GGAG(0, s(T470), T461) → DELETE1_IN_GAG(s(T470), T461)
DELETE1_IN_GAG(s(T664), tree(0, T653, T655)) → DELETE1_IN_GAG(s(T664), T655)
DELETE1_IN_GAG(s(T675), tree(s(T673), T653, T655)) → P79_IN_GGAG(T673, T675, T655)
P79_IN_GGAG(T281, T287, T263) → U16_GGAG(T281, T287, T263, lessc46_in_gg(T281, T287))
U16_GGAG(T281, T287, T263, lessc46_out_gg(T281, T287)) → DELETE1_IN_GAG(s(T287), T263)
P116_IN_GGAG(s(T479), s(T481), T461) → P79_IN_GGAG(T479, T481, T461)
P72_IN_GGAG(s(T281), s(T283), T263) → P79_IN_GGAG(T281, T283, T263)

The TRS R consists of the following rules:

lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))

The set Q consists of the following terms:

lessc34_in_gg(x0, x1)
lessc46_in_gg(x0, x1)
U82_gg(x0, x1, x2)
U83_gg(x0, x1, x2)

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

(47) 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(T130, T122, T125) → U8_GGAG(T130, T122, T125, lessc34_in_gg(T130, T122))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
U8_GGAG(T130, T122, T125, lessc34_out_gg(T130, T122)) → DELETE1_IN_GAG(T130, T125)
The graph contains the following edges 1 >= 1, 4 > 1, 3 >= 2
DELETE1_IN_GAG(T126, tree(T122, T125, T124)) → P32_IN_GGAG(T126, T122, T125)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
P44_IN_GGAG(T163, T171, T166) → U5_GGAG(T163, T171, T166, lessc46_in_gg(T163, T171))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
U5_GGAG(T163, T171, T166, lessc46_out_gg(T163, T171)) → DELETE1_IN_GAG(T171, T166)
The graph contains the following edges 2 >= 1, 4 > 1, 3 >= 2
DELETE1_IN_GAG(T167, tree(T163, T164, T166)) → P44_IN_GGAG(T163, T167, T166)
The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3
DELETE1_IN_GAG(0, tree(s(T209), T202, T201)) → DELETE1_IN_GAG(0, T202)
The graph contains the following edges 1 >= 1, 2 > 2
DELETE1_IN_GAG(s(T664), tree(0, T653, T655)) → DELETE1_IN_GAG(s(T664), T655)
The graph contains the following edges 1 >= 1, 2 > 2
P72_IN_GGAG(0, s(T272), T263) → DELETE1_IN_GAG(s(T272), T263)
The graph contains the following edges 2 >= 1, 3 >= 2
P72_IN_GGAG(s(T281), s(T283), T263) → P79_IN_GGAG(T281, T283, T263)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
DELETE1_IN_GAG(T264, tree(T260, T261, T263)) → P72_IN_GGAG(T260, T264, T263)
The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3
DELETE1_IN_GAG(T462, tree(T458, T459, T461)) → P116_IN_GGAG(T458, T462, T461)
The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3
P65_IN_GGAG(T227, T222, T202) → U13_GGAG(T227, T222, T202, lessc34_in_gg(T227, T222))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
U13_GGAG(T227, T222, T202, lessc34_out_gg(T227, T222)) → DELETE1_IN_GAG(s(T227), T202)
The graph contains the following edges 3 >= 2
DELETE1_IN_GAG(s(T223), tree(s(T222), T202, T201)) → P65_IN_GGAG(T223, T222, T202)
The graph contains the following edges 1 > 1, 2 > 2, 2 > 3
DELETE1_IN_GAG(s(T675), tree(s(T673), T653, T655)) → P79_IN_GGAG(T673, T675, T655)
The graph contains the following edges 2 > 1, 1 > 2, 2 > 3
P116_IN_GGAG(0, s(T470), T461) → DELETE1_IN_GAG(s(T470), T461)
The graph contains the following edges 2 >= 1, 3 >= 2
U16_GGAG(T281, T287, T263, lessc46_out_gg(T281, T287)) → DELETE1_IN_GAG(s(T287), T263)
The graph contains the following edges 3 >= 2
P116_IN_GGAG(s(T479), s(T481), T461) → P79_IN_GGAG(T479, T481, T461)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
P79_IN_GGAG(T281, T287, T263) → U16_GGAG(T281, T287, T263, lessc46_in_gg(T281, T287))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

(48) YES

(49) Obligation:

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

DELETE1_IN_AAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → P44_IN_GAAG(T163, T167, T168, T166)
P44_IN_GAAG(T163, T171, T172, T166) → U5_GAAG(T163, T171, T172, T166, lessc46_in_ga(T163, T171))
U5_GAAG(T163, T171, T172, T166, lessc46_out_ga(T163, T171)) → DELETE1_IN_AAG(T171, T172, T166)
DELETE1_IN_AAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → P72_IN_GAAG(T260, T264, T265, T263)
P72_IN_GAAG(0, s(T272), T271, T263) → DELETE1_IN_AAG(s(T272), T271, T263)
DELETE1_IN_AAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → P116_IN_GAAG(T458, T462, T463, T461)
P116_IN_GAAG(0, s(T470), T469, T461) → DELETE1_IN_AAG(s(T470), T469, T461)
DELETE1_IN_AAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → DELETE1_IN_AAG(s(T664), T663, T655)
DELETE1_IN_AAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → P79_IN_GAAG(T673, T675, T676, T655)
P79_IN_GAAG(T281, T287, T288, T263) → U16_GAAG(T281, T287, T288, T263, lessc46_in_ga(T281, T287))
U16_GAAG(T281, T287, T288, T263, lessc46_out_ga(T281, T287)) → DELETE1_IN_AAG(s(T287), T288, T263)
P116_IN_GAAG(s(T479), s(T481), T482, T461) → P79_IN_GAAG(T479, T481, T482, T461)
P72_IN_GAAG(s(T281), s(T283), T284, T263) → P79_IN_GAAG(T281, T283, T284, T263)

The TRS R consists of the following rules:

lessc34_in_ag(0, s(T138)) → lessc34_out_ag(0, s(T138))
lessc34_in_ag(s(T145), s(T144)) → U82_ag(T145, T144, lessc34_in_ag(T145, T144))
U82_ag(T145, T144, lessc34_out_ag(T145, T144)) → lessc34_out_ag(s(T145), s(T144))
lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))
lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3) = tree(x1, x2, x3)
s(x1) = s(x1)
lessc34_in_ag(x1, x2) = lessc34_in_ag(x2)
lessc34_out_ag(x1, x2) = lessc34_out_ag(x1, x2)
U82_ag(x1, x2, x3) = U82_ag(x2, x3)
lessc34_in_gg(x1, x2) = lessc34_in_gg(x1, x2)
0 = 0
lessc34_out_gg(x1, x2) = lessc34_out_gg(x1, x2)
U82_gg(x1, x2, x3) = U82_gg(x1, x2, x3)
lessc46_in_gg(x1, x2) = lessc46_in_gg(x1, x2)
lessc46_out_gg(x1, x2) = lessc46_out_gg(x1, x2)
U83_gg(x1, x2, x3) = U83_gg(x1, x2, x3)
lessc46_in_ga(x1, x2) = lessc46_in_ga(x1)
lessc46_out_ga(x1, x2) = lessc46_out_ga(x1)
U83_ga(x1, x2, x3) = U83_ga(x1, x3)
DELETE1_IN_AAG(x1, x2, x3) = DELETE1_IN_AAG(x3)
P44_IN_GAAG(x1, x2, x3, x4) = P44_IN_GAAG(x1, x4)
U5_GAAG(x1, x2, x3, x4, x5) = U5_GAAG(x1, x4, x5)
P72_IN_GAAG(x1, x2, x3, x4) = P72_IN_GAAG(x1, x4)
P79_IN_GAAG(x1, x2, x3, x4) = P79_IN_GAAG(x1, x4)
U16_GAAG(x1, x2, x3, x4, x5) = U16_GAAG(x1, x4, x5)
P116_IN_GAAG(x1, x2, x3, x4) = P116_IN_GAAG(x1, x4)

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

(50) UsableRulesProof (EQUIVALENT transformation)

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

(51) Obligation:

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

DELETE1_IN_AAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → P44_IN_GAAG(T163, T167, T168, T166)
P44_IN_GAAG(T163, T171, T172, T166) → U5_GAAG(T163, T171, T172, T166, lessc46_in_ga(T163, T171))
U5_GAAG(T163, T171, T172, T166, lessc46_out_ga(T163, T171)) → DELETE1_IN_AAG(T171, T172, T166)
DELETE1_IN_AAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → P72_IN_GAAG(T260, T264, T265, T263)
P72_IN_GAAG(0, s(T272), T271, T263) → DELETE1_IN_AAG(s(T272), T271, T263)
DELETE1_IN_AAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → P116_IN_GAAG(T458, T462, T463, T461)
P116_IN_GAAG(0, s(T470), T469, T461) → DELETE1_IN_AAG(s(T470), T469, T461)
DELETE1_IN_AAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → DELETE1_IN_AAG(s(T664), T663, T655)
DELETE1_IN_AAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → P79_IN_GAAG(T673, T675, T676, T655)
P79_IN_GAAG(T281, T287, T288, T263) → U16_GAAG(T281, T287, T288, T263, lessc46_in_ga(T281, T287))
U16_GAAG(T281, T287, T288, T263, lessc46_out_ga(T281, T287)) → DELETE1_IN_AAG(s(T287), T288, T263)
P116_IN_GAAG(s(T479), s(T481), T482, T461) → P79_IN_GAAG(T479, T481, T482, T461)
P72_IN_GAAG(s(T281), s(T283), T284, T263) → P79_IN_GAAG(T281, T283, T284, T263)

The TRS R consists of the following rules:

lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3) = tree(x1, x2, x3)
s(x1) = s(x1)
0 = 0
lessc46_in_ga(x1, x2) = lessc46_in_ga(x1)
lessc46_out_ga(x1, x2) = lessc46_out_ga(x1)
U83_ga(x1, x2, x3) = U83_ga(x1, x3)
DELETE1_IN_AAG(x1, x2, x3) = DELETE1_IN_AAG(x3)
P44_IN_GAAG(x1, x2, x3, x4) = P44_IN_GAAG(x1, x4)
U5_GAAG(x1, x2, x3, x4, x5) = U5_GAAG(x1, x4, x5)
P72_IN_GAAG(x1, x2, x3, x4) = P72_IN_GAAG(x1, x4)
P79_IN_GAAG(x1, x2, x3, x4) = P79_IN_GAAG(x1, x4)
U16_GAAG(x1, x2, x3, x4, x5) = U16_GAAG(x1, x4, x5)
P116_IN_GAAG(x1, x2, x3, x4) = P116_IN_GAAG(x1, x4)

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

(52) PiDPToQDPProof (SOUND transformation)

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

(53) Obligation:

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

DELETE1_IN_AAG(tree(T163, T164, T166)) → P44_IN_GAAG(T163, T166)
P44_IN_GAAG(T163, T166) → U5_GAAG(T163, T166, lessc46_in_ga(T163))
U5_GAAG(T163, T166, lessc46_out_ga(T163)) → DELETE1_IN_AAG(T166)
DELETE1_IN_AAG(tree(T260, T261, T263)) → P72_IN_GAAG(T260, T263)
P72_IN_GAAG(0, T263) → DELETE1_IN_AAG(T263)
DELETE1_IN_AAG(tree(T458, T459, T461)) → P116_IN_GAAG(T458, T461)
P116_IN_GAAG(0, T461) → DELETE1_IN_AAG(T461)
DELETE1_IN_AAG(tree(0, T653, T655)) → DELETE1_IN_AAG(T655)
DELETE1_IN_AAG(tree(s(T673), T653, T655)) → P79_IN_GAAG(T673, T655)
P79_IN_GAAG(T281, T263) → U16_GAAG(T281, T263, lessc46_in_ga(T281))
U16_GAAG(T281, T263, lessc46_out_ga(T281)) → DELETE1_IN_AAG(T263)
P116_IN_GAAG(s(T479), T461) → P79_IN_GAAG(T479, T461)
P72_IN_GAAG(s(T281), T263) → P79_IN_GAAG(T281, T263)

The TRS R consists of the following rules:

lessc46_in_ga(0) → lessc46_out_ga(0)
lessc46_in_ga(s(T184)) → U83_ga(T184, lessc46_in_ga(T184))
U83_ga(T184, lessc46_out_ga(T184)) → lessc46_out_ga(s(T184))

The set Q consists of the following terms:

lessc46_in_ga(x0)
U83_ga(x0, x1)

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

(54) 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:

P44_IN_GAAG(T163, T166) → U5_GAAG(T163, T166, lessc46_in_ga(T163))
The graph contains the following edges 1 >= 1, 2 >= 2
U5_GAAG(T163, T166, lessc46_out_ga(T163)) → DELETE1_IN_AAG(T166)
The graph contains the following edges 2 >= 1
DELETE1_IN_AAG(tree(T163, T164, T166)) → P44_IN_GAAG(T163, T166)
The graph contains the following edges 1 > 1, 1 > 2
DELETE1_IN_AAG(tree(0, T653, T655)) → DELETE1_IN_AAG(T655)
The graph contains the following edges 1 > 1
P72_IN_GAAG(0, T263) → DELETE1_IN_AAG(T263)
The graph contains the following edges 2 >= 1
P72_IN_GAAG(s(T281), T263) → P79_IN_GAAG(T281, T263)
The graph contains the following edges 1 > 1, 2 >= 2
DELETE1_IN_AAG(tree(T260, T261, T263)) → P72_IN_GAAG(T260, T263)
The graph contains the following edges 1 > 1, 1 > 2
P116_IN_GAAG(0, T461) → DELETE1_IN_AAG(T461)
The graph contains the following edges 2 >= 1
U16_GAAG(T281, T263, lessc46_out_ga(T281)) → DELETE1_IN_AAG(T263)
The graph contains the following edges 2 >= 1
P116_IN_GAAG(s(T479), T461) → P79_IN_GAAG(T479, T461)
The graph contains the following edges 1 > 1, 2 >= 2
P79_IN_GAAG(T281, T263) → U16_GAAG(T281, T263, lessc46_in_ga(T281))
The graph contains the following edges 1 >= 1, 2 >= 2
DELETE1_IN_AAG(tree(T458, T459, T461)) → P116_IN_GAAG(T458, T461)
The graph contains the following edges 1 > 1, 1 > 2
DELETE1_IN_AAG(tree(s(T673), T653, T655)) → P79_IN_GAAG(T673, T655)
The graph contains the following edges 1 > 1, 1 > 2

(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 (SOUND transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (EQUIVALENT transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (EQUIVALENT transformation)

(25) Obligation:

(26) QDPSizeChangeProof (EQUIVALENT transformation)

(27) YES

(28) Obligation:

(29) UsableRulesProof (EQUIVALENT transformation)

(30) Obligation:

(31) PiDPToQDPProof (SOUND transformation)

(32) Obligation:

(33) QDPSizeChangeProof (EQUIVALENT transformation)

(34) YES

(35) Obligation:

(36) UsableRulesProof (EQUIVALENT transformation)

(37) Obligation:

(38) PiDPToQDPProof (SOUND transformation)

(39) Obligation:

(40) QDPSizeChangeProof (EQUIVALENT transformation)

(41) YES

(42) Obligation:

(43) UsableRulesProof (EQUIVALENT transformation)

(44) Obligation:

(45) PiDPToQDPProof (SOUND transformation)

(46) Obligation:

(47) QDPSizeChangeProof (EQUIVALENT transformation)

(48) YES

(49) Obligation:

(50) UsableRulesProof (EQUIVALENT transformation)

(51) Obligation:

(52) PiDPToQDPProof (SOUND transformation)

(53) Obligation:

(54) QDPSizeChangeProof (EQUIVALENT transformation)

(55) YES