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] CPNF: [ b … b, a … a ] 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.000 [s] problems/r12.trs: Success(UNC) real 0.01 user 0.00 sys 0.01