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

(0) Obligation:

Clauses:

init_vars(E1, E2, E1init, E2init) :- ','(find_all_vars(E1, Vars1), ','(find_all_vars(E2, Vars2), ','(intersect(Vars1, Vars2, _X, Notin1, Notin2), ','(init_vars2(Notin1, E1, E1init), init_vars2(Notin2, E2, E2init))))).
find_all_vars(E, Vars) :- ','(find_all_vars2(E, Vars0), sort(Vars0, Vars)).
find_all_vars2([], []).
find_all_vars2(.(=(Vars, _Values), Es), AllVars) :- ','(append(Vars, AllVars1, AllVars), find_all_vars2(Es, AllVars1)).
init_vars2(Notin, E, Einit) :- ','(init_vars3(Notin, E, Einit0), sort(Einit0, Einit)).
init_vars3([], E, E).
init_vars3(.(Var, Vars), E, .(=(.(Var, []), .(unbound, [])), Es)) :- init_vars3(Vars, E, Es).
append([], A, A).
append(.(A, B), C, .(A, D)) :- append(B, C, D).
intersect(As, [], [], [], As) :- !.
intersect([], Bs, [], Bs, []) :- !.
intersect(.(A, As), .(B, Bs), Cs, Ds, Es) :- ;(;(->(=(A, B), ','(=(Cs, .(A, Cs2)), intersect(As, Bs, Cs2, Ds, Es))), ->(@<(A, B), ','(=(Es, .(A, Es2)), intersect(As, .(B, Bs), Cs, Ds, Es2)))), ','(=(Ds, .(B, Ds2)), intersect(.(A, As), Bs, Cs, Ds2, Es))).
get_query(E1, E2) :- ','(=(E1, .(=(X, .(a, [])), .(=(X, .(a, [])), .(=(X, .(a, [])), .(=(X, .(a, [])), []))))), ','(=(E2, .(=(Y, .(a, [])), .(=(Y, .(a, [])), .(=(Y, .(a, [])), .(=(Y, .(a, [])), []))))), ','(=(X, .(5, .(7, .(8, .(3, .(2, .(4, .(1, .(6, .(9, .(15, .(17, .(18, .(13, .(12, .(14, .(11, .(16, .(19, .(25, .(27, .(28, .(23, .(22, .(24, .(21, .(26, .(29, [])))))))))))))))))))))))))))), =(Y, .(15, .(17, .(18, .(13, .(12, .(14, .(11, .(16, .(19, .(35, .(37, .(38, .(33, .(32, .(34, .(5, .(7, .(8, .(3, .(2, .(4, .(1, .(6, .(9, .(31, .(36, .(39, []))))))))))))))))))))))))))))))).

Query: init_vars(g,g,a,a)

