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