Consider the TRS R consisting of the rewrite rule 1: g(x,a,b) -> g(b,b,a) There is one dependency pair: 2: G(x,a,b) -> G(b,b,a) The approximated dependency graph contains no SCCs and hence the TRS is trivially terminating.