NO
(ignored inputs)COMMENT cops number: 543 submitted by: Aart Middeldorp [120] Example 1
input TRS:
   [ c : 0,
     d : 0,
     f : 1,
     g : 1 ]
   [ f(c) -> g(c),
     g(c) -> f(c),
     c -> d ]
unknown Strongly Non-Overlapping
unknown Right-Reducible
Call a UNC decision procedure for shallow TRSs...
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]

...Not UNC found by the decision procedure.
Check distinct normal forms in critical pair closure
distinct normal forms of a term: f(d) = g(d)
cops-gAY55SHB.trs: Success(not UNR)
(1 msec.)