Prover9 Examples: Miscellany

This is a collection of miscellaneous Prover9 examples.

Distributivity from a nonstandard Boolean algebra basis

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

Orthomodular lattice problem

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

A lemma in Robbins algebra

prover9 -f RBA-2.in > RBA-2.out ; ### ( RBA-2.out.xml )

Existence of a fixed point combinator from B and W.

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

Fixed point property from S and K

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

Reflexivity from EC single axiom XCB

prover9 -f xcb-reflex.in > xcb-reflex.out ; ### ( xcb-reflex.out.xml )

Schubert's Steamroller

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

A trivial set theory problem

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

A hardware verification problem from TPTP

prover9 -f HWV006-1.in > HWV006-1.out ; ### ( HWV006-1.out.xml )

A problem from Vladimir Lifschitz

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