%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT094+1 : TPTP v9.3.1. Bugfixed v9.3.1. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n029.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.15s 0.80s % Output : Proof 0.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT094+1 : TPTP v9.3.1. Bugfixed v9.3.1. % 0.00/0.04 % Command : run_zenon %s %d % 0.11/0.36 % Computer : n029.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.36 % CPULimit : 300 % 0.11/0.36 % WCLimit : 300 % 0.11/0.36 % DateTime : Mon Sep 7 14:27:26 UTC 2026 % 0.11/0.36 % CPUTime : % 0.15/0.80 (* PROOF-FOUND *) % 0.15/0.80 % SZS status Theorem % 0.15/0.80 (* BEGIN-PROOF *) % 0.15/0.80 % SZS output start Proof % 0.15/0.80 Theorem odrl653 : ((subs_verdict (v0) (v800) (present) (v0) (v600) (present)) = (conflict)). % 0.15/0.80 Proof. % 0.15/0.80 apply NNPP. intro zenon_G. % 0.15/0.80 generalize (axis_subsumes_def (v0)). zenon_intro zenon_H50. % 0.15/0.80 generalize (zenon_H50 (v800)). zenon_intro zenon_H51. % 0.15/0.80 generalize (zenon_H51 (v0)). zenon_intro zenon_H52. % 0.15/0.80 generalize (zenon_H52 (v600)). zenon_intro zenon_H53. % 0.15/0.80 apply (zenon_equiv_s _ _ zenon_H53); [ zenon_intro no_subs_hint; zenon_intro zenon_H56 | zenon_intro zenon_H55; zenon_intro zenon_H54 ]. % 0.15/0.80 generalize (subs_present_no (v0)). zenon_intro zenon_H57. % 0.15/0.80 generalize (zenon_H57 (v800)). zenon_intro zenon_H58. % 0.15/0.80 generalize (zenon_H58 (v0)). zenon_intro zenon_H59. % 0.15/0.80 generalize (zenon_H59 (v600)). zenon_intro zenon_H5a. % 0.15/0.80 apply (zenon_imply_s _ _ zenon_H5a); [ zenon_intro zenon_H5c | zenon_intro zenon_H5b ]. % 0.15/0.80 apply zenon_H5c. zenon_intro zenon_H55. % 0.15/0.80 generalize (axis_subsumes_def (v0)). zenon_intro zenon_H50. % 0.15/0.80 generalize (zenon_H50 (v800)). zenon_intro zenon_H51. % 0.15/0.80 generalize (zenon_H51 (v0)). zenon_intro zenon_H52. % 0.15/0.80 generalize (zenon_H52 (v600)). zenon_intro zenon_H53. % 0.15/0.80 apply (zenon_equiv_s _ _ zenon_H53); [ zenon_intro no_subs_hint; zenon_intro zenon_H56 | zenon_intro zenon_H55; zenon_intro zenon_H54 ]. % 0.15/0.80 exact (no_subs_hint zenon_H55). % 0.15/0.80 exact (zenon_H56 zenon_H54). % 0.15/0.80 exact (zenon_G zenon_H5b). % 0.15/0.80 exact (no_subs_hint zenon_H55). % 0.15/0.80 Qed. % 0.15/0.80 % SZS output end Proof % 0.15/0.80 (* END-PROOF *) % 0.15/0.80 nodes searched: 12513 % 0.15/0.80 max branch formulas: 1640 % 0.15/0.80 proof nodes created: 184 % 0.15/0.80 formulas created: 16018 % 0.15/0.80 %------------------------------------------------------------------------------