YES(?,O(n^1))

Problem:
 a(b(c(x1))) -> c(b(a(x1)))
 C(B(A(x1))) -> A(B(C(x1)))
 b(a(C(x1))) -> C(a(b(x1)))
 c(A(B(x1))) -> B(A(c(x1)))
 A(c(b(x1))) -> b(c(A(x1)))
 B(C(a(x1))) -> a(C(B(x1)))
 a(A(x1)) -> x1
 A(a(x1)) -> x1
 b(B(x1)) -> x1
 B(b(x1)) -> x1
 c(C(x1)) -> x1
 C(c(x1)) -> x1

Proof:
 Bounds Processor:
  bound: 0
  enrichment: match
  automaton:
   final states: {7,6,5,4,3,2}
   transitions:
    a0(1) -> 2*
    b0(1) -> 4*
    c0(1) -> 5*
    C0(1) -> 3*
    B0(1) -> 7*
    A0(1) -> 6*
    f120() -> 1*
  problem:
   
  Qed