(ignored inputs)COMMENT TPDB SRS_Standard/Zantema_04/z069
Rewrite Rules:
   [ a(b(?x)) -> C(?x),
     b(c(?x)) -> A(?x),
     c(a(?x)) -> B(?x),
     A(C(?x)) -> b(?x),
     C(B(?x)) -> a(?x),
     B(A(?x)) -> c(?x),
     a(a(a(a(?x)))) -> A(A(A(?x))),
     A(A(A(A(?x)))) -> a(a(a(?x))),
     b(b(b(b(?x)))) -> B(B(B(?x))),
     B(B(B(B(?x)))) -> b(b(b(?x))),
     c(c(c(c(?x)))) -> C(C(C(?x))),
     C(C(C(C(?x)))) -> c(c(c(?x))),
     B(a(a(a(?x)))) -> c(A(A(A(?x)))),
     A(A(A(b(?x)))) -> a(a(a(C(?x)))),
     C(b(b(b(?x)))) -> a(B(B(B(?x)))),
     B(B(B(c(?x)))) -> b(b(b(A(?x)))),
     A(c(c(c(?x)))) -> b(C(C(C(?x)))),
     C(C(C(a(?x)))) -> c(c(c(B(?x)))),
     a(A(?x)) -> ?x,
     A(a(?x)) -> ?x,
     b(B(?x)) -> ?x,
     B(b(?x)) -> ?x,
     c(C(?x)) -> ?x,
     C(c(?x)) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ a(A(?x_1)) = C(c(?x_1)),
     a(B(B(B(?x_8)))) = C(b(b(b(?x_8)))),
     a(?x_20) = C(B(?x_20)),
     b(B(?x_2)) = A(a(?x_2)),
     b(C(C(C(?x_10)))) = A(c(c(c(?x_10)))),
     b(?x_22) = A(C(?x_22)),
     c(C(?x)) = B(b(?x)),
     c(A(A(A(?x_6)))) = B(a(a(a(?x_6)))),
     c(?x_18) = B(A(?x_18)),
     A(a(?x_4)) = b(B(?x_4)),
     A(c(c(c(?x_11)))) = b(C(C(C(?x_11)))),
     A(a(B(B(B(?x_14))))) = b(b(b(b(?x_14)))),
     A(c(c(c(B(?x_17))))) = b(C(C(a(?x_17)))),
     A(?x_23) = b(c(?x_23)),
     C(c(?x_5)) = a(A(?x_5)),
     C(b(b(b(?x_9)))) = a(B(B(B(?x_9)))),
     C(c(A(A(A(?x_12))))) = a(a(a(a(?x_12)))),
     C(b(b(b(A(?x_15))))) = a(B(B(c(?x_15)))),
     C(?x_21) = a(b(?x_21)),
     B(b(?x_3)) = c(C(?x_3)),
     B(a(a(a(?x_7)))) = c(A(A(A(?x_7)))),
     B(a(a(a(C(?x_13))))) = c(A(A(b(?x_13)))),
     B(b(C(C(C(?x_16))))) = c(c(c(c(?x_16)))),
     B(?x_19) = c(a(?x_19)),
     a(a(a(C(?x)))) = A(A(A(b(?x)))),
     a(a(a(?x_18))) = A(A(A(A(?x_18)))),
     A(A(A(b(?x_3)))) = a(a(a(C(?x_3)))),
     A(a(a(a(C(?x_13))))) = a(a(a(b(?x_13)))),
     A(A(a(a(a(C(?x_13)))))) = a(a(a(A(b(?x_13))))),
     A(A(A(a(a(a(C(?x_13))))))) = a(a(a(A(A(b(?x_13)))))),
     A(A(A(b(C(C(C(?x_16))))))) = a(a(a(c(c(c(?x_16)))))),
     A(A(A(?x_19))) = a(a(a(a(?x_19)))),
     b(b(b(A(?x_1)))) = B(B(B(c(?x_1)))),
     b(b(b(?x_20))) = B(B(B(B(?x_20)))),
     B(B(B(c(?x_5)))) = b(b(b(A(?x_5)))),
     B(B(B(c(A(A(A(?x_12))))))) = b(b(b(a(a(a(?x_12)))))),
     B(b(b(b(A(?x_15))))) = b(b(b(c(?x_15)))),
     B(B(b(b(b(A(?x_15)))))) = b(b(b(B(c(?x_15))))),
     B(B(B(b(b(b(A(?x_15))))))) = b(b(b(B(B(c(?x_15)))))),
     B(B(B(?x_21))) = b(b(b(b(?x_21)))),
     c(c(c(B(?x_2)))) = C(C(C(a(?x_2)))),
     c(c(c(?x_22))) = C(C(C(C(?x_22)))),
     C(C(C(a(?x_4)))) = c(c(c(B(?x_4)))),
     C(C(C(a(B(B(B(?x_14))))))) = c(c(c(b(b(b(?x_14)))))),
     C(c(c(c(B(?x_17))))) = c(c(c(a(?x_17)))),
     C(C(c(c(c(B(?x_17)))))) = c(c(c(C(a(?x_17))))),
     C(C(C(c(c(c(B(?x_17))))))) = c(c(c(C(C(a(?x_17)))))),
     C(C(C(?x_23))) = c(c(c(c(?x_23)))),
     B(a(a(C(?x)))) = c(A(A(A(b(?x))))),
     B(A(A(A(?x_6)))) = c(A(A(A(a(?x_6))))),
     B(a(A(A(A(?x_6))))) = c(A(A(A(a(a(?x_6)))))),
     B(a(a(A(A(A(?x_6)))))) = c(A(A(A(a(a(a(?x_6))))))),
     B(a(a(?x_18))) = c(A(A(A(A(?x_18))))),
     A(A(A(A(?x_1)))) = a(a(a(C(c(?x_1))))),
     A(A(A(B(B(B(?x_8)))))) = a(a(a(C(b(b(b(?x_8))))))),
     A(A(A(?x_20))) = a(a(a(C(B(?x_20))))),
     C(b(b(A(?x_1)))) = a(B(B(B(c(?x_1))))),
     C(B(B(B(?x_8)))) = a(B(B(B(b(?x_8))))),
     C(b(B(B(B(?x_8))))) = a(B(B(B(b(b(?x_8)))))),
     C(b(b(B(B(B(?x_8)))))) = a(B(B(B(b(b(b(?x_8))))))),
     C(b(b(?x_20))) = a(B(B(B(B(?x_20))))),
     B(B(B(B(?x_2)))) = b(b(b(A(a(?x_2))))),
     B(B(B(C(C(C(?x_10)))))) = b(b(b(A(c(c(c(?x_10))))))),
     B(B(B(?x_22))) = b(b(b(A(C(?x_22))))),
     A(c(c(B(?x_2)))) = b(C(C(C(a(?x_2))))),
     A(C(C(C(?x_10)))) = b(C(C(C(c(?x_10))))),
     A(c(C(C(C(?x_10))))) = b(C(C(C(c(c(?x_10)))))),
     A(c(c(C(C(C(?x_10)))))) = b(C(C(C(c(c(c(?x_10))))))),
     A(c(c(?x_22))) = b(C(C(C(C(?x_22))))),
     C(C(C(C(?x)))) = c(c(c(B(b(?x))))),
     C(C(C(A(A(A(?x_6)))))) = c(c(c(B(a(a(a(?x_6))))))),
     C(C(C(?x_18))) = c(c(c(B(A(?x_18))))),
     a(b(?x_3)) = C(?x_3),
     a(a(a(a(?x_7)))) = A(A(A(?x_7))),
     a(a(a(a(C(?x_13))))) = A(A(b(?x_13))),
     a(b(C(C(C(?x_16))))) = c(c(c(?x_16))),
     a(?x_19) = a(?x_19),
     A(C(?x)) = b(?x),
     A(A(A(A(?x_6)))) = a(a(a(?x_6))),
     A(?x_18) = A(?x_18),
     b(c(?x_5)) = A(?x_5),
     b(b(b(b(?x_9)))) = B(B(B(?x_9))),
     b(c(A(A(A(?x_12))))) = a(a(a(?x_12))),
     b(b(b(b(A(?x_15))))) = B(B(c(?x_15))),
     b(?x_21) = b(?x_21),
     B(A(?x_1)) = c(?x_1),
     B(B(B(B(?x_8)))) = b(b(b(?x_8))),
     B(?x_20) = B(?x_20),
     c(a(?x_4)) = B(?x_4),
     c(c(c(c(?x_11)))) = C(C(C(?x_11))),
     c(a(B(B(B(?x_14))))) = b(b(b(?x_14))),
     c(c(c(c(B(?x_17))))) = C(C(a(?x_17))),
     c(?x_23) = c(?x_23),
     C(B(?x_2)) = a(?x_2),
     C(C(C(C(?x_10)))) = c(c(c(?x_10))),
     C(?x_22) = C(?x_22),
     a(A(A(A(?x)))) = A(A(A(a(?x)))),
     a(a(A(A(A(?x))))) = A(A(A(a(a(?x))))),
     a(a(a(A(A(A(?x)))))) = A(A(A(a(a(a(?x)))))),
     A(a(a(a(?x)))) = a(a(a(A(?x)))),
     A(A(a(a(a(?x))))) = a(a(a(A(A(?x))))),
     A(A(A(a(a(a(?x)))))) = a(a(a(A(A(A(?x)))))),
     b(B(B(B(?x)))) = B(B(B(b(?x)))),
     b(b(B(B(B(?x))))) = B(B(B(b(b(?x))))),
     b(b(b(B(B(B(?x)))))) = B(B(B(b(b(b(?x)))))),
     B(b(b(b(?x)))) = b(b(b(B(?x)))),
     B(B(b(b(b(?x))))) = b(b(b(B(B(?x))))),
     B(B(B(b(b(b(?x)))))) = b(b(b(B(B(B(?x)))))),
     c(C(C(C(?x)))) = C(C(C(c(?x)))),
     c(c(C(C(C(?x))))) = C(C(C(c(c(?x))))),
     c(c(c(C(C(C(?x)))))) = C(C(C(c(c(c(?x)))))),
     C(c(c(c(?x)))) = c(c(c(C(?x)))),
     C(C(c(c(c(?x))))) = c(c(c(C(C(?x))))),
     C(C(C(c(c(c(?x)))))) = c(c(c(C(C(C(?x)))))) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
Terminating, WCR
Knuth & Bendix
Direct Methods: CR

Combined result: CR
962.trs: Success(CR)
YES
(97 msec.)