[1] 0+x0 -> x0

[2] 1 *x0 -> x0

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

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

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

[6] 0 *0 -> 0

Completion succeeded.
{ [-1] 0+x0 = x0 (trace = Original(1,))
  [-2] 1 *x0 = x0 (trace = Original(2,))
  [-3] (x+y) *x0 = (x0 *x)+(x0 *y) (trace = Original(3,))
  [-7] x0 *x = (0 *x)+(x0 *x) (trace = Superposition of [1] 0+x0 -> x0 over 
                                                         [3] (x+y) *x0 ->
                                                          (x0 *x)+(x0 *y) at 0))
  [-16] (0 *x5)+x5 = 1 *x5 (trace = Superposition of [2] 1 *x0 -> x0 over 
                                                      [4] (0 *x)+(x0 *x) ->
                                                       x0 *x at 1))
  [-17] (0 *x0)+x0 = x0 (trace = Rewriting [-16] (0 *x5)+x5 = 1 *x5 by 
                                 ([2] 1 *x0 -> x0 at R./\))
  [-18] 0 *0 = 0 (trace = Superposition of [1] 0+x0 -> x0 over 
                                            [5] (0 *x0)+x0 -> x0 at /\))
   }
(7 equations)
{ [1] 0+x0 -> x0 (trace = Oriented([-1] 0+x0 = x0))
  [2] 1 *x0 -> x0 (trace = Oriented([-2] 1 *x0 = x0))
  [3] (x+y) *x0 -> (x0 *x)+(x0 *y) (trace = Oriented([-3] (x+y) *x0 = 
                                                          (x0 *x)+(x0 *y)))
  [4] (0 *x)+(x0 *x) -> x0 *x (trace = Reverted([-7] x0 *x = (0 *x)+(x0 *x)))
  [5] (0 *x0)+x0 -> x0 (trace = Oriented([-17] (0 *x0)+x0 = x0))
  [6] 0 *0 -> 0 (trace = Oriented([-18] 0 *0 = 0))
   }
(6 rules)

real	0m0.085s
user	0m0.080s
sys	0m0.004s