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