Consider the TRS R consisting of the rewrite rule

1: (neg(x) - neg(x)) - (neg(y) - neg(y)) -> (x - y) - (x - y)

There are 2 dependency pairs:

2: (neg(x) - neg(x)) -# (neg(y) - neg(y)) -> (x - y) -# (x - y)
3: (neg(x) - neg(x)) -# (neg(y) - neg(y)) -> x -# y

Consider the SCC {2,3}.
By taking the polynomial interpretation
[neg](x) = x + 1
and [-](x,y) = [-#](x,y) = x + y + 1,
the rules in {1-3}
are strictly decreasing.
Hence the TRS is terminating.