%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : MGT035-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:11:35 PM UTC 2026
% Result : Unsatisfiable 117.60s 33.11s
% Output : Proof 117.60s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
cnf(f19,hypothesis,
( greater_or_equal(sk2(A),equilibrium(A))
| ~ stable(A)
| ~ environment(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a4_41) ).
fof(f19_nnf,plain,
! [A] :
( greater_or_equal(sk2(A),equilibrium(A))
| ~ stable(A)
| ~ environment(A) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [A] :
( greater_or_equal(sk2(A),equilibrium(A))
| ~ stable(A)
| ~ environment(A) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
( greater_or_equal(sk2(X0),equilibrium(X0))
| ~ stable(X0)
| ~ environment(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(f20,negated_conjecture,
environment(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t4_42) ).
fof(f20_nnf,plain,
environment(sk3),
inference(nnf_transformation,[status(thm)],[f20]) ).
cnf(c20,plain,
environment(sk3),
inference(cnf_transformation,[status(esa)],[f20_nnf]) ).
cnf(p90,plain,
( greater_or_equal(sk2(sk3),equilibrium(sk3))
| ~ stable(sk3) ),
inference(resolution,[status(thm)],[c19,c20]) ).
cnf(f21,negated_conjecture,
stable(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t4_43) ).
fof(f21_nnf,plain,
stable(sk3),
inference(nnf_transformation,[status(thm)],[f21]) ).
cnf(c21,plain,
stable(sk3),
inference(cnf_transformation,[status(esa)],[f21_nnf]) ).
cnf(p91,plain,
greater_or_equal(sk2(sk3),equilibrium(sk3)),
inference(resolution,[status(thm)],[p90,c21]) ).
cnf(f2,axiom,
( A = B
| greater(A,B)
| ~ greater_or_equal(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_or_equal_24) ).
fof(f2_nnf,plain,
! [A,B] :
( A = B
| greater(A,B)
| ~ greater_or_equal(A,B) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,B] :
( A = B
| greater(A,B)
| ~ greater_or_equal(A,B) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( X0 = X1
| greater(X0,X1)
| ~ greater_or_equal(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p92,plain,
( sk2(sk3) = equilibrium(sk3)
| greater(sk2(sk3),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[p91,c2]) ).
cnf(f18,hypothesis,
( in_environment(A,sk2(A))
| ~ stable(A)
| ~ environment(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a4_40) ).
fof(f18_nnf,plain,
! [A] :
( in_environment(A,sk2(A))
| ~ stable(A)
| ~ environment(A) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [A] :
( in_environment(A,sk2(A))
| ~ stable(A)
| ~ environment(A) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( in_environment(X0,sk2(X0))
| ~ stable(X0)
| ~ environment(X0) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p36,plain,
( in_environment(sk3,sk2(sk3))
| ~ stable(sk3) ),
inference(resolution,[status(thm)],[c18,c20]) ).
cnf(p38,plain,
in_environment(sk3,sk2(sk3)),
inference(resolution,[status(thm)],[p36,c21]) ).
cnf(f23,negated_conjecture,
( greater_or_equal(sk4(A),A)
| ~ in_environment(sk3,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t4_45) ).
fof(f23_nnf,plain,
! [A] :
( greater_or_equal(sk4(A),A)
| ~ in_environment(sk3,A) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [A] :
( greater_or_equal(sk4(A),A)
| ~ in_environment(sk3,A) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( greater_or_equal(sk4(X0),X0)
| ~ in_environment(sk3,X0) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p39,plain,
greater_or_equal(sk4(sk2(sk3)),sk2(sk3)),
inference(resolution,[status(thm)],[p38,c23]) ).
cnf(p44,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| greater(sk4(sk2(sk3)),sk2(sk3)) ),
inference(resolution,[status(thm)],[p39,c2]) ).
cnf(f0,axiom,
( greater(A,C)
| ~ greater(B,C)
| ~ greater(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_transitivity_22) ).
fof(f0_nnf,plain,
! [A,B,C] :
( greater(A,C)
| ~ greater(B,C)
| ~ greater(A,B) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B,C] :
( greater(A,C)
| ~ greater(B,C)
| ~ greater(A,B) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p47,plain,
( greater(sk4(sk2(sk3)),X0)
| ~ greater(sk2(sk3),X0)
| sk4(sk2(sk3)) = sk2(sk3) ),
inference(resolution,[status(thm)],[p44,c0]) ).
cnf(p94,plain,
( greater(sk4(sk2(sk3)),equilibrium(sk3))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p92,p47]) ).
cnf(f3,axiom,
( greater_or_equal(A,B)
| ~ greater(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_or_equal_25) ).
fof(f3_nnf,plain,
! [A,B] :
( greater_or_equal(A,B)
| ~ greater(A,B) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B] :
( greater_or_equal(A,B)
| ~ greater(A,B) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( greater_or_equal(X0,X1)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p98,plain,
( greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p94,c3]) ).
cnf(f11,hypothesis,
( greater(zero,growth_rate(first_movers,B))
| greater(zero,growth_rate(efficient_producers,B))
| growth_rate(first_movers,B) = zero
| ~ greater_or_equal(B,equilibrium(A))
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ environment(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l6_33) ).
fof(f11_nnf,plain,
! [A,B] :
( greater(zero,growth_rate(first_movers,B))
| greater(zero,growth_rate(efficient_producers,B))
| growth_rate(first_movers,B) = zero
| ~ greater_or_equal(B,equilibrium(A))
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ environment(A) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [A,B] :
( greater(zero,growth_rate(first_movers,B))
| greater(zero,growth_rate(efficient_producers,B))
| growth_rate(first_movers,B) = zero
| ~ greater_or_equal(B,equilibrium(A))
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ environment(A) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( greater(zero,growth_rate(first_movers,X1))
| greater(zero,growth_rate(efficient_producers,X1))
| growth_rate(first_movers,X1) = zero
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p62,plain,
( greater(zero,growth_rate(first_movers,X0))
| greater(zero,growth_rate(efficient_producers,X0))
| growth_rate(first_movers,X0) = zero
| ~ greater_or_equal(X0,equilibrium(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0) ),
inference(resolution,[status(thm)],[c11,c20]) ).
cnf(f22,negated_conjecture,
( subpopulations(first_movers,efficient_producers,sk3,sk4(A))
| ~ in_environment(sk3,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t4_44) ).
fof(f22_nnf,plain,
! [A] :
( subpopulations(first_movers,efficient_producers,sk3,sk4(A))
| ~ in_environment(sk3,A) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [A] :
( subpopulations(first_movers,efficient_producers,sk3,sk4(A))
| ~ in_environment(sk3,A) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk4(X0))
| ~ in_environment(sk3,X0) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(p41,plain,
subpopulations(first_movers,efficient_producers,sk3,sk4(sk2(sk3))),
inference(resolution,[status(thm)],[p38,c22]) ).
cnf(p71,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[p62,p41]) ).
cnf(p102,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p98,p71]) ).
cnf(p119,plain,
( greater(zero,X0)
| ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),X0)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p102,c0]) ).
cnf(p137,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p119]) ).
cnf(f17,hypothesis,
( greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| ~ greater_or_equal(B,sk1(A))
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ stable(A)
| ~ environment(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1_39) ).
fof(f17_nnf,plain,
! [A,B] :
( greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| ~ greater_or_equal(B,sk1(A))
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ stable(A)
| ~ environment(A) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [A,B] :
( greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B))
| ~ greater_or_equal(B,sk1(A))
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ stable(A)
| ~ environment(A) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| ~ greater_or_equal(X1,sk1(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ stable(X0)
| ~ environment(X0) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p83,plain,
( greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ~ greater_or_equal(X0,sk1(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0)
| ~ stable(sk3) ),
inference(resolution,[status(thm)],[c17,c20]) ).
cnf(p84,plain,
( greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ~ greater_or_equal(X0,sk1(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0) ),
inference(resolution,[status(thm)],[p83,c21]) ).
cnf(p86,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| ~ greater_or_equal(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[p84,p41]) ).
cnf(f16,hypothesis,
( in_environment(A,sk1(A))
| ~ stable(A)
| ~ environment(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1_38) ).
fof(f16_nnf,plain,
! [A] :
( in_environment(A,sk1(A))
| ~ stable(A)
| ~ environment(A) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [A] :
( in_environment(A,sk1(A))
| ~ stable(A)
| ~ environment(A) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( in_environment(X0,sk1(X0))
| ~ stable(X0)
| ~ environment(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p26,plain,
( in_environment(sk3,sk1(sk3))
| ~ stable(sk3) ),
inference(resolution,[status(thm)],[c16,c20]) ).
cnf(p27,plain,
in_environment(sk3,sk1(sk3)),
inference(resolution,[status(thm)],[p26,c21]) ).
cnf(f1,axiom,
( greater(B,C)
| C = B
| greater(C,B)
| ~ in_environment(A,C)
| ~ in_environment(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_times_in_environment_23) ).
fof(f1_nnf,plain,
! [A,B,C] :
( greater(B,C)
| C = B
| greater(C,B)
| ~ in_environment(A,C)
| ~ in_environment(A,B) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B,C] :
( greater(B,C)
| C = B
| greater(C,B)
| ~ in_environment(A,C)
| ~ in_environment(A,B) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( greater(X1,X2)
| X2 = X1
| greater(X2,X1)
| ~ in_environment(X0,X2)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p31,plain,
( greater(sk1(sk3),X0)
| X0 = sk1(sk3)
| greater(X0,sk1(sk3))
| ~ in_environment(sk3,X0) ),
inference(resolution,[status(thm)],[p27,c1]) ).
cnf(p43,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(sk2(sk3),sk1(sk3)) ),
inference(resolution,[status(thm)],[p38,p31]) ).
cnf(p51,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(sk4(sk2(sk3)),sk1(sk3))
| sk4(sk2(sk3)) = sk2(sk3) ),
inference(resolution,[status(thm)],[p47,p43]) ).
cnf(p59,plain,
( greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3) ),
inference(resolution,[status(thm)],[p51,c3]) ).
cnf(p95,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[p86,p59]) ).
cnf(p145,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p137,p95]) ).
cnf(p150,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p145]) ).
cnf(f8,hypothesis,
( greater(growth_rate(efficient_producers,B),zero)
| greater(growth_rate(first_movers,B),zero)
| growth_rate(first_movers,B) = zero
| ~ greater_or_equal(B,equilibrium(A))
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ environment(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l6_30) ).
fof(f8_nnf,plain,
! [A,B] :
( greater(growth_rate(efficient_producers,B),zero)
| greater(growth_rate(first_movers,B),zero)
| growth_rate(first_movers,B) = zero
| ~ greater_or_equal(B,equilibrium(A))
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ environment(A) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A,B] :
( greater(growth_rate(efficient_producers,B),zero)
| greater(growth_rate(first_movers,B),zero)
| growth_rate(first_movers,B) = zero
| ~ greater_or_equal(B,equilibrium(A))
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ environment(A) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( greater(growth_rate(efficient_producers,X1),zero)
| greater(growth_rate(first_movers,X1),zero)
| growth_rate(first_movers,X1) = zero
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p48,plain,
( greater(growth_rate(efficient_producers,X0),zero)
| greater(growth_rate(first_movers,X0),zero)
| growth_rate(first_movers,X0) = zero
| ~ greater_or_equal(X0,equilibrium(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0) ),
inference(resolution,[status(thm)],[c8,c20]) ).
cnf(p64,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[p48,p41]) ).
cnf(p99,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p98,p64]) ).
cnf(p112,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p99,c3]) ).
cnf(f5,hypothesis,
( outcompetes(C,B,D)
| ~ greater(zero,growth_rate(B,D))
| ~ greater_or_equal(growth_rate(C,D),zero)
| ~ subpopulations(B,C,A,D)
| ~ environment(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_27) ).
fof(f5_nnf,plain,
! [A,B,C,D] :
( outcompetes(C,B,D)
| ~ greater(zero,growth_rate(B,D))
| ~ greater_or_equal(growth_rate(C,D),zero)
| ~ subpopulations(B,C,A,D)
| ~ environment(A) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A,B,C,D] :
( outcompetes(C,B,D)
| ~ greater(zero,growth_rate(B,D))
| ~ greater_or_equal(growth_rate(C,D),zero)
| ~ subpopulations(B,C,A,D)
| ~ environment(A) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( outcompetes(X2,X1,X3)
| ~ greater(zero,growth_rate(X1,X3))
| ~ greater_or_equal(growth_rate(X2,X3),zero)
| ~ subpopulations(X1,X2,X0,X3)
| ~ environment(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p34,plain,
( outcompetes(X1,X0,X2)
| ~ greater(zero,growth_rate(X0,X2))
| ~ greater_or_equal(growth_rate(X1,X2),zero)
| ~ subpopulations(X0,X1,sk3,X2) ),
inference(resolution,[status(thm)],[c5,c20]) ).
cnf(p46,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ greater_or_equal(growth_rate(efficient_producers,sk4(sk2(sk3))),zero) ),
inference(resolution,[status(thm)],[p41,p34]) ).
cnf(p131,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p112,p46]) ).
cnf(p155,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p150,p131]) ).
cnf(p198,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p155]) ).
cnf(p205,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| sk2(sk3) = equilibrium(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p198]) ).
cnf(p209,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p205]) ).
cnf(p107,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),X0)
| ~ greater(growth_rate(first_movers,sk4(sk2(sk3))),X0)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3) ),
inference(resolution,[status(thm)],[p95,c0]) ).
cnf(p214,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p209,p107]) ).
cnf(p287,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p214]) ).
cnf(p308,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| greater(sk1(sk3),sk2(sk3))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p287]) ).
cnf(p310,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p308]) ).
cnf(p314,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p310,c3]) ).
cnf(p320,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p314,p46]) ).
cnf(p329,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p320]) ).
cnf(p335,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p329,p150]) ).
cnf(p447,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p335]) ).
cnf(p557,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p447]) ).
cnf(p564,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p557]) ).
cnf(p567,plain,
( greater(sk1(sk3),sk2(sk3))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p564]) ).
cnf(p569,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p567]) ).
cnf(p573,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p569,p95]) ).
cnf(p591,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p573]) ).
cnf(p594,plain,
( greater(sk1(sk3),sk2(sk3))
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p591]) ).
cnf(p596,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p594]) ).
cnf(p605,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p596,c3]) ).
cnf(p608,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p605,p46]) ).
cnf(p628,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p608]) ).
cnf(f15,hypothesis,
( greater(zero,growth_rate(first_movers,B))
| greater(zero,growth_rate(efficient_producers,B))
| growth_rate(efficient_producers,B) = zero
| ~ greater_or_equal(B,equilibrium(A))
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ environment(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l6_37) ).
fof(f15_nnf,plain,
! [A,B] :
( greater(zero,growth_rate(first_movers,B))
| greater(zero,growth_rate(efficient_producers,B))
| growth_rate(efficient_producers,B) = zero
| ~ greater_or_equal(B,equilibrium(A))
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ environment(A) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [A,B] :
( greater(zero,growth_rate(first_movers,B))
| greater(zero,growth_rate(efficient_producers,B))
| growth_rate(efficient_producers,B) = zero
| ~ greater_or_equal(B,equilibrium(A))
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ environment(A) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( greater(zero,growth_rate(first_movers,X1))
| greater(zero,growth_rate(efficient_producers,X1))
| growth_rate(efficient_producers,X1) = zero
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p80,plain,
( greater(zero,growth_rate(first_movers,X0))
| greater(zero,growth_rate(efficient_producers,X0))
| growth_rate(efficient_producers,X0) = zero
| ~ greater_or_equal(X0,equilibrium(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0) ),
inference(resolution,[status(thm)],[c15,c20]) ).
cnf(p82,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[p80,p41]) ).
cnf(p106,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[p82,p98]) ).
cnf(p129,plain,
( greater(zero,X0)
| ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),X0)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[p106,c0]) ).
cnf(p142,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero ),
inference(factoring,[status(thm)],[p129]) ).
cnf(p148,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[p142,p95]) ).
cnf(p182,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero ),
inference(factoring,[status(thm)],[p148]) ).
cnf(p631,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p628,p182]) ).
cnf(p724,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p631]) ).
cnf(p737,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p724]) ).
cnf(p743,plain,
( greater(sk1(sk3),sk2(sk3))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p737]) ).
cnf(p745,plain,
( growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p743]) ).
cnf(p748,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p745,p95]) ).
cnf(p757,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p748]) ).
cnf(p760,plain,
( greater(sk1(sk3),sk2(sk3))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p757]) ).
cnf(p762,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p760]) ).
cnf(p772,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p762,p628]) ).
cnf(p844,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p772]) ).
cnf(p856,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p844]) ).
cnf(p857,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p856]) ).
cnf(p860,plain,
( greater(sk1(sk3),sk2(sk3))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p857]) ).
cnf(p862,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p860]) ).
cnf(f24,negated_conjecture,
( ~ outcompetes(efficient_producers,first_movers,sk4(A))
| ~ in_environment(sk3,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t4_46) ).
fof(f24_nnf,plain,
! [A] :
( ~ outcompetes(efficient_producers,first_movers,sk4(A))
| ~ in_environment(sk3,A) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [A] :
( ~ outcompetes(efficient_producers,first_movers,sk4(A))
| ~ in_environment(sk3,A) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( ~ outcompetes(efficient_producers,first_movers,sk4(X0))
| ~ in_environment(sk3,X0) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p40,plain,
~ outcompetes(efficient_producers,first_movers,sk4(sk2(sk3))),
inference(resolution,[status(thm)],[p38,c24]) ).
cnf(p869,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p862,p40]) ).
cnf(p875,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| ~ greater_or_equal(sk2(sk3),equilibrium(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p869,p64]) ).
cnf(p944,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p875,p91]) ).
cnf(p986,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p869,p944]) ).
cnf(p1195,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p986]) ).
cnf(p1445,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p1195]) ).
cnf(p1551,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p1445]) ).
cnf(p880,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| ~ greater_or_equal(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p869,p86]) ).
cnf(p50,plain,
( greater_or_equal(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p43,c3]) ).
cnf(p919,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p880,p50]) ).
cnf(p955,plain,
( greater(sk1(sk3),sk2(sk3))
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p919]) ).
cnf(p957,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p955]) ).
cnf(p962,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk4(sk2(sk3))))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p869,p957]) ).
cnf(p1149,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk4(sk2(sk3))))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p962]) ).
cnf(p1152,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk4(sk2(sk3))))
| greater(sk1(sk3),sk2(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p1149]) ).
cnf(p1154,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk4(sk2(sk3))))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p1152]) ).
cnf(p1157,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),X0)
| ~ greater(growth_rate(first_movers,sk4(sk2(sk3))),X0)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p1154,c0]) ).
cnf(p1562,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p1551,p1157]) ).
cnf(p2182,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p1562]) ).
cnf(p2492,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2182]) ).
cnf(p2495,plain,
( greater(sk1(sk3),sk2(sk3))
| greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2492]) ).
cnf(p2497,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2495]) ).
cnf(p2509,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p2497,p1154]) ).
cnf(p2578,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2509]) ).
cnf(p2579,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2578]) ).
cnf(p2582,plain,
( greater(sk1(sk3),sk2(sk3))
| greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2579]) ).
cnf(p2586,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2582]) ).
cnf(p2590,plain,
( greater_or_equal(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2586,c3]) ).
cnf(p873,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk2(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p869,p41]) ).
cnf(p891,plain,
( outcompetes(efficient_producers,first_movers,sk2(sk3))
| ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| ~ greater_or_equal(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p873,p34]) ).
cnf(p2595,plain,
( outcompetes(efficient_producers,first_movers,sk2(sk3))
| ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2590,p891]) ).
cnf(p2639,plain,
( outcompetes(efficient_producers,first_movers,sk2(sk3))
| ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2595]) ).
cnf(p2642,plain,
( outcompetes(efficient_producers,first_movers,sk2(sk3))
| ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2639]) ).
cnf(p2644,plain,
( outcompetes(efficient_producers,first_movers,sk2(sk3))
| ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2642]) ).
cnf(p883,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| ~ greater_or_equal(sk2(sk3),equilibrium(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p869,p82]) ).
cnf(p1023,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p883,p91]) ).
cnf(p1227,plain,
( greater(zero,X0)
| ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),X0)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p1023,c0]) ).
cnf(p1337,plain,
( ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p1227]) ).
cnf(p1369,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p1337,p957]) ).
cnf(p1791,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p1369]) ).
cnf(p1814,plain,
( greater(sk1(sk3),sk2(sk3))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p1791]) ).
cnf(p1816,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p1814]) ).
cnf(p1823,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p869,p1816]) ).
cnf(p2382,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p1823]) ).
cnf(p2385,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2382]) ).
cnf(p2387,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2385]) ).
cnf(p963,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p869,p957]) ).
cnf(p1159,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p963]) ).
cnf(p1175,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p1159]) ).
cnf(p1180,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p1175]) ).
cnf(p2398,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p2387,p1180]) ).
cnf(p2420,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2398]) ).
cnf(p2421,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(zero,growth_rate(first_movers,sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2420]) ).
cnf(p2424,plain,
( greater(sk1(sk3),sk2(sk3))
| greater(zero,growth_rate(first_movers,sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2421]) ).
cnf(p2428,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2424]) ).
cnf(p2647,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk2(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2644,p2428]) ).
cnf(p2652,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk2(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2647]) ).
cnf(p2655,plain,
( greater(sk1(sk3),sk2(sk3))
| outcompetes(efficient_producers,first_movers,sk2(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2652]) ).
cnf(p2661,plain,
( outcompetes(efficient_producers,first_movers,sk2(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2655]) ).
cnf(p872,plain,
( ~ outcompetes(efficient_producers,first_movers,sk2(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p869,p40]) ).
cnf(p2664,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2661,p872]) ).
cnf(p2672,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2664]) ).
cnf(p2675,plain,
( greater(sk1(sk3),sk2(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2672]) ).
cnf(p2677,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2675]) ).
cnf(p2680,plain,
( greater(sk1(sk3),X0)
| ~ greater(sk2(sk3),X0)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2677,c0]) ).
cnf(p2695,plain,
( sk2(sk3) = equilibrium(sk3)
| greater(sk1(sk3),equilibrium(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2680,p92]) ).
cnf(p2699,plain,
( greater(sk1(sk3),equilibrium(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2695]) ).
cnf(p28,plain,
greater_or_equal(sk4(sk1(sk3)),sk1(sk3)),
inference(resolution,[status(thm)],[p27,c23]) ).
cnf(p32,plain,
( sk4(sk1(sk3)) = sk1(sk3)
| greater(sk4(sk1(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[c2,p28]) ).
cnf(p33,plain,
( greater(sk4(sk1(sk3)),X0)
| ~ greater(sk1(sk3),X0)
| sk4(sk1(sk3)) = sk1(sk3) ),
inference(resolution,[status(thm)],[p32,c0]) ).
cnf(p2704,plain,
( greater(sk4(sk1(sk3)),equilibrium(sk3))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2699,p33]) ).
cnf(p2723,plain,
( greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2704,c3]) ).
cnf(p30,plain,
subpopulations(first_movers,efficient_producers,sk3,sk4(sk1(sk3))),
inference(resolution,[status(thm)],[p27,c22]) ).
cnf(p63,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[p48,p30]) ).
cnf(p2733,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2723,p63]) ).
cnf(p2756,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2733,c3]) ).
cnf(p35,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero) ),
inference(resolution,[status(thm)],[p34,p30]) ).
cnf(p2810,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2756,p35]) ).
cnf(p70,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[p62,p30]) ).
cnf(p2736,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2723,p70]) ).
cnf(p2772,plain,
( greater(zero,X0)
| ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),X0)
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2736,c0]) ).
cnf(p85,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3))))
| ~ greater_or_equal(sk4(sk1(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[p84,p30]) ).
cnf(p87,plain,
greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3)))),
inference(resolution,[status(thm)],[p85,p28]) ).
cnf(p2907,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2772,p87]) ).
cnf(p2908,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2907]) ).
cnf(p2999,plain,
( growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2810,p2908]) ).
cnf(p3477,plain,
( growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2999]) ).
cnf(p4196,plain,
( sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p3477]) ).
cnf(p4211,plain,
( sk2(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4196]) ).
cnf(p4212,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4211]) ).
cnf(p88,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),X0)
| ~ greater(growth_rate(first_movers,sk4(sk1(sk3))),X0) ),
inference(resolution,[status(thm)],[p87,c0]) ).
cnf(p4220,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p4212,p88]) ).
cnf(p4239,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p4220,c3]) ).
cnf(p4243,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p4239,p35]) ).
cnf(p4275,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4243]) ).
cnf(p4278,plain,
( growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p4275,p2908]) ).
cnf(p4638,plain,
( sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4278]) ).
cnf(p4641,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4638]) ).
cnf(p4642,plain,
( sk2(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4641]) ).
cnf(p4644,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4642]) ).
cnf(p89,plain,
greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3)))),
inference(resolution,[status(thm)],[p87,c3]) ).
cnf(p4651,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p4644,p89]) ).
cnf(p4668,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p4651,p35]) ).
cnf(p4680,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4668]) ).
cnf(p81,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[p80,p30]) ).
cnf(p2740,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2723,p81]) ).
cnf(p2796,plain,
( greater(zero,X0)
| ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),X0)
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2740,c0]) ).
cnf(p2952,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2796,p87]) ).
cnf(p2953,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2952]) ).
cnf(p4685,plain,
( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p4680,p2953]) ).
cnf(p4696,plain,
( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4685]) ).
cnf(p4699,plain,
( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4696]) ).
cnf(p4701,plain,
( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4699]) ).
cnf(p4704,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p4701,p87]) ).
cnf(p4716,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p4704,p4680]) ).
cnf(p4729,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4716]) ).
cnf(p4733,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4729]) ).
cnf(p4734,plain,
( sk2(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4733]) ).
cnf(p4736,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4734]) ).
cnf(p29,plain,
~ outcompetes(efficient_producers,first_movers,sk4(sk1(sk3))),
inference(resolution,[status(thm)],[p27,c24]) ).
cnf(p4739,plain,
( sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p4736,p29]) ).
cnf(p4745,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| ~ greater_or_equal(sk1(sk3),equilibrium(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p4739,p63]) ).
cnf(p2703,plain,
( greater_or_equal(sk1(sk3),equilibrium(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2699,c3]) ).
cnf(p4888,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p4745,p2703]) ).
cnf(p5202,plain,
( sk2(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4888]) ).
cnf(p5243,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5202]) ).
cnf(p5248,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p4739,p5243]) ).
cnf(p6053,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5248]) ).
cnf(p6266,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p6053]) ).
cnf(p4750,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk4(sk1(sk3))))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p4739,p87]) ).
cnf(p4777,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),X0)
| ~ greater(growth_rate(first_movers,sk4(sk1(sk3))),X0)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p4750,c0]) ).
cnf(p6273,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p6266,p4777]) ).
cnf(p7596,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p6273]) ).
cnf(p7621,plain,
( sk2(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p7596]) ).
cnf(p7623,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p7621]) ).
cnf(p7631,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p7623,p4750]) ).
cnf(p7714,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p7631]) ).
cnf(p7716,plain,
( sk2(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p7714]) ).
cnf(p7718,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p7716]) ).
cnf(p7722,plain,
( greater_or_equal(growth_rate(efficient_producers,sk1(sk3)),zero)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p7718,c3]) ).
cnf(p4743,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p4739,p30]) ).
cnf(p4764,plain,
( outcompetes(efficient_producers,first_movers,sk1(sk3))
| ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ greater_or_equal(growth_rate(efficient_producers,sk1(sk3)),zero)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p4743,p34]) ).
cnf(p7726,plain,
( outcompetes(efficient_producers,first_movers,sk1(sk3))
| ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p7722,p4764]) ).
cnf(p7747,plain,
( outcompetes(efficient_producers,first_movers,sk1(sk3))
| ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p7726]) ).
cnf(p7761,plain,
( outcompetes(efficient_producers,first_movers,sk1(sk3))
| ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p7747]) ).
cnf(p4757,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| ~ greater_or_equal(sk1(sk3),equilibrium(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p4739,p81]) ).
cnf(p4918,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p4757,p2703]) ).
cnf(p5277,plain,
( sk2(sk3) = sk1(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4918]) ).
cnf(p5612,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5277]) ).
cnf(p5615,plain,
( greater(zero,X0)
| ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),X0)
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p5612,c0]) ).
cnf(p5654,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p5615,p87]) ).
cnf(p5657,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5654]) ).
cnf(p5668,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p4739,p5657]) ).
cnf(p5685,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5668]) ).
cnf(p5688,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5685]) ).
cnf(p4751,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk1(sk3)))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p4739,p87]) ).
cnf(p5693,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p5688,p4751]) ).
cnf(p5723,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5693]) ).
cnf(p5724,plain,
( sk2(sk3) = sk1(sk3)
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5723]) ).
cnf(p5726,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5724]) ).
cnf(p7764,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk1(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p7761,p5726]) ).
cnf(p7769,plain,
( sk2(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk1(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p7764]) ).
cnf(p7771,plain,
( outcompetes(efficient_producers,first_movers,sk1(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p7769]) ).
cnf(p4742,plain,
( ~ outcompetes(efficient_producers,first_movers,sk1(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p4739,p29]) ).
cnf(p7774,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p7771,p4742]) ).
cnf(p7789,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p7774]) ).
cnf(p7791,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p7789]) ).
cnf(p7796,plain,
( greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p7791,p39]) ).
cnf(p7903,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p7796,p86]) ).
cnf(p7913,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p7903,p137]) ).
cnf(p8102,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p7913]) ).
cnf(p8105,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p8102,p131]) ).
cnf(p9494,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p8105]) ).
cnf(p10221,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p9494]) ).
cnf(p10222,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10221]) ).
cnf(p7909,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),X0)
| ~ greater(growth_rate(first_movers,sk4(sk2(sk3))),X0)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p7903,c0]) ).
cnf(p10226,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p10222,p7909]) ).
cnf(p10288,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10226]) ).
cnf(p10290,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p10288,c3]) ).
cnf(p10291,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p10290,p46]) ).
cnf(p10309,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10291]) ).
cnf(p10311,plain,
( growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p10309,p8102]) ).
cnf(p10449,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10311]) ).
cnf(p10451,plain,
( sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10449]) ).
cnf(p10452,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10451]) ).
cnf(p10458,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p10452,p7903]) ).
cnf(p10504,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10458]) ).
cnf(p10506,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p10504,c3]) ).
cnf(p10507,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p10506,p46]) ).
cnf(p10523,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10507]) ).
cnf(p7914,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p7903,p142]) ).
cnf(p8118,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p7914]) ).
cnf(p10525,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p10523,p8118]) ).
cnf(p10538,plain,
( growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10525]) ).
cnf(p10539,plain,
( growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10538]) ).
cnf(p10540,plain,
( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p7791,p10539]) ).
cnf(p10547,plain,
( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10540]) ).
cnf(p10548,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p10547,p87]) ).
cnf(p10524,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p7791,p10523]) ).
cnf(p10531,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10524]) ).
cnf(p10551,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p10548,p10531]) ).
cnf(p10560,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10551]) ).
cnf(p10563,plain,
( sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10560]) ).
cnf(p10564,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10563]) ).
cnf(p10566,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p10564,p40]) ).
cnf(p10570,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| ~ greater_or_equal(sk2(sk3),equilibrium(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p10566,p64]) ).
cnf(p10871,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p10570,p91]) ).
cnf(p11148,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p10566,p10871]) ).
cnf(p11911,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p11148]) ).
cnf(p12065,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p10566,p11911]) ).
cnf(p14402,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p12065]) ).
cnf(p10580,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk4(sk2(sk3))))
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p10566,p7903]) ).
cnf(p10917,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk4(sk2(sk3))))
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10580]) ).
cnf(p14415,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| sk2(sk3) = equilibrium(sk3)
| greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p14402,p10917]) ).
cnf(p14445,plain,
( sk2(sk3) = equilibrium(sk3)
| greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p14415]) ).
cnf(p14446,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p14445]) ).
cnf(p14448,plain,
( greater_or_equal(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p14446,c3]) ).
cnf(p10568,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk2(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p10566,p41]) ).
cnf(p10622,plain,
( outcompetes(efficient_producers,first_movers,sk2(sk3))
| ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| ~ greater_or_equal(growth_rate(efficient_producers,sk2(sk3)),zero)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p10568,p34]) ).
cnf(p14454,plain,
( outcompetes(efficient_producers,first_movers,sk2(sk3))
| ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| sk2(sk3) = equilibrium(sk3)
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p14448,p10622]) ).
cnf(p14465,plain,
( outcompetes(efficient_producers,first_movers,sk2(sk3))
| ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p14454]) ).
cnf(p10578,plain,
( sk4(sk1(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p7791,p10566]) ).
cnf(p10637,plain,
( sk4(sk1(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10578]) ).
cnf(p10652,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| ~ greater_or_equal(sk2(sk3),equilibrium(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p10637,p81]) ).
cnf(p11012,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p10652,p91]) ).
cnf(p11310,plain,
( greater(zero,X0)
| ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),X0)
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p11012,c0]) ).
cnf(p12722,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p11310,p87]) ).
cnf(p12733,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p12722]) ).
cnf(p12736,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p10637,p12733]) ).
cnf(p12762,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p12736]) ).
cnf(p10646,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk2(sk3)))
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p10637,p87]) ).
cnf(p12767,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| sk2(sk3) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk2(sk3)))
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p12762,p10646]) ).
cnf(p12788,plain,
( sk2(sk3) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk2(sk3)))
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p12767]) ).
cnf(p12793,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p12788]) ).
cnf(p14469,plain,
( sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk2(sk3))
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p14465,p12793]) ).
cnf(p14470,plain,
( outcompetes(efficient_producers,first_movers,sk2(sk3))
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p14469]) ).
cnf(p10645,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk4(sk1(sk3))))
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p10637,p87]) ).
cnf(p10657,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p10637,p10645]) ).
cnf(p10901,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10657]) ).
cnf(p10902,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),X0)
| ~ greater(growth_rate(first_movers,sk2(sk3)),X0)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p10901,c0]) ).
cnf(p14476,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk2(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p14470,p10902]) ).
cnf(p14535,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| outcompetes(efficient_producers,first_movers,sk2(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p14476]) ).
cnf(p14547,plain,
( greater_or_equal(growth_rate(efficient_producers,sk2(sk3)),zero)
| outcompetes(efficient_producers,first_movers,sk2(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p14535,c3]) ).
cnf(p14552,plain,
( outcompetes(efficient_producers,first_movers,sk2(sk3))
| ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk2(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p14547,p10622]) ).
cnf(p14646,plain,
( outcompetes(efficient_producers,first_movers,sk2(sk3))
| ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| outcompetes(efficient_producers,first_movers,sk2(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p14552]) ).
cnf(p14648,plain,
( ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| outcompetes(efficient_producers,first_movers,sk2(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p14646]) ).
cnf(p14651,plain,
( sk2(sk3) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk2(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p14648,p12793]) ).
cnf(p14652,plain,
( outcompetes(efficient_producers,first_movers,sk2(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p14651]) ).
cnf(p10567,plain,
( ~ outcompetes(efficient_producers,first_movers,sk2(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p10566,p40]) ).
cnf(p14664,plain,
( sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p14652,p10567]) ).
cnf(p14666,plain,
sk2(sk3) = equilibrium(sk3),
inference(factoring,[status(thm)],[p14664]) ).
cnf(p14696,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),growth_rate(first_movers,sk4(equilibrium(sk3)))) ),
inference(demodulation,[status(thm)],[p14666,p95]) ).
cnf(p14694,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| ~ greater_or_equal(sk4(equilibrium(sk3)),equilibrium(sk3)) ),
inference(demodulation,[status(thm)],[p14666,p82]) ).
cnf(p14668,plain,
greater_or_equal(sk4(equilibrium(sk3)),equilibrium(sk3)),
inference(demodulation,[status(thm)],[p14666,p39]) ).
cnf(p14908,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p14694,p14668]) ).
cnf(p14909,plain,
( greater(zero,X0)
| ~ greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),X0)
| greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p14908,c0]) ).
cnf(p14912,plain,
( ~ greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(factoring,[status(thm)],[p14909]) ).
cnf(p14916,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p14696,p14912]) ).
cnf(f12,hypothesis,
( greater(growth_rate(efficient_producers,B),zero)
| greater(growth_rate(first_movers,B),zero)
| growth_rate(efficient_producers,B) = zero
| ~ greater_or_equal(B,equilibrium(A))
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ environment(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l6_34) ).
fof(f12_nnf,plain,
! [A,B] :
( greater(growth_rate(efficient_producers,B),zero)
| greater(growth_rate(first_movers,B),zero)
| growth_rate(efficient_producers,B) = zero
| ~ greater_or_equal(B,equilibrium(A))
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ environment(A) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [A,B] :
( greater(growth_rate(efficient_producers,B),zero)
| greater(growth_rate(first_movers,B),zero)
| growth_rate(efficient_producers,B) = zero
| ~ greater_or_equal(B,equilibrium(A))
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ environment(A) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( greater(growth_rate(efficient_producers,X1),zero)
| greater(growth_rate(first_movers,X1),zero)
| growth_rate(efficient_producers,X1) = zero
| ~ greater_or_equal(X1,equilibrium(X0))
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p69,plain,
( greater(growth_rate(efficient_producers,X0),zero)
| greater(growth_rate(first_movers,X0),zero)
| growth_rate(efficient_producers,X0) = zero
| ~ greater_or_equal(X0,equilibrium(sk3))
| ~ subpopulations(first_movers,efficient_producers,sk3,X0) ),
inference(resolution,[status(thm)],[c12,c20]) ).
cnf(p73,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| ~ greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[p69,p41]) ).
cnf(p14691,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| ~ greater_or_equal(sk4(equilibrium(sk3)),equilibrium(sk3)) ),
inference(demodulation,[status(thm)],[p14666,p73]) ).
cnf(p14894,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p14691,p14668]) ).
cnf(p14896,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p14894,c3]) ).
cnf(p14674,plain,
( outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| ~ greater_or_equal(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero) ),
inference(demodulation,[status(thm)],[p14666,p46]) ).
cnf(p14897,plain,
( outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p14896,p14674]) ).
cnf(p14929,plain,
( outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p14916,p14897]) ).
cnf(p15061,plain,
( outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p14929]) ).
cnf(p14698,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),X0)
| ~ greater(growth_rate(first_movers,sk4(equilibrium(sk3))),X0)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(demodulation,[status(thm)],[p14666,p107]) ).
cnf(p15064,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p15061,p14698]) ).
cnf(p15247,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p15064]) ).
cnf(p15250,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| greater(sk1(sk3),equilibrium(sk3))
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p15247]) ).
cnf(p15252,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p15250]) ).
cnf(p15254,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p15252,c3]) ).
cnf(p15256,plain,
( outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p15254,p14674]) ).
cnf(p15263,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p15256]) ).
cnf(p15264,plain,
( growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p15263,p14916]) ).
cnf(p15689,plain,
( growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p15264]) ).
cnf(p16239,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p15689]) ).
cnf(p16250,plain,
( greater(sk1(sk3),equilibrium(sk3))
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p16239]) ).
cnf(p16252,plain,
( outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p16250]) ).
cnf(p16259,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p16252,p14696]) ).
cnf(p16517,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p16259]) ).
cnf(p16940,plain,
( greater(sk1(sk3),equilibrium(sk3))
| greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p16517]) ).
cnf(p16944,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p16940]) ).
cnf(f4,axiom,
( greater_or_equal(A,B)
| A != B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_or_equal_26) ).
fof(f4_nnf,plain,
! [A,B] :
( greater_or_equal(A,B)
| A != B ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,B] :
( greater_or_equal(A,B)
| A != B ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( greater_or_equal(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p16257,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p16252,c4]) ).
cnf(p16263,plain,
( outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p16257,p14674]) ).
cnf(p16264,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p16263]) ).
cnf(p16947,plain,
( outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p16944,p16264]) ).
cnf(p17757,plain,
( outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p16947]) ).
cnf(p17763,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p17757]) ).
cnf(p17764,plain,
( greater(sk1(sk3),equilibrium(sk3))
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p17763]) ).
cnf(p17766,plain,
( outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p17764]) ).
cnf(p14669,plain,
~ outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3))),
inference(demodulation,[status(thm)],[p14666,p40]) ).
cnf(p17767,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p17766,p14669]) ).
cnf(p14687,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| ~ greater_or_equal(sk4(equilibrium(sk3)),equilibrium(sk3)) ),
inference(demodulation,[status(thm)],[p14666,p64]) ).
cnf(p14874,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p14687,p14668]) ).
cnf(p17772,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p17767,p14874]) ).
cnf(p17829,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(growth_rate(first_movers,equilibrium(sk3)),zero)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p17767,p17772]) ).
cnf(p18167,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(growth_rate(first_movers,equilibrium(sk3)),zero)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p17829]) ).
cnf(p18169,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(growth_rate(first_movers,equilibrium(sk3)),zero)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18167]) ).
cnf(p14695,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),growth_rate(first_movers,sk4(equilibrium(sk3))))
| ~ greater_or_equal(sk4(equilibrium(sk3)),sk1(sk3)) ),
inference(demodulation,[status(thm)],[p14666,p86]) ).
cnf(p17770,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),growth_rate(first_movers,sk4(equilibrium(sk3))))
| ~ greater_or_equal(equilibrium(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p17767,p14695]) ).
cnf(p14677,plain,
( greater_or_equal(equilibrium(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(demodulation,[status(thm)],[p14666,p50]) ).
cnf(p17820,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p17770,p14677]) ).
cnf(p17939,plain,
( greater(sk1(sk3),equilibrium(sk3))
| greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p17820]) ).
cnf(p17941,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p17939]) ).
cnf(p17948,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p17767,p17941]) ).
cnf(p17973,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(sk1(sk3),equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p17948]) ).
cnf(p17975,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p17973]) ).
cnf(p18176,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(growth_rate(first_movers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p18169,p17975]) ).
cnf(p18182,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(growth_rate(first_movers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18176]) ).
cnf(p18183,plain,
( greater(sk1(sk3),equilibrium(sk3))
| greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(growth_rate(first_movers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18182]) ).
cnf(p18187,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(growth_rate(first_movers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18183]) ).
cnf(p18189,plain,
( greater_or_equal(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(growth_rate(first_movers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18187,c3]) ).
cnf(p14670,plain,
subpopulations(first_movers,efficient_producers,sk3,sk4(equilibrium(sk3))),
inference(demodulation,[status(thm)],[p14666,p41]) ).
cnf(p17769,plain,
( subpopulations(first_movers,efficient_producers,sk3,equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p17767,p14670]) ).
cnf(p17808,plain,
( outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| ~ greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| ~ greater_or_equal(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p17769,p34]) ).
cnf(p18190,plain,
( outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| ~ greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(growth_rate(first_movers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18189,p17808]) ).
cnf(p18194,plain,
( outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| ~ greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| greater(growth_rate(first_movers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18190]) ).
cnf(p18196,plain,
( outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| ~ greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| greater(growth_rate(first_movers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18194]) ).
cnf(p17947,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p17941,p14912]) ).
cnf(p17968,plain,
( greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p17767,p17947]) ).
cnf(p18094,plain,
( greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p17968]) ).
cnf(p18096,plain,
( greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18094]) ).
cnf(p17949,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),growth_rate(first_movers,equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p17767,p17941]) ).
cnf(p17982,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),growth_rate(first_movers,equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p17949]) ).
cnf(p17984,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),growth_rate(first_movers,equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p17982]) ).
cnf(p18101,plain,
( greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p18096,p17984]) ).
cnf(p18108,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18101]) ).
cnf(p18109,plain,
( greater(sk1(sk3),equilibrium(sk3))
| greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18108]) ).
cnf(p18111,plain,
( greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18109]) ).
cnf(p18197,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| greater(growth_rate(first_movers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18196,p18111]) ).
cnf(p18198,plain,
( greater(sk1(sk3),equilibrium(sk3))
| outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| greater(growth_rate(first_movers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18197]) ).
cnf(p18202,plain,
( outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| greater(growth_rate(first_movers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18198]) ).
cnf(p17817,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),growth_rate(first_movers,equilibrium(sk3)))
| ~ greater_or_equal(equilibrium(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p17769,p84]) ).
cnf(p17818,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,equilibrium(sk3)),growth_rate(first_movers,equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p17817,p14677]) ).
cnf(p17822,plain,
( greater(sk1(sk3),equilibrium(sk3))
| greater(growth_rate(efficient_producers,equilibrium(sk3)),growth_rate(first_movers,equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p17818]) ).
cnf(p17824,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),growth_rate(first_movers,equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p17822]) ).
cnf(p17825,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),X0)
| ~ greater(growth_rate(first_movers,equilibrium(sk3)),X0)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p17824,c0]) ).
cnf(p18205,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18202,p17825]) ).
cnf(p18216,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18205]) ).
cnf(p18218,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18216]) ).
cnf(p18220,plain,
( greater_or_equal(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18218,c3]) ).
cnf(p18221,plain,
( outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| ~ greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18220,p17808]) ).
cnf(p18241,plain,
( outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| ~ greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18221]) ).
cnf(p18244,plain,
( outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| ~ greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18241]) ).
cnf(p18248,plain,
( ~ greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18244]) ).
cnf(p18249,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18248,p18111]) ).
cnf(p18250,plain,
( greater(sk1(sk3),equilibrium(sk3))
| outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18249]) ).
cnf(p18252,plain,
( outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18250]) ).
cnf(p17768,plain,
( ~ outcompetes(efficient_producers,first_movers,equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p17767,p14669]) ).
cnf(p18253,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18252,p17768]) ).
cnf(p18254,plain,
( greater(sk1(sk3),equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18253]) ).
cnf(p18256,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18254]) ).
cnf(p18259,plain,
( greater(sk4(sk1(sk3)),equilibrium(sk3))
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18256,p33]) ).
cnf(p18261,plain,
( greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18259,c3]) ).
cnf(p72,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| ~ greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[p69,p30]) ).
cnf(p18266,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18261,p72]) ).
cnf(p18286,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18266,c3]) ).
cnf(p18304,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18286,p35]) ).
cnf(p18269,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18261,p81]) ).
cnf(p18292,plain,
( greater(zero,X0)
| ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),X0)
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18269,c0]) ).
cnf(p18358,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18292,p87]) ).
cnf(p18359,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18358]) ).
cnf(p18381,plain,
( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18304,p18359]) ).
cnf(p19359,plain,
( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18381]) ).
cnf(p20421,plain,
( sk4(sk1(sk3)) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p19359]) ).
cnf(p20441,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p20421]) ).
cnf(p20444,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p20441,p88]) ).
cnf(p20448,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p20444,c3]) ).
cnf(p20449,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p20448,p35]) ).
cnf(p20481,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p20449]) ).
cnf(p20482,plain,
( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p20481,p18359]) ).
cnf(p21990,plain,
( sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p20482]) ).
cnf(p22121,plain,
( equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p21990]) ).
cnf(p22122,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p22121]) ).
cnf(p22123,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p22122,p87]) ).
cnf(p18262,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18261,p63]) ).
cnf(p18271,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18262,c3]) ).
cnf(p18300,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18271,p35]) ).
cnf(p18265,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18261,p70]) ).
cnf(p18277,plain,
( greater(zero,X0)
| ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),X0)
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18265,c0]) ).
cnf(p18325,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18277,p87]) ).
cnf(p18326,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18325]) ).
cnf(p18377,plain,
( growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18300,p18326]) ).
cnf(p19338,plain,
( growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p18377]) ).
cnf(p20393,plain,
( sk4(sk1(sk3)) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p19338]) ).
cnf(p20394,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p20393]) ).
cnf(p20397,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p20394,p88]) ).
cnf(p20399,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p20397,c3]) ).
cnf(p20402,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p20399,p35]) ).
cnf(p20434,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p20402]) ).
cnf(p20437,plain,
( growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p20434,p18326]) ).
cnf(p21719,plain,
( sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p20437]) ).
cnf(p22088,plain,
( equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p21719]) ).
cnf(p22090,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p22088]) ).
cnf(p22093,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p22090,p89]) ).
cnf(p22097,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p22093,p35]) ).
cnf(p22105,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p22097]) ).
cnf(p22136,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p22123,p22105]) ).
cnf(p22140,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p22136]) ).
cnf(p22143,plain,
( equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p22140]) ).
cnf(p22146,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p22143]) ).
cnf(p22147,plain,
( sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p22146,p29]) ).
cnf(p22151,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| ~ greater_or_equal(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p22147,p63]) ).
cnf(p18258,plain,
( greater_or_equal(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p18256,c3]) ).
cnf(p22407,plain,
( equilibrium(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p22151,p18258]) ).
cnf(p22425,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p22407]) ).
cnf(p22429,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| equilibrium(sk3) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p22147,p22425]) ).
cnf(p22439,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p22429]) ).
cnf(p22156,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk4(sk1(sk3))))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p22147,p87]) ).
cnf(p22207,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),X0)
| ~ greater(growth_rate(first_movers,sk4(sk1(sk3))),X0)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p22156,c0]) ).
cnf(p22450,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| equilibrium(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p22439,p22207]) ).
cnf(p23041,plain,
( equilibrium(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p22450]) ).
cnf(p23042,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p23041]) ).
cnf(p23048,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| equilibrium(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p23042,p22156]) ).
cnf(p23075,plain,
( equilibrium(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p23048]) ).
cnf(p23078,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p23075]) ).
cnf(p23080,plain,
( greater_or_equal(growth_rate(efficient_producers,sk1(sk3)),zero)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p23078,c3]) ).
cnf(p22149,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p22147,p30]) ).
cnf(p22197,plain,
( outcompetes(efficient_producers,first_movers,sk1(sk3))
| ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| ~ greater_or_equal(growth_rate(efficient_producers,sk1(sk3)),zero)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p22149,p34]) ).
cnf(p23081,plain,
( outcompetes(efficient_producers,first_movers,sk1(sk3))
| ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| equilibrium(sk3) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p23080,p22197]) ).
cnf(p23091,plain,
( outcompetes(efficient_producers,first_movers,sk1(sk3))
| ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p23081]) ).
cnf(p22205,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| growth_rate(efficient_producers,sk1(sk3)) = zero
| ~ greater_or_equal(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p22149,p80]) ).
cnf(p22253,plain,
( equilibrium(sk3) = sk1(sk3)
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| growth_rate(efficient_producers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p22205,p18258]) ).
cnf(p22371,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| growth_rate(efficient_producers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p22253]) ).
cnf(p22372,plain,
( greater(zero,X0)
| ~ greater(growth_rate(efficient_producers,sk1(sk3)),X0)
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| growth_rate(efficient_producers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p22371,c0]) ).
cnf(p22387,plain,
( ~ greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3)))
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| growth_rate(efficient_producers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p22372]) ).
cnf(p22206,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3)))
| ~ greater_or_equal(sk1(sk3),sk1(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p22149,p84]) ).
cnf(p25,plain,
greater_or_equal(X0,X0),
inference(equality_resolution,[status(thm)],[c4]) ).
cnf(p22214,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3)))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p22206,p25]) ).
cnf(p22390,plain,
( equilibrium(sk3) = sk1(sk3)
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| growth_rate(efficient_producers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p22387,p22214]) ).
cnf(p22391,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| growth_rate(efficient_producers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p22390]) ).
cnf(p23094,plain,
( growth_rate(efficient_producers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk1(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p23091,p22391]) ).
cnf(p23123,plain,
( growth_rate(efficient_producers,sk1(sk3)) = zero
| outcompetes(efficient_producers,first_movers,sk1(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p23094]) ).
cnf(p23126,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk1(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p23123,p22214]) ).
cnf(p23135,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| outcompetes(efficient_producers,first_movers,sk1(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p23126]) ).
cnf(p23148,plain,
( outcompetes(efficient_producers,first_movers,sk1(sk3))
| equilibrium(sk3) = sk1(sk3)
| outcompetes(efficient_producers,first_movers,sk1(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p23135,p23091]) ).
cnf(p23150,plain,
( outcompetes(efficient_producers,first_movers,sk1(sk3))
| outcompetes(efficient_producers,first_movers,sk1(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p23148]) ).
cnf(p23152,plain,
( outcompetes(efficient_producers,first_movers,sk1(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p23150]) ).
cnf(p22148,plain,
( ~ outcompetes(efficient_producers,first_movers,sk1(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p22147,p29]) ).
cnf(p23153,plain,
( equilibrium(sk3) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p23152,p22148]) ).
cnf(p23155,plain,
equilibrium(sk3) = sk1(sk3),
inference(factoring,[status(thm)],[p23153]) ).
cnf(p23157,plain,
greater_or_equal(sk4(equilibrium(sk3)),sk1(sk3)),
inference(superposition,[status(thm)],[p23155,p28]) ).
cnf(p23228,plain,
greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),growth_rate(first_movers,sk4(equilibrium(sk3)))),
inference(resolution,[status(thm)],[p23157,p14695]) ).
cnf(p14690,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| ~ greater_or_equal(sk4(equilibrium(sk3)),equilibrium(sk3)) ),
inference(demodulation,[status(thm)],[p14666,p71]) ).
cnf(p14889,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(equilibrium(sk3))))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p14690,p14668]) ).
cnf(p14890,plain,
( greater(zero,X0)
| ~ greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),X0)
| greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p14889,c0]) ).
cnf(p14893,plain,
( ~ greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(factoring,[status(thm)],[p14890]) ).
cnf(p23256,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p23228,p14893]) ).
cnf(p14876,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p14874,c3]) ).
cnf(p14877,plain,
( outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p14876,p14674]) ).
cnf(p23278,plain,
( outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p23256,p14877]) ).
cnf(p23481,plain,
( outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(factoring,[status(thm)],[p23278]) ).
cnf(p23254,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),X0)
| ~ greater(growth_rate(first_movers,sk4(equilibrium(sk3))),X0) ),
inference(resolution,[status(thm)],[p23228,c0]) ).
cnf(p23485,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p23481,p23254]) ).
cnf(p23494,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p23485,c3]) ).
cnf(p23497,plain,
( outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p23494,p14674]) ).
cnf(p23566,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(factoring,[status(thm)],[p23497]) ).
cnf(p23568,plain,
( growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p23566,p23256]) ).
cnf(p23572,plain,
( outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(factoring,[status(thm)],[p23568]) ).
cnf(p23170,plain,
greater_or_equal(growth_rate(efficient_producers,sk4(equilibrium(sk3))),growth_rate(first_movers,sk4(sk1(sk3)))),
inference(superposition,[status(thm)],[p23155,p89]) ).
cnf(p23249,plain,
greater_or_equal(growth_rate(efficient_producers,sk4(equilibrium(sk3))),growth_rate(first_movers,sk4(equilibrium(sk3)))),
inference(superposition,[status(thm)],[p23155,p23170]) ).
cnf(p23580,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3))) ),
inference(superposition,[status(thm)],[p23572,p23249]) ).
cnf(p23585,plain,
( outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3))) ),
inference(resolution,[status(thm)],[p23580,p14674]) ).
cnf(p23598,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3))) ),
inference(factoring,[status(thm)],[p23585]) ).
cnf(p23258,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p23228,p14912]) ).
cnf(p23599,plain,
( growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3))) ),
inference(resolution,[status(thm)],[p23598,p23258]) ).
cnf(p23605,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3))) ),
inference(superposition,[status(thm)],[p23599,p23228]) ).
cnf(p23611,plain,
( outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3)))
| outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3))) ),
inference(resolution,[status(thm)],[p23605,p23598]) ).
cnf(p23612,plain,
outcompetes(efficient_producers,first_movers,sk4(equilibrium(sk3))),
inference(factoring,[status(thm)],[p23611]) ).
cnf(p23613,plain,
$false,
inference(resolution,[status(thm)],[p23612,p14669]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT035-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/0.38 % Computer : n002.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Thu Sep 24 01:10:20 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 117.60/33.11 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 117.60/33.11 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------