assign(max_minutes, 5).

assign(max_weight,35).
set(restrict_denials).

% clear(auto_denials).

% clear(print_given).

% list(weights).
% 
%   weight(g(_)) = 1.
%   weight(g(x)) = weight(x) + 3.
% 
%   weight(h(_)) = 1.
%   weight(h(x)) = weight(x) + 3.
% 
% end_of_list.

assign(eq_defs, fold).

formulas(assumptions).

  x + y = y + x                 # label(Commutativity).
  (x + y) + z = x + (y + z)     # label(Associativity).
  ((x + y)' + (x + y')')' = x   # label(Robbins).

end_of_list.

formulas(goals).

  (exists a exists b ((a + b)' = a')) # answer(Winker2a).
  (exists a exists b ((a + b)' = b')) # answer(Winker2b).
  (exists a exists b (a + b = a)) # answer(Winker1a).
  (exists a exists b (a + b = b)) # answer(Winker1b).
  (x + y')' + (x' + y')' = y # answer(Huntington).

end_of_list.

formulas(assumptions).

  g(x) = (x + x')'.
  h(x) = (x + (x + (x + g(x))))'.

end_of_list.