Automated proofs for the paper:
"Complementation in representable theories of region-based space" to appear in Notre Dame Journal of Formal Logic (NDJFL)

---

---

Section 5.1: Mereological closure operations

Lemma 5.1. Proof output for (M-I) with input file.

Lemma 5.2. Proof output for (M-S) with input file.

Lemma 5.3. Proof that (M-C) is sufficient to prove that L is uniquely complemented and thus Boolean with input file;
Proof that if L is Boolean and thus uniquely complemented, (M-C) must hold with input file.

Lemma 5.4. Proof output for (O-Ext) with input file, this is not really new, since it is well known that overlap is extensional in contact algebras defined over Boolean lattices.

---

Section 5.2: Topological closure operations

---

Section 5.2.1: Topological complement operation

Lemma 5.9. Proof output for (C4) with input file.

Lemma 5.10. Proof output for (Ext) with input file.

Lemma 5.11. Proof output for (-Con) with input file.

Lemma 5.12. Proof output for (Int) with input file.

Lemma 5.14. Example satisfying (Uni) but not (C5) with input file.

Lemma 5.15. Example satisfying (Uni) but not (C5) with input file.

---

Section 5.2.2: Quasi-topological complement operation

Lemma 5.16. Proof output for (Con) with input file.

Lemma 5.17. Proof output for (Int) with input file.

Lemma 5.18. Proof output for (Uni) with input file.

Lemma 5.19. Example satisfying (Uni) but not (C5) with input file.

---

Section 6.2: On spatially representable WCAs with distributive models

Lemma 6.4. Proof output showing that (-Con) and (-C4) cannot hold in a EWBCA with input file.

Lemma 6.8. Proof output showing that (Atom) cannot hold in a WBCA' with input file.

---