%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : MGT029-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n017.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:23 PM UTC 2026
% Result : Unsatisfiable 59.76s 13.09s
% Output : Proof 59.76s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
cnf(f8,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/sandbox/benchmark/theBenchmark.p',l6_27) ).
fof(f8_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)],[f8]) ).
fof(f8_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)],[f8_nnf]) ).
cnf(c8,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)],[f8_sk]) ).
cnf(f17,negated_conjecture,
environment(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l11_36) ).
fof(f17_nnf,plain,
environment(sk3),
inference(nnf_transformation,[status(thm)],[f17]) ).
cnf(c17,plain,
environment(sk3),
inference(cnf_transformation,[status(esa)],[f17_nnf]) ).
cnf(p48,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)],[c8,c17]) ).
cnf(f15,hypothesis,
( in_environment(A,sk2(A))
| ~ stable(A)
| ~ environment(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a4_34) ).
fof(f15_nnf,plain,
! [A] :
( in_environment(A,sk2(A))
| ~ stable(A)
| ~ environment(A) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [A] :
( in_environment(A,sk2(A))
| ~ stable(A)
| ~ environment(A) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( in_environment(X0,sk2(X0))
| ~ stable(X0)
| ~ environment(X0) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p33,plain,
( in_environment(sk3,sk2(sk3))
| ~ stable(sk3) ),
inference(resolution,[status(thm)],[c15,c17]) ).
cnf(f18,negated_conjecture,
stable(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l11_37) ).
fof(f18_nnf,plain,
stable(sk3),
inference(nnf_transformation,[status(thm)],[f18]) ).
cnf(c18,plain,
stable(sk3),
inference(cnf_transformation,[status(esa)],[f18_nnf]) ).
cnf(p35,plain,
in_environment(sk3,sk2(sk3)),
inference(resolution,[status(thm)],[p33,c18]) ).
cnf(f19,negated_conjecture,
( subpopulations(first_movers,efficient_producers,sk3,sk4(A))
| ~ in_environment(sk3,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l11_38) ).
fof(f19_nnf,plain,
! [A] :
( subpopulations(first_movers,efficient_producers,sk3,sk4(A))
| ~ in_environment(sk3,A) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [A] :
( subpopulations(first_movers,efficient_producers,sk3,sk4(A))
| ~ in_environment(sk3,A) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk4(X0))
| ~ in_environment(sk3,X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p37,plain,
subpopulations(first_movers,efficient_producers,sk3,sk4(sk2(sk3))),
inference(resolution,[status(thm)],[p35,c19]) ).
cnf(p65,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)],[p48,p37]) ).
cnf(f16,hypothesis,
( greater_or_equal(sk2(A),equilibrium(A))
| ~ stable(A)
| ~ environment(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a4_35) ).
fof(f16_nnf,plain,
! [A] :
( greater_or_equal(sk2(A),equilibrium(A))
| ~ stable(A)
| ~ environment(A) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [A] :
( greater_or_equal(sk2(A),equilibrium(A))
| ~ stable(A)
| ~ environment(A) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( greater_or_equal(sk2(X0),equilibrium(X0))
| ~ stable(X0)
| ~ environment(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p82,plain,
( greater_or_equal(sk2(sk3),equilibrium(sk3))
| ~ stable(sk3) ),
inference(resolution,[status(thm)],[c16,c17]) ).
cnf(p83,plain,
greater_or_equal(sk2(sk3),equilibrium(sk3)),
inference(resolution,[status(thm)],[p82,c18]) ).
cnf(f2,axiom,
( A = B
| greater(A,B)
| ~ greater_or_equal(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal_21) ).
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(p84,plain,
( sk2(sk3) = equilibrium(sk3)
| greater(sk2(sk3),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[p83,c2]) ).
cnf(f20,negated_conjecture,
( greater_or_equal(sk4(A),A)
| ~ in_environment(sk3,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l11_39) ).
fof(f20_nnf,plain,
! [A] :
( greater_or_equal(sk4(A),A)
| ~ in_environment(sk3,A) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [A] :
( greater_or_equal(sk4(A),A)
| ~ in_environment(sk3,A) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( greater_or_equal(sk4(X0),X0)
| ~ in_environment(sk3,X0) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p36,plain,
greater_or_equal(sk4(sk2(sk3)),sk2(sk3)),
inference(resolution,[status(thm)],[p35,c20]) ).
cnf(p41,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| greater(sk4(sk2(sk3)),sk2(sk3)) ),
inference(resolution,[status(thm)],[p36,c2]) ).
cnf(f0,axiom,
( greater(A,C)
| ~ greater(B,C)
| ~ greater(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_transitivity_19) ).
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(p44,plain,
( greater(sk4(sk2(sk3)),X0)
| ~ greater(sk2(sk3),X0)
| sk4(sk2(sk3)) = sk2(sk3) ),
inference(resolution,[status(thm)],[p41,c0]) ).
cnf(p86,plain,
( greater(sk4(sk2(sk3)),equilibrium(sk3))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p84,p44]) ).
cnf(f3,axiom,
( greater_or_equal(A,B)
| ~ greater(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal_22) ).
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(p90,plain,
( greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p86,c3]) ).
cnf(p94,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(first_movers,sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[p65,p90]) ).
cnf(p113,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(first_movers,sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[p94,c0]) ).
cnf(p131,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(first_movers,sk4(sk2(sk3))) = zero ),
inference(factoring,[status(thm)],[p113]) ).
cnf(f14,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/sandbox/benchmark/theBenchmark.p',l1_33) ).
fof(f14_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)],[f14]) ).
fof(f14_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)],[f14_nnf]) ).
cnf(c14,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)],[f14_sk]) ).
cnf(p75,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)],[c14,c17]) ).
cnf(p76,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)],[p75,c18]) ).
cnf(p78,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)],[p76,p37]) ).
cnf(f13,hypothesis,
( in_environment(A,sk1(A))
| ~ stable(A)
| ~ environment(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l1_32) ).
fof(f13_nnf,plain,
! [A] :
( in_environment(A,sk1(A))
| ~ stable(A)
| ~ environment(A) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [A] :
( in_environment(A,sk1(A))
| ~ stable(A)
| ~ environment(A) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( in_environment(X0,sk1(X0))
| ~ stable(X0)
| ~ environment(X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p23,plain,
( in_environment(sk3,sk1(sk3))
| ~ stable(sk3) ),
inference(resolution,[status(thm)],[c13,c17]) ).
cnf(p24,plain,
in_environment(sk3,sk1(sk3)),
inference(resolution,[status(thm)],[p23,c18]) ).
cnf(f1,axiom,
( greater(B,C)
| C = B
| greater(C,B)
| ~ in_environment(A,C)
| ~ in_environment(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_times_in_environment_20) ).
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(p28,plain,
( greater(sk1(sk3),X0)
| X0 = sk1(sk3)
| greater(X0,sk1(sk3))
| ~ in_environment(sk3,X0) ),
inference(resolution,[status(thm)],[p24,c1]) ).
cnf(p40,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(sk2(sk3),sk1(sk3)) ),
inference(resolution,[status(thm)],[p35,p28]) ).
cnf(p47,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)],[p44,p40]) ).
cnf(p55,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)],[p47,c3]) ).
cnf(p87,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)],[p78,p55]) ).
cnf(p139,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(first_movers,sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[p131,p87]) ).
cnf(p143,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(first_movers,sk4(sk2(sk3))) = zero ),
inference(factoring,[status(thm)],[p139]) ).
cnf(f5,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/sandbox/benchmark/theBenchmark.p',l6_24) ).
fof(f5_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)],[f5]) ).
fof(f5_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)],[f5_nnf]) ).
cnf(c5,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)],[f5_sk]) ).
cnf(p31,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)],[c5,c17]) ).
cnf(p42,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)],[p37,p31]) ).
cnf(p91,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)],[p90,p42]) ).
cnf(f21,negated_conjecture,
( ~ greater(zero,growth_rate(first_movers,sk4(A)))
| ~ greater(growth_rate(efficient_producers,sk4(A)),zero)
| ~ in_environment(sk3,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l11_40) ).
fof(f21_nnf,plain,
! [A] :
( ~ greater(zero,growth_rate(first_movers,sk4(A)))
| ~ greater(growth_rate(efficient_producers,sk4(A)),zero)
| ~ in_environment(sk3,A) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [A] :
( ~ greater(zero,growth_rate(first_movers,sk4(A)))
| ~ greater(growth_rate(efficient_producers,sk4(A)),zero)
| ~ in_environment(sk3,A) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(X0)))
| ~ greater(growth_rate(efficient_producers,sk4(X0)),zero)
| ~ in_environment(sk3,X0) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p38,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero) ),
inference(resolution,[status(thm)],[p35,c21]) ).
cnf(p105,plain,
( ~ 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)],[p91,p38]) ).
cnf(p152,plain,
( 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)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[p143,p105]) ).
cnf(p196,plain,
( 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)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero ),
inference(factoring,[status(thm)],[p152]) ).
cnf(p200,plain,
( greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| sk2(sk3) = equilibrium(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero ),
inference(factoring,[status(thm)],[p196]) ).
cnf(p201,plain,
( greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero ),
inference(factoring,[status(thm)],[p200]) ).
cnf(p99,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)],[p87,c0]) ).
cnf(p209,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[p201,p99]) ).
cnf(p301,plain,
( greater(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)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero ),
inference(factoring,[status(thm)],[p209]) ).
cnf(p306,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| greater(sk1(sk3),sk2(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero ),
inference(factoring,[status(thm)],[p301]) ).
cnf(p313,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero ),
inference(factoring,[status(thm)],[p306]) ).
cnf(p318,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[p313,p38]) ).
cnf(p326,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[p318,p143]) ).
cnf(p449,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero ),
inference(factoring,[status(thm)],[p326]) ).
cnf(p495,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero ),
inference(factoring,[status(thm)],[p449]) ).
cnf(p501,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero ),
inference(factoring,[status(thm)],[p495]) ).
cnf(p504,plain,
( greater(sk1(sk3),sk2(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero ),
inference(factoring,[status(thm)],[p501]) ).
cnf(p506,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero ),
inference(factoring,[status(thm)],[p504]) ).
cnf(p510,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p506,p87]) ).
cnf(p527,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p510]) ).
cnf(p530,plain,
( greater(sk1(sk3),sk2(sk3))
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p527]) ).
cnf(p532,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p530]) ).
cnf(p540,plain,
( ~ greater(zero,growth_rate(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)],[p532,p38]) ).
cnf(f12,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/sandbox/benchmark/theBenchmark.p',l6_31) ).
fof(f12_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)],[f12]) ).
fof(f12_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)],[f12_nnf]) ).
cnf(c12,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)],[f12_sk]) ).
cnf(p72,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)],[c12,c17]) ).
cnf(p74,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)],[p72,p37]) ).
cnf(p98,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)],[p74,p90]) ).
cnf(p125,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)],[p98,c0]) ).
cnf(p136,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)],[p125]) ).
cnf(p141,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)],[p136,p87]) ).
cnf(p177,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)],[p141]) ).
cnf(p550,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
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p540,p177]) ).
cnf(p632,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p550]) ).
cnf(p635,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p632]) ).
cnf(p638,plain,
( greater(sk1(sk3),sk2(sk3))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p635]) ).
cnf(p642,plain,
( growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p638]) ).
cnf(p645,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| greater(zero,growth_rate(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)],[p642,p87]) ).
cnf(p655,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(zero,growth_rate(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)],[p645]) ).
cnf(p658,plain,
( greater(sk1(sk3),sk2(sk3))
| greater(zero,growth_rate(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)],[p655]) ).
cnf(p660,plain,
( greater(zero,growth_rate(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)],[p658]) ).
cnf(p665,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p660,p540]) ).
cnf(p685,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p665]) ).
cnf(p688,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p685]) ).
cnf(p691,plain,
( greater(sk1(sk3),sk2(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p688]) ).
cnf(p693,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p691]) ).
cnf(p702,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)],[p693,p42]) ).
cnf(p767,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)],[p702,p83]) ).
cnf(p800,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)],[p693,p767]) ).
cnf(p1003,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)],[p800]) ).
cnf(p1197,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)],[p1003]) ).
cnf(p1259,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)],[p1197]) ).
cnf(p703,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)],[p693,p78]) ).
cnf(p46,plain,
( greater_or_equal(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p40,c3]) ).
cnf(p743,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)],[p703,p46]) ).
cnf(p768,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)],[p743]) ).
cnf(p770,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)],[p768]) ).
cnf(p778,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)],[p693,p770]) ).
cnf(p960,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)],[p778]) ).
cnf(p963,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)],[p960]) ).
cnf(p965,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)],[p963]) ).
cnf(p968,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)],[p965,c0]) ).
cnf(p1268,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)],[p1259,p968]) ).
cnf(p1647,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| 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)],[p1268]) ).
cnf(p2408,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)],[p1647]) ).
cnf(p2421,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)],[p2408]) ).
cnf(p2423,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)],[p2421]) ).
cnf(p2433,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)],[p2423,p965]) ).
cnf(p2575,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)],[p2433]) ).
cnf(p2576,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)],[p2575]) ).
cnf(p2579,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)],[p2576]) ).
cnf(p2584,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)],[p2579]) ).
cnf(p701,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk2(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)],[p693,p38]) ).
cnf(p2589,plain,
( ~ greater(zero,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(resolution,[status(thm)],[p2584,p701]) ).
cnf(p2600,plain,
( ~ greater(zero,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)],[p2589]) ).
cnf(p2603,plain,
( ~ greater(zero,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)],[p2600]) ).
cnf(p2607,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2603]) ).
cnf(p2610,plain,
( ~ 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(superposition,[status(thm)],[p693,p2607]) ).
cnf(p2624,plain,
( ~ 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)],[p2610]) ).
cnf(p2627,plain,
( ~ 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)],[p2624]) ).
cnf(p2629,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)],[p2627]) ).
cnf(p710,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)],[p693,p74]) ).
cnf(p846,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)],[p710,p83]) ).
cnf(p1044,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)],[p846,c0]) ).
cnf(p1203,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)],[p1044]) ).
cnf(p1235,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)],[p1203,p770]) ).
cnf(p1580,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)],[p1235]) ).
cnf(p1583,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)],[p1580]) ).
cnf(p1585,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)],[p1583]) ).
cnf(p1590,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)],[p693,p1585]) ).
cnf(p2176,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)],[p1590]) ).
cnf(p2182,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)],[p2176]) ).
cnf(p2184,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)],[p2182]) ).
cnf(p779,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)],[p693,p770]) ).
cnf(p970,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)],[p779]) ).
cnf(p983,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)],[p970]) ).
cnf(p988,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)],[p983]) ).
cnf(p2195,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)],[p2184,p988]) ).
cnf(p2504,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)],[p2195]) ).
cnf(p2505,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)],[p2504]) ).
cnf(p2508,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)],[p2505]) ).
cnf(p2510,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)],[p2508]) ).
cnf(p2634,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)],[p2629,p2510]) ).
cnf(p2644,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)],[p2634]) ).
cnf(p2647,plain,
( greater(sk1(sk3),sk2(sk3))
| greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2644]) ).
cnf(p2652,plain,
( greater(sk1(sk3),sk2(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2647]) ).
cnf(p2655,plain,
( greater(sk1(sk3),X0)
| ~ greater(sk2(sk3),X0)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2652,c0]) ).
cnf(p2665,plain,
( sk2(sk3) = equilibrium(sk3)
| greater(sk1(sk3),equilibrium(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2655,p84]) ).
cnf(p2671,plain,
( greater(sk1(sk3),equilibrium(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p2665]) ).
cnf(p25,plain,
greater_or_equal(sk4(sk1(sk3)),sk1(sk3)),
inference(resolution,[status(thm)],[p24,c20]) ).
cnf(p29,plain,
( sk4(sk1(sk3)) = sk1(sk3)
| greater(sk4(sk1(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[c2,p25]) ).
cnf(p30,plain,
( greater(sk4(sk1(sk3)),X0)
| ~ greater(sk1(sk3),X0)
| sk4(sk1(sk3)) = sk1(sk3) ),
inference(resolution,[status(thm)],[p29,c0]) ).
cnf(p2676,plain,
( greater(sk4(sk1(sk3)),equilibrium(sk3))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2671,p30]) ).
cnf(p2696,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)],[p2676,c3]) ).
cnf(p26,plain,
subpopulations(first_movers,efficient_producers,sk3,sk4(sk1(sk3))),
inference(resolution,[status(thm)],[p24,c19]) ).
cnf(p64,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)],[p48,p26]) ).
cnf(p2707,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)],[p2696,p64]) ).
cnf(p2745,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)],[p2707,c0]) ).
cnf(p77,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)],[p76,p26]) ).
cnf(p79,plain,
greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3)))),
inference(resolution,[status(thm)],[p77,p25]) ).
cnf(p2909,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)],[p2745,p79]) ).
cnf(p2910,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)],[p2909]) ).
cnf(p32,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)],[p31,p26]) ).
cnf(p2704,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)],[p2696,p32]) ).
cnf(p27,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero) ),
inference(resolution,[status(thm)],[p24,c21]) ).
cnf(p2729,plain,
( ~ 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)],[p2704,p27]) ).
cnf(p2925,plain,
( 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)
| 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)],[p2910,p2729]) ).
cnf(p3378,plain,
( greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(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)],[p2925]) ).
cnf(p3664,plain,
( greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(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)],[p3378]) ).
cnf(p3665,plain,
( greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| sk2(sk3) = 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)],[p3664]) ).
cnf(p3667,plain,
( 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)],[p3665]) ).
cnf(p80,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),X0)
| ~ greater(growth_rate(first_movers,sk4(sk1(sk3))),X0) ),
inference(resolution,[status(thm)],[p79,c0]) ).
cnf(p3676,plain,
( greater(growth_rate(efficient_producers,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)],[p3667,p80]) ).
cnf(p3695,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(resolution,[status(thm)],[p3676,p27]) ).
cnf(p3704,plain,
( growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(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)],[p3695,p2910]) ).
cnf(p3868,plain,
( sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(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)],[p3704]) ).
cnf(p3871,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(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)],[p3868]) ).
cnf(p3872,plain,
( sk2(sk3) = 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)],[p3871]) ).
cnf(p3874,plain,
( 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)],[p3872]) ).
cnf(p3879,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p3874,p79]) ).
cnf(p3892,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p3879,p27]) ).
cnf(p73,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)],[p72,p26]) ).
cnf(p2711,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)],[p2696,p73]) ).
cnf(p2773,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)],[p2711,c0]) ).
cnf(p2953,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)],[p2773,p79]) ).
cnf(p2954,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)],[p2953]) ).
cnf(p3900,plain,
( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p3892,p2954]) ).
cnf(p3931,plain,
( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p3900]) ).
cnf(p3932,plain,
( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk2(sk3) = sk1(sk3)
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p3931]) ).
cnf(p3934,plain,
( 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)],[p3932]) ).
cnf(p3937,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p3934,p79]) ).
cnf(p3953,plain,
( sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p3937,p3892]) ).
cnf(p3967,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p3953]) ).
cnf(p3969,plain,
( sk2(sk3) = sk1(sk3)
| sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p3967]) ).
cnf(p3971,plain,
( sk4(sk1(sk3)) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p3969]) ).
cnf(p3974,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p3971,p26]) ).
cnf(p3992,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| ~ greater_or_equal(sk1(sk3),equilibrium(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p3974,p31]) ).
cnf(p2675,plain,
( greater_or_equal(sk1(sk3),equilibrium(sk3))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p2671,c3]) ).
cnf(p4045,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p3992,p2675]) ).
cnf(p4198,plain,
( sk2(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4045]) ).
cnf(p4203,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4198]) ).
cnf(p3975,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p3971,p27]) ).
cnf(p4208,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p4203,p3975]) ).
cnf(p4702,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| sk2(sk3) = sk1(sk3)
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4208]) ).
cnf(p4734,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4702]) ).
cnf(p4737,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p3971,p4734]) ).
cnf(p5088,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4737]) ).
cnf(p5090,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5088]) ).
cnf(p3988,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)],[p3971,p73]) ).
cnf(p4155,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)],[p3988,p2675]) ).
cnf(p4536,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)],[p4155]) ).
cnf(p4864,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)],[p4536]) ).
cnf(p4867,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)],[p4864,c0]) ).
cnf(p4907,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)],[p4867,p79]) ).
cnf(p4910,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)],[p4907]) ).
cnf(p4921,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)],[p3971,p4910]) ).
cnf(p4949,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)],[p4921]) ).
cnf(p4951,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)],[p4949]) ).
cnf(p3978,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)],[p3971,p79]) ).
cnf(p4956,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)],[p4951,p3978]) ).
cnf(p4986,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)],[p4956]) ).
cnf(p4987,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)],[p4986]) ).
cnf(p4989,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p4987]) ).
cnf(p5093,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p5090,p4989]) ).
cnf(p5097,plain,
( sk2(sk3) = sk1(sk3)
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5093]) ).
cnf(p5099,plain,
( greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5097]) ).
cnf(p3982,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),X0)
| ~ greater(growth_rate(first_movers,sk1(sk3)),X0)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p3971,p80]) ).
cnf(p5105,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p5099,p3982]) ).
cnf(p5405,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5105]) ).
cnf(p5407,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5405]) ).
cnf(p5412,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p5407,p27]) ).
cnf(p5418,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p3971,p5412]) ).
cnf(p5437,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5418]) ).
cnf(p5439,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5437]) ).
cnf(p5443,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p5439,p4989]) ).
cnf(p5446,plain,
( sk2(sk3) = sk1(sk3)
| growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5443]) ).
cnf(p5449,plain,
( growth_rate(first_movers,sk1(sk3)) = zero
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5446]) ).
cnf(p5453,plain,
( greater(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)],[p5449,p3978]) ).
cnf(p5490,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5453]) ).
cnf(p5492,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5490]) ).
cnf(p5498,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p5492,p27]) ).
cnf(p5504,plain,
( ~ 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(superposition,[status(thm)],[p3971,p5498]) ).
cnf(p5523,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5504]) ).
cnf(p5525,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5523]) ).
cnf(p5528,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p5525,p4989]) ).
cnf(p5532,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5528]) ).
cnf(p5534,plain,
( sk2(sk3) = sk1(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5532]) ).
cnf(p5539,plain,
( greater_or_equal(sk4(sk2(sk3)),sk1(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p5534,p36]) ).
cnf(p5606,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p5539,p78]) ).
cnf(p5615,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p5606,p131]) ).
cnf(p5741,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5615]) ).
cnf(p5744,plain,
( 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)
| sk4(sk2(sk3)) = sk2(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p5741,p105]) ).
cnf(p6067,plain,
( greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5744]) ).
cnf(p7409,plain,
( greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| sk4(sk2(sk3)) = sk2(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p6067]) ).
cnf(p7413,plain,
( greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| sk4(sk2(sk3)) = sk2(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p7409]) ).
cnf(p7416,plain,
( greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| sk4(sk2(sk3)) = sk2(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p5534,p7413]) ).
cnf(p7445,plain,
( greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| sk4(sk2(sk3)) = sk2(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p7416]) ).
cnf(p7448,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| sk4(sk2(sk3)) = sk2(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p7445,p80]) ).
cnf(p7462,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| sk4(sk2(sk3)) = sk2(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p7448,p27]) ).
cnf(p5750,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p5534,p5741]) ).
cnf(p5767,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5750]) ).
cnf(p7465,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p7462,p5767]) ).
cnf(p8268,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p7465]) ).
cnf(p8271,plain,
( sk2(sk3) = equilibrium(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p8268]) ).
cnf(p8272,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| growth_rate(first_movers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p8271]) ).
cnf(p8274,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p5534,p8272]) ).
cnf(p8320,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p8274]) ).
cnf(p8322,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p8320,p79]) ).
cnf(p8333,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p8322,p27]) ).
cnf(p5616,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)],[p5606,p136]) ).
cnf(p5755,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)],[p5616]) ).
cnf(p5762,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p5534,p5755]) ).
cnf(p5774,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p5762]) ).
cnf(p8335,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p8333,p5774]) ).
cnf(p8382,plain,
( growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| sk2(sk3) = equilibrium(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p8335]) ).
cnf(p8383,plain,
( growth_rate(efficient_producers,sk4(sk2(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p8382]) ).
cnf(p8384,plain,
( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p5534,p8383]) ).
cnf(p8394,plain,
( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p8384]) ).
cnf(p8395,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p8394,p79]) ).
cnf(p8399,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p8395,p8333]) ).
cnf(p8404,plain,
( sk2(sk3) = equilibrium(sk3)
| sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p8399]) ).
cnf(p8405,plain,
( sk4(sk2(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p8404]) ).
cnf(p8416,plain,
( sk4(sk1(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p5534,p8405]) ).
cnf(p8467,plain,
( sk4(sk1(sk3)) = sk2(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p8416]) ).
cnf(p8406,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk2(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p8405,p37]) ).
cnf(p8457,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| growth_rate(first_movers,sk2(sk3)) = zero
| ~ greater_or_equal(sk2(sk3),equilibrium(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p8406,p31]) ).
cnf(p8742,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p8457,p83]) ).
cnf(p8407,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ greater(growth_rate(efficient_producers,sk2(sk3)),zero)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p8405,p38]) ).
cnf(p8856,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| sk2(sk3) = equilibrium(sk3)
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p8742,p8407]) ).
cnf(p9487,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p8856]) ).
cnf(p9488,plain,
( ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p8405,p9487]) ).
cnf(p9519,plain,
( ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p9488]) ).
cnf(p8460,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| greater(zero,growth_rate(efficient_producers,sk2(sk3)))
| growth_rate(first_movers,sk2(sk3)) = zero
| ~ greater_or_equal(sk2(sk3),equilibrium(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p8406,p48]) ).
cnf(p8752,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| greater(zero,growth_rate(efficient_producers,sk2(sk3)))
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p8460,p83]) ).
cnf(p8874,plain,
( greater(zero,X0)
| ~ greater(growth_rate(efficient_producers,sk2(sk3)),X0)
| greater(zero,growth_rate(first_movers,sk2(sk3)))
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p8752,c0]) ).
cnf(p9271,plain,
( ~ greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))
| greater(zero,growth_rate(first_movers,sk2(sk3)))
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p8874]) ).
cnf(p8471,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk4(sk1(sk3))))
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p8467,p79]) ).
cnf(p8487,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)],[p8467,p8471]) ).
cnf(p8720,plain,
( greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p8487]) ).
cnf(p9282,plain,
( sk2(sk3) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk2(sk3)))
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p9271,p8720]) ).
cnf(p9283,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p9282]) ).
cnf(p9522,plain,
( growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3)
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p9519,p9283]) ).
cnf(p9557,plain,
( sk2(sk3) = equilibrium(sk3)
| greater(growth_rate(first_movers,sk2(sk3)),zero)
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p9522]) ).
cnf(p9559,plain,
( greater(growth_rate(first_movers,sk2(sk3)),zero)
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p9557]) ).
cnf(p8476,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),X0)
| ~ greater(growth_rate(first_movers,sk2(sk3)),X0)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p8467,p80]) ).
cnf(p9564,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p9559,p8476]) ).
cnf(p9631,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p9564]) ).
cnf(p9634,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p9631,p27]) ).
cnf(p9636,plain,
( ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p8467,p9634]) ).
cnf(p9643,plain,
( ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p9636]) ).
cnf(p9645,plain,
( growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p9643,p9283]) ).
cnf(p9658,plain,
( sk2(sk3) = equilibrium(sk3)
| growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p9645]) ).
cnf(p9660,plain,
( growth_rate(first_movers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p9658]) ).
cnf(p8472,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk2(sk3)))
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p8467,p79]) ).
cnf(p9663,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p9660,p8472]) ).
cnf(p9712,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p9663]) ).
cnf(p9715,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p9712,p27]) ).
cnf(p9718,plain,
( ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p8467,p9715]) ).
cnf(p9725,plain,
( ~ greater(zero,growth_rate(first_movers,sk2(sk3)))
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p9718]) ).
cnf(p8464,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| greater(zero,growth_rate(efficient_producers,sk2(sk3)))
| growth_rate(efficient_producers,sk2(sk3)) = zero
| ~ greater_or_equal(sk2(sk3),equilibrium(sk3))
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p8406,p72]) ).
cnf(p8768,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| greater(zero,growth_rate(efficient_producers,sk2(sk3)))
| growth_rate(efficient_producers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p8464,p83]) ).
cnf(p8900,plain,
( greater(zero,X0)
| ~ greater(growth_rate(efficient_producers,sk2(sk3)),X0)
| greater(zero,growth_rate(first_movers,sk2(sk3)))
| growth_rate(efficient_producers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p8768,c0]) ).
cnf(p9303,plain,
( ~ greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))
| greater(zero,growth_rate(first_movers,sk2(sk3)))
| growth_rate(efficient_producers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p8900]) ).
cnf(p9316,plain,
( sk2(sk3) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk2(sk3)))
| growth_rate(efficient_producers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p9303,p8720]) ).
cnf(p9317,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| growth_rate(efficient_producers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p9316]) ).
cnf(p9727,plain,
( growth_rate(efficient_producers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p9725,p9317]) ).
cnf(p9735,plain,
( growth_rate(efficient_producers,sk2(sk3)) = zero
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p9727]) ).
cnf(p9740,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p9735,p8720]) ).
cnf(p9836,plain,
( greater(zero,growth_rate(first_movers,sk2(sk3)))
| sk2(sk3) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p9740]) ).
cnf(p9840,plain,
( sk2(sk3) = equilibrium(sk3)
| sk2(sk3) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p9836,p9725]) ).
cnf(p9841,plain,
sk2(sk3) = equilibrium(sk3),
inference(factoring,[status(thm)],[p9840]) ).
cnf(p9868,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)],[p9841,p74]) ).
cnf(p9843,plain,
greater_or_equal(sk4(equilibrium(sk3)),equilibrium(sk3)),
inference(demodulation,[status(thm)],[p9841,p36]) ).
cnf(p10044,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)],[p9868,p9843]) ).
cnf(p10045,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)],[p10044,c0]) ).
cnf(p10048,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)],[p10045]) ).
cnf(p9870,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)],[p9841,p87]) ).
cnf(p10052,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p10048,p9870]) ).
cnf(f9,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/sandbox/benchmark/theBenchmark.p',l6_28) ).
fof(f9_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)],[f9]) ).
fof(f9_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)],[f9_nnf]) ).
cnf(c9,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)],[f9_sk]) ).
cnf(p53,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)],[c9,c17]) ).
cnf(p67,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)],[p53,p37]) ).
cnf(p9865,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)],[p9841,p67]) ).
cnf(p10030,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)],[p9865,p9843]) ).
cnf(p9845,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| ~ greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero) ),
inference(demodulation,[status(thm)],[p9841,p38]) ).
cnf(p10033,plain,
( ~ 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)],[p10030,p9845]) ).
cnf(p10065,plain,
( 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)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p10052,p10033]) ).
cnf(p10162,plain,
( greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(factoring,[status(thm)],[p10065]) ).
cnf(p9872,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)],[p9841,p99]) ).
cnf(p10167,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p10162,p9872]) ).
cnf(p10355,plain,
( greater(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)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(factoring,[status(thm)],[p10167]) ).
cnf(p10367,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| greater(sk1(sk3),equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(factoring,[status(thm)],[p10355]) ).
cnf(p10369,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(factoring,[status(thm)],[p10367]) ).
cnf(p10372,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p10369,p9845]) ).
cnf(p10377,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p10372,p10052]) ).
cnf(p11073,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(factoring,[status(thm)],[p10377]) ).
cnf(p11086,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(factoring,[status(thm)],[p11073]) ).
cnf(p11092,plain,
( greater(sk1(sk3),equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(factoring,[status(thm)],[p11086]) ).
cnf(p11094,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(factoring,[status(thm)],[p11092]) ).
cnf(p11097,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p11094,p9870]) ).
cnf(p11140,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p11097]) ).
cnf(p11143,plain,
( greater(sk1(sk3),equilibrium(sk3))
| greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p11140]) ).
cnf(p11145,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p11143]) ).
cnf(p9864,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)],[p9841,p65]) ).
cnf(p10025,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)],[p9864,p9843]) ).
cnf(p10026,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)],[p10025,c0]) ).
cnf(p10029,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)],[p10026]) ).
cnf(p10050,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p9870,p10029]) ).
cnf(p9849,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)],[p9841,p42]) ).
cnf(p10010,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)],[p9849,p9843]) ).
cnf(p10013,plain,
( ~ 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)],[p10010,p9845]) ).
cnf(p10059,plain,
( 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
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p10050,p10013]) ).
cnf(p10139,plain,
( 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)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10059]) ).
cnf(p10146,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p10139,p9872]) ).
cnf(p10313,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10146]) ).
cnf(p10316,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| greater(sk1(sk3),equilibrium(sk3))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10313]) ).
cnf(p10318,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10316]) ).
cnf(p10325,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p10318,p9845]) ).
cnf(p10326,plain,
( growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p10325,p10050]) ).
cnf(p11008,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p10326]) ).
cnf(p11068,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p11008]) ).
cnf(p11071,plain,
( greater(sk1(sk3),equilibrium(sk3))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p11068]) ).
cnf(p11077,plain,
( growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p11071]) ).
cnf(p11079,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(superposition,[status(thm)],[p11077,p9870]) ).
cnf(p11125,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(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)],[p11079]) ).
cnf(p11128,plain,
( greater(sk1(sk3),equilibrium(sk3))
| greater(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)],[p11125]) ).
cnf(p11130,plain,
( greater(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)],[p11128]) ).
cnf(p11132,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p11130,p9845]) ).
cnf(p11148,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(resolution,[status(thm)],[p11145,p11132]) ).
cnf(p11149,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p11148]) ).
cnf(p11152,plain,
( greater(sk1(sk3),equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p11149]) ).
cnf(p11154,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| sk4(equilibrium(sk3)) = equilibrium(sk3) ),
inference(factoring,[status(thm)],[p11152]) ).
cnf(p9869,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)],[p9841,p78]) ).
cnf(p11157,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)],[p11154,p9869]) ).
cnf(p9852,plain,
( greater_or_equal(equilibrium(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(demodulation,[status(thm)],[p9841,p46]) ).
cnf(p11205,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)],[p11157,p9852]) ).
cnf(p11308,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)],[p11205]) ).
cnf(p11310,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)],[p11308]) ).
cnf(p11314,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p11310,p10029]) ).
cnf(p11328,plain,
( 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
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p11314,p10013]) ).
cnf(p11356,plain,
( 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(factoring,[status(thm)],[p11328]) ).
cnf(p11317,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)],[p11154,p11310]) ).
cnf(p11342,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)],[p11317]) ).
cnf(p11344,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)],[p11342]) ).
cnf(p11345,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),X0)
| ~ greater(growth_rate(first_movers,sk4(equilibrium(sk3))),X0)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p11344,c0]) ).
cnf(p11361,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p11356,p11345]) ).
cnf(p11533,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p11361]) ).
cnf(p11535,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p11533]) ).
cnf(p11540,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(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p11535,p11344]) ).
cnf(p11546,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p11540]) ).
cnf(p11547,plain,
( greater(sk1(sk3),equilibrium(sk3))
| greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p11546]) ).
cnf(p11549,plain,
( greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p11547]) ).
cnf(p11156,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| ~ greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p11154,p9845]) ).
cnf(p11552,plain,
( ~ greater(zero,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(resolution,[status(thm)],[p11549,p11156]) ).
cnf(p11555,plain,
( ~ greater(zero,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)],[p11552]) ).
cnf(p11557,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p11555]) ).
cnf(p11561,plain,
( ~ greater(zero,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)],[p11154,p11557]) ).
cnf(p11565,plain,
( ~ greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p11561]) ).
cnf(p11567,plain,
( ~ greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p11565]) ).
cnf(p11316,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)],[p11310,p10048]) ).
cnf(p11337,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)],[p11154,p11316]) ).
cnf(p11473,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)],[p11337]) ).
cnf(p11475,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)],[p11473]) ).
cnf(p11318,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)],[p11154,p11310]) ).
cnf(p11351,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)],[p11318]) ).
cnf(p11353,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)],[p11351]) ).
cnf(p11480,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)],[p11475,p11353]) ).
cnf(p11484,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)],[p11480]) ).
cnf(p11485,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)],[p11484]) ).
cnf(p11487,plain,
( greater(zero,growth_rate(first_movers,equilibrium(sk3)))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p11485]) ).
cnf(p11568,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p11567,p11487]) ).
cnf(p11572,plain,
( greater(sk1(sk3),equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p11568]) ).
cnf(p11574,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p11572]) ).
cnf(p11577,plain,
( greater(sk4(sk1(sk3)),equilibrium(sk3))
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p11574,p30]) ).
cnf(p11579,plain,
( greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p11577,c3]) ).
cnf(p11583,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)],[p11579,p64]) ).
cnf(p11597,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)],[p11583,c0]) ).
cnf(p11641,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)],[p11597,p79]) ).
cnf(p11642,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)],[p11641]) ).
cnf(p11580,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)],[p11579,p32]) ).
cnf(p11590,plain,
( ~ 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)],[p11580,p27]) ).
cnf(p11651,plain,
( 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)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p11642,p11590]) ).
cnf(p12034,plain,
( greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p11651]) ).
cnf(p12089,plain,
( greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| equilibrium(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12034]) ).
cnf(p12090,plain,
( 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)],[p12089]) ).
cnf(p12093,plain,
( greater(growth_rate(efficient_producers,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)],[p12090,p80]) ).
cnf(p12100,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(resolution,[status(thm)],[p12093,p27]) ).
cnf(p12101,plain,
( growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12100,p11642]) ).
cnf(p12124,plain,
( sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12101]) ).
cnf(p12128,plain,
( equilibrium(sk3) = sk1(sk3)
| growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12124]) ).
cnf(p12129,plain,
( growth_rate(first_movers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12128]) ).
cnf(p12131,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p12129,p79]) ).
cnf(p12141,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12131,p27]) ).
cnf(p11587,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)],[p11579,p73]) ).
cnf(p11614,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)],[p11587,c0]) ).
cnf(p11663,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)],[p11614,p79]) ).
cnf(p11664,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)],[p11663]) ).
cnf(p12143,plain,
( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3)
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12141,p11664]) ).
cnf(p12153,plain,
( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| equilibrium(sk3) = sk1(sk3)
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12143]) ).
cnf(p12157,plain,
( growth_rate(efficient_producers,sk4(sk1(sk3))) = zero
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12153]) ).
cnf(p12158,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p12157,p79]) ).
cnf(p12168,plain,
( sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3)
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12158,p12141]) ).
cnf(p12173,plain,
( equilibrium(sk3) = sk1(sk3)
| sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12168]) ).
cnf(p12174,plain,
( sk4(sk1(sk3)) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12173]) ).
cnf(p12175,plain,
( subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p12174,p26]) ).
cnf(p12191,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| ~ greater_or_equal(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12175,p31]) ).
cnf(p11576,plain,
( greater_or_equal(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p11574,c3]) ).
cnf(p12211,plain,
( equilibrium(sk3) = sk1(sk3)
| greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12191,p11576]) ).
cnf(p12228,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12211]) ).
cnf(p12176,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ greater(growth_rate(efficient_producers,sk1(sk3)),zero)
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p12174,p27]) ).
cnf(p12231,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| equilibrium(sk3) = sk1(sk3)
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12228,p12176]) ).
cnf(p12338,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12231]) ).
cnf(p12339,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p12174,p12338]) ).
cnf(p12343,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12339]) ).
cnf(p12194,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| growth_rate(first_movers,sk1(sk3)) = zero
| ~ greater_or_equal(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12175,p48]) ).
cnf(p12217,plain,
( equilibrium(sk3) = sk1(sk3)
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12194,p11576]) ).
cnf(p12252,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| greater(zero,growth_rate(efficient_producers,sk1(sk3)))
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12217]) ).
cnf(p12253,plain,
( greater(zero,X0)
| ~ greater(growth_rate(efficient_producers,sk1(sk3)),X0)
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12252,c0]) ).
cnf(p12262,plain,
( ~ greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3)))
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12253]) ).
cnf(p12199,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)],[p12175,p76]) ).
cnf(f4,axiom,
( greater_or_equal(A,B)
| A != B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal_23) ).
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(p22,plain,
greater_or_equal(X0,X0),
inference(equality_resolution,[status(thm)],[c4]) ).
cnf(p12206,plain,
( greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3)))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12199,p22]) ).
cnf(p12268,plain,
( equilibrium(sk3) = sk1(sk3)
| greater(zero,growth_rate(first_movers,sk1(sk3)))
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12262,p12206]) ).
cnf(p12269,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12268]) ).
cnf(p12344,plain,
( growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3)
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12343,p12269]) ).
cnf(p12347,plain,
( equilibrium(sk3) = sk1(sk3)
| greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12344]) ).
cnf(p12348,plain,
( greater(growth_rate(first_movers,sk1(sk3)),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12347]) ).
cnf(p12183,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),X0)
| ~ greater(growth_rate(first_movers,sk1(sk3)),X0)
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p12174,p80]) ).
cnf(p12354,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| equilibrium(sk3) = sk1(sk3)
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12348,p12183]) ).
cnf(p12371,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12354]) ).
cnf(p12377,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12371,p27]) ).
cnf(p12378,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p12174,p12377]) ).
cnf(p12384,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12378]) ).
cnf(p12385,plain,
( growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3)
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12384,p12269]) ).
cnf(p12388,plain,
( equilibrium(sk3) = sk1(sk3)
| growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12385]) ).
cnf(p12389,plain,
( growth_rate(first_movers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12388]) ).
cnf(p12179,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk1(sk3)))
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p12174,p79]) ).
cnf(p12395,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| equilibrium(sk3) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p12389,p12179]) ).
cnf(p12411,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12395]) ).
cnf(p12414,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12411,p27]) ).
cnf(p12418,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| equilibrium(sk3) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p12174,p12414]) ).
cnf(p12421,plain,
( ~ greater(zero,growth_rate(first_movers,sk1(sk3)))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12418]) ).
cnf(p12198,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)],[p12175,p72]) ).
cnf(p12226,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)],[p12198,p11576]) ).
cnf(p12309,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)],[p12226]) ).
cnf(p12310,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)],[p12309,c0]) ).
cnf(p12322,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)],[p12310]) ).
cnf(p12325,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)],[p12322,p12206]) ).
cnf(p12326,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| growth_rate(efficient_producers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12325]) ).
cnf(p12426,plain,
( growth_rate(efficient_producers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12421,p12326]) ).
cnf(p12429,plain,
( growth_rate(efficient_producers,sk1(sk3)) = zero
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12426]) ).
cnf(p12436,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| equilibrium(sk3) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(superposition,[status(thm)],[p12429,p12206]) ).
cnf(p12556,plain,
( greater(zero,growth_rate(first_movers,sk1(sk3)))
| equilibrium(sk3) = sk1(sk3) ),
inference(factoring,[status(thm)],[p12436]) ).
cnf(p12565,plain,
( equilibrium(sk3) = sk1(sk3)
| equilibrium(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[p12556,p12421]) ).
cnf(p12566,plain,
equilibrium(sk3) = sk1(sk3),
inference(factoring,[status(thm)],[p12565]) ).
cnf(p12568,plain,
greater_or_equal(sk4(equilibrium(sk3)),sk1(sk3)),
inference(superposition,[status(thm)],[p12566,p25]) ).
cnf(p12626,plain,
greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),growth_rate(first_movers,sk4(equilibrium(sk3)))),
inference(resolution,[status(thm)],[p12568,p9869]) ).
cnf(p12656,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p12626,p10029]) ).
cnf(p12703,plain,
( 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)],[p12656,p10013]) ).
cnf(p12787,plain,
( greater(growth_rate(first_movers,sk4(equilibrium(sk3))),zero)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(factoring,[status(thm)],[p12703]) ).
cnf(p12654,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),X0)
| ~ greater(growth_rate(first_movers,sk4(equilibrium(sk3))),X0) ),
inference(resolution,[status(thm)],[p12626,c0]) ).
cnf(p12792,plain,
( greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero)
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p12787,p12654]) ).
cnf(p12805,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p12792,p9845]) ).
cnf(p12814,plain,
( growth_rate(first_movers,sk4(equilibrium(sk3))) = zero
| growth_rate(first_movers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p12805,p12656]) ).
cnf(p12816,plain,
growth_rate(first_movers,sk4(equilibrium(sk3))) = zero,
inference(factoring,[status(thm)],[p12814]) ).
cnf(p12658,plain,
( greater(zero,growth_rate(first_movers,sk4(equilibrium(sk3))))
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(resolution,[status(thm)],[p12626,p10048]) ).
cnf(p12833,plain,
( greater(zero,zero)
| growth_rate(efficient_producers,sk4(equilibrium(sk3))) = zero ),
inference(demodulation,[status(thm)],[p12816,p12658]) ).
cnf(p12830,plain,
greater(growth_rate(efficient_producers,sk4(equilibrium(sk3))),zero),
inference(demodulation,[status(thm)],[p12816,p12626]) ).
cnf(p12856,plain,
( greater(zero,zero)
| greater(zero,zero) ),
inference(superposition,[status(thm)],[p12833,p12830]) ).
cnf(p12858,plain,
greater(zero,zero),
inference(factoring,[status(thm)],[p12856]) ).
cnf(p12576,plain,
greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(equilibrium(sk3)))),
inference(superposition,[status(thm)],[p12566,p79]) ).
cnf(p12823,plain,
greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero),
inference(demodulation,[status(thm)],[p12816,p12576]) ).
cnf(p12839,plain,
~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3)))),
inference(resolution,[status(thm)],[p12823,p27]) ).
cnf(p12845,plain,
~ greater(zero,zero),
inference(superposition,[status(thm)],[p12566,p12839]) ).
cnf(p12859,plain,
$false,
inference(resolution,[status(thm)],[p12858,p12845]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT029-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.35 % Computer : n017.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Thu Sep 24 01:00:30 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 59.76/13.09 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 59.76/13.09 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------