YES
The TRS could be proven terminating. The proof took 40 ms.
Problem 1 was processed with processor DependencyGraph (1ms).
f#(a, b, X) | → | f#(X, X, X) |
f(a, b, X) | → | f(X, X, X) | c | → | a | |
c | → | b |
Termination of terms over the following signature is verified: f, b, c, a
Context-sensitive strategy:
μ(T) = μ(b) = μ(c) = μ(a) = μ(c#) = ∅
μ(f) = μ(f#) = {3}