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