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