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]

CPNF:
   [ b … f(a'),
     a … a',
     b … b,
     c … c ]
Time: 0.000 [s]

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

proof:
     f(a')
->R^ f(a)
->R^ b

     b
Total Time: 0.000 [s]

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