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:
 RT Transformation Processor:
  strict:
   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()
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [g](x0, x1) = x0 + x1 + 1,
    
    [f](x0, x1) = x0 + x1 + 1,
    
    [s](x0) = x0,
    
    [a] = 0
   orientation:
    s(a()) = 0 >= 0 = a()
    
    s(s(x)) = x >= x = x
    
    s(f(x,y)) = x + y + 1 >= x + y + 1 = f(s(y),s(x))
    
    s(g(x,y)) = x + y + 1 >= x + y + 1 = g(s(x),s(y))
    
    f(x,a()) = x + 1 >= x = x
    
    f(a(),y) = y + 1 >= y = y
    
    f(g(x,y),g(u,v)) = u + v + x + y + 3 >= u + v + x + y + 3 = g(f(x,u),f(y,v))
    
    g(a(),a()) = 1 >= 0 = a()
   problem:
    strict:
     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(g(x,y),g(u,v)) -> g(f(x,u),f(y,v))
    weak:
     f(x,a()) -> x
     f(a(),y) -> y
     g(a(),a()) -> a()
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [g](x0, x1) = x0 + x1,
     
     [f](x0, x1) = x0 + x1,
     
     [s](x0) = x0 + 2,
     
     [a] = 0
    orientation:
     s(a()) = 2 >= 0 = a()
     
     s(s(x)) = x + 4 >= x = x
     
     s(f(x,y)) = x + y + 2 >= x + y + 4 = f(s(y),s(x))
     
     s(g(x,y)) = x + y + 2 >= x + y + 4 = g(s(x),s(y))
     
     f(g(x,y),g(u,v)) = u + v + x + y >= u + v + x + y = g(f(x,u),f(y,v))
     
     f(x,a()) = x >= x = x
     
     f(a(),y) = y >= y = y
     
     g(a(),a()) = 0 >= 0 = a()
    problem:
     strict:
      s(f(x,y)) -> f(s(y),s(x))
      s(g(x,y)) -> g(s(x),s(y))
      f(g(x,y),g(u,v)) -> g(f(x,u),f(y,v))
     weak:
      s(a()) -> a()
      s(s(x)) -> x
      f(x,a()) -> x
      f(a(),y) -> y
      g(a(),a()) -> a()
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [g](x0, x1) = x0 + x1 + 1,
      
      [f](x0, x1) = x0 + x1,
      
      [s](x0) = x0,
      
      [a] = 6
     orientation:
      s(f(x,y)) = x + y >= x + y = f(s(y),s(x))
      
      s(g(x,y)) = x + y + 1 >= x + y + 1 = g(s(x),s(y))
      
      f(g(x,y),g(u,v)) = u + v + x + y + 2 >= u + v + x + y + 1 = g(f(x,u),f(y,v))
      
      s(a()) = 6 >= 6 = a()
      
      s(s(x)) = x >= x = x
      
      f(x,a()) = x + 6 >= x = x
      
      f(a(),y) = y + 6 >= y = y
      
      g(a(),a()) = 13 >= 6 = a()
     problem:
      strict:
       s(f(x,y)) -> f(s(y),s(x))
       s(g(x,y)) -> g(s(x),s(y))
      weak:
       f(g(x,y),g(u,v)) -> g(f(x,u),f(y,v))
       s(a()) -> a()
       s(s(x)) -> x
       f(x,a()) -> x
       f(a(),y) -> y
       g(a(),a()) -> a()
     Matrix Interpretation Processor:
      dimension: 2
      interpretation:
                     [1 1]          [7]
       [g](x0, x1) = [0 1]x0 + x1 + [8],
       
                               [3]
       [f](x0, x1) = x0 + x1 + [4],
       
                 [1 2]     [8]
       [s](x0) = [0 1]x0 + [0],
       
             [1]
       [a] = [0]
      orientation:
                   [1 2]    [1 2]    [19]    [1 2]    [1 2]    [19]               
       s(f(x,y)) = [0 1]x + [0 1]y + [4 ] >= [0 1]x + [0 1]y + [4 ] = f(s(y),s(x))
       
                   [1 3]    [1 2]    [31]    [1 3]    [1 2]    [23]               
       s(g(x,y)) = [0 1]x + [0 1]y + [8 ] >= [0 1]x + [0 1]y + [8 ] = g(s(x),s(y))
       
                          [1 1]        [1 1]        [17]    [1 1]        [1 1]        [17]                   
       f(g(x,y),g(u,v)) = [0 1]u + v + [0 1]x + y + [20] >= [0 1]u + v + [0 1]x + y + [16] = g(f(x,u),f(y,v))
       
                [9]    [1]      
       s(a()) = [0] >= [0] = a()
       
                 [1 4]    [16]         
       s(s(x)) = [0 1]x + [0 ] >= x = x
       
                      [4]         
       f(x,a()) = x + [4] >= x = x
       
                      [4]         
       f(a(),y) = y + [4] >= y = y
       
                    [9]    [1]      
       g(a(),a()) = [8] >= [0] = a()
      problem:
       strict:
        s(f(x,y)) -> f(s(y),s(x))
       weak:
        s(g(x,y)) -> g(s(x),s(y))
        f(g(x,y),g(u,v)) -> g(f(x,u),f(y,v))
        s(a()) -> a()
        s(s(x)) -> x
        f(x,a()) -> x
        f(a(),y) -> y
        g(a(),a()) -> a()
      Matrix Interpretation Processor:
       dimension: 2
       interpretation:
                      [1 9]     [1 8]     [0]
        [g](x0, x1) = [0 1]x0 + [0 1]x1 + [5],
        
                      [1 2]     [1 2]     [1]
        [f](x0, x1) = [0 1]x0 + [0 1]x1 + [1],
        
                  [1 2]     [1]
        [s](x0) = [0 1]x0 + [0],
        
              [1]
        [a] = [0]
       orientation:
                    [1 4]    [1 4]    [4]    [1 4]    [1 4]    [3]               
        s(f(x,y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = f(s(y),s(x))
        
                    [1  11]    [1  10]    [11]    [1  11]    [1  10]    [2]               
        s(g(x,y)) = [0  1 ]x + [0  1 ]y + [5 ] >= [0  1 ]x + [0  1 ]y + [5] = g(s(x),s(y))
        
                           [1  11]    [1  10]    [1  11]    [1  10]    [21]    [1  11]    [1  10]    [1  11]    [1  10]    [19]                   
        f(g(x,y),g(u,v)) = [0  1 ]u + [0  1 ]v + [0  1 ]x + [0  1 ]y + [11] >= [0  1 ]u + [0  1 ]v + [0  1 ]x + [0  1 ]y + [7 ] = g(f(x,u),f(y,v))
        
                 [2]    [1]      
        s(a()) = [0] >= [0] = a()
        
                  [1 4]    [2]         
        s(s(x)) = [0 1]x + [0] >= x = x
        
                   [1 2]    [2]         
        f(x,a()) = [0 1]x + [1] >= x = x
        
                   [1 2]    [2]         
        f(a(),y) = [0 1]y + [1] >= y = y
        
                     [2]    [1]      
        g(a(),a()) = [5] >= [0] = a()
       problem:
        strict:
         
        weak:
         s(f(x,y)) -> f(s(y),s(x))
         s(g(x,y)) -> g(s(x),s(y))
         f(g(x,y),g(u,v)) -> g(f(x,u),f(y,v))
         s(a()) -> a()
         s(s(x)) -> x
         f(x,a()) -> x
         f(a(),y) -> y
         g(a(),a()) -> a()
       Qed