YES(?,O(n^2))

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

Proof:
 RT Transformation Processor:
  strict:
   +(-(x,y),z) -> -(+(x,z),y)
   -(+(x,y),y) -> x
  weak:
   
  Bounds Processor:
   bound: 0
   enrichment: match-rt
   automaton:
    final states: {3}
    transitions:
     +0(3,3) -> 3*
     -0(3,3) -> 3*
   problem:
    strict:
     +(-(x,y),z) -> -(+(x,z),y)
    weak:
     -(+(x,y),y) -> x
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
                   [1 1]     [1 0]     [4]
     [+](x0, x1) = [0 1]x0 + [0 0]x1 + [4],
     
                   [1 1]     [1 8]     [2]
     [-](x0, x1) = [0 1]x0 + [0 0]x1 + [9]
    orientation:
                   [1 2]    [1 8]    [1 0]    [15]    [1 2]    [1 8]    [1 0]    [10]              
     +(-(x,y),z) = [0 1]x + [0 0]y + [0 0]z + [13] >= [0 1]x + [0 0]y + [0 0]z + [13] = -(+(x,z),y)
     
                   [1 2]    [2 8]    [10]         
     -(+(x,y),y) = [0 1]x + [0 0]y + [13] >= x = x
    problem:
     strict:
      
     weak:
      +(-(x,y),z) -> -(+(x,z),y)
      -(+(x,y),y) -> x
    Qed