%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR039+1 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n024.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 00:02:00 EDT 2022 % Result : Theorem 2.66s 2.82s % Output : Proof 2.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : CSR039+1 : TPTP v8.1.0. Released v3.4.0. % 0.10/0.13 % Command : run_zenon %s %d % 0.13/0.34 % Computer : n024.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 : Fri Jun 10 19:06:04 EDT 2022 % 0.13/0.34 % CPUTime : % 2.66/2.82 (* PROOF-FOUND *) % 2.66/2.82 % SZS status Theorem % 2.66/2.82 (* BEGIN-PROOF *) % 2.66/2.82 % SZS output start Proof % 2.66/2.82 Theorem query39 : ((mtvisible (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn (s_http_wwwpoweripodsearchinfobrown_ipodhtml))) (c_translation_7)))->(disjointwith (c_tptpcol_15_93775) (c_tptpcol_13_18664))). % 2.66/2.82 Proof. % 2.66/2.82 assert (zenon_L1_ : (~((c_tptpcol_11_93764) = (c_tptpcol_11_93764))) -> False). % 2.66/2.82 do 0 intro. intros zenon_H9f. % 2.66/2.82 apply zenon_H9f. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L1_ *) % 2.66/2.82 assert (zenon_L2_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (~(genls (c_tptpcol_13_93766) (c_tptpcol_11_93764))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Ha0 zenon_Ha1. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_93766) = (c_tptpcol_12_93765)))/\(~(genls (c_tptpcol_13_93766) (c_tptpcol_12_93765))))); [ zenon_intro zenon_Ha2 | zenon_intro zenon_Ha3 ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_Ha2). zenon_intro zenon_Ha5. zenon_intro zenon_Ha4. % 2.66/2.82 exact (zenon_Ha4 just53). % 2.66/2.82 cut ((genls (c_tptpcol_12_93765) (c_tptpcol_11_93764)) = (genls (c_tptpcol_13_93766) (c_tptpcol_11_93764))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_Ha1. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just51. % 2.66/2.82 cut (((c_tptpcol_11_93764) = (c_tptpcol_11_93764))); [idtac | apply NNPP; zenon_intro zenon_H9f]. % 2.66/2.82 cut (((c_tptpcol_12_93765) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_Ha6]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_Ha3); [ zenon_intro zenon_Ha8 | zenon_intro zenon_Ha7 ]. % 2.66/2.82 apply zenon_Ha8. zenon_intro zenon_Ha9. % 2.66/2.82 elim (classic ((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [ zenon_intro zenon_Haa | zenon_intro zenon_Hab ]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766)) = ((c_tptpcol_12_93765) = (c_tptpcol_13_93766))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_Ha6. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_Haa. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_12_93765))); [idtac | apply NNPP; zenon_intro zenon_Ha5]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_Ha5 zenon_Ha9). % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_Ha7. zenon_intro just53. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_93766)). zenon_intro zenon_Hac. % 2.66/2.82 generalize (zenon_Hac (c_tptpcol_12_93765)). zenon_intro zenon_Had. % 2.66/2.82 generalize (zenon_Had (c_tptpcol_11_93764)). zenon_intro zenon_Hae. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_Hae); [ zenon_intro zenon_Ha4 | zenon_intro zenon_Haf ]. % 2.66/2.82 exact (zenon_Ha4 just53). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_Haf); [ zenon_intro zenon_Hb1 | zenon_intro zenon_Hb0 ]. % 2.66/2.82 exact (zenon_Hb1 just51). % 2.66/2.82 exact (zenon_Ha1 zenon_Hb0). % 2.66/2.82 apply zenon_H9f. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L2_ *) % 2.66/2.82 assert (zenon_L3_ : (~((c_tptpcol_10_93700) = (c_tptpcol_10_93700))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Hb2. % 2.66/2.82 apply zenon_Hb2. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L3_ *) % 2.66/2.82 assert (zenon_L4_ : (~((c_tptpcol_9_93699) = (c_tptpcol_9_93699))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Hb3. % 2.66/2.82 apply zenon_Hb3. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L4_ *) % 2.66/2.82 assert (zenon_L5_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (~(genls (c_tptpcol_13_93766) (c_tptpcol_9_93699))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Ha0 zenon_Hb4. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_93766) = (c_tptpcol_10_93700)))/\(~(genls (c_tptpcol_13_93766) (c_tptpcol_10_93700))))); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hb6 ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_Hb5). zenon_intro zenon_Hb8. zenon_intro zenon_Hb7. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_93766) = (c_tptpcol_11_93764)))/\(~(genls (c_tptpcol_13_93766) (c_tptpcol_11_93764))))); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hba ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_Hb9). zenon_intro zenon_Hbb. zenon_intro zenon_Ha1. % 2.66/2.82 apply (zenon_L2_); trivial. % 2.66/2.82 cut ((genls (c_tptpcol_11_93764) (c_tptpcol_10_93700)) = (genls (c_tptpcol_13_93766) (c_tptpcol_10_93700))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_Hb7. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just49. % 2.66/2.82 cut (((c_tptpcol_10_93700) = (c_tptpcol_10_93700))); [idtac | apply NNPP; zenon_intro zenon_Hb2]. % 2.66/2.82 cut (((c_tptpcol_11_93764) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_Hbc]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_Hba); [ zenon_intro zenon_Hbe | zenon_intro zenon_Hbd ]. % 2.66/2.82 apply zenon_Hbe. zenon_intro zenon_Hbf. % 2.66/2.82 elim (classic ((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [ zenon_intro zenon_Haa | zenon_intro zenon_Hab ]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766)) = ((c_tptpcol_11_93764) = (c_tptpcol_13_93766))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_Hbc. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_Haa. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_11_93764))); [idtac | apply NNPP; zenon_intro zenon_Hbb]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_Hbb zenon_Hbf). % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_Hbd. zenon_intro zenon_Hb0. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_93766)). zenon_intro zenon_Hac. % 2.66/2.82 generalize (zenon_Hac (c_tptpcol_11_93764)). zenon_intro zenon_Hc0. % 2.66/2.82 generalize (zenon_Hc0 (c_tptpcol_10_93700)). zenon_intro zenon_Hc1. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_Hc1); [ zenon_intro zenon_Ha1 | zenon_intro zenon_Hc2 ]. % 2.66/2.82 exact (zenon_Ha1 zenon_Hb0). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_Hc2); [ zenon_intro zenon_Hc4 | zenon_intro zenon_Hc3 ]. % 2.66/2.82 exact (zenon_Hc4 just49). % 2.66/2.82 exact (zenon_Hb7 zenon_Hc3). % 2.66/2.82 apply zenon_Hb2. apply refl_equal. % 2.66/2.82 cut ((genls (c_tptpcol_10_93700) (c_tptpcol_9_93699)) = (genls (c_tptpcol_13_93766) (c_tptpcol_9_93699))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_Hb4. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just47. % 2.66/2.82 cut (((c_tptpcol_9_93699) = (c_tptpcol_9_93699))); [idtac | apply NNPP; zenon_intro zenon_Hb3]. % 2.66/2.82 cut (((c_tptpcol_10_93700) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_Hb6); [ zenon_intro zenon_Hc7 | zenon_intro zenon_Hc6 ]. % 2.66/2.82 apply zenon_Hc7. zenon_intro zenon_Hc8. % 2.66/2.82 elim (classic ((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [ zenon_intro zenon_Haa | zenon_intro zenon_Hab ]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766)) = ((c_tptpcol_10_93700) = (c_tptpcol_13_93766))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_Hc5. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_Haa. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_10_93700))); [idtac | apply NNPP; zenon_intro zenon_Hb8]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_Hb8 zenon_Hc8). % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_Hc6. zenon_intro zenon_Hc3. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_93766)). zenon_intro zenon_Hac. % 2.66/2.82 generalize (zenon_Hac (c_tptpcol_10_93700)). zenon_intro zenon_Hc9. % 2.66/2.82 generalize (zenon_Hc9 (c_tptpcol_9_93699)). zenon_intro zenon_Hca. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_Hca); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hcb ]. % 2.66/2.82 exact (zenon_Hb7 zenon_Hc3). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_Hcb); [ zenon_intro zenon_Hcd | zenon_intro zenon_Hcc ]. % 2.66/2.82 exact (zenon_Hcd just47). % 2.66/2.82 exact (zenon_Hb4 zenon_Hcc). % 2.66/2.82 apply zenon_Hb3. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L5_ *) % 2.66/2.82 assert (zenon_L6_ : (~((c_tptpcol_8_93698) = (c_tptpcol_8_93698))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Hce. % 2.66/2.82 apply zenon_Hce. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L6_ *) % 2.66/2.82 assert (zenon_L7_ : (~((c_tptpcol_7_93186) = (c_tptpcol_7_93186))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Hcf. % 2.66/2.82 apply zenon_Hcf. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L7_ *) % 2.66/2.82 assert (zenon_L8_ : (~((c_tptpcol_6_92162) = (c_tptpcol_6_92162))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Hd0. % 2.66/2.82 apply zenon_Hd0. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L8_ *) % 2.66/2.82 assert (zenon_L9_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (~(genls (c_tptpcol_13_93766) (c_tptpcol_6_92162))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Ha0 zenon_Hd1. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_93766) = (c_tptpcol_7_93186)))/\(~(genls (c_tptpcol_13_93766) (c_tptpcol_7_93186))))); [ zenon_intro zenon_Hd2 | zenon_intro zenon_Hd3 ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_Hd2). zenon_intro zenon_Hd5. zenon_intro zenon_Hd4. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_93766) = (c_tptpcol_8_93698)))/\(~(genls (c_tptpcol_13_93766) (c_tptpcol_8_93698))))); [ zenon_intro zenon_Hd6 | zenon_intro zenon_Hd7 ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_Hd6). zenon_intro zenon_Hd9. zenon_intro zenon_Hd8. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_93766) = (c_tptpcol_9_93699)))/\(~(genls (c_tptpcol_13_93766) (c_tptpcol_9_93699))))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_Hda). zenon_intro zenon_Hdc. zenon_intro zenon_Hb4. % 2.66/2.82 apply (zenon_L5_); trivial. % 2.66/2.82 cut ((genls (c_tptpcol_9_93699) (c_tptpcol_8_93698)) = (genls (c_tptpcol_13_93766) (c_tptpcol_8_93698))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_Hd8. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just45. % 2.66/2.82 cut (((c_tptpcol_8_93698) = (c_tptpcol_8_93698))); [idtac | apply NNPP; zenon_intro zenon_Hce]. % 2.66/2.82 cut (((c_tptpcol_9_93699) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_Hdd]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_Hdb); [ zenon_intro zenon_Hdf | zenon_intro zenon_Hde ]. % 2.66/2.82 apply zenon_Hdf. zenon_intro zenon_He0. % 2.66/2.82 elim (classic ((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [ zenon_intro zenon_Haa | zenon_intro zenon_Hab ]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766)) = ((c_tptpcol_9_93699) = (c_tptpcol_13_93766))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_Hdd. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_Haa. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_9_93699))); [idtac | apply NNPP; zenon_intro zenon_Hdc]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_Hdc zenon_He0). % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_Hde. zenon_intro zenon_Hcc. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_93766)). zenon_intro zenon_Hac. % 2.66/2.82 generalize (zenon_Hac (c_tptpcol_9_93699)). zenon_intro zenon_He1. % 2.66/2.82 generalize (zenon_He1 (c_tptpcol_8_93698)). zenon_intro zenon_He2. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_He2); [ zenon_intro zenon_Hb4 | zenon_intro zenon_He3 ]. % 2.66/2.82 exact (zenon_Hb4 zenon_Hcc). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_He3); [ zenon_intro zenon_He5 | zenon_intro zenon_He4 ]. % 2.66/2.82 exact (zenon_He5 just45). % 2.66/2.82 exact (zenon_Hd8 zenon_He4). % 2.66/2.82 apply zenon_Hce. apply refl_equal. % 2.66/2.82 cut ((genls (c_tptpcol_8_93698) (c_tptpcol_7_93186)) = (genls (c_tptpcol_13_93766) (c_tptpcol_7_93186))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_Hd4. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just43. % 2.66/2.82 cut (((c_tptpcol_7_93186) = (c_tptpcol_7_93186))); [idtac | apply NNPP; zenon_intro zenon_Hcf]. % 2.66/2.82 cut (((c_tptpcol_8_93698) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_He6]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_Hd7); [ zenon_intro zenon_He8 | zenon_intro zenon_He7 ]. % 2.66/2.82 apply zenon_He8. zenon_intro zenon_He9. % 2.66/2.82 elim (classic ((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [ zenon_intro zenon_Haa | zenon_intro zenon_Hab ]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766)) = ((c_tptpcol_8_93698) = (c_tptpcol_13_93766))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_He6. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_Haa. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_8_93698))); [idtac | apply NNPP; zenon_intro zenon_Hd9]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_Hd9 zenon_He9). % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_He7. zenon_intro zenon_He4. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_93766)). zenon_intro zenon_Hac. % 2.66/2.82 generalize (zenon_Hac (c_tptpcol_8_93698)). zenon_intro zenon_Hea. % 2.66/2.82 generalize (zenon_Hea (c_tptpcol_7_93186)). zenon_intro zenon_Heb. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_Heb); [ zenon_intro zenon_Hd8 | zenon_intro zenon_Hec ]. % 2.66/2.82 exact (zenon_Hd8 zenon_He4). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_Hec); [ zenon_intro zenon_Hee | zenon_intro zenon_Hed ]. % 2.66/2.82 exact (zenon_Hee just43). % 2.66/2.82 exact (zenon_Hd4 zenon_Hed). % 2.66/2.82 apply zenon_Hcf. apply refl_equal. % 2.66/2.82 cut ((genls (c_tptpcol_7_93186) (c_tptpcol_6_92162)) = (genls (c_tptpcol_13_93766) (c_tptpcol_6_92162))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_Hd1. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just41. % 2.66/2.82 cut (((c_tptpcol_6_92162) = (c_tptpcol_6_92162))); [idtac | apply NNPP; zenon_intro zenon_Hd0]. % 2.66/2.82 cut (((c_tptpcol_7_93186) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_Hef]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_Hd3); [ zenon_intro zenon_Hf1 | zenon_intro zenon_Hf0 ]. % 2.66/2.82 apply zenon_Hf1. zenon_intro zenon_Hf2. % 2.66/2.82 elim (classic ((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [ zenon_intro zenon_Haa | zenon_intro zenon_Hab ]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766)) = ((c_tptpcol_7_93186) = (c_tptpcol_13_93766))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_Hef. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_Haa. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_7_93186))); [idtac | apply NNPP; zenon_intro zenon_Hd5]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_Hd5 zenon_Hf2). % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_Hf0. zenon_intro zenon_Hed. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_93766)). zenon_intro zenon_Hac. % 2.66/2.82 generalize (zenon_Hac (c_tptpcol_7_93186)). zenon_intro zenon_Hf3. % 2.66/2.82 generalize (zenon_Hf3 (c_tptpcol_6_92162)). zenon_intro zenon_Hf4. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_Hf4); [ zenon_intro zenon_Hd4 | zenon_intro zenon_Hf5 ]. % 2.66/2.82 exact (zenon_Hd4 zenon_Hed). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_Hf5); [ zenon_intro zenon_Hf7 | zenon_intro zenon_Hf6 ]. % 2.66/2.82 exact (zenon_Hf7 just41). % 2.66/2.82 exact (zenon_Hd1 zenon_Hf6). % 2.66/2.82 apply zenon_Hd0. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L9_ *) % 2.66/2.82 assert (zenon_L10_ : (~((c_tptpcol_5_90114) = (c_tptpcol_5_90114))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Hf8. % 2.66/2.82 apply zenon_Hf8. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L10_ *) % 2.66/2.82 assert (zenon_L11_ : (~((c_tptpcol_4_90113) = (c_tptpcol_4_90113))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Hf9. % 2.66/2.82 apply zenon_Hf9. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L11_ *) % 2.66/2.82 assert (zenon_L12_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (~(genls (c_tptpcol_13_93766) (c_tptpcol_4_90113))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Ha0 zenon_Hfa. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_93766) = (c_tptpcol_5_90114)))/\(~(genls (c_tptpcol_13_93766) (c_tptpcol_5_90114))))); [ zenon_intro zenon_Hfb | zenon_intro zenon_Hfc ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_Hfb). zenon_intro zenon_Hfe. zenon_intro zenon_Hfd. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_93766) = (c_tptpcol_6_92162)))/\(~(genls (c_tptpcol_13_93766) (c_tptpcol_6_92162))))); [ zenon_intro zenon_Hff | zenon_intro zenon_H100 ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_Hff). zenon_intro zenon_H101. zenon_intro zenon_Hd1. % 2.66/2.82 apply (zenon_L9_); trivial. % 2.66/2.82 cut ((genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) = (genls (c_tptpcol_13_93766) (c_tptpcol_5_90114))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_Hfd. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just39. % 2.66/2.82 cut (((c_tptpcol_5_90114) = (c_tptpcol_5_90114))); [idtac | apply NNPP; zenon_intro zenon_Hf8]. % 2.66/2.82 cut (((c_tptpcol_6_92162) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_H102]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H100); [ zenon_intro zenon_H104 | zenon_intro zenon_H103 ]. % 2.66/2.82 apply zenon_H104. zenon_intro zenon_H105. % 2.66/2.82 elim (classic ((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [ zenon_intro zenon_Haa | zenon_intro zenon_Hab ]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766)) = ((c_tptpcol_6_92162) = (c_tptpcol_13_93766))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H102. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_Haa. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_6_92162))); [idtac | apply NNPP; zenon_intro zenon_H101]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_H101 zenon_H105). % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_H103. zenon_intro zenon_Hf6. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_93766)). zenon_intro zenon_Hac. % 2.66/2.82 generalize (zenon_Hac (c_tptpcol_6_92162)). zenon_intro zenon_H106. % 2.66/2.82 generalize (zenon_H106 (c_tptpcol_5_90114)). zenon_intro zenon_H107. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H107); [ zenon_intro zenon_Hd1 | zenon_intro zenon_H108 ]. % 2.66/2.82 exact (zenon_Hd1 zenon_Hf6). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H108); [ zenon_intro zenon_H10a | zenon_intro zenon_H109 ]. % 2.66/2.82 exact (zenon_H10a just39). % 2.66/2.82 exact (zenon_Hfd zenon_H109). % 2.66/2.82 apply zenon_Hf8. apply refl_equal. % 2.66/2.82 cut ((genls (c_tptpcol_5_90114) (c_tptpcol_4_90113)) = (genls (c_tptpcol_13_93766) (c_tptpcol_4_90113))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_Hfa. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just37. % 2.66/2.82 cut (((c_tptpcol_4_90113) = (c_tptpcol_4_90113))); [idtac | apply NNPP; zenon_intro zenon_Hf9]. % 2.66/2.82 cut (((c_tptpcol_5_90114) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_H10b]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_Hfc); [ zenon_intro zenon_H10d | zenon_intro zenon_H10c ]. % 2.66/2.82 apply zenon_H10d. zenon_intro zenon_H10e. % 2.66/2.82 elim (classic ((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [ zenon_intro zenon_Haa | zenon_intro zenon_Hab ]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766)) = ((c_tptpcol_5_90114) = (c_tptpcol_13_93766))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H10b. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_Haa. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_5_90114))); [idtac | apply NNPP; zenon_intro zenon_Hfe]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_Hfe zenon_H10e). % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_H10c. zenon_intro zenon_H109. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_93766)). zenon_intro zenon_Hac. % 2.66/2.82 generalize (zenon_Hac (c_tptpcol_5_90114)). zenon_intro zenon_H10f. % 2.66/2.82 generalize (zenon_H10f (c_tptpcol_4_90113)). zenon_intro zenon_H110. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H110); [ zenon_intro zenon_Hfd | zenon_intro zenon_H111 ]. % 2.66/2.82 exact (zenon_Hfd zenon_H109). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H111); [ zenon_intro zenon_H113 | zenon_intro zenon_H112 ]. % 2.66/2.82 exact (zenon_H113 just37). % 2.66/2.82 exact (zenon_Hfa zenon_H112). % 2.66/2.82 apply zenon_Hf9. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L12_ *) % 2.66/2.82 assert (zenon_L13_ : (~((c_tptpcol_3_81921) = (c_tptpcol_3_81921))) -> False). % 2.66/2.82 do 0 intro. intros zenon_H114. % 2.66/2.82 apply zenon_H114. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L13_ *) % 2.66/2.82 assert (zenon_L14_ : (~((c_tptpcol_2_65537) = (c_tptpcol_2_65537))) -> False). % 2.66/2.82 do 0 intro. intros zenon_H115. % 2.66/2.82 apply zenon_H115. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L14_ *) % 2.66/2.82 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_13_93766) (c_tptpcol_2_65537))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Ha0 zenon_H116. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_93766) = (c_tptpcol_3_81921)))/\(~(genls (c_tptpcol_13_93766) (c_tptpcol_3_81921))))); [ zenon_intro zenon_H117 | zenon_intro zenon_H118 ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_H117). zenon_intro zenon_H11a. zenon_intro zenon_H119. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_93766) = (c_tptpcol_4_90113)))/\(~(genls (c_tptpcol_13_93766) (c_tptpcol_4_90113))))); [ zenon_intro zenon_H11b | zenon_intro zenon_H11c ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_H11b). zenon_intro zenon_H11d. zenon_intro zenon_Hfa. % 2.66/2.82 apply (zenon_L12_); trivial. % 2.66/2.82 cut ((genls (c_tptpcol_4_90113) (c_tptpcol_3_81921)) = (genls (c_tptpcol_13_93766) (c_tptpcol_3_81921))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H119. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just35. % 2.66/2.82 cut (((c_tptpcol_3_81921) = (c_tptpcol_3_81921))); [idtac | apply NNPP; zenon_intro zenon_H114]. % 2.66/2.82 cut (((c_tptpcol_4_90113) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_H11e]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H11c); [ zenon_intro zenon_H120 | zenon_intro zenon_H11f ]. % 2.66/2.82 apply zenon_H120. zenon_intro zenon_H121. % 2.66/2.82 elim (classic ((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [ zenon_intro zenon_Haa | zenon_intro zenon_Hab ]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766)) = ((c_tptpcol_4_90113) = (c_tptpcol_13_93766))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H11e. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_Haa. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_4_90113))); [idtac | apply NNPP; zenon_intro zenon_H11d]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_H11d zenon_H121). % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_H11f. zenon_intro zenon_H112. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_93766)). zenon_intro zenon_Hac. % 2.66/2.82 generalize (zenon_Hac (c_tptpcol_4_90113)). zenon_intro zenon_H122. % 2.66/2.82 generalize (zenon_H122 (c_tptpcol_3_81921)). zenon_intro zenon_H123. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H123); [ zenon_intro zenon_Hfa | zenon_intro zenon_H124 ]. % 2.66/2.82 exact (zenon_Hfa zenon_H112). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H124); [ zenon_intro zenon_H126 | zenon_intro zenon_H125 ]. % 2.66/2.82 exact (zenon_H126 just35). % 2.66/2.82 exact (zenon_H119 zenon_H125). % 2.66/2.82 apply zenon_H114. apply refl_equal. % 2.66/2.82 cut ((genls (c_tptpcol_3_81921) (c_tptpcol_2_65537)) = (genls (c_tptpcol_13_93766) (c_tptpcol_2_65537))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H116. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just33. % 2.66/2.82 cut (((c_tptpcol_2_65537) = (c_tptpcol_2_65537))); [idtac | apply NNPP; zenon_intro zenon_H115]. % 2.66/2.82 cut (((c_tptpcol_3_81921) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_H127]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H118); [ zenon_intro zenon_H129 | zenon_intro zenon_H128 ]. % 2.66/2.82 apply zenon_H129. zenon_intro zenon_H12a. % 2.66/2.82 elim (classic ((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [ zenon_intro zenon_Haa | zenon_intro zenon_Hab ]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766)) = ((c_tptpcol_3_81921) = (c_tptpcol_13_93766))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H127. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_Haa. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_3_81921))); [idtac | apply NNPP; zenon_intro zenon_H11a]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_H11a zenon_H12a). % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_H128. zenon_intro zenon_H125. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_93766)). zenon_intro zenon_Hac. % 2.66/2.82 generalize (zenon_Hac (c_tptpcol_3_81921)). zenon_intro zenon_H12b. % 2.66/2.82 generalize (zenon_H12b (c_tptpcol_2_65537)). zenon_intro zenon_H12c. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H12c); [ zenon_intro zenon_H119 | zenon_intro zenon_H12d ]. % 2.66/2.82 exact (zenon_H119 zenon_H125). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H12d); [ zenon_intro zenon_H12f | zenon_intro zenon_H12e ]. % 2.66/2.82 exact (zenon_H12f just33). % 2.66/2.82 exact (zenon_H116 zenon_H12e). % 2.66/2.82 apply zenon_H115. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L15_ *) % 2.66/2.82 assert (zenon_L16_ : (~((c_tptpcol_1_65536) = (c_tptpcol_1_65536))) -> False). % 2.66/2.82 do 0 intro. intros zenon_H130. % 2.66/2.82 apply zenon_H130. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L16_ *) % 2.66/2.82 assert (zenon_L17_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (~(genls (c_tptpcol_13_93766) (c_tptpcol_1_65536))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Ha0 zenon_H131. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_93766) = (c_tptpcol_2_65537)))/\(~(genls (c_tptpcol_13_93766) (c_tptpcol_2_65537))))); [ zenon_intro zenon_H132 | zenon_intro zenon_H133 ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_H132). zenon_intro zenon_H134. zenon_intro zenon_H116. % 2.66/2.82 apply (zenon_L15_); trivial. % 2.66/2.82 cut ((genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) = (genls (c_tptpcol_13_93766) (c_tptpcol_1_65536))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H131. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just31. % 2.66/2.82 cut (((c_tptpcol_1_65536) = (c_tptpcol_1_65536))); [idtac | apply NNPP; zenon_intro zenon_H130]. % 2.66/2.82 cut (((c_tptpcol_2_65537) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_H135]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H133); [ zenon_intro zenon_H137 | zenon_intro zenon_H136 ]. % 2.66/2.82 apply zenon_H137. zenon_intro zenon_H138. % 2.66/2.82 elim (classic ((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [ zenon_intro zenon_Haa | zenon_intro zenon_Hab ]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766)) = ((c_tptpcol_2_65537) = (c_tptpcol_13_93766))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H135. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_Haa. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_2_65537))); [idtac | apply NNPP; zenon_intro zenon_H134]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_H134 zenon_H138). % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 apply zenon_H136. zenon_intro zenon_H12e. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_93766)). zenon_intro zenon_Hac. % 2.66/2.82 generalize (zenon_Hac (c_tptpcol_2_65537)). zenon_intro zenon_H139. % 2.66/2.82 generalize (zenon_H139 (c_tptpcol_1_65536)). zenon_intro zenon_H13a. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H13a); [ zenon_intro zenon_H116 | zenon_intro zenon_H13b ]. % 2.66/2.82 exact (zenon_H116 zenon_H12e). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H13b); [ zenon_intro zenon_H13d | zenon_intro zenon_H13c ]. % 2.66/2.82 exact (zenon_H13d just31). % 2.66/2.82 exact (zenon_H131 zenon_H13c). % 2.66/2.82 apply zenon_H130. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L17_ *) % 2.66/2.82 assert (zenon_L18_ : (~((c_tptpcol_11_18631) = (c_tptpcol_11_18631))) -> False). % 2.66/2.82 do 0 intro. intros zenon_H13e. % 2.66/2.82 apply zenon_H13e. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L18_ *) % 2.66/2.82 assert (zenon_L19_ : (~((c_tptpcol_10_18567) = (c_tptpcol_10_18567))) -> False). % 2.66/2.82 do 0 intro. intros zenon_H13f. % 2.66/2.82 apply zenon_H13f. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L19_ *) % 2.66/2.82 assert (zenon_L20_ : (~((c_tptpcol_9_18439) = (c_tptpcol_9_18439))) -> False). % 2.66/2.82 do 0 intro. intros zenon_H140. % 2.66/2.82 apply zenon_H140. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L20_ *) % 2.66/2.82 assert (zenon_L21_ : (~((c_tptpcol_8_18438) = (c_tptpcol_8_18438))) -> False). % 2.66/2.82 do 0 intro. intros zenon_H141. % 2.66/2.82 apply zenon_H141. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L21_ *) % 2.66/2.82 assert (zenon_L22_ : (~((c_tptpcol_7_18437) = (c_tptpcol_7_18437))) -> False). % 2.66/2.82 do 0 intro. intros zenon_H142. % 2.66/2.82 apply zenon_H142. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L22_ *) % 2.66/2.82 assert (zenon_L23_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (~(genls (c_tptpcol_13_18664) (c_tptpcol_7_18437))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Ha0 zenon_H143. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_18664) = (c_tptpcol_8_18438)))/\(~(genls (c_tptpcol_13_18664) (c_tptpcol_8_18438))))); [ zenon_intro zenon_H144 | zenon_intro zenon_H145 ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_H144). zenon_intro zenon_H147. zenon_intro zenon_H146. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_18664) = (c_tptpcol_9_18439)))/\(~(genls (c_tptpcol_13_18664) (c_tptpcol_9_18439))))); [ zenon_intro zenon_H148 | zenon_intro zenon_H149 ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_H148). zenon_intro zenon_H14b. zenon_intro zenon_H14a. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_18664) = (c_tptpcol_10_18567)))/\(~(genls (c_tptpcol_13_18664) (c_tptpcol_10_18567))))); [ zenon_intro zenon_H14c | zenon_intro zenon_H14d ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_H14c). zenon_intro zenon_H14f. zenon_intro zenon_H14e. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_18664) = (c_tptpcol_11_18631)))/\(~(genls (c_tptpcol_13_18664) (c_tptpcol_11_18631))))); [ zenon_intro zenon_H150 | zenon_intro zenon_H151 ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_H150). zenon_intro zenon_H153. zenon_intro zenon_H152. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_18664) = (c_tptpcol_12_18663)))/\(~(genls (c_tptpcol_13_18664) (c_tptpcol_12_18663))))); [ zenon_intro zenon_H154 | zenon_intro zenon_H155 ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_H154). zenon_intro zenon_H157. zenon_intro zenon_H156. % 2.66/2.82 exact (zenon_H156 just29). % 2.66/2.82 cut ((genls (c_tptpcol_12_18663) (c_tptpcol_11_18631)) = (genls (c_tptpcol_13_18664) (c_tptpcol_11_18631))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H152. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just27. % 2.66/2.82 cut (((c_tptpcol_11_18631) = (c_tptpcol_11_18631))); [idtac | apply NNPP; zenon_intro zenon_H13e]. % 2.66/2.82 cut (((c_tptpcol_12_18663) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H158]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H155); [ zenon_intro zenon_H15a | zenon_intro zenon_H159 ]. % 2.66/2.82 apply zenon_H15a. zenon_intro zenon_H15b. % 2.66/2.82 elim (classic ((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [ zenon_intro zenon_H15c | zenon_intro zenon_H15d ]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664)) = ((c_tptpcol_12_18663) = (c_tptpcol_13_18664))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H158. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_H15c. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H15d]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_12_18663))); [idtac | apply NNPP; zenon_intro zenon_H157]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_H157 zenon_H15b). % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H159. zenon_intro just29. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_18664)). zenon_intro zenon_H15e. % 2.66/2.82 generalize (zenon_H15e (c_tptpcol_12_18663)). zenon_intro zenon_H15f. % 2.66/2.82 generalize (zenon_H15f (c_tptpcol_11_18631)). zenon_intro zenon_H160. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H160); [ zenon_intro zenon_H156 | zenon_intro zenon_H161 ]. % 2.66/2.82 exact (zenon_H156 just29). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H161); [ zenon_intro zenon_H163 | zenon_intro zenon_H162 ]. % 2.66/2.82 exact (zenon_H163 just27). % 2.66/2.82 exact (zenon_H152 zenon_H162). % 2.66/2.82 apply zenon_H13e. apply refl_equal. % 2.66/2.82 cut ((genls (c_tptpcol_11_18631) (c_tptpcol_10_18567)) = (genls (c_tptpcol_13_18664) (c_tptpcol_10_18567))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H14e. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just25. % 2.66/2.82 cut (((c_tptpcol_10_18567) = (c_tptpcol_10_18567))); [idtac | apply NNPP; zenon_intro zenon_H13f]. % 2.66/2.82 cut (((c_tptpcol_11_18631) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H164]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H151); [ zenon_intro zenon_H166 | zenon_intro zenon_H165 ]. % 2.66/2.82 apply zenon_H166. zenon_intro zenon_H167. % 2.66/2.82 elim (classic ((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [ zenon_intro zenon_H15c | zenon_intro zenon_H15d ]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664)) = ((c_tptpcol_11_18631) = (c_tptpcol_13_18664))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H164. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_H15c. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H15d]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_11_18631))); [idtac | apply NNPP; zenon_intro zenon_H153]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_H153 zenon_H167). % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H165. zenon_intro zenon_H162. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_18664)). zenon_intro zenon_H15e. % 2.66/2.82 generalize (zenon_H15e (c_tptpcol_11_18631)). zenon_intro zenon_H168. % 2.66/2.82 generalize (zenon_H168 (c_tptpcol_10_18567)). zenon_intro zenon_H169. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H169); [ zenon_intro zenon_H152 | zenon_intro zenon_H16a ]. % 2.66/2.82 exact (zenon_H152 zenon_H162). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H16a); [ zenon_intro zenon_H16c | zenon_intro zenon_H16b ]. % 2.66/2.82 exact (zenon_H16c just25). % 2.66/2.82 exact (zenon_H14e zenon_H16b). % 2.66/2.82 apply zenon_H13f. apply refl_equal. % 2.66/2.82 cut ((genls (c_tptpcol_10_18567) (c_tptpcol_9_18439)) = (genls (c_tptpcol_13_18664) (c_tptpcol_9_18439))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H14a. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just23. % 2.66/2.82 cut (((c_tptpcol_9_18439) = (c_tptpcol_9_18439))); [idtac | apply NNPP; zenon_intro zenon_H140]. % 2.66/2.82 cut (((c_tptpcol_10_18567) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H16d]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H14d); [ zenon_intro zenon_H16f | zenon_intro zenon_H16e ]. % 2.66/2.82 apply zenon_H16f. zenon_intro zenon_H170. % 2.66/2.82 elim (classic ((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [ zenon_intro zenon_H15c | zenon_intro zenon_H15d ]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664)) = ((c_tptpcol_10_18567) = (c_tptpcol_13_18664))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H16d. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_H15c. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H15d]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_10_18567))); [idtac | apply NNPP; zenon_intro zenon_H14f]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_H14f zenon_H170). % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H16e. zenon_intro zenon_H16b. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_18664)). zenon_intro zenon_H15e. % 2.66/2.82 generalize (zenon_H15e (c_tptpcol_10_18567)). zenon_intro zenon_H171. % 2.66/2.82 generalize (zenon_H171 (c_tptpcol_9_18439)). zenon_intro zenon_H172. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H172); [ zenon_intro zenon_H14e | zenon_intro zenon_H173 ]. % 2.66/2.82 exact (zenon_H14e zenon_H16b). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H173); [ zenon_intro zenon_H175 | zenon_intro zenon_H174 ]. % 2.66/2.82 exact (zenon_H175 just23). % 2.66/2.82 exact (zenon_H14a zenon_H174). % 2.66/2.82 apply zenon_H140. apply refl_equal. % 2.66/2.82 cut ((genls (c_tptpcol_9_18439) (c_tptpcol_8_18438)) = (genls (c_tptpcol_13_18664) (c_tptpcol_8_18438))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H146. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just21. % 2.66/2.82 cut (((c_tptpcol_8_18438) = (c_tptpcol_8_18438))); [idtac | apply NNPP; zenon_intro zenon_H141]. % 2.66/2.82 cut (((c_tptpcol_9_18439) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H176]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H149); [ zenon_intro zenon_H178 | zenon_intro zenon_H177 ]. % 2.66/2.82 apply zenon_H178. zenon_intro zenon_H179. % 2.66/2.82 elim (classic ((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [ zenon_intro zenon_H15c | zenon_intro zenon_H15d ]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664)) = ((c_tptpcol_9_18439) = (c_tptpcol_13_18664))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H176. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_H15c. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H15d]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_9_18439))); [idtac | apply NNPP; zenon_intro zenon_H14b]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_H14b zenon_H179). % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H177. zenon_intro zenon_H174. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_18664)). zenon_intro zenon_H15e. % 2.66/2.82 generalize (zenon_H15e (c_tptpcol_9_18439)). zenon_intro zenon_H17a. % 2.66/2.82 generalize (zenon_H17a (c_tptpcol_8_18438)). zenon_intro zenon_H17b. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H17b); [ zenon_intro zenon_H14a | zenon_intro zenon_H17c ]. % 2.66/2.82 exact (zenon_H14a zenon_H174). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H17c); [ zenon_intro zenon_H17e | zenon_intro zenon_H17d ]. % 2.66/2.82 exact (zenon_H17e just21). % 2.66/2.82 exact (zenon_H146 zenon_H17d). % 2.66/2.82 apply zenon_H141. apply refl_equal. % 2.66/2.82 cut ((genls (c_tptpcol_8_18438) (c_tptpcol_7_18437)) = (genls (c_tptpcol_13_18664) (c_tptpcol_7_18437))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H143. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just19. % 2.66/2.82 cut (((c_tptpcol_7_18437) = (c_tptpcol_7_18437))); [idtac | apply NNPP; zenon_intro zenon_H142]. % 2.66/2.82 cut (((c_tptpcol_8_18438) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H17f]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H145); [ zenon_intro zenon_H181 | zenon_intro zenon_H180 ]. % 2.66/2.82 apply zenon_H181. zenon_intro zenon_H182. % 2.66/2.82 elim (classic ((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [ zenon_intro zenon_H15c | zenon_intro zenon_H15d ]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664)) = ((c_tptpcol_8_18438) = (c_tptpcol_13_18664))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H17f. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_H15c. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H15d]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_8_18438))); [idtac | apply NNPP; zenon_intro zenon_H147]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_H147 zenon_H182). % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H180. zenon_intro zenon_H17d. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_18664)). zenon_intro zenon_H15e. % 2.66/2.82 generalize (zenon_H15e (c_tptpcol_8_18438)). zenon_intro zenon_H183. % 2.66/2.82 generalize (zenon_H183 (c_tptpcol_7_18437)). zenon_intro zenon_H184. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H184); [ zenon_intro zenon_H146 | zenon_intro zenon_H185 ]. % 2.66/2.82 exact (zenon_H146 zenon_H17d). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H185); [ zenon_intro zenon_H187 | zenon_intro zenon_H186 ]. % 2.66/2.82 exact (zenon_H187 just19). % 2.66/2.82 exact (zenon_H143 zenon_H186). % 2.66/2.82 apply zenon_H142. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L23_ *) % 2.66/2.82 assert (zenon_L24_ : (~((c_tptpcol_6_18436) = (c_tptpcol_6_18436))) -> False). % 2.66/2.82 do 0 intro. intros zenon_H188. % 2.66/2.82 apply zenon_H188. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L24_ *) % 2.66/2.82 assert (zenon_L25_ : (~((c_tptpcol_5_16388) = (c_tptpcol_5_16388))) -> False). % 2.66/2.82 do 0 intro. intros zenon_H189. % 2.66/2.82 apply zenon_H189. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L25_ *) % 2.66/2.82 assert (zenon_L26_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (~(genls (c_tptpcol_13_18664) (c_tptpcol_5_16388))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Ha0 zenon_H18a. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_18664) = (c_tptpcol_6_18436)))/\(~(genls (c_tptpcol_13_18664) (c_tptpcol_6_18436))))); [ zenon_intro zenon_H18b | zenon_intro zenon_H18c ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_H18b). zenon_intro zenon_H18e. zenon_intro zenon_H18d. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_18664) = (c_tptpcol_7_18437)))/\(~(genls (c_tptpcol_13_18664) (c_tptpcol_7_18437))))); [ zenon_intro zenon_H18f | zenon_intro zenon_H190 ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_H18f). zenon_intro zenon_H191. zenon_intro zenon_H143. % 2.66/2.82 apply (zenon_L23_); trivial. % 2.66/2.82 cut ((genls (c_tptpcol_7_18437) (c_tptpcol_6_18436)) = (genls (c_tptpcol_13_18664) (c_tptpcol_6_18436))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H18d. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just17. % 2.66/2.82 cut (((c_tptpcol_6_18436) = (c_tptpcol_6_18436))); [idtac | apply NNPP; zenon_intro zenon_H188]. % 2.66/2.82 cut (((c_tptpcol_7_18437) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H192]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H190); [ zenon_intro zenon_H194 | zenon_intro zenon_H193 ]. % 2.66/2.82 apply zenon_H194. zenon_intro zenon_H195. % 2.66/2.82 elim (classic ((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [ zenon_intro zenon_H15c | zenon_intro zenon_H15d ]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664)) = ((c_tptpcol_7_18437) = (c_tptpcol_13_18664))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H192. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_H15c. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H15d]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_7_18437))); [idtac | apply NNPP; zenon_intro zenon_H191]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_H191 zenon_H195). % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H193. zenon_intro zenon_H186. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_18664)). zenon_intro zenon_H15e. % 2.66/2.82 generalize (zenon_H15e (c_tptpcol_7_18437)). zenon_intro zenon_H196. % 2.66/2.82 generalize (zenon_H196 (c_tptpcol_6_18436)). zenon_intro zenon_H197. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H197); [ zenon_intro zenon_H143 | zenon_intro zenon_H198 ]. % 2.66/2.82 exact (zenon_H143 zenon_H186). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H198); [ zenon_intro zenon_H19a | zenon_intro zenon_H199 ]. % 2.66/2.82 exact (zenon_H19a just17). % 2.66/2.82 exact (zenon_H18d zenon_H199). % 2.66/2.82 apply zenon_H188. apply refl_equal. % 2.66/2.82 cut ((genls (c_tptpcol_6_18436) (c_tptpcol_5_16388)) = (genls (c_tptpcol_13_18664) (c_tptpcol_5_16388))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H18a. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just15. % 2.66/2.82 cut (((c_tptpcol_5_16388) = (c_tptpcol_5_16388))); [idtac | apply NNPP; zenon_intro zenon_H189]. % 2.66/2.82 cut (((c_tptpcol_6_18436) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H19b]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H18c); [ zenon_intro zenon_H19d | zenon_intro zenon_H19c ]. % 2.66/2.82 apply zenon_H19d. zenon_intro zenon_H19e. % 2.66/2.82 elim (classic ((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [ zenon_intro zenon_H15c | zenon_intro zenon_H15d ]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664)) = ((c_tptpcol_6_18436) = (c_tptpcol_13_18664))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H19b. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_H15c. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H15d]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_6_18436))); [idtac | apply NNPP; zenon_intro zenon_H18e]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_H18e zenon_H19e). % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H19c. zenon_intro zenon_H199. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_18664)). zenon_intro zenon_H15e. % 2.66/2.82 generalize (zenon_H15e (c_tptpcol_6_18436)). zenon_intro zenon_H19f. % 2.66/2.82 generalize (zenon_H19f (c_tptpcol_5_16388)). zenon_intro zenon_H1a0. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H1a0); [ zenon_intro zenon_H18d | zenon_intro zenon_H1a1 ]. % 2.66/2.82 exact (zenon_H18d zenon_H199). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H1a1); [ zenon_intro zenon_H1a3 | zenon_intro zenon_H1a2 ]. % 2.66/2.82 exact (zenon_H1a3 just15). % 2.66/2.82 exact (zenon_H18a zenon_H1a2). % 2.66/2.82 apply zenon_H189. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L26_ *) % 2.66/2.82 assert (zenon_L27_ : (~((c_tptpcol_4_16387) = (c_tptpcol_4_16387))) -> False). % 2.66/2.82 do 0 intro. intros zenon_H1a4. % 2.66/2.82 apply zenon_H1a4. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L27_ *) % 2.66/2.82 assert (zenon_L28_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (~(genls (c_tptpcol_13_18664) (c_tptpcol_4_16387))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Ha0 zenon_H1a5. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_18664) = (c_tptpcol_5_16388)))/\(~(genls (c_tptpcol_13_18664) (c_tptpcol_5_16388))))); [ zenon_intro zenon_H1a6 | zenon_intro zenon_H1a7 ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_H1a6). zenon_intro zenon_H1a8. zenon_intro zenon_H18a. % 2.66/2.82 apply (zenon_L26_); trivial. % 2.66/2.82 cut ((genls (c_tptpcol_5_16388) (c_tptpcol_4_16387)) = (genls (c_tptpcol_13_18664) (c_tptpcol_4_16387))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H1a5. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just13. % 2.66/2.82 cut (((c_tptpcol_4_16387) = (c_tptpcol_4_16387))); [idtac | apply NNPP; zenon_intro zenon_H1a4]. % 2.66/2.82 cut (((c_tptpcol_5_16388) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H1a9]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H1a7); [ zenon_intro zenon_H1ab | zenon_intro zenon_H1aa ]. % 2.66/2.82 apply zenon_H1ab. zenon_intro zenon_H1ac. % 2.66/2.82 elim (classic ((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [ zenon_intro zenon_H15c | zenon_intro zenon_H15d ]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664)) = ((c_tptpcol_5_16388) = (c_tptpcol_13_18664))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H1a9. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_H15c. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H15d]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_5_16388))); [idtac | apply NNPP; zenon_intro zenon_H1a8]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_H1a8 zenon_H1ac). % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H1aa. zenon_intro zenon_H1a2. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_18664)). zenon_intro zenon_H15e. % 2.66/2.82 generalize (zenon_H15e (c_tptpcol_5_16388)). zenon_intro zenon_H1ad. % 2.66/2.82 generalize (zenon_H1ad (c_tptpcol_4_16387)). zenon_intro zenon_H1ae. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H1ae); [ zenon_intro zenon_H18a | zenon_intro zenon_H1af ]. % 2.66/2.82 exact (zenon_H18a zenon_H1a2). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H1af); [ zenon_intro zenon_H1b1 | zenon_intro zenon_H1b0 ]. % 2.66/2.82 exact (zenon_H1b1 just13). % 2.66/2.82 exact (zenon_H1a5 zenon_H1b0). % 2.66/2.82 apply zenon_H1a4. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L28_ *) % 2.66/2.82 assert (zenon_L29_ : (~((c_tptpcol_3_16386) = (c_tptpcol_3_16386))) -> False). % 2.66/2.82 do 0 intro. intros zenon_H1b2. % 2.66/2.82 apply zenon_H1b2. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L29_ *) % 2.66/2.82 assert (zenon_L30_ : (~((c_tptpcol_2_2) = (c_tptpcol_2_2))) -> False). % 2.66/2.82 do 0 intro. intros zenon_H1b3. % 2.66/2.82 apply zenon_H1b3. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L30_ *) % 2.66/2.82 assert (zenon_L31_ : (~((c_tptpcol_1_1) = (c_tptpcol_1_1))) -> False). % 2.66/2.82 do 0 intro. intros zenon_H1b4. % 2.66/2.82 apply zenon_H1b4. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L31_ *) % 2.66/2.82 assert (zenon_L32_ : (~((c_tptpcol_13_93766) = (c_tptpcol_13_93766))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Hab. % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L32_ *) % 2.66/2.82 assert (zenon_L33_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (~(genls (c_tptpcol_15_93775) (c_tptpcol_13_93766))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Ha0 zenon_H1b5. % 2.66/2.82 elim (classic ((~((c_tptpcol_15_93775) = (c_tptpcol_14_93774)))/\(~(genls (c_tptpcol_15_93775) (c_tptpcol_14_93774))))); [ zenon_intro zenon_H1b6 | zenon_intro zenon_H1b7 ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_H1b6). zenon_intro zenon_H1b9. zenon_intro zenon_H1b8. % 2.66/2.82 exact (zenon_H1b8 just57). % 2.66/2.82 cut ((genls (c_tptpcol_14_93774) (c_tptpcol_13_93766)) = (genls (c_tptpcol_15_93775) (c_tptpcol_13_93766))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H1b5. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just55. % 2.66/2.82 cut (((c_tptpcol_13_93766) = (c_tptpcol_13_93766))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 2.66/2.82 cut (((c_tptpcol_14_93774) = (c_tptpcol_15_93775))); [idtac | apply NNPP; zenon_intro zenon_H1ba]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H1b7); [ zenon_intro zenon_H1bc | zenon_intro zenon_H1bb ]. % 2.66/2.82 apply zenon_H1bc. zenon_intro zenon_H1bd. % 2.66/2.82 elim (classic ((c_tptpcol_15_93775) = (c_tptpcol_15_93775))); [ zenon_intro zenon_H1be | zenon_intro zenon_H1bf ]. % 2.66/2.82 cut (((c_tptpcol_15_93775) = (c_tptpcol_15_93775)) = ((c_tptpcol_14_93774) = (c_tptpcol_15_93775))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H1ba. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_H1be. % 2.66/2.82 cut (((c_tptpcol_15_93775) = (c_tptpcol_15_93775))); [idtac | apply NNPP; zenon_intro zenon_H1bf]. % 2.66/2.82 cut (((c_tptpcol_15_93775) = (c_tptpcol_14_93774))); [idtac | apply NNPP; zenon_intro zenon_H1b9]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_H1b9 zenon_H1bd). % 2.66/2.82 apply zenon_H1bf. apply refl_equal. % 2.66/2.82 apply zenon_H1bf. apply refl_equal. % 2.66/2.82 apply zenon_H1bb. zenon_intro just57. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_15_93775)). zenon_intro zenon_H1c0. % 2.66/2.82 generalize (zenon_H1c0 (c_tptpcol_14_93774)). zenon_intro zenon_H1c1. % 2.66/2.82 generalize (zenon_H1c1 (c_tptpcol_13_93766)). zenon_intro zenon_H1c2. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H1c2); [ zenon_intro zenon_H1b8 | zenon_intro zenon_H1c3 ]. % 2.66/2.82 exact (zenon_H1b8 just57). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H1c3); [ zenon_intro zenon_H1c5 | zenon_intro zenon_H1c4 ]. % 2.66/2.82 exact (zenon_H1c5 just55). % 2.66/2.82 exact (zenon_H1b5 zenon_H1c4). % 2.66/2.82 apply zenon_Hab. apply refl_equal. % 2.66/2.82 (* end of lemma zenon_L33_ *) % 2.66/2.82 assert (zenon_L34_ : (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, (((disjointwith (c_tptpcol_13_18664) (c_tptpcol_13_93766))/\(genls NEW (c_tptpcol_13_93766)))->(disjointwith (c_tptpcol_13_18664) NEW))) -> (disjointwith (c_tptpcol_13_18664) (c_tptpcol_13_93766)) -> (~(disjointwith (c_tptpcol_15_93775) (c_tptpcol_13_18664))) -> False). % 2.66/2.82 do 0 intro. intros zenon_Ha0 zenon_H1c6 zenon_H1c7 zenon_H1c8. % 2.66/2.82 generalize (zenon_H1c6 (c_tptpcol_15_93775)). zenon_intro zenon_H1c9. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H1c9); [ zenon_intro zenon_H1cb | zenon_intro zenon_H1ca ]. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H1cb); [ zenon_intro zenon_H1cc | zenon_intro zenon_H1b5 ]. % 2.66/2.82 exact (zenon_H1cc zenon_H1c7). % 2.66/2.82 apply (zenon_L33_); trivial. % 2.66/2.82 generalize (just76 (c_tptpcol_13_18664)). zenon_intro zenon_H1cd. % 2.66/2.82 generalize (zenon_H1cd (c_tptpcol_15_93775)). zenon_intro zenon_H1ce. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H1ce); [ zenon_intro zenon_H1d0 | zenon_intro zenon_H1cf ]. % 2.66/2.82 exact (zenon_H1d0 zenon_H1ca). % 2.66/2.82 exact (zenon_H1c8 zenon_H1cf). % 2.66/2.82 (* end of lemma zenon_L34_ *) % 2.66/2.82 assert (zenon_L35_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (~(disjointwith (c_tptpcol_15_93775) (c_tptpcol_13_18664))) -> (genls (c_tptpcol_13_93766) (c_tptpcol_13_93766)) -> (disjointwith (c_tptpcol_1_65536) (c_tptpcol_13_18664)) -> False). % 2.66/2.82 do 0 intro. intros zenon_Ha0 zenon_H1c8 zenon_H1d1 zenon_H1d2. % 2.66/2.82 generalize (just77 (c_tptpcol_13_18664)). zenon_intro zenon_H1d3. % 2.66/2.82 generalize (zenon_H1d3 (c_tptpcol_13_93766)). zenon_intro zenon_H1c6. % 2.66/2.82 generalize (zenon_H1d3 (c_tptpcol_1_65536)). zenon_intro zenon_H1d4. % 2.66/2.82 generalize (zenon_H1c6 (c_tptpcol_13_93766)). zenon_intro zenon_H1d5. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H1d5); [ zenon_intro zenon_H1d6 | zenon_intro zenon_H1c7 ]. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H1d6); [ zenon_intro zenon_H1cc | zenon_intro zenon_H1d7 ]. % 2.66/2.82 generalize (zenon_H1d4 (c_tptpcol_13_93766)). zenon_intro zenon_H1d8. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H1d8); [ zenon_intro zenon_H1d9 | zenon_intro zenon_H1c7 ]. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H1d9); [ zenon_intro zenon_H1da | zenon_intro zenon_H131 ]. % 2.66/2.82 generalize (just76 (c_tptpcol_1_65536)). zenon_intro zenon_H1db. % 2.66/2.82 generalize (zenon_H1db (c_tptpcol_13_18664)). zenon_intro zenon_H1dc. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H1dc); [ zenon_intro zenon_H1de | zenon_intro zenon_H1dd ]. % 2.66/2.82 exact (zenon_H1de zenon_H1d2). % 2.66/2.82 exact (zenon_H1da zenon_H1dd). % 2.66/2.82 apply (zenon_L17_); trivial. % 2.66/2.82 exact (zenon_H1cc zenon_H1c7). % 2.66/2.82 exact (zenon_H1d7 zenon_H1d1). % 2.66/2.82 apply (zenon_L34_); trivial. % 2.66/2.82 (* end of lemma zenon_L35_ *) % 2.66/2.82 assert (zenon_L36_ : (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, (((disjointwith (c_tptpcol_1_65536) (c_tptpcol_1_1))/\(genls NEW (c_tptpcol_1_1)))->(disjointwith (c_tptpcol_1_65536) NEW))) -> (~(disjointwith (c_tptpcol_15_93775) (c_tptpcol_13_18664))) -> (genls (c_tptpcol_13_93766) (c_tptpcol_13_93766)) -> False). % 2.66/2.82 do 0 intro. intros zenon_Ha0 zenon_H1df zenon_H1c8 zenon_H1d1. % 2.66/2.82 generalize (zenon_H1df (c_tptpcol_13_18664)). zenon_intro zenon_H1e0. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H1e0); [ zenon_intro zenon_H1e1 | zenon_intro zenon_H1d2 ]. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H1e1); [ zenon_intro zenon_H1e3 | zenon_intro zenon_H1e2 ]. % 2.66/2.82 generalize (just76 (c_tptpcol_1_1)). zenon_intro zenon_H1e4. % 2.66/2.82 generalize (zenon_H1e4 (c_tptpcol_1_65536)). zenon_intro zenon_H1e5. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H1e5); [ zenon_intro zenon_H1e7 | zenon_intro zenon_H1e6 ]. % 2.66/2.82 exact (zenon_H1e7 just59). % 2.66/2.82 exact (zenon_H1e3 zenon_H1e6). % 2.66/2.82 elim (classic ((~((c_tptpcol_13_18664) = (c_tptpcol_2_2)))/\(~(genls (c_tptpcol_13_18664) (c_tptpcol_2_2))))); [ zenon_intro zenon_H1e8 | zenon_intro zenon_H1e9 ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_H1e8). zenon_intro zenon_H1eb. zenon_intro zenon_H1ea. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_18664) = (c_tptpcol_3_16386)))/\(~(genls (c_tptpcol_13_18664) (c_tptpcol_3_16386))))); [ zenon_intro zenon_H1ec | zenon_intro zenon_H1ed ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_H1ec). zenon_intro zenon_H1ef. zenon_intro zenon_H1ee. % 2.66/2.82 elim (classic ((~((c_tptpcol_13_18664) = (c_tptpcol_4_16387)))/\(~(genls (c_tptpcol_13_18664) (c_tptpcol_4_16387))))); [ zenon_intro zenon_H1f0 | zenon_intro zenon_H1f1 ]. % 2.66/2.82 apply (zenon_and_s _ _ zenon_H1f0). zenon_intro zenon_H1f2. zenon_intro zenon_H1a5. % 2.66/2.82 apply (zenon_L28_); trivial. % 2.66/2.82 cut ((genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) = (genls (c_tptpcol_13_18664) (c_tptpcol_3_16386))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H1ee. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just11. % 2.66/2.82 cut (((c_tptpcol_3_16386) = (c_tptpcol_3_16386))); [idtac | apply NNPP; zenon_intro zenon_H1b2]. % 2.66/2.82 cut (((c_tptpcol_4_16387) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H1f3]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H1f1); [ zenon_intro zenon_H1f5 | zenon_intro zenon_H1f4 ]. % 2.66/2.82 apply zenon_H1f5. zenon_intro zenon_H1f6. % 2.66/2.82 elim (classic ((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [ zenon_intro zenon_H15c | zenon_intro zenon_H15d ]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664)) = ((c_tptpcol_4_16387) = (c_tptpcol_13_18664))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H1f3. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_H15c. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H15d]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_4_16387))); [idtac | apply NNPP; zenon_intro zenon_H1f2]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_H1f2 zenon_H1f6). % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H1f4. zenon_intro zenon_H1b0. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_18664)). zenon_intro zenon_H15e. % 2.66/2.82 generalize (zenon_H15e (c_tptpcol_4_16387)). zenon_intro zenon_H1f7. % 2.66/2.82 generalize (zenon_H1f7 (c_tptpcol_3_16386)). zenon_intro zenon_H1f8. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H1f8); [ zenon_intro zenon_H1a5 | zenon_intro zenon_H1f9 ]. % 2.66/2.82 exact (zenon_H1a5 zenon_H1b0). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H1f9); [ zenon_intro zenon_H1fb | zenon_intro zenon_H1fa ]. % 2.66/2.82 exact (zenon_H1fb just11). % 2.66/2.82 exact (zenon_H1ee zenon_H1fa). % 2.66/2.82 apply zenon_H1b2. apply refl_equal. % 2.66/2.82 cut ((genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) = (genls (c_tptpcol_13_18664) (c_tptpcol_2_2))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H1ea. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just9. % 2.66/2.82 cut (((c_tptpcol_2_2) = (c_tptpcol_2_2))); [idtac | apply NNPP; zenon_intro zenon_H1b3]. % 2.66/2.82 cut (((c_tptpcol_3_16386) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H1fc]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H1ed); [ zenon_intro zenon_H1fe | zenon_intro zenon_H1fd ]. % 2.66/2.82 apply zenon_H1fe. zenon_intro zenon_H1ff. % 2.66/2.82 elim (classic ((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [ zenon_intro zenon_H15c | zenon_intro zenon_H15d ]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664)) = ((c_tptpcol_3_16386) = (c_tptpcol_13_18664))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H1fc. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_H15c. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H15d]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_3_16386))); [idtac | apply NNPP; zenon_intro zenon_H1ef]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_H1ef zenon_H1ff). % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H1fd. zenon_intro zenon_H1fa. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_18664)). zenon_intro zenon_H15e. % 2.66/2.82 generalize (zenon_H15e (c_tptpcol_3_16386)). zenon_intro zenon_H200. % 2.66/2.82 generalize (zenon_H200 (c_tptpcol_2_2)). zenon_intro zenon_H201. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H201); [ zenon_intro zenon_H1ee | zenon_intro zenon_H202 ]. % 2.66/2.82 exact (zenon_H1ee zenon_H1fa). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H202); [ zenon_intro zenon_H204 | zenon_intro zenon_H203 ]. % 2.66/2.82 exact (zenon_H204 just9). % 2.66/2.82 exact (zenon_H1ea zenon_H203). % 2.66/2.82 apply zenon_H1b3. apply refl_equal. % 2.66/2.82 cut ((genls (c_tptpcol_2_2) (c_tptpcol_1_1)) = (genls (c_tptpcol_13_18664) (c_tptpcol_1_1))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H1e2. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact just7. % 2.66/2.82 cut (((c_tptpcol_1_1) = (c_tptpcol_1_1))); [idtac | apply NNPP; zenon_intro zenon_H1b4]. % 2.66/2.82 cut (((c_tptpcol_2_2) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H205]. % 2.66/2.82 congruence. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H1e9); [ zenon_intro zenon_H207 | zenon_intro zenon_H206 ]. % 2.66/2.82 apply zenon_H207. zenon_intro zenon_H208. % 2.66/2.82 elim (classic ((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [ zenon_intro zenon_H15c | zenon_intro zenon_H15d ]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664)) = ((c_tptpcol_2_2) = (c_tptpcol_13_18664))). % 2.66/2.82 intro zenon_D_pnotp. % 2.66/2.82 apply zenon_H205. % 2.66/2.82 rewrite <- zenon_D_pnotp. % 2.66/2.82 exact zenon_H15c. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_13_18664))); [idtac | apply NNPP; zenon_intro zenon_H15d]. % 2.66/2.82 cut (((c_tptpcol_13_18664) = (c_tptpcol_2_2))); [idtac | apply NNPP; zenon_intro zenon_H1eb]. % 2.66/2.82 congruence. % 2.66/2.82 exact (zenon_H1eb zenon_H208). % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H15d. apply refl_equal. % 2.66/2.82 apply zenon_H206. zenon_intro zenon_H203. % 2.66/2.82 generalize (zenon_Ha0 (c_tptpcol_13_18664)). zenon_intro zenon_H15e. % 2.66/2.82 generalize (zenon_H15e (c_tptpcol_2_2)). zenon_intro zenon_H209. % 2.66/2.82 generalize (zenon_H209 (c_tptpcol_1_1)). zenon_intro zenon_H20a. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H20a); [ zenon_intro zenon_H1ea | zenon_intro zenon_H20b ]. % 2.66/2.82 exact (zenon_H1ea zenon_H203). % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H20b); [ zenon_intro zenon_H20d | zenon_intro zenon_H20c ]. % 2.66/2.82 exact (zenon_H20d just7). % 2.66/2.82 exact (zenon_H1e2 zenon_H20c). % 2.66/2.82 apply zenon_H1b4. apply refl_equal. % 2.66/2.82 apply (zenon_L35_); trivial. % 2.66/2.82 (* end of lemma zenon_L36_ *) % 2.66/2.82 apply NNPP. intro zenon_G. % 2.66/2.82 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_Ha0 | zenon_intro zenon_H20e ]. % 2.66/2.82 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H20f. zenon_intro zenon_H1c8. % 2.66/2.82 generalize (just78 (c_tptpcol_1_65536)). zenon_intro zenon_H210. % 2.66/2.82 generalize (just77 (c_tptpcol_1_65536)). zenon_intro zenon_H211. % 2.66/2.82 generalize (just75 (c_tptpcol_13_93766)). zenon_intro zenon_H212. % 2.66/2.82 generalize (zenon_H211 (c_tptpcol_1_1)). zenon_intro zenon_H1df. % 2.66/2.82 generalize (zenon_H211 (c_tptpcol_2_2)). zenon_intro zenon_H213. % 2.66/2.82 generalize (just140 (c_tptpcol_13_93766)). zenon_intro zenon_H214. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H214); [ zenon_intro zenon_H215 | zenon_intro zenon_H1d1 ]. % 2.66/2.82 generalize (zenon_H212 (c_tptpcol_3_16386)). zenon_intro zenon_H216. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H216); [ zenon_intro zenon_H218 | zenon_intro zenon_H217 ]. % 2.66/2.82 generalize (zenon_H210 (c_tptpcol_3_16386)). zenon_intro zenon_H219. % 2.66/2.82 generalize (zenon_H213 (c_tptpcol_3_16386)). zenon_intro zenon_H21a. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H21a); [ zenon_intro zenon_H21c | zenon_intro zenon_H21b ]. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H21c); [ zenon_intro zenon_H21d | zenon_intro zenon_H204 ]. % 2.66/2.82 generalize (zenon_H1df (c_tptpcol_2_2)). zenon_intro zenon_H21e. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H21e); [ zenon_intro zenon_H220 | zenon_intro zenon_H21f ]. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H220); [ zenon_intro zenon_H1e3 | zenon_intro zenon_H20d ]. % 2.66/2.82 generalize (just76 (c_tptpcol_1_1)). zenon_intro zenon_H1e4. % 2.66/2.82 generalize (zenon_H1e4 (c_tptpcol_1_65536)). zenon_intro zenon_H1e5. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H1e5); [ zenon_intro zenon_H1e7 | zenon_intro zenon_H1e6 ]. % 2.66/2.82 exact (zenon_H1e7 just59). % 2.66/2.82 exact (zenon_H1e3 zenon_H1e6). % 2.66/2.82 exact (zenon_H20d just7). % 2.66/2.82 exact (zenon_H21d zenon_H21f). % 2.66/2.82 exact (zenon_H204 just9). % 2.66/2.82 generalize (zenon_H219 (c_tptpcol_13_93766)). zenon_intro zenon_H221. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H221); [ zenon_intro zenon_H223 | zenon_intro zenon_H222 ]. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H223); [ zenon_intro zenon_H224 | zenon_intro zenon_H131 ]. % 2.66/2.82 exact (zenon_H224 zenon_H21b). % 2.66/2.82 apply (zenon_L17_); trivial. % 2.66/2.82 exact (zenon_H218 zenon_H222). % 2.66/2.82 exact (zenon_H215 zenon_H217). % 2.66/2.82 apply (zenon_L36_); trivial. % 2.66/2.82 apply zenon_H20e. zenon_intro zenon_Tx_vd. apply NNPP. zenon_intro zenon_H226. % 2.66/2.82 apply zenon_H226. zenon_intro zenon_Ty_vf. apply NNPP. zenon_intro zenon_H228. % 2.66/2.82 apply zenon_H228. zenon_intro zenon_Tz_vh. apply NNPP. zenon_intro zenon_H22a. % 2.66/2.82 apply (zenon_notimply_s _ _ zenon_H22a). zenon_intro zenon_H22c. zenon_intro zenon_H22b. % 2.66/2.82 apply (zenon_notimply_s _ _ zenon_H22b). zenon_intro zenon_H22e. zenon_intro zenon_H22d. % 2.66/2.82 generalize (just139 zenon_Tx_vd). zenon_intro zenon_H22f. % 2.66/2.82 generalize (zenon_H22f zenon_Ty_vf). zenon_intro zenon_H230. % 2.66/2.82 generalize (zenon_H230 zenon_Tz_vh). zenon_intro zenon_H231. % 2.66/2.82 apply (zenon_imply_s _ _ zenon_H231); [ zenon_intro zenon_H233 | zenon_intro zenon_H232 ]. % 2.66/2.82 apply (zenon_notand_s _ _ zenon_H233); [ zenon_intro zenon_H235 | zenon_intro zenon_H234 ]. % 2.66/2.82 exact (zenon_H235 zenon_H22c). % 2.66/2.82 exact (zenon_H234 zenon_H22e). % 2.66/2.82 exact (zenon_H22d zenon_H232). % 2.66/2.82 Qed. % 2.66/2.82 % SZS output end Proof % 2.66/2.82 (* END-PROOF *) % 2.66/2.82 nodes searched: 91065 % 2.66/2.82 max branch formulas: 14990 % 2.66/2.82 proof nodes created: 331 % 2.66/2.82 formulas created: 426935 % 2.66/2.82 %------------------------------------------------------------------------------