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) = 2x0 + 1,
    
    [*](x0, x1) = x0 + x1 + 1,
    
    [e] = 2
   orientation:
    *(e(),x) = x + 3 >= x = x
    
    *(-(x),x) = 3x + 2 >= 2 = e()
    
    *(*(x,y),z) = x + y + z + 2 >= x + y + z + 2 = *(x,*(y,z))
    
    *(-(x),*(x,y)) = 3x + y + 3 >= y = y
    
    *(x,e()) = x + 3 >= x = x
    
    -(e()) = 5 >= 2 = e()
    
    -(-(x)) = 4x + 3 >= x = x
    
    *(x,-(x)) = 3x + 2 >= 2 = e()
    
    *(x,*(-(x),y)) = 3x + y + 3 >= y = y
    
    -(*(x,y)) = 2x + 2y + 3 >= 2x + 2y + 3 = *(-(y),-(x))
   problem:
    *(-(x),x) -> e()
    *(*(x,y),z) -> *(x,*(y,z))
    *(x,-(x)) -> e()
    -(*(x,y)) -> *(-(y),-(x))
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [-](x0) = x0,
     
     [*](x0, x1) = x0 + x1 + 4,
     
     [e] = 0
    orientation:
     *(-(x),x) = 2x + 4 >= 0 = e()
     
     *(*(x,y),z) = x + y + z + 8 >= x + y + z + 8 = *(x,*(y,z))
     
     *(x,-(x)) = 2x + 4 >= 0 = e()
     
     -(*(x,y)) = x + y + 4 >= x + y + 4 = *(-(y),-(x))
    problem:
     *(*(x,y),z) -> *(x,*(y,z))
     -(*(x,y)) -> *(-(y),-(x))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [-](x0) = 2x0 + 3,
      
      [*](x0, x1) = x0 + x1 + 6
     orientation:
      *(*(x,y),z) = x + y + z + 12 >= x + y + z + 12 = *(x,*(y,z))
      
      -(*(x,y)) = 2x + 2y + 15 >= 2x + 2y + 12 = *(-(y),-(x))
     problem:
      *(*(x,y),z) -> *(x,*(y,z))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [*](x0, x1) = 2x0 + x1 + 1
      orientation:
       *(*(x,y),z) = 4x + 2y + z + 3 >= 2x + 2y + z + 2 = *(x,*(y,z))
      problem:
       
      Qed