(VAR x y z) (RULES +(0,y) -> y +(x,0) -> x +(s(x),y) -> s(+(x,y)) +(x,s(y)) -> s(+(x,y)) +(x,+(y,z)) -> +(+(x,y),z) +(+(x,y),z) -> +(x,+(y,z)) ) (COMMENT full experiments for [35] submitted by: Takahito Aoto and Yoshihito Toyama )