Consider the TRS R consisting of the rewrite rules

1: 1 . x -> x
2: x . 1 -> x
3: i(x) . x -> 1
4: x . i(x) -> 1
5: i(1) -> 1
6: i(i(x)) -> x
7: i(y) . (y . z) -> z
8: y . (i(y) . z) -> z
9: (x . y) . z -> x . (y . z)
10: i(x . y) -> i(y) . i(x)

There are 5 dependency pairs:

11: (x . y) .# z -> x .# (y . z)
12: (x . y) .# z -> y .# z
13: I(x . y) -> i(y) .# i(x)
14: I(x . y) -> I(y)
15: I(x . y) -> I(x)

The approximated dependency graph contains 2 SCCs:
{11,12}
and {14,15}.

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

- Consider the SCC {11}.
By taking the polynomial interpretation
[1] = 1,
[.#](x,y) = [i](x) = x + 1
and [.](x,y) = x + y + 1,
rule 9
is weakly decreasing and
the rules in {1-4,7,8,11}
are strictly decreasing.


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

Hence the TRS is terminating.