YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   c(a(a(b(c(a(x1)))))) -> a(a(b(c(c(a(a(b(c(x1)))))))))
  weak:
   
  Bounds Processor:
   bound: 3
   enrichment: match-rt
   automaton:
    final states: {4}
    transitions:
     a3(89) -> 90*
     a3(84) -> 85*
     a3(111) -> 112*
     a3(106) -> 107*
     a3(88) -> 89*
     a3(83) -> 84*
     a3(110) -> 111*
     a3(105) -> 106*
     a1(22) -> 23*
     a1(17) -> 18*
     a1(23) -> 24*
     a1(18) -> 19*
     b3(87) -> 88*
     b3(82) -> 83*
     b3(109) -> 110*
     b3(104) -> 105*
     b1(21) -> 22*
     b1(16) -> 17*
     c3(107) -> 108*
     c3(86) -> 87*
     c3(81) -> 82*
     c3(108) -> 109*
     c3(103) -> 104*
     c3(85) -> 86*
     c1(75) -> 76*
     c1(20) -> 21*
     c1(15) -> 16*
     c1(39) -> 40*
     c1(19) -> 20*
     a2(32) -> 33*
     a2(27) -> 28*
     a2(59) -> 60*
     a2(54) -> 55*
     a2(58) -> 59*
     a2(53) -> 54*
     a2(33) -> 34*
     a2(28) -> 29*
     c0(4) -> 4*
     b2(57) -> 58*
     b2(52) -> 53*
     b2(31) -> 32*
     b2(26) -> 27*
     a0(4) -> 4*
     c2(55) -> 56*
     c2(30) -> 31*
     c2(25) -> 26*
     c2(29) -> 30*
     c2(91) -> 92*
     c2(56) -> 57*
     c2(51) -> 52*
     c2(63) -> 64*
     b0(4) -> 4*
     4 -> 15*
     22 -> 63*
     23 -> 39,25
     24 -> 16,20,4
     32 -> 103,91
     33 -> 81,75,51
     34 -> 30,16,21,20
     40 -> 16*
     60 -> 16,21
     64 -> 26*
     76 -> 16*
     90 -> 31*
     92 -> 26*
     112 -> 86,56
   problem:
    strict:
     
    weak:
     c(a(a(b(c(a(x1)))))) -> a(a(b(c(c(a(a(b(c(x1)))))))))
   Qed