/usr/share/doc/prover9-doc/examples/BA2.in is in prover9-doc 0.0.200902a-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 | formulas(assumptions).
% 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.
|