YES 1 decompositions #1 ----------- 1: a(b(x1)) -> c(a(x1)) 2: b(a(x2)) -> a(b(x2)) 3: a(c(x3)) -> b(b(x3)) 4: b(c(x4)) -> c(b(x4)) 5: c(b(x5)) -> b(a(x5)) 7: c(a(x7)) -> b(c(x7)) 8: b(a(x8)) -> c(c(x8)) 9: b(b(x9)) -> c(c(x9)) @Rule Labeling --- R 1: a(b(x1)) -> c(a(x1)) 2: b(a(x2)) -> a(b(x2)) 3: a(c(x3)) -> b(b(x3)) 4: b(c(x4)) -> c(b(x4)) 5: c(b(x5)) -> b(a(x5)) 7: c(a(x7)) -> b(c(x7)) 8: b(a(x8)) -> c(c(x8)) 9: b(b(x9)) -> c(c(x9)) --- S 1: a(b(x1)) -> c(a(x1)) 2: b(a(x2)) -> a(b(x2)) 3: a(c(x3)) -> b(b(x3)) 4: b(c(x4)) -> c(b(x4)) 5: c(b(x5)) -> b(a(x5)) 7: c(a(x7)) -> b(c(x7)) 8: b(a(x8)) -> c(c(x8)) 9: b(b(x9)) -> c(c(x9)) NOTE: input TRS is reduced original is 1: a(b(x1)) -> c(a(x1)) 2: b(a(x2)) -> a(b(x2)) 3: a(c(x3)) -> b(b(x3)) 4: b(c(x4)) -> c(b(x4)) 5: c(b(x5)) -> b(a(x5)) 6: b(a(x6)) -> c(c(x6)) 7: c(a(x7)) -> b(c(x7)) 8: b(a(x8)) -> c(c(x8)) 9: b(b(x9)) -> c(c(x9)) reduced to 1: a(b(x1)) -> c(a(x1)) 2: b(a(x2)) -> a(b(x2)) 3: a(c(x3)) -> b(b(x3)) 4: b(c(x4)) -> c(b(x4)) 5: c(b(x5)) -> b(a(x5)) 7: c(a(x7)) -> b(c(x7)) 8: b(a(x8)) -> c(c(x8)) 9: b(b(x9)) -> c(c(x9))