NO (ignored inputs)COMMENT Cops #647 - #721: generated ground TRSs; evenly distributed in the UNR/UNC/NFP/CR hierarchy submitted by: Bertram Felgenhauer Rewrite Rules: [ h(f(f(c)),h(c,h(c,h(h(f(b),f(f(f(f(b))))),b)))) -> h(h(a,a),f(c)), h(b,h(c,h(b,h(a,b)))) -> a, f(c) -> f(f(a)), a -> f(f(b)) ] Apply Direct Methods... Inner CPs: [ h(f(f(f(a))),h(c,h(c,h(h(f(b),f(f(f(f(b))))),b)))) = h(h(a,a),f(c)), h(b,h(c,h(b,h(f(f(b)),b)))) = a ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Combined result: not CR 708.trs: Success(not CR) (1895 msec.)