Consider the TRS R consisting of the rewrite rule 1: f(g(h(x,y)),f(a,a)) -> f(h(x,x),g(f(y,a))) There are 2 dependency pairs: 2: F(g(h(x,y)),f(a,a)) -> F(h(x,x),g(f(y,a))) 3: F(g(h(x,y)),f(a,a)) -> F(y,a) The approximated dependency graph contains no SCCs and hence the TRS is trivially terminating.