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