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).

  g(x) = (x + x')'             # label(definition_g).
  h(x) = x + (x + (x + g(x)))  # label(definition_h).

end_of_list.

formulas(goals).

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

end_of_list.