YES (ignored inputs)COMMENT Cops #647 - #721: generated ground TRSs; evenly distributed in the UNR/UNC/NFP/CR hierarchy submitted by: Bertram Felgenhauer input TRS: [ a -> c, a -> h(c,a), h(b,f(c)) -> b, c -> h(a,h(h(b,a),a)) ] TRS: [ a -> c, a -> h(c,a), h(b,f(c)) -> b, c -> h(a,h(h(b,a),a)) ] unknown Non-Omega-Overlapping unknown Right-Reducible Check distinct normal forms in critical pair closure...failed New rules by rule reversing: [ a -> c, h(c,a) -> a, h(b,f(c)) -> b, c -> c, h(a,h(h(b,a),a)) -> c ] unknown UNC Completion (Strongly Closed) unknown UNC Completion (Development Closed) Obtained TRSs: [ a -> c, h(c,a) -> a, h(b,f(c)) -> b, c -> c, h(a,h(h(b,a),a)) -> c, h(c,c) -> a, h(c,h(h(b,a),a)) -> c, h(a,h(h(b,c),a)) -> c, h(a,h(h(b,a),c)) -> c, h(c,h(h(b,c),a)) -> c, h(c,h(h(b,a),c)) -> c, h(a,h(h(b,c),c)) -> c, h(c,h(h(b,c),c)) -> c ] ...linear strongly closed TRS UNC Completion (General) problems/668.trs: Success(UNC) (20 msec.)