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 ]
New rules by rule reversing:
   [ a(?x) -> b(?x),
     b(b(c(?x))) -> b(b(c(?x))),
     c(a(c(a(a(?x))))) -> b(b(c(?x))),
     c(c(?x)) -> ?x ]
constructed TRS:
   [ a(?x) -> b(?x),
     b(b(c(?x))) -> b(b(c(?x))),
     c(a(c(a(a(?x))))) -> b(b(c(?x))),
     c(c(?x)) -> ?x,
     b(b(b(b(c(?x_2))))) -> b(b(b(b(c(?x_2))))),
     b(b(c(c(?x_3)))) -> b(b(?x_3)),
     b(b(c(?x_2))) -> c(b(c(b(b(?x_2))))),
     c(b(b(c(?x_2)))) -> b(c(b(b(?x_2)))),
     b(b(b(b(c(?x_2))))) -> b(b(b(b(c(?x_2))))),
     b(b(c(c(?x_3)))) -> b(b(?x_3)),
     b(b(c(b(b(c(?x_7)))))) -> b(c(b(c(b(b(b(b(?x_7)))))))),
     b(b(c(?x_2))) -> c(b(c(b(b(?x_2))))),
     c(b(b(c(?x_2)))) -> b(c(b(b(?x_2)))),
     b(b(b(b(b(b(c(?x_2))))))) -> b(b(b(b(b(b(c(?x_2))))))),
     b(b(b(b(c(c(?x_3)))))) -> b(b(b(b(?x_3)))),
     b(b(c(b(c(b(b(?x_6))))))) -> b(b(b(b(c(?x_6))))),
     b(b(b(b(b(c(b(b(?x_7)))))))) -> b(b(b(b(c(b(b(c(?x_7)))))))),
     b(b(c(b(b(c(?x_2)))))) -> b(b(a(c(a(a(?x_2)))))),
     c(b(c(b(b(a(c(a(a(?x_2))))))))) -> b(b(b(b(c(?x_2))))),
     c(b(c(b(b(c(?x_3)))))) -> b(b(?x_3)),
     c(b(c(b(b(b(b(c(?x_7)))))))) -> b(c(b(c(b(b(b(b(?x_7)))))))),
     b(c(b(b(a(c(a(a(?x_2)))))))) -> c(b(b(b(b(c(?x_2)))))),
     b(c(b(b(c(?x_3))))) -> c(b(b(?x_3))),
     b(c(b(b(b(b(c(?x))))))) -> c(b(c(b(c(b(b(b(b(?x))))))))) ]
convertible distinct normal forms: b(c(b(b(b(b(?x_12)))))) = b(b(b(b(?x_12))))
UNC Completion (Development Closed)
problems/980.trs: Success(not UNC)
(276 msec.)