Consider the TRS R consisting of the rewrite rules 1: f(f(x)) -> g(f(x)) 2: g(g(x)) -> f(x) There are 2 dependency pairs: 3: F(f(x)) -> G(f(x)) 4: G(g(x)) -> F(x) Consider the SCC {3,4}. By taking the polynomial interpretation [f](x) = [F](x) = [g](x) = [G](x) = x + 1, the rules in {1,3} are weakly decreasing and the rules in {2,4} are strictly decreasing. Hence the TRS is terminating.