%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : GEO222+3 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n016.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 06:31:18 EDT 2022 % Result : Theorem 20.51s 20.73s % Output : Proof 20.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GEO222+3 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n016.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sat Jun 18 11:16:52 EDT 2022 % 0.13/0.34 % CPUTime : % 20.51/20.73 % SZS status Theorem % 20.51/20.73 (* PROOF-FOUND *) % 20.51/20.73 (* BEGIN-PROOF *) % 20.51/20.73 % SZS output start Proof % 20.51/20.73 1. (convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) (-. (convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) ### Axiom % 20.51/20.73 2. (convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) (-. (convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) ### Axiom % 20.51/20.73 3. (-. (convergent_lines T_0 T_0)) (convergent_lines T_0 T_0) ### Axiom % 20.51/20.73 4. (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) ### Axiom % 20.51/20.73 5. (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) ### Axiom % 20.51/20.73 6. (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) ### Axiom % 20.51/20.73 7. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1)) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) ### Axiom % 20.51/20.73 8. (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1)) ### All 7 % 20.51/20.73 9. (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) ### Axiom % 20.51/20.73 10. (convergent_lines (orthogonal_through_point T_0 T_1) T_0) (-. (convergent_lines (orthogonal_through_point T_0 T_1) T_0)) ### Axiom % 20.51/20.73 11. (((-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) /\ (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0))) => (-. (convergent_lines (orthogonal_through_point T_0 T_1) T_0))) (convergent_lines (orthogonal_through_point T_0 T_1) T_0) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) ### DisjTree 8 9 10 % 20.51/20.73 12. (All N, (((-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) /\ (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N))) => (-. (convergent_lines (orthogonal_through_point T_0 T_1) N)))) (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) (convergent_lines (orthogonal_through_point T_0 T_1) T_0) ### All 11 % 20.51/20.73 13. (All M, (All N, (((-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) M)) /\ (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N))) => (-. (convergent_lines M N))))) (convergent_lines (orthogonal_through_point T_0 T_1) T_0) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) ### All 12 % 20.51/20.73 14. (-. (-. (convergent_lines (orthogonal_through_point T_0 T_1) T_0))) (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) (All M, (All N, (((-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) M)) /\ (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N))) => (-. (convergent_lines M N))))) ### NotNot 13 % 20.51/20.73 15. (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0) ### Axiom % 20.51/20.74 16. (-. (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0))) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) ### NotNot 15 % 20.51/20.74 17. (-. ((-. (convergent_lines (orthogonal_through_point T_0 T_1) T_0)) /\ (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)))) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (All M, (All N, (((-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) M)) /\ (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N))) => (-. (convergent_lines M N))))) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) ### NotAnd 14 16 % 20.51/20.74 18. (All M, (-. ((-. (convergent_lines (orthogonal_through_point T_0 T_1) M)) /\ (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) M))))) (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) (All M, (All N, (((-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) M)) /\ (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N))) => (-. (convergent_lines M N))))) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) ### All 17 % 20.51/20.74 19. (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (All M, (All N, (((-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) M)) /\ (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N))) => (-. (convergent_lines M N))))) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) ### All 18 % 20.51/20.74 20. (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) (All M, (All N, (((-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) M)) /\ (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N))) => (-. (convergent_lines M N))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) ### All 19 % 20.51/20.74 21. (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All M, (All N, (((-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) M)) /\ (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N))) => (-. (convergent_lines M N))))) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) ### All 20 % 20.51/20.74 22. (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) ### All 21 % 20.51/20.74 23. (apart_point_and_line T_1 T_0) (-. (apart_point_and_line T_1 T_0)) ### Axiom % 20.51/20.74 24. (distinct_lines T_0 (orthogonal_through_point T_0 T_1)) (-. (distinct_lines T_0 (orthogonal_through_point T_0 T_1))) ### Axiom % 20.51/20.74 25. (convergent_lines T_0 (orthogonal_through_point T_0 T_1)) (-. (convergent_lines T_0 (orthogonal_through_point T_0 T_1))) ### Axiom % 20.51/20.74 26. (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) ### Axiom % 20.51/20.74 27. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) ### Axiom % 20.58/20.78 28. (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1)) ### Axiom % 20.58/20.78 29. ((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1)) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) ### And 28 % 20.58/20.78 30. (-. (unorthogonal_lines T_0 (orthogonal_through_point T_0 T_1))) (unorthogonal_lines T_0 (orthogonal_through_point T_0 T_1)) ### Axiom % 20.58/20.78 31. ((convergent_lines T_0 (orthogonal_through_point T_0 T_1)) /\ (unorthogonal_lines T_0 (orthogonal_through_point T_0 T_1))) (-. (unorthogonal_lines T_0 (orthogonal_through_point T_0 T_1))) ### And 30 % 20.58/20.78 32. (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) => (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1)) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) \/ ((convergent_lines T_0 (orthogonal_through_point T_0 T_1)) /\ (unorthogonal_lines T_0 (orthogonal_through_point T_0 T_1))))) (-. (unorthogonal_lines T_0 (orthogonal_through_point T_0 T_1))) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) ### DisjTree 26 27 29 31 % 20.58/20.78 33. (All N, (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) => (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N)) \/ ((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) (-. (unorthogonal_lines T_0 (orthogonal_through_point T_0 T_1))) ### All 32 % 20.58/20.78 34. (-. (convergent_lines T_0 T_0)) (convergent_lines T_0 T_0) ### Axiom % 20.58/20.78 35. ((convergent_lines T_0 T_0) /\ (unorthogonal_lines T_0 T_0)) (-. (convergent_lines T_0 T_0)) ### And 34 % 20.58/20.78 36. (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0) ### Axiom % 20.58/20.78 37. ((convergent_lines (orthogonal_through_point T_0 T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) ### And 36 % 20.58/20.78 38. (((convergent_lines T_0 (orthogonal_through_point T_0 T_1)) /\ (unorthogonal_lines T_0 (orthogonal_through_point T_0 T_1))) => (((convergent_lines T_0 T_0) /\ (unorthogonal_lines T_0 T_0)) \/ ((convergent_lines (orthogonal_through_point T_0 T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)))) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (-. (convergent_lines T_0 T_0)) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All N, (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) => (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N)) \/ ((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N))))) (convergent_lines T_0 (orthogonal_through_point T_0 T_1)) ### DisjTree 25 33 35 37 % 20.58/20.78 39. (All N, (((convergent_lines T_0 (orthogonal_through_point T_0 T_1)) /\ (unorthogonal_lines T_0 (orthogonal_through_point T_0 T_1))) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines (orthogonal_through_point T_0 T_1) N) /\ (unorthogonal_lines (orthogonal_through_point T_0 T_1) N))))) (convergent_lines T_0 (orthogonal_through_point T_0 T_1)) (All N, (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) => (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N)) \/ ((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) (-. (convergent_lines T_0 T_0)) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) ### All 38 % 20.58/20.78 40. (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (-. (convergent_lines T_0 T_0)) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All N, (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) => (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N)) \/ ((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N))))) (convergent_lines T_0 (orthogonal_through_point T_0 T_1)) ### All 39 % 20.58/20.78 41. ((distinct_lines T_0 (orthogonal_through_point T_0 T_1)) => (convergent_lines T_0 (orthogonal_through_point T_0 T_1))) (All N, (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) => (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N)) \/ ((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) (-. (convergent_lines T_0 T_0)) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (distinct_lines T_0 (orthogonal_through_point T_0 T_1)) ### Imply 24 40 % 20.58/20.81 42. (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (distinct_lines T_0 (orthogonal_through_point T_0 T_1)) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (-. (convergent_lines T_0 T_0)) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All N, (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) => (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N)) \/ ((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N))))) ### All 41 % 20.58/20.81 43. (-. (apart_point_and_line T_1 (orthogonal_through_point T_0 T_1))) (apart_point_and_line T_1 (orthogonal_through_point T_0 T_1)) ### Axiom % 20.58/20.81 44. ((apart_point_and_line T_1 T_0) => ((distinct_lines T_0 (orthogonal_through_point T_0 T_1)) \/ (apart_point_and_line T_1 (orthogonal_through_point T_0 T_1)))) (-. (apart_point_and_line T_1 (orthogonal_through_point T_0 T_1))) (All N, (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) => (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N)) \/ ((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) (-. (convergent_lines T_0 T_0)) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (apart_point_and_line T_1 T_0) ### DisjTree 23 42 43 % 20.58/20.81 45. (All Z, ((apart_point_and_line T_1 T_0) => ((distinct_lines T_0 Z) \/ (apart_point_and_line T_1 Z)))) (apart_point_and_line T_1 T_0) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (-. (convergent_lines T_0 T_0)) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All N, (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) => (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N)) \/ ((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N))))) (-. (apart_point_and_line T_1 (orthogonal_through_point T_0 T_1))) ### All 44 % 20.58/20.81 46. (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) (-. (apart_point_and_line T_1 (orthogonal_through_point T_0 T_1))) (All N, (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) => (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N)) \/ ((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (convergent_lines T_0 T_0)) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (apart_point_and_line T_1 T_0) (All Z, ((apart_point_and_line T_1 T_0) => ((distinct_lines T_0 Z) \/ (apart_point_and_line T_1 Z)))) ### All 45 % 20.58/20.81 47. (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All Z, ((apart_point_and_line T_1 T_0) => ((distinct_lines T_0 Z) \/ (apart_point_and_line T_1 Z)))) (apart_point_and_line T_1 T_0) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (-. (convergent_lines T_0 T_0)) (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All N, (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) => (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N)) \/ ((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N))))) (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) ### All 46 % 20.58/20.81 48. (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) (All N, (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) => (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N)) \/ ((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (convergent_lines T_0 T_0)) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (apart_point_and_line T_1 T_0) (All Z, ((apart_point_and_line T_1 T_0) => ((distinct_lines T_0 Z) \/ (apart_point_and_line T_1 Z)))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) ### All 47 % 20.58/20.81 49. (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All Z, ((apart_point_and_line T_1 T_0) => ((distinct_lines T_0 Z) \/ (apart_point_and_line T_1 Z)))) (apart_point_and_line T_1 T_0) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (-. (convergent_lines T_0 T_0)) (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All N, (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) => (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N)) \/ ((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N))))) ### All 48 % 20.58/20.82 50. ((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) (All N, (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) => (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N)) \/ ((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (convergent_lines T_0 T_0)) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (apart_point_and_line T_1 T_0) (All Z, ((apart_point_and_line T_1 T_0) => ((distinct_lines T_0 Z) \/ (apart_point_and_line T_1 Z)))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) ### And 49 % 20.58/20.82 51. (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) => (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) \/ ((convergent_lines T_0 T_0) /\ (unorthogonal_lines T_0 T_0)))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All Z, ((apart_point_and_line T_1 T_0) => ((distinct_lines T_0 Z) \/ (apart_point_and_line T_1 Z)))) (apart_point_and_line T_1 T_0) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (-. (convergent_lines T_0 T_0)) (All N, (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) => (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N)) \/ ((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) ### DisjTree 6 22 50 35 % 20.58/20.82 52. (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All N, (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0)) => (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N)) \/ ((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N))))) (-. (convergent_lines T_0 T_0)) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (apart_point_and_line T_1 T_0) (All Z, ((apart_point_and_line T_1 T_0) => ((distinct_lines T_0 Z) \/ (apart_point_and_line T_1 Z)))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) ### All 51 % 20.58/20.82 53. (All M, (All N, (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) M) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) M)) => (((convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) /\ (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All Z, ((apart_point_and_line T_1 T_0) => ((distinct_lines T_0 Z) \/ (apart_point_and_line T_1 Z)))) (apart_point_and_line T_1 T_0) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (-. (convergent_lines T_0 T_0)) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) ### All 52 % 20.58/20.82 54. (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (-. (convergent_lines T_0 T_0)) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (apart_point_and_line T_1 T_0) (All Z, ((apart_point_and_line T_1 T_0) => ((distinct_lines T_0 Z) \/ (apart_point_and_line T_1 Z)))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) ### All 53 % 20.58/20.82 55. (All Y, (All Z, ((apart_point_and_line T_1 Y) => ((distinct_lines Y Z) \/ (apart_point_and_line T_1 Z))))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (apart_point_and_line T_1 T_0) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (-. (convergent_lines T_0 T_0)) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) ### All 54 % 20.67/20.85 56. (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (-. (convergent_lines T_0 T_0)) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (apart_point_and_line T_1 T_0) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) ### All 55 % 20.67/20.85 57. (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1)) ### Axiom % 20.67/20.85 58. (convergent_lines (orthogonal_through_point T_0 T_1) T_0) (-. (convergent_lines (orthogonal_through_point T_0 T_1) T_0)) ### Axiom % 20.67/20.85 59. (-. (convergent_lines (orthogonal_through_point T_0 T_1) (orthogonal_through_point T_0 T_1))) (convergent_lines (orthogonal_through_point T_0 T_1) (orthogonal_through_point T_0 T_1)) ### Axiom % 20.67/20.85 60. (-. (convergent_lines T_0 (orthogonal_through_point T_0 T_1))) (convergent_lines T_0 (orthogonal_through_point T_0 T_1)) ### Axiom % 20.67/20.85 61. ((convergent_lines (orthogonal_through_point T_0 T_1) T_0) => ((convergent_lines (orthogonal_through_point T_0 T_1) (orthogonal_through_point T_0 T_1)) \/ (convergent_lines T_0 (orthogonal_through_point T_0 T_1)))) (-. (convergent_lines T_0 (orthogonal_through_point T_0 T_1))) (-. (convergent_lines (orthogonal_through_point T_0 T_1) (orthogonal_through_point T_0 T_1))) (convergent_lines (orthogonal_through_point T_0 T_1) T_0) ### DisjTree 58 59 60 % 20.67/20.85 62. (All Z, ((convergent_lines (orthogonal_through_point T_0 T_1) T_0) => ((convergent_lines (orthogonal_through_point T_0 T_1) Z) \/ (convergent_lines T_0 Z)))) (convergent_lines (orthogonal_through_point T_0 T_1) T_0) (-. (convergent_lines (orthogonal_through_point T_0 T_1) (orthogonal_through_point T_0 T_1))) (-. (convergent_lines T_0 (orthogonal_through_point T_0 T_1))) ### All 61 % 20.67/20.85 63. (unorthogonal_lines T_0 (orthogonal_through_point T_0 T_1)) (-. (unorthogonal_lines T_0 (orthogonal_through_point T_0 T_1))) ### Axiom % 20.67/20.85 64. (((convergent_lines T_0 (orthogonal_through_point T_0 T_1)) /\ (unorthogonal_lines T_0 (orthogonal_through_point T_0 T_1))) => (((convergent_lines T_0 T_0) /\ (unorthogonal_lines T_0 T_0)) \/ ((convergent_lines (orthogonal_through_point T_0 T_1) T_0) /\ (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)))) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (-. (convergent_lines T_0 T_0)) (unorthogonal_lines T_0 (orthogonal_through_point T_0 T_1)) (-. (convergent_lines (orthogonal_through_point T_0 T_1) (orthogonal_through_point T_0 T_1))) (convergent_lines (orthogonal_through_point T_0 T_1) T_0) (All Z, ((convergent_lines (orthogonal_through_point T_0 T_1) T_0) => ((convergent_lines (orthogonal_through_point T_0 T_1) Z) \/ (convergent_lines T_0 Z)))) ### DisjTree 62 63 35 37 % 20.67/20.85 65. (All N, (((convergent_lines T_0 (orthogonal_through_point T_0 T_1)) /\ (unorthogonal_lines T_0 (orthogonal_through_point T_0 T_1))) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines (orthogonal_through_point T_0 T_1) N) /\ (unorthogonal_lines (orthogonal_through_point T_0 T_1) N))))) (All Z, ((convergent_lines (orthogonal_through_point T_0 T_1) T_0) => ((convergent_lines (orthogonal_through_point T_0 T_1) Z) \/ (convergent_lines T_0 Z)))) (convergent_lines (orthogonal_through_point T_0 T_1) T_0) (-. (convergent_lines (orthogonal_through_point T_0 T_1) (orthogonal_through_point T_0 T_1))) (unorthogonal_lines T_0 (orthogonal_through_point T_0 T_1)) (-. (convergent_lines T_0 T_0)) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) ### All 64 % 20.67/20.85 66. (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (-. (convergent_lines T_0 T_0)) (unorthogonal_lines T_0 (orthogonal_through_point T_0 T_1)) (-. (convergent_lines (orthogonal_through_point T_0 T_1) (orthogonal_through_point T_0 T_1))) (convergent_lines (orthogonal_through_point T_0 T_1) T_0) (All Z, ((convergent_lines (orthogonal_through_point T_0 T_1) T_0) => ((convergent_lines (orthogonal_through_point T_0 T_1) Z) \/ (convergent_lines T_0 Z)))) ### All 65 % 20.67/20.85 67. (All X, (-. (convergent_lines X X))) (All Z, ((convergent_lines (orthogonal_through_point T_0 T_1) T_0) => ((convergent_lines (orthogonal_through_point T_0 T_1) Z) \/ (convergent_lines T_0 Z)))) (convergent_lines (orthogonal_through_point T_0 T_1) T_0) (unorthogonal_lines T_0 (orthogonal_through_point T_0 T_1)) (-. (convergent_lines T_0 T_0)) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) ### All 66 % 20.67/20.85 68. ((distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) => ((apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) \/ ((apart_point_and_line T_1 T_0) \/ ((unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1)) \/ (unorthogonal_lines T_0 (orthogonal_through_point T_0 T_1)))))) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (convergent_lines (orthogonal_through_point T_0 T_1) T_0) (All Z, ((convergent_lines (orthogonal_through_point T_0 T_1) T_0) => ((convergent_lines (orthogonal_through_point T_0 T_1) Z) \/ (convergent_lines T_0 Z)))) (All X, (-. (convergent_lines X X))) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (-. (convergent_lines T_0 T_0)) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) ### DisjTree 4 5 56 57 67 % 20.67/20.86 69. (All N, ((distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) => ((apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) \/ ((apart_point_and_line T_1 T_0) \/ ((unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) \/ (unorthogonal_lines T_0 N)))))) (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (-. (convergent_lines T_0 T_0)) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (-. (unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) (orthogonal_through_point T_0 T_1))) (All X, (-. (convergent_lines X X))) (All Z, ((convergent_lines (orthogonal_through_point T_0 T_1) T_0) => ((convergent_lines (orthogonal_through_point T_0 T_1) Z) \/ (convergent_lines T_0 Z)))) (convergent_lines (orthogonal_through_point T_0 T_1) T_0) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) ### All 68 % 20.67/20.86 70. (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (convergent_lines (orthogonal_through_point T_0 T_1) T_0) (All Z, ((convergent_lines (orthogonal_through_point T_0 T_1) T_0) => ((convergent_lines (orthogonal_through_point T_0 T_1) Z) \/ (convergent_lines T_0 Z)))) (All X, (-. (convergent_lines X X))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (-. (convergent_lines T_0 T_0)) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All N, ((distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) => ((apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) \/ ((apart_point_and_line T_1 T_0) \/ ((unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) \/ (unorthogonal_lines T_0 N)))))) ### All 69 % 20.67/20.86 71. (All Y, (All Z, ((convergent_lines (orthogonal_through_point T_0 T_1) Y) => ((convergent_lines (orthogonal_through_point T_0 T_1) Z) \/ (convergent_lines Y Z))))) (All N, ((distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) => ((apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) \/ ((apart_point_and_line T_1 T_0) \/ ((unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) \/ (unorthogonal_lines T_0 N)))))) (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (-. (convergent_lines T_0 T_0)) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All X, (-. (convergent_lines X X))) (convergent_lines (orthogonal_through_point T_0 T_1) T_0) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) ### All 70 % 20.67/20.86 72. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (convergent_lines (orthogonal_through_point T_0 T_1) T_0) (All X, (-. (convergent_lines X X))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (-. (convergent_lines T_0 T_0)) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All N, ((distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) => ((apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) \/ ((apart_point_and_line T_1 T_0) \/ ((unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) \/ (unorthogonal_lines T_0 N)))))) ### All 71 % 20.70/20.89 73. (-. (-. (convergent_lines (orthogonal_through_point T_0 T_1) T_0))) (All N, ((distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) => ((apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) \/ ((apart_point_and_line T_1 T_0) \/ ((unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) \/ (unorthogonal_lines T_0 N)))))) (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (-. (convergent_lines T_0 T_0)) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All X, (-. (convergent_lines X X))) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) ### NotNot 72 % 20.70/20.89 74. (-. ((-. (convergent_lines (orthogonal_through_point T_0 T_1) T_0)) /\ (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (All X, (-. (convergent_lines X X))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (-. (convergent_lines T_0 T_0)) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All N, ((distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) => ((apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) \/ ((apart_point_and_line T_1 T_0) \/ ((unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) \/ (unorthogonal_lines T_0 N)))))) ### NotAnd 73 16 % 20.70/20.89 75. (All M, (-. ((-. (convergent_lines (orthogonal_through_point T_0 T_1) M)) /\ (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) M))))) (All N, ((distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) => ((apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) \/ ((apart_point_and_line T_1 T_0) \/ ((unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) \/ (unorthogonal_lines T_0 N)))))) (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (-. (convergent_lines T_0 T_0)) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All X, (-. (convergent_lines X X))) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) ### All 74 % 20.70/20.89 76. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) (-. (unorthogonal_lines (orthogonal_through_point T_0 T_1) T_0)) (All X, (-. (convergent_lines X X))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (-. (convergent_lines T_0 T_0)) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All N, ((distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) => ((apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) \/ ((apart_point_and_line T_1 T_0) \/ ((unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) \/ (unorthogonal_lines T_0 N)))))) ### All 75 % 20.70/20.89 77. (All N, ((distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) => ((apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) \/ ((apart_point_and_line T_1 T_0) \/ ((unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) \/ (unorthogonal_lines T_0 N)))))) (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (-. (convergent_lines T_0 T_0)) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All X, (-. (convergent_lines X X))) (All L, (-. (unorthogonal_lines (orthogonal_through_point L T_1) L))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) ### All 76 % 20.70/20.90 78. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (-. (convergent_lines X X))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (-. (convergent_lines T_0 T_0)) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All N, ((distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) => ((apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) \/ ((apart_point_and_line T_1 T_0) \/ ((unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) \/ (unorthogonal_lines T_0 N)))))) ### All 77 % 20.70/20.90 79. (All M, (All N, ((distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) M) => ((apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) \/ ((apart_point_and_line T_1 M) \/ ((unorthogonal_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) N) \/ (unorthogonal_lines M N))))))) (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (-. (convergent_lines T_0 T_0)) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) ### All 78 % 20.70/20.90 80. (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line T_1 L) \/ ((apart_point_and_line T_1 M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N)))))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (-. (convergent_lines X X))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (-. (convergent_lines T_0 T_0)) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) ### All 79 % 20.70/20.90 81. (All A, (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line A L) \/ ((apart_point_and_line A M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N))))))))) (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (-. (convergent_lines T_0 T_0)) (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) ### All 80 % 20.70/20.90 82. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (-. (convergent_lines X X))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All Y, ((distinct_lines T_0 Y) => (convergent_lines T_0 Y))) (-. (convergent_lines T_0 T_0)) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All A, (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line A L) \/ ((apart_point_and_line A M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N))))))))) ### All 81 % 20.70/20.90 83. (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All A, (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line A L) \/ ((apart_point_and_line A M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N))))))))) (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (-. (convergent_lines T_0 T_0)) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) ### All 82 % 20.70/20.90 84. ((convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) => ((convergent_lines T_0 T_0) \/ (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (-. (convergent_lines X X))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (All A, (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line A L) \/ ((apart_point_and_line A M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N))))))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (-. (convergent_lines T_0 T_0)) (convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) ### DisjTree 2 3 83 % 20.70/20.90 85. (All Z, ((convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) => ((convergent_lines T_0 Z) \/ (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) Z)))) (convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) (-. (convergent_lines T_0 T_0)) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All A, (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line A L) \/ ((apart_point_and_line A M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N))))))))) (distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) ### All 84 % 20.70/20.90 86. (-. (convergent_lines T_0 T_0)) (convergent_lines T_0 T_0) ### Axiom % 20.70/20.90 87. ((convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) => ((distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) T_0) \/ (convergent_lines T_0 T_0))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (-. (convergent_lines X X))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (All A, (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line A L) \/ ((apart_point_and_line A M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N))))))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (-. (convergent_lines T_0 T_0)) (All Z, ((convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) => ((convergent_lines T_0 Z) \/ (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) Z)))) (convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) ### DisjTree 1 85 86 % 20.70/20.90 88. (All Z, ((convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) => ((distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) Z) \/ (convergent_lines T_0 Z)))) (convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) (All Z, ((convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) => ((convergent_lines T_0 Z) \/ (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) Z)))) (-. (convergent_lines T_0 T_0)) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All A, (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line A L) \/ ((apart_point_and_line A M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N))))))))) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) ### All 87 % 20.70/20.92 89. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (-. (convergent_lines X X))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (All A, (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line A L) \/ ((apart_point_and_line A M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N))))))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All Z, ((convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) => ((convergent_lines T_0 Z) \/ (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) Z)))) (convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) (All Z, ((convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) => ((distinct_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) Z) \/ (convergent_lines T_0 Z)))) ### All 88 % 20.70/20.92 90. (All Y, (All Z, ((convergent_lines T_0 Y) => ((distinct_lines Y Z) \/ (convergent_lines T_0 Z))))) (convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) (All Z, ((convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) => ((convergent_lines T_0 Z) \/ (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) Z)))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All A, (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line A L) \/ ((apart_point_and_line A M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N))))))))) (-. (apart_point_and_line T_1 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) ### All 89 % 20.70/20.92 91. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (-. (convergent_lines X X))) (All L, (-. (apart_point_and_line T_1 (orthogonal_through_point L T_1)))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All A, (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line A L) \/ ((apart_point_and_line A M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N))))))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All Z, ((convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) => ((convergent_lines T_0 Z) \/ (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) Z)))) (convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) (All Y, (All Z, ((convergent_lines T_0 Y) => ((distinct_lines Y Z) \/ (convergent_lines T_0 Z))))) ### All 90 % 20.70/20.92 92. (All A, (All L, (-. (apart_point_and_line A (orthogonal_through_point L A))))) (All Y, (All Z, ((convergent_lines T_0 Y) => ((distinct_lines Y Z) \/ (convergent_lines T_0 Z))))) (convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) (All Z, ((convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) => ((convergent_lines T_0 Z) \/ (convergent_lines (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1) Z)))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All A, (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line A L) \/ ((apart_point_and_line A M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) ### All 91 % 20.70/20.92 93. (All Y, (All Z, ((convergent_lines T_0 Y) => ((convergent_lines T_0 Z) \/ (convergent_lines Y Z))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (-. (convergent_lines X X))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All A, (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line A L) \/ ((apart_point_and_line A M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N))))))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) (All Y, (All Z, ((convergent_lines T_0 Y) => ((distinct_lines Y Z) \/ (convergent_lines T_0 Z))))) (All A, (All L, (-. (apart_point_and_line A (orthogonal_through_point L A))))) ### All 92 % 20.70/20.92 94. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All A, (All L, (-. (apart_point_and_line A (orthogonal_through_point L A))))) (convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All A, (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line A L) \/ ((apart_point_and_line A M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All Y, (All Z, ((convergent_lines T_0 Y) => ((convergent_lines T_0 Z) \/ (convergent_lines Y Z))))) ### All 93 % 20.70/20.92 95. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (-. (convergent_lines X X))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All A, (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line A L) \/ ((apart_point_and_line A M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N))))))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)) (All A, (All L, (-. (apart_point_and_line A (orthogonal_through_point L A))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) ### All 94 % 20.70/20.92 96. (-. (-. (convergent_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1)))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All A, (All L, (-. (apart_point_and_line A (orthogonal_through_point L A))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All A, (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line A L) \/ ((apart_point_and_line A M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) ### NotNot 95 % 20.70/20.92 97. (-. (parallel_lines T_0 (orthogonal_through_point (orthogonal_through_point T_0 T_1) T_1))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (-. (convergent_lines X X))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All A, (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line A L) \/ ((apart_point_and_line A M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N))))))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All A, (All L, (-. (apart_point_and_line A (orthogonal_through_point L A))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) ### Definition-Pseudo(parallel_lines) 96 % 20.70/20.92 98. (-. (All L, (parallel_lines L (orthogonal_through_point (orthogonal_through_point L T_1) T_1)))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) (All A, (All L, (-. (apart_point_and_line A (orthogonal_through_point L A))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All A, (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line A L) \/ ((apart_point_and_line A M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N))))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All X, (-. (convergent_lines X X))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) ### NotAllEx 97 % 20.70/20.92 99. (-. (All A, (All L, (parallel_lines L (orthogonal_through_point (orthogonal_through_point L A) A))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All X, (-. (convergent_lines X X))) (All A, (All L, (-. (unorthogonal_lines (orthogonal_through_point L A) L)))) (All L, (All M, (-. ((-. (convergent_lines L M)) /\ (-. (unorthogonal_lines L M)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((apart_point_and_line X Y) => ((distinct_lines Y Z) \/ (apart_point_and_line X Z)))))) (All A, (All L, (All M, (All N, ((distinct_lines L M) => ((apart_point_and_line A L) \/ ((apart_point_and_line A M) \/ ((unorthogonal_lines L N) \/ (unorthogonal_lines M N))))))))) (All X, (All Y, ((distinct_lines X Y) => (convergent_lines X Y)))) (All A, (All L, (-. (apart_point_and_line A (orthogonal_through_point L A))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((distinct_lines Y Z) \/ (convergent_lines X Z)))))) ### NotAllEx 98 % 20.70/20.92 % SZS output end Proof % 20.70/20.92 (* END-PROOF *) %------------------------------------------------------------------------------