Prover9 Examples: FOF Reduction

These examples use the program FOF-prover9, which is a variant of prover9 that attempts to reduce a problem to independent subproblems before calling the ordinary Prover9 search code.

Most of these examples are from TPTP v3.0.1.

Note that the XML proof files do not show the problem reduction; they show only the refutations of the subproblems.

fof-prover9 -f andrews.in > andrews.out ; ### ( andrews.out.xml )

fof-prover9 -f ALG033+1.in > ALG033+1.out ; ### ( ALG033+1.out.xml )

fof-prover9 -f ALG043+1.in > ALG043+1.out ; ### ( ALG043+1.out.xml )

fof-prover9 -f ALG189+1.in > ALG189+1.out ; ### ( ALG189+1.out.xml )

fof-prover9 -f GEO146+1.in > GEO146+1.out ; ### ( GEO146+1.out.xml )

fof-prover9 -f GEO147+1.in > GEO147+1.out ; ### ( GEO147+1.out.xml )

fof-prover9 -f MGT025+1.in > MGT025+1.out ; ### ( MGT025+1.out.xml )

fof-prover9 -f MGT063+1.in > MGT063+1.out ; ### ( MGT063+1.out.xml )

fof-prover9 -f SET587+3.in > SET587+3.out ; ### ( SET587+3.out.xml )

fof-prover9 -f SET593+3.in > SET593+3.out ; ### ( SET593+3.out.xml )

fof-prover9 -f SET598+3.in > SET598+3.out ; ### ( SET598+3.out.xml )

fof-prover9 -f SET660+3.in > SET660+3.out ; ### ( SET660+3.out.xml )

fof-prover9 -f SET667+3.in > SET667+3.out ; ### ( SET667+3.out.xml )

fof-prover9 -f SET668+3.in > SET668+3.out ; ### ( SET668+3.out.xml )

fof-prover9 -f SWC258+1.in > SWC258+1.out ; ### ( SWC258+1.out.xml )

fof-prover9 -f SWC339+1.in > SWC339+1.out ; ### ( SWC339+1.out.xml )

fof-prover9 -f SYN551+2.in > SYN551+2.out ; ### ( SYN551+2.out.xml )