YES

Problem:
 a(b(x1)) -> C(x1)
 b(c(x1)) -> A(x1)
 c(a(x1)) -> B(x1)
 A(C(x1)) -> b(x1)
 C(B(x1)) -> a(x1)
 B(A(x1)) -> c(x1)
 a(a(a(a(x1)))) -> A(A(A(x1)))
 A(A(A(A(x1)))) -> a(a(a(x1)))
 b(b(b(b(x1)))) -> B(B(B(x1)))
 B(B(B(B(x1)))) -> b(b(b(x1)))
 c(c(c(c(x1)))) -> C(C(C(x1)))
 C(C(C(C(x1)))) -> c(c(c(x1)))
 B(a(a(a(x1)))) -> c(A(A(A(x1))))
 A(A(A(b(x1)))) -> a(a(a(C(x1))))
 C(b(b(b(x1)))) -> a(B(B(B(x1))))
 B(B(B(c(x1)))) -> b(b(b(A(x1))))
 A(c(c(c(x1)))) -> b(C(C(C(x1))))
 C(C(C(a(x1)))) -> c(c(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:
 DP Processor:
  DPs:
   a#(b(x1)) -> C#(x1)
   b#(c(x1)) -> A#(x1)
   c#(a(x1)) -> B#(x1)
   A#(C(x1)) -> b#(x1)
   C#(B(x1)) -> a#(x1)
   B#(A(x1)) -> c#(x1)
   a#(a(a(a(x1)))) -> A#(x1)
   a#(a(a(a(x1)))) -> A#(A(x1))
   a#(a(a(a(x1)))) -> A#(A(A(x1)))
   A#(A(A(A(x1)))) -> a#(x1)
   A#(A(A(A(x1)))) -> a#(a(x1))
   A#(A(A(A(x1)))) -> a#(a(a(x1)))
   b#(b(b(b(x1)))) -> B#(x1)
   b#(b(b(b(x1)))) -> B#(B(x1))
   b#(b(b(b(x1)))) -> B#(B(B(x1)))
   B#(B(B(B(x1)))) -> b#(x1)
   B#(B(B(B(x1)))) -> b#(b(x1))
   B#(B(B(B(x1)))) -> b#(b(b(x1)))
   c#(c(c(c(x1)))) -> C#(x1)
   c#(c(c(c(x1)))) -> C#(C(x1))
   c#(c(c(c(x1)))) -> C#(C(C(x1)))
   C#(C(C(C(x1)))) -> c#(x1)
   C#(C(C(C(x1)))) -> c#(c(x1))
   C#(C(C(C(x1)))) -> c#(c(c(x1)))
   B#(a(a(a(x1)))) -> A#(x1)
   B#(a(a(a(x1)))) -> A#(A(x1))
   B#(a(a(a(x1)))) -> A#(A(A(x1)))
   B#(a(a(a(x1)))) -> c#(A(A(A(x1))))
   A#(A(A(b(x1)))) -> C#(x1)
   A#(A(A(b(x1)))) -> a#(C(x1))
   A#(A(A(b(x1)))) -> a#(a(C(x1)))
   A#(A(A(b(x1)))) -> a#(a(a(C(x1))))
   C#(b(b(b(x1)))) -> B#(x1)
   C#(b(b(b(x1)))) -> B#(B(x1))
   C#(b(b(b(x1)))) -> B#(B(B(x1)))
   C#(b(b(b(x1)))) -> a#(B(B(B(x1))))
   B#(B(B(c(x1)))) -> A#(x1)
   B#(B(B(c(x1)))) -> b#(A(x1))
   B#(B(B(c(x1)))) -> b#(b(A(x1)))
   B#(B(B(c(x1)))) -> b#(b(b(A(x1))))
   A#(c(c(c(x1)))) -> C#(x1)
   A#(c(c(c(x1)))) -> C#(C(x1))
   A#(c(c(c(x1)))) -> C#(C(C(x1)))
   A#(c(c(c(x1)))) -> b#(C(C(C(x1))))
   C#(C(C(a(x1)))) -> B#(x1)
   C#(C(C(a(x1)))) -> c#(B(x1))
   C#(C(C(a(x1)))) -> c#(c(B(x1)))
   C#(C(C(a(x1)))) -> c#(c(c(B(x1))))
  TRS:
   a(b(x1)) -> C(x1)
   b(c(x1)) -> A(x1)
   c(a(x1)) -> B(x1)
   A(C(x1)) -> b(x1)
   C(B(x1)) -> a(x1)
   B(A(x1)) -> c(x1)
   a(a(a(a(x1)))) -> A(A(A(x1)))
   A(A(A(A(x1)))) -> a(a(a(x1)))
   b(b(b(b(x1)))) -> B(B(B(x1)))
   B(B(B(B(x1)))) -> b(b(b(x1)))
   c(c(c(c(x1)))) -> C(C(C(x1)))
   C(C(C(C(x1)))) -> c(c(c(x1)))
   B(a(a(a(x1)))) -> c(A(A(A(x1))))
   A(A(A(b(x1)))) -> a(a(a(C(x1))))
   C(b(b(b(x1)))) -> a(B(B(B(x1))))
   B(B(B(c(x1)))) -> b(b(b(A(x1))))
   A(c(c(c(x1)))) -> b(C(C(C(x1))))
   C(C(C(a(x1)))) -> c(c(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
  TDG Processor:
   DPs:
    a#(b(x1)) -> C#(x1)
    b#(c(x1)) -> A#(x1)
    c#(a(x1)) -> B#(x1)
    A#(C(x1)) -> b#(x1)
    C#(B(x1)) -> a#(x1)
    B#(A(x1)) -> c#(x1)
    a#(a(a(a(x1)))) -> A#(x1)
    a#(a(a(a(x1)))) -> A#(A(x1))
    a#(a(a(a(x1)))) -> A#(A(A(x1)))
    A#(A(A(A(x1)))) -> a#(x1)
    A#(A(A(A(x1)))) -> a#(a(x1))
    A#(A(A(A(x1)))) -> a#(a(a(x1)))
    b#(b(b(b(x1)))) -> B#(x1)
    b#(b(b(b(x1)))) -> B#(B(x1))
    b#(b(b(b(x1)))) -> B#(B(B(x1)))
    B#(B(B(B(x1)))) -> b#(x1)
    B#(B(B(B(x1)))) -> b#(b(x1))
    B#(B(B(B(x1)))) -> b#(b(b(x1)))
    c#(c(c(c(x1)))) -> C#(x1)
    c#(c(c(c(x1)))) -> C#(C(x1))
    c#(c(c(c(x1)))) -> C#(C(C(x1)))
    C#(C(C(C(x1)))) -> c#(x1)
    C#(C(C(C(x1)))) -> c#(c(x1))
    C#(C(C(C(x1)))) -> c#(c(c(x1)))
    B#(a(a(a(x1)))) -> A#(x1)
    B#(a(a(a(x1)))) -> A#(A(x1))
    B#(a(a(a(x1)))) -> A#(A(A(x1)))
    B#(a(a(a(x1)))) -> c#(A(A(A(x1))))
    A#(A(A(b(x1)))) -> C#(x1)
    A#(A(A(b(x1)))) -> a#(C(x1))
    A#(A(A(b(x1)))) -> a#(a(C(x1)))
    A#(A(A(b(x1)))) -> a#(a(a(C(x1))))
    C#(b(b(b(x1)))) -> B#(x1)
    C#(b(b(b(x1)))) -> B#(B(x1))
    C#(b(b(b(x1)))) -> B#(B(B(x1)))
    C#(b(b(b(x1)))) -> a#(B(B(B(x1))))
    B#(B(B(c(x1)))) -> A#(x1)
    B#(B(B(c(x1)))) -> b#(A(x1))
    B#(B(B(c(x1)))) -> b#(b(A(x1)))
    B#(B(B(c(x1)))) -> b#(b(b(A(x1))))
    A#(c(c(c(x1)))) -> C#(x1)
    A#(c(c(c(x1)))) -> C#(C(x1))
    A#(c(c(c(x1)))) -> C#(C(C(x1)))
    A#(c(c(c(x1)))) -> b#(C(C(C(x1))))
    C#(C(C(a(x1)))) -> B#(x1)
    C#(C(C(a(x1)))) -> c#(B(x1))
    C#(C(C(a(x1)))) -> c#(c(B(x1)))
    C#(C(C(a(x1)))) -> c#(c(c(B(x1))))
   TRS:
    a(b(x1)) -> C(x1)
    b(c(x1)) -> A(x1)
    c(a(x1)) -> B(x1)
    A(C(x1)) -> b(x1)
    C(B(x1)) -> a(x1)
    B(A(x1)) -> c(x1)
    a(a(a(a(x1)))) -> A(A(A(x1)))
    A(A(A(A(x1)))) -> a(a(a(x1)))
    b(b(b(b(x1)))) -> B(B(B(x1)))
    B(B(B(B(x1)))) -> b(b(b(x1)))
    c(c(c(c(x1)))) -> C(C(C(x1)))
    C(C(C(C(x1)))) -> c(c(c(x1)))
    B(a(a(a(x1)))) -> c(A(A(A(x1))))
    A(A(A(b(x1)))) -> a(a(a(C(x1))))
    C(b(b(b(x1)))) -> a(B(B(B(x1))))
    B(B(B(c(x1)))) -> b(b(b(A(x1))))
    A(c(c(c(x1)))) -> b(C(C(C(x1))))
    C(C(C(a(x1)))) -> c(c(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
   graph:
    B#(B(B(B(x1)))) -> b#(b(b(x1))) ->
    b#(b(b(b(x1)))) -> B#(B(B(x1)))
    B#(B(B(B(x1)))) -> b#(b(b(x1))) -> b#(b(b(b(x1)))) -> B#(B(x1))
    B#(B(B(B(x1)))) -> b#(b(b(x1))) -> b#(b(b(b(x1)))) -> B#(x1)
    B#(B(B(B(x1)))) -> b#(b(b(x1))) -> b#(c(x1)) -> A#(x1)
    B#(B(B(B(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> B#(B(B(x1)))
    B#(B(B(B(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> B#(B(x1))
    B#(B(B(B(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> B#(x1)
    B#(B(B(B(x1)))) -> b#(b(x1)) -> b#(c(x1)) -> A#(x1)
    B#(B(B(B(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> B#(B(B(x1)))
    B#(B(B(B(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> B#(B(x1))
    B#(B(B(B(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> B#(x1)
    B#(B(B(B(x1)))) -> b#(x1) -> b#(c(x1)) -> A#(x1)
    B#(B(B(c(x1)))) -> A#(x1) -> A#(c(c(c(x1)))) -> b#(C(C(C(x1))))
    B#(B(B(c(x1)))) -> A#(x1) -> A#(c(c(c(x1)))) -> C#(C(C(x1)))
    B#(B(B(c(x1)))) -> A#(x1) -> A#(c(c(c(x1)))) -> C#(C(x1))
    B#(B(B(c(x1)))) -> A#(x1) -> A#(c(c(c(x1)))) -> C#(x1)
    B#(B(B(c(x1)))) -> A#(x1) -> A#(A(A(b(x1)))) -> a#(a(a(C(x1))))
    B#(B(B(c(x1)))) -> A#(x1) -> A#(A(A(b(x1)))) -> a#(a(C(x1)))
    B#(B(B(c(x1)))) -> A#(x1) -> A#(A(A(b(x1)))) -> a#(C(x1))
    B#(B(B(c(x1)))) -> A#(x1) -> A#(A(A(b(x1)))) -> C#(x1)
    B#(B(B(c(x1)))) -> A#(x1) -> A#(A(A(A(x1)))) -> a#(a(a(x1)))
    B#(B(B(c(x1)))) -> A#(x1) -> A#(A(A(A(x1)))) -> a#(a(x1))
    B#(B(B(c(x1)))) -> A#(x1) -> A#(A(A(A(x1)))) -> a#(x1)
    B#(B(B(c(x1)))) -> A#(x1) -> A#(C(x1)) -> b#(x1)
    B#(B(B(c(x1)))) -> b#(A(x1)) -> b#(b(b(b(x1)))) -> B#(B(B(x1)))
    B#(B(B(c(x1)))) -> b#(A(x1)) -> b#(b(b(b(x1)))) -> B#(B(x1))
    B#(B(B(c(x1)))) -> b#(A(x1)) -> b#(b(b(b(x1)))) -> B#(x1)
    B#(B(B(c(x1)))) -> b#(A(x1)) -> b#(c(x1)) -> A#(x1)
    B#(B(B(c(x1)))) -> b#(b(A(x1))) ->
    b#(b(b(b(x1)))) -> B#(B(B(x1)))
    B#(B(B(c(x1)))) -> b#(b(A(x1))) -> b#(b(b(b(x1)))) -> B#(B(x1))
    B#(B(B(c(x1)))) -> b#(b(A(x1))) -> b#(b(b(b(x1)))) -> B#(x1)
    B#(B(B(c(x1)))) -> b#(b(A(x1))) -> b#(c(x1)) -> A#(x1)
    B#(B(B(c(x1)))) -> b#(b(b(A(x1)))) ->
    b#(b(b(b(x1)))) -> B#(B(B(x1)))
    B#(B(B(c(x1)))) -> b#(b(b(A(x1)))) ->
    b#(b(b(b(x1)))) -> B#(B(x1))
    B#(B(B(c(x1)))) -> b#(b(b(A(x1)))) ->
    b#(b(b(b(x1)))) -> B#(x1)
    B#(B(B(c(x1)))) -> b#(b(b(A(x1)))) -> b#(c(x1)) -> A#(x1)
    B#(A(x1)) -> c#(x1) -> c#(c(c(c(x1)))) -> C#(C(C(x1)))
    B#(A(x1)) -> c#(x1) -> c#(c(c(c(x1)))) -> C#(C(x1))
    B#(A(x1)) -> c#(x1) -> c#(c(c(c(x1)))) -> C#(x1)
    B#(A(x1)) -> c#(x1) -> c#(a(x1)) -> B#(x1)
    B#(a(a(a(x1)))) -> c#(A(A(A(x1)))) ->
    c#(c(c(c(x1)))) -> C#(C(C(x1)))
    B#(a(a(a(x1)))) -> c#(A(A(A(x1)))) ->
    c#(c(c(c(x1)))) -> C#(C(x1))
    B#(a(a(a(x1)))) -> c#(A(A(A(x1)))) ->
    c#(c(c(c(x1)))) -> C#(x1)
    B#(a(a(a(x1)))) -> c#(A(A(A(x1)))) -> c#(a(x1)) -> B#(x1)
    B#(a(a(a(x1)))) -> A#(A(A(x1))) ->
    A#(c(c(c(x1)))) -> b#(C(C(C(x1))))
    B#(a(a(a(x1)))) -> A#(A(A(x1))) ->
    A#(c(c(c(x1)))) -> C#(C(C(x1)))
    B#(a(a(a(x1)))) -> A#(A(A(x1))) -> A#(c(c(c(x1)))) -> C#(C(x1))
    B#(a(a(a(x1)))) -> A#(A(A(x1))) -> A#(c(c(c(x1)))) -> C#(x1)
    B#(a(a(a(x1)))) -> A#(A(A(x1))) ->
    A#(A(A(b(x1)))) -> a#(a(a(C(x1))))
    B#(a(a(a(x1)))) -> A#(A(A(x1))) ->
    A#(A(A(b(x1)))) -> a#(a(C(x1)))
    B#(a(a(a(x1)))) -> A#(A(A(x1))) -> A#(A(A(b(x1)))) -> a#(C(x1))
    B#(a(a(a(x1)))) -> A#(A(A(x1))) -> A#(A(A(b(x1)))) -> C#(x1)
    B#(a(a(a(x1)))) -> A#(A(A(x1))) ->
    A#(A(A(A(x1)))) -> a#(a(a(x1)))
    B#(a(a(a(x1)))) -> A#(A(A(x1))) -> A#(A(A(A(x1)))) -> a#(a(x1))
    B#(a(a(a(x1)))) -> A#(A(A(x1))) -> A#(A(A(A(x1)))) -> a#(x1)
    B#(a(a(a(x1)))) -> A#(A(A(x1))) -> A#(C(x1)) -> b#(x1)
    B#(a(a(a(x1)))) -> A#(A(x1)) -> A#(c(c(c(x1)))) -> b#(C(C(C(x1))))
    B#(a(a(a(x1)))) -> A#(A(x1)) -> A#(c(c(c(x1)))) -> C#(C(C(x1)))
    B#(a(a(a(x1)))) -> A#(A(x1)) -> A#(c(c(c(x1)))) -> C#(C(x1))
    B#(a(a(a(x1)))) -> A#(A(x1)) -> A#(c(c(c(x1)))) -> C#(x1)
    B#(a(a(a(x1)))) -> A#(A(x1)) -> A#(A(A(b(x1)))) -> a#(a(a(C(x1))))
    B#(a(a(a(x1)))) -> A#(A(x1)) -> A#(A(A(b(x1)))) -> a#(a(C(x1)))
    B#(a(a(a(x1)))) -> A#(A(x1)) -> A#(A(A(b(x1)))) -> a#(C(x1))
    B#(a(a(a(x1)))) -> A#(A(x1)) -> A#(A(A(b(x1)))) -> C#(x1)
    B#(a(a(a(x1)))) -> A#(A(x1)) -> A#(A(A(A(x1)))) -> a#(a(a(x1)))
    B#(a(a(a(x1)))) -> A#(A(x1)) -> A#(A(A(A(x1)))) -> a#(a(x1))
    B#(a(a(a(x1)))) -> A#(A(x1)) -> A#(A(A(A(x1)))) -> a#(x1)
    B#(a(a(a(x1)))) -> A#(A(x1)) -> A#(C(x1)) -> b#(x1)
    B#(a(a(a(x1)))) -> A#(x1) -> A#(c(c(c(x1)))) -> b#(C(C(C(x1))))
    B#(a(a(a(x1)))) -> A#(x1) -> A#(c(c(c(x1)))) -> C#(C(C(x1)))
    B#(a(a(a(x1)))) -> A#(x1) -> A#(c(c(c(x1)))) -> C#(C(x1))
    B#(a(a(a(x1)))) -> A#(x1) -> A#(c(c(c(x1)))) -> C#(x1)
    B#(a(a(a(x1)))) -> A#(x1) -> A#(A(A(b(x1)))) -> a#(a(a(C(x1))))
    B#(a(a(a(x1)))) -> A#(x1) -> A#(A(A(b(x1)))) -> a#(a(C(x1)))
    B#(a(a(a(x1)))) -> A#(x1) -> A#(A(A(b(x1)))) -> a#(C(x1))
    B#(a(a(a(x1)))) -> A#(x1) -> A#(A(A(b(x1)))) -> C#(x1)
    B#(a(a(a(x1)))) -> A#(x1) -> A#(A(A(A(x1)))) -> a#(a(a(x1)))
    B#(a(a(a(x1)))) -> A#(x1) -> A#(A(A(A(x1)))) -> a#(a(x1))
    B#(a(a(a(x1)))) -> A#(x1) -> A#(A(A(A(x1)))) -> a#(x1)
    B#(a(a(a(x1)))) -> A#(x1) -> A#(C(x1)) -> b#(x1)
    c#(c(c(c(x1)))) -> C#(C(C(x1))) ->
    C#(C(C(a(x1)))) -> c#(c(c(B(x1))))
    c#(c(c(c(x1)))) -> C#(C(C(x1))) ->
    C#(C(C(a(x1)))) -> c#(c(B(x1)))
    c#(c(c(c(x1)))) -> C#(C(C(x1))) -> C#(C(C(a(x1)))) -> c#(B(x1))
    c#(c(c(c(x1)))) -> C#(C(C(x1))) -> C#(C(C(a(x1)))) -> B#(x1)
    c#(c(c(c(x1)))) -> C#(C(C(x1))) ->
    C#(b(b(b(x1)))) -> a#(B(B(B(x1))))
    c#(c(c(c(x1)))) -> C#(C(C(x1))) ->
    C#(b(b(b(x1)))) -> B#(B(B(x1)))
    c#(c(c(c(x1)))) -> C#(C(C(x1))) -> C#(b(b(b(x1)))) -> B#(B(x1))
    c#(c(c(c(x1)))) -> C#(C(C(x1))) -> C#(b(b(b(x1)))) -> B#(x1)
    c#(c(c(c(x1)))) -> C#(C(C(x1))) ->
    C#(C(C(C(x1)))) -> c#(c(c(x1)))
    c#(c(c(c(x1)))) -> C#(C(C(x1))) -> C#(C(C(C(x1)))) -> c#(c(x1))
    c#(c(c(c(x1)))) -> C#(C(C(x1))) -> C#(C(C(C(x1)))) -> c#(x1)
    c#(c(c(c(x1)))) -> C#(C(C(x1))) -> C#(B(x1)) -> a#(x1)
    c#(c(c(c(x1)))) -> C#(C(x1)) -> C#(C(C(a(x1)))) -> c#(c(c(B(x1))))
    c#(c(c(c(x1)))) -> C#(C(x1)) -> C#(C(C(a(x1)))) -> c#(c(B(x1)))
    c#(c(c(c(x1)))) -> C#(C(x1)) -> C#(C(C(a(x1)))) -> c#(B(x1))
    c#(c(c(c(x1)))) -> C#(C(x1)) -> C#(C(C(a(x1)))) -> B#(x1)
    c#(c(c(c(x1)))) -> C#(C(x1)) -> C#(b(b(b(x1)))) -> a#(B(B(B(x1))))
    c#(c(c(c(x1)))) -> C#(C(x1)) -> C#(b(b(b(x1)))) -> B#(B(B(x1)))
    c#(c(c(c(x1)))) -> C#(C(x1)) -> C#(b(b(b(x1)))) -> B#(B(x1))
    c#(c(c(c(x1)))) -> C#(C(x1)) -> C#(b(b(b(x1)))) -> B#(x1)
    c#(c(c(c(x1)))) -> C#(C(x1)) -> C#(C(C(C(x1)))) -> c#(c(c(x1)))
    c#(c(c(c(x1)))) -> C#(C(x1)) -> C#(C(C(C(x1)))) -> c#(c(x1))
    c#(c(c(c(x1)))) -> C#(C(x1)) -> C#(C(C(C(x1)))) -> c#(x1)
    c#(c(c(c(x1)))) -> C#(C(x1)) -> C#(B(x1)) -> a#(x1)
    c#(c(c(c(x1)))) -> C#(x1) -> C#(C(C(a(x1)))) -> c#(c(c(B(x1))))
    c#(c(c(c(x1)))) -> C#(x1) -> C#(C(C(a(x1)))) -> c#(c(B(x1)))
    c#(c(c(c(x1)))) -> C#(x1) -> C#(C(C(a(x1)))) -> c#(B(x1))
    c#(c(c(c(x1)))) -> C#(x1) -> C#(C(C(a(x1)))) -> B#(x1)
    c#(c(c(c(x1)))) -> C#(x1) -> C#(b(b(b(x1)))) -> a#(B(B(B(x1))))
    c#(c(c(c(x1)))) -> C#(x1) -> C#(b(b(b(x1)))) -> B#(B(B(x1)))
    c#(c(c(c(x1)))) -> C#(x1) -> C#(b(b(b(x1)))) -> B#(B(x1))
    c#(c(c(c(x1)))) -> C#(x1) -> C#(b(b(b(x1)))) -> B#(x1)
    c#(c(c(c(x1)))) -> C#(x1) -> C#(C(C(C(x1)))) -> c#(c(c(x1)))
    c#(c(c(c(x1)))) -> C#(x1) -> C#(C(C(C(x1)))) -> c#(c(x1))
    c#(c(c(c(x1)))) -> C#(x1) -> C#(C(C(C(x1)))) -> c#(x1)
    c#(c(c(c(x1)))) -> C#(x1) -> C#(B(x1)) -> a#(x1)
    c#(a(x1)) -> B#(x1) -> B#(B(B(c(x1)))) -> b#(b(b(A(x1))))
    c#(a(x1)) -> B#(x1) -> B#(B(B(c(x1)))) -> b#(b(A(x1)))
    c#(a(x1)) -> B#(x1) -> B#(B(B(c(x1)))) -> b#(A(x1))
    c#(a(x1)) -> B#(x1) -> B#(B(B(c(x1)))) -> A#(x1)
    c#(a(x1)) -> B#(x1) -> B#(a(a(a(x1)))) -> c#(A(A(A(x1))))
    c#(a(x1)) -> B#(x1) -> B#(a(a(a(x1)))) -> A#(A(A(x1)))
    c#(a(x1)) -> B#(x1) -> B#(a(a(a(x1)))) -> A#(A(x1))
    c#(a(x1)) -> B#(x1) -> B#(a(a(a(x1)))) -> A#(x1)
    c#(a(x1)) -> B#(x1) -> B#(B(B(B(x1)))) -> b#(b(b(x1)))
    c#(a(x1)) -> B#(x1) -> B#(B(B(B(x1)))) -> b#(b(x1))
    c#(a(x1)) -> B#(x1) -> B#(B(B(B(x1)))) -> b#(x1)
    c#(a(x1)) -> B#(x1) -> B#(A(x1)) -> c#(x1)
    A#(A(A(A(x1)))) -> a#(a(a(x1))) ->
    a#(a(a(a(x1)))) -> A#(A(A(x1)))
    A#(A(A(A(x1)))) -> a#(a(a(x1))) -> a#(a(a(a(x1)))) -> A#(A(x1))
    A#(A(A(A(x1)))) -> a#(a(a(x1))) -> a#(a(a(a(x1)))) -> A#(x1)
    A#(A(A(A(x1)))) -> a#(a(a(x1))) -> a#(b(x1)) -> C#(x1)
    A#(A(A(A(x1)))) -> a#(a(x1)) -> a#(a(a(a(x1)))) -> A#(A(A(x1)))
    A#(A(A(A(x1)))) -> a#(a(x1)) -> a#(a(a(a(x1)))) -> A#(A(x1))
    A#(A(A(A(x1)))) -> a#(a(x1)) -> a#(a(a(a(x1)))) -> A#(x1)
    A#(A(A(A(x1)))) -> a#(a(x1)) -> a#(b(x1)) -> C#(x1)
    A#(A(A(A(x1)))) -> a#(x1) -> a#(a(a(a(x1)))) -> A#(A(A(x1)))
    A#(A(A(A(x1)))) -> a#(x1) -> a#(a(a(a(x1)))) -> A#(A(x1))
    A#(A(A(A(x1)))) -> a#(x1) -> a#(a(a(a(x1)))) -> A#(x1)
    A#(A(A(A(x1)))) -> a#(x1) -> a#(b(x1)) -> C#(x1)
    A#(A(A(b(x1)))) -> C#(x1) -> C#(C(C(a(x1)))) -> c#(c(c(B(x1))))
    A#(A(A(b(x1)))) -> C#(x1) -> C#(C(C(a(x1)))) -> c#(c(B(x1)))
    A#(A(A(b(x1)))) -> C#(x1) -> C#(C(C(a(x1)))) -> c#(B(x1))
    A#(A(A(b(x1)))) -> C#(x1) -> C#(C(C(a(x1)))) -> B#(x1)
    A#(A(A(b(x1)))) -> C#(x1) -> C#(b(b(b(x1)))) -> a#(B(B(B(x1))))
    A#(A(A(b(x1)))) -> C#(x1) -> C#(b(b(b(x1)))) -> B#(B(B(x1)))
    A#(A(A(b(x1)))) -> C#(x1) -> C#(b(b(b(x1)))) -> B#(B(x1))
    A#(A(A(b(x1)))) -> C#(x1) -> C#(b(b(b(x1)))) -> B#(x1)
    A#(A(A(b(x1)))) -> C#(x1) -> C#(C(C(C(x1)))) -> c#(c(c(x1)))
    A#(A(A(b(x1)))) -> C#(x1) -> C#(C(C(C(x1)))) -> c#(c(x1))
    A#(A(A(b(x1)))) -> C#(x1) -> C#(C(C(C(x1)))) -> c#(x1)
    A#(A(A(b(x1)))) -> C#(x1) -> C#(B(x1)) -> a#(x1)
    A#(A(A(b(x1)))) -> a#(C(x1)) -> a#(a(a(a(x1)))) -> A#(A(A(x1)))
    A#(A(A(b(x1)))) -> a#(C(x1)) -> a#(a(a(a(x1)))) -> A#(A(x1))
    A#(A(A(b(x1)))) -> a#(C(x1)) -> a#(a(a(a(x1)))) -> A#(x1)
    A#(A(A(b(x1)))) -> a#(C(x1)) -> a#(b(x1)) -> C#(x1)
    A#(A(A(b(x1)))) -> a#(a(C(x1))) ->
    a#(a(a(a(x1)))) -> A#(A(A(x1)))
    A#(A(A(b(x1)))) -> a#(a(C(x1))) -> a#(a(a(a(x1)))) -> A#(A(x1))
    A#(A(A(b(x1)))) -> a#(a(C(x1))) -> a#(a(a(a(x1)))) -> A#(x1)
    A#(A(A(b(x1)))) -> a#(a(C(x1))) -> a#(b(x1)) -> C#(x1)
    A#(A(A(b(x1)))) -> a#(a(a(C(x1)))) ->
    a#(a(a(a(x1)))) -> A#(A(A(x1)))
    A#(A(A(b(x1)))) -> a#(a(a(C(x1)))) ->
    a#(a(a(a(x1)))) -> A#(A(x1))
    A#(A(A(b(x1)))) -> a#(a(a(C(x1)))) ->
    a#(a(a(a(x1)))) -> A#(x1)
    A#(A(A(b(x1)))) -> a#(a(a(C(x1)))) -> a#(b(x1)) -> C#(x1)
    A#(c(c(c(x1)))) -> b#(C(C(C(x1)))) ->
    b#(b(b(b(x1)))) -> B#(B(B(x1)))
    A#(c(c(c(x1)))) -> b#(C(C(C(x1)))) ->
    b#(b(b(b(x1)))) -> B#(B(x1))
    A#(c(c(c(x1)))) -> b#(C(C(C(x1)))) ->
    b#(b(b(b(x1)))) -> B#(x1)
    A#(c(c(c(x1)))) -> b#(C(C(C(x1)))) -> b#(c(x1)) -> A#(x1)
    A#(c(c(c(x1)))) -> C#(C(C(x1))) ->
    C#(C(C(a(x1)))) -> c#(c(c(B(x1))))
    A#(c(c(c(x1)))) -> C#(C(C(x1))) ->
    C#(C(C(a(x1)))) -> c#(c(B(x1)))
    A#(c(c(c(x1)))) -> C#(C(C(x1))) -> C#(C(C(a(x1)))) -> c#(B(x1))
    A#(c(c(c(x1)))) -> C#(C(C(x1))) -> C#(C(C(a(x1)))) -> B#(x1)
    A#(c(c(c(x1)))) -> C#(C(C(x1))) ->
    C#(b(b(b(x1)))) -> a#(B(B(B(x1))))
    A#(c(c(c(x1)))) -> C#(C(C(x1))) ->
    C#(b(b(b(x1)))) -> B#(B(B(x1)))
    A#(c(c(c(x1)))) -> C#(C(C(x1))) -> C#(b(b(b(x1)))) -> B#(B(x1))
    A#(c(c(c(x1)))) -> C#(C(C(x1))) -> C#(b(b(b(x1)))) -> B#(x1)
    A#(c(c(c(x1)))) -> C#(C(C(x1))) ->
    C#(C(C(C(x1)))) -> c#(c(c(x1)))
    A#(c(c(c(x1)))) -> C#(C(C(x1))) -> C#(C(C(C(x1)))) -> c#(c(x1))
    A#(c(c(c(x1)))) -> C#(C(C(x1))) -> C#(C(C(C(x1)))) -> c#(x1)
    A#(c(c(c(x1)))) -> C#(C(C(x1))) -> C#(B(x1)) -> a#(x1)
    A#(c(c(c(x1)))) -> C#(C(x1)) -> C#(C(C(a(x1)))) -> c#(c(c(B(x1))))
    A#(c(c(c(x1)))) -> C#(C(x1)) -> C#(C(C(a(x1)))) -> c#(c(B(x1)))
    A#(c(c(c(x1)))) -> C#(C(x1)) -> C#(C(C(a(x1)))) -> c#(B(x1))
    A#(c(c(c(x1)))) -> C#(C(x1)) -> C#(C(C(a(x1)))) -> B#(x1)
    A#(c(c(c(x1)))) -> C#(C(x1)) -> C#(b(b(b(x1)))) -> a#(B(B(B(x1))))
    A#(c(c(c(x1)))) -> C#(C(x1)) -> C#(b(b(b(x1)))) -> B#(B(B(x1)))
    A#(c(c(c(x1)))) -> C#(C(x1)) -> C#(b(b(b(x1)))) -> B#(B(x1))
    A#(c(c(c(x1)))) -> C#(C(x1)) -> C#(b(b(b(x1)))) -> B#(x1)
    A#(c(c(c(x1)))) -> C#(C(x1)) -> C#(C(C(C(x1)))) -> c#(c(c(x1)))
    A#(c(c(c(x1)))) -> C#(C(x1)) -> C#(C(C(C(x1)))) -> c#(c(x1))
    A#(c(c(c(x1)))) -> C#(C(x1)) -> C#(C(C(C(x1)))) -> c#(x1)
    A#(c(c(c(x1)))) -> C#(C(x1)) -> C#(B(x1)) -> a#(x1)
    A#(c(c(c(x1)))) -> C#(x1) -> C#(C(C(a(x1)))) -> c#(c(c(B(x1))))
    A#(c(c(c(x1)))) -> C#(x1) -> C#(C(C(a(x1)))) -> c#(c(B(x1)))
    A#(c(c(c(x1)))) -> C#(x1) -> C#(C(C(a(x1)))) -> c#(B(x1))
    A#(c(c(c(x1)))) -> C#(x1) -> C#(C(C(a(x1)))) -> B#(x1)
    A#(c(c(c(x1)))) -> C#(x1) -> C#(b(b(b(x1)))) -> a#(B(B(B(x1))))
    A#(c(c(c(x1)))) -> C#(x1) -> C#(b(b(b(x1)))) -> B#(B(B(x1)))
    A#(c(c(c(x1)))) -> C#(x1) -> C#(b(b(b(x1)))) -> B#(B(x1))
    A#(c(c(c(x1)))) -> C#(x1) -> C#(b(b(b(x1)))) -> B#(x1)
    A#(c(c(c(x1)))) -> C#(x1) -> C#(C(C(C(x1)))) -> c#(c(c(x1)))
    A#(c(c(c(x1)))) -> C#(x1) -> C#(C(C(C(x1)))) -> c#(c(x1))
    A#(c(c(c(x1)))) -> C#(x1) -> C#(C(C(C(x1)))) -> c#(x1)
    A#(c(c(c(x1)))) -> C#(x1) -> C#(B(x1)) -> a#(x1)
    A#(C(x1)) -> b#(x1) -> b#(b(b(b(x1)))) -> B#(B(B(x1)))
    A#(C(x1)) -> b#(x1) -> b#(b(b(b(x1)))) -> B#(B(x1))
    A#(C(x1)) -> b#(x1) -> b#(b(b(b(x1)))) -> B#(x1)
    A#(C(x1)) -> b#(x1) -> b#(c(x1)) -> A#(x1)
    b#(c(x1)) -> A#(x1) -> A#(c(c(c(x1)))) -> b#(C(C(C(x1))))
    b#(c(x1)) -> A#(x1) -> A#(c(c(c(x1)))) -> C#(C(C(x1)))
    b#(c(x1)) -> A#(x1) -> A#(c(c(c(x1)))) -> C#(C(x1))
    b#(c(x1)) -> A#(x1) -> A#(c(c(c(x1)))) -> C#(x1)
    b#(c(x1)) -> A#(x1) -> A#(A(A(b(x1)))) -> a#(a(a(C(x1))))
    b#(c(x1)) -> A#(x1) -> A#(A(A(b(x1)))) -> a#(a(C(x1)))
    b#(c(x1)) -> A#(x1) -> A#(A(A(b(x1)))) -> a#(C(x1))
    b#(c(x1)) -> A#(x1) -> A#(A(A(b(x1)))) -> C#(x1)
    b#(c(x1)) -> A#(x1) -> A#(A(A(A(x1)))) -> a#(a(a(x1)))
    b#(c(x1)) -> A#(x1) -> A#(A(A(A(x1)))) -> a#(a(x1))
    b#(c(x1)) -> A#(x1) -> A#(A(A(A(x1)))) -> a#(x1)
    b#(c(x1)) -> A#(x1) -> A#(C(x1)) -> b#(x1)
    b#(b(b(b(x1)))) -> B#(B(B(x1))) ->
    B#(B(B(c(x1)))) -> b#(b(b(A(x1))))
    b#(b(b(b(x1)))) -> B#(B(B(x1))) ->
    B#(B(B(c(x1)))) -> b#(b(A(x1)))
    b#(b(b(b(x1)))) -> B#(B(B(x1))) -> B#(B(B(c(x1)))) -> b#(A(x1))
    b#(b(b(b(x1)))) -> B#(B(B(x1))) -> B#(B(B(c(x1)))) -> A#(x1)
    b#(b(b(b(x1)))) -> B#(B(B(x1))) ->
    B#(a(a(a(x1)))) -> c#(A(A(A(x1))))
    b#(b(b(b(x1)))) -> B#(B(B(x1))) ->
    B#(a(a(a(x1)))) -> A#(A(A(x1)))
    b#(b(b(b(x1)))) -> B#(B(B(x1))) -> B#(a(a(a(x1)))) -> A#(A(x1))
    b#(b(b(b(x1)))) -> B#(B(B(x1))) -> B#(a(a(a(x1)))) -> A#(x1)
    b#(b(b(b(x1)))) -> B#(B(B(x1))) ->
    B#(B(B(B(x1)))) -> b#(b(b(x1)))
    b#(b(b(b(x1)))) -> B#(B(B(x1))) -> B#(B(B(B(x1)))) -> b#(b(x1))
    b#(b(b(b(x1)))) -> B#(B(B(x1))) -> B#(B(B(B(x1)))) -> b#(x1)
    b#(b(b(b(x1)))) -> B#(B(B(x1))) -> B#(A(x1)) -> c#(x1)
    b#(b(b(b(x1)))) -> B#(B(x1)) -> B#(B(B(c(x1)))) -> b#(b(b(A(x1))))
    b#(b(b(b(x1)))) -> B#(B(x1)) -> B#(B(B(c(x1)))) -> b#(b(A(x1)))
    b#(b(b(b(x1)))) -> B#(B(x1)) -> B#(B(B(c(x1)))) -> b#(A(x1))
    b#(b(b(b(x1)))) -> B#(B(x1)) -> B#(B(B(c(x1)))) -> A#(x1)
    b#(b(b(b(x1)))) -> B#(B(x1)) -> B#(a(a(a(x1)))) -> c#(A(A(A(x1))))
    b#(b(b(b(x1)))) -> B#(B(x1)) -> B#(a(a(a(x1)))) -> A#(A(A(x1)))
    b#(b(b(b(x1)))) -> B#(B(x1)) -> B#(a(a(a(x1)))) -> A#(A(x1))
    b#(b(b(b(x1)))) -> B#(B(x1)) -> B#(a(a(a(x1)))) -> A#(x1)
    b#(b(b(b(x1)))) -> B#(B(x1)) -> B#(B(B(B(x1)))) -> b#(b(b(x1)))
    b#(b(b(b(x1)))) -> B#(B(x1)) -> B#(B(B(B(x1)))) -> b#(b(x1))
    b#(b(b(b(x1)))) -> B#(B(x1)) -> B#(B(B(B(x1)))) -> b#(x1)
    b#(b(b(b(x1)))) -> B#(B(x1)) -> B#(A(x1)) -> c#(x1)
    b#(b(b(b(x1)))) -> B#(x1) -> B#(B(B(c(x1)))) -> b#(b(b(A(x1))))
    b#(b(b(b(x1)))) -> B#(x1) -> B#(B(B(c(x1)))) -> b#(b(A(x1)))
    b#(b(b(b(x1)))) -> B#(x1) -> B#(B(B(c(x1)))) -> b#(A(x1))
    b#(b(b(b(x1)))) -> B#(x1) -> B#(B(B(c(x1)))) -> A#(x1)
    b#(b(b(b(x1)))) -> B#(x1) -> B#(a(a(a(x1)))) -> c#(A(A(A(x1))))
    b#(b(b(b(x1)))) -> B#(x1) -> B#(a(a(a(x1)))) -> A#(A(A(x1)))
    b#(b(b(b(x1)))) -> B#(x1) -> B#(a(a(a(x1)))) -> A#(A(x1))
    b#(b(b(b(x1)))) -> B#(x1) -> B#(a(a(a(x1)))) -> A#(x1)
    b#(b(b(b(x1)))) -> B#(x1) -> B#(B(B(B(x1)))) -> b#(b(b(x1)))
    b#(b(b(b(x1)))) -> B#(x1) -> B#(B(B(B(x1)))) -> b#(b(x1))
    b#(b(b(b(x1)))) -> B#(x1) -> B#(B(B(B(x1)))) -> b#(x1)
    b#(b(b(b(x1)))) -> B#(x1) -> B#(A(x1)) -> c#(x1)
    C#(B(x1)) -> a#(x1) -> a#(a(a(a(x1)))) -> A#(A(A(x1)))
    C#(B(x1)) -> a#(x1) -> a#(a(a(a(x1)))) -> A#(A(x1))
    C#(B(x1)) -> a#(x1) -> a#(a(a(a(x1)))) -> A#(x1)
    C#(B(x1)) -> a#(x1) -> a#(b(x1)) -> C#(x1)
    C#(C(C(C(x1)))) -> c#(c(c(x1))) ->
    c#(c(c(c(x1)))) -> C#(C(C(x1)))
    C#(C(C(C(x1)))) -> c#(c(c(x1))) -> c#(c(c(c(x1)))) -> C#(C(x1))
    C#(C(C(C(x1)))) -> c#(c(c(x1))) -> c#(c(c(c(x1)))) -> C#(x1)
    C#(C(C(C(x1)))) -> c#(c(c(x1))) -> c#(a(x1)) -> B#(x1)
    C#(C(C(C(x1)))) -> c#(c(x1)) -> c#(c(c(c(x1)))) -> C#(C(C(x1)))
    C#(C(C(C(x1)))) -> c#(c(x1)) -> c#(c(c(c(x1)))) -> C#(C(x1))
    C#(C(C(C(x1)))) -> c#(c(x1)) -> c#(c(c(c(x1)))) -> C#(x1)
    C#(C(C(C(x1)))) -> c#(c(x1)) -> c#(a(x1)) -> B#(x1)
    C#(C(C(C(x1)))) -> c#(x1) -> c#(c(c(c(x1)))) -> C#(C(C(x1)))
    C#(C(C(C(x1)))) -> c#(x1) -> c#(c(c(c(x1)))) -> C#(C(x1))
    C#(C(C(C(x1)))) -> c#(x1) -> c#(c(c(c(x1)))) -> C#(x1)
    C#(C(C(C(x1)))) -> c#(x1) -> c#(a(x1)) -> B#(x1)
    C#(C(C(a(x1)))) -> B#(x1) -> B#(B(B(c(x1)))) -> b#(b(b(A(x1))))
    C#(C(C(a(x1)))) -> B#(x1) -> B#(B(B(c(x1)))) -> b#(b(A(x1)))
    C#(C(C(a(x1)))) -> B#(x1) -> B#(B(B(c(x1)))) -> b#(A(x1))
    C#(C(C(a(x1)))) -> B#(x1) -> B#(B(B(c(x1)))) -> A#(x1)
    C#(C(C(a(x1)))) -> B#(x1) -> B#(a(a(a(x1)))) -> c#(A(A(A(x1))))
    C#(C(C(a(x1)))) -> B#(x1) -> B#(a(a(a(x1)))) -> A#(A(A(x1)))
    C#(C(C(a(x1)))) -> B#(x1) -> B#(a(a(a(x1)))) -> A#(A(x1))
    C#(C(C(a(x1)))) -> B#(x1) -> B#(a(a(a(x1)))) -> A#(x1)
    C#(C(C(a(x1)))) -> B#(x1) -> B#(B(B(B(x1)))) -> b#(b(b(x1)))
    C#(C(C(a(x1)))) -> B#(x1) -> B#(B(B(B(x1)))) -> b#(b(x1))
    C#(C(C(a(x1)))) -> B#(x1) -> B#(B(B(B(x1)))) -> b#(x1)
    C#(C(C(a(x1)))) -> B#(x1) -> B#(A(x1)) -> c#(x1)
    C#(C(C(a(x1)))) -> c#(B(x1)) -> c#(c(c(c(x1)))) -> C#(C(C(x1)))
    C#(C(C(a(x1)))) -> c#(B(x1)) -> c#(c(c(c(x1)))) -> C#(C(x1))
    C#(C(C(a(x1)))) -> c#(B(x1)) -> c#(c(c(c(x1)))) -> C#(x1)
    C#(C(C(a(x1)))) -> c#(B(x1)) -> c#(a(x1)) -> B#(x1)
    C#(C(C(a(x1)))) -> c#(c(B(x1))) ->
    c#(c(c(c(x1)))) -> C#(C(C(x1)))
    C#(C(C(a(x1)))) -> c#(c(B(x1))) -> c#(c(c(c(x1)))) -> C#(C(x1))
    C#(C(C(a(x1)))) -> c#(c(B(x1))) -> c#(c(c(c(x1)))) -> C#(x1)
    C#(C(C(a(x1)))) -> c#(c(B(x1))) -> c#(a(x1)) -> B#(x1)
    C#(C(C(a(x1)))) -> c#(c(c(B(x1)))) ->
    c#(c(c(c(x1)))) -> C#(C(C(x1)))
    C#(C(C(a(x1)))) -> c#(c(c(B(x1)))) ->
    c#(c(c(c(x1)))) -> C#(C(x1))
    C#(C(C(a(x1)))) -> c#(c(c(B(x1)))) ->
    c#(c(c(c(x1)))) -> C#(x1)
    C#(C(C(a(x1)))) -> c#(c(c(B(x1)))) -> c#(a(x1)) -> B#(x1)
    C#(b(b(b(x1)))) -> B#(B(B(x1))) ->
    B#(B(B(c(x1)))) -> b#(b(b(A(x1))))
    C#(b(b(b(x1)))) -> B#(B(B(x1))) ->
    B#(B(B(c(x1)))) -> b#(b(A(x1)))
    C#(b(b(b(x1)))) -> B#(B(B(x1))) -> B#(B(B(c(x1)))) -> b#(A(x1))
    C#(b(b(b(x1)))) -> B#(B(B(x1))) -> B#(B(B(c(x1)))) -> A#(x1)
    C#(b(b(b(x1)))) -> B#(B(B(x1))) ->
    B#(a(a(a(x1)))) -> c#(A(A(A(x1))))
    C#(b(b(b(x1)))) -> B#(B(B(x1))) ->
    B#(a(a(a(x1)))) -> A#(A(A(x1)))
    C#(b(b(b(x1)))) -> B#(B(B(x1))) -> B#(a(a(a(x1)))) -> A#(A(x1))
    C#(b(b(b(x1)))) -> B#(B(B(x1))) -> B#(a(a(a(x1)))) -> A#(x1)
    C#(b(b(b(x1)))) -> B#(B(B(x1))) ->
    B#(B(B(B(x1)))) -> b#(b(b(x1)))
    C#(b(b(b(x1)))) -> B#(B(B(x1))) -> B#(B(B(B(x1)))) -> b#(b(x1))
    C#(b(b(b(x1)))) -> B#(B(B(x1))) -> B#(B(B(B(x1)))) -> b#(x1)
    C#(b(b(b(x1)))) -> B#(B(B(x1))) -> B#(A(x1)) -> c#(x1)
    C#(b(b(b(x1)))) -> B#(B(x1)) -> B#(B(B(c(x1)))) -> b#(b(b(A(x1))))
    C#(b(b(b(x1)))) -> B#(B(x1)) -> B#(B(B(c(x1)))) -> b#(b(A(x1)))
    C#(b(b(b(x1)))) -> B#(B(x1)) -> B#(B(B(c(x1)))) -> b#(A(x1))
    C#(b(b(b(x1)))) -> B#(B(x1)) -> B#(B(B(c(x1)))) -> A#(x1)
    C#(b(b(b(x1)))) -> B#(B(x1)) -> B#(a(a(a(x1)))) -> c#(A(A(A(x1))))
    C#(b(b(b(x1)))) -> B#(B(x1)) -> B#(a(a(a(x1)))) -> A#(A(A(x1)))
    C#(b(b(b(x1)))) -> B#(B(x1)) -> B#(a(a(a(x1)))) -> A#(A(x1))
    C#(b(b(b(x1)))) -> B#(B(x1)) -> B#(a(a(a(x1)))) -> A#(x1)
    C#(b(b(b(x1)))) -> B#(B(x1)) -> B#(B(B(B(x1)))) -> b#(b(b(x1)))
    C#(b(b(b(x1)))) -> B#(B(x1)) -> B#(B(B(B(x1)))) -> b#(b(x1))
    C#(b(b(b(x1)))) -> B#(B(x1)) -> B#(B(B(B(x1)))) -> b#(x1)
    C#(b(b(b(x1)))) -> B#(B(x1)) -> B#(A(x1)) -> c#(x1)
    C#(b(b(b(x1)))) -> B#(x1) -> B#(B(B(c(x1)))) -> b#(b(b(A(x1))))
    C#(b(b(b(x1)))) -> B#(x1) -> B#(B(B(c(x1)))) -> b#(b(A(x1)))
    C#(b(b(b(x1)))) -> B#(x1) -> B#(B(B(c(x1)))) -> b#(A(x1))
    C#(b(b(b(x1)))) -> B#(x1) -> B#(B(B(c(x1)))) -> A#(x1)
    C#(b(b(b(x1)))) -> B#(x1) -> B#(a(a(a(x1)))) -> c#(A(A(A(x1))))
    C#(b(b(b(x1)))) -> B#(x1) -> B#(a(a(a(x1)))) -> A#(A(A(x1)))
    C#(b(b(b(x1)))) -> B#(x1) -> B#(a(a(a(x1)))) -> A#(A(x1))
    C#(b(b(b(x1)))) -> B#(x1) -> B#(a(a(a(x1)))) -> A#(x1)
    C#(b(b(b(x1)))) -> B#(x1) -> B#(B(B(B(x1)))) -> b#(b(b(x1)))
    C#(b(b(b(x1)))) -> B#(x1) -> B#(B(B(B(x1)))) -> b#(b(x1))
    C#(b(b(b(x1)))) -> B#(x1) -> B#(B(B(B(x1)))) -> b#(x1)
    C#(b(b(b(x1)))) -> B#(x1) -> B#(A(x1)) -> c#(x1)
    C#(b(b(b(x1)))) -> a#(B(B(B(x1)))) ->
    a#(a(a(a(x1)))) -> A#(A(A(x1)))
    C#(b(b(b(x1)))) -> a#(B(B(B(x1)))) ->
    a#(a(a(a(x1)))) -> A#(A(x1))
    C#(b(b(b(x1)))) -> a#(B(B(B(x1)))) ->
    a#(a(a(a(x1)))) -> A#(x1)
    C#(b(b(b(x1)))) -> a#(B(B(B(x1)))) -> a#(b(x1)) -> C#(x1)
    a#(a(a(a(x1)))) -> A#(A(A(x1))) ->
    A#(c(c(c(x1)))) -> b#(C(C(C(x1))))
    a#(a(a(a(x1)))) -> A#(A(A(x1))) ->
    A#(c(c(c(x1)))) -> C#(C(C(x1)))
    a#(a(a(a(x1)))) -> A#(A(A(x1))) -> A#(c(c(c(x1)))) -> C#(C(x1))
    a#(a(a(a(x1)))) -> A#(A(A(x1))) -> A#(c(c(c(x1)))) -> C#(x1)
    a#(a(a(a(x1)))) -> A#(A(A(x1))) ->
    A#(A(A(b(x1)))) -> a#(a(a(C(x1))))
    a#(a(a(a(x1)))) -> A#(A(A(x1))) ->
    A#(A(A(b(x1)))) -> a#(a(C(x1)))
    a#(a(a(a(x1)))) -> A#(A(A(x1))) -> A#(A(A(b(x1)))) -> a#(C(x1))
    a#(a(a(a(x1)))) -> A#(A(A(x1))) -> A#(A(A(b(x1)))) -> C#(x1)
    a#(a(a(a(x1)))) -> A#(A(A(x1))) ->
    A#(A(A(A(x1)))) -> a#(a(a(x1)))
    a#(a(a(a(x1)))) -> A#(A(A(x1))) -> A#(A(A(A(x1)))) -> a#(a(x1))
    a#(a(a(a(x1)))) -> A#(A(A(x1))) -> A#(A(A(A(x1)))) -> a#(x1)
    a#(a(a(a(x1)))) -> A#(A(A(x1))) -> A#(C(x1)) -> b#(x1)
    a#(a(a(a(x1)))) -> A#(A(x1)) -> A#(c(c(c(x1)))) -> b#(C(C(C(x1))))
    a#(a(a(a(x1)))) -> A#(A(x1)) -> A#(c(c(c(x1)))) -> C#(C(C(x1)))
    a#(a(a(a(x1)))) -> A#(A(x1)) -> A#(c(c(c(x1)))) -> C#(C(x1))
    a#(a(a(a(x1)))) -> A#(A(x1)) -> A#(c(c(c(x1)))) -> C#(x1)
    a#(a(a(a(x1)))) -> A#(A(x1)) -> A#(A(A(b(x1)))) -> a#(a(a(C(x1))))
    a#(a(a(a(x1)))) -> A#(A(x1)) -> A#(A(A(b(x1)))) -> a#(a(C(x1)))
    a#(a(a(a(x1)))) -> A#(A(x1)) -> A#(A(A(b(x1)))) -> a#(C(x1))
    a#(a(a(a(x1)))) -> A#(A(x1)) -> A#(A(A(b(x1)))) -> C#(x1)
    a#(a(a(a(x1)))) -> A#(A(x1)) -> A#(A(A(A(x1)))) -> a#(a(a(x1)))
    a#(a(a(a(x1)))) -> A#(A(x1)) -> A#(A(A(A(x1)))) -> a#(a(x1))
    a#(a(a(a(x1)))) -> A#(A(x1)) -> A#(A(A(A(x1)))) -> a#(x1)
    a#(a(a(a(x1)))) -> A#(A(x1)) -> A#(C(x1)) -> b#(x1)
    a#(a(a(a(x1)))) -> A#(x1) -> A#(c(c(c(x1)))) -> b#(C(C(C(x1))))
    a#(a(a(a(x1)))) -> A#(x1) -> A#(c(c(c(x1)))) -> C#(C(C(x1)))
    a#(a(a(a(x1)))) -> A#(x1) -> A#(c(c(c(x1)))) -> C#(C(x1))
    a#(a(a(a(x1)))) -> A#(x1) -> A#(c(c(c(x1)))) -> C#(x1)
    a#(a(a(a(x1)))) -> A#(x1) -> A#(A(A(b(x1)))) -> a#(a(a(C(x1))))
    a#(a(a(a(x1)))) -> A#(x1) -> A#(A(A(b(x1)))) -> a#(a(C(x1)))
    a#(a(a(a(x1)))) -> A#(x1) -> A#(A(A(b(x1)))) -> a#(C(x1))
    a#(a(a(a(x1)))) -> A#(x1) -> A#(A(A(b(x1)))) -> C#(x1)
    a#(a(a(a(x1)))) -> A#(x1) -> A#(A(A(A(x1)))) -> a#(a(a(x1)))
    a#(a(a(a(x1)))) -> A#(x1) -> A#(A(A(A(x1)))) -> a#(a(x1))
    a#(a(a(a(x1)))) -> A#(x1) -> A#(A(A(A(x1)))) -> a#(x1)
    a#(a(a(a(x1)))) -> A#(x1) -> A#(C(x1)) -> b#(x1)
    a#(b(x1)) -> C#(x1) -> C#(C(C(a(x1)))) -> c#(c(c(B(x1))))
    a#(b(x1)) -> C#(x1) -> C#(C(C(a(x1)))) -> c#(c(B(x1)))
    a#(b(x1)) -> C#(x1) -> C#(C(C(a(x1)))) -> c#(B(x1))
    a#(b(x1)) -> C#(x1) -> C#(C(C(a(x1)))) -> B#(x1)
    a#(b(x1)) -> C#(x1) -> C#(b(b(b(x1)))) -> a#(B(B(B(x1))))
    a#(b(x1)) -> C#(x1) -> C#(b(b(b(x1)))) -> B#(B(B(x1)))
    a#(b(x1)) -> C#(x1) -> C#(b(b(b(x1)))) -> B#(B(x1))
    a#(b(x1)) -> C#(x1) -> C#(b(b(b(x1)))) -> B#(x1)
    a#(b(x1)) -> C#(x1) -> C#(C(C(C(x1)))) -> c#(c(c(x1)))
    a#(b(x1)) -> C#(x1) -> C#(C(C(C(x1)))) -> c#(c(x1))
    a#(b(x1)) -> C#(x1) -> C#(C(C(C(x1)))) -> c#(x1)
    a#(b(x1)) -> C#(x1) -> C#(B(x1)) -> a#(x1)
   KBO Processor:
    weight function:
     w0 = 1
     w(B#) = w(c#) = w(A#) = w(C#) = w(a#) = w(B) = w(A) = w(c) = w(C) = w(
     a) = w(b) = 1
     w(b#) = 0
    precedence:
     b# > C > A > B# > A# ~ C# ~ B > c# ~ a# ~ c ~ a ~ b
    problem:
     DPs:
      
     TRS:
      
    Qed