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

(0) Obligation:

Clauses:

f(A, [], RES) :- g(A, [], RES).
f(.(A, As), .(B, Bs), RES) :- f(.(B, .(A, As)), Bs, RES).
g([], RES, RES).
g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES).

Query: f(g,g,a)

(1) LPReorderTransformerProof (EQUIVALENT transformation)

Reordered facts before rules in definite LP [PROLOG].

(2) Obligation:

Clauses:

g([], RES, RES).
f(A, [], RES) :- g(A, [], RES).
f(.(A, As), .(B, Bs), RES) :- f(.(B, .(A, As)), Bs, RES).
g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES).

Query: f(g,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];
2 [label="2: f(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: f(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | f(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: f(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: f(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: g(T12, [], T14)\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: g(T12, [], T14), SCOPE: 2, CLAUSE: 0 | g(T12, [], T14), SCOPE: 2, CLAUSE: 3\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: true | g([], [], T14), SCOPE: 2, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: g(T12, [], T14), SCOPE: 2, CLAUSE: 3\n\nT12 is ground\nX15 is free\ng(T12, [], T14) !=? g([], X15, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: g([], [], T14), SCOPE: 2, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: g(T22, .(T21, []), T24)\n\nT21 is ground\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: g(T22, .(T21, []), T24), SCOPE: 3, CLAUSE: 0 | g(T22, .(T21, []), T24), SCOPE: 3, CLAUSE: 3\n\nT21 is ground\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: true | g([], .(T29, []), T24), SCOPE: 3, CLAUSE: 3\n\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: g(T22, .(T21, []), T24), SCOPE: 3, CLAUSE: 3\n\nT21 is ground\nT22 is ground\nX36 is free\ng(T22, .(T21, []), T24) !=? g([], X36, X36)", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: g([], .(T29, []), T24), SCOPE: 3, CLAUSE: 3\n\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: g(T39, .(T38, .(T40, [])), T42)\n\nT38 is ground\nT39 is ground\nT40 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: g(T39, .(T38, .(T40, [])), T42), SCOPE: 4, CLAUSE: 0 | g(T39, .(T38, .(T40, [])), T42), SCOPE: 4, CLAUSE: 3\n\nT38 is ground\nT39 is ground\nT40 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: true | g([], .(T51, .(T52, [])), T42), SCOPE: 4, CLAUSE: 3\n\nT51 is ground\nT52 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: g(T39, .(T38, .(T40, [])), T42), SCOPE: 4, CLAUSE: 3\n\nT38 is ground\nT39 is ground\nT40 is ground\nX57 is free\ng(T39, .(T38, .(T40, [])), T42) !=? g([], X57, X57)", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: g([], .(T51, .(T52, [])), T42), SCOPE: 4, CLAUSE: 3\n\nT51 is ground\nT52 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: g(T64, .(T63, .(T65, .(T66, []))), T68)\n\nT63 is ground\nT64 is ground\nT65 is ground\nT66 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: g(T64, .(T63, .(T65, .(T66, []))), T68), SCOPE: 5, CLAUSE: 0 | g(T64, .(T63, .(T65, .(T66, []))), T68), SCOPE: 5, CLAUSE: 3\n\nT63 is ground\nT64 is ground\nT65 is ground\nT66 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: true | g([], .(T81, .(T82, .(T83, []))), T68), SCOPE: 5, CLAUSE: 3\n\nT81 is ground\nT82 is ground\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: g(T64, .(T63, .(T65, .(T66, []))), T68), SCOPE: 5, CLAUSE: 3\n\nT63 is ground\nT64 is ground\nT65 is ground\nT66 is ground\nX78 is free\ng(T64, .(T63, .(T65, .(T66, []))), T68) !=? g([], X78, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: g([], .(T81, .(T82, .(T83, []))), T68), SCOPE: 5, CLAUSE: 3\n\nT81 is ground\nT82 is ground\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: g(T97, .(T96, .(T98, .(T99, .(T100, [])))), T102)\n\nT96 is ground\nT97 is ground\nT98 is ground\nT99 is ground\nT100 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: g(T97, .(T96, .(T98, .(T99, .(T100, [])))), T102), SCOPE: 6, CLAUSE: 0 | g(T97, .(T96, .(T98, .(T99, .(T100, [])))), T102), SCOPE: 6, CLAUSE: 3\n\nT96 is ground\nT97 is ground\nT98 is ground\nT99 is ground\nT100 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: true | g([], .(T119, .(T120, .(T121, .(T122, [])))), T102), SCOPE: 6, CLAUSE: 3\n\nT119 is ground\nT120 is ground\nT121 is ground\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: g(T97, .(T96, .(T98, .(T99, .(T100, [])))), T102), SCOPE: 6, CLAUSE: 3\n\nT96 is ground\nT97 is ground\nT98 is ground\nT99 is ground\nT100 is ground\nX99 is free\ng(T97, .(T96, .(T98, .(T99, .(T100, [])))), T102) !=? g([], X99, X99)", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: g([], .(T119, .(T120, .(T121, .(T122, [])))), T102), SCOPE: 6, CLAUSE: 3\n\nT119 is ground\nT120 is ground\nT121 is ground\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: g(T138, .(T137, .(T139, .(T140, .(T141, .(T142, []))))), T144)\n\nT137 is ground\nT138 is ground\nT139 is ground\nT140 is ground\nT141 is ground\nT142 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: g(T138, .(T137, .(T139, .(T140, .(T141, .(T142, []))))), T144), SCOPE: 7, CLAUSE: 0 | g(T138, .(T137, .(T139, .(T140, .(T141, .(T142, []))))), T144), SCOPE: 7, CLAUSE: 3\n\nT137 is ground\nT138 is ground\nT139 is ground\nT140 is ground\nT141 is ground\nT142 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: true | g([], .(T165, .(T166, .(T167, .(T168, .(T169, []))))), T144), SCOPE: 7, CLAUSE: 3\n\nT165 is ground\nT166 is ground\nT167 is ground\nT168 is ground\nT169 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: g(T138, .(T137, .(T139, .(T140, .(T141, .(T142, []))))), T144), SCOPE: 7, CLAUSE: 3\n\nT137 is ground\nT138 is ground\nT139 is ground\nT140 is ground\nT141 is ground\nT142 is ground\nX120 is free\ng(T138, .(T137, .(T139, .(T140, .(T141, .(T142, []))))), T144) !=? g([], X120, X120)", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: g([], .(T165, .(T166, .(T167, .(T168, .(T169, []))))), T144), SCOPE: 7, CLAUSE: 3\n\nT165 is ground\nT166 is ground\nT167 is ground\nT168 is ground\nT169 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: g(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), T194)\n\nT186 is ground\nT187 is ground\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: g(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), T194), SCOPE: 8, CLAUSE: 0 | g(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), T194), SCOPE: 8, CLAUSE: 3\n\nT186 is ground\nT187 is ground\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: true | g([], .(T219, .(T220, .(T221, .(T222, .(T223, .(T224, [])))))), T194), SCOPE: 8, CLAUSE: 3\n\nT219 is ground\nT220 is ground\nT221 is ground\nT222 is ground\nT223 is ground\nT224 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: g(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), T194), SCOPE: 8, CLAUSE: 3\n\nT186 is ground\nT187 is ground\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nT192 is ground\nX141 is free\ng(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), T194) !=? g([], X141, X141)", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: g([], .(T219, .(T220, .(T221, .(T222, .(T223, .(T224, [])))))), T194), SCOPE: 8, CLAUSE: 3\n\nT219 is ground\nT220 is ground\nT221 is ground\nT222 is ground\nT223 is ground\nT224 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: g(T244, .(T243, .(T245, .(T246, .(T247, .(T248, .(T249, .(T250, []))))))), T252)\n\nT243 is ground\nT244 is ground\nT245 is ground\nT246 is ground\nT247 is ground\nT248 is ground\nT249 is ground\nT250 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: g(T244, .(T243, .(T245, .(T246, .(T247, .(T248, .(T249, .(T250, []))))))), T252), SCOPE: 9, CLAUSE: 0 | g(T244, .(T243, .(T245, .(T246, .(T247, .(T248, .(T249, .(T250, []))))))), T252), SCOPE: 9, CLAUSE: 3\n\nT243 is ground\nT244 is ground\nT245 is ground\nT246 is ground\nT247 is ground\nT248 is ground\nT249 is ground\nT250 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: true | g([], .(T281, .(T282, .(T283, .(T284, .(T285, .(T286, .(T287, []))))))), T252), SCOPE: 9, CLAUSE: 3\n\nT281 is ground\nT282 is ground\nT283 is ground\nT284 is ground\nT285 is ground\nT286 is ground\nT287 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: g(T244, .(T243, .(T245, .(T246, .(T247, .(T248, .(T249, .(T250, []))))))), T252), SCOPE: 9, CLAUSE: 3\n\nT243 is ground\nT244 is ground\nT245 is ground\nT246 is ground\nT247 is ground\nT248 is ground\nT249 is ground\nT250 is ground\nX162 is free\ng(T244, .(T243, .(T245, .(T246, .(T247, .(T248, .(T249, .(T250, []))))))), T252) !=? g([], X162, X162)", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: g([], .(T281, .(T282, .(T283, .(T284, .(T285, .(T286, .(T287, []))))))), T252), SCOPE: 9, CLAUSE: 3\n\nT281 is ground\nT282 is ground\nT283 is ground\nT284 is ground\nT285 is ground\nT286 is ground\nT287 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: g(T309, .(T308, .(T310, .(T311, .(T312, .(T313, .(T314, .(T315, .(T316, [])))))))), T318)\n\nT308 is ground\nT309 is ground\nT310 is ground\nT311 is ground\nT312 is ground\nT313 is ground\nT314 is ground\nT315 is ground\nT316 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: g(T309, .(T308, T335), T318)\n\nT308 is ground\nT309 is ground\nT335 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: g(T309, .(T308, T335), T318), SCOPE: 10, CLAUSE: 0 | g(T309, .(T308, T335), T318), SCOPE: 10, CLAUSE: 3\n\nT308 is ground\nT309 is ground\nT335 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: true | g([], .(T344, T345), T318), SCOPE: 10, CLAUSE: 3\n\nT344 is ground\nT345 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: g(T309, .(T308, T335), T318), SCOPE: 10, CLAUSE: 3\n\nT308 is ground\nT309 is ground\nT335 is ground\nX185 is free\ng(T309, .(T308, T335), T318) !=? g([], X185, X185)", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: g([], .(T344, T345), T318), SCOPE: 10, CLAUSE: 3\n\nT344 is ground\nT345 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: g(T357, .(T356, .(T358, T359)), T361)\n\nT356 is ground\nT357 is ground\nT358 is ground\nT359 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: f(.(T380, .(T378, T379)), T381, T383)\n\nT378 is ground\nT379 is ground\nT380 is ground\nT381 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 148 [arrowhead = none ];
148 -> 3;

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

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

151 [label="EVAL with clause\nf(X9, [], X10) :- g(X9, [], X10).\nand substitutionT1 -> T12,\nX9 -> T12,\nT2 -> [],\nT3 -> T14,\nX10 -> T14,\nT13 -> T14", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 151 [arrowhead = none ];
151 -> 9;

152 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 152 [arrowhead = none ];
152 -> 10;

153 [label="EVAL with clause\nf(.(X214, X215), .(X216, X217), X218) :- f(.(X216, .(X214, X215)), X217, X218).\nand substitutionX214 -> T378,\nX215 -> T379,\nT1 -> .(T378, T379),\nX216 -> T380,\nX217 -> T381,\nT2 -> .(T380, T381),\nT3 -> T383,\nX218 -> T383,\nT382 -> T383", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 153 [arrowhead = none ];
153 -> 145;

154 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 154 [arrowhead = none ];
154 -> 147;

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

156 [label="EVAL with clause\ng([], X15, X15).\nand substitutionT12 -> [],\nX15 -> [],\nT14 -> []", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 156 [arrowhead = none ];
156 -> 21;

157 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 157 [arrowhead = none ];
157 -> 22;

158 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 158 [arrowhead = none ];
158 -> 23;

159 [label="EVAL with clause\ng(.(X28, X29), X30, X31) :- g(X29, .(X28, X30), X31).\nand substitutionX28 -> T21,\nX29 -> T22,\nT12 -> .(T21, T22),\nX30 -> [],\nT14 -> T24,\nX31 -> T24,\nT23 -> T24", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 159 [arrowhead = none ];
159 -> 28;

160 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 160 [arrowhead = none ];
160 -> 29;

161 [label="BACKTRACK\nfor clause: g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 161 [arrowhead = none ];
161 -> 25;

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

163 [label="EVAL with clause\ng([], X36, X36).\nand substitutionT22 -> [],\nT21 -> T29,\nX36 -> .(T29, []),\nT24 -> .(T29, [])", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 163 [arrowhead = none ];
163 -> 35;

164 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
34 -> 164 [arrowhead = none ];
164 -> 36;

165 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 165 [arrowhead = none ];
165 -> 37;

166 [label="EVAL with clause\ng(.(X49, X50), X51, X52) :- g(X50, .(X49, X51), X52).\nand substitutionX49 -> T38,\nX50 -> T39,\nT22 -> .(T38, T39),\nT21 -> T40,\nX51 -> .(T40, []),\nT24 -> T42,\nX52 -> T42,\nT41 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 166 [arrowhead = none ];
166 -> 41;

167 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 167 [arrowhead = none ];
167 -> 42;

168 [label="BACKTRACK\nfor clause: g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 168 [arrowhead = none ];
168 -> 38;

169 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
41 -> 169 [arrowhead = none ];
169 -> 44;

170 [label="EVAL with clause\ng([], X57, X57).\nand substitutionT39 -> [],\nT38 -> T51,\nT40 -> T52,\nX57 -> .(T51, .(T52, [])),\nT42 -> .(T51, .(T52, []))", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 170 [arrowhead = none ];
170 -> 46;

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

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

173 [label="EVAL with clause\ng(.(X70, X71), X72, X73) :- g(X71, .(X70, X72), X73).\nand substitutionX70 -> T63,\nX71 -> T64,\nT39 -> .(T63, T64),\nT38 -> T65,\nT40 -> T66,\nX72 -> .(T65, .(T66, [])),\nT42 -> T68,\nX73 -> T68,\nT67 -> T68", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 173 [arrowhead = none ];
173 -> 53;

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

175 [label="BACKTRACK\nfor clause: g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
50 -> 175 [arrowhead = none ];
175 -> 52;

176 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
53 -> 176 [arrowhead = none ];
176 -> 57;

177 [label="EVAL with clause\ng([], X78, X78).\nand substitutionT64 -> [],\nT63 -> T81,\nT65 -> T82,\nT66 -> T83,\nX78 -> .(T81, .(T82, .(T83, []))),\nT68 -> .(T81, .(T82, .(T83, [])))", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 177 [arrowhead = none ];
177 -> 59;

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

179 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 179 [arrowhead = none ];
179 -> 62;

180 [label="EVAL with clause\ng(.(X91, X92), X93, X94) :- g(X92, .(X91, X93), X94).\nand substitutionX91 -> T96,\nX92 -> T97,\nT64 -> .(T96, T97),\nT63 -> T98,\nT65 -> T99,\nT66 -> T100,\nX93 -> .(T98, .(T99, .(T100, []))),\nT68 -> T102,\nX94 -> T102,\nT101 -> T102", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 180 [arrowhead = none ];
180 -> 67;

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

182 [label="BACKTRACK\nfor clause: g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 182 [arrowhead = none ];
182 -> 64;

183 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
67 -> 183 [arrowhead = none ];
183 -> 71;

184 [label="EVAL with clause\ng([], X99, X99).\nand substitutionT97 -> [],\nT96 -> T119,\nT98 -> T120,\nT99 -> T121,\nT100 -> T122,\nX99 -> .(T119, .(T120, .(T121, .(T122, [])))),\nT102 -> .(T119, .(T120, .(T121, .(T122, []))))", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 184 [arrowhead = none ];
184 -> 73;

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

186 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
73 -> 186 [arrowhead = none ];
186 -> 75;

187 [label="EVAL with clause\ng(.(X112, X113), X114, X115) :- g(X113, .(X112, X114), X115).\nand substitutionX112 -> T137,\nX113 -> T138,\nT97 -> .(T137, T138),\nT96 -> T139,\nT98 -> T140,\nT99 -> T141,\nT100 -> T142,\nX114 -> .(T139, .(T140, .(T141, .(T142, [])))),\nT102 -> T144,\nX115 -> T144,\nT143 -> T144", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 187 [arrowhead = none ];
187 -> 81;

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

189 [label="BACKTRACK\nfor clause: g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
75 -> 189 [arrowhead = none ];
189 -> 77;

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

191 [label="EVAL with clause\ng([], X120, X120).\nand substitutionT138 -> [],\nT137 -> T165,\nT139 -> T166,\nT140 -> T167,\nT141 -> T168,\nT142 -> T169,\nX120 -> .(T165, .(T166, .(T167, .(T168, .(T169, []))))),\nT144 -> .(T165, .(T166, .(T167, .(T168, .(T169, [])))))", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 191 [arrowhead = none ];
191 -> 87;

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

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

194 [label="EVAL with clause\ng(.(X133, X134), X135, X136) :- g(X134, .(X133, X135), X136).\nand substitutionX133 -> T186,\nX134 -> T187,\nT138 -> .(T186, T187),\nT137 -> T188,\nT139 -> T189,\nT140 -> T190,\nT141 -> T191,\nT142 -> T192,\nX135 -> .(T188, .(T189, .(T190, .(T191, .(T192, []))))),\nT144 -> T194,\nX136 -> T194,\nT193 -> T194", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 194 [arrowhead = none ];
194 -> 95;

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

196 [label="BACKTRACK\nfor clause: g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
89 -> 196 [arrowhead = none ];
196 -> 91;

197 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
95 -> 197 [arrowhead = none ];
197 -> 99;

198 [label="EVAL with clause\ng([], X141, X141).\nand substitutionT187 -> [],\nT186 -> T219,\nT188 -> T220,\nT189 -> T221,\nT190 -> T222,\nT191 -> T223,\nT192 -> T224,\nX141 -> .(T219, .(T220, .(T221, .(T222, .(T223, .(T224, [])))))),\nT194 -> .(T219, .(T220, .(T221, .(T222, .(T223, .(T224, []))))))", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 198 [arrowhead = none ];
198 -> 101;

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

200 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 200 [arrowhead = none ];
200 -> 103;

201 [label="EVAL with clause\ng(.(X154, X155), X156, X157) :- g(X155, .(X154, X156), X157).\nand substitutionX154 -> T243,\nX155 -> T244,\nT187 -> .(T243, T244),\nT186 -> T245,\nT188 -> T246,\nT189 -> T247,\nT190 -> T248,\nT191 -> T249,\nT192 -> T250,\nX156 -> .(T245, .(T246, .(T247, .(T248, .(T249, .(T250, [])))))),\nT194 -> T252,\nX157 -> T252,\nT251 -> T252", fontsize=14, style = filled, fillcolor = lightblue];
102 -> 201 [arrowhead = none ];
201 -> 109;

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

203 [label="BACKTRACK\nfor clause: g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
103 -> 203 [arrowhead = none ];
203 -> 104;

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

205 [label="EVAL with clause\ng([], X162, X162).\nand substitutionT244 -> [],\nT243 -> T281,\nT245 -> T282,\nT246 -> T283,\nT247 -> T284,\nT248 -> T285,\nT249 -> T286,\nT250 -> T287,\nX162 -> .(T281, .(T282, .(T283, .(T284, .(T285, .(T286, .(T287, []))))))),\nT252 -> .(T281, .(T282, .(T283, .(T284, .(T285, .(T286, .(T287, [])))))))", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 205 [arrowhead = none ];
205 -> 115;

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

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

208 [label="EVAL with clause\ng(.(X175, X176), X177, X178) :- g(X176, .(X175, X177), X178).\nand substitutionX175 -> T308,\nX176 -> T309,\nT244 -> .(T308, T309),\nT243 -> T310,\nT245 -> T311,\nT246 -> T312,\nT247 -> T313,\nT248 -> T314,\nT249 -> T315,\nT250 -> T316,\nX177 -> .(T310, .(T311, .(T312, .(T313, .(T314, .(T315, .(T316, []))))))),\nT252 -> T318,\nX178 -> T318,\nT317 -> T318", fontsize=14, style = filled, fillcolor = lightblue];
116 -> 208 [arrowhead = none ];
208 -> 123;

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

210 [label="BACKTRACK\nfor clause: g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
117 -> 210 [arrowhead = none ];
210 -> 118;

211 [label="GENERALIZATION\nT335 <-- .(T310, .(T311, .(T312, .(T313, .(T314, .(T315, .(T316, [])))))))\n\nNew Knowledge:\nT335 is ground", fontsize=14, style = filled, fillcolor = violet];
123 -> 211 [arrowhead = none ];
211 -> 127;

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

213 [label="EVAL with clause\ng([], X185, X185).\nand substitutionT309 -> [],\nT308 -> T344,\nT335 -> T345,\nX185 -> .(T344, T345),\nT318 -> .(T344, T345)", fontsize=14, style = filled, fillcolor = lightblue];
130 -> 213 [arrowhead = none ];
213 -> 132;

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

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

216 [label="EVAL with clause\ng(.(X198, X199), X200, X201) :- g(X199, .(X198, X200), X201).\nand substitutionX198 -> T356,\nX199 -> T357,\nT309 -> .(T356, T357),\nT308 -> T358,\nT335 -> T359,\nX200 -> .(T358, T359),\nT318 -> T361,\nX201 -> T361,\nT360 -> T361", fontsize=14, style = filled, fillcolor = lightblue];
135 -> 216 [arrowhead = none ];
216 -> 141;

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

218 [label="BACKTRACK\nfor clause: g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
136 -> 218 [arrowhead = none ];
218 -> 138;

219 [label="INSTANCE with matching:\nT309 -> T357\nT308 -> T356\nT335 -> .(T358, T359)\nT318 -> T361", fontsize=14, style = filled, fillcolor = lightgrey];
141 -> 219 [arrowhead = none , style=dashed];
219 -> 127[style=dashed];

220 [label="INSTANCE with matching:\nT1 -> .(T380, .(T378, T379))\nT2 -> T381\nT3 -> T383", fontsize=14, style = filled, fillcolor = lightgrey];
145 -> 220 [arrowhead = none , style=dashed];
220 -> 2[style=dashed];

}

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, z1) → U1(f3_in(z0, z1), z0, z1)
U1(f3_out1(z0), z1, z2) → f2_out1(z0)
U1(f3_out2(z0), z1, z2) → f2_out1(z0)
f127_in([], z0, z1) → f127_out1(.(z0, z1))
f127_in(.(z0, z1), z2, z3) → U2(f127_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f127_out1(z0), .(z1, z2), z3, z4) → f127_out1(z0)
f5_in([], []) → f5_out1([])
f5_in(.(z0, []), []) → f5_out1(.(z0, []))
f5_in(.(z0, .(z1, [])), []) → f5_out1(.(z1, .(z0, [])))
f5_in(.(z0, .(z1, .(z2, []))), []) → f5_out1(.(z2, .(z1, .(z0, []))))
f5_in(.(z0, .(z1, .(z2, .(z3, [])))), []) → f5_out1(.(z3, .(z2, .(z1, .(z0, [])))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, []))))), []) → f5_out1(.(z4, .(z3, .(z2, .(z1, .(z0, []))))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, [])))))), []) → f5_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, []))))))), []) → f5_out1(.(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → U3(f127_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), [])
U3(f127_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9)))))))), []) → f5_out1(z0)
f6_in(.(z0, z1), .(z2, z3)) → U4(f2_in(.(z2, .(z0, z1)), z3), .(z0, z1), .(z2, z3))
U4(f2_out1(z0), .(z1, z2), .(z3, z4)) → f6_out1(z0)
f3_in(z0, z1) → U5(f5_in(z0, z1), f6_in(z0, z1), z0, z1)
U5(f5_out1(z0), z1, z2, z3) → f3_out1(z0)
U5(z0, f6_out1(z1), z2, z3) → f3_out2(z1)

