assign(max_seconds, 30). assign(new_constants, 1). formulas(sos). % These four equations are a basis for Boolean algebra (BA) x v (y v z) = y v (x v z) # label(AJ). x ^ y = (x' v y')' # label(DM). x v x' = y v y' # label(ONE). (x v y') ^ (x v y) = x # label(CUT). end_of_list. formulas(goals). x'' = x # answer(CC). x v (x ^ y) = x # answer(B1). x ^ (y v z) = (x ^ y) v (x ^ z) # answer(DIST1). x v (y ^ (x v z)) = x v (z ^ (x v y)) # answer(MOD). end_of_list.