set(auto).
formula_list(usable).
all X Y ($GT(X,Y) -> max(X,Y,X)).
all X Y ($LE(X,Y) -> max(X,Y,Y)).
all X Y ($GT(X,Y) -> min(X,Y,Y)).
all X Y ($LE(X,Y) -> min(X,Y,X)).
all A B (delta(st(A,B),st(0,B))).
all A B (delta(st(A,B),st(A,0))).
all A B (delta(st(A,B),st(3,B))).
all A B (delta(st(A,B),st(A,5))).
all A B NA NB (max(0,$DIFF($SUM(A,B),5), NA) & min($SUM(A,B),5,NB) -> 
				delta(st(A,B),st(NA,NB))).
all A B NA NB (max(0,$DIFF($SUM(A,B),3), NB) & min($SUM(A,B),3,NA) -> 
				delta(st(A,B),st(NA,NB))).

all X Y (delta(X,Y) -> deltaX(X,Y)).
all A0 B0 A1 B1 A2 B2 (delta(st(A0,B0),st(A2,B2)) & deltaX(st(A2,B2),st(A1,B1)) 
				-> deltaX(st(A0,B0),st(A1,B1))).

all X Y (gt(X,Y) -> mymax(X,Y,X)).
all X Y ($LE(X,Y) -> mymax(X,Y,Y)).

-(exists x (mymax(3,2,x))).
%-(exists X (max(0,$DIFF($SUM(0,5),3), X) & min($SUM(A,B),3,3) )).
%-(exists X delta(st(0,5),st(3,2))).
end_of_list.

list(sos).
%-$EQ($SUM(3,2),5).
%-delta(st(3,4),st(X,5)).% | $ANS(X).
end_of_list.