Tuples:

F2_IN(z0, z1) → c(U1'(f3_in(z0, z1), z0, z1), F3_IN(z0, z1))
F127_IN(.(z0, z1), z2, z3) → c4(U2'(f127_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F127_IN(z1, z0, .(z2, z3)))
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c14(U3'(f127_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []), F127_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F6_IN(.(z0, z1), .(z2, z3)) → c16(U4'(f2_in(.(z2, .(z0, z1)), z3), .(z0, z1), .(z2, z3)), F2_IN(.(z2, .(z0, z1)), z3))
F3_IN(z0, z1) → c18(U5'(f5_in(z0, z1), f6_in(z0, z1), z0, z1), F5_IN(z0, z1), F6_IN(z0, z1))

S tuples:

F2_IN(z0, z1) → c(U1'(f3_in(z0, z1), z0, z1), F3_IN(z0, z1))
F127_IN(.(z0, z1), z2, z3) → c4(U2'(f127_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F127_IN(z1, z0, .(z2, z3)))
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c14(U3'(f127_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []), F127_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F6_IN(.(z0, z1), .(z2, z3)) → c16(U4'(f2_in(.(z2, .(z0, z1)), z3), .(z0, z1), .(z2, z3)), F2_IN(.(z2, .(z0, z1)), z3))
F3_IN(z0, z1) → c18(U5'(f5_in(z0, z1), f6_in(z0, z1), z0, z1), F5_IN(z0, z1), F6_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f127_in, U2, f5_in, U3, f6_in, U4, f3_in, U5

Defined Pair Symbols:

F2_IN, F127_IN, F5_IN, F6_IN, F3_IN

Compound Symbols:

c, c4, c14, c16, c18

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

Split RHS of tuples not part of any SCC

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, z1) → U1(f3_in(z0, z1), z0, z1)
U1(f3_out1(z0), z1, z2) → f2_out1(z0)
U1(f3_out2(z0), z1, z2) → f2_out1(z0)
f127_in([], z0, z1) → f127_out1(.(z0, z1))
f127_in(.(z0, z1), z2, z3) → U2(f127_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f127_out1(z0), .(z1, z2), z3, z4) → f127_out1(z0)
f5_in([], []) → f5_out1([])
f5_in(.(z0, []), []) → f5_out1(.(z0, []))
f5_in(.(z0, .(z1, [])), []) → f5_out1(.(z1, .(z0, [])))
f5_in(.(z0, .(z1, .(z2, []))), []) → f5_out1(.(z2, .(z1, .(z0, []))))
f5_in(.(z0, .(z1, .(z2, .(z3, [])))), []) → f5_out1(.(z3, .(z2, .(z1, .(z0, [])))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, []))))), []) → f5_out1(.(z4, .(z3, .(z2, .(z1, .(z0, []))))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, [])))))), []) → f5_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, []))))))), []) → f5_out1(.(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → U3(f127_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), [])
U3(f127_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9)))))))), []) → f5_out1(z0)
f6_in(.(z0, z1), .(z2, z3)) → U4(f2_in(.(z2, .(z0, z1)), z3), .(z0, z1), .(z2, z3))
U4(f2_out1(z0), .(z1, z2), .(z3, z4)) → f6_out1(z0)
f3_in(z0, z1) → U5(f5_in(z0, z1), f6_in(z0, z1), z0, z1)
U5(f5_out1(z0), z1, z2, z3) → f3_out1(z0)
U5(z0, f6_out1(z1), z2, z3) → f3_out2(z1)

Tuples:

