(0) Obligation:

Clauses:

p(X, X, a) :- !.
p(X, Y, Z) :- ','(eq(Z, a), ','(eq(X, Y), p(X, Y, Z))).
eq(X, X).

Query: p(a,a,a)

(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)

The root node satisfies the determinacy criterion.

(2) YES