include("ortholattice-header"). % Modify the basic strategy. lex([A, B, C, D, 0, 1, x v x, x ^ x, c(x), f(x,x)]). assign(max_proofs, 2). % BA basis: { AJ, DM, ONE, CUT } list(sos). x v (y v z) = y v (x v z). % AJ x ^ y = c(c(x) v c(y)). % DM x v c(x) = y v c(y). % ONE (x v c(y)) ^ (x v y) = x. % CUT % Axiom ONE allows us to name the constant. Also name its complement. x v c(x) = 1. % ONEa c(1) = 0. end_of_list. list(passive). A v (A ^ B) != A | $Ans(B1). % denial of B1 c(c(A)) != A | $Ans(CC). % denial of CC end_of_list.