List of theorems

List of theorems in general/Connectivity_for_betweenness.gh:

(→ (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D)) (∃ c′ (∃ d′ (∃ b′ (∃ b″ (∧ (∧ (∧ (∧ (∧ (between A D c′) (≡ D c′ C D)) (∧ (between A C d′) (≡ C d′ C D))) (∧ (between A c′ b′) (≡ c′ b′ C B))) (∧ (between A d′ b″) (≡ d′ b″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))))))))
(→ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (between B D C′))
(→ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (between B″ D′ C))
(→ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (≡ D C′ D′ C))
(→ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (≡ B C′ B″ C))
(→ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (between A B C′))
(→ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (between B C′ B′))
(→ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (between A C B″))
(→ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (between B″ C B))
(→ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (≡ B B′ B″ B))
(→ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (between A B D′))
(→ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (= B″ B′))
(→ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (between B C D′))
(→ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (between B′ C′ D))
(→ (∧ (= B″ B′) (≡ B C′ B″ C)) (≡ B C′ B′ C))
(→ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (≡ B C′ B′ C))
(→ (∧ (¬ (= B C)) (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D)))) (≡ C′ D′ C D))
(→ (∧ (= B C) (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D)))) (= B′ C′))
(→ (∧ (∧ (= B″ B′) (= B′ C′)) (≡ D′ B″ D B)) (≡ C′ D′ B D))
(→ (∧ (∧ (∧ (= B″ B′) (= B′ C′)) (≡ D′ B″ D B)) (= B C)) (≡ C′ D′ C D))
(→ (∧ (= B C) (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D)))) (≡ C′ D′ C D))
(→ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (≡ C′ D′ C D))
(→ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∃ e (∧ (between C e C′) (between D e D′))))
(→ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∃ e (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C e C′) (between D e D′)))))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (≡ E C E C′))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (≡ E D E D′))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∃ r (∃ p (∃ q (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C p) (≡ C p C D′))) (∧ (between D′ C r) (≡ C r C E))) (∧ (between p r q) (≡ r q r p)))))))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (= C D′)) (= D′ C′))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (= C D′)) (= C C′))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′))) (¬ (= C D′)))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′))) (between P C E))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′))) (≡ R P E D′))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′))) (≡ R Q E D))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′))) (≡ D′ D P Q))
(→ (∧ (= D′ E) (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′)))) (= E D))
(→ (∧ (= D′ E) (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′)))) (= D′ D))
(→ (∧ (= D′ E) (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′)))) (= P Q))
(→ (∧ (= D′ E) (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′)))) (≡ C Q C D))
(→ (∧ (¬ (= D′ E)) (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′)))) (≡ C Q C D))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′))) (≡ C Q C D))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′))) (≡ C P C Q))
(→ (∧ (≡ C R C E) (= R C)) (= C E))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (= R C)) (= C E))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (= R C)) (= E C′))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (= R C)) (= C C′))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′))) (¬ (= R C)))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′))) (≡ D′ P D′ Q))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′))) (between C D′ B′))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′))) (≡ B′ P B′ Q))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′))) (≡ B P B Q))
(→ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (between B′ C B))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (= B B′)) (= C C′))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′))) (¬ (= B B′)))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′))) (≡ C′ P C′ Q))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′))) (≡ P P P Q))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′))) (= P Q))
(→ (∧ (= x y) (≡ x y z w)) (= z w))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (¬ (= C C′))) (= D D′))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (∨ (= C C′) (= D D′)))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (= C C′)) (between A D C))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (= D D′)) (between A C D))
(→ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (∧ (between A D C′) (≡ D C′ C D)) (∧ (between A C D′) (≡ C D′ C D))) (∧ (between A C′ B′) (≡ C′ B′ C B))) (∧ (between A D′ B″) (≡ D′ B″ D B))) (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))) (∧ (between C E C′) (between D E D′))) (∧ (between C′ C P) (≡ C P C D′))) (∧ (between D′ C R) (≡ C R C E))) (∧ (between P R Q) (≡ R Q R P))) (∨ (between A C D) (between A D C)))
(→ (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D)) (∨ (between A C D) (between A D C)))