Consider the TRS R consisting of the rewrite rules

1: minus(minus(x)) -> x
2: minus(h(x)) -> h(minus(x))
3: minus(f(x,y)) -> f(minus(y),minus(x))

There are 3 dependency pairs:

4: MINUS(h(x)) -> MINUS(x)
5: MINUS(f(x,y)) -> MINUS(y)
6: MINUS(f(x,y)) -> MINUS(x)

The approximated dependency graph contains one SCC:
{4-6}.

- Consider the SCC {4-6}.
There are no usable rules.
By taking the polynomial interpretation
[h](x) = [MINUS](x) = x + 1
and [f](x,y) = x + y + 1,
the rules in {4-6}
are strictly decreasing.

Hence the TRS is terminating.