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