YES (THEORY (AC plus ) ) (VAR x2 x1 x y ) (RULES plus(x2,p(x1)) -> p(plus(x1,x2)) plus(x2,s(x1)) -> s(plus(x1,x2)) p(s(x)) -> x s(p(x)) -> x plus(s(x),y) -> s(plus(x,y)) plus(p(x1),x2) -> p(plus(x1,x2)) )