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