assign(max_minutes, 5).

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

clear(auto_denials).

clear(print_given).

list(weights).

  weight(g(_)) = 1.
  weight(g(x)) = 1000.

  weight(h(_)) = 1.
  weight(h(x)) = 1000.

  weight(f(_,_)) = 1.
  weight(f(x,y)) = 1000.

end_of_list.

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.