Consider the TRS R consisting of the rewrite rules 1: d(x) -> e(u(x)) 2: d(u(x)) -> c(x) 3: c(u(x)) -> b(x) 4: v(e(x)) -> x 5: b(u(x)) -> a(e(x)) There are 2 dependency pairs: 6: D(u(x)) -> C(x) 7: C(u(x)) -> B(x) The approximated dependency graph contains no SCCs and hence the TRS is trivially terminating.