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.001 [s] The number of normal forms that must be checked: 905 Time: 0.180 [s] Now checking all the pairs... Time to check pairs: 0.107 [s] The TRS has Uniqueness of Normal Forms. Total Time: 0.288 [s] problems/738.trs: Success(UNC) real 0.32 user 0.30 sys 0.00