assign(max_seconds, 60).

assign(max_weight, 25).

list(weights).
weight(x') = weight(x).                    % weight(x') = weight(x)
end_of_list.

formulas(sos).

% candidate

x ^ (y v (z ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ (y v u)))) # label(H49).

end_of_list.

formulas(goals).

x ^ (y v z) = (x ^ y) v (x ^ z) # label(distributivity).

end_of_list.