[1] 0+x0 -> x0

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

[3] i(0) -> 0

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

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

[10] m(x,x0+y) -> m(x,x0)+m(x,y)

[11] m(x,0)+m(x,x0) -> m(x,x0)

[12] m(x0,0) -> 0

[13] m(x,i(x0))+m(x,x0) -> 0

[14] i(m(x0,i(x))) -> m(x0,x)

[15] m(x0,i(x)) -> i(m(x0,x))

[16] m(x+y,x0) -> m(x,x0)+m(y,x0)

[17] m(0,x)+m(x0,x) -> m(x0,x)

[18] m(0,x0) -> 0

[19] m(i(x0),x)+m(x0,x) -> 0

[20] i(m(i(x),x0)) -> m(x,x0)

[21] m(i(x),x0) -> i(m(x,x0))

Completion succeeded.
{ [-1] 0+x0 = x0 (trace = Original(1,))
  [-2] i(x0)+x0 = 0 (trace = Original(2,))
  [-3] m(x+y,x0) = m(x,x0)+m(y,x0) (trace = Original(3,))
  [-4] m(x,x0+y) = m(x,x0)+m(x,y) (trace = Original(4,))
  [-6] i(0) = 0 (trace = Superposition of [1] 0+x0 -> x0 over 
                                           [2] i(x0)+x0 -> 0 at /\))
  [-25] 0+i(x6) = 0+i(x6+x8)+x8 (trace = Superposition of [-2] i(x0)+x0+x ->
                                                           0+x over 
                                                           [-2] i(x0)+x0+x ->
                                                            0+x at /\))
  [-26] i(x0) = i(x0+x)+x (trace = Rewriting [-25] 0+i(x6) = 0+i(x6+x8)+x8 by 
                                   ([1] 0+x0 -> x0 at L./\).([1] 0+x0 -> x0 at 
                                                            R./\))
  [-60] 0+x7 = 0+i(i(x7)) (trace = Superposition of [-2] i(x0)+x0+x -> 0+x over 
                                                     [-2] i(x0)+x0+x -> 0+x at /\))
  [-61] x0 = i(i(x0)) (trace = Rewriting [-60] 0+x7 = 0+i(i(x7)) by (
                                                                    [1] 
                                                                    0+x0 -> 
                                                                    x0 at 
                                                                    L./\).
                               ([1] 0+x0 -> x0 at R./\))
  [-117] i(0+x6+x8)+i(x5)+x8 = i(x5+x6) (trace = Superposition of [-2] 
                                                                  i(x0)
                                                                   +x0
                                                                   +x ->
                                                                   0+x over 
                                                                   [7] 
                                                                   i(x0+x)
                                                                    +
                                                                    x ->
                                                                    i(x0) at 0.0))
  [-118] i(x0)+i(x) = i(x0+x) (trace = Rewriting [-117] i(0+x6+x8)+i(x5)+x8 = 
                                                        i(x5+x6) by (
                                                                    [1] 
                                                                    0+x0 -> 
                                                                    x0 at 
                                                                    L.0.0).
                                       ([-7] i(x0+x)+x+y -> i(x0)+y at 
                                       L./\))
  [-203] m(x,x0) = m(x,0)+m(x,x0) (trace = Superposition of [1] 0+x0 -> x0 over 
                                                             [10] m(x,x0+y) ->
                                                              m(x,x0)+m(x,y) at 1))
  [-205] m(y,0) = m(y,i(x6))+m(y,x6) (trace = Superposition of [2] i(x0)+x0 ->
                                                                0 over 
                                                                [10] 
                                                                m(x,x0+y) ->
                                                                 m(x,x0)+m(x,y) at 1))
  [-221] 0+m(y,0) = m(y,x0)+i(m(y,x0)) (trace = Superposition of [-2] 
                                                                 i(x0)
                                                                  +x0
                                                                  +x ->
                                                                  0+x over 
                                                                  [-11] 
                                                                  m(x,0)
                                                                   +m(x,x0)
                                                                   +y ->
                                                                   m(x,x0)+y at /\))
  [-222] m(x0,0) = 0 (trace = Rewriting [-221] 0+m(y,0) = m(y,x0)+i(m(y,x0)) by 
                              ([1] 0+x0 -> x0 at L./\).([2] i(x0)+x0 -> 0 at 
                                                       R./\))
  [-230] 0 = m(x,i(x0))+m(x,x0) (trace = Rewriting [-205] m(y,0) = m(y,i(x6))
                                                                    +
                                                                    m(y,x6) by 
                                         ([12] m(x0,0) -> 0 at L./\))
  [-239] 0+m(y,i(x0)) = 0+i(m(y,x0)) (trace = Superposition of [-2] i(x0)+x0+x ->
                                                                0+x over 
                                                                [-13] 
                                                                m(x,i(x0))
                                                                 +m(x,x0)
                                                                 +y ->
                                                                 0+y at /\))
  [-240] m(x0,i(x)) = i(m(x0,x)) (trace = Rewriting [-239] 0+m(y,i(x0)) = 
                                                           0+i(m(y,x0)) by 
                                          ([1] 0+x0 -> x0 at L./\).([1] 
                                                                    0+x0 -> 
                                                                    x0 at 
                                                                   R./\))
  [-259] m(x0,x) = m(0,x)+m(x0,x) (trace = Superposition of [1] 0+x0 -> x0 over 
                                                             [16] m(x+y,x0) ->
                                                              m(x,x0)+m(y,x0) at 0))
  [-261] m(0,x0) = m(i(x6),x0)+m(x6,x0) (trace = Superposition of [2] 
                                                                  i(x0)+x0 -> 
                                                                  0 over 
                                                                   [16] 
                                                                   m(
                                                                    x+y,
                                                                    x0) ->
                                                                    m(x,x0)
                                                                    +m(y,x0) at 0))
  [-287] 0+m(0,y) = m(x0,y)+i(m(x0,y)) (trace = Superposition of [-2] 
                                                                 i(x0)
                                                                  +x0
                                                                  +x ->
                                                                  0+x over 
                                                                  [-17] 
                                                                  m(0,x)
                                                                   +m(x0,x)
                                                                   +y ->
                                                                   m(x0,x)+y at /\))
  [-288] m(0,x0) = 0 (trace = Rewriting [-287] 0+m(0,y) = m(x0,y)+i(m(x0,y)) by 
                              ([1] 0+x0 -> x0 at L./\).([2] i(x0)+x0 -> 0 at 
                                                       R./\))
  [-299] 0 = m(i(x0),x)+m(x0,x) (trace = Rewriting [-261] m(0,x0) = m(i(x6),x0)
                                                                    +m(x6,x0) by 
                                         ([18] m(0,x0) -> 0 at L./\))
  [-316] 0+m(i(x0),y) = 0+i(m(x0,y)) (trace = Superposition of [-2] i(x0)+x0+x ->
                                                                0+x over 
                                                                [-19] 
                                                                m(i(x0),x)
                                                                 +m(x0,x)
                                                                 +y ->
                                                                 0+y at /\))
  [-317] m(i(x),x0) = i(m(x,x0)) (trace = Rewriting [-316] 0+m(i(x0),y) = 
                                                           0+i(m(x0,y)) by 
                                          ([1] 0+x0 -> x0 at L./\).([1] 
                                                                    0+x0 -> 
                                                                    x0 at 
                                                                   R./\))
   }
