(0) Obligation:

Clauses:

p :- ','(q, !).
p :- p.
q :- ','(!, failure(a)).
q.
failure(b).

Query: p()

(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)

The root node satisfies the determinacy criterion.

(2) YES