(0) Obligation:

Clauses:

num(0) :- !.
num(X) :- ','(p(X, Y), num(Y)).
p(0, 0).
p(s(X), X).

Query: num(g)

(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)

The root node satisfies the determinacy criterion.

(2) YES