Consider the TRS R consisting of the rewrite rules

1: minus(minus(x)) -> x
2: minux(x + y) -> minus(y) + minus(x)
3: minus(x) + (x + y) -> y
4: (x + y) + minus(y) -> x

There are 3 dependency pairs:

5: MINUX(x + y) -> minus(y) +# minus(x)
6: MINUX(x + y) -> MINUS(y)
7: MINUX(x + y) -> MINUS(x)

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