Runtime Complexity of the query pattern
inorder(g,a)
w.r.t. the given Prolog program could be shown to be BOUNDS(O(1), O(n^2)).

(0) Obligation:

Clauses:

inorder(nil, []).
inorder(tree(L, V, R), I) :- ','(inorder(L, LI), ','(inorder(R, RI), append(LI, .(V, RI), I))).
append([], X, X).
append(.(X, Xs), Ys, .(X, Zs)) :- append(Xs, Ys, Zs).

Query: inorder(g,a)

(1) LPReorderTransformerProof (EQUIVALENT transformation)

Reordered facts before rules in definite LP [PROLOG].

(2) Obligation:

Clauses:

inorder(nil, []).
append([], X, X).
inorder(tree(L, V, R), I) :- ','(inorder(L, LI), ','(inorder(R, RI), append(LI, .(V, RI), I))).
append(.(X, Xs), Ys, .(X, Zs)) :- append(Xs, Ys, Zs).

Query: inorder(g,a)

(3) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: inorder(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: inorder(T1, T2), SCOPE: 1, CLAUSE: 0 | inorder(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: true | inorder(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: inorder(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\ninorder(T1, T2) !=? inorder(nil, [])", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: inorder(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(inorder(T11, X19), ','(inorder(T13, X20), append(X19, .(T12, X20), T15)))\n\nT11 is ground\nT12 is ground\nT13 is ground\nX19 is free\nX20 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: inorder(T11, X19)\n\nT11 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(inorder(T13, X20), append(T16, .(T12, X20), T15))\n\nT12 is ground\nT13 is ground\nT16 is ground\nX20 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: inorder(T11, X19), SCOPE: 2, CLAUSE: 0 | inorder(T11, X19), SCOPE: 2, CLAUSE: 2\n\nT11 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: true | inorder(nil, X19), SCOPE: 2, CLAUSE: 2\n\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: inorder(T11, X19), SCOPE: 2, CLAUSE: 2\n\nT11 is ground\nX19 is free\ninorder(T11, X19) !=? inorder(nil, [])", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: inorder(nil, X19), SCOPE: 2, CLAUSE: 2\n\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(inorder(T23, X41), ','(inorder(T25, X42), append(X41, .(T24, X42), X43)))\n\nT23 is ground\nT24 is ground\nT25 is ground\nX43 is free\nX41 is free\nX42 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: inorder(T23, X41)\n\nT23 is ground\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(inorder(T25, X42), append(T26, .(T24, X42), X43))\n\nT24 is ground\nT25 is ground\nT26 is ground\nX43 is free\nX42 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: inorder(T25, X42)\n\nT25 is ground\nX42 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: append(T26, .(T24, T27), X43)\n\nT24 is ground\nT26 is ground\nT27 is ground\nX43 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: append(T26, .(T24, T27), X43), SCOPE: 3, CLAUSE: 1 | append(T26, .(T24, T27), X43), SCOPE: 3, CLAUSE: 3\n\nT24 is ground\nT26 is ground\nT27 is ground\nX43 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: true | append([], .(T36, T37), X43), SCOPE: 3, CLAUSE: 3\n\nT36 is ground\nT37 is ground\nX43 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: append(T26, .(T24, T27), X43), SCOPE: 3, CLAUSE: 3\n\nT24 is ground\nT26 is ground\nT27 is ground\nX43 is free\nX48 is free\nappend(T26, .(T24, T27), X43) !=? append([], X48, X48)", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: append([], .(T36, T37), X43), SCOPE: 3, CLAUSE: 3\n\nT36 is ground\nT37 is ground\nX43 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: append(T47, .(T48, T49), X67)\n\nT47 is ground\nT48 is ground\nT49 is ground\nX67 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: inorder(T13, X20)\n\nT13 is ground\nX20 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: append(T16, .(T12, T54), T15)\n\nT12 is ground\nT16 is ground\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: append(T16, .(T12, T54), T15), SCOPE: 4, CLAUSE: 1 | append(T16, .(T12, T54), T15), SCOPE: 4, CLAUSE: 3\n\nT12 is ground\nT16 is ground\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: true | append([], .(T63, T64), T15), SCOPE: 4, CLAUSE: 3\n\nT63 is ground\nT64 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: append(T16, .(T12, T54), T15), SCOPE: 4, CLAUSE: 3\n\nT12 is ground\nT16 is ground\nT54 is ground\nX74 is free\nappend(T16, .(T12, T54), T15) !=? append([], X74, X74)", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: append([], .(T63, T64), T15), SCOPE: 4, CLAUSE: 3\n\nT63 is ground\nT64 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: append(T76, .(T77, T78), T80)\n\nT76 is ground\nT77 is ground\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 80 [arrowhead = none ];
80 -> 3;

81 [label="EVAL with clause\ninorder(nil, []).\nand substitutionT1 -> nil,\nT2 -> []", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 81 [arrowhead = none ];
81 -> 5;

82 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 82 [arrowhead = none ];
82 -> 8;

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

84 [label="EVAL with clause\ninorder(tree(X15, X16, X17), X18) :- ','(inorder(X15, X19), ','(inorder(X17, X20), append(X19, .(X16, X20), X18))).\nand substitutionX15 -> T11,\nX16 -> T12,\nX17 -> T13,\nT1 -> tree(T11, T12, T13),\nT2 -> T15,\nX18 -> T15,\nT14 -> T15", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 84 [arrowhead = none ];
84 -> 16;

85 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 85 [arrowhead = none ];
85 -> 18;

86 [label="BACKTRACK\nfor clause: inorder(tree(L, V, R), I) :- ','(inorder(L, LI), ','(inorder(R, RI), append(LI, .(V, RI), I)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 86 [arrowhead = none ];
86 -> 12;

87 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
16 -> 87 [arrowhead = none ];
87 -> 22;

88 [label="SPLIT 2\nnew knowledge:\nT11 is ground\nT16 is ground\nreplacements:X19 -> T16", fontsize=14, style = filled, fillcolor = violet];
16 -> 88 [arrowhead = none ];
88 -> 23;

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

90 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
23 -> 90 [arrowhead = none ];
90 -> 62;

91 [label="SPLIT 2\nnew knowledge:\nT13 is ground\nT54 is ground\nreplacements:X20 -> T54", fontsize=14, style = filled, fillcolor = violet];
23 -> 91 [arrowhead = none ];
91 -> 63;

92 [label="EVAL with clause\ninorder(nil, []).\nand substitutionT11 -> nil,\nX19 -> []", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 92 [arrowhead = none ];
92 -> 28;

93 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 93 [arrowhead = none ];
93 -> 30;

94 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 94 [arrowhead = none ];
94 -> 32;

95 [label="EVAL with clause\ninorder(tree(X37, X38, X39), X40) :- ','(inorder(X37, X41), ','(inorder(X39, X42), append(X41, .(X38, X42), X40))).\nand substitutionX37 -> T23,\nX38 -> T24,\nX39 -> T25,\nT11 -> tree(T23, T24, T25),\nX19 -> X43,\nX40 -> X43", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 95 [arrowhead = none ];
95 -> 37;

96 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 96 [arrowhead = none ];
96 -> 39;

97 [label="BACKTRACK\nfor clause: inorder(tree(L, V, R), I) :- ','(inorder(L, LI), ','(inorder(R, RI), append(LI, .(V, RI), I)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
32 -> 97 [arrowhead = none ];
97 -> 34;

98 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
37 -> 98 [arrowhead = none ];
98 -> 40;

99 [label="SPLIT 2\nnew knowledge:\nT23 is ground\nT26 is ground\nreplacements:X41 -> T26", fontsize=14, style = filled, fillcolor = violet];
37 -> 99 [arrowhead = none ];
99 -> 41;

100 [label="INSTANCE with matching:\nT11 -> T23\nX19 -> X41", fontsize=14, style = filled, fillcolor = lightgrey];
40 -> 100 [arrowhead = none , style=dashed];
100 -> 22[style=dashed];

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

102 [label="SPLIT 2\nnew knowledge:\nT25 is ground\nT27 is ground\nreplacements:X42 -> T27", fontsize=14, style = filled, fillcolor = violet];
41 -> 102 [arrowhead = none ];
102 -> 45;

103 [label="INSTANCE with matching:\nT11 -> T25\nX19 -> X42", fontsize=14, style = filled, fillcolor = lightgrey];
44 -> 103 [arrowhead = none , style=dashed];
103 -> 22[style=dashed];

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

105 [label="EVAL with clause\nappend([], X48, X48).\nand substitutionT26 -> [],\nT24 -> T36,\nT27 -> T37,\nX48 -> .(T36, T37),\nX43 -> .(T36, T37)", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 105 [arrowhead = none ];
105 -> 50;

106 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 106 [arrowhead = none ];
106 -> 51;

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

108 [label="EVAL with clause\nappend(.(X63, X64), X65, .(X63, X66)) :- append(X64, X65, X66).\nand substitutionX63 -> T46,\nX64 -> T47,\nT26 -> .(T46, T47),\nT24 -> T48,\nT27 -> T49,\nX65 -> .(T48, T49),\nX66 -> X67,\nX43 -> .(T46, X67)", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 108 [arrowhead = none ];
108 -> 58;

109 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 109 [arrowhead = none ];
109 -> 59;

110 [label="BACKTRACK\nfor clause: append(.(X, Xs), Ys, .(X, Zs)) :- append(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 110 [arrowhead = none ];
110 -> 55;

111 [label="INSTANCE with matching:\nT26 -> T47\nT24 -> T48\nT27 -> T49\nX43 -> X67", fontsize=14, style = filled, fillcolor = lightgrey];
58 -> 111 [arrowhead = none , style=dashed];
111 -> 45[style=dashed];

112 [label="INSTANCE with matching:\nT11 -> T13\nX19 -> X20", fontsize=14, style = filled, fillcolor = lightgrey];
62 -> 112 [arrowhead = none , style=dashed];
112 -> 22[style=dashed];

113 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
63 -> 113 [arrowhead = none ];
113 -> 65;

114 [label="EVAL with clause\nappend([], X74, X74).\nand substitutionT16 -> [],\nT12 -> T63,\nT54 -> T64,\nX74 -> .(T63, T64),\nT15 -> .(T63, T64)", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 114 [arrowhead = none ];
114 -> 70;

115 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 115 [arrowhead = none ];
115 -> 72;

116 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
70 -> 116 [arrowhead = none ];
116 -> 74;

117 [label="EVAL with clause\nappend(.(X87, X88), X89, .(X87, X90)) :- append(X88, X89, X90).\nand substitutionX87 -> T75,\nX88 -> T76,\nT16 -> .(T75, T76),\nT12 -> T77,\nT54 -> T78,\nX89 -> .(T77, T78),\nX90 -> T80,\nT15 -> .(T75, T80),\nT79 -> T80", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 117 [arrowhead = none ];
117 -> 78;

118 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 118 [arrowhead = none ];
118 -> 79;

119 [label="BACKTRACK\nfor clause: append(.(X, Xs), Ys, .(X, Zs)) :- append(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
74 -> 119 [arrowhead = none ];
119 -> 75;

120 [label="INSTANCE with matching:\nT16 -> T76\nT12 -> T77\nT54 -> T78\nT15 -> T80", fontsize=14, style = filled, fillcolor = lightgrey];
78 -> 120 [arrowhead = none , style=dashed];
120 -> 63[style=dashed];

}

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(nil) → f1_out1([])
f1_in(tree(z0, z1, z2)) → U1(f16_in(z0, z2, z1), tree(z0, z1, z2))
U1(f16_out1(z0, z1, z2), tree(z3, z4, z5)) → f1_out1(z2)
f22_in(nil) → f22_out1([])
f22_in(tree(z0, z1, z2)) → U2(f37_in(z0, z2, z1), tree(z0, z1, z2))
U2(f37_out1(z0, z1, z2), tree(z3, z4, z5)) → f22_out1(z2)
f63_in([], z0, z1) → f63_out1(.(z0, z1))
f63_in(.(z0, z1), z2, z3) → U3(f63_in(z1, z2, z3), .(z0, z1), z2, z3)
U3(f63_out1(z0), .(z1, z2), z3, z4) → f63_out1(.(z1, z0))
f45_in([], z0, z1) → f45_out1(.(z0, z1))
f45_in(.(z0, z1), z2, z3) → U4(f45_in(z1, z2, z3), .(z0, z1), z2, z3)
U4(f45_out1(z0), .(z1, z2), z3, z4) → f45_out1(.(z1, z0))
f16_in(z0, z1, z2) → U5(f22_in(z0), z0, z1, z2)
U5(f22_out1(z0), z1, z2, z3) → U6(f23_in(z2, z0, z3), z1, z2, z3, z0)
U6(f23_out1(z0, z1), z2, z3, z4, z5) → f16_out1(z5, z0, z1)
f23_in(z0, z1, z2) → U7(f22_in(z0), z0, z1, z2)
U7(f22_out1(z0), z1, z2, z3) → U8(f63_in(z2, z3, z0), z1, z2, z3, z0)
U8(f63_out1(z0), z1, z2, z3, z4) → f23_out1(z4, z0)
f37_in(z0, z1, z2) → U9(f22_in(z0), z0, z1, z2)
U9(f22_out1(z0), z1, z2, z3) → U10(f41_in(z2, z0, z3), z1, z2, z3, z0)
U10(f41_out1(z0, z1), z2, z3, z4, z5) → f37_out1(z5, z0, z1)
f41_in(z0, z1, z2) → U11(f22_in(z0), z0, z1, z2)
U11(f22_out1(z0), z1, z2, z3) → U12(f45_in(z2, z3, z0), z1, z2, z3, z0)
U12(f45_out1(z0), z1, z2, z3, z4) → f41_out1(z4, z0)

Tuples:

F1_IN(tree(z0, z1, z2)) → c1(U1'(f16_in(z0, z2, z1), tree(z0, z1, z2)), F16_IN(z0, z2, z1))
F22_IN(tree(z0, z1, z2)) → c4(U2'(f37_in(z0, z2, z1), tree(z0, z1, z2)), F37_IN(z0, z2, z1))
F63_IN(.(z0, z1), z2, z3) → c7(U3'(f63_in(z1, z2, z3), .(z0, z1), z2, z3), F63_IN(z1, z2, z3))
F45_IN(.(z0, z1), z2, z3) → c10(U4'(f45_in(z1, z2, z3), .(z0, z1), z2, z3), F45_IN(z1, z2, z3))
F16_IN(z0, z1, z2) → c12(U5'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c13(U6'(f23_in(z2, z0, z3), z1, z2, z3, z0), F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c15(U7'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c16(U8'(f63_in(z2, z3, z0), z1, z2, z3, z0), F63_IN(z2, z3, z0))
F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U9'(f22_out1(z0), z1, z2, z3) → c19(U10'(f41_in(z2, z0, z3), z1, z2, z3, z0), F41_IN(z2, z0, z3))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U11'(f22_out1(z0), z1, z2, z3) → c22(U12'(f45_in(z2, z3, z0), z1, z2, z3, z0), F45_IN(z2, z3, z0))

S tuples:

F1_IN(tree(z0, z1, z2)) → c1(U1'(f16_in(z0, z2, z1), tree(z0, z1, z2)), F16_IN(z0, z2, z1))
F22_IN(tree(z0, z1, z2)) → c4(U2'(f37_in(z0, z2, z1), tree(z0, z1, z2)), F37_IN(z0, z2, z1))
F63_IN(.(z0, z1), z2, z3) → c7(U3'(f63_in(z1, z2, z3), .(z0, z1), z2, z3), F63_IN(z1, z2, z3))
F45_IN(.(z0, z1), z2, z3) → c10(U4'(f45_in(z1, z2, z3), .(z0, z1), z2, z3), F45_IN(z1, z2, z3))
F16_IN(z0, z1, z2) → c12(U5'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c13(U6'(f23_in(z2, z0, z3), z1, z2, z3, z0), F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c15(U7'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c16(U8'(f63_in(z2, z3, z0), z1, z2, z3, z0), F63_IN(z2, z3, z0))
F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U9'(f22_out1(z0), z1, z2, z3) → c19(U10'(f41_in(z2, z0, z3), z1, z2, z3, z0), F41_IN(z2, z0, z3))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U11'(f22_out1(z0), z1, z2, z3) → c22(U12'(f45_in(z2, z3, z0), z1, z2, z3, z0), F45_IN(z2, z3, z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f22_in, U2, f63_in, U3, f45_in, U4, f16_in, U5, U6, f23_in, U7, U8, f37_in, U9, U10, f41_in, U11, U12

Defined Pair Symbols:

F1_IN, F22_IN, F63_IN, F45_IN, F16_IN, U5', F23_IN, U7', F37_IN, U9', F41_IN, U11'

Compound Symbols:

c1, c4, c7, c10, c12, c13, c15, c16, c18, c19, c21, c22

(5) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(nil) → f1_out1([])
f1_in(tree(z0, z1, z2)) → U1(f16_in(z0, z2, z1), tree(z0, z1, z2))
U1(f16_out1(z0, z1, z2), tree(z3, z4, z5)) → f1_out1(z2)
f22_in(nil) → f22_out1([])
f22_in(tree(z0, z1, z2)) → U2(f37_in(z0, z2, z1), tree(z0, z1, z2))
U2(f37_out1(z0, z1, z2), tree(z3, z4, z5)) → f22_out1(z2)
f63_in([], z0, z1) → f63_out1(.(z0, z1))
f63_in(.(z0, z1), z2, z3) → U3(f63_in(z1, z2, z3), .(z0, z1), z2, z3)
U3(f63_out1(z0), .(z1, z2), z3, z4) → f63_out1(.(z1, z0))
f45_in([], z0, z1) → f45_out1(.(z0, z1))
f45_in(.(z0, z1), z2, z3) → U4(f45_in(z1, z2, z3), .(z0, z1), z2, z3)
U4(f45_out1(z0), .(z1, z2), z3, z4) → f45_out1(.(z1, z0))
f16_in(z0, z1, z2) → U5(f22_in(z0), z0, z1, z2)
U5(f22_out1(z0), z1, z2, z3) → U6(f23_in(z2, z0, z3), z1, z2, z3, z0)
U6(f23_out1(z0, z1), z2, z3, z4, z5) → f16_out1(z5, z0, z1)
f23_in(z0, z1, z2) → U7(f22_in(z0), z0, z1, z2)
U7(f22_out1(z0), z1, z2, z3) → U8(f63_in(z2, z3, z0), z1, z2, z3, z0)
U8(f63_out1(z0), z1, z2, z3, z4) → f23_out1(z4, z0)
f37_in(z0, z1, z2) → U9(f22_in(z0), z0, z1, z2)
U9(f22_out1(z0), z1, z2, z3) → U10(f41_in(z2, z0, z3), z1, z2, z3, z0)
U10(f41_out1(z0, z1), z2, z3, z4, z5) → f37_out1(z5, z0, z1)
f41_in(z0, z1, z2) → U11(f22_in(z0), z0, z1, z2)
U11(f22_out1(z0), z1, z2, z3) → U12(f45_in(z2, z3, z0), z1, z2, z3, z0)
U12(f45_out1(z0), z1, z2, z3, z4) → f41_out1(z4, z0)

Tuples:

F22_IN(tree(z0, z1, z2)) → c4(U2'(f37_in(z0, z2, z1), tree(z0, z1, z2)), F37_IN(z0, z2, z1))
F63_IN(.(z0, z1), z2, z3) → c7(U3'(f63_in(z1, z2, z3), .(z0, z1), z2, z3), F63_IN(z1, z2, z3))
F45_IN(.(z0, z1), z2, z3) → c10(U4'(f45_in(z1, z2, z3), .(z0, z1), z2, z3), F45_IN(z1, z2, z3))
F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U9'(f22_out1(z0), z1, z2, z3) → c19(U10'(f41_in(z2, z0, z3), z1, z2, z3, z0), F41_IN(z2, z0, z3))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F1_IN(tree(z0, z1, z2)) → c(U1'(f16_in(z0, z2, z1), tree(z0, z1, z2)))
F1_IN(tree(z0, z1, z2)) → c(F16_IN(z0, z2, z1))
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(U6'(f23_in(z2, z0, z3), z1, z2, z3, z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(U8'(f63_in(z2, z3, z0), z1, z2, z3, z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
U11'(f22_out1(z0), z1, z2, z3) → c(U12'(f45_in(z2, z3, z0), z1, z2, z3, z0))
U11'(f22_out1(z0), z1, z2, z3) → c(F45_IN(z2, z3, z0))

S tuples:

F22_IN(tree(z0, z1, z2)) → c4(U2'(f37_in(z0, z2, z1), tree(z0, z1, z2)), F37_IN(z0, z2, z1))
F63_IN(.(z0, z1), z2, z3) → c7(U3'(f63_in(z1, z2, z3), .(z0, z1), z2, z3), F63_IN(z1, z2, z3))
F45_IN(.(z0, z1), z2, z3) → c10(U4'(f45_in(z1, z2, z3), .(z0, z1), z2, z3), F45_IN(z1, z2, z3))
F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U9'(f22_out1(z0), z1, z2, z3) → c19(U10'(f41_in(z2, z0, z3), z1, z2, z3, z0), F41_IN(z2, z0, z3))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F1_IN(tree(z0, z1, z2)) → c(U1'(f16_in(z0, z2, z1), tree(z0, z1, z2)))
F1_IN(tree(z0, z1, z2)) → c(F16_IN(z0, z2, z1))
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(U6'(f23_in(z2, z0, z3), z1, z2, z3, z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(U8'(f63_in(z2, z3, z0), z1, z2, z3, z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
U11'(f22_out1(z0), z1, z2, z3) → c(U12'(f45_in(z2, z3, z0), z1, z2, z3, z0))
U11'(f22_out1(z0), z1, z2, z3) → c(F45_IN(z2, z3, z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f22_in, U2, f63_in, U3, f45_in, U4, f16_in, U5, U6, f23_in, U7, U8, f37_in, U9, U10, f41_in, U11, U12

Defined Pair Symbols:

F22_IN, F63_IN, F45_IN, F37_IN, U9', F41_IN, F1_IN, F16_IN, U5', F23_IN, U7', U11'

Compound Symbols:

c4, c7, c10, c18, c19, c21, c

(7) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 8 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(nil) → f1_out1([])
f1_in(tree(z0, z1, z2)) → U1(f16_in(z0, z2, z1), tree(z0, z1, z2))
U1(f16_out1(z0, z1, z2), tree(z3, z4, z5)) → f1_out1(z2)
f22_in(nil) → f22_out1([])
f22_in(tree(z0, z1, z2)) → U2(f37_in(z0, z2, z1), tree(z0, z1, z2))
U2(f37_out1(z0, z1, z2), tree(z3, z4, z5)) → f22_out1(z2)
f63_in([], z0, z1) → f63_out1(.(z0, z1))
f63_in(.(z0, z1), z2, z3) → U3(f63_in(z1, z2, z3), .(z0, z1), z2, z3)
U3(f63_out1(z0), .(z1, z2), z3, z4) → f63_out1(.(z1, z0))
f45_in([], z0, z1) → f45_out1(.(z0, z1))
f45_in(.(z0, z1), z2, z3) → U4(f45_in(z1, z2, z3), .(z0, z1), z2, z3)
U4(f45_out1(z0), .(z1, z2), z3, z4) → f45_out1(.(z1, z0))
f16_in(z0, z1, z2) → U5(f22_in(z0), z0, z1, z2)
U5(f22_out1(z0), z1, z2, z3) → U6(f23_in(z2, z0, z3), z1, z2, z3, z0)
U6(f23_out1(z0, z1), z2, z3, z4, z5) → f16_out1(z5, z0, z1)
f23_in(z0, z1, z2) → U7(f22_in(z0), z0, z1, z2)
U7(f22_out1(z0), z1, z2, z3) → U8(f63_in(z2, z3, z0), z1, z2, z3, z0)
U8(f63_out1(z0), z1, z2, z3, z4) → f23_out1(z4, z0)
f37_in(z0, z1, z2) → U9(f22_in(z0), z0, z1, z2)
U9(f22_out1(z0), z1, z2, z3) → U10(f41_in(z2, z0, z3), z1, z2, z3, z0)
U10(f41_out1(z0, z1), z2, z3, z4, z5) → f37_out1(z5, z0, z1)
f41_in(z0, z1, z2) → U11(f22_in(z0), z0, z1, z2)
U11(f22_out1(z0), z1, z2, z3) → U12(f45_in(z2, z3, z0), z1, z2, z3, z0)
U12(f45_out1(z0), z1, z2, z3, z4) → f41_out1(z4, z0)

Tuples:

F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F1_IN(tree(z0, z1, z2)) → c(F16_IN(z0, z2, z1))
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
U11'(f22_out1(z0), z1, z2, z3) → c(F45_IN(z2, z3, z0))
F22_IN(tree(z0, z1, z2)) → c4(F37_IN(z0, z2, z1))
F63_IN(.(z0, z1), z2, z3) → c7(F63_IN(z1, z2, z3))
F45_IN(.(z0, z1), z2, z3) → c10(F45_IN(z1, z2, z3))
U9'(f22_out1(z0), z1, z2, z3) → c19(F41_IN(z2, z0, z3))
F1_IN(tree(z0, z1, z2)) → c
U5'(f22_out1(z0), z1, z2, z3) → c
U7'(f22_out1(z0), z1, z2, z3) → c
U11'(f22_out1(z0), z1, z2, z3) → c

S tuples:

F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F1_IN(tree(z0, z1, z2)) → c(F16_IN(z0, z2, z1))
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
U11'(f22_out1(z0), z1, z2, z3) → c(F45_IN(z2, z3, z0))
F22_IN(tree(z0, z1, z2)) → c4(F37_IN(z0, z2, z1))
F63_IN(.(z0, z1), z2, z3) → c7(F63_IN(z1, z2, z3))
F45_IN(.(z0, z1), z2, z3) → c10(F45_IN(z1, z2, z3))
U9'(f22_out1(z0), z1, z2, z3) → c19(F41_IN(z2, z0, z3))
F1_IN(tree(z0, z1, z2)) → c
U5'(f22_out1(z0), z1, z2, z3) → c
U7'(f22_out1(z0), z1, z2, z3) → c
U11'(f22_out1(z0), z1, z2, z3) → c

K tuples:none
Defined Rule Symbols:

f1_in, U1, f22_in, U2, f63_in, U3, f45_in, U4, f16_in, U5, U6, f23_in, U7, U8, f37_in, U9, U10, f41_in, U11, U12

Defined Pair Symbols:

F37_IN, F41_IN, F1_IN, F16_IN, U5', F23_IN, U7', U11', F22_IN, F63_IN, F45_IN, U9'

Compound Symbols:

c18, c21, c, c4, c7, c10, c19, c

(9) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F1_IN(tree(z0, z1, z2)) → c(F16_IN(z0, z2, z1))
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
F1_IN(tree(z0, z1, z2)) → c
U5'(f22_out1(z0), z1, z2, z3) → c
U7'(f22_out1(z0), z1, z2, z3) → c
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
U5'(f22_out1(z0), z1, z2, z3) → c
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
U7'(f22_out1(z0), z1, z2, z3) → c

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(nil) → f1_out1([])
f1_in(tree(z0, z1, z2)) → U1(f16_in(z0, z2, z1), tree(z0, z1, z2))
U1(f16_out1(z0, z1, z2), tree(z3, z4, z5)) → f1_out1(z2)
f22_in(nil) → f22_out1([])
f22_in(tree(z0, z1, z2)) → U2(f37_in(z0, z2, z1), tree(z0, z1, z2))
U2(f37_out1(z0, z1, z2), tree(z3, z4, z5)) → f22_out1(z2)
f63_in([], z0, z1) → f63_out1(.(z0, z1))
f63_in(.(z0, z1), z2, z3) → U3(f63_in(z1, z2, z3), .(z0, z1), z2, z3)
U3(f63_out1(z0), .(z1, z2), z3, z4) → f63_out1(.(z1, z0))
f45_in([], z0, z1) → f45_out1(.(z0, z1))
f45_in(.(z0, z1), z2, z3) → U4(f45_in(z1, z2, z3), .(z0, z1), z2, z3)
U4(f45_out1(z0), .(z1, z2), z3, z4) → f45_out1(.(z1, z0))
f16_in(z0, z1, z2) → U5(f22_in(z0), z0, z1, z2)
U5(f22_out1(z0), z1, z2, z3) → U6(f23_in(z2, z0, z3), z1, z2, z3, z0)
U6(f23_out1(z0, z1), z2, z3, z4, z5) → f16_out1(z5, z0, z1)
f23_in(z0, z1, z2) → U7(f22_in(z0), z0, z1, z2)
U7(f22_out1(z0), z1, z2, z3) → U8(f63_in(z2, z3, z0), z1, z2, z3, z0)
U8(f63_out1(z0), z1, z2, z3, z4) → f23_out1(z4, z0)
f37_in(z0, z1, z2) → U9(f22_in(z0), z0, z1, z2)
U9(f22_out1(z0), z1, z2, z3) → U10(f41_in(z2, z0, z3), z1, z2, z3, z0)
U10(f41_out1(z0, z1), z2, z3, z4, z5) → f37_out1(z5, z0, z1)
f41_in(z0, z1, z2) → U11(f22_in(z0), z0, z1, z2)
U11(f22_out1(z0), z1, z2, z3) → U12(f45_in(z2, z3, z0), z1, z2, z3, z0)
U12(f45_out1(z0), z1, z2, z3, z4) → f41_out1(z4, z0)

Tuples:

F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F1_IN(tree(z0, z1, z2)) → c(F16_IN(z0, z2, z1))
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
U11'(f22_out1(z0), z1, z2, z3) → c(F45_IN(z2, z3, z0))
F22_IN(tree(z0, z1, z2)) → c4(F37_IN(z0, z2, z1))
F63_IN(.(z0, z1), z2, z3) → c7(F63_IN(z1, z2, z3))
F45_IN(.(z0, z1), z2, z3) → c10(F45_IN(z1, z2, z3))
U9'(f22_out1(z0), z1, z2, z3) → c19(F41_IN(z2, z0, z3))
F1_IN(tree(z0, z1, z2)) → c
U5'(f22_out1(z0), z1, z2, z3) → c
U7'(f22_out1(z0), z1, z2, z3) → c
U11'(f22_out1(z0), z1, z2, z3) → c

S tuples:

F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U11'(f22_out1(z0), z1, z2, z3) → c(F45_IN(z2, z3, z0))
F22_IN(tree(z0, z1, z2)) → c4(F37_IN(z0, z2, z1))
F63_IN(.(z0, z1), z2, z3) → c7(F63_IN(z1, z2, z3))
F45_IN(.(z0, z1), z2, z3) → c10(F45_IN(z1, z2, z3))
U9'(f22_out1(z0), z1, z2, z3) → c19(F41_IN(z2, z0, z3))
U11'(f22_out1(z0), z1, z2, z3) → c

K tuples:

F1_IN(tree(z0, z1, z2)) → c(F16_IN(z0, z2, z1))
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
F1_IN(tree(z0, z1, z2)) → c
U5'(f22_out1(z0), z1, z2, z3) → c
U7'(f22_out1(z0), z1, z2, z3) → c

Defined Rule Symbols:

f1_in, U1, f22_in, U2, f63_in, U3, f45_in, U4, f16_in, U5, U6, f23_in, U7, U8, f37_in, U9, U10, f41_in, U11, U12

Defined Pair Symbols:

F37_IN, F41_IN, F1_IN, F16_IN, U5', F23_IN, U7', U11', F22_IN, F63_IN, F45_IN, U9'

Compound Symbols:

c18, c21, c, c4, c7, c10, c19, c

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F22_IN(tree(z0, z1, z2)) → c4(F37_IN(z0, z2, z1))

We considered the (Usable) Rules:

f22_in(nil) → f22_out1([])
f22_in(tree(z0, z1, z2)) → U2(f37_in(z0, z2, z1), tree(z0, z1, z2))
f37_in(z0, z1, z2) → U9(f22_in(z0), z0, z1, z2)
U2(f37_out1(z0, z1, z2), tree(z3, z4, z5)) → f22_out1(z2)
U9(f22_out1(z0), z1, z2, z3) → U10(f41_in(z2, z0, z3), z1, z2, z3, z0)
f41_in(z0, z1, z2) → U11(f22_in(z0), z0, z1, z2)
U10(f41_out1(z0, z1), z2, z3, z4, z5) → f37_out1(z5, z0, z1)
U11(f22_out1(z0), z1, z2, z3) → U12(f45_in(z2, z3, z0), z1, z2, z3, z0)
f45_in([], z0, z1) → f45_out1(.(z0, z1))
f45_in(.(z0, z1), z2, z3) → U4(f45_in(z1, z2, z3), .(z0, z1), z2, z3)
U12(f45_out1(z0), z1, z2, z3, z4) → f41_out1(z4, z0)
U4(f45_out1(z0), .(z1, z2), z3, z4) → f45_out1(.(z1, z0))

And the Tuples:

F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F1_IN(tree(z0, z1, z2)) → c(F16_IN(z0, z2, z1))
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
U11'(f22_out1(z0), z1, z2, z3) → c(F45_IN(z2, z3, z0))
F22_IN(tree(z0, z1, z2)) → c4(F37_IN(z0, z2, z1))
F63_IN(.(z0, z1), z2, z3) → c7(F63_IN(z1, z2, z3))
F45_IN(.(z0, z1), z2, z3) → c10(F45_IN(z1, z2, z3))
U9'(f22_out1(z0), z1, z2, z3) → c19(F41_IN(z2, z0, z3))
F1_IN(tree(z0, z1, z2)) → c
U5'(f22_out1(z0), z1, z2, z3) → c
U7'(f22_out1(z0), z1, z2, z3) → c
U11'(f22_out1(z0), z1, z2, z3) → c

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = 0   
POL(F16_IN(x₁, x₂, x₃)) = [3] + x₁ + [3]x₂ + [2]x₃   
POL(F1_IN(x₁)) = [3]x₁   
POL(F22_IN(x₁)) = x₁   
POL(F23_IN(x₁, x₂, x₃)) = x₁   
POL(F37_IN(x₁, x₂, x₃)) = x₁ + x₂   
POL(F41_IN(x₁, x₂, x₃)) = x₁   
POL(F45_IN(x₁, x₂, x₃)) = 0   
POL(F63_IN(x₁, x₂, x₃)) = 0   
POL(U10(x₁, x₂, x₃, x₄, x₅)) = [2] + x₁   
POL(U11(x₁, x₂, x₃, x₄)) = 0   
POL(U11'(x₁, x₂, x₃, x₄)) = 0   
POL(U12(x₁, x₂, x₃, x₄, x₅)) = 0   
POL(U2(x₁, x₂)) = 0   
POL(U4(x₁, x₂, x₃, x₄)) = 0   
POL(U5'(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₄   
POL(U7'(x₁, x₂, x₃, x₄)) = x₂   
POL(U9(x₁, x₂, x₃, x₄)) = [2]   
POL(U9'(x₁, x₂, x₃, x₄)) = x₃   
POL([]) = 0   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c19(x₁)) = x₁   
POL(c21(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(f22_in(x₁)) = 0   
POL(f22_out1(x₁)) = 0   
POL(f37_in(x₁, x₂, x₃)) = [2]   
POL(f37_out1(x₁, x₂, x₃)) = [2]   
POL(f41_in(x₁, x₂, x₃)) = 0   
POL(f41_out1(x₁, x₂)) = [2] + x₂   
POL(f45_in(x₁, x₂, x₃)) = 0   
POL(f45_out1(x₁)) = 0   
POL(nil) = 0   
POL(tree(x₁, x₂, x₃)) = [1] + x₁ + x₂ + x₃   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(nil) → f1_out1([])
f1_in(tree(z0, z1, z2)) → U1(f16_in(z0, z2, z1), tree(z0, z1, z2))
U1(f16_out1(z0, z1, z2), tree(z3, z4, z5)) → f1_out1(z2)
f22_in(nil) → f22_out1([])
f22_in(tree(z0, z1, z2)) → U2(f37_in(z0, z2, z1), tree(z0, z1, z2))
U2(f37_out1(z0, z1, z2), tree(z3, z4, z5)) → f22_out1(z2)
f63_in([], z0, z1) → f63_out1(.(z0, z1))
f63_in(.(z0, z1), z2, z3) → U3(f63_in(z1, z2, z3), .(z0, z1), z2, z3)
U3(f63_out1(z0), .(z1, z2), z3, z4) → f63_out1(.(z1, z0))
f45_in([], z0, z1) → f45_out1(.(z0, z1))
f45_in(.(z0, z1), z2, z3) → U4(f45_in(z1, z2, z3), .(z0, z1), z2, z3)
U4(f45_out1(z0), .(z1, z2), z3, z4) → f45_out1(.(z1, z0))
f16_in(z0, z1, z2) → U5(f22_in(z0), z0, z1, z2)
U5(f22_out1(z0), z1, z2, z3) → U6(f23_in(z2, z0, z3), z1, z2, z3, z0)
U6(f23_out1(z0, z1), z2, z3, z4, z5) → f16_out1(z5, z0, z1)
f23_in(z0, z1, z2) → U7(f22_in(z0), z0, z1, z2)
U7(f22_out1(z0), z1, z2, z3) → U8(f63_in(z2, z3, z0), z1, z2, z3, z0)
U8(f63_out1(z0), z1, z2, z3, z4) → f23_out1(z4, z0)
f37_in(z0, z1, z2) → U9(f22_in(z0), z0, z1, z2)
U9(f22_out1(z0), z1, z2, z3) → U10(f41_in(z2, z0, z3), z1, z2, z3, z0)
U10(f41_out1(z0, z1), z2, z3, z4, z5) → f37_out1(z5, z0, z1)
f41_in(z0, z1, z2) → U11(f22_in(z0), z0, z1, z2)
U11(f22_out1(z0), z1, z2, z3) → U12(f45_in(z2, z3, z0), z1, z2, z3, z0)
U12(f45_out1(z0), z1, z2, z3, z4) → f41_out1(z4, z0)

Tuples:

F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F1_IN(tree(z0, z1, z2)) → c(F16_IN(z0, z2, z1))
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
U11'(f22_out1(z0), z1, z2, z3) → c(F45_IN(z2, z3, z0))
F22_IN(tree(z0, z1, z2)) → c4(F37_IN(z0, z2, z1))
F63_IN(.(z0, z1), z2, z3) → c7(F63_IN(z1, z2, z3))
F45_IN(.(z0, z1), z2, z3) → c10(F45_IN(z1, z2, z3))
U9'(f22_out1(z0), z1, z2, z3) → c19(F41_IN(z2, z0, z3))
F1_IN(tree(z0, z1, z2)) → c
U5'(f22_out1(z0), z1, z2, z3) → c
U7'(f22_out1(z0), z1, z2, z3) → c
U11'(f22_out1(z0), z1, z2, z3) → c

S tuples:

F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U11'(f22_out1(z0), z1, z2, z3) → c(F45_IN(z2, z3, z0))
F63_IN(.(z0, z1), z2, z3) → c7(F63_IN(z1, z2, z3))
F45_IN(.(z0, z1), z2, z3) → c10(F45_IN(z1, z2, z3))
U9'(f22_out1(z0), z1, z2, z3) → c19(F41_IN(z2, z0, z3))
U11'(f22_out1(z0), z1, z2, z3) → c

K tuples:

F1_IN(tree(z0, z1, z2)) → c(F16_IN(z0, z2, z1))
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
F1_IN(tree(z0, z1, z2)) → c
U5'(f22_out1(z0), z1, z2, z3) → c
U7'(f22_out1(z0), z1, z2, z3) → c
F22_IN(tree(z0, z1, z2)) → c4(F37_IN(z0, z2, z1))

Defined Rule Symbols:

f1_in, U1, f22_in, U2, f63_in, U3, f45_in, U4, f16_in, U5, U6, f23_in, U7, U8, f37_in, U9, U10, f41_in, U11, U12

Defined Pair Symbols:

F37_IN, F41_IN, F1_IN, F16_IN, U5', F23_IN, U7', U11', F22_IN, F63_IN, F45_IN, U9'

Compound Symbols:

c18, c21, c, c4, c7, c10, c19, c

(13) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U9'(f22_out1(z0), z1, z2, z3) → c19(F41_IN(z2, z0, z3))
F22_IN(tree(z0, z1, z2)) → c4(F37_IN(z0, z2, z1))
U9'(f22_out1(z0), z1, z2, z3) → c19(F41_IN(z2, z0, z3))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U11'(f22_out1(z0), z1, z2, z3) → c(F45_IN(z2, z3, z0))
F22_IN(tree(z0, z1, z2)) → c4(F37_IN(z0, z2, z1))
U11'(f22_out1(z0), z1, z2, z3) → c

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(nil) → f1_out1([])
f1_in(tree(z0, z1, z2)) → U1(f16_in(z0, z2, z1), tree(z0, z1, z2))
U1(f16_out1(z0, z1, z2), tree(z3, z4, z5)) → f1_out1(z2)
f22_in(nil) → f22_out1([])
f22_in(tree(z0, z1, z2)) → U2(f37_in(z0, z2, z1), tree(z0, z1, z2))
U2(f37_out1(z0, z1, z2), tree(z3, z4, z5)) → f22_out1(z2)
f63_in([], z0, z1) → f63_out1(.(z0, z1))
f63_in(.(z0, z1), z2, z3) → U3(f63_in(z1, z2, z3), .(z0, z1), z2, z3)
U3(f63_out1(z0), .(z1, z2), z3, z4) → f63_out1(.(z1, z0))
f45_in([], z0, z1) → f45_out1(.(z0, z1))
f45_in(.(z0, z1), z2, z3) → U4(f45_in(z1, z2, z3), .(z0, z1), z2, z3)
U4(f45_out1(z0), .(z1, z2), z3, z4) → f45_out1(.(z1, z0))
f16_in(z0, z1, z2) → U5(f22_in(z0), z0, z1, z2)
U5(f22_out1(z0), z1, z2, z3) → U6(f23_in(z2, z0, z3), z1, z2, z3, z0)
U6(f23_out1(z0, z1), z2, z3, z4, z5) → f16_out1(z5, z0, z1)
f23_in(z0, z1, z2) → U7(f22_in(z0), z0, z1, z2)
U7(f22_out1(z0), z1, z2, z3) → U8(f63_in(z2, z3, z0), z1, z2, z3, z0)
U8(f63_out1(z0), z1, z2, z3, z4) → f23_out1(z4, z0)
f37_in(z0, z1, z2) → U9(f22_in(z0), z0, z1, z2)
U9(f22_out1(z0), z1, z2, z3) → U10(f41_in(z2, z0, z3), z1, z2, z3, z0)
U10(f41_out1(z0, z1), z2, z3, z4, z5) → f37_out1(z5, z0, z1)
f41_in(z0, z1, z2) → U11(f22_in(z0), z0, z1, z2)
U11(f22_out1(z0), z1, z2, z3) → U12(f45_in(z2, z3, z0), z1, z2, z3, z0)
U12(f45_out1(z0), z1, z2, z3, z4) → f41_out1(z4, z0)

Tuples:

F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F1_IN(tree(z0, z1, z2)) → c(F16_IN(z0, z2, z1))
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
U11'(f22_out1(z0), z1, z2, z3) → c(F45_IN(z2, z3, z0))
F22_IN(tree(z0, z1, z2)) → c4(F37_IN(z0, z2, z1))
F63_IN(.(z0, z1), z2, z3) → c7(F63_IN(z1, z2, z3))
F45_IN(.(z0, z1), z2, z3) → c10(F45_IN(z1, z2, z3))
U9'(f22_out1(z0), z1, z2, z3) → c19(F41_IN(z2, z0, z3))
F1_IN(tree(z0, z1, z2)) → c
U5'(f22_out1(z0), z1, z2, z3) → c
U7'(f22_out1(z0), z1, z2, z3) → c
U11'(f22_out1(z0), z1, z2, z3) → c

S tuples:

F63_IN(.(z0, z1), z2, z3) → c7(F63_IN(z1, z2, z3))
F45_IN(.(z0, z1), z2, z3) → c10(F45_IN(z1, z2, z3))

K tuples:

F1_IN(tree(z0, z1, z2)) → c(F16_IN(z0, z2, z1))
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
F1_IN(tree(z0, z1, z2)) → c
U5'(f22_out1(z0), z1, z2, z3) → c
U7'(f22_out1(z0), z1, z2, z3) → c
F22_IN(tree(z0, z1, z2)) → c4(F37_IN(z0, z2, z1))
F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U9'(f22_out1(z0), z1, z2, z3) → c19(F41_IN(z2, z0, z3))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U11'(f22_out1(z0), z1, z2, z3) → c(F45_IN(z2, z3, z0))
U11'(f22_out1(z0), z1, z2, z3) → c

Defined Rule Symbols:

f1_in, U1, f22_in, U2, f63_in, U3, f45_in, U4, f16_in, U5, U6, f23_in, U7, U8, f37_in, U9, U10, f41_in, U11, U12

Defined Pair Symbols:

F37_IN, F41_IN, F1_IN, F16_IN, U5', F23_IN, U7', U11', F22_IN, F63_IN, F45_IN, U9'

Compound Symbols:

c18, c21, c, c4, c7, c10, c19, c

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F63_IN(.(z0, z1), z2, z3) → c7(F63_IN(z1, z2, z3))

We considered the (Usable) Rules:

f22_in(nil) → f22_out1([])
f22_in(tree(z0, z1, z2)) → U2(f37_in(z0, z2, z1), tree(z0, z1, z2))
f37_in(z0, z1, z2) → U9(f22_in(z0), z0, z1, z2)
U2(f37_out1(z0, z1, z2), tree(z3, z4, z5)) → f22_out1(z2)
U9(f22_out1(z0), z1, z2, z3) → U10(f41_in(z2, z0, z3), z1, z2, z3, z0)
f41_in(z0, z1, z2) → U11(f22_in(z0), z0, z1, z2)
U10(f41_out1(z0, z1), z2, z3, z4, z5) → f37_out1(z5, z0, z1)
U11(f22_out1(z0), z1, z2, z3) → U12(f45_in(z2, z3, z0), z1, z2, z3, z0)
f45_in([], z0, z1) → f45_out1(.(z0, z1))
f45_in(.(z0, z1), z2, z3) → U4(f45_in(z1, z2, z3), .(z0, z1), z2, z3)
U12(f45_out1(z0), z1, z2, z3, z4) → f41_out1(z4, z0)
U4(f45_out1(z0), .(z1, z2), z3, z4) → f45_out1(.(z1, z0))

And the Tuples:

F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F1_IN(tree(z0, z1, z2)) → c(F16_IN(z0, z2, z1))
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
U11'(f22_out1(z0), z1, z2, z3) → c(F45_IN(z2, z3, z0))
F22_IN(tree(z0, z1, z2)) → c4(F37_IN(z0, z2, z1))
F63_IN(.(z0, z1), z2, z3) → c7(F63_IN(z1, z2, z3))
F45_IN(.(z0, z1), z2, z3) → c10(F45_IN(z1, z2, z3))
U9'(f22_out1(z0), z1, z2, z3) → c19(F41_IN(z2, z0, z3))
F1_IN(tree(z0, z1, z2)) → c
U5'(f22_out1(z0), z1, z2, z3) → c
U7'(f22_out1(z0), z1, z2, z3) → c
U11'(f22_out1(z0), z1, z2, z3) → c

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = [1] + x₂   
POL(F16_IN(x₁, x₂, x₃)) = [3] + [2]x₁ + x₂   
POL(F1_IN(x₁)) = [2]x₁   
POL(F22_IN(x₁)) = x₁   
POL(F23_IN(x₁, x₂, x₃)) = x₁ + x₂   
POL(F37_IN(x₁, x₂, x₃)) = [1] + x₁ + x₂   
POL(F41_IN(x₁, x₂, x₃)) = x₁   
POL(F45_IN(x₁, x₂, x₃)) = 0   
POL(F63_IN(x₁, x₂, x₃)) = x₁   
POL(U10(x₁, x₂, x₃, x₄, x₅)) = x₁   
POL(U11(x₁, x₂, x₃, x₄)) = [3] + x₁ + x₃   
POL(U11'(x₁, x₂, x₃, x₄)) = 0   
POL(U12(x₁, x₂, x₃, x₄, x₅)) = x₁   
POL(U2(x₁, x₂)) = x₁   
POL(U4(x₁, x₂, x₃, x₄)) = [1] + x₁   
POL(U5'(x₁, x₂, x₃, x₄)) = x₁ + x₃   
POL(U7'(x₁, x₂, x₃, x₄)) = x₂ + x₃   
POL(U9(x₁, x₂, x₃, x₄)) = [3] + x₁ + [2]x₃   
POL(U9'(x₁, x₂, x₃, x₄)) = x₃   
POL([]) = 0   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c19(x₁)) = x₁   
POL(c21(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(f22_in(x₁)) = [2]x₁   
POL(f22_out1(x₁)) = x₁   
POL(f37_in(x₁, x₂, x₃)) = [3] + [2]x₁ + [2]x₂   
POL(f37_out1(x₁, x₂, x₃)) = x₃   
POL(f41_in(x₁, x₂, x₃)) = [3] + [2]x₁ + x₂   
POL(f41_out1(x₁, x₂)) = x₂   
POL(f45_in(x₁, x₂, x₃)) = [2] + x₁ + x₃   
POL(f45_out1(x₁)) = x₁   
POL(nil) = 0   
POL(tree(x₁, x₂, x₃)) = [2] + x₁ + x₃   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(nil) → f1_out1([])
f1_in(tree(z0, z1, z2)) → U1(f16_in(z0, z2, z1), tree(z0, z1, z2))
U1(f16_out1(z0, z1, z2), tree(z3, z4, z5)) → f1_out1(z2)
f22_in(nil) → f22_out1([])
f22_in(tree(z0, z1, z2)) → U2(f37_in(z0, z2, z1), tree(z0, z1, z2))
U2(f37_out1(z0, z1, z2), tree(z3, z4, z5)) → f22_out1(z2)
f63_in([], z0, z1) → f63_out1(.(z0, z1))
f63_in(.(z0, z1), z2, z3) → U3(f63_in(z1, z2, z3), .(z0, z1), z2, z3)
U3(f63_out1(z0), .(z1, z2), z3, z4) → f63_out1(.(z1, z0))
f45_in([], z0, z1) → f45_out1(.(z0, z1))
f45_in(.(z0, z1), z2, z3) → U4(f45_in(z1, z2, z3), .(z0, z1), z2, z3)
U4(f45_out1(z0), .(z1, z2), z3, z4) → f45_out1(.(z1, z0))
f16_in(z0, z1, z2) → U5(f22_in(z0), z0, z1, z2)
U5(f22_out1(z0), z1, z2, z3) → U6(f23_in(z2, z0, z3), z1, z2, z3, z0)
U6(f23_out1(z0, z1), z2, z3, z4, z5) → f16_out1(z5, z0, z1)
f23_in(z0, z1, z2) → U7(f22_in(z0), z0, z1, z2)
U7(f22_out1(z0), z1, z2, z3) → U8(f63_in(z2, z3, z0), z1, z2, z3, z0)
U8(f63_out1(z0), z1, z2, z3, z4) → f23_out1(z4, z0)
f37_in(z0, z1, z2) → U9(f22_in(z0), z0, z1, z2)
U9(f22_out1(z0), z1, z2, z3) → U10(f41_in(z2, z0, z3), z1, z2, z3, z0)
U10(f41_out1(z0, z1), z2, z3, z4, z5) → f37_out1(z5, z0, z1)
f41_in(z0, z1, z2) → U11(f22_in(z0), z0, z1, z2)
U11(f22_out1(z0), z1, z2, z3) → U12(f45_in(z2, z3, z0), z1, z2, z3, z0)
U12(f45_out1(z0), z1, z2, z3, z4) → f41_out1(z4, z0)

Tuples:

F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F1_IN(tree(z0, z1, z2)) → c(F16_IN(z0, z2, z1))
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
U11'(f22_out1(z0), z1, z2, z3) → c(F45_IN(z2, z3, z0))
F22_IN(tree(z0, z1, z2)) → c4(F37_IN(z0, z2, z1))
F63_IN(.(z0, z1), z2, z3) → c7(F63_IN(z1, z2, z3))
F45_IN(.(z0, z1), z2, z3) → c10(F45_IN(z1, z2, z3))
U9'(f22_out1(z0), z1, z2, z3) → c19(F41_IN(z2, z0, z3))
F1_IN(tree(z0, z1, z2)) → c
U5'(f22_out1(z0), z1, z2, z3) → c
U7'(f22_out1(z0), z1, z2, z3) → c
U11'(f22_out1(z0), z1, z2, z3) → c

S tuples:

F45_IN(.(z0, z1), z2, z3) → c10(F45_IN(z1, z2, z3))

K tuples:

F1_IN(tree(z0, z1, z2)) → c(F16_IN(z0, z2, z1))
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
F1_IN(tree(z0, z1, z2)) → c
U5'(f22_out1(z0), z1, z2, z3) → c
U7'(f22_out1(z0), z1, z2, z3) → c
F22_IN(tree(z0, z1, z2)) → c4(F37_IN(z0, z2, z1))
F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U9'(f22_out1(z0), z1, z2, z3) → c19(F41_IN(z2, z0, z3))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U11'(f22_out1(z0), z1, z2, z3) → c(F45_IN(z2, z3, z0))
U11'(f22_out1(z0), z1, z2, z3) → c
F63_IN(.(z0, z1), z2, z3) → c7(F63_IN(z1, z2, z3))

Defined Rule Symbols:

f1_in, U1, f22_in, U2, f63_in, U3, f45_in, U4, f16_in, U5, U6, f23_in, U7, U8, f37_in, U9, U10, f41_in, U11, U12

Defined Pair Symbols:

F37_IN, F41_IN, F1_IN, F16_IN, U5', F23_IN, U7', U11', F22_IN, F63_IN, F45_IN, U9'

Compound Symbols:

c18, c21, c, c4, c7, c10, c19, c

(17) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F45_IN(.(z0, z1), z2, z3) → c10(F45_IN(z1, z2, z3))

We considered the (Usable) Rules:

f22_in(nil) → f22_out1([])
f22_in(tree(z0, z1, z2)) → U2(f37_in(z0, z2, z1), tree(z0, z1, z2))
f37_in(z0, z1, z2) → U9(f22_in(z0), z0, z1, z2)
U2(f37_out1(z0, z1, z2), tree(z3, z4, z5)) → f22_out1(z2)
U9(f22_out1(z0), z1, z2, z3) → U10(f41_in(z2, z0, z3), z1, z2, z3, z0)
f41_in(z0, z1, z2) → U11(f22_in(z0), z0, z1, z2)
U10(f41_out1(z0, z1), z2, z3, z4, z5) → f37_out1(z5, z0, z1)
U11(f22_out1(z0), z1, z2, z3) → U12(f45_in(z2, z3, z0), z1, z2, z3, z0)
f45_in([], z0, z1) → f45_out1(.(z0, z1))
f45_in(.(z0, z1), z2, z3) → U4(f45_in(z1, z2, z3), .(z0, z1), z2, z3)
U12(f45_out1(z0), z1, z2, z3, z4) → f41_out1(z4, z0)
U4(f45_out1(z0), .(z1, z2), z3, z4) → f45_out1(.(z1, z0))

And the Tuples:

F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F1_IN(tree(z0, z1, z2)) → c(F16_IN(z0, z2, z1))
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
U11'(f22_out1(z0), z1, z2, z3) → c(F45_IN(z2, z3, z0))
F22_IN(tree(z0, z1, z2)) → c4(F37_IN(z0, z2, z1))
F63_IN(.(z0, z1), z2, z3) → c7(F63_IN(z1, z2, z3))
F45_IN(.(z0, z1), z2, z3) → c10(F45_IN(z1, z2, z3))
U9'(f22_out1(z0), z1, z2, z3) → c19(F41_IN(z2, z0, z3))
F1_IN(tree(z0, z1, z2)) → c
U5'(f22_out1(z0), z1, z2, z3) → c
U7'(f22_out1(z0), z1, z2, z3) → c
U11'(f22_out1(z0), z1, z2, z3) → c

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = [1] + x₂   
POL(F16_IN(x₁, x₂, x₃)) = [1] + x₁ + x₂ + x₂·x₃ + x₁·x₃ + x₁² + x₁·x₂ + x₂²   
POL(F1_IN(x₁)) = [1] + x₁ + x₁²   
POL(F22_IN(x₁)) = x₁²   
POL(F23_IN(x₁, x₂, x₃)) = [1] + x₁²   
POL(F37_IN(x₁, x₂, x₃)) = x₁² + x₁·x₂ + x₂²   
POL(F41_IN(x₁, x₂, x₃)) = x₁² + x₁·x₂   
POL(F45_IN(x₁, x₂, x₃)) = x₁   
POL(F63_IN(x₁, x₂, x₃)) = 0   
POL(U10(x₁, x₂, x₃, x₄, x₅)) = [1] + x₁   
POL(U11(x₁, x₂, x₃, x₄)) = x₁ + x₃   
POL(U11'(x₁, x₂, x₃, x₄)) = x₁·x₃   
POL(U12(x₁, x₂, x₃, x₄, x₅)) = x₁   
POL(U2(x₁, x₂)) = x₁   
POL(U4(x₁, x₂, x₃, x₄)) = [1] + x₁   
POL(U5'(x₁, x₂, x₃, x₄)) = [1] + x₃²   
POL(U7'(x₁, x₂, x₃, x₄)) = 0   
POL(U9(x₁, x₂, x₃, x₄)) = x₁ + x₃   
POL(U9'(x₁, x₂, x₃, x₄)) = x₁·x₃ + x₃²   
POL([]) = 0   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c19(x₁)) = x₁   
POL(c21(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(f22_in(x₁)) = x₁   
POL(f22_out1(x₁)) = [1] + x₁   
POL(f37_in(x₁, x₂, x₃)) = x₁ + x₂   
POL(f37_out1(x₁, x₂, x₃)) = [1] + x₃   
POL(f41_in(x₁, x₂, x₃)) = x₁ + x₂   
POL(f41_out1(x₁, x₂)) = x₂   
POL(f45_in(x₁, x₂, x₃)) = [1] + x₁ + x₃   
POL(f45_out1(x₁)) = x₁   
POL(nil) = [1]   
POL(tree(x₁, x₂, x₃)) = x₁ + x₂ + x₃   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(nil) → f1_out1([])
f1_in(tree(z0, z1, z2)) → U1(f16_in(z0, z2, z1), tree(z0, z1, z2))
U1(f16_out1(z0, z1, z2), tree(z3, z4, z5)) → f1_out1(z2)
f22_in(nil) → f22_out1([])
f22_in(tree(z0, z1, z2)) → U2(f37_in(z0, z2, z1), tree(z0, z1, z2))
U2(f37_out1(z0, z1, z2), tree(z3, z4, z5)) → f22_out1(z2)
f63_in([], z0, z1) → f63_out1(.(z0, z1))
f63_in(.(z0, z1), z2, z3) → U3(f63_in(z1, z2, z3), .(z0, z1), z2, z3)
U3(f63_out1(z0), .(z1, z2), z3, z4) → f63_out1(.(z1, z0))
f45_in([], z0, z1) → f45_out1(.(z0, z1))
f45_in(.(z0, z1), z2, z3) → U4(f45_in(z1, z2, z3), .(z0, z1), z2, z3)
U4(f45_out1(z0), .(z1, z2), z3, z4) → f45_out1(.(z1, z0))
f16_in(z0, z1, z2) → U5(f22_in(z0), z0, z1, z2)
U5(f22_out1(z0), z1, z2, z3) → U6(f23_in(z2, z0, z3), z1, z2, z3, z0)
U6(f23_out1(z0, z1), z2, z3, z4, z5) → f16_out1(z5, z0, z1)
f23_in(z0, z1, z2) → U7(f22_in(z0), z0, z1, z2)
U7(f22_out1(z0), z1, z2, z3) → U8(f63_in(z2, z3, z0), z1, z2, z3, z0)
U8(f63_out1(z0), z1, z2, z3, z4) → f23_out1(z4, z0)
f37_in(z0, z1, z2) → U9(f22_in(z0), z0, z1, z2)
U9(f22_out1(z0), z1, z2, z3) → U10(f41_in(z2, z0, z3), z1, z2, z3, z0)
U10(f41_out1(z0, z1), z2, z3, z4, z5) → f37_out1(z5, z0, z1)
f41_in(z0, z1, z2) → U11(f22_in(z0), z0, z1, z2)
U11(f22_out1(z0), z1, z2, z3) → U12(f45_in(z2, z3, z0), z1, z2, z3, z0)
U12(f45_out1(z0), z1, z2, z3, z4) → f41_out1(z4, z0)

Tuples:

F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
F1_IN(tree(z0, z1, z2)) → c(F16_IN(z0, z2, z1))
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
U11'(f22_out1(z0), z1, z2, z3) → c(F45_IN(z2, z3, z0))
F22_IN(tree(z0, z1, z2)) → c4(F37_IN(z0, z2, z1))
F63_IN(.(z0, z1), z2, z3) → c7(F63_IN(z1, z2, z3))
F45_IN(.(z0, z1), z2, z3) → c10(F45_IN(z1, z2, z3))
U9'(f22_out1(z0), z1, z2, z3) → c19(F41_IN(z2, z0, z3))
F1_IN(tree(z0, z1, z2)) → c
U5'(f22_out1(z0), z1, z2, z3) → c
U7'(f22_out1(z0), z1, z2, z3) → c
U11'(f22_out1(z0), z1, z2, z3) → c

S tuples:none
K tuples:

F1_IN(tree(z0, z1, z2)) → c(F16_IN(z0, z2, z1))
F16_IN(z0, z1, z2) → c(U5'(f22_in(z0), z0, z1, z2))
F16_IN(z0, z1, z2) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2, z3) → c(F23_IN(z2, z0, z3))
F23_IN(z0, z1, z2) → c(U7'(f22_in(z0), z0, z1, z2))
F23_IN(z0, z1, z2) → c(F22_IN(z0))
U7'(f22_out1(z0), z1, z2, z3) → c(F63_IN(z2, z3, z0))
F1_IN(tree(z0, z1, z2)) → c
U5'(f22_out1(z0), z1, z2, z3) → c
U7'(f22_out1(z0), z1, z2, z3) → c
F22_IN(tree(z0, z1, z2)) → c4(F37_IN(z0, z2, z1))
F37_IN(z0, z1, z2) → c18(U9'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U9'(f22_out1(z0), z1, z2, z3) → c19(F41_IN(z2, z0, z3))
F41_IN(z0, z1, z2) → c21(U11'(f22_in(z0), z0, z1, z2), F22_IN(z0))
U11'(f22_out1(z0), z1, z2, z3) → c(F45_IN(z2, z3, z0))
U11'(f22_out1(z0), z1, z2, z3) → c
F63_IN(.(z0, z1), z2, z3) → c7(F63_IN(z1, z2, z3))
F45_IN(.(z0, z1), z2, z3) → c10(F45_IN(z1, z2, z3))

Defined Rule Symbols:

f1_in, U1, f22_in, U2, f63_in, U3, f45_in, U4, f16_in, U5, U6, f23_in, U7, U8, f37_in, U9, U10, f41_in, U11, U12

Defined Pair Symbols:

F37_IN, F41_IN, F1_IN, F16_IN, U5', F23_IN, U7', U11', F22_IN, F63_IN, F45_IN, U9'

Compound Symbols:

c18, c21, c, c4, c7, c10, c19, c

(19) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(20) BOUNDS(O(1), O(1))

(21) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: inorder(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: inorder(T1, T2), SCOPE: 1, CLAUSE: 0 | inorder(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: true | inorder(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: inorder(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\ninorder(T1, T2) !=? inorder(nil, [])", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: inorder(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(inorder(T7, X13), ','(inorder(T9, X14), append(X13, .(T8, X14), T11)))\n\nT7 is ground\nT8 is ground\nT9 is ground\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(inorder(T7, X13), ','(inorder(T9, X14), append(X13, .(T8, X14), T11))), SCOPE: 2, CLAUSE: 0 | ','(inorder(T7, X13), ','(inorder(T9, X14), append(X13, .(T8, X14), T11))), SCOPE: 2, CLAUSE: 2\n\nT7 is ground\nT8 is ground\nT9 is ground\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(inorder(T9, X14), append([], .(T8, X14), T11)) | ','(inorder(nil, X13), ','(inorder(T9, X14), append(X13, .(T8, X14), T11))), SCOPE: 2, CLAUSE: 2\n\nT8 is ground\nT9 is ground\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(inorder(T7, X13), ','(inorder(T9, X14), append(X13, .(T8, X14), T11))), SCOPE: 2, CLAUSE: 2\n\nT7 is ground\nT8 is ground\nT9 is ground\nX13 is free\nX14 is free\ninorder(T7, X13) !=? inorder(nil, [])", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(inorder(T9, X14), append([], .(T8, X14), T11))\n\nT8 is ground\nT9 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(inorder(nil, X13), ','(inorder(T9, X14), append(X13, .(T8, X14), T11))), SCOPE: 2, CLAUSE: 2\n\nT8 is ground\nT9 is ground\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: inorder(T9, X14)\n\nT9 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: append([], .(T8, T12), T11)\n\nT8 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: inorder(T9, X14), SCOPE: 3, CLAUSE: 0 | inorder(T9, X14), SCOPE: 3, CLAUSE: 2\n\nT9 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: true | inorder(nil, X14), SCOPE: 3, CLAUSE: 2\n\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: inorder(T9, X14), SCOPE: 3, CLAUSE: 2\n\nT9 is ground\nX14 is free\ninorder(T9, X14) !=? inorder(nil, [])", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: inorder(nil, X14), SCOPE: 3, CLAUSE: 2\n\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(inorder(T19, X35), ','(inorder(T21, X36), append(X35, .(T20, X36), X37)))\n\nT19 is ground\nT20 is ground\nT21 is ground\nX37 is free\nX35 is free\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: inorder(T19, X35)\n\nT19 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(inorder(T21, X36), append(T22, .(T20, X36), X37))\n\nT20 is ground\nT21 is ground\nT22 is ground\nX37 is free\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: inorder(T21, X36)\n\nT21 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: append(T22, .(T20, T23), X37)\n\nT20 is ground\nT22 is ground\nT23 is ground\nX37 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: append(T22, .(T20, T23), X37), SCOPE: 4, CLAUSE: 1 | append(T22, .(T20, T23), X37), SCOPE: 4, CLAUSE: 3\n\nT20 is ground\nT22 is ground\nT23 is ground\nX37 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: true | append([], .(T32, T33), X37), SCOPE: 4, CLAUSE: 3\n\nT32 is ground\nT33 is ground\nX37 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: append(T22, .(T20, T23), X37), SCOPE: 4, CLAUSE: 3\n\nT20 is ground\nT22 is ground\nT23 is ground\nX37 is free\nX42 is free\nappend(T22, .(T20, T23), X37) !=? append([], X42, X42)", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: append([], .(T32, T33), X37), SCOPE: 4, CLAUSE: 3\n\nT32 is ground\nT33 is ground\nX37 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: append(T43, .(T44, T45), X61)\n\nT43 is ground\nT44 is ground\nT45 is ground\nX61 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: append([], .(T8, T12), T11), SCOPE: 5, CLAUSE: 1 | append([], .(T8, T12), T11), SCOPE: 5, CLAUSE: 3\n\nT8 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: true | append([], .(T58, T59), T11), SCOPE: 5, CLAUSE: 3\n\nT58 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: append([], .(T8, T12), T11), SCOPE: 5, CLAUSE: 3\n\nT8 is ground\nT12 is ground\nX68 is free\nappend([], .(T8, T12), T11) !=? append([], X68, X68)", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: append([], .(T58, T59), T11), SCOPE: 5, CLAUSE: 3\n\nT58 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(','(inorder(T66, X97), ','(inorder(T68, X98), append(X97, .(T67, X98), X99))), ','(inorder(T9, X14), append(X99, .(T8, X14), T11)))\n\nT8 is ground\nT9 is ground\nT66 is ground\nT67 is ground\nT68 is ground\nX14 is free\nX99 is free\nX97 is free\nX98 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: inorder(T66, X97)\n\nT66 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(','(inorder(T68, X98), append(T69, .(T67, X98), X99)), ','(inorder(T9, X14), append(X99, .(T8, X14), T11)))\n\nT8 is ground\nT9 is ground\nT67 is ground\nT68 is ground\nT69 is ground\nX14 is free\nX99 is free\nX98 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: inorder(T68, X98)\n\nT68 is ground\nX98 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ','(append(T69, .(T67, T70), X99), ','(inorder(T9, X14), append(X99, .(T8, X14), T11)))\n\nT8 is ground\nT9 is ground\nT67 is ground\nT69 is ground\nT70 is ground\nX14 is free\nX99 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: append(T69, .(T67, T70), X99)\n\nT67 is ground\nT69 is ground\nT70 is ground\nX99 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(inorder(T9, X14), append(T75, .(T8, X14), T11))\n\nT8 is ground\nT9 is ground\nT75 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: inorder(T9, X14)\n\nT9 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: append(T75, .(T8, T80), T11)\n\nT8 is ground\nT75 is ground\nT80 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: append(T75, .(T8, T80), T11), SCOPE: 6, CLAUSE: 1 | append(T75, .(T8, T80), T11), SCOPE: 6, CLAUSE: 3\n\nT8 is ground\nT75 is ground\nT80 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: true | append([], .(T89, T90), T11), SCOPE: 6, CLAUSE: 3\n\nT89 is ground\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: append(T75, .(T8, T80), T11), SCOPE: 6, CLAUSE: 3\n\nT8 is ground\nT75 is ground\nT80 is ground\nX108 is free\nappend(T75, .(T8, T80), T11) !=? append([], X108, X108)", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: append([], .(T89, T90), T11), SCOPE: 6, CLAUSE: 3\n\nT89 is ground\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: append(T102, .(T103, T104), T106)\n\nT102 is ground\nT103 is ground\nT104 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 95 [arrowhead = none ];
95 -> 4;

96 [label="EVAL with clause\ninorder(nil, []).\nand substitutionT1 -> nil,\nT2 -> []", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 96 [arrowhead = none ];
96 -> 6;

97 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 97 [arrowhead = none ];
97 -> 7;

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

99 [label="EVAL with clause\ninorder(tree(X9, X10, X11), X12) :- ','(inorder(X9, X13), ','(inorder(X11, X14), append(X13, .(X10, X14), X12))).\nand substitutionX9 -> T7,\nX10 -> T8,\nX11 -> T9,\nT1 -> tree(T7, T8, T9),\nT2 -> T11,\nX12 -> T11,\nT10 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 99 [arrowhead = none ];
99 -> 13;

100 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 100 [arrowhead = none ];
100 -> 14;

101 [label="BACKTRACK\nfor clause: inorder(tree(L, V, R), I) :- ','(inorder(L, LI), ','(inorder(R, RI), append(LI, .(V, RI), I)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 101 [arrowhead = none ];
101 -> 10;

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

103 [label="EVAL with clause\ninorder(nil, []).\nand substitutionT7 -> nil,\nX13 -> []", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 103 [arrowhead = none ];
103 -> 17;

104 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 104 [arrowhead = none ];
104 -> 19;

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

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

107 [label="EVAL with clause\ninorder(tree(X93, X94, X95), X96) :- ','(inorder(X93, X97), ','(inorder(X95, X98), append(X97, .(X94, X98), X96))).\nand substitutionX93 -> T66,\nX94 -> T67,\nX95 -> T68,\nT7 -> tree(T66, T67, T68),\nX13 -> X99,\nX96 -> X99", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 107 [arrowhead = none ];
107 -> 76;

108 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 108 [arrowhead = none ];
108 -> 77;

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

110 [label="SPLIT 2\nnew knowledge:\nT9 is ground\nT12 is ground\nreplacements:X14 -> T12", fontsize=14, style = filled, fillcolor = violet];
20 -> 110 [arrowhead = none ];
110 -> 25;

111 [label="BACKTRACK\nfor clause: inorder(tree(L, V, R), I) :- ','(inorder(L, LI), ','(inorder(R, RI), append(LI, .(V, RI), I)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 111 [arrowhead = none ];
111 -> 73;

112 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
24 -> 112 [arrowhead = none ];
112 -> 27;

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

114 [label="EVAL with clause\ninorder(nil, []).\nand substitutionT9 -> nil,\nX14 -> []", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 114 [arrowhead = none ];
114 -> 29;

115 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 115 [arrowhead = none ];
115 -> 31;

116 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 116 [arrowhead = none ];
116 -> 33;

117 [label="EVAL with clause\ninorder(tree(X31, X32, X33), X34) :- ','(inorder(X31, X35), ','(inorder(X33, X36), append(X35, .(X32, X36), X34))).\nand substitutionX31 -> T19,\nX32 -> T20,\nX33 -> T21,\nT9 -> tree(T19, T20, T21),\nX14 -> X37,\nX34 -> X37", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 117 [arrowhead = none ];
117 -> 36;

118 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 118 [arrowhead = none ];
118 -> 38;

119 [label="BACKTRACK\nfor clause: inorder(tree(L, V, R), I) :- ','(inorder(L, LI), ','(inorder(R, RI), append(LI, .(V, RI), I)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 119 [arrowhead = none ];
119 -> 35;

120 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
36 -> 120 [arrowhead = none ];
120 -> 42;

121 [label="SPLIT 2\nnew knowledge:\nT19 is ground\nT22 is ground\nreplacements:X35 -> T22", fontsize=14, style = filled, fillcolor = violet];
36 -> 121 [arrowhead = none ];
121 -> 43;

122 [label="INSTANCE with matching:\nT9 -> T19\nX14 -> X35", fontsize=14, style = filled, fillcolor = lightgrey];
42 -> 122 [arrowhead = none , style=dashed];
122 -> 24[style=dashed];

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

124 [label="SPLIT 2\nnew knowledge:\nT21 is ground\nT23 is ground\nreplacements:X36 -> T23", fontsize=14, style = filled, fillcolor = violet];
43 -> 124 [arrowhead = none ];
124 -> 47;

125 [label="INSTANCE with matching:\nT9 -> T21\nX14 -> X36", fontsize=14, style = filled, fillcolor = lightgrey];
46 -> 125 [arrowhead = none , style=dashed];
125 -> 24[style=dashed];

126 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
47 -> 126 [arrowhead = none ];
126 -> 49;

127 [label="EVAL with clause\nappend([], X42, X42).\nand substitutionT22 -> [],\nT20 -> T32,\nT23 -> T33,\nX42 -> .(T32, T33),\nX37 -> .(T32, T33)", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 127 [arrowhead = none ];
127 -> 52;

128 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 128 [arrowhead = none ];
128 -> 54;

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

130 [label="EVAL with clause\nappend(.(X57, X58), X59, .(X57, X60)) :- append(X58, X59, X60).\nand substitutionX57 -> T42,\nX58 -> T43,\nT22 -> .(T42, T43),\nT20 -> T44,\nT23 -> T45,\nX59 -> .(T44, T45),\nX60 -> X61,\nX37 -> .(T42, X61)", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 130 [arrowhead = none ];
130 -> 60;

131 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 131 [arrowhead = none ];
131 -> 61;

132 [label="BACKTRACK\nfor clause: append(.(X, Xs), Ys, .(X, Zs)) :- append(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
56 -> 132 [arrowhead = none ];
132 -> 57;

133 [label="INSTANCE with matching:\nT22 -> T43\nT20 -> T44\nT23 -> T45\nX37 -> X61", fontsize=14, style = filled, fillcolor = lightgrey];
60 -> 133 [arrowhead = none , style=dashed];
133 -> 47[style=dashed];

134 [label="EVAL with clause\nappend([], X68, X68).\nand substitutionT8 -> T58,\nT12 -> T59,\nX68 -> .(T58, T59),\nT11 -> .(T58, T59)", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 134 [arrowhead = none ];
134 -> 66;

135 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 135 [arrowhead = none ];
135 -> 67;

136 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
66 -> 136 [arrowhead = none ];
136 -> 68;

137 [label="BACKTRACK\nfor clause: append(.(X, Xs), Ys, .(X, Zs)) :- append(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
67 -> 137 [arrowhead = none ];
137 -> 71;

138 [label="BACKTRACK\nfor clause: append(.(X, Xs), Ys, .(X, Zs)) :- append(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
68 -> 138 [arrowhead = none ];
138 -> 69;

139 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
76 -> 139 [arrowhead = none ];
139 -> 80;

140 [label="SPLIT 2\nnew knowledge:\nT66 is ground\nT69 is ground\nreplacements:X97 -> T69", fontsize=14, style = filled, fillcolor = violet];
76 -> 140 [arrowhead = none ];
140 -> 81;

141 [label="INSTANCE with matching:\nT9 -> T66\nX14 -> X97", fontsize=14, style = filled, fillcolor = lightgrey];
80 -> 141 [arrowhead = none , style=dashed];
141 -> 24[style=dashed];

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

143 [label="SPLIT 2\nnew knowledge:\nT68 is ground\nT70 is ground\nreplacements:X98 -> T70", fontsize=14, style = filled, fillcolor = violet];
81 -> 143 [arrowhead = none ];
143 -> 83;

144 [label="INSTANCE with matching:\nT9 -> T68\nX14 -> X98", fontsize=14, style = filled, fillcolor = lightgrey];
82 -> 144 [arrowhead = none , style=dashed];
144 -> 24[style=dashed];

145 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
83 -> 145 [arrowhead = none ];
145 -> 84;

146 [label="SPLIT 2\nnew knowledge:\nT69 is ground\nT67 is ground\nT70 is ground\nT75 is ground\nreplacements:X99 -> T75", fontsize=14, style = filled, fillcolor = violet];
83 -> 146 [arrowhead = none ];
146 -> 85;

147 [label="INSTANCE with matching:\nT22 -> T69\nT20 -> T67\nT23 -> T70\nX37 -> X99", fontsize=14, style = filled, fillcolor = lightgrey];
84 -> 147 [arrowhead = none , style=dashed];
147 -> 47[style=dashed];

148 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
85 -> 148 [arrowhead = none ];
148 -> 86;

149 [label="SPLIT 2\nnew knowledge:\nT9 is ground\nT80 is ground\nreplacements:X14 -> T80", fontsize=14, style = filled, fillcolor = violet];
85 -> 149 [arrowhead = none ];
149 -> 87;

150 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
86 -> 150 [arrowhead = none , style=dashed];
150 -> 24[style=dashed];

151 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
87 -> 151 [arrowhead = none ];
151 -> 88;

152 [label="EVAL with clause\nappend([], X108, X108).\nand substitutionT75 -> [],\nT8 -> T89,\nT80 -> T90,\nX108 -> .(T89, T90),\nT11 -> .(T89, T90)", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 152 [arrowhead = none ];
152 -> 89;

153 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 153 [arrowhead = none ];
153 -> 90;

154 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
89 -> 154 [arrowhead = none ];
154 -> 91;

155 [label="EVAL with clause\nappend(.(X121, X122), X123, .(X121, X124)) :- append(X122, X123, X124).\nand substitutionX121 -> T101,\nX122 -> T102,\nT75 -> .(T101, T102),\nT8 -> T103,\nT80 -> T104,\nX123 -> .(T103, T104),\nX124 -> T106,\nT11 -> .(T101, T106),\nT105 -> T106", fontsize=14, style = filled, fillcolor = lightblue];
90 -> 155 [arrowhead = none ];
155 -> 93;

156 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
90 -> 156 [arrowhead = none ];
156 -> 94;

157 [label="BACKTRACK\nfor clause: append(.(X, Xs), Ys, .(X, Zs)) :- append(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
91 -> 157 [arrowhead = none ];
157 -> 92;

158 [label="INSTANCE with matching:\nT75 -> T102\nT8 -> T103\nT80 -> T104\nT11 -> T106", fontsize=14, style = filled, fillcolor = lightgrey];
93 -> 158 [arrowhead = none , style=dashed];
158 -> 87[style=dashed];

}

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1([])
f2_in(tree(nil, z0, z1)) → U1(f17_in(z1, z0), tree(nil, z0, z1))
f2_in(tree(tree(z0, z1, z2), z3, z4)) → U2(f76_in(z0, z2, z1, z4, z3), tree(tree(z0, z1, z2), z3, z4))
U1(f17_out1(z0, z1), tree(nil, z2, z3)) → f2_out1(z1)
U1(f17_out2(z0, z1, z2), tree(nil, z3, z4)) → f2_out1(z2)
U2(f76_out1(z0, z1, z2, z3, z4), tree(tree(z5, z6, z7), z8, z9)) → f2_out1(z4)
f24_in(nil) → f24_out1([])
f24_in(tree(z0, z1, z2)) → U3(f36_in(z0, z2, z1), tree(z0, z1, z2))
U3(f36_out1(z0, z1, z2), tree(z3, z4, z5)) → f24_out1(z2)
f47_in([], z0, z1) → f47_out1(.(z0, z1))
f47_in(.(z0, z1), z2, z3) → U4(f47_in(z1, z2, z3), .(z0, z1), z2, z3)
U4(f47_out1(z0), .(z1, z2), z3, z4) → f47_out1(.(z1, z0))
f87_in([], z0, z1) → f87_out1(.(z0, z1))
f87_in(.(z0, z1), z2, z3) → U5(f87_in(z1, z2, z3), .(z0, z1), z2, z3)
U5(f87_out1(z0), .(z1, z2), z3, z4) → f87_out1(.(z1, z0))
f25_in(z0, z1) → f25_out1(.(z0, z1))
f20_in(z0, z1) → U6(f24_in(z0), z0, z1)
U6(f24_out1(z0), z1, z2) → U7(f25_in(z2, z0), z1, z2, z0)
U7(f25_out1(z0), z1, z2, z3) → f20_out1(z3, z0)
f36_in(z0, z1, z2) → U8(f24_in(z0), z0, z1, z2)
U8(f24_out1(z0), z1, z2, z3) → U9(f43_in(z2, z0, z3), z1, z2, z3, z0)
U9(f43_out1(z0, z1), z2, z3, z4, z5) → f36_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U10(f24_in(z0), z0, z1, z2)
U10(f24_out1(z0), z1, z2, z3) → U11(f47_in(z2, z3, z0), z1, z2, z3, z0)
U11(f47_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f76_in(z0, z1, z2, z3, z4) → U12(f24_in(z0), z0, z1, z2, z3, z4)
U12(f24_out1(z0), z1, z2, z3, z4, z5) → U13(f81_in(z2, z0, z3, z4, z5), z1, z2, z3, z4, z5, z0)
U13(f81_out1(z0, z1, z2, z3), z4, z5, z6, z7, z8, z9) → f76_out1(z9, z0, z1, z2, z3)
f81_in(z0, z1, z2, z3, z4) → U14(f24_in(z0), z0, z1, z2, z3, z4)
U14(f24_out1(z0), z1, z2, z3, z4, z5) → U15(f83_in(z2, z3, z0, z4, z5), z1, z2, z3, z4, z5, z0)
U15(f83_out1(z0, z1, z2), z3, z4, z5, z6, z7, z8) → f81_out1(z8, z0, z1, z2)
f83_in(z0, z1, z2, z3, z4) → U16(f47_in(z0, z1, z2), z0, z1, z2, z3, z4)
U16(f47_out1(z0), z1, z2, z3, z4, z5) → U17(f85_in(z4, z0, z5), z1, z2, z3, z4, z5, z0)
U17(f85_out1(z0, z1), z2, z3, z4, z5, z6, z7) → f83_out1(z7, z0, z1)
f85_in(z0, z1, z2) → U18(f24_in(z0), z0, z1, z2)
U18(f24_out1(z0), z1, z2, z3) → U19(f87_in(z2, z3, z0), z1, z2, z3, z0)
U19(f87_out1(z0), z1, z2, z3, z4) → f85_out1(z4, z0)
f17_in(z0, z1) → U20(f20_in(z0, z1), f21_in(z0, z1), z0, z1)
U20(f20_out1(z0, z1), z2, z3, z4) → f17_out1(z0, z1)
U20(z0, f21_out1(z1, z2, z3), z4, z5) → f17_out2(z1, z2, z3)

Tuples:

F2_IN(tree(nil, z0, z1)) → c1(U1'(f17_in(z1, z0), tree(nil, z0, z1)), F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c2(U2'(f76_in(z0, z2, z1, z4, z3), tree(tree(z0, z1, z2), z3, z4)), F76_IN(z0, z2, z1, z4, z3))
F24_IN(tree(z0, z1, z2)) → c7(U3'(f36_in(z0, z2, z1), tree(z0, z1, z2)), F36_IN(z0, z2, z1))
F47_IN(.(z0, z1), z2, z3) → c10(U4'(f47_in(z1, z2, z3), .(z0, z1), z2, z3), F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(U5'(f87_in(z1, z2, z3), .(z0, z1), z2, z3), F87_IN(z1, z2, z3))
F20_IN(z0, z1) → c16(U6'(f24_in(z0), z0, z1), F24_IN(z0))
U6'(f24_out1(z0), z1, z2) → c17(U7'(f25_in(z2, z0), z1, z2, z0), F25_IN(z2, z0))
F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
U8'(f24_out1(z0), z1, z2, z3) → c20(U9'(f43_in(z2, z0, z3), z1, z2, z3, z0), F43_IN(z2, z0, z3))
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c23(U11'(f47_in(z2, z3, z0), z1, z2, z3, z0), F47_IN(z2, z3, z0))
F76_IN(z0, z1, z2, z3, z4) → c25(U12'(f24_in(z0), z0, z1, z2, z3, z4), F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c26(U13'(f81_in(z2, z0, z3, z4, z5), z1, z2, z3, z4, z5, z0), F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c28(U14'(f24_in(z0), z0, z1, z2, z3, z4), F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c29(U15'(f83_in(z2, z3, z0, z4, z5), z1, z2, z3, z4, z5, z0), F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c31(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4), F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c32(U17'(f85_in(z4, z0, z5), z1, z2, z3, z4, z5, z0), F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c34(U18'(f24_in(z0), z0, z1, z2), F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c35(U19'(f87_in(z2, z3, z0), z1, z2, z3, z0), F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c37(U20'(f20_in(z0, z1), f21_in(z0, z1), z0, z1), F20_IN(z0, z1))

S tuples:

F2_IN(tree(nil, z0, z1)) → c1(U1'(f17_in(z1, z0), tree(nil, z0, z1)), F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c2(U2'(f76_in(z0, z2, z1, z4, z3), tree(tree(z0, z1, z2), z3, z4)), F76_IN(z0, z2, z1, z4, z3))
F24_IN(tree(z0, z1, z2)) → c7(U3'(f36_in(z0, z2, z1), tree(z0, z1, z2)), F36_IN(z0, z2, z1))
F47_IN(.(z0, z1), z2, z3) → c10(U4'(f47_in(z1, z2, z3), .(z0, z1), z2, z3), F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(U5'(f87_in(z1, z2, z3), .(z0, z1), z2, z3), F87_IN(z1, z2, z3))
F20_IN(z0, z1) → c16(U6'(f24_in(z0), z0, z1), F24_IN(z0))
U6'(f24_out1(z0), z1, z2) → c17(U7'(f25_in(z2, z0), z1, z2, z0), F25_IN(z2, z0))
F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
U8'(f24_out1(z0), z1, z2, z3) → c20(U9'(f43_in(z2, z0, z3), z1, z2, z3, z0), F43_IN(z2, z0, z3))
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c23(U11'(f47_in(z2, z3, z0), z1, z2, z3, z0), F47_IN(z2, z3, z0))
F76_IN(z0, z1, z2, z3, z4) → c25(U12'(f24_in(z0), z0, z1, z2, z3, z4), F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c26(U13'(f81_in(z2, z0, z3, z4, z5), z1, z2, z3, z4, z5, z0), F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c28(U14'(f24_in(z0), z0, z1, z2, z3, z4), F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c29(U15'(f83_in(z2, z3, z0, z4, z5), z1, z2, z3, z4, z5, z0), F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c31(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4), F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c32(U17'(f85_in(z4, z0, z5), z1, z2, z3, z4, z5, z0), F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c34(U18'(f24_in(z0), z0, z1, z2), F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c35(U19'(f87_in(z2, z3, z0), z1, z2, z3, z0), F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c37(U20'(f20_in(z0, z1), f21_in(z0, z1), z0, z1), F20_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, f24_in, U3, f47_in, U4, f87_in, U5, f25_in, f20_in, U6, U7, f36_in, U8, U9, f43_in, U10, U11, f76_in, U12, U13, f81_in, U14, U15, f83_in, U16, U17, f85_in, U18, U19, f17_in, U20

Defined Pair Symbols:

F2_IN, F24_IN, F47_IN, F87_IN, F20_IN, U6', F36_IN, U8', F43_IN, U10', F76_IN, U12', F81_IN, U14', F83_IN, U16', F85_IN, U18', F17_IN

Compound Symbols:

c1, c2, c7, c10, c13, c16, c17, c19, c20, c22, c23, c25, c26, c28, c29, c31, c32, c34, c35, c37

(23) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1([])
f2_in(tree(nil, z0, z1)) → U1(f17_in(z1, z0), tree(nil, z0, z1))
f2_in(tree(tree(z0, z1, z2), z3, z4)) → U2(f76_in(z0, z2, z1, z4, z3), tree(tree(z0, z1, z2), z3, z4))
U1(f17_out1(z0, z1), tree(nil, z2, z3)) → f2_out1(z1)
U1(f17_out2(z0, z1, z2), tree(nil, z3, z4)) → f2_out1(z2)
U2(f76_out1(z0, z1, z2, z3, z4), tree(tree(z5, z6, z7), z8, z9)) → f2_out1(z4)
f24_in(nil) → f24_out1([])
f24_in(tree(z0, z1, z2)) → U3(f36_in(z0, z2, z1), tree(z0, z1, z2))
U3(f36_out1(z0, z1, z2), tree(z3, z4, z5)) → f24_out1(z2)
f47_in([], z0, z1) → f47_out1(.(z0, z1))
f47_in(.(z0, z1), z2, z3) → U4(f47_in(z1, z2, z3), .(z0, z1), z2, z3)
U4(f47_out1(z0), .(z1, z2), z3, z4) → f47_out1(.(z1, z0))
f87_in([], z0, z1) → f87_out1(.(z0, z1))
f87_in(.(z0, z1), z2, z3) → U5(f87_in(z1, z2, z3), .(z0, z1), z2, z3)
U5(f87_out1(z0), .(z1, z2), z3, z4) → f87_out1(.(z1, z0))
f25_in(z0, z1) → f25_out1(.(z0, z1))
f20_in(z0, z1) → U6(f24_in(z0), z0, z1)
U6(f24_out1(z0), z1, z2) → U7(f25_in(z2, z0), z1, z2, z0)
U7(f25_out1(z0), z1, z2, z3) → f20_out1(z3, z0)
f36_in(z0, z1, z2) → U8(f24_in(z0), z0, z1, z2)
U8(f24_out1(z0), z1, z2, z3) → U9(f43_in(z2, z0, z3), z1, z2, z3, z0)
U9(f43_out1(z0, z1), z2, z3, z4, z5) → f36_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U10(f24_in(z0), z0, z1, z2)
U10(f24_out1(z0), z1, z2, z3) → U11(f47_in(z2, z3, z0), z1, z2, z3, z0)
U11(f47_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f76_in(z0, z1, z2, z3, z4) → U12(f24_in(z0), z0, z1, z2, z3, z4)
U12(f24_out1(z0), z1, z2, z3, z4, z5) → U13(f81_in(z2, z0, z3, z4, z5), z1, z2, z3, z4, z5, z0)
U13(f81_out1(z0, z1, z2, z3), z4, z5, z6, z7, z8, z9) → f76_out1(z9, z0, z1, z2, z3)
f81_in(z0, z1, z2, z3, z4) → U14(f24_in(z0), z0, z1, z2, z3, z4)
U14(f24_out1(z0), z1, z2, z3, z4, z5) → U15(f83_in(z2, z3, z0, z4, z5), z1, z2, z3, z4, z5, z0)
U15(f83_out1(z0, z1, z2), z3, z4, z5, z6, z7, z8) → f81_out1(z8, z0, z1, z2)
f83_in(z0, z1, z2, z3, z4) → U16(f47_in(z0, z1, z2), z0, z1, z2, z3, z4)
U16(f47_out1(z0), z1, z2, z3, z4, z5) → U17(f85_in(z4, z0, z5), z1, z2, z3, z4, z5, z0)
U17(f85_out1(z0, z1), z2, z3, z4, z5, z6, z7) → f83_out1(z7, z0, z1)
f85_in(z0, z1, z2) → U18(f24_in(z0), z0, z1, z2)
U18(f24_out1(z0), z1, z2, z3) → U19(f87_in(z2, z3, z0), z1, z2, z3, z0)
U19(f87_out1(z0), z1, z2, z3, z4) → f85_out1(z4, z0)
f17_in(z0, z1) → U20(f20_in(z0, z1), f21_in(z0, z1), z0, z1)
U20(f20_out1(z0, z1), z2, z3, z4) → f17_out1(z0, z1)
U20(z0, f21_out1(z1, z2, z3), z4, z5) → f17_out2(z1, z2, z3)

Tuples:

F24_IN(tree(z0, z1, z2)) → c7(U3'(f36_in(z0, z2, z1), tree(z0, z1, z2)), F36_IN(z0, z2, z1))
F47_IN(.(z0, z1), z2, z3) → c10(U4'(f47_in(z1, z2, z3), .(z0, z1), z2, z3), F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(U5'(f87_in(z1, z2, z3), .(z0, z1), z2, z3), F87_IN(z1, z2, z3))
F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
U8'(f24_out1(z0), z1, z2, z3) → c20(U9'(f43_in(z2, z0, z3), z1, z2, z3, z0), F43_IN(z2, z0, z3))
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F2_IN(tree(nil, z0, z1)) → c(U1'(f17_in(z1, z0), tree(nil, z0, z1)))
F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(U2'(f76_in(z0, z2, z1, z4, z3), tree(tree(z0, z1, z2), z3, z4)))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U6'(f24_out1(z0), z1, z2) → c(U7'(f25_in(z2, z0), z1, z2, z0))
U6'(f24_out1(z0), z1, z2) → c(F25_IN(z2, z0))
U10'(f24_out1(z0), z1, z2, z3) → c(U11'(f47_in(z2, z3, z0), z1, z2, z3, z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(U13'(f81_in(z2, z0, z3, z4, z5), z1, z2, z3, z4, z5, z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(U15'(f83_in(z2, z3, z0, z4, z5), z1, z2, z3, z4, z5, z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(U17'(f85_in(z4, z0, z5), z1, z2, z3, z4, z5, z0))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(U19'(f87_in(z2, z3, z0), z1, z2, z3, z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(U20'(f20_in(z0, z1), f21_in(z0, z1), z0, z1))
F17_IN(z0, z1) → c(F20_IN(z0, z1))

S tuples:

F24_IN(tree(z0, z1, z2)) → c7(U3'(f36_in(z0, z2, z1), tree(z0, z1, z2)), F36_IN(z0, z2, z1))
F47_IN(.(z0, z1), z2, z3) → c10(U4'(f47_in(z1, z2, z3), .(z0, z1), z2, z3), F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(U5'(f87_in(z1, z2, z3), .(z0, z1), z2, z3), F87_IN(z1, z2, z3))
F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
U8'(f24_out1(z0), z1, z2, z3) → c20(U9'(f43_in(z2, z0, z3), z1, z2, z3, z0), F43_IN(z2, z0, z3))
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F2_IN(tree(nil, z0, z1)) → c(U1'(f17_in(z1, z0), tree(nil, z0, z1)))
F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(U2'(f76_in(z0, z2, z1, z4, z3), tree(tree(z0, z1, z2), z3, z4)))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U6'(f24_out1(z0), z1, z2) → c(U7'(f25_in(z2, z0), z1, z2, z0))
U6'(f24_out1(z0), z1, z2) → c(F25_IN(z2, z0))
U10'(f24_out1(z0), z1, z2, z3) → c(U11'(f47_in(z2, z3, z0), z1, z2, z3, z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(U13'(f81_in(z2, z0, z3, z4, z5), z1, z2, z3, z4, z5, z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(U15'(f83_in(z2, z3, z0, z4, z5), z1, z2, z3, z4, z5, z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(U17'(f85_in(z4, z0, z5), z1, z2, z3, z4, z5, z0))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(U19'(f87_in(z2, z3, z0), z1, z2, z3, z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(U20'(f20_in(z0, z1), f21_in(z0, z1), z0, z1))
F17_IN(z0, z1) → c(F20_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, f24_in, U3, f47_in, U4, f87_in, U5, f25_in, f20_in, U6, U7, f36_in, U8, U9, f43_in, U10, U11, f76_in, U12, U13, f81_in, U14, U15, f83_in, U16, U17, f85_in, U18, U19, f17_in, U20

Defined Pair Symbols:

F24_IN, F47_IN, F87_IN, F36_IN, U8', F43_IN, F2_IN, F20_IN, U6', U10', F76_IN, U12', F81_IN, U14', F83_IN, U16', F85_IN, U18', F17_IN

Compound Symbols:

c7, c10, c13, c19, c20, c22, c

(25) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 14 trailing tuple parts

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1([])
f2_in(tree(nil, z0, z1)) → U1(f17_in(z1, z0), tree(nil, z0, z1))
f2_in(tree(tree(z0, z1, z2), z3, z4)) → U2(f76_in(z0, z2, z1, z4, z3), tree(tree(z0, z1, z2), z3, z4))
U1(f17_out1(z0, z1), tree(nil, z2, z3)) → f2_out1(z1)
U1(f17_out2(z0, z1, z2), tree(nil, z3, z4)) → f2_out1(z2)
U2(f76_out1(z0, z1, z2, z3, z4), tree(tree(z5, z6, z7), z8, z9)) → f2_out1(z4)
f24_in(nil) → f24_out1([])
f24_in(tree(z0, z1, z2)) → U3(f36_in(z0, z2, z1), tree(z0, z1, z2))
U3(f36_out1(z0, z1, z2), tree(z3, z4, z5)) → f24_out1(z2)
f47_in([], z0, z1) → f47_out1(.(z0, z1))
f47_in(.(z0, z1), z2, z3) → U4(f47_in(z1, z2, z3), .(z0, z1), z2, z3)
U4(f47_out1(z0), .(z1, z2), z3, z4) → f47_out1(.(z1, z0))
f87_in([], z0, z1) → f87_out1(.(z0, z1))
f87_in(.(z0, z1), z2, z3) → U5(f87_in(z1, z2, z3), .(z0, z1), z2, z3)
U5(f87_out1(z0), .(z1, z2), z3, z4) → f87_out1(.(z1, z0))
f25_in(z0, z1) → f25_out1(.(z0, z1))
f20_in(z0, z1) → U6(f24_in(z0), z0, z1)
U6(f24_out1(z0), z1, z2) → U7(f25_in(z2, z0), z1, z2, z0)
U7(f25_out1(z0), z1, z2, z3) → f20_out1(z3, z0)
f36_in(z0, z1, z2) → U8(f24_in(z0), z0, z1, z2)
U8(f24_out1(z0), z1, z2, z3) → U9(f43_in(z2, z0, z3), z1, z2, z3, z0)
U9(f43_out1(z0, z1), z2, z3, z4, z5) → f36_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U10(f24_in(z0), z0, z1, z2)
U10(f24_out1(z0), z1, z2, z3) → U11(f47_in(z2, z3, z0), z1, z2, z3, z0)
U11(f47_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f76_in(z0, z1, z2, z3, z4) → U12(f24_in(z0), z0, z1, z2, z3, z4)
U12(f24_out1(z0), z1, z2, z3, z4, z5) → U13(f81_in(z2, z0, z3, z4, z5), z1, z2, z3, z4, z5, z0)
U13(f81_out1(z0, z1, z2, z3), z4, z5, z6, z7, z8, z9) → f76_out1(z9, z0, z1, z2, z3)
f81_in(z0, z1, z2, z3, z4) → U14(f24_in(z0), z0, z1, z2, z3, z4)
U14(f24_out1(z0), z1, z2, z3, z4, z5) → U15(f83_in(z2, z3, z0, z4, z5), z1, z2, z3, z4, z5, z0)
U15(f83_out1(z0, z1, z2), z3, z4, z5, z6, z7, z8) → f81_out1(z8, z0, z1, z2)
f83_in(z0, z1, z2, z3, z4) → U16(f47_in(z0, z1, z2), z0, z1, z2, z3, z4)
U16(f47_out1(z0), z1, z2, z3, z4, z5) → U17(f85_in(z4, z0, z5), z1, z2, z3, z4, z5, z0)
U17(f85_out1(z0, z1), z2, z3, z4, z5, z6, z7) → f83_out1(z7, z0, z1)
f85_in(z0, z1, z2) → U18(f24_in(z0), z0, z1, z2)
U18(f24_out1(z0), z1, z2, z3) → U19(f87_in(z2, z3, z0), z1, z2, z3, z0)
U19(f87_out1(z0), z1, z2, z3, z4) → f85_out1(z4, z0)
f17_in(z0, z1) → U20(f20_in(z0, z1), f21_in(z0, z1), z0, z1)
U20(f20_out1(z0, z1), z2, z3, z4) → f17_out1(z0, z1)
U20(z0, f21_out1(z1, z2, z3), z4, z5) → f17_out2(z1, z2, z3)

Tuples:

F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))
F47_IN(.(z0, z1), z2, z3) → c10(F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(F87_IN(z1, z2, z3))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))
F2_IN(tree(nil, z0, z1)) → c
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c
U6'(f24_out1(z0), z1, z2) → c
U10'(f24_out1(z0), z1, z2, z3) → c
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
U18'(f24_out1(z0), z1, z2, z3) → c
F17_IN(z0, z1) → c

S tuples:

F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))
F47_IN(.(z0, z1), z2, z3) → c10(F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(F87_IN(z1, z2, z3))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))
F2_IN(tree(nil, z0, z1)) → c
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c
U6'(f24_out1(z0), z1, z2) → c
U10'(f24_out1(z0), z1, z2, z3) → c
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
U18'(f24_out1(z0), z1, z2, z3) → c
F17_IN(z0, z1) → c

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, f24_in, U3, f47_in, U4, f87_in, U5, f25_in, f20_in, U6, U7, f36_in, U8, U9, f43_in, U10, U11, f76_in, U12, U13, f81_in, U14, U15, f83_in, U16, U17, f85_in, U18, U19, f17_in, U20

Defined Pair Symbols:

F36_IN, F43_IN, F2_IN, F20_IN, U10', F76_IN, U12', F81_IN, U14', F83_IN, U16', F85_IN, U18', F17_IN, F24_IN, F47_IN, F87_IN, U8', U6'

Compound Symbols:

c19, c22, c, c7, c10, c13, c20, c

(27) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F2_IN(tree(nil, z0, z1)) → c
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
U18'(f24_out1(z0), z1, z2, z3) → c
F17_IN(z0, z1) → c
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F17_IN(z0, z1) → c
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
U18'(f24_out1(z0), z1, z2, z3) → c
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U6'(f24_out1(z0), z1, z2) → c
U6'(f24_out1(z0), z1, z2) → c

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1([])
f2_in(tree(nil, z0, z1)) → U1(f17_in(z1, z0), tree(nil, z0, z1))
f2_in(tree(tree(z0, z1, z2), z3, z4)) → U2(f76_in(z0, z2, z1, z4, z3), tree(tree(z0, z1, z2), z3, z4))
U1(f17_out1(z0, z1), tree(nil, z2, z3)) → f2_out1(z1)
U1(f17_out2(z0, z1, z2), tree(nil, z3, z4)) → f2_out1(z2)
U2(f76_out1(z0, z1, z2, z3, z4), tree(tree(z5, z6, z7), z8, z9)) → f2_out1(z4)
f24_in(nil) → f24_out1([])
f24_in(tree(z0, z1, z2)) → U3(f36_in(z0, z2, z1), tree(z0, z1, z2))
U3(f36_out1(z0, z1, z2), tree(z3, z4, z5)) → f24_out1(z2)
f47_in([], z0, z1) → f47_out1(.(z0, z1))
f47_in(.(z0, z1), z2, z3) → U4(f47_in(z1, z2, z3), .(z0, z1), z2, z3)
U4(f47_out1(z0), .(z1, z2), z3, z4) → f47_out1(.(z1, z0))
f87_in([], z0, z1) → f87_out1(.(z0, z1))
f87_in(.(z0, z1), z2, z3) → U5(f87_in(z1, z2, z3), .(z0, z1), z2, z3)
U5(f87_out1(z0), .(z1, z2), z3, z4) → f87_out1(.(z1, z0))
f25_in(z0, z1) → f25_out1(.(z0, z1))
f20_in(z0, z1) → U6(f24_in(z0), z0, z1)
U6(f24_out1(z0), z1, z2) → U7(f25_in(z2, z0), z1, z2, z0)
U7(f25_out1(z0), z1, z2, z3) → f20_out1(z3, z0)
f36_in(z0, z1, z2) → U8(f24_in(z0), z0, z1, z2)
U8(f24_out1(z0), z1, z2, z3) → U9(f43_in(z2, z0, z3), z1, z2, z3, z0)
U9(f43_out1(z0, z1), z2, z3, z4, z5) → f36_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U10(f24_in(z0), z0, z1, z2)
U10(f24_out1(z0), z1, z2, z3) → U11(f47_in(z2, z3, z0), z1, z2, z3, z0)
U11(f47_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f76_in(z0, z1, z2, z3, z4) → U12(f24_in(z0), z0, z1, z2, z3, z4)
U12(f24_out1(z0), z1, z2, z3, z4, z5) → U13(f81_in(z2, z0, z3, z4, z5), z1, z2, z3, z4, z5, z0)
U13(f81_out1(z0, z1, z2, z3), z4, z5, z6, z7, z8, z9) → f76_out1(z9, z0, z1, z2, z3)
f81_in(z0, z1, z2, z3, z4) → U14(f24_in(z0), z0, z1, z2, z3, z4)
U14(f24_out1(z0), z1, z2, z3, z4, z5) → U15(f83_in(z2, z3, z0, z4, z5), z1, z2, z3, z4, z5, z0)
U15(f83_out1(z0, z1, z2), z3, z4, z5, z6, z7, z8) → f81_out1(z8, z0, z1, z2)
f83_in(z0, z1, z2, z3, z4) → U16(f47_in(z0, z1, z2), z0, z1, z2, z3, z4)
U16(f47_out1(z0), z1, z2, z3, z4, z5) → U17(f85_in(z4, z0, z5), z1, z2, z3, z4, z5, z0)
U17(f85_out1(z0, z1), z2, z3, z4, z5, z6, z7) → f83_out1(z7, z0, z1)
f85_in(z0, z1, z2) → U18(f24_in(z0), z0, z1, z2)
U18(f24_out1(z0), z1, z2, z3) → U19(f87_in(z2, z3, z0), z1, z2, z3, z0)
U19(f87_out1(z0), z1, z2, z3, z4) → f85_out1(z4, z0)
f17_in(z0, z1) → U20(f20_in(z0, z1), f21_in(z0, z1), z0, z1)
U20(f20_out1(z0, z1), z2, z3, z4) → f17_out1(z0, z1)
U20(z0, f21_out1(z1, z2, z3), z4, z5) → f17_out2(z1, z2, z3)

Tuples:

F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))
F47_IN(.(z0, z1), z2, z3) → c10(F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(F87_IN(z1, z2, z3))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))
F2_IN(tree(nil, z0, z1)) → c
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c
U6'(f24_out1(z0), z1, z2) → c
U10'(f24_out1(z0), z1, z2, z3) → c
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
U18'(f24_out1(z0), z1, z2, z3) → c
F17_IN(z0, z1) → c

S tuples:

F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))
F47_IN(.(z0, z1), z2, z3) → c10(F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(F87_IN(z1, z2, z3))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))
U10'(f24_out1(z0), z1, z2, z3) → c

K tuples:

F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F2_IN(tree(nil, z0, z1)) → c
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
U18'(f24_out1(z0), z1, z2, z3) → c
F17_IN(z0, z1) → c
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U6'(f24_out1(z0), z1, z2) → c

Defined Rule Symbols:

f2_in, U1, U2, f24_in, U3, f47_in, U4, f87_in, U5, f25_in, f20_in, U6, U7, f36_in, U8, U9, f43_in, U10, U11, f76_in, U12, U13, f81_in, U14, U15, f83_in, U16, U17, f85_in, U18, U19, f17_in, U20

Defined Pair Symbols:

F36_IN, F43_IN, F2_IN, F20_IN, U10', F76_IN, U12', F81_IN, U14', F83_IN, U16', F85_IN, U18', F17_IN, F24_IN, F47_IN, F87_IN, U8', U6'

Compound Symbols:

c19, c22, c, c7, c10, c13, c20, c

(29) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))

We considered the (Usable) Rules:

f24_in(nil) → f24_out1([])
f24_in(tree(z0, z1, z2)) → U3(f36_in(z0, z2, z1), tree(z0, z1, z2))
f36_in(z0, z1, z2) → U8(f24_in(z0), z0, z1, z2)
U3(f36_out1(z0, z1, z2), tree(z3, z4, z5)) → f24_out1(z2)
U8(f24_out1(z0), z1, z2, z3) → U9(f43_in(z2, z0, z3), z1, z2, z3, z0)
f43_in(z0, z1, z2) → U10(f24_in(z0), z0, z1, z2)
U9(f43_out1(z0, z1), z2, z3, z4, z5) → f36_out1(z5, z0, z1)
U10(f24_out1(z0), z1, z2, z3) → U11(f47_in(z2, z3, z0), z1, z2, z3, z0)
f47_in([], z0, z1) → f47_out1(.(z0, z1))
f47_in(.(z0, z1), z2, z3) → U4(f47_in(z1, z2, z3), .(z0, z1), z2, z3)
U11(f47_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
U4(f47_out1(z0), .(z1, z2), z3, z4) → f47_out1(.(z1, z0))

And the Tuples:

F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))
F47_IN(.(z0, z1), z2, z3) → c10(F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(F87_IN(z1, z2, z3))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))
F2_IN(tree(nil, z0, z1)) → c
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c
U6'(f24_out1(z0), z1, z2) → c
U10'(f24_out1(z0), z1, z2, z3) → c
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
U18'(f24_out1(z0), z1, z2, z3) → c
F17_IN(z0, z1) → c

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = 0   
POL(F17_IN(x₁, x₂)) = [3] + [2]x₁ + [3]x₂   
POL(F20_IN(x₁, x₂)) = [3] + x₁ + [2]x₂   
POL(F24_IN(x₁)) = x₁   
POL(F2_IN(x₁)) = [3]x₁   
POL(F36_IN(x₁, x₂, x₃)) = [1] + x₁ + x₂   
POL(F43_IN(x₁, x₂, x₃)) = [1] + x₁   
POL(F47_IN(x₁, x₂, x₃)) = 0   
POL(F76_IN(x₁, x₂, x₃, x₄, x₅)) = [2] + x₁ + [2]x₂ + [3]x₃ + [3]x₄ + [3]x₅   
POL(F81_IN(x₁, x₂, x₃, x₄, x₅)) = [1] + x₁ + [2]x₃ + [3]x₄ + [3]x₅   
POL(F83_IN(x₁, x₂, x₃, x₄, x₅)) = [1] + [2]x₂ + [2]x₄ + [2]x₅   
POL(F85_IN(x₁, x₂, x₃)) = [1] + x₁ + x₃   
POL(F87_IN(x₁, x₂, x₃)) = x₂   
POL(U10(x₁, x₂, x₃, x₄)) = 0   
POL(U10'(x₁, x₂, x₃, x₄)) = 0   
POL(U11(x₁, x₂, x₃, x₄, x₅)) = 0   
POL(U12'(x₁, x₂, x₃, x₄, x₅, x₆)) = [2] + x₂ + x₃ + [2]x₄ + [3]x₅ + [3]x₆   
POL(U14'(x₁, x₂, x₃, x₄, x₅, x₆)) = [1] + x₂ + [2]x₄ + [3]x₅ + [2]x₆   
POL(U16'(x₁, x₂, x₃, x₄, x₅, x₆)) = [1] + x₃ + [2]x₅ + x₆   
POL(U18'(x₁, x₂, x₃, x₄)) = x₄   
POL(U3(x₁, x₂)) = 0   
POL(U4(x₁, x₂, x₃, x₄)) = 0   
POL(U6'(x₁, x₂, x₃)) = x₂ + x₃   
POL(U8(x₁, x₂, x₃, x₄)) = 0   
POL(U8'(x₁, x₂, x₃, x₄)) = [1] + x₃   
POL(U9(x₁, x₂, x₃, x₄, x₅)) = 0   
POL([]) = 0   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c19(x₁, x₂)) = x₁ + x₂   
POL(c20(x₁)) = x₁   
POL(c22(x₁, x₂)) = x₁ + x₂   
POL(c7(x₁)) = x₁   
POL(f24_in(x₁)) = 0   
POL(f24_out1(x₁)) = 0   
POL(f36_in(x₁, x₂, x₃)) = 0   
POL(f36_out1(x₁, x₂, x₃)) = 0   
POL(f43_in(x₁, x₂, x₃)) = 0   
POL(f43_out1(x₁, x₂)) = 0   
POL(f47_in(x₁, x₂, x₃)) = 0   
POL(f47_out1(x₁)) = 0   
POL(nil) = 0   
POL(tree(x₁, x₂, x₃)) = [1] + x₁ + x₂ + x₃   

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1([])
f2_in(tree(nil, z0, z1)) → U1(f17_in(z1, z0), tree(nil, z0, z1))
f2_in(tree(tree(z0, z1, z2), z3, z4)) → U2(f76_in(z0, z2, z1, z4, z3), tree(tree(z0, z1, z2), z3, z4))
U1(f17_out1(z0, z1), tree(nil, z2, z3)) → f2_out1(z1)
U1(f17_out2(z0, z1, z2), tree(nil, z3, z4)) → f2_out1(z2)
U2(f76_out1(z0, z1, z2, z3, z4), tree(tree(z5, z6, z7), z8, z9)) → f2_out1(z4)
f24_in(nil) → f24_out1([])
f24_in(tree(z0, z1, z2)) → U3(f36_in(z0, z2, z1), tree(z0, z1, z2))
U3(f36_out1(z0, z1, z2), tree(z3, z4, z5)) → f24_out1(z2)
f47_in([], z0, z1) → f47_out1(.(z0, z1))
f47_in(.(z0, z1), z2, z3) → U4(f47_in(z1, z2, z3), .(z0, z1), z2, z3)
U4(f47_out1(z0), .(z1, z2), z3, z4) → f47_out1(.(z1, z0))
f87_in([], z0, z1) → f87_out1(.(z0, z1))
f87_in(.(z0, z1), z2, z3) → U5(f87_in(z1, z2, z3), .(z0, z1), z2, z3)
U5(f87_out1(z0), .(z1, z2), z3, z4) → f87_out1(.(z1, z0))
f25_in(z0, z1) → f25_out1(.(z0, z1))
f20_in(z0, z1) → U6(f24_in(z0), z0, z1)
U6(f24_out1(z0), z1, z2) → U7(f25_in(z2, z0), z1, z2, z0)
U7(f25_out1(z0), z1, z2, z3) → f20_out1(z3, z0)
f36_in(z0, z1, z2) → U8(f24_in(z0), z0, z1, z2)
U8(f24_out1(z0), z1, z2, z3) → U9(f43_in(z2, z0, z3), z1, z2, z3, z0)
U9(f43_out1(z0, z1), z2, z3, z4, z5) → f36_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U10(f24_in(z0), z0, z1, z2)
U10(f24_out1(z0), z1, z2, z3) → U11(f47_in(z2, z3, z0), z1, z2, z3, z0)
U11(f47_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f76_in(z0, z1, z2, z3, z4) → U12(f24_in(z0), z0, z1, z2, z3, z4)
U12(f24_out1(z0), z1, z2, z3, z4, z5) → U13(f81_in(z2, z0, z3, z4, z5), z1, z2, z3, z4, z5, z0)
U13(f81_out1(z0, z1, z2, z3), z4, z5, z6, z7, z8, z9) → f76_out1(z9, z0, z1, z2, z3)
f81_in(z0, z1, z2, z3, z4) → U14(f24_in(z0), z0, z1, z2, z3, z4)
U14(f24_out1(z0), z1, z2, z3, z4, z5) → U15(f83_in(z2, z3, z0, z4, z5), z1, z2, z3, z4, z5, z0)
U15(f83_out1(z0, z1, z2), z3, z4, z5, z6, z7, z8) → f81_out1(z8, z0, z1, z2)
f83_in(z0, z1, z2, z3, z4) → U16(f47_in(z0, z1, z2), z0, z1, z2, z3, z4)
U16(f47_out1(z0), z1, z2, z3, z4, z5) → U17(f85_in(z4, z0, z5), z1, z2, z3, z4, z5, z0)
U17(f85_out1(z0, z1), z2, z3, z4, z5, z6, z7) → f83_out1(z7, z0, z1)
f85_in(z0, z1, z2) → U18(f24_in(z0), z0, z1, z2)
U18(f24_out1(z0), z1, z2, z3) → U19(f87_in(z2, z3, z0), z1, z2, z3, z0)
U19(f87_out1(z0), z1, z2, z3, z4) → f85_out1(z4, z0)
f17_in(z0, z1) → U20(f20_in(z0, z1), f21_in(z0, z1), z0, z1)
U20(f20_out1(z0, z1), z2, z3, z4) → f17_out1(z0, z1)
U20(z0, f21_out1(z1, z2, z3), z4, z5) → f17_out2(z1, z2, z3)

Tuples:

F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))
F47_IN(.(z0, z1), z2, z3) → c10(F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(F87_IN(z1, z2, z3))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))
F2_IN(tree(nil, z0, z1)) → c
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c
U6'(f24_out1(z0), z1, z2) → c
U10'(f24_out1(z0), z1, z2, z3) → c
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
U18'(f24_out1(z0), z1, z2, z3) → c
F17_IN(z0, z1) → c

S tuples:

F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))
F47_IN(.(z0, z1), z2, z3) → c10(F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(F87_IN(z1, z2, z3))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))
U10'(f24_out1(z0), z1, z2, z3) → c

K tuples:

F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F2_IN(tree(nil, z0, z1)) → c
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
U18'(f24_out1(z0), z1, z2, z3) → c
F17_IN(z0, z1) → c
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U6'(f24_out1(z0), z1, z2) → c
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))

Defined Rule Symbols:

f2_in, U1, U2, f24_in, U3, f47_in, U4, f87_in, U5, f25_in, f20_in, U6, U7, f36_in, U8, U9, f43_in, U10, U11, f76_in, U12, U13, f81_in, U14, U15, f83_in, U16, U17, f85_in, U18, U19, f17_in, U20

Defined Pair Symbols:

F36_IN, F43_IN, F2_IN, F20_IN, U10', F76_IN, U12', F81_IN, U14', F83_IN, U16', F85_IN, U18', F17_IN, F24_IN, F47_IN, F87_IN, U8', U6'

Compound Symbols:

c19, c22, c, c7, c10, c13, c20, c

(31) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
U10'(f24_out1(z0), z1, z2, z3) → c

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1([])
f2_in(tree(nil, z0, z1)) → U1(f17_in(z1, z0), tree(nil, z0, z1))
f2_in(tree(tree(z0, z1, z2), z3, z4)) → U2(f76_in(z0, z2, z1, z4, z3), tree(tree(z0, z1, z2), z3, z4))
U1(f17_out1(z0, z1), tree(nil, z2, z3)) → f2_out1(z1)
U1(f17_out2(z0, z1, z2), tree(nil, z3, z4)) → f2_out1(z2)
U2(f76_out1(z0, z1, z2, z3, z4), tree(tree(z5, z6, z7), z8, z9)) → f2_out1(z4)
f24_in(nil) → f24_out1([])
f24_in(tree(z0, z1, z2)) → U3(f36_in(z0, z2, z1), tree(z0, z1, z2))
U3(f36_out1(z0, z1, z2), tree(z3, z4, z5)) → f24_out1(z2)
f47_in([], z0, z1) → f47_out1(.(z0, z1))
f47_in(.(z0, z1), z2, z3) → U4(f47_in(z1, z2, z3), .(z0, z1), z2, z3)
U4(f47_out1(z0), .(z1, z2), z3, z4) → f47_out1(.(z1, z0))
f87_in([], z0, z1) → f87_out1(.(z0, z1))
f87_in(.(z0, z1), z2, z3) → U5(f87_in(z1, z2, z3), .(z0, z1), z2, z3)
U5(f87_out1(z0), .(z1, z2), z3, z4) → f87_out1(.(z1, z0))
f25_in(z0, z1) → f25_out1(.(z0, z1))
f20_in(z0, z1) → U6(f24_in(z0), z0, z1)
U6(f24_out1(z0), z1, z2) → U7(f25_in(z2, z0), z1, z2, z0)
U7(f25_out1(z0), z1, z2, z3) → f20_out1(z3, z0)
f36_in(z0, z1, z2) → U8(f24_in(z0), z0, z1, z2)
U8(f24_out1(z0), z1, z2, z3) → U9(f43_in(z2, z0, z3), z1, z2, z3, z0)
U9(f43_out1(z0, z1), z2, z3, z4, z5) → f36_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U10(f24_in(z0), z0, z1, z2)
U10(f24_out1(z0), z1, z2, z3) → U11(f47_in(z2, z3, z0), z1, z2, z3, z0)
U11(f47_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f76_in(z0, z1, z2, z3, z4) → U12(f24_in(z0), z0, z1, z2, z3, z4)
U12(f24_out1(z0), z1, z2, z3, z4, z5) → U13(f81_in(z2, z0, z3, z4, z5), z1, z2, z3, z4, z5, z0)
U13(f81_out1(z0, z1, z2, z3), z4, z5, z6, z7, z8, z9) → f76_out1(z9, z0, z1, z2, z3)
f81_in(z0, z1, z2, z3, z4) → U14(f24_in(z0), z0, z1, z2, z3, z4)
U14(f24_out1(z0), z1, z2, z3, z4, z5) → U15(f83_in(z2, z3, z0, z4, z5), z1, z2, z3, z4, z5, z0)
U15(f83_out1(z0, z1, z2), z3, z4, z5, z6, z7, z8) → f81_out1(z8, z0, z1, z2)
f83_in(z0, z1, z2, z3, z4) → U16(f47_in(z0, z1, z2), z0, z1, z2, z3, z4)
U16(f47_out1(z0), z1, z2, z3, z4, z5) → U17(f85_in(z4, z0, z5), z1, z2, z3, z4, z5, z0)
U17(f85_out1(z0, z1), z2, z3, z4, z5, z6, z7) → f83_out1(z7, z0, z1)
f85_in(z0, z1, z2) → U18(f24_in(z0), z0, z1, z2)
U18(f24_out1(z0), z1, z2, z3) → U19(f87_in(z2, z3, z0), z1, z2, z3, z0)
U19(f87_out1(z0), z1, z2, z3, z4) → f85_out1(z4, z0)
f17_in(z0, z1) → U20(f20_in(z0, z1), f21_in(z0, z1), z0, z1)
U20(f20_out1(z0, z1), z2, z3, z4) → f17_out1(z0, z1)
U20(z0, f21_out1(z1, z2, z3), z4, z5) → f17_out2(z1, z2, z3)

Tuples:

F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))
F47_IN(.(z0, z1), z2, z3) → c10(F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(F87_IN(z1, z2, z3))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))
F2_IN(tree(nil, z0, z1)) → c
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c
U6'(f24_out1(z0), z1, z2) → c
U10'(f24_out1(z0), z1, z2, z3) → c
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
U18'(f24_out1(z0), z1, z2, z3) → c
F17_IN(z0, z1) → c

S tuples:

F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))
F47_IN(.(z0, z1), z2, z3) → c10(F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(F87_IN(z1, z2, z3))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))

K tuples:

F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F2_IN(tree(nil, z0, z1)) → c
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
U18'(f24_out1(z0), z1, z2, z3) → c
F17_IN(z0, z1) → c
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U6'(f24_out1(z0), z1, z2) → c
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
U10'(f24_out1(z0), z1, z2, z3) → c

Defined Rule Symbols:

f2_in, U1, U2, f24_in, U3, f47_in, U4, f87_in, U5, f25_in, f20_in, U6, U7, f36_in, U8, U9, f43_in, U10, U11, f76_in, U12, U13, f81_in, U14, U15, f83_in, U16, U17, f85_in, U18, U19, f17_in, U20

Defined Pair Symbols:

F36_IN, F43_IN, F2_IN, F20_IN, U10', F76_IN, U12', F81_IN, U14', F83_IN, U16', F85_IN, U18', F17_IN, F24_IN, F47_IN, F87_IN, U8', U6'

Compound Symbols:

c19, c22, c, c7, c10, c13, c20, c

(33) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))

We considered the (Usable) Rules:

f24_in(nil) → f24_out1([])
f24_in(tree(z0, z1, z2)) → U3(f36_in(z0, z2, z1), tree(z0, z1, z2))
f36_in(z0, z1, z2) → U8(f24_in(z0), z0, z1, z2)
U3(f36_out1(z0, z1, z2), tree(z3, z4, z5)) → f24_out1(z2)
U8(f24_out1(z0), z1, z2, z3) → U9(f43_in(z2, z0, z3), z1, z2, z3, z0)
f43_in(z0, z1, z2) → U10(f24_in(z0), z0, z1, z2)
U9(f43_out1(z0, z1), z2, z3, z4, z5) → f36_out1(z5, z0, z1)
U10(f24_out1(z0), z1, z2, z3) → U11(f47_in(z2, z3, z0), z1, z2, z3, z0)
f47_in([], z0, z1) → f47_out1(.(z0, z1))
f47_in(.(z0, z1), z2, z3) → U4(f47_in(z1, z2, z3), .(z0, z1), z2, z3)
U11(f47_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
U4(f47_out1(z0), .(z1, z2), z3, z4) → f47_out1(.(z1, z0))

And the Tuples:

F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))
F47_IN(.(z0, z1), z2, z3) → c10(F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(F87_IN(z1, z2, z3))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))
F2_IN(tree(nil, z0, z1)) → c
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c
U6'(f24_out1(z0), z1, z2) → c
U10'(f24_out1(z0), z1, z2, z3) → c
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
U18'(f24_out1(z0), z1, z2, z3) → c
F17_IN(z0, z1) → c

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = 0   
POL(F17_IN(x₁, x₂)) = [2] + [3]x₁ + [2]x₂   
POL(F20_IN(x₁, x₂)) = [2] + x₁ + x₂   
POL(F24_IN(x₁)) = x₁   
POL(F2_IN(x₁)) = [3]x₁   
POL(F36_IN(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(F43_IN(x₁, x₂, x₃)) = x₁ + x₃   
POL(F47_IN(x₁, x₂, x₃)) = 0   
POL(F76_IN(x₁, x₂, x₃, x₄, x₅)) = [2] + [2]x₁ + [3]x₂ + [2]x₃ + [3]x₄ + [3]x₅   
POL(F81_IN(x₁, x₂, x₃, x₄, x₅)) = [2] + x₁ + [3]x₄ + [2]x₅   
POL(F83_IN(x₁, x₂, x₃, x₄, x₅)) = [1] + [3]x₄   
POL(F85_IN(x₁, x₂, x₃)) = [2]x₁   
POL(F87_IN(x₁, x₂, x₃)) = 0   
POL(U10(x₁, x₂, x₃, x₄)) = 0   
POL(U10'(x₁, x₂, x₃, x₄)) = x₄   
POL(U11(x₁, x₂, x₃, x₄, x₅)) = 0   
POL(U12'(x₁, x₂, x₃, x₄, x₅, x₆)) = [2] + x₁ + x₂ + x₃ + [3]x₅ + [3]x₆   
POL(U14'(x₁, x₂, x₃, x₄, x₅, x₆)) = [2] + x₂ + [3]x₅   
POL(U16'(x₁, x₂, x₃, x₄, x₅, x₆)) = [2]x₅   
POL(U18'(x₁, x₂, x₃, x₄)) = [2]x₁   
POL(U3(x₁, x₂)) = 0   
POL(U4(x₁, x₂, x₃, x₄)) = 0   
POL(U6'(x₁, x₂, x₃)) = [2] + x₂ + x₃   
POL(U8(x₁, x₂, x₃, x₄)) = 0   
POL(U8'(x₁, x₂, x₃, x₄)) = x₃ + x₄   
POL(U9(x₁, x₂, x₃, x₄, x₅)) = 0   
POL([]) = 0   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c19(x₁, x₂)) = x₁ + x₂   
POL(c20(x₁)) = x₁   
POL(c22(x₁, x₂)) = x₁ + x₂   
POL(c7(x₁)) = x₁   
POL(f24_in(x₁)) = x₁   
POL(f24_out1(x₁)) = 0   
POL(f36_in(x₁, x₂, x₃)) = 0   
POL(f36_out1(x₁, x₂, x₃)) = 0   
POL(f43_in(x₁, x₂, x₃)) = 0   
POL(f43_out1(x₁, x₂)) = 0   
POL(f47_in(x₁, x₂, x₃)) = 0   
POL(f47_out1(x₁)) = 0   
POL(nil) = 0   
POL(tree(x₁, x₂, x₃)) = [1] + x₁ + x₂ + x₃   

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1([])
f2_in(tree(nil, z0, z1)) → U1(f17_in(z1, z0), tree(nil, z0, z1))
f2_in(tree(tree(z0, z1, z2), z3, z4)) → U2(f76_in(z0, z2, z1, z4, z3), tree(tree(z0, z1, z2), z3, z4))
U1(f17_out1(z0, z1), tree(nil, z2, z3)) → f2_out1(z1)
U1(f17_out2(z0, z1, z2), tree(nil, z3, z4)) → f2_out1(z2)
U2(f76_out1(z0, z1, z2, z3, z4), tree(tree(z5, z6, z7), z8, z9)) → f2_out1(z4)
f24_in(nil) → f24_out1([])
f24_in(tree(z0, z1, z2)) → U3(f36_in(z0, z2, z1), tree(z0, z1, z2))
U3(f36_out1(z0, z1, z2), tree(z3, z4, z5)) → f24_out1(z2)
f47_in([], z0, z1) → f47_out1(.(z0, z1))
f47_in(.(z0, z1), z2, z3) → U4(f47_in(z1, z2, z3), .(z0, z1), z2, z3)
U4(f47_out1(z0), .(z1, z2), z3, z4) → f47_out1(.(z1, z0))
f87_in([], z0, z1) → f87_out1(.(z0, z1))
f87_in(.(z0, z1), z2, z3) → U5(f87_in(z1, z2, z3), .(z0, z1), z2, z3)
U5(f87_out1(z0), .(z1, z2), z3, z4) → f87_out1(.(z1, z0))
f25_in(z0, z1) → f25_out1(.(z0, z1))
f20_in(z0, z1) → U6(f24_in(z0), z0, z1)
U6(f24_out1(z0), z1, z2) → U7(f25_in(z2, z0), z1, z2, z0)
U7(f25_out1(z0), z1, z2, z3) → f20_out1(z3, z0)
f36_in(z0, z1, z2) → U8(f24_in(z0), z0, z1, z2)
U8(f24_out1(z0), z1, z2, z3) → U9(f43_in(z2, z0, z3), z1, z2, z3, z0)
U9(f43_out1(z0, z1), z2, z3, z4, z5) → f36_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U10(f24_in(z0), z0, z1, z2)
U10(f24_out1(z0), z1, z2, z3) → U11(f47_in(z2, z3, z0), z1, z2, z3, z0)
U11(f47_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f76_in(z0, z1, z2, z3, z4) → U12(f24_in(z0), z0, z1, z2, z3, z4)
U12(f24_out1(z0), z1, z2, z3, z4, z5) → U13(f81_in(z2, z0, z3, z4, z5), z1, z2, z3, z4, z5, z0)
U13(f81_out1(z0, z1, z2, z3), z4, z5, z6, z7, z8, z9) → f76_out1(z9, z0, z1, z2, z3)
f81_in(z0, z1, z2, z3, z4) → U14(f24_in(z0), z0, z1, z2, z3, z4)
U14(f24_out1(z0), z1, z2, z3, z4, z5) → U15(f83_in(z2, z3, z0, z4, z5), z1, z2, z3, z4, z5, z0)
U15(f83_out1(z0, z1, z2), z3, z4, z5, z6, z7, z8) → f81_out1(z8, z0, z1, z2)
f83_in(z0, z1, z2, z3, z4) → U16(f47_in(z0, z1, z2), z0, z1, z2, z3, z4)
U16(f47_out1(z0), z1, z2, z3, z4, z5) → U17(f85_in(z4, z0, z5), z1, z2, z3, z4, z5, z0)
U17(f85_out1(z0, z1), z2, z3, z4, z5, z6, z7) → f83_out1(z7, z0, z1)
f85_in(z0, z1, z2) → U18(f24_in(z0), z0, z1, z2)
U18(f24_out1(z0), z1, z2, z3) → U19(f87_in(z2, z3, z0), z1, z2, z3, z0)
U19(f87_out1(z0), z1, z2, z3, z4) → f85_out1(z4, z0)
f17_in(z0, z1) → U20(f20_in(z0, z1), f21_in(z0, z1), z0, z1)
U20(f20_out1(z0, z1), z2, z3, z4) → f17_out1(z0, z1)
U20(z0, f21_out1(z1, z2, z3), z4, z5) → f17_out2(z1, z2, z3)

Tuples:

F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))
F47_IN(.(z0, z1), z2, z3) → c10(F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(F87_IN(z1, z2, z3))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))
F2_IN(tree(nil, z0, z1)) → c
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c
U6'(f24_out1(z0), z1, z2) → c
U10'(f24_out1(z0), z1, z2, z3) → c
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
U18'(f24_out1(z0), z1, z2, z3) → c
F17_IN(z0, z1) → c

S tuples:

F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F47_IN(.(z0, z1), z2, z3) → c10(F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(F87_IN(z1, z2, z3))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))

K tuples:

F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F2_IN(tree(nil, z0, z1)) → c
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
U18'(f24_out1(z0), z1, z2, z3) → c
F17_IN(z0, z1) → c
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U6'(f24_out1(z0), z1, z2) → c
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
U10'(f24_out1(z0), z1, z2, z3) → c
F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))

Defined Rule Symbols:

f2_in, U1, U2, f24_in, U3, f47_in, U4, f87_in, U5, f25_in, f20_in, U6, U7, f36_in, U8, U9, f43_in, U10, U11, f76_in, U12, U13, f81_in, U14, U15, f83_in, U16, U17, f85_in, U18, U19, f17_in, U20

Defined Pair Symbols:

F36_IN, F43_IN, F2_IN, F20_IN, U10', F76_IN, U12', F81_IN, U14', F83_IN, U16', F85_IN, U18', F17_IN, F24_IN, F47_IN, F87_IN, U8', U6'

Compound Symbols:

c19, c22, c, c7, c10, c13, c20, c

(35) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))
F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1([])
f2_in(tree(nil, z0, z1)) → U1(f17_in(z1, z0), tree(nil, z0, z1))
f2_in(tree(tree(z0, z1, z2), z3, z4)) → U2(f76_in(z0, z2, z1, z4, z3), tree(tree(z0, z1, z2), z3, z4))
U1(f17_out1(z0, z1), tree(nil, z2, z3)) → f2_out1(z1)
U1(f17_out2(z0, z1, z2), tree(nil, z3, z4)) → f2_out1(z2)
U2(f76_out1(z0, z1, z2, z3, z4), tree(tree(z5, z6, z7), z8, z9)) → f2_out1(z4)
f24_in(nil) → f24_out1([])
f24_in(tree(z0, z1, z2)) → U3(f36_in(z0, z2, z1), tree(z0, z1, z2))
U3(f36_out1(z0, z1, z2), tree(z3, z4, z5)) → f24_out1(z2)
f47_in([], z0, z1) → f47_out1(.(z0, z1))
f47_in(.(z0, z1), z2, z3) → U4(f47_in(z1, z2, z3), .(z0, z1), z2, z3)
U4(f47_out1(z0), .(z1, z2), z3, z4) → f47_out1(.(z1, z0))
f87_in([], z0, z1) → f87_out1(.(z0, z1))
f87_in(.(z0, z1), z2, z3) → U5(f87_in(z1, z2, z3), .(z0, z1), z2, z3)
U5(f87_out1(z0), .(z1, z2), z3, z4) → f87_out1(.(z1, z0))
f25_in(z0, z1) → f25_out1(.(z0, z1))
f20_in(z0, z1) → U6(f24_in(z0), z0, z1)
U6(f24_out1(z0), z1, z2) → U7(f25_in(z2, z0), z1, z2, z0)
U7(f25_out1(z0), z1, z2, z3) → f20_out1(z3, z0)
f36_in(z0, z1, z2) → U8(f24_in(z0), z0, z1, z2)
U8(f24_out1(z0), z1, z2, z3) → U9(f43_in(z2, z0, z3), z1, z2, z3, z0)
U9(f43_out1(z0, z1), z2, z3, z4, z5) → f36_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U10(f24_in(z0), z0, z1, z2)
U10(f24_out1(z0), z1, z2, z3) → U11(f47_in(z2, z3, z0), z1, z2, z3, z0)
U11(f47_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f76_in(z0, z1, z2, z3, z4) → U12(f24_in(z0), z0, z1, z2, z3, z4)
U12(f24_out1(z0), z1, z2, z3, z4, z5) → U13(f81_in(z2, z0, z3, z4, z5), z1, z2, z3, z4, z5, z0)
U13(f81_out1(z0, z1, z2, z3), z4, z5, z6, z7, z8, z9) → f76_out1(z9, z0, z1, z2, z3)
f81_in(z0, z1, z2, z3, z4) → U14(f24_in(z0), z0, z1, z2, z3, z4)
U14(f24_out1(z0), z1, z2, z3, z4, z5) → U15(f83_in(z2, z3, z0, z4, z5), z1, z2, z3, z4, z5, z0)
U15(f83_out1(z0, z1, z2), z3, z4, z5, z6, z7, z8) → f81_out1(z8, z0, z1, z2)
f83_in(z0, z1, z2, z3, z4) → U16(f47_in(z0, z1, z2), z0, z1, z2, z3, z4)
U16(f47_out1(z0), z1, z2, z3, z4, z5) → U17(f85_in(z4, z0, z5), z1, z2, z3, z4, z5, z0)
U17(f85_out1(z0, z1), z2, z3, z4, z5, z6, z7) → f83_out1(z7, z0, z1)
f85_in(z0, z1, z2) → U18(f24_in(z0), z0, z1, z2)
U18(f24_out1(z0), z1, z2, z3) → U19(f87_in(z2, z3, z0), z1, z2, z3, z0)
U19(f87_out1(z0), z1, z2, z3, z4) → f85_out1(z4, z0)
f17_in(z0, z1) → U20(f20_in(z0, z1), f21_in(z0, z1), z0, z1)
U20(f20_out1(z0, z1), z2, z3, z4) → f17_out1(z0, z1)
U20(z0, f21_out1(z1, z2, z3), z4, z5) → f17_out2(z1, z2, z3)

Tuples:

F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))
F47_IN(.(z0, z1), z2, z3) → c10(F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(F87_IN(z1, z2, z3))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))
F2_IN(tree(nil, z0, z1)) → c
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c
U6'(f24_out1(z0), z1, z2) → c
U10'(f24_out1(z0), z1, z2, z3) → c
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
U18'(f24_out1(z0), z1, z2, z3) → c
F17_IN(z0, z1) → c

S tuples:

F47_IN(.(z0, z1), z2, z3) → c10(F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(F87_IN(z1, z2, z3))

K tuples:

F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F2_IN(tree(nil, z0, z1)) → c
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
U18'(f24_out1(z0), z1, z2, z3) → c
F17_IN(z0, z1) → c
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U6'(f24_out1(z0), z1, z2) → c
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
U10'(f24_out1(z0), z1, z2, z3) → c
F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))
F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))

Defined Rule Symbols:

f2_in, U1, U2, f24_in, U3, f47_in, U4, f87_in, U5, f25_in, f20_in, U6, U7, f36_in, U8, U9, f43_in, U10, U11, f76_in, U12, U13, f81_in, U14, U15, f83_in, U16, U17, f85_in, U18, U19, f17_in, U20

Defined Pair Symbols:

F36_IN, F43_IN, F2_IN, F20_IN, U10', F76_IN, U12', F81_IN, U14', F83_IN, U16', F85_IN, U18', F17_IN, F24_IN, F47_IN, F87_IN, U8', U6'

Compound Symbols:

c19, c22, c, c7, c10, c13, c20, c

(37) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F87_IN(.(z0, z1), z2, z3) → c13(F87_IN(z1, z2, z3))

We considered the (Usable) Rules:

f24_in(nil) → f24_out1([])
f24_in(tree(z0, z1, z2)) → U3(f36_in(z0, z2, z1), tree(z0, z1, z2))
f36_in(z0, z1, z2) → U8(f24_in(z0), z0, z1, z2)
U3(f36_out1(z0, z1, z2), tree(z3, z4, z5)) → f24_out1(z2)
U8(f24_out1(z0), z1, z2, z3) → U9(f43_in(z2, z0, z3), z1, z2, z3, z0)
f43_in(z0, z1, z2) → U10(f24_in(z0), z0, z1, z2)
U9(f43_out1(z0, z1), z2, z3, z4, z5) → f36_out1(z5, z0, z1)
U10(f24_out1(z0), z1, z2, z3) → U11(f47_in(z2, z3, z0), z1, z2, z3, z0)
f47_in([], z0, z1) → f47_out1(.(z0, z1))
f47_in(.(z0, z1), z2, z3) → U4(f47_in(z1, z2, z3), .(z0, z1), z2, z3)
U11(f47_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
U4(f47_out1(z0), .(z1, z2), z3, z4) → f47_out1(.(z1, z0))

And the Tuples:

F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))
F47_IN(.(z0, z1), z2, z3) → c10(F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(F87_IN(z1, z2, z3))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))
F2_IN(tree(nil, z0, z1)) → c
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c
U6'(f24_out1(z0), z1, z2) → c
U10'(f24_out1(z0), z1, z2, z3) → c
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
U18'(f24_out1(z0), z1, z2, z3) → c
F17_IN(z0, z1) → c

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = [1] + x₂   
POL(F17_IN(x₁, x₂)) = [3] + [2]x₁ + [2]x₂   
POL(F20_IN(x₁, x₂)) = [3] + x₂   
POL(F24_IN(x₁)) = 0   
POL(F2_IN(x₁)) = [2]x₁   
POL(F36_IN(x₁, x₂, x₃)) = 0   
POL(F43_IN(x₁, x₂, x₃)) = 0   
POL(F47_IN(x₁, x₂, x₃)) = 0   
POL(F76_IN(x₁, x₂, x₃, x₄, x₅)) = [2] + [2]x₁ + [2]x₂ + [2]x₃ + [2]x₄ + x₅   
POL(F81_IN(x₁, x₂, x₃, x₄, x₅)) = [1] + [2]x₁ + x₂ + x₃ + x₅   
POL(F83_IN(x₁, x₂, x₃, x₄, x₅)) = [1] + x₁ + x₂ + x₃ + x₅   
POL(F85_IN(x₁, x₂, x₃)) = x₂   
POL(F87_IN(x₁, x₂, x₃)) = x₁   
POL(U10(x₁, x₂, x₃, x₄)) = [1] + x₁ + x₃   
POL(U10'(x₁, x₂, x₃, x₄)) = 0   
POL(U11(x₁, x₂, x₃, x₄, x₅)) = x₁   
POL(U12'(x₁, x₂, x₃, x₄, x₅, x₆)) = [2] + x₁ + [2]x₃ + [2]x₄ + x₅ + x₆   
POL(U14'(x₁, x₂, x₃, x₄, x₅, x₆)) = [1] + x₁ + x₃ + x₄ + x₆   
POL(U16'(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁   
POL(U18'(x₁, x₂, x₃, x₄)) = x₃   
POL(U3(x₁, x₂)) = x₁   
POL(U4(x₁, x₂, x₃, x₄)) = [1] + x₁   
POL(U6'(x₁, x₂, x₃)) = x₃   
POL(U8(x₁, x₂, x₃, x₄)) = [1] + x₁ + [2]x₃ + x₄   
POL(U8'(x₁, x₂, x₃, x₄)) = 0   
POL(U9(x₁, x₂, x₃, x₄, x₅)) = x₁   
POL([]) = 0   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c19(x₁, x₂)) = x₁ + x₂   
POL(c20(x₁)) = x₁   
POL(c22(x₁, x₂)) = x₁ + x₂   
POL(c7(x₁)) = x₁   
POL(f24_in(x₁)) = [2]x₁   
POL(f24_out1(x₁)) = x₁   
POL(f36_in(x₁, x₂, x₃)) = [1] + [2]x₁ + [2]x₂ + x₃   
POL(f36_out1(x₁, x₂, x₃)) = x₃   
POL(f43_in(x₁, x₂, x₃)) = [1] + [2]x₁ + x₂   
POL(f43_out1(x₁, x₂)) = x₂   
POL(f47_in(x₁, x₂, x₃)) = [1] + x₁ + x₃   
POL(f47_out1(x₁)) = x₁   
POL(nil) = 0   
POL(tree(x₁, x₂, x₃)) = [2] + x₁ + x₂ + x₃   

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1([])
f2_in(tree(nil, z0, z1)) → U1(f17_in(z1, z0), tree(nil, z0, z1))
f2_in(tree(tree(z0, z1, z2), z3, z4)) → U2(f76_in(z0, z2, z1, z4, z3), tree(tree(z0, z1, z2), z3, z4))
U1(f17_out1(z0, z1), tree(nil, z2, z3)) → f2_out1(z1)
U1(f17_out2(z0, z1, z2), tree(nil, z3, z4)) → f2_out1(z2)
U2(f76_out1(z0, z1, z2, z3, z4), tree(tree(z5, z6, z7), z8, z9)) → f2_out1(z4)
f24_in(nil) → f24_out1([])
f24_in(tree(z0, z1, z2)) → U3(f36_in(z0, z2, z1), tree(z0, z1, z2))
U3(f36_out1(z0, z1, z2), tree(z3, z4, z5)) → f24_out1(z2)
f47_in([], z0, z1) → f47_out1(.(z0, z1))
f47_in(.(z0, z1), z2, z3) → U4(f47_in(z1, z2, z3), .(z0, z1), z2, z3)
U4(f47_out1(z0), .(z1, z2), z3, z4) → f47_out1(.(z1, z0))
f87_in([], z0, z1) → f87_out1(.(z0, z1))
f87_in(.(z0, z1), z2, z3) → U5(f87_in(z1, z2, z3), .(z0, z1), z2, z3)
U5(f87_out1(z0), .(z1, z2), z3, z4) → f87_out1(.(z1, z0))
f25_in(z0, z1) → f25_out1(.(z0, z1))
f20_in(z0, z1) → U6(f24_in(z0), z0, z1)
U6(f24_out1(z0), z1, z2) → U7(f25_in(z2, z0), z1, z2, z0)
U7(f25_out1(z0), z1, z2, z3) → f20_out1(z3, z0)
f36_in(z0, z1, z2) → U8(f24_in(z0), z0, z1, z2)
U8(f24_out1(z0), z1, z2, z3) → U9(f43_in(z2, z0, z3), z1, z2, z3, z0)
U9(f43_out1(z0, z1), z2, z3, z4, z5) → f36_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U10(f24_in(z0), z0, z1, z2)
U10(f24_out1(z0), z1, z2, z3) → U11(f47_in(z2, z3, z0), z1, z2, z3, z0)
U11(f47_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f76_in(z0, z1, z2, z3, z4) → U12(f24_in(z0), z0, z1, z2, z3, z4)
U12(f24_out1(z0), z1, z2, z3, z4, z5) → U13(f81_in(z2, z0, z3, z4, z5), z1, z2, z3, z4, z5, z0)
U13(f81_out1(z0, z1, z2, z3), z4, z5, z6, z7, z8, z9) → f76_out1(z9, z0, z1, z2, z3)
f81_in(z0, z1, z2, z3, z4) → U14(f24_in(z0), z0, z1, z2, z3, z4)
U14(f24_out1(z0), z1, z2, z3, z4, z5) → U15(f83_in(z2, z3, z0, z4, z5), z1, z2, z3, z4, z5, z0)
U15(f83_out1(z0, z1, z2), z3, z4, z5, z6, z7, z8) → f81_out1(z8, z0, z1, z2)
f83_in(z0, z1, z2, z3, z4) → U16(f47_in(z0, z1, z2), z0, z1, z2, z3, z4)
U16(f47_out1(z0), z1, z2, z3, z4, z5) → U17(f85_in(z4, z0, z5), z1, z2, z3, z4, z5, z0)
U17(f85_out1(z0, z1), z2, z3, z4, z5, z6, z7) → f83_out1(z7, z0, z1)
f85_in(z0, z1, z2) → U18(f24_in(z0), z0, z1, z2)
U18(f24_out1(z0), z1, z2, z3) → U19(f87_in(z2, z3, z0), z1, z2, z3, z0)
U19(f87_out1(z0), z1, z2, z3, z4) → f85_out1(z4, z0)
f17_in(z0, z1) → U20(f20_in(z0, z1), f21_in(z0, z1), z0, z1)
U20(f20_out1(z0, z1), z2, z3, z4) → f17_out1(z0, z1)
U20(z0, f21_out1(z1, z2, z3), z4, z5) → f17_out2(z1, z2, z3)

Tuples:

F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))
F47_IN(.(z0, z1), z2, z3) → c10(F47_IN(z1, z2, z3))
F87_IN(.(z0, z1), z2, z3) → c13(F87_IN(z1, z2, z3))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))
F2_IN(tree(nil, z0, z1)) → c
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c
U6'(f24_out1(z0), z1, z2) → c
U10'(f24_out1(z0), z1, z2, z3) → c
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
U18'(f24_out1(z0), z1, z2, z3) → c
F17_IN(z0, z1) → c

S tuples:

F47_IN(.(z0, z1), z2, z3) → c10(F47_IN(z1, z2, z3))

K tuples:

F2_IN(tree(nil, z0, z1)) → c(F17_IN(z1, z0))
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c(F76_IN(z0, z2, z1, z4, z3))
F76_IN(z0, z1, z2, z3, z4) → c(U12'(f24_in(z0), z0, z1, z2, z3, z4))
F76_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F81_IN(z2, z0, z3, z4, z5))
F81_IN(z0, z1, z2, z3, z4) → c(U14'(f24_in(z0), z0, z1, z2, z3, z4))
F81_IN(z0, z1, z2, z3, z4) → c(F24_IN(z0))
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c(F83_IN(z2, z3, z0, z4, z5))
F83_IN(z0, z1, z2, z3, z4) → c(U16'(f47_in(z0, z1, z2), z0, z1, z2, z3, z4))
F83_IN(z0, z1, z2, z3, z4) → c(F47_IN(z0, z1, z2))
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c(F85_IN(z4, z0, z5))
F85_IN(z0, z1, z2) → c(U18'(f24_in(z0), z0, z1, z2))
F85_IN(z0, z1, z2) → c(F24_IN(z0))
U18'(f24_out1(z0), z1, z2, z3) → c(F87_IN(z2, z3, z0))
F17_IN(z0, z1) → c(F20_IN(z0, z1))
F2_IN(tree(nil, z0, z1)) → c
F2_IN(tree(tree(z0, z1, z2), z3, z4)) → c
U12'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U14'(f24_out1(z0), z1, z2, z3, z4, z5) → c
U16'(f47_out1(z0), z1, z2, z3, z4, z5) → c
U18'(f24_out1(z0), z1, z2, z3) → c
F17_IN(z0, z1) → c
F20_IN(z0, z1) → c(U6'(f24_in(z0), z0, z1))
F20_IN(z0, z1) → c(F24_IN(z0))
U6'(f24_out1(z0), z1, z2) → c
F43_IN(z0, z1, z2) → c22(U10'(f24_in(z0), z0, z1, z2), F24_IN(z0))
U10'(f24_out1(z0), z1, z2, z3) → c(F47_IN(z2, z3, z0))
U10'(f24_out1(z0), z1, z2, z3) → c
F24_IN(tree(z0, z1, z2)) → c7(F36_IN(z0, z2, z1))
F36_IN(z0, z1, z2) → c19(U8'(f24_in(z0), z0, z1, z2), F24_IN(z0))
U8'(f24_out1(z0), z1, z2, z3) → c20(F43_IN(z2, z0, z3))
F87_IN(.(z0, z1), z2, z3) → c13(F87_IN(z1, z2, z3))

Defined Rule Symbols:

f2_in, U1, U2, f24_in, U3, f47_in, U4, f87_in, U5, f25_in, f20_in, U6, U7, f36_in, U8, U9, f43_in, U10, U11, f76_in, U12, U13, f81_in, U14, U15, f83_in, U16, U17, f85_in, U18, U19, f17_in, U20

Defined Pair Symbols:

F36_IN, F43_IN, F2_IN, F20_IN, U10', F76_IN, U12', F81_IN, U14', F83_IN, U16', F85_IN, U18', F17_IN, F24_IN, F47_IN, F87_IN, U8', U6'

Compound Symbols:

c19, c22, c, c7, c10, c13, c20, c