[1] f(1) -> 1

[2] 1 *x0 -> x0

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

[4] i(1) -> 1

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

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

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

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

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

[10] f(i(x0)) *f(x0) -> 1

[11] i(f(i(x0))) -> f(x0)

[12] f(i(x0)) -> i(f(x0))

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

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

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

Completion succeeded.
{ [-1] 1 *x0 = x0 (trace = Original(1,))
  [-2] i(x0) *x0 = 1 (trace = Original(2,))
  [-3] f(1) = 1 (trace = Original(3,))
  [-4] f(x0 *x) = f(x0) *f(x) (trace = Original(4,))
  [-7] i(1) = 1 (trace = Superposition of [2] 1 *x0 -> x0 over 
                                           [3] i(x0) *x0 -> 1 at /\))
  [-26] 1 *i(x6) = 1 *i(x6 *x8) *x8 (trace = Superposition of [-3] i(x0) *x0 *x ->
                                                               1 *x over 
                                                               [-3] i(x0)
                                                                     *
                                                                    x0
                                                                     *
                                                                    x ->
                                                                1 *x at /\))
  [-27] i(x0) = i(x0 *x) *x (trace = Rewriting [-26] 1 *i(x6) = 1 *i(x6 *x8)
                                                                  *x8 by 
                                     ([2] 1 *x0 -> x0 at L./\).([2] 1 *x0 -> x0 at 
                                                               R./\))
  [-61] 1 *x7 = 1 *i(i(x7)) (trace = Superposition of [-3] i(x0) *x0 *x -> 1 *x over 
                                                       [-3] i(x0) *x0 *x ->
                                                        1 *x at /\))
  [-62] x0 = i(i(x0)) (trace = Rewriting [-61] 1 *x7 = 1 *i(i(x7)) by 
                               ([2] 1 *x0 -> x0 at L./\).([2] 1 *x0 -> x0 at 
                                                         R./\))
  [-118] i(1 *x6 *x8) *i(x5) *x8 = i(x5 *x6) (trace = Superposition of 
                                                      [-3] i(x0) *x0 *x -> 1 *x over 
                                                       [8] i(x0 *x) *x -> i(x0) at 0.0))
  [-119] i(x0) *i(x) = i(x0 *x) (trace = Rewriting [-118] i(1 *x6 *x8)
                                                            *i(x5) *x8 = 
                                                          i(x5 *x6) by 
                                         ([2] 1 *x0 -> x0 at L.0.0).(
                                                                    [-8] 
                                                                    i(x0 *x)
                                                                     *
                                                                    x *
                                                                    y ->
                                                                     
                                                                    i(x0) *y at 
                                                                    L.
                                                                    /\))
  [-170] f(1) = f(i(x4)) *f(x4) (trace = Superposition of [3] i(x0) *x0 -> 1 over 
                                                           [9] f(x0 *x) ->
                                                            f(x0) *f(x) at 0))
  [-171] 1 = f(i(x0)) *f(x0) (trace = Rewriting [-170] f(1) = f(i(x4)) *f(x4) by 
                                      ([1] f(1) -> 1 at L./\))
  [-192] i(1) *f(i(x0)) = i(f(x0)) (trace = Superposition of [8] i(x0 *x) *x ->
                                                              i(x0) over 
                                                              [10] f(i(x0))
                                                                     *
                                                                    f(x0) ->
                                                               1 at 0.0))
  [-193] f(i(x0)) = i(f(x0)) (trace = Rewriting [-192] i(1) *f(i(x0)) = 
                                                       i(f(x0)) by ([4] 
                                                                    i(1) -> 
                                                                    1 at 
                                                                   L.0).
                                      ([2] 1 *x0 -> x0 at L./\))
   }
(15 equations)
{ [-8] i(x0 *x) *x *y -> i(x0) *y (trace = Extension of [8] i(x0 *x) *x ->
                                                         i(x0))
  [-3] i(x0) *x0 *x -> 1 *x (trace = Extension of [3] i(x0) *x0 -> 1)
  [1] f(1) -> 1 (trace = Oriented([-3] f(1) = 1))
  [2] 1 *x0 -> x0 (trace = Oriented([-1] 1 *x0 = x0))
  [3] i(x0) *x0 -> 1 (trace = Oriented([-2] i(x0) *x0 = 1))
  [4] i(1) -> 1 (trace = Oriented([-7] i(1) = 1))
  [8] i(x0 *x) *x -> i(x0) (trace = Reverted([-27] i(x0) = i(x0 *x) *x))
  [9] f(x0 *x) -> f(x0) *f(x) (trace = Oriented([-4] f(x0 *x) = f(x0) *f(x)))
  [10] f(i(x0)) *f(x0) -> 1 (trace = Reverted([-171] 1 = f(i(x0)) *f(x0)))
   }
(9 rules)

real	0m0.045s
user	0m0.036s
sys	0m0.008s