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.