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