YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 4
  enrichment: match
  automaton:
   final states: {4}
   transitions:
    b3(107) -> 108*
    b3(87) -> 88*
    b3(109) -> 110*
    b3(85) -> 86*
    c3(86) -> 87*
    c3(110) -> 111*
    a4(127) -> 128*
    a4(122) -> 123*
    a4(126) -> 127*
    b4(123) -> 124*
    b4(125) -> 126*
    a0(4) -> 4*
    c4(124) -> 125*
    b0(4) -> 4*
    c0(4) -> 4*
    a1(20) -> 21*
    a1(47) -> 48*
    a1(19) -> 20*
    a1(11) -> 12*
    a1(13) -> 14*
    b1(12) -> 13*
    b1(14) -> 15*
    b1(43) -> 44*
    b1(18) -> 19*
    c1(15) -> 16*
    c1(17) -> 18*
    a2(75) -> 76*
    a2(60) -> 61*
    a2(79) -> 80*
    a2(69) -> 70*
    a2(54) -> 55*
    a2(49) -> 50*
    a2(26) -> 27*
    a2(53) -> 54*
    a2(28) -> 29*
    a2(80) -> 81*
    b2(50) -> 51*
    b2(102) -> 103*
    b2(52) -> 53*
    b2(27) -> 28*
    b2(29) -> 30*
    b2(76) -> 77*
    b2(78) -> 79*
    b2(58) -> 59*
    b2(100) -> 101*
    c2(30) -> 31*
    c2(77) -> 78*
    c2(51) -> 52*
    a3(89) -> 90*
    a3(84) -> 85*
    a3(106) -> 107*
    a3(108) -> 109*
    a3(88) -> 89*
    a3(120) -> 121*
    4 -> 11*
    13 -> 69,17
    14 -> 49,47
    16 -> 70,27,12,14,4
    19 -> 60*
    20 -> 43,26
    21 -> 12,4
    29 -> 84,75
    31 -> 70,27,29,12,4,11,14
    44 -> 13*
    48 -> 12*
    54 -> 58*
    55 -> 50,48,12
    59 -> 28*
    61 -> 27*
    70 -> 27*
    79 -> 106*
    80 -> 100*
    81 -> 102,4,48
    90 -> 85,76,50
    101 -> 28*
    103 -> 28*
    109 -> 122,120
    111 -> 29,75,84
    121 -> 85*
    128 -> 85*
  problem:
   
  Qed