MAYBE Problem: f(f(f(a(),x),y),z) -> f(f(x,z),f(y,z)) f(f(b(),x),y) -> x f(c(),y) -> y Proof: DP Processor: DPs: f#(f(f(a(),x),y),z) -> f#(y,z) f#(f(f(a(),x),y),z) -> f#(x,z) f#(f(f(a(),x),y),z) -> f#(f(x,z),f(y,z)) TRS: f(f(f(a(),x),y),z) -> f(f(x,z),f(y,z)) f(f(b(),x),y) -> x f(c(),y) -> y Open