(0) Obligation:

Clauses:

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

Query: p(a,a,a)

(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)

The root node satisfies the determinacy criterion.

(2) YES