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(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))), b(a(b(?x_2))) -> b(c(c(?x_2))), b(b(a(?x_5))) -> b(c(a(?x_5))), a(a(b(?x_2))) -> b(a(c(?x_2))), a(b(a(?x))) -> b(a(a(?x))), c(b(?x_1)) -> b(c(?x_1)), b(a(a(c(?x_10)))) -> b(a(b(a(?x_10)))), b(a(a(a(?x_11)))) -> b(a(c(b(?x_11)))), b(a(a(a(?x_12)))) -> b(a(b(c(?x_12)))), b(b(c(?x_17))) -> b(a(b(?x_17))), b(a(b(b(?x_9)))) -> c(b(a(a(?x_9)))), b(b(a(c(?x_15)))) -> c(b(a(b(?x_15)))), b(b(a(a(?x_16)))) -> c(b(b(a(?x_16)))), a(a(a(c(?x_10)))) -> a(b(b(a(?x_10)))), a(a(a(a(?x_11)))) -> a(b(c(b(?x_11)))), a(a(a(a(?x_12)))) -> a(b(b(c(?x_12)))), a(b(c(?x_17))) -> a(b(b(?x_17))), 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(a(?x_8)))) -> a(a(b(a(?x_8)))), c(b(c(c(?x_13)))) -> a(b(b(b(?x_13)))), c(b(c(a(?x_14)))) -> a(a(b(a(?x_14)))), b(a(b(b(?x_9)))) -> b(c(a(a(?x_9)))), b(b(a(c(?x_15)))) -> b(c(a(b(?x_15)))), a(a(b(b(?x_9)))) -> b(a(a(a(?x_9)))), a(b(a(c(?x_15)))) -> b(a(a(b(?x_15)))), a(b(a(a(?x_16)))) -> b(a(b(a(?x_16)))), b(a(a(b(?x_2)))) -> b(a(b(c(?x_2)))), b(b(a(?x_5))) -> b(a(b(?x_5))), b(a(b(b(?x_9)))) -> b(a(b(a(?x_9)))), b(a(a(b(b(?x_9))))) -> b(a(b(a(a(?x_9))))), b(b(a(c(?x_15)))) -> b(a(b(b(?x_15)))), 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(b(c(c(?x_13))))) -> c(b(c(a(b(?x_13))))), b(a(b(c(a(?x_14))))) -> c(b(c(b(a(?x_14))))), b(b(a(a(?x_16)))) -> c(b(c(a(?x_16)))), b(c(b(?x_1))) -> c(b(a(?x_1))), b(b(a(b(?x_2)))) -> c(b(a(c(?x_2)))), b(b(c(?x_4))) -> c(b(a(?x_4))), b(b(b(a(?x_5)))) -> c(b(a(a(?x_5)))), b(b(a(b(?x_6)))) -> c(b(a(a(?x_6)))), b(c(b(c(?x_7)))) -> c(b(a(b(?x_7)))), b(b(a(b(b(?x_9))))) -> c(b(a(a(a(?x_9))))), b(b(c(c(?x_13)))) -> c(b(a(b(?x_13)))), b(b(b(a(c(?x_15))))) -> c(b(a(a(b(?x_15))))), b(b(b(a(a(?x_16))))) -> c(b(a(b(a(?x_16))))), 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(b(a(c(?x_15)))) -> a(b(b(b(?x_15)))), a(a(b(a(c(?x_15))))) -> a(b(b(a(b(?x_15))))), a(a(b(a(a(?x_16))))) -> a(b(b(b(a(?x_16))))), c(c(b(?x_1))) -> a(a(c(?x_1))), c(b(a(b(?x_2)))) -> a(a(c(c(?x_2)))), c(b(b(a(?x_5)))) -> a(a(c(a(?x_5)))), 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_9))))) -> a(a(c(a(a(?x_9))))), c(b(c(c(?x_13)))) -> a(a(c(b(?x_13)))), c(b(b(a(c(?x_15))))) -> a(a(c(a(b(?x_15))))), 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(a(?x_8))))) -> a(a(a(b(a(?x_8))))), c(a(a(c(?x_10)))) -> a(a(a(a(?x_10)))), a(a(a(c(?x_12)))) -> c(a(b(b(?x_12)))), c(c(b(c(c(?x_13))))) -> a(a(a(a(b(?x_13))))), c(c(b(c(a(?x_14))))) -> a(a(a(b(a(?x_14))))), c(b(a(a(?x_3)))) -> a(b(b(b(?x_3)))), c(b(a(a(c(?x_10))))) -> a(a(a(b(a(?x_10))))), c(b(a(a(a(?x_11))))) -> a(a(a(c(b(?x_11))))), c(b(b(c(?x_17)))) -> a(b(b(b(?x_17)))), 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(b(c(a(?x_14))))) -> b(c(c(b(a(?x_14))))), b(b(a(a(?x_16)))) -> b(c(c(a(?x_16)))), b(c(b(?x_1))) -> b(c(a(?x_1))), b(b(a(b(?x_2)))) -> b(c(a(c(?x_2)))), b(b(c(?x_4))) -> b(c(a(?x_4))), b(b(b(a(?x_5)))) -> b(c(a(a(?x_5)))), 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(a(b(b(?x_9))))) -> b(c(a(a(a(?x_9))))), b(b(c(c(?x_13)))) -> b(c(a(b(?x_13)))), b(b(b(a(c(?x_15))))) -> b(c(a(a(b(?x_15))))), b(b(b(a(a(?x_16))))) -> b(c(a(b(a(?x_16))))), a(a(b(a(?x)))) -> b(a(c(c(?x)))), a(a(c(b(?x_1)))) -> b(a(c(a(?x_1)))), a(a(b(c(?x_4)))) -> b(a(c(a(?x_4)))), a(a(b(a(b(?x_6))))) -> b(a(c(a(a(?x_6))))), a(a(c(b(c(?x_7))))) -> b(a(c(a(b(?x_7))))), a(a(b(c(c(?x_13))))) -> b(a(c(a(b(?x_13))))), a(a(b(c(a(?x_14))))) -> b(a(c(b(a(?x_14))))), a(b(a(a(?x_16)))) -> b(a(c(a(?x_16)))), b(a(a(?x_1))) -> a(b(b(?x_1))), a(b(a(b(?x_2)))) -> b(a(a(c(?x_2)))), 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(a(b(b(?x_9))))) -> b(a(a(a(a(?x_9))))), a(b(c(c(?x_13)))) -> b(a(a(b(?x_13)))), a(b(b(a(c(?x_15))))) -> b(a(a(a(b(?x_15))))), c(b(a(?x))) -> b(c(c(?x))), c(c(b(?x_1))) -> b(c(a(?x_1))), c(b(c(?x_4))) -> b(c(a(?x_4))), 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_8)))) -> b(c(b(a(?x_8)))), c(b(c(c(?x_13)))) -> b(c(a(b(?x_13)))), c(b(c(a(?x_14)))) -> b(c(b(a(?x_14)))), b(a(c(b(c(?x))))) -> c(b(c(a(b(?x))))), a(a(b(b(?x)))) -> a(b(b(a(?x)))), a(b(b(a(a(?x))))) -> a(b(b(b(b(?x))))), c(b(a(a(a(?x))))) -> a(a(a(b(c(?x))))), b(a(b(c(c(?x))))) -> b(c(c(a(b(?x))))), a(b(b(a(a(?x))))) -> b(a(a(b(a(?x))))), c(b(b(?x_7))) -> c(b(c(?x_7))), c(b(b(?x_13))) -> b(c(c(?x_13))), a(a(c(?x_10))) -> a(b(b(?x_10))), b(c(a(?x_6))) -> b(a(b(?x_6))), b(c(b(?x_7))) -> c(b(c(?x_7))), b(c(b(?x_13))) -> b(c(c(?x_13))), a(a(c(?x_10))) -> b(c(a(?x_10))), b(c(c(?x_12))) -> a(b(b(?x_12))) ] convertible distinct normal forms: c(c(a(b(b(?x_22))))) = a(b(b(b(b(?x_22))))) UNC Completion (Development Closed) problems/991.trs: Success(not UNC) (31892 msec.)