%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : KRS155+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n018.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.39s 0.55s % Output : Proof 0.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : KRS155+1 : TPTP v8.1.0. Released v3.1.0. % 0.04/0.13 % Command : run_zenon %s %d % 0.12/0.34 % Computer : n018.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Tue Jun 7 14:53:51 EDT 2022 % 0.12/0.34 % CPUTime : % 0.39/0.55 (* PROOF-FOUND *) % 0.39/0.55 % SZS status Theorem % 0.39/0.55 (* BEGIN-PROOF *) % 0.39/0.55 % SZS output start Proof % 0.39/0.55 Theorem the_axiom : ((forall X : zenon_U, ((cowlThing X)/\(~(cowlNothing X))))/\((forall X : zenon_U, ((xsd_string X)<->(~(xsd_integer X))))/\((cC20 (iV8467))/\((cC4 (iV8467))/\((cC8 (iV8467))/\((cC82 (iV8467))/\((cC62 (iV8467))/\((cC14 (iV8467))/\((cC34 (iV8467))/\((cC10 (iV8467))/\((cowlThing (iV8467))/\((cC48 (iV8467))/\((cowlThing (iV8471))/\((cC80 (iV8471))/\((cC58 (iV8472))/\((cC60 (iV8472))/\(cowlThing (iV8472)))))))))))))))))). % 0.39/0.55 Proof. % 0.39/0.55 assert (zenon_L1_ : (~(exists Y : zenon_U, ((rR1 (iV8467) Y)/\(cC2xcomp Y)))) -> (~(exists Y0 : zenon_U, (ra_Px3 (iV8473) Y0))) -> False). % 0.39/0.55 do 0 intro. intros zenon_H87 zenon_H88. % 0.39/0.55 apply zenon_H87. exists (iV8473). apply NNPP. zenon_intro zenon_H89. % 0.39/0.55 apply (zenon_notand_s _ _ zenon_H89); [ zenon_intro zenon_H8b | zenon_intro zenon_H8a ]. % 0.39/0.55 exact (zenon_H8b axiom_108). % 0.39/0.55 generalize (axiom_12 (iV8473)). zenon_intro zenon_H8c. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_H8c); [ zenon_intro zenon_H8a; zenon_intro zenon_H8d | zenon_intro axiom_125; zenon_intro zenon_H88 ]. % 0.39/0.55 exact (zenon_H8d zenon_H88). % 0.39/0.55 exact (zenon_H8a axiom_125). % 0.39/0.55 (* end of lemma zenon_L1_ *) % 0.39/0.55 assert (zenon_L2_ : (~(exists Y0 : zenon_U, (ra_Px3 (iV8473) Y0))) -> (~(cC4 (iV8467))) -> False). % 0.39/0.55 do 0 intro. intros zenon_H88 zenon_H8e. % 0.39/0.55 generalize (axiom_35 (iV8467)). zenon_intro zenon_H8f. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_H8f); [ zenon_intro zenon_H8e; zenon_intro zenon_H87 | zenon_intro zenon_H91; zenon_intro zenon_H90 ]. % 0.39/0.55 apply (zenon_L1_); trivial. % 0.39/0.55 exact (zenon_H8e zenon_H91). % 0.39/0.55 (* end of lemma zenon_L2_ *) % 0.39/0.55 assert (zenon_L3_ : (exists Y : zenon_U, (ra_Px28 (iV8469) Y)) -> (~(cC8 (iV8467))) -> False). % 0.39/0.55 do 0 intro. intros zenon_H92 zenon_H93. % 0.39/0.55 generalize (axiom_79 (iV8467)). zenon_intro zenon_H94. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H93; zenon_intro zenon_H97 | zenon_intro zenon_H96; zenon_intro zenon_H95 ]. % 0.39/0.55 apply zenon_H97. exists (iV8469). apply NNPP. zenon_intro zenon_H98. % 0.39/0.55 apply (zenon_notand_s _ _ zenon_H98); [ zenon_intro zenon_H9a | zenon_intro zenon_H99 ]. % 0.39/0.55 exact (zenon_H9a axiom_105). % 0.39/0.55 generalize (axiom_60 (iV8469)). zenon_intro zenon_H9b. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_H9b); [ zenon_intro zenon_H99; zenon_intro zenon_H9c | zenon_intro axiom_113; zenon_intro zenon_H92 ]. % 0.39/0.55 exact (zenon_H9c zenon_H92). % 0.39/0.55 exact (zenon_H99 axiom_113). % 0.39/0.55 exact (zenon_H93 zenon_H96). % 0.39/0.55 (* end of lemma zenon_L3_ *) % 0.39/0.55 assert (zenon_L4_ : (~(exists Y0 : zenon_U, (ra_Px20 (iV8471) Y0))) -> (~(exists Y0 : zenon_U, (ra_Px3 (iV8471) Y0))) -> (~(cC80 (iV8471))) -> False). % 0.39/0.55 do 0 intro. intros zenon_H9d zenon_H9e zenon_H9f. % 0.39/0.55 generalize (axiom_80 (iV8471)). zenon_intro zenon_Ha0. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_Ha0); [ zenon_intro zenon_H9f; zenon_intro zenon_Ha3 | zenon_intro zenon_Ha2; zenon_intro zenon_Ha1 ]. % 0.39/0.55 apply (zenon_notand_s _ _ zenon_Ha3); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Ha4 ]. % 0.39/0.55 generalize (axiom_78 (iV8471)). zenon_intro zenon_Ha6. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_Ha6); [ zenon_intro zenon_Ha5; zenon_intro zenon_Ha7 | zenon_intro axiom_118; zenon_intro zenon_H9d ]. % 0.39/0.55 exact (zenon_Ha7 zenon_H9d). % 0.39/0.55 exact (zenon_Ha5 axiom_118). % 0.39/0.55 generalize (axiom_12 (iV8471)). zenon_intro zenon_Ha8. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_Ha8); [ zenon_intro zenon_Ha4; zenon_intro zenon_Ha9 | zenon_intro axiom_119; zenon_intro zenon_H9e ]. % 0.39/0.55 exact (zenon_Ha9 zenon_H9e). % 0.39/0.55 exact (zenon_Ha4 axiom_119). % 0.39/0.55 exact (zenon_H9f zenon_Ha2). % 0.39/0.55 (* end of lemma zenon_L4_ *) % 0.39/0.55 assert (zenon_L5_ : (~(exists Y0 : zenon_U, (ra_Px3 (iV8472) Y0))) -> (~(cC2xcomp (iV8472))) -> False). % 0.39/0.55 do 0 intro. intros zenon_Haa zenon_Hab. % 0.39/0.55 generalize (axiom_12 (iV8472)). zenon_intro zenon_Hac. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_Hac); [ zenon_intro zenon_Hab; zenon_intro zenon_Had | zenon_intro axiom_122; zenon_intro zenon_Haa ]. % 0.39/0.55 exact (zenon_Had zenon_Haa). % 0.39/0.55 exact (zenon_Hab axiom_122). % 0.39/0.55 (* end of lemma zenon_L5_ *) % 0.39/0.55 assert (zenon_L6_ : (exists Y0 : zenon_U, (ra_Px3 (iV8476) Y0)) -> (~(cC2 (iV8476))) -> False). % 0.39/0.55 do 0 intro. intros zenon_Hae zenon_Haf. % 0.39/0.55 generalize (axiom_11 (iV8476)). zenon_intro zenon_Hb0. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_Hb0); [ zenon_intro zenon_Haf; zenon_intro zenon_Hb1 | zenon_intro axiom_132; zenon_intro zenon_Hae ]. % 0.39/0.55 exact (zenon_Hb1 zenon_Hae). % 0.39/0.55 exact (zenon_Haf axiom_132). % 0.39/0.55 (* end of lemma zenon_L6_ *) % 0.39/0.55 assert (zenon_L7_ : (exists Y0 : zenon_U, (ra_Px3 (iV8476) Y0)) -> (~(cC58 (iV8472))) -> False). % 0.39/0.55 do 0 intro. intros zenon_Hae zenon_Hb2. % 0.39/0.55 generalize (axiom_57 (iV8472)). zenon_intro zenon_Hb3. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_Hb3); [ zenon_intro zenon_Hb2; zenon_intro zenon_Hb6 | zenon_intro zenon_Hb5; zenon_intro zenon_Hb4 ]. % 0.39/0.55 apply zenon_Hb6. exists (iV8476). apply NNPP. zenon_intro zenon_Hb7. % 0.39/0.55 apply (zenon_notand_s _ _ zenon_Hb7); [ zenon_intro zenon_Hb8 | zenon_intro zenon_Haf ]. % 0.39/0.55 exact (zenon_Hb8 axiom_124). % 0.39/0.55 apply (zenon_L6_); trivial. % 0.39/0.55 exact (zenon_Hb2 zenon_Hb5). % 0.39/0.55 (* end of lemma zenon_L7_ *) % 0.39/0.55 assert (zenon_L8_ : (~(exists Y0 : zenon_U, (ra_Px3 (iV8472) Y0))) -> (exists Y0 : zenon_U, (ra_Px3 (iV8476) Y0)) -> (~(cC60 (iV8472))) -> False). % 0.39/0.55 do 0 intro. intros zenon_Haa zenon_Hae zenon_Hb9. % 0.39/0.55 generalize (axiom_61 (iV8472)). zenon_intro zenon_Hba. % 0.39/0.55 apply (zenon_equiv_s _ _ zenon_Hba); [ zenon_intro zenon_Hb9; zenon_intro zenon_Hbd | zenon_intro zenon_Hbc; zenon_intro zenon_Hbb ]. % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Hbd); [ zenon_intro zenon_Hab | zenon_intro zenon_Hb2 ]. % 0.39/0.56 apply (zenon_L5_); trivial. % 0.39/0.56 apply (zenon_L7_); trivial. % 0.39/0.56 exact (zenon_Hb9 zenon_Hbc). % 0.39/0.56 (* end of lemma zenon_L8_ *) % 0.39/0.56 apply NNPP. intro zenon_G. % 0.39/0.56 generalize (axiom_60 (iV8469)). zenon_intro zenon_H9b. % 0.39/0.56 apply (zenon_equiv_s _ _ zenon_H9b); [ zenon_intro zenon_H99; zenon_intro zenon_H9c | zenon_intro axiom_113; zenon_intro zenon_H92 ]. % 0.39/0.56 exact (zenon_H99 axiom_113). % 0.39/0.56 generalize (axiom_78 (iV8471)). zenon_intro zenon_Ha6. % 0.39/0.56 apply (zenon_equiv_s _ _ zenon_Ha6); [ zenon_intro zenon_Ha5; zenon_intro zenon_Ha7 | zenon_intro axiom_118; zenon_intro zenon_H9d ]. % 0.39/0.56 exact (zenon_Ha5 axiom_118). % 0.39/0.56 generalize (axiom_12 (iV8471)). zenon_intro zenon_Ha8. % 0.39/0.56 apply (zenon_equiv_s _ _ zenon_Ha8); [ zenon_intro zenon_Ha4; zenon_intro zenon_Ha9 | zenon_intro axiom_119; zenon_intro zenon_H9e ]. % 0.39/0.56 exact (zenon_Ha4 axiom_119). % 0.39/0.56 generalize (axiom_12 (iV8472)). zenon_intro zenon_Hac. % 0.39/0.56 apply (zenon_equiv_s _ _ zenon_Hac); [ zenon_intro zenon_Hab; zenon_intro zenon_Had | zenon_intro axiom_122; zenon_intro zenon_Haa ]. % 0.39/0.56 exact (zenon_Hab axiom_122). % 0.39/0.56 generalize (axiom_12 (iV8473)). zenon_intro zenon_H8c. % 0.39/0.56 apply (zenon_equiv_s _ _ zenon_H8c); [ zenon_intro zenon_H8a; zenon_intro zenon_H8d | zenon_intro axiom_125; zenon_intro zenon_H88 ]. % 0.39/0.56 exact (zenon_H8a axiom_125). % 0.39/0.56 generalize (axiom_27 (iV8474)). zenon_intro zenon_Hbe. % 0.39/0.56 apply (zenon_equiv_s _ _ zenon_Hbe); [ zenon_intro zenon_Hc1; zenon_intro zenon_Hc0 | zenon_intro axiom_127; zenon_intro zenon_Hbf ]. % 0.39/0.56 exact (zenon_Hc1 axiom_127). % 0.39/0.56 generalize (axiom_11 (iV8476)). zenon_intro zenon_Hb0. % 0.39/0.56 apply (zenon_equiv_s _ _ zenon_Hb0); [ zenon_intro zenon_Haf; zenon_intro zenon_Hb1 | zenon_intro axiom_132; zenon_intro zenon_Hae ]. % 0.39/0.56 exact (zenon_Haf axiom_132). % 0.39/0.56 apply (zenon_notand_s _ _ zenon_G); [ zenon_intro zenon_Hc3 | zenon_intro zenon_Hc2 ]. % 0.39/0.56 exact (zenon_Hc3 axiom_0). % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Hc2); [ zenon_intro zenon_Hc5 | zenon_intro zenon_Hc4 ]. % 0.39/0.56 exact (zenon_Hc5 axiom_1). % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Hc4); [ zenon_intro zenon_Hc7 | zenon_intro zenon_Hc6 ]. % 0.39/0.56 generalize (axiom_13 (iV8467)). zenon_intro zenon_Hc8. % 0.39/0.56 apply (zenon_equiv_s _ _ zenon_Hc8); [ zenon_intro zenon_Hc7; zenon_intro zenon_H87 | zenon_intro zenon_Hc9; zenon_intro zenon_H90 ]. % 0.39/0.56 apply (zenon_L1_); trivial. % 0.39/0.56 exact (zenon_Hc7 zenon_Hc9). % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Hc6); [ zenon_intro zenon_H8e | zenon_intro zenon_Hca ]. % 0.39/0.56 apply (zenon_L2_); trivial. % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Hca); [ zenon_intro zenon_H93 | zenon_intro zenon_Hcb ]. % 0.39/0.56 apply (zenon_L3_); trivial. % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Hcb); [ zenon_intro zenon_Hcd | zenon_intro zenon_Hcc ]. % 0.39/0.56 generalize (axiom_82 (iV8467)). zenon_intro zenon_Hce. % 0.39/0.56 apply (zenon_equiv_s _ _ zenon_Hce); [ zenon_intro zenon_Hcd; zenon_intro zenon_Hd1 | zenon_intro zenon_Hd0; zenon_intro zenon_Hcf ]. % 0.39/0.56 apply zenon_Hd1. exists (iV8471). apply NNPP. zenon_intro zenon_Hd2. % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Hd2); [ zenon_intro zenon_Hd3 | zenon_intro zenon_H9f ]. % 0.39/0.56 exact (zenon_Hd3 axiom_103). % 0.39/0.56 apply (zenon_L4_); trivial. % 0.39/0.56 exact (zenon_Hcd zenon_Hd0). % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Hcc); [ zenon_intro zenon_Hd5 | zenon_intro zenon_Hd4 ]. % 0.39/0.56 generalize (axiom_62 (iV8467)). zenon_intro zenon_Hd6. % 0.39/0.56 apply (zenon_equiv_s _ _ zenon_Hd6); [ zenon_intro zenon_Hd5; zenon_intro zenon_Hd9 | zenon_intro zenon_Hd8; zenon_intro zenon_Hd7 ]. % 0.39/0.56 apply zenon_Hd9. exists (iV8472). apply NNPP. zenon_intro zenon_Hda. % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Hda); [ zenon_intro zenon_Hdb | zenon_intro zenon_Hb9 ]. % 0.39/0.56 exact (zenon_Hdb axiom_110). % 0.39/0.56 apply (zenon_L8_); trivial. % 0.39/0.56 exact (zenon_Hd5 zenon_Hd8). % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Hd4); [ zenon_intro zenon_Hdd | zenon_intro zenon_Hdc ]. % 0.39/0.56 generalize (axiom_5 (iV8467)). zenon_intro zenon_Hde. % 0.39/0.56 apply (zenon_equiv_s _ _ zenon_Hde); [ zenon_intro zenon_Hdd; zenon_intro zenon_He1 | zenon_intro zenon_He0; zenon_intro zenon_Hdf ]. % 0.39/0.56 apply zenon_He1. exists (iV8470). apply NNPP. zenon_intro zenon_He2. % 0.39/0.56 apply (zenon_notand_s _ _ zenon_He2); [ zenon_intro zenon_He4 | zenon_intro zenon_He3 ]. % 0.39/0.56 exact (zenon_He4 axiom_104). % 0.39/0.56 exact (zenon_He3 axiom_116). % 0.39/0.56 exact (zenon_Hdd zenon_He0). % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Hdc); [ zenon_intro zenon_He6 | zenon_intro zenon_He5 ]. % 0.39/0.56 generalize (axiom_29 (iV8467)). zenon_intro zenon_He7. % 0.39/0.56 apply (zenon_equiv_s _ _ zenon_He7); [ zenon_intro zenon_He6; zenon_intro zenon_Hea | zenon_intro zenon_He9; zenon_intro zenon_He8 ]. % 0.39/0.56 apply zenon_Hea. exists (iV8474). apply NNPP. zenon_intro zenon_Heb. % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Heb); [ zenon_intro zenon_Hec | zenon_intro zenon_Hc1 ]. % 0.39/0.56 exact (zenon_Hec axiom_106). % 0.39/0.56 generalize (axiom_27 (iV8474)). zenon_intro zenon_Hbe. % 0.39/0.56 apply (zenon_equiv_s _ _ zenon_Hbe); [ zenon_intro zenon_Hc1; zenon_intro zenon_Hc0 | zenon_intro axiom_127; zenon_intro zenon_Hbf ]. % 0.39/0.56 exact (zenon_Hc0 zenon_Hbf). % 0.39/0.56 exact (zenon_Hc1 axiom_127). % 0.39/0.56 exact (zenon_He6 zenon_He9). % 0.39/0.56 apply (zenon_notand_s _ _ zenon_He5); [ zenon_intro zenon_Hee | zenon_intro zenon_Hed ]. % 0.39/0.56 generalize (axiom_2 (iV8467)). zenon_intro zenon_Hef. % 0.39/0.56 apply (zenon_equiv_s _ _ zenon_Hef); [ zenon_intro zenon_Hee; zenon_intro zenon_Hf2 | zenon_intro zenon_Hf1; zenon_intro zenon_Hf0 ]. % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Hf2); [ zenon_intro zenon_H8e | zenon_intro zenon_H93 ]. % 0.39/0.56 apply (zenon_L2_); trivial. % 0.39/0.56 apply (zenon_L3_); trivial. % 0.39/0.56 exact (zenon_Hee zenon_Hf1). % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Hed); [ zenon_intro zenon_Hf4 | zenon_intro zenon_Hf3 ]. % 0.39/0.56 exact (zenon_Hf4 axiom_102). % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Hf3); [ zenon_intro zenon_Hf6 | zenon_intro zenon_Hf5 ]. % 0.39/0.56 generalize (axiom_44 (iV8467)). zenon_intro zenon_Hf7. % 0.39/0.56 apply (zenon_equiv_s _ _ zenon_Hf7); [ zenon_intro zenon_Hf6; zenon_intro zenon_H87 | zenon_intro zenon_Hf8; zenon_intro zenon_H90 ]. % 0.39/0.56 apply (zenon_L1_); trivial. % 0.39/0.56 exact (zenon_Hf6 zenon_Hf8). % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Hf5); [ zenon_intro zenon_Hfa | zenon_intro zenon_Hf9 ]. % 0.39/0.56 exact (zenon_Hfa axiom_120). % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Hf9); [ zenon_intro zenon_H9f | zenon_intro zenon_Hfb ]. % 0.39/0.56 apply (zenon_L4_); trivial. % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Hfb); [ zenon_intro zenon_Hb2 | zenon_intro zenon_Hfc ]. % 0.39/0.56 apply (zenon_L7_); trivial. % 0.39/0.56 apply (zenon_notand_s _ _ zenon_Hfc); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hfd ]. % 0.39/0.56 apply (zenon_L8_); trivial. % 0.39/0.56 exact (zenon_Hfd axiom_123). % 0.39/0.56 Qed. % 0.39/0.56 % SZS output end Proof % 0.39/0.56 (* END-PROOF *) % 0.39/0.56 nodes searched: 2956 % 0.39/0.56 max branch formulas: 615 % 0.39/0.56 proof nodes created: 124 % 0.39/0.56 formulas created: 7681 % 0.39/0.56 %------------------------------------------------------------------------------