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

(0) Obligation:

Clauses:

insert(X, void, tree(X, void, void)).
insert(X, tree(X, Left, Right), tree(X, Left, Right)).
insert(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), insert(X, Left, Left1)).
insert(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), insert(X, Right, Right1)).
less(0, s(X1)).
less(s(X), s(Y)) :- less(X, Y).

Queries:

insert(g,a,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: insert(T1, T2, T3)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | insert(T5, T2, T3), SCOPE: 1, CLAUSE: 1 | insert(T5, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T5, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\ninsert(T1, T2, T3) !=? insert(X3, void, tree(X3, void, void))", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: insert(T5, T2, T3), SCOPE: 1, CLAUSE: 1 | insert(T5, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T5, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: true | insert(T9, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T9, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: insert(T5, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T5, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT5 is ground\ninsert(T5, T2, T3) !=? insert(X8, tree(X8, X9, X10), tree(X8, X9, X10))", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: insert(T9, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T9, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(less(T17, T22), insert(T17, T23, T24)) | insert(T17, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: insert(T9, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT9 is ground\ninsert(T9, T2, T3) !=? insert(X19, tree(X20, X21, X22), tree(X20, X23, X22))", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(less(T17, T22), insert(T17, T23, T24)), SCOPE: 2, CLAUSE: 4 | ','(less(T17, T22), insert(T17, T23, T24)), SCOPE: 2, CLAUSE: 5 | ?_2 | insert(T17, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(less(T17, T22), insert(T17, T23, T24)), SCOPE: 2, CLAUSE: 4\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(less(T17, T22), insert(T17, T23, T24)), SCOPE: 2, CLAUSE: 5 | ?_2 | insert(T17, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: insert(0, T30, T31)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(less(T17, T22), insert(T17, T23, T24)), SCOPE: 2, CLAUSE: 5\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ?_2 | insert(T17, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(less(T40, T42), insert(s(T40), T43, T44))\n\nT40 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: less(T40, T42)\n\nT40 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: insert(s(T40), T47, T48)\n\nT40 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: less(T40, T42), SCOPE: 3, CLAUSE: 4 | less(T40, T42), SCOPE: 3, CLAUSE: 5\n\nT40 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: less(T40, T42), SCOPE: 3, CLAUSE: 4\n\nT40 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: less(T40, T42), SCOPE: 3, CLAUSE: 5\n\nT40 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: less(T60, T62)\n\nT60 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: insert(T17, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(less(T82, T77), insert(T77, T83, T84))\n\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: less(T82, T77)\n\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: insert(T77, T87, T88)\n\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: less(T82, T77), SCOPE: 4, CLAUSE: 4 | less(T82, T77), SCOPE: 4, CLAUSE: 5\n\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: less(T82, T77), SCOPE: 4, CLAUSE: 4\n\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: less(T82, T77), SCOPE: 4, CLAUSE: 5\n\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: less(T102, T101)\n\nT101 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(less(T117, T112), insert(T112, T118, T119))\n\nT112 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(less(T117, T112), insert(T112, T118, T119)), SCOPE: 5, CLAUSE: 4 | ','(less(T117, T112), insert(T112, T118, T119)), SCOPE: 5, CLAUSE: 5\n\nT112 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(less(T117, T112), insert(T112, T118, T119)), SCOPE: 5, CLAUSE: 4\n\nT112 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(less(T117, T112), insert(T112, T118, T119)), SCOPE: 5, CLAUSE: 5\n\nT112 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: insert(s(T124), T125, T126)\n\nT124 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(less(T135, T134), insert(s(T134), T136, T137))\n\nT134 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: less(T135, T134)\n\nT134 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: insert(s(T134), T140, T141)\n\nT134 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(less(T151, T156), insert(T151, T157, T158)) | insert(T151, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT151 is ground\ninsert(T151, T2, T3) !=? insert(X8, tree(X8, X9, X10), tree(X8, X9, X10))", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: insert(T5, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT5 is ground\ninsert(T5, T2, T3) !=? insert(X8, tree(X8, X9, X10), tree(X8, X9, X10))\ninsert(T5, T2, T3) !=? insert(X155, tree(X156, X157, X158), tree(X156, X159, X158))", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(less(T151, T156), insert(T151, T157, T158)), SCOPE: 6, CLAUSE: 4 | ','(less(T151, T156), insert(T151, T157, T158)), SCOPE: 6, CLAUSE: 5 | ?_6 | insert(T151, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT151 is ground\ninsert(T151, T2, T3) !=? insert(X8, tree(X8, X9, X10), tree(X8, X9, X10))", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(less(T151, T156), insert(T151, T157, T158)), SCOPE: 6, CLAUSE: 4\n\nT151 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(less(T151, T156), insert(T151, T157, T158)), SCOPE: 6, CLAUSE: 5 | ?_6 | insert(T151, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT151 is ground\ninsert(T151, T2, T3) !=? insert(X8, tree(X8, X9, X10), tree(X8, X9, X10))", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: insert(0, T164, T165)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(less(T151, T156), insert(T151, T157, T158)), SCOPE: 6, CLAUSE: 5\n\nT151 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ?_6 | insert(T151, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT151 is ground\ninsert(T151, T2, T3) !=? insert(X8, tree(X8, X9, X10), tree(X8, X9, X10))", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(less(T174, T176), insert(s(T174), T177, T178))\n\nT174 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: insert(T151, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT151 is ground\ninsert(T151, T2, T3) !=? insert(X8, tree(X8, X9, X10), tree(X8, X9, X10))", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(less(T196, T191), insert(T191, T197, T198))\n\nT191 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(less(T211, T206), insert(T206, T212, T213))\n\nT206 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(less(T211, T206), insert(T206, T212, T213)), SCOPE: 7, CLAUSE: 4 | ','(less(T211, T206), insert(T206, T212, T213)), SCOPE: 7, CLAUSE: 5\n\nT206 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(less(T211, T206), insert(T206, T212, T213)), SCOPE: 7, CLAUSE: 4\n\nT206 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(less(T211, T206), insert(T206, T212, T213)), SCOPE: 7, CLAUSE: 5\n\nT206 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: insert(s(T218), T219, T220)\n\nT218 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(less(T229, T228), insert(s(T228), T230, T231))\n\nT228 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: true | insert(T237, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T237, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT237 is ground\ninsert(T237, T2, T3) !=? insert(X3, void, tree(X3, void, void))", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\ninsert(T1, T2, T3) !=? insert(X3, void, tree(X3, void, void))\ninsert(T1, T2, T3) !=? insert(X245, tree(X245, X246, X247), tree(X245, X246, X247))", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: insert(T237, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T237, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT237 is ground\ninsert(T237, T2, T3) !=? insert(X3, void, tree(X3, void, void))", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(less(T245, T250), insert(T245, T251, T252)) | insert(T245, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT245 is ground\ninsert(T245, T2, T3) !=? insert(X3, void, tree(X3, void, void))", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: insert(T237, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT237 is ground\ninsert(T237, T2, T3) !=? insert(X3, void, tree(X3, void, void))\ninsert(T237, T2, T3) !=? insert(X256, tree(X257, X258, X259), tree(X257, X260, X259))", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(less(T245, T250), insert(T245, T251, T252)), SCOPE: 8, CLAUSE: 4 | ','(less(T245, T250), insert(T245, T251, T252)), SCOPE: 8, CLAUSE: 5 | ?_8 | insert(T245, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT245 is ground\ninsert(T245, T2, T3) !=? insert(X3, void, tree(X3, void, void))", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ','(less(T245, T250), insert(T245, T251, T252)), SCOPE: 8, CLAUSE: 4\n\nT245 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(less(T245, T250), insert(T245, T251, T252)), SCOPE: 8, CLAUSE: 5 | ?_8 | insert(T245, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT245 is ground\ninsert(T245, T2, T3) !=? insert(X3, void, tree(X3, void, void))", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: insert(0, T258, T259)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(less(T245, T250), insert(T245, T251, T252)), SCOPE: 8, CLAUSE: 5\n\nT245 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ?_8 | insert(T245, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT245 is ground\ninsert(T245, T2, T3) !=? insert(X3, void, tree(X3, void, void))", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(less(T268, T270), insert(s(T268), T271, T272))\n\nT268 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: insert(T245, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT245 is ground\ninsert(T245, T2, T3) !=? insert(X3, void, tree(X3, void, void))", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(less(T290, T285), insert(T285, T291, T292))\n\nT285 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(less(T305, T300), insert(T300, T306, T307))\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(less(T305, T300), insert(T300, T306, T307)), SCOPE: 9, CLAUSE: 4 | ','(less(T305, T300), insert(T300, T306, T307)), SCOPE: 9, CLAUSE: 5\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(less(T305, T300), insert(T300, T306, T307)), SCOPE: 9, CLAUSE: 4\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(less(T305, T300), insert(T300, T306, T307)), SCOPE: 9, CLAUSE: 5\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: insert(s(T312), T313, T314)\n\nT312 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(less(T323, T322), insert(s(T322), T324, T325))\n\nT322 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ','(less(T333, T338), insert(T333, T339, T340)) | insert(T333, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT333 is ground\ninsert(T333, T2, T3) !=? insert(X3, void, tree(X3, void, void))\ninsert(T333, T2, T3) !=? insert(X245, tree(X245, X246, X247), tree(X245, X246, X247))", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\ninsert(T1, T2, T3) !=? insert(X3, void, tree(X3, void, void))\ninsert(T1, T2, T3) !=? insert(X245, tree(X245, X246, X247), tree(X245, X246, X247))\ninsert(T1, T2, T3) !=? insert(X348, tree(X349, X350, X351), tree(X349, X352, X351))", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(less(T333, T338), insert(T333, T339, T340)), SCOPE: 10, CLAUSE: 4 | ','(less(T333, T338), insert(T333, T339, T340)), SCOPE: 10, CLAUSE: 5 | ?_10 | insert(T333, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT333 is ground\ninsert(T333, T2, T3) !=? insert(X3, void, tree(X3, void, void))\ninsert(T333, T2, T3) !=? insert(X245, tree(X245, X246, X247), tree(X245, X246, X247))", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(less(T333, T338), insert(T333, T339, T340)), SCOPE: 10, CLAUSE: 4\n\nT333 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(less(T333, T338), insert(T333, T339, T340)), SCOPE: 10, CLAUSE: 5 | ?_10 | insert(T333, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT333 is ground\ninsert(T333, T2, T3) !=? insert(X3, void, tree(X3, void, void))\ninsert(T333, T2, T3) !=? insert(X245, tree(X245, X246, X247), tree(X245, X246, X247))", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: insert(0, T346, T347)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(less(T333, T338), insert(T333, T339, T340)), SCOPE: 10, CLAUSE: 5\n\nT333 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ?_10 | insert(T333, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT333 is ground\ninsert(T333, T2, T3) !=? insert(X3, void, tree(X3, void, void))\ninsert(T333, T2, T3) !=? insert(X245, tree(X245, X246, X247), tree(X245, X246, X247))", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(less(T356, T358), insert(s(T356), T359, T360))\n\nT356 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: insert(T333, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT333 is ground\ninsert(T333, T2, T3) !=? insert(X3, void, tree(X3, void, void))\ninsert(T333, T2, T3) !=? insert(X245, tree(X245, X246, X247), tree(X245, X246, X247))", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(less(T378, T373), insert(T373, T379, T380))\n\nT373 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ','(less(T393, T388), insert(T388, T394, T395))\n\nT388 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(less(T393, T388), insert(T388, T394, T395)), SCOPE: 11, CLAUSE: 4 | ','(less(T393, T388), insert(T388, T394, T395)), SCOPE: 11, CLAUSE: 5\n\nT388 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(less(T393, T388), insert(T388, T394, T395)), SCOPE: 11, CLAUSE: 4\n\nT388 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: ','(less(T393, T388), insert(T388, T394, T395)), SCOPE: 11, CLAUSE: 5\n\nT388 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: insert(s(T400), T401, T402)\n\nT400 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(less(T411, T410), insert(s(T410), T412, T413))\n\nT410 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 126 [arrowhead = none ];
126 -> 2;

127 [label="EVAL with clause\ninsert(X3, void, tree(X3, void, void)).\nand substitution\nT1 -> T5\nX3 -> T5\nT2 -> void\nT3 -> tree(T5, void, void)", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 127 [arrowhead = none ];
127 -> 3;

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

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

130 [label="EVAL with clause\ninsert(X245, tree(X245, X246, X247), tree(X245, X246, X247)).\nand substitution\nT1 -> T237\nX245 -> T237\nX246 -> T238\nX247 -> T239\nT2 -> tree(T237, T238, T239)\nT3 -> tree(T237, T238, T239)", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 130 [arrowhead = none ];
130 -> 77;

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

132 [label="EVAL with clause\ninsert(X8, tree(X8, X9, X10), tree(X8, X9, X10)).\nand substitution\nT5 -> T9\nX8 -> T9\nX9 -> T10\nX10 -> T11\nT2 -> tree(T9, T10, T11)\nT3 -> tree(T9, T10, T11)", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 132 [arrowhead = none ];
132 -> 6;

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

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

135 [label="EVAL with clause\ninsert(X155, tree(X156, X157, X158), tree(X156, X159, X158)) :- ','(less(X155, X156), insert(X155, X157, X159)).\nand substitution\nT5 -> T151\nX155 -> T151\nX156 -> T156\nX157 -> T157\nX158 -> T154\nT2 -> tree(T156, T157, T154)\nX159 -> T158\nT3 -> tree(T156, T158, T154)\nT152 -> T156\nT153 -> T157\nT155 -> T158", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 135 [arrowhead = none ];
135 -> 54;

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

137 [label="EVAL with clause\ninsert(X19, tree(X20, X21, X22), tree(X20, X23, X22)) :- ','(less(X19, X20), insert(X19, X21, X23)).\nand substitution\nT9 -> T17\nX19 -> T17\nX20 -> T22\nX21 -> T23\nX22 -> T20\nT2 -> tree(T22, T23, T20)\nX23 -> T24\nT3 -> tree(T22, T24, T20)\nT18 -> T22\nT19 -> T23\nT21 -> T24", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 137 [arrowhead = none ];
137 -> 9;

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

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

140 [label="EVAL with clause\ninsert(X118, tree(X119, X120, X121), tree(X119, X120, X122)) :- ','(less(X119, X118), insert(X118, X121, X122)).\nand substitution\nT9 -> T112\nX118 -> T112\nX119 -> T117\nX120 -> T114\nX121 -> T118\nT2 -> tree(T117, T114, T118)\nX122 -> T119\nT3 -> tree(T117, T114, T119)\nT113 -> T117\nT115 -> T118\nT116 -> T119", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 140 [arrowhead = none ];
140 -> 43;

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

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

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

144 [label="EVAL with clause\nless(0, s(X33)).\nand substitution\nT17 -> 0\nX33 -> T29\nT22 -> s(T29)\nT23 -> T30\nT24 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 144 [arrowhead = none ];
144 -> 14;

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

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

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

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

149 [label="EVAL with clause\nless(s(X45), s(X46)) :- less(X45, X46).\nand substitution\nX45 -> T40\nT17 -> s(T40)\nX46 -> T42\nT22 -> s(T42)\nT41 -> T42\nT23 -> T43\nT24 -> T44", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 149 [arrowhead = none ];
149 -> 18;

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

151 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 151 [arrowhead = none ];
151 -> 30;

152 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
18 -> 152 [arrowhead = none ];
152 -> 20;

153 [label="SPLIT 2\nreplacements:\nT43 -> T47\nT44 -> T48", fontsize=14, style = filled, fillcolor = violet];
18 -> 153 [arrowhead = none ];
153 -> 21;

154 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
20 -> 154 [arrowhead = none ];
154 -> 22;

155 [label="INSTANCE with matching:\nT1 -> s(T40)\nT2 -> T47\nT3 -> T48", fontsize=14, style = filled, fillcolor = lightgrey];
21 -> 155 [arrowhead = none , style=dashed];
155 -> 1[style=dashed];

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

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

158 [label="EVAL with clause\nless(0, s(X57)).\nand substitution\nT40 -> 0\nX57 -> T55\nT42 -> s(T55)", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 158 [arrowhead = none ];
158 -> 25;

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

160 [label="EVAL with clause\nless(s(X63), s(X64)) :- less(X63, X64).\nand substitution\nX63 -> T60\nT40 -> s(T60)\nX64 -> T62\nT42 -> s(T62)\nT61 -> T62", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 160 [arrowhead = none ];
160 -> 28;

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

162 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 162 [arrowhead = none ];
162 -> 27;

163 [label="INSTANCE with matching:\nT40 -> T60\nT42 -> T62", fontsize=14, style = filled, fillcolor = lightgrey];
28 -> 163 [arrowhead = none , style=dashed];
163 -> 20[style=dashed];

164 [label="EVAL with clause\ninsert(X81, tree(X82, X83, X84), tree(X82, X83, X85)) :- ','(less(X82, X81), insert(X81, X84, X85)).\nand substitution\nT17 -> T77\nX81 -> T77\nX82 -> T82\nX83 -> T79\nX84 -> T83\nT2 -> tree(T82, T79, T83)\nX85 -> T84\nT3 -> tree(T82, T79, T84)\nT78 -> T82\nT80 -> T83\nT81 -> T84", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 164 [arrowhead = none ];
164 -> 31;

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

166 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
31 -> 166 [arrowhead = none ];
166 -> 33;

167 [label="SPLIT 2\nnew knowledge:\nT82 is ground\nreplacements:\nT83 -> T87\nT84 -> T88", fontsize=14, style = filled, fillcolor = violet];
31 -> 167 [arrowhead = none ];
167 -> 34;

168 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
33 -> 168 [arrowhead = none ];
168 -> 35;

169 [label="INSTANCE with matching:\nT1 -> T77\nT2 -> T87\nT3 -> T88", fontsize=14, style = filled, fillcolor = lightgrey];
34 -> 169 [arrowhead = none , style=dashed];
169 -> 1[style=dashed];

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

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

172 [label="EVAL with clause\nless(0, s(X99)).\nand substitution\nT82 -> 0\nX99 -> T95\nT77 -> s(T95)", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 172 [arrowhead = none ];
172 -> 38;

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

174 [label="EVAL with clause\nless(s(X105), s(X106)) :- less(X105, X106).\nand substitution\nX105 -> T102\nT82 -> s(T102)\nX106 -> T101\nT77 -> s(T101)\nT100 -> T102", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 174 [arrowhead = none ];
174 -> 41;

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

176 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
38 -> 176 [arrowhead = none ];
176 -> 40;

177 [label="INSTANCE with matching:\nT82 -> T102\nT77 -> T101", fontsize=14, style = filled, fillcolor = lightgrey];
41 -> 177 [arrowhead = none , style=dashed];
177 -> 33[style=dashed];

178 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
43 -> 178 [arrowhead = none ];
178 -> 45;

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

180 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 180 [arrowhead = none ];
180 -> 47;

181 [label="EVAL with clause\nless(0, s(X132)).\nand substitution\nT117 -> 0\nX132 -> T124\nT112 -> s(T124)\nT118 -> T125\nT119 -> T126", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 181 [arrowhead = none ];
181 -> 48;

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

183 [label="EVAL with clause\nless(s(X140), s(X141)) :- less(X140, X141).\nand substitution\nX140 -> T135\nT117 -> s(T135)\nX141 -> T134\nT112 -> s(T134)\nT133 -> T135\nT118 -> T136\nT119 -> T137", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 183 [arrowhead = none ];
183 -> 50;

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

185 [label="INSTANCE with matching:\nT1 -> s(T124)\nT2 -> T125\nT3 -> T126", fontsize=14, style = filled, fillcolor = lightgrey];
48 -> 185 [arrowhead = none , style=dashed];
185 -> 1[style=dashed];

186 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
50 -> 186 [arrowhead = none ];
186 -> 52;

187 [label="SPLIT 2\nnew knowledge:\nT135 is ground\nreplacements:\nT136 -> T140\nT137 -> T141", fontsize=14, style = filled, fillcolor = violet];
50 -> 187 [arrowhead = none ];
187 -> 53;

188 [label="INSTANCE with matching:\nT82 -> T135\nT77 -> T134", fontsize=14, style = filled, fillcolor = lightgrey];
52 -> 188 [arrowhead = none , style=dashed];
188 -> 33[style=dashed];

189 [label="INSTANCE with matching:\nT1 -> s(T134)\nT2 -> T140\nT3 -> T141", fontsize=14, style = filled, fillcolor = lightgrey];
53 -> 189 [arrowhead = none , style=dashed];
189 -> 1[style=dashed];

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

191 [label="EVAL with clause\ninsert(X214, tree(X215, X216, X217), tree(X215, X216, X218)) :- ','(less(X215, X214), insert(X214, X217, X218)).\nand substitution\nT5 -> T206\nX214 -> T206\nX215 -> T211\nX216 -> T208\nX217 -> T212\nT2 -> tree(T211, T208, T212)\nX218 -> T213\nT3 -> tree(T211, T208, T213)\nT207 -> T211\nT209 -> T212\nT210 -> T213", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 191 [arrowhead = none ];
191 -> 68;

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

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

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

195 [label="EVAL with clause\nless(0, s(X169)).\nand substitution\nT151 -> 0\nX169 -> T163\nT156 -> s(T163)\nT157 -> T164\nT158 -> T165", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 195 [arrowhead = none ];
195 -> 59;

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

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

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

199 [label="INSTANCE with matching:\nT1 -> 0\nT2 -> T164\nT3 -> T165", fontsize=14, style = filled, fillcolor = lightgrey];
59 -> 199 [arrowhead = none , style=dashed];
199 -> 1[style=dashed];

200 [label="EVAL with clause\nless(s(X181), s(X182)) :- less(X181, X182).\nand substitution\nX181 -> T174\nT151 -> s(T174)\nX182 -> T176\nT156 -> s(T176)\nT175 -> T176\nT157 -> T177\nT158 -> T178", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 200 [arrowhead = none ];
200 -> 63;

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

202 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 202 [arrowhead = none ];
202 -> 65;

203 [label="INSTANCE with matching:\nT40 -> T174\nT42 -> T176\nT43 -> T177\nT44 -> T178", fontsize=14, style = filled, fillcolor = lightgrey];
63 -> 203 [arrowhead = none , style=dashed];
203 -> 18[style=dashed];

204 [label="EVAL with clause\ninsert(X197, tree(X198, X199, X200), tree(X198, X199, X201)) :- ','(less(X198, X197), insert(X197, X200, X201)).\nand substitution\nT151 -> T191\nX197 -> T191\nX198 -> T196\nX199 -> T193\nX200 -> T197\nT2 -> tree(T196, T193, T197)\nX201 -> T198\nT3 -> tree(T196, T193, T198)\nT192 -> T196\nT194 -> T197\nT195 -> T198", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 204 [arrowhead = none ];
204 -> 66;

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

206 [label="INSTANCE with matching:\nT117 -> T196\nT112 -> T191\nT118 -> T197\nT119 -> T198", fontsize=14, style = filled, fillcolor = lightgrey];
66 -> 206 [arrowhead = none , style=dashed];
206 -> 43[style=dashed];

207 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
68 -> 207 [arrowhead = none ];
207 -> 70;

208 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
70 -> 208 [arrowhead = none ];
208 -> 71;

209 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
70 -> 209 [arrowhead = none ];
209 -> 72;

210 [label="EVAL with clause\nless(0, s(X228)).\nand substitution\nT211 -> 0\nX228 -> T218\nT206 -> s(T218)\nT212 -> T219\nT213 -> T220", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 210 [arrowhead = none ];
210 -> 73;

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

212 [label="EVAL with clause\nless(s(X236), s(X237)) :- less(X236, X237).\nand substitution\nX236 -> T229\nT211 -> s(T229)\nX237 -> T228\nT206 -> s(T228)\nT227 -> T229\nT212 -> T230\nT213 -> T231", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 212 [arrowhead = none ];
212 -> 75;

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

214 [label="INSTANCE with matching:\nT1 -> s(T218)\nT2 -> T219\nT3 -> T220", fontsize=14, style = filled, fillcolor = lightgrey];
73 -> 214 [arrowhead = none , style=dashed];
214 -> 1[style=dashed];

215 [label="INSTANCE with matching:\nT135 -> T229\nT134 -> T228\nT136 -> T230\nT137 -> T231", fontsize=14, style = filled, fillcolor = lightgrey];
75 -> 215 [arrowhead = none , style=dashed];
215 -> 50[style=dashed];

216 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 216 [arrowhead = none ];
216 -> 79;

217 [label="EVAL with clause\ninsert(X348, tree(X349, X350, X351), tree(X349, X352, X351)) :- ','(less(X348, X349), insert(X348, X350, X352)).\nand substitution\nT1 -> T333\nX348 -> T333\nX349 -> T338\nX350 -> T339\nX351 -> T336\nT2 -> tree(T338, T339, T336)\nX352 -> T340\nT3 -> tree(T338, T340, T336)\nT334 -> T338\nT335 -> T339\nT337 -> T340", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 217 [arrowhead = none ];
217 -> 103;

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

219 [label="EVAL with clause\ninsert(X256, tree(X257, X258, X259), tree(X257, X260, X259)) :- ','(less(X256, X257), insert(X256, X258, X260)).\nand substitution\nT237 -> T245\nX256 -> T245\nX257 -> T250\nX258 -> T251\nX259 -> T248\nT2 -> tree(T250, T251, T248)\nX260 -> T252\nT3 -> tree(T250, T252, T248)\nT246 -> T250\nT247 -> T251\nT249 -> T252", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 219 [arrowhead = none ];
219 -> 80;

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

221 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
80 -> 221 [arrowhead = none ];
221 -> 82;

222 [label="EVAL with clause\ninsert(X315, tree(X316, X317, X318), tree(X316, X317, X319)) :- ','(less(X316, X315), insert(X315, X318, X319)).\nand substitution\nT237 -> T300\nX315 -> T300\nX316 -> T305\nX317 -> T302\nX318 -> T306\nT2 -> tree(T305, T302, T306)\nX319 -> T307\nT3 -> tree(T305, T302, T307)\nT301 -> T305\nT303 -> T306\nT304 -> T307", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 222 [arrowhead = none ];
222 -> 94;

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

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

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

226 [label="EVAL with clause\nless(0, s(X270)).\nand substitution\nT245 -> 0\nX270 -> T257\nT250 -> s(T257)\nT251 -> T258\nT252 -> T259", fontsize=14, style = filled, fillcolor = lightblue];
83 -> 226 [arrowhead = none ];
226 -> 85;

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

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

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

230 [label="INSTANCE with matching:\nT1 -> 0\nT2 -> T258\nT3 -> T259", fontsize=14, style = filled, fillcolor = lightgrey];
85 -> 230 [arrowhead = none , style=dashed];
230 -> 1[style=dashed];

231 [label="EVAL with clause\nless(s(X282), s(X283)) :- less(X282, X283).\nand substitution\nX282 -> T268\nT245 -> s(T268)\nX283 -> T270\nT250 -> s(T270)\nT269 -> T270\nT251 -> T271\nT252 -> T272", fontsize=14, style = filled, fillcolor = lightblue];
87 -> 231 [arrowhead = none ];
231 -> 89;

232 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
87 -> 232 [arrowhead = none ];
232 -> 90;

233 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 233 [arrowhead = none ];
233 -> 91;

234 [label="INSTANCE with matching:\nT174 -> T268\nT176 -> T270\nT177 -> T271\nT178 -> T272", fontsize=14, style = filled, fillcolor = lightgrey];
89 -> 234 [arrowhead = none , style=dashed];
234 -> 63[style=dashed];

235 [label="EVAL with clause\ninsert(X298, tree(X299, X300, X301), tree(X299, X300, X302)) :- ','(less(X299, X298), insert(X298, X301, X302)).\nand substitution\nT245 -> T285\nX298 -> T285\nX299 -> T290\nX300 -> T287\nX301 -> T291\nT2 -> tree(T290, T287, T291)\nX302 -> T292\nT3 -> tree(T290, T287, T292)\nT286 -> T290\nT288 -> T291\nT289 -> T292", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 235 [arrowhead = none ];
235 -> 92;

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

237 [label="INSTANCE with matching:\nT211 -> T290\nT206 -> T285\nT212 -> T291\nT213 -> T292", fontsize=14, style = filled, fillcolor = lightgrey];
92 -> 237 [arrowhead = none , style=dashed];
237 -> 68[style=dashed];

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

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

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

241 [label="EVAL with clause\nless(0, s(X329)).\nand substitution\nT305 -> 0\nX329 -> T312\nT300 -> s(T312)\nT306 -> T313\nT307 -> T314", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 241 [arrowhead = none ];
241 -> 99;

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

243 [label="EVAL with clause\nless(s(X337), s(X338)) :- less(X337, X338).\nand substitution\nX337 -> T323\nT305 -> s(T323)\nX338 -> T322\nT300 -> s(T322)\nT321 -> T323\nT306 -> T324\nT307 -> T325", fontsize=14, style = filled, fillcolor = lightblue];
98 -> 243 [arrowhead = none ];
243 -> 101;

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

245 [label="INSTANCE with matching:\nT1 -> s(T312)\nT2 -> T313\nT3 -> T314", fontsize=14, style = filled, fillcolor = lightgrey];
99 -> 245 [arrowhead = none , style=dashed];
245 -> 1[style=dashed];

246 [label="INSTANCE with matching:\nT229 -> T323\nT228 -> T322\nT230 -> T324\nT231 -> T325", fontsize=14, style = filled, fillcolor = lightgrey];
101 -> 246 [arrowhead = none , style=dashed];
246 -> 75[style=dashed];

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

248 [label="EVAL with clause\ninsert(X407, tree(X408, X409, X410), tree(X408, X409, X411)) :- ','(less(X408, X407), insert(X407, X410, X411)).\nand substitution\nT1 -> T388\nX407 -> T388\nX408 -> T393\nX409 -> T390\nX410 -> T394\nT2 -> tree(T393, T390, T394)\nX411 -> T395\nT3 -> tree(T393, T390, T395)\nT389 -> T393\nT391 -> T394\nT392 -> T395", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 248 [arrowhead = none ];
248 -> 117;

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

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

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

252 [label="EVAL with clause\nless(0, s(X362)).\nand substitution\nT333 -> 0\nX362 -> T345\nT338 -> s(T345)\nT339 -> T346\nT340 -> T347", fontsize=14, style = filled, fillcolor = lightblue];
106 -> 252 [arrowhead = none ];
252 -> 108;

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

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

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

256 [label="INSTANCE with matching:\nT1 -> 0\nT2 -> T346\nT3 -> T347", fontsize=14, style = filled, fillcolor = lightgrey];
108 -> 256 [arrowhead = none , style=dashed];
256 -> 1[style=dashed];

257 [label="EVAL with clause\nless(s(X374), s(X375)) :- less(X374, X375).\nand substitution\nX374 -> T356\nT333 -> s(T356)\nX375 -> T358\nT338 -> s(T358)\nT357 -> T358\nT339 -> T359\nT340 -> T360", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 257 [arrowhead = none ];
257 -> 112;

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

259 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
111 -> 259 [arrowhead = none ];
259 -> 114;

260 [label="INSTANCE with matching:\nT174 -> T356\nT176 -> T358\nT177 -> T359\nT178 -> T360", fontsize=14, style = filled, fillcolor = lightgrey];
112 -> 260 [arrowhead = none , style=dashed];
260 -> 63[style=dashed];

261 [label="EVAL with clause\ninsert(X390, tree(X391, X392, X393), tree(X391, X392, X394)) :- ','(less(X391, X390), insert(X390, X393, X394)).\nand substitution\nT333 -> T373\nX390 -> T373\nX391 -> T378\nX392 -> T375\nX393 -> T379\nT2 -> tree(T378, T375, T379)\nX394 -> T380\nT3 -> tree(T378, T375, T380)\nT374 -> T378\nT376 -> T379\nT377 -> T380", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 261 [arrowhead = none ];
261 -> 115;

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

263 [label="INSTANCE with matching:\nT211 -> T378\nT206 -> T373\nT212 -> T379\nT213 -> T380", fontsize=14, style = filled, fillcolor = lightgrey];
115 -> 263 [arrowhead = none , style=dashed];
263 -> 68[style=dashed];

264 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
117 -> 264 [arrowhead = none ];
264 -> 119;

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

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

267 [label="EVAL with clause\nless(0, s(X421)).\nand substitution\nT393 -> 0\nX421 -> T400\nT388 -> s(T400)\nT394 -> T401\nT395 -> T402", fontsize=14, style = filled, fillcolor = lightblue];
120 -> 267 [arrowhead = none ];
267 -> 122;

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

269 [label="EVAL with clause\nless(s(X429), s(X430)) :- less(X429, X430).\nand substitution\nX429 -> T411\nT393 -> s(T411)\nX430 -> T410\nT388 -> s(T410)\nT409 -> T411\nT394 -> T412\nT395 -> T413", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 269 [arrowhead = none ];
269 -> 124;

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

271 [label="INSTANCE with matching:\nT1 -> s(T400)\nT2 -> T401\nT3 -> T402", fontsize=14, style = filled, fillcolor = lightgrey];
122 -> 271 [arrowhead = none , style=dashed];
271 -> 1[style=dashed];

272 [label="INSTANCE with matching:\nT229 -> T411\nT228 -> T410\nT230 -> T412\nT231 -> T413", fontsize=14, style = filled, fillcolor = lightgrey];
124 -> 272 [arrowhead = none , style=dashed];
272 -> 75[style=dashed];

}

(2) Obligation:

Triples:

less20(s(T60), s(T62)) :- less20(T60, T62).
less33(s(T102), s(T101)) :- less33(T102, T101).
p18(T40, T42, T43, T44) :- less20(T40, T42).
p18(T40, T42, T47, T48) :- ','(lessc20(T40, T42), insert1(s(T40), T47, T48)).
p43(0, s(T124), T125, T126) :- insert1(s(T124), T125, T126).
p43(s(T135), s(T134), T136, T137) :- p50(T135, T134, T136, T137).
p50(T135, T134, T136, T137) :- less33(T135, T134).
p50(T135, T134, T140, T141) :- ','(lessc33(T135, T134), insert1(s(T134), T140, T141)).
p68(0, s(T218), T219, T220) :- insert1(s(T218), T219, T220).
p68(s(T229), s(T228), T230, T231) :- p50(T229, T228, T230, T231).
insert1(0, tree(s(T29), T30, T20), tree(s(T29), T31, T20)) :- insert1(0, T30, T31).
insert1(s(T40), tree(s(T42), T43, T20), tree(s(T42), T44, T20)) :- p18(T40, T42, T43, T44).
insert1(T77, tree(T82, T79, T83), tree(T82, T79, T84)) :- less33(T82, T77).
insert1(T77, tree(T82, T79, T87), tree(T82, T79, T88)) :- ','(lessc33(T82, T77), insert1(T77, T87, T88)).
insert1(T112, tree(T117, T114, T118), tree(T117, T114, T119)) :- p43(T117, T112, T118, T119).
insert1(0, tree(s(T163), T164, T154), tree(s(T163), T165, T154)) :- insert1(0, T164, T165).
insert1(s(T174), tree(s(T176), T177, T154), tree(s(T176), T178, T154)) :- p18(T174, T176, T177, T178).
insert1(T191, tree(T196, T193, T197), tree(T196, T193, T198)) :- p43(T196, T191, T197, T198).
insert1(T206, tree(T211, T208, T212), tree(T211, T208, T213)) :- p68(T211, T206, T212, T213).
insert1(0, tree(s(T257), T258, T248), tree(s(T257), T259, T248)) :- insert1(0, T258, T259).
insert1(s(T268), tree(s(T270), T271, T248), tree(s(T270), T272, T248)) :- p18(T268, T270, T271, T272).
insert1(T285, tree(T290, T287, T291), tree(T290, T287, T292)) :- p68(T290, T285, T291, T292).
insert1(s(T312), tree(0, T302, T313), tree(0, T302, T314)) :- insert1(s(T312), T313, T314).
insert1(s(T322), tree(s(T323), T302, T324), tree(s(T323), T302, T325)) :- p50(T323, T322, T324, T325).
insert1(0, tree(s(T345), T346, T336), tree(s(T345), T347, T336)) :- insert1(0, T346, T347).
insert1(s(T356), tree(s(T358), T359, T336), tree(s(T358), T360, T336)) :- p18(T356, T358, T359, T360).
insert1(T373, tree(T378, T375, T379), tree(T378, T375, T380)) :- p68(T378, T373, T379, T380).
insert1(s(T400), tree(0, T390, T401), tree(0, T390, T402)) :- insert1(s(T400), T401, T402).
insert1(s(T410), tree(s(T411), T390, T412), tree(s(T411), T390, T413)) :- p50(T411, T410, T412, T413).

Clauses:

insertc1(T5, void, tree(T5, void, void)).
insertc1(T9, tree(T9, T10, T11), tree(T9, T10, T11)).
insertc1(0, tree(s(T29), T30, T20), tree(s(T29), T31, T20)) :- insertc1(0, T30, T31).
insertc1(s(T40), tree(s(T42), T43, T20), tree(s(T42), T44, T20)) :- qc18(T40, T42, T43, T44).
insertc1(T77, tree(T82, T79, T87), tree(T82, T79, T88)) :- ','(lessc33(T82, T77), insertc1(T77, T87, T88)).
insertc1(T112, tree(T117, T114, T118), tree(T117, T114, T119)) :- qc43(T117, T112, T118, T119).
insertc1(0, tree(s(T163), T164, T154), tree(s(T163), T165, T154)) :- insertc1(0, T164, T165).
insertc1(s(T174), tree(s(T176), T177, T154), tree(s(T176), T178, T154)) :- qc18(T174, T176, T177, T178).
insertc1(T191, tree(T196, T193, T197), tree(T196, T193, T198)) :- qc43(T196, T191, T197, T198).
insertc1(T206, tree(T211, T208, T212), tree(T211, T208, T213)) :- qc68(T211, T206, T212, T213).
insertc1(T237, tree(T237, T238, T239), tree(T237, T238, T239)).
insertc1(0, tree(s(T257), T258, T248), tree(s(T257), T259, T248)) :- insertc1(0, T258, T259).
insertc1(s(T268), tree(s(T270), T271, T248), tree(s(T270), T272, T248)) :- qc18(T268, T270, T271, T272).
insertc1(T285, tree(T290, T287, T291), tree(T290, T287, T292)) :- qc68(T290, T285, T291, T292).
insertc1(s(T312), tree(0, T302, T313), tree(0, T302, T314)) :- insertc1(s(T312), T313, T314).
insertc1(s(T322), tree(s(T323), T302, T324), tree(s(T323), T302, T325)) :- qc50(T323, T322, T324, T325).
insertc1(0, tree(s(T345), T346, T336), tree(s(T345), T347, T336)) :- insertc1(0, T346, T347).
insertc1(s(T356), tree(s(T358), T359, T336), tree(s(T358), T360, T336)) :- qc18(T356, T358, T359, T360).
insertc1(T373, tree(T378, T375, T379), tree(T378, T375, T380)) :- qc68(T378, T373, T379, T380).
insertc1(s(T400), tree(0, T390, T401), tree(0, T390, T402)) :- insertc1(s(T400), T401, T402).
insertc1(s(T410), tree(s(T411), T390, T412), tree(s(T411), T390, T413)) :- qc50(T411, T410, T412, T413).
lessc20(0, s(T55)).
lessc20(s(T60), s(T62)) :- lessc20(T60, T62).
lessc33(0, s(T95)).
lessc33(s(T102), s(T101)) :- lessc33(T102, T101).
qc18(T40, T42, T47, T48) :- ','(lessc20(T40, T42), insertc1(s(T40), T47, T48)).
qc43(0, s(T124), T125, T126) :- insertc1(s(T124), T125, T126).
qc43(s(T135), s(T134), T136, T137) :- qc50(T135, T134, T136, T137).
qc50(T135, T134, T140, T141) :- ','(lessc33(T135, T134), insertc1(s(T134), T140, T141)).
qc68(0, s(T218), T219, T220) :- insertc1(s(T218), T219, T220).
qc68(s(T229), s(T228), T230, T231) :- qc50(T229, T228, T230, T231).

Afs:

insert1(x1, x2, x3)  =  insert1(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:
insert1_in: (b,f,f)
p18_in: (b,f,f,f)
less20_in: (b,f)
lessc20_in: (b,f)
less33_in: (f,b)
lessc33_in: (f,b)
p43_in: (f,b,f,f)
p50_in: (f,b,f,f)
p68_in: (f,b,f,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

INSERT1_IN_GAA(0, tree(s(T29), T30, T20), tree(s(T29), T31, T20)) → U13_GAA(T29, T30, T20, T31, insert1_in_gaa(0, T30, T31))
INSERT1_IN_GAA(0, tree(s(T29), T30, T20), tree(s(T29), T31, T20)) → INSERT1_IN_GAA(0, T30, T31)
INSERT1_IN_GAA(s(T40), tree(s(T42), T43, T20), tree(s(T42), T44, T20)) → U14_GAA(T40, T42, T43, T20, T44, p18_in_gaaa(T40, T42, T43, T44))
INSERT1_IN_GAA(s(T40), tree(s(T42), T43, T20), tree(s(T42), T44, T20)) → P18_IN_GAAA(T40, T42, T43, T44)
P18_IN_GAAA(T40, T42, T43, T44) → U3_GAAA(T40, T42, T43, T44, less20_in_ga(T40, T42))
P18_IN_GAAA(T40, T42, T43, T44) → LESS20_IN_GA(T40, T42)
LESS20_IN_GA(s(T60), s(T62)) → U1_GA(T60, T62, less20_in_ga(T60, T62))
LESS20_IN_GA(s(T60), s(T62)) → LESS20_IN_GA(T60, T62)
P18_IN_GAAA(T40, T42, T47, T48) → U4_GAAA(T40, T42, T47, T48, lessc20_in_ga(T40, T42))
U4_GAAA(T40, T42, T47, T48, lessc20_out_ga(T40, T42)) → U5_GAAA(T40, T42, T47, T48, insert1_in_gaa(s(T40), T47, T48))
U4_GAAA(T40, T42, T47, T48, lessc20_out_ga(T40, T42)) → INSERT1_IN_GAA(s(T40), T47, T48)
INSERT1_IN_GAA(T77, tree(T82, T79, T83), tree(T82, T79, T84)) → U15_GAA(T77, T82, T79, T83, T84, less33_in_ag(T82, T77))
INSERT1_IN_GAA(T77, tree(T82, T79, T83), tree(T82, T79, T84)) → LESS33_IN_AG(T82, T77)
LESS33_IN_AG(s(T102), s(T101)) → U2_AG(T102, T101, less33_in_ag(T102, T101))
LESS33_IN_AG(s(T102), s(T101)) → LESS33_IN_AG(T102, T101)
INSERT1_IN_GAA(T77, tree(T82, T79, T87), tree(T82, T79, T88)) → U16_GAA(T77, T82, T79, T87, T88, lessc33_in_ag(T82, T77))
U16_GAA(T77, T82, T79, T87, T88, lessc33_out_ag(T82, T77)) → U17_GAA(T77, T82, T79, T87, T88, insert1_in_gaa(T77, T87, T88))
U16_GAA(T77, T82, T79, T87, T88, lessc33_out_ag(T82, T77)) → INSERT1_IN_GAA(T77, T87, T88)
INSERT1_IN_GAA(T112, tree(T117, T114, T118), tree(T117, T114, T119)) → U18_GAA(T112, T117, T114, T118, T119, p43_in_agaa(T117, T112, T118, T119))
INSERT1_IN_GAA(T112, tree(T117, T114, T118), tree(T117, T114, T119)) → P43_IN_AGAA(T117, T112, T118, T119)
P43_IN_AGAA(0, s(T124), T125, T126) → U6_AGAA(T124, T125, T126, insert1_in_gaa(s(T124), T125, T126))
P43_IN_AGAA(0, s(T124), T125, T126) → INSERT1_IN_GAA(s(T124), T125, T126)
INSERT1_IN_GAA(0, tree(s(T163), T164, T154), tree(s(T163), T165, T154)) → U19_GAA(T163, T164, T154, T165, insert1_in_gaa(0, T164, T165))
INSERT1_IN_GAA(s(T174), tree(s(T176), T177, T154), tree(s(T176), T178, T154)) → U20_GAA(T174, T176, T177, T154, T178, p18_in_gaaa(T174, T176, T177, T178))
INSERT1_IN_GAA(T191, tree(T196, T193, T197), tree(T196, T193, T198)) → U21_GAA(T191, T196, T193, T197, T198, p43_in_agaa(T196, T191, T197, T198))
P43_IN_AGAA(s(T135), s(T134), T136, T137) → U7_AGAA(T135, T134, T136, T137, p50_in_agaa(T135, T134, T136, T137))
P43_IN_AGAA(s(T135), s(T134), T136, T137) → P50_IN_AGAA(T135, T134, T136, T137)
P50_IN_AGAA(T135, T134, T136, T137) → U8_AGAA(T135, T134, T136, T137, less33_in_ag(T135, T134))
P50_IN_AGAA(T135, T134, T136, T137) → LESS33_IN_AG(T135, T134)
P50_IN_AGAA(T135, T134, T140, T141) → U9_AGAA(T135, T134, T140, T141, lessc33_in_ag(T135, T134))
U9_AGAA(T135, T134, T140, T141, lessc33_out_ag(T135, T134)) → U10_AGAA(T135, T134, T140, T141, insert1_in_gaa(s(T134), T140, T141))
U9_AGAA(T135, T134, T140, T141, lessc33_out_ag(T135, T134)) → INSERT1_IN_GAA(s(T134), T140, T141)
INSERT1_IN_GAA(T206, tree(T211, T208, T212), tree(T211, T208, T213)) → U22_GAA(T206, T211, T208, T212, T213, p68_in_agaa(T211, T206, T212, T213))
INSERT1_IN_GAA(T206, tree(T211, T208, T212), tree(T211, T208, T213)) → P68_IN_AGAA(T211, T206, T212, T213)
P68_IN_AGAA(0, s(T218), T219, T220) → U11_AGAA(T218, T219, T220, insert1_in_gaa(s(T218), T219, T220))
P68_IN_AGAA(0, s(T218), T219, T220) → INSERT1_IN_GAA(s(T218), T219, T220)
INSERT1_IN_GAA(0, tree(s(T257), T258, T248), tree(s(T257), T259, T248)) → U23_GAA(T257, T258, T248, T259, insert1_in_gaa(0, T258, T259))
INSERT1_IN_GAA(s(T268), tree(s(T270), T271, T248), tree(s(T270), T272, T248)) → U24_GAA(T268, T270, T271, T248, T272, p18_in_gaaa(T268, T270, T271, T272))
INSERT1_IN_GAA(T285, tree(T290, T287, T291), tree(T290, T287, T292)) → U25_GAA(T285, T290, T287, T291, T292, p68_in_agaa(T290, T285, T291, T292))
P68_IN_AGAA(s(T229), s(T228), T230, T231) → U12_AGAA(T229, T228, T230, T231, p50_in_agaa(T229, T228, T230, T231))
P68_IN_AGAA(s(T229), s(T228), T230, T231) → P50_IN_AGAA(T229, T228, T230, T231)
INSERT1_IN_GAA(s(T312), tree(0, T302, T313), tree(0, T302, T314)) → U26_GAA(T312, T302, T313, T314, insert1_in_gaa(s(T312), T313, T314))
INSERT1_IN_GAA(s(T312), tree(0, T302, T313), tree(0, T302, T314)) → INSERT1_IN_GAA(s(T312), T313, T314)
INSERT1_IN_GAA(s(T322), tree(s(T323), T302, T324), tree(s(T323), T302, T325)) → U27_GAA(T322, T323, T302, T324, T325, p50_in_agaa(T323, T322, T324, T325))
INSERT1_IN_GAA(s(T322), tree(s(T323), T302, T324), tree(s(T323), T302, T325)) → P50_IN_AGAA(T323, T322, T324, T325)
INSERT1_IN_GAA(0, tree(s(T345), T346, T336), tree(s(T345), T347, T336)) → U28_GAA(T345, T346, T336, T347, insert1_in_gaa(0, T346, T347))
INSERT1_IN_GAA(s(T356), tree(s(T358), T359, T336), tree(s(T358), T360, T336)) → U29_GAA(T356, T358, T359, T336, T360, p18_in_gaaa(T356, T358, T359, T360))
INSERT1_IN_GAA(T373, tree(T378, T375, T379), tree(T378, T375, T380)) → U30_GAA(T373, T378, T375, T379, T380, p68_in_agaa(T378, T373, T379, T380))
INSERT1_IN_GAA(s(T400), tree(0, T390, T401), tree(0, T390, T402)) → U31_GAA(T400, T390, T401, T402, insert1_in_gaa(s(T400), T401, T402))
INSERT1_IN_GAA(s(T410), tree(s(T411), T390, T412), tree(s(T411), T390, T413)) → U32_GAA(T410, T411, T390, T412, T413, p50_in_agaa(T411, T410, T412, T413))

The TRS R consists of the following rules:

lessc20_in_ga(0, s(T55)) → lessc20_out_ga(0, s(T55))
lessc20_in_ga(s(T60), s(T62)) → U53_ga(T60, T62, lessc20_in_ga(T60, T62))
U53_ga(T60, T62, lessc20_out_ga(T60, T62)) → lessc20_out_ga(s(T60), s(T62))
lessc33_in_ag(0, s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T102), s(T101)) → U54_ag(T102, T101, lessc33_in_ag(T102, T101))
U54_ag(T102, T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The argument filtering Pi contains the following mapping:
insert1_in_gaa(x1, x2, x3)  =  insert1_in_gaa(x1)
0  =  0
s(x1)  =  s(x1)
p18_in_gaaa(x1, x2, x3, x4)  =  p18_in_gaaa(x1)
less20_in_ga(x1, x2)  =  less20_in_ga(x1)
lessc20_in_ga(x1, x2)  =  lessc20_in_ga(x1)
lessc20_out_ga(x1, x2)  =  lessc20_out_ga(x1)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
less33_in_ag(x1, x2)  =  less33_in_ag(x2)
lessc33_in_ag(x1, x2)  =  lessc33_in_ag(x2)
lessc33_out_ag(x1, x2)  =  lessc33_out_ag(x1, x2)
U54_ag(x1, x2, x3)  =  U54_ag(x2, x3)
p43_in_agaa(x1, x2, x3, x4)  =  p43_in_agaa(x2)
p50_in_agaa(x1, x2, x3, x4)  =  p50_in_agaa(x2)
p68_in_agaa(x1, x2, x3, x4)  =  p68_in_agaa(x2)
INSERT1_IN_GAA(x1, x2, x3)  =  INSERT1_IN_GAA(x1)
U13_GAA(x1, x2, x3, x4, x5)  =  U13_GAA(x5)
U14_GAA(x1, x2, x3, x4, x5, x6)  =  U14_GAA(x1, x6)
P18_IN_GAAA(x1, x2, x3, x4)  =  P18_IN_GAAA(x1)
U3_GAAA(x1, x2, x3, x4, x5)  =  U3_GAAA(x1, x5)
LESS20_IN_GA(x1, x2)  =  LESS20_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U4_GAAA(x1, x2, x3, x4, x5)  =  U4_GAAA(x1, x5)
U5_GAAA(x1, x2, x3, x4, x5)  =  U5_GAAA(x1, x5)
U15_GAA(x1, x2, x3, x4, x5, x6)  =  U15_GAA(x1, x6)
LESS33_IN_AG(x1, x2)  =  LESS33_IN_AG(x2)
U2_AG(x1, x2, x3)  =  U2_AG(x2, x3)
U16_GAA(x1, x2, x3, x4, x5, x6)  =  U16_GAA(x1, x6)
U17_GAA(x1, x2, x3, x4, x5, x6)  =  U17_GAA(x1, x6)
U18_GAA(x1, x2, x3, x4, x5, x6)  =  U18_GAA(x1, x6)
P43_IN_AGAA(x1, x2, x3, x4)  =  P43_IN_AGAA(x2)
U6_AGAA(x1, x2, x3, x4)  =  U6_AGAA(x1, x4)
U19_GAA(x1, x2, x3, x4, x5)  =  U19_GAA(x5)
U20_GAA(x1, x2, x3, x4, x5, x6)  =  U20_GAA(x1, x6)
U21_GAA(x1, x2, x3, x4, x5, x6)  =  U21_GAA(x1, x6)
U7_AGAA(x1, x2, x3, x4, x5)  =  U7_AGAA(x2, x5)
P50_IN_AGAA(x1, x2, x3, x4)  =  P50_IN_AGAA(x2)
U8_AGAA(x1, x2, x3, x4, x5)  =  U8_AGAA(x2, x5)
U9_AGAA(x1, x2, x3, x4, x5)  =  U9_AGAA(x2, x5)
U10_AGAA(x1, x2, x3, x4, x5)  =  U10_AGAA(x1, x2, x5)
U22_GAA(x1, x2, x3, x4, x5, x6)  =  U22_GAA(x1, x6)
P68_IN_AGAA(x1, x2, x3, x4)  =  P68_IN_AGAA(x2)
U11_AGAA(x1, x2, x3, x4)  =  U11_AGAA(x1, x4)
U23_GAA(x1, x2, x3, x4, x5)  =  U23_GAA(x5)
U24_GAA(x1, x2, x3, x4, x5, x6)  =  U24_GAA(x1, x6)
U25_GAA(x1, x2, x3, x4, x5, x6)  =  U25_GAA(x1, x6)
U12_AGAA(x1, x2, x3, x4, x5)  =  U12_AGAA(x2, x5)
U26_GAA(x1, x2, x3, x4, x5)  =  U26_GAA(x1, x5)
U27_GAA(x1, x2, x3, x4, x5, x6)  =  U27_GAA(x1, x6)
U28_GAA(x1, x2, x3, x4, x5)  =  U28_GAA(x5)
U29_GAA(x1, x2, x3, x4, x5, x6)  =  U29_GAA(x1, x6)
U30_GAA(x1, x2, x3, x4, x5, x6)  =  U30_GAA(x1, x6)
U31_GAA(x1, x2, x3, x4, x5)  =  U31_GAA(x1, x5)
U32_GAA(x1, x2, x3, x4, x5, x6)  =  U32_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:

INSERT1_IN_GAA(0, tree(s(T29), T30, T20), tree(s(T29), T31, T20)) → U13_GAA(T29, T30, T20, T31, insert1_in_gaa(0, T30, T31))
INSERT1_IN_GAA(0, tree(s(T29), T30, T20), tree(s(T29), T31, T20)) → INSERT1_IN_GAA(0, T30, T31)
INSERT1_IN_GAA(s(T40), tree(s(T42), T43, T20), tree(s(T42), T44, T20)) → U14_GAA(T40, T42, T43, T20, T44, p18_in_gaaa(T40, T42, T43, T44))
INSERT1_IN_GAA(s(T40), tree(s(T42), T43, T20), tree(s(T42), T44, T20)) → P18_IN_GAAA(T40, T42, T43, T44)
P18_IN_GAAA(T40, T42, T43, T44) → U3_GAAA(T40, T42, T43, T44, less20_in_ga(T40, T42))
P18_IN_GAAA(T40, T42, T43, T44) → LESS20_IN_GA(T40, T42)
LESS20_IN_GA(s(T60), s(T62)) → U1_GA(T60, T62, less20_in_ga(T60, T62))
LESS20_IN_GA(s(T60), s(T62)) → LESS20_IN_GA(T60, T62)
P18_IN_GAAA(T40, T42, T47, T48) → U4_GAAA(T40, T42, T47, T48, lessc20_in_ga(T40, T42))
U4_GAAA(T40, T42, T47, T48, lessc20_out_ga(T40, T42)) → U5_GAAA(T40, T42, T47, T48, insert1_in_gaa(s(T40), T47, T48))
U4_GAAA(T40, T42, T47, T48, lessc20_out_ga(T40, T42)) → INSERT1_IN_GAA(s(T40), T47, T48)
INSERT1_IN_GAA(T77, tree(T82, T79, T83), tree(T82, T79, T84)) → U15_GAA(T77, T82, T79, T83, T84, less33_in_ag(T82, T77))
INSERT1_IN_GAA(T77, tree(T82, T79, T83), tree(T82, T79, T84)) → LESS33_IN_AG(T82, T77)
LESS33_IN_AG(s(T102), s(T101)) → U2_AG(T102, T101, less33_in_ag(T102, T101))
LESS33_IN_AG(s(T102), s(T101)) → LESS33_IN_AG(T102, T101)
INSERT1_IN_GAA(T77, tree(T82, T79, T87), tree(T82, T79, T88)) → U16_GAA(T77, T82, T79, T87, T88, lessc33_in_ag(T82, T77))
U16_GAA(T77, T82, T79, T87, T88, lessc33_out_ag(T82, T77)) → U17_GAA(T77, T82, T79, T87, T88, insert1_in_gaa(T77, T87, T88))
U16_GAA(T77, T82, T79, T87, T88, lessc33_out_ag(T82, T77)) → INSERT1_IN_GAA(T77, T87, T88)
INSERT1_IN_GAA(T112, tree(T117, T114, T118), tree(T117, T114, T119)) → U18_GAA(T112, T117, T114, T118, T119, p43_in_agaa(T117, T112, T118, T119))
INSERT1_IN_GAA(T112, tree(T117, T114, T118), tree(T117, T114, T119)) → P43_IN_AGAA(T117, T112, T118, T119)
P43_IN_AGAA(0, s(T124), T125, T126) → U6_AGAA(T124, T125, T126, insert1_in_gaa(s(T124), T125, T126))
P43_IN_AGAA(0, s(T124), T125, T126) → INSERT1_IN_GAA(s(T124), T125, T126)
INSERT1_IN_GAA(0, tree(s(T163), T164, T154), tree(s(T163), T165, T154)) → U19_GAA(T163, T164, T154, T165, insert1_in_gaa(0, T164, T165))
INSERT1_IN_GAA(s(T174), tree(s(T176), T177, T154), tree(s(T176), T178, T154)) → U20_GAA(T174, T176, T177, T154, T178, p18_in_gaaa(T174, T176, T177, T178))
INSERT1_IN_GAA(T191, tree(T196, T193, T197), tree(T196, T193, T198)) → U21_GAA(T191, T196, T193, T197, T198, p43_in_agaa(T196, T191, T197, T198))
P43_IN_AGAA(s(T135), s(T134), T136, T137) → U7_AGAA(T135, T134, T136, T137, p50_in_agaa(T135, T134, T136, T137))
P43_IN_AGAA(s(T135), s(T134), T136, T137) → P50_IN_AGAA(T135, T134, T136, T137)
P50_IN_AGAA(T135, T134, T136, T137) → U8_AGAA(T135, T134, T136, T137, less33_in_ag(T135, T134))
P50_IN_AGAA(T135, T134, T136, T137) → LESS33_IN_AG(T135, T134)
P50_IN_AGAA(T135, T134, T140, T141) → U9_AGAA(T135, T134, T140, T141, lessc33_in_ag(T135, T134))
U9_AGAA(T135, T134, T140, T141, lessc33_out_ag(T135, T134)) → U10_AGAA(T135, T134, T140, T141, insert1_in_gaa(s(T134), T140, T141))
U9_AGAA(T135, T134, T140, T141, lessc33_out_ag(T135, T134)) → INSERT1_IN_GAA(s(T134), T140, T141)
INSERT1_IN_GAA(T206, tree(T211, T208, T212), tree(T211, T208, T213)) → U22_GAA(T206, T211, T208, T212, T213, p68_in_agaa(T211, T206, T212, T213))
INSERT1_IN_GAA(T206, tree(T211, T208, T212), tree(T211, T208, T213)) → P68_IN_AGAA(T211, T206, T212, T213)
P68_IN_AGAA(0, s(T218), T219, T220) → U11_AGAA(T218, T219, T220, insert1_in_gaa(s(T218), T219, T220))
P68_IN_AGAA(0, s(T218), T219, T220) → INSERT1_IN_GAA(s(T218), T219, T220)
INSERT1_IN_GAA(0, tree(s(T257), T258, T248), tree(s(T257), T259, T248)) → U23_GAA(T257, T258, T248, T259, insert1_in_gaa(0, T258, T259))
INSERT1_IN_GAA(s(T268), tree(s(T270), T271, T248), tree(s(T270), T272, T248)) → U24_GAA(T268, T270, T271, T248, T272, p18_in_gaaa(T268, T270, T271, T272))
INSERT1_IN_GAA(T285, tree(T290, T287, T291), tree(T290, T287, T292)) → U25_GAA(T285, T290, T287, T291, T292, p68_in_agaa(T290, T285, T291, T292))
P68_IN_AGAA(s(T229), s(T228), T230, T231) → U12_AGAA(T229, T228, T230, T231, p50_in_agaa(T229, T228, T230, T231))
P68_IN_AGAA(s(T229), s(T228), T230, T231) → P50_IN_AGAA(T229, T228, T230, T231)
INSERT1_IN_GAA(s(T312), tree(0, T302, T313), tree(0, T302, T314)) → U26_GAA(T312, T302, T313, T314, insert1_in_gaa(s(T312), T313, T314))
INSERT1_IN_GAA(s(T312), tree(0, T302, T313), tree(0, T302, T314)) → INSERT1_IN_GAA(s(T312), T313, T314)
INSERT1_IN_GAA(s(T322), tree(s(T323), T302, T324), tree(s(T323), T302, T325)) → U27_GAA(T322, T323, T302, T324, T325, p50_in_agaa(T323, T322, T324, T325))
INSERT1_IN_GAA(s(T322), tree(s(T323), T302, T324), tree(s(T323), T302, T325)) → P50_IN_AGAA(T323, T322, T324, T325)
INSERT1_IN_GAA(0, tree(s(T345), T346, T336), tree(s(T345), T347, T336)) → U28_GAA(T345, T346, T336, T347, insert1_in_gaa(0, T346, T347))
INSERT1_IN_GAA(s(T356), tree(s(T358), T359, T336), tree(s(T358), T360, T336)) → U29_GAA(T356, T358, T359, T336, T360, p18_in_gaaa(T356, T358, T359, T360))
INSERT1_IN_GAA(T373, tree(T378, T375, T379), tree(T378, T375, T380)) → U30_GAA(T373, T378, T375, T379, T380, p68_in_agaa(T378, T373, T379, T380))
INSERT1_IN_GAA(s(T400), tree(0, T390, T401), tree(0, T390, T402)) → U31_GAA(T400, T390, T401, T402, insert1_in_gaa(s(T400), T401, T402))
INSERT1_IN_GAA(s(T410), tree(s(T411), T390, T412), tree(s(T411), T390, T413)) → U32_GAA(T410, T411, T390, T412, T413, p50_in_agaa(T411, T410, T412, T413))

The TRS R consists of the following rules:

lessc20_in_ga(0, s(T55)) → lessc20_out_ga(0, s(T55))
lessc20_in_ga(s(T60), s(T62)) → U53_ga(T60, T62, lessc20_in_ga(T60, T62))
U53_ga(T60, T62, lessc20_out_ga(T60, T62)) → lessc20_out_ga(s(T60), s(T62))
lessc33_in_ag(0, s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T102), s(T101)) → U54_ag(T102, T101, lessc33_in_ag(T102, T101))
U54_ag(T102, T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The argument filtering Pi contains the following mapping:
insert1_in_gaa(x1, x2, x3)  =  insert1_in_gaa(x1)
0  =  0
s(x1)  =  s(x1)
p18_in_gaaa(x1, x2, x3, x4)  =  p18_in_gaaa(x1)
less20_in_ga(x1, x2)  =  less20_in_ga(x1)
lessc20_in_ga(x1, x2)  =  lessc20_in_ga(x1)
lessc20_out_ga(x1, x2)  =  lessc20_out_ga(x1)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
less33_in_ag(x1, x2)  =  less33_in_ag(x2)
lessc33_in_ag(x1, x2)  =  lessc33_in_ag(x2)
lessc33_out_ag(x1, x2)  =  lessc33_out_ag(x1, x2)
U54_ag(x1, x2, x3)  =  U54_ag(x2, x3)
p43_in_agaa(x1, x2, x3, x4)  =  p43_in_agaa(x2)
p50_in_agaa(x1, x2, x3, x4)  =  p50_in_agaa(x2)
p68_in_agaa(x1, x2, x3, x4)  =  p68_in_agaa(x2)
INSERT1_IN_GAA(x1, x2, x3)  =  INSERT1_IN_GAA(x1)
U13_GAA(x1, x2, x3, x4, x5)  =  U13_GAA(x5)
U14_GAA(x1, x2, x3, x4, x5, x6)  =  U14_GAA(x1, x6)
P18_IN_GAAA(x1, x2, x3, x4)  =  P18_IN_GAAA(x1)
U3_GAAA(x1, x2, x3, x4, x5)  =  U3_GAAA(x1, x5)
LESS20_IN_GA(x1, x2)  =  LESS20_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U4_GAAA(x1, x2, x3, x4, x5)  =  U4_GAAA(x1, x5)
U5_GAAA(x1, x2, x3, x4, x5)  =  U5_GAAA(x1, x5)
U15_GAA(x1, x2, x3, x4, x5, x6)  =  U15_GAA(x1, x6)
LESS33_IN_AG(x1, x2)  =  LESS33_IN_AG(x2)
U2_AG(x1, x2, x3)  =  U2_AG(x2, x3)
U16_GAA(x1, x2, x3, x4, x5, x6)  =  U16_GAA(x1, x6)
U17_GAA(x1, x2, x3, x4, x5, x6)  =  U17_GAA(x1, x6)
U18_GAA(x1, x2, x3, x4, x5, x6)  =  U18_GAA(x1, x6)
P43_IN_AGAA(x1, x2, x3, x4)  =  P43_IN_AGAA(x2)
U6_AGAA(x1, x2, x3, x4)  =  U6_AGAA(x1, x4)
U19_GAA(x1, x2, x3, x4, x5)  =  U19_GAA(x5)
U20_GAA(x1, x2, x3, x4, x5, x6)  =  U20_GAA(x1, x6)
U21_GAA(x1, x2, x3, x4, x5, x6)  =  U21_GAA(x1, x6)
U7_AGAA(x1, x2, x3, x4, x5)  =  U7_AGAA(x2, x5)
P50_IN_AGAA(x1, x2, x3, x4)  =  P50_IN_AGAA(x2)
U8_AGAA(x1, x2, x3, x4, x5)  =  U8_AGAA(x2, x5)
U9_AGAA(x1, x2, x3, x4, x5)  =  U9_AGAA(x2, x5)
U10_AGAA(x1, x2, x3, x4, x5)  =  U10_AGAA(x1, x2, x5)
U22_GAA(x1, x2, x3, x4, x5, x6)  =  U22_GAA(x1, x6)
P68_IN_AGAA(x1, x2, x3, x4)  =  P68_IN_AGAA(x2)
U11_AGAA(x1, x2, x3, x4)  =  U11_AGAA(x1, x4)
U23_GAA(x1, x2, x3, x4, x5)  =  U23_GAA(x5)
U24_GAA(x1, x2, x3, x4, x5, x6)  =  U24_GAA(x1, x6)
U25_GAA(x1, x2, x3, x4, x5, x6)  =  U25_GAA(x1, x6)
U12_AGAA(x1, x2, x3, x4, x5)  =  U12_AGAA(x2, x5)
U26_GAA(x1, x2, x3, x4, x5)  =  U26_GAA(x1, x5)
U27_GAA(x1, x2, x3, x4, x5, x6)  =  U27_GAA(x1, x6)
U28_GAA(x1, x2, x3, x4, x5)  =  U28_GAA(x5)
U29_GAA(x1, x2, x3, x4, x5, x6)  =  U29_GAA(x1, x6)
U30_GAA(x1, x2, x3, x4, x5, x6)  =  U30_GAA(x1, x6)
U31_GAA(x1, x2, x3, x4, x5)  =  U31_GAA(x1, x5)
U32_GAA(x1, x2, x3, x4, x5, x6)  =  U32_GAA(x1, x6)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

LESS33_IN_AG(s(T102), s(T101)) → LESS33_IN_AG(T102, T101)

The TRS R consists of the following rules:

lessc20_in_ga(0, s(T55)) → lessc20_out_ga(0, s(T55))
lessc20_in_ga(s(T60), s(T62)) → U53_ga(T60, T62, lessc20_in_ga(T60, T62))
U53_ga(T60, T62, lessc20_out_ga(T60, T62)) → lessc20_out_ga(s(T60), s(T62))
lessc33_in_ag(0, s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T102), s(T101)) → U54_ag(T102, T101, lessc33_in_ag(T102, T101))
U54_ag(T102, T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
lessc20_in_ga(x1, x2)  =  lessc20_in_ga(x1)
lessc20_out_ga(x1, x2)  =  lessc20_out_ga(x1)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
lessc33_in_ag(x1, x2)  =  lessc33_in_ag(x2)
lessc33_out_ag(x1, x2)  =  lessc33_out_ag(x1, x2)
U54_ag(x1, x2, x3)  =  U54_ag(x2, x3)
LESS33_IN_AG(x1, x2)  =  LESS33_IN_AG(x2)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

LESS33_IN_AG(s(T102), s(T101)) → LESS33_IN_AG(T102, T101)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LESS33_IN_AG(x1, x2)  =  LESS33_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:

LESS33_IN_AG(s(T101)) → LESS33_IN_AG(T101)

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:

• LESS33_IN_AG(s(T101)) → LESS33_IN_AG(T101)
  The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

LESS20_IN_GA(s(T60), s(T62)) → LESS20_IN_GA(T60, T62)

The TRS R consists of the following rules:

lessc20_in_ga(0, s(T55)) → lessc20_out_ga(0, s(T55))
lessc20_in_ga(s(T60), s(T62)) → U53_ga(T60, T62, lessc20_in_ga(T60, T62))
U53_ga(T60, T62, lessc20_out_ga(T60, T62)) → lessc20_out_ga(s(T60), s(T62))
lessc33_in_ag(0, s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T102), s(T101)) → U54_ag(T102, T101, lessc33_in_ag(T102, T101))
U54_ag(T102, T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
lessc20_in_ga(x1, x2)  =  lessc20_in_ga(x1)
lessc20_out_ga(x1, x2)  =  lessc20_out_ga(x1)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
lessc33_in_ag(x1, x2)  =  lessc33_in_ag(x2)
lessc33_out_ag(x1, x2)  =  lessc33_out_ag(x1, x2)
U54_ag(x1, x2, x3)  =  U54_ag(x2, x3)
LESS20_IN_GA(x1, x2)  =  LESS20_IN_GA(x1)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

LESS20_IN_GA(s(T60), s(T62)) → LESS20_IN_GA(T60, T62)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LESS20_IN_GA(x1, x2)  =  LESS20_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:

LESS20_IN_GA(s(T60)) → LESS20_IN_GA(T60)

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:

• LESS20_IN_GA(s(T60)) → LESS20_IN_GA(T60)
  The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

INSERT1_IN_GAA(T77, tree(T82, T79, T87), tree(T82, T79, T88)) → U16_GAA(T77, T82, T79, T87, T88, lessc33_in_ag(T82, T77))
U16_GAA(T77, T82, T79, T87, T88, lessc33_out_ag(T82, T77)) → INSERT1_IN_GAA(T77, T87, T88)
INSERT1_IN_GAA(0, tree(s(T29), T30, T20), tree(s(T29), T31, T20)) → INSERT1_IN_GAA(0, T30, T31)
INSERT1_IN_GAA(T112, tree(T117, T114, T118), tree(T117, T114, T119)) → P43_IN_AGAA(T117, T112, T118, T119)
P43_IN_AGAA(0, s(T124), T125, T126) → INSERT1_IN_GAA(s(T124), T125, T126)
INSERT1_IN_GAA(s(T40), tree(s(T42), T43, T20), tree(s(T42), T44, T20)) → P18_IN_GAAA(T40, T42, T43, T44)
P18_IN_GAAA(T40, T42, T47, T48) → U4_GAAA(T40, T42, T47, T48, lessc20_in_ga(T40, T42))
U4_GAAA(T40, T42, T47, T48, lessc20_out_ga(T40, T42)) → INSERT1_IN_GAA(s(T40), T47, T48)
INSERT1_IN_GAA(T206, tree(T211, T208, T212), tree(T211, T208, T213)) → P68_IN_AGAA(T211, T206, T212, T213)
P68_IN_AGAA(0, s(T218), T219, T220) → INSERT1_IN_GAA(s(T218), T219, T220)
INSERT1_IN_GAA(s(T312), tree(0, T302, T313), tree(0, T302, T314)) → INSERT1_IN_GAA(s(T312), T313, T314)
INSERT1_IN_GAA(s(T322), tree(s(T323), T302, T324), tree(s(T323), T302, T325)) → P50_IN_AGAA(T323, T322, T324, T325)
P50_IN_AGAA(T135, T134, T140, T141) → U9_AGAA(T135, T134, T140, T141, lessc33_in_ag(T135, T134))
U9_AGAA(T135, T134, T140, T141, lessc33_out_ag(T135, T134)) → INSERT1_IN_GAA(s(T134), T140, T141)
P68_IN_AGAA(s(T229), s(T228), T230, T231) → P50_IN_AGAA(T229, T228, T230, T231)
P43_IN_AGAA(s(T135), s(T134), T136, T137) → P50_IN_AGAA(T135, T134, T136, T137)

The TRS R consists of the following rules:

lessc20_in_ga(0, s(T55)) → lessc20_out_ga(0, s(T55))
lessc20_in_ga(s(T60), s(T62)) → U53_ga(T60, T62, lessc20_in_ga(T60, T62))
U53_ga(T60, T62, lessc20_out_ga(T60, T62)) → lessc20_out_ga(s(T60), s(T62))
lessc33_in_ag(0, s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T102), s(T101)) → U54_ag(T102, T101, lessc33_in_ag(T102, T101))
U54_ag(T102, T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
lessc20_in_ga(x1, x2)  =  lessc20_in_ga(x1)
lessc20_out_ga(x1, x2)  =  lessc20_out_ga(x1)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
lessc33_in_ag(x1, x2)  =  lessc33_in_ag(x2)
lessc33_out_ag(x1, x2)  =  lessc33_out_ag(x1, x2)
U54_ag(x1, x2, x3)  =  U54_ag(x2, x3)
INSERT1_IN_GAA(x1, x2, x3)  =  INSERT1_IN_GAA(x1)
P18_IN_GAAA(x1, x2, x3, x4)  =  P18_IN_GAAA(x1)
U4_GAAA(x1, x2, x3, x4, x5)  =  U4_GAAA(x1, x5)
U16_GAA(x1, x2, x3, x4, x5, x6)  =  U16_GAA(x1, x6)
P43_IN_AGAA(x1, x2, x3, x4)  =  P43_IN_AGAA(x2)
P50_IN_AGAA(x1, x2, x3, x4)  =  P50_IN_AGAA(x2)
U9_AGAA(x1, x2, x3, x4, x5)  =  U9_AGAA(x2, x5)
P68_IN_AGAA(x1, x2, x3, x4)  =  P68_IN_AGAA(x2)

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

(22) PiDPToQDPProof (SOUND transformation)

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

(23) Obligation:

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

INSERT1_IN_GAA(T77) → U16_GAA(T77, lessc33_in_ag(T77))
U16_GAA(T77, lessc33_out_ag(T82, T77)) → INSERT1_IN_GAA(T77)
INSERT1_IN_GAA(0) → INSERT1_IN_GAA(0)
INSERT1_IN_GAA(T112) → P43_IN_AGAA(T112)
P43_IN_AGAA(s(T124)) → INSERT1_IN_GAA(s(T124))
INSERT1_IN_GAA(s(T40)) → P18_IN_GAAA(T40)
P18_IN_GAAA(T40) → U4_GAAA(T40, lessc20_in_ga(T40))
U4_GAAA(T40, lessc20_out_ga(T40)) → INSERT1_IN_GAA(s(T40))
INSERT1_IN_GAA(T206) → P68_IN_AGAA(T206)
P68_IN_AGAA(s(T218)) → INSERT1_IN_GAA(s(T218))
INSERT1_IN_GAA(s(T312)) → INSERT1_IN_GAA(s(T312))
INSERT1_IN_GAA(s(T322)) → P50_IN_AGAA(T322)
P50_IN_AGAA(T134) → U9_AGAA(T134, lessc33_in_ag(T134))
U9_AGAA(T134, lessc33_out_ag(T135, T134)) → INSERT1_IN_GAA(s(T134))
P68_IN_AGAA(s(T228)) → P50_IN_AGAA(T228)
P43_IN_AGAA(s(T134)) → P50_IN_AGAA(T134)

The TRS R consists of the following rules:

lessc20_in_ga(0) → lessc20_out_ga(0)
lessc20_in_ga(s(T60)) → U53_ga(T60, lessc20_in_ga(T60))
U53_ga(T60, lessc20_out_ga(T60)) → lessc20_out_ga(s(T60))
lessc33_in_ag(s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T101)) → U54_ag(T101, lessc33_in_ag(T101))
U54_ag(T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The set Q consists of the following terms:

lessc20_in_ga(x0)
U53_ga(x0, x1)
lessc33_in_ag(x0)
U54_ag(x0, x1)

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

(24) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule INSERT1_IN_GAA(T77) → U16_GAA(T77, lessc33_in_ag(T77)) at position [1] we obtained the following new rules [LPAR04]:

INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), lessc33_out_ag(0, s(x0)))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))

(25) Obligation:

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

U16_GAA(T77, lessc33_out_ag(T82, T77)) → INSERT1_IN_GAA(T77)
INSERT1_IN_GAA(0) → INSERT1_IN_GAA(0)
INSERT1_IN_GAA(T112) → P43_IN_AGAA(T112)
P43_IN_AGAA(s(T124)) → INSERT1_IN_GAA(s(T124))
INSERT1_IN_GAA(s(T40)) → P18_IN_GAAA(T40)
P18_IN_GAAA(T40) → U4_GAAA(T40, lessc20_in_ga(T40))
U4_GAAA(T40, lessc20_out_ga(T40)) → INSERT1_IN_GAA(s(T40))
INSERT1_IN_GAA(T206) → P68_IN_AGAA(T206)
P68_IN_AGAA(s(T218)) → INSERT1_IN_GAA(s(T218))
INSERT1_IN_GAA(s(T312)) → INSERT1_IN_GAA(s(T312))
INSERT1_IN_GAA(s(T322)) → P50_IN_AGAA(T322)
P50_IN_AGAA(T134) → U9_AGAA(T134, lessc33_in_ag(T134))
U9_AGAA(T134, lessc33_out_ag(T135, T134)) → INSERT1_IN_GAA(s(T134))
P68_IN_AGAA(s(T228)) → P50_IN_AGAA(T228)
P43_IN_AGAA(s(T134)) → P50_IN_AGAA(T134)
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), lessc33_out_ag(0, s(x0)))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))

The TRS R consists of the following rules:

lessc20_in_ga(0) → lessc20_out_ga(0)
lessc20_in_ga(s(T60)) → U53_ga(T60, lessc20_in_ga(T60))
U53_ga(T60, lessc20_out_ga(T60)) → lessc20_out_ga(s(T60))
lessc33_in_ag(s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T101)) → U54_ag(T101, lessc33_in_ag(T101))
U54_ag(T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The set Q consists of the following terms:

lessc20_in_ga(x0)
U53_ga(x0, x1)
lessc33_in_ag(x0)
U54_ag(x0, x1)

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

(26) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P18_IN_GAAA(T40) → U4_GAAA(T40, lessc20_in_ga(T40)) at position [1] we obtained the following new rules [LPAR04]:

P18_IN_GAAA(0) → U4_GAAA(0, lessc20_out_ga(0))
P18_IN_GAAA(s(x0)) → U4_GAAA(s(x0), U53_ga(x0, lessc20_in_ga(x0)))

(27) Obligation:

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

U16_GAA(T77, lessc33_out_ag(T82, T77)) → INSERT1_IN_GAA(T77)
INSERT1_IN_GAA(0) → INSERT1_IN_GAA(0)
INSERT1_IN_GAA(T112) → P43_IN_AGAA(T112)
P43_IN_AGAA(s(T124)) → INSERT1_IN_GAA(s(T124))
INSERT1_IN_GAA(s(T40)) → P18_IN_GAAA(T40)
U4_GAAA(T40, lessc20_out_ga(T40)) → INSERT1_IN_GAA(s(T40))
INSERT1_IN_GAA(T206) → P68_IN_AGAA(T206)
P68_IN_AGAA(s(T218)) → INSERT1_IN_GAA(s(T218))
INSERT1_IN_GAA(s(T312)) → INSERT1_IN_GAA(s(T312))
INSERT1_IN_GAA(s(T322)) → P50_IN_AGAA(T322)
P50_IN_AGAA(T134) → U9_AGAA(T134, lessc33_in_ag(T134))
U9_AGAA(T134, lessc33_out_ag(T135, T134)) → INSERT1_IN_GAA(s(T134))
P68_IN_AGAA(s(T228)) → P50_IN_AGAA(T228)
P43_IN_AGAA(s(T134)) → P50_IN_AGAA(T134)
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), lessc33_out_ag(0, s(x0)))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
P18_IN_GAAA(0) → U4_GAAA(0, lessc20_out_ga(0))
P18_IN_GAAA(s(x0)) → U4_GAAA(s(x0), U53_ga(x0, lessc20_in_ga(x0)))

The TRS R consists of the following rules:

lessc20_in_ga(0) → lessc20_out_ga(0)
lessc20_in_ga(s(T60)) → U53_ga(T60, lessc20_in_ga(T60))
U53_ga(T60, lessc20_out_ga(T60)) → lessc20_out_ga(s(T60))
lessc33_in_ag(s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T101)) → U54_ag(T101, lessc33_in_ag(T101))
U54_ag(T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The set Q consists of the following terms:

lessc20_in_ga(x0)
U53_ga(x0, x1)
lessc33_in_ag(x0)
U54_ag(x0, x1)

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

(28) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P50_IN_AGAA(T134) → U9_AGAA(T134, lessc33_in_ag(T134)) at position [1] we obtained the following new rules [LPAR04]:

P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), lessc33_out_ag(0, s(x0)))
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))

(29) Obligation:

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

U16_GAA(T77, lessc33_out_ag(T82, T77)) → INSERT1_IN_GAA(T77)
INSERT1_IN_GAA(0) → INSERT1_IN_GAA(0)
INSERT1_IN_GAA(T112) → P43_IN_AGAA(T112)
P43_IN_AGAA(s(T124)) → INSERT1_IN_GAA(s(T124))
INSERT1_IN_GAA(s(T40)) → P18_IN_GAAA(T40)
U4_GAAA(T40, lessc20_out_ga(T40)) → INSERT1_IN_GAA(s(T40))
INSERT1_IN_GAA(T206) → P68_IN_AGAA(T206)
P68_IN_AGAA(s(T218)) → INSERT1_IN_GAA(s(T218))
INSERT1_IN_GAA(s(T312)) → INSERT1_IN_GAA(s(T312))
INSERT1_IN_GAA(s(T322)) → P50_IN_AGAA(T322)
U9_AGAA(T134, lessc33_out_ag(T135, T134)) → INSERT1_IN_GAA(s(T134))
P68_IN_AGAA(s(T228)) → P50_IN_AGAA(T228)
P43_IN_AGAA(s(T134)) → P50_IN_AGAA(T134)
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), lessc33_out_ag(0, s(x0)))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
P18_IN_GAAA(0) → U4_GAAA(0, lessc20_out_ga(0))
P18_IN_GAAA(s(x0)) → U4_GAAA(s(x0), U53_ga(x0, lessc20_in_ga(x0)))
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), lessc33_out_ag(0, s(x0)))
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))

The TRS R consists of the following rules:

lessc20_in_ga(0) → lessc20_out_ga(0)
lessc20_in_ga(s(T60)) → U53_ga(T60, lessc20_in_ga(T60))
U53_ga(T60, lessc20_out_ga(T60)) → lessc20_out_ga(s(T60))
lessc33_in_ag(s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T101)) → U54_ag(T101, lessc33_in_ag(T101))
U54_ag(T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The set Q consists of the following terms:

lessc20_in_ga(x0)
U53_ga(x0, x1)
lessc33_in_ag(x0)
U54_ag(x0, x1)

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

(30) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U16_GAA(T77, lessc33_out_ag(T82, T77)) → INSERT1_IN_GAA(T77) we obtained the following new rules [LPAR04]:

U16_GAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(z0))
U16_GAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(z0))

(31) Obligation:

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

INSERT1_IN_GAA(0) → INSERT1_IN_GAA(0)
INSERT1_IN_GAA(T112) → P43_IN_AGAA(T112)
P43_IN_AGAA(s(T124)) → INSERT1_IN_GAA(s(T124))
INSERT1_IN_GAA(s(T40)) → P18_IN_GAAA(T40)
U4_GAAA(T40, lessc20_out_ga(T40)) → INSERT1_IN_GAA(s(T40))
INSERT1_IN_GAA(T206) → P68_IN_AGAA(T206)
P68_IN_AGAA(s(T218)) → INSERT1_IN_GAA(s(T218))
INSERT1_IN_GAA(s(T312)) → INSERT1_IN_GAA(s(T312))
INSERT1_IN_GAA(s(T322)) → P50_IN_AGAA(T322)
U9_AGAA(T134, lessc33_out_ag(T135, T134)) → INSERT1_IN_GAA(s(T134))
P68_IN_AGAA(s(T228)) → P50_IN_AGAA(T228)
P43_IN_AGAA(s(T134)) → P50_IN_AGAA(T134)
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), lessc33_out_ag(0, s(x0)))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
P18_IN_GAAA(0) → U4_GAAA(0, lessc20_out_ga(0))
P18_IN_GAAA(s(x0)) → U4_GAAA(s(x0), U53_ga(x0, lessc20_in_ga(x0)))
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), lessc33_out_ag(0, s(x0)))
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
U16_GAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(z0))
U16_GAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(z0))

The TRS R consists of the following rules:

lessc20_in_ga(0) → lessc20_out_ga(0)
lessc20_in_ga(s(T60)) → U53_ga(T60, lessc20_in_ga(T60))
U53_ga(T60, lessc20_out_ga(T60)) → lessc20_out_ga(s(T60))
lessc33_in_ag(s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T101)) → U54_ag(T101, lessc33_in_ag(T101))
U54_ag(T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The set Q consists of the following terms:

lessc20_in_ga(x0)
U53_ga(x0, x1)
lessc33_in_ag(x0)
U54_ag(x0, x1)

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

(32) DependencyGraphProof (EQUIVALENT transformation)

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

(33) Complex Obligation (AND)

(34) Obligation:

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

P43_IN_AGAA(s(T124)) → INSERT1_IN_GAA(s(T124))
INSERT1_IN_GAA(T112) → P43_IN_AGAA(T112)
P43_IN_AGAA(s(T134)) → P50_IN_AGAA(T134)
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), lessc33_out_ag(0, s(x0)))
U9_AGAA(T134, lessc33_out_ag(T135, T134)) → INSERT1_IN_GAA(s(T134))
INSERT1_IN_GAA(s(T40)) → P18_IN_GAAA(T40)
P18_IN_GAAA(0) → U4_GAAA(0, lessc20_out_ga(0))
U4_GAAA(T40, lessc20_out_ga(T40)) → INSERT1_IN_GAA(s(T40))
INSERT1_IN_GAA(T206) → P68_IN_AGAA(T206)
P68_IN_AGAA(s(T218)) → INSERT1_IN_GAA(s(T218))
INSERT1_IN_GAA(s(T312)) → INSERT1_IN_GAA(s(T312))
INSERT1_IN_GAA(s(T322)) → P50_IN_AGAA(T322)
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), lessc33_out_ag(0, s(x0)))
U16_GAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(z0))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
U16_GAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(z0))
P68_IN_AGAA(s(T228)) → P50_IN_AGAA(T228)
P18_IN_GAAA(s(x0)) → U4_GAAA(s(x0), U53_ga(x0, lessc20_in_ga(x0)))

The TRS R consists of the following rules:

lessc20_in_ga(0) → lessc20_out_ga(0)
lessc20_in_ga(s(T60)) → U53_ga(T60, lessc20_in_ga(T60))
U53_ga(T60, lessc20_out_ga(T60)) → lessc20_out_ga(s(T60))
lessc33_in_ag(s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T101)) → U54_ag(T101, lessc33_in_ag(T101))
U54_ag(T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The set Q consists of the following terms:

lessc20_in_ga(x0)
U53_ga(x0, x1)
lessc33_in_ag(x0)
U54_ag(x0, x1)

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

(35) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule INSERT1_IN_GAA(T112) → P43_IN_AGAA(T112) we obtained the following new rules [LPAR04]:

INSERT1_IN_GAA(s(z0)) → P43_IN_AGAA(s(z0))

(36) Obligation:

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

P43_IN_AGAA(s(T124)) → INSERT1_IN_GAA(s(T124))
P43_IN_AGAA(s(T134)) → P50_IN_AGAA(T134)
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), lessc33_out_ag(0, s(x0)))
U9_AGAA(T134, lessc33_out_ag(T135, T134)) → INSERT1_IN_GAA(s(T134))
INSERT1_IN_GAA(s(T40)) → P18_IN_GAAA(T40)
P18_IN_GAAA(0) → U4_GAAA(0, lessc20_out_ga(0))
U4_GAAA(T40, lessc20_out_ga(T40)) → INSERT1_IN_GAA(s(T40))
INSERT1_IN_GAA(T206) → P68_IN_AGAA(T206)
P68_IN_AGAA(s(T218)) → INSERT1_IN_GAA(s(T218))
INSERT1_IN_GAA(s(T312)) → INSERT1_IN_GAA(s(T312))
INSERT1_IN_GAA(s(T322)) → P50_IN_AGAA(T322)
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), lessc33_out_ag(0, s(x0)))
U16_GAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(z0))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
U16_GAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(z0))
P68_IN_AGAA(s(T228)) → P50_IN_AGAA(T228)
P18_IN_GAAA(s(x0)) → U4_GAAA(s(x0), U53_ga(x0, lessc20_in_ga(x0)))
INSERT1_IN_GAA(s(z0)) → P43_IN_AGAA(s(z0))

The TRS R consists of the following rules:

lessc20_in_ga(0) → lessc20_out_ga(0)
lessc20_in_ga(s(T60)) → U53_ga(T60, lessc20_in_ga(T60))
U53_ga(T60, lessc20_out_ga(T60)) → lessc20_out_ga(s(T60))
lessc33_in_ag(s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T101)) → U54_ag(T101, lessc33_in_ag(T101))
U54_ag(T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The set Q consists of the following terms:

lessc20_in_ga(x0)
U53_ga(x0, x1)
lessc33_in_ag(x0)
U54_ag(x0, x1)

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

(37) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U9_AGAA(T134, lessc33_out_ag(T135, T134)) → INSERT1_IN_GAA(s(T134)) we obtained the following new rules [LPAR04]:

U9_AGAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(s(z0)))
U9_AGAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(s(z0)))

(38) Obligation:

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

P43_IN_AGAA(s(T124)) → INSERT1_IN_GAA(s(T124))
P43_IN_AGAA(s(T134)) → P50_IN_AGAA(T134)
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), lessc33_out_ag(0, s(x0)))
INSERT1_IN_GAA(s(T40)) → P18_IN_GAAA(T40)
P18_IN_GAAA(0) → U4_GAAA(0, lessc20_out_ga(0))
U4_GAAA(T40, lessc20_out_ga(T40)) → INSERT1_IN_GAA(s(T40))
INSERT1_IN_GAA(T206) → P68_IN_AGAA(T206)
P68_IN_AGAA(s(T218)) → INSERT1_IN_GAA(s(T218))
INSERT1_IN_GAA(s(T312)) → INSERT1_IN_GAA(s(T312))
INSERT1_IN_GAA(s(T322)) → P50_IN_AGAA(T322)
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), lessc33_out_ag(0, s(x0)))
U16_GAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(z0))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
U16_GAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(z0))
P68_IN_AGAA(s(T228)) → P50_IN_AGAA(T228)
P18_IN_GAAA(s(x0)) → U4_GAAA(s(x0), U53_ga(x0, lessc20_in_ga(x0)))
INSERT1_IN_GAA(s(z0)) → P43_IN_AGAA(s(z0))
U9_AGAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(s(z0)))
U9_AGAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(s(z0)))

