YES(?,O(n^2))

Problem:
 s(a()) -> a()
 s(s(x)) -> x
 s(f(x,y)) -> f(s(y),s(x))
 s(g(x,y)) -> g(s(x),s(y))
 f(x,a()) -> x
 f(a(),y) -> y
 f(g(x,y),g(u,v)) -> g(f(x,u),f(y,v))
 g(a(),a()) -> a()

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
                 [1 1]     [1 8]     [12]
   [g](x0, x1) = [0 1]x0 + [0 1]x1 + [1 ],
   
                           [0]
   [f](x0, x1) = x0 + x1 + [1],
   
             [1 8]     [4]
   [s](x0) = [0 1]x0 + [0],
   
         [1]
   [a] = [0]
  orientation:
            [5]    [1]      
   s(a()) = [0] >= [0] = a()
   
             [1  16]    [8]         
   s(s(x)) = [0  1 ]x + [0] >= x = x
   
               [1 8]    [1 8]    [12]    [1 8]    [1 8]    [8]               
   s(f(x,y)) = [0 1]x + [0 1]y + [1 ] >= [0 1]x + [0 1]y + [1] = f(s(y),s(x))
   
               [1 9]    [1  16]    [24]    [1 9]    [1  16]    [20]               
   s(g(x,y)) = [0 1]x + [0  1 ]y + [1 ] >= [0 1]x + [0  1 ]y + [1 ] = g(s(x),s(y))
   
                  [1]         
   f(x,a()) = x + [1] >= x = x
   
                  [1]         
   f(a(),y) = y + [1] >= y = y
   
                      [1 1]    [1 8]    [1 1]    [1 8]    [24]    [1 1]    [1 8]    [1 1]    [1 8]    [21]                   
   f(g(x,y),g(u,v)) = [0 1]u + [0 1]v + [0 1]x + [0 1]y + [3 ] >= [0 1]u + [0 1]v + [0 1]x + [0 1]y + [3 ] = g(f(x,u),f(y,v))
   
                [14]    [1]      
   g(a(),a()) = [1 ] >= [0] = a()
  problem:
   
  Qed