%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR034+1 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n028.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 00:01:55 EDT 2022 % Result : Theorem 0.19s 0.53s % Output : Proof 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : CSR034+1 : TPTP v8.1.0. Released v3.4.0. % 0.07/0.13 % Command : run_zenon %s %d % 0.12/0.34 % Computer : n028.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 : Sat Jun 11 19:17:20 EDT 2022 % 0.12/0.34 % CPUTime : % 0.19/0.53 (* PROOF-FOUND *) % 0.19/0.53 % SZS status Theorem % 0.19/0.53 (* BEGIN-PROOF *) % 0.19/0.53 % SZS output start Proof % 0.19/0.53 Theorem query34 : (exists COL : zenon_U, ((mtvisible (c_tptp_member3515_mt))->(isa (c_wanica_districtsuriname) COL))). % 0.19/0.53 Proof. % 0.19/0.53 apply NNPP. intro zenon_G. % 0.19/0.53 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genlmt x y)->((genlmt y z)->(genlmt x z))))))); [ zenon_intro zenon_H3c | zenon_intro zenon_H3d ]. % 0.19/0.53 apply (zenon_imply_s _ _ just14); [ zenon_intro zenon_H3f | zenon_intro zenon_H3e ]. % 0.19/0.53 apply zenon_G. exists zenon_E. apply NNPP. zenon_intro zenon_H40. % 0.19/0.53 apply (zenon_notimply_s _ _ zenon_H40). zenon_intro zenon_H42. zenon_intro zenon_H41. % 0.19/0.53 generalize (just62 (c_tptp_member3515_mt)). zenon_intro zenon_H43. % 0.19/0.53 generalize (zenon_H43 (c_worldgeographymt)). zenon_intro zenon_H44. % 0.19/0.53 apply (zenon_imply_s _ _ zenon_H44); [ zenon_intro zenon_H46 | zenon_intro zenon_H45 ]. % 0.19/0.53 apply (zenon_notand_s _ _ zenon_H46); [ zenon_intro zenon_H48 | zenon_intro zenon_H47 ]. % 0.19/0.53 exact (zenon_H48 zenon_H42). % 0.19/0.53 elim (classic ((~((c_tptp_member3515_mt) = (c_worldgeographydualistmt)))/\(~(genlmt (c_tptp_member3515_mt) (c_worldgeographydualistmt))))); [ zenon_intro zenon_H49 | zenon_intro zenon_H4a ]. % 0.19/0.53 apply (zenon_and_s _ _ zenon_H49). zenon_intro zenon_H4c. zenon_intro zenon_H4b. % 0.19/0.53 elim (classic ((~((c_tptp_member3515_mt) = (c_unitedstatesgeographydualistmt)))/\(~(genlmt (c_tptp_member3515_mt) (c_unitedstatesgeographydualistmt))))); [ zenon_intro zenon_H4d | zenon_intro zenon_H4e ]. % 0.19/0.53 apply (zenon_and_s _ _ zenon_H4d). zenon_intro zenon_H50. zenon_intro zenon_H4f. % 0.19/0.53 elim (classic ((~((c_tptp_member3515_mt) = (c_worldcompletedualistgeographymt)))/\(~(genlmt (c_tptp_member3515_mt) (c_worldcompletedualistgeographymt))))); [ zenon_intro zenon_H51 | zenon_intro zenon_H52 ]. % 0.19/0.53 apply (zenon_and_s _ _ zenon_H51). zenon_intro zenon_H54. zenon_intro zenon_H53. % 0.19/0.53 elim (classic ((~((c_tptp_member3515_mt) = (c_ethnicgroupsvocabularymt)))/\(~(genlmt (c_tptp_member3515_mt) (c_ethnicgroupsvocabularymt))))); [ zenon_intro zenon_H55 | zenon_intro zenon_H56 ]. % 0.19/0.53 apply (zenon_and_s _ _ zenon_H55). zenon_intro zenon_H58. zenon_intro zenon_H57. % 0.19/0.53 elim (classic ((~((c_tptp_member3515_mt) = (c_ethnicgroupsmt)))/\(~(genlmt (c_tptp_member3515_mt) (c_ethnicgroupsmt))))); [ zenon_intro zenon_H59 | zenon_intro zenon_H5a ]. % 0.19/0.53 apply (zenon_and_s _ _ zenon_H59). zenon_intro zenon_H5c. zenon_intro zenon_H5b. % 0.19/0.53 elim (classic ((~((c_tptp_member3515_mt) = (c_massmediadatamt)))/\(~(genlmt (c_tptp_member3515_mt) (c_massmediadatamt))))); [ zenon_intro zenon_H5d | zenon_intro zenon_H5e ]. % 0.19/0.53 apply (zenon_and_s _ _ zenon_H5d). zenon_intro zenon_H60. zenon_intro zenon_H5f. % 0.19/0.53 elim (classic ((~((c_tptp_member3515_mt) = (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))))/\(~(genlmt (c_tptp_member3515_mt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)))))); [ zenon_intro zenon_H61 | zenon_intro zenon_H62 ]. % 0.19/0.53 apply (zenon_and_s _ _ zenon_H61). zenon_intro zenon_H64. zenon_intro zenon_H63. % 0.19/0.53 elim (classic ((~((c_tptp_member3515_mt) = (c_organizationdatamt)))/\(~(genlmt (c_tptp_member3515_mt) (c_organizationdatamt))))); [ zenon_intro zenon_H65 | zenon_intro zenon_H66 ]. % 0.19/0.53 apply (zenon_and_s _ _ zenon_H65). zenon_intro zenon_H68. zenon_intro zenon_H67. % 0.19/0.53 elim (classic ((~((c_tptp_member3515_mt) = (c_nooescapearchitecturemt)))/\(~(genlmt (c_tptp_member3515_mt) (c_nooescapearchitecturemt))))); [ zenon_intro zenon_H69 | zenon_intro zenon_H6a ]. % 0.19/0.53 apply (zenon_and_s _ _ zenon_H69). zenon_intro zenon_H6c. zenon_intro zenon_H6b. % 0.19/0.53 elim (classic ((~((c_tptp_member3515_mt) = (c_testvocabularymt)))/\(~(genlmt (c_tptp_member3515_mt) (c_testvocabularymt))))); [ zenon_intro zenon_H6d | zenon_intro zenon_H6e ]. % 0.19/0.53 apply (zenon_and_s _ _ zenon_H6d). zenon_intro zenon_H70. zenon_intro zenon_H6f. % 0.19/0.53 elim (classic ((~((c_tptp_member3515_mt) = (c_keinteractionresourcetestmt)))/\(~(genlmt (c_tptp_member3515_mt) (c_keinteractionresourcetestmt))))); [ zenon_intro zenon_H71 | zenon_intro zenon_H72 ]. % 0.19/0.53 apply (zenon_and_s _ _ zenon_H71). zenon_intro zenon_H74. zenon_intro zenon_H73. % 0.19/0.53 elim (classic ((~((c_tptp_member3515_mt) = (c_cyclistsmt)))/\(~(genlmt (c_tptp_member3515_mt) (c_cyclistsmt))))); [ zenon_intro zenon_H75 | zenon_intro zenon_H76 ]. % 0.19/0.53 apply (zenon_and_s _ _ zenon_H75). zenon_intro zenon_H78. zenon_intro zenon_H77. % 0.19/0.53 elim (classic ((~((c_tptp_member3515_mt) = (c_tptp_spindleheadmt)))/\(~(genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt))))); [ zenon_intro zenon_H79 | zenon_intro zenon_H7a ]. % 0.19/0.53 apply (zenon_and_s _ _ zenon_H79). zenon_intro zenon_H7c. zenon_intro zenon_H7b. % 0.19/0.53 exact (zenon_H7b just19). % 0.19/0.53 cut ((genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) = (genlmt (c_tptp_member3515_mt) (c_cyclistsmt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_H77. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact just18. % 0.19/0.53 cut (((c_cyclistsmt) = (c_cyclistsmt))); [idtac | apply NNPP; zenon_intro zenon_H7d]. % 0.19/0.53 cut (((c_tptp_spindleheadmt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H7e]. % 0.19/0.53 congruence. % 0.19/0.53 apply (zenon_notand_s _ _ zenon_H7a); [ zenon_intro zenon_H80 | zenon_intro zenon_H7f ]. % 0.19/0.53 apply zenon_H80. zenon_intro zenon_H81. % 0.19/0.53 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H82 | zenon_intro zenon_H83 ]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_tptp_spindleheadmt) = (c_tptp_member3515_mt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_H7e. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact zenon_H82. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H83]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_spindleheadmt))); [idtac | apply NNPP; zenon_intro zenon_H7c]. % 0.19/0.53 congruence. % 0.19/0.53 exact (zenon_H7c zenon_H81). % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_H7f. zenon_intro just19. % 0.19/0.53 generalize (zenon_H3c (c_tptp_member3515_mt)). zenon_intro zenon_H84. % 0.19/0.53 generalize (zenon_H84 (c_tptp_spindleheadmt)). zenon_intro zenon_H85. % 0.19/0.53 generalize (zenon_H85 (c_cyclistsmt)). zenon_intro zenon_H86. % 0.19/0.53 apply (zenon_imply_s _ _ zenon_H86); [ zenon_intro zenon_H7b | zenon_intro zenon_H87 ]. % 0.19/0.53 exact (zenon_H7b just19). % 0.19/0.53 apply (zenon_imply_s _ _ zenon_H87); [ zenon_intro zenon_H89 | zenon_intro zenon_H88 ]. % 0.19/0.53 exact (zenon_H89 just18). % 0.19/0.53 exact (zenon_H77 zenon_H88). % 0.19/0.53 apply zenon_H7d. apply refl_equal. % 0.19/0.53 cut ((genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) = (genlmt (c_tptp_member3515_mt) (c_keinteractionresourcetestmt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_H73. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact just9. % 0.19/0.53 cut (((c_keinteractionresourcetestmt) = (c_keinteractionresourcetestmt))); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 0.19/0.53 cut (((c_cyclistsmt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H8b]. % 0.19/0.53 congruence. % 0.19/0.53 apply (zenon_notand_s _ _ zenon_H76); [ zenon_intro zenon_H8d | zenon_intro zenon_H8c ]. % 0.19/0.53 apply zenon_H8d. zenon_intro zenon_H8e. % 0.19/0.53 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H82 | zenon_intro zenon_H83 ]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_cyclistsmt) = (c_tptp_member3515_mt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_H8b. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact zenon_H82. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H83]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_cyclistsmt))); [idtac | apply NNPP; zenon_intro zenon_H78]. % 0.19/0.53 congruence. % 0.19/0.53 exact (zenon_H78 zenon_H8e). % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_H8c. zenon_intro zenon_H88. % 0.19/0.53 generalize (zenon_H3c (c_tptp_member3515_mt)). zenon_intro zenon_H84. % 0.19/0.53 generalize (zenon_H84 (c_cyclistsmt)). zenon_intro zenon_H8f. % 0.19/0.53 generalize (zenon_H8f (c_keinteractionresourcetestmt)). zenon_intro zenon_H90. % 0.19/0.53 apply (zenon_imply_s _ _ zenon_H90); [ zenon_intro zenon_H77 | zenon_intro zenon_H91 ]. % 0.19/0.53 exact (zenon_H77 zenon_H88). % 0.19/0.53 apply (zenon_imply_s _ _ zenon_H91); [ zenon_intro zenon_H93 | zenon_intro zenon_H92 ]. % 0.19/0.53 exact (zenon_H93 just9). % 0.19/0.53 exact (zenon_H73 zenon_H92). % 0.19/0.53 apply zenon_H8a. apply refl_equal. % 0.19/0.53 cut ((genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) = (genlmt (c_tptp_member3515_mt) (c_testvocabularymt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_H6f. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact just10. % 0.19/0.53 cut (((c_testvocabularymt) = (c_testvocabularymt))); [idtac | apply NNPP; zenon_intro zenon_H94]. % 0.19/0.53 cut (((c_keinteractionresourcetestmt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H95]. % 0.19/0.53 congruence. % 0.19/0.53 apply (zenon_notand_s _ _ zenon_H72); [ zenon_intro zenon_H97 | zenon_intro zenon_H96 ]. % 0.19/0.53 apply zenon_H97. zenon_intro zenon_H98. % 0.19/0.53 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H82 | zenon_intro zenon_H83 ]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_keinteractionresourcetestmt) = (c_tptp_member3515_mt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_H95. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact zenon_H82. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H83]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_keinteractionresourcetestmt))); [idtac | apply NNPP; zenon_intro zenon_H74]. % 0.19/0.53 congruence. % 0.19/0.53 exact (zenon_H74 zenon_H98). % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_H96. zenon_intro zenon_H92. % 0.19/0.53 generalize (zenon_H3c (c_tptp_member3515_mt)). zenon_intro zenon_H84. % 0.19/0.53 generalize (zenon_H84 (c_keinteractionresourcetestmt)). zenon_intro zenon_H99. % 0.19/0.53 generalize (zenon_H99 (c_testvocabularymt)). zenon_intro zenon_H9a. % 0.19/0.53 apply (zenon_imply_s _ _ zenon_H9a); [ zenon_intro zenon_H73 | zenon_intro zenon_H9b ]. % 0.19/0.53 exact (zenon_H73 zenon_H92). % 0.19/0.53 apply (zenon_imply_s _ _ zenon_H9b); [ zenon_intro zenon_H9d | zenon_intro zenon_H9c ]. % 0.19/0.53 exact (zenon_H9d just10). % 0.19/0.53 exact (zenon_H6f zenon_H9c). % 0.19/0.53 apply zenon_H94. apply refl_equal. % 0.19/0.53 cut ((genlmt (c_testvocabularymt) (c_nooescapearchitecturemt)) = (genlmt (c_tptp_member3515_mt) (c_nooescapearchitecturemt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_H6b. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact just5. % 0.19/0.53 cut (((c_nooescapearchitecturemt) = (c_nooescapearchitecturemt))); [idtac | apply NNPP; zenon_intro zenon_H9e]. % 0.19/0.53 cut (((c_testvocabularymt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H9f]. % 0.19/0.53 congruence. % 0.19/0.53 apply (zenon_notand_s _ _ zenon_H6e); [ zenon_intro zenon_Ha1 | zenon_intro zenon_Ha0 ]. % 0.19/0.53 apply zenon_Ha1. zenon_intro zenon_Ha2. % 0.19/0.53 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H82 | zenon_intro zenon_H83 ]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_testvocabularymt) = (c_tptp_member3515_mt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_H9f. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact zenon_H82. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H83]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_testvocabularymt))); [idtac | apply NNPP; zenon_intro zenon_H70]. % 0.19/0.53 congruence. % 0.19/0.53 exact (zenon_H70 zenon_Ha2). % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_Ha0. zenon_intro zenon_H9c. % 0.19/0.53 generalize (zenon_H3c (c_tptp_member3515_mt)). zenon_intro zenon_H84. % 0.19/0.53 generalize (zenon_H84 (c_testvocabularymt)). zenon_intro zenon_Ha3. % 0.19/0.53 generalize (zenon_Ha3 (c_nooescapearchitecturemt)). zenon_intro zenon_Ha4. % 0.19/0.53 apply (zenon_imply_s _ _ zenon_Ha4); [ zenon_intro zenon_H6f | zenon_intro zenon_Ha5 ]. % 0.19/0.53 exact (zenon_H6f zenon_H9c). % 0.19/0.53 apply (zenon_imply_s _ _ zenon_Ha5); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Ha6 ]. % 0.19/0.53 exact (zenon_Ha7 just5). % 0.19/0.53 exact (zenon_H6b zenon_Ha6). % 0.19/0.53 apply zenon_H9e. apply refl_equal. % 0.19/0.53 cut ((genlmt (c_nooescapearchitecturemt) (c_organizationdatamt)) = (genlmt (c_tptp_member3515_mt) (c_organizationdatamt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_H67. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact just4. % 0.19/0.53 cut (((c_organizationdatamt) = (c_organizationdatamt))); [idtac | apply NNPP; zenon_intro zenon_Ha8]. % 0.19/0.53 cut (((c_nooescapearchitecturemt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_Ha9]. % 0.19/0.53 congruence. % 0.19/0.53 apply (zenon_notand_s _ _ zenon_H6a); [ zenon_intro zenon_Hab | zenon_intro zenon_Haa ]. % 0.19/0.53 apply zenon_Hab. zenon_intro zenon_Hac. % 0.19/0.53 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H82 | zenon_intro zenon_H83 ]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_nooescapearchitecturemt) = (c_tptp_member3515_mt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_Ha9. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact zenon_H82. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H83]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_nooescapearchitecturemt))); [idtac | apply NNPP; zenon_intro zenon_H6c]. % 0.19/0.53 congruence. % 0.19/0.53 exact (zenon_H6c zenon_Hac). % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_Haa. zenon_intro zenon_Ha6. % 0.19/0.53 generalize (zenon_H3c (c_tptp_member3515_mt)). zenon_intro zenon_H84. % 0.19/0.53 generalize (zenon_H84 (c_nooescapearchitecturemt)). zenon_intro zenon_Had. % 0.19/0.53 generalize (zenon_Had (c_organizationdatamt)). zenon_intro zenon_Hae. % 0.19/0.53 apply (zenon_imply_s _ _ zenon_Hae); [ zenon_intro zenon_H6b | zenon_intro zenon_Haf ]. % 0.19/0.53 exact (zenon_H6b zenon_Ha6). % 0.19/0.53 apply (zenon_imply_s _ _ zenon_Haf); [ zenon_intro zenon_Hb1 | zenon_intro zenon_Hb0 ]. % 0.19/0.53 exact (zenon_Hb1 just4). % 0.19/0.53 exact (zenon_H67 zenon_Hb0). % 0.19/0.53 apply zenon_Ha8. apply refl_equal. % 0.19/0.53 cut ((genlmt (c_organizationdatamt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))) = (genlmt (c_tptp_member3515_mt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_H63. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact just16. % 0.19/0.53 cut (((f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) = (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)))); [idtac | apply NNPP; zenon_intro zenon_Hb2]. % 0.19/0.53 cut (((c_organizationdatamt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_Hb3]. % 0.19/0.53 congruence. % 0.19/0.53 apply (zenon_notand_s _ _ zenon_H66); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hb4 ]. % 0.19/0.53 apply zenon_Hb5. zenon_intro zenon_Hb6. % 0.19/0.53 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H82 | zenon_intro zenon_H83 ]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_organizationdatamt) = (c_tptp_member3515_mt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_Hb3. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact zenon_H82. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H83]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_organizationdatamt))); [idtac | apply NNPP; zenon_intro zenon_H68]. % 0.19/0.53 congruence. % 0.19/0.53 exact (zenon_H68 zenon_Hb6). % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_Hb4. zenon_intro zenon_Hb0. % 0.19/0.53 generalize (zenon_H3c (c_tptp_member3515_mt)). zenon_intro zenon_H84. % 0.19/0.53 generalize (zenon_H84 (c_organizationdatamt)). zenon_intro zenon_Hb7. % 0.19/0.53 generalize (zenon_Hb7 (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))). zenon_intro zenon_Hb8. % 0.19/0.53 apply (zenon_imply_s _ _ zenon_Hb8); [ zenon_intro zenon_H67 | zenon_intro zenon_Hb9 ]. % 0.19/0.53 exact (zenon_H67 zenon_Hb0). % 0.19/0.53 apply (zenon_imply_s _ _ zenon_Hb9); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hba ]. % 0.19/0.53 exact (zenon_Hbb just16). % 0.19/0.53 exact (zenon_H63 zenon_Hba). % 0.19/0.53 apply zenon_Hb2. apply refl_equal. % 0.19/0.53 cut ((genlmt (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) (c_massmediadatamt)) = (genlmt (c_tptp_member3515_mt) (c_massmediadatamt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_H5f. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact just17. % 0.19/0.53 cut (((c_massmediadatamt) = (c_massmediadatamt))); [idtac | apply NNPP; zenon_intro zenon_Hbc]. % 0.19/0.53 cut (((f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_Hbd]. % 0.19/0.53 congruence. % 0.19/0.53 apply (zenon_notand_s _ _ zenon_H62); [ zenon_intro zenon_Hbf | zenon_intro zenon_Hbe ]. % 0.19/0.53 apply zenon_Hbf. zenon_intro zenon_Hc0. % 0.19/0.53 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H82 | zenon_intro zenon_H83 ]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) = (c_tptp_member3515_mt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_Hbd. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact zenon_H82. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H83]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 0.19/0.53 congruence. % 0.19/0.53 exact (zenon_H64 zenon_Hc0). % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_Hbe. zenon_intro zenon_Hba. % 0.19/0.53 generalize (zenon_H3c (c_tptp_member3515_mt)). zenon_intro zenon_H84. % 0.19/0.53 generalize (zenon_H84 (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))). zenon_intro zenon_Hc1. % 0.19/0.53 generalize (zenon_Hc1 (c_massmediadatamt)). zenon_intro zenon_Hc2. % 0.19/0.53 apply (zenon_imply_s _ _ zenon_Hc2); [ zenon_intro zenon_H63 | zenon_intro zenon_Hc3 ]. % 0.19/0.53 exact (zenon_H63 zenon_Hba). % 0.19/0.53 apply (zenon_imply_s _ _ zenon_Hc3); [ zenon_intro zenon_Hc5 | zenon_intro zenon_Hc4 ]. % 0.19/0.53 exact (zenon_Hc5 just17). % 0.19/0.53 exact (zenon_H5f zenon_Hc4). % 0.19/0.53 apply zenon_Hbc. apply refl_equal. % 0.19/0.53 cut ((genlmt (c_massmediadatamt) (c_ethnicgroupsmt)) = (genlmt (c_tptp_member3515_mt) (c_ethnicgroupsmt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_H5b. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact just12. % 0.19/0.53 cut (((c_ethnicgroupsmt) = (c_ethnicgroupsmt))); [idtac | apply NNPP; zenon_intro zenon_Hc6]. % 0.19/0.53 cut (((c_massmediadatamt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_Hc7]. % 0.19/0.53 congruence. % 0.19/0.53 apply (zenon_notand_s _ _ zenon_H5e); [ zenon_intro zenon_Hc9 | zenon_intro zenon_Hc8 ]. % 0.19/0.53 apply zenon_Hc9. zenon_intro zenon_Hca. % 0.19/0.53 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H82 | zenon_intro zenon_H83 ]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_massmediadatamt) = (c_tptp_member3515_mt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_Hc7. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact zenon_H82. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H83]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_massmediadatamt))); [idtac | apply NNPP; zenon_intro zenon_H60]. % 0.19/0.53 congruence. % 0.19/0.53 exact (zenon_H60 zenon_Hca). % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_Hc8. zenon_intro zenon_Hc4. % 0.19/0.53 generalize (zenon_H3c (c_tptp_member3515_mt)). zenon_intro zenon_H84. % 0.19/0.53 generalize (zenon_H84 (c_massmediadatamt)). zenon_intro zenon_Hcb. % 0.19/0.53 generalize (zenon_Hcb (c_ethnicgroupsmt)). zenon_intro zenon_Hcc. % 0.19/0.53 apply (zenon_imply_s _ _ zenon_Hcc); [ zenon_intro zenon_H5f | zenon_intro zenon_Hcd ]. % 0.19/0.53 exact (zenon_H5f zenon_Hc4). % 0.19/0.53 apply (zenon_imply_s _ _ zenon_Hcd); [ zenon_intro zenon_Hcf | zenon_intro zenon_Hce ]. % 0.19/0.53 exact (zenon_Hcf just12). % 0.19/0.53 exact (zenon_H5b zenon_Hce). % 0.19/0.53 apply zenon_Hc6. apply refl_equal. % 0.19/0.53 cut ((genlmt (c_ethnicgroupsmt) (c_ethnicgroupsvocabularymt)) = (genlmt (c_tptp_member3515_mt) (c_ethnicgroupsvocabularymt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_H57. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact just15. % 0.19/0.53 cut (((c_ethnicgroupsvocabularymt) = (c_ethnicgroupsvocabularymt))); [idtac | apply NNPP; zenon_intro zenon_Hd0]. % 0.19/0.53 cut (((c_ethnicgroupsmt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_Hd1]. % 0.19/0.53 congruence. % 0.19/0.53 apply (zenon_notand_s _ _ zenon_H5a); [ zenon_intro zenon_Hd3 | zenon_intro zenon_Hd2 ]. % 0.19/0.53 apply zenon_Hd3. zenon_intro zenon_Hd4. % 0.19/0.53 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H82 | zenon_intro zenon_H83 ]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_ethnicgroupsmt) = (c_tptp_member3515_mt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_Hd1. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact zenon_H82. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H83]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_ethnicgroupsmt))); [idtac | apply NNPP; zenon_intro zenon_H5c]. % 0.19/0.53 congruence. % 0.19/0.53 exact (zenon_H5c zenon_Hd4). % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_Hd2. zenon_intro zenon_Hce. % 0.19/0.53 generalize (zenon_H3c (c_tptp_member3515_mt)). zenon_intro zenon_H84. % 0.19/0.53 generalize (zenon_H84 (c_ethnicgroupsmt)). zenon_intro zenon_Hd5. % 0.19/0.53 generalize (zenon_Hd5 (c_ethnicgroupsvocabularymt)). zenon_intro zenon_Hd6. % 0.19/0.53 apply (zenon_imply_s _ _ zenon_Hd6); [ zenon_intro zenon_H5b | zenon_intro zenon_Hd7 ]. % 0.19/0.53 exact (zenon_H5b zenon_Hce). % 0.19/0.53 apply (zenon_imply_s _ _ zenon_Hd7); [ zenon_intro zenon_Hd9 | zenon_intro zenon_Hd8 ]. % 0.19/0.53 exact (zenon_Hd9 just15). % 0.19/0.53 exact (zenon_H57 zenon_Hd8). % 0.19/0.53 apply zenon_Hd0. apply refl_equal. % 0.19/0.53 cut ((genlmt (c_ethnicgroupsvocabularymt) (c_worldcompletedualistgeographymt)) = (genlmt (c_tptp_member3515_mt) (c_worldcompletedualistgeographymt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_H53. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact just2. % 0.19/0.53 cut (((c_worldcompletedualistgeographymt) = (c_worldcompletedualistgeographymt))); [idtac | apply NNPP; zenon_intro zenon_Hda]. % 0.19/0.53 cut (((c_ethnicgroupsvocabularymt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 0.19/0.53 congruence. % 0.19/0.53 apply (zenon_notand_s _ _ zenon_H56); [ zenon_intro zenon_Hdd | zenon_intro zenon_Hdc ]. % 0.19/0.53 apply zenon_Hdd. zenon_intro zenon_Hde. % 0.19/0.53 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H82 | zenon_intro zenon_H83 ]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_ethnicgroupsvocabularymt) = (c_tptp_member3515_mt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_Hdb. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact zenon_H82. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H83]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_ethnicgroupsvocabularymt))); [idtac | apply NNPP; zenon_intro zenon_H58]. % 0.19/0.53 congruence. % 0.19/0.53 exact (zenon_H58 zenon_Hde). % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_Hdc. zenon_intro zenon_Hd8. % 0.19/0.53 generalize (zenon_H3c (c_tptp_member3515_mt)). zenon_intro zenon_H84. % 0.19/0.53 generalize (zenon_H84 (c_ethnicgroupsvocabularymt)). zenon_intro zenon_Hdf. % 0.19/0.53 generalize (zenon_Hdf (c_worldcompletedualistgeographymt)). zenon_intro zenon_He0. % 0.19/0.53 apply (zenon_imply_s _ _ zenon_He0); [ zenon_intro zenon_H57 | zenon_intro zenon_He1 ]. % 0.19/0.53 exact (zenon_H57 zenon_Hd8). % 0.19/0.53 apply (zenon_imply_s _ _ zenon_He1); [ zenon_intro zenon_He3 | zenon_intro zenon_He2 ]. % 0.19/0.53 exact (zenon_He3 just2). % 0.19/0.53 exact (zenon_H53 zenon_He2). % 0.19/0.53 apply zenon_Hda. apply refl_equal. % 0.19/0.53 cut ((genlmt (c_worldcompletedualistgeographymt) (c_unitedstatesgeographydualistmt)) = (genlmt (c_tptp_member3515_mt) (c_unitedstatesgeographydualistmt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_H4f. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact just11. % 0.19/0.53 cut (((c_unitedstatesgeographydualistmt) = (c_unitedstatesgeographydualistmt))); [idtac | apply NNPP; zenon_intro zenon_He4]. % 0.19/0.53 cut (((c_worldcompletedualistgeographymt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_He5]. % 0.19/0.53 congruence. % 0.19/0.53 apply (zenon_notand_s _ _ zenon_H52); [ zenon_intro zenon_He7 | zenon_intro zenon_He6 ]. % 0.19/0.53 apply zenon_He7. zenon_intro zenon_He8. % 0.19/0.53 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H82 | zenon_intro zenon_H83 ]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_worldcompletedualistgeographymt) = (c_tptp_member3515_mt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_He5. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact zenon_H82. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H83]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_worldcompletedualistgeographymt))); [idtac | apply NNPP; zenon_intro zenon_H54]. % 0.19/0.53 congruence. % 0.19/0.53 exact (zenon_H54 zenon_He8). % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_He6. zenon_intro zenon_He2. % 0.19/0.53 generalize (zenon_H3c (c_tptp_member3515_mt)). zenon_intro zenon_H84. % 0.19/0.53 generalize (zenon_H84 (c_worldcompletedualistgeographymt)). zenon_intro zenon_He9. % 0.19/0.53 generalize (zenon_He9 (c_unitedstatesgeographydualistmt)). zenon_intro zenon_Hea. % 0.19/0.53 apply (zenon_imply_s _ _ zenon_Hea); [ zenon_intro zenon_H53 | zenon_intro zenon_Heb ]. % 0.19/0.53 exact (zenon_H53 zenon_He2). % 0.19/0.53 apply (zenon_imply_s _ _ zenon_Heb); [ zenon_intro zenon_Hed | zenon_intro zenon_Hec ]. % 0.19/0.53 exact (zenon_Hed just11). % 0.19/0.53 exact (zenon_H4f zenon_Hec). % 0.19/0.53 apply zenon_He4. apply refl_equal. % 0.19/0.53 cut ((genlmt (c_unitedstatesgeographydualistmt) (c_worldgeographydualistmt)) = (genlmt (c_tptp_member3515_mt) (c_worldgeographydualistmt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_H4b. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact just8. % 0.19/0.53 cut (((c_worldgeographydualistmt) = (c_worldgeographydualistmt))); [idtac | apply NNPP; zenon_intro zenon_Hee]. % 0.19/0.53 cut (((c_unitedstatesgeographydualistmt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_Hef]. % 0.19/0.53 congruence. % 0.19/0.53 apply (zenon_notand_s _ _ zenon_H4e); [ zenon_intro zenon_Hf1 | zenon_intro zenon_Hf0 ]. % 0.19/0.53 apply zenon_Hf1. zenon_intro zenon_Hf2. % 0.19/0.53 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H82 | zenon_intro zenon_H83 ]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_unitedstatesgeographydualistmt) = (c_tptp_member3515_mt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_Hef. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact zenon_H82. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H83]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_unitedstatesgeographydualistmt))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 0.19/0.53 congruence. % 0.19/0.53 exact (zenon_H50 zenon_Hf2). % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_Hf0. zenon_intro zenon_Hec. % 0.19/0.53 generalize (zenon_H3c (c_tptp_member3515_mt)). zenon_intro zenon_H84. % 0.19/0.53 generalize (zenon_H84 (c_unitedstatesgeographydualistmt)). zenon_intro zenon_Hf3. % 0.19/0.53 generalize (zenon_Hf3 (c_worldgeographydualistmt)). zenon_intro zenon_Hf4. % 0.19/0.53 apply (zenon_imply_s _ _ zenon_Hf4); [ zenon_intro zenon_H4f | zenon_intro zenon_Hf5 ]. % 0.19/0.53 exact (zenon_H4f zenon_Hec). % 0.19/0.53 apply (zenon_imply_s _ _ zenon_Hf5); [ zenon_intro zenon_Hf7 | zenon_intro zenon_Hf6 ]. % 0.19/0.53 exact (zenon_Hf7 just8). % 0.19/0.53 exact (zenon_H4b zenon_Hf6). % 0.19/0.53 apply zenon_Hee. apply refl_equal. % 0.19/0.53 cut ((genlmt (c_worldgeographydualistmt) (c_worldgeographymt)) = (genlmt (c_tptp_member3515_mt) (c_worldgeographymt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_H47. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact just1. % 0.19/0.53 cut (((c_worldgeographymt) = (c_worldgeographymt))); [idtac | apply NNPP; zenon_intro zenon_Hf8]. % 0.19/0.53 cut (((c_worldgeographydualistmt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_Hf9]. % 0.19/0.53 congruence. % 0.19/0.53 apply (zenon_notand_s _ _ zenon_H4a); [ zenon_intro zenon_Hfb | zenon_intro zenon_Hfa ]. % 0.19/0.53 apply zenon_Hfb. zenon_intro zenon_Hfc. % 0.19/0.53 elim (classic ((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [ zenon_intro zenon_H82 | zenon_intro zenon_H83 ]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt)) = ((c_worldgeographydualistmt) = (c_tptp_member3515_mt))). % 0.19/0.53 intro zenon_D_pnotp. % 0.19/0.53 apply zenon_Hf9. % 0.19/0.53 rewrite <- zenon_D_pnotp. % 0.19/0.53 exact zenon_H82. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_tptp_member3515_mt))); [idtac | apply NNPP; zenon_intro zenon_H83]. % 0.19/0.53 cut (((c_tptp_member3515_mt) = (c_worldgeographydualistmt))); [idtac | apply NNPP; zenon_intro zenon_H4c]. % 0.19/0.53 congruence. % 0.19/0.53 exact (zenon_H4c zenon_Hfc). % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_H83. apply refl_equal. % 0.19/0.53 apply zenon_Hfa. zenon_intro zenon_Hf6. % 0.19/0.53 generalize (zenon_H3c (c_tptp_member3515_mt)). zenon_intro zenon_H84. % 0.19/0.53 generalize (zenon_H84 (c_worldgeographydualistmt)). zenon_intro zenon_Hfd. % 0.19/0.53 generalize (zenon_Hfd (c_worldgeographymt)). zenon_intro zenon_Hfe. % 0.19/0.53 apply (zenon_imply_s _ _ zenon_Hfe); [ zenon_intro zenon_H4b | zenon_intro zenon_Hff ]. % 0.19/0.53 exact (zenon_H4b zenon_Hf6). % 0.19/0.53 apply (zenon_imply_s _ _ zenon_Hff); [ zenon_intro zenon_H101 | zenon_intro zenon_H100 ]. % 0.19/0.53 exact (zenon_H101 just1). % 0.19/0.53 exact (zenon_H47 zenon_H100). % 0.19/0.53 apply zenon_Hf8. apply refl_equal. % 0.19/0.53 exact (zenon_H3f zenon_H45). % 0.19/0.53 apply zenon_G. exists (c_state_geopolitical). apply NNPP. zenon_intro zenon_H102. % 0.19/0.53 apply (zenon_notimply_s _ _ zenon_H102). zenon_intro zenon_H42. zenon_intro zenon_H103. % 0.19/0.53 generalize (just52 (c_wanica_districtsuriname)). zenon_intro zenon_H104. % 0.19/0.53 apply (zenon_imply_s _ _ zenon_H104); [ zenon_intro zenon_H106 | zenon_intro zenon_H105 ]. % 0.19/0.53 exact (zenon_H106 zenon_H3e). % 0.19/0.53 exact (zenon_H103 zenon_H105). % 0.19/0.53 apply zenon_H3d. zenon_intro zenon_Tx_kd. apply NNPP. zenon_intro zenon_H108. % 0.19/0.53 apply zenon_H108. zenon_intro zenon_Ty_kf. apply NNPP. zenon_intro zenon_H10a. % 0.19/0.53 apply zenon_H10a. zenon_intro zenon_Tz_kh. apply NNPP. zenon_intro zenon_H10c. % 0.19/0.53 apply (zenon_notimply_s _ _ zenon_H10c). zenon_intro zenon_H10e. zenon_intro zenon_H10d. % 0.19/0.53 apply (zenon_notimply_s _ _ zenon_H10d). zenon_intro zenon_H110. zenon_intro zenon_H10f. % 0.19/0.53 generalize (just67 zenon_Tx_kd). zenon_intro zenon_H111. % 0.19/0.53 generalize (zenon_H111 zenon_Ty_kf). zenon_intro zenon_H112. % 0.19/0.53 generalize (zenon_H112 zenon_Tz_kh). zenon_intro zenon_H113. % 0.19/0.53 apply (zenon_imply_s _ _ zenon_H113); [ zenon_intro zenon_H115 | zenon_intro zenon_H114 ]. % 0.19/0.53 apply (zenon_notand_s _ _ zenon_H115); [ zenon_intro zenon_H117 | zenon_intro zenon_H116 ]. % 0.19/0.53 exact (zenon_H117 zenon_H10e). % 0.19/0.53 exact (zenon_H116 zenon_H110). % 0.19/0.53 exact (zenon_H10f zenon_H114). % 0.19/0.53 Qed. % 0.19/0.53 % SZS output end Proof % 0.19/0.53 (* END-PROOF *) % 0.19/0.53 nodes searched: 319 % 0.19/0.53 max branch formulas: 229 % 0.19/0.53 proof nodes created: 50 % 0.19/0.53 formulas created: 2263 % 0.19/0.53 %------------------------------------------------------------------------------