YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 4
  enrichment: match
  automaton:
   final states: {6,5}
   transitions:
    b3(174) -> 175*
    b3(169) -> 170*
    b3(176) -> 177*
    b3(131) -> 132*
    b3(218) -> 219*
    b3(133) -> 134*
    b3(265) -> 266*
    b3(287) -> 288*
    a1(15) -> 16*
    a1(17) -> 18*
    a1(36) -> 37*
    a1(33) -> 34*
    c4(282) -> 283*
    c4(262) -> 263*
    c4(257) -> 258*
    c4(202) -> 203*
    c4(192) -> 193*
    c4(254) -> 255*
    c4(296) -> 297*
    c4(206) -> 207*
    c4(191) -> 192*
    c4(283) -> 284*
    c4(263) -> 264*
    c4(258) -> 259*
    c4(203) -> 204*
    c4(295) -> 296*
    c4(255) -> 256*
    c4(205) -> 206*
    c1(60) -> 61*
    c1(25) -> 26*
    c1(27) -> 28*
    c1(34) -> 35*
    c1(19) -> 20*
    c1(43) -> 44*
    c1(13) -> 14*
    b1(42) -> 43*
    b1(14) -> 15*
    b1(16) -> 17*
    a2(70) -> 71*
    a2(97) -> 98*
    a2(47) -> 48*
    a2(49) -> 50*
    a2(166) -> 167*
    a2(68) -> 69*
    a2(160) -> 161*
    a2(100) -> 101*
    c2(252) -> 253*
    c2(45) -> 46*
    c2(117) -> 118*
    c2(92) -> 93*
    c2(82) -> 83*
    c2(159) -> 160*
    c2(99) -> 100*
    c2(79) -> 80*
    c2(81) -> 82*
    c2(66) -> 67*
    c2(93) -> 94*
    c2(78) -> 79*
    c2(58) -> 59*
    c2(185) -> 186*
    c2(165) -> 166*
    c2(125) -> 126*
    b0(5) -> 5*
    b0(6) -> 5*
    b2(67) -> 68*
    b2(164) -> 165*
    b2(69) -> 70*
    b2(46) -> 47*
    b2(158) -> 159*
    b2(98) -> 99*
    b2(48) -> 49*
    c0(5) -> 5*
    c0(6) -> 5*
    a3(267) -> 268*
    a3(177) -> 178*
    a3(132) -> 133*
    a3(134) -> 135*
    a3(171) -> 172*
    a3(208) -> 209*
    a3(168) -> 169*
    a3(220) -> 221*
    a3(210) -> 211*
    a3(175) -> 176*
    a0(5) -> 5*
    a0(6) -> 5*
    c3(197) -> 198*
    c3(142) -> 143*
    c3(137) -> 138*
    c3(219) -> 220*
    c3(199) -> 200*
    c3(189) -> 190*
    c3(154) -> 155*
    c3(139) -> 140*
    c3(246) -> 247*
    c3(196) -> 197*
    c3(151) -> 152*
    c3(136) -> 137*
    c3(248) -> 249*
    c3(173) -> 174*
    c3(153) -> 154*
    c3(143) -> 144*
    c3(280) -> 281*
    c3(200) -> 201*
    c3(170) -> 171*
    c3(150) -> 151*
    c3(140) -> 141*
    c3(130) -> 131*
    d0(5) -> 6*
    d0(6) -> 6*
    5 -> 33,13
    6 -> 36,19
    14 -> 78,27
    16 -> 81*
    17 -> 97,66,60
    18 -> 46,47,34,42,20,25,14,27,15,5
    20 -> 25,14
    26 -> 5*
    28 -> 5*
    33 -> 58*
    34 -> 42*
    35 -> 16*
    36 -> 45*
    37 -> 34*
    42 -> 92*
    44 -> 17*
    46 -> 150*
    48 -> 142*
    49 -> 168,130,125
    50 -> 164,17
    59 -> 46*
    61 -> 14*
    67 -> 153*
    69 -> 136*
    70 -> 208,189,185
    71 -> 158,17,47,15
    80 -> 15*
    83 -> 17*
    94 -> 43*
    98 -> 139*
    100 -> 117*
    101 -> 48,142,16,34,42
    118 -> 46*
    126 -> 67*
    131 -> 191*
    133 -> 202*
    135 -> 218,68
    138 -> 70*
    141 -> 99*
    144 -> 49*
    152 -> 47*
    155 -> 68*
    158 -> 199*
    160 -> 267,248
    161 -> 18,47,5,15,20,46,78,16
    164 -> 196*
    166 -> 210,173
    167 -> 18*
    169 -> 205*
    171 -> 280,252
    172 -> 69,136,287,18,47,5,15,20,46,78,48,16,34,42,92,81,142,98
    174 -> 262*
    176 -> 254*
    177 -> 246*
    178 -> 265,68,15,5,17,47
    186 -> 67*
    190 -> 131*
    193 -> 132*
    198 -> 165*
    201 -> 159*
    204 -> 134*
    207 -> 170*
    209 -> 169*
    211 -> 169*
    218 -> 257*
    221 -> 69,136
    247 -> 174*
    249 -> 174*
    253 -> 46*
    256 -> 177*
    259 -> 219*
    264 -> 175*
    265 -> 282*
    266 -> 170*
    268 -> 169*
    281 -> 174*
    284 -> 266*
    287 -> 295*
    288 -> 170*
    297 -> 288*
  problem:
   
  Qed