/usr/share/doc/prover9-doc/examples/RBA-2.tptp 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 | % The LADR formulas contain function or predicate symbols
% that are not legal TPTP symbols, and we have replaced those
% symbols with new symbols. Here is the list of the unaccepted
% symbols and the corresponding replacements.
%
% (arity 1) ' tptp0
% (arity 2) + tptp1
cnf(sos,axiom,tptp1(A,B) = tptp1(B,A)).
cnf(sos,axiom,tptp1(tptp1(A,B),C) = tptp1(A,tptp1(B,C))).
cnf(sos,axiom,tptp0(tptp1(tptp0(tptp1(A,B)),tptp0(tptp1(A,tptp0(B))))) = A).
fof(sos,axiom,? [X0] : tptp1(X0,X0) = X0).
fof(goals,conjecture,! [X1] : ! [X2] : tptp1(tptp0(tptp1(X1,tptp0(X2))),tptp0(tptp1(tptp0(X1),tptp0(X2)))) = X2).
|