Consider the TRS R consisting of the rewrite rules

1: f(x,y,z) -> g(x <= y,x,y,z)
2: g(true,x,y,z) -> z
3: g(false,x,y,z) -> f(f(p(x),y,z),f(p(y),z,x),f(p(z),x,y))
4: p(0) -> 0
5: p(s(x)) -> x

There are 8 dependency pairs:

6: F(x,y,z) -> G(x <= y,x,y,z)
7: G(false,x,y,z) -> F(f(p(x),y,z),f(p(y),z,x),f(p(z),x,y))
8: G(false,x,y,z) -> F(p(x),y,z)
9: G(false,x,y,z) -> P(x)
10: G(false,x,y,z) -> F(p(y),z,x)
11: G(false,x,y,z) -> P(y)
12: G(false,x,y,z) -> F(p(z),x,y)
13: G(false,x,y,z) -> P(z)

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