/usr/share/doc/prover9-doc/examples/LT-82-2-interp.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 | formulas(sos).
% lattice theory
x v y = y v x.
(x v y) v z = x v (y v z).
x ^ y = y ^ x.
(x ^ y) ^ z = x^ (y ^ z).
x ^ (x v y) = x.
x v (x ^ y) = x.
% This input is for Mace4, so we can include the following,
% because finite lattices always have 0 and 1.
x v 0 = x.
x ^ 1 = x.
end_of_list.
formulas(sos).
end_of_list.
% We want the following to be false, so we put it in the goals list.
formulas(goals).
x ^ (y v (x ^ z)) = x ^ (y v (z ^ ((x ^ (y v z)) v (y ^ z)))) # label(H2).
end_of_list.
|