%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : PHI015+1 : TPTP v8.1.0. Released v7.2.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n027.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 : Mon Jul 18 16:50:15 EDT 2022 % Result : Theorem 10.44s 10.66s % Output : Proof 10.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : PHI015+1 : TPTP v8.1.0. Released v7.2.0. % 0.07/0.12 % Command : run_zenon %s %d % 0.13/0.33 % Computer : n027.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.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Thu Jun 2 01:26:34 EDT 2022 % 0.13/0.34 % CPUTime : % 10.44/10.66 (* PROOF-FOUND *) % 10.44/10.66 % SZS status Theorem % 10.44/10.66 (* BEGIN-PROOF *) % 10.44/10.66 % SZS output start Proof % 10.44/10.66 Theorem god_exists : (exemplifies_property (existence) (god)). % 10.44/10.66 Proof. % 10.44/10.66 assert (zenon_L1_ : (forall F : zenon_U, ((is_the (god) F)->((property F)/\(object (god))))) -> (~(object (god))) -> False). % 10.44/10.66 do 0 intro. intros zenon_Hb zenon_Hc. % 10.44/10.66 generalize (zenon_Hb (none_greater)). zenon_intro zenon_Hd. % 10.44/10.66 apply (zenon_imply_s _ _ zenon_Hd); [ zenon_intro zenon_Hf | zenon_intro zenon_He ]. % 10.44/10.66 exact (zenon_Hf definition_god). % 10.44/10.66 apply (zenon_and_s _ _ zenon_He). zenon_intro zenon_H11. zenon_intro zenon_H10. % 10.44/10.66 exact (zenon_Hc zenon_H10). % 10.44/10.66 (* end of lemma zenon_L1_ *) % 10.44/10.66 assert (zenon_L2_ : (~(object (god))) -> False). % 10.44/10.66 do 0 intro. intros zenon_Hc. % 10.44/10.66 generalize (description_is_property_and_described_is_object (god)). zenon_intro zenon_Hb. % 10.44/10.66 apply (zenon_L1_); trivial. % 10.44/10.66 (* end of lemma zenon_L2_ *) % 10.44/10.66 assert (zenon_L3_ : forall (zenon_TX_v : zenon_U), (forall F : zenon_U, ((exemplifies_property F zenon_TX_v)->((property F)/\(object zenon_TX_v)))) -> (exemplifies_property (none_greater) zenon_TX_v) -> (~(property (none_greater))) -> False). % 10.44/10.66 do 1 intro. intros zenon_H12 zenon_H13 zenon_H14. % 10.44/10.66 generalize (zenon_H12 (none_greater)). zenon_intro zenon_H16. % 10.44/10.66 apply (zenon_imply_s _ _ zenon_H16); [ zenon_intro zenon_H18 | zenon_intro zenon_H17 ]. % 10.44/10.66 exact (zenon_H18 zenon_H13). % 10.44/10.66 apply (zenon_and_s _ _ zenon_H17). zenon_intro zenon_H11. zenon_intro zenon_H19. % 10.44/10.66 exact (zenon_H14 zenon_H11). % 10.44/10.66 (* end of lemma zenon_L3_ *) % 10.44/10.66 assert (zenon_L4_ : forall (zenon_TX_v : zenon_U), (~(forall Z : zenon_U, ((object Z)->((exemplifies_property (none_greater) Z)->(Z = zenon_TX_v))))) -> (~(exists Y : zenon_U, ((object Y)/\((exemplifies_relation (greater_than) Y zenon_TX_v)/\(exemplifies_property (conceivable) Y))))) -> (exemplifies_property (conceivable) zenon_TX_v) -> (object zenon_TX_v) -> (forall Y : zenon_U, (((object zenon_TX_v)/\(object Y))->((exemplifies_relation (greater_than) zenon_TX_v Y)\/((exemplifies_relation (greater_than) Y zenon_TX_v)\/(zenon_TX_v = Y))))) -> False). % 10.44/10.66 do 1 intro. intros zenon_H1a zenon_H1b zenon_H1c zenon_H19 zenon_H1d. % 10.44/10.66 apply (zenon_notallex_s (fun Z : zenon_U => ((object Z)->((exemplifies_property (none_greater) Z)->(Z = zenon_TX_v)))) zenon_H1a); [ zenon_intro zenon_H1e; idtac ]. % 10.44/10.66 elim zenon_H1e. zenon_intro zenon_TZ_bf. zenon_intro zenon_H20. % 10.44/10.66 apply (zenon_notimply_s _ _ zenon_H20). zenon_intro zenon_H22. zenon_intro zenon_H21. % 10.44/10.66 apply (zenon_notimply_s _ _ zenon_H21). zenon_intro zenon_H24. zenon_intro zenon_H23. % 10.44/10.66 generalize (zenon_H1d zenon_TZ_bf). zenon_intro zenon_H25. % 10.44/10.66 apply (zenon_imply_s _ _ zenon_H25); [ zenon_intro zenon_H27 | zenon_intro zenon_H26 ]. % 10.44/10.66 apply (zenon_notand_s _ _ zenon_H27); [ zenon_intro zenon_H29 | zenon_intro zenon_H28 ]. % 10.44/10.66 exact (zenon_H29 zenon_H19). % 10.44/10.66 exact (zenon_H28 zenon_H22). % 10.44/10.66 apply (zenon_or_s _ _ zenon_H26); [ zenon_intro zenon_H2b | zenon_intro zenon_H2a ]. % 10.44/10.66 generalize (definition_none_greater zenon_TZ_bf). zenon_intro zenon_H2c. % 10.44/10.66 apply (zenon_imply_s _ _ zenon_H2c); [ zenon_intro zenon_H28 | zenon_intro zenon_H2d ]. % 10.44/10.66 exact (zenon_H28 zenon_H22). % 10.44/10.66 apply (zenon_equiv_s _ _ zenon_H2d); [ zenon_intro zenon_H30; zenon_intro zenon_H2f | zenon_intro zenon_H24; zenon_intro zenon_H2e ]. % 10.44/10.66 exact (zenon_H30 zenon_H24). % 10.44/10.66 apply (zenon_and_s _ _ zenon_H2e). zenon_intro zenon_H32. zenon_intro zenon_H31. % 10.44/10.66 apply zenon_H31. exists zenon_TX_v. apply NNPP. zenon_intro zenon_H33. % 10.44/10.66 apply (zenon_notand_s _ _ zenon_H33); [ zenon_intro zenon_H29 | zenon_intro zenon_H34 ]. % 10.44/10.66 exact (zenon_H29 zenon_H19). % 10.44/10.66 apply (zenon_notand_s _ _ zenon_H34); [ zenon_intro zenon_H36 | zenon_intro zenon_H35 ]. % 10.44/10.66 exact (zenon_H36 zenon_H2b). % 10.44/10.66 exact (zenon_H35 zenon_H1c). % 10.44/10.66 apply (zenon_or_s _ _ zenon_H2a); [ zenon_intro zenon_H38 | zenon_intro zenon_H37 ]. % 10.44/10.66 generalize (definition_none_greater zenon_TZ_bf). zenon_intro zenon_H2c. % 10.44/10.66 apply (zenon_imply_s _ _ zenon_H2c); [ zenon_intro zenon_H28 | zenon_intro zenon_H2d ]. % 10.44/10.66 exact (zenon_H28 zenon_H22). % 10.44/10.66 apply (zenon_equiv_s _ _ zenon_H2d); [ zenon_intro zenon_H30; zenon_intro zenon_H2f | zenon_intro zenon_H24; zenon_intro zenon_H2e ]. % 10.44/10.66 exact (zenon_H30 zenon_H24). % 10.44/10.66 apply (zenon_and_s _ _ zenon_H2e). zenon_intro zenon_H32. zenon_intro zenon_H31. % 10.44/10.66 apply zenon_H1b. exists zenon_TZ_bf. apply NNPP. zenon_intro zenon_H39. % 10.44/10.66 apply (zenon_notand_s _ _ zenon_H39); [ zenon_intro zenon_H28 | zenon_intro zenon_H3a ]. % 10.44/10.66 exact (zenon_H28 zenon_H22). % 10.44/10.66 apply (zenon_notand_s _ _ zenon_H3a); [ zenon_intro zenon_H3c | zenon_intro zenon_H3b ]. % 10.44/10.66 exact (zenon_H3c zenon_H38). % 10.44/10.66 exact (zenon_H3b zenon_H32). % 10.44/10.66 apply zenon_H23. apply sym_equal. exact zenon_H37. % 10.44/10.66 (* end of lemma zenon_L4_ *) % 10.44/10.66 assert (zenon_L5_ : forall (zenon_TX_v : zenon_U), (~(exists Y : zenon_U, ((object Y)/\((exemplifies_property (none_greater) Y)/\((forall Z : zenon_U, ((object Z)->((exemplifies_property (none_greater) Z)->(Z = Y))))/\(Y = zenon_TX_v)))))) -> (object zenon_TX_v) -> (exemplifies_property (none_greater) zenon_TX_v) -> (forall Y : zenon_U, (((object zenon_TX_v)/\(object Y))->((exemplifies_relation (greater_than) zenon_TX_v Y)\/((exemplifies_relation (greater_than) Y zenon_TX_v)\/(zenon_TX_v = Y))))) -> (exemplifies_property (conceivable) zenon_TX_v) -> (~(exists Y : zenon_U, ((object Y)/\((exemplifies_relation (greater_than) Y zenon_TX_v)/\(exemplifies_property (conceivable) Y))))) -> False). % 10.44/10.66 do 1 intro. intros zenon_H3d zenon_H19 zenon_H13 zenon_H1d zenon_H1c zenon_H1b. % 10.44/10.66 apply zenon_H3d. exists zenon_TX_v. apply NNPP. zenon_intro zenon_H3e. % 10.44/10.66 apply (zenon_notand_s _ _ zenon_H3e); [ zenon_intro zenon_H29 | zenon_intro zenon_H3f ]. % 10.44/10.66 exact (zenon_H29 zenon_H19). % 10.44/10.66 apply (zenon_notand_s _ _ zenon_H3f); [ zenon_intro zenon_H18 | zenon_intro zenon_H40 ]. % 10.44/10.66 exact (zenon_H18 zenon_H13). % 10.44/10.66 apply (zenon_notand_s _ _ zenon_H40); [ zenon_intro zenon_H1a | zenon_intro zenon_H41 ]. % 10.44/10.66 apply (zenon_L4_ zenon_TX_v); trivial. % 10.44/10.66 apply zenon_H41. apply refl_equal. % 10.44/10.66 (* end of lemma zenon_L5_ *) % 10.44/10.66 assert (zenon_L6_ : (((is_the (god) (none_greater))/\(exemplifies_property (none_greater) (god)))<->(exists Y : zenon_U, ((object Y)/\((exemplifies_property (none_greater) Y)/\((forall Z : zenon_U, ((object Z)->((exemplifies_property (none_greater) Z)->(Z = Y))))/\(exemplifies_property (none_greater) Y)))))) -> (~(exemplifies_property (none_greater) (god))) -> (exists Y : zenon_U, ((object Y)/\((exemplifies_property (none_greater) Y)/\((forall Z : zenon_U, ((object Z)->((exemplifies_property (none_greater) Z)->(Z = Y))))/\(exemplifies_property (none_greater) Y))))) -> False). % 10.44/10.66 do 0 intro. intros zenon_H42 zenon_H43 zenon_H44. % 10.44/10.66 apply (zenon_equiv_s _ _ zenon_H42); [ zenon_intro zenon_H47; zenon_intro zenon_H46 | zenon_intro zenon_H45; zenon_intro zenon_H44 ]. % 10.44/10.66 exact (zenon_H46 zenon_H44). % 10.44/10.66 apply (zenon_and_s _ _ zenon_H45). zenon_intro definition_god. zenon_intro zenon_H48. % 10.44/10.66 exact (zenon_H43 zenon_H48). % 10.44/10.66 (* end of lemma zenon_L6_ *) % 10.44/10.66 assert (zenon_L7_ : forall (zenon_TX_v : zenon_U), (forall X : zenon_U, (((property (none_greater))/\((property (none_greater))/\(object X)))->(((is_the X (none_greater))/\(exemplifies_property (none_greater) X))<->(exists Y : zenon_U, ((object Y)/\((exemplifies_property (none_greater) Y)/\((forall Z : zenon_U, ((object Z)->((exemplifies_property (none_greater) Z)->(Z = Y))))/\(exemplifies_property (none_greater) Y)))))))) -> (forall F : zenon_U, ((exemplifies_property F zenon_TX_v)->((property F)/\(object zenon_TX_v)))) -> (exemplifies_property (none_greater) zenon_TX_v) -> (object (god)) -> (~(exemplifies_property (none_greater) (god))) -> (exists Y : zenon_U, ((object Y)/\((exemplifies_property (none_greater) Y)/\((forall Z : zenon_U, ((object Z)->((exemplifies_property (none_greater) Z)->(Z = Y))))/\(exemplifies_property (none_greater) Y))))) -> False). % 10.44/10.66 do 1 intro. intros zenon_H49 zenon_H12 zenon_H13 zenon_H10 zenon_H43 zenon_H44. % 10.44/10.66 generalize (zenon_H49 (god)). zenon_intro zenon_H4a. % 10.44/10.66 apply (zenon_imply_s _ _ zenon_H4a); [ zenon_intro zenon_H4b | zenon_intro zenon_H42 ]. % 10.44/10.66 apply (zenon_notand_s _ _ zenon_H4b); [ zenon_intro zenon_H14 | zenon_intro zenon_H4c ]. % 10.44/10.66 apply (zenon_L3_ zenon_TX_v); trivial. % 10.44/10.66 apply (zenon_notand_s _ _ zenon_H4c); [ zenon_intro zenon_H14 | zenon_intro zenon_Hc ]. % 10.44/10.66 apply (zenon_L3_ zenon_TX_v); trivial. % 10.44/10.66 exact (zenon_Hc zenon_H10). % 10.44/10.66 apply (zenon_L6_); trivial. % 10.44/10.66 (* end of lemma zenon_L7_ *) % 10.44/10.66 assert (zenon_L8_ : forall (zenon_TX_v : zenon_U), (forall G : zenon_U, (forall X : zenon_U, (((property (none_greater))/\((property G)/\(object X)))->(((is_the X (none_greater))/\(exemplifies_property G X))<->(exists Y : zenon_U, ((object Y)/\((exemplifies_property (none_greater) Y)/\((forall Z : zenon_U, ((object Z)->((exemplifies_property (none_greater) Z)->(Z = Y))))/\(exemplifies_property G Y))))))))) -> (is_the zenon_TX_v (none_greater)) -> (object (god)) -> (~(exemplifies_property (none_greater) (god))) -> (object zenon_TX_v) -> (exemplifies_property (none_greater) zenon_TX_v) -> (forall F : zenon_U, ((exemplifies_property F zenon_TX_v)->((property F)/\(object zenon_TX_v)))) -> False). % 10.44/10.66 do 1 intro. intros zenon_H4d zenon_H4e zenon_H10 zenon_H43 zenon_H19 zenon_H13 zenon_H12. % 10.44/10.66 generalize (zenon_H4d (none_greater)). zenon_intro zenon_H49. % 10.44/10.66 generalize (zenon_H49 zenon_TX_v). zenon_intro zenon_H4f. % 10.44/10.66 apply (zenon_imply_s _ _ zenon_H4f); [ zenon_intro zenon_H51 | zenon_intro zenon_H50 ]. % 10.44/10.66 apply (zenon_notand_s _ _ zenon_H51); [ zenon_intro zenon_H14 | zenon_intro zenon_H52 ]. % 10.44/10.66 apply (zenon_L3_ zenon_TX_v); trivial. % 10.44/10.66 apply (zenon_notand_s _ _ zenon_H52); [ zenon_intro zenon_H14 | zenon_intro zenon_H29 ]. % 10.44/10.66 apply (zenon_L3_ zenon_TX_v); trivial. % 10.44/10.66 exact (zenon_H29 zenon_H19). % 10.44/10.66 apply (zenon_equiv_s _ _ zenon_H50); [ zenon_intro zenon_H54; zenon_intro zenon_H46 | zenon_intro zenon_H53; zenon_intro zenon_H44 ]. % 10.44/10.66 apply (zenon_notand_s _ _ zenon_H54); [ zenon_intro zenon_H55 | zenon_intro zenon_H18 ]. % 10.44/10.66 exact (zenon_H55 zenon_H4e). % 10.44/10.66 exact (zenon_H18 zenon_H13). % 10.44/10.66 apply (zenon_L7_ zenon_TX_v); trivial. % 10.44/10.66 (* end of lemma zenon_L8_ *) % 10.44/10.66 assert (zenon_L9_ : forall (zenon_TX_v : zenon_U), ((is_the zenon_TX_v (none_greater))/\(zenon_TX_v = zenon_TX_v)) -> (forall F : zenon_U, ((exemplifies_property F zenon_TX_v)->((property F)/\(object zenon_TX_v)))) -> (exemplifies_property (none_greater) zenon_TX_v) -> (object zenon_TX_v) -> (~(exemplifies_property (none_greater) (god))) -> (object (god)) -> (forall G : zenon_U, (forall X : zenon_U, (((property (none_greater))/\((property G)/\(object X)))->(((is_the X (none_greater))/\(exemplifies_property G X))<->(exists Y : zenon_U, ((object Y)/\((exemplifies_property (none_greater) Y)/\((forall Z : zenon_U, ((object Z)->((exemplifies_property (none_greater) Z)->(Z = Y))))/\(exemplifies_property G Y))))))))) -> False). % 10.44/10.66 do 1 intro. intros zenon_H56 zenon_H12 zenon_H13 zenon_H19 zenon_H43 zenon_H10 zenon_H4d. % 10.44/10.66 apply (zenon_and_s _ _ zenon_H56). zenon_intro zenon_H4e. zenon_intro zenon_H57. % 10.44/10.66 apply (zenon_L8_ zenon_TX_v); trivial. % 10.44/10.66 (* end of lemma zenon_L9_ *) % 10.44/10.66 assert (zenon_L10_ : forall (zenon_TX_v : zenon_U), (forall X : zenon_U, (forall W : zenon_U, (((property (none_greater))/\((object X)/\(object W)))->(((is_the X (none_greater))/\(X = W))<->(exists Y : zenon_U, ((object Y)/\((exemplifies_property (none_greater) Y)/\((forall Z : zenon_U, ((object Z)->((exemplifies_property (none_greater) Z)->(Z = Y))))/\(Y = W))))))))) -> (forall Y : zenon_U, (((object zenon_TX_v)/\(object Y))->((exemplifies_relation (greater_than) zenon_TX_v Y)\/((exemplifies_relation (greater_than) Y zenon_TX_v)\/(zenon_TX_v = Y))))) -> (exemplifies_property (conceivable) zenon_TX_v) -> (~(exists Y : zenon_U, ((object Y)/\((exemplifies_relation (greater_than) Y zenon_TX_v)/\(exemplifies_property (conceivable) Y))))) -> (~(exemplifies_property (none_greater) (god))) -> (object (god)) -> (forall G : zenon_U, (forall X : zenon_U, (((property (none_greater))/\((property G)/\(object X)))->(((is_the X (none_greater))/\(exemplifies_property G X))<->(exists Y : zenon_U, ((object Y)/\((exemplifies_property (none_greater) Y)/\((forall Z : zenon_U, ((object Z)->((exemplifies_property (none_greater) Z)->(Z = Y))))/\(exemplifies_property G Y))))))))) -> (object zenon_TX_v) -> (exemplifies_property (none_greater) zenon_TX_v) -> (forall F : zenon_U, ((exemplifies_property F zenon_TX_v)->((property F)/\(object zenon_TX_v)))) -> False). % 10.44/10.66 do 1 intro. intros zenon_H58 zenon_H1d zenon_H1c zenon_H1b zenon_H43 zenon_H10 zenon_H4d zenon_H19 zenon_H13 zenon_H12. % 10.44/10.66 generalize (zenon_H58 zenon_TX_v). zenon_intro zenon_H59. % 10.44/10.66 generalize (zenon_H59 zenon_TX_v). zenon_intro zenon_H5a. % 10.44/10.66 apply (zenon_imply_s _ _ zenon_H5a); [ zenon_intro zenon_H5c | zenon_intro zenon_H5b ]. % 10.44/10.66 apply (zenon_notand_s _ _ zenon_H5c); [ zenon_intro zenon_H14 | zenon_intro zenon_H5d ]. % 10.44/10.66 apply (zenon_L3_ zenon_TX_v); trivial. % 10.44/10.66 apply (zenon_notand_s _ _ zenon_H5d); [ zenon_intro zenon_H29 | zenon_intro zenon_H29 ]. % 10.44/10.66 exact (zenon_H29 zenon_H19). % 10.44/10.66 exact (zenon_H29 zenon_H19). % 10.44/10.66 apply (zenon_equiv_s _ _ zenon_H5b); [ zenon_intro zenon_H5f; zenon_intro zenon_H3d | zenon_intro zenon_H56; zenon_intro zenon_H5e ]. % 10.44/10.66 apply (zenon_L5_ zenon_TX_v); trivial. % 10.44/10.66 apply (zenon_L9_ zenon_TX_v); trivial. % 10.44/10.66 (* end of lemma zenon_L10_ *) % 10.44/10.66 assert (zenon_L11_ : forall (zenon_TX_v : zenon_U), (object zenon_TX_v) -> (~(exemplifies_property (none_greater) (god))) -> (object (god)) -> (exemplifies_property (none_greater) zenon_TX_v) -> False). % 10.44/10.66 do 1 intro. intros zenon_H19 zenon_H43 zenon_H10 zenon_H13. % 10.44/10.66 generalize (definition_none_greater zenon_TX_v). zenon_intro zenon_H60. % 10.44/10.66 apply (zenon_imply_s _ _ zenon_H60); [ zenon_intro zenon_H29 | zenon_intro zenon_H61 ]. % 10.44/10.66 exact (zenon_H29 zenon_H19). % 10.44/10.66 apply (zenon_equiv_s _ _ zenon_H61); [ zenon_intro zenon_H18; zenon_intro zenon_H63 | zenon_intro zenon_H13; zenon_intro zenon_H62 ]. % 10.44/10.66 exact (zenon_H18 zenon_H13). % 10.44/10.66 apply (zenon_and_s _ _ zenon_H62). zenon_intro zenon_H1c. zenon_intro zenon_H1b. % 10.44/10.66 generalize (exemplifier_is_object_and_exemplified_is_property zenon_TX_v). zenon_intro zenon_H12. % 10.44/10.66 generalize (description_axiom_schema_instance (none_greater)). zenon_intro zenon_H4d. % 10.44/10.66 generalize (connectedness_of_greater_than zenon_TX_v). zenon_intro zenon_H1d. % 10.44/10.66 generalize (description_axiom_identity_instance (none_greater)). zenon_intro zenon_H58. % 10.44/10.66 apply (zenon_L10_ zenon_TX_v); trivial. % 10.44/10.66 (* end of lemma zenon_L11_ *) % 10.44/10.66 assert (zenon_L12_ : forall (zenon_TX_v : zenon_U), (object zenon_TX_v) -> (~(exemplifies_property (none_greater) (god))) -> (exemplifies_property (none_greater) zenon_TX_v) -> False). % 10.44/10.66 do 1 intro. intros zenon_H19 zenon_H43 zenon_H13. % 10.44/10.66 generalize (description_is_property_and_described_is_object (god)). zenon_intro zenon_Hb. % 10.44/10.66 generalize (zenon_Hb (none_greater)). zenon_intro zenon_Hd. % 10.44/10.66 apply (zenon_imply_s _ _ zenon_Hd); [ zenon_intro zenon_Hf | zenon_intro zenon_He ]. % 10.44/10.66 exact (zenon_Hf definition_god). % 10.44/10.66 apply (zenon_and_s _ _ zenon_He). zenon_intro zenon_H11. zenon_intro zenon_H10. % 10.44/10.66 apply (zenon_L11_ zenon_TX_v); trivial. % 10.44/10.66 (* end of lemma zenon_L12_ *) % 10.44/10.66 assert (zenon_L13_ : (object (god)) -> (~(exemplifies_property (existence) (god))) -> (~(exists Y : zenon_U, ((object Y)/\((exemplifies_relation (greater_than) Y (god))/\(exemplifies_property (conceivable) Y))))) -> False). % 10.44/10.66 do 0 intro. intros zenon_H10 zenon_G zenon_H64. % 10.44/10.66 generalize (premise_2 (god)). zenon_intro zenon_H65. % 10.44/10.66 apply (zenon_imply_s _ _ zenon_H65); [ zenon_intro zenon_Hc | zenon_intro zenon_H66 ]. % 10.44/10.66 exact (zenon_Hc zenon_H10). % 10.44/10.66 apply (zenon_imply_s _ _ zenon_H66); [ zenon_intro zenon_H68 | zenon_intro zenon_H67 ]. % 10.44/10.66 apply (zenon_notand_s _ _ zenon_H68); [ zenon_intro zenon_Hf | zenon_intro zenon_H69 ]. % 10.44/10.66 exact (zenon_Hf definition_god). % 10.44/10.66 exact (zenon_H69 zenon_G). % 10.44/10.66 exact (zenon_H64 zenon_H67). % 10.44/10.66 (* end of lemma zenon_L13_ *) % 10.44/10.66 apply NNPP. intro zenon_G. % 10.44/10.66 elim premise_1. zenon_intro zenon_TX_v. zenon_intro zenon_H6a. % 10.44/10.66 apply (zenon_and_s _ _ zenon_H6a). zenon_intro zenon_H19. zenon_intro zenon_H13. % 10.44/10.66 generalize (definition_none_greater (god)). zenon_intro zenon_H6b. % 10.44/10.66 apply (zenon_imply_s _ _ zenon_H6b); [ zenon_intro zenon_Hc | zenon_intro zenon_H6c ]. % 10.44/10.66 apply (zenon_L2_); trivial. % 10.44/10.66 apply (zenon_equiv_s _ _ zenon_H6c); [ zenon_intro zenon_H43; zenon_intro zenon_H6e | zenon_intro zenon_H48; zenon_intro zenon_H6d ]. % 10.44/10.66 apply (zenon_L12_ zenon_TX_v); trivial. % 10.44/10.66 apply (zenon_and_s _ _ zenon_H6d). zenon_intro zenon_H6f. zenon_intro zenon_H64. % 10.44/10.66 generalize (exemplifier_is_object_and_exemplified_is_property (god)). zenon_intro zenon_H70. % 10.44/10.66 generalize (zenon_H70 (conceivable)). zenon_intro zenon_H71. % 10.44/10.66 apply (zenon_imply_s _ _ zenon_H71); [ zenon_intro zenon_H73 | zenon_intro zenon_H72 ]. % 10.44/10.67 exact (zenon_H73 zenon_H6f). % 10.44/10.67 apply (zenon_and_s _ _ zenon_H72). zenon_intro zenon_H74. zenon_intro zenon_H10. % 10.44/10.67 apply (zenon_L13_); trivial. % 10.44/10.67 Qed. % 10.44/10.67 % SZS output end Proof % 10.44/10.67 (* END-PROOF *) % 10.44/10.67 nodes searched: 430721 % 10.44/10.67 max branch formulas: 4374 % 10.44/10.67 proof nodes created: 29080 % 10.44/10.67 formulas created: 951370 % 10.44/10.67 %------------------------------------------------------------------------------