NO (ignored inputs)COMMENT doi:10.1145/322217.322230 [12] p. 811 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama input TRS: [ F(?x) -> A, F(?x) -> G(F(?x)), G(F(?x)) -> F(H(?x)), G(F(?x)) -> B ] TRS: [ F(?x) -> A, F(?x) -> G(F(?x)), G(F(?x)) -> F(H(?x)), G(F(?x)) -> B ] New rules by rule reversing: [ F(?x) -> A, G(F(?x)) -> F(?x), G(F(?x)) -> F(H(?x)), G(F(?x)) -> B ] constructed TRS: [ F(?x) -> A, G(F(?x)) -> F(?x), G(F(?x)) -> F(H(?x)), G(F(?x)) -> B ] convertible distinct normal forms: G(A) = B UNC Completion (Development Closed) problems/43.trs: Success(not UNC) (4 msec.)