%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : KRS153+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.62s 0.80s % Output : Proof 0.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : KRS153+1 : TPTP v8.1.0. Released v3.1.0. % 0.10/0.13 % Command : run_zenon %s %d % 0.13/0.34 % Computer : n019.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Tue Jun 7 20:45:25 EDT 2022 % 0.13/0.34 % CPUTime : % 0.62/0.80 (* PROOF-FOUND *) % 0.62/0.80 % SZS status Theorem % 0.62/0.80 (* BEGIN-PROOF *) % 0.62/0.80 % SZS output start Proof % 0.62/0.80 Theorem the_axiom : ((forall X : zenon_U, ((cowlThing X)/\(~(cowlNothing X))))/\((forall X : zenon_U, ((xsd_string X)<->(~(xsd_integer X))))/\((cC106 (iV16439))/\((cC28 (iV16439))/\((cC130 (iV16439))/\((cowlThing (iV16439))/\((cC108 (iV16439))/\((cC104 (iV16439))/\((cC80 (iV16440))/\((cowlThing (iV16440))/\((cC82 (iV16440))/\((cC98 (iV16440))/\((cowlThing (iV16448))/\((cC38 (iV16448))/\((cC62 (iV16453))/\((cowlThing (iV16453))/\((cC76 (iV16453))/\((cC60 (iV16453))/\((cC44 (iV16455))/\((cowlThing (iV16455))/\((cC56 (iV16455))/\((cC42 (iV16455))/\((cowlThing (iV16457))/\((cC38 (iV16457))/\((cC68 (iV16459))/\((cowlThing (iV16459))/\((cC88 (iV16459))/\((cC50 (iV16459))/\((cC34 (iV16459))/\((cowlThing (iV16460))/\((cC38 (iV16460))/\((cC44 (iV16461))/\((cowlThing (iV16461))/\((cC56 (iV16461))/\((cC42 (iV16461))/\((cowlThing (iV16462))/\((cC38 (iV16462))/\((cC62 (iV16463))/\((cowlThing (iV16463))/\((cC76 (iV16463))/\((cC60 (iV16463))/\((cC44 (iV16464))/\((cowlThing (iV16464))/\((cC56 (iV16464))/\((cC42 (iV16464))/\((cowlThing (iV16465))/\(cC38 (iV16465)))))))))))))))))))))))))))))))))))))))))))))))). % 0.62/0.80 Proof. % 0.62/0.80 assert (zenon_L1_ : (~(cC80 (iV16440))) -> False). % 0.62/0.80 do 0 intro. intros zenon_Hc9. % 0.62/0.80 generalize (axiom_49 (iV16440)). zenon_intro zenon_Hca. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_Hca); [ zenon_intro zenon_Hc9; zenon_intro zenon_Hcd | zenon_intro zenon_Hcc; zenon_intro zenon_Hcb ]. % 0.62/0.80 apply zenon_Hcd. exists (iV16463). apply NNPP. zenon_intro zenon_Hce. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_Hce); [ zenon_intro zenon_Hd0 | zenon_intro zenon_Hcf ]. % 0.62/0.80 exact (zenon_Hd0 axiom_73). % 0.62/0.80 exact (zenon_Hcf axiom_175). % 0.62/0.80 exact (zenon_Hc9 zenon_Hcc). % 0.62/0.80 (* end of lemma zenon_L1_ *) % 0.62/0.80 assert (zenon_L2_ : (~(exists Y : zenon_U, ((rR1 (iV16440) Y)/\(~(cC76 Y))))) -> (~(cC82 (iV16440))) -> False). % 0.62/0.80 do 0 intro. intros zenon_Hd1 zenon_Hd2. % 0.62/0.80 generalize (axiom_50 (iV16440)). zenon_intro zenon_Hd3. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_Hd3); [ zenon_intro zenon_Hd2; zenon_intro zenon_Hd6 | zenon_intro zenon_Hd5; zenon_intro zenon_Hd4 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_Hd6); [ zenon_intro zenon_Hd7 | zenon_intro zenon_Hc9 ]. % 0.62/0.80 apply zenon_Hd7. zenon_intro zenon_Hd8. % 0.62/0.80 generalize (axiom_48 (iV16440)). zenon_intro zenon_Hd9. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_Hd9); [ zenon_intro axiom_70; zenon_intro zenon_Hd1 | zenon_intro zenon_Hd8; zenon_intro zenon_Hda ]. % 0.62/0.80 exact (axiom_70 zenon_Hd8). % 0.62/0.80 exact (zenon_Hd1 zenon_Hda). % 0.62/0.80 apply (zenon_L1_); trivial. % 0.62/0.80 exact (zenon_Hd2 zenon_Hd5). % 0.62/0.80 (* end of lemma zenon_L2_ *) % 0.62/0.80 assert (zenon_L3_ : (~(cC60 (iV16453))) -> False). % 0.62/0.80 do 0 intro. intros zenon_Hdb. % 0.62/0.80 generalize (axiom_39 (iV16453)). zenon_intro zenon_Hdc. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_Hdc); [ zenon_intro zenon_Hdb; zenon_intro zenon_Hdf | zenon_intro zenon_Hde; zenon_intro zenon_Hdd ]. % 0.62/0.80 apply zenon_Hdf. exists (iV16461). apply NNPP. zenon_intro zenon_He0. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_He0); [ zenon_intro zenon_He2 | zenon_intro zenon_He1 ]. % 0.62/0.80 exact (zenon_He2 axiom_96). % 0.62/0.80 exact (zenon_He1 axiom_151). % 0.62/0.80 exact (zenon_Hdb zenon_Hde). % 0.62/0.80 (* end of lemma zenon_L3_ *) % 0.62/0.80 assert (zenon_L4_ : (~(exists Y : zenon_U, ((rR1 (iV16453) Y)/\(~(cC56 Y))))) -> (~(cC62 (iV16453))) -> False). % 0.62/0.80 do 0 intro. intros zenon_He3 zenon_He4. % 0.62/0.80 generalize (axiom_40 (iV16453)). zenon_intro zenon_He5. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_He5); [ zenon_intro zenon_He4; zenon_intro zenon_He8 | zenon_intro zenon_He7; zenon_intro zenon_He6 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_He8); [ zenon_intro zenon_Hdb | zenon_intro zenon_He9 ]. % 0.62/0.80 apply (zenon_L3_); trivial. % 0.62/0.80 apply zenon_He9. zenon_intro zenon_Hea. % 0.62/0.80 generalize (axiom_37 (iV16453)). zenon_intro zenon_Heb. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_Heb); [ zenon_intro axiom_91; zenon_intro zenon_He3 | zenon_intro zenon_Hea; zenon_intro zenon_Hec ]. % 0.62/0.80 exact (axiom_91 zenon_Hea). % 0.62/0.80 exact (zenon_He3 zenon_Hec). % 0.62/0.80 exact (zenon_He4 zenon_He7). % 0.62/0.80 (* end of lemma zenon_L4_ *) % 0.62/0.80 assert (zenon_L5_ : (~(cC42 (iV16455))) -> False). % 0.62/0.80 do 0 intro. intros zenon_Hed. % 0.62/0.80 generalize (axiom_29 (iV16455)). zenon_intro zenon_Hee. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_Hee); [ zenon_intro zenon_Hed; zenon_intro zenon_Hf1 | zenon_intro zenon_Hf0; zenon_intro zenon_Hef ]. % 0.62/0.80 apply zenon_Hf1. exists (iV16460). apply NNPP. zenon_intro zenon_Hf2. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_Hf2); [ zenon_intro zenon_Hf4 | zenon_intro zenon_Hf3 ]. % 0.62/0.80 exact (zenon_Hf4 axiom_107). % 0.62/0.80 exact (zenon_Hf3 axiom_141). % 0.62/0.80 exact (zenon_Hed zenon_Hf0). % 0.62/0.80 (* end of lemma zenon_L5_ *) % 0.62/0.80 assert (zenon_L6_ : (~(exists Y : zenon_U, ((rR1 (iV16455) Y)/\(~(cC38 Y))))) -> (~(cC44 (iV16455))) -> False). % 0.62/0.80 do 0 intro. intros zenon_Hf5 zenon_Hf6. % 0.62/0.80 generalize (axiom_30 (iV16455)). zenon_intro zenon_Hf7. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_Hf7); [ zenon_intro zenon_Hf6; zenon_intro zenon_Hfa | zenon_intro zenon_Hf9; zenon_intro zenon_Hf8 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_Hfa); [ zenon_intro zenon_Hfb | zenon_intro zenon_Hed ]. % 0.62/0.80 apply zenon_Hfb. zenon_intro zenon_Hfc. % 0.62/0.80 generalize (axiom_28 (iV16455)). zenon_intro zenon_Hfd. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_Hfd); [ zenon_intro axiom_98; zenon_intro zenon_Hf5 | zenon_intro zenon_Hfc; zenon_intro zenon_Hfe ]. % 0.62/0.80 exact (axiom_98 zenon_Hfc). % 0.62/0.80 exact (zenon_Hf5 zenon_Hfe). % 0.62/0.80 apply (zenon_L5_); trivial. % 0.62/0.80 exact (zenon_Hf6 zenon_Hf9). % 0.62/0.80 (* end of lemma zenon_L6_ *) % 0.62/0.80 assert (zenon_L7_ : (~(~(cC8 (iV16462)))) -> False). % 0.62/0.80 do 0 intro. intros zenon_Hff. % 0.62/0.80 exact (zenon_Hff axiom_159). % 0.62/0.80 (* end of lemma zenon_L7_ *) % 0.62/0.80 assert (zenon_L8_ : (~(cC42 (iV16461))) -> False). % 0.62/0.80 do 0 intro. intros zenon_H100. % 0.62/0.80 generalize (axiom_29 (iV16461)). zenon_intro zenon_H101. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H101); [ zenon_intro zenon_H100; zenon_intro zenon_H104 | zenon_intro zenon_H103; zenon_intro zenon_H102 ]. % 0.62/0.80 apply zenon_H104. exists (iV16462). apply NNPP. zenon_intro zenon_H105. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H105); [ zenon_intro zenon_H106 | zenon_intro zenon_Hff ]. % 0.62/0.80 exact (zenon_H106 axiom_157). % 0.62/0.80 exact (zenon_Hff axiom_159). % 0.62/0.80 exact (zenon_H100 zenon_H103). % 0.62/0.80 (* end of lemma zenon_L8_ *) % 0.62/0.80 assert (zenon_L9_ : (~(exists Y : zenon_U, ((rR1 (iV16461) Y)/\(~(cC38 Y))))) -> (~(cC44 (iV16461))) -> False). % 0.62/0.80 do 0 intro. intros zenon_H107 zenon_H108. % 0.62/0.80 generalize (axiom_30 (iV16461)). zenon_intro zenon_H109. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H109); [ zenon_intro zenon_H108; zenon_intro zenon_H10c | zenon_intro zenon_H10b; zenon_intro zenon_H10a ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H10c); [ zenon_intro zenon_H10d | zenon_intro zenon_H100 ]. % 0.62/0.80 apply zenon_H10d. zenon_intro zenon_H10e. % 0.62/0.80 generalize (axiom_28 (iV16461)). zenon_intro zenon_H10f. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H10f); [ zenon_intro axiom_147; zenon_intro zenon_H107 | zenon_intro zenon_H10e; zenon_intro zenon_H110 ]. % 0.62/0.80 exact (axiom_147 zenon_H10e). % 0.62/0.80 exact (zenon_H107 zenon_H110). % 0.62/0.80 apply (zenon_L8_); trivial. % 0.62/0.80 exact (zenon_H108 zenon_H10b). % 0.62/0.80 (* end of lemma zenon_L9_ *) % 0.62/0.80 assert (zenon_L10_ : (~(~(cC12 (iV16464)))) -> False). % 0.62/0.80 do 0 intro. intros zenon_H111. % 0.62/0.80 exact (zenon_H111 axiom_183). % 0.62/0.80 (* end of lemma zenon_L10_ *) % 0.62/0.80 assert (zenon_L11_ : (~(cC60 (iV16463))) -> False). % 0.62/0.80 do 0 intro. intros zenon_H112. % 0.62/0.80 generalize (axiom_39 (iV16463)). zenon_intro zenon_H113. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H113); [ zenon_intro zenon_H112; zenon_intro zenon_H116 | zenon_intro zenon_H115; zenon_intro zenon_H114 ]. % 0.62/0.80 apply zenon_H116. exists (iV16464). apply NNPP. zenon_intro zenon_H117. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H117); [ zenon_intro zenon_H118 | zenon_intro zenon_H111 ]. % 0.62/0.80 exact (zenon_H118 axiom_177). % 0.62/0.80 exact (zenon_H111 axiom_183). % 0.62/0.80 exact (zenon_H112 zenon_H115). % 0.62/0.80 (* end of lemma zenon_L11_ *) % 0.62/0.80 assert (zenon_L12_ : (~(exists Y : zenon_U, ((rR1 (iV16463) Y)/\(~(cC56 Y))))) -> (~(cC62 (iV16463))) -> False). % 0.62/0.80 do 0 intro. intros zenon_H119 zenon_H11a. % 0.62/0.80 generalize (axiom_40 (iV16463)). zenon_intro zenon_H11b. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H11b); [ zenon_intro zenon_H11a; zenon_intro zenon_H11e | zenon_intro zenon_H11d; zenon_intro zenon_H11c ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H11e); [ zenon_intro zenon_H112 | zenon_intro zenon_H11f ]. % 0.62/0.80 apply (zenon_L11_); trivial. % 0.62/0.80 apply zenon_H11f. zenon_intro zenon_H120. % 0.62/0.80 generalize (axiom_37 (iV16463)). zenon_intro zenon_H121. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H121); [ zenon_intro axiom_174; zenon_intro zenon_H119 | zenon_intro zenon_H120; zenon_intro zenon_H122 ]. % 0.62/0.80 exact (axiom_174 zenon_H120). % 0.62/0.80 exact (zenon_H119 zenon_H122). % 0.62/0.80 exact (zenon_H11a zenon_H11d). % 0.62/0.80 (* end of lemma zenon_L12_ *) % 0.62/0.80 assert (zenon_L13_ : (~(~(cC8 (iV16465)))) -> False). % 0.62/0.80 do 0 intro. intros zenon_H123. % 0.62/0.80 exact (zenon_H123 axiom_194). % 0.62/0.80 (* end of lemma zenon_L13_ *) % 0.62/0.80 assert (zenon_L14_ : (~(cC42 (iV16464))) -> False). % 0.62/0.80 do 0 intro. intros zenon_H124. % 0.62/0.80 generalize (axiom_29 (iV16464)). zenon_intro zenon_H125. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H125); [ zenon_intro zenon_H124; zenon_intro zenon_H128 | zenon_intro zenon_H127; zenon_intro zenon_H126 ]. % 0.62/0.80 apply zenon_H128. exists (iV16465). apply NNPP. zenon_intro zenon_H129. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H129); [ zenon_intro zenon_H12a | zenon_intro zenon_H123 ]. % 0.62/0.80 exact (zenon_H12a axiom_188). % 0.62/0.80 exact (zenon_H123 axiom_194). % 0.62/0.80 exact (zenon_H124 zenon_H127). % 0.62/0.80 (* end of lemma zenon_L14_ *) % 0.62/0.80 assert (zenon_L15_ : (~(exists Y : zenon_U, ((rR1 (iV16464) Y)/\(~(cC38 Y))))) -> (~(cC44 (iV16464))) -> False). % 0.62/0.80 do 0 intro. intros zenon_H12b zenon_H12c. % 0.62/0.80 generalize (axiom_30 (iV16464)). zenon_intro zenon_H12d. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H12d); [ zenon_intro zenon_H12c; zenon_intro zenon_H130 | zenon_intro zenon_H12f; zenon_intro zenon_H12e ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H130); [ zenon_intro zenon_H131 | zenon_intro zenon_H124 ]. % 0.62/0.80 apply zenon_H131. zenon_intro zenon_H132. % 0.62/0.80 generalize (axiom_28 (iV16464)). zenon_intro zenon_H133. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H133); [ zenon_intro axiom_179; zenon_intro zenon_H12b | zenon_intro zenon_H132; zenon_intro zenon_H134 ]. % 0.62/0.80 exact (axiom_179 zenon_H132). % 0.62/0.80 exact (zenon_H12b zenon_H134). % 0.62/0.80 apply (zenon_L14_); trivial. % 0.62/0.80 exact (zenon_H12c zenon_H12f). % 0.62/0.80 (* end of lemma zenon_L15_ *) % 0.62/0.80 apply NNPP. intro zenon_G. % 0.62/0.80 generalize (axiom_59 (iV16439)). zenon_intro zenon_H135. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H135); [ zenon_intro zenon_H138; zenon_intro zenon_H137 | zenon_intro axiom_61; zenon_intro zenon_H136 ]. % 0.62/0.80 exact (zenon_H138 axiom_61). % 0.62/0.80 apply (zenon_and_s _ _ zenon_H136). zenon_intro zenon_H13a. zenon_intro zenon_H139. % 0.62/0.80 generalize (axiom_6 (iV16439)). zenon_intro zenon_H13b. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H13b); [ zenon_intro zenon_H13e; zenon_intro zenon_H13d | zenon_intro zenon_H13a; zenon_intro zenon_H13c ]. % 0.62/0.80 exact (zenon_H13e zenon_H13a). % 0.62/0.80 apply (zenon_and_s _ _ zenon_H13c). zenon_intro zenon_H140. zenon_intro zenon_H13f. % 0.62/0.80 generalize (axiom_22 (iV16439)). zenon_intro zenon_H141. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H141); [ zenon_intro zenon_H144; zenon_intro zenon_H143 | zenon_intro zenon_H140; zenon_intro zenon_H142 ]. % 0.62/0.80 exact (zenon_H144 zenon_H140). % 0.62/0.80 generalize (axiom_5 (iV16439)). zenon_intro zenon_H145. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H145); [ zenon_intro zenon_H148; zenon_intro zenon_H147 | zenon_intro zenon_H13f; zenon_intro zenon_H146 ]. % 0.62/0.80 exact (zenon_H148 zenon_H13f). % 0.62/0.80 apply (zenon_and_s _ _ zenon_H146). zenon_intro axiom_62. zenon_intro zenon_H149. % 0.62/0.80 generalize (axiom_4 (iV16439)). zenon_intro zenon_H14a. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H14a); [ zenon_intro zenon_H14d; zenon_intro zenon_H14c | zenon_intro zenon_H149; zenon_intro zenon_H14b ]. % 0.62/0.80 exact (zenon_H14d zenon_H149). % 0.62/0.80 generalize (axiom_15 (iV16439)). zenon_intro zenon_H14e. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H14e); [ zenon_intro zenon_H151; zenon_intro zenon_H150 | zenon_intro zenon_H139; zenon_intro zenon_H14f ]. % 0.62/0.80 exact (zenon_H151 zenon_H139). % 0.62/0.80 generalize (axiom_48 (iV16440)). zenon_intro zenon_Hd9. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_Hd9); [ zenon_intro axiom_70; zenon_intro zenon_Hd1 | zenon_intro zenon_Hd8; zenon_intro zenon_Hda ]. % 0.62/0.80 generalize (axiom_57 (iV16440)). zenon_intro zenon_H152. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H152); [ zenon_intro axiom_71; zenon_intro zenon_H155 | zenon_intro zenon_H154; zenon_intro zenon_H153 ]. % 0.62/0.80 generalize (axiom_26 (iV16448)). zenon_intro zenon_H156. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H156); [ zenon_intro axiom_76; zenon_intro zenon_H159 | zenon_intro zenon_H158; zenon_intro zenon_H157 ]. % 0.62/0.80 generalize (axiom_37 (iV16453)). zenon_intro zenon_Heb. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_Heb); [ zenon_intro axiom_91; zenon_intro zenon_He3 | zenon_intro zenon_Hea; zenon_intro zenon_Hec ]. % 0.62/0.80 generalize (axiom_46 (iV16453)). zenon_intro zenon_H15a. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H15a); [ zenon_intro axiom_92; zenon_intro zenon_H15d | zenon_intro zenon_H15c; zenon_intro zenon_H15b ]. % 0.62/0.80 generalize (axiom_28 (iV16455)). zenon_intro zenon_Hfd. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_Hfd); [ zenon_intro axiom_98; zenon_intro zenon_Hf5 | zenon_intro zenon_Hfc; zenon_intro zenon_Hfe ]. % 0.62/0.80 generalize (axiom_35 (iV16455)). zenon_intro zenon_H15e. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H15e); [ zenon_intro axiom_103; zenon_intro zenon_H161 | zenon_intro zenon_H160; zenon_intro zenon_H15f ]. % 0.62/0.80 generalize (axiom_26 (iV16457)). zenon_intro zenon_H162. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H162); [ zenon_intro axiom_108; zenon_intro zenon_H165 | zenon_intro zenon_H164; zenon_intro zenon_H163 ]. % 0.62/0.80 generalize (axiom_26 (iV16460)). zenon_intro zenon_H166. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H166); [ zenon_intro axiom_137; zenon_intro zenon_H169 | zenon_intro zenon_H168; zenon_intro zenon_H167 ]. % 0.62/0.80 generalize (axiom_28 (iV16461)). zenon_intro zenon_H10f. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H10f); [ zenon_intro axiom_147; zenon_intro zenon_H107 | zenon_intro zenon_H10e; zenon_intro zenon_H110 ]. % 0.62/0.80 generalize (axiom_35 (iV16461)). zenon_intro zenon_H16a. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H16a); [ zenon_intro axiom_152; zenon_intro zenon_H16d | zenon_intro zenon_H16c; zenon_intro zenon_H16b ]. % 0.62/0.80 generalize (axiom_26 (iV16462)). zenon_intro zenon_H16e. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H16e); [ zenon_intro axiom_161; zenon_intro zenon_H171 | zenon_intro zenon_H170; zenon_intro zenon_H16f ]. % 0.62/0.80 generalize (axiom_46 (iV16463)). zenon_intro zenon_H172. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H172); [ zenon_intro axiom_173; zenon_intro zenon_H175 | zenon_intro zenon_H174; zenon_intro zenon_H173 ]. % 0.62/0.80 generalize (axiom_37 (iV16463)). zenon_intro zenon_H121. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H121); [ zenon_intro axiom_174; zenon_intro zenon_H119 | zenon_intro zenon_H120; zenon_intro zenon_H122 ]. % 0.62/0.80 generalize (axiom_28 (iV16464)). zenon_intro zenon_H133. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H133); [ zenon_intro axiom_179; zenon_intro zenon_H12b | zenon_intro zenon_H132; zenon_intro zenon_H134 ]. % 0.62/0.80 generalize (axiom_35 (iV16464)). zenon_intro zenon_H176. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H176); [ zenon_intro axiom_181; zenon_intro zenon_H179 | zenon_intro zenon_H178; zenon_intro zenon_H177 ]. % 0.62/0.80 generalize (axiom_26 (iV16465)). zenon_intro zenon_H17a. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H17a); [ zenon_intro axiom_195; zenon_intro zenon_H17d | zenon_intro zenon_H17c; zenon_intro zenon_H17b ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_G); [ zenon_intro zenon_H17f | zenon_intro zenon_H17e ]. % 0.62/0.80 exact (zenon_H17f axiom_0). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H17e); [ zenon_intro zenon_H181 | zenon_intro zenon_H180 ]. % 0.62/0.80 exact (zenon_H181 axiom_1). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H180); [ zenon_intro zenon_H148 | zenon_intro zenon_H182 ]. % 0.62/0.80 generalize (axiom_5 (iV16439)). zenon_intro zenon_H145. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H145); [ zenon_intro zenon_H148; zenon_intro zenon_H147 | zenon_intro zenon_H13f; zenon_intro zenon_H146 ]. % 0.62/0.80 exact (zenon_H147 zenon_H146). % 0.62/0.80 exact (zenon_H148 zenon_H13f). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H182); [ zenon_intro zenon_H144 | zenon_intro zenon_H183 ]. % 0.62/0.80 generalize (axiom_22 (iV16439)). zenon_intro zenon_H141. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H141); [ zenon_intro zenon_H144; zenon_intro zenon_H143 | zenon_intro zenon_H140; zenon_intro zenon_H142 ]. % 0.62/0.80 exact (zenon_H143 zenon_H142). % 0.62/0.80 exact (zenon_H144 zenon_H140). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H183); [ zenon_intro zenon_H151 | zenon_intro zenon_H184 ]. % 0.62/0.80 generalize (axiom_15 (iV16439)). zenon_intro zenon_H14e. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H14e); [ zenon_intro zenon_H151; zenon_intro zenon_H150 | zenon_intro zenon_H139; zenon_intro zenon_H14f ]. % 0.62/0.80 exact (zenon_H150 zenon_H14f). % 0.62/0.80 exact (zenon_H151 zenon_H139). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H184); [ zenon_intro zenon_H186 | zenon_intro zenon_H185 ]. % 0.62/0.80 exact (zenon_H186 axiom_63). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H185); [ zenon_intro zenon_H13e | zenon_intro zenon_H187 ]. % 0.62/0.80 generalize (axiom_6 (iV16439)). zenon_intro zenon_H13b. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H13b); [ zenon_intro zenon_H13e; zenon_intro zenon_H13d | zenon_intro zenon_H13a; zenon_intro zenon_H13c ]. % 0.62/0.80 exact (zenon_H13d zenon_H13c). % 0.62/0.80 exact (zenon_H13e zenon_H13a). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H187); [ zenon_intro zenon_H14d | zenon_intro zenon_H188 ]. % 0.62/0.80 generalize (axiom_4 (iV16439)). zenon_intro zenon_H14a. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H14a); [ zenon_intro zenon_H14d; zenon_intro zenon_H14c | zenon_intro zenon_H149; zenon_intro zenon_H14b ]. % 0.62/0.80 exact (zenon_H14c zenon_H14b). % 0.62/0.80 exact (zenon_H14d zenon_H149). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H188); [ zenon_intro zenon_Hc9 | zenon_intro zenon_H189 ]. % 0.62/0.80 apply (zenon_L1_); trivial. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H189); [ zenon_intro zenon_H18b | zenon_intro zenon_H18a ]. % 0.62/0.80 exact (zenon_H18b axiom_72). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H18a); [ zenon_intro zenon_Hd2 | zenon_intro zenon_H18c ]. % 0.62/0.80 apply (zenon_L2_); trivial. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H18c); [ zenon_intro zenon_H18e | zenon_intro zenon_H18d ]. % 0.62/0.80 generalize (axiom_58 (iV16440)). zenon_intro zenon_H18f. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H18f); [ zenon_intro zenon_H18e; zenon_intro zenon_H192 | zenon_intro zenon_H191; zenon_intro zenon_H190 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H192); [ zenon_intro zenon_H193 | zenon_intro zenon_Hd2 ]. % 0.62/0.80 apply zenon_H193. zenon_intro zenon_H154. % 0.62/0.80 generalize (axiom_57 (iV16440)). zenon_intro zenon_H152. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H152); [ zenon_intro axiom_71; zenon_intro zenon_H155 | zenon_intro zenon_H154; zenon_intro zenon_H153 ]. % 0.62/0.80 exact (axiom_71 zenon_H154). % 0.62/0.80 exact (zenon_H155 zenon_H153). % 0.62/0.80 apply (zenon_L2_); trivial. % 0.62/0.80 exact (zenon_H18e zenon_H191). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H18d); [ zenon_intro zenon_H195 | zenon_intro zenon_H194 ]. % 0.62/0.80 exact (zenon_H195 axiom_84). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H194); [ zenon_intro zenon_H197 | zenon_intro zenon_H196 ]. % 0.62/0.80 generalize (axiom_27 (iV16448)). zenon_intro zenon_H198. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H198); [ zenon_intro zenon_H197; zenon_intro zenon_H19b | zenon_intro zenon_H19a; zenon_intro zenon_H199 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H19b); [ zenon_intro zenon_H19d | zenon_intro zenon_H19c ]. % 0.62/0.80 apply zenon_H19d. zenon_intro zenon_H158. % 0.62/0.80 generalize (axiom_26 (iV16448)). zenon_intro zenon_H156. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H156); [ zenon_intro axiom_76; zenon_intro zenon_H159 | zenon_intro zenon_H158; zenon_intro zenon_H157 ]. % 0.62/0.80 exact (axiom_76 zenon_H158). % 0.62/0.80 exact (zenon_H159 zenon_H157). % 0.62/0.80 exact (zenon_H19c axiom_79). % 0.62/0.80 exact (zenon_H197 zenon_H19a). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H196); [ zenon_intro zenon_He4 | zenon_intro zenon_H19e ]. % 0.62/0.80 apply (zenon_L4_); trivial. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H19e); [ zenon_intro zenon_H1a0 | zenon_intro zenon_H19f ]. % 0.62/0.80 exact (zenon_H1a0 axiom_94). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H19f); [ zenon_intro zenon_H1a2 | zenon_intro zenon_H1a1 ]. % 0.62/0.80 generalize (axiom_47 (iV16453)). zenon_intro zenon_H1a3. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H1a3); [ zenon_intro zenon_H1a2; zenon_intro zenon_H1a6 | zenon_intro zenon_H1a5; zenon_intro zenon_H1a4 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1a6); [ zenon_intro zenon_H1a7 | zenon_intro zenon_He4 ]. % 0.62/0.80 apply zenon_H1a7. zenon_intro zenon_H15c. % 0.62/0.80 generalize (axiom_46 (iV16453)). zenon_intro zenon_H15a. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H15a); [ zenon_intro axiom_92; zenon_intro zenon_H15d | zenon_intro zenon_H15c; zenon_intro zenon_H15b ]. % 0.62/0.80 exact (axiom_92 zenon_H15c). % 0.62/0.80 exact (zenon_H15d zenon_H15b). % 0.62/0.80 apply (zenon_L4_); trivial. % 0.62/0.80 exact (zenon_H1a2 zenon_H1a5). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1a1); [ zenon_intro zenon_Hdb | zenon_intro zenon_H1a8 ]. % 0.62/0.80 apply (zenon_L3_); trivial. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1a8); [ zenon_intro zenon_Hf6 | zenon_intro zenon_H1a9 ]. % 0.62/0.80 apply (zenon_L6_); trivial. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1a9); [ zenon_intro zenon_H1ab | zenon_intro zenon_H1aa ]. % 0.62/0.80 exact (zenon_H1ab axiom_105). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1aa); [ zenon_intro zenon_H1ad | zenon_intro zenon_H1ac ]. % 0.62/0.80 generalize (axiom_36 (iV16455)). zenon_intro zenon_H1ae. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H1ae); [ zenon_intro zenon_H1ad; zenon_intro zenon_H1b1 | zenon_intro zenon_H1b0; zenon_intro zenon_H1af ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1b1); [ zenon_intro zenon_Hf6 | zenon_intro zenon_H1b2 ]. % 0.62/0.80 apply (zenon_L6_); trivial. % 0.62/0.80 apply zenon_H1b2. zenon_intro zenon_H160. % 0.62/0.80 generalize (axiom_35 (iV16455)). zenon_intro zenon_H15e. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H15e); [ zenon_intro axiom_103; zenon_intro zenon_H161 | zenon_intro zenon_H160; zenon_intro zenon_H15f ]. % 0.62/0.80 exact (axiom_103 zenon_H160). % 0.62/0.80 exact (zenon_H161 zenon_H15f). % 0.62/0.80 exact (zenon_H1ad zenon_H1b0). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1ac); [ zenon_intro zenon_Hed | zenon_intro zenon_H1b3 ]. % 0.62/0.80 apply (zenon_L5_); trivial. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1b3); [ zenon_intro zenon_H1b5 | zenon_intro zenon_H1b4 ]. % 0.62/0.80 exact (zenon_H1b5 axiom_117). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1b4); [ zenon_intro zenon_H1b7 | zenon_intro zenon_H1b6 ]. % 0.62/0.80 generalize (axiom_27 (iV16457)). zenon_intro zenon_H1b8. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H1b8); [ zenon_intro zenon_H1b7; zenon_intro zenon_H1bb | zenon_intro zenon_H1ba; zenon_intro zenon_H1b9 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1bb); [ zenon_intro zenon_H1bd | zenon_intro zenon_H1bc ]. % 0.62/0.80 apply zenon_H1bd. zenon_intro zenon_H164. % 0.62/0.80 generalize (axiom_26 (iV16457)). zenon_intro zenon_H162. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H162); [ zenon_intro axiom_108; zenon_intro zenon_H165 | zenon_intro zenon_H164; zenon_intro zenon_H163 ]. % 0.62/0.80 exact (axiom_108 zenon_H164). % 0.62/0.80 exact (zenon_H165 zenon_H163). % 0.62/0.80 exact (zenon_H1bc axiom_113). % 0.62/0.80 exact (zenon_H1b7 zenon_H1ba). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1b6); [ zenon_intro zenon_H1bf | zenon_intro zenon_H1be ]. % 0.62/0.80 generalize (axiom_43 (iV16459)). zenon_intro zenon_H1c0. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H1c0); [ zenon_intro zenon_H1bf; zenon_intro zenon_H1c3 | zenon_intro zenon_H1c2; zenon_intro zenon_H1c1 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1c3); [ zenon_intro zenon_H1c5 | zenon_intro zenon_H1c4 ]. % 0.62/0.80 apply zenon_H1c5. zenon_intro zenon_H1c6. % 0.62/0.80 generalize (axiom_41 (iV16459)). zenon_intro zenon_H1c7. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H1c7); [ zenon_intro axiom_133; zenon_intro zenon_H1c9 | zenon_intro zenon_H1c6; zenon_intro zenon_H1c8 ]. % 0.62/0.80 exact (axiom_133 zenon_H1c6). % 0.62/0.80 apply (zenon_and_s _ _ zenon_H1c8). zenon_intro zenon_H1ca. zenon_intro axiom_128. % 0.62/0.80 exact (axiom_129 zenon_H1ca). % 0.62/0.80 apply zenon_H1c4. zenon_intro zenon_H1cb. % 0.62/0.80 generalize (axiom_42 (iV16459)). zenon_intro zenon_H1cc. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H1cc); [ zenon_intro axiom_127; zenon_intro zenon_H1ce | zenon_intro zenon_H1cb; zenon_intro zenon_H1cd ]. % 0.62/0.80 exact (axiom_127 zenon_H1cb). % 0.62/0.80 apply (zenon_and_s _ _ zenon_H1cd). zenon_intro axiom_129. zenon_intro zenon_H1cf. % 0.62/0.80 exact (zenon_H1cf axiom_128). % 0.62/0.80 exact (zenon_H1bf zenon_H1c2). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1be); [ zenon_intro zenon_H1d1 | zenon_intro zenon_H1d0 ]. % 0.62/0.80 exact (zenon_H1d1 axiom_134). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1d0); [ zenon_intro zenon_H1d3 | zenon_intro zenon_H1d2 ]. % 0.62/0.80 generalize (axiom_53 (iV16459)). zenon_intro zenon_H1d4. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H1d4); [ zenon_intro zenon_H1d3; zenon_intro zenon_H1d7 | zenon_intro zenon_H1d6; zenon_intro zenon_H1d5 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1d7); [ zenon_intro zenon_H1d9 | zenon_intro zenon_H1d8 ]. % 0.62/0.80 apply zenon_H1d9. zenon_intro zenon_H1da. % 0.62/0.80 generalize (axiom_51 (iV16459)). zenon_intro zenon_H1db. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H1db); [ zenon_intro axiom_132; zenon_intro zenon_H1dd | zenon_intro zenon_H1da; zenon_intro zenon_H1dc ]. % 0.62/0.80 exact (axiom_132 zenon_H1da). % 0.62/0.80 apply (zenon_and_s _ _ zenon_H1dc). zenon_intro zenon_H1de. zenon_intro axiom_128. % 0.62/0.80 exact (axiom_130 zenon_H1de). % 0.62/0.80 apply zenon_H1d8. zenon_intro zenon_H1df. % 0.62/0.80 generalize (axiom_52 (iV16459)). zenon_intro zenon_H1e0. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H1e0); [ zenon_intro axiom_123; zenon_intro zenon_H1e2 | zenon_intro zenon_H1df; zenon_intro zenon_H1e1 ]. % 0.62/0.80 exact (axiom_123 zenon_H1df). % 0.62/0.80 apply (zenon_and_s _ _ zenon_H1e1). zenon_intro zenon_H1cf. zenon_intro axiom_130. % 0.62/0.80 exact (zenon_H1cf axiom_128). % 0.62/0.80 exact (zenon_H1d3 zenon_H1d6). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1d2); [ zenon_intro zenon_H1e4 | zenon_intro zenon_H1e3 ]. % 0.62/0.80 generalize (axiom_33 (iV16459)). zenon_intro zenon_H1e5. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H1e5); [ zenon_intro zenon_H1e4; zenon_intro zenon_H1e8 | zenon_intro zenon_H1e7; zenon_intro zenon_H1e6 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1e8); [ zenon_intro zenon_H1ea | zenon_intro zenon_H1e9 ]. % 0.62/0.80 apply zenon_H1ea. zenon_intro zenon_H1eb. % 0.62/0.80 generalize (axiom_31 (iV16459)). zenon_intro zenon_H1ec. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H1ec); [ zenon_intro axiom_124; zenon_intro zenon_H1ee | zenon_intro zenon_H1eb; zenon_intro zenon_H1ed ]. % 0.62/0.80 exact (axiom_124 zenon_H1eb). % 0.62/0.80 apply (zenon_and_s _ _ zenon_H1ed). zenon_intro zenon_H1ca. zenon_intro axiom_119. % 0.62/0.80 exact (axiom_129 zenon_H1ca). % 0.62/0.80 apply zenon_H1e9. zenon_intro zenon_H1ef. % 0.62/0.80 generalize (axiom_32 (iV16459)). zenon_intro zenon_H1f0. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H1f0); [ zenon_intro axiom_120; zenon_intro zenon_H1f2 | zenon_intro zenon_H1ef; zenon_intro zenon_H1f1 ]. % 0.62/0.80 exact (axiom_120 zenon_H1ef). % 0.62/0.80 apply (zenon_and_s _ _ zenon_H1f1). zenon_intro axiom_129. zenon_intro zenon_H1f3. % 0.62/0.80 exact (zenon_H1f3 axiom_119). % 0.62/0.80 exact (zenon_H1e4 zenon_H1e7). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1e3); [ zenon_intro zenon_H1f5 | zenon_intro zenon_H1f4 ]. % 0.62/0.80 generalize (axiom_25 (iV16459)). zenon_intro zenon_H1f6. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H1f6); [ zenon_intro zenon_H1f5; zenon_intro zenon_H1f9 | zenon_intro zenon_H1f8; zenon_intro zenon_H1f7 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1f9); [ zenon_intro zenon_H1fb | zenon_intro zenon_H1fa ]. % 0.62/0.80 apply zenon_H1fb. zenon_intro zenon_H1fc. % 0.62/0.80 generalize (axiom_24 (iV16459)). zenon_intro zenon_H1fd. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H1fd); [ zenon_intro axiom_135; zenon_intro zenon_H1ff | zenon_intro zenon_H1fc; zenon_intro zenon_H1fe ]. % 0.62/0.80 exact (axiom_135 zenon_H1fc). % 0.62/0.80 apply (zenon_and_s _ _ zenon_H1fe). zenon_intro axiom_130. zenon_intro zenon_H1f3. % 0.62/0.80 exact (zenon_H1f3 axiom_119). % 0.62/0.80 apply zenon_H1fa. zenon_intro zenon_H200. % 0.62/0.80 generalize (axiom_23 (iV16459)). zenon_intro zenon_H201. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H201); [ zenon_intro axiom_121; zenon_intro zenon_H203 | zenon_intro zenon_H200; zenon_intro zenon_H202 ]. % 0.62/0.80 exact (axiom_121 zenon_H200). % 0.62/0.80 apply (zenon_and_s _ _ zenon_H202). zenon_intro axiom_119. zenon_intro zenon_H1de. % 0.62/0.80 exact (axiom_130 zenon_H1de). % 0.62/0.80 exact (zenon_H1f5 zenon_H1f8). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H1f4); [ zenon_intro zenon_H205 | zenon_intro zenon_H204 ]. % 0.62/0.80 exact (zenon_H205 axiom_146). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H204); [ zenon_intro zenon_H207 | zenon_intro zenon_H206 ]. % 0.62/0.80 generalize (axiom_27 (iV16460)). zenon_intro zenon_H208. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H208); [ zenon_intro zenon_H207; zenon_intro zenon_H20b | zenon_intro zenon_H20a; zenon_intro zenon_H209 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H20b); [ zenon_intro zenon_H20d | zenon_intro zenon_H20c ]. % 0.62/0.80 apply zenon_H20d. zenon_intro zenon_H168. % 0.62/0.80 generalize (axiom_26 (iV16460)). zenon_intro zenon_H166. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H166); [ zenon_intro axiom_137; zenon_intro zenon_H169 | zenon_intro zenon_H168; zenon_intro zenon_H167 ]. % 0.62/0.80 exact (axiom_137 zenon_H168). % 0.62/0.80 exact (zenon_H169 zenon_H167). % 0.62/0.80 exact (zenon_H20c axiom_140). % 0.62/0.80 exact (zenon_H207 zenon_H20a). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H206); [ zenon_intro zenon_H108 | zenon_intro zenon_H20e ]. % 0.62/0.80 apply (zenon_L9_); trivial. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H20e); [ zenon_intro zenon_H210 | zenon_intro zenon_H20f ]. % 0.62/0.80 exact (zenon_H210 axiom_155). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H20f); [ zenon_intro zenon_H212 | zenon_intro zenon_H211 ]. % 0.62/0.80 generalize (axiom_36 (iV16461)). zenon_intro zenon_H213. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H213); [ zenon_intro zenon_H212; zenon_intro zenon_H216 | zenon_intro zenon_H215; zenon_intro zenon_H214 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H216); [ zenon_intro zenon_H108 | zenon_intro zenon_H217 ]. % 0.62/0.80 apply (zenon_L9_); trivial. % 0.62/0.80 apply zenon_H217. zenon_intro zenon_H16c. % 0.62/0.80 generalize (axiom_35 (iV16461)). zenon_intro zenon_H16a. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H16a); [ zenon_intro axiom_152; zenon_intro zenon_H16d | zenon_intro zenon_H16c; zenon_intro zenon_H16b ]. % 0.62/0.80 exact (axiom_152 zenon_H16c). % 0.62/0.80 exact (zenon_H16d zenon_H16b). % 0.62/0.80 exact (zenon_H212 zenon_H215). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H211); [ zenon_intro zenon_H100 | zenon_intro zenon_H218 ]. % 0.62/0.80 apply (zenon_L8_); trivial. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H218); [ zenon_intro zenon_H21a | zenon_intro zenon_H219 ]. % 0.62/0.80 exact (zenon_H21a axiom_168). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H219); [ zenon_intro zenon_H21c | zenon_intro zenon_H21b ]. % 0.62/0.80 generalize (axiom_27 (iV16462)). zenon_intro zenon_H21d. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H21d); [ zenon_intro zenon_H21c; zenon_intro zenon_H220 | zenon_intro zenon_H21f; zenon_intro zenon_H21e ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H220); [ zenon_intro zenon_H222 | zenon_intro zenon_H221 ]. % 0.62/0.80 apply zenon_H222. zenon_intro zenon_H170. % 0.62/0.80 generalize (axiom_26 (iV16462)). zenon_intro zenon_H16e. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H16e); [ zenon_intro axiom_161; zenon_intro zenon_H171 | zenon_intro zenon_H170; zenon_intro zenon_H16f ]. % 0.62/0.80 exact (axiom_161 zenon_H170). % 0.62/0.80 exact (zenon_H171 zenon_H16f). % 0.62/0.80 exact (zenon_H221 axiom_162). % 0.62/0.80 exact (zenon_H21c zenon_H21f). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H21b); [ zenon_intro zenon_H11a | zenon_intro zenon_H223 ]. % 0.62/0.80 apply (zenon_L12_); trivial. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H223); [ zenon_intro zenon_H225 | zenon_intro zenon_H224 ]. % 0.62/0.80 exact (zenon_H225 axiom_176). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H224); [ zenon_intro zenon_H227 | zenon_intro zenon_H226 ]. % 0.62/0.80 generalize (axiom_47 (iV16463)). zenon_intro zenon_H228. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H228); [ zenon_intro zenon_H227; zenon_intro zenon_H22b | zenon_intro zenon_H22a; zenon_intro zenon_H229 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H22b); [ zenon_intro zenon_H22c | zenon_intro zenon_H11a ]. % 0.62/0.80 apply zenon_H22c. zenon_intro zenon_H174. % 0.62/0.80 generalize (axiom_46 (iV16463)). zenon_intro zenon_H172. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H172); [ zenon_intro axiom_173; zenon_intro zenon_H175 | zenon_intro zenon_H174; zenon_intro zenon_H173 ]. % 0.62/0.80 exact (axiom_173 zenon_H174). % 0.62/0.80 exact (zenon_H175 zenon_H173). % 0.62/0.80 apply (zenon_L12_); trivial. % 0.62/0.80 exact (zenon_H227 zenon_H22a). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H226); [ zenon_intro zenon_H112 | zenon_intro zenon_H22d ]. % 0.62/0.80 apply (zenon_L11_); trivial. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H22d); [ zenon_intro zenon_H12c | zenon_intro zenon_H22e ]. % 0.62/0.80 apply (zenon_L15_); trivial. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H22e); [ zenon_intro zenon_H230 | zenon_intro zenon_H22f ]. % 0.62/0.80 exact (zenon_H230 axiom_187). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H22f); [ zenon_intro zenon_H232 | zenon_intro zenon_H231 ]. % 0.62/0.80 generalize (axiom_36 (iV16464)). zenon_intro zenon_H233. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H233); [ zenon_intro zenon_H232; zenon_intro zenon_H236 | zenon_intro zenon_H235; zenon_intro zenon_H234 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H236); [ zenon_intro zenon_H12c | zenon_intro zenon_H237 ]. % 0.62/0.80 apply (zenon_L15_); trivial. % 0.62/0.80 apply zenon_H237. zenon_intro zenon_H178. % 0.62/0.80 generalize (axiom_35 (iV16464)). zenon_intro zenon_H176. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H176); [ zenon_intro axiom_181; zenon_intro zenon_H179 | zenon_intro zenon_H178; zenon_intro zenon_H177 ]. % 0.62/0.80 exact (axiom_181 zenon_H178). % 0.62/0.80 exact (zenon_H179 zenon_H177). % 0.62/0.80 exact (zenon_H232 zenon_H235). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H231); [ zenon_intro zenon_H124 | zenon_intro zenon_H238 ]. % 0.62/0.80 apply (zenon_L14_); trivial. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H238); [ zenon_intro zenon_H23a | zenon_intro zenon_H239 ]. % 0.62/0.80 exact (zenon_H23a axiom_198). % 0.62/0.80 generalize (axiom_27 (iV16465)). zenon_intro zenon_H23b. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H23b); [ zenon_intro zenon_H239; zenon_intro zenon_H23e | zenon_intro zenon_H23d; zenon_intro zenon_H23c ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H23e); [ zenon_intro zenon_H240 | zenon_intro zenon_H23f ]. % 0.62/0.80 apply zenon_H240. zenon_intro zenon_H17c. % 0.62/0.80 generalize (axiom_26 (iV16465)). zenon_intro zenon_H17a. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H17a); [ zenon_intro axiom_195; zenon_intro zenon_H17d | zenon_intro zenon_H17c; zenon_intro zenon_H17b ]. % 0.62/0.80 exact (axiom_195 zenon_H17c). % 0.62/0.80 exact (zenon_H17d zenon_H17b). % 0.62/0.80 exact (zenon_H23f axiom_196). % 0.62/0.80 exact (zenon_H239 zenon_H23d). % 0.62/0.80 exact (axiom_195 zenon_H17c). % 0.62/0.80 exact (axiom_181 zenon_H178). % 0.62/0.80 exact (axiom_179 zenon_H132). % 0.62/0.80 exact (axiom_174 zenon_H120). % 0.62/0.80 exact (axiom_173 zenon_H174). % 0.62/0.80 exact (axiom_161 zenon_H170). % 0.62/0.80 exact (axiom_152 zenon_H16c). % 0.62/0.80 exact (axiom_147 zenon_H10e). % 0.62/0.80 exact (axiom_137 zenon_H168). % 0.62/0.80 exact (axiom_108 zenon_H164). % 0.62/0.80 exact (axiom_103 zenon_H160). % 0.62/0.80 exact (axiom_98 zenon_Hfc). % 0.62/0.80 exact (axiom_92 zenon_H15c). % 0.62/0.80 exact (axiom_91 zenon_Hea). % 0.62/0.80 exact (axiom_76 zenon_H158). % 0.62/0.80 exact (axiom_71 zenon_H154). % 0.62/0.80 exact (axiom_70 zenon_Hd8). % 0.62/0.80 Qed. % 0.62/0.80 % SZS output end Proof % 0.62/0.80 (* END-PROOF *) % 0.62/0.80 nodes searched: 17402 % 0.62/0.80 max branch formulas: 3196 % 0.62/0.80 proof nodes created: 512 % 0.62/0.80 formulas created: 71090 % 0.62/0.80 %------------------------------------------------------------------------------