Problem:
 *(e(),x) -> x
 *(-(x),x) -> e()
 *(*(x,y),z) -> *(x,*(y,z))
 *(-(x),*(x,y)) -> y
 *(x,e()) -> x
 -(e()) -> e()
 -(-(x)) -> x
 *(x,-(x)) -> e()
 *(x,*(-(x),y)) -> y
 -(*(x,y)) -> *(-(y),-(x))

Proof:
 Church Rosser Transformation Processor (kb):
  *(e(),x) -> x
  *(-(x),x) -> e()
  *(*(x,y),z) -> *(x,*(y,z))
  *(-(x),*(x,y)) -> y
  *(x,e()) -> x
  -(e()) -> e()
  -(-(x)) -> x
  *(x,-(x)) -> e()
  *(x,*(-(x),y)) -> y
  -(*(x,y)) -> *(-(y),-(x))
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [-](x0) = 4x0 + 1,
    
    [*](x0, x1) = x0 + x1 + 3,
    
    [e] = 4
   orientation:
    *(e(),x) = x + 7 >= x = x
    
    *(-(x),x) = 5x + 4 >= 4 = e()
    
    *(*(x,y),z) = x + y + z + 6 >= x + y + z + 6 = *(x,*(y,z))
    
    *(-(x),*(x,y)) = 5x + y + 7 >= y = y
    
    *(x,e()) = x + 7 >= x = x
    
    -(e()) = 17 >= 4 = e()
    
    -(-(x)) = 16x + 5 >= x = x
    
    *(x,-(x)) = 5x + 4 >= 4 = e()
    
    *(x,*(-(x),y)) = 5x + y + 7 >= y = y
    
    -(*(x,y)) = 4x + 4y + 13 >= 4x + 4y + 5 = *(-(y),-(x))
   problem:
    *(-(x),x) -> e()
    *(*(x,y),z) -> *(x,*(y,z))
    *(x,-(x)) -> e()
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [-](x0) = 2x0 + 2,
     
     [*](x0, x1) = 2x0 + x1 + 5,
     
     [e] = 0
    orientation:
     *(-(x),x) = 5x + 9 >= 0 = e()
     
     *(*(x,y),z) = 4x + 2y + z + 15 >= 2x + 2y + z + 10 = *(x,*(y,z))
     
     *(x,-(x)) = 4x + 7 >= 0 = e()
    problem:
     
    Qed