%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT084+1 : TPTP v9.3.1. Bugfixed v9.3.1. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n018.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.20s 0.48s % Output : Proof 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT084+1 : TPTP v9.3.1. Bugfixed v9.3.1. % 0.00/0.03 % Command : run_zenon %s %d % 0.09/0.34 % Computer : n018.cluster.edu % 0.09/0.34 % Model : x86_64 x86_64 % 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.34 % Memory : 8046.5625MB % 0.09/0.34 % OS : Linux 6.8.0-71-generic % 0.09/0.34 % CPULimit : 300 % 0.09/0.34 % WCLimit : 300 % 0.09/0.34 % DateTime : Mon Sep 7 14:20:22 UTC 2026 % 0.09/0.35 % CPUTime : % 0.20/0.48 (* PROOF-FOUND *) % 0.20/0.48 % SZS status Theorem % 0.20/0.48 (* BEGIN-PROOF *) % 0.20/0.48 % SZS output start Proof % 0.20/0.48 Theorem odrl432 : (~(exists X : zenon_U, (exists Y : zenon_U, (exists Z : zenon_U, ((in_lopen X (v0) (v600))/\((leq (v600) X)/\((in_lopen Y (v0) (v400))/\((less (v400) Y)/\((in_lopen Z (v0) (v200))/\(leq (v200) Z)))))))))). % 0.20/0.48 Proof. % 0.20/0.48 apply NNPP. intro zenon_G. % 0.20/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_H27 | zenon_intro zenon_H28 ]. % 0.20/0.48 apply zenon_G. zenon_intro zenon_H29. % 0.20/0.48 elim zenon_H29. zenon_intro zenon_TX_bq. zenon_intro zenon_H2b. % 0.20/0.48 elim zenon_H2b. zenon_intro zenon_TY_bs. zenon_intro zenon_H2d. % 0.20/0.48 elim zenon_H2d. zenon_intro zenon_TZ_bu. zenon_intro zenon_H2f. % 0.20/0.48 apply (zenon_and_s _ _ zenon_H2f). zenon_intro zenon_H31. zenon_intro zenon_H30. % 0.20/0.48 apply (zenon_and_s _ _ zenon_H30). zenon_intro zenon_H33. zenon_intro zenon_H32. % 0.20/0.48 apply (zenon_and_s _ _ zenon_H32). zenon_intro zenon_H35. zenon_intro zenon_H34. % 0.20/0.48 apply (zenon_and_s _ _ zenon_H34). zenon_intro zenon_H37. zenon_intro zenon_H36. % 0.20/0.48 generalize (in_lopen zenon_TY_bs). zenon_intro zenon_H38. % 0.20/0.48 generalize (zenon_H38 (v0)). zenon_intro zenon_H39. % 0.20/0.48 generalize (zenon_H39 (v400)). zenon_intro zenon_H3a. % 0.20/0.48 apply (zenon_equiv_s _ _ zenon_H3a); [ zenon_intro zenon_H3d; zenon_intro zenon_H3c | zenon_intro zenon_H35; zenon_intro zenon_H3b ]. % 0.20/0.48 exact (zenon_H3d zenon_H35). % 0.20/0.48 apply (zenon_and_s _ _ zenon_H3b). zenon_intro zenon_H3f. zenon_intro zenon_H3e. % 0.20/0.48 generalize (leq_def zenon_TY_bs). zenon_intro zenon_H40. % 0.20/0.48 generalize (zenon_H40 (v400)). zenon_intro zenon_H41. % 0.20/0.48 apply (zenon_equiv_s _ _ zenon_H41); [ zenon_intro zenon_H44; zenon_intro zenon_H43 | zenon_intro zenon_H3e; zenon_intro zenon_H42 ]. % 0.20/0.48 exact (zenon_H44 zenon_H3e). % 0.20/0.48 apply (zenon_or_s _ _ zenon_H42); [ zenon_intro zenon_H46 | zenon_intro zenon_H45 ]. % 0.20/0.48 generalize (irreflexive zenon_TY_bs). zenon_intro zenon_H47. % 0.20/0.48 elim (classic ((~(zenon_TY_bs = (v400)))/\(~(less zenon_TY_bs (v400))))); [ zenon_intro zenon_H48 | zenon_intro zenon_H49 ]. % 0.20/0.48 apply (zenon_and_s _ _ zenon_H48). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 0.20/0.48 exact (zenon_H4a zenon_H46). % 0.20/0.48 cut ((less (v400) zenon_TY_bs) = (less zenon_TY_bs zenon_TY_bs)). % 0.20/0.48 intro zenon_D_pnotp. % 0.20/0.48 apply zenon_H47. % 0.20/0.48 rewrite <- zenon_D_pnotp. % 0.20/0.48 exact zenon_H37. % 0.20/0.48 cut ((zenon_TY_bs = zenon_TY_bs)); [idtac | apply NNPP; zenon_intro zenon_H4c]. % 0.20/0.48 cut (((v400) = zenon_TY_bs)); [idtac | apply NNPP; zenon_intro zenon_H4d]. % 0.20/0.48 congruence. % 0.20/0.48 apply (zenon_notand_s _ _ zenon_H49); [ zenon_intro zenon_H4f | zenon_intro zenon_H4e ]. % 0.20/0.48 apply zenon_H4f. zenon_intro zenon_H45. % 0.20/0.48 elim (classic (zenon_TY_bs = zenon_TY_bs)); [ zenon_intro zenon_H50 | zenon_intro zenon_H4c ]. % 0.20/0.48 cut ((zenon_TY_bs = zenon_TY_bs) = ((v400) = zenon_TY_bs)). % 0.20/0.48 intro zenon_D_pnotp. % 0.20/0.48 apply zenon_H4d. % 0.20/0.48 rewrite <- zenon_D_pnotp. % 0.20/0.48 exact zenon_H50. % 0.20/0.48 cut ((zenon_TY_bs = zenon_TY_bs)); [idtac | apply NNPP; zenon_intro zenon_H4c]. % 0.20/0.48 cut ((zenon_TY_bs = (v400))); [idtac | apply NNPP; zenon_intro zenon_H4b]. % 0.20/0.48 congruence. % 0.20/0.48 exact (zenon_H4b zenon_H45). % 0.20/0.48 apply zenon_H4c. apply refl_equal. % 0.20/0.48 apply zenon_H4c. apply refl_equal. % 0.20/0.48 apply zenon_H4e. zenon_intro zenon_H46. % 0.20/0.48 generalize (zenon_H27 zenon_TY_bs). zenon_intro zenon_H51. % 0.20/0.48 generalize (zenon_H51 (v400)). zenon_intro zenon_H52. % 0.20/0.48 generalize (zenon_H52 zenon_TY_bs). zenon_intro zenon_H53. % 0.20/0.48 apply (zenon_imply_s _ _ zenon_H53); [ zenon_intro zenon_H4a | zenon_intro zenon_H54 ]. % 0.20/0.48 exact (zenon_H4a zenon_H46). % 0.20/0.48 apply (zenon_imply_s _ _ zenon_H54); [ zenon_intro zenon_H56 | zenon_intro zenon_H55 ]. % 0.20/0.48 exact (zenon_H56 zenon_H37). % 0.20/0.48 exact (zenon_H47 zenon_H55). % 0.20/0.48 apply zenon_H4c. apply refl_equal. % 0.20/0.48 generalize (irreflexive zenon_TY_bs). zenon_intro zenon_H47. % 0.20/0.48 elim (classic ((~(zenon_TY_bs = (v400)))/\(~(less zenon_TY_bs (v400))))); [ zenon_intro zenon_H48 | zenon_intro zenon_H49 ]. % 0.20/0.48 apply (zenon_and_s _ _ zenon_H48). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 0.20/0.48 exact (zenon_H4b zenon_H45). % 0.20/0.48 cut ((less (v400) zenon_TY_bs) = (less zenon_TY_bs zenon_TY_bs)). % 0.20/0.48 intro zenon_D_pnotp. % 0.20/0.48 apply zenon_H47. % 0.20/0.48 rewrite <- zenon_D_pnotp. % 0.20/0.48 exact zenon_H37. % 0.20/0.48 cut ((zenon_TY_bs = zenon_TY_bs)); [idtac | apply NNPP; zenon_intro zenon_H4c]. % 0.20/0.48 cut (((v400) = zenon_TY_bs)); [idtac | apply NNPP; zenon_intro zenon_H4d]. % 0.20/0.48 congruence. % 0.20/0.48 apply (zenon_notand_s _ _ zenon_H49); [ zenon_intro zenon_H4f | zenon_intro zenon_H4e ]. % 0.20/0.48 apply zenon_H4f. zenon_intro zenon_H45. % 0.20/0.48 elim (classic (zenon_TY_bs = zenon_TY_bs)); [ zenon_intro zenon_H50 | zenon_intro zenon_H4c ]. % 0.20/0.48 cut ((zenon_TY_bs = zenon_TY_bs) = ((v400) = zenon_TY_bs)). % 0.20/0.48 intro zenon_D_pnotp. % 0.20/0.48 apply zenon_H4d. % 0.20/0.48 rewrite <- zenon_D_pnotp. % 0.20/0.48 exact zenon_H50. % 0.20/0.48 cut ((zenon_TY_bs = zenon_TY_bs)); [idtac | apply NNPP; zenon_intro zenon_H4c]. % 0.20/0.48 cut ((zenon_TY_bs = (v400))); [idtac | apply NNPP; zenon_intro zenon_H4b]. % 0.20/0.48 congruence. % 0.20/0.48 exact (zenon_H4b zenon_H45). % 0.20/0.48 apply zenon_H4c. apply refl_equal. % 0.20/0.48 apply zenon_H4c. apply refl_equal. % 0.20/0.48 apply zenon_H4e. zenon_intro zenon_H46. % 0.20/0.48 generalize (zenon_H27 zenon_TY_bs). zenon_intro zenon_H51. % 0.20/0.48 generalize (zenon_H51 (v400)). zenon_intro zenon_H52. % 0.20/0.48 generalize (zenon_H52 zenon_TY_bs). zenon_intro zenon_H53. % 0.20/0.48 apply (zenon_imply_s _ _ zenon_H53); [ zenon_intro zenon_H4a | zenon_intro zenon_H54 ]. % 0.20/0.48 exact (zenon_H4a zenon_H46). % 0.20/0.48 apply (zenon_imply_s _ _ zenon_H54); [ zenon_intro zenon_H56 | zenon_intro zenon_H55 ]. % 0.20/0.48 exact (zenon_H56 zenon_H37). % 0.20/0.48 exact (zenon_H47 zenon_H55). % 0.20/0.48 apply zenon_H4c. apply refl_equal. % 0.20/0.48 apply zenon_H28. zenon_intro zenon_Tx_dj. apply NNPP. zenon_intro zenon_H58. % 0.20/0.48 apply zenon_H58. zenon_intro zenon_Ty_dl. apply NNPP. zenon_intro zenon_H5a. % 0.20/0.48 apply zenon_H5a. zenon_intro zenon_Tz_dn. apply NNPP. zenon_intro zenon_H5c. % 0.20/0.48 apply (zenon_notimply_s _ _ zenon_H5c). zenon_intro zenon_H5e. zenon_intro zenon_H5d. % 0.20/0.48 apply (zenon_notimply_s _ _ zenon_H5d). zenon_intro zenon_H60. zenon_intro zenon_H5f. % 0.20/0.48 generalize (transitive zenon_Tx_dj). zenon_intro zenon_H61. % 0.20/0.48 generalize (zenon_H61 zenon_Ty_dl). zenon_intro zenon_H62. % 0.20/0.48 generalize (zenon_H62 zenon_Tz_dn). zenon_intro zenon_H63. % 0.20/0.48 apply (zenon_imply_s _ _ zenon_H63); [ zenon_intro zenon_H65 | zenon_intro zenon_H64 ]. % 0.20/0.48 apply (zenon_notand_s _ _ zenon_H65); [ zenon_intro zenon_H67 | zenon_intro zenon_H66 ]. % 0.20/0.48 exact (zenon_H67 zenon_H5e). % 0.20/0.48 exact (zenon_H66 zenon_H60). % 0.20/0.48 exact (zenon_H5f zenon_H64). % 0.20/0.48 Qed. % 0.20/0.48 % SZS output end Proof % 0.20/0.48 (* END-PROOF *) % 0.20/0.48 nodes searched: 1082 % 0.20/0.48 max branch formulas: 273 % 0.20/0.48 proof nodes created: 70 % 0.20/0.48 formulas created: 3092 % 0.20/0.48 %------------------------------------------------------------------------------