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.