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:
 RT Transformation Processor:
  strict:
   a(c(b(x1))) -> b(a(b(a(x1))))
   b(x1) -> c(a(c(x1)))
   a(a(x1)) -> a(b(c(a(x1))))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [a](x0) = x0,
    
    [c](x0) = x0 + 16,
    
    [b](x0) = x0
   orientation:
    a(c(b(x1))) = x1 + 16 >= x1 = b(a(b(a(x1))))
    
    b(x1) = x1 >= x1 + 32 = c(a(c(x1)))
    
    a(a(x1)) = x1 >= x1 + 16 = a(b(c(a(x1))))
   problem:
    strict:
     b(x1) -> c(a(c(x1)))
     a(a(x1)) -> a(b(c(a(x1))))
    weak:
     a(c(b(x1))) -> b(a(b(a(x1))))
   Bounds Processor:
    bound: 5
    enrichment: match-rt
    automaton:
     final states: {4}
     transitions:
      a3(232) -> 233*
      a3(197) -> 198*
      a3(294) -> 295*
      a3(229) -> 230*
      a3(341) -> 342*
      a3(336) -> 337*
      a3(201) -> 202*
      a3(181) -> 182*
      a3(338) -> 339*
      a3(298) -> 299*
      a3(430) -> 431*
      a3(370) -> 371*
      a3(103) -> 104*
      a3(437) -> 438*
      a3(317) -> 318*
      b3(429) -> 430*
      b3(339) -> 340*
      b3(231) -> 232*
      b3(343) -> 344*
      b3(337) -> 338*
      c4(464) -> 465*
      c4(409) -> 410*
      c4(399) -> 400*
      c4(411) -> 412*
      c4(458) -> 459*
      c4(405) -> 406*
      c4(320) -> 321*
      c4(462) -> 463*
      c4(407) -> 408*
      c4(397) -> 398*
      c4(322) -> 323*
      a4(406) -> 407*
      a4(321) -> 322*
      a4(463) -> 464*
      a4(398) -> 399*
      a4(460) -> 461*
      a4(410) -> 411*
      a4(457) -> 458*
      b0(4) -> 4*
      b4(459) -> 460*
      c0(4) -> 4*
      c5(475) -> 476*
      c5(477) -> 478*
      a0(4) -> 4*
      a5(476) -> 477*
      c1(69) -> 70*
      c1(19) -> 20*
      c1(71) -> 72*
      c1(23) -> 24*
      a1(70) -> 71*
      a1(247) -> 248*
      a1(107) -> 108*
      a1(21) -> 22*
      a1(18) -> 19*
      a1(155) -> 156*
      a1(479) -> 480*
      b1(20) -> 21*
      b1(106) -> 107*
      b1(108) -> 109*
      a2(45) -> 46*
      a2(157) -> 158*
      a2(127) -> 128*
      a2(259) -> 260*
      a2(42) -> 43*
      a2(426) -> 427*
      a2(224) -> 225*
      a2(493) -> 494*
      a2(226) -> 227*
      a2(166) -> 167*
      a2(66) -> 67*
      a2(168) -> 169*
      a2(160) -> 161*
      a2(140) -> 141*
      b2(227) -> 228*
      b2(167) -> 168*
      b2(169) -> 170*
      b2(159) -> 160*
      b2(44) -> 45*
      b2(258) -> 259*
      b2(225) -> 226*
      c2(65) -> 66*
      c2(257) -> 258*
      c2(67) -> 68*
      c2(139) -> 140*
      c2(141) -> 142*
      c2(126) -> 127*
      c2(158) -> 159*
      c2(128) -> 129*
      c2(43) -> 44*
      c3(202) -> 203*
      c3(182) -> 183*
      c3(102) -> 103*
      c3(299) -> 300*
      c3(316) -> 317*
      c3(104) -> 105*
      c3(428) -> 429*
      c3(196) -> 197*
      c3(318) -> 319*
      c3(293) -> 294*
      c3(198) -> 199*
      c3(295) -> 296*
      c3(230) -> 231*
      c3(200) -> 201*
      c3(180) -> 181*
      c3(342) -> 343*
      c3(297) -> 298*
      4 -> 69,18
      19 -> 106*
      20 -> 65*
      21 -> 42*
      22 -> 19,23,4
      24 -> 20*
      44 -> 102*
      46 -> 480,19
      68 -> 21,42
      72 -> 4,18
      105 -> 45*
      106 -> 126*
      107 -> 157*
      108 -> 166,155,139
      109 -> 71,19,4
      129 -> 107*
      142 -> 109,19
      156 -> 106*
      159 -> 196*
      161 -> 167,156
      167 -> 200*
      168 -> 229*
      169 -> 370,257,247,224,180
      170 -> 128,19,106,126,71
      183 -> 170*
      199 -> 160*
      203 -> 168*
      225 -> 297*
      226 -> 341*
      227 -> 336,293
      228 -> 108,19,106,126
      231 -> 320*
      233 -> 371,337,225
      248 -> 106*
      258 -> 316*
      260 -> 248*
      296 -> 228*
      300 -> 226*
      319 -> 259*
      323 -> 232*
      337 -> 409*
      338 -> 493,457
      339 -> 479,437,428,426,397
      340 -> 141,158,128
      343 -> 405*
      344 -> 336*
      371 -> 337*
      400 -> 340*
      408 -> 344*
      412 -> 338*
      427 -> 225*
      429 -> 462*
      431 -> 427*
      438 -> 337*
      459 -> 475*
      461 -> 438*
      465 -> 430*
      478 -> 460*
      480 -> 106*
      494 -> 43*
    problem:
     strict:
      b(x1) -> c(a(c(x1)))
     weak:
      a(a(x1)) -> a(b(c(a(x1))))
      a(c(b(x1))) -> b(a(b(a(x1))))
    Bounds Processor:
     bound: 5
     enrichment: match-rt
     automaton:
      final states: {3,2,1}
      transitions:
       a3(262) -> 263*
       a3(232) -> 233*
       a3(192) -> 193*
       a3(289) -> 290*
       a3(82) -> 83*
       a3(154) -> 155*
       a3(346) -> 347*
       a3(266) -> 267*
       a3(211) -> 212*
       a3(368) -> 369*
       a3(113) -> 114*
       a3(240) -> 241*
       a3(190) -> 191*
       a3(352) -> 353*
       a3(332) -> 333*
       a3(100) -> 101*
       a3(287) -> 288*
       b3(331) -> 332*
       b3(191) -> 192*
       b3(288) -> 289*
       b3(213) -> 214*
       b3(193) -> 194*
       b3(290) -> 291*
       c4(217) -> 218*
       c4(197) -> 198*
       c4(304) -> 305*
       c4(294) -> 295*
       c4(306) -> 307*
       c4(338) -> 339*
       c4(313) -> 314*
       c4(203) -> 204*
       c4(340) -> 341*
       c4(215) -> 216*
       c4(205) -> 206*
       c4(195) -> 196*
       c4(292) -> 293*
       a4(339) -> 340*
       a4(204) -> 205*
       a4(216) -> 217*
       a4(196) -> 197*
       a4(293) -> 294*
       a4(315) -> 316*
       a4(305) -> 306*
       a4(312) -> 313*
       b0(2) -> 1*
       b0(1) -> 1*
       b0(3) -> 1*
       b4(314) -> 315*
       c0(2) -> 2*
       c0(1) -> 2*
       c0(3) -> 2*
       c5(326) -> 327*
       c5(328) -> 329*
       a0(2) -> 3*
       a0(1) -> 3*
       a0(3) -> 3*
       a5(327) -> 328*
       c1(20) -> 21*
       c1(5) -> 6*
       c1(27) -> 28*
       c1(7) -> 8*
       c1(18) -> 19*
       a1(45) -> 46*
       a1(52) -> 53*
       a1(124) -> 125*
       a1(29) -> 30*
       a1(358) -> 359*
       a1(126) -> 127*
       a1(26) -> 27*
       a1(6) -> 7*
       a1(178) -> 179*
       a1(43) -> 44*
       a1(180) -> 181*
       b1(127) -> 128*
       b1(51) -> 52*
       b1(53) -> 54*
       b1(28) -> 29*
       b1(125) -> 126*
       a2(65) -> 66*
       a2(237) -> 238*
       a2(172) -> 173*
       a2(77) -> 78*
       a2(32) -> 33*
       a2(219) -> 220*
       a2(149) -> 150*
       a2(134) -> 135*
       a2(94) -> 95*
       a2(74) -> 75*
       a2(69) -> 70*
       a2(96) -> 97*
       a2(248) -> 249*
       a2(365) -> 366*
       a2(250) -> 251*
       a2(170) -> 171*
       a2(362) -> 363*
       a2(130) -> 131*
       b2(364) -> 365*
       b2(97) -> 98*
       b2(249) -> 250*
       b2(251) -> 252*
       b2(236) -> 237*
       b2(221) -> 222*
       b2(151) -> 152*
       b2(76) -> 77*
       b2(95) -> 96*
       c2(75) -> 76*
       c2(70) -> 71*
       c2(129) -> 130*
       c2(64) -> 65*
       c2(363) -> 364*
       c2(131) -> 132*
       c2(66) -> 67*
       c2(31) -> 32*
       c2(133) -> 134*
       c2(68) -> 69*
       c2(235) -> 236*
       c2(33) -> 34*
       c2(220) -> 221*
       c2(150) -> 151*
       c2(135) -> 136*
       c3(267) -> 268*
       c3(212) -> 213*
       c3(369) -> 370*
       c3(112) -> 113*
       c3(239) -> 240*
       c3(114) -> 115*
       c3(99) -> 100*
       c3(261) -> 262*
       c3(241) -> 242*
       c3(231) -> 232*
       c3(101) -> 102*
       c3(81) -> 82*
       c3(263) -> 264*
       c3(233) -> 234*
       c3(153) -> 154*
       c3(330) -> 331*
       c3(83) -> 84*
       c3(265) -> 266*
       c3(367) -> 368*
       c3(155) -> 156*
       1 -> 43,18
       2 -> 26,20
       3 -> 45,5
       8 -> 1*
       19 -> 6*
       21 -> 6*
       27 -> 51*
       28 -> 31*
       29 -> 74*
       30 -> 46,27,68,3,5
       34 -> 29*
       44 -> 27*
       46 -> 27*
       51 -> 68*
       52 -> 149*
       53 -> 124,94,64
       54 -> 27,51,7,3
       67 -> 54*
       71 -> 52*
       76 -> 81*
       78 -> 46,27,68
       84 -> 77*
       95 -> 125,133,112
       96 -> 211*
       97 -> 235,190,180,172,99
       98 -> 53,94,64,124,70,7,44
       102 -> 98,44,27,68
       115 -> 96*
       125 -> 133*
       126 -> 219*
       127 -> 178,170,129
       128 -> 27,3,51
       132 -> 128,51,68
       136 -> 126*
       151 -> 153*
       152 -> 94*
       156 -> 152*
       171 -> 179,51,95
       173 -> 95*
       179 -> 51*
       181 -> 51*
       191 -> 347,173,95,203
       192 -> 362,312
       193 -> 358,330,287,248,195
       194 -> 66,150,70
       198 -> 194*
       206 -> 192*
       213 -> 215*
       214 -> 190*
       218 -> 214,190
       221 -> 231*
       222 -> 170*
       234 -> 222*
       236 -> 239*
       238 -> 181*
       242 -> 237*
       249 -> 261*
       250 -> 352*
       251 -> 346,265
       252 -> 46,53,94,64,124
       264 -> 250*
       268 -> 252,124
       288 -> 304*
       290 -> 292*
       291 -> 150*
       295 -> 291,150
       307 -> 289*
       314 -> 326*
       316 -> 288,304
       329 -> 315*
       331 -> 338*
       333 -> 249*
       341 -> 332*
       347 -> 191*
       353 -> 212*
       359 -> 51*
       364 -> 367*
       366 -> 359*
       370 -> 365*
     problem:
      strict:
       
      weak:
       b(x1) -> c(a(c(x1)))
       a(a(x1)) -> a(b(c(a(x1))))
       a(c(b(x1))) -> b(a(b(a(x1))))
     Qed