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(b,a) -> a, a -> c, h(c,c) -> a, f(b) -> c ] Make it flat: [ h(b,a) -> a, a -> c, h(c,c) -> a, f(b) -> c ] Time: 0.000 [s] Make it Complete (R^): [ c = h(b,a), h(b,c) = a, h(b,a) = h(c,c), h(b,a) = h(a,a), h(b,a) = h(a,c), h(b,a) = h(c,a), h(b,c) = c, h(b,c) = h(c,c), h(b,c) = h(a,c), h(b,c) = h(a,a), h(b,c) = h(c,a), h(b,c) = h(b,a), h(b,c) = f(b), h(b,a) = f(b), h(b,a) = a, a = f(b), h(c,a) = a, h(a,c) = a, h(c,a) = c, h(a,c) = c, h(c,a) = f(b), h(a,a) = f(b), h(c,a) = h(a,c), h(c,a) = h(a,a), h(a,c) = h(a,a), h(c,a) = h(c,c), h(a,a) = a, h(a,a) = c, h(a,a) = h(c,c), h(a,c) = h(c,c), h(a,c) = f(b), h(c,c) = f(b), c = h(c,c), a = c, h(c,c) = a, f(b) = c ] Time: 0.014 [s] CPNF: [ a … h(b,c), b … b, a … c ] Time: 0.000 [s] The TRS doesn't have Uniqueness of Normal Forms. Counter Example: h(b,c) <->* c proof: h(b,c) ->R^ h(b,a) ->R^ a c ->R^ a Total Time: 0.015 [s] problems/702.trs: Success(not UNC) real 0.03 user 0.02 sys 0.00