Left Termination proof of /tmp/tmpkcEzHJ/delete-bff.pl

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

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 NonTerminationProof (⇔)

        ↳27 NO

    ↳28 PiDP

        ↳29 PiDPToQDPProof (⇐)

        ↳30 QDP

        ↳31 Narrowing (⇐)

        ↳32 QDP

        ↳33 Narrowing (⇐)

        ↳34 QDP

        ↳35 Narrowing (⇐)

        ↳36 QDP

        ↳37 Narrowing (⇐)

        ↳38 QDP

        ↳39 Instantiation (⇔)

        ↳40 QDP

        ↳41 Instantiation (⇔)

        ↳42 QDP

        ↳43 Instantiation (⇔)

        ↳44 QDP

        ↳45 DependencyGraphProof (⇔)

        ↳46 AND

            ↳47 QDP

                ↳48 Instantiation (⇔)

                ↳49 QDP

                ↳50 Instantiation (⇔)

                ↳51 QDP

                ↳52 Instantiation (⇔)

                ↳53 QDP

                ↳54 Instantiation (⇔)

                ↳55 QDP

                ↳56 Instantiation (⇔)

                ↳57 QDP

                ↳58 ForwardInstantiation (⇔)

                ↳59 QDP

                ↳60 ForwardInstantiation (⇔)

                ↳61 QDP

                ↳62 ForwardInstantiation (⇔)

                ↳63 QDP

                ↳64 ForwardInstantiation (⇔)

                ↳65 QDP

                ↳66 NonTerminationProof (⇔)

                ↳67 NO

            ↳68 QDP

                ↳69 UsableRulesProof (⇔)

                ↳70 QDP

                ↳71 QReductionProof (⇔)

                ↳72 QDP

                ↳73 NonTerminationProof (⇔)

                ↳74 NO

(0) Obligation:

Clauses:

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

Queries:

