YES (ignored inputs)COMMENT Cops #647 - #721: generated ground TRSs; evenly distributed in the UNR/UNC/NFP/CR hierarchy submitted by: Bertram Felgenhauer Input: [ b -> h(b,a), b -> h(f(b),f(h(b,a))) ] Make it flat: [ b -> h(b,a), !cr_0 -> f(b), !cr_1 -> h(b,a), !cr_2 -> f(!cr_1), b -> h(!cr_0,!cr_2) ] Time: 0.000 [s] Make it Complete (R^): [ f(b) = !cr_2, h(!cr_1,a) = !cr_1, f(!cr_1) = f(b), h(!cr_0,!cr_0) = b, h(!cr_0,!cr_0) = h(b,a), h(!cr_0,!cr_0) = !cr_1, h(!cr_0,!cr_0) = h(!cr_1,a), h(!cr_2,!cr_2) = b, h(!cr_2,!cr_2) = h(b,a), h(!cr_2,!cr_2) = !cr_1, h(!cr_2,!cr_0) = h(!cr_1,a), h(!cr_0,!cr_0) = h(!cr_2,!cr_2), h(!cr_0,!cr_0) = h(!cr_2,!cr_0), h(!cr_2,!cr_2) = h(!cr_2,!cr_0), h(!cr_0,!cr_0) = h(!cr_0,!cr_2), h(!cr_2,!cr_0) = b, h(!cr_2,!cr_0) = h(b,a), h(!cr_2,!cr_0) = !cr_1, h(!cr_2,!cr_0) = h(!cr_0,!cr_2), h(!cr_2,!cr_2) = h(!cr_0,!cr_2), h(!cr_2,!cr_2) = h(!cr_1,a), !cr_0 = !cr_2, f(!cr_1) = !cr_0, h(!cr_1,a) = b, h(!cr_1,a) = h(b,a), h(!cr_1,a) = h(!cr_0,!cr_2), b = !cr_1, h(!cr_0,!cr_2) = !cr_1, h(b,a) = h(!cr_0,!cr_2), b = h(b,a), !cr_0 = f(b), !cr_1 = h(b,a), !cr_2 = f(!cr_1), b = h(!cr_0,!cr_2) ] Time: 0.018 [s] CPNF: [ a … a ] 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.019 [s] problems/721.trs: Success(UNC) real 0.04 user 0.03 sys 0.01