The TRS R consists of the following rules:

lessc20_in_ga(0) → lessc20_out_ga(0)
lessc20_in_ga(s(T60)) → U53_ga(T60, lessc20_in_ga(T60))
U53_ga(T60, lessc20_out_ga(T60)) → lessc20_out_ga(s(T60))
lessc33_in_ag(s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T101)) → U54_ag(T101, lessc33_in_ag(T101))
U54_ag(T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The set Q consists of the following terms:

lessc20_in_ga(x0)
U53_ga(x0, x1)
lessc33_in_ag(x0)
U54_ag(x0, x1)

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

(39) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U4_GAAA(T40, lessc20_out_ga(T40)) → INSERT1_IN_GAA(s(T40)) we obtained the following new rules [LPAR04]:

U4_GAAA(0, lessc20_out_ga(0)) → INSERT1_IN_GAA(s(0))
U4_GAAA(s(z0), lessc20_out_ga(s(z0))) → INSERT1_IN_GAA(s(s(z0)))

(40) Obligation:

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

P43_IN_AGAA(s(T124)) → INSERT1_IN_GAA(s(T124))
P43_IN_AGAA(s(T134)) → P50_IN_AGAA(T134)
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), lessc33_out_ag(0, s(x0)))
INSERT1_IN_GAA(s(T40)) → P18_IN_GAAA(T40)
P18_IN_GAAA(0) → U4_GAAA(0, lessc20_out_ga(0))
INSERT1_IN_GAA(T206) → P68_IN_AGAA(T206)
P68_IN_AGAA(s(T218)) → INSERT1_IN_GAA(s(T218))
INSERT1_IN_GAA(s(T312)) → INSERT1_IN_GAA(s(T312))
INSERT1_IN_GAA(s(T322)) → P50_IN_AGAA(T322)
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), lessc33_out_ag(0, s(x0)))
U16_GAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(z0))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
U16_GAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(z0))
P68_IN_AGAA(s(T228)) → P50_IN_AGAA(T228)
P18_IN_GAAA(s(x0)) → U4_GAAA(s(x0), U53_ga(x0, lessc20_in_ga(x0)))
INSERT1_IN_GAA(s(z0)) → P43_IN_AGAA(s(z0))
U9_AGAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(s(z0)))
U9_AGAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(s(z0)))
U4_GAAA(0, lessc20_out_ga(0)) → INSERT1_IN_GAA(s(0))
U4_GAAA(s(z0), lessc20_out_ga(s(z0))) → INSERT1_IN_GAA(s(s(z0)))

