/usr/share/doc/prover9-doc/examples/MOL.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 | formulas(assumptions).
x v (y v z) = y v (x v z). % AJ
x v (x ^ y) = x. % B1
x ^ y = (x' v y')'. % DM
x'' = x. % CC
x v x' = y v y'. % ONE
x v (y ^ (x v z)) = x v (z ^ (x v y)). % MOD
end_of_list.
formulas(goals).
x ^ (y v z) = (x ^ y) v (x ^ z).
end_of_list.
|