NO Problem: a(x1) -> x1 a(b(x1)) -> b(a(c(b(c(x1))))) b(x1) -> a(x1) c(c(x1)) -> x1 Proof: Unfolding Processor: loop length: 11 terms: a(b(c(b(x33260)))) b(a(c(b(c(c(b(x33260))))))) a(a(c(b(c(c(b(x33260))))))) a(a(c(a(c(c(b(x33260))))))) a(a(c(a(b(x33260))))) a(a(c(b(a(c(b(c(x33260)))))))) a(a(c(a(a(c(b(c(x33260)))))))) a(a(c(a(c(b(c(x33260))))))) a(a(c(c(b(c(x33260)))))) a(a(b(c(x33260)))) a(b(a(c(b(c(c(x33260))))))) context: [] substitution: x33260 -> c(c(x33260)) Qed