YES(?,O(n^1))

Problem:
 f(a(),a()) -> f(a(),b())
 f(a(),b()) -> f(s(a()),c())
 f(s(X),c()) -> f(X,c())
 f(c(),c()) -> f(a(),a())

Proof:
 RT Transformation Processor:
  strict:
   f(a(),a()) -> f(a(),b())
   f(a(),b()) -> f(s(a()),c())
   f(s(X),c()) -> f(X,c())
   f(c(),c()) -> f(a(),a())
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [c] = 21,
    
    [s](x0) = x0 + 2,
    
    [b] = 4,
    
    [f](x0, x1) = x0 + x1 + 8,
    
    [a] = 9
   orientation:
    f(a(),a()) = 26 >= 21 = f(a(),b())
    
    f(a(),b()) = 21 >= 40 = f(s(a()),c())
    
    f(s(X),c()) = X + 31 >= X + 29 = f(X,c())
    
    f(c(),c()) = 50 >= 26 = f(a(),a())
   problem:
    strict:
     f(a(),b()) -> f(s(a()),c())
    weak:
     f(a(),a()) -> f(a(),b())
     f(s(X),c()) -> f(X,c())
     f(c(),c()) -> f(a(),a())
   Bounds Processor:
    bound: 1
    enrichment: match-rt
    automaton:
     final states: {6}
     transitions:
      f1(11,10) -> 6*
      f1(12,10) -> 6*
      s1(11) -> 12*
      a1() -> 11*
      c1() -> 10*
      f0(6,6) -> 6*
      a0() -> 6*
      b0() -> 6*
      s0(6) -> 6*
      c0() -> 6*
    problem:
     strict:
      
     weak:
      f(a(),b()) -> f(s(a()),c())
      f(a(),a()) -> f(a(),b())
      f(s(X),c()) -> f(X,c())
      f(c(),c()) -> f(a(),a())
    Qed