Consider the TRS R consisting of the rewrite rules 1: f(f(X)) -> f(g(f(g(f(X))))) 2: f(g(f(X))) -> f(g(X)) There are 3 dependency pairs: 3: F(f(X)) -> F(g(f(g(f(X))))) 4: F(f(X)) -> F(g(f(X))) 5: F(g(f(X))) -> F(g(X)) The approximated dependency graph contains one SCC: {5}. - Consider the SCC {5}. There are no usable rules. By taking the polynomial interpretation [f](x) = [F](x) = [g](x) = x + 1, rule 5 is strictly decreasing. Hence the TRS is terminating.