Consider the TRS R consisting of the rewrite rules

1: f(g(i(a,b,b'),c),d) -> if(e,f(b . c,d'),f(b' . c,d'))
2: f(g(h(a,b),c),d) -> if(e,f(b . g(h(a,b),c),d),f(c,d'))

There are 4 dependency pairs:

3: F(g(i(a,b,b'),c),d) -> F(b . c,d')
4: F(g(i(a,b,b'),c),d) -> F(b' . c,d')
5: F(g(h(a,b),c),d) -> F(b . g(h(a,b),c),d)
6: F(g(h(a,b),c),d) -> F(c,d')

The approximated dependency graph contains no SCCs
and hence the TRS is trivially terminating.