include("ortholattice-header"). % MOL basis: { AJ, B1, DM, CC, ONE, MOD } % MOL_SS basis: { A_SS, B_SS, ONE_SS, MOD_SS } list(sos). x v (y v z) = y v (x v z). % AJ x v (x ^ y) = x. % B1 x ^ y = c(c(x) v c(y)). % DM c(c(x)) = x. % CC x v c(x) = y v c(y). % ONE x v (y ^ (x v z)) = x v (z ^ (x v y)). % MOD f(x,y) = c(x) v c(y). % DEF_SS end_of_list. % The following command orders the relevant operations as f < v < c < ^ % so that everything is rewritten in terms of f whenever possible. lex([D, C, B, A, 0, 1, f(x,x), x v x, c(x), x ^ x]). assign(max_proofs, 7). list(passive). f(A,f(f(B,C),f(B,C))) != f(B,f(f(A,C),f(A,C))) | $Ans(A_SS). f(f(A,A),f(A,B)) != A | $Ans(B_SS). f(A,f(A,A)) != f(B,f(B,B)) | $Ans(ONE_SS). f(A,f(B,f(A,f(C,C)))) != f(A,f(C,f(A,f(B,B)))) | $Ans(MOD_SS). A v B != f(f(A,A),f(B,B)) | $Ans(DEF_J). A ^ B != f(f(A,B),f(A,B)) | $Ans(DEF_M). c(A) != f(A,A) | $Ans(DEF_C). end_of_list.