YES
(ignored inputs)COMMENT doi:10.1007/3-540-45744-5_49 [153] Example 14 submitted by: Raul Gutierrez and Salvador Lucas
Input:
   [ f(?x,?x) -> f(a,b) ]

Make it flat:
   [ f(?x,?x) -> f(a,b) ]
Time: 0.000 [s]

Make it Complete (R^):
   [ f(?x,?x) = f(?x_1,?x_1),
     f(?x,?x) = f(a,b) ]
Time: 0.000 [s]

The number of normal forms that must be checked: 1266
Time: 0.549 [s]

Now checking all the pairs...

Time to check pairs: 0.308 [s]

The TRS has Uniqueness of Normal Forms.
Total Time: 0.857 [s]

problems/801.trs: Success(UNC)
real 0.88
user 0.86
sys 0.02