YES(?,O(n^1))

Problem:
 f(a(),b()) -> f(a(),c())
 f(c(),d()) -> f(b(),d())

Proof:
 RT Transformation Processor:
  strict:
   f(a(),b()) -> f(a(),c())
   f(c(),d()) -> f(b(),d())
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [d] = 0,
    
    [c] = 2,
    
    [f](x0, x1) = x0 + x1 + 23,
    
    [b] = 1,
    
    [a] = 3
   orientation:
    f(a(),b()) = 27 >= 28 = f(a(),c())
    
    f(c(),d()) = 25 >= 24 = f(b(),d())
   problem:
    strict:
     f(a(),b()) -> f(a(),c())
    weak:
     f(c(),d()) -> f(b(),d())
   Bounds Processor:
    bound: 1
    enrichment: match-rt
    automaton:
     final states: {5,4,3,2,1}
     transitions:
      f1(8,7) -> 1*
      a1() -> 8*
      c1() -> 7*
      f0(3,1) -> 1*
      f0(3,3) -> 1*
      f0(3,5) -> 1*
      f0(4,2) -> 1*
      f0(4,4) -> 1*
      f0(5,1) -> 1*
      f0(5,3) -> 1*
      f0(5,5) -> 1*
      f0(1,2) -> 1*
      f0(1,4) -> 1*
      f0(2,1) -> 1*
      f0(2,3) -> 1*
      f0(2,5) -> 1*
      f0(3,2) -> 1*
      f0(3,4) -> 1*
      f0(4,1) -> 1*
      f0(4,3) -> 1*
      f0(4,5) -> 1*
      f0(5,2) -> 1*
      f0(5,4) -> 1*
      f0(1,1) -> 1*
      f0(1,3) -> 1*
      f0(1,5) -> 1*
      f0(2,2) -> 1*
      f0(2,4) -> 1*
      a0() -> 2*
      b0() -> 3*
      c0() -> 4*
      d0() -> 5*
    problem:
     strict:
      
     weak:
      f(a(),b()) -> f(a(),c())
      f(c(),d()) -> f(b(),d())
    Qed