Consider the TRS R consisting of the rewrite rule

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

There are 2 dependency pairs:

2: x *# (y + z) -> x *# y
3: x *# (y + z) -> x *# z

The approximated dependency graph contains one SCC:
{2,3}.

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

Hence the TRS is terminating.