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 -> f(b), b -> f(b), h(h(h(h(h(h(h(a,h(c,h(f(c),b))),h(b,h(b,h(f(f(h(c,b))),a)))),h(a,a)),b),f(h(h(f(a),a),c))),a),h(c,a)) -> f(a), c -> h(b,b) ] Make it flat: [ h(!cl_19,!cl_20) -> f(a), !cl_20 -> !cl_20, h(c,a) -> !cl_20, !cl_18 -> !cl_18, h(!cl_13,!cl_17) -> !cl_18, !cl_16 -> !cl_16, h(!cl_15,c) -> !cl_16, f(a) -> !cl_14, !cl_12 -> !cl_12, h(!cl_10,!cl_11) -> !cl_12, !cl_10 -> !cl_10, h(!cl_3,!cl_9) -> !cl_10, !cl_8 -> !cl_8, h(b,!cl_7) -> !cl_8, !cl_6 -> !cl_6, f(!cl_5) -> !cl_6, !cl_4 -> !cl_4, h(c,b) -> !cl_4, !cl_2 -> !cl_2, h(c,!cl_1) -> !cl_2, b -> f(b), b -> f(b), !cl_0 -> !cl_0, f(c) -> !cl_0, c -> h(b,b), h(!cl_0,b) -> !cl_1, !cl_1 -> !cl_1, h(a,!cl_2) -> !cl_3, !cl_3 -> !cl_3, f(!cl_4) -> !cl_5, !cl_5 -> !cl_5, h(!cl_6,a) -> !cl_7, !cl_7 -> !cl_7, h(b,!cl_8) -> !cl_9, !cl_9 -> !cl_9, h(a,a) -> !cl_11, h(!cl_12,b) -> !cl_13, !cl_13 -> !cl_13, h(!cl_14,a) -> !cl_15, f(!cl_16) -> !cl_17, !cl_17 -> !cl_17, h(!cl_18,a) -> !cl_19, !cl_19 -> !cl_19 ] Time: 0.017 [s] Make it Complete (R^): [ h(!cl_19,!cl_20) = !cl_14, h(!cl_19,!cl_20) = f(a), h(c,a) = !cl_20, h(!cl_13,!cl_17) = !cl_18, h(!cl_15,c) = !cl_16, f(a) = !cl_14, h(!cl_10,!cl_11) = !cl_12, h(!cl_3,!cl_9) = !cl_10, h(b,!cl_7) = !cl_8, f(!cl_5) = !cl_6, h(c,b) = !cl_4, h(c,!cl_1) = !cl_2, b = f(b), f(c) = !cl_0, c = h(b,b), h(!cl_0,b) = !cl_1, h(a,!cl_2) = !cl_3, f(!cl_4) = !cl_5, h(!cl_6,a) = !cl_7, h(b,!cl_8) = !cl_9, h(a,a) = !cl_11, h(!cl_12,b) = !cl_13, h(!cl_14,a) = !cl_15, f(!cl_16) = !cl_17, h(!cl_18,a) = !cl_19 ] Time: 0.002 [s] CPNF: [ !cl_11 … !cl_11, !cl_14 … !cl_14, !cl_15 … !cl_15, 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.020 [s] problems/651.trs: Success(UNC) real 0.04 user 0.03 sys 0.01