%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR040+1 : TPTP v8.1.0. Released v3.4.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 : Sat Jul 16 00:02:01 EDT 2022 % Result : Theorem 6.25s 6.45s % Output : Proof 6.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : CSR040+1 : TPTP v8.1.0. Released v3.4.0. % 0.06/0.12 % Command : run_zenon %s %d % 0.13/0.33 % Computer : n019.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Sat Jun 11 15:01:40 EDT 2022 % 0.13/0.34 % CPUTime : % 6.25/6.45 (* PROOF-FOUND *) % 6.25/6.45 % SZS status Theorem % 6.25/6.45 (* BEGIN-PROOF *) % 6.25/6.45 % SZS output start Proof % 6.25/6.45 Theorem query40 : ((mtvisible (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn (s_http_wwwthedailybulletincompostcardsmar9chtm))) (c_translation_14)))->(~(tptpcol_15_109185 (c_tptpcol_16_62187)))). % 6.25/6.45 Proof. % 6.25/6.45 assert (zenon_L1_ : (~(fixedordercollection (c_tptpcol_16_62187))) -> False). % 6.25/6.45 do 0 intro. intros zenon_H86. % 6.25/6.45 generalize (just4 (c_tptpcol_16_62187)). zenon_intro zenon_H87. % 6.25/6.45 apply (zenon_imply_s _ _ zenon_H87); [ zenon_intro zenon_H89 | zenon_intro zenon_H88 ]. % 6.25/6.45 exact (zenon_H89 just17). % 6.25/6.45 exact (zenon_H86 zenon_H88). % 6.25/6.45 (* end of lemma zenon_L1_ *) % 6.25/6.45 assert (zenon_L2_ : (~((c_tptpcol_12_109157) = (c_tptpcol_12_109157))) -> False). % 6.25/6.45 do 0 intro. intros zenon_H8a. % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 (* end of lemma zenon_L2_ *) % 6.25/6.45 assert (zenon_L3_ : (~((c_tptpcol_10_109061) = (c_tptpcol_10_109061))) -> False). % 6.25/6.45 do 0 intro. intros zenon_H8b. % 6.25/6.45 apply zenon_H8b. apply refl_equal. % 6.25/6.45 (* end of lemma zenon_L3_ *) % 6.25/6.45 assert (zenon_L4_ : (~((c_tptpcol_9_109060) = (c_tptpcol_9_109060))) -> False). % 6.25/6.45 do 0 intro. intros zenon_H8c. % 6.25/6.45 apply zenon_H8c. apply refl_equal. % 6.25/6.45 (* end of lemma zenon_L4_ *) % 6.25/6.45 assert (zenon_L5_ : (~((c_tptpcol_8_109059) = (c_tptpcol_8_109059))) -> False). % 6.25/6.45 do 0 intro. intros zenon_H8d. % 6.25/6.45 apply zenon_H8d. apply refl_equal. % 6.25/6.45 (* end of lemma zenon_L5_ *) % 6.25/6.45 assert (zenon_L6_ : (~((c_tptpcol_7_108547) = (c_tptpcol_7_108547))) -> False). % 6.25/6.45 do 0 intro. intros zenon_H8e. % 6.25/6.45 apply zenon_H8e. apply refl_equal. % 6.25/6.45 (* end of lemma zenon_L6_ *) % 6.25/6.45 assert (zenon_L7_ : (~((c_tptpcol_6_108546) = (c_tptpcol_6_108546))) -> False). % 6.25/6.45 do 0 intro. intros zenon_H8f. % 6.25/6.45 apply zenon_H8f. apply refl_equal. % 6.25/6.45 (* end of lemma zenon_L7_ *) % 6.25/6.45 assert (zenon_L8_ : (~((c_tptpcol_5_106498) = (c_tptpcol_5_106498))) -> False). % 6.25/6.45 do 0 intro. intros zenon_H90. % 6.25/6.45 apply zenon_H90. apply refl_equal. % 6.25/6.45 (* end of lemma zenon_L8_ *) % 6.25/6.45 assert (zenon_L9_ : (~((c_tptpcol_4_106497) = (c_tptpcol_4_106497))) -> False). % 6.25/6.45 do 0 intro. intros zenon_H91. % 6.25/6.45 apply zenon_H91. apply refl_equal. % 6.25/6.45 (* end of lemma zenon_L9_ *) % 6.25/6.45 assert (zenon_L10_ : (~((c_tptpcol_3_98305) = (c_tptpcol_3_98305))) -> False). % 6.25/6.45 do 0 intro. intros zenon_H92. % 6.25/6.45 apply zenon_H92. apply refl_equal. % 6.25/6.45 (* end of lemma zenon_L10_ *) % 6.25/6.45 assert (zenon_L11_ : (~((c_tptpcol_2_98304) = (c_tptpcol_2_98304))) -> False). % 6.25/6.45 do 0 intro. intros zenon_H93. % 6.25/6.45 apply zenon_H93. apply refl_equal. % 6.25/6.45 (* end of lemma zenon_L11_ *) % 6.25/6.45 assert (zenon_L12_ : (~((c_tptpcol_1_65536) = (c_tptpcol_1_65536))) -> False). % 6.25/6.45 do 0 intro. intros zenon_H94. % 6.25/6.45 apply zenon_H94. apply refl_equal. % 6.25/6.45 (* end of lemma zenon_L12_ *) % 6.25/6.45 assert (zenon_L13_ : (~((c_tptpcol_0_0) = (c_tptpcol_0_0))) -> False). % 6.25/6.45 do 0 intro. intros zenon_H95. % 6.25/6.45 apply zenon_H95. apply refl_equal. % 6.25/6.45 (* end of lemma zenon_L13_ *) % 6.25/6.45 assert (zenon_L14_ : (~((c_individual) = (c_individual))) -> False). % 6.25/6.45 do 0 intro. intros zenon_H96. % 6.25/6.45 apply zenon_H96. apply refl_equal. % 6.25/6.45 (* end of lemma zenon_L14_ *) % 6.25/6.45 assert (zenon_L15_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (~(genls (c_tptpcol_12_109157) (c_individual))) -> False). % 6.25/6.45 do 0 intro. intros zenon_H97 zenon_H98. % 6.25/6.45 elim (classic ((~((c_tptpcol_12_109157) = (c_tptpcol_0_0)))/\(~(genls (c_tptpcol_12_109157) (c_tptpcol_0_0))))); [ zenon_intro zenon_H99 | zenon_intro zenon_H9a ]. % 6.25/6.45 apply (zenon_and_s _ _ zenon_H99). zenon_intro zenon_H9c. zenon_intro zenon_H9b. % 6.25/6.45 elim (classic ((~((c_tptpcol_12_109157) = (c_tptpcol_1_65536)))/\(~(genls (c_tptpcol_12_109157) (c_tptpcol_1_65536))))); [ zenon_intro zenon_H9d | zenon_intro zenon_H9e ]. % 6.25/6.45 apply (zenon_and_s _ _ zenon_H9d). zenon_intro zenon_Ha0. zenon_intro zenon_H9f. % 6.25/6.45 elim (classic ((~((c_tptpcol_12_109157) = (c_tptpcol_2_98304)))/\(~(genls (c_tptpcol_12_109157) (c_tptpcol_2_98304))))); [ zenon_intro zenon_Ha1 | zenon_intro zenon_Ha2 ]. % 6.25/6.45 apply (zenon_and_s _ _ zenon_Ha1). zenon_intro zenon_Ha4. zenon_intro zenon_Ha3. % 6.25/6.45 elim (classic ((~((c_tptpcol_12_109157) = (c_tptpcol_3_98305)))/\(~(genls (c_tptpcol_12_109157) (c_tptpcol_3_98305))))); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Ha6 ]. % 6.25/6.45 apply (zenon_and_s _ _ zenon_Ha5). zenon_intro zenon_Ha8. zenon_intro zenon_Ha7. % 6.25/6.45 elim (classic ((~((c_tptpcol_12_109157) = (c_tptpcol_4_106497)))/\(~(genls (c_tptpcol_12_109157) (c_tptpcol_4_106497))))); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Haa ]. % 6.25/6.45 apply (zenon_and_s _ _ zenon_Ha9). zenon_intro zenon_Hac. zenon_intro zenon_Hab. % 6.25/6.45 elim (classic ((~((c_tptpcol_12_109157) = (c_tptpcol_5_106498)))/\(~(genls (c_tptpcol_12_109157) (c_tptpcol_5_106498))))); [ zenon_intro zenon_Had | zenon_intro zenon_Hae ]. % 6.25/6.45 apply (zenon_and_s _ _ zenon_Had). zenon_intro zenon_Hb0. zenon_intro zenon_Haf. % 6.25/6.45 elim (classic ((~((c_tptpcol_12_109157) = (c_tptpcol_6_108546)))/\(~(genls (c_tptpcol_12_109157) (c_tptpcol_6_108546))))); [ zenon_intro zenon_Hb1 | zenon_intro zenon_Hb2 ]. % 6.25/6.45 apply (zenon_and_s _ _ zenon_Hb1). zenon_intro zenon_Hb4. zenon_intro zenon_Hb3. % 6.25/6.45 elim (classic ((~((c_tptpcol_12_109157) = (c_tptpcol_7_108547)))/\(~(genls (c_tptpcol_12_109157) (c_tptpcol_7_108547))))); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hb6 ]. % 6.25/6.45 apply (zenon_and_s _ _ zenon_Hb5). zenon_intro zenon_Hb8. zenon_intro zenon_Hb7. % 6.25/6.45 elim (classic ((~((c_tptpcol_12_109157) = (c_tptpcol_8_109059)))/\(~(genls (c_tptpcol_12_109157) (c_tptpcol_8_109059))))); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hba ]. % 6.25/6.45 apply (zenon_and_s _ _ zenon_Hb9). zenon_intro zenon_Hbc. zenon_intro zenon_Hbb. % 6.25/6.45 elim (classic ((~((c_tptpcol_12_109157) = (c_tptpcol_9_109060)))/\(~(genls (c_tptpcol_12_109157) (c_tptpcol_9_109060))))); [ zenon_intro zenon_Hbd | zenon_intro zenon_Hbe ]. % 6.25/6.45 apply (zenon_and_s _ _ zenon_Hbd). zenon_intro zenon_Hc0. zenon_intro zenon_Hbf. % 6.25/6.45 elim (classic ((~((c_tptpcol_12_109157) = (c_tptpcol_10_109061)))/\(~(genls (c_tptpcol_12_109157) (c_tptpcol_10_109061))))); [ zenon_intro zenon_Hc1 | zenon_intro zenon_Hc2 ]. % 6.25/6.45 apply (zenon_and_s _ _ zenon_Hc1). zenon_intro zenon_Hc4. zenon_intro zenon_Hc3. % 6.25/6.45 elim (classic ((~((c_tptpcol_12_109157) = (c_tptpcol_11_109125)))/\(~(genls (c_tptpcol_12_109157) (c_tptpcol_11_109125))))); [ zenon_intro zenon_Hc5 | zenon_intro zenon_Hc6 ]. % 6.25/6.45 apply (zenon_and_s _ _ zenon_Hc5). zenon_intro zenon_Hc8. zenon_intro zenon_Hc7. % 6.25/6.45 exact (zenon_Hc7 just40). % 6.25/6.45 cut ((genls (c_tptpcol_11_109125) (c_tptpcol_10_109061)) = (genls (c_tptpcol_12_109157) (c_tptpcol_10_109061))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_Hc3. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact just38. % 6.25/6.45 cut (((c_tptpcol_10_109061) = (c_tptpcol_10_109061))); [idtac | apply NNPP; zenon_intro zenon_H8b]. % 6.25/6.45 cut (((c_tptpcol_11_109125) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_Hc9]. % 6.25/6.45 congruence. % 6.25/6.45 apply (zenon_notand_s _ _ zenon_Hc6); [ zenon_intro zenon_Hcb | zenon_intro zenon_Hca ]. % 6.25/6.45 apply zenon_Hcb. zenon_intro zenon_Hcc. % 6.25/6.45 elim (classic ((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [ zenon_intro zenon_Hcd | zenon_intro zenon_H8a ]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157)) = ((c_tptpcol_11_109125) = (c_tptpcol_12_109157))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_Hc9. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact zenon_Hcd. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_11_109125))); [idtac | apply NNPP; zenon_intro zenon_Hc8]. % 6.25/6.45 congruence. % 6.25/6.45 exact (zenon_Hc8 zenon_Hcc). % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_Hca. zenon_intro just40. % 6.25/6.45 generalize (zenon_H97 (c_tptpcol_12_109157)). zenon_intro zenon_Hce. % 6.25/6.45 generalize (zenon_Hce (c_tptpcol_11_109125)). zenon_intro zenon_Hcf. % 6.25/6.45 generalize (zenon_Hcf (c_tptpcol_10_109061)). zenon_intro zenon_Hd0. % 6.25/6.45 apply (zenon_imply_s _ _ zenon_Hd0); [ zenon_intro zenon_Hc7 | zenon_intro zenon_Hd1 ]. % 6.25/6.45 exact (zenon_Hc7 just40). % 6.25/6.45 apply (zenon_imply_s _ _ zenon_Hd1); [ zenon_intro zenon_Hd3 | zenon_intro zenon_Hd2 ]. % 6.25/6.45 exact (zenon_Hd3 just38). % 6.25/6.45 exact (zenon_Hc3 zenon_Hd2). % 6.25/6.45 apply zenon_H8b. apply refl_equal. % 6.25/6.45 cut ((genls (c_tptpcol_10_109061) (c_tptpcol_9_109060)) = (genls (c_tptpcol_12_109157) (c_tptpcol_9_109060))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_Hbf. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact just36. % 6.25/6.45 cut (((c_tptpcol_9_109060) = (c_tptpcol_9_109060))); [idtac | apply NNPP; zenon_intro zenon_H8c]. % 6.25/6.45 cut (((c_tptpcol_10_109061) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_Hd4]. % 6.25/6.45 congruence. % 6.25/6.45 apply (zenon_notand_s _ _ zenon_Hc2); [ zenon_intro zenon_Hd6 | zenon_intro zenon_Hd5 ]. % 6.25/6.45 apply zenon_Hd6. zenon_intro zenon_Hd7. % 6.25/6.45 elim (classic ((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [ zenon_intro zenon_Hcd | zenon_intro zenon_H8a ]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157)) = ((c_tptpcol_10_109061) = (c_tptpcol_12_109157))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_Hd4. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact zenon_Hcd. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_10_109061))); [idtac | apply NNPP; zenon_intro zenon_Hc4]. % 6.25/6.45 congruence. % 6.25/6.45 exact (zenon_Hc4 zenon_Hd7). % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_Hd5. zenon_intro zenon_Hd2. % 6.25/6.45 generalize (zenon_H97 (c_tptpcol_12_109157)). zenon_intro zenon_Hce. % 6.25/6.45 generalize (zenon_Hce (c_tptpcol_10_109061)). zenon_intro zenon_Hd8. % 6.25/6.45 generalize (zenon_Hd8 (c_tptpcol_9_109060)). zenon_intro zenon_Hd9. % 6.25/6.45 apply (zenon_imply_s _ _ zenon_Hd9); [ zenon_intro zenon_Hc3 | zenon_intro zenon_Hda ]. % 6.25/6.45 exact (zenon_Hc3 zenon_Hd2). % 6.25/6.45 apply (zenon_imply_s _ _ zenon_Hda); [ zenon_intro zenon_Hdc | zenon_intro zenon_Hdb ]. % 6.25/6.45 exact (zenon_Hdc just36). % 6.25/6.45 exact (zenon_Hbf zenon_Hdb). % 6.25/6.45 apply zenon_H8c. apply refl_equal. % 6.25/6.45 cut ((genls (c_tptpcol_9_109060) (c_tptpcol_8_109059)) = (genls (c_tptpcol_12_109157) (c_tptpcol_8_109059))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_Hbb. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact just34. % 6.25/6.45 cut (((c_tptpcol_8_109059) = (c_tptpcol_8_109059))); [idtac | apply NNPP; zenon_intro zenon_H8d]. % 6.25/6.45 cut (((c_tptpcol_9_109060) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_Hdd]. % 6.25/6.45 congruence. % 6.25/6.45 apply (zenon_notand_s _ _ zenon_Hbe); [ zenon_intro zenon_Hdf | zenon_intro zenon_Hde ]. % 6.25/6.45 apply zenon_Hdf. zenon_intro zenon_He0. % 6.25/6.45 elim (classic ((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [ zenon_intro zenon_Hcd | zenon_intro zenon_H8a ]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157)) = ((c_tptpcol_9_109060) = (c_tptpcol_12_109157))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_Hdd. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact zenon_Hcd. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_9_109060))); [idtac | apply NNPP; zenon_intro zenon_Hc0]. % 6.25/6.45 congruence. % 6.25/6.45 exact (zenon_Hc0 zenon_He0). % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_Hde. zenon_intro zenon_Hdb. % 6.25/6.45 generalize (zenon_H97 (c_tptpcol_12_109157)). zenon_intro zenon_Hce. % 6.25/6.45 generalize (zenon_Hce (c_tptpcol_9_109060)). zenon_intro zenon_He1. % 6.25/6.45 generalize (zenon_He1 (c_tptpcol_8_109059)). zenon_intro zenon_He2. % 6.25/6.45 apply (zenon_imply_s _ _ zenon_He2); [ zenon_intro zenon_Hbf | zenon_intro zenon_He3 ]. % 6.25/6.45 exact (zenon_Hbf zenon_Hdb). % 6.25/6.45 apply (zenon_imply_s _ _ zenon_He3); [ zenon_intro zenon_He5 | zenon_intro zenon_He4 ]. % 6.25/6.45 exact (zenon_He5 just34). % 6.25/6.45 exact (zenon_Hbb zenon_He4). % 6.25/6.45 apply zenon_H8d. apply refl_equal. % 6.25/6.45 cut ((genls (c_tptpcol_8_109059) (c_tptpcol_7_108547)) = (genls (c_tptpcol_12_109157) (c_tptpcol_7_108547))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_Hb7. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact just32. % 6.25/6.45 cut (((c_tptpcol_7_108547) = (c_tptpcol_7_108547))); [idtac | apply NNPP; zenon_intro zenon_H8e]. % 6.25/6.45 cut (((c_tptpcol_8_109059) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_He6]. % 6.25/6.45 congruence. % 6.25/6.45 apply (zenon_notand_s _ _ zenon_Hba); [ zenon_intro zenon_He8 | zenon_intro zenon_He7 ]. % 6.25/6.45 apply zenon_He8. zenon_intro zenon_He9. % 6.25/6.45 elim (classic ((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [ zenon_intro zenon_Hcd | zenon_intro zenon_H8a ]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157)) = ((c_tptpcol_8_109059) = (c_tptpcol_12_109157))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_He6. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact zenon_Hcd. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_8_109059))); [idtac | apply NNPP; zenon_intro zenon_Hbc]. % 6.25/6.45 congruence. % 6.25/6.45 exact (zenon_Hbc zenon_He9). % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_He7. zenon_intro zenon_He4. % 6.25/6.45 generalize (zenon_H97 (c_tptpcol_12_109157)). zenon_intro zenon_Hce. % 6.25/6.45 generalize (zenon_Hce (c_tptpcol_8_109059)). zenon_intro zenon_Hea. % 6.25/6.45 generalize (zenon_Hea (c_tptpcol_7_108547)). zenon_intro zenon_Heb. % 6.25/6.45 apply (zenon_imply_s _ _ zenon_Heb); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hec ]. % 6.25/6.45 exact (zenon_Hbb zenon_He4). % 6.25/6.45 apply (zenon_imply_s _ _ zenon_Hec); [ zenon_intro zenon_Hee | zenon_intro zenon_Hed ]. % 6.25/6.45 exact (zenon_Hee just32). % 6.25/6.45 exact (zenon_Hb7 zenon_Hed). % 6.25/6.45 apply zenon_H8e. apply refl_equal. % 6.25/6.45 cut ((genls (c_tptpcol_7_108547) (c_tptpcol_6_108546)) = (genls (c_tptpcol_12_109157) (c_tptpcol_6_108546))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_Hb3. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact just30. % 6.25/6.45 cut (((c_tptpcol_6_108546) = (c_tptpcol_6_108546))); [idtac | apply NNPP; zenon_intro zenon_H8f]. % 6.25/6.45 cut (((c_tptpcol_7_108547) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_Hef]. % 6.25/6.45 congruence. % 6.25/6.45 apply (zenon_notand_s _ _ zenon_Hb6); [ zenon_intro zenon_Hf1 | zenon_intro zenon_Hf0 ]. % 6.25/6.45 apply zenon_Hf1. zenon_intro zenon_Hf2. % 6.25/6.45 elim (classic ((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [ zenon_intro zenon_Hcd | zenon_intro zenon_H8a ]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157)) = ((c_tptpcol_7_108547) = (c_tptpcol_12_109157))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_Hef. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact zenon_Hcd. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_7_108547))); [idtac | apply NNPP; zenon_intro zenon_Hb8]. % 6.25/6.45 congruence. % 6.25/6.45 exact (zenon_Hb8 zenon_Hf2). % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_Hf0. zenon_intro zenon_Hed. % 6.25/6.45 generalize (zenon_H97 (c_tptpcol_12_109157)). zenon_intro zenon_Hce. % 6.25/6.45 generalize (zenon_Hce (c_tptpcol_7_108547)). zenon_intro zenon_Hf3. % 6.25/6.45 generalize (zenon_Hf3 (c_tptpcol_6_108546)). zenon_intro zenon_Hf4. % 6.25/6.45 apply (zenon_imply_s _ _ zenon_Hf4); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hf5 ]. % 6.25/6.45 exact (zenon_Hb7 zenon_Hed). % 6.25/6.45 apply (zenon_imply_s _ _ zenon_Hf5); [ zenon_intro zenon_Hf7 | zenon_intro zenon_Hf6 ]. % 6.25/6.45 exact (zenon_Hf7 just30). % 6.25/6.45 exact (zenon_Hb3 zenon_Hf6). % 6.25/6.45 apply zenon_H8f. apply refl_equal. % 6.25/6.45 cut ((genls (c_tptpcol_6_108546) (c_tptpcol_5_106498)) = (genls (c_tptpcol_12_109157) (c_tptpcol_5_106498))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_Haf. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact just28. % 6.25/6.45 cut (((c_tptpcol_5_106498) = (c_tptpcol_5_106498))); [idtac | apply NNPP; zenon_intro zenon_H90]. % 6.25/6.45 cut (((c_tptpcol_6_108546) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_Hf8]. % 6.25/6.45 congruence. % 6.25/6.45 apply (zenon_notand_s _ _ zenon_Hb2); [ zenon_intro zenon_Hfa | zenon_intro zenon_Hf9 ]. % 6.25/6.45 apply zenon_Hfa. zenon_intro zenon_Hfb. % 6.25/6.45 elim (classic ((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [ zenon_intro zenon_Hcd | zenon_intro zenon_H8a ]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157)) = ((c_tptpcol_6_108546) = (c_tptpcol_12_109157))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_Hf8. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact zenon_Hcd. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_6_108546))); [idtac | apply NNPP; zenon_intro zenon_Hb4]. % 6.25/6.45 congruence. % 6.25/6.45 exact (zenon_Hb4 zenon_Hfb). % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_Hf9. zenon_intro zenon_Hf6. % 6.25/6.45 generalize (zenon_H97 (c_tptpcol_12_109157)). zenon_intro zenon_Hce. % 6.25/6.45 generalize (zenon_Hce (c_tptpcol_6_108546)). zenon_intro zenon_Hfc. % 6.25/6.45 generalize (zenon_Hfc (c_tptpcol_5_106498)). zenon_intro zenon_Hfd. % 6.25/6.45 apply (zenon_imply_s _ _ zenon_Hfd); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hfe ]. % 6.25/6.45 exact (zenon_Hb3 zenon_Hf6). % 6.25/6.45 apply (zenon_imply_s _ _ zenon_Hfe); [ zenon_intro zenon_H100 | zenon_intro zenon_Hff ]. % 6.25/6.45 exact (zenon_H100 just28). % 6.25/6.45 exact (zenon_Haf zenon_Hff). % 6.25/6.45 apply zenon_H90. apply refl_equal. % 6.25/6.45 cut ((genls (c_tptpcol_5_106498) (c_tptpcol_4_106497)) = (genls (c_tptpcol_12_109157) (c_tptpcol_4_106497))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_Hab. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact just26. % 6.25/6.45 cut (((c_tptpcol_4_106497) = (c_tptpcol_4_106497))); [idtac | apply NNPP; zenon_intro zenon_H91]. % 6.25/6.45 cut (((c_tptpcol_5_106498) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H101]. % 6.25/6.45 congruence. % 6.25/6.45 apply (zenon_notand_s _ _ zenon_Hae); [ zenon_intro zenon_H103 | zenon_intro zenon_H102 ]. % 6.25/6.45 apply zenon_H103. zenon_intro zenon_H104. % 6.25/6.45 elim (classic ((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [ zenon_intro zenon_Hcd | zenon_intro zenon_H8a ]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157)) = ((c_tptpcol_5_106498) = (c_tptpcol_12_109157))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_H101. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact zenon_Hcd. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_5_106498))); [idtac | apply NNPP; zenon_intro zenon_Hb0]. % 6.25/6.45 congruence. % 6.25/6.45 exact (zenon_Hb0 zenon_H104). % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_H102. zenon_intro zenon_Hff. % 6.25/6.45 generalize (zenon_H97 (c_tptpcol_12_109157)). zenon_intro zenon_Hce. % 6.25/6.45 generalize (zenon_Hce (c_tptpcol_5_106498)). zenon_intro zenon_H105. % 6.25/6.45 generalize (zenon_H105 (c_tptpcol_4_106497)). zenon_intro zenon_H106. % 6.25/6.45 apply (zenon_imply_s _ _ zenon_H106); [ zenon_intro zenon_Haf | zenon_intro zenon_H107 ]. % 6.25/6.45 exact (zenon_Haf zenon_Hff). % 6.25/6.45 apply (zenon_imply_s _ _ zenon_H107); [ zenon_intro zenon_H109 | zenon_intro zenon_H108 ]. % 6.25/6.45 exact (zenon_H109 just26). % 6.25/6.45 exact (zenon_Hab zenon_H108). % 6.25/6.45 apply zenon_H91. apply refl_equal. % 6.25/6.45 cut ((genls (c_tptpcol_4_106497) (c_tptpcol_3_98305)) = (genls (c_tptpcol_12_109157) (c_tptpcol_3_98305))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_Ha7. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact just24. % 6.25/6.45 cut (((c_tptpcol_3_98305) = (c_tptpcol_3_98305))); [idtac | apply NNPP; zenon_intro zenon_H92]. % 6.25/6.45 cut (((c_tptpcol_4_106497) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H10a]. % 6.25/6.45 congruence. % 6.25/6.45 apply (zenon_notand_s _ _ zenon_Haa); [ zenon_intro zenon_H10c | zenon_intro zenon_H10b ]. % 6.25/6.45 apply zenon_H10c. zenon_intro zenon_H10d. % 6.25/6.45 elim (classic ((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [ zenon_intro zenon_Hcd | zenon_intro zenon_H8a ]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157)) = ((c_tptpcol_4_106497) = (c_tptpcol_12_109157))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_H10a. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact zenon_Hcd. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_4_106497))); [idtac | apply NNPP; zenon_intro zenon_Hac]. % 6.25/6.45 congruence. % 6.25/6.45 exact (zenon_Hac zenon_H10d). % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_H10b. zenon_intro zenon_H108. % 6.25/6.45 generalize (zenon_H97 (c_tptpcol_12_109157)). zenon_intro zenon_Hce. % 6.25/6.45 generalize (zenon_Hce (c_tptpcol_4_106497)). zenon_intro zenon_H10e. % 6.25/6.45 generalize (zenon_H10e (c_tptpcol_3_98305)). zenon_intro zenon_H10f. % 6.25/6.45 apply (zenon_imply_s _ _ zenon_H10f); [ zenon_intro zenon_Hab | zenon_intro zenon_H110 ]. % 6.25/6.45 exact (zenon_Hab zenon_H108). % 6.25/6.45 apply (zenon_imply_s _ _ zenon_H110); [ zenon_intro zenon_H112 | zenon_intro zenon_H111 ]. % 6.25/6.45 exact (zenon_H112 just24). % 6.25/6.45 exact (zenon_Ha7 zenon_H111). % 6.25/6.45 apply zenon_H92. apply refl_equal. % 6.25/6.45 cut ((genls (c_tptpcol_3_98305) (c_tptpcol_2_98304)) = (genls (c_tptpcol_12_109157) (c_tptpcol_2_98304))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_Ha3. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact just22. % 6.25/6.45 cut (((c_tptpcol_2_98304) = (c_tptpcol_2_98304))); [idtac | apply NNPP; zenon_intro zenon_H93]. % 6.25/6.45 cut (((c_tptpcol_3_98305) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H113]. % 6.25/6.45 congruence. % 6.25/6.45 apply (zenon_notand_s _ _ zenon_Ha6); [ zenon_intro zenon_H115 | zenon_intro zenon_H114 ]. % 6.25/6.45 apply zenon_H115. zenon_intro zenon_H116. % 6.25/6.45 elim (classic ((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [ zenon_intro zenon_Hcd | zenon_intro zenon_H8a ]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157)) = ((c_tptpcol_3_98305) = (c_tptpcol_12_109157))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_H113. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact zenon_Hcd. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_3_98305))); [idtac | apply NNPP; zenon_intro zenon_Ha8]. % 6.25/6.45 congruence. % 6.25/6.45 exact (zenon_Ha8 zenon_H116). % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_H114. zenon_intro zenon_H111. % 6.25/6.45 generalize (zenon_H97 (c_tptpcol_12_109157)). zenon_intro zenon_Hce. % 6.25/6.45 generalize (zenon_Hce (c_tptpcol_3_98305)). zenon_intro zenon_H117. % 6.25/6.45 generalize (zenon_H117 (c_tptpcol_2_98304)). zenon_intro zenon_H118. % 6.25/6.45 apply (zenon_imply_s _ _ zenon_H118); [ zenon_intro zenon_Ha7 | zenon_intro zenon_H119 ]. % 6.25/6.45 exact (zenon_Ha7 zenon_H111). % 6.25/6.45 apply (zenon_imply_s _ _ zenon_H119); [ zenon_intro zenon_H11b | zenon_intro zenon_H11a ]. % 6.25/6.45 exact (zenon_H11b just22). % 6.25/6.45 exact (zenon_Ha3 zenon_H11a). % 6.25/6.45 apply zenon_H93. apply refl_equal. % 6.25/6.45 cut ((genls (c_tptpcol_2_98304) (c_tptpcol_1_65536)) = (genls (c_tptpcol_12_109157) (c_tptpcol_1_65536))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_H9f. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact just20. % 6.25/6.45 cut (((c_tptpcol_1_65536) = (c_tptpcol_1_65536))); [idtac | apply NNPP; zenon_intro zenon_H94]. % 6.25/6.45 cut (((c_tptpcol_2_98304) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H11c]. % 6.25/6.45 congruence. % 6.25/6.45 apply (zenon_notand_s _ _ zenon_Ha2); [ zenon_intro zenon_H11e | zenon_intro zenon_H11d ]. % 6.25/6.45 apply zenon_H11e. zenon_intro zenon_H11f. % 6.25/6.45 elim (classic ((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [ zenon_intro zenon_Hcd | zenon_intro zenon_H8a ]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157)) = ((c_tptpcol_2_98304) = (c_tptpcol_12_109157))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_H11c. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact zenon_Hcd. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_2_98304))); [idtac | apply NNPP; zenon_intro zenon_Ha4]. % 6.25/6.45 congruence. % 6.25/6.45 exact (zenon_Ha4 zenon_H11f). % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_H11d. zenon_intro zenon_H11a. % 6.25/6.45 generalize (zenon_H97 (c_tptpcol_12_109157)). zenon_intro zenon_Hce. % 6.25/6.45 generalize (zenon_Hce (c_tptpcol_2_98304)). zenon_intro zenon_H120. % 6.25/6.45 generalize (zenon_H120 (c_tptpcol_1_65536)). zenon_intro zenon_H121. % 6.25/6.45 apply (zenon_imply_s _ _ zenon_H121); [ zenon_intro zenon_Ha3 | zenon_intro zenon_H122 ]. % 6.25/6.45 exact (zenon_Ha3 zenon_H11a). % 6.25/6.45 apply (zenon_imply_s _ _ zenon_H122); [ zenon_intro zenon_H124 | zenon_intro zenon_H123 ]. % 6.25/6.45 exact (zenon_H124 just20). % 6.25/6.45 exact (zenon_H9f zenon_H123). % 6.25/6.45 apply zenon_H94. apply refl_equal. % 6.25/6.45 cut ((genls (c_tptpcol_1_65536) (c_tptpcol_0_0)) = (genls (c_tptpcol_12_109157) (c_tptpcol_0_0))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_H9b. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact just18. % 6.25/6.45 cut (((c_tptpcol_0_0) = (c_tptpcol_0_0))); [idtac | apply NNPP; zenon_intro zenon_H95]. % 6.25/6.45 cut (((c_tptpcol_1_65536) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H125]. % 6.25/6.45 congruence. % 6.25/6.45 apply (zenon_notand_s _ _ zenon_H9e); [ zenon_intro zenon_H127 | zenon_intro zenon_H126 ]. % 6.25/6.45 apply zenon_H127. zenon_intro zenon_H128. % 6.25/6.45 elim (classic ((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [ zenon_intro zenon_Hcd | zenon_intro zenon_H8a ]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157)) = ((c_tptpcol_1_65536) = (c_tptpcol_12_109157))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_H125. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact zenon_Hcd. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_1_65536))); [idtac | apply NNPP; zenon_intro zenon_Ha0]. % 6.25/6.45 congruence. % 6.25/6.45 exact (zenon_Ha0 zenon_H128). % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_H126. zenon_intro zenon_H123. % 6.25/6.45 generalize (zenon_H97 (c_tptpcol_12_109157)). zenon_intro zenon_Hce. % 6.25/6.45 generalize (zenon_Hce (c_tptpcol_1_65536)). zenon_intro zenon_H129. % 6.25/6.45 generalize (zenon_H129 (c_tptpcol_0_0)). zenon_intro zenon_H12a. % 6.25/6.45 apply (zenon_imply_s _ _ zenon_H12a); [ zenon_intro zenon_H9f | zenon_intro zenon_H12b ]. % 6.25/6.45 exact (zenon_H9f zenon_H123). % 6.25/6.45 apply (zenon_imply_s _ _ zenon_H12b); [ zenon_intro zenon_H12d | zenon_intro zenon_H12c ]. % 6.25/6.45 exact (zenon_H12d just18). % 6.25/6.45 exact (zenon_H9b zenon_H12c). % 6.25/6.45 apply zenon_H95. apply refl_equal. % 6.25/6.45 cut ((genls (c_tptpcol_0_0) (c_individual)) = (genls (c_tptpcol_12_109157) (c_individual))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_H98. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact just15. % 6.25/6.45 cut (((c_individual) = (c_individual))); [idtac | apply NNPP; zenon_intro zenon_H96]. % 6.25/6.45 cut (((c_tptpcol_0_0) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H12e]. % 6.25/6.45 congruence. % 6.25/6.45 apply (zenon_notand_s _ _ zenon_H9a); [ zenon_intro zenon_H130 | zenon_intro zenon_H12f ]. % 6.25/6.45 apply zenon_H130. zenon_intro zenon_H131. % 6.25/6.45 elim (classic ((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [ zenon_intro zenon_Hcd | zenon_intro zenon_H8a ]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157)) = ((c_tptpcol_0_0) = (c_tptpcol_12_109157))). % 6.25/6.45 intro zenon_D_pnotp. % 6.25/6.45 apply zenon_H12e. % 6.25/6.45 rewrite <- zenon_D_pnotp. % 6.25/6.45 exact zenon_Hcd. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 6.25/6.45 cut (((c_tptpcol_12_109157) = (c_tptpcol_0_0))); [idtac | apply NNPP; zenon_intro zenon_H9c]. % 6.25/6.45 congruence. % 6.25/6.45 exact (zenon_H9c zenon_H131). % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_H8a. apply refl_equal. % 6.25/6.45 apply zenon_H12f. zenon_intro zenon_H12c. % 6.25/6.45 generalize (zenon_H97 (c_tptpcol_12_109157)). zenon_intro zenon_Hce. % 6.25/6.45 generalize (zenon_Hce (c_tptpcol_0_0)). zenon_intro zenon_H132. % 6.25/6.45 generalize (zenon_H132 (c_individual)). zenon_intro zenon_H133. % 6.25/6.45 apply (zenon_imply_s _ _ zenon_H133); [ zenon_intro zenon_H9b | zenon_intro zenon_H134 ]. % 6.25/6.45 exact (zenon_H9b zenon_H12c). % 6.25/6.45 apply (zenon_imply_s _ _ zenon_H134); [ zenon_intro zenon_H136 | zenon_intro zenon_H135 ]. % 6.25/6.45 exact (zenon_H136 just15). % 6.25/6.45 exact (zenon_H98 zenon_H135). % 6.25/6.45 apply zenon_H96. apply refl_equal. % 6.25/6.45 (* end of lemma zenon_L15_ *) % 6.25/6.45 assert (zenon_L16_ : (isa (c_tptpcol_16_62187) (c_individual)) -> (~(individual (c_tptpcol_16_62187))) -> False). % 6.25/6.45 do 0 intro. intros zenon_H137 zenon_H138. % 6.25/6.45 generalize (just95 (c_tptpcol_16_62187)). zenon_intro zenon_H139. % 6.25/6.45 apply (zenon_imply_s _ _ zenon_H139); [ zenon_intro zenon_H13b | zenon_intro zenon_H13a ]. % 6.25/6.46 exact (zenon_H13b zenon_H137). % 6.25/6.46 exact (zenon_H138 zenon_H13a). % 6.25/6.46 (* end of lemma zenon_L16_ *) % 6.25/6.46 assert (zenon_L17_ : (collection (c_tptpcol_16_62187)) -> (isa (c_tptpcol_16_62187) (c_individual)) -> False). % 6.25/6.46 do 0 intro. intros zenon_H13c zenon_H137. % 6.25/6.46 generalize (just9 (c_tptpcol_16_62187)). zenon_intro zenon_H13d. % 6.25/6.46 apply (zenon_notand_s _ _ zenon_H13d); [ zenon_intro zenon_H13e | zenon_intro zenon_H138 ]. % 6.25/6.46 exact (zenon_H13e zenon_H13c). % 6.25/6.46 apply (zenon_L16_); trivial. % 6.25/6.46 (* end of lemma zenon_L17_ *) % 6.25/6.46 assert (zenon_L18_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (forall NEW : zenon_U, (((isa (c_tptpcol_16_62187) (c_tptpcol_12_109157))/\(genls (c_tptpcol_12_109157) NEW))->(isa (c_tptpcol_16_62187) NEW))) -> (isa (c_tptpcol_16_62187) (c_tptpcol_12_109157)) -> (collection (c_tptpcol_16_62187)) -> False). % 6.25/6.46 do 0 intro. intros zenon_H97 zenon_H13f zenon_H140 zenon_H13c. % 6.25/6.46 generalize (zenon_H13f (c_individual)). zenon_intro zenon_H141. % 6.25/6.46 apply (zenon_imply_s _ _ zenon_H141); [ zenon_intro zenon_H142 | zenon_intro zenon_H137 ]. % 6.25/6.46 apply (zenon_notand_s _ _ zenon_H142); [ zenon_intro zenon_H143 | zenon_intro zenon_H98 ]. % 6.25/6.46 exact (zenon_H143 zenon_H140). % 6.25/6.46 apply (zenon_L15_); trivial. % 6.25/6.46 apply (zenon_L17_); trivial. % 6.25/6.46 (* end of lemma zenon_L18_ *) % 6.25/6.46 assert (zenon_L19_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (forall OLD : zenon_U, (forall NEW : zenon_U, (((isa (c_tptpcol_16_62187) OLD)/\(genls OLD NEW))->(isa (c_tptpcol_16_62187) NEW)))) -> (collection (c_tptpcol_16_62187)) -> (tptpcol_15_109185 (c_tptpcol_16_62187)) -> False). % 6.25/6.46 do 0 intro. intros zenon_H97 zenon_H144 zenon_H13c zenon_H145. % 6.25/6.46 generalize (zenon_H144 (c_tptpcol_15_109185)). zenon_intro zenon_H146. % 6.25/6.46 generalize (zenon_H144 (c_tptpcol_14_109181)). zenon_intro zenon_H147. % 6.25/6.46 generalize (zenon_H144 (c_tptpcol_12_109157)). zenon_intro zenon_H13f. % 6.25/6.46 generalize (zenon_H147 (c_tptpcol_12_109157)). zenon_intro zenon_H148. % 6.25/6.46 apply (zenon_imply_s _ _ zenon_H148); [ zenon_intro zenon_H149 | zenon_intro zenon_H140 ]. % 6.25/6.46 apply (zenon_notand_s _ _ zenon_H149); [ zenon_intro zenon_H14b | zenon_intro zenon_H14a ]. % 6.25/6.46 generalize (just62 (c_tptpcol_16_62187)). zenon_intro zenon_H14c. % 6.25/6.46 apply (zenon_imply_s _ _ zenon_H14c); [ zenon_intro zenon_H14e | zenon_intro zenon_H14d ]. % 6.25/6.46 exact (zenon_H14e zenon_H145). % 6.25/6.46 generalize (zenon_H146 (c_tptpcol_14_109181)). zenon_intro zenon_H14f. % 6.25/6.46 apply (zenon_imply_s _ _ zenon_H14f); [ zenon_intro zenon_H151 | zenon_intro zenon_H150 ]. % 6.25/6.46 apply (zenon_notand_s _ _ zenon_H151); [ zenon_intro zenon_H153 | zenon_intro zenon_H152 ]. % 6.25/6.46 exact (zenon_H153 zenon_H14d). % 6.25/6.46 exact (zenon_H152 just46). % 6.25/6.46 exact (zenon_H14b zenon_H150). % 6.25/6.46 elim (classic ((~((c_tptpcol_14_109181) = (c_tptpcol_13_109173)))/\(~(genls (c_tptpcol_14_109181) (c_tptpcol_13_109173))))); [ zenon_intro zenon_H154 | zenon_intro zenon_H155 ]. % 6.25/6.46 apply (zenon_and_s _ _ zenon_H154). zenon_intro zenon_H157. zenon_intro zenon_H156. % 6.25/6.46 exact (zenon_H156 just44). % 6.25/6.46 cut ((genls (c_tptpcol_13_109173) (c_tptpcol_12_109157)) = (genls (c_tptpcol_14_109181) (c_tptpcol_12_109157))). % 6.25/6.46 intro zenon_D_pnotp. % 6.25/6.46 apply zenon_H14a. % 6.25/6.46 rewrite <- zenon_D_pnotp. % 6.25/6.46 exact just42. % 6.25/6.46 cut (((c_tptpcol_12_109157) = (c_tptpcol_12_109157))); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 6.25/6.46 cut (((c_tptpcol_13_109173) = (c_tptpcol_14_109181))); [idtac | apply NNPP; zenon_intro zenon_H158]. % 6.25/6.46 congruence. % 6.25/6.46 apply (zenon_notand_s _ _ zenon_H155); [ zenon_intro zenon_H15a | zenon_intro zenon_H159 ]. % 6.25/6.46 apply zenon_H15a. zenon_intro zenon_H15b. % 6.25/6.46 elim (classic ((c_tptpcol_14_109181) = (c_tptpcol_14_109181))); [ zenon_intro zenon_H15c | zenon_intro zenon_H15d ]. % 6.25/6.46 cut (((c_tptpcol_14_109181) = (c_tptpcol_14_109181)) = ((c_tptpcol_13_109173) = (c_tptpcol_14_109181))). % 6.25/6.46 intro zenon_D_pnotp. % 6.25/6.46 apply zenon_H158. % 6.25/6.46 rewrite <- zenon_D_pnotp. % 6.25/6.46 exact zenon_H15c. % 6.25/6.46 cut (((c_tptpcol_14_109181) = (c_tptpcol_14_109181))); [idtac | apply NNPP; zenon_intro zenon_H15d]. % 6.25/6.46 cut (((c_tptpcol_14_109181) = (c_tptpcol_13_109173))); [idtac | apply NNPP; zenon_intro zenon_H157]. % 6.25/6.46 congruence. % 6.25/6.46 exact (zenon_H157 zenon_H15b). % 6.25/6.46 apply zenon_H15d. apply refl_equal. % 6.25/6.46 apply zenon_H15d. apply refl_equal. % 6.25/6.46 apply zenon_H159. zenon_intro just44. % 6.25/6.46 generalize (zenon_H97 (c_tptpcol_14_109181)). zenon_intro zenon_H15e. % 6.25/6.46 generalize (zenon_H15e (c_tptpcol_13_109173)). zenon_intro zenon_H15f. % 6.25/6.46 generalize (zenon_H15f (c_tptpcol_12_109157)). zenon_intro zenon_H160. % 6.25/6.46 apply (zenon_imply_s _ _ zenon_H160); [ zenon_intro zenon_H156 | zenon_intro zenon_H161 ]. % 6.25/6.46 exact (zenon_H156 just44). % 6.25/6.46 apply (zenon_imply_s _ _ zenon_H161); [ zenon_intro zenon_H163 | zenon_intro zenon_H162 ]. % 6.25/6.46 exact (zenon_H163 just42). % 6.25/6.46 exact (zenon_H14a zenon_H162). % 6.25/6.46 apply zenon_H8a. apply refl_equal. % 6.25/6.46 apply (zenon_L18_); trivial. % 6.25/6.46 (* end of lemma zenon_L19_ *) % 6.25/6.46 apply NNPP. intro zenon_G. % 6.25/6.46 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z))))))); [ zenon_intro zenon_H97 | zenon_intro zenon_H164 ]. % 6.25/6.46 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H166. zenon_intro zenon_H165. % 6.25/6.46 apply zenon_H165. zenon_intro zenon_H145. % 6.25/6.46 generalize (just122 (c_tptpcol_16_62187)). zenon_intro zenon_H167. % 6.25/6.46 apply (zenon_imply_s _ _ zenon_H167); [ zenon_intro zenon_H13e | zenon_intro zenon_H168 ]. % 6.25/6.46 generalize (just14 (c_tptpcol_16_62187)). zenon_intro zenon_H169. % 6.25/6.46 apply (zenon_imply_s _ _ zenon_H169); [ zenon_intro zenon_H86 | zenon_intro zenon_H13c ]. % 6.25/6.46 apply (zenon_L1_); trivial. % 6.25/6.46 exact (zenon_H13e zenon_H13c). % 6.25/6.46 generalize (just111 (c_tptpcol_16_62187)). zenon_intro zenon_H144. % 6.25/6.46 generalize (just119 (c_tptpcol_16_62187)). zenon_intro zenon_H16a. % 6.25/6.46 generalize (zenon_H16a (c_tptpcol_16_62187)). zenon_intro zenon_H16b. % 6.25/6.46 apply (zenon_imply_s _ _ zenon_H16b); [ zenon_intro zenon_H16c | zenon_intro zenon_H13c ]. % 6.25/6.46 exact (zenon_H16c zenon_H168). % 6.25/6.46 apply (zenon_L19_); trivial. % 6.25/6.46 apply zenon_H164. zenon_intro zenon_Tx_ob. apply NNPP. zenon_intro zenon_H16e. % 6.25/6.46 apply zenon_H16e. zenon_intro zenon_Ty_od. apply NNPP. zenon_intro zenon_H170. % 6.25/6.46 apply zenon_H170. zenon_intro zenon_Tz_of. apply NNPP. zenon_intro zenon_H172. % 6.25/6.46 apply (zenon_notimply_s _ _ zenon_H172). zenon_intro zenon_H174. zenon_intro zenon_H173. % 6.25/6.46 apply (zenon_notimply_s _ _ zenon_H173). zenon_intro zenon_H176. zenon_intro zenon_H175. % 6.25/6.46 generalize (just121 zenon_Tx_ob). zenon_intro zenon_H177. % 6.25/6.46 generalize (zenon_H177 zenon_Ty_od). zenon_intro zenon_H178. % 6.25/6.46 generalize (zenon_H178 zenon_Tz_of). zenon_intro zenon_H179. % 6.25/6.46 apply (zenon_imply_s _ _ zenon_H179); [ zenon_intro zenon_H17b | zenon_intro zenon_H17a ]. % 6.25/6.46 apply (zenon_notand_s _ _ zenon_H17b); [ zenon_intro zenon_H17d | zenon_intro zenon_H17c ]. % 6.25/6.46 exact (zenon_H17d zenon_H174). % 6.25/6.46 exact (zenon_H17c zenon_H176). % 6.25/6.46 exact (zenon_H175 zenon_H17a). % 6.25/6.46 Qed. % 6.25/6.46 % SZS output end Proof % 6.25/6.46 (* END-PROOF *) % 6.25/6.46 nodes searched: 288073 % 6.25/6.46 max branch formulas: 16076 % 6.25/6.46 proof nodes created: 1073 % 6.25/6.46 formulas created: 920706 % 6.25/6.46 %------------------------------------------------------------------------------