The TRS R consists of the following rules:

lessc20_in_ga(0) → lessc20_out_ga(0)
lessc20_in_ga(s(T60)) → U53_ga(T60, lessc20_in_ga(T60))
U53_ga(T60, lessc20_out_ga(T60)) → lessc20_out_ga(s(T60))
lessc33_in_ag(s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T101)) → U54_ag(T101, lessc33_in_ag(T101))
U54_ag(T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The set Q consists of the following terms:

lessc20_in_ga(x0)
U53_ga(x0, x1)
lessc33_in_ag(x0)
U54_ag(x0, x1)

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

(41) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule INSERT1_IN_GAA(T206) → P68_IN_AGAA(T206) we obtained the following new rules [LPAR04]:

INSERT1_IN_GAA(s(z0)) → P68_IN_AGAA(s(z0))
INSERT1_IN_GAA(s(s(z0))) → P68_IN_AGAA(s(s(z0)))
INSERT1_IN_GAA(s(0)) → P68_IN_AGAA(s(0))

(42) Obligation:

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

P43_IN_AGAA(s(T124)) → INSERT1_IN_GAA(s(T124))
P43_IN_AGAA(s(T134)) → P50_IN_AGAA(T134)
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), lessc33_out_ag(0, s(x0)))
INSERT1_IN_GAA(s(T40)) → P18_IN_GAAA(T40)
P18_IN_GAAA(0) → U4_GAAA(0, lessc20_out_ga(0))
P68_IN_AGAA(s(T218)) → INSERT1_IN_GAA(s(T218))
INSERT1_IN_GAA(s(T312)) → INSERT1_IN_GAA(s(T312))
INSERT1_IN_GAA(s(T322)) → P50_IN_AGAA(T322)
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), lessc33_out_ag(0, s(x0)))
U16_GAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(z0))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
U16_GAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(z0))
P68_IN_AGAA(s(T228)) → P50_IN_AGAA(T228)
P18_IN_GAAA(s(x0)) → U4_GAAA(s(x0), U53_ga(x0, lessc20_in_ga(x0)))
INSERT1_IN_GAA(s(z0)) → P43_IN_AGAA(s(z0))
U9_AGAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(s(z0)))
U9_AGAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(s(z0)))
U4_GAAA(0, lessc20_out_ga(0)) → INSERT1_IN_GAA(s(0))
U4_GAAA(s(z0), lessc20_out_ga(s(z0))) → INSERT1_IN_GAA(s(s(z0)))
INSERT1_IN_GAA(s(z0)) → P68_IN_AGAA(s(z0))
INSERT1_IN_GAA(s(s(z0))) → P68_IN_AGAA(s(s(z0)))
INSERT1_IN_GAA(s(0)) → P68_IN_AGAA(s(0))

