%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : KRS151+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n024.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.41s 0.60s % Output : Proof 0.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KRS151+1 : TPTP v8.1.0. Released v3.1.0. % 0.03/0.13 % Command : run_zenon %s %d % 0.12/0.35 % Computer : n024.cluster.edu % 0.12/0.35 % Model : x86_64 x86_64 % 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.35 % Memory : 8042.1875MB % 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.35 % CPULimit : 300 % 0.12/0.35 % WCLimit : 600 % 0.12/0.35 % DateTime : Tue Jun 7 14:32:19 EDT 2022 % 0.12/0.35 % CPUTime : % 0.41/0.60 (* PROOF-FOUND *) % 0.41/0.60 % SZS status Theorem % 0.41/0.60 (* BEGIN-PROOF *) % 0.41/0.60 % SZS output start Proof % 0.41/0.60 Theorem the_axiom : ((forall X : zenon_U, ((cowlThing X)/\(~(cowlNothing X))))/\((forall X : zenon_U, ((xsd_string X)<->(~(xsd_integer X))))/\((cowlThing (iV21026))/\((cC84 (iV21026))/\((cC16 (iV21026))/\((cC36 (iV21026))/\((cC42 (iV21026))/\((cC88 (iV21026))/\((cC86 (iV21026))/\((cC174 (iV21026))/\((cC20 (iV21026))/\((cC156 (iV21026))/\((cC60 (iV21026))/\((cC38 (iV21026))/\((cC158 (iV21026))/\((cC10 (iV21026))/\((cC134 (iV21026))/\((cC22 (iV21026))/\((cC168 (iV21026))/\((cC56 (iV21026))/\((cC78 (iV21026))/\((cC58 (iV21026))/\((cC152 (iV21026))/\((cC40 (iV21026))/\((cC132 (iV21026))/\((cC130 (iV21026))/\((cC62 (iV21026))/\((cC154 (iV21026))/\((cC80 (iV21026))/\((cC8 (iV21026))/\((cC136 (iV21026))/\((cC112 (iV21026))/\((cC180 (iV21026))/\((cC114 (iV21026))/\((cC64 (iV21026))/\((cC110 (iV21026))/\((cC116 (iV21026))/\((cC82 (iV21026))/\((cC138 (iV21026))/\((cC4 (iV21026))/\((cC108 (iV21026))/\((cC14 (iV21026))/\((cC90 (iV21026))/\((cowlThing (iV21027))/\((cC30 (iV21027))/\((cC24 (iV21027))/\((cowlThing (iV21029))/\((cC50 (iV21029))/\((cC44 (iV21029))/\((cowlThing (iV21030))/\((cC66 (iV21030))/\(cC72 (iV21030))))))))))))))))))))))))))))))))))))))))))))))))))))). % 0.41/0.60 Proof. % 0.41/0.60 assert (zenon_L1_ : (~(~(cC18 (iV21030)))) -> False). % 0.41/0.60 do 0 intro. intros zenon_Hf3. % 0.41/0.60 exact (zenon_Hf3 axiom_202). % 0.41/0.60 (* end of lemma zenon_L1_ *) % 0.41/0.60 assert (zenon_L2_ : (~(~(cC12 (iV21029)))) -> False). % 0.41/0.60 do 0 intro. intros zenon_Hf4. % 0.41/0.60 exact (zenon_Hf4 axiom_163). % 0.41/0.60 (* end of lemma zenon_L2_ *) % 0.41/0.60 assert (zenon_L3_ : (~(~(cC2 (iV21027)))) -> False). % 0.41/0.60 do 0 intro. intros zenon_Hf5. % 0.41/0.60 exact (zenon_Hf5 axiom_150). % 0.41/0.60 (* end of lemma zenon_L3_ *) % 0.41/0.60 assert (zenon_L4_ : (~((forall X : zenon_U, ((cowlThing X)/\(~(cowlNothing X))))/\((forall X : zenon_U, ((xsd_string X)<->(~(xsd_integer X))))/\((cowlThing (iV21026))/\((cC84 (iV21026))/\((cC16 (iV21026))/\((cC36 (iV21026))/\((cC42 (iV21026))/\((cC88 (iV21026))/\((cC86 (iV21026))/\((cC174 (iV21026))/\((cC20 (iV21026))/\((cC156 (iV21026))/\((cC60 (iV21026))/\((cC38 (iV21026))/\((cC158 (iV21026))/\((cC10 (iV21026))/\((cC134 (iV21026))/\((cC22 (iV21026))/\((cC168 (iV21026))/\((cC56 (iV21026))/\((cC78 (iV21026))/\((cC58 (iV21026))/\((cC152 (iV21026))/\((cC40 (iV21026))/\((cC132 (iV21026))/\((cC130 (iV21026))/\((cC62 (iV21026))/\((cC154 (iV21026))/\((cC80 (iV21026))/\((cC8 (iV21026))/\((cC136 (iV21026))/\((cC112 (iV21026))/\((cC180 (iV21026))/\((cC114 (iV21026))/\((cC64 (iV21026))/\((cC110 (iV21026))/\((cC116 (iV21026))/\((cC82 (iV21026))/\((cC138 (iV21026))/\((cC4 (iV21026))/\((cC108 (iV21026))/\((cC14 (iV21026))/\((cC90 (iV21026))/\((cowlThing (iV21027))/\((cC30 (iV21027))/\((cC24 (iV21027))/\((cowlThing (iV21029))/\((cC50 (iV21029))/\((cC44 (iV21029))/\((cowlThing (iV21030))/\((cC66 (iV21030))/\(cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) -> ((cC14 (iV21026))/\(cC10 (iV21026))) -> ((~(cC28 (iV21026)))/\(~(cC34 (iV21026)))) -> ((cC40 (iV21026))/\(cC38 (iV21026))) -> ((cC82 (iV21026))/\(cC84 (iV21026))) -> ((cC168 (iV21026))/\(~(cC172 (iV21026)))) -> (exists Y : zenon_U, ((rR1 (iV21026) Y)/\(~(cC18 Y)))) -> ((cC154 (iV21026))/\(cC138 (iV21026))) -> ((cC58 (iV21026))/\(cC42 (iV21026))) -> ((cC36 (iV21026))/\(cTOP (iV21026))) -> ((cC22 (iV21026))/\(cC156 (iV21026))) -> ((cC8 (iV21026))/\(cC4 (iV21026))) -> ((cC132 (iV21026))/\(cC116 (iV21026))) -> ((cC16 (iV21026))/\(cC20 (iV21026))) -> ((~(cC166 (iV21026)))/\(~(cC162 (iV21026)))) -> ((~(cC48 (iV21026)))/\(~(cC54 (iV21026)))) -> ((~(cC70 (iV21026)))/\(~(cC76 (iV21026)))) -> ((cC56 (iV21026))/\(cTOP (iV21026))) -> ((~(cC150 (iV21026)))/\(~(cC144 (iV21026)))) -> ((cTOP (iV21026))/\(cC130 (iV21026))) -> ((~(cC122 (iV21026)))/\(~(cC128 (iV21026)))) -> ((cTOP (iV21026))/\(cC152 (iV21026))) -> ((cTOP (iV21026))/\(cC78 (iV21026))) -> (exists Y : zenon_U, ((rR1 (iV21026) Y)/\(~(cC6 Y)))) -> ((cC90 (iV21026))/\(cC110 (iV21026))) -> ((~(cC178 (iV21026)))/\(cC174 (iV21026))) -> ((cC62 (iV21026))/\(cC60 (iV21026))) -> ((cC108 (iV21026))/\(cTOP (iV21026))) -> ((cC114 (iV21026))/\(cC112 (iV21026))) -> ((cC80 (iV21026))/\(cC64 (iV21026))) -> ((cC136 (iV21026))/\(cC134 (iV21026))) -> (exists Y : zenon_U, ((rR1 (iV21026) Y)/\(~(cC2 Y)))) -> ((~(cC106 (iV21026)))/\(~(cC98 (iV21026)))) -> (exists Y : zenon_U, ((rR1 (iV21026) Y)/\(~(cC12 Y)))) -> ((cC88 (iV21026))/\(cC86 (iV21026))) -> (exists Y : zenon_U, ((rR1 (iV21027) Y)/\(~(cC12 Y)))) -> (exists Y : zenon_U, ((rR1 (iV21027) Y)/\(~(cC2 Y)))) -> (exists Y : zenon_U, ((rR1 (iV21029) Y)/\(~(cC12 Y)))) -> (exists Y : zenon_U, ((rR1 (iV21029) Y)/\(~(cC2 Y)))) -> (exists Y : zenon_U, ((rR1 (iV21030) Y)/\(~(cC2 Y)))) -> (exists Y : zenon_U, ((rR1 (iV21030) Y)/\(~(cC12 Y)))) -> False). % 0.41/0.60 do 0 intro. intros zenon_G zenon_Hf6 zenon_Hf7 zenon_Hf8 zenon_Hf9 zenon_Hfa zenon_Hfb zenon_Hfc zenon_Hfd zenon_Hfe zenon_Hff zenon_H100 zenon_H101 zenon_H102 zenon_H103 zenon_H104 zenon_H105 zenon_H106 zenon_H107 zenon_H108 zenon_H109 zenon_H10a zenon_H10b zenon_H10c zenon_H10d zenon_H10e zenon_H10f zenon_H110 zenon_H111 zenon_H112 zenon_H113 zenon_H114 zenon_H115 zenon_H116 zenon_H117 zenon_H118 zenon_H119 zenon_H11a zenon_H11b zenon_H11c zenon_H11d. % 0.41/0.60 apply (zenon_notand_s _ _ zenon_G); [ zenon_intro zenon_H11f | zenon_intro zenon_H11e ]. % 0.41/0.60 exact (zenon_H11f axiom_0). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H11e); [ zenon_intro zenon_H121 | zenon_intro zenon_H120 ]. % 0.41/0.60 exact (zenon_H121 axiom_1). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H120); [ zenon_intro zenon_H123 | zenon_intro zenon_H122 ]. % 0.41/0.60 exact (zenon_H123 axiom_120). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H122); [ zenon_intro zenon_H125 | zenon_intro zenon_H124 ]. % 0.41/0.60 generalize (axiom_79 (iV21026)). zenon_intro zenon_H126. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H126); [ zenon_intro zenon_H125; zenon_intro zenon_H128 | zenon_intro zenon_H127; zenon_intro axiom_88 ]. % 0.41/0.60 exact (zenon_H128 axiom_88). % 0.41/0.60 exact (zenon_H125 zenon_H127). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H124); [ zenon_intro zenon_H12a | zenon_intro zenon_H129 ]. % 0.41/0.60 generalize (axiom_33 (iV21026)). zenon_intro zenon_H12b. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H12b); [ zenon_intro zenon_H12a; zenon_intro zenon_H12d | zenon_intro zenon_H12c; zenon_intro zenon_Hf6 ]. % 0.41/0.60 exact (zenon_H12d zenon_Hf6). % 0.41/0.60 exact (zenon_H12a zenon_H12c). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H129); [ zenon_intro zenon_H12f | zenon_intro zenon_H12e ]. % 0.41/0.60 generalize (axiom_53 (iV21026)). zenon_intro zenon_H130. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H130); [ zenon_intro zenon_H12f; zenon_intro zenon_H132 | zenon_intro zenon_H131; zenon_intro zenon_Hf7 ]. % 0.41/0.60 exact (zenon_H132 zenon_Hf7). % 0.41/0.60 exact (zenon_H12f zenon_H131). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H12e); [ zenon_intro zenon_H134 | zenon_intro zenon_H133 ]. % 0.41/0.60 generalize (axiom_57 (iV21026)). zenon_intro zenon_H135. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H135); [ zenon_intro zenon_H134; zenon_intro zenon_H137 | zenon_intro zenon_H136; zenon_intro zenon_Hf8 ]. % 0.41/0.60 exact (zenon_H137 zenon_Hf8). % 0.41/0.60 exact (zenon_H134 zenon_H136). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H133); [ zenon_intro zenon_H139 | zenon_intro zenon_H138 ]. % 0.41/0.60 generalize (axiom_81 (iV21026)). zenon_intro zenon_H13a. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H13a); [ zenon_intro zenon_H139; zenon_intro zenon_H128 | zenon_intro zenon_H13b; zenon_intro axiom_88 ]. % 0.41/0.60 exact (zenon_H128 axiom_88). % 0.41/0.60 exact (zenon_H139 zenon_H13b). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H138); [ zenon_intro zenon_H13d | zenon_intro zenon_H13c ]. % 0.41/0.60 generalize (axiom_80 (iV21026)). zenon_intro zenon_H13e. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H13e); [ zenon_intro zenon_H13d; zenon_intro zenon_H140 | zenon_intro zenon_H13f; zenon_intro zenon_Hf9 ]. % 0.41/0.60 exact (zenon_H140 zenon_Hf9). % 0.41/0.60 exact (zenon_H13d zenon_H13f). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H13c); [ zenon_intro zenon_H142 | zenon_intro zenon_H141 ]. % 0.41/0.60 generalize (axiom_41 (iV21026)). zenon_intro zenon_H143. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H143); [ zenon_intro zenon_H142; zenon_intro zenon_H145 | zenon_intro zenon_H144; zenon_intro zenon_Hfa ]. % 0.41/0.60 exact (zenon_H145 zenon_Hfa). % 0.41/0.60 exact (zenon_H142 zenon_H144). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H141); [ zenon_intro zenon_H147 | zenon_intro zenon_H146 ]. % 0.41/0.60 generalize (axiom_45 (iV21026)). zenon_intro zenon_H148. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H148); [ zenon_intro zenon_H147; zenon_intro zenon_H14a | zenon_intro zenon_H149; zenon_intro zenon_Hfb ]. % 0.41/0.60 exact (zenon_H14a zenon_Hfb). % 0.41/0.60 exact (zenon_H147 zenon_H149). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H146); [ zenon_intro zenon_H14c | zenon_intro zenon_H14b ]. % 0.41/0.60 generalize (axiom_31 (iV21026)). zenon_intro zenon_H14d. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H14d); [ zenon_intro zenon_H14c; zenon_intro zenon_H14f | zenon_intro zenon_H14e; zenon_intro zenon_Hfc ]. % 0.41/0.60 exact (zenon_H14f zenon_Hfc). % 0.41/0.60 exact (zenon_H14c zenon_H14e). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H14b); [ zenon_intro zenon_H151 | zenon_intro zenon_H150 ]. % 0.41/0.60 generalize (axiom_66 (iV21026)). zenon_intro zenon_H152. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H152); [ zenon_intro zenon_H151; zenon_intro zenon_H154 | zenon_intro zenon_H153; zenon_intro zenon_Hfd ]. % 0.41/0.60 exact (zenon_H154 zenon_Hfd). % 0.41/0.60 exact (zenon_H151 zenon_H153). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H150); [ zenon_intro zenon_H156 | zenon_intro zenon_H155 ]. % 0.41/0.60 generalize (axiom_54 (iV21026)). zenon_intro zenon_H157. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H157); [ zenon_intro zenon_H156; zenon_intro zenon_H159 | zenon_intro zenon_H158; zenon_intro zenon_Hfe ]. % 0.41/0.60 exact (zenon_H159 zenon_Hfe). % 0.41/0.60 exact (zenon_H156 zenon_H158). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H155); [ zenon_intro zenon_H15b | zenon_intro zenon_H15a ]. % 0.41/0.60 generalize (axiom_32 (iV21026)). zenon_intro zenon_H15c. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H15c); [ zenon_intro zenon_H15b; zenon_intro zenon_H15e | zenon_intro zenon_H15d; zenon_intro zenon_Hff ]. % 0.41/0.60 exact (zenon_H15e zenon_Hff). % 0.41/0.60 exact (zenon_H15b zenon_H15d). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H15a); [ zenon_intro zenon_H160 | zenon_intro zenon_H15f ]. % 0.41/0.60 generalize (axiom_2 (iV21026)). zenon_intro zenon_H161. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H161); [ zenon_intro zenon_H160; zenon_intro zenon_H163 | zenon_intro zenon_H162; zenon_intro zenon_H100 ]. % 0.41/0.60 exact (zenon_H163 zenon_H100). % 0.41/0.60 exact (zenon_H160 zenon_H162). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H15f); [ zenon_intro zenon_H165 | zenon_intro zenon_H164 ]. % 0.41/0.60 generalize (axiom_19 (iV21026)). zenon_intro zenon_H166. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H166); [ zenon_intro zenon_H165; zenon_intro zenon_H168 | zenon_intro zenon_H167; zenon_intro zenon_H101 ]. % 0.41/0.60 exact (zenon_H168 zenon_H101). % 0.41/0.60 exact (zenon_H165 zenon_H167). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H164); [ zenon_intro zenon_H16a | zenon_intro zenon_H169 ]. % 0.41/0.60 generalize (axiom_46 (iV21026)). zenon_intro zenon_H16b. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H16b); [ zenon_intro zenon_H16a; zenon_intro zenon_H16d | zenon_intro zenon_H16c; zenon_intro zenon_H102 ]. % 0.41/0.60 exact (zenon_H16d zenon_H102). % 0.41/0.60 exact (zenon_H16a zenon_H16c). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H169); [ zenon_intro zenon_H16f | zenon_intro zenon_H16e ]. % 0.41/0.60 generalize (axiom_38 (iV21026)). zenon_intro zenon_H170. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H170); [ zenon_intro zenon_H16f; zenon_intro zenon_H172 | zenon_intro zenon_H171; zenon_intro zenon_H103 ]. % 0.41/0.60 exact (zenon_H172 zenon_H103). % 0.41/0.60 exact (zenon_H16f zenon_H171). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H16e); [ zenon_intro zenon_H174 | zenon_intro zenon_H173 ]. % 0.41/0.60 generalize (axiom_64 (iV21026)). zenon_intro zenon_H175. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H175); [ zenon_intro zenon_H174; zenon_intro zenon_H177 | zenon_intro zenon_H176; zenon_intro zenon_H104 ]. % 0.41/0.60 exact (zenon_H177 zenon_H104). % 0.41/0.60 exact (zenon_H174 zenon_H176). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H173); [ zenon_intro zenon_H179 | zenon_intro zenon_H178 ]. % 0.41/0.60 generalize (axiom_75 (iV21026)). zenon_intro zenon_H17a. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H17a); [ zenon_intro zenon_H179; zenon_intro zenon_H17c | zenon_intro zenon_H17b; zenon_intro zenon_H105 ]. % 0.41/0.60 exact (zenon_H17c zenon_H105). % 0.41/0.60 exact (zenon_H179 zenon_H17b). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H178); [ zenon_intro zenon_H17e | zenon_intro zenon_H17d ]. % 0.41/0.60 generalize (axiom_65 (iV21026)). zenon_intro zenon_H17f. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H17f); [ zenon_intro zenon_H17e; zenon_intro zenon_H181 | zenon_intro zenon_H180; zenon_intro zenon_H106 ]. % 0.41/0.60 exact (zenon_H181 zenon_H106). % 0.41/0.60 exact (zenon_H17e zenon_H180). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H17d); [ zenon_intro zenon_H183 | zenon_intro zenon_H182 ]. % 0.41/0.60 generalize (axiom_29 (iV21026)). zenon_intro zenon_H184. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H184); [ zenon_intro zenon_H183; zenon_intro zenon_H186 | zenon_intro zenon_H185; zenon_intro zenon_H107 ]. % 0.41/0.60 exact (zenon_H186 zenon_H107). % 0.41/0.60 exact (zenon_H183 zenon_H185). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H182); [ zenon_intro zenon_H188 | zenon_intro zenon_H187 ]. % 0.41/0.60 generalize (axiom_56 (iV21026)). zenon_intro zenon_H189. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H189); [ zenon_intro zenon_H188; zenon_intro zenon_H128 | zenon_intro zenon_H18a; zenon_intro axiom_88 ]. % 0.41/0.60 exact (zenon_H128 axiom_88). % 0.41/0.60 exact (zenon_H188 zenon_H18a). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H187); [ zenon_intro zenon_H18c | zenon_intro zenon_H18b ]. % 0.41/0.60 generalize (axiom_18 (iV21026)). zenon_intro zenon_H18d. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H18d); [ zenon_intro zenon_H18c; zenon_intro zenon_H18f | zenon_intro zenon_H18e; zenon_intro zenon_H108 ]. % 0.41/0.60 exact (zenon_H18f zenon_H108). % 0.41/0.60 exact (zenon_H18c zenon_H18e). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H18b); [ zenon_intro zenon_H191 | zenon_intro zenon_H190 ]. % 0.41/0.60 generalize (axiom_17 (iV21026)). zenon_intro zenon_H192. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H192); [ zenon_intro zenon_H191; zenon_intro zenon_H194 | zenon_intro zenon_H193; zenon_intro zenon_H109 ]. % 0.41/0.60 exact (zenon_H194 zenon_H109). % 0.41/0.60 exact (zenon_H191 zenon_H193). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H190); [ zenon_intro zenon_H196 | zenon_intro zenon_H195 ]. % 0.41/0.60 generalize (axiom_67 (iV21026)). zenon_intro zenon_H197. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H197); [ zenon_intro zenon_H196; zenon_intro zenon_H128 | zenon_intro zenon_H198; zenon_intro axiom_88 ]. % 0.41/0.60 exact (zenon_H128 axiom_88). % 0.41/0.60 exact (zenon_H196 zenon_H198). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H195); [ zenon_intro zenon_H19a | zenon_intro zenon_H199 ]. % 0.41/0.60 generalize (axiom_30 (iV21026)). zenon_intro zenon_H19b. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H19b); [ zenon_intro zenon_H19a; zenon_intro zenon_H19d | zenon_intro zenon_H19c; zenon_intro zenon_H10a ]. % 0.41/0.60 exact (zenon_H19d zenon_H10a). % 0.41/0.60 exact (zenon_H19a zenon_H19c). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H199); [ zenon_intro zenon_H19f | zenon_intro zenon_H19e ]. % 0.41/0.60 generalize (axiom_77 (iV21026)). zenon_intro zenon_H1a0. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1a0); [ zenon_intro zenon_H19f; zenon_intro zenon_H1a2 | zenon_intro zenon_H1a1; zenon_intro zenon_H10b ]. % 0.41/0.60 exact (zenon_H1a2 zenon_H10b). % 0.41/0.60 exact (zenon_H19f zenon_H1a1). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H19e); [ zenon_intro zenon_H1a4 | zenon_intro zenon_H1a3 ]. % 0.41/0.60 generalize (axiom_76 (iV21026)). zenon_intro zenon_H1a5. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1a5); [ zenon_intro zenon_H1a4; zenon_intro zenon_H1a7 | zenon_intro zenon_H1a6; zenon_intro zenon_H10c ]. % 0.41/0.60 exact (zenon_H1a7 zenon_H10c). % 0.41/0.60 exact (zenon_H1a4 zenon_H1a6). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1a3); [ zenon_intro zenon_H1a9 | zenon_intro zenon_H1a8 ]. % 0.41/0.60 generalize (axiom_20 (iV21026)). zenon_intro zenon_H1aa. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1aa); [ zenon_intro zenon_H1a9; zenon_intro zenon_H128 | zenon_intro zenon_H1ab; zenon_intro axiom_88 ]. % 0.41/0.60 exact (zenon_H128 axiom_88). % 0.41/0.60 exact (zenon_H1a9 zenon_H1ab). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1a8); [ zenon_intro zenon_H1ad | zenon_intro zenon_H1ac ]. % 0.41/0.60 generalize (axiom_8 (iV21026)). zenon_intro zenon_H1ae. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1ae); [ zenon_intro zenon_H1ad; zenon_intro zenon_H1b0 | zenon_intro zenon_H1af; zenon_intro zenon_H10d ]. % 0.41/0.60 exact (zenon_H1b0 zenon_H10d). % 0.41/0.60 exact (zenon_H1ad zenon_H1af). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1ac); [ zenon_intro zenon_H1b2 | zenon_intro zenon_H1b1 ]. % 0.41/0.60 generalize (axiom_44 (iV21026)). zenon_intro zenon_H1b3. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1b3); [ zenon_intro zenon_H1b2; zenon_intro zenon_H1b5 | zenon_intro zenon_H1b4; zenon_intro zenon_H10e ]. % 0.41/0.60 exact (zenon_H1b5 zenon_H10e). % 0.41/0.60 exact (zenon_H1b2 zenon_H1b4). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1b1); [ zenon_intro zenon_H1b7 | zenon_intro zenon_H1b6 ]. % 0.41/0.60 generalize (axiom_9 (iV21026)). zenon_intro zenon_H1b8. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1b8); [ zenon_intro zenon_H1b7; zenon_intro zenon_H128 | zenon_intro zenon_H1b9; zenon_intro axiom_88 ]. % 0.41/0.60 exact (zenon_H128 axiom_88). % 0.41/0.60 exact (zenon_H1b7 zenon_H1b9). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1b6); [ zenon_intro zenon_H1bb | zenon_intro zenon_H1ba ]. % 0.41/0.60 generalize (axiom_68 (iV21026)). zenon_intro zenon_H1bc. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1bc); [ zenon_intro zenon_H1bb; zenon_intro zenon_H1be | zenon_intro zenon_H1bd; zenon_intro zenon_H10f ]. % 0.41/0.60 exact (zenon_H1be zenon_H10f). % 0.41/0.60 exact (zenon_H1bb zenon_H1bd). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1ba); [ zenon_intro zenon_H1c0 | zenon_intro zenon_H1bf ]. % 0.41/0.60 generalize (axiom_7 (iV21026)). zenon_intro zenon_H1c1. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1c1); [ zenon_intro zenon_H1c0; zenon_intro zenon_H1c3 | zenon_intro zenon_H1c2; zenon_intro zenon_H110 ]. % 0.41/0.60 exact (zenon_H1c3 zenon_H110). % 0.41/0.60 exact (zenon_H1c0 zenon_H1c2). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1bf); [ zenon_intro zenon_H1c5 | zenon_intro zenon_H1c4 ]. % 0.41/0.60 generalize (axiom_10 (iV21026)). zenon_intro zenon_H1c6. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1c6); [ zenon_intro zenon_H1c5; zenon_intro zenon_H1c8 | zenon_intro zenon_H1c7; zenon_intro zenon_H111 ]. % 0.41/0.60 exact (zenon_H1c8 zenon_H111). % 0.41/0.60 exact (zenon_H1c5 zenon_H1c7). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1c4); [ zenon_intro zenon_H1ca | zenon_intro zenon_H1c9 ]. % 0.41/0.60 generalize (axiom_78 (iV21026)). zenon_intro zenon_H1cb. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1cb); [ zenon_intro zenon_H1ca; zenon_intro zenon_H1cd | zenon_intro zenon_H1cc; zenon_intro zenon_H112 ]. % 0.41/0.60 exact (zenon_H1cd zenon_H112). % 0.41/0.60 exact (zenon_H1ca zenon_H1cc). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1c9); [ zenon_intro zenon_H1cf | zenon_intro zenon_H1ce ]. % 0.41/0.60 generalize (axiom_21 (iV21026)). zenon_intro zenon_H1d0. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1d0); [ zenon_intro zenon_H1cf; zenon_intro zenon_H1d2 | zenon_intro zenon_H1d1; zenon_intro zenon_H113 ]. % 0.41/0.60 exact (zenon_H1d2 zenon_H113). % 0.41/0.60 exact (zenon_H1cf zenon_H1d1). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1ce); [ zenon_intro zenon_H1d4 | zenon_intro zenon_H1d3 ]. % 0.41/0.60 generalize (axiom_55 (iV21026)). zenon_intro zenon_H1d5. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1d5); [ zenon_intro zenon_H1d4; zenon_intro zenon_H1d7 | zenon_intro zenon_H1d6; zenon_intro zenon_H114 ]. % 0.41/0.60 exact (zenon_H1d7 zenon_H114). % 0.41/0.60 exact (zenon_H1d4 zenon_H1d6). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1d3); [ zenon_intro zenon_H1d9 | zenon_intro zenon_H1d8 ]. % 0.41/0.60 generalize (axiom_6 (iV21026)). zenon_intro zenon_H1da. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1da); [ zenon_intro zenon_H1d9; zenon_intro zenon_H1dc | zenon_intro zenon_H1db; zenon_intro zenon_H115 ]. % 0.41/0.60 exact (zenon_H1dc zenon_H115). % 0.41/0.60 exact (zenon_H1d9 zenon_H1db). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1d8); [ zenon_intro zenon_H1de | zenon_intro zenon_H1dd ]. % 0.41/0.60 generalize (axiom_22 (iV21026)). zenon_intro zenon_H1df. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1df); [ zenon_intro zenon_H1de; zenon_intro zenon_H1e1 | zenon_intro zenon_H1e0; zenon_intro zenon_H116 ]. % 0.41/0.60 exact (zenon_H1e1 zenon_H116). % 0.41/0.60 exact (zenon_H1de zenon_H1e0). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1dd); [ zenon_intro zenon_H1e3 | zenon_intro zenon_H1e2 ]. % 0.41/0.60 generalize (axiom_82 (iV21026)). zenon_intro zenon_H1e4. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1e4); [ zenon_intro zenon_H1e3; zenon_intro zenon_H1e6 | zenon_intro zenon_H1e5; zenon_intro zenon_H117 ]. % 0.41/0.60 exact (zenon_H1e6 zenon_H117). % 0.41/0.60 exact (zenon_H1e3 zenon_H1e5). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1e2); [ zenon_intro zenon_H1e8 | zenon_intro zenon_H1e7 ]. % 0.41/0.60 exact (zenon_H1e8 axiom_151). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1e7); [ zenon_intro zenon_H1ea | zenon_intro zenon_H1e9 ]. % 0.41/0.60 generalize (axiom_50 (iV21027)). zenon_intro zenon_H1eb. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1eb); [ zenon_intro zenon_H1ea; zenon_intro zenon_H1ed | zenon_intro zenon_H1ec; zenon_intro zenon_H118 ]. % 0.41/0.60 exact (zenon_H1ed zenon_H118). % 0.41/0.60 exact (zenon_H1ea zenon_H1ec). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1e9); [ zenon_intro zenon_H1ef | zenon_intro zenon_H1ee ]. % 0.41/0.60 generalize (axiom_47 (iV21027)). zenon_intro zenon_H1f0. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1f0); [ zenon_intro zenon_H1ef; zenon_intro zenon_H1f2 | zenon_intro zenon_H1f1; zenon_intro zenon_H119 ]. % 0.41/0.60 exact (zenon_H1f2 zenon_H119). % 0.41/0.60 exact (zenon_H1ef zenon_H1f1). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1ee); [ zenon_intro zenon_H1f4 | zenon_intro zenon_H1f3 ]. % 0.41/0.60 exact (zenon_H1f4 axiom_180). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1f3); [ zenon_intro zenon_H1f6 | zenon_intro zenon_H1f5 ]. % 0.41/0.60 generalize (axiom_61 (iV21029)). zenon_intro zenon_H1f7. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1f7); [ zenon_intro zenon_H1f6; zenon_intro zenon_H1f9 | zenon_intro zenon_H1f8; zenon_intro zenon_H11a ]. % 0.41/0.60 exact (zenon_H1f9 zenon_H11a). % 0.41/0.60 exact (zenon_H1f6 zenon_H1f8). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1f5); [ zenon_intro zenon_H1fb | zenon_intro zenon_H1fa ]. % 0.41/0.60 generalize (axiom_58 (iV21029)). zenon_intro zenon_H1fc. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1fc); [ zenon_intro zenon_H1fb; zenon_intro zenon_H1fe | zenon_intro zenon_H1fd; zenon_intro zenon_H11b ]. % 0.41/0.60 exact (zenon_H1fe zenon_H11b). % 0.41/0.60 exact (zenon_H1fb zenon_H1fd). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1fa); [ zenon_intro zenon_H200 | zenon_intro zenon_H1ff ]. % 0.41/0.60 exact (zenon_H200 axiom_207). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H1ff); [ zenon_intro zenon_H202 | zenon_intro zenon_H201 ]. % 0.41/0.60 generalize (axiom_69 (iV21030)). zenon_intro zenon_H203. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H203); [ zenon_intro zenon_H202; zenon_intro zenon_H205 | zenon_intro zenon_H204; zenon_intro zenon_H11c ]. % 0.41/0.60 exact (zenon_H205 zenon_H11c). % 0.41/0.60 exact (zenon_H202 zenon_H204). % 0.41/0.60 generalize (axiom_72 (iV21030)). zenon_intro zenon_H206. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H206); [ zenon_intro zenon_H201; zenon_intro zenon_H208 | zenon_intro zenon_H207; zenon_intro zenon_H11d ]. % 0.41/0.60 exact (zenon_H208 zenon_H11d). % 0.41/0.60 exact (zenon_H201 zenon_H207). % 0.41/0.60 (* end of lemma zenon_L4_ *) % 0.41/0.60 assert (zenon_L5_ : (~((~(cC66 (iV21030)))/\(~(cC18 (iV21030))))) -> (~((~(cC12 (iV21029)))/\(~(cC44 (iV21029))))) -> (~((~(cC24 (iV21027)))/\(~(cC2 (iV21027))))) -> ((cC14 (iV21026))/\(cC10 (iV21026))) -> ((~(cC28 (iV21026)))/\(~(cC34 (iV21026)))) -> ((cC40 (iV21026))/\(cC38 (iV21026))) -> ((cC82 (iV21026))/\(cC84 (iV21026))) -> ((cC168 (iV21026))/\(~(cC172 (iV21026)))) -> (exists Y : zenon_U, ((rR1 (iV21026) Y)/\(~(cC18 Y)))) -> ((cC154 (iV21026))/\(cC138 (iV21026))) -> ((cC58 (iV21026))/\(cC42 (iV21026))) -> ((cC36 (iV21026))/\(cTOP (iV21026))) -> ((cC22 (iV21026))/\(cC156 (iV21026))) -> ((cC8 (iV21026))/\(cC4 (iV21026))) -> ((cC132 (iV21026))/\(cC116 (iV21026))) -> ((cC16 (iV21026))/\(cC20 (iV21026))) -> ((~(cC166 (iV21026)))/\(~(cC162 (iV21026)))) -> ((~(cC48 (iV21026)))/\(~(cC54 (iV21026)))) -> ((~(cC70 (iV21026)))/\(~(cC76 (iV21026)))) -> ((cC56 (iV21026))/\(cTOP (iV21026))) -> ((~(cC150 (iV21026)))/\(~(cC144 (iV21026)))) -> ((cTOP (iV21026))/\(cC130 (iV21026))) -> ((~(cC122 (iV21026)))/\(~(cC128 (iV21026)))) -> ((cTOP (iV21026))/\(cC152 (iV21026))) -> ((cTOP (iV21026))/\(cC78 (iV21026))) -> (exists Y : zenon_U, ((rR1 (iV21026) Y)/\(~(cC6 Y)))) -> ((cC90 (iV21026))/\(cC110 (iV21026))) -> ((~(cC178 (iV21026)))/\(cC174 (iV21026))) -> ((cC62 (iV21026))/\(cC60 (iV21026))) -> ((cC108 (iV21026))/\(cTOP (iV21026))) -> ((cC114 (iV21026))/\(cC112 (iV21026))) -> ((cC80 (iV21026))/\(cC64 (iV21026))) -> ((cC136 (iV21026))/\(cC134 (iV21026))) -> (exists Y : zenon_U, ((rR1 (iV21026) Y)/\(~(cC2 Y)))) -> ((~(cC106 (iV21026)))/\(~(cC98 (iV21026)))) -> (exists Y : zenon_U, ((rR1 (iV21026) Y)/\(~(cC12 Y)))) -> ((cC88 (iV21026))/\(cC86 (iV21026))) -> (exists Y : zenon_U, ((rR1 (iV21030) Y)/\(~(cC12 Y)))) -> (~((forall X : zenon_U, ((cowlThing X)/\(~(cowlNothing X))))/\((forall X : zenon_U, ((xsd_string X)<->(~(xsd_integer X))))/\((cowlThing (iV21026))/\((cC84 (iV21026))/\((cC16 (iV21026))/\((cC36 (iV21026))/\((cC42 (iV21026))/\((cC88 (iV21026))/\((cC86 (iV21026))/\((cC174 (iV21026))/\((cC20 (iV21026))/\((cC156 (iV21026))/\((cC60 (iV21026))/\((cC38 (iV21026))/\((cC158 (iV21026))/\((cC10 (iV21026))/\((cC134 (iV21026))/\((cC22 (iV21026))/\((cC168 (iV21026))/\((cC56 (iV21026))/\((cC78 (iV21026))/\((cC58 (iV21026))/\((cC152 (iV21026))/\((cC40 (iV21026))/\((cC132 (iV21026))/\((cC130 (iV21026))/\((cC62 (iV21026))/\((cC154 (iV21026))/\((cC80 (iV21026))/\((cC8 (iV21026))/\((cC136 (iV21026))/\((cC112 (iV21026))/\((cC180 (iV21026))/\((cC114 (iV21026))/\((cC64 (iV21026))/\((cC110 (iV21026))/\((cC116 (iV21026))/\((cC82 (iV21026))/\((cC138 (iV21026))/\((cC4 (iV21026))/\((cC108 (iV21026))/\((cC14 (iV21026))/\((cC90 (iV21026))/\((cowlThing (iV21027))/\((cC30 (iV21027))/\((cC24 (iV21027))/\((cowlThing (iV21029))/\((cC50 (iV21029))/\((cC44 (iV21029))/\((cowlThing (iV21030))/\((cC66 (iV21030))/\(cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) -> (~((~(cC2 (iV21027)))/\(~(cC30 (iV21027))))) -> (~((~(cC12 (iV21029)))/\(~(cC50 (iV21029))))) -> False). % 0.41/0.60 do 0 intro. intros zenon_H209 zenon_H20a zenon_H20b zenon_Hf6 zenon_Hf7 zenon_Hf8 zenon_Hf9 zenon_Hfa zenon_Hfb zenon_Hfc zenon_Hfd zenon_Hfe zenon_Hff zenon_H100 zenon_H101 zenon_H102 zenon_H103 zenon_H104 zenon_H105 zenon_H106 zenon_H107 zenon_H108 zenon_H109 zenon_H10a zenon_H10b zenon_H10c zenon_H10d zenon_H10e zenon_H10f zenon_H110 zenon_H111 zenon_H112 zenon_H113 zenon_H114 zenon_H115 zenon_H116 zenon_H117 zenon_H11d zenon_G zenon_H20c zenon_H20d. % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H209); [ zenon_intro zenon_H20e | zenon_intro zenon_Hf3 ]. % 0.41/0.60 apply zenon_H20e. zenon_intro zenon_H204. % 0.41/0.60 generalize (axiom_69 (iV21030)). zenon_intro zenon_H203. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H203); [ zenon_intro zenon_H202; zenon_intro zenon_H205 | zenon_intro zenon_H204; zenon_intro zenon_H11c ]. % 0.41/0.60 exact (zenon_H202 zenon_H204). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H20d); [ zenon_intro zenon_Hf4 | zenon_intro zenon_H20f ]. % 0.41/0.60 exact (zenon_Hf4 axiom_163). % 0.41/0.60 apply zenon_H20f. zenon_intro zenon_H1f8. % 0.41/0.60 generalize (axiom_61 (iV21029)). zenon_intro zenon_H1f7. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1f7); [ zenon_intro zenon_H1f6; zenon_intro zenon_H1f9 | zenon_intro zenon_H1f8; zenon_intro zenon_H11a ]. % 0.41/0.60 exact (zenon_H1f6 zenon_H1f8). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H20a); [ zenon_intro zenon_Hf4 | zenon_intro zenon_H210 ]. % 0.41/0.60 exact (zenon_Hf4 axiom_163). % 0.41/0.60 apply zenon_H210. zenon_intro zenon_H1fd. % 0.41/0.60 generalize (axiom_58 (iV21029)). zenon_intro zenon_H1fc. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1fc); [ zenon_intro zenon_H1fb; zenon_intro zenon_H1fe | zenon_intro zenon_H1fd; zenon_intro zenon_H11b ]. % 0.41/0.60 exact (zenon_H1fb zenon_H1fd). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H20c); [ zenon_intro zenon_Hf5 | zenon_intro zenon_H211 ]. % 0.41/0.60 exact (zenon_Hf5 axiom_150). % 0.41/0.60 apply zenon_H211. zenon_intro zenon_H1ec. % 0.41/0.60 generalize (axiom_50 (iV21027)). zenon_intro zenon_H1eb. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1eb); [ zenon_intro zenon_H1ea; zenon_intro zenon_H1ed | zenon_intro zenon_H1ec; zenon_intro zenon_H118 ]. % 0.41/0.60 exact (zenon_H1ea zenon_H1ec). % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H20b); [ zenon_intro zenon_H212 | zenon_intro zenon_Hf5 ]. % 0.41/0.60 apply zenon_H212. zenon_intro zenon_H1f1. % 0.41/0.60 generalize (axiom_47 (iV21027)). zenon_intro zenon_H1f0. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1f0); [ zenon_intro zenon_H1ef; zenon_intro zenon_H1f2 | zenon_intro zenon_H1f1; zenon_intro zenon_H119 ]. % 0.41/0.60 exact (zenon_H1ef zenon_H1f1). % 0.41/0.60 apply (zenon_L4_); trivial. % 0.41/0.60 exact (zenon_Hf5 axiom_150). % 0.41/0.60 exact (zenon_Hf3 axiom_202). % 0.41/0.60 (* end of lemma zenon_L5_ *) % 0.41/0.60 apply NNPP. intro zenon_G. % 0.41/0.60 generalize (axiom_86 (iV21026)). zenon_intro zenon_H213. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H213); [ zenon_intro zenon_H216; zenon_intro zenon_H215 | zenon_intro axiom_89; zenon_intro zenon_H214 ]. % 0.41/0.60 exact (zenon_H216 axiom_89). % 0.41/0.60 apply (zenon_and_s _ _ zenon_H214). zenon_intro zenon_H15d. zenon_intro zenon_H1b4. % 0.41/0.60 generalize (axiom_32 (iV21026)). zenon_intro zenon_H15c. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H15c); [ zenon_intro zenon_H15b; zenon_intro zenon_H15e | zenon_intro zenon_H15d; zenon_intro zenon_Hff ]. % 0.41/0.60 exact (zenon_H15b zenon_H15d). % 0.41/0.60 apply (zenon_and_s _ _ zenon_Hff). zenon_intro zenon_H16c. zenon_intro zenon_H14e. % 0.41/0.60 generalize (axiom_46 (iV21026)). zenon_intro zenon_H16b. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H16b); [ zenon_intro zenon_H16a; zenon_intro zenon_H16d | zenon_intro zenon_H16c; zenon_intro zenon_H102 ]. % 0.41/0.60 exact (zenon_H16a zenon_H16c). % 0.41/0.60 apply (zenon_and_s _ _ zenon_H102). zenon_intro zenon_H12c. zenon_intro zenon_H149. % 0.41/0.60 generalize (axiom_33 (iV21026)). zenon_intro zenon_H12b. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H12b); [ zenon_intro zenon_H12a; zenon_intro zenon_H12d | zenon_intro zenon_H12c; zenon_intro zenon_Hf6 ]. % 0.41/0.60 exact (zenon_H12a zenon_H12c). % 0.41/0.60 apply (zenon_and_s _ _ zenon_Hf6). zenon_intro zenon_H1e0. zenon_intro zenon_H162. % 0.41/0.60 generalize (axiom_22 (iV21026)). zenon_intro zenon_H1df. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1df); [ zenon_intro zenon_H1de; zenon_intro zenon_H1e1 | zenon_intro zenon_H1e0; zenon_intro zenon_H116 ]. % 0.41/0.60 exact (zenon_H1de zenon_H1e0). % 0.41/0.60 generalize (axiom_2 (iV21026)). zenon_intro zenon_H161. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H161); [ zenon_intro zenon_H160; zenon_intro zenon_H163 | zenon_intro zenon_H162; zenon_intro zenon_H100 ]. % 0.41/0.60 exact (zenon_H160 zenon_H162). % 0.41/0.60 apply (zenon_and_s _ _ zenon_H100). zenon_intro zenon_H1a6. zenon_intro zenon_H1d6. % 0.41/0.60 generalize (axiom_76 (iV21026)). zenon_intro zenon_H1a5. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1a5); [ zenon_intro zenon_H1a4; zenon_intro zenon_H1a7 | zenon_intro zenon_H1a6; zenon_intro zenon_H10c ]. % 0.41/0.60 exact (zenon_H1a4 zenon_H1a6). % 0.41/0.60 generalize (axiom_55 (iV21026)). zenon_intro zenon_H1d5. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1d5); [ zenon_intro zenon_H1d4; zenon_intro zenon_H1d7 | zenon_intro zenon_H1d6; zenon_intro zenon_H114 ]. % 0.41/0.60 exact (zenon_H1d4 zenon_H1d6). % 0.41/0.60 generalize (axiom_45 (iV21026)). zenon_intro zenon_H148. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H148); [ zenon_intro zenon_H147; zenon_intro zenon_H14a | zenon_intro zenon_H149; zenon_intro zenon_Hfb ]. % 0.41/0.60 exact (zenon_H147 zenon_H149). % 0.41/0.60 generalize (axiom_31 (iV21026)). zenon_intro zenon_H14d. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H14d); [ zenon_intro zenon_H14c; zenon_intro zenon_H14f | zenon_intro zenon_H14e; zenon_intro zenon_Hfc ]. % 0.41/0.60 exact (zenon_H14c zenon_H14e). % 0.41/0.60 apply (zenon_and_s _ _ zenon_Hfc). zenon_intro zenon_H19c. zenon_intro zenon_H1d1. % 0.41/0.60 generalize (axiom_30 (iV21026)). zenon_intro zenon_H19b. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H19b); [ zenon_intro zenon_H19a; zenon_intro zenon_H19d | zenon_intro zenon_H19c; zenon_intro zenon_H10a ]. % 0.41/0.60 exact (zenon_H19a zenon_H19c). % 0.41/0.60 apply (zenon_and_s _ _ zenon_H10a). zenon_intro axiom_88. zenon_intro zenon_H185. % 0.41/0.60 generalize (axiom_29 (iV21026)). zenon_intro zenon_H184. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H184); [ zenon_intro zenon_H183; zenon_intro zenon_H186 | zenon_intro zenon_H185; zenon_intro zenon_H107 ]. % 0.41/0.60 exact (zenon_H183 zenon_H185). % 0.41/0.60 generalize (axiom_21 (iV21026)). zenon_intro zenon_H1d0. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1d0); [ zenon_intro zenon_H1cf; zenon_intro zenon_H1d2 | zenon_intro zenon_H1d1; zenon_intro zenon_H113 ]. % 0.41/0.60 exact (zenon_H1cf zenon_H1d1). % 0.41/0.60 apply (zenon_and_s _ _ zenon_H113). zenon_intro zenon_H1ab. zenon_intro zenon_H167. % 0.41/0.60 generalize (axiom_19 (iV21026)). zenon_intro zenon_H166. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H166); [ zenon_intro zenon_H165; zenon_intro zenon_H168 | zenon_intro zenon_H167; zenon_intro zenon_H101 ]. % 0.41/0.60 exact (zenon_H165 zenon_H167). % 0.41/0.60 apply (zenon_and_s _ _ zenon_H101). zenon_intro zenon_H18e. zenon_intro zenon_H1c7. % 0.41/0.60 generalize (axiom_18 (iV21026)). zenon_intro zenon_H18d. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H18d); [ zenon_intro zenon_H18c; zenon_intro zenon_H18f | zenon_intro zenon_H18e; zenon_intro zenon_H108 ]. % 0.41/0.60 exact (zenon_H18c zenon_H18e). % 0.41/0.60 apply (zenon_and_s _ _ zenon_H108). zenon_intro axiom_88. zenon_intro zenon_H193. % 0.41/0.60 generalize (axiom_17 (iV21026)). zenon_intro zenon_H192. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H192); [ zenon_intro zenon_H191; zenon_intro zenon_H194 | zenon_intro zenon_H193; zenon_intro zenon_H109 ]. % 0.41/0.60 exact (zenon_H191 zenon_H193). % 0.41/0.60 generalize (axiom_10 (iV21026)). zenon_intro zenon_H1c6. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1c6); [ zenon_intro zenon_H1c5; zenon_intro zenon_H1c8 | zenon_intro zenon_H1c7; zenon_intro zenon_H111 ]. % 0.41/0.60 exact (zenon_H1c5 zenon_H1c7). % 0.41/0.60 apply (zenon_and_s _ _ zenon_H111). zenon_intro zenon_H1b9. zenon_intro zenon_H1af. % 0.41/0.60 generalize (axiom_8 (iV21026)). zenon_intro zenon_H1ae. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1ae); [ zenon_intro zenon_H1ad; zenon_intro zenon_H1b0 | zenon_intro zenon_H1af; zenon_intro zenon_H10d ]. % 0.41/0.60 exact (zenon_H1ad zenon_H1af). % 0.41/0.60 apply (zenon_and_s _ _ zenon_H10d). zenon_intro zenon_H1e5. zenon_intro zenon_H1c2. % 0.41/0.60 generalize (axiom_82 (iV21026)). zenon_intro zenon_H1e4. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1e4); [ zenon_intro zenon_H1e3; zenon_intro zenon_H1e6 | zenon_intro zenon_H1e5; zenon_intro zenon_H117 ]. % 0.41/0.60 exact (zenon_H1e3 zenon_H1e5). % 0.41/0.60 apply (zenon_and_s _ _ zenon_H117). zenon_intro zenon_H13b. zenon_intro zenon_H13f. % 0.41/0.60 generalize (axiom_80 (iV21026)). zenon_intro zenon_H13e. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H13e); [ zenon_intro zenon_H13d; zenon_intro zenon_H140 | zenon_intro zenon_H13f; zenon_intro zenon_Hf9 ]. % 0.41/0.60 exact (zenon_H13d zenon_H13f). % 0.41/0.60 apply (zenon_and_s _ _ zenon_Hf9). zenon_intro zenon_H1cc. zenon_intro zenon_H127. % 0.41/0.60 generalize (axiom_78 (iV21026)). zenon_intro zenon_H1cb. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1cb); [ zenon_intro zenon_H1ca; zenon_intro zenon_H1cd | zenon_intro zenon_H1cc; zenon_intro zenon_H112 ]. % 0.41/0.60 exact (zenon_H1ca zenon_H1cc). % 0.41/0.60 apply (zenon_and_s _ _ zenon_H112). zenon_intro zenon_H1a1. zenon_intro zenon_H1bd. % 0.41/0.60 generalize (axiom_77 (iV21026)). zenon_intro zenon_H1a0. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1a0); [ zenon_intro zenon_H19f; zenon_intro zenon_H1a2 | zenon_intro zenon_H1a1; zenon_intro zenon_H10b ]. % 0.41/0.60 exact (zenon_H19f zenon_H1a1). % 0.41/0.60 apply (zenon_and_s _ _ zenon_H10b). zenon_intro axiom_88. zenon_intro zenon_H17b. % 0.41/0.60 generalize (axiom_75 (iV21026)). zenon_intro zenon_H17a. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H17a); [ zenon_intro zenon_H179; zenon_intro zenon_H17c | zenon_intro zenon_H17b; zenon_intro zenon_H105 ]. % 0.41/0.60 exact (zenon_H179 zenon_H17b). % 0.41/0.60 generalize (axiom_68 (iV21026)). zenon_intro zenon_H1bc. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1bc); [ zenon_intro zenon_H1bb; zenon_intro zenon_H1be | zenon_intro zenon_H1bd; zenon_intro zenon_H10f ]. % 0.41/0.60 exact (zenon_H1bb zenon_H1bd). % 0.41/0.60 apply (zenon_and_s _ _ zenon_H10f). zenon_intro zenon_H198. zenon_intro zenon_H153. % 0.41/0.60 generalize (axiom_66 (iV21026)). zenon_intro zenon_H152. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H152); [ zenon_intro zenon_H151; zenon_intro zenon_H154 | zenon_intro zenon_H153; zenon_intro zenon_Hfd ]. % 0.41/0.60 exact (zenon_H151 zenon_H153). % 0.41/0.60 apply (zenon_and_s _ _ zenon_Hfd). zenon_intro zenon_H180. zenon_intro zenon_H136. % 0.41/0.60 generalize (axiom_65 (iV21026)). zenon_intro zenon_H17f. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H17f); [ zenon_intro zenon_H17e; zenon_intro zenon_H181 | zenon_intro zenon_H180; zenon_intro zenon_H106 ]. % 0.41/0.60 exact (zenon_H17e zenon_H180). % 0.41/0.60 apply (zenon_and_s _ _ zenon_H106). zenon_intro zenon_H176. zenon_intro axiom_88. % 0.41/0.60 generalize (axiom_64 (iV21026)). zenon_intro zenon_H175. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H175); [ zenon_intro zenon_H174; zenon_intro zenon_H177 | zenon_intro zenon_H176; zenon_intro zenon_H104 ]. % 0.41/0.60 exact (zenon_H174 zenon_H176). % 0.41/0.60 generalize (axiom_57 (iV21026)). zenon_intro zenon_H135. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H135); [ zenon_intro zenon_H134; zenon_intro zenon_H137 | zenon_intro zenon_H136; zenon_intro zenon_Hf8 ]. % 0.41/0.60 exact (zenon_H134 zenon_H136). % 0.41/0.60 apply (zenon_and_s _ _ zenon_Hf8). zenon_intro zenon_H18a. zenon_intro zenon_H158. % 0.41/0.60 generalize (axiom_54 (iV21026)). zenon_intro zenon_H157. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H157); [ zenon_intro zenon_H156; zenon_intro zenon_H159 | zenon_intro zenon_H158; zenon_intro zenon_Hfe ]. % 0.41/0.60 exact (zenon_H156 zenon_H158). % 0.41/0.60 apply (zenon_and_s _ _ zenon_Hfe). zenon_intro zenon_H131. zenon_intro axiom_88. % 0.41/0.60 generalize (axiom_53 (iV21026)). zenon_intro zenon_H130. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H130); [ zenon_intro zenon_H12f; zenon_intro zenon_H132 | zenon_intro zenon_H131; zenon_intro zenon_Hf7 ]. % 0.41/0.60 exact (zenon_H12f zenon_H131). % 0.41/0.60 generalize (axiom_7 (iV21026)). zenon_intro zenon_H1c1. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1c1); [ zenon_intro zenon_H1c0; zenon_intro zenon_H1c3 | zenon_intro zenon_H1c2; zenon_intro zenon_H110 ]. % 0.41/0.60 exact (zenon_H1c0 zenon_H1c2). % 0.41/0.60 apply (zenon_and_s _ _ zenon_H110). zenon_intro zenon_H1db. zenon_intro axiom_88. % 0.41/0.60 generalize (axiom_6 (iV21026)). zenon_intro zenon_H1da. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1da); [ zenon_intro zenon_H1d9; zenon_intro zenon_H1dc | zenon_intro zenon_H1db; zenon_intro zenon_H115 ]. % 0.41/0.60 exact (zenon_H1d9 zenon_H1db). % 0.41/0.60 generalize (axiom_44 (iV21026)). zenon_intro zenon_H1b3. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H1b3); [ zenon_intro zenon_H1b2; zenon_intro zenon_H1b5 | zenon_intro zenon_H1b4; zenon_intro zenon_H10e ]. % 0.41/0.60 exact (zenon_H1b2 zenon_H1b4). % 0.41/0.60 apply (zenon_and_s _ _ zenon_H10e). zenon_intro axiom_99. zenon_intro zenon_H144. % 0.41/0.60 generalize (axiom_41 (iV21026)). zenon_intro zenon_H143. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H143); [ zenon_intro zenon_H142; zenon_intro zenon_H145 | zenon_intro zenon_H144; zenon_intro zenon_Hfa ]. % 0.41/0.60 exact (zenon_H142 zenon_H144). % 0.41/0.60 apply (zenon_and_s _ _ zenon_Hfa). zenon_intro zenon_H171. zenon_intro axiom_116. % 0.41/0.60 generalize (axiom_38 (iV21026)). zenon_intro zenon_H170. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H170); [ zenon_intro zenon_H16f; zenon_intro zenon_H172 | zenon_intro zenon_H171; zenon_intro zenon_H103 ]. % 0.41/0.60 exact (zenon_H16f zenon_H171). % 0.41/0.60 generalize (axiom_48 (iV21027)). zenon_intro zenon_H217. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H217); [ zenon_intro axiom_126; zenon_intro zenon_H20b | zenon_intro zenon_H219; zenon_intro zenon_H218 ]. % 0.41/0.60 generalize (axiom_51 (iV21027)). zenon_intro zenon_H21a. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H21a); [ zenon_intro axiom_136; zenon_intro zenon_H20c | zenon_intro zenon_H21c; zenon_intro zenon_H21b ]. % 0.41/0.60 generalize (axiom_59 (iV21029)). zenon_intro zenon_H21d. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H21d); [ zenon_intro axiom_157; zenon_intro zenon_H20a | zenon_intro zenon_H21f; zenon_intro zenon_H21e ]. % 0.41/0.60 generalize (axiom_62 (iV21029)). zenon_intro zenon_H220. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H220); [ zenon_intro axiom_168; zenon_intro zenon_H20d | zenon_intro zenon_H222; zenon_intro zenon_H221 ]. % 0.41/0.60 generalize (axiom_70 (iV21030)). zenon_intro zenon_H223. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H223); [ zenon_intro axiom_191; zenon_intro zenon_H209 | zenon_intro zenon_H225; zenon_intro zenon_H224 ]. % 0.41/0.60 generalize (axiom_73 (iV21030)). zenon_intro zenon_H226. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H226); [ zenon_intro axiom_192; zenon_intro zenon_H229 | zenon_intro zenon_H228; zenon_intro zenon_H227 ]. % 0.41/0.60 apply (zenon_notand_s _ _ zenon_H229); [ zenon_intro zenon_Hf3 | zenon_intro zenon_H22a ]. % 0.41/0.60 exact (zenon_Hf3 axiom_202). % 0.41/0.60 apply zenon_H22a. zenon_intro zenon_H207. % 0.41/0.60 generalize (axiom_72 (iV21030)). zenon_intro zenon_H206. % 0.41/0.60 apply (zenon_equiv_s _ _ zenon_H206); [ zenon_intro zenon_H201; zenon_intro zenon_H208 | zenon_intro zenon_H207; zenon_intro zenon_H11d ]. % 0.41/0.60 exact (zenon_H201 zenon_H207). % 0.41/0.60 apply (zenon_L5_); trivial. % 0.41/0.60 exact (axiom_192 zenon_H228). % 0.41/0.60 exact (axiom_191 zenon_H225). % 0.41/0.60 exact (axiom_168 zenon_H222). % 0.41/0.60 exact (axiom_157 zenon_H21f). % 0.41/0.60 exact (axiom_136 zenon_H21c). % 0.41/0.60 exact (axiom_126 zenon_H219). % 0.41/0.60 Qed. % 0.41/0.60 % SZS output end Proof % 0.41/0.60 (* END-PROOF *) % 0.41/0.60 nodes searched: 360 % 0.41/0.60 max branch formulas: 371 % 0.41/0.60 proof nodes created: 204 % 0.41/0.60 formulas created: 2642 % 0.41/0.60 %------------------------------------------------------------------------------