NO
(ignored inputs)COMMENT doi:10.1007/11538363_37 [41] Example 1
Input:
   [ f(a) -> b,
     a -> a',
     f(b) -> c ]

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

Make it Complete (R^):
   [ f(a') = f(a),
     f(a') = b,
     f(a) = b,
     a = a',
     f(b) = c ]
Time: 0.000 [s]

The number of normal forms that must be checked: 21
Time: 0.002 [s]

Now checking all the pairs...

Time to check pairs: 0.001 [s]

The TRS doesn't have Uniqueness of Normal Forms.
Counter Example: 
     f(f(c))
<->* f(f(f(f(a'))))

proof:
     f(f(c))

     f(f(f(f(a'))))
->R^ f(f(f(f(a))))
->R^ f(f(f(b)))
->R^ f(f(c))
Total Time: 0.003 [s]

problems/225.trs: Success(not UNC)
real 0.04
user 0.01
sys 0.01