delete(g,a,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: delete(T1, T2, T3)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | delete(T6, T2, T3), SCOPE: 1, CLAUSE: 1 | delete(T6, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T6, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T6, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\ndelete(T1, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: delete(T6, T2, T3), SCOPE: 1, CLAUSE: 1 | delete(T6, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T6, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T6, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: true | delete(T10, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T10, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T10, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: delete(T6, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T6, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T6, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT6 is ground\ndelete(T6, T2, T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: delete(T10, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T10, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T10, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: delmin(T22, T23, T24) | delete(T17, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T17, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: delete(T10, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T10, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT10 is ground\ndelete(T10, T2, T3) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: delmin(T22, T23, T24), SCOPE: 2, CLAUSE: 5 | delmin(T22, T23, T24), SCOPE: 2, CLAUSE: 6 | ?_2 | delete(T17, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T17, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: delmin(T22, T23, T24), SCOPE: 2, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: delmin(T22, T23, T24), SCOPE: 2, CLAUSE: 6 | ?_2 | delete(T17, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T17, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT17 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, T23, T24), SCOPE: 2, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ?_2 | delete(T17, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T17, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: delmin(T65, T66, T67)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: delmin(T65, T66, T67), SCOPE: 3, CLAUSE: 5 | delmin(T65, T66, T67), SCOPE: 3, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: delmin(T65, T66, T67), SCOPE: 3, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: delmin(T65, T66, T67), SCOPE: 3, CLAUSE: 6\n\n", 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(T100, T101, T102)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: delete(T17, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T17, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: delete(T17, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: delete(T17, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(less(T127, T132), delete(T127, T133, T134))\n\nT127 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: less(T127, T132)\n\nT127 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: delete(T127, T137, T138)\n\nT127 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: less(T127, T132), SCOPE: 4, CLAUSE: 7 | less(T127, T132), SCOPE: 4, CLAUSE: 8\n\nT127 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: less(T127, T132), SCOPE: 4, CLAUSE: 7\n\nT127 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: less(T127, T132), SCOPE: 4, CLAUSE: 8\n\nT127 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(T150, T152)\n\nT150 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(less(T174, T169), delete(T169, T175, T176))\n\nT169 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: less(T174, T169)\n\nT169 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: delete(T169, T179, T180)\n\nT169 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: less(T174, T169), SCOPE: 5, CLAUSE: 7 | less(T174, T169), SCOPE: 5, CLAUSE: 8\n\nT169 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: less(T174, T169), SCOPE: 5, CLAUSE: 7\n\nT169 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: less(T174, T169), SCOPE: 5, CLAUSE: 8\n\nT169 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(T194, T193)\n\nT193 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(less(T206, T211), delete(T206, T212, T213)) | delete(T206, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT206 is ground\ndelete(T206, T2, T3) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: delete(T10, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT10 is ground\ndelete(T10, T2, T3) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))\ndelete(T10, T2, T3) !=? delete(X226, tree(X227, X228, X229), tree(X227, X230, X229))", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(less(T206, T211), delete(T206, T212, T213)), SCOPE: 6, CLAUSE: 7 | ','(less(T206, T211), delete(T206, T212, T213)), SCOPE: 6, CLAUSE: 8 | ?_6 | delete(T206, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT206 is ground\ndelete(T206, T2, T3) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(less(T206, T211), delete(T206, T212, T213)), SCOPE: 6, CLAUSE: 7\n\nT206 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(less(T206, T211), delete(T206, T212, T213)), SCOPE: 6, CLAUSE: 8 | ?_6 | delete(T206, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT206 is ground\ndelete(T206, T2, T3) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: delete(0, T219, T220)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(less(T206, T211), delete(T206, T212, T213)), SCOPE: 6, CLAUSE: 8\n\nT206 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ?_6 | delete(T206, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT206 is ground\ndelete(T206, T2, T3) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(less(T231, T233), delete(s(T231), T234, T235))\n\nT231 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: less(T231, T233)\n\nT231 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: delete(s(T231), T238, T239)\n\nT231 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: delete(T206, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT206 is ground\ndelete(T206, T2, T3) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(less(T261, T256), delete(T256, T262, T263))\n\nT256 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(less(T276, T271), delete(T271, T277, T278))\n\nT271 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(less(T276, T271), delete(T271, T277, T278)), SCOPE: 7, CLAUSE: 7 | ','(less(T276, T271), delete(T271, T277, T278)), SCOPE: 7, CLAUSE: 8\n\nT271 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(less(T276, T271), delete(T271, T277, T278)), SCOPE: 7, CLAUSE: 7\n\nT271 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(less(T276, T271), delete(T271, T277, T278)), SCOPE: 7, CLAUSE: 8\n\nT271 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: delete(s(T283), T284, T285)\n\nT283 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(less(T296, T295), delete(s(T295), T297, T298))\n\nT295 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: less(T296, T295)\n\nT295 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: delete(s(T295), T301, T302)\n\nT295 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: delmin(T319, T320, T321) | delete(T314, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T314, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT314 is ground\ndelete(T314, T2, T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: delete(T6, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T6, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT6 is ground\ndelete(T6, T2, T3) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T6, T2, T3) !=? delete(X334, tree(X334, X335, X336), tree(X337, X335, X338))", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: delmin(T319, T320, T321), SCOPE: 8, CLAUSE: 5 | delmin(T319, T320, T321), SCOPE: 8, CLAUSE: 6 | ?_8 | delete(T314, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T314, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT314 is ground\ndelete(T314, T2, T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: delmin(T319, T320, T321), SCOPE: 8, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: delmin(T319, T320, T321), SCOPE: 8, CLAUSE: 6 | ?_8 | delete(T314, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T314, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT314 is ground\ndelete(T314, T2, T3) !=? 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(T319, T320, T321), SCOPE: 8, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ?_8 | delete(T314, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T314, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT314 is ground\ndelete(T314, T2, T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: delmin(T362, T363, T364)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: delete(T314, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T314, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT314 is ground\ndelete(T314, T2, T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: delete(T314, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT314 is ground\ndelete(T314, T2, T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: delete(T314, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT314 is ground\ndelete(T314, T2, T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(less(T389, T394), delete(T389, T395, T396))\n\nT389 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(less(T414, T409), delete(T409, T415, T416))\n\nT409 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ','(less(T424, T429), delete(T424, T430, T431)) | delete(T424, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT424 is ground\ndelete(T424, T2, T3) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T424, T2, T3) !=? delete(X334, tree(X334, X335, X336), tree(X337, X335, X338))", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: delete(T6, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT6 is ground\ndelete(T6, T2, T3) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T6, T2, T3) !=? delete(X334, tree(X334, X335, X336), tree(X337, X335, X338))\ndelete(T6, T2, T3) !=? delete(X455, tree(X456, X457, X458), tree(X456, X459, X458))", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(less(T424, T429), delete(T424, T430, T431)), SCOPE: 9, CLAUSE: 7 | ','(less(T424, T429), delete(T424, T430, T431)), SCOPE: 9, CLAUSE: 8 | ?_9 | delete(T424, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT424 is ground\ndelete(T424, T2, T3) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T424, T2, T3) !=? delete(X334, tree(X334, X335, X336), tree(X337, X335, X338))", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(less(T424, T429), delete(T424, T430, T431)), SCOPE: 9, CLAUSE: 7\n\nT424 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(less(T424, T429), delete(T424, T430, T431)), SCOPE: 9, CLAUSE: 8 | ?_9 | delete(T424, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT424 is ground\ndelete(T424, T2, T3) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T424, T2, T3) !=? delete(X334, tree(X334, X335, X336), tree(X337, X335, X338))", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: delete(0, T437, T438)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(less(T424, T429), delete(T424, T430, T431)), SCOPE: 9, CLAUSE: 8\n\nT424 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ?_9 | delete(T424, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT424 is ground\ndelete(T424, T2, T3) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T424, T2, T3) !=? delete(X334, tree(X334, X335, X336), tree(X337, X335, X338))", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(less(T449, T451), delete(s(T449), T452, T453))\n\nT449 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: delete(T424, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT424 is ground\ndelete(T424, T2, T3) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T424, T2, T3) !=? delete(X334, tree(X334, X335, X336), tree(X337, X335, X338))", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: ','(less(T471, T466), delete(T466, T472, T473))\n\nT466 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ','(less(T486, T481), delete(T481, T487, T488))\n\nT481 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: ','(less(T486, T481), delete(T481, T487, T488)), SCOPE: 10, CLAUSE: 7 | ','(less(T486, T481), delete(T481, T487, T488)), SCOPE: 10, CLAUSE: 8\n\nT481 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(less(T486, T481), delete(T481, T487, T488)), SCOPE: 10, CLAUSE: 7\n\nT481 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(less(T486, T481), delete(T481, T487, T488)), SCOPE: 10, CLAUSE: 8\n\nT481 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: delete(s(T493), T494, T495)\n\nT493 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: ','(less(T506, T505), delete(s(T505), T507, T508))\n\nT505 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: true | delete(T513, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T513, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T513, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT513 is ground\ndelete(T513, T2, T3) !=? 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\nT1 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(T513, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T513, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T513, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT513 is ground\ndelete(T513, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: delmin(T525, T526, T527) | delete(T520, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T520, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT520 is ground\ndelete(T520, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: delete(T513, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T513, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT513 is ground\ndelete(T513, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T513, T2, T3) !=? delete(X557, tree(X557, X558, X559), tree(X560, X558, X561))", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: delmin(T525, T526, T527), SCOPE: 11, CLAUSE: 5 | delmin(T525, T526, T527), SCOPE: 11, CLAUSE: 6 | ?_11 | delete(T520, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T520, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT520 is ground\ndelete(T520, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: delmin(T525, T526, T527), SCOPE: 11, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: delmin(T525, T526, T527), SCOPE: 11, CLAUSE: 6 | ?_11 | delete(T520, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T520, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT520 is ground\ndelete(T520, T2, T3) !=? 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(T525, T526, T527), SCOPE: 11, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ?_11 | delete(T520, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T520, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT520 is ground\ndelete(T520, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: delmin(T568, T569, T570)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: delete(T520, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T520, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT520 is ground\ndelete(T520, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: delete(T520, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT520 is ground\ndelete(T520, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: delete(T520, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT520 is ground\ndelete(T520, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ','(less(T595, T600), delete(T595, T601, T602))\n\nT595 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: ','(less(T620, T615), delete(T615, T621, T622))\n\nT615 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: ','(less(T630, T635), delete(T630, T636, T637)) | delete(T630, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT630 is ground\ndelete(T630, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T630, T2, T3) !=? delete(X557, tree(X557, X558, X559), tree(X560, X558, X561))", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: delete(T513, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT513 is ground\ndelete(T513, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T513, T2, T3) !=? delete(X557, tree(X557, X558, X559), tree(X560, X558, X561))\ndelete(T513, T2, T3) !=? delete(X678, tree(X679, X680, X681), tree(X679, X682, X681))", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: ','(less(T630, T635), delete(T630, T636, T637)), SCOPE: 12, CLAUSE: 7 | ','(less(T630, T635), delete(T630, T636, T637)), SCOPE: 12, CLAUSE: 8 | ?_12 | delete(T630, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT630 is ground\ndelete(T630, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T630, T2, T3) !=? delete(X557, tree(X557, X558, X559), tree(X560, X558, X561))", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: ','(less(T630, T635), delete(T630, T636, T637)), SCOPE: 12, CLAUSE: 7\n\nT630 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: ','(less(T630, T635), delete(T630, T636, T637)), SCOPE: 12, CLAUSE: 8 | ?_12 | delete(T630, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT630 is ground\ndelete(T630, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T630, T2, T3) !=? delete(X557, tree(X557, X558, X559), tree(X560, X558, X561))", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: delete(0, T643, T644)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: ','(less(T630, T635), delete(T630, T636, T637)), SCOPE: 12, CLAUSE: 8\n\nT630 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: ?_12 | delete(T630, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT630 is ground\ndelete(T630, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T630, T2, T3) !=? delete(X557, tree(X557, X558, X559), tree(X560, X558, X561))", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: ','(less(T655, T657), delete(s(T655), T658, T659))\n\nT655 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: delete(T630, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT630 is ground\ndelete(T630, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T630, T2, T3) !=? delete(X557, tree(X557, X558, X559), tree(X560, X558, X561))", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: ','(less(T677, T672), delete(T672, T678, T679))\n\nT672 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ','(less(T692, T687), delete(T687, T693, T694))\n\nT687 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: ','(less(T692, T687), delete(T687, T693, T694)), SCOPE: 13, CLAUSE: 7 | ','(less(T692, T687), delete(T687, T693, T694)), SCOPE: 13, CLAUSE: 8\n\nT687 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ','(less(T692, T687), delete(T687, T693, T694)), SCOPE: 13, CLAUSE: 7\n\nT687 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: ','(less(T692, T687), delete(T687, T693, T694)), SCOPE: 13, CLAUSE: 8\n\nT687 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: delete(s(T699), T700, T701)\n\nT699 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: ','(less(T712, T711), delete(s(T711), T713, T714))\n\nT711 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: delmin(T727, T728, T729) | delete(T722, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T722, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT722 is ground\ndelete(T722, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T722, T2, T3) !=? 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\nT1 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(T727, T728, T729), SCOPE: 14, CLAUSE: 5 | delmin(T727, T728, T729), SCOPE: 14, CLAUSE: 6 | ?_14 | delete(T722, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T722, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT722 is ground\ndelete(T722, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T722, T2, T3) !=? delete(X548, tree(X548, X549, void), X549)", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: delmin(T727, T728, T729), SCOPE: 14, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: delmin(T727, T728, T729), SCOPE: 14, CLAUSE: 6 | ?_14 | delete(T722, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T722, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT722 is ground\ndelete(T722, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T722, T2, T3) !=? 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(T727, T728, T729), SCOPE: 14, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: ?_14 | delete(T722, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T722, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT722 is ground\ndelete(T722, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T722, T2, T3) !=? delete(X548, tree(X548, X549, void), X549)", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: delmin(T770, T771, T772)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: delete(T722, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T722, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT722 is ground\ndelete(T722, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T722, T2, T3) !=? delete(X548, tree(X548, X549, void), X549)", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: delete(T722, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT722 is ground\ndelete(T722, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T722, T2, T3) !=? delete(X548, tree(X548, X549, void), X549)", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: delete(T722, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT722 is ground\ndelete(T722, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T722, T2, T3) !=? delete(X548, tree(X548, X549, void), X549)", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: ','(less(T797, T802), delete(T797, T803, T804))\n\nT797 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: ','(less(T822, T817), delete(T817, T823, T824))\n\nT817 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: ','(less(T832, T837), delete(T832, T838, T839)) | delete(T832, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT832 is ground\ndelete(T832, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T832, T2, T3) !=? delete(X548, tree(X548, X549, void), X549)\ndelete(T832, T2, T3) !=? 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\nT1 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(T832, T837), delete(T832, T838, T839)), SCOPE: 15, CLAUSE: 7 | ','(less(T832, T837), delete(T832, T838, T839)), SCOPE: 15, CLAUSE: 8 | ?_15 | delete(T832, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT832 is ground\ndelete(T832, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T832, T2, T3) !=? delete(X548, tree(X548, X549, void), X549)\ndelete(T832, T2, T3) !=? delete(X774, tree(X774, X775, X776), tree(X777, X775, X778))", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: ','(less(T832, T837), delete(T832, T838, T839)), SCOPE: 15, CLAUSE: 7\n\nT832 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(less(T832, T837), delete(T832, T838, T839)), SCOPE: 15, CLAUSE: 8 | ?_15 | delete(T832, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT832 is ground\ndelete(T832, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T832, T2, T3) !=? delete(X548, tree(X548, X549, void), X549)\ndelete(T832, T2, T3) !=? delete(X774, tree(X774, X775, X776), tree(X777, X775, X778))", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: delete(0, T845, T846)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ','(less(T832, T837), delete(T832, T838, T839)), SCOPE: 15, CLAUSE: 8\n\nT832 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: ?_15 | delete(T832, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT832 is ground\ndelete(T832, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T832, T2, T3) !=? delete(X548, tree(X548, X549, void), X549)\ndelete(T832, T2, T3) !=? delete(X774, tree(X774, X775, X776), tree(X777, X775, X778))", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: ','(less(T857, T859), delete(s(T857), T860, T861))\n\nT857 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: delete(T832, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT832 is ground\ndelete(T832, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T832, T2, T3) !=? delete(X548, tree(X548, X549, void), X549)\ndelete(T832, T2, T3) !=? delete(X774, tree(X774, X775, X776), tree(X777, X775, X778))", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: ','(less(T879, T874), delete(T874, T880, T881))\n\nT874 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: ','(less(T894, T889), delete(T889, T895, T896))\n\nT889 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: ','(less(T894, T889), delete(T889, T895, T896)), SCOPE: 16, CLAUSE: 7 | ','(less(T894, T889), delete(T889, T895, T896)), SCOPE: 16, CLAUSE: 8\n\nT889 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: ','(less(T894, T889), delete(T889, T895, T896)), SCOPE: 16, CLAUSE: 7\n\nT889 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: ','(less(T894, T889), delete(T889, T895, T896)), SCOPE: 16, CLAUSE: 8\n\nT889 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: delete(s(T901), T902, T903)\n\nT901 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: ','(less(T914, T913), delete(s(T913), T915, T916))\n\nT913 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 -> T513\nX548 -> T513\nX549 -> T514\nT2 -> tree(T513, T514, void)\nT3 -> T514", 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\nT6 -> T10\nX12 -> T10\nX13 -> T11\nT2 -> tree(T10, T11, void)\nT3 -> 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\nT6 -> T314\nX334 -> T314\nX335 -> T315\nX336 -> T319\nT2 -> tree(T314, T315, T319)\nX337 -> T320\nX338 -> T321\nT3 -> tree(T320, T315, T321)\nT316 -> T319\nT317 -> T320\nT318 -> T321", 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\nT10 -> T17\nX21 -> T17\nX22 -> T18\nX23 -> T22\nT2 -> tree(T17, T18, T22)\nX24 -> T23\nX25 -> T24\nT3 -> tree(T23, T18, T24)\nT19 -> T22\nT20 -> T23\nT21 -> T24", 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\nT10 -> T206\nX226 -> T206\nX227 -> T211\nX228 -> T212\nX229 -> T209\nT2 -> tree(T211, T212, T209)\nX230 -> T213\nT3 -> tree(T211, T213, T209)\nT207 -> T211\nT208 -> T212\nT210 -> T213", 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 -> T33\nX40 -> T34\nT22 -> tree(T33, void, T34)\nT23 -> T33\nT24 -> T34", 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 -> T59\nX68 -> T65\nX69 -> T61\nT22 -> tree(T59, T65, T61)\nT23 -> T66\nX70 -> T66\nX71 -> T67\nX72 -> T64\nT24 -> tree(T59, T67, T64)\nT60 -> T65\nT62 -> T66\nT63 -> T67", 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 -> T80\nX92 -> T81\nT65 -> tree(T80, void, T81)\nT66 -> T80\nT67 -> T81", 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 -> T94\nX108 -> T100\nX109 -> T96\nT65 -> tree(T94, T100, T96)\nT66 -> T101\nX110 -> T101\nX111 -> T102\nX112 -> T99\nT67 -> tree(T94, T102, T99)\nT95 -> T100\nT97 -> T101\nT98 -> T102", 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:\nT65 -> T100\nT66 -> T101\nT67 -> T102", 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\nT17 -> T127\nX143 -> T127\nX144 -> T132\nX145 -> T133\nX146 -> T130\nT2 -> tree(T132, T133, T130)\nX147 -> T134\nT3 -> tree(T132, T134, T130)\nT128 -> T132\nT129 -> T133\nT131 -> T134", 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\nT17 -> T169\nX187 -> T169\nX188 -> T174\nX189 -> T171\nX190 -> T175\nT2 -> tree(T174, T171, T175)\nX191 -> T176\nT3 -> tree(T174, T171, T176)\nT170 -> T174\nT172 -> T175\nT173 -> T176", 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\nreplacements:\nT133 -> T137\nT134 -> T138", 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 -> T127\nT2 -> T137\nT3 -> T138", 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\nT127 -> 0\nX161 -> T145\nT132 -> s(T145)", 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 -> T150\nT127 -> s(T150)\nX168 -> T152\nT132 -> s(T152)\nT151 -> T152", 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:\nT127 -> T150\nT132 -> T152", 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\nnew knowledge:\nT174 is ground\nreplacements:\nT175 -> T179\nT176 -> T180", 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 -> T169\nT2 -> T179\nT3 -> T180", 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\nT174 -> 0\nX205 -> T187\nT169 -> s(T187)", 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 -> T194\nT174 -> s(T194)\nX212 -> T193\nT169 -> s(T193)\nT192 -> T194", 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:\nT174 -> T194\nT169 -> T193", 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\nT10 -> T271\nX293 -> T271\nX294 -> T276\nX295 -> T273\nX296 -> T277\nT2 -> tree(T276, T273, T277)\nX297 -> T278\nT3 -> tree(T276, T273, T278)\nT272 -> T276\nT274 -> T277\nT275 -> T278", 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\nT206 -> 0\nX240 -> T218\nT211 -> s(T218)\nT212 -> T219\nT213 -> T220", 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 -> T219\nT3 -> T220", 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 -> T231\nT206 -> s(T231)\nX255 -> T233\nT211 -> s(T233)\nT232 -> T233\nT212 -> T234\nT213 -> T235", 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\nreplacements:\nT234 -> T238\nT235 -> T239", fontsize=14, style = filled, fillcolor = violet];
65 -> 291 [arrowhead = none ];
291 -> 68;

292 [label="INSTANCE with matching:\nT127 -> T231\nT132 -> T233", fontsize=14, style = filled, fillcolor = lightgrey];
67 -> 292 [arrowhead = none , style=dashed];
292 -> 34[style=dashed];

293 [label="INSTANCE with matching:\nT1 -> s(T231)\nT2 -> T238\nT3 -> T239", 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\nT206 -> T256\nX276 -> T256\nX277 -> T261\nX278 -> T258\nX279 -> T262\nT2 -> tree(T261, T258, T262)\nX280 -> T263\nT3 -> tree(T261, T258, T263)\nT257 -> T261\nT259 -> T262\nT260 -> T263", 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:\nT174 -> T261\nT169 -> T256\nT175 -> T262\nT176 -> T263", 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\nT276 -> 0\nX307 -> T283\nT271 -> s(T283)\nT277 -> T284\nT278 -> T285", 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 -> T296\nT276 -> s(T296)\nX318 -> T295\nT271 -> s(T295)\nT294 -> T296\nT277 -> T297\nT278 -> T298", 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(T283)\nT2 -> T284\nT3 -> T285", 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\nnew knowledge:\nT296 is ground\nreplacements:\nT297 -> T301\nT298 -> T302", fontsize=14, style = filled, fillcolor = violet];
79 -> 306 [arrowhead = none ];
306 -> 82;

307 [label="INSTANCE with matching:\nT174 -> T296\nT169 -> T295", fontsize=14, style = filled, fillcolor = lightgrey];
81 -> 307 [arrowhead = none , style=dashed];
307 -> 46[style=dashed];

308 [label="INSTANCE with matching:\nT1 -> s(T295)\nT2 -> T301\nT3 -> T302", 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\nT6 -> T424\nX455 -> T424\nX456 -> T429\nX457 -> T430\nX458 -> T427\nT2 -> tree(T429, T430, T427)\nX459 -> T431\nT3 -> tree(T429, T431, T427)\nT425 -> T429\nT426 -> T430\nT428 -> T431", 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 -> T330\nX353 -> T331\nT319 -> tree(T330, void, T331)\nT320 -> T330\nT321 -> T331", 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 -> T356\nX381 -> T362\nX382 -> T358\nT319 -> tree(T356, T362, T358)\nT320 -> T363\nX383 -> T363\nX384 -> T364\nX385 -> T361\nT321 -> tree(T356, T364, T361)\nT357 -> T362\nT359 -> T363\nT360 -> T364", 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:\nT65 -> T362\nT66 -> T363\nT67 -> T364", 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\nT314 -> T389\nX416 -> T389\nX417 -> T394\nX418 -> T395\nX419 -> T392\nT2 -> tree(T394, T395, T392)\nX420 -> T396\nT3 -> tree(T394, T396, T392)\nT390 -> T394\nT391 -> T395\nT393 -> T396", 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\nT314 -> T409\nX438 -> T409\nX439 -> T414\nX440 -> T411\nX441 -> T415\nT2 -> tree(T414, T411, T415)\nX442 -> T416\nT3 -> tree(T414, T411, T416)\nT410 -> T414\nT412 -> T415\nT413 -> T416", 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:\nT127 -> T389\nT132 -> T394\nT133 -> T395\nT134 -> T396", fontsize=14, style = filled, fillcolor = lightgrey];
98 -> 329 [arrowhead = none , style=dashed];
329 -> 32[style=dashed];

330 [label="INSTANCE with matching:\nT276 -> T414\nT271 -> T409\nT277 -> T415\nT278 -> T416", 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\nT6 -> T481\nX516 -> T481\nX517 -> T486\nX518 -> T483\nX519 -> T487\nT2 -> tree(T486, T483, T487)\nX520 -> T488\nT3 -> tree(T486, T483, T488)\nT482 -> T486\nT484 -> T487\nT485 -> T488", 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\nT424 -> 0\nX469 -> T436\nT429 -> s(T436)\nT430 -> T437\nT431 -> T438", 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 -> T437\nT3 -> T438", 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 -> T449\nT424 -> s(T449)\nX484 -> T451\nT429 -> s(T451)\nT450 -> T451\nT430 -> T452\nT431 -> T453", 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:\nT231 -> T449\nT233 -> T451\nT234 -> T452\nT235 -> T453", 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\nT424 -> T466\nX499 -> T466\nX500 -> T471\nX501 -> T468\nX502 -> T472\nT2 -> tree(T471, T468, T472)\nX503 -> T473\nT3 -> tree(T471, T468, T473)\nT467 -> T471\nT469 -> T472\nT470 -> T473", 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:\nT276 -> T471\nT271 -> T466\nT277 -> T472\nT278 -> T473", 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\nT486 -> 0\nX530 -> T493\nT481 -> s(T493)\nT487 -> T494\nT488 -> T495", 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 -> T506\nT486 -> s(T506)\nX541 -> T505\nT481 -> s(T505)\nT504 -> T506\nT487 -> T507\nT488 -> T508", 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(T493)\nT2 -> T494\nT3 -> T495", fontsize=14, style = filled, fillcolor = lightgrey];
121 -> 355 [arrowhead = none , style=dashed];
355 -> 1[style=dashed];

356 [label="INSTANCE with matching:\nT296 -> T506\nT295 -> T505\nT297 -> T507\nT298 -> T508", 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 -> T722\nX774 -> T722\nX775 -> T723\nX776 -> T727\nT2 -> tree(T722, T723, T727)\nX777 -> T728\nX778 -> T729\nT3 -> tree(T728, T723, T729)\nT724 -> T727\nT725 -> T728\nT726 -> T729", 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\nT513 -> T520\nX557 -> T520\nX558 -> T521\nX559 -> T525\nT2 -> tree(T520, T521, T525)\nX560 -> T526\nX561 -> T527\nT3 -> tree(T526, T521, T527)\nT522 -> T525\nT523 -> T526\nT524 -> T527", 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\nT513 -> T630\nX678 -> T630\nX679 -> T635\nX680 -> T636\nX681 -> T633\nT2 -> tree(T635, T636, T633)\nX682 -> T637\nT3 -> tree(T635, T637, T633)\nT631 -> T635\nT632 -> T636\nT634 -> T637", 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 -> T536\nX576 -> T537\nT525 -> tree(T536, void, T537)\nT526 -> T536\nT527 -> T537", 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 -> T562\nX604 -> T568\nX605 -> T564\nT525 -> tree(T562, T568, T564)\nT526 -> T569\nX606 -> T569\nX607 -> T570\nX608 -> T567\nT527 -> tree(T562, T570, T567)\nT563 -> T568\nT565 -> T569\nT566 -> T570", 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:\nT362 -> T568\nT363 -> T569\nT364 -> T570", 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\nT520 -> T595\nX639 -> T595\nX640 -> T600\nX641 -> T601\nX642 -> T598\nT2 -> tree(T600, T601, T598)\nX643 -> T602\nT3 -> tree(T600, T602, T598)\nT596 -> T600\nT597 -> T601\nT599 -> T602", 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\nT520 -> T615\nX661 -> T615\nX662 -> T620\nX663 -> T617\nX664 -> T621\nT2 -> tree(T620, T617, T621)\nX665 -> T622\nT3 -> tree(T620, T617, T622)\nT616 -> T620\nT618 -> T621\nT619 -> T622", 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:\nT389 -> T595\nT394 -> T600\nT395 -> T601\nT396 -> T602", fontsize=14, style = filled, fillcolor = lightgrey];
143 -> 382 [arrowhead = none , style=dashed];
382 -> 98[style=dashed];

383 [label="INSTANCE with matching:\nT486 -> T620\nT481 -> T615\nT487 -> T621\nT488 -> T622", 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\nT513 -> T687\nX739 -> T687\nX740 -> T692\nX741 -> T689\nX742 -> T693\nT2 -> tree(T692, T689, T693)\nX743 -> T694\nT3 -> tree(T692, T689, T694)\nT688 -> T692\nT690 -> T693\nT691 -> T694", 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\nT630 -> 0\nX692 -> T642\nT635 -> s(T642)\nT636 -> T643\nT637 -> T644", 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 -> T643\nT3 -> T644", 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 -> T655\nT630 -> s(T655)\nX707 -> T657\nT635 -> s(T657)\nT656 -> T657\nT636 -> T658\nT637 -> T659", 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:\nT449 -> T655\nT451 -> T657\nT452 -> T658\nT453 -> T659", 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\nT630 -> T672\nX722 -> T672\nX723 -> T677\nX724 -> T674\nX725 -> T678\nT2 -> tree(T677, T674, T678)\nX726 -> T679\nT3 -> tree(T677, T674, T679)\nT673 -> T677\nT675 -> T678\nT676 -> T679", 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:\nT486 -> T677\nT481 -> T672\nT487 -> T678\nT488 -> T679", 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\nT692 -> 0\nX753 -> T699\nT687 -> s(T699)\nT693 -> T700\nT694 -> T701", 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 -> T712\nT692 -> s(T712)\nX764 -> T711\nT687 -> s(T711)\nT710 -> T712\nT693 -> T713\nT694 -> T714", 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(T699)\nT2 -> T700\nT3 -> T701", fontsize=14, style = filled, fillcolor = lightgrey];
166 -> 408 [arrowhead = none , style=dashed];
408 -> 1[style=dashed];

409 [label="INSTANCE with matching:\nT506 -> T712\nT505 -> T711\nT507 -> T713\nT508 -> T714", 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 -> T832\nX895 -> T832\nX896 -> T837\nX897 -> T838\nX898 -> T835\nT2 -> tree(T837, T838, T835)\nX899 -> T839\nT3 -> tree(T837, T839, T835)\nT833 -> T837\nT834 -> T838\nT836 -> T839", 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 -> T738\nX793 -> T739\nT727 -> tree(T738, void, T739)\nT728 -> T738\nT729 -> T739", 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 -> T764\nX821 -> T770\nX822 -> T766\nT727 -> tree(T764, T770, T766)\nT728 -> T771\nX823 -> T771\nX824 -> T772\nX825 -> T769\nT729 -> tree(T764, T772, T769)\nT765 -> T770\nT767 -> T771\nT768 -> T772", 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:\nT362 -> T770\nT363 -> T771\nT364 -> T772", 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\nT722 -> T797\nX856 -> T797\nX857 -> T802\nX858 -> T803\nX859 -> T800\nT2 -> tree(T802, T803, T800)\nX860 -> T804\nT3 -> tree(T802, T804, T800)\nT798 -> T802\nT799 -> T803\nT801 -> T804", 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\nT722 -> T817\nX878 -> T817\nX879 -> T822\nX880 -> T819\nX881 -> T823\nT2 -> tree(T822, T819, T823)\nX882 -> T824\nT3 -> tree(T822, T819, T824)\nT818 -> T822\nT820 -> T823\nT821 -> T824", 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:\nT389 -> T797\nT394 -> T802\nT395 -> T803\nT396 -> T804", fontsize=14, style = filled, fillcolor = lightgrey];
185 -> 430 [arrowhead = none , style=dashed];
430 -> 98[style=dashed];

431 [label="INSTANCE with matching:\nT486 -> T822\nT481 -> T817\nT487 -> T823\nT488 -> T824", 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 -> T889\nX956 -> T889\nX957 -> T894\nX958 -> T891\nX959 -> T895\nT2 -> tree(T894, T891, T895)\nX960 -> T896\nT3 -> tree(T894, T891, T896)\nT890 -> T894\nT892 -> T895\nT893 -> T896", 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\nT832 -> 0\nX909 -> T844\nT837 -> s(T844)\nT838 -> T845\nT839 -> T846", 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 -> T845\nT3 -> T846", 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 -> T857\nT832 -> s(T857)\nX924 -> T859\nT837 -> s(T859)\nT858 -> T859\nT838 -> T860\nT839 -> T861", 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:\nT449 -> T857\nT451 -> T859\nT452 -> T860\nT453 -> T861", 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\nT832 -> T874\nX939 -> T874\nX940 -> T879\nX941 -> T876\nX942 -> T880\nT2 -> tree(T879, T876, T880)\nX943 -> T881\nT3 -> tree(T879, T876, T881)\nT875 -> T879\nT877 -> T880\nT878 -> T881", 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:\nT486 -> T879\nT481 -> T874\nT487 -> T880\nT488 -> T881", 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\nT894 -> 0\nX970 -> T901\nT889 -> s(T901)\nT895 -> T902\nT896 -> T903", 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 -> T914\nT894 -> s(T914)\nX981 -> T913\nT889 -> s(T913)\nT912 -> T914\nT895 -> T915\nT896 -> T916", 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(T901)\nT2 -> T902\nT3 -> T903", fontsize=14, style = filled, fillcolor = lightgrey];
208 -> 456 [arrowhead = none , style=dashed];
456 -> 1[style=dashed];

457 [label="INSTANCE with matching:\nT506 -> T914\nT505 -> T913\nT507 -> T915\nT508 -> T916", fontsize=14, style = filled, fillcolor = lightgrey];
210 -> 457 [arrowhead = none , style=dashed];
457 -> 123[style=dashed];

}

(2) Obligation:

Triples:

delmin19(tree(T94, T100, T96), T101, tree(T94, T102, T99)) :- delmin19(T100, T101, T102).
less34(s(T150), s(T152)) :- less34(T150, T152).
less46(s(T194), s(T193)) :- less46(T194, T193).
p44(T174, T169, T175, T176) :- less46(T174, T169).
p44(T174, T169, T179, T180) :- ','(lessc46(T174, T169), delete1(T169, T179, T180)).
p32(T127, T132, T133, T134) :- less34(T127, T132).
p32(T127, T132, T137, T138) :- ','(lessc34(T127, T132), delete1(T127, T137, T138)).
p72(0, s(T283), T284, T285) :- delete1(s(T283), T284, T285).
p72(s(T296), s(T295), T297, T298) :- p79(T296, T295, T297, T298).
p65(T231, T233, T234, T235) :- less34(T231, T233).
p65(T231, T233, T238, T239) :- ','(lessc34(T231, T233), delete1(s(T231), T238, T239)).
p79(T296, T295, T297, T298) :- less46(T296, T295).
p79(T296, T295, T301, T302) :- ','(lessc46(T296, T295), delete1(s(T295), T301, T302)).
p116(0, s(T493), T494, T495) :- delete1(s(T493), T494, T495).
p116(s(T506), s(T505), T507, T508) :- p79(T506, T505, T507, T508).
delete1(T17, tree(T17, T18, tree(T59, T65, T61)), tree(T66, T18, tree(T59, T67, T64))) :- delmin19(T65, T66, T67).
delete1(T127, tree(T132, T133, T130), tree(T132, T134, T130)) :- p32(T127, T132, T133, T134).
delete1(T169, tree(T174, T171, T175), tree(T174, T171, T176)) :- p44(T174, T169, T175, T176).
delete1(0, tree(s(T218), T219, T209), tree(s(T218), T220, T209)) :- delete1(0, T219, T220).
delete1(s(T231), tree(s(T233), T234, T209), tree(s(T233), T235, T209)) :- p65(T231, T233, T234, T235).
delete1(T256, tree(T261, T258, T262), tree(T261, T258, T263)) :- p44(T261, T256, T262, T263).
delete1(T271, tree(T276, T273, T277), tree(T276, T273, T278)) :- p72(T276, T271, T277, T278).
delete1(T314, tree(T314, T315, tree(T356, T362, T358)), tree(T363, T315, tree(T356, T364, T361))) :- delmin19(T362, T363, T364).
delete1(T389, tree(T394, T395, T392), tree(T394, T396, T392)) :- p32(T389, T394, T395, T396).
delete1(T409, tree(T414, T411, T415), tree(T414, T411, T416)) :- p72(T414, T409, T415, T416).
delete1(0, tree(s(T436), T437, T427), tree(s(T436), T438, T427)) :- delete1(0, T437, T438).
delete1(s(T449), tree(s(T451), T452, T427), tree(s(T451), T453, T427)) :- p65(T449, T451, T452, T453).
delete1(T466, tree(T471, T468, T472), tree(T471, T468, T473)) :- p72(T471, T466, T472, T473).
delete1(T481, tree(T486, T483, T487), tree(T486, T483, T488)) :- p116(T486, T481, T487, T488).
delete1(T520, tree(T520, T521, tree(T562, T568, T564)), tree(T569, T521, tree(T562, T570, T567))) :- delmin19(T568, T569, T570).
delete1(T595, tree(T600, T601, T598), tree(T600, T602, T598)) :- p32(T595, T600, T601, T602).
delete1(T615, tree(T620, T617, T621), tree(T620, T617, T622)) :- p116(T620, T615, T621, T622).
delete1(0, tree(s(T642), T643, T633), tree(s(T642), T644, T633)) :- delete1(0, T643, T644).
delete1(s(T655), tree(s(T657), T658, T633), tree(s(T657), T659, T633)) :- p65(T655, T657, T658, T659).
delete1(T672, tree(T677, T674, T678), tree(T677, T674, T679)) :- p116(T677, T672, T678, T679).
delete1(s(T699), tree(0, T689, T700), tree(0, T689, T701)) :- delete1(s(T699), T700, T701).
delete1(s(T711), tree(s(T712), T689, T713), tree(s(T712), T689, T714)) :- p79(T712, T711, T713, T714).
delete1(T722, tree(T722, T723, tree(T764, T770, T766)), tree(T771, T723, tree(T764, T772, T769))) :- delmin19(T770, T771, T772).
delete1(T797, tree(T802, T803, T800), tree(T802, T804, T800)) :- p32(T797, T802, T803, T804).
delete1(T817, tree(T822, T819, T823), tree(T822, T819, T824)) :- p116(T822, T817, T823, T824).
delete1(0, tree(s(T844), T845, T835), tree(s(T844), T846, T835)) :- delete1(0, T845, T846).
delete1(s(T857), tree(s(T859), T860, T835), tree(s(T859), T861, T835)) :- p65(T857, T859, T860, T861).
delete1(T874, tree(T879, T876, T880), tree(T879, T876, T881)) :- p116(T879, T874, T880, T881).
delete1(s(T901), tree(0, T891, T902), tree(0, T891, T903)) :- delete1(s(T901), T902, T903).
delete1(s(T913), tree(s(T914), T891, T915), tree(s(T914), T891, T916)) :- p79(T914, T913, T915, T916).

Clauses:

delminc19(tree(T80, void, T81), T80, T81).
delminc19(tree(T94, T100, T96), T101, tree(T94, T102, T99)) :- delminc19(T100, T101, T102).
deletec1(T6, tree(T6, void, T7), T7).
deletec1(T10, tree(T10, T11, void), T11).
deletec1(T17, tree(T17, T18, tree(T33, void, T34)), tree(T33, T18, T34)).
deletec1(T17, tree(T17, T18, tree(T59, T65, T61)), tree(T66, T18, tree(T59, T67, T64))) :- delminc19(T65, T66, T67).
deletec1(T127, tree(T132, T133, T130), tree(T132, T134, T130)) :- qc32(T127, T132, T133, T134).
deletec1(T169, tree(T174, T171, T175), tree(T174, T171, T176)) :- qc44(T174, T169, T175, T176).
deletec1(0, tree(s(T218), T219, T209), tree(s(T218), T220, T209)) :- deletec1(0, T219, T220).
deletec1(s(T231), tree(s(T233), T234, T209), tree(s(T233), T235, T209)) :- qc65(T231, T233, T234, T235).
deletec1(T256, tree(T261, T258, T262), tree(T261, T258, T263)) :- qc44(T261, T256, T262, T263).
deletec1(T271, tree(T276, T273, T277), tree(T276, T273, T278)) :- qc72(T276, T271, T277, T278).
deletec1(T314, tree(T314, T315, tree(T330, void, T331)), tree(T330, T315, T331)).
deletec1(T314, tree(T314, T315, tree(T356, T362, T358)), tree(T363, T315, tree(T356, T364, T361))) :- delminc19(T362, T363, T364).
deletec1(T389, tree(T394, T395, T392), tree(T394, T396, T392)) :- qc32(T389, T394, T395, T396).
deletec1(T409, tree(T414, T411, T415), tree(T414, T411, T416)) :- qc72(T414, T409, T415, T416).
deletec1(0, tree(s(T436), T437, T427), tree(s(T436), T438, T427)) :- deletec1(0, T437, T438).
deletec1(s(T449), tree(s(T451), T452, T427), tree(s(T451), T453, T427)) :- qc65(T449, T451, T452, T453).
deletec1(T466, tree(T471, T468, T472), tree(T471, T468, T473)) :- qc72(T471, T466, T472, T473).
deletec1(T481, tree(T486, T483, T487), tree(T486, T483, T488)) :- qc116(T486, T481, T487, T488).
deletec1(T513, tree(T513, T514, void), T514).
deletec1(T520, tree(T520, T521, tree(T536, void, T537)), tree(T536, T521, T537)).
deletec1(T520, tree(T520, T521, tree(T562, T568, T564)), tree(T569, T521, tree(T562, T570, T567))) :- delminc19(T568, T569, T570).
deletec1(T595, tree(T600, T601, T598), tree(T600, T602, T598)) :- qc32(T595, T600, T601, T602).
deletec1(T615, tree(T620, T617, T621), tree(T620, T617, T622)) :- qc116(T620, T615, T621, T622).
deletec1(0, tree(s(T642), T643, T633), tree(s(T642), T644, T633)) :- deletec1(0, T643, T644).
deletec1(s(T655), tree(s(T657), T658, T633), tree(s(T657), T659, T633)) :- qc65(T655, T657, T658, T659).
deletec1(T672, tree(T677, T674, T678), tree(T677, T674, T679)) :- qc116(T677, T672, T678, T679).
deletec1(s(T699), tree(0, T689, T700), tree(0, T689, T701)) :- deletec1(s(T699), T700, T701).
deletec1(s(T711), tree(s(T712), T689, T713), tree(s(T712), T689, T714)) :- qc79(T712, T711, T713, T714).
deletec1(T722, tree(T722, T723, tree(T738, void, T739)), tree(T738, T723, T739)).
deletec1(T722, tree(T722, T723, tree(T764, T770, T766)), tree(T771, T723, tree(T764, T772, T769))) :- delminc19(T770, T771, T772).
deletec1(T797, tree(T802, T803, T800), tree(T802, T804, T800)) :- qc32(T797, T802, T803, T804).
deletec1(T817, tree(T822, T819, T823), tree(T822, T819, T824)) :- qc116(T822, T817, T823, T824).
deletec1(0, tree(s(T844), T845, T835), tree(s(T844), T846, T835)) :- deletec1(0, T845, T846).
deletec1(s(T857), tree(s(T859), T860, T835), tree(s(T859), T861, T835)) :- qc65(T857, T859, T860, T861).
deletec1(T874, tree(T879, T876, T880), tree(T879, T876, T881)) :- qc116(T879, T874, T880, T881).
deletec1(s(T901), tree(0, T891, T902), tree(0, T891, T903)) :- deletec1(s(T901), T902, T903).
deletec1(s(T913), tree(s(T914), T891, T915), tree(s(T914), T891, T916)) :- qc79(T914, T913, T915, T916).
lessc34(0, s(T145)).
lessc34(s(T150), s(T152)) :- lessc34(T150, T152).
lessc46(0, s(T187)).
lessc46(s(T194), s(T193)) :- lessc46(T194, T193).
qc44(T174, T169, T179, T180) :- ','(lessc46(T174, T169), deletec1(T169, T179, T180)).
qc32(T127, T132, T137, T138) :- ','(lessc34(T127, T132), deletec1(T127, T137, T138)).
qc72(0, s(T283), T284, T285) :- deletec1(s(T283), T284, T285).
qc72(s(T296), s(T295), T297, T298) :- qc79(T296, T295, T297, T298).
qc65(T231, T233, T238, T239) :- ','(lessc34(T231, T233), deletec1(s(T231), T238, T239)).
qc79(T296, T295, T301, T302) :- ','(lessc46(T296, T295), deletec1(s(T295), T301, T302)).
qc116(0, s(T493), T494, T495) :- deletec1(s(T493), T494, T495).
qc116(s(T506), s(T505), T507, T508) :- qc79(T506, T505, T507, T508).

Afs:

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

(3) TriplesToPiDPProof (SOUND transformation)

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

DELETE1_IN_GAA(T17, tree(T17, T18, tree(T59, T65, T61)), tree(T66, T18, tree(T59, T67, T64))) → U20_GAA(T17, T18, T59, T65, T61, T66, T67, T64, delmin19_in_aaa(T65, T66, T67))
DELETE1_IN_GAA(T17, tree(T17, T18, tree(T59, T65, T61)), tree(T66, T18, tree(T59, T67, T64))) → DELMIN19_IN_AAA(T65, T66, T67)
DELMIN19_IN_AAA(tree(T94, T100, T96), T101, tree(T94, T102, T99)) → U1_AAA(T94, T100, T96, T101, T102, T99, delmin19_in_aaa(T100, T101, T102))
DELMIN19_IN_AAA(tree(T94, T100, T96), T101, tree(T94, T102, T99)) → DELMIN19_IN_AAA(T100, T101, T102)
DELETE1_IN_GAA(T127, tree(T132, T133, T130), tree(T132, T134, T130)) → U21_GAA(T127, T132, T133, T130, T134, p32_in_gaaa(T127, T132, T133, T134))
DELETE1_IN_GAA(T127, tree(T132, T133, T130), tree(T132, T134, T130)) → P32_IN_GAAA(T127, T132, T133, T134)
P32_IN_GAAA(T127, T132, T133, T134) → U7_GAAA(T127, T132, T133, T134, less34_in_ga(T127, T132))
P32_IN_GAAA(T127, T132, T133, T134) → LESS34_IN_GA(T127, T132)
LESS34_IN_GA(s(T150), s(T152)) → U2_GA(T150, T152, less34_in_ga(T150, T152))
LESS34_IN_GA(s(T150), s(T152)) → LESS34_IN_GA(T150, T152)
P32_IN_GAAA(T127, T132, T137, T138) → U8_GAAA(T127, T132, T137, T138, lessc34_in_ga(T127, T132))
U8_GAAA(T127, T132, T137, T138, lessc34_out_ga(T127, T132)) → U9_GAAA(T127, T132, T137, T138, delete1_in_gaa(T127, T137, T138))
U8_GAAA(T127, T132, T137, T138, lessc34_out_ga(T127, T132)) → DELETE1_IN_GAA(T127, T137, T138)
DELETE1_IN_GAA(T169, tree(T174, T171, T175), tree(T174, T171, T176)) → U22_GAA(T169, T174, T171, T175, T176, p44_in_agaa(T174, T169, T175, T176))
DELETE1_IN_GAA(T169, tree(T174, T171, T175), tree(T174, T171, T176)) → P44_IN_AGAA(T174, T169, T175, T176)
P44_IN_AGAA(T174, T169, T175, T176) → U4_AGAA(T174, T169, T175, T176, less46_in_ag(T174, T169))
P44_IN_AGAA(T174, T169, T175, T176) → LESS46_IN_AG(T174, T169)
LESS46_IN_AG(s(T194), s(T193)) → U3_AG(T194, T193, less46_in_ag(T194, T193))
LESS46_IN_AG(s(T194), s(T193)) → LESS46_IN_AG(T194, T193)
P44_IN_AGAA(T174, T169, T179, T180) → U5_AGAA(T174, T169, T179, T180, lessc46_in_ag(T174, T169))
U5_AGAA(T174, T169, T179, T180, lessc46_out_ag(T174, T169)) → U6_AGAA(T174, T169, T179, T180, delete1_in_gaa(T169, T179, T180))
U5_AGAA(T174, T169, T179, T180, lessc46_out_ag(T174, T169)) → DELETE1_IN_GAA(T169, T179, T180)
DELETE1_IN_GAA(0, tree(s(T218), T219, T209), tree(s(T218), T220, T209)) → U23_GAA(T218, T219, T209, T220, delete1_in_gaa(0, T219, T220))
DELETE1_IN_GAA(0, tree(s(T218), T219, T209), tree(s(T218), T220, T209)) → DELETE1_IN_GAA(0, T219, T220)
DELETE1_IN_GAA(s(T231), tree(s(T233), T234, T209), tree(s(T233), T235, T209)) → U24_GAA(T231, T233, T234, T209, T235, p65_in_gaaa(T231, T233, T234, T235))
DELETE1_IN_GAA(s(T231), tree(s(T233), T234, T209), tree(s(T233), T235, T209)) → P65_IN_GAAA(T231, T233, T234, T235)
P65_IN_GAAA(T231, T233, T234, T235) → U12_GAAA(T231, T233, T234, T235, less34_in_ga(T231, T233))
P65_IN_GAAA(T231, T233, T234, T235) → LESS34_IN_GA(T231, T233)
P65_IN_GAAA(T231, T233, T238, T239) → U13_GAAA(T231, T233, T238, T239, lessc34_in_ga(T231, T233))
U13_GAAA(T231, T233, T238, T239, lessc34_out_ga(T231, T233)) → U14_GAAA(T231, T233, T238, T239, delete1_in_gaa(s(T231), T238, T239))
U13_GAAA(T231, T233, T238, T239, lessc34_out_ga(T231, T233)) → DELETE1_IN_GAA(s(T231), T238, T239)
DELETE1_IN_GAA(T256, tree(T261, T258, T262), tree(T261, T258, T263)) → U25_GAA(T256, T261, T258, T262, T263, p44_in_agaa(T261, T256, T262, T263))
DELETE1_IN_GAA(T271, tree(T276, T273, T277), tree(T276, T273, T278)) → U26_GAA(T271, T276, T273, T277, T278, p72_in_agaa(T276, T271, T277, T278))
DELETE1_IN_GAA(T271, tree(T276, T273, T277), tree(T276, T273, T278)) → P72_IN_AGAA(T276, T271, T277, T278)
P72_IN_AGAA(0, s(T283), T284, T285) → U10_AGAA(T283, T284, T285, delete1_in_gaa(s(T283), T284, T285))
P72_IN_AGAA(0, s(T283), T284, T285) → DELETE1_IN_GAA(s(T283), T284, T285)
DELETE1_IN_GAA(T314, tree(T314, T315, tree(T356, T362, T358)), tree(T363, T315, tree(T356, T364, T361))) → U27_GAA(T314, T315, T356, T362, T358, T363, T364, T361, delmin19_in_aaa(T362, T363, T364))
DELETE1_IN_GAA(T389, tree(T394, T395, T392), tree(T394, T396, T392)) → U28_GAA(T389, T394, T395, T392, T396, p32_in_gaaa(T389, T394, T395, T396))
DELETE1_IN_GAA(T409, tree(T414, T411, T415), tree(T414, T411, T416)) → U29_GAA(T409, T414, T411, T415, T416, p72_in_agaa(T414, T409, T415, T416))
P72_IN_AGAA(s(T296), s(T295), T297, T298) → U11_AGAA(T296, T295, T297, T298, p79_in_agaa(T296, T295, T297, T298))
P72_IN_AGAA(s(T296), s(T295), T297, T298) → P79_IN_AGAA(T296, T295, T297, T298)
P79_IN_AGAA(T296, T295, T297, T298) → U15_AGAA(T296, T295, T297, T298, less46_in_ag(T296, T295))
P79_IN_AGAA(T296, T295, T297, T298) → LESS46_IN_AG(T296, T295)
P79_IN_AGAA(T296, T295, T301, T302) → U16_AGAA(T296, T295, T301, T302, lessc46_in_ag(T296, T295))
U16_AGAA(T296, T295, T301, T302, lessc46_out_ag(T296, T295)) → U17_AGAA(T296, T295, T301, T302, delete1_in_gaa(s(T295), T301, T302))
U16_AGAA(T296, T295, T301, T302, lessc46_out_ag(T296, T295)) → DELETE1_IN_GAA(s(T295), T301, T302)
DELETE1_IN_GAA(0, tree(s(T436), T437, T427), tree(s(T436), T438, T427)) → U30_GAA(T436, T437, T427, T438, delete1_in_gaa(0, T437, T438))
DELETE1_IN_GAA(s(T449), tree(s(T451), T452, T427), tree(s(T451), T453, T427)) → U31_GAA(T449, T451, T452, T427, T453, p65_in_gaaa(T449, T451, T452, T453))
DELETE1_IN_GAA(T466, tree(T471, T468, T472), tree(T471, T468, T473)) → U32_GAA(T466, T471, T468, T472, T473, p72_in_agaa(T471, T466, T472, T473))
DELETE1_IN_GAA(T481, tree(T486, T483, T487), tree(T486, T483, T488)) → U33_GAA(T481, T486, T483, T487, T488, p116_in_agaa(T486, T481, T487, T488))
DELETE1_IN_GAA(T481, tree(T486, T483, T487), tree(T486, T483, T488)) → P116_IN_AGAA(T486, T481, T487, T488)
P116_IN_AGAA(0, s(T493), T494, T495) → U18_AGAA(T493, T494, T495, delete1_in_gaa(s(T493), T494, T495))
P116_IN_AGAA(0, s(T493), T494, T495) → DELETE1_IN_GAA(s(T493), T494, T495)
DELETE1_IN_GAA(T520, tree(T520, T521, tree(T562, T568, T564)), tree(T569, T521, tree(T562, T570, T567))) → U34_GAA(T520, T521, T562, T568, T564, T569, T570, T567, delmin19_in_aaa(T568, T569, T570))
DELETE1_IN_GAA(T595, tree(T600, T601, T598), tree(T600, T602, T598)) → U35_GAA(T595, T600, T601, T598, T602, p32_in_gaaa(T595, T600, T601, T602))
DELETE1_IN_GAA(T615, tree(T620, T617, T621), tree(T620, T617, T622)) → U36_GAA(T615, T620, T617, T621, T622, p116_in_agaa(T620, T615, T621, T622))
P116_IN_AGAA(s(T506), s(T505), T507, T508) → U19_AGAA(T506, T505, T507, T508, p79_in_agaa(T506, T505, T507, T508))
P116_IN_AGAA(s(T506), s(T505), T507, T508) → P79_IN_AGAA(T506, T505, T507, T508)
DELETE1_IN_GAA(0, tree(s(T642), T643, T633), tree(s(T642), T644, T633)) → U37_GAA(T642, T643, T633, T644, delete1_in_gaa(0, T643, T644))
DELETE1_IN_GAA(s(T655), tree(s(T657), T658, T633), tree(s(T657), T659, T633)) → U38_GAA(T655, T657, T658, T633, T659, p65_in_gaaa(T655, T657, T658, T659))
DELETE1_IN_GAA(T672, tree(T677, T674, T678), tree(T677, T674, T679)) → U39_GAA(T672, T677, T674, T678, T679, p116_in_agaa(T677, T672, T678, T679))
DELETE1_IN_GAA(s(T699), tree(0, T689, T700), tree(0, T689, T701)) → U40_GAA(T699, T689, T700, T701, delete1_in_gaa(s(T699), T700, T701))
DELETE1_IN_GAA(s(T699), tree(0, T689, T700), tree(0, T689, T701)) → DELETE1_IN_GAA(s(T699), T700, T701)
DELETE1_IN_GAA(s(T711), tree(s(T712), T689, T713), tree(s(T712), T689, T714)) → U41_GAA(T711, T712, T689, T713, T714, p79_in_agaa(T712, T711, T713, T714))
DELETE1_IN_GAA(s(T711), tree(s(T712), T689, T713), tree(s(T712), T689, T714)) → P79_IN_AGAA(T712, T711, T713, T714)
DELETE1_IN_GAA(T722, tree(T722, T723, tree(T764, T770, T766)), tree(T771, T723, tree(T764, T772, T769))) → U42_GAA(T722, T723, T764, T770, T766, T771, T772, T769, delmin19_in_aaa(T770, T771, T772))
DELETE1_IN_GAA(T797, tree(T802, T803, T800), tree(T802, T804, T800)) → U43_GAA(T797, T802, T803, T800, T804, p32_in_gaaa(T797, T802, T803, T804))
DELETE1_IN_GAA(T817, tree(T822, T819, T823), tree(T822, T819, T824)) → U44_GAA(T817, T822, T819, T823, T824, p116_in_agaa(T822, T817, T823, T824))
DELETE1_IN_GAA(0, tree(s(T844), T845, T835), tree(s(T844), T846, T835)) → U45_GAA(T844, T845, T835, T846, delete1_in_gaa(0, T845, T846))
DELETE1_IN_GAA(s(T857), tree(s(T859), T860, T835), tree(s(T859), T861, T835)) → U46_GAA(T857, T859, T860, T835, T861, p65_in_gaaa(T857, T859, T860, T861))
DELETE1_IN_GAA(T874, tree(T879, T876, T880), tree(T879, T876, T881)) → U47_GAA(T874, T879, T876, T880, T881, p116_in_agaa(T879, T874, T880, T881))
DELETE1_IN_GAA(s(T901), tree(0, T891, T902), tree(0, T891, T903)) → U48_GAA(T901, T891, T902, T903, delete1_in_gaa(s(T901), T902, T903))
DELETE1_IN_GAA(s(T913), tree(s(T914), T891, T915), tree(s(T914), T891, T916)) → U49_GAA(T913, T914, T891, T915, T916, p79_in_agaa(T914, T913, T915, T916))

The TRS R consists of the following rules:

lessc34_in_ga(0, s(T145)) → lessc34_out_ga(0, s(T145))
lessc34_in_ga(s(T150), s(T152)) → U82_ga(T150, T152, lessc34_in_ga(T150, T152))
U82_ga(T150, T152, lessc34_out_ga(T150, T152)) → lessc34_out_ga(s(T150), s(T152))
lessc46_in_ag(0, s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T194), s(T193)) → U83_ag(T194, T193, lessc46_in_ag(T194, T193))
U83_ag(T194, T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The argument filtering Pi contains the following mapping:
delete1_in_gaa(x1, x2, x3) = delete1_in_gaa(x1)
delmin19_in_aaa(x1, x2, x3) = delmin19_in_aaa
p32_in_gaaa(x1, x2, x3, x4) = p32_in_gaaa(x1)
less34_in_ga(x1, x2) = less34_in_ga(x1)
s(x1) = s(x1)
lessc34_in_ga(x1, x2) = lessc34_in_ga(x1)
0 = 0
lessc34_out_ga(x1, x2) = lessc34_out_ga(x1)
U82_ga(x1, x2, x3) = U82_ga(x1, x3)
p44_in_agaa(x1, x2, x3, x4) = p44_in_agaa(x2)
less46_in_ag(x1, x2) = less46_in_ag(x2)
lessc46_in_ag(x1, x2) = lessc46_in_ag(x2)
lessc46_out_ag(x1, x2) = lessc46_out_ag(x1, x2)
U83_ag(x1, x2, x3) = U83_ag(x2, x3)
p65_in_gaaa(x1, x2, x3, x4) = p65_in_gaaa(x1)
p72_in_agaa(x1, x2, x3, x4) = p72_in_agaa(x2)
p79_in_agaa(x1, x2, x3, x4) = p79_in_agaa(x2)
p116_in_agaa(x1, x2, x3, x4) = p116_in_agaa(x2)
DELETE1_IN_GAA(x1, x2, x3) = DELETE1_IN_GAA(x1)
U20_GAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U20_GAA(x1, x9)
DELMIN19_IN_AAA(x1, x2, x3) = DELMIN19_IN_AAA
U1_AAA(x1, x2, x3, x4, x5, x6, x7) = U1_AAA(x7)
U21_GAA(x1, x2, x3, x4, x5, x6) = U21_GAA(x1, x6)
P32_IN_GAAA(x1, x2, x3, x4) = P32_IN_GAAA(x1)
U7_GAAA(x1, x2, x3, x4, x5) = U7_GAAA(x1, x5)
LESS34_IN_GA(x1, x2) = LESS34_IN_GA(x1)
U2_GA(x1, x2, x3) = U2_GA(x1, x3)
U8_GAAA(x1, x2, x3, x4, x5) = U8_GAAA(x1, x5)
U9_GAAA(x1, x2, x3, x4, x5) = U9_GAAA(x1, x5)
U22_GAA(x1, x2, x3, x4, x5, x6) = U22_GAA(x1, x6)
P44_IN_AGAA(x1, x2, x3, x4) = P44_IN_AGAA(x2)
U4_AGAA(x1, x2, x3, x4, x5) = U4_AGAA(x2, x5)
LESS46_IN_AG(x1, x2) = LESS46_IN_AG(x2)
U3_AG(x1, x2, x3) = U3_AG(x2, x3)
U5_AGAA(x1, x2, x3, x4, x5) = U5_AGAA(x2, x5)
U6_AGAA(x1, x2, x3, x4, x5) = U6_AGAA(x1, x2, x5)
U23_GAA(x1, x2, x3, x4, x5) = U23_GAA(x5)
U24_GAA(x1, x2, x3, x4, x5, x6) = U24_GAA(x1, x6)
P65_IN_GAAA(x1, x2, x3, x4) = P65_IN_GAAA(x1)
U12_GAAA(x1, x2, x3, x4, x5) = U12_GAAA(x1, x5)
U13_GAAA(x1, x2, x3, x4, x5) = U13_GAAA(x1, x5)
U14_GAAA(x1, x2, x3, x4, x5) = U14_GAAA(x1, x5)
U25_GAA(x1, x2, x3, x4, x5, x6) = U25_GAA(x1, x6)
U26_GAA(x1, x2, x3, x4, x5, x6) = U26_GAA(x1, x6)
P72_IN_AGAA(x1, x2, x3, x4) = P72_IN_AGAA(x2)
U10_AGAA(x1, x2, x3, x4) = U10_AGAA(x1, x4)
U27_GAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U27_GAA(x1, x9)
U28_GAA(x1, x2, x3, x4, x5, x6) = U28_GAA(x1, x6)
U29_GAA(x1, x2, x3, x4, x5, x6) = U29_GAA(x1, x6)
U11_AGAA(x1, x2, x3, x4, x5) = U11_AGAA(x2, x5)
P79_IN_AGAA(x1, x2, x3, x4) = P79_IN_AGAA(x2)
U15_AGAA(x1, x2, x3, x4, x5) = U15_AGAA(x2, x5)
U16_AGAA(x1, x2, x3, x4, x5) = U16_AGAA(x2, x5)
U17_AGAA(x1, x2, x3, x4, x5) = U17_AGAA(x1, x2, x5)
U30_GAA(x1, x2, x3, x4, x5) = U30_GAA(x5)
U31_GAA(x1, x2, x3, x4, x5, x6) = U31_GAA(x1, x6)
U32_GAA(x1, x2, x3, x4, x5, x6) = U32_GAA(x1, x6)
U33_GAA(x1, x2, x3, x4, x5, x6) = U33_GAA(x1, x6)
P116_IN_AGAA(x1, x2, x3, x4) = P116_IN_AGAA(x2)
U18_AGAA(x1, x2, x3, x4) = U18_AGAA(x1, x4)
U34_GAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U34_GAA(x1, x9)
U35_GAA(x1, x2, x3, x4, x5, x6) = U35_GAA(x1, x6)
U36_GAA(x1, x2, x3, x4, x5, x6) = U36_GAA(x1, x6)
U19_AGAA(x1, x2, x3, x4, x5) = U19_AGAA(x2, x5)
U37_GAA(x1, x2, x3, x4, x5) = U37_GAA(x5)
U38_GAA(x1, x2, x3, x4, x5, x6) = U38_GAA(x1, x6)
U39_GAA(x1, x2, x3, x4, x5, x6) = U39_GAA(x1, x6)
U40_GAA(x1, x2, x3, x4, x5) = U40_GAA(x1, x5)
U41_GAA(x1, x2, x3, x4, x5, x6) = U41_GAA(x1, x6)
U42_GAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U42_GAA(x1, x9)
U43_GAA(x1, x2, x3, x4, x5, x6) = U43_GAA(x1, x6)
U44_GAA(x1, x2, x3, x4, x5, x6) = U44_GAA(x1, x6)
U45_GAA(x1, x2, x3, x4, x5) = U45_GAA(x5)
U46_GAA(x1, x2, x3, x4, x5, x6) = U46_GAA(x1, x6)
U47_GAA(x1, x2, x3, x4, x5, x6) = U47_GAA(x1, x6)
U48_GAA(x1, x2, x3, x4, x5) = U48_GAA(x1, x5)
U49_GAA(x1, x2, x3, x4, x5, x6) = U49_GAA(x1, 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_GAA(T17, tree(T17, T18, tree(T59, T65, T61)), tree(T66, T18, tree(T59, T67, T64))) → U20_GAA(T17, T18, T59, T65, T61, T66, T67, T64, delmin19_in_aaa(T65, T66, T67))
DELETE1_IN_GAA(T17, tree(T17, T18, tree(T59, T65, T61)), tree(T66, T18, tree(T59, T67, T64))) → DELMIN19_IN_AAA(T65, T66, T67)
DELMIN19_IN_AAA(tree(T94, T100, T96), T101, tree(T94, T102, T99)) → U1_AAA(T94, T100, T96, T101, T102, T99, delmin19_in_aaa(T100, T101, T102))
DELMIN19_IN_AAA(tree(T94, T100, T96), T101, tree(T94, T102, T99)) → DELMIN19_IN_AAA(T100, T101, T102)
DELETE1_IN_GAA(T127, tree(T132, T133, T130), tree(T132, T134, T130)) → U21_GAA(T127, T132, T133, T130, T134, p32_in_gaaa(T127, T132, T133, T134))
DELETE1_IN_GAA(T127, tree(T132, T133, T130), tree(T132, T134, T130)) → P32_IN_GAAA(T127, T132, T133, T134)
P32_IN_GAAA(T127, T132, T133, T134) → U7_GAAA(T127, T132, T133, T134, less34_in_ga(T127, T132))
P32_IN_GAAA(T127, T132, T133, T134) → LESS34_IN_GA(T127, T132)
LESS34_IN_GA(s(T150), s(T152)) → U2_GA(T150, T152, less34_in_ga(T150, T152))
LESS34_IN_GA(s(T150), s(T152)) → LESS34_IN_GA(T150, T152)
P32_IN_GAAA(T127, T132, T137, T138) → U8_GAAA(T127, T132, T137, T138, lessc34_in_ga(T127, T132))
U8_GAAA(T127, T132, T137, T138, lessc34_out_ga(T127, T132)) → U9_GAAA(T127, T132, T137, T138, delete1_in_gaa(T127, T137, T138))
U8_GAAA(T127, T132, T137, T138, lessc34_out_ga(T127, T132)) → DELETE1_IN_GAA(T127, T137, T138)
DELETE1_IN_GAA(T169, tree(T174, T171, T175), tree(T174, T171, T176)) → U22_GAA(T169, T174, T171, T175, T176, p44_in_agaa(T174, T169, T175, T176))
DELETE1_IN_GAA(T169, tree(T174, T171, T175), tree(T174, T171, T176)) → P44_IN_AGAA(T174, T169, T175, T176)
P44_IN_AGAA(T174, T169, T175, T176) → U4_AGAA(T174, T169, T175, T176, less46_in_ag(T174, T169))
P44_IN_AGAA(T174, T169, T175, T176) → LESS46_IN_AG(T174, T169)
LESS46_IN_AG(s(T194), s(T193)) → U3_AG(T194, T193, less46_in_ag(T194, T193))
LESS46_IN_AG(s(T194), s(T193)) → LESS46_IN_AG(T194, T193)
P44_IN_AGAA(T174, T169, T179, T180) → U5_AGAA(T174, T169, T179, T180, lessc46_in_ag(T174, T169))
U5_AGAA(T174, T169, T179, T180, lessc46_out_ag(T174, T169)) → U6_AGAA(T174, T169, T179, T180, delete1_in_gaa(T169, T179, T180))
U5_AGAA(T174, T169, T179, T180, lessc46_out_ag(T174, T169)) → DELETE1_IN_GAA(T169, T179, T180)
DELETE1_IN_GAA(0, tree(s(T218), T219, T209), tree(s(T218), T220, T209)) → U23_GAA(T218, T219, T209, T220, delete1_in_gaa(0, T219, T220))
DELETE1_IN_GAA(0, tree(s(T218), T219, T209), tree(s(T218), T220, T209)) → DELETE1_IN_GAA(0, T219, T220)
DELETE1_IN_GAA(s(T231), tree(s(T233), T234, T209), tree(s(T233), T235, T209)) → U24_GAA(T231, T233, T234, T209, T235, p65_in_gaaa(T231, T233, T234, T235))
DELETE1_IN_GAA(s(T231), tree(s(T233), T234, T209), tree(s(T233), T235, T209)) → P65_IN_GAAA(T231, T233, T234, T235)
P65_IN_GAAA(T231, T233, T234, T235) → U12_GAAA(T231, T233, T234, T235, less34_in_ga(T231, T233))
P65_IN_GAAA(T231, T233, T234, T235) → LESS34_IN_GA(T231, T233)
P65_IN_GAAA(T231, T233, T238, T239) → U13_GAAA(T231, T233, T238, T239, lessc34_in_ga(T231, T233))
U13_GAAA(T231, T233, T238, T239, lessc34_out_ga(T231, T233)) → U14_GAAA(T231, T233, T238, T239, delete1_in_gaa(s(T231), T238, T239))
U13_GAAA(T231, T233, T238, T239, lessc34_out_ga(T231, T233)) → DELETE1_IN_GAA(s(T231), T238, T239)
DELETE1_IN_GAA(T256, tree(T261, T258, T262), tree(T261, T258, T263)) → U25_GAA(T256, T261, T258, T262, T263, p44_in_agaa(T261, T256, T262, T263))
DELETE1_IN_GAA(T271, tree(T276, T273, T277), tree(T276, T273, T278)) → U26_GAA(T271, T276, T273, T277, T278, p72_in_agaa(T276, T271, T277, T278))
DELETE1_IN_GAA(T271, tree(T276, T273, T277), tree(T276, T273, T278)) → P72_IN_AGAA(T276, T271, T277, T278)
P72_IN_AGAA(0, s(T283), T284, T285) → U10_AGAA(T283, T284, T285, delete1_in_gaa(s(T283), T284, T285))
P72_IN_AGAA(0, s(T283), T284, T285) → DELETE1_IN_GAA(s(T283), T284, T285)
DELETE1_IN_GAA(T314, tree(T314, T315, tree(T356, T362, T358)), tree(T363, T315, tree(T356, T364, T361))) → U27_GAA(T314, T315, T356, T362, T358, T363, T364, T361, delmin19_in_aaa(T362, T363, T364))
DELETE1_IN_GAA(T389, tree(T394, T395, T392), tree(T394, T396, T392)) → U28_GAA(T389, T394, T395, T392, T396, p32_in_gaaa(T389, T394, T395, T396))
DELETE1_IN_GAA(T409, tree(T414, T411, T415), tree(T414, T411, T416)) → U29_GAA(T409, T414, T411, T415, T416, p72_in_agaa(T414, T409, T415, T416))
P72_IN_AGAA(s(T296), s(T295), T297, T298) → U11_AGAA(T296, T295, T297, T298, p79_in_agaa(T296, T295, T297, T298))
P72_IN_AGAA(s(T296), s(T295), T297, T298) → P79_IN_AGAA(T296, T295, T297, T298)
P79_IN_AGAA(T296, T295, T297, T298) → U15_AGAA(T296, T295, T297, T298, less46_in_ag(T296, T295))
P79_IN_AGAA(T296, T295, T297, T298) → LESS46_IN_AG(T296, T295)
P79_IN_AGAA(T296, T295, T301, T302) → U16_AGAA(T296, T295, T301, T302, lessc46_in_ag(T296, T295))
U16_AGAA(T296, T295, T301, T302, lessc46_out_ag(T296, T295)) → U17_AGAA(T296, T295, T301, T302, delete1_in_gaa(s(T295), T301, T302))
U16_AGAA(T296, T295, T301, T302, lessc46_out_ag(T296, T295)) → DELETE1_IN_GAA(s(T295), T301, T302)
DELETE1_IN_GAA(0, tree(s(T436), T437, T427), tree(s(T436), T438, T427)) → U30_GAA(T436, T437, T427, T438, delete1_in_gaa(0, T437, T438))
DELETE1_IN_GAA(s(T449), tree(s(T451), T452, T427), tree(s(T451), T453, T427)) → U31_GAA(T449, T451, T452, T427, T453, p65_in_gaaa(T449, T451, T452, T453))
DELETE1_IN_GAA(T466, tree(T471, T468, T472), tree(T471, T468, T473)) → U32_GAA(T466, T471, T468, T472, T473, p72_in_agaa(T471, T466, T472, T473))
DELETE1_IN_GAA(T481, tree(T486, T483, T487), tree(T486, T483, T488)) → U33_GAA(T481, T486, T483, T487, T488, p116_in_agaa(T486, T481, T487, T488))
DELETE1_IN_GAA(T481, tree(T486, T483, T487), tree(T486, T483, T488)) → P116_IN_AGAA(T486, T481, T487, T488)
P116_IN_AGAA(0, s(T493), T494, T495) → U18_AGAA(T493, T494, T495, delete1_in_gaa(s(T493), T494, T495))
P116_IN_AGAA(0, s(T493), T494, T495) → DELETE1_IN_GAA(s(T493), T494, T495)
DELETE1_IN_GAA(T520, tree(T520, T521, tree(T562, T568, T564)), tree(T569, T521, tree(T562, T570, T567))) → U34_GAA(T520, T521, T562, T568, T564, T569, T570, T567, delmin19_in_aaa(T568, T569, T570))
DELETE1_IN_GAA(T595, tree(T600, T601, T598), tree(T600, T602, T598)) → U35_GAA(T595, T600, T601, T598, T602, p32_in_gaaa(T595, T600, T601, T602))
DELETE1_IN_GAA(T615, tree(T620, T617, T621), tree(T620, T617, T622)) → U36_GAA(T615, T620, T617, T621, T622, p116_in_agaa(T620, T615, T621, T622))
P116_IN_AGAA(s(T506), s(T505), T507, T508) → U19_AGAA(T506, T505, T507, T508, p79_in_agaa(T506, T505, T507, T508))
P116_IN_AGAA(s(T506), s(T505), T507, T508) → P79_IN_AGAA(T506, T505, T507, T508)
DELETE1_IN_GAA(0, tree(s(T642), T643, T633), tree(s(T642), T644, T633)) → U37_GAA(T642, T643, T633, T644, delete1_in_gaa(0, T643, T644))
DELETE1_IN_GAA(s(T655), tree(s(T657), T658, T633), tree(s(T657), T659, T633)) → U38_GAA(T655, T657, T658, T633, T659, p65_in_gaaa(T655, T657, T658, T659))
DELETE1_IN_GAA(T672, tree(T677, T674, T678), tree(T677, T674, T679)) → U39_GAA(T672, T677, T674, T678, T679, p116_in_agaa(T677, T672, T678, T679))
DELETE1_IN_GAA(s(T699), tree(0, T689, T700), tree(0, T689, T701)) → U40_GAA(T699, T689, T700, T701, delete1_in_gaa(s(T699), T700, T701))
DELETE1_IN_GAA(s(T699), tree(0, T689, T700), tree(0, T689, T701)) → DELETE1_IN_GAA(s(T699), T700, T701)
DELETE1_IN_GAA(s(T711), tree(s(T712), T689, T713), tree(s(T712), T689, T714)) → U41_GAA(T711, T712, T689, T713, T714, p79_in_agaa(T712, T711, T713, T714))
DELETE1_IN_GAA(s(T711), tree(s(T712), T689, T713), tree(s(T712), T689, T714)) → P79_IN_AGAA(T712, T711, T713, T714)
DELETE1_IN_GAA(T722, tree(T722, T723, tree(T764, T770, T766)), tree(T771, T723, tree(T764, T772, T769))) → U42_GAA(T722, T723, T764, T770, T766, T771, T772, T769, delmin19_in_aaa(T770, T771, T772))
DELETE1_IN_GAA(T797, tree(T802, T803, T800), tree(T802, T804, T800)) → U43_GAA(T797, T802, T803, T800, T804, p32_in_gaaa(T797, T802, T803, T804))
DELETE1_IN_GAA(T817, tree(T822, T819, T823), tree(T822, T819, T824)) → U44_GAA(T817, T822, T819, T823, T824, p116_in_agaa(T822, T817, T823, T824))
DELETE1_IN_GAA(0, tree(s(T844), T845, T835), tree(s(T844), T846, T835)) → U45_GAA(T844, T845, T835, T846, delete1_in_gaa(0, T845, T846))
DELETE1_IN_GAA(s(T857), tree(s(T859), T860, T835), tree(s(T859), T861, T835)) → U46_GAA(T857, T859, T860, T835, T861, p65_in_gaaa(T857, T859, T860, T861))
DELETE1_IN_GAA(T874, tree(T879, T876, T880), tree(T879, T876, T881)) → U47_GAA(T874, T879, T876, T880, T881, p116_in_agaa(T879, T874, T880, T881))
DELETE1_IN_GAA(s(T901), tree(0, T891, T902), tree(0, T891, T903)) → U48_GAA(T901, T891, T902, T903, delete1_in_gaa(s(T901), T902, T903))
DELETE1_IN_GAA(s(T913), tree(s(T914), T891, T915), tree(s(T914), T891, T916)) → U49_GAA(T913, T914, T891, T915, T916, p79_in_agaa(T914, T913, T915, T916))

The TRS R consists of the following rules:

lessc34_in_ga(0, s(T145)) → lessc34_out_ga(0, s(T145))
lessc34_in_ga(s(T150), s(T152)) → U82_ga(T150, T152, lessc34_in_ga(T150, T152))
U82_ga(T150, T152, lessc34_out_ga(T150, T152)) → lessc34_out_ga(s(T150), s(T152))
lessc46_in_ag(0, s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T194), s(T193)) → U83_ag(T194, T193, lessc46_in_ag(T194, T193))
U83_ag(T194, T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 50 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

LESS46_IN_AG(s(T194), s(T193)) → LESS46_IN_AG(T194, T193)

The TRS R consists of the following rules:

lessc34_in_ga(0, s(T145)) → lessc34_out_ga(0, s(T145))
lessc34_in_ga(s(T150), s(T152)) → U82_ga(T150, T152, lessc34_in_ga(T150, T152))
U82_ga(T150, T152, lessc34_out_ga(T150, T152)) → lessc34_out_ga(s(T150), s(T152))
lessc46_in_ag(0, s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T194), s(T193)) → U83_ag(T194, T193, lessc46_in_ag(T194, T193))
U83_ag(T194, T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

(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_AG(s(T194), s(T193)) → LESS46_IN_AG(T194, T193)

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

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_AG(s(T193)) → LESS46_IN_AG(T193)

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

(13) YES

(14) Obligation:

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

LESS34_IN_GA(s(T150), s(T152)) → LESS34_IN_GA(T150, T152)

The TRS R consists of the following rules:

lessc34_in_ga(0, s(T145)) → lessc34_out_ga(0, s(T145))
lessc34_in_ga(s(T150), s(T152)) → U82_ga(T150, T152, lessc34_in_ga(T150, T152))
U82_ga(T150, T152, lessc34_out_ga(T150, T152)) → lessc34_out_ga(s(T150), s(T152))
lessc46_in_ag(0, s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T194), s(T193)) → U83_ag(T194, T193, lessc46_in_ag(T194, T193))
U83_ag(T194, T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

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

LESS34_IN_GA(s(T150), s(T152)) → LESS34_IN_GA(T150, T152)

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

LESS34_IN_GA(s(T150)) → LESS34_IN_GA(T150)

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:

LESS34_IN_GA(s(T150)) → LESS34_IN_GA(T150)
The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

DELMIN19_IN_AAA(tree(T94, T100, T96), T101, tree(T94, T102, T99)) → DELMIN19_IN_AAA(T100, T101, T102)

The TRS R consists of the following rules:

lessc34_in_ga(0, s(T145)) → lessc34_out_ga(0, s(T145))
lessc34_in_ga(s(T150), s(T152)) → U82_ga(T150, T152, lessc34_in_ga(T150, T152))
U82_ga(T150, T152, lessc34_out_ga(T150, T152)) → lessc34_out_ga(s(T150), s(T152))
lessc46_in_ag(0, s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T194), s(T193)) → U83_ag(T194, T193, lessc46_in_ag(T194, T193))
U83_ag(T194, T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

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

DELMIN19_IN_AAA(tree(T94, T100, T96), T101, tree(T94, T102, T99)) → DELMIN19_IN_AAA(T100, T101, T102)

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

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

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

DELMIN19_IN_AAA → DELMIN19_IN_AAA

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

(26) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = DELMIN19_IN_AAA evaluates to t =DELMIN19_IN_AAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Matcher: [ ]
Semiunifier: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from DELMIN19_IN_AAA to DELMIN19_IN_AAA.

(27) NO

(28) Obligation:

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

DELETE1_IN_GAA(T127, tree(T132, T133, T130), tree(T132, T134, T130)) → P32_IN_GAAA(T127, T132, T133, T134)
P32_IN_GAAA(T127, T132, T137, T138) → U8_GAAA(T127, T132, T137, T138, lessc34_in_ga(T127, T132))
U8_GAAA(T127, T132, T137, T138, lessc34_out_ga(T127, T132)) → DELETE1_IN_GAA(T127, T137, T138)
DELETE1_IN_GAA(T169, tree(T174, T171, T175), tree(T174, T171, T176)) → P44_IN_AGAA(T174, T169, T175, T176)
P44_IN_AGAA(T174, T169, T179, T180) → U5_AGAA(T174, T169, T179, T180, lessc46_in_ag(T174, T169))
U5_AGAA(T174, T169, T179, T180, lessc46_out_ag(T174, T169)) → DELETE1_IN_GAA(T169, T179, T180)
DELETE1_IN_GAA(0, tree(s(T218), T219, T209), tree(s(T218), T220, T209)) → DELETE1_IN_GAA(0, T219, T220)
DELETE1_IN_GAA(T271, tree(T276, T273, T277), tree(T276, T273, T278)) → P72_IN_AGAA(T276, T271, T277, T278)
P72_IN_AGAA(0, s(T283), T284, T285) → DELETE1_IN_GAA(s(T283), T284, T285)
DELETE1_IN_GAA(s(T231), tree(s(T233), T234, T209), tree(s(T233), T235, T209)) → P65_IN_GAAA(T231, T233, T234, T235)
P65_IN_GAAA(T231, T233, T238, T239) → U13_GAAA(T231, T233, T238, T239, lessc34_in_ga(T231, T233))
U13_GAAA(T231, T233, T238, T239, lessc34_out_ga(T231, T233)) → DELETE1_IN_GAA(s(T231), T238, T239)
DELETE1_IN_GAA(T481, tree(T486, T483, T487), tree(T486, T483, T488)) → P116_IN_AGAA(T486, T481, T487, T488)
P116_IN_AGAA(0, s(T493), T494, T495) → DELETE1_IN_GAA(s(T493), T494, T495)
DELETE1_IN_GAA(s(T699), tree(0, T689, T700), tree(0, T689, T701)) → DELETE1_IN_GAA(s(T699), T700, T701)
DELETE1_IN_GAA(s(T711), tree(s(T712), T689, T713), tree(s(T712), T689, T714)) → P79_IN_AGAA(T712, T711, T713, T714)
P79_IN_AGAA(T296, T295, T301, T302) → U16_AGAA(T296, T295, T301, T302, lessc46_in_ag(T296, T295))
U16_AGAA(T296, T295, T301, T302, lessc46_out_ag(T296, T295)) → DELETE1_IN_GAA(s(T295), T301, T302)
P116_IN_AGAA(s(T506), s(T505), T507, T508) → P79_IN_AGAA(T506, T505, T507, T508)
P72_IN_AGAA(s(T296), s(T295), T297, T298) → P79_IN_AGAA(T296, T295, T297, T298)

The TRS R consists of the following rules:

lessc34_in_ga(0, s(T145)) → lessc34_out_ga(0, s(T145))
lessc34_in_ga(s(T150), s(T152)) → U82_ga(T150, T152, lessc34_in_ga(T150, T152))
U82_ga(T150, T152, lessc34_out_ga(T150, T152)) → lessc34_out_ga(s(T150), s(T152))
lessc46_in_ag(0, s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T194), s(T193)) → U83_ag(T194, T193, lessc46_in_ag(T194, T193))
U83_ag(T194, T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
lessc34_in_ga(x1, x2) = lessc34_in_ga(x1)
0 = 0
lessc34_out_ga(x1, x2) = lessc34_out_ga(x1)
U82_ga(x1, x2, x3) = U82_ga(x1, x3)
lessc46_in_ag(x1, x2) = lessc46_in_ag(x2)
lessc46_out_ag(x1, x2) = lessc46_out_ag(x1, x2)
U83_ag(x1, x2, x3) = U83_ag(x2, x3)
DELETE1_IN_GAA(x1, x2, x3) = DELETE1_IN_GAA(x1)
P32_IN_GAAA(x1, x2, x3, x4) = P32_IN_GAAA(x1)
U8_GAAA(x1, x2, x3, x4, x5) = U8_GAAA(x1, x5)
P44_IN_AGAA(x1, x2, x3, x4) = P44_IN_AGAA(x2)
U5_AGAA(x1, x2, x3, x4, x5) = U5_AGAA(x2, x5)
P65_IN_GAAA(x1, x2, x3, x4) = P65_IN_GAAA(x1)
U13_GAAA(x1, x2, x3, x4, x5) = U13_GAAA(x1, x5)
P72_IN_AGAA(x1, x2, x3, x4) = P72_IN_AGAA(x2)
P79_IN_AGAA(x1, x2, x3, x4) = P79_IN_AGAA(x2)
U16_AGAA(x1, x2, x3, x4, x5) = U16_AGAA(x2, x5)
P116_IN_AGAA(x1, x2, x3, x4) = P116_IN_AGAA(x2)

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

(29) PiDPToQDPProof (SOUND transformation)

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

(30) Obligation:

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

DELETE1_IN_GAA(T127) → P32_IN_GAAA(T127)
P32_IN_GAAA(T127) → U8_GAAA(T127, lessc34_in_ga(T127))
U8_GAAA(T127, lessc34_out_ga(T127)) → DELETE1_IN_GAA(T127)
DELETE1_IN_GAA(T169) → P44_IN_AGAA(T169)
P44_IN_AGAA(T169) → U5_AGAA(T169, lessc46_in_ag(T169))
U5_AGAA(T169, lessc46_out_ag(T174, T169)) → DELETE1_IN_GAA(T169)
DELETE1_IN_GAA(0) → DELETE1_IN_GAA(0)
DELETE1_IN_GAA(T271) → P72_IN_AGAA(T271)
P72_IN_AGAA(s(T283)) → DELETE1_IN_GAA(s(T283))
DELETE1_IN_GAA(s(T231)) → P65_IN_GAAA(T231)
P65_IN_GAAA(T231) → U13_GAAA(T231, lessc34_in_ga(T231))
U13_GAAA(T231, lessc34_out_ga(T231)) → DELETE1_IN_GAA(s(T231))
DELETE1_IN_GAA(T481) → P116_IN_AGAA(T481)
P116_IN_AGAA(s(T493)) → DELETE1_IN_GAA(s(T493))
DELETE1_IN_GAA(s(T699)) → DELETE1_IN_GAA(s(T699))
DELETE1_IN_GAA(s(T711)) → P79_IN_AGAA(T711)
P79_IN_AGAA(T295) → U16_AGAA(T295, lessc46_in_ag(T295))
U16_AGAA(T295, lessc46_out_ag(T296, T295)) → DELETE1_IN_GAA(s(T295))
P116_IN_AGAA(s(T505)) → P79_IN_AGAA(T505)
P72_IN_AGAA(s(T295)) → P79_IN_AGAA(T295)

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(31) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P32_IN_GAAA(T127) → U8_GAAA(T127, lessc34_in_ga(T127)) at position [1] we obtained the following new rules [LPAR04]:

P32_IN_GAAA(0) → U8_GAAA(0, lessc34_out_ga(0))
P32_IN_GAAA(s(x0)) → U8_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))

(32) Obligation:

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

DELETE1_IN_GAA(T127) → P32_IN_GAAA(T127)
U8_GAAA(T127, lessc34_out_ga(T127)) → DELETE1_IN_GAA(T127)
DELETE1_IN_GAA(T169) → P44_IN_AGAA(T169)
P44_IN_AGAA(T169) → U5_AGAA(T169, lessc46_in_ag(T169))
U5_AGAA(T169, lessc46_out_ag(T174, T169)) → DELETE1_IN_GAA(T169)
DELETE1_IN_GAA(0) → DELETE1_IN_GAA(0)
DELETE1_IN_GAA(T271) → P72_IN_AGAA(T271)
P72_IN_AGAA(s(T283)) → DELETE1_IN_GAA(s(T283))
DELETE1_IN_GAA(s(T231)) → P65_IN_GAAA(T231)
P65_IN_GAAA(T231) → U13_GAAA(T231, lessc34_in_ga(T231))
U13_GAAA(T231, lessc34_out_ga(T231)) → DELETE1_IN_GAA(s(T231))
DELETE1_IN_GAA(T481) → P116_IN_AGAA(T481)
P116_IN_AGAA(s(T493)) → DELETE1_IN_GAA(s(T493))
DELETE1_IN_GAA(s(T699)) → DELETE1_IN_GAA(s(T699))
DELETE1_IN_GAA(s(T711)) → P79_IN_AGAA(T711)
P79_IN_AGAA(T295) → U16_AGAA(T295, lessc46_in_ag(T295))
U16_AGAA(T295, lessc46_out_ag(T296, T295)) → DELETE1_IN_GAA(s(T295))
P116_IN_AGAA(s(T505)) → P79_IN_AGAA(T505)
P72_IN_AGAA(s(T295)) → P79_IN_AGAA(T295)
P32_IN_GAAA(0) → U8_GAAA(0, lessc34_out_ga(0))
P32_IN_GAAA(s(x0)) → U8_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(33) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P44_IN_AGAA(T169) → U5_AGAA(T169, lessc46_in_ag(T169)) at position [1] we obtained the following new rules [LPAR04]:

P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))

(34) Obligation:

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

DELETE1_IN_GAA(T127) → P32_IN_GAAA(T127)
U8_GAAA(T127, lessc34_out_ga(T127)) → DELETE1_IN_GAA(T127)
DELETE1_IN_GAA(T169) → P44_IN_AGAA(T169)
U5_AGAA(T169, lessc46_out_ag(T174, T169)) → DELETE1_IN_GAA(T169)
DELETE1_IN_GAA(0) → DELETE1_IN_GAA(0)
DELETE1_IN_GAA(T271) → P72_IN_AGAA(T271)
P72_IN_AGAA(s(T283)) → DELETE1_IN_GAA(s(T283))
DELETE1_IN_GAA(s(T231)) → P65_IN_GAAA(T231)
P65_IN_GAAA(T231) → U13_GAAA(T231, lessc34_in_ga(T231))
U13_GAAA(T231, lessc34_out_ga(T231)) → DELETE1_IN_GAA(s(T231))
DELETE1_IN_GAA(T481) → P116_IN_AGAA(T481)
P116_IN_AGAA(s(T493)) → DELETE1_IN_GAA(s(T493))
DELETE1_IN_GAA(s(T699)) → DELETE1_IN_GAA(s(T699))
DELETE1_IN_GAA(s(T711)) → P79_IN_AGAA(T711)
P79_IN_AGAA(T295) → U16_AGAA(T295, lessc46_in_ag(T295))
U16_AGAA(T295, lessc46_out_ag(T296, T295)) → DELETE1_IN_GAA(s(T295))
P116_IN_AGAA(s(T505)) → P79_IN_AGAA(T505)
P72_IN_AGAA(s(T295)) → P79_IN_AGAA(T295)
P32_IN_GAAA(0) → U8_GAAA(0, lessc34_out_ga(0))
P32_IN_GAAA(s(x0)) → U8_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(35) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P65_IN_GAAA(T231) → U13_GAAA(T231, lessc34_in_ga(T231)) at position [1] we obtained the following new rules [LPAR04]:

P65_IN_GAAA(0) → U13_GAAA(0, lessc34_out_ga(0))
P65_IN_GAAA(s(x0)) → U13_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))

(36) Obligation:

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

DELETE1_IN_GAA(T127) → P32_IN_GAAA(T127)
U8_GAAA(T127, lessc34_out_ga(T127)) → DELETE1_IN_GAA(T127)
DELETE1_IN_GAA(T169) → P44_IN_AGAA(T169)
U5_AGAA(T169, lessc46_out_ag(T174, T169)) → DELETE1_IN_GAA(T169)
DELETE1_IN_GAA(0) → DELETE1_IN_GAA(0)
DELETE1_IN_GAA(T271) → P72_IN_AGAA(T271)
P72_IN_AGAA(s(T283)) → DELETE1_IN_GAA(s(T283))
DELETE1_IN_GAA(s(T231)) → P65_IN_GAAA(T231)
U13_GAAA(T231, lessc34_out_ga(T231)) → DELETE1_IN_GAA(s(T231))
DELETE1_IN_GAA(T481) → P116_IN_AGAA(T481)
P116_IN_AGAA(s(T493)) → DELETE1_IN_GAA(s(T493))
DELETE1_IN_GAA(s(T699)) → DELETE1_IN_GAA(s(T699))
DELETE1_IN_GAA(s(T711)) → P79_IN_AGAA(T711)
P79_IN_AGAA(T295) → U16_AGAA(T295, lessc46_in_ag(T295))
U16_AGAA(T295, lessc46_out_ag(T296, T295)) → DELETE1_IN_GAA(s(T295))
P116_IN_AGAA(s(T505)) → P79_IN_AGAA(T505)
P72_IN_AGAA(s(T295)) → P79_IN_AGAA(T295)
P32_IN_GAAA(0) → U8_GAAA(0, lessc34_out_ga(0))
P32_IN_GAAA(s(x0)) → U8_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
P65_IN_GAAA(0) → U13_GAAA(0, lessc34_out_ga(0))
P65_IN_GAAA(s(x0)) → U13_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(37) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P79_IN_AGAA(T295) → U16_AGAA(T295, lessc46_in_ag(T295)) at position [1] we obtained the following new rules [LPAR04]:

P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))

(38) Obligation:

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

DELETE1_IN_GAA(T127) → P32_IN_GAAA(T127)
U8_GAAA(T127, lessc34_out_ga(T127)) → DELETE1_IN_GAA(T127)
DELETE1_IN_GAA(T169) → P44_IN_AGAA(T169)
U5_AGAA(T169, lessc46_out_ag(T174, T169)) → DELETE1_IN_GAA(T169)
DELETE1_IN_GAA(0) → DELETE1_IN_GAA(0)
DELETE1_IN_GAA(T271) → P72_IN_AGAA(T271)
P72_IN_AGAA(s(T283)) → DELETE1_IN_GAA(s(T283))
DELETE1_IN_GAA(s(T231)) → P65_IN_GAAA(T231)
U13_GAAA(T231, lessc34_out_ga(T231)) → DELETE1_IN_GAA(s(T231))
DELETE1_IN_GAA(T481) → P116_IN_AGAA(T481)
P116_IN_AGAA(s(T493)) → DELETE1_IN_GAA(s(T493))
DELETE1_IN_GAA(s(T699)) → DELETE1_IN_GAA(s(T699))
DELETE1_IN_GAA(s(T711)) → P79_IN_AGAA(T711)
U16_AGAA(T295, lessc46_out_ag(T296, T295)) → DELETE1_IN_GAA(s(T295))
P116_IN_AGAA(s(T505)) → P79_IN_AGAA(T505)
P72_IN_AGAA(s(T295)) → P79_IN_AGAA(T295)
P32_IN_GAAA(0) → U8_GAAA(0, lessc34_out_ga(0))
P32_IN_GAAA(s(x0)) → U8_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
P65_IN_GAAA(0) → U13_GAAA(0, lessc34_out_ga(0))
P65_IN_GAAA(s(x0)) → U13_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(39) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U8_GAAA(T127, lessc34_out_ga(T127)) → DELETE1_IN_GAA(T127) we obtained the following new rules [LPAR04]:

U8_GAAA(0, lessc34_out_ga(0)) → DELETE1_IN_GAA(0)
U8_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(z0))

(40) Obligation:

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

DELETE1_IN_GAA(T127) → P32_IN_GAAA(T127)
DELETE1_IN_GAA(T169) → P44_IN_AGAA(T169)
U5_AGAA(T169, lessc46_out_ag(T174, T169)) → DELETE1_IN_GAA(T169)
DELETE1_IN_GAA(0) → DELETE1_IN_GAA(0)
DELETE1_IN_GAA(T271) → P72_IN_AGAA(T271)
P72_IN_AGAA(s(T283)) → DELETE1_IN_GAA(s(T283))
DELETE1_IN_GAA(s(T231)) → P65_IN_GAAA(T231)
U13_GAAA(T231, lessc34_out_ga(T231)) → DELETE1_IN_GAA(s(T231))
DELETE1_IN_GAA(T481) → P116_IN_AGAA(T481)
P116_IN_AGAA(s(T493)) → DELETE1_IN_GAA(s(T493))
DELETE1_IN_GAA(s(T699)) → DELETE1_IN_GAA(s(T699))
DELETE1_IN_GAA(s(T711)) → P79_IN_AGAA(T711)
U16_AGAA(T295, lessc46_out_ag(T296, T295)) → DELETE1_IN_GAA(s(T295))
P116_IN_AGAA(s(T505)) → P79_IN_AGAA(T505)
P72_IN_AGAA(s(T295)) → P79_IN_AGAA(T295)
P32_IN_GAAA(0) → U8_GAAA(0, lessc34_out_ga(0))
P32_IN_GAAA(s(x0)) → U8_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
P65_IN_GAAA(0) → U13_GAAA(0, lessc34_out_ga(0))
P65_IN_GAAA(s(x0)) → U13_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
U8_GAAA(0, lessc34_out_ga(0)) → DELETE1_IN_GAA(0)
U8_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(z0))

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(41) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U5_AGAA(T169, lessc46_out_ag(T174, T169)) → DELETE1_IN_GAA(T169) we obtained the following new rules [LPAR04]:

U5_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(z0))
U5_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(z0))

(42) Obligation:

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

DELETE1_IN_GAA(T127) → P32_IN_GAAA(T127)
DELETE1_IN_GAA(T169) → P44_IN_AGAA(T169)
DELETE1_IN_GAA(0) → DELETE1_IN_GAA(0)
DELETE1_IN_GAA(T271) → P72_IN_AGAA(T271)
P72_IN_AGAA(s(T283)) → DELETE1_IN_GAA(s(T283))
DELETE1_IN_GAA(s(T231)) → P65_IN_GAAA(T231)
U13_GAAA(T231, lessc34_out_ga(T231)) → DELETE1_IN_GAA(s(T231))
DELETE1_IN_GAA(T481) → P116_IN_AGAA(T481)
P116_IN_AGAA(s(T493)) → DELETE1_IN_GAA(s(T493))
DELETE1_IN_GAA(s(T699)) → DELETE1_IN_GAA(s(T699))
DELETE1_IN_GAA(s(T711)) → P79_IN_AGAA(T711)
U16_AGAA(T295, lessc46_out_ag(T296, T295)) → DELETE1_IN_GAA(s(T295))
P116_IN_AGAA(s(T505)) → P79_IN_AGAA(T505)
P72_IN_AGAA(s(T295)) → P79_IN_AGAA(T295)
P32_IN_GAAA(0) → U8_GAAA(0, lessc34_out_ga(0))
P32_IN_GAAA(s(x0)) → U8_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
P65_IN_GAAA(0) → U13_GAAA(0, lessc34_out_ga(0))
P65_IN_GAAA(s(x0)) → U13_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
U8_GAAA(0, lessc34_out_ga(0)) → DELETE1_IN_GAA(0)
U8_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(z0))
U5_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(z0))
U5_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(z0))

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(43) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule DELETE1_IN_GAA(T127) → P32_IN_GAAA(T127) we obtained the following new rules [LPAR04]:

DELETE1_IN_GAA(0) → P32_IN_GAAA(0)
DELETE1_IN_GAA(s(z0)) → P32_IN_GAAA(s(z0))

(44) Obligation:

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

DELETE1_IN_GAA(T169) → P44_IN_AGAA(T169)
DELETE1_IN_GAA(0) → DELETE1_IN_GAA(0)
DELETE1_IN_GAA(T271) → P72_IN_AGAA(T271)
P72_IN_AGAA(s(T283)) → DELETE1_IN_GAA(s(T283))
DELETE1_IN_GAA(s(T231)) → P65_IN_GAAA(T231)
U13_GAAA(T231, lessc34_out_ga(T231)) → DELETE1_IN_GAA(s(T231))
DELETE1_IN_GAA(T481) → P116_IN_AGAA(T481)
P116_IN_AGAA(s(T493)) → DELETE1_IN_GAA(s(T493))
DELETE1_IN_GAA(s(T699)) → DELETE1_IN_GAA(s(T699))
DELETE1_IN_GAA(s(T711)) → P79_IN_AGAA(T711)
U16_AGAA(T295, lessc46_out_ag(T296, T295)) → DELETE1_IN_GAA(s(T295))
P116_IN_AGAA(s(T505)) → P79_IN_AGAA(T505)
P72_IN_AGAA(s(T295)) → P79_IN_AGAA(T295)
P32_IN_GAAA(0) → U8_GAAA(0, lessc34_out_ga(0))
P32_IN_GAAA(s(x0)) → U8_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
P65_IN_GAAA(0) → U13_GAAA(0, lessc34_out_ga(0))
P65_IN_GAAA(s(x0)) → U13_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
U8_GAAA(0, lessc34_out_ga(0)) → DELETE1_IN_GAA(0)
U8_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(z0))
U5_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(z0))
U5_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(z0))
DELETE1_IN_GAA(0) → P32_IN_GAAA(0)
DELETE1_IN_GAA(s(z0)) → P32_IN_GAAA(s(z0))

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(45) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.

(46) Complex Obligation (AND)

(47) Obligation:

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

P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
U5_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(z0))
DELETE1_IN_GAA(T169) → P44_IN_AGAA(T169)
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
U5_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(z0))
DELETE1_IN_GAA(T271) → P72_IN_AGAA(T271)
P72_IN_AGAA(s(T283)) → DELETE1_IN_GAA(s(T283))
DELETE1_IN_GAA(s(T231)) → P65_IN_GAAA(T231)
P65_IN_GAAA(0) → U13_GAAA(0, lessc34_out_ga(0))
U13_GAAA(T231, lessc34_out_ga(T231)) → DELETE1_IN_GAA(s(T231))
DELETE1_IN_GAA(T481) → P116_IN_AGAA(T481)
P116_IN_AGAA(s(T493)) → DELETE1_IN_GAA(s(T493))
DELETE1_IN_GAA(s(T699)) → DELETE1_IN_GAA(s(T699))
DELETE1_IN_GAA(s(T711)) → P79_IN_AGAA(T711)
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
U16_AGAA(T295, lessc46_out_ag(T296, T295)) → DELETE1_IN_GAA(s(T295))
DELETE1_IN_GAA(s(z0)) → P32_IN_GAAA(s(z0))
P32_IN_GAAA(s(x0)) → U8_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
U8_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(z0))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
P116_IN_AGAA(s(T505)) → P79_IN_AGAA(T505)
P65_IN_GAAA(s(x0)) → U13_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P72_IN_AGAA(s(T295)) → P79_IN_AGAA(T295)

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(48) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule DELETE1_IN_GAA(T169) → P44_IN_AGAA(T169) we obtained the following new rules [LPAR04]:

DELETE1_IN_GAA(s(z0)) → P44_IN_AGAA(s(z0))

(49) Obligation:

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

P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
U5_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(z0))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
U5_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(z0))
DELETE1_IN_GAA(T271) → P72_IN_AGAA(T271)
P72_IN_AGAA(s(T283)) → DELETE1_IN_GAA(s(T283))
DELETE1_IN_GAA(s(T231)) → P65_IN_GAAA(T231)
P65_IN_GAAA(0) → U13_GAAA(0, lessc34_out_ga(0))
U13_GAAA(T231, lessc34_out_ga(T231)) → DELETE1_IN_GAA(s(T231))
DELETE1_IN_GAA(T481) → P116_IN_AGAA(T481)
P116_IN_AGAA(s(T493)) → DELETE1_IN_GAA(s(T493))
DELETE1_IN_GAA(s(T699)) → DELETE1_IN_GAA(s(T699))
DELETE1_IN_GAA(s(T711)) → P79_IN_AGAA(T711)
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
U16_AGAA(T295, lessc46_out_ag(T296, T295)) → DELETE1_IN_GAA(s(T295))
DELETE1_IN_GAA(s(z0)) → P32_IN_GAAA(s(z0))
P32_IN_GAAA(s(x0)) → U8_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
U8_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(z0))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
P116_IN_AGAA(s(T505)) → P79_IN_AGAA(T505)
P65_IN_GAAA(s(x0)) → U13_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P72_IN_AGAA(s(T295)) → P79_IN_AGAA(T295)
DELETE1_IN_GAA(s(z0)) → P44_IN_AGAA(s(z0))

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(50) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule DELETE1_IN_GAA(T271) → P72_IN_AGAA(T271) we obtained the following new rules [LPAR04]:

DELETE1_IN_GAA(s(z0)) → P72_IN_AGAA(s(z0))

(51) Obligation:

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

P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
U5_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(z0))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
U5_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(z0))
P72_IN_AGAA(s(T283)) → DELETE1_IN_GAA(s(T283))
DELETE1_IN_GAA(s(T231)) → P65_IN_GAAA(T231)
P65_IN_GAAA(0) → U13_GAAA(0, lessc34_out_ga(0))
U13_GAAA(T231, lessc34_out_ga(T231)) → DELETE1_IN_GAA(s(T231))
DELETE1_IN_GAA(T481) → P116_IN_AGAA(T481)
P116_IN_AGAA(s(T493)) → DELETE1_IN_GAA(s(T493))
DELETE1_IN_GAA(s(T699)) → DELETE1_IN_GAA(s(T699))
DELETE1_IN_GAA(s(T711)) → P79_IN_AGAA(T711)
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
U16_AGAA(T295, lessc46_out_ag(T296, T295)) → DELETE1_IN_GAA(s(T295))
DELETE1_IN_GAA(s(z0)) → P32_IN_GAAA(s(z0))
P32_IN_GAAA(s(x0)) → U8_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
U8_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(z0))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
P116_IN_AGAA(s(T505)) → P79_IN_AGAA(T505)
P65_IN_GAAA(s(x0)) → U13_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P72_IN_AGAA(s(T295)) → P79_IN_AGAA(T295)
DELETE1_IN_GAA(s(z0)) → P44_IN_AGAA(s(z0))
DELETE1_IN_GAA(s(z0)) → P72_IN_AGAA(s(z0))

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(52) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U13_GAAA(T231, lessc34_out_ga(T231)) → DELETE1_IN_GAA(s(T231)) we obtained the following new rules [LPAR04]:

U13_GAAA(0, lessc34_out_ga(0)) → DELETE1_IN_GAA(s(0))
U13_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(s(z0)))

(53) Obligation:

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

P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
U5_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(z0))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
U5_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(z0))
P72_IN_AGAA(s(T283)) → DELETE1_IN_GAA(s(T283))
DELETE1_IN_GAA(s(T231)) → P65_IN_GAAA(T231)
P65_IN_GAAA(0) → U13_GAAA(0, lessc34_out_ga(0))
DELETE1_IN_GAA(T481) → P116_IN_AGAA(T481)
P116_IN_AGAA(s(T493)) → DELETE1_IN_GAA(s(T493))
DELETE1_IN_GAA(s(T699)) → DELETE1_IN_GAA(s(T699))
DELETE1_IN_GAA(s(T711)) → P79_IN_AGAA(T711)
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
U16_AGAA(T295, lessc46_out_ag(T296, T295)) → DELETE1_IN_GAA(s(T295))
DELETE1_IN_GAA(s(z0)) → P32_IN_GAAA(s(z0))
P32_IN_GAAA(s(x0)) → U8_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
U8_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(z0))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
P116_IN_AGAA(s(T505)) → P79_IN_AGAA(T505)
P65_IN_GAAA(s(x0)) → U13_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P72_IN_AGAA(s(T295)) → P79_IN_AGAA(T295)
DELETE1_IN_GAA(s(z0)) → P44_IN_AGAA(s(z0))
DELETE1_IN_GAA(s(z0)) → P72_IN_AGAA(s(z0))
U13_GAAA(0, lessc34_out_ga(0)) → DELETE1_IN_GAA(s(0))
U13_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(s(z0)))

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(54) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule DELETE1_IN_GAA(T481) → P116_IN_AGAA(T481) we obtained the following new rules [LPAR04]:

DELETE1_IN_GAA(s(z0)) → P116_IN_AGAA(s(z0))
DELETE1_IN_GAA(s(0)) → P116_IN_AGAA(s(0))
DELETE1_IN_GAA(s(s(z0))) → P116_IN_AGAA(s(s(z0)))

(55) Obligation:

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

P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
U5_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(z0))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
U5_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(z0))
P72_IN_AGAA(s(T283)) → DELETE1_IN_GAA(s(T283))
DELETE1_IN_GAA(s(T231)) → P65_IN_GAAA(T231)
P65_IN_GAAA(0) → U13_GAAA(0, lessc34_out_ga(0))
P116_IN_AGAA(s(T493)) → DELETE1_IN_GAA(s(T493))
DELETE1_IN_GAA(s(T699)) → DELETE1_IN_GAA(s(T699))
DELETE1_IN_GAA(s(T711)) → P79_IN_AGAA(T711)
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
U16_AGAA(T295, lessc46_out_ag(T296, T295)) → DELETE1_IN_GAA(s(T295))
DELETE1_IN_GAA(s(z0)) → P32_IN_GAAA(s(z0))
P32_IN_GAAA(s(x0)) → U8_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
U8_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(z0))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
P116_IN_AGAA(s(T505)) → P79_IN_AGAA(T505)
P65_IN_GAAA(s(x0)) → U13_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P72_IN_AGAA(s(T295)) → P79_IN_AGAA(T295)
DELETE1_IN_GAA(s(z0)) → P44_IN_AGAA(s(z0))
DELETE1_IN_GAA(s(z0)) → P72_IN_AGAA(s(z0))
U13_GAAA(0, lessc34_out_ga(0)) → DELETE1_IN_GAA(s(0))
U13_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(s(z0)))
DELETE1_IN_GAA(s(z0)) → P116_IN_AGAA(s(z0))
DELETE1_IN_GAA(s(0)) → P116_IN_AGAA(s(0))
DELETE1_IN_GAA(s(s(z0))) → P116_IN_AGAA(s(s(z0)))

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(56) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U16_AGAA(T295, lessc46_out_ag(T296, T295)) → DELETE1_IN_GAA(s(T295)) we obtained the following new rules [LPAR04]:

U16_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(s(z0)))
U16_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(s(z0)))

(57) Obligation:

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

P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
U5_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(z0))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
U5_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(z0))
P72_IN_AGAA(s(T283)) → DELETE1_IN_GAA(s(T283))
DELETE1_IN_GAA(s(T231)) → P65_IN_GAAA(T231)
P65_IN_GAAA(0) → U13_GAAA(0, lessc34_out_ga(0))
P116_IN_AGAA(s(T493)) → DELETE1_IN_GAA(s(T493))
DELETE1_IN_GAA(s(T699)) → DELETE1_IN_GAA(s(T699))
DELETE1_IN_GAA(s(T711)) → P79_IN_AGAA(T711)
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
DELETE1_IN_GAA(s(z0)) → P32_IN_GAAA(s(z0))
P32_IN_GAAA(s(x0)) → U8_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
U8_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(z0))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
P116_IN_AGAA(s(T505)) → P79_IN_AGAA(T505)
P65_IN_GAAA(s(x0)) → U13_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P72_IN_AGAA(s(T295)) → P79_IN_AGAA(T295)
DELETE1_IN_GAA(s(z0)) → P44_IN_AGAA(s(z0))
DELETE1_IN_GAA(s(z0)) → P72_IN_AGAA(s(z0))
U13_GAAA(0, lessc34_out_ga(0)) → DELETE1_IN_GAA(s(0))
U13_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(s(z0)))
DELETE1_IN_GAA(s(z0)) → P116_IN_AGAA(s(z0))
DELETE1_IN_GAA(s(0)) → P116_IN_AGAA(s(0))
DELETE1_IN_GAA(s(s(z0))) → P116_IN_AGAA(s(s(z0)))
U16_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(s(z0)))
U16_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(s(z0)))

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(58) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule DELETE1_IN_GAA(s(T231)) → P65_IN_GAAA(T231) we obtained the following new rules [LPAR04]:

DELETE1_IN_GAA(s(0)) → P65_IN_GAAA(0)
DELETE1_IN_GAA(s(s(y_0))) → P65_IN_GAAA(s(y_0))

(59) Obligation:

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

P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
U5_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(z0))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
U5_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(z0))
P72_IN_AGAA(s(T283)) → DELETE1_IN_GAA(s(T283))
P65_IN_GAAA(0) → U13_GAAA(0, lessc34_out_ga(0))
P116_IN_AGAA(s(T493)) → DELETE1_IN_GAA(s(T493))
DELETE1_IN_GAA(s(T699)) → DELETE1_IN_GAA(s(T699))
DELETE1_IN_GAA(s(T711)) → P79_IN_AGAA(T711)
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
DELETE1_IN_GAA(s(z0)) → P32_IN_GAAA(s(z0))
P32_IN_GAAA(s(x0)) → U8_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
U8_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(z0))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
P116_IN_AGAA(s(T505)) → P79_IN_AGAA(T505)
P65_IN_GAAA(s(x0)) → U13_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P72_IN_AGAA(s(T295)) → P79_IN_AGAA(T295)
DELETE1_IN_GAA(s(z0)) → P44_IN_AGAA(s(z0))
DELETE1_IN_GAA(s(z0)) → P72_IN_AGAA(s(z0))
U13_GAAA(0, lessc34_out_ga(0)) → DELETE1_IN_GAA(s(0))
U13_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(s(z0)))
DELETE1_IN_GAA(s(z0)) → P116_IN_AGAA(s(z0))
DELETE1_IN_GAA(s(0)) → P116_IN_AGAA(s(0))
DELETE1_IN_GAA(s(s(z0))) → P116_IN_AGAA(s(s(z0)))
U16_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(s(z0)))
U16_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(s(z0)))
DELETE1_IN_GAA(s(0)) → P65_IN_GAAA(0)
DELETE1_IN_GAA(s(s(y_0))) → P65_IN_GAAA(s(y_0))

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(60) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule DELETE1_IN_GAA(s(T711)) → P79_IN_AGAA(T711) we obtained the following new rules [LPAR04]:

DELETE1_IN_GAA(s(s(y_0))) → P79_IN_AGAA(s(y_0))

(61) Obligation:

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

P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
U5_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(z0))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
U5_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(z0))
P72_IN_AGAA(s(T283)) → DELETE1_IN_GAA(s(T283))
P65_IN_GAAA(0) → U13_GAAA(0, lessc34_out_ga(0))
P116_IN_AGAA(s(T493)) → DELETE1_IN_GAA(s(T493))
DELETE1_IN_GAA(s(T699)) → DELETE1_IN_GAA(s(T699))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
DELETE1_IN_GAA(s(z0)) → P32_IN_GAAA(s(z0))
P32_IN_GAAA(s(x0)) → U8_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
U8_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(z0))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
P116_IN_AGAA(s(T505)) → P79_IN_AGAA(T505)
P65_IN_GAAA(s(x0)) → U13_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P72_IN_AGAA(s(T295)) → P79_IN_AGAA(T295)
DELETE1_IN_GAA(s(z0)) → P44_IN_AGAA(s(z0))
DELETE1_IN_GAA(s(z0)) → P72_IN_AGAA(s(z0))
U13_GAAA(0, lessc34_out_ga(0)) → DELETE1_IN_GAA(s(0))
U13_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(s(z0)))
DELETE1_IN_GAA(s(z0)) → P116_IN_AGAA(s(z0))
DELETE1_IN_GAA(s(0)) → P116_IN_AGAA(s(0))
DELETE1_IN_GAA(s(s(z0))) → P116_IN_AGAA(s(s(z0)))
U16_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(s(z0)))
U16_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(s(z0)))
DELETE1_IN_GAA(s(0)) → P65_IN_GAAA(0)
DELETE1_IN_GAA(s(s(y_0))) → P65_IN_GAAA(s(y_0))
DELETE1_IN_GAA(s(s(y_0))) → P79_IN_AGAA(s(y_0))

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(62) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule P116_IN_AGAA(s(T505)) → P79_IN_AGAA(T505) we obtained the following new rules [LPAR04]:

