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

(0) Obligation:

Clauses:

transpose(A, B) :- transpose_aux(A, [], B).
transpose_aux(.(R, Rs), X1, .(C, Cs)) :- ','(row2col(R, .(C, Cs), Cols1, [], Accm), transpose_aux(Rs, Accm, Cols1)).
transpose_aux([], X, X).
row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), A, B) :- row2col(Xs, Cols, Cols1, .([], A), B).
row2col([], [], [], A, A).

Query: transpose(g,a)

(1) LPReorderTransformerProof (EQUIVALENT transformation)

Reordered facts before rules in definite LP [PROLOG].

(2) Obligation:

Clauses:

transpose_aux([], X, X).
row2col([], [], [], A, A).
transpose(A, B) :- transpose_aux(A, [], B).
transpose_aux(.(R, Rs), X1, .(C, Cs)) :- ','(row2col(R, .(C, Cs), Cols1, [], Accm), transpose_aux(Rs, Accm, Cols1)).
row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), A, B) :- row2col(Xs, Cols, Cols1, .([], A), B).

Query: transpose(g,a)

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

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: transpose(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: transpose(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: transpose_aux(T8, [], T10)\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: transpose_aux(T8, [], T10), SCOPE: 2, CLAUSE: 0 | transpose_aux(T8, [], T10), SCOPE: 2, CLAUSE: 3\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: true | transpose_aux([], [], T10), SCOPE: 2, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: transpose_aux(T8, [], T10), SCOPE: 2, CLAUSE: 3\n\nT8 is ground\nX14 is free\ntranspose_aux(T8, [], T10) !=? transpose_aux([], X14, X14)", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: transpose_aux([], [], T10), SCOPE: 2, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(row2col(T19, .(T23, T24), X37, [], X38), transpose_aux(T20, X38, X37))\n\nT19 is ground\nT20 is ground\nX37 is free\nX38 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: row2col(T19, .(T23, T24), X37, [], X38)\n\nT19 is ground\nX37 is free\nX38 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: transpose_aux(T20, T26, T25)\n\nT20 is ground\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: row2col(T19, .(T23, T24), X37, [], X38), SCOPE: 3, CLAUSE: 1 | row2col(T19, .(T23, T24), X37, [], X38), SCOPE: 3, CLAUSE: 4\n\nT19 is ground\nX37 is free\nX38 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: row2col(T19, .(T23, T24), X37, [], X38), SCOPE: 3, CLAUSE: 4\n\nT19 is ground\nX37 is free\nX38 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: row2col(T36, T39, X69, .([], []), X70)\n\nT36 is ground\nX69 is free\nX70 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: row2col(T36, T39, X69, .([], []), X70), SCOPE: 4, CLAUSE: 1 | row2col(T36, T39, X69, .([], []), X70), SCOPE: 4, CLAUSE: 4\n\nT36 is ground\nX69 is free\nX70 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: true | row2col([], T39, X69, .([], []), X70), SCOPE: 4, CLAUSE: 4\n\nX69 is free\nX70 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: row2col(T36, T39, X69, .([], []), X70), SCOPE: 4, CLAUSE: 4\n\nT36 is ground\nX69 is free\nX70 is free\nX75 is free\nrow2col(T36, T39, X69, .([], []), X70) !=? row2col([], [], [], X75, X75)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: row2col([], T39, X69, .([], []), X70), SCOPE: 4, CLAUSE: 4\n\nX69 is free\nX70 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: row2col(T49, T52, X108, .([], .([], [])), X109)\n\nT49 is ground\nX108 is free\nX109 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: row2col(T49, T52, X108, .([], .([], [])), X109), SCOPE: 5, CLAUSE: 1 | row2col(T49, T52, X108, .([], .([], [])), X109), SCOPE: 5, CLAUSE: 4\n\nT49 is ground\nX108 is free\nX109 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: true | row2col([], T52, X108, .([], .([], [])), X109), SCOPE: 5, CLAUSE: 4\n\nX108 is free\nX109 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: row2col(T49, T52, X108, .([], .([], [])), X109), SCOPE: 5, CLAUSE: 4\n\nT49 is ground\nX108 is free\nX109 is free\nX114 is free\nrow2col(T49, T52, X108, .([], .([], [])), X109) !=? row2col([], [], [], X114, X114)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: row2col([], T52, X108, .([], .([], [])), X109), SCOPE: 5, CLAUSE: 4\n\nX108 is free\nX109 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: row2col(T62, T65, X147, .([], .([], .([], []))), X148)\n\nT62 is ground\nX147 is free\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: row2col(T62, T65, X147, .([], .([], .([], []))), X148), SCOPE: 6, CLAUSE: 1 | row2col(T62, T65, X147, .([], .([], .([], []))), X148), SCOPE: 6, CLAUSE: 4\n\nT62 is ground\nX147 is free\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: true | row2col([], T65, X147, .([], .([], .([], []))), X148), SCOPE: 6, CLAUSE: 4\n\nX147 is free\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: row2col(T62, T65, X147, .([], .([], .([], []))), X148), SCOPE: 6, CLAUSE: 4\n\nT62 is ground\nX147 is free\nX148 is free\nX153 is free\nrow2col(T62, T65, X147, .([], .([], .([], []))), X148) !=? row2col([], [], [], X153, X153)", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: row2col([], T65, X147, .([], .([], .([], []))), X148), SCOPE: 6, CLAUSE: 4\n\nX147 is free\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: row2col(T75, T78, X186, .([], .([], .([], .([], [])))), X187)\n\nT75 is ground\nX186 is free\nX187 is free", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: row2col(T75, T78, X186, .([], .([], .([], .([], [])))), X187), SCOPE: 7, CLAUSE: 1 | row2col(T75, T78, X186, .([], .([], .([], .([], [])))), X187), SCOPE: 7, CLAUSE: 4\n\nT75 is ground\nX186 is free\nX187 is free", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: true | row2col([], T78, X186, .([], .([], .([], .([], [])))), X187), SCOPE: 7, CLAUSE: 4\n\nX186 is free\nX187 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: row2col(T75, T78, X186, .([], .([], .([], .([], [])))), X187), SCOPE: 7, CLAUSE: 4\n\nT75 is ground\nX186 is free\nX187 is free\nX192 is free\nrow2col(T75, T78, X186, .([], .([], .([], .([], [])))), X187) !=? row2col([], [], [], X192, X192)", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: row2col([], T78, X186, .([], .([], .([], .([], [])))), X187), SCOPE: 7, CLAUSE: 4\n\nX186 is free\nX187 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: row2col(T88, T91, X225, .([], .([], .([], .([], .([], []))))), X226)\n\nT88 is ground\nX225 is free\nX226 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: row2col(T88, T91, X225, .([], .([], .([], .([], .([], []))))), X226), SCOPE: 8, CLAUSE: 1 | row2col(T88, T91, X225, .([], .([], .([], .([], .([], []))))), X226), SCOPE: 8, CLAUSE: 4\n\nT88 is ground\nX225 is free\nX226 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: true | row2col([], T91, X225, .([], .([], .([], .([], .([], []))))), X226), SCOPE: 8, CLAUSE: 4\n\nX225 is free\nX226 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: row2col(T88, T91, X225, .([], .([], .([], .([], .([], []))))), X226), SCOPE: 8, CLAUSE: 4\n\nT88 is ground\nX225 is free\nX226 is free\nX231 is free\nrow2col(T88, T91, X225, .([], .([], .([], .([], .([], []))))), X226) !=? row2col([], [], [], X231, X231)", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: row2col([], T91, X225, .([], .([], .([], .([], .([], []))))), X226), SCOPE: 8, CLAUSE: 4\n\nX225 is free\nX226 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: row2col(T101, T104, X264, .([], .([], .([], .([], .([], .([], [])))))), X265)\n\nT101 is ground\nX264 is free\nX265 is free", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: row2col(T101, T104, X264, .([], .([], .([], .([], .([], .([], [])))))), X265), SCOPE: 9, CLAUSE: 1 | row2col(T101, T104, X264, .([], .([], .([], .([], .([], .([], [])))))), X265), SCOPE: 9, CLAUSE: 4\n\nT101 is ground\nX264 is free\nX265 is free", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: true | row2col([], T104, X264, .([], .([], .([], .([], .([], .([], [])))))), X265), SCOPE: 9, CLAUSE: 4\n\nX264 is free\nX265 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: row2col(T101, T104, X264, .([], .([], .([], .([], .([], .([], [])))))), X265), SCOPE: 9, CLAUSE: 4\n\nT101 is ground\nX264 is free\nX265 is free\nX270 is free\nrow2col(T101, T104, X264, .([], .([], .([], .([], .([], .([], [])))))), X265) !=? row2col([], [], [], X270, X270)", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: row2col([], T104, X264, .([], .([], .([], .([], .([], .([], [])))))), X265), SCOPE: 9, CLAUSE: 4\n\nX264 is free\nX265 is free", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: row2col(T114, T117, X303, .([], .([], .([], .([], .([], .([], .([], []))))))), X304)\n\nT114 is ground\nX303 is free\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: row2col(T114, T117, X303, .([], .([], .([], .([], .([], .([], .([], []))))))), X304), SCOPE: 10, CLAUSE: 1 | row2col(T114, T117, X303, .([], .([], .([], .([], .([], .([], .([], []))))))), X304), SCOPE: 10, CLAUSE: 4\n\nT114 is ground\nX303 is free\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: true | row2col([], T117, X303, .([], .([], .([], .([], .([], .([], .([], []))))))), X304), SCOPE: 10, CLAUSE: 4\n\nX303 is free\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: row2col(T114, T117, X303, .([], .([], .([], .([], .([], .([], .([], []))))))), X304), SCOPE: 10, CLAUSE: 4\n\nT114 is ground\nX303 is free\nX304 is free\nX309 is free\nrow2col(T114, T117, X303, .([], .([], .([], .([], .([], .([], .([], []))))))), X304) !=? row2col([], [], [], X309, X309)", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: row2col([], T117, X303, .([], .([], .([], .([], .([], .([], .([], []))))))), X304), SCOPE: 10, CLAUSE: 4\n\nX303 is free\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: row2col(T127, T130, X342, .([], .([], .([], .([], .([], .([], .([], .([], [])))))))), X343)\n\nT127 is ground\nX342 is free\nX343 is free", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: row2col(T127, T130, X342, .([], T131), X343)\n\nT127 is ground\nT131 is ground\nX342 is free\nX343 is free", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: row2col(T127, T130, X342, .([], T131), X343), SCOPE: 11, CLAUSE: 1 | row2col(T127, T130, X342, .([], T131), X343), SCOPE: 11, CLAUSE: 4\n\nT127 is ground\nT131 is ground\nX342 is free\nX343 is free", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: true | row2col([], T130, X342, .([], T136), X343), SCOPE: 11, CLAUSE: 4\n\nT136 is ground\nX342 is free\nX343 is free", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: row2col(T127, T130, X342, .([], T131), X343), SCOPE: 11, CLAUSE: 4\n\nT127 is ground\nT131 is ground\nX342 is free\nX343 is free\nX350 is free\nrow2col(T127, T130, X342, .([], T131), X343) !=? row2col([], [], [], X350, X350)", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: row2col([], T130, X342, .([], T136), X343), SCOPE: 11, CLAUSE: 4\n\nT136 is ground\nX342 is free\nX343 is free", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: row2col(T148, T152, X383, .([], .([], T151)), X384)\n\nT148 is ground\nT151 is ground\nX383 is free\nX384 is free", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: transpose_aux(T20, T26, T25), SCOPE: 12, CLAUSE: 0 | transpose_aux(T20, T26, T25), SCOPE: 12, CLAUSE: 3\n\nT20 is ground\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: true | transpose_aux([], T159, T25), SCOPE: 12, CLAUSE: 3\n\nT159 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: transpose_aux(T20, T26, T25), SCOPE: 12, CLAUSE: 3\n\nT20 is ground\nT26 is ground\nX391 is free\ntranspose_aux(T20, T26, T25) !=? transpose_aux([], X391, X391)", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: transpose_aux([], T159, T25), SCOPE: 12, CLAUSE: 3\n\nT159 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: ','(row2col(T170, .(T175, T176), X414, [], X415), transpose_aux(T171, X415, X414))\n\nT170 is ground\nT171 is ground\nX414 is free\nX415 is free", 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="ONLY EVAL with clause\ntranspose(X8, X9) :- transpose_aux(X8, [], X9).\nand substitutionT1 -> T8,\nX8 -> T8,\nT2 -> T10,\nX9 -> T10,\nT9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 160 [arrowhead = none ];
160 -> 6;

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

162 [label="EVAL with clause\ntranspose_aux([], X14, X14).\nand substitutionT8 -> [],\nX14 -> [],\nT10 -> []", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 162 [arrowhead = none ];
162 -> 13;

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

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

165 [label="EVAL with clause\ntranspose_aux(.(X32, X33), X34, .(X35, X36)) :- ','(row2col(X32, .(X35, X36), X37, [], X38), transpose_aux(X33, X38, X37)).\nand substitutionX32 -> T19,\nX33 -> T20,\nT8 -> .(T19, T20),\nX34 -> [],\nX35 -> T23,\nX36 -> T24,\nT10 -> .(T23, T24),\nT21 -> T23,\nT22 -> T24", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 165 [arrowhead = none ];
165 -> 19;

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

167 [label="BACKTRACK\nfor clause: transpose_aux(.(R, Rs), X1, .(C, Cs)) :- ','(row2col(R, .(C, Cs), Cols1, [], Accm), transpose_aux(Rs, Accm, Cols1))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 167 [arrowhead = none ];
167 -> 16;

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

169 [label="SPLIT 2\nnew knowledge:\nT19 is ground\nT26 is ground\nreplacements:X37 -> T25,\nX38 -> T26", fontsize=14, style = filled, fillcolor = violet];
19 -> 169 [arrowhead = none ];
169 -> 24;

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

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

172 [label="BACKTRACK\nfor clause: row2col([], [], [], A, A)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 172 [arrowhead = none ];
172 -> 28;

173 [label="EVAL with clause\nrow2col(.(X62, X63), .(.(X62, X64), X65), .(X64, X66), X67, X68) :- row2col(X63, X65, X66, .([], X67), X68).\nand substitutionX62 -> T35,\nX63 -> T36,\nT19 -> .(T35, T36),\nX64 -> T37,\nT23 -> .(T35, T37),\nT24 -> T39,\nX65 -> T39,\nX66 -> X69,\nX37 -> .(T37, X69),\nX67 -> [],\nX38 -> X70,\nX68 -> X70,\nT38 -> T39", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 173 [arrowhead = none ];
173 -> 29;

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

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

176 [label="EVAL with clause\nrow2col([], [], [], X75, X75).\nand substitutionT36 -> [],\nT39 -> [],\nX69 -> [],\nX75 -> .([], []),\nX70 -> .([], [])", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 176 [arrowhead = none ];
176 -> 33;

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

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

179 [label="EVAL with clause\nrow2col(.(X101, X102), .(.(X101, X103), X104), .(X103, X105), X106, X107) :- row2col(X102, X104, X105, .([], X106), X107).\nand substitutionX101 -> T48,\nX102 -> T49,\nT36 -> .(T48, T49),\nX103 -> T50,\nX104 -> T52,\nT39 -> .(.(T48, T50), T52),\nX105 -> X108,\nX69 -> .(T50, X108),\nX106 -> .([], []),\nX70 -> X109,\nX107 -> X109,\nT51 -> T52", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 179 [arrowhead = none ];
179 -> 43;

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

181 [label="BACKTRACK\nfor clause: row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), A, B) :- row2col(Xs, Cols, Cols1, .([], A), B)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 181 [arrowhead = none ];
181 -> 38;

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

183 [label="EVAL with clause\nrow2col([], [], [], X114, X114).\nand substitutionT49 -> [],\nT52 -> [],\nX108 -> [],\nX114 -> .([], .([], [])),\nX109 -> .([], .([], []))", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 183 [arrowhead = none ];
183 -> 49;

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

185 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 185 [arrowhead = none ];
185 -> 51;

186 [label="EVAL with clause\nrow2col(.(X140, X141), .(.(X140, X142), X143), .(X142, X144), X145, X146) :- row2col(X141, X143, X144, .([], X145), X146).\nand substitutionX140 -> T61,\nX141 -> T62,\nT49 -> .(T61, T62),\nX142 -> T63,\nX143 -> T65,\nT52 -> .(.(T61, T63), T65),\nX144 -> X147,\nX108 -> .(T63, X147),\nX145 -> .([], .([], [])),\nX109 -> X148,\nX146 -> X148,\nT64 -> T65", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 186 [arrowhead = none ];
186 -> 57;

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

188 [label="BACKTRACK\nfor clause: row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), A, B) :- row2col(Xs, Cols, Cols1, .([], A), B)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 188 [arrowhead = none ];
188 -> 53;

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

190 [label="EVAL with clause\nrow2col([], [], [], X153, X153).\nand substitutionT62 -> [],\nT65 -> [],\nX147 -> [],\nX153 -> .([], .([], .([], []))),\nX148 -> .([], .([], .([], [])))", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 190 [arrowhead = none ];
190 -> 63;

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

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

193 [label="EVAL with clause\nrow2col(.(X179, X180), .(.(X179, X181), X182), .(X181, X183), X184, X185) :- row2col(X180, X182, X183, .([], X184), X185).\nand substitutionX179 -> T74,\nX180 -> T75,\nT62 -> .(T74, T75),\nX181 -> T76,\nX182 -> T78,\nT65 -> .(.(T74, T76), T78),\nX183 -> X186,\nX147 -> .(T76, X186),\nX184 -> .([], .([], .([], []))),\nX148 -> X187,\nX185 -> X187,\nT77 -> T78", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 193 [arrowhead = none ];
193 -> 71;

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

195 [label="BACKTRACK\nfor clause: row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), A, B) :- row2col(Xs, Cols, Cols1, .([], A), B)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 195 [arrowhead = none ];
195 -> 67;

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

197 [label="EVAL with clause\nrow2col([], [], [], X192, X192).\nand substitutionT75 -> [],\nT78 -> [],\nX186 -> [],\nX192 -> .([], .([], .([], .([], [])))),\nX187 -> .([], .([], .([], .([], []))))", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 197 [arrowhead = none ];
197 -> 76;

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

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

200 [label="EVAL with clause\nrow2col(.(X218, X219), .(.(X218, X220), X221), .(X220, X222), X223, X224) :- row2col(X219, X221, X222, .([], X223), X224).\nand substitutionX218 -> T87,\nX219 -> T88,\nT75 -> .(T87, T88),\nX220 -> T89,\nX221 -> T91,\nT78 -> .(.(T87, T89), T91),\nX222 -> X225,\nX186 -> .(T89, X225),\nX223 -> .([], .([], .([], .([], [])))),\nX187 -> X226,\nX224 -> X226,\nT90 -> T91", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 200 [arrowhead = none ];
200 -> 85;

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

202 [label="BACKTRACK\nfor clause: row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), A, B) :- row2col(Xs, Cols, Cols1, .([], A), B)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
79 -> 202 [arrowhead = none ];
202 -> 80;

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

204 [label="EVAL with clause\nrow2col([], [], [], X231, X231).\nand substitutionT88 -> [],\nT91 -> [],\nX225 -> [],\nX231 -> .([], .([], .([], .([], .([], []))))),\nX226 -> .([], .([], .([], .([], .([], [])))))", fontsize=14, style = filled, fillcolor = lightblue];
89 -> 204 [arrowhead = none ];
204 -> 90;

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

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

207 [label="EVAL with clause\nrow2col(.(X257, X258), .(.(X257, X259), X260), .(X259, X261), X262, X263) :- row2col(X258, X260, X261, .([], X262), X263).\nand substitutionX257 -> T100,\nX258 -> T101,\nT88 -> .(T100, T101),\nX259 -> T102,\nX260 -> T104,\nT91 -> .(.(T100, T102), T104),\nX261 -> X264,\nX225 -> .(T102, X264),\nX262 -> .([], .([], .([], .([], .([], []))))),\nX226 -> X265,\nX263 -> X265,\nT103 -> T104", fontsize=14, style = filled, fillcolor = lightblue];
92 -> 207 [arrowhead = none ];
207 -> 99;

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

209 [label="BACKTRACK\nfor clause: row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), A, B) :- row2col(Xs, Cols, Cols1, .([], A), B)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
93 -> 209 [arrowhead = none ];
209 -> 94;

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

211 [label="EVAL with clause\nrow2col([], [], [], X270, X270).\nand substitutionT101 -> [],\nT104 -> [],\nX264 -> [],\nX270 -> .([], .([], .([], .([], .([], .([], [])))))),\nX265 -> .([], .([], .([], .([], .([], .([], []))))))", fontsize=14, style = filled, fillcolor = lightblue];
102 -> 211 [arrowhead = none ];
211 -> 104;

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

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

214 [label="EVAL with clause\nrow2col(.(X296, X297), .(.(X296, X298), X299), .(X298, X300), X301, X302) :- row2col(X297, X299, X300, .([], X301), X302).\nand substitutionX296 -> T113,\nX297 -> T114,\nT101 -> .(T113, T114),\nX298 -> T115,\nX299 -> T117,\nT104 -> .(.(T113, T115), T117),\nX300 -> X303,\nX264 -> .(T115, X303),\nX301 -> .([], .([], .([], .([], .([], .([], [])))))),\nX265 -> X304,\nX302 -> X304,\nT116 -> T117", fontsize=14, style = filled, fillcolor = lightblue];
106 -> 214 [arrowhead = none ];
214 -> 113;

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

216 [label="BACKTRACK\nfor clause: row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), A, B) :- row2col(Xs, Cols, Cols1, .([], A), B)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
107 -> 216 [arrowhead = none ];
216 -> 108;

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

218 [label="EVAL with clause\nrow2col([], [], [], X309, X309).\nand substitutionT114 -> [],\nT117 -> [],\nX303 -> [],\nX309 -> .([], .([], .([], .([], .([], .([], .([], []))))))),\nX304 -> .([], .([], .([], .([], .([], .([], .([], [])))))))", fontsize=14, style = filled, fillcolor = lightblue];
117 -> 218 [arrowhead = none ];
218 -> 118;

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

220 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
118 -> 220 [arrowhead = none ];
220 -> 120;

221 [label="EVAL with clause\nrow2col(.(X335, X336), .(.(X335, X337), X338), .(X337, X339), X340, X341) :- row2col(X336, X338, X339, .([], X340), X341).\nand substitutionX335 -> T126,\nX336 -> T127,\nT114 -> .(T126, T127),\nX337 -> T128,\nX338 -> T130,\nT117 -> .(.(T126, T128), T130),\nX339 -> X342,\nX303 -> .(T128, X342),\nX340 -> .([], .([], .([], .([], .([], .([], .([], []))))))),\nX304 -> X343,\nX341 -> X343,\nT129 -> T130", fontsize=14, style = filled, fillcolor = lightblue];
119 -> 221 [arrowhead = none ];
221 -> 127;

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

223 [label="BACKTRACK\nfor clause: row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), A, B) :- row2col(Xs, Cols, Cols1, .([], A), B)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
120 -> 223 [arrowhead = none ];
223 -> 122;

224 [label="GENERALIZATION\nT131 <-- .([], .([], .([], .([], .([], .([], .([], [])))))))\n\nNew Knowledge:\nT131 is ground", fontsize=14, style = filled, fillcolor = violet];
127 -> 224 [arrowhead = none ];
224 -> 131;

225 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
131 -> 225 [arrowhead = none ];
225 -> 133;

226 [label="EVAL with clause\nrow2col([], [], [], X350, X350).\nand substitutionT127 -> [],\nT130 -> [],\nX342 -> [],\nT131 -> T136,\nX350 -> .([], T136),\nX343 -> .([], T136)", fontsize=14, style = filled, fillcolor = lightblue];
133 -> 226 [arrowhead = none ];
226 -> 134;

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

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

229 [label="EVAL with clause\nrow2col(.(X376, X377), .(.(X376, X378), X379), .(X378, X380), X381, X382) :- row2col(X377, X379, X380, .([], X381), X382).\nand substitutionX376 -> T147,\nX377 -> T148,\nT127 -> .(T147, T148),\nX378 -> T149,\nX379 -> T152,\nT130 -> .(.(T147, T149), T152),\nX380 -> X383,\nX342 -> .(T149, X383),\nT131 -> T151,\nX381 -> .([], T151),\nX343 -> X384,\nX382 -> X384,\nT150 -> T152", fontsize=14, style = filled, fillcolor = lightblue];
135 -> 229 [arrowhead = none ];
229 -> 143;

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

231 [label="BACKTRACK\nfor clause: row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), A, B) :- row2col(Xs, Cols, Cols1, .([], A), B)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
136 -> 231 [arrowhead = none ];
231 -> 138;

232 [label="INSTANCE with matching:\nT127 -> T148\nT130 -> T152\nX342 -> X383\nT131 -> .([], T151)\nX343 -> X384", fontsize=14, style = filled, fillcolor = lightgrey];
143 -> 232 [arrowhead = none , style=dashed];
232 -> 131[style=dashed];

233 [label="EVAL with clause\ntranspose_aux([], X391, X391).\nand substitutionT20 -> [],\nT26 -> T159,\nX391 -> T159,\nT25 -> T159", fontsize=14, style = filled, fillcolor = lightblue];
147 -> 233 [arrowhead = none ];
233 -> 148;

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

235 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
148 -> 235 [arrowhead = none ];
235 -> 151;

236 [label="EVAL with clause\ntranspose_aux(.(X409, X410), X411, .(X412, X413)) :- ','(row2col(X409, .(X412, X413), X414, [], X415), transpose_aux(X410, X415, X414)).\nand substitutionX409 -> T170,\nX410 -> T171,\nT20 -> .(T170, T171),\nT26 -> T172,\nX411 -> T172,\nX412 -> T175,\nX413 -> T176,\nT25 -> .(T175, T176),\nT173 -> T175,\nT174 -> T176", fontsize=14, style = filled, fillcolor = lightblue];
149 -> 236 [arrowhead = none ];
236 -> 157;

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

238 [label="BACKTRACK\nfor clause: transpose_aux(.(R, Rs), X1, .(C, Cs)) :- ','(row2col(R, .(C, Cs), Cols1, [], Accm), transpose_aux(Rs, Accm, Cols1))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
151 -> 238 [arrowhead = none ];
238 -> 152;

239 [label="INSTANCE with matching:\nT19 -> T170\nT23 -> T175\nT24 -> T176\nX37 -> X414\nX38 -> X415\nT20 -> T171", fontsize=14, style = filled, fillcolor = lightgrey];
157 -> 239 [arrowhead = none , style=dashed];
239 -> 19[style=dashed];

}

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, z1)) → U1(f19_in(z0, z1), .(z0, z1))
U1(f19_out1(z0), .(z1, z2)) → f1_out1
f131_in([], z0) → f131_out1(.([], z0))
f131_in(.(z0, z1), z2) → U2(f131_in(z1, .([], z2)), .(z0, z1), z2)
U2(f131_out1(z0), .(z1, z2), z3) → f131_out1(z0)
f23_in(.(z0, [])) → f23_out1(.([], []))
f23_in(.(z0, .(z1, []))) → f23_out1(.([], .([], [])))
f23_in(.(z0, .(z1, .(z2, [])))) → f23_out1(.([], .([], .([], []))))
f23_in(.(z0, .(z1, .(z2, .(z3, []))))) → f23_out1(.([], .([], .([], .([], [])))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f23_out1(.([], .([], .([], .([], .([], []))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f23_out1(.([], .([], .([], .([], .([], .([], [])))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f23_out1(.([], .([], .([], .([], .([], .([], .([], []))))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U3(f131_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U3(f131_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f23_out1(z0)
f24_in([], z0) → f24_out1
f24_in(.(z0, z1), z2) → U4(f19_in(z0, z1), .(z0, z1), z2)
U4(f19_out1(z0), .(z1, z2), z3) → f24_out1
f19_in(z0, z1) → U5(f23_in(z0), z0, z1)
U5(f23_out1(z0), z1, z2) → U6(f24_in(z2, z0), z1, z2, z0)
U6(f24_out1, z0, z1, z2) → f19_out1(z2)

Tuples:

F1_IN(.(z0, z1)) → c1(U1'(f19_in(z0, z1), .(z0, z1)), F19_IN(z0, z1))
F131_IN(.(z0, z1), z2) → c4(U2'(f131_in(z1, .([], z2)), .(z0, z1), z2), F131_IN(z1, .([], z2)))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c13(U3'(f131_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F131_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F24_IN(.(z0, z1), z2) → c16(U4'(f19_in(z0, z1), .(z0, z1), z2), F19_IN(z0, z1))
F19_IN(z0, z1) → c18(U5'(f23_in(z0), z0, z1), F23_IN(z0))
U5'(f23_out1(z0), z1, z2) → c19(U6'(f24_in(z2, z0), z1, z2, z0), F24_IN(z2, z0))

S tuples:

F1_IN(.(z0, z1)) → c1(U1'(f19_in(z0, z1), .(z0, z1)), F19_IN(z0, z1))
F131_IN(.(z0, z1), z2) → c4(U2'(f131_in(z1, .([], z2)), .(z0, z1), z2), F131_IN(z1, .([], z2)))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c13(U3'(f131_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F131_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F24_IN(.(z0, z1), z2) → c16(U4'(f19_in(z0, z1), .(z0, z1), z2), F19_IN(z0, z1))
F19_IN(z0, z1) → c18(U5'(f23_in(z0), z0, z1), F23_IN(z0))
U5'(f23_out1(z0), z1, z2) → c19(U6'(f24_in(z2, z0), z1, z2, z0), F24_IN(z2, z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f131_in, U2, f23_in, U3, f24_in, U4, f19_in, U5, U6

Defined Pair Symbols:

F1_IN, F131_IN, F23_IN, F24_IN, F19_IN, U5'

Compound Symbols:

c1, c4, c13, c16, c18, c19

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

Split RHS of tuples not part of any SCC

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, z1)) → U1(f19_in(z0, z1), .(z0, z1))
U1(f19_out1(z0), .(z1, z2)) → f1_out1
f131_in([], z0) → f131_out1(.([], z0))
f131_in(.(z0, z1), z2) → U2(f131_in(z1, .([], z2)), .(z0, z1), z2)
U2(f131_out1(z0), .(z1, z2), z3) → f131_out1(z0)
f23_in(.(z0, [])) → f23_out1(.([], []))
f23_in(.(z0, .(z1, []))) → f23_out1(.([], .([], [])))
f23_in(.(z0, .(z1, .(z2, [])))) → f23_out1(.([], .([], .([], []))))
f23_in(.(z0, .(z1, .(z2, .(z3, []))))) → f23_out1(.([], .([], .([], .([], [])))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f23_out1(.([], .([], .([], .([], .([], []))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f23_out1(.([], .([], .([], .([], .([], .([], [])))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f23_out1(.([], .([], .([], .([], .([], .([], .([], []))))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U3(f131_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U3(f131_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f23_out1(z0)
f24_in([], z0) → f24_out1
f24_in(.(z0, z1), z2) → U4(f19_in(z0, z1), .(z0, z1), z2)
U4(f19_out1(z0), .(z1, z2), z3) → f24_out1
f19_in(z0, z1) → U5(f23_in(z0), z0, z1)
U5(f23_out1(z0), z1, z2) → U6(f24_in(z2, z0), z1, z2, z0)
U6(f24_out1, z0, z1, z2) → f19_out1(z2)

Tuples:

F131_IN(.(z0, z1), z2) → c4(U2'(f131_in(z1, .([], z2)), .(z0, z1), z2), F131_IN(z1, .([], z2)))
F24_IN(.(z0, z1), z2) → c16(U4'(f19_in(z0, z1), .(z0, z1), z2), F19_IN(z0, z1))
F19_IN(z0, z1) → c18(U5'(f23_in(z0), z0, z1), F23_IN(z0))
U5'(f23_out1(z0), z1, z2) → c19(U6'(f24_in(z2, z0), z1, z2, z0), F24_IN(z2, z0))
F1_IN(.(z0, z1)) → c(U1'(f19_in(z0, z1), .(z0, z1)))
F1_IN(.(z0, z1)) → c(F19_IN(z0, z1))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U3'(f131_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F131_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))

S tuples:

F131_IN(.(z0, z1), z2) → c4(U2'(f131_in(z1, .([], z2)), .(z0, z1), z2), F131_IN(z1, .([], z2)))
F24_IN(.(z0, z1), z2) → c16(U4'(f19_in(z0, z1), .(z0, z1), z2), F19_IN(z0, z1))
F19_IN(z0, z1) → c18(U5'(f23_in(z0), z0, z1), F23_IN(z0))
U5'(f23_out1(z0), z1, z2) → c19(U6'(f24_in(z2, z0), z1, z2, z0), F24_IN(z2, z0))
F1_IN(.(z0, z1)) → c(U1'(f19_in(z0, z1), .(z0, z1)))
F1_IN(.(z0, z1)) → c(F19_IN(z0, z1))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U3'(f131_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F131_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f131_in, U2, f23_in, U3, f24_in, U4, f19_in, U5, U6

Defined Pair Symbols:

F131_IN, F24_IN, F19_IN, U5', F1_IN, F23_IN

Compound Symbols:

c4, c16, c18, c19, c

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

Removed 5 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, z1)) → U1(f19_in(z0, z1), .(z0, z1))
U1(f19_out1(z0), .(z1, z2)) → f1_out1
f131_in([], z0) → f131_out1(.([], z0))
f131_in(.(z0, z1), z2) → U2(f131_in(z1, .([], z2)), .(z0, z1), z2)
U2(f131_out1(z0), .(z1, z2), z3) → f131_out1(z0)
f23_in(.(z0, [])) → f23_out1(.([], []))
f23_in(.(z0, .(z1, []))) → f23_out1(.([], .([], [])))
f23_in(.(z0, .(z1, .(z2, [])))) → f23_out1(.([], .([], .([], []))))
f23_in(.(z0, .(z1, .(z2, .(z3, []))))) → f23_out1(.([], .([], .([], .([], [])))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f23_out1(.([], .([], .([], .([], .([], []))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f23_out1(.([], .([], .([], .([], .([], .([], [])))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f23_out1(.([], .([], .([], .([], .([], .([], .([], []))))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U3(f131_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U3(f131_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f23_out1(z0)
f24_in([], z0) → f24_out1
f24_in(.(z0, z1), z2) → U4(f19_in(z0, z1), .(z0, z1), z2)
U4(f19_out1(z0), .(z1, z2), z3) → f24_out1
f19_in(z0, z1) → U5(f23_in(z0), z0, z1)
U5(f23_out1(z0), z1, z2) → U6(f24_in(z2, z0), z1, z2, z0)
U6(f24_out1, z0, z1, z2) → f19_out1(z2)

Tuples:

F19_IN(z0, z1) → c18(U5'(f23_in(z0), z0, z1), F23_IN(z0))
F1_IN(.(z0, z1)) → c(F19_IN(z0, z1))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F131_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F131_IN(.(z0, z1), z2) → c4(F131_IN(z1, .([], z2)))
F24_IN(.(z0, z1), z2) → c16(F19_IN(z0, z1))
U5'(f23_out1(z0), z1, z2) → c19(F24_IN(z2, z0))
F1_IN(.(z0, z1)) → c
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:

F19_IN(z0, z1) → c18(U5'(f23_in(z0), z0, z1), F23_IN(z0))
F1_IN(.(z0, z1)) → c(F19_IN(z0, z1))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F131_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F131_IN(.(z0, z1), z2) → c4(F131_IN(z1, .([], z2)))
F24_IN(.(z0, z1), z2) → c16(F19_IN(z0, z1))
U5'(f23_out1(z0), z1, z2) → c19(F24_IN(z2, z0))
F1_IN(.(z0, z1)) → c
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

K tuples:none
Defined Rule Symbols:

f1_in, U1, f131_in, U2, f23_in, U3, f24_in, U4, f19_in, U5, U6

Defined Pair Symbols:

F19_IN, F1_IN, F23_IN, F131_IN, F24_IN, U5'

Compound Symbols:

c18, c, c4, c16, c19, c

(9) CdtKnowledgeProof (EQUIVALENT transformation)

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

F1_IN(.(z0, z1)) → c(F19_IN(z0, z1))
F1_IN(.(z0, z1)) → c

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, z1)) → U1(f19_in(z0, z1), .(z0, z1))
U1(f19_out1(z0), .(z1, z2)) → f1_out1
f131_in([], z0) → f131_out1(.([], z0))
f131_in(.(z0, z1), z2) → U2(f131_in(z1, .([], z2)), .(z0, z1), z2)
U2(f131_out1(z0), .(z1, z2), z3) → f131_out1(z0)
f23_in(.(z0, [])) → f23_out1(.([], []))
f23_in(.(z0, .(z1, []))) → f23_out1(.([], .([], [])))
f23_in(.(z0, .(z1, .(z2, [])))) → f23_out1(.([], .([], .([], []))))
f23_in(.(z0, .(z1, .(z2, .(z3, []))))) → f23_out1(.([], .([], .([], .([], [])))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f23_out1(.([], .([], .([], .([], .([], []))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f23_out1(.([], .([], .([], .([], .([], .([], [])))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f23_out1(.([], .([], .([], .([], .([], .([], .([], []))))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U3(f131_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U3(f131_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f23_out1(z0)
f24_in([], z0) → f24_out1
f24_in(.(z0, z1), z2) → U4(f19_in(z0, z1), .(z0, z1), z2)
U4(f19_out1(z0), .(z1, z2), z3) → f24_out1
f19_in(z0, z1) → U5(f23_in(z0), z0, z1)
U5(f23_out1(z0), z1, z2) → U6(f24_in(z2, z0), z1, z2, z0)
U6(f24_out1, z0, z1, z2) → f19_out1(z2)

Tuples:

F19_IN(z0, z1) → c18(U5'(f23_in(z0), z0, z1), F23_IN(z0))
F1_IN(.(z0, z1)) → c(F19_IN(z0, z1))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F131_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F131_IN(.(z0, z1), z2) → c4(F131_IN(z1, .([], z2)))
F24_IN(.(z0, z1), z2) → c16(F19_IN(z0, z1))
U5'(f23_out1(z0), z1, z2) → c19(F24_IN(z2, z0))
F1_IN(.(z0, z1)) → c
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:

F19_IN(z0, z1) → c18(U5'(f23_in(z0), z0, z1), F23_IN(z0))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F131_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F131_IN(.(z0, z1), z2) → c4(F131_IN(z1, .([], z2)))
F24_IN(.(z0, z1), z2) → c16(F19_IN(z0, z1))
U5'(f23_out1(z0), z1, z2) → c19(F24_IN(z2, z0))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

K tuples:

F1_IN(.(z0, z1)) → c(F19_IN(z0, z1))
F1_IN(.(z0, z1)) → c

Defined Rule Symbols:

f1_in, U1, f131_in, U2, f23_in, U3, f24_in, U4, f19_in, U5, U6

Defined Pair Symbols:

F19_IN, F1_IN, F23_IN, F131_IN, F24_IN, U5'

Compound Symbols:

c18, c, c4, c16, c19, c

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

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

F19_IN(z0, z1) → c18(U5'(f23_in(z0), z0, z1), F23_IN(z0))
F24_IN(.(z0, z1), z2) → c16(F19_IN(z0, z1))
U5'(f23_out1(z0), z1, z2) → c19(F24_IN(z2, z0))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

We considered the (Usable) Rules:

f23_in(.(z0, [])) → f23_out1(.([], []))
f23_in(.(z0, .(z1, []))) → f23_out1(.([], .([], [])))
f23_in(.(z0, .(z1, .(z2, [])))) → f23_out1(.([], .([], .([], []))))
f23_in(.(z0, .(z1, .(z2, .(z3, []))))) → f23_out1(.([], .([], .([], .([], [])))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f23_out1(.([], .([], .([], .([], .([], []))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f23_out1(.([], .([], .([], .([], .([], .([], [])))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f23_out1(.([], .([], .([], .([], .([], .([], .([], []))))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U3(f131_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
f131_in([], z0) → f131_out1(.([], z0))
f131_in(.(z0, z1), z2) → U2(f131_in(z1, .([], z2)), .(z0, z1), z2)
U3(f131_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f23_out1(z0)
U2(f131_out1(z0), .(z1, z2), z3) → f131_out1(z0)

And the Tuples:

F19_IN(z0, z1) → c18(U5'(f23_in(z0), z0, z1), F23_IN(z0))
F1_IN(.(z0, z1)) → c(F19_IN(z0, z1))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F131_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F131_IN(.(z0, z1), z2) → c4(F131_IN(z1, .([], z2)))
F24_IN(.(z0, z1), z2) → c16(F19_IN(z0, z1))
U5'(f23_out1(z0), z1, z2) → c19(F24_IN(z2, z0))
F1_IN(.(z0, z1)) → c
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

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

POL(.(x₁, x₂)) = [2] + x₁ + x₂   
POL(F131_IN(x₁, x₂)) = [2] + x₁ + x₂   
POL(F19_IN(x₁, x₂)) = [2] + x₁ + [2]x₂   
POL(F1_IN(x₁)) = [1] + [2]x₁   
POL(F23_IN(x₁)) = x₁   
POL(F24_IN(x₁, x₂)) = [2]x₁   
POL(U2(x₁, x₂, x₃)) = 0   
POL(U3(x₁, x₂)) = 0   
POL(U5'(x₁, x₂, x₃)) = [1] + [2]x₃   
POL([]) = 0   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c16(x₁)) = x₁   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c19(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(f131_in(x₁, x₂)) = 0   
POL(f131_out1(x₁)) = 0   
POL(f23_in(x₁)) = 0   
POL(f23_out1(x₁)) = 0   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, z1)) → U1(f19_in(z0, z1), .(z0, z1))
U1(f19_out1(z0), .(z1, z2)) → f1_out1
f131_in([], z0) → f131_out1(.([], z0))
f131_in(.(z0, z1), z2) → U2(f131_in(z1, .([], z2)), .(z0, z1), z2)
U2(f131_out1(z0), .(z1, z2), z3) → f131_out1(z0)
f23_in(.(z0, [])) → f23_out1(.([], []))
f23_in(.(z0, .(z1, []))) → f23_out1(.([], .([], [])))
f23_in(.(z0, .(z1, .(z2, [])))) → f23_out1(.([], .([], .([], []))))
f23_in(.(z0, .(z1, .(z2, .(z3, []))))) → f23_out1(.([], .([], .([], .([], [])))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f23_out1(.([], .([], .([], .([], .([], []))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f23_out1(.([], .([], .([], .([], .([], .([], [])))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f23_out1(.([], .([], .([], .([], .([], .([], .([], []))))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U3(f131_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U3(f131_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f23_out1(z0)
f24_in([], z0) → f24_out1
f24_in(.(z0, z1), z2) → U4(f19_in(z0, z1), .(z0, z1), z2)
U4(f19_out1(z0), .(z1, z2), z3) → f24_out1
f19_in(z0, z1) → U5(f23_in(z0), z0, z1)
U5(f23_out1(z0), z1, z2) → U6(f24_in(z2, z0), z1, z2, z0)
U6(f24_out1, z0, z1, z2) → f19_out1(z2)

Tuples:

F19_IN(z0, z1) → c18(U5'(f23_in(z0), z0, z1), F23_IN(z0))
F1_IN(.(z0, z1)) → c(F19_IN(z0, z1))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F131_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F131_IN(.(z0, z1), z2) → c4(F131_IN(z1, .([], z2)))
F24_IN(.(z0, z1), z2) → c16(F19_IN(z0, z1))
U5'(f23_out1(z0), z1, z2) → c19(F24_IN(z2, z0))
F1_IN(.(z0, z1)) → c
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:

F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F131_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F131_IN(.(z0, z1), z2) → c4(F131_IN(z1, .([], z2)))

K tuples:

F1_IN(.(z0, z1)) → c(F19_IN(z0, z1))
F1_IN(.(z0, z1)) → c
F19_IN(z0, z1) → c18(U5'(f23_in(z0), z0, z1), F23_IN(z0))
F24_IN(.(z0, z1), z2) → c16(F19_IN(z0, z1))
U5'(f23_out1(z0), z1, z2) → c19(F24_IN(z2, z0))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

Defined Rule Symbols:

f1_in, U1, f131_in, U2, f23_in, U3, f24_in, U4, f19_in, U5, U6

Defined Pair Symbols:

F19_IN, F1_IN, F23_IN, F131_IN, F24_IN, U5'

Compound Symbols:

c18, c, c4, c16, c19, c

(13) CdtKnowledgeProof (EQUIVALENT transformation)

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

F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F131_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, z1)) → U1(f19_in(z0, z1), .(z0, z1))
U1(f19_out1(z0), .(z1, z2)) → f1_out1
f131_in([], z0) → f131_out1(.([], z0))
f131_in(.(z0, z1), z2) → U2(f131_in(z1, .([], z2)), .(z0, z1), z2)
U2(f131_out1(z0), .(z1, z2), z3) → f131_out1(z0)
f23_in(.(z0, [])) → f23_out1(.([], []))
f23_in(.(z0, .(z1, []))) → f23_out1(.([], .([], [])))
f23_in(.(z0, .(z1, .(z2, [])))) → f23_out1(.([], .([], .([], []))))
f23_in(.(z0, .(z1, .(z2, .(z3, []))))) → f23_out1(.([], .([], .([], .([], [])))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f23_out1(.([], .([], .([], .([], .([], []))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f23_out1(.([], .([], .([], .([], .([], .([], [])))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f23_out1(.([], .([], .([], .([], .([], .([], .([], []))))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U3(f131_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U3(f131_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f23_out1(z0)
f24_in([], z0) → f24_out1
f24_in(.(z0, z1), z2) → U4(f19_in(z0, z1), .(z0, z1), z2)
U4(f19_out1(z0), .(z1, z2), z3) → f24_out1
f19_in(z0, z1) → U5(f23_in(z0), z0, z1)
U5(f23_out1(z0), z1, z2) → U6(f24_in(z2, z0), z1, z2, z0)
U6(f24_out1, z0, z1, z2) → f19_out1(z2)

Tuples:

F19_IN(z0, z1) → c18(U5'(f23_in(z0), z0, z1), F23_IN(z0))
F1_IN(.(z0, z1)) → c(F19_IN(z0, z1))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F131_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F131_IN(.(z0, z1), z2) → c4(F131_IN(z1, .([], z2)))
F24_IN(.(z0, z1), z2) → c16(F19_IN(z0, z1))
U5'(f23_out1(z0), z1, z2) → c19(F24_IN(z2, z0))
F1_IN(.(z0, z1)) → c
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:

F131_IN(.(z0, z1), z2) → c4(F131_IN(z1, .([], z2)))

K tuples:

F1_IN(.(z0, z1)) → c(F19_IN(z0, z1))
F1_IN(.(z0, z1)) → c
F19_IN(z0, z1) → c18(U5'(f23_in(z0), z0, z1), F23_IN(z0))
F24_IN(.(z0, z1), z2) → c16(F19_IN(z0, z1))
U5'(f23_out1(z0), z1, z2) → c19(F24_IN(z2, z0))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F131_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))

Defined Rule Symbols:

f1_in, U1, f131_in, U2, f23_in, U3, f24_in, U4, f19_in, U5, U6

Defined Pair Symbols:

F19_IN, F1_IN, F23_IN, F131_IN, F24_IN, U5'

Compound Symbols:

c18, c, c4, c16, c19, c

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

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

F131_IN(.(z0, z1), z2) → c4(F131_IN(z1, .([], z2)))

We considered the (Usable) Rules:

f23_in(.(z0, [])) → f23_out1(.([], []))
f23_in(.(z0, .(z1, []))) → f23_out1(.([], .([], [])))
f23_in(.(z0, .(z1, .(z2, [])))) → f23_out1(.([], .([], .([], []))))
f23_in(.(z0, .(z1, .(z2, .(z3, []))))) → f23_out1(.([], .([], .([], .([], [])))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f23_out1(.([], .([], .([], .([], .([], []))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f23_out1(.([], .([], .([], .([], .([], .([], [])))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f23_out1(.([], .([], .([], .([], .([], .([], .([], []))))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U3(f131_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
f131_in([], z0) → f131_out1(.([], z0))
f131_in(.(z0, z1), z2) → U2(f131_in(z1, .([], z2)), .(z0, z1), z2)
U3(f131_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f23_out1(z0)
U2(f131_out1(z0), .(z1, z2), z3) → f131_out1(z0)

And the Tuples:

F19_IN(z0, z1) → c18(U5'(f23_in(z0), z0, z1), F23_IN(z0))
F1_IN(.(z0, z1)) → c(F19_IN(z0, z1))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F131_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F131_IN(.(z0, z1), z2) → c4(F131_IN(z1, .([], z2)))
F24_IN(.(z0, z1), z2) → c16(F19_IN(z0, z1))
U5'(f23_out1(z0), z1, z2) → c19(F24_IN(z2, z0))
F1_IN(.(z0, z1)) → c
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

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

POL(.(x₁, x₂)) = [2] + x₁ + x₂   
POL(F131_IN(x₁, x₂)) = x₁   
POL(F19_IN(x₁, x₂)) = [1] + x₁ + x₂   
POL(F1_IN(x₁)) = x₁   
POL(F23_IN(x₁)) = x₁   
POL(F24_IN(x₁, x₂)) = x₁   
POL(U2(x₁, x₂, x₃)) = [1]   
POL(U3(x₁, x₂)) = 0   
POL(U5'(x₁, x₂, x₃)) = x₃   
POL([]) = 0   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c16(x₁)) = x₁   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c19(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(f131_in(x₁, x₂)) = [1]   
POL(f131_out1(x₁)) = [1]   
POL(f23_in(x₁)) = 0   
POL(f23_out1(x₁)) = 0   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, z1)) → U1(f19_in(z0, z1), .(z0, z1))
U1(f19_out1(z0), .(z1, z2)) → f1_out1
f131_in([], z0) → f131_out1(.([], z0))
f131_in(.(z0, z1), z2) → U2(f131_in(z1, .([], z2)), .(z0, z1), z2)
U2(f131_out1(z0), .(z1, z2), z3) → f131_out1(z0)
f23_in(.(z0, [])) → f23_out1(.([], []))
f23_in(.(z0, .(z1, []))) → f23_out1(.([], .([], [])))
f23_in(.(z0, .(z1, .(z2, [])))) → f23_out1(.([], .([], .([], []))))
f23_in(.(z0, .(z1, .(z2, .(z3, []))))) → f23_out1(.([], .([], .([], .([], [])))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f23_out1(.([], .([], .([], .([], .([], []))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f23_out1(.([], .([], .([], .([], .([], .([], [])))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f23_out1(.([], .([], .([], .([], .([], .([], .([], []))))))))
f23_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U3(f131_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U3(f131_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f23_out1(z0)
f24_in([], z0) → f24_out1
f24_in(.(z0, z1), z2) → U4(f19_in(z0, z1), .(z0, z1), z2)
U4(f19_out1(z0), .(z1, z2), z3) → f24_out1
f19_in(z0, z1) → U5(f23_in(z0), z0, z1)
U5(f23_out1(z0), z1, z2) → U6(f24_in(z2, z0), z1, z2, z0)
U6(f24_out1, z0, z1, z2) → f19_out1(z2)

Tuples:

F19_IN(z0, z1) → c18(U5'(f23_in(z0), z0, z1), F23_IN(z0))
F1_IN(.(z0, z1)) → c(F19_IN(z0, z1))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F131_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F131_IN(.(z0, z1), z2) → c4(F131_IN(z1, .([], z2)))
F24_IN(.(z0, z1), z2) → c16(F19_IN(z0, z1))
U5'(f23_out1(z0), z1, z2) → c19(F24_IN(z2, z0))
F1_IN(.(z0, z1)) → c
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:none
K tuples:

F1_IN(.(z0, z1)) → c(F19_IN(z0, z1))
F1_IN(.(z0, z1)) → c
F19_IN(z0, z1) → c18(U5'(f23_in(z0), z0, z1), F23_IN(z0))
F24_IN(.(z0, z1), z2) → c16(F19_IN(z0, z1))
U5'(f23_out1(z0), z1, z2) → c19(F24_IN(z2, z0))
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
F23_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F131_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F131_IN(.(z0, z1), z2) → c4(F131_IN(z1, .([], z2)))

Defined Rule Symbols:

f1_in, U1, f131_in, U2, f23_in, U3, f24_in, U4, f19_in, U5, U6

Defined Pair Symbols:

F19_IN, F1_IN, F23_IN, F131_IN, F24_IN, U5'

Compound Symbols:

c18, c, c4, c16, c19, c

(17) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

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

(19) 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: transpose(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: transpose(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: transpose_aux(T5, [], T7)\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: transpose_aux(T5, [], T7), SCOPE: 2, CLAUSE: 0 | transpose_aux(T5, [], T7), SCOPE: 2, CLAUSE: 3\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: true | transpose_aux([], [], T7), SCOPE: 2, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: transpose_aux(T5, [], T7), SCOPE: 2, CLAUSE: 3\n\nT5 is ground\nX8 is free\ntranspose_aux(T5, [], T7) !=? transpose_aux([], X8, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: transpose_aux([], [], T7), SCOPE: 2, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(row2col(T16, .(T20, T21), X31, [], X32), transpose_aux(T17, X32, X31))\n\nT16 is ground\nT17 is ground\nX31 is free\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: row2col(T16, .(T20, T21), X31, [], X32)\n\nT16 is ground\nX31 is free\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: transpose_aux(T17, T23, T22)\n\nT17 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: row2col(T16, .(T20, T21), X31, [], X32), SCOPE: 3, CLAUSE: 1 | row2col(T16, .(T20, T21), X31, [], X32), SCOPE: 3, CLAUSE: 4\n\nT16 is ground\nX31 is free\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: row2col(T16, .(T20, T21), X31, [], X32), SCOPE: 3, CLAUSE: 4\n\nT16 is ground\nX31 is free\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: row2col(T33, T36, X63, .([], []), X64)\n\nT33 is ground\nX63 is free\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: row2col(T33, T36, X63, .([], []), X64), SCOPE: 4, CLAUSE: 1 | row2col(T33, T36, X63, .([], []), X64), SCOPE: 4, CLAUSE: 4\n\nT33 is ground\nX63 is free\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: true | row2col([], T36, X63, .([], []), X64), SCOPE: 4, CLAUSE: 4\n\nX63 is free\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: row2col(T33, T36, X63, .([], []), X64), SCOPE: 4, CLAUSE: 4\n\nT33 is ground\nX63 is free\nX64 is free\nX69 is free\nrow2col(T33, T36, X63, .([], []), X64) !=? row2col([], [], [], X69, X69)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: row2col([], T36, X63, .([], []), X64), SCOPE: 4, CLAUSE: 4\n\nX63 is free\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: row2col(T46, T49, X102, .([], .([], [])), X103)\n\nT46 is ground\nX102 is free\nX103 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: row2col(T46, T49, X102, .([], .([], [])), X103), SCOPE: 5, CLAUSE: 1 | row2col(T46, T49, X102, .([], .([], [])), X103), SCOPE: 5, CLAUSE: 4\n\nT46 is ground\nX102 is free\nX103 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: true | row2col([], T49, X102, .([], .([], [])), X103), SCOPE: 5, CLAUSE: 4\n\nX102 is free\nX103 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: row2col(T46, T49, X102, .([], .([], [])), X103), SCOPE: 5, CLAUSE: 4\n\nT46 is ground\nX102 is free\nX103 is free\nX108 is free\nrow2col(T46, T49, X102, .([], .([], [])), X103) !=? row2col([], [], [], X108, X108)", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: row2col([], T49, X102, .([], .([], [])), X103), SCOPE: 5, CLAUSE: 4\n\nX102 is free\nX103 is free", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: row2col(T59, T62, X141, .([], .([], .([], []))), X142)\n\nT59 is ground\nX141 is free\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: row2col(T59, T62, X141, .([], .([], .([], []))), X142), SCOPE: 6, CLAUSE: 1 | row2col(T59, T62, X141, .([], .([], .([], []))), X142), SCOPE: 6, CLAUSE: 4\n\nT59 is ground\nX141 is free\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: true | row2col([], T62, X141, .([], .([], .([], []))), X142), SCOPE: 6, CLAUSE: 4\n\nX141 is free\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: row2col(T59, T62, X141, .([], .([], .([], []))), X142), SCOPE: 6, CLAUSE: 4\n\nT59 is ground\nX141 is free\nX142 is free\nX147 is free\nrow2col(T59, T62, X141, .([], .([], .([], []))), X142) !=? row2col([], [], [], X147, X147)", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: row2col([], T62, X141, .([], .([], .([], []))), X142), SCOPE: 6, CLAUSE: 4\n\nX141 is free\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: row2col(T72, T75, X180, .([], .([], .([], .([], [])))), X181)\n\nT72 is ground\nX180 is free\nX181 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: row2col(T72, T75, X180, .([], .([], .([], .([], [])))), X181), SCOPE: 7, CLAUSE: 1 | row2col(T72, T75, X180, .([], .([], .([], .([], [])))), X181), SCOPE: 7, CLAUSE: 4\n\nT72 is ground\nX180 is free\nX181 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: true | row2col([], T75, X180, .([], .([], .([], .([], [])))), X181), SCOPE: 7, CLAUSE: 4\n\nX180 is free\nX181 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: row2col(T72, T75, X180, .([], .([], .([], .([], [])))), X181), SCOPE: 7, CLAUSE: 4\n\nT72 is ground\nX180 is free\nX181 is free\nX186 is free\nrow2col(T72, T75, X180, .([], .([], .([], .([], [])))), X181) !=? row2col([], [], [], X186, X186)", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: row2col([], T75, X180, .([], .([], .([], .([], [])))), X181), SCOPE: 7, CLAUSE: 4\n\nX180 is free\nX181 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: row2col(T85, T88, X219, .([], .([], .([], .([], .([], []))))), X220)\n\nT85 is ground\nX219 is free\nX220 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: row2col(T85, T88, X219, .([], .([], .([], .([], .([], []))))), X220), SCOPE: 8, CLAUSE: 1 | row2col(T85, T88, X219, .([], .([], .([], .([], .([], []))))), X220), SCOPE: 8, CLAUSE: 4\n\nT85 is ground\nX219 is free\nX220 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: true | row2col([], T88, X219, .([], .([], .([], .([], .([], []))))), X220), SCOPE: 8, CLAUSE: 4\n\nX219 is free\nX220 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: row2col(T85, T88, X219, .([], .([], .([], .([], .([], []))))), X220), SCOPE: 8, CLAUSE: 4\n\nT85 is ground\nX219 is free\nX220 is free\nX225 is free\nrow2col(T85, T88, X219, .([], .([], .([], .([], .([], []))))), X220) !=? row2col([], [], [], X225, X225)", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: row2col([], T88, X219, .([], .([], .([], .([], .([], []))))), X220), SCOPE: 8, CLAUSE: 4\n\nX219 is free\nX220 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: row2col(T98, T101, X258, .([], .([], .([], .([], .([], .([], [])))))), X259)\n\nT98 is ground\nX258 is free\nX259 is free", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: row2col(T98, T101, X258, .([], .([], .([], .([], .([], .([], [])))))), X259), SCOPE: 9, CLAUSE: 1 | row2col(T98, T101, X258, .([], .([], .([], .([], .([], .([], [])))))), X259), SCOPE: 9, CLAUSE: 4\n\nT98 is ground\nX258 is free\nX259 is free", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: true | row2col([], T101, X258, .([], .([], .([], .([], .([], .([], [])))))), X259), SCOPE: 9, CLAUSE: 4\n\nX258 is free\nX259 is free", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: row2col(T98, T101, X258, .([], .([], .([], .([], .([], .([], [])))))), X259), SCOPE: 9, CLAUSE: 4\n\nT98 is ground\nX258 is free\nX259 is free\nX264 is free\nrow2col(T98, T101, X258, .([], .([], .([], .([], .([], .([], [])))))), X259) !=? row2col([], [], [], X264, X264)", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: row2col([], T101, X258, .([], .([], .([], .([], .([], .([], [])))))), X259), SCOPE: 9, CLAUSE: 4\n\nX258 is free\nX259 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: row2col(T111, T114, X297, .([], .([], .([], .([], .([], .([], .([], []))))))), X298)\n\nT111 is ground\nX297 is free\nX298 is free", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: row2col(T111, T114, X297, .([], .([], .([], .([], .([], .([], .([], []))))))), X298), SCOPE: 10, CLAUSE: 1 | row2col(T111, T114, X297, .([], .([], .([], .([], .([], .([], .([], []))))))), X298), SCOPE: 10, CLAUSE: 4\n\nT111 is ground\nX297 is free\nX298 is free", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: true | row2col([], T114, X297, .([], .([], .([], .([], .([], .([], .([], []))))))), X298), SCOPE: 10, CLAUSE: 4\n\nX297 is free\nX298 is free", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: row2col(T111, T114, X297, .([], .([], .([], .([], .([], .([], .([], []))))))), X298), SCOPE: 10, CLAUSE: 4\n\nT111 is ground\nX297 is free\nX298 is free\nX303 is free\nrow2col(T111, T114, X297, .([], .([], .([], .([], .([], .([], .([], []))))))), X298) !=? row2col([], [], [], X303, X303)", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: row2col([], T114, X297, .([], .([], .([], .([], .([], .([], .([], []))))))), X298), SCOPE: 10, CLAUSE: 4\n\nX297 is free\nX298 is free", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: row2col(T124, T127, X336, .([], .([], .([], .([], .([], .([], .([], .([], [])))))))), X337)\n\nT124 is ground\nX336 is free\nX337 is free", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: row2col(T124, T127, X336, .([], T128), X337)\n\nT124 is ground\nT128 is ground\nX336 is free\nX337 is free", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: row2col(T124, T127, X336, .([], T128), X337), SCOPE: 11, CLAUSE: 1 | row2col(T124, T127, X336, .([], T128), X337), SCOPE: 11, CLAUSE: 4\n\nT124 is ground\nT128 is ground\nX336 is free\nX337 is free", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: true | row2col([], T127, X336, .([], T133), X337), SCOPE: 11, CLAUSE: 4\n\nT133 is ground\nX336 is free\nX337 is free", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: row2col(T124, T127, X336, .([], T128), X337), SCOPE: 11, CLAUSE: 4\n\nT124 is ground\nT128 is ground\nX336 is free\nX337 is free\nX344 is free\nrow2col(T124, T127, X336, .([], T128), X337) !=? row2col([], [], [], X344, X344)", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: row2col([], T127, X336, .([], T133), X337), SCOPE: 11, CLAUSE: 4\n\nT133 is ground\nX336 is free\nX337 is free", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: row2col(T145, T149, X377, .([], .([], T148)), X378)\n\nT145 is ground\nT148 is ground\nX377 is free\nX378 is free", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: transpose_aux(T17, T23, T22), SCOPE: 12, CLAUSE: 0 | transpose_aux(T17, T23, T22), SCOPE: 12, CLAUSE: 3\n\nT17 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: true | transpose_aux([], T156, T22), SCOPE: 12, CLAUSE: 3\n\nT156 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: transpose_aux(T17, T23, T22), SCOPE: 12, CLAUSE: 3\n\nT17 is ground\nT23 is ground\nX385 is free\ntranspose_aux(T17, T23, T22) !=? transpose_aux([], X385, X385)", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: transpose_aux([], T156, T22), SCOPE: 12, CLAUSE: 3\n\nT156 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: ','(row2col(T167, .(T172, T173), X408, [], X409), transpose_aux(T168, X409, X408))\n\nT167 is ground\nT168 is ground\nX408 is free\nX409 is free", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 161 [arrowhead = none ];
161 -> 3;

162 [label="ONLY EVAL with clause\ntranspose(X4, X5) :- transpose_aux(X4, [], X5).\nand substitutionT1 -> T5,\nX4 -> T5,\nT2 -> T7,\nX5 -> T7,\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 162 [arrowhead = none ];
162 -> 5;

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

164 [label="EVAL with clause\ntranspose_aux([], X8, X8).\nand substitutionT5 -> [],\nX8 -> [],\nT7 -> []", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 164 [arrowhead = none ];
164 -> 8;

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

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

167 [label="EVAL with clause\ntranspose_aux(.(X26, X27), X28, .(X29, X30)) :- ','(row2col(X26, .(X29, X30), X31, [], X32), transpose_aux(X27, X32, X31)).\nand substitutionX26 -> T16,\nX27 -> T17,\nT5 -> .(T16, T17),\nX28 -> [],\nX29 -> T20,\nX30 -> T21,\nT7 -> .(T20, T21),\nT18 -> T20,\nT19 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 167 [arrowhead = none ];
167 -> 17;

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

169 [label="BACKTRACK\nfor clause: transpose_aux(.(R, Rs), X1, .(C, Cs)) :- ','(row2col(R, .(C, Cs), Cols1, [], Accm), transpose_aux(Rs, Accm, Cols1))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 169 [arrowhead = none ];
169 -> 11;

170 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
17 -> 170 [arrowhead = none ];
170 -> 21;

171 [label="SPLIT 2\nnew knowledge:\nT16 is ground\nT23 is ground\nreplacements:X31 -> T22,\nX32 -> T23", fontsize=14, style = filled, fillcolor = violet];
17 -> 171 [arrowhead = none ];
171 -> 22;

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

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

174 [label="BACKTRACK\nfor clause: row2col([], [], [], A, A)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 174 [arrowhead = none ];
174 -> 27;

175 [label="EVAL with clause\nrow2col(.(X56, X57), .(.(X56, X58), X59), .(X58, X60), X61, X62) :- row2col(X57, X59, X60, .([], X61), X62).\nand substitutionX56 -> T32,\nX57 -> T33,\nT16 -> .(T32, T33),\nX58 -> T34,\nT20 -> .(T32, T34),\nT21 -> T36,\nX59 -> T36,\nX60 -> X63,\nX31 -> .(T34, X63),\nX61 -> [],\nX32 -> X64,\nX62 -> X64,\nT35 -> T36", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 175 [arrowhead = none ];
175 -> 32;

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

177 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
32 -> 177 [arrowhead = none ];
177 -> 37;

178 [label="EVAL with clause\nrow2col([], [], [], X69, X69).\nand substitutionT33 -> [],\nT36 -> [],\nX63 -> [],\nX69 -> .([], []),\nX64 -> .([], [])", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 178 [arrowhead = none ];
178 -> 39;

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

180 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 180 [arrowhead = none ];
180 -> 41;

181 [label="EVAL with clause\nrow2col(.(X95, X96), .(.(X95, X97), X98), .(X97, X99), X100, X101) :- row2col(X96, X98, X99, .([], X100), X101).\nand substitutionX95 -> T45,\nX96 -> T46,\nT33 -> .(T45, T46),\nX97 -> T47,\nX98 -> T49,\nT36 -> .(.(T45, T47), T49),\nX99 -> X102,\nX63 -> .(T47, X102),\nX100 -> .([], []),\nX64 -> X103,\nX101 -> X103,\nT48 -> T49", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 181 [arrowhead = none ];
181 -> 45;

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

183 [label="BACKTRACK\nfor clause: row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), A, B) :- row2col(Xs, Cols, Cols1, .([], A), B)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 183 [arrowhead = none ];
183 -> 42;

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

185 [label="EVAL with clause\nrow2col([], [], [], X108, X108).\nand substitutionT46 -> [],\nT49 -> [],\nX102 -> [],\nX108 -> .([], .([], [])),\nX103 -> .([], .([], []))", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 185 [arrowhead = none ];
185 -> 52;

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

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

188 [label="EVAL with clause\nrow2col(.(X134, X135), .(.(X134, X136), X137), .(X136, X138), X139, X140) :- row2col(X135, X137, X138, .([], X139), X140).\nand substitutionX134 -> T58,\nX135 -> T59,\nT46 -> .(T58, T59),\nX136 -> T60,\nX137 -> T62,\nT49 -> .(.(T58, T60), T62),\nX138 -> X141,\nX102 -> .(T60, X141),\nX139 -> .([], .([], [])),\nX103 -> X142,\nX140 -> X142,\nT61 -> T62", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 188 [arrowhead = none ];
188 -> 59;

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

190 [label="BACKTRACK\nfor clause: row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), A, B) :- row2col(Xs, Cols, Cols1, .([], A), B)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 190 [arrowhead = none ];
190 -> 56;

191 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
59 -> 191 [arrowhead = none ];
191 -> 62;

192 [label="EVAL with clause\nrow2col([], [], [], X147, X147).\nand substitutionT59 -> [],\nT62 -> [],\nX141 -> [],\nX147 -> .([], .([], .([], []))),\nX142 -> .([], .([], .([], [])))", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 192 [arrowhead = none ];
192 -> 66;

193 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 193 [arrowhead = none ];
193 -> 68;

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

195 [label="EVAL with clause\nrow2col(.(X173, X174), .(.(X173, X175), X176), .(X175, X177), X178, X179) :- row2col(X174, X176, X177, .([], X178), X179).\nand substitutionX173 -> T71,\nX174 -> T72,\nT59 -> .(T71, T72),\nX175 -> T73,\nX176 -> T75,\nT62 -> .(.(T71, T73), T75),\nX177 -> X180,\nX141 -> .(T73, X180),\nX178 -> .([], .([], .([], []))),\nX142 -> X181,\nX179 -> X181,\nT74 -> T75", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 195 [arrowhead = none ];
195 -> 73;

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

197 [label="BACKTRACK\nfor clause: row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), A, B) :- row2col(Xs, Cols, Cols1, .([], A), B)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 197 [arrowhead = none ];
197 -> 70;

198 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
73 -> 198 [arrowhead = none ];
198 -> 77;

199 [label="EVAL with clause\nrow2col([], [], [], X186, X186).\nand substitutionT72 -> [],\nT75 -> [],\nX180 -> [],\nX186 -> .([], .([], .([], .([], [])))),\nX181 -> .([], .([], .([], .([], []))))", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 199 [arrowhead = none ];
199 -> 81;

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

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

202 [label="EVAL with clause\nrow2col(.(X212, X213), .(.(X212, X214), X215), .(X214, X216), X217, X218) :- row2col(X213, X215, X216, .([], X217), X218).\nand substitutionX212 -> T84,\nX213 -> T85,\nT72 -> .(T84, T85),\nX214 -> T86,\nX215 -> T88,\nT75 -> .(.(T84, T86), T88),\nX216 -> X219,\nX180 -> .(T86, X219),\nX217 -> .([], .([], .([], .([], [])))),\nX181 -> X220,\nX218 -> X220,\nT87 -> T88", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 202 [arrowhead = none ];
202 -> 87;

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

204 [label="BACKTRACK\nfor clause: row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), A, B) :- row2col(Xs, Cols, Cols1, .([], A), B)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
83 -> 204 [arrowhead = none ];
204 -> 84;

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

206 [label="EVAL with clause\nrow2col([], [], [], X225, X225).\nand substitutionT85 -> [],\nT88 -> [],\nX219 -> [],\nX225 -> .([], .([], .([], .([], .([], []))))),\nX220 -> .([], .([], .([], .([], .([], [])))))", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 206 [arrowhead = none ];
206 -> 95;

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

208 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
95 -> 208 [arrowhead = none ];
208 -> 97;

209 [label="EVAL with clause\nrow2col(.(X251, X252), .(.(X251, X253), X254), .(X253, X255), X256, X257) :- row2col(X252, X254, X255, .([], X256), X257).\nand substitutionX251 -> T97,\nX252 -> T98,\nT85 -> .(T97, T98),\nX253 -> T99,\nX254 -> T101,\nT88 -> .(.(T97, T99), T101),\nX255 -> X258,\nX219 -> .(T99, X258),\nX256 -> .([], .([], .([], .([], .([], []))))),\nX220 -> X259,\nX257 -> X259,\nT100 -> T101", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 209 [arrowhead = none ];
209 -> 101;

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

211 [label="BACKTRACK\nfor clause: row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), A, B) :- row2col(Xs, Cols, Cols1, .([], A), B)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
97 -> 211 [arrowhead = none ];
211 -> 98;

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

213 [label="EVAL with clause\nrow2col([], [], [], X264, X264).\nand substitutionT98 -> [],\nT101 -> [],\nX258 -> [],\nX264 -> .([], .([], .([], .([], .([], .([], [])))))),\nX259 -> .([], .([], .([], .([], .([], .([], []))))))", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 213 [arrowhead = none ];
213 -> 109;

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

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

216 [label="EVAL with clause\nrow2col(.(X290, X291), .(.(X290, X292), X293), .(X292, X294), X295, X296) :- row2col(X291, X293, X294, .([], X295), X296).\nand substitutionX290 -> T110,\nX291 -> T111,\nT98 -> .(T110, T111),\nX292 -> T112,\nX293 -> T114,\nT101 -> .(.(T110, T112), T114),\nX294 -> X297,\nX258 -> .(T112, X297),\nX295 -> .([], .([], .([], .([], .([], .([], [])))))),\nX259 -> X298,\nX296 -> X298,\nT113 -> T114", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 216 [arrowhead = none ];
216 -> 115;

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

218 [label="BACKTRACK\nfor clause: row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), A, B) :- row2col(Xs, Cols, Cols1, .([], A), B)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
111 -> 218 [arrowhead = none ];
218 -> 112;

219 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
115 -> 219 [arrowhead = none ];
219 -> 121;

220 [label="EVAL with clause\nrow2col([], [], [], X303, X303).\nand substitutionT111 -> [],\nT114 -> [],\nX297 -> [],\nX303 -> .([], .([], .([], .([], .([], .([], .([], []))))))),\nX298 -> .([], .([], .([], .([], .([], .([], .([], [])))))))", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 220 [arrowhead = none ];
220 -> 123;

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

222 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
123 -> 222 [arrowhead = none ];
222 -> 125;

223 [label="EVAL with clause\nrow2col(.(X329, X330), .(.(X329, X331), X332), .(X331, X333), X334, X335) :- row2col(X330, X332, X333, .([], X334), X335).\nand substitutionX329 -> T123,\nX330 -> T124,\nT111 -> .(T123, T124),\nX331 -> T125,\nX332 -> T127,\nT114 -> .(.(T123, T125), T127),\nX333 -> X336,\nX297 -> .(T125, X336),\nX334 -> .([], .([], .([], .([], .([], .([], .([], []))))))),\nX298 -> X337,\nX335 -> X337,\nT126 -> T127", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 223 [arrowhead = none ];
223 -> 129;

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

225 [label="BACKTRACK\nfor clause: row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), A, B) :- row2col(Xs, Cols, Cols1, .([], A), B)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
125 -> 225 [arrowhead = none ];
225 -> 126;

226 [label="GENERALIZATION\nT128 <-- .([], .([], .([], .([], .([], .([], .([], [])))))))\n\nNew Knowledge:\nT128 is ground", fontsize=14, style = filled, fillcolor = violet];
129 -> 226 [arrowhead = none ];
226 -> 132;

227 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
132 -> 227 [arrowhead = none ];
227 -> 137;

228 [label="EVAL with clause\nrow2col([], [], [], X344, X344).\nand substitutionT124 -> [],\nT127 -> [],\nX336 -> [],\nT128 -> T133,\nX344 -> .([], T133),\nX337 -> .([], T133)", fontsize=14, style = filled, fillcolor = lightblue];
137 -> 228 [arrowhead = none ];
228 -> 139;

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

230 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
139 -> 230 [arrowhead = none ];
230 -> 141;

231 [label="EVAL with clause\nrow2col(.(X370, X371), .(.(X370, X372), X373), .(X372, X374), X375, X376) :- row2col(X371, X373, X374, .([], X375), X376).\nand substitutionX370 -> T144,\nX371 -> T145,\nT124 -> .(T144, T145),\nX372 -> T146,\nX373 -> T149,\nT127 -> .(.(T144, T146), T149),\nX374 -> X377,\nX336 -> .(T146, X377),\nT128 -> T148,\nX375 -> .([], T148),\nX337 -> X378,\nX376 -> X378,\nT147 -> T149", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 231 [arrowhead = none ];
231 -> 145;

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

233 [label="BACKTRACK\nfor clause: row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), A, B) :- row2col(Xs, Cols, Cols1, .([], A), B)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
141 -> 233 [arrowhead = none ];
233 -> 142;

234 [label="INSTANCE with matching:\nT124 -> T145\nT127 -> T149\nX336 -> X377\nT128 -> .([], T148)\nX337 -> X378", fontsize=14, style = filled, fillcolor = lightgrey];
145 -> 234 [arrowhead = none , style=dashed];
234 -> 132[style=dashed];

235 [label="EVAL with clause\ntranspose_aux([], X385, X385).\nand substitutionT17 -> [],\nT23 -> T156,\nX385 -> T156,\nT22 -> T156", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 235 [arrowhead = none ];
235 -> 153;

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

237 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
153 -> 237 [arrowhead = none ];
237 -> 155;

238 [label="EVAL with clause\ntranspose_aux(.(X403, X404), X405, .(X406, X407)) :- ','(row2col(X403, .(X406, X407), X408, [], X409), transpose_aux(X404, X409, X408)).\nand substitutionX403 -> T167,\nX404 -> T168,\nT17 -> .(T167, T168),\nT23 -> T169,\nX405 -> T169,\nX406 -> T172,\nX407 -> T173,\nT22 -> .(T172, T173),\nT170 -> T172,\nT171 -> T173", fontsize=14, style = filled, fillcolor = lightblue];
154 -> 238 [arrowhead = none ];
238 -> 159;

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

240 [label="BACKTRACK\nfor clause: transpose_aux(.(R, Rs), X1, .(C, Cs)) :- ','(row2col(R, .(C, Cs), Cols1, [], Accm), transpose_aux(Rs, Accm, Cols1))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
155 -> 240 [arrowhead = none ];
240 -> 156;

241 [label="INSTANCE with matching:\nT16 -> T167\nT20 -> T172\nT21 -> T173\nX31 -> X408\nX32 -> X409\nT17 -> T168", fontsize=14, style = filled, fillcolor = lightgrey];
159 -> 241 [arrowhead = none , style=dashed];
241 -> 17[style=dashed];

}

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, z1)) → U1(f17_in(z0, z1), .(z0, z1))
U1(f17_out1(z0), .(z1, z2)) → f2_out1
f132_in([], z0) → f132_out1(.([], z0))
f132_in(.(z0, z1), z2) → U2(f132_in(z1, .([], z2)), .(z0, z1), z2)
U2(f132_out1(z0), .(z1, z2), z3) → f132_out1(z0)
f21_in(.(z0, [])) → f21_out1(.([], []))
f21_in(.(z0, .(z1, []))) → f21_out1(.([], .([], [])))
f21_in(.(z0, .(z1, .(z2, [])))) → f21_out1(.([], .([], .([], []))))
f21_in(.(z0, .(z1, .(z2, .(z3, []))))) → f21_out1(.([], .([], .([], .([], [])))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f21_out1(.([], .([], .([], .([], .([], []))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f21_out1(.([], .([], .([], .([], .([], .([], [])))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f21_out1(.([], .([], .([], .([], .([], .([], .([], []))))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U3(f132_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U3(f132_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f21_out1(z0)
f22_in([], z0) → f22_out1
f22_in(.(z0, z1), z2) → U4(f17_in(z0, z1), .(z0, z1), z2)
U4(f17_out1(z0), .(z1, z2), z3) → f22_out1
f17_in(z0, z1) → U5(f21_in(z0), z0, z1)
U5(f21_out1(z0), z1, z2) → U6(f22_in(z2, z0), z1, z2, z0)
U6(f22_out1, z0, z1, z2) → f17_out1(z2)

Tuples:

F2_IN(.(z0, z1)) → c1(U1'(f17_in(z0, z1), .(z0, z1)), F17_IN(z0, z1))
F132_IN(.(z0, z1), z2) → c4(U2'(f132_in(z1, .([], z2)), .(z0, z1), z2), F132_IN(z1, .([], z2)))
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c13(U3'(f132_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F132_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F22_IN(.(z0, z1), z2) → c16(U4'(f17_in(z0, z1), .(z0, z1), z2), F17_IN(z0, z1))
F17_IN(z0, z1) → c18(U5'(f21_in(z0), z0, z1), F21_IN(z0))
U5'(f21_out1(z0), z1, z2) → c19(U6'(f22_in(z2, z0), z1, z2, z0), F22_IN(z2, z0))

S tuples:

F2_IN(.(z0, z1)) → c1(U1'(f17_in(z0, z1), .(z0, z1)), F17_IN(z0, z1))
F132_IN(.(z0, z1), z2) → c4(U2'(f132_in(z1, .([], z2)), .(z0, z1), z2), F132_IN(z1, .([], z2)))
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c13(U3'(f132_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F132_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F22_IN(.(z0, z1), z2) → c16(U4'(f17_in(z0, z1), .(z0, z1), z2), F17_IN(z0, z1))
F17_IN(z0, z1) → c18(U5'(f21_in(z0), z0, z1), F21_IN(z0))
U5'(f21_out1(z0), z1, z2) → c19(U6'(f22_in(z2, z0), z1, z2, z0), F22_IN(z2, z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f132_in, U2, f21_in, U3, f22_in, U4, f17_in, U5, U6

Defined Pair Symbols:

F2_IN, F132_IN, F21_IN, F22_IN, F17_IN, U5'

Compound Symbols:

c1, c4, c13, c16, c18, c19

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

Split RHS of tuples not part of any SCC

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, z1)) → U1(f17_in(z0, z1), .(z0, z1))
U1(f17_out1(z0), .(z1, z2)) → f2_out1
f132_in([], z0) → f132_out1(.([], z0))
f132_in(.(z0, z1), z2) → U2(f132_in(z1, .([], z2)), .(z0, z1), z2)
U2(f132_out1(z0), .(z1, z2), z3) → f132_out1(z0)
f21_in(.(z0, [])) → f21_out1(.([], []))
f21_in(.(z0, .(z1, []))) → f21_out1(.([], .([], [])))
f21_in(.(z0, .(z1, .(z2, [])))) → f21_out1(.([], .([], .([], []))))
f21_in(.(z0, .(z1, .(z2, .(z3, []))))) → f21_out1(.([], .([], .([], .([], [])))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f21_out1(.([], .([], .([], .([], .([], []))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f21_out1(.([], .([], .([], .([], .([], .([], [])))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f21_out1(.([], .([], .([], .([], .([], .([], .([], []))))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U3(f132_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U3(f132_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f21_out1(z0)
f22_in([], z0) → f22_out1
f22_in(.(z0, z1), z2) → U4(f17_in(z0, z1), .(z0, z1), z2)
U4(f17_out1(z0), .(z1, z2), z3) → f22_out1
f17_in(z0, z1) → U5(f21_in(z0), z0, z1)
U5(f21_out1(z0), z1, z2) → U6(f22_in(z2, z0), z1, z2, z0)
U6(f22_out1, z0, z1, z2) → f17_out1(z2)

Tuples:

F132_IN(.(z0, z1), z2) → c4(U2'(f132_in(z1, .([], z2)), .(z0, z1), z2), F132_IN(z1, .([], z2)))
F22_IN(.(z0, z1), z2) → c16(U4'(f17_in(z0, z1), .(z0, z1), z2), F17_IN(z0, z1))
F17_IN(z0, z1) → c18(U5'(f21_in(z0), z0, z1), F21_IN(z0))
U5'(f21_out1(z0), z1, z2) → c19(U6'(f22_in(z2, z0), z1, z2, z0), F22_IN(z2, z0))
F2_IN(.(z0, z1)) → c(U1'(f17_in(z0, z1), .(z0, z1)))
F2_IN(.(z0, z1)) → c(F17_IN(z0, z1))
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U3'(f132_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F132_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))

S tuples:

F132_IN(.(z0, z1), z2) → c4(U2'(f132_in(z1, .([], z2)), .(z0, z1), z2), F132_IN(z1, .([], z2)))
F22_IN(.(z0, z1), z2) → c16(U4'(f17_in(z0, z1), .(z0, z1), z2), F17_IN(z0, z1))
F17_IN(z0, z1) → c18(U5'(f21_in(z0), z0, z1), F21_IN(z0))
U5'(f21_out1(z0), z1, z2) → c19(U6'(f22_in(z2, z0), z1, z2, z0), F22_IN(z2, z0))
F2_IN(.(z0, z1)) → c(U1'(f17_in(z0, z1), .(z0, z1)))
F2_IN(.(z0, z1)) → c(F17_IN(z0, z1))
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U3'(f132_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F132_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f132_in, U2, f21_in, U3, f22_in, U4, f17_in, U5, U6

Defined Pair Symbols:

F132_IN, F22_IN, F17_IN, U5', F2_IN, F21_IN

Compound Symbols:

c4, c16, c18, c19, c

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

Removed 5 trailing tuple parts

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, z1)) → U1(f17_in(z0, z1), .(z0, z1))
U1(f17_out1(z0), .(z1, z2)) → f2_out1
f132_in([], z0) → f132_out1(.([], z0))
f132_in(.(z0, z1), z2) → U2(f132_in(z1, .([], z2)), .(z0, z1), z2)
U2(f132_out1(z0), .(z1, z2), z3) → f132_out1(z0)
f21_in(.(z0, [])) → f21_out1(.([], []))
f21_in(.(z0, .(z1, []))) → f21_out1(.([], .([], [])))
f21_in(.(z0, .(z1, .(z2, [])))) → f21_out1(.([], .([], .([], []))))
f21_in(.(z0, .(z1, .(z2, .(z3, []))))) → f21_out1(.([], .([], .([], .([], [])))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f21_out1(.([], .([], .([], .([], .([], []))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f21_out1(.([], .([], .([], .([], .([], .([], [])))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f21_out1(.([], .([], .([], .([], .([], .([], .([], []))))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U3(f132_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U3(f132_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f21_out1(z0)
f22_in([], z0) → f22_out1
f22_in(.(z0, z1), z2) → U4(f17_in(z0, z1), .(z0, z1), z2)
U4(f17_out1(z0), .(z1, z2), z3) → f22_out1
f17_in(z0, z1) → U5(f21_in(z0), z0, z1)
U5(f21_out1(z0), z1, z2) → U6(f22_in(z2, z0), z1, z2, z0)
U6(f22_out1, z0, z1, z2) → f17_out1(z2)

Tuples:

F17_IN(z0, z1) → c18(U5'(f21_in(z0), z0, z1), F21_IN(z0))
F2_IN(.(z0, z1)) → c(F17_IN(z0, z1))
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F132_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F132_IN(.(z0, z1), z2) → c4(F132_IN(z1, .([], z2)))
F22_IN(.(z0, z1), z2) → c16(F17_IN(z0, z1))
U5'(f21_out1(z0), z1, z2) → c19(F22_IN(z2, z0))
F2_IN(.(z0, z1)) → c
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:

F17_IN(z0, z1) → c18(U5'(f21_in(z0), z0, z1), F21_IN(z0))
F2_IN(.(z0, z1)) → c(F17_IN(z0, z1))
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F132_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F132_IN(.(z0, z1), z2) → c4(F132_IN(z1, .([], z2)))
F22_IN(.(z0, z1), z2) → c16(F17_IN(z0, z1))
U5'(f21_out1(z0), z1, z2) → c19(F22_IN(z2, z0))
F2_IN(.(z0, z1)) → c
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

K tuples:none
Defined Rule Symbols:

f2_in, U1, f132_in, U2, f21_in, U3, f22_in, U4, f17_in, U5, U6

Defined Pair Symbols:

F17_IN, F2_IN, F21_IN, F132_IN, F22_IN, U5'

Compound Symbols:

c18, c, c4, c16, c19, c

(25) CdtKnowledgeProof (EQUIVALENT transformation)

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

F2_IN(.(z0, z1)) → c(F17_IN(z0, z1))
F2_IN(.(z0, z1)) → c

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, z1)) → U1(f17_in(z0, z1), .(z0, z1))
U1(f17_out1(z0), .(z1, z2)) → f2_out1
f132_in([], z0) → f132_out1(.([], z0))
f132_in(.(z0, z1), z2) → U2(f132_in(z1, .([], z2)), .(z0, z1), z2)
U2(f132_out1(z0), .(z1, z2), z3) → f132_out1(z0)
f21_in(.(z0, [])) → f21_out1(.([], []))
f21_in(.(z0, .(z1, []))) → f21_out1(.([], .([], [])))
f21_in(.(z0, .(z1, .(z2, [])))) → f21_out1(.([], .([], .([], []))))
f21_in(.(z0, .(z1, .(z2, .(z3, []))))) → f21_out1(.([], .([], .([], .([], [])))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f21_out1(.([], .([], .([], .([], .([], []))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f21_out1(.([], .([], .([], .([], .([], .([], [])))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f21_out1(.([], .([], .([], .([], .([], .([], .([], []))))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U3(f132_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U3(f132_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f21_out1(z0)
f22_in([], z0) → f22_out1
f22_in(.(z0, z1), z2) → U4(f17_in(z0, z1), .(z0, z1), z2)
U4(f17_out1(z0), .(z1, z2), z3) → f22_out1
f17_in(z0, z1) → U5(f21_in(z0), z0, z1)
U5(f21_out1(z0), z1, z2) → U6(f22_in(z2, z0), z1, z2, z0)
U6(f22_out1, z0, z1, z2) → f17_out1(z2)

Tuples:

F17_IN(z0, z1) → c18(U5'(f21_in(z0), z0, z1), F21_IN(z0))
F2_IN(.(z0, z1)) → c(F17_IN(z0, z1))
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F132_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F132_IN(.(z0, z1), z2) → c4(F132_IN(z1, .([], z2)))
F22_IN(.(z0, z1), z2) → c16(F17_IN(z0, z1))
U5'(f21_out1(z0), z1, z2) → c19(F22_IN(z2, z0))
F2_IN(.(z0, z1)) → c
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:

F17_IN(z0, z1) → c18(U5'(f21_in(z0), z0, z1), F21_IN(z0))
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F132_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F132_IN(.(z0, z1), z2) → c4(F132_IN(z1, .([], z2)))
F22_IN(.(z0, z1), z2) → c16(F17_IN(z0, z1))
U5'(f21_out1(z0), z1, z2) → c19(F22_IN(z2, z0))
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

K tuples:

F2_IN(.(z0, z1)) → c(F17_IN(z0, z1))
F2_IN(.(z0, z1)) → c

Defined Rule Symbols:

f2_in, U1, f132_in, U2, f21_in, U3, f22_in, U4, f17_in, U5, U6

Defined Pair Symbols:

F17_IN, F2_IN, F21_IN, F132_IN, F22_IN, U5'

Compound Symbols:

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

F17_IN(z0, z1) → c18(U5'(f21_in(z0), z0, z1), F21_IN(z0))
F22_IN(.(z0, z1), z2) → c16(F17_IN(z0, z1))
U5'(f21_out1(z0), z1, z2) → c19(F22_IN(z2, z0))
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

We considered the (Usable) Rules:

f21_in(.(z0, [])) → f21_out1(.([], []))
f21_in(.(z0, .(z1, []))) → f21_out1(.([], .([], [])))
f21_in(.(z0, .(z1, .(z2, [])))) → f21_out1(.([], .([], .([], []))))
f21_in(.(z0, .(z1, .(z2, .(z3, []))))) → f21_out1(.([], .([], .([], .([], [])))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f21_out1(.([], .([], .([], .([], .([], []))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f21_out1(.([], .([], .([], .([], .([], .([], [])))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f21_out1(.([], .([], .([], .([], .([], .([], .([], []))))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U3(f132_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
f132_in([], z0) → f132_out1(.([], z0))
f132_in(.(z0, z1), z2) → U2(f132_in(z1, .([], z2)), .(z0, z1), z2)
U3(f132_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f21_out1(z0)
U2(f132_out1(z0), .(z1, z2), z3) → f132_out1(z0)

And the Tuples:

F17_IN(z0, z1) → c18(U5'(f21_in(z0), z0, z1), F21_IN(z0))
F2_IN(.(z0, z1)) → c(F17_IN(z0, z1))
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F132_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F132_IN(.(z0, z1), z2) → c4(F132_IN(z1, .([], z2)))
F22_IN(.(z0, z1), z2) → c16(F17_IN(z0, z1))
U5'(f21_out1(z0), z1, z2) → c19(F22_IN(z2, z0))
F2_IN(.(z0, z1)) → c
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

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

POL(.(x₁, x₂)) = [2] + x₁ + x₂   
POL(F132_IN(x₁, x₂)) = [2] + x₁ + x₂   
POL(F17_IN(x₁, x₂)) = [2] + x₁ + [2]x₂   
POL(F21_IN(x₁)) = x₁   
POL(F22_IN(x₁, x₂)) = [2]x₁   
POL(F2_IN(x₁)) = [1] + [2]x₁   
POL(U2(x₁, x₂, x₃)) = 0   
POL(U3(x₁, x₂)) = 0   
POL(U5'(x₁, x₂, x₃)) = [1] + [2]x₃   
POL([]) = 0   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c16(x₁)) = x₁   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c19(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(f132_in(x₁, x₂)) = 0   
POL(f132_out1(x₁)) = 0   
POL(f21_in(x₁)) = 0   
POL(f21_out1(x₁)) = 0   

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, z1)) → U1(f17_in(z0, z1), .(z0, z1))
U1(f17_out1(z0), .(z1, z2)) → f2_out1
f132_in([], z0) → f132_out1(.([], z0))
f132_in(.(z0, z1), z2) → U2(f132_in(z1, .([], z2)), .(z0, z1), z2)
U2(f132_out1(z0), .(z1, z2), z3) → f132_out1(z0)
f21_in(.(z0, [])) → f21_out1(.([], []))
f21_in(.(z0, .(z1, []))) → f21_out1(.([], .([], [])))
f21_in(.(z0, .(z1, .(z2, [])))) → f21_out1(.([], .([], .([], []))))
f21_in(.(z0, .(z1, .(z2, .(z3, []))))) → f21_out1(.([], .([], .([], .([], [])))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f21_out1(.([], .([], .([], .([], .([], []))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f21_out1(.([], .([], .([], .([], .([], .([], [])))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f21_out1(.([], .([], .([], .([], .([], .([], .([], []))))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U3(f132_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U3(f132_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f21_out1(z0)
f22_in([], z0) → f22_out1
f22_in(.(z0, z1), z2) → U4(f17_in(z0, z1), .(z0, z1), z2)
U4(f17_out1(z0), .(z1, z2), z3) → f22_out1
f17_in(z0, z1) → U5(f21_in(z0), z0, z1)
U5(f21_out1(z0), z1, z2) → U6(f22_in(z2, z0), z1, z2, z0)
U6(f22_out1, z0, z1, z2) → f17_out1(z2)

Tuples:

F17_IN(z0, z1) → c18(U5'(f21_in(z0), z0, z1), F21_IN(z0))
F2_IN(.(z0, z1)) → c(F17_IN(z0, z1))
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F132_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F132_IN(.(z0, z1), z2) → c4(F132_IN(z1, .([], z2)))
F22_IN(.(z0, z1), z2) → c16(F17_IN(z0, z1))
U5'(f21_out1(z0), z1, z2) → c19(F22_IN(z2, z0))
F2_IN(.(z0, z1)) → c
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:

F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F132_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F132_IN(.(z0, z1), z2) → c4(F132_IN(z1, .([], z2)))

K tuples:

F2_IN(.(z0, z1)) → c(F17_IN(z0, z1))
F2_IN(.(z0, z1)) → c
F17_IN(z0, z1) → c18(U5'(f21_in(z0), z0, z1), F21_IN(z0))
F22_IN(.(z0, z1), z2) → c16(F17_IN(z0, z1))
U5'(f21_out1(z0), z1, z2) → c19(F22_IN(z2, z0))
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

Defined Rule Symbols:

f2_in, U1, f132_in, U2, f21_in, U3, f22_in, U4, f17_in, U5, U6

Defined Pair Symbols:

F17_IN, F2_IN, F21_IN, F132_IN, F22_IN, U5'

Compound Symbols:

c18, c, c4, c16, c19, c

(29) CdtKnowledgeProof (EQUIVALENT transformation)

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

F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F132_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, z1)) → U1(f17_in(z0, z1), .(z0, z1))
U1(f17_out1(z0), .(z1, z2)) → f2_out1
f132_in([], z0) → f132_out1(.([], z0))
f132_in(.(z0, z1), z2) → U2(f132_in(z1, .([], z2)), .(z0, z1), z2)
U2(f132_out1(z0), .(z1, z2), z3) → f132_out1(z0)
f21_in(.(z0, [])) → f21_out1(.([], []))
f21_in(.(z0, .(z1, []))) → f21_out1(.([], .([], [])))
f21_in(.(z0, .(z1, .(z2, [])))) → f21_out1(.([], .([], .([], []))))
f21_in(.(z0, .(z1, .(z2, .(z3, []))))) → f21_out1(.([], .([], .([], .([], [])))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f21_out1(.([], .([], .([], .([], .([], []))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f21_out1(.([], .([], .([], .([], .([], .([], [])))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f21_out1(.([], .([], .([], .([], .([], .([], .([], []))))))))
f21_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U3(f132_in(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U3(f132_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f21_out1(z0)
f22_in([], z0) → f22_out1
f22_in(.(z0, z1), z2) → U4(f17_in(z0, z1), .(z0, z1), z2)
U4(f17_out1(z0), .(z1, z2), z3) → f22_out1
f17_in(z0, z1) → U5(f21_in(z0), z0, z1)
U5(f21_out1(z0), z1, z2) → U6(f22_in(z2, z0), z1, z2, z0)
U6(f22_out1, z0, z1, z2) → f17_out1(z2)

Tuples:

F17_IN(z0, z1) → c18(U5'(f21_in(z0), z0, z1), F21_IN(z0))
F2_IN(.(z0, z1)) → c(F17_IN(z0, z1))
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F132_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))
F132_IN(.(z0, z1), z2) → c4(F132_IN(z1, .([], z2)))
F22_IN(.(z0, z1), z2) → c16(F17_IN(z0, z1))
U5'(f21_out1(z0), z1, z2) → c19(F22_IN(z2, z0))
F2_IN(.(z0, z1)) → c
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:

F132_IN(.(z0, z1), z2) → c4(F132_IN(z1, .([], z2)))

K tuples:

F2_IN(.(z0, z1)) → c(F17_IN(z0, z1))
F2_IN(.(z0, z1)) → c
F17_IN(z0, z1) → c18(U5'(f21_in(z0), z0, z1), F21_IN(z0))
F22_IN(.(z0, z1), z2) → c16(F17_IN(z0, z1))
U5'(f21_out1(z0), z1, z2) → c19(F22_IN(z2, z0))
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
F21_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F132_IN(z8, .([], .([], .([], .([], .([], .([], .([], [])))))))))

Defined Rule Symbols:

f2_in, U1, f132_in, U2, f21_in, U3, f22_in, U4, f17_in, U5, U6

Defined Pair Symbols:

F17_IN, F2_IN, F21_IN, F132_IN, F22_IN, U5'

Compound Symbols:

c18, c, c4, c16, c19, c