Prover9 Examples: Ternary Relations in Lattices

These theorems are based on the following paper. This work is part of an ongoing project of Padmanabhan, Veroff, and McCune.
A implies B.
prover9 -f head.in ab.in > ab.out ; ### ( ab.out.xml )
B implies C.
prover9 -f head.in bc.in > bc.out ; ### ( bc.out.xml )
B implies CS.
prover9 -f head.in bcs.in > bcs.out ; ### ( bcs.out.xml )
C implies D.
prover9 -f head.in cd.in > cd.out ; ### ( cd.out.xml )
CS implies D.
prover9 -f head.in csd.in > csd.out ; ### ( csd.out.xml )
Theorem 2, 1 implies 2.
prover9 -f head.in t2_12.in > t2_12.out ; ### ( t2_12.out.xml )
Theorem 2, 2 implies 3.
prover9 -f head.in t2_23.in > t2_23.out ; ### ( t2_23.out.xml )
Theorem 3, 1 implies 2.
prover9 -f head.in t3_12.in > t3_12.out ; ### ( t3_12.out.xml )
Theorem 4, 1 implies 2.
prover9 -f head.in t4_12.in > t4_12.out ; ### ( t4_12.out.xml )