The TRS R consists of the following rules:

lessc20_in_ga(0) → lessc20_out_ga(0)
lessc20_in_ga(s(T60)) → U53_ga(T60, lessc20_in_ga(T60))
U53_ga(T60, lessc20_out_ga(T60)) → lessc20_out_ga(s(T60))
lessc33_in_ag(s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T101)) → U54_ag(T101, lessc33_in_ag(T101))
U54_ag(T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The set Q consists of the following terms:

lessc20_in_ga(x0)
U53_ga(x0, x1)
lessc33_in_ag(x0)
U54_ag(x0, x1)

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

(43) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule P43_IN_AGAA(s(T134)) → P50_IN_AGAA(T134) we obtained the following new rules [LPAR04]:

P43_IN_AGAA(s(s(y_0))) → P50_IN_AGAA(s(y_0))

(44) Obligation:

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

P43_IN_AGAA(s(T124)) → INSERT1_IN_GAA(s(T124))
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), lessc33_out_ag(0, s(x0)))
INSERT1_IN_GAA(s(T40)) → P18_IN_GAAA(T40)
P18_IN_GAAA(0) → U4_GAAA(0, lessc20_out_ga(0))
P68_IN_AGAA(s(T218)) → INSERT1_IN_GAA(s(T218))
INSERT1_IN_GAA(s(T312)) → INSERT1_IN_GAA(s(T312))
INSERT1_IN_GAA(s(T322)) → P50_IN_AGAA(T322)
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), lessc33_out_ag(0, s(x0)))
U16_GAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(z0))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
U16_GAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(z0))
P68_IN_AGAA(s(T228)) → P50_IN_AGAA(T228)
P18_IN_GAAA(s(x0)) → U4_GAAA(s(x0), U53_ga(x0, lessc20_in_ga(x0)))
INSERT1_IN_GAA(s(z0)) → P43_IN_AGAA(s(z0))
U9_AGAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(s(z0)))
U9_AGAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(s(z0)))
U4_GAAA(0, lessc20_out_ga(0)) → INSERT1_IN_GAA(s(0))
U4_GAAA(s(z0), lessc20_out_ga(s(z0))) → INSERT1_IN_GAA(s(s(z0)))
INSERT1_IN_GAA(s(z0)) → P68_IN_AGAA(s(z0))
INSERT1_IN_GAA(s(s(z0))) → P68_IN_AGAA(s(s(z0)))
INSERT1_IN_GAA(s(0)) → P68_IN_AGAA(s(0))
P43_IN_AGAA(s(s(y_0))) → P50_IN_AGAA(s(y_0))

