%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : KRS147+1 : TPTP v8.1.0. Released v3.1.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 : Sun Jul 17 03:39:36 EDT 2022 % Result : Theorem 0.20s 0.53s % Output : Proof 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : KRS147+1 : TPTP v8.1.0. Released v3.1.0. % 0.11/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 : Tue Jun 7 11:18:02 EDT 2022 % 0.13/0.33 % CPUTime : % 0.20/0.53 (* PROOF-FOUND *) % 0.20/0.53 % SZS status Theorem % 0.20/0.53 (* BEGIN-PROOF *) % 0.20/0.53 % SZS output start Proof % 0.20/0.53 Theorem the_axiom : ((forall X : zenon_U, ((cowlThing X)/\(~(cowlNothing X))))/\((forall X : zenon_U, ((xsd_string X)<->(~(xsd_integer X))))/\((cC10 (iV8467))/\((cC48 (iV8467))/\((cC4 (iV8467))/\((cC82 (iV8467))/\((cC14 (iV8467))/\((cC8 (iV8467))/\((cC20 (iV8467))/\((cowlThing (iV8467))/\((cC62 (iV8467))/\((cC34 (iV8467))/\((cowlThing (iV8471))/\((cC80 (iV8471))/\((cC60 (iV8472))/\((cowlThing (iV8472))/\(cC58 (iV8472)))))))))))))))))). % 0.20/0.53 Proof. % 0.20/0.53 assert (zenon_L1_ : (~(forall X : zenon_U, ((xsd_string X)<->(~(xsd_integer X))))) -> False). % 0.20/0.53 do 0 intro. intros zenon_H57. % 0.20/0.53 exact (zenon_H57 axiom_1). % 0.20/0.53 (* end of lemma zenon_L1_ *) % 0.20/0.53 assert (zenon_L2_ : (~(~(cC2 (iV8475)))) -> False). % 0.20/0.53 do 0 intro. intros zenon_H58. % 0.20/0.53 exact (zenon_H58 axiom_82). % 0.20/0.53 (* end of lemma zenon_L2_ *) % 0.20/0.53 assert (zenon_L3_ : (~(exists Y : zenon_U, ((rR1 (iV8467) Y)/\(~(cC2 Y))))) -> False). % 0.20/0.53 do 0 intro. intros zenon_H59. % 0.20/0.53 apply zenon_H59. exists (iV8475). apply NNPP. zenon_intro zenon_H5a. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_H5a); [ zenon_intro zenon_H5b | zenon_intro zenon_H58 ]. % 0.20/0.53 exact (zenon_H5b axiom_59). % 0.20/0.53 exact (zenon_H58 axiom_82). % 0.20/0.53 (* end of lemma zenon_L3_ *) % 0.20/0.53 assert (zenon_L4_ : (~(cC4 (iV8467))) -> False). % 0.20/0.53 do 0 intro. intros zenon_H5c. % 0.20/0.53 generalize (axiom_17 (iV8467)). zenon_intro zenon_H5d. % 0.20/0.53 apply (zenon_equiv_s _ _ zenon_H5d); [ zenon_intro zenon_H5c; zenon_intro zenon_H59 | zenon_intro zenon_H5f; zenon_intro zenon_H5e ]. % 0.20/0.53 apply (zenon_L3_); trivial. % 0.20/0.53 exact (zenon_H5c zenon_H5f). % 0.20/0.53 (* end of lemma zenon_L4_ *) % 0.20/0.53 assert (zenon_L5_ : (~(exists Y : zenon_U, ((rR1 (iV8471) Y)/\(~(cC2 Y))))) -> (~(cC8 (iV8467))) -> False). % 0.20/0.53 do 0 intro. intros zenon_H60 zenon_H61. % 0.20/0.53 generalize (axiom_39 (iV8467)). zenon_intro zenon_H62. % 0.20/0.53 apply (zenon_equiv_s _ _ zenon_H62); [ zenon_intro zenon_H61; zenon_intro zenon_H65 | zenon_intro zenon_H64; zenon_intro zenon_H63 ]. % 0.20/0.53 apply zenon_H65. exists (iV8471). apply NNPP. zenon_intro zenon_H66. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_H66); [ zenon_intro zenon_H68 | zenon_intro zenon_H67 ]. % 0.20/0.53 exact (zenon_H68 axiom_55). % 0.20/0.53 apply zenon_H67. zenon_intro zenon_H69. % 0.20/0.53 generalize (axiom_28 (iV8471)). zenon_intro zenon_H6a. % 0.20/0.53 apply (zenon_equiv_s _ _ zenon_H6a); [ zenon_intro zenon_H6c; zenon_intro zenon_H60 | zenon_intro zenon_H69; zenon_intro zenon_H6b ]. % 0.20/0.53 exact (zenon_H6c zenon_H69). % 0.20/0.53 exact (zenon_H60 zenon_H6b). % 0.20/0.53 exact (zenon_H61 zenon_H64). % 0.20/0.53 (* end of lemma zenon_L5_ *) % 0.20/0.53 assert (zenon_L6_ : (~(exists Y : zenon_U, ((rR1 (iV8471) Y)/\(~(cC2 Y))))) -> (~(cC80 (iV8471))) -> False). % 0.20/0.53 do 0 intro. intros zenon_H60 zenon_H6d. % 0.20/0.53 generalize (axiom_40 (iV8471)). zenon_intro zenon_H6e. % 0.20/0.53 apply (zenon_equiv_s _ _ zenon_H6e); [ zenon_intro zenon_H6d; zenon_intro zenon_H71 | zenon_intro zenon_H70; zenon_intro zenon_H6f ]. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_H71); [ zenon_intro zenon_H73 | zenon_intro zenon_H72 ]. % 0.20/0.53 exact (zenon_H73 axiom_70). % 0.20/0.53 apply zenon_H72. zenon_intro zenon_H74. % 0.20/0.53 generalize (axiom_38 (iV8471)). zenon_intro zenon_H75. % 0.20/0.53 apply (zenon_equiv_s _ _ zenon_H75); [ zenon_intro axiom_71; zenon_intro zenon_H60 | zenon_intro zenon_H74; zenon_intro zenon_H6b ]. % 0.20/0.53 exact (axiom_71 zenon_H74). % 0.20/0.53 exact (zenon_H60 zenon_H6b). % 0.20/0.53 exact (zenon_H6d zenon_H70). % 0.20/0.53 (* end of lemma zenon_L6_ *) % 0.20/0.53 assert (zenon_L7_ : (~(exists Y : zenon_U, ((rR1 (iV8471) Y)/\(~(cC2 Y))))) -> (~(cC82 (iV8467))) -> False). % 0.20/0.53 do 0 intro. intros zenon_H60 zenon_H76. % 0.20/0.53 generalize (axiom_41 (iV8467)). zenon_intro zenon_H77. % 0.20/0.53 apply (zenon_equiv_s _ _ zenon_H77); [ zenon_intro zenon_H76; zenon_intro zenon_H7a | zenon_intro zenon_H79; zenon_intro zenon_H78 ]. % 0.20/0.53 apply zenon_H7a. exists (iV8471). apply NNPP. zenon_intro zenon_H7b. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_H7b); [ zenon_intro zenon_H68 | zenon_intro zenon_H6d ]. % 0.20/0.53 exact (zenon_H68 axiom_55). % 0.20/0.53 apply (zenon_L6_); trivial. % 0.20/0.53 exact (zenon_H76 zenon_H79). % 0.20/0.53 (* end of lemma zenon_L7_ *) % 0.20/0.53 assert (zenon_L8_ : (~(cC14 (iV8467))) -> False). % 0.20/0.53 do 0 intro. intros zenon_H7c. % 0.20/0.53 generalize (axiom_4 (iV8467)). zenon_intro zenon_H7d. % 0.20/0.53 apply (zenon_equiv_s _ _ zenon_H7d); [ zenon_intro zenon_H7c; zenon_intro zenon_H80 | zenon_intro zenon_H7f; zenon_intro zenon_H7e ]. % 0.20/0.53 apply zenon_H80. exists (iV8470). apply NNPP. zenon_intro zenon_H81. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_H81); [ zenon_intro zenon_H83 | zenon_intro zenon_H82 ]. % 0.20/0.53 exact (zenon_H83 axiom_62). % 0.20/0.53 exact (zenon_H82 axiom_68). % 0.20/0.53 exact (zenon_H7c zenon_H7f). % 0.20/0.53 (* end of lemma zenon_L8_ *) % 0.20/0.53 assert (zenon_L9_ : (~(cC58 (iV8472))) -> False). % 0.20/0.53 do 0 intro. intros zenon_H84. % 0.20/0.53 generalize (axiom_27 (iV8472)). zenon_intro zenon_H85. % 0.20/0.53 apply (zenon_equiv_s _ _ zenon_H85); [ zenon_intro zenon_H84; zenon_intro zenon_H88 | zenon_intro zenon_H87; zenon_intro zenon_H86 ]. % 0.20/0.53 apply zenon_H88. exists (iV8476). apply NNPP. zenon_intro zenon_H89. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_H89); [ zenon_intro zenon_H8b | zenon_intro zenon_H8a ]. % 0.20/0.53 exact (zenon_H8b axiom_76). % 0.20/0.53 exact (zenon_H8a axiom_84). % 0.20/0.53 exact (zenon_H84 zenon_H87). % 0.20/0.53 (* end of lemma zenon_L9_ *) % 0.20/0.53 assert (zenon_L10_ : (~(cC60 (iV8472))) -> False). % 0.20/0.53 do 0 intro. intros zenon_H8c. % 0.20/0.53 generalize (axiom_29 (iV8472)). zenon_intro zenon_H8d. % 0.20/0.53 apply (zenon_equiv_s _ _ zenon_H8d); [ zenon_intro zenon_H8c; zenon_intro zenon_H90 | zenon_intro zenon_H8f; zenon_intro zenon_H8e ]. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_H90); [ zenon_intro zenon_H84 | zenon_intro zenon_H91 ]. % 0.20/0.53 apply (zenon_L9_); trivial. % 0.20/0.53 exact (zenon_H91 axiom_74). % 0.20/0.53 exact (zenon_H8c zenon_H8f). % 0.20/0.53 (* end of lemma zenon_L10_ *) % 0.20/0.53 assert (zenon_L11_ : (~(cC62 (iV8467))) -> False). % 0.20/0.53 do 0 intro. intros zenon_H92. % 0.20/0.53 generalize (axiom_30 (iV8467)). zenon_intro zenon_H93. % 0.20/0.53 apply (zenon_equiv_s _ _ zenon_H93); [ zenon_intro zenon_H92; zenon_intro zenon_H96 | zenon_intro zenon_H95; zenon_intro zenon_H94 ]. % 0.20/0.53 apply zenon_H96. exists (iV8472). apply NNPP. zenon_intro zenon_H97. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_H97); [ zenon_intro zenon_H98 | zenon_intro zenon_H8c ]. % 0.20/0.53 exact (zenon_H98 axiom_60). % 0.20/0.53 apply (zenon_L10_); trivial. % 0.20/0.53 exact (zenon_H92 zenon_H95). % 0.20/0.53 (* end of lemma zenon_L11_ *) % 0.20/0.53 assert (zenon_L12_ : (~(exists Y : zenon_U, ((rR1 (iV8474) Y)/\(cC2 Y)))) -> (~(cC34 (iV8467))) -> False). % 0.20/0.53 do 0 intro. intros zenon_H99 zenon_H9a. % 0.20/0.53 generalize (axiom_14 (iV8467)). zenon_intro zenon_H9b. % 0.20/0.53 apply (zenon_equiv_s _ _ zenon_H9b); [ zenon_intro zenon_H9a; zenon_intro zenon_H9e | zenon_intro zenon_H9d; zenon_intro zenon_H9c ]. % 0.20/0.53 apply zenon_H9e. exists (iV8474). apply NNPP. zenon_intro zenon_H9f. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_H9f); [ zenon_intro zenon_Ha1 | zenon_intro zenon_Ha0 ]. % 0.20/0.53 exact (zenon_Ha1 axiom_61). % 0.20/0.53 apply zenon_Ha0. zenon_intro zenon_Ha2. % 0.20/0.53 generalize (axiom_13 (iV8474)). zenon_intro zenon_Ha3. % 0.20/0.53 apply (zenon_equiv_s _ _ zenon_Ha3); [ zenon_intro axiom_80; zenon_intro zenon_H99 | zenon_intro zenon_Ha2; zenon_intro zenon_Ha4 ]. % 0.20/0.53 exact (axiom_80 zenon_Ha2). % 0.20/0.53 exact (zenon_H99 zenon_Ha4). % 0.20/0.53 exact (zenon_H9a zenon_H9d). % 0.20/0.53 (* end of lemma zenon_L12_ *) % 0.20/0.53 apply NNPP. intro zenon_G. % 0.20/0.53 generalize (axiom_38 (iV8471)). zenon_intro zenon_H75. % 0.20/0.53 apply (zenon_equiv_s _ _ zenon_H75); [ zenon_intro axiom_71; zenon_intro zenon_H60 | zenon_intro zenon_H74; zenon_intro zenon_H6b ]. % 0.20/0.53 generalize (axiom_13 (iV8474)). zenon_intro zenon_Ha3. % 0.20/0.53 apply (zenon_equiv_s _ _ zenon_Ha3); [ zenon_intro axiom_80; zenon_intro zenon_H99 | zenon_intro zenon_Ha2; zenon_intro zenon_Ha4 ]. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_G); [ zenon_intro zenon_Ha6 | zenon_intro zenon_Ha5 ]. % 0.20/0.53 exact (zenon_Ha6 axiom_0). % 0.20/0.53 apply (zenon_notand_s _ _ zenon_Ha5); [ zenon_intro zenon_H57 | zenon_intro zenon_Ha7 ]. % 0.20/0.53 exact (zenon_H57 axiom_1). % 0.20/0.53 apply (zenon_notand_s _ _ zenon_Ha7); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Ha8 ]. % 0.20/0.53 generalize (axiom_2 (iV8467)). zenon_intro zenon_Haa. % 0.20/0.53 apply (zenon_equiv_s _ _ zenon_Haa); [ zenon_intro zenon_Ha9; zenon_intro zenon_Had | zenon_intro zenon_Hac; zenon_intro zenon_Hab ]. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_Had); [ zenon_intro zenon_H5c | zenon_intro zenon_H61 ]. % 0.20/0.53 apply (zenon_L4_); trivial. % 0.20/0.53 apply (zenon_L5_); trivial. % 0.20/0.53 exact (zenon_Ha9 zenon_Hac). % 0.20/0.53 apply (zenon_notand_s _ _ zenon_Ha8); [ zenon_intro zenon_Haf | zenon_intro zenon_Hae ]. % 0.20/0.53 generalize (axiom_22 (iV8467)). zenon_intro zenon_Hb0. % 0.20/0.53 apply (zenon_equiv_s _ _ zenon_Hb0); [ zenon_intro zenon_Haf; zenon_intro zenon_H59 | zenon_intro zenon_Hb1; zenon_intro zenon_H5e ]. % 0.20/0.53 apply (zenon_L3_); trivial. % 0.20/0.53 exact (zenon_Haf zenon_Hb1). % 0.20/0.53 apply (zenon_notand_s _ _ zenon_Hae); [ zenon_intro zenon_H5c | zenon_intro zenon_Hb2 ]. % 0.20/0.53 apply (zenon_L4_); trivial. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_Hb2); [ zenon_intro zenon_H76 | zenon_intro zenon_Hb3 ]. % 0.20/0.53 apply (zenon_L7_); trivial. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_Hb3); [ zenon_intro zenon_H7c | zenon_intro zenon_Hb4 ]. % 0.20/0.53 apply (zenon_L8_); trivial. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_Hb4); [ zenon_intro zenon_H61 | zenon_intro zenon_Hb5 ]. % 0.20/0.53 apply (zenon_L5_); trivial. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_Hb5); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hb6 ]. % 0.20/0.53 generalize (axiom_7 (iV8467)). zenon_intro zenon_Hb8. % 0.20/0.53 apply (zenon_equiv_s _ _ zenon_Hb8); [ zenon_intro zenon_Hb7; zenon_intro zenon_H59 | zenon_intro zenon_Hb9; zenon_intro zenon_H5e ]. % 0.20/0.53 apply (zenon_L3_); trivial. % 0.20/0.53 exact (zenon_Hb7 zenon_Hb9). % 0.20/0.53 apply (zenon_notand_s _ _ zenon_Hb6); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hba ]. % 0.20/0.53 exact (zenon_Hbb axiom_52). % 0.20/0.53 apply (zenon_notand_s _ _ zenon_Hba); [ zenon_intro zenon_H92 | zenon_intro zenon_Hbc ]. % 0.20/0.53 apply (zenon_L11_); trivial. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_Hbc); [ zenon_intro zenon_H9a | zenon_intro zenon_Hbd ]. % 0.20/0.53 apply (zenon_L12_); trivial. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_Hbd); [ zenon_intro zenon_Hbf | zenon_intro zenon_Hbe ]. % 0.20/0.53 exact (zenon_Hbf axiom_72). % 0.20/0.53 apply (zenon_notand_s _ _ zenon_Hbe); [ zenon_intro zenon_H6d | zenon_intro zenon_Hc0 ]. % 0.20/0.53 apply (zenon_L6_); trivial. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_Hc0); [ zenon_intro zenon_H8c | zenon_intro zenon_Hc1 ]. % 0.20/0.53 apply (zenon_L10_); trivial. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_Hc1); [ zenon_intro zenon_Hc2 | zenon_intro zenon_H84 ]. % 0.20/0.53 exact (zenon_Hc2 axiom_75). % 0.20/0.53 apply (zenon_L9_); trivial. % 0.20/0.53 exact (axiom_80 zenon_Ha2). % 0.20/0.53 exact (axiom_71 zenon_H74). % 0.20/0.53 Qed. % 0.20/0.53 % SZS output end Proof % 0.20/0.53 (* END-PROOF *) % 0.20/0.53 nodes searched: 1115 % 0.20/0.53 max branch formulas: 245 % 0.20/0.53 proof nodes created: 96 % 0.20/0.53 formulas created: 3495 % 0.20/0.53 %------------------------------------------------------------------------------