MAYBE (ignored inputs)COMMENT TPDB SRS_Standard/Secret_06_SRS/secr6 input TRS: [ a(b(c(?x))) -> c(c(c(b(b(b(a(a(a(?x))))))))), c(b(?x)) -> a(a(a(?x))), a(?x) -> ?x, b(?x) -> ?x, c(?x) -> ?x ] TRS: [ a(b(c(?x))) -> c(c(c(b(b(b(a(a(a(?x))))))))), c(b(?x)) -> a(a(a(?x))), a(?x) -> ?x, b(?x) -> ?x, c(?x) -> ?x ] New rules by rule reversing: [ c(c(c(b(b(b(a(a(a(?x))))))))) -> a(b(c(?x))), a(a(a(?x))) -> c(b(?x)), a(?x) -> ?x, b(?x) -> ?x, c(?x) -> ?x ] Check distinct normal forms in critical pair closure...failed problems/938.trs: Failure(unknown UNC) (16 msec.)