MAYBE

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

Proof:
 Complexity Transformation Processor:
  strict:
   a(a(b(b(b(b(a(a(x1)))))))) -> a(a(c(c(a(a(b(b(x1))))))))
   a(a(c(c(x1)))) -> c(c(c(c(a(a(x1))))))
   c(c(c(c(c(c(x1)))))) -> b(b(c(c(b(b(x1))))))
  weak:
   
  Bounds Processor:
   bound: 1
   enrichment: match
   automaton:
    final states: {4}
    transitions:
     a1(434) -> 435*
     a1(20) -> 21*
     a1(217) -> 218*
     a1(162) -> 163*
     a1(476) -> 477*
     a1(17) -> 18*
     a1(154) -> 155*
     a1(186) -> 187*
     a1(111) -> 112*
     a1(500) -> 501*
     a1(21) -> 22*
     a1(16) -> 17*
     a1(153) -> 154*
     a1(472) -> 473*
     a1(190) -> 191*
     a1(110) -> 111*
     c1(157) -> 158*
     c1(112) -> 113*
     c1(114) -> 115*
     c1(281) -> 282*
     c1(19) -> 20*
     c1(156) -> 157*
     c1(293) -> 294*
     c1(158) -> 159*
     c1(113) -> 114*
     c1(18) -> 19*
     c1(155) -> 156*
     c1(115) -> 116*
     c1(292) -> 293*
     c1(282) -> 283*
     b1(75) -> 76*
     b1(15) -> 16*
     b1(294) -> 295*
     b1(284) -> 285*
     b1(279) -> 280*
     b1(386) -> 387*
     b1(356) -> 357*
     b1(331) -> 332*
     b1(291) -> 292*
     b1(69) -> 70*
     b1(14) -> 15*
     b1(283) -> 284*
     b1(405) -> 406*
     b1(390) -> 391*
     b1(295) -> 296*
     b1(290) -> 291*
     b1(280) -> 281*
     b1(362) -> 363*
     a0(4) -> 4*
     b0(4) -> 4*
     c0(4) -> 4*
     4 -> 110,14
     18 -> 153*
     20 -> 69*
     21 -> 75*
     22 -> 111,112,18,4
     70 -> 15*
     76 -> 15*
     112 -> 476,356
     113 -> 434,386
     114 -> 390,186
     115 -> 405,217
     116 -> 111,112,4
     155 -> 472,279
     156 -> 500,362
     157 -> 290,162
     158 -> 331,190
     159 -> 473,477,155,22
     163 -> 154*
     187 -> 154*
     191 -> 154*
     218 -> 154*
     285 -> 158,157,116,113,115,114,4,20
     296 -> 156,19,159,113,116
     332 -> 291*
     357 -> 280*
     363 -> 280*
     387 -> 280*
     391 -> 280*
     406 -> 280*
     435 -> 154*
     473 -> 154*
     477 -> 154*
     501 -> 154*
   problem:
    strict:
     a(a(c(c(x1)))) -> c(c(c(c(a(a(x1))))))
     c(c(c(c(c(c(x1)))))) -> b(b(c(c(b(b(x1))))))
    weak:
     a(a(b(b(b(b(a(a(x1)))))))) -> a(a(c(c(a(a(b(b(x1))))))))
   Open