# File prover.in.0 # Proof obligation in the TPTP3/TSTP prover syntax, generated with haRVey. # compiled with: eprover -l 4 --tstp-in --tstp-out -xAuto -tAuto --processed-clauses-limit=9 prover.in.0 1> prover.ou.0 2> prover.st.0 fof(haRVey_clue1, axiom, ~('p'('0x7312a8'))). fof(haRVey_clue2, axiom, (![Xvar_1] : ('p'(Xvar_1)))).