assign(max_seconds, 120).

assign(max_weight, 50).

function_order([v, c, ^, f]).  % rewrite to join/complement

formulas(sos).

f(f(f(f(y,x),f(x,z)),u),f(x,f(f(z,f(f(x,x),z)),z))) = x # label(OML_Sh).

x v y = f(f(x,x),f(y,y)) # label(Def_join).
x ^ y = f(f(x,y),f(x,y)) # label(Def_meet).
c(x) = f(x,x) # label(Def_complement).

end_of_list.

formulas(goals).

x v (x ^ y) = x                # answer(B1).
x v (c(x) ^ (x v y)) = x v y   # answer(OM).

x v (y v z) = y v (x v z)      # answer(AJ).
x ^ y = c(c(x) v c(y))         # answer(DM).
f(x,y) = c(x) v c(y)           # answer(DEF_SS).

x v x = x                      # answer(idempotence_join).
x ^ x = x                      # answer(idempotence_meet).
c(c(x)) = x                    # answer(cc).
y v x = x v y                  # answer(commutativity_join).
y v x = x v y                  # answer(commutativity_meet).
x v c(x) = y v c(y)            # answer(1).
x ^ c(x) = y ^ c(y)            # answer(0).

(x v y) v z = x v (y v z)      # answer(assoc_join).
(x ^ y) ^ z = x ^ (y ^ z)      # answer(assoc_meet).

end_of_list.