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