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(a(x1))))) -> A(A(A(x1)))
 A(A(A(A(x1)))) -> a(a(a(a(x1))))
 b(b(b(b(b(x1))))) -> B(B(B(x1)))
 B(B(B(B(x1)))) -> b(b(b(b(x1))))
 c(c(c(c(c(x1))))) -> C(C(C(x1)))
 C(C(C(C(x1)))) -> c(c(c(c(x1))))
 B(a(a(a(a(x1))))) -> c(A(A(A(x1))))
 A(A(A(b(x1)))) -> a(a(a(a(C(x1)))))
 C(b(b(b(b(x1))))) -> a(B(B(B(x1))))
 B(B(B(c(x1)))) -> b(b(b(b(A(x1)))))
 A(c(c(c(c(x1))))) -> b(C(C(C(x1))))
 C(C(C(a(x1)))) -> c(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(a(x1))))) -> A#(x1)
   a#(a(a(a(a(x1))))) -> A#(A(x1))
   a#(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)))
   A#(A(A(A(x1)))) -> a#(a(a(a(x1))))
   b#(b(b(b(b(x1))))) -> B#(x1)
   b#(b(b(b(b(x1))))) -> B#(B(x1))
   b#(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)))
   B#(B(B(B(x1)))) -> b#(b(b(b(x1))))
   c#(c(c(c(c(x1))))) -> C#(x1)
   c#(c(c(c(c(x1))))) -> C#(C(x1))
   c#(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)))
   C#(C(C(C(x1)))) -> c#(c(c(c(x1))))
   B#(a(a(a(a(x1))))) -> A#(x1)
   B#(a(a(a(a(x1))))) -> A#(A(x1))
   B#(a(a(a(a(x1))))) -> A#(A(A(x1)))
   B#(a(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))))
   A#(A(A(b(x1)))) -> a#(a(a(a(C(x1)))))
   C#(b(b(b(b(x1))))) -> B#(x1)
   C#(b(b(b(b(x1))))) -> B#(B(x1))
   C#(b(b(b(b(x1))))) -> B#(B(B(x1)))
   C#(b(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))))
   B#(B(B(c(x1)))) -> b#(b(b(b(A(x1)))))
   A#(c(c(c(c(x1))))) -> C#(x1)
   A#(c(c(c(c(x1))))) -> C#(C(x1))
   A#(c(c(c(c(x1))))) -> C#(C(C(x1)))
   A#(c(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))))
   C#(C(C(a(x1)))) -> c#(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(a(x1))))) -> A(A(A(x1)))
   A(A(A(A(x1)))) -> a(a(a(a(x1))))
   b(b(b(b(b(x1))))) -> B(B(B(x1)))
   B(B(B(B(x1)))) -> b(b(b(b(x1))))
   c(c(c(c(c(x1))))) -> C(C(C(x1)))
   C(C(C(C(x1)))) -> c(c(c(c(x1))))
   B(a(a(a(a(x1))))) -> c(A(A(A(x1))))
   A(A(A(b(x1)))) -> a(a(a(a(C(x1)))))
   C(b(b(b(b(x1))))) -> a(B(B(B(x1))))
   B(B(B(c(x1)))) -> b(b(b(b(A(x1)))))
   A(c(c(c(c(x1))))) -> b(C(C(C(x1))))
   C(C(C(a(x1)))) -> c(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
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [B#](x0) = 2x0 + 7,
    
    [c#](x0) = 2x0 + 2,
    
    [A#](x0) = 2x0 + 8,
    
    [b#](x0) = 2x0 + 2,
    
    [C#](x0) = 2x0 + 8,
    
    [a#](x0) = 2x0 + 1,
    
    [B](x0) = x0 + 6,
    
    [A](x0) = x0 + 6,
    
    [c](x0) = x0 + 4,
    
    [C](x0) = x0 + 6,
    
    [a](x0) = x0 + 4,
    
    [b](x0) = x0 + 4
   orientation:
    a#(b(x1)) = 2x1 + 9 >= 2x1 + 8 = C#(x1)
    
    b#(c(x1)) = 2x1 + 10 >= 2x1 + 8 = A#(x1)
    
    c#(a(x1)) = 2x1 + 10 >= 2x1 + 7 = B#(x1)
    
    A#(C(x1)) = 2x1 + 20 >= 2x1 + 2 = b#(x1)
    
    C#(B(x1)) = 2x1 + 20 >= 2x1 + 1 = a#(x1)
    
    B#(A(x1)) = 2x1 + 19 >= 2x1 + 2 = c#(x1)
    
    a#(a(a(a(a(x1))))) = 2x1 + 33 >= 2x1 + 8 = A#(x1)
    
    a#(a(a(a(a(x1))))) = 2x1 + 33 >= 2x1 + 20 = A#(A(x1))
    
    a#(a(a(a(a(x1))))) = 2x1 + 33 >= 2x1 + 32 = A#(A(A(x1)))
    
    A#(A(A(A(x1)))) = 2x1 + 44 >= 2x1 + 1 = a#(x1)
    
    A#(A(A(A(x1)))) = 2x1 + 44 >= 2x1 + 9 = a#(a(x1))
    
    A#(A(A(A(x1)))) = 2x1 + 44 >= 2x1 + 17 = a#(a(a(x1)))
    
    A#(A(A(A(x1)))) = 2x1 + 44 >= 2x1 + 25 = a#(a(a(a(x1))))
    
    b#(b(b(b(b(x1))))) = 2x1 + 34 >= 2x1 + 7 = B#(x1)
    
    b#(b(b(b(b(x1))))) = 2x1 + 34 >= 2x1 + 19 = B#(B(x1))
    
    b#(b(b(b(b(x1))))) = 2x1 + 34 >= 2x1 + 31 = B#(B(B(x1)))
    
    B#(B(B(B(x1)))) = 2x1 + 43 >= 2x1 + 2 = b#(x1)
    
    B#(B(B(B(x1)))) = 2x1 + 43 >= 2x1 + 10 = b#(b(x1))
    
    B#(B(B(B(x1)))) = 2x1 + 43 >= 2x1 + 18 = b#(b(b(x1)))
    
    B#(B(B(B(x1)))) = 2x1 + 43 >= 2x1 + 26 = b#(b(b(b(x1))))
    
    c#(c(c(c(c(x1))))) = 2x1 + 34 >= 2x1 + 8 = C#(x1)
    
    c#(c(c(c(c(x1))))) = 2x1 + 34 >= 2x1 + 20 = C#(C(x1))
    
    c#(c(c(c(c(x1))))) = 2x1 + 34 >= 2x1 + 32 = C#(C(C(x1)))
    
    C#(C(C(C(x1)))) = 2x1 + 44 >= 2x1 + 2 = c#(x1)
    
    C#(C(C(C(x1)))) = 2x1 + 44 >= 2x1 + 10 = c#(c(x1))
    
    C#(C(C(C(x1)))) = 2x1 + 44 >= 2x1 + 18 = c#(c(c(x1)))
    
    C#(C(C(C(x1)))) = 2x1 + 44 >= 2x1 + 26 = c#(c(c(c(x1))))
    
    B#(a(a(a(a(x1))))) = 2x1 + 39 >= 2x1 + 8 = A#(x1)
    
    B#(a(a(a(a(x1))))) = 2x1 + 39 >= 2x1 + 20 = A#(A(x1))
    
    B#(a(a(a(a(x1))))) = 2x1 + 39 >= 2x1 + 32 = A#(A(A(x1)))
    
    B#(a(a(a(a(x1))))) = 2x1 + 39 >= 2x1 + 38 = c#(A(A(A(x1))))
    
    A#(A(A(b(x1)))) = 2x1 + 40 >= 2x1 + 8 = C#(x1)
    
    A#(A(A(b(x1)))) = 2x1 + 40 >= 2x1 + 13 = a#(C(x1))
    
    A#(A(A(b(x1)))) = 2x1 + 40 >= 2x1 + 21 = a#(a(C(x1)))
    
    A#(A(A(b(x1)))) = 2x1 + 40 >= 2x1 + 29 = a#(a(a(C(x1))))
    
    A#(A(A(b(x1)))) = 2x1 + 40 >= 2x1 + 37 = a#(a(a(a(C(x1)))))
    
    C#(b(b(b(b(x1))))) = 2x1 + 40 >= 2x1 + 7 = B#(x1)
    
    C#(b(b(b(b(x1))))) = 2x1 + 40 >= 2x1 + 19 = B#(B(x1))
    
    C#(b(b(b(b(x1))))) = 2x1 + 40 >= 2x1 + 31 = B#(B(B(x1)))
    
    C#(b(b(b(b(x1))))) = 2x1 + 40 >= 2x1 + 37 = a#(B(B(B(x1))))
    
    B#(B(B(c(x1)))) = 2x1 + 39 >= 2x1 + 8 = A#(x1)
    
    B#(B(B(c(x1)))) = 2x1 + 39 >= 2x1 + 14 = b#(A(x1))
    
    B#(B(B(c(x1)))) = 2x1 + 39 >= 2x1 + 22 = b#(b(A(x1)))
    
    B#(B(B(c(x1)))) = 2x1 + 39 >= 2x1 + 30 = b#(b(b(A(x1))))
    
    B#(B(B(c(x1)))) = 2x1 + 39 >= 2x1 + 38 = b#(b(b(b(A(x1)))))
    
    A#(c(c(c(c(x1))))) = 2x1 + 40 >= 2x1 + 8 = C#(x1)
    
    A#(c(c(c(c(x1))))) = 2x1 + 40 >= 2x1 + 20 = C#(C(x1))
    
    A#(c(c(c(c(x1))))) = 2x1 + 40 >= 2x1 + 32 = C#(C(C(x1)))
    
    A#(c(c(c(c(x1))))) = 2x1 + 40 >= 2x1 + 38 = b#(C(C(C(x1))))
    
    C#(C(C(a(x1)))) = 2x1 + 40 >= 2x1 + 7 = B#(x1)
    
    C#(C(C(a(x1)))) = 2x1 + 40 >= 2x1 + 14 = c#(B(x1))
    
    C#(C(C(a(x1)))) = 2x1 + 40 >= 2x1 + 22 = c#(c(B(x1)))
    
    C#(C(C(a(x1)))) = 2x1 + 40 >= 2x1 + 30 = c#(c(c(B(x1))))
    
    C#(C(C(a(x1)))) = 2x1 + 40 >= 2x1 + 38 = c#(c(c(c(B(x1)))))
    
    a(b(x1)) = x1 + 8 >= x1 + 6 = C(x1)
    
    b(c(x1)) = x1 + 8 >= x1 + 6 = A(x1)
    
    c(a(x1)) = x1 + 8 >= x1 + 6 = B(x1)
    
    A(C(x1)) = x1 + 12 >= x1 + 4 = b(x1)
    
    C(B(x1)) = x1 + 12 >= x1 + 4 = a(x1)
    
    B(A(x1)) = x1 + 12 >= x1 + 4 = c(x1)
    
    a(a(a(a(a(x1))))) = x1 + 20 >= x1 + 18 = A(A(A(x1)))
    
    A(A(A(A(x1)))) = x1 + 24 >= x1 + 16 = a(a(a(a(x1))))
    
    b(b(b(b(b(x1))))) = x1 + 20 >= x1 + 18 = B(B(B(x1)))
    
    B(B(B(B(x1)))) = x1 + 24 >= x1 + 16 = b(b(b(b(x1))))
    
    c(c(c(c(c(x1))))) = x1 + 20 >= x1 + 18 = C(C(C(x1)))
    
    C(C(C(C(x1)))) = x1 + 24 >= x1 + 16 = c(c(c(c(x1))))
    
    B(a(a(a(a(x1))))) = x1 + 22 >= x1 + 22 = c(A(A(A(x1))))
    
    A(A(A(b(x1)))) = x1 + 22 >= x1 + 22 = a(a(a(a(C(x1)))))
    
    C(b(b(b(b(x1))))) = x1 + 22 >= x1 + 22 = a(B(B(B(x1))))
    
    B(B(B(c(x1)))) = x1 + 22 >= x1 + 22 = b(b(b(b(A(x1)))))
    
    A(c(c(c(c(x1))))) = x1 + 22 >= x1 + 22 = b(C(C(C(x1))))
    
    C(C(C(a(x1)))) = x1 + 22 >= x1 + 22 = c(c(c(c(B(x1)))))
    
    a(A(x1)) = x1 + 10 >= x1 = x1
    
    A(a(x1)) = x1 + 10 >= x1 = x1
    
    b(B(x1)) = x1 + 10 >= x1 = x1
    
    B(b(x1)) = x1 + 10 >= x1 = x1
    
    c(C(x1)) = x1 + 10 >= x1 = x1
    
    C(c(x1)) = x1 + 10 >= x1 = x1
   problem:
    DPs:
     
    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(a(x1))))) -> A(A(A(x1)))
     A(A(A(A(x1)))) -> a(a(a(a(x1))))
     b(b(b(b(b(x1))))) -> B(B(B(x1)))
     B(B(B(B(x1)))) -> b(b(b(b(x1))))
     c(c(c(c(c(x1))))) -> C(C(C(x1)))
     C(C(C(C(x1)))) -> c(c(c(c(x1))))
     B(a(a(a(a(x1))))) -> c(A(A(A(x1))))
     A(A(A(b(x1)))) -> a(a(a(a(C(x1)))))
     C(b(b(b(b(x1))))) -> a(B(B(B(x1))))
     B(B(B(c(x1)))) -> b(b(b(b(A(x1)))))
     A(c(c(c(c(x1))))) -> b(C(C(C(x1))))
     C(C(C(a(x1)))) -> c(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
   Qed