%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT079+1 : TPTP v9.3.1. Bugfixed v9.3.1. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n005.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 17.64s 17.95s % Output : Proof 17.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT079+1 : TPTP v9.3.1. Bugfixed v9.3.1. % 0.00/0.04 % Command : run_zenon %s %d % 0.09/0.36 % Computer : n005.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Mon Sep 7 14:14:50 UTC 2026 % 0.09/0.36 % CPUTime : % 17.64/17.95 (* PROOF-FOUND *) % 17.64/17.95 % SZS status Theorem % 17.64/17.95 (* BEGIN-PROOF *) % 17.64/17.95 % SZS output start Proof % 17.64/17.95 Theorem odrl350 : (exists X : zenon_U, (exists Y : zenon_U, (exists Z : zenon_U, ((in_lopen X (v0) (v600))/\((in_lopen Y (v0) (v400))/\((in_lopen Z (v0) (v32))/\(~((in_lopen X (v0) (v1200))/\((in_lopen Y (v0) (v800))/\(in_lopen Z (v0) (v16))))))))))). % 17.64/17.95 Proof. % 17.64/17.95 assert (zenon_L1_ : (~((v16) = (v16))) -> False). % 17.64/17.95 do 0 intro. intros zenon_H39. % 17.64/17.95 apply zenon_H39. apply refl_equal. % 17.64/17.95 (* end of lemma zenon_L1_ *) % 17.64/17.95 assert (zenon_L2_ : (~(leq (v16) (v600))) -> False). % 17.64/17.95 do 0 intro. intros zenon_H3a. % 17.64/17.95 generalize (leq_def (v16)). zenon_intro zenon_H3b. % 17.64/17.95 generalize (zenon_H3b (v600)). zenon_intro zenon_H3c. % 17.64/17.95 apply (zenon_equiv_s _ _ zenon_H3c); [ zenon_intro zenon_H3a; zenon_intro zenon_H3f | zenon_intro zenon_H3e; zenon_intro zenon_H3d ]. % 17.64/17.95 apply (zenon_notor_s _ _ zenon_H3f). zenon_intro zenon_H41. zenon_intro zenon_H40. % 17.64/17.95 exact (zenon_H41 ord_v16_v600). % 17.64/17.95 exact (zenon_H3a zenon_H3e). % 17.64/17.95 (* end of lemma zenon_L2_ *) % 17.64/17.95 assert (zenon_L3_ : (~(in_lopen (v32) (v0) (v400))) -> False). % 17.64/17.95 do 0 intro. intros zenon_H42. % 17.64/17.95 generalize (in_lopen (v32)). zenon_intro zenon_H43. % 17.64/17.95 generalize (zenon_H43 (v0)). zenon_intro zenon_H44. % 17.64/17.95 generalize (zenon_H44 (v400)). zenon_intro zenon_H45. % 17.64/17.95 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H42; zenon_intro zenon_H48 | zenon_intro zenon_H47; zenon_intro zenon_H46 ]. % 17.64/17.95 apply (zenon_notand_s _ _ zenon_H48); [ zenon_intro zenon_H4a | zenon_intro zenon_H49 ]. % 17.64/17.95 exact (zenon_H4a ord_v0_v32). % 17.64/17.95 generalize (leq_def (v32)). zenon_intro zenon_H4b. % 17.64/17.95 generalize (zenon_H4b (v400)). zenon_intro zenon_H4c. % 17.64/17.95 apply (zenon_equiv_s _ _ zenon_H4c); [ zenon_intro zenon_H49; zenon_intro zenon_H4f | zenon_intro zenon_H4e; zenon_intro zenon_H4d ]. % 17.64/17.95 apply (zenon_notor_s _ _ zenon_H4f). zenon_intro zenon_H51. zenon_intro zenon_H50. % 17.64/17.95 exact (zenon_H51 ord_v32_v400). % 17.64/17.95 exact (zenon_H49 zenon_H4e). % 17.64/17.95 exact (zenon_H42 zenon_H47). % 17.64/17.95 (* end of lemma zenon_L3_ *) % 17.64/17.95 assert (zenon_L4_ : (~((v32) = (v32))) -> False). % 17.64/17.95 do 0 intro. intros zenon_H52. % 17.64/17.95 apply zenon_H52. apply refl_equal. % 17.64/17.95 (* end of lemma zenon_L4_ *) % 17.64/17.95 assert (zenon_L5_ : (~(in_lopen (v32) (v0) (v32))) -> False). % 17.64/17.95 do 0 intro. intros zenon_H53. % 17.64/17.95 generalize (in_lopen (v32)). zenon_intro zenon_H43. % 17.64/17.95 generalize (zenon_H43 (v0)). zenon_intro zenon_H44. % 17.64/17.95 generalize (zenon_H44 (v32)). zenon_intro zenon_H54. % 17.64/17.95 apply (zenon_equiv_s _ _ zenon_H54); [ zenon_intro zenon_H53; zenon_intro zenon_H57 | zenon_intro zenon_H56; zenon_intro zenon_H55 ]. % 17.64/17.95 apply (zenon_notand_s _ _ zenon_H57); [ zenon_intro zenon_H4a | zenon_intro zenon_H58 ]. % 17.64/17.95 exact (zenon_H4a ord_v0_v32). % 17.64/17.95 generalize (leq_def (v32)). zenon_intro zenon_H4b. % 17.64/17.95 generalize (zenon_H4b (v32)). zenon_intro zenon_H59. % 17.64/17.95 apply (zenon_equiv_s _ _ zenon_H59); [ zenon_intro zenon_H58; zenon_intro zenon_H5c | zenon_intro zenon_H5b; zenon_intro zenon_H5a ]. % 17.64/17.95 apply (zenon_notor_s _ _ zenon_H5c). zenon_intro zenon_H5d. zenon_intro zenon_H52. % 17.64/17.95 apply zenon_H52. apply refl_equal. % 17.64/17.95 exact (zenon_H58 zenon_H5b). % 17.64/17.95 exact (zenon_H53 zenon_H56). % 17.64/17.95 (* end of lemma zenon_L5_ *) % 17.64/17.95 assert (zenon_L6_ : (in_lopen (v32) (v0) (v16)) -> (~((v16) = (v32))) -> (~(less (v32) (v16))) -> False). % 17.64/17.95 do 0 intro. intros zenon_H5e zenon_H5f zenon_H60. % 17.64/17.95 generalize (in_lopen (v32)). zenon_intro zenon_H43. % 17.64/17.95 generalize (zenon_H43 (v0)). zenon_intro zenon_H44. % 17.64/17.95 generalize (zenon_H44 (v16)). zenon_intro zenon_H61. % 17.64/17.95 apply (zenon_equiv_s _ _ zenon_H61); [ zenon_intro zenon_H64; zenon_intro zenon_H63 | zenon_intro zenon_H5e; zenon_intro zenon_H62 ]. % 17.64/17.95 exact (zenon_H64 zenon_H5e). % 17.64/17.95 apply (zenon_and_s _ _ zenon_H62). zenon_intro ord_v0_v32. zenon_intro zenon_H65. % 17.64/17.95 generalize (leq_def (v32)). zenon_intro zenon_H4b. % 17.64/17.95 generalize (zenon_H4b (v16)). zenon_intro zenon_H66. % 17.64/17.95 apply (zenon_equiv_s _ _ zenon_H66); [ zenon_intro zenon_H69; zenon_intro zenon_H68 | zenon_intro zenon_H65; zenon_intro zenon_H67 ]. % 17.64/17.95 exact (zenon_H69 zenon_H65). % 17.64/17.95 apply (zenon_or_s _ _ zenon_H67); [ zenon_intro zenon_H6b | zenon_intro zenon_H6a ]. % 17.64/17.95 exact (zenon_H60 zenon_H6b). % 17.64/17.95 apply zenon_H5f. apply sym_equal. exact zenon_H6a. % 17.64/17.95 (* end of lemma zenon_L6_ *) % 17.64/17.95 assert (zenon_L7_ : (~(exists Y : zenon_U, (exists Z : zenon_U, ((in_lopen (v16) (v0) (v600))/\((in_lopen Y (v0) (v400))/\((in_lopen Z (v0) (v32))/\(~((in_lopen (v16) (v0) (v1200))/\((in_lopen Y (v0) (v800))/\(in_lopen Z (v0) (v16))))))))))) -> (~(less (v32) (v16))) -> (~((v16) = (v32))) -> False). % 17.64/17.95 do 0 intro. intros zenon_H6c zenon_H60 zenon_H5f. % 17.64/17.95 apply zenon_H6c. exists (v32). apply NNPP. zenon_intro zenon_H6d. % 17.64/17.95 apply zenon_H6d. exists (v32). apply NNPP. zenon_intro zenon_H6e. % 17.64/17.95 apply (zenon_notand_s _ _ zenon_H6e); [ zenon_intro zenon_H70 | zenon_intro zenon_H6f ]. % 17.64/17.95 generalize (in_lopen (v16)). zenon_intro zenon_H71. % 17.64/17.95 generalize (zenon_H71 (v0)). zenon_intro zenon_H72. % 17.64/17.95 generalize (zenon_H72 (v600)). zenon_intro zenon_H73. % 17.64/17.95 apply (zenon_equiv_s _ _ zenon_H73); [ zenon_intro zenon_H70; zenon_intro zenon_H76 | zenon_intro zenon_H75; zenon_intro zenon_H74 ]. % 17.64/17.95 apply (zenon_notand_s _ _ zenon_H76); [ zenon_intro zenon_H77 | zenon_intro zenon_H3a ]. % 17.64/17.95 exact (zenon_H77 ord_v0_v16). % 17.64/17.95 apply (zenon_L2_); trivial. % 17.64/17.95 exact (zenon_H70 zenon_H75). % 17.64/17.95 apply (zenon_notand_s _ _ zenon_H6f); [ zenon_intro zenon_H42 | zenon_intro zenon_H78 ]. % 17.64/17.95 apply (zenon_L3_); trivial. % 17.64/17.95 apply (zenon_notand_s _ _ zenon_H78); [ zenon_intro zenon_H53 | zenon_intro zenon_H79 ]. % 17.64/17.95 apply (zenon_L5_); trivial. % 17.64/17.95 apply zenon_H79. zenon_intro zenon_H7a. % 17.64/17.95 apply (zenon_and_s _ _ zenon_H7a). zenon_intro zenon_H7c. zenon_intro zenon_H7b. % 17.64/17.95 apply (zenon_and_s _ _ zenon_H7b). zenon_intro zenon_H7d. zenon_intro zenon_H5e. % 17.64/17.95 apply (zenon_L6_); trivial. % 17.64/17.95 (* end of lemma zenon_L7_ *) % 17.64/17.95 assert (zenon_L8_ : (~(exists X : zenon_U, (exists Y : zenon_U, (exists Z : zenon_U, ((in_lopen X (v0) (v600))/\((in_lopen Y (v0) (v400))/\((in_lopen Z (v0) (v32))/\(~((in_lopen X (v0) (v1200))/\((in_lopen Y (v0) (v800))/\(in_lopen Z (v0) (v16)))))))))))) -> (~((v16) = (v32))) -> (~(less (v32) (v16))) -> False). % 17.64/17.95 do 0 intro. intros zenon_G zenon_H5f zenon_H60. % 17.64/17.95 apply zenon_G. exists (v16). apply NNPP. zenon_intro zenon_H6c. % 17.64/17.95 apply (zenon_L7_); trivial. % 17.64/17.95 (* end of lemma zenon_L8_ *) % 17.64/17.95 assert (zenon_L9_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((less x y)->((less y z)->(less x z)))))) -> (~(less (v16) (v16))) -> (~(exists X : zenon_U, (exists Y : zenon_U, (exists Z : zenon_U, ((in_lopen X (v0) (v600))/\((in_lopen Y (v0) (v400))/\((in_lopen Z (v0) (v32))/\(~((in_lopen X (v0) (v1200))/\((in_lopen Y (v0) (v800))/\(in_lopen Z (v0) (v16)))))))))))) -> (~((v16) = (v32))) -> False). % 17.64/17.95 do 0 intro. intros zenon_H7e zenon_H7f zenon_G zenon_H5f. % 17.64/17.95 elim (classic (less (v32) (v16))); [ zenon_intro zenon_H6b | zenon_intro zenon_H60 ]. % 17.64/17.95 generalize (zenon_H7e (v16)). zenon_intro zenon_H80. % 17.64/17.95 generalize (zenon_H80 (v32)). zenon_intro zenon_H81. % 17.64/17.95 generalize (zenon_H81 (v16)). zenon_intro zenon_H82. % 17.64/17.95 apply (zenon_imply_s _ _ zenon_H82); [ zenon_intro zenon_H84 | zenon_intro zenon_H83 ]. % 17.64/17.95 exact (zenon_H84 ord_v16_v32). % 17.64/17.95 apply (zenon_imply_s _ _ zenon_H83); [ zenon_intro zenon_H60 | zenon_intro zenon_H85 ]. % 17.64/17.95 exact (zenon_H60 zenon_H6b). % 17.64/17.95 exact (zenon_H7f zenon_H85). % 17.64/17.95 apply (zenon_L8_); trivial. % 17.64/17.95 (* end of lemma zenon_L9_ *) % 17.64/17.95 apply NNPP. intro zenon_G. % 17.64/17.95 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_H7e | zenon_intro zenon_H86 ]. % 17.64/17.95 apply (zenon_and_s _ _ distinct). zenon_intro zenon_H88. zenon_intro zenon_H87. % 17.64/17.95 apply (zenon_and_s _ _ zenon_H87). zenon_intro zenon_H8a. zenon_intro zenon_H89. % 17.64/17.95 apply (zenon_and_s _ _ zenon_H89). zenon_intro zenon_H8c. zenon_intro zenon_H8b. % 17.64/17.95 apply (zenon_and_s _ _ zenon_H8b). zenon_intro zenon_H8e. zenon_intro zenon_H8d. % 17.64/17.95 apply (zenon_and_s _ _ zenon_H8d). zenon_intro zenon_H90. zenon_intro zenon_H8f. % 17.64/17.95 apply (zenon_and_s _ _ zenon_H8f). zenon_intro zenon_H92. zenon_intro zenon_H91. % 17.64/17.95 apply (zenon_and_s _ _ zenon_H91). zenon_intro zenon_H5f. zenon_intro zenon_H93. % 17.64/17.95 generalize (irreflexive (v16)). zenon_intro zenon_H7f. % 17.64/17.95 apply (zenon_L9_); trivial. % 17.64/17.95 apply zenon_H86. zenon_intro zenon_Tx_fs. apply NNPP. zenon_intro zenon_H95. % 17.64/17.95 apply zenon_H95. zenon_intro zenon_Ty_fu. apply NNPP. zenon_intro zenon_H97. % 17.64/17.95 apply zenon_H97. zenon_intro zenon_Tz_fw. apply NNPP. zenon_intro zenon_H99. % 17.64/17.95 apply (zenon_notimply_s _ _ zenon_H99). zenon_intro zenon_H9b. zenon_intro zenon_H9a. % 17.64/17.96 apply (zenon_notimply_s _ _ zenon_H9a). zenon_intro zenon_H9d. zenon_intro zenon_H9c. % 17.64/17.96 generalize (transitive zenon_Tx_fs). zenon_intro zenon_H9e. % 17.64/17.96 generalize (zenon_H9e zenon_Ty_fu). zenon_intro zenon_H9f. % 17.64/17.96 generalize (zenon_H9f zenon_Tz_fw). zenon_intro zenon_Ha0. % 17.64/17.96 apply (zenon_imply_s _ _ zenon_Ha0); [ zenon_intro zenon_Ha2 | zenon_intro zenon_Ha1 ]. % 17.64/17.96 apply (zenon_notand_s _ _ zenon_Ha2); [ zenon_intro zenon_Ha4 | zenon_intro zenon_Ha3 ]. % 17.64/17.96 exact (zenon_Ha4 zenon_H9b). % 17.64/17.96 exact (zenon_Ha3 zenon_H9d). % 17.64/17.96 exact (zenon_H9c zenon_Ha1). % 17.64/17.96 Qed. % 17.64/17.96 % SZS output end Proof % 17.64/17.96 (* END-PROOF *) % 17.64/17.96 nodes searched: 1317858 % 17.64/17.96 max branch formulas: 6068 % 17.64/17.96 proof nodes created: 1709 % 17.64/17.96 formulas created: 401580 % 17.64/17.96 %------------------------------------------------------------------------------