(0) Obligation:

Clauses:

q :- p(s(s(0))).
p(s(X)) :- p(X).
p(0).
p(s(s(s(0)))) :- p(s(s(s(0)))).

Query: q()

(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)

The root node satisfies the determinacy criterion.

(2) YES