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