/usr/share/doc/prover9-doc/examples/hard.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 25 26 27 28 29 30 31 32 33 | % assign(new_constants, 1).
assign(eq_defs, fold).
set(restrict_denials).
formulas(assumptions).
% Veroff's 2-basis for BA in terms of the Sheffer stroke.
f(x,y) = f(y,x).
f(f(x,y),f(x,f(y,z))) = x.
% Define a new operation (which turns out to be complement).
% The "assign(eq_defs, fold)" above causes this definition to be
% oriented as a rewrite rule so that the operation is introduced
% whenever possible.
x' = f(x,x).
end_of_list.
formulas(goals).
% Sheffer basis for Boolean Algebra
f(f(x,x),f(x,x)) = x # label(Sheffer_1).
f(x,f(y,f(y,y))) = f(x,x) # label(Sheffer_2).
f(f(f(y,y),x),f(f(z,z),x)) = f(f(x,f(y,z)),f(x,f(y,z))) # label(Sheffer_3).
end_of_list.
|