YES (ignored inputs)COMMENT Cops #647 - #721: generated ground TRSs; evenly distributed in the UNR/UNC/NFP/CR hierarchy submitted by: Bertram Felgenhauer Input: [ f(h(b,a)) -> a, f(f(f(c))) -> c, b -> c, c -> c, a -> a ] Make it flat: [ f(!cl_2) -> c, f(!cl_1) -> a, !cl_2 -> !cl_2, f(!cl_0) -> !cl_2, !cl_0 -> !cl_0, f(c) -> !cl_0, a -> a, c -> c, b -> c, h(b,a) -> !cl_1, !cl_1 -> !cl_1 ] Time: 0.000 [s] Make it Complete (R^): [ b = f(!cl_2), f(!cl_2) = c, f(!cl_1) = a, f(!cl_0) = !cl_2, f(b) = f(c), f(b) = !cl_0, f(c) = !cl_0, h(c,a) = h(b,a), h(c,a) = !cl_1, b = c, h(b,a) = !cl_1 ] Time: 0.001 [s] CPNF: [ ] Time: 0.000 [s] Now checking all the pairs in CW... Time to check pairs: 0.000 [s] The TRS has Uniqueness of Normal Forms. Total Time: 0.002 [s] problems/683.trs: Success(UNC) real 0.04 user 0.02 sys 0.01