Prover9 Examples: FOF Reduction

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 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 SYN551+2.in > SYN551+2.out ; ### ( SYN551+2.out.xml )