The TRS R consists of the following rules:

lessc20_in_ga(0) → lessc20_out_ga(0)
lessc20_in_ga(s(T60)) → U53_ga(T60, lessc20_in_ga(T60))
U53_ga(T60, lessc20_out_ga(T60)) → lessc20_out_ga(s(T60))
lessc33_in_ag(s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T101)) → U54_ag(T101, lessc33_in_ag(T101))
U54_ag(T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The set Q consists of the following terms:

lessc20_in_ga(x0)
U53_ga(x0, x1)
lessc33_in_ag(x0)
U54_ag(x0, x1)

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

(45) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule INSERT1_IN_GAA(s(T40)) → P18_IN_GAAA(T40) we obtained the following new rules [LPAR04]:

INSERT1_IN_GAA(s(0)) → P18_IN_GAAA(0)
INSERT1_IN_GAA(s(s(y_0))) → P18_IN_GAAA(s(y_0))

(46) Obligation:

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

P43_IN_AGAA(s(T124)) → INSERT1_IN_GAA(s(T124))
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), lessc33_out_ag(0, s(x0)))
P18_IN_GAAA(0) → U4_GAAA(0, lessc20_out_ga(0))
P68_IN_AGAA(s(T218)) → INSERT1_IN_GAA(s(T218))
INSERT1_IN_GAA(s(T312)) → INSERT1_IN_GAA(s(T312))
INSERT1_IN_GAA(s(T322)) → P50_IN_AGAA(T322)
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), lessc33_out_ag(0, s(x0)))
U16_GAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(z0))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
U16_GAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(z0))
P68_IN_AGAA(s(T228)) → P50_IN_AGAA(T228)
P18_IN_GAAA(s(x0)) → U4_GAAA(s(x0), U53_ga(x0, lessc20_in_ga(x0)))
INSERT1_IN_GAA(s(z0)) → P43_IN_AGAA(s(z0))
U9_AGAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(s(z0)))
U9_AGAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(s(z0)))
U4_GAAA(0, lessc20_out_ga(0)) → INSERT1_IN_GAA(s(0))
U4_GAAA(s(z0), lessc20_out_ga(s(z0))) → INSERT1_IN_GAA(s(s(z0)))
INSERT1_IN_GAA(s(z0)) → P68_IN_AGAA(s(z0))
INSERT1_IN_GAA(s(s(z0))) → P68_IN_AGAA(s(s(z0)))
INSERT1_IN_GAA(s(0)) → P68_IN_AGAA(s(0))
P43_IN_AGAA(s(s(y_0))) → P50_IN_AGAA(s(y_0))
INSERT1_IN_GAA(s(0)) → P18_IN_GAAA(0)
INSERT1_IN_GAA(s(s(y_0))) → P18_IN_GAAA(s(y_0))

