(0) Obligation:
Clauses:
f(0, 1, X) :- f(X, X, X).
Queries:
f(a,a,g).
(1) PrologToPrologProblemTransformerProof (SOUND transformation)
Built Prolog problem from termination graph.
(2) Obligation:
Clauses:
(3) PPisEmptyProof (EQUIVALENT transformation)
The Prolog program is empty. Hence, it trivially terminates.
(4) YES