%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT092+1 : TPTP v9.3.1. Bugfixed v9.3.1. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n026.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:28 AM UTC 2026 % Result : Theorem 0.14s 0.45s % Output : Proof 0.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT092+1 : TPTP v9.3.1. Bugfixed v9.3.1. % 0.00/0.03 % Command : run_zenon %s %d % 0.09/0.35 % Computer : n026.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Mon Sep 7 14:26:42 UTC 2026 % 0.09/0.35 % CPUTime : % 0.14/0.45 (* PROOF-FOUND *) % 0.14/0.45 % SZS status Theorem % 0.14/0.45 (* BEGIN-PROOF *) % 0.14/0.45 % SZS output start Proof % 0.14/0.45 Theorem odrl633 : (completion_conflict (v400) (v800) (v0) (v1200)). % 0.14/0.45 Proof. % 0.14/0.45 assert (zenon_L1_ : (~((v1200) = (v1200))) -> False). % 0.14/0.45 do 0 intro. intros zenon_H2a. % 0.14/0.45 apply zenon_H2a. apply refl_equal. % 0.14/0.45 (* end of lemma zenon_L1_ *) % 0.14/0.45 apply NNPP. intro zenon_G. % 0.14/0.45 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_H2b | zenon_intro zenon_H2c ]. % 0.14/0.45 generalize (sharpness_conflict (v400)). zenon_intro zenon_H2d. % 0.14/0.45 generalize (zenon_H2d (v800)). zenon_intro zenon_H2e. % 0.14/0.45 generalize (zenon_H2e (v0)). zenon_intro zenon_H2f. % 0.14/0.45 generalize (zenon_H2f (v1200)). zenon_intro zenon_H30. % 0.14/0.45 apply (zenon_imply_s _ _ zenon_H30); [ zenon_intro zenon_H32 | zenon_intro zenon_H31 ]. % 0.14/0.45 apply (zenon_notand_s _ _ zenon_H32); [ zenon_intro zenon_H34 | zenon_intro zenon_H33 ]. % 0.14/0.45 generalize (leq_def (v0)). zenon_intro zenon_H35. % 0.14/0.45 generalize (zenon_H35 (v400)). zenon_intro zenon_H36. % 0.14/0.45 apply (zenon_equiv_s _ _ zenon_H36); [ zenon_intro zenon_H34; zenon_intro zenon_H39 | zenon_intro zenon_H38; zenon_intro zenon_H37 ]. % 0.14/0.45 apply (zenon_notor_s _ _ zenon_H39). zenon_intro zenon_H3b. zenon_intro zenon_H3a. % 0.14/0.45 exact (zenon_H3b ord_v0_v400). % 0.14/0.45 exact (zenon_H34 zenon_H38). % 0.14/0.45 apply (zenon_notand_s _ _ zenon_H33); [ zenon_intro zenon_H3d | zenon_intro zenon_H3c ]. % 0.14/0.45 generalize (leq_def (v400)). zenon_intro zenon_H3e. % 0.14/0.45 generalize (zenon_H3e (v1200)). zenon_intro zenon_H3f. % 0.14/0.45 apply (zenon_equiv_s _ _ zenon_H3f); [ zenon_intro zenon_H3d; zenon_intro zenon_H42 | zenon_intro zenon_H41; zenon_intro zenon_H40 ]. % 0.14/0.45 apply (zenon_notor_s _ _ zenon_H42). zenon_intro zenon_H44. zenon_intro zenon_H43. % 0.14/0.45 elim (classic ((~((v400) = (v800)))/\(~(less (v400) (v800))))); [ zenon_intro zenon_H45 | zenon_intro zenon_H46 ]. % 0.14/0.45 apply (zenon_and_s _ _ zenon_H45). zenon_intro zenon_H48. zenon_intro zenon_H47. % 0.14/0.45 exact (zenon_H47 ord_v400_v800). % 0.14/0.45 cut ((less (v800) (v1200)) = (less (v400) (v1200))). % 0.14/0.45 intro zenon_D_pnotp. % 0.14/0.45 apply zenon_H44. % 0.14/0.45 rewrite <- zenon_D_pnotp. % 0.14/0.45 exact ord_v800_v1200. % 0.14/0.45 cut (((v1200) = (v1200))); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 0.14/0.45 cut (((v800) = (v400))); [idtac | apply NNPP; zenon_intro zenon_H49]. % 0.14/0.45 congruence. % 0.14/0.45 apply (zenon_notand_s _ _ zenon_H46); [ zenon_intro zenon_H4b | zenon_intro zenon_H4a ]. % 0.14/0.45 apply zenon_H4b. zenon_intro zenon_H4c. % 0.14/0.45 elim (classic ((v400) = (v400))); [ zenon_intro zenon_H4d | zenon_intro zenon_H4e ]. % 0.14/0.45 cut (((v400) = (v400)) = ((v800) = (v400))). % 0.14/0.45 intro zenon_D_pnotp. % 0.14/0.45 apply zenon_H49. % 0.14/0.45 rewrite <- zenon_D_pnotp. % 0.14/0.45 exact zenon_H4d. % 0.14/0.45 cut (((v400) = (v400))); [idtac | apply NNPP; zenon_intro zenon_H4e]. % 0.14/0.45 cut (((v400) = (v800))); [idtac | apply NNPP; zenon_intro zenon_H48]. % 0.14/0.45 congruence. % 0.14/0.45 exact (zenon_H48 zenon_H4c). % 0.14/0.45 apply zenon_H4e. apply refl_equal. % 0.14/0.45 apply zenon_H4e. apply refl_equal. % 0.14/0.45 apply zenon_H4a. zenon_intro ord_v400_v800. % 0.14/0.45 generalize (zenon_H2b (v400)). zenon_intro zenon_H4f. % 0.14/0.45 generalize (zenon_H4f (v800)). zenon_intro zenon_H50. % 0.14/0.45 generalize (zenon_H50 (v1200)). zenon_intro zenon_H51. % 0.14/0.45 apply (zenon_imply_s _ _ zenon_H51); [ zenon_intro zenon_H47 | zenon_intro zenon_H52 ]. % 0.14/0.45 exact (zenon_H47 ord_v400_v800). % 0.14/0.45 apply (zenon_imply_s _ _ zenon_H52); [ zenon_intro zenon_H54 | zenon_intro zenon_H53 ]. % 0.14/0.45 exact (zenon_H54 ord_v800_v1200). % 0.14/0.45 exact (zenon_H44 zenon_H53). % 0.14/0.45 apply zenon_H2a. apply refl_equal. % 0.14/0.45 exact (zenon_H3d zenon_H41). % 0.14/0.45 apply (zenon_notand_s _ _ zenon_H3c); [ zenon_intro zenon_H47 | zenon_intro zenon_H55 ]. % 0.14/0.45 exact (zenon_H47 ord_v400_v800). % 0.14/0.45 generalize (leq_def (v800)). zenon_intro zenon_H56. % 0.14/0.45 generalize (zenon_H56 (v1200)). zenon_intro zenon_H57. % 0.14/0.45 apply (zenon_equiv_s _ _ zenon_H57); [ zenon_intro zenon_H55; zenon_intro zenon_H5a | zenon_intro zenon_H59; zenon_intro zenon_H58 ]. % 0.14/0.45 apply (zenon_notor_s _ _ zenon_H5a). zenon_intro zenon_H54. zenon_intro zenon_H5b. % 0.14/0.45 exact (zenon_H54 ord_v800_v1200). % 0.14/0.45 exact (zenon_H55 zenon_H59). % 0.14/0.45 exact (zenon_G zenon_H31). % 0.14/0.45 apply zenon_H2c. zenon_intro zenon_Tx_do. apply NNPP. zenon_intro zenon_H5d. % 0.14/0.45 apply zenon_H5d. zenon_intro zenon_Ty_dq. apply NNPP. zenon_intro zenon_H5f. % 0.14/0.45 apply zenon_H5f. zenon_intro zenon_Tz_ds. apply NNPP. zenon_intro zenon_H61. % 0.14/0.45 apply (zenon_notimply_s _ _ zenon_H61). zenon_intro zenon_H63. zenon_intro zenon_H62. % 0.14/0.45 apply (zenon_notimply_s _ _ zenon_H62). zenon_intro zenon_H65. zenon_intro zenon_H64. % 0.14/0.45 generalize (transitive zenon_Tx_do). zenon_intro zenon_H66. % 0.14/0.45 generalize (zenon_H66 zenon_Ty_dq). zenon_intro zenon_H67. % 0.14/0.45 generalize (zenon_H67 zenon_Tz_ds). zenon_intro zenon_H68. % 0.14/0.45 apply (zenon_imply_s _ _ zenon_H68); [ zenon_intro zenon_H6a | zenon_intro zenon_H69 ]. % 0.14/0.45 apply (zenon_notand_s _ _ zenon_H6a); [ zenon_intro zenon_H6c | zenon_intro zenon_H6b ]. % 0.14/0.45 exact (zenon_H6c zenon_H63). % 0.14/0.45 exact (zenon_H6b zenon_H65). % 0.14/0.45 exact (zenon_H64 zenon_H69). % 0.14/0.45 Qed. % 0.14/0.45 % SZS output end Proof % 0.14/0.45 (* END-PROOF *) % 0.14/0.45 nodes searched: 316 % 0.14/0.45 max branch formulas: 252 % 0.14/0.45 proof nodes created: 23 % 0.14/0.45 formulas created: 2425 % 0.14/0.45 %------------------------------------------------------------------------------