The TRS R consists of the following rules:

lessc20_in_ga(0) → lessc20_out_ga(0)
lessc20_in_ga(s(T60)) → U53_ga(T60, lessc20_in_ga(T60))
U53_ga(T60, lessc20_out_ga(T60)) → lessc20_out_ga(s(T60))
lessc33_in_ag(s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T101)) → U54_ag(T101, lessc33_in_ag(T101))
U54_ag(T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The set Q consists of the following terms:

lessc20_in_ga(x0)
U53_ga(x0, x1)
lessc33_in_ag(x0)
U54_ag(x0, x1)

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

(47) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule INSERT1_IN_GAA(s(T322)) → P50_IN_AGAA(T322) we obtained the following new rules [LPAR04]:

INSERT1_IN_GAA(s(s(y_0))) → P50_IN_AGAA(s(y_0))

(48) Obligation:

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

P43_IN_AGAA(s(T124)) → INSERT1_IN_GAA(s(T124))
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), lessc33_out_ag(0, s(x0)))
P18_IN_GAAA(0) → U4_GAAA(0, lessc20_out_ga(0))
P68_IN_AGAA(s(T218)) → INSERT1_IN_GAA(s(T218))
INSERT1_IN_GAA(s(T312)) → INSERT1_IN_GAA(s(T312))
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), lessc33_out_ag(0, s(x0)))
U16_GAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(z0))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
U16_GAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(z0))
P68_IN_AGAA(s(T228)) → P50_IN_AGAA(T228)
P18_IN_GAAA(s(x0)) → U4_GAAA(s(x0), U53_ga(x0, lessc20_in_ga(x0)))
INSERT1_IN_GAA(s(z0)) → P43_IN_AGAA(s(z0))
U9_AGAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(s(z0)))
U9_AGAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(s(z0)))
U4_GAAA(0, lessc20_out_ga(0)) → INSERT1_IN_GAA(s(0))
U4_GAAA(s(z0), lessc20_out_ga(s(z0))) → INSERT1_IN_GAA(s(s(z0)))
INSERT1_IN_GAA(s(z0)) → P68_IN_AGAA(s(z0))
INSERT1_IN_GAA(s(s(z0))) → P68_IN_AGAA(s(s(z0)))
INSERT1_IN_GAA(s(0)) → P68_IN_AGAA(s(0))
P43_IN_AGAA(s(s(y_0))) → P50_IN_AGAA(s(y_0))
INSERT1_IN_GAA(s(0)) → P18_IN_GAAA(0)
INSERT1_IN_GAA(s(s(y_0))) → P18_IN_GAAA(s(y_0))
INSERT1_IN_GAA(s(s(y_0))) → P50_IN_AGAA(s(y_0))

