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(137) -> 138*
    b3(184) -> 185*
    b3(179) -> 180*
    b3(139) -> 140*
    b3(226) -> 227*
    b3(186) -> 187*
    b3(303) -> 304*
    b3(240) -> 241*
    a1(15) -> 16*
    a1(17) -> 18*
    a1(36) -> 37*
    a1(33) -> 34*
    c4(277) -> 278*
    c4(217) -> 218*
    c4(289) -> 290*
    c4(219) -> 220*
    c4(301) -> 302*
    c4(291) -> 292*
    c4(216) -> 217*
    c4(206) -> 207*
    c4(318) -> 319*
    c4(288) -> 289*
    c4(278) -> 279*
    c4(300) -> 301*
    c4(220) -> 221*
    c4(205) -> 206*
    c4(292) -> 293*
    c1(60) -> 61*
    c1(25) -> 26*
    c1(27) -> 28*
    c1(34) -> 35*
    c1(19) -> 20*
    c1(191) -> 192*
    c1(275) -> 276*
    c1(43) -> 44*
    c1(13) -> 14*
    b1(42) -> 43*
    b1(14) -> 15*
    b1(16) -> 17*
    a2(70) -> 71*
    a2(47) -> 48*
    a2(174) -> 175*
    a2(104) -> 105*
    a2(49) -> 50*
    a2(166) -> 167*
    a2(101) -> 102*
    a2(68) -> 69*
    c2(45) -> 46*
    c2(92) -> 93*
    c2(82) -> 83*
    c2(269) -> 270*
    c2(244) -> 245*
    c2(189) -> 190*
    c2(79) -> 80*
    c2(201) -> 202*
    c2(131) -> 132*
    c2(81) -> 82*
    c2(66) -> 67*
    c2(173) -> 174*
    c2(123) -> 124*
    c2(103) -> 104*
    c2(93) -> 94*
    c2(78) -> 79*
    c2(58) -> 59*
    c2(165) -> 166*
    b0(5) -> 5*
    b0(6) -> 5*
    b2(172) -> 173*
    b2(102) -> 103*
    b2(67) -> 68*
    b2(164) -> 165*
    b2(69) -> 70*
    b2(46) -> 47*
    b2(48) -> 49*
    c0(5) -> 5*
    c0(6) -> 5*
    a3(242) -> 243*
    a3(187) -> 188*
    a3(311) -> 312*
    a3(181) -> 182*
    a3(228) -> 229*
    a3(178) -> 179*
    a3(138) -> 139*
    a3(230) -> 231*
    a3(225) -> 226*
    a3(185) -> 186*
    a3(140) -> 141*
    a0(5) -> 5*
    a0(6) -> 5*
    c3(267) -> 268*
    c3(227) -> 228*
    c3(157) -> 158*
    c3(142) -> 143*
    c3(214) -> 215*
    c3(159) -> 160*
    c3(149) -> 150*
    c3(241) -> 242*
    c3(211) -> 212*
    c3(156) -> 157*
    c3(146) -> 147*
    c3(136) -> 137*
    c3(213) -> 214*
    c3(203) -> 204*
    c3(183) -> 184*
    c3(148) -> 149*
    c3(143) -> 144*
    c3(210) -> 211*
    c3(180) -> 181*
    c3(160) -> 161*
    c3(145) -> 146*
    d0(5) -> 6*
    d0(6) -> 6*
    5 -> 33,13
    6 -> 36,19
    14 -> 78,27
    16 -> 81*
    17 -> 101,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 -> 145*
    47 -> 244*
    48 -> 148*
    49 -> 178,136,131
    50 -> 15,172,17
    59 -> 46*
    61 -> 14*
    67 -> 142*
    69 -> 156*
    70 -> 225,203,201
    71 -> 164,17,47,15
    80 -> 15*
    83 -> 17*
    94 -> 43*
    102 -> 159*
    104 -> 123*
    105 -> 48,148,16,34,42
    124 -> 46*
    132 -> 67*
    137 -> 219*
    139 -> 216*
    141 -> 240,68
    144 -> 68*
    147 -> 47*
    150 -> 49*
    158 -> 70*
    161 -> 103*
    164 -> 213*
    166 -> 311,275,269,267
    167 -> 18,47,34,42,5,92,15,20,46,78,16
    172 -> 210*
    174 -> 230,191,189,183
    175 -> 16,81,18
    179 -> 205*
    182 -> 102*
    184 -> 300*
    186 -> 291*
    188 -> 303,47
    190 -> 46*
    192 -> 14*
    202 -> 67*
    204 -> 137*
    207 -> 180*
    212 -> 173*
    215 -> 165*
    218 -> 140*
    221 -> 138*
    226 -> 277*
    229 -> 48,102,159,148
    231 -> 226*
    240 -> 288*
    243 -> 69,156
    245 -> 104*
    268 -> 184*
    270 -> 46*
    276 -> 14*
    279 -> 304,227
    290 -> 241*
    293 -> 187*
    302 -> 185*
    303 -> 318*
    304 -> 227*
    312 -> 226*
    319 -> 278*
  problem:
   
  Qed