YES Input: [ f(?x,?x) -> g(?x), f(a,b) -> g(a) ] Make it flat: [ f(?x,?x) -> g(?x), f(a,b) -> g(a) ] Time: 0.000 [s] Make it Complete (R^): [ f(a,a) = g(a), f(a,a) = f(a,b), f(?x,?x) = g(?x), f(a,b) = g(a) ] Time: 0.000 [s] The number of normal forms that must be checked: 1686 Time: 0.561 [s] Now checking all the pairs... Time to check pairs: 0.338 [s] The TRS has Uniqueness of Normal Forms. Total Time: 0.900 [s] problems/r12.trs: Success(UNC) real 0.95 user 0.90 sys 0.01