The TRS R consists of the following rules:

lessc20_in_ga(0) → lessc20_out_ga(0)
lessc20_in_ga(s(T60)) → U53_ga(T60, lessc20_in_ga(T60))
U53_ga(T60, lessc20_out_ga(T60)) → lessc20_out_ga(s(T60))
lessc33_in_ag(s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T101)) → U54_ag(T101, lessc33_in_ag(T101))
U54_ag(T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The set Q consists of the following terms:

lessc20_in_ga(x0)
U53_ga(x0, x1)
lessc33_in_ag(x0)
U54_ag(x0, x1)

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

(49) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule P68_IN_AGAA(s(T228)) → P50_IN_AGAA(T228) we obtained the following new rules [LPAR04]:

P68_IN_AGAA(s(s(y_0))) → P50_IN_AGAA(s(y_0))

(50) Obligation:

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

P43_IN_AGAA(s(T124)) → INSERT1_IN_GAA(s(T124))
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), lessc33_out_ag(0, s(x0)))
P18_IN_GAAA(0) → U4_GAAA(0, lessc20_out_ga(0))
P68_IN_AGAA(s(T218)) → INSERT1_IN_GAA(s(T218))
INSERT1_IN_GAA(s(T312)) → INSERT1_IN_GAA(s(T312))
P50_IN_AGAA(s(x0)) → U9_AGAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), lessc33_out_ag(0, s(x0)))
U16_GAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(z0))
INSERT1_IN_GAA(s(x0)) → U16_GAA(s(x0), U54_ag(x0, lessc33_in_ag(x0)))
U16_GAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(z0))
P18_IN_GAAA(s(x0)) → U4_GAAA(s(x0), U53_ga(x0, lessc20_in_ga(x0)))
INSERT1_IN_GAA(s(z0)) → P43_IN_AGAA(s(z0))
U9_AGAA(s(z0), lessc33_out_ag(0, s(z0))) → INSERT1_IN_GAA(s(s(z0)))
U9_AGAA(s(z0), lessc33_out_ag(x1, s(z0))) → INSERT1_IN_GAA(s(s(z0)))
U4_GAAA(0, lessc20_out_ga(0)) → INSERT1_IN_GAA(s(0))
U4_GAAA(s(z0), lessc20_out_ga(s(z0))) → INSERT1_IN_GAA(s(s(z0)))
INSERT1_IN_GAA(s(z0)) → P68_IN_AGAA(s(z0))
INSERT1_IN_GAA(s(s(z0))) → P68_IN_AGAA(s(s(z0)))
INSERT1_IN_GAA(s(0)) → P68_IN_AGAA(s(0))
P43_IN_AGAA(s(s(y_0))) → P50_IN_AGAA(s(y_0))
INSERT1_IN_GAA(s(0)) → P18_IN_GAAA(0)
INSERT1_IN_GAA(s(s(y_0))) → P18_IN_GAAA(s(y_0))
INSERT1_IN_GAA(s(s(y_0))) → P50_IN_AGAA(s(y_0))
P68_IN_AGAA(s(s(y_0))) → P50_IN_AGAA(s(y_0))

