YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 5
  enrichment: match
  automaton:
   final states: {4}
   transitions:
    a3(237) -> 238*
    a3(219) -> 220*
    a3(159) -> 160*
    a3(196) -> 197*
    a3(166) -> 167*
    a3(136) -> 137*
    a3(208) -> 209*
    a3(193) -> 194*
    a3(138) -> 139*
    a3(128) -> 129*
    a3(103) -> 104*
    a3(170) -> 171*
    a3(120) -> 121*
    b3(137) -> 138*
    b3(139) -> 140*
    b3(195) -> 196*
    c4(212) -> 213*
    c4(214) -> 215*
    c4(226) -> 227*
    c4(216) -> 217*
    c4(248) -> 249*
    c4(228) -> 229*
    c4(210) -> 211*
    a4(247) -> 248*
    a4(227) -> 228*
    a4(211) -> 212*
    a4(250) -> 251*
    a4(215) -> 216*
    a0(4) -> 4*
    b4(249) -> 250*
    c0(4) -> 4*
    c5(256) -> 257*
    c5(258) -> 259*
    b0(4) -> 4*
    a5(257) -> 258*
    a1(25) -> 26*
    a1(10) -> 11*
    a1(27) -> 28*
    a1(12) -> 13*
    a1(29) -> 30*
    a1(141) -> 142*
    a1(16) -> 17*
    a1(98) -> 99*
    b1(30) -> 31*
    b1(24) -> 25*
    b1(11) -> 12*
    b1(28) -> 29*
    b1(13) -> 14*
    c1(15) -> 16*
    c1(17) -> 18*
    c1(23) -> 24*
    a2(75) -> 76*
    a2(55) -> 56*
    a2(107) -> 108*
    a2(134) -> 135*
    a2(59) -> 60*
    a2(44) -> 45*
    a2(151) -> 152*
    a2(131) -> 132*
    a2(116) -> 117*
    a2(46) -> 47*
    a2(88) -> 89*
    a2(78) -> 79*
    a2(68) -> 69*
    a2(200) -> 201*
    a2(185) -> 186*
    a2(100) -> 101*
    a2(90) -> 91*
    b2(45) -> 46*
    b2(187) -> 188*
    b2(77) -> 78*
    b2(47) -> 48*
    b2(89) -> 90*
    b2(91) -> 92*
    b2(133) -> 134*
    c2(60) -> 61*
    c2(132) -> 133*
    c2(117) -> 118*
    c2(67) -> 68*
    c2(69) -> 70*
    c2(54) -> 55*
    c2(186) -> 187*
    c2(106) -> 107*
    c2(76) -> 77*
    c2(56) -> 57*
    c2(108) -> 109*
    c2(58) -> 59*
    c2(115) -> 116*
    c3(167) -> 168*
    c3(127) -> 128*
    c3(102) -> 103*
    c3(194) -> 195*
    c3(169) -> 170*
    c3(129) -> 130*
    c3(119) -> 120*
    c3(104) -> 105*
    c3(171) -> 172*
    c3(121) -> 122*
    c3(218) -> 219*
    c3(178) -> 179*
    c3(220) -> 221*
    c3(165) -> 166*
    4 -> 15,10
    11 -> 54,23
    12 -> 131*
    13 -> 58,44,27
    14 -> 11,17,23,4
    18 -> 4*
    24 -> 67*
    25 -> 75*
    26 -> 11,23,4
    28 -> 115*
    29 -> 185*
    30 -> 106,100,98
    31 -> 11,4,23
    45 -> 127*
    46 -> 193*
    47 -> 136,119,88
    48 -> 56,11,17
    57 -> 12*
    61 -> 14,4
    70 -> 25*
    77 -> 102*
    79 -> 11,23
    89 -> 165*
    90 -> 237*
    91 -> 178,159,151,141
    92 -> 13,4,11
    99 -> 11*
    101 -> 99,11,54,45
    105 -> 78*
    109 -> 31*
    118 -> 29*
    122 -> 92,4,10,15,48,17
    130 -> 46*
    133 -> 169*
    135 -> 45,28
    137 -> 226*
    138 -> 247*
    139 -> 210,208,200
    140 -> 60,56,132
    142 -> 11*
    152 -> 45*
    160 -> 137*
    168 -> 90*
    172 -> 134*
    179 -> 120*
    187 -> 218*
    188 -> 100*
    195 -> 214*
    197 -> 160,152,142,11,23,45,137,89
    201 -> 89*
    209 -> 137*
    213 -> 140*
    217 -> 196*
    221 -> 188*
    229 -> 138*
    238 -> 194*
    249 -> 256*
    251 -> 201,209
    259 -> 250*
  problem:
   
  Qed