%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT076+1 : TPTP v9.3.1. Bugfixed v9.3.1. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n020.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.13s 0.43s % Output : Proof 0.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT076+1 : TPTP v9.3.1. Bugfixed v9.3.1. % 0.00/0.03 % Command : run_zenon %s %d % 0.08/0.34 % Computer : n020.cluster.edu % 0.08/0.34 % Model : x86_64 x86_64 % 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.34 % Memory : 8046.5625MB % 0.08/0.34 % OS : Linux 6.8.0-71-generic % 0.08/0.34 % CPULimit : 300 % 0.08/0.34 % WCLimit : 300 % 0.08/0.34 % DateTime : Mon Sep 7 14:12:58 UTC 2026 % 0.08/0.34 % CPUTime : % 0.13/0.43 (* PROOF-FOUND *) % 0.13/0.43 % SZS status Theorem % 0.13/0.43 (* BEGIN-PROOF *) % 0.13/0.43 % SZS output start Proof % 0.13/0.43 Theorem odrl311 : (forall X : zenon_U, ((leq (v800) X)->(leq (v400) X))). % 0.13/0.43 Proof. % 0.13/0.43 apply NNPP. intro zenon_G. % 0.13/0.43 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_H23 | zenon_intro zenon_H24 ]. % 0.13/0.43 apply (zenon_notallex_s (fun X : zenon_U => ((leq (v800) X)->(leq (v400) X))) zenon_G); [ zenon_intro zenon_H25; idtac ]. % 0.13/0.43 elim zenon_H25. zenon_intro zenon_TX_bm. zenon_intro zenon_H27. % 0.13/0.43 apply (zenon_notimply_s _ _ zenon_H27). zenon_intro zenon_H29. zenon_intro zenon_H28. % 0.13/0.43 generalize (leq_def (v800)). zenon_intro zenon_H2a. % 0.13/0.43 generalize (zenon_H2a zenon_TX_bm). zenon_intro zenon_H2b. % 0.13/0.43 apply (zenon_equiv_s _ _ zenon_H2b); [ zenon_intro zenon_H2e; zenon_intro zenon_H2d | zenon_intro zenon_H29; zenon_intro zenon_H2c ]. % 0.13/0.43 exact (zenon_H2e zenon_H29). % 0.13/0.43 generalize (leq_def (v400)). zenon_intro zenon_H2f. % 0.13/0.43 generalize (zenon_H2f zenon_TX_bm). zenon_intro zenon_H30. % 0.13/0.43 apply (zenon_equiv_s _ _ zenon_H30); [ zenon_intro zenon_H28; zenon_intro zenon_H33 | zenon_intro zenon_H32; zenon_intro zenon_H31 ]. % 0.13/0.43 apply (zenon_notor_s _ _ zenon_H33). zenon_intro zenon_H35. zenon_intro zenon_H34. % 0.13/0.43 apply (zenon_or_s _ _ zenon_H2c); [ zenon_intro zenon_H37 | zenon_intro zenon_H36 ]. % 0.13/0.43 elim (classic ((~((v400) = (v800)))/\(~(less (v400) (v800))))); [ zenon_intro zenon_H38 | zenon_intro zenon_H39 ]. % 0.13/0.43 apply (zenon_and_s _ _ zenon_H38). zenon_intro zenon_H3b. zenon_intro zenon_H3a. % 0.13/0.43 exact (zenon_H3a ord_v400_v800). % 0.13/0.43 cut ((less (v800) zenon_TX_bm) = (less (v400) zenon_TX_bm)). % 0.13/0.43 intro zenon_D_pnotp. % 0.13/0.43 apply zenon_H35. % 0.13/0.43 rewrite <- zenon_D_pnotp. % 0.13/0.43 exact zenon_H37. % 0.13/0.43 cut ((zenon_TX_bm = zenon_TX_bm)); [idtac | apply NNPP; zenon_intro zenon_H3c]. % 0.13/0.43 cut (((v800) = (v400))); [idtac | apply NNPP; zenon_intro zenon_H3d]. % 0.13/0.43 congruence. % 0.13/0.43 apply (zenon_notand_s _ _ zenon_H39); [ zenon_intro zenon_H3f | zenon_intro zenon_H3e ]. % 0.13/0.43 apply zenon_H3f. zenon_intro zenon_H40. % 0.13/0.43 elim (classic ((v400) = (v400))); [ zenon_intro zenon_H41 | zenon_intro zenon_H42 ]. % 0.13/0.43 cut (((v400) = (v400)) = ((v800) = (v400))). % 0.13/0.43 intro zenon_D_pnotp. % 0.13/0.43 apply zenon_H3d. % 0.13/0.43 rewrite <- zenon_D_pnotp. % 0.13/0.43 exact zenon_H41. % 0.13/0.43 cut (((v400) = (v400))); [idtac | apply NNPP; zenon_intro zenon_H42]. % 0.13/0.43 cut (((v400) = (v800))); [idtac | apply NNPP; zenon_intro zenon_H3b]. % 0.13/0.43 congruence. % 0.13/0.43 exact (zenon_H3b zenon_H40). % 0.13/0.43 apply zenon_H42. apply refl_equal. % 0.13/0.43 apply zenon_H42. apply refl_equal. % 0.13/0.43 apply zenon_H3e. zenon_intro ord_v400_v800. % 0.13/0.43 generalize (zenon_H23 (v400)). zenon_intro zenon_H43. % 0.13/0.43 generalize (zenon_H43 (v800)). zenon_intro zenon_H44. % 0.13/0.43 generalize (zenon_H44 zenon_TX_bm). zenon_intro zenon_H45. % 0.13/0.43 apply (zenon_imply_s _ _ zenon_H45); [ zenon_intro zenon_H3a | zenon_intro zenon_H46 ]. % 0.13/0.43 exact (zenon_H3a ord_v400_v800). % 0.13/0.43 apply (zenon_imply_s _ _ zenon_H46); [ zenon_intro zenon_H48 | zenon_intro zenon_H47 ]. % 0.13/0.43 exact (zenon_H48 zenon_H37). % 0.13/0.43 exact (zenon_H35 zenon_H47). % 0.13/0.43 apply zenon_H3c. apply refl_equal. % 0.13/0.43 cut ((less (v400) (v800)) = (less (v400) zenon_TX_bm)). % 0.13/0.43 intro zenon_D_pnotp. % 0.13/0.43 apply zenon_H35. % 0.13/0.43 rewrite <- zenon_D_pnotp. % 0.13/0.43 exact ord_v400_v800. % 0.13/0.43 cut (((v800) = zenon_TX_bm)); [idtac | apply NNPP; zenon_intro zenon_H49]. % 0.13/0.43 cut (((v400) = (v400))); [idtac | apply NNPP; zenon_intro zenon_H42]. % 0.13/0.43 congruence. % 0.13/0.43 apply zenon_H42. apply refl_equal. % 0.13/0.43 exact (zenon_H49 zenon_H36). % 0.13/0.43 exact (zenon_H28 zenon_H32). % 0.13/0.43 apply zenon_H24. zenon_intro zenon_Tx_cw. apply NNPP. zenon_intro zenon_H4b. % 0.13/0.43 apply zenon_H4b. zenon_intro zenon_Ty_cy. apply NNPP. zenon_intro zenon_H4d. % 0.13/0.43 apply zenon_H4d. zenon_intro zenon_Tz_da. apply NNPP. zenon_intro zenon_H4f. % 0.13/0.43 apply (zenon_notimply_s _ _ zenon_H4f). zenon_intro zenon_H51. zenon_intro zenon_H50. % 0.13/0.43 apply (zenon_notimply_s _ _ zenon_H50). zenon_intro zenon_H53. zenon_intro zenon_H52. % 0.13/0.43 generalize (transitive zenon_Tx_cw). zenon_intro zenon_H54. % 0.13/0.43 generalize (zenon_H54 zenon_Ty_cy). zenon_intro zenon_H55. % 0.13/0.43 generalize (zenon_H55 zenon_Tz_da). zenon_intro zenon_H56. % 0.13/0.43 apply (zenon_imply_s _ _ zenon_H56); [ zenon_intro zenon_H58 | zenon_intro zenon_H57 ]. % 0.13/0.43 apply (zenon_notand_s _ _ zenon_H58); [ zenon_intro zenon_H5a | zenon_intro zenon_H59 ]. % 0.13/0.43 exact (zenon_H5a zenon_H51). % 0.13/0.43 exact (zenon_H59 zenon_H53). % 0.13/0.43 exact (zenon_H52 zenon_H57). % 0.13/0.43 Qed. % 0.13/0.43 % SZS output end Proof % 0.13/0.43 (* END-PROOF *) % 0.13/0.43 nodes searched: 139 % 0.13/0.43 max branch formulas: 100 % 0.13/0.43 proof nodes created: 12 % 0.13/0.43 formulas created: 1097 % 0.13/0.43 %------------------------------------------------------------------------------