%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT082+1 : TPTP v9.3.1. Bugfixed v9.3.1. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n027.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:24:27 AM UTC 2026 % Result : Theorem 0.45s 0.74s % Output : Proof 0.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT082+1 : TPTP v9.3.1. Bugfixed v9.3.1. % 0.00/0.04 % Command : run_zenon %s %d % 0.08/0.35 % Computer : n027.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Mon Sep 7 14:20:00 UTC 2026 % 0.08/0.36 % CPUTime : % 0.45/0.74 (* PROOF-FOUND *) % 0.45/0.74 % SZS status Theorem % 0.45/0.74 (* BEGIN-PROOF *) % 0.45/0.74 % SZS output start Proof % 0.45/0.74 Theorem odrl411 : (~(exists X : zenon_U, (exists Y : zenon_U, (exists Z : zenon_U, ((in_closed X (v600) (v600))/\((in_closed X (v601) (v601))/\((less (v300) Y)/\((in_open Y (v0) (v500))/\((leq (v16) Z)/\(in_lopen Z (v0) (v32))))))))))). % 0.45/0.74 Proof. % 0.45/0.74 assert (zenon_L1_ : forall (zenon_TX_ch : zenon_U), (less zenon_TX_ch (v600)) -> (~(leq zenon_TX_ch (v600))) -> False). % 0.45/0.74 do 1 intro. intros zenon_H39 zenon_H3a. % 0.45/0.74 generalize (leq_def zenon_TX_ch). zenon_intro zenon_H3c. % 0.45/0.74 generalize (zenon_H3c (v600)). zenon_intro zenon_H3d. % 0.45/0.74 apply (zenon_equiv_s _ _ zenon_H3d); [ zenon_intro zenon_H3a; zenon_intro zenon_H40 | zenon_intro zenon_H3f; zenon_intro zenon_H3e ]. % 0.45/0.74 apply (zenon_notor_s _ _ zenon_H40). zenon_intro zenon_H42. zenon_intro zenon_H41. % 0.45/0.74 exact (zenon_H42 zenon_H39). % 0.45/0.74 exact (zenon_H3a zenon_H3f). % 0.45/0.74 (* end of lemma zenon_L1_ *) % 0.45/0.74 assert (zenon_L2_ : forall (zenon_TX_ch : zenon_U), (less (v600) zenon_TX_ch) -> (~(leq (v600) zenon_TX_ch)) -> False). % 0.45/0.74 do 1 intro. intros zenon_H43 zenon_H44. % 0.45/0.74 generalize (leq_def (v600)). zenon_intro zenon_H45. % 0.45/0.74 generalize (zenon_H45 zenon_TX_ch). zenon_intro zenon_H46. % 0.45/0.74 apply (zenon_equiv_s _ _ zenon_H46); [ zenon_intro zenon_H44; zenon_intro zenon_H49 | zenon_intro zenon_H48; zenon_intro zenon_H47 ]. % 0.45/0.74 apply (zenon_notor_s _ _ zenon_H49). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 0.45/0.74 exact (zenon_H4b zenon_H43). % 0.45/0.74 exact (zenon_H44 zenon_H48). % 0.45/0.74 (* end of lemma zenon_L2_ *) % 0.45/0.74 assert (zenon_L3_ : forall (zenon_TX_ch : zenon_U), (less zenon_TX_ch (v601)) -> (~(leq zenon_TX_ch (v601))) -> False). % 0.45/0.74 do 1 intro. intros zenon_H4c zenon_H4d. % 0.45/0.74 generalize (leq_def zenon_TX_ch). zenon_intro zenon_H3c. % 0.45/0.74 generalize (zenon_H3c (v601)). zenon_intro zenon_H4e. % 0.45/0.74 apply (zenon_equiv_s _ _ zenon_H4e); [ zenon_intro zenon_H4d; zenon_intro zenon_H51 | zenon_intro zenon_H50; zenon_intro zenon_H4f ]. % 0.45/0.74 apply (zenon_notor_s _ _ zenon_H51). zenon_intro zenon_H53. zenon_intro zenon_H52. % 0.45/0.74 exact (zenon_H53 zenon_H4c). % 0.45/0.74 exact (zenon_H4d zenon_H50). % 0.45/0.74 (* end of lemma zenon_L3_ *) % 0.45/0.74 assert (zenon_L4_ : forall (zenon_TX_ch : zenon_U), (less (v601) zenon_TX_ch) -> (~(leq (v601) zenon_TX_ch)) -> False). % 0.45/0.74 do 1 intro. intros zenon_H54 zenon_H55. % 0.45/0.74 generalize (leq_def (v601)). zenon_intro zenon_H56. % 0.45/0.74 generalize (zenon_H56 zenon_TX_ch). zenon_intro zenon_H57. % 0.45/0.74 apply (zenon_equiv_s _ _ zenon_H57); [ zenon_intro zenon_H55; zenon_intro zenon_H5a | zenon_intro zenon_H59; zenon_intro zenon_H58 ]. % 0.45/0.74 apply (zenon_notor_s _ _ zenon_H5a). zenon_intro zenon_H5c. zenon_intro zenon_H5b. % 0.45/0.74 exact (zenon_H5c zenon_H54). % 0.45/0.74 exact (zenon_H55 zenon_H59). % 0.45/0.74 (* end of lemma zenon_L4_ *) % 0.45/0.74 assert (zenon_L5_ : (~((v600) = (v600))) -> False). % 0.45/0.74 do 0 intro. intros zenon_H5d. % 0.45/0.74 apply zenon_H5d. apply refl_equal. % 0.45/0.74 (* end of lemma zenon_L5_ *) % 0.45/0.74 assert (zenon_L6_ : forall (zenon_TX_ch : zenon_U), (zenon_TX_ch = (v600)) -> (less zenon_TX_ch (v601)) -> (less (v601) zenon_TX_ch) -> (~((v600) = (v601))) -> False). % 0.45/0.74 do 1 intro. intros zenon_H5e zenon_H4c zenon_H54 zenon_H5f. % 0.45/0.74 elim (classic ((v601) = (v601))); [ zenon_intro zenon_H60 | zenon_intro zenon_H61 ]. % 0.45/0.74 cut (((v601) = (v601)) = ((v600) = (v601))). % 0.45/0.74 intro zenon_D_pnotp. % 0.45/0.74 apply zenon_H5f. % 0.45/0.74 rewrite <- zenon_D_pnotp. % 0.45/0.74 exact zenon_H60. % 0.45/0.74 cut (((v601) = (v601))); [idtac | apply NNPP; zenon_intro zenon_H61]. % 0.45/0.74 cut (((v601) = (v600))); [idtac | apply NNPP; zenon_intro zenon_H62]. % 0.45/0.74 congruence. % 0.45/0.74 cut ((zenon_TX_ch = (v600)) = ((v601) = (v600))). % 0.45/0.74 intro zenon_D_pnotp. % 0.45/0.74 apply zenon_H62. % 0.45/0.74 rewrite <- zenon_D_pnotp. % 0.45/0.74 exact zenon_H5e. % 0.45/0.74 cut (((v600) = (v600))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 0.45/0.74 cut ((zenon_TX_ch = (v601))); [idtac | apply NNPP; zenon_intro zenon_H52]. % 0.45/0.74 congruence. % 0.45/0.74 elim (classic ((v601) = (v601))); [ zenon_intro zenon_H60 | zenon_intro zenon_H61 ]. % 0.45/0.74 cut (((v601) = (v601)) = (zenon_TX_ch = (v601))). % 0.45/0.74 intro zenon_D_pnotp. % 0.45/0.74 apply zenon_H52. % 0.45/0.74 rewrite <- zenon_D_pnotp. % 0.45/0.74 exact zenon_H60. % 0.45/0.74 cut (((v601) = (v601))); [idtac | apply NNPP; zenon_intro zenon_H61]. % 0.45/0.74 cut (((v601) = zenon_TX_ch)); [idtac | apply NNPP; zenon_intro zenon_H5b]. % 0.45/0.74 congruence. % 0.45/0.74 generalize (leq_antisym zenon_TX_ch). zenon_intro zenon_H63. % 0.45/0.74 generalize (zenon_H63 (v601)). zenon_intro zenon_H64. % 0.45/0.74 apply (zenon_imply_s _ _ zenon_H64); [ zenon_intro zenon_H66 | zenon_intro zenon_H65 ]. % 0.45/0.74 apply (zenon_notand_s _ _ zenon_H66); [ zenon_intro zenon_H4d | zenon_intro zenon_H55 ]. % 0.45/0.74 apply (zenon_L3_ zenon_TX_ch); trivial. % 0.45/0.74 apply (zenon_L4_ zenon_TX_ch); trivial. % 0.45/0.74 apply zenon_H5b. apply sym_equal. exact zenon_H65. % 0.45/0.74 apply zenon_H61. apply refl_equal. % 0.45/0.74 apply zenon_H61. apply refl_equal. % 0.45/0.74 apply zenon_H5d. apply refl_equal. % 0.45/0.74 apply zenon_H61. apply refl_equal. % 0.45/0.74 apply zenon_H61. apply refl_equal. % 0.45/0.74 (* end of lemma zenon_L6_ *) % 0.45/0.74 assert (zenon_L7_ : (~((v601) = (v601))) -> False). % 0.45/0.74 do 0 intro. intros zenon_H61. % 0.45/0.74 apply zenon_H61. apply refl_equal. % 0.45/0.74 (* end of lemma zenon_L7_ *) % 0.45/0.74 apply NNPP. intro zenon_G. % 0.45/0.74 apply (zenon_and_s _ _ distinct). zenon_intro zenon_H68. zenon_intro zenon_H67. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H67). zenon_intro zenon_H6a. zenon_intro zenon_H69. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H69). zenon_intro zenon_H6c. zenon_intro zenon_H6b. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H6b). zenon_intro zenon_H6e. zenon_intro zenon_H6d. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H6d). zenon_intro zenon_H70. zenon_intro zenon_H6f. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H6f). zenon_intro zenon_H72. zenon_intro zenon_H71. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H71). zenon_intro zenon_H74. zenon_intro zenon_H73. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H73). zenon_intro zenon_H76. zenon_intro zenon_H75. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H75). zenon_intro zenon_H78. zenon_intro zenon_H77. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H77). zenon_intro zenon_H7a. zenon_intro zenon_H79. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H79). zenon_intro zenon_H7c. zenon_intro zenon_H7b. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H7b). zenon_intro zenon_H7e. zenon_intro zenon_H7d. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H7d). zenon_intro zenon_H80. zenon_intro zenon_H7f. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H7f). zenon_intro zenon_H82. zenon_intro zenon_H81. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H81). zenon_intro zenon_H84. zenon_intro zenon_H83. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H83). zenon_intro zenon_H86. zenon_intro zenon_H85. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H85). zenon_intro zenon_H88. zenon_intro zenon_H87. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H87). zenon_intro zenon_H8a. zenon_intro zenon_H89. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H89). zenon_intro zenon_H8c. zenon_intro zenon_H8b. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H8b). zenon_intro zenon_H8d. zenon_intro zenon_H5f. % 0.45/0.74 apply zenon_G. zenon_intro zenon_H8e. % 0.45/0.74 elim zenon_H8e. zenon_intro zenon_TX_ch. zenon_intro zenon_H8f. % 0.45/0.74 elim zenon_H8f. zenon_intro zenon_TY_fo. zenon_intro zenon_H91. % 0.45/0.74 elim zenon_H91. zenon_intro zenon_TZ_fq. zenon_intro zenon_H93. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H93). zenon_intro zenon_H95. zenon_intro zenon_H94. % 0.45/0.74 apply (zenon_and_s _ _ zenon_H94). zenon_intro zenon_H97. zenon_intro zenon_H96. % 0.45/0.74 generalize (in_closed zenon_TX_ch). zenon_intro zenon_H98. % 0.45/0.74 generalize (zenon_H98 (v600)). zenon_intro zenon_H99. % 0.45/0.74 generalize (zenon_H99 (v600)). zenon_intro zenon_H9a. % 0.45/0.74 apply (zenon_equiv_s _ _ zenon_H9a); [ zenon_intro zenon_H9d; zenon_intro zenon_H9c | zenon_intro zenon_H95; zenon_intro zenon_H9b ]. % 0.45/0.74 exact (zenon_H9d zenon_H95). % 0.45/0.74 apply (zenon_and_s _ _ zenon_H9b). zenon_intro zenon_H48. zenon_intro zenon_H3f. % 0.45/0.74 generalize (leq_def (v600)). zenon_intro zenon_H45. % 0.45/0.74 generalize (zenon_H45 zenon_TX_ch). zenon_intro zenon_H46. % 0.45/0.74 apply (zenon_equiv_s _ _ zenon_H46); [ zenon_intro zenon_H44; zenon_intro zenon_H49 | zenon_intro zenon_H48; zenon_intro zenon_H47 ]. % 0.45/0.74 exact (zenon_H44 zenon_H48). % 0.45/0.74 generalize (leq_def zenon_TX_ch). zenon_intro zenon_H3c. % 0.45/0.74 generalize (zenon_H3c (v600)). zenon_intro zenon_H3d. % 0.45/0.74 apply (zenon_equiv_s _ _ zenon_H3d); [ zenon_intro zenon_H3a; zenon_intro zenon_H40 | zenon_intro zenon_H3f; zenon_intro zenon_H3e ]. % 0.45/0.74 exact (zenon_H3a zenon_H3f). % 0.45/0.74 generalize (in_closed zenon_TX_ch). zenon_intro zenon_H98. % 0.45/0.74 generalize (zenon_H98 (v601)). zenon_intro zenon_H9e. % 0.45/0.74 generalize (zenon_H9e (v601)). zenon_intro zenon_H9f. % 0.45/0.74 apply (zenon_equiv_s _ _ zenon_H9f); [ zenon_intro zenon_Ha2; zenon_intro zenon_Ha1 | zenon_intro zenon_H97; zenon_intro zenon_Ha0 ]. % 0.45/0.74 exact (zenon_Ha2 zenon_H97). % 0.45/0.74 apply (zenon_and_s _ _ zenon_Ha0). zenon_intro zenon_H59. zenon_intro zenon_H50. % 0.45/0.74 generalize (leq_def (v601)). zenon_intro zenon_H56. % 0.45/0.74 generalize (zenon_H56 zenon_TX_ch). zenon_intro zenon_H57. % 0.45/0.74 apply (zenon_equiv_s _ _ zenon_H57); [ zenon_intro zenon_H55; zenon_intro zenon_H5a | zenon_intro zenon_H59; zenon_intro zenon_H58 ]. % 0.45/0.74 exact (zenon_H55 zenon_H59). % 0.45/0.74 generalize (leq_def zenon_TX_ch). zenon_intro zenon_H3c. % 0.45/0.74 generalize (zenon_H3c (v601)). zenon_intro zenon_H4e. % 0.45/0.74 apply (zenon_equiv_s _ _ zenon_H4e); [ zenon_intro zenon_H4d; zenon_intro zenon_H51 | zenon_intro zenon_H50; zenon_intro zenon_H4f ]. % 0.45/0.74 exact (zenon_H4d zenon_H50). % 0.45/0.74 apply (zenon_or_s _ _ zenon_H4f); [ zenon_intro zenon_H4c | zenon_intro zenon_H65 ]. % 0.45/0.74 apply (zenon_or_s _ _ zenon_H58); [ zenon_intro zenon_H54 | zenon_intro zenon_Ha3 ]. % 0.45/0.74 apply (zenon_or_s _ _ zenon_H3e); [ zenon_intro zenon_H39 | zenon_intro zenon_H5e ]. % 0.45/0.74 apply (zenon_or_s _ _ zenon_H47); [ zenon_intro zenon_H43 | zenon_intro zenon_Ha4 ]. % 0.45/0.74 generalize (leq_antisym zenon_TX_ch). zenon_intro zenon_H63. % 0.45/0.74 generalize (zenon_H63 (v600)). zenon_intro zenon_Ha5. % 0.45/0.74 apply (zenon_imply_s _ _ zenon_Ha5); [ zenon_intro zenon_Ha6 | zenon_intro zenon_H5e ]. % 0.45/0.74 apply (zenon_notand_s _ _ zenon_Ha6); [ zenon_intro zenon_H3a | zenon_intro zenon_H44 ]. % 0.45/0.74 apply (zenon_L1_ zenon_TX_ch); trivial. % 0.45/0.74 apply (zenon_L2_ zenon_TX_ch); trivial. % 0.45/0.74 apply (zenon_L6_ zenon_TX_ch); trivial. % 0.45/0.74 cut (((v600) = zenon_TX_ch) = ((v600) = (v601))). % 0.45/0.74 intro zenon_D_pnotp. % 0.45/0.74 apply zenon_H5f. % 0.45/0.74 rewrite <- zenon_D_pnotp. % 0.45/0.74 exact zenon_Ha4. % 0.45/0.74 cut ((zenon_TX_ch = (v601))); [idtac | apply NNPP; zenon_intro zenon_H52]. % 0.45/0.74 cut (((v600) = (v600))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 0.45/0.74 congruence. % 0.45/0.74 apply zenon_H5d. apply refl_equal. % 0.45/0.74 generalize (leq_antisym zenon_TX_ch). zenon_intro zenon_H63. % 0.45/0.74 generalize (zenon_H63 (v601)). zenon_intro zenon_H64. % 0.45/0.74 apply (zenon_imply_s _ _ zenon_H64); [ zenon_intro zenon_H66 | zenon_intro zenon_H65 ]. % 0.45/0.74 apply (zenon_notand_s _ _ zenon_H66); [ zenon_intro zenon_H4d | zenon_intro zenon_H55 ]. % 0.45/0.74 apply (zenon_L3_ zenon_TX_ch); trivial. % 0.45/0.74 apply (zenon_L4_ zenon_TX_ch); trivial. % 0.45/0.74 exact (zenon_H52 zenon_H65). % 0.45/0.74 apply (zenon_L6_ zenon_TX_ch); trivial. % 0.45/0.74 apply (zenon_or_s _ _ zenon_H3e); [ zenon_intro zenon_H39 | zenon_intro zenon_H5e ]. % 0.45/0.74 apply (zenon_or_s _ _ zenon_H47); [ zenon_intro zenon_H43 | zenon_intro zenon_Ha4 ]. % 0.45/0.74 elim (classic ((v601) = (v601))); [ zenon_intro zenon_H60 | zenon_intro zenon_H61 ]. % 0.45/0.74 cut (((v601) = (v601)) = ((v600) = (v601))). % 0.45/0.74 intro zenon_D_pnotp. % 0.45/0.74 apply zenon_H5f. % 0.45/0.74 rewrite <- zenon_D_pnotp. % 0.45/0.74 exact zenon_H60. % 0.45/0.74 cut (((v601) = (v601))); [idtac | apply NNPP; zenon_intro zenon_H61]. % 0.45/0.74 cut (((v601) = (v600))); [idtac | apply NNPP; zenon_intro zenon_H62]. % 0.45/0.74 congruence. % 0.45/0.74 cut (((v601) = zenon_TX_ch) = ((v601) = (v600))). % 0.45/0.74 intro zenon_D_pnotp. % 0.45/0.74 apply zenon_H62. % 0.45/0.74 rewrite <- zenon_D_pnotp. % 0.45/0.74 exact zenon_Ha3. % 0.45/0.74 cut ((zenon_TX_ch = (v600))); [idtac | apply NNPP; zenon_intro zenon_H41]. % 0.45/0.74 cut (((v601) = (v601))); [idtac | apply NNPP; zenon_intro zenon_H61]. % 0.45/0.74 congruence. % 0.45/0.74 apply zenon_H61. apply refl_equal. % 0.45/0.74 generalize (leq_antisym zenon_TX_ch). zenon_intro zenon_H63. % 0.45/0.74 generalize (zenon_H63 (v600)). zenon_intro zenon_Ha5. % 0.45/0.74 apply (zenon_imply_s _ _ zenon_Ha5); [ zenon_intro zenon_Ha6 | zenon_intro zenon_H5e ]. % 0.45/0.74 apply (zenon_notand_s _ _ zenon_Ha6); [ zenon_intro zenon_H3a | zenon_intro zenon_H44 ]. % 0.45/0.74 apply (zenon_L1_ zenon_TX_ch); trivial. % 0.45/0.74 apply (zenon_L2_ zenon_TX_ch); trivial. % 0.45/0.74 exact (zenon_H41 zenon_H5e). % 0.45/0.74 apply zenon_H61. apply refl_equal. % 0.45/0.74 apply zenon_H61. apply refl_equal. % 0.45/0.74 elim (classic ((v601) = (v601))); [ zenon_intro zenon_H60 | zenon_intro zenon_H61 ]. % 0.45/0.74 cut (((v601) = (v601)) = ((v600) = (v601))). % 0.45/0.74 intro zenon_D_pnotp. % 0.45/0.74 apply zenon_H5f. % 0.45/0.74 rewrite <- zenon_D_pnotp. % 0.45/0.74 exact zenon_H60. % 0.45/0.74 cut (((v601) = (v601))); [idtac | apply NNPP; zenon_intro zenon_H61]. % 0.45/0.74 cut (((v601) = (v600))); [idtac | apply NNPP; zenon_intro zenon_H62]. % 0.45/0.74 congruence. % 0.45/0.74 cut (((v601) = zenon_TX_ch) = ((v601) = (v600))). % 0.45/0.74 intro zenon_D_pnotp. % 0.45/0.74 apply zenon_H62. % 0.45/0.74 rewrite <- zenon_D_pnotp. % 0.45/0.74 exact zenon_Ha3. % 0.45/0.74 cut ((zenon_TX_ch = (v600))); [idtac | apply NNPP; zenon_intro zenon_H41]. % 0.45/0.74 cut (((v601) = (v601))); [idtac | apply NNPP; zenon_intro zenon_H61]. % 0.45/0.74 congruence. % 0.45/0.74 apply zenon_H61. apply refl_equal. % 0.45/0.74 apply zenon_H41. apply sym_equal. exact zenon_Ha4. % 0.45/0.74 apply zenon_H61. apply refl_equal. % 0.45/0.74 apply zenon_H61. apply refl_equal. % 0.45/0.74 elim (classic ((v601) = (v601))); [ zenon_intro zenon_H60 | zenon_intro zenon_H61 ]. % 0.45/0.74 cut (((v601) = (v601)) = ((v600) = (v601))). % 0.45/0.74 intro zenon_D_pnotp. % 0.45/0.74 apply zenon_H5f. % 0.45/0.74 rewrite <- zenon_D_pnotp. % 0.45/0.74 exact zenon_H60. % 0.45/0.74 cut (((v601) = (v601))); [idtac | apply NNPP; zenon_intro zenon_H61]. % 0.45/0.74 cut (((v601) = (v600))); [idtac | apply NNPP; zenon_intro zenon_H62]. % 0.45/0.74 congruence. % 0.45/0.74 cut (((v601) = zenon_TX_ch) = ((v601) = (v600))). % 0.45/0.74 intro zenon_D_pnotp. % 0.45/0.74 apply zenon_H62. % 0.45/0.74 rewrite <- zenon_D_pnotp. % 0.45/0.74 exact zenon_Ha3. % 0.45/0.74 cut ((zenon_TX_ch = (v600))); [idtac | apply NNPP; zenon_intro zenon_H41]. % 0.45/0.74 cut (((v601) = (v601))); [idtac | apply NNPP; zenon_intro zenon_H61]. % 0.45/0.74 congruence. % 0.45/0.74 apply zenon_H61. apply refl_equal. % 0.45/0.74 exact (zenon_H41 zenon_H5e). % 0.45/0.74 apply zenon_H61. apply refl_equal. % 0.45/0.74 apply zenon_H61. apply refl_equal. % 0.45/0.74 apply (zenon_or_s _ _ zenon_H3e); [ zenon_intro zenon_H39 | zenon_intro zenon_H5e ]. % 0.45/0.74 apply (zenon_or_s _ _ zenon_H47); [ zenon_intro zenon_H43 | zenon_intro zenon_Ha4 ]. % 0.45/0.74 cut ((zenon_TX_ch = (v601)) = ((v600) = (v601))). % 0.45/0.74 intro zenon_D_pnotp. % 0.45/0.74 apply zenon_H5f. % 0.45/0.74 rewrite <- zenon_D_pnotp. % 0.45/0.74 exact zenon_H65. % 0.45/0.74 cut (((v601) = (v601))); [idtac | apply NNPP; zenon_intro zenon_H61]. % 0.45/0.74 cut ((zenon_TX_ch = (v600))); [idtac | apply NNPP; zenon_intro zenon_H41]. % 0.45/0.74 congruence. % 0.45/0.74 elim (classic ((v600) = (v600))); [ zenon_intro zenon_Ha7 | zenon_intro zenon_H5d ]. % 0.45/0.74 cut (((v600) = (v600)) = (zenon_TX_ch = (v600))). % 0.45/0.74 intro zenon_D_pnotp. % 0.45/0.74 apply zenon_H41. % 0.45/0.74 rewrite <- zenon_D_pnotp. % 0.45/0.74 exact zenon_Ha7. % 0.45/0.74 cut (((v600) = (v600))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 0.45/0.74 cut (((v600) = zenon_TX_ch)); [idtac | apply NNPP; zenon_intro zenon_H4a]. % 0.45/0.74 congruence. % 0.45/0.74 generalize (leq_antisym zenon_TX_ch). zenon_intro zenon_H63. % 0.45/0.74 generalize (zenon_H63 (v600)). zenon_intro zenon_Ha5. % 0.45/0.74 apply (zenon_imply_s _ _ zenon_Ha5); [ zenon_intro zenon_Ha6 | zenon_intro zenon_H5e ]. % 0.45/0.74 apply (zenon_notand_s _ _ zenon_Ha6); [ zenon_intro zenon_H3a | zenon_intro zenon_H44 ]. % 0.45/0.74 apply (zenon_L1_ zenon_TX_ch); trivial. % 0.45/0.74 apply (zenon_L2_ zenon_TX_ch); trivial. % 0.45/0.74 apply zenon_H4a. apply sym_equal. exact zenon_H5e. % 0.45/0.74 apply zenon_H5d. apply refl_equal. % 0.45/0.74 apply zenon_H5d. apply refl_equal. % 0.45/0.74 apply zenon_H61. apply refl_equal. % 0.45/0.74 cut ((zenon_TX_ch = (v601)) = ((v600) = (v601))). % 0.45/0.74 intro zenon_D_pnotp. % 0.45/0.74 apply zenon_H5f. % 0.45/0.74 rewrite <- zenon_D_pnotp. % 0.45/0.74 exact zenon_H65. % 0.45/0.74 cut (((v601) = (v601))); [idtac | apply NNPP; zenon_intro zenon_H61]. % 0.45/0.74 cut ((zenon_TX_ch = (v600))); [idtac | apply NNPP; zenon_intro zenon_H41]. % 0.45/0.74 congruence. % 0.45/0.74 elim (classic ((v600) = (v600))); [ zenon_intro zenon_Ha7 | zenon_intro zenon_H5d ]. % 0.45/0.74 cut (((v600) = (v600)) = (zenon_TX_ch = (v600))). % 0.45/0.74 intro zenon_D_pnotp. % 0.45/0.74 apply zenon_H41. % 0.45/0.74 rewrite <- zenon_D_pnotp. % 0.45/0.74 exact zenon_Ha7. % 0.45/0.74 cut (((v600) = (v600))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 0.45/0.74 cut (((v600) = zenon_TX_ch)); [idtac | apply NNPP; zenon_intro zenon_H4a]. % 0.45/0.74 congruence. % 0.45/0.74 exact (zenon_H4a zenon_Ha4). % 0.45/0.74 apply zenon_H5d. apply refl_equal. % 0.45/0.74 apply zenon_H5d. apply refl_equal. % 0.45/0.74 apply zenon_H61. apply refl_equal. % 0.45/0.74 cut ((zenon_TX_ch = (v601)) = ((v600) = (v601))). % 0.45/0.74 intro zenon_D_pnotp. % 0.45/0.74 apply zenon_H5f. % 0.45/0.74 rewrite <- zenon_D_pnotp. % 0.45/0.74 exact zenon_H65. % 0.45/0.74 cut (((v601) = (v601))); [idtac | apply NNPP; zenon_intro zenon_H61]. % 0.45/0.74 cut ((zenon_TX_ch = (v600))); [idtac | apply NNPP; zenon_intro zenon_H41]. % 0.45/0.74 congruence. % 0.45/0.74 exact (zenon_H41 zenon_H5e). % 0.45/0.74 apply zenon_H61. apply refl_equal. % 0.45/0.74 Qed. % 0.45/0.74 % SZS output end Proof % 0.45/0.74 (* END-PROOF *) % 0.45/0.74 nodes searched: 35331 % 0.45/0.74 max branch formulas: 1249 % 0.45/0.74 proof nodes created: 658 % 0.45/0.74 formulas created: 29748 % 0.45/0.74 %------------------------------------------------------------------------------