%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR061+1 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n026.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:22 EDT 2022 % Result : Theorem 0.43s 0.62s % Output : Proof 0.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : CSR061+1 : TPTP v8.1.0. Released v3.4.0. % 0.11/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n026.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Sat Jun 11 06:51:49 EDT 2022 % 0.12/0.33 % CPUTime : % 0.43/0.62 (* PROOF-FOUND *) % 0.43/0.62 % SZS status Theorem % 0.43/0.62 (* BEGIN-PROOF *) % 0.43/0.62 % SZS output start Proof % 0.43/0.62 Theorem query61 : ((mtvisible (c_timehasnoendmt))->(disjointwith (c_tptpcol_8_114177) (c_tptpcol_14_118118))). % 0.43/0.62 Proof. % 0.43/0.62 assert (zenon_L1_ : (~((c_tptpcol_6_116738) = (c_tptpcol_6_116738))) -> False). % 0.43/0.62 do 0 intro. intros zenon_H6b. % 0.43/0.62 apply zenon_H6b. apply refl_equal. % 0.43/0.62 (* end of lemma zenon_L1_ *) % 0.43/0.62 assert (zenon_L2_ : (~((c_tptpcol_5_114690) = (c_tptpcol_5_114690))) -> False). % 0.43/0.62 do 0 intro. intros zenon_H6c. % 0.43/0.62 apply zenon_H6c. apply refl_equal. % 0.43/0.62 (* end of lemma zenon_L2_ *) % 0.43/0.62 assert (zenon_L3_ : (~((c_tptpcol_4_114689) = (c_tptpcol_4_114689))) -> False). % 0.43/0.62 do 0 intro. intros zenon_H6d. % 0.43/0.62 apply zenon_H6d. apply refl_equal. % 0.43/0.62 (* end of lemma zenon_L3_ *) % 0.43/0.62 assert (zenon_L4_ : (~((c_tptpcol_3_114688) = (c_tptpcol_3_114688))) -> False). % 0.43/0.62 do 0 intro. intros zenon_H6e. % 0.43/0.62 apply zenon_H6e. apply refl_equal. % 0.43/0.62 (* end of lemma zenon_L4_ *) % 0.43/0.62 assert (zenon_L5_ : (~((c_tptpcol_12_118116) = (c_tptpcol_12_118116))) -> False). % 0.43/0.62 do 0 intro. intros zenon_H6f. % 0.43/0.62 apply zenon_H6f. apply refl_equal. % 0.43/0.62 (* end of lemma zenon_L5_ *) % 0.43/0.62 assert (zenon_L6_ : (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_118118) (c_tptpcol_12_118116))) -> False). % 0.43/0.62 do 0 intro. intros zenon_H70 zenon_H71. % 0.43/0.62 elim (classic ((~((c_tptpcol_14_118118) = (c_tptpcol_13_118117)))/\(~(genls (c_tptpcol_14_118118) (c_tptpcol_13_118117))))); [ zenon_intro zenon_H72 | zenon_intro zenon_H73 ]. % 0.43/0.62 apply (zenon_and_s _ _ zenon_H72). zenon_intro zenon_H75. zenon_intro zenon_H74. % 0.43/0.62 exact (zenon_H74 just35). % 0.43/0.62 cut ((genls (c_tptpcol_13_118117) (c_tptpcol_12_118116)) = (genls (c_tptpcol_14_118118) (c_tptpcol_12_118116))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_H71. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact just33. % 0.43/0.62 cut (((c_tptpcol_12_118116) = (c_tptpcol_12_118116))); [idtac | apply NNPP; zenon_intro zenon_H6f]. % 0.43/0.62 cut (((c_tptpcol_13_118117) = (c_tptpcol_14_118118))); [idtac | apply NNPP; zenon_intro zenon_H76]. % 0.43/0.62 congruence. % 0.43/0.62 apply (zenon_notand_s _ _ zenon_H73); [ zenon_intro zenon_H78 | zenon_intro zenon_H77 ]. % 0.43/0.62 apply zenon_H78. zenon_intro zenon_H79. % 0.43/0.62 elim (classic ((c_tptpcol_14_118118) = (c_tptpcol_14_118118))); [ zenon_intro zenon_H7a | zenon_intro zenon_H7b ]. % 0.43/0.62 cut (((c_tptpcol_14_118118) = (c_tptpcol_14_118118)) = ((c_tptpcol_13_118117) = (c_tptpcol_14_118118))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_H76. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact zenon_H7a. % 0.43/0.62 cut (((c_tptpcol_14_118118) = (c_tptpcol_14_118118))); [idtac | apply NNPP; zenon_intro zenon_H7b]. % 0.43/0.62 cut (((c_tptpcol_14_118118) = (c_tptpcol_13_118117))); [idtac | apply NNPP; zenon_intro zenon_H75]. % 0.43/0.62 congruence. % 0.43/0.62 exact (zenon_H75 zenon_H79). % 0.43/0.62 apply zenon_H7b. apply refl_equal. % 0.43/0.62 apply zenon_H7b. apply refl_equal. % 0.43/0.62 apply zenon_H77. zenon_intro just35. % 0.43/0.62 generalize (zenon_H70 (c_tptpcol_14_118118)). zenon_intro zenon_H7c. % 0.43/0.62 generalize (zenon_H7c (c_tptpcol_13_118117)). zenon_intro zenon_H7d. % 0.43/0.62 generalize (zenon_H7d (c_tptpcol_12_118116)). zenon_intro zenon_H7e. % 0.43/0.62 apply (zenon_imply_s _ _ zenon_H7e); [ zenon_intro zenon_H74 | zenon_intro zenon_H7f ]. % 0.43/0.62 exact (zenon_H74 just35). % 0.43/0.62 apply (zenon_imply_s _ _ zenon_H7f); [ zenon_intro zenon_H81 | zenon_intro zenon_H80 ]. % 0.43/0.62 exact (zenon_H81 just33). % 0.43/0.62 exact (zenon_H71 zenon_H80). % 0.43/0.62 apply zenon_H6f. apply refl_equal. % 0.43/0.62 (* end of lemma zenon_L6_ *) % 0.43/0.62 assert (zenon_L7_ : (~((c_tptpcol_11_118084) = (c_tptpcol_11_118084))) -> False). % 0.43/0.62 do 0 intro. intros zenon_H82. % 0.43/0.62 apply zenon_H82. apply refl_equal. % 0.43/0.62 (* end of lemma zenon_L7_ *) % 0.43/0.62 assert (zenon_L8_ : (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_118118) (c_tptpcol_11_118084))) -> False). % 0.43/0.62 do 0 intro. intros zenon_H70 zenon_H83. % 0.43/0.62 elim (classic ((~((c_tptpcol_14_118118) = (c_tptpcol_12_118116)))/\(~(genls (c_tptpcol_14_118118) (c_tptpcol_12_118116))))); [ zenon_intro zenon_H84 | zenon_intro zenon_H85 ]. % 0.43/0.62 apply (zenon_and_s _ _ zenon_H84). zenon_intro zenon_H86. zenon_intro zenon_H71. % 0.43/0.62 apply (zenon_L6_); trivial. % 0.43/0.62 cut ((genls (c_tptpcol_12_118116) (c_tptpcol_11_118084)) = (genls (c_tptpcol_14_118118) (c_tptpcol_11_118084))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_H83. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact just31. % 0.43/0.62 cut (((c_tptpcol_11_118084) = (c_tptpcol_11_118084))); [idtac | apply NNPP; zenon_intro zenon_H82]. % 0.43/0.62 cut (((c_tptpcol_12_118116) = (c_tptpcol_14_118118))); [idtac | apply NNPP; zenon_intro zenon_H87]. % 0.43/0.62 congruence. % 0.43/0.62 apply (zenon_notand_s _ _ zenon_H85); [ zenon_intro zenon_H89 | zenon_intro zenon_H88 ]. % 0.43/0.62 apply zenon_H89. zenon_intro zenon_H8a. % 0.43/0.62 elim (classic ((c_tptpcol_14_118118) = (c_tptpcol_14_118118))); [ zenon_intro zenon_H7a | zenon_intro zenon_H7b ]. % 0.43/0.62 cut (((c_tptpcol_14_118118) = (c_tptpcol_14_118118)) = ((c_tptpcol_12_118116) = (c_tptpcol_14_118118))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_H87. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact zenon_H7a. % 0.43/0.62 cut (((c_tptpcol_14_118118) = (c_tptpcol_14_118118))); [idtac | apply NNPP; zenon_intro zenon_H7b]. % 0.43/0.62 cut (((c_tptpcol_14_118118) = (c_tptpcol_12_118116))); [idtac | apply NNPP; zenon_intro zenon_H86]. % 0.43/0.62 congruence. % 0.43/0.62 exact (zenon_H86 zenon_H8a). % 0.43/0.62 apply zenon_H7b. apply refl_equal. % 0.43/0.62 apply zenon_H7b. apply refl_equal. % 0.43/0.62 apply zenon_H88. zenon_intro zenon_H80. % 0.43/0.62 generalize (zenon_H70 (c_tptpcol_14_118118)). zenon_intro zenon_H7c. % 0.43/0.62 generalize (zenon_H7c (c_tptpcol_12_118116)). zenon_intro zenon_H8b. % 0.43/0.62 generalize (zenon_H8b (c_tptpcol_11_118084)). zenon_intro zenon_H8c. % 0.43/0.62 apply (zenon_imply_s _ _ zenon_H8c); [ zenon_intro zenon_H71 | zenon_intro zenon_H8d ]. % 0.43/0.62 exact (zenon_H71 zenon_H80). % 0.43/0.62 apply (zenon_imply_s _ _ zenon_H8d); [ zenon_intro zenon_H8f | zenon_intro zenon_H8e ]. % 0.43/0.62 exact (zenon_H8f just31). % 0.43/0.62 exact (zenon_H83 zenon_H8e). % 0.43/0.62 apply zenon_H82. apply refl_equal. % 0.43/0.62 (* end of lemma zenon_L8_ *) % 0.43/0.62 assert (zenon_L9_ : (~((c_tptpcol_10_118020) = (c_tptpcol_10_118020))) -> False). % 0.43/0.62 do 0 intro. intros zenon_H90. % 0.43/0.62 apply zenon_H90. apply refl_equal. % 0.43/0.62 (* end of lemma zenon_L9_ *) % 0.43/0.62 assert (zenon_L10_ : (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_118118) (c_tptpcol_10_118020))) -> False). % 0.43/0.62 do 0 intro. intros zenon_H70 zenon_H91. % 0.43/0.62 elim (classic ((~((c_tptpcol_14_118118) = (c_tptpcol_11_118084)))/\(~(genls (c_tptpcol_14_118118) (c_tptpcol_11_118084))))); [ zenon_intro zenon_H92 | zenon_intro zenon_H93 ]. % 0.43/0.62 apply (zenon_and_s _ _ zenon_H92). zenon_intro zenon_H94. zenon_intro zenon_H83. % 0.43/0.62 apply (zenon_L8_); trivial. % 0.43/0.62 cut ((genls (c_tptpcol_11_118084) (c_tptpcol_10_118020)) = (genls (c_tptpcol_14_118118) (c_tptpcol_10_118020))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_H91. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact just29. % 0.43/0.62 cut (((c_tptpcol_10_118020) = (c_tptpcol_10_118020))); [idtac | apply NNPP; zenon_intro zenon_H90]. % 0.43/0.62 cut (((c_tptpcol_11_118084) = (c_tptpcol_14_118118))); [idtac | apply NNPP; zenon_intro zenon_H95]. % 0.43/0.62 congruence. % 0.43/0.62 apply (zenon_notand_s _ _ zenon_H93); [ zenon_intro zenon_H97 | zenon_intro zenon_H96 ]. % 0.43/0.62 apply zenon_H97. zenon_intro zenon_H98. % 0.43/0.62 elim (classic ((c_tptpcol_14_118118) = (c_tptpcol_14_118118))); [ zenon_intro zenon_H7a | zenon_intro zenon_H7b ]. % 0.43/0.62 cut (((c_tptpcol_14_118118) = (c_tptpcol_14_118118)) = ((c_tptpcol_11_118084) = (c_tptpcol_14_118118))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_H95. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact zenon_H7a. % 0.43/0.62 cut (((c_tptpcol_14_118118) = (c_tptpcol_14_118118))); [idtac | apply NNPP; zenon_intro zenon_H7b]. % 0.43/0.62 cut (((c_tptpcol_14_118118) = (c_tptpcol_11_118084))); [idtac | apply NNPP; zenon_intro zenon_H94]. % 0.43/0.62 congruence. % 0.43/0.62 exact (zenon_H94 zenon_H98). % 0.43/0.62 apply zenon_H7b. apply refl_equal. % 0.43/0.62 apply zenon_H7b. apply refl_equal. % 0.43/0.62 apply zenon_H96. zenon_intro zenon_H8e. % 0.43/0.62 generalize (zenon_H70 (c_tptpcol_14_118118)). zenon_intro zenon_H7c. % 0.43/0.62 generalize (zenon_H7c (c_tptpcol_11_118084)). zenon_intro zenon_H99. % 0.43/0.62 generalize (zenon_H99 (c_tptpcol_10_118020)). zenon_intro zenon_H9a. % 0.43/0.62 apply (zenon_imply_s _ _ zenon_H9a); [ zenon_intro zenon_H83 | zenon_intro zenon_H9b ]. % 0.43/0.62 exact (zenon_H83 zenon_H8e). % 0.43/0.62 apply (zenon_imply_s _ _ zenon_H9b); [ zenon_intro zenon_H9d | zenon_intro zenon_H9c ]. % 0.43/0.62 exact (zenon_H9d just29). % 0.43/0.62 exact (zenon_H91 zenon_H9c). % 0.43/0.62 apply zenon_H90. apply refl_equal. % 0.43/0.62 (* end of lemma zenon_L10_ *) % 0.43/0.62 assert (zenon_L11_ : (~((c_tptpcol_9_118019) = (c_tptpcol_9_118019))) -> False). % 0.43/0.62 do 0 intro. intros zenon_H9e. % 0.43/0.62 apply zenon_H9e. apply refl_equal. % 0.43/0.62 (* end of lemma zenon_L11_ *) % 0.43/0.62 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_14_118118) (c_tptpcol_9_118019))) -> False). % 0.43/0.62 do 0 intro. intros zenon_H70 zenon_H9f. % 0.43/0.62 elim (classic ((~((c_tptpcol_14_118118) = (c_tptpcol_10_118020)))/\(~(genls (c_tptpcol_14_118118) (c_tptpcol_10_118020))))); [ zenon_intro zenon_Ha0 | zenon_intro zenon_Ha1 ]. % 0.43/0.62 apply (zenon_and_s _ _ zenon_Ha0). zenon_intro zenon_Ha2. zenon_intro zenon_H91. % 0.43/0.62 apply (zenon_L10_); trivial. % 0.43/0.62 cut ((genls (c_tptpcol_10_118020) (c_tptpcol_9_118019)) = (genls (c_tptpcol_14_118118) (c_tptpcol_9_118019))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_H9f. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact just27. % 0.43/0.62 cut (((c_tptpcol_9_118019) = (c_tptpcol_9_118019))); [idtac | apply NNPP; zenon_intro zenon_H9e]. % 0.43/0.62 cut (((c_tptpcol_10_118020) = (c_tptpcol_14_118118))); [idtac | apply NNPP; zenon_intro zenon_Ha3]. % 0.43/0.62 congruence. % 0.43/0.62 apply (zenon_notand_s _ _ zenon_Ha1); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Ha4 ]. % 0.43/0.62 apply zenon_Ha5. zenon_intro zenon_Ha6. % 0.43/0.62 elim (classic ((c_tptpcol_14_118118) = (c_tptpcol_14_118118))); [ zenon_intro zenon_H7a | zenon_intro zenon_H7b ]. % 0.43/0.62 cut (((c_tptpcol_14_118118) = (c_tptpcol_14_118118)) = ((c_tptpcol_10_118020) = (c_tptpcol_14_118118))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_Ha3. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact zenon_H7a. % 0.43/0.62 cut (((c_tptpcol_14_118118) = (c_tptpcol_14_118118))); [idtac | apply NNPP; zenon_intro zenon_H7b]. % 0.43/0.62 cut (((c_tptpcol_14_118118) = (c_tptpcol_10_118020))); [idtac | apply NNPP; zenon_intro zenon_Ha2]. % 0.43/0.62 congruence. % 0.43/0.62 exact (zenon_Ha2 zenon_Ha6). % 0.43/0.62 apply zenon_H7b. apply refl_equal. % 0.43/0.62 apply zenon_H7b. apply refl_equal. % 0.43/0.62 apply zenon_Ha4. zenon_intro zenon_H9c. % 0.43/0.62 generalize (zenon_H70 (c_tptpcol_14_118118)). zenon_intro zenon_H7c. % 0.43/0.62 generalize (zenon_H7c (c_tptpcol_10_118020)). zenon_intro zenon_Ha7. % 0.43/0.62 generalize (zenon_Ha7 (c_tptpcol_9_118019)). zenon_intro zenon_Ha8. % 0.43/0.62 apply (zenon_imply_s _ _ zenon_Ha8); [ zenon_intro zenon_H91 | zenon_intro zenon_Ha9 ]. % 0.43/0.62 exact (zenon_H91 zenon_H9c). % 0.43/0.62 apply (zenon_imply_s _ _ zenon_Ha9); [ zenon_intro zenon_Hab | zenon_intro zenon_Haa ]. % 0.43/0.62 exact (zenon_Hab just27). % 0.43/0.62 exact (zenon_H9f zenon_Haa). % 0.43/0.62 apply zenon_H9e. apply refl_equal. % 0.43/0.62 (* end of lemma zenon_L12_ *) % 0.43/0.62 assert (zenon_L13_ : (~((c_tptpcol_8_117763) = (c_tptpcol_8_117763))) -> False). % 0.43/0.62 do 0 intro. intros zenon_Hac. % 0.43/0.62 apply zenon_Hac. apply refl_equal. % 0.43/0.62 (* end of lemma zenon_L13_ *) % 0.43/0.62 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_14_118118) (c_tptpcol_8_117763))) -> False). % 0.43/0.62 do 0 intro. intros zenon_H70 zenon_Had. % 0.43/0.62 elim (classic ((~((c_tptpcol_14_118118) = (c_tptpcol_9_118019)))/\(~(genls (c_tptpcol_14_118118) (c_tptpcol_9_118019))))); [ zenon_intro zenon_Hae | zenon_intro zenon_Haf ]. % 0.43/0.62 apply (zenon_and_s _ _ zenon_Hae). zenon_intro zenon_Hb0. zenon_intro zenon_H9f. % 0.43/0.62 apply (zenon_L12_); trivial. % 0.43/0.62 cut ((genls (c_tptpcol_9_118019) (c_tptpcol_8_117763)) = (genls (c_tptpcol_14_118118) (c_tptpcol_8_117763))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_Had. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact just25. % 0.43/0.62 cut (((c_tptpcol_8_117763) = (c_tptpcol_8_117763))); [idtac | apply NNPP; zenon_intro zenon_Hac]. % 0.43/0.62 cut (((c_tptpcol_9_118019) = (c_tptpcol_14_118118))); [idtac | apply NNPP; zenon_intro zenon_Hb1]. % 0.43/0.62 congruence. % 0.43/0.62 apply (zenon_notand_s _ _ zenon_Haf); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hb2 ]. % 0.43/0.62 apply zenon_Hb3. zenon_intro zenon_Hb4. % 0.43/0.62 elim (classic ((c_tptpcol_14_118118) = (c_tptpcol_14_118118))); [ zenon_intro zenon_H7a | zenon_intro zenon_H7b ]. % 0.43/0.62 cut (((c_tptpcol_14_118118) = (c_tptpcol_14_118118)) = ((c_tptpcol_9_118019) = (c_tptpcol_14_118118))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_Hb1. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact zenon_H7a. % 0.43/0.62 cut (((c_tptpcol_14_118118) = (c_tptpcol_14_118118))); [idtac | apply NNPP; zenon_intro zenon_H7b]. % 0.43/0.62 cut (((c_tptpcol_14_118118) = (c_tptpcol_9_118019))); [idtac | apply NNPP; zenon_intro zenon_Hb0]. % 0.43/0.62 congruence. % 0.43/0.62 exact (zenon_Hb0 zenon_Hb4). % 0.43/0.62 apply zenon_H7b. apply refl_equal. % 0.43/0.62 apply zenon_H7b. apply refl_equal. % 0.43/0.62 apply zenon_Hb2. zenon_intro zenon_Haa. % 0.43/0.62 generalize (zenon_H70 (c_tptpcol_14_118118)). zenon_intro zenon_H7c. % 0.43/0.62 generalize (zenon_H7c (c_tptpcol_9_118019)). zenon_intro zenon_Hb5. % 0.43/0.62 generalize (zenon_Hb5 (c_tptpcol_8_117763)). zenon_intro zenon_Hb6. % 0.43/0.62 apply (zenon_imply_s _ _ zenon_Hb6); [ zenon_intro zenon_H9f | zenon_intro zenon_Hb7 ]. % 0.43/0.62 exact (zenon_H9f zenon_Haa). % 0.43/0.62 apply (zenon_imply_s _ _ zenon_Hb7); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hb8 ]. % 0.43/0.62 exact (zenon_Hb9 just25). % 0.43/0.62 exact (zenon_Had zenon_Hb8). % 0.43/0.62 apply zenon_Hac. apply refl_equal. % 0.43/0.62 (* end of lemma zenon_L14_ *) % 0.43/0.62 assert (zenon_L15_ : (~((c_tptpcol_6_112641) = (c_tptpcol_6_112641))) -> False). % 0.43/0.62 do 0 intro. intros zenon_Hba. % 0.43/0.62 apply zenon_Hba. apply refl_equal. % 0.43/0.62 (* end of lemma zenon_L15_ *) % 0.43/0.62 assert (zenon_L16_ : (~((c_tptpcol_5_110593) = (c_tptpcol_5_110593))) -> False). % 0.43/0.62 do 0 intro. intros zenon_Hbb. % 0.43/0.62 apply zenon_Hbb. apply refl_equal. % 0.43/0.62 (* end of lemma zenon_L16_ *) % 0.43/0.62 assert (zenon_L17_ : (~((c_tptpcol_4_106497) = (c_tptpcol_4_106497))) -> False). % 0.43/0.62 do 0 intro. intros zenon_Hbc. % 0.43/0.62 apply zenon_Hbc. apply refl_equal. % 0.43/0.62 (* end of lemma zenon_L17_ *) % 0.43/0.62 assert (zenon_L18_ : (~((c_tptpcol_3_98305) = (c_tptpcol_3_98305))) -> False). % 0.43/0.62 do 0 intro. intros zenon_Hbd. % 0.43/0.62 apply zenon_Hbd. apply refl_equal. % 0.43/0.62 (* end of lemma zenon_L18_ *) % 0.43/0.62 assert (zenon_L19_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (forall ARG2 : zenon_U, (forall NEW : zenon_U, (((disjointwith (c_tptpcol_3_98305) ARG2)/\(genls NEW (c_tptpcol_3_98305)))->(disjointwith NEW ARG2)))) -> (~(disjointwith (c_tptpcol_8_114177) (c_tptpcol_14_118118))) -> (disjointwith (c_tptpcol_3_98305) (c_tptpcol_14_118118)) -> False). % 0.43/0.62 do 0 intro. intros zenon_H70 zenon_Hbe zenon_Hbf zenon_Hc0. % 0.43/0.62 generalize (zenon_Hbe (c_tptpcol_14_118118)). zenon_intro zenon_Hc1. % 0.43/0.62 generalize (zenon_Hc1 (c_tptpcol_8_114177)). zenon_intro zenon_Hc2. % 0.43/0.62 apply (zenon_imply_s _ _ zenon_Hc2); [ zenon_intro zenon_Hc4 | zenon_intro zenon_Hc3 ]. % 0.43/0.62 apply (zenon_notand_s _ _ zenon_Hc4); [ zenon_intro zenon_Hc6 | zenon_intro zenon_Hc5 ]. % 0.43/0.62 exact (zenon_Hc6 zenon_Hc0). % 0.43/0.62 elim (classic ((~((c_tptpcol_8_114177) = (c_tptpcol_4_106497)))/\(~(genls (c_tptpcol_8_114177) (c_tptpcol_4_106497))))); [ zenon_intro zenon_Hc7 | zenon_intro zenon_Hc8 ]. % 0.43/0.62 apply (zenon_and_s _ _ zenon_Hc7). zenon_intro zenon_Hca. zenon_intro zenon_Hc9. % 0.43/0.62 elim (classic ((~((c_tptpcol_8_114177) = (c_tptpcol_5_110593)))/\(~(genls (c_tptpcol_8_114177) (c_tptpcol_5_110593))))); [ zenon_intro zenon_Hcb | zenon_intro zenon_Hcc ]. % 0.43/0.62 apply (zenon_and_s _ _ zenon_Hcb). zenon_intro zenon_Hce. zenon_intro zenon_Hcd. % 0.43/0.62 elim (classic ((~((c_tptpcol_8_114177) = (c_tptpcol_6_112641)))/\(~(genls (c_tptpcol_8_114177) (c_tptpcol_6_112641))))); [ zenon_intro zenon_Hcf | zenon_intro zenon_Hd0 ]. % 0.43/0.62 apply (zenon_and_s _ _ zenon_Hcf). zenon_intro zenon_Hd2. zenon_intro zenon_Hd1. % 0.43/0.62 elim (classic ((~((c_tptpcol_8_114177) = (c_tptpcol_7_113665)))/\(~(genls (c_tptpcol_8_114177) (c_tptpcol_7_113665))))); [ zenon_intro zenon_Hd3 | zenon_intro zenon_Hd4 ]. % 0.43/0.62 apply (zenon_and_s _ _ zenon_Hd3). zenon_intro zenon_Hd6. zenon_intro zenon_Hd5. % 0.43/0.62 exact (zenon_Hd5 just13). % 0.43/0.62 cut ((genls (c_tptpcol_7_113665) (c_tptpcol_6_112641)) = (genls (c_tptpcol_8_114177) (c_tptpcol_6_112641))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_Hd1. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact just11. % 0.43/0.62 cut (((c_tptpcol_6_112641) = (c_tptpcol_6_112641))); [idtac | apply NNPP; zenon_intro zenon_Hba]. % 0.43/0.62 cut (((c_tptpcol_7_113665) = (c_tptpcol_8_114177))); [idtac | apply NNPP; zenon_intro zenon_Hd7]. % 0.43/0.62 congruence. % 0.43/0.62 apply (zenon_notand_s _ _ zenon_Hd4); [ zenon_intro zenon_Hd9 | zenon_intro zenon_Hd8 ]. % 0.43/0.62 apply zenon_Hd9. zenon_intro zenon_Hda. % 0.43/0.62 elim (classic ((c_tptpcol_8_114177) = (c_tptpcol_8_114177))); [ zenon_intro zenon_Hdb | zenon_intro zenon_Hdc ]. % 0.43/0.62 cut (((c_tptpcol_8_114177) = (c_tptpcol_8_114177)) = ((c_tptpcol_7_113665) = (c_tptpcol_8_114177))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_Hd7. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact zenon_Hdb. % 0.43/0.62 cut (((c_tptpcol_8_114177) = (c_tptpcol_8_114177))); [idtac | apply NNPP; zenon_intro zenon_Hdc]. % 0.43/0.62 cut (((c_tptpcol_8_114177) = (c_tptpcol_7_113665))); [idtac | apply NNPP; zenon_intro zenon_Hd6]. % 0.43/0.62 congruence. % 0.43/0.62 exact (zenon_Hd6 zenon_Hda). % 0.43/0.62 apply zenon_Hdc. apply refl_equal. % 0.43/0.62 apply zenon_Hdc. apply refl_equal. % 0.43/0.62 apply zenon_Hd8. zenon_intro just13. % 0.43/0.62 generalize (zenon_H70 (c_tptpcol_8_114177)). zenon_intro zenon_Hdd. % 0.43/0.62 generalize (zenon_Hdd (c_tptpcol_7_113665)). zenon_intro zenon_Hde. % 0.43/0.62 generalize (zenon_Hde (c_tptpcol_6_112641)). zenon_intro zenon_Hdf. % 0.43/0.62 apply (zenon_imply_s _ _ zenon_Hdf); [ zenon_intro zenon_Hd5 | zenon_intro zenon_He0 ]. % 0.43/0.62 exact (zenon_Hd5 just13). % 0.43/0.62 apply (zenon_imply_s _ _ zenon_He0); [ zenon_intro zenon_He2 | zenon_intro zenon_He1 ]. % 0.43/0.62 exact (zenon_He2 just11). % 0.43/0.62 exact (zenon_Hd1 zenon_He1). % 0.43/0.62 apply zenon_Hba. apply refl_equal. % 0.43/0.62 cut ((genls (c_tptpcol_6_112641) (c_tptpcol_5_110593)) = (genls (c_tptpcol_8_114177) (c_tptpcol_5_110593))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_Hcd. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact just9. % 0.43/0.62 cut (((c_tptpcol_5_110593) = (c_tptpcol_5_110593))); [idtac | apply NNPP; zenon_intro zenon_Hbb]. % 0.43/0.62 cut (((c_tptpcol_6_112641) = (c_tptpcol_8_114177))); [idtac | apply NNPP; zenon_intro zenon_He3]. % 0.43/0.62 congruence. % 0.43/0.62 apply (zenon_notand_s _ _ zenon_Hd0); [ zenon_intro zenon_He5 | zenon_intro zenon_He4 ]. % 0.43/0.62 apply zenon_He5. zenon_intro zenon_He6. % 0.43/0.62 elim (classic ((c_tptpcol_8_114177) = (c_tptpcol_8_114177))); [ zenon_intro zenon_Hdb | zenon_intro zenon_Hdc ]. % 0.43/0.62 cut (((c_tptpcol_8_114177) = (c_tptpcol_8_114177)) = ((c_tptpcol_6_112641) = (c_tptpcol_8_114177))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_He3. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact zenon_Hdb. % 0.43/0.62 cut (((c_tptpcol_8_114177) = (c_tptpcol_8_114177))); [idtac | apply NNPP; zenon_intro zenon_Hdc]. % 0.43/0.62 cut (((c_tptpcol_8_114177) = (c_tptpcol_6_112641))); [idtac | apply NNPP; zenon_intro zenon_Hd2]. % 0.43/0.62 congruence. % 0.43/0.62 exact (zenon_Hd2 zenon_He6). % 0.43/0.62 apply zenon_Hdc. apply refl_equal. % 0.43/0.62 apply zenon_Hdc. apply refl_equal. % 0.43/0.62 apply zenon_He4. zenon_intro zenon_He1. % 0.43/0.62 generalize (zenon_H70 (c_tptpcol_8_114177)). zenon_intro zenon_Hdd. % 0.43/0.62 generalize (zenon_Hdd (c_tptpcol_6_112641)). zenon_intro zenon_He7. % 0.43/0.62 generalize (zenon_He7 (c_tptpcol_5_110593)). zenon_intro zenon_He8. % 0.43/0.62 apply (zenon_imply_s _ _ zenon_He8); [ zenon_intro zenon_Hd1 | zenon_intro zenon_He9 ]. % 0.43/0.62 exact (zenon_Hd1 zenon_He1). % 0.43/0.62 apply (zenon_imply_s _ _ zenon_He9); [ zenon_intro zenon_Heb | zenon_intro zenon_Hea ]. % 0.43/0.62 exact (zenon_Heb just9). % 0.43/0.62 exact (zenon_Hcd zenon_Hea). % 0.43/0.62 apply zenon_Hbb. apply refl_equal. % 0.43/0.62 cut ((genls (c_tptpcol_5_110593) (c_tptpcol_4_106497)) = (genls (c_tptpcol_8_114177) (c_tptpcol_4_106497))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_Hc9. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact just7. % 0.43/0.62 cut (((c_tptpcol_4_106497) = (c_tptpcol_4_106497))); [idtac | apply NNPP; zenon_intro zenon_Hbc]. % 0.43/0.62 cut (((c_tptpcol_5_110593) = (c_tptpcol_8_114177))); [idtac | apply NNPP; zenon_intro zenon_Hec]. % 0.43/0.62 congruence. % 0.43/0.62 apply (zenon_notand_s _ _ zenon_Hcc); [ zenon_intro zenon_Hee | zenon_intro zenon_Hed ]. % 0.43/0.62 apply zenon_Hee. zenon_intro zenon_Hef. % 0.43/0.62 elim (classic ((c_tptpcol_8_114177) = (c_tptpcol_8_114177))); [ zenon_intro zenon_Hdb | zenon_intro zenon_Hdc ]. % 0.43/0.62 cut (((c_tptpcol_8_114177) = (c_tptpcol_8_114177)) = ((c_tptpcol_5_110593) = (c_tptpcol_8_114177))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_Hec. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact zenon_Hdb. % 0.43/0.62 cut (((c_tptpcol_8_114177) = (c_tptpcol_8_114177))); [idtac | apply NNPP; zenon_intro zenon_Hdc]. % 0.43/0.62 cut (((c_tptpcol_8_114177) = (c_tptpcol_5_110593))); [idtac | apply NNPP; zenon_intro zenon_Hce]. % 0.43/0.62 congruence. % 0.43/0.62 exact (zenon_Hce zenon_Hef). % 0.43/0.62 apply zenon_Hdc. apply refl_equal. % 0.43/0.62 apply zenon_Hdc. apply refl_equal. % 0.43/0.62 apply zenon_Hed. zenon_intro zenon_Hea. % 0.43/0.62 generalize (zenon_H70 (c_tptpcol_8_114177)). zenon_intro zenon_Hdd. % 0.43/0.62 generalize (zenon_Hdd (c_tptpcol_5_110593)). zenon_intro zenon_Hf0. % 0.43/0.62 generalize (zenon_Hf0 (c_tptpcol_4_106497)). zenon_intro zenon_Hf1. % 0.43/0.62 apply (zenon_imply_s _ _ zenon_Hf1); [ zenon_intro zenon_Hcd | zenon_intro zenon_Hf2 ]. % 0.43/0.62 exact (zenon_Hcd zenon_Hea). % 0.43/0.62 apply (zenon_imply_s _ _ zenon_Hf2); [ zenon_intro zenon_Hf4 | zenon_intro zenon_Hf3 ]. % 0.43/0.62 exact (zenon_Hf4 just7). % 0.43/0.62 exact (zenon_Hc9 zenon_Hf3). % 0.43/0.62 apply zenon_Hbc. apply refl_equal. % 0.43/0.62 cut ((genls (c_tptpcol_4_106497) (c_tptpcol_3_98305)) = (genls (c_tptpcol_8_114177) (c_tptpcol_3_98305))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_Hc5. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact just5. % 0.43/0.62 cut (((c_tptpcol_3_98305) = (c_tptpcol_3_98305))); [idtac | apply NNPP; zenon_intro zenon_Hbd]. % 0.43/0.62 cut (((c_tptpcol_4_106497) = (c_tptpcol_8_114177))); [idtac | apply NNPP; zenon_intro zenon_Hf5]. % 0.43/0.62 congruence. % 0.43/0.62 apply (zenon_notand_s _ _ zenon_Hc8); [ zenon_intro zenon_Hf7 | zenon_intro zenon_Hf6 ]. % 0.43/0.62 apply zenon_Hf7. zenon_intro zenon_Hf8. % 0.43/0.62 elim (classic ((c_tptpcol_8_114177) = (c_tptpcol_8_114177))); [ zenon_intro zenon_Hdb | zenon_intro zenon_Hdc ]. % 0.43/0.62 cut (((c_tptpcol_8_114177) = (c_tptpcol_8_114177)) = ((c_tptpcol_4_106497) = (c_tptpcol_8_114177))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_Hf5. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact zenon_Hdb. % 0.43/0.62 cut (((c_tptpcol_8_114177) = (c_tptpcol_8_114177))); [idtac | apply NNPP; zenon_intro zenon_Hdc]. % 0.43/0.62 cut (((c_tptpcol_8_114177) = (c_tptpcol_4_106497))); [idtac | apply NNPP; zenon_intro zenon_Hca]. % 0.43/0.62 congruence. % 0.43/0.62 exact (zenon_Hca zenon_Hf8). % 0.43/0.62 apply zenon_Hdc. apply refl_equal. % 0.43/0.62 apply zenon_Hdc. apply refl_equal. % 0.43/0.62 apply zenon_Hf6. zenon_intro zenon_Hf3. % 0.43/0.62 generalize (zenon_H70 (c_tptpcol_8_114177)). zenon_intro zenon_Hdd. % 0.43/0.62 generalize (zenon_Hdd (c_tptpcol_4_106497)). zenon_intro zenon_Hf9. % 0.43/0.62 generalize (zenon_Hf9 (c_tptpcol_3_98305)). zenon_intro zenon_Hfa. % 0.43/0.62 apply (zenon_imply_s _ _ zenon_Hfa); [ zenon_intro zenon_Hc9 | zenon_intro zenon_Hfb ]. % 0.43/0.62 exact (zenon_Hc9 zenon_Hf3). % 0.43/0.62 apply (zenon_imply_s _ _ zenon_Hfb); [ zenon_intro zenon_Hfd | zenon_intro zenon_Hfc ]. % 0.43/0.62 exact (zenon_Hfd just5). % 0.43/0.62 exact (zenon_Hc5 zenon_Hfc). % 0.43/0.62 apply zenon_Hbd. apply refl_equal. % 0.43/0.62 exact (zenon_Hbf zenon_Hc3). % 0.43/0.62 (* end of lemma zenon_L19_ *) % 0.43/0.62 apply NNPP. intro zenon_G. % 0.43/0.62 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_H70 | zenon_intro zenon_Hfe ]. % 0.43/0.62 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_Hff. zenon_intro zenon_Hbf. % 0.43/0.62 generalize (just56 (c_tptpcol_3_98305)). zenon_intro zenon_Hbe. % 0.43/0.62 generalize (just55 (c_tptpcol_3_98305)). zenon_intro zenon_H100. % 0.43/0.62 generalize (zenon_H100 (c_tptpcol_8_117763)). zenon_intro zenon_H101. % 0.43/0.62 generalize (zenon_H100 (c_tptpcol_3_114688)). zenon_intro zenon_H102. % 0.43/0.62 generalize (zenon_H102 (c_tptpcol_8_117763)). zenon_intro zenon_H103. % 0.43/0.62 apply (zenon_imply_s _ _ zenon_H103); [ zenon_intro zenon_H105 | zenon_intro zenon_H104 ]. % 0.43/0.62 apply (zenon_notand_s _ _ zenon_H105); [ zenon_intro zenon_H107 | zenon_intro zenon_H106 ]. % 0.43/0.62 exact (zenon_H107 just37). % 0.43/0.62 elim (classic ((~((c_tptpcol_8_117763) = (c_tptpcol_4_114689)))/\(~(genls (c_tptpcol_8_117763) (c_tptpcol_4_114689))))); [ zenon_intro zenon_H108 | zenon_intro zenon_H109 ]. % 0.43/0.62 apply (zenon_and_s _ _ zenon_H108). zenon_intro zenon_H10b. zenon_intro zenon_H10a. % 0.43/0.62 elim (classic ((~((c_tptpcol_8_117763) = (c_tptpcol_5_114690)))/\(~(genls (c_tptpcol_8_117763) (c_tptpcol_5_114690))))); [ zenon_intro zenon_H10c | zenon_intro zenon_H10d ]. % 0.43/0.62 apply (zenon_and_s _ _ zenon_H10c). zenon_intro zenon_H10f. zenon_intro zenon_H10e. % 0.43/0.62 elim (classic ((~((c_tptpcol_8_117763) = (c_tptpcol_6_116738)))/\(~(genls (c_tptpcol_8_117763) (c_tptpcol_6_116738))))); [ zenon_intro zenon_H110 | zenon_intro zenon_H111 ]. % 0.43/0.62 apply (zenon_and_s _ _ zenon_H110). zenon_intro zenon_H113. zenon_intro zenon_H112. % 0.43/0.62 elim (classic ((~((c_tptpcol_8_117763) = (c_tptpcol_7_117762)))/\(~(genls (c_tptpcol_8_117763) (c_tptpcol_7_117762))))); [ zenon_intro zenon_H114 | zenon_intro zenon_H115 ]. % 0.43/0.62 apply (zenon_and_s _ _ zenon_H114). zenon_intro zenon_H117. zenon_intro zenon_H116. % 0.43/0.62 exact (zenon_H116 just23). % 0.43/0.62 cut ((genls (c_tptpcol_7_117762) (c_tptpcol_6_116738)) = (genls (c_tptpcol_8_117763) (c_tptpcol_6_116738))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_H112. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact just21. % 0.43/0.62 cut (((c_tptpcol_6_116738) = (c_tptpcol_6_116738))); [idtac | apply NNPP; zenon_intro zenon_H6b]. % 0.43/0.62 cut (((c_tptpcol_7_117762) = (c_tptpcol_8_117763))); [idtac | apply NNPP; zenon_intro zenon_H118]. % 0.43/0.62 congruence. % 0.43/0.62 apply (zenon_notand_s _ _ zenon_H115); [ zenon_intro zenon_H11a | zenon_intro zenon_H119 ]. % 0.43/0.62 apply zenon_H11a. zenon_intro zenon_H11b. % 0.43/0.62 elim (classic ((c_tptpcol_8_117763) = (c_tptpcol_8_117763))); [ zenon_intro zenon_H11c | zenon_intro zenon_Hac ]. % 0.43/0.62 cut (((c_tptpcol_8_117763) = (c_tptpcol_8_117763)) = ((c_tptpcol_7_117762) = (c_tptpcol_8_117763))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_H118. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact zenon_H11c. % 0.43/0.62 cut (((c_tptpcol_8_117763) = (c_tptpcol_8_117763))); [idtac | apply NNPP; zenon_intro zenon_Hac]. % 0.43/0.62 cut (((c_tptpcol_8_117763) = (c_tptpcol_7_117762))); [idtac | apply NNPP; zenon_intro zenon_H117]. % 0.43/0.62 congruence. % 0.43/0.62 exact (zenon_H117 zenon_H11b). % 0.43/0.62 apply zenon_Hac. apply refl_equal. % 0.43/0.62 apply zenon_Hac. apply refl_equal. % 0.43/0.62 apply zenon_H119. zenon_intro just23. % 0.43/0.62 generalize (zenon_H70 (c_tptpcol_8_117763)). zenon_intro zenon_H11d. % 0.43/0.62 generalize (zenon_H11d (c_tptpcol_7_117762)). zenon_intro zenon_H11e. % 0.43/0.62 generalize (zenon_H11e (c_tptpcol_6_116738)). zenon_intro zenon_H11f. % 0.43/0.62 apply (zenon_imply_s _ _ zenon_H11f); [ zenon_intro zenon_H116 | zenon_intro zenon_H120 ]. % 0.43/0.62 exact (zenon_H116 just23). % 0.43/0.62 apply (zenon_imply_s _ _ zenon_H120); [ zenon_intro zenon_H122 | zenon_intro zenon_H121 ]. % 0.43/0.62 exact (zenon_H122 just21). % 0.43/0.62 exact (zenon_H112 zenon_H121). % 0.43/0.62 apply zenon_H6b. apply refl_equal. % 0.43/0.62 cut ((genls (c_tptpcol_6_116738) (c_tptpcol_5_114690)) = (genls (c_tptpcol_8_117763) (c_tptpcol_5_114690))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_H10e. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact just19. % 0.43/0.62 cut (((c_tptpcol_5_114690) = (c_tptpcol_5_114690))); [idtac | apply NNPP; zenon_intro zenon_H6c]. % 0.43/0.62 cut (((c_tptpcol_6_116738) = (c_tptpcol_8_117763))); [idtac | apply NNPP; zenon_intro zenon_H123]. % 0.43/0.62 congruence. % 0.43/0.62 apply (zenon_notand_s _ _ zenon_H111); [ zenon_intro zenon_H125 | zenon_intro zenon_H124 ]. % 0.43/0.62 apply zenon_H125. zenon_intro zenon_H126. % 0.43/0.62 elim (classic ((c_tptpcol_8_117763) = (c_tptpcol_8_117763))); [ zenon_intro zenon_H11c | zenon_intro zenon_Hac ]. % 0.43/0.62 cut (((c_tptpcol_8_117763) = (c_tptpcol_8_117763)) = ((c_tptpcol_6_116738) = (c_tptpcol_8_117763))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_H123. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact zenon_H11c. % 0.43/0.62 cut (((c_tptpcol_8_117763) = (c_tptpcol_8_117763))); [idtac | apply NNPP; zenon_intro zenon_Hac]. % 0.43/0.62 cut (((c_tptpcol_8_117763) = (c_tptpcol_6_116738))); [idtac | apply NNPP; zenon_intro zenon_H113]. % 0.43/0.62 congruence. % 0.43/0.62 exact (zenon_H113 zenon_H126). % 0.43/0.62 apply zenon_Hac. apply refl_equal. % 0.43/0.62 apply zenon_Hac. apply refl_equal. % 0.43/0.62 apply zenon_H124. zenon_intro zenon_H121. % 0.43/0.62 generalize (zenon_H70 (c_tptpcol_8_117763)). zenon_intro zenon_H11d. % 0.43/0.62 generalize (zenon_H11d (c_tptpcol_6_116738)). zenon_intro zenon_H127. % 0.43/0.62 generalize (zenon_H127 (c_tptpcol_5_114690)). zenon_intro zenon_H128. % 0.43/0.62 apply (zenon_imply_s _ _ zenon_H128); [ zenon_intro zenon_H112 | zenon_intro zenon_H129 ]. % 0.43/0.62 exact (zenon_H112 zenon_H121). % 0.43/0.62 apply (zenon_imply_s _ _ zenon_H129); [ zenon_intro zenon_H12b | zenon_intro zenon_H12a ]. % 0.43/0.62 exact (zenon_H12b just19). % 0.43/0.62 exact (zenon_H10e zenon_H12a). % 0.43/0.62 apply zenon_H6c. apply refl_equal. % 0.43/0.62 cut ((genls (c_tptpcol_5_114690) (c_tptpcol_4_114689)) = (genls (c_tptpcol_8_117763) (c_tptpcol_4_114689))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_H10a. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact just17. % 0.43/0.62 cut (((c_tptpcol_4_114689) = (c_tptpcol_4_114689))); [idtac | apply NNPP; zenon_intro zenon_H6d]. % 0.43/0.62 cut (((c_tptpcol_5_114690) = (c_tptpcol_8_117763))); [idtac | apply NNPP; zenon_intro zenon_H12c]. % 0.43/0.62 congruence. % 0.43/0.62 apply (zenon_notand_s _ _ zenon_H10d); [ zenon_intro zenon_H12e | zenon_intro zenon_H12d ]. % 0.43/0.62 apply zenon_H12e. zenon_intro zenon_H12f. % 0.43/0.62 elim (classic ((c_tptpcol_8_117763) = (c_tptpcol_8_117763))); [ zenon_intro zenon_H11c | zenon_intro zenon_Hac ]. % 0.43/0.62 cut (((c_tptpcol_8_117763) = (c_tptpcol_8_117763)) = ((c_tptpcol_5_114690) = (c_tptpcol_8_117763))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_H12c. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact zenon_H11c. % 0.43/0.62 cut (((c_tptpcol_8_117763) = (c_tptpcol_8_117763))); [idtac | apply NNPP; zenon_intro zenon_Hac]. % 0.43/0.62 cut (((c_tptpcol_8_117763) = (c_tptpcol_5_114690))); [idtac | apply NNPP; zenon_intro zenon_H10f]. % 0.43/0.62 congruence. % 0.43/0.62 exact (zenon_H10f zenon_H12f). % 0.43/0.62 apply zenon_Hac. apply refl_equal. % 0.43/0.62 apply zenon_Hac. apply refl_equal. % 0.43/0.62 apply zenon_H12d. zenon_intro zenon_H12a. % 0.43/0.62 generalize (zenon_H70 (c_tptpcol_8_117763)). zenon_intro zenon_H11d. % 0.43/0.62 generalize (zenon_H11d (c_tptpcol_5_114690)). zenon_intro zenon_H130. % 0.43/0.62 generalize (zenon_H130 (c_tptpcol_4_114689)). zenon_intro zenon_H131. % 0.43/0.62 apply (zenon_imply_s _ _ zenon_H131); [ zenon_intro zenon_H10e | zenon_intro zenon_H132 ]. % 0.43/0.62 exact (zenon_H10e zenon_H12a). % 0.43/0.62 apply (zenon_imply_s _ _ zenon_H132); [ zenon_intro zenon_H134 | zenon_intro zenon_H133 ]. % 0.43/0.62 exact (zenon_H134 just17). % 0.43/0.62 exact (zenon_H10a zenon_H133). % 0.43/0.62 apply zenon_H6d. apply refl_equal. % 0.43/0.62 cut ((genls (c_tptpcol_4_114689) (c_tptpcol_3_114688)) = (genls (c_tptpcol_8_117763) (c_tptpcol_3_114688))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_H106. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact just15. % 0.43/0.62 cut (((c_tptpcol_3_114688) = (c_tptpcol_3_114688))); [idtac | apply NNPP; zenon_intro zenon_H6e]. % 0.43/0.62 cut (((c_tptpcol_4_114689) = (c_tptpcol_8_117763))); [idtac | apply NNPP; zenon_intro zenon_H135]. % 0.43/0.62 congruence. % 0.43/0.62 apply (zenon_notand_s _ _ zenon_H109); [ zenon_intro zenon_H137 | zenon_intro zenon_H136 ]. % 0.43/0.62 apply zenon_H137. zenon_intro zenon_H138. % 0.43/0.62 elim (classic ((c_tptpcol_8_117763) = (c_tptpcol_8_117763))); [ zenon_intro zenon_H11c | zenon_intro zenon_Hac ]. % 0.43/0.62 cut (((c_tptpcol_8_117763) = (c_tptpcol_8_117763)) = ((c_tptpcol_4_114689) = (c_tptpcol_8_117763))). % 0.43/0.62 intro zenon_D_pnotp. % 0.43/0.62 apply zenon_H135. % 0.43/0.62 rewrite <- zenon_D_pnotp. % 0.43/0.62 exact zenon_H11c. % 0.43/0.62 cut (((c_tptpcol_8_117763) = (c_tptpcol_8_117763))); [idtac | apply NNPP; zenon_intro zenon_Hac]. % 0.43/0.62 cut (((c_tptpcol_8_117763) = (c_tptpcol_4_114689))); [idtac | apply NNPP; zenon_intro zenon_H10b]. % 0.43/0.62 congruence. % 0.43/0.62 exact (zenon_H10b zenon_H138). % 0.43/0.62 apply zenon_Hac. apply refl_equal. % 0.43/0.62 apply zenon_Hac. apply refl_equal. % 0.43/0.62 apply zenon_H136. zenon_intro zenon_H133. % 0.43/0.62 generalize (zenon_H70 (c_tptpcol_8_117763)). zenon_intro zenon_H11d. % 0.43/0.62 generalize (zenon_H11d (c_tptpcol_4_114689)). zenon_intro zenon_H139. % 0.43/0.62 generalize (zenon_H139 (c_tptpcol_3_114688)). zenon_intro zenon_H13a. % 0.43/0.62 apply (zenon_imply_s _ _ zenon_H13a); [ zenon_intro zenon_H10a | zenon_intro zenon_H13b ]. % 0.43/0.62 exact (zenon_H10a zenon_H133). % 0.43/0.62 apply (zenon_imply_s _ _ zenon_H13b); [ zenon_intro zenon_H13d | zenon_intro zenon_H13c ]. % 0.43/0.62 exact (zenon_H13d just15). % 0.43/0.62 exact (zenon_H106 zenon_H13c). % 0.43/0.62 apply zenon_H6e. apply refl_equal. % 0.43/0.62 generalize (zenon_H101 (c_tptpcol_14_118118)). zenon_intro zenon_H13e. % 0.43/0.62 apply (zenon_imply_s _ _ zenon_H13e); [ zenon_intro zenon_H13f | zenon_intro zenon_Hc0 ]. % 0.43/0.62 apply (zenon_notand_s _ _ zenon_H13f); [ zenon_intro zenon_H140 | zenon_intro zenon_Had ]. % 0.43/0.62 exact (zenon_H140 zenon_H104). % 0.43/0.62 apply (zenon_L14_); trivial. % 0.43/0.62 apply (zenon_L19_); trivial. % 0.43/0.62 apply zenon_Hfe. zenon_intro zenon_Tx_mj. apply NNPP. zenon_intro zenon_H142. % 0.43/0.62 apply zenon_H142. zenon_intro zenon_Ty_ml. apply NNPP. zenon_intro zenon_H144. % 0.43/0.62 apply zenon_H144. zenon_intro zenon_Tz_mn. apply NNPP. zenon_intro zenon_H146. % 0.43/0.62 apply (zenon_notimply_s _ _ zenon_H146). zenon_intro zenon_H148. zenon_intro zenon_H147. % 0.43/0.62 apply (zenon_notimply_s _ _ zenon_H147). zenon_intro zenon_H14a. zenon_intro zenon_H149. % 0.43/0.62 generalize (just97 zenon_Tx_mj). zenon_intro zenon_H14b. % 0.43/0.62 generalize (zenon_H14b zenon_Ty_ml). zenon_intro zenon_H14c. % 0.43/0.62 generalize (zenon_H14c zenon_Tz_mn). zenon_intro zenon_H14d. % 0.43/0.62 apply (zenon_imply_s _ _ zenon_H14d); [ zenon_intro zenon_H14f | zenon_intro zenon_H14e ]. % 0.43/0.62 apply (zenon_notand_s _ _ zenon_H14f); [ zenon_intro zenon_H151 | zenon_intro zenon_H150 ]. % 0.43/0.62 exact (zenon_H151 zenon_H148). % 0.43/0.62 exact (zenon_H150 zenon_H14a). % 0.43/0.62 exact (zenon_H149 zenon_H14e). % 0.43/0.62 Qed. % 0.43/0.62 % SZS output end Proof % 0.43/0.62 (* END-PROOF *) % 0.43/0.62 nodes searched: 4590 % 0.43/0.62 max branch formulas: 2330 % 0.43/0.62 proof nodes created: 91 % 0.43/0.62 formulas created: 26380 % 0.43/0.62 %------------------------------------------------------------------------------