NO (ignored inputs)COMMENT Cops #647 - #721: generated ground TRSs; evenly distributed in the UNR/UNC/NFP/CR hierarchy submitted by: Bertram Felgenhauer Input: [ c -> f(b), c -> b ] Make it flat: [ c -> f(b), c -> b ] Time: 0.000 [s] Make it Complete (R^): [ f(c) = c, f(c) = f(b), f(c) = b, b = f(b), c = f(b), c = b ] Time: 0.001 [s] The number of normal forms that must be checked: 9 Time: 0.000 [s] Now checking all the pairs... Time to check pairs: 0.000 [s] The TRS doesn't have Uniqueness of Normal Forms. Counter Example: f(b) <->* f(f(b)) proof: f(b) ->R^ c ->R^ b f(f(b)) ->R^ f(c) ->R^ f(b) ->R^ c ->R^ b Total Time: 0.001 [s] problems/710.trs: Success(not UNC) real 0.02 user 0.02 sys 0.00