NO
(ignored inputs)COMMENT from experiments for [44] submitted by: Tsubasa Suzuki , Takahito Aoto , and Yoshihito Toyama
input TRS:
   [ a(?x) -> g(h(b(?x))),
     a(?x) -> g(c(?x)),
     b(?x) -> g(b(?x)),
     g(a(?x)) -> g(h(a(?x))) ]
TRS:
   [ a(?x) -> g(h(b(?x))),
     a(?x) -> g(c(?x)),
     b(?x) -> g(b(?x)),
     g(a(?x)) -> g(h(a(?x))) ]
constructed TRS:
   [ a(?x) -> g(h(b(?x))),
     a(?x) -> g(c(?x)),
     b(?x) -> g(b(?x)),
     g(a(?x)) -> g(h(a(?x))),
     g(g(h(b(?x)))) -> g(h(g(c(?x)))),
     g(h(a(?x_1))) -> g(g(c(?x_1))),
     g(h(b(?x))) -> g(c(?x)) ]
convertible distinct normal forms: g(h(g(c(?x_1)))) = g(g(c(?x_1)))
UNC Completion (Development Closed)
problems/239.trs: Success(not UNC)
(0 msec.)