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