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