Consider the TRS R consisting of the rewrite rules

1: x + 0 -> x
2: x + i(x) -> 0
3: (x + y) + z -> x + (y + z)
4: x * (y + z) -> (x * y) + (x * z)
5: (x + y) * z -> (x * z) + (y * z)

There are 8 dependency pairs:

6: (x + y) +# z -> x +# (y + z)
7: (x + y) +# z -> y +# z
8: x *# (y + z) -> (x * y) +# (x * z)
9: x *# (y + z) -> x *# y
10: x *# (y + z) -> x *# z
11: (x + y) *# z -> (x * z) +# (y * z)
12: (x + y) *# z -> x *# z
13: (x + y) *# z -> y *# z

The approximated dependency graph contains 2 SCCs:
{6,7}
and {9,10,12,13}.

- Consider the SCC {6,7}.
The usable rules are {1-3}.
By taking the polynomial interpretation
[0] = 1,
[i](x) = x + 1
and [+](x,y) = [+#](x,y) = x + y + 1,
the rules in {3,6}
are weakly decreasing and
the rules in {1,2,7}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {6}.
By taking the polynomial interpretation
[0] = 1,
[+#](x,y) = [i](x) = x + 1
and [+](x,y) = x + y + 1,
rule 3
is weakly decreasing and
the rules in {1,2,6}
are strictly decreasing.


- Consider the SCC {9,10,12,13}.
There are no usable rules.
By taking the polynomial interpretation
[*#](x,y) = [+](x,y) = x + y + 1,
the rules in {9,10,12,13}
are strictly decreasing.

Hence the TRS is terminating.