P116_IN_AGAA(s(s(y_0))) → P79_IN_AGAA(s(y_0))

(63) Obligation:

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

P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
U5_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(z0))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
U5_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(z0))
P72_IN_AGAA(s(T283)) → DELETE1_IN_GAA(s(T283))
P65_IN_GAAA(0) → U13_GAAA(0, lessc34_out_ga(0))
P116_IN_AGAA(s(T493)) → DELETE1_IN_GAA(s(T493))
DELETE1_IN_GAA(s(T699)) → DELETE1_IN_GAA(s(T699))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
DELETE1_IN_GAA(s(z0)) → P32_IN_GAAA(s(z0))
P32_IN_GAAA(s(x0)) → U8_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
U8_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(z0))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
P65_IN_GAAA(s(x0)) → U13_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
P72_IN_AGAA(s(T295)) → P79_IN_AGAA(T295)
DELETE1_IN_GAA(s(z0)) → P44_IN_AGAA(s(z0))
DELETE1_IN_GAA(s(z0)) → P72_IN_AGAA(s(z0))
U13_GAAA(0, lessc34_out_ga(0)) → DELETE1_IN_GAA(s(0))
U13_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(s(z0)))
DELETE1_IN_GAA(s(z0)) → P116_IN_AGAA(s(z0))
DELETE1_IN_GAA(s(0)) → P116_IN_AGAA(s(0))
DELETE1_IN_GAA(s(s(z0))) → P116_IN_AGAA(s(s(z0)))
U16_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(s(z0)))
U16_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(s(z0)))
DELETE1_IN_GAA(s(0)) → P65_IN_GAAA(0)
DELETE1_IN_GAA(s(s(y_0))) → P65_IN_GAAA(s(y_0))
DELETE1_IN_GAA(s(s(y_0))) → P79_IN_AGAA(s(y_0))
P116_IN_AGAA(s(s(y_0))) → P79_IN_AGAA(s(y_0))

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(64) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule P72_IN_AGAA(s(T295)) → P79_IN_AGAA(T295) we obtained the following new rules [LPAR04]:

