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:
 RT Transformation Processor:
  strict:
   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))))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [d](x0) = x0 + 16,
    
    [b](x0) = x0 + 6,
    
    [c](x0) = x0 + 8,
    
    [a](x0) = x0 + 4
   orientation:
    b(c(a(x1))) = x1 + 18 >= x1 + 28 = a(b(a(b(c(x1)))))
    
    b(x1) = x1 + 6 >= x1 + 16 = c(c(x1))
    
    c(d(x1)) = x1 + 24 >= x1 + 22 = a(b(c(a(x1))))
    
    a(a(x1)) = x1 + 8 >= x1 + 22 = a(c(b(a(x1))))
   problem:
    strict:
     b(c(a(x1))) -> a(b(a(b(c(x1)))))
     b(x1) -> c(c(x1))
     a(a(x1)) -> a(c(b(a(x1))))
    weak:
     c(d(x1)) -> a(b(c(a(x1))))
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [d](x0) = x0 + 24,
     
     [b](x0) = x0 + 13,
     
     [c](x0) = x0 + 1,
     
     [a](x0) = x0 + 1
    orientation:
     b(c(a(x1))) = x1 + 15 >= x1 + 29 = a(b(a(b(c(x1)))))
     
     b(x1) = x1 + 13 >= x1 + 2 = c(c(x1))
     
     a(a(x1)) = x1 + 2 >= x1 + 16 = a(c(b(a(x1))))
     
     c(d(x1)) = x1 + 25 >= x1 + 16 = a(b(c(a(x1))))
    problem:
     strict:
      b(c(a(x1))) -> a(b(a(b(c(x1)))))
      a(a(x1)) -> a(c(b(a(x1))))
     weak:
      b(x1) -> c(c(x1))
      c(d(x1)) -> a(b(c(a(x1))))
    Bounds Processor:
     bound: 4
     enrichment: match-rt
     automaton:
      final states: {6,5}
      transitions:
       b3(202) -> 203*
       b3(369) -> 370*
       b3(391) -> 392*
       b3(367) -> 368*
       a1(27) -> 28*
       a1(69) -> 70*
       a1(29) -> 30*
       a1(24) -> 25*
       c4(486) -> 487*
       c4(503) -> 504*
       c4(473) -> 474*
       c4(490) -> 491*
       c4(487) -> 488*
       c4(472) -> 473*
       c4(504) -> 505*
       c4(489) -> 490*
       b1(70) -> 71*
       b1(25) -> 26*
       b1(68) -> 69*
       b1(43) -> 44*
       c1(147) -> 148*
       c1(127) -> 128*
       c1(67) -> 68*
       c1(109) -> 110*
       c1(26) -> 27*
       c1(350) -> 351*
       c1(83) -> 84*
       c1(85) -> 86*
       a2(45) -> 46*
       a2(224) -> 225*
       a2(161) -> 162*
       a2(163) -> 164*
       a2(48) -> 49*
       b2(222) -> 223*
       b2(162) -> 163*
       b2(253) -> 254*
       b2(46) -> 47*
       b2(160) -> 161*
       b0(5) -> 5*
       b0(6) -> 5*
       c2(182) -> 183*
       c2(364) -> 365*
       c2(107) -> 108*
       c2(304) -> 305*
       c2(47) -> 48*
       c2(159) -> 160*
       c2(129) -> 130*
       c2(321) -> 322*
       c2(348) -> 349*
       c2(106) -> 107*
       c2(303) -> 304*
       c2(223) -> 224*
       c2(180) -> 181*
       c2(165) -> 166*
       c2(322) -> 323*
       c0(5) -> 5*
       c0(6) -> 5*
       c3(459) -> 460*
       c3(429) -> 430*
       c3(441) -> 442*
       c3(366) -> 367*
       c3(144) -> 145*
       c3(443) -> 444*
       c3(460) -> 461*
       c3(440) -> 441*
       c3(430) -> 431*
       c3(203) -> 204*
       c3(427) -> 428*
       c3(392) -> 393*
       c3(145) -> 146*
       a0(5) -> 5*
       a0(6) -> 5*
       a3(204) -> 205*
       a3(201) -> 202*
       a3(393) -> 394*
       a3(368) -> 369*
       a3(420) -> 421*
       a3(370) -> 371*
       d0(5) -> 6*
       d0(6) -> 6*
       5 -> 83,24
       6 -> 85,29
       24 -> 182*
       25 -> 147,129
       27 -> 165,67,45
       28 -> 181,160,161,86,68,109,69,25,43,5
       29 -> 180*
       30 -> 25*
       43 -> 106*
       44 -> 26*
       46 -> 144*
       48 -> 159*
       49 -> 162,70,25
       68 -> 321*
       70 -> 303*
       71 -> 27*
       84 -> 127,68
       86 -> 109,68
       108 -> 44*
       110 -> 5*
       128 -> 5*
       130 -> 107*
       146 -> 254,47
       148 -> 70*
       160 -> 459*
       162 -> 440*
       163 -> 427,364,201
       164 -> 161,71,69,222,27,67
       166 -> 160*
       181 -> 160*
       183 -> 160*
       202 -> 472*
       205 -> 162,46,144
       222 -> 429*
       224 -> 420,366,350,348
       225 -> 70,253,28,43,5,83,24,182,25,106
       253 -> 443*
       254 -> 47*
       305 -> 71,27,67
       323 -> 69*
       349 -> 160*
       351 -> 68*
       365 -> 160*
       367 -> 489*
       369 -> 503*
       371 -> 391,161
       391 -> 486*
       394 -> 162*
       421 -> 202*
       428 -> 367*
       431 -> 223*
       442 -> 163,201
       444 -> 145*
       461 -> 161*
       474 -> 203*
       488 -> 392*
       491 -> 368*
       505 -> 370*
     problem:
      strict:
       b(c(a(x1))) -> a(b(a(b(c(x1)))))
      weak:
       a(a(x1)) -> a(c(b(a(x1))))
       b(x1) -> c(c(x1))
       c(d(x1)) -> a(b(c(a(x1))))
     Bounds Processor:
      bound: 4
      enrichment: match-rt
      automaton:
       final states: {6,5}
       transitions:
        b3(257) -> 258*
        b3(202) -> 203*
        b3(172) -> 173*
        b3(251) -> 252*
        b3(133) -> 134*
        b3(170) -> 171*
        b3(145) -> 146*
        b3(135) -> 136*
        a1(15) -> 16*
        a1(17) -> 18*
        a1(106) -> 107*
        a1(46) -> 47*
        a1(48) -> 49*
        c4(282) -> 283*
        c4(277) -> 278*
        c4(294) -> 295*
        c4(214) -> 215*
        c4(276) -> 277*
        c4(246) -> 247*
        c4(308) -> 309*
        c4(298) -> 299*
        c4(283) -> 284*
        c4(213) -> 214*
        c4(305) -> 306*
        c4(295) -> 296*
        c4(245) -> 246*
        c4(307) -> 308*
        c4(297) -> 298*
        b1(37) -> 38*
        b1(14) -> 15*
        b1(16) -> 17*
        b1(105) -> 106*
        c1(25) -> 26*
        c1(77) -> 78*
        c1(104) -> 105*
        c1(79) -> 80*
        c1(261) -> 262*
        c1(19) -> 20*
        c1(161) -> 162*
        c1(126) -> 127*
        c1(118) -> 119*
        c1(38) -> 39*
        c1(13) -> 14*
        c1(195) -> 196*
        a2(112) -> 113*
        a2(159) -> 160*
        a2(59) -> 60*
        a2(29) -> 30*
        a2(181) -> 182*
        a2(61) -> 62*
        a2(31) -> 32*
        a2(110) -> 111*
        b2(30) -> 31*
        b2(157) -> 158*
        b2(57) -> 58*
        b2(109) -> 110*
        b2(111) -> 112*
        b2(28) -> 29*
        b0(5) -> 5*
        b0(6) -> 5*
        c2(70) -> 71*
        c2(222) -> 223*
        c2(167) -> 168*
        c2(92) -> 93*
        c2(269) -> 270*
        c2(27) -> 28*
        c2(179) -> 180*
        c2(226) -> 227*
        c2(71) -> 72*
        c2(223) -> 224*
        c2(193) -> 194*
        c2(158) -> 159*
        c2(128) -> 129*
        c2(108) -> 109*
        c2(93) -> 94*
        c2(58) -> 59*
        c2(225) -> 226*
        c2(130) -> 131*
        c2(120) -> 121*
        c0(5) -> 5*
        c0(6) -> 5*
        c3(267) -> 268*
        c3(252) -> 253*
        c3(242) -> 243*
        c3(217) -> 218*
        c3(132) -> 133*
        c3(67) -> 68*
        c3(219) -> 220*
        c3(169) -> 170*
        c3(286) -> 287*
        c3(216) -> 217*
        c3(146) -> 147*
        c3(96) -> 97*
        c3(243) -> 244*
        c3(203) -> 204*
        c3(285) -> 286*
        c3(68) -> 69*
        c3(220) -> 221*
        c3(185) -> 186*
        c3(95) -> 96*
        a0(5) -> 5*
        a0(6) -> 5*
        a3(147) -> 148*
        a3(204) -> 205*
        a3(134) -> 135*
        a3(201) -> 202*
        a3(171) -> 172*
        a3(136) -> 137*
        a3(253) -> 254*
        a3(173) -> 174*
        a3(250) -> 251*
        d0(5) -> 6*
        d0(6) -> 6*
        5 -> 46,13
        6 -> 48,19
        14 -> 92,79
        15 -> 195*
        16 -> 70*
        17 -> 61,27,25
        18 -> 47,110,37,15,5
        20 -> 77,14
        26 -> 14*
        28 -> 67*
        30 -> 95*
        31 -> 201,193,185
        32 -> 106,110,57,15
        37 -> 222*
        39 -> 17*
        46 -> 108*
        47 -> 104,37
        48 -> 128*
        49 -> 126,37
        57 -> 242*
        59 -> 267,261,179
        60 -> 107,111,47,16
        62 -> 57*
        69 -> 29*
        72 -> 17*
        78 -> 5,13
        80 -> 5,13
        94 -> 15*
        97 -> 31*
        105 -> 225*
        106 -> 181,130,118
        107 -> 129,109,20,5,13,14
        109 -> 216*
        110 -> 269*
        111 -> 219*
        112 -> 250,132,120
        113 -> 15,195,157,106
        119 -> 14*
        121 -> 28*
        127 -> 105*
        129 -> 109*
        131 -> 28*
        133 -> 245*
        135 -> 213*
        137 -> 145,29
        145 -> 282*
        148 -> 30,95
        157 -> 285*
        159 -> 169,167,161
        160 -> 16,107
        162 -> 14*
        168 -> 28*
        170 -> 294*
        172 -> 276*
        174 -> 257,110
        180 -> 109*
        182 -> 57*
        186 -> 133*
        194 -> 28*
        196 -> 17*
        202 -> 297*
        205 -> 182,57,242,111
        215 -> 136*
        218 -> 110*
        221 -> 112,120,132
        224 -> 38*
        227 -> 106*
        244 -> 58*
        247 -> 134*
        251 -> 307*
        254 -> 182,57,242
        257 -> 305*
        258 -> 203*
        262 -> 14*
        268 -> 170*
        270 -> 59*
        278 -> 173*
        284 -> 146*
        287 -> 158*
        296 -> 171*
        299 -> 258,203
        306 -> 298*
        309 -> 252*
      problem:
       strict:
        
       weak:
        b(c(a(x1))) -> a(b(a(b(c(x1)))))
        a(a(x1)) -> a(c(b(a(x1))))
        b(x1) -> c(c(x1))
        c(d(x1)) -> a(b(c(a(x1))))
      Qed