F2_IN(z0, z1) → c(U1'(f3_in(z0, z1), z0, z1), F3_IN(z0, z1))
F127_IN(.(z0, z1), z2, z3) → c4(U2'(f127_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F127_IN(z1, z0, .(z2, z3)))
F6_IN(.(z0, z1), .(z2, z3)) → c16(U4'(f2_in(.(z2, .(z0, z1)), z3), .(z0, z1), .(z2, z3)), F2_IN(.(z2, .(z0, z1)), z3))
F3_IN(z0, z1) → c18(U5'(f5_in(z0, z1), f6_in(z0, z1), z0, z1), F5_IN(z0, z1), F6_IN(z0, z1))
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1(U3'(f127_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []))
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1(F127_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))

S tuples:

F2_IN(z0, z1) → c(U1'(f3_in(z0, z1), z0, z1), F3_IN(z0, z1))
F127_IN(.(z0, z1), z2, z3) → c4(U2'(f127_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F127_IN(z1, z0, .(z2, z3)))
F6_IN(.(z0, z1), .(z2, z3)) → c16(U4'(f2_in(.(z2, .(z0, z1)), z3), .(z0, z1), .(z2, z3)), F2_IN(.(z2, .(z0, z1)), z3))
F3_IN(z0, z1) → c18(U5'(f5_in(z0, z1), f6_in(z0, z1), z0, z1), F5_IN(z0, z1), F6_IN(z0, z1))
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1(U3'(f127_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []))
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1(F127_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f127_in, U2, f5_in, U3, f6_in, U4, f3_in, U5

Defined Pair Symbols:

F2_IN, F127_IN, F6_IN, F3_IN, F5_IN

Compound Symbols:

c, c4, c16, c18, c1

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

Removed 5 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, z1) → U1(f3_in(z0, z1), z0, z1)
U1(f3_out1(z0), z1, z2) → f2_out1(z0)
U1(f3_out2(z0), z1, z2) → f2_out1(z0)
f127_in([], z0, z1) → f127_out1(.(z0, z1))
f127_in(.(z0, z1), z2, z3) → U2(f127_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f127_out1(z0), .(z1, z2), z3, z4) → f127_out1(z0)
f5_in([], []) → f5_out1([])
f5_in(.(z0, []), []) → f5_out1(.(z0, []))
f5_in(.(z0, .(z1, [])), []) → f5_out1(.(z1, .(z0, [])))
f5_in(.(z0, .(z1, .(z2, []))), []) → f5_out1(.(z2, .(z1, .(z0, []))))
f5_in(.(z0, .(z1, .(z2, .(z3, [])))), []) → f5_out1(.(z3, .(z2, .(z1, .(z0, [])))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, []))))), []) → f5_out1(.(z4, .(z3, .(z2, .(z1, .(z0, []))))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, [])))))), []) → f5_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, []))))))), []) → f5_out1(.(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → U3(f127_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), [])
U3(f127_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9)))))))), []) → f5_out1(z0)
f6_in(.(z0, z1), .(z2, z3)) → U4(f2_in(.(z2, .(z0, z1)), z3), .(z0, z1), .(z2, z3))
U4(f2_out1(z0), .(z1, z2), .(z3, z4)) → f6_out1(z0)
f3_in(z0, z1) → U5(f5_in(z0, z1), f6_in(z0, z1), z0, z1)
U5(f5_out1(z0), z1, z2, z3) → f3_out1(z0)
U5(z0, f6_out1(z1), z2, z3) → f3_out2(z1)

Tuples:

F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1(F127_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F2_IN(z0, z1) → c(F3_IN(z0, z1))
F127_IN(.(z0, z1), z2, z3) → c4(F127_IN(z1, z0, .(z2, z3)))
F6_IN(.(z0, z1), .(z2, z3)) → c16(F2_IN(.(z2, .(z0, z1)), z3))
F3_IN(z0, z1) → c18(F5_IN(z0, z1), F6_IN(z0, z1))
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1

S tuples:

F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1(F127_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F2_IN(z0, z1) → c(F3_IN(z0, z1))
F127_IN(.(z0, z1), z2, z3) → c4(F127_IN(z1, z0, .(z2, z3)))
F6_IN(.(z0, z1), .(z2, z3)) → c16(F2_IN(.(z2, .(z0, z1)), z3))
F3_IN(z0, z1) → c18(F5_IN(z0, z1), F6_IN(z0, z1))
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1

K tuples:none
Defined Rule Symbols:

f2_in, U1, f127_in, U2, f5_in, U3, f6_in, U4, f3_in, U5

Defined Pair Symbols:

F5_IN, F2_IN, F127_IN, F6_IN, F3_IN

Compound Symbols:

c1, c, c4, c16, c18, 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.

F2_IN(z0, z1) → c(F3_IN(z0, z1))
F6_IN(.(z0, z1), .(z2, z3)) → c16(F2_IN(.(z2, .(z0, z1)), z3))

We considered the (Usable) Rules:none
And the Tuples:

F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1(F127_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F2_IN(z0, z1) → c(F3_IN(z0, z1))
F127_IN(.(z0, z1), z2, z3) → c4(F127_IN(z1, z0, .(z2, z3)))
F6_IN(.(z0, z1), .(z2, z3)) → c16(F2_IN(.(z2, .(z0, z1)), z3))
F3_IN(z0, z1) → c18(F5_IN(z0, z1), F6_IN(z0, z1))
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1

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

POL(.(x₁, x₂)) = [2] + x₂   
POL(F127_IN(x₁, x₂, x₃)) = 0   
POL(F2_IN(x₁, x₂)) = [1] + x₂   
POL(F3_IN(x₁, x₂)) = x₂   
POL(F5_IN(x₁, x₂)) = 0   
POL(F6_IN(x₁, x₂)) = x₂   
POL([]) = 0   
POL(c(x₁)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c16(x₁)) = x₁   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, z1) → U1(f3_in(z0, z1), z0, z1)
U1(f3_out1(z0), z1, z2) → f2_out1(z0)
U1(f3_out2(z0), z1, z2) → f2_out1(z0)
f127_in([], z0, z1) → f127_out1(.(z0, z1))
f127_in(.(z0, z1), z2, z3) → U2(f127_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f127_out1(z0), .(z1, z2), z3, z4) → f127_out1(z0)
f5_in([], []) → f5_out1([])
f5_in(.(z0, []), []) → f5_out1(.(z0, []))
f5_in(.(z0, .(z1, [])), []) → f5_out1(.(z1, .(z0, [])))
f5_in(.(z0, .(z1, .(z2, []))), []) → f5_out1(.(z2, .(z1, .(z0, []))))
f5_in(.(z0, .(z1, .(z2, .(z3, [])))), []) → f5_out1(.(z3, .(z2, .(z1, .(z0, [])))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, []))))), []) → f5_out1(.(z4, .(z3, .(z2, .(z1, .(z0, []))))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, [])))))), []) → f5_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, []))))))), []) → f5_out1(.(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → U3(f127_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), [])
U3(f127_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9)))))))), []) → f5_out1(z0)
f6_in(.(z0, z1), .(z2, z3)) → U4(f2_in(.(z2, .(z0, z1)), z3), .(z0, z1), .(z2, z3))
U4(f2_out1(z0), .(z1, z2), .(z3, z4)) → f6_out1(z0)
f3_in(z0, z1) → U5(f5_in(z0, z1), f6_in(z0, z1), z0, z1)
U5(f5_out1(z0), z1, z2, z3) → f3_out1(z0)
U5(z0, f6_out1(z1), z2, z3) → f3_out2(z1)

Tuples:

F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1(F127_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F2_IN(z0, z1) → c(F3_IN(z0, z1))
F127_IN(.(z0, z1), z2, z3) → c4(F127_IN(z1, z0, .(z2, z3)))
F6_IN(.(z0, z1), .(z2, z3)) → c16(F2_IN(.(z2, .(z0, z1)), z3))
F3_IN(z0, z1) → c18(F5_IN(z0, z1), F6_IN(z0, z1))
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1

S tuples:

F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1(F127_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F127_IN(.(z0, z1), z2, z3) → c4(F127_IN(z1, z0, .(z2, z3)))
F3_IN(z0, z1) → c18(F5_IN(z0, z1), F6_IN(z0, z1))
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1

K tuples:

F2_IN(z0, z1) → c(F3_IN(z0, z1))
F6_IN(.(z0, z1), .(z2, z3)) → c16(F2_IN(.(z2, .(z0, z1)), z3))

Defined Rule Symbols:

f2_in, U1, f127_in, U2, f5_in, U3, f6_in, U4, f3_in, U5

Defined Pair Symbols:

F5_IN, F2_IN, F127_IN, F6_IN, F3_IN

Compound Symbols:

c1, c, c4, c16, c18, c1

(11) CdtKnowledgeProof (EQUIVALENT transformation)

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

F3_IN(z0, z1) → c18(F5_IN(z0, z1), F6_IN(z0, z1))
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1(F127_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F6_IN(.(z0, z1), .(z2, z3)) → c16(F2_IN(.(z2, .(z0, z1)), z3))
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, z1) → U1(f3_in(z0, z1), z0, z1)
U1(f3_out1(z0), z1, z2) → f2_out1(z0)
U1(f3_out2(z0), z1, z2) → f2_out1(z0)
f127_in([], z0, z1) → f127_out1(.(z0, z1))
f127_in(.(z0, z1), z2, z3) → U2(f127_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f127_out1(z0), .(z1, z2), z3, z4) → f127_out1(z0)
f5_in([], []) → f5_out1([])
f5_in(.(z0, []), []) → f5_out1(.(z0, []))
f5_in(.(z0, .(z1, [])), []) → f5_out1(.(z1, .(z0, [])))
f5_in(.(z0, .(z1, .(z2, []))), []) → f5_out1(.(z2, .(z1, .(z0, []))))
f5_in(.(z0, .(z1, .(z2, .(z3, [])))), []) → f5_out1(.(z3, .(z2, .(z1, .(z0, [])))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, []))))), []) → f5_out1(.(z4, .(z3, .(z2, .(z1, .(z0, []))))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, [])))))), []) → f5_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, []))))))), []) → f5_out1(.(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → U3(f127_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), [])
U3(f127_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9)))))))), []) → f5_out1(z0)
f6_in(.(z0, z1), .(z2, z3)) → U4(f2_in(.(z2, .(z0, z1)), z3), .(z0, z1), .(z2, z3))
U4(f2_out1(z0), .(z1, z2), .(z3, z4)) → f6_out1(z0)
f3_in(z0, z1) → U5(f5_in(z0, z1), f6_in(z0, z1), z0, z1)
U5(f5_out1(z0), z1, z2, z3) → f3_out1(z0)
U5(z0, f6_out1(z1), z2, z3) → f3_out2(z1)

Tuples:

F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1(F127_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F2_IN(z0, z1) → c(F3_IN(z0, z1))
F127_IN(.(z0, z1), z2, z3) → c4(F127_IN(z1, z0, .(z2, z3)))
F6_IN(.(z0, z1), .(z2, z3)) → c16(F2_IN(.(z2, .(z0, z1)), z3))
F3_IN(z0, z1) → c18(F5_IN(z0, z1), F6_IN(z0, z1))
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1

S tuples:

F127_IN(.(z0, z1), z2, z3) → c4(F127_IN(z1, z0, .(z2, z3)))

K tuples:

F2_IN(z0, z1) → c(F3_IN(z0, z1))
F6_IN(.(z0, z1), .(z2, z3)) → c16(F2_IN(.(z2, .(z0, z1)), z3))
F3_IN(z0, z1) → c18(F5_IN(z0, z1), F6_IN(z0, z1))
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1(F127_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))

Defined Rule Symbols:

f2_in, U1, f127_in, U2, f5_in, U3, f6_in, U4, f3_in, U5

Defined Pair Symbols:

F5_IN, F2_IN, F127_IN, F6_IN, F3_IN

Compound Symbols:

c1, c, c4, c16, c18, c1

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

F127_IN(.(z0, z1), z2, z3) → c4(F127_IN(z1, z0, .(z2, z3)))

We considered the (Usable) Rules:none
And the Tuples:

F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1(F127_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F2_IN(z0, z1) → c(F3_IN(z0, z1))
F127_IN(.(z0, z1), z2, z3) → c4(F127_IN(z1, z0, .(z2, z3)))
F6_IN(.(z0, z1), .(z2, z3)) → c16(F2_IN(.(z2, .(z0, z1)), z3))
F3_IN(z0, z1) → c18(F5_IN(z0, z1), F6_IN(z0, z1))
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1

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

POL(.(x₁, x₂)) = [1] + x₂   
POL(F127_IN(x₁, x₂, x₃)) = x₁   
POL(F2_IN(x₁, x₂)) = x₁ + x₂ + x₂² + x₁·x₂   
POL(F3_IN(x₁, x₂)) = x₁ + x₂ + x₂² + x₁·x₂   
POL(F5_IN(x₁, x₂)) = x₁   
POL(F6_IN(x₁, x₂)) = x₂ + x₂² + x₁·x₂   
POL([]) = 0   
POL(c(x₁)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c16(x₁)) = x₁   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, z1) → U1(f3_in(z0, z1), z0, z1)
U1(f3_out1(z0), z1, z2) → f2_out1(z0)
U1(f3_out2(z0), z1, z2) → f2_out1(z0)
f127_in([], z0, z1) → f127_out1(.(z0, z1))
f127_in(.(z0, z1), z2, z3) → U2(f127_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f127_out1(z0), .(z1, z2), z3, z4) → f127_out1(z0)
f5_in([], []) → f5_out1([])
f5_in(.(z0, []), []) → f5_out1(.(z0, []))
f5_in(.(z0, .(z1, [])), []) → f5_out1(.(z1, .(z0, [])))
f5_in(.(z0, .(z1, .(z2, []))), []) → f5_out1(.(z2, .(z1, .(z0, []))))
f5_in(.(z0, .(z1, .(z2, .(z3, [])))), []) → f5_out1(.(z3, .(z2, .(z1, .(z0, [])))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, []))))), []) → f5_out1(.(z4, .(z3, .(z2, .(z1, .(z0, []))))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, [])))))), []) → f5_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, []))))))), []) → f5_out1(.(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))))
f5_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → U3(f127_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), [])
U3(f127_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9)))))))), []) → f5_out1(z0)
f6_in(.(z0, z1), .(z2, z3)) → U4(f2_in(.(z2, .(z0, z1)), z3), .(z0, z1), .(z2, z3))
U4(f2_out1(z0), .(z1, z2), .(z3, z4)) → f6_out1(z0)
f3_in(z0, z1) → U5(f5_in(z0, z1), f6_in(z0, z1), z0, z1)
U5(f5_out1(z0), z1, z2, z3) → f3_out1(z0)
U5(z0, f6_out1(z1), z2, z3) → f3_out2(z1)

Tuples:

