(0) Obligation:

Clauses:

even(0).
even(s(X)) :- odd(X).
odd(s(X)) :- even(X).

Query: even(g)

(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)

The root node satisfies the determinacy criterion.

(2) YES