YES
(ignored inputs)COMMENT doi:10.1007/3-540-61064-2_39 [10] Example 2 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
Input:
   [ f(a,a) -> b,
     a -> a',
     f(a',?x) -> f(?x,?x),
     f(?x,a') -> f(?x,?x),
     f(a',a') -> b,
     b -> f(a',a') ]

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

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

CPNF:
   [ 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.013 [s]

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