%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : KRS154+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n019.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:37 EDT 2022 % Result : Theorem 0.19s 0.52s % Output : Proof 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : KRS154+1 : TPTP v8.1.0. Released v3.1.0. % 0.06/0.12 % Command : run_zenon %s %d % 0.11/0.32 % Computer : n019.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 600 % 0.11/0.32 % DateTime : Tue Jun 7 16:24:40 EDT 2022 % 0.11/0.32 % CPUTime : % 0.19/0.52 (* PROOF-FOUND *) % 0.19/0.52 % SZS status Theorem % 0.19/0.52 (* BEGIN-PROOF *) % 0.19/0.52 % SZS output start Proof % 0.19/0.52 Theorem the_axiom : ((forall X : zenon_U, ((cowlThing X)/\(~(cowlNothing X))))/\((forall X : zenon_U, ((xsd_string X)<->(~(xsd_integer X))))/\((cC58 (iV822576))/\((cC116 (iV822576))/\((cC114 (iV822576))/\((cowlThing (iV822576))/\((cC94 (iV822576))/\((cC80 (iV822576))/\((cC110 (iV822576))/\((cC136 (iV822576))/\(cC56 (iV822576)))))))))))). % 0.19/0.52 Proof. % 0.19/0.52 assert (zenon_L1_ : (~(exists Y : zenon_U, (ra_Px1 (iV822576) Y))) -> (exists Y : zenon_U, (ra_Px16 (iV822576) Y)) -> (~(cC56 (iV822576))) -> False). % 0.19/0.52 do 0 intro. intros zenon_Haa zenon_Hab zenon_Hac. % 0.19/0.52 generalize (axiom_93 (iV822576)). zenon_intro zenon_Had. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Had); [ zenon_intro zenon_Hac; zenon_intro zenon_Hb0 | zenon_intro zenon_Haf; zenon_intro zenon_Hae ]. % 0.19/0.52 apply (zenon_notand_s _ _ zenon_Hb0); [ zenon_intro zenon_Hb2 | zenon_intro zenon_Hb1 ]. % 0.19/0.52 generalize (axiom_75 (iV822576)). zenon_intro zenon_Hb3. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hb3); [ zenon_intro zenon_Hb2; zenon_intro zenon_Hb4 | zenon_intro axiom_149; zenon_intro zenon_Haa ]. % 0.19/0.52 exact (zenon_Hb4 zenon_Haa). % 0.19/0.52 exact (zenon_Hb2 axiom_149). % 0.19/0.52 generalize (axiom_3 (iV822576)). zenon_intro zenon_Hb5. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hb5); [ zenon_intro zenon_Hb1; zenon_intro zenon_Hb6 | zenon_intro axiom_167; zenon_intro zenon_Hab ]. % 0.19/0.52 exact (zenon_Hb6 zenon_Hab). % 0.19/0.52 exact (zenon_Hb1 axiom_167). % 0.19/0.52 exact (zenon_Hac zenon_Haf). % 0.19/0.52 (* end of lemma zenon_L1_ *) % 0.19/0.52 assert (zenon_L2_ : (~(exists Y0 : zenon_U, (ra_Px39 (iV822576) Y0))) -> (~(exists Y0 : zenon_U, (ra_Px38 (iV822576) Y0))) -> (~(cC114 (iV822576))) -> False). % 0.19/0.52 do 0 intro. intros zenon_Hb7 zenon_Hb8 zenon_Hb9. % 0.19/0.52 generalize (axiom_21 (iV822576)). zenon_intro zenon_Hba. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hba); [ zenon_intro zenon_Hb9; zenon_intro zenon_Hbd | zenon_intro zenon_Hbc; zenon_intro zenon_Hbb ]. % 0.19/0.52 apply (zenon_notand_s _ _ zenon_Hbd); [ zenon_intro zenon_Hbf | zenon_intro zenon_Hbe ]. % 0.19/0.52 generalize (axiom_20 (iV822576)). zenon_intro zenon_Hc0. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hc0); [ zenon_intro zenon_Hbf; zenon_intro zenon_Hc1 | zenon_intro axiom_151; zenon_intro zenon_Hb7 ]. % 0.19/0.52 exact (zenon_Hc1 zenon_Hb7). % 0.19/0.52 exact (zenon_Hbf axiom_151). % 0.19/0.52 generalize (axiom_141 (iV822576)). zenon_intro zenon_Hc2. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hc2); [ zenon_intro zenon_Hbe; zenon_intro zenon_Hc3 | zenon_intro axiom_153; zenon_intro zenon_Hb8 ]. % 0.19/0.52 exact (zenon_Hc3 zenon_Hb8). % 0.19/0.52 exact (zenon_Hbe axiom_153). % 0.19/0.52 exact (zenon_Hb9 zenon_Hbc). % 0.19/0.52 (* end of lemma zenon_L2_ *) % 0.19/0.52 assert (zenon_L3_ : (exists Y : zenon_U, (ra_Px25 (iV822576) Y)) -> (~(exists Y0 : zenon_U, (ra_Px24 (iV822576) Y0))) -> (~(cC80 (iV822576))) -> False). % 0.19/0.52 do 0 intro. intros zenon_Hc4 zenon_Hc5 zenon_Hc6. % 0.19/0.52 generalize (axiom_117 (iV822576)). zenon_intro zenon_Hc7. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hc7); [ zenon_intro zenon_Hc6; zenon_intro zenon_Hca | zenon_intro zenon_Hc9; zenon_intro zenon_Hc8 ]. % 0.19/0.52 apply (zenon_notand_s _ _ zenon_Hca); [ zenon_intro zenon_Hcc | zenon_intro zenon_Hcb ]. % 0.19/0.52 generalize (axiom_113 (iV822576)). zenon_intro zenon_Hcd. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hcd); [ zenon_intro zenon_Hcc; zenon_intro zenon_Hce | zenon_intro axiom_158; zenon_intro zenon_Hc4 ]. % 0.19/0.52 exact (zenon_Hce zenon_Hc4). % 0.19/0.52 exact (zenon_Hcc axiom_158). % 0.19/0.52 generalize (axiom_110 (iV822576)). zenon_intro zenon_Hcf. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hcf); [ zenon_intro zenon_Hcb; zenon_intro zenon_Hd0 | zenon_intro axiom_152; zenon_intro zenon_Hc5 ]. % 0.19/0.52 exact (zenon_Hd0 zenon_Hc5). % 0.19/0.52 exact (zenon_Hcb axiom_152). % 0.19/0.52 exact (zenon_Hc6 zenon_Hc9). % 0.19/0.52 (* end of lemma zenon_L3_ *) % 0.19/0.52 assert (zenon_L4_ : (~(exists Y0 : zenon_U, (ra_Px39 (iV822576) Y0))) -> (~(exists Y0 : zenon_U, (ra_Px38 (iV822576) Y0))) -> (exists Y : zenon_U, (ra_Px25 (iV822576) Y)) -> (~(exists Y0 : zenon_U, (ra_Px24 (iV822576) Y0))) -> (~(cC116 (iV822576))) -> False). % 0.19/0.52 do 0 intro. intros zenon_Hb7 zenon_Hb8 zenon_Hc4 zenon_Hc5 zenon_Hd1. % 0.19/0.52 generalize (axiom_22 (iV822576)). zenon_intro zenon_Hd2. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hd2); [ zenon_intro zenon_Hd1; zenon_intro zenon_Hd5 | zenon_intro zenon_Hd4; zenon_intro zenon_Hd3 ]. % 0.19/0.52 apply (zenon_notand_s _ _ zenon_Hd5); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hc6 ]. % 0.19/0.52 apply (zenon_L2_); trivial. % 0.19/0.52 apply (zenon_L3_); trivial. % 0.19/0.52 exact (zenon_Hd1 zenon_Hd4). % 0.19/0.52 (* end of lemma zenon_L4_ *) % 0.19/0.52 apply NNPP. intro zenon_G. % 0.19/0.52 generalize (axiom_9 (iV822576)). zenon_intro zenon_Hd6. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hd6); [ zenon_intro zenon_Hd9; zenon_intro zenon_Hd8 | zenon_intro axiom_147; zenon_intro zenon_Hd7 ]. % 0.19/0.52 exact (zenon_Hd9 axiom_147). % 0.19/0.52 generalize (axiom_14 (iV822576)). zenon_intro zenon_Hda. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hda); [ zenon_intro zenon_Hdd; zenon_intro zenon_Hdc | zenon_intro axiom_148; zenon_intro zenon_Hdb ]. % 0.19/0.52 exact (zenon_Hdd axiom_148). % 0.19/0.52 generalize (axiom_75 (iV822576)). zenon_intro zenon_Hb3. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hb3); [ zenon_intro zenon_Hb2; zenon_intro zenon_Hb4 | zenon_intro axiom_149; zenon_intro zenon_Haa ]. % 0.19/0.52 exact (zenon_Hb2 axiom_149). % 0.19/0.52 generalize (axiom_20 (iV822576)). zenon_intro zenon_Hc0. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hc0); [ zenon_intro zenon_Hbf; zenon_intro zenon_Hc1 | zenon_intro axiom_151; zenon_intro zenon_Hb7 ]. % 0.19/0.52 exact (zenon_Hbf axiom_151). % 0.19/0.52 generalize (axiom_110 (iV822576)). zenon_intro zenon_Hcf. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hcf); [ zenon_intro zenon_Hcb; zenon_intro zenon_Hd0 | zenon_intro axiom_152; zenon_intro zenon_Hc5 ]. % 0.19/0.52 exact (zenon_Hcb axiom_152). % 0.19/0.52 generalize (axiom_141 (iV822576)). zenon_intro zenon_Hc2. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hc2); [ zenon_intro zenon_Hbe; zenon_intro zenon_Hc3 | zenon_intro axiom_153; zenon_intro zenon_Hb8 ]. % 0.19/0.52 exact (zenon_Hbe axiom_153). % 0.19/0.52 generalize (axiom_113 (iV822576)). zenon_intro zenon_Hcd. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hcd); [ zenon_intro zenon_Hcc; zenon_intro zenon_Hce | zenon_intro axiom_158; zenon_intro zenon_Hc4 ]. % 0.19/0.52 exact (zenon_Hcc axiom_158). % 0.19/0.52 generalize (axiom_40 (iV822576)). zenon_intro zenon_Hde. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hde); [ zenon_intro zenon_He1; zenon_intro zenon_He0 | zenon_intro axiom_160; zenon_intro zenon_Hdf ]. % 0.19/0.52 exact (zenon_He1 axiom_160). % 0.19/0.52 generalize (axiom_126 (iV822576)). zenon_intro zenon_He2. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_He2); [ zenon_intro zenon_He5; zenon_intro zenon_He4 | zenon_intro axiom_161; zenon_intro zenon_He3 ]. % 0.19/0.52 exact (zenon_He5 axiom_161). % 0.19/0.52 generalize (axiom_71 (iV822576)). zenon_intro zenon_He6. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_He6); [ zenon_intro zenon_He9; zenon_intro zenon_He8 | zenon_intro axiom_162; zenon_intro zenon_He7 ]. % 0.19/0.52 exact (zenon_He9 axiom_162). % 0.19/0.52 generalize (axiom_3 (iV822576)). zenon_intro zenon_Hb5. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hb5); [ zenon_intro zenon_Hb1; zenon_intro zenon_Hb6 | zenon_intro axiom_167; zenon_intro zenon_Hab ]. % 0.19/0.52 exact (zenon_Hb1 axiom_167). % 0.19/0.52 generalize (axiom_135 (iV822576)). zenon_intro zenon_Hea. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hea); [ zenon_intro zenon_Hed; zenon_intro zenon_Hec | zenon_intro axiom_168; zenon_intro zenon_Heb ]. % 0.19/0.52 exact (zenon_Hed axiom_168). % 0.19/0.52 apply (zenon_notand_s _ _ zenon_G); [ zenon_intro zenon_Hef | zenon_intro zenon_Hee ]. % 0.19/0.52 exact (zenon_Hef axiom_0). % 0.19/0.52 apply (zenon_notand_s _ _ zenon_Hee); [ zenon_intro zenon_Hf1 | zenon_intro zenon_Hf0 ]. % 0.19/0.52 exact (zenon_Hf1 axiom_1). % 0.19/0.52 apply (zenon_notand_s _ _ zenon_Hf0); [ zenon_intro zenon_Hf3 | zenon_intro zenon_Hf2 ]. % 0.19/0.52 generalize (axiom_94 (iV822576)). zenon_intro zenon_Hf4. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hf4); [ zenon_intro zenon_Hf3; zenon_intro zenon_Hf7 | zenon_intro zenon_Hf6; zenon_intro zenon_Hf5 ]. % 0.19/0.52 apply (zenon_notand_s _ _ zenon_Hf7); [ zenon_intro zenon_He9 | zenon_intro zenon_Hac ]. % 0.19/0.52 generalize (axiom_71 (iV822576)). zenon_intro zenon_He6. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_He6); [ zenon_intro zenon_He9; zenon_intro zenon_He8 | zenon_intro axiom_162; zenon_intro zenon_He7 ]. % 0.19/0.52 exact (zenon_He8 zenon_He7). % 0.19/0.52 exact (zenon_He9 axiom_162). % 0.19/0.52 apply (zenon_L1_); trivial. % 0.19/0.52 exact (zenon_Hf3 zenon_Hf6). % 0.19/0.52 apply (zenon_notand_s _ _ zenon_Hf2); [ zenon_intro zenon_Hd1 | zenon_intro zenon_Hf8 ]. % 0.19/0.52 apply (zenon_L4_); trivial. % 0.19/0.52 apply (zenon_notand_s _ _ zenon_Hf8); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hf9 ]. % 0.19/0.52 apply (zenon_L2_); trivial. % 0.19/0.52 apply (zenon_notand_s _ _ zenon_Hf9); [ zenon_intro zenon_Hfb | zenon_intro zenon_Hfa ]. % 0.19/0.52 exact (zenon_Hfb axiom_166). % 0.19/0.52 apply (zenon_notand_s _ _ zenon_Hfa); [ zenon_intro zenon_Hfd | zenon_intro zenon_Hfc ]. % 0.19/0.52 generalize (axiom_136 (iV822576)). zenon_intro zenon_Hfe. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hfe); [ zenon_intro zenon_Hfd; zenon_intro zenon_H101 | zenon_intro zenon_H100; zenon_intro zenon_Hff ]. % 0.19/0.52 apply (zenon_notand_s _ _ zenon_H101); [ zenon_intro zenon_He5 | zenon_intro zenon_Hed ]. % 0.19/0.52 generalize (axiom_126 (iV822576)). zenon_intro zenon_He2. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_He2); [ zenon_intro zenon_He5; zenon_intro zenon_He4 | zenon_intro axiom_161; zenon_intro zenon_He3 ]. % 0.19/0.52 exact (zenon_He4 zenon_He3). % 0.19/0.52 exact (zenon_He5 axiom_161). % 0.19/0.52 generalize (axiom_135 (iV822576)). zenon_intro zenon_Hea. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hea); [ zenon_intro zenon_Hed; zenon_intro zenon_Hec | zenon_intro axiom_168; zenon_intro zenon_Heb ]. % 0.19/0.52 exact (zenon_Hec zenon_Heb). % 0.19/0.52 exact (zenon_Hed axiom_168). % 0.19/0.52 exact (zenon_Hfd zenon_H100). % 0.19/0.52 apply (zenon_notand_s _ _ zenon_Hfc); [ zenon_intro zenon_Hc6 | zenon_intro zenon_H102 ]. % 0.19/0.52 apply (zenon_L3_); trivial. % 0.19/0.52 apply (zenon_notand_s _ _ zenon_H102); [ zenon_intro zenon_H104 | zenon_intro zenon_H103 ]. % 0.19/0.52 generalize (axiom_15 (iV822576)). zenon_intro zenon_H105. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_H105); [ zenon_intro zenon_H104; zenon_intro zenon_H108 | zenon_intro zenon_H107; zenon_intro zenon_H106 ]. % 0.19/0.52 apply (zenon_notand_s _ _ zenon_H108); [ zenon_intro zenon_Hd9 | zenon_intro zenon_Hdd ]. % 0.19/0.52 generalize (axiom_9 (iV822576)). zenon_intro zenon_Hd6. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hd6); [ zenon_intro zenon_Hd9; zenon_intro zenon_Hd8 | zenon_intro axiom_147; zenon_intro zenon_Hd7 ]. % 0.19/0.52 exact (zenon_Hd8 zenon_Hd7). % 0.19/0.52 exact (zenon_Hd9 axiom_147). % 0.19/0.52 generalize (axiom_14 (iV822576)). zenon_intro zenon_Hda. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hda); [ zenon_intro zenon_Hdd; zenon_intro zenon_Hdc | zenon_intro axiom_148; zenon_intro zenon_Hdb ]. % 0.19/0.52 exact (zenon_Hdc zenon_Hdb). % 0.19/0.52 exact (zenon_Hdd axiom_148). % 0.19/0.52 exact (zenon_H104 zenon_H107). % 0.19/0.52 apply (zenon_notand_s _ _ zenon_H103); [ zenon_intro zenon_H109 | zenon_intro zenon_Hac ]. % 0.19/0.52 generalize (axiom_42 (iV822576)). zenon_intro zenon_H10a. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_H10a); [ zenon_intro zenon_H109; zenon_intro zenon_H10d | zenon_intro zenon_H10c; zenon_intro zenon_H10b ]. % 0.19/0.52 apply (zenon_notand_s _ _ zenon_H10d); [ zenon_intro zenon_He1 | zenon_intro zenon_Hd1 ]. % 0.19/0.52 generalize (axiom_40 (iV822576)). zenon_intro zenon_Hde. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_Hde); [ zenon_intro zenon_He1; zenon_intro zenon_He0 | zenon_intro axiom_160; zenon_intro zenon_Hdf ]. % 0.19/0.52 exact (zenon_He0 zenon_Hdf). % 0.19/0.52 exact (zenon_He1 axiom_160). % 0.19/0.52 apply (zenon_L4_); trivial. % 0.19/0.52 exact (zenon_H109 zenon_H10c). % 0.19/0.52 apply (zenon_L1_); trivial. % 0.19/0.52 Qed. % 0.19/0.52 % SZS output end Proof % 0.19/0.52 (* END-PROOF *) % 0.19/0.52 nodes searched: 1918 % 0.19/0.52 max branch formulas: 865 % 0.19/0.52 proof nodes created: 77 % 0.19/0.52 formulas created: 7385 % 0.19/0.52 %------------------------------------------------------------------------------