%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT078+1 : TPTP v9.3.1. Bugfixed v9.3.1. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n006.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:26 AM UTC 2026 % Result : Theorem 0.19s 0.48s % Output : Proof 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT078+1 : TPTP v9.3.1. Bugfixed v9.3.1. % 0.00/0.04 % Command : run_zenon %s %d % 0.02/0.35 % Computer : n006.cluster.edu % 0.02/0.35 % Model : x86_64 x86_64 % 0.02/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.02/0.35 % Memory : 8046.5625MB % 0.02/0.35 % OS : Linux 6.8.0-71-generic % 0.02/0.35 % CPULimit : 300 % 0.02/0.36 % WCLimit : 300 % 0.02/0.36 % DateTime : Mon Sep 7 14:13:31 UTC 2026 % 0.02/0.36 % CPUTime : % 0.19/0.48 (* PROOF-FOUND *) % 0.19/0.48 % SZS status Theorem % 0.19/0.48 (* BEGIN-PROOF *) % 0.19/0.48 % SZS output start Proof % 0.19/0.48 Theorem odrl341 : (~(exists X : zenon_U, (exists Y : zenon_U, (exists Z : zenon_U, ((in_lopen X (v0) (v600))/\((leq (v1200) X)/\((in_lopen Y (v0) (v800))/\((leq (v200) Y)/\((in_lopen Z (v0) (v32))/\(leq (v8) Z)))))))))). % 0.19/0.48 Proof. % 0.19/0.48 assert (zenon_L1_ : (~((v800) = (v800))) -> False). % 0.19/0.48 do 0 intro. intros zenon_H39. % 0.19/0.48 apply zenon_H39. apply refl_equal. % 0.19/0.48 (* end of lemma zenon_L1_ *) % 0.19/0.48 assert (zenon_L2_ : (~((v1200) = (v1200))) -> False). % 0.19/0.48 do 0 intro. intros zenon_H3a. % 0.19/0.48 apply zenon_H3a. apply refl_equal. % 0.19/0.48 (* end of lemma zenon_L2_ *) % 0.19/0.48 assert (zenon_L3_ : (~((v600) = (v600))) -> False). % 0.19/0.48 do 0 intro. intros zenon_H3b. % 0.19/0.48 apply zenon_H3b. apply refl_equal. % 0.19/0.48 (* end of lemma zenon_L3_ *) % 0.19/0.48 assert (zenon_L4_ : forall (zenon_TX_cm : 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_cm zenon_TX_cm)) -> (less zenon_TX_cm (v600)) -> ((v1200) = zenon_TX_cm) -> False). % 0.19/0.48 do 1 intro. intros zenon_H3c zenon_H3d zenon_H3e zenon_H3f. % 0.19/0.48 elim (classic (less (v600) zenon_TX_cm)); [ zenon_intro zenon_H41 | zenon_intro zenon_H42 ]. % 0.19/0.48 generalize (zenon_H3c zenon_TX_cm). zenon_intro zenon_H43. % 0.19/0.48 generalize (zenon_H43 (v600)). zenon_intro zenon_H44. % 0.19/0.48 generalize (zenon_H44 zenon_TX_cm). zenon_intro zenon_H45. % 0.19/0.48 apply (zenon_imply_s _ _ zenon_H45); [ zenon_intro zenon_H47 | zenon_intro zenon_H46 ]. % 0.19/0.48 exact (zenon_H47 zenon_H3e). % 0.19/0.48 apply (zenon_imply_s _ _ zenon_H46); [ zenon_intro zenon_H42 | zenon_intro zenon_H48 ]. % 0.19/0.48 exact (zenon_H42 zenon_H41). % 0.19/0.48 exact (zenon_H3d zenon_H48). % 0.19/0.48 cut ((less (v600) (v1200)) = (less (v600) zenon_TX_cm)). % 0.19/0.48 intro zenon_D_pnotp. % 0.19/0.48 apply zenon_H42. % 0.19/0.48 rewrite <- zenon_D_pnotp. % 0.19/0.48 exact ord_v600_v1200. % 0.19/0.48 cut (((v1200) = zenon_TX_cm)); [idtac | apply NNPP; zenon_intro zenon_H49]. % 0.19/0.48 cut (((v600) = (v600))); [idtac | apply NNPP; zenon_intro zenon_H3b]. % 0.19/0.48 congruence. % 0.19/0.48 apply zenon_H3b. apply refl_equal. % 0.19/0.48 exact (zenon_H49 zenon_H3f). % 0.19/0.48 (* end of lemma zenon_L4_ *) % 0.19/0.48 apply NNPP. intro zenon_G. % 0.19/0.48 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_H3c | zenon_intro zenon_H4a ]. % 0.19/0.48 apply (zenon_and_s _ _ distinct). zenon_intro zenon_H4c. zenon_intro zenon_H4b. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H4b). zenon_intro zenon_H4e. zenon_intro zenon_H4d. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H4d). zenon_intro zenon_H50. zenon_intro zenon_H4f. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H4f). zenon_intro zenon_H52. zenon_intro zenon_H51. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H51). zenon_intro zenon_H54. zenon_intro zenon_H53. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H53). zenon_intro zenon_H56. zenon_intro zenon_H55. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H55). zenon_intro zenon_H58. zenon_intro zenon_H57. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H57). zenon_intro zenon_H5a. zenon_intro zenon_H59. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H59). zenon_intro zenon_H5c. zenon_intro zenon_H5b. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H5b). zenon_intro zenon_H5e. zenon_intro zenon_H5d. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H5d). zenon_intro zenon_H60. zenon_intro zenon_H5f. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H5f). zenon_intro zenon_H62. zenon_intro zenon_H61. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H61). zenon_intro zenon_H64. zenon_intro zenon_H63. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H63). zenon_intro zenon_H66. zenon_intro zenon_H65. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H65). zenon_intro zenon_H68. zenon_intro zenon_H67. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H67). zenon_intro zenon_H6a. zenon_intro zenon_H69. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H69). zenon_intro zenon_H6c. zenon_intro zenon_H6b. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H6b). zenon_intro zenon_H6e. zenon_intro zenon_H6d. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H6d). zenon_intro zenon_H70. zenon_intro zenon_H6f. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H6f). zenon_intro zenon_H72. zenon_intro zenon_H71. % 0.19/0.48 apply zenon_G. zenon_intro zenon_H73. % 0.19/0.48 elim zenon_H73. zenon_intro zenon_TX_cm. zenon_intro zenon_H74. % 0.19/0.48 elim zenon_H74. zenon_intro zenon_TY_en. zenon_intro zenon_H76. % 0.19/0.48 elim zenon_H76. zenon_intro zenon_TZ_ep. zenon_intro zenon_H78. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H78). zenon_intro zenon_H7a. zenon_intro zenon_H79. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H79). zenon_intro zenon_H7c. zenon_intro zenon_H7b. % 0.19/0.48 generalize (in_lopen zenon_TX_cm). zenon_intro zenon_H7d. % 0.19/0.48 generalize (zenon_H7d (v0)). zenon_intro zenon_H7e. % 0.19/0.48 generalize (zenon_H7e (v600)). zenon_intro zenon_H7f. % 0.19/0.48 apply (zenon_equiv_s _ _ zenon_H7f); [ zenon_intro zenon_H82; zenon_intro zenon_H81 | zenon_intro zenon_H7a; zenon_intro zenon_H80 ]. % 0.19/0.48 exact (zenon_H82 zenon_H7a). % 0.19/0.48 apply (zenon_and_s _ _ zenon_H80). zenon_intro zenon_H84. zenon_intro zenon_H83. % 0.19/0.48 generalize (leq_def zenon_TX_cm). zenon_intro zenon_H85. % 0.19/0.48 generalize (zenon_H85 (v600)). zenon_intro zenon_H86. % 0.19/0.48 apply (zenon_equiv_s _ _ zenon_H86); [ zenon_intro zenon_H89; zenon_intro zenon_H88 | zenon_intro zenon_H83; zenon_intro zenon_H87 ]. % 0.19/0.48 exact (zenon_H89 zenon_H83). % 0.19/0.48 generalize (leq_def (v1200)). zenon_intro zenon_H8a. % 0.19/0.48 generalize (zenon_H8a zenon_TX_cm). zenon_intro zenon_H8b. % 0.19/0.48 apply (zenon_equiv_s _ _ zenon_H8b); [ zenon_intro zenon_H8e; zenon_intro zenon_H8d | zenon_intro zenon_H7c; zenon_intro zenon_H8c ]. % 0.19/0.48 exact (zenon_H8e zenon_H7c). % 0.19/0.48 apply (zenon_or_s _ _ zenon_H8c); [ zenon_intro zenon_H8f | zenon_intro zenon_H3f ]. % 0.19/0.48 apply (zenon_or_s _ _ zenon_H87); [ zenon_intro zenon_H3e | zenon_intro zenon_H90 ]. % 0.19/0.48 generalize (irreflexive zenon_TX_cm). zenon_intro zenon_H3d. % 0.19/0.48 elim (classic ((~(zenon_TX_cm = (v1200)))/\(~(less zenon_TX_cm (v1200))))); [ zenon_intro zenon_H91 | zenon_intro zenon_H92 ]. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H91). zenon_intro zenon_H94. zenon_intro zenon_H93. % 0.19/0.48 elim (classic ((~(zenon_TX_cm = (v800)))/\(~(less zenon_TX_cm (v800))))); [ zenon_intro zenon_H95 | zenon_intro zenon_H96 ]. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H95). zenon_intro zenon_H98. zenon_intro zenon_H97. % 0.19/0.48 elim (classic ((~(zenon_TX_cm = (v600)))/\(~(less zenon_TX_cm (v600))))); [ zenon_intro zenon_H99 | zenon_intro zenon_H9a ]. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H99). zenon_intro zenon_H9b. zenon_intro zenon_H47. % 0.19/0.48 exact (zenon_H47 zenon_H3e). % 0.19/0.48 cut ((less (v600) (v800)) = (less zenon_TX_cm (v800))). % 0.19/0.48 intro zenon_D_pnotp. % 0.19/0.48 apply zenon_H97. % 0.19/0.48 rewrite <- zenon_D_pnotp. % 0.19/0.48 exact ord_v600_v800. % 0.19/0.48 cut (((v800) = (v800))); [idtac | apply NNPP; zenon_intro zenon_H39]. % 0.19/0.48 cut (((v600) = zenon_TX_cm)); [idtac | apply NNPP; zenon_intro zenon_H9c]. % 0.19/0.48 congruence. % 0.19/0.48 apply (zenon_notand_s _ _ zenon_H9a); [ zenon_intro zenon_H9e | zenon_intro zenon_H9d ]. % 0.19/0.48 apply zenon_H9e. zenon_intro zenon_H90. % 0.19/0.48 elim (classic (zenon_TX_cm = zenon_TX_cm)); [ zenon_intro zenon_H9f | zenon_intro zenon_Ha0 ]. % 0.19/0.48 cut ((zenon_TX_cm = zenon_TX_cm) = ((v600) = zenon_TX_cm)). % 0.19/0.48 intro zenon_D_pnotp. % 0.19/0.48 apply zenon_H9c. % 0.19/0.48 rewrite <- zenon_D_pnotp. % 0.19/0.48 exact zenon_H9f. % 0.19/0.48 cut ((zenon_TX_cm = zenon_TX_cm)); [idtac | apply NNPP; zenon_intro zenon_Ha0]. % 0.19/0.48 cut ((zenon_TX_cm = (v600))); [idtac | apply NNPP; zenon_intro zenon_H9b]. % 0.19/0.48 congruence. % 0.19/0.48 exact (zenon_H9b zenon_H90). % 0.19/0.48 apply zenon_Ha0. apply refl_equal. % 0.19/0.48 apply zenon_Ha0. apply refl_equal. % 0.19/0.48 apply zenon_H9d. zenon_intro zenon_H3e. % 0.19/0.48 generalize (zenon_H3c zenon_TX_cm). zenon_intro zenon_H43. % 0.19/0.48 generalize (zenon_H43 (v600)). zenon_intro zenon_H44. % 0.19/0.48 generalize (zenon_H44 (v800)). zenon_intro zenon_Ha1. % 0.19/0.48 apply (zenon_imply_s _ _ zenon_Ha1); [ zenon_intro zenon_H47 | zenon_intro zenon_Ha2 ]. % 0.19/0.48 exact (zenon_H47 zenon_H3e). % 0.19/0.48 apply (zenon_imply_s _ _ zenon_Ha2); [ zenon_intro zenon_Ha4 | zenon_intro zenon_Ha3 ]. % 0.19/0.48 exact (zenon_Ha4 ord_v600_v800). % 0.19/0.48 exact (zenon_H97 zenon_Ha3). % 0.19/0.48 apply zenon_H39. apply refl_equal. % 0.19/0.48 cut ((less (v800) (v1200)) = (less zenon_TX_cm (v1200))). % 0.19/0.48 intro zenon_D_pnotp. % 0.19/0.48 apply zenon_H93. % 0.19/0.48 rewrite <- zenon_D_pnotp. % 0.19/0.48 exact ord_v800_v1200. % 0.19/0.48 cut (((v1200) = (v1200))); [idtac | apply NNPP; zenon_intro zenon_H3a]. % 0.19/0.48 cut (((v800) = zenon_TX_cm)); [idtac | apply NNPP; zenon_intro zenon_Ha5]. % 0.19/0.48 congruence. % 0.19/0.48 apply (zenon_notand_s _ _ zenon_H96); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Ha6 ]. % 0.19/0.48 apply zenon_Ha7. zenon_intro zenon_Ha8. % 0.19/0.48 elim (classic (zenon_TX_cm = zenon_TX_cm)); [ zenon_intro zenon_H9f | zenon_intro zenon_Ha0 ]. % 0.19/0.48 cut ((zenon_TX_cm = zenon_TX_cm) = ((v800) = zenon_TX_cm)). % 0.19/0.48 intro zenon_D_pnotp. % 0.19/0.48 apply zenon_Ha5. % 0.19/0.48 rewrite <- zenon_D_pnotp. % 0.19/0.48 exact zenon_H9f. % 0.19/0.48 cut ((zenon_TX_cm = zenon_TX_cm)); [idtac | apply NNPP; zenon_intro zenon_Ha0]. % 0.19/0.48 cut ((zenon_TX_cm = (v800))); [idtac | apply NNPP; zenon_intro zenon_H98]. % 0.19/0.48 congruence. % 0.19/0.48 exact (zenon_H98 zenon_Ha8). % 0.19/0.48 apply zenon_Ha0. apply refl_equal. % 0.19/0.48 apply zenon_Ha0. apply refl_equal. % 0.19/0.48 apply zenon_Ha6. zenon_intro zenon_Ha3. % 0.19/0.48 generalize (zenon_H3c zenon_TX_cm). zenon_intro zenon_H43. % 0.19/0.48 generalize (zenon_H43 (v800)). zenon_intro zenon_Ha9. % 0.19/0.48 generalize (zenon_Ha9 (v1200)). zenon_intro zenon_Haa. % 0.19/0.48 apply (zenon_imply_s _ _ zenon_Haa); [ zenon_intro zenon_H97 | zenon_intro zenon_Hab ]. % 0.19/0.48 exact (zenon_H97 zenon_Ha3). % 0.19/0.48 apply (zenon_imply_s _ _ zenon_Hab); [ zenon_intro zenon_Had | zenon_intro zenon_Hac ]. % 0.19/0.48 exact (zenon_Had ord_v800_v1200). % 0.19/0.48 exact (zenon_H93 zenon_Hac). % 0.19/0.48 apply zenon_H3a. apply refl_equal. % 0.19/0.48 cut ((less (v1200) zenon_TX_cm) = (less zenon_TX_cm zenon_TX_cm)). % 0.19/0.48 intro zenon_D_pnotp. % 0.19/0.48 apply zenon_H3d. % 0.19/0.48 rewrite <- zenon_D_pnotp. % 0.19/0.48 exact zenon_H8f. % 0.19/0.48 cut ((zenon_TX_cm = zenon_TX_cm)); [idtac | apply NNPP; zenon_intro zenon_Ha0]. % 0.19/0.48 cut (((v1200) = zenon_TX_cm)); [idtac | apply NNPP; zenon_intro zenon_H49]. % 0.19/0.48 congruence. % 0.19/0.48 apply (zenon_notand_s _ _ zenon_H92); [ zenon_intro zenon_Haf | zenon_intro zenon_Hae ]. % 0.19/0.48 apply zenon_Haf. zenon_intro zenon_Hb0. % 0.19/0.48 elim (classic (zenon_TX_cm = zenon_TX_cm)); [ zenon_intro zenon_H9f | zenon_intro zenon_Ha0 ]. % 0.19/0.48 cut ((zenon_TX_cm = zenon_TX_cm) = ((v1200) = zenon_TX_cm)). % 0.19/0.48 intro zenon_D_pnotp. % 0.19/0.48 apply zenon_H49. % 0.19/0.48 rewrite <- zenon_D_pnotp. % 0.19/0.48 exact zenon_H9f. % 0.19/0.48 cut ((zenon_TX_cm = zenon_TX_cm)); [idtac | apply NNPP; zenon_intro zenon_Ha0]. % 0.19/0.48 cut ((zenon_TX_cm = (v1200))); [idtac | apply NNPP; zenon_intro zenon_H94]. % 0.19/0.48 congruence. % 0.19/0.48 exact (zenon_H94 zenon_Hb0). % 0.19/0.48 apply zenon_Ha0. apply refl_equal. % 0.19/0.48 apply zenon_Ha0. apply refl_equal. % 0.19/0.48 apply zenon_Hae. zenon_intro zenon_Hac. % 0.19/0.48 generalize (zenon_H3c zenon_TX_cm). zenon_intro zenon_H43. % 0.19/0.48 generalize (zenon_H43 (v1200)). zenon_intro zenon_Hb1. % 0.19/0.48 generalize (zenon_Hb1 zenon_TX_cm). zenon_intro zenon_Hb2. % 0.19/0.48 apply (zenon_imply_s _ _ zenon_Hb2); [ zenon_intro zenon_H93 | zenon_intro zenon_Hb3 ]. % 0.19/0.48 exact (zenon_H93 zenon_Hac). % 0.19/0.48 apply (zenon_imply_s _ _ zenon_Hb3); [ zenon_intro zenon_Hb4 | zenon_intro zenon_H48 ]. % 0.19/0.48 exact (zenon_Hb4 zenon_H8f). % 0.19/0.48 exact (zenon_H3d zenon_H48). % 0.19/0.48 apply zenon_Ha0. apply refl_equal. % 0.19/0.48 generalize (irreflexive zenon_TX_cm). zenon_intro zenon_H3d. % 0.19/0.48 elim (classic ((~(zenon_TX_cm = (v1200)))/\(~(less zenon_TX_cm (v1200))))); [ zenon_intro zenon_H91 | zenon_intro zenon_H92 ]. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H91). zenon_intro zenon_H94. zenon_intro zenon_H93. % 0.19/0.48 elim (classic ((~(zenon_TX_cm = (v800)))/\(~(less zenon_TX_cm (v800))))); [ zenon_intro zenon_H95 | zenon_intro zenon_H96 ]. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H95). zenon_intro zenon_H98. zenon_intro zenon_H97. % 0.19/0.48 elim (classic ((~(zenon_TX_cm = (v600)))/\(~(less zenon_TX_cm (v600))))); [ zenon_intro zenon_H99 | zenon_intro zenon_H9a ]. % 0.19/0.48 apply (zenon_and_s _ _ zenon_H99). zenon_intro zenon_H9b. zenon_intro zenon_H47. % 0.19/0.48 exact (zenon_H9b zenon_H90). % 0.19/0.48 cut ((less (v600) (v800)) = (less zenon_TX_cm (v800))). % 0.19/0.48 intro zenon_D_pnotp. % 0.19/0.48 apply zenon_H97. % 0.19/0.48 rewrite <- zenon_D_pnotp. % 0.19/0.48 exact ord_v600_v800. % 0.19/0.48 cut (((v800) = (v800))); [idtac | apply NNPP; zenon_intro zenon_H39]. % 0.19/0.48 cut (((v600) = zenon_TX_cm)); [idtac | apply NNPP; zenon_intro zenon_H9c]. % 0.19/0.48 congruence. % 0.19/0.48 apply (zenon_notand_s _ _ zenon_H9a); [ zenon_intro zenon_H9e | zenon_intro zenon_H9d ]. % 0.19/0.48 apply zenon_H9e. zenon_intro zenon_H90. % 0.19/0.48 elim (classic (zenon_TX_cm = zenon_TX_cm)); [ zenon_intro zenon_H9f | zenon_intro zenon_Ha0 ]. % 0.19/0.48 cut ((zenon_TX_cm = zenon_TX_cm) = ((v600) = zenon_TX_cm)). % 0.19/0.48 intro zenon_D_pnotp. % 0.19/0.48 apply zenon_H9c. % 0.19/0.48 rewrite <- zenon_D_pnotp. % 0.19/0.48 exact zenon_H9f. % 0.19/0.48 cut ((zenon_TX_cm = zenon_TX_cm)); [idtac | apply NNPP; zenon_intro zenon_Ha0]. % 0.19/0.48 cut ((zenon_TX_cm = (v600))); [idtac | apply NNPP; zenon_intro zenon_H9b]. % 0.19/0.48 congruence. % 0.19/0.48 exact (zenon_H9b zenon_H90). % 0.19/0.48 apply zenon_Ha0. apply refl_equal. % 0.19/0.48 apply zenon_Ha0. apply refl_equal. % 0.19/0.48 apply zenon_H9d. zenon_intro zenon_H3e. % 0.19/0.48 generalize (zenon_H3c zenon_TX_cm). zenon_intro zenon_H43. % 0.19/0.48 generalize (zenon_H43 (v600)). zenon_intro zenon_H44. % 0.19/0.48 generalize (zenon_H44 (v800)). zenon_intro zenon_Ha1. % 0.19/0.48 apply (zenon_imply_s _ _ zenon_Ha1); [ zenon_intro zenon_H47 | zenon_intro zenon_Ha2 ]. % 0.19/0.48 exact (zenon_H47 zenon_H3e). % 0.19/0.48 apply (zenon_imply_s _ _ zenon_Ha2); [ zenon_intro zenon_Ha4 | zenon_intro zenon_Ha3 ]. % 0.19/0.48 exact (zenon_Ha4 ord_v600_v800). % 0.19/0.48 exact (zenon_H97 zenon_Ha3). % 0.19/0.48 apply zenon_H39. apply refl_equal. % 0.19/0.48 cut ((less (v800) (v1200)) = (less zenon_TX_cm (v1200))). % 0.19/0.48 intro zenon_D_pnotp. % 0.19/0.48 apply zenon_H93. % 0.19/0.48 rewrite <- zenon_D_pnotp. % 0.19/0.48 exact ord_v800_v1200. % 0.19/0.48 cut (((v1200) = (v1200))); [idtac | apply NNPP; zenon_intro zenon_H3a]. % 0.19/0.48 cut (((v800) = zenon_TX_cm)); [idtac | apply NNPP; zenon_intro zenon_Ha5]. % 0.19/0.48 congruence. % 0.19/0.48 apply (zenon_notand_s _ _ zenon_H96); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Ha6 ]. % 0.19/0.48 apply zenon_Ha7. zenon_intro zenon_Ha8. % 0.19/0.48 elim (classic (zenon_TX_cm = zenon_TX_cm)); [ zenon_intro zenon_H9f | zenon_intro zenon_Ha0 ]. % 0.19/0.48 cut ((zenon_TX_cm = zenon_TX_cm) = ((v800) = zenon_TX_cm)). % 0.19/0.48 intro zenon_D_pnotp. % 0.19/0.48 apply zenon_Ha5. % 0.19/0.48 rewrite <- zenon_D_pnotp. % 0.19/0.48 exact zenon_H9f. % 0.19/0.48 cut ((zenon_TX_cm = zenon_TX_cm)); [idtac | apply NNPP; zenon_intro zenon_Ha0]. % 0.19/0.48 cut ((zenon_TX_cm = (v800))); [idtac | apply NNPP; zenon_intro zenon_H98]. % 0.19/0.48 congruence. % 0.19/0.48 exact (zenon_H98 zenon_Ha8). % 0.19/0.48 apply zenon_Ha0. apply refl_equal. % 0.19/0.48 apply zenon_Ha0. apply refl_equal. % 0.19/0.48 apply zenon_Ha6. zenon_intro zenon_Ha3. % 0.19/0.48 generalize (zenon_H3c zenon_TX_cm). zenon_intro zenon_H43. % 0.19/0.48 generalize (zenon_H43 (v800)). zenon_intro zenon_Ha9. % 0.19/0.48 generalize (zenon_Ha9 (v1200)). zenon_intro zenon_Haa. % 0.19/0.48 apply (zenon_imply_s _ _ zenon_Haa); [ zenon_intro zenon_H97 | zenon_intro zenon_Hab ]. % 0.19/0.48 exact (zenon_H97 zenon_Ha3). % 0.19/0.48 apply (zenon_imply_s _ _ zenon_Hab); [ zenon_intro zenon_Had | zenon_intro zenon_Hac ]. % 0.19/0.48 exact (zenon_Had ord_v800_v1200). % 0.19/0.48 exact (zenon_H93 zenon_Hac). % 0.19/0.48 apply zenon_H3a. apply refl_equal. % 0.19/0.48 cut ((less (v1200) zenon_TX_cm) = (less zenon_TX_cm zenon_TX_cm)). % 0.19/0.48 intro zenon_D_pnotp. % 0.19/0.48 apply zenon_H3d. % 0.19/0.48 rewrite <- zenon_D_pnotp. % 0.19/0.48 exact zenon_H8f. % 0.19/0.48 cut ((zenon_TX_cm = zenon_TX_cm)); [idtac | apply NNPP; zenon_intro zenon_Ha0]. % 0.19/0.48 cut (((v1200) = zenon_TX_cm)); [idtac | apply NNPP; zenon_intro zenon_H49]. % 0.19/0.48 congruence. % 0.19/0.48 apply (zenon_notand_s _ _ zenon_H92); [ zenon_intro zenon_Haf | zenon_intro zenon_Hae ]. % 0.19/0.48 apply zenon_Haf. zenon_intro zenon_Hb0. % 0.19/0.48 elim (classic (zenon_TX_cm = zenon_TX_cm)); [ zenon_intro zenon_H9f | zenon_intro zenon_Ha0 ]. % 0.19/0.48 cut ((zenon_TX_cm = zenon_TX_cm) = ((v1200) = zenon_TX_cm)). % 0.19/0.48 intro zenon_D_pnotp. % 0.19/0.48 apply zenon_H49. % 0.19/0.48 rewrite <- zenon_D_pnotp. % 0.19/0.48 exact zenon_H9f. % 0.19/0.48 cut ((zenon_TX_cm = zenon_TX_cm)); [idtac | apply NNPP; zenon_intro zenon_Ha0]. % 0.19/0.48 cut ((zenon_TX_cm = (v1200))); [idtac | apply NNPP; zenon_intro zenon_H94]. % 0.19/0.48 congruence. % 0.19/0.48 exact (zenon_H94 zenon_Hb0). % 0.19/0.48 apply zenon_Ha0. apply refl_equal. % 0.19/0.48 apply zenon_Ha0. apply refl_equal. % 0.19/0.48 apply zenon_Hae. zenon_intro zenon_Hac. % 0.19/0.48 generalize (zenon_H3c zenon_TX_cm). zenon_intro zenon_H43. % 0.19/0.48 generalize (zenon_H43 (v1200)). zenon_intro zenon_Hb1. % 0.19/0.48 generalize (zenon_Hb1 zenon_TX_cm). zenon_intro zenon_Hb2. % 0.19/0.48 apply (zenon_imply_s _ _ zenon_Hb2); [ zenon_intro zenon_H93 | zenon_intro zenon_Hb3 ]. % 0.19/0.48 exact (zenon_H93 zenon_Hac). % 0.19/0.48 apply (zenon_imply_s _ _ zenon_Hb3); [ zenon_intro zenon_Hb4 | zenon_intro zenon_H48 ]. % 0.19/0.48 exact (zenon_Hb4 zenon_H8f). % 0.19/0.48 exact (zenon_H3d zenon_H48). % 0.19/0.48 apply zenon_Ha0. apply refl_equal. % 0.19/0.48 apply (zenon_or_s _ _ zenon_H87); [ zenon_intro zenon_H3e | zenon_intro zenon_H90 ]. % 0.19/0.48 generalize (irreflexive zenon_TX_cm). zenon_intro zenon_H3d. % 0.19/0.48 apply (zenon_L4_ zenon_TX_cm); trivial. % 0.19/0.48 elim (classic ((v1200) = (v1200))); [ zenon_intro zenon_Hb5 | zenon_intro zenon_H3a ]. % 0.19/0.48 cut (((v1200) = (v1200)) = ((v600) = (v1200))). % 0.19/0.48 intro zenon_D_pnotp. % 0.19/0.48 apply zenon_H72. % 0.19/0.48 rewrite <- zenon_D_pnotp. % 0.19/0.48 exact zenon_Hb5. % 0.19/0.48 cut (((v1200) = (v1200))); [idtac | apply NNPP; zenon_intro zenon_H3a]. % 0.19/0.48 cut (((v1200) = (v600))); [idtac | apply NNPP; zenon_intro zenon_Hb6]. % 0.19/0.48 congruence. % 0.19/0.48 cut (((v1200) = zenon_TX_cm) = ((v1200) = (v600))). % 0.19/0.48 intro zenon_D_pnotp. % 0.19/0.48 apply zenon_Hb6. % 0.19/0.48 rewrite <- zenon_D_pnotp. % 0.19/0.48 exact zenon_H3f. % 0.19/0.48 cut ((zenon_TX_cm = (v600))); [idtac | apply NNPP; zenon_intro zenon_H9b]. % 0.19/0.48 cut (((v1200) = (v1200))); [idtac | apply NNPP; zenon_intro zenon_H3a]. % 0.19/0.48 congruence. % 0.19/0.48 apply zenon_H3a. apply refl_equal. % 0.19/0.48 exact (zenon_H9b zenon_H90). % 0.19/0.48 apply zenon_H3a. apply refl_equal. % 0.19/0.48 apply zenon_H3a. apply refl_equal. % 0.19/0.48 apply zenon_H4a. zenon_intro zenon_Tx_hb. apply NNPP. zenon_intro zenon_Hb8. % 0.19/0.48 apply zenon_Hb8. zenon_intro zenon_Ty_hd. apply NNPP. zenon_intro zenon_Hba. % 0.19/0.48 apply zenon_Hba. zenon_intro zenon_Tz_hf. apply NNPP. zenon_intro zenon_Hbc. % 0.19/0.48 apply (zenon_notimply_s _ _ zenon_Hbc). zenon_intro zenon_Hbe. zenon_intro zenon_Hbd. % 0.19/0.48 apply (zenon_notimply_s _ _ zenon_Hbd). zenon_intro zenon_Hc0. zenon_intro zenon_Hbf. % 0.19/0.48 generalize (transitive zenon_Tx_hb). zenon_intro zenon_Hc1. % 0.19/0.48 generalize (zenon_Hc1 zenon_Ty_hd). zenon_intro zenon_Hc2. % 0.19/0.48 generalize (zenon_Hc2 zenon_Tz_hf). zenon_intro zenon_Hc3. % 0.19/0.48 apply (zenon_imply_s _ _ zenon_Hc3); [ zenon_intro zenon_Hc5 | zenon_intro zenon_Hc4 ]. % 0.19/0.48 apply (zenon_notand_s _ _ zenon_Hc5); [ zenon_intro zenon_Hc7 | zenon_intro zenon_Hc6 ]. % 0.19/0.48 exact (zenon_Hc7 zenon_Hbe). % 0.19/0.48 exact (zenon_Hc6 zenon_Hc0). % 0.19/0.48 exact (zenon_Hbf zenon_Hc4). % 0.19/0.48 Qed. % 0.19/0.48 % SZS output end Proof % 0.19/0.48 (* END-PROOF *) % 0.19/0.48 nodes searched: 4135 % 0.19/0.48 max branch formulas: 382 % 0.19/0.48 proof nodes created: 158 % 0.19/0.48 formulas created: 4677 % 0.19/0.48 %------------------------------------------------------------------------------