YES(?,O(n^3))

Problem:
 g(s(x)) -> f(x)
 f(0()) -> s(0())
 f(s(x)) -> s(s(g(x)))
 g(0()) -> 0()

Proof:
 RT Transformation Processor:
  strict:
   g(s(x)) -> f(x)
   f(0()) -> s(0())
   f(s(x)) -> s(s(g(x)))
   g(0()) -> 0()
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [0] = 0,
    
    [f](x0) = x0 + 18,
    
    [g](x0) = x0 + 27,
    
    [s](x0) = x0 + 1
   orientation:
    g(s(x)) = x + 28 >= x + 18 = f(x)
    
    f(0()) = 18 >= 1 = s(0())
    
    f(s(x)) = x + 19 >= x + 29 = s(s(g(x)))
    
    g(0()) = 27 >= 0 = 0()
   problem:
    strict:
     f(s(x)) -> s(s(g(x)))
    weak:
     g(s(x)) -> f(x)
     f(0()) -> s(0())
     g(0()) -> 0()
   Matrix Interpretation Processor:
    dimension: 3
    interpretation:
           [2]
     [0] = [0]
           [7],
     
               [1 0 1]     [0]
     [f](x0) = [0 0 0]x0 + [0]
               [0 0 1]     [2],
     
               [1 0 1]     [0]
     [g](x0) = [0 0 0]x0 + [0]
               [0 0 1]     [1],
     
               [1 0 0]     [0]
     [s](x0) = [0 0 0]x0 + [0]
               [0 0 1]     [1]
    orientation:
               [1 0 1]    [1]    [1 0 1]    [0]             
     f(s(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = s(s(g(x)))
               [0 0 1]    [3]    [0 0 1]    [3]             
     
               [1 0 1]    [1]    [1 0 1]    [0]       
     g(s(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = f(x)
               [0 0 1]    [2]    [0 0 1]    [2]       
     
              [9]    [2]         
     f(0()) = [0] >= [0] = s(0())
              [9]    [8]         
     
              [9]    [2]      
     g(0()) = [0] >= [0] = 0()
              [8]    [7]      
    problem:
     strict:
      
     weak:
      f(s(x)) -> s(s(g(x)))
      g(s(x)) -> f(x)
      f(0()) -> s(0())
      g(0()) -> 0()
    Qed