(0) Obligation:

Clauses:

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

Query: select(g,g,a)

(1) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, .(z0, z1)) → f2_out1
f2_in(z0, .(z0, z1)) → U1(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U2(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z1, z2)) → U3(f2_in(z0, z2), z0, .(z1, z2))
U1(f2_out1, z0, .(z0, z1)) → f2_out1
U2(f2_out1, z0, .(z0, z1)) → f2_out1
U3(f2_out1, z0, .(z1, z2)) → f2_out1
Tuples:

F2_IN(z0, .(z0, z1)) → c1(U1'(f2_in(z0, z1), z0, .(z0, z1)), F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(U2'(f2_in(z0, z1), z0, .(z0, z1)), F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c3(U3'(f2_in(z0, z2), z0, .(z1, z2)), F2_IN(z0, z2))
S tuples:

F2_IN(z0, .(z0, z1)) → c1(U1'(f2_in(z0, z1), z0, .(z0, z1)), F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(U2'(f2_in(z0, z1), z0, .(z0, z1)), F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c3(U3'(f2_in(z0, z2), z0, .(z1, z2)), F2_IN(z0, z2))
K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, U3

Defined Pair Symbols:

F2_IN

Compound Symbols:

c1, c2, c3

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

Removed 3 trailing tuple parts

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, .(z0, z1)) → f2_out1
f2_in(z0, .(z0, z1)) → U1(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U2(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z1, z2)) → U3(f2_in(z0, z2), z0, .(z1, z2))
U1(f2_out1, z0, .(z0, z1)) → f2_out1
U2(f2_out1, z0, .(z0, z1)) → f2_out1
U3(f2_out1, z0, .(z1, z2)) → f2_out1
Tuples:

F2_IN(z0, .(z0, z1)) → c1(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c3(F2_IN(z0, z2))
S tuples:

F2_IN(z0, .(z0, z1)) → c1(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c3(F2_IN(z0, z2))
K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, U3

Defined Pair Symbols:

F2_IN

Compound Symbols:

c1, c2, c3

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

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

F2_IN(z0, .(z0, z1)) → c1(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c3(F2_IN(z0, z2))
We considered the (Usable) Rules:none
And the Tuples:

F2_IN(z0, .(z0, z1)) → c1(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c3(F2_IN(z0, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x1, x2)) = [2] + x2   
POL(F2_IN(x1, x2)) = [2]x2   
POL(c1(x1)) = x1   
POL(c2(x1)) = x1   
POL(c3(x1)) = x1   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, .(z0, z1)) → f2_out1
f2_in(z0, .(z0, z1)) → U1(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U2(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z1, z2)) → U3(f2_in(z0, z2), z0, .(z1, z2))
U1(f2_out1, z0, .(z0, z1)) → f2_out1
U2(f2_out1, z0, .(z0, z1)) → f2_out1
U3(f2_out1, z0, .(z1, z2)) → f2_out1
Tuples:

F2_IN(z0, .(z0, z1)) → c1(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c3(F2_IN(z0, z2))
S tuples:none
K tuples:

F2_IN(z0, .(z0, z1)) → c1(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c3(F2_IN(z0, z2))
Defined Rule Symbols:

f2_in, U1, U2, U3

Defined Pair Symbols:

F2_IN

Compound Symbols:

c1, c2, c3

(7) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(8) BOUNDS(O(1), O(1))

(9) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, .(z0, z1)) → f1_out1
f1_in(z0, .(z0, z1)) → U1(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U2(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z1, z2)) → U3(f1_in(z0, z2), z0, .(z1, z2))
U1(f1_out1, z0, .(z0, z1)) → f1_out1
U2(f1_out1, z0, .(z0, z1)) → f1_out1
U3(f1_out1, z0, .(z1, z2)) → f1_out1
Tuples:

F1_IN(z0, .(z0, z1)) → c1(U1'(f1_in(z0, z1), z0, .(z0, z1)), F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(U2'(f1_in(z0, z1), z0, .(z0, z1)), F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c3(U3'(f1_in(z0, z2), z0, .(z1, z2)), F1_IN(z0, z2))
S tuples:

F1_IN(z0, .(z0, z1)) → c1(U1'(f1_in(z0, z1), z0, .(z0, z1)), F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(U2'(f1_in(z0, z1), z0, .(z0, z1)), F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c3(U3'(f1_in(z0, z2), z0, .(z1, z2)), F1_IN(z0, z2))
K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, U3

Defined Pair Symbols:

F1_IN

Compound Symbols:

c1, c2, c3

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

Removed 3 trailing tuple parts

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, .(z0, z1)) → f1_out1
f1_in(z0, .(z0, z1)) → U1(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U2(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z1, z2)) → U3(f1_in(z0, z2), z0, .(z1, z2))
U1(f1_out1, z0, .(z0, z1)) → f1_out1
U2(f1_out1, z0, .(z0, z1)) → f1_out1
U3(f1_out1, z0, .(z1, z2)) → f1_out1
Tuples:

F1_IN(z0, .(z0, z1)) → c1(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c3(F1_IN(z0, z2))
S tuples:

F1_IN(z0, .(z0, z1)) → c1(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c3(F1_IN(z0, z2))
K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, U3

Defined Pair Symbols:

F1_IN

Compound Symbols:

c1, c2, c3

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

F1_IN(z0, .(z0, z1)) → c1(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c3(F1_IN(z0, z2))
We considered the (Usable) Rules:none
And the Tuples:

F1_IN(z0, .(z0, z1)) → c1(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c3(F1_IN(z0, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x1, x2)) = [2] + x2   
POL(F1_IN(x1, x2)) = [2]x2   
POL(c1(x1)) = x1   
POL(c2(x1)) = x1   
POL(c3(x1)) = x1   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, .(z0, z1)) → f1_out1
f1_in(z0, .(z0, z1)) → U1(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U2(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z1, z2)) → U3(f1_in(z0, z2), z0, .(z1, z2))
U1(f1_out1, z0, .(z0, z1)) → f1_out1
U2(f1_out1, z0, .(z0, z1)) → f1_out1
U3(f1_out1, z0, .(z1, z2)) → f1_out1
Tuples:

F1_IN(z0, .(z0, z1)) → c1(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c3(F1_IN(z0, z2))
S tuples:none
K tuples:

F1_IN(z0, .(z0, z1)) → c1(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c3(F1_IN(z0, z2))
Defined Rule Symbols:

f1_in, U1, U2, U3

Defined Pair Symbols:

F1_IN

Compound Symbols:

c1, c2, c3