/usr/share/doc/prover9-doc/examples/group.demods 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 | formulas(demodulators).
% This is the complete set of reductions for free groups.
% It can be used to canonicalize group terms.
(x * y) * z = x * (y * z).
e * x = x.
x * e = x.
x' * x = e.
x * x' = e.
x' ' = x.
e' = e.
x * (x' * y) = y.
x' * (x * y) = y.
(x * y)' = y' * x'.
end_of_list.
|