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