NO Problem: f(h(x),y) -> h(f(y,f(x,h(a())))) Proof: Unfolding Processor: loop length: 6 terms: f(h(h(x660)),h(h(x888))) h(f(h(h(x888)),f(h(x660),h(a())))) h(h(f(f(h(x660),h(a())),f(h(x888),h(a()))))) h(h(f(h(f(h(a()),f(x660,h(a())))),f(h(x888),h(a()))))) h(h(f(h(h(f(f(x660,h(a())),f(a(),h(a()))))),f(h(x888),h(a()))))) h(h(f(h(h(f(f(x660,h(a())),f(a(),h(a()))))),h(f(h(a()),f(x888,h(a()))))))) context: h(h([])) substitution: x660 -> f(f(x660,h(a())),f(a(),h(a()))) x888 -> f(f(x888,h(a())),f(a(),h(a()))) Qed