# KEY
#  - not
#  + and
#  / or
#  = if and only if
#  > implies
#  a-z represent variables

(1/a)
(0>a)
(a=a)
(a>1)
(-a/a)
((a+b)>a)
((a+b)>b)
((a>b)/a)
(a>(a/b))
(a>(b>a))
(-(a+b)/a)
(-(a+b)/b)
(-(a>b)>a)
(-a/(a/b))
(-a/(b>a))
(-a>(a>b))
((-a/b)/a)
((-a>a)=a)
((a>-b)/b)
(a>(-a>b))
(-(-a/b)>a)
(-(a>-a)=a)
(-(a>-b)>b)
(-a=(a>-a))
(a>-(-a+b))
(((a+b)+a)>b)
(((a+b)+b)>a)
(((a+b)+c)>a)
(((a+b)+c)>b)
(((a+b)/a)=a)
(((a+b)/b)=b)
(((a+b)=a)/a)
(((a+b)=b)/b)
(((a+b)>c)/a)
(((a+b)>c)/b)
(((a/b)+a)=a)
(((a/b)+b)=b)
(((a/b)=a)/b)
(((a/b)=b)/a)
(((a=b)+a)>b)
(((a=b)+b)>a)
(((a=b)/a)/b)
(((a=b)/b)/a)
(((a=b)=a)=b)
(((a=b)=b)=a)
(((a>b)+b)=b)
(((a>b)/c)/a)
(((a>b)=a)>a)
(((a>b)>a)=a)
((a+b)>(a/b))
((a+b)>(a/c))
((a+b)>(a=b))
((a+b)>(b/c))
((a+b)>(c>a))
((a+b)>(c>b))
((a/b)/(a=b))
((a/b)/(a>c))
((a/b)/(b>c))
((a>(b>c))/b)
((a>b)/(b>a))
((a>b)/(b>c))
((a>b)/(c>a))
(a>((a+b)=b))
(a>((a/b)/b))
(a>((a/b)/c))
(a>((a/b)=a))
(a>((b>a)/c))
(a>((b>a)=a))
(a>(b>(a/c)))
(a>(b>(c>a)))
(-((a+b)+a)/b)
(-((a+b)+b)/a)
(-((a+b)+c)/a)
(-((a+b)+c)/b)
(-((a+b)/a)/a)
(-((a+b)/b)/b)
(-((a+b)=a)>a)
(-((a+b)=b)>b)
(-((a+b)>c)>a)
(-((a+b)>c)>b)
(-((a/b)=a)>b)
(-((a/b)=b)>a)
(-((a=b)+a)/b)
(-((a=b)+b)/a)
(-((a=b)/a)>b)
(-((a=b)/b)>a)
(-((a=b)=a)/b)
(-((a=b)=b)/a)
(-((a>b)/c)>a)
(-((a>b)=a)/a)
(-(a+b)/(a/b))
(-(a+b)/(a/c))
(-(a+b)/(a=b))
(-(a+b)/(b/c))
(-(a+b)/(c>a))
(-(a+b)/(c>b))
(-(a/b)>(a=b))
(-(a/b)>(a>c))
(-(a/b)>(b>c))
(-(a=b)>(a/b))
(-(a>(b>c))>b)
(-(a>b)>(a/c))
(-(a>b)>(b>a))
(-(a>b)>(b>c))
(-(a>b)>(c>a))
(-a/((a+b)=b))
(-a/((a/b)+a))
(-a/((a/b)/b))
(-a/((a/b)/c))
(-a/((a/b)=a))
(-a/((a=b)=b))
(-a/((b>a)+a))
(-a/((b>a)/c))
(-a/((b>a)=a))
(-a/(b>(a/c)))
(-a/(b>(c>a)))
(-a>((a+b)=a))
(-a>((a+b)>c))
(-a>((a/b)=b))
(-a>((a=b)/b))
(-a>((a>b)/c))
(-a>(b>(a>c)))
((-(a+b)/c)/a)
((-(a+b)/c)/b)
((-(a+b)=a)>a)
((-(a+b)=b)>b)
((-(a+b)>a)=a)
((-(a+b)>b)=b)
((-(a/b)/a)/b)
((-(a/b)/b)/a)
((-(a/b)=a)>b)
((-(a/b)=b)>a)
((-(a=b)=a)/b)
((-(a=b)=b)/a)
((-(a>b)+c)>a)
((-(a>b)/a)=a)
((-(a>b)=a)/a)
((-(a>b)>c)/a)
((-a+(a/b))>b)
((-a+(a>b))/a)
((-a+b)/(b>a))
((-a+b)>(a>c))
((-a/b)/(a/b))
((-a/b)/(a/c))
((-a/b)/(c>a))
((-a/b)=(a>b))
((-a=(a+b))>a)
((-a=(a/b))>b)
((-a=(a=b))/b)
((-a=(a>b))/a)
((-a=b)/(a=b))
((-a=b)>(a/b))
((-a>(a+b))=a)
((-a>b)/(a>c))
((-a>b)=(a/b))
(((-a+b)=b)/a)
(((-a/b)+a)>b)
(((-a/b)/b)/a)
(((-a/b)/c)/a)
(((-a/b)=a)>a)
(((-a/b)=a)>b)
(((-a/b)>a)=a)
(((-a=b)=a)/b)
(((-a=b)=b)/a)
(((-a>b)+a)=a)
(((a>-b)/c)/b)
(((a>-b)=b)>b)
(((a>-b)>b)=b)
((a+b)/(a>-b))
((a+b)/(b>-a))
((a+b)>(-a>c))
((a+b)>(-b>c))
((a/b)/(c>-a))
((a/b)/(c>-b))
((a=b)>(-a/b))
((a=b)>(-b/a))
((a>-(a+b))/b)
((a>-(b+c))/b)
((a>-(b+c))/c)
((a>-b)/(b/c))
((a>-b)/(c>b))
((a>(-b/c))/b)
((a>(b>-c))/c)
((a>b)/(c>-b))
(a>(-(a/b)>b))
(a>(-(a/b)>c))
(a>(-(a=b)/b))
(a>(-(b>a)>c))
(a>(-b/(a+b)))
(a>(-b/(a=b)))
(a>((-a+b)>c))
(a>((-a/b)=b))
(a>((-a=b)/b))
(a>((-a>b)/c))
(a>((-a>b)=a))
(a>((-b+a)/b))
(a>((-b=a)/b))
(a>(b>(-a>c)))
(-(-(a+b)/c)>a)
(-(-(a+b)/c)>b)
(-(-(a+b)=a)/a)
(-(-(a+b)=b)/b)
(-(-(a/b)/a)>b)
(-(-(a/b)/b)>a)
(-(-(a/b)=a)/b)
(-(-(a/b)=b)/a)
(-(-(a=b)=a)=b)
(-(-(a=b)=b)=a)
(-(-(a>b)+c)/a)
(-(-(a>b)/a)/a)
(-(-(a>b)=a)>a)
(-(-(a>b)>c)>a)
(-(-a+(a/b))/b)
(-(-a+(a>b))=a)
(-(-a+b)/(a>c))
(-(-a+b)=(b>a))
(-(-a/b)/(a>b))
(-(-a/b)>(a/b))
(-(-a/b)>(a/c))
(-(-a/b)>(c>a))
(-(-a=(a+b))/a)
(-(-a=(a/b))/b)
(-(-a=(a=b))=b)
(-(-a=(a>b))>a)
(-(-a=b)/(a/b))
(-(-a=b)=(a=b))
(-(-a>b)>(a>c))
(-((-a+b)=b)>a)
(-((-a/b)+a)/b)
(-((-a/b)/b)>a)
(-((-a/b)/c)>a)
(-((-a/b)=a)/a)
(-((-a/b)=a)/b)
(-((-a=b)=a)=b)
(-((-a=b)=b)=a)
(-((a/b)>-a)=a)
(-((a/b)>-b)=b)
(-((a>-b)/c)>b)
(-((a>-b)=b)/b)
(-((a>b)>-b)=b)
(-(a+b)/(-a>c))
(-(a+b)/(-b>c))
(-(a+b)=(a>-b))
(-(a+b)=(b>-a))
(-(a/b)/(-a>b))
(-(a/b)/(-b>a))
(-(a/b)>(-a/b))
(-(a/b)>(-a/c))
(-(a/b)>(-b/a))
(-(a/b)>(-b/c))
(-(a/b)>(c>-a))
(-(a/b)>(c>-b))
(-(a=b)/(-a/b))
(-(a=b)/(-b/a))
(-(a=b)=(-a=b))
(-(a=b)=(-b=a))
(-(a>-(a+b))>b)
(-(a>-(a/b))=a)
(-(a>-(b+c))>b)
(-(a>-(b+c))>c)
(-(a>-(b>a))=a)
(-(a>-b)=(a+b))
(-(a>-b)>(b/c))
(-(a>-b)>(c>b))
(-(a>(-a+b))=a)
(-(a>(-b/c))>b)
(-(a>(b>-c))>c)
(-(a>b)=(-b+a))
(-(a>b)>(-a>c))
(-(a>b)>(-b/c))
(-(a>b)>(c>-b))
(-a/(-(a/b)>b))
(-a/(-(a/b)>c))
(-a/(-(a=b)/b))
(-a/(-(b>a)>c))
(-a/(-b/(a+b)))
(-a/(-b/(a=b)))
(-a/((-a>b)+a))
(-a/((-a>b)=a))
(-a/((-b+a)/b))
(-a/((-b=a)/b))
(-a=(-(a=b)=b))
(-a=(-a+(a>b)))
(-a=(-b=(a=b)))
(-a=((-b=a)=b))
(-a=((a/b)>-a))
(-a=((b>a)>-a))
(-a=(a>-(a/b)))
(-a=(a>-(b>a)))
(-a=(a>(-a+b)))
(-a>(-(a+b)/c))
(-a>(-(a/b)/b))
(-a>(-(a>b)=a))
(-a>(-(a>b)>c))
(-a>(-a=(a>b)))
(-a>(b>-(a+b)))
(-a>(b>-(a+c)))
((-(-a+b)+a)=a)
((-(-a+b)+b)>a)
((-(-a+b)=b)>a)
((-(-a/b)+c)>a)
((-(-a/b)/a)=a)
((-(-a/b)=a)/a)
((-(-a/b)=a)/b)
((-(-a/b)>b)/a)
((-(-a/b)>c)/a)
((-(-a=b)+a)>b)
((-(-a=b)+b)>a)
((-(-a=b)/a)/b)
((-(-a=b)/b)/a)
((-(-a=b)=a)=b)
((-(-a=b)=b)=a)
((-(a+b)+a)>-b)
((-(a+b)+b)>-a)
((-(a+b)=a)>-b)
((-(a+b)=b)>-a)
((-(a/b)+c)>-a)
((-(a/b)+c)>-b)
((-(a/b)=a)>-a)
((-(a/b)=b)>-b)
((-(a=b)+a)>-b)
((-(a=b)+b)>-a)
((-(a>-b)+c)>b)
((-(a>-b)/b)=b)
((-(a>-b)=b)/b)
((-(a>-b)>c)/b)
((-(a>b)+c)>-b)
((-(a>b)=b)>-b)
((-a+(-a/b))/a)
((-a+(-b=a))>b)
((-a+(a=b))>-b)
((-a+(b>-a))/a)
((-a+b)/(-b/a))
((-a+b)>-(a+b))
((-a+b)>-(a+c))
((-a+b)>-(a=b))
((-a+b)>(-b=a))
((-a/(-b+a))/b)
((-a/(-b=a))/b)
((-a/b)/(-b+a))
((-a/b)/(-b=a))
((-a=(-a/b))/a)
((-a=(-b+a))>b)
((-a=(-b=a))=b)
((-a=(a+b))>-b)
((-a=(a/b))>-a)
((-a=(b>-a))/a)
((-a=(b>a))>-a)
((-a=b)/(-b/a))
((-a=b)=(-b=a))
((-a=b)>-(a+b))
((-a>b)=(-b>a))
(((-a+b)=a)>-a)
(((-a+b)=a)>-b)
(((-a=b)+a)>-b)
((a+b)>-(-a+b))
((a+b)>-(-a+c))
((a+b)>-(-a=b))
((a+b)>-(-b+a))
((a+b)>-(-b+c))
((a+b)>-(-b=a))
((a=b)>-(-a+b))
((a=b)>-(-b+a))
((a>-b)=(b>-a))
(a>-(-(a+b)+b))
(a>-(-(a+b)=b))
(a>-(-(a/b)+c))
(a>-(-(a/b)=a))
(a>-(-(a=b)+b))
(a>-(-(b>a)+c))
(a>-(-(b>a)=a))
(a>-(-a=(a/b)))
(a>-(-a=(b>a)))
(a>-(-b+(a=b)))
(a>-(-b=(a+b)))
(a>-((-a+b)+b))
(a>-((-a+b)+c))
(a>-((-a+b)=a))
(a>-((-a=b)+b))
(a>-((-b+a)=b))
(a>-((-b=a)+b))
(a>(-(-a+b)/c))
(a>(-(-a+b)=a))
(a>(-(-a/b)/b))
(a>(-(-a>b)>c))
(a>(-(-b+a)=b))
(a>(-a=(-a+b)))
(a>(b>-(-a+b)))
(a>(b>-(-a+c)))
(-(-(-a+b)+b)/a)
(-(-(-a+b)=b)/a)
(-(-(-a/b)+c)/a)
(-(-(-a/b)/a)/a)
(-(-(-a/b)=a)>a)
(-(-(-a/b)=a)>b)
(-(-(-a/b)>b)>a)
(-(-(-a/b)>c)>a)
(-(-(-a=b)+a)/b)
(-(-(-a=b)+b)/a)
(-(-(-a=b)/a)>b)
(-(-(-a=b)/b)>a)
(-(-(-a=b)=a)/b)
(-(-(-a=b)=b)/a)
(-(-(a>-b)+c)/b)
(-(-(a>-b)/b)/b)
(-(-(a>-b)=b)>b)
(-(-(a>-b)>c)>b)
(-(-a+(-a/b))=a)
(-(-a+(-b=a))/b)
(-(-a+(b>-a))=a)
(-(-a+b)/(-b=a))
(-(-a+b)=(-b/a))
(-(-a/(-a+b))=a)
(-(-a/(-b+a))>b)
(-(-a/(-b=a))>b)
(-(-a/b)=(-b+a))
(-(-a/b)>(-b=a))
(-(-a=(-a/b))>a)
(-(-a=(-b+a))/b)
(-(-a=(-b=a))/b)
(-(-a=(b>-a))>a)
(-(-a=b)/(-b=a))
(-(-a=b)>(-b/a))
(-(-a>a)=(a>-a))
(-((-a>b)>-a)=a)
(-(a>-(-a>b))=a)
(-(a>-a)=(-a>a))
(-a/(-(-a+b)+a))
(-a/(-(-a+b)=a))
(-a/(-(-b+a)=b))
(-a/(-(-b=a)=b))
(-a=(a>-(-a>b)))
(-a>(-(-a/b)=a))
(-a>(-(-b/a)=b))
(-a>(-(-b=a)/b))
(-a>(-(b>-a)=a))
((-(-a>b)=a)>-a)
(a>-(-(-a/b)=b))
(a>-(-(-a>b)+c))
(a>-(-(-a>b)=a))
(a>-(-a=(-a>b)))
(a>-(-b+(-a/b)))
(a>-(-b=(-a/b)))
((((a+b)+a)+a)>b)
((((a+b)+a)+c)>b)
((((a+b)+a)/b)=b)
((((a+b)+a)=b)/b)
((((a+b)+a)>c)/b)
((((a+b)+b)+b)>a)
((((a+b)+b)+c)>a)
((((a+b)+b)/a)=a)
((((a+b)+b)=a)/a)
((((a+b)+b)>c)/a)
((((a+b)+c)+a)>b)
((((a+b)+c)+b)>a)
((((a+b)+c)+c)>a)
((((a+b)+c)+c)>b)
((((a+b)+c)+d)>a)
((((a+b)+c)+d)>b)
((((a+b)+c)/a)=a)
((((a+b)+c)/b)=b)
((((a+b)+c)=a)/a)
((((a+b)+c)=b)/b)
((((a+b)+c)>d)/a)
((((a+b)+c)>d)/b)
((((a+b)/a)+b)>a)
((((a+b)/a)+c)>a)
((((a+b)/a)/a)=a)
((((a+b)/a)>b)/a)
((((a+b)/a)>c)/a)
((((a+b)/b)+a)>b)
((((a+b)/b)+c)>b)
((((a+b)/b)/b)=b)
((((a+b)/b)>a)/b)
((((a+b)/b)>c)/b)
((((a+b)/c)=c)/a)
((((a+b)/c)=c)/b)
((((a+b)/c)>a)/c)
((((a+b)/c)>b)/c)
((((a+b)=a)+a)>b)
((((a+b)=a)+b)=b)
((((a+b)=a)/b)/a)
((((a+b)=a)/c)/a)
((((a+b)=a)=a)>a)
((((a+b)=a)=a)>b)
((((a+b)=a)>a)=a)
((((a+b)=b)+a)=a)
((((a+b)=b)+b)>a)
((((a+b)=b)/a)/b)
((((a+b)=b)/c)/b)
((((a+b)=b)=b)>a)
((((a+b)=b)=b)>b)
((((a+b)=b)>b)=b)
((((a+b)=c)+c)>a)
((((a+b)=c)+c)>b)
((((a+b)=c)/a)/c)
((((a+b)=c)/b)/c)
((((a+b)=c)/c)/a)
((((a+b)=c)/c)/b)
((((a+b)=c)=c)>a)