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