NO (ignored inputs)COMMENT submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama input TRS: [ I(?x) -> I(B(?x)), F(E(?x),?x) -> G(?x), E(?x) -> ?x ] TRS: [ I(?x) -> I(B(?x)), F(E(?x),?x) -> G(?x), E(?x) -> ?x ] Check distinct normal forms in critical pair closure convertible distinct normal forms: F(?x,?x) = G(?x) problems/98.trs: Success(not UNC) (0 msec.)