The TRS R consists of the following rules:

lessc20_in_ga(0) → lessc20_out_ga(0)
lessc20_in_ga(s(T60)) → U53_ga(T60, lessc20_in_ga(T60))
U53_ga(T60, lessc20_out_ga(T60)) → lessc20_out_ga(s(T60))
lessc33_in_ag(s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T101)) → U54_ag(T101, lessc33_in_ag(T101))
U54_ag(T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The set Q consists of the following terms:

lessc20_in_ga(x0)
U53_ga(x0, x1)
lessc33_in_ag(x0)
U54_ag(x0, x1)

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

(51) 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 = INSERT1_IN_GAA(s(T312)) evaluates to t =INSERT1_IN_GAA(s(T312))

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 INSERT1_IN_GAA(s(T312)) to INSERT1_IN_GAA(s(T312)).

(52) NO

(53) Obligation:

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

INSERT1_IN_GAA(0) → INSERT1_IN_GAA(0)

The TRS R consists of the following rules:

lessc20_in_ga(0) → lessc20_out_ga(0)
lessc20_in_ga(s(T60)) → U53_ga(T60, lessc20_in_ga(T60))
U53_ga(T60, lessc20_out_ga(T60)) → lessc20_out_ga(s(T60))
lessc33_in_ag(s(T95)) → lessc33_out_ag(0, s(T95))
lessc33_in_ag(s(T101)) → U54_ag(T101, lessc33_in_ag(T101))
U54_ag(T101, lessc33_out_ag(T102, T101)) → lessc33_out_ag(s(T102), s(T101))

The set Q consists of the following terms:

lessc20_in_ga(x0)
U53_ga(x0, x1)
lessc33_in_ag(x0)
U54_ag(x0, x1)

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

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

(55) Obligation:

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

INSERT1_IN_GAA(0) → INSERT1_IN_GAA(0)

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

lessc20_in_ga(x0)
U53_ga(x0, x1)
lessc33_in_ag(x0)
U54_ag(x0, x1)

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

(56) 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].

lessc20_in_ga(x0)
U53_ga(x0, x1)
lessc33_in_ag(x0)
U54_ag(x0, x1)

(57) Obligation:

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

INSERT1_IN_GAA(0) → INSERT1_IN_GAA(0)

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

(58) 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 = INSERT1_IN_GAA(0) evaluates to t =INSERT1_IN_GAA(0)

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

• Semiunifier: [ ]
• Matcher: [ ]

---

Rewriting sequence

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

(59) NO