(1) 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: init_vars(T1, T2, T3, T4)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: init_vars(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(find_all_vars(T9, X9), ','(find_all_vars(T10, X10), ','(intersect(X9, X10, X11, X12, X13), ','(init_vars2(X12, T9, T13), init_vars2(X13, T10, T14)))))\n\nT9 is ground\nT10 is ground\nX9 is free\nX10 is free\nX11 is free\nX12 is free\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(find_all_vars(T9, X9), ','(find_all_vars(T10, X10), ','(intersect(X9, X10, X11, X12, X13), ','(init_vars2(X12, T9, T13), init_vars2(X13, T10, T14))))), SCOPE: 2, CLAUSE: 1\n\nT9 is ground\nT10 is ground\nX9 is free\nX10 is free\nX11 is free\nX12 is free\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(','(find_all_vars2(T17, X23), sort(X23, X24)), ','(find_all_vars(T10, X10), ','(intersect(X24, X10, X11, X12, X13), ','(init_vars2(X12, T17, T13), init_vars2(X13, T10, T14)))))\n\nT10 is ground\nT17 is ground\nX10 is free\nX11 is free\nX12 is free\nX13 is free\nX24 is free\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: find_all_vars2(T17, X23)\n\nT17 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(sort(T18, X24), ','(find_all_vars(T10, X10), ','(intersect(X24, X10, X11, X12, X13), ','(init_vars2(X12, T17, T13), init_vars2(X13, T10, T14)))))\n\nT10 is ground\nT17 is ground\nX10 is free\nX11 is free\nX12 is free\nX13 is free\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: find_all_vars2(T17, X23), SCOPE: 3, CLAUSE: 2 | find_all_vars2(T17, X23), SCOPE: 3, CLAUSE: 3\n\nT17 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: true | find_all_vars2([], X23), SCOPE: 3, CLAUSE: 3\n\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: find_all_vars2(T17, X23), SCOPE: 3, CLAUSE: 3\n\nT17 is ground\nX23 is free\nfind_all_vars2(T17, X23) !=? find_all_vars2([], [])", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: find_all_vars2([], X23), SCOPE: 3, CLAUSE: 3\n\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(append(T25, X44, X45), find_all_vars2(T27, X44))\n\nT25 is ground\nT27 is ground\nX45 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: append(T25, X44, X45)\n\nT25 is ground\nX45 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: find_all_vars2(T27, T28)\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: append(T25, X44, X45), SCOPE: 4, CLAUSE: 7 | append(T25, X44, X45), SCOPE: 4, CLAUSE: 8\n\nT25 is ground\nX45 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: true | append([], X44, X45), SCOPE: 4, CLAUSE: 8\n\nX45 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: append(T25, X44, X45), SCOPE: 4, CLAUSE: 8\n\nT25 is ground\nX45 is free\nX44 is free\nX58 is free\nappend(T25, X44, X45) !=? append([], X58, X58)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: append([], X44, X45), SCOPE: 4, CLAUSE: 8\n\nX45 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: append(T35, X80, X81)\n\nT35 is ground\nX80 is free\nX81 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: find_all_vars2(T27, T28), SCOPE: 5, CLAUSE: 2 | find_all_vars2(T27, T28), SCOPE: 5, CLAUSE: 3\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: true | find_all_vars2([], T28), SCOPE: 5, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: find_all_vars2(T27, T28), SCOPE: 5, CLAUSE: 3\n\nT27 is ground\nfind_all_vars2(T27, T28) !=? find_all_vars2([], [])", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: find_all_vars2([], T28), SCOPE: 5, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(append(T44, X103, T48), find_all_vars2(T46, X103))\n\nT44 is ground\nT46 is ground\nX103 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: append(T44, X103, T48)\n\nT44 is ground\nX103 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: find_all_vars2(T46, T51)\n\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: append(T44, X103, T48), SCOPE: 6, CLAUSE: 7 | append(T44, X103, T48), SCOPE: 6, CLAUSE: 8\n\nT44 is ground\nX103 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: true | append([], X103, T48), SCOPE: 6, CLAUSE: 8\n\nX103 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: append(T44, X103, T48), SCOPE: 6, CLAUSE: 8\n\nT44 is ground\nX103 is free\nX116 is free\nappend(T44, X103, T48) !=? append([], X116, X116)", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: append([], X103, T48), SCOPE: 6, CLAUSE: 8\n\nX103 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: append(T64, X136, T66)\n\nT64 is ground\nX136 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", 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 -> 4;

81 [label="ONLY EVAL with clause\ninit_vars(X5, X6, X7, X8) :- ','(find_all_vars(X5, X9), ','(find_all_vars(X6, X10), ','(intersect(X9, X10, X11, X12, X13), ','(init_vars2(X12, X5, X7), init_vars2(X13, X6, X8))))).\nand substitutionT1 -> T9,\nX5 -> T9,\nT2 -> T10,\nX6 -> T10,\nT3 -> T13,\nX7 -> T13,\nT4 -> T14,\nX8 -> T14,\nT11 -> T13,\nT12 -> T14", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 81 [arrowhead = none ];
81 -> 5;

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

83 [label="ONLY EVAL with clause\nfind_all_vars(X21, X22) :- ','(find_all_vars2(X21, X23), sort(X23, X22)).\nand substitutionT9 -> T17,\nX21 -> T17,\nX9 -> X24,\nX22 -> X24", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 83 [arrowhead = none ];
83 -> 8;

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

85 [label="SPLIT 2\nnew knowledge:\nT17 is ground\nreplacements:X23 -> T18", fontsize=14, style = filled, fillcolor = violet];
8 -> 85 [arrowhead = none ];
85 -> 11;

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

87 [label="UNDEFINED ERROR", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 87 [arrowhead = none ];
87 -> 79;

88 [label="EVAL with clause\nfind_all_vars2([], []).\nand substitutionT17 -> [],\nX23 -> []", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 88 [arrowhead = none ];
88 -> 15;

89 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 89 [arrowhead = none ];
89 -> 16;

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

91 [label="EVAL with clause\nfind_all_vars2(.(=(X40, X41), X42), X43) :- ','(append(X40, X44, X43), find_all_vars2(X42, X44)).\nand substitutionX40 -> T25,\nX41 -> T26,\nX42 -> T27,\nT17 -> .(=(T25, T26), T27),\nX23 -> X45,\nX43 -> X45", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 91 [arrowhead = none ];
91 -> 26;

92 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 92 [arrowhead = none ];
92 -> 28;

93 [label="BACKTRACK\nfor clause: find_all_vars2(.(=(Vars, _Values), Es), AllVars) :- ','(append(Vars, AllVars1, AllVars), find_all_vars2(Es, AllVars1))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 93 [arrowhead = none ];
93 -> 18;

94 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
26 -> 94 [arrowhead = none ];
94 -> 29;

95 [label="SPLIT 2\nnew knowledge:\nT25 is ground\nreplacements:X44 -> T28,\nX45 -> T29", fontsize=14, style = filled, fillcolor = violet];
26 -> 95 [arrowhead = none ];
95 -> 30;

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

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

98 [label="EVAL with clause\nappend([], X58, X58).\nand substitutionT25 -> [],\nX44 -> X59,\nX58 -> X59,\nX45 -> X59", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 98 [arrowhead = none ];
98 -> 34;

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

100 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
34 -> 100 [arrowhead = none ];
100 -> 36;

101 [label="EVAL with clause\nappend(.(X76, X77), X78, .(X76, X79)) :- append(X77, X78, X79).\nand substitutionX76 -> T34,\nX77 -> T35,\nT25 -> .(T34, T35),\nX44 -> X80,\nX78 -> X80,\nX79 -> X81,\nX45 -> .(T34, X81)", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 101 [arrowhead = none ];
101 -> 44;

102 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 102 [arrowhead = none ];
102 -> 46;

103 [label="BACKTRACK\nfor clause: append(.(A, B), C, .(A, D)) :- append(B, C, D)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 103 [arrowhead = none ];
103 -> 37;

104 [label="INSTANCE with matching:\nT25 -> T35\nX44 -> X80\nX45 -> X81", fontsize=14, style = filled, fillcolor = lightgrey];
44 -> 104 [arrowhead = none , style=dashed];
104 -> 29[style=dashed];

105 [label="EVAL with clause\nfind_all_vars2([], []).\nand substitutionT27 -> [],\nT28 -> []", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 105 [arrowhead = none ];
105 -> 48;

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

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

108 [label="EVAL with clause\nfind_all_vars2(.(=(X99, X100), X101), X102) :- ','(append(X99, X103, X102), find_all_vars2(X101, X103)).\nand substitutionX99 -> T44,\nX100 -> T45,\nX101 -> T46,\nT27 -> .(=(T44, T45), T46),\nT28 -> T48,\nX102 -> T48,\nT47 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 108 [arrowhead = none ];
108 -> 58;

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

110 [label="BACKTRACK\nfor clause: find_all_vars2(.(=(Vars, _Values), Es), AllVars) :- ','(append(Vars, AllVars1, AllVars), find_all_vars2(Es, AllVars1))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
50 -> 110 [arrowhead = none ];
110 -> 53;

111 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
58 -> 111 [arrowhead = none ];
111 -> 61;

112 [label="SPLIT 2\nnew knowledge:\nT44 is ground\nreplacements:X103 -> T51", fontsize=14, style = filled, fillcolor = violet];
58 -> 112 [arrowhead = none ];
112 -> 62;

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

114 [label="INSTANCE with matching:\nT27 -> T46\nT28 -> T51", fontsize=14, style = filled, fillcolor = lightgrey];
62 -> 114 [arrowhead = none , style=dashed];
114 -> 30[style=dashed];

115 [label="EVAL with clause\nappend([], X116, X116).\nand substitutionT44 -> [],\nX103 -> T56,\nX116 -> T56,\nT48 -> T56,\nX117 -> T56", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 115 [arrowhead = none ];
115 -> 66;

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

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

118 [label="EVAL with clause\nappend(.(X132, X133), X134, .(X132, X135)) :- append(X133, X134, X135).\nand substitutionX132 -> T63,\nX133 -> T64,\nT44 -> .(T63, T64),\nX103 -> X136,\nX134 -> X136,\nX135 -> T66,\nT48 -> .(T63, T66),\nT65 -> T66", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 118 [arrowhead = none ];
118 -> 74;

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

120 [label="BACKTRACK\nfor clause: append(.(A, B), C, .(A, D)) :- append(B, C, D)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
68 -> 120 [arrowhead = none ];
120 -> 71;

121 [label="INSTANCE with matching:\nT44 -> T64\nX103 -> X136\nT48 -> T66", fontsize=14, style = filled, fillcolor = lightgrey];
74 -> 121 [arrowhead = none , style=dashed];
121 -> 61[style=dashed];

}

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f8_in(z0, z1), z0, z1)
U1(f8_out1(z0, z1, z2, z3, z4, z5, z6, z7), z8, z9) → f1_out1(z6, z7)
f29_in([]) → f29_out1
f29_in(.(z0, z1)) → U2(f29_in(z1), .(z0, z1))
U2(f29_out1, .(z0, z1)) → f29_out1
f30_in([]) → f30_out1
f30_in(.(=(z0, z1), z2)) → U3(f58_in(z0, z2), .(=(z0, z1), z2))
U3(f58_out1, .(=(z0, z1), z2)) → f30_out1
f61_in([]) → f61_out1
f61_in(.(z0, z1)) → U4(f61_in(z1), .(z0, z1))
U4(f61_out1, .(z0, z1)) → f61_out1
f9_in([]) → f9_out1
f9_in(.(=(z0, z1), z2)) → U5(f26_in(z0, z2), .(=(z0, z1), z2))
U5(f26_out1, .(=(z0, z1), z2)) → f9_out1
f8_in(z0, z1) → U6(f9_in(z0), z0, z1)
U6(f9_out1, z0, z1) → U7(f11_in(z1, z0), z0, z1)
U7(f11_out1(z0, z1, z2, z3, z4, z5, z6, z7), z8, z9) → f8_out1(z0, z1, z2, z3, z4, z5, z6, z7)
f26_in(z0, z1) → U8(f29_in(z0), z0, z1)
U8(f29_out1, z0, z1) → U9(f30_in(z1), z0, z1)
U9(f30_out1, z0, z1) → f26_out1
f58_in(z0, z1) → U10(f61_in(z0), z0, z1)
U10(f61_out1, z0, z1) → U11(f30_in(z1), z0, z1)
U11(f30_out1, z0, z1) → f58_out1

Tuples:

F1_IN(z0, z1) → c(U1'(f8_in(z0, z1), z0, z1), F8_IN(z0, z1))
F29_IN(.(z0, z1)) → c3(U2'(f29_in(z1), .(z0, z1)), F29_IN(z1))
F30_IN(.(=(z0, z1), z2)) → c6(U3'(f58_in(z0, z2), .(=(z0, z1), z2)), F58_IN(z0, z2))
F61_IN(.(z0, z1)) → c9(U4'(f61_in(z1), .(z0, z1)), F61_IN(z1))
F9_IN(.(=(z0, z1), z2)) → c12(U5'(f26_in(z0, z2), .(=(z0, z1), z2)), F26_IN(z0, z2))
F8_IN(z0, z1) → c14(U6'(f9_in(z0), z0, z1), F9_IN(z0))
U6'(f9_out1, z0, z1) → c15(U7'(f11_in(z1, z0), z0, z1))
F26_IN(z0, z1) → c17(U8'(f29_in(z0), z0, z1), F29_IN(z0))
U8'(f29_out1, z0, z1) → c18(U9'(f30_in(z1), z0, z1), F30_IN(z1))
F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
U10'(f61_out1, z0, z1) → c21(U11'(f30_in(z1), z0, z1), F30_IN(z1))

S tuples:

F1_IN(z0, z1) → c(U1'(f8_in(z0, z1), z0, z1), F8_IN(z0, z1))
F29_IN(.(z0, z1)) → c3(U2'(f29_in(z1), .(z0, z1)), F29_IN(z1))
F30_IN(.(=(z0, z1), z2)) → c6(U3'(f58_in(z0, z2), .(=(z0, z1), z2)), F58_IN(z0, z2))
F61_IN(.(z0, z1)) → c9(U4'(f61_in(z1), .(z0, z1)), F61_IN(z1))
F9_IN(.(=(z0, z1), z2)) → c12(U5'(f26_in(z0, z2), .(=(z0, z1), z2)), F26_IN(z0, z2))
F8_IN(z0, z1) → c14(U6'(f9_in(z0), z0, z1), F9_IN(z0))
U6'(f9_out1, z0, z1) → c15(U7'(f11_in(z1, z0), z0, z1))
F26_IN(z0, z1) → c17(U8'(f29_in(z0), z0, z1), F29_IN(z0))
U8'(f29_out1, z0, z1) → c18(U9'(f30_in(z1), z0, z1), F30_IN(z1))
F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
U10'(f61_out1, z0, z1) → c21(U11'(f30_in(z1), z0, z1), F30_IN(z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f29_in, U2, f30_in, U3, f61_in, U4, f9_in, U5, f8_in, U6, U7, f26_in, U8, U9, f58_in, U10, U11

Defined Pair Symbols:

F1_IN, F29_IN, F30_IN, F61_IN, F9_IN, F8_IN, U6', F26_IN, U8', F58_IN, U10'

Compound Symbols:

c, c3, c6, c9, c12, c14, c15, c17, c18, c20, c21

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

Split RHS of tuples not part of any SCC

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f8_in(z0, z1), z0, z1)
U1(f8_out1(z0, z1, z2, z3, z4, z5, z6, z7), z8, z9) → f1_out1(z6, z7)
f29_in([]) → f29_out1
f29_in(.(z0, z1)) → U2(f29_in(z1), .(z0, z1))
U2(f29_out1, .(z0, z1)) → f29_out1
f30_in([]) → f30_out1
f30_in(.(=(z0, z1), z2)) → U3(f58_in(z0, z2), .(=(z0, z1), z2))
U3(f58_out1, .(=(z0, z1), z2)) → f30_out1
f61_in([]) → f61_out1
f61_in(.(z0, z1)) → U4(f61_in(z1), .(z0, z1))
U4(f61_out1, .(z0, z1)) → f61_out1
f9_in([]) → f9_out1
f9_in(.(=(z0, z1), z2)) → U5(f26_in(z0, z2), .(=(z0, z1), z2))
U5(f26_out1, .(=(z0, z1), z2)) → f9_out1
f8_in(z0, z1) → U6(f9_in(z0), z0, z1)
U6(f9_out1, z0, z1) → U7(f11_in(z1, z0), z0, z1)
U7(f11_out1(z0, z1, z2, z3, z4, z5, z6, z7), z8, z9) → f8_out1(z0, z1, z2, z3, z4, z5, z6, z7)
f26_in(z0, z1) → U8(f29_in(z0), z0, z1)
U8(f29_out1, z0, z1) → U9(f30_in(z1), z0, z1)
U9(f30_out1, z0, z1) → f26_out1
f58_in(z0, z1) → U10(f61_in(z0), z0, z1)
U10(f61_out1, z0, z1) → U11(f30_in(z1), z0, z1)
U11(f30_out1, z0, z1) → f58_out1

Tuples:

F29_IN(.(z0, z1)) → c3(U2'(f29_in(z1), .(z0, z1)), F29_IN(z1))
F30_IN(.(=(z0, z1), z2)) → c6(U3'(f58_in(z0, z2), .(=(z0, z1), z2)), F58_IN(z0, z2))
F61_IN(.(z0, z1)) → c9(U4'(f61_in(z1), .(z0, z1)), F61_IN(z1))
U6'(f9_out1, z0, z1) → c15(U7'(f11_in(z1, z0), z0, z1))
F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
U10'(f61_out1, z0, z1) → c21(U11'(f30_in(z1), z0, z1), F30_IN(z1))
F1_IN(z0, z1) → c1(U1'(f8_in(z0, z1), z0, z1))
F1_IN(z0, z1) → c1(F8_IN(z0, z1))
F9_IN(.(=(z0, z1), z2)) → c1(U5'(f26_in(z0, z2), .(=(z0, z1), z2)))
F9_IN(.(=(z0, z1), z2)) → c1(F26_IN(z0, z2))
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
F26_IN(z0, z1) → c1(U8'(f29_in(z0), z0, z1))
F26_IN(z0, z1) → c1(F29_IN(z0))
U8'(f29_out1, z0, z1) → c1(U9'(f30_in(z1), z0, z1))
U8'(f29_out1, z0, z1) → c1(F30_IN(z1))

S tuples:

F29_IN(.(z0, z1)) → c3(U2'(f29_in(z1), .(z0, z1)), F29_IN(z1))
F30_IN(.(=(z0, z1), z2)) → c6(U3'(f58_in(z0, z2), .(=(z0, z1), z2)), F58_IN(z0, z2))
F61_IN(.(z0, z1)) → c9(U4'(f61_in(z1), .(z0, z1)), F61_IN(z1))
U6'(f9_out1, z0, z1) → c15(U7'(f11_in(z1, z0), z0, z1))
F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
U10'(f61_out1, z0, z1) → c21(U11'(f30_in(z1), z0, z1), F30_IN(z1))
F1_IN(z0, z1) → c1(U1'(f8_in(z0, z1), z0, z1))
F1_IN(z0, z1) → c1(F8_IN(z0, z1))
F9_IN(.(=(z0, z1), z2)) → c1(U5'(f26_in(z0, z2), .(=(z0, z1), z2)))
F9_IN(.(=(z0, z1), z2)) → c1(F26_IN(z0, z2))
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
F26_IN(z0, z1) → c1(U8'(f29_in(z0), z0, z1))
F26_IN(z0, z1) → c1(F29_IN(z0))
U8'(f29_out1, z0, z1) → c1(U9'(f30_in(z1), z0, z1))
U8'(f29_out1, z0, z1) → c1(F30_IN(z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f29_in, U2, f30_in, U3, f61_in, U4, f9_in, U5, f8_in, U6, U7, f26_in, U8, U9, f58_in, U10, U11

Defined Pair Symbols:

F29_IN, F30_IN, F61_IN, U6', F58_IN, U10', F1_IN, F9_IN, F8_IN, F26_IN, U8'

Compound Symbols:

c3, c6, c9, c15, c20, c21, c1

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

Removed 8 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f8_in(z0, z1), z0, z1)
U1(f8_out1(z0, z1, z2, z3, z4, z5, z6, z7), z8, z9) → f1_out1(z6, z7)
f29_in([]) → f29_out1
f29_in(.(z0, z1)) → U2(f29_in(z1), .(z0, z1))
U2(f29_out1, .(z0, z1)) → f29_out1
f30_in([]) → f30_out1
f30_in(.(=(z0, z1), z2)) → U3(f58_in(z0, z2), .(=(z0, z1), z2))
U3(f58_out1, .(=(z0, z1), z2)) → f30_out1
f61_in([]) → f61_out1
f61_in(.(z0, z1)) → U4(f61_in(z1), .(z0, z1))
U4(f61_out1, .(z0, z1)) → f61_out1
f9_in([]) → f9_out1
f9_in(.(=(z0, z1), z2)) → U5(f26_in(z0, z2), .(=(z0, z1), z2))
U5(f26_out1, .(=(z0, z1), z2)) → f9_out1
f8_in(z0, z1) → U6(f9_in(z0), z0, z1)
U6(f9_out1, z0, z1) → U7(f11_in(z1, z0), z0, z1)
U7(f11_out1(z0, z1, z2, z3, z4, z5, z6, z7), z8, z9) → f8_out1(z0, z1, z2, z3, z4, z5, z6, z7)
f26_in(z0, z1) → U8(f29_in(z0), z0, z1)
U8(f29_out1, z0, z1) → U9(f30_in(z1), z0, z1)
U9(f30_out1, z0, z1) → f26_out1
f58_in(z0, z1) → U10(f61_in(z0), z0, z1)
U10(f61_out1, z0, z1) → U11(f30_in(z1), z0, z1)
U11(f30_out1, z0, z1) → f58_out1

Tuples:

F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
F1_IN(z0, z1) → c1(F8_IN(z0, z1))
F9_IN(.(=(z0, z1), z2)) → c1(F26_IN(z0, z2))
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
F26_IN(z0, z1) → c1(U8'(f29_in(z0), z0, z1))
F26_IN(z0, z1) → c1(F29_IN(z0))
U8'(f29_out1, z0, z1) → c1(F30_IN(z1))
F29_IN(.(z0, z1)) → c3(F29_IN(z1))
F30_IN(.(=(z0, z1), z2)) → c6(F58_IN(z0, z2))
F61_IN(.(z0, z1)) → c9(F61_IN(z1))
U6'(f9_out1, z0, z1) → c15
U10'(f61_out1, z0, z1) → c21(F30_IN(z1))
F1_IN(z0, z1) → c1
F9_IN(.(=(z0, z1), z2)) → c1
U8'(f29_out1, z0, z1) → c1

S tuples:

F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
F1_IN(z0, z1) → c1(F8_IN(z0, z1))
F9_IN(.(=(z0, z1), z2)) → c1(F26_IN(z0, z2))
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
F26_IN(z0, z1) → c1(U8'(f29_in(z0), z0, z1))
F26_IN(z0, z1) → c1(F29_IN(z0))
U8'(f29_out1, z0, z1) → c1(F30_IN(z1))
F29_IN(.(z0, z1)) → c3(F29_IN(z1))
F30_IN(.(=(z0, z1), z2)) → c6(F58_IN(z0, z2))
F61_IN(.(z0, z1)) → c9(F61_IN(z1))
U6'(f9_out1, z0, z1) → c15
U10'(f61_out1, z0, z1) → c21(F30_IN(z1))
F1_IN(z0, z1) → c1
F9_IN(.(=(z0, z1), z2)) → c1
U8'(f29_out1, z0, z1) → c1

K tuples:none
Defined Rule Symbols:

f1_in, U1, f29_in, U2, f30_in, U3, f61_in, U4, f9_in, U5, f8_in, U6, U7, f26_in, U8, U9, f58_in, U10, U11

Defined Pair Symbols:

F58_IN, F1_IN, F9_IN, F8_IN, F26_IN, U8', F29_IN, F30_IN, F61_IN, U6', U10'

Compound Symbols:

c20, c1, c3, c6, c9, c15, c21, c1

(7) CdtKnowledgeProof (EQUIVALENT transformation)

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

F1_IN(z0, z1) → c1(F8_IN(z0, z1))
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
U6'(f9_out1, z0, z1) → c15
F1_IN(z0, z1) → c1
F9_IN(.(=(z0, z1), z2)) → c1
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
U6'(f9_out1, z0, z1) → c15
F9_IN(.(=(z0, z1), z2)) → c1(F26_IN(z0, z2))
F9_IN(.(=(z0, z1), z2)) → c1
F26_IN(z0, z1) → c1(U8'(f29_in(z0), z0, z1))
F26_IN(z0, z1) → c1(F29_IN(z0))
U8'(f29_out1, z0, z1) → c1(F30_IN(z1))
U8'(f29_out1, z0, z1) → c1

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f8_in(z0, z1), z0, z1)
U1(f8_out1(z0, z1, z2, z3, z4, z5, z6, z7), z8, z9) → f1_out1(z6, z7)
f29_in([]) → f29_out1
f29_in(.(z0, z1)) → U2(f29_in(z1), .(z0, z1))
U2(f29_out1, .(z0, z1)) → f29_out1
f30_in([]) → f30_out1
f30_in(.(=(z0, z1), z2)) → U3(f58_in(z0, z2), .(=(z0, z1), z2))
U3(f58_out1, .(=(z0, z1), z2)) → f30_out1
f61_in([]) → f61_out1
f61_in(.(z0, z1)) → U4(f61_in(z1), .(z0, z1))
U4(f61_out1, .(z0, z1)) → f61_out1
f9_in([]) → f9_out1
f9_in(.(=(z0, z1), z2)) → U5(f26_in(z0, z2), .(=(z0, z1), z2))
U5(f26_out1, .(=(z0, z1), z2)) → f9_out1
f8_in(z0, z1) → U6(f9_in(z0), z0, z1)
U6(f9_out1, z0, z1) → U7(f11_in(z1, z0), z0, z1)
U7(f11_out1(z0, z1, z2, z3, z4, z5, z6, z7), z8, z9) → f8_out1(z0, z1, z2, z3, z4, z5, z6, z7)
f26_in(z0, z1) → U8(f29_in(z0), z0, z1)
U8(f29_out1, z0, z1) → U9(f30_in(z1), z0, z1)
U9(f30_out1, z0, z1) → f26_out1
f58_in(z0, z1) → U10(f61_in(z0), z0, z1)
U10(f61_out1, z0, z1) → U11(f30_in(z1), z0, z1)
U11(f30_out1, z0, z1) → f58_out1

Tuples:

F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
F1_IN(z0, z1) → c1(F8_IN(z0, z1))
F9_IN(.(=(z0, z1), z2)) → c1(F26_IN(z0, z2))
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
F26_IN(z0, z1) → c1(U8'(f29_in(z0), z0, z1))
F26_IN(z0, z1) → c1(F29_IN(z0))
U8'(f29_out1, z0, z1) → c1(F30_IN(z1))
F29_IN(.(z0, z1)) → c3(F29_IN(z1))
F30_IN(.(=(z0, z1), z2)) → c6(F58_IN(z0, z2))
F61_IN(.(z0, z1)) → c9(F61_IN(z1))
U6'(f9_out1, z0, z1) → c15
U10'(f61_out1, z0, z1) → c21(F30_IN(z1))
F1_IN(z0, z1) → c1
F9_IN(.(=(z0, z1), z2)) → c1
U8'(f29_out1, z0, z1) → c1

S tuples:

F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
F29_IN(.(z0, z1)) → c3(F29_IN(z1))
F30_IN(.(=(z0, z1), z2)) → c6(F58_IN(z0, z2))
F61_IN(.(z0, z1)) → c9(F61_IN(z1))
U10'(f61_out1, z0, z1) → c21(F30_IN(z1))

K tuples:

F1_IN(z0, z1) → c1(F8_IN(z0, z1))
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
U6'(f9_out1, z0, z1) → c15
F1_IN(z0, z1) → c1
F9_IN(.(=(z0, z1), z2)) → c1
F9_IN(.(=(z0, z1), z2)) → c1(F26_IN(z0, z2))
F26_IN(z0, z1) → c1(U8'(f29_in(z0), z0, z1))
F26_IN(z0, z1) → c1(F29_IN(z0))
U8'(f29_out1, z0, z1) → c1(F30_IN(z1))
U8'(f29_out1, z0, z1) → c1

Defined Rule Symbols:

f1_in, U1, f29_in, U2, f30_in, U3, f61_in, U4, f9_in, U5, f8_in, U6, U7, f26_in, U8, U9, f58_in, U10, U11

Defined Pair Symbols:

F58_IN, F1_IN, F9_IN, F8_IN, F26_IN, U8', F29_IN, F30_IN, F61_IN, U6', U10'

Compound Symbols:

c20, c1, c3, c6, c9, c15, c21, c1

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

F29_IN(.(z0, z1)) → c3(F29_IN(z1))

We considered the (Usable) Rules:

f29_in([]) → f29_out1
f29_in(.(z0, z1)) → U2(f29_in(z1), .(z0, z1))
U2(f29_out1, .(z0, z1)) → f29_out1
f9_in([]) → f9_out1
f9_in(.(=(z0, z1), z2)) → U5(f26_in(z0, z2), .(=(z0, z1), z2))
f26_in(z0, z1) → U8(f29_in(z0), z0, z1)
U5(f26_out1, .(=(z0, z1), z2)) → f9_out1
U8(f29_out1, z0, z1) → U9(f30_in(z1), z0, z1)
f30_in([]) → f30_out1
f30_in(.(=(z0, z1), z2)) → U3(f58_in(z0, z2), .(=(z0, z1), z2))
U9(f30_out1, z0, z1) → f26_out1
f58_in(z0, z1) → U10(f61_in(z0), z0, z1)
U3(f58_out1, .(=(z0, z1), z2)) → f30_out1
f61_in([]) → f61_out1
f61_in(.(z0, z1)) → U4(f61_in(z1), .(z0, z1))
U10(f61_out1, z0, z1) → U11(f30_in(z1), z0, z1)
U11(f30_out1, z0, z1) → f58_out1
U4(f61_out1, .(z0, z1)) → f61_out1

And the Tuples:

F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
F1_IN(z0, z1) → c1(F8_IN(z0, z1))
F9_IN(.(=(z0, z1), z2)) → c1(F26_IN(z0, z2))
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
F26_IN(z0, z1) → c1(U8'(f29_in(z0), z0, z1))
F26_IN(z0, z1) → c1(F29_IN(z0))
U8'(f29_out1, z0, z1) → c1(F30_IN(z1))
F29_IN(.(z0, z1)) → c3(F29_IN(z1))
F30_IN(.(=(z0, z1), z2)) → c6(F58_IN(z0, z2))
F61_IN(.(z0, z1)) → c9(F61_IN(z1))
U6'(f9_out1, z0, z1) → c15
U10'(f61_out1, z0, z1) → c21(F30_IN(z1))
F1_IN(z0, z1) → c1
F9_IN(.(=(z0, z1), z2)) → c1
U8'(f29_out1, z0, z1) → c1

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

POL(.(x₁, x₂)) = [1] + x₁ + x₂   
POL(=(x₁, x₂)) = [2] + x₁ + x₂   
POL(F1_IN(x₁, x₂)) = [3] + [3]x₁ + [2]x₂   
POL(F26_IN(x₁, x₂)) = [3] + x₁   
POL(F29_IN(x₁)) = x₁   
POL(F30_IN(x₁)) = 0   
POL(F58_IN(x₁, x₂)) = 0   
POL(F61_IN(x₁)) = 0   
POL(F8_IN(x₁, x₂)) = [2] + [3]x₁ + x₂   
POL(F9_IN(x₁)) = [2] + [3]x₁   
POL(U10(x₁, x₂, x₃)) = [2]x₃   
POL(U10'(x₁, x₂, x₃)) = 0   
POL(U11(x₁, x₂, x₃)) = 0   
POL(U2(x₁, x₂)) = x₂   
POL(U3(x₁, x₂)) = 0   
POL(U4(x₁, x₂)) = 0   
POL(U5(x₁, x₂)) = x₂   
POL(U6'(x₁, x₂, x₃)) = [1] + x₁ + x₂   
POL(U8(x₁, x₂, x₃)) = [3] + [2]x₂ + [2]x₃   
POL(U8'(x₁, x₂, x₃)) = [1]   
POL(U9(x₁, x₂, x₃)) = [3] + x₂ + x₃   
POL([]) = 0   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c15) = 0   
POL(c20(x₁, x₂)) = x₁ + x₂   
POL(c21(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c9(x₁)) = x₁   
POL(f26_in(x₁, x₂)) = [3] + [2]x₁ + [3]x₂   
POL(f26_out1) = [2]   
POL(f29_in(x₁)) = x₁   
POL(f29_out1) = 0   
POL(f30_in(x₁)) = 0   
POL(f30_out1) = 0   
POL(f58_in(x₁, x₂)) = [3] + [2]x₂   
POL(f58_out1) = 0   
POL(f61_in(x₁)) = 0   
POL(f61_out1) = 0   
POL(f9_in(x₁)) = [2]x₁   
POL(f9_out1) = 0   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f8_in(z0, z1), z0, z1)
U1(f8_out1(z0, z1, z2, z3, z4, z5, z6, z7), z8, z9) → f1_out1(z6, z7)
f29_in([]) → f29_out1
f29_in(.(z0, z1)) → U2(f29_in(z1), .(z0, z1))
U2(f29_out1, .(z0, z1)) → f29_out1
f30_in([]) → f30_out1
f30_in(.(=(z0, z1), z2)) → U3(f58_in(z0, z2), .(=(z0, z1), z2))
U3(f58_out1, .(=(z0, z1), z2)) → f30_out1
f61_in([]) → f61_out1
f61_in(.(z0, z1)) → U4(f61_in(z1), .(z0, z1))
U4(f61_out1, .(z0, z1)) → f61_out1
f9_in([]) → f9_out1
f9_in(.(=(z0, z1), z2)) → U5(f26_in(z0, z2), .(=(z0, z1), z2))
U5(f26_out1, .(=(z0, z1), z2)) → f9_out1
f8_in(z0, z1) → U6(f9_in(z0), z0, z1)
U6(f9_out1, z0, z1) → U7(f11_in(z1, z0), z0, z1)
U7(f11_out1(z0, z1, z2, z3, z4, z5, z6, z7), z8, z9) → f8_out1(z0, z1, z2, z3, z4, z5, z6, z7)
f26_in(z0, z1) → U8(f29_in(z0), z0, z1)
U8(f29_out1, z0, z1) → U9(f30_in(z1), z0, z1)
U9(f30_out1, z0, z1) → f26_out1
f58_in(z0, z1) → U10(f61_in(z0), z0, z1)
U10(f61_out1, z0, z1) → U11(f30_in(z1), z0, z1)
U11(f30_out1, z0, z1) → f58_out1

Tuples:

F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
F1_IN(z0, z1) → c1(F8_IN(z0, z1))
F9_IN(.(=(z0, z1), z2)) → c1(F26_IN(z0, z2))
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
F26_IN(z0, z1) → c1(U8'(f29_in(z0), z0, z1))
F26_IN(z0, z1) → c1(F29_IN(z0))
U8'(f29_out1, z0, z1) → c1(F30_IN(z1))
F29_IN(.(z0, z1)) → c3(F29_IN(z1))
F30_IN(.(=(z0, z1), z2)) → c6(F58_IN(z0, z2))
F61_IN(.(z0, z1)) → c9(F61_IN(z1))
U6'(f9_out1, z0, z1) → c15
U10'(f61_out1, z0, z1) → c21(F30_IN(z1))
F1_IN(z0, z1) → c1
F9_IN(.(=(z0, z1), z2)) → c1
U8'(f29_out1, z0, z1) → c1

S tuples:

F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
F30_IN(.(=(z0, z1), z2)) → c6(F58_IN(z0, z2))
F61_IN(.(z0, z1)) → c9(F61_IN(z1))
U10'(f61_out1, z0, z1) → c21(F30_IN(z1))

K tuples:

F1_IN(z0, z1) → c1(F8_IN(z0, z1))
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
U6'(f9_out1, z0, z1) → c15
F1_IN(z0, z1) → c1
F9_IN(.(=(z0, z1), z2)) → c1
F9_IN(.(=(z0, z1), z2)) → c1(F26_IN(z0, z2))
F26_IN(z0, z1) → c1(U8'(f29_in(z0), z0, z1))
F26_IN(z0, z1) → c1(F29_IN(z0))
U8'(f29_out1, z0, z1) → c1(F30_IN(z1))
U8'(f29_out1, z0, z1) → c1
F29_IN(.(z0, z1)) → c3(F29_IN(z1))

Defined Rule Symbols:

f1_in, U1, f29_in, U2, f30_in, U3, f61_in, U4, f9_in, U5, f8_in, U6, U7, f26_in, U8, U9, f58_in, U10, U11

Defined Pair Symbols:

F58_IN, F1_IN, F9_IN, F8_IN, F26_IN, U8', F29_IN, F30_IN, F61_IN, U6', U10'

Compound Symbols:

c20, c1, c3, c6, c9, c15, c21, c1

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

F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
F30_IN(.(=(z0, z1), z2)) → c6(F58_IN(z0, z2))

We considered the (Usable) Rules:

f29_in([]) → f29_out1
f29_in(.(z0, z1)) → U2(f29_in(z1), .(z0, z1))
U2(f29_out1, .(z0, z1)) → f29_out1
f9_in([]) → f9_out1
f9_in(.(=(z0, z1), z2)) → U5(f26_in(z0, z2), .(=(z0, z1), z2))
f26_in(z0, z1) → U8(f29_in(z0), z0, z1)
U5(f26_out1, .(=(z0, z1), z2)) → f9_out1
U8(f29_out1, z0, z1) → U9(f30_in(z1), z0, z1)
f30_in([]) → f30_out1
f30_in(.(=(z0, z1), z2)) → U3(f58_in(z0, z2), .(=(z0, z1), z2))
U9(f30_out1, z0, z1) → f26_out1
f58_in(z0, z1) → U10(f61_in(z0), z0, z1)
U3(f58_out1, .(=(z0, z1), z2)) → f30_out1
f61_in([]) → f61_out1
f61_in(.(z0, z1)) → U4(f61_in(z1), .(z0, z1))
U10(f61_out1, z0, z1) → U11(f30_in(z1), z0, z1)
U11(f30_out1, z0, z1) → f58_out1
U4(f61_out1, .(z0, z1)) → f61_out1

And the Tuples:

F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
F1_IN(z0, z1) → c1(F8_IN(z0, z1))
F9_IN(.(=(z0, z1), z2)) → c1(F26_IN(z0, z2))
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
F26_IN(z0, z1) → c1(U8'(f29_in(z0), z0, z1))
F26_IN(z0, z1) → c1(F29_IN(z0))
U8'(f29_out1, z0, z1) → c1(F30_IN(z1))
F29_IN(.(z0, z1)) → c3(F29_IN(z1))
F30_IN(.(=(z0, z1), z2)) → c6(F58_IN(z0, z2))
F61_IN(.(z0, z1)) → c9(F61_IN(z1))
U6'(f9_out1, z0, z1) → c15
U10'(f61_out1, z0, z1) → c21(F30_IN(z1))
F1_IN(z0, z1) → c1
F9_IN(.(=(z0, z1), z2)) → c1
U8'(f29_out1, z0, z1) → c1

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

POL(.(x₁, x₂)) = [2] + x₂   
POL(=(x₁, x₂)) = 0   
POL(F1_IN(x₁, x₂)) = [2] + [2]x₁ + [2]x₂   
POL(F26_IN(x₁, x₂)) = [1] + [2]x₂   
POL(F29_IN(x₁)) = [1]   
POL(F30_IN(x₁)) = [2]x₁   
POL(F58_IN(x₁, x₂)) = [1] + [2]x₂   
POL(F61_IN(x₁)) = 0   
POL(F8_IN(x₁, x₂)) = [1] + [2]x₁   
POL(F9_IN(x₁)) = [2]x₁   
POL(U10(x₁, x₂, x₃)) = [3] + [3]x₃   
POL(U10'(x₁, x₂, x₃)) = [2]x₃   
POL(U11(x₁, x₂, x₃)) = [1] + x₁   
POL(U2(x₁, x₂)) = 0   
POL(U3(x₁, x₂)) = [2]x₂   
POL(U4(x₁, x₂)) = 0   
POL(U5(x₁, x₂)) = [3]x₁   
POL(U6'(x₁, x₂, x₃)) = 0   
POL(U8(x₁, x₂, x₃)) = 0   
POL(U8'(x₁, x₂, x₃)) = [2]x₃   
POL(U9(x₁, x₂, x₃)) = 0   
POL([]) = [2]   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c15) = 0   
POL(c20(x₁, x₂)) = x₁ + x₂   
POL(c21(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c9(x₁)) = x₁   
POL(f26_in(x₁, x₂)) = x₂   
POL(f26_out1) = 0   
POL(f29_in(x₁)) = [2]   
POL(f29_out1) = 0   
POL(f30_in(x₁)) = [2] + [3]x₁   
POL(f30_out1) = [3]   
POL(f58_in(x₁, x₂)) = [3] + x₁ + [3]x₂   
POL(f58_out1) = [2]   
POL(f61_in(x₁)) = 0   
POL(f61_out1) = 0   
POL(f9_in(x₁)) = [2] + [3]x₁   
POL(f9_out1) = 0   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f8_in(z0, z1), z0, z1)
U1(f8_out1(z0, z1, z2, z3, z4, z5, z6, z7), z8, z9) → f1_out1(z6, z7)
f29_in([]) → f29_out1
f29_in(.(z0, z1)) → U2(f29_in(z1), .(z0, z1))
U2(f29_out1, .(z0, z1)) → f29_out1
f30_in([]) → f30_out1
f30_in(.(=(z0, z1), z2)) → U3(f58_in(z0, z2), .(=(z0, z1), z2))
U3(f58_out1, .(=(z0, z1), z2)) → f30_out1
f61_in([]) → f61_out1
f61_in(.(z0, z1)) → U4(f61_in(z1), .(z0, z1))
U4(f61_out1, .(z0, z1)) → f61_out1
f9_in([]) → f9_out1
f9_in(.(=(z0, z1), z2)) → U5(f26_in(z0, z2), .(=(z0, z1), z2))
U5(f26_out1, .(=(z0, z1), z2)) → f9_out1
f8_in(z0, z1) → U6(f9_in(z0), z0, z1)
U6(f9_out1, z0, z1) → U7(f11_in(z1, z0), z0, z1)
U7(f11_out1(z0, z1, z2, z3, z4, z5, z6, z7), z8, z9) → f8_out1(z0, z1, z2, z3, z4, z5, z6, z7)
f26_in(z0, z1) → U8(f29_in(z0), z0, z1)
U8(f29_out1, z0, z1) → U9(f30_in(z1), z0, z1)
U9(f30_out1, z0, z1) → f26_out1
f58_in(z0, z1) → U10(f61_in(z0), z0, z1)
U10(f61_out1, z0, z1) → U11(f30_in(z1), z0, z1)
U11(f30_out1, z0, z1) → f58_out1

Tuples:

F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
F1_IN(z0, z1) → c1(F8_IN(z0, z1))
F9_IN(.(=(z0, z1), z2)) → c1(F26_IN(z0, z2))
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
F26_IN(z0, z1) → c1(U8'(f29_in(z0), z0, z1))
F26_IN(z0, z1) → c1(F29_IN(z0))
U8'(f29_out1, z0, z1) → c1(F30_IN(z1))
F29_IN(.(z0, z1)) → c3(F29_IN(z1))
F30_IN(.(=(z0, z1), z2)) → c6(F58_IN(z0, z2))
F61_IN(.(z0, z1)) → c9(F61_IN(z1))
U6'(f9_out1, z0, z1) → c15
U10'(f61_out1, z0, z1) → c21(F30_IN(z1))
F1_IN(z0, z1) → c1
F9_IN(.(=(z0, z1), z2)) → c1
U8'(f29_out1, z0, z1) → c1

S tuples:

F61_IN(.(z0, z1)) → c9(F61_IN(z1))
U10'(f61_out1, z0, z1) → c21(F30_IN(z1))

K tuples:

F1_IN(z0, z1) → c1(F8_IN(z0, z1))
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
U6'(f9_out1, z0, z1) → c15
F1_IN(z0, z1) → c1
F9_IN(.(=(z0, z1), z2)) → c1
F9_IN(.(=(z0, z1), z2)) → c1(F26_IN(z0, z2))
F26_IN(z0, z1) → c1(U8'(f29_in(z0), z0, z1))
F26_IN(z0, z1) → c1(F29_IN(z0))
U8'(f29_out1, z0, z1) → c1(F30_IN(z1))
U8'(f29_out1, z0, z1) → c1
F29_IN(.(z0, z1)) → c3(F29_IN(z1))
F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
F30_IN(.(=(z0, z1), z2)) → c6(F58_IN(z0, z2))

Defined Rule Symbols:

f1_in, U1, f29_in, U2, f30_in, U3, f61_in, U4, f9_in, U5, f8_in, U6, U7, f26_in, U8, U9, f58_in, U10, U11

Defined Pair Symbols:

F58_IN, F1_IN, F9_IN, F8_IN, F26_IN, U8', F29_IN, F30_IN, F61_IN, U6', U10'

Compound Symbols:

c20, c1, c3, c6, c9, c15, c21, c1

(13) CdtKnowledgeProof (EQUIVALENT transformation)

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

U10'(f61_out1, z0, z1) → c21(F30_IN(z1))
F30_IN(.(=(z0, z1), z2)) → c6(F58_IN(z0, z2))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f8_in(z0, z1), z0, z1)
U1(f8_out1(z0, z1, z2, z3, z4, z5, z6, z7), z8, z9) → f1_out1(z6, z7)
f29_in([]) → f29_out1
f29_in(.(z0, z1)) → U2(f29_in(z1), .(z0, z1))
U2(f29_out1, .(z0, z1)) → f29_out1
f30_in([]) → f30_out1
f30_in(.(=(z0, z1), z2)) → U3(f58_in(z0, z2), .(=(z0, z1), z2))
U3(f58_out1, .(=(z0, z1), z2)) → f30_out1
f61_in([]) → f61_out1
f61_in(.(z0, z1)) → U4(f61_in(z1), .(z0, z1))
U4(f61_out1, .(z0, z1)) → f61_out1
f9_in([]) → f9_out1
f9_in(.(=(z0, z1), z2)) → U5(f26_in(z0, z2), .(=(z0, z1), z2))
U5(f26_out1, .(=(z0, z1), z2)) → f9_out1
f8_in(z0, z1) → U6(f9_in(z0), z0, z1)
U6(f9_out1, z0, z1) → U7(f11_in(z1, z0), z0, z1)
U7(f11_out1(z0, z1, z2, z3, z4, z5, z6, z7), z8, z9) → f8_out1(z0, z1, z2, z3, z4, z5, z6, z7)
f26_in(z0, z1) → U8(f29_in(z0), z0, z1)
U8(f29_out1, z0, z1) → U9(f30_in(z1), z0, z1)
U9(f30_out1, z0, z1) → f26_out1
f58_in(z0, z1) → U10(f61_in(z0), z0, z1)
U10(f61_out1, z0, z1) → U11(f30_in(z1), z0, z1)
U11(f30_out1, z0, z1) → f58_out1

Tuples:

F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
F1_IN(z0, z1) → c1(F8_IN(z0, z1))
F9_IN(.(=(z0, z1), z2)) → c1(F26_IN(z0, z2))
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
F26_IN(z0, z1) → c1(U8'(f29_in(z0), z0, z1))
F26_IN(z0, z1) → c1(F29_IN(z0))
U8'(f29_out1, z0, z1) → c1(F30_IN(z1))
F29_IN(.(z0, z1)) → c3(F29_IN(z1))
F30_IN(.(=(z0, z1), z2)) → c6(F58_IN(z0, z2))
F61_IN(.(z0, z1)) → c9(F61_IN(z1))
U6'(f9_out1, z0, z1) → c15
U10'(f61_out1, z0, z1) → c21(F30_IN(z1))
F1_IN(z0, z1) → c1
F9_IN(.(=(z0, z1), z2)) → c1
U8'(f29_out1, z0, z1) → c1

S tuples:

F61_IN(.(z0, z1)) → c9(F61_IN(z1))

K tuples:

F1_IN(z0, z1) → c1(F8_IN(z0, z1))
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
U6'(f9_out1, z0, z1) → c15
F1_IN(z0, z1) → c1
F9_IN(.(=(z0, z1), z2)) → c1
F9_IN(.(=(z0, z1), z2)) → c1(F26_IN(z0, z2))
F26_IN(z0, z1) → c1(U8'(f29_in(z0), z0, z1))
F26_IN(z0, z1) → c1(F29_IN(z0))
U8'(f29_out1, z0, z1) → c1(F30_IN(z1))
U8'(f29_out1, z0, z1) → c1
F29_IN(.(z0, z1)) → c3(F29_IN(z1))
F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
F30_IN(.(=(z0, z1), z2)) → c6(F58_IN(z0, z2))
U10'(f61_out1, z0, z1) → c21(F30_IN(z1))

Defined Rule Symbols:

f1_in, U1, f29_in, U2, f30_in, U3, f61_in, U4, f9_in, U5, f8_in, U6, U7, f26_in, U8, U9, f58_in, U10, U11

Defined Pair Symbols:

F58_IN, F1_IN, F9_IN, F8_IN, F26_IN, U8', F29_IN, F30_IN, F61_IN, U6', U10'

Compound Symbols:

c20, c1, c3, c6, c9, c15, c21, c1

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

F61_IN(.(z0, z1)) → c9(F61_IN(z1))

We considered the (Usable) Rules:

f29_in([]) → f29_out1
f29_in(.(z0, z1)) → U2(f29_in(z1), .(z0, z1))
U2(f29_out1, .(z0, z1)) → f29_out1
f9_in([]) → f9_out1
f9_in(.(=(z0, z1), z2)) → U5(f26_in(z0, z2), .(=(z0, z1), z2))
f26_in(z0, z1) → U8(f29_in(z0), z0, z1)
U5(f26_out1, .(=(z0, z1), z2)) → f9_out1
U8(f29_out1, z0, z1) → U9(f30_in(z1), z0, z1)
f30_in([]) → f30_out1
f30_in(.(=(z0, z1), z2)) → U3(f58_in(z0, z2), .(=(z0, z1), z2))
U9(f30_out1, z0, z1) → f26_out1
f58_in(z0, z1) → U10(f61_in(z0), z0, z1)
U3(f58_out1, .(=(z0, z1), z2)) → f30_out1
f61_in([]) → f61_out1
f61_in(.(z0, z1)) → U4(f61_in(z1), .(z0, z1))
U10(f61_out1, z0, z1) → U11(f30_in(z1), z0, z1)
U11(f30_out1, z0, z1) → f58_out1
U4(f61_out1, .(z0, z1)) → f61_out1

And the Tuples:

F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
F1_IN(z0, z1) → c1(F8_IN(z0, z1))
F9_IN(.(=(z0, z1), z2)) → c1(F26_IN(z0, z2))
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
F26_IN(z0, z1) → c1(U8'(f29_in(z0), z0, z1))
F26_IN(z0, z1) → c1(F29_IN(z0))
U8'(f29_out1, z0, z1) → c1(F30_IN(z1))
F29_IN(.(z0, z1)) → c3(F29_IN(z1))
F30_IN(.(=(z0, z1), z2)) → c6(F58_IN(z0, z2))
F61_IN(.(z0, z1)) → c9(F61_IN(z1))
U6'(f9_out1, z0, z1) → c15
U10'(f61_out1, z0, z1) → c21(F30_IN(z1))
F1_IN(z0, z1) → c1
F9_IN(.(=(z0, z1), z2)) → c1
U8'(f29_out1, z0, z1) → c1

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

POL(.(x₁, x₂)) = [1] + x₁ + x₂   
POL(=(x₁, x₂)) = x₁ + x₂   
POL(F1_IN(x₁, x₂)) = [2] + [3]x₁ + [2]x₂   
POL(F26_IN(x₁, x₂)) = [2] + [3]x₁ + [3]x₂   
POL(F29_IN(x₁)) = [1] + [2]x₁   
POL(F30_IN(x₁)) = [2]x₁   
POL(F58_IN(x₁, x₂)) = [2] + x₁ + [2]x₂   
POL(F61_IN(x₁)) = x₁   
POL(F8_IN(x₁, x₂)) = [1] + [3]x₁ + x₂   
POL(F9_IN(x₁)) = [1] + [3]x₁   
POL(U10(x₁, x₂, x₃)) = 0   
POL(U10'(x₁, x₂, x₃)) = [2]x₃   
POL(U11(x₁, x₂, x₃)) = 0   
POL(U2(x₁, x₂)) = 0   
POL(U3(x₁, x₂)) = x₁   
POL(U4(x₁, x₂)) = [3] + x₂   
POL(U5(x₁, x₂)) = [2] + [2]x₂   
POL(U6'(x₁, x₂, x₃)) = 0   
POL(U8(x₁, x₂, x₃)) = 0   
POL(U8'(x₁, x₂, x₃)) = [2] + [3]x₃   
POL(U9(x₁, x₂, x₃)) = 0   
POL([]) = [1]   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c15) = 0   
POL(c20(x₁, x₂)) = x₁ + x₂   
POL(c21(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c9(x₁)) = x₁   
POL(f26_in(x₁, x₂)) = 0   
POL(f26_out1) = 0   
POL(f29_in(x₁)) = 0   
POL(f29_out1) = 0   
POL(f30_in(x₁)) = [2]x₁   
POL(f30_out1) = 0   
POL(f58_in(x₁, x₂)) = x₂   
POL(f58_out1) = 0   
POL(f61_in(x₁)) = [2] + [2]x₁   
POL(f61_out1) = [2]   
POL(f9_in(x₁)) = [2] + [2]x₁   
POL(f9_out1) = [3]   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f8_in(z0, z1), z0, z1)
U1(f8_out1(z0, z1, z2, z3, z4, z5, z6, z7), z8, z9) → f1_out1(z6, z7)
f29_in([]) → f29_out1
f29_in(.(z0, z1)) → U2(f29_in(z1), .(z0, z1))
U2(f29_out1, .(z0, z1)) → f29_out1
f30_in([]) → f30_out1
f30_in(.(=(z0, z1), z2)) → U3(f58_in(z0, z2), .(=(z0, z1), z2))
U3(f58_out1, .(=(z0, z1), z2)) → f30_out1
f61_in([]) → f61_out1
f61_in(.(z0, z1)) → U4(f61_in(z1), .(z0, z1))
U4(f61_out1, .(z0, z1)) → f61_out1
f9_in([]) → f9_out1
f9_in(.(=(z0, z1), z2)) → U5(f26_in(z0, z2), .(=(z0, z1), z2))
U5(f26_out1, .(=(z0, z1), z2)) → f9_out1
f8_in(z0, z1) → U6(f9_in(z0), z0, z1)
U6(f9_out1, z0, z1) → U7(f11_in(z1, z0), z0, z1)
U7(f11_out1(z0, z1, z2, z3, z4, z5, z6, z7), z8, z9) → f8_out1(z0, z1, z2, z3, z4, z5, z6, z7)
f26_in(z0, z1) → U8(f29_in(z0), z0, z1)
U8(f29_out1, z0, z1) → U9(f30_in(z1), z0, z1)
U9(f30_out1, z0, z1) → f26_out1
f58_in(z0, z1) → U10(f61_in(z0), z0, z1)
U10(f61_out1, z0, z1) → U11(f30_in(z1), z0, z1)
U11(f30_out1, z0, z1) → f58_out1

Tuples:

F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
F1_IN(z0, z1) → c1(F8_IN(z0, z1))
F9_IN(.(=(z0, z1), z2)) → c1(F26_IN(z0, z2))
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
F26_IN(z0, z1) → c1(U8'(f29_in(z0), z0, z1))
F26_IN(z0, z1) → c1(F29_IN(z0))
U8'(f29_out1, z0, z1) → c1(F30_IN(z1))
F29_IN(.(z0, z1)) → c3(F29_IN(z1))
F30_IN(.(=(z0, z1), z2)) → c6(F58_IN(z0, z2))
F61_IN(.(z0, z1)) → c9(F61_IN(z1))
U6'(f9_out1, z0, z1) → c15
U10'(f61_out1, z0, z1) → c21(F30_IN(z1))
F1_IN(z0, z1) → c1
F9_IN(.(=(z0, z1), z2)) → c1
U8'(f29_out1, z0, z1) → c1

S tuples:none
K tuples:

F1_IN(z0, z1) → c1(F8_IN(z0, z1))
F8_IN(z0, z1) → c1(U6'(f9_in(z0), z0, z1))
F8_IN(z0, z1) → c1(F9_IN(z0))
U6'(f9_out1, z0, z1) → c15
F1_IN(z0, z1) → c1
F9_IN(.(=(z0, z1), z2)) → c1
F9_IN(.(=(z0, z1), z2)) → c1(F26_IN(z0, z2))
F26_IN(z0, z1) → c1(U8'(f29_in(z0), z0, z1))
F26_IN(z0, z1) → c1(F29_IN(z0))
U8'(f29_out1, z0, z1) → c1(F30_IN(z1))
U8'(f29_out1, z0, z1) → c1
F29_IN(.(z0, z1)) → c3(F29_IN(z1))
F58_IN(z0, z1) → c20(U10'(f61_in(z0), z0, z1), F61_IN(z0))
F30_IN(.(=(z0, z1), z2)) → c6(F58_IN(z0, z2))
U10'(f61_out1, z0, z1) → c21(F30_IN(z1))
F61_IN(.(z0, z1)) → c9(F61_IN(z1))

Defined Rule Symbols:

f1_in, U1, f29_in, U2, f30_in, U3, f61_in, U4, f9_in, U5, f8_in, U6, U7, f26_in, U8, U9, f58_in, U10, U11

Defined Pair Symbols:

F58_IN, F1_IN, F9_IN, F8_IN, F26_IN, U8', F29_IN, F30_IN, F61_IN, U6', U10'

Compound Symbols:

c20, c1, c3, c6, c9, c15, c21, c1

(17) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(18) BOUNDS(O(1), O(1))