(COMMENT 
4-ary Ackermann and arith

)

(VAR z  y  x l)
(RULES
a(h,h,h,x) -> s(x)
a(l,x,s(y),h) -> a(l,x,y,s(h))
a(l,x,s(y),s(z)) -> a(l,x,y,a(l,x,s(y),z))
a(l,s(x),h,z) -> a(l,x,z,z)
a(s(l),h,h,z) -> a(l,z,h,z)
+(x, h) -> x 
+(h, x) -> x 
+(s(x), s(y)) -> s(s(+(x,y)))
+(+(x,y),z) -> +(x,+(y,z))
s(h) -> 1
*(h,x) -> h
*(x,h) -> h
*(s(x), s(y)) -> s(+(+(*(x, y), x), y))
)