Consider the TRS R consisting of the rewrite rules

1: p(s(x)) -> x
2: s(p(x)) -> x
3: 0 + y -> y
4: s(x) + y -> s(x + y)
5: p(x) + y -> p(x + y)
6: minus(0) -> 0
7: minus(s(x)) -> p(minus(x))
8: minus(p(x)) -> s(minus(x))
9: 0 * y -> 0
10: s(x) * y -> (x * y) + y
11: p(x) * y -> (x * y) + minus(y)

There are 13 dependency pairs:

12: s(x) +# y -> S(x + y)
13: s(x) +# y -> x +# y
14: p(x) +# y -> P(x + y)
15: p(x) +# y -> x +# y
16: MINUS(s(x)) -> P(minus(x))
17: MINUS(s(x)) -> MINUS(x)
18: MINUS(p(x)) -> S(minus(x))
19: MINUS(p(x)) -> MINUS(x)
20: s(x) *# y -> (x * y) +# y
21: s(x) *# y -> x *# y
22: p(x) *# y -> (x * y) +# minus(y)
23: p(x) *# y -> x *# y
24: p(x) *# y -> MINUS(y)

The approximated dependency graph contains 3 SCCs:
{13,15},
{17,19}
and {21,23}.

- Consider the SCC {13,15}.
There are no usable rules.
By taking the polynomial interpretation
[p](x) = [s](x) = x + 1
and [+#](x,y) = x + y + 1,
the rules in {13,15}
are strictly decreasing.

- Consider the SCC {17,19}.
There are no usable rules.
By taking the polynomial interpretation
[MINUS](x) = [p](x) = [s](x) = x + 1,
the rules in {17,19}
are strictly decreasing.

- Consider the SCC {21,23}.
There are no usable rules.
By taking the polynomial interpretation
[p](x) = [s](x) = x + 1
and [*#](x,y) = x + y + 1,
the rules in {21,23}
are strictly decreasing.

Hence the TRS is terminating.