%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : MGT027+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% Command : run_E %s %d THM
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:24:00 AM UTC 2026
% Result : Theorem 0.03s 0.33s
% Output : Proof 0.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : MGT027+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.01 % Command : run_E %s %d THM
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Mon Sep 7 12:13:43 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.33 % SZS status Theorem
% 0.03/0.33 % SZS output start Proof
% 0.03/0.33 tff(greater_type, type, (
% 0.03/0.33 greater: ( $i * $i ) > $o)).
% 0.03/0.33 tff(appear_type, type, (
% 0.03/0.33 appear: ( $i * $i ) > $i)).
% 0.03/0.33 tff(tptp_fun_E_2_type, type, (
% 0.03/0.33 tptp_fun_E_2: $i)).
% 0.03/0.33 tff(efficient_producers_type, type, (
% 0.03/0.33 efficient_producers: $i)).
% 0.03/0.33 tff(tptp_fun_T_0_type, type, (
% 0.03/0.33 tptp_fun_T_0: $i > $i)).
% 0.03/0.33 tff(tptp_fun_To_1_type, type, (
% 0.03/0.33 tptp_fun_To_1: $i > $i)).
% 0.03/0.33 tff(in_environment_type, type, (
% 0.03/0.33 in_environment: ( $i * $i ) > $o)).
% 0.03/0.33 tff(stable_type, type, (
% 0.03/0.33 stable: $i > $o)).
% 0.03/0.33 tff(contracts_from_type, type, (
% 0.03/0.33 contracts_from: ( $i * $i ) > $o)).
% 0.03/0.33 tff(first_movers_type, type, (
% 0.03/0.33 first_movers: $i)).
% 0.03/0.33 tff(environment_type, type, (
% 0.03/0.33 environment: $i > $o)).
% 0.03/0.33 tff(zero_type, type, (
% 0.03/0.33 zero: $i)).
% 0.03/0.33 tff(cardinality_at_time_type, type, (
% 0.03/0.33 cardinality_at_time: ( $i * $i ) > $i)).
% 0.03/0.33 tff(subpopulations_type, type, (
% 0.03/0.33 subpopulations: ( $i * $i * $i * $i ) > $o)).
% 0.03/0.33 tff(greater_or_equal_type, type, (
% 0.03/0.33 greater_or_equal: ( $i * $i ) > $o)).
% 0.03/0.33 tff(growth_rate_type, type, (
% 0.03/0.33 growth_rate: ( $i * $i ) > $i)).
% 0.03/0.33 tff(1,assumption,(greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))), introduced(assumption)).
% 0.03/0.33 tff(2,assumption,(~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))), introduced(assumption)).
% 0.03/0.33 tff(3,plain,
% 0.03/0.33 (((environment(E!2) & stable(E!2)) & ![To: $i] : (~(greater(To, appear(efficient_producers, E!2)) & contracts_from(To, first_movers)))) <=> (environment(E!2) & stable(E!2) & ![To: $i] : (~(greater(To, appear(efficient_producers, E!2)) & contracts_from(To, first_movers))))),
% 0.03/0.33 inference(rewrite,[status(thm)],[])).
% 0.03/0.33 tff(4,plain,
% 0.03/0.33 ((~![E: $i] : ((~(environment(E) & stable(E))) | ?[To: $i] : (greater(To, appear(efficient_producers, E)) & contracts_from(To, first_movers)))) <=> (~![E: $i] : ((~(environment(E) & stable(E))) | ?[To: $i] : (greater(To, appear(efficient_producers, E)) & contracts_from(To, first_movers))))),
% 0.03/0.33 inference(rewrite,[status(thm)],[])).
% 0.03/0.33 tff(5,plain,
% 0.03/0.33 ((~![E: $i] : ((environment(E) & stable(E)) => ?[To: $i] : (greater(To, appear(efficient_producers, E)) & contracts_from(To, first_movers)))) <=> (~![E: $i] : ((~(environment(E) & stable(E))) | ?[To: $i] : (greater(To, appear(efficient_producers, E)) & contracts_from(To, first_movers))))),
% 0.03/0.33 inference(rewrite,[status(thm)],[])).
% 0.03/0.33 tff(6,axiom,(~![E: $i] : ((environment(E) & stable(E)) => ?[To: $i] : (greater(To, appear(efficient_producers, E)) & contracts_from(To, first_movers)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','prove_l9')).
% 0.03/0.33 tff(7,plain,
% 0.03/0.33 (~![E: $i] : ((~(environment(E) & stable(E))) | ?[To: $i] : (greater(To, appear(efficient_producers, E)) & contracts_from(To, first_movers)))),
% 0.03/0.33 inference(modus_ponens,[status(thm)],[6, 5])).
% 0.03/0.33 tff(8,plain,
% 0.03/0.33 (~![E: $i] : ((~(environment(E) & stable(E))) | ?[To: $i] : (greater(To, appear(efficient_producers, E)) & contracts_from(To, first_movers)))),
% 0.03/0.33 inference(modus_ponens,[status(thm)],[7, 4])).
% 0.03/0.33 tff(9,plain,
% 0.03/0.33 (~![E: $i] : ((~(environment(E) & stable(E))) | ?[To: $i] : (greater(To, appear(efficient_producers, E)) & contracts_from(To, first_movers)))),
% 0.03/0.33 inference(modus_ponens,[status(thm)],[8, 4])).
% 0.03/0.33 tff(10,plain,
% 0.03/0.33 (~![E: $i] : ((~(environment(E) & stable(E))) | ?[To: $i] : (greater(To, appear(efficient_producers, E)) & contracts_from(To, first_movers)))),
% 0.03/0.33 inference(modus_ponens,[status(thm)],[9, 4])).
% 0.03/0.33 tff(11,plain,
% 0.03/0.33 (environment(E!2) & stable(E!2) & ![To: $i] : (~(greater(To, appear(efficient_producers, E!2)) & contracts_from(To, first_movers)))),
% 0.03/0.33 inference(modus_ponens,[status(thm)],[10, 3])).
% 0.03/0.33 tff(12,plain,
% 0.03/0.33 (stable(E!2)),
% 0.03/0.33 inference(and_elim,[status(thm)],[11])).
% 0.03/0.33 tff(13,plain,
% 0.03/0.33 (environment(E!2)),
% 0.03/0.33 inference(and_elim,[status(thm)],[11])).
% 0.03/0.33 tff(14,plain,
% 0.03/0.33 (^[E: $i] : refl((in_environment(E, appear(efficient_producers, E)) | (~environment(E)) | (~stable(E))) <=> (in_environment(E, appear(efficient_producers, E)) | (~environment(E)) | (~stable(E))))),
% 0.03/0.33 inference(bind,[status(th)],[])).
% 0.03/0.33 tff(15,plain,
% 0.03/0.33 (![E: $i] : (in_environment(E, appear(efficient_producers, E)) | (~environment(E)) | (~stable(E))) <=> ![E: $i] : (in_environment(E, appear(efficient_producers, E)) | (~environment(E)) | (~stable(E)))),
% 0.03/0.33 inference(quant_intro,[status(thm)],[14])).
% 0.03/0.33 tff(16,plain,
% 0.03/0.33 (^[E: $i] : trans(monotonicity(trans(monotonicity(rewrite((environment(E) & stable(E)) <=> (~((~environment(E)) | (~stable(E))))), ((~(environment(E) & stable(E))) <=> (~(~((~environment(E)) | (~stable(E))))))), rewrite((~(~((~environment(E)) | (~stable(E))))) <=> ((~environment(E)) | (~stable(E)))), ((~(environment(E) & stable(E))) <=> ((~environment(E)) | (~stable(E))))), (((~(environment(E) & stable(E))) | in_environment(E, appear(efficient_producers, E))) <=> (((~environment(E)) | (~stable(E))) | in_environment(E, appear(efficient_producers, E))))), rewrite((((~environment(E)) | (~stable(E))) | in_environment(E, appear(efficient_producers, E))) <=> (in_environment(E, appear(efficient_producers, E)) | (~environment(E)) | (~stable(E)))), (((~(environment(E) & stable(E))) | in_environment(E, appear(efficient_producers, E))) <=> (in_environment(E, appear(efficient_producers, E)) | (~environment(E)) | (~stable(E)))))),
% 0.03/0.33 inference(bind,[status(th)],[])).
% 0.03/0.33 tff(17,plain,
% 0.03/0.33 (![E: $i] : ((~(environment(E) & stable(E))) | in_environment(E, appear(efficient_producers, E))) <=> ![E: $i] : (in_environment(E, appear(efficient_producers, E)) | (~environment(E)) | (~stable(E)))),
% 0.03/0.33 inference(quant_intro,[status(thm)],[16])).
% 0.03/0.33 tff(18,plain,
% 0.03/0.33 (![E: $i] : ((~(environment(E) & stable(E))) | in_environment(E, appear(efficient_producers, E))) <=> ![E: $i] : ((~(environment(E) & stable(E))) | in_environment(E, appear(efficient_producers, E)))),
% 0.03/0.33 inference(rewrite,[status(thm)],[])).
% 0.03/0.33 tff(19,plain,
% 0.03/0.33 (^[E: $i] : rewrite(((environment(E) & stable(E)) => in_environment(E, appear(efficient_producers, E))) <=> ((~(environment(E) & stable(E))) | in_environment(E, appear(efficient_producers, E))))),
% 0.03/0.33 inference(bind,[status(th)],[])).
% 0.03/0.33 tff(20,plain,
% 0.03/0.33 (![E: $i] : ((environment(E) & stable(E)) => in_environment(E, appear(efficient_producers, E))) <=> ![E: $i] : ((~(environment(E) & stable(E))) | in_environment(E, appear(efficient_producers, E)))),
% 0.03/0.33 inference(quant_intro,[status(thm)],[19])).
% 0.03/0.33 tff(21,axiom,(![E: $i] : ((environment(E) & stable(E)) => in_environment(E, appear(efficient_producers, E)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mp_EP_in_stable_environments')).
% 0.03/0.33 tff(22,plain,
% 0.03/0.33 (![E: $i] : ((~(environment(E) & stable(E))) | in_environment(E, appear(efficient_producers, E)))),
% 0.03/0.33 inference(modus_ponens,[status(thm)],[21, 20])).
% 0.03/0.33 tff(23,plain,
% 0.03/0.33 (![E: $i] : ((~(environment(E) & stable(E))) | in_environment(E, appear(efficient_producers, E)))),
% 0.03/0.33 inference(modus_ponens,[status(thm)],[22, 18])).
% 0.03/0.33 tff(24,plain,(
% 0.03/0.33 ![E: $i] : ((~(environment(E) & stable(E))) | in_environment(E, appear(efficient_producers, E)))),
% 0.03/0.33 inference(skolemize,[status(sab)],[23])).
% 0.03/0.33 tff(25,plain,
% 0.03/0.33 (![E: $i] : (in_environment(E, appear(efficient_producers, E)) | (~environment(E)) | (~stable(E)))),
% 0.03/0.33 inference(modus_ponens,[status(thm)],[24, 17])).
% 0.03/0.33 tff(26,plain,
% 0.03/0.33 (![E: $i] : (in_environment(E, appear(efficient_producers, E)) | (~environment(E)) | (~stable(E)))),
% 0.03/0.33 inference(modus_ponens,[status(thm)],[25, 15])).
% 0.03/0.33 tff(27,plain,
% 0.03/0.33 (((~![E: $i] : (in_environment(E, appear(efficient_producers, E)) | (~environment(E)) | (~stable(E)))) | (in_environment(E!2, appear(efficient_producers, E!2)) | (~environment(E!2)) | (~stable(E!2)))) <=> ((~![E: $i] : (in_environment(E, appear(efficient_producers, E)) | (~environment(E)) | (~stable(E)))) | in_environment(E!2, appear(efficient_producers, E!2)) | (~environment(E!2)) | (~stable(E!2)))),
% 0.03/0.33 inference(rewrite,[status(thm)],[])).
% 0.03/0.33 tff(28,plain,
% 0.03/0.33 ((~![E: $i] : (in_environment(E, appear(efficient_producers, E)) | (~environment(E)) | (~stable(E)))) | (in_environment(E!2, appear(efficient_producers, E!2)) | (~environment(E!2)) | (~stable(E!2)))),
% 0.03/0.33 inference(quant_inst,[status(thm)],[])).
% 0.03/0.33 tff(29,plain,
% 0.03/0.33 ((~![E: $i] : (in_environment(E, appear(efficient_producers, E)) | (~environment(E)) | (~stable(E)))) | in_environment(E!2, appear(efficient_producers, E!2)) | (~environment(E!2)) | (~stable(E!2))),
% 0.03/0.33 inference(modus_ponens,[status(thm)],[28, 27])).
% 0.03/0.33 tff(30,plain,
% 0.03/0.33 (in_environment(E!2, appear(efficient_producers, E!2))),
% 0.03/0.33 inference(unit_resolution,[status(thm)],[29, 26, 13, 12])).
% 0.03/0.33 tff(31,plain,
% 0.03/0.33 (^[E: $i, T1: $i, T2: $i] : refl((in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1))) <=> (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1))))),
% 0.03/0.33 inference(bind,[status(th)],[])).
% 0.03/0.33 tff(32,plain,
% 0.03/0.33 (![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1))) <=> ![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))),
% 0.03/0.33 inference(quant_intro,[status(thm)],[31])).
% 0.03/0.33 tff(33,plain,
% 0.03/0.33 (^[E: $i, T1: $i, T2: $i] : trans(monotonicity(trans(monotonicity(rewrite((environment(E) & stable(E) & in_environment(E, T1) & greater(T2, T1)) <=> (~((~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1))))), ((~(environment(E) & stable(E) & in_environment(E, T1) & greater(T2, T1))) <=> (~(~((~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1))))))), rewrite((~(~((~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1))))) <=> ((~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))), ((~(environment(E) & stable(E) & in_environment(E, T1) & greater(T2, T1))) <=> ((~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1))))), (((~(environment(E) & stable(E) & in_environment(E, T1) & greater(T2, T1))) | in_environment(E, T2)) <=> (((~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1))) | in_environment(E, T2)))), rewrite((((~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1))) | in_environment(E, T2)) <=> (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))), (((~(environment(E) & stable(E) & in_environment(E, T1) & greater(T2, T1))) | in_environment(E, T2)) <=> (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))))),
% 0.03/0.33 inference(bind,[status(th)],[])).
% 0.03/0.33 tff(34,plain,
% 0.03/0.33 (![E: $i, T1: $i, T2: $i] : ((~(environment(E) & stable(E) & in_environment(E, T1) & greater(T2, T1))) | in_environment(E, T2)) <=> ![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))),
% 0.03/0.33 inference(quant_intro,[status(thm)],[33])).
% 0.03/0.33 tff(35,plain,
% 0.03/0.33 (![E: $i, T1: $i, T2: $i] : ((~(environment(E) & stable(E) & in_environment(E, T1) & greater(T2, T1))) | in_environment(E, T2)) <=> ![E: $i, T1: $i, T2: $i] : ((~(environment(E) & stable(E) & in_environment(E, T1) & greater(T2, T1))) | in_environment(E, T2))),
% 0.03/0.33 inference(rewrite,[status(thm)],[])).
% 0.03/0.33 tff(36,plain,
% 0.03/0.33 (^[E: $i, T1: $i, T2: $i] : trans(monotonicity(trans(monotonicity(rewrite(((environment(E) & stable(E)) & in_environment(E, T1)) <=> (environment(E) & stable(E) & in_environment(E, T1))), ((((environment(E) & stable(E)) & in_environment(E, T1)) & greater(T2, T1)) <=> ((environment(E) & stable(E) & in_environment(E, T1)) & greater(T2, T1)))), rewrite(((environment(E) & stable(E) & in_environment(E, T1)) & greater(T2, T1)) <=> (environment(E) & stable(E) & in_environment(E, T1) & greater(T2, T1))), ((((environment(E) & stable(E)) & in_environment(E, T1)) & greater(T2, T1)) <=> (environment(E) & stable(E) & in_environment(E, T1) & greater(T2, T1)))), (((((environment(E) & stable(E)) & in_environment(E, T1)) & greater(T2, T1)) => in_environment(E, T2)) <=> ((environment(E) & stable(E) & in_environment(E, T1) & greater(T2, T1)) => in_environment(E, T2)))), rewrite(((environment(E) & stable(E) & in_environment(E, T1) & greater(T2, T1)) => in_environment(E, T2)) <=> ((~(environment(E) & stable(E) & in_environment(E, T1) & greater(T2, T1))) | in_environment(E, T2))), (((((environment(E) & stable(E)) & in_environment(E, T1)) & greater(T2, T1)) => in_environment(E, T2)) <=> ((~(environment(E) & stable(E) & in_environment(E, T1) & greater(T2, T1))) | in_environment(E, T2))))),
% 0.03/0.33 inference(bind,[status(th)],[])).
% 0.03/0.33 tff(37,plain,
% 0.03/0.33 (![E: $i, T1: $i, T2: $i] : ((((environment(E) & stable(E)) & in_environment(E, T1)) & greater(T2, T1)) => in_environment(E, T2)) <=> ![E: $i, T1: $i, T2: $i] : ((~(environment(E) & stable(E) & in_environment(E, T1) & greater(T2, T1))) | in_environment(E, T2))),
% 0.03/0.33 inference(quant_intro,[status(thm)],[36])).
% 0.03/0.33 tff(38,axiom,(![E: $i, T1: $i, T2: $i] : ((((environment(E) & stable(E)) & in_environment(E, T1)) & greater(T2, T1)) => in_environment(E, T2))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mp_long_stable_environments')).
% 0.03/0.33 tff(39,plain,
% 0.03/0.33 (![E: $i, T1: $i, T2: $i] : ((~(environment(E) & stable(E) & in_environment(E, T1) & greater(T2, T1))) | in_environment(E, T2))),
% 0.03/0.33 inference(modus_ponens,[status(thm)],[38, 37])).
% 0.03/0.33 tff(40,plain,
% 0.03/0.33 (![E: $i, T1: $i, T2: $i] : ((~(environment(E) & stable(E) & in_environment(E, T1) & greater(T2, T1))) | in_environment(E, T2))),
% 0.03/0.33 inference(modus_ponens,[status(thm)],[39, 35])).
% 0.03/0.33 tff(41,plain,(
% 0.03/0.33 ![E: $i, T1: $i, T2: $i] : ((~(environment(E) & stable(E) & in_environment(E, T1) & greater(T2, T1))) | in_environment(E, T2))),
% 0.03/0.33 inference(skolemize,[status(sab)],[40])).
% 0.03/0.33 tff(42,plain,
% 0.03/0.33 (![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))),
% 0.03/0.33 inference(modus_ponens,[status(thm)],[41, 34])).
% 0.03/0.33 tff(43,plain,
% 0.03/0.33 (![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))),
% 0.03/0.33 inference(modus_ponens,[status(thm)],[42, 32])).
% 0.03/0.33 tff(44,plain,
% 0.03/0.33 (((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))) | ((~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, appear(efficient_producers, E!2))) | in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))) <=> ((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))) | (~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, appear(efficient_producers, E!2))) | in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))),
% 0.03/0.33 inference(rewrite,[status(thm)],[])).
% 0.03/0.33 tff(45,plain,
% 0.03/0.33 ((in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, appear(efficient_producers, E!2))) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)))) <=> ((~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, appear(efficient_producers, E!2))) | in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))),
% 0.03/0.33 inference(rewrite,[status(thm)],[])).
% 0.03/0.33 tff(46,plain,
% 0.03/0.33 (((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))) | (in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, appear(efficient_producers, E!2))) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))) <=> ((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))) | ((~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, appear(efficient_producers, E!2))) | in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)))))),
% 0.03/0.33 inference(monotonicity,[status(thm)],[45])).
% 0.03/0.33 tff(47,plain,
% 0.03/0.33 (((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))) | (in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, appear(efficient_producers, E!2))) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))) <=> ((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))) | (~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, appear(efficient_producers, E!2))) | in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))),
% 0.03/0.33 inference(transitivity,[status(thm)],[46, 44])).
% 0.03/0.33 tff(48,plain,
% 0.03/0.33 ((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))) | (in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, appear(efficient_producers, E!2))) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))),
% 0.03/0.33 inference(quant_inst,[status(thm)],[])).
% 0.03/0.33 tff(49,plain,
% 0.03/0.33 ((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))) | (~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, appear(efficient_producers, E!2))) | in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)))),
% 0.03/0.33 inference(modus_ponens,[status(thm)],[48, 47])).
% 0.03/0.33 tff(50,plain,
% 0.03/0.33 ($false),
% 0.03/0.33 inference(unit_resolution,[status(thm)],[49, 43, 13, 12, 30, 2, 1])).
% 0.03/0.33 tff(51,plain,(in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)))), inference(lemma,lemma(discharge,[]))).
% 0.03/0.33 tff(52,plain,
% 0.03/0.33 (in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))),
% 0.03/0.33 inference(unit_resolution,[status(thm)],[51, 1])).
% 0.03/0.33 tff(53,assumption,(~in_environment(E!2, tptp_fun_To_1(E!2))), introduced(assumption)).
% 0.03/0.33 tff(54,plain,
% 0.03/0.33 (^[E: $i] : refl(((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E)))))))) <=> ((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E)))))))))),
% 0.03/0.33 inference(bind,[status(th)],[])).
% 0.03/0.33 tff(55,plain,
% 0.03/0.33 (![E: $i] : ((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E)))))))) <=> ![E: $i] : ((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E))))))))),
% 0.03/0.33 inference(quant_intro,[status(thm)],[54])).
% 0.03/0.33 tff(56,plain,
% 0.03/0.33 (^[E: $i] : rewrite(((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E)))))))) <=> ((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E)))))))))),
% 0.03/0.33 inference(bind,[status(th)],[])).
% 0.03/0.33 tff(57,plain,
% 0.10/0.34 (![E: $i] : ((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E)))))))) <=> ![E: $i] : ((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E))))))))),
% 0.10/0.34 inference(quant_intro,[status(thm)],[56])).
% 0.10/0.34 tff(58,plain,
% 0.10/0.34 (![E: $i] : ((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E)))))))) <=> ![E: $i] : ((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E))))))))),
% 0.10/0.34 inference(transitivity,[status(thm)],[57, 55])).
% 0.10/0.34 tff(59,plain,
% 0.10/0.34 (^[E: $i] : trans(monotonicity(trans(monotonicity(rewrite((environment(E) & stable(E)) <=> (~((~environment(E)) | (~stable(E))))), ((~(environment(E) & stable(E))) <=> (~(~((~environment(E)) | (~stable(E))))))), rewrite((~(~((~environment(E)) | (~stable(E))))) <=> ((~environment(E)) | (~stable(E)))), ((~(environment(E) & stable(E))) <=> ((~environment(E)) | (~stable(E))))), trans(monotonicity(quant_intro(proof_bind(^[T: $i] : trans(monotonicity(trans(monotonicity(rewrite((subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, tptp_fun_To_1(E))) <=> (~((~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E)))))), ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, tptp_fun_To_1(E)))) <=> (~(~((~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E)))))))), rewrite((~(~((~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E)))))) <=> ((~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E))))), ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, tptp_fun_To_1(E)))) <=> ((~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E)))))), (((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, tptp_fun_To_1(E)))) | greater(zero, growth_rate(first_movers, T))) <=> (((~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E)))) | greater(zero, growth_rate(first_movers, T))))), rewrite((((~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E)))) | greater(zero, growth_rate(first_movers, T))) <=> (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E))))), (((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, tptp_fun_To_1(E)))) | greater(zero, growth_rate(first_movers, T))) <=> (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E))))))), (![T: $i] : ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, tptp_fun_To_1(E)))) | greater(zero, growth_rate(first_movers, T))) <=> ![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E)))))), ((greater(tptp_fun_To_1(E), appear(efficient_producers, E)) & ![T: $i] : ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, tptp_fun_To_1(E)))) | greater(zero, growth_rate(first_movers, T)))) <=> (greater(tptp_fun_To_1(E), appear(efficient_producers, E)) & ![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E))))))), rewrite((greater(tptp_fun_To_1(E), appear(efficient_producers, E)) & ![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E))))) <=> (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E)))))))), ((greater(tptp_fun_To_1(E), appear(efficient_producers, E)) & ![T: $i] : ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, tptp_fun_To_1(E)))) | greater(zero, growth_rate(first_movers, T)))) <=> (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E))))))))), (((~(environment(E) & stable(E))) | (greater(tptp_fun_To_1(E), appear(efficient_producers, E)) & ![T: $i] : ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, tptp_fun_To_1(E)))) | greater(zero, growth_rate(first_movers, T))))) <=> (((~environment(E)) | (~stable(E))) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E)))))))))), rewrite((((~environment(E)) | (~stable(E))) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E)))))))) <=> ((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E))))))))), (((~(environment(E) & stable(E))) | (greater(tptp_fun_To_1(E), appear(efficient_producers, E)) & ![T: $i] : ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, tptp_fun_To_1(E)))) | greater(zero, growth_rate(first_movers, T))))) <=> ((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E))))))))))),
% 0.10/0.34 inference(bind,[status(th)],[])).
% 0.10/0.34 tff(60,plain,
% 0.10/0.34 (![E: $i] : ((~(environment(E) & stable(E))) | (greater(tptp_fun_To_1(E), appear(efficient_producers, E)) & ![T: $i] : ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, tptp_fun_To_1(E)))) | greater(zero, growth_rate(first_movers, T))))) <=> ![E: $i] : ((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E))))))))),
% 0.10/0.34 inference(quant_intro,[status(thm)],[59])).
% 0.10/0.34 tff(61,plain,
% 0.10/0.34 (![E: $i] : ((~(environment(E) & stable(E))) | ?[To: $i] : (greater(To, appear(efficient_producers, E)) & ![T: $i] : ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T))))) <=> ![E: $i] : ((~(environment(E) & stable(E))) | ?[To: $i] : (greater(To, appear(efficient_producers, E)) & ![T: $i] : ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T)))))),
% 0.10/0.34 inference(rewrite,[status(thm)],[])).
% 0.10/0.34 tff(62,plain,
% 0.10/0.34 (^[E: $i] : trans(monotonicity(quant_intro(proof_bind(^[To: $i] : rewrite((greater(To, appear(efficient_producers, E)) & ![T: $i] : ((subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, To)) => greater(zero, growth_rate(first_movers, T)))) <=> (greater(To, appear(efficient_producers, E)) & ![T: $i] : ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T)))))), (?[To: $i] : (greater(To, appear(efficient_producers, E)) & ![T: $i] : ((subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, To)) => greater(zero, growth_rate(first_movers, T)))) <=> ?[To: $i] : (greater(To, appear(efficient_producers, E)) & ![T: $i] : ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T)))))), (((environment(E) & stable(E)) => ?[To: $i] : (greater(To, appear(efficient_producers, E)) & ![T: $i] : ((subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, To)) => greater(zero, growth_rate(first_movers, T))))) <=> ((environment(E) & stable(E)) => ?[To: $i] : (greater(To, appear(efficient_producers, E)) & ![T: $i] : ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T))))))), rewrite(((environment(E) & stable(E)) => ?[To: $i] : (greater(To, appear(efficient_producers, E)) & ![T: $i] : ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T))))) <=> ((~(environment(E) & stable(E))) | ?[To: $i] : (greater(To, appear(efficient_producers, E)) & ![T: $i] : ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T)))))), (((environment(E) & stable(E)) => ?[To: $i] : (greater(To, appear(efficient_producers, E)) & ![T: $i] : ((subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, To)) => greater(zero, growth_rate(first_movers, T))))) <=> ((~(environment(E) & stable(E))) | ?[To: $i] : (greater(To, appear(efficient_producers, E)) & ![T: $i] : ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T)))))))),
% 0.10/0.34 inference(bind,[status(th)],[])).
% 0.10/0.34 tff(63,plain,
% 0.10/0.34 (![E: $i] : ((environment(E) & stable(E)) => ?[To: $i] : (greater(To, appear(efficient_producers, E)) & ![T: $i] : ((subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, To)) => greater(zero, growth_rate(first_movers, T))))) <=> ![E: $i] : ((~(environment(E) & stable(E))) | ?[To: $i] : (greater(To, appear(efficient_producers, E)) & ![T: $i] : ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T)))))),
% 0.10/0.34 inference(quant_intro,[status(thm)],[62])).
% 0.10/0.34 tff(64,axiom,(![E: $i] : ((environment(E) & stable(E)) => ?[To: $i] : (greater(To, appear(efficient_producers, E)) & ![T: $i] : ((subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, To)) => greater(zero, growth_rate(first_movers, T)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','l10')).
% 0.10/0.34 tff(65,plain,
% 0.10/0.34 (![E: $i] : ((~(environment(E) & stable(E))) | ?[To: $i] : (greater(To, appear(efficient_producers, E)) & ![T: $i] : ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T)))))),
% 0.10/0.34 inference(modus_ponens,[status(thm)],[64, 63])).
% 0.10/0.34 tff(66,plain,
% 0.10/0.34 (![E: $i] : ((~(environment(E) & stable(E))) | ?[To: $i] : (greater(To, appear(efficient_producers, E)) & ![T: $i] : ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T)))))),
% 0.10/0.34 inference(modus_ponens,[status(thm)],[65, 61])).
% 0.10/0.34 tff(67,plain,(
% 0.10/0.34 ![E: $i] : ((~(environment(E) & stable(E))) | (greater(tptp_fun_To_1(E), appear(efficient_producers, E)) & ![T: $i] : ((~(subpopulations(first_movers, efficient_producers, E, T) & greater_or_equal(T, tptp_fun_To_1(E)))) | greater(zero, growth_rate(first_movers, T)))))),
% 0.10/0.34 inference(skolemize,[status(sab)],[66])).
% 0.10/0.34 tff(68,plain,
% 0.10/0.34 (![E: $i] : ((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E))))))))),
% 0.10/0.34 inference(modus_ponens,[status(thm)],[67, 60])).
% 0.10/0.34 tff(69,plain,
% 0.10/0.34 (![E: $i] : ((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E))))))))),
% 0.10/0.34 inference(modus_ponens,[status(thm)],[68, 58])).
% 0.10/0.34 tff(70,plain,
% 0.10/0.34 (((~![E: $i] : ((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E))))))))) | ((~environment(E!2)) | (~stable(E!2)) | (~((~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E!2, T)) | (~greater_or_equal(T, tptp_fun_To_1(E!2))))))))) <=> ((~![E: $i] : ((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E))))))))) | (~environment(E!2)) | (~stable(E!2)) | (~((~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E!2, T)) | (~greater_or_equal(T, tptp_fun_To_1(E!2))))))))),
% 0.10/0.34 inference(rewrite,[status(thm)],[])).
% 0.10/0.34 tff(71,plain,
% 0.10/0.34 ((~![E: $i] : ((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E))))))))) | ((~environment(E!2)) | (~stable(E!2)) | (~((~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E!2, T)) | (~greater_or_equal(T, tptp_fun_To_1(E!2))))))))),
% 0.10/0.34 inference(quant_inst,[status(thm)],[])).
% 0.10/0.34 tff(72,plain,
% 0.10/0.34 ((~![E: $i] : ((~environment(E)) | (~stable(E)) | (~((~greater(tptp_fun_To_1(E), appear(efficient_producers, E))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E, T)) | (~greater_or_equal(T, tptp_fun_To_1(E))))))))) | (~environment(E!2)) | (~stable(E!2)) | (~((~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E!2, T)) | (~greater_or_equal(T, tptp_fun_To_1(E!2)))))))),
% 0.10/0.34 inference(modus_ponens,[status(thm)],[71, 70])).
% 0.10/0.34 tff(73,plain,
% 0.10/0.34 (~((~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E!2, T)) | (~greater_or_equal(T, tptp_fun_To_1(E!2))))))),
% 0.10/0.34 inference(unit_resolution,[status(thm)],[72, 69, 13, 12])).
% 0.10/0.34 tff(74,plain,
% 0.10/0.34 (((~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E!2, T)) | (~greater_or_equal(T, tptp_fun_To_1(E!2)))))) | greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))),
% 0.10/0.34 inference(tautology,[status(thm)],[])).
% 0.10/0.34 tff(75,plain,
% 0.10/0.34 (greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))),
% 0.10/0.34 inference(unit_resolution,[status(thm)],[74, 73])).
% 0.10/0.34 tff(76,plain,
% 0.10/0.34 (((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))) | ((~environment(E!2)) | (~stable(E!2)) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~in_environment(E!2, appear(efficient_producers, E!2))) | in_environment(E!2, tptp_fun_To_1(E!2)))) <=> ((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))) | (~environment(E!2)) | (~stable(E!2)) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~in_environment(E!2, appear(efficient_producers, E!2))) | in_environment(E!2, tptp_fun_To_1(E!2)))),
% 0.10/0.34 inference(rewrite,[status(thm)],[])).
% 0.10/0.34 tff(77,plain,
% 0.10/0.34 ((in_environment(E!2, tptp_fun_To_1(E!2)) | (~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, appear(efficient_producers, E!2))) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2)))) <=> ((~environment(E!2)) | (~stable(E!2)) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~in_environment(E!2, appear(efficient_producers, E!2))) | in_environment(E!2, tptp_fun_To_1(E!2)))),
% 0.10/0.34 inference(rewrite,[status(thm)],[])).
% 0.10/0.34 tff(78,plain,
% 0.10/0.34 (((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))) | (in_environment(E!2, tptp_fun_To_1(E!2)) | (~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, appear(efficient_producers, E!2))) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))))) <=> ((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))) | ((~environment(E!2)) | (~stable(E!2)) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~in_environment(E!2, appear(efficient_producers, E!2))) | in_environment(E!2, tptp_fun_To_1(E!2))))),
% 0.10/0.34 inference(monotonicity,[status(thm)],[77])).
% 0.10/0.34 tff(79,plain,
% 0.10/0.34 (((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))) | (in_environment(E!2, tptp_fun_To_1(E!2)) | (~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, appear(efficient_producers, E!2))) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))))) <=> ((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))) | (~environment(E!2)) | (~stable(E!2)) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~in_environment(E!2, appear(efficient_producers, E!2))) | in_environment(E!2, tptp_fun_To_1(E!2)))),
% 0.10/0.34 inference(transitivity,[status(thm)],[78, 76])).
% 0.10/0.34 tff(80,plain,
% 0.10/0.34 ((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))) | (in_environment(E!2, tptp_fun_To_1(E!2)) | (~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, appear(efficient_producers, E!2))) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))))),
% 0.10/0.34 inference(quant_inst,[status(thm)],[])).
% 0.10/0.34 tff(81,plain,
% 0.10/0.34 ((~![E: $i, T1: $i, T2: $i] : (in_environment(E, T2) | (~environment(E)) | (~stable(E)) | (~in_environment(E, T1)) | (~greater(T2, T1)))) | (~environment(E!2)) | (~stable(E!2)) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~in_environment(E!2, appear(efficient_producers, E!2))) | in_environment(E!2, tptp_fun_To_1(E!2))),
% 0.10/0.34 inference(modus_ponens,[status(thm)],[80, 79])).
% 0.10/0.34 tff(82,plain,
% 0.10/0.34 ($false),
% 0.10/0.34 inference(unit_resolution,[status(thm)],[81, 43, 13, 12, 30, 75, 53])).
% 0.10/0.34 tff(83,plain,(in_environment(E!2, tptp_fun_To_1(E!2))), inference(lemma,lemma(discharge,[]))).
% 0.10/0.34 tff(84,plain,
% 0.10/0.34 (^[To: $i] : refl(((~greater(To, appear(efficient_producers, E!2))) | (~contracts_from(To, first_movers))) <=> ((~greater(To, appear(efficient_producers, E!2))) | (~contracts_from(To, first_movers))))),
% 0.10/0.34 inference(bind,[status(th)],[])).
% 0.10/0.34 tff(85,plain,
% 0.10/0.34 (![To: $i] : ((~greater(To, appear(efficient_producers, E!2))) | (~contracts_from(To, first_movers))) <=> ![To: $i] : ((~greater(To, appear(efficient_producers, E!2))) | (~contracts_from(To, first_movers)))),
% 0.10/0.34 inference(quant_intro,[status(thm)],[84])).
% 0.10/0.34 tff(86,plain,
% 0.10/0.34 (^[To: $i] : trans(monotonicity(rewrite((greater(To, appear(efficient_producers, E!2)) & contracts_from(To, first_movers)) <=> (~((~greater(To, appear(efficient_producers, E!2))) | (~contracts_from(To, first_movers))))), ((~(greater(To, appear(efficient_producers, E!2)) & contracts_from(To, first_movers))) <=> (~(~((~greater(To, appear(efficient_producers, E!2))) | (~contracts_from(To, first_movers))))))), rewrite((~(~((~greater(To, appear(efficient_producers, E!2))) | (~contracts_from(To, first_movers))))) <=> ((~greater(To, appear(efficient_producers, E!2))) | (~contracts_from(To, first_movers)))), ((~(greater(To, appear(efficient_producers, E!2)) & contracts_from(To, first_movers))) <=> ((~greater(To, appear(efficient_producers, E!2))) | (~contracts_from(To, first_movers)))))),
% 0.10/0.34 inference(bind,[status(th)],[])).
% 0.10/0.34 tff(87,plain,
% 0.10/0.34 (![To: $i] : (~(greater(To, appear(efficient_producers, E!2)) & contracts_from(To, first_movers))) <=> ![To: $i] : ((~greater(To, appear(efficient_producers, E!2))) | (~contracts_from(To, first_movers)))),
% 0.10/0.34 inference(quant_intro,[status(thm)],[86])).
% 0.10/0.34 tff(88,plain,
% 0.10/0.34 (![To: $i] : (~(greater(To, appear(efficient_producers, E!2)) & contracts_from(To, first_movers)))),
% 0.10/0.34 inference(and_elim,[status(thm)],[11])).
% 0.10/0.34 tff(89,plain,
% 0.10/0.34 (![To: $i] : ((~greater(To, appear(efficient_producers, E!2))) | (~contracts_from(To, first_movers)))),
% 0.10/0.34 inference(modus_ponens,[status(thm)],[88, 87])).
% 0.10/0.34 tff(90,plain,
% 0.10/0.34 (![To: $i] : ((~greater(To, appear(efficient_producers, E!2))) | (~contracts_from(To, first_movers)))),
% 0.10/0.34 inference(modus_ponens,[status(thm)],[89, 85])).
% 0.10/0.34 tff(91,plain,
% 0.10/0.34 (((~![To: $i] : ((~greater(To, appear(efficient_producers, E!2))) | (~contracts_from(To, first_movers)))) | ((~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~contracts_from(tptp_fun_To_1(E!2), first_movers)))) <=> ((~![To: $i] : ((~greater(To, appear(efficient_producers, E!2))) | (~contracts_from(To, first_movers)))) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~contracts_from(tptp_fun_To_1(E!2), first_movers)))),
% 0.10/0.34 inference(rewrite,[status(thm)],[])).
% 0.10/0.34 tff(92,plain,
% 0.10/0.34 ((~![To: $i] : ((~greater(To, appear(efficient_producers, E!2))) | (~contracts_from(To, first_movers)))) | ((~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~contracts_from(tptp_fun_To_1(E!2), first_movers)))),
% 0.10/0.34 inference(quant_inst,[status(thm)],[])).
% 0.10/0.34 tff(93,plain,
% 0.10/0.34 ((~![To: $i] : ((~greater(To, appear(efficient_producers, E!2))) | (~contracts_from(To, first_movers)))) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~contracts_from(tptp_fun_To_1(E!2), first_movers))),
% 0.10/0.34 inference(modus_ponens,[status(thm)],[92, 91])).
% 0.10/0.34 tff(94,plain,
% 0.10/0.34 (~contracts_from(tptp_fun_To_1(E!2), first_movers)),
% 0.10/0.34 inference(unit_resolution,[status(thm)],[93, 90, 75])).
% 0.10/0.34 tff(95,plain,
% 0.10/0.34 (^[E: $i, To: $i] : refl((contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To))))) <=> (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To))))))),
% 0.10/0.34 inference(bind,[status(th)],[])).
% 0.10/0.34 tff(96,plain,
% 0.10/0.34 (![E: $i, To: $i] : (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To))))) <=> ![E: $i, To: $i] : (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To)))))),
% 0.10/0.34 inference(quant_intro,[status(thm)],[95])).
% 0.10/0.34 tff(97,plain,
% 0.10/0.34 (^[E: $i, To: $i] : trans(monotonicity(rewrite((~((~(greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero) & greater_or_equal(tptp_fun_T_0(To), To))) | greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))))) <=> (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To))))), ((contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~((~(greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero) & greater_or_equal(tptp_fun_T_0(To), To))) | greater(zero, growth_rate(first_movers, tptp_fun_T_0(To)))))) <=> (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To))))))), rewrite((contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To))))) <=> (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To)))))), ((contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~((~(greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero) & greater_or_equal(tptp_fun_T_0(To), To))) | greater(zero, growth_rate(first_movers, tptp_fun_T_0(To)))))) <=> (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To)))))))),
% 0.10/0.34 inference(bind,[status(th)],[])).
% 0.10/0.34 tff(98,plain,
% 0.10/0.34 (![E: $i, To: $i] : (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~((~(greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero) & greater_or_equal(tptp_fun_T_0(To), To))) | greater(zero, growth_rate(first_movers, tptp_fun_T_0(To)))))) <=> ![E: $i, To: $i] : (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To)))))),
% 0.10/0.34 inference(quant_intro,[status(thm)],[97])).
% 0.10/0.34 tff(99,plain,
% 0.10/0.34 (^[E: $i, To: $i] : rewrite((((~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~((~(greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero) & greater_or_equal(tptp_fun_T_0(To), To))) | greater(zero, growth_rate(first_movers, tptp_fun_T_0(To)))))) | contracts_from(To, first_movers)) <=> (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~((~(greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero) & greater_or_equal(tptp_fun_T_0(To), To))) | greater(zero, growth_rate(first_movers, tptp_fun_T_0(To)))))))),
% 0.10/0.34 inference(bind,[status(th)],[])).
% 0.10/0.34 tff(100,plain,
% 0.10/0.34 (![E: $i, To: $i] : (((~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~((~(greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero) & greater_or_equal(tptp_fun_T_0(To), To))) | greater(zero, growth_rate(first_movers, tptp_fun_T_0(To)))))) | contracts_from(To, first_movers)) <=> ![E: $i, To: $i] : (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~((~(greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero) & greater_or_equal(tptp_fun_T_0(To), To))) | greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))))))),
% 0.10/0.34 inference(quant_intro,[status(thm)],[99])).
% 0.10/0.34 tff(101,plain,
% 0.10/0.34 (![E: $i, To: $i] : ((~(environment(E) & stable(E) & in_environment(E, To) & ![T: $i] : ((~(greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T))))) | contracts_from(To, first_movers)) <=> ![E: $i, To: $i] : ((~(environment(E) & stable(E) & in_environment(E, To) & ![T: $i] : ((~(greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T))))) | contracts_from(To, first_movers))),
% 0.10/0.34 inference(rewrite,[status(thm)],[])).
% 0.10/0.34 tff(102,plain,
% 0.10/0.34 (^[E: $i, To: $i] : trans(monotonicity(trans(monotonicity(rewrite(((environment(E) & stable(E)) & in_environment(E, To)) <=> (environment(E) & stable(E) & in_environment(E, To))), quant_intro(proof_bind(^[T: $i] : rewrite(((greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To)) => greater(zero, growth_rate(first_movers, T))) <=> ((~(greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T))))), (![T: $i] : ((greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To)) => greater(zero, growth_rate(first_movers, T))) <=> ![T: $i] : ((~(greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T))))), ((((environment(E) & stable(E)) & in_environment(E, To)) & ![T: $i] : ((greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To)) => greater(zero, growth_rate(first_movers, T)))) <=> ((environment(E) & stable(E) & in_environment(E, To)) & ![T: $i] : ((~(greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T)))))), rewrite(((environment(E) & stable(E) & in_environment(E, To)) & ![T: $i] : ((~(greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T)))) <=> (environment(E) & stable(E) & in_environment(E, To) & ![T: $i] : ((~(greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T))))), ((((environment(E) & stable(E)) & in_environment(E, To)) & ![T: $i] : ((greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To)) => greater(zero, growth_rate(first_movers, T)))) <=> (environment(E) & stable(E) & in_environment(E, To) & ![T: $i] : ((~(greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T)))))), (((((environment(E) & stable(E)) & in_environment(E, To)) & ![T: $i] : ((greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To)) => greater(zero, growth_rate(first_movers, T)))) => contracts_from(To, first_movers)) <=> ((environment(E) & stable(E) & in_environment(E, To) & ![T: $i] : ((~(greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T)))) => contracts_from(To, first_movers)))), rewrite(((environment(E) & stable(E) & in_environment(E, To) & ![T: $i] : ((~(greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T)))) => contracts_from(To, first_movers)) <=> ((~(environment(E) & stable(E) & in_environment(E, To) & ![T: $i] : ((~(greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T))))) | contracts_from(To, first_movers))), (((((environment(E) & stable(E)) & in_environment(E, To)) & ![T: $i] : ((greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To)) => greater(zero, growth_rate(first_movers, T)))) => contracts_from(To, first_movers)) <=> ((~(environment(E) & stable(E) & in_environment(E, To) & ![T: $i] : ((~(greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T))))) | contracts_from(To, first_movers))))),
% 0.10/0.34 inference(bind,[status(th)],[])).
% 0.10/0.34 tff(103,plain,
% 0.10/0.34 (![E: $i, To: $i] : ((((environment(E) & stable(E)) & in_environment(E, To)) & ![T: $i] : ((greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To)) => greater(zero, growth_rate(first_movers, T)))) => contracts_from(To, first_movers)) <=> ![E: $i, To: $i] : ((~(environment(E) & stable(E) & in_environment(E, To) & ![T: $i] : ((~(greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T))))) | contracts_from(To, first_movers))),
% 0.10/0.34 inference(quant_intro,[status(thm)],[102])).
% 0.10/0.34 tff(104,axiom,(![E: $i, To: $i] : ((((environment(E) & stable(E)) & in_environment(E, To)) & ![T: $i] : ((greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To)) => greater(zero, growth_rate(first_movers, T)))) => contracts_from(To, first_movers))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mp_contracts_from')).
% 0.10/0.34 tff(105,plain,
% 0.10/0.34 (![E: $i, To: $i] : ((~(environment(E) & stable(E) & in_environment(E, To) & ![T: $i] : ((~(greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T))))) | contracts_from(To, first_movers))),
% 0.10/0.34 inference(modus_ponens,[status(thm)],[104, 103])).
% 0.10/0.34 tff(106,plain,
% 0.10/0.34 (![E: $i, To: $i] : ((~(environment(E) & stable(E) & in_environment(E, To) & ![T: $i] : ((~(greater(cardinality_at_time(first_movers, T), zero) & greater_or_equal(T, To))) | greater(zero, growth_rate(first_movers, T))))) | contracts_from(To, first_movers))),
% 0.10/0.34 inference(modus_ponens,[status(thm)],[105, 101])).
% 0.10/0.34 tff(107,plain,(
% 0.10/0.34 ![E: $i, To: $i] : (((~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~((~(greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero) & greater_or_equal(tptp_fun_T_0(To), To))) | greater(zero, growth_rate(first_movers, tptp_fun_T_0(To)))))) | contracts_from(To, first_movers))),
% 0.10/0.34 inference(skolemize,[status(sab)],[106])).
% 0.10/0.34 tff(108,plain,
% 0.10/0.34 (![E: $i, To: $i] : (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~((~(greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero) & greater_or_equal(tptp_fun_T_0(To), To))) | greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))))))),
% 0.10/0.34 inference(modus_ponens,[status(thm)],[107, 100])).
% 0.10/0.34 tff(109,plain,
% 0.10/0.34 (![E: $i, To: $i] : (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To)))))),
% 0.10/0.34 inference(modus_ponens,[status(thm)],[108, 98])).
% 0.10/0.34 tff(110,plain,
% 0.10/0.34 (![E: $i, To: $i] : (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To)))))),
% 0.10/0.34 inference(modus_ponens,[status(thm)],[109, 96])).
% 0.10/0.34 tff(111,plain,
% 0.10/0.34 (((~![E: $i, To: $i] : (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To)))))) | ((~environment(E!2)) | (~stable(E!2)) | contracts_from(tptp_fun_To_1(E!2), first_movers) | (~in_environment(E!2, tptp_fun_To_1(E!2))) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))))))) <=> ((~![E: $i, To: $i] : (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To)))))) | (~environment(E!2)) | (~stable(E!2)) | contracts_from(tptp_fun_To_1(E!2), first_movers) | (~in_environment(E!2, tptp_fun_To_1(E!2))) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))))))),
% 0.10/0.34 inference(rewrite,[status(thm)],[])).
% 0.10/0.34 tff(112,plain,
% 0.10/0.34 ((contracts_from(tptp_fun_To_1(E!2), first_movers) | (~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, tptp_fun_To_1(E!2))) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2)))))) <=> ((~environment(E!2)) | (~stable(E!2)) | contracts_from(tptp_fun_To_1(E!2), first_movers) | (~in_environment(E!2, tptp_fun_To_1(E!2))) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))))))),
% 0.10/0.34 inference(rewrite,[status(thm)],[])).
% 0.10/0.34 tff(113,plain,
% 0.10/0.34 ((~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))))) <=> (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2)))))),
% 0.10/0.34 inference(rewrite,[status(thm)],[])).
% 0.10/0.34 tff(114,plain,
% 0.10/0.34 ((contracts_from(tptp_fun_To_1(E!2), first_movers) | (~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, tptp_fun_To_1(E!2))) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2)))))) <=> (contracts_from(tptp_fun_To_1(E!2), first_movers) | (~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, tptp_fun_To_1(E!2))) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))))))),
% 0.10/0.34 inference(monotonicity,[status(thm)],[113])).
% 0.10/0.34 tff(115,plain,
% 0.10/0.34 ((contracts_from(tptp_fun_To_1(E!2), first_movers) | (~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, tptp_fun_To_1(E!2))) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2)))))) <=> ((~environment(E!2)) | (~stable(E!2)) | contracts_from(tptp_fun_To_1(E!2), first_movers) | (~in_environment(E!2, tptp_fun_To_1(E!2))) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))))))),
% 0.10/0.34 inference(transitivity,[status(thm)],[114, 112])).
% 0.10/0.34 tff(116,plain,
% 0.10/0.34 (((~![E: $i, To: $i] : (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To)))))) | (contracts_from(tptp_fun_To_1(E!2), first_movers) | (~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, tptp_fun_To_1(E!2))) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))))))) <=> ((~![E: $i, To: $i] : (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To)))))) | ((~environment(E!2)) | (~stable(E!2)) | contracts_from(tptp_fun_To_1(E!2), first_movers) | (~in_environment(E!2, tptp_fun_To_1(E!2))) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2)))))))),
% 0.10/0.34 inference(monotonicity,[status(thm)],[115])).
% 0.10/0.34 tff(117,plain,
% 0.10/0.34 (((~![E: $i, To: $i] : (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To)))))) | (contracts_from(tptp_fun_To_1(E!2), first_movers) | (~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, tptp_fun_To_1(E!2))) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))))))) <=> ((~![E: $i, To: $i] : (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To)))))) | (~environment(E!2)) | (~stable(E!2)) | contracts_from(tptp_fun_To_1(E!2), first_movers) | (~in_environment(E!2, tptp_fun_To_1(E!2))) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))))))),
% 0.10/0.34 inference(transitivity,[status(thm)],[116, 111])).
% 0.10/0.34 tff(118,plain,
% 0.10/0.34 ((~![E: $i, To: $i] : (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To)))))) | (contracts_from(tptp_fun_To_1(E!2), first_movers) | (~environment(E!2)) | (~stable(E!2)) | (~in_environment(E!2, tptp_fun_To_1(E!2))) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))))))),
% 0.10/0.34 inference(quant_inst,[status(thm)],[])).
% 0.10/0.34 tff(119,plain,
% 0.10/0.34 ((~![E: $i, To: $i] : (contracts_from(To, first_movers) | (~environment(E)) | (~stable(E)) | (~in_environment(E, To)) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(To))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(To)), zero)) | (~greater_or_equal(tptp_fun_T_0(To), To)))))) | (~environment(E!2)) | (~stable(E!2)) | contracts_from(tptp_fun_To_1(E!2), first_movers) | (~in_environment(E!2, tptp_fun_To_1(E!2))) | (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2)))))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[118, 117])).
% 0.10/0.35 tff(120,plain,
% 0.10/0.35 (~(greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))))),
% 0.10/0.35 inference(unit_resolution,[status(thm)],[119, 110, 13, 12, 94, 83])).
% 0.10/0.35 tff(121,plain,
% 0.10/0.35 ((greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2)))) | greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))),
% 0.10/0.35 inference(tautology,[status(thm)],[])).
% 0.10/0.35 tff(122,plain,
% 0.10/0.35 (greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))),
% 0.10/0.35 inference(unit_resolution,[status(thm)],[121, 120])).
% 0.10/0.35 tff(123,plain,
% 0.10/0.35 ((greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2)))) | (~greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))))),
% 0.10/0.35 inference(tautology,[status(thm)],[])).
% 0.10/0.35 tff(124,plain,
% 0.10/0.35 (~greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))))),
% 0.10/0.35 inference(unit_resolution,[status(thm)],[123, 120])).
% 0.10/0.35 tff(125,plain,
% 0.10/0.35 (((~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E!2, T)) | (~greater_or_equal(T, tptp_fun_To_1(E!2)))))) | ![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E!2, T)) | (~greater_or_equal(T, tptp_fun_To_1(E!2))))),
% 0.10/0.35 inference(tautology,[status(thm)],[])).
% 0.10/0.35 tff(126,plain,
% 0.10/0.35 (![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E!2, T)) | (~greater_or_equal(T, tptp_fun_To_1(E!2))))),
% 0.10/0.35 inference(unit_resolution,[status(thm)],[125, 73])).
% 0.10/0.35 tff(127,plain,
% 0.10/0.35 (((~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E!2, T)) | (~greater_or_equal(T, tptp_fun_To_1(E!2))))) | (greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))) | (~subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))))) <=> ((~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E!2, T)) | (~greater_or_equal(T, tptp_fun_To_1(E!2))))) | greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))) | (~subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))))),
% 0.10/0.35 inference(rewrite,[status(thm)],[])).
% 0.10/0.35 tff(128,plain,
% 0.10/0.35 ((greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2)))) <=> (greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))) | (~subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))))),
% 0.10/0.35 inference(rewrite,[status(thm)],[])).
% 0.10/0.35 tff(129,plain,
% 0.10/0.35 (((~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E!2, T)) | (~greater_or_equal(T, tptp_fun_To_1(E!2))))) | (greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))))) <=> ((~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E!2, T)) | (~greater_or_equal(T, tptp_fun_To_1(E!2))))) | (greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))) | (~subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))))))),
% 0.10/0.35 inference(monotonicity,[status(thm)],[128])).
% 0.10/0.35 tff(130,plain,
% 0.10/0.35 (((~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E!2, T)) | (~greater_or_equal(T, tptp_fun_To_1(E!2))))) | (greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))))) <=> ((~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E!2, T)) | (~greater_or_equal(T, tptp_fun_To_1(E!2))))) | greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))) | (~subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))))),
% 0.10/0.35 inference(transitivity,[status(thm)],[129, 127])).
% 0.10/0.35 tff(131,plain,
% 0.10/0.35 ((~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E!2, T)) | (~greater_or_equal(T, tptp_fun_To_1(E!2))))) | (greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))))),
% 0.10/0.35 inference(quant_inst,[status(thm)],[])).
% 0.10/0.35 tff(132,plain,
% 0.10/0.35 ((~![T: $i] : (greater(zero, growth_rate(first_movers, T)) | (~subpopulations(first_movers, efficient_producers, E!2, T)) | (~greater_or_equal(T, tptp_fun_To_1(E!2))))) | greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))) | (~subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[131, 130])).
% 0.10/0.35 tff(133,plain,
% 0.10/0.35 (~subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))),
% 0.10/0.35 inference(unit_resolution,[status(thm)],[132, 126, 124, 122])).
% 0.10/0.35 tff(134,plain,
% 0.10/0.35 ((greater(zero, growth_rate(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2)))) | greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)),
% 0.10/0.35 inference(tautology,[status(thm)],[])).
% 0.10/0.35 tff(135,plain,
% 0.10/0.35 (greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)),
% 0.10/0.35 inference(unit_resolution,[status(thm)],[134, 120])).
% 0.10/0.35 tff(136,plain,
% 0.10/0.35 (^[E: $i, T: $i] : refl((subpopulations(first_movers, efficient_producers, E, T) | (~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero))) <=> (subpopulations(first_movers, efficient_producers, E, T) | (~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero))))),
% 0.10/0.35 inference(bind,[status(th)],[])).
% 0.10/0.35 tff(137,plain,
% 0.10/0.35 (![E: $i, T: $i] : (subpopulations(first_movers, efficient_producers, E, T) | (~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero))) <=> ![E: $i, T: $i] : (subpopulations(first_movers, efficient_producers, E, T) | (~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero)))),
% 0.10/0.35 inference(quant_intro,[status(thm)],[136])).
% 0.10/0.35 tff(138,plain,
% 0.10/0.35 (^[E: $i, T: $i] : trans(monotonicity(trans(monotonicity(rewrite((environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero) & greater(cardinality_at_time(efficient_producers, T), zero)) <=> (~((~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero))))), ((~(environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero) & greater(cardinality_at_time(efficient_producers, T), zero))) <=> (~(~((~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero))))))), rewrite((~(~((~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero))))) <=> ((~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero)))), ((~(environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero) & greater(cardinality_at_time(efficient_producers, T), zero))) <=> ((~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero))))), (((~(environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero) & greater(cardinality_at_time(efficient_producers, T), zero))) | subpopulations(first_movers, efficient_producers, E, T)) <=> (((~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero))) | subpopulations(first_movers, efficient_producers, E, T)))), rewrite((((~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero))) | subpopulations(first_movers, efficient_producers, E, T)) <=> (subpopulations(first_movers, efficient_producers, E, T) | (~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero)))), (((~(environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero) & greater(cardinality_at_time(efficient_producers, T), zero))) | subpopulations(first_movers, efficient_producers, E, T)) <=> (subpopulations(first_movers, efficient_producers, E, T) | (~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero)))))),
% 0.10/0.35 inference(bind,[status(th)],[])).
% 0.10/0.35 tff(139,plain,
% 0.10/0.35 (![E: $i, T: $i] : ((~(environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero) & greater(cardinality_at_time(efficient_producers, T), zero))) | subpopulations(first_movers, efficient_producers, E, T)) <=> ![E: $i, T: $i] : (subpopulations(first_movers, efficient_producers, E, T) | (~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero)))),
% 0.10/0.35 inference(quant_intro,[status(thm)],[138])).
% 0.10/0.35 tff(140,plain,
% 0.10/0.35 (![E: $i, T: $i] : ((~(environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero) & greater(cardinality_at_time(efficient_producers, T), zero))) | subpopulations(first_movers, efficient_producers, E, T)) <=> ![E: $i, T: $i] : ((~(environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero) & greater(cardinality_at_time(efficient_producers, T), zero))) | subpopulations(first_movers, efficient_producers, E, T))),
% 0.10/0.35 inference(rewrite,[status(thm)],[])).
% 0.10/0.35 tff(141,plain,
% 0.10/0.35 (^[E: $i, T: $i] : trans(monotonicity(trans(monotonicity(rewrite(((environment(E) & in_environment(E, T)) & greater(cardinality_at_time(first_movers, T), zero)) <=> (environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero))), ((((environment(E) & in_environment(E, T)) & greater(cardinality_at_time(first_movers, T), zero)) & greater(cardinality_at_time(efficient_producers, T), zero)) <=> ((environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero)) & greater(cardinality_at_time(efficient_producers, T), zero)))), rewrite(((environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero)) & greater(cardinality_at_time(efficient_producers, T), zero)) <=> (environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero) & greater(cardinality_at_time(efficient_producers, T), zero))), ((((environment(E) & in_environment(E, T)) & greater(cardinality_at_time(first_movers, T), zero)) & greater(cardinality_at_time(efficient_producers, T), zero)) <=> (environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero) & greater(cardinality_at_time(efficient_producers, T), zero)))), (((((environment(E) & in_environment(E, T)) & greater(cardinality_at_time(first_movers, T), zero)) & greater(cardinality_at_time(efficient_producers, T), zero)) => subpopulations(first_movers, efficient_producers, E, T)) <=> ((environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero) & greater(cardinality_at_time(efficient_producers, T), zero)) => subpopulations(first_movers, efficient_producers, E, T)))), rewrite(((environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero) & greater(cardinality_at_time(efficient_producers, T), zero)) => subpopulations(first_movers, efficient_producers, E, T)) <=> ((~(environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero) & greater(cardinality_at_time(efficient_producers, T), zero))) | subpopulations(first_movers, efficient_producers, E, T))), (((((environment(E) & in_environment(E, T)) & greater(cardinality_at_time(first_movers, T), zero)) & greater(cardinality_at_time(efficient_producers, T), zero)) => subpopulations(first_movers, efficient_producers, E, T)) <=> ((~(environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero) & greater(cardinality_at_time(efficient_producers, T), zero))) | subpopulations(first_movers, efficient_producers, E, T))))),
% 0.10/0.35 inference(bind,[status(th)],[])).
% 0.10/0.35 tff(142,plain,
% 0.10/0.35 (![E: $i, T: $i] : ((((environment(E) & in_environment(E, T)) & greater(cardinality_at_time(first_movers, T), zero)) & greater(cardinality_at_time(efficient_producers, T), zero)) => subpopulations(first_movers, efficient_producers, E, T)) <=> ![E: $i, T: $i] : ((~(environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero) & greater(cardinality_at_time(efficient_producers, T), zero))) | subpopulations(first_movers, efficient_producers, E, T))),
% 0.10/0.35 inference(quant_intro,[status(thm)],[141])).
% 0.10/0.35 tff(143,axiom,(![E: $i, T: $i] : ((((environment(E) & in_environment(E, T)) & greater(cardinality_at_time(first_movers, T), zero)) & greater(cardinality_at_time(efficient_producers, T), zero)) => subpopulations(first_movers, efficient_producers, E, T))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mp_non_empty_fm_and_ep')).
% 0.10/0.35 tff(144,plain,
% 0.10/0.35 (![E: $i, T: $i] : ((~(environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero) & greater(cardinality_at_time(efficient_producers, T), zero))) | subpopulations(first_movers, efficient_producers, E, T))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[143, 142])).
% 0.10/0.35 tff(145,plain,
% 0.10/0.35 (![E: $i, T: $i] : ((~(environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero) & greater(cardinality_at_time(efficient_producers, T), zero))) | subpopulations(first_movers, efficient_producers, E, T))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[144, 140])).
% 0.10/0.35 tff(146,plain,(
% 0.10/0.35 ![E: $i, T: $i] : ((~(environment(E) & in_environment(E, T) & greater(cardinality_at_time(first_movers, T), zero) & greater(cardinality_at_time(efficient_producers, T), zero))) | subpopulations(first_movers, efficient_producers, E, T))),
% 0.10/0.35 inference(skolemize,[status(sab)],[145])).
% 0.10/0.35 tff(147,plain,
% 0.10/0.35 (![E: $i, T: $i] : (subpopulations(first_movers, efficient_producers, E, T) | (~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero)))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[146, 139])).
% 0.10/0.35 tff(148,plain,
% 0.10/0.35 (![E: $i, T: $i] : (subpopulations(first_movers, efficient_producers, E, T) | (~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero)))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[147, 137])).
% 0.10/0.35 tff(149,plain,
% 0.10/0.35 (((~![E: $i, T: $i] : (subpopulations(first_movers, efficient_producers, E, T) | (~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero)))) | ((~environment(E!2)) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)))) <=> ((~![E: $i, T: $i] : (subpopulations(first_movers, efficient_producers, E, T) | (~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero)))) | (~environment(E!2)) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)))),
% 0.10/0.35 inference(rewrite,[status(thm)],[])).
% 0.10/0.35 tff(150,plain,
% 0.10/0.35 ((subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~environment(E!2)) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero))) <=> ((~environment(E!2)) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)))),
% 0.10/0.35 inference(rewrite,[status(thm)],[])).
% 0.10/0.35 tff(151,plain,
% 0.10/0.35 (((~![E: $i, T: $i] : (subpopulations(first_movers, efficient_producers, E, T) | (~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero)))) | (subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~environment(E!2)) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)))) <=> ((~![E: $i, T: $i] : (subpopulations(first_movers, efficient_producers, E, T) | (~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero)))) | ((~environment(E!2)) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero))))),
% 0.10/0.35 inference(monotonicity,[status(thm)],[150])).
% 0.10/0.35 tff(152,plain,
% 0.10/0.35 (((~![E: $i, T: $i] : (subpopulations(first_movers, efficient_producers, E, T) | (~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero)))) | (subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~environment(E!2)) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)))) <=> ((~![E: $i, T: $i] : (subpopulations(first_movers, efficient_producers, E, T) | (~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero)))) | (~environment(E!2)) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)))),
% 0.10/0.35 inference(transitivity,[status(thm)],[151, 149])).
% 0.10/0.35 tff(153,plain,
% 0.10/0.35 ((~![E: $i, T: $i] : (subpopulations(first_movers, efficient_producers, E, T) | (~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero)))) | (subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~environment(E!2)) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | (~greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)))),
% 0.10/0.35 inference(quant_inst,[status(thm)],[])).
% 0.10/0.35 tff(154,plain,
% 0.10/0.35 ((~![E: $i, T: $i] : (subpopulations(first_movers, efficient_producers, E, T) | (~environment(E)) | (~in_environment(E, T)) | (~greater(cardinality_at_time(first_movers, T), zero)) | (~greater(cardinality_at_time(efficient_producers, T), zero)))) | (~environment(E!2)) | (~greater(cardinality_at_time(first_movers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)) | subpopulations(first_movers, efficient_producers, E!2, tptp_fun_T_0(tptp_fun_To_1(E!2))) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[153, 152])).
% 0.10/0.35 tff(155,plain,
% 0.10/0.35 ((~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero))),
% 0.10/0.35 inference(unit_resolution,[status(thm)],[154, 148, 13, 135, 133])).
% 0.10/0.35 tff(156,plain,
% 0.10/0.35 (~greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)),
% 0.10/0.35 inference(unit_resolution,[status(thm)],[155, 52])).
% 0.10/0.35 tff(157,plain,
% 0.10/0.35 (^[X: $i, Y: $i] : refl((greater_or_equal(X, Y) <=> ((X = Y) | greater(X, Y))) <=> (greater_or_equal(X, Y) <=> ((X = Y) | greater(X, Y))))),
% 0.10/0.35 inference(bind,[status(th)],[])).
% 0.10/0.35 tff(158,plain,
% 0.10/0.35 (![X: $i, Y: $i] : (greater_or_equal(X, Y) <=> ((X = Y) | greater(X, Y))) <=> ![X: $i, Y: $i] : (greater_or_equal(X, Y) <=> ((X = Y) | greater(X, Y)))),
% 0.10/0.35 inference(quant_intro,[status(thm)],[157])).
% 0.10/0.35 tff(159,plain,
% 0.10/0.35 (![X: $i, Y: $i] : (greater_or_equal(X, Y) <=> ((X = Y) | greater(X, Y))) <=> ![X: $i, Y: $i] : (greater_or_equal(X, Y) <=> ((X = Y) | greater(X, Y)))),
% 0.10/0.35 inference(rewrite,[status(thm)],[])).
% 0.10/0.35 tff(160,plain,
% 0.10/0.35 (^[X: $i, Y: $i] : rewrite((greater_or_equal(X, Y) <=> (greater(X, Y) | (X = Y))) <=> (greater_or_equal(X, Y) <=> ((X = Y) | greater(X, Y))))),
% 0.10/0.35 inference(bind,[status(th)],[])).
% 0.10/0.35 tff(161,plain,
% 0.10/0.35 (![X: $i, Y: $i] : (greater_or_equal(X, Y) <=> (greater(X, Y) | (X = Y))) <=> ![X: $i, Y: $i] : (greater_or_equal(X, Y) <=> ((X = Y) | greater(X, Y)))),
% 0.10/0.35 inference(quant_intro,[status(thm)],[160])).
% 0.10/0.35 tff(162,axiom,(![X: $i, Y: $i] : (greater_or_equal(X, Y) <=> (greater(X, Y) | (X = Y)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mp_greater_or_equal')).
% 0.10/0.35 tff(163,plain,
% 0.10/0.35 (![X: $i, Y: $i] : (greater_or_equal(X, Y) <=> ((X = Y) | greater(X, Y)))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[162, 161])).
% 0.10/0.35 tff(164,plain,
% 0.10/0.35 (![X: $i, Y: $i] : (greater_or_equal(X, Y) <=> ((X = Y) | greater(X, Y)))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[163, 159])).
% 0.10/0.35 tff(165,plain,(
% 0.10/0.35 ![X: $i, Y: $i] : (greater_or_equal(X, Y) <=> ((X = Y) | greater(X, Y)))),
% 0.10/0.35 inference(skolemize,[status(sab)],[164])).
% 0.10/0.35 tff(166,plain,
% 0.10/0.35 (![X: $i, Y: $i] : (greater_or_equal(X, Y) <=> ((X = Y) | greater(X, Y)))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[165, 158])).
% 0.10/0.35 tff(167,plain,
% 0.10/0.35 ((~![X: $i, Y: $i] : (greater_or_equal(X, Y) <=> ((X = Y) | greater(X, Y)))) | (greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)) <=> ((tptp_fun_T_0(tptp_fun_To_1(E!2)) = appear(efficient_producers, E!2)) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))),
% 0.10/0.35 inference(quant_inst,[status(thm)],[])).
% 0.10/0.35 tff(168,plain,
% 0.10/0.35 (greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)) <=> ((tptp_fun_T_0(tptp_fun_To_1(E!2)) = appear(efficient_producers, E!2)) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)))),
% 0.10/0.35 inference(unit_resolution,[status(thm)],[167, 166])).
% 0.10/0.35 tff(169,plain,
% 0.10/0.35 (((tptp_fun_T_0(tptp_fun_To_1(E!2)) = appear(efficient_producers, E!2)) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)))),
% 0.10/0.35 inference(tautology,[status(thm)],[])).
% 0.10/0.35 tff(170,plain,
% 0.10/0.35 ((tptp_fun_T_0(tptp_fun_To_1(E!2)) = appear(efficient_producers, E!2)) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))),
% 0.10/0.35 inference(unit_resolution,[status(thm)],[169, 1])).
% 0.10/0.35 tff(171,plain,
% 0.10/0.35 ((~(greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)) <=> ((tptp_fun_T_0(tptp_fun_To_1(E!2)) = appear(efficient_producers, E!2)) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))) | greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)) | (~((tptp_fun_T_0(tptp_fun_To_1(E!2)) = appear(efficient_producers, E!2)) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))),
% 0.10/0.35 inference(tautology,[status(thm)],[])).
% 0.10/0.35 tff(172,plain,
% 0.10/0.35 ((~(greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)) <=> ((tptp_fun_T_0(tptp_fun_To_1(E!2)) = appear(efficient_producers, E!2)) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))) | greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))),
% 0.10/0.35 inference(unit_resolution,[status(thm)],[171, 170])).
% 0.10/0.35 tff(173,plain,
% 0.10/0.35 (greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))),
% 0.10/0.35 inference(unit_resolution,[status(thm)],[172, 168])).
% 0.10/0.35 tff(174,plain,
% 0.10/0.35 (^[E: $i, T: $i] : refl((greater(cardinality_at_time(efficient_producers, T), zero) | (~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E)))) <=> (greater(cardinality_at_time(efficient_producers, T), zero) | (~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E)))))),
% 0.10/0.35 inference(bind,[status(th)],[])).
% 0.10/0.35 tff(175,plain,
% 0.10/0.35 (![E: $i, T: $i] : (greater(cardinality_at_time(efficient_producers, T), zero) | (~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E)))) <=> ![E: $i, T: $i] : (greater(cardinality_at_time(efficient_producers, T), zero) | (~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E))))),
% 0.10/0.35 inference(quant_intro,[status(thm)],[174])).
% 0.10/0.35 tff(176,plain,
% 0.10/0.35 (^[E: $i, T: $i] : trans(monotonicity(trans(monotonicity(rewrite((environment(E) & in_environment(E, T) & greater_or_equal(T, appear(efficient_producers, E))) <=> (~((~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E)))))), ((~(environment(E) & in_environment(E, T) & greater_or_equal(T, appear(efficient_producers, E)))) <=> (~(~((~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E)))))))), rewrite((~(~((~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E)))))) <=> ((~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E))))), ((~(environment(E) & in_environment(E, T) & greater_or_equal(T, appear(efficient_producers, E)))) <=> ((~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E)))))), (((~(environment(E) & in_environment(E, T) & greater_or_equal(T, appear(efficient_producers, E)))) | greater(cardinality_at_time(efficient_producers, T), zero)) <=> (((~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E)))) | greater(cardinality_at_time(efficient_producers, T), zero)))), rewrite((((~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E)))) | greater(cardinality_at_time(efficient_producers, T), zero)) <=> (greater(cardinality_at_time(efficient_producers, T), zero) | (~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E))))), (((~(environment(E) & in_environment(E, T) & greater_or_equal(T, appear(efficient_producers, E)))) | greater(cardinality_at_time(efficient_producers, T), zero)) <=> (greater(cardinality_at_time(efficient_producers, T), zero) | (~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E))))))),
% 0.10/0.35 inference(bind,[status(th)],[])).
% 0.10/0.35 tff(177,plain,
% 0.10/0.35 (![E: $i, T: $i] : ((~(environment(E) & in_environment(E, T) & greater_or_equal(T, appear(efficient_producers, E)))) | greater(cardinality_at_time(efficient_producers, T), zero)) <=> ![E: $i, T: $i] : (greater(cardinality_at_time(efficient_producers, T), zero) | (~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E))))),
% 0.10/0.35 inference(quant_intro,[status(thm)],[176])).
% 0.10/0.35 tff(178,plain,
% 0.10/0.35 (![E: $i, T: $i] : ((~(environment(E) & in_environment(E, T) & greater_or_equal(T, appear(efficient_producers, E)))) | greater(cardinality_at_time(efficient_producers, T), zero)) <=> ![E: $i, T: $i] : ((~(environment(E) & in_environment(E, T) & greater_or_equal(T, appear(efficient_producers, E)))) | greater(cardinality_at_time(efficient_producers, T), zero))),
% 0.10/0.35 inference(rewrite,[status(thm)],[])).
% 0.10/0.35 tff(179,plain,
% 0.10/0.35 (^[E: $i, T: $i] : trans(monotonicity(rewrite(((environment(E) & in_environment(E, T)) & greater_or_equal(T, appear(efficient_producers, E))) <=> (environment(E) & in_environment(E, T) & greater_or_equal(T, appear(efficient_producers, E)))), ((((environment(E) & in_environment(E, T)) & greater_or_equal(T, appear(efficient_producers, E))) => greater(cardinality_at_time(efficient_producers, T), zero)) <=> ((environment(E) & in_environment(E, T) & greater_or_equal(T, appear(efficient_producers, E))) => greater(cardinality_at_time(efficient_producers, T), zero)))), rewrite(((environment(E) & in_environment(E, T) & greater_or_equal(T, appear(efficient_producers, E))) => greater(cardinality_at_time(efficient_producers, T), zero)) <=> ((~(environment(E) & in_environment(E, T) & greater_or_equal(T, appear(efficient_producers, E)))) | greater(cardinality_at_time(efficient_producers, T), zero))), ((((environment(E) & in_environment(E, T)) & greater_or_equal(T, appear(efficient_producers, E))) => greater(cardinality_at_time(efficient_producers, T), zero)) <=> ((~(environment(E) & in_environment(E, T) & greater_or_equal(T, appear(efficient_producers, E)))) | greater(cardinality_at_time(efficient_producers, T), zero))))),
% 0.10/0.35 inference(bind,[status(th)],[])).
% 0.10/0.35 tff(180,plain,
% 0.10/0.35 (![E: $i, T: $i] : (((environment(E) & in_environment(E, T)) & greater_or_equal(T, appear(efficient_producers, E))) => greater(cardinality_at_time(efficient_producers, T), zero)) <=> ![E: $i, T: $i] : ((~(environment(E) & in_environment(E, T) & greater_or_equal(T, appear(efficient_producers, E)))) | greater(cardinality_at_time(efficient_producers, T), zero))),
% 0.10/0.35 inference(quant_intro,[status(thm)],[179])).
% 0.10/0.35 tff(181,axiom,(![E: $i, T: $i] : (((environment(E) & in_environment(E, T)) & greater_or_equal(T, appear(efficient_producers, E))) => greater(cardinality_at_time(efficient_producers, T), zero))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t6')).
% 0.10/0.35 tff(182,plain,
% 0.10/0.35 (![E: $i, T: $i] : ((~(environment(E) & in_environment(E, T) & greater_or_equal(T, appear(efficient_producers, E)))) | greater(cardinality_at_time(efficient_producers, T), zero))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[181, 180])).
% 0.10/0.35 tff(183,plain,
% 0.10/0.35 (![E: $i, T: $i] : ((~(environment(E) & in_environment(E, T) & greater_or_equal(T, appear(efficient_producers, E)))) | greater(cardinality_at_time(efficient_producers, T), zero))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[182, 178])).
% 0.10/0.35 tff(184,plain,(
% 0.10/0.35 ![E: $i, T: $i] : ((~(environment(E) & in_environment(E, T) & greater_or_equal(T, appear(efficient_producers, E)))) | greater(cardinality_at_time(efficient_producers, T), zero))),
% 0.10/0.35 inference(skolemize,[status(sab)],[183])).
% 0.10/0.35 tff(185,plain,
% 0.10/0.35 (![E: $i, T: $i] : (greater(cardinality_at_time(efficient_producers, T), zero) | (~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E))))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[184, 177])).
% 0.10/0.35 tff(186,plain,
% 0.10/0.35 (![E: $i, T: $i] : (greater(cardinality_at_time(efficient_producers, T), zero) | (~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E))))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[185, 175])).
% 0.10/0.35 tff(187,plain,
% 0.10/0.35 (((~![E: $i, T: $i] : (greater(cardinality_at_time(efficient_producers, T), zero) | (~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E))))) | ((~environment(E!2)) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))) <=> ((~![E: $i, T: $i] : (greater(cardinality_at_time(efficient_producers, T), zero) | (~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E))))) | (~environment(E!2)) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))),
% 0.10/0.35 inference(rewrite,[status(thm)],[])).
% 0.10/0.35 tff(188,plain,
% 0.10/0.35 ((greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero) | (~environment(E!2)) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)))) <=> ((~environment(E!2)) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))),
% 0.10/0.35 inference(rewrite,[status(thm)],[])).
% 0.10/0.35 tff(189,plain,
% 0.10/0.35 (((~![E: $i, T: $i] : (greater(cardinality_at_time(efficient_producers, T), zero) | (~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E))))) | (greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero) | (~environment(E!2)) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))) <=> ((~![E: $i, T: $i] : (greater(cardinality_at_time(efficient_producers, T), zero) | (~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E))))) | ((~environment(E!2)) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)))))),
% 0.10/0.35 inference(monotonicity,[status(thm)],[188])).
% 0.10/0.35 tff(190,plain,
% 0.10/0.35 (((~![E: $i, T: $i] : (greater(cardinality_at_time(efficient_producers, T), zero) | (~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E))))) | (greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero) | (~environment(E!2)) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))) <=> ((~![E: $i, T: $i] : (greater(cardinality_at_time(efficient_producers, T), zero) | (~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E))))) | (~environment(E!2)) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))),
% 0.10/0.35 inference(transitivity,[status(thm)],[189, 187])).
% 0.10/0.35 tff(191,plain,
% 0.10/0.35 ((~![E: $i, T: $i] : (greater(cardinality_at_time(efficient_producers, T), zero) | (~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E))))) | (greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero) | (~environment(E!2)) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))),
% 0.10/0.35 inference(quant_inst,[status(thm)],[])).
% 0.10/0.35 tff(192,plain,
% 0.10/0.35 ((~![E: $i, T: $i] : (greater(cardinality_at_time(efficient_producers, T), zero) | (~environment(E)) | (~in_environment(E, T)) | (~greater_or_equal(T, appear(efficient_producers, E))))) | (~environment(E!2)) | (~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[191, 190])).
% 0.10/0.35 tff(193,plain,
% 0.10/0.35 ((~in_environment(E!2, tptp_fun_T_0(tptp_fun_To_1(E!2)))) | greater(cardinality_at_time(efficient_producers, tptp_fun_T_0(tptp_fun_To_1(E!2))), zero)),
% 0.10/0.35 inference(unit_resolution,[status(thm)],[192, 186, 13, 173])).
% 0.10/0.35 tff(194,plain,
% 0.10/0.35 ($false),
% 0.10/0.35 inference(unit_resolution,[status(thm)],[193, 156, 52])).
% 0.10/0.35 tff(195,plain,(~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))), inference(lemma,lemma(discharge,[]))).
% 0.10/0.35 tff(196,assumption,(greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))), introduced(assumption)).
% 0.10/0.35 tff(197,plain,
% 0.10/0.35 (![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(X, Y)) | (~greater(Y, Z))) <=> ![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(X, Y)) | (~greater(Y, Z)))),
% 0.10/0.35 inference(rewrite,[status(thm)],[])).
% 0.10/0.35 tff(198,plain,
% 0.10/0.35 (^[X: $i, Y: $i, Z: $i] : trans(monotonicity(trans(monotonicity(rewrite((greater(X, Y) & greater(Y, Z)) <=> (~((~greater(X, Y)) | (~greater(Y, Z))))), ((~(greater(X, Y) & greater(Y, Z))) <=> (~(~((~greater(X, Y)) | (~greater(Y, Z))))))), rewrite((~(~((~greater(X, Y)) | (~greater(Y, Z))))) <=> ((~greater(X, Y)) | (~greater(Y, Z)))), ((~(greater(X, Y) & greater(Y, Z))) <=> ((~greater(X, Y)) | (~greater(Y, Z))))), (((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z)) <=> (((~greater(X, Y)) | (~greater(Y, Z))) | greater(X, Z)))), rewrite((((~greater(X, Y)) | (~greater(Y, Z))) | greater(X, Z)) <=> (greater(X, Z) | (~greater(X, Y)) | (~greater(Y, Z)))), (((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z)) <=> (greater(X, Z) | (~greater(X, Y)) | (~greater(Y, Z)))))),
% 0.10/0.35 inference(bind,[status(th)],[])).
% 0.10/0.35 tff(199,plain,
% 0.10/0.35 (![X: $i, Y: $i, Z: $i] : ((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z)) <=> ![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(X, Y)) | (~greater(Y, Z)))),
% 0.10/0.35 inference(quant_intro,[status(thm)],[198])).
% 0.10/0.35 tff(200,plain,
% 0.10/0.35 (![X: $i, Y: $i, Z: $i] : ((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z)) <=> ![X: $i, Y: $i, Z: $i] : ((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z))),
% 0.10/0.35 inference(rewrite,[status(thm)],[])).
% 0.10/0.35 tff(201,plain,
% 0.10/0.35 (^[X: $i, Y: $i, Z: $i] : rewrite(((greater(X, Y) & greater(Y, Z)) => greater(X, Z)) <=> ((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z)))),
% 0.10/0.35 inference(bind,[status(th)],[])).
% 0.10/0.35 tff(202,plain,
% 0.10/0.35 (![X: $i, Y: $i, Z: $i] : ((greater(X, Y) & greater(Y, Z)) => greater(X, Z)) <=> ![X: $i, Y: $i, Z: $i] : ((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z))),
% 0.10/0.35 inference(quant_intro,[status(thm)],[201])).
% 0.10/0.35 tff(203,axiom,(![X: $i, Y: $i, Z: $i] : ((greater(X, Y) & greater(Y, Z)) => greater(X, Z))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mp_greater_transitivity')).
% 0.10/0.35 tff(204,plain,
% 0.10/0.35 (![X: $i, Y: $i, Z: $i] : ((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[203, 202])).
% 0.10/0.35 tff(205,plain,
% 0.10/0.35 (![X: $i, Y: $i, Z: $i] : ((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[204, 200])).
% 0.10/0.35 tff(206,plain,(
% 0.10/0.35 ![X: $i, Y: $i, Z: $i] : ((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z))),
% 0.10/0.35 inference(skolemize,[status(sab)],[205])).
% 0.10/0.35 tff(207,plain,
% 0.10/0.35 (![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(X, Y)) | (~greater(Y, Z)))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[206, 199])).
% 0.10/0.35 tff(208,plain,
% 0.10/0.35 (![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(X, Y)) | (~greater(Y, Z)))),
% 0.10/0.35 inference(modus_ponens,[status(thm)],[207, 197])).
% 0.10/0.35 tff(209,plain,
% 0.10/0.35 (((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(X, Y)) | (~greater(Y, Z)))) | ((~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)))) <=> ((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(X, Y)) | (~greater(Y, Z)))) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)))),
% 0.10/0.35 inference(rewrite,[status(thm)],[])).
% 0.10/0.35 tff(210,plain,
% 0.10/0.35 ((greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2)))) <=> ((~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)))),
% 0.10/0.35 inference(rewrite,[status(thm)],[])).
% 0.10/0.35 tff(211,plain,
% 0.10/0.35 (((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(X, Y)) | (~greater(Y, Z)))) | (greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))))) <=> ((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(X, Y)) | (~greater(Y, Z)))) | ((~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))))),
% 0.10/0.35 inference(monotonicity,[status(thm)],[210])).
% 0.10/0.35 tff(212,plain,
% 0.10/0.35 (((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(X, Y)) | (~greater(Y, Z)))) | (greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))))) <=> ((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(X, Y)) | (~greater(Y, Z)))) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)))),
% 0.10/0.36 inference(transitivity,[status(thm)],[211, 209])).
% 0.10/0.36 tff(213,plain,
% 0.10/0.36 ((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(X, Y)) | (~greater(Y, Z)))) | (greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))))),
% 0.10/0.36 inference(quant_inst,[status(thm)],[])).
% 0.10/0.36 tff(214,plain,
% 0.10/0.36 ((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(X, Y)) | (~greater(Y, Z)))) | (~greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))) | (~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))),
% 0.10/0.36 inference(modus_ponens,[status(thm)],[213, 212])).
% 0.10/0.36 tff(215,plain,
% 0.10/0.36 ($false),
% 0.10/0.36 inference(unit_resolution,[status(thm)],[214, 208, 75, 196, 195])).
% 0.10/0.36 tff(216,plain,(~greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))), inference(lemma,lemma(discharge,[]))).
% 0.10/0.36 tff(217,plain,
% 0.10/0.36 ((~![X: $i, Y: $i] : (greater_or_equal(X, Y) <=> ((X = Y) | greater(X, Y)))) | (greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2)) <=> ((tptp_fun_T_0(tptp_fun_To_1(E!2)) = tptp_fun_To_1(E!2)) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))))),
% 0.10/0.36 inference(quant_inst,[status(thm)],[])).
% 0.10/0.36 tff(218,plain,
% 0.10/0.36 (greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2)) <=> ((tptp_fun_T_0(tptp_fun_To_1(E!2)) = tptp_fun_To_1(E!2)) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2)))),
% 0.10/0.36 inference(unit_resolution,[status(thm)],[217, 166])).
% 0.10/0.36 tff(219,plain,
% 0.10/0.36 ((~(greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2)) <=> ((tptp_fun_T_0(tptp_fun_To_1(E!2)) = tptp_fun_To_1(E!2)) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))))) | (~greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))) | ((tptp_fun_T_0(tptp_fun_To_1(E!2)) = tptp_fun_To_1(E!2)) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2)))),
% 0.10/0.36 inference(tautology,[status(thm)],[])).
% 0.10/0.36 tff(220,plain,
% 0.10/0.36 ((~(greater_or_equal(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2)) <=> ((tptp_fun_T_0(tptp_fun_To_1(E!2)) = tptp_fun_To_1(E!2)) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))))) | ((tptp_fun_T_0(tptp_fun_To_1(E!2)) = tptp_fun_To_1(E!2)) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2)))),
% 0.10/0.36 inference(unit_resolution,[status(thm)],[219, 122])).
% 0.10/0.36 tff(221,plain,
% 0.10/0.36 ((tptp_fun_T_0(tptp_fun_To_1(E!2)) = tptp_fun_To_1(E!2)) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))),
% 0.10/0.36 inference(unit_resolution,[status(thm)],[220, 218])).
% 0.10/0.36 tff(222,plain,
% 0.10/0.36 ((~((tptp_fun_T_0(tptp_fun_To_1(E!2)) = tptp_fun_To_1(E!2)) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2)))) | (tptp_fun_T_0(tptp_fun_To_1(E!2)) = tptp_fun_To_1(E!2)) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))),
% 0.10/0.36 inference(tautology,[status(thm)],[])).
% 0.10/0.36 tff(223,plain,
% 0.10/0.36 ((tptp_fun_T_0(tptp_fun_To_1(E!2)) = tptp_fun_To_1(E!2)) | greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), tptp_fun_To_1(E!2))),
% 0.10/0.36 inference(unit_resolution,[status(thm)],[222, 221])).
% 0.10/0.36 tff(224,plain,
% 0.10/0.36 (tptp_fun_T_0(tptp_fun_To_1(E!2)) = tptp_fun_To_1(E!2)),
% 0.10/0.36 inference(unit_resolution,[status(thm)],[223, 216])).
% 0.10/0.36 tff(225,plain,
% 0.10/0.36 (greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2)) <=> greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2))),
% 0.10/0.36 inference(monotonicity,[status(thm)],[224])).
% 0.10/0.36 tff(226,plain,
% 0.10/0.36 (greater(tptp_fun_To_1(E!2), appear(efficient_producers, E!2)) <=> greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))),
% 0.10/0.36 inference(symmetry,[status(thm)],[225])).
% 0.10/0.36 tff(227,plain,
% 0.10/0.36 (greater(tptp_fun_T_0(tptp_fun_To_1(E!2)), appear(efficient_producers, E!2))),
% 0.10/0.36 inference(modus_ponens,[status(thm)],[75, 226])).
% 0.10/0.36 tff(228,plain,
% 0.10/0.36 ($false),
% 0.10/0.36 inference(unit_resolution,[status(thm)],[195, 227])).
% 0.10/0.36 % SZS output end Proof
% 0.10/0.36 % E exiting
%------------------------------------------------------------------------------