NO (ignored inputs)COMMENT Cops #647 - #721: generated ground TRSs; evenly distributed in the UNR/UNC/NFP/CR hierarchy submitted by: Bertram Felgenhauer Input: [ h(a,c) -> b, c -> a, b -> f(b) ] Make it flat: [ h(a,c) -> b, c -> a, b -> f(b) ] Time: 0.000 [s] Make it Complete (R^): [ h(c,c) = b, h(a,a) = b, h(c,c) = f(b), h(c,a) = f(b), h(c,c) = h(a,a), h(c,c) = h(c,a), h(a,a) = h(c,a), h(c,c) = h(a,c), h(c,a) = b, h(c,a) = h(a,c), h(a,a) = h(a,c), h(a,a) = f(b), h(a,c) = f(b), h(a,c) = b, c = a, b = f(b) ] Time: 0.003 [s] CPNF: [ b … f(h(a,a)), b … h(a,a), a … a ] Time: 0.000 [s] The TRS doesn't have Uniqueness of Normal Forms. Counter Example: f(h(a,a)) <->* h(a,a) proof: f(h(a,a)) ->R^ f(f(b)) ->R^ f(b) ->R^ b h(a,a) ->R^ f(b) ->R^ b Total Time: 0.003 [s] problems/696.trs: Success(not UNC) real 0.02 user 0.01 sys 0.00