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