(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