(VAR x y z)
(THEORY (AC p min max))
(RULES
plus(x,0) -> x
plus(x,s(y)) -> s(plus(x,y))
min(0,y) -> 0
min(s(x),s(y)) -> s(min(x,y))
max(0,y) -> y
max(s(x),s(y)) -> s(max(x,y))
)