[1] 0+x0 -> x0

[2] 1 *x0 -> x0

[3] i(x0)+x0 -> 0

[4] i(0) -> 0

[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] i(i(x0)+i(x)) -> x0+x

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

[11] i(x0+x) -> i(x0)+i(x)

[12] (x+y) *x0 -> (x0 *x)+(x0 *y)

[13] (0 *x)+(x0 *x) -> x0 *x

[14] (0 *x0)+x0 -> x0

[15] 0 *0 -> 0

[16] 0 *x0 -> 0

[17] (i(x0) *x)+(x0 *x) -> 0

[18] (i(1) *x0)+x0 -> 0

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

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

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

Completion succeeded.
{ [-1] 0+x0 = x0 (trace = Original(1,))
  [-2] i(x0)+x0 = 0 (trace = Original(2,))
  [-3] 1 *x0 = x0 (trace = Original(3,))
  [-4] (x+y) *x0 = (x0 *x)+(x0 *y) (trace = Original(4,))
  [-7] i(0) = 0 (trace = Superposition of [1] 0+x0 -> x0 over 
                                           [3] i(x0)+x0 -> 0 at /\))
  [-26] 0+i(x6) = 0+i(x6+x8)+x8 (trace = Superposition of [-3] i(x0)+x0+x ->
                                                           0+x over 
                                                           [-3] i(x0)+x0+x ->
                                                            0+x at /\))
  [-27] i(x0) = i(x0+x)+x (trace = Rewriting [-26] 0+i(x6) = 0+i(x6+x8)+x8 by 
                                   ([1] 0+x0 -> x0 at L./\).([1] 0+x0 -> x0 at 
                                                            R./\))
  [-61] 0+x7 = 0+i(i(x7)) (trace = Superposition of [-3] i(x0)+x0+x -> 0+x over 
                                                     [-3] i(x0)+x0+x -> 0+x at /\))
  [-62] x0 = i(i(x0)) (trace = Rewriting [-61] 0+x7 = 0+i(i(x7)) by (
                                                                    [1] 
                                                                    0+x0 -> 
                                                                    x0 at 
                                                                    L./\).
                               ([1] 0+x0 -> x0 at R./\))
  [-118] i(0+x6+x8)+i(x5)+x8 = i(x5+x6) (trace = Superposition of [-3] 
                                                                  i(x0)
                                                                   +x0
                                                                   +x ->
                                                                   0+x over 
                                                                   [8] 
                                                                   i(x0+x)
                                                                    +
                                                                    x ->
                                                                    i(x0) at 0.0))
  [-119] i(x0)+i(x) = i(x0+x) (trace = Rewriting [-118] i(0+x6+x8)+i(x5)+x8 = 
                                                        i(x5+x6) by (
                                                                    [1] 
                                                                    0+x0 -> 
                                                                    x0 at 
                                                                    L.0.0).
                                       ([-8] i(x0+x)+x+y -> i(x0)+y at 
                                       L./\))
  [-218] x0 *x = (0 *x)+(x0 *x) (trace = Superposition of [1] 0+x0 -> x0 over 
                                                           [12] (x+y) *x0 ->
                                                            (x0 *x)+(x0 *y) at 0))
  [-225] 0 *x0 = (i(x6) *x0)+(x0 *x6) (trace = Superposition of [3] i(x0)+x0 ->
                                                                 0 over 
                                                                 [12] 
                                                                 (x+y) *x0 ->
                                                                  (x0 *x)
                                                                   +(x0 *y) at 0))
  [-257] (0 *x5)+x5 = 1 *x5 (trace = Superposition of [2] 1 *x0 -> x0 over 
                                                       [13] (0 *x)+(x0 *x) ->
                                                        x0 *x at 1))
  [-258] (0 *x0)+x0 = x0 (trace = Rewriting [-257] (0 *x5)+x5 = 1 *x5 by 
                                  ([2] 1 *x0 -> x0 at R./\))
  [-273] 0+(0 *x7) = i(x7)+x7 (trace = Superposition of [-3] i(x0)+x0+x -> 0+x over 
                                                         [-14] (0 *x0)+x0+x ->
                                                          x0+x at /\))
  [-274] 0 *x0 = 0 (trace = Rewriting [-273] 0+(0 *x7) = i(x7)+x7 by 
                            ([1] 0+x0 -> x0 at L./\).([3] i(x0)+x0 -> 0 at 
                                                     R./\))
  [-304] 0 = (i(x0) *x)+(x0 *x) (trace = Rewriting [-225] 0 *x0 = (i(x6) *x0)
                                                                   +(x0 *x6) by 
                                         ([16] 0 *x0 -> 0 at L./\))
  [-307] (i(1) *x0)+x0 = 0 (trace = Superposition of [2] 1 *x0 -> x0 over 
                                                      [17] (i(x0) *x)+(x0 *x) ->
                                                       0 at 1))
  [-331] 0+(i(1) *x7) = 0+i(x7) (trace = Superposition of [-3] i(x0)+x0+x ->
                                                           0+x over 
                                                           [-18] (i(1) *x0)
                                                                  +x0
                                                                  +x ->
                                                            0+x at /\))
  [-332] i(1) *x0 = i(x0) (trace = Rewriting [-331] 0+(i(1) *x7) = 0+i(x7) by 
                                   ([1] 0+x0 -> x0 at L./\).([1] 0+x0 -> x0 at 
                                                            R./\))
  [-356] i(x0 *x) = i(x) *x0 (trace = Superposition of [20] i(1) *x0 -> i(x0) over 
                                                        [-20] i(1) *x0 *x ->
                                                         i(x0) *x at /\))
   }
