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