NO
(ignored inputs)COMMENT [120] Example 1 submitted by: Aart Middeldorp
input TRS:
   [ f(c) -> g(c),
     g(c) -> f(c),
     c -> d ]
TRS:
   [ f(c) -> g(c),
     g(c) -> f(c),
     c -> d ]
Check distinct normal forms in critical pair closure
convertible distinct normal forms: f(d) = g(d)
problems/543.trs: Success(not UNC)
(0 msec.)