%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR049+1 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n027.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:10 EDT 2022 % Result : Theorem 0.70s 0.90s % Output : Proof 0.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : CSR049+1 : TPTP v8.1.0. Released v3.4.0. % 0.07/0.13 % Command : run_zenon %s %d % 0.13/0.34 % Computer : n027.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 13:57:59 EDT 2022 % 0.13/0.35 % CPUTime : % 0.70/0.90 (* PROOF-FOUND *) % 0.70/0.90 % SZS status Theorem % 0.70/0.90 (* BEGIN-PROOF *) % 0.70/0.90 % SZS output start Proof % 0.70/0.90 Theorem query49 : ((mtvisible (c_unitedstatesgeographypeoplemt))->(disjointwith (c_tptpcol_16_26926) (c_tptpcol_16_92269))). % 0.70/0.90 Proof. % 0.70/0.90 assert (zenon_L1_ : (~((c_tptpcol_6_92162) = (c_tptpcol_6_92162))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Ha5. % 0.70/0.90 apply zenon_Ha5. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L1_ *) % 0.70/0.90 assert (zenon_L2_ : (~((c_tptpcol_5_90114) = (c_tptpcol_5_90114))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Ha6. % 0.70/0.90 apply zenon_Ha6. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L2_ *) % 0.70/0.90 assert (zenon_L3_ : (~((c_tptpcol_4_90113) = (c_tptpcol_4_90113))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Ha7. % 0.70/0.90 apply zenon_Ha7. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L3_ *) % 0.70/0.90 assert (zenon_L4_ : (~((c_tptpcol_3_81921) = (c_tptpcol_3_81921))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Ha8. % 0.70/0.90 apply zenon_Ha8. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L4_ *) % 0.70/0.90 assert (zenon_L5_ : (~((c_tptpcol_2_65537) = (c_tptpcol_2_65537))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Ha9. % 0.70/0.90 apply zenon_Ha9. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L5_ *) % 0.70/0.90 assert (zenon_L6_ : (~((c_tptpcol_1_65536) = (c_tptpcol_1_65536))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Haa. % 0.70/0.90 apply zenon_Haa. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L6_ *) % 0.70/0.90 assert (zenon_L7_ : (~((c_tptpcol_11_92230) = (c_tptpcol_11_92230))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hab. % 0.70/0.90 apply zenon_Hab. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L7_ *) % 0.70/0.90 assert (zenon_L8_ : (~((c_tptpcol_10_92166) = (c_tptpcol_10_92166))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hac. % 0.70/0.90 apply zenon_Hac. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L8_ *) % 0.70/0.90 assert (zenon_L9_ : (~((c_tptpcol_9_92165) = (c_tptpcol_9_92165))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Had. % 0.70/0.90 apply zenon_Had. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L9_ *) % 0.70/0.90 assert (zenon_L10_ : (~((c_tptpcol_8_92164) = (c_tptpcol_8_92164))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hae. % 0.70/0.90 apply zenon_Hae. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L10_ *) % 0.70/0.90 assert (zenon_L11_ : (~((c_tptpcol_14_92264) = (c_tptpcol_14_92264))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Haf. % 0.70/0.90 apply zenon_Haf. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L11_ *) % 0.70/0.90 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_16_92269) (c_tptpcol_14_92264))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hb0 zenon_Hb1. % 0.70/0.90 elim (classic ((~((c_tptpcol_16_92269) = (c_tptpcol_15_92268)))/\(~(genls (c_tptpcol_16_92269) (c_tptpcol_15_92268))))); [ zenon_intro zenon_Hb2 | zenon_intro zenon_Hb3 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_Hb2). zenon_intro zenon_Hb5. zenon_intro zenon_Hb4. % 0.70/0.90 exact (zenon_Hb4 just65). % 0.70/0.90 cut ((genls (c_tptpcol_15_92268) (c_tptpcol_14_92264)) = (genls (c_tptpcol_16_92269) (c_tptpcol_14_92264))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_Hb1. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just63. % 0.70/0.90 cut (((c_tptpcol_14_92264) = (c_tptpcol_14_92264))); [idtac | apply NNPP; zenon_intro zenon_Haf]. % 0.70/0.90 cut (((c_tptpcol_15_92268) = (c_tptpcol_16_92269))); [idtac | apply NNPP; zenon_intro zenon_Hb6]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_Hb3); [ zenon_intro zenon_Hb8 | zenon_intro zenon_Hb7 ]. % 0.70/0.90 apply zenon_Hb8. zenon_intro zenon_Hb9. % 0.70/0.90 elim (classic ((c_tptpcol_16_92269) = (c_tptpcol_16_92269))); [ zenon_intro zenon_Hba | zenon_intro zenon_Hbb ]. % 0.70/0.90 cut (((c_tptpcol_16_92269) = (c_tptpcol_16_92269)) = ((c_tptpcol_15_92268) = (c_tptpcol_16_92269))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_Hb6. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_Hba. % 0.70/0.90 cut (((c_tptpcol_16_92269) = (c_tptpcol_16_92269))); [idtac | apply NNPP; zenon_intro zenon_Hbb]. % 0.70/0.90 cut (((c_tptpcol_16_92269) = (c_tptpcol_15_92268))); [idtac | apply NNPP; zenon_intro zenon_Hb5]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_Hb5 zenon_Hb9). % 0.70/0.90 apply zenon_Hbb. apply refl_equal. % 0.70/0.90 apply zenon_Hbb. apply refl_equal. % 0.70/0.90 apply zenon_Hb7. zenon_intro just65. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_16_92269)). zenon_intro zenon_Hbc. % 0.70/0.90 generalize (zenon_Hbc (c_tptpcol_15_92268)). zenon_intro zenon_Hbd. % 0.70/0.90 generalize (zenon_Hbd (c_tptpcol_14_92264)). zenon_intro zenon_Hbe. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_Hbe); [ zenon_intro zenon_Hb4 | zenon_intro zenon_Hbf ]. % 0.70/0.90 exact (zenon_Hb4 just65). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_Hbf); [ zenon_intro zenon_Hc1 | zenon_intro zenon_Hc0 ]. % 0.70/0.90 exact (zenon_Hc1 just63). % 0.70/0.90 exact (zenon_Hb1 zenon_Hc0). % 0.70/0.90 apply zenon_Haf. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L12_ *) % 0.70/0.90 assert (zenon_L13_ : (~((c_tptpcol_13_92263) = (c_tptpcol_13_92263))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hc2. % 0.70/0.90 apply zenon_Hc2. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L13_ *) % 0.70/0.90 assert (zenon_L14_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (~(genls (c_tptpcol_16_92269) (c_tptpcol_13_92263))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hb0 zenon_Hc3. % 0.70/0.90 elim (classic ((~((c_tptpcol_16_92269) = (c_tptpcol_14_92264)))/\(~(genls (c_tptpcol_16_92269) (c_tptpcol_14_92264))))); [ zenon_intro zenon_Hc4 | zenon_intro zenon_Hc5 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_Hc4). zenon_intro zenon_Hc6. zenon_intro zenon_Hb1. % 0.70/0.90 apply (zenon_L12_); trivial. % 0.70/0.90 cut ((genls (c_tptpcol_14_92264) (c_tptpcol_13_92263)) = (genls (c_tptpcol_16_92269) (c_tptpcol_13_92263))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_Hc3. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just61. % 0.70/0.90 cut (((c_tptpcol_13_92263) = (c_tptpcol_13_92263))); [idtac | apply NNPP; zenon_intro zenon_Hc2]. % 0.70/0.90 cut (((c_tptpcol_14_92264) = (c_tptpcol_16_92269))); [idtac | apply NNPP; zenon_intro zenon_Hc7]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_Hc5); [ zenon_intro zenon_Hc9 | zenon_intro zenon_Hc8 ]. % 0.70/0.90 apply zenon_Hc9. zenon_intro zenon_Hca. % 0.70/0.90 elim (classic ((c_tptpcol_16_92269) = (c_tptpcol_16_92269))); [ zenon_intro zenon_Hba | zenon_intro zenon_Hbb ]. % 0.70/0.90 cut (((c_tptpcol_16_92269) = (c_tptpcol_16_92269)) = ((c_tptpcol_14_92264) = (c_tptpcol_16_92269))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_Hc7. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_Hba. % 0.70/0.90 cut (((c_tptpcol_16_92269) = (c_tptpcol_16_92269))); [idtac | apply NNPP; zenon_intro zenon_Hbb]. % 0.70/0.90 cut (((c_tptpcol_16_92269) = (c_tptpcol_14_92264))); [idtac | apply NNPP; zenon_intro zenon_Hc6]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_Hc6 zenon_Hca). % 0.70/0.90 apply zenon_Hbb. apply refl_equal. % 0.70/0.90 apply zenon_Hbb. apply refl_equal. % 0.70/0.90 apply zenon_Hc8. zenon_intro zenon_Hc0. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_16_92269)). zenon_intro zenon_Hbc. % 0.70/0.90 generalize (zenon_Hbc (c_tptpcol_14_92264)). zenon_intro zenon_Hcb. % 0.70/0.90 generalize (zenon_Hcb (c_tptpcol_13_92263)). zenon_intro zenon_Hcc. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_Hcc); [ zenon_intro zenon_Hb1 | zenon_intro zenon_Hcd ]. % 0.70/0.90 exact (zenon_Hb1 zenon_Hc0). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_Hcd); [ zenon_intro zenon_Hcf | zenon_intro zenon_Hce ]. % 0.70/0.90 exact (zenon_Hcf just61). % 0.70/0.90 exact (zenon_Hc3 zenon_Hce). % 0.70/0.90 apply zenon_Hc2. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L14_ *) % 0.70/0.90 assert (zenon_L15_ : (~((c_tptpcol_14_26921) = (c_tptpcol_14_26921))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hd0. % 0.70/0.90 apply zenon_Hd0. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L15_ *) % 0.70/0.90 assert (zenon_L16_ : (~((c_tptpcol_13_26920) = (c_tptpcol_13_26920))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hd1. % 0.70/0.90 apply zenon_Hd1. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L16_ *) % 0.70/0.90 assert (zenon_L17_ : (~((c_tptpcol_12_26919) = (c_tptpcol_12_26919))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hd2. % 0.70/0.90 apply zenon_Hd2. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L17_ *) % 0.70/0.90 assert (zenon_L18_ : (~((c_tptpcol_11_26887) = (c_tptpcol_11_26887))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hd3. % 0.70/0.90 apply zenon_Hd3. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L18_ *) % 0.70/0.90 assert (zenon_L19_ : (~((c_tptpcol_10_26886) = (c_tptpcol_10_26886))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hd4. % 0.70/0.90 apply zenon_Hd4. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L19_ *) % 0.70/0.90 assert (zenon_L20_ : (~((c_tptpcol_9_26885) = (c_tptpcol_9_26885))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hd5. % 0.70/0.90 apply zenon_Hd5. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L20_ *) % 0.70/0.90 assert (zenon_L21_ : (~((c_tptpcol_8_26629) = (c_tptpcol_8_26629))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hd6. % 0.70/0.90 apply zenon_Hd6. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L21_ *) % 0.70/0.90 assert (zenon_L22_ : (~((c_tptpcol_7_26628) = (c_tptpcol_7_26628))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hd7. % 0.70/0.90 apply zenon_Hd7. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L22_ *) % 0.70/0.90 assert (zenon_L23_ : (~((c_tptpcol_6_26627) = (c_tptpcol_6_26627))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hd8. % 0.70/0.90 apply zenon_Hd8. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L23_ *) % 0.70/0.90 assert (zenon_L24_ : (~((c_tptpcol_5_24579) = (c_tptpcol_5_24579))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hd9. % 0.70/0.90 apply zenon_Hd9. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L24_ *) % 0.70/0.90 assert (zenon_L25_ : (~((c_tptpcol_4_24578) = (c_tptpcol_4_24578))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hda. % 0.70/0.90 apply zenon_Hda. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L25_ *) % 0.70/0.90 assert (zenon_L26_ : (~((c_tptpcol_3_16386) = (c_tptpcol_3_16386))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hdb. % 0.70/0.90 apply zenon_Hdb. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L26_ *) % 0.70/0.90 assert (zenon_L27_ : (~((c_tptpcol_2_2) = (c_tptpcol_2_2))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hdc. % 0.70/0.90 apply zenon_Hdc. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L27_ *) % 0.70/0.90 assert (zenon_L28_ : (~((c_tptpcol_1_1) = (c_tptpcol_1_1))) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hdd. % 0.70/0.90 apply zenon_Hdd. apply refl_equal. % 0.70/0.90 (* end of lemma zenon_L28_ *) % 0.70/0.90 assert (zenon_L29_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (forall ARG2 : zenon_U, (forall NEW : zenon_U, (((disjointwith (c_tptpcol_1_1) ARG2)/\(genls NEW (c_tptpcol_1_1)))->(disjointwith NEW ARG2)))) -> (~(disjointwith (c_tptpcol_16_26926) (c_tptpcol_16_92269))) -> (disjointwith (c_tptpcol_1_1) (c_tptpcol_16_92269)) -> False). % 0.70/0.90 do 0 intro. intros zenon_Hb0 zenon_Hde zenon_Hdf zenon_He0. % 0.70/0.90 generalize (zenon_Hde (c_tptpcol_16_92269)). zenon_intro zenon_He1. % 0.70/0.90 generalize (zenon_He1 (c_tptpcol_16_26926)). zenon_intro zenon_He2. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_He2); [ zenon_intro zenon_He4 | zenon_intro zenon_He3 ]. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_He4); [ zenon_intro zenon_He6 | zenon_intro zenon_He5 ]. % 0.70/0.90 exact (zenon_He6 zenon_He0). % 0.70/0.90 elim (classic ((~((c_tptpcol_16_26926) = (c_tptpcol_2_2)))/\(~(genls (c_tptpcol_16_26926) (c_tptpcol_2_2))))); [ zenon_intro zenon_He7 | zenon_intro zenon_He8 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_He7). zenon_intro zenon_Hea. zenon_intro zenon_He9. % 0.70/0.90 elim (classic ((~((c_tptpcol_16_26926) = (c_tptpcol_3_16386)))/\(~(genls (c_tptpcol_16_26926) (c_tptpcol_3_16386))))); [ zenon_intro zenon_Heb | zenon_intro zenon_Hec ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_Heb). zenon_intro zenon_Hee. zenon_intro zenon_Hed. % 0.70/0.90 elim (classic ((~((c_tptpcol_16_26926) = (c_tptpcol_4_24578)))/\(~(genls (c_tptpcol_16_26926) (c_tptpcol_4_24578))))); [ zenon_intro zenon_Hef | zenon_intro zenon_Hf0 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_Hef). zenon_intro zenon_Hf2. zenon_intro zenon_Hf1. % 0.70/0.90 elim (classic ((~((c_tptpcol_16_26926) = (c_tptpcol_5_24579)))/\(~(genls (c_tptpcol_16_26926) (c_tptpcol_5_24579))))); [ zenon_intro zenon_Hf3 | zenon_intro zenon_Hf4 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_Hf3). zenon_intro zenon_Hf6. zenon_intro zenon_Hf5. % 0.70/0.90 elim (classic ((~((c_tptpcol_16_26926) = (c_tptpcol_6_26627)))/\(~(genls (c_tptpcol_16_26926) (c_tptpcol_6_26627))))); [ zenon_intro zenon_Hf7 | zenon_intro zenon_Hf8 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_Hf7). zenon_intro zenon_Hfa. zenon_intro zenon_Hf9. % 0.70/0.90 elim (classic ((~((c_tptpcol_16_26926) = (c_tptpcol_7_26628)))/\(~(genls (c_tptpcol_16_26926) (c_tptpcol_7_26628))))); [ zenon_intro zenon_Hfb | zenon_intro zenon_Hfc ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_Hfb). zenon_intro zenon_Hfe. zenon_intro zenon_Hfd. % 0.70/0.90 elim (classic ((~((c_tptpcol_16_26926) = (c_tptpcol_8_26629)))/\(~(genls (c_tptpcol_16_26926) (c_tptpcol_8_26629))))); [ zenon_intro zenon_Hff | zenon_intro zenon_H100 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_Hff). zenon_intro zenon_H102. zenon_intro zenon_H101. % 0.70/0.90 elim (classic ((~((c_tptpcol_16_26926) = (c_tptpcol_9_26885)))/\(~(genls (c_tptpcol_16_26926) (c_tptpcol_9_26885))))); [ zenon_intro zenon_H103 | zenon_intro zenon_H104 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_H103). zenon_intro zenon_H106. zenon_intro zenon_H105. % 0.70/0.90 elim (classic ((~((c_tptpcol_16_26926) = (c_tptpcol_10_26886)))/\(~(genls (c_tptpcol_16_26926) (c_tptpcol_10_26886))))); [ zenon_intro zenon_H107 | zenon_intro zenon_H108 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_H107). zenon_intro zenon_H10a. zenon_intro zenon_H109. % 0.70/0.90 elim (classic ((~((c_tptpcol_16_26926) = (c_tptpcol_11_26887)))/\(~(genls (c_tptpcol_16_26926) (c_tptpcol_11_26887))))); [ zenon_intro zenon_H10b | zenon_intro zenon_H10c ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_H10b). zenon_intro zenon_H10e. zenon_intro zenon_H10d. % 0.70/0.90 elim (classic ((~((c_tptpcol_16_26926) = (c_tptpcol_12_26919)))/\(~(genls (c_tptpcol_16_26926) (c_tptpcol_12_26919))))); [ zenon_intro zenon_H10f | zenon_intro zenon_H110 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_H10f). zenon_intro zenon_H112. zenon_intro zenon_H111. % 0.70/0.90 elim (classic ((~((c_tptpcol_16_26926) = (c_tptpcol_13_26920)))/\(~(genls (c_tptpcol_16_26926) (c_tptpcol_13_26920))))); [ zenon_intro zenon_H113 | zenon_intro zenon_H114 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_H113). zenon_intro zenon_H116. zenon_intro zenon_H115. % 0.70/0.90 elim (classic ((~((c_tptpcol_16_26926) = (c_tptpcol_14_26921)))/\(~(genls (c_tptpcol_16_26926) (c_tptpcol_14_26921))))); [ zenon_intro zenon_H117 | zenon_intro zenon_H118 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_H117). zenon_intro zenon_H11a. zenon_intro zenon_H119. % 0.70/0.90 elim (classic ((~((c_tptpcol_16_26926) = (c_tptpcol_15_26925)))/\(~(genls (c_tptpcol_16_26926) (c_tptpcol_15_26925))))); [ zenon_intro zenon_H11b | zenon_intro zenon_H11c ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_H11b). zenon_intro zenon_H11e. zenon_intro zenon_H11d. % 0.70/0.90 exact (zenon_H11d just35). % 0.70/0.90 cut ((genls (c_tptpcol_15_26925) (c_tptpcol_14_26921)) = (genls (c_tptpcol_16_26926) (c_tptpcol_14_26921))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H119. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just33. % 0.70/0.90 cut (((c_tptpcol_14_26921) = (c_tptpcol_14_26921))); [idtac | apply NNPP; zenon_intro zenon_Hd0]. % 0.70/0.90 cut (((c_tptpcol_15_26925) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H11f]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H11c); [ zenon_intro zenon_H121 | zenon_intro zenon_H120 ]. % 0.70/0.90 apply zenon_H121. zenon_intro zenon_H122. % 0.70/0.90 elim (classic ((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [ zenon_intro zenon_H123 | zenon_intro zenon_H124 ]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926)) = ((c_tptpcol_15_26925) = (c_tptpcol_16_26926))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H11f. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H123. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H124]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_15_26925))); [idtac | apply NNPP; zenon_intro zenon_H11e]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_H11e zenon_H122). % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H120. zenon_intro just35. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_16_26926)). zenon_intro zenon_H125. % 0.70/0.90 generalize (zenon_H125 (c_tptpcol_15_26925)). zenon_intro zenon_H126. % 0.70/0.90 generalize (zenon_H126 (c_tptpcol_14_26921)). zenon_intro zenon_H127. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H127); [ zenon_intro zenon_H11d | zenon_intro zenon_H128 ]. % 0.70/0.90 exact (zenon_H11d just35). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H128); [ zenon_intro zenon_H12a | zenon_intro zenon_H129 ]. % 0.70/0.90 exact (zenon_H12a just33). % 0.70/0.90 exact (zenon_H119 zenon_H129). % 0.70/0.90 apply zenon_Hd0. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_14_26921) (c_tptpcol_13_26920)) = (genls (c_tptpcol_16_26926) (c_tptpcol_13_26920))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H115. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just31. % 0.70/0.90 cut (((c_tptpcol_13_26920) = (c_tptpcol_13_26920))); [idtac | apply NNPP; zenon_intro zenon_Hd1]. % 0.70/0.90 cut (((c_tptpcol_14_26921) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H12b]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H118); [ zenon_intro zenon_H12d | zenon_intro zenon_H12c ]. % 0.70/0.90 apply zenon_H12d. zenon_intro zenon_H12e. % 0.70/0.90 elim (classic ((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [ zenon_intro zenon_H123 | zenon_intro zenon_H124 ]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926)) = ((c_tptpcol_14_26921) = (c_tptpcol_16_26926))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H12b. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H123. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H124]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_14_26921))); [idtac | apply NNPP; zenon_intro zenon_H11a]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_H11a zenon_H12e). % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H12c. zenon_intro zenon_H129. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_16_26926)). zenon_intro zenon_H125. % 0.70/0.90 generalize (zenon_H125 (c_tptpcol_14_26921)). zenon_intro zenon_H12f. % 0.70/0.90 generalize (zenon_H12f (c_tptpcol_13_26920)). zenon_intro zenon_H130. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H130); [ zenon_intro zenon_H119 | zenon_intro zenon_H131 ]. % 0.70/0.90 exact (zenon_H119 zenon_H129). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H131); [ zenon_intro zenon_H133 | zenon_intro zenon_H132 ]. % 0.70/0.90 exact (zenon_H133 just31). % 0.70/0.90 exact (zenon_H115 zenon_H132). % 0.70/0.90 apply zenon_Hd1. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_13_26920) (c_tptpcol_12_26919)) = (genls (c_tptpcol_16_26926) (c_tptpcol_12_26919))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H111. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just29. % 0.70/0.90 cut (((c_tptpcol_12_26919) = (c_tptpcol_12_26919))); [idtac | apply NNPP; zenon_intro zenon_Hd2]. % 0.70/0.90 cut (((c_tptpcol_13_26920) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H134]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H114); [ zenon_intro zenon_H136 | zenon_intro zenon_H135 ]. % 0.70/0.90 apply zenon_H136. zenon_intro zenon_H137. % 0.70/0.90 elim (classic ((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [ zenon_intro zenon_H123 | zenon_intro zenon_H124 ]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926)) = ((c_tptpcol_13_26920) = (c_tptpcol_16_26926))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H134. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H123. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H124]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_13_26920))); [idtac | apply NNPP; zenon_intro zenon_H116]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_H116 zenon_H137). % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H135. zenon_intro zenon_H132. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_16_26926)). zenon_intro zenon_H125. % 0.70/0.90 generalize (zenon_H125 (c_tptpcol_13_26920)). zenon_intro zenon_H138. % 0.70/0.90 generalize (zenon_H138 (c_tptpcol_12_26919)). zenon_intro zenon_H139. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H139); [ zenon_intro zenon_H115 | zenon_intro zenon_H13a ]. % 0.70/0.90 exact (zenon_H115 zenon_H132). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H13a); [ zenon_intro zenon_H13c | zenon_intro zenon_H13b ]. % 0.70/0.90 exact (zenon_H13c just29). % 0.70/0.90 exact (zenon_H111 zenon_H13b). % 0.70/0.90 apply zenon_Hd2. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_12_26919) (c_tptpcol_11_26887)) = (genls (c_tptpcol_16_26926) (c_tptpcol_11_26887))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H10d. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just27. % 0.70/0.90 cut (((c_tptpcol_11_26887) = (c_tptpcol_11_26887))); [idtac | apply NNPP; zenon_intro zenon_Hd3]. % 0.70/0.90 cut (((c_tptpcol_12_26919) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H13d]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H110); [ zenon_intro zenon_H13f | zenon_intro zenon_H13e ]. % 0.70/0.90 apply zenon_H13f. zenon_intro zenon_H140. % 0.70/0.90 elim (classic ((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [ zenon_intro zenon_H123 | zenon_intro zenon_H124 ]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926)) = ((c_tptpcol_12_26919) = (c_tptpcol_16_26926))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H13d. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H123. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H124]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_12_26919))); [idtac | apply NNPP; zenon_intro zenon_H112]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_H112 zenon_H140). % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H13e. zenon_intro zenon_H13b. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_16_26926)). zenon_intro zenon_H125. % 0.70/0.90 generalize (zenon_H125 (c_tptpcol_12_26919)). zenon_intro zenon_H141. % 0.70/0.90 generalize (zenon_H141 (c_tptpcol_11_26887)). zenon_intro zenon_H142. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H142); [ zenon_intro zenon_H111 | zenon_intro zenon_H143 ]. % 0.70/0.90 exact (zenon_H111 zenon_H13b). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H143); [ zenon_intro zenon_H145 | zenon_intro zenon_H144 ]. % 0.70/0.90 exact (zenon_H145 just27). % 0.70/0.90 exact (zenon_H10d zenon_H144). % 0.70/0.90 apply zenon_Hd3. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_11_26887) (c_tptpcol_10_26886)) = (genls (c_tptpcol_16_26926) (c_tptpcol_10_26886))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H109. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just25. % 0.70/0.90 cut (((c_tptpcol_10_26886) = (c_tptpcol_10_26886))); [idtac | apply NNPP; zenon_intro zenon_Hd4]. % 0.70/0.90 cut (((c_tptpcol_11_26887) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H146]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H10c); [ zenon_intro zenon_H148 | zenon_intro zenon_H147 ]. % 0.70/0.90 apply zenon_H148. zenon_intro zenon_H149. % 0.70/0.90 elim (classic ((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [ zenon_intro zenon_H123 | zenon_intro zenon_H124 ]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926)) = ((c_tptpcol_11_26887) = (c_tptpcol_16_26926))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H146. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H123. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H124]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_11_26887))); [idtac | apply NNPP; zenon_intro zenon_H10e]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_H10e zenon_H149). % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H147. zenon_intro zenon_H144. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_16_26926)). zenon_intro zenon_H125. % 0.70/0.90 generalize (zenon_H125 (c_tptpcol_11_26887)). zenon_intro zenon_H14a. % 0.70/0.90 generalize (zenon_H14a (c_tptpcol_10_26886)). zenon_intro zenon_H14b. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H14b); [ zenon_intro zenon_H10d | zenon_intro zenon_H14c ]. % 0.70/0.90 exact (zenon_H10d zenon_H144). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H14c); [ zenon_intro zenon_H14e | zenon_intro zenon_H14d ]. % 0.70/0.90 exact (zenon_H14e just25). % 0.70/0.90 exact (zenon_H109 zenon_H14d). % 0.70/0.90 apply zenon_Hd4. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_10_26886) (c_tptpcol_9_26885)) = (genls (c_tptpcol_16_26926) (c_tptpcol_9_26885))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H105. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just23. % 0.70/0.90 cut (((c_tptpcol_9_26885) = (c_tptpcol_9_26885))); [idtac | apply NNPP; zenon_intro zenon_Hd5]. % 0.70/0.90 cut (((c_tptpcol_10_26886) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H14f]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H108); [ zenon_intro zenon_H151 | zenon_intro zenon_H150 ]. % 0.70/0.90 apply zenon_H151. zenon_intro zenon_H152. % 0.70/0.90 elim (classic ((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [ zenon_intro zenon_H123 | zenon_intro zenon_H124 ]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926)) = ((c_tptpcol_10_26886) = (c_tptpcol_16_26926))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H14f. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H123. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H124]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_10_26886))); [idtac | apply NNPP; zenon_intro zenon_H10a]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_H10a zenon_H152). % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H150. zenon_intro zenon_H14d. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_16_26926)). zenon_intro zenon_H125. % 0.70/0.90 generalize (zenon_H125 (c_tptpcol_10_26886)). zenon_intro zenon_H153. % 0.70/0.90 generalize (zenon_H153 (c_tptpcol_9_26885)). zenon_intro zenon_H154. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H154); [ zenon_intro zenon_H109 | zenon_intro zenon_H155 ]. % 0.70/0.90 exact (zenon_H109 zenon_H14d). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H155); [ zenon_intro zenon_H157 | zenon_intro zenon_H156 ]. % 0.70/0.90 exact (zenon_H157 just23). % 0.70/0.90 exact (zenon_H105 zenon_H156). % 0.70/0.90 apply zenon_Hd5. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_9_26885) (c_tptpcol_8_26629)) = (genls (c_tptpcol_16_26926) (c_tptpcol_8_26629))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H101. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just21. % 0.70/0.90 cut (((c_tptpcol_8_26629) = (c_tptpcol_8_26629))); [idtac | apply NNPP; zenon_intro zenon_Hd6]. % 0.70/0.90 cut (((c_tptpcol_9_26885) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H158]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H104); [ zenon_intro zenon_H15a | zenon_intro zenon_H159 ]. % 0.70/0.90 apply zenon_H15a. zenon_intro zenon_H15b. % 0.70/0.90 elim (classic ((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [ zenon_intro zenon_H123 | zenon_intro zenon_H124 ]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926)) = ((c_tptpcol_9_26885) = (c_tptpcol_16_26926))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H158. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H123. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H124]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_9_26885))); [idtac | apply NNPP; zenon_intro zenon_H106]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_H106 zenon_H15b). % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H159. zenon_intro zenon_H156. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_16_26926)). zenon_intro zenon_H125. % 0.70/0.90 generalize (zenon_H125 (c_tptpcol_9_26885)). zenon_intro zenon_H15c. % 0.70/0.90 generalize (zenon_H15c (c_tptpcol_8_26629)). zenon_intro zenon_H15d. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H15d); [ zenon_intro zenon_H105 | zenon_intro zenon_H15e ]. % 0.70/0.90 exact (zenon_H105 zenon_H156). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H15e); [ zenon_intro zenon_H160 | zenon_intro zenon_H15f ]. % 0.70/0.90 exact (zenon_H160 just21). % 0.70/0.90 exact (zenon_H101 zenon_H15f). % 0.70/0.90 apply zenon_Hd6. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_8_26629) (c_tptpcol_7_26628)) = (genls (c_tptpcol_16_26926) (c_tptpcol_7_26628))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_Hfd. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just19. % 0.70/0.90 cut (((c_tptpcol_7_26628) = (c_tptpcol_7_26628))); [idtac | apply NNPP; zenon_intro zenon_Hd7]. % 0.70/0.90 cut (((c_tptpcol_8_26629) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H161]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H100); [ zenon_intro zenon_H163 | zenon_intro zenon_H162 ]. % 0.70/0.90 apply zenon_H163. zenon_intro zenon_H164. % 0.70/0.90 elim (classic ((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [ zenon_intro zenon_H123 | zenon_intro zenon_H124 ]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926)) = ((c_tptpcol_8_26629) = (c_tptpcol_16_26926))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H161. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H123. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H124]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_8_26629))); [idtac | apply NNPP; zenon_intro zenon_H102]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_H102 zenon_H164). % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H162. zenon_intro zenon_H15f. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_16_26926)). zenon_intro zenon_H125. % 0.70/0.90 generalize (zenon_H125 (c_tptpcol_8_26629)). zenon_intro zenon_H165. % 0.70/0.90 generalize (zenon_H165 (c_tptpcol_7_26628)). zenon_intro zenon_H166. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H166); [ zenon_intro zenon_H101 | zenon_intro zenon_H167 ]. % 0.70/0.90 exact (zenon_H101 zenon_H15f). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H167); [ zenon_intro zenon_H169 | zenon_intro zenon_H168 ]. % 0.70/0.90 exact (zenon_H169 just19). % 0.70/0.90 exact (zenon_Hfd zenon_H168). % 0.70/0.90 apply zenon_Hd7. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_7_26628) (c_tptpcol_6_26627)) = (genls (c_tptpcol_16_26926) (c_tptpcol_6_26627))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_Hf9. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just17. % 0.70/0.90 cut (((c_tptpcol_6_26627) = (c_tptpcol_6_26627))); [idtac | apply NNPP; zenon_intro zenon_Hd8]. % 0.70/0.90 cut (((c_tptpcol_7_26628) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H16a]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_Hfc); [ zenon_intro zenon_H16c | zenon_intro zenon_H16b ]. % 0.70/0.90 apply zenon_H16c. zenon_intro zenon_H16d. % 0.70/0.90 elim (classic ((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [ zenon_intro zenon_H123 | zenon_intro zenon_H124 ]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926)) = ((c_tptpcol_7_26628) = (c_tptpcol_16_26926))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H16a. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H123. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H124]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_7_26628))); [idtac | apply NNPP; zenon_intro zenon_Hfe]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_Hfe zenon_H16d). % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H16b. zenon_intro zenon_H168. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_16_26926)). zenon_intro zenon_H125. % 0.70/0.90 generalize (zenon_H125 (c_tptpcol_7_26628)). zenon_intro zenon_H16e. % 0.70/0.90 generalize (zenon_H16e (c_tptpcol_6_26627)). zenon_intro zenon_H16f. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H16f); [ zenon_intro zenon_Hfd | zenon_intro zenon_H170 ]. % 0.70/0.90 exact (zenon_Hfd zenon_H168). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H170); [ zenon_intro zenon_H172 | zenon_intro zenon_H171 ]. % 0.70/0.90 exact (zenon_H172 just17). % 0.70/0.90 exact (zenon_Hf9 zenon_H171). % 0.70/0.90 apply zenon_Hd8. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_6_26627) (c_tptpcol_5_24579)) = (genls (c_tptpcol_16_26926) (c_tptpcol_5_24579))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_Hf5. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just15. % 0.70/0.90 cut (((c_tptpcol_5_24579) = (c_tptpcol_5_24579))); [idtac | apply NNPP; zenon_intro zenon_Hd9]. % 0.70/0.90 cut (((c_tptpcol_6_26627) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H173]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_Hf8); [ zenon_intro zenon_H175 | zenon_intro zenon_H174 ]. % 0.70/0.90 apply zenon_H175. zenon_intro zenon_H176. % 0.70/0.90 elim (classic ((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [ zenon_intro zenon_H123 | zenon_intro zenon_H124 ]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926)) = ((c_tptpcol_6_26627) = (c_tptpcol_16_26926))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H173. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H123. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H124]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_6_26627))); [idtac | apply NNPP; zenon_intro zenon_Hfa]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_Hfa zenon_H176). % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H174. zenon_intro zenon_H171. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_16_26926)). zenon_intro zenon_H125. % 0.70/0.90 generalize (zenon_H125 (c_tptpcol_6_26627)). zenon_intro zenon_H177. % 0.70/0.90 generalize (zenon_H177 (c_tptpcol_5_24579)). zenon_intro zenon_H178. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H178); [ zenon_intro zenon_Hf9 | zenon_intro zenon_H179 ]. % 0.70/0.90 exact (zenon_Hf9 zenon_H171). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H179); [ zenon_intro zenon_H17b | zenon_intro zenon_H17a ]. % 0.70/0.90 exact (zenon_H17b just15). % 0.70/0.90 exact (zenon_Hf5 zenon_H17a). % 0.70/0.90 apply zenon_Hd9. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_5_24579) (c_tptpcol_4_24578)) = (genls (c_tptpcol_16_26926) (c_tptpcol_4_24578))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_Hf1. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just13. % 0.70/0.90 cut (((c_tptpcol_4_24578) = (c_tptpcol_4_24578))); [idtac | apply NNPP; zenon_intro zenon_Hda]. % 0.70/0.90 cut (((c_tptpcol_5_24579) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H17c]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_Hf4); [ zenon_intro zenon_H17e | zenon_intro zenon_H17d ]. % 0.70/0.90 apply zenon_H17e. zenon_intro zenon_H17f. % 0.70/0.90 elim (classic ((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [ zenon_intro zenon_H123 | zenon_intro zenon_H124 ]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926)) = ((c_tptpcol_5_24579) = (c_tptpcol_16_26926))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H17c. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H123. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H124]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_5_24579))); [idtac | apply NNPP; zenon_intro zenon_Hf6]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_Hf6 zenon_H17f). % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H17d. zenon_intro zenon_H17a. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_16_26926)). zenon_intro zenon_H125. % 0.70/0.90 generalize (zenon_H125 (c_tptpcol_5_24579)). zenon_intro zenon_H180. % 0.70/0.90 generalize (zenon_H180 (c_tptpcol_4_24578)). zenon_intro zenon_H181. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H181); [ zenon_intro zenon_Hf5 | zenon_intro zenon_H182 ]. % 0.70/0.90 exact (zenon_Hf5 zenon_H17a). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H182); [ zenon_intro zenon_H184 | zenon_intro zenon_H183 ]. % 0.70/0.90 exact (zenon_H184 just13). % 0.70/0.90 exact (zenon_Hf1 zenon_H183). % 0.70/0.90 apply zenon_Hda. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_4_24578) (c_tptpcol_3_16386)) = (genls (c_tptpcol_16_26926) (c_tptpcol_3_16386))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_Hed. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just11. % 0.70/0.90 cut (((c_tptpcol_3_16386) = (c_tptpcol_3_16386))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 0.70/0.90 cut (((c_tptpcol_4_24578) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H185]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_Hf0); [ zenon_intro zenon_H187 | zenon_intro zenon_H186 ]. % 0.70/0.90 apply zenon_H187. zenon_intro zenon_H188. % 0.70/0.90 elim (classic ((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [ zenon_intro zenon_H123 | zenon_intro zenon_H124 ]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926)) = ((c_tptpcol_4_24578) = (c_tptpcol_16_26926))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H185. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H123. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H124]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_4_24578))); [idtac | apply NNPP; zenon_intro zenon_Hf2]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_Hf2 zenon_H188). % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H186. zenon_intro zenon_H183. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_16_26926)). zenon_intro zenon_H125. % 0.70/0.90 generalize (zenon_H125 (c_tptpcol_4_24578)). zenon_intro zenon_H189. % 0.70/0.90 generalize (zenon_H189 (c_tptpcol_3_16386)). zenon_intro zenon_H18a. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H18a); [ zenon_intro zenon_Hf1 | zenon_intro zenon_H18b ]. % 0.70/0.90 exact (zenon_Hf1 zenon_H183). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H18b); [ zenon_intro zenon_H18d | zenon_intro zenon_H18c ]. % 0.70/0.90 exact (zenon_H18d just11). % 0.70/0.90 exact (zenon_Hed zenon_H18c). % 0.70/0.90 apply zenon_Hdb. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) = (genls (c_tptpcol_16_26926) (c_tptpcol_2_2))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_He9. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just9. % 0.70/0.90 cut (((c_tptpcol_2_2) = (c_tptpcol_2_2))); [idtac | apply NNPP; zenon_intro zenon_Hdc]. % 0.70/0.90 cut (((c_tptpcol_3_16386) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H18e]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_Hec); [ zenon_intro zenon_H190 | zenon_intro zenon_H18f ]. % 0.70/0.90 apply zenon_H190. zenon_intro zenon_H191. % 0.70/0.90 elim (classic ((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [ zenon_intro zenon_H123 | zenon_intro zenon_H124 ]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926)) = ((c_tptpcol_3_16386) = (c_tptpcol_16_26926))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H18e. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H123. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H124]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_3_16386))); [idtac | apply NNPP; zenon_intro zenon_Hee]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_Hee zenon_H191). % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H18f. zenon_intro zenon_H18c. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_16_26926)). zenon_intro zenon_H125. % 0.70/0.90 generalize (zenon_H125 (c_tptpcol_3_16386)). zenon_intro zenon_H192. % 0.70/0.90 generalize (zenon_H192 (c_tptpcol_2_2)). zenon_intro zenon_H193. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H193); [ zenon_intro zenon_Hed | zenon_intro zenon_H194 ]. % 0.70/0.90 exact (zenon_Hed zenon_H18c). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H194); [ zenon_intro zenon_H196 | zenon_intro zenon_H195 ]. % 0.70/0.90 exact (zenon_H196 just9). % 0.70/0.90 exact (zenon_He9 zenon_H195). % 0.70/0.90 apply zenon_Hdc. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_2_2) (c_tptpcol_1_1)) = (genls (c_tptpcol_16_26926) (c_tptpcol_1_1))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_He5. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just7. % 0.70/0.90 cut (((c_tptpcol_1_1) = (c_tptpcol_1_1))); [idtac | apply NNPP; zenon_intro zenon_Hdd]. % 0.70/0.90 cut (((c_tptpcol_2_2) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H197]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_He8); [ zenon_intro zenon_H199 | zenon_intro zenon_H198 ]. % 0.70/0.90 apply zenon_H199. zenon_intro zenon_H19a. % 0.70/0.90 elim (classic ((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [ zenon_intro zenon_H123 | zenon_intro zenon_H124 ]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926)) = ((c_tptpcol_2_2) = (c_tptpcol_16_26926))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H197. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H123. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_16_26926))); [idtac | apply NNPP; zenon_intro zenon_H124]. % 0.70/0.90 cut (((c_tptpcol_16_26926) = (c_tptpcol_2_2))); [idtac | apply NNPP; zenon_intro zenon_Hea]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_Hea zenon_H19a). % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H124. apply refl_equal. % 0.70/0.90 apply zenon_H198. zenon_intro zenon_H195. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_16_26926)). zenon_intro zenon_H125. % 0.70/0.90 generalize (zenon_H125 (c_tptpcol_2_2)). zenon_intro zenon_H19b. % 0.70/0.90 generalize (zenon_H19b (c_tptpcol_1_1)). zenon_intro zenon_H19c. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H19c); [ zenon_intro zenon_He9 | zenon_intro zenon_H19d ]. % 0.70/0.90 exact (zenon_He9 zenon_H195). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H19d); [ zenon_intro zenon_H19f | zenon_intro zenon_H19e ]. % 0.70/0.90 exact (zenon_H19f just7). % 0.70/0.90 exact (zenon_He5 zenon_H19e). % 0.70/0.90 apply zenon_Hdd. apply refl_equal. % 0.70/0.90 exact (zenon_Hdf zenon_He3). % 0.70/0.90 (* end of lemma zenon_L29_ *) % 0.70/0.90 apply NNPP. intro zenon_G. % 0.70/0.90 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_Hb0 | zenon_intro zenon_H1a0 ]. % 0.70/0.90 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H1a1. zenon_intro zenon_Hdf. % 0.70/0.90 generalize (just86 (c_tptpcol_1_1)). zenon_intro zenon_Hde. % 0.70/0.90 generalize (just85 (c_tptpcol_1_1)). zenon_intro zenon_H1a2. % 0.70/0.90 generalize (zenon_H1a2 (c_tptpcol_8_92164)). zenon_intro zenon_H1a3. % 0.70/0.90 generalize (zenon_H1a2 (c_tptpcol_13_92263)). zenon_intro zenon_H1a4. % 0.70/0.90 generalize (zenon_H1a2 (c_tptpcol_1_65536)). zenon_intro zenon_H1a5. % 0.70/0.90 generalize (zenon_H1a3 (c_tptpcol_13_92263)). zenon_intro zenon_H1a6. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H1a6); [ zenon_intro zenon_H1a8 | zenon_intro zenon_H1a7 ]. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H1a8); [ zenon_intro zenon_H1aa | zenon_intro zenon_H1a9 ]. % 0.70/0.90 generalize (zenon_H1a5 (c_tptpcol_8_92164)). zenon_intro zenon_H1ab. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H1ab); [ zenon_intro zenon_H1ad | zenon_intro zenon_H1ac ]. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H1ad); [ zenon_intro zenon_H1af | zenon_intro zenon_H1ae ]. % 0.70/0.90 exact (zenon_H1af just67). % 0.70/0.90 elim (classic ((~((c_tptpcol_8_92164) = (c_tptpcol_2_65537)))/\(~(genls (c_tptpcol_8_92164) (c_tptpcol_2_65537))))); [ zenon_intro zenon_H1b0 | zenon_intro zenon_H1b1 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_H1b0). zenon_intro zenon_H1b3. zenon_intro zenon_H1b2. % 0.70/0.90 elim (classic ((~((c_tptpcol_8_92164) = (c_tptpcol_3_81921)))/\(~(genls (c_tptpcol_8_92164) (c_tptpcol_3_81921))))); [ zenon_intro zenon_H1b4 | zenon_intro zenon_H1b5 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_H1b4). zenon_intro zenon_H1b7. zenon_intro zenon_H1b6. % 0.70/0.90 elim (classic ((~((c_tptpcol_8_92164) = (c_tptpcol_4_90113)))/\(~(genls (c_tptpcol_8_92164) (c_tptpcol_4_90113))))); [ zenon_intro zenon_H1b8 | zenon_intro zenon_H1b9 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_H1b8). zenon_intro zenon_H1bb. zenon_intro zenon_H1ba. % 0.70/0.90 elim (classic ((~((c_tptpcol_8_92164) = (c_tptpcol_5_90114)))/\(~(genls (c_tptpcol_8_92164) (c_tptpcol_5_90114))))); [ zenon_intro zenon_H1bc | zenon_intro zenon_H1bd ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_H1bc). zenon_intro zenon_H1bf. zenon_intro zenon_H1be. % 0.70/0.90 elim (classic ((~((c_tptpcol_8_92164) = (c_tptpcol_6_92162)))/\(~(genls (c_tptpcol_8_92164) (c_tptpcol_6_92162))))); [ zenon_intro zenon_H1c0 | zenon_intro zenon_H1c1 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_H1c0). zenon_intro zenon_H1c3. zenon_intro zenon_H1c2. % 0.70/0.90 elim (classic ((~((c_tptpcol_8_92164) = (c_tptpcol_7_92163)))/\(~(genls (c_tptpcol_8_92164) (c_tptpcol_7_92163))))); [ zenon_intro zenon_H1c4 | zenon_intro zenon_H1c5 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_H1c4). zenon_intro zenon_H1c7. zenon_intro zenon_H1c6. % 0.70/0.90 exact (zenon_H1c6 just49). % 0.70/0.90 cut ((genls (c_tptpcol_7_92163) (c_tptpcol_6_92162)) = (genls (c_tptpcol_8_92164) (c_tptpcol_6_92162))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H1c2. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just47. % 0.70/0.90 cut (((c_tptpcol_6_92162) = (c_tptpcol_6_92162))); [idtac | apply NNPP; zenon_intro zenon_Ha5]. % 0.70/0.90 cut (((c_tptpcol_7_92163) = (c_tptpcol_8_92164))); [idtac | apply NNPP; zenon_intro zenon_H1c8]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H1c5); [ zenon_intro zenon_H1ca | zenon_intro zenon_H1c9 ]. % 0.70/0.90 apply zenon_H1ca. zenon_intro zenon_H1cb. % 0.70/0.90 elim (classic ((c_tptpcol_8_92164) = (c_tptpcol_8_92164))); [ zenon_intro zenon_H1cc | zenon_intro zenon_Hae ]. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_8_92164)) = ((c_tptpcol_7_92163) = (c_tptpcol_8_92164))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H1c8. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H1cc. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_8_92164))); [idtac | apply NNPP; zenon_intro zenon_Hae]. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_7_92163))); [idtac | apply NNPP; zenon_intro zenon_H1c7]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_H1c7 zenon_H1cb). % 0.70/0.90 apply zenon_Hae. apply refl_equal. % 0.70/0.90 apply zenon_Hae. apply refl_equal. % 0.70/0.90 apply zenon_H1c9. zenon_intro just49. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_8_92164)). zenon_intro zenon_H1cd. % 0.70/0.90 generalize (zenon_H1cd (c_tptpcol_7_92163)). zenon_intro zenon_H1ce. % 0.70/0.90 generalize (zenon_H1ce (c_tptpcol_6_92162)). zenon_intro zenon_H1cf. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H1cf); [ zenon_intro zenon_H1c6 | zenon_intro zenon_H1d0 ]. % 0.70/0.90 exact (zenon_H1c6 just49). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H1d0); [ zenon_intro zenon_H1d2 | zenon_intro zenon_H1d1 ]. % 0.70/0.90 exact (zenon_H1d2 just47). % 0.70/0.90 exact (zenon_H1c2 zenon_H1d1). % 0.70/0.90 apply zenon_Ha5. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_6_92162) (c_tptpcol_5_90114)) = (genls (c_tptpcol_8_92164) (c_tptpcol_5_90114))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H1be. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just45. % 0.70/0.90 cut (((c_tptpcol_5_90114) = (c_tptpcol_5_90114))); [idtac | apply NNPP; zenon_intro zenon_Ha6]. % 0.70/0.90 cut (((c_tptpcol_6_92162) = (c_tptpcol_8_92164))); [idtac | apply NNPP; zenon_intro zenon_H1d3]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H1c1); [ zenon_intro zenon_H1d5 | zenon_intro zenon_H1d4 ]. % 0.70/0.90 apply zenon_H1d5. zenon_intro zenon_H1d6. % 0.70/0.90 elim (classic ((c_tptpcol_8_92164) = (c_tptpcol_8_92164))); [ zenon_intro zenon_H1cc | zenon_intro zenon_Hae ]. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_8_92164)) = ((c_tptpcol_6_92162) = (c_tptpcol_8_92164))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H1d3. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H1cc. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_8_92164))); [idtac | apply NNPP; zenon_intro zenon_Hae]. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_6_92162))); [idtac | apply NNPP; zenon_intro zenon_H1c3]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_H1c3 zenon_H1d6). % 0.70/0.90 apply zenon_Hae. apply refl_equal. % 0.70/0.90 apply zenon_Hae. apply refl_equal. % 0.70/0.90 apply zenon_H1d4. zenon_intro zenon_H1d1. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_8_92164)). zenon_intro zenon_H1cd. % 0.70/0.90 generalize (zenon_H1cd (c_tptpcol_6_92162)). zenon_intro zenon_H1d7. % 0.70/0.90 generalize (zenon_H1d7 (c_tptpcol_5_90114)). zenon_intro zenon_H1d8. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H1d8); [ zenon_intro zenon_H1c2 | zenon_intro zenon_H1d9 ]. % 0.70/0.90 exact (zenon_H1c2 zenon_H1d1). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H1d9); [ zenon_intro zenon_H1db | zenon_intro zenon_H1da ]. % 0.70/0.90 exact (zenon_H1db just45). % 0.70/0.90 exact (zenon_H1be zenon_H1da). % 0.70/0.90 apply zenon_Ha6. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_5_90114) (c_tptpcol_4_90113)) = (genls (c_tptpcol_8_92164) (c_tptpcol_4_90113))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H1ba. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just43. % 0.70/0.90 cut (((c_tptpcol_4_90113) = (c_tptpcol_4_90113))); [idtac | apply NNPP; zenon_intro zenon_Ha7]. % 0.70/0.90 cut (((c_tptpcol_5_90114) = (c_tptpcol_8_92164))); [idtac | apply NNPP; zenon_intro zenon_H1dc]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H1bd); [ zenon_intro zenon_H1de | zenon_intro zenon_H1dd ]. % 0.70/0.90 apply zenon_H1de. zenon_intro zenon_H1df. % 0.70/0.90 elim (classic ((c_tptpcol_8_92164) = (c_tptpcol_8_92164))); [ zenon_intro zenon_H1cc | zenon_intro zenon_Hae ]. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_8_92164)) = ((c_tptpcol_5_90114) = (c_tptpcol_8_92164))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H1dc. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H1cc. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_8_92164))); [idtac | apply NNPP; zenon_intro zenon_Hae]. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_5_90114))); [idtac | apply NNPP; zenon_intro zenon_H1bf]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_H1bf zenon_H1df). % 0.70/0.90 apply zenon_Hae. apply refl_equal. % 0.70/0.90 apply zenon_Hae. apply refl_equal. % 0.70/0.90 apply zenon_H1dd. zenon_intro zenon_H1da. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_8_92164)). zenon_intro zenon_H1cd. % 0.70/0.90 generalize (zenon_H1cd (c_tptpcol_5_90114)). zenon_intro zenon_H1e0. % 0.70/0.90 generalize (zenon_H1e0 (c_tptpcol_4_90113)). zenon_intro zenon_H1e1. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H1e1); [ zenon_intro zenon_H1be | zenon_intro zenon_H1e2 ]. % 0.70/0.90 exact (zenon_H1be zenon_H1da). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H1e2); [ zenon_intro zenon_H1e4 | zenon_intro zenon_H1e3 ]. % 0.70/0.90 exact (zenon_H1e4 just43). % 0.70/0.90 exact (zenon_H1ba zenon_H1e3). % 0.70/0.90 apply zenon_Ha7. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_4_90113) (c_tptpcol_3_81921)) = (genls (c_tptpcol_8_92164) (c_tptpcol_3_81921))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H1b6. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just41. % 0.70/0.90 cut (((c_tptpcol_3_81921) = (c_tptpcol_3_81921))); [idtac | apply NNPP; zenon_intro zenon_Ha8]. % 0.70/0.90 cut (((c_tptpcol_4_90113) = (c_tptpcol_8_92164))); [idtac | apply NNPP; zenon_intro zenon_H1e5]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H1b9); [ zenon_intro zenon_H1e7 | zenon_intro zenon_H1e6 ]. % 0.70/0.90 apply zenon_H1e7. zenon_intro zenon_H1e8. % 0.70/0.90 elim (classic ((c_tptpcol_8_92164) = (c_tptpcol_8_92164))); [ zenon_intro zenon_H1cc | zenon_intro zenon_Hae ]. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_8_92164)) = ((c_tptpcol_4_90113) = (c_tptpcol_8_92164))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H1e5. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H1cc. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_8_92164))); [idtac | apply NNPP; zenon_intro zenon_Hae]. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_4_90113))); [idtac | apply NNPP; zenon_intro zenon_H1bb]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_H1bb zenon_H1e8). % 0.70/0.90 apply zenon_Hae. apply refl_equal. % 0.70/0.90 apply zenon_Hae. apply refl_equal. % 0.70/0.90 apply zenon_H1e6. zenon_intro zenon_H1e3. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_8_92164)). zenon_intro zenon_H1cd. % 0.70/0.90 generalize (zenon_H1cd (c_tptpcol_4_90113)). zenon_intro zenon_H1e9. % 0.70/0.90 generalize (zenon_H1e9 (c_tptpcol_3_81921)). zenon_intro zenon_H1ea. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H1ea); [ zenon_intro zenon_H1ba | zenon_intro zenon_H1eb ]. % 0.70/0.90 exact (zenon_H1ba zenon_H1e3). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H1eb); [ zenon_intro zenon_H1ed | zenon_intro zenon_H1ec ]. % 0.70/0.90 exact (zenon_H1ed just41). % 0.70/0.90 exact (zenon_H1b6 zenon_H1ec). % 0.70/0.90 apply zenon_Ha8. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_3_81921) (c_tptpcol_2_65537)) = (genls (c_tptpcol_8_92164) (c_tptpcol_2_65537))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H1b2. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just39. % 0.70/0.90 cut (((c_tptpcol_2_65537) = (c_tptpcol_2_65537))); [idtac | apply NNPP; zenon_intro zenon_Ha9]. % 0.70/0.90 cut (((c_tptpcol_3_81921) = (c_tptpcol_8_92164))); [idtac | apply NNPP; zenon_intro zenon_H1ee]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H1b5); [ zenon_intro zenon_H1f0 | zenon_intro zenon_H1ef ]. % 0.70/0.90 apply zenon_H1f0. zenon_intro zenon_H1f1. % 0.70/0.90 elim (classic ((c_tptpcol_8_92164) = (c_tptpcol_8_92164))); [ zenon_intro zenon_H1cc | zenon_intro zenon_Hae ]. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_8_92164)) = ((c_tptpcol_3_81921) = (c_tptpcol_8_92164))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H1ee. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H1cc. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_8_92164))); [idtac | apply NNPP; zenon_intro zenon_Hae]. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_3_81921))); [idtac | apply NNPP; zenon_intro zenon_H1b7]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_H1b7 zenon_H1f1). % 0.70/0.90 apply zenon_Hae. apply refl_equal. % 0.70/0.90 apply zenon_Hae. apply refl_equal. % 0.70/0.90 apply zenon_H1ef. zenon_intro zenon_H1ec. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_8_92164)). zenon_intro zenon_H1cd. % 0.70/0.90 generalize (zenon_H1cd (c_tptpcol_3_81921)). zenon_intro zenon_H1f2. % 0.70/0.90 generalize (zenon_H1f2 (c_tptpcol_2_65537)). zenon_intro zenon_H1f3. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H1f3); [ zenon_intro zenon_H1b6 | zenon_intro zenon_H1f4 ]. % 0.70/0.90 exact (zenon_H1b6 zenon_H1ec). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H1f4); [ zenon_intro zenon_H1f6 | zenon_intro zenon_H1f5 ]. % 0.70/0.90 exact (zenon_H1f6 just39). % 0.70/0.90 exact (zenon_H1b2 zenon_H1f5). % 0.70/0.90 apply zenon_Ha9. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) = (genls (c_tptpcol_8_92164) (c_tptpcol_1_65536))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H1ae. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just37. % 0.70/0.90 cut (((c_tptpcol_1_65536) = (c_tptpcol_1_65536))); [idtac | apply NNPP; zenon_intro zenon_Haa]. % 0.70/0.90 cut (((c_tptpcol_2_65537) = (c_tptpcol_8_92164))); [idtac | apply NNPP; zenon_intro zenon_H1f7]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H1b1); [ zenon_intro zenon_H1f9 | zenon_intro zenon_H1f8 ]. % 0.70/0.90 apply zenon_H1f9. zenon_intro zenon_H1fa. % 0.70/0.90 elim (classic ((c_tptpcol_8_92164) = (c_tptpcol_8_92164))); [ zenon_intro zenon_H1cc | zenon_intro zenon_Hae ]. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_8_92164)) = ((c_tptpcol_2_65537) = (c_tptpcol_8_92164))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H1f7. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H1cc. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_8_92164))); [idtac | apply NNPP; zenon_intro zenon_Hae]. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_2_65537))); [idtac | apply NNPP; zenon_intro zenon_H1b3]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_H1b3 zenon_H1fa). % 0.70/0.90 apply zenon_Hae. apply refl_equal. % 0.70/0.90 apply zenon_Hae. apply refl_equal. % 0.70/0.90 apply zenon_H1f8. zenon_intro zenon_H1f5. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_8_92164)). zenon_intro zenon_H1cd. % 0.70/0.90 generalize (zenon_H1cd (c_tptpcol_2_65537)). zenon_intro zenon_H1fb. % 0.70/0.90 generalize (zenon_H1fb (c_tptpcol_1_65536)). zenon_intro zenon_H1fc. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H1fc); [ zenon_intro zenon_H1b2 | zenon_intro zenon_H1fd ]. % 0.70/0.90 exact (zenon_H1b2 zenon_H1f5). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H1fd); [ zenon_intro zenon_H1ff | zenon_intro zenon_H1fe ]. % 0.70/0.90 exact (zenon_H1ff just37). % 0.70/0.90 exact (zenon_H1ae zenon_H1fe). % 0.70/0.90 apply zenon_Haa. apply refl_equal. % 0.70/0.90 exact (zenon_H1aa zenon_H1ac). % 0.70/0.90 elim (classic ((~((c_tptpcol_13_92263) = (c_tptpcol_9_92165)))/\(~(genls (c_tptpcol_13_92263) (c_tptpcol_9_92165))))); [ zenon_intro zenon_H200 | zenon_intro zenon_H201 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_H200). zenon_intro zenon_H203. zenon_intro zenon_H202. % 0.70/0.90 elim (classic ((~((c_tptpcol_13_92263) = (c_tptpcol_10_92166)))/\(~(genls (c_tptpcol_13_92263) (c_tptpcol_10_92166))))); [ zenon_intro zenon_H204 | zenon_intro zenon_H205 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_H204). zenon_intro zenon_H207. zenon_intro zenon_H206. % 0.70/0.90 elim (classic ((~((c_tptpcol_13_92263) = (c_tptpcol_11_92230)))/\(~(genls (c_tptpcol_13_92263) (c_tptpcol_11_92230))))); [ zenon_intro zenon_H208 | zenon_intro zenon_H209 ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_H208). zenon_intro zenon_H20b. zenon_intro zenon_H20a. % 0.70/0.90 elim (classic ((~((c_tptpcol_13_92263) = (c_tptpcol_12_92262)))/\(~(genls (c_tptpcol_13_92263) (c_tptpcol_12_92262))))); [ zenon_intro zenon_H20c | zenon_intro zenon_H20d ]. % 0.70/0.90 apply (zenon_and_s _ _ zenon_H20c). zenon_intro zenon_H20f. zenon_intro zenon_H20e. % 0.70/0.90 exact (zenon_H20e just59). % 0.70/0.90 cut ((genls (c_tptpcol_12_92262) (c_tptpcol_11_92230)) = (genls (c_tptpcol_13_92263) (c_tptpcol_11_92230))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H20a. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just57. % 0.70/0.90 cut (((c_tptpcol_11_92230) = (c_tptpcol_11_92230))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 0.70/0.90 cut (((c_tptpcol_12_92262) = (c_tptpcol_13_92263))); [idtac | apply NNPP; zenon_intro zenon_H210]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H20d); [ zenon_intro zenon_H212 | zenon_intro zenon_H211 ]. % 0.70/0.90 apply zenon_H212. zenon_intro zenon_H213. % 0.70/0.90 elim (classic ((c_tptpcol_13_92263) = (c_tptpcol_13_92263))); [ zenon_intro zenon_H214 | zenon_intro zenon_Hc2 ]. % 0.70/0.90 cut (((c_tptpcol_13_92263) = (c_tptpcol_13_92263)) = ((c_tptpcol_12_92262) = (c_tptpcol_13_92263))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H210. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H214. % 0.70/0.90 cut (((c_tptpcol_13_92263) = (c_tptpcol_13_92263))); [idtac | apply NNPP; zenon_intro zenon_Hc2]. % 0.70/0.90 cut (((c_tptpcol_13_92263) = (c_tptpcol_12_92262))); [idtac | apply NNPP; zenon_intro zenon_H20f]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_H20f zenon_H213). % 0.70/0.90 apply zenon_Hc2. apply refl_equal. % 0.70/0.90 apply zenon_Hc2. apply refl_equal. % 0.70/0.90 apply zenon_H211. zenon_intro just59. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_13_92263)). zenon_intro zenon_H215. % 0.70/0.90 generalize (zenon_H215 (c_tptpcol_12_92262)). zenon_intro zenon_H216. % 0.70/0.90 generalize (zenon_H216 (c_tptpcol_11_92230)). zenon_intro zenon_H217. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H217); [ zenon_intro zenon_H20e | zenon_intro zenon_H218 ]. % 0.70/0.90 exact (zenon_H20e just59). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H218); [ zenon_intro zenon_H21a | zenon_intro zenon_H219 ]. % 0.70/0.90 exact (zenon_H21a just57). % 0.70/0.90 exact (zenon_H20a zenon_H219). % 0.70/0.90 apply zenon_Hab. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_11_92230) (c_tptpcol_10_92166)) = (genls (c_tptpcol_13_92263) (c_tptpcol_10_92166))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H206. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just55. % 0.70/0.90 cut (((c_tptpcol_10_92166) = (c_tptpcol_10_92166))); [idtac | apply NNPP; zenon_intro zenon_Hac]. % 0.70/0.90 cut (((c_tptpcol_11_92230) = (c_tptpcol_13_92263))); [idtac | apply NNPP; zenon_intro zenon_H21b]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H209); [ zenon_intro zenon_H21d | zenon_intro zenon_H21c ]. % 0.70/0.90 apply zenon_H21d. zenon_intro zenon_H21e. % 0.70/0.90 elim (classic ((c_tptpcol_13_92263) = (c_tptpcol_13_92263))); [ zenon_intro zenon_H214 | zenon_intro zenon_Hc2 ]. % 0.70/0.90 cut (((c_tptpcol_13_92263) = (c_tptpcol_13_92263)) = ((c_tptpcol_11_92230) = (c_tptpcol_13_92263))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H21b. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H214. % 0.70/0.90 cut (((c_tptpcol_13_92263) = (c_tptpcol_13_92263))); [idtac | apply NNPP; zenon_intro zenon_Hc2]. % 0.70/0.90 cut (((c_tptpcol_13_92263) = (c_tptpcol_11_92230))); [idtac | apply NNPP; zenon_intro zenon_H20b]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_H20b zenon_H21e). % 0.70/0.90 apply zenon_Hc2. apply refl_equal. % 0.70/0.90 apply zenon_Hc2. apply refl_equal. % 0.70/0.90 apply zenon_H21c. zenon_intro zenon_H219. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_13_92263)). zenon_intro zenon_H215. % 0.70/0.90 generalize (zenon_H215 (c_tptpcol_11_92230)). zenon_intro zenon_H21f. % 0.70/0.90 generalize (zenon_H21f (c_tptpcol_10_92166)). zenon_intro zenon_H220. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H220); [ zenon_intro zenon_H20a | zenon_intro zenon_H221 ]. % 0.70/0.90 exact (zenon_H20a zenon_H219). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H221); [ zenon_intro zenon_H223 | zenon_intro zenon_H222 ]. % 0.70/0.90 exact (zenon_H223 just55). % 0.70/0.90 exact (zenon_H206 zenon_H222). % 0.70/0.90 apply zenon_Hac. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_10_92166) (c_tptpcol_9_92165)) = (genls (c_tptpcol_13_92263) (c_tptpcol_9_92165))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H202. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just53. % 0.70/0.90 cut (((c_tptpcol_9_92165) = (c_tptpcol_9_92165))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 0.70/0.90 cut (((c_tptpcol_10_92166) = (c_tptpcol_13_92263))); [idtac | apply NNPP; zenon_intro zenon_H224]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H205); [ zenon_intro zenon_H226 | zenon_intro zenon_H225 ]. % 0.70/0.90 apply zenon_H226. zenon_intro zenon_H227. % 0.70/0.90 elim (classic ((c_tptpcol_13_92263) = (c_tptpcol_13_92263))); [ zenon_intro zenon_H214 | zenon_intro zenon_Hc2 ]. % 0.70/0.90 cut (((c_tptpcol_13_92263) = (c_tptpcol_13_92263)) = ((c_tptpcol_10_92166) = (c_tptpcol_13_92263))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H224. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H214. % 0.70/0.90 cut (((c_tptpcol_13_92263) = (c_tptpcol_13_92263))); [idtac | apply NNPP; zenon_intro zenon_Hc2]. % 0.70/0.90 cut (((c_tptpcol_13_92263) = (c_tptpcol_10_92166))); [idtac | apply NNPP; zenon_intro zenon_H207]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_H207 zenon_H227). % 0.70/0.90 apply zenon_Hc2. apply refl_equal. % 0.70/0.90 apply zenon_Hc2. apply refl_equal. % 0.70/0.90 apply zenon_H225. zenon_intro zenon_H222. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_13_92263)). zenon_intro zenon_H215. % 0.70/0.90 generalize (zenon_H215 (c_tptpcol_10_92166)). zenon_intro zenon_H228. % 0.70/0.90 generalize (zenon_H228 (c_tptpcol_9_92165)). zenon_intro zenon_H229. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H229); [ zenon_intro zenon_H206 | zenon_intro zenon_H22a ]. % 0.70/0.90 exact (zenon_H206 zenon_H222). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H22a); [ zenon_intro zenon_H22c | zenon_intro zenon_H22b ]. % 0.70/0.90 exact (zenon_H22c just53). % 0.70/0.90 exact (zenon_H202 zenon_H22b). % 0.70/0.90 apply zenon_Had. apply refl_equal. % 0.70/0.90 cut ((genls (c_tptpcol_9_92165) (c_tptpcol_8_92164)) = (genls (c_tptpcol_13_92263) (c_tptpcol_8_92164))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H1a9. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact just51. % 0.70/0.90 cut (((c_tptpcol_8_92164) = (c_tptpcol_8_92164))); [idtac | apply NNPP; zenon_intro zenon_Hae]. % 0.70/0.90 cut (((c_tptpcol_9_92165) = (c_tptpcol_13_92263))); [idtac | apply NNPP; zenon_intro zenon_H22d]. % 0.70/0.90 congruence. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H201); [ zenon_intro zenon_H22f | zenon_intro zenon_H22e ]. % 0.70/0.90 apply zenon_H22f. zenon_intro zenon_H230. % 0.70/0.90 elim (classic ((c_tptpcol_13_92263) = (c_tptpcol_13_92263))); [ zenon_intro zenon_H214 | zenon_intro zenon_Hc2 ]. % 0.70/0.90 cut (((c_tptpcol_13_92263) = (c_tptpcol_13_92263)) = ((c_tptpcol_9_92165) = (c_tptpcol_13_92263))). % 0.70/0.90 intro zenon_D_pnotp. % 0.70/0.90 apply zenon_H22d. % 0.70/0.90 rewrite <- zenon_D_pnotp. % 0.70/0.90 exact zenon_H214. % 0.70/0.90 cut (((c_tptpcol_13_92263) = (c_tptpcol_13_92263))); [idtac | apply NNPP; zenon_intro zenon_Hc2]. % 0.70/0.90 cut (((c_tptpcol_13_92263) = (c_tptpcol_9_92165))); [idtac | apply NNPP; zenon_intro zenon_H203]. % 0.70/0.90 congruence. % 0.70/0.90 exact (zenon_H203 zenon_H230). % 0.70/0.90 apply zenon_Hc2. apply refl_equal. % 0.70/0.90 apply zenon_Hc2. apply refl_equal. % 0.70/0.90 apply zenon_H22e. zenon_intro zenon_H22b. % 0.70/0.90 generalize (zenon_Hb0 (c_tptpcol_13_92263)). zenon_intro zenon_H215. % 0.70/0.90 generalize (zenon_H215 (c_tptpcol_9_92165)). zenon_intro zenon_H231. % 0.70/0.90 generalize (zenon_H231 (c_tptpcol_8_92164)). zenon_intro zenon_H232. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H232); [ zenon_intro zenon_H202 | zenon_intro zenon_H233 ]. % 0.70/0.90 exact (zenon_H202 zenon_H22b). % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H233); [ zenon_intro zenon_H235 | zenon_intro zenon_H234 ]. % 0.70/0.90 exact (zenon_H235 just51). % 0.70/0.90 exact (zenon_H1a9 zenon_H234). % 0.70/0.90 apply zenon_Hae. apply refl_equal. % 0.70/0.90 generalize (zenon_H1a4 (c_tptpcol_16_92269)). zenon_intro zenon_H236. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H236); [ zenon_intro zenon_H237 | zenon_intro zenon_He0 ]. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H237); [ zenon_intro zenon_H238 | zenon_intro zenon_Hc3 ]. % 0.70/0.90 exact (zenon_H238 zenon_H1a7). % 0.70/0.90 apply (zenon_L14_); trivial. % 0.70/0.90 apply (zenon_L29_); trivial. % 0.70/0.90 apply zenon_H1a0. zenon_intro zenon_Tx_vx. apply NNPP. zenon_intro zenon_H23a. % 0.70/0.90 apply zenon_H23a. zenon_intro zenon_Ty_vz. apply NNPP. zenon_intro zenon_H23c. % 0.70/0.90 apply zenon_H23c. zenon_intro zenon_Tz_wb. apply NNPP. zenon_intro zenon_H23e. % 0.70/0.90 apply (zenon_notimply_s _ _ zenon_H23e). zenon_intro zenon_H240. zenon_intro zenon_H23f. % 0.70/0.90 apply (zenon_notimply_s _ _ zenon_H23f). zenon_intro zenon_H242. zenon_intro zenon_H241. % 0.70/0.90 generalize (just155 zenon_Tx_vx). zenon_intro zenon_H243. % 0.70/0.90 generalize (zenon_H243 zenon_Ty_vz). zenon_intro zenon_H244. % 0.70/0.90 generalize (zenon_H244 zenon_Tz_wb). zenon_intro zenon_H245. % 0.70/0.90 apply (zenon_imply_s _ _ zenon_H245); [ zenon_intro zenon_H247 | zenon_intro zenon_H246 ]. % 0.70/0.90 apply (zenon_notand_s _ _ zenon_H247); [ zenon_intro zenon_H249 | zenon_intro zenon_H248 ]. % 0.70/0.90 exact (zenon_H249 zenon_H240). % 0.70/0.90 exact (zenon_H248 zenon_H242). % 0.70/0.90 exact (zenon_H241 zenon_H246). % 0.70/0.90 Qed. % 0.70/0.90 % SZS output end Proof % 0.70/0.90 (* END-PROOF *) % 0.70/0.90 nodes searched: 13863 % 0.70/0.90 max branch formulas: 5543 % 0.70/0.90 proof nodes created: 123 % 0.70/0.90 formulas created: 70741 % 0.70/0.90 %------------------------------------------------------------------------------