YES (ignored inputs)COMMENT generated by FORT "UN & ~NFP" submitted by: Franziska Rapp input TRS: [ a -> a, f(b,a) -> f(a,b), f(?x,a) -> b ] TRS: [ a -> a, f(b,a) -> f(a,b), f(?x,a) -> b ] unknown Non-Omega-Overlapping unknown Right-Reducible Check distinct normal forms in critical pair closure...failed Obtained TRSs: [ a -> a, f(b,a) -> b, f(?x,a) -> b, f(a,b) -> b ] ...linear strongly closed TRS UNC Completion (General) problems/738.trs: Success(UNC) (4 msec.)