YES(?,O(n^1))

Problem:
 a(b(a(a(x1)))) -> c(b(a(b(a(x1)))))
 a(c(b(x1))) -> a(a(b(c(b(a(x1))))))

Proof:
 RT Transformation Processor:
  strict:
   a(b(a(a(x1)))) -> c(b(a(b(a(x1)))))
   a(c(b(x1))) -> a(a(b(c(b(a(x1))))))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [c](x0) = x0,
    
    [b](x0) = x0,
    
    [a](x0) = x0 + 1
   orientation:
    a(b(a(a(x1)))) = x1 + 3 >= x1 + 2 = c(b(a(b(a(x1)))))
    
    a(c(b(x1))) = x1 + 1 >= x1 + 3 = a(a(b(c(b(a(x1))))))
   problem:
    strict:
     a(c(b(x1))) -> a(a(b(c(b(a(x1))))))
    weak:
     a(b(a(a(x1)))) -> c(b(a(b(a(x1)))))
   Bounds Processor:
    bound: 3
    enrichment: match-rt
    automaton:
     final states: {4}
     transitions:
      a3(62) -> 63*
      a3(63) -> 64*
      a3(58) -> 59*
      a1(42) -> 43*
      a1(17) -> 18*
      a1(12) -> 13*
      a1(24) -> 25*
      a1(16) -> 17*
      a1(28) -> 29*
      b3(59) -> 60*
      b3(61) -> 62*
      b1(25) -> 26*
      b1(15) -> 16*
      b1(23) -> 24*
      b1(13) -> 14*
      c3(60) -> 61*
      c1(14) -> 15*
      c1(26) -> 27*
      a2(65) -> 66*
      a2(40) -> 41*
      a2(35) -> 36*
      a2(47) -> 48*
      a2(69) -> 70*
      a2(39) -> 40*
      a2(91) -> 92*
      a2(86) -> 87*
      a2(76) -> 77*
      a2(90) -> 91*
      a2(80) -> 81*
      a0(4) -> 4*
      b2(87) -> 88*
      b2(104) -> 105*
      b2(89) -> 90*
      b2(46) -> 47*
      b2(36) -> 37*
      b2(48) -> 49*
      b2(38) -> 39*
      c0(4) -> 4*
      c2(37) -> 38*
      c2(49) -> 50*
      c2(88) -> 89*
      b0(4) -> 4*
      4 -> 12*
      14 -> 42*
      16 -> 65*
      17 -> 69,23
      18 -> 13,4
      24 -> 80*
      25 -> 35,28
      27 -> 77,43,25,35,13,4
      29 -> 13*
      40 -> 46*
      41 -> 29,36,13
      42 -> 76*
      43 -> 25*
      48 -> 86,58
      50 -> 48,58,77,86,43,25,35
      64 -> 59,87,36
      66 -> 46*
      70 -> 46*
      77 -> 46*
      81 -> 46*
      91 -> 104*
      92 -> 29*
      105 -> 47*
    problem:
     strict:
      
     weak:
      a(c(b(x1))) -> a(a(b(c(b(a(x1))))))
      a(b(a(a(x1)))) -> c(b(a(b(a(x1)))))
    Qed