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

Proof:
 AT confluence processor
  Complete TRS T' of input TRS:
  -(+(x,y)) -> +(-(x),-(y))
  +(-(x),-(y)) -> -(+(x,y))
  
   T' = (P union S) with
  
   TRS P:-(+(x,y)) -> +(-(x),-(y))
         +(-(x),-(y)) -> -(+(x,y))
  
   TRS S:
  
  S is left-linear and P is reversible.
  
   CP(S,S) = 
  
   CP(S,P union P^-1) = 
  
  
   PCP_in(P union P^-1,S) = 
  
  
  We have to check termination of S:
  
  Qed