%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT049+1 : TPTP v9.3.0. Released v2.4.0. % 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:23 AM UTC 2026 % Result : Theorem 5.24s 5.53s % Output : Proof 5.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : MGT049+1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.06 % Command : run_zenon %s %d % 0.16/0.42 % Computer : n020.cluster.edu % 0.16/0.42 % Model : x86_64 x86_64 % 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.42 % Memory : 8046.5625MB % 0.16/0.42 % OS : Linux 6.8.0-71-generic % 0.16/0.42 % CPULimit : 300 % 0.16/0.42 % WCLimit : 300 % 0.16/0.42 % DateTime : Mon Sep 7 13:16:43 UTC 2026 % 0.16/0.42 % CPUTime : % 5.24/5.53 (* PROOF-FOUND *) % 5.24/5.53 % SZS status Theorem % 5.24/5.53 (* BEGIN-PROOF *) % 5.24/5.53 % SZS output start Proof % 5.24/5.53 Theorem lemma_6 : (forall X : zenon_U, (forall T0 : zenon_U, (forall T : zenon_U, (((organization X)/\(greater (age X T) (age X T0)))->((position X T) = (position X T0)))))). % 5.24/5.53 Proof. % 5.24/5.53 assert (zenon_L1_ : forall (zenon_TT_n : zenon_U) (zenon_TX_o : zenon_U), (forall T : zenon_U, ((organization zenon_TX_o)->((external_ties zenon_TX_o T) = (external_ties zenon_TX_o zenon_E)))) -> (organization zenon_TX_o) -> (~((external_ties zenon_TX_o zenon_E) = (external_ties zenon_TX_o zenon_TT_n))) -> False). % 5.24/5.53 do 2 intro. intros zenon_Ha zenon_Hb zenon_Hc. % 5.24/5.53 generalize (zenon_Ha zenon_TT_n). zenon_intro zenon_Hf. % 5.24/5.53 apply (zenon_imply_s _ _ zenon_Hf); [ zenon_intro zenon_H11 | zenon_intro zenon_H10 ]. % 5.24/5.53 exact (zenon_H11 zenon_Hb). % 5.24/5.53 apply zenon_Hc. apply sym_equal. exact zenon_H10. % 5.24/5.53 (* end of lemma zenon_L1_ *) % 5.24/5.53 assert (zenon_L2_ : forall (zenon_TT_n : zenon_U) (zenon_TT0_v : zenon_U) (zenon_TX_o : zenon_U), (~(greater (external_ties zenon_TX_o zenon_TT0_v) (external_ties zenon_TX_o zenon_TT_n))) -> (~((external_ties zenon_TX_o zenon_TT0_v) = (external_ties zenon_TX_o zenon_TT_n))) -> (~(greater (external_ties zenon_TX_o zenon_TT_n) (external_ties zenon_TX_o zenon_TT0_v))) -> False). % 5.24/5.53 do 3 intro. intros zenon_H12 zenon_H13 zenon_H14. % 5.24/5.53 generalize (meaning_postulate_greater_comparable (external_ties zenon_TX_o zenon_TT0_v)). zenon_intro zenon_H16. % 5.24/5.53 generalize (zenon_H16 (external_ties zenon_TX_o zenon_TT_n)). zenon_intro zenon_H17. % 5.24/5.53 apply (zenon_or_s _ _ zenon_H17); [ zenon_intro zenon_H19 | zenon_intro zenon_H18 ]. % 5.24/5.53 generalize (definition_smaller (external_ties zenon_TX_o zenon_TT0_v)). zenon_intro zenon_H1a. % 5.24/5.53 generalize (zenon_H1a (external_ties zenon_TX_o zenon_TT_n)). zenon_intro zenon_H1b. % 5.24/5.53 apply (zenon_equiv_s _ _ zenon_H1b); [ zenon_intro zenon_H1d; zenon_intro zenon_H14 | zenon_intro zenon_H19; zenon_intro zenon_H1c ]. % 5.24/5.53 exact (zenon_H1d zenon_H19). % 5.24/5.53 exact (zenon_H14 zenon_H1c). % 5.24/5.53 apply (zenon_or_s _ _ zenon_H18); [ zenon_intro zenon_H1f | zenon_intro zenon_H1e ]. % 5.24/5.53 exact (zenon_H13 zenon_H1f). % 5.24/5.53 exact (zenon_H12 zenon_H1e). % 5.24/5.53 (* end of lemma zenon_L2_ *) % 5.24/5.53 assert (zenon_L3_ : forall (zenon_TT_n : zenon_U) (zenon_TX_o : zenon_U), (forall T : zenon_U, ((organization zenon_TX_o)->((external_ties zenon_TX_o T) = (external_ties zenon_TX_o zenon_E)))) -> (organization zenon_TX_o) -> (~((external_ties zenon_TX_o zenon_TT_n) = (external_ties zenon_TX_o zenon_E))) -> False). % 5.24/5.53 do 2 intro. intros zenon_Ha zenon_Hb zenon_H20. % 5.24/5.53 generalize (zenon_Ha zenon_TT_n). zenon_intro zenon_Hf. % 5.24/5.53 apply (zenon_imply_s _ _ zenon_Hf); [ zenon_intro zenon_H11 | zenon_intro zenon_H10 ]. % 5.24/5.53 exact (zenon_H11 zenon_Hb). % 5.24/5.53 exact (zenon_H20 zenon_H10). % 5.24/5.53 (* end of lemma zenon_L3_ *) % 5.24/5.53 assert (zenon_L4_ : forall (zenon_TT0_v : zenon_U) (zenon_TT_n : zenon_U) (zenon_TX_o : zenon_U), (~((position zenon_TX_o zenon_TT_n) = (position zenon_TX_o zenon_TT0_v))) -> (~(greater (external_ties zenon_TX_o zenon_TT_n) (external_ties zenon_TX_o zenon_TT0_v))) -> (organization zenon_TX_o) -> (forall T : zenon_U, ((organization zenon_TX_o)->(((greater (external_ties zenon_TX_o T) (external_ties zenon_TX_o zenon_TT_n))->(greater (position zenon_TX_o T) (position zenon_TX_o zenon_TT_n)))/\(((external_ties zenon_TX_o T) = (external_ties zenon_TX_o zenon_TT_n))->((position zenon_TX_o T) = (position zenon_TX_o zenon_TT_n)))))) -> (forall T : zenon_U, ((organization zenon_TX_o)->((external_ties zenon_TX_o T) = (external_ties zenon_TX_o zenon_E)))) -> (~(greater (external_ties zenon_TX_o zenon_TT_n) (external_ties zenon_TX_o zenon_TT_n))) -> ((external_ties zenon_TX_o zenon_TT0_v) = (external_ties zenon_TX_o zenon_E)) -> False). % 5.24/5.53 do 3 intro. intros zenon_H21 zenon_H14 zenon_Hb zenon_H22 zenon_Ha zenon_H23 zenon_H24. % 5.24/5.53 elim (classic ((external_ties zenon_TX_o zenon_E) = (external_ties zenon_TX_o zenon_TT0_v))); [ zenon_intro zenon_H25 | zenon_intro zenon_H26 ]. % 5.24/5.53 elim (classic (greater (external_ties zenon_TX_o zenon_TT0_v) (external_ties zenon_TX_o zenon_TT_n))); [ zenon_intro zenon_H1e | zenon_intro zenon_H12 ]. % 5.24/5.53 elim (classic (greater (external_ties zenon_TX_o zenon_E) (external_ties zenon_TX_o zenon_TT_n))); [ zenon_intro zenon_H27 | zenon_intro zenon_H28 ]. % 5.24/5.53 cut ((greater (external_ties zenon_TX_o zenon_E) (external_ties zenon_TX_o zenon_TT_n)) = (greater (external_ties zenon_TX_o zenon_TT_n) (external_ties zenon_TX_o zenon_TT_n))). % 5.24/5.53 intro zenon_D_pnotp. % 5.24/5.53 apply zenon_H23. % 5.24/5.53 rewrite <- zenon_D_pnotp. % 5.24/5.53 exact zenon_H27. % 5.24/5.53 cut (((external_ties zenon_TX_o zenon_TT_n) = (external_ties zenon_TX_o zenon_TT_n))); [idtac | apply NNPP; zenon_intro zenon_H29]. % 5.24/5.53 cut (((external_ties zenon_TX_o zenon_E) = (external_ties zenon_TX_o zenon_TT_n))); [idtac | apply NNPP; zenon_intro zenon_Hc]. % 5.24/5.53 congruence. % 5.24/5.53 elim (classic ((external_ties zenon_TX_o zenon_TT_n) = (external_ties zenon_TX_o zenon_TT_n))); [ zenon_intro zenon_H2a | zenon_intro zenon_H29 ]. % 5.24/5.53 cut (((external_ties zenon_TX_o zenon_TT_n) = (external_ties zenon_TX_o zenon_TT_n)) = ((external_ties zenon_TX_o zenon_E) = (external_ties zenon_TX_o zenon_TT_n))). % 5.24/5.53 intro zenon_D_pnotp. % 5.24/5.53 apply zenon_Hc. % 5.24/5.53 rewrite <- zenon_D_pnotp. % 5.24/5.53 exact zenon_H2a. % 5.24/5.53 cut (((external_ties zenon_TX_o zenon_TT_n) = (external_ties zenon_TX_o zenon_TT_n))); [idtac | apply NNPP; zenon_intro zenon_H29]. % 5.24/5.53 cut (((external_ties zenon_TX_o zenon_TT_n) = (external_ties zenon_TX_o zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H20]. % 5.24/5.53 congruence. % 5.24/5.53 apply (zenon_L3_ zenon_TT_n zenon_TX_o); trivial. % 5.24/5.53 apply zenon_H29. apply refl_equal. % 5.24/5.53 apply zenon_H29. apply refl_equal. % 5.24/5.53 apply zenon_H29. apply refl_equal. % 5.24/5.53 cut ((greater (external_ties zenon_TX_o zenon_TT0_v) (external_ties zenon_TX_o zenon_TT_n)) = (greater (external_ties zenon_TX_o zenon_E) (external_ties zenon_TX_o zenon_TT_n))). % 5.24/5.53 intro zenon_D_pnotp. % 5.24/5.53 apply zenon_H28. % 5.24/5.53 rewrite <- zenon_D_pnotp. % 5.24/5.53 exact zenon_H1e. % 5.24/5.53 cut (((external_ties zenon_TX_o zenon_TT_n) = (external_ties zenon_TX_o zenon_TT_n))); [idtac | apply NNPP; zenon_intro zenon_H29]. % 5.24/5.53 cut (((external_ties zenon_TX_o zenon_TT0_v) = (external_ties zenon_TX_o zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H2b]. % 5.24/5.53 congruence. % 5.24/5.53 elim (classic ((external_ties zenon_TX_o zenon_E) = (external_ties zenon_TX_o zenon_E))); [ zenon_intro zenon_H2c | zenon_intro zenon_H2d ]. % 5.24/5.53 cut (((external_ties zenon_TX_o zenon_E) = (external_ties zenon_TX_o zenon_E)) = ((external_ties zenon_TX_o zenon_TT0_v) = (external_ties zenon_TX_o zenon_E))). % 5.24/5.53 intro zenon_D_pnotp. % 5.24/5.53 apply zenon_H2b. % 5.24/5.53 rewrite <- zenon_D_pnotp. % 5.24/5.53 exact zenon_H2c. % 5.24/5.53 cut (((external_ties zenon_TX_o zenon_E) = (external_ties zenon_TX_o zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H2d]. % 5.24/5.53 cut (((external_ties zenon_TX_o zenon_E) = (external_ties zenon_TX_o zenon_TT0_v))); [idtac | apply NNPP; zenon_intro zenon_H26]. % 5.24/5.53 congruence. % 5.24/5.53 exact (zenon_H26 zenon_H25). % 5.24/5.53 apply zenon_H2d. apply refl_equal. % 5.24/5.53 apply zenon_H2d. apply refl_equal. % 5.24/5.53 apply zenon_H29. apply refl_equal. % 5.24/5.53 generalize (zenon_H22 zenon_TT0_v). zenon_intro zenon_H2e. % 5.24/5.53 apply (zenon_imply_s _ _ zenon_H2e); [ zenon_intro zenon_H11 | zenon_intro zenon_H2f ]. % 5.24/5.53 exact (zenon_H11 zenon_Hb). % 5.24/5.53 apply (zenon_and_s _ _ zenon_H2f). zenon_intro zenon_H31. zenon_intro zenon_H30. % 5.24/5.53 apply (zenon_imply_s _ _ zenon_H30); [ zenon_intro zenon_H13 | zenon_intro zenon_H32 ]. % 5.24/5.53 apply (zenon_L2_ zenon_TT_n zenon_TT0_v zenon_TX_o); trivial. % 5.24/5.53 apply zenon_H21. apply sym_equal. exact zenon_H32. % 5.24/5.53 elim (classic ((external_ties zenon_TX_o zenon_TT0_v) = (external_ties zenon_TX_o zenon_TT0_v))); [ zenon_intro zenon_H33 | zenon_intro zenon_H34 ]. % 5.24/5.53 cut (((external_ties zenon_TX_o zenon_TT0_v) = (external_ties zenon_TX_o zenon_TT0_v)) = ((external_ties zenon_TX_o zenon_E) = (external_ties zenon_TX_o zenon_TT0_v))). % 5.24/5.53 intro zenon_D_pnotp. % 5.24/5.53 apply zenon_H26. % 5.24/5.53 rewrite <- zenon_D_pnotp. % 5.24/5.53 exact zenon_H33. % 5.24/5.53 cut (((external_ties zenon_TX_o zenon_TT0_v) = (external_ties zenon_TX_o zenon_TT0_v))); [idtac | apply NNPP; zenon_intro zenon_H34]. % 5.24/5.53 cut (((external_ties zenon_TX_o zenon_TT0_v) = (external_ties zenon_TX_o zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H2b]. % 5.24/5.53 congruence. % 5.24/5.53 exact (zenon_H2b zenon_H24). % 5.24/5.53 apply zenon_H34. apply refl_equal. % 5.24/5.53 apply zenon_H34. apply refl_equal. % 5.24/5.53 (* end of lemma zenon_L4_ *) % 5.24/5.53 apply NNPP. intro zenon_G. % 5.24/5.53 apply (zenon_notallex_s (fun X : zenon_U => (forall T0 : zenon_U, (forall T : zenon_U, (((organization X)/\(greater (age X T) (age X T0)))->((position X T) = (position X T0)))))) zenon_G); [ zenon_intro zenon_H35; idtac ]. % 5.24/5.54 elim zenon_H35. zenon_intro zenon_TX_o. zenon_intro zenon_H36. % 5.24/5.54 apply (zenon_notallex_s (fun T0 : zenon_U => (forall T : zenon_U, (((organization zenon_TX_o)/\(greater (age zenon_TX_o T) (age zenon_TX_o T0)))->((position zenon_TX_o T) = (position zenon_TX_o T0))))) zenon_H36); [ zenon_intro zenon_H37; idtac ]. % 5.24/5.54 elim zenon_H37. zenon_intro zenon_TT0_v. zenon_intro zenon_H38. % 5.24/5.54 apply (zenon_notallex_s (fun T : zenon_U => (((organization zenon_TX_o)/\(greater (age zenon_TX_o T) (age zenon_TX_o zenon_TT0_v)))->((position zenon_TX_o T) = (position zenon_TX_o zenon_TT0_v)))) zenon_H38); [ zenon_intro zenon_H39; idtac ]. % 5.24/5.54 elim zenon_H39. zenon_intro zenon_TT_n. zenon_intro zenon_H3a. % 5.24/5.54 apply (zenon_notimply_s _ _ zenon_H3a). zenon_intro zenon_H3b. zenon_intro zenon_H21. % 5.24/5.54 apply (zenon_and_s _ _ zenon_H3b). zenon_intro zenon_Hb. zenon_intro zenon_H3c. % 5.24/5.54 generalize (assumption_6 zenon_TX_o). zenon_intro zenon_H3d. % 5.24/5.54 generalize (zenon_H3d zenon_TT_n). zenon_intro zenon_H22. % 5.24/5.54 generalize (zenon_H22 zenon_TT_n). zenon_intro zenon_H3e. % 5.24/5.54 apply (zenon_imply_s _ _ zenon_H3e); [ zenon_intro zenon_H11 | zenon_intro zenon_H3f ]. % 5.24/5.54 exact (zenon_H11 zenon_Hb). % 5.24/5.54 apply (zenon_and_s _ _ zenon_H3f). zenon_intro zenon_H41. zenon_intro zenon_H40. % 5.24/5.54 apply (zenon_imply_s _ _ zenon_H41); [ zenon_intro zenon_H23 | zenon_intro zenon_H42 ]. % 5.24/5.54 generalize (assumption_11 zenon_TX_o). zenon_intro zenon_H0. % 5.24/5.54 generalize (zenon_H0 zenon_E). zenon_intro zenon_Ha. % 5.24/5.54 generalize (zenon_Ha zenon_TT0_v). zenon_intro zenon_H43. % 5.24/5.54 apply (zenon_imply_s _ _ zenon_H43); [ zenon_intro zenon_H11 | zenon_intro zenon_H24 ]. % 5.24/5.54 exact (zenon_H11 zenon_Hb). % 5.24/5.54 elim (classic (greater (external_ties zenon_TX_o zenon_TT_n) (external_ties zenon_TX_o zenon_TT0_v))); [ zenon_intro zenon_H1c | zenon_intro zenon_H14 ]. % 5.24/5.54 elim (classic (greater (external_ties zenon_TX_o zenon_TT_n) (external_ties zenon_TX_o zenon_E))); [ zenon_intro zenon_H44 | zenon_intro zenon_H45 ]. % 5.24/5.54 cut ((greater (external_ties zenon_TX_o zenon_TT_n) (external_ties zenon_TX_o zenon_E)) = (greater (external_ties zenon_TX_o zenon_TT_n) (external_ties zenon_TX_o zenon_TT_n))). % 5.24/5.54 intro zenon_D_pnotp. % 5.24/5.54 apply zenon_H23. % 5.24/5.54 rewrite <- zenon_D_pnotp. % 5.24/5.54 exact zenon_H44. % 5.24/5.54 cut (((external_ties zenon_TX_o zenon_E) = (external_ties zenon_TX_o zenon_TT_n))); [idtac | apply NNPP; zenon_intro zenon_Hc]. % 5.24/5.54 cut (((external_ties zenon_TX_o zenon_TT_n) = (external_ties zenon_TX_o zenon_TT_n))); [idtac | apply NNPP; zenon_intro zenon_H29]. % 5.24/5.54 congruence. % 5.24/5.54 apply zenon_H29. apply refl_equal. % 5.24/5.54 apply (zenon_L1_ zenon_TT_n zenon_TX_o); trivial. % 5.24/5.54 cut ((greater (external_ties zenon_TX_o zenon_TT_n) (external_ties zenon_TX_o zenon_TT0_v)) = (greater (external_ties zenon_TX_o zenon_TT_n) (external_ties zenon_TX_o zenon_E))). % 5.24/5.54 intro zenon_D_pnotp. % 5.24/5.54 apply zenon_H45. % 5.24/5.54 rewrite <- zenon_D_pnotp. % 5.24/5.54 exact zenon_H1c. % 5.24/5.54 cut (((external_ties zenon_TX_o zenon_TT0_v) = (external_ties zenon_TX_o zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H2b]. % 5.24/5.54 cut (((external_ties zenon_TX_o zenon_TT_n) = (external_ties zenon_TX_o zenon_TT_n))); [idtac | apply NNPP; zenon_intro zenon_H29]. % 5.24/5.54 congruence. % 5.24/5.54 apply zenon_H29. apply refl_equal. % 5.24/5.54 exact (zenon_H2b zenon_H24). % 5.24/5.54 apply (zenon_L4_ zenon_TT0_v zenon_TT_n zenon_TX_o); trivial. % 5.24/5.54 generalize (meaning_postulate_greater_strict (position zenon_TX_o zenon_TT_n)). zenon_intro zenon_H46. % 5.24/5.54 generalize (zenon_H46 (position zenon_TX_o zenon_TT_n)). zenon_intro zenon_H47. % 5.24/5.54 apply (zenon_notand_s _ _ zenon_H47); [ zenon_intro zenon_H48 | zenon_intro zenon_H48 ]. % 5.24/5.54 exact (zenon_H48 zenon_H42). % 5.24/5.54 exact (zenon_H48 zenon_H42). % 5.24/5.54 Qed. % 5.24/5.54 % SZS output end Proof % 5.24/5.54 (* END-PROOF *) % 5.24/5.54 nodes searched: 106309 % 5.24/5.54 max branch formulas: 931 % 5.24/5.54 proof nodes created: 1427 % 5.24/5.54 formulas created: 20969 % 5.24/5.54 %------------------------------------------------------------------------------