YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   c(b(a(a(x1)))) -> a(a(b(a(a(b(c(b(a(c(x1))))))))))
  weak:
   
  Bounds Processor:
   bound: 3
   enrichment: match-rt
   automaton:
    final states: {4}
    transitions:
     a3(137) -> 138*
     a3(132) -> 133*
     a3(102) -> 103*
     a3(97) -> 98*
     a3(139) -> 140*
     a3(129) -> 130*
     a3(104) -> 105*
     a3(136) -> 137*
     a3(126) -> 127*
     a3(121) -> 122*
     a3(101) -> 102*
     a3(128) -> 129*
     a3(140) -> 141*
     a3(125) -> 126*
     a3(105) -> 106*
     a1(25) -> 26*
     a1(22) -> 23*
     a1(17) -> 18*
     a1(24) -> 25*
     a1(21) -> 22*
     b3(127) -> 128*
     b3(122) -> 123*
     b3(124) -> 125*
     b3(138) -> 139*
     b3(133) -> 134*
     b3(103) -> 104*
     b3(98) -> 99*
     b3(135) -> 136*
     b3(100) -> 101*
     b1(20) -> 21*
     b1(23) -> 24*
     b1(18) -> 19*
     c3(134) -> 135*
     c3(99) -> 100*
     c3(131) -> 132*
     c3(96) -> 97*
     c3(123) -> 124*
     c3(120) -> 121*
     c1(27) -> 28*
     c1(19) -> 20*
     c1(16) -> 17*
     c1(33) -> 34*
     a2(55) -> 56*
     a2(45) -> 46*
     a2(40) -> 41*
     a2(47) -> 48*
     a2(94) -> 95*
     a2(59) -> 60*
     a2(44) -> 45*
     a2(91) -> 92*
     a2(86) -> 87*
     a2(56) -> 57*
     a2(51) -> 52*
     a2(93) -> 94*
     a2(58) -> 59*
     a2(48) -> 49*
     a2(90) -> 91*
     c0(4) -> 4*
     b2(92) -> 93*
     b2(87) -> 88*
     b2(57) -> 58*
     b2(52) -> 53*
     b2(89) -> 90*
     b2(54) -> 55*
     b2(46) -> 47*
     b2(41) -> 42*
     b2(43) -> 44*
     b0(4) -> 4*
     c2(50) -> 51*
     c2(72) -> 73*
     c2(42) -> 43*
     c2(39) -> 40*
     c2(88) -> 89*
     c2(53) -> 54*
     c2(85) -> 86*
     a0(4) -> 4*
     4 -> 16*
     21 -> 50*
     24 -> 27*
     25 -> 39,33
     26 -> 17,4
     28 -> 17*
     34 -> 17*
     44 -> 120*
     47 -> 85*
     49 -> 20*
     59 -> 72*
     60 -> 28,17
     73 -> 40*
     94 -> 96*
     95 -> 51*
     106 -> 54*
     129 -> 131*
     130 -> 86*
     141 -> 89*
   problem:
    strict:
     
    weak:
     c(b(a(a(x1)))) -> a(a(b(a(a(b(c(b(a(c(x1))))))))))
   Qed