F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1(F127_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F2_IN(z0, z1) → c(F3_IN(z0, z1))
F127_IN(.(z0, z1), z2, z3) → c4(F127_IN(z1, z0, .(z2, z3)))
F6_IN(.(z0, z1), .(z2, z3)) → c16(F2_IN(.(z2, .(z0, z1)), z3))
F3_IN(z0, z1) → c18(F5_IN(z0, z1), F6_IN(z0, z1))
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1

S tuples:none
K tuples:

F2_IN(z0, z1) → c(F3_IN(z0, z1))
F6_IN(.(z0, z1), .(z2, z3)) → c16(F2_IN(.(z2, .(z0, z1)), z3))
F3_IN(z0, z1) → c18(F5_IN(z0, z1), F6_IN(z0, z1))
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1
F5_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), []) → c1(F127_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F127_IN(.(z0, z1), z2, z3) → c4(F127_IN(z1, z0, .(z2, z3)))

Defined Rule Symbols:

f2_in, U1, f127_in, U2, f5_in, U3, f6_in, U4, f3_in, U5

Defined Pair Symbols:

F5_IN, F2_IN, F127_IN, F6_IN, F3_IN

Compound Symbols:

c1, c, c4, c16, c18, c1

(15) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(16) BOUNDS(O(1), O(1))

(17) 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: f(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: f(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | f(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: g(T6, [], T8) | f(T6, [], T3), SCOPE: 1, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: f(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nX3 is free\nX4 is free\nf(T1, T2, T3) !=? f(X3, [], X4)", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: g(T6, [], T8), SCOPE: 2, CLAUSE: 0 | g(T6, [], T8), SCOPE: 2, CLAUSE: 3 | ?_2 | f(T6, [], T3), SCOPE: 1, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: true | g([], [], T8), SCOPE: 2, CLAUSE: 3 | ?_2 | f([], [], T3), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: g(T6, [], T8), SCOPE: 2, CLAUSE: 3 | ?_2 | f(T6, [], T3), SCOPE: 1, CLAUSE: 2\n\nT6 is ground\nX7 is free\ng(T6, [], T8) !=? g([], X7, X7)", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: g([], [], T8), SCOPE: 2, CLAUSE: 3 | ?_2 | f([], [], T3), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ?_2 | f([], [], T3), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: f([], [], T3), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: g(T6, [], T8), SCOPE: 2, CLAUSE: 3\n\nT6 is ground\nX7 is free\ng(T6, [], T8) !=? g([], X7, X7)", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ?_2 | f(T6, [], T3), SCOPE: 1, CLAUSE: 2\n\nT6 is ground\nX7 is free\ng(T6, [], T8) !=? g([], X7, X7)", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: g(T22, .(T21, []), T24)\n\nT21 is ground\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: g(T22, .(T21, []), T24), SCOPE: 3, CLAUSE: 0 | g(T22, .(T21, []), T24), SCOPE: 3, CLAUSE: 3\n\nT21 is ground\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: true | g([], .(T29, []), T24), SCOPE: 3, CLAUSE: 3\n\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: g(T22, .(T21, []), T24), SCOPE: 3, CLAUSE: 3\n\nT21 is ground\nT22 is ground\nX41 is free\ng(T22, .(T21, []), T24) !=? g([], X41, X41)", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: g([], .(T29, []), T24), SCOPE: 3, CLAUSE: 3\n\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: g(T39, .(T38, .(T40, [])), T42)\n\nT38 is ground\nT39 is ground\nT40 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: g(T39, .(T38, .(T40, [])), T42), SCOPE: 4, CLAUSE: 0 | g(T39, .(T38, .(T40, [])), T42), SCOPE: 4, CLAUSE: 3\n\nT38 is ground\nT39 is ground\nT40 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: true | g([], .(T51, .(T52, [])), T42), SCOPE: 4, CLAUSE: 3\n\nT51 is ground\nT52 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: g(T39, .(T38, .(T40, [])), T42), SCOPE: 4, CLAUSE: 3\n\nT38 is ground\nT39 is ground\nT40 is ground\nX62 is free\ng(T39, .(T38, .(T40, [])), T42) !=? g([], X62, X62)", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: g([], .(T51, .(T52, [])), T42), SCOPE: 4, CLAUSE: 3\n\nT51 is ground\nT52 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: g(T64, .(T63, .(T65, .(T66, []))), T68)\n\nT63 is ground\nT64 is ground\nT65 is ground\nT66 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: g(T64, .(T63, .(T65, .(T66, []))), T68), SCOPE: 5, CLAUSE: 0 | g(T64, .(T63, .(T65, .(T66, []))), T68), SCOPE: 5, CLAUSE: 3\n\nT63 is ground\nT64 is ground\nT65 is ground\nT66 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: true | g([], .(T81, .(T82, .(T83, []))), T68), SCOPE: 5, CLAUSE: 3\n\nT81 is ground\nT82 is ground\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: g(T64, .(T63, .(T65, .(T66, []))), T68), SCOPE: 5, CLAUSE: 3\n\nT63 is ground\nT64 is ground\nT65 is ground\nT66 is ground\nX83 is free\ng(T64, .(T63, .(T65, .(T66, []))), T68) !=? g([], X83, X83)", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: g([], .(T81, .(T82, .(T83, []))), T68), SCOPE: 5, CLAUSE: 3\n\nT81 is ground\nT82 is ground\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: g(T97, .(T96, .(T98, .(T99, .(T100, [])))), T102)\n\nT96 is ground\nT97 is ground\nT98 is ground\nT99 is ground\nT100 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: g(T97, .(T96, .(T98, .(T99, .(T100, [])))), T102), SCOPE: 6, CLAUSE: 0 | g(T97, .(T96, .(T98, .(T99, .(T100, [])))), T102), SCOPE: 6, CLAUSE: 3\n\nT96 is ground\nT97 is ground\nT98 is ground\nT99 is ground\nT100 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: true | g([], .(T119, .(T120, .(T121, .(T122, [])))), T102), SCOPE: 6, CLAUSE: 3\n\nT119 is ground\nT120 is ground\nT121 is ground\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: g(T97, .(T96, .(T98, .(T99, .(T100, [])))), T102), SCOPE: 6, CLAUSE: 3\n\nT96 is ground\nT97 is ground\nT98 is ground\nT99 is ground\nT100 is ground\nX104 is free\ng(T97, .(T96, .(T98, .(T99, .(T100, [])))), T102) !=? g([], X104, X104)", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: g([], .(T119, .(T120, .(T121, .(T122, [])))), T102), SCOPE: 6, CLAUSE: 3\n\nT119 is ground\nT120 is ground\nT121 is ground\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: g(T138, .(T137, .(T139, .(T140, .(T141, .(T142, []))))), T144)\n\nT137 is ground\nT138 is ground\nT139 is ground\nT140 is ground\nT141 is ground\nT142 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: g(T138, .(T137, .(T139, .(T140, .(T141, .(T142, []))))), T144), SCOPE: 7, CLAUSE: 0 | g(T138, .(T137, .(T139, .(T140, .(T141, .(T142, []))))), T144), SCOPE: 7, CLAUSE: 3\n\nT137 is ground\nT138 is ground\nT139 is ground\nT140 is ground\nT141 is ground\nT142 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: true | g([], .(T165, .(T166, .(T167, .(T168, .(T169, []))))), T144), SCOPE: 7, CLAUSE: 3\n\nT165 is ground\nT166 is ground\nT167 is ground\nT168 is ground\nT169 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: g(T138, .(T137, .(T139, .(T140, .(T141, .(T142, []))))), T144), SCOPE: 7, CLAUSE: 3\n\nT137 is ground\nT138 is ground\nT139 is ground\nT140 is ground\nT141 is ground\nT142 is ground\nX125 is free\ng(T138, .(T137, .(T139, .(T140, .(T141, .(T142, []))))), T144) !=? g([], X125, X125)", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: g([], .(T165, .(T166, .(T167, .(T168, .(T169, []))))), T144), SCOPE: 7, CLAUSE: 3\n\nT165 is ground\nT166 is ground\nT167 is ground\nT168 is ground\nT169 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: g(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), T194)\n\nT186 is ground\nT187 is ground\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: g(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), T194), SCOPE: 8, CLAUSE: 0 | g(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), T194), SCOPE: 8, CLAUSE: 3\n\nT186 is ground\nT187 is ground\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: true | g([], .(T219, .(T220, .(T221, .(T222, .(T223, .(T224, [])))))), T194), SCOPE: 8, CLAUSE: 3\n\nT219 is ground\nT220 is ground\nT221 is ground\nT222 is ground\nT223 is ground\nT224 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: g(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), T194), SCOPE: 8, CLAUSE: 3\n\nT186 is ground\nT187 is ground\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nT192 is ground\nX146 is free\ng(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), T194) !=? g([], X146, X146)", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: g([], .(T219, .(T220, .(T221, .(T222, .(T223, .(T224, [])))))), T194), SCOPE: 8, CLAUSE: 3\n\nT219 is ground\nT220 is ground\nT221 is ground\nT222 is ground\nT223 is ground\nT224 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: g(T244, .(T243, .(T245, .(T246, .(T247, .(T248, .(T249, .(T250, []))))))), T252)\n\nT243 is ground\nT244 is ground\nT245 is ground\nT246 is ground\nT247 is ground\nT248 is ground\nT249 is ground\nT250 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: g(T244, .(T243, .(T245, .(T246, .(T247, .(T248, .(T249, .(T250, []))))))), T252), SCOPE: 9, CLAUSE: 0 | g(T244, .(T243, .(T245, .(T246, .(T247, .(T248, .(T249, .(T250, []))))))), T252), SCOPE: 9, CLAUSE: 3\n\nT243 is ground\nT244 is ground\nT245 is ground\nT246 is ground\nT247 is ground\nT248 is ground\nT249 is ground\nT250 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: true | g([], .(T281, .(T282, .(T283, .(T284, .(T285, .(T286, .(T287, []))))))), T252), SCOPE: 9, CLAUSE: 3\n\nT281 is ground\nT282 is ground\nT283 is ground\nT284 is ground\nT285 is ground\nT286 is ground\nT287 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: g(T244, .(T243, .(T245, .(T246, .(T247, .(T248, .(T249, .(T250, []))))))), T252), SCOPE: 9, CLAUSE: 3\n\nT243 is ground\nT244 is ground\nT245 is ground\nT246 is ground\nT247 is ground\nT248 is ground\nT249 is ground\nT250 is ground\nX167 is free\ng(T244, .(T243, .(T245, .(T246, .(T247, .(T248, .(T249, .(T250, []))))))), T252) !=? g([], X167, X167)", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: g([], .(T281, .(T282, .(T283, .(T284, .(T285, .(T286, .(T287, []))))))), T252), SCOPE: 9, CLAUSE: 3\n\nT281 is ground\nT282 is ground\nT283 is ground\nT284 is ground\nT285 is ground\nT286 is ground\nT287 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: g(T309, .(T308, .(T310, .(T311, .(T312, .(T313, .(T314, .(T315, .(T316, [])))))))), T318)\n\nT308 is ground\nT309 is ground\nT310 is ground\nT311 is ground\nT312 is ground\nT313 is ground\nT314 is ground\nT315 is ground\nT316 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: g(T309, .(T308, T335), T318)\n\nT308 is ground\nT309 is ground\nT335 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: g(T309, .(T308, T335), T318), SCOPE: 10, CLAUSE: 0 | g(T309, .(T308, T335), T318), SCOPE: 10, CLAUSE: 3\n\nT308 is ground\nT309 is ground\nT335 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: true | g([], .(T344, T345), T318), SCOPE: 10, CLAUSE: 3\n\nT344 is ground\nT345 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: g(T309, .(T308, T335), T318), SCOPE: 10, CLAUSE: 3\n\nT308 is ground\nT309 is ground\nT335 is ground\nX190 is free\ng(T309, .(T308, T335), T318) !=? g([], X190, X190)", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: g([], .(T344, T345), T318), SCOPE: 10, CLAUSE: 3\n\nT344 is ground\nT345 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: g(T357, .(T356, .(T358, T359)), T361)\n\nT356 is ground\nT357 is ground\nT358 is ground\nT359 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: f(T6, [], T3), SCOPE: 1, CLAUSE: 2\n\nT6 is ground\nX7 is free\ng(T6, [], T8) !=? g([], X7, X7)", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: f(.(T377, .(T375, T376)), T378, T380)\n\nT375 is ground\nT376 is ground\nT377 is ground\nT378 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: f(.(T377, .(T375, T376)), T378, T380), SCOPE: 11, CLAUSE: 1 | f(.(T377, .(T375, T376)), T378, T380), SCOPE: 11, CLAUSE: 2\n\nT375 is ground\nT376 is ground\nT377 is ground\nT378 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: f(.(T377, .(T375, T376)), T378, T380), SCOPE: 11, CLAUSE: 1\n\nT375 is ground\nT376 is ground\nT377 is ground\nT378 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: f(.(T377, .(T375, T376)), T378, T380), SCOPE: 11, CLAUSE: 2\n\nT375 is ground\nT376 is ground\nT377 is ground\nT378 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: g(.(T397, .(T398, T399)), [], T401)\n\nT397 is ground\nT398 is ground\nT399 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: g(.(T397, .(T398, T399)), [], T401), SCOPE: 12, CLAUSE: 0 | g(.(T397, .(T398, T399)), [], T401), SCOPE: 12, CLAUSE: 3\n\nT397 is ground\nT398 is ground\nT399 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: g(.(T397, .(T398, T399)), [], T401), SCOPE: 12, CLAUSE: 3\n\nT397 is ground\nT398 is ground\nT399 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: g(.(T412, T413), .(T411, []), T415)\n\nT411 is ground\nT412 is ground\nT413 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: f(.(T431, .(T428, .(T429, T430))), T432, T434)\n\nT428 is ground\nT429 is ground\nT430 is ground\nT431 is ground\nT432 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 159 [arrowhead = none ];
159 -> 4;

160 [label="EVAL with clause\nf(X3, [], X4) :- g(X3, [], X4).\nand substitutionT1 -> T6,\nX3 -> T6,\nT2 -> [],\nT3 -> T8,\nX4 -> T8,\nT7 -> T8", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 160 [arrowhead = none ];
160 -> 7;

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

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

163 [label="EVAL with clause\nf(.(X219, X220), .(X221, X222), X223) :- f(.(X221, .(X219, X220)), X222, X223).\nand substitutionX219 -> T375,\nX220 -> T376,\nT1 -> .(T375, T376),\nX221 -> T377,\nX222 -> T378,\nT2 -> .(T377, T378),\nT3 -> T380,\nX223 -> T380,\nT379 -> T380", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 163 [arrowhead = none ];
163 -> 146;

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

165 [label="EVAL with clause\ng([], X7, X7).\nand substitutionT6 -> [],\nX7 -> [],\nT8 -> []", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 165 [arrowhead = none ];
165 -> 12;

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

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

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

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

170 [label="BACKTRACK\nfor clause: g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
14 -> 170 [arrowhead = none ];
170 -> 15;

171 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 171 [arrowhead = none ];
171 -> 16;

172 [label="BACKTRACK\nfor clause: f(.(A, As), .(B, Bs), RES) :- f(.(B, .(A, As)), Bs, RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 172 [arrowhead = none ];
172 -> 17;

173 [label="EVAL with clause\ng(.(X33, X34), X35, X36) :- g(X34, .(X33, X35), X36).\nand substitutionX33 -> T21,\nX34 -> T22,\nT6 -> .(T21, T22),\nX35 -> [],\nT8 -> T24,\nX36 -> T24,\nT23 -> T24", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 173 [arrowhead = none ];
173 -> 24;

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

175 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 175 [arrowhead = none ];
175 -> 143;

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

177 [label="EVAL with clause\ng([], X41, X41).\nand substitutionT22 -> [],\nT21 -> T29,\nX41 -> .(T29, []),\nT24 -> .(T29, [])", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 177 [arrowhead = none ];
177 -> 30;

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

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

180 [label="EVAL with clause\ng(.(X54, X55), X56, X57) :- g(X55, .(X54, X56), X57).\nand substitutionX54 -> T38,\nX55 -> T39,\nT22 -> .(T38, T39),\nT21 -> T40,\nX56 -> .(T40, []),\nT24 -> T42,\nX57 -> T42,\nT41 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 180 [arrowhead = none ];
180 -> 39;

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

182 [label="BACKTRACK\nfor clause: g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
32 -> 182 [arrowhead = none ];
182 -> 33;

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

184 [label="EVAL with clause\ng([], X62, X62).\nand substitutionT39 -> [],\nT38 -> T51,\nT40 -> T52,\nX62 -> .(T51, .(T52, [])),\nT42 -> .(T51, .(T52, []))", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 184 [arrowhead = none ];
184 -> 45;

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

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

187 [label="EVAL with clause\ng(.(X75, X76), X77, X78) :- g(X76, .(X75, X77), X78).\nand substitutionX75 -> T63,\nX76 -> T64,\nT39 -> .(T63, T64),\nT38 -> T65,\nT40 -> T66,\nX77 -> .(T65, .(T66, [])),\nT42 -> T68,\nX78 -> T68,\nT67 -> T68", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 187 [arrowhead = none ];
187 -> 54;

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

189 [label="BACKTRACK\nfor clause: g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 189 [arrowhead = none ];
189 -> 51;

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

191 [label="EVAL with clause\ng([], X83, X83).\nand substitutionT64 -> [],\nT63 -> T81,\nT65 -> T82,\nT66 -> T83,\nX83 -> .(T81, .(T82, .(T83, []))),\nT68 -> .(T81, .(T82, .(T83, [])))", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 191 [arrowhead = none ];
191 -> 60;

192 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
58 -> 192 [arrowhead = none ];
192 -> 63;

193 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 193 [arrowhead = none ];
193 -> 65;

194 [label="EVAL with clause\ng(.(X96, X97), X98, X99) :- g(X97, .(X96, X98), X99).\nand substitutionX96 -> T96,\nX97 -> T97,\nT64 -> .(T96, T97),\nT63 -> T98,\nT65 -> T99,\nT66 -> T100,\nX98 -> .(T98, .(T99, .(T100, []))),\nT68 -> T102,\nX99 -> T102,\nT101 -> T102", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 194 [arrowhead = none ];
194 -> 68;

195 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
63 -> 195 [arrowhead = none ];
195 -> 70;

196 [label="BACKTRACK\nfor clause: g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 196 [arrowhead = none ];
196 -> 66;

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

198 [label="EVAL with clause\ng([], X104, X104).\nand substitutionT97 -> [],\nT96 -> T119,\nT98 -> T120,\nT99 -> T121,\nT100 -> T122,\nX104 -> .(T119, .(T120, .(T121, .(T122, [])))),\nT102 -> .(T119, .(T120, .(T121, .(T122, []))))", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 198 [arrowhead = none ];
198 -> 76;

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

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

201 [label="EVAL with clause\ng(.(X117, X118), X119, X120) :- g(X118, .(X117, X119), X120).\nand substitutionX117 -> T137,\nX118 -> T138,\nT97 -> .(T137, T138),\nT96 -> T139,\nT98 -> T140,\nT99 -> T141,\nT100 -> T142,\nX119 -> .(T139, .(T140, .(T141, .(T142, [])))),\nT102 -> T144,\nX120 -> T144,\nT143 -> T144", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 201 [arrowhead = none ];
201 -> 83;

202 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
78 -> 202 [arrowhead = none ];
202 -> 84;

203 [label="BACKTRACK\nfor clause: g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
79 -> 203 [arrowhead = none ];
203 -> 80;

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

205 [label="EVAL with clause\ng([], X125, X125).\nand substitutionT138 -> [],\nT137 -> T165,\nT139 -> T166,\nT140 -> T167,\nT141 -> T168,\nT142 -> T169,\nX125 -> .(T165, .(T166, .(T167, .(T168, .(T169, []))))),\nT144 -> .(T165, .(T166, .(T167, .(T168, .(T169, [])))))", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 205 [arrowhead = none ];
205 -> 90;

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

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

208 [label="EVAL with clause\ng(.(X138, X139), X140, X141) :- g(X139, .(X138, X140), X141).\nand substitutionX138 -> T186,\nX139 -> T187,\nT138 -> .(T186, T187),\nT137 -> T188,\nT139 -> T189,\nT140 -> T190,\nT141 -> T191,\nT142 -> T192,\nX140 -> .(T188, .(T189, .(T190, .(T191, .(T192, []))))),\nT144 -> T194,\nX141 -> T194,\nT193 -> T194", fontsize=14, style = filled, fillcolor = lightblue];
92 -> 208 [arrowhead = none ];
208 -> 97;

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

210 [label="BACKTRACK\nfor clause: g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
93 -> 210 [arrowhead = none ];
210 -> 94;

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

212 [label="EVAL with clause\ng([], X146, X146).\nand substitutionT187 -> [],\nT186 -> T219,\nT188 -> T220,\nT189 -> T221,\nT190 -> T222,\nT191 -> T223,\nT192 -> T224,\nX146 -> .(T219, .(T220, .(T221, .(T222, .(T223, .(T224, [])))))),\nT194 -> .(T219, .(T220, .(T221, .(T222, .(T223, .(T224, []))))))", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 212 [arrowhead = none ];
212 -> 105;

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

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

215 [label="EVAL with clause\ng(.(X159, X160), X161, X162) :- g(X160, .(X159, X161), X162).\nand substitutionX159 -> T243,\nX160 -> T244,\nT187 -> .(T243, T244),\nT186 -> T245,\nT188 -> T246,\nT189 -> T247,\nT190 -> T248,\nT191 -> T249,\nT192 -> T250,\nX161 -> .(T245, .(T246, .(T247, .(T248, .(T249, .(T250, [])))))),\nT194 -> T252,\nX162 -> T252,\nT251 -> T252", fontsize=14, style = filled, fillcolor = lightblue];
106 -> 215 [arrowhead = none ];
215 -> 111;

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

217 [label="BACKTRACK\nfor clause: g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
107 -> 217 [arrowhead = none ];
217 -> 108;

218 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
111 -> 218 [arrowhead = none ];
218 -> 114;

219 [label="EVAL with clause\ng([], X167, X167).\nand substitutionT244 -> [],\nT243 -> T281,\nT245 -> T282,\nT246 -> T283,\nT247 -> T284,\nT248 -> T285,\nT249 -> T286,\nT250 -> T287,\nX167 -> .(T281, .(T282, .(T283, .(T284, .(T285, .(T286, .(T287, []))))))),\nT252 -> .(T281, .(T282, .(T283, .(T284, .(T285, .(T286, .(T287, [])))))))", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 219 [arrowhead = none ];
219 -> 119;

220 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
114 -> 220 [arrowhead = none ];
220 -> 120;

221 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
119 -> 221 [arrowhead = none ];
221 -> 121;

222 [label="EVAL with clause\ng(.(X180, X181), X182, X183) :- g(X181, .(X180, X182), X183).\nand substitutionX180 -> T308,\nX181 -> T309,\nT244 -> .(T308, T309),\nT243 -> T310,\nT245 -> T311,\nT246 -> T312,\nT247 -> T313,\nT248 -> T314,\nT249 -> T315,\nT250 -> T316,\nX182 -> .(T310, .(T311, .(T312, .(T313, .(T314, .(T315, .(T316, []))))))),\nT252 -> T318,\nX183 -> T318,\nT317 -> T318", fontsize=14, style = filled, fillcolor = lightblue];
120 -> 222 [arrowhead = none ];
222 -> 125;

223 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
120 -> 223 [arrowhead = none ];
223 -> 126;

224 [label="BACKTRACK\nfor clause: g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
121 -> 224 [arrowhead = none ];
224 -> 122;

225 [label="GENERALIZATION\nT335 <-- .(T310, .(T311, .(T312, .(T313, .(T314, .(T315, .(T316, [])))))))\n\nNew Knowledge:\nT335 is ground", fontsize=14, style = filled, fillcolor = violet];
125 -> 225 [arrowhead = none ];
225 -> 128;

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

227 [label="EVAL with clause\ng([], X190, X190).\nand substitutionT309 -> [],\nT308 -> T344,\nT335 -> T345,\nX190 -> .(T344, T345),\nT318 -> .(T344, T345)", fontsize=14, style = filled, fillcolor = lightblue];
129 -> 227 [arrowhead = none ];
227 -> 131;

228 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
129 -> 228 [arrowhead = none ];
228 -> 133;

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

230 [label="EVAL with clause\ng(.(X203, X204), X205, X206) :- g(X204, .(X203, X205), X206).\nand substitutionX203 -> T356,\nX204 -> T357,\nT309 -> .(T356, T357),\nT308 -> T358,\nT335 -> T359,\nX205 -> .(T358, T359),\nT318 -> T361,\nX206 -> T361,\nT360 -> T361", fontsize=14, style = filled, fillcolor = lightblue];
133 -> 230 [arrowhead = none ];
230 -> 139;

231 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
133 -> 231 [arrowhead = none ];
231 -> 140;

232 [label="BACKTRACK\nfor clause: g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
134 -> 232 [arrowhead = none ];
232 -> 137;

233 [label="INSTANCE with matching:\nT309 -> T357\nT308 -> T356\nT335 -> .(T358, T359)\nT318 -> T361", fontsize=14, style = filled, fillcolor = lightgrey];
139 -> 233 [arrowhead = none , style=dashed];
233 -> 128[style=dashed];

234 [label="BACKTRACK\nfor clause: f(.(A, As), .(B, Bs), RES) :- f(.(B, .(A, As)), Bs, RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
143 -> 234 [arrowhead = none ];
234 -> 144;

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

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

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

238 [label="EVAL with clause\nf(X232, [], X233) :- g(X232, [], X233).\nand substitutionT377 -> T397,\nT375 -> T398,\nT376 -> T399,\nX232 -> .(T397, .(T398, T399)),\nT378 -> [],\nT380 -> T401,\nX233 -> T401,\nT400 -> T401", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 238 [arrowhead = none ];
238 -> 152;

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

240 [label="EVAL with clause\nf(.(X263, X264), .(X265, X266), X267) :- f(.(X265, .(X263, X264)), X266, X267).\nand substitutionT377 -> T428,\nX263 -> T428,\nT375 -> T429,\nT376 -> T430,\nX264 -> .(T429, T430),\nX265 -> T431,\nX266 -> T432,\nT378 -> .(T431, T432),\nT380 -> T434,\nX267 -> T434,\nT433 -> T434", fontsize=14, style = filled, fillcolor = lightblue];
151 -> 240 [arrowhead = none ];
240 -> 157;

241 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
151 -> 241 [arrowhead = none ];
241 -> 158;

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

243 [label="BACKTRACK\nfor clause: g([], RES, RES)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
154 -> 243 [arrowhead = none ];
243 -> 155;

244 [label="ONLY EVAL with clause\ng(.(X247, X248), X249, X250) :- g(X248, .(X247, X249), X250).\nand substitutionT397 -> T411,\nX247 -> T411,\nT398 -> T412,\nT399 -> T413,\nX248 -> .(T412, T413),\nX249 -> [],\nT401 -> T415,\nX250 -> T415,\nT414 -> T415", fontsize=14, style = filled, fillcolor = lightblue];
155 -> 244 [arrowhead = none ];
244 -> 156;

245 [label="INSTANCE with matching:\nT22 -> .(T412, T413)\nT21 -> T411\nT24 -> T415", fontsize=14, style = filled, fillcolor = lightgrey];
156 -> 245 [arrowhead = none , style=dashed];
245 -> 24[style=dashed];

246 [label="INSTANCE with matching:\nT1 -> .(T431, .(T428, .(T429, T430)))\nT2 -> T432\nT3 -> T434", fontsize=14, style = filled, fillcolor = lightgrey];
157 -> 246 [arrowhead = none , style=dashed];
246 -> 1[style=dashed];

}

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([], []) → f1_out1([])
f1_in(z0, []) → U1(f13_in(z0), z0, [])
f1_in(.(z0, z1), .(z2, z3)) → U2(f149_in(z2, z0, z1, z3), .(z0, z1), .(z2, z3))
U1(f13_out1(z0), z1, []) → f1_out1(z0)
U1(f13_out3(z0), z1, []) → f1_out1(z0)
U2(f149_out1(z0), .(z1, z2), .(z3, z4)) → f1_out1(z0)
U2(f149_out2(z0), .(z1, z2), .(z3, z4)) → f1_out1(z0)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, []), z1) → f24_out1(.(z0, .(z1, [])))
f24_in(.(z0, .(z1, [])), z2) → f24_out1(.(z1, .(z0, .(z2, []))))
f24_in(.(z0, .(z1, .(z2, []))), z3) → f24_out1(.(z2, .(z1, .(z0, .(z3, [])))))
f24_in(.(z0, .(z1, .(z2, .(z3, [])))), z4) → f24_out1(.(z3, .(z2, .(z1, .(z0, .(z4, []))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, []))))), z5) → f24_out1(.(z4, .(z3, .(z2, .(z1, .(z0, .(z5, [])))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, [])))))), z6) → f24_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z6, []))))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → U3(f128_in(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8)
U3(f128_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))), z9) → f24_out1(z0)
f128_in([], z0, z1) → f128_out1(.(z0, z1))
f128_in(.(z0, z1), z2, z3) → U4(f128_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U4(f128_out1(z0), .(z1, z2), z3, z4) → f128_out1(z0)
f18_in(.(z0, z1)) → U5(f24_in(z1, z0), .(z0, z1))
U5(f24_out1(z0), .(z1, z2)) → f18_out1(z0)
f150_in(z0, z1, z2, []) → U6(f24_in(.(z1, z2), z0), z0, z1, z2, [])
U6(f24_out1(z0), z1, z2, z3, []) → f150_out1(z0)
f151_in(z0, z1, z2, .(z3, z4)) → U7(f1_in(.(z3, .(z0, .(z1, z2))), z4), z0, z1, z2, .(z3, z4))
U7(f1_out1(z0), z1, z2, z3, .(z4, z5)) → f151_out1(z0)
f13_in(z0) → U8(f18_in(z0), f19_in(z0), z0)
U8(f18_out1(z0), z1, z2) → f13_out1(z0)
U8(z0, f19_out2(z1), z2) → f13_out3(z1)
f149_in(z0, z1, z2, z3) → U9(f150_in(z0, z1, z2, z3), f151_in(z0, z1, z2, z3), z0, z1, z2, z3)
U9(f150_out1(z0), z1, z2, z3, z4, z5) → f149_out1(z0)
U9(z0, f151_out1(z1), z2, z3, z4, z5) → f149_out2(z1)

Tuples:

F1_IN(z0, []) → c1(U1'(f13_in(z0), z0, []), F13_IN(z0))
F1_IN(.(z0, z1), .(z2, z3)) → c2(U2'(f149_in(z2, z0, z1, z3), .(z0, z1), .(z2, z3)), F149_IN(z2, z0, z1, z3))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c14(U3'(f128_in(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8), F128_IN(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))))
F128_IN(.(z0, z1), z2, z3) → c17(U4'(f128_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F128_IN(z1, z0, .(z2, z3)))
F18_IN(.(z0, z1)) → c19(U5'(f24_in(z1, z0), .(z0, z1)), F24_IN(z1, z0))
F150_IN(z0, z1, z2, []) → c21(U6'(f24_in(.(z1, z2), z0), z0, z1, z2, []), F24_IN(.(z1, z2), z0))
F151_IN(z0, z1, z2, .(z3, z4)) → c23(U7'(f1_in(.(z3, .(z0, .(z1, z2))), z4), z0, z1, z2, .(z3, z4)), F1_IN(.(z3, .(z0, .(z1, z2))), z4))
F13_IN(z0) → c25(U8'(f18_in(z0), f19_in(z0), z0), F18_IN(z0))
F149_IN(z0, z1, z2, z3) → c28(U9'(f150_in(z0, z1, z2, z3), f151_in(z0, z1, z2, z3), z0, z1, z2, z3), F150_IN(z0, z1, z2, z3), F151_IN(z0, z1, z2, z3))

S tuples:

F1_IN(z0, []) → c1(U1'(f13_in(z0), z0, []), F13_IN(z0))
F1_IN(.(z0, z1), .(z2, z3)) → c2(U2'(f149_in(z2, z0, z1, z3), .(z0, z1), .(z2, z3)), F149_IN(z2, z0, z1, z3))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c14(U3'(f128_in(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8), F128_IN(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))))
F128_IN(.(z0, z1), z2, z3) → c17(U4'(f128_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F128_IN(z1, z0, .(z2, z3)))
F18_IN(.(z0, z1)) → c19(U5'(f24_in(z1, z0), .(z0, z1)), F24_IN(z1, z0))
F150_IN(z0, z1, z2, []) → c21(U6'(f24_in(.(z1, z2), z0), z0, z1, z2, []), F24_IN(.(z1, z2), z0))
F151_IN(z0, z1, z2, .(z3, z4)) → c23(U7'(f1_in(.(z3, .(z0, .(z1, z2))), z4), z0, z1, z2, .(z3, z4)), F1_IN(.(z3, .(z0, .(z1, z2))), z4))
F13_IN(z0) → c25(U8'(f18_in(z0), f19_in(z0), z0), F18_IN(z0))
F149_IN(z0, z1, z2, z3) → c28(U9'(f150_in(z0, z1, z2, z3), f151_in(z0, z1, z2, z3), z0, z1, z2, z3), F150_IN(z0, z1, z2, z3), F151_IN(z0, z1, z2, z3))

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, f24_in, U3, f128_in, U4, f18_in, U5, f150_in, U6, f151_in, U7, f13_in, U8, f149_in, U9

Defined Pair Symbols:

F1_IN, F24_IN, F128_IN, F18_IN, F150_IN, F151_IN, F13_IN, F149_IN

Compound Symbols:

c1, c2, c14, c17, c19, c21, c23, c25, c28

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

Split RHS of tuples not part of any SCC

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([], []) → f1_out1([])
f1_in(z0, []) → U1(f13_in(z0), z0, [])
f1_in(.(z0, z1), .(z2, z3)) → U2(f149_in(z2, z0, z1, z3), .(z0, z1), .(z2, z3))
U1(f13_out1(z0), z1, []) → f1_out1(z0)
U1(f13_out3(z0), z1, []) → f1_out1(z0)
U2(f149_out1(z0), .(z1, z2), .(z3, z4)) → f1_out1(z0)
U2(f149_out2(z0), .(z1, z2), .(z3, z4)) → f1_out1(z0)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, []), z1) → f24_out1(.(z0, .(z1, [])))
f24_in(.(z0, .(z1, [])), z2) → f24_out1(.(z1, .(z0, .(z2, []))))
f24_in(.(z0, .(z1, .(z2, []))), z3) → f24_out1(.(z2, .(z1, .(z0, .(z3, [])))))
f24_in(.(z0, .(z1, .(z2, .(z3, [])))), z4) → f24_out1(.(z3, .(z2, .(z1, .(z0, .(z4, []))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, []))))), z5) → f24_out1(.(z4, .(z3, .(z2, .(z1, .(z0, .(z5, [])))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, [])))))), z6) → f24_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z6, []))))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → U3(f128_in(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8)
U3(f128_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))), z9) → f24_out1(z0)
f128_in([], z0, z1) → f128_out1(.(z0, z1))
f128_in(.(z0, z1), z2, z3) → U4(f128_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U4(f128_out1(z0), .(z1, z2), z3, z4) → f128_out1(z0)
f18_in(.(z0, z1)) → U5(f24_in(z1, z0), .(z0, z1))
U5(f24_out1(z0), .(z1, z2)) → f18_out1(z0)
f150_in(z0, z1, z2, []) → U6(f24_in(.(z1, z2), z0), z0, z1, z2, [])
U6(f24_out1(z0), z1, z2, z3, []) → f150_out1(z0)
f151_in(z0, z1, z2, .(z3, z4)) → U7(f1_in(.(z3, .(z0, .(z1, z2))), z4), z0, z1, z2, .(z3, z4))
U7(f1_out1(z0), z1, z2, z3, .(z4, z5)) → f151_out1(z0)
f13_in(z0) → U8(f18_in(z0), f19_in(z0), z0)
U8(f18_out1(z0), z1, z2) → f13_out1(z0)
U8(z0, f19_out2(z1), z2) → f13_out3(z1)
f149_in(z0, z1, z2, z3) → U9(f150_in(z0, z1, z2, z3), f151_in(z0, z1, z2, z3), z0, z1, z2, z3)
U9(f150_out1(z0), z1, z2, z3, z4, z5) → f149_out1(z0)
U9(z0, f151_out1(z1), z2, z3, z4, z5) → f149_out2(z1)

Tuples:

F1_IN(.(z0, z1), .(z2, z3)) → c2(U2'(f149_in(z2, z0, z1, z3), .(z0, z1), .(z2, z3)), F149_IN(z2, z0, z1, z3))
F128_IN(.(z0, z1), z2, z3) → c17(U4'(f128_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F128_IN(z1, z0, .(z2, z3)))
F151_IN(z0, z1, z2, .(z3, z4)) → c23(U7'(f1_in(.(z3, .(z0, .(z1, z2))), z4), z0, z1, z2, .(z3, z4)), F1_IN(.(z3, .(z0, .(z1, z2))), z4))
F149_IN(z0, z1, z2, z3) → c28(U9'(f150_in(z0, z1, z2, z3), f151_in(z0, z1, z2, z3), z0, z1, z2, z3), F150_IN(z0, z1, z2, z3), F151_IN(z0, z1, z2, z3))
F1_IN(z0, []) → c(U1'(f13_in(z0), z0, []))
F1_IN(z0, []) → c(F13_IN(z0))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c(U3'(f128_in(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c(F128_IN(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))))
F18_IN(.(z0, z1)) → c(U5'(f24_in(z1, z0), .(z0, z1)))
F18_IN(.(z0, z1)) → c(F24_IN(z1, z0))
F150_IN(z0, z1, z2, []) → c(U6'(f24_in(.(z1, z2), z0), z0, z1, z2, []))
F150_IN(z0, z1, z2, []) → c(F24_IN(.(z1, z2), z0))
F13_IN(z0) → c(U8'(f18_in(z0), f19_in(z0), z0))
F13_IN(z0) → c(F18_IN(z0))

S tuples:

F1_IN(.(z0, z1), .(z2, z3)) → c2(U2'(f149_in(z2, z0, z1, z3), .(z0, z1), .(z2, z3)), F149_IN(z2, z0, z1, z3))
F128_IN(.(z0, z1), z2, z3) → c17(U4'(f128_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F128_IN(z1, z0, .(z2, z3)))
F151_IN(z0, z1, z2, .(z3, z4)) → c23(U7'(f1_in(.(z3, .(z0, .(z1, z2))), z4), z0, z1, z2, .(z3, z4)), F1_IN(.(z3, .(z0, .(z1, z2))), z4))
F149_IN(z0, z1, z2, z3) → c28(U9'(f150_in(z0, z1, z2, z3), f151_in(z0, z1, z2, z3), z0, z1, z2, z3), F150_IN(z0, z1, z2, z3), F151_IN(z0, z1, z2, z3))
F1_IN(z0, []) → c(U1'(f13_in(z0), z0, []))
F1_IN(z0, []) → c(F13_IN(z0))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c(U3'(f128_in(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c(F128_IN(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))))
F18_IN(.(z0, z1)) → c(U5'(f24_in(z1, z0), .(z0, z1)))
F18_IN(.(z0, z1)) → c(F24_IN(z1, z0))
F150_IN(z0, z1, z2, []) → c(U6'(f24_in(.(z1, z2), z0), z0, z1, z2, []))
F150_IN(z0, z1, z2, []) → c(F24_IN(.(z1, z2), z0))
F13_IN(z0) → c(U8'(f18_in(z0), f19_in(z0), z0))
F13_IN(z0) → c(F18_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, f24_in, U3, f128_in, U4, f18_in, U5, f150_in, U6, f151_in, U7, f13_in, U8, f149_in, U9

Defined Pair Symbols:

F1_IN, F128_IN, F151_IN, F149_IN, F24_IN, F18_IN, F150_IN, F13_IN

Compound Symbols:

c2, c17, c23, c28, c

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

Removed 9 trailing tuple parts

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([], []) → f1_out1([])
f1_in(z0, []) → U1(f13_in(z0), z0, [])
f1_in(.(z0, z1), .(z2, z3)) → U2(f149_in(z2, z0, z1, z3), .(z0, z1), .(z2, z3))
U1(f13_out1(z0), z1, []) → f1_out1(z0)
U1(f13_out3(z0), z1, []) → f1_out1(z0)
U2(f149_out1(z0), .(z1, z2), .(z3, z4)) → f1_out1(z0)
U2(f149_out2(z0), .(z1, z2), .(z3, z4)) → f1_out1(z0)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, []), z1) → f24_out1(.(z0, .(z1, [])))
f24_in(.(z0, .(z1, [])), z2) → f24_out1(.(z1, .(z0, .(z2, []))))
f24_in(.(z0, .(z1, .(z2, []))), z3) → f24_out1(.(z2, .(z1, .(z0, .(z3, [])))))
f24_in(.(z0, .(z1, .(z2, .(z3, [])))), z4) → f24_out1(.(z3, .(z2, .(z1, .(z0, .(z4, []))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, []))))), z5) → f24_out1(.(z4, .(z3, .(z2, .(z1, .(z0, .(z5, [])))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, [])))))), z6) → f24_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z6, []))))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → U3(f128_in(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8)
U3(f128_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))), z9) → f24_out1(z0)
f128_in([], z0, z1) → f128_out1(.(z0, z1))
f128_in(.(z0, z1), z2, z3) → U4(f128_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U4(f128_out1(z0), .(z1, z2), z3, z4) → f128_out1(z0)
f18_in(.(z0, z1)) → U5(f24_in(z1, z0), .(z0, z1))
U5(f24_out1(z0), .(z1, z2)) → f18_out1(z0)
f150_in(z0, z1, z2, []) → U6(f24_in(.(z1, z2), z0), z0, z1, z2, [])
U6(f24_out1(z0), z1, z2, z3, []) → f150_out1(z0)
f151_in(z0, z1, z2, .(z3, z4)) → U7(f1_in(.(z3, .(z0, .(z1, z2))), z4), z0, z1, z2, .(z3, z4))
U7(f1_out1(z0), z1, z2, z3, .(z4, z5)) → f151_out1(z0)
f13_in(z0) → U8(f18_in(z0), f19_in(z0), z0)
U8(f18_out1(z0), z1, z2) → f13_out1(z0)
U8(z0, f19_out2(z1), z2) → f13_out3(z1)
f149_in(z0, z1, z2, z3) → U9(f150_in(z0, z1, z2, z3), f151_in(z0, z1, z2, z3), z0, z1, z2, z3)
U9(f150_out1(z0), z1, z2, z3, z4, z5) → f149_out1(z0)
U9(z0, f151_out1(z1), z2, z3, z4, z5) → f149_out2(z1)

Tuples:

F1_IN(z0, []) → c(F13_IN(z0))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c(F128_IN(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))))
F18_IN(.(z0, z1)) → c(F24_IN(z1, z0))
F150_IN(z0, z1, z2, []) → c(F24_IN(.(z1, z2), z0))
F13_IN(z0) → c(F18_IN(z0))
F1_IN(.(z0, z1), .(z2, z3)) → c2(F149_IN(z2, z0, z1, z3))
F128_IN(.(z0, z1), z2, z3) → c17(F128_IN(z1, z0, .(z2, z3)))
F151_IN(z0, z1, z2, .(z3, z4)) → c23(F1_IN(.(z3, .(z0, .(z1, z2))), z4))
F149_IN(z0, z1, z2, z3) → c28(F150_IN(z0, z1, z2, z3), F151_IN(z0, z1, z2, z3))
F1_IN(z0, []) → c
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c
F18_IN(.(z0, z1)) → c
F150_IN(z0, z1, z2, []) → c
F13_IN(z0) → c

S tuples:

F1_IN(z0, []) → c(F13_IN(z0))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c(F128_IN(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))))
F18_IN(.(z0, z1)) → c(F24_IN(z1, z0))
F150_IN(z0, z1, z2, []) → c(F24_IN(.(z1, z2), z0))
F13_IN(z0) → c(F18_IN(z0))
F1_IN(.(z0, z1), .(z2, z3)) → c2(F149_IN(z2, z0, z1, z3))
F128_IN(.(z0, z1), z2, z3) → c17(F128_IN(z1, z0, .(z2, z3)))
F151_IN(z0, z1, z2, .(z3, z4)) → c23(F1_IN(.(z3, .(z0, .(z1, z2))), z4))
F149_IN(z0, z1, z2, z3) → c28(F150_IN(z0, z1, z2, z3), F151_IN(z0, z1, z2, z3))
F1_IN(z0, []) → c
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c
F18_IN(.(z0, z1)) → c
F150_IN(z0, z1, z2, []) → c
F13_IN(z0) → c

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, f24_in, U3, f128_in, U4, f18_in, U5, f150_in, U6, f151_in, U7, f13_in, U8, f149_in, U9

Defined Pair Symbols:

F1_IN, F24_IN, F18_IN, F150_IN, F13_IN, F128_IN, F151_IN, F149_IN

Compound Symbols:

c, c2, c17, c23, c28, c

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

F13_IN(z0) → c(F18_IN(z0))
F1_IN(z0, []) → c
F13_IN(z0) → c

We considered the (Usable) Rules:none
And the Tuples:

F1_IN(z0, []) → c(F13_IN(z0))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c(F128_IN(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))))
F18_IN(.(z0, z1)) → c(F24_IN(z1, z0))
F150_IN(z0, z1, z2, []) → c(F24_IN(.(z1, z2), z0))
F13_IN(z0) → c(F18_IN(z0))
F1_IN(.(z0, z1), .(z2, z3)) → c2(F149_IN(z2, z0, z1, z3))
F128_IN(.(z0, z1), z2, z3) → c17(F128_IN(z1, z0, .(z2, z3)))
F151_IN(z0, z1, z2, .(z3, z4)) → c23(F1_IN(.(z3, .(z0, .(z1, z2))), z4))
F149_IN(z0, z1, z2, z3) → c28(F150_IN(z0, z1, z2, z3), F151_IN(z0, z1, z2, z3))
F1_IN(z0, []) → c
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c
F18_IN(.(z0, z1)) → c
F150_IN(z0, z1, z2, []) → c
F13_IN(z0) → c

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

POL(.(x₁, x₂)) = 0   
POL(F128_IN(x₁, x₂, x₃)) = [2]x₃   
POL(F13_IN(x₁)) = [1] + x₁   
POL(F149_IN(x₁, x₂, x₃, x₄)) = [1]   
POL(F150_IN(x₁, x₂, x₃, x₄)) = 0   
POL(F151_IN(x₁, x₂, x₃, x₄)) = [1]   
POL(F18_IN(x₁)) = x₁   
POL(F1_IN(x₁, x₂)) = [1] + x₁   
POL(F24_IN(x₁, x₂)) = 0   
POL([]) = 0   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c17(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c23(x₁)) = x₁   
POL(c28(x₁, x₂)) = x₁ + x₂   

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([], []) → f1_out1([])
f1_in(z0, []) → U1(f13_in(z0), z0, [])
f1_in(.(z0, z1), .(z2, z3)) → U2(f149_in(z2, z0, z1, z3), .(z0, z1), .(z2, z3))
U1(f13_out1(z0), z1, []) → f1_out1(z0)
U1(f13_out3(z0), z1, []) → f1_out1(z0)
U2(f149_out1(z0), .(z1, z2), .(z3, z4)) → f1_out1(z0)
U2(f149_out2(z0), .(z1, z2), .(z3, z4)) → f1_out1(z0)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, []), z1) → f24_out1(.(z0, .(z1, [])))
f24_in(.(z0, .(z1, [])), z2) → f24_out1(.(z1, .(z0, .(z2, []))))
f24_in(.(z0, .(z1, .(z2, []))), z3) → f24_out1(.(z2, .(z1, .(z0, .(z3, [])))))
f24_in(.(z0, .(z1, .(z2, .(z3, [])))), z4) → f24_out1(.(z3, .(z2, .(z1, .(z0, .(z4, []))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, []))))), z5) → f24_out1(.(z4, .(z3, .(z2, .(z1, .(z0, .(z5, [])))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, [])))))), z6) → f24_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z6, []))))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → U3(f128_in(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8)
U3(f128_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))), z9) → f24_out1(z0)
f128_in([], z0, z1) → f128_out1(.(z0, z1))
f128_in(.(z0, z1), z2, z3) → U4(f128_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U4(f128_out1(z0), .(z1, z2), z3, z4) → f128_out1(z0)
f18_in(.(z0, z1)) → U5(f24_in(z1, z0), .(z0, z1))
U5(f24_out1(z0), .(z1, z2)) → f18_out1(z0)
f150_in(z0, z1, z2, []) → U6(f24_in(.(z1, z2), z0), z0, z1, z2, [])
U6(f24_out1(z0), z1, z2, z3, []) → f150_out1(z0)
f151_in(z0, z1, z2, .(z3, z4)) → U7(f1_in(.(z3, .(z0, .(z1, z2))), z4), z0, z1, z2, .(z3, z4))
U7(f1_out1(z0), z1, z2, z3, .(z4, z5)) → f151_out1(z0)
f13_in(z0) → U8(f18_in(z0), f19_in(z0), z0)
U8(f18_out1(z0), z1, z2) → f13_out1(z0)
U8(z0, f19_out2(z1), z2) → f13_out3(z1)
f149_in(z0, z1, z2, z3) → U9(f150_in(z0, z1, z2, z3), f151_in(z0, z1, z2, z3), z0, z1, z2, z3)
U9(f150_out1(z0), z1, z2, z3, z4, z5) → f149_out1(z0)
U9(z0, f151_out1(z1), z2, z3, z4, z5) → f149_out2(z1)

Tuples:

F1_IN(z0, []) → c(F13_IN(z0))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c(F128_IN(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))))
F18_IN(.(z0, z1)) → c(F24_IN(z1, z0))
F150_IN(z0, z1, z2, []) → c(F24_IN(.(z1, z2), z0))
F13_IN(z0) → c(F18_IN(z0))
F1_IN(.(z0, z1), .(z2, z3)) → c2(F149_IN(z2, z0, z1, z3))
F128_IN(.(z0, z1), z2, z3) → c17(F128_IN(z1, z0, .(z2, z3)))
F151_IN(z0, z1, z2, .(z3, z4)) → c23(F1_IN(.(z3, .(z0, .(z1, z2))), z4))
F149_IN(z0, z1, z2, z3) → c28(F150_IN(z0, z1, z2, z3), F151_IN(z0, z1, z2, z3))
F1_IN(z0, []) → c
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c
F18_IN(.(z0, z1)) → c
F150_IN(z0, z1, z2, []) → c
F13_IN(z0) → c

S tuples:

F1_IN(z0, []) → c(F13_IN(z0))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c(F128_IN(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))))
F18_IN(.(z0, z1)) → c(F24_IN(z1, z0))
F150_IN(z0, z1, z2, []) → c(F24_IN(.(z1, z2), z0))
F1_IN(.(z0, z1), .(z2, z3)) → c2(F149_IN(z2, z0, z1, z3))
F128_IN(.(z0, z1), z2, z3) → c17(F128_IN(z1, z0, .(z2, z3)))
F151_IN(z0, z1, z2, .(z3, z4)) → c23(F1_IN(.(z3, .(z0, .(z1, z2))), z4))
F149_IN(z0, z1, z2, z3) → c28(F150_IN(z0, z1, z2, z3), F151_IN(z0, z1, z2, z3))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c
F18_IN(.(z0, z1)) → c
F150_IN(z0, z1, z2, []) → c

K tuples:

F13_IN(z0) → c(F18_IN(z0))
F1_IN(z0, []) → c
F13_IN(z0) → c

Defined Rule Symbols:

f1_in, U1, U2, f24_in, U3, f128_in, U4, f18_in, U5, f150_in, U6, f151_in, U7, f13_in, U8, f149_in, U9

Defined Pair Symbols:

F1_IN, F24_IN, F18_IN, F150_IN, F13_IN, F128_IN, F151_IN, F149_IN

Compound Symbols:

c, c2, c17, c23, c28, c

(25) CdtKnowledgeProof (EQUIVALENT transformation)

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

F18_IN(.(z0, z1)) → c(F24_IN(z1, z0))
F18_IN(.(z0, z1)) → c

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([], []) → f1_out1([])
f1_in(z0, []) → U1(f13_in(z0), z0, [])
f1_in(.(z0, z1), .(z2, z3)) → U2(f149_in(z2, z0, z1, z3), .(z0, z1), .(z2, z3))
U1(f13_out1(z0), z1, []) → f1_out1(z0)
U1(f13_out3(z0), z1, []) → f1_out1(z0)
U2(f149_out1(z0), .(z1, z2), .(z3, z4)) → f1_out1(z0)
U2(f149_out2(z0), .(z1, z2), .(z3, z4)) → f1_out1(z0)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, []), z1) → f24_out1(.(z0, .(z1, [])))
f24_in(.(z0, .(z1, [])), z2) → f24_out1(.(z1, .(z0, .(z2, []))))
f24_in(.(z0, .(z1, .(z2, []))), z3) → f24_out1(.(z2, .(z1, .(z0, .(z3, [])))))
f24_in(.(z0, .(z1, .(z2, .(z3, [])))), z4) → f24_out1(.(z3, .(z2, .(z1, .(z0, .(z4, []))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, []))))), z5) → f24_out1(.(z4, .(z3, .(z2, .(z1, .(z0, .(z5, [])))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, [])))))), z6) → f24_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z6, []))))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → U3(f128_in(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8)
U3(f128_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))), z9) → f24_out1(z0)
f128_in([], z0, z1) → f128_out1(.(z0, z1))
f128_in(.(z0, z1), z2, z3) → U4(f128_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U4(f128_out1(z0), .(z1, z2), z3, z4) → f128_out1(z0)
f18_in(.(z0, z1)) → U5(f24_in(z1, z0), .(z0, z1))
U5(f24_out1(z0), .(z1, z2)) → f18_out1(z0)
f150_in(z0, z1, z2, []) → U6(f24_in(.(z1, z2), z0), z0, z1, z2, [])
U6(f24_out1(z0), z1, z2, z3, []) → f150_out1(z0)
f151_in(z0, z1, z2, .(z3, z4)) → U7(f1_in(.(z3, .(z0, .(z1, z2))), z4), z0, z1, z2, .(z3, z4))
U7(f1_out1(z0), z1, z2, z3, .(z4, z5)) → f151_out1(z0)
f13_in(z0) → U8(f18_in(z0), f19_in(z0), z0)
U8(f18_out1(z0), z1, z2) → f13_out1(z0)
U8(z0, f19_out2(z1), z2) → f13_out3(z1)
f149_in(z0, z1, z2, z3) → U9(f150_in(z0, z1, z2, z3), f151_in(z0, z1, z2, z3), z0, z1, z2, z3)
U9(f150_out1(z0), z1, z2, z3, z4, z5) → f149_out1(z0)
U9(z0, f151_out1(z1), z2, z3, z4, z5) → f149_out2(z1)

Tuples:

F1_IN(z0, []) → c(F13_IN(z0))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c(F128_IN(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))))
F18_IN(.(z0, z1)) → c(F24_IN(z1, z0))
F150_IN(z0, z1, z2, []) → c(F24_IN(.(z1, z2), z0))
F13_IN(z0) → c(F18_IN(z0))
F1_IN(.(z0, z1), .(z2, z3)) → c2(F149_IN(z2, z0, z1, z3))
F128_IN(.(z0, z1), z2, z3) → c17(F128_IN(z1, z0, .(z2, z3)))
F151_IN(z0, z1, z2, .(z3, z4)) → c23(F1_IN(.(z3, .(z0, .(z1, z2))), z4))
F149_IN(z0, z1, z2, z3) → c28(F150_IN(z0, z1, z2, z3), F151_IN(z0, z1, z2, z3))
F1_IN(z0, []) → c
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c
F18_IN(.(z0, z1)) → c
F150_IN(z0, z1, z2, []) → c
F13_IN(z0) → c

