YES
(ignored inputs)COMMENT doi:10.1109/LICS.2002.1029852 [25] Example 3 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
Input:
   [ f(a) -> f(f(a)),
     f(?x) -> f(a) ]

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

Make it Complete (R^):
   [ !cr_0 = f(?x_1),
     !cr_0 = f(!cr_0),
     !cr_0 = f(a),
     f(!cr_0) = f(?x_1),
     f(a) = f(!cr_0),
     f(?x) = f(?x_1),
     f(?x) = f(a) ]
Time: 0.001 [s]

The number of normal forms that must be checked: 3
Time: 0.000 [s]

Now checking all the pairs...

Time to check pairs: 0.000 [s]

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

problems/82.trs: Success(UNC)
real 0.02
user 0.01
sys 0.01