assign(max_seconds, 30). formulas(theory). % Modular ortholattice (MOL) in terms of the Sheffer stroke f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))). % A_SS f(f(x,x),f(x,y)) = x. % B_SS f(x,f(x,x)) = f(y,f(y,y)). % ONE_SS f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))). % MOD_SS % lemmas: f(x,f(x,x)) = 1. f(x,y) = f(y,x). % commutativity end_of_list. formulas(goals). % The following, along with commutitiviy, gives Boolean, % so denying this produces a non-Boolean MOL. f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2). end_of_list.