MAYBE (ignored inputs)COMMENT doi:10.1007/978-3-642-40885-4_22 [44] Example 8 submitted by: Tsubasa Suzuki , Takahito Aoto , and Yoshihito Toyama input TRS: [ a -> h(c), a -> h(f(c)), h(?x) -> h(h(?x)), f(?x) -> f(g(?x)) ] TRS: [ a -> h(c), a -> h(f(c)), h(?x) -> h(h(?x)), f(?x) -> f(g(?x)) ] New rules by rule reversing: [ a -> a, h(c) -> a, a -> a, h(f(c)) -> a, h(?x) -> h(?x), h(h(?x)) -> h(?x), f(?x) -> f(?x), f(g(?x)) -> f(?x) ] Check distinct normal forms in critical pair closure...failed problems/245.trs: Failure(unknown UNC) (4 msec.)