(25 equations)
{ [-19] m(i(x0),x)+m(x0,x)+y -> 0+y (trace = Extension of [19] m(i(x0),x)
                                                                +m(x0,x) ->
                                                           0)
  [-17] m(0,x)+m(x0,x)+y -> m(x0,x)+y (trace = Extension of [17] m(0,x)+m(x0,x) ->
                                                             m(x0,x))
  [-13] m(x,i(x0))+m(x,x0)+y -> 0+y (trace = Extension of [13] m(x,i(x0))
                                                                +m(x,x0) ->
                                                           0)
  [-11] m(x,0)+m(x,x0)+y -> m(x,x0)+y (trace = Extension of [11] m(x,0)+m(x,x0) ->
                                                             m(x,x0))
  [-7] i(x0+x)+x+y -> i(x0)+y (trace = Extension of [7] i(x0+x)+x -> i(x0))
  [-2] i(x0)+x0+x -> 0+x (trace = Extension of [2] i(x0)+x0 -> 0)
  [1] 0+x0 -> x0 (trace = Oriented([-1] 0+x0 = x0))
  [2] i(x0)+x0 -> 0 (trace = Oriented([-2] i(x0)+x0 = 0))
  [7] i(x0+x)+x -> i(x0) (trace = Reverted([-26] i(x0) = i(x0+x)+x))
  [10] m(x,x0+y) -> m(x,x0)+m(x,y) (trace = Oriented([-4] m(x,x0+y) = 
                                                          m(x,x0)+m(x,y)))
  [11] m(x,0)+m(x,x0) -> m(x,x0) (trace = Reverted([-203] m(x,x0) = m(x,0)
                                                                    +m(x,x0)))
  [12] m(x0,0) -> 0 (trace = Oriented([-222] m(x0,0) = 0))
  [13] m(x,i(x0))+m(x,x0) -> 0 (trace = Reverted([-230] 0 = m(x,i(x0))+m(x,x0)))
  [16] m(x+y,x0) -> m(x,x0)+m(y,x0) (trace = Oriented([-3] m(x+y,x0) = 
                                                           m(x,x0)+m(y,x0)))
  [17] m(0,x)+m(x0,x) -> m(x0,x) (trace = Reverted([-259] m(x0,x) = m(0,x)
                                                                    +m(x0,x)))
  [18] m(0,x0) -> 0 (trace = Oriented([-288] m(0,x0) = 0))
  [19] m(i(x0),x)+m(x0,x) -> 0 (trace = Reverted([-299] 0 = m(i(x0),x)+m(x0,x)))
   }
(17 rules)

real	0m0.065s
user	0m0.048s
sys	0m0.020s