YES(?,O(n^2))

Problem:
 a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
 f(a(x),a(y)) -> a(f(x,y))
 f(b(x),b(y)) -> b(f(x,y))

Proof:
 RT Transformation Processor:
  strict:
   a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
   f(a(x),a(y)) -> a(f(x,y))
   f(b(x),b(y)) -> b(f(x,y))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [b](x0) = x0 + 1,
    
    [a](x0) = x0,
    
    [f](x0, x1) = x0 + x1 + 13
   orientation:
    a(a(f(x,y))) = x + y + 13 >= x + y + 17 = f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
    
    f(a(x),a(y)) = x + y + 13 >= x + y + 13 = a(f(x,y))
    
    f(b(x),b(y)) = x + y + 15 >= x + y + 14 = b(f(x,y))
   problem:
    strict:
     a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
     f(a(x),a(y)) -> a(f(x,y))
    weak:
     f(b(x),b(y)) -> b(f(x,y))
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [b](x0) = x0,
     
     [a](x0) = x0 + 1,
     
     [f](x0, x1) = x0 + x1 + 27
    orientation:
     a(a(f(x,y))) = x + y + 29 >= x + y + 33 = f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
     
     f(a(x),a(y)) = x + y + 29 >= x + y + 28 = a(f(x,y))
     
     f(b(x),b(y)) = x + y + 27 >= x + y + 27 = b(f(x,y))
    problem:
     strict:
      a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
     weak:
      f(a(x),a(y)) -> a(f(x,y))
      f(b(x),b(y)) -> b(f(x,y))
    Matrix Interpretation Processor:
     dimension: 2
     interpretation:
                [1 0]  
      [b](x0) = [0 0]x0,
      
                [1 4]     [0]
      [a](x0) = [0 1]x0 + [2],
      
                              [10]
      [f](x0, x1) = x0 + x1 + [0 ]
     orientation:
                     [1 8]    [1 8]    [18]    [1 4]    [1 4]    [10]                                       
      a(a(f(x,y))) = [0 1]x + [0 1]y + [4 ] >= [0 0]x + [0 0]y + [4 ] = f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
      
                     [1 4]    [1 4]    [10]    [1 4]    [1 4]    [10]            
      f(a(x),a(y)) = [0 1]x + [0 1]y + [4 ] >= [0 1]x + [0 1]y + [2 ] = a(f(x,y))
      
                     [1 0]    [1 0]    [10]    [1 0]    [1 0]    [10]            
      f(b(x),b(y)) = [0 0]x + [0 0]y + [0 ] >= [0 0]x + [0 0]y + [0 ] = b(f(x,y))
     problem:
      strict:
       
      weak:
       a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
       f(a(x),a(y)) -> a(f(x,y))
       f(b(x),b(y)) -> b(f(x,y))
     Qed