YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 4
  enrichment: match
  automaton:
   final states: {4}
   transitions:
    a3(121) -> 122*
    a3(118) -> 119*
    b3(119) -> 120*
    c4(127) -> 128*
    c4(126) -> 127*
    b0(4) -> 4*
    c0(4) -> 4*
    a0(4) -> 4*
    a1(22) -> 23*
    a1(11) -> 12*
    a1(13) -> 14*
    c1(15) -> 16*
    c1(24) -> 25*
    c1(16) -> 17*
    c1(53) -> 54*
    b1(10) -> 11*
    b1(12) -> 13*
    b1(26) -> 27*
    b1(23) -> 24*
    a2(65) -> 66*
    a2(55) -> 56*
    a2(67) -> 68*
    a2(58) -> 59*
    c2(77) -> 78*
    c2(57) -> 58*
    c2(47) -> 48*
    c2(44) -> 45*
    c2(34) -> 35*
    c2(46) -> 47*
    c2(78) -> 79*
    c2(43) -> 44*
    c2(33) -> 34*
    b2(64) -> 65*
    b2(66) -> 67*
    b2(56) -> 57*
    b2(93) -> 94*
    b2(105) -> 106*
    c3(80) -> 81*
    c3(107) -> 108*
    c3(97) -> 98*
    c3(116) -> 117*
    c3(101) -> 102*
    c3(81) -> 82*
    c3(108) -> 109*
    c3(98) -> 99*
    c3(120) -> 121*
    c3(115) -> 116*
    c3(100) -> 101*
    4 -> 22,15,10
    10 -> 46*
    11 -> 53*
    12 -> 33*
    13 -> 64,55,26
    14 -> 23,11,4
    17 -> 4*
    23 -> 43*
    25 -> 13*
    26 -> 77*
    27 -> 11*
    35 -> 13*
    45 -> 24*
    48 -> 11*
    54 -> 13*
    56 -> 80*
    59 -> 12,33,23
    64 -> 100*
    66 -> 97*
    67 -> 118,93
    68 -> 105,65,27,11,53
    79 -> 27*
    82 -> 57*
    93 -> 107*
    94 -> 65*
    99 -> 67*
    102 -> 65*
    105 -> 115*
    106 -> 57*
    109 -> 94*
    117 -> 106*
    119 -> 126*
    122 -> 66,97
    128 -> 120*
  problem:
   
  Qed