Consider the TRS R consisting of the rewrite rules 1: f(x,y) -> x 2: g(a) -> h(a,b,a) 3: i(x) -> f(x,x) 4: h(x,x,y) -> g(x) There are 3 dependency pairs: 5: G(a) -> H(a,b,a) 6: I(x) -> F(x,x) 7: H(x,x,y) -> G(x) The approximated dependency graph contains no SCCs and hence the TRS is trivially terminating.