P72_IN_AGAA(s(s(y_0))) → P79_IN_AGAA(s(y_0))

(65) Obligation:

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

P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
U5_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(z0))
P44_IN_AGAA(s(x0)) → U5_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
U5_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(z0))
P72_IN_AGAA(s(T283)) → DELETE1_IN_GAA(s(T283))
P65_IN_GAAA(0) → U13_GAAA(0, lessc34_out_ga(0))
P116_IN_AGAA(s(T493)) → DELETE1_IN_GAA(s(T493))
DELETE1_IN_GAA(s(T699)) → DELETE1_IN_GAA(s(T699))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), lessc46_out_ag(0, s(x0)))
DELETE1_IN_GAA(s(z0)) → P32_IN_GAAA(s(z0))
P32_IN_GAAA(s(x0)) → U8_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
U8_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(z0))
P79_IN_AGAA(s(x0)) → U16_AGAA(s(x0), U83_ag(x0, lessc46_in_ag(x0)))
P65_IN_GAAA(s(x0)) → U13_GAAA(s(x0), U82_ga(x0, lessc34_in_ga(x0)))
DELETE1_IN_GAA(s(z0)) → P44_IN_AGAA(s(z0))
DELETE1_IN_GAA(s(z0)) → P72_IN_AGAA(s(z0))
U13_GAAA(0, lessc34_out_ga(0)) → DELETE1_IN_GAA(s(0))
U13_GAAA(s(z0), lessc34_out_ga(s(z0))) → DELETE1_IN_GAA(s(s(z0)))
DELETE1_IN_GAA(s(z0)) → P116_IN_AGAA(s(z0))
DELETE1_IN_GAA(s(0)) → P116_IN_AGAA(s(0))
DELETE1_IN_GAA(s(s(z0))) → P116_IN_AGAA(s(s(z0)))
U16_AGAA(s(z0), lessc46_out_ag(0, s(z0))) → DELETE1_IN_GAA(s(s(z0)))
U16_AGAA(s(z0), lessc46_out_ag(x1, s(z0))) → DELETE1_IN_GAA(s(s(z0)))
DELETE1_IN_GAA(s(0)) → P65_IN_GAAA(0)
DELETE1_IN_GAA(s(s(y_0))) → P65_IN_GAAA(s(y_0))
DELETE1_IN_GAA(s(s(y_0))) → P79_IN_AGAA(s(y_0))
P116_IN_AGAA(s(s(y_0))) → P79_IN_AGAA(s(y_0))
P72_IN_AGAA(s(s(y_0))) → P79_IN_AGAA(s(y_0))

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(66) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = DELETE1_IN_GAA(s(T699)) evaluates to t =DELETE1_IN_GAA(s(T699))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Matcher: [ ]
Semiunifier: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from DELETE1_IN_GAA(s(T699)) to DELETE1_IN_GAA(s(T699)).

