%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : MGT020+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% Command : run_E %s %d THM
% Computer : n002.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:23:58 AM UTC 2026
% Result : Theorem 0.08s 0.41s
% Output : Proof 0.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT020+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.03 % Command : run_E %s %d THM
% 0.08/0.35 % Computer : n002.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 7 12:03:53 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.41 % SZS status Theorem
% 0.08/0.41 % SZS output start Proof
% 0.08/0.41 tff(greater_or_equal_type, type, (
% 0.08/0.41 greater_or_equal: ( $i * $i ) > $o)).
% 0.08/0.41 tff(initial_FM_EP_type, type, (
% 0.08/0.41 initial_FM_EP: $i > $i)).
% 0.08/0.41 tff(tptp_fun_E_1_type, type, (
% 0.08/0.41 tptp_fun_E_1: $i)).
% 0.08/0.41 tff(subpopulations_type, type, (
% 0.08/0.41 subpopulations: ( $i * $i * $i * $i ) > $o)).
% 0.08/0.41 tff(efficient_producers_type, type, (
% 0.08/0.41 efficient_producers: $i)).
% 0.08/0.41 tff(first_movers_type, type, (
% 0.08/0.41 first_movers: $i)).
% 0.08/0.41 tff(in_environment_type, type, (
% 0.08/0.41 in_environment: ( $i * $i ) > $o)).
% 0.08/0.41 tff(environment_type, type, (
% 0.08/0.41 environment: $i > $o)).
% 0.08/0.41 tff(tptp_fun_T_0_type, type, (
% 0.08/0.41 tptp_fun_T_0: $i)).
% 0.08/0.41 tff(greater_type, type, (
% 0.08/0.41 greater: ( $i * $i ) > $o)).
% 0.08/0.41 tff(disbanding_rate_type, type, (
% 0.08/0.41 disbanding_rate: ( $i * $i ) > $i)).
% 0.08/0.41 tff(start_time_type, type, (
% 0.08/0.41 start_time: $i > $i)).
% 0.08/0.41 tff(decreases_type, type, (
% 0.08/0.41 decreases: $i > $o)).
% 0.08/0.41 tff(difference_type, type, (
% 0.08/0.41 difference: ( $i * $i ) > $i)).
% 0.08/0.41 tff(1,plain,
% 0.08/0.41 ((~![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | greater(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) <=> (~![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | greater(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))))),
% 0.08/0.41 inference(rewrite,[status(thm)],[])).
% 0.08/0.41 tff(2,plain,
% 0.08/0.41 ((~![E: $i, T: $i] : ((environment(E) & subpopulations(first_movers, efficient_producers, E, T)) => greater(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) <=> (~![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | greater(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))))),
% 0.08/0.41 inference(rewrite,[status(thm)],[])).
% 0.08/0.41 tff(3,axiom,(~![E: $i, T: $i] : ((environment(E) & subpopulations(first_movers, efficient_producers, E, T)) => greater(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove_l2')).
% 0.08/0.41 tff(4,plain,
% 0.08/0.41 (~![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | greater(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))),
% 0.08/0.41 inference(modus_ponens,[status(thm)],[3, 2])).
% 0.08/0.41 tff(5,plain,
% 0.08/0.41 (~![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | greater(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))),
% 0.08/0.41 inference(modus_ponens,[status(thm)],[4, 1])).
% 0.08/0.41 tff(6,plain,
% 0.08/0.41 (~![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | greater(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))),
% 0.08/0.41 inference(modus_ponens,[status(thm)],[5, 1])).
% 0.08/0.41 tff(7,plain,
% 0.08/0.41 (~![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | greater(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))),
% 0.08/0.41 inference(modus_ponens,[status(thm)],[6, 1])).
% 0.08/0.41 tff(8,plain,(
% 0.08/0.41 ~((~(environment(E!1) & subpopulations(first_movers, efficient_producers, E!1, T!0))) | greater(disbanding_rate(first_movers, T!0), disbanding_rate(efficient_producers, T!0)))),
% 0.08/0.41 inference(skolemize,[status(sab)],[7])).
% 0.08/0.41 tff(9,plain,
% 0.08/0.41 (environment(E!1) & subpopulations(first_movers, efficient_producers, E!1, T!0)),
% 0.08/0.41 inference(or_elim,[status(thm)],[8])).
% 0.08/0.41 tff(10,plain,
% 0.08/0.41 (environment(E!1)),
% 0.08/0.41 inference(and_elim,[status(thm)],[9])).
% 0.08/0.41 tff(11,plain,
% 0.08/0.41 (^[E: $i, T: $i] : refl(((~environment(E)) | (~((~((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E)))) | (~((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E))))))) <=> ((~environment(E)) | (~((~((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E)))) | (~((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E))))))))),
% 0.08/0.42 inference(bind,[status(th)],[])).
% 0.08/0.42 tff(12,plain,
% 0.08/0.42 (![E: $i, T: $i] : ((~environment(E)) | (~((~((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E)))) | (~((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E))))))) <=> ![E: $i, T: $i] : ((~environment(E)) | (~((~((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E)))) | (~((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))))),
% 0.08/0.42 inference(quant_intro,[status(thm)],[11])).
% 0.08/0.42 tff(13,plain,
% 0.08/0.42 (^[E: $i, T: $i] : rewrite(((~environment(E)) | (((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E))) & ((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E))))) <=> ((~environment(E)) | (~((~((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E)))) | (~((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E))))))))),
% 0.08/0.42 inference(bind,[status(th)],[])).
% 0.08/0.42 tff(14,plain,
% 0.08/0.42 (![E: $i, T: $i] : ((~environment(E)) | (((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E))) & ((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E))))) <=> ![E: $i, T: $i] : ((~environment(E)) | (~((~((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E)))) | (~((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))))),
% 0.08/0.42 inference(quant_intro,[status(thm)],[13])).
% 0.08/0.42 tff(15,plain,
% 0.08/0.42 (![E: $i, T: $i] : ((~environment(E)) | (((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E))) & ((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E))))) <=> ![E: $i, T: $i] : ((~environment(E)) | (((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E))) & ((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))),
% 0.08/0.42 inference(rewrite,[status(thm)],[])).
% 0.08/0.42 tff(16,plain,
% 0.08/0.42 (^[E: $i, T: $i] : trans(monotonicity(rewrite(((in_environment(E, initial_FM_EP(E)) => subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E))) & (subpopulations(first_movers, efficient_producers, E, T) => greater_or_equal(T, initial_FM_EP(E)))) <=> (((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E))) & ((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E))))), ((environment(E) => ((in_environment(E, initial_FM_EP(E)) => subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E))) & (subpopulations(first_movers, efficient_producers, E, T) => greater_or_equal(T, initial_FM_EP(E))))) <=> (environment(E) => (((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E))) & ((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E))))))), rewrite((environment(E) => (((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E))) & ((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E))))) <=> ((~environment(E)) | (((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E))) & ((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))), ((environment(E) => ((in_environment(E, initial_FM_EP(E)) => subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E))) & (subpopulations(first_movers, efficient_producers, E, T) => greater_or_equal(T, initial_FM_EP(E))))) <=> ((~environment(E)) | (((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E))) & ((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))))),
% 0.08/0.42 inference(bind,[status(th)],[])).
% 0.08/0.42 tff(17,plain,
% 0.08/0.42 (![E: $i, T: $i] : (environment(E) => ((in_environment(E, initial_FM_EP(E)) => subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E))) & (subpopulations(first_movers, efficient_producers, E, T) => greater_or_equal(T, initial_FM_EP(E))))) <=> ![E: $i, T: $i] : ((~environment(E)) | (((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E))) & ((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))),
% 0.08/0.42 inference(quant_intro,[status(thm)],[16])).
% 0.08/0.42 tff(18,axiom,(![E: $i, T: $i] : (environment(E) => ((in_environment(E, initial_FM_EP(E)) => subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E))) & (subpopulations(first_movers, efficient_producers, E, T) => greater_or_equal(T, initial_FM_EP(E)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp_earliest_time_point')).
% 0.08/0.42 tff(19,plain,
% 0.08/0.42 (![E: $i, T: $i] : ((~environment(E)) | (((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E))) & ((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))),
% 0.08/0.42 inference(modus_ponens,[status(thm)],[18, 17])).
% 0.08/0.42 tff(20,plain,
% 0.08/0.42 (![E: $i, T: $i] : ((~environment(E)) | (((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E))) & ((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))),
% 0.08/0.42 inference(modus_ponens,[status(thm)],[19, 15])).
% 0.08/0.42 tff(21,plain,(
% 0.08/0.42 ![E: $i, T: $i] : ((~environment(E)) | (((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E))) & ((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))),
% 0.08/0.42 inference(skolemize,[status(sab)],[20])).
% 0.08/0.42 tff(22,plain,
% 0.08/0.42 (![E: $i, T: $i] : ((~environment(E)) | (~((~((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E)))) | (~((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))))),
% 0.08/0.42 inference(modus_ponens,[status(thm)],[21, 14])).
% 0.08/0.42 tff(23,plain,
% 0.08/0.42 (![E: $i, T: $i] : ((~environment(E)) | (~((~((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E)))) | (~((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))))),
% 0.08/0.42 inference(modus_ponens,[status(thm)],[22, 12])).
% 0.08/0.42 tff(24,plain,
% 0.08/0.42 (((~![E: $i, T: $i] : ((~environment(E)) | (~((~((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E)))) | (~((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))))) | ((~environment(E!1)) | (~((~((~in_environment(E!1, initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))) | (~((~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))) | greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1)))))))) <=> ((~![E: $i, T: $i] : ((~environment(E)) | (~((~((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E)))) | (~((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))))) | (~environment(E!1)) | (~((~((~in_environment(E!1, initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))) | (~((~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))) | greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1)))))))),
% 0.08/0.42 inference(rewrite,[status(thm)],[])).
% 0.08/0.42 tff(25,plain,
% 0.08/0.42 ((~![E: $i, T: $i] : ((~environment(E)) | (~((~((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E)))) | (~((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))))) | ((~environment(E!1)) | (~((~((~in_environment(E!1, initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))) | (~((~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))) | greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1)))))))),
% 0.08/0.42 inference(quant_inst,[status(thm)],[])).
% 0.08/0.42 tff(26,plain,
% 0.08/0.42 ((~![E: $i, T: $i] : ((~environment(E)) | (~((~((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E)))) | (~((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))))) | (~environment(E!1)) | (~((~((~in_environment(E!1, initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))) | (~((~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))) | greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1))))))),
% 0.08/0.42 inference(modus_ponens,[status(thm)],[25, 24])).
% 0.08/0.42 tff(27,plain,
% 0.08/0.42 (~((~((~in_environment(E!1, initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))) | (~((~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))) | greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1)))))),
% 0.08/0.42 inference(unit_resolution,[status(thm)],[26, 23, 10])).
% 0.08/0.42 tff(28,plain,
% 0.08/0.42 (((~((~in_environment(E!1, initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))) | (~((~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))) | greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1))))) | ((~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))) | greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1)))),
% 0.08/0.42 inference(tautology,[status(thm)],[])).
% 0.08/0.42 tff(29,plain,
% 0.08/0.42 ((~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))) | greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1))),
% 0.08/0.42 inference(unit_resolution,[status(thm)],[28, 27])).
% 0.08/0.42 tff(30,assumption,(~in_environment(E!1, initial_FM_EP(E!1))), introduced(assumption)).
% 0.08/0.42 tff(31,plain,
% 0.08/0.42 (^[E: $i, T: $i] : refl((in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T))) <=> (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T))))),
% 0.08/0.42 inference(bind,[status(th)],[])).
% 0.08/0.42 tff(32,plain,
% 0.08/0.42 (![E: $i, T: $i] : (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T))) <=> ![E: $i, T: $i] : (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))),
% 0.08/0.42 inference(quant_intro,[status(thm)],[31])).
% 0.08/0.42 tff(33,plain,
% 0.08/0.42 (^[E: $i, T: $i] : trans(monotonicity(trans(monotonicity(rewrite((environment(E) & subpopulations(first_movers, efficient_producers, E, T)) <=> (~((~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T))))), ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) <=> (~(~((~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T))))))), rewrite((~(~((~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T))))) <=> ((~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))), ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) <=> ((~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T))))), (((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | in_environment(E, T)) <=> (((~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T))) | in_environment(E, T)))), rewrite((((~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T))) | in_environment(E, T)) <=> (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))), (((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | in_environment(E, T)) <=> (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))))),
% 0.08/0.42 inference(bind,[status(th)],[])).
% 0.08/0.42 tff(34,plain,
% 0.08/0.42 (![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | in_environment(E, T)) <=> ![E: $i, T: $i] : (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))),
% 0.08/0.42 inference(quant_intro,[status(thm)],[33])).
% 0.08/0.42 tff(35,plain,
% 0.08/0.42 (![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | in_environment(E, T)) <=> ![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | in_environment(E, T))),
% 0.08/0.42 inference(rewrite,[status(thm)],[])).
% 0.08/0.42 tff(36,plain,
% 0.08/0.42 (^[E: $i, T: $i] : rewrite(((environment(E) & subpopulations(first_movers, efficient_producers, E, T)) => in_environment(E, T)) <=> ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | in_environment(E, T)))),
% 0.08/0.42 inference(bind,[status(th)],[])).
% 0.08/0.42 tff(37,plain,
% 0.08/0.42 (![E: $i, T: $i] : ((environment(E) & subpopulations(first_movers, efficient_producers, E, T)) => in_environment(E, T)) <=> ![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | in_environment(E, T))),
% 0.08/0.42 inference(quant_intro,[status(thm)],[36])).
% 0.08/0.42 tff(38,axiom,(![E: $i, T: $i] : ((environment(E) & subpopulations(first_movers, efficient_producers, E, T)) => in_environment(E, T))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp_time_point_occurs')).
% 0.08/0.42 tff(39,plain,
% 0.08/0.42 (![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | in_environment(E, T))),
% 0.08/0.42 inference(modus_ponens,[status(thm)],[38, 37])).
% 0.08/0.42 tff(40,plain,
% 0.08/0.42 (![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | in_environment(E, T))),
% 0.08/0.42 inference(modus_ponens,[status(thm)],[39, 35])).
% 0.08/0.42 tff(41,plain,(
% 0.08/0.42 ![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | in_environment(E, T))),
% 0.08/0.42 inference(skolemize,[status(sab)],[40])).
% 0.08/0.42 tff(42,plain,
% 0.08/0.42 (![E: $i, T: $i] : (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))),
% 0.08/0.42 inference(modus_ponens,[status(thm)],[41, 34])).
% 0.08/0.42 tff(43,plain,
% 0.08/0.42 (![E: $i, T: $i] : (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))),
% 0.08/0.42 inference(modus_ponens,[status(thm)],[42, 32])).
% 0.08/0.42 tff(44,plain,
% 0.08/0.42 (((~![E: $i, T: $i] : (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | ((~environment(E!1)) | in_environment(E!1, initial_FM_EP(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))))) <=> ((~![E: $i, T: $i] : (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | (~environment(E!1)) | in_environment(E!1, initial_FM_EP(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))))),
% 0.08/0.42 inference(rewrite,[status(thm)],[])).
% 0.08/0.42 tff(45,plain,
% 0.08/0.42 ((in_environment(E!1, initial_FM_EP(E!1)) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))) <=> ((~environment(E!1)) | in_environment(E!1, initial_FM_EP(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))))),
% 0.08/0.42 inference(rewrite,[status(thm)],[])).
% 0.08/0.42 tff(46,plain,
% 0.08/0.42 (((~![E: $i, T: $i] : (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | (in_environment(E!1, initial_FM_EP(E!1)) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))))) <=> ((~![E: $i, T: $i] : (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | ((~environment(E!1)) | in_environment(E!1, initial_FM_EP(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))))),
% 0.08/0.42 inference(monotonicity,[status(thm)],[45])).
% 0.08/0.42 tff(47,plain,
% 0.08/0.42 (((~![E: $i, T: $i] : (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | (in_environment(E!1, initial_FM_EP(E!1)) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))))) <=> ((~![E: $i, T: $i] : (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | (~environment(E!1)) | in_environment(E!1, initial_FM_EP(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))))),
% 0.08/0.42 inference(transitivity,[status(thm)],[46, 44])).
% 0.08/0.42 tff(48,plain,
% 0.08/0.42 ((~![E: $i, T: $i] : (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | (in_environment(E!1, initial_FM_EP(E!1)) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))))),
% 0.08/0.42 inference(quant_inst,[status(thm)],[])).
% 0.08/0.42 tff(49,plain,
% 0.08/0.42 ((~![E: $i, T: $i] : (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | (~environment(E!1)) | in_environment(E!1, initial_FM_EP(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))),
% 0.08/0.42 inference(modus_ponens,[status(thm)],[48, 47])).
% 0.08/0.42 tff(50,plain,
% 0.08/0.42 (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))),
% 0.08/0.42 inference(unit_resolution,[status(thm)],[49, 43, 10, 30])).
% 0.08/0.42 tff(51,assumption,(T!0 = initial_FM_EP(E!1)), introduced(assumption)).
% 0.08/0.42 tff(52,plain,
% 0.08/0.42 (subpopulations(first_movers, efficient_producers, E!1, T!0) <=> subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))),
% 0.08/0.42 inference(monotonicity,[status(thm)],[51])).
% 0.08/0.42 tff(53,plain,
% 0.08/0.42 (subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)) <=> subpopulations(first_movers, efficient_producers, E!1, T!0)),
% 0.08/0.42 inference(symmetry,[status(thm)],[52])).
% 0.08/0.42 tff(54,plain,
% 0.08/0.42 ((~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))) <=> (~subpopulations(first_movers, efficient_producers, E!1, T!0))),
% 0.08/0.42 inference(monotonicity,[status(thm)],[53])).
% 0.08/0.42 tff(55,assumption,(~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))), introduced(assumption)).
% 0.08/0.42 tff(56,plain,
% 0.08/0.42 (~subpopulations(first_movers, efficient_producers, E!1, T!0)),
% 0.08/0.42 inference(modus_ponens,[status(thm)],[55, 54])).
% 0.08/0.42 tff(57,plain,
% 0.08/0.42 (subpopulations(first_movers, efficient_producers, E!1, T!0)),
% 0.08/0.42 inference(and_elim,[status(thm)],[9])).
% 0.08/0.42 tff(58,plain,
% 0.08/0.42 ($false),
% 0.08/0.42 inference(unit_resolution,[status(thm)],[57, 56])).
% 0.08/0.42 tff(59,plain,((~(T!0 = initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))), inference(lemma,lemma(discharge,[]))).
% 0.08/0.42 tff(60,plain,
% 0.08/0.42 (~(T!0 = initial_FM_EP(E!1))),
% 0.08/0.42 inference(unit_resolution,[status(thm)],[59, 50])).
% 0.08/0.42 tff(61,plain,
% 0.08/0.42 (((~![E: $i, T: $i] : ((~environment(E)) | (~((~((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E)))) | (~((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))))) | ((~environment(E!1)) | (~((~((~in_environment(E!1, initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))) | (~((~subpopulations(first_movers, efficient_producers, E!1, T!0)) | greater_or_equal(T!0, initial_FM_EP(E!1)))))))) <=> ((~![E: $i, T: $i] : ((~environment(E)) | (~((~((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E)))) | (~((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))))) | (~environment(E!1)) | (~((~((~in_environment(E!1, initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))) | (~((~subpopulations(first_movers, efficient_producers, E!1, T!0)) | greater_or_equal(T!0, initial_FM_EP(E!1)))))))),
% 0.08/0.43 inference(rewrite,[status(thm)],[])).
% 0.08/0.43 tff(62,plain,
% 0.08/0.43 ((~![E: $i, T: $i] : ((~environment(E)) | (~((~((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E)))) | (~((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))))) | ((~environment(E!1)) | (~((~((~in_environment(E!1, initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))) | (~((~subpopulations(first_movers, efficient_producers, E!1, T!0)) | greater_or_equal(T!0, initial_FM_EP(E!1)))))))),
% 0.08/0.43 inference(quant_inst,[status(thm)],[])).
% 0.08/0.43 tff(63,plain,
% 0.08/0.43 ((~![E: $i, T: $i] : ((~environment(E)) | (~((~((~in_environment(E, initial_FM_EP(E))) | subpopulations(first_movers, efficient_producers, E, initial_FM_EP(E)))) | (~((~subpopulations(first_movers, efficient_producers, E, T)) | greater_or_equal(T, initial_FM_EP(E)))))))) | (~environment(E!1)) | (~((~((~in_environment(E!1, initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))) | (~((~subpopulations(first_movers, efficient_producers, E!1, T!0)) | greater_or_equal(T!0, initial_FM_EP(E!1))))))),
% 0.08/0.43 inference(modus_ponens,[status(thm)],[62, 61])).
% 0.08/0.43 tff(64,plain,
% 0.08/0.43 (~((~((~in_environment(E!1, initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))) | (~((~subpopulations(first_movers, efficient_producers, E!1, T!0)) | greater_or_equal(T!0, initial_FM_EP(E!1)))))),
% 0.08/0.43 inference(unit_resolution,[status(thm)],[63, 23, 10])).
% 0.08/0.43 tff(65,plain,
% 0.08/0.43 (((~((~in_environment(E!1, initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))) | (~((~subpopulations(first_movers, efficient_producers, E!1, T!0)) | greater_or_equal(T!0, initial_FM_EP(E!1))))) | ((~subpopulations(first_movers, efficient_producers, E!1, T!0)) | greater_or_equal(T!0, initial_FM_EP(E!1)))),
% 0.08/0.43 inference(tautology,[status(thm)],[])).
% 0.08/0.43 tff(66,plain,
% 0.08/0.43 ((~subpopulations(first_movers, efficient_producers, E!1, T!0)) | greater_or_equal(T!0, initial_FM_EP(E!1))),
% 0.08/0.43 inference(unit_resolution,[status(thm)],[65, 64])).
% 0.08/0.43 tff(67,plain,
% 0.08/0.43 ((~((~subpopulations(first_movers, efficient_producers, E!1, T!0)) | greater_or_equal(T!0, initial_FM_EP(E!1)))) | (~subpopulations(first_movers, efficient_producers, E!1, T!0)) | greater_or_equal(T!0, initial_FM_EP(E!1))),
% 0.08/0.43 inference(tautology,[status(thm)],[])).
% 0.08/0.43 tff(68,plain,
% 0.08/0.43 ((~((~subpopulations(first_movers, efficient_producers, E!1, T!0)) | greater_or_equal(T!0, initial_FM_EP(E!1)))) | greater_or_equal(T!0, initial_FM_EP(E!1))),
% 0.08/0.43 inference(unit_resolution,[status(thm)],[67, 57])).
% 0.08/0.43 tff(69,plain,
% 0.08/0.43 (greater_or_equal(T!0, initial_FM_EP(E!1))),
% 0.08/0.43 inference(unit_resolution,[status(thm)],[68, 66])).
% 0.08/0.43 tff(70,plain,
% 0.08/0.43 (^[X: $i, Y: $i] : refl(((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y))) <=> ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y))))),
% 0.08/0.43 inference(bind,[status(th)],[])).
% 0.08/0.43 tff(71,plain,
% 0.08/0.43 (![X: $i, Y: $i] : ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y))) <=> ![X: $i, Y: $i] : ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y)))),
% 0.08/0.43 inference(quant_intro,[status(thm)],[70])).
% 0.08/0.43 tff(72,plain,
% 0.08/0.43 (![X: $i, Y: $i] : ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y))) <=> ![X: $i, Y: $i] : ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y)))),
% 0.08/0.43 inference(rewrite,[status(thm)],[])).
% 0.08/0.43 tff(73,plain,
% 0.08/0.43 (^[X: $i, Y: $i] : trans(monotonicity(rewrite((greater(X, Y) | (X = Y)) <=> ((X = Y) | greater(X, Y))), ((greater_or_equal(X, Y) => (greater(X, Y) | (X = Y))) <=> (greater_or_equal(X, Y) => ((X = Y) | greater(X, Y))))), rewrite((greater_or_equal(X, Y) => ((X = Y) | greater(X, Y))) <=> ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y)))), ((greater_or_equal(X, Y) => (greater(X, Y) | (X = Y))) <=> ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y)))))),
% 0.08/0.43 inference(bind,[status(th)],[])).
% 0.08/0.43 tff(74,plain,
% 0.08/0.43 (![X: $i, Y: $i] : (greater_or_equal(X, Y) => (greater(X, Y) | (X = Y))) <=> ![X: $i, Y: $i] : ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y)))),
% 0.08/0.43 inference(quant_intro,[status(thm)],[73])).
% 0.08/0.43 tff(75,axiom,(![X: $i, Y: $i] : (greater_or_equal(X, Y) => (greater(X, Y) | (X = Y)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp_greater_or_equal')).
% 0.08/0.43 tff(76,plain,
% 0.08/0.43 (![X: $i, Y: $i] : ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y)))),
% 0.08/0.43 inference(modus_ponens,[status(thm)],[75, 74])).
% 0.08/0.43 tff(77,plain,
% 0.08/0.43 (![X: $i, Y: $i] : ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y)))),
% 0.08/0.43 inference(modus_ponens,[status(thm)],[76, 72])).
% 0.08/0.43 tff(78,plain,(
% 0.08/0.43 ![X: $i, Y: $i] : ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y)))),
% 0.08/0.43 inference(skolemize,[status(sab)],[77])).
% 0.08/0.43 tff(79,plain,
% 0.08/0.43 (![X: $i, Y: $i] : ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y)))),
% 0.08/0.43 inference(modus_ponens,[status(thm)],[78, 71])).
% 0.08/0.43 tff(80,plain,
% 0.08/0.43 (((~![X: $i, Y: $i] : ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y)))) | ((~greater_or_equal(T!0, initial_FM_EP(E!1))) | (T!0 = initial_FM_EP(E!1)) | greater(T!0, initial_FM_EP(E!1)))) <=> ((~![X: $i, Y: $i] : ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y)))) | (~greater_or_equal(T!0, initial_FM_EP(E!1))) | (T!0 = initial_FM_EP(E!1)) | greater(T!0, initial_FM_EP(E!1)))),
% 0.08/0.43 inference(rewrite,[status(thm)],[])).
% 0.08/0.43 tff(81,plain,
% 0.08/0.43 (((T!0 = initial_FM_EP(E!1)) | greater(T!0, initial_FM_EP(E!1)) | (~greater_or_equal(T!0, initial_FM_EP(E!1)))) <=> ((~greater_or_equal(T!0, initial_FM_EP(E!1))) | (T!0 = initial_FM_EP(E!1)) | greater(T!0, initial_FM_EP(E!1)))),
% 0.08/0.43 inference(rewrite,[status(thm)],[])).
% 0.08/0.43 tff(82,plain,
% 0.08/0.43 (((~![X: $i, Y: $i] : ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y)))) | ((T!0 = initial_FM_EP(E!1)) | greater(T!0, initial_FM_EP(E!1)) | (~greater_or_equal(T!0, initial_FM_EP(E!1))))) <=> ((~![X: $i, Y: $i] : ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y)))) | ((~greater_or_equal(T!0, initial_FM_EP(E!1))) | (T!0 = initial_FM_EP(E!1)) | greater(T!0, initial_FM_EP(E!1))))),
% 0.08/0.43 inference(monotonicity,[status(thm)],[81])).
% 0.08/0.43 tff(83,plain,
% 0.08/0.43 (((~![X: $i, Y: $i] : ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y)))) | ((T!0 = initial_FM_EP(E!1)) | greater(T!0, initial_FM_EP(E!1)) | (~greater_or_equal(T!0, initial_FM_EP(E!1))))) <=> ((~![X: $i, Y: $i] : ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y)))) | (~greater_or_equal(T!0, initial_FM_EP(E!1))) | (T!0 = initial_FM_EP(E!1)) | greater(T!0, initial_FM_EP(E!1)))),
% 0.08/0.43 inference(transitivity,[status(thm)],[82, 80])).
% 0.08/0.43 tff(84,plain,
% 0.08/0.43 ((~![X: $i, Y: $i] : ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y)))) | ((T!0 = initial_FM_EP(E!1)) | greater(T!0, initial_FM_EP(E!1)) | (~greater_or_equal(T!0, initial_FM_EP(E!1))))),
% 0.08/0.43 inference(quant_inst,[status(thm)],[])).
% 0.08/0.43 tff(85,plain,
% 0.08/0.43 ((~![X: $i, Y: $i] : ((X = Y) | greater(X, Y) | (~greater_or_equal(X, Y)))) | (~greater_or_equal(T!0, initial_FM_EP(E!1))) | (T!0 = initial_FM_EP(E!1)) | greater(T!0, initial_FM_EP(E!1))),
% 0.08/0.43 inference(modus_ponens,[status(thm)],[84, 83])).
% 0.08/0.43 tff(86,plain,
% 0.08/0.43 ((T!0 = initial_FM_EP(E!1)) | greater(T!0, initial_FM_EP(E!1))),
% 0.08/0.43 inference(unit_resolution,[status(thm)],[85, 79, 69])).
% 0.08/0.43 tff(87,plain,
% 0.08/0.43 (greater(T!0, initial_FM_EP(E!1))),
% 0.08/0.43 inference(unit_resolution,[status(thm)],[86, 60])).
% 0.08/0.43 tff(88,plain,
% 0.08/0.43 (^[E: $i] : refl(((~environment(E)) | greater_or_equal(initial_FM_EP(E), start_time(E))) <=> ((~environment(E)) | greater_or_equal(initial_FM_EP(E), start_time(E))))),
% 0.08/0.43 inference(bind,[status(th)],[])).
% 0.08/0.43 tff(89,plain,
% 0.08/0.43 (![E: $i] : ((~environment(E)) | greater_or_equal(initial_FM_EP(E), start_time(E))) <=> ![E: $i] : ((~environment(E)) | greater_or_equal(initial_FM_EP(E), start_time(E)))),
% 0.08/0.43 inference(quant_intro,[status(thm)],[88])).
% 0.08/0.43 tff(90,plain,
% 0.08/0.43 (![E: $i] : ((~environment(E)) | greater_or_equal(initial_FM_EP(E), start_time(E))) <=> ![E: $i] : ((~environment(E)) | greater_or_equal(initial_FM_EP(E), start_time(E)))),
% 0.08/0.43 inference(rewrite,[status(thm)],[])).
% 0.08/0.43 tff(91,plain,
% 0.08/0.43 (^[E: $i] : rewrite((environment(E) => greater_or_equal(initial_FM_EP(E), start_time(E))) <=> ((~environment(E)) | greater_or_equal(initial_FM_EP(E), start_time(E))))),
% 0.08/0.43 inference(bind,[status(th)],[])).
% 0.08/0.43 tff(92,plain,
% 0.08/0.43 (![E: $i] : (environment(E) => greater_or_equal(initial_FM_EP(E), start_time(E))) <=> ![E: $i] : ((~environment(E)) | greater_or_equal(initial_FM_EP(E), start_time(E)))),
% 0.08/0.43 inference(quant_intro,[status(thm)],[91])).
% 0.08/0.43 tff(93,axiom,(![E: $i] : (environment(E) => greater_or_equal(initial_FM_EP(E), start_time(E)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp_initial_time')).
% 0.08/0.43 tff(94,plain,
% 0.08/0.43 (![E: $i] : ((~environment(E)) | greater_or_equal(initial_FM_EP(E), start_time(E)))),
% 0.08/0.43 inference(modus_ponens,[status(thm)],[93, 92])).
% 0.08/0.43 tff(95,plain,
% 0.08/0.43 (![E: $i] : ((~environment(E)) | greater_or_equal(initial_FM_EP(E), start_time(E)))),
% 0.08/0.43 inference(modus_ponens,[status(thm)],[94, 90])).
% 0.08/0.43 tff(96,plain,(
% 0.08/0.43 ![E: $i] : ((~environment(E)) | greater_or_equal(initial_FM_EP(E), start_time(E)))),
% 0.08/0.43 inference(skolemize,[status(sab)],[95])).
% 0.08/0.43 tff(97,plain,
% 0.08/0.43 (![E: $i] : ((~environment(E)) | greater_or_equal(initial_FM_EP(E), start_time(E)))),
% 0.08/0.43 inference(modus_ponens,[status(thm)],[96, 89])).
% 0.08/0.43 tff(98,plain,
% 0.08/0.43 (((~![E: $i] : ((~environment(E)) | greater_or_equal(initial_FM_EP(E), start_time(E)))) | ((~environment(E!1)) | greater_or_equal(initial_FM_EP(E!1), start_time(E!1)))) <=> ((~![E: $i] : ((~environment(E)) | greater_or_equal(initial_FM_EP(E), start_time(E)))) | (~environment(E!1)) | greater_or_equal(initial_FM_EP(E!1), start_time(E!1)))),
% 0.08/0.43 inference(rewrite,[status(thm)],[])).
% 0.08/0.43 tff(99,plain,
% 0.08/0.43 ((~![E: $i] : ((~environment(E)) | greater_or_equal(initial_FM_EP(E), start_time(E)))) | ((~environment(E!1)) | greater_or_equal(initial_FM_EP(E!1), start_time(E!1)))),
% 0.08/0.43 inference(quant_inst,[status(thm)],[])).
% 0.08/0.43 tff(100,plain,
% 0.08/0.43 ((~![E: $i] : ((~environment(E)) | greater_or_equal(initial_FM_EP(E), start_time(E)))) | (~environment(E!1)) | greater_or_equal(initial_FM_EP(E!1), start_time(E!1))),
% 0.08/0.43 inference(modus_ponens,[status(thm)],[99, 98])).
% 0.08/0.43 tff(101,plain,
% 0.08/0.43 (greater_or_equal(initial_FM_EP(E!1), start_time(E!1))),
% 0.08/0.43 inference(unit_resolution,[status(thm)],[100, 97, 10])).
% 0.08/0.43 tff(102,plain,
% 0.08/0.43 (((~![E: $i, T: $i] : (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | (in_environment(E!1, T!0) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, T!0)))) <=> ((~![E: $i, T: $i] : (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | in_environment(E!1, T!0) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, T!0)))),
% 0.08/0.43 inference(rewrite,[status(thm)],[])).
% 0.08/0.43 tff(103,plain,
% 0.08/0.43 ((~![E: $i, T: $i] : (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | (in_environment(E!1, T!0) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, T!0)))),
% 0.08/0.43 inference(quant_inst,[status(thm)],[])).
% 0.08/0.43 tff(104,plain,
% 0.08/0.43 ((~![E: $i, T: $i] : (in_environment(E, T) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | in_environment(E!1, T!0) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, T!0))),
% 0.08/0.43 inference(modus_ponens,[status(thm)],[103, 102])).
% 0.08/0.43 tff(105,plain,
% 0.08/0.43 (in_environment(E!1, T!0)),
% 0.08/0.43 inference(unit_resolution,[status(thm)],[104, 43, 10, 57])).
% 0.08/0.43 tff(106,plain,
% 0.08/0.43 (^[E: $i, T1: $i, T2: $i] : refl((in_environment(E, T1) | (~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2))) <=> (in_environment(E, T1) | (~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2))))),
% 0.08/0.43 inference(bind,[status(th)],[])).
% 0.08/0.43 tff(107,plain,
% 0.08/0.43 (![E: $i, T1: $i, T2: $i] : (in_environment(E, T1) | (~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2))) <=> ![E: $i, T1: $i, T2: $i] : (in_environment(E, T1) | (~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2)))),
% 0.08/0.43 inference(quant_intro,[status(thm)],[106])).
% 0.08/0.43 tff(108,plain,
% 0.08/0.43 (^[E: $i, T1: $i, T2: $i] : trans(monotonicity(trans(monotonicity(rewrite((environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1) & in_environment(E, T2)) <=> (~((~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2))))), ((~(environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1) & in_environment(E, T2))) <=> (~(~((~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2))))))), rewrite((~(~((~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2))))) <=> ((~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2)))), ((~(environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1) & in_environment(E, T2))) <=> ((~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2))))), (((~(environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1) & in_environment(E, T2))) | in_environment(E, T1)) <=> (((~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2))) | in_environment(E, T1)))), rewrite((((~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2))) | in_environment(E, T1)) <=> (in_environment(E, T1) | (~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2)))), (((~(environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1) & in_environment(E, T2))) | in_environment(E, T1)) <=> (in_environment(E, T1) | (~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2)))))),
% 0.08/0.43 inference(bind,[status(th)],[])).
% 0.08/0.43 tff(109,plain,
% 0.08/0.43 (![E: $i, T1: $i, T2: $i] : ((~(environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1) & in_environment(E, T2))) | in_environment(E, T1)) <=> ![E: $i, T1: $i, T2: $i] : (in_environment(E, T1) | (~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2)))),
% 0.08/0.43 inference(quant_intro,[status(thm)],[108])).
% 0.08/0.43 tff(110,plain,
% 0.08/0.43 (![E: $i, T1: $i, T2: $i] : ((~(environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1) & in_environment(E, T2))) | in_environment(E, T1)) <=> ![E: $i, T1: $i, T2: $i] : ((~(environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1) & in_environment(E, T2))) | in_environment(E, T1))),
% 0.08/0.43 inference(rewrite,[status(thm)],[])).
% 0.08/0.43 tff(111,plain,
% 0.08/0.43 (^[E: $i, T1: $i, T2: $i] : trans(monotonicity(trans(monotonicity(rewrite(((environment(E) & greater_or_equal(T1, start_time(E))) & greater(T2, T1)) <=> (environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1))), ((((environment(E) & greater_or_equal(T1, start_time(E))) & greater(T2, T1)) & in_environment(E, T2)) <=> ((environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1)) & in_environment(E, T2)))), rewrite(((environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1)) & in_environment(E, T2)) <=> (environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1) & in_environment(E, T2))), ((((environment(E) & greater_or_equal(T1, start_time(E))) & greater(T2, T1)) & in_environment(E, T2)) <=> (environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1) & in_environment(E, T2)))), (((((environment(E) & greater_or_equal(T1, start_time(E))) & greater(T2, T1)) & in_environment(E, T2)) => in_environment(E, T1)) <=> ((environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1) & in_environment(E, T2)) => in_environment(E, T1)))), rewrite(((environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1) & in_environment(E, T2)) => in_environment(E, T1)) <=> ((~(environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1) & in_environment(E, T2))) | in_environment(E, T1))), (((((environment(E) & greater_or_equal(T1, start_time(E))) & greater(T2, T1)) & in_environment(E, T2)) => in_environment(E, T1)) <=> ((~(environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1) & in_environment(E, T2))) | in_environment(E, T1))))),
% 0.08/0.43 inference(bind,[status(th)],[])).
% 0.08/0.43 tff(112,plain,
% 0.08/0.43 (![E: $i, T1: $i, T2: $i] : ((((environment(E) & greater_or_equal(T1, start_time(E))) & greater(T2, T1)) & in_environment(E, T2)) => in_environment(E, T1)) <=> ![E: $i, T1: $i, T2: $i] : ((~(environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1) & in_environment(E, T2))) | in_environment(E, T1))),
% 0.08/0.43 inference(quant_intro,[status(thm)],[111])).
% 0.08/0.43 tff(113,axiom,(![E: $i, T1: $i, T2: $i] : ((((environment(E) & greater_or_equal(T1, start_time(E))) & greater(T2, T1)) & in_environment(E, T2)) => in_environment(E, T1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp_times_in_order')).
% 0.08/0.43 tff(114,plain,
% 0.08/0.43 (![E: $i, T1: $i, T2: $i] : ((~(environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1) & in_environment(E, T2))) | in_environment(E, T1))),
% 0.08/0.43 inference(modus_ponens,[status(thm)],[113, 112])).
% 0.08/0.43 tff(115,plain,
% 0.08/0.43 (![E: $i, T1: $i, T2: $i] : ((~(environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1) & in_environment(E, T2))) | in_environment(E, T1))),
% 0.08/0.43 inference(modus_ponens,[status(thm)],[114, 110])).
% 0.08/0.43 tff(116,plain,(
% 0.08/0.43 ![E: $i, T1: $i, T2: $i] : ((~(environment(E) & greater_or_equal(T1, start_time(E)) & greater(T2, T1) & in_environment(E, T2))) | in_environment(E, T1))),
% 0.08/0.43 inference(skolemize,[status(sab)],[115])).
% 0.08/0.43 tff(117,plain,
% 0.08/0.43 (![E: $i, T1: $i, T2: $i] : (in_environment(E, T1) | (~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2)))),
% 0.08/0.43 inference(modus_ponens,[status(thm)],[116, 109])).
% 0.08/0.43 tff(118,plain,
% 0.08/0.43 (![E: $i, T1: $i, T2: $i] : (in_environment(E, T1) | (~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2)))),
% 0.08/0.43 inference(modus_ponens,[status(thm)],[117, 107])).
% 0.08/0.43 tff(119,plain,
% 0.08/0.43 (((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T1) | (~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2)))) | ((~environment(E!1)) | in_environment(E!1, initial_FM_EP(E!1)) | (~greater_or_equal(initial_FM_EP(E!1), start_time(E!1))) | (~greater(T!0, initial_FM_EP(E!1))) | (~in_environment(E!1, T!0)))) <=> ((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T1) | (~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2)))) | (~environment(E!1)) | in_environment(E!1, initial_FM_EP(E!1)) | (~greater_or_equal(initial_FM_EP(E!1), start_time(E!1))) | (~greater(T!0, initial_FM_EP(E!1))) | (~in_environment(E!1, T!0)))),
% 0.08/0.43 inference(rewrite,[status(thm)],[])).
% 0.08/0.43 tff(120,plain,
% 0.08/0.43 ((in_environment(E!1, initial_FM_EP(E!1)) | (~environment(E!1)) | (~greater_or_equal(initial_FM_EP(E!1), start_time(E!1))) | (~greater(T!0, initial_FM_EP(E!1))) | (~in_environment(E!1, T!0))) <=> ((~environment(E!1)) | in_environment(E!1, initial_FM_EP(E!1)) | (~greater_or_equal(initial_FM_EP(E!1), start_time(E!1))) | (~greater(T!0, initial_FM_EP(E!1))) | (~in_environment(E!1, T!0)))),
% 0.08/0.43 inference(rewrite,[status(thm)],[])).
% 0.08/0.43 tff(121,plain,
% 0.08/0.43 (((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T1) | (~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2)))) | (in_environment(E!1, initial_FM_EP(E!1)) | (~environment(E!1)) | (~greater_or_equal(initial_FM_EP(E!1), start_time(E!1))) | (~greater(T!0, initial_FM_EP(E!1))) | (~in_environment(E!1, T!0)))) <=> ((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T1) | (~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2)))) | ((~environment(E!1)) | in_environment(E!1, initial_FM_EP(E!1)) | (~greater_or_equal(initial_FM_EP(E!1), start_time(E!1))) | (~greater(T!0, initial_FM_EP(E!1))) | (~in_environment(E!1, T!0))))),
% 0.08/0.43 inference(monotonicity,[status(thm)],[120])).
% 0.08/0.43 tff(122,plain,
% 0.08/0.43 (((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T1) | (~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2)))) | (in_environment(E!1, initial_FM_EP(E!1)) | (~environment(E!1)) | (~greater_or_equal(initial_FM_EP(E!1), start_time(E!1))) | (~greater(T!0, initial_FM_EP(E!1))) | (~in_environment(E!1, T!0)))) <=> ((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T1) | (~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2)))) | (~environment(E!1)) | in_environment(E!1, initial_FM_EP(E!1)) | (~greater_or_equal(initial_FM_EP(E!1), start_time(E!1))) | (~greater(T!0, initial_FM_EP(E!1))) | (~in_environment(E!1, T!0)))),
% 0.08/0.43 inference(transitivity,[status(thm)],[121, 119])).
% 0.08/0.43 tff(123,plain,
% 0.08/0.43 ((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T1) | (~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2)))) | (in_environment(E!1, initial_FM_EP(E!1)) | (~environment(E!1)) | (~greater_or_equal(initial_FM_EP(E!1), start_time(E!1))) | (~greater(T!0, initial_FM_EP(E!1))) | (~in_environment(E!1, T!0)))),
% 0.08/0.43 inference(quant_inst,[status(thm)],[])).
% 0.08/0.43 tff(124,plain,
% 0.08/0.43 ((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T1) | (~environment(E)) | (~greater_or_equal(T1, start_time(E))) | (~greater(T2, T1)) | (~in_environment(E, T2)))) | (~environment(E!1)) | in_environment(E!1, initial_FM_EP(E!1)) | (~greater_or_equal(initial_FM_EP(E!1), start_time(E!1))) | (~greater(T!0, initial_FM_EP(E!1))) | (~in_environment(E!1, T!0))),
% 0.08/0.43 inference(modus_ponens,[status(thm)],[123, 122])).
% 0.08/0.43 tff(125,plain,
% 0.08/0.43 ($false),
% 0.08/0.43 inference(unit_resolution,[status(thm)],[124, 118, 10, 105, 30, 101, 87])).
% 0.08/0.43 tff(126,plain,(in_environment(E!1, initial_FM_EP(E!1))), inference(lemma,lemma(discharge,[]))).
% 0.08/0.43 tff(127,plain,
% 0.08/0.43 (((~((~in_environment(E!1, initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))) | (~((~subpopulations(first_movers, efficient_producers, E!1, T!0)) | greater_or_equal(T!0, initial_FM_EP(E!1))))) | ((~in_environment(E!1, initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))),
% 0.08/0.43 inference(tautology,[status(thm)],[])).
% 0.08/0.43 tff(128,plain,
% 0.08/0.43 ((~in_environment(E!1, initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))),
% 0.08/0.43 inference(unit_resolution,[status(thm)],[127, 64])).
% 0.08/0.43 tff(129,plain,
% 0.08/0.43 ((~((~in_environment(E!1, initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))) | (~in_environment(E!1, initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))),
% 0.08/0.43 inference(tautology,[status(thm)],[])).
% 0.08/0.43 tff(130,plain,
% 0.08/0.43 ((~in_environment(E!1, initial_FM_EP(E!1))) | subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))),
% 0.08/0.43 inference(unit_resolution,[status(thm)],[129, 128])).
% 0.08/0.43 tff(131,plain,
% 0.08/0.43 (subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))),
% 0.08/0.43 inference(unit_resolution,[status(thm)],[130, 126])).
% 0.08/0.43 tff(132,plain,
% 0.08/0.43 ((~((~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))) | greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1)))) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))) | greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1))),
% 0.08/0.43 inference(tautology,[status(thm)],[])).
% 0.08/0.43 tff(133,plain,
% 0.08/0.43 ((~((~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))) | greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1)))) | greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1))),
% 0.08/0.43 inference(unit_resolution,[status(thm)],[132, 131])).
% 0.08/0.43 tff(134,plain,
% 0.08/0.43 (greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1))),
% 0.08/0.44 inference(unit_resolution,[status(thm)],[133, 29])).
% 0.08/0.44 tff(135,plain,
% 0.08/0.44 (^[E: $i, T: $i] : refl(((~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T))) <=> ((~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T))))),
% 0.08/0.44 inference(bind,[status(th)],[])).
% 0.08/0.44 tff(136,plain,
% 0.08/0.44 (![E: $i, T: $i] : ((~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T))) <=> ![E: $i, T: $i] : ((~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))),
% 0.08/0.44 inference(quant_intro,[status(thm)],[135])).
% 0.08/0.44 tff(137,plain,
% 0.08/0.44 (^[E: $i, T: $i] : trans(monotonicity(trans(monotonicity(rewrite((environment(E) & subpopulations(first_movers, efficient_producers, E, T)) <=> (~((~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T))))), ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) <=> (~(~((~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T))))))), rewrite((~(~((~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T))))) <=> ((~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))), ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) <=> ((~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T))))), (((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | (~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))))) <=> (((~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T))) | (~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))))))), rewrite((((~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T))) | (~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))))) <=> ((~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))), (((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | (~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))))) <=> ((~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))))),
% 0.08/0.44 inference(bind,[status(th)],[])).
% 0.08/0.44 tff(138,plain,
% 0.08/0.44 (![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | (~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))))) <=> ![E: $i, T: $i] : ((~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))),
% 0.08/0.44 inference(quant_intro,[status(thm)],[137])).
% 0.08/0.44 tff(139,plain,
% 0.08/0.44 (![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | (~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))))) <=> ![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | (~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))))),
% 0.08/0.44 inference(rewrite,[status(thm)],[])).
% 0.08/0.44 tff(140,plain,
% 0.08/0.44 (^[E: $i, T: $i] : rewrite(((environment(E) & subpopulations(first_movers, efficient_producers, E, T)) => (~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))))) <=> ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | (~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))))))),
% 0.08/0.44 inference(bind,[status(th)],[])).
% 0.08/0.44 tff(141,plain,
% 0.08/0.44 (![E: $i, T: $i] : ((environment(E) & subpopulations(first_movers, efficient_producers, E, T)) => (~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))))) <=> ![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | (~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))))),
% 0.08/0.44 inference(quant_intro,[status(thm)],[140])).
% 0.08/0.44 tff(142,axiom,(![E: $i, T: $i] : ((environment(E) & subpopulations(first_movers, efficient_producers, E, T)) => (~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','l3')).
% 0.08/0.44 tff(143,plain,
% 0.08/0.44 (![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | (~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))))),
% 0.08/0.44 inference(modus_ponens,[status(thm)],[142, 141])).
% 0.08/0.44 tff(144,plain,
% 0.08/0.44 (![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | (~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))))),
% 0.08/0.44 inference(modus_ponens,[status(thm)],[143, 139])).
% 0.08/0.44 tff(145,plain,(
% 0.08/0.44 ![E: $i, T: $i] : ((~(environment(E) & subpopulations(first_movers, efficient_producers, E, T))) | (~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))))),
% 0.08/0.44 inference(skolemize,[status(sab)],[144])).
% 0.08/0.44 tff(146,plain,
% 0.08/0.44 (![E: $i, T: $i] : ((~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))),
% 0.08/0.44 inference(modus_ponens,[status(thm)],[145, 138])).
% 0.08/0.44 tff(147,plain,
% 0.08/0.44 (![E: $i, T: $i] : ((~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))),
% 0.08/0.44 inference(modus_ponens,[status(thm)],[146, 136])).
% 0.08/0.44 tff(148,plain,
% 0.08/0.44 (((~![E: $i, T: $i] : ((~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | ((~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))) | (~decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1))))))) <=> ((~![E: $i, T: $i] : ((~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))) | (~decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1))))))),
% 0.08/0.44 inference(rewrite,[status(thm)],[])).
% 0.08/0.44 tff(149,plain,
% 0.08/0.44 (((~decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1))))) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1)))) <=> ((~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))) | (~decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1))))))),
% 0.08/0.44 inference(rewrite,[status(thm)],[])).
% 0.08/0.44 tff(150,plain,
% 0.08/0.44 (((~![E: $i, T: $i] : ((~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | ((~decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1))))) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))))) <=> ((~![E: $i, T: $i] : ((~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | ((~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))) | (~decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))))))),
% 0.08/0.44 inference(monotonicity,[status(thm)],[149])).
% 0.08/0.44 tff(151,plain,
% 0.08/0.44 (((~![E: $i, T: $i] : ((~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | ((~decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1))))) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))))) <=> ((~![E: $i, T: $i] : ((~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))) | (~decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1))))))),
% 0.08/0.44 inference(transitivity,[status(thm)],[150, 148])).
% 0.08/0.44 tff(152,plain,
% 0.08/0.44 ((~![E: $i, T: $i] : ((~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | ((~decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1))))) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))))),
% 0.08/0.44 inference(quant_inst,[status(thm)],[])).
% 0.08/0.44 tff(153,plain,
% 0.08/0.44 ((~![E: $i, T: $i] : ((~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) | (~environment(E)) | (~subpopulations(first_movers, efficient_producers, E, T)))) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, initial_FM_EP(E!1))) | (~decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))))),
% 0.08/0.44 inference(modus_ponens,[status(thm)],[152, 151])).
% 0.08/0.44 tff(154,plain,
% 0.08/0.44 (~decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1))))),
% 0.08/0.44 inference(unit_resolution,[status(thm)],[153, 147, 10, 131])).
% 0.08/0.44 tff(155,plain,
% 0.08/0.44 (^[E: $i] : refl(((~environment(E)) | greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E)))) <=> ((~environment(E)) | greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E)))))),
% 0.08/0.44 inference(bind,[status(th)],[])).
% 0.08/0.44 tff(156,plain,
% 0.08/0.44 (![E: $i] : ((~environment(E)) | greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E)))) <=> ![E: $i] : ((~environment(E)) | greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E))))),
% 0.08/0.44 inference(quant_intro,[status(thm)],[155])).
% 0.08/0.44 tff(157,plain,
% 0.08/0.44 (![E: $i] : ((~environment(E)) | greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E)))) <=> ![E: $i] : ((~environment(E)) | greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E))))),
% 0.08/0.44 inference(rewrite,[status(thm)],[])).
% 0.08/0.44 tff(158,plain,
% 0.08/0.44 (^[E: $i] : rewrite((environment(E) => greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E)))) <=> ((~environment(E)) | greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E)))))),
% 0.08/0.44 inference(bind,[status(th)],[])).
% 0.08/0.44 tff(159,plain,
% 0.08/0.44 (![E: $i] : (environment(E) => greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E)))) <=> ![E: $i] : ((~environment(E)) | greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E))))),
% 0.08/0.44 inference(quant_intro,[status(thm)],[158])).
% 0.08/0.44 tff(160,axiom,(![E: $i] : (environment(E) => greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','a8')).
% 0.08/0.44 tff(161,plain,
% 0.08/0.44 (![E: $i] : ((~environment(E)) | greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E))))),
% 0.08/0.44 inference(modus_ponens,[status(thm)],[160, 159])).
% 0.08/0.44 tff(162,plain,
% 0.08/0.44 (![E: $i] : ((~environment(E)) | greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E))))),
% 0.08/0.44 inference(modus_ponens,[status(thm)],[161, 157])).
% 0.08/0.44 tff(163,plain,(
% 0.08/0.44 ![E: $i] : ((~environment(E)) | greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E))))),
% 0.08/0.44 inference(skolemize,[status(sab)],[162])).
% 0.08/0.44 tff(164,plain,
% 0.08/0.44 (![E: $i] : ((~environment(E)) | greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E))))),
% 0.08/0.44 inference(modus_ponens,[status(thm)],[163, 156])).
% 0.08/0.44 tff(165,plain,
% 0.08/0.44 (((~![E: $i] : ((~environment(E)) | greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E))))) | ((~environment(E!1)) | greater(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1))))) <=> ((~![E: $i] : ((~environment(E)) | greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E))))) | (~environment(E!1)) | greater(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1))))),
% 0.08/0.44 inference(rewrite,[status(thm)],[])).
% 0.08/0.44 tff(166,plain,
% 0.08/0.44 ((~![E: $i] : ((~environment(E)) | greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E))))) | ((~environment(E!1)) | greater(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1))))),
% 0.08/0.44 inference(quant_inst,[status(thm)],[])).
% 0.08/0.44 tff(167,plain,
% 0.08/0.44 ((~![E: $i] : ((~environment(E)) | greater(disbanding_rate(first_movers, initial_FM_EP(E)), disbanding_rate(efficient_producers, initial_FM_EP(E))))) | (~environment(E!1)) | greater(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))),
% 0.08/0.44 inference(modus_ponens,[status(thm)],[166, 165])).
% 0.08/0.44 tff(168,plain,
% 0.08/0.44 (greater(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))),
% 0.08/0.44 inference(unit_resolution,[status(thm)],[167, 164, 10])).
% 0.08/0.44 tff(169,plain,
% 0.08/0.44 (~greater(disbanding_rate(first_movers, T!0), disbanding_rate(efficient_producers, T!0))),
% 0.08/0.44 inference(or_elim,[status(thm)],[8])).
% 0.08/0.44 tff(170,plain,
% 0.08/0.44 (^[E: $i, T: $i, T1: $i, T2: $i] : refl((greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1)))) <=> (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1)))))),
% 0.08/0.44 inference(bind,[status(th)],[])).
% 0.08/0.44 tff(171,plain,
% 0.08/0.44 (![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1)))) <=> ![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))),
% 0.08/0.44 inference(quant_intro,[status(thm)],[170])).
% 0.08/0.44 tff(172,plain,
% 0.08/0.44 (^[E: $i, T: $i, T1: $i, T2: $i] : trans(monotonicity(trans(monotonicity(rewrite((environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))) <=> (~((~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1)))))), ((~(environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1)))) <=> (~(~((~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1)))))))), rewrite((~(~((~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1)))))) <=> ((~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))), ((~(environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1)))) <=> ((~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1)))))), ((greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~(environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))) <=> (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | ((~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))))), rewrite((greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | ((~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))) <=> (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))), ((greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~(environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))) <=> (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))))),
% 0.08/0.44 inference(bind,[status(th)],[])).
% 0.08/0.44 tff(173,plain,
% 0.08/0.44 (![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~(environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))) <=> ![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))),
% 0.08/0.44 inference(quant_intro,[status(thm)],[172])).
% 0.08/0.44 tff(174,plain,
% 0.08/0.44 (![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~(environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))) <=> ![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~(environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1)))))),
% 0.08/0.44 inference(rewrite,[status(thm)],[])).
% 0.08/0.44 tff(175,plain,
% 0.08/0.44 (^[E: $i, T: $i, T1: $i, T2: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite(((environment(E) & greater_or_equal(T, T1)) & greater_or_equal(T2, T)) <=> (environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T))), ((((environment(E) & greater_or_equal(T, T1)) & greater_or_equal(T2, T)) & subpopulations(first_movers, efficient_producers, E, T2)) <=> ((environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T)) & subpopulations(first_movers, efficient_producers, E, T2)))), rewrite(((environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T)) & subpopulations(first_movers, efficient_producers, E, T2)) <=> (environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2))), ((((environment(E) & greater_or_equal(T, T1)) & greater_or_equal(T2, T)) & subpopulations(first_movers, efficient_producers, E, T2)) <=> (environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2)))), (((((environment(E) & greater_or_equal(T, T1)) & greater_or_equal(T2, T)) & subpopulations(first_movers, efficient_producers, E, T2)) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))) <=> ((environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2)) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))), rewrite(((environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2)) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))) <=> (environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1)))), (((((environment(E) & greater_or_equal(T, T1)) & greater_or_equal(T2, T)) & subpopulations(first_movers, efficient_producers, E, T2)) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))) <=> (environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))), rewrite(((~decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T)))) => greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2))) <=> (decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)))), ((((((environment(E) & greater_or_equal(T, T1)) & greater_or_equal(T2, T)) & subpopulations(first_movers, efficient_producers, E, 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(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, 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)))))), rewrite(((environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, 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)))) <=> (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~(environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1)))))), ((((((environment(E) & greater_or_equal(T, T1)) & greater_or_equal(T2, T)) & subpopulations(first_movers, efficient_producers, E, 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)))) <=> (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~(environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1)))))))),
% 0.08/0.45 inference(bind,[status(th)],[])).
% 0.08/0.45 tff(176,plain,
% 0.08/0.45 (![E: $i, T: $i, T1: $i, T2: $i] : (((((environment(E) & greater_or_equal(T, T1)) & greater_or_equal(T2, T)) & subpopulations(first_movers, efficient_producers, E, 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)))) <=> ![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~(environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1)))))),
% 0.08/0.45 inference(quant_intro,[status(thm)],[175])).
% 0.08/0.45 tff(177,axiom,(![E: $i, T: $i, T1: $i, T2: $i] : (((((environment(E) & greater_or_equal(T, T1)) & greater_or_equal(T2, T)) & subpopulations(first_movers, efficient_producers, E, 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))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp_positive_function_difference')).
% 0.08/0.45 tff(178,plain,
% 0.08/0.45 (![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~(environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1)))))),
% 0.08/0.45 inference(modus_ponens,[status(thm)],[177, 176])).
% 0.08/0.45 tff(179,plain,
% 0.08/0.45 (![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~(environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1)))))),
% 0.08/0.45 inference(modus_ponens,[status(thm)],[178, 174])).
% 0.08/0.45 tff(180,plain,(
% 0.08/0.45 ![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~(environment(E) & greater_or_equal(T, T1) & greater_or_equal(T2, T) & subpopulations(first_movers, efficient_producers, E, T2) & greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1)))))),
% 0.08/0.45 inference(skolemize,[status(sab)],[179])).
% 0.08/0.45 tff(181,plain,
% 0.08/0.45 (![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))),
% 0.08/0.45 inference(modus_ponens,[status(thm)],[180, 173])).
% 0.08/0.45 tff(182,plain,
% 0.08/0.45 (![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))),
% 0.08/0.45 inference(modus_ponens,[status(thm)],[181, 171])).
% 0.08/0.45 tff(183,plain,
% 0.08/0.45 (((~![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))) | (greater(disbanding_rate(first_movers, T!0), disbanding_rate(efficient_producers, T!0)) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, T!0)) | (~greater_or_equal(T!0, initial_FM_EP(E!1))) | decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))) | (~greater(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))) | (~greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1))))) <=> ((~![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))) | greater(disbanding_rate(first_movers, T!0), disbanding_rate(efficient_producers, T!0)) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, T!0)) | (~greater_or_equal(T!0, initial_FM_EP(E!1))) | decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))) | (~greater(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))) | (~greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1))))),
% 0.08/0.45 inference(rewrite,[status(thm)],[])).
% 0.08/0.45 tff(184,plain,
% 0.08/0.45 ((greater(disbanding_rate(first_movers, T!0), disbanding_rate(efficient_producers, T!0)) | decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))) | (~environment(E!1)) | (~greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1))) | (~greater_or_equal(T!0, initial_FM_EP(E!1))) | (~subpopulations(first_movers, efficient_producers, E!1, T!0)) | (~greater(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1))))) <=> (greater(disbanding_rate(first_movers, T!0), disbanding_rate(efficient_producers, T!0)) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, T!0)) | (~greater_or_equal(T!0, initial_FM_EP(E!1))) | decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))) | (~greater(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))) | (~greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1))))),
% 0.08/0.45 inference(rewrite,[status(thm)],[])).
% 0.08/0.45 tff(185,plain,
% 0.08/0.45 (((~![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))) | (greater(disbanding_rate(first_movers, T!0), disbanding_rate(efficient_producers, T!0)) | decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))) | (~environment(E!1)) | (~greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1))) | (~greater_or_equal(T!0, initial_FM_EP(E!1))) | (~subpopulations(first_movers, efficient_producers, E!1, T!0)) | (~greater(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))))) <=> ((~![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))) | (greater(disbanding_rate(first_movers, T!0), disbanding_rate(efficient_producers, T!0)) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, T!0)) | (~greater_or_equal(T!0, initial_FM_EP(E!1))) | decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))) | (~greater(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))) | (~greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1)))))),
% 0.08/0.45 inference(monotonicity,[status(thm)],[184])).
% 0.08/0.45 tff(186,plain,
% 0.08/0.45 (((~![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))) | (greater(disbanding_rate(first_movers, T!0), disbanding_rate(efficient_producers, T!0)) | decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))) | (~environment(E!1)) | (~greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1))) | (~greater_or_equal(T!0, initial_FM_EP(E!1))) | (~subpopulations(first_movers, efficient_producers, E!1, T!0)) | (~greater(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))))) <=> ((~![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))) | greater(disbanding_rate(first_movers, T!0), disbanding_rate(efficient_producers, T!0)) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, T!0)) | (~greater_or_equal(T!0, initial_FM_EP(E!1))) | decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))) | (~greater(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))) | (~greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1))))),
% 0.08/0.45 inference(transitivity,[status(thm)],[185, 183])).
% 0.08/0.45 tff(187,plain,
% 0.08/0.45 ((~![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))) | (greater(disbanding_rate(first_movers, T!0), disbanding_rate(efficient_producers, T!0)) | decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))) | (~environment(E!1)) | (~greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1))) | (~greater_or_equal(T!0, initial_FM_EP(E!1))) | (~subpopulations(first_movers, efficient_producers, E!1, T!0)) | (~greater(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))))),
% 0.22/0.46 inference(quant_inst,[status(thm)],[])).
% 0.22/0.46 tff(188,plain,
% 0.22/0.46 ((~![E: $i, T: $i, T1: $i, T2: $i] : (greater(disbanding_rate(first_movers, T2), disbanding_rate(efficient_producers, T2)) | decreases(difference(disbanding_rate(first_movers, T), disbanding_rate(efficient_producers, T))) | (~environment(E)) | (~greater_or_equal(T, T1)) | (~greater_or_equal(T2, T)) | (~subpopulations(first_movers, efficient_producers, E, T2)) | (~greater(disbanding_rate(first_movers, T1), disbanding_rate(efficient_producers, T1))))) | greater(disbanding_rate(first_movers, T!0), disbanding_rate(efficient_producers, T!0)) | (~environment(E!1)) | (~subpopulations(first_movers, efficient_producers, E!1, T!0)) | (~greater_or_equal(T!0, initial_FM_EP(E!1))) | decreases(difference(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))) | (~greater(disbanding_rate(first_movers, initial_FM_EP(E!1)), disbanding_rate(efficient_producers, initial_FM_EP(E!1)))) | (~greater_or_equal(initial_FM_EP(E!1), initial_FM_EP(E!1)))),
% 0.22/0.46 inference(modus_ponens,[status(thm)],[187, 186])).
% 0.22/0.46 tff(189,plain,
% 0.22/0.46 ($false),
% 0.22/0.46 inference(unit_resolution,[status(thm)],[188, 182, 10, 57, 169, 69, 168, 154, 134])).
% 0.22/0.46 % SZS output end Proof
% 0.22/0.46 % E exiting
%------------------------------------------------------------------------------