(0) Obligation:
Clauses:
even(X) :- ','(eq(Y, f(e, f(o, Y))), c(Y, X)).
c(f(e, X1), 0).
c(f(X2, X), s(Y)) :- c(X, Y).
eq(X, X).
Query: even(g)
(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)
The root node satisfies the determinacy criterion.
(2) YES