S tuples:

F1_IN(z0, []) → c(F13_IN(z0))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c(F128_IN(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))))
F150_IN(z0, z1, z2, []) → c(F24_IN(.(z1, z2), z0))
F1_IN(.(z0, z1), .(z2, z3)) → c2(F149_IN(z2, z0, z1, z3))
F128_IN(.(z0, z1), z2, z3) → c17(F128_IN(z1, z0, .(z2, z3)))
F151_IN(z0, z1, z2, .(z3, z4)) → c23(F1_IN(.(z3, .(z0, .(z1, z2))), z4))
F149_IN(z0, z1, z2, z3) → c28(F150_IN(z0, z1, z2, z3), F151_IN(z0, z1, z2, z3))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c
F150_IN(z0, z1, z2, []) → c

K tuples:

F13_IN(z0) → c(F18_IN(z0))
F1_IN(z0, []) → c
F13_IN(z0) → c
F18_IN(.(z0, z1)) → c(F24_IN(z1, z0))
F18_IN(.(z0, z1)) → c

Defined Rule Symbols:

f1_in, U1, U2, f24_in, U3, f128_in, U4, f18_in, U5, f150_in, U6, f151_in, U7, f13_in, U8, f149_in, U9

Defined Pair Symbols:

F1_IN, F24_IN, F18_IN, F150_IN, F13_IN, F128_IN, F151_IN, F149_IN

