NO
(ignored inputs)COMMENT submitted by: Johannes Waldmann
input TRS:
   [ b(c(?x)) -> b(a(?x)),
     b(a(?x)) -> c(b(?x)),
     a(c(?x)) -> a(b(?x)),
     c(b(?x)) -> a(a(?x)),
     b(a(?x)) -> b(c(?x)),
     a(a(?x)) -> b(a(?x)) ]
TRS:
   [ b(c(?x)) -> b(a(?x)),
     b(a(?x)) -> c(b(?x)),
     a(c(?x)) -> a(b(?x)),
     c(b(?x)) -> a(a(?x)),
     b(a(?x)) -> b(c(?x)),
     a(a(?x)) -> b(a(?x)) ]
constructed TRS:
   [ b(c(?x)) -> b(a(?x)),
     b(a(?x)) -> c(b(?x)),
     a(c(?x)) -> a(b(?x)),
     c(b(?x)) -> a(a(?x)),
     b(a(?x)) -> b(c(?x)),
     a(a(?x)) -> b(a(?x)),
     b(a(a(?x_3))) -> b(a(b(?x_3))),
     b(a(b(?x_2))) -> c(b(c(?x_2))),
     b(c(?x_4)) -> c(b(?x_4)),
     b(b(a(?x_5))) -> c(b(a(?x_5))),
     a(a(a(?x_3))) -> a(b(b(?x_3))),
     c(b(a(?x))) -> a(a(c(?x))),
     c(c(b(?x_1))) -> a(a(a(?x_1))),
     c(b(c(?x_4))) -> a(a(a(?x_4))),
     c(b(?x_1)) -> b(c(?x_1)),
     b(a(b(?x_2))) -> b(c(c(?x_2))),
     b(b(a(?x_5))) -> b(c(a(?x_5))),
     a(b(a(?x))) -> b(a(a(?x))),
     c(b(c(?x_7))) -> c(b(b(?x_7))),
     b(a(b(b(?x_10)))) -> c(b(a(a(?x_10)))),
     b(c(c(?x_15))) -> c(b(b(?x_15))),
     a(b(c(?x_14))) -> a(b(b(?x_14))),
     c(b(a(b(?x_6)))) -> a(a(a(a(?x_6)))),
     c(c(b(c(?x_7)))) -> a(b(b(b(?x_7)))),
     c(c(b(?x_8))) -> a(a(c(?x_8))),
     c(c(b(a(?x_9)))) -> a(a(b(a(?x_9)))),
     a(a(c(?x_11))) -> a(b(b(?x_11))),
     c(b(c(c(?x_15)))) -> a(b(b(b(?x_15)))),
     c(b(c(a(?x_16)))) -> a(a(b(a(?x_16)))),
     b(a(b(?x_6))) -> b(c(a(?x_6))),
     c(b(c(?x_7))) -> b(c(b(?x_7))),
     b(a(b(b(?x_10)))) -> b(c(a(a(?x_10)))),
     b(c(c(?x_15))) -> b(c(b(?x_15))),
     b(a(a(?x_10))) -> a(b(b(?x_10))),
     a(b(a(a(?x_17)))) -> b(a(b(a(?x_17)))),
     b(a(a(b(?x_2)))) -> b(a(b(c(?x_2)))),
     b(a(b(b(?x_10)))) -> b(a(b(a(?x_10)))),
     b(a(a(b(b(?x_10))))) -> b(a(b(a(a(?x_10))))),
     b(a(b(a(?x)))) -> c(b(c(c(?x)))),
     b(a(c(b(?x_1)))) -> c(b(c(a(?x_1)))),
     b(a(b(c(?x_4)))) -> c(b(c(a(?x_4)))),
     b(a(b(a(b(?x_6))))) -> c(b(c(a(a(?x_6))))),
     b(a(c(b(c(?x))))) -> c(b(c(a(b(?x))))),
     b(a(c(b(?x_8)))) -> c(b(c(c(?x_8)))),
     b(a(b(c(c(?x_15))))) -> c(b(c(a(b(?x_15))))),
     b(a(a(?x_3))) -> c(b(b(?x_3))),
     b(a(a(c(?x_11)))) -> c(b(b(a(?x_11)))),
     b(a(a(a(?x_13)))) -> c(b(b(c(?x_13)))),
     b(c(b(?x_1))) -> c(b(a(?x_1))),
     b(b(c(?x_4))) -> c(b(a(?x_4))),
     b(b(b(a(?x_5)))) -> c(b(a(a(?x_5)))),
     b(c(b(c(?x_7)))) -> c(b(a(b(?x_7)))),
     b(b(c(c(?x_15)))) -> c(b(a(b(?x_15)))),
     b(b(b(a(a(?x_17))))) -> c(b(a(b(a(?x_17))))),
     a(b(b(c(?x_2)))) -> a(b(b(b(?x_2)))),
     a(b(a(?x_5))) -> a(b(b(?x_5))),
     a(a(b(a(?x_5)))) -> a(b(b(a(?x_5)))),
     a(a(b(b(?x)))) -> a(b(b(a(?x)))),
     a(b(b(a(a(?x))))) -> a(b(b(b(b(?x))))),
     a(a(b(a(a(?x_17))))) -> a(b(b(b(a(?x_17))))),
     c(b(a(b(?x_2)))) -> a(a(c(c(?x_2)))),
     c(b(a(b(?x_6)))) -> a(a(c(a(?x_6)))),
     c(c(b(c(?x_7)))) -> a(a(c(b(?x_7)))),
     c(b(a(b(b(?x_10))))) -> a(a(c(a(a(?x_10))))),
     b(c(a(?x_11))) -> a(a(c(?x_11))),
     c(b(c(c(?x_15)))) -> a(a(c(b(?x_15)))),
     c(b(b(a(a(?x_17))))) -> a(a(c(b(a(?x_17))))),
     c(c(b(a(?x)))) -> a(a(a(c(?x)))),
     c(c(c(b(?x_1)))) -> a(a(a(a(?x_1)))),
     c(a(a(?x_3))) -> a(b(b(?x_3))),
     c(c(b(c(?x_4)))) -> a(a(a(a(?x_4)))),
     c(c(b(a(b(?x_6))))) -> a(a(a(a(a(?x_6))))),
     c(c(c(b(c(?x_7))))) -> a(a(a(a(b(?x_7))))),
     c(c(c(b(?x_8)))) -> a(a(a(c(?x_8)))),
     c(c(c(b(a(?x_9))))) -> a(a(a(b(a(?x_9))))),
     c(a(a(c(?x_11)))) -> a(a(a(a(?x_11)))),
     a(a(a(c(?x_13)))) -> c(a(b(b(?x_13)))),
     c(c(b(c(c(?x_15))))) -> a(a(a(a(b(?x_15))))),
     c(c(b(c(a(?x_16))))) -> a(a(a(b(a(?x_16))))),
     c(b(a(a(?x_3)))) -> a(b(b(b(?x_3)))),
     c(b(a(a(c(?x_11))))) -> a(a(a(b(a(?x_11))))),
     c(b(a(a(a(?x))))) -> a(a(a(b(c(?x))))),
     b(c(c(?x_13))) -> a(b(b(?x_13))),
     c(b(b(c(?x_14)))) -> a(b(b(b(?x_14)))),
     c(c(b(?x_1))) -> b(c(a(?x_1))),
     c(b(a(b(?x_6)))) -> b(c(a(a(?x_6)))),
     c(c(b(c(?x_7)))) -> b(c(a(b(?x_7)))),
     c(c(b(a(?x_9)))) -> b(c(b(a(?x_9)))),
     c(b(c(c(?x_15)))) -> b(c(a(b(?x_15)))),
     c(b(c(a(?x_16)))) -> b(c(b(a(?x_16)))),
     b(a(b(a(?x)))) -> b(c(c(c(?x)))),
     b(a(c(b(?x_1)))) -> b(c(c(a(?x_1)))),
     b(a(b(c(?x_4)))) -> b(c(c(a(?x_4)))),
     b(a(b(a(b(?x_6))))) -> b(c(c(a(a(?x_6))))),
     b(a(c(b(c(?x_7))))) -> b(c(c(a(b(?x_7))))),
     b(a(c(b(?x_8)))) -> b(c(c(c(?x_8)))),
     b(a(b(c(c(?x))))) -> b(c(c(a(b(?x))))),
     b(b(a(a(?x_17)))) -> b(c(c(a(?x_17)))),
     b(b(c(?x_4))) -> b(c(a(?x_4))),
     b(b(a(b(?x_6)))) -> b(c(a(a(?x_6)))),
     b(c(b(c(?x_7)))) -> b(c(a(b(?x_7)))),
     b(b(c(c(?x_15)))) -> b(c(a(b(?x_15)))),
     a(b(c(?x_4))) -> b(a(a(?x_4))),
     a(b(b(a(?x_5)))) -> b(a(a(a(?x_5)))),
     a(b(a(b(?x_6)))) -> b(a(a(a(?x_6)))),
     a(c(b(c(?x_7)))) -> b(a(a(b(?x_7)))),
     a(b(c(c(?x_15)))) -> b(a(a(b(?x_15)))),
     a(b(b(a(a(?x))))) -> b(a(a(b(a(?x))))) ]
convertible distinct normal forms: c(a(b(b(?x_105)))) = a(b(b(b(?x_105))))
UNC Completion (Strongly Closed)
problems/991.trs: Success(not UNC)
(8860 msec.)