%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : MGT035-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% Command : run_E %s %d THM
% Computer : n001.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:02 AM UTC 2026
% Result : Unsatisfiable 0.20s 0.54s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT035-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : run_E %s %d THM
% 0.06/0.34 % Computer : n001.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Mon Sep 7 12:40:09 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.20/0.54 % SZS status Unsatisfiable
% 0.20/0.54 % SZS output start Proof
% 0.20/0.54 tff(greater_type, type, (
% 0.20/0.54 greater: ( $i * $i ) > $o)).
% 0.20/0.54 tff(sk1_type, type, (
% 0.20/0.54 sk1: $i > $i)).
% 0.20/0.54 tff(sk3_type, type, (
% 0.20/0.54 sk3: $i)).
% 0.20/0.54 tff(sk4_type, type, (
% 0.20/0.54 sk4: $i > $i)).
% 0.20/0.54 tff(sk2_type, type, (
% 0.20/0.54 sk2: $i > $i)).
% 0.20/0.54 tff(greater_or_equal_type, type, (
% 0.20/0.54 greater_or_equal: ( $i * $i ) > $o)).
% 0.20/0.54 tff(growth_rate_type, type, (
% 0.20/0.54 growth_rate: ( $i * $i ) > $i)).
% 0.20/0.54 tff(first_movers_type, type, (
% 0.20/0.54 first_movers: $i)).
% 0.20/0.54 tff(efficient_producers_type, type, (
% 0.20/0.54 efficient_producers: $i)).
% 0.20/0.54 tff(equilibrium_type, type, (
% 0.20/0.54 equilibrium: $i > $i)).
% 0.20/0.54 tff(in_environment_type, type, (
% 0.20/0.54 in_environment: ( $i * $i ) > $o)).
% 0.20/0.54 tff(stable_type, type, (
% 0.20/0.54 stable: $i > $o)).
% 0.20/0.54 tff(environment_type, type, (
% 0.20/0.54 environment: $i > $o)).
% 0.20/0.54 tff(zero_type, type, (
% 0.20/0.54 zero: $i)).
% 0.20/0.54 tff(subpopulations_type, type, (
% 0.20/0.54 subpopulations: ( $i * $i * $i * $i ) > $o)).
% 0.20/0.54 tff(outcompetes_type, type, (
% 0.20/0.54 outcompetes: ( $i * $i * $i ) > $o)).
% 0.20/0.54 tff(1,assumption,(~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))), introduced(assumption)).
% 0.20/0.54 tff(2,plain,
% 0.20/0.54 (^[B: $i, A: $i] : refl(((~greater(A, B)) | greater_or_equal(A, B)) <=> ((~greater(A, B)) | greater_or_equal(A, B)))),
% 0.20/0.54 inference(bind,[status(th)],[])).
% 0.20/0.54 tff(3,plain,
% 0.20/0.54 (![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B)) <=> ![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))),
% 0.20/0.54 inference(quant_intro,[status(thm)],[2])).
% 0.20/0.54 tff(4,plain,
% 0.20/0.54 (![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B)) <=> ![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))),
% 0.20/0.54 inference(rewrite,[status(thm)],[])).
% 0.20/0.54 tff(5,axiom,(![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp_greater_or_equal_25')).
% 0.20/0.54 tff(6,plain,
% 0.20/0.54 (![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))),
% 0.20/0.54 inference(modus_ponens,[status(thm)],[5, 4])).
% 0.20/0.54 tff(7,plain,(
% 0.20/0.54 ![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))),
% 0.20/0.54 inference(skolemize,[status(sab)],[6])).
% 0.20/0.54 tff(8,plain,
% 0.20/0.54 (![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))),
% 0.20/0.54 inference(modus_ponens,[status(thm)],[7, 3])).
% 0.20/0.54 tff(9,plain,
% 0.20/0.54 (((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | ((~greater(sk4(sk2(sk3)), equilibrium(sk3))) | greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3)))) <=> ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | (~greater(sk4(sk2(sk3)), equilibrium(sk3))) | greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3)))),
% 0.20/0.54 inference(rewrite,[status(thm)],[])).
% 0.20/0.54 tff(10,plain,
% 0.20/0.54 ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | ((~greater(sk4(sk2(sk3)), equilibrium(sk3))) | greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3)))),
% 0.20/0.54 inference(quant_inst,[status(thm)],[])).
% 0.20/0.54 tff(11,plain,
% 0.20/0.54 ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | (~greater(sk4(sk2(sk3)), equilibrium(sk3))) | greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))),
% 0.20/0.54 inference(modus_ponens,[status(thm)],[10, 9])).
% 0.20/0.54 tff(12,plain,
% 0.20/0.54 (~greater(sk4(sk2(sk3)), equilibrium(sk3))),
% 0.20/0.55 inference(unit_resolution,[status(thm)],[11, 8, 1])).
% 0.20/0.55 tff(13,assumption,(greater(sk4(sk2(sk3)), sk2(sk3))), introduced(assumption)).
% 0.20/0.55 tff(14,assumption,(sk2(sk3) = equilibrium(sk3)), introduced(assumption)).
% 0.20/0.55 tff(15,plain,
% 0.20/0.55 (greater_or_equal(sk4(sk2(sk3)), sk2(sk3)) <=> greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))),
% 0.20/0.55 inference(monotonicity,[status(thm)],[14])).
% 0.20/0.55 tff(16,plain,
% 0.20/0.55 (greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3)) <=> greater_or_equal(sk4(sk2(sk3)), sk2(sk3))),
% 0.20/0.55 inference(symmetry,[status(thm)],[15])).
% 0.20/0.55 tff(17,plain,
% 0.20/0.55 ((~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) <=> (~greater_or_equal(sk4(sk2(sk3)), sk2(sk3)))),
% 0.20/0.55 inference(monotonicity,[status(thm)],[16])).
% 0.20/0.55 tff(18,plain,
% 0.20/0.55 (~greater_or_equal(sk4(sk2(sk3)), sk2(sk3))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[1, 17])).
% 0.20/0.55 tff(19,plain,
% 0.20/0.55 (stable(sk3) <=> stable(sk3)),
% 0.20/0.55 inference(rewrite,[status(thm)],[])).
% 0.20/0.55 tff(20,axiom,(stable(sk3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove_t4_43')).
% 0.20/0.55 tff(21,plain,
% 0.20/0.55 (stable(sk3)),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[20, 19])).
% 0.20/0.55 tff(22,plain,
% 0.20/0.55 (environment(sk3) <=> environment(sk3)),
% 0.20/0.55 inference(rewrite,[status(thm)],[])).
% 0.20/0.55 tff(23,axiom,(environment(sk3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove_t4_42')).
% 0.20/0.55 tff(24,plain,
% 0.20/0.55 (environment(sk3)),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[23, 22])).
% 0.20/0.55 tff(25,plain,
% 0.20/0.55 (^[A: $i] : refl((in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A))) <=> (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A))))),
% 0.20/0.55 inference(bind,[status(th)],[])).
% 0.20/0.55 tff(26,plain,
% 0.20/0.55 (![A: $i] : (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A))) <=> ![A: $i] : (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A)))),
% 0.20/0.55 inference(quant_intro,[status(thm)],[25])).
% 0.20/0.55 tff(27,plain,
% 0.20/0.55 (![A: $i] : (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A))) <=> ![A: $i] : (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A)))),
% 0.20/0.55 inference(rewrite,[status(thm)],[])).
% 0.20/0.55 tff(28,plain,
% 0.20/0.55 (^[A: $i] : rewrite((((~environment(A)) | (~stable(A))) | in_environment(A, sk2(A))) <=> (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A))))),
% 0.20/0.55 inference(bind,[status(th)],[])).
% 0.20/0.55 tff(29,plain,
% 0.20/0.55 (![A: $i] : (((~environment(A)) | (~stable(A))) | in_environment(A, sk2(A))) <=> ![A: $i] : (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A)))),
% 0.20/0.55 inference(quant_intro,[status(thm)],[28])).
% 0.20/0.55 tff(30,axiom,(![A: $i] : (((~environment(A)) | (~stable(A))) | in_environment(A, sk2(A)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','a4_40')).
% 0.20/0.55 tff(31,plain,
% 0.20/0.55 (![A: $i] : (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A)))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[30, 29])).
% 0.20/0.55 tff(32,plain,
% 0.20/0.55 (![A: $i] : (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A)))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[31, 27])).
% 0.20/0.55 tff(33,plain,(
% 0.20/0.55 ![A: $i] : (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A)))),
% 0.20/0.55 inference(skolemize,[status(sab)],[32])).
% 0.20/0.55 tff(34,plain,
% 0.20/0.55 (![A: $i] : (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A)))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[33, 26])).
% 0.20/0.55 tff(35,plain,
% 0.20/0.55 (((~![A: $i] : (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A)))) | ((~stable(sk3)) | (~environment(sk3)) | in_environment(sk3, sk2(sk3)))) <=> ((~![A: $i] : (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A)))) | (~stable(sk3)) | (~environment(sk3)) | in_environment(sk3, sk2(sk3)))),
% 0.20/0.55 inference(rewrite,[status(thm)],[])).
% 0.20/0.55 tff(36,plain,
% 0.20/0.55 ((in_environment(sk3, sk2(sk3)) | (~stable(sk3)) | (~environment(sk3))) <=> ((~stable(sk3)) | (~environment(sk3)) | in_environment(sk3, sk2(sk3)))),
% 0.20/0.55 inference(rewrite,[status(thm)],[])).
% 0.20/0.55 tff(37,plain,
% 0.20/0.55 (((~![A: $i] : (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A)))) | (in_environment(sk3, sk2(sk3)) | (~stable(sk3)) | (~environment(sk3)))) <=> ((~![A: $i] : (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A)))) | ((~stable(sk3)) | (~environment(sk3)) | in_environment(sk3, sk2(sk3))))),
% 0.20/0.55 inference(monotonicity,[status(thm)],[36])).
% 0.20/0.55 tff(38,plain,
% 0.20/0.55 (((~![A: $i] : (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A)))) | (in_environment(sk3, sk2(sk3)) | (~stable(sk3)) | (~environment(sk3)))) <=> ((~![A: $i] : (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A)))) | (~stable(sk3)) | (~environment(sk3)) | in_environment(sk3, sk2(sk3)))),
% 0.20/0.55 inference(transitivity,[status(thm)],[37, 35])).
% 0.20/0.55 tff(39,plain,
% 0.20/0.55 ((~![A: $i] : (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A)))) | (in_environment(sk3, sk2(sk3)) | (~stable(sk3)) | (~environment(sk3)))),
% 0.20/0.55 inference(quant_inst,[status(thm)],[])).
% 0.20/0.55 tff(40,plain,
% 0.20/0.55 ((~![A: $i] : (in_environment(A, sk2(A)) | (~stable(A)) | (~environment(A)))) | (~stable(sk3)) | (~environment(sk3)) | in_environment(sk3, sk2(sk3))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[39, 38])).
% 0.20/0.55 tff(41,plain,
% 0.20/0.55 (in_environment(sk3, sk2(sk3))),
% 0.20/0.55 inference(unit_resolution,[status(thm)],[40, 34, 24, 21])).
% 0.20/0.55 tff(42,plain,
% 0.20/0.55 (^[A: $i] : refl(((~in_environment(sk3, A)) | greater_or_equal(sk4(A), A)) <=> ((~in_environment(sk3, A)) | greater_or_equal(sk4(A), A)))),
% 0.20/0.55 inference(bind,[status(th)],[])).
% 0.20/0.55 tff(43,plain,
% 0.20/0.55 (![A: $i] : ((~in_environment(sk3, A)) | greater_or_equal(sk4(A), A)) <=> ![A: $i] : ((~in_environment(sk3, A)) | greater_or_equal(sk4(A), A))),
% 0.20/0.55 inference(quant_intro,[status(thm)],[42])).
% 0.20/0.55 tff(44,plain,
% 0.20/0.55 (![A: $i] : ((~in_environment(sk3, A)) | greater_or_equal(sk4(A), A)) <=> ![A: $i] : ((~in_environment(sk3, A)) | greater_or_equal(sk4(A), A))),
% 0.20/0.55 inference(rewrite,[status(thm)],[])).
% 0.20/0.55 tff(45,axiom,(![A: $i] : ((~in_environment(sk3, A)) | greater_or_equal(sk4(A), A))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove_t4_45')).
% 0.20/0.55 tff(46,plain,
% 0.20/0.55 (![A: $i] : ((~in_environment(sk3, A)) | greater_or_equal(sk4(A), A))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[45, 44])).
% 0.20/0.55 tff(47,plain,(
% 0.20/0.55 ![A: $i] : ((~in_environment(sk3, A)) | greater_or_equal(sk4(A), A))),
% 0.20/0.55 inference(skolemize,[status(sab)],[46])).
% 0.20/0.55 tff(48,plain,
% 0.20/0.55 (![A: $i] : ((~in_environment(sk3, A)) | greater_or_equal(sk4(A), A))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[47, 43])).
% 0.20/0.55 tff(49,plain,
% 0.20/0.55 (((~![A: $i] : ((~in_environment(sk3, A)) | greater_or_equal(sk4(A), A))) | ((~in_environment(sk3, sk2(sk3))) | greater_or_equal(sk4(sk2(sk3)), sk2(sk3)))) <=> ((~![A: $i] : ((~in_environment(sk3, A)) | greater_or_equal(sk4(A), A))) | (~in_environment(sk3, sk2(sk3))) | greater_or_equal(sk4(sk2(sk3)), sk2(sk3)))),
% 0.20/0.55 inference(rewrite,[status(thm)],[])).
% 0.20/0.55 tff(50,plain,
% 0.20/0.55 ((~![A: $i] : ((~in_environment(sk3, A)) | greater_or_equal(sk4(A), A))) | ((~in_environment(sk3, sk2(sk3))) | greater_or_equal(sk4(sk2(sk3)), sk2(sk3)))),
% 0.20/0.55 inference(quant_inst,[status(thm)],[])).
% 0.20/0.55 tff(51,plain,
% 0.20/0.55 ((~![A: $i] : ((~in_environment(sk3, A)) | greater_or_equal(sk4(A), A))) | (~in_environment(sk3, sk2(sk3))) | greater_or_equal(sk4(sk2(sk3)), sk2(sk3))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[50, 49])).
% 0.20/0.55 tff(52,plain,
% 0.20/0.55 (greater_or_equal(sk4(sk2(sk3)), sk2(sk3))),
% 0.20/0.55 inference(unit_resolution,[status(thm)],[51, 48, 41])).
% 0.20/0.55 tff(53,plain,
% 0.20/0.55 ($false),
% 0.20/0.55 inference(unit_resolution,[status(thm)],[52, 18])).
% 0.20/0.55 tff(54,plain,((~(sk2(sk3) = equilibrium(sk3))) | greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.55 tff(55,plain,
% 0.20/0.55 (~(sk2(sk3) = equilibrium(sk3))),
% 0.20/0.55 inference(unit_resolution,[status(thm)],[54, 1])).
% 0.20/0.55 tff(56,plain,
% 0.20/0.55 (^[A: $i] : refl(((~stable(A)) | (~environment(A)) | greater_or_equal(sk2(A), equilibrium(A))) <=> ((~stable(A)) | (~environment(A)) | greater_or_equal(sk2(A), equilibrium(A))))),
% 0.20/0.55 inference(bind,[status(th)],[])).
% 0.20/0.55 tff(57,plain,
% 0.20/0.55 (![A: $i] : ((~stable(A)) | (~environment(A)) | greater_or_equal(sk2(A), equilibrium(A))) <=> ![A: $i] : ((~stable(A)) | (~environment(A)) | greater_or_equal(sk2(A), equilibrium(A)))),
% 0.20/0.55 inference(quant_intro,[status(thm)],[56])).
% 0.20/0.55 tff(58,plain,
% 0.20/0.55 (![A: $i] : ((~stable(A)) | (~environment(A)) | greater_or_equal(sk2(A), equilibrium(A))) <=> ![A: $i] : ((~stable(A)) | (~environment(A)) | greater_or_equal(sk2(A), equilibrium(A)))),
% 0.20/0.55 inference(rewrite,[status(thm)],[])).
% 0.20/0.55 tff(59,plain,
% 0.20/0.55 (^[A: $i] : rewrite((((~environment(A)) | (~stable(A))) | greater_or_equal(sk2(A), equilibrium(A))) <=> ((~stable(A)) | (~environment(A)) | greater_or_equal(sk2(A), equilibrium(A))))),
% 0.20/0.55 inference(bind,[status(th)],[])).
% 0.20/0.55 tff(60,plain,
% 0.20/0.55 (![A: $i] : (((~environment(A)) | (~stable(A))) | greater_or_equal(sk2(A), equilibrium(A))) <=> ![A: $i] : ((~stable(A)) | (~environment(A)) | greater_or_equal(sk2(A), equilibrium(A)))),
% 0.20/0.55 inference(quant_intro,[status(thm)],[59])).
% 0.20/0.55 tff(61,axiom,(![A: $i] : (((~environment(A)) | (~stable(A))) | greater_or_equal(sk2(A), equilibrium(A)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','a4_41')).
% 0.20/0.55 tff(62,plain,
% 0.20/0.55 (![A: $i] : ((~stable(A)) | (~environment(A)) | greater_or_equal(sk2(A), equilibrium(A)))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[61, 60])).
% 0.20/0.55 tff(63,plain,
% 0.20/0.55 (![A: $i] : ((~stable(A)) | (~environment(A)) | greater_or_equal(sk2(A), equilibrium(A)))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[62, 58])).
% 0.20/0.55 tff(64,plain,(
% 0.20/0.55 ![A: $i] : ((~stable(A)) | (~environment(A)) | greater_or_equal(sk2(A), equilibrium(A)))),
% 0.20/0.55 inference(skolemize,[status(sab)],[63])).
% 0.20/0.55 tff(65,plain,
% 0.20/0.55 (![A: $i] : ((~stable(A)) | (~environment(A)) | greater_or_equal(sk2(A), equilibrium(A)))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[64, 57])).
% 0.20/0.55 tff(66,plain,
% 0.20/0.55 (((~![A: $i] : ((~stable(A)) | (~environment(A)) | greater_or_equal(sk2(A), equilibrium(A)))) | ((~stable(sk3)) | (~environment(sk3)) | greater_or_equal(sk2(sk3), equilibrium(sk3)))) <=> ((~![A: $i] : ((~stable(A)) | (~environment(A)) | greater_or_equal(sk2(A), equilibrium(A)))) | (~stable(sk3)) | (~environment(sk3)) | greater_or_equal(sk2(sk3), equilibrium(sk3)))),
% 0.20/0.55 inference(rewrite,[status(thm)],[])).
% 0.20/0.55 tff(67,plain,
% 0.20/0.55 ((~![A: $i] : ((~stable(A)) | (~environment(A)) | greater_or_equal(sk2(A), equilibrium(A)))) | ((~stable(sk3)) | (~environment(sk3)) | greater_or_equal(sk2(sk3), equilibrium(sk3)))),
% 0.20/0.55 inference(quant_inst,[status(thm)],[])).
% 0.20/0.55 tff(68,plain,
% 0.20/0.55 ((~![A: $i] : ((~stable(A)) | (~environment(A)) | greater_or_equal(sk2(A), equilibrium(A)))) | (~stable(sk3)) | (~environment(sk3)) | greater_or_equal(sk2(sk3), equilibrium(sk3))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[67, 66])).
% 0.20/0.55 tff(69,plain,
% 0.20/0.55 (greater_or_equal(sk2(sk3), equilibrium(sk3))),
% 0.20/0.55 inference(unit_resolution,[status(thm)],[68, 65, 24, 21])).
% 0.20/0.55 tff(70,plain,
% 0.20/0.55 (^[B: $i, A: $i] : refl(((A = B) | greater(A, B) | (~greater_or_equal(A, B))) <=> ((A = B) | greater(A, B) | (~greater_or_equal(A, B))))),
% 0.20/0.55 inference(bind,[status(th)],[])).
% 0.20/0.55 tff(71,plain,
% 0.20/0.55 (![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B))) <=> ![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))),
% 0.20/0.55 inference(quant_intro,[status(thm)],[70])).
% 0.20/0.55 tff(72,plain,
% 0.20/0.55 (![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B))) <=> ![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))),
% 0.20/0.55 inference(rewrite,[status(thm)],[])).
% 0.20/0.55 tff(73,plain,
% 0.20/0.55 (^[B: $i, A: $i] : rewrite((((~greater_or_equal(A, B)) | greater(A, B)) | (A = B)) <=> ((A = B) | greater(A, B) | (~greater_or_equal(A, B))))),
% 0.20/0.55 inference(bind,[status(th)],[])).
% 0.20/0.55 tff(74,plain,
% 0.20/0.55 (![B: $i, A: $i] : (((~greater_or_equal(A, B)) | greater(A, B)) | (A = B)) <=> ![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))),
% 0.20/0.55 inference(quant_intro,[status(thm)],[73])).
% 0.20/0.55 tff(75,axiom,(![B: $i, A: $i] : (((~greater_or_equal(A, B)) | greater(A, B)) | (A = B))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp_greater_or_equal_24')).
% 0.20/0.55 tff(76,plain,
% 0.20/0.55 (![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[75, 74])).
% 0.20/0.55 tff(77,plain,
% 0.20/0.55 (![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[76, 72])).
% 0.20/0.55 tff(78,plain,(
% 0.20/0.55 ![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))),
% 0.20/0.55 inference(skolemize,[status(sab)],[77])).
% 0.20/0.55 tff(79,plain,
% 0.20/0.55 (![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[78, 71])).
% 0.20/0.55 tff(80,plain,
% 0.20/0.55 (((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((~greater_or_equal(sk2(sk3), equilibrium(sk3))) | (sk2(sk3) = equilibrium(sk3)) | greater(sk2(sk3), equilibrium(sk3)))) <=> ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | (~greater_or_equal(sk2(sk3), equilibrium(sk3))) | (sk2(sk3) = equilibrium(sk3)) | greater(sk2(sk3), equilibrium(sk3)))),
% 0.20/0.55 inference(rewrite,[status(thm)],[])).
% 0.20/0.55 tff(81,plain,
% 0.20/0.55 (((sk2(sk3) = equilibrium(sk3)) | greater(sk2(sk3), equilibrium(sk3)) | (~greater_or_equal(sk2(sk3), equilibrium(sk3)))) <=> ((~greater_or_equal(sk2(sk3), equilibrium(sk3))) | (sk2(sk3) = equilibrium(sk3)) | greater(sk2(sk3), equilibrium(sk3)))),
% 0.20/0.55 inference(rewrite,[status(thm)],[])).
% 0.20/0.55 tff(82,plain,
% 0.20/0.55 (((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((sk2(sk3) = equilibrium(sk3)) | greater(sk2(sk3), equilibrium(sk3)) | (~greater_or_equal(sk2(sk3), equilibrium(sk3))))) <=> ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((~greater_or_equal(sk2(sk3), equilibrium(sk3))) | (sk2(sk3) = equilibrium(sk3)) | greater(sk2(sk3), equilibrium(sk3))))),
% 0.20/0.55 inference(monotonicity,[status(thm)],[81])).
% 0.20/0.55 tff(83,plain,
% 0.20/0.55 (((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((sk2(sk3) = equilibrium(sk3)) | greater(sk2(sk3), equilibrium(sk3)) | (~greater_or_equal(sk2(sk3), equilibrium(sk3))))) <=> ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | (~greater_or_equal(sk2(sk3), equilibrium(sk3))) | (sk2(sk3) = equilibrium(sk3)) | greater(sk2(sk3), equilibrium(sk3)))),
% 0.20/0.55 inference(transitivity,[status(thm)],[82, 80])).
% 0.20/0.55 tff(84,plain,
% 0.20/0.55 ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((sk2(sk3) = equilibrium(sk3)) | greater(sk2(sk3), equilibrium(sk3)) | (~greater_or_equal(sk2(sk3), equilibrium(sk3))))),
% 0.20/0.55 inference(quant_inst,[status(thm)],[])).
% 0.20/0.55 tff(85,plain,
% 0.20/0.55 ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | (~greater_or_equal(sk2(sk3), equilibrium(sk3))) | (sk2(sk3) = equilibrium(sk3)) | greater(sk2(sk3), equilibrium(sk3))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[84, 83])).
% 0.20/0.55 tff(86,plain,
% 0.20/0.55 ((sk2(sk3) = equilibrium(sk3)) | greater(sk2(sk3), equilibrium(sk3))),
% 0.20/0.55 inference(unit_resolution,[status(thm)],[85, 79, 69])).
% 0.20/0.55 tff(87,plain,
% 0.20/0.55 (greater(sk2(sk3), equilibrium(sk3))),
% 0.20/0.55 inference(unit_resolution,[status(thm)],[86, 55])).
% 0.20/0.55 tff(88,plain,
% 0.20/0.55 (![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B))) <=> ![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))),
% 0.20/0.55 inference(rewrite,[status(thm)],[])).
% 0.20/0.55 tff(89,plain,
% 0.20/0.55 (![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B))) <=> ![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))),
% 0.20/0.55 inference(rewrite,[status(thm)],[])).
% 0.20/0.55 tff(90,plain,
% 0.20/0.55 (^[B: $i, A: $i, C: $i] : rewrite((((~greater(A, B)) | (~greater(B, C))) | greater(A, C)) <=> (greater(A, C) | (~greater(B, C)) | (~greater(A, B))))),
% 0.20/0.55 inference(bind,[status(th)],[])).
% 0.20/0.55 tff(91,plain,
% 0.20/0.55 (![B: $i, A: $i, C: $i] : (((~greater(A, B)) | (~greater(B, C))) | greater(A, C)) <=> ![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))),
% 0.20/0.55 inference(quant_intro,[status(thm)],[90])).
% 0.20/0.55 tff(92,axiom,(![B: $i, A: $i, C: $i] : (((~greater(A, B)) | (~greater(B, C))) | greater(A, C))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp_greater_transitivity_22')).
% 0.20/0.55 tff(93,plain,
% 0.20/0.55 (![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[92, 91])).
% 0.20/0.55 tff(94,plain,
% 0.20/0.55 (![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[93, 89])).
% 0.20/0.55 tff(95,plain,(
% 0.20/0.55 ![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))),
% 0.20/0.55 inference(skolemize,[status(sab)],[94])).
% 0.20/0.55 tff(96,plain,
% 0.20/0.55 (![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))),
% 0.20/0.55 inference(modus_ponens,[status(thm)],[95, 88])).
% 0.20/0.55 tff(97,plain,
% 0.20/0.55 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(sk4(sk2(sk3)), equilibrium(sk3)) | (~greater(sk2(sk3), equilibrium(sk3))) | (~greater(sk4(sk2(sk3)), sk2(sk3))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(sk4(sk2(sk3)), equilibrium(sk3)) | (~greater(sk2(sk3), equilibrium(sk3))) | (~greater(sk4(sk2(sk3)), sk2(sk3))))),
% 0.20/0.55 inference(rewrite,[status(thm)],[])).
% 0.20/0.55 tff(98,plain,
% 0.20/0.55 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(sk4(sk2(sk3)), equilibrium(sk3)) | (~greater(sk2(sk3), equilibrium(sk3))) | (~greater(sk4(sk2(sk3)), sk2(sk3))))),
% 0.30/0.55 inference(quant_inst,[status(thm)],[])).
% 0.30/0.55 tff(99,plain,
% 0.30/0.55 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(sk4(sk2(sk3)), equilibrium(sk3)) | (~greater(sk2(sk3), equilibrium(sk3))) | (~greater(sk4(sk2(sk3)), sk2(sk3)))),
% 0.30/0.55 inference(modus_ponens,[status(thm)],[98, 97])).
% 0.30/0.55 tff(100,plain,
% 0.30/0.55 ($false),
% 0.30/0.55 inference(unit_resolution,[status(thm)],[99, 96, 87, 13, 12])).
% 0.30/0.55 tff(101,plain,(greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3)) | (~greater(sk4(sk2(sk3)), sk2(sk3)))), inference(lemma,lemma(discharge,[]))).
% 0.30/0.55 tff(102,plain,
% 0.30/0.55 (~greater(sk4(sk2(sk3)), sk2(sk3))),
% 0.30/0.55 inference(unit_resolution,[status(thm)],[101, 1])).
% 0.30/0.55 tff(103,plain,
% 0.30/0.55 (((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((sk4(sk2(sk3)) = sk2(sk3)) | greater(sk4(sk2(sk3)), sk2(sk3)) | (~greater_or_equal(sk4(sk2(sk3)), sk2(sk3))))) <=> ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | (sk4(sk2(sk3)) = sk2(sk3)) | greater(sk4(sk2(sk3)), sk2(sk3)) | (~greater_or_equal(sk4(sk2(sk3)), sk2(sk3))))),
% 0.30/0.55 inference(rewrite,[status(thm)],[])).
% 0.30/0.55 tff(104,plain,
% 0.30/0.55 ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((sk4(sk2(sk3)) = sk2(sk3)) | greater(sk4(sk2(sk3)), sk2(sk3)) | (~greater_or_equal(sk4(sk2(sk3)), sk2(sk3))))),
% 0.30/0.55 inference(quant_inst,[status(thm)],[])).
% 0.30/0.55 tff(105,plain,
% 0.30/0.55 ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | (sk4(sk2(sk3)) = sk2(sk3)) | greater(sk4(sk2(sk3)), sk2(sk3)) | (~greater_or_equal(sk4(sk2(sk3)), sk2(sk3)))),
% 0.30/0.55 inference(modus_ponens,[status(thm)],[104, 103])).
% 0.30/0.55 tff(106,plain,
% 0.30/0.55 ((sk4(sk2(sk3)) = sk2(sk3)) | greater(sk4(sk2(sk3)), sk2(sk3))),
% 0.30/0.55 inference(unit_resolution,[status(thm)],[105, 79, 52])).
% 0.30/0.55 tff(107,plain,
% 0.30/0.55 (sk4(sk2(sk3)) = sk2(sk3)),
% 0.30/0.55 inference(unit_resolution,[status(thm)],[106, 102])).
% 0.30/0.55 tff(108,plain,
% 0.30/0.55 (greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3)) <=> greater_or_equal(sk2(sk3), equilibrium(sk3))),
% 0.30/0.55 inference(monotonicity,[status(thm)],[107])).
% 0.30/0.55 tff(109,plain,
% 0.30/0.55 (greater_or_equal(sk2(sk3), equilibrium(sk3)) <=> greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))),
% 0.30/0.55 inference(symmetry,[status(thm)],[108])).
% 0.30/0.55 tff(110,plain,
% 0.30/0.55 (greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))),
% 0.30/0.55 inference(modus_ponens,[status(thm)],[69, 109])).
% 0.30/0.55 tff(111,plain,
% 0.30/0.55 ($false),
% 0.30/0.55 inference(unit_resolution,[status(thm)],[1, 110])).
% 0.30/0.55 tff(112,plain,(greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))), inference(lemma,lemma(discharge,[]))).
% 0.30/0.55 tff(113,assumption,(greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))), introduced(assumption)).
% 0.30/0.55 tff(114,assumption,(greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))), introduced(assumption)).
% 0.30/0.55 tff(115,assumption,(~(growth_rate(first_movers, sk4(sk2(sk3))) = zero)), introduced(assumption)).
% 0.30/0.55 tff(116,assumption,(~greater(zero, growth_rate(first_movers, sk4(sk2(sk3))))), introduced(assumption)).
% 0.30/0.55 tff(117,plain,
% 0.30/0.55 (^[A: $i] : refl(((~in_environment(sk3, A)) | subpopulations(first_movers, efficient_producers, sk3, sk4(A))) <=> ((~in_environment(sk3, A)) | subpopulations(first_movers, efficient_producers, sk3, sk4(A))))),
% 0.30/0.55 inference(bind,[status(th)],[])).
% 0.30/0.55 tff(118,plain,
% 0.30/0.55 (![A: $i] : ((~in_environment(sk3, A)) | subpopulations(first_movers, efficient_producers, sk3, sk4(A))) <=> ![A: $i] : ((~in_environment(sk3, A)) | subpopulations(first_movers, efficient_producers, sk3, sk4(A)))),
% 0.30/0.55 inference(quant_intro,[status(thm)],[117])).
% 0.30/0.55 tff(119,plain,
% 0.30/0.55 (![A: $i] : ((~in_environment(sk3, A)) | subpopulations(first_movers, efficient_producers, sk3, sk4(A))) <=> ![A: $i] : ((~in_environment(sk3, A)) | subpopulations(first_movers, efficient_producers, sk3, sk4(A)))),
% 0.30/0.55 inference(rewrite,[status(thm)],[])).
% 0.30/0.55 tff(120,axiom,(![A: $i] : ((~in_environment(sk3, A)) | subpopulations(first_movers, efficient_producers, sk3, sk4(A)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove_t4_44')).
% 0.30/0.55 tff(121,plain,
% 0.30/0.55 (![A: $i] : ((~in_environment(sk3, A)) | subpopulations(first_movers, efficient_producers, sk3, sk4(A)))),
% 0.30/0.56 inference(modus_ponens,[status(thm)],[120, 119])).
% 0.30/0.56 tff(122,plain,(
% 0.30/0.56 ![A: $i] : ((~in_environment(sk3, A)) | subpopulations(first_movers, efficient_producers, sk3, sk4(A)))),
% 0.30/0.56 inference(skolemize,[status(sab)],[121])).
% 0.30/0.56 tff(123,plain,
% 0.30/0.56 (![A: $i] : ((~in_environment(sk3, A)) | subpopulations(first_movers, efficient_producers, sk3, sk4(A)))),
% 0.30/0.56 inference(modus_ponens,[status(thm)],[122, 118])).
% 0.30/0.56 tff(124,plain,
% 0.30/0.56 (((~![A: $i] : ((~in_environment(sk3, A)) | subpopulations(first_movers, efficient_producers, sk3, sk4(A)))) | ((~in_environment(sk3, sk2(sk3))) | subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3))))) <=> ((~![A: $i] : ((~in_environment(sk3, A)) | subpopulations(first_movers, efficient_producers, sk3, sk4(A)))) | (~in_environment(sk3, sk2(sk3))) | subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3))))),
% 0.30/0.56 inference(rewrite,[status(thm)],[])).
% 0.30/0.56 tff(125,plain,
% 0.30/0.56 ((~![A: $i] : ((~in_environment(sk3, A)) | subpopulations(first_movers, efficient_producers, sk3, sk4(A)))) | ((~in_environment(sk3, sk2(sk3))) | subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3))))),
% 0.30/0.56 inference(quant_inst,[status(thm)],[])).
% 0.30/0.56 tff(126,plain,
% 0.30/0.56 ((~![A: $i] : ((~in_environment(sk3, A)) | subpopulations(first_movers, efficient_producers, sk3, sk4(A)))) | (~in_environment(sk3, sk2(sk3))) | subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))),
% 0.30/0.56 inference(modus_ponens,[status(thm)],[125, 124])).
% 0.30/0.56 tff(127,plain,
% 0.30/0.56 (subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))),
% 0.30/0.56 inference(unit_resolution,[status(thm)],[126, 123, 41])).
% 0.30/0.56 tff(128,plain,
% 0.30/0.56 (^[B: $i, A: $i] : refl((greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B))) <=> (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B))))),
% 0.30/0.56 inference(bind,[status(th)],[])).
% 0.30/0.56 tff(129,plain,
% 0.30/0.56 (![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B))) <=> ![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))),
% 0.30/0.56 inference(quant_intro,[status(thm)],[128])).
% 0.30/0.56 tff(130,plain,
% 0.30/0.56 (![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B))) <=> ![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))),
% 0.30/0.56 inference(rewrite,[status(thm)],[])).
% 0.30/0.56 tff(131,plain,
% 0.30/0.56 (^[B: $i, A: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) <=> ((~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))), (((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) <=> (((~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | (growth_rate(first_movers, B) = zero)))), rewrite((((~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | (growth_rate(first_movers, B) = zero)) <=> ((growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))), (((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) <=> ((growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))))), ((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) | greater(zero, growth_rate(efficient_producers, B))) <=> (((growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | greater(zero, growth_rate(efficient_producers, B))))), rewrite((((growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | greater(zero, growth_rate(efficient_producers, B))) <=> ((growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))), ((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) | greater(zero, growth_rate(efficient_producers, B))) <=> ((growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B))))), (((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) | greater(zero, growth_rate(efficient_producers, B))) | greater(zero, growth_rate(first_movers, B))) <=> (((growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B))) | greater(zero, growth_rate(first_movers, B))))), rewrite((((growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B))) | greater(zero, growth_rate(first_movers, B))) <=> (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))), (((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) | greater(zero, growth_rate(efficient_producers, B))) | greater(zero, growth_rate(first_movers, B))) <=> (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))))),
% 0.30/0.56 inference(bind,[status(th)],[])).
% 0.30/0.56 tff(132,plain,
% 0.30/0.56 (![B: $i, A: $i] : ((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) | greater(zero, growth_rate(efficient_producers, B))) | greater(zero, growth_rate(first_movers, B))) <=> ![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))),
% 0.30/0.56 inference(quant_intro,[status(thm)],[131])).
% 0.30/0.56 tff(133,axiom,(![B: $i, A: $i] : ((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) | greater(zero, growth_rate(efficient_producers, B))) | greater(zero, growth_rate(first_movers, B)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','l6_33')).
% 0.30/0.56 tff(134,plain,
% 0.30/0.56 (![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))),
% 0.30/0.56 inference(modus_ponens,[status(thm)],[133, 132])).
% 0.30/0.56 tff(135,plain,
% 0.30/0.56 (![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))),
% 0.30/0.56 inference(modus_ponens,[status(thm)],[134, 130])).
% 0.30/0.56 tff(136,plain,(
% 0.30/0.56 ![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))),
% 0.30/0.56 inference(skolemize,[status(sab)],[135])).
% 0.30/0.56 tff(137,plain,
% 0.30/0.56 (![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))),
% 0.30/0.56 inference(modus_ponens,[status(thm)],[136, 129])).
% 0.30/0.56 tff(138,plain,
% 0.30/0.56 (((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))) | ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3)))) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero))) <=> ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3)))) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero))),
% 0.30/0.56 inference(rewrite,[status(thm)],[])).
% 0.30/0.56 tff(139,plain,
% 0.30/0.56 ((greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3)) | greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3))))) <=> ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3)))) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero))),
% 0.30/0.56 inference(rewrite,[status(thm)],[])).
% 0.30/0.56 tff(140,plain,
% 0.30/0.56 (((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))) | (greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3)) | greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3)))))) <=> ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))) | ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3)))) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero)))),
% 0.30/0.56 inference(monotonicity,[status(thm)],[139])).
% 0.30/0.56 tff(141,plain,
% 0.30/0.56 (((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))) | (greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3)) | greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3)))))) <=> ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3)))) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero))),
% 0.30/0.56 inference(transitivity,[status(thm)],[140, 138])).
% 0.30/0.56 tff(142,plain,
% 0.30/0.56 ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))) | (greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3)) | greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3)))))),
% 0.30/0.56 inference(quant_inst,[status(thm)],[])).
% 0.30/0.56 tff(143,plain,
% 0.30/0.56 ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3)))) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero)),
% 0.30/0.56 inference(modus_ponens,[status(thm)],[142, 141])).
% 0.30/0.56 tff(144,plain,
% 0.30/0.56 (greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3)))) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero)),
% 0.30/0.57 inference(unit_resolution,[status(thm)],[143, 137, 24, 127])).
% 0.30/0.57 tff(145,plain,
% 0.30/0.57 (greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3))))),
% 0.30/0.57 inference(unit_resolution,[status(thm)],[144, 116, 113, 115])).
% 0.30/0.57 tff(146,plain,
% 0.30/0.57 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3))))) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3))))) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))))),
% 0.30/0.57 inference(rewrite,[status(thm)],[])).
% 0.30/0.57 tff(147,plain,
% 0.30/0.57 ((greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))) | (~greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3)))))) <=> (greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3))))) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))))),
% 0.30/0.57 inference(rewrite,[status(thm)],[])).
% 0.30/0.57 tff(148,plain,
% 0.30/0.57 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))) | (~greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3))))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3))))) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))))))),
% 0.30/0.57 inference(monotonicity,[status(thm)],[147])).
% 0.30/0.57 tff(149,plain,
% 0.30/0.57 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))) | (~greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3))))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3))))) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))))),
% 0.30/0.57 inference(transitivity,[status(thm)],[148, 146])).
% 0.30/0.57 tff(150,plain,
% 0.30/0.57 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))) | (~greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3))))))),
% 0.30/0.57 inference(quant_inst,[status(thm)],[])).
% 0.30/0.57 tff(151,plain,
% 0.30/0.57 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater(zero, growth_rate(efficient_producers, sk4(sk2(sk3))))) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))))),
% 0.30/0.57 inference(modus_ponens,[status(thm)],[150, 149])).
% 0.30/0.57 tff(152,plain,
% 0.30/0.57 ($false),
% 0.30/0.57 inference(unit_resolution,[status(thm)],[151, 96, 114, 116, 145])).
% 0.30/0.57 tff(153,plain,(greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero)), inference(lemma,lemma(discharge,[]))).
% 0.30/0.57 tff(154,plain,
% 0.30/0.57 (greater(zero, growth_rate(first_movers, sk4(sk2(sk3))))),
% 0.30/0.57 inference(unit_resolution,[status(thm)],[153, 115, 113, 114])).
% 0.30/0.57 tff(155,plain,
% 0.30/0.57 (^[A: $i] : refl(((~in_environment(sk3, A)) | (~outcompetes(efficient_producers, first_movers, sk4(A)))) <=> ((~in_environment(sk3, A)) | (~outcompetes(efficient_producers, first_movers, sk4(A)))))),
% 0.30/0.57 inference(bind,[status(th)],[])).
% 0.30/0.57 tff(156,plain,
% 0.30/0.57 (![A: $i] : ((~in_environment(sk3, A)) | (~outcompetes(efficient_producers, first_movers, sk4(A)))) <=> ![A: $i] : ((~in_environment(sk3, A)) | (~outcompetes(efficient_producers, first_movers, sk4(A))))),
% 0.30/0.57 inference(quant_intro,[status(thm)],[155])).
% 0.30/0.57 tff(157,plain,
% 0.30/0.57 (![A: $i] : ((~in_environment(sk3, A)) | (~outcompetes(efficient_producers, first_movers, sk4(A)))) <=> ![A: $i] : ((~in_environment(sk3, A)) | (~outcompetes(efficient_producers, first_movers, sk4(A))))),
% 0.30/0.57 inference(rewrite,[status(thm)],[])).
% 0.30/0.57 tff(158,axiom,(![A: $i] : ((~in_environment(sk3, A)) | (~outcompetes(efficient_producers, first_movers, sk4(A))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove_t4_46')).
% 0.30/0.57 tff(159,plain,
% 0.30/0.57 (![A: $i] : ((~in_environment(sk3, A)) | (~outcompetes(efficient_producers, first_movers, sk4(A))))),
% 0.30/0.57 inference(modus_ponens,[status(thm)],[158, 157])).
% 0.30/0.57 tff(160,plain,(
% 0.30/0.57 ![A: $i] : ((~in_environment(sk3, A)) | (~outcompetes(efficient_producers, first_movers, sk4(A))))),
% 0.30/0.57 inference(skolemize,[status(sab)],[159])).
% 0.30/0.57 tff(161,plain,
% 0.30/0.57 (![A: $i] : ((~in_environment(sk3, A)) | (~outcompetes(efficient_producers, first_movers, sk4(A))))),
% 0.30/0.57 inference(modus_ponens,[status(thm)],[160, 156])).
% 0.30/0.57 tff(162,plain,
% 0.30/0.57 (((~![A: $i] : ((~in_environment(sk3, A)) | (~outcompetes(efficient_producers, first_movers, sk4(A))))) | ((~in_environment(sk3, sk2(sk3))) | (~outcompetes(efficient_producers, first_movers, sk4(sk2(sk3)))))) <=> ((~![A: $i] : ((~in_environment(sk3, A)) | (~outcompetes(efficient_producers, first_movers, sk4(A))))) | (~in_environment(sk3, sk2(sk3))) | (~outcompetes(efficient_producers, first_movers, sk4(sk2(sk3)))))),
% 0.30/0.57 inference(rewrite,[status(thm)],[])).
% 0.30/0.57 tff(163,plain,
% 0.30/0.57 ((~![A: $i] : ((~in_environment(sk3, A)) | (~outcompetes(efficient_producers, first_movers, sk4(A))))) | ((~in_environment(sk3, sk2(sk3))) | (~outcompetes(efficient_producers, first_movers, sk4(sk2(sk3)))))),
% 0.30/0.57 inference(quant_inst,[status(thm)],[])).
% 0.30/0.57 tff(164,plain,
% 0.30/0.57 ((~![A: $i] : ((~in_environment(sk3, A)) | (~outcompetes(efficient_producers, first_movers, sk4(A))))) | (~in_environment(sk3, sk2(sk3))) | (~outcompetes(efficient_producers, first_movers, sk4(sk2(sk3))))),
% 0.30/0.57 inference(modus_ponens,[status(thm)],[163, 162])).
% 0.30/0.57 tff(165,plain,
% 0.30/0.57 (~outcompetes(efficient_producers, first_movers, sk4(sk2(sk3)))),
% 0.30/0.57 inference(unit_resolution,[status(thm)],[164, 161, 41])).
% 0.30/0.57 tff(166,plain,
% 0.30/0.57 (^[B: $i, D: $i, A: $i, C: $i] : refl((outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A))) <=> (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A))))),
% 0.30/0.57 inference(bind,[status(th)],[])).
% 0.30/0.57 tff(167,plain,
% 0.30/0.57 (![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A))) <=> ![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))),
% 0.30/0.57 inference(quant_intro,[status(thm)],[166])).
% 0.30/0.57 tff(168,plain,
% 0.30/0.57 (![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A))) <=> ![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))),
% 0.30/0.57 inference(rewrite,[status(thm)],[])).
% 0.30/0.57 tff(169,plain,
% 0.30/0.57 (^[B: $i, D: $i, A: $i, C: $i] : trans(monotonicity(trans(monotonicity(rewrite((((~environment(A)) | (~subpopulations(B, C, A, D))) | (~greater_or_equal(growth_rate(C, D), zero))) <=> ((~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))), (((((~environment(A)) | (~subpopulations(B, C, A, D))) | (~greater_or_equal(growth_rate(C, D), zero))) | (~greater(zero, growth_rate(B, D)))) <=> (((~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A))) | (~greater(zero, growth_rate(B, D)))))), rewrite((((~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A))) | (~greater(zero, growth_rate(B, D)))) <=> ((~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))), (((((~environment(A)) | (~subpopulations(B, C, A, D))) | (~greater_or_equal(growth_rate(C, D), zero))) | (~greater(zero, growth_rate(B, D)))) <=> ((~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A))))), ((((((~environment(A)) | (~subpopulations(B, C, A, D))) | (~greater_or_equal(growth_rate(C, D), zero))) | (~greater(zero, growth_rate(B, D)))) | outcompetes(C, B, D)) <=> (((~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A))) | outcompetes(C, B, D)))), rewrite((((~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A))) | outcompetes(C, B, D)) <=> (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))), ((((((~environment(A)) | (~subpopulations(B, C, A, D))) | (~greater_or_equal(growth_rate(C, D), zero))) | (~greater(zero, growth_rate(B, D)))) | outcompetes(C, B, D)) <=> (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))))),
% 0.30/0.57 inference(bind,[status(th)],[])).
% 0.30/0.57 tff(170,plain,
% 0.30/0.57 (![B: $i, D: $i, A: $i, C: $i] : (((((~environment(A)) | (~subpopulations(B, C, A, D))) | (~greater_or_equal(growth_rate(C, D), zero))) | (~greater(zero, growth_rate(B, D)))) | outcompetes(C, B, D)) <=> ![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))),
% 0.30/0.57 inference(quant_intro,[status(thm)],[169])).
% 0.30/0.57 tff(171,axiom,(![B: $i, D: $i, A: $i, C: $i] : (((((~environment(A)) | (~subpopulations(B, C, A, D))) | (~greater_or_equal(growth_rate(C, D), zero))) | (~greater(zero, growth_rate(B, D)))) | outcompetes(C, B, D))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','d2_27')).
% 0.30/0.57 tff(172,plain,
% 0.30/0.57 (![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))),
% 0.30/0.57 inference(modus_ponens,[status(thm)],[171, 170])).
% 0.30/0.57 tff(173,plain,
% 0.30/0.57 (![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))),
% 0.30/0.57 inference(modus_ponens,[status(thm)],[172, 168])).
% 0.30/0.57 tff(174,plain,(
% 0.30/0.57 ![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))),
% 0.30/0.57 inference(skolemize,[status(sab)],[173])).
% 0.30/0.57 tff(175,plain,
% 0.30/0.57 (![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))),
% 0.30/0.57 inference(modus_ponens,[status(thm)],[174, 167])).
% 0.30/0.57 tff(176,plain,
% 0.30/0.57 (((~![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | ((~environment(sk3)) | outcompetes(efficient_producers, first_movers, sk4(sk2(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~greater(zero, growth_rate(first_movers, sk4(sk2(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)))) <=> ((~![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | (~environment(sk3)) | outcompetes(efficient_producers, first_movers, sk4(sk2(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~greater(zero, growth_rate(first_movers, sk4(sk2(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)))),
% 0.30/0.57 inference(rewrite,[status(thm)],[])).
% 0.30/0.57 tff(177,plain,
% 0.30/0.57 ((outcompetes(efficient_producers, first_movers, sk4(sk2(sk3))) | (~greater(zero, growth_rate(first_movers, sk4(sk2(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3))) <=> ((~environment(sk3)) | outcompetes(efficient_producers, first_movers, sk4(sk2(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~greater(zero, growth_rate(first_movers, sk4(sk2(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)))),
% 0.30/0.57 inference(rewrite,[status(thm)],[])).
% 0.30/0.57 tff(178,plain,
% 0.30/0.57 (((~![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | (outcompetes(efficient_producers, first_movers, sk4(sk2(sk3))) | (~greater(zero, growth_rate(first_movers, sk4(sk2(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3)))) <=> ((~![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | ((~environment(sk3)) | outcompetes(efficient_producers, first_movers, sk4(sk2(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~greater(zero, growth_rate(first_movers, sk4(sk2(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), zero))))),
% 0.30/0.57 inference(monotonicity,[status(thm)],[177])).
% 0.30/0.57 tff(179,plain,
% 0.30/0.57 (((~![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | (outcompetes(efficient_producers, first_movers, sk4(sk2(sk3))) | (~greater(zero, growth_rate(first_movers, sk4(sk2(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3)))) <=> ((~![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | (~environment(sk3)) | outcompetes(efficient_producers, first_movers, sk4(sk2(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~greater(zero, growth_rate(first_movers, sk4(sk2(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)))),
% 0.30/0.57 inference(transitivity,[status(thm)],[178, 176])).
% 0.30/0.57 tff(180,plain,
% 0.30/0.57 ((~![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | (outcompetes(efficient_producers, first_movers, sk4(sk2(sk3))) | (~greater(zero, growth_rate(first_movers, sk4(sk2(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3)))),
% 0.30/0.58 inference(quant_inst,[status(thm)],[])).
% 0.30/0.58 tff(181,plain,
% 0.30/0.58 ((~![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | (~environment(sk3)) | outcompetes(efficient_producers, first_movers, sk4(sk2(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~greater(zero, growth_rate(first_movers, sk4(sk2(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), zero))),
% 0.30/0.58 inference(modus_ponens,[status(thm)],[180, 179])).
% 0.30/0.58 tff(182,plain,
% 0.30/0.58 ((~greater(zero, growth_rate(first_movers, sk4(sk2(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), zero))),
% 0.30/0.58 inference(unit_resolution,[status(thm)],[181, 175, 24, 165, 127])).
% 0.30/0.58 tff(183,plain,
% 0.30/0.58 (~greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)),
% 0.30/0.58 inference(unit_resolution,[status(thm)],[182, 154])).
% 0.30/0.58 tff(184,plain,
% 0.30/0.58 (((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | ((~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)) | greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), zero))) <=> ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)) | greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), zero))),
% 0.30/0.58 inference(rewrite,[status(thm)],[])).
% 0.30/0.58 tff(185,plain,
% 0.30/0.58 ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | ((~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)) | greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), zero))),
% 0.30/0.58 inference(quant_inst,[status(thm)],[])).
% 0.30/0.58 tff(186,plain,
% 0.30/0.58 ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)) | greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)),
% 0.30/0.58 inference(modus_ponens,[status(thm)],[185, 184])).
% 0.30/0.58 tff(187,plain,
% 0.30/0.58 (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)),
% 0.30/0.58 inference(unit_resolution,[status(thm)],[186, 8, 183])).
% 0.30/0.58 tff(188,plain,
% 0.30/0.58 (^[B: $i, A: $i] : refl((greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) <=> (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))))),
% 0.30/0.58 inference(bind,[status(th)],[])).
% 0.30/0.58 tff(189,plain,
% 0.30/0.58 (![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) <=> ![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))),
% 0.30/0.58 inference(quant_intro,[status(thm)],[188])).
% 0.30/0.58 tff(190,plain,
% 0.30/0.58 (![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) <=> ![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))),
% 0.30/0.58 inference(rewrite,[status(thm)],[])).
% 0.30/0.58 tff(191,plain,
% 0.30/0.58 (^[B: $i, A: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) <=> ((~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))), (((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) <=> (((~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | (growth_rate(first_movers, B) = zero)))), rewrite((((~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | (growth_rate(first_movers, B) = zero)) <=> ((growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))), (((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) <=> ((growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))))), ((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) <=> (((growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | greater(growth_rate(first_movers, B), zero)))), rewrite((((growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | greater(growth_rate(first_movers, B), zero)) <=> (greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))), ((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) <=> (greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))))), (((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) | greater(growth_rate(efficient_producers, B), zero)) <=> ((greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | greater(growth_rate(efficient_producers, B), zero)))), rewrite(((greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | greater(growth_rate(efficient_producers, B), zero)) <=> (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))), (((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) | greater(growth_rate(efficient_producers, B), zero)) <=> (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))))),
% 0.30/0.58 inference(bind,[status(th)],[])).
% 0.30/0.58 tff(192,plain,
% 0.30/0.58 (![B: $i, A: $i] : ((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) | greater(growth_rate(efficient_producers, B), zero)) <=> ![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))),
% 0.30/0.58 inference(quant_intro,[status(thm)],[191])).
% 0.30/0.58 tff(193,axiom,(![B: $i, A: $i] : ((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) | greater(growth_rate(efficient_producers, B), zero))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','l6_30')).
% 0.30/0.58 tff(194,plain,
% 0.30/0.58 (![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))),
% 0.30/0.58 inference(modus_ponens,[status(thm)],[193, 192])).
% 0.30/0.58 tff(195,plain,
% 0.30/0.58 (![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))),
% 0.30/0.58 inference(modus_ponens,[status(thm)],[194, 190])).
% 0.30/0.58 tff(196,plain,(
% 0.30/0.58 ![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))),
% 0.30/0.58 inference(skolemize,[status(sab)],[195])).
% 0.30/0.58 tff(197,plain,
% 0.30/0.58 (![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))),
% 0.30/0.58 inference(modus_ponens,[status(thm)],[196, 189])).
% 0.30/0.58 tff(198,plain,
% 0.30/0.58 (((~![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero))) <=> ((~![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero))),
% 0.30/0.58 inference(rewrite,[status(thm)],[])).
% 0.30/0.58 tff(199,plain,
% 0.30/0.58 ((greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3))) <=> ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero))),
% 0.30/0.58 inference(rewrite,[status(thm)],[])).
% 0.30/0.58 tff(200,plain,
% 0.30/0.58 (((~![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | (greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3)))) <=> ((~![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero)))),
% 0.30/0.58 inference(monotonicity,[status(thm)],[199])).
% 0.30/0.58 tff(201,plain,
% 0.30/0.58 (((~![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | (greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3)))) <=> ((~![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero))),
% 0.30/0.58 inference(transitivity,[status(thm)],[200, 198])).
% 0.30/0.58 tff(202,plain,
% 0.30/0.58 ((~![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | (greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3)))),
% 0.30/0.58 inference(quant_inst,[status(thm)],[])).
% 0.30/0.58 tff(203,plain,
% 0.30/0.58 ((~![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero)),
% 0.30/0.58 inference(modus_ponens,[status(thm)],[202, 201])).
% 0.30/0.58 tff(204,plain,
% 0.30/0.58 ((~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero) | (growth_rate(first_movers, sk4(sk2(sk3))) = zero)),
% 0.30/0.58 inference(unit_resolution,[status(thm)],[203, 197, 24, 127])).
% 0.30/0.58 tff(205,plain,
% 0.30/0.58 (greater(growth_rate(first_movers, sk4(sk2(sk3))), zero)),
% 0.30/0.58 inference(unit_resolution,[status(thm)],[204, 187, 113, 115])).
% 0.30/0.58 tff(206,plain,
% 0.30/0.58 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero) | (~greater(growth_rate(first_movers, sk4(sk2(sk3))), zero)) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero) | (~greater(growth_rate(first_movers, sk4(sk2(sk3))), zero)) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))))),
% 0.30/0.58 inference(rewrite,[status(thm)],[])).
% 0.30/0.58 tff(207,plain,
% 0.30/0.58 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero) | (~greater(growth_rate(first_movers, sk4(sk2(sk3))), zero)) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))))),
% 0.30/0.58 inference(quant_inst,[status(thm)],[])).
% 0.30/0.58 tff(208,plain,
% 0.30/0.58 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero) | (~greater(growth_rate(first_movers, sk4(sk2(sk3))), zero)) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))))),
% 0.30/0.58 inference(modus_ponens,[status(thm)],[207, 206])).
% 0.30/0.58 tff(209,plain,
% 0.30/0.58 ($false),
% 0.30/0.58 inference(unit_resolution,[status(thm)],[208, 96, 114, 187, 205])).
% 0.30/0.58 tff(210,plain,((growth_rate(first_movers, sk4(sk2(sk3))) = zero) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3)))), inference(lemma,lemma(discharge,[]))).
% 0.30/0.58 tff(211,plain,
% 0.30/0.58 (growth_rate(first_movers, sk4(sk2(sk3))) = zero),
% 0.30/0.58 inference(unit_resolution,[status(thm)],[210, 114, 113])).
% 0.30/0.58 tff(212,plain,
% 0.30/0.58 (zero = growth_rate(first_movers, sk4(sk2(sk3)))),
% 0.30/0.58 inference(symmetry,[status(thm)],[211])).
% 0.30/0.58 tff(213,plain,
% 0.30/0.58 (greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))) <=> greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)),
% 0.30/0.58 inference(monotonicity,[status(thm)],[211])).
% 0.30/0.58 tff(214,plain,
% 0.30/0.58 (((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | ((~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))) | greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))))) <=> ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))) | greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))))),
% 0.30/0.59 inference(rewrite,[status(thm)],[])).
% 0.30/0.59 tff(215,plain,
% 0.30/0.59 ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | ((~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))) | greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))))),
% 0.30/0.59 inference(quant_inst,[status(thm)],[])).
% 0.30/0.59 tff(216,plain,
% 0.30/0.59 ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))) | greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))),
% 0.30/0.59 inference(modus_ponens,[status(thm)],[215, 214])).
% 0.30/0.59 tff(217,plain,
% 0.30/0.59 (greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))),
% 0.30/0.59 inference(unit_resolution,[status(thm)],[216, 8, 114])).
% 0.30/0.59 tff(218,plain,
% 0.30/0.59 (greater_or_equal(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)),
% 0.30/0.59 inference(modus_ponens,[status(thm)],[217, 213])).
% 0.30/0.59 tff(219,plain,
% 0.30/0.59 (~greater(zero, growth_rate(first_movers, sk4(sk2(sk3))))),
% 0.30/0.59 inference(unit_resolution,[status(thm)],[182, 218])).
% 0.30/0.59 tff(220,plain,
% 0.30/0.59 (greater(growth_rate(first_movers, sk4(sk2(sk3))), zero) <=> greater(zero, growth_rate(first_movers, sk4(sk2(sk3))))),
% 0.30/0.59 inference(monotonicity,[status(thm)],[211, 212])).
% 0.30/0.59 tff(221,plain,
% 0.30/0.59 (greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) <=> greater(growth_rate(first_movers, sk4(sk2(sk3))), zero)),
% 0.30/0.59 inference(symmetry,[status(thm)],[220])).
% 0.30/0.59 tff(222,plain,
% 0.30/0.59 ((~greater(zero, growth_rate(first_movers, sk4(sk2(sk3))))) <=> (~greater(growth_rate(first_movers, sk4(sk2(sk3))), zero))),
% 0.30/0.59 inference(monotonicity,[status(thm)],[221])).
% 0.30/0.59 tff(223,plain,
% 0.30/0.59 (~greater(growth_rate(first_movers, sk4(sk2(sk3))), zero)),
% 0.30/0.59 inference(modus_ponens,[status(thm)],[219, 222])).
% 0.30/0.59 tff(224,plain,
% 0.30/0.59 (^[B: $i, A: $i] : refl((greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero)) <=> (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero)))),
% 0.30/0.59 inference(bind,[status(th)],[])).
% 0.30/0.59 tff(225,plain,
% 0.30/0.59 (![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero)) <=> ![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))),
% 0.30/0.59 inference(quant_intro,[status(thm)],[224])).
% 0.30/0.59 tff(226,plain,
% 0.30/0.59 (![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero)) <=> ![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))),
% 0.30/0.59 inference(rewrite,[status(thm)],[])).
% 0.30/0.59 tff(227,plain,
% 0.30/0.59 (^[B: $i, A: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) <=> ((~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))), (((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(efficient_producers, B) = zero)) <=> (((~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | (growth_rate(efficient_producers, B) = zero)))), rewrite((((~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | (growth_rate(efficient_producers, B) = zero)) <=> ((~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))), (((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(efficient_producers, B) = zero)) <=> ((~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero)))), ((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(efficient_producers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) <=> (((~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero)) | greater(growth_rate(first_movers, B), zero)))), rewrite((((~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) <=> (greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))), ((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(efficient_producers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) <=> (greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero)))), (((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(efficient_producers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) | greater(zero, growth_rate(first_movers, B))) <=> ((greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero)) | greater(zero, growth_rate(first_movers, B))))), rewrite(((greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero)) | greater(zero, growth_rate(first_movers, B))) <=> (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))), (((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(efficient_producers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) | greater(zero, growth_rate(first_movers, B))) <=> (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))))),
% 0.30/0.59 inference(bind,[status(th)],[])).
% 0.30/0.59 tff(228,plain,
% 0.30/0.59 (![B: $i, A: $i] : ((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(efficient_producers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) | greater(zero, growth_rate(first_movers, B))) <=> ![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))),
% 0.30/0.59 inference(quant_intro,[status(thm)],[227])).
% 0.30/0.59 tff(229,axiom,(![B: $i, A: $i] : ((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(efficient_producers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) | greater(zero, growth_rate(first_movers, B)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','l6_35')).
% 0.30/0.59 tff(230,plain,
% 0.30/0.59 (![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))),
% 0.30/0.59 inference(modus_ponens,[status(thm)],[229, 228])).
% 0.30/0.59 tff(231,plain,
% 0.30/0.59 (![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))),
% 0.30/0.59 inference(modus_ponens,[status(thm)],[230, 226])).
% 0.30/0.59 tff(232,plain,(
% 0.30/0.59 ![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))),
% 0.30/0.59 inference(skolemize,[status(sab)],[231])).
% 0.30/0.59 tff(233,plain,
% 0.30/0.59 (![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))),
% 0.30/0.59 inference(modus_ponens,[status(thm)],[232, 225])).
% 0.30/0.59 tff(234,plain,
% 0.30/0.59 (((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))) | ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (growth_rate(efficient_producers, sk4(sk2(sk3))) = zero) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero))) <=> ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (growth_rate(efficient_producers, sk4(sk2(sk3))) = zero) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero))),
% 0.30/0.59 inference(rewrite,[status(thm)],[])).
% 0.30/0.59 tff(235,plain,
% 0.30/0.59 ((greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3)) | (growth_rate(efficient_producers, sk4(sk2(sk3))) = zero)) <=> ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (growth_rate(efficient_producers, sk4(sk2(sk3))) = zero) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero))),
% 0.30/0.59 inference(rewrite,[status(thm)],[])).
% 0.30/0.59 tff(236,plain,
% 0.30/0.59 (((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))) | (greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3)) | (growth_rate(efficient_producers, sk4(sk2(sk3))) = zero))) <=> ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))) | ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (growth_rate(efficient_producers, sk4(sk2(sk3))) = zero) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero)))),
% 0.30/0.59 inference(monotonicity,[status(thm)],[235])).
% 0.30/0.59 tff(237,plain,
% 0.30/0.59 (((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))) | (greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3)) | (growth_rate(efficient_producers, sk4(sk2(sk3))) = zero))) <=> ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (growth_rate(efficient_producers, sk4(sk2(sk3))) = zero) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero))),
% 0.30/0.59 inference(transitivity,[status(thm)],[236, 234])).
% 0.30/0.59 tff(238,plain,
% 0.30/0.59 ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))) | (greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3)) | (growth_rate(efficient_producers, sk4(sk2(sk3))) = zero))),
% 0.30/0.59 inference(quant_inst,[status(thm)],[])).
% 0.30/0.59 tff(239,plain,
% 0.30/0.59 ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (growth_rate(efficient_producers, sk4(sk2(sk3))) = zero) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero)),
% 0.30/0.60 inference(modus_ponens,[status(thm)],[238, 237])).
% 0.30/0.60 tff(240,plain,
% 0.30/0.60 (greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3))) | (growth_rate(efficient_producers, sk4(sk2(sk3))) = zero) | greater(growth_rate(first_movers, sk4(sk2(sk3))), zero)),
% 0.30/0.60 inference(unit_resolution,[status(thm)],[239, 233, 24, 127])).
% 0.30/0.60 tff(241,plain,
% 0.30/0.60 (growth_rate(efficient_producers, sk4(sk2(sk3))) = zero),
% 0.30/0.60 inference(unit_resolution,[status(thm)],[240, 223, 113, 219])).
% 0.30/0.60 tff(242,plain,
% 0.30/0.60 (greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero) <=> greater(zero, growth_rate(first_movers, sk4(sk2(sk3))))),
% 0.30/0.60 inference(monotonicity,[status(thm)],[241, 212])).
% 0.30/0.60 tff(243,plain,
% 0.30/0.60 (greater(zero, growth_rate(first_movers, sk4(sk2(sk3)))) <=> greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)),
% 0.30/0.60 inference(symmetry,[status(thm)],[242])).
% 0.30/0.60 tff(244,plain,
% 0.30/0.60 ((~greater(zero, growth_rate(first_movers, sk4(sk2(sk3))))) <=> (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero))),
% 0.30/0.60 inference(monotonicity,[status(thm)],[243])).
% 0.30/0.60 tff(245,plain,
% 0.30/0.60 (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)),
% 0.30/0.60 inference(modus_ponens,[status(thm)],[219, 244])).
% 0.30/0.60 tff(246,plain,
% 0.30/0.60 (greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))) <=> greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)),
% 0.30/0.60 inference(monotonicity,[status(thm)],[211])).
% 0.30/0.60 tff(247,plain,
% 0.30/0.60 (greater(growth_rate(efficient_producers, sk4(sk2(sk3))), zero)),
% 0.30/0.60 inference(modus_ponens,[status(thm)],[114, 246])).
% 0.30/0.60 tff(248,plain,
% 0.30/0.60 ($false),
% 0.30/0.60 inference(unit_resolution,[status(thm)],[247, 245])).
% 0.30/0.60 tff(249,plain,((~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))) | (~greater_or_equal(sk4(sk2(sk3)), equilibrium(sk3)))), inference(lemma,lemma(discharge,[]))).
% 0.30/0.60 tff(250,plain,
% 0.30/0.60 (~greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3))))),
% 0.30/0.60 inference(unit_resolution,[status(thm)],[249, 112])).
% 0.30/0.60 tff(251,plain,
% 0.30/0.60 (^[B: $i, A: $i] : refl(((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A)))) <=> ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A)))))),
% 0.30/0.60 inference(bind,[status(th)],[])).
% 0.30/0.60 tff(252,plain,
% 0.30/0.60 (![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A)))) <=> ![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))),
% 0.30/0.60 inference(quant_intro,[status(thm)],[251])).
% 0.30/0.60 tff(253,plain,
% 0.30/0.60 (![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A)))) <=> ![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))),
% 0.30/0.60 inference(rewrite,[status(thm)],[])).
% 0.30/0.60 tff(254,plain,
% 0.30/0.60 (^[B: $i, A: $i] : trans(monotonicity(trans(monotonicity(rewrite((((~environment(A)) | (~stable(A))) | (~subpopulations(first_movers, efficient_producers, A, B))) <=> ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))), (((((~environment(A)) | (~stable(A))) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, sk1(A)))) <=> (((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | (~greater_or_equal(B, sk1(A)))))), rewrite((((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | (~greater_or_equal(B, sk1(A)))) <=> ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (~greater_or_equal(B, sk1(A))))), (((((~environment(A)) | (~stable(A))) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, sk1(A)))) <=> ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (~greater_or_equal(B, sk1(A)))))), ((((((~environment(A)) | (~stable(A))) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, sk1(A)))) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B))) <=> (((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (~greater_or_equal(B, sk1(A)))) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B))))), rewrite((((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (~greater_or_equal(B, sk1(A)))) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B))) <=> ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))), ((((((~environment(A)) | (~stable(A))) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, sk1(A)))) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B))) <=> ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))))),
% 0.30/0.60 inference(bind,[status(th)],[])).
% 0.30/0.60 tff(255,plain,
% 0.30/0.60 (![B: $i, A: $i] : (((((~environment(A)) | (~stable(A))) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, sk1(A)))) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B))) <=> ![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))),
% 0.30/0.60 inference(quant_intro,[status(thm)],[254])).
% 0.30/0.60 tff(256,axiom,(![B: $i, A: $i] : (((((~environment(A)) | (~stable(A))) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, sk1(A)))) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','l1_39')).
% 0.30/0.60 tff(257,plain,
% 0.30/0.60 (![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))),
% 0.30/0.60 inference(modus_ponens,[status(thm)],[256, 255])).
% 0.30/0.60 tff(258,plain,
% 0.30/0.60 (![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))),
% 0.30/0.60 inference(modus_ponens,[status(thm)],[257, 253])).
% 0.30/0.60 tff(259,plain,(
% 0.30/0.60 ![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))),
% 0.30/0.60 inference(skolemize,[status(sab)],[258])).
% 0.30/0.60 tff(260,plain,
% 0.30/0.60 (![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))),
% 0.30/0.60 inference(modus_ponens,[status(thm)],[259, 252])).
% 0.30/0.60 tff(261,plain,
% 0.30/0.60 (((~![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))) | ((~stable(sk3)) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), sk1(sk3))))) <=> ((~![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))) | (~stable(sk3)) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), sk1(sk3))))),
% 0.30/0.60 inference(rewrite,[status(thm)],[])).
% 0.30/0.60 tff(262,plain,
% 0.30/0.60 (((~stable(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3)) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), sk1(sk3)))) <=> ((~stable(sk3)) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), sk1(sk3))))),
% 0.30/0.60 inference(rewrite,[status(thm)],[])).
% 0.30/0.60 tff(263,plain,
% 0.30/0.60 (((~![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))) | ((~stable(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3)) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), sk1(sk3))))) <=> ((~![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))) | ((~stable(sk3)) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), sk1(sk3)))))),
% 0.30/0.60 inference(monotonicity,[status(thm)],[262])).
% 0.30/0.60 tff(264,plain,
% 0.30/0.60 (((~![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))) | ((~stable(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3)) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), sk1(sk3))))) <=> ((~![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))) | (~stable(sk3)) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), sk1(sk3))))),
% 0.30/0.60 inference(transitivity,[status(thm)],[263, 261])).
% 0.30/0.60 tff(265,plain,
% 0.30/0.60 ((~![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))) | ((~stable(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | (~environment(sk3)) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), sk1(sk3))))),
% 0.30/0.60 inference(quant_inst,[status(thm)],[])).
% 0.30/0.60 tff(266,plain,
% 0.30/0.60 ((~![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))) | (~stable(sk3)) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk2(sk3)))) | greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), sk1(sk3)))),
% 0.30/0.60 inference(modus_ponens,[status(thm)],[265, 264])).
% 0.30/0.60 tff(267,plain,
% 0.30/0.60 (greater(growth_rate(efficient_producers, sk4(sk2(sk3))), growth_rate(first_movers, sk4(sk2(sk3)))) | (~greater_or_equal(sk4(sk2(sk3)), sk1(sk3)))),
% 0.30/0.60 inference(unit_resolution,[status(thm)],[266, 260, 24, 21, 127])).
% 0.30/0.60 tff(268,plain,
% 0.30/0.60 (~greater_or_equal(sk4(sk2(sk3)), sk1(sk3))),
% 0.30/0.60 inference(unit_resolution,[status(thm)],[267, 250])).
% 0.30/0.60 tff(269,assumption,(greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))), introduced(assumption)).
% 0.30/0.60 tff(270,assumption,(~(growth_rate(first_movers, sk4(sk1(sk3))) = zero)), introduced(assumption)).
% 0.30/0.60 tff(271,assumption,(~greater(growth_rate(first_movers, sk4(sk1(sk3))), zero)), introduced(assumption)).
% 0.30/0.60 tff(272,plain,
% 0.30/0.60 (^[A: $i] : refl((in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A))) <=> (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A))))),
% 0.30/0.60 inference(bind,[status(th)],[])).
% 0.30/0.60 tff(273,plain,
% 0.30/0.60 (![A: $i] : (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A))) <=> ![A: $i] : (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A)))),
% 0.30/0.60 inference(quant_intro,[status(thm)],[272])).
% 0.30/0.60 tff(274,plain,
% 0.30/0.60 (![A: $i] : (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A))) <=> ![A: $i] : (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A)))),
% 0.30/0.60 inference(rewrite,[status(thm)],[])).
% 0.30/0.60 tff(275,plain,
% 0.30/0.60 (^[A: $i] : rewrite((((~environment(A)) | (~stable(A))) | in_environment(A, sk1(A))) <=> (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A))))),
% 0.30/0.60 inference(bind,[status(th)],[])).
% 0.30/0.60 tff(276,plain,
% 0.30/0.60 (![A: $i] : (((~environment(A)) | (~stable(A))) | in_environment(A, sk1(A))) <=> ![A: $i] : (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A)))),
% 0.30/0.60 inference(quant_intro,[status(thm)],[275])).
% 0.30/0.60 tff(277,axiom,(![A: $i] : (((~environment(A)) | (~stable(A))) | in_environment(A, sk1(A)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','l1_38')).
% 0.30/0.60 tff(278,plain,
% 0.30/0.60 (![A: $i] : (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A)))),
% 0.30/0.60 inference(modus_ponens,[status(thm)],[277, 276])).
% 0.30/0.60 tff(279,plain,
% 0.30/0.60 (![A: $i] : (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A)))),
% 0.30/0.60 inference(modus_ponens,[status(thm)],[278, 274])).
% 0.30/0.60 tff(280,plain,(
% 0.30/0.60 ![A: $i] : (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A)))),
% 0.30/0.60 inference(skolemize,[status(sab)],[279])).
% 0.30/0.60 tff(281,plain,
% 0.30/0.60 (![A: $i] : (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A)))),
% 0.30/0.60 inference(modus_ponens,[status(thm)],[280, 273])).
% 0.30/0.60 tff(282,plain,
% 0.30/0.60 (((~![A: $i] : (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A)))) | ((~stable(sk3)) | (~environment(sk3)) | in_environment(sk3, sk1(sk3)))) <=> ((~![A: $i] : (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A)))) | (~stable(sk3)) | (~environment(sk3)) | in_environment(sk3, sk1(sk3)))),
% 0.30/0.60 inference(rewrite,[status(thm)],[])).
% 0.30/0.60 tff(283,plain,
% 0.30/0.60 ((in_environment(sk3, sk1(sk3)) | (~stable(sk3)) | (~environment(sk3))) <=> ((~stable(sk3)) | (~environment(sk3)) | in_environment(sk3, sk1(sk3)))),
% 0.30/0.60 inference(rewrite,[status(thm)],[])).
% 0.30/0.60 tff(284,plain,
% 0.30/0.60 (((~![A: $i] : (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A)))) | (in_environment(sk3, sk1(sk3)) | (~stable(sk3)) | (~environment(sk3)))) <=> ((~![A: $i] : (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A)))) | ((~stable(sk3)) | (~environment(sk3)) | in_environment(sk3, sk1(sk3))))),
% 0.30/0.60 inference(monotonicity,[status(thm)],[283])).
% 0.30/0.60 tff(285,plain,
% 0.30/0.60 (((~![A: $i] : (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A)))) | (in_environment(sk3, sk1(sk3)) | (~stable(sk3)) | (~environment(sk3)))) <=> ((~![A: $i] : (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A)))) | (~stable(sk3)) | (~environment(sk3)) | in_environment(sk3, sk1(sk3)))),
% 0.30/0.60 inference(transitivity,[status(thm)],[284, 282])).
% 0.30/0.60 tff(286,plain,
% 0.30/0.60 ((~![A: $i] : (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A)))) | (in_environment(sk3, sk1(sk3)) | (~stable(sk3)) | (~environment(sk3)))),
% 0.30/0.60 inference(quant_inst,[status(thm)],[])).
% 0.30/0.60 tff(287,plain,
% 0.30/0.60 ((~![A: $i] : (in_environment(A, sk1(A)) | (~stable(A)) | (~environment(A)))) | (~stable(sk3)) | (~environment(sk3)) | in_environment(sk3, sk1(sk3))),
% 0.30/0.60 inference(modus_ponens,[status(thm)],[286, 285])).
% 0.30/0.60 tff(288,plain,
% 0.30/0.60 (in_environment(sk3, sk1(sk3))),
% 0.30/0.60 inference(unit_resolution,[status(thm)],[287, 281, 24, 21])).
% 0.30/0.60 tff(289,plain,
% 0.30/0.60 (((~![A: $i] : ((~in_environment(sk3, A)) | subpopulations(first_movers, efficient_producers, sk3, sk4(A)))) | ((~in_environment(sk3, sk1(sk3))) | subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3))))) <=> ((~![A: $i] : ((~in_environment(sk3, A)) | subpopulations(first_movers, efficient_producers, sk3, sk4(A)))) | (~in_environment(sk3, sk1(sk3))) | subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3))))),
% 0.30/0.60 inference(rewrite,[status(thm)],[])).
% 0.30/0.60 tff(290,plain,
% 0.30/0.60 ((~![A: $i] : ((~in_environment(sk3, A)) | subpopulations(first_movers, efficient_producers, sk3, sk4(A)))) | ((~in_environment(sk3, sk1(sk3))) | subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3))))),
% 0.30/0.60 inference(quant_inst,[status(thm)],[])).
% 0.30/0.60 tff(291,plain,
% 0.30/0.60 ((~![A: $i] : ((~in_environment(sk3, A)) | subpopulations(first_movers, efficient_producers, sk3, sk4(A)))) | (~in_environment(sk3, sk1(sk3))) | subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))),
% 0.30/0.60 inference(modus_ponens,[status(thm)],[290, 289])).
% 0.30/0.60 tff(292,plain,
% 0.30/0.60 (subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))),
% 0.30/0.60 inference(unit_resolution,[status(thm)],[291, 123, 288])).
% 0.30/0.60 tff(293,plain,
% 0.30/0.60 (^[B: $i, A: $i] : refl((greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) <=> (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))))),
% 0.30/0.60 inference(bind,[status(th)],[])).
% 0.30/0.60 tff(294,plain,
% 0.30/0.60 (![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) <=> ![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))),
% 0.30/0.60 inference(quant_intro,[status(thm)],[293])).
% 0.30/0.60 tff(295,plain,
% 0.30/0.60 (![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) <=> ![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))),
% 0.30/0.61 inference(rewrite,[status(thm)],[])).
% 0.30/0.61 tff(296,plain,
% 0.30/0.61 (^[B: $i, A: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) <=> ((~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))), (((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) <=> (((~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | (growth_rate(first_movers, B) = zero)))), rewrite((((~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | (growth_rate(first_movers, B) = zero)) <=> ((growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))), (((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) <=> ((growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))))), ((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) <=> (((growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | greater(growth_rate(first_movers, B), zero)))), rewrite((((growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | greater(growth_rate(first_movers, B), zero)) <=> (greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))), ((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) <=> (greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))))), (((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) | greater(zero, growth_rate(first_movers, B))) <=> ((greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | greater(zero, growth_rate(first_movers, B))))), rewrite(((greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A))) | greater(zero, growth_rate(first_movers, B))) <=> (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))), (((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) | greater(zero, growth_rate(first_movers, B))) <=> (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))))),
% 0.30/0.61 inference(bind,[status(th)],[])).
% 0.30/0.61 tff(297,plain,
% 0.30/0.61 (![B: $i, A: $i] : ((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) | greater(zero, growth_rate(first_movers, B))) <=> ![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))),
% 0.30/0.61 inference(quant_intro,[status(thm)],[296])).
% 0.30/0.61 tff(298,axiom,(![B: $i, A: $i] : ((((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, B))) | (~greater_or_equal(B, equilibrium(A)))) | (growth_rate(first_movers, B) = zero)) | greater(growth_rate(first_movers, B), zero)) | greater(zero, growth_rate(first_movers, B)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','l6_31')).
% 0.30/0.61 tff(299,plain,
% 0.30/0.61 (![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))),
% 0.30/0.61 inference(modus_ponens,[status(thm)],[298, 297])).
% 0.30/0.61 tff(300,plain,
% 0.30/0.61 (![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))),
% 0.30/0.61 inference(modus_ponens,[status(thm)],[299, 295])).
% 0.30/0.61 tff(301,plain,(
% 0.30/0.61 ![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))),
% 0.30/0.61 inference(skolemize,[status(sab)],[300])).
% 0.30/0.61 tff(302,plain,
% 0.30/0.61 (![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))),
% 0.30/0.61 inference(modus_ponens,[status(thm)],[301, 294])).
% 0.30/0.61 tff(303,plain,
% 0.30/0.61 (((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero))) <=> ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero))),
% 0.30/0.61 inference(rewrite,[status(thm)],[])).
% 0.30/0.61 tff(304,plain,
% 0.30/0.61 ((greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3))) <=> ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero))),
% 0.30/0.61 inference(rewrite,[status(thm)],[])).
% 0.30/0.61 tff(305,plain,
% 0.30/0.61 (((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | (greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)))) <=> ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero)))),
% 0.30/0.61 inference(monotonicity,[status(thm)],[304])).
% 0.30/0.61 tff(306,plain,
% 0.30/0.61 (((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | (greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)))) <=> ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero))),
% 0.30/0.61 inference(transitivity,[status(thm)],[305, 303])).
% 0.30/0.61 tff(307,plain,
% 0.30/0.61 ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | (greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)))),
% 0.30/0.61 inference(quant_inst,[status(thm)],[])).
% 0.30/0.61 tff(308,plain,
% 0.30/0.61 ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero)),
% 0.30/0.61 inference(modus_ponens,[status(thm)],[307, 306])).
% 0.30/0.61 tff(309,plain,
% 0.30/0.61 (greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero)),
% 0.30/0.61 inference(unit_resolution,[status(thm)],[308, 302, 24, 292])).
% 0.30/0.61 tff(310,plain,
% 0.30/0.61 (greater(zero, growth_rate(first_movers, sk4(sk1(sk3))))),
% 0.30/0.61 inference(unit_resolution,[status(thm)],[309, 271, 269, 270])).
% 0.30/0.61 tff(311,plain,
% 0.30/0.61 (((~![A: $i] : ((~in_environment(sk3, A)) | (~outcompetes(efficient_producers, first_movers, sk4(A))))) | ((~in_environment(sk3, sk1(sk3))) | (~outcompetes(efficient_producers, first_movers, sk4(sk1(sk3)))))) <=> ((~![A: $i] : ((~in_environment(sk3, A)) | (~outcompetes(efficient_producers, first_movers, sk4(A))))) | (~in_environment(sk3, sk1(sk3))) | (~outcompetes(efficient_producers, first_movers, sk4(sk1(sk3)))))),
% 0.30/0.61 inference(rewrite,[status(thm)],[])).
% 0.30/0.61 tff(312,plain,
% 0.30/0.61 ((~![A: $i] : ((~in_environment(sk3, A)) | (~outcompetes(efficient_producers, first_movers, sk4(A))))) | ((~in_environment(sk3, sk1(sk3))) | (~outcompetes(efficient_producers, first_movers, sk4(sk1(sk3)))))),
% 0.30/0.61 inference(quant_inst,[status(thm)],[])).
% 0.30/0.61 tff(313,plain,
% 0.30/0.61 ((~![A: $i] : ((~in_environment(sk3, A)) | (~outcompetes(efficient_producers, first_movers, sk4(A))))) | (~in_environment(sk3, sk1(sk3))) | (~outcompetes(efficient_producers, first_movers, sk4(sk1(sk3))))),
% 0.30/0.61 inference(modus_ponens,[status(thm)],[312, 311])).
% 0.30/0.61 tff(314,plain,
% 0.30/0.61 (~outcompetes(efficient_producers, first_movers, sk4(sk1(sk3)))),
% 0.30/0.61 inference(unit_resolution,[status(thm)],[313, 161, 288])).
% 0.30/0.61 tff(315,plain,
% 0.30/0.61 (((~![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | ((~environment(sk3)) | outcompetes(efficient_producers, first_movers, sk4(sk1(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~greater(zero, growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)))) <=> ((~![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | (~environment(sk3)) | outcompetes(efficient_producers, first_movers, sk4(sk1(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~greater(zero, growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)))),
% 0.30/0.61 inference(rewrite,[status(thm)],[])).
% 0.30/0.61 tff(316,plain,
% 0.30/0.61 ((outcompetes(efficient_producers, first_movers, sk4(sk1(sk3))) | (~greater(zero, growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3))) <=> ((~environment(sk3)) | outcompetes(efficient_producers, first_movers, sk4(sk1(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~greater(zero, growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)))),
% 0.30/0.61 inference(rewrite,[status(thm)],[])).
% 0.30/0.61 tff(317,plain,
% 0.30/0.61 (((~![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | (outcompetes(efficient_producers, first_movers, sk4(sk1(sk3))) | (~greater(zero, growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)))) <=> ((~![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | ((~environment(sk3)) | outcompetes(efficient_producers, first_movers, sk4(sk1(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~greater(zero, growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero))))),
% 0.30/0.62 inference(monotonicity,[status(thm)],[316])).
% 0.30/0.62 tff(318,plain,
% 0.30/0.62 (((~![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | (outcompetes(efficient_producers, first_movers, sk4(sk1(sk3))) | (~greater(zero, growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)))) <=> ((~![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | (~environment(sk3)) | outcompetes(efficient_producers, first_movers, sk4(sk1(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~greater(zero, growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)))),
% 0.30/0.62 inference(transitivity,[status(thm)],[317, 315])).
% 0.30/0.62 tff(319,plain,
% 0.30/0.62 ((~![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | (outcompetes(efficient_producers, first_movers, sk4(sk1(sk3))) | (~greater(zero, growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)))),
% 0.30/0.62 inference(quant_inst,[status(thm)],[])).
% 0.30/0.62 tff(320,plain,
% 0.30/0.62 ((~![B: $i, D: $i, A: $i, C: $i] : (outcompetes(C, B, D) | (~greater(zero, growth_rate(B, D))) | (~greater_or_equal(growth_rate(C, D), zero)) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | (~environment(sk3)) | outcompetes(efficient_producers, first_movers, sk4(sk1(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~greater(zero, growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero))),
% 0.30/0.62 inference(modus_ponens,[status(thm)],[319, 318])).
% 0.30/0.62 tff(321,plain,
% 0.30/0.62 ((~greater(zero, growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero))),
% 0.30/0.62 inference(unit_resolution,[status(thm)],[320, 175, 24, 314, 292])).
% 0.30/0.62 tff(322,plain,
% 0.30/0.62 (~greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)),
% 0.30/0.62 inference(unit_resolution,[status(thm)],[321, 310])).
% 0.30/0.62 tff(323,plain,
% 0.30/0.62 (((~![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero))) <=> ((~![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero))),
% 0.30/0.62 inference(rewrite,[status(thm)],[])).
% 0.30/0.62 tff(324,plain,
% 0.30/0.62 ((greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3))) <=> ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero))),
% 0.30/0.62 inference(rewrite,[status(thm)],[])).
% 0.30/0.62 tff(325,plain,
% 0.30/0.62 (((~![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | (greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)))) <=> ((~![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero)))),
% 0.30/0.62 inference(monotonicity,[status(thm)],[324])).
% 0.30/0.62 tff(326,plain,
% 0.30/0.62 (((~![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | (greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)))) <=> ((~![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero))),
% 0.30/0.62 inference(transitivity,[status(thm)],[325, 323])).
% 0.30/0.62 tff(327,plain,
% 0.30/0.62 ((~![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | (greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)))),
% 0.30/0.62 inference(quant_inst,[status(thm)],[])).
% 0.30/0.62 tff(328,plain,
% 0.30/0.62 ((~![B: $i, A: $i] : (greater(growth_rate(efficient_producers, B), zero) | greater(growth_rate(first_movers, B), zero) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero)),
% 0.30/0.62 inference(modus_ponens,[status(thm)],[327, 326])).
% 0.30/0.62 tff(329,plain,
% 0.30/0.62 ((~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero)),
% 0.30/0.62 inference(unit_resolution,[status(thm)],[328, 197, 24, 292])).
% 0.30/0.62 tff(330,plain,
% 0.30/0.62 (greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)),
% 0.30/0.62 inference(unit_resolution,[status(thm)],[329, 271, 269, 270])).
% 0.30/0.62 tff(331,plain,
% 0.30/0.62 (((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | ((~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)) | greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero))) <=> ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)) | greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero))),
% 0.30/0.62 inference(rewrite,[status(thm)],[])).
% 0.30/0.62 tff(332,plain,
% 0.30/0.62 ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | ((~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)) | greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero))),
% 0.30/0.62 inference(quant_inst,[status(thm)],[])).
% 0.30/0.62 tff(333,plain,
% 0.30/0.62 ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)) | greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)),
% 0.30/0.62 inference(modus_ponens,[status(thm)],[332, 331])).
% 0.30/0.62 tff(334,plain,
% 0.30/0.62 ($false),
% 0.30/0.62 inference(unit_resolution,[status(thm)],[333, 8, 330, 322])).
% 0.30/0.62 tff(335,plain,(greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero)), inference(lemma,lemma(discharge,[]))).
% 0.30/0.62 tff(336,plain,
% 0.30/0.62 (greater(growth_rate(first_movers, sk4(sk1(sk3))), zero)),
% 0.30/0.62 inference(unit_resolution,[status(thm)],[335, 269, 270])).
% 0.30/0.62 tff(337,plain,
% 0.30/0.62 (((~![A: $i] : ((~in_environment(sk3, A)) | greater_or_equal(sk4(A), A))) | ((~in_environment(sk3, sk1(sk3))) | greater_or_equal(sk4(sk1(sk3)), sk1(sk3)))) <=> ((~![A: $i] : ((~in_environment(sk3, A)) | greater_or_equal(sk4(A), A))) | (~in_environment(sk3, sk1(sk3))) | greater_or_equal(sk4(sk1(sk3)), sk1(sk3)))),
% 0.30/0.62 inference(rewrite,[status(thm)],[])).
% 0.30/0.62 tff(338,plain,
% 0.30/0.62 ((~![A: $i] : ((~in_environment(sk3, A)) | greater_or_equal(sk4(A), A))) | ((~in_environment(sk3, sk1(sk3))) | greater_or_equal(sk4(sk1(sk3)), sk1(sk3)))),
% 0.30/0.62 inference(quant_inst,[status(thm)],[])).
% 0.30/0.62 tff(339,plain,
% 0.30/0.62 ((~![A: $i] : ((~in_environment(sk3, A)) | greater_or_equal(sk4(A), A))) | (~in_environment(sk3, sk1(sk3))) | greater_or_equal(sk4(sk1(sk3)), sk1(sk3))),
% 0.30/0.62 inference(modus_ponens,[status(thm)],[338, 337])).
% 0.30/0.62 tff(340,plain,
% 0.30/0.62 (greater_or_equal(sk4(sk1(sk3)), sk1(sk3))),
% 0.30/0.62 inference(unit_resolution,[status(thm)],[339, 48, 288])).
% 0.30/0.62 tff(341,plain,
% 0.30/0.62 (((~![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))) | ((~stable(sk3)) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), sk1(sk3))))) <=> ((~![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))) | (~stable(sk3)) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), sk1(sk3))))),
% 0.30/0.62 inference(rewrite,[status(thm)],[])).
% 0.30/0.62 tff(342,plain,
% 0.30/0.62 (((~stable(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), sk1(sk3)))) <=> ((~stable(sk3)) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), sk1(sk3))))),
% 0.30/0.62 inference(rewrite,[status(thm)],[])).
% 0.30/0.62 tff(343,plain,
% 0.30/0.62 (((~![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))) | ((~stable(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), sk1(sk3))))) <=> ((~![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))) | ((~stable(sk3)) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), sk1(sk3)))))),
% 0.30/0.62 inference(monotonicity,[status(thm)],[342])).
% 0.30/0.62 tff(344,plain,
% 0.30/0.62 (((~![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))) | ((~stable(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), sk1(sk3))))) <=> ((~![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))) | (~stable(sk3)) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), sk1(sk3))))),
% 0.30/0.62 inference(transitivity,[status(thm)],[343, 341])).
% 0.30/0.62 tff(345,plain,
% 0.30/0.62 ((~![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))) | ((~stable(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), sk1(sk3))))),
% 0.37/0.63 inference(quant_inst,[status(thm)],[])).
% 0.37/0.63 tff(346,plain,
% 0.37/0.63 ((~![B: $i, A: $i] : ((~stable(A)) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(growth_rate(efficient_producers, B), growth_rate(first_movers, B)) | (~greater_or_equal(B, sk1(A))))) | (~stable(sk3)) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), sk1(sk3)))),
% 0.37/0.63 inference(modus_ponens,[status(thm)],[345, 344])).
% 0.37/0.63 tff(347,plain,
% 0.37/0.63 (greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))),
% 0.37/0.63 inference(unit_resolution,[status(thm)],[346, 260, 24, 21, 292, 340])).
% 0.37/0.63 tff(348,plain,
% 0.37/0.63 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater(growth_rate(first_movers, sk4(sk1(sk3))), zero)))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater(growth_rate(first_movers, sk4(sk1(sk3))), zero)))),
% 0.37/0.63 inference(rewrite,[status(thm)],[])).
% 0.37/0.63 tff(349,plain,
% 0.37/0.63 ((greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | (~greater(growth_rate(first_movers, sk4(sk1(sk3))), zero)) | (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3)))))) <=> (greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater(growth_rate(first_movers, sk4(sk1(sk3))), zero)))),
% 0.37/0.63 inference(rewrite,[status(thm)],[])).
% 0.37/0.63 tff(350,plain,
% 0.37/0.63 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | (~greater(growth_rate(first_movers, sk4(sk1(sk3))), zero)) | (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater(growth_rate(first_movers, sk4(sk1(sk3))), zero))))),
% 0.37/0.63 inference(monotonicity,[status(thm)],[349])).
% 0.37/0.63 tff(351,plain,
% 0.37/0.63 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | (~greater(growth_rate(first_movers, sk4(sk1(sk3))), zero)) | (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater(growth_rate(first_movers, sk4(sk1(sk3))), zero)))),
% 0.37/0.63 inference(transitivity,[status(thm)],[350, 348])).
% 0.37/0.63 tff(352,plain,
% 0.37/0.63 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | (~greater(growth_rate(first_movers, sk4(sk1(sk3))), zero)) | (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))))),
% 0.37/0.63 inference(quant_inst,[status(thm)],[])).
% 0.37/0.63 tff(353,plain,
% 0.37/0.63 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) | (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater(growth_rate(first_movers, sk4(sk1(sk3))), zero))),
% 0.37/0.63 inference(modus_ponens,[status(thm)],[352, 351])).
% 0.37/0.63 tff(354,plain,
% 0.37/0.63 (greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)),
% 0.37/0.63 inference(unit_resolution,[status(thm)],[353, 96, 347, 336])).
% 0.37/0.63 tff(355,plain,
% 0.37/0.63 (greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)),
% 0.37/0.63 inference(unit_resolution,[status(thm)],[333, 8, 354])).
% 0.37/0.63 tff(356,plain,
% 0.37/0.63 (~greater(zero, growth_rate(first_movers, sk4(sk1(sk3))))),
% 0.37/0.63 inference(unit_resolution,[status(thm)],[321, 355])).
% 0.37/0.63 tff(357,plain,
% 0.37/0.63 (((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))) | ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(zero, growth_rate(efficient_producers, sk4(sk1(sk3)))) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero))) <=> ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(zero, growth_rate(efficient_producers, sk4(sk1(sk3)))) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero))),
% 0.37/0.63 inference(rewrite,[status(thm)],[])).
% 0.37/0.63 tff(358,plain,
% 0.37/0.63 ((greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)) | greater(zero, growth_rate(efficient_producers, sk4(sk1(sk3))))) <=> ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(zero, growth_rate(efficient_producers, sk4(sk1(sk3)))) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero))),
% 0.37/0.63 inference(rewrite,[status(thm)],[])).
% 0.37/0.63 tff(359,plain,
% 0.37/0.63 (((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))) | (greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)) | greater(zero, growth_rate(efficient_producers, sk4(sk1(sk3)))))) <=> ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))) | ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(zero, growth_rate(efficient_producers, sk4(sk1(sk3)))) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero)))),
% 0.37/0.63 inference(monotonicity,[status(thm)],[358])).
% 0.37/0.63 tff(360,plain,
% 0.37/0.63 (((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))) | (greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)) | greater(zero, growth_rate(efficient_producers, sk4(sk1(sk3)))))) <=> ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(zero, growth_rate(efficient_producers, sk4(sk1(sk3)))) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero))),
% 0.37/0.63 inference(transitivity,[status(thm)],[359, 357])).
% 0.37/0.63 tff(361,plain,
% 0.37/0.63 ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))) | (greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)) | greater(zero, growth_rate(efficient_producers, sk4(sk1(sk3)))))),
% 0.37/0.63 inference(quant_inst,[status(thm)],[])).
% 0.37/0.63 tff(362,plain,
% 0.37/0.63 ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | (growth_rate(first_movers, B) = zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | greater(zero, growth_rate(efficient_producers, B)))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(zero, growth_rate(efficient_producers, sk4(sk1(sk3)))) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero)),
% 0.37/0.63 inference(modus_ponens,[status(thm)],[361, 360])).
% 0.37/0.63 tff(363,plain,
% 0.37/0.63 (greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | greater(zero, growth_rate(efficient_producers, sk4(sk1(sk3)))) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero)),
% 0.37/0.63 inference(unit_resolution,[status(thm)],[362, 137, 24, 292])).
% 0.37/0.63 tff(364,plain,
% 0.37/0.63 (greater(zero, growth_rate(efficient_producers, sk4(sk1(sk3))))),
% 0.37/0.63 inference(unit_resolution,[status(thm)],[363, 356, 269, 270])).
% 0.37/0.63 tff(365,plain,
% 0.37/0.63 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater(zero, growth_rate(efficient_producers, sk4(sk1(sk3))))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater(zero, growth_rate(efficient_producers, sk4(sk1(sk3))))))),
% 0.37/0.63 inference(rewrite,[status(thm)],[])).
% 0.37/0.63 tff(366,plain,
% 0.37/0.63 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater(zero, growth_rate(efficient_producers, sk4(sk1(sk3))))))),
% 0.37/0.63 inference(quant_inst,[status(thm)],[])).
% 0.37/0.63 tff(367,plain,
% 0.37/0.63 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))) | (~greater(zero, growth_rate(efficient_producers, sk4(sk1(sk3)))))),
% 0.37/0.63 inference(modus_ponens,[status(thm)],[366, 365])).
% 0.37/0.63 tff(368,plain,
% 0.37/0.63 ($false),
% 0.37/0.63 inference(unit_resolution,[status(thm)],[367, 96, 347, 356, 364])).
% 0.37/0.63 tff(369,plain,((~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (growth_rate(first_movers, sk4(sk1(sk3))) = zero)), inference(lemma,lemma(discharge,[]))).
% 0.37/0.63 tff(370,plain,
% 0.37/0.63 (growth_rate(first_movers, sk4(sk1(sk3))) = zero),
% 0.37/0.63 inference(unit_resolution,[status(thm)],[369, 269])).
% 0.37/0.63 tff(371,plain,
% 0.37/0.63 (zero = growth_rate(first_movers, sk4(sk1(sk3)))),
% 0.37/0.63 inference(symmetry,[status(thm)],[370])).
% 0.37/0.63 tff(372,plain,
% 0.37/0.63 (greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3)))) <=> greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)),
% 0.37/0.63 inference(monotonicity,[status(thm)],[370])).
% 0.37/0.63 tff(373,plain,
% 0.37/0.63 (((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | ((~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))) | greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3)))))) <=> ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))) | greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3)))))),
% 0.37/0.63 inference(rewrite,[status(thm)],[])).
% 0.37/0.63 tff(374,plain,
% 0.37/0.63 ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | ((~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))) | greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3)))))),
% 0.37/0.63 inference(quant_inst,[status(thm)],[])).
% 0.37/0.63 tff(375,plain,
% 0.37/0.63 ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))) | greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))),
% 0.37/0.63 inference(modus_ponens,[status(thm)],[374, 373])).
% 0.37/0.63 tff(376,plain,
% 0.37/0.63 (greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3))))),
% 0.37/0.63 inference(unit_resolution,[status(thm)],[375, 8, 347])).
% 0.37/0.63 tff(377,plain,
% 0.37/0.63 (greater_or_equal(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)),
% 0.37/0.63 inference(modus_ponens,[status(thm)],[376, 372])).
% 0.37/0.63 tff(378,plain,
% 0.37/0.63 (~greater(zero, growth_rate(first_movers, sk4(sk1(sk3))))),
% 0.37/0.63 inference(unit_resolution,[status(thm)],[321, 377])).
% 0.37/0.63 tff(379,plain,
% 0.37/0.63 (greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) <=> greater(zero, growth_rate(first_movers, sk4(sk1(sk3))))),
% 0.37/0.63 inference(monotonicity,[status(thm)],[370, 371])).
% 0.37/0.63 tff(380,plain,
% 0.37/0.63 (greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) <=> greater(growth_rate(first_movers, sk4(sk1(sk3))), zero)),
% 0.37/0.63 inference(symmetry,[status(thm)],[379])).
% 0.37/0.63 tff(381,plain,
% 0.37/0.63 ((~greater(zero, growth_rate(first_movers, sk4(sk1(sk3))))) <=> (~greater(growth_rate(first_movers, sk4(sk1(sk3))), zero))),
% 0.37/0.63 inference(monotonicity,[status(thm)],[380])).
% 0.37/0.63 tff(382,plain,
% 0.37/0.63 (~greater(growth_rate(first_movers, sk4(sk1(sk3))), zero)),
% 0.37/0.63 inference(modus_ponens,[status(thm)],[378, 381])).
% 0.37/0.63 tff(383,plain,
% 0.37/0.63 (((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))) | ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (growth_rate(efficient_producers, sk4(sk1(sk3))) = zero) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero))) <=> ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (growth_rate(efficient_producers, sk4(sk1(sk3))) = zero) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero))),
% 0.37/0.64 inference(rewrite,[status(thm)],[])).
% 0.37/0.64 tff(384,plain,
% 0.37/0.64 ((greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)) | (growth_rate(efficient_producers, sk4(sk1(sk3))) = zero)) <=> ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (growth_rate(efficient_producers, sk4(sk1(sk3))) = zero) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero))),
% 0.37/0.64 inference(rewrite,[status(thm)],[])).
% 0.37/0.64 tff(385,plain,
% 0.37/0.64 (((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))) | (greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)) | (growth_rate(efficient_producers, sk4(sk1(sk3))) = zero))) <=> ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))) | ((~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (growth_rate(efficient_producers, sk4(sk1(sk3))) = zero) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero)))),
% 0.37/0.64 inference(monotonicity,[status(thm)],[384])).
% 0.37/0.64 tff(386,plain,
% 0.37/0.64 (((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))) | (greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)) | (growth_rate(efficient_producers, sk4(sk1(sk3))) = zero))) <=> ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (growth_rate(efficient_producers, sk4(sk1(sk3))) = zero) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero))),
% 0.37/0.64 inference(transitivity,[status(thm)],[385, 383])).
% 0.37/0.64 tff(387,plain,
% 0.37/0.64 ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))) | (greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | (~environment(sk3)) | (growth_rate(efficient_producers, sk4(sk1(sk3))) = zero))),
% 0.37/0.64 inference(quant_inst,[status(thm)],[])).
% 0.37/0.64 tff(388,plain,
% 0.37/0.64 ((~![B: $i, A: $i] : (greater(zero, growth_rate(first_movers, B)) | greater(growth_rate(first_movers, B), zero) | (~greater_or_equal(B, equilibrium(A))) | (~subpopulations(first_movers, efficient_producers, A, B)) | (~environment(A)) | (growth_rate(efficient_producers, B) = zero))) | (~environment(sk3)) | (~subpopulations(first_movers, efficient_producers, sk3, sk4(sk1(sk3)))) | greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (growth_rate(efficient_producers, sk4(sk1(sk3))) = zero) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero)),
% 0.37/0.64 inference(modus_ponens,[status(thm)],[387, 386])).
% 0.37/0.64 tff(389,plain,
% 0.37/0.64 (greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) | (~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))) | (growth_rate(efficient_producers, sk4(sk1(sk3))) = zero) | greater(growth_rate(first_movers, sk4(sk1(sk3))), zero)),
% 0.37/0.64 inference(unit_resolution,[status(thm)],[388, 233, 24, 292])).
% 0.37/0.64 tff(390,plain,
% 0.37/0.64 (growth_rate(efficient_producers, sk4(sk1(sk3))) = zero),
% 0.37/0.64 inference(unit_resolution,[status(thm)],[389, 382, 269, 378])).
% 0.37/0.64 tff(391,plain,
% 0.37/0.64 (greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero) <=> greater(zero, growth_rate(first_movers, sk4(sk1(sk3))))),
% 0.37/0.64 inference(monotonicity,[status(thm)],[390, 371])).
% 0.37/0.64 tff(392,plain,
% 0.37/0.64 (greater(zero, growth_rate(first_movers, sk4(sk1(sk3)))) <=> greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)),
% 0.37/0.64 inference(symmetry,[status(thm)],[391])).
% 0.37/0.64 tff(393,plain,
% 0.37/0.64 ((~greater(zero, growth_rate(first_movers, sk4(sk1(sk3))))) <=> (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero))),
% 0.37/0.64 inference(monotonicity,[status(thm)],[392])).
% 0.37/0.64 tff(394,plain,
% 0.37/0.64 (~greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)),
% 0.37/0.64 inference(modus_ponens,[status(thm)],[378, 393])).
% 0.37/0.64 tff(395,plain,
% 0.37/0.64 (greater(growth_rate(efficient_producers, sk4(sk1(sk3))), growth_rate(first_movers, sk4(sk1(sk3)))) <=> greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)),
% 0.37/0.64 inference(monotonicity,[status(thm)],[370])).
% 0.37/0.64 tff(396,plain,
% 0.37/0.64 (greater(growth_rate(efficient_producers, sk4(sk1(sk3))), zero)),
% 0.37/0.64 inference(modus_ponens,[status(thm)],[347, 395])).
% 0.37/0.64 tff(397,plain,
% 0.37/0.64 ($false),
% 0.37/0.64 inference(unit_resolution,[status(thm)],[396, 394])).
% 0.37/0.64 tff(398,plain,(~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))), inference(lemma,lemma(discharge,[]))).
% 0.37/0.64 tff(399,assumption,(~greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))), introduced(assumption)).
% 0.37/0.64 tff(400,plain,
% 0.37/0.64 (((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | ((~greater(sk4(sk1(sk3)), equilibrium(sk3))) | greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3)))) <=> ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | (~greater(sk4(sk1(sk3)), equilibrium(sk3))) | greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3)))),
% 0.37/0.64 inference(rewrite,[status(thm)],[])).
% 0.37/0.64 tff(401,plain,
% 0.37/0.64 ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | ((~greater(sk4(sk1(sk3)), equilibrium(sk3))) | greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3)))),
% 0.37/0.64 inference(quant_inst,[status(thm)],[])).
% 0.37/0.64 tff(402,plain,
% 0.37/0.64 ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | (~greater(sk4(sk1(sk3)), equilibrium(sk3))) | greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))),
% 0.37/0.64 inference(modus_ponens,[status(thm)],[401, 400])).
% 0.37/0.64 tff(403,plain,
% 0.37/0.64 (~greater(sk4(sk1(sk3)), equilibrium(sk3))),
% 0.37/0.64 inference(unit_resolution,[status(thm)],[402, 8, 399])).
% 0.37/0.64 tff(404,assumption,(greater(sk1(sk3), equilibrium(sk3))), introduced(assumption)).
% 0.37/0.64 tff(405,assumption,(~greater(sk4(sk1(sk3)), equilibrium(sk3))), introduced(assumption)).
% 0.37/0.64 tff(406,assumption,(greater(sk4(sk1(sk3)), sk1(sk3))), introduced(assumption)).
% 0.37/0.64 tff(407,plain,
% 0.37/0.64 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(sk4(sk1(sk3)), equilibrium(sk3)) | (~greater(sk1(sk3), equilibrium(sk3))) | (~greater(sk4(sk1(sk3)), sk1(sk3))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(sk4(sk1(sk3)), equilibrium(sk3)) | (~greater(sk1(sk3), equilibrium(sk3))) | (~greater(sk4(sk1(sk3)), sk1(sk3))))),
% 0.37/0.64 inference(rewrite,[status(thm)],[])).
% 0.37/0.64 tff(408,plain,
% 0.37/0.64 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(sk4(sk1(sk3)), equilibrium(sk3)) | (~greater(sk1(sk3), equilibrium(sk3))) | (~greater(sk4(sk1(sk3)), sk1(sk3))))),
% 0.37/0.64 inference(quant_inst,[status(thm)],[])).
% 0.37/0.64 tff(409,plain,
% 0.37/0.64 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(sk4(sk1(sk3)), equilibrium(sk3)) | (~greater(sk1(sk3), equilibrium(sk3))) | (~greater(sk4(sk1(sk3)), sk1(sk3)))),
% 0.37/0.64 inference(modus_ponens,[status(thm)],[408, 407])).
% 0.37/0.64 tff(410,plain,
% 0.37/0.64 ($false),
% 0.37/0.64 inference(unit_resolution,[status(thm)],[409, 96, 406, 405, 404])).
% 0.37/0.64 tff(411,plain,((~greater(sk1(sk3), equilibrium(sk3))) | (~greater(sk4(sk1(sk3)), sk1(sk3))) | greater(sk4(sk1(sk3)), equilibrium(sk3))), inference(lemma,lemma(discharge,[]))).
% 0.37/0.64 tff(412,plain,
% 0.37/0.64 (~greater(sk4(sk1(sk3)), sk1(sk3))),
% 0.37/0.64 inference(unit_resolution,[status(thm)],[411, 404, 403])).
% 0.37/0.64 tff(413,plain,
% 0.37/0.64 (((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((~greater_or_equal(sk4(sk1(sk3)), sk1(sk3))) | (sk4(sk1(sk3)) = sk1(sk3)) | greater(sk4(sk1(sk3)), sk1(sk3)))) <=> ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | (~greater_or_equal(sk4(sk1(sk3)), sk1(sk3))) | (sk4(sk1(sk3)) = sk1(sk3)) | greater(sk4(sk1(sk3)), sk1(sk3)))),
% 0.37/0.64 inference(rewrite,[status(thm)],[])).
% 0.37/0.64 tff(414,plain,
% 0.37/0.64 (((sk4(sk1(sk3)) = sk1(sk3)) | greater(sk4(sk1(sk3)), sk1(sk3)) | (~greater_or_equal(sk4(sk1(sk3)), sk1(sk3)))) <=> ((~greater_or_equal(sk4(sk1(sk3)), sk1(sk3))) | (sk4(sk1(sk3)) = sk1(sk3)) | greater(sk4(sk1(sk3)), sk1(sk3)))),
% 0.37/0.64 inference(rewrite,[status(thm)],[])).
% 0.37/0.64 tff(415,plain,
% 0.37/0.64 (((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((sk4(sk1(sk3)) = sk1(sk3)) | greater(sk4(sk1(sk3)), sk1(sk3)) | (~greater_or_equal(sk4(sk1(sk3)), sk1(sk3))))) <=> ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((~greater_or_equal(sk4(sk1(sk3)), sk1(sk3))) | (sk4(sk1(sk3)) = sk1(sk3)) | greater(sk4(sk1(sk3)), sk1(sk3))))),
% 0.37/0.64 inference(monotonicity,[status(thm)],[414])).
% 0.37/0.64 tff(416,plain,
% 0.37/0.64 (((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((sk4(sk1(sk3)) = sk1(sk3)) | greater(sk4(sk1(sk3)), sk1(sk3)) | (~greater_or_equal(sk4(sk1(sk3)), sk1(sk3))))) <=> ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | (~greater_or_equal(sk4(sk1(sk3)), sk1(sk3))) | (sk4(sk1(sk3)) = sk1(sk3)) | greater(sk4(sk1(sk3)), sk1(sk3)))),
% 0.37/0.64 inference(transitivity,[status(thm)],[415, 413])).
% 0.37/0.64 tff(417,plain,
% 0.37/0.64 ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((sk4(sk1(sk3)) = sk1(sk3)) | greater(sk4(sk1(sk3)), sk1(sk3)) | (~greater_or_equal(sk4(sk1(sk3)), sk1(sk3))))),
% 0.37/0.64 inference(quant_inst,[status(thm)],[])).
% 0.37/0.64 tff(418,plain,
% 0.37/0.64 ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | (~greater_or_equal(sk4(sk1(sk3)), sk1(sk3))) | (sk4(sk1(sk3)) = sk1(sk3)) | greater(sk4(sk1(sk3)), sk1(sk3))),
% 0.37/0.64 inference(modus_ponens,[status(thm)],[417, 416])).
% 0.37/0.64 tff(419,plain,
% 0.37/0.64 ((sk4(sk1(sk3)) = sk1(sk3)) | greater(sk4(sk1(sk3)), sk1(sk3))),
% 0.37/0.64 inference(unit_resolution,[status(thm)],[418, 79, 340])).
% 0.37/0.64 tff(420,plain,
% 0.37/0.64 (sk4(sk1(sk3)) = sk1(sk3)),
% 0.37/0.64 inference(unit_resolution,[status(thm)],[419, 412])).
% 0.37/0.64 tff(421,plain,
% 0.37/0.64 (greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3)) <=> greater_or_equal(sk1(sk3), equilibrium(sk3))),
% 0.37/0.64 inference(monotonicity,[status(thm)],[420])).
% 0.37/0.64 tff(422,plain,
% 0.37/0.64 (greater_or_equal(sk1(sk3), equilibrium(sk3)) <=> greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))),
% 0.37/0.64 inference(symmetry,[status(thm)],[421])).
% 0.37/0.64 tff(423,assumption,(~greater_or_equal(sk1(sk3), equilibrium(sk3))), introduced(assumption)).
% 0.37/0.64 tff(424,plain,
% 0.37/0.64 (((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | ((~greater(sk1(sk3), equilibrium(sk3))) | greater_or_equal(sk1(sk3), equilibrium(sk3)))) <=> ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | (~greater(sk1(sk3), equilibrium(sk3))) | greater_or_equal(sk1(sk3), equilibrium(sk3)))),
% 0.37/0.64 inference(rewrite,[status(thm)],[])).
% 0.37/0.64 tff(425,plain,
% 0.37/0.64 ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | ((~greater(sk1(sk3), equilibrium(sk3))) | greater_or_equal(sk1(sk3), equilibrium(sk3)))),
% 0.37/0.64 inference(quant_inst,[status(thm)],[])).
% 0.37/0.64 tff(426,plain,
% 0.37/0.64 ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | (~greater(sk1(sk3), equilibrium(sk3))) | greater_or_equal(sk1(sk3), equilibrium(sk3))),
% 0.37/0.64 inference(modus_ponens,[status(thm)],[425, 424])).
% 0.37/0.64 tff(427,plain,
% 0.37/0.64 ($false),
% 0.37/0.64 inference(unit_resolution,[status(thm)],[426, 8, 423, 404])).
% 0.37/0.64 tff(428,plain,((~greater(sk1(sk3), equilibrium(sk3))) | greater_or_equal(sk1(sk3), equilibrium(sk3))), inference(lemma,lemma(discharge,[]))).
% 0.37/0.64 tff(429,plain,
% 0.37/0.64 (greater_or_equal(sk1(sk3), equilibrium(sk3))),
% 0.37/0.64 inference(unit_resolution,[status(thm)],[428, 404])).
% 0.37/0.64 tff(430,plain,
% 0.37/0.64 (greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))),
% 0.37/0.64 inference(modus_ponens,[status(thm)],[429, 422])).
% 0.37/0.64 tff(431,plain,
% 0.37/0.64 ($false),
% 0.37/0.64 inference(unit_resolution,[status(thm)],[399, 430])).
% 0.37/0.64 tff(432,plain,((~greater(sk1(sk3), equilibrium(sk3))) | greater_or_equal(sk4(sk1(sk3)), equilibrium(sk3))), inference(lemma,lemma(discharge,[]))).
% 0.37/0.64 tff(433,plain,
% 0.37/0.64 (~greater(sk1(sk3), equilibrium(sk3))),
% 0.37/0.64 inference(unit_resolution,[status(thm)],[432, 398])).
% 0.37/0.64 tff(434,assumption,(~greater(sk1(sk3), equilibrium(sk3))), introduced(assumption)).
% 0.37/0.64 tff(435,assumption,(greater(sk1(sk3), sk2(sk3))), introduced(assumption)).
% 0.37/0.64 tff(436,assumption,(greater(sk2(sk3), equilibrium(sk3))), introduced(assumption)).
% 0.37/0.64 tff(437,plain,
% 0.37/0.64 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | ((~greater(sk2(sk3), equilibrium(sk3))) | greater(sk1(sk3), equilibrium(sk3)) | (~greater(sk1(sk3), sk2(sk3))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (~greater(sk2(sk3), equilibrium(sk3))) | greater(sk1(sk3), equilibrium(sk3)) | (~greater(sk1(sk3), sk2(sk3))))),
% 0.37/0.64 inference(rewrite,[status(thm)],[])).
% 0.37/0.64 tff(438,plain,
% 0.37/0.64 ((greater(sk1(sk3), equilibrium(sk3)) | (~greater(sk2(sk3), equilibrium(sk3))) | (~greater(sk1(sk3), sk2(sk3)))) <=> ((~greater(sk2(sk3), equilibrium(sk3))) | greater(sk1(sk3), equilibrium(sk3)) | (~greater(sk1(sk3), sk2(sk3))))),
% 0.37/0.64 inference(rewrite,[status(thm)],[])).
% 0.37/0.64 tff(439,plain,
% 0.37/0.64 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(sk1(sk3), equilibrium(sk3)) | (~greater(sk2(sk3), equilibrium(sk3))) | (~greater(sk1(sk3), sk2(sk3))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | ((~greater(sk2(sk3), equilibrium(sk3))) | greater(sk1(sk3), equilibrium(sk3)) | (~greater(sk1(sk3), sk2(sk3)))))),
% 0.37/0.64 inference(monotonicity,[status(thm)],[438])).
% 0.37/0.64 tff(440,plain,
% 0.37/0.64 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(sk1(sk3), equilibrium(sk3)) | (~greater(sk2(sk3), equilibrium(sk3))) | (~greater(sk1(sk3), sk2(sk3))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (~greater(sk2(sk3), equilibrium(sk3))) | greater(sk1(sk3), equilibrium(sk3)) | (~greater(sk1(sk3), sk2(sk3))))),
% 0.37/0.65 inference(transitivity,[status(thm)],[439, 437])).
% 0.37/0.65 tff(441,plain,
% 0.37/0.65 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(sk1(sk3), equilibrium(sk3)) | (~greater(sk2(sk3), equilibrium(sk3))) | (~greater(sk1(sk3), sk2(sk3))))),
% 0.37/0.65 inference(quant_inst,[status(thm)],[])).
% 0.37/0.65 tff(442,plain,
% 0.37/0.65 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (~greater(sk2(sk3), equilibrium(sk3))) | greater(sk1(sk3), equilibrium(sk3)) | (~greater(sk1(sk3), sk2(sk3)))),
% 0.37/0.65 inference(modus_ponens,[status(thm)],[441, 440])).
% 0.37/0.65 tff(443,plain,
% 0.37/0.65 ($false),
% 0.37/0.65 inference(unit_resolution,[status(thm)],[442, 96, 436, 435, 434])).
% 0.37/0.65 tff(444,plain,((~greater(sk1(sk3), sk2(sk3))) | (~greater(sk2(sk3), equilibrium(sk3))) | greater(sk1(sk3), equilibrium(sk3))), inference(lemma,lemma(discharge,[]))).
% 0.37/0.65 tff(445,plain,
% 0.37/0.65 (~greater(sk2(sk3), equilibrium(sk3))),
% 0.37/0.65 inference(unit_resolution,[status(thm)],[444, 435, 434])).
% 0.37/0.65 tff(446,plain,
% 0.37/0.65 (sk2(sk3) = equilibrium(sk3)),
% 0.37/0.65 inference(unit_resolution,[status(thm)],[86, 445])).
% 0.37/0.65 tff(447,plain,
% 0.37/0.65 (greater(sk1(sk3), sk2(sk3)) <=> greater(sk1(sk3), equilibrium(sk3))),
% 0.37/0.65 inference(monotonicity,[status(thm)],[446])).
% 0.37/0.65 tff(448,plain,
% 0.37/0.65 (greater(sk1(sk3), equilibrium(sk3)) <=> greater(sk1(sk3), sk2(sk3))),
% 0.37/0.65 inference(symmetry,[status(thm)],[447])).
% 0.37/0.65 tff(449,plain,
% 0.37/0.65 ((~greater(sk1(sk3), equilibrium(sk3))) <=> (~greater(sk1(sk3), sk2(sk3)))),
% 0.37/0.65 inference(monotonicity,[status(thm)],[448])).
% 0.37/0.65 tff(450,plain,
% 0.37/0.65 (~greater(sk1(sk3), sk2(sk3))),
% 0.37/0.65 inference(modus_ponens,[status(thm)],[434, 449])).
% 0.37/0.65 tff(451,plain,
% 0.37/0.65 ($false),
% 0.37/0.65 inference(unit_resolution,[status(thm)],[435, 450])).
% 0.37/0.65 tff(452,plain,((~greater(sk1(sk3), sk2(sk3))) | greater(sk1(sk3), equilibrium(sk3))), inference(lemma,lemma(discharge,[]))).
% 0.37/0.65 tff(453,plain,
% 0.37/0.65 (~greater(sk1(sk3), sk2(sk3))),
% 0.37/0.65 inference(unit_resolution,[status(thm)],[452, 433])).
% 0.37/0.65 tff(454,assumption,(~greater(sk1(sk3), sk2(sk3))), introduced(assumption)).
% 0.37/0.65 tff(455,assumption,(~greater_or_equal(sk4(sk2(sk3)), sk1(sk3))), introduced(assumption)).
% 0.37/0.65 tff(456,assumption,(sk1(sk3) = sk2(sk3)), introduced(assumption)).
% 0.37/0.65 tff(457,plain,
% 0.37/0.65 (greater_or_equal(sk4(sk2(sk3)), sk1(sk3)) <=> greater_or_equal(sk4(sk2(sk3)), sk2(sk3))),
% 0.37/0.65 inference(monotonicity,[status(thm)],[456])).
% 0.37/0.65 tff(458,plain,
% 0.37/0.65 (greater_or_equal(sk4(sk2(sk3)), sk2(sk3)) <=> greater_or_equal(sk4(sk2(sk3)), sk1(sk3))),
% 0.37/0.65 inference(symmetry,[status(thm)],[457])).
% 0.37/0.65 tff(459,plain,
% 0.37/0.65 (greater_or_equal(sk4(sk2(sk3)), sk1(sk3))),
% 0.37/0.65 inference(modus_ponens,[status(thm)],[52, 458])).
% 0.37/0.65 tff(460,plain,
% 0.37/0.65 ($false),
% 0.37/0.65 inference(unit_resolution,[status(thm)],[455, 459])).
% 0.37/0.65 tff(461,plain,((~(sk1(sk3) = sk2(sk3))) | greater_or_equal(sk4(sk2(sk3)), sk1(sk3))), inference(lemma,lemma(discharge,[]))).
% 0.37/0.65 tff(462,plain,
% 0.37/0.65 (~(sk1(sk3) = sk2(sk3))),
% 0.37/0.65 inference(unit_resolution,[status(thm)],[461, 455])).
% 0.37/0.65 tff(463,plain,
% 0.37/0.65 (^[B: $i, A: $i, C: $i] : refl((greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B))) <=> (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B))))),
% 0.37/0.65 inference(bind,[status(th)],[])).
% 0.37/0.65 tff(464,plain,
% 0.37/0.65 (![B: $i, A: $i, C: $i] : (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B))) <=> ![B: $i, A: $i, C: $i] : (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))),
% 0.37/0.65 inference(quant_intro,[status(thm)],[463])).
% 0.37/0.65 tff(465,plain,
% 0.37/0.65 (![B: $i, A: $i, C: $i] : (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B))) <=> ![B: $i, A: $i, C: $i] : (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))),
% 0.37/0.65 inference(rewrite,[status(thm)],[])).
% 0.37/0.65 tff(466,plain,
% 0.37/0.65 (^[B: $i, A: $i, C: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite(((~in_environment(A, B)) | (~in_environment(A, C))) <=> ((~in_environment(A, C)) | (~in_environment(A, B)))), ((((~in_environment(A, B)) | (~in_environment(A, C))) | greater(C, B)) <=> (((~in_environment(A, C)) | (~in_environment(A, B))) | greater(C, B)))), rewrite((((~in_environment(A, C)) | (~in_environment(A, B))) | greater(C, B)) <=> (greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))), ((((~in_environment(A, B)) | (~in_environment(A, C))) | greater(C, B)) <=> (greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B))))), (((((~in_environment(A, B)) | (~in_environment(A, C))) | greater(C, B)) | (C = B)) <=> ((greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B))) | (C = B)))), rewrite(((greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B))) | (C = B)) <=> ((C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))), (((((~in_environment(A, B)) | (~in_environment(A, C))) | greater(C, B)) | (C = B)) <=> ((C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B))))), ((((((~in_environment(A, B)) | (~in_environment(A, C))) | greater(C, B)) | (C = B)) | greater(B, C)) <=> (((C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B))) | greater(B, C)))), rewrite((((C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B))) | greater(B, C)) <=> (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))), ((((((~in_environment(A, B)) | (~in_environment(A, C))) | greater(C, B)) | (C = B)) | greater(B, C)) <=> (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))))),
% 0.37/0.65 inference(bind,[status(th)],[])).
% 0.37/0.65 tff(467,plain,
% 0.37/0.65 (![B: $i, A: $i, C: $i] : (((((~in_environment(A, B)) | (~in_environment(A, C))) | greater(C, B)) | (C = B)) | greater(B, C)) <=> ![B: $i, A: $i, C: $i] : (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))),
% 0.37/0.65 inference(quant_intro,[status(thm)],[466])).
% 0.37/0.65 tff(468,axiom,(![B: $i, A: $i, C: $i] : (((((~in_environment(A, B)) | (~in_environment(A, C))) | greater(C, B)) | (C = B)) | greater(B, C))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp_times_in_environment_23')).
% 0.37/0.65 tff(469,plain,
% 0.37/0.65 (![B: $i, A: $i, C: $i] : (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))),
% 0.37/0.65 inference(modus_ponens,[status(thm)],[468, 467])).
% 0.37/0.65 tff(470,plain,
% 0.37/0.65 (![B: $i, A: $i, C: $i] : (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))),
% 0.37/0.65 inference(modus_ponens,[status(thm)],[469, 465])).
% 0.37/0.65 tff(471,plain,(
% 0.37/0.65 ![B: $i, A: $i, C: $i] : (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))),
% 0.37/0.65 inference(skolemize,[status(sab)],[470])).
% 0.37/0.65 tff(472,plain,
% 0.37/0.65 (![B: $i, A: $i, C: $i] : (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))),
% 0.37/0.65 inference(modus_ponens,[status(thm)],[471, 464])).
% 0.37/0.65 tff(473,plain,
% 0.37/0.65 (((~![B: $i, A: $i, C: $i] : (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))) | ((~in_environment(sk3, sk1(sk3))) | (~in_environment(sk3, sk2(sk3))) | greater(sk1(sk3), sk2(sk3)) | greater(sk2(sk3), sk1(sk3)) | (sk1(sk3) = sk2(sk3)))) <=> ((~![B: $i, A: $i, C: $i] : (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))) | (~in_environment(sk3, sk1(sk3))) | (~in_environment(sk3, sk2(sk3))) | greater(sk1(sk3), sk2(sk3)) | greater(sk2(sk3), sk1(sk3)) | (sk1(sk3) = sk2(sk3)))),
% 0.37/0.65 inference(rewrite,[status(thm)],[])).
% 0.37/0.65 tff(474,plain,
% 0.37/0.65 ((greater(sk2(sk3), sk1(sk3)) | (sk1(sk3) = sk2(sk3)) | greater(sk1(sk3), sk2(sk3)) | (~in_environment(sk3, sk1(sk3))) | (~in_environment(sk3, sk2(sk3)))) <=> ((~in_environment(sk3, sk1(sk3))) | (~in_environment(sk3, sk2(sk3))) | greater(sk1(sk3), sk2(sk3)) | greater(sk2(sk3), sk1(sk3)) | (sk1(sk3) = sk2(sk3)))),
% 0.37/0.65 inference(rewrite,[status(thm)],[])).
% 0.37/0.65 tff(475,plain,
% 0.37/0.65 (((~![B: $i, A: $i, C: $i] : (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))) | (greater(sk2(sk3), sk1(sk3)) | (sk1(sk3) = sk2(sk3)) | greater(sk1(sk3), sk2(sk3)) | (~in_environment(sk3, sk1(sk3))) | (~in_environment(sk3, sk2(sk3))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))) | ((~in_environment(sk3, sk1(sk3))) | (~in_environment(sk3, sk2(sk3))) | greater(sk1(sk3), sk2(sk3)) | greater(sk2(sk3), sk1(sk3)) | (sk1(sk3) = sk2(sk3))))),
% 0.37/0.65 inference(monotonicity,[status(thm)],[474])).
% 0.37/0.65 tff(476,plain,
% 0.37/0.65 (((~![B: $i, A: $i, C: $i] : (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))) | (greater(sk2(sk3), sk1(sk3)) | (sk1(sk3) = sk2(sk3)) | greater(sk1(sk3), sk2(sk3)) | (~in_environment(sk3, sk1(sk3))) | (~in_environment(sk3, sk2(sk3))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))) | (~in_environment(sk3, sk1(sk3))) | (~in_environment(sk3, sk2(sk3))) | greater(sk1(sk3), sk2(sk3)) | greater(sk2(sk3), sk1(sk3)) | (sk1(sk3) = sk2(sk3)))),
% 0.37/0.65 inference(transitivity,[status(thm)],[475, 473])).
% 0.37/0.65 tff(477,plain,
% 0.37/0.65 ((~![B: $i, A: $i, C: $i] : (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))) | (greater(sk2(sk3), sk1(sk3)) | (sk1(sk3) = sk2(sk3)) | greater(sk1(sk3), sk2(sk3)) | (~in_environment(sk3, sk1(sk3))) | (~in_environment(sk3, sk2(sk3))))),
% 0.37/0.65 inference(quant_inst,[status(thm)],[])).
% 0.37/0.65 tff(478,plain,
% 0.37/0.65 ((~![B: $i, A: $i, C: $i] : (greater(B, C) | (C = B) | greater(C, B) | (~in_environment(A, C)) | (~in_environment(A, B)))) | (~in_environment(sk3, sk1(sk3))) | (~in_environment(sk3, sk2(sk3))) | greater(sk1(sk3), sk2(sk3)) | greater(sk2(sk3), sk1(sk3)) | (sk1(sk3) = sk2(sk3))),
% 0.37/0.65 inference(modus_ponens,[status(thm)],[477, 476])).
% 0.37/0.65 tff(479,plain,
% 0.37/0.65 (greater(sk1(sk3), sk2(sk3)) | greater(sk2(sk3), sk1(sk3)) | (sk1(sk3) = sk2(sk3))),
% 0.37/0.65 inference(unit_resolution,[status(thm)],[478, 472, 288, 41])).
% 0.37/0.65 tff(480,plain,
% 0.37/0.65 (greater(sk2(sk3), sk1(sk3))),
% 0.37/0.65 inference(unit_resolution,[status(thm)],[479, 462, 454])).
% 0.37/0.65 tff(481,assumption,(greater(sk2(sk3), sk1(sk3))), introduced(assumption)).
% 0.37/0.65 tff(482,assumption,(~greater(sk4(sk2(sk3)), sk1(sk3))), introduced(assumption)).
% 0.37/0.65 tff(483,plain,
% 0.37/0.65 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(sk4(sk2(sk3)), sk1(sk3)) | (~greater(sk4(sk2(sk3)), sk2(sk3))) | (~greater(sk2(sk3), sk1(sk3))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(sk4(sk2(sk3)), sk1(sk3)) | (~greater(sk4(sk2(sk3)), sk2(sk3))) | (~greater(sk2(sk3), sk1(sk3))))),
% 0.37/0.65 inference(rewrite,[status(thm)],[])).
% 0.37/0.65 tff(484,plain,
% 0.37/0.65 ((greater(sk4(sk2(sk3)), sk1(sk3)) | (~greater(sk2(sk3), sk1(sk3))) | (~greater(sk4(sk2(sk3)), sk2(sk3)))) <=> (greater(sk4(sk2(sk3)), sk1(sk3)) | (~greater(sk4(sk2(sk3)), sk2(sk3))) | (~greater(sk2(sk3), sk1(sk3))))),
% 0.37/0.65 inference(rewrite,[status(thm)],[])).
% 0.37/0.65 tff(485,plain,
% 0.37/0.65 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(sk4(sk2(sk3)), sk1(sk3)) | (~greater(sk2(sk3), sk1(sk3))) | (~greater(sk4(sk2(sk3)), sk2(sk3))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(sk4(sk2(sk3)), sk1(sk3)) | (~greater(sk4(sk2(sk3)), sk2(sk3))) | (~greater(sk2(sk3), sk1(sk3)))))),
% 0.37/0.65 inference(monotonicity,[status(thm)],[484])).
% 0.37/0.65 tff(486,plain,
% 0.37/0.65 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(sk4(sk2(sk3)), sk1(sk3)) | (~greater(sk2(sk3), sk1(sk3))) | (~greater(sk4(sk2(sk3)), sk2(sk3))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(sk4(sk2(sk3)), sk1(sk3)) | (~greater(sk4(sk2(sk3)), sk2(sk3))) | (~greater(sk2(sk3), sk1(sk3))))),
% 0.37/0.66 inference(transitivity,[status(thm)],[485, 483])).
% 0.37/0.66 tff(487,plain,
% 0.37/0.66 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(sk4(sk2(sk3)), sk1(sk3)) | (~greater(sk2(sk3), sk1(sk3))) | (~greater(sk4(sk2(sk3)), sk2(sk3))))),
% 0.37/0.66 inference(quant_inst,[status(thm)],[])).
% 0.37/0.66 tff(488,plain,
% 0.37/0.66 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(sk4(sk2(sk3)), sk1(sk3)) | (~greater(sk4(sk2(sk3)), sk2(sk3))) | (~greater(sk2(sk3), sk1(sk3)))),
% 0.37/0.66 inference(modus_ponens,[status(thm)],[487, 486])).
% 0.37/0.66 tff(489,plain,
% 0.37/0.66 ($false),
% 0.37/0.66 inference(unit_resolution,[status(thm)],[488, 96, 13, 482, 481])).
% 0.37/0.66 tff(490,plain,((~greater(sk2(sk3), sk1(sk3))) | (~greater(sk4(sk2(sk3)), sk2(sk3))) | greater(sk4(sk2(sk3)), sk1(sk3))), inference(lemma,lemma(discharge,[]))).
% 0.37/0.66 tff(491,plain,
% 0.37/0.66 (greater(sk4(sk2(sk3)), sk1(sk3))),
% 0.37/0.66 inference(unit_resolution,[status(thm)],[490, 480, 13])).
% 0.37/0.66 tff(492,plain,
% 0.37/0.66 (((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | ((~greater(sk4(sk2(sk3)), sk1(sk3))) | greater_or_equal(sk4(sk2(sk3)), sk1(sk3)))) <=> ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | (~greater(sk4(sk2(sk3)), sk1(sk3))) | greater_or_equal(sk4(sk2(sk3)), sk1(sk3)))),
% 0.37/0.66 inference(rewrite,[status(thm)],[])).
% 0.37/0.66 tff(493,plain,
% 0.37/0.66 ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | ((~greater(sk4(sk2(sk3)), sk1(sk3))) | greater_or_equal(sk4(sk2(sk3)), sk1(sk3)))),
% 0.37/0.66 inference(quant_inst,[status(thm)],[])).
% 0.37/0.66 tff(494,plain,
% 0.37/0.66 ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | (~greater(sk4(sk2(sk3)), sk1(sk3))) | greater_or_equal(sk4(sk2(sk3)), sk1(sk3))),
% 0.37/0.66 inference(modus_ponens,[status(thm)],[493, 492])).
% 0.37/0.66 tff(495,plain,
% 0.37/0.66 ($false),
% 0.37/0.66 inference(unit_resolution,[status(thm)],[494, 8, 455, 491])).
% 0.37/0.66 tff(496,plain,(greater_or_equal(sk4(sk2(sk3)), sk1(sk3)) | (~greater(sk4(sk2(sk3)), sk2(sk3))) | greater(sk1(sk3), sk2(sk3))), inference(lemma,lemma(discharge,[]))).
% 0.37/0.66 tff(497,plain,
% 0.37/0.66 (~greater(sk4(sk2(sk3)), sk2(sk3))),
% 0.37/0.66 inference(unit_resolution,[status(thm)],[496, 453, 268])).
% 0.37/0.66 tff(498,plain,
% 0.37/0.66 (sk4(sk2(sk3)) = sk2(sk3)),
% 0.37/0.66 inference(unit_resolution,[status(thm)],[106, 497])).
% 0.37/0.66 tff(499,plain,
% 0.37/0.66 (greater(sk4(sk2(sk3)), sk1(sk3)) <=> greater(sk2(sk3), sk1(sk3))),
% 0.37/0.66 inference(monotonicity,[status(thm)],[498])).
% 0.37/0.66 tff(500,plain,
% 0.37/0.66 (greater(sk2(sk3), sk1(sk3)) <=> greater(sk4(sk2(sk3)), sk1(sk3))),
% 0.37/0.66 inference(symmetry,[status(thm)],[499])).
% 0.37/0.66 tff(501,plain,
% 0.37/0.66 (~(sk1(sk3) = sk2(sk3))),
% 0.37/0.66 inference(unit_resolution,[status(thm)],[461, 268])).
% 0.37/0.66 tff(502,plain,
% 0.37/0.66 (greater(sk2(sk3), sk1(sk3))),
% 0.37/0.66 inference(unit_resolution,[status(thm)],[479, 453, 501])).
% 0.37/0.66 tff(503,plain,
% 0.37/0.66 (greater(sk4(sk2(sk3)), sk1(sk3))),
% 0.37/0.66 inference(modus_ponens,[status(thm)],[502, 500])).
% 0.37/0.66 tff(504,plain,
% 0.37/0.66 (~greater(sk4(sk2(sk3)), sk1(sk3))),
% 0.37/0.66 inference(unit_resolution,[status(thm)],[494, 8, 268])).
% 0.37/0.66 tff(505,plain,
% 0.37/0.66 ($false),
% 0.37/0.66 inference(unit_resolution,[status(thm)],[504, 503])).
% 0.37/0.66 % SZS output end Proof
% 0.37/0.66 % E exiting
%------------------------------------------------------------------------------