%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : GEO203+2 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n022.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:02 EDT 2022 % Result : Theorem 38.38s 38.61s % Output : Proof 38.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GEO203+2 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.34 % Computer : n022.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Fri Jun 17 15:34:17 EDT 2022 % 0.12/0.34 % CPUTime : % 38.38/38.61 % SZS status Theorem % 38.38/38.61 (* PROOF-FOUND *) % 38.38/38.61 (* BEGIN-PROOF *) % 38.38/38.61 % SZS output start Proof % 38.38/38.61 1. (convergent_lines T_0 T_1) (-. (convergent_lines T_0 T_1)) ### Axiom % 38.38/38.61 2. (convergent_lines T_0 T_2) (-. (convergent_lines T_0 T_2)) ### Axiom % 38.38/38.61 3. (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (-. (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1))) ### Axiom % 38.38/38.61 4. (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (-. (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1))) ### Axiom % 38.38/38.61 5. (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (-. (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1))) ### Axiom % 38.38/38.61 6. (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (-. (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0)) ### Axiom % 38.38/38.61 7. (-. (apart_point_and_line (intersection_point T_0 T_2) (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)))) (apart_point_and_line (intersection_point T_0 T_2) (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1))) ### Axiom % 38.38/38.61 8. (-. (apart_point_and_line (intersection_point T_0 T_2) T_0)) (apart_point_and_line (intersection_point T_0 T_2) T_0) ### Axiom % 38.38/38.61 9. (-. (apart_point_and_line (intersection_point T_0 T_1) (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)))) (apart_point_and_line (intersection_point T_0 T_1) (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1))) ### Axiom % 38.38/38.61 10. (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (apart_point_and_line (intersection_point T_0 T_1) T_0) ### Axiom % 38.38/38.61 11. (((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) /\ (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0)) => ((apart_point_and_line (intersection_point T_0 T_2) (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1))) \/ ((apart_point_and_line (intersection_point T_0 T_2) T_0) \/ ((apart_point_and_line (intersection_point T_0 T_1) (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1))) \/ (apart_point_and_line (intersection_point T_0 T_1) T_0))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (-. (apart_point_and_line (intersection_point T_0 T_1) (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)))) (-. (apart_point_and_line (intersection_point T_0 T_2) T_0)) (-. (apart_point_and_line (intersection_point T_0 T_2) (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)))) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) ### DisjTree 5 6 7 8 9 10 % 38.38/38.61 12. (All V, (((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) /\ (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) V)) => ((apart_point_and_line (intersection_point T_0 T_2) (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1))) \/ ((apart_point_and_line (intersection_point T_0 T_2) V) \/ ((apart_point_and_line (intersection_point T_0 T_1) (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1))) \/ (apart_point_and_line (intersection_point T_0 T_1) V)))))) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (-. (apart_point_and_line (intersection_point T_0 T_2) (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)))) (-. (apart_point_and_line (intersection_point T_0 T_2) T_0)) (-. (apart_point_and_line (intersection_point T_0 T_1) (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) ### All 11 % 38.38/38.61 13. (All U, (All V, (((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_2) U) \/ ((apart_point_and_line (intersection_point T_0 T_2) V) \/ ((apart_point_and_line (intersection_point T_0 T_1) U) \/ (apart_point_and_line (intersection_point T_0 T_1) V))))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (-. (apart_point_and_line (intersection_point T_0 T_1) (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)))) (-. (apart_point_and_line (intersection_point T_0 T_2) T_0)) (-. (apart_point_and_line (intersection_point T_0 T_2) (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)))) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) ### All 12 % 38.38/38.61 14. (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1)) ### Axiom % 38.38/38.61 15. ((distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_2)) /\ (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) ### And 14 % 38.38/38.61 16. ((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) => ((apart_point_and_line (intersection_point T_0 T_1) (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1))) => ((distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_2)) /\ (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))))) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (-. (apart_point_and_line (intersection_point T_0 T_2) (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)))) (-. (apart_point_and_line (intersection_point T_0 T_2) T_0)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (All U, (All V, (((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_2) U) \/ ((apart_point_and_line (intersection_point T_0 T_2) V) \/ ((apart_point_and_line (intersection_point T_0 T_1) U) \/ (apart_point_and_line (intersection_point T_0 T_1) V))))))) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) ### DisjTree 4 13 15 % 38.38/38.61 17. (All Z, ((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) => ((apart_point_and_line Z (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1))) => ((distinct_points Z (intersection_point T_0 T_2)) /\ (distinct_points Z (intersection_point T_0 T_1)))))) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (All U, (All V, (((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_2) U) \/ ((apart_point_and_line (intersection_point T_0 T_2) V) \/ ((apart_point_and_line (intersection_point T_0 T_1) U) \/ (apart_point_and_line (intersection_point T_0 T_1) V))))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (-. (apart_point_and_line (intersection_point T_0 T_2) T_0)) (-. (apart_point_and_line (intersection_point T_0 T_2) (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)))) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) ### All 16 % 38.38/38.61 18. (-. (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_2))) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_2)) ### Axiom % 38.38/38.61 19. ((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_2)) /\ (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1))) (-. (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_2))) ### And 18 % 38.81/39.03 20. ((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) => ((apart_point_and_line (intersection_point T_0 T_2) (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1))) => ((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_2)) /\ (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1))))) (-. (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_2))) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (-. (apart_point_and_line (intersection_point T_0 T_2) T_0)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (All U, (All V, (((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_2) U) \/ ((apart_point_and_line (intersection_point T_0 T_2) V) \/ ((apart_point_and_line (intersection_point T_0 T_1) U) \/ (apart_point_and_line (intersection_point T_0 T_1) V))))))) (All Z, ((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) => ((apart_point_and_line Z (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1))) => ((distinct_points Z (intersection_point T_0 T_2)) /\ (distinct_points Z (intersection_point T_0 T_1)))))) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) ### DisjTree 3 17 19 % 38.81/39.03 21. (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (All Z, ((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) => ((apart_point_and_line Z (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1))) => ((distinct_points Z (intersection_point T_0 T_2)) /\ (distinct_points Z (intersection_point T_0 T_1)))))) (All U, (All V, (((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_2) U) \/ ((apart_point_and_line (intersection_point T_0 T_2) V) \/ ((apart_point_and_line (intersection_point T_0 T_1) U) \/ (apart_point_and_line (intersection_point T_0 T_1) V))))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (-. (apart_point_and_line (intersection_point T_0 T_2) T_0)) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (-. (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_2))) ### All 20 % 38.81/39.03 22. (-. ((apart_point_and_line (intersection_point T_0 T_2) T_0) \/ (apart_point_and_line (intersection_point T_0 T_2) T_2))) (-. (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_2))) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (All U, (All V, (((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_2) U) \/ ((apart_point_and_line (intersection_point T_0 T_2) V) \/ ((apart_point_and_line (intersection_point T_0 T_1) U) \/ (apart_point_and_line (intersection_point T_0 T_1) V))))))) (All Z, ((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) => ((apart_point_and_line Z (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1))) => ((distinct_points Z (intersection_point T_0 T_2)) /\ (distinct_points Z (intersection_point T_0 T_1)))))) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) ### NotOr 21 % 38.81/39.03 23. (-. (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_2))) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_2)) ### Axiom % 38.81/39.03 24. ((convergent_lines T_0 T_2) => (((apart_point_and_line (intersection_point T_0 T_2) T_0) \/ (apart_point_and_line (intersection_point T_0 T_2) T_2)) => (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_2)))) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (All Z, ((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) => ((apart_point_and_line Z (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1))) => ((distinct_points Z (intersection_point T_0 T_2)) /\ (distinct_points Z (intersection_point T_0 T_1)))))) (All U, (All V, (((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_2) U) \/ ((apart_point_and_line (intersection_point T_0 T_2) V) \/ ((apart_point_and_line (intersection_point T_0 T_1) U) \/ (apart_point_and_line (intersection_point T_0 T_1) V))))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (-. (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_2))) (convergent_lines T_0 T_2) ### DisjTree 2 22 23 % 38.81/39.03 25. (All Z, ((convergent_lines T_0 T_2) => (((apart_point_and_line Z T_0) \/ (apart_point_and_line Z T_2)) => (distinct_points Z (intersection_point T_0 T_2))))) (convergent_lines T_0 T_2) (-. (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_2))) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (All U, (All V, (((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_2) U) \/ ((apart_point_and_line (intersection_point T_0 T_2) V) \/ ((apart_point_and_line (intersection_point T_0 T_1) U) \/ (apart_point_and_line (intersection_point T_0 T_1) V))))))) (All Z, ((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) => ((apart_point_and_line Z (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1))) => ((distinct_points Z (intersection_point T_0 T_2)) /\ (distinct_points Z (intersection_point T_0 T_1)))))) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) ### All 24 % 38.81/39.03 26. (All Y, (All Z, ((distinct_points (intersection_point T_0 T_2) Y) => ((apart_point_and_line Z (line_connecting (intersection_point T_0 T_2) Y)) => ((distinct_points Z (intersection_point T_0 T_2)) /\ (distinct_points Z Y)))))) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (All U, (All V, (((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_2) U) \/ ((apart_point_and_line (intersection_point T_0 T_2) V) \/ ((apart_point_and_line (intersection_point T_0 T_1) U) \/ (apart_point_and_line (intersection_point T_0 T_1) V))))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (-. (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_2))) (convergent_lines T_0 T_2) (All Z, ((convergent_lines T_0 T_2) => (((apart_point_and_line Z T_0) \/ (apart_point_and_line Z T_2)) => (distinct_points Z (intersection_point T_0 T_2))))) ### All 25 % 38.81/39.03 27. (All Y, (All Z, ((convergent_lines T_0 Y) => (((apart_point_and_line Z T_0) \/ (apart_point_and_line Z Y)) => (distinct_points Z (intersection_point T_0 Y)))))) (convergent_lines T_0 T_2) (-. (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_2))) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (All U, (All V, (((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_2) U) \/ ((apart_point_and_line (intersection_point T_0 T_2) V) \/ ((apart_point_and_line (intersection_point T_0 T_1) U) \/ (apart_point_and_line (intersection_point T_0 T_1) V))))))) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (All Y, (All Z, ((distinct_points (intersection_point T_0 T_2) Y) => ((apart_point_and_line Z (line_connecting (intersection_point T_0 T_2) Y)) => ((distinct_points Z (intersection_point T_0 T_2)) /\ (distinct_points Z Y)))))) ### All 26 % 38.88/39.05 28. (All X, (-. (distinct_points X X))) (All Y, (All Z, ((distinct_points (intersection_point T_0 T_2) Y) => ((apart_point_and_line Z (line_connecting (intersection_point T_0 T_2) Y)) => ((distinct_points Z (intersection_point T_0 T_2)) /\ (distinct_points Z Y)))))) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (All U, (All V, (((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_2) U) \/ ((apart_point_and_line (intersection_point T_0 T_2) V) \/ ((apart_point_and_line (intersection_point T_0 T_1) U) \/ (apart_point_and_line (intersection_point T_0 T_1) V))))))) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (convergent_lines T_0 T_2) (All Y, (All Z, ((convergent_lines T_0 Y) => (((apart_point_and_line Z T_0) \/ (apart_point_and_line Z Y)) => (distinct_points Z (intersection_point T_0 Y)))))) ### All 27 % 38.88/39.05 29. (All X, (All Y, (All Z, ((distinct_points X Y) => ((apart_point_and_line Z (line_connecting X Y)) => ((distinct_points Z X) /\ (distinct_points Z Y))))))) (All Y, (All Z, ((convergent_lines T_0 Y) => (((apart_point_and_line Z T_0) \/ (apart_point_and_line Z Y)) => (distinct_points Z (intersection_point T_0 Y)))))) (convergent_lines T_0 T_2) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (All U, (All V, (((distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_2) U) \/ ((apart_point_and_line (intersection_point T_0 T_2) V) \/ ((apart_point_and_line (intersection_point T_0 T_1) U) \/ (apart_point_and_line (intersection_point T_0 T_1) V))))))) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (All X, (-. (distinct_points X X))) ### All 28 % 38.88/39.05 30. (All Y, (All U, (All V, (((distinct_points (intersection_point T_0 T_2) Y) /\ (distinct_lines U V)) => ((apart_point_and_line (intersection_point T_0 T_2) U) \/ ((apart_point_and_line (intersection_point T_0 T_2) V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V)))))))) (All X, (-. (distinct_points X X))) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (convergent_lines T_0 T_2) (All Y, (All Z, ((convergent_lines T_0 Y) => (((apart_point_and_line Z T_0) \/ (apart_point_and_line Z Y)) => (distinct_points Z (intersection_point T_0 Y)))))) (All X, (All Y, (All Z, ((distinct_points X Y) => ((apart_point_and_line Z (line_connecting X Y)) => ((distinct_points Z X) /\ (distinct_points Z Y))))))) ### All 29 % 38.88/39.05 31. (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((distinct_points X Y) => ((apart_point_and_line Z (line_connecting X Y)) => ((distinct_points Z X) /\ (distinct_points Z Y))))))) (All Y, (All Z, ((convergent_lines T_0 Y) => (((apart_point_and_line Z T_0) \/ (apart_point_and_line Z Y)) => (distinct_points Z (intersection_point T_0 Y)))))) (convergent_lines T_0 T_2) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (-. (apart_point_and_line (intersection_point T_0 T_1) T_0)) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (All X, (-. (distinct_points X X))) ### All 30 % 38.88/39.05 32. (-. ((apart_point_and_line (intersection_point T_0 T_1) T_0) \/ (apart_point_and_line (intersection_point T_0 T_1) T_1))) (All X, (-. (distinct_points X X))) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (convergent_lines T_0 T_2) (All Y, (All Z, ((convergent_lines T_0 Y) => (((apart_point_and_line Z T_0) \/ (apart_point_and_line Z Y)) => (distinct_points Z (intersection_point T_0 Y)))))) (All X, (All Y, (All Z, ((distinct_points X Y) => ((apart_point_and_line Z (line_connecting X Y)) => ((distinct_points Z X) /\ (distinct_points Z Y))))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) ### NotOr 31 % 38.88/39.05 33. (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1)) ### Axiom % 38.88/39.05 34. ((convergent_lines T_0 T_1) => (((apart_point_and_line (intersection_point T_0 T_1) T_0) \/ (apart_point_and_line (intersection_point T_0 T_1) T_1)) => (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1)))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((distinct_points X Y) => ((apart_point_and_line Z (line_connecting X Y)) => ((distinct_points Z X) /\ (distinct_points Z Y))))))) (All Y, (All Z, ((convergent_lines T_0 Y) => (((apart_point_and_line Z T_0) \/ (apart_point_and_line Z Y)) => (distinct_points Z (intersection_point T_0 Y)))))) (convergent_lines T_0 T_2) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (All X, (-. (distinct_points X X))) (convergent_lines T_0 T_1) ### DisjTree 1 32 33 % 38.88/39.05 35. (All Z, ((convergent_lines T_0 T_1) => (((apart_point_and_line Z T_0) \/ (apart_point_and_line Z T_1)) => (distinct_points Z (intersection_point T_0 T_1))))) (convergent_lines T_0 T_1) (All X, (-. (distinct_points X X))) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (convergent_lines T_0 T_2) (All Y, (All Z, ((convergent_lines T_0 Y) => (((apart_point_and_line Z T_0) \/ (apart_point_and_line Z Y)) => (distinct_points Z (intersection_point T_0 Y)))))) (All X, (All Y, (All Z, ((distinct_points X Y) => ((apart_point_and_line Z (line_connecting X Y)) => ((distinct_points Z X) /\ (distinct_points Z Y))))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) ### All 34 % 38.88/39.06 36. (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((distinct_points X Y) => ((apart_point_and_line Z (line_connecting X Y)) => ((distinct_points Z X) /\ (distinct_points Z Y))))))) (All Y, (All Z, ((convergent_lines T_0 Y) => (((apart_point_and_line Z T_0) \/ (apart_point_and_line Z Y)) => (distinct_points Z (intersection_point T_0 Y)))))) (convergent_lines T_0 T_2) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (All X, (-. (distinct_points X X))) (convergent_lines T_0 T_1) ### All 35 % 38.88/39.06 37. (All X, (All Y, (All Z, ((convergent_lines X Y) => (((apart_point_and_line Z X) \/ (apart_point_and_line Z Y)) => (distinct_points Z (intersection_point X Y))))))) (convergent_lines T_0 T_1) (All X, (-. (distinct_points X X))) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (-. (distinct_points (intersection_point T_0 T_1) (intersection_point T_0 T_1))) (convergent_lines T_0 T_2) (All X, (All Y, (All Z, ((distinct_points X Y) => ((apart_point_and_line Z (line_connecting X Y)) => ((distinct_points Z X) /\ (distinct_points Z Y))))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) ### All 36 % 38.88/39.06 38. (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((distinct_points X Y) => ((apart_point_and_line Z (line_connecting X Y)) => ((distinct_points Z X) /\ (distinct_points Z Y))))))) (convergent_lines T_0 T_2) (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0) (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)) (All X, (-. (distinct_points X X))) (convergent_lines T_0 T_1) (All X, (All Y, (All Z, ((convergent_lines X Y) => (((apart_point_and_line Z X) \/ (apart_point_and_line Z Y)) => (distinct_points Z (intersection_point X Y))))))) ### All 37 % 38.88/39.06 39. (-. (((convergent_lines T_0 T_2) /\ ((convergent_lines T_0 T_1) /\ (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 T_1)))) => (-. (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 T_1)) T_0)))) (All X, (All Y, (All Z, ((convergent_lines X Y) => (((apart_point_and_line Z X) \/ (apart_point_and_line Z Y)) => (distinct_points Z (intersection_point X Y))))))) (All X, (-. (distinct_points X X))) (All X, (All Y, (All Z, ((distinct_points X Y) => ((apart_point_and_line Z (line_connecting X Y)) => ((distinct_points Z X) /\ (distinct_points Z Y))))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) ### ConjTree 38 % 38.88/39.06 40. (-. (All Z, (((convergent_lines T_0 T_2) /\ ((convergent_lines T_0 Z) /\ (distinct_points (intersection_point T_0 T_2) (intersection_point T_0 Z)))) => (-. (distinct_lines (line_connecting (intersection_point T_0 T_2) (intersection_point T_0 Z)) T_0))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((distinct_points X Y) => ((apart_point_and_line Z (line_connecting X Y)) => ((distinct_points Z X) /\ (distinct_points Z Y))))))) (All X, (-. (distinct_points X X))) (All X, (All Y, (All Z, ((convergent_lines X Y) => (((apart_point_and_line Z X) \/ (apart_point_and_line Z Y)) => (distinct_points Z (intersection_point X Y))))))) ### NotAllEx 39 % 38.88/39.06 41. (-. (All Y, (All Z, (((convergent_lines T_0 Y) /\ ((convergent_lines T_0 Z) /\ (distinct_points (intersection_point T_0 Y) (intersection_point T_0 Z)))) => (-. (distinct_lines (line_connecting (intersection_point T_0 Y) (intersection_point T_0 Z)) T_0)))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => (((apart_point_and_line Z X) \/ (apart_point_and_line Z Y)) => (distinct_points Z (intersection_point X Y))))))) (All X, (-. (distinct_points X X))) (All X, (All Y, (All Z, ((distinct_points X Y) => ((apart_point_and_line Z (line_connecting X Y)) => ((distinct_points Z X) /\ (distinct_points Z Y))))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) ### NotAllEx 40 % 38.88/39.06 42. (-. (All X, (All Y, (All Z, (((convergent_lines X Y) /\ ((convergent_lines X Z) /\ (distinct_points (intersection_point X Y) (intersection_point X Z)))) => (-. (distinct_lines (line_connecting (intersection_point X Y) (intersection_point X Z)) X))))))) (All X, (All Y, (All U, (All V, (((distinct_points X Y) /\ (distinct_lines U V)) => ((apart_point_and_line X U) \/ ((apart_point_and_line X V) \/ ((apart_point_and_line Y U) \/ (apart_point_and_line Y V))))))))) (All X, (All Y, (All Z, ((distinct_points X Y) => ((apart_point_and_line Z (line_connecting X Y)) => ((distinct_points Z X) /\ (distinct_points Z Y))))))) (All X, (-. (distinct_points X X))) (All X, (All Y, (All Z, ((convergent_lines X Y) => (((apart_point_and_line Z X) \/ (apart_point_and_line Z Y)) => (distinct_points Z (intersection_point X Y))))))) ### NotAllEx 41 % 38.88/39.06 % SZS output end Proof % 38.88/39.06 (* END-PROOF *) %------------------------------------------------------------------------------