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

Proof:
 AT confluence processor
  Complete TRS T' of input TRS:
  -(+(x,y)) -> +(-(x),-(y))
  +(x,y) -> +(y,x)
  
   T' = (P union S) with
  
   TRS P:+(x,y) -> +(y,x)
  
   TRS S:-(+(x,y)) -> +(-(x),-(y))
  
  S is left-linear and P is reversible.
  
   CP(S,S) = 
  
   CP(S,P union P^-1) = 
  
  
   PCP_in(P union P^-1,S) = 
  -(+(y,x)) = +(-(x),-(y))
  
  
  We have to check termination of S:
  
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [-](x0) = 6x0 + 1,
    
    [+](x0, x1) = 5x0 + 5x1 + 2
   orientation:
    -(+(x,y)) = 30x + 30y + 13 >= 30x + 30y + 12 = +(-(x),-(y))
   problem:
    
   Qed