[1] 1 *x0 -> x0

[2] i(x0) *x0 -> 1

[3] i(1) -> 1

[4] i(i(x0)) -> x0

[5] i(i(x0 *x) *x) -> x0

[6] i(i(x0) *x) *x -> x0

[7] i(x0 *x) *x -> i(x0)

[8] i(i(x0) *i(x)) -> x0 *x

[9] i(i(x) *x0) -> i(x0) *x

[10] i(x0 *x) -> i(x0) *i(x)

Completion succeeded.
{ [-1] 1 *x0 = x0 (trace = Original(1,))
  [-2] i(x0) *x0 = 1 (trace = Original(2,))
  [-4] i(1) = 1 (trace = Superposition of [1] 1 *x0 -> x0 over 
                                           [2] i(x0) *x0 -> 1 at /\))
  [-23] 1 *i(x6) = 1 *i(x6 *x8) *x8 (trace = Superposition of [-2] i(x0) *x0 *x ->
                                                               1 *x over 
                                                               [-2] i(x0)
                                                                     *
                                                                    x0
                                                                     *
                                                                    x ->
                                                                1 *x at /\))
  [-24] i(x0) = i(x0 *x) *x (trace = Rewriting [-23] 1 *i(x6) = 1 *i(x6 *x8)
                                                                  *x8 by 
                                     ([1] 1 *x0 -> x0 at L./\).([1] 1 *x0 -> x0 at 
                                                               R./\))
  [-58] 1 *x7 = 1 *i(i(x7)) (trace = Superposition of [-2] i(x0) *x0 *x -> 1 *x over 
                                                       [-2] i(x0) *x0 *x ->
                                                        1 *x at /\))
  [-59] x0 = i(i(x0)) (trace = Rewriting [-58] 1 *x7 = 1 *i(i(x7)) by 
                               ([1] 1 *x0 -> x0 at L./\).([1] 1 *x0 -> x0 at 
                                                         R./\))
  [-115] i(1 *x6 *x8) *i(x5) *x8 = i(x5 *x6) (trace = Superposition of 
                                                      [-2] i(x0) *x0 *x -> 1 *x over 
                                                       [7] i(x0 *x) *x -> i(x0) at 0.0))
  [-116] i(x0) *i(x) = i(x0 *x) (trace = Rewriting [-115] i(1 *x6 *x8)
                                                            *i(x5) *x8 = 
                                                          i(x5 *x6) by 
                                         ([1] 1 *x0 -> x0 at L.0.0).(
                                                                    [-7] 
                                                                    i(x0 *x)
                                                                     *
                                                                    x *
                                                                    y ->
                                                                     
                                                                    i(x0) *y at 
                                                                    L.
                                                                    /\))
   }
(9 equations)
{ [-7] i(x0 *x) *x *y -> i(x0) *y (trace = Extension of [7] i(x0 *x) *x ->
                                                         i(x0))
  [-2] i(x0) *x0 *x -> 1 *x (trace = Extension of [2] i(x0) *x0 -> 1)
  [1] 1 *x0 -> x0 (trace = Oriented([-1] 1 *x0 = x0))
  [2] i(x0) *x0 -> 1 (trace = Oriented([-2] i(x0) *x0 = 1))
  [7] i(x0 *x) *x -> i(x0) (trace = Reverted([-24] i(x0) = i(x0 *x) *x))
   }
(5 rules)

real	0m0.047s
user	0m0.048s
sys	0m0.004s