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(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(c(?x_2))) -> c(b(c(b(b(?x_2))))),
     b(b(a(c(a(a(c(?x))))))) -> c(b(c(b(b(b(b(?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)))),
     c(a(c(a(a(a(c(a(a(a(c(a(a(c(?x_5)))))))))))))) -> b(b(b(b(b(b(?x_5)))))),
     c(a(c(a(a(b(c(a(a(c(?x_7)))))))))) -> b(b(b(b(?x_7)))),
     c(a(c(a(a(a(c(b(a(c(?x_8)))))))))) -> b(b(b(b(?x_8)))),
     c(a(c(a(a(a(c(a(b(c(?x_9)))))))))) -> b(b(b(b(?x_9)))),
     a(c(a(a(c(?x_3))))) -> c(b(b(?x_3))),
     a(c(a(a(a(c(a(a(c(?x_5))))))))) -> c(b(b(b(b(?x_5))))),
     b(c(a(a(c(?x_7))))) -> c(b(b(?x_7))),
     a(c(b(a(c(?x_8))))) -> c(b(b(?x_8))),
     a(c(a(b(c(?x_9))))) -> c(b(b(?x_9))),
     b(b(c(?x_2))) -> c(b(c(b(b(?x_2))))),
     c(a(c(a(a(b(b(?x_4))))))) -> c(b(c(b(b(b(b(?x_4))))))),
     b(b(a(c(a(a(a(c(a(a(c(?x_5))))))))))) -> c(b(c(b(b(b(b(b(b(?x_5))))))))),
     b(b(a(a(c(?x_6))))) -> c(b(c(b(c(b(b(?x_6))))))),
     b(b(b(c(a(a(c(?x_7))))))) -> c(b(c(b(b(b(b(?x_7))))))),
     b(b(a(c(b(a(c(?x_8))))))) -> c(b(c(b(b(b(b(?x_8))))))),
     b(b(a(c(a(b(c(?x_9))))))) -> c(b(c(b(b(b(b(?x_9))))))),
     c(b(c(a(a(a(c(a(a(c(?x_5)))))))))) -> b(b(b(b(?x_5)))),
     c(a(c(b(a(a(c(a(a(c(?x_5)))))))))) -> b(b(b(b(?x_5)))),
     c(a(c(a(b(a(c(a(a(c(?x_5)))))))))) -> b(b(b(b(?x_5)))),
     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(c(b(b(?x_6))))))))))) -> b(b(b(b(a(a(c(?x_6))))))),
     c(a(c(a(a(a(c(a(a(b(b(?x_7))))))))))) -> b(b(b(b(b(c(a(a(c(?x_7))))))))),
     c(a(c(a(a(a(c(a(a(b(b(?x_8))))))))))) -> b(b(b(b(a(c(b(a(c(?x_8))))))))),
     c(a(c(a(a(a(c(a(a(b(b(?x_9))))))))))) -> b(b(b(b(a(c(a(b(c(?x_9))))))))),
     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_5)))))))))))) -> b(c(b(b(b(b(b(b(?x_5)))))))),
     c(b(b(b(c(a(a(c(?x_7)))))))) -> b(c(b(b(b(b(?x_7)))))),
     c(b(b(a(c(b(a(c(?x_8)))))))) -> b(c(b(b(b(b(?x_8)))))),
     c(b(b(a(c(a(b(c(?x_9)))))))) -> b(c(b(b(b(b(?x_9)))))),
     c(b(c(b(a(c(?x_7)))))) -> b(b(?x_7)),
     c(b(c(a(b(c(?x_7)))))) -> b(b(?x_7)),
     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_8)))))) -> b(b(?x_8)),
     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(c(?x_2)))))) -> b(b(?x_2)),
     c(b(c(b(b(a(c(a(a(c(?x_3)))))))))) -> b(b(b(b(?x_3)))),
     c(b(c(b(b(a(c(a(a(a(c(a(a(c(?x_5)))))))))))))) -> b(b(b(b(b(b(?x_5)))))),
     c(b(c(b(b(b(c(a(a(c(?x_7)))))))))) -> b(b(b(b(?x_7)))),
     c(b(c(b(b(a(c(b(a(c(?x_8)))))))))) -> b(b(b(b(?x_8)))),
     c(b(c(b(b(a(c(a(b(c(?x_9)))))))))) -> b(b(b(b(?x_9)))),
     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_5)))))))))))))))) -> b(b(a(c(a(a(b(b(b(b(?x_5)))))))))),
     c(b(c(b(b(b(b(a(a(c(?x_6)))))))))) -> b(b(a(c(a(c(b(b(?x_6)))))))),
     c(b(c(b(b(b(b(b(c(a(a(c(?x_7)))))))))))) -> b(b(a(c(a(a(b(b(?x_7)))))))),
     c(b(c(b(b(b(b(a(c(b(a(c(?x_8)))))))))))) -> b(b(a(c(a(a(b(b(?x_8)))))))),
     c(b(c(b(b(b(b(a(c(a(b(c(?x_9)))))))))))) -> b(b(a(c(a(a(b(b(?x_9)))))))),
     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(b(b(a(a(c(?x)))))) -> b(c(b(c(b(b(?x)))))) ]
convertible distinct normal forms: c(b(b(b(b(b(b(b(b(?x_13))))))))) = b(b(b(b(b(b(b(?x_13)))))))
UNC Completion (Development Closed)
problems/980.trs: Success(not UNC)
(53612 msec.)