assign(max_seconds, 300).
assign(order, kbo).
assign(new_constants, 1).
set(restrict_denials).
assign(eq_defs, fold).

formulas(assumptions).

  % Single axiom for Ortholattices (OL) in terms of Sheffer stroke.

  f(f(f(f(y,x),f(x,z)),u),f(x,f(f(x,f(f(y,y),y)),z))) = x # label(OL_Sh).

  % Define some operations.

  x v y = f(f(x,x),f(y,y))  # label(definition_join).
  x ^ y = f(f(x,y),f(x,y))  # label(definition_meet).
  x' = f(x,x)               # label(definition_complementation).

end_of_list.

formulas(goals).

  % 3-basis for OL in terms of Sheffer stroke.

  f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z)))  # answer(assoc).
  f(f(x,x),f(x,y)) = x                           # answer(absorb).
  f(x,f(x,x)) = f(y,f(y,y))                      # answer(one).

  f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z)))
     & f(f(x,x),f(x,y)) = x
     & f(x,f(x,x)) = f(y,f(y,y))
     # answer(combined).

end_of_list.