Compound Symbols:

c, c2, c17, c23, c28, c

(27) 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(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c(F128_IN(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))))
F1_IN(.(z0, z1), .(z2, z3)) → c2(F149_IN(z2, z0, z1, z3))
F151_IN(z0, z1, z2, .(z3, z4)) → c23(F1_IN(.(z3, .(z0, .(z1, z2))), z4))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c
F150_IN(z0, z1, z2, []) → c

We considered the (Usable) Rules:none
And the Tuples:

F1_IN(z0, []) → c(F13_IN(z0))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c(F128_IN(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))))
F18_IN(.(z0, z1)) → c(F24_IN(z1, z0))
F150_IN(z0, z1, z2, []) → c(F24_IN(.(z1, z2), z0))
F13_IN(z0) → c(F18_IN(z0))
F1_IN(.(z0, z1), .(z2, z3)) → c2(F149_IN(z2, z0, z1, z3))
F128_IN(.(z0, z1), z2, z3) → c17(F128_IN(z1, z0, .(z2, z3)))
F151_IN(z0, z1, z2, .(z3, z4)) → c23(F1_IN(.(z3, .(z0, .(z1, z2))), z4))
F149_IN(z0, z1, z2, z3) → c28(F150_IN(z0, z1, z2, z3), F151_IN(z0, z1, z2, z3))
F1_IN(z0, []) → c
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c
F18_IN(.(z0, z1)) → c
F150_IN(z0, z1, z2, []) → c
F13_IN(z0) → c

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

