formulas(sos).
% Associativity
x ^ (y ^ z)= (x ^ y) ^ z # label (s1).
x v (y v z)= (x v y) v z # label (s2).
% Absorption
(y ^ x) v x= x # label (s3).
x ^ (x v y)= x # label (s4).
(y v x) ^ x= x # label (s5).
x v (x ^ y)= x # label (s6).
% Commutativity
x ^ y= y ^ x # label (s7).
x v y= y v x # label (s8).
% Idempotency
x ^ x= x # label (s9).
x v x=x # label (s10).
% *Absorption
(x ^ y) v x= x # label (s11).
x ^ (y v x)= x # label (s12).
(x v y) ^ x= x # label (s13).
x v (y ^ x)= x # label (s14).
% Right-handed
x ^ ( y ^ x ) = y ^ x # label (s15).
x v ( y v x) = x v y # label (s16).
% Left-handed
x ^ ( y ^ x) = x ^ y # label (s17).
x v ( y v x) = y v x # label (s18).
% Regularity
x ^ ( y ^ ( x ^ ( w ^ x) ) ) = x ^ ( y ^ ( w ^ x ) ) # label (s19).
x v ( y v ( x v ( w v x ) ) ) =x v ( y v ( w v x ) ) # label (s20).
%Rectangularity
x ^ y= y v x # label (s21).
% Symmetricity
x ^ ( y ^ (x v ( y v x) ) )= ( ( (x v y ) v x) ^ y ) ^ x # label (s22).
x v ( y v (x ^ ( y ^ x) ) ) = ( ( (x ^ y) ^ x) v y ) v x # label (s23).
% Normality
x ^ ( y ^ ( z ^ w) ) = x ^ ( z ^ ( y ^ w ) ) # label (s24).
x v ( y v ( z v w) )= x v ( z v ( y v w ) ) # label (s25).
% Quasi-distributivity
((x ^ (y v z)) ^ ((x ^ y) v (x ^ z)) ) ^ (x ^ (y v z))=x ^ (y v z) # label (s26).
% Cancellation = s22 + s23 + s26 + s27
(((x ^ (y ^ z) )^ x) v ( ( ((x v (y ^ z)) v x) ^ y ) ^ z ) ^ ((x v (y ^ z)) v x)) v ((x ^ (y ^ z) ) ^ x)=(((x ^ (y ^ z)) ^ x) v ( ( ( ((x v (y ^ z)) v x) ^ z) ^ y ) ^ ((x v (y ^ z) )v x))) v ((x ^ (y ^ z)) ^ x) # label (s27).
% Strongly Symmetric
((y v ( x v y )) ^ x ) ^ (y v ( x v y))=(((y ^ x ) ^ y) v x )v ((y ^ x) ^ y) # label (s28).
% Distributivity
(x ^ (y v z) ) ^ x= ((x ^ y )^ x) v ((x ^ z )^ x) # label (s29).
(x v (y ^ z)) v x= ((x v y )v x) ^ ((x v z )v x) # label (s30).
% Mid Distributivity
x ^ (y v z)= (x ^ y) v (x ^ z) # label (s31).
(x v y) ^ z= (x ^ z) v (y ^ z) # label (s32).
x v (y ^ z)= (x v y) ^ (x v z) # label (s33).
(x ^ y) v z= (x v z) ^ (y v z) # label (s34).
% Bidistributivity
(x ^ (y v z) ) ^ w= ((x ^ y ) ^ w) v ((x ^ z ) ^ w) # label (s35).
(x v (y ^ z) ) v w= ((x v y ) v w) ^ ((x v z ) v w) # label (s36).
% Categoricity
(x ^ ((((x ^ z ) ^ x) v y ) v ((x ^ z ) ^ x))) ^ x = (x ^ ((((z ^ x) ^ z) v y) v ((z ^ x ) ^ z))) ^ x # label (s37).
(x v ( (((x v z) v x) ^ y ) ^ ((x v z) v x)) ) v x = (x v ((((z v x ) v z) ^ y) ^ ((z v x ) v z))) v x # label (s38).
% Strict Categoricity
(x v (((y ^ z ) ^ u )^ y)) v x = (x v (((y ^ u) ^ z) ^ y) ) v x # label (s39).
(x ^ (((y v z )v u ) v y)) ^ x = (x ^ (( (y v u) v z) v y)) ^ x # label (s40).