Left Termination of the query pattern
select(g,g,a)
w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

select(X, Y, Zs) :- ','(no(empty(Y)), ','(head(Y, X), tail(Y, Zs))).
select(X, Y, Z) :- ','(no(empty(Y)), ','(head(Y, H), ','(head(Z, H), ','(tail(Y, T), ','(tail(Z, Zs), select(X, T, Zs)))))).
head([], X1).
head(.(H, X2), H).
tail([], []).
tail(.(X3, T), T).
empty([]).
no(X) :- ','(X, ','(!, failure(a))).
no(X4).
failure(b).

Query: select(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: select(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: select(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | select(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(no(empty(T8)), ','(head(T8, T7), tail(T8, T10))) | select(T7, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(no(empty(T8)), ','(head(T8, T7), tail(T8, T10))), SCOPE: 2, CLAUSE: 7 | ','(no(empty(T8)), ','(head(T8, T7), tail(T8, T10))), SCOPE: 2, CLAUSE: 8 | ?_2 | select(T7, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(','(call(empty(T13)), ','(!_2, failure(a))), ','(head(T13, T7), tail(T13, T10))) | ','(no(empty(T13)), ','(head(T13, T7), tail(T13, T10))), SCOPE: 2, CLAUSE: 8 | ?_2 | select(T7, T13, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(empty(T13), ','(','(!_2, failure(a)), ','(head(T13, T7), tail(T13, T10)))) | ?_3 | ','(no(empty(T13)), ','(head(T13, T7), tail(T13, T10))), SCOPE: 2, CLAUSE: 8 | ?_2 | select(T7, T13, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(empty(T13), ','(','(!_2, failure(a)), ','(head(T13, T7), tail(T13, T10)))), SCOPE: 4, CLAUSE: 6 | ?_4 | ?_3 | ','(no(empty(T13)), ','(head(T13, T7), tail(T13, T10))), SCOPE: 2, CLAUSE: 8 | ?_2 | select(T7, T13, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(','(!_2, failure(a)), ','(head([], T7), tail([], T10))) | ?_4 | ?_3 | ','(no(empty([])), ','(head([], T7), tail([], T10))), SCOPE: 2, CLAUSE: 8 | ?_2 | select(T7, [], T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ?_4 | ?_3 | ','(no(empty(T13)), ','(head(T13, T7), tail(T13, T10))), SCOPE: 2, CLAUSE: 8 | ?_2 | select(T7, T13, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT13 is ground\nempty(T13) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(failure(a), ','(head([], T7), tail([], T10))) | select(T7, [], T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(failure(a), ','(head([], T7), tail([], T10)))\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: select(T7, [], T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(failure(a), ','(head([], T7), tail([], T10))), SCOPE: 5, CLAUSE: 9\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(no(empty([])), ','(head([], X31), ','(head(T22, X31), ','(tail([], X32), ','(tail(T22, X33), select(T20, X32, X33))))))\n\nT20 is ground\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(no(empty([])), ','(head([], X31), ','(head(T22, X31), ','(tail([], X32), ','(tail(T22, X33), select(T20, X32, X33)))))), SCOPE: 6, CLAUSE: 7 | ','(no(empty([])), ','(head([], X31), ','(head(T22, X31), ','(tail([], X32), ','(tail(T22, X33), select(T20, X32, X33)))))), SCOPE: 6, CLAUSE: 8\n\nT20 is ground\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(','(call(empty([])), ','(!_6, failure(a))), ','(head([], X31), ','(head(T22, X31), ','(tail([], X32), ','(tail(T22, X33), select(T20, X32, X33)))))) | ','(no(empty([])), ','(head([], X31), ','(head(T22, X31), ','(tail([], X32), ','(tail(T22, X33), select(T20, X32, X33)))))), SCOPE: 6, CLAUSE: 8\n\nT20 is ground\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(empty([]), ','(','(!_6, failure(a)), ','(head([], X31), ','(head(T22, X31), ','(tail([], X32), ','(tail(T22, X33), select(T20, X32, X33))))))) | ?_7 | ','(no(empty([])), ','(head([], X31), ','(head(T22, X31), ','(tail([], X32), ','(tail(T22, X33), select(T20, X32, X33)))))), SCOPE: 6, CLAUSE: 8\n\nT20 is ground\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(empty([]), ','(','(!_6, failure(a)), ','(head([], X31), ','(head(T22, X31), ','(tail([], X32), ','(tail(T22, X33), select(T20, X32, X33))))))), SCOPE: 8, CLAUSE: 6 | ?_8 | ?_7 | ','(no(empty([])), ','(head([], X31), ','(head(T22, X31), ','(tail([], X32), ','(tail(T22, X33), select(T20, X32, X33)))))), SCOPE: 6, CLAUSE: 8\n\nT20 is ground\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(','(!_6, failure(a)), ','(head([], X31), ','(head(T22, X31), ','(tail([], X32), ','(tail(T22, X33), select(T20, X32, X33)))))) | ?_8 | ?_7 | ','(no(empty([])), ','(head([], X31), ','(head(T22, X31), ','(tail([], X32), ','(tail(T22, X33), select(T20, X32, X33)))))), SCOPE: 6, CLAUSE: 8\n\nT20 is ground\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(failure(a), ','(head([], X31), ','(head(T22, X31), ','(tail([], X32), ','(tail(T22, X33), select(T20, X32, X33))))))\n\nT20 is ground\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(failure(a), ','(head([], X31), ','(head(T22, X31), ','(tail([], X32), ','(tail(T22, X33), select(T20, X32, X33)))))), SCOPE: 9, CLAUSE: 9\n\nT20 is ground\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ?_3 | ','(no(empty(T13)), ','(head(T13, T7), tail(T13, T10))), SCOPE: 2, CLAUSE: 8 | ?_2 | select(T7, T13, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT13 is ground\nempty(T13) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(no(empty(T13)), ','(head(T13, T7), tail(T13, T10))), SCOPE: 2, CLAUSE: 8 | ?_2 | select(T7, T13, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT13 is ground\nempty(T13) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(no(empty(T13)), ','(head(T13, T7), tail(T13, T10))), SCOPE: 2, CLAUSE: 8\n\nT7 is ground\nT13 is ground\nempty(T13) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ?_2 | select(T7, T13, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT13 is ground\nempty(T13) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(head(T29, T7), tail(T29, T10))\n\nT7 is ground\nT29 is ground\nempty(T29) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(head(T29, T7), tail(T29, T10)), SCOPE: 10, CLAUSE: 2 | ','(head(T29, T7), tail(T29, T10)), SCOPE: 10, CLAUSE: 3\n\nT7 is ground\nT29 is ground\nempty(T29) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(head(T29, T7), tail(T29, T10)), SCOPE: 10, CLAUSE: 3\n\nT7 is ground\nT29 is ground\nempty(T29) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: tail(.(T35, T36), T10)\n\nT35 is ground\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: tail(.(T35, T36), T10), SCOPE: 11, CLAUSE: 4 | tail(.(T35, T36), T10), SCOPE: 11, CLAUSE: 5\n\nT35 is ground\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: tail(.(T35, T36), T10), SCOPE: 11, CLAUSE: 5\n\nT35 is ground\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: select(T7, T13, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT13 is ground\nempty(T13) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(no(empty(T52)), ','(head(T52, X82), ','(head(T54, X82), ','(tail(T52, X83), ','(tail(T54, X84), select(T51, X83, X84))))))\n\nT51 is ground\nT52 is ground\nX82 is free\nX83 is free\nX84 is free\nempty(T52) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(no(empty(T52)), ','(head(T52, X82), ','(head(T54, X82), ','(tail(T52, X83), ','(tail(T54, X84), select(T51, X83, X84)))))), SCOPE: 12, CLAUSE: 7 | ','(no(empty(T52)), ','(head(T52, X82), ','(head(T54, X82), ','(tail(T52, X83), ','(tail(T54, X84), select(T51, X83, X84)))))), SCOPE: 12, CLAUSE: 8\n\nT51 is ground\nT52 is ground\nX82 is free\nX83 is free\nX84 is free\nempty(T52) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: ','(','(call(empty(T58)), ','(!_12, failure(a))), ','(head(T58, X82), ','(head(T54, X82), ','(tail(T58, X83), ','(tail(T54, X84), select(T51, X83, X84)))))) | ','(no(empty(T58)), ','(head(T58, X82), ','(head(T54, X82), ','(tail(T58, X83), ','(tail(T54, X84), select(T51, X83, X84)))))), SCOPE: 12, CLAUSE: 8\n\nT51 is ground\nT58 is ground\nX82 is free\nX83 is free\nX84 is free\nempty(T58) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ','(empty(T58), ','(','(!_12, failure(a)), ','(head(T58, X82), ','(head(T54, X82), ','(tail(T58, X83), ','(tail(T54, X84), select(T51, X83, X84))))))) | ?_13 | ','(no(empty(T58)), ','(head(T58, X82), ','(head(T54, X82), ','(tail(T58, X83), ','(tail(T54, X84), select(T51, X83, X84)))))), SCOPE: 12, CLAUSE: 8\n\nT51 is ground\nT58 is ground\nX82 is free\nX83 is free\nX84 is free\nempty(T58) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ','(empty(T58), ','(','(!_12, failure(a)), ','(head(T58, X82), ','(head(T54, X82), ','(tail(T58, X83), ','(tail(T54, X84), select(T51, X83, X84))))))), SCOPE: 14, CLAUSE: 6 | ?_14 | ?_13 | ','(no(empty(T58)), ','(head(T58, X82), ','(head(T54, X82), ','(tail(T58, X83), ','(tail(T54, X84), select(T51, X83, X84)))))), SCOPE: 12, CLAUSE: 8\n\nT51 is ground\nT58 is ground\nX82 is free\nX83 is free\nX84 is free\nempty(T58) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: ?_14 | ?_13 | ','(no(empty(T58)), ','(head(T58, X82), ','(head(T54, X82), ','(tail(T58, X83), ','(tail(T54, X84), select(T51, X83, X84)))))), SCOPE: 12, CLAUSE: 8\n\nT51 is ground\nT58 is ground\nX82 is free\nX83 is free\nX84 is free\nempty(T58) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ?_13 | ','(no(empty(T58)), ','(head(T58, X82), ','(head(T54, X82), ','(tail(T58, X83), ','(tail(T54, X84), select(T51, X83, X84)))))), SCOPE: 12, CLAUSE: 8\n\nT51 is ground\nT58 is ground\nX82 is free\nX83 is free\nX84 is free\nempty(T58) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: ','(no(empty(T58)), ','(head(T58, X82), ','(head(T54, X82), ','(tail(T58, X83), ','(tail(T54, X84), select(T51, X83, X84)))))), SCOPE: 12, CLAUSE: 8\n\nT51 is ground\nT58 is ground\nX82 is free\nX83 is free\nX84 is free\nempty(T58) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: ','(head(T62, X82), ','(head(T54, X82), ','(tail(T62, X83), ','(tail(T54, X84), select(T51, X83, X84)))))\n\nT51 is ground\nT62 is ground\nX82 is free\nX83 is free\nX84 is free\nempty(T62) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: ','(head(T62, X82), ','(head(T54, X82), ','(tail(T62, X83), ','(tail(T54, X84), select(T51, X83, X84))))), SCOPE: 15, CLAUSE: 2 | ','(head(T62, X82), ','(head(T54, X82), ','(tail(T62, X83), ','(tail(T54, X84), select(T51, X83, X84))))), SCOPE: 15, CLAUSE: 3\n\nT51 is ground\nT62 is ground\nX82 is free\nX83 is free\nX84 is free\nempty(T62) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: ','(head(T62, X82), ','(head(T54, X82), ','(tail(T62, X83), ','(tail(T54, X84), select(T51, X83, X84))))), SCOPE: 15, CLAUSE: 3\n\nT51 is ground\nT62 is ground\nX82 is free\nX83 is free\nX84 is free\nempty(T62) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: ','(head(T54, T68), ','(tail(.(T68, T69), X83), ','(tail(T54, X84), select(T51, X83, X84))))\n\nT51 is ground\nT68 is ground\nT69 is ground\nX83 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: ','(head(T54, T68), ','(tail(.(T68, T69), X83), ','(tail(T54, X84), select(T51, X83, X84)))), SCOPE: 16, CLAUSE: 2 | ','(head(T54, T68), ','(tail(.(T68, T69), X83), ','(tail(T54, X84), select(T51, X83, X84)))), SCOPE: 16, CLAUSE: 3\n\nT51 is ground\nT68 is ground\nT69 is ground\nX83 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: ','(head(T54, T68), ','(tail(.(T68, T69), X83), ','(tail(T54, X84), select(T51, X83, X84)))), SCOPE: 16, CLAUSE: 2\n\nT51 is ground\nT68 is ground\nT69 is ground\nX83 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: ','(head(T54, T68), ','(tail(.(T68, T69), X83), ','(tail(T54, X84), select(T51, X83, X84)))), SCOPE: 16, CLAUSE: 3\n\nT51 is ground\nT68 is ground\nT69 is ground\nX83 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ','(tail(.(T75, T69), X83), ','(tail([], X84), select(T51, X83, X84)))\n\nT51 is ground\nT69 is ground\nT75 is ground\nX83 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: ','(tail(.(T75, T69), X83), ','(tail([], X84), select(T51, X83, X84))), SCOPE: 17, CLAUSE: 4 | ','(tail(.(T75, T69), X83), ','(tail([], X84), select(T51, X83, X84))), SCOPE: 17, CLAUSE: 5\n\nT51 is ground\nT69 is ground\nT75 is ground\nX83 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: ','(tail(.(T75, T69), X83), ','(tail([], X84), select(T51, X83, X84))), SCOPE: 17, CLAUSE: 5\n\nT51 is ground\nT69 is ground\nT75 is ground\nX83 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: ','(tail([], X84), select(T51, T84, X84))\n\nT51 is ground\nT84 is ground\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: ','(tail([], X84), select(T51, T84, X84)), SCOPE: 18, CLAUSE: 4 | ','(tail([], X84), select(T51, T84, X84)), SCOPE: 18, CLAUSE: 5\n\nT51 is ground\nT84 is ground\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: ','(tail([], X84), select(T51, T84, X84)), SCOPE: 18, CLAUSE: 4\n\nT51 is ground\nT84 is ground\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: ','(tail([], X84), select(T51, T84, X84)), SCOPE: 18, CLAUSE: 5\n\nT51 is ground\nT84 is ground\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="B: select(T51, T84, [])\n\nT51 is ground\nT84 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: select(T51, T84, []), SCOPE: 19, CLAUSE: 0 | select(T51, T84, []), SCOPE: 19, CLAUSE: 1\n\nT51 is ground\nT84 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: select(T51, T84, []), SCOPE: 19, CLAUSE: 0\n\nT51 is ground\nT84 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: select(T51, T84, []), SCOPE: 19, CLAUSE: 1\n\nT51 is ground\nT84 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: ','(no(empty(T102)), ','(head(T102, T101), tail(T102, [])))\n\nT101 is ground\nT102 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: ','(no(empty(T102)), ','(head(T102, T101), tail(T102, []))), SCOPE: 20, CLAUSE: 7 | ','(no(empty(T102)), ','(head(T102, T101), tail(T102, []))), SCOPE: 20, CLAUSE: 8\n\nT101 is ground\nT102 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: ','(','(call(empty(T105)), ','(!_20, failure(a))), ','(head(T105, T101), tail(T105, []))) | ','(no(empty(T105)), ','(head(T105, T101), tail(T105, []))), SCOPE: 20, CLAUSE: 8\n\nT101 is ground\nT105 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: ','(empty(T105), ','(','(!_20, failure(a)), ','(head(T105, T101), tail(T105, [])))) | ?_21 | ','(no(empty(T105)), ','(head(T105, T101), tail(T105, []))), SCOPE: 20, CLAUSE: 8\n\nT101 is ground\nT105 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: ','(empty(T105), ','(','(!_20, failure(a)), ','(head(T105, T101), tail(T105, [])))), SCOPE: 22, CLAUSE: 6 | ?_22 | ?_21 | ','(no(empty(T105)), ','(head(T105, T101), tail(T105, []))), SCOPE: 20, CLAUSE: 8\n\nT101 is ground\nT105 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: ','(','(!_20, failure(a)), ','(head([], T101), tail([], []))) | ?_22 | ?_21 | ','(no(empty([])), ','(head([], T101), tail([], []))), SCOPE: 20, CLAUSE: 8\n\nT101 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: ?_22 | ?_21 | ','(no(empty(T105)), ','(head(T105, T101), tail(T105, []))), SCOPE: 20, CLAUSE: 8\n\nT101 is ground\nT105 is ground\nempty(T105) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: ','(failure(a), ','(head([], T101), tail([], [])))\n\nT101 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: ','(failure(a), ','(head([], T101), tail([], []))), SCOPE: 23, CLAUSE: 9\n\nT101 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: ?_21 | ','(no(empty(T105)), ','(head(T105, T101), tail(T105, []))), SCOPE: 20, CLAUSE: 8\n\nT101 is ground\nT105 is ground\nempty(T105) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: ','(no(empty(T105)), ','(head(T105, T101), tail(T105, []))), SCOPE: 20, CLAUSE: 8\n\nT101 is ground\nT105 is ground\nempty(T105) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: ','(head(T108, T101), tail(T108, []))\n\nT101 is ground\nT108 is ground\nempty(T108) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: ','(head(T108, T101), tail(T108, [])), SCOPE: 24, CLAUSE: 2 | ','(head(T108, T101), tail(T108, [])), SCOPE: 24, CLAUSE: 3\n\nT101 is ground\nT108 is ground\nempty(T108) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: ','(head(T108, T101), tail(T108, [])), SCOPE: 24, CLAUSE: 3\n\nT101 is ground\nT108 is ground\nempty(T108) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: tail(.(T114, T115), [])\n\nT114 is ground\nT115 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: tail(.(T114, T115), []), SCOPE: 25, CLAUSE: 4 | tail(.(T114, T115), []), SCOPE: 25, CLAUSE: 5\n\nT114 is ground\nT115 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="246: tail(.(T114, T115), []), SCOPE: 25, CLAUSE: 5\n\nT114 is ground\nT115 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
252 [label="252: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
265 [label="265: ','(no(empty(T128)), ','(head(T128, X203), ','(head([], X203), ','(tail(T128, X204), ','(tail([], X205), select(T127, X204, X205))))))\n\nT127 is ground\nT128 is ground\nX203 is free\nX204 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
270 [label="270: ','(no(empty(T128)), ','(head(T128, X203), ','(head([], X203), ','(tail(T128, X204), ','(tail([], X205), select(T127, X204, X205)))))), SCOPE: 26, CLAUSE: 7 | ','(no(empty(T128)), ','(head(T128, X203), ','(head([], X203), ','(tail(T128, X204), ','(tail([], X205), select(T127, X204, X205)))))), SCOPE: 26, CLAUSE: 8\n\nT127 is ground\nT128 is ground\nX203 is free\nX204 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
272 [label="272: ','(','(call(empty(T132)), ','(!_26, failure(a))), ','(head(T132, X203), ','(head([], X203), ','(tail(T132, X204), ','(tail([], X205), select(T127, X204, X205)))))) | ','(no(empty(T132)), ','(head(T132, X203), ','(head([], X203), ','(tail(T132, X204), ','(tail([], X205), select(T127, X204, X205)))))), SCOPE: 26, CLAUSE: 8\n\nT127 is ground\nT132 is ground\nX203 is free\nX204 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
274 [label="274: ','(empty(T132), ','(','(!_26, failure(a)), ','(head(T132, X203), ','(head([], X203), ','(tail(T132, X204), ','(tail([], X205), select(T127, X204, X205))))))) | ?_27 | ','(no(empty(T132)), ','(head(T132, X203), ','(head([], X203), ','(tail(T132, X204), ','(tail([], X205), select(T127, X204, X205)))))), SCOPE: 26, CLAUSE: 8\n\nT127 is ground\nT132 is ground\nX203 is free\nX204 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
276 [label="276: ','(empty(T132), ','(','(!_26, failure(a)), ','(head(T132, X203), ','(head([], X203), ','(tail(T132, X204), ','(tail([], X205), select(T127, X204, X205))))))), SCOPE: 28, CLAUSE: 6 | ?_28 | ?_27 | ','(no(empty(T132)), ','(head(T132, X203), ','(head([], X203), ','(tail(T132, X204), ','(tail([], X205), select(T127, X204, X205)))))), SCOPE: 26, CLAUSE: 8\n\nT127 is ground\nT132 is ground\nX203 is free\nX204 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
277 [label="277: ','(','(!_26, failure(a)), ','(head([], X203), ','(head([], X203), ','(tail([], X204), ','(tail([], X205), select(T127, X204, X205)))))) | ?_28 | ?_27 | ','(no(empty([])), ','(head([], X203), ','(head([], X203), ','(tail([], X204), ','(tail([], X205), select(T127, X204, X205)))))), SCOPE: 26, CLAUSE: 8\n\nT127 is ground\nX203 is free\nX204 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
278 [label="278: ?_28 | ?_27 | ','(no(empty(T132)), ','(head(T132, X203), ','(head([], X203), ','(tail(T132, X204), ','(tail([], X205), select(T127, X204, X205)))))), SCOPE: 26, CLAUSE: 8\n\nT127 is ground\nT132 is ground\nX203 is free\nX204 is free\nX205 is free\nempty(T132) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
281 [label="281: ','(failure(a), ','(head([], X203), ','(head([], X203), ','(tail([], X204), ','(tail([], X205), select(T127, X204, X205))))))\n\nT127 is ground\nX203 is free\nX204 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
285 [label="285: ','(failure(a), ','(head([], X203), ','(head([], X203), ','(tail([], X204), ','(tail([], X205), select(T127, X204, X205)))))), SCOPE: 29, CLAUSE: 9\n\nT127 is ground\nX203 is free\nX204 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
286 [label="286: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
288 [label="288: ?_27 | ','(no(empty(T132)), ','(head(T132, X203), ','(head([], X203), ','(tail(T132, X204), ','(tail([], X205), select(T127, X204, X205)))))), SCOPE: 26, CLAUSE: 8\n\nT127 is ground\nT132 is ground\nX203 is free\nX204 is free\nX205 is free\nempty(T132) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
290 [label="290: ','(no(empty(T132)), ','(head(T132, X203), ','(head([], X203), ','(tail(T132, X204), ','(tail([], X205), select(T127, X204, X205)))))), SCOPE: 26, CLAUSE: 8\n\nT127 is ground\nT132 is ground\nX203 is free\nX204 is free\nX205 is free\nempty(T132) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
299 [label="299: ','(head(T137, X203), ','(head([], X203), ','(tail(T137, X204), ','(tail([], X205), select(T127, X204, X205)))))\n\nT127 is ground\nT137 is ground\nX203 is free\nX204 is free\nX205 is free\nempty(T137) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
300 [label="300: ','(head(T137, X203), ','(head([], X203), ','(tail(T137, X204), ','(tail([], X205), select(T127, X204, X205))))), SCOPE: 30, CLAUSE: 2 | ','(head(T137, X203), ','(head([], X203), ','(tail(T137, X204), ','(tail([], X205), select(T127, X204, X205))))), SCOPE: 30, CLAUSE: 3\n\nT127 is ground\nT137 is ground\nX203 is free\nX204 is free\nX205 is free\nempty(T137) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
302 [label="302: ','(head(T137, X203), ','(head([], X203), ','(tail(T137, X204), ','(tail([], X205), select(T127, X204, X205))))), SCOPE: 30, CLAUSE: 3\n\nT127 is ground\nT137 is ground\nX203 is free\nX204 is free\nX205 is free\nempty(T137) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
306 [label="306: ','(head([], T143), ','(tail(.(T143, T144), X204), ','(tail([], X205), select(T127, X204, X205))))\n\nT127 is ground\nT143 is ground\nT144 is ground\nX204 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
307 [label="307: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
310 [label="310: ','(head([], T143), ','(tail(.(T143, T144), X204), ','(tail([], X205), select(T127, X204, X205)))), SCOPE: 31, CLAUSE: 2 | ','(head([], T143), ','(tail(.(T143, T144), X204), ','(tail([], X205), select(T127, X204, X205)))), SCOPE: 31, CLAUSE: 3\n\nT127 is ground\nT143 is ground\nT144 is ground\nX204 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
315 [label="315: ','(head([], T143), ','(tail(.(T143, T144), X204), ','(tail([], X205), select(T127, X204, X205)))), SCOPE: 31, CLAUSE: 2\n\nT127 is ground\nT143 is ground\nT144 is ground\nX204 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
316 [label="316: ','(head([], T143), ','(tail(.(T143, T144), X204), ','(tail([], X205), select(T127, X204, X205)))), SCOPE: 31, CLAUSE: 3\n\nT127 is ground\nT143 is ground\nT144 is ground\nX204 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
319 [label="319: ','(tail(.(T152, T144), X204), ','(tail([], X205), select(T127, X204, X205)))\n\nT127 is ground\nT144 is ground\nT152 is ground\nX204 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
323 [label="323: ','(tail(.(T152, T144), X204), ','(tail([], X205), select(T127, X204, X205))), SCOPE: 32, CLAUSE: 4 | ','(tail(.(T152, T144), X204), ','(tail([], X205), select(T127, X204, X205))), SCOPE: 32, CLAUSE: 5\n\nT127 is ground\nT144 is ground\nT152 is ground\nX204 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
324 [label="324: ','(tail(.(T152, T144), X204), ','(tail([], X205), select(T127, X204, X205))), SCOPE: 32, CLAUSE: 5\n\nT127 is ground\nT144 is ground\nT152 is ground\nX204 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
331 [label="331: ','(tail([], X205), select(T127, T161, X205))\n\nT127 is ground\nT161 is ground\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
332 [label="332: ','(tail([], X205), select(T127, T161, X205)), SCOPE: 33, CLAUSE: 4 | ','(tail([], X205), select(T127, T161, X205)), SCOPE: 33, CLAUSE: 5\n\nT127 is ground\nT161 is ground\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
334 [label="334: ','(tail([], X205), select(T127, T161, X205)), SCOPE: 33, CLAUSE: 4\n\nT127 is ground\nT161 is ground\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
335 [label="335: ','(tail([], X205), select(T127, T161, X205)), SCOPE: 33, CLAUSE: 5\n\nT127 is ground\nT161 is ground\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
339 [label="339: select(T127, T161, [])\n\nT127 is ground\nT161 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
346 [label="346: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
347 [label="347: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
348 [label="348: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
354 [label="354: ','(tail(.(T174, T69), X83), ','(tail(.(T174, T176), X84), select(T51, X83, X84)))\n\nT51 is ground\nT69 is ground\nT174 is ground\nX83 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
355 [label="355: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
356 [label="356: ','(tail(.(T174, T69), X83), ','(tail(.(T174, T176), X84), select(T51, X83, X84))), SCOPE: 34, CLAUSE: 4 | ','(tail(.(T174, T69), X83), ','(tail(.(T174, T176), X84), select(T51, X83, X84))), SCOPE: 34, CLAUSE: 5\n\nT51 is ground\nT69 is ground\nT174 is ground\nX83 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
357 [label="357: ','(tail(.(T174, T69), X83), ','(tail(.(T174, T176), X84), select(T51, X83, X84))), SCOPE: 34, CLAUSE: 5\n\nT51 is ground\nT69 is ground\nT174 is ground\nX83 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
365 [label="365: ','(tail(.(T184, T176), X84), select(T51, T185, X84))\n\nT51 is ground\nT184 is ground\nT185 is ground\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
366 [label="366: ','(tail(.(T184, T176), X84), select(T51, T185, X84)), SCOPE: 35, CLAUSE: 4 | ','(tail(.(T184, T176), X84), select(T51, T185, X84)), SCOPE: 35, CLAUSE: 5\n\nT51 is ground\nT184 is ground\nT185 is ground\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
367 [label="367: ','(tail(.(T184, T176), X84), select(T51, T185, X84)), SCOPE: 35, CLAUSE: 5\n\nT51 is ground\nT184 is ground\nT185 is ground\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
372 [label="372: select(T51, T185, T198)\n\nT51 is ground\nT185 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
373 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 373 [arrowhead = none ];
373 -> 5;

374 [label="ONLY EVAL with clause\nselect(X8, X9, X10) :- ','(no(empty(X9)), ','(head(X9, X8), tail(X9, X10))).\nand substitutionT1 -> T7,\nX8 -> T7,\nT2 -> T8,\nX9 -> T8,\nT3 -> T10,\nX10 -> T10,\nT9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 374 [arrowhead = none ];
374 -> 7;

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

376 [label="ONLY EVAL with clause\nno(X13) :- ','(call(X13), ','(!_2, failure(a))).\nand substitutionT8 -> T13,\nX13 -> empty(T13)", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 376 [arrowhead = none ];
376 -> 13;

377 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
13 -> 377 [arrowhead = none ];
377 -> 14;

378 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
14 -> 378 [arrowhead = none ];
378 -> 18;

379 [label="EVAL with clause\nempty([]).\nand substitutionT13 -> []", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 379 [arrowhead = none ];
379 -> 21;

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

381 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 381 [arrowhead = none ];
381 -> 28;

382 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 382 [arrowhead = none ];
382 -> 66;

383 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
28 -> 383 [arrowhead = none ];
383 -> 34;

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

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

386 [label="ONLY EVAL with clause\nselect(X28, X29, X30) :- ','(no(empty(X29)), ','(head(X29, X31), ','(head(X30, X31), ','(tail(X29, X32), ','(tail(X30, X33), select(X28, X32, X33)))))).\nand substitutionT7 -> T20,\nX28 -> T20,\nX29 -> [],\nT3 -> T22,\nX30 -> T22,\nT21 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 386 [arrowhead = none ];
386 -> 49;

387 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
40 -> 387 [arrowhead = none ];
387 -> 42;

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

389 [label="ONLY EVAL with clause\nno(X41) :- ','(call(X41), ','(!_6, failure(a))).\nand substitutionX41 -> empty([])", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 389 [arrowhead = none ];
389 -> 57;

390 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
57 -> 390 [arrowhead = none ];
390 -> 58;

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

392 [label="ONLY EVAL with clause\nempty([]).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 392 [arrowhead = none ];
392 -> 60;

393 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 393 [arrowhead = none ];
393 -> 62;

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

395 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 395 [arrowhead = none ];
395 -> 65;

396 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
66 -> 396 [arrowhead = none ];
396 -> 67;

397 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
67 -> 397 [arrowhead = none ];
397 -> 69;

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

399 [label="ONLY EVAL with clause\nno(X51).\nand substitutionT13 -> T29,\nX51 -> empty(T29)", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 399 [arrowhead = none ];
399 -> 72;

400 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
70 -> 400 [arrowhead = none ];
400 -> 108;

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

402 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T29), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
74 -> 402 [arrowhead = none ];
402 -> 76;

403 [label="EVAL with clause\nhead(.(X57, X58), X57).\nand substitutionX57 -> T35,\nX58 -> T36,\nT29 -> .(T35, T36),\nT7 -> T35", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 403 [arrowhead = none ];
403 -> 83;

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

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

406 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 406 [arrowhead = none ];
406 -> 90;

407 [label="EVAL with clause\ntail(.(X63, X64), X64).\nand substitutionT35 -> T41,\nX63 -> T41,\nT36 -> T42,\nX64 -> T42,\nT10 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
90 -> 407 [arrowhead = none ];
407 -> 98;

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

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

410 [label="ONLY EVAL with clause\nselect(X79, X80, X81) :- ','(no(empty(X80)), ','(head(X80, X82), ','(head(X81, X82), ','(tail(X80, X83), ','(tail(X81, X84), select(X79, X83, X84)))))).\nand substitutionT7 -> T51,\nX79 -> T51,\nT13 -> T52,\nX80 -> T52,\nT3 -> T54,\nX81 -> T54,\nT53 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 410 [arrowhead = none ];
410 -> 120;

411 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
120 -> 411 [arrowhead = none ];
411 -> 122;

412 [label="ONLY EVAL with clause\nno(X92) :- ','(call(X92), ','(!_12, failure(a))).\nand substitutionT52 -> T58,\nX92 -> empty(T58)", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 412 [arrowhead = none ];
412 -> 127;

413 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
127 -> 413 [arrowhead = none ];
413 -> 129;

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

415 [label="BACKTRACK\nfor clause: empty([])\nwith clash: (empty(T58), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
130 -> 415 [arrowhead = none ];
415 -> 133;

416 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
133 -> 416 [arrowhead = none ];
416 -> 135;

417 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
135 -> 417 [arrowhead = none ];
417 -> 136;

418 [label="ONLY EVAL with clause\nno(X100).\nand substitutionT58 -> T62,\nX100 -> empty(T62)", fontsize=14, style = filled, fillcolor = lightblue];
136 -> 418 [arrowhead = none ];
418 -> 142;

419 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
142 -> 419 [arrowhead = none ];
419 -> 145;

420 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T62), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
145 -> 420 [arrowhead = none ];
420 -> 146;

421 [label="EVAL with clause\nhead(.(X112, X113), X112).\nand substitutionX112 -> T68,\nX113 -> T69,\nT62 -> .(T68, T69),\nX82 -> T68", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 421 [arrowhead = none ];
421 -> 151;

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

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

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

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

426 [label="EVAL with clause\nhead([], X123).\nand substitutionT54 -> [],\nT68 -> T75,\nX123 -> T75", fontsize=14, style = filled, fillcolor = lightblue];
157 -> 426 [arrowhead = none ];
426 -> 161;

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

428 [label="EVAL with clause\nhead(.(X298, X299), X298).\nand substitutionX298 -> T174,\nX299 -> T176,\nT54 -> .(T174, T176),\nT68 -> T174,\nT175 -> T176", fontsize=14, style = filled, fillcolor = lightblue];
158 -> 428 [arrowhead = none ];
428 -> 354;

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

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

431 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
165 -> 431 [arrowhead = none ];
431 -> 167;

432 [label="ONLY EVAL with clause\ntail(.(X137, X138), X138).\nand substitutionT75 -> T83,\nX137 -> T83,\nT69 -> T84,\nX138 -> T84,\nX83 -> T84", fontsize=14, style = filled, fillcolor = lightblue];
167 -> 432 [arrowhead = none ];
432 -> 173;

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

434 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
176 -> 434 [arrowhead = none ];
434 -> 177;

435 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
176 -> 435 [arrowhead = none ];
435 -> 178;

436 [label="ONLY EVAL with clause\ntail([], []).\nand substitutionX84 -> []", fontsize=14, style = filled, fillcolor = lightblue];
177 -> 436 [arrowhead = none ];
436 -> 181;

437 [label="BACKTRACK\nfor clause: tail(.(X3, T), T)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
178 -> 437 [arrowhead = none ];
437 -> 348;

438 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
181 -> 438 [arrowhead = none ];
438 -> 186;

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

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

441 [label="ONLY EVAL with clause\nselect(X164, X165, X166) :- ','(no(empty(X165)), ','(head(X165, X164), tail(X165, X166))).\nand substitutionT51 -> T101,\nX164 -> T101,\nT84 -> T102,\nX165 -> T102,\nX166 -> []", fontsize=14, style = filled, fillcolor = lightblue];
197 -> 441 [arrowhead = none ];
441 -> 206;

442 [label="ONLY EVAL with clause\nselect(X200, X201, X202) :- ','(no(empty(X201)), ','(head(X201, X203), ','(head(X202, X203), ','(tail(X201, X204), ','(tail(X202, X205), select(X200, X204, X205)))))).\nand substitutionT51 -> T127,\nX200 -> T127,\nT84 -> T128,\nX201 -> T128,\nX202 -> []", fontsize=14, style = filled, fillcolor = lightblue];
198 -> 442 [arrowhead = none ];
442 -> 265;

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

444 [label="ONLY EVAL with clause\nno(X169) :- ','(call(X169), ','(!_20, failure(a))).\nand substitutionT102 -> T105,\nX169 -> empty(T105)", fontsize=14, style = filled, fillcolor = lightblue];
207 -> 444 [arrowhead = none ];
444 -> 209;

445 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
209 -> 445 [arrowhead = none ];
445 -> 213;

446 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
213 -> 446 [arrowhead = none ];
446 -> 216;

447 [label="EVAL with clause\nempty([]).\nand substitutionT105 -> []", fontsize=14, style = filled, fillcolor = lightblue];
216 -> 447 [arrowhead = none ];
447 -> 217;

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

449 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
217 -> 449 [arrowhead = none ];
449 -> 219;

450 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
218 -> 450 [arrowhead = none ];
450 -> 224;

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

452 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
221 -> 452 [arrowhead = none ];
452 -> 223;

453 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
224 -> 453 [arrowhead = none ];
453 -> 228;

454 [label="ONLY EVAL with clause\nno(X172).\nand substitutionT105 -> T108,\nX172 -> empty(T108)", fontsize=14, style = filled, fillcolor = lightblue];
228 -> 454 [arrowhead = none ];
454 -> 232;

455 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
232 -> 455 [arrowhead = none ];
455 -> 234;

456 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T108), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
234 -> 456 [arrowhead = none ];
456 -> 238;

457 [label="EVAL with clause\nhead(.(X178, X179), X178).\nand substitutionX178 -> T114,\nX179 -> T115,\nT108 -> .(T114, T115),\nT101 -> T114", fontsize=14, style = filled, fillcolor = lightblue];
238 -> 457 [arrowhead = none ];
457 -> 242;

458 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
238 -> 458 [arrowhead = none ];
458 -> 243;

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

460 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
245 -> 460 [arrowhead = none ];
460 -> 246;

461 [label="EVAL with clause\ntail(.(X184, X185), X185).\nand substitutionT114 -> T120,\nX184 -> T120,\nT115 -> [],\nX185 -> [],\nT121 -> []", fontsize=14, style = filled, fillcolor = lightblue];
246 -> 461 [arrowhead = none ];
461 -> 249;

462 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
246 -> 462 [arrowhead = none ];
462 -> 252;

463 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
249 -> 463 [arrowhead = none ];
463 -> 254;

464 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
265 -> 464 [arrowhead = none ];
464 -> 270;

465 [label="ONLY EVAL with clause\nno(X213) :- ','(call(X213), ','(!_26, failure(a))).\nand substitutionT128 -> T132,\nX213 -> empty(T132)", fontsize=14, style = filled, fillcolor = lightblue];
270 -> 465 [arrowhead = none ];
465 -> 272;

466 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
272 -> 466 [arrowhead = none ];
466 -> 274;

467 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
274 -> 467 [arrowhead = none ];
467 -> 276;

468 [label="EVAL with clause\nempty([]).\nand substitutionT132 -> []", fontsize=14, style = filled, fillcolor = lightblue];
276 -> 468 [arrowhead = none ];
468 -> 277;

469 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
276 -> 469 [arrowhead = none ];
469 -> 278;

470 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
277 -> 470 [arrowhead = none ];
470 -> 281;

471 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
278 -> 471 [arrowhead = none ];
471 -> 288;

472 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
281 -> 472 [arrowhead = none ];
472 -> 285;

473 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
285 -> 473 [arrowhead = none ];
473 -> 286;

474 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
288 -> 474 [arrowhead = none ];
474 -> 290;

475 [label="ONLY EVAL with clause\nno(X226).\nand substitutionT132 -> T137,\nX226 -> empty(T137)", fontsize=14, style = filled, fillcolor = lightblue];
290 -> 475 [arrowhead = none ];
475 -> 299;

476 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
299 -> 476 [arrowhead = none ];
476 -> 300;

477 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T137), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
300 -> 477 [arrowhead = none ];
477 -> 302;

478 [label="EVAL with clause\nhead(.(X238, X239), X238).\nand substitutionX238 -> T143,\nX239 -> T144,\nT137 -> .(T143, T144),\nX203 -> T143", fontsize=14, style = filled, fillcolor = lightblue];
302 -> 478 [arrowhead = none ];
478 -> 306;

479 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
302 -> 479 [arrowhead = none ];
479 -> 307;

480 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
306 -> 480 [arrowhead = none ];
480 -> 310;

481 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
310 -> 481 [arrowhead = none ];
481 -> 315;

482 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
310 -> 482 [arrowhead = none ];
482 -> 316;

483 [label="ONLY EVAL with clause\nhead([], X259).\nand substitutionT143 -> T152,\nX259 -> T152", fontsize=14, style = filled, fillcolor = lightblue];
315 -> 483 [arrowhead = none ];
483 -> 319;

484 [label="BACKTRACK\nfor clause: head(.(H, X2), H)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
316 -> 484 [arrowhead = none ];
484 -> 347;

485 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
319 -> 485 [arrowhead = none ];
485 -> 323;

486 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
323 -> 486 [arrowhead = none ];
486 -> 324;

487 [label="ONLY EVAL with clause\ntail(.(X273, X274), X274).\nand substitutionT152 -> T160,\nX273 -> T160,\nT144 -> T161,\nX274 -> T161,\nX204 -> T161", fontsize=14, style = filled, fillcolor = lightblue];
324 -> 487 [arrowhead = none ];
487 -> 331;

488 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
331 -> 488 [arrowhead = none ];
488 -> 332;

489 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
332 -> 489 [arrowhead = none ];
489 -> 334;

490 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
332 -> 490 [arrowhead = none ];
490 -> 335;

491 [label="ONLY EVAL with clause\ntail([], []).\nand substitutionX205 -> []", fontsize=14, style = filled, fillcolor = lightblue];
334 -> 491 [arrowhead = none ];
491 -> 339;

492 [label="BACKTRACK\nfor clause: tail(.(X3, T), T)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
335 -> 492 [arrowhead = none ];
492 -> 346;

493 [label="INSTANCE with matching:\nT51 -> T127\nT84 -> T161", fontsize=14, style = filled, fillcolor = lightgrey];
339 -> 493 [arrowhead = none , style=dashed];
493 -> 181[style=dashed];

494 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
354 -> 494 [arrowhead = none ];
494 -> 356;

495 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
356 -> 495 [arrowhead = none ];
495 -> 357;

496 [label="ONLY EVAL with clause\ntail(.(X313, X314), X314).\nand substitutionT174 -> T184,\nX313 -> T184,\nT69 -> T185,\nX314 -> T185,\nX83 -> T185", fontsize=14, style = filled, fillcolor = lightblue];
357 -> 496 [arrowhead = none ];
496 -> 365;

497 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
365 -> 497 [arrowhead = none ];
497 -> 366;

498 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
366 -> 498 [arrowhead = none ];
498 -> 367;

499 [label="ONLY EVAL with clause\ntail(.(X326, X327), X327).\nand substitutionT184 -> T196,\nX326 -> T196,\nT176 -> T198,\nX327 -> T198,\nX84 -> T198,\nT197 -> T198", fontsize=14, style = filled, fillcolor = lightblue];
367 -> 499 [arrowhead = none ];
499 -> 372;

500 [label="INSTANCE with matching:\nT1 -> T51\nT2 -> T185\nT3 -> T198", fontsize=14, style = filled, fillcolor = lightgrey];
372 -> 500 [arrowhead = none , style=dashed];
500 -> 1[style=dashed];

}

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

selectA_in_gga(T41, .(T41, T42), T42) → selectA_out_gga(T41, .(T41, T42), T42)
selectA_in_gga(T51, .(T83, T84), []) → U1_gga(T51, T83, T84, selectB_in_gg(T51, T84))
selectB_in_gg(T120, .(T120, [])) → selectB_out_gg(T120, .(T120, []))
selectB_in_gg(T127, .(T160, T161)) → U3_gg(T127, T160, T161, selectB_in_gg(T127, T161))
U3_gg(T127, T160, T161, selectB_out_gg(T127, T161)) → selectB_out_gg(T127, .(T160, T161))
U1_gga(T51, T83, T84, selectB_out_gg(T51, T84)) → selectA_out_gga(T51, .(T83, T84), [])
selectA_in_gga(T51, .(T196, T185), .(T196, T198)) → U2_gga(T51, T196, T185, T198, selectA_in_gga(T51, T185, T198))
U2_gga(T51, T196, T185, T198, selectA_out_gga(T51, T185, T198)) → selectA_out_gga(T51, .(T196, T185), .(T196, T198))

The argument filtering Pi contains the following mapping:
selectA_in_gga(x1, x2, x3)  =  selectA_in_gga(x1, x2)
.(x1, x2)  =  .(x1, x2)
selectA_out_gga(x1, x2, x3)  =  selectA_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x3, x4)
selectB_in_gg(x1, x2)  =  selectB_in_gg(x1, x2)
[]  =  []
selectB_out_gg(x1, x2)  =  selectB_out_gg(x1, x2)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x1, x2, x3, x4)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

SELECTA_IN_GGA(T51, .(T83, T84), []) → U1_GGA(T51, T83, T84, selectB_in_gg(T51, T84))
SELECTA_IN_GGA(T51, .(T83, T84), []) → SELECTB_IN_GG(T51, T84)
SELECTB_IN_GG(T127, .(T160, T161)) → U3_GG(T127, T160, T161, selectB_in_gg(T127, T161))
SELECTB_IN_GG(T127, .(T160, T161)) → SELECTB_IN_GG(T127, T161)
SELECTA_IN_GGA(T51, .(T196, T185), .(T196, T198)) → U2_GGA(T51, T196, T185, T198, selectA_in_gga(T51, T185, T198))
SELECTA_IN_GGA(T51, .(T196, T185), .(T196, T198)) → SELECTA_IN_GGA(T51, T185, T198)

The TRS R consists of the following rules:

selectA_in_gga(T41, .(T41, T42), T42) → selectA_out_gga(T41, .(T41, T42), T42)
selectA_in_gga(T51, .(T83, T84), []) → U1_gga(T51, T83, T84, selectB_in_gg(T51, T84))
selectB_in_gg(T120, .(T120, [])) → selectB_out_gg(T120, .(T120, []))
selectB_in_gg(T127, .(T160, T161)) → U3_gg(T127, T160, T161, selectB_in_gg(T127, T161))
U3_gg(T127, T160, T161, selectB_out_gg(T127, T161)) → selectB_out_gg(T127, .(T160, T161))
U1_gga(T51, T83, T84, selectB_out_gg(T51, T84)) → selectA_out_gga(T51, .(T83, T84), [])
selectA_in_gga(T51, .(T196, T185), .(T196, T198)) → U2_gga(T51, T196, T185, T198, selectA_in_gga(T51, T185, T198))
U2_gga(T51, T196, T185, T198, selectA_out_gga(T51, T185, T198)) → selectA_out_gga(T51, .(T196, T185), .(T196, T198))

The argument filtering Pi contains the following mapping:
selectA_in_gga(x1, x2, x3)  =  selectA_in_gga(x1, x2)
.(x1, x2)  =  .(x1, x2)
selectA_out_gga(x1, x2, x3)  =  selectA_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x3, x4)
selectB_in_gg(x1, x2)  =  selectB_in_gg(x1, x2)
[]  =  []
selectB_out_gg(x1, x2)  =  selectB_out_gg(x1, x2)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x1, x2, x3, x4)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
SELECTA_IN_GGA(x1, x2, x3)  =  SELECTA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x3, x4)
SELECTB_IN_GG(x1, x2)  =  SELECTB_IN_GG(x1, x2)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x1, x2, x3, x4)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x2, x3, x5)

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

(4) Obligation:

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

SELECTA_IN_GGA(T51, .(T83, T84), []) → U1_GGA(T51, T83, T84, selectB_in_gg(T51, T84))
SELECTA_IN_GGA(T51, .(T83, T84), []) → SELECTB_IN_GG(T51, T84)
SELECTB_IN_GG(T127, .(T160, T161)) → U3_GG(T127, T160, T161, selectB_in_gg(T127, T161))
SELECTB_IN_GG(T127, .(T160, T161)) → SELECTB_IN_GG(T127, T161)
SELECTA_IN_GGA(T51, .(T196, T185), .(T196, T198)) → U2_GGA(T51, T196, T185, T198, selectA_in_gga(T51, T185, T198))
SELECTA_IN_GGA(T51, .(T196, T185), .(T196, T198)) → SELECTA_IN_GGA(T51, T185, T198)

The TRS R consists of the following rules:

selectA_in_gga(T41, .(T41, T42), T42) → selectA_out_gga(T41, .(T41, T42), T42)
selectA_in_gga(T51, .(T83, T84), []) → U1_gga(T51, T83, T84, selectB_in_gg(T51, T84))
selectB_in_gg(T120, .(T120, [])) → selectB_out_gg(T120, .(T120, []))
selectB_in_gg(T127, .(T160, T161)) → U3_gg(T127, T160, T161, selectB_in_gg(T127, T161))
U3_gg(T127, T160, T161, selectB_out_gg(T127, T161)) → selectB_out_gg(T127, .(T160, T161))
U1_gga(T51, T83, T84, selectB_out_gg(T51, T84)) → selectA_out_gga(T51, .(T83, T84), [])
selectA_in_gga(T51, .(T196, T185), .(T196, T198)) → U2_gga(T51, T196, T185, T198, selectA_in_gga(T51, T185, T198))
U2_gga(T51, T196, T185, T198, selectA_out_gga(T51, T185, T198)) → selectA_out_gga(T51, .(T196, T185), .(T196, T198))

The argument filtering Pi contains the following mapping:
selectA_in_gga(x1, x2, x3)  =  selectA_in_gga(x1, x2)
.(x1, x2)  =  .(x1, x2)
selectA_out_gga(x1, x2, x3)  =  selectA_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x3, x4)
selectB_in_gg(x1, x2)  =  selectB_in_gg(x1, x2)
[]  =  []
selectB_out_gg(x1, x2)  =  selectB_out_gg(x1, x2)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x1, x2, x3, x4)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
SELECTA_IN_GGA(x1, x2, x3)  =  SELECTA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x3, x4)
SELECTB_IN_GG(x1, x2)  =  SELECTB_IN_GG(x1, x2)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x1, x2, x3, x4)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x2, x3, x5)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 4 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

SELECTB_IN_GG(T127, .(T160, T161)) → SELECTB_IN_GG(T127, T161)

The TRS R consists of the following rules:

selectA_in_gga(T41, .(T41, T42), T42) → selectA_out_gga(T41, .(T41, T42), T42)
selectA_in_gga(T51, .(T83, T84), []) → U1_gga(T51, T83, T84, selectB_in_gg(T51, T84))
selectB_in_gg(T120, .(T120, [])) → selectB_out_gg(T120, .(T120, []))
selectB_in_gg(T127, .(T160, T161)) → U3_gg(T127, T160, T161, selectB_in_gg(T127, T161))
U3_gg(T127, T160, T161, selectB_out_gg(T127, T161)) → selectB_out_gg(T127, .(T160, T161))
U1_gga(T51, T83, T84, selectB_out_gg(T51, T84)) → selectA_out_gga(T51, .(T83, T84), [])
selectA_in_gga(T51, .(T196, T185), .(T196, T198)) → U2_gga(T51, T196, T185, T198, selectA_in_gga(T51, T185, T198))
U2_gga(T51, T196, T185, T198, selectA_out_gga(T51, T185, T198)) → selectA_out_gga(T51, .(T196, T185), .(T196, T198))

The argument filtering Pi contains the following mapping:
selectA_in_gga(x1, x2, x3)  =  selectA_in_gga(x1, x2)
.(x1, x2)  =  .(x1, x2)
selectA_out_gga(x1, x2, x3)  =  selectA_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x3, x4)
selectB_in_gg(x1, x2)  =  selectB_in_gg(x1, x2)
[]  =  []
selectB_out_gg(x1, x2)  =  selectB_out_gg(x1, x2)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x1, x2, x3, x4)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
SELECTB_IN_GG(x1, x2)  =  SELECTB_IN_GG(x1, x2)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

SELECTB_IN_GG(T127, .(T160, T161)) → SELECTB_IN_GG(T127, T161)

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

(10) PiDPToQDPProof (EQUIVALENT transformation)

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

(11) Obligation:

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

SELECTB_IN_GG(T127, .(T160, T161)) → SELECTB_IN_GG(T127, T161)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• SELECTB_IN_GG(T127, .(T160, T161)) → SELECTB_IN_GG(T127, T161)
  The graph contains the following edges 1 >= 1, 2 > 2

(13) YES

(14) Obligation:

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

SELECTA_IN_GGA(T51, .(T196, T185), .(T196, T198)) → SELECTA_IN_GGA(T51, T185, T198)

The TRS R consists of the following rules:

selectA_in_gga(T41, .(T41, T42), T42) → selectA_out_gga(T41, .(T41, T42), T42)
selectA_in_gga(T51, .(T83, T84), []) → U1_gga(T51, T83, T84, selectB_in_gg(T51, T84))
selectB_in_gg(T120, .(T120, [])) → selectB_out_gg(T120, .(T120, []))
selectB_in_gg(T127, .(T160, T161)) → U3_gg(T127, T160, T161, selectB_in_gg(T127, T161))
U3_gg(T127, T160, T161, selectB_out_gg(T127, T161)) → selectB_out_gg(T127, .(T160, T161))
U1_gga(T51, T83, T84, selectB_out_gg(T51, T84)) → selectA_out_gga(T51, .(T83, T84), [])
selectA_in_gga(T51, .(T196, T185), .(T196, T198)) → U2_gga(T51, T196, T185, T198, selectA_in_gga(T51, T185, T198))
U2_gga(T51, T196, T185, T198, selectA_out_gga(T51, T185, T198)) → selectA_out_gga(T51, .(T196, T185), .(T196, T198))

The argument filtering Pi contains the following mapping:
selectA_in_gga(x1, x2, x3)  =  selectA_in_gga(x1, x2)
.(x1, x2)  =  .(x1, x2)
selectA_out_gga(x1, x2, x3)  =  selectA_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x3, x4)
selectB_in_gg(x1, x2)  =  selectB_in_gg(x1, x2)
[]  =  []
selectB_out_gg(x1, x2)  =  selectB_out_gg(x1, x2)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x1, x2, x3, x4)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
SELECTA_IN_GGA(x1, x2, x3)  =  SELECTA_IN_GGA(x1, x2)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

SELECTA_IN_GGA(T51, .(T196, T185), .(T196, T198)) → SELECTA_IN_GGA(T51, T185, T198)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
SELECTA_IN_GGA(x1, x2, x3)  =  SELECTA_IN_GGA(x1, x2)

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

SELECTA_IN_GGA(T51, .(T196, T185)) → SELECTA_IN_GGA(T51, T185)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• SELECTA_IN_GGA(T51, .(T196, T185)) → SELECTA_IN_GGA(T51, T185)
  The graph contains the following edges 1 >= 1, 2 > 2

(20) YES