Consider the TRS R consisting of the rewrite rules

1: (x - y) + z -> (x + z) - y
2: (x + y) - y -> x

There are 2 dependency pairs:

3: (x - y) +# z -> (x + z) -# y
4: (x - y) +# z -> x +# z

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

- Consider the SCC {4}.
There are no usable rules.
By taking the polynomial interpretation
[+#](x,y) = [-](x,y) = x + y + 1,
rule 4
is strictly decreasing.

Hence the TRS is terminating.