%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR036+1 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n009.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:01:57 EDT 2022 % Result : Theorem 0.85s 1.03s % Output : Proof 0.85s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.14 % Problem : CSR036+1 : TPTP v8.1.0. Released v3.4.0. % 0.12/0.15 % Command : run_zenon %s %d % 0.15/0.37 % Computer : n009.cluster.edu % 0.15/0.37 % Model : x86_64 x86_64 % 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.37 % Memory : 8042.1875MB % 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.37 % CPULimit : 300 % 0.15/0.37 % WCLimit : 600 % 0.15/0.37 % DateTime : Sat Jun 11 13:34:38 EDT 2022 % 0.15/0.37 % CPUTime : % 0.85/1.03 (* PROOF-FOUND *) % 0.85/1.03 % SZS status Theorem % 0.85/1.03 (* BEGIN-PROOF *) % 0.85/1.03 % SZS output start Proof % 0.85/1.03 Theorem query36 : ((mtvisible (c_tptp_member974_mt))->(disjointwith (c_tptpcol_15_22076) (c_tptpcol_16_72795))). % 0.85/1.03 Proof. % 0.85/1.03 assert (zenon_L1_ : (~((c_tptpcol_12_72775) = (c_tptpcol_12_72775))) -> False). % 0.85/1.03 do 0 intro. intros zenon_Ha2. % 0.85/1.03 apply zenon_Ha2. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L1_ *) % 0.85/1.03 assert (zenon_L2_ : (~((c_tptpcol_11_72774) = (c_tptpcol_11_72774))) -> False). % 0.85/1.03 do 0 intro. intros zenon_Ha3. % 0.85/1.03 apply zenon_Ha3. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L2_ *) % 0.85/1.03 assert (zenon_L3_ : (~((c_tptpcol_10_72710) = (c_tptpcol_10_72710))) -> False). % 0.85/1.03 do 0 intro. intros zenon_Ha4. % 0.85/1.03 apply zenon_Ha4. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L3_ *) % 0.85/1.03 assert (zenon_L4_ : (~((c_tptpcol_9_72709) = (c_tptpcol_9_72709))) -> False). % 0.85/1.03 do 0 intro. intros zenon_Ha5. % 0.85/1.03 apply zenon_Ha5. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L4_ *) % 0.85/1.03 assert (zenon_L5_ : (~((c_tptpcol_8_72708) = (c_tptpcol_8_72708))) -> False). % 0.85/1.03 do 0 intro. intros zenon_Ha6. % 0.85/1.03 apply zenon_Ha6. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L5_ *) % 0.85/1.03 assert (zenon_L6_ : (~((c_tptpcol_7_72707) = (c_tptpcol_7_72707))) -> False). % 0.85/1.03 do 0 intro. intros zenon_Ha7. % 0.85/1.03 apply zenon_Ha7. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L6_ *) % 0.85/1.03 assert (zenon_L7_ : (~((c_tptpcol_6_71683) = (c_tptpcol_6_71683))) -> False). % 0.85/1.03 do 0 intro. intros zenon_Ha8. % 0.85/1.03 apply zenon_Ha8. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L7_ *) % 0.85/1.03 assert (zenon_L8_ : (~((c_tptpcol_5_69635) = (c_tptpcol_5_69635))) -> False). % 0.85/1.03 do 0 intro. intros zenon_Ha9. % 0.85/1.03 apply zenon_Ha9. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L8_ *) % 0.85/1.03 assert (zenon_L9_ : (~((c_tptpcol_4_65539) = (c_tptpcol_4_65539))) -> False). % 0.85/1.03 do 0 intro. intros zenon_Haa. % 0.85/1.03 apply zenon_Haa. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L9_ *) % 0.85/1.03 assert (zenon_L10_ : (~((c_tptpcol_3_65538) = (c_tptpcol_3_65538))) -> False). % 0.85/1.03 do 0 intro. intros zenon_Hab. % 0.85/1.03 apply zenon_Hab. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L10_ *) % 0.85/1.03 assert (zenon_L11_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (~(genls (c_tptpcol_14_72792) (c_tptpcol_3_65538))) -> False). % 0.85/1.03 do 0 intro. intros zenon_Hac zenon_Had. % 0.85/1.03 elim (classic ((~((c_tptpcol_14_72792) = (c_tptpcol_4_65539)))/\(~(genls (c_tptpcol_14_72792) (c_tptpcol_4_65539))))); [ zenon_intro zenon_Hae | zenon_intro zenon_Haf ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_Hae). zenon_intro zenon_Hb1. zenon_intro zenon_Hb0. % 0.85/1.03 elim (classic ((~((c_tptpcol_14_72792) = (c_tptpcol_5_69635)))/\(~(genls (c_tptpcol_14_72792) (c_tptpcol_5_69635))))); [ zenon_intro zenon_Hb2 | zenon_intro zenon_Hb3 ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_Hb2). zenon_intro zenon_Hb5. zenon_intro zenon_Hb4. % 0.85/1.03 elim (classic ((~((c_tptpcol_14_72792) = (c_tptpcol_6_71683)))/\(~(genls (c_tptpcol_14_72792) (c_tptpcol_6_71683))))); [ zenon_intro zenon_Hb6 | zenon_intro zenon_Hb7 ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_Hb6). zenon_intro zenon_Hb9. zenon_intro zenon_Hb8. % 0.85/1.03 elim (classic ((~((c_tptpcol_14_72792) = (c_tptpcol_7_72707)))/\(~(genls (c_tptpcol_14_72792) (c_tptpcol_7_72707))))); [ zenon_intro zenon_Hba | zenon_intro zenon_Hbb ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_Hba). zenon_intro zenon_Hbd. zenon_intro zenon_Hbc. % 0.85/1.03 elim (classic ((~((c_tptpcol_14_72792) = (c_tptpcol_8_72708)))/\(~(genls (c_tptpcol_14_72792) (c_tptpcol_8_72708))))); [ zenon_intro zenon_Hbe | zenon_intro zenon_Hbf ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_Hbe). zenon_intro zenon_Hc1. zenon_intro zenon_Hc0. % 0.85/1.03 elim (classic ((~((c_tptpcol_14_72792) = (c_tptpcol_9_72709)))/\(~(genls (c_tptpcol_14_72792) (c_tptpcol_9_72709))))); [ zenon_intro zenon_Hc2 | zenon_intro zenon_Hc3 ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_Hc2). zenon_intro zenon_Hc5. zenon_intro zenon_Hc4. % 0.85/1.03 elim (classic ((~((c_tptpcol_14_72792) = (c_tptpcol_10_72710)))/\(~(genls (c_tptpcol_14_72792) (c_tptpcol_10_72710))))); [ zenon_intro zenon_Hc6 | zenon_intro zenon_Hc7 ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_Hc6). zenon_intro zenon_Hc9. zenon_intro zenon_Hc8. % 0.85/1.03 elim (classic ((~((c_tptpcol_14_72792) = (c_tptpcol_11_72774)))/\(~(genls (c_tptpcol_14_72792) (c_tptpcol_11_72774))))); [ zenon_intro zenon_Hca | zenon_intro zenon_Hcb ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_Hca). zenon_intro zenon_Hcd. zenon_intro zenon_Hcc. % 0.85/1.03 elim (classic ((~((c_tptpcol_14_72792) = (c_tptpcol_12_72775)))/\(~(genls (c_tptpcol_14_72792) (c_tptpcol_12_72775))))); [ zenon_intro zenon_Hce | zenon_intro zenon_Hcf ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_Hce). zenon_intro zenon_Hd1. zenon_intro zenon_Hd0. % 0.85/1.03 elim (classic ((~((c_tptpcol_14_72792) = (c_tptpcol_13_72791)))/\(~(genls (c_tptpcol_14_72792) (c_tptpcol_13_72791))))); [ zenon_intro zenon_Hd2 | zenon_intro zenon_Hd3 ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_Hd2). zenon_intro zenon_Hd5. zenon_intro zenon_Hd4. % 0.85/1.03 exact (zenon_Hd4 just58). % 0.85/1.03 cut ((genls (c_tptpcol_13_72791) (c_tptpcol_12_72775)) = (genls (c_tptpcol_14_72792) (c_tptpcol_12_72775))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_Hd0. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact just56. % 0.85/1.03 cut (((c_tptpcol_12_72775) = (c_tptpcol_12_72775))); [idtac | apply NNPP; zenon_intro zenon_Ha2]. % 0.85/1.03 cut (((c_tptpcol_13_72791) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_Hd6]. % 0.85/1.03 congruence. % 0.85/1.03 apply (zenon_notand_s _ _ zenon_Hd3); [ zenon_intro zenon_Hd8 | zenon_intro zenon_Hd7 ]. % 0.85/1.03 apply zenon_Hd8. zenon_intro zenon_Hd9. % 0.85/1.03 elim (classic ((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792)) = ((c_tptpcol_13_72791) = (c_tptpcol_14_72792))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_Hd6. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact zenon_Hda. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_13_72791))); [idtac | apply NNPP; zenon_intro zenon_Hd5]. % 0.85/1.03 congruence. % 0.85/1.03 exact (zenon_Hd5 zenon_Hd9). % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_Hd7. zenon_intro just58. % 0.85/1.03 generalize (zenon_Hac (c_tptpcol_14_72792)). zenon_intro zenon_Hdc. % 0.85/1.03 generalize (zenon_Hdc (c_tptpcol_13_72791)). zenon_intro zenon_Hdd. % 0.85/1.03 generalize (zenon_Hdd (c_tptpcol_12_72775)). zenon_intro zenon_Hde. % 0.85/1.03 apply (zenon_imply_s _ _ zenon_Hde); [ zenon_intro zenon_Hd4 | zenon_intro zenon_Hdf ]. % 0.85/1.03 exact (zenon_Hd4 just58). % 0.85/1.03 apply (zenon_imply_s _ _ zenon_Hdf); [ zenon_intro zenon_He1 | zenon_intro zenon_He0 ]. % 0.85/1.03 exact (zenon_He1 just56). % 0.85/1.03 exact (zenon_Hd0 zenon_He0). % 0.85/1.03 apply zenon_Ha2. apply refl_equal. % 0.85/1.03 cut ((genls (c_tptpcol_12_72775) (c_tptpcol_11_72774)) = (genls (c_tptpcol_14_72792) (c_tptpcol_11_72774))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_Hcc. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact just54. % 0.85/1.03 cut (((c_tptpcol_11_72774) = (c_tptpcol_11_72774))); [idtac | apply NNPP; zenon_intro zenon_Ha3]. % 0.85/1.03 cut (((c_tptpcol_12_72775) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_He2]. % 0.85/1.03 congruence. % 0.85/1.03 apply (zenon_notand_s _ _ zenon_Hcf); [ zenon_intro zenon_He4 | zenon_intro zenon_He3 ]. % 0.85/1.03 apply zenon_He4. zenon_intro zenon_He5. % 0.85/1.03 elim (classic ((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792)) = ((c_tptpcol_12_72775) = (c_tptpcol_14_72792))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_He2. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact zenon_Hda. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_12_72775))); [idtac | apply NNPP; zenon_intro zenon_Hd1]. % 0.85/1.03 congruence. % 0.85/1.03 exact (zenon_Hd1 zenon_He5). % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_He3. zenon_intro zenon_He0. % 0.85/1.03 generalize (zenon_Hac (c_tptpcol_14_72792)). zenon_intro zenon_Hdc. % 0.85/1.03 generalize (zenon_Hdc (c_tptpcol_12_72775)). zenon_intro zenon_He6. % 0.85/1.03 generalize (zenon_He6 (c_tptpcol_11_72774)). zenon_intro zenon_He7. % 0.85/1.03 apply (zenon_imply_s _ _ zenon_He7); [ zenon_intro zenon_Hd0 | zenon_intro zenon_He8 ]. % 0.85/1.03 exact (zenon_Hd0 zenon_He0). % 0.85/1.03 apply (zenon_imply_s _ _ zenon_He8); [ zenon_intro zenon_Hea | zenon_intro zenon_He9 ]. % 0.85/1.03 exact (zenon_Hea just54). % 0.85/1.03 exact (zenon_Hcc zenon_He9). % 0.85/1.03 apply zenon_Ha3. apply refl_equal. % 0.85/1.03 cut ((genls (c_tptpcol_11_72774) (c_tptpcol_10_72710)) = (genls (c_tptpcol_14_72792) (c_tptpcol_10_72710))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_Hc8. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact just52. % 0.85/1.03 cut (((c_tptpcol_10_72710) = (c_tptpcol_10_72710))); [idtac | apply NNPP; zenon_intro zenon_Ha4]. % 0.85/1.03 cut (((c_tptpcol_11_72774) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_Heb]. % 0.85/1.03 congruence. % 0.85/1.03 apply (zenon_notand_s _ _ zenon_Hcb); [ zenon_intro zenon_Hed | zenon_intro zenon_Hec ]. % 0.85/1.03 apply zenon_Hed. zenon_intro zenon_Hee. % 0.85/1.03 elim (classic ((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792)) = ((c_tptpcol_11_72774) = (c_tptpcol_14_72792))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_Heb. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact zenon_Hda. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_11_72774))); [idtac | apply NNPP; zenon_intro zenon_Hcd]. % 0.85/1.03 congruence. % 0.85/1.03 exact (zenon_Hcd zenon_Hee). % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_Hec. zenon_intro zenon_He9. % 0.85/1.03 generalize (zenon_Hac (c_tptpcol_14_72792)). zenon_intro zenon_Hdc. % 0.85/1.03 generalize (zenon_Hdc (c_tptpcol_11_72774)). zenon_intro zenon_Hef. % 0.85/1.03 generalize (zenon_Hef (c_tptpcol_10_72710)). zenon_intro zenon_Hf0. % 0.85/1.03 apply (zenon_imply_s _ _ zenon_Hf0); [ zenon_intro zenon_Hcc | zenon_intro zenon_Hf1 ]. % 0.85/1.03 exact (zenon_Hcc zenon_He9). % 0.85/1.03 apply (zenon_imply_s _ _ zenon_Hf1); [ zenon_intro zenon_Hf3 | zenon_intro zenon_Hf2 ]. % 0.85/1.03 exact (zenon_Hf3 just52). % 0.85/1.03 exact (zenon_Hc8 zenon_Hf2). % 0.85/1.03 apply zenon_Ha4. apply refl_equal. % 0.85/1.03 cut ((genls (c_tptpcol_10_72710) (c_tptpcol_9_72709)) = (genls (c_tptpcol_14_72792) (c_tptpcol_9_72709))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_Hc4. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact just50. % 0.85/1.03 cut (((c_tptpcol_9_72709) = (c_tptpcol_9_72709))); [idtac | apply NNPP; zenon_intro zenon_Ha5]. % 0.85/1.03 cut (((c_tptpcol_10_72710) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_Hf4]. % 0.85/1.03 congruence. % 0.85/1.03 apply (zenon_notand_s _ _ zenon_Hc7); [ zenon_intro zenon_Hf6 | zenon_intro zenon_Hf5 ]. % 0.85/1.03 apply zenon_Hf6. zenon_intro zenon_Hf7. % 0.85/1.03 elim (classic ((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792)) = ((c_tptpcol_10_72710) = (c_tptpcol_14_72792))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_Hf4. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact zenon_Hda. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_10_72710))); [idtac | apply NNPP; zenon_intro zenon_Hc9]. % 0.85/1.03 congruence. % 0.85/1.03 exact (zenon_Hc9 zenon_Hf7). % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_Hf5. zenon_intro zenon_Hf2. % 0.85/1.03 generalize (zenon_Hac (c_tptpcol_14_72792)). zenon_intro zenon_Hdc. % 0.85/1.03 generalize (zenon_Hdc (c_tptpcol_10_72710)). zenon_intro zenon_Hf8. % 0.85/1.03 generalize (zenon_Hf8 (c_tptpcol_9_72709)). zenon_intro zenon_Hf9. % 0.85/1.03 apply (zenon_imply_s _ _ zenon_Hf9); [ zenon_intro zenon_Hc8 | zenon_intro zenon_Hfa ]. % 0.85/1.03 exact (zenon_Hc8 zenon_Hf2). % 0.85/1.03 apply (zenon_imply_s _ _ zenon_Hfa); [ zenon_intro zenon_Hfc | zenon_intro zenon_Hfb ]. % 0.85/1.03 exact (zenon_Hfc just50). % 0.85/1.03 exact (zenon_Hc4 zenon_Hfb). % 0.85/1.03 apply zenon_Ha5. apply refl_equal. % 0.85/1.03 cut ((genls (c_tptpcol_9_72709) (c_tptpcol_8_72708)) = (genls (c_tptpcol_14_72792) (c_tptpcol_8_72708))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_Hc0. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact just48. % 0.85/1.03 cut (((c_tptpcol_8_72708) = (c_tptpcol_8_72708))); [idtac | apply NNPP; zenon_intro zenon_Ha6]. % 0.85/1.03 cut (((c_tptpcol_9_72709) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_Hfd]. % 0.85/1.03 congruence. % 0.85/1.03 apply (zenon_notand_s _ _ zenon_Hc3); [ zenon_intro zenon_Hff | zenon_intro zenon_Hfe ]. % 0.85/1.03 apply zenon_Hff. zenon_intro zenon_H100. % 0.85/1.03 elim (classic ((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792)) = ((c_tptpcol_9_72709) = (c_tptpcol_14_72792))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_Hfd. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact zenon_Hda. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_9_72709))); [idtac | apply NNPP; zenon_intro zenon_Hc5]. % 0.85/1.03 congruence. % 0.85/1.03 exact (zenon_Hc5 zenon_H100). % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_Hfe. zenon_intro zenon_Hfb. % 0.85/1.03 generalize (zenon_Hac (c_tptpcol_14_72792)). zenon_intro zenon_Hdc. % 0.85/1.03 generalize (zenon_Hdc (c_tptpcol_9_72709)). zenon_intro zenon_H101. % 0.85/1.03 generalize (zenon_H101 (c_tptpcol_8_72708)). zenon_intro zenon_H102. % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H102); [ zenon_intro zenon_Hc4 | zenon_intro zenon_H103 ]. % 0.85/1.03 exact (zenon_Hc4 zenon_Hfb). % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H103); [ zenon_intro zenon_H105 | zenon_intro zenon_H104 ]. % 0.85/1.03 exact (zenon_H105 just48). % 0.85/1.03 exact (zenon_Hc0 zenon_H104). % 0.85/1.03 apply zenon_Ha6. apply refl_equal. % 0.85/1.03 cut ((genls (c_tptpcol_8_72708) (c_tptpcol_7_72707)) = (genls (c_tptpcol_14_72792) (c_tptpcol_7_72707))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_Hbc. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact just46. % 0.85/1.03 cut (((c_tptpcol_7_72707) = (c_tptpcol_7_72707))); [idtac | apply NNPP; zenon_intro zenon_Ha7]. % 0.85/1.03 cut (((c_tptpcol_8_72708) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_H106]. % 0.85/1.03 congruence. % 0.85/1.03 apply (zenon_notand_s _ _ zenon_Hbf); [ zenon_intro zenon_H108 | zenon_intro zenon_H107 ]. % 0.85/1.03 apply zenon_H108. zenon_intro zenon_H109. % 0.85/1.03 elim (classic ((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792)) = ((c_tptpcol_8_72708) = (c_tptpcol_14_72792))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_H106. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact zenon_Hda. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_8_72708))); [idtac | apply NNPP; zenon_intro zenon_Hc1]. % 0.85/1.03 congruence. % 0.85/1.03 exact (zenon_Hc1 zenon_H109). % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_H107. zenon_intro zenon_H104. % 0.85/1.03 generalize (zenon_Hac (c_tptpcol_14_72792)). zenon_intro zenon_Hdc. % 0.85/1.03 generalize (zenon_Hdc (c_tptpcol_8_72708)). zenon_intro zenon_H10a. % 0.85/1.03 generalize (zenon_H10a (c_tptpcol_7_72707)). zenon_intro zenon_H10b. % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H10b); [ zenon_intro zenon_Hc0 | zenon_intro zenon_H10c ]. % 0.85/1.03 exact (zenon_Hc0 zenon_H104). % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H10c); [ zenon_intro zenon_H10e | zenon_intro zenon_H10d ]. % 0.85/1.03 exact (zenon_H10e just46). % 0.85/1.03 exact (zenon_Hbc zenon_H10d). % 0.85/1.03 apply zenon_Ha7. apply refl_equal. % 0.85/1.03 cut ((genls (c_tptpcol_7_72707) (c_tptpcol_6_71683)) = (genls (c_tptpcol_14_72792) (c_tptpcol_6_71683))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_Hb8. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact just44. % 0.85/1.03 cut (((c_tptpcol_6_71683) = (c_tptpcol_6_71683))); [idtac | apply NNPP; zenon_intro zenon_Ha8]. % 0.85/1.03 cut (((c_tptpcol_7_72707) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_H10f]. % 0.85/1.03 congruence. % 0.85/1.03 apply (zenon_notand_s _ _ zenon_Hbb); [ zenon_intro zenon_H111 | zenon_intro zenon_H110 ]. % 0.85/1.03 apply zenon_H111. zenon_intro zenon_H112. % 0.85/1.03 elim (classic ((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792)) = ((c_tptpcol_7_72707) = (c_tptpcol_14_72792))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_H10f. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact zenon_Hda. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_7_72707))); [idtac | apply NNPP; zenon_intro zenon_Hbd]. % 0.85/1.03 congruence. % 0.85/1.03 exact (zenon_Hbd zenon_H112). % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_H110. zenon_intro zenon_H10d. % 0.85/1.03 generalize (zenon_Hac (c_tptpcol_14_72792)). zenon_intro zenon_Hdc. % 0.85/1.03 generalize (zenon_Hdc (c_tptpcol_7_72707)). zenon_intro zenon_H113. % 0.85/1.03 generalize (zenon_H113 (c_tptpcol_6_71683)). zenon_intro zenon_H114. % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H114); [ zenon_intro zenon_Hbc | zenon_intro zenon_H115 ]. % 0.85/1.03 exact (zenon_Hbc zenon_H10d). % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H115); [ zenon_intro zenon_H117 | zenon_intro zenon_H116 ]. % 0.85/1.03 exact (zenon_H117 just44). % 0.85/1.03 exact (zenon_Hb8 zenon_H116). % 0.85/1.03 apply zenon_Ha8. apply refl_equal. % 0.85/1.03 cut ((genls (c_tptpcol_6_71683) (c_tptpcol_5_69635)) = (genls (c_tptpcol_14_72792) (c_tptpcol_5_69635))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_Hb4. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact just42. % 0.85/1.03 cut (((c_tptpcol_5_69635) = (c_tptpcol_5_69635))); [idtac | apply NNPP; zenon_intro zenon_Ha9]. % 0.85/1.03 cut (((c_tptpcol_6_71683) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_H118]. % 0.85/1.03 congruence. % 0.85/1.03 apply (zenon_notand_s _ _ zenon_Hb7); [ zenon_intro zenon_H11a | zenon_intro zenon_H119 ]. % 0.85/1.03 apply zenon_H11a. zenon_intro zenon_H11b. % 0.85/1.03 elim (classic ((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792)) = ((c_tptpcol_6_71683) = (c_tptpcol_14_72792))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_H118. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact zenon_Hda. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_6_71683))); [idtac | apply NNPP; zenon_intro zenon_Hb9]. % 0.85/1.03 congruence. % 0.85/1.03 exact (zenon_Hb9 zenon_H11b). % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_H119. zenon_intro zenon_H116. % 0.85/1.03 generalize (zenon_Hac (c_tptpcol_14_72792)). zenon_intro zenon_Hdc. % 0.85/1.03 generalize (zenon_Hdc (c_tptpcol_6_71683)). zenon_intro zenon_H11c. % 0.85/1.03 generalize (zenon_H11c (c_tptpcol_5_69635)). zenon_intro zenon_H11d. % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H11d); [ zenon_intro zenon_Hb8 | zenon_intro zenon_H11e ]. % 0.85/1.03 exact (zenon_Hb8 zenon_H116). % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H11e); [ zenon_intro zenon_H120 | zenon_intro zenon_H11f ]. % 0.85/1.03 exact (zenon_H120 just42). % 0.85/1.03 exact (zenon_Hb4 zenon_H11f). % 0.85/1.03 apply zenon_Ha9. apply refl_equal. % 0.85/1.03 cut ((genls (c_tptpcol_5_69635) (c_tptpcol_4_65539)) = (genls (c_tptpcol_14_72792) (c_tptpcol_4_65539))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_Hb0. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact just40. % 0.85/1.03 cut (((c_tptpcol_4_65539) = (c_tptpcol_4_65539))); [idtac | apply NNPP; zenon_intro zenon_Haa]. % 0.85/1.03 cut (((c_tptpcol_5_69635) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_H121]. % 0.85/1.03 congruence. % 0.85/1.03 apply (zenon_notand_s _ _ zenon_Hb3); [ zenon_intro zenon_H123 | zenon_intro zenon_H122 ]. % 0.85/1.03 apply zenon_H123. zenon_intro zenon_H124. % 0.85/1.03 elim (classic ((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792)) = ((c_tptpcol_5_69635) = (c_tptpcol_14_72792))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_H121. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact zenon_Hda. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_5_69635))); [idtac | apply NNPP; zenon_intro zenon_Hb5]. % 0.85/1.03 congruence. % 0.85/1.03 exact (zenon_Hb5 zenon_H124). % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_H122. zenon_intro zenon_H11f. % 0.85/1.03 generalize (zenon_Hac (c_tptpcol_14_72792)). zenon_intro zenon_Hdc. % 0.85/1.03 generalize (zenon_Hdc (c_tptpcol_5_69635)). zenon_intro zenon_H125. % 0.85/1.03 generalize (zenon_H125 (c_tptpcol_4_65539)). zenon_intro zenon_H126. % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H126); [ zenon_intro zenon_Hb4 | zenon_intro zenon_H127 ]. % 0.85/1.03 exact (zenon_Hb4 zenon_H11f). % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H127); [ zenon_intro zenon_H129 | zenon_intro zenon_H128 ]. % 0.85/1.03 exact (zenon_H129 just40). % 0.85/1.03 exact (zenon_Hb0 zenon_H128). % 0.85/1.03 apply zenon_Haa. apply refl_equal. % 0.85/1.03 cut ((genls (c_tptpcol_4_65539) (c_tptpcol_3_65538)) = (genls (c_tptpcol_14_72792) (c_tptpcol_3_65538))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_Had. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact just38. % 0.85/1.03 cut (((c_tptpcol_3_65538) = (c_tptpcol_3_65538))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 0.85/1.03 cut (((c_tptpcol_4_65539) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_H12a]. % 0.85/1.03 congruence. % 0.85/1.03 apply (zenon_notand_s _ _ zenon_Haf); [ zenon_intro zenon_H12c | zenon_intro zenon_H12b ]. % 0.85/1.03 apply zenon_H12c. zenon_intro zenon_H12d. % 0.85/1.03 elim (classic ((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792)) = ((c_tptpcol_4_65539) = (c_tptpcol_14_72792))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_H12a. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact zenon_Hda. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_4_65539))); [idtac | apply NNPP; zenon_intro zenon_Hb1]. % 0.85/1.03 congruence. % 0.85/1.03 exact (zenon_Hb1 zenon_H12d). % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 apply zenon_H12b. zenon_intro zenon_H128. % 0.85/1.03 generalize (zenon_Hac (c_tptpcol_14_72792)). zenon_intro zenon_Hdc. % 0.85/1.03 generalize (zenon_Hdc (c_tptpcol_4_65539)). zenon_intro zenon_H12e. % 0.85/1.03 generalize (zenon_H12e (c_tptpcol_3_65538)). zenon_intro zenon_H12f. % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H12f); [ zenon_intro zenon_Hb0 | zenon_intro zenon_H130 ]. % 0.85/1.03 exact (zenon_Hb0 zenon_H128). % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H130); [ zenon_intro zenon_H132 | zenon_intro zenon_H131 ]. % 0.85/1.03 exact (zenon_H132 just38). % 0.85/1.03 exact (zenon_Had zenon_H131). % 0.85/1.03 apply zenon_Hab. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L11_ *) % 0.85/1.03 assert (zenon_L12_ : (~((c_tptpcol_2_65537) = (c_tptpcol_2_65537))) -> False). % 0.85/1.03 do 0 intro. intros zenon_H133. % 0.85/1.03 apply zenon_H133. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L12_ *) % 0.85/1.03 assert (zenon_L13_ : (~((c_tptpcol_1_65536) = (c_tptpcol_1_65536))) -> False). % 0.85/1.03 do 0 intro. intros zenon_H134. % 0.85/1.03 apply zenon_H134. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L13_ *) % 0.85/1.03 assert (zenon_L14_ : (~((c_tptpcol_14_72792) = (c_tptpcol_14_72792))) -> False). % 0.85/1.03 do 0 intro. intros zenon_Hdb. % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L14_ *) % 0.85/1.03 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_16_72795) (c_tptpcol_14_72792))) -> False). % 0.85/1.03 do 0 intro. intros zenon_Hac zenon_H135. % 0.85/1.03 elim (classic ((~((c_tptpcol_16_72795) = (c_tptpcol_15_72793)))/\(~(genls (c_tptpcol_16_72795) (c_tptpcol_15_72793))))); [ zenon_intro zenon_H136 | zenon_intro zenon_H137 ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_H136). zenon_intro zenon_H139. zenon_intro zenon_H138. % 0.85/1.03 exact (zenon_H138 just62). % 0.85/1.03 cut ((genls (c_tptpcol_15_72793) (c_tptpcol_14_72792)) = (genls (c_tptpcol_16_72795) (c_tptpcol_14_72792))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_H135. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact just60. % 0.85/1.03 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 0.85/1.03 cut (((c_tptpcol_15_72793) = (c_tptpcol_16_72795))); [idtac | apply NNPP; zenon_intro zenon_H13a]. % 0.85/1.03 congruence. % 0.85/1.03 apply (zenon_notand_s _ _ zenon_H137); [ zenon_intro zenon_H13c | zenon_intro zenon_H13b ]. % 0.85/1.03 apply zenon_H13c. zenon_intro zenon_H13d. % 0.85/1.03 elim (classic ((c_tptpcol_16_72795) = (c_tptpcol_16_72795))); [ zenon_intro zenon_H13e | zenon_intro zenon_H13f ]. % 0.85/1.03 cut (((c_tptpcol_16_72795) = (c_tptpcol_16_72795)) = ((c_tptpcol_15_72793) = (c_tptpcol_16_72795))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_H13a. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact zenon_H13e. % 0.85/1.03 cut (((c_tptpcol_16_72795) = (c_tptpcol_16_72795))); [idtac | apply NNPP; zenon_intro zenon_H13f]. % 0.85/1.03 cut (((c_tptpcol_16_72795) = (c_tptpcol_15_72793))); [idtac | apply NNPP; zenon_intro zenon_H139]. % 0.85/1.03 congruence. % 0.85/1.03 exact (zenon_H139 zenon_H13d). % 0.85/1.03 apply zenon_H13f. apply refl_equal. % 0.85/1.03 apply zenon_H13f. apply refl_equal. % 0.85/1.03 apply zenon_H13b. zenon_intro just62. % 0.85/1.03 generalize (zenon_Hac (c_tptpcol_16_72795)). zenon_intro zenon_H140. % 0.85/1.03 generalize (zenon_H140 (c_tptpcol_15_72793)). zenon_intro zenon_H141. % 0.85/1.03 generalize (zenon_H141 (c_tptpcol_14_72792)). zenon_intro zenon_H142. % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H142); [ zenon_intro zenon_H138 | zenon_intro zenon_H143 ]. % 0.85/1.03 exact (zenon_H138 just62). % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H143); [ zenon_intro zenon_H145 | zenon_intro zenon_H144 ]. % 0.85/1.03 exact (zenon_H145 just60). % 0.85/1.03 exact (zenon_H135 zenon_H144). % 0.85/1.03 apply zenon_Hdb. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L15_ *) % 0.85/1.03 assert (zenon_L16_ : (~((c_tptpcol_13_22071) = (c_tptpcol_13_22071))) -> False). % 0.85/1.03 do 0 intro. intros zenon_H146. % 0.85/1.03 apply zenon_H146. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L16_ *) % 0.85/1.03 assert (zenon_L17_ : (~((c_tptpcol_12_22055) = (c_tptpcol_12_22055))) -> False). % 0.85/1.03 do 0 intro. intros zenon_H147. % 0.85/1.03 apply zenon_H147. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L17_ *) % 0.85/1.03 assert (zenon_L18_ : (~((c_tptpcol_11_22023) = (c_tptpcol_11_22023))) -> False). % 0.85/1.03 do 0 intro. intros zenon_H148. % 0.85/1.03 apply zenon_H148. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L18_ *) % 0.85/1.03 assert (zenon_L19_ : (~((c_tptpcol_10_22022) = (c_tptpcol_10_22022))) -> False). % 0.85/1.03 do 0 intro. intros zenon_H149. % 0.85/1.03 apply zenon_H149. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L19_ *) % 0.85/1.03 assert (zenon_L20_ : (~((c_tptpcol_9_22021) = (c_tptpcol_9_22021))) -> False). % 0.85/1.03 do 0 intro. intros zenon_H14a. % 0.85/1.03 apply zenon_H14a. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L20_ *) % 0.85/1.03 assert (zenon_L21_ : (~((c_tptpcol_8_22020) = (c_tptpcol_8_22020))) -> False). % 0.85/1.03 do 0 intro. intros zenon_H14b. % 0.85/1.03 apply zenon_H14b. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L21_ *) % 0.85/1.03 assert (zenon_L22_ : (~((c_tptpcol_7_21508) = (c_tptpcol_7_21508))) -> False). % 0.85/1.03 do 0 intro. intros zenon_H14c. % 0.85/1.03 apply zenon_H14c. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L22_ *) % 0.85/1.03 assert (zenon_L23_ : (~((c_tptpcol_6_20484) = (c_tptpcol_6_20484))) -> False). % 0.85/1.03 do 0 intro. intros zenon_H14d. % 0.85/1.03 apply zenon_H14d. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L23_ *) % 0.85/1.03 assert (zenon_L24_ : (~((c_tptpcol_5_20483) = (c_tptpcol_5_20483))) -> False). % 0.85/1.03 do 0 intro. intros zenon_H14e. % 0.85/1.03 apply zenon_H14e. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L24_ *) % 0.85/1.03 assert (zenon_L25_ : (~((c_tptpcol_4_16387) = (c_tptpcol_4_16387))) -> False). % 0.85/1.03 do 0 intro. intros zenon_H14f. % 0.85/1.03 apply zenon_H14f. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L25_ *) % 0.85/1.03 assert (zenon_L26_ : (~((c_tptpcol_3_16386) = (c_tptpcol_3_16386))) -> False). % 0.85/1.03 do 0 intro. intros zenon_H150. % 0.85/1.03 apply zenon_H150. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L26_ *) % 0.85/1.03 assert (zenon_L27_ : (~((c_tptpcol_2_2) = (c_tptpcol_2_2))) -> False). % 0.85/1.03 do 0 intro. intros zenon_H151. % 0.85/1.03 apply zenon_H151. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L27_ *) % 0.85/1.03 assert (zenon_L28_ : (~((c_tptpcol_1_1) = (c_tptpcol_1_1))) -> False). % 0.85/1.03 do 0 intro. intros zenon_H152. % 0.85/1.03 apply zenon_H152. apply refl_equal. % 0.85/1.03 (* end of lemma zenon_L28_ *) % 0.85/1.03 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_15_22076) (c_tptpcol_16_72795))) -> (disjointwith (c_tptpcol_1_1) (c_tptpcol_16_72795)) -> False). % 0.85/1.03 do 0 intro. intros zenon_Hac zenon_H153 zenon_H154 zenon_H155. % 0.85/1.03 generalize (zenon_H153 (c_tptpcol_16_72795)). zenon_intro zenon_H156. % 0.85/1.03 generalize (zenon_H156 (c_tptpcol_15_22076)). zenon_intro zenon_H157. % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H157); [ zenon_intro zenon_H159 | zenon_intro zenon_H158 ]. % 0.85/1.03 apply (zenon_notand_s _ _ zenon_H159); [ zenon_intro zenon_H15b | zenon_intro zenon_H15a ]. % 0.85/1.03 exact (zenon_H15b zenon_H155). % 0.85/1.03 elim (classic ((~((c_tptpcol_15_22076) = (c_tptpcol_2_2)))/\(~(genls (c_tptpcol_15_22076) (c_tptpcol_2_2))))); [ zenon_intro zenon_H15c | zenon_intro zenon_H15d ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_H15c). zenon_intro zenon_H15f. zenon_intro zenon_H15e. % 0.85/1.03 elim (classic ((~((c_tptpcol_15_22076) = (c_tptpcol_3_16386)))/\(~(genls (c_tptpcol_15_22076) (c_tptpcol_3_16386))))); [ zenon_intro zenon_H160 | zenon_intro zenon_H161 ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_H160). zenon_intro zenon_H163. zenon_intro zenon_H162. % 0.85/1.03 elim (classic ((~((c_tptpcol_15_22076) = (c_tptpcol_4_16387)))/\(~(genls (c_tptpcol_15_22076) (c_tptpcol_4_16387))))); [ zenon_intro zenon_H164 | zenon_intro zenon_H165 ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_H164). zenon_intro zenon_H167. zenon_intro zenon_H166. % 0.85/1.03 elim (classic ((~((c_tptpcol_15_22076) = (c_tptpcol_5_20483)))/\(~(genls (c_tptpcol_15_22076) (c_tptpcol_5_20483))))); [ zenon_intro zenon_H168 | zenon_intro zenon_H169 ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_H168). zenon_intro zenon_H16b. zenon_intro zenon_H16a. % 0.85/1.03 elim (classic ((~((c_tptpcol_15_22076) = (c_tptpcol_6_20484)))/\(~(genls (c_tptpcol_15_22076) (c_tptpcol_6_20484))))); [ zenon_intro zenon_H16c | zenon_intro zenon_H16d ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_H16c). zenon_intro zenon_H16f. zenon_intro zenon_H16e. % 0.85/1.03 elim (classic ((~((c_tptpcol_15_22076) = (c_tptpcol_7_21508)))/\(~(genls (c_tptpcol_15_22076) (c_tptpcol_7_21508))))); [ zenon_intro zenon_H170 | zenon_intro zenon_H171 ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_H170). zenon_intro zenon_H173. zenon_intro zenon_H172. % 0.85/1.03 elim (classic ((~((c_tptpcol_15_22076) = (c_tptpcol_8_22020)))/\(~(genls (c_tptpcol_15_22076) (c_tptpcol_8_22020))))); [ zenon_intro zenon_H174 | zenon_intro zenon_H175 ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_H174). zenon_intro zenon_H177. zenon_intro zenon_H176. % 0.85/1.03 elim (classic ((~((c_tptpcol_15_22076) = (c_tptpcol_9_22021)))/\(~(genls (c_tptpcol_15_22076) (c_tptpcol_9_22021))))); [ zenon_intro zenon_H178 | zenon_intro zenon_H179 ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_H178). zenon_intro zenon_H17b. zenon_intro zenon_H17a. % 0.85/1.03 elim (classic ((~((c_tptpcol_15_22076) = (c_tptpcol_10_22022)))/\(~(genls (c_tptpcol_15_22076) (c_tptpcol_10_22022))))); [ zenon_intro zenon_H17c | zenon_intro zenon_H17d ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_H17c). zenon_intro zenon_H17f. zenon_intro zenon_H17e. % 0.85/1.03 elim (classic ((~((c_tptpcol_15_22076) = (c_tptpcol_11_22023)))/\(~(genls (c_tptpcol_15_22076) (c_tptpcol_11_22023))))); [ zenon_intro zenon_H180 | zenon_intro zenon_H181 ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_H180). zenon_intro zenon_H183. zenon_intro zenon_H182. % 0.85/1.03 elim (classic ((~((c_tptpcol_15_22076) = (c_tptpcol_12_22055)))/\(~(genls (c_tptpcol_15_22076) (c_tptpcol_12_22055))))); [ zenon_intro zenon_H184 | zenon_intro zenon_H185 ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_H184). zenon_intro zenon_H187. zenon_intro zenon_H186. % 0.85/1.03 elim (classic ((~((c_tptpcol_15_22076) = (c_tptpcol_13_22071)))/\(~(genls (c_tptpcol_15_22076) (c_tptpcol_13_22071))))); [ zenon_intro zenon_H188 | zenon_intro zenon_H189 ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_H188). zenon_intro zenon_H18b. zenon_intro zenon_H18a. % 0.85/1.03 elim (classic ((~((c_tptpcol_15_22076) = (c_tptpcol_14_22072)))/\(~(genls (c_tptpcol_15_22076) (c_tptpcol_14_22072))))); [ zenon_intro zenon_H18c | zenon_intro zenon_H18d ]. % 0.85/1.03 apply (zenon_and_s _ _ zenon_H18c). zenon_intro zenon_H18f. zenon_intro zenon_H18e. % 0.85/1.03 exact (zenon_H18e just32). % 0.85/1.03 cut ((genls (c_tptpcol_14_22072) (c_tptpcol_13_22071)) = (genls (c_tptpcol_15_22076) (c_tptpcol_13_22071))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_H18a. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact just30. % 0.85/1.03 cut (((c_tptpcol_13_22071) = (c_tptpcol_13_22071))); [idtac | apply NNPP; zenon_intro zenon_H146]. % 0.85/1.03 cut (((c_tptpcol_14_22072) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H190]. % 0.85/1.03 congruence. % 0.85/1.03 apply (zenon_notand_s _ _ zenon_H18d); [ zenon_intro zenon_H192 | zenon_intro zenon_H191 ]. % 0.85/1.03 apply zenon_H192. zenon_intro zenon_H193. % 0.85/1.03 elim (classic ((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [ zenon_intro zenon_H194 | zenon_intro zenon_H195 ]. % 0.85/1.03 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076)) = ((c_tptpcol_14_22072) = (c_tptpcol_15_22076))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_H190. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact zenon_H194. % 0.85/1.03 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H195]. % 0.85/1.03 cut (((c_tptpcol_15_22076) = (c_tptpcol_14_22072))); [idtac | apply NNPP; zenon_intro zenon_H18f]. % 0.85/1.03 congruence. % 0.85/1.03 exact (zenon_H18f zenon_H193). % 0.85/1.03 apply zenon_H195. apply refl_equal. % 0.85/1.03 apply zenon_H195. apply refl_equal. % 0.85/1.03 apply zenon_H191. zenon_intro just32. % 0.85/1.03 generalize (zenon_Hac (c_tptpcol_15_22076)). zenon_intro zenon_H196. % 0.85/1.03 generalize (zenon_H196 (c_tptpcol_14_22072)). zenon_intro zenon_H197. % 0.85/1.03 generalize (zenon_H197 (c_tptpcol_13_22071)). zenon_intro zenon_H198. % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H198); [ zenon_intro zenon_H18e | zenon_intro zenon_H199 ]. % 0.85/1.03 exact (zenon_H18e just32). % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H199); [ zenon_intro zenon_H19b | zenon_intro zenon_H19a ]. % 0.85/1.03 exact (zenon_H19b just30). % 0.85/1.03 exact (zenon_H18a zenon_H19a). % 0.85/1.03 apply zenon_H146. apply refl_equal. % 0.85/1.03 cut ((genls (c_tptpcol_13_22071) (c_tptpcol_12_22055)) = (genls (c_tptpcol_15_22076) (c_tptpcol_12_22055))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_H186. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact just28. % 0.85/1.03 cut (((c_tptpcol_12_22055) = (c_tptpcol_12_22055))); [idtac | apply NNPP; zenon_intro zenon_H147]. % 0.85/1.03 cut (((c_tptpcol_13_22071) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H19c]. % 0.85/1.03 congruence. % 0.85/1.03 apply (zenon_notand_s _ _ zenon_H189); [ zenon_intro zenon_H19e | zenon_intro zenon_H19d ]. % 0.85/1.03 apply zenon_H19e. zenon_intro zenon_H19f. % 0.85/1.03 elim (classic ((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [ zenon_intro zenon_H194 | zenon_intro zenon_H195 ]. % 0.85/1.03 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076)) = ((c_tptpcol_13_22071) = (c_tptpcol_15_22076))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_H19c. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact zenon_H194. % 0.85/1.03 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H195]. % 0.85/1.03 cut (((c_tptpcol_15_22076) = (c_tptpcol_13_22071))); [idtac | apply NNPP; zenon_intro zenon_H18b]. % 0.85/1.03 congruence. % 0.85/1.03 exact (zenon_H18b zenon_H19f). % 0.85/1.03 apply zenon_H195. apply refl_equal. % 0.85/1.03 apply zenon_H195. apply refl_equal. % 0.85/1.03 apply zenon_H19d. zenon_intro zenon_H19a. % 0.85/1.03 generalize (zenon_Hac (c_tptpcol_15_22076)). zenon_intro zenon_H196. % 0.85/1.03 generalize (zenon_H196 (c_tptpcol_13_22071)). zenon_intro zenon_H1a0. % 0.85/1.03 generalize (zenon_H1a0 (c_tptpcol_12_22055)). zenon_intro zenon_H1a1. % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H1a1); [ zenon_intro zenon_H18a | zenon_intro zenon_H1a2 ]. % 0.85/1.03 exact (zenon_H18a zenon_H19a). % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H1a2); [ zenon_intro zenon_H1a4 | zenon_intro zenon_H1a3 ]. % 0.85/1.03 exact (zenon_H1a4 just28). % 0.85/1.03 exact (zenon_H186 zenon_H1a3). % 0.85/1.03 apply zenon_H147. apply refl_equal. % 0.85/1.03 cut ((genls (c_tptpcol_12_22055) (c_tptpcol_11_22023)) = (genls (c_tptpcol_15_22076) (c_tptpcol_11_22023))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_H182. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact just26. % 0.85/1.03 cut (((c_tptpcol_11_22023) = (c_tptpcol_11_22023))); [idtac | apply NNPP; zenon_intro zenon_H148]. % 0.85/1.03 cut (((c_tptpcol_12_22055) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H1a5]. % 0.85/1.03 congruence. % 0.85/1.03 apply (zenon_notand_s _ _ zenon_H185); [ zenon_intro zenon_H1a7 | zenon_intro zenon_H1a6 ]. % 0.85/1.03 apply zenon_H1a7. zenon_intro zenon_H1a8. % 0.85/1.03 elim (classic ((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [ zenon_intro zenon_H194 | zenon_intro zenon_H195 ]. % 0.85/1.03 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076)) = ((c_tptpcol_12_22055) = (c_tptpcol_15_22076))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_H1a5. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact zenon_H194. % 0.85/1.03 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H195]. % 0.85/1.03 cut (((c_tptpcol_15_22076) = (c_tptpcol_12_22055))); [idtac | apply NNPP; zenon_intro zenon_H187]. % 0.85/1.03 congruence. % 0.85/1.03 exact (zenon_H187 zenon_H1a8). % 0.85/1.03 apply zenon_H195. apply refl_equal. % 0.85/1.03 apply zenon_H195. apply refl_equal. % 0.85/1.03 apply zenon_H1a6. zenon_intro zenon_H1a3. % 0.85/1.03 generalize (zenon_Hac (c_tptpcol_15_22076)). zenon_intro zenon_H196. % 0.85/1.03 generalize (zenon_H196 (c_tptpcol_12_22055)). zenon_intro zenon_H1a9. % 0.85/1.03 generalize (zenon_H1a9 (c_tptpcol_11_22023)). zenon_intro zenon_H1aa. % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H1aa); [ zenon_intro zenon_H186 | zenon_intro zenon_H1ab ]. % 0.85/1.03 exact (zenon_H186 zenon_H1a3). % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H1ab); [ zenon_intro zenon_H1ad | zenon_intro zenon_H1ac ]. % 0.85/1.03 exact (zenon_H1ad just26). % 0.85/1.03 exact (zenon_H182 zenon_H1ac). % 0.85/1.03 apply zenon_H148. apply refl_equal. % 0.85/1.03 cut ((genls (c_tptpcol_11_22023) (c_tptpcol_10_22022)) = (genls (c_tptpcol_15_22076) (c_tptpcol_10_22022))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_H17e. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact just24. % 0.85/1.03 cut (((c_tptpcol_10_22022) = (c_tptpcol_10_22022))); [idtac | apply NNPP; zenon_intro zenon_H149]. % 0.85/1.03 cut (((c_tptpcol_11_22023) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H1ae]. % 0.85/1.03 congruence. % 0.85/1.03 apply (zenon_notand_s _ _ zenon_H181); [ zenon_intro zenon_H1b0 | zenon_intro zenon_H1af ]. % 0.85/1.03 apply zenon_H1b0. zenon_intro zenon_H1b1. % 0.85/1.03 elim (classic ((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [ zenon_intro zenon_H194 | zenon_intro zenon_H195 ]. % 0.85/1.03 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076)) = ((c_tptpcol_11_22023) = (c_tptpcol_15_22076))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_H1ae. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact zenon_H194. % 0.85/1.03 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H195]. % 0.85/1.03 cut (((c_tptpcol_15_22076) = (c_tptpcol_11_22023))); [idtac | apply NNPP; zenon_intro zenon_H183]. % 0.85/1.03 congruence. % 0.85/1.03 exact (zenon_H183 zenon_H1b1). % 0.85/1.03 apply zenon_H195. apply refl_equal. % 0.85/1.03 apply zenon_H195. apply refl_equal. % 0.85/1.03 apply zenon_H1af. zenon_intro zenon_H1ac. % 0.85/1.03 generalize (zenon_Hac (c_tptpcol_15_22076)). zenon_intro zenon_H196. % 0.85/1.03 generalize (zenon_H196 (c_tptpcol_11_22023)). zenon_intro zenon_H1b2. % 0.85/1.03 generalize (zenon_H1b2 (c_tptpcol_10_22022)). zenon_intro zenon_H1b3. % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H1b3); [ zenon_intro zenon_H182 | zenon_intro zenon_H1b4 ]. % 0.85/1.03 exact (zenon_H182 zenon_H1ac). % 0.85/1.03 apply (zenon_imply_s _ _ zenon_H1b4); [ zenon_intro zenon_H1b6 | zenon_intro zenon_H1b5 ]. % 0.85/1.03 exact (zenon_H1b6 just24). % 0.85/1.03 exact (zenon_H17e zenon_H1b5). % 0.85/1.03 apply zenon_H149. apply refl_equal. % 0.85/1.03 cut ((genls (c_tptpcol_10_22022) (c_tptpcol_9_22021)) = (genls (c_tptpcol_15_22076) (c_tptpcol_9_22021))). % 0.85/1.03 intro zenon_D_pnotp. % 0.85/1.03 apply zenon_H17a. % 0.85/1.03 rewrite <- zenon_D_pnotp. % 0.85/1.03 exact just22. % 0.85/1.03 cut (((c_tptpcol_9_22021) = (c_tptpcol_9_22021))); [idtac | apply NNPP; zenon_intro zenon_H14a]. % 0.85/1.03 cut (((c_tptpcol_10_22022) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H1b7]. % 0.85/1.03 congruence. % 0.85/1.03 apply (zenon_notand_s _ _ zenon_H17d); [ zenon_intro zenon_H1b9 | zenon_intro zenon_H1b8 ]. % 0.85/1.04 apply zenon_H1b9. zenon_intro zenon_H1ba. % 0.85/1.04 elim (classic ((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [ zenon_intro zenon_H194 | zenon_intro zenon_H195 ]. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076)) = ((c_tptpcol_10_22022) = (c_tptpcol_15_22076))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H1b7. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact zenon_H194. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H195]. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_10_22022))); [idtac | apply NNPP; zenon_intro zenon_H17f]. % 0.85/1.04 congruence. % 0.85/1.04 exact (zenon_H17f zenon_H1ba). % 0.85/1.04 apply zenon_H195. apply refl_equal. % 0.85/1.04 apply zenon_H195. apply refl_equal. % 0.85/1.04 apply zenon_H1b8. zenon_intro zenon_H1b5. % 0.85/1.04 generalize (zenon_Hac (c_tptpcol_15_22076)). zenon_intro zenon_H196. % 0.85/1.04 generalize (zenon_H196 (c_tptpcol_10_22022)). zenon_intro zenon_H1bb. % 0.85/1.04 generalize (zenon_H1bb (c_tptpcol_9_22021)). zenon_intro zenon_H1bc. % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H1bc); [ zenon_intro zenon_H17e | zenon_intro zenon_H1bd ]. % 0.85/1.04 exact (zenon_H17e zenon_H1b5). % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H1bd); [ zenon_intro zenon_H1bf | zenon_intro zenon_H1be ]. % 0.85/1.04 exact (zenon_H1bf just22). % 0.85/1.04 exact (zenon_H17a zenon_H1be). % 0.85/1.04 apply zenon_H14a. apply refl_equal. % 0.85/1.04 cut ((genls (c_tptpcol_9_22021) (c_tptpcol_8_22020)) = (genls (c_tptpcol_15_22076) (c_tptpcol_8_22020))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H176. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact just20. % 0.85/1.04 cut (((c_tptpcol_8_22020) = (c_tptpcol_8_22020))); [idtac | apply NNPP; zenon_intro zenon_H14b]. % 0.85/1.04 cut (((c_tptpcol_9_22021) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H1c0]. % 0.85/1.04 congruence. % 0.85/1.04 apply (zenon_notand_s _ _ zenon_H179); [ zenon_intro zenon_H1c2 | zenon_intro zenon_H1c1 ]. % 0.85/1.04 apply zenon_H1c2. zenon_intro zenon_H1c3. % 0.85/1.04 elim (classic ((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [ zenon_intro zenon_H194 | zenon_intro zenon_H195 ]. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076)) = ((c_tptpcol_9_22021) = (c_tptpcol_15_22076))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H1c0. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact zenon_H194. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H195]. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_9_22021))); [idtac | apply NNPP; zenon_intro zenon_H17b]. % 0.85/1.04 congruence. % 0.85/1.04 exact (zenon_H17b zenon_H1c3). % 0.85/1.04 apply zenon_H195. apply refl_equal. % 0.85/1.04 apply zenon_H195. apply refl_equal. % 0.85/1.04 apply zenon_H1c1. zenon_intro zenon_H1be. % 0.85/1.04 generalize (zenon_Hac (c_tptpcol_15_22076)). zenon_intro zenon_H196. % 0.85/1.04 generalize (zenon_H196 (c_tptpcol_9_22021)). zenon_intro zenon_H1c4. % 0.85/1.04 generalize (zenon_H1c4 (c_tptpcol_8_22020)). zenon_intro zenon_H1c5. % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H1c5); [ zenon_intro zenon_H17a | zenon_intro zenon_H1c6 ]. % 0.85/1.04 exact (zenon_H17a zenon_H1be). % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H1c6); [ zenon_intro zenon_H1c8 | zenon_intro zenon_H1c7 ]. % 0.85/1.04 exact (zenon_H1c8 just20). % 0.85/1.04 exact (zenon_H176 zenon_H1c7). % 0.85/1.04 apply zenon_H14b. apply refl_equal. % 0.85/1.04 cut ((genls (c_tptpcol_8_22020) (c_tptpcol_7_21508)) = (genls (c_tptpcol_15_22076) (c_tptpcol_7_21508))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H172. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact just18. % 0.85/1.04 cut (((c_tptpcol_7_21508) = (c_tptpcol_7_21508))); [idtac | apply NNPP; zenon_intro zenon_H14c]. % 0.85/1.04 cut (((c_tptpcol_8_22020) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H1c9]. % 0.85/1.04 congruence. % 0.85/1.04 apply (zenon_notand_s _ _ zenon_H175); [ zenon_intro zenon_H1cb | zenon_intro zenon_H1ca ]. % 0.85/1.04 apply zenon_H1cb. zenon_intro zenon_H1cc. % 0.85/1.04 elim (classic ((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [ zenon_intro zenon_H194 | zenon_intro zenon_H195 ]. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076)) = ((c_tptpcol_8_22020) = (c_tptpcol_15_22076))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H1c9. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact zenon_H194. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H195]. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_8_22020))); [idtac | apply NNPP; zenon_intro zenon_H177]. % 0.85/1.04 congruence. % 0.85/1.04 exact (zenon_H177 zenon_H1cc). % 0.85/1.04 apply zenon_H195. apply refl_equal. % 0.85/1.04 apply zenon_H195. apply refl_equal. % 0.85/1.04 apply zenon_H1ca. zenon_intro zenon_H1c7. % 0.85/1.04 generalize (zenon_Hac (c_tptpcol_15_22076)). zenon_intro zenon_H196. % 0.85/1.04 generalize (zenon_H196 (c_tptpcol_8_22020)). zenon_intro zenon_H1cd. % 0.85/1.04 generalize (zenon_H1cd (c_tptpcol_7_21508)). zenon_intro zenon_H1ce. % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H1ce); [ zenon_intro zenon_H176 | zenon_intro zenon_H1cf ]. % 0.85/1.04 exact (zenon_H176 zenon_H1c7). % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H1cf); [ zenon_intro zenon_H1d1 | zenon_intro zenon_H1d0 ]. % 0.85/1.04 exact (zenon_H1d1 just18). % 0.85/1.04 exact (zenon_H172 zenon_H1d0). % 0.85/1.04 apply zenon_H14c. apply refl_equal. % 0.85/1.04 cut ((genls (c_tptpcol_7_21508) (c_tptpcol_6_20484)) = (genls (c_tptpcol_15_22076) (c_tptpcol_6_20484))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H16e. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact just16. % 0.85/1.04 cut (((c_tptpcol_6_20484) = (c_tptpcol_6_20484))); [idtac | apply NNPP; zenon_intro zenon_H14d]. % 0.85/1.04 cut (((c_tptpcol_7_21508) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H1d2]. % 0.85/1.04 congruence. % 0.85/1.04 apply (zenon_notand_s _ _ zenon_H171); [ zenon_intro zenon_H1d4 | zenon_intro zenon_H1d3 ]. % 0.85/1.04 apply zenon_H1d4. zenon_intro zenon_H1d5. % 0.85/1.04 elim (classic ((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [ zenon_intro zenon_H194 | zenon_intro zenon_H195 ]. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076)) = ((c_tptpcol_7_21508) = (c_tptpcol_15_22076))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H1d2. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact zenon_H194. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H195]. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_7_21508))); [idtac | apply NNPP; zenon_intro zenon_H173]. % 0.85/1.04 congruence. % 0.85/1.04 exact (zenon_H173 zenon_H1d5). % 0.85/1.04 apply zenon_H195. apply refl_equal. % 0.85/1.04 apply zenon_H195. apply refl_equal. % 0.85/1.04 apply zenon_H1d3. zenon_intro zenon_H1d0. % 0.85/1.04 generalize (zenon_Hac (c_tptpcol_15_22076)). zenon_intro zenon_H196. % 0.85/1.04 generalize (zenon_H196 (c_tptpcol_7_21508)). zenon_intro zenon_H1d6. % 0.85/1.04 generalize (zenon_H1d6 (c_tptpcol_6_20484)). zenon_intro zenon_H1d7. % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H1d7); [ zenon_intro zenon_H172 | zenon_intro zenon_H1d8 ]. % 0.85/1.04 exact (zenon_H172 zenon_H1d0). % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H1d8); [ zenon_intro zenon_H1da | zenon_intro zenon_H1d9 ]. % 0.85/1.04 exact (zenon_H1da just16). % 0.85/1.04 exact (zenon_H16e zenon_H1d9). % 0.85/1.04 apply zenon_H14d. apply refl_equal. % 0.85/1.04 cut ((genls (c_tptpcol_6_20484) (c_tptpcol_5_20483)) = (genls (c_tptpcol_15_22076) (c_tptpcol_5_20483))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H16a. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact just14. % 0.85/1.04 cut (((c_tptpcol_5_20483) = (c_tptpcol_5_20483))); [idtac | apply NNPP; zenon_intro zenon_H14e]. % 0.85/1.04 cut (((c_tptpcol_6_20484) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H1db]. % 0.85/1.04 congruence. % 0.85/1.04 apply (zenon_notand_s _ _ zenon_H16d); [ zenon_intro zenon_H1dd | zenon_intro zenon_H1dc ]. % 0.85/1.04 apply zenon_H1dd. zenon_intro zenon_H1de. % 0.85/1.04 elim (classic ((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [ zenon_intro zenon_H194 | zenon_intro zenon_H195 ]. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076)) = ((c_tptpcol_6_20484) = (c_tptpcol_15_22076))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H1db. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact zenon_H194. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H195]. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_6_20484))); [idtac | apply NNPP; zenon_intro zenon_H16f]. % 0.85/1.04 congruence. % 0.85/1.04 exact (zenon_H16f zenon_H1de). % 0.85/1.04 apply zenon_H195. apply refl_equal. % 0.85/1.04 apply zenon_H195. apply refl_equal. % 0.85/1.04 apply zenon_H1dc. zenon_intro zenon_H1d9. % 0.85/1.04 generalize (zenon_Hac (c_tptpcol_15_22076)). zenon_intro zenon_H196. % 0.85/1.04 generalize (zenon_H196 (c_tptpcol_6_20484)). zenon_intro zenon_H1df. % 0.85/1.04 generalize (zenon_H1df (c_tptpcol_5_20483)). zenon_intro zenon_H1e0. % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H1e0); [ zenon_intro zenon_H16e | zenon_intro zenon_H1e1 ]. % 0.85/1.04 exact (zenon_H16e zenon_H1d9). % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H1e1); [ zenon_intro zenon_H1e3 | zenon_intro zenon_H1e2 ]. % 0.85/1.04 exact (zenon_H1e3 just14). % 0.85/1.04 exact (zenon_H16a zenon_H1e2). % 0.85/1.04 apply zenon_H14e. apply refl_equal. % 0.85/1.04 cut ((genls (c_tptpcol_5_20483) (c_tptpcol_4_16387)) = (genls (c_tptpcol_15_22076) (c_tptpcol_4_16387))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H166. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact just12. % 0.85/1.04 cut (((c_tptpcol_4_16387) = (c_tptpcol_4_16387))); [idtac | apply NNPP; zenon_intro zenon_H14f]. % 0.85/1.04 cut (((c_tptpcol_5_20483) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H1e4]. % 0.85/1.04 congruence. % 0.85/1.04 apply (zenon_notand_s _ _ zenon_H169); [ zenon_intro zenon_H1e6 | zenon_intro zenon_H1e5 ]. % 0.85/1.04 apply zenon_H1e6. zenon_intro zenon_H1e7. % 0.85/1.04 elim (classic ((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [ zenon_intro zenon_H194 | zenon_intro zenon_H195 ]. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076)) = ((c_tptpcol_5_20483) = (c_tptpcol_15_22076))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H1e4. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact zenon_H194. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H195]. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_5_20483))); [idtac | apply NNPP; zenon_intro zenon_H16b]. % 0.85/1.04 congruence. % 0.85/1.04 exact (zenon_H16b zenon_H1e7). % 0.85/1.04 apply zenon_H195. apply refl_equal. % 0.85/1.04 apply zenon_H195. apply refl_equal. % 0.85/1.04 apply zenon_H1e5. zenon_intro zenon_H1e2. % 0.85/1.04 generalize (zenon_Hac (c_tptpcol_15_22076)). zenon_intro zenon_H196. % 0.85/1.04 generalize (zenon_H196 (c_tptpcol_5_20483)). zenon_intro zenon_H1e8. % 0.85/1.04 generalize (zenon_H1e8 (c_tptpcol_4_16387)). zenon_intro zenon_H1e9. % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H1e9); [ zenon_intro zenon_H16a | zenon_intro zenon_H1ea ]. % 0.85/1.04 exact (zenon_H16a zenon_H1e2). % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H1ea); [ zenon_intro zenon_H1ec | zenon_intro zenon_H1eb ]. % 0.85/1.04 exact (zenon_H1ec just12). % 0.85/1.04 exact (zenon_H166 zenon_H1eb). % 0.85/1.04 apply zenon_H14f. apply refl_equal. % 0.85/1.04 cut ((genls (c_tptpcol_4_16387) (c_tptpcol_3_16386)) = (genls (c_tptpcol_15_22076) (c_tptpcol_3_16386))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H162. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact just10. % 0.85/1.04 cut (((c_tptpcol_3_16386) = (c_tptpcol_3_16386))); [idtac | apply NNPP; zenon_intro zenon_H150]. % 0.85/1.04 cut (((c_tptpcol_4_16387) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H1ed]. % 0.85/1.04 congruence. % 0.85/1.04 apply (zenon_notand_s _ _ zenon_H165); [ zenon_intro zenon_H1ef | zenon_intro zenon_H1ee ]. % 0.85/1.04 apply zenon_H1ef. zenon_intro zenon_H1f0. % 0.85/1.04 elim (classic ((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [ zenon_intro zenon_H194 | zenon_intro zenon_H195 ]. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076)) = ((c_tptpcol_4_16387) = (c_tptpcol_15_22076))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H1ed. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact zenon_H194. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H195]. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_4_16387))); [idtac | apply NNPP; zenon_intro zenon_H167]. % 0.85/1.04 congruence. % 0.85/1.04 exact (zenon_H167 zenon_H1f0). % 0.85/1.04 apply zenon_H195. apply refl_equal. % 0.85/1.04 apply zenon_H195. apply refl_equal. % 0.85/1.04 apply zenon_H1ee. zenon_intro zenon_H1eb. % 0.85/1.04 generalize (zenon_Hac (c_tptpcol_15_22076)). zenon_intro zenon_H196. % 0.85/1.04 generalize (zenon_H196 (c_tptpcol_4_16387)). zenon_intro zenon_H1f1. % 0.85/1.04 generalize (zenon_H1f1 (c_tptpcol_3_16386)). zenon_intro zenon_H1f2. % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H1f2); [ zenon_intro zenon_H166 | zenon_intro zenon_H1f3 ]. % 0.85/1.04 exact (zenon_H166 zenon_H1eb). % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H1f3); [ zenon_intro zenon_H1f5 | zenon_intro zenon_H1f4 ]. % 0.85/1.04 exact (zenon_H1f5 just10). % 0.85/1.04 exact (zenon_H162 zenon_H1f4). % 0.85/1.04 apply zenon_H150. apply refl_equal. % 0.85/1.04 cut ((genls (c_tptpcol_3_16386) (c_tptpcol_2_2)) = (genls (c_tptpcol_15_22076) (c_tptpcol_2_2))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H15e. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact just8. % 0.85/1.04 cut (((c_tptpcol_2_2) = (c_tptpcol_2_2))); [idtac | apply NNPP; zenon_intro zenon_H151]. % 0.85/1.04 cut (((c_tptpcol_3_16386) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H1f6]. % 0.85/1.04 congruence. % 0.85/1.04 apply (zenon_notand_s _ _ zenon_H161); [ zenon_intro zenon_H1f8 | zenon_intro zenon_H1f7 ]. % 0.85/1.04 apply zenon_H1f8. zenon_intro zenon_H1f9. % 0.85/1.04 elim (classic ((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [ zenon_intro zenon_H194 | zenon_intro zenon_H195 ]. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076)) = ((c_tptpcol_3_16386) = (c_tptpcol_15_22076))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H1f6. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact zenon_H194. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H195]. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_3_16386))); [idtac | apply NNPP; zenon_intro zenon_H163]. % 0.85/1.04 congruence. % 0.85/1.04 exact (zenon_H163 zenon_H1f9). % 0.85/1.04 apply zenon_H195. apply refl_equal. % 0.85/1.04 apply zenon_H195. apply refl_equal. % 0.85/1.04 apply zenon_H1f7. zenon_intro zenon_H1f4. % 0.85/1.04 generalize (zenon_Hac (c_tptpcol_15_22076)). zenon_intro zenon_H196. % 0.85/1.04 generalize (zenon_H196 (c_tptpcol_3_16386)). zenon_intro zenon_H1fa. % 0.85/1.04 generalize (zenon_H1fa (c_tptpcol_2_2)). zenon_intro zenon_H1fb. % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H1fb); [ zenon_intro zenon_H162 | zenon_intro zenon_H1fc ]. % 0.85/1.04 exact (zenon_H162 zenon_H1f4). % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H1fc); [ zenon_intro zenon_H1fe | zenon_intro zenon_H1fd ]. % 0.85/1.04 exact (zenon_H1fe just8). % 0.85/1.04 exact (zenon_H15e zenon_H1fd). % 0.85/1.04 apply zenon_H151. apply refl_equal. % 0.85/1.04 cut ((genls (c_tptpcol_2_2) (c_tptpcol_1_1)) = (genls (c_tptpcol_15_22076) (c_tptpcol_1_1))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H15a. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact just6. % 0.85/1.04 cut (((c_tptpcol_1_1) = (c_tptpcol_1_1))); [idtac | apply NNPP; zenon_intro zenon_H152]. % 0.85/1.04 cut (((c_tptpcol_2_2) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H1ff]. % 0.85/1.04 congruence. % 0.85/1.04 apply (zenon_notand_s _ _ zenon_H15d); [ zenon_intro zenon_H201 | zenon_intro zenon_H200 ]. % 0.85/1.04 apply zenon_H201. zenon_intro zenon_H202. % 0.85/1.04 elim (classic ((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [ zenon_intro zenon_H194 | zenon_intro zenon_H195 ]. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076)) = ((c_tptpcol_2_2) = (c_tptpcol_15_22076))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H1ff. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact zenon_H194. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_15_22076))); [idtac | apply NNPP; zenon_intro zenon_H195]. % 0.85/1.04 cut (((c_tptpcol_15_22076) = (c_tptpcol_2_2))); [idtac | apply NNPP; zenon_intro zenon_H15f]. % 0.85/1.04 congruence. % 0.85/1.04 exact (zenon_H15f zenon_H202). % 0.85/1.04 apply zenon_H195. apply refl_equal. % 0.85/1.04 apply zenon_H195. apply refl_equal. % 0.85/1.04 apply zenon_H200. zenon_intro zenon_H1fd. % 0.85/1.04 generalize (zenon_Hac (c_tptpcol_15_22076)). zenon_intro zenon_H196. % 0.85/1.04 generalize (zenon_H196 (c_tptpcol_2_2)). zenon_intro zenon_H203. % 0.85/1.04 generalize (zenon_H203 (c_tptpcol_1_1)). zenon_intro zenon_H204. % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H204); [ zenon_intro zenon_H15e | zenon_intro zenon_H205 ]. % 0.85/1.04 exact (zenon_H15e zenon_H1fd). % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H205); [ zenon_intro zenon_H207 | zenon_intro zenon_H206 ]. % 0.85/1.04 exact (zenon_H207 just6). % 0.85/1.04 exact (zenon_H15a zenon_H206). % 0.85/1.04 apply zenon_H152. apply refl_equal. % 0.85/1.04 exact (zenon_H154 zenon_H158). % 0.85/1.04 (* end of lemma zenon_L29_ *) % 0.85/1.04 apply NNPP. intro zenon_G. % 0.85/1.04 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_Hac | zenon_intro zenon_H208 ]. % 0.85/1.04 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H209. zenon_intro zenon_H154. % 0.85/1.04 generalize (just85 (c_tptpcol_1_1)). zenon_intro zenon_H153. % 0.85/1.04 generalize (just84 (c_tptpcol_1_1)). zenon_intro zenon_H20a. % 0.85/1.04 generalize (zenon_H20a (c_tptpcol_14_72792)). zenon_intro zenon_H20b. % 0.85/1.04 generalize (zenon_H20a (c_tptpcol_1_65536)). zenon_intro zenon_H20c. % 0.85/1.04 generalize (zenon_H20b (c_tptpcol_16_72795)). zenon_intro zenon_H20d. % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H20d); [ zenon_intro zenon_H20e | zenon_intro zenon_H155 ]. % 0.85/1.04 apply (zenon_notand_s _ _ zenon_H20e); [ zenon_intro zenon_H20f | zenon_intro zenon_H135 ]. % 0.85/1.04 generalize (zenon_H20c (c_tptpcol_14_72792)). zenon_intro zenon_H210. % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H210); [ zenon_intro zenon_H212 | zenon_intro zenon_H211 ]. % 0.85/1.04 apply (zenon_notand_s _ _ zenon_H212); [ zenon_intro zenon_H214 | zenon_intro zenon_H213 ]. % 0.85/1.04 exact (zenon_H214 just64). % 0.85/1.04 elim (classic ((~((c_tptpcol_14_72792) = (c_tptpcol_2_65537)))/\(~(genls (c_tptpcol_14_72792) (c_tptpcol_2_65537))))); [ zenon_intro zenon_H215 | zenon_intro zenon_H216 ]. % 0.85/1.04 apply (zenon_and_s _ _ zenon_H215). zenon_intro zenon_H218. zenon_intro zenon_H217. % 0.85/1.04 elim (classic ((~((c_tptpcol_14_72792) = (c_tptpcol_3_65538)))/\(~(genls (c_tptpcol_14_72792) (c_tptpcol_3_65538))))); [ zenon_intro zenon_H219 | zenon_intro zenon_H21a ]. % 0.85/1.04 apply (zenon_and_s _ _ zenon_H219). zenon_intro zenon_H21b. zenon_intro zenon_Had. % 0.85/1.04 apply (zenon_L11_); trivial. % 0.85/1.04 cut ((genls (c_tptpcol_3_65538) (c_tptpcol_2_65537)) = (genls (c_tptpcol_14_72792) (c_tptpcol_2_65537))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H217. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact just36. % 0.85/1.04 cut (((c_tptpcol_2_65537) = (c_tptpcol_2_65537))); [idtac | apply NNPP; zenon_intro zenon_H133]. % 0.85/1.04 cut (((c_tptpcol_3_65538) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_H21c]. % 0.85/1.04 congruence. % 0.85/1.04 apply (zenon_notand_s _ _ zenon_H21a); [ zenon_intro zenon_H21e | zenon_intro zenon_H21d ]. % 0.85/1.04 apply zenon_H21e. zenon_intro zenon_H21f. % 0.85/1.04 elim (classic ((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 0.85/1.04 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792)) = ((c_tptpcol_3_65538) = (c_tptpcol_14_72792))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H21c. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact zenon_Hda. % 0.85/1.04 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 0.85/1.04 cut (((c_tptpcol_14_72792) = (c_tptpcol_3_65538))); [idtac | apply NNPP; zenon_intro zenon_H21b]. % 0.85/1.04 congruence. % 0.85/1.04 exact (zenon_H21b zenon_H21f). % 0.85/1.04 apply zenon_Hdb. apply refl_equal. % 0.85/1.04 apply zenon_Hdb. apply refl_equal. % 0.85/1.04 apply zenon_H21d. zenon_intro zenon_H131. % 0.85/1.04 generalize (zenon_Hac (c_tptpcol_14_72792)). zenon_intro zenon_Hdc. % 0.85/1.04 generalize (zenon_Hdc (c_tptpcol_3_65538)). zenon_intro zenon_H220. % 0.85/1.04 generalize (zenon_H220 (c_tptpcol_2_65537)). zenon_intro zenon_H221. % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H221); [ zenon_intro zenon_Had | zenon_intro zenon_H222 ]. % 0.85/1.04 exact (zenon_Had zenon_H131). % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H222); [ zenon_intro zenon_H224 | zenon_intro zenon_H223 ]. % 0.85/1.04 exact (zenon_H224 just36). % 0.85/1.04 exact (zenon_H217 zenon_H223). % 0.85/1.04 apply zenon_H133. apply refl_equal. % 0.85/1.04 cut ((genls (c_tptpcol_2_65537) (c_tptpcol_1_65536)) = (genls (c_tptpcol_14_72792) (c_tptpcol_1_65536))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H213. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact just34. % 0.85/1.04 cut (((c_tptpcol_1_65536) = (c_tptpcol_1_65536))); [idtac | apply NNPP; zenon_intro zenon_H134]. % 0.85/1.04 cut (((c_tptpcol_2_65537) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_H225]. % 0.85/1.04 congruence. % 0.85/1.04 apply (zenon_notand_s _ _ zenon_H216); [ zenon_intro zenon_H227 | zenon_intro zenon_H226 ]. % 0.85/1.04 apply zenon_H227. zenon_intro zenon_H228. % 0.85/1.04 elim (classic ((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [ zenon_intro zenon_Hda | zenon_intro zenon_Hdb ]. % 0.85/1.04 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792)) = ((c_tptpcol_2_65537) = (c_tptpcol_14_72792))). % 0.85/1.04 intro zenon_D_pnotp. % 0.85/1.04 apply zenon_H225. % 0.85/1.04 rewrite <- zenon_D_pnotp. % 0.85/1.04 exact zenon_Hda. % 0.85/1.04 cut (((c_tptpcol_14_72792) = (c_tptpcol_14_72792))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 0.85/1.04 cut (((c_tptpcol_14_72792) = (c_tptpcol_2_65537))); [idtac | apply NNPP; zenon_intro zenon_H218]. % 0.85/1.04 congruence. % 0.85/1.04 exact (zenon_H218 zenon_H228). % 0.85/1.04 apply zenon_Hdb. apply refl_equal. % 0.85/1.04 apply zenon_Hdb. apply refl_equal. % 0.85/1.04 apply zenon_H226. zenon_intro zenon_H223. % 0.85/1.04 generalize (zenon_Hac (c_tptpcol_14_72792)). zenon_intro zenon_Hdc. % 0.85/1.04 generalize (zenon_Hdc (c_tptpcol_2_65537)). zenon_intro zenon_H229. % 0.85/1.04 generalize (zenon_H229 (c_tptpcol_1_65536)). zenon_intro zenon_H22a. % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H22a); [ zenon_intro zenon_H217 | zenon_intro zenon_H22b ]. % 0.85/1.04 exact (zenon_H217 zenon_H223). % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H22b); [ zenon_intro zenon_H22d | zenon_intro zenon_H22c ]. % 0.85/1.04 exact (zenon_H22d just34). % 0.85/1.04 exact (zenon_H213 zenon_H22c). % 0.85/1.04 apply zenon_H134. apply refl_equal. % 0.85/1.04 exact (zenon_H20f zenon_H211). % 0.85/1.04 apply (zenon_L15_); trivial. % 0.85/1.04 apply (zenon_L29_); trivial. % 0.85/1.04 apply zenon_H208. zenon_intro zenon_Tx_vm. apply NNPP. zenon_intro zenon_H22f. % 0.85/1.04 apply zenon_H22f. zenon_intro zenon_Ty_vo. apply NNPP. zenon_intro zenon_H231. % 0.85/1.04 apply zenon_H231. zenon_intro zenon_Tz_vq. apply NNPP. zenon_intro zenon_H233. % 0.85/1.04 apply (zenon_notimply_s _ _ zenon_H233). zenon_intro zenon_H235. zenon_intro zenon_H234. % 0.85/1.04 apply (zenon_notimply_s _ _ zenon_H234). zenon_intro zenon_H237. zenon_intro zenon_H236. % 0.85/1.04 generalize (just152 zenon_Tx_vm). zenon_intro zenon_H238. % 0.85/1.04 generalize (zenon_H238 zenon_Ty_vo). zenon_intro zenon_H239. % 0.85/1.04 generalize (zenon_H239 zenon_Tz_vq). zenon_intro zenon_H23a. % 0.85/1.04 apply (zenon_imply_s _ _ zenon_H23a); [ zenon_intro zenon_H23c | zenon_intro zenon_H23b ]. % 0.85/1.04 apply (zenon_notand_s _ _ zenon_H23c); [ zenon_intro zenon_H23e | zenon_intro zenon_H23d ]. % 0.85/1.04 exact (zenon_H23e zenon_H235). % 0.85/1.04 exact (zenon_H23d zenon_H237). % 0.85/1.04 exact (zenon_H236 zenon_H23b). % 0.85/1.04 Qed. % 0.85/1.04 % SZS output end Proof % 0.85/1.04 (* END-PROOF *) % 0.85/1.04 nodes searched: 17132 % 0.85/1.04 max branch formulas: 6054 % 0.85/1.04 proof nodes created: 178 % 0.85/1.04 formulas created: 85010 % 0.85/1.04 %------------------------------------------------------------------------------