NO
(ignored inputs)COMMENT [120] Example 1 submitted by: Aart Middeldorp
Input:
   [ f(c) -> g(c),
     g(c) -> f(c),
     c -> d ]

Make it flat:
   [ f(c) -> g(c),
     g(c) -> f(c),
     c -> d ]
Time: 0.000 [s]

Make it Complete (R^):
   [ g(d) = f(c),
     g(d) = g(c),
     g(d) = f(d),
     f(d) = f(c),
     f(d) = g(c),
     f(c) = g(c),
     c = d ]
Time: 0.001 [s]

CPNF:
   [ c … d ]
Time: 0.000 [s]

Now checking all the pairs in CW...

Time to check pairs: 0.000 [s]

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

proof:
     g(d)
->R^ g(c)
->R^ f(c)

     f(d)
->R^ f(c)
Total Time: 0.001 [s]

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