(0) Obligation:

Clauses:

p(b).
p(a) :- p1(X).
p1(b) :- !.
p1(a) :- p1(X).

Query: p(g)

(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)

The root node satisfies the determinacy criterion.

(2) YES