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