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