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