YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   c(a(b(a(b(x1))))) -> a(b(a(b(b(a(b(b(c(a(b(c(a(x1)))))))))))))
  weak:
   
  Bounds Processor:
   bound: 3
   enrichment: match-rt
   automaton:
    final states: {4}
    transitions:
     a3(122) -> 123*
     a3(129) -> 130*
     a3(119) -> 120*
     a3(131) -> 132*
     a3(126) -> 127*
     a1(22) -> 23*
     a1(39) -> 40*
     a1(29) -> 30*
     a1(19) -> 20*
     a1(31) -> 32*
     a1(26) -> 27*
     a1(33) -> 34*
     b3(127) -> 128*
     b3(124) -> 125*
     b3(121) -> 122*
     b3(128) -> 129*
     b3(130) -> 131*
     b3(125) -> 126*
     b1(30) -> 31*
     b1(25) -> 26*
     b1(27) -> 28*
     b1(24) -> 25*
     b1(21) -> 22*
     b1(28) -> 29*
     c3(123) -> 124*
     c3(120) -> 121*
     c1(20) -> 21*
     c1(23) -> 24*
     a2(55) -> 56*
     a2(45) -> 46*
     a2(92) -> 93*
     a2(87) -> 88*
     a2(62) -> 63*
     a2(57) -> 58*
     a2(52) -> 53*
     a2(99) -> 100*
     a2(89) -> 90*
     a2(69) -> 70*
     a2(59) -> 60*
     a2(101) -> 102*
     a2(96) -> 97*
     a2(71) -> 72*
     a2(66) -> 67*
     a2(48) -> 49*
     c0(4) -> 4*
     b2(70) -> 71*
     b2(65) -> 66*
     b2(50) -> 51*
     b2(97) -> 98*
     b2(67) -> 68*
     b2(47) -> 48*
     b2(94) -> 95*
     b2(64) -> 65*
     b2(54) -> 55*
     b2(91) -> 92*
     b2(61) -> 62*
     b2(56) -> 57*
     b2(51) -> 52*
     b2(98) -> 99*
     b2(68) -> 69*
     b2(53) -> 54*
     b2(100) -> 101*
     b2(95) -> 96*
     a0(4) -> 4*
     c2(60) -> 61*
     c2(49) -> 50*
     c2(46) -> 47*
     c2(93) -> 94*
     c2(63) -> 64*
     c2(90) -> 91*
     b0(4) -> 4*
     4 -> 19*
     25 -> 59*
     28 -> 33*
     30 -> 45,39
     32 -> 21,4
     34 -> 20*
     40 -> 20*
     56 -> 89*
     58 -> 24*
     70 -> 87*
     72 -> 21*
     88 -> 46*
     100 -> 119*
     102 -> 61*
     132 -> 64*
   problem:
    strict:
     
    weak:
     c(a(b(a(b(x1))))) -> a(b(a(b(b(a(b(b(c(a(b(c(a(x1)))))))))))))
   Qed