
formulas(theory).

  % Orthomodular lattice (OML)

  f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # label(A_SS).
  f(f(x,x),f(x,y)) = x                          # label(B_SS).
  f(x,f(x,x)) = f(y,f(y,y))                     # label(ONE_SS).
  f(x,f(x,f(x,y))) = f(x,y)                     # label(OM_SS).

  % lemmas/definitions

  f(x,f(x,x)) = 1                               # label(ONE_CONSTANT).
  f(1,1) = 0.

  % denial of modularity

  f(A,f(B,f(A,f(C,C)))) != f(A,f(C,f(A,f(B,B)))) # answer(MOD_SS).

end_of_list.
