I am working on proving the following question:
| ∀x [Dodec(x) → LeftOf(x, a)] | ∀x [Tet(x) → RightOf(x, a)] |––– | ∀x [SameCol(x, a) → Cube(x)]
The question has the following rules:
[…] give a proof that uses Ana Con but only where the premises and conclusions of the citation are literals (including ⊥). You may use Taut Con but do not use FO Con in any of the proofs.
I have completed the following two proofs, but neither are accepted by the program, because it is being very picky on Ana Con:
However, I can't think of any other way to prove this that would make the program happy. What other methods could I try?