(0) Obligation:

Clauses:

t :- ','(eq(X, f(X)), !).
t :- t.
eq(X, X).

Query: t()

(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)

The root node satisfies the determinacy criterion.

(2) YES