%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT020+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n028.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:18 AM UTC 2026 % Result : Theorem 0.39s 0.63s % Output : Proof 0.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : MGT020+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.06 % Command : run_zenon %s %d % 0.18/0.43 % Computer : n028.cluster.edu % 0.18/0.43 % Model : x86_64 x86_64 % 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.43 % Memory : 8046.5625MB % 0.18/0.43 % OS : Linux 6.8.0-71-generic % 0.18/0.43 % CPULimit : 300 % 0.18/0.44 % WCLimit : 300 % 0.18/0.44 % DateTime : Mon Sep 7 12:02:32 UTC 2026 % 0.18/0.44 % CPUTime : % 0.39/0.63 (* PROOF-FOUND *) % 0.39/0.63 % SZS status Theorem % 0.39/0.63 (* BEGIN-PROOF *) % 0.39/0.63 % SZS output start Proof % 0.39/0.63 Theorem prove_l2 : (forall E : zenon_U, (forall T : zenon_U, (((environment E)/\(subpopulations (first_movers) (efficient_producers) E T))->(greater (disbanding_rate (first_movers) T) (disbanding_rate (efficient_producers) T))))). % 0.39/0.63 Proof. % 0.39/0.63 assert (zenon_L1_ : forall (zenon_TT_p : zenon_U) (zenon_TE_q : zenon_U), (forall T : zenon_U, ((environment zenon_TE_q)->(((in_environment zenon_TE_q (initial_FM_EP zenon_TE_q))->(subpopulations (first_movers) (efficient_producers) zenon_TE_q (initial_FM_EP zenon_TE_q)))/\((subpopulations (first_movers) (efficient_producers) zenon_TE_q T)->(greater_or_equal T (initial_FM_EP zenon_TE_q)))))) -> (environment zenon_TE_q) -> (subpopulations (first_movers) (efficient_producers) zenon_TE_q zenon_TT_p) -> (~(greater_or_equal zenon_TT_p (initial_FM_EP zenon_TE_q))) -> False). % 0.39/0.63 do 2 intro. intros zenon_H0 zenon_Hc zenon_Hd zenon_He. % 0.39/0.63 generalize (zenon_H0 zenon_TT_p). zenon_intro zenon_H11. % 0.39/0.63 apply (zenon_imply_s _ _ zenon_H11); [ zenon_intro zenon_H13 | zenon_intro zenon_H12 ]. % 0.39/0.63 exact (zenon_H13 zenon_Hc). % 0.39/0.63 apply (zenon_and_s _ _ zenon_H12). zenon_intro zenon_H15. zenon_intro zenon_H14. % 0.39/0.63 apply (zenon_imply_s _ _ zenon_H14); [ zenon_intro zenon_H17 | zenon_intro zenon_H16 ]. % 0.39/0.63 exact (zenon_H17 zenon_Hd). % 0.39/0.63 exact (zenon_He zenon_H16). % 0.39/0.63 (* end of lemma zenon_L1_ *) % 0.39/0.63 assert (zenon_L2_ : (~((first_movers) = (first_movers))) -> False). % 0.39/0.63 do 0 intro. intros zenon_H18. % 0.39/0.63 apply zenon_H18. apply refl_equal. % 0.39/0.63 (* end of lemma zenon_L2_ *) % 0.39/0.63 assert (zenon_L3_ : forall (zenon_TT_p : zenon_U) (zenon_TE_q : zenon_U), (~((disbanding_rate (first_movers) (initial_FM_EP zenon_TE_q)) = (disbanding_rate (first_movers) zenon_TT_p))) -> (zenon_TT_p = (initial_FM_EP zenon_TE_q)) -> False). % 0.39/0.63 do 2 intro. intros zenon_H19 zenon_H1a. % 0.39/0.63 cut (((initial_FM_EP zenon_TE_q) = zenon_TT_p)); [idtac | apply NNPP; zenon_intro zenon_H1b]. % 0.39/0.63 cut (((first_movers) = (first_movers))); [idtac | apply NNPP; zenon_intro zenon_H18]. % 0.39/0.63 congruence. % 0.39/0.63 apply zenon_H18. apply refl_equal. % 0.39/0.63 apply zenon_H1b. apply sym_equal. exact zenon_H1a. % 0.39/0.63 (* end of lemma zenon_L3_ *) % 0.39/0.63 assert (zenon_L4_ : (~((efficient_producers) = (efficient_producers))) -> False). % 0.39/0.63 do 0 intro. intros zenon_H1c. % 0.39/0.63 apply zenon_H1c. apply refl_equal. % 0.39/0.63 (* end of lemma zenon_L4_ *) % 0.39/0.63 assert (zenon_L5_ : forall (zenon_TT_p : zenon_U) (zenon_TE_q : zenon_U), (~((disbanding_rate (efficient_producers) (initial_FM_EP zenon_TE_q)) = (disbanding_rate (efficient_producers) zenon_TT_p))) -> (zenon_TT_p = (initial_FM_EP zenon_TE_q)) -> False). % 0.39/0.63 do 2 intro. intros zenon_H1d zenon_H1a. % 0.39/0.63 cut (((initial_FM_EP zenon_TE_q) = zenon_TT_p)); [idtac | apply NNPP; zenon_intro zenon_H1b]. % 0.39/0.63 cut (((efficient_producers) = (efficient_producers))); [idtac | apply NNPP; zenon_intro zenon_H1c]. % 0.39/0.63 congruence. % 0.39/0.63 apply zenon_H1c. apply refl_equal. % 0.39/0.63 apply zenon_H1b. apply sym_equal. exact zenon_H1a. % 0.39/0.63 (* end of lemma zenon_L5_ *) % 0.39/0.63 assert (zenon_L6_ : forall (zenon_TT_p : zenon_U) (zenon_TE_q : zenon_U), (forall T1 : zenon_U, (forall T2 : zenon_U, (((environment zenon_TE_q)/\((greater_or_equal (initial_FM_EP zenon_TE_q) T1)/\((greater_or_equal T2 (initial_FM_EP zenon_TE_q))/\((subpopulations (first_movers) (efficient_producers) zenon_TE_q T2)/\(greater (disbanding_rate (first_movers) T1) (disbanding_rate (efficient_producers) T1))))))->((~(decreases (difference (disbanding_rate (first_movers) (initial_FM_EP zenon_TE_q)) (disbanding_rate (efficient_producers) (initial_FM_EP zenon_TE_q)))))->(greater (disbanding_rate (first_movers) T2) (disbanding_rate (efficient_producers) T2)))))) -> (~(greater (disbanding_rate (first_movers) zenon_TT_p) (disbanding_rate (efficient_producers) zenon_TT_p))) -> (subpopulations (first_movers) (efficient_producers) zenon_TE_q zenon_TT_p) -> (subpopulations (first_movers) (efficient_producers) zenon_TE_q (initial_FM_EP zenon_TE_q)) -> (forall T : zenon_U, ((environment zenon_TE_q)->(((in_environment zenon_TE_q (initial_FM_EP zenon_TE_q))->(subpopulations (first_movers) (efficient_producers) zenon_TE_q (initial_FM_EP zenon_TE_q)))/\((subpopulations (first_movers) (efficient_producers) zenon_TE_q T)->(greater_or_equal T (initial_FM_EP zenon_TE_q)))))) -> (environment zenon_TE_q) -> False). % 0.39/0.63 do 2 intro. intros zenon_H1e zenon_H1f zenon_Hd zenon_H20 zenon_H0 zenon_Hc. % 0.39/0.63 generalize (zenon_H1e (initial_FM_EP zenon_TE_q)). zenon_intro zenon_H21. % 0.39/0.63 generalize (zenon_H21 zenon_TT_p). zenon_intro zenon_H22. % 0.39/0.63 apply (zenon_imply_s _ _ zenon_H22); [ zenon_intro zenon_H24 | zenon_intro zenon_H23 ]. % 0.39/0.63 apply (zenon_notand_s _ _ zenon_H24); [ zenon_intro zenon_H13 | zenon_intro zenon_H25 ]. % 0.39/0.63 exact (zenon_H13 zenon_Hc). % 0.39/0.63 apply (zenon_notand_s _ _ zenon_H25); [ zenon_intro zenon_H27 | zenon_intro zenon_H26 ]. % 0.39/0.63 generalize (zenon_H0 (initial_FM_EP zenon_TE_q)). zenon_intro zenon_H28. % 0.39/0.63 apply (zenon_imply_s _ _ zenon_H28); [ zenon_intro zenon_H13 | zenon_intro zenon_H29 ]. % 0.39/0.63 exact (zenon_H13 zenon_Hc). % 0.39/0.63 apply (zenon_and_s _ _ zenon_H29). zenon_intro zenon_H15. zenon_intro zenon_H2a. % 0.39/0.63 apply (zenon_imply_s _ _ zenon_H2a); [ zenon_intro zenon_H2c | zenon_intro zenon_H2b ]. % 0.39/0.63 exact (zenon_H2c zenon_H20). % 0.39/0.63 exact (zenon_H27 zenon_H2b). % 0.39/0.63 apply (zenon_notand_s _ _ zenon_H26); [ zenon_intro zenon_He | zenon_intro zenon_H2d ]. % 0.39/0.63 apply (zenon_L1_ zenon_TT_p zenon_TE_q); trivial. % 0.39/0.63 apply (zenon_notand_s _ _ zenon_H2d); [ zenon_intro zenon_H17 | zenon_intro zenon_H2e ]. % 0.39/0.63 exact (zenon_H17 zenon_Hd). % 0.39/0.63 generalize (a8 zenon_TE_q). zenon_intro zenon_H2f. % 0.39/0.63 apply (zenon_imply_s _ _ zenon_H2f); [ zenon_intro zenon_H13 | zenon_intro zenon_H30 ]. % 0.39/0.63 exact (zenon_H13 zenon_Hc). % 0.39/0.63 exact (zenon_H2e zenon_H30). % 0.39/0.63 apply (zenon_imply_s _ _ zenon_H23); [ zenon_intro zenon_H32 | zenon_intro zenon_H31 ]. % 0.39/0.63 apply zenon_H32. zenon_intro zenon_H33. % 0.39/0.63 generalize (l3 zenon_TE_q). zenon_intro zenon_H34. % 0.39/0.63 generalize (zenon_H34 (initial_FM_EP zenon_TE_q)). zenon_intro zenon_H35. % 0.39/0.63 apply (zenon_imply_s _ _ zenon_H35); [ zenon_intro zenon_H37 | zenon_intro zenon_H36 ]. % 0.39/0.63 apply (zenon_notand_s _ _ zenon_H37); [ zenon_intro zenon_H13 | zenon_intro zenon_H2c ]. % 0.39/0.63 exact (zenon_H13 zenon_Hc). % 0.39/0.63 exact (zenon_H2c zenon_H20). % 0.39/0.63 exact (zenon_H36 zenon_H33). % 0.39/0.63 exact (zenon_H1f zenon_H31). % 0.39/0.63 (* end of lemma zenon_L6_ *) % 0.39/0.63 assert (zenon_L7_ : forall (zenon_TT_p : zenon_U) (zenon_TE_q : zenon_U), (forall T : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((environment zenon_TE_q)/\((greater_or_equal T T1)/\((greater_or_equal T2 T)/\((subpopulations (first_movers) (efficient_producers) zenon_TE_q T2)/\(greater (disbanding_rate (first_movers) T1) (disbanding_rate (efficient_producers) T1))))))->((~(decreases (difference (disbanding_rate (first_movers) T) (disbanding_rate (efficient_producers) T))))->(greater (disbanding_rate (first_movers) T2) (disbanding_rate (efficient_producers) T2))))))) -> (environment zenon_TE_q) -> (forall T : zenon_U, ((environment zenon_TE_q)->(((in_environment zenon_TE_q (initial_FM_EP zenon_TE_q))->(subpopulations (first_movers) (efficient_producers) zenon_TE_q (initial_FM_EP zenon_TE_q)))/\((subpopulations (first_movers) (efficient_producers) zenon_TE_q T)->(greater_or_equal T (initial_FM_EP zenon_TE_q)))))) -> (subpopulations (first_movers) (efficient_producers) zenon_TE_q (initial_FM_EP zenon_TE_q)) -> (subpopulations (first_movers) (efficient_producers) zenon_TE_q zenon_TT_p) -> (~(greater (disbanding_rate (first_movers) zenon_TT_p) (disbanding_rate (efficient_producers) zenon_TT_p))) -> False). % 0.39/0.63 do 2 intro. intros zenon_H38 zenon_Hc zenon_H0 zenon_H20 zenon_Hd zenon_H1f. % 0.39/0.63 generalize (zenon_H38 (initial_FM_EP zenon_TE_q)). zenon_intro zenon_H1e. % 0.39/0.63 apply (zenon_L6_ zenon_TT_p zenon_TE_q); trivial. % 0.39/0.63 (* end of lemma zenon_L7_ *) % 0.39/0.63 apply NNPP. intro zenon_G. % 0.39/0.63 apply (zenon_notallex_s (fun E : zenon_U => (forall T : zenon_U, (((environment E)/\(subpopulations (first_movers) (efficient_producers) E T))->(greater (disbanding_rate (first_movers) T) (disbanding_rate (efficient_producers) T))))) zenon_G); [ zenon_intro zenon_H39; idtac ]. % 0.39/0.63 elim zenon_H39. zenon_intro zenon_TE_q. zenon_intro zenon_H3a. % 0.39/0.63 apply (zenon_notallex_s (fun T : zenon_U => (((environment zenon_TE_q)/\(subpopulations (first_movers) (efficient_producers) zenon_TE_q T))->(greater (disbanding_rate (first_movers) T) (disbanding_rate (efficient_producers) T)))) zenon_H3a); [ zenon_intro zenon_H3b; idtac ]. % 0.39/0.63 elim zenon_H3b. zenon_intro zenon_TT_p. zenon_intro zenon_H3c. % 0.39/0.63 apply (zenon_notimply_s _ _ zenon_H3c). zenon_intro zenon_H3d. zenon_intro zenon_H1f. % 0.39/0.63 apply (zenon_and_s _ _ zenon_H3d). zenon_intro zenon_Hc. zenon_intro zenon_Hd. % 0.39/0.63 generalize (mp_time_point_occurs zenon_TE_q). zenon_intro zenon_H3e. % 0.39/0.63 generalize (mp_times_in_order zenon_TE_q). zenon_intro zenon_H3f. % 0.39/0.63 generalize (zenon_H3e zenon_TT_p). zenon_intro zenon_H40. % 0.39/0.63 apply (zenon_imply_s _ _ zenon_H40); [ zenon_intro zenon_H42 | zenon_intro zenon_H41 ]. % 0.39/0.63 apply (zenon_notand_s _ _ zenon_H42); [ zenon_intro zenon_H13 | zenon_intro zenon_H17 ]. % 0.39/0.63 exact (zenon_H13 zenon_Hc). % 0.39/0.63 exact (zenon_H17 zenon_Hd). % 0.39/0.63 generalize (mp_positive_function_difference zenon_TE_q). zenon_intro zenon_H38. % 0.39/0.63 generalize (mp_earliest_time_point zenon_TE_q). zenon_intro zenon_H0. % 0.39/0.63 generalize (zenon_H0 zenon_E). zenon_intro zenon_H43. % 0.39/0.63 apply (zenon_imply_s _ _ zenon_H43); [ zenon_intro zenon_H13 | zenon_intro zenon_H44 ]. % 0.39/0.63 exact (zenon_H13 zenon_Hc). % 0.39/0.63 apply (zenon_and_s _ _ zenon_H44). zenon_intro zenon_H15. zenon_intro zenon_H45. % 0.39/0.63 apply (zenon_imply_s _ _ zenon_H15); [ zenon_intro zenon_H46 | zenon_intro zenon_H20 ]. % 0.39/0.63 generalize (mp_initial_time zenon_TE_q). zenon_intro zenon_H47. % 0.39/0.63 apply (zenon_imply_s _ _ zenon_H47); [ zenon_intro zenon_H13 | zenon_intro zenon_H48 ]. % 0.39/0.63 exact (zenon_H13 zenon_Hc). % 0.39/0.63 generalize (zenon_H3f (initial_FM_EP zenon_TE_q)). zenon_intro zenon_H49. % 0.39/0.63 generalize (zenon_H49 zenon_TT_p). zenon_intro zenon_H4a. % 0.39/0.63 apply (zenon_imply_s _ _ zenon_H4a); [ zenon_intro zenon_H4c | zenon_intro zenon_H4b ]. % 0.39/0.63 apply (zenon_notand_s _ _ zenon_H4c); [ zenon_intro zenon_H13 | zenon_intro zenon_H4d ]. % 0.39/0.63 exact (zenon_H13 zenon_Hc). % 0.39/0.63 apply (zenon_notand_s _ _ zenon_H4d); [ zenon_intro zenon_H4f | zenon_intro zenon_H4e ]. % 0.39/0.63 exact (zenon_H4f zenon_H48). % 0.39/0.63 apply (zenon_notand_s _ _ zenon_H4e); [ zenon_intro zenon_H51 | zenon_intro zenon_H50 ]. % 0.39/0.63 generalize (mp_greater_or_equal zenon_TT_p). zenon_intro zenon_H52. % 0.39/0.63 generalize (zenon_H52 (initial_FM_EP zenon_TE_q)). zenon_intro zenon_H53. % 0.39/0.63 apply (zenon_imply_s _ _ zenon_H53); [ zenon_intro zenon_He | zenon_intro zenon_H54 ]. % 0.39/0.63 apply (zenon_L1_ zenon_TT_p zenon_TE_q); trivial. % 0.39/0.63 apply (zenon_or_s _ _ zenon_H54); [ zenon_intro zenon_H55 | zenon_intro zenon_H1a ]. % 0.39/0.63 exact (zenon_H51 zenon_H55). % 0.39/0.63 generalize (a8 zenon_TE_q). zenon_intro zenon_H2f. % 0.39/0.63 apply (zenon_imply_s _ _ zenon_H2f); [ zenon_intro zenon_H13 | zenon_intro zenon_H30 ]. % 0.39/0.63 exact (zenon_H13 zenon_Hc). % 0.39/0.63 cut ((greater (disbanding_rate (first_movers) (initial_FM_EP zenon_TE_q)) (disbanding_rate (efficient_producers) (initial_FM_EP zenon_TE_q))) = (greater (disbanding_rate (first_movers) zenon_TT_p) (disbanding_rate (efficient_producers) zenon_TT_p))). % 0.39/0.63 intro zenon_D_pnotp. % 0.39/0.63 apply zenon_H1f. % 0.39/0.63 rewrite <- zenon_D_pnotp. % 0.39/0.63 exact zenon_H30. % 0.39/0.63 cut (((disbanding_rate (efficient_producers) (initial_FM_EP zenon_TE_q)) = (disbanding_rate (efficient_producers) zenon_TT_p))); [idtac | apply NNPP; zenon_intro zenon_H1d]. % 0.39/0.63 cut (((disbanding_rate (first_movers) (initial_FM_EP zenon_TE_q)) = (disbanding_rate (first_movers) zenon_TT_p))); [idtac | apply NNPP; zenon_intro zenon_H19]. % 0.39/0.63 congruence. % 0.39/0.63 apply (zenon_L3_ zenon_TT_p zenon_TE_q); trivial. % 0.39/0.63 apply (zenon_L5_ zenon_TT_p zenon_TE_q); trivial. % 0.39/0.63 exact (zenon_H50 zenon_H41). % 0.39/0.63 exact (zenon_H46 zenon_H4b). % 0.39/0.63 apply (zenon_L7_ zenon_TT_p zenon_TE_q); trivial. % 0.39/0.63 Qed. % 0.39/0.63 % SZS output end Proof % 0.39/0.63 (* END-PROOF *) % 0.39/0.63 nodes searched: 831 % 0.39/0.63 max branch formulas: 323 % 0.39/0.63 proof nodes created: 132 % 0.39/0.63 formulas created: 3069 % 0.39/0.63 %------------------------------------------------------------------------------