Problem:
 -(+(x,-(x))) -> 0()
 +(x,-(x)) -> 0()
 -(+(0(),0())) -> 0()
 +(0(),0()) -> 0()
 -(0()) -> 0()

Proof:
 Church Rosser Transformation Processor (kb):
  -(+(x,-(x))) -> 0()
  +(x,-(x)) -> 0()
  -(+(0(),0())) -> 0()
  +(0(),0()) -> 0()
  -(0()) -> 0()
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [+](x0, x1) = 7x0 + 5x1,
    
    [-](x0) = x0 + 2,
    
    [0] = 1
   orientation:
    -(+(x,-(x))) = 12x + 12 >= 1 = 0()
    
    +(x,-(x)) = 12x + 10 >= 1 = 0()
    
    -(+(0(),0())) = 14 >= 1 = 0()
    
    +(0(),0()) = 12 >= 1 = 0()
    
    -(0()) = 3 >= 1 = 0()
   problem:
    
   Qed