(0) Obligation:

Clauses:

q :- p(X, Y).
p(a, b) :- !.
p(a, a) :- p(a, a).

Query: q()

(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)

The root node satisfies the determinacy criterion.

(2) YES