YES (ignored inputs)COMMENT submitted by: Johannes Waldmann input TRS: [ a(c(?x)) -> c(a(?x)), a(a(?x)) -> a(a(?x)), a(b(?x)) -> c(a(?x)), a(a(?x)) -> a(c(?x)), c(a(?x)) -> c(b(?x)), b(b(?x)) -> a(c(?x)), b(a(?x)) -> a(c(?x)), c(b(?x)) -> a(b(?x)), a(a(?x)) -> c(a(?x)) ] Try persistent and layer-preserving decomposition... Sort Assignment: a : 16=>16 b : 16=>16 c : 16=>16 maximal types: {16} ...decomposition failed. TRS: [ a(c(?x)) -> c(a(?x)), a(a(?x)) -> a(a(?x)), a(b(?x)) -> c(a(?x)), a(a(?x)) -> a(c(?x)), c(a(?x)) -> c(b(?x)), b(b(?x)) -> a(c(?x)), b(a(?x)) -> a(c(?x)), c(b(?x)) -> a(b(?x)), a(a(?x)) -> c(a(?x)) ] unknown Non-Omega-Overlapping Right-Reducible problems/1019.trs: Success(UNC) (0 msec.)