%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : PHI010+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:14 EDT 2022 % Result : Theorem 118.09s 118.35s % Output : Proof 118.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : PHI010+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.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Thu Jun 2 01:11:49 EDT 2022 % 0.13/0.33 % CPUTime : % 118.09/118.35 (* PROOF-FOUND *) % 118.09/118.35 % SZS status Theorem % 118.09/118.35 (* BEGIN-PROOF *) % 118.09/118.35 % SZS output start Proof % 118.09/118.35 Theorem lemma_1 : (forall X : zenon_U, (forall F : zenon_U, (forall Y : zenon_U, (((object X)/\((property F)/\(object Y)))->(((is_the X F)/\(X = Y))->(exemplifies_property F Y)))))). % 118.09/118.35 Proof. % 118.09/118.35 assert (zenon_L1_ : forall (zenon_TY_j : zenon_U) (zenon_TF_k : zenon_U) (zenon_TX_l : zenon_U), (((is_the zenon_TX_l zenon_TF_k)/\(zenon_TX_l = zenon_TY_j))<->(exists Y : zenon_U, ((object Y)/\((exemplifies_property zenon_TF_k Y)/\((forall Z : zenon_U, ((object Z)->((exemplifies_property zenon_TF_k Z)->(Z = Y))))/\(Y = zenon_TY_j)))))) -> (~(exists Y : zenon_U, ((object Y)/\((exemplifies_property zenon_TF_k Y)/\((forall Z : zenon_U, ((object Z)->((exemplifies_property zenon_TF_k Z)->(Z = Y))))/\(Y = zenon_TY_j)))))) -> (is_the zenon_TX_l zenon_TF_k) -> (zenon_TX_l = zenon_TY_j) -> False). % 118.09/118.35 do 3 intro. intros zenon_H5 zenon_H6 zenon_H7 zenon_H8. % 118.09/118.35 apply (zenon_equiv_s _ _ zenon_H5); [ zenon_intro zenon_He; zenon_intro zenon_H6 | zenon_intro zenon_Hd; zenon_intro zenon_Hc ]. % 118.09/118.35 apply (zenon_notand_s _ _ zenon_He); [ zenon_intro zenon_H10 | zenon_intro zenon_Hf ]. % 118.09/118.35 exact (zenon_H10 zenon_H7). % 118.09/118.35 exact (zenon_Hf zenon_H8). % 118.09/118.35 exact (zenon_H6 zenon_Hc). % 118.09/118.35 (* end of lemma zenon_L1_ *) % 118.09/118.35 assert (zenon_L2_ : forall (zenon_TY_j : zenon_U) (zenon_TF_k : zenon_U), (exists Y : zenon_U, ((object Y)/\((exemplifies_property zenon_TF_k Y)/\((forall Z : zenon_U, ((object Z)->((exemplifies_property zenon_TF_k Z)->(Z = Y))))/\(Y = zenon_TY_j))))) -> (~(exemplifies_property zenon_TF_k zenon_TY_j)) -> False). % 118.09/118.35 do 2 intro. intros zenon_Hc zenon_H11. % 118.09/118.35 elim zenon_Hc. zenon_intro zenon_TY_s. zenon_intro zenon_H13. % 118.09/118.35 apply (zenon_and_s _ _ zenon_H13). zenon_intro zenon_H15. zenon_intro zenon_H14. % 118.09/118.35 apply (zenon_and_s _ _ zenon_H14). zenon_intro zenon_H17. zenon_intro zenon_H16. % 118.09/118.35 apply (zenon_and_s _ _ zenon_H16). zenon_intro zenon_H19. zenon_intro zenon_H18. % 118.09/118.35 cut ((exemplifies_property zenon_TF_k zenon_TY_s) = (exemplifies_property zenon_TF_k zenon_TY_j)). % 118.09/118.35 intro zenon_D_pnotp. % 118.09/118.35 apply zenon_H11. % 118.09/118.35 rewrite <- zenon_D_pnotp. % 118.09/118.35 exact zenon_H17. % 118.09/118.35 cut ((zenon_TY_s = zenon_TY_j)); [idtac | apply NNPP; zenon_intro zenon_H1a]. % 118.09/118.35 cut ((zenon_TF_k = zenon_TF_k)); [idtac | apply NNPP; zenon_intro zenon_H1b]. % 118.09/118.35 congruence. % 118.09/118.35 apply zenon_H1b. apply refl_equal. % 118.09/118.35 exact (zenon_H1a zenon_H18). % 118.09/118.35 (* end of lemma zenon_L2_ *) % 118.09/118.35 apply NNPP. intro zenon_G. % 118.09/118.35 apply (zenon_notallex_s (fun X : zenon_U => (forall F : zenon_U, (forall Y : zenon_U, (((object X)/\((property F)/\(object Y)))->(((is_the X F)/\(X = Y))->(exemplifies_property F Y)))))) zenon_G); [ zenon_intro zenon_H1c; idtac ]. % 118.09/118.35 elim zenon_H1c. zenon_intro zenon_TX_l. zenon_intro zenon_H1d. % 118.09/118.35 apply (zenon_notallex_s (fun F : zenon_U => (forall Y : zenon_U, (((object zenon_TX_l)/\((property F)/\(object Y)))->(((is_the zenon_TX_l F)/\(zenon_TX_l = Y))->(exemplifies_property F Y))))) zenon_H1d); [ zenon_intro zenon_H1e; idtac ]. % 118.09/118.35 elim zenon_H1e. zenon_intro zenon_TF_k. zenon_intro zenon_H1f. % 118.09/118.35 apply (zenon_notallex_s (fun Y : zenon_U => (((object zenon_TX_l)/\((property zenon_TF_k)/\(object Y)))->(((is_the zenon_TX_l zenon_TF_k)/\(zenon_TX_l = Y))->(exemplifies_property zenon_TF_k Y)))) zenon_H1f); [ zenon_intro zenon_H20; idtac ]. % 118.09/118.35 elim zenon_H20. zenon_intro zenon_TY_j. zenon_intro zenon_H21. % 118.09/118.35 apply (zenon_notimply_s _ _ zenon_H21). zenon_intro zenon_H23. zenon_intro zenon_H22. % 118.09/118.35 apply (zenon_notimply_s _ _ zenon_H22). zenon_intro zenon_Hd. zenon_intro zenon_H11. % 118.09/118.35 apply (zenon_and_s _ _ zenon_Hd). zenon_intro zenon_H7. zenon_intro zenon_H8. % 118.09/118.35 apply (zenon_and_s _ _ zenon_H23). zenon_intro zenon_H25. zenon_intro zenon_H24. % 118.09/118.35 apply (zenon_and_s _ _ zenon_H24). zenon_intro zenon_H27. zenon_intro zenon_H26. % 118.09/118.35 generalize (description_axiom_identity_instance zenon_TF_k). zenon_intro zenon_H28. % 118.09/118.35 generalize (zenon_H28 zenon_TX_l). zenon_intro zenon_H29. % 118.09/118.35 generalize (zenon_H29 zenon_TY_j). zenon_intro zenon_H2a. % 118.09/118.35 apply (zenon_imply_s _ _ zenon_H2a); [ zenon_intro zenon_H2b | zenon_intro zenon_H5 ]. % 118.09/118.35 apply (zenon_notand_s _ _ zenon_H2b); [ zenon_intro zenon_H2d | zenon_intro zenon_H2c ]. % 118.09/118.35 exact (zenon_H2d zenon_H27). % 118.09/118.35 apply (zenon_notand_s _ _ zenon_H2c); [ zenon_intro zenon_H2f | zenon_intro zenon_H2e ]. % 118.09/118.35 exact (zenon_H2f zenon_H25). % 118.09/118.35 exact (zenon_H2e zenon_H26). % 118.09/118.35 apply (zenon_equiv_s _ _ zenon_H5); [ zenon_intro zenon_He; zenon_intro zenon_H6 | zenon_intro zenon_Hd; zenon_intro zenon_Hc ]. % 118.09/118.35 apply (zenon_L1_ zenon_TY_j zenon_TF_k zenon_TX_l); trivial. % 118.09/118.35 apply (zenon_L2_ zenon_TY_j zenon_TF_k); trivial. % 118.09/118.35 Qed. % 118.09/118.35 % SZS output end Proof % 118.09/118.35 (* END-PROOF *) % 118.09/118.35 nodes searched: 4457176 % 118.09/118.35 max branch formulas: 17821 % 118.09/118.35 proof nodes created: 167757 % 118.09/118.35 formulas created: 6699893 % 118.09/118.35 %------------------------------------------------------------------------------