YES (ignored inputs)COMMENT generated by FORT "UN & ~NFP" submitted by: Franziska Rapp Input: [ a -> a, f(b,a) -> f(a,b), f(?x,a) -> b ] Make it flat: [ a -> a, f(b,a) -> f(a,b), f(?x,a) -> b ] Time: 0.000 [s] Make it Complete (R^): [ f(a,b) = b, f(b,a) = b, f(?x_1,a) = f(b,a), f(a,b) = f(?x_1,a), f(b,a) = f(a,b), f(?x,a) = f(?x_1,a), f(?x,a) = b ] Time: 0.002 [s] CPNF: [ b … b ] Time: 0.000 [s] Now checking all the pairs in CW... Time to check pairs: 0.000 [s] The TRS has Uniqueness of Normal Forms. Total Time: 0.002 [s] problems/738.trs: Success(UNC) real 0.02 user 0.02 sys 0.00