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: [ f(h(b,c)) -> c, a -> h(h(h(f(a),b),h(c,c)),f(b)), h(f(a),a) -> h(c,a), b -> b, h(h(b,f(b)),h(a,c)) -> b ] Try persistent and layer-preserving decomposition... Sort Assignment: a : =>9 b : =>9 c : =>9 f : 9=>9 h : 9*9=>9 maximal types: {9} ...decomposition failed. TRS: [ f(h(b,c)) -> c, a -> h(h(h(f(a),b),h(c,c)),f(b)), h(f(a),a) -> h(c,a), b -> b, h(h(b,f(b)),h(a,c)) -> b ] unknown Non-Omega-Overlapping unknown Right-Reducible Check distinct normal forms in critical pair closure...failed New rules by rule reversing: [ f(h(b,c)) -> c, a -> a, h(h(h(f(a),b),h(c,c)),f(b)) -> a, h(f(a),a) -> h(c,a), b -> b, h(h(b,f(b)),h(a,c)) -> b ] confluent TRS: [ f(h(b,c)) -> c, a -> a, h(h(h(f(a),b),h(c,c)),f(b)) -> a, h(f(a),a) -> h(c,a), b -> b, h(h(b,f(b)),h(a,c)) -> b ] UNC Completion (Strongly Closed) problems/701.trs: Success(UNC) (4 msec.)