%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SEU386+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n017.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 : Tue Jul 19 16:01:42 EDT 2022 % Result : Theorem 3.23s 3.46s % Output : Proof 3.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SEU386+1 : TPTP v8.1.0. Released v3.3.0. % 0.10/0.12 % Command : run_zenon %s %d % 0.13/0.33 % Computer : n017.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Sun Jun 19 08:12:43 EDT 2022 % 0.13/0.33 % CPUTime : % 3.23/3.46 Zenon warning: unused variable (B : zenon_U) in reflexivity_r1_tarski % 3.23/3.46 (* PROOF-FOUND *) % 3.23/3.46 % SZS status Theorem % 3.23/3.46 (* BEGIN-PROOF *) % 3.23/3.46 % SZS output start Proof % 3.23/3.46 Theorem t29_waybel_9 : (forall A : zenon_U, (((~(empty_carrier A))/\((topological_space A)/\(top_str A)))->(forall B : zenon_U, (((~(empty_carrier B))/\((transitive_relstr B)/\((directed_relstr B)/\(net_str B A))))->(forall C : zenon_U, ((element C (the_carrier A))->((in C (lim_points_of_net A B))->(is_a_cluster_point_of_netstr A B C)))))))). % 3.23/3.46 Proof. % 3.23/3.46 assert (zenon_L1_ : forall (zenon_TB_bw : zenon_U) (zenon_TA_bx : zenon_U), (~(element (lim_points_of_net zenon_TA_bx zenon_TB_bw) (powerset (the_carrier zenon_TA_bx)))) -> (net_str zenon_TB_bw zenon_TA_bx) -> (directed_relstr zenon_TB_bw) -> (transitive_relstr zenon_TB_bw) -> (~(empty_carrier zenon_TB_bw)) -> (top_str zenon_TA_bx) -> (topological_space zenon_TA_bx) -> (~(empty_carrier zenon_TA_bx)) -> False). % 3.23/3.46 do 2 intro. intros zenon_H28 zenon_H29 zenon_H2a zenon_H2b zenon_H2c zenon_H2d zenon_H2e zenon_H2f. % 3.23/3.46 generalize (dt_k11_yellow_6 zenon_TA_bx). zenon_intro zenon_H32. % 3.23/3.46 generalize (zenon_H32 zenon_TB_bw). zenon_intro zenon_H33. % 3.23/3.46 apply (zenon_imply_s _ _ zenon_H33); [ zenon_intro zenon_H35 | zenon_intro zenon_H34 ]. % 3.23/3.46 apply (zenon_notand_s _ _ zenon_H35); [ zenon_intro zenon_H37 | zenon_intro zenon_H36 ]. % 3.23/3.46 exact (zenon_H37 zenon_H2f). % 3.23/3.46 apply (zenon_notand_s _ _ zenon_H36); [ zenon_intro zenon_H39 | zenon_intro zenon_H38 ]. % 3.23/3.46 exact (zenon_H39 zenon_H2e). % 3.23/3.46 apply (zenon_notand_s _ _ zenon_H38); [ zenon_intro zenon_H3b | zenon_intro zenon_H3a ]. % 3.23/3.46 exact (zenon_H3b zenon_H2d). % 3.23/3.46 apply (zenon_notand_s _ _ zenon_H3a); [ zenon_intro zenon_H3d | zenon_intro zenon_H3c ]. % 3.23/3.46 exact (zenon_H3d zenon_H2c). % 3.23/3.46 apply (zenon_notand_s _ _ zenon_H3c); [ zenon_intro zenon_H3f | zenon_intro zenon_H3e ]. % 3.23/3.46 exact (zenon_H3f zenon_H2b). % 3.23/3.46 apply (zenon_notand_s _ _ zenon_H3e); [ zenon_intro zenon_H41 | zenon_intro zenon_H40 ]. % 3.23/3.46 exact (zenon_H41 zenon_H2a). % 3.23/3.46 exact (zenon_H40 zenon_H29). % 3.23/3.46 exact (zenon_H28 zenon_H34). % 3.23/3.46 (* end of lemma zenon_L1_ *) % 3.23/3.46 assert (zenon_L2_ : forall (zenon_TD_cr : zenon_U) (zenon_TB_bw : zenon_U) (zenon_TC_cs : zenon_U) (zenon_TA_bx : zenon_U), (forall E : zenon_U, ((point_neighbourhood E zenon_TA_bx zenon_TC_cs)->(is_eventually_in zenon_TA_bx zenon_TB_bw E))) -> (point_neighbourhood zenon_TD_cr zenon_TA_bx zenon_TC_cs) -> (~(is_eventually_in zenon_TA_bx zenon_TB_bw zenon_TD_cr)) -> False). % 3.23/3.46 do 4 intro. intros zenon_H42 zenon_H43 zenon_H44. % 3.23/3.46 generalize (zenon_H42 zenon_TD_cr). zenon_intro zenon_H47. % 3.23/3.46 apply (zenon_imply_s _ _ zenon_H47); [ zenon_intro zenon_H49 | zenon_intro zenon_H48 ]. % 3.23/3.46 exact (zenon_H49 zenon_H43). % 3.23/3.46 exact (zenon_H44 zenon_H48). % 3.23/3.46 (* end of lemma zenon_L2_ *) % 3.23/3.46 apply NNPP. intro zenon_G. % 3.23/3.46 apply (zenon_notallex_s (fun A : zenon_U => (((~(empty_carrier A))/\((topological_space A)/\(top_str A)))->(forall B : zenon_U, (((~(empty_carrier B))/\((transitive_relstr B)/\((directed_relstr B)/\(net_str B A))))->(forall C : zenon_U, ((element C (the_carrier A))->((in C (lim_points_of_net A B))->(is_a_cluster_point_of_netstr A B C)))))))) zenon_G); [ zenon_intro zenon_H4a; idtac ]. % 3.23/3.46 elim zenon_H4a. zenon_intro zenon_TA_bx. zenon_intro zenon_H4b. % 3.23/3.46 apply (zenon_notimply_s _ _ zenon_H4b). zenon_intro zenon_H4d. zenon_intro zenon_H4c. % 3.23/3.46 apply (zenon_and_s _ _ zenon_H4d). zenon_intro zenon_H2f. zenon_intro zenon_H4e. % 3.23/3.46 apply (zenon_and_s _ _ zenon_H4e). zenon_intro zenon_H2e. zenon_intro zenon_H2d. % 3.23/3.46 apply (zenon_notallex_s (fun B : zenon_U => (((~(empty_carrier B))/\((transitive_relstr B)/\((directed_relstr B)/\(net_str B zenon_TA_bx))))->(forall C : zenon_U, ((element C (the_carrier zenon_TA_bx))->((in C (lim_points_of_net zenon_TA_bx B))->(is_a_cluster_point_of_netstr zenon_TA_bx B C)))))) zenon_H4c); [ zenon_intro zenon_H4f; idtac ]. % 3.23/3.46 elim zenon_H4f. zenon_intro zenon_TB_bw. zenon_intro zenon_H50. % 3.23/3.46 apply (zenon_notimply_s _ _ zenon_H50). zenon_intro zenon_H52. zenon_intro zenon_H51. % 3.23/3.46 apply (zenon_and_s _ _ zenon_H52). zenon_intro zenon_H2c. zenon_intro zenon_H53. % 3.23/3.46 apply (zenon_and_s _ _ zenon_H53). zenon_intro zenon_H2b. zenon_intro zenon_H54. % 3.23/3.46 apply (zenon_and_s _ _ zenon_H54). zenon_intro zenon_H2a. zenon_intro zenon_H29. % 3.23/3.46 apply (zenon_notallex_s (fun C : zenon_U => ((element C (the_carrier zenon_TA_bx))->((in C (lim_points_of_net zenon_TA_bx zenon_TB_bw))->(is_a_cluster_point_of_netstr zenon_TA_bx zenon_TB_bw C)))) zenon_H51); [ zenon_intro zenon_H55; idtac ]. % 3.23/3.46 elim zenon_H55. zenon_intro zenon_TC_cs. zenon_intro zenon_H56. % 3.23/3.46 apply (zenon_notimply_s _ _ zenon_H56). zenon_intro zenon_H58. zenon_intro zenon_H57. % 3.23/3.46 apply (zenon_notimply_s _ _ zenon_H57). zenon_intro zenon_H5a. zenon_intro zenon_H59. % 3.23/3.46 generalize (d9_waybel_9 zenon_TA_bx). zenon_intro zenon_H5b. % 3.23/3.46 apply (zenon_imply_s _ _ zenon_H5b); [ zenon_intro zenon_H5d | zenon_intro zenon_H5c ]. % 3.23/3.46 apply (zenon_notand_s _ _ zenon_H5d); [ zenon_intro zenon_H37 | zenon_intro zenon_H5e ]. % 3.23/3.46 exact (zenon_H37 zenon_H2f). % 3.23/3.46 apply (zenon_notand_s _ _ zenon_H5e); [ zenon_intro zenon_H39 | zenon_intro zenon_H3b ]. % 3.23/3.46 exact (zenon_H39 zenon_H2e). % 3.23/3.46 exact (zenon_H3b zenon_H2d). % 3.23/3.46 generalize (zenon_H5c zenon_TB_bw). zenon_intro zenon_H5f. % 3.23/3.46 apply (zenon_imply_s _ _ zenon_H5f); [ zenon_intro zenon_H61 | zenon_intro zenon_H60 ]. % 3.23/3.46 apply (zenon_notand_s _ _ zenon_H61); [ zenon_intro zenon_H3d | zenon_intro zenon_H40 ]. % 3.23/3.46 exact (zenon_H3d zenon_H2c). % 3.23/3.46 exact (zenon_H40 zenon_H29). % 3.23/3.46 generalize (zenon_H60 zenon_TC_cs). zenon_intro zenon_H62. % 3.23/3.46 apply (zenon_imply_s _ _ zenon_H62); [ zenon_intro zenon_H64 | zenon_intro zenon_H63 ]. % 3.23/3.46 exact (zenon_H64 zenon_H58). % 3.23/3.46 apply (zenon_equiv_s _ _ zenon_H63); [ zenon_intro zenon_H59; zenon_intro zenon_H67 | zenon_intro zenon_H66; zenon_intro zenon_H65 ]. % 3.23/3.46 apply (zenon_notallex_s (fun D : zenon_U => ((point_neighbourhood D zenon_TA_bx zenon_TC_cs)->(is_often_in zenon_TA_bx zenon_TB_bw D))) zenon_H67); [ zenon_intro zenon_H68; idtac ]. % 3.23/3.46 elim zenon_H68. zenon_intro zenon_TD_cr. zenon_intro zenon_H69. % 3.23/3.46 apply (zenon_notimply_s _ _ zenon_H69). zenon_intro zenon_H43. zenon_intro zenon_H6a. % 3.23/3.46 generalize (t28_yellow_6 zenon_TA_bx). zenon_intro zenon_H6b. % 3.23/3.46 apply (zenon_imply_s _ _ zenon_H6b); [ zenon_intro zenon_H6d | zenon_intro zenon_H6c ]. % 3.23/3.46 apply (zenon_notand_s _ _ zenon_H6d); [ zenon_intro zenon_H37 | zenon_intro zenon_H6e ]. % 3.23/3.46 exact (zenon_H37 zenon_H2f). % 3.23/3.46 generalize (dt_l1_pre_topc zenon_TA_bx). zenon_intro zenon_H6f. % 3.23/3.46 apply (zenon_imply_s _ _ zenon_H6f); [ zenon_intro zenon_H3b | zenon_intro zenon_H70 ]. % 3.23/3.46 exact (zenon_H3b zenon_H2d). % 3.23/3.46 exact (zenon_H6e zenon_H70). % 3.23/3.46 generalize (zenon_H6c zenon_TB_bw). zenon_intro zenon_H71. % 3.23/3.46 apply (zenon_imply_s _ _ zenon_H71); [ zenon_intro zenon_H3a | zenon_intro zenon_H72 ]. % 3.23/3.46 apply (zenon_notand_s _ _ zenon_H3a); [ zenon_intro zenon_H3d | zenon_intro zenon_H3c ]. % 3.23/3.46 exact (zenon_H3d zenon_H2c). % 3.23/3.46 apply (zenon_notand_s _ _ zenon_H3c); [ zenon_intro zenon_H3f | zenon_intro zenon_H3e ]. % 3.23/3.46 exact (zenon_H3f zenon_H2b). % 3.23/3.46 apply (zenon_notand_s _ _ zenon_H3e); [ zenon_intro zenon_H41 | zenon_intro zenon_H40 ]. % 3.23/3.46 exact (zenon_H41 zenon_H2a). % 3.23/3.46 exact (zenon_H40 zenon_H29). % 3.23/3.46 generalize (zenon_H72 zenon_TD_cr). zenon_intro zenon_H73. % 3.23/3.46 apply (zenon_imply_s _ _ zenon_H73); [ zenon_intro zenon_H44 | zenon_intro zenon_H74 ]. % 3.23/3.46 generalize (d18_yellow_6 zenon_TA_bx). zenon_intro zenon_H75. % 3.23/3.46 apply (zenon_imply_s _ _ zenon_H75); [ zenon_intro zenon_H5d | zenon_intro zenon_H76 ]. % 3.23/3.46 apply (zenon_notand_s _ _ zenon_H5d); [ zenon_intro zenon_H37 | zenon_intro zenon_H5e ]. % 3.23/3.46 exact (zenon_H37 zenon_H2f). % 3.23/3.46 apply (zenon_notand_s _ _ zenon_H5e); [ zenon_intro zenon_H39 | zenon_intro zenon_H3b ]. % 3.23/3.46 exact (zenon_H39 zenon_H2e). % 3.23/3.46 exact (zenon_H3b zenon_H2d). % 3.23/3.46 generalize (zenon_H76 zenon_TB_bw). zenon_intro zenon_H77. % 3.23/3.46 apply (zenon_imply_s _ _ zenon_H77); [ zenon_intro zenon_H3a | zenon_intro zenon_H78 ]. % 3.23/3.46 apply (zenon_notand_s _ _ zenon_H3a); [ zenon_intro zenon_H3d | zenon_intro zenon_H3c ]. % 3.23/3.46 exact (zenon_H3d zenon_H2c). % 3.23/3.46 apply (zenon_notand_s _ _ zenon_H3c); [ zenon_intro zenon_H3f | zenon_intro zenon_H3e ]. % 3.23/3.46 exact (zenon_H3f zenon_H2b). % 3.23/3.46 apply (zenon_notand_s _ _ zenon_H3e); [ zenon_intro zenon_H41 | zenon_intro zenon_H40 ]. % 3.23/3.46 exact (zenon_H41 zenon_H2a). % 3.23/3.46 exact (zenon_H40 zenon_H29). % 3.23/3.46 generalize (zenon_H78 (lim_points_of_net zenon_TA_bx zenon_TB_bw)). zenon_intro zenon_H79. % 3.23/3.46 apply (zenon_imply_s _ _ zenon_H79); [ zenon_intro zenon_H28 | zenon_intro zenon_H7a ]. % 3.23/3.46 apply (zenon_L1_ zenon_TB_bw zenon_TA_bx); trivial. % 3.23/3.46 apply (zenon_equiv_s _ _ zenon_H7a); [ zenon_intro zenon_H7e; zenon_intro zenon_H7d | zenon_intro zenon_H7c; zenon_intro zenon_H7b ]. % 3.23/3.46 apply zenon_H7e. apply refl_equal. % 3.23/3.46 generalize (zenon_H7b zenon_TC_cs). zenon_intro zenon_H7f. % 3.23/3.46 apply (zenon_imply_s _ _ zenon_H7f); [ zenon_intro zenon_H64 | zenon_intro zenon_H80 ]. % 3.23/3.46 exact (zenon_H64 zenon_H58). % 3.23/3.46 apply (zenon_equiv_s _ _ zenon_H80); [ zenon_intro zenon_H82; zenon_intro zenon_H81 | zenon_intro zenon_H5a; zenon_intro zenon_H42 ]. % 3.23/3.46 exact (zenon_H82 zenon_H5a). % 3.23/3.46 apply (zenon_L2_ zenon_TD_cr zenon_TB_bw zenon_TC_cs zenon_TA_bx); trivial. % 3.23/3.46 exact (zenon_H6a zenon_H74). % 3.23/3.46 exact (zenon_H59 zenon_H66). % 3.23/3.46 Qed. % 3.23/3.46 % SZS output end Proof % 3.23/3.46 (* END-PROOF *) % 3.23/3.46 nodes searched: 125492 % 3.23/3.46 max branch formulas: 9724 % 3.23/3.46 proof nodes created: 6485 % 3.23/3.46 formulas created: 373974 % 3.23/3.46 %------------------------------------------------------------------------------