POL(.(x₁, x₂)) = [2] + x₂   
POL(F128_IN(x₁, x₂, x₃)) = 0   
POL(F13_IN(x₁)) = [2]   
POL(F149_IN(x₁, x₂, x₃, x₄)) = [1] + x₄   
POL(F150_IN(x₁, x₂, x₃, x₄)) = [1]   
POL(F151_IN(x₁, x₂, x₃, x₄)) = x₄   
POL(F18_IN(x₁)) = [2]   
POL(F1_IN(x₁, x₂)) = x₂   
POL(F24_IN(x₁, x₂)) = [1]   
POL([]) = [2]   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c17(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c23(x₁)) = x₁   
POL(c28(x₁, x₂)) = x₁ + x₂   

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([], []) → f1_out1([])
f1_in(z0, []) → U1(f13_in(z0), z0, [])
f1_in(.(z0, z1), .(z2, z3)) → U2(f149_in(z2, z0, z1, z3), .(z0, z1), .(z2, z3))
U1(f13_out1(z0), z1, []) → f1_out1(z0)
U1(f13_out3(z0), z1, []) → f1_out1(z0)
U2(f149_out1(z0), .(z1, z2), .(z3, z4)) → f1_out1(z0)
U2(f149_out2(z0), .(z1, z2), .(z3, z4)) → f1_out1(z0)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, []), z1) → f24_out1(.(z0, .(z1, [])))
f24_in(.(z0, .(z1, [])), z2) → f24_out1(.(z1, .(z0, .(z2, []))))
f24_in(.(z0, .(z1, .(z2, []))), z3) → f24_out1(.(z2, .(z1, .(z0, .(z3, [])))))
f24_in(.(z0, .(z1, .(z2, .(z3, [])))), z4) → f24_out1(.(z3, .(z2, .(z1, .(z0, .(z4, []))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, []))))), z5) → f24_out1(.(z4, .(z3, .(z2, .(z1, .(z0, .(z5, [])))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, [])))))), z6) → f24_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z6, []))))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → U3(f128_in(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8)
U3(f128_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))), z9) → f24_out1(z0)
f128_in([], z0, z1) → f128_out1(.(z0, z1))
f128_in(.(z0, z1), z2, z3) → U4(f128_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U4(f128_out1(z0), .(z1, z2), z3, z4) → f128_out1(z0)
f18_in(.(z0, z1)) → U5(f24_in(z1, z0), .(z0, z1))
U5(f24_out1(z0), .(z1, z2)) → f18_out1(z0)
f150_in(z0, z1, z2, []) → U6(f24_in(.(z1, z2), z0), z0, z1, z2, [])
U6(f24_out1(z0), z1, z2, z3, []) → f150_out1(z0)
f151_in(z0, z1, z2, .(z3, z4)) → U7(f1_in(.(z3, .(z0, .(z1, z2))), z4), z0, z1, z2, .(z3, z4))
U7(f1_out1(z0), z1, z2, z3, .(z4, z5)) → f151_out1(z0)
f13_in(z0) → U8(f18_in(z0), f19_in(z0), z0)
U8(f18_out1(z0), z1, z2) → f13_out1(z0)
U8(z0, f19_out2(z1), z2) → f13_out3(z1)
f149_in(z0, z1, z2, z3) → U9(f150_in(z0, z1, z2, z3), f151_in(z0, z1, z2, z3), z0, z1, z2, z3)
U9(f150_out1(z0), z1, z2, z3, z4, z5) → f149_out1(z0)
U9(z0, f151_out1(z1), z2, z3, z4, z5) → f149_out2(z1)

Tuples:

F1_IN(z0, []) → c(F13_IN(z0))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c(F128_IN(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))))
F18_IN(.(z0, z1)) → c(F24_IN(z1, z0))
F150_IN(z0, z1, z2, []) → c(F24_IN(.(z1, z2), z0))
F13_IN(z0) → c(F18_IN(z0))
F1_IN(.(z0, z1), .(z2, z3)) → c2(F149_IN(z2, z0, z1, z3))
F128_IN(.(z0, z1), z2, z3) → c17(F128_IN(z1, z0, .(z2, z3)))
F151_IN(z0, z1, z2, .(z3, z4)) → c23(F1_IN(.(z3, .(z0, .(z1, z2))), z4))
F149_IN(z0, z1, z2, z3) → c28(F150_IN(z0, z1, z2, z3), F151_IN(z0, z1, z2, z3))
F1_IN(z0, []) → c
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c
F18_IN(.(z0, z1)) → c
F150_IN(z0, z1, z2, []) → c
F13_IN(z0) → c

