%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : GEO191+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n012.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 07:00:35 EDT 2022 % Result : Theorem 0.83s 1.04s % Output : Proof 0.83s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GEO191+1 : TPTP v8.1.0. Released v3.3.0. % 0.07/0.13 % Command : run_zenon %s %d % 0.12/0.34 % Computer : n012.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:12:39 EDT 2022 % 0.12/0.34 % CPUTime : % 0.83/1.04 (* PROOF-FOUND *) % 0.83/1.04 % SZS status Theorem % 0.83/1.04 (* BEGIN-PROOF *) % 0.83/1.04 % SZS output start Proof % 0.83/1.04 Theorem con : (forall X : zenon_U, (forall Y : zenon_U, (forall U : zenon_U, (forall V : zenon_U, (((convergent_lines X Y)/\((convergent_lines U V)/\((apart_point_and_line (intersection_point X Y) U)\/(apart_point_and_line (intersection_point X Y) V))))->((apart_point_and_line (intersection_point U V) X)\/(apart_point_and_line (intersection_point U V) Y))))))). % 0.83/1.04 Proof. % 0.83/1.04 assert (zenon_L1_ : forall (zenon_TV_t : zenon_U) (zenon_TU_u : zenon_U), (forall Z : zenon_U, ((convergent_lines zenon_TU_u zenon_TV_t)->((convergent_lines zenon_TU_u Z)\/(convergent_lines zenon_TV_t Z)))) -> (convergent_lines zenon_TU_u zenon_TV_t) -> (~(convergent_lines zenon_TU_u zenon_TU_u)) -> (~(convergent_lines zenon_TV_t zenon_TU_u)) -> False). % 0.83/1.04 do 2 intro. intros zenon_Hf zenon_H10 zenon_H11 zenon_H12. % 0.83/1.04 generalize (zenon_Hf zenon_TU_u). zenon_intro zenon_H15. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H15); [ zenon_intro zenon_H17 | zenon_intro zenon_H16 ]. % 0.83/1.04 exact (zenon_H17 zenon_H10). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H16); [ zenon_intro zenon_H19 | zenon_intro zenon_H18 ]. % 0.83/1.04 exact (zenon_H11 zenon_H19). % 0.83/1.04 exact (zenon_H12 zenon_H18). % 0.83/1.04 (* end of lemma zenon_L1_ *) % 0.83/1.04 assert (zenon_L2_ : forall (zenon_TX_bb : zenon_U), (convergent_lines zenon_TX_bb zenon_TX_bb) -> False). % 0.83/1.04 do 1 intro. intros zenon_H1a. % 0.83/1.04 generalize (apart3 zenon_TX_bb). zenon_intro zenon_H1c. % 0.83/1.04 exact (zenon_H1c zenon_H1a). % 0.83/1.04 (* end of lemma zenon_L2_ *) % 0.83/1.04 assert (zenon_L3_ : forall (zenon_TX_bb : zenon_U) (zenon_TY_bi : zenon_U), (forall Y : zenon_U, (forall Z : zenon_U, ((convergent_lines zenon_TY_bi Y)->((distinct_lines Y Z)\/(convergent_lines zenon_TY_bi Z))))) -> (~(convergent_lines zenon_TY_bi zenon_TY_bi)) -> (~(distinct_lines zenon_TX_bb zenon_TY_bi)) -> (convergent_lines zenon_TX_bb zenon_TY_bi) -> (forall Z : zenon_U, ((convergent_lines zenon_TX_bb zenon_TY_bi)->((convergent_lines zenon_TX_bb Z)\/(convergent_lines zenon_TY_bi Z)))) -> False). % 0.83/1.04 do 2 intro. intros zenon_H1d zenon_H1e zenon_H1f zenon_H20 zenon_H21. % 0.83/1.04 generalize (zenon_H1d zenon_TX_bb). zenon_intro zenon_H23. % 0.83/1.04 generalize (zenon_H23 zenon_TY_bi). zenon_intro zenon_H24. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H24); [ zenon_intro zenon_H26 | zenon_intro zenon_H25 ]. % 0.83/1.04 generalize (zenon_H21 zenon_TX_bb). zenon_intro zenon_H27. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H27); [ zenon_intro zenon_H29 | zenon_intro zenon_H28 ]. % 0.83/1.04 exact (zenon_H29 zenon_H20). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H28); [ zenon_intro zenon_H1a | zenon_intro zenon_H2a ]. % 0.83/1.04 apply (zenon_L2_ zenon_TX_bb); trivial. % 0.83/1.04 exact (zenon_H26 zenon_H2a). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H25); [ zenon_intro zenon_H2c | zenon_intro zenon_H2b ]. % 0.83/1.04 exact (zenon_H1f zenon_H2c). % 0.83/1.04 exact (zenon_H1e zenon_H2b). % 0.83/1.04 (* end of lemma zenon_L3_ *) % 0.83/1.04 assert (zenon_L4_ : forall (zenon_TY_bi : zenon_U) (zenon_TX_bb : zenon_U), (forall Y : zenon_U, ((convergent_lines zenon_TX_bb Y)->(~(apart_point_and_line (intersection_point zenon_TX_bb Y) zenon_TX_bb)))) -> (convergent_lines zenon_TX_bb zenon_TY_bi) -> (apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) zenon_TX_bb) -> False). % 0.83/1.04 do 2 intro. intros zenon_H2d zenon_H20 zenon_H2e. % 0.83/1.04 generalize (zenon_H2d zenon_TY_bi). zenon_intro zenon_H2f. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H2f); [ zenon_intro zenon_H29 | zenon_intro zenon_H30 ]. % 0.83/1.04 exact (zenon_H29 zenon_H20). % 0.83/1.04 exact (zenon_H30 zenon_H2e). % 0.83/1.04 (* end of lemma zenon_L4_ *) % 0.83/1.04 assert (zenon_L5_ : forall (zenon_TY_bi : zenon_U) (zenon_TX_bb : zenon_U), (apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) zenon_TX_bb) -> (convergent_lines zenon_TX_bb zenon_TY_bi) -> False). % 0.83/1.04 do 2 intro. intros zenon_H2e zenon_H20. % 0.83/1.04 generalize (ci3 zenon_TX_bb). zenon_intro zenon_H2d. % 0.83/1.04 apply (zenon_L4_ zenon_TY_bi zenon_TX_bb); trivial. % 0.83/1.04 (* end of lemma zenon_L5_ *) % 0.83/1.04 assert (zenon_L6_ : forall (zenon_TV_t : zenon_U) (zenon_TU_u : zenon_U), (apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TV_t) -> (convergent_lines zenon_TU_u zenon_TV_t) -> False). % 0.83/1.04 do 2 intro. intros zenon_H31 zenon_H10. % 0.83/1.04 generalize (ci4 zenon_TU_u). zenon_intro zenon_H32. % 0.83/1.04 generalize (zenon_H32 zenon_TV_t). zenon_intro zenon_H33. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H33); [ zenon_intro zenon_H17 | zenon_intro zenon_H34 ]. % 0.83/1.04 exact (zenon_H17 zenon_H10). % 0.83/1.04 exact (zenon_H34 zenon_H31). % 0.83/1.04 (* end of lemma zenon_L6_ *) % 0.83/1.04 assert (zenon_L7_ : forall (zenon_TV_t : zenon_U) (zenon_TU_u : zenon_U), (forall Y : zenon_U, ((convergent_lines zenon_TU_u Y)->(~(apart_point_and_line (intersection_point zenon_TU_u Y) zenon_TU_u)))) -> (convergent_lines zenon_TU_u zenon_TV_t) -> (apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TU_u) -> False). % 0.83/1.04 do 2 intro. intros zenon_H35 zenon_H10 zenon_H36. % 0.83/1.04 generalize (zenon_H35 zenon_TV_t). zenon_intro zenon_H37. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H37); [ zenon_intro zenon_H17 | zenon_intro zenon_H38 ]. % 0.83/1.04 exact (zenon_H17 zenon_H10). % 0.83/1.04 exact (zenon_H38 zenon_H36). % 0.83/1.04 (* end of lemma zenon_L7_ *) % 0.83/1.04 assert (zenon_L8_ : forall (zenon_TV_t : zenon_U) (zenon_TU_u : zenon_U), (forall Y : zenon_U, ((convergent_lines zenon_TU_u Y)->(~(apart_point_and_line (intersection_point zenon_TU_u Y) zenon_TU_u)))) -> (convergent_lines zenon_TU_u zenon_TV_t) -> (~(apart_point_and_line (intersection_point zenon_TV_t zenon_TU_u) zenon_TU_u)) -> (~(apart_point_and_line (intersection_point zenon_TV_t zenon_TU_u) zenon_TV_t)) -> (distinct_lines zenon_TV_t zenon_TU_u) -> (distinct_points (intersection_point zenon_TV_t zenon_TU_u) (intersection_point zenon_TU_u zenon_TV_t)) -> False). % 0.83/1.04 do 2 intro. intros zenon_H35 zenon_H10 zenon_H39 zenon_H3a zenon_H3b zenon_H3c. % 0.83/1.04 generalize (cu1 (intersection_point zenon_TV_t zenon_TU_u)). zenon_intro zenon_H3d. % 0.83/1.04 generalize (zenon_H3d (intersection_point zenon_TU_u zenon_TV_t)). zenon_intro zenon_H3e. % 0.83/1.04 generalize (zenon_H3e zenon_TV_t). zenon_intro zenon_H3f. % 0.83/1.04 generalize (zenon_H3f zenon_TU_u). zenon_intro zenon_H40. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H40); [ zenon_intro zenon_H42 | zenon_intro zenon_H41 ]. % 0.83/1.04 apply (zenon_notand_s _ _ zenon_H42); [ zenon_intro zenon_H44 | zenon_intro zenon_H43 ]. % 0.83/1.04 exact (zenon_H44 zenon_H3c). % 0.83/1.04 exact (zenon_H43 zenon_H3b). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H41); [ zenon_intro zenon_H46 | zenon_intro zenon_H45 ]. % 0.83/1.04 exact (zenon_H3a zenon_H46). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H45); [ zenon_intro zenon_H48 | zenon_intro zenon_H47 ]. % 0.83/1.04 exact (zenon_H39 zenon_H48). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H47); [ zenon_intro zenon_H31 | zenon_intro zenon_H36 ]. % 0.83/1.04 apply (zenon_L6_ zenon_TV_t zenon_TU_u); trivial. % 0.83/1.04 apply (zenon_L7_ zenon_TV_t zenon_TU_u); trivial. % 0.83/1.04 (* end of lemma zenon_L8_ *) % 0.83/1.04 assert (zenon_L9_ : forall (zenon_TU_u : zenon_U) (zenon_TV_t : zenon_U), (forall Y : zenon_U, ((convergent_lines zenon_TV_t Y)->(~(apart_point_and_line (intersection_point zenon_TV_t Y) zenon_TV_t)))) -> (forall Z : zenon_U, ((convergent_lines zenon_TU_u zenon_TV_t)->((convergent_lines zenon_TU_u Z)\/(convergent_lines zenon_TV_t Z)))) -> (convergent_lines zenon_TU_u zenon_TV_t) -> (~(convergent_lines zenon_TU_u zenon_TU_u)) -> (apart_point_and_line (intersection_point zenon_TV_t zenon_TU_u) zenon_TV_t) -> False). % 0.83/1.04 do 2 intro. intros zenon_H49 zenon_Hf zenon_H10 zenon_H11 zenon_H46. % 0.83/1.04 generalize (zenon_H49 zenon_TU_u). zenon_intro zenon_H4a. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H4a); [ zenon_intro zenon_H12 | zenon_intro zenon_H3a ]. % 0.83/1.04 apply (zenon_L1_ zenon_TV_t zenon_TU_u); trivial. % 0.83/1.04 exact (zenon_H3a zenon_H46). % 0.83/1.04 (* end of lemma zenon_L9_ *) % 0.83/1.04 assert (zenon_L10_ : forall (zenon_TX_bb : zenon_U) (zenon_TU_u : zenon_U) (zenon_TV_t : zenon_U), (apart_point_and_line (intersection_point zenon_TV_t zenon_TU_u) zenon_TX_bb) -> (forall Y : zenon_U, ((convergent_lines zenon_TU_u Y)->(~(apart_point_and_line (intersection_point zenon_TU_u Y) zenon_TU_u)))) -> (convergent_lines zenon_TU_u zenon_TV_t) -> (~(apart_point_and_line (intersection_point zenon_TV_t zenon_TU_u) zenon_TU_u)) -> (distinct_lines zenon_TV_t zenon_TU_u) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TX_bb)) -> (~(distinct_lines zenon_TV_t zenon_TV_t)) -> (forall Y : zenon_U, ((convergent_lines zenon_TV_t Y)->(~(apart_point_and_line (intersection_point zenon_TV_t Y) zenon_TV_t)))) -> (forall Z : zenon_U, ((convergent_lines zenon_TU_u zenon_TV_t)->((convergent_lines zenon_TU_u Z)\/(convergent_lines zenon_TV_t Z)))) -> (~(convergent_lines zenon_TU_u zenon_TU_u)) -> False). % 0.83/1.04 do 3 intro. intros zenon_H4b zenon_H35 zenon_H10 zenon_H39 zenon_H3b zenon_H4c zenon_H4d zenon_H49 zenon_Hf zenon_H11. % 0.83/1.04 generalize (ceq2 (intersection_point zenon_TV_t zenon_TU_u)). zenon_intro zenon_H4e. % 0.83/1.04 generalize (zenon_H4e zenon_TV_t). zenon_intro zenon_H4f. % 0.83/1.04 generalize (zenon_H4f zenon_TV_t). zenon_intro zenon_H50. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H50); [ zenon_intro zenon_H3a | zenon_intro zenon_H51 ]. % 0.83/1.04 generalize (ceq1 (intersection_point zenon_TV_t zenon_TU_u)). zenon_intro zenon_H52. % 0.83/1.04 generalize (zenon_H52 zenon_TX_bb). zenon_intro zenon_H53. % 0.83/1.04 generalize (zenon_H53 (intersection_point zenon_TU_u zenon_TV_t)). zenon_intro zenon_H54. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H54); [ zenon_intro zenon_H56 | zenon_intro zenon_H55 ]. % 0.83/1.04 exact (zenon_H56 zenon_H4b). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H55); [ zenon_intro zenon_H3c | zenon_intro zenon_H57 ]. % 0.83/1.04 apply (zenon_L8_ zenon_TV_t zenon_TU_u); trivial. % 0.83/1.04 exact (zenon_H4c zenon_H57). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H51); [ zenon_intro zenon_H58 | zenon_intro zenon_H46 ]. % 0.83/1.04 exact (zenon_H4d zenon_H58). % 0.83/1.04 apply (zenon_L9_ zenon_TU_u zenon_TV_t); trivial. % 0.83/1.04 (* end of lemma zenon_L10_ *) % 0.83/1.04 assert (zenon_L11_ : forall (zenon_TV_t : zenon_U) (zenon_TU_u : zenon_U), (forall Y : zenon_U, ((convergent_lines zenon_TU_u Y)->(~(apart_point_and_line (intersection_point zenon_TU_u Y) zenon_TU_u)))) -> (convergent_lines zenon_TU_u zenon_TV_t) -> (~(apart_point_and_line (intersection_point zenon_TV_t zenon_TU_u) zenon_TU_u)) -> (distinct_lines zenon_TV_t zenon_TU_u) -> (distinct_points (intersection_point zenon_TV_t zenon_TU_u) (intersection_point zenon_TU_u zenon_TV_t)) -> (~(distinct_lines zenon_TV_t zenon_TV_t)) -> (forall Y : zenon_U, ((convergent_lines zenon_TV_t Y)->(~(apart_point_and_line (intersection_point zenon_TV_t Y) zenon_TV_t)))) -> (forall Z : zenon_U, ((convergent_lines zenon_TU_u zenon_TV_t)->((convergent_lines zenon_TU_u Z)\/(convergent_lines zenon_TV_t Z)))) -> (~(convergent_lines zenon_TU_u zenon_TU_u)) -> False). % 0.83/1.04 do 2 intro. intros zenon_H35 zenon_H10 zenon_H39 zenon_H3b zenon_H3c zenon_H4d zenon_H49 zenon_Hf zenon_H11. % 0.83/1.04 generalize (ceq2 (intersection_point zenon_TV_t zenon_TU_u)). zenon_intro zenon_H4e. % 0.83/1.04 generalize (zenon_H4e zenon_TV_t). zenon_intro zenon_H4f. % 0.83/1.04 generalize (zenon_H4f zenon_TV_t). zenon_intro zenon_H50. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H50); [ zenon_intro zenon_H3a | zenon_intro zenon_H51 ]. % 0.83/1.04 apply (zenon_L8_ zenon_TV_t zenon_TU_u); trivial. % 0.83/1.04 apply (zenon_or_s _ _ zenon_H51); [ zenon_intro zenon_H58 | zenon_intro zenon_H46 ]. % 0.83/1.04 exact (zenon_H4d zenon_H58). % 0.83/1.04 apply (zenon_L9_ zenon_TU_u zenon_TV_t); trivial. % 0.83/1.04 (* end of lemma zenon_L11_ *) % 0.83/1.04 assert (zenon_L12_ : forall (zenon_TY_bi : zenon_U) (zenon_TU_u : zenon_U) (zenon_TV_t : zenon_U), (apart_point_and_line (intersection_point zenon_TV_t zenon_TU_u) zenon_TY_bi) -> (forall Y : zenon_U, ((convergent_lines zenon_TU_u Y)->(~(apart_point_and_line (intersection_point zenon_TU_u Y) zenon_TU_u)))) -> (convergent_lines zenon_TU_u zenon_TV_t) -> (~(apart_point_and_line (intersection_point zenon_TV_t zenon_TU_u) zenon_TU_u)) -> (distinct_lines zenon_TV_t zenon_TU_u) -> (~(distinct_lines zenon_TV_t zenon_TV_t)) -> (forall Y : zenon_U, ((convergent_lines zenon_TV_t Y)->(~(apart_point_and_line (intersection_point zenon_TV_t Y) zenon_TV_t)))) -> (forall Z : zenon_U, ((convergent_lines zenon_TU_u zenon_TV_t)->((convergent_lines zenon_TU_u Z)\/(convergent_lines zenon_TV_t Z)))) -> (~(convergent_lines zenon_TU_u zenon_TU_u)) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TY_bi)) -> False). % 0.83/1.04 do 3 intro. intros zenon_H59 zenon_H35 zenon_H10 zenon_H39 zenon_H3b zenon_H4d zenon_H49 zenon_Hf zenon_H11 zenon_H5a. % 0.83/1.04 generalize (ceq1 (intersection_point zenon_TV_t zenon_TU_u)). zenon_intro zenon_H52. % 0.83/1.04 generalize (zenon_H52 zenon_TY_bi). zenon_intro zenon_H5b. % 0.83/1.04 generalize (zenon_H5b (intersection_point zenon_TU_u zenon_TV_t)). zenon_intro zenon_H5c. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H5c); [ zenon_intro zenon_H5e | zenon_intro zenon_H5d ]. % 0.83/1.04 exact (zenon_H5e zenon_H59). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H5d); [ zenon_intro zenon_H3c | zenon_intro zenon_H5f ]. % 0.83/1.04 apply (zenon_L11_ zenon_TV_t zenon_TU_u); trivial. % 0.83/1.04 exact (zenon_H5a zenon_H5f). % 0.83/1.04 (* end of lemma zenon_L12_ *) % 0.83/1.04 assert (zenon_L13_ : forall (zenon_TU_u : zenon_U) (zenon_TV_t : zenon_U) (zenon_TY_bi : zenon_U) (zenon_TX_bb : zenon_U), (forall U : zenon_U, (forall V : zenon_U, (((distinct_points (intersection_point zenon_TX_bb zenon_TY_bi) (intersection_point zenon_TV_t zenon_TU_u))/\(distinct_lines U V))->((apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) U)\/((apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) V)\/((apart_point_and_line (intersection_point zenon_TV_t zenon_TU_u) U)\/(apart_point_and_line (intersection_point zenon_TV_t zenon_TU_u) V))))))) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TY_bi)) -> (~(convergent_lines zenon_TU_u zenon_TU_u)) -> (forall Z : zenon_U, ((convergent_lines zenon_TU_u zenon_TV_t)->((convergent_lines zenon_TU_u Z)\/(convergent_lines zenon_TV_t Z)))) -> (forall Y : zenon_U, ((convergent_lines zenon_TV_t Y)->(~(apart_point_and_line (intersection_point zenon_TV_t Y) zenon_TV_t)))) -> (~(distinct_lines zenon_TV_t zenon_TV_t)) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TX_bb)) -> (distinct_lines zenon_TV_t zenon_TU_u) -> (~(apart_point_and_line (intersection_point zenon_TV_t zenon_TU_u) zenon_TU_u)) -> (convergent_lines zenon_TU_u zenon_TV_t) -> (forall Y : zenon_U, ((convergent_lines zenon_TU_u Y)->(~(apart_point_and_line (intersection_point zenon_TU_u Y) zenon_TU_u)))) -> (~(apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) zenon_TY_bi)) -> (convergent_lines zenon_TX_bb zenon_TY_bi) -> (distinct_lines zenon_TX_bb zenon_TY_bi) -> (distinct_points (intersection_point zenon_TX_bb zenon_TY_bi) (intersection_point zenon_TV_t zenon_TU_u)) -> False). % 0.83/1.04 do 4 intro. intros zenon_H60 zenon_H5a zenon_H11 zenon_Hf zenon_H49 zenon_H4d zenon_H4c zenon_H3b zenon_H39 zenon_H10 zenon_H35 zenon_H61 zenon_H20 zenon_H2c zenon_H62. % 0.83/1.04 generalize (zenon_H60 zenon_TX_bb). zenon_intro zenon_H63. % 0.83/1.04 generalize (zenon_H63 zenon_TY_bi). zenon_intro zenon_H64. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H64); [ zenon_intro zenon_H66 | zenon_intro zenon_H65 ]. % 0.83/1.04 apply (zenon_notand_s _ _ zenon_H66); [ zenon_intro zenon_H67 | zenon_intro zenon_H1f ]. % 0.83/1.04 exact (zenon_H67 zenon_H62). % 0.83/1.04 exact (zenon_H1f zenon_H2c). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H65); [ zenon_intro zenon_H2e | zenon_intro zenon_H68 ]. % 0.83/1.04 apply (zenon_L5_ zenon_TY_bi zenon_TX_bb); trivial. % 0.83/1.04 apply (zenon_or_s _ _ zenon_H68); [ zenon_intro zenon_H6a | zenon_intro zenon_H69 ]. % 0.83/1.04 exact (zenon_H61 zenon_H6a). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H69); [ zenon_intro zenon_H4b | zenon_intro zenon_H59 ]. % 0.83/1.04 apply (zenon_L10_ zenon_TX_bb zenon_TU_u zenon_TV_t); trivial. % 0.83/1.04 apply (zenon_L12_ zenon_TY_bi zenon_TU_u zenon_TV_t); trivial. % 0.83/1.04 (* end of lemma zenon_L13_ *) % 0.83/1.04 assert (zenon_L14_ : forall (zenon_TY_bi : zenon_U) (zenon_TX_bb : zenon_U), (apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) zenon_TY_bi) -> (convergent_lines zenon_TX_bb zenon_TY_bi) -> False). % 0.83/1.04 do 2 intro. intros zenon_H6a zenon_H20. % 0.83/1.04 generalize (ci4 zenon_TX_bb). zenon_intro zenon_H6b. % 0.83/1.04 generalize (zenon_H6b zenon_TY_bi). zenon_intro zenon_H6c. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H6c); [ zenon_intro zenon_H29 | zenon_intro zenon_H61 ]. % 0.83/1.04 exact (zenon_H29 zenon_H20). % 0.83/1.04 exact (zenon_H61 zenon_H6a). % 0.83/1.04 (* end of lemma zenon_L14_ *) % 0.83/1.04 assert (zenon_L15_ : forall (zenon_TV_t : zenon_U) (zenon_TU_u : zenon_U) (zenon_TY_bi : zenon_U) (zenon_TX_bb : zenon_U), (forall Y : zenon_U, (forall Z : zenon_U, ((apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) Y)->((distinct_lines Y Z)\/(apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) Z))))) -> (forall Z : zenon_U, ((convergent_lines zenon_TU_u zenon_TV_t)->((convergent_lines zenon_TU_u Z)\/(convergent_lines zenon_TV_t Z)))) -> (convergent_lines zenon_TU_u zenon_TV_t) -> (~(convergent_lines zenon_TU_u zenon_TU_u)) -> (forall Z : zenon_U, ((apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) zenon_TU_u)->((distinct_points (intersection_point zenon_TX_bb zenon_TY_bi) Z)\/(apart_point_and_line Z zenon_TU_u)))) -> (apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) zenon_TU_u) -> (forall Y : zenon_U, (forall U : zenon_U, (forall V : zenon_U, (((distinct_points (intersection_point zenon_TX_bb zenon_TY_bi) Y)/\(distinct_lines U V))->((apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) U)\/((apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) V)\/((apart_point_and_line Y U)\/(apart_point_and_line Y V)))))))) -> (~(distinct_lines zenon_TY_bi zenon_TY_bi)) -> (forall Y : zenon_U, ((convergent_lines zenon_TU_u Y)->(~(apart_point_and_line (intersection_point zenon_TU_u Y) zenon_TU_u)))) -> (distinct_lines zenon_TV_t zenon_TU_u) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TX_bb)) -> (~(distinct_lines zenon_TV_t zenon_TV_t)) -> (forall Y : zenon_U, ((convergent_lines zenon_TV_t Y)->(~(apart_point_and_line (intersection_point zenon_TV_t Y) zenon_TV_t)))) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TY_bi)) -> (~(convergent_lines zenon_TY_bi zenon_TY_bi)) -> (convergent_lines zenon_TX_bb zenon_TY_bi) -> (forall Z : zenon_U, ((convergent_lines zenon_TX_bb zenon_TY_bi)->((convergent_lines zenon_TX_bb Z)\/(convergent_lines zenon_TY_bi Z)))) -> False). % 0.83/1.04 do 4 intro. intros zenon_H6d zenon_Hf zenon_H10 zenon_H11 zenon_H6e zenon_H6f zenon_H70 zenon_H71 zenon_H35 zenon_H3b zenon_H4c zenon_H4d zenon_H49 zenon_H5a zenon_H1e zenon_H20 zenon_H21. % 0.83/1.04 generalize (zenon_H6d zenon_TY_bi). zenon_intro zenon_H72. % 0.83/1.04 generalize (ci4 zenon_TV_t). zenon_intro zenon_H73. % 0.83/1.04 generalize (zenon_H72 zenon_TY_bi). zenon_intro zenon_H74. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H74); [ zenon_intro zenon_H61 | zenon_intro zenon_H75 ]. % 0.83/1.04 generalize (zenon_H73 zenon_TU_u). zenon_intro zenon_H76. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H76); [ zenon_intro zenon_H12 | zenon_intro zenon_H39 ]. % 0.83/1.04 apply (zenon_L1_ zenon_TV_t zenon_TU_u); trivial. % 0.83/1.04 generalize (zenon_H6e (intersection_point zenon_TV_t zenon_TU_u)). zenon_intro zenon_H77. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H77); [ zenon_intro zenon_H79 | zenon_intro zenon_H78 ]. % 0.83/1.04 exact (zenon_H79 zenon_H6f). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H78); [ zenon_intro zenon_H62 | zenon_intro zenon_H48 ]. % 0.83/1.04 generalize (zenon_H70 (intersection_point zenon_TV_t zenon_TU_u)). zenon_intro zenon_H60. % 0.83/1.04 generalize (apart5 zenon_TX_bb). zenon_intro zenon_H7a. % 0.83/1.04 generalize (zenon_H7a zenon_TY_bi). zenon_intro zenon_H7b. % 0.83/1.04 generalize (zenon_H7b zenon_TY_bi). zenon_intro zenon_H7c. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H7c); [ zenon_intro zenon_H1f | zenon_intro zenon_H7d ]. % 0.83/1.04 generalize (ceq3 zenon_TY_bi). zenon_intro zenon_H1d. % 0.83/1.04 apply (zenon_L3_ zenon_TX_bb zenon_TY_bi); trivial. % 0.83/1.04 apply (zenon_or_s _ _ zenon_H7d); [ zenon_intro zenon_H2c | zenon_intro zenon_H7e ]. % 0.83/1.04 apply (zenon_L13_ zenon_TU_u zenon_TV_t zenon_TY_bi zenon_TX_bb); trivial. % 0.83/1.04 exact (zenon_H71 zenon_H7e). % 0.83/1.04 exact (zenon_H39 zenon_H48). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H75); [ zenon_intro zenon_H7e | zenon_intro zenon_H6a ]. % 0.83/1.04 exact (zenon_H71 zenon_H7e). % 0.83/1.04 apply (zenon_L14_ zenon_TY_bi zenon_TX_bb); trivial. % 0.83/1.04 (* end of lemma zenon_L15_ *) % 0.83/1.04 assert (zenon_L16_ : forall (zenon_TV_t : zenon_U) (zenon_TU_u : zenon_U) (zenon_TY_bi : zenon_U) (zenon_TX_bb : zenon_U), (forall Y : zenon_U, (forall U : zenon_U, (forall V : zenon_U, (((distinct_points (intersection_point zenon_TX_bb zenon_TY_bi) Y)/\(distinct_lines U V))->((apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) U)\/((apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) V)\/((apart_point_and_line Y U)\/(apart_point_and_line Y V)))))))) -> (distinct_points (intersection_point zenon_TX_bb zenon_TY_bi) (intersection_point zenon_TU_u zenon_TV_t)) -> (distinct_lines zenon_TY_bi zenon_TU_u) -> (~(apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) zenon_TY_bi)) -> (~(apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) zenon_TU_u)) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TY_bi)) -> (forall Y : zenon_U, ((convergent_lines zenon_TU_u Y)->(~(apart_point_and_line (intersection_point zenon_TU_u Y) zenon_TU_u)))) -> (convergent_lines zenon_TU_u zenon_TV_t) -> False). % 0.83/1.04 do 4 intro. intros zenon_H70 zenon_H7f zenon_H80 zenon_H61 zenon_H79 zenon_H5a zenon_H35 zenon_H10. % 0.83/1.04 generalize (zenon_H70 (intersection_point zenon_TU_u zenon_TV_t)). zenon_intro zenon_H81. % 0.83/1.04 generalize (zenon_H81 zenon_TY_bi). zenon_intro zenon_H82. % 0.83/1.04 generalize (zenon_H82 zenon_TU_u). zenon_intro zenon_H83. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H83); [ zenon_intro zenon_H85 | zenon_intro zenon_H84 ]. % 0.83/1.04 apply (zenon_notand_s _ _ zenon_H85); [ zenon_intro zenon_H87 | zenon_intro zenon_H86 ]. % 0.83/1.04 exact (zenon_H87 zenon_H7f). % 0.83/1.04 exact (zenon_H86 zenon_H80). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H84); [ zenon_intro zenon_H6a | zenon_intro zenon_H88 ]. % 0.83/1.04 exact (zenon_H61 zenon_H6a). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H88); [ zenon_intro zenon_H6f | zenon_intro zenon_H89 ]. % 0.83/1.04 exact (zenon_H79 zenon_H6f). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H89); [ zenon_intro zenon_H5f | zenon_intro zenon_H36 ]. % 0.83/1.04 exact (zenon_H5a zenon_H5f). % 0.83/1.04 apply (zenon_L7_ zenon_TV_t zenon_TU_u); trivial. % 0.83/1.04 (* end of lemma zenon_L16_ *) % 0.83/1.04 assert (zenon_L17_ : forall (zenon_TX_bb : zenon_U) (zenon_TY_bi : zenon_U) (zenon_TV_t : zenon_U) (zenon_TU_u : zenon_U), (forall Y : zenon_U, (forall Z : zenon_U, ((convergent_lines zenon_TU_u Y)->((distinct_lines Y Z)\/(convergent_lines zenon_TU_u Z))))) -> (forall Z : zenon_U, ((convergent_lines zenon_TU_u zenon_TV_t)->((distinct_lines zenon_TV_t Z)\/(convergent_lines zenon_TU_u Z)))) -> (convergent_lines zenon_TU_u zenon_TV_t) -> (convergent_lines zenon_TU_u zenon_TY_bi) -> (forall Z : zenon_U, ((convergent_lines zenon_TU_u zenon_TV_t)->((convergent_lines zenon_TU_u Z)\/(convergent_lines zenon_TV_t Z)))) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TX_bb)) -> (forall Y : zenon_U, ((convergent_lines zenon_TV_t Y)->(~(apart_point_and_line (intersection_point zenon_TV_t Y) zenon_TV_t)))) -> (~(convergent_lines zenon_TY_bi zenon_TY_bi)) -> (forall Z : zenon_U, ((convergent_lines zenon_TX_bb zenon_TY_bi)->((convergent_lines zenon_TX_bb Z)\/(convergent_lines zenon_TY_bi Z)))) -> (convergent_lines zenon_TX_bb zenon_TY_bi) -> (apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) zenon_TV_t) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TY_bi)) -> False). % 0.83/1.04 do 4 intro. intros zenon_H8a zenon_H8b zenon_H10 zenon_H8c zenon_Hf zenon_H4c zenon_H49 zenon_H1e zenon_H21 zenon_H20 zenon_H8d zenon_H5a. % 0.83/1.04 generalize (zenon_H8a zenon_TY_bi). zenon_intro zenon_H8e. % 0.83/1.04 generalize (ceq2 (intersection_point zenon_TX_bb zenon_TY_bi)). zenon_intro zenon_H6d. % 0.83/1.04 generalize (ceq1 (intersection_point zenon_TX_bb zenon_TY_bi)). zenon_intro zenon_H8f. % 0.83/1.04 generalize (zenon_H8f zenon_TV_t). zenon_intro zenon_H90. % 0.83/1.04 generalize (cu1 (intersection_point zenon_TX_bb zenon_TY_bi)). zenon_intro zenon_H70. % 0.83/1.04 generalize (apart3 zenon_TU_u). zenon_intro zenon_H11. % 0.83/1.04 generalize (zenon_H8b zenon_TU_u). zenon_intro zenon_H91. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H91); [ zenon_intro zenon_H17 | zenon_intro zenon_H92 ]. % 0.83/1.04 exact (zenon_H17 zenon_H10). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H92); [ zenon_intro zenon_H3b | zenon_intro zenon_H19 ]. % 0.83/1.04 generalize (zenon_H8e zenon_TU_u). zenon_intro zenon_H93. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H93); [ zenon_intro zenon_H95 | zenon_intro zenon_H94 ]. % 0.83/1.04 exact (zenon_H95 zenon_H8c). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H94); [ zenon_intro zenon_H80 | zenon_intro zenon_H19 ]. % 0.83/1.04 generalize (apart2 zenon_TU_u). zenon_intro zenon_H96. % 0.83/1.04 generalize (ci3 zenon_TU_u). zenon_intro zenon_H35. % 0.83/1.04 generalize (zenon_H6d zenon_TU_u). zenon_intro zenon_H97. % 0.83/1.04 generalize (zenon_H97 zenon_TU_u). zenon_intro zenon_H98. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H98); [ zenon_intro zenon_H79 | zenon_intro zenon_H99 ]. % 0.83/1.04 generalize (apart2 zenon_TY_bi). zenon_intro zenon_H71. % 0.83/1.04 generalize (zenon_H6d zenon_TY_bi). zenon_intro zenon_H72. % 0.83/1.04 generalize (zenon_H72 zenon_TY_bi). zenon_intro zenon_H74. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H74); [ zenon_intro zenon_H61 | zenon_intro zenon_H75 ]. % 0.83/1.04 generalize (apart2 zenon_TV_t). zenon_intro zenon_H4d. % 0.83/1.04 generalize (ceq2 (intersection_point zenon_TU_u zenon_TV_t)). zenon_intro zenon_H9a. % 0.83/1.04 generalize (zenon_H9a zenon_TV_t). zenon_intro zenon_H9b. % 0.83/1.04 generalize (zenon_H9b zenon_TV_t). zenon_intro zenon_H9c. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H9c); [ zenon_intro zenon_H34 | zenon_intro zenon_H9d ]. % 0.83/1.04 generalize (zenon_H90 (intersection_point zenon_TU_u zenon_TV_t)). zenon_intro zenon_H9e. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H9e); [ zenon_intro zenon_Ha0 | zenon_intro zenon_H9f ]. % 0.83/1.04 exact (zenon_Ha0 zenon_H8d). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H9f); [ zenon_intro zenon_H7f | zenon_intro zenon_H31 ]. % 0.83/1.04 apply (zenon_L16_ zenon_TV_t zenon_TU_u zenon_TY_bi zenon_TX_bb); trivial. % 0.83/1.04 exact (zenon_H34 zenon_H31). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H9d); [ zenon_intro zenon_H58 | zenon_intro zenon_H31 ]. % 0.83/1.04 exact (zenon_H4d zenon_H58). % 0.83/1.04 apply (zenon_L6_ zenon_TV_t zenon_TU_u); trivial. % 0.83/1.04 apply (zenon_or_s _ _ zenon_H75); [ zenon_intro zenon_H7e | zenon_intro zenon_H6a ]. % 0.83/1.04 exact (zenon_H71 zenon_H7e). % 0.83/1.04 apply (zenon_L14_ zenon_TY_bi zenon_TX_bb); trivial. % 0.83/1.04 apply (zenon_or_s _ _ zenon_H99); [ zenon_intro zenon_Ha1 | zenon_intro zenon_H6f ]. % 0.83/1.04 exact (zenon_H96 zenon_Ha1). % 0.83/1.04 generalize (zenon_H8f zenon_TU_u). zenon_intro zenon_H6e. % 0.83/1.04 generalize (apart2 zenon_TV_t). zenon_intro zenon_H4d. % 0.83/1.04 generalize (apart2 zenon_TY_bi). zenon_intro zenon_H71. % 0.83/1.04 apply (zenon_L15_ zenon_TV_t zenon_TU_u zenon_TY_bi zenon_TX_bb); trivial. % 0.83/1.04 exact (zenon_H11 zenon_H19). % 0.83/1.04 exact (zenon_H11 zenon_H19). % 0.83/1.04 (* end of lemma zenon_L17_ *) % 0.83/1.04 assert (zenon_L18_ : forall (zenon_TY_bi : zenon_U) (zenon_TV_t : zenon_U), (apart_point_and_line (intersection_point zenon_TV_t zenon_TY_bi) zenon_TY_bi) -> (convergent_lines zenon_TV_t zenon_TY_bi) -> False). % 0.83/1.04 do 2 intro. intros zenon_Ha2 zenon_Ha3. % 0.83/1.04 generalize (ci4 zenon_TV_t). zenon_intro zenon_H73. % 0.83/1.04 generalize (zenon_H73 zenon_TY_bi). zenon_intro zenon_Ha4. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_Ha4); [ zenon_intro zenon_Ha6 | zenon_intro zenon_Ha5 ]. % 0.83/1.04 exact (zenon_Ha6 zenon_Ha3). % 0.83/1.04 exact (zenon_Ha5 zenon_Ha2). % 0.83/1.04 (* end of lemma zenon_L18_ *) % 0.83/1.04 assert (zenon_L19_ : forall (zenon_TU_u : zenon_U) (zenon_TY_bi : zenon_U) (zenon_TV_t : zenon_U), (forall Y : zenon_U, (forall U : zenon_U, (forall V : zenon_U, (((distinct_points (intersection_point zenon_TV_t zenon_TY_bi) Y)/\(distinct_lines U V))->((apart_point_and_line (intersection_point zenon_TV_t zenon_TY_bi) U)\/((apart_point_and_line (intersection_point zenon_TV_t zenon_TY_bi) V)\/((apart_point_and_line Y U)\/(apart_point_and_line Y V)))))))) -> (distinct_points (intersection_point zenon_TV_t zenon_TY_bi) (intersection_point zenon_TU_u zenon_TV_t)) -> (distinct_lines zenon_TY_bi zenon_TV_t) -> (convergent_lines zenon_TV_t zenon_TY_bi) -> (~(apart_point_and_line (intersection_point zenon_TV_t zenon_TY_bi) zenon_TV_t)) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TY_bi)) -> (convergent_lines zenon_TU_u zenon_TV_t) -> False). % 0.83/1.04 do 3 intro. intros zenon_Ha7 zenon_Ha8 zenon_Ha9 zenon_Ha3 zenon_Haa zenon_H5a zenon_H10. % 0.83/1.04 generalize (zenon_Ha7 (intersection_point zenon_TU_u zenon_TV_t)). zenon_intro zenon_Hab. % 0.83/1.04 generalize (zenon_Hab zenon_TY_bi). zenon_intro zenon_Hac. % 0.83/1.04 generalize (zenon_Hac zenon_TV_t). zenon_intro zenon_Had. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_Had); [ zenon_intro zenon_Haf | zenon_intro zenon_Hae ]. % 0.83/1.04 apply (zenon_notand_s _ _ zenon_Haf); [ zenon_intro zenon_Hb1 | zenon_intro zenon_Hb0 ]. % 0.83/1.04 exact (zenon_Hb1 zenon_Ha8). % 0.83/1.04 exact (zenon_Hb0 zenon_Ha9). % 0.83/1.04 apply (zenon_or_s _ _ zenon_Hae); [ zenon_intro zenon_Ha2 | zenon_intro zenon_Hb2 ]. % 0.83/1.04 apply (zenon_L18_ zenon_TY_bi zenon_TV_t); trivial. % 0.83/1.04 apply (zenon_or_s _ _ zenon_Hb2); [ zenon_intro zenon_Hb4 | zenon_intro zenon_Hb3 ]. % 0.83/1.04 exact (zenon_Haa zenon_Hb4). % 0.83/1.04 apply (zenon_or_s _ _ zenon_Hb3); [ zenon_intro zenon_H5f | zenon_intro zenon_H31 ]. % 0.83/1.04 exact (zenon_H5a zenon_H5f). % 0.83/1.04 apply (zenon_L6_ zenon_TV_t zenon_TU_u); trivial. % 0.83/1.04 (* end of lemma zenon_L19_ *) % 0.83/1.04 assert (zenon_L20_ : forall (zenon_TY_bi : zenon_U) (zenon_TV_t : zenon_U) (zenon_TU_u : zenon_U), (convergent_lines zenon_TU_u zenon_TV_t) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TY_bi)) -> (~(apart_point_and_line (intersection_point zenon_TV_t zenon_TY_bi) zenon_TV_t)) -> (convergent_lines zenon_TV_t zenon_TY_bi) -> (distinct_lines zenon_TY_bi zenon_TV_t) -> (distinct_points (intersection_point zenon_TV_t zenon_TY_bi) (intersection_point zenon_TU_u zenon_TV_t)) -> False). % 0.83/1.04 do 3 intro. intros zenon_H10 zenon_H5a zenon_Haa zenon_Ha3 zenon_Ha9 zenon_Ha8. % 0.83/1.04 generalize (cu1 (intersection_point zenon_TV_t zenon_TY_bi)). zenon_intro zenon_Ha7. % 0.83/1.04 apply (zenon_L19_ zenon_TU_u zenon_TY_bi zenon_TV_t); trivial. % 0.83/1.04 (* end of lemma zenon_L20_ *) % 0.83/1.04 assert (zenon_L21_ : forall (zenon_TU_u : zenon_U) (zenon_TX_bb : zenon_U) (zenon_TY_bi : zenon_U) (zenon_TV_t : zenon_U), (apart_point_and_line (intersection_point zenon_TV_t zenon_TY_bi) zenon_TX_bb) -> (convergent_lines zenon_TU_u zenon_TV_t) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TY_bi)) -> (~(apart_point_and_line (intersection_point zenon_TV_t zenon_TY_bi) zenon_TV_t)) -> (convergent_lines zenon_TV_t zenon_TY_bi) -> (distinct_lines zenon_TY_bi zenon_TV_t) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TX_bb)) -> False). % 0.83/1.04 do 4 intro. intros zenon_Hb5 zenon_H10 zenon_H5a zenon_Haa zenon_Ha3 zenon_Ha9 zenon_H4c. % 0.83/1.04 generalize (ceq1 (intersection_point zenon_TV_t zenon_TY_bi)). zenon_intro zenon_Hb6. % 0.83/1.04 generalize (zenon_Hb6 zenon_TX_bb). zenon_intro zenon_Hb7. % 0.83/1.04 generalize (zenon_Hb7 (intersection_point zenon_TU_u zenon_TV_t)). zenon_intro zenon_Hb8. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_Hb8); [ zenon_intro zenon_Hba | zenon_intro zenon_Hb9 ]. % 0.83/1.04 exact (zenon_Hba zenon_Hb5). % 0.83/1.04 apply (zenon_or_s _ _ zenon_Hb9); [ zenon_intro zenon_Ha8 | zenon_intro zenon_H57 ]. % 0.83/1.04 apply (zenon_L20_ zenon_TY_bi zenon_TV_t zenon_TU_u); trivial. % 0.83/1.04 exact (zenon_H4c zenon_H57). % 0.83/1.04 (* end of lemma zenon_L21_ *) % 0.83/1.04 assert (zenon_L22_ : forall (zenon_TU_u : zenon_U) (zenon_TV_t : zenon_U) (zenon_TY_bi : zenon_U) (zenon_TX_bb : zenon_U), (forall Z : zenon_U, ((apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) zenon_TV_t)->((distinct_points (intersection_point zenon_TX_bb zenon_TY_bi) Z)\/(apart_point_and_line Z zenon_TV_t)))) -> (apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) zenon_TV_t) -> (convergent_lines zenon_TU_u zenon_TV_t) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TY_bi)) -> (~(apart_point_and_line (intersection_point zenon_TV_t zenon_TY_bi) zenon_TV_t)) -> (convergent_lines zenon_TV_t zenon_TY_bi) -> (distinct_lines zenon_TY_bi zenon_TV_t) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TX_bb)) -> (forall Z : zenon_U, ((convergent_lines zenon_TX_bb zenon_TY_bi)->((convergent_lines zenon_TX_bb Z)\/(convergent_lines zenon_TY_bi Z)))) -> (convergent_lines zenon_TX_bb zenon_TY_bi) -> (~(convergent_lines zenon_TY_bi zenon_TY_bi)) -> (forall Y : zenon_U, (forall Z : zenon_U, ((convergent_lines zenon_TY_bi Y)->((distinct_lines Y Z)\/(convergent_lines zenon_TY_bi Z))))) -> False). % 0.83/1.04 do 4 intro. intros zenon_H90 zenon_H8d zenon_H10 zenon_H5a zenon_Haa zenon_Ha3 zenon_Ha9 zenon_H4c zenon_H21 zenon_H20 zenon_H1e zenon_H1d. % 0.83/1.04 generalize (zenon_H90 (intersection_point zenon_TV_t zenon_TY_bi)). zenon_intro zenon_Hbb. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_Hbb); [ zenon_intro zenon_Ha0 | zenon_intro zenon_Hbc ]. % 0.83/1.04 exact (zenon_Ha0 zenon_H8d). % 0.83/1.04 apply (zenon_or_s _ _ zenon_Hbc); [ zenon_intro zenon_Hbd | zenon_intro zenon_Hb4 ]. % 0.83/1.04 generalize (cu1 (intersection_point zenon_TX_bb zenon_TY_bi)). zenon_intro zenon_H70. % 0.83/1.04 generalize (zenon_H70 (intersection_point zenon_TV_t zenon_TY_bi)). zenon_intro zenon_Hbe. % 0.83/1.04 generalize (apart5 zenon_TX_bb). zenon_intro zenon_H7a. % 0.83/1.04 generalize (apart2 zenon_TY_bi). zenon_intro zenon_H71. % 0.83/1.04 generalize (zenon_H7a zenon_TY_bi). zenon_intro zenon_H7b. % 0.83/1.04 generalize (zenon_H7b zenon_TY_bi). zenon_intro zenon_H7c. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H7c); [ zenon_intro zenon_H1f | zenon_intro zenon_H7d ]. % 0.83/1.04 apply (zenon_L3_ zenon_TX_bb zenon_TY_bi); trivial. % 0.83/1.04 apply (zenon_or_s _ _ zenon_H7d); [ zenon_intro zenon_H2c | zenon_intro zenon_H7e ]. % 0.83/1.04 generalize (zenon_Hbe zenon_TX_bb). zenon_intro zenon_Hbf. % 0.83/1.04 generalize (zenon_Hbf zenon_TY_bi). zenon_intro zenon_Hc0. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_Hc0); [ zenon_intro zenon_Hc2 | zenon_intro zenon_Hc1 ]. % 0.83/1.04 apply (zenon_notand_s _ _ zenon_Hc2); [ zenon_intro zenon_Hc3 | zenon_intro zenon_H1f ]. % 0.83/1.04 exact (zenon_Hc3 zenon_Hbd). % 0.83/1.04 exact (zenon_H1f zenon_H2c). % 0.83/1.04 apply (zenon_or_s _ _ zenon_Hc1); [ zenon_intro zenon_H2e | zenon_intro zenon_Hc4 ]. % 0.83/1.04 apply (zenon_L5_ zenon_TY_bi zenon_TX_bb); trivial. % 0.83/1.04 apply (zenon_or_s _ _ zenon_Hc4); [ zenon_intro zenon_H6a | zenon_intro zenon_Hc5 ]. % 0.83/1.04 apply (zenon_L14_ zenon_TY_bi zenon_TX_bb); trivial. % 0.83/1.04 apply (zenon_or_s _ _ zenon_Hc5); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Ha2 ]. % 0.83/1.04 apply (zenon_L21_ zenon_TU_u zenon_TX_bb zenon_TY_bi zenon_TV_t); trivial. % 0.83/1.04 apply (zenon_L18_ zenon_TY_bi zenon_TV_t); trivial. % 0.83/1.04 exact (zenon_H71 zenon_H7e). % 0.83/1.04 exact (zenon_Haa zenon_Hb4). % 0.83/1.04 (* end of lemma zenon_L22_ *) % 0.83/1.04 assert (zenon_L23_ : forall (zenon_TU_u : zenon_U) (zenon_TX_bb : zenon_U) (zenon_TY_bi : zenon_U) (zenon_TV_t : zenon_U), (convergent_lines zenon_TV_t zenon_TY_bi) -> (apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) zenon_TV_t) -> (convergent_lines zenon_TU_u zenon_TV_t) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TY_bi)) -> (~(apart_point_and_line (intersection_point zenon_TV_t zenon_TY_bi) zenon_TV_t)) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TX_bb)) -> (forall Z : zenon_U, ((convergent_lines zenon_TX_bb zenon_TY_bi)->((convergent_lines zenon_TX_bb Z)\/(convergent_lines zenon_TY_bi Z)))) -> (convergent_lines zenon_TX_bb zenon_TY_bi) -> (~(convergent_lines zenon_TY_bi zenon_TY_bi)) -> (~(convergent_lines zenon_TV_t zenon_TV_t)) -> (forall Y : zenon_U, (forall Z : zenon_U, ((convergent_lines zenon_TV_t Y)->((distinct_lines Y Z)\/(convergent_lines zenon_TV_t Z))))) -> False). % 0.83/1.04 do 4 intro. intros zenon_Ha3 zenon_H8d zenon_H10 zenon_H5a zenon_Haa zenon_H4c zenon_H21 zenon_H20 zenon_H1e zenon_Hc6 zenon_Hc7. % 0.83/1.04 generalize (ceq3 zenon_TY_bi). zenon_intro zenon_H1d. % 0.83/1.04 generalize (zenon_Hc7 zenon_TY_bi). zenon_intro zenon_Hc8. % 0.83/1.04 generalize (zenon_Hc8 zenon_TV_t). zenon_intro zenon_Hc9. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_Hc9); [ zenon_intro zenon_Ha6 | zenon_intro zenon_Hca ]. % 0.83/1.04 exact (zenon_Ha6 zenon_Ha3). % 0.83/1.04 apply (zenon_or_s _ _ zenon_Hca); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Hcb ]. % 0.83/1.04 generalize (ceq1 (intersection_point zenon_TX_bb zenon_TY_bi)). zenon_intro zenon_H8f. % 0.83/1.04 generalize (zenon_H8f zenon_TV_t). zenon_intro zenon_H90. % 0.83/1.04 apply (zenon_L22_ zenon_TU_u zenon_TV_t zenon_TY_bi zenon_TX_bb); trivial. % 0.83/1.04 exact (zenon_Hc6 zenon_Hcb). % 0.83/1.04 (* end of lemma zenon_L23_ *) % 0.83/1.04 assert (zenon_L24_ : forall (zenon_TU_u : zenon_U) (zenon_TX_bb : zenon_U) (zenon_TY_bi : zenon_U) (zenon_TV_t : zenon_U), (~(convergent_lines zenon_TV_t zenon_TV_t)) -> (~(convergent_lines zenon_TY_bi zenon_TY_bi)) -> (convergent_lines zenon_TX_bb zenon_TY_bi) -> (forall Z : zenon_U, ((convergent_lines zenon_TX_bb zenon_TY_bi)->((convergent_lines zenon_TX_bb Z)\/(convergent_lines zenon_TY_bi Z)))) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TX_bb)) -> (~(apart_point_and_line (intersection_point zenon_TV_t zenon_TY_bi) zenon_TV_t)) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TY_bi)) -> (convergent_lines zenon_TU_u zenon_TV_t) -> (apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) zenon_TV_t) -> (convergent_lines zenon_TV_t zenon_TY_bi) -> False). % 0.83/1.04 do 4 intro. intros zenon_Hc6 zenon_H1e zenon_H20 zenon_H21 zenon_H4c zenon_Haa zenon_H5a zenon_H10 zenon_H8d zenon_Ha3. % 0.83/1.04 generalize (ceq3 zenon_TV_t). zenon_intro zenon_Hc7. % 0.83/1.04 apply (zenon_L23_ zenon_TU_u zenon_TX_bb zenon_TY_bi zenon_TV_t); trivial. % 0.83/1.04 (* end of lemma zenon_L24_ *) % 0.83/1.04 assert (zenon_L25_ : forall (zenon_TX_bb : zenon_U) (zenon_TY_bi : zenon_U) (zenon_TV_t : zenon_U) (zenon_TU_u : zenon_U), (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TY_bi)) -> (apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) zenon_TV_t) -> (convergent_lines zenon_TX_bb zenon_TY_bi) -> (~(apart_point_and_line (intersection_point zenon_TU_u zenon_TV_t) zenon_TX_bb)) -> (convergent_lines zenon_TU_u zenon_TV_t) -> False). % 0.83/1.04 do 4 intro. intros zenon_H5a zenon_H8d zenon_H20 zenon_H4c zenon_H10. % 0.83/1.04 generalize (ci3 zenon_TV_t). zenon_intro zenon_H49. % 0.83/1.04 generalize (ax6 zenon_TU_u). zenon_intro zenon_Hcc. % 0.83/1.04 generalize (apart3 zenon_TY_bi). zenon_intro zenon_H1e. % 0.83/1.04 generalize (apart3 zenon_TV_t). zenon_intro zenon_Hc6. % 0.83/1.04 generalize (ax6 zenon_TX_bb). zenon_intro zenon_Hcd. % 0.83/1.04 generalize (zenon_H49 zenon_TY_bi). zenon_intro zenon_Hce. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_Hce); [ zenon_intro zenon_Ha6 | zenon_intro zenon_Haa ]. % 0.83/1.04 generalize (ceq3 zenon_TU_u). zenon_intro zenon_H8a. % 0.83/1.04 generalize (zenon_Hcc zenon_TV_t). zenon_intro zenon_Hf. % 0.83/1.04 generalize (zenon_H8a zenon_TV_t). zenon_intro zenon_H8b. % 0.83/1.04 generalize (zenon_Hcd zenon_TY_bi). zenon_intro zenon_H21. % 0.83/1.04 generalize (zenon_Hf zenon_TY_bi). zenon_intro zenon_Hcf. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_Hcf); [ zenon_intro zenon_H17 | zenon_intro zenon_Hd0 ]. % 0.83/1.04 exact (zenon_H17 zenon_H10). % 0.83/1.04 apply (zenon_or_s _ _ zenon_Hd0); [ zenon_intro zenon_H8c | zenon_intro zenon_Ha3 ]. % 0.83/1.04 apply (zenon_L17_ zenon_TX_bb zenon_TY_bi zenon_TV_t zenon_TU_u); trivial. % 0.83/1.04 exact (zenon_Ha6 zenon_Ha3). % 0.83/1.04 generalize (ceq3 zenon_TU_u). zenon_intro zenon_H8a. % 0.83/1.04 generalize (zenon_Hcc zenon_TV_t). zenon_intro zenon_Hf. % 0.83/1.04 generalize (zenon_H8a zenon_TV_t). zenon_intro zenon_H8b. % 0.83/1.04 generalize (zenon_Hcd zenon_TY_bi). zenon_intro zenon_H21. % 0.83/1.04 generalize (zenon_Hf zenon_TY_bi). zenon_intro zenon_Hcf. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_Hcf); [ zenon_intro zenon_H17 | zenon_intro zenon_Hd0 ]. % 0.83/1.04 exact (zenon_H17 zenon_H10). % 0.83/1.04 apply (zenon_or_s _ _ zenon_Hd0); [ zenon_intro zenon_H8c | zenon_intro zenon_Ha3 ]. % 0.83/1.04 apply (zenon_L17_ zenon_TX_bb zenon_TY_bi zenon_TV_t zenon_TU_u); trivial. % 0.83/1.04 apply (zenon_L24_ zenon_TU_u zenon_TX_bb zenon_TY_bi zenon_TV_t); trivial. % 0.83/1.04 (* end of lemma zenon_L25_ *) % 0.83/1.04 apply NNPP. intro zenon_G. % 0.83/1.04 apply (zenon_notallex_s (fun X : zenon_U => (forall Y : zenon_U, (forall U : zenon_U, (forall V : zenon_U, (((convergent_lines X Y)/\((convergent_lines U V)/\((apart_point_and_line (intersection_point X Y) U)\/(apart_point_and_line (intersection_point X Y) V))))->((apart_point_and_line (intersection_point U V) X)\/(apart_point_and_line (intersection_point U V) Y))))))) zenon_G); [ zenon_intro zenon_Hd1; idtac ]. % 0.83/1.04 elim zenon_Hd1. zenon_intro zenon_TX_bb. zenon_intro zenon_Hd2. % 0.83/1.04 apply (zenon_notallex_s (fun Y : zenon_U => (forall U : zenon_U, (forall V : zenon_U, (((convergent_lines zenon_TX_bb Y)/\((convergent_lines U V)/\((apart_point_and_line (intersection_point zenon_TX_bb Y) U)\/(apart_point_and_line (intersection_point zenon_TX_bb Y) V))))->((apart_point_and_line (intersection_point U V) zenon_TX_bb)\/(apart_point_and_line (intersection_point U V) Y)))))) zenon_Hd2); [ zenon_intro zenon_Hd3; idtac ]. % 0.83/1.04 elim zenon_Hd3. zenon_intro zenon_TY_bi. zenon_intro zenon_Hd4. % 0.83/1.04 apply (zenon_notallex_s (fun U : zenon_U => (forall V : zenon_U, (((convergent_lines zenon_TX_bb zenon_TY_bi)/\((convergent_lines U V)/\((apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) U)\/(apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) V))))->((apart_point_and_line (intersection_point U V) zenon_TX_bb)\/(apart_point_and_line (intersection_point U V) zenon_TY_bi))))) zenon_Hd4); [ zenon_intro zenon_Hd5; idtac ]. % 0.83/1.04 elim zenon_Hd5. zenon_intro zenon_TU_u. zenon_intro zenon_Hd6. % 0.83/1.04 apply (zenon_notallex_s (fun V : zenon_U => (((convergent_lines zenon_TX_bb zenon_TY_bi)/\((convergent_lines zenon_TU_u V)/\((apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) zenon_TU_u)\/(apart_point_and_line (intersection_point zenon_TX_bb zenon_TY_bi) V))))->((apart_point_and_line (intersection_point zenon_TU_u V) zenon_TX_bb)\/(apart_point_and_line (intersection_point zenon_TU_u V) zenon_TY_bi)))) zenon_Hd6); [ zenon_intro zenon_Hd7; idtac ]. % 0.83/1.04 elim zenon_Hd7. zenon_intro zenon_TV_t. zenon_intro zenon_Hd8. % 0.83/1.04 apply (zenon_notimply_s _ _ zenon_Hd8). zenon_intro zenon_Hda. zenon_intro zenon_Hd9. % 0.83/1.04 apply (zenon_notor_s _ _ zenon_Hd9). zenon_intro zenon_H4c. zenon_intro zenon_H5a. % 0.83/1.04 apply (zenon_and_s _ _ zenon_Hda). zenon_intro zenon_H20. zenon_intro zenon_Hdb. % 0.83/1.04 apply (zenon_and_s _ _ zenon_Hdb). zenon_intro zenon_H10. zenon_intro zenon_Hdc. % 0.83/1.04 apply (zenon_or_s _ _ zenon_Hdc); [ zenon_intro zenon_H6f | zenon_intro zenon_H8d ]. % 0.83/1.04 generalize (ci3 zenon_TU_u). zenon_intro zenon_H35. % 0.83/1.04 generalize (ax6 zenon_TU_u). zenon_intro zenon_Hcc. % 0.83/1.04 generalize (apart3 zenon_TY_bi). zenon_intro zenon_H1e. % 0.83/1.04 generalize (ax6 zenon_TX_bb). zenon_intro zenon_Hcd. % 0.83/1.04 generalize (ceq3 zenon_TU_u). zenon_intro zenon_H8a. % 0.83/1.04 generalize (zenon_Hcc zenon_TV_t). zenon_intro zenon_Hf. % 0.83/1.04 generalize (zenon_H8a zenon_TV_t). zenon_intro zenon_H8b. % 0.83/1.04 generalize (zenon_Hcd zenon_TY_bi). zenon_intro zenon_H21. % 0.83/1.04 generalize (apart2 zenon_TV_t). zenon_intro zenon_H4d. % 0.83/1.04 generalize (ceq2 (intersection_point zenon_TX_bb zenon_TY_bi)). zenon_intro zenon_H6d. % 0.83/1.04 generalize (apart2 zenon_TY_bi). zenon_intro zenon_H71. % 0.83/1.04 generalize (ceq1 (intersection_point zenon_TX_bb zenon_TY_bi)). zenon_intro zenon_H8f. % 0.83/1.04 generalize (zenon_H8f zenon_TU_u). zenon_intro zenon_H6e. % 0.83/1.04 generalize (cu1 (intersection_point zenon_TX_bb zenon_TY_bi)). zenon_intro zenon_H70. % 0.83/1.04 generalize (ci3 zenon_TV_t). zenon_intro zenon_H49. % 0.83/1.04 generalize (zenon_H8b zenon_TU_u). zenon_intro zenon_H91. % 0.83/1.04 apply (zenon_imply_s _ _ zenon_H91); [ zenon_intro zenon_H17 | zenon_intro zenon_H92 ]. % 0.83/1.04 exact (zenon_H17 zenon_H10). % 0.83/1.04 apply (zenon_or_s _ _ zenon_H92); [ zenon_intro zenon_H3b | zenon_intro zenon_H19 ]. % 0.83/1.04 generalize (apart3 zenon_TU_u). zenon_intro zenon_H11. % 0.83/1.04 apply (zenon_L15_ zenon_TV_t zenon_TU_u zenon_TY_bi zenon_TX_bb); trivial. % 0.83/1.04 generalize (apart3 zenon_TU_u). zenon_intro zenon_H11. % 0.83/1.04 exact (zenon_H11 zenon_H19). % 0.83/1.04 apply (zenon_L25_ zenon_TX_bb zenon_TY_bi zenon_TV_t zenon_TU_u); trivial. % 0.83/1.04 Qed. % 0.83/1.04 % SZS output end Proof % 0.83/1.04 (* END-PROOF *) % 0.83/1.04 nodes searched: 38140 % 0.83/1.04 max branch formulas: 2464 % 0.83/1.04 proof nodes created: 3007 % 0.83/1.04 formulas created: 114394 % 0.83/1.04 %------------------------------------------------------------------------------