(0) Obligation:

Clauses:

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

Query: f(a)

(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)

The root node satisfies the determinacy criterion.

(2) YES