assign(max_seconds, 60). assign(max_weight, 25). assign(constant_weight, 0). assign(nest_penalty, 2). formulas(sos). % candidate x ^ (y v (x ^ z)) = x ^ (y v (x ^ ((x ^ y) v (z ^ (x v y))))) # label(H7). end_of_list. formulas(goals). all x all y (x ^ y = x -> x' v y' = x'). % order reversibility end_of_list.