Prover9 Examples: Hao Wang Problems

These are the three ExQ challenge from the paper

Hao Wang, "Formalization and automatic theorem proving", in Wayne A. Kalenich (ed.), Proceedings of IFIP Congress 65, pp. 51--58, Washington, D.C., 1965.

There are two versions of each.

With equality axiomatized (resolution with equality axioms).

Wang 1

prover9 -f wang.in wang1.in > wang1.out ; ### ( wang1.out.xml )

Wang 2

prover9 -f wang.in wang2.in > wang2.out ; ### ( wang2.out.xml )

Wang 3

prover9 -f wang.in wang3.in > wang3.out ; ### ( wang3.out.xml )

With equality built in (paramodulation and demodulation).

Wang 1

prover9 -f wang-eq.in wang1-eq.in > wang1-eq.out ; ### ( wang1-eq.out.xml )

Wang 2

prover9 -f wang-eq.in wang2-eq.in > wang2-eq.out ; ### ( wang2-eq.out.xml )

Wang 3

prover9 -f wang-eq.in wang3-eq.in > wang3-eq.out ; ### ( wang3-eq.out.xml )