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

(0) Obligation:

Clauses:

select(X, .(X, Xs), Xs).
select(X, .(Y, Xs), .(Y, Zs)) :- select(X, Xs, Zs).

Query: select(a,a,g)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: select(T1, T2, T3)\n\nT3 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\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: select(T1, T2, T3), SCOPE: 1, CLAUSE: 0\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: select(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: select(T26, T27, T25)\n\nT25 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 27 [arrowhead = none ];
27 -> 5;

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

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

30 [label="EVAL with clause\nselect(X9, .(X9, X10), X10).\nand substitutionT1 -> T12,\nX9 -> T12,\nX10 -> T13,\nT2 -> .(T12, T13),\nT3 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 30 [arrowhead = none ];
30 -> 11;

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

32 [label="EVAL with clause\nselect(X19, .(X20, X21), .(X20, X22)) :- select(X19, X21, X22).\nand substitutionT1 -> T26,\nX19 -> T26,\nX20 -> T23,\nX21 -> T27,\nT2 -> .(T23, T27),\nX22 -> T25,\nT3 -> .(T23, T25),\nT22 -> T26,\nT24 -> T27", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 32 [arrowhead = none ];
32 -> 24;

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

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

35 [label="INSTANCE with matching:\nT1 -> T26\nT2 -> T27\nT3 -> T25", fontsize=14, style = filled, fillcolor = lightgrey];
24 -> 35 [arrowhead = none , style=dashed];
35 -> 2[style=dashed];

}

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f2_in(T13) → f2_out1
f2_in(.(T23, T25)) → U1(f2_in(T25), .(T23, T25))
U1(f2_out1, .(T23, T25)) → f2_out1

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 1 + x₁ + 2·x₂   
POL(U1(x₁, x₂)) = x₁ + x₂   
POL(f2_in(x₁)) = 2 + 2·x₁   
POL(f2_out1) = 0   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

f2_in(T13) → f2_out1
f2_in(.(T23, T25)) → U1(f2_in(T25), .(T23, T25))
U1(f2_out1, .(T23, T25)) → f2_out1

(4) Obligation:

Q restricted rewrite system:
R is empty.
Q is empty.

(5) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(6) YES