%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : KRS157+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n029.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:38 EDT 2022 % Result : Theorem 0.39s 0.54s % Output : Proof 0.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : KRS157+1 : TPTP v8.1.0. Released v3.1.0. % 0.08/0.14 % Command : run_zenon %s %d % 0.14/0.35 % Computer : n029.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Tue Jun 7 16:29:05 EDT 2022 % 0.14/0.36 % CPUTime : % 0.39/0.54 (* PROOF-FOUND *) % 0.39/0.54 % SZS status Theorem % 0.39/0.54 (* BEGIN-PROOF *) % 0.39/0.54 % SZS output start Proof % 0.39/0.54 Theorem the_axiom : ((forall X : zenon_U, ((cowlThing X)/\(~(cowlNothing X))))/\((forall X : zenon_U, ((xsd_string X)<->(~(xsd_integer X))))/\((cC14 (iV3102))/\((cC44 (iV3102))/\((cC216 (iV3102))/\((cC64 (iV3102))/\((cC46 (iV3102))/\((cC28 (iV3102))/\((cowlThing (iV3102))/\(cC30 (iV3102))))))))))). % 0.39/0.54 Proof. % 0.39/0.54 apply NNPP. intro zenon_G. % 0.39/0.54 generalize (axiom_201 (iV3102)). zenon_intro zenon_Hdc. % 0.39/0.54 apply (zenon_equiv_s _ _ zenon_Hdc); [ zenon_intro zenon_Hdf; zenon_intro zenon_Hde | zenon_intro axiom_202; zenon_intro zenon_Hdd ]. % 0.39/0.54 exact (zenon_Hdf axiom_202). % 0.39/0.54 apply (zenon_and_s _ _ zenon_Hdd). zenon_intro zenon_He1. zenon_intro zenon_He0. % 0.39/0.54 generalize (axiom_121 (iV3102)). zenon_intro zenon_He2. % 0.39/0.54 apply (zenon_equiv_s _ _ zenon_He2); [ zenon_intro zenon_He5; zenon_intro zenon_He4 | zenon_intro zenon_He1; zenon_intro zenon_He3 ]. % 0.39/0.54 exact (zenon_He5 zenon_He1). % 0.39/0.54 apply (zenon_and_s _ _ zenon_He3). zenon_intro zenon_He6. zenon_intro axiom_216. % 0.39/0.54 generalize (axiom_166 (iV3102)). zenon_intro zenon_He7. % 0.39/0.54 apply (zenon_equiv_s _ _ zenon_He7); [ zenon_intro zenon_Hea; zenon_intro zenon_He9 | zenon_intro zenon_He6; zenon_intro zenon_He8 ]. % 0.39/0.54 exact (zenon_Hea zenon_He6). % 0.39/0.54 generalize (axiom_148 (iV3102)). zenon_intro zenon_Heb. % 0.39/0.54 apply (zenon_equiv_s _ _ zenon_Heb); [ zenon_intro zenon_Hee; zenon_intro zenon_Hed | zenon_intro zenon_He0; zenon_intro zenon_Hec ]. % 0.39/0.54 exact (zenon_Hee zenon_He0). % 0.39/0.54 apply (zenon_and_s _ _ zenon_Hec). zenon_intro zenon_Hf0. zenon_intro zenon_Hef. % 0.39/0.54 generalize (axiom_132 (iV3102)). zenon_intro zenon_Hf1. % 0.39/0.54 apply (zenon_equiv_s _ _ zenon_Hf1); [ zenon_intro zenon_Hf4; zenon_intro zenon_Hf3 | zenon_intro zenon_Hf0; zenon_intro zenon_Hf2 ]. % 0.39/0.54 exact (zenon_Hf4 zenon_Hf0). % 0.39/0.54 apply (zenon_and_s _ _ zenon_Hf2). zenon_intro zenon_Hf6. zenon_intro zenon_Hf5. % 0.39/0.54 generalize (axiom_131 (iV3102)). zenon_intro zenon_Hf7. % 0.39/0.54 apply (zenon_equiv_s _ _ zenon_Hf7); [ zenon_intro zenon_Hfa; zenon_intro zenon_Hf9 | zenon_intro zenon_Hf6; zenon_intro zenon_Hf8 ]. % 0.39/0.54 exact (zenon_Hfa zenon_Hf6). % 0.39/0.55 generalize (axiom_44 (iV3102)). zenon_intro zenon_Hfb. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_Hfb); [ zenon_intro zenon_Hfe; zenon_intro zenon_Hfd | zenon_intro zenon_Hf5; zenon_intro zenon_Hfc ]. % 0.39/0.55 exact (zenon_Hfe zenon_Hf5). % 0.39/0.55 generalize (axiom_147 (iV3102)). zenon_intro zenon_Hff. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_Hff); [ zenon_intro zenon_H102; zenon_intro zenon_H101 | zenon_intro zenon_Hef; zenon_intro zenon_H100 ]. % 0.39/0.55 exact (zenon_H102 zenon_Hef). % 0.39/0.55 apply (zenon_notand_s _ _ zenon_G); [ zenon_intro zenon_H104 | zenon_intro zenon_H103 ]. % 0.39/0.55 exact (zenon_H104 axiom_0). % 0.39/0.55 apply (zenon_notand_s _ _ zenon_H103); [ zenon_intro zenon_H106 | zenon_intro zenon_H105 ]. % 0.39/0.55 exact (zenon_H106 axiom_1). % 0.39/0.55 apply (zenon_notand_s _ _ zenon_H105); [ zenon_intro zenon_Hfe | zenon_intro zenon_H107 ]. % 0.39/0.55 generalize (axiom_44 (iV3102)). zenon_intro zenon_Hfb. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_Hfb); [ zenon_intro zenon_Hfe; zenon_intro zenon_Hfd | zenon_intro zenon_Hf5; zenon_intro zenon_Hfc ]. % 0.39/0.55 exact (zenon_Hfd zenon_Hfc). % 0.39/0.55 exact (zenon_Hfe zenon_Hf5). % 0.39/0.55 apply (zenon_notand_s _ _ zenon_H107); [ zenon_intro zenon_H102 | zenon_intro zenon_H108 ]. % 0.39/0.55 generalize (axiom_147 (iV3102)). zenon_intro zenon_Hff. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_Hff); [ zenon_intro zenon_H102; zenon_intro zenon_H101 | zenon_intro zenon_Hef; zenon_intro zenon_H100 ]. % 0.39/0.55 exact (zenon_H101 zenon_H100). % 0.39/0.55 exact (zenon_H102 zenon_Hef). % 0.39/0.55 apply (zenon_notand_s _ _ zenon_H108); [ zenon_intro zenon_He5 | zenon_intro zenon_H109 ]. % 0.39/0.55 generalize (axiom_121 (iV3102)). zenon_intro zenon_He2. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_He2); [ zenon_intro zenon_He5; zenon_intro zenon_He4 | zenon_intro zenon_He1; zenon_intro zenon_He3 ]. % 0.39/0.55 exact (zenon_He4 zenon_He3). % 0.39/0.55 exact (zenon_He5 zenon_He1). % 0.39/0.55 apply (zenon_notand_s _ _ zenon_H109); [ zenon_intro zenon_Hea | zenon_intro zenon_H10a ]. % 0.39/0.55 generalize (axiom_166 (iV3102)). zenon_intro zenon_He7. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_He7); [ zenon_intro zenon_Hea; zenon_intro zenon_He9 | zenon_intro zenon_He6; zenon_intro zenon_He8 ]. % 0.39/0.55 exact (zenon_He9 zenon_He8). % 0.39/0.55 exact (zenon_Hea zenon_He6). % 0.39/0.55 apply (zenon_notand_s _ _ zenon_H10a); [ zenon_intro zenon_Hee | zenon_intro zenon_H10b ]. % 0.39/0.55 generalize (axiom_148 (iV3102)). zenon_intro zenon_Heb. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_Heb); [ zenon_intro zenon_Hee; zenon_intro zenon_Hed | zenon_intro zenon_He0; zenon_intro zenon_Hec ]. % 0.39/0.55 exact (zenon_Hed zenon_Hec). % 0.39/0.55 exact (zenon_Hee zenon_He0). % 0.39/0.55 apply (zenon_notand_s _ _ zenon_H10b); [ zenon_intro zenon_Hfa | zenon_intro zenon_H10c ]. % 0.39/0.55 generalize (axiom_131 (iV3102)). zenon_intro zenon_Hf7. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_Hf7); [ zenon_intro zenon_Hfa; zenon_intro zenon_Hf9 | zenon_intro zenon_Hf6; zenon_intro zenon_Hf8 ]. % 0.39/0.55 exact (zenon_Hf9 zenon_Hf8). % 0.39/0.55 exact (zenon_Hfa zenon_Hf6). % 0.39/0.55 apply (zenon_notand_s _ _ zenon_H10c); [ zenon_intro zenon_H10d | zenon_intro zenon_Hf4 ]. % 0.39/0.55 exact (zenon_H10d axiom_217). % 0.39/0.55 generalize (axiom_132 (iV3102)). zenon_intro zenon_Hf1. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_Hf1); [ zenon_intro zenon_Hf4; zenon_intro zenon_Hf3 | zenon_intro zenon_Hf0; zenon_intro zenon_Hf2 ]. % 0.39/0.55 exact (zenon_Hf3 zenon_Hf2). % 0.39/0.55 exact (zenon_Hf4 zenon_Hf0). % 0.39/0.55 Qed. % 0.39/0.55 % SZS output end Proof % 0.39/0.55 (* END-PROOF *) % 0.39/0.55 nodes searched: 56 % 0.39/0.55 max branch formulas: 142 % 0.39/0.55 proof nodes created: 36 % 0.39/0.55 formulas created: 2143 % 0.39/0.55 %------------------------------------------------------------------------------