YES

The TRS could be proven terminating. The proof took 40 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (1ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

f#(a, b, X)f#(X, X, X)

Rewrite Rules

f(a, b, X)f(X, X, X)ca
cb

Original Signature

Termination of terms over the following signature is verified: f, b, c, a

Strategy

Context-sensitive strategy:
μ(T) = μ(b) = μ(c) = μ(a) = μ(c#) = ∅
μ(f) = μ(f#) = {3}


There are no SCCs!