(0) Obligation:

Clauses:

f([], RES, RES).
f(.(Head, Tail), X, RES) :- g(Tail, X, .(Head, Tail), RES).
g(A, B, C, RES) :- f(A, .(B, C), RES).

Query: f(g,g,a)

(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)

The root node satisfies the determinacy criterion.

(2) YES