NO
af/ONE-SORTED/543.trs
Input rules:
   [ f(c) -> g(c),
     g(c) -> f(c),
     c -> d ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ f(c) -> g(c),
     g(c) -> f(c),
     c -> d ]
Constructor pattern: [d,f(?x_1),g(?x_1)]
Defined pattern: [c]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
candidate for c:
   [ c -> d ]
Find a quasi-ordering ...
order successfully found
Precedence:
 c : Mul;
 d : Mul;
 g : Mul,  f : Mul;
Rules:
   [ c -> d ]
Conjectures:
   [ f(c) = g(c),
     g(c) = f(c) ]
STEP 0
ES:
   [ f(c) = g(c),
     g(c) = f(c) ]
HS:
   [ ]
ES0:
   [ f(d) = g(d),
     g(d) = f(d) ]
HS0:
   [ ]
ES1:
   [ f(d) = g(d),
     g(d) = f(d) ]
HS1:
   [ ]
No equation to expand
check Non-Ground-Confluence...
ground constructor terms for instantiation: {d,f(d),g(d)}
ground terms for instantiation: {d:o,f(d):o,g(d):o}
obtain 9 rules by 3 steps unfolding
obtain 12 candidates for checking non-joinability
check by TCAP-Approximation (success)
Witness for Non-Confluence: <f(d) <- g(c) -> g(d)>
: Success(not GCR)
(4 msec.)
0.02