% query: p([T1 $= 0 $| s(T1) $| plus(T1,T1) $| mul(T1,T1) $| f(T1)],[T2 $=MAX])
p(plus(0,X),X).
p(plus(s(X),Y),s(Z)):- p(plus(X,Y),Z).
p(mul(0,X),0).
p(mul(s(X),Y),Z):- p(mul(X,Y),T), p(plus(T,Y),Z).
p(f(mul(X,Y)),Z):- p(f(X),Z1),p(f(Y),Z2),p(mul(Z1,Z2),Z).
p(f(plus(X,Y)),Z):- p(f(X),Z1),p(f(Y),Z2),p(plus(Z1,Z2),Z).
p(f(s(X)),s(Z)):- p(f(X),Z).
