YES

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

Proof:
 String Reversal Processor:
  b(b(a(a(x1)))) -> a(a(a(a(a(b(b(b(x1))))))))
  Bounds Processor:
   bound: 5
   enrichment: match
   automaton:
    final states: {2,1}
    transitions:
     b3(252) -> 253*
     b3(212) -> 213*
     b3(152) -> 153*
     b3(254) -> 255*
     b3(214) -> 215*
     b3(204) -> 205*
     b3(194) -> 195*
     b3(174) -> 175*
     b3(154) -> 155*
     b3(129) -> 130*
     b3(261) -> 262*
     b3(196) -> 197*
     b3(176) -> 177*
     b3(161) -> 162*
     b3(253) -> 254*
     b3(213) -> 214*
     b3(203) -> 204*
     b3(153) -> 154*
     b3(128) -> 129*
     b3(205) -> 206*
     b3(195) -> 196*
     b3(175) -> 176*
     b3(130) -> 131*
     a4(272) -> 273*
     a4(237) -> 238*
     a4(389) -> 390*
     a4(359) -> 360*
     a4(354) -> 355*
     a4(329) -> 330*
     a4(314) -> 315*
     a4(304) -> 305*
     a4(284) -> 285*
     a4(274) -> 275*
     a4(239) -> 240*
     a4(386) -> 387*
     a4(361) -> 362*
     a4(351) -> 352*
     a4(331) -> 332*
     a4(311) -> 312*
     a4(301) -> 302*
     a4(281) -> 282*
     a4(271) -> 272*
     a4(236) -> 237*
     a4(388) -> 389*
     a4(363) -> 364*
     a4(353) -> 354*
     a4(328) -> 329*
     a4(313) -> 314*
     a4(303) -> 304*
     a4(283) -> 284*
     a4(273) -> 274*
     a4(238) -> 239*
     a4(390) -> 391*
     a4(360) -> 361*
     a4(350) -> 351*
     a4(330) -> 331*
     a4(310) -> 311*
     a4(305) -> 306*
     a4(285) -> 286*
     a4(270) -> 271*
     a4(235) -> 236*
     a4(387) -> 388*
     a4(362) -> 363*
     a4(352) -> 353*
     a4(332) -> 333*
     a4(312) -> 313*
     a4(302) -> 303*
     a4(282) -> 283*
     b4(267) -> 268*
     b4(232) -> 233*
     b4(384) -> 385*
     b4(349) -> 350*
     b4(334) -> 335*
     b4(309) -> 310*
     b4(299) -> 300*
     b4(279) -> 280*
     b4(269) -> 270*
     b4(234) -> 235*
     b4(356) -> 357*
     b4(326) -> 327*
     b4(383) -> 384*
     b4(358) -> 359*
     b4(348) -> 349*
     b4(308) -> 309*
     b4(298) -> 299*
     b4(278) -> 279*
     b4(268) -> 269*
     b4(233) -> 234*
     b4(385) -> 386*
     b4(325) -> 326*
     b4(300) -> 301*
     b4(280) -> 281*
     b4(357) -> 358*
     b4(347) -> 348*
     b4(327) -> 328*
     b4(307) -> 308*
     b4(287) -> 288*
     b0(2) -> 1*
     b0(1) -> 1*
     a5(409) -> 410*
     a5(399) -> 400*
     a5(411) -> 412*
     a5(396) -> 397*
     a5(408) -> 409*
     a5(398) -> 399*
     a5(410) -> 411*
     a5(395) -> 396*
     a5(412) -> 413*
     a5(397) -> 398*
     a0(2) -> 2*
     a0(1) -> 2*
     b5(394) -> 395*
     b5(406) -> 407*
     b5(393) -> 394*
     b5(405) -> 406*
     b5(407) -> 408*
     b5(392) -> 393*
     a1(40) -> 41*
     a1(10) -> 11*
     a1(37) -> 38*
     a1(7) -> 8*
     a1(39) -> 40*
     a1(9) -> 10*
     a1(36) -> 37*
     a1(11) -> 12*
     a1(38) -> 39*
     a1(8) -> 9*
     b1(35) -> 36*
     b1(5) -> 6*
     b1(44) -> 45*
     b1(34) -> 35*
     b1(4) -> 5*
     b1(111) -> 112*
     b1(66) -> 67*
     b1(31) -> 32*
     b1(6) -> 7*
     b1(33) -> 34*
     a2(60) -> 61*
     a2(187) -> 188*
     a2(122) -> 123*
     a2(92) -> 93*
     a2(62) -> 63*
     a2(189) -> 190*
     a2(124) -> 125*
     a2(89) -> 90*
     a2(59) -> 60*
     a2(186) -> 187*
     a2(126) -> 127*
     a2(91) -> 92*
     a2(61) -> 62*
     a2(188) -> 189*
     a2(123) -> 124*
     a2(88) -> 89*
     a2(58) -> 59*
     a2(190) -> 191*
     a2(125) -> 126*
     a2(90) -> 91*
     b2(55) -> 56*
     b2(117) -> 118*
     b2(87) -> 88*
     b2(57) -> 58*
     b2(184) -> 185*
     b2(139) -> 140*
     b2(119) -> 120*
     b2(109) -> 110*
     b2(79) -> 80*
     b2(64) -> 65*
     b2(141) -> 142*
     b2(121) -> 122*
     b2(86) -> 87*
     b2(56) -> 57*
     b2(183) -> 184*
     b2(103) -> 104*
     b2(185) -> 186*
     b2(120) -> 121*
     b2(115) -> 116*
     b2(85) -> 86*
     a3(257) -> 258*
     a3(217) -> 218*
     a3(207) -> 208*
     a3(197) -> 198*
     a3(177) -> 178*
     a3(157) -> 158*
     a3(132) -> 133*
     a3(259) -> 260*
     a3(219) -> 220*
     a3(209) -> 210*
     a3(199) -> 200*
     a3(179) -> 180*
     a3(159) -> 160*
     a3(134) -> 135*
     a3(256) -> 257*
     a3(216) -> 217*
     a3(206) -> 207*
     a3(201) -> 202*
     a3(181) -> 182*
     a3(156) -> 157*
     a3(131) -> 132*
     a3(258) -> 259*
     a3(218) -> 219*
     a3(208) -> 209*
     a3(198) -> 199*
     a3(178) -> 179*
     a3(158) -> 159*
     a3(133) -> 134*
     a3(255) -> 256*
     a3(215) -> 216*
     a3(210) -> 211*
     a3(200) -> 201*
     a3(180) -> 181*
     a3(155) -> 156*
     a3(135) -> 136*
     1 -> 31*
     2 -> 4*
     7 -> 119*
     8 -> 64*
     9 -> 85*
     10 -> 55,44
     11 -> 33*
     12 -> 6,32,1
     32 -> 5*
     36 -> 141*
     37 -> 103*
     38 -> 117*
     39 -> 79*
     40 -> 66*
     41 -> 6,1,32
     45 -> 5*
     58 -> 174*
     59 -> 161,139
     60 -> 152*
     61 -> 128,115,111
     62 -> 109*
     63 -> 120,57,1,31,7,32,6
     65 -> 56*
     67 -> 5*
     80 -> 56*
     89 -> 203*
     91 -> 183*
     93 -> 35*
     104 -> 56*
     110 -> 56*
     112 -> 5*
     116 -> 56*
     118 -> 56*
     127 -> 87*
     132 -> 334*
     134 -> 287*
     136 -> 175,122,121
     140 -> 56*
     142 -> 56*
     156 -> 232*
     158 -> 212*
     160 -> 154,130,57
     162 -> 153*
     182 -> 154*
     187 -> 252*
     189 -> 194*
     191 -> 142*
     197 -> 347*
     198 -> 298*
     199 -> 307*
     200 -> 267*
     201 -> 261*
     202 -> 58*
     211 -> 185*
     216 -> 325*
     218 -> 278*
     220 -> 175*
     240 -> 214*
     256 -> 383*
     258 -> 356*
     260 -> 196*
     262 -> 153*
     275 -> 176*
     286 -> 177*
     288 -> 279*
     306 -> 269*
     315 -> 154*
     333 -> 280*
     335 -> 326*
     355 -> 309*
     360 -> 405*
     362 -> 392*
     364 -> 348*
     391 -> 358*
     400 -> 350*
     413 -> 394*
   problem:
    
   Qed