%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : MGT026-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% Command : run_E %s %d THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:24:00 AM UTC 2026
% Result : Unsatisfiable 0.11s 0.39s
% Output : Proof 0.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT026-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.02 % Command : run_E %s %d THM
% 0.07/0.33 % Computer : n026.cluster.edu
% 0.07/0.33 % Model : x86_64 x86_64
% 0.07/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.33 % Memory : 8046.5625MB
% 0.07/0.33 % OS : Linux 6.8.0-71-generic
% 0.07/0.33 % CPULimit : 300
% 0.07/0.33 % WCLimit : 300
% 0.07/0.33 % DateTime : Mon Sep 7 12:15:44 UTC 2026
% 0.07/0.33 % CPUTime :
% 0.11/0.39 % SZS status Unsatisfiable
% 0.11/0.39 % SZS output start Proof
% 0.11/0.39 tff(greater_type, type, (
% 0.11/0.39 greater: ( $i * $i ) > $o)).
% 0.11/0.39 tff(growth_rate_type, type, (
% 0.11/0.39 growth_rate: ( $i * $i ) > $i)).
% 0.11/0.39 tff(sk2_type, type, (
% 0.11/0.39 sk2: $i)).
% 0.11/0.39 tff(first_movers_type, type, (
% 0.11/0.39 first_movers: $i)).
% 0.11/0.39 tff(efficient_producers_type, type, (
% 0.11/0.39 efficient_producers: $i)).
% 0.11/0.39 tff(subpopulations_type, type, (
% 0.11/0.39 subpopulations: ( $i * $i * $i * $i ) > $o)).
% 0.11/0.39 tff(sk1_type, type, (
% 0.11/0.39 sk1: $i)).
% 0.11/0.39 tff(zero_type, type, (
% 0.11/0.39 zero: $i)).
% 0.11/0.39 tff(cardinality_at_time_type, type, (
% 0.11/0.39 cardinality_at_time: ( $i * $i ) > $i)).
% 0.11/0.39 tff(greater_or_equal_type, type, (
% 0.11/0.39 greater_or_equal: ( $i * $i ) > $o)).
% 0.11/0.39 tff(appear_type, type, (
% 0.11/0.39 appear: ( $i * $i ) > $i)).
% 0.11/0.39 tff(critical_point_type, type, (
% 0.11/0.39 critical_point: $i > $i)).
% 0.11/0.39 tff(environment_type, type, (
% 0.11/0.39 environment: $i > $o)).
% 0.11/0.39 tff(in_environment_type, type, (
% 0.11/0.39 in_environment: ( $i * $i ) > $o)).
% 0.11/0.39 tff(subpopulation_type, type, (
% 0.11/0.39 subpopulation: ( $i * $i * $i ) > $o)).
% 0.11/0.39 tff(selection_favors_type, type, (
% 0.11/0.39 selection_favors: ( $i * $i * $i ) > $o)).
% 0.11/0.39 tff(1,assumption,(~greater(sk2, appear(efficient_producers, sk1))), introduced(assumption)).
% 0.11/0.39 tff(2,assumption,(greater(critical_point(sk1), appear(efficient_producers, sk1))), introduced(assumption)).
% 0.11/0.39 tff(3,plain,
% 0.11/0.39 (greater(sk2, critical_point(sk1)) <=> greater(sk2, critical_point(sk1))),
% 0.11/0.39 inference(rewrite,[status(thm)],[])).
% 0.11/0.39 tff(4,axiom,(greater(sk2, critical_point(sk1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove_l8_44')).
% 0.11/0.39 tff(5,plain,
% 0.11/0.39 (greater(sk2, critical_point(sk1))),
% 0.11/0.39 inference(modus_ponens,[status(thm)],[4, 3])).
% 0.11/0.39 tff(6,plain,
% 0.11/0.39 (![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.11/0.39 inference(rewrite,[status(thm)],[])).
% 0.11/0.39 tff(7,plain,
% 0.11/0.39 (![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.11/0.39 inference(rewrite,[status(thm)],[])).
% 0.11/0.39 tff(8,plain,
% 0.11/0.39 (^[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.11/0.39 inference(bind,[status(th)],[])).
% 0.11/0.39 tff(9,plain,
% 0.11/0.39 (![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.11/0.39 inference(quant_intro,[status(thm)],[8])).
% 0.11/0.39 tff(10,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_35')).
% 0.11/0.39 tff(11,plain,
% 0.11/0.39 (![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))),
% 0.11/0.39 inference(modus_ponens,[status(thm)],[10, 9])).
% 0.11/0.39 tff(12,plain,
% 0.11/0.39 (![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))),
% 0.11/0.39 inference(modus_ponens,[status(thm)],[11, 7])).
% 0.11/0.39 tff(13,plain,(
% 0.11/0.39 ![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))),
% 0.11/0.39 inference(skolemize,[status(sab)],[12])).
% 0.11/0.39 tff(14,plain,
% 0.11/0.39 (![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))),
% 0.11/0.39 inference(modus_ponens,[status(thm)],[13, 6])).
% 0.11/0.39 tff(15,plain,
% 0.11/0.39 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | ((~greater(sk2, critical_point(sk1))) | greater(sk2, appear(efficient_producers, sk1)) | (~greater(critical_point(sk1), appear(efficient_producers, sk1))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (~greater(sk2, critical_point(sk1))) | greater(sk2, appear(efficient_producers, sk1)) | (~greater(critical_point(sk1), appear(efficient_producers, sk1))))),
% 0.11/0.39 inference(rewrite,[status(thm)],[])).
% 0.11/0.39 tff(16,plain,
% 0.11/0.39 ((greater(sk2, appear(efficient_producers, sk1)) | (~greater(critical_point(sk1), appear(efficient_producers, sk1))) | (~greater(sk2, critical_point(sk1)))) <=> ((~greater(sk2, critical_point(sk1))) | greater(sk2, appear(efficient_producers, sk1)) | (~greater(critical_point(sk1), appear(efficient_producers, sk1))))),
% 0.11/0.39 inference(rewrite,[status(thm)],[])).
% 0.11/0.39 tff(17,plain,
% 0.11/0.39 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(sk2, appear(efficient_producers, sk1)) | (~greater(critical_point(sk1), appear(efficient_producers, sk1))) | (~greater(sk2, critical_point(sk1))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | ((~greater(sk2, critical_point(sk1))) | greater(sk2, appear(efficient_producers, sk1)) | (~greater(critical_point(sk1), appear(efficient_producers, sk1)))))),
% 0.11/0.39 inference(monotonicity,[status(thm)],[16])).
% 0.11/0.39 tff(18,plain,
% 0.11/0.39 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(sk2, appear(efficient_producers, sk1)) | (~greater(critical_point(sk1), appear(efficient_producers, sk1))) | (~greater(sk2, critical_point(sk1))))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (~greater(sk2, critical_point(sk1))) | greater(sk2, appear(efficient_producers, sk1)) | (~greater(critical_point(sk1), appear(efficient_producers, sk1))))),
% 0.11/0.39 inference(transitivity,[status(thm)],[17, 15])).
% 0.11/0.39 tff(19,plain,
% 0.11/0.39 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(sk2, appear(efficient_producers, sk1)) | (~greater(critical_point(sk1), appear(efficient_producers, sk1))) | (~greater(sk2, critical_point(sk1))))),
% 0.11/0.39 inference(quant_inst,[status(thm)],[])).
% 0.11/0.39 tff(20,plain,
% 0.11/0.39 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (~greater(sk2, critical_point(sk1))) | greater(sk2, appear(efficient_producers, sk1)) | (~greater(critical_point(sk1), appear(efficient_producers, sk1)))),
% 0.11/0.39 inference(modus_ponens,[status(thm)],[19, 18])).
% 0.11/0.39 tff(21,plain,
% 0.11/0.39 ($false),
% 0.11/0.39 inference(unit_resolution,[status(thm)],[20, 14, 5, 2, 1])).
% 0.11/0.39 tff(22,plain,((~greater(critical_point(sk1), appear(efficient_producers, sk1))) | greater(sk2, appear(efficient_producers, sk1))), inference(lemma,lemma(discharge,[]))).
% 0.11/0.39 tff(23,plain,
% 0.11/0.39 (~greater(critical_point(sk1), appear(efficient_producers, sk1))),
% 0.11/0.39 inference(unit_resolution,[status(thm)],[22, 1])).
% 0.11/0.39 tff(24,plain,
% 0.11/0.39 (environment(sk1) <=> environment(sk1)),
% 0.11/0.39 inference(rewrite,[status(thm)],[])).
% 0.11/0.39 tff(25,axiom,(environment(sk1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove_l8_42')).
% 0.11/0.39 tff(26,plain,
% 0.11/0.39 (environment(sk1)),
% 0.11/0.39 inference(modus_ponens,[status(thm)],[25, 24])).
% 0.11/0.39 tff(27,plain,
% 0.11/0.39 (^[A: $i] : refl(((~environment(A)) | greater_or_equal(critical_point(A), appear(efficient_producers, A))) <=> ((~environment(A)) | greater_or_equal(critical_point(A), appear(efficient_producers, A))))),
% 0.11/0.39 inference(bind,[status(th)],[])).
% 0.11/0.39 tff(28,plain,
% 0.11/0.39 (![A: $i] : ((~environment(A)) | greater_or_equal(critical_point(A), appear(efficient_producers, A))) <=> ![A: $i] : ((~environment(A)) | greater_or_equal(critical_point(A), appear(efficient_producers, A)))),
% 0.11/0.39 inference(quant_intro,[status(thm)],[27])).
% 0.11/0.39 tff(29,plain,
% 0.11/0.39 (![A: $i] : ((~environment(A)) | greater_or_equal(critical_point(A), appear(efficient_producers, A))) <=> ![A: $i] : ((~environment(A)) | greater_or_equal(critical_point(A), appear(efficient_producers, A)))),
% 0.11/0.39 inference(rewrite,[status(thm)],[])).
% 0.11/0.39 tff(30,axiom,(![A: $i] : ((~environment(A)) | greater_or_equal(critical_point(A), appear(efficient_producers, A)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp_critical_point_after_EP_34')).
% 0.11/0.39 tff(31,plain,
% 0.11/0.39 (![A: $i] : ((~environment(A)) | greater_or_equal(critical_point(A), appear(efficient_producers, A)))),
% 0.11/0.39 inference(modus_ponens,[status(thm)],[30, 29])).
% 0.11/0.39 tff(32,plain,(
% 0.11/0.39 ![A: $i] : ((~environment(A)) | greater_or_equal(critical_point(A), appear(efficient_producers, A)))),
% 0.11/0.39 inference(skolemize,[status(sab)],[31])).
% 0.11/0.39 tff(33,plain,
% 0.11/0.39 (![A: $i] : ((~environment(A)) | greater_or_equal(critical_point(A), appear(efficient_producers, A)))),
% 0.11/0.39 inference(modus_ponens,[status(thm)],[32, 28])).
% 0.11/0.39 tff(34,plain,
% 0.11/0.40 (((~![A: $i] : ((~environment(A)) | greater_or_equal(critical_point(A), appear(efficient_producers, A)))) | ((~environment(sk1)) | greater_or_equal(critical_point(sk1), appear(efficient_producers, sk1)))) <=> ((~![A: $i] : ((~environment(A)) | greater_or_equal(critical_point(A), appear(efficient_producers, A)))) | (~environment(sk1)) | greater_or_equal(critical_point(sk1), appear(efficient_producers, sk1)))),
% 0.11/0.40 inference(rewrite,[status(thm)],[])).
% 0.11/0.40 tff(35,plain,
% 0.11/0.40 ((~![A: $i] : ((~environment(A)) | greater_or_equal(critical_point(A), appear(efficient_producers, A)))) | ((~environment(sk1)) | greater_or_equal(critical_point(sk1), appear(efficient_producers, sk1)))),
% 0.11/0.40 inference(quant_inst,[status(thm)],[])).
% 0.11/0.40 tff(36,plain,
% 0.11/0.40 ((~![A: $i] : ((~environment(A)) | greater_or_equal(critical_point(A), appear(efficient_producers, A)))) | (~environment(sk1)) | greater_or_equal(critical_point(sk1), appear(efficient_producers, sk1))),
% 0.11/0.40 inference(modus_ponens,[status(thm)],[35, 34])).
% 0.11/0.40 tff(37,plain,
% 0.11/0.40 (greater_or_equal(critical_point(sk1), appear(efficient_producers, sk1))),
% 0.11/0.40 inference(unit_resolution,[status(thm)],[36, 33, 26])).
% 0.11/0.40 tff(38,plain,
% 0.11/0.40 (^[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.11/0.40 inference(bind,[status(th)],[])).
% 0.11/0.40 tff(39,plain,
% 0.11/0.40 (![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.11/0.40 inference(quant_intro,[status(thm)],[38])).
% 0.11/0.40 tff(40,plain,
% 0.11/0.40 (![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.11/0.40 inference(rewrite,[status(thm)],[])).
% 0.11/0.40 tff(41,plain,
% 0.11/0.40 (^[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.11/0.40 inference(bind,[status(th)],[])).
% 0.11/0.40 tff(42,plain,
% 0.11/0.40 (![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.11/0.40 inference(quant_intro,[status(thm)],[41])).
% 0.11/0.40 tff(43,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_36')).
% 0.11/0.40 tff(44,plain,
% 0.11/0.40 (![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))),
% 0.11/0.40 inference(modus_ponens,[status(thm)],[43, 42])).
% 0.11/0.40 tff(45,plain,
% 0.11/0.40 (![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))),
% 0.11/0.40 inference(modus_ponens,[status(thm)],[44, 40])).
% 0.11/0.40 tff(46,plain,(
% 0.11/0.40 ![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))),
% 0.11/0.40 inference(skolemize,[status(sab)],[45])).
% 0.11/0.40 tff(47,plain,
% 0.11/0.40 (![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))),
% 0.11/0.40 inference(modus_ponens,[status(thm)],[46, 39])).
% 0.11/0.40 tff(48,plain,
% 0.11/0.40 (((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((~greater_or_equal(critical_point(sk1), appear(efficient_producers, sk1))) | (critical_point(sk1) = appear(efficient_producers, sk1)) | greater(critical_point(sk1), appear(efficient_producers, sk1)))) <=> ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | (~greater_or_equal(critical_point(sk1), appear(efficient_producers, sk1))) | (critical_point(sk1) = appear(efficient_producers, sk1)) | greater(critical_point(sk1), appear(efficient_producers, sk1)))),
% 0.11/0.40 inference(rewrite,[status(thm)],[])).
% 0.11/0.40 tff(49,plain,
% 0.11/0.40 (((critical_point(sk1) = appear(efficient_producers, sk1)) | greater(critical_point(sk1), appear(efficient_producers, sk1)) | (~greater_or_equal(critical_point(sk1), appear(efficient_producers, sk1)))) <=> ((~greater_or_equal(critical_point(sk1), appear(efficient_producers, sk1))) | (critical_point(sk1) = appear(efficient_producers, sk1)) | greater(critical_point(sk1), appear(efficient_producers, sk1)))),
% 0.11/0.40 inference(rewrite,[status(thm)],[])).
% 0.11/0.40 tff(50,plain,
% 0.11/0.40 (((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((critical_point(sk1) = appear(efficient_producers, sk1)) | greater(critical_point(sk1), appear(efficient_producers, sk1)) | (~greater_or_equal(critical_point(sk1), appear(efficient_producers, sk1))))) <=> ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((~greater_or_equal(critical_point(sk1), appear(efficient_producers, sk1))) | (critical_point(sk1) = appear(efficient_producers, sk1)) | greater(critical_point(sk1), appear(efficient_producers, sk1))))),
% 0.11/0.40 inference(monotonicity,[status(thm)],[49])).
% 0.11/0.40 tff(51,plain,
% 0.11/0.40 (((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((critical_point(sk1) = appear(efficient_producers, sk1)) | greater(critical_point(sk1), appear(efficient_producers, sk1)) | (~greater_or_equal(critical_point(sk1), appear(efficient_producers, sk1))))) <=> ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | (~greater_or_equal(critical_point(sk1), appear(efficient_producers, sk1))) | (critical_point(sk1) = appear(efficient_producers, sk1)) | greater(critical_point(sk1), appear(efficient_producers, sk1)))),
% 0.11/0.40 inference(transitivity,[status(thm)],[50, 48])).
% 0.11/0.40 tff(52,plain,
% 0.11/0.40 ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((critical_point(sk1) = appear(efficient_producers, sk1)) | greater(critical_point(sk1), appear(efficient_producers, sk1)) | (~greater_or_equal(critical_point(sk1), appear(efficient_producers, sk1))))),
% 0.11/0.40 inference(quant_inst,[status(thm)],[])).
% 0.11/0.40 tff(53,plain,
% 0.11/0.40 ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | (~greater_or_equal(critical_point(sk1), appear(efficient_producers, sk1))) | (critical_point(sk1) = appear(efficient_producers, sk1)) | greater(critical_point(sk1), appear(efficient_producers, sk1))),
% 0.11/0.40 inference(modus_ponens,[status(thm)],[52, 51])).
% 0.11/0.40 tff(54,plain,
% 0.11/0.40 ((critical_point(sk1) = appear(efficient_producers, sk1)) | greater(critical_point(sk1), appear(efficient_producers, sk1))),
% 0.11/0.40 inference(unit_resolution,[status(thm)],[53, 47, 37])).
% 0.11/0.40 tff(55,plain,
% 0.11/0.40 (critical_point(sk1) = appear(efficient_producers, sk1)),
% 0.11/0.40 inference(unit_resolution,[status(thm)],[54, 23])).
% 0.11/0.40 tff(56,plain,
% 0.11/0.40 (greater(sk2, critical_point(sk1)) <=> greater(sk2, appear(efficient_producers, sk1))),
% 0.11/0.40 inference(monotonicity,[status(thm)],[55])).
% 0.11/0.40 tff(57,plain,
% 0.11/0.40 (greater(sk2, appear(efficient_producers, sk1)) <=> greater(sk2, critical_point(sk1))),
% 0.11/0.40 inference(symmetry,[status(thm)],[56])).
% 0.11/0.40 tff(58,plain,
% 0.11/0.40 ((~greater(sk2, appear(efficient_producers, sk1))) <=> (~greater(sk2, critical_point(sk1)))),
% 0.11/0.40 inference(monotonicity,[status(thm)],[57])).
% 0.11/0.40 tff(59,plain,
% 0.11/0.40 (~greater(sk2, critical_point(sk1))),
% 0.11/0.40 inference(modus_ponens,[status(thm)],[1, 58])).
% 0.11/0.40 tff(60,plain,
% 0.11/0.40 ($false),
% 0.11/0.40 inference(unit_resolution,[status(thm)],[5, 59])).
% 0.11/0.40 tff(61,plain,(greater(sk2, appear(efficient_producers, sk1))), inference(lemma,lemma(discharge,[]))).
% 0.11/0.40 tff(62,plain,
% 0.11/0.40 (^[B: $i, A: $i] : refl(((~greater(A, B)) | greater_or_equal(A, B)) <=> ((~greater(A, B)) | greater_or_equal(A, B)))),
% 0.11/0.40 inference(bind,[status(th)],[])).
% 0.11/0.40 tff(63,plain,
% 0.11/0.40 (![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.11/0.40 inference(quant_intro,[status(thm)],[62])).
% 0.11/0.40 tff(64,plain,
% 0.11/0.40 (![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.11/0.40 inference(rewrite,[status(thm)],[])).
% 0.11/0.40 tff(65,axiom,(![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp_greater_or_equal_37')).
% 0.11/0.40 tff(66,plain,
% 0.11/0.40 (![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))),
% 0.11/0.40 inference(modus_ponens,[status(thm)],[65, 64])).
% 0.11/0.40 tff(67,plain,(
% 0.11/0.40 ![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))),
% 0.11/0.40 inference(skolemize,[status(sab)],[66])).
% 0.11/0.40 tff(68,plain,
% 0.11/0.40 (![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))),
% 0.11/0.40 inference(modus_ponens,[status(thm)],[67, 63])).
% 0.11/0.40 tff(69,plain,
% 0.11/0.40 (((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | ((~greater(sk2, appear(efficient_producers, sk1))) | greater_or_equal(sk2, appear(efficient_producers, sk1)))) <=> ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | (~greater(sk2, appear(efficient_producers, sk1))) | greater_or_equal(sk2, appear(efficient_producers, sk1)))),
% 0.11/0.40 inference(rewrite,[status(thm)],[])).
% 0.11/0.40 tff(70,plain,
% 0.11/0.40 ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | ((~greater(sk2, appear(efficient_producers, sk1))) | greater_or_equal(sk2, appear(efficient_producers, sk1)))),
% 0.11/0.40 inference(quant_inst,[status(thm)],[])).
% 0.11/0.40 tff(71,plain,
% 0.11/0.40 ((~![B: $i, A: $i] : ((~greater(A, B)) | greater_or_equal(A, B))) | (~greater(sk2, appear(efficient_producers, sk1))) | greater_or_equal(sk2, appear(efficient_producers, sk1))),
% 0.11/0.40 inference(modus_ponens,[status(thm)],[70, 69])).
% 0.11/0.40 tff(72,plain,
% 0.11/0.40 (greater_or_equal(sk2, appear(efficient_producers, sk1))),
% 0.11/0.40 inference(unit_resolution,[status(thm)],[71, 68, 61])).
% 0.11/0.40 tff(73,plain,
% 0.11/0.40 (in_environment(sk1, sk2) <=> in_environment(sk1, sk2)),
% 0.11/0.40 inference(rewrite,[status(thm)],[])).
% 0.11/0.40 tff(74,axiom,(in_environment(sk1, sk2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove_l8_43')).
% 0.11/0.40 tff(75,plain,
% 0.11/0.40 (in_environment(sk1, sk2)),
% 0.11/0.40 inference(modus_ponens,[status(thm)],[74, 73])).
% 0.11/0.40 tff(76,plain,
% 0.11/0.40 (^[B: $i, A: $i] : refl((greater(cardinality_at_time(efficient_producers, B), zero) | (~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A)))) <=> (greater(cardinality_at_time(efficient_producers, B), zero) | (~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A)))))),
% 0.11/0.40 inference(bind,[status(th)],[])).
% 0.11/0.40 tff(77,plain,
% 0.11/0.40 (![B: $i, A: $i] : (greater(cardinality_at_time(efficient_producers, B), zero) | (~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A)))) <=> ![B: $i, A: $i] : (greater(cardinality_at_time(efficient_producers, B), zero) | (~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A))))),
% 0.11/0.40 inference(quant_intro,[status(thm)],[76])).
% 0.11/0.40 tff(78,plain,
% 0.11/0.40 (![B: $i, A: $i] : (greater(cardinality_at_time(efficient_producers, B), zero) | (~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A)))) <=> ![B: $i, A: $i] : (greater(cardinality_at_time(efficient_producers, B), zero) | (~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A))))),
% 0.11/0.40 inference(rewrite,[status(thm)],[])).
% 0.11/0.40 tff(79,plain,
% 0.11/0.40 (^[B: $i, A: $i] : trans(monotonicity(rewrite((((~environment(A)) | (~in_environment(A, B))) | (~greater_or_equal(B, appear(efficient_producers, A)))) <=> ((~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A))))), (((((~environment(A)) | (~in_environment(A, B))) | (~greater_or_equal(B, appear(efficient_producers, A)))) | greater(cardinality_at_time(efficient_producers, B), zero)) <=> (((~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A)))) | greater(cardinality_at_time(efficient_producers, B), zero)))), rewrite((((~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A)))) | greater(cardinality_at_time(efficient_producers, B), zero)) <=> (greater(cardinality_at_time(efficient_producers, B), zero) | (~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A))))), (((((~environment(A)) | (~in_environment(A, B))) | (~greater_or_equal(B, appear(efficient_producers, A)))) | greater(cardinality_at_time(efficient_producers, B), zero)) <=> (greater(cardinality_at_time(efficient_producers, B), zero) | (~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A))))))),
% 0.11/0.40 inference(bind,[status(th)],[])).
% 0.11/0.40 tff(80,plain,
% 0.11/0.40 (![B: $i, A: $i] : ((((~environment(A)) | (~in_environment(A, B))) | (~greater_or_equal(B, appear(efficient_producers, A)))) | greater(cardinality_at_time(efficient_producers, B), zero)) <=> ![B: $i, A: $i] : (greater(cardinality_at_time(efficient_producers, B), zero) | (~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A))))),
% 0.11/0.40 inference(quant_intro,[status(thm)],[79])).
% 0.11/0.40 tff(81,axiom,(![B: $i, A: $i] : ((((~environment(A)) | (~in_environment(A, B))) | (~greater_or_equal(B, appear(efficient_producers, A)))) | greater(cardinality_at_time(efficient_producers, B), zero))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t6_41')).
% 0.11/0.40 tff(82,plain,
% 0.11/0.40 (![B: $i, A: $i] : (greater(cardinality_at_time(efficient_producers, B), zero) | (~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A))))),
% 0.11/0.40 inference(modus_ponens,[status(thm)],[81, 80])).
% 0.11/0.40 tff(83,plain,
% 0.11/0.40 (![B: $i, A: $i] : (greater(cardinality_at_time(efficient_producers, B), zero) | (~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A))))),
% 0.11/0.40 inference(modus_ponens,[status(thm)],[82, 78])).
% 0.11/0.40 tff(84,plain,(
% 0.11/0.40 ![B: $i, A: $i] : (greater(cardinality_at_time(efficient_producers, B), zero) | (~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A))))),
% 0.11/0.40 inference(skolemize,[status(sab)],[83])).
% 0.11/0.40 tff(85,plain,
% 0.11/0.40 (![B: $i, A: $i] : (greater(cardinality_at_time(efficient_producers, B), zero) | (~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A))))),
% 0.11/0.40 inference(modus_ponens,[status(thm)],[84, 77])).
% 0.11/0.40 tff(86,plain,
% 0.11/0.40 (((~![B: $i, A: $i] : (greater(cardinality_at_time(efficient_producers, B), zero) | (~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A))))) | (greater(cardinality_at_time(efficient_producers, sk2), zero) | (~in_environment(sk1, sk2)) | (~environment(sk1)) | (~greater_or_equal(sk2, appear(efficient_producers, sk1))))) <=> ((~![B: $i, A: $i] : (greater(cardinality_at_time(efficient_producers, B), zero) | (~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A))))) | greater(cardinality_at_time(efficient_producers, sk2), zero) | (~in_environment(sk1, sk2)) | (~environment(sk1)) | (~greater_or_equal(sk2, appear(efficient_producers, sk1))))),
% 0.11/0.40 inference(rewrite,[status(thm)],[])).
% 0.11/0.40 tff(87,plain,
% 0.11/0.40 ((~![B: $i, A: $i] : (greater(cardinality_at_time(efficient_producers, B), zero) | (~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A))))) | (greater(cardinality_at_time(efficient_producers, sk2), zero) | (~in_environment(sk1, sk2)) | (~environment(sk1)) | (~greater_or_equal(sk2, appear(efficient_producers, sk1))))),
% 0.11/0.40 inference(quant_inst,[status(thm)],[])).
% 0.11/0.40 tff(88,plain,
% 0.11/0.40 ((~![B: $i, A: $i] : (greater(cardinality_at_time(efficient_producers, B), zero) | (~in_environment(A, B)) | (~environment(A)) | (~greater_or_equal(B, appear(efficient_producers, A))))) | greater(cardinality_at_time(efficient_producers, sk2), zero) | (~in_environment(sk1, sk2)) | (~environment(sk1)) | (~greater_or_equal(sk2, appear(efficient_producers, sk1)))),
% 0.11/0.40 inference(modus_ponens,[status(thm)],[87, 86])).
% 0.11/0.40 tff(89,plain,
% 0.11/0.40 (greater(cardinality_at_time(efficient_producers, sk2), zero) | (~greater_or_equal(sk2, appear(efficient_producers, sk1)))),
% 0.11/0.40 inference(unit_resolution,[status(thm)],[88, 85, 26, 75])).
% 0.11/0.40 tff(90,plain,
% 0.11/0.40 (greater(cardinality_at_time(efficient_producers, sk2), zero)),
% 0.11/0.40 inference(unit_resolution,[status(thm)],[89, 72])).
% 0.11/0.40 tff(91,plain,
% 0.11/0.40 (^[B: $i, A: $i] : refl((subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A))) <=> (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A))))),
% 0.11/0.40 inference(bind,[status(th)],[])).
% 0.11/0.40 tff(92,plain,
% 0.11/0.40 (![B: $i, A: $i] : (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A))) <=> ![B: $i, A: $i] : (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.40 inference(quant_intro,[status(thm)],[91])).
% 0.11/0.40 tff(93,plain,
% 0.11/0.40 (![B: $i, A: $i] : (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A))) <=> ![B: $i, A: $i] : (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.40 inference(rewrite,[status(thm)],[])).
% 0.11/0.40 tff(94,plain,
% 0.11/0.40 (^[B: $i, A: $i] : rewrite((((~environment(A)) | (~in_environment(A, B))) | subpopulation(first_movers, A, B)) <=> (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A))))),
% 0.11/0.40 inference(bind,[status(th)],[])).
% 0.11/0.40 tff(95,plain,
% 0.11/0.40 (![B: $i, A: $i] : (((~environment(A)) | (~in_environment(A, B))) | subpopulation(first_movers, A, B)) <=> ![B: $i, A: $i] : (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.40 inference(quant_intro,[status(thm)],[94])).
% 0.11/0.40 tff(96,axiom,(![B: $i, A: $i] : (((~environment(A)) | (~in_environment(A, B))) | subpopulation(first_movers, A, B))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp_subpopulations_32')).
% 0.11/0.40 tff(97,plain,
% 0.11/0.40 (![B: $i, A: $i] : (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.40 inference(modus_ponens,[status(thm)],[96, 95])).
% 0.11/0.40 tff(98,plain,
% 0.11/0.40 (![B: $i, A: $i] : (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.40 inference(modus_ponens,[status(thm)],[97, 93])).
% 0.11/0.40 tff(99,plain,(
% 0.11/0.40 ![B: $i, A: $i] : (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.40 inference(skolemize,[status(sab)],[98])).
% 0.11/0.40 tff(100,plain,
% 0.11/0.40 (![B: $i, A: $i] : (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.40 inference(modus_ponens,[status(thm)],[99, 92])).
% 0.11/0.40 tff(101,plain,
% 0.11/0.40 (((~![B: $i, A: $i] : (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A)))) | ((~in_environment(sk1, sk2)) | (~environment(sk1)) | subpopulation(first_movers, sk1, sk2))) <=> ((~![B: $i, A: $i] : (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A)))) | (~in_environment(sk1, sk2)) | (~environment(sk1)) | subpopulation(first_movers, sk1, sk2))),
% 0.11/0.40 inference(rewrite,[status(thm)],[])).
% 0.11/0.40 tff(102,plain,
% 0.11/0.40 ((subpopulation(first_movers, sk1, sk2) | (~in_environment(sk1, sk2)) | (~environment(sk1))) <=> ((~in_environment(sk1, sk2)) | (~environment(sk1)) | subpopulation(first_movers, sk1, sk2))),
% 0.11/0.40 inference(rewrite,[status(thm)],[])).
% 0.11/0.40 tff(103,plain,
% 0.11/0.40 (((~![B: $i, A: $i] : (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A)))) | (subpopulation(first_movers, sk1, sk2) | (~in_environment(sk1, sk2)) | (~environment(sk1)))) <=> ((~![B: $i, A: $i] : (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A)))) | ((~in_environment(sk1, sk2)) | (~environment(sk1)) | subpopulation(first_movers, sk1, sk2)))),
% 0.11/0.40 inference(monotonicity,[status(thm)],[102])).
% 0.11/0.40 tff(104,plain,
% 0.11/0.40 (((~![B: $i, A: $i] : (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A)))) | (subpopulation(first_movers, sk1, sk2) | (~in_environment(sk1, sk2)) | (~environment(sk1)))) <=> ((~![B: $i, A: $i] : (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A)))) | (~in_environment(sk1, sk2)) | (~environment(sk1)) | subpopulation(first_movers, sk1, sk2))),
% 0.11/0.40 inference(transitivity,[status(thm)],[103, 101])).
% 0.11/0.40 tff(105,plain,
% 0.11/0.40 ((~![B: $i, A: $i] : (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A)))) | (subpopulation(first_movers, sk1, sk2) | (~in_environment(sk1, sk2)) | (~environment(sk1)))),
% 0.11/0.40 inference(quant_inst,[status(thm)],[])).
% 0.11/0.40 tff(106,plain,
% 0.11/0.40 ((~![B: $i, A: $i] : (subpopulation(first_movers, A, B) | (~in_environment(A, B)) | (~environment(A)))) | (~in_environment(sk1, sk2)) | (~environment(sk1)) | subpopulation(first_movers, sk1, sk2)),
% 0.11/0.40 inference(modus_ponens,[status(thm)],[105, 104])).
% 0.11/0.40 tff(107,plain,
% 0.11/0.40 (subpopulation(first_movers, sk1, sk2)),
% 0.11/0.40 inference(unit_resolution,[status(thm)],[106, 100, 26, 75])).
% 0.11/0.41 tff(108,plain,
% 0.11/0.41 (^[B: $i, A: $i] : refl((subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A))) <=> (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A))))),
% 0.11/0.41 inference(bind,[status(th)],[])).
% 0.11/0.41 tff(109,plain,
% 0.11/0.41 (![B: $i, A: $i] : (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A))) <=> ![B: $i, A: $i] : (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.41 inference(quant_intro,[status(thm)],[108])).
% 0.11/0.41 tff(110,plain,
% 0.11/0.41 (![B: $i, A: $i] : (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A))) <=> ![B: $i, A: $i] : (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.41 inference(rewrite,[status(thm)],[])).
% 0.11/0.41 tff(111,plain,
% 0.11/0.41 (^[B: $i, A: $i] : rewrite((((~environment(A)) | (~in_environment(A, B))) | subpopulation(efficient_producers, A, B)) <=> (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A))))),
% 0.11/0.41 inference(bind,[status(th)],[])).
% 0.11/0.41 tff(112,plain,
% 0.11/0.41 (![B: $i, A: $i] : (((~environment(A)) | (~in_environment(A, B))) | subpopulation(efficient_producers, A, B)) <=> ![B: $i, A: $i] : (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.41 inference(quant_intro,[status(thm)],[111])).
% 0.11/0.41 tff(113,axiom,(![B: $i, A: $i] : (((~environment(A)) | (~in_environment(A, B))) | subpopulation(efficient_producers, A, B))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp_subpopulations_33')).
% 0.11/0.41 tff(114,plain,
% 0.11/0.41 (![B: $i, A: $i] : (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.41 inference(modus_ponens,[status(thm)],[113, 112])).
% 0.11/0.41 tff(115,plain,
% 0.11/0.41 (![B: $i, A: $i] : (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.41 inference(modus_ponens,[status(thm)],[114, 110])).
% 0.11/0.41 tff(116,plain,(
% 0.11/0.41 ![B: $i, A: $i] : (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.41 inference(skolemize,[status(sab)],[115])).
% 0.11/0.41 tff(117,plain,
% 0.11/0.41 (![B: $i, A: $i] : (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.41 inference(modus_ponens,[status(thm)],[116, 109])).
% 0.11/0.41 tff(118,plain,
% 0.11/0.41 (((~![B: $i, A: $i] : (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A)))) | ((~in_environment(sk1, sk2)) | (~environment(sk1)) | subpopulation(efficient_producers, sk1, sk2))) <=> ((~![B: $i, A: $i] : (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A)))) | (~in_environment(sk1, sk2)) | (~environment(sk1)) | subpopulation(efficient_producers, sk1, sk2))),
% 0.11/0.41 inference(rewrite,[status(thm)],[])).
% 0.11/0.41 tff(119,plain,
% 0.11/0.41 ((subpopulation(efficient_producers, sk1, sk2) | (~in_environment(sk1, sk2)) | (~environment(sk1))) <=> ((~in_environment(sk1, sk2)) | (~environment(sk1)) | subpopulation(efficient_producers, sk1, sk2))),
% 0.11/0.41 inference(rewrite,[status(thm)],[])).
% 0.11/0.41 tff(120,plain,
% 0.11/0.41 (((~![B: $i, A: $i] : (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A)))) | (subpopulation(efficient_producers, sk1, sk2) | (~in_environment(sk1, sk2)) | (~environment(sk1)))) <=> ((~![B: $i, A: $i] : (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A)))) | ((~in_environment(sk1, sk2)) | (~environment(sk1)) | subpopulation(efficient_producers, sk1, sk2)))),
% 0.11/0.41 inference(monotonicity,[status(thm)],[119])).
% 0.11/0.41 tff(121,plain,
% 0.11/0.41 (((~![B: $i, A: $i] : (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A)))) | (subpopulation(efficient_producers, sk1, sk2) | (~in_environment(sk1, sk2)) | (~environment(sk1)))) <=> ((~![B: $i, A: $i] : (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A)))) | (~in_environment(sk1, sk2)) | (~environment(sk1)) | subpopulation(efficient_producers, sk1, sk2))),
% 0.11/0.41 inference(transitivity,[status(thm)],[120, 118])).
% 0.11/0.41 tff(122,plain,
% 0.11/0.41 ((~![B: $i, A: $i] : (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A)))) | (subpopulation(efficient_producers, sk1, sk2) | (~in_environment(sk1, sk2)) | (~environment(sk1)))),
% 0.11/0.41 inference(quant_inst,[status(thm)],[])).
% 0.11/0.41 tff(123,plain,
% 0.11/0.41 ((~![B: $i, A: $i] : (subpopulation(efficient_producers, A, B) | (~in_environment(A, B)) | (~environment(A)))) | (~in_environment(sk1, sk2)) | (~environment(sk1)) | subpopulation(efficient_producers, sk1, sk2)),
% 0.11/0.41 inference(modus_ponens,[status(thm)],[122, 121])).
% 0.11/0.41 tff(124,plain,
% 0.11/0.41 (subpopulation(efficient_producers, sk1, sk2)),
% 0.11/0.41 inference(unit_resolution,[status(thm)],[123, 117, 26, 75])).
% 0.11/0.41 tff(125,plain,
% 0.11/0.41 ((~selection_favors(efficient_producers, first_movers, sk2)) <=> (~selection_favors(efficient_producers, first_movers, sk2))),
% 0.11/0.41 inference(rewrite,[status(thm)],[])).
% 0.11/0.41 tff(126,axiom,(~selection_favors(efficient_producers, first_movers, sk2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove_l8_45')).
% 0.11/0.41 tff(127,plain,
% 0.11/0.41 (~selection_favors(efficient_producers, first_movers, sk2)),
% 0.11/0.41 inference(modus_ponens,[status(thm)],[126, 125])).
% 0.11/0.41 tff(128,plain,
% 0.11/0.41 (^[B: $i, D: $i, A: $i, C: $i] : refl(((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C))) <=> ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C))))),
% 0.11/0.41 inference(bind,[status(th)],[])).
% 0.11/0.41 tff(129,plain,
% 0.11/0.41 (![B: $i, D: $i, A: $i, C: $i] : ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C))) <=> ![B: $i, D: $i, A: $i, C: $i] : ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))),
% 0.11/0.41 inference(quant_intro,[status(thm)],[128])).
% 0.11/0.41 tff(130,plain,
% 0.11/0.41 (![B: $i, D: $i, A: $i, C: $i] : ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C))) <=> ![B: $i, D: $i, A: $i, C: $i] : ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))),
% 0.11/0.41 inference(rewrite,[status(thm)],[])).
% 0.11/0.41 tff(131,plain,
% 0.11/0.41 (^[B: $i, D: $i, A: $i, C: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite((((~environment(A)) | (~subpopulation(B, A, C))) | (~subpopulation(D, A, C))) <=> ((~environment(A)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))), (((((~environment(A)) | (~subpopulation(B, A, C))) | (~subpopulation(D, A, C))) | (~greater(cardinality_at_time(B, C), zero))) <=> (((~environment(A)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C))) | (~greater(cardinality_at_time(B, C), zero))))), rewrite((((~environment(A)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C))) | (~greater(cardinality_at_time(B, C), zero))) <=> ((~environment(A)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))), (((((~environment(A)) | (~subpopulation(B, A, C))) | (~subpopulation(D, A, C))) | (~greater(cardinality_at_time(B, C), zero))) <=> ((~environment(A)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C))))), ((((((~environment(A)) | (~subpopulation(B, A, C))) | (~subpopulation(D, A, C))) | (~greater(cardinality_at_time(B, C), zero))) | (~(cardinality_at_time(D, C) = zero))) <=> (((~environment(A)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C))) | (~(cardinality_at_time(D, C) = zero))))), rewrite((((~environment(A)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C))) | (~(cardinality_at_time(D, C) = zero))) <=> ((~environment(A)) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))), ((((((~environment(A)) | (~subpopulation(B, A, C))) | (~subpopulation(D, A, C))) | (~greater(cardinality_at_time(B, C), zero))) | (~(cardinality_at_time(D, C) = zero))) <=> ((~environment(A)) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C))))), (((((((~environment(A)) | (~subpopulation(B, A, C))) | (~subpopulation(D, A, C))) | (~greater(cardinality_at_time(B, C), zero))) | (~(cardinality_at_time(D, C) = zero))) | selection_favors(B, D, C)) <=> (((~environment(A)) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C))) | selection_favors(B, D, C)))), rewrite((((~environment(A)) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C))) | selection_favors(B, D, C)) <=> ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))), (((((((~environment(A)) | (~subpopulation(B, A, C))) | (~subpopulation(D, A, C))) | (~greater(cardinality_at_time(B, C), zero))) | (~(cardinality_at_time(D, C) = zero))) | selection_favors(B, D, C)) <=> ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))))),
% 0.11/0.41 inference(bind,[status(th)],[])).
% 0.11/0.41 tff(132,plain,
% 0.11/0.41 (![B: $i, D: $i, A: $i, C: $i] : ((((((~environment(A)) | (~subpopulation(B, A, C))) | (~subpopulation(D, A, C))) | (~greater(cardinality_at_time(B, C), zero))) | (~(cardinality_at_time(D, C) = zero))) | selection_favors(B, D, C)) <=> ![B: $i, D: $i, A: $i, C: $i] : ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))),
% 0.11/0.41 inference(quant_intro,[status(thm)],[131])).
% 0.11/0.41 tff(133,axiom,(![B: $i, D: $i, A: $i, C: $i] : ((((((~environment(A)) | (~subpopulation(B, A, C))) | (~subpopulation(D, A, C))) | (~greater(cardinality_at_time(B, C), zero))) | (~(cardinality_at_time(D, C) = zero))) | selection_favors(B, D, C))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp2_favour_members_29')).
% 0.11/0.41 tff(134,plain,
% 0.11/0.41 (![B: $i, D: $i, A: $i, C: $i] : ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))),
% 0.11/0.41 inference(modus_ponens,[status(thm)],[133, 132])).
% 0.11/0.41 tff(135,plain,
% 0.11/0.41 (![B: $i, D: $i, A: $i, C: $i] : ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))),
% 0.11/0.41 inference(modus_ponens,[status(thm)],[134, 130])).
% 0.11/0.41 tff(136,plain,(
% 0.11/0.41 ![B: $i, D: $i, A: $i, C: $i] : ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))),
% 0.11/0.41 inference(skolemize,[status(sab)],[135])).
% 0.11/0.41 tff(137,plain,
% 0.11/0.41 (![B: $i, D: $i, A: $i, C: $i] : ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))),
% 0.11/0.41 inference(modus_ponens,[status(thm)],[136, 129])).
% 0.11/0.41 tff(138,plain,
% 0.11/0.41 (((~![B: $i, D: $i, A: $i, C: $i] : ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))) | (selection_favors(efficient_producers, first_movers, sk2) | (~environment(sk1)) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~(cardinality_at_time(first_movers, sk2) = zero)) | (~subpopulation(first_movers, sk1, sk2)) | (~subpopulation(efficient_producers, sk1, sk2)))) <=> ((~![B: $i, D: $i, A: $i, C: $i] : ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))) | selection_favors(efficient_producers, first_movers, sk2) | (~environment(sk1)) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~(cardinality_at_time(first_movers, sk2) = zero)) | (~subpopulation(first_movers, sk1, sk2)) | (~subpopulation(efficient_producers, sk1, sk2)))),
% 0.11/0.41 inference(rewrite,[status(thm)],[])).
% 0.11/0.41 tff(139,plain,
% 0.11/0.41 (((~environment(sk1)) | selection_favors(efficient_producers, first_movers, sk2) | (~(cardinality_at_time(first_movers, sk2) = zero)) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~subpopulation(first_movers, sk1, sk2)) | (~subpopulation(efficient_producers, sk1, sk2))) <=> (selection_favors(efficient_producers, first_movers, sk2) | (~environment(sk1)) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~(cardinality_at_time(first_movers, sk2) = zero)) | (~subpopulation(first_movers, sk1, sk2)) | (~subpopulation(efficient_producers, sk1, sk2)))),
% 0.11/0.41 inference(rewrite,[status(thm)],[])).
% 0.11/0.41 tff(140,plain,
% 0.11/0.41 (((~![B: $i, D: $i, A: $i, C: $i] : ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))) | ((~environment(sk1)) | selection_favors(efficient_producers, first_movers, sk2) | (~(cardinality_at_time(first_movers, sk2) = zero)) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~subpopulation(first_movers, sk1, sk2)) | (~subpopulation(efficient_producers, sk1, sk2)))) <=> ((~![B: $i, D: $i, A: $i, C: $i] : ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))) | (selection_favors(efficient_producers, first_movers, sk2) | (~environment(sk1)) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~(cardinality_at_time(first_movers, sk2) = zero)) | (~subpopulation(first_movers, sk1, sk2)) | (~subpopulation(efficient_producers, sk1, sk2))))),
% 0.11/0.41 inference(monotonicity,[status(thm)],[139])).
% 0.11/0.41 tff(141,plain,
% 0.11/0.41 (((~![B: $i, D: $i, A: $i, C: $i] : ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))) | ((~environment(sk1)) | selection_favors(efficient_producers, first_movers, sk2) | (~(cardinality_at_time(first_movers, sk2) = zero)) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~subpopulation(first_movers, sk1, sk2)) | (~subpopulation(efficient_producers, sk1, sk2)))) <=> ((~![B: $i, D: $i, A: $i, C: $i] : ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))) | selection_favors(efficient_producers, first_movers, sk2) | (~environment(sk1)) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~(cardinality_at_time(first_movers, sk2) = zero)) | (~subpopulation(first_movers, sk1, sk2)) | (~subpopulation(efficient_producers, sk1, sk2)))),
% 0.11/0.41 inference(transitivity,[status(thm)],[140, 138])).
% 0.11/0.41 tff(142,plain,
% 0.11/0.41 ((~![B: $i, D: $i, A: $i, C: $i] : ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))) | ((~environment(sk1)) | selection_favors(efficient_producers, first_movers, sk2) | (~(cardinality_at_time(first_movers, sk2) = zero)) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~subpopulation(first_movers, sk1, sk2)) | (~subpopulation(efficient_producers, sk1, sk2)))),
% 0.11/0.41 inference(quant_inst,[status(thm)],[])).
% 0.11/0.41 tff(143,plain,
% 0.11/0.41 ((~![B: $i, D: $i, A: $i, C: $i] : ((~environment(A)) | selection_favors(B, D, C) | (~(cardinality_at_time(D, C) = zero)) | (~greater(cardinality_at_time(B, C), zero)) | (~subpopulation(D, A, C)) | (~subpopulation(B, A, C)))) | selection_favors(efficient_producers, first_movers, sk2) | (~environment(sk1)) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~(cardinality_at_time(first_movers, sk2) = zero)) | (~subpopulation(first_movers, sk1, sk2)) | (~subpopulation(efficient_producers, sk1, sk2))),
% 0.11/0.41 inference(modus_ponens,[status(thm)],[142, 141])).
% 0.11/0.41 tff(144,plain,
% 0.11/0.41 ((~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~(cardinality_at_time(first_movers, sk2) = zero))),
% 0.11/0.41 inference(unit_resolution,[status(thm)],[143, 137, 26, 127, 124, 107])).
% 0.11/0.41 tff(145,plain,
% 0.11/0.41 (~(cardinality_at_time(first_movers, sk2) = zero)),
% 0.11/0.41 inference(unit_resolution,[status(thm)],[144, 90])).
% 0.11/0.41 tff(146,plain,
% 0.11/0.41 (^[B: $i, A: $i] : refl((greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A))) <=> (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A))))),
% 0.11/0.41 inference(bind,[status(th)],[])).
% 0.11/0.41 tff(147,plain,
% 0.11/0.41 (![B: $i, A: $i] : (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A))) <=> ![B: $i, A: $i] : (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.41 inference(quant_intro,[status(thm)],[146])).
% 0.11/0.41 tff(148,plain,
% 0.11/0.41 (![B: $i, A: $i] : (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A))) <=> ![B: $i, A: $i] : (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.41 inference(rewrite,[status(thm)],[])).
% 0.11/0.41 tff(149,plain,
% 0.11/0.41 (^[B: $i, A: $i] : rewrite((((~environment(A)) | (~in_environment(A, B))) | greater_or_equal(cardinality_at_time(first_movers, B), zero)) <=> (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A))))),
% 0.11/0.41 inference(bind,[status(th)],[])).
% 0.11/0.41 tff(150,plain,
% 0.11/0.41 (![B: $i, A: $i] : (((~environment(A)) | (~in_environment(A, B))) | greater_or_equal(cardinality_at_time(first_movers, B), zero)) <=> ![B: $i, A: $i] : (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.41 inference(quant_intro,[status(thm)],[149])).
% 0.11/0.41 tff(151,axiom,(![B: $i, A: $i] : (((~environment(A)) | (~in_environment(A, B))) | greater_or_equal(cardinality_at_time(first_movers, B), zero))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp_first_movers_exist_31')).
% 0.11/0.41 tff(152,plain,
% 0.11/0.41 (![B: $i, A: $i] : (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.41 inference(modus_ponens,[status(thm)],[151, 150])).
% 0.11/0.41 tff(153,plain,
% 0.11/0.41 (![B: $i, A: $i] : (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.41 inference(modus_ponens,[status(thm)],[152, 148])).
% 0.11/0.41 tff(154,plain,(
% 0.11/0.41 ![B: $i, A: $i] : (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.41 inference(skolemize,[status(sab)],[153])).
% 0.11/0.41 tff(155,plain,
% 0.11/0.41 (![B: $i, A: $i] : (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.41 inference(modus_ponens,[status(thm)],[154, 147])).
% 0.11/0.41 tff(156,plain,
% 0.11/0.41 (((~![B: $i, A: $i] : (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A)))) | ((~in_environment(sk1, sk2)) | (~environment(sk1)) | greater_or_equal(cardinality_at_time(first_movers, sk2), zero))) <=> ((~![B: $i, A: $i] : (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A)))) | (~in_environment(sk1, sk2)) | (~environment(sk1)) | greater_or_equal(cardinality_at_time(first_movers, sk2), zero))),
% 0.11/0.42 inference(rewrite,[status(thm)],[])).
% 0.11/0.42 tff(157,plain,
% 0.11/0.42 ((greater_or_equal(cardinality_at_time(first_movers, sk2), zero) | (~in_environment(sk1, sk2)) | (~environment(sk1))) <=> ((~in_environment(sk1, sk2)) | (~environment(sk1)) | greater_or_equal(cardinality_at_time(first_movers, sk2), zero))),
% 0.11/0.42 inference(rewrite,[status(thm)],[])).
% 0.11/0.42 tff(158,plain,
% 0.11/0.42 (((~![B: $i, A: $i] : (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A)))) | (greater_or_equal(cardinality_at_time(first_movers, sk2), zero) | (~in_environment(sk1, sk2)) | (~environment(sk1)))) <=> ((~![B: $i, A: $i] : (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A)))) | ((~in_environment(sk1, sk2)) | (~environment(sk1)) | greater_or_equal(cardinality_at_time(first_movers, sk2), zero)))),
% 0.11/0.42 inference(monotonicity,[status(thm)],[157])).
% 0.11/0.42 tff(159,plain,
% 0.11/0.42 (((~![B: $i, A: $i] : (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A)))) | (greater_or_equal(cardinality_at_time(first_movers, sk2), zero) | (~in_environment(sk1, sk2)) | (~environment(sk1)))) <=> ((~![B: $i, A: $i] : (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A)))) | (~in_environment(sk1, sk2)) | (~environment(sk1)) | greater_or_equal(cardinality_at_time(first_movers, sk2), zero))),
% 0.11/0.42 inference(transitivity,[status(thm)],[158, 156])).
% 0.11/0.42 tff(160,plain,
% 0.11/0.42 ((~![B: $i, A: $i] : (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A)))) | (greater_or_equal(cardinality_at_time(first_movers, sk2), zero) | (~in_environment(sk1, sk2)) | (~environment(sk1)))),
% 0.11/0.42 inference(quant_inst,[status(thm)],[])).
% 0.11/0.42 tff(161,plain,
% 0.11/0.42 ((~![B: $i, A: $i] : (greater_or_equal(cardinality_at_time(first_movers, B), zero) | (~in_environment(A, B)) | (~environment(A)))) | (~in_environment(sk1, sk2)) | (~environment(sk1)) | greater_or_equal(cardinality_at_time(first_movers, sk2), zero)),
% 0.11/0.42 inference(modus_ponens,[status(thm)],[160, 159])).
% 0.11/0.42 tff(162,plain,
% 0.11/0.42 (greater_or_equal(cardinality_at_time(first_movers, sk2), zero)),
% 0.11/0.42 inference(unit_resolution,[status(thm)],[161, 155, 26, 75])).
% 0.11/0.42 tff(163,plain,
% 0.11/0.42 (((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | (greater(cardinality_at_time(first_movers, sk2), zero) | (cardinality_at_time(first_movers, sk2) = zero) | (~greater_or_equal(cardinality_at_time(first_movers, sk2), zero)))) <=> ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | greater(cardinality_at_time(first_movers, sk2), zero) | (cardinality_at_time(first_movers, sk2) = zero) | (~greater_or_equal(cardinality_at_time(first_movers, sk2), zero)))),
% 0.11/0.42 inference(rewrite,[status(thm)],[])).
% 0.11/0.42 tff(164,plain,
% 0.11/0.42 (((cardinality_at_time(first_movers, sk2) = zero) | greater(cardinality_at_time(first_movers, sk2), zero) | (~greater_or_equal(cardinality_at_time(first_movers, sk2), zero))) <=> (greater(cardinality_at_time(first_movers, sk2), zero) | (cardinality_at_time(first_movers, sk2) = zero) | (~greater_or_equal(cardinality_at_time(first_movers, sk2), zero)))),
% 0.11/0.42 inference(rewrite,[status(thm)],[])).
% 0.11/0.42 tff(165,plain,
% 0.11/0.42 (((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((cardinality_at_time(first_movers, sk2) = zero) | greater(cardinality_at_time(first_movers, sk2), zero) | (~greater_or_equal(cardinality_at_time(first_movers, sk2), zero)))) <=> ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | (greater(cardinality_at_time(first_movers, sk2), zero) | (cardinality_at_time(first_movers, sk2) = zero) | (~greater_or_equal(cardinality_at_time(first_movers, sk2), zero))))),
% 0.11/0.42 inference(monotonicity,[status(thm)],[164])).
% 0.11/0.42 tff(166,plain,
% 0.11/0.42 (((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((cardinality_at_time(first_movers, sk2) = zero) | greater(cardinality_at_time(first_movers, sk2), zero) | (~greater_or_equal(cardinality_at_time(first_movers, sk2), zero)))) <=> ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | greater(cardinality_at_time(first_movers, sk2), zero) | (cardinality_at_time(first_movers, sk2) = zero) | (~greater_or_equal(cardinality_at_time(first_movers, sk2), zero)))),
% 0.11/0.42 inference(transitivity,[status(thm)],[165, 163])).
% 0.11/0.42 tff(167,plain,
% 0.11/0.42 ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | ((cardinality_at_time(first_movers, sk2) = zero) | greater(cardinality_at_time(first_movers, sk2), zero) | (~greater_or_equal(cardinality_at_time(first_movers, sk2), zero)))),
% 0.11/0.42 inference(quant_inst,[status(thm)],[])).
% 0.11/0.42 tff(168,plain,
% 0.11/0.42 ((~![B: $i, A: $i] : ((A = B) | greater(A, B) | (~greater_or_equal(A, B)))) | greater(cardinality_at_time(first_movers, sk2), zero) | (cardinality_at_time(first_movers, sk2) = zero) | (~greater_or_equal(cardinality_at_time(first_movers, sk2), zero))),
% 0.11/0.42 inference(modus_ponens,[status(thm)],[167, 166])).
% 0.11/0.42 tff(169,plain,
% 0.11/0.42 (greater(cardinality_at_time(first_movers, sk2), zero) | (cardinality_at_time(first_movers, sk2) = zero)),
% 0.11/0.42 inference(unit_resolution,[status(thm)],[168, 47, 162])).
% 0.11/0.42 tff(170,plain,
% 0.11/0.42 (greater(cardinality_at_time(first_movers, sk2), zero)),
% 0.11/0.42 inference(unit_resolution,[status(thm)],[169, 145])).
% 0.11/0.42 tff(171,plain,
% 0.11/0.42 (^[B: $i, A: $i] : refl((subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A))) <=> (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A))))),
% 0.11/0.42 inference(bind,[status(th)],[])).
% 0.11/0.42 tff(172,plain,
% 0.11/0.42 (![B: $i, A: $i] : (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A))) <=> ![B: $i, A: $i] : (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.42 inference(quant_intro,[status(thm)],[171])).
% 0.11/0.42 tff(173,plain,
% 0.11/0.42 (![B: $i, A: $i] : (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A))) <=> ![B: $i, A: $i] : (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.42 inference(rewrite,[status(thm)],[])).
% 0.11/0.42 tff(174,plain,
% 0.11/0.42 (^[B: $i, A: $i] : trans(monotonicity(trans(monotonicity(rewrite((((~environment(A)) | (~in_environment(A, B))) | (~greater(cardinality_at_time(first_movers, B), zero))) <=> ((~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))), (((((~environment(A)) | (~in_environment(A, B))) | (~greater(cardinality_at_time(first_movers, B), zero))) | (~greater(cardinality_at_time(efficient_producers, B), zero))) <=> (((~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A))) | (~greater(cardinality_at_time(efficient_producers, B), zero))))), rewrite((((~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A))) | (~greater(cardinality_at_time(efficient_producers, B), zero))) <=> ((~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))), (((((~environment(A)) | (~in_environment(A, B))) | (~greater(cardinality_at_time(first_movers, B), zero))) | (~greater(cardinality_at_time(efficient_producers, B), zero))) <=> ((~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A))))), ((((((~environment(A)) | (~in_environment(A, B))) | (~greater(cardinality_at_time(first_movers, B), zero))) | (~greater(cardinality_at_time(efficient_producers, B), zero))) | subpopulations(first_movers, efficient_producers, A, B)) <=> (((~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A))) | subpopulations(first_movers, efficient_producers, A, B)))), rewrite((((~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A))) | subpopulations(first_movers, efficient_producers, A, B)) <=> (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))), ((((((~environment(A)) | (~in_environment(A, B))) | (~greater(cardinality_at_time(first_movers, B), zero))) | (~greater(cardinality_at_time(efficient_producers, B), zero))) | subpopulations(first_movers, efficient_producers, A, B)) <=> (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))))),
% 0.11/0.42 inference(bind,[status(th)],[])).
% 0.11/0.42 tff(175,plain,
% 0.11/0.42 (![B: $i, A: $i] : (((((~environment(A)) | (~in_environment(A, B))) | (~greater(cardinality_at_time(first_movers, B), zero))) | (~greater(cardinality_at_time(efficient_producers, B), zero))) | subpopulations(first_movers, efficient_producers, A, B)) <=> ![B: $i, A: $i] : (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.42 inference(quant_intro,[status(thm)],[174])).
% 0.11/0.42 tff(176,axiom,(![B: $i, A: $i] : (((((~environment(A)) | (~in_environment(A, B))) | (~greater(cardinality_at_time(first_movers, B), zero))) | (~greater(cardinality_at_time(efficient_producers, B), zero))) | subpopulations(first_movers, efficient_producers, A, B))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp_non_empty_fm_and_ep_30')).
% 0.11/0.42 tff(177,plain,
% 0.11/0.42 (![B: $i, A: $i] : (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.42 inference(modus_ponens,[status(thm)],[176, 175])).
% 0.11/0.42 tff(178,plain,
% 0.11/0.42 (![B: $i, A: $i] : (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.42 inference(modus_ponens,[status(thm)],[177, 173])).
% 0.11/0.42 tff(179,plain,(
% 0.11/0.42 ![B: $i, A: $i] : (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.42 inference(skolemize,[status(sab)],[178])).
% 0.11/0.42 tff(180,plain,
% 0.11/0.42 (![B: $i, A: $i] : (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))),
% 0.11/0.42 inference(modus_ponens,[status(thm)],[179, 172])).
% 0.11/0.42 tff(181,plain,
% 0.11/0.42 (((~![B: $i, A: $i] : (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))) | ((~in_environment(sk1, sk2)) | (~environment(sk1)) | subpopulations(first_movers, efficient_producers, sk1, sk2) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~greater(cardinality_at_time(first_movers, sk2), zero)))) <=> ((~![B: $i, A: $i] : (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))) | (~in_environment(sk1, sk2)) | (~environment(sk1)) | subpopulations(first_movers, efficient_producers, sk1, sk2) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~greater(cardinality_at_time(first_movers, sk2), zero)))),
% 0.11/0.42 inference(rewrite,[status(thm)],[])).
% 0.11/0.42 tff(182,plain,
% 0.11/0.42 ((subpopulations(first_movers, efficient_producers, sk1, sk2) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~greater(cardinality_at_time(first_movers, sk2), zero)) | (~in_environment(sk1, sk2)) | (~environment(sk1))) <=> ((~in_environment(sk1, sk2)) | (~environment(sk1)) | subpopulations(first_movers, efficient_producers, sk1, sk2) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~greater(cardinality_at_time(first_movers, sk2), zero)))),
% 0.11/0.42 inference(rewrite,[status(thm)],[])).
% 0.11/0.42 tff(183,plain,
% 0.11/0.42 (((~![B: $i, A: $i] : (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))) | (subpopulations(first_movers, efficient_producers, sk1, sk2) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~greater(cardinality_at_time(first_movers, sk2), zero)) | (~in_environment(sk1, sk2)) | (~environment(sk1)))) <=> ((~![B: $i, A: $i] : (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))) | ((~in_environment(sk1, sk2)) | (~environment(sk1)) | subpopulations(first_movers, efficient_producers, sk1, sk2) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~greater(cardinality_at_time(first_movers, sk2), zero))))),
% 0.11/0.42 inference(monotonicity,[status(thm)],[182])).
% 0.11/0.42 tff(184,plain,
% 0.11/0.42 (((~![B: $i, A: $i] : (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))) | (subpopulations(first_movers, efficient_producers, sk1, sk2) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~greater(cardinality_at_time(first_movers, sk2), zero)) | (~in_environment(sk1, sk2)) | (~environment(sk1)))) <=> ((~![B: $i, A: $i] : (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))) | (~in_environment(sk1, sk2)) | (~environment(sk1)) | subpopulations(first_movers, efficient_producers, sk1, sk2) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~greater(cardinality_at_time(first_movers, sk2), zero)))),
% 0.11/0.42 inference(transitivity,[status(thm)],[183, 181])).
% 0.11/0.42 tff(185,plain,
% 0.11/0.42 ((~![B: $i, A: $i] : (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))) | (subpopulations(first_movers, efficient_producers, sk1, sk2) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~greater(cardinality_at_time(first_movers, sk2), zero)) | (~in_environment(sk1, sk2)) | (~environment(sk1)))),
% 0.11/0.42 inference(quant_inst,[status(thm)],[])).
% 0.11/0.42 tff(186,plain,
% 0.11/0.42 ((~![B: $i, A: $i] : (subpopulations(first_movers, efficient_producers, A, B) | (~greater(cardinality_at_time(efficient_producers, B), zero)) | (~greater(cardinality_at_time(first_movers, B), zero)) | (~in_environment(A, B)) | (~environment(A)))) | (~in_environment(sk1, sk2)) | (~environment(sk1)) | subpopulations(first_movers, efficient_producers, sk1, sk2) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~greater(cardinality_at_time(first_movers, sk2), zero))),
% 0.11/0.42 inference(modus_ponens,[status(thm)],[185, 184])).
% 0.11/0.42 tff(187,plain,
% 0.11/0.42 (subpopulations(first_movers, efficient_producers, sk1, sk2) | (~greater(cardinality_at_time(efficient_producers, sk2), zero)) | (~greater(cardinality_at_time(first_movers, sk2), zero))),
% 0.11/0.42 inference(unit_resolution,[status(thm)],[186, 180, 26, 75])).
% 0.11/0.42 tff(188,plain,
% 0.11/0.42 (subpopulations(first_movers, efficient_producers, sk1, sk2)),
% 0.11/0.42 inference(unit_resolution,[status(thm)],[187, 170, 90])).
% 0.11/0.42 tff(189,plain,
% 0.11/0.42 (^[A: $i, C: $i] : refl(((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~greater(C, critical_point(A)))) <=> ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~greater(C, critical_point(A)))))),
% 0.11/0.42 inference(bind,[status(th)],[])).
% 0.11/0.42 tff(190,plain,
% 0.11/0.42 (![A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~greater(C, critical_point(A)))) <=> ![A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~greater(C, critical_point(A))))),
% 0.11/0.42 inference(quant_intro,[status(thm)],[189])).
% 0.11/0.42 tff(191,plain,
% 0.11/0.42 (![A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~greater(C, critical_point(A)))) <=> ![A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~greater(C, critical_point(A))))),
% 0.11/0.42 inference(rewrite,[status(thm)],[])).
% 0.11/0.42 tff(192,plain,
% 0.11/0.42 (^[A: $i, C: $i] : rewrite(((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~greater(C, critical_point(A))) | (~subpopulations(first_movers, efficient_producers, A, C))) <=> ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~greater(C, critical_point(A)))))),
% 0.11/0.42 inference(bind,[status(th)],[])).
% 0.11/0.42 tff(193,plain,
% 0.11/0.42 (![A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~greater(C, critical_point(A))) | (~subpopulations(first_movers, efficient_producers, A, C))) <=> ![A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~greater(C, critical_point(A))))),
% 0.11/0.42 inference(quant_intro,[status(thm)],[192])).
% 0.11/0.42 tff(194,plain,
% 0.11/0.42 (![B: $i, A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~greater(C, critical_point(A))) | (~subpopulations(first_movers, efficient_producers, A, C))) <=> ![A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~greater(C, critical_point(A))) | (~subpopulations(first_movers, efficient_producers, A, C)))),
% 0.11/0.43 inference(elim_unused_vars,[status(thm)],[])).
% 0.11/0.43 tff(195,plain,
% 0.11/0.43 (![B: $i, A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~greater(C, B)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~(B = critical_point(A)))) <=> ![B: $i, A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~greater(C, critical_point(A))) | (~subpopulations(first_movers, efficient_producers, A, C)))),
% 0.11/0.43 inference(destructive_equality_resolution,[status(thm)],[])).
% 0.11/0.43 tff(196,plain,
% 0.11/0.43 (![B: $i, A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~greater(C, B)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~(B = critical_point(A)))) <=> ![A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~greater(C, critical_point(A))) | (~subpopulations(first_movers, efficient_producers, A, C)))),
% 0.11/0.43 inference(transitivity,[status(thm)],[195, 194])).
% 0.11/0.43 tff(197,plain,
% 0.11/0.43 (![B: $i, A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~greater(C, B)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~(B = critical_point(A)))) <=> ![A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~greater(C, critical_point(A))))),
% 0.11/0.43 inference(transitivity,[status(thm)],[196, 193])).
% 0.11/0.43 tff(198,plain,
% 0.11/0.43 (^[B: $i, A: $i, C: $i] : trans(monotonicity(trans(monotonicity(rewrite((((~environment(A)) | (~(B = critical_point(A)))) | (~subpopulations(first_movers, efficient_producers, A, C))) <=> ((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~(B = critical_point(A))))), (((((~environment(A)) | (~(B = critical_point(A)))) | (~subpopulations(first_movers, efficient_producers, A, C))) | (~greater(C, B))) <=> (((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~(B = critical_point(A)))) | (~greater(C, B))))), rewrite((((~environment(A)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~(B = critical_point(A)))) | (~greater(C, B))) <=> ((~environment(A)) | (~greater(C, B)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~(B = critical_point(A))))), (((((~environment(A)) | (~(B = critical_point(A)))) | (~subpopulations(first_movers, efficient_producers, A, C))) | (~greater(C, B))) <=> ((~environment(A)) | (~greater(C, B)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~(B = critical_point(A)))))), ((((((~environment(A)) | (~(B = critical_point(A)))) | (~subpopulations(first_movers, efficient_producers, A, C))) | (~greater(C, B))) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C))) <=> (((~environment(A)) | (~greater(C, B)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~(B = critical_point(A)))) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C))))), rewrite((((~environment(A)) | (~greater(C, B)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~(B = critical_point(A)))) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C))) <=> ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~greater(C, B)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~(B = critical_point(A))))), ((((((~environment(A)) | (~(B = critical_point(A)))) | (~subpopulations(first_movers, efficient_producers, A, C))) | (~greater(C, B))) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C))) <=> ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~greater(C, B)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~(B = critical_point(A))))))),
% 0.11/0.43 inference(bind,[status(th)],[])).
% 0.11/0.43 tff(199,plain,
% 0.11/0.43 (![B: $i, A: $i, C: $i] : (((((~environment(A)) | (~(B = critical_point(A)))) | (~subpopulations(first_movers, efficient_producers, A, C))) | (~greater(C, B))) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C))) <=> ![B: $i, A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~greater(C, B)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~(B = critical_point(A))))),
% 0.11/0.43 inference(quant_intro,[status(thm)],[198])).
% 0.11/0.43 tff(200,plain,
% 0.11/0.43 (![B: $i, A: $i, C: $i] : (((((~environment(A)) | (~(B = critical_point(A)))) | (~subpopulations(first_movers, efficient_producers, A, C))) | (~greater(C, B))) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C))) <=> ![A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~greater(C, critical_point(A))))),
% 0.11/0.43 inference(transitivity,[status(thm)],[199, 197])).
% 0.11/0.43 tff(201,axiom,(![B: $i, A: $i, C: $i] : (((((~environment(A)) | (~(B = critical_point(A)))) | (~subpopulations(first_movers, efficient_producers, A, C))) | (~greater(C, B))) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','d1_40')).
% 0.11/0.43 tff(202,plain,
% 0.11/0.43 (![A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~greater(C, critical_point(A))))),
% 0.11/0.43 inference(modus_ponens,[status(thm)],[201, 200])).
% 0.11/0.43 tff(203,plain,
% 0.11/0.43 (![A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~greater(C, critical_point(A))))),
% 0.11/0.43 inference(modus_ponens,[status(thm)],[202, 191])).
% 0.11/0.43 tff(204,plain,(
% 0.11/0.43 ![A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~greater(C, critical_point(A))))),
% 0.11/0.43 inference(skolemize,[status(sab)],[203])).
% 0.11/0.43 tff(205,plain,
% 0.11/0.43 (![A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~greater(C, critical_point(A))))),
% 0.11/0.43 inference(modus_ponens,[status(thm)],[204, 190])).
% 0.11/0.43 tff(206,plain,
% 0.11/0.43 (((~![A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~greater(C, critical_point(A))))) | ((~environment(sk1)) | greater(growth_rate(efficient_producers, sk2), growth_rate(first_movers, sk2)) | (~subpopulations(first_movers, efficient_producers, sk1, sk2)) | (~greater(sk2, critical_point(sk1))))) <=> ((~![A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~greater(C, critical_point(A))))) | (~environment(sk1)) | greater(growth_rate(efficient_producers, sk2), growth_rate(first_movers, sk2)) | (~subpopulations(first_movers, efficient_producers, sk1, sk2)) | (~greater(sk2, critical_point(sk1))))),
% 0.11/0.43 inference(rewrite,[status(thm)],[])).
% 0.11/0.43 tff(207,plain,
% 0.11/0.43 ((~![A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~greater(C, critical_point(A))))) | ((~environment(sk1)) | greater(growth_rate(efficient_producers, sk2), growth_rate(first_movers, sk2)) | (~subpopulations(first_movers, efficient_producers, sk1, sk2)) | (~greater(sk2, critical_point(sk1))))),
% 0.11/0.43 inference(quant_inst,[status(thm)],[])).
% 0.11/0.43 tff(208,plain,
% 0.11/0.43 ((~![A: $i, C: $i] : ((~environment(A)) | greater(growth_rate(efficient_producers, C), growth_rate(first_movers, C)) | (~subpopulations(first_movers, efficient_producers, A, C)) | (~greater(C, critical_point(A))))) | (~environment(sk1)) | greater(growth_rate(efficient_producers, sk2), growth_rate(first_movers, sk2)) | (~subpopulations(first_movers, efficient_producers, sk1, sk2)) | (~greater(sk2, critical_point(sk1)))),
% 0.11/0.43 inference(modus_ponens,[status(thm)],[207, 206])).
% 0.11/0.43 tff(209,plain,
% 0.11/0.43 (greater(growth_rate(efficient_producers, sk2), growth_rate(first_movers, sk2)) | (~subpopulations(first_movers, efficient_producers, sk1, sk2))),
% 0.11/0.43 inference(unit_resolution,[status(thm)],[208, 205, 26, 5])).
% 0.11/0.43 tff(210,plain,
% 0.11/0.43 (greater(growth_rate(efficient_producers, sk2), growth_rate(first_movers, sk2))),
% 0.11/0.43 inference(unit_resolution,[status(thm)],[209, 188])).
% 0.11/0.43 tff(211,plain,
% 0.11/0.43 (^[B: $i, D: $i, A: $i, C: $i] : refl((selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A))) <=> (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A))))),
% 0.11/0.43 inference(bind,[status(th)],[])).
% 0.11/0.43 tff(212,plain,
% 0.11/0.43 (![B: $i, D: $i, A: $i, C: $i] : (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A))) <=> ![B: $i, D: $i, A: $i, C: $i] : (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A)))),
% 0.11/0.43 inference(quant_intro,[status(thm)],[211])).
% 0.11/0.43 tff(213,plain,
% 0.11/0.43 (![B: $i, D: $i, A: $i, C: $i] : (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A))) <=> ![B: $i, D: $i, A: $i, C: $i] : (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A)))),
% 0.11/0.43 inference(rewrite,[status(thm)],[])).
% 0.11/0.43 tff(214,plain,
% 0.11/0.43 (^[B: $i, D: $i, A: $i, C: $i] : trans(monotonicity(rewrite((((~environment(A)) | (~subpopulations(B, C, A, D))) | (~greater(growth_rate(C, D), growth_rate(B, D)))) <=> ((~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A)))), (((((~environment(A)) | (~subpopulations(B, C, A, D))) | (~greater(growth_rate(C, D), growth_rate(B, D)))) | selection_favors(C, B, D)) <=> (((~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A))) | selection_favors(C, B, D)))), rewrite((((~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A))) | selection_favors(C, B, D)) <=> (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A)))), (((((~environment(A)) | (~subpopulations(B, C, A, D))) | (~greater(growth_rate(C, D), growth_rate(B, D)))) | selection_favors(C, B, D)) <=> (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A)))))),
% 0.11/0.43 inference(bind,[status(th)],[])).
% 0.11/0.43 tff(215,plain,
% 0.11/0.43 (![B: $i, D: $i, A: $i, C: $i] : ((((~environment(A)) | (~subpopulations(B, C, A, D))) | (~greater(growth_rate(C, D), growth_rate(B, D)))) | selection_favors(C, B, D)) <=> ![B: $i, D: $i, A: $i, C: $i] : (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A)))),
% 0.11/0.43 inference(quant_intro,[status(thm)],[214])).
% 0.11/0.43 tff(216,axiom,(![B: $i, D: $i, A: $i, C: $i] : ((((~environment(A)) | (~subpopulations(B, C, A, D))) | (~greater(growth_rate(C, D), growth_rate(B, D)))) | selection_favors(C, B, D))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp1_high_growth_rates_28')).
% 0.11/0.43 tff(217,plain,
% 0.11/0.43 (![B: $i, D: $i, A: $i, C: $i] : (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A)))),
% 0.11/0.43 inference(modus_ponens,[status(thm)],[216, 215])).
% 0.11/0.43 tff(218,plain,
% 0.11/0.43 (![B: $i, D: $i, A: $i, C: $i] : (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A)))),
% 0.11/0.43 inference(modus_ponens,[status(thm)],[217, 213])).
% 0.11/0.43 tff(219,plain,(
% 0.11/0.43 ![B: $i, D: $i, A: $i, C: $i] : (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A)))),
% 0.11/0.43 inference(skolemize,[status(sab)],[218])).
% 0.11/0.43 tff(220,plain,
% 0.11/0.43 (![B: $i, D: $i, A: $i, C: $i] : (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A)))),
% 0.11/0.43 inference(modus_ponens,[status(thm)],[219, 212])).
% 0.11/0.43 tff(221,plain,
% 0.11/0.43 (((~![B: $i, D: $i, A: $i, C: $i] : (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | (selection_favors(efficient_producers, first_movers, sk2) | (~environment(sk1)) | (~subpopulations(first_movers, efficient_producers, sk1, sk2)) | (~greater(growth_rate(efficient_producers, sk2), growth_rate(first_movers, sk2))))) <=> ((~![B: $i, D: $i, A: $i, C: $i] : (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | selection_favors(efficient_producers, first_movers, sk2) | (~environment(sk1)) | (~subpopulations(first_movers, efficient_producers, sk1, sk2)) | (~greater(growth_rate(efficient_producers, sk2), growth_rate(first_movers, sk2))))),
% 0.11/0.43 inference(rewrite,[status(thm)],[])).
% 0.11/0.43 tff(222,plain,
% 0.11/0.43 ((selection_favors(efficient_producers, first_movers, sk2) | (~greater(growth_rate(efficient_producers, sk2), growth_rate(first_movers, sk2))) | (~subpopulations(first_movers, efficient_producers, sk1, sk2)) | (~environment(sk1))) <=> (selection_favors(efficient_producers, first_movers, sk2) | (~environment(sk1)) | (~subpopulations(first_movers, efficient_producers, sk1, sk2)) | (~greater(growth_rate(efficient_producers, sk2), growth_rate(first_movers, sk2))))),
% 0.11/0.43 inference(rewrite,[status(thm)],[])).
% 0.11/0.43 tff(223,plain,
% 0.11/0.43 (((~![B: $i, D: $i, A: $i, C: $i] : (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | (selection_favors(efficient_producers, first_movers, sk2) | (~greater(growth_rate(efficient_producers, sk2), growth_rate(first_movers, sk2))) | (~subpopulations(first_movers, efficient_producers, sk1, sk2)) | (~environment(sk1)))) <=> ((~![B: $i, D: $i, A: $i, C: $i] : (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | (selection_favors(efficient_producers, first_movers, sk2) | (~environment(sk1)) | (~subpopulations(first_movers, efficient_producers, sk1, sk2)) | (~greater(growth_rate(efficient_producers, sk2), growth_rate(first_movers, sk2)))))),
% 0.11/0.43 inference(monotonicity,[status(thm)],[222])).
% 0.11/0.43 tff(224,plain,
% 0.11/0.43 (((~![B: $i, D: $i, A: $i, C: $i] : (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | (selection_favors(efficient_producers, first_movers, sk2) | (~greater(growth_rate(efficient_producers, sk2), growth_rate(first_movers, sk2))) | (~subpopulations(first_movers, efficient_producers, sk1, sk2)) | (~environment(sk1)))) <=> ((~![B: $i, D: $i, A: $i, C: $i] : (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | selection_favors(efficient_producers, first_movers, sk2) | (~environment(sk1)) | (~subpopulations(first_movers, efficient_producers, sk1, sk2)) | (~greater(growth_rate(efficient_producers, sk2), growth_rate(first_movers, sk2))))),
% 0.11/0.43 inference(transitivity,[status(thm)],[223, 221])).
% 0.11/0.43 tff(225,plain,
% 0.11/0.43 ((~![B: $i, D: $i, A: $i, C: $i] : (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | (selection_favors(efficient_producers, first_movers, sk2) | (~greater(growth_rate(efficient_producers, sk2), growth_rate(first_movers, sk2))) | (~subpopulations(first_movers, efficient_producers, sk1, sk2)) | (~environment(sk1)))),
% 0.11/0.44 inference(quant_inst,[status(thm)],[])).
% 0.11/0.44 tff(226,plain,
% 0.11/0.44 ((~![B: $i, D: $i, A: $i, C: $i] : (selection_favors(C, B, D) | (~greater(growth_rate(C, D), growth_rate(B, D))) | (~subpopulations(B, C, A, D)) | (~environment(A)))) | selection_favors(efficient_producers, first_movers, sk2) | (~environment(sk1)) | (~subpopulations(first_movers, efficient_producers, sk1, sk2)) | (~greater(growth_rate(efficient_producers, sk2), growth_rate(first_movers, sk2)))),
% 0.11/0.44 inference(modus_ponens,[status(thm)],[225, 224])).
% 0.11/0.44 tff(227,plain,
% 0.11/0.44 ($false),
% 0.11/0.44 inference(unit_resolution,[status(thm)],[226, 220, 26, 127, 188, 210])).
% 0.11/0.44 % SZS output end Proof
% 0.11/0.44 % E exiting
%------------------------------------------------------------------------------