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