%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SWB014+2 : TPTP v8.1.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n025.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 19:26:47 EDT 2022 % Result : Theorem 4.46s 4.65s % Output : Proof 4.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWB014+2 : TPTP v8.1.0. Released v5.2.0. % 0.06/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n025.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Wed Jun 1 08:48:28 EDT 2022 % 0.12/0.33 % CPUTime : % 4.46/4.65 (* PROOF-FOUND *) % 4.46/4.65 % SZS status Theorem % 4.46/4.65 (* BEGIN-PROOF *) % 4.46/4.65 % SZS output start Proof % 4.46/4.65 Theorem testcase_conclusion_fullish_014_Harry_belongs_to_some_Species : (exists BNODE_x : zenon_U, ((iext (uri_rdf_type) (uri_ex_harry) BNODE_x)/\(iext (uri_rdf_type) BNODE_x (uri_ex_Species)))). % 4.46/4.65 Proof. % 4.46/4.65 assert (zenon_L1_ : forall (zenon_TBNODE_u_h : zenon_U), (forall C : zenon_U, ((iext (uri_rdf_type) (uri_ex_harry) C)<->(icext C (uri_ex_harry)))) -> (iext (uri_rdf_type) (uri_ex_harry) zenon_TBNODE_u_h) -> (~(icext zenon_TBNODE_u_h (uri_ex_harry))) -> False). % 4.46/4.65 do 1 intro. intros zenon_H4 zenon_H5 zenon_H6. % 4.46/4.65 generalize (zenon_H4 zenon_TBNODE_u_h). zenon_intro zenon_H8. % 4.46/4.65 apply (zenon_equiv_s _ _ zenon_H8); [ zenon_intro zenon_Ha; zenon_intro zenon_H6 | zenon_intro zenon_H5; zenon_intro zenon_H9 ]. % 4.46/4.65 exact (zenon_Ha zenon_H5). % 4.46/4.65 exact (zenon_H6 zenon_H9). % 4.46/4.65 (* end of lemma zenon_L1_ *) % 4.46/4.65 assert (zenon_L2_ : ((icext (uri_ex_Eagle) (uri_ex_harry))\/(icext (uri_ex_Falcon) (uri_ex_harry))) -> (~(icext (uri_ex_Falcon) (uri_ex_harry))) -> (~(icext (uri_ex_Eagle) (uri_ex_harry))) -> False). % 4.46/4.65 do 0 intro. intros zenon_Hb zenon_Hc zenon_Hd. % 4.46/4.65 apply (zenon_or_s _ _ zenon_Hb); [ zenon_intro zenon_Hf | zenon_intro zenon_He ]. % 4.46/4.65 exact (zenon_Hd zenon_Hf). % 4.46/4.65 exact (zenon_Hc zenon_He). % 4.46/4.65 (* end of lemma zenon_L2_ *) % 4.46/4.65 apply NNPP. intro zenon_G. % 4.46/4.65 elim testcase_premise_fullish_014_Harry_belongs_to_some_Species. zenon_intro zenon_TBNODE_u_h. zenon_intro zenon_H10. % 4.46/4.65 elim zenon_H10. zenon_intro zenon_TBNODE_l1_r. zenon_intro zenon_H12. % 4.46/4.65 elim zenon_H12. zenon_intro zenon_TBNODE_l2_t. zenon_intro zenon_H14. % 4.46/4.65 apply (zenon_and_s _ _ zenon_H14). zenon_intro zenon_H16. zenon_intro zenon_H15. % 4.46/4.65 apply (zenon_and_s _ _ zenon_H15). zenon_intro zenon_H18. zenon_intro zenon_H17. % 4.46/4.65 apply (zenon_and_s _ _ zenon_H17). zenon_intro zenon_H5. zenon_intro zenon_H19. % 4.46/4.65 apply (zenon_and_s _ _ zenon_H19). zenon_intro zenon_H1b. zenon_intro zenon_H1a. % 4.46/4.65 apply (zenon_and_s _ _ zenon_H1a). zenon_intro zenon_H1d. zenon_intro zenon_H1c. % 4.46/4.65 apply (zenon_and_s _ _ zenon_H1c). zenon_intro zenon_H1f. zenon_intro zenon_H1e. % 4.46/4.65 apply (zenon_and_s _ _ zenon_H1e). zenon_intro zenon_H21. zenon_intro zenon_H20. % 4.46/4.65 apply zenon_G. exists (uri_ex_Falcon). apply NNPP. zenon_intro zenon_H22. % 4.46/4.65 apply (zenon_notand_s _ _ zenon_H22); [ zenon_intro zenon_H24 | zenon_intro zenon_H23 ]. % 4.46/4.65 apply zenon_G. exists (uri_ex_Eagle). apply NNPP. zenon_intro zenon_H25. % 4.46/4.65 apply (zenon_notand_s _ _ zenon_H25); [ zenon_intro zenon_H27 | zenon_intro zenon_H26 ]. % 4.46/4.65 generalize (rdfs_cext_def (uri_ex_harry)). zenon_intro zenon_H4. % 4.46/4.65 generalize (zenon_H4 (uri_ex_Falcon)). zenon_intro zenon_H28. % 4.46/4.65 apply (zenon_equiv_s _ _ zenon_H28); [ zenon_intro zenon_H24; zenon_intro zenon_Hc | zenon_intro zenon_H29; zenon_intro zenon_He ]. % 4.46/4.65 generalize (zenon_H4 (uri_ex_Eagle)). zenon_intro zenon_H2a. % 4.46/4.65 apply (zenon_equiv_s _ _ zenon_H2a); [ zenon_intro zenon_H27; zenon_intro zenon_Hd | zenon_intro zenon_H2b; zenon_intro zenon_Hf ]. % 4.46/4.65 generalize (owl_bool_unionof_class_002 zenon_TBNODE_u_h). zenon_intro zenon_H2c. % 4.46/4.65 generalize (zenon_H2c zenon_TBNODE_l1_r). zenon_intro zenon_H2d. % 4.46/4.65 generalize (zenon_H2d (uri_ex_Eagle)). zenon_intro zenon_H2e. % 4.46/4.65 generalize (zenon_H2e zenon_TBNODE_l2_t). zenon_intro zenon_H2f. % 4.46/4.65 generalize (zenon_H2f (uri_ex_Falcon)). zenon_intro zenon_H30. % 4.46/4.65 apply (zenon_imply_s _ _ zenon_H30); [ zenon_intro zenon_H32 | zenon_intro zenon_H31 ]. % 4.46/4.65 apply (zenon_notand_s _ _ zenon_H32); [ zenon_intro zenon_H34 | zenon_intro zenon_H33 ]. % 4.46/4.65 exact (zenon_H34 zenon_H1d). % 4.46/4.65 apply (zenon_notand_s _ _ zenon_H33); [ zenon_intro zenon_H36 | zenon_intro zenon_H35 ]. % 4.46/4.65 exact (zenon_H36 zenon_H1f). % 4.46/4.65 apply (zenon_notand_s _ _ zenon_H35); [ zenon_intro zenon_H38 | zenon_intro zenon_H37 ]. % 4.46/4.65 exact (zenon_H38 zenon_H21). % 4.46/4.65 exact (zenon_H37 zenon_H20). % 4.46/4.65 apply (zenon_equiv_s _ _ zenon_H31); [ zenon_intro zenon_H3b; zenon_intro zenon_H3a | zenon_intro zenon_H1b; zenon_intro zenon_H39 ]. % 4.46/4.65 exact (zenon_H3b zenon_H1b). % 4.46/4.65 apply (zenon_and_s _ _ zenon_H39). zenon_intro zenon_H3d. zenon_intro zenon_H3c. % 4.46/4.65 apply (zenon_and_s _ _ zenon_H3c). zenon_intro zenon_H3f. zenon_intro zenon_H3e. % 4.46/4.65 apply (zenon_and_s _ _ zenon_H3e). zenon_intro zenon_H41. zenon_intro zenon_H40. % 4.46/4.65 generalize (zenon_H40 (uri_ex_harry)). zenon_intro zenon_H42. % 4.46/4.65 apply (zenon_equiv_s _ _ zenon_H42); [ zenon_intro zenon_H6; zenon_intro zenon_H43 | zenon_intro zenon_H9; zenon_intro zenon_Hb ]. % 4.46/4.65 apply (zenon_L1_ zenon_TBNODE_u_h); trivial. % 4.46/4.65 apply (zenon_L2_); trivial. % 4.46/4.65 exact (zenon_H27 zenon_H2b). % 4.46/4.65 exact (zenon_H24 zenon_H29). % 4.46/4.65 exact (zenon_H26 zenon_H16). % 4.46/4.65 exact (zenon_H23 zenon_H18). % 4.46/4.65 Qed. % 4.46/4.65 % SZS output end Proof % 4.46/4.65 (* END-PROOF *) % 4.46/4.65 nodes searched: 444932 % 4.46/4.65 max branch formulas: 7866 % 4.46/4.65 proof nodes created: 5884 % 4.46/4.65 formulas created: 677177 % 4.46/4.65 %------------------------------------------------------------------------------