NO
(ignored inputs)COMMENT TPDB SRS_Standard/Waldmann_07_size12/size-12-alpha-3-num-412
input TRS:
   [ a(?x) -> b(?x),
     b(b(c(?x))) -> c(a(c(a(a(?x))))),
     c(c(?x)) -> ?x ]
TRS:
   [ a(?x) -> b(?x),
     b(b(c(?x))) -> c(a(c(a(a(?x))))),
     c(c(?x)) -> ?x ]
constructed TRS:
   [ a(?x) -> b(?x),
     b(b(c(?x))) -> c(a(c(a(a(?x))))),
     c(c(?x)) -> ?x,
     c(a(c(a(a(c(?x_2)))))) -> b(b(?x_2)),
     c(a(c(a(a(a(c(a(a(c(?x_3)))))))))) -> b(b(b(b(?x_3)))),
     a(c(a(a(c(?x_3))))) -> c(b(b(?x_3))),
     c(b(c(a(a(c(?x_3)))))) -> b(b(?x_3)),
     c(a(c(b(a(c(?x_3)))))) -> b(b(?x_3)),
     c(a(c(a(b(c(?x_3)))))) -> b(b(?x_3)),
     b(b(a(c(a(a(c(?x))))))) -> c(b(c(b(b(b(b(?x))))))),
     b(c(a(a(c(?x_5))))) -> c(b(b(?x_5))),
     c(a(c(a(a(a(c(a(a(a(c(a(a(c(?x_4)))))))))))))) -> b(b(b(b(b(b(?x_4)))))),
     c(a(c(a(a(b(c(a(a(c(?x_6)))))))))) -> b(b(b(b(?x_6)))),
     c(a(c(a(a(a(c(b(a(c(?x_7)))))))))) -> b(b(b(b(?x_7)))),
     c(a(c(a(a(a(c(a(b(c(?x_8)))))))))) -> b(b(b(b(?x_8)))),
     a(c(a(a(a(c(a(a(c(?x_4))))))))) -> c(b(b(b(b(?x_4))))),
     a(c(b(a(c(?x_7))))) -> c(b(b(?x_7))),
     a(c(a(b(c(?x_8))))) -> c(b(b(?x_8))),
     c(a(c(a(a(b(b(?x))))))) -> c(b(c(b(b(b(b(?x))))))),
     b(b(a(c(a(a(a(c(a(a(c(?x_4))))))))))) -> c(b(c(b(b(b(b(b(b(?x_4))))))))),
     b(b(a(a(c(?x_5))))) -> c(b(c(b(c(b(b(?x_5))))))),
     b(b(b(c(a(a(c(?x_6))))))) -> c(b(c(b(b(b(b(?x_6))))))),
     b(b(a(c(b(a(c(?x_7))))))) -> c(b(c(b(b(b(b(?x_7))))))),
     b(b(a(c(a(b(c(?x_8))))))) -> c(b(c(b(b(b(b(?x_8))))))),
     c(b(c(a(a(a(c(a(a(c(?x_4)))))))))) -> b(b(b(b(?x_4)))),
     c(a(c(b(a(a(c(a(a(c(?x_4)))))))))) -> b(b(b(b(?x_4)))),
     c(a(c(a(b(a(c(a(a(c(?x_4)))))))))) -> b(b(b(b(?x_4)))),
     c(a(c(a(a(a(c(a(a(?x_2))))))))) -> b(b(b(b(c(?x_2))))),
     c(a(c(a(a(a(c(a(a(b(b(?x_3))))))))))) -> b(b(b(b(c(b(b(?x_3))))))),
     c(a(c(a(a(a(c(a(a(b(b(b(b(?x))))))))))))) -> b(b(b(b(a(c(a(a(c(b(b(?x))))))))))),
     c(a(c(a(a(a(c(a(c(b(b(?x_5))))))))))) -> b(b(b(b(a(a(c(?x_5))))))),
     c(a(c(a(a(a(c(a(a(b(b(?x_6))))))))))) -> b(b(b(b(b(c(a(a(c(?x_6))))))))),
     c(a(c(a(a(a(c(a(a(b(b(?x_7))))))))))) -> b(b(b(b(a(c(b(a(c(?x_7))))))))),
     c(a(c(a(a(a(c(a(a(b(b(?x_8))))))))))) -> b(b(b(b(a(c(a(b(c(?x_8))))))))),
     c(b(b(c(?x_2)))) -> b(c(b(b(?x_2)))),
     c(b(b(a(c(a(a(c(?x_3)))))))) -> b(c(b(b(b(b(?x_3)))))),
     c(b(b(a(c(a(a(a(c(a(a(c(?x_4)))))))))))) -> b(c(b(b(b(b(b(b(?x_4)))))))),
     c(b(b(a(a(c(?x)))))) -> b(c(b(c(b(b(?x)))))),
     c(b(b(b(c(a(a(c(?x_6)))))))) -> b(c(b(b(b(b(?x_6)))))),
     c(b(b(a(c(b(a(c(?x_7)))))))) -> b(c(b(b(b(b(?x_7)))))),
     c(b(b(a(c(a(b(c(?x_8)))))))) -> b(c(b(b(b(b(?x_8)))))),
     c(b(c(b(a(c(?x_6)))))) -> b(b(?x_6)),
     c(b(c(a(b(c(?x_6)))))) -> b(b(?x_6)),
     b(b(c(?x_2))) -> c(b(c(b(b(?x_2))))),
     c(b(c(a(a(b(b(?x_3))))))) -> c(b(c(b(b(b(b(?x_3))))))),
     c(a(c(b(b(c(?x_7)))))) -> b(b(?x_7)),
     c(a(c(b(a(b(b(?x_3))))))) -> c(b(c(b(b(b(b(?x_3))))))),
     c(a(c(a(b(b(b(?x_3))))))) -> c(b(c(b(b(b(b(?x_3))))))),
     c(b(c(b(b(b(b(c(?x_2)))))))) -> b(b(a(c(a(a(?x_2)))))),
     c(b(c(b(b(b(b(a(c(a(a(c(?x_3)))))))))))) -> b(b(a(c(a(a(b(b(?x_3)))))))),
     c(b(c(b(b(b(b(a(c(a(a(a(c(a(a(c(?x_4)))))))))))))))) -> b(b(a(c(a(a(b(b(b(b(?x_4)))))))))),
     b(b(c(b(b(?x_5))))) -> c(b(c(b(b(b(b(?x_5))))))),
     c(b(c(b(b(b(b(a(a(c(?x_5)))))))))) -> b(b(a(c(a(c(b(b(?x_5)))))))),
     c(b(c(b(b(b(b(b(c(a(a(c(?x_6)))))))))))) -> b(b(a(c(a(a(b(b(?x_6)))))))),
     c(b(c(b(b(b(b(a(c(b(a(c(?x_7)))))))))))) -> b(b(a(c(a(a(b(b(?x_7)))))))),
     c(b(c(b(b(b(b(a(c(a(b(c(?x_8)))))))))))) -> b(b(a(c(a(a(b(b(?x_8)))))))) ]
convertible distinct normal forms: c(b(c(b(b(b(b(b(b(?x_2))))))))) = b(b(b(b(b(?x_2)))))
UNC Completion (Strongly Closed)
problems/980.trs: Success(not UNC)
(20876 msec.)