Problem: f(x,x) -> plus(plus(x,x),x) plus(x,y) -> plus(y,x) Proof: Open