%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT080+1 : TPTP v9.3.1. Bugfixed v9.3.1. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n028.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.64s 1.02s % Output : Proof 0.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT080+1 : TPTP v9.3.1. Bugfixed v9.3.1. % 0.00/0.03 % Command : run_zenon %s %d % 0.07/0.34 % Computer : n028.cluster.edu % 0.07/0.34 % Model : x86_64 x86_64 % 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.34 % Memory : 8046.5625MB % 0.07/0.34 % OS : Linux 6.8.0-71-generic % 0.07/0.34 % CPULimit : 300 % 0.07/0.34 % WCLimit : 300 % 0.07/0.34 % DateTime : Mon Sep 7 14:17:47 UTC 2026 % 0.07/0.34 % CPUTime : % 0.64/1.02 (* PROOF-FOUND *) % 0.64/1.02 % SZS status Theorem % 0.64/1.02 (* BEGIN-PROOF *) % 0.64/1.02 % SZS output start Proof % 0.64/1.02 Theorem odrl365 : (~(exists X : zenon_U, (exists Y : zenon_U, (exists Z : zenon_U, (exists W : zenon_U, ((in_closed X (v600) (v600))/\((in_closed X (v800) (v800))/\((less (v100) Y)/\((in_open Y (v0) (v500))/\((leq (v8) Z)/\((in_lopen Z (v0) (v32))/\((in_lopen W (v0) (v300))/\(leq (v150) W))))))))))))). % 0.64/1.02 Proof. % 0.64/1.02 assert (zenon_L1_ : forall (zenon_TX_da : zenon_U), (less zenon_TX_da (v600)) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((less x y)->((less y z)->(less x z)))))) -> (~(less zenon_TX_da zenon_TX_da)) -> (less (v600) zenon_TX_da) -> False). % 0.64/1.02 do 1 intro. intros zenon_H4a zenon_H4b zenon_H4c zenon_H4d. % 0.64/1.02 elim (classic ((~(zenon_TX_da = (v600)))/\(~(less zenon_TX_da (v600))))); [ zenon_intro zenon_H4f | zenon_intro zenon_H50 ]. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H4f). zenon_intro zenon_H52. zenon_intro zenon_H51. % 0.64/1.02 exact (zenon_H51 zenon_H4a). % 0.64/1.02 cut ((less (v600) zenon_TX_da) = (less zenon_TX_da zenon_TX_da)). % 0.64/1.02 intro zenon_D_pnotp. % 0.64/1.02 apply zenon_H4c. % 0.64/1.02 rewrite <- zenon_D_pnotp. % 0.64/1.02 exact zenon_H4d. % 0.64/1.02 cut ((zenon_TX_da = zenon_TX_da)); [idtac | apply NNPP; zenon_intro zenon_H53]. % 0.64/1.02 cut (((v600) = zenon_TX_da)); [idtac | apply NNPP; zenon_intro zenon_H54]. % 0.64/1.02 congruence. % 0.64/1.02 apply (zenon_notand_s _ _ zenon_H50); [ zenon_intro zenon_H56 | zenon_intro zenon_H55 ]. % 0.64/1.02 apply zenon_H56. zenon_intro zenon_H57. % 0.64/1.02 elim (classic (zenon_TX_da = zenon_TX_da)); [ zenon_intro zenon_H58 | zenon_intro zenon_H53 ]. % 0.64/1.02 cut ((zenon_TX_da = zenon_TX_da) = ((v600) = zenon_TX_da)). % 0.64/1.02 intro zenon_D_pnotp. % 0.64/1.02 apply zenon_H54. % 0.64/1.02 rewrite <- zenon_D_pnotp. % 0.64/1.02 exact zenon_H58. % 0.64/1.02 cut ((zenon_TX_da = zenon_TX_da)); [idtac | apply NNPP; zenon_intro zenon_H53]. % 0.64/1.02 cut ((zenon_TX_da = (v600))); [idtac | apply NNPP; zenon_intro zenon_H52]. % 0.64/1.02 congruence. % 0.64/1.02 exact (zenon_H52 zenon_H57). % 0.64/1.02 apply zenon_H53. apply refl_equal. % 0.64/1.02 apply zenon_H53. apply refl_equal. % 0.64/1.02 apply zenon_H55. zenon_intro zenon_H4a. % 0.64/1.02 generalize (zenon_H4b zenon_TX_da). zenon_intro zenon_H59. % 0.64/1.02 generalize (zenon_H59 (v600)). zenon_intro zenon_H5a. % 0.64/1.02 generalize (zenon_H5a zenon_TX_da). zenon_intro zenon_H5b. % 0.64/1.02 apply (zenon_imply_s _ _ zenon_H5b); [ zenon_intro zenon_H51 | zenon_intro zenon_H5c ]. % 0.64/1.02 exact (zenon_H51 zenon_H4a). % 0.64/1.02 apply (zenon_imply_s _ _ zenon_H5c); [ zenon_intro zenon_H5e | zenon_intro zenon_H5d ]. % 0.64/1.02 exact (zenon_H5e zenon_H4d). % 0.64/1.02 exact (zenon_H4c zenon_H5d). % 0.64/1.02 apply zenon_H53. apply refl_equal. % 0.64/1.02 (* end of lemma zenon_L1_ *) % 0.64/1.02 assert (zenon_L2_ : forall (zenon_TX_da : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((less x y)->((less y z)->(less x z)))))) -> (less zenon_TX_da (v600)) -> (less (v600) zenon_TX_da) -> False). % 0.64/1.02 do 1 intro. intros zenon_H4b zenon_H4a zenon_H4d. % 0.64/1.02 generalize (irreflexive zenon_TX_da). zenon_intro zenon_H4c. % 0.64/1.02 apply (zenon_L1_ zenon_TX_da); trivial. % 0.64/1.02 (* end of lemma zenon_L2_ *) % 0.64/1.02 assert (zenon_L3_ : (~((v800) = (v800))) -> False). % 0.64/1.02 do 0 intro. intros zenon_H5f. % 0.64/1.02 apply zenon_H5f. apply refl_equal. % 0.64/1.02 (* end of lemma zenon_L3_ *) % 0.64/1.02 apply NNPP. intro zenon_G. % 0.64/1.02 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((less x y)->((less y z)->(less x z))))))); [ zenon_intro zenon_H4b | zenon_intro zenon_H60 ]. % 0.64/1.02 apply (zenon_and_s _ _ distinct). zenon_intro zenon_H62. zenon_intro zenon_H61. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H61). zenon_intro zenon_H64. zenon_intro zenon_H63. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H63). zenon_intro zenon_H66. zenon_intro zenon_H65. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H65). zenon_intro zenon_H68. zenon_intro zenon_H67. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H67). zenon_intro zenon_H6a. zenon_intro zenon_H69. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H69). zenon_intro zenon_H6c. zenon_intro zenon_H6b. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H6b). zenon_intro zenon_H6e. zenon_intro zenon_H6d. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H6d). zenon_intro zenon_H70. zenon_intro zenon_H6f. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H6f). zenon_intro zenon_H72. zenon_intro zenon_H71. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H71). zenon_intro zenon_H74. zenon_intro zenon_H73. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H73). zenon_intro zenon_H76. zenon_intro zenon_H75. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H75). zenon_intro zenon_H78. zenon_intro zenon_H77. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H77). zenon_intro zenon_H7a. zenon_intro zenon_H79. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H79). zenon_intro zenon_H7c. zenon_intro zenon_H7b. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H7b). zenon_intro zenon_H7e. zenon_intro zenon_H7d. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H7d). zenon_intro zenon_H80. zenon_intro zenon_H7f. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H7f). zenon_intro zenon_H82. zenon_intro zenon_H81. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H81). zenon_intro zenon_H84. zenon_intro zenon_H83. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H83). zenon_intro zenon_H86. zenon_intro zenon_H85. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H85). zenon_intro zenon_H88. zenon_intro zenon_H87. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H87). zenon_intro zenon_H8a. zenon_intro zenon_H89. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H89). zenon_intro zenon_H8c. zenon_intro zenon_H8b. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H8b). zenon_intro zenon_H8e. zenon_intro zenon_H8d. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H8d). zenon_intro zenon_H90. zenon_intro zenon_H8f. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H8f). zenon_intro zenon_H92. zenon_intro zenon_H91. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H91). zenon_intro zenon_H94. zenon_intro zenon_H93. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H93). zenon_intro zenon_H96. zenon_intro zenon_H95. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H95). zenon_intro zenon_H98. zenon_intro zenon_H97. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H97). zenon_intro zenon_H9a. zenon_intro zenon_H99. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H99). zenon_intro zenon_H9c. zenon_intro zenon_H9b. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H9b). zenon_intro zenon_H9e. zenon_intro zenon_H9d. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H9d). zenon_intro zenon_Ha0. zenon_intro zenon_H9f. % 0.64/1.02 apply (zenon_and_s _ _ zenon_H9f). zenon_intro zenon_Ha2. zenon_intro zenon_Ha1. % 0.64/1.02 apply (zenon_and_s _ _ zenon_Ha1). zenon_intro zenon_Ha4. zenon_intro zenon_Ha3. % 0.64/1.02 apply (zenon_and_s _ _ zenon_Ha3). zenon_intro zenon_Ha6. zenon_intro zenon_Ha5. % 0.64/1.02 apply zenon_G. zenon_intro zenon_Ha7. % 0.64/1.02 elim zenon_Ha7. zenon_intro zenon_TX_da. zenon_intro zenon_Ha8. % 0.64/1.02 elim zenon_Ha8. zenon_intro zenon_TY_gn. zenon_intro zenon_Haa. % 0.64/1.02 elim zenon_Haa. zenon_intro zenon_TZ_gp. zenon_intro zenon_Hac. % 0.64/1.02 elim zenon_Hac. zenon_intro zenon_TW_gr. zenon_intro zenon_Hae. % 0.64/1.02 apply (zenon_and_s _ _ zenon_Hae). zenon_intro zenon_Hb0. zenon_intro zenon_Haf. % 0.64/1.02 apply (zenon_and_s _ _ zenon_Haf). zenon_intro zenon_Hb2. zenon_intro zenon_Hb1. % 0.64/1.02 generalize (in_closed zenon_TX_da). zenon_intro zenon_Hb3. % 0.64/1.02 generalize (zenon_Hb3 (v600)). zenon_intro zenon_Hb4. % 0.64/1.02 generalize (zenon_Hb4 (v600)). zenon_intro zenon_Hb5. % 0.64/1.02 apply (zenon_equiv_s _ _ zenon_Hb5); [ zenon_intro zenon_Hb8; zenon_intro zenon_Hb7 | zenon_intro zenon_Hb0; zenon_intro zenon_Hb6 ]. % 0.64/1.02 exact (zenon_Hb8 zenon_Hb0). % 0.64/1.02 apply (zenon_and_s _ _ zenon_Hb6). zenon_intro zenon_Hba. zenon_intro zenon_Hb9. % 0.64/1.02 generalize (leq_def (v600)). zenon_intro zenon_Hbb. % 0.64/1.02 generalize (zenon_Hbb zenon_TX_da). zenon_intro zenon_Hbc. % 0.64/1.02 apply (zenon_equiv_s _ _ zenon_Hbc); [ zenon_intro zenon_Hbf; zenon_intro zenon_Hbe | zenon_intro zenon_Hba; zenon_intro zenon_Hbd ]. % 0.64/1.02 exact (zenon_Hbf zenon_Hba). % 0.64/1.02 generalize (leq_def zenon_TX_da). zenon_intro zenon_Hc0. % 0.64/1.02 generalize (zenon_Hc0 (v600)). zenon_intro zenon_Hc1. % 0.64/1.02 apply (zenon_equiv_s _ _ zenon_Hc1); [ zenon_intro zenon_Hc4; zenon_intro zenon_Hc3 | zenon_intro zenon_Hb9; zenon_intro zenon_Hc2 ]. % 0.64/1.02 exact (zenon_Hc4 zenon_Hb9). % 0.64/1.02 generalize (in_closed zenon_TX_da). zenon_intro zenon_Hb3. % 0.64/1.02 generalize (zenon_Hb3 (v800)). zenon_intro zenon_Hc5. % 0.64/1.02 generalize (zenon_Hc5 (v800)). zenon_intro zenon_Hc6. % 0.64/1.02 apply (zenon_equiv_s _ _ zenon_Hc6); [ zenon_intro zenon_Hc9; zenon_intro zenon_Hc8 | zenon_intro zenon_Hb2; zenon_intro zenon_Hc7 ]. % 0.64/1.02 exact (zenon_Hc9 zenon_Hb2). % 0.64/1.02 apply (zenon_and_s _ _ zenon_Hc7). zenon_intro zenon_Hcb. zenon_intro zenon_Hca. % 0.64/1.02 generalize (leq_def (v800)). zenon_intro zenon_Hcc. % 0.64/1.02 generalize (zenon_Hcc zenon_TX_da). zenon_intro zenon_Hcd. % 0.64/1.02 apply (zenon_equiv_s _ _ zenon_Hcd); [ zenon_intro zenon_Hd0; zenon_intro zenon_Hcf | zenon_intro zenon_Hcb; zenon_intro zenon_Hce ]. % 0.64/1.02 exact (zenon_Hd0 zenon_Hcb). % 0.64/1.02 generalize (leq_def zenon_TX_da). zenon_intro zenon_Hc0. % 0.64/1.02 generalize (zenon_Hc0 (v800)). zenon_intro zenon_Hd1. % 0.64/1.02 apply (zenon_equiv_s _ _ zenon_Hd1); [ zenon_intro zenon_Hd4; zenon_intro zenon_Hd3 | zenon_intro zenon_Hca; zenon_intro zenon_Hd2 ]. % 0.64/1.02 exact (zenon_Hd4 zenon_Hca). % 0.64/1.02 apply (zenon_or_s _ _ zenon_Hd2); [ zenon_intro zenon_Hd6 | zenon_intro zenon_Hd5 ]. % 0.64/1.02 apply (zenon_or_s _ _ zenon_Hce); [ zenon_intro zenon_Hd8 | zenon_intro zenon_Hd7 ]. % 0.64/1.02 generalize (irreflexive zenon_TX_da). zenon_intro zenon_H4c. % 0.64/1.02 elim (classic ((~(zenon_TX_da = (v800)))/\(~(less zenon_TX_da (v800))))); [ zenon_intro zenon_Hd9 | zenon_intro zenon_Hda ]. % 0.64/1.02 apply (zenon_and_s _ _ zenon_Hd9). zenon_intro zenon_Hdc. zenon_intro zenon_Hdb. % 0.64/1.02 exact (zenon_Hdb zenon_Hd6). % 0.64/1.02 cut ((less (v800) zenon_TX_da) = (less zenon_TX_da zenon_TX_da)). % 0.64/1.02 intro zenon_D_pnotp. % 0.64/1.02 apply zenon_H4c. % 0.64/1.02 rewrite <- zenon_D_pnotp. % 0.64/1.02 exact zenon_Hd8. % 0.64/1.02 cut ((zenon_TX_da = zenon_TX_da)); [idtac | apply NNPP; zenon_intro zenon_H53]. % 0.64/1.02 cut (((v800) = zenon_TX_da)); [idtac | apply NNPP; zenon_intro zenon_Hdd]. % 0.64/1.02 congruence. % 0.64/1.02 apply (zenon_notand_s _ _ zenon_Hda); [ zenon_intro zenon_Hdf | zenon_intro zenon_Hde ]. % 0.64/1.02 apply zenon_Hdf. zenon_intro zenon_Hd5. % 0.64/1.02 elim (classic (zenon_TX_da = zenon_TX_da)); [ zenon_intro zenon_H58 | zenon_intro zenon_H53 ]. % 0.64/1.02 cut ((zenon_TX_da = zenon_TX_da) = ((v800) = zenon_TX_da)). % 0.64/1.02 intro zenon_D_pnotp. % 0.64/1.02 apply zenon_Hdd. % 0.64/1.02 rewrite <- zenon_D_pnotp. % 0.64/1.02 exact zenon_H58. % 0.64/1.02 cut ((zenon_TX_da = zenon_TX_da)); [idtac | apply NNPP; zenon_intro zenon_H53]. % 0.64/1.02 cut ((zenon_TX_da = (v800))); [idtac | apply NNPP; zenon_intro zenon_Hdc]. % 0.64/1.02 congruence. % 0.64/1.02 exact (zenon_Hdc zenon_Hd5). % 0.64/1.02 apply zenon_H53. apply refl_equal. % 0.64/1.02 apply zenon_H53. apply refl_equal. % 0.64/1.02 apply zenon_Hde. zenon_intro zenon_Hd6. % 0.64/1.02 generalize (zenon_H4b zenon_TX_da). zenon_intro zenon_H59. % 0.64/1.02 generalize (zenon_H59 (v800)). zenon_intro zenon_He0. % 0.64/1.02 generalize (zenon_He0 zenon_TX_da). zenon_intro zenon_He1. % 0.64/1.02 apply (zenon_imply_s _ _ zenon_He1); [ zenon_intro zenon_Hdb | zenon_intro zenon_He2 ]. % 0.64/1.02 exact (zenon_Hdb zenon_Hd6). % 0.64/1.02 apply (zenon_imply_s _ _ zenon_He2); [ zenon_intro zenon_He3 | zenon_intro zenon_H5d ]. % 0.64/1.02 exact (zenon_He3 zenon_Hd8). % 0.64/1.02 exact (zenon_H4c zenon_H5d). % 0.64/1.02 apply zenon_H53. apply refl_equal. % 0.64/1.02 apply (zenon_or_s _ _ zenon_Hc2); [ zenon_intro zenon_H4a | zenon_intro zenon_H57 ]. % 0.64/1.02 apply (zenon_or_s _ _ zenon_Hbd); [ zenon_intro zenon_H4d | zenon_intro zenon_He4 ]. % 0.64/1.02 apply (zenon_L2_ zenon_TX_da); trivial. % 0.64/1.02 elim (classic ((v800) = (v800))); [ zenon_intro zenon_He5 | zenon_intro zenon_H5f ]. % 0.64/1.02 cut (((v800) = (v800)) = ((v600) = (v800))). % 0.64/1.02 intro zenon_D_pnotp. % 0.64/1.02 apply zenon_Ha5. % 0.64/1.02 rewrite <- zenon_D_pnotp. % 0.64/1.02 exact zenon_He5. % 0.64/1.02 cut (((v800) = (v800))); [idtac | apply NNPP; zenon_intro zenon_H5f]. % 0.64/1.02 cut (((v800) = (v600))); [idtac | apply NNPP; zenon_intro zenon_He6]. % 0.64/1.02 congruence. % 0.64/1.02 cut (((v800) = zenon_TX_da) = ((v800) = (v600))). % 0.64/1.02 intro zenon_D_pnotp. % 0.64/1.02 apply zenon_He6. % 0.64/1.02 rewrite <- zenon_D_pnotp. % 0.64/1.02 exact zenon_Hd7. % 0.64/1.02 cut ((zenon_TX_da = (v600))); [idtac | apply NNPP; zenon_intro zenon_H52]. % 0.64/1.02 cut (((v800) = (v800))); [idtac | apply NNPP; zenon_intro zenon_H5f]. % 0.64/1.02 congruence. % 0.64/1.02 apply zenon_H5f. apply refl_equal. % 0.64/1.02 apply zenon_H52. apply sym_equal. exact zenon_He4. % 0.64/1.02 apply zenon_H5f. apply refl_equal. % 0.64/1.02 apply zenon_H5f. apply refl_equal. % 0.64/1.02 elim (classic ((v800) = (v800))); [ zenon_intro zenon_He5 | zenon_intro zenon_H5f ]. % 0.64/1.02 cut (((v800) = (v800)) = ((v600) = (v800))). % 0.64/1.02 intro zenon_D_pnotp. % 0.64/1.02 apply zenon_Ha5. % 0.64/1.02 rewrite <- zenon_D_pnotp. % 0.64/1.02 exact zenon_He5. % 0.64/1.02 cut (((v800) = (v800))); [idtac | apply NNPP; zenon_intro zenon_H5f]. % 0.64/1.02 cut (((v800) = (v600))); [idtac | apply NNPP; zenon_intro zenon_He6]. % 0.64/1.02 congruence. % 0.64/1.02 cut (((v800) = zenon_TX_da) = ((v800) = (v600))). % 0.64/1.02 intro zenon_D_pnotp. % 0.64/1.02 apply zenon_He6. % 0.64/1.02 rewrite <- zenon_D_pnotp. % 0.64/1.02 exact zenon_Hd7. % 0.64/1.02 cut ((zenon_TX_da = (v600))); [idtac | apply NNPP; zenon_intro zenon_H52]. % 0.64/1.02 cut (((v800) = (v800))); [idtac | apply NNPP; zenon_intro zenon_H5f]. % 0.64/1.02 congruence. % 0.64/1.02 apply zenon_H5f. apply refl_equal. % 0.64/1.02 exact (zenon_H52 zenon_H57). % 0.64/1.02 apply zenon_H5f. apply refl_equal. % 0.64/1.02 apply zenon_H5f. apply refl_equal. % 0.64/1.02 apply (zenon_or_s _ _ zenon_Hc2); [ zenon_intro zenon_H4a | zenon_intro zenon_H57 ]. % 0.64/1.02 apply (zenon_or_s _ _ zenon_Hbd); [ zenon_intro zenon_H4d | zenon_intro zenon_He4 ]. % 0.64/1.02 apply (zenon_L2_ zenon_TX_da); trivial. % 0.64/1.02 cut ((zenon_TX_da = (v800)) = ((v600) = (v800))). % 0.64/1.02 intro zenon_D_pnotp. % 0.64/1.02 apply zenon_Ha5. % 0.64/1.02 rewrite <- zenon_D_pnotp. % 0.64/1.02 exact zenon_Hd5. % 0.64/1.02 cut (((v800) = (v800))); [idtac | apply NNPP; zenon_intro zenon_H5f]. % 0.64/1.02 cut ((zenon_TX_da = (v600))); [idtac | apply NNPP; zenon_intro zenon_H52]. % 0.64/1.02 congruence. % 0.64/1.02 elim (classic ((v600) = (v600))); [ zenon_intro zenon_He7 | zenon_intro zenon_He8 ]. % 0.64/1.02 cut (((v600) = (v600)) = (zenon_TX_da = (v600))). % 0.64/1.02 intro zenon_D_pnotp. % 0.64/1.02 apply zenon_H52. % 0.64/1.02 rewrite <- zenon_D_pnotp. % 0.64/1.02 exact zenon_He7. % 0.64/1.02 cut (((v600) = (v600))); [idtac | apply NNPP; zenon_intro zenon_He8]. % 0.64/1.02 cut (((v600) = zenon_TX_da)); [idtac | apply NNPP; zenon_intro zenon_H54]. % 0.64/1.02 congruence. % 0.64/1.02 exact (zenon_H54 zenon_He4). % 0.64/1.02 apply zenon_He8. apply refl_equal. % 0.64/1.02 apply zenon_He8. apply refl_equal. % 0.64/1.02 apply zenon_H5f. apply refl_equal. % 0.64/1.02 cut ((zenon_TX_da = (v800)) = ((v600) = (v800))). % 0.64/1.02 intro zenon_D_pnotp. % 0.64/1.02 apply zenon_Ha5. % 0.64/1.02 rewrite <- zenon_D_pnotp. % 0.64/1.02 exact zenon_Hd5. % 0.64/1.02 cut (((v800) = (v800))); [idtac | apply NNPP; zenon_intro zenon_H5f]. % 0.64/1.02 cut ((zenon_TX_da = (v600))); [idtac | apply NNPP; zenon_intro zenon_H52]. % 0.64/1.02 congruence. % 0.64/1.02 exact (zenon_H52 zenon_H57). % 0.64/1.02 apply zenon_H5f. apply refl_equal. % 0.64/1.02 apply zenon_H60. zenon_intro zenon_Tx_iz. apply NNPP. zenon_intro zenon_Hea. % 0.64/1.02 apply zenon_Hea. zenon_intro zenon_Ty_jb. apply NNPP. zenon_intro zenon_Hec. % 0.64/1.02 apply zenon_Hec. zenon_intro zenon_Tz_jd. apply NNPP. zenon_intro zenon_Hee. % 0.64/1.02 apply (zenon_notimply_s _ _ zenon_Hee). zenon_intro zenon_Hf0. zenon_intro zenon_Hef. % 0.64/1.02 apply (zenon_notimply_s _ _ zenon_Hef). zenon_intro zenon_Hf2. zenon_intro zenon_Hf1. % 0.64/1.02 generalize (transitive zenon_Tx_iz). zenon_intro zenon_Hf3. % 0.64/1.02 generalize (zenon_Hf3 zenon_Ty_jb). zenon_intro zenon_Hf4. % 0.64/1.02 generalize (zenon_Hf4 zenon_Tz_jd). zenon_intro zenon_Hf5. % 0.64/1.02 apply (zenon_imply_s _ _ zenon_Hf5); [ zenon_intro zenon_Hf7 | zenon_intro zenon_Hf6 ]. % 0.64/1.02 apply (zenon_notand_s _ _ zenon_Hf7); [ zenon_intro zenon_Hf9 | zenon_intro zenon_Hf8 ]. % 0.64/1.02 exact (zenon_Hf9 zenon_Hf0). % 0.64/1.02 exact (zenon_Hf8 zenon_Hf2). % 0.64/1.02 exact (zenon_Hf1 zenon_Hf6). % 0.64/1.02 Qed. % 0.64/1.02 % SZS output end Proof % 0.64/1.02 (* END-PROOF *) % 0.64/1.02 nodes searched: 21962 % 0.64/1.02 max branch formulas: 1329 % 0.64/1.02 proof nodes created: 414 % 0.64/1.02 formulas created: 25782 % 0.64/1.02 %------------------------------------------------------------------------------