(22 equations)
{ [-20] i(1) *x0 *x -> i(x0) *x (trace = Extension of [20] i(1) *x0 -> i(x0))
  [-18] (i(1) *x0)+x0+x -> 0+x (trace = Extension of [18] (i(1) *x0)+x0 -> 0)
  [-14] (0 *x0)+x0+x -> x0+x (trace = Extension of [14] (0 *x0)+x0 -> x0)
  [-8] i(x0+x)+x+y -> i(x0)+y (trace = Extension of [8] i(x0+x)+x -> i(x0))
  [-3] i(x0)+x0+x -> 0+x (trace = Extension of [3] i(x0)+x0 -> 0)
  [1] 0+x0 -> x0 (trace = Oriented([-1] 0+x0 = x0))
  [2] 1 *x0 -> x0 (trace = Oriented([-3] 1 *x0 = x0))
  [3] i(x0)+x0 -> 0 (trace = Oriented([-2] i(x0)+x0 = 0))
  [8] i(x0+x)+x -> i(x0) (trace = Reverted([-27] i(x0) = i(x0+x)+x))
  [12] (x+y) *x0 -> (x0 *x)+(x0 *y) (trace = Oriented([-4] (x+y) *x0 = 
                                                           (x0 *x)+(x0 *y)))
  [13] (0 *x)+(x0 *x) -> x0 *x (trace = Reverted([-218] x0 *x = (0 *x)+(x0 *x)))
  [14] (0 *x0)+x0 -> x0 (trace = Oriented([-258] (0 *x0)+x0 = x0))
  [16] 0 *x0 -> 0 (trace = Oriented([-274] 0 *x0 = 0))
  [17] (i(x0) *x)+(x0 *x) -> 0 (trace = Reverted([-304] 0 = (i(x0) *x)+(x0 *x)))
  [18] (i(1) *x0)+x0 -> 0 (trace = Oriented([-307] (i(1) *x0)+x0 = 0))
  [20] i(1) *x0 -> i(x0) (trace = Oriented([-332] i(1) *x0 = i(x0)))
  [21] i(x) *x0 -> i(x0 *x) (trace = Reverted([-356] i(x0 *x) = i(x) *x0))
   }
(17 rules)

real	0m0.117s
user	0m0.108s
sys	0m0.012s