(67) NO

(68) Obligation:

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

DELETE1_IN_GAA(0) → DELETE1_IN_GAA(0)
DELETE1_IN_GAA(0) → P32_IN_GAAA(0)
P32_IN_GAAA(0) → U8_GAAA(0, lessc34_out_ga(0))
U8_GAAA(0, lessc34_out_ga(0)) → DELETE1_IN_GAA(0)

The TRS R consists of the following rules:

lessc34_in_ga(0) → lessc34_out_ga(0)
lessc34_in_ga(s(T150)) → U82_ga(T150, lessc34_in_ga(T150))
U82_ga(T150, lessc34_out_ga(T150)) → lessc34_out_ga(s(T150))
lessc46_in_ag(s(T187)) → lessc46_out_ag(0, s(T187))
lessc46_in_ag(s(T193)) → U83_ag(T193, lessc46_in_ag(T193))
U83_ag(T193, lessc46_out_ag(T194, T193)) → lessc46_out_ag(s(T194), s(T193))

The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(69) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(70) Obligation:

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

DELETE1_IN_GAA(0) → DELETE1_IN_GAA(0)
DELETE1_IN_GAA(0) → P32_IN_GAAA(0)
P32_IN_GAAA(0) → U8_GAAA(0, lessc34_out_ga(0))
U8_GAAA(0, lessc34_out_ga(0)) → DELETE1_IN_GAA(0)