S tuples:

F1_IN(z0, []) → c(F13_IN(z0))
F150_IN(z0, z1, z2, []) → c(F24_IN(.(z1, z2), z0))
F128_IN(.(z0, z1), z2, z3) → c17(F128_IN(z1, z0, .(z2, z3)))
F149_IN(z0, z1, z2, z3) → c28(F150_IN(z0, z1, z2, z3), F151_IN(z0, z1, z2, z3))

K tuples:

F13_IN(z0) → c(F18_IN(z0))
F1_IN(z0, []) → c
F13_IN(z0) → c
F18_IN(.(z0, z1)) → c(F24_IN(z1, z0))
F18_IN(.(z0, z1)) → c
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c(F128_IN(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))))
F1_IN(.(z0, z1), .(z2, z3)) → c2(F149_IN(z2, z0, z1, z3))
F151_IN(z0, z1, z2, .(z3, z4)) → c23(F1_IN(.(z3, .(z0, .(z1, z2))), z4))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c
F150_IN(z0, z1, z2, []) → c

Defined Rule Symbols:

f1_in, U1, U2, f24_in, U3, f128_in, U4, f18_in, U5, f150_in, U6, f151_in, U7, f13_in, U8, f149_in, U9

Defined Pair Symbols:

F1_IN, F24_IN, F18_IN, F150_IN, F13_IN, F128_IN, F151_IN, F149_IN

Compound Symbols:

c, c2, c17, c23, c28, c

(29) CdtKnowledgeProof (EQUIVALENT transformation)

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

F1_IN(z0, []) → c(F13_IN(z0))
F149_IN(z0, z1, z2, z3) → c28(F150_IN(z0, z1, z2, z3), F151_IN(z0, z1, z2, z3))
F13_IN(z0) → c(F18_IN(z0))
F13_IN(z0) → c
F150_IN(z0, z1, z2, []) → c(F24_IN(.(z1, z2), z0))
F151_IN(z0, z1, z2, .(z3, z4)) → c23(F1_IN(.(z3, .(z0, .(z1, z2))), z4))
F150_IN(z0, z1, z2, []) → c
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c(F128_IN(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([], []) → f1_out1([])
f1_in(z0, []) → U1(f13_in(z0), z0, [])
f1_in(.(z0, z1), .(z2, z3)) → U2(f149_in(z2, z0, z1, z3), .(z0, z1), .(z2, z3))
U1(f13_out1(z0), z1, []) → f1_out1(z0)
U1(f13_out3(z0), z1, []) → f1_out1(z0)
U2(f149_out1(z0), .(z1, z2), .(z3, z4)) → f1_out1(z0)
U2(f149_out2(z0), .(z1, z2), .(z3, z4)) → f1_out1(z0)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, []), z1) → f24_out1(.(z0, .(z1, [])))
f24_in(.(z0, .(z1, [])), z2) → f24_out1(.(z1, .(z0, .(z2, []))))
f24_in(.(z0, .(z1, .(z2, []))), z3) → f24_out1(.(z2, .(z1, .(z0, .(z3, [])))))
f24_in(.(z0, .(z1, .(z2, .(z3, [])))), z4) → f24_out1(.(z3, .(z2, .(z1, .(z0, .(z4, []))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, []))))), z5) → f24_out1(.(z4, .(z3, .(z2, .(z1, .(z0, .(z5, [])))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, [])))))), z6) → f24_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z6, []))))))))
f24_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → U3(f128_in(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8)
U3(f128_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))), z9) → f24_out1(z0)
f128_in([], z0, z1) → f128_out1(.(z0, z1))
f128_in(.(z0, z1), z2, z3) → U4(f128_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U4(f128_out1(z0), .(z1, z2), z3, z4) → f128_out1(z0)
f18_in(.(z0, z1)) → U5(f24_in(z1, z0), .(z0, z1))
U5(f24_out1(z0), .(z1, z2)) → f18_out1(z0)
f150_in(z0, z1, z2, []) → U6(f24_in(.(z1, z2), z0), z0, z1, z2, [])
U6(f24_out1(z0), z1, z2, z3, []) → f150_out1(z0)
f151_in(z0, z1, z2, .(z3, z4)) → U7(f1_in(.(z3, .(z0, .(z1, z2))), z4), z0, z1, z2, .(z3, z4))
U7(f1_out1(z0), z1, z2, z3, .(z4, z5)) → f151_out1(z0)
f13_in(z0) → U8(f18_in(z0), f19_in(z0), z0)
U8(f18_out1(z0), z1, z2) → f13_out1(z0)
U8(z0, f19_out2(z1), z2) → f13_out3(z1)
f149_in(z0, z1, z2, z3) → U9(f150_in(z0, z1, z2, z3), f151_in(z0, z1, z2, z3), z0, z1, z2, z3)
U9(f150_out1(z0), z1, z2, z3, z4, z5) → f149_out1(z0)
U9(z0, f151_out1(z1), z2, z3, z4, z5) → f149_out2(z1)

Tuples:

F1_IN(z0, []) → c(F13_IN(z0))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c(F128_IN(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))))
F18_IN(.(z0, z1)) → c(F24_IN(z1, z0))
F150_IN(z0, z1, z2, []) → c(F24_IN(.(z1, z2), z0))
F13_IN(z0) → c(F18_IN(z0))
F1_IN(.(z0, z1), .(z2, z3)) → c2(F149_IN(z2, z0, z1, z3))
F128_IN(.(z0, z1), z2, z3) → c17(F128_IN(z1, z0, .(z2, z3)))
F151_IN(z0, z1, z2, .(z3, z4)) → c23(F1_IN(.(z3, .(z0, .(z1, z2))), z4))
F149_IN(z0, z1, z2, z3) → c28(F150_IN(z0, z1, z2, z3), F151_IN(z0, z1, z2, z3))
F1_IN(z0, []) → c
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c
F18_IN(.(z0, z1)) → c
F150_IN(z0, z1, z2, []) → c
F13_IN(z0) → c

S tuples:

F128_IN(.(z0, z1), z2, z3) → c17(F128_IN(z1, z0, .(z2, z3)))

K tuples:

F13_IN(z0) → c(F18_IN(z0))
F1_IN(z0, []) → c
F13_IN(z0) → c
F18_IN(.(z0, z1)) → c(F24_IN(z1, z0))
F18_IN(.(z0, z1)) → c
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c(F128_IN(z7, z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, .(z8, [])))))))))
F1_IN(.(z0, z1), .(z2, z3)) → c2(F149_IN(z2, z0, z1, z3))
F151_IN(z0, z1, z2, .(z3, z4)) → c23(F1_IN(.(z3, .(z0, .(z1, z2))), z4))
F24_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, z7))))))), z8) → c
F150_IN(z0, z1, z2, []) → c
F1_IN(z0, []) → c(F13_IN(z0))
F149_IN(z0, z1, z2, z3) → c28(F150_IN(z0, z1, z2, z3), F151_IN(z0, z1, z2, z3))
F150_IN(z0, z1, z2, []) → c(F24_IN(.(z1, z2), z0))

Defined Rule Symbols:

f1_in, U1, U2, f24_in, U3, f128_in, U4, f18_in, U5, f150_in, U6, f151_in, U7, f13_in, U8, f149_in, U9

Defined Pair Symbols:

F1_IN, F24_IN, F18_IN, F150_IN, F13_IN, F128_IN, F151_IN, F149_IN

Compound Symbols:

c, c2, c17, c23, c28, c