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(f(b),a)) -> b, f(c) -> b, b -> f(b) ] Make it flat: [ f(!cl_1) -> b, !cl_1 -> !cl_1, h(!cl_0,a) -> !cl_1, f(c) -> b, b -> f(b), f(b) -> !cl_0, !cl_0 -> !cl_0 ] Time: 0.000 [s] Make it Complete (R^): [ !cl_0 = f(!cl_1), f(!cl_1) = f(b), f(!cl_1) = f(!cl_0), f(!cl_1) = f(c), f(!cl_1) = b, h(b,a) = h(!cl_0,a), h(b,a) = !cl_1, h(!cl_0,a) = !cl_1, !cl_0 = f(c), f(c) = f(b), f(c) = f(!cl_0), f(c) = b, f(!cl_0) = !cl_0, f(!cl_0) = f(b), f(!cl_0) = b, b = !cl_0, b = f(b), f(b) = !cl_0 ] Time: 0.002 [s] CPNF: [ a … a, c … c ] 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/711.trs: Success(UNC) real 0.02 user 0.00 sys 0.01