R is empty.
The set Q consists of the following terms:

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

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

(71) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

lessc34_in_ga(x0)
U82_ga(x0, x1)
lessc46_in_ag(x0)
U83_ag(x0, x1)

(72) Obligation:

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

DELETE1_IN_GAA(0) → DELETE1_IN_GAA(0)
DELETE1_IN_GAA(0) → P32_IN_GAAA(0)
P32_IN_GAAA(0) → U8_GAAA(0, lessc34_out_ga(0))
U8_GAAA(0, lessc34_out_ga(0)) → DELETE1_IN_GAA(0)

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

(73) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = DELETE1_IN_GAA(0) evaluates to t =DELETE1_IN_GAA(0)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Matcher: [ ]
Semiunifier: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from DELETE1_IN_GAA(0) to DELETE1_IN_GAA(0).

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

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) NonTerminationProof (EQUIVALENT transformation)

(27) NO

(28) Obligation:

(29) PiDPToQDPProof (SOUND transformation)

(30) Obligation:

(31) Narrowing (SOUND transformation)

(32) Obligation:

(33) Narrowing (SOUND transformation)

(34) Obligation:

(35) Narrowing (SOUND transformation)

(36) Obligation:

(37) Narrowing (SOUND transformation)

(38) Obligation:

(39) Instantiation (EQUIVALENT transformation)

(40) Obligation:

(41) Instantiation (EQUIVALENT transformation)

(42) Obligation:

(43) Instantiation (EQUIVALENT transformation)

(44) Obligation:

(45) DependencyGraphProof (EQUIVALENT transformation)

(46) Complex Obligation (AND)

(47) Obligation:

(48) Instantiation (EQUIVALENT transformation)

(49) Obligation:

(50) Instantiation (EQUIVALENT transformation)

(51) Obligation:

(52) Instantiation (EQUIVALENT transformation)

(53) Obligation:

(54) Instantiation (EQUIVALENT transformation)

(55) Obligation:

(56) Instantiation (EQUIVALENT transformation)

(57) Obligation:

(58) ForwardInstantiation (EQUIVALENT transformation)

(59) Obligation:

(60) ForwardInstantiation (EQUIVALENT transformation)

(61) Obligation:

(62) ForwardInstantiation (EQUIVALENT transformation)

(63) Obligation:

(64) ForwardInstantiation (EQUIVALENT transformation)

(65) Obligation:

(66) NonTerminationProof (EQUIVALENT transformation)

(67) NO

(68) Obligation:

(69) UsableRulesProof (EQUIVALENT transformation)

(70) Obligation:

(71) QReductionProof (EQUIVALENT transformation)

(72) Obligation:

(73) NonTerminationProof (EQUIVALENT transformation)

(74) NO