%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : KRS161+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sun Jul 17 03:39:38 EDT 2022 % Result : Theorem 0.48s 0.66s % Output : Proof 0.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : KRS161+1 : TPTP v8.1.0. Released v3.1.0. % 0.11/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n017.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Tue Jun 7 07:23:02 EDT 2022 % 0.12/0.33 % CPUTime : % 0.48/0.66 (* PROOF-FOUND *) % 0.48/0.66 % SZS status Theorem % 0.48/0.66 (* BEGIN-PROOF *) % 0.48/0.66 % SZS output start Proof % 0.48/0.66 Theorem the_axiom : ((forall X : zenon_U, ((cowlThing X)/\(~(cowlNothing X))))/\((forall X : zenon_U, ((xsd_string X)<->(~(xsd_integer X))))/\((cC130 (iV16439))/\((cC108 (iV16439))/\((cC104 (iV16439))/\((cC106 (iV16439))/\((cC28 (iV16439))/\((cowlThing (iV16439))/\((cC98 (iV16440))/\((cC80 (iV16440))/\((cC82 (iV16440))/\((cowlThing (iV16440))/\((cC38 (iV16448))/\((cowlThing (iV16448))/\((cC76 (iV16453))/\((cC62 (iV16453))/\((cowlThing (iV16453))/\((cC60 (iV16453))/\((cC56 (iV16455))/\((cC44 (iV16455))/\((cC42 (iV16455))/\((cowlThing (iV16455))/\((cC38 (iV16457))/\((cowlThing (iV16457))/\((cC50 (iV16459))/\((cC88 (iV16459))/\((cC34 (iV16459))/\((cC68 (iV16459))/\((cowlThing (iV16459))/\((cC38 (iV16460))/\((cowlThing (iV16460))/\((cC42 (iV16461))/\((cC56 (iV16461))/\((cC44 (iV16461))/\((cowlThing (iV16461))/\((cC38 (iV16462))/\((cowlThing (iV16462))/\((cC76 (iV16463))/\((cC62 (iV16463))/\((cowlThing (iV16463))/\((cC60 (iV16463))/\((cC56 (iV16464))/\((cC42 (iV16464))/\((cC44 (iV16464))/\((cowlThing (iV16464))/\((cC38 (iV16465))/\(cowlThing (iV16465)))))))))))))))))))))))))))))))))))))))))))))))). % 0.48/0.66 Proof. % 0.48/0.66 assert (zenon_L1_ : (~(cC98 (iV16440))) -> False). % 0.48/0.66 do 0 intro. intros zenon_H11f. % 0.48/0.66 generalize (axiom_146 (iV16440)). zenon_intro zenon_H120. % 0.48/0.66 apply (zenon_imply_s _ _ zenon_H120); [ zenon_intro zenon_H122 | zenon_intro zenon_H121 ]. % 0.48/0.66 exact (zenon_H122 axiom_150). % 0.48/0.66 exact (zenon_H11f zenon_H121). % 0.48/0.66 (* end of lemma zenon_L1_ *) % 0.48/0.66 assert (zenon_L2_ : (~(cC80 (iV16440))) -> False). % 0.48/0.66 do 0 intro. intros zenon_H123. % 0.48/0.66 generalize (axiom_119 (iV16440)). zenon_intro zenon_H124. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H124); [ zenon_intro zenon_H123; zenon_intro zenon_H127 | zenon_intro zenon_H126; zenon_intro zenon_H125 ]. % 0.48/0.66 generalize (axiom_143 (iV16440)). zenon_intro zenon_H128. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H128); [ zenon_intro zenon_H11f; zenon_intro zenon_H12a | zenon_intro zenon_H121; zenon_intro zenon_H129 ]. % 0.48/0.66 apply (zenon_L1_); trivial. % 0.48/0.66 apply (zenon_and_s _ _ zenon_H129). zenon_intro axiom_154. zenon_intro zenon_H12b. % 0.48/0.66 generalize (axiom_120 (iV16440)). zenon_intro zenon_H12c. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H12c); [ zenon_intro zenon_H12f; zenon_intro zenon_H12e | zenon_intro zenon_H12b; zenon_intro zenon_H12d ]. % 0.48/0.66 exact (zenon_H12f zenon_H12b). % 0.48/0.66 apply (zenon_and_s _ _ zenon_H12d). zenon_intro zenon_H126. zenon_intro axiom_158. % 0.48/0.66 generalize (axiom_119 (iV16440)). zenon_intro zenon_H124. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H124); [ zenon_intro zenon_H123; zenon_intro zenon_H127 | zenon_intro zenon_H126; zenon_intro zenon_H125 ]. % 0.48/0.66 exact (zenon_H123 zenon_H126). % 0.48/0.66 exact (zenon_H127 zenon_H125). % 0.48/0.66 exact (zenon_H123 zenon_H126). % 0.48/0.66 (* end of lemma zenon_L2_ *) % 0.48/0.66 assert (zenon_L3_ : (~(exists Y0 : zenon_U, (ra_Px18 (iV16461) Y0))) -> (~(cC60 (iV16453))) -> False). % 0.48/0.66 do 0 intro. intros zenon_H130 zenon_H131. % 0.48/0.66 generalize (axiom_91 (iV16453)). zenon_intro zenon_H132. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H132); [ zenon_intro zenon_H131; zenon_intro zenon_H135 | zenon_intro zenon_H134; zenon_intro zenon_H133 ]. % 0.48/0.66 apply zenon_H135. exists (iV16461). apply NNPP. zenon_intro zenon_H136. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H136); [ zenon_intro zenon_H138 | zenon_intro zenon_H137 ]. % 0.48/0.66 exact (zenon_H138 axiom_182). % 0.48/0.66 generalize (axiom_21 (iV16461)). zenon_intro zenon_H139. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H139); [ zenon_intro zenon_H137; zenon_intro zenon_H13a | zenon_intro axiom_237; zenon_intro zenon_H130 ]. % 0.48/0.66 exact (zenon_H13a zenon_H130). % 0.48/0.66 exact (zenon_H137 axiom_237). % 0.48/0.66 exact (zenon_H131 zenon_H134). % 0.48/0.66 (* end of lemma zenon_L3_ *) % 0.48/0.66 assert (zenon_L4_ : (~(exists Y0 : zenon_U, (ra_Px18 (iV16461) Y0))) -> (exists Y : zenon_U, (ra_Px19 (iV16453) Y)) -> (~(cC62 (iV16453))) -> False). % 0.48/0.66 do 0 intro. intros zenon_H130 zenon_H13b zenon_H13c. % 0.48/0.66 generalize (axiom_92 (iV16453)). zenon_intro zenon_H13d. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H13d); [ zenon_intro zenon_H13c; zenon_intro zenon_H140 | zenon_intro zenon_H13f; zenon_intro zenon_H13e ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H140); [ zenon_intro zenon_H131 | zenon_intro zenon_H141 ]. % 0.48/0.66 apply (zenon_L3_); trivial. % 0.48/0.66 generalize (axiom_87 (iV16453)). zenon_intro zenon_H142. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H142); [ zenon_intro zenon_H141; zenon_intro zenon_H143 | zenon_intro axiom_181; zenon_intro zenon_H13b ]. % 0.48/0.66 exact (zenon_H143 zenon_H13b). % 0.48/0.66 exact (zenon_H141 axiom_181). % 0.48/0.66 exact (zenon_H13c zenon_H13f). % 0.48/0.66 (* end of lemma zenon_L4_ *) % 0.48/0.66 assert (zenon_L5_ : (~(exists Y0 : zenon_U, (ra_Px9 (iV16460) Y0))) -> (~(cC8xcomp (iV16460))) -> False). % 0.48/0.66 do 0 intro. intros zenon_H144 zenon_H145. % 0.48/0.66 generalize (axiom_118 (iV16460)). zenon_intro zenon_H146. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H146); [ zenon_intro zenon_H145; zenon_intro zenon_H147 | zenon_intro axiom_227; zenon_intro zenon_H144 ]. % 0.48/0.66 exact (zenon_H147 zenon_H144). % 0.48/0.66 exact (zenon_H145 axiom_227). % 0.48/0.66 (* end of lemma zenon_L5_ *) % 0.48/0.66 assert (zenon_L6_ : (~(exists Y0 : zenon_U, (ra_Px9 (iV16460) Y0))) -> (~(cC42 (iV16455))) -> False). % 0.48/0.66 do 0 intro. intros zenon_H144 zenon_H148. % 0.48/0.66 generalize (axiom_65 (iV16455)). zenon_intro zenon_H149. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H149); [ zenon_intro zenon_H148; zenon_intro zenon_H14c | zenon_intro zenon_H14b; zenon_intro zenon_H14a ]. % 0.48/0.66 apply zenon_H14c. exists (iV16460). apply NNPP. zenon_intro zenon_H14d. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H14d); [ zenon_intro zenon_H14e | zenon_intro zenon_H145 ]. % 0.48/0.66 exact (zenon_H14e axiom_193). % 0.48/0.66 apply (zenon_L5_); trivial. % 0.48/0.66 exact (zenon_H148 zenon_H14b). % 0.48/0.66 (* end of lemma zenon_L6_ *) % 0.48/0.66 assert (zenon_L7_ : (exists Y : zenon_U, (ra_Px10 (iV16455) Y)) -> (~(exists Y0 : zenon_U, (ra_Px9 (iV16460) Y0))) -> (~(cC44 (iV16455))) -> False). % 0.48/0.66 do 0 intro. intros zenon_H14f zenon_H144 zenon_H150. % 0.48/0.66 generalize (axiom_66 (iV16455)). zenon_intro zenon_H151. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H151); [ zenon_intro zenon_H150; zenon_intro zenon_H154 | zenon_intro zenon_H153; zenon_intro zenon_H152 ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H154); [ zenon_intro zenon_H155 | zenon_intro zenon_H148 ]. % 0.48/0.66 generalize (axiom_64 (iV16455)). zenon_intro zenon_H156. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H156); [ zenon_intro zenon_H155; zenon_intro zenon_H157 | zenon_intro axiom_185; zenon_intro zenon_H14f ]. % 0.48/0.66 exact (zenon_H157 zenon_H14f). % 0.48/0.66 exact (zenon_H155 axiom_185). % 0.48/0.66 apply (zenon_L6_); trivial. % 0.48/0.66 exact (zenon_H150 zenon_H153). % 0.48/0.66 (* end of lemma zenon_L7_ *) % 0.48/0.66 assert (zenon_L8_ : (~(exists Y0 : zenon_U, (ra_Px9 (iV16462) Y0))) -> (~(cC42 (iV16461))) -> False). % 0.48/0.66 do 0 intro. intros zenon_H158 zenon_H159. % 0.48/0.66 generalize (axiom_65 (iV16461)). zenon_intro zenon_H15a. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H15a); [ zenon_intro zenon_H159; zenon_intro zenon_H15d | zenon_intro zenon_H15c; zenon_intro zenon_H15b ]. % 0.48/0.66 apply zenon_H15d. exists (iV16462). apply NNPP. zenon_intro zenon_H15e. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H15e); [ zenon_intro zenon_H160 | zenon_intro zenon_H15f ]. % 0.48/0.66 exact (zenon_H160 axiom_243). % 0.48/0.66 generalize (axiom_118 (iV16462)). zenon_intro zenon_H161. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H161); [ zenon_intro zenon_H15f; zenon_intro zenon_H162 | zenon_intro axiom_249; zenon_intro zenon_H158 ]. % 0.48/0.66 exact (zenon_H162 zenon_H158). % 0.48/0.66 exact (zenon_H15f axiom_249). % 0.48/0.66 exact (zenon_H159 zenon_H15c). % 0.48/0.66 (* end of lemma zenon_L8_ *) % 0.48/0.66 assert (zenon_L9_ : (exists Y : zenon_U, (ra_Px10 (iV16461) Y)) -> (~(exists Y0 : zenon_U, (ra_Px9 (iV16462) Y0))) -> (~(cC44 (iV16461))) -> False). % 0.48/0.66 do 0 intro. intros zenon_H163 zenon_H158 zenon_H164. % 0.48/0.66 generalize (axiom_66 (iV16461)). zenon_intro zenon_H165. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H165); [ zenon_intro zenon_H164; zenon_intro zenon_H168 | zenon_intro zenon_H167; zenon_intro zenon_H166 ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H168); [ zenon_intro zenon_H169 | zenon_intro zenon_H159 ]. % 0.48/0.66 generalize (axiom_64 (iV16461)). zenon_intro zenon_H16a. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H16a); [ zenon_intro zenon_H169; zenon_intro zenon_H16b | zenon_intro axiom_234; zenon_intro zenon_H163 ]. % 0.48/0.66 exact (zenon_H16b zenon_H163). % 0.48/0.66 exact (zenon_H169 axiom_234). % 0.48/0.66 apply (zenon_L8_); trivial. % 0.48/0.66 exact (zenon_H164 zenon_H167). % 0.48/0.66 (* end of lemma zenon_L9_ *) % 0.48/0.66 assert (zenon_L10_ : (~(exists Y0 : zenon_U, (ra_Px18 (iV16464) Y0))) -> (~(cC12xcomp (iV16464))) -> False). % 0.48/0.66 do 0 intro. intros zenon_H16c zenon_H16d. % 0.48/0.66 generalize (axiom_21 (iV16464)). zenon_intro zenon_H16e. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H16e); [ zenon_intro zenon_H16d; zenon_intro zenon_H16f | zenon_intro axiom_267; zenon_intro zenon_H16c ]. % 0.48/0.66 exact (zenon_H16f zenon_H16c). % 0.48/0.66 exact (zenon_H16d axiom_267). % 0.48/0.66 (* end of lemma zenon_L10_ *) % 0.48/0.66 assert (zenon_L11_ : (~(exists Y0 : zenon_U, (ra_Px18 (iV16464) Y0))) -> (~(cC60 (iV16463))) -> False). % 0.48/0.66 do 0 intro. intros zenon_H16c zenon_H170. % 0.48/0.66 generalize (axiom_91 (iV16463)). zenon_intro zenon_H171. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H171); [ zenon_intro zenon_H170; zenon_intro zenon_H174 | zenon_intro zenon_H173; zenon_intro zenon_H172 ]. % 0.48/0.66 apply zenon_H174. exists (iV16464). apply NNPP. zenon_intro zenon_H175. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H175); [ zenon_intro zenon_H176 | zenon_intro zenon_H16d ]. % 0.48/0.66 exact (zenon_H176 axiom_263). % 0.48/0.66 apply (zenon_L10_); trivial. % 0.48/0.66 exact (zenon_H170 zenon_H173). % 0.48/0.66 (* end of lemma zenon_L11_ *) % 0.48/0.66 assert (zenon_L12_ : (~(exists Y0 : zenon_U, (ra_Px18 (iV16464) Y0))) -> (exists Y : zenon_U, (ra_Px19 (iV16463) Y)) -> (~(cC62 (iV16463))) -> False). % 0.48/0.66 do 0 intro. intros zenon_H16c zenon_H177 zenon_H178. % 0.48/0.66 generalize (axiom_92 (iV16463)). zenon_intro zenon_H179. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H179); [ zenon_intro zenon_H178; zenon_intro zenon_H17c | zenon_intro zenon_H17b; zenon_intro zenon_H17a ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H17c); [ zenon_intro zenon_H170 | zenon_intro zenon_H17d ]. % 0.48/0.66 apply (zenon_L11_); trivial. % 0.48/0.66 generalize (axiom_87 (iV16463)). zenon_intro zenon_H17e. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H17e); [ zenon_intro zenon_H17d; zenon_intro zenon_H17f | zenon_intro axiom_262; zenon_intro zenon_H177 ]. % 0.48/0.66 exact (zenon_H17f zenon_H177). % 0.48/0.66 exact (zenon_H17d axiom_262). % 0.48/0.66 exact (zenon_H178 zenon_H17b). % 0.48/0.66 (* end of lemma zenon_L12_ *) % 0.48/0.66 assert (zenon_L13_ : (~(exists Y0 : zenon_U, (ra_Px9 (iV16465) Y0))) -> (~(cC8xcomp (iV16465))) -> False). % 0.48/0.66 do 0 intro. intros zenon_H180 zenon_H181. % 0.48/0.66 generalize (axiom_118 (iV16465)). zenon_intro zenon_H182. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H182); [ zenon_intro zenon_H181; zenon_intro zenon_H183 | zenon_intro axiom_280; zenon_intro zenon_H180 ]. % 0.48/0.66 exact (zenon_H183 zenon_H180). % 0.48/0.66 exact (zenon_H181 axiom_280). % 0.48/0.66 (* end of lemma zenon_L13_ *) % 0.48/0.66 assert (zenon_L14_ : (~(exists Y0 : zenon_U, (ra_Px9 (iV16465) Y0))) -> (~(cC42 (iV16464))) -> False). % 0.48/0.66 do 0 intro. intros zenon_H180 zenon_H184. % 0.48/0.66 generalize (axiom_65 (iV16464)). zenon_intro zenon_H185. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H185); [ zenon_intro zenon_H184; zenon_intro zenon_H188 | zenon_intro zenon_H187; zenon_intro zenon_H186 ]. % 0.48/0.66 apply zenon_H188. exists (iV16465). apply NNPP. zenon_intro zenon_H189. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H189); [ zenon_intro zenon_H18a | zenon_intro zenon_H181 ]. % 0.48/0.66 exact (zenon_H18a axiom_274). % 0.48/0.66 apply (zenon_L13_); trivial. % 0.48/0.66 exact (zenon_H184 zenon_H187). % 0.48/0.66 (* end of lemma zenon_L14_ *) % 0.48/0.66 assert (zenon_L15_ : (exists Y : zenon_U, (ra_Px10 (iV16464) Y)) -> (~(exists Y0 : zenon_U, (ra_Px9 (iV16465) Y0))) -> (~(cC44 (iV16464))) -> False). % 0.48/0.66 do 0 intro. intros zenon_H18b zenon_H180 zenon_H18c. % 0.48/0.66 generalize (axiom_66 (iV16464)). zenon_intro zenon_H18d. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H18d); [ zenon_intro zenon_H18c; zenon_intro zenon_H190 | zenon_intro zenon_H18f; zenon_intro zenon_H18e ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H190); [ zenon_intro zenon_H191 | zenon_intro zenon_H184 ]. % 0.48/0.66 generalize (axiom_64 (iV16464)). zenon_intro zenon_H192. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H192); [ zenon_intro zenon_H191; zenon_intro zenon_H193 | zenon_intro axiom_266; zenon_intro zenon_H18b ]. % 0.48/0.66 exact (zenon_H193 zenon_H18b). % 0.48/0.66 exact (zenon_H191 axiom_266). % 0.48/0.66 apply (zenon_L14_); trivial. % 0.48/0.66 exact (zenon_H18c zenon_H18f). % 0.48/0.66 (* end of lemma zenon_L15_ *) % 0.48/0.66 apply NNPP. intro zenon_G. % 0.48/0.66 generalize (axiom_145 (iV16439)). zenon_intro zenon_H194. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H194); [ zenon_intro zenon_H197; zenon_intro zenon_H196 | zenon_intro axiom_149; zenon_intro zenon_H195 ]. % 0.48/0.66 exact (zenon_H197 axiom_149). % 0.48/0.66 apply (zenon_and_s _ _ zenon_H195). zenon_intro zenon_H199. zenon_intro zenon_H198. % 0.48/0.66 generalize (axiom_12 (iV16439)). zenon_intro zenon_H19a. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H19a); [ zenon_intro zenon_H19d; zenon_intro zenon_H19c | zenon_intro zenon_H199; zenon_intro zenon_H19b ]. % 0.48/0.66 exact (zenon_H19d zenon_H199). % 0.48/0.66 apply (zenon_and_s _ _ zenon_H19b). zenon_intro zenon_H19f. zenon_intro zenon_H19e. % 0.48/0.66 generalize (axiom_44 (iV16439)). zenon_intro zenon_H1a0. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1a0); [ zenon_intro zenon_H1a3; zenon_intro zenon_H1a2 | zenon_intro zenon_H19f; zenon_intro zenon_H1a1 ]. % 0.48/0.66 exact (zenon_H1a3 zenon_H19f). % 0.48/0.66 generalize (axiom_11 (iV16439)). zenon_intro zenon_H1a4. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1a4); [ zenon_intro zenon_H1a7; zenon_intro zenon_H1a6 | zenon_intro zenon_H19e; zenon_intro zenon_H1a5 ]. % 0.48/0.66 exact (zenon_H1a7 zenon_H19e). % 0.48/0.66 apply (zenon_and_s _ _ zenon_H1a5). zenon_intro zenon_H1a8. zenon_intro axiom_148. % 0.48/0.66 generalize (axiom_10 (iV16439)). zenon_intro zenon_H1a9. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1a9); [ zenon_intro zenon_H1ac; zenon_intro zenon_H1ab | zenon_intro zenon_H1a8; zenon_intro zenon_H1aa ]. % 0.48/0.66 exact (zenon_H1ac zenon_H1a8). % 0.48/0.66 generalize (axiom_29 (iV16439)). zenon_intro zenon_H1ad. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1ad); [ zenon_intro zenon_H1b0; zenon_intro zenon_H1af | zenon_intro zenon_H198; zenon_intro zenon_H1ae ]. % 0.48/0.66 exact (zenon_H1b0 zenon_H198). % 0.48/0.66 generalize (axiom_116 (iV16440)). zenon_intro zenon_H1b1. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1b1); [ zenon_intro zenon_H1b4; zenon_intro zenon_H1b3 | zenon_intro axiom_158; zenon_intro zenon_H1b2 ]. % 0.48/0.66 exact (zenon_H1b4 axiom_158). % 0.48/0.66 generalize (axiom_56 (iV16448)). zenon_intro zenon_H1b5. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1b5); [ zenon_intro zenon_H1b8; zenon_intro zenon_H1b7 | zenon_intro axiom_168; zenon_intro zenon_H1b6 ]. % 0.48/0.66 exact (zenon_H1b8 axiom_168). % 0.48/0.66 generalize (axiom_110 (iV16453)). zenon_intro zenon_H1b9. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1b9); [ zenon_intro zenon_H1bc; zenon_intro zenon_H1bb | zenon_intro axiom_174; zenon_intro zenon_H1ba ]. % 0.48/0.66 exact (zenon_H1bc axiom_174). % 0.48/0.66 generalize (axiom_87 (iV16453)). zenon_intro zenon_H142. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H142); [ zenon_intro zenon_H141; zenon_intro zenon_H143 | zenon_intro axiom_181; zenon_intro zenon_H13b ]. % 0.48/0.66 exact (zenon_H141 axiom_181). % 0.48/0.66 generalize (axiom_64 (iV16455)). zenon_intro zenon_H156. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H156); [ zenon_intro zenon_H155; zenon_intro zenon_H157 | zenon_intro axiom_185; zenon_intro zenon_H14f ]. % 0.48/0.66 exact (zenon_H155 axiom_185). % 0.48/0.66 generalize (axiom_81 (iV16455)). zenon_intro zenon_H1bd. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1bd); [ zenon_intro zenon_H1c0; zenon_intro zenon_H1bf | zenon_intro axiom_190; zenon_intro zenon_H1be ]. % 0.48/0.66 exact (zenon_H1c0 axiom_190). % 0.48/0.66 generalize (axiom_56 (iV16457)). zenon_intro zenon_H1c1. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1c1); [ zenon_intro zenon_H1c4; zenon_intro zenon_H1c3 | zenon_intro axiom_201; zenon_intro zenon_H1c2 ]. % 0.48/0.66 exact (zenon_H1c4 axiom_201). % 0.48/0.66 generalize (axiom_47 (iV16459)). zenon_intro zenon_H1c5. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1c5); [ zenon_intro zenon_H1c8; zenon_intro zenon_H1c7 | zenon_intro axiom_209; zenon_intro zenon_H1c6 ]. % 0.48/0.66 exact (zenon_H1c8 axiom_209). % 0.48/0.66 generalize (axiom_123 (iV16459)). zenon_intro zenon_H1c9. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1c9); [ zenon_intro zenon_H1cc; zenon_intro zenon_H1cb | zenon_intro axiom_210; zenon_intro zenon_H1ca ]. % 0.48/0.66 exact (zenon_H1cc axiom_210). % 0.48/0.66 generalize (axiom_69 (iV16459)). zenon_intro zenon_H1cd. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1cd); [ zenon_intro zenon_H1d0; zenon_intro zenon_H1cf | zenon_intro axiom_212; zenon_intro zenon_H1ce ]. % 0.48/0.66 exact (zenon_H1d0 axiom_212). % 0.48/0.66 generalize (axiom_95 (iV16459)). zenon_intro zenon_H1d1. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1d1); [ zenon_intro zenon_H1d4; zenon_intro zenon_H1d3 | zenon_intro axiom_213; zenon_intro zenon_H1d2 ]. % 0.48/0.66 exact (zenon_H1d4 axiom_213). % 0.48/0.66 generalize (axiom_126 (iV16459)). zenon_intro zenon_H1d5. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1d5); [ zenon_intro zenon_H1d8; zenon_intro zenon_H1d7 | zenon_intro axiom_215; zenon_intro zenon_H1d6 ]. % 0.48/0.66 exact (zenon_H1d8 axiom_215). % 0.48/0.66 generalize (axiom_50 (iV16459)). zenon_intro zenon_H1d9. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1d9); [ zenon_intro zenon_H1dc; zenon_intro zenon_H1db | zenon_intro axiom_216; zenon_intro zenon_H1da ]. % 0.48/0.66 exact (zenon_H1dc axiom_216). % 0.48/0.66 generalize (axiom_72 (iV16459)). zenon_intro zenon_H1dd. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1dd); [ zenon_intro zenon_H1e0; zenon_intro zenon_H1df | zenon_intro axiom_217; zenon_intro zenon_H1de ]. % 0.48/0.66 exact (zenon_H1e0 axiom_217). % 0.48/0.66 generalize (axiom_98 (iV16459)). zenon_intro zenon_H1e1. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1e1); [ zenon_intro zenon_H1e4; zenon_intro zenon_H1e3 | zenon_intro axiom_221; zenon_intro zenon_H1e2 ]. % 0.48/0.66 exact (zenon_H1e4 axiom_221). % 0.48/0.66 generalize (axiom_118 (iV16460)). zenon_intro zenon_H146. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H146); [ zenon_intro zenon_H145; zenon_intro zenon_H147 | zenon_intro axiom_227; zenon_intro zenon_H144 ]. % 0.48/0.66 exact (zenon_H145 axiom_227). % 0.48/0.66 generalize (axiom_56 (iV16460)). zenon_intro zenon_H1e5. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1e5); [ zenon_intro zenon_H1e8; zenon_intro zenon_H1e7 | zenon_intro axiom_228; zenon_intro zenon_H1e6 ]. % 0.48/0.66 exact (zenon_H1e8 axiom_228). % 0.48/0.66 generalize (axiom_64 (iV16461)). zenon_intro zenon_H16a. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H16a); [ zenon_intro zenon_H169; zenon_intro zenon_H16b | zenon_intro axiom_234; zenon_intro zenon_H163 ]. % 0.48/0.66 exact (zenon_H169 axiom_234). % 0.48/0.66 generalize (axiom_21 (iV16461)). zenon_intro zenon_H139. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H139); [ zenon_intro zenon_H137; zenon_intro zenon_H13a | zenon_intro axiom_237; zenon_intro zenon_H130 ]. % 0.48/0.66 exact (zenon_H137 axiom_237). % 0.48/0.66 generalize (axiom_81 (iV16461)). zenon_intro zenon_H1e9. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1e9); [ zenon_intro zenon_H1ec; zenon_intro zenon_H1eb | zenon_intro axiom_240; zenon_intro zenon_H1ea ]. % 0.48/0.66 exact (zenon_H1ec axiom_240). % 0.48/0.66 generalize (axiom_118 (iV16462)). zenon_intro zenon_H161. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H161); [ zenon_intro zenon_H15f; zenon_intro zenon_H162 | zenon_intro axiom_249; zenon_intro zenon_H158 ]. % 0.48/0.66 exact (zenon_H15f axiom_249). % 0.48/0.66 generalize (axiom_56 (iV16462)). zenon_intro zenon_H1ed. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1ed); [ zenon_intro zenon_H1f0; zenon_intro zenon_H1ef | zenon_intro axiom_252; zenon_intro zenon_H1ee ]. % 0.48/0.66 exact (zenon_H1f0 axiom_252). % 0.48/0.66 generalize (axiom_110 (iV16463)). zenon_intro zenon_H1f1. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1f1); [ zenon_intro zenon_H1f4; zenon_intro zenon_H1f3 | zenon_intro axiom_255; zenon_intro zenon_H1f2 ]. % 0.48/0.66 exact (zenon_H1f4 axiom_255). % 0.48/0.66 generalize (axiom_87 (iV16463)). zenon_intro zenon_H17e. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H17e); [ zenon_intro zenon_H17d; zenon_intro zenon_H17f | zenon_intro axiom_262; zenon_intro zenon_H177 ]. % 0.48/0.66 exact (zenon_H17d axiom_262). % 0.48/0.66 generalize (axiom_64 (iV16464)). zenon_intro zenon_H192. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H192); [ zenon_intro zenon_H191; zenon_intro zenon_H193 | zenon_intro axiom_266; zenon_intro zenon_H18b ]. % 0.48/0.66 exact (zenon_H191 axiom_266). % 0.48/0.66 generalize (axiom_21 (iV16464)). zenon_intro zenon_H16e. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H16e); [ zenon_intro zenon_H16d; zenon_intro zenon_H16f | zenon_intro axiom_267; zenon_intro zenon_H16c ]. % 0.48/0.66 exact (zenon_H16d axiom_267). % 0.48/0.66 generalize (axiom_81 (iV16464)). zenon_intro zenon_H1f5. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1f5); [ zenon_intro zenon_H1f8; zenon_intro zenon_H1f7 | zenon_intro axiom_270; zenon_intro zenon_H1f6 ]. % 0.48/0.66 exact (zenon_H1f8 axiom_270). % 0.48/0.66 generalize (axiom_118 (iV16465)). zenon_intro zenon_H182. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H182); [ zenon_intro zenon_H181; zenon_intro zenon_H183 | zenon_intro axiom_280; zenon_intro zenon_H180 ]. % 0.48/0.66 exact (zenon_H181 axiom_280). % 0.48/0.66 generalize (axiom_56 (iV16465)). zenon_intro zenon_H1f9. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1f9); [ zenon_intro zenon_H1fc; zenon_intro zenon_H1fb | zenon_intro axiom_282; zenon_intro zenon_H1fa ]. % 0.48/0.66 exact (zenon_H1fc axiom_282). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_G); [ zenon_intro zenon_H1fe | zenon_intro zenon_H1fd ]. % 0.48/0.66 exact (zenon_H1fe axiom_0). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H1fd); [ zenon_intro zenon_H200 | zenon_intro zenon_H1ff ]. % 0.48/0.66 exact (zenon_H200 axiom_1). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H1ff); [ zenon_intro zenon_H1b0 | zenon_intro zenon_H201 ]. % 0.48/0.66 generalize (axiom_29 (iV16439)). zenon_intro zenon_H1ad. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1ad); [ zenon_intro zenon_H1b0; zenon_intro zenon_H1af | zenon_intro zenon_H198; zenon_intro zenon_H1ae ]. % 0.48/0.66 exact (zenon_H1af zenon_H1ae). % 0.48/0.66 exact (zenon_H1b0 zenon_H198). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H201); [ zenon_intro zenon_H19d | zenon_intro zenon_H202 ]. % 0.48/0.66 generalize (axiom_12 (iV16439)). zenon_intro zenon_H19a. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H19a); [ zenon_intro zenon_H19d; zenon_intro zenon_H19c | zenon_intro zenon_H199; zenon_intro zenon_H19b ]. % 0.48/0.66 exact (zenon_H19c zenon_H19b). % 0.48/0.66 exact (zenon_H19d zenon_H199). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H202); [ zenon_intro zenon_H1ac | zenon_intro zenon_H203 ]. % 0.48/0.66 generalize (axiom_10 (iV16439)). zenon_intro zenon_H1a9. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1a9); [ zenon_intro zenon_H1ac; zenon_intro zenon_H1ab | zenon_intro zenon_H1a8; zenon_intro zenon_H1aa ]. % 0.48/0.66 exact (zenon_H1ab zenon_H1aa). % 0.48/0.66 exact (zenon_H1ac zenon_H1a8). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H203); [ zenon_intro zenon_H1a7 | zenon_intro zenon_H204 ]. % 0.48/0.66 generalize (axiom_11 (iV16439)). zenon_intro zenon_H1a4. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1a4); [ zenon_intro zenon_H1a7; zenon_intro zenon_H1a6 | zenon_intro zenon_H19e; zenon_intro zenon_H1a5 ]. % 0.48/0.66 exact (zenon_H1a6 zenon_H1a5). % 0.48/0.66 exact (zenon_H1a7 zenon_H19e). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H204); [ zenon_intro zenon_H1a3 | zenon_intro zenon_H205 ]. % 0.48/0.66 generalize (axiom_44 (iV16439)). zenon_intro zenon_H1a0. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1a0); [ zenon_intro zenon_H1a3; zenon_intro zenon_H1a2 | zenon_intro zenon_H19f; zenon_intro zenon_H1a1 ]. % 0.48/0.66 exact (zenon_H1a2 zenon_H1a1). % 0.48/0.66 exact (zenon_H1a3 zenon_H19f). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H205); [ zenon_intro zenon_H207 | zenon_intro zenon_H206 ]. % 0.48/0.66 exact (zenon_H207 axiom_147). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H206); [ zenon_intro zenon_H11f | zenon_intro zenon_H208 ]. % 0.48/0.66 apply (zenon_L1_); trivial. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H208); [ zenon_intro zenon_H123 | zenon_intro zenon_H209 ]. % 0.48/0.66 apply (zenon_L2_); trivial. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H209); [ zenon_intro zenon_H12f | zenon_intro zenon_H20a ]. % 0.48/0.66 generalize (axiom_120 (iV16440)). zenon_intro zenon_H12c. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H12c); [ zenon_intro zenon_H12f; zenon_intro zenon_H12e | zenon_intro zenon_H12b; zenon_intro zenon_H12d ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H12e); [ zenon_intro zenon_H123 | zenon_intro zenon_H1b4 ]. % 0.48/0.66 apply (zenon_L2_); trivial. % 0.48/0.66 generalize (axiom_116 (iV16440)). zenon_intro zenon_H1b1. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1b1); [ zenon_intro zenon_H1b4; zenon_intro zenon_H1b3 | zenon_intro axiom_158; zenon_intro zenon_H1b2 ]. % 0.48/0.66 exact (zenon_H1b3 zenon_H1b2). % 0.48/0.66 exact (zenon_H1b4 axiom_158). % 0.48/0.66 exact (zenon_H12f zenon_H12b). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H20a); [ zenon_intro zenon_H20c | zenon_intro zenon_H20b ]. % 0.48/0.66 exact (zenon_H20c axiom_153). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H20b); [ zenon_intro zenon_H20e | zenon_intro zenon_H20d ]. % 0.48/0.66 generalize (axiom_57 (iV16448)). zenon_intro zenon_H20f. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H20f); [ zenon_intro zenon_H20e; zenon_intro zenon_H212 | zenon_intro zenon_H211; zenon_intro zenon_H210 ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H212); [ zenon_intro zenon_H213 | zenon_intro zenon_H1b8 ]. % 0.48/0.66 exact (zenon_H213 axiom_163). % 0.48/0.66 generalize (axiom_56 (iV16448)). zenon_intro zenon_H1b5. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1b5); [ zenon_intro zenon_H1b8; zenon_intro zenon_H1b7 | zenon_intro axiom_168; zenon_intro zenon_H1b6 ]. % 0.48/0.66 exact (zenon_H1b7 zenon_H1b6). % 0.48/0.66 exact (zenon_H1b8 axiom_168). % 0.48/0.66 exact (zenon_H20e zenon_H211). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H20d); [ zenon_intro zenon_H215 | zenon_intro zenon_H214 ]. % 0.48/0.66 exact (zenon_H215 axiom_162). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H214); [ zenon_intro zenon_H217 | zenon_intro zenon_H216 ]. % 0.48/0.66 generalize (axiom_112 (iV16453)). zenon_intro zenon_H218. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H218); [ zenon_intro zenon_H217; zenon_intro zenon_H21b | zenon_intro zenon_H21a; zenon_intro zenon_H219 ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H21b); [ zenon_intro zenon_H1bc | zenon_intro zenon_H13c ]. % 0.48/0.66 generalize (axiom_110 (iV16453)). zenon_intro zenon_H1b9. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1b9); [ zenon_intro zenon_H1bc; zenon_intro zenon_H1bb | zenon_intro axiom_174; zenon_intro zenon_H1ba ]. % 0.48/0.66 exact (zenon_H1bb zenon_H1ba). % 0.48/0.66 exact (zenon_H1bc axiom_174). % 0.48/0.66 apply (zenon_L4_); trivial. % 0.48/0.66 exact (zenon_H217 zenon_H21a). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H216); [ zenon_intro zenon_H13c | zenon_intro zenon_H21c ]. % 0.48/0.66 apply (zenon_L4_); trivial. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H21c); [ zenon_intro zenon_H21e | zenon_intro zenon_H21d ]. % 0.48/0.66 exact (zenon_H21e axiom_175). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H21d); [ zenon_intro zenon_H131 | zenon_intro zenon_H21f ]. % 0.48/0.66 apply (zenon_L3_); trivial. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H21f); [ zenon_intro zenon_H221 | zenon_intro zenon_H220 ]. % 0.48/0.66 generalize (axiom_82 (iV16455)). zenon_intro zenon_H222. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H222); [ zenon_intro zenon_H221; zenon_intro zenon_H225 | zenon_intro zenon_H224; zenon_intro zenon_H223 ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H225); [ zenon_intro zenon_H1c0 | zenon_intro zenon_H150 ]. % 0.48/0.66 generalize (axiom_81 (iV16455)). zenon_intro zenon_H1bd. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1bd); [ zenon_intro zenon_H1c0; zenon_intro zenon_H1bf | zenon_intro axiom_190; zenon_intro zenon_H1be ]. % 0.48/0.66 exact (zenon_H1bf zenon_H1be). % 0.48/0.66 exact (zenon_H1c0 axiom_190). % 0.48/0.66 apply (zenon_L7_); trivial. % 0.48/0.66 exact (zenon_H221 zenon_H224). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H220); [ zenon_intro zenon_H150 | zenon_intro zenon_H226 ]. % 0.48/0.66 apply (zenon_L7_); trivial. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H226); [ zenon_intro zenon_H148 | zenon_intro zenon_H227 ]. % 0.48/0.66 apply (zenon_L6_); trivial. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H227); [ zenon_intro zenon_H229 | zenon_intro zenon_H228 ]. % 0.48/0.66 exact (zenon_H229 axiom_184). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H228); [ zenon_intro zenon_H22b | zenon_intro zenon_H22a ]. % 0.48/0.66 generalize (axiom_57 (iV16457)). zenon_intro zenon_H22c. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H22c); [ zenon_intro zenon_H22b; zenon_intro zenon_H22f | zenon_intro zenon_H22e; zenon_intro zenon_H22d ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H22f); [ zenon_intro zenon_H230 | zenon_intro zenon_H1c4 ]. % 0.48/0.66 exact (zenon_H230 axiom_197). % 0.48/0.66 generalize (axiom_56 (iV16457)). zenon_intro zenon_H1c1. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1c1); [ zenon_intro zenon_H1c4; zenon_intro zenon_H1c3 | zenon_intro axiom_201; zenon_intro zenon_H1c2 ]. % 0.48/0.66 exact (zenon_H1c3 zenon_H1c2). % 0.48/0.66 exact (zenon_H1c4 axiom_201). % 0.48/0.66 exact (zenon_H22b zenon_H22e). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H22a); [ zenon_intro zenon_H232 | zenon_intro zenon_H231 ]. % 0.48/0.66 exact (zenon_H232 axiom_195). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H231); [ zenon_intro zenon_H234 | zenon_intro zenon_H233 ]. % 0.48/0.66 generalize (axiom_73 (iV16459)). zenon_intro zenon_H235. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H235); [ zenon_intro zenon_H234; zenon_intro zenon_H238 | zenon_intro zenon_H237; zenon_intro zenon_H236 ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H238); [ zenon_intro zenon_H1d0 | zenon_intro zenon_H1e0 ]. % 0.48/0.66 generalize (axiom_69 (iV16459)). zenon_intro zenon_H1cd. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1cd); [ zenon_intro zenon_H1d0; zenon_intro zenon_H1cf | zenon_intro axiom_212; zenon_intro zenon_H1ce ]. % 0.48/0.66 exact (zenon_H1cf zenon_H1ce). % 0.48/0.66 exact (zenon_H1d0 axiom_212). % 0.48/0.66 generalize (axiom_72 (iV16459)). zenon_intro zenon_H1dd. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1dd); [ zenon_intro zenon_H1e0; zenon_intro zenon_H1df | zenon_intro axiom_217; zenon_intro zenon_H1de ]. % 0.48/0.66 exact (zenon_H1df zenon_H1de). % 0.48/0.66 exact (zenon_H1e0 axiom_217). % 0.48/0.66 exact (zenon_H234 zenon_H237). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H233); [ zenon_intro zenon_H23a | zenon_intro zenon_H239 ]. % 0.48/0.66 generalize (axiom_128 (iV16459)). zenon_intro zenon_H23b. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H23b); [ zenon_intro zenon_H23a; zenon_intro zenon_H23e | zenon_intro zenon_H23d; zenon_intro zenon_H23c ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H23e); [ zenon_intro zenon_H1cc | zenon_intro zenon_H1d8 ]. % 0.48/0.66 generalize (axiom_123 (iV16459)). zenon_intro zenon_H1c9. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1c9); [ zenon_intro zenon_H1cc; zenon_intro zenon_H1cb | zenon_intro axiom_210; zenon_intro zenon_H1ca ]. % 0.48/0.66 exact (zenon_H1cb zenon_H1ca). % 0.48/0.66 exact (zenon_H1cc axiom_210). % 0.48/0.66 generalize (axiom_126 (iV16459)). zenon_intro zenon_H1d5. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1d5); [ zenon_intro zenon_H1d8; zenon_intro zenon_H1d7 | zenon_intro axiom_215; zenon_intro zenon_H1d6 ]. % 0.48/0.66 exact (zenon_H1d7 zenon_H1d6). % 0.48/0.66 exact (zenon_H1d8 axiom_215). % 0.48/0.66 exact (zenon_H23a zenon_H23d). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H239); [ zenon_intro zenon_H240 | zenon_intro zenon_H23f ]. % 0.48/0.66 generalize (axiom_52 (iV16459)). zenon_intro zenon_H241. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H241); [ zenon_intro zenon_H240; zenon_intro zenon_H244 | zenon_intro zenon_H243; zenon_intro zenon_H242 ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H244); [ zenon_intro zenon_H1c8 | zenon_intro zenon_H1dc ]. % 0.48/0.66 generalize (axiom_47 (iV16459)). zenon_intro zenon_H1c5. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1c5); [ zenon_intro zenon_H1c8; zenon_intro zenon_H1c7 | zenon_intro axiom_209; zenon_intro zenon_H1c6 ]. % 0.48/0.66 exact (zenon_H1c7 zenon_H1c6). % 0.48/0.66 exact (zenon_H1c8 axiom_209). % 0.48/0.66 generalize (axiom_50 (iV16459)). zenon_intro zenon_H1d9. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1d9); [ zenon_intro zenon_H1dc; zenon_intro zenon_H1db | zenon_intro axiom_216; zenon_intro zenon_H1da ]. % 0.48/0.66 exact (zenon_H1db zenon_H1da). % 0.48/0.66 exact (zenon_H1dc axiom_216). % 0.48/0.66 exact (zenon_H240 zenon_H243). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H23f); [ zenon_intro zenon_H246 | zenon_intro zenon_H245 ]. % 0.48/0.66 generalize (axiom_100 (iV16459)). zenon_intro zenon_H247. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H247); [ zenon_intro zenon_H246; zenon_intro zenon_H24a | zenon_intro zenon_H249; zenon_intro zenon_H248 ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H24a); [ zenon_intro zenon_H1d4 | zenon_intro zenon_H1e4 ]. % 0.48/0.66 generalize (axiom_95 (iV16459)). zenon_intro zenon_H1d1. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1d1); [ zenon_intro zenon_H1d4; zenon_intro zenon_H1d3 | zenon_intro axiom_213; zenon_intro zenon_H1d2 ]. % 0.48/0.66 exact (zenon_H1d3 zenon_H1d2). % 0.48/0.66 exact (zenon_H1d4 axiom_213). % 0.48/0.66 generalize (axiom_98 (iV16459)). zenon_intro zenon_H1e1. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1e1); [ zenon_intro zenon_H1e4; zenon_intro zenon_H1e3 | zenon_intro axiom_221; zenon_intro zenon_H1e2 ]. % 0.48/0.66 exact (zenon_H1e3 zenon_H1e2). % 0.48/0.66 exact (zenon_H1e4 axiom_221). % 0.48/0.66 exact (zenon_H246 zenon_H249). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H245); [ zenon_intro zenon_H24c | zenon_intro zenon_H24b ]. % 0.48/0.66 exact (zenon_H24c axiom_205). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H24b); [ zenon_intro zenon_H24e | zenon_intro zenon_H24d ]. % 0.48/0.66 generalize (axiom_57 (iV16460)). zenon_intro zenon_H24f. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H24f); [ zenon_intro zenon_H24e; zenon_intro zenon_H252 | zenon_intro zenon_H251; zenon_intro zenon_H250 ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H252); [ zenon_intro zenon_H253 | zenon_intro zenon_H1e8 ]. % 0.48/0.66 exact (zenon_H253 axiom_225). % 0.48/0.66 generalize (axiom_56 (iV16460)). zenon_intro zenon_H1e5. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1e5); [ zenon_intro zenon_H1e8; zenon_intro zenon_H1e7 | zenon_intro axiom_228; zenon_intro zenon_H1e6 ]. % 0.48/0.66 exact (zenon_H1e7 zenon_H1e6). % 0.48/0.66 exact (zenon_H1e8 axiom_228). % 0.48/0.66 exact (zenon_H24e zenon_H251). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H24d); [ zenon_intro zenon_H255 | zenon_intro zenon_H254 ]. % 0.48/0.66 exact (zenon_H255 axiom_223). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H254); [ zenon_intro zenon_H159 | zenon_intro zenon_H256 ]. % 0.48/0.66 apply (zenon_L8_); trivial. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H256); [ zenon_intro zenon_H258 | zenon_intro zenon_H257 ]. % 0.48/0.66 generalize (axiom_82 (iV16461)). zenon_intro zenon_H259. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H259); [ zenon_intro zenon_H258; zenon_intro zenon_H25c | zenon_intro zenon_H25b; zenon_intro zenon_H25a ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H25c); [ zenon_intro zenon_H1ec | zenon_intro zenon_H164 ]. % 0.48/0.66 generalize (axiom_81 (iV16461)). zenon_intro zenon_H1e9. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1e9); [ zenon_intro zenon_H1ec; zenon_intro zenon_H1eb | zenon_intro axiom_240; zenon_intro zenon_H1ea ]. % 0.48/0.66 exact (zenon_H1eb zenon_H1ea). % 0.48/0.66 exact (zenon_H1ec axiom_240). % 0.48/0.66 apply (zenon_L9_); trivial. % 0.48/0.66 exact (zenon_H258 zenon_H25b). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H257); [ zenon_intro zenon_H164 | zenon_intro zenon_H25d ]. % 0.48/0.66 apply (zenon_L9_); trivial. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H25d); [ zenon_intro zenon_H25f | zenon_intro zenon_H25e ]. % 0.48/0.66 exact (zenon_H25f axiom_233). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H25e); [ zenon_intro zenon_H261 | zenon_intro zenon_H260 ]. % 0.48/0.66 generalize (axiom_57 (iV16462)). zenon_intro zenon_H262. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H262); [ zenon_intro zenon_H261; zenon_intro zenon_H265 | zenon_intro zenon_H264; zenon_intro zenon_H263 ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H265); [ zenon_intro zenon_H266 | zenon_intro zenon_H1f0 ]. % 0.48/0.66 exact (zenon_H266 axiom_247). % 0.48/0.66 generalize (axiom_56 (iV16462)). zenon_intro zenon_H1ed. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1ed); [ zenon_intro zenon_H1f0; zenon_intro zenon_H1ef | zenon_intro axiom_252; zenon_intro zenon_H1ee ]. % 0.48/0.66 exact (zenon_H1ef zenon_H1ee). % 0.48/0.66 exact (zenon_H1f0 axiom_252). % 0.48/0.66 exact (zenon_H261 zenon_H264). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H260); [ zenon_intro zenon_H268 | zenon_intro zenon_H267 ]. % 0.48/0.66 exact (zenon_H268 axiom_246). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H267); [ zenon_intro zenon_H26a | zenon_intro zenon_H269 ]. % 0.48/0.66 generalize (axiom_112 (iV16463)). zenon_intro zenon_H26b. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H26b); [ zenon_intro zenon_H26a; zenon_intro zenon_H26e | zenon_intro zenon_H26d; zenon_intro zenon_H26c ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H26e); [ zenon_intro zenon_H1f4 | zenon_intro zenon_H178 ]. % 0.48/0.66 generalize (axiom_110 (iV16463)). zenon_intro zenon_H1f1. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1f1); [ zenon_intro zenon_H1f4; zenon_intro zenon_H1f3 | zenon_intro axiom_255; zenon_intro zenon_H1f2 ]. % 0.48/0.66 exact (zenon_H1f3 zenon_H1f2). % 0.48/0.66 exact (zenon_H1f4 axiom_255). % 0.48/0.66 apply (zenon_L12_); trivial. % 0.48/0.66 exact (zenon_H26a zenon_H26d). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H269); [ zenon_intro zenon_H178 | zenon_intro zenon_H26f ]. % 0.48/0.66 apply (zenon_L12_); trivial. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H26f); [ zenon_intro zenon_H271 | zenon_intro zenon_H270 ]. % 0.48/0.66 exact (zenon_H271 axiom_256). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H270); [ zenon_intro zenon_H170 | zenon_intro zenon_H272 ]. % 0.48/0.66 apply (zenon_L11_); trivial. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H272); [ zenon_intro zenon_H274 | zenon_intro zenon_H273 ]. % 0.48/0.66 generalize (axiom_82 (iV16464)). zenon_intro zenon_H275. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H275); [ zenon_intro zenon_H274; zenon_intro zenon_H278 | zenon_intro zenon_H277; zenon_intro zenon_H276 ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H278); [ zenon_intro zenon_H1f8 | zenon_intro zenon_H18c ]. % 0.48/0.66 generalize (axiom_81 (iV16464)). zenon_intro zenon_H1f5. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1f5); [ zenon_intro zenon_H1f8; zenon_intro zenon_H1f7 | zenon_intro axiom_270; zenon_intro zenon_H1f6 ]. % 0.48/0.66 exact (zenon_H1f7 zenon_H1f6). % 0.48/0.66 exact (zenon_H1f8 axiom_270). % 0.48/0.66 apply (zenon_L15_); trivial. % 0.48/0.66 exact (zenon_H274 zenon_H277). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H273); [ zenon_intro zenon_H184 | zenon_intro zenon_H279 ]. % 0.48/0.66 apply (zenon_L14_); trivial. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H279); [ zenon_intro zenon_H18c | zenon_intro zenon_H27a ]. % 0.48/0.66 apply (zenon_L15_); trivial. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H27a); [ zenon_intro zenon_H27c | zenon_intro zenon_H27b ]. % 0.48/0.66 exact (zenon_H27c axiom_264). % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H27b); [ zenon_intro zenon_H27e | zenon_intro zenon_H27d ]. % 0.48/0.66 generalize (axiom_57 (iV16465)). zenon_intro zenon_H27f. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H27f); [ zenon_intro zenon_H27e; zenon_intro zenon_H282 | zenon_intro zenon_H281; zenon_intro zenon_H280 ]. % 0.48/0.66 apply (zenon_notand_s _ _ zenon_H282); [ zenon_intro zenon_H283 | zenon_intro zenon_H1fc ]. % 0.48/0.66 exact (zenon_H283 axiom_277). % 0.48/0.66 generalize (axiom_56 (iV16465)). zenon_intro zenon_H1f9. % 0.48/0.66 apply (zenon_equiv_s _ _ zenon_H1f9); [ zenon_intro zenon_H1fc; zenon_intro zenon_H1fb | zenon_intro axiom_282; zenon_intro zenon_H1fa ]. % 0.48/0.66 exact (zenon_H1fb zenon_H1fa). % 0.48/0.66 exact (zenon_H1fc axiom_282). % 0.48/0.66 exact (zenon_H27e zenon_H281). % 0.48/0.66 exact (zenon_H27d axiom_276). % 0.48/0.66 Qed. % 0.48/0.66 % SZS output end Proof % 0.48/0.66 (* END-PROOF *) % 0.48/0.66 nodes searched: 14095 % 0.48/0.66 max branch formulas: 1289 % 0.48/0.66 proof nodes created: 344 % 0.48/0.66 formulas created: 26204 % 0.48/0.66 %------------------------------------------------------------------------------