%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : MGT029-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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 : Sun Sep 27 08:01:05 AM UTC 2026
% Result : Unsatisfiable 194.05s 50.06s
% Output : CNFRefutation 194.05s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
cnf(mp_greater_transitivity_19,axiom,
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ) ).
cnf(mp_times_in_environment_20,axiom,
( greater(X1,X2)
| X2 = X1
| greater(X2,X1)
| ~ 'in$uenvironment'(X0,X2)
| ~ 'in$uenvironment'(X0,X1) ) ).
cnf(mp_greater_or_equal_21,axiom,
( X0 = X1
| greater(X0,X1)
| ~ 'greater$uor$uequal'(X0,X1) ) ).
cnf(mp_greater_or_equal_22,axiom,
( 'greater$uor$uequal'(X0,X1)
| ~ greater(X0,X1) ) ).
cnf(mp_greater_or_equal_23,axiom,
( 'greater$uor$uequal'(X0,X1)
| X0 != X1 ) ).
cnf(l6_24,hypothesis,
( greater('growth$urate'('efficient$uproducers',X1),zero)
| greater('growth$urate'('first$umovers',X1),zero)
| 'growth$urate'('first$umovers',X1) = zero
| ~ 'greater$uor$uequal'(X1,equilibrium(X0))
| ~ subpopulations('first$umovers','efficient$uproducers',X0,X1)
| ~ environment(X0) ) ).
cnf(l6_26,hypothesis,
( greater('growth$urate'('efficient$uproducers',X1),zero)
| greater(zero,'growth$urate'('efficient$uproducers',X1))
| 'growth$urate'('first$umovers',X1) = zero
| ~ 'greater$uor$uequal'(X1,equilibrium(X0))
| ~ subpopulations('first$umovers','efficient$uproducers',X0,X1)
| ~ environment(X0) ) ).
cnf(l6_31,hypothesis,
( greater(zero,'growth$urate'('first$umovers',X1))
| greater(zero,'growth$urate'('efficient$uproducers',X1))
| 'growth$urate'('efficient$uproducers',X1) = zero
| ~ 'greater$uor$uequal'(X1,equilibrium(X0))
| ~ subpopulations('first$umovers','efficient$uproducers',X0,X1)
| ~ environment(X0) ) ).
cnf(l1_32,hypothesis,
( 'in$uenvironment'(X0,sk1(X0))
| ~ stable(X0)
| ~ environment(X0) ) ).
cnf(l1_33,hypothesis,
( greater('growth$urate'('efficient$uproducers',X1),'growth$urate'('first$umovers',X1))
| ~ 'greater$uor$uequal'(X1,sk1(X0))
| ~ subpopulations('first$umovers','efficient$uproducers',X0,X1)
| ~ stable(X0)
| ~ environment(X0) ) ).
cnf(a4_34,hypothesis,
( 'in$uenvironment'(X0,sk2(X0))
| ~ stable(X0)
| ~ environment(X0) ) ).
cnf(a4_35,hypothesis,
( 'greater$uor$uequal'(sk2(X0),equilibrium(X0))
| ~ stable(X0)
| ~ environment(X0) ) ).
cnf(prove_l11_36,negated_conjecture,
environment(sk3) ).
cnf(prove_l11_37,negated_conjecture,
stable(sk3) ).
cnf(prove_l11_38,negated_conjecture,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk4(X0))
| ~ 'in$uenvironment'(sk3,X0) ) ).
cnf(prove_l11_39,negated_conjecture,
( 'greater$uor$uequal'(sk4(X0),X0)
| ~ 'in$uenvironment'(sk3,X0) ) ).
cnf(prove_l11_40,negated_conjecture,
( ~ greater(zero,'growth$urate'('first$umovers',sk4(X0)))
| ~ greater('growth$urate'('efficient$uproducers',sk4(X0)),zero)
| ~ 'in$uenvironment'(sk3,X0) ) ).
cnf(c0,plain,
( greater(X2,X1)
| ~ greater(X2,X0)
| ~ greater(X0,X1) ),
inference(clausification,[status(esa)],[mp_greater_transitivity_19]) ).
cnf(c1,plain,
( ~ 'in$uenvironment'(X2,X1)
| greater(X1,X0)
| X1 = X0
| ~ 'in$uenvironment'(X2,X0)
| greater(X0,X1) ),
inference(clausification,[status(esa)],[mp_times_in_environment_20]) ).
cnf(c2,plain,
( X1 = X0
| ~ 'greater$uor$uequal'(X0,X1)
| greater(X0,X1) ),
inference(clausification,[status(esa)],[mp_greater_or_equal_21]) ).
cnf(c3,plain,
( 'greater$uor$uequal'(X0,X1)
| ~ greater(X0,X1) ),
inference(clausification,[status(esa)],[mp_greater_or_equal_22]) ).
cnf(c4,plain,
( 'greater$uor$uequal'(X1,X0)
| X0 != X1 ),
inference(clausification,[status(esa)],[mp_greater_or_equal_23]) ).
cnf(c5,plain,
( ~ 'greater$uor$uequal'(X0,equilibrium(X1))
| ~ environment(X1)
| greater('growth$urate'('first$umovers',X0),zero)
| ~ subpopulations('first$umovers','efficient$uproducers',X1,X0)
| 'growth$urate'('first$umovers',X0) = zero
| greater('growth$urate'('efficient$uproducers',X0),zero) ),
inference(clausification,[status(esa)],[l6_24]) ).
cnf(c7,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',X0,X1)
| greater('growth$urate'('efficient$uproducers',X1),zero)
| greater(zero,'growth$urate'('efficient$uproducers',X1))
| ~ 'greater$uor$uequal'(X1,equilibrium(X0))
| 'growth$urate'('first$umovers',X1) = zero
| ~ environment(X0) ),
inference(clausification,[status(esa)],[l6_26]) ).
cnf(c12,plain,
( greater(zero,'growth$urate'('efficient$uproducers',X1))
| greater(zero,'growth$urate'('first$umovers',X1))
| ~ subpopulations('first$umovers','efficient$uproducers',X0,X1)
| ~ 'greater$uor$uequal'(X1,equilibrium(X0))
| 'growth$urate'('efficient$uproducers',X1) = zero
| ~ environment(X0) ),
inference(clausification,[status(esa)],[l6_31]) ).
cnf(c13,plain,
( 'in$uenvironment'(X0,sk1(X0))
| ~ environment(X0)
| ~ stable(X0) ),
inference(clausification,[status(esa)],[l1_32]) ).
cnf(c14,plain,
( greater('growth$urate'('efficient$uproducers',X1),'growth$urate'('first$umovers',X1))
| ~ stable(X0)
| ~ environment(X0)
| ~ 'greater$uor$uequal'(X1,sk1(X0))
| ~ subpopulations('first$umovers','efficient$uproducers',X0,X1) ),
inference(clausification,[status(esa)],[l1_33]) ).
cnf(c15,plain,
( 'in$uenvironment'(X0,sk2(X0))
| ~ environment(X0)
| ~ stable(X0) ),
inference(clausification,[status(esa)],[a4_34]) ).
cnf(c16,plain,
( 'greater$uor$uequal'(sk2(X0),equilibrium(X0))
| ~ environment(X0)
| ~ stable(X0) ),
inference(clausification,[status(esa)],[a4_35]) ).
cnf(c17,plain,
environment(sk3),
inference(clausification,[status(esa)],[prove_l11_36]) ).
cnf(c18,plain,
stable(sk3),
inference(clausification,[status(esa)],[prove_l11_37]) ).
cnf(c19,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk4(X0))
| ~ 'in$uenvironment'(sk3,X0) ),
inference(clausification,[status(esa)],[prove_l11_38]) ).
cnf(c20,plain,
( 'greater$uor$uequal'(sk4(X0),X0)
| ~ 'in$uenvironment'(sk3,X0) ),
inference(clausification,[status(esa)],[prove_l11_39]) ).
cnf(c21,plain,
( ~ greater(zero,'growth$urate'('first$umovers',sk4(X0)))
| ~ 'in$uenvironment'(sk3,X0)
| ~ greater('growth$urate'('efficient$uproducers',sk4(X0)),zero) ),
inference(clausification,[status(esa)],[prove_l11_40]) ).
cnf(d0,plain,
( ~ stable(sk3)
| 'in$uenvironment'(sk3,sk1(sk3)) ),
inference(resolution,[status(thm)],[c13,c17]) ).
cnf(d1,plain,
'in$uenvironment'(sk3,sk1(sk3)),
inference(resolution,[status(thm)],[c18,d0]) ).
cnf(d2,plain,
'greater$uor$uequal'(sk4(sk1(sk3)),sk1(sk3)),
inference(resolution,[status(thm)],[d1,c20]) ).
cnf(d3,plain,
( ~ stable(sk3)
| ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),'growth$urate'('first$umovers',sk4(sk1(sk3)))) ),
inference(resolution,[status(thm)],[c14,d2]) ).
cnf(d4,plain,
( ~ stable(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),'growth$urate'('first$umovers',sk4(sk1(sk3)))) ),
inference(resolution,[status(thm)],[c17,d3]) ).
cnf(d5,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),'growth$urate'('first$umovers',sk4(sk1(sk3)))) ),
inference(resolution,[status(thm)],[c18,d4]) ).
cnf(d6,plain,
subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3))),
inference(resolution,[status(thm)],[c19,d1]) ).
cnf(d7,plain,
greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),'growth$urate'('first$umovers',sk4(sk1(sk3)))),
inference(resolution,[status(thm)],[d6,d5]) ).
cnf(d8,plain,
( ~ stable(sk3)
| 'in$uenvironment'(sk3,sk2(sk3)) ),
inference(resolution,[status(thm)],[c15,c17]) ).
cnf(d9,plain,
'in$uenvironment'(sk3,sk2(sk3)),
inference(resolution,[status(thm)],[c18,d8]) ).
cnf(d10,plain,
'greater$uor$uequal'(sk4(sk2(sk3)),sk2(sk3)),
inference(resolution,[status(thm)],[d9,c20]) ).
cnf(d11,plain,
( ~ stable(sk3)
| 'greater$uor$uequal'(sk2(sk3),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[c16,c17]) ).
cnf(d12,plain,
'greater$uor$uequal'(sk2(sk3),equilibrium(sk3)),
inference(resolution,[status(thm)],[c18,d11]) ).
cnf(d13,plain,
( ~ 'in$uenvironment'(sk3,X0)
| greater(X0,sk1(sk3))
| greater(sk1(sk3),X0)
| X0 = sk1(sk3) ),
inference(resolution,[status(thm)],[d1,c1]) ).
cnf(d14,plain,
( greater(sk1(sk3),sk2(sk3))
| greater(sk2(sk3),sk1(sk3))
| sk2(sk3) = sk1(sk3) ),
inference(resolution,[status(thm)],[d13,d9]) ).
cnf(d15,plain,
( greater(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),sk2(sk3))
| 'greater$uor$uequal'(sk1(sk3),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[d14,d12]) ).
cnf(d16,plain,
( greater(sk2(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk2(sk3) ),
inference(resolution,[status(thm)],[d12,c2]) ).
cnf(d17,plain,
( greater(sk2(sk3),equilibrium(sk3))
| 'greater$uor$uequal'(sk1(sk3),equilibrium(sk3))
| greater(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[d16,d15]) ).
cnf(d18,plain,
( 'greater$uor$uequal'(sk1(sk3),equilibrium(sk3))
| 'greater$uor$uequal'(sk1(sk3),equilibrium(sk3))
| greater(sk2(sk3),sk1(sk3))
| greater(sk2(sk3),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d17,c3]) ).
cnf(d19,plain,
( ~ greater(X0,sk2(sk3))
| greater(X0,equilibrium(sk3))
| 'greater$uor$uequal'(sk1(sk3),equilibrium(sk3))
| greater(sk2(sk3),sk1(sk3)) ),
inference(resolution,[status(thm)],[d18,c0]) ).
cnf(d20,plain,
( 'greater$uor$uequal'(sk1(sk3),equilibrium(sk3))
| greater(sk2(sk3),sk1(sk3))
| 'greater$uor$uequal'(sk1(sk3),equilibrium(sk3))
| greater(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d19,d15]) ).
cnf(d21,plain,
( 'greater$uor$uequal'(sk1(sk3),equilibrium(sk3))
| 'greater$uor$uequal'(sk1(sk3),equilibrium(sk3))
| greater(sk2(sk3),sk1(sk3)) ),
inference(resolution,[status(thm)],[d20,c3]) ).
cnf(d22,plain,
( 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| 'greater$uor$uequal'(sk1(sk3),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d21,c3]) ).
cnf(d23,plain,
( greater(sk1(sk3),equilibrium(sk3))
| equilibrium(sk3) = sk1(sk3)
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3)) ),
inference(resolution,[status(thm)],[d22,c2]) ).
cnf(d24,plain,
( 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[d23,d2]) ).
cnf(d25,plain,
( ~ greater(X0,sk1(sk3))
| greater(X0,equilibrium(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3)) ),
inference(resolution,[status(thm)],[d24,c0]) ).
cnf(d26,plain,
( greater(sk4(sk1(sk3)),sk1(sk3))
| sk1(sk3) = sk4(sk1(sk3)) ),
inference(resolution,[status(thm)],[d2,c2]) ).
cnf(d27,plain,
( greater(sk4(sk1(sk3)),sk1(sk3))
| ~ 'in$uenvironment'(sk3,sk1(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| ~ greater('growth$urate'('efficient$uproducers',sk1(sk3)),zero) ),
inference(superposition,[status(thm)],[d26,c21]) ).
cnf(d28,plain,
( greater(sk4(sk1(sk3)),sk1(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| ~ greater('growth$urate'('efficient$uproducers',sk1(sk3)),zero) ),
inference(resolution,[status(thm)],[d1,d27]) ).
cnf(d29,plain,
'greater$uor$uequal'(X0,X0),
inference(equality_resolution,[status(thm)],[c4]) ).
cnf(d30,plain,
( ~ stable(X0)
| ~ environment(X0)
| ~ subpopulations('first$umovers','efficient$uproducers',X0,sk1(X0))
| greater('growth$urate'('efficient$uproducers',sk1(X0)),'growth$urate'('first$umovers',sk1(X0))) ),
inference(resolution,[status(thm)],[c14,d29]) ).
cnf(d31,plain,
subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3))),
inference(resolution,[status(thm)],[c19,d9]) ).
cnf(d32,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| sk2(sk3) = sk4(sk2(sk3)) ),
inference(resolution,[status(thm)],[d10,c2]) ).
cnf(d33,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3)) ),
inference(superposition,[status(thm)],[d32,d31]) ).
cnf(d34,plain,
( greater(sk2(sk3),equilibrium(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[d16,d10]) ).
cnf(d35,plain,
( ~ greater(X0,sk2(sk3))
| greater(X0,equilibrium(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d34,c0]) ).
cnf(d36,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),equilibrium(sk3))
| greater(sk4(sk2(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d35,d33]) ).
cnf(d37,plain,
( 'greater$uor$uequal'(sk4(sk2(sk3)),equilibrium(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d36,c3]) ).
cnf(d38,plain,
( 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| ~ stable(sk3)
| ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,X0)
| greater('growth$urate'('efficient$uproducers',X0),'growth$urate'('first$umovers',X0))
| ~ 'greater$uor$uequal'(X0,equilibrium(sk3)) ),
inference(superposition,[status(thm)],[d23,c14]) ).
cnf(d39,plain,
( ~ stable(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,X0)
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| ~ 'greater$uor$uequal'(X0,equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',X0),'growth$urate'('first$umovers',X0)) ),
inference(resolution,[status(thm)],[c17,d38]) ).
cnf(d40,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,X0)
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| ~ 'greater$uor$uequal'(X0,equilibrium(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',X0),'growth$urate'('first$umovers',X0)) ),
inference(resolution,[status(thm)],[c18,d39]) ).
cnf(d41,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[d40,d37]) ).
cnf(d42,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[d31,d41]) ).
cnf(d43,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk2(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk2(sk3))) = zero
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3)) ),
inference(resolution,[status(thm)],[d37,c5]) ).
cnf(d44,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk2(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[c17,d43]) ).
cnf(d45,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk2(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[d31,d44]) ).
cnf(d46,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk2(sk3))),zero)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero) ),
inference(superposition,[status(thm)],[d45,d42]) ).
cnf(d47,plain,
( ~ greater(X0,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| greater(X0,zero)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero) ),
inference(resolution,[status(thm)],[d46,c0]) ).
cnf(d48,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero) ),
inference(resolution,[status(thm)],[d47,d42]) ).
cnf(d49,plain,
( ~ 'in$uenvironment'(sk3,sk2(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d48,c21]) ).
cnf(d50,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[d9,d49]) ).
cnf(d51,plain,
( ~ greater(X0,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(X0,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d42,c0]) ).
cnf(d52,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk2(sk3))) = zero
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3)) ),
inference(resolution,[status(thm)],[d37,c12]) ).
cnf(d53,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[c17,d52]) ).
cnf(d54,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[d31,d53]) ).
cnf(d55,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(superposition,[status(thm)],[d54,d42]) ).
cnf(d56,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d50,d55]) ).
cnf(d57,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d56,d51]) ).
cnf(d58,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk1(sk3),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d57,d50]) ).
cnf(d59,plain,
( ~ greater(X0,sk1(sk3))
| greater(X0,equilibrium(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3)) ),
inference(resolution,[status(thm)],[d58,c0]) ).
cnf(d60,plain,
( greater(sk4(sk1(sk3)),sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3)) ),
inference(superposition,[status(thm)],[d26,d6]) ).
cnf(d61,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d25,d60]) ).
cnf(d62,plain,
( 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3)) ),
inference(resolution,[status(thm)],[d61,c3]) ).
cnf(d63,plain,
( greater(sk2(sk3),sk1(sk3))
| sk1(sk3) = sk2(sk3)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d62,c2]) ).
cnf(d64,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(sk2(sk3),sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[d63,d37]) ).
cnf(d65,plain,
( ~ greater(X0,sk2(sk3))
| greater(X0,sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d64,c0]) ).
cnf(d66,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d65,d33]) ).
cnf(d67,plain,
( 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d66,c3]) ).
cnf(d68,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk1(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk1(sk3))) = zero
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d67,c5]) ).
cnf(d69,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk1(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk1(sk3))) = zero ),
inference(resolution,[status(thm)],[c17,d68]) ).
cnf(d70,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk1(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk1(sk3))) = zero ),
inference(resolution,[status(thm)],[d6,d69]) ).
cnf(d71,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero) ),
inference(superposition,[status(thm)],[d70,d7]) ).
cnf(d72,plain,
( ~ greater(X0,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| greater(X0,zero)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero) ),
inference(resolution,[status(thm)],[d71,c0]) ).
cnf(d73,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero) ),
inference(resolution,[status(thm)],[d72,d7]) ).
cnf(d74,plain,
( ~ 'in$uenvironment'(sk3,sk1(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d73,c21]) ).
cnf(d75,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3)))) ),
inference(resolution,[status(thm)],[d1,d74]) ).
cnf(d76,plain,
( ~ greater(X0,'growth$urate'('efficient$uproducers',sk4(sk1(sk3))))
| greater(X0,'growth$urate'('first$umovers',sk4(sk1(sk3)))) ),
inference(resolution,[status(thm)],[d7,c0]) ).
cnf(d77,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk1(sk3))) = zero
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d67,c12]) ).
cnf(d78,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk1(sk3))) = zero ),
inference(resolution,[status(thm)],[c17,d77]) ).
cnf(d79,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk1(sk3))) = zero ),
inference(resolution,[status(thm)],[d6,d78]) ).
cnf(d80,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3)))) ),
inference(superposition,[status(thm)],[d79,d7]) ).
cnf(d81,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d75,d80]) ).
cnf(d82,plain,
( greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d81,d76]) ).
cnf(d83,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d82,d75]) ).
cnf(d84,plain,
( ~ stable(sk3)
| ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3)) ),
inference(resolution,[status(thm)],[d83,c14]) ).
cnf(d85,plain,
( ~ stable(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[c17,d84]) ).
cnf(d86,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[c18,d85]) ).
cnf(d87,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[d31,d86]) ).
cnf(d88,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk2(sk3))),zero)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero) ),
inference(superposition,[status(thm)],[d45,d87]) ).
cnf(d89,plain,
( ~ greater(X0,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| greater(X0,zero)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero) ),
inference(resolution,[status(thm)],[d88,c0]) ).
cnf(d90,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero) ),
inference(resolution,[status(thm)],[d89,d87]) ).
cnf(d91,plain,
( ~ 'in$uenvironment'(sk3,sk2(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3)) ),
inference(resolution,[status(thm)],[d90,c21]) ).
cnf(d92,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[d9,d91]) ).
cnf(d93,plain,
( ~ greater(X0,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(X0,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3)) ),
inference(resolution,[status(thm)],[d87,c0]) ).
cnf(d94,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(superposition,[status(thm)],[d54,d87]) ).
cnf(d95,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3)) ),
inference(resolution,[status(thm)],[d92,d94]) ).
cnf(d96,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3)) ),
inference(resolution,[status(thm)],[d95,d93]) ).
cnf(d97,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3)) ),
inference(resolution,[status(thm)],[d96,d92]) ).
cnf(d98,plain,
( ~ stable(sk3)
| ~ environment(sk3)
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),'growth$urate'('first$umovers',sk1(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3)) ),
inference(resolution,[status(thm)],[d97,d30]) ).
cnf(d99,plain,
( ~ stable(sk3)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),'growth$urate'('first$umovers',sk1(sk3))) ),
inference(resolution,[status(thm)],[c17,d98]) ).
cnf(d100,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),'growth$urate'('first$umovers',sk1(sk3))) ),
inference(resolution,[status(thm)],[c18,d99]) ).
cnf(d101,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),zero)
| greater('growth$urate'('first$umovers',sk1(sk3)),zero)
| 'growth$urate'('first$umovers',sk1(sk3)) = zero
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3)) ),
inference(resolution,[status(thm)],[d22,c5]) ).
cnf(d102,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),zero)
| greater('growth$urate'('first$umovers',sk1(sk3)),zero)
| 'growth$urate'('first$umovers',sk1(sk3)) = zero ),
inference(resolution,[status(thm)],[c17,d101]) ).
cnf(d103,plain,
( 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),zero)
| greater('growth$urate'('first$umovers',sk1(sk3)),zero)
| 'growth$urate'('first$umovers',sk1(sk3)) = zero
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3)) ),
inference(resolution,[status(thm)],[d97,d102]) ).
cnf(d104,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),zero)
| greater('growth$urate'('first$umovers',sk1(sk3)),zero)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),zero) ),
inference(superposition,[status(thm)],[d103,d100]) ).
cnf(d105,plain,
( ~ greater(X0,'growth$urate'('first$umovers',sk1(sk3)))
| greater(X0,zero)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),zero) ),
inference(resolution,[status(thm)],[d104,c0]) ).
cnf(d106,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),zero)
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),zero) ),
inference(resolution,[status(thm)],[d105,d100]) ).
cnf(d107,plain,
( greater(sk4(sk1(sk3)),sk1(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3)) ),
inference(resolution,[status(thm)],[d106,d28]) ).
cnf(d108,plain,
( greater(sk4(sk1(sk3)),sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk4(sk1(sk3)),sk1(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk1(sk3))) ),
inference(superposition,[status(thm)],[d26,d107]) ).
cnf(d109,plain,
( greater(sk4(sk1(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),'growth$urate'('first$umovers',sk4(sk1(sk3)))) ),
inference(superposition,[status(thm)],[d26,d7]) ).
cnf(d110,plain,
( greater(sk4(sk1(sk3)),sk1(sk3))
| greater(sk4(sk1(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),'growth$urate'('first$umovers',sk1(sk3))) ),
inference(superposition,[status(thm)],[d26,d109]) ).
cnf(d111,plain,
( ~ greater(X0,'growth$urate'('efficient$uproducers',sk1(sk3)))
| greater(X0,'growth$urate'('first$umovers',sk1(sk3)))
| greater(sk4(sk1(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d110,c0]) ).
cnf(d112,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk1(sk3)))
| greater(zero,'growth$urate'('first$umovers',sk1(sk3)))
| 'growth$urate'('efficient$uproducers',sk1(sk3)) = zero
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3)) ),
inference(resolution,[status(thm)],[d22,c12]) ).
cnf(d113,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk1(sk3)))
| greater(zero,'growth$urate'('first$umovers',sk1(sk3)))
| 'growth$urate'('efficient$uproducers',sk1(sk3)) = zero ),
inference(resolution,[status(thm)],[c17,d112]) ).
cnf(d114,plain,
( 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk1(sk3)))
| greater(zero,'growth$urate'('first$umovers',sk1(sk3)))
| 'growth$urate'('efficient$uproducers',sk1(sk3)) = zero
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3)) ),
inference(resolution,[status(thm)],[d97,d113]) ).
cnf(d115,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk1(sk3)))
| greater(zero,'growth$urate'('first$umovers',sk1(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater(zero,'growth$urate'('first$umovers',sk1(sk3))) ),
inference(superposition,[status(thm)],[d114,d100]) ).
cnf(d116,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk4(sk1(sk3)),sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk1(sk3))) ),
inference(resolution,[status(thm)],[d115,d108]) ).
cnf(d117,plain,
( greater(sk4(sk1(sk3)),sk1(sk3))
| greater(zero,'growth$urate'('first$umovers',sk1(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk4(sk1(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d116,d111]) ).
cnf(d118,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk4(sk1(sk3)),sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk4(sk1(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d117,d108]) ).
cnf(d119,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk4(sk1(sk3)),equilibrium(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3)) ),
inference(resolution,[status(thm)],[d118,d59]) ).
cnf(d120,plain,
( 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3)) ),
inference(resolution,[status(thm)],[d119,c3]) ).
cnf(d121,plain,
( greater(sk2(sk3),sk1(sk3))
| sk1(sk3) = sk2(sk3)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d120,c2]) ).
cnf(d122,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(sk2(sk3),sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(superposition,[status(thm)],[d121,d37]) ).
cnf(d123,plain,
( ~ greater(X0,sk2(sk3))
| greater(X0,sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d122,c0]) ).
cnf(d124,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d123,d33]) ).
cnf(d125,plain,
( 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d124,c3]) ).
cnf(d126,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk1(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk1(sk3))) = zero
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d125,c5]) ).
cnf(d127,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk1(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk1(sk3))) = zero ),
inference(resolution,[status(thm)],[c17,d126]) ).
cnf(d128,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk1(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk1(sk3))) = zero ),
inference(resolution,[status(thm)],[d6,d127]) ).
cnf(d129,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero) ),
inference(superposition,[status(thm)],[d128,d7]) ).
cnf(d130,plain,
( ~ greater(X0,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| greater(X0,zero)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero) ),
inference(resolution,[status(thm)],[d129,c0]) ).
cnf(d131,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero) ),
inference(resolution,[status(thm)],[d130,d7]) ).
cnf(d132,plain,
( ~ 'in$uenvironment'(sk3,sk1(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d131,c21]) ).
cnf(d133,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3)))) ),
inference(resolution,[status(thm)],[d1,d132]) ).
cnf(d134,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk1(sk3))) = zero
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d125,c12]) ).
cnf(d135,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk1(sk3))) = zero ),
inference(resolution,[status(thm)],[c17,d134]) ).
cnf(d136,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk1(sk3))) = zero ),
inference(resolution,[status(thm)],[d6,d135]) ).
cnf(d137,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3)))) ),
inference(superposition,[status(thm)],[d136,d7]) ).
cnf(d138,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3)))) ),
inference(resolution,[status(thm)],[d137,d133]) ).
cnf(d139,plain,
( greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d138,d76]) ).
cnf(d140,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d139,d133]) ).
cnf(d141,plain,
( ~ stable(sk3)
| ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3)) ),
inference(resolution,[status(thm)],[d140,c14]) ).
cnf(d142,plain,
( ~ stable(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[c17,d141]) ).
cnf(d143,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[c18,d142]) ).
cnf(d144,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[d31,d143]) ).
cnf(d145,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk2(sk3))),zero)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero) ),
inference(superposition,[status(thm)],[d45,d144]) ).
cnf(d146,plain,
( ~ greater(X0,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| greater(X0,zero)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero) ),
inference(resolution,[status(thm)],[d145,c0]) ).
cnf(d147,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero) ),
inference(resolution,[status(thm)],[d146,d144]) ).
cnf(d148,plain,
( ~ 'in$uenvironment'(sk3,sk2(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3)) ),
inference(resolution,[status(thm)],[d147,c21]) ).
cnf(d149,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[d9,d148]) ).
cnf(d150,plain,
( ~ greater(X0,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(X0,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3)) ),
inference(resolution,[status(thm)],[d144,c0]) ).
cnf(d151,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(superposition,[status(thm)],[d54,d144]) ).
cnf(d152,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3)) ),
inference(resolution,[status(thm)],[d149,d151]) ).
cnf(d153,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3)) ),
inference(resolution,[status(thm)],[d152,d150]) ).
cnf(d154,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3)) ),
inference(resolution,[status(thm)],[d153,d149]) ).
cnf(d155,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(sk2(sk3),sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3)) ),
inference(superposition,[status(thm)],[d63,d154]) ).
cnf(d156,plain,
( ~ greater(X0,sk2(sk3))
| greater(X0,sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d155,c0]) ).
cnf(d157,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| ~ 'in$uenvironment'(sk3,sk2(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| ~ greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero) ),
inference(superposition,[status(thm)],[d32,c21]) ).
cnf(d158,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| ~ greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero) ),
inference(resolution,[status(thm)],[d9,d157]) ).
cnf(d159,plain,
( ~ stable(sk3)
| ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),'growth$urate'('first$umovers',sk2(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d62,c14]) ).
cnf(d160,plain,
( ~ stable(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),'growth$urate'('first$umovers',sk2(sk3))) ),
inference(resolution,[status(thm)],[c17,d159]) ).
cnf(d161,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),'growth$urate'('first$umovers',sk2(sk3))) ),
inference(resolution,[status(thm)],[c18,d160]) ).
cnf(d162,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),'growth$urate'('first$umovers',sk2(sk3))) ),
inference(resolution,[status(thm)],[d154,d161]) ).
cnf(d163,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero)
| greater('growth$urate'('first$umovers',sk2(sk3)),zero)
| 'growth$urate'('first$umovers',sk2(sk3)) = zero ),
inference(resolution,[status(thm)],[d12,c5]) ).
cnf(d164,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero)
| greater('growth$urate'('first$umovers',sk2(sk3)),zero)
| 'growth$urate'('first$umovers',sk2(sk3)) = zero ),
inference(resolution,[status(thm)],[c17,d163]) ).
cnf(d165,plain,
( greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero)
| greater('growth$urate'('first$umovers',sk2(sk3)),zero)
| 'growth$urate'('first$umovers',sk2(sk3)) = zero ),
inference(resolution,[status(thm)],[d154,d164]) ).
cnf(d166,plain,
( greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero)
| greater('growth$urate'('first$umovers',sk2(sk3)),zero)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero) ),
inference(superposition,[status(thm)],[d165,d162]) ).
cnf(d167,plain,
( ~ greater(X0,'growth$urate'('first$umovers',sk2(sk3)))
| greater(X0,zero)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero) ),
inference(resolution,[status(thm)],[d166,c0]) ).
cnf(d168,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero)
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero) ),
inference(resolution,[status(thm)],[d167,d162]) ).
cnf(d169,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d168,d158]) ).
cnf(d170,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk2(sk3))) ),
inference(superposition,[status(thm)],[d32,d169]) ).
cnf(d171,plain,
( ~ greater(X0,'growth$urate'('efficient$uproducers',sk2(sk3)))
| greater(X0,'growth$urate'('first$umovers',sk2(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d162,c0]) ).
cnf(d172,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3)))
| greater(zero,'growth$urate'('first$umovers',sk2(sk3)))
| 'growth$urate'('efficient$uproducers',sk2(sk3)) = zero ),
inference(resolution,[status(thm)],[d12,c12]) ).
cnf(d173,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3)))
| greater(zero,'growth$urate'('first$umovers',sk2(sk3)))
| 'growth$urate'('efficient$uproducers',sk2(sk3)) = zero ),
inference(resolution,[status(thm)],[c17,d172]) ).
cnf(d174,plain,
( greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3)))
| greater(zero,'growth$urate'('first$umovers',sk2(sk3)))
| 'growth$urate'('efficient$uproducers',sk2(sk3)) = zero ),
inference(resolution,[status(thm)],[d154,d173]) ).
cnf(d175,plain,
( greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3)))
| greater(zero,'growth$urate'('first$umovers',sk2(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(zero,'growth$urate'('first$umovers',sk2(sk3))) ),
inference(superposition,[status(thm)],[d174,d162]) ).
cnf(d176,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3)) ),
inference(resolution,[status(thm)],[d170,d175]) ).
cnf(d177,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(zero,'growth$urate'('first$umovers',sk2(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3)) ),
inference(resolution,[status(thm)],[d176,d171]) ).
cnf(d178,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3)) ),
inference(resolution,[status(thm)],[d177,d170]) ).
cnf(d179,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(sk4(sk2(sk3)),sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d178,d156]) ).
cnf(d180,plain,
( 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d179,c3]) ).
cnf(d181,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk1(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk1(sk3))) = zero
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d180,c5]) ).
cnf(d182,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk1(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk1(sk3))) = zero ),
inference(resolution,[status(thm)],[c17,d181]) ).
cnf(d183,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk1(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk1(sk3))) = zero ),
inference(resolution,[status(thm)],[d6,d182]) ).
cnf(d184,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero) ),
inference(superposition,[status(thm)],[d183,d7]) ).
cnf(d185,plain,
( ~ greater(X0,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| greater(X0,zero)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero) ),
inference(resolution,[status(thm)],[d184,c0]) ).
cnf(d186,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero) ),
inference(resolution,[status(thm)],[d185,d7]) ).
cnf(d187,plain,
( ~ 'in$uenvironment'(sk3,sk1(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d186,c21]) ).
cnf(d188,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3)))) ),
inference(resolution,[status(thm)],[d1,d187]) ).
cnf(d189,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk1(sk3))) = zero
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d180,c12]) ).
cnf(d190,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk1(sk3))) = zero ),
inference(resolution,[status(thm)],[c17,d189]) ).
cnf(d191,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk1(sk3))) = zero ),
inference(resolution,[status(thm)],[d6,d190]) ).
cnf(d192,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3)))) ),
inference(superposition,[status(thm)],[d191,d7]) ).
cnf(d193,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3)))) ),
inference(resolution,[status(thm)],[d192,d188]) ).
cnf(d194,plain,
( greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d193,d76]) ).
cnf(d195,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d194,d188]) ).
cnf(d196,plain,
( ~ stable(sk3)
| ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3)) ),
inference(resolution,[status(thm)],[d195,c14]) ).
cnf(d197,plain,
( ~ stable(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[c17,d196]) ).
cnf(d198,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[c18,d197]) ).
cnf(d199,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[d31,d198]) ).
cnf(d200,plain,
( ~ greater(X0,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(X0,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3)) ),
inference(resolution,[status(thm)],[d199,c0]) ).
cnf(d201,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(X0,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| ~ greater(X0,'growth$urate'('efficient$uproducers',sk2(sk3))) ),
inference(superposition,[status(thm)],[d32,d200]) ).
cnf(d202,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(superposition,[status(thm)],[d32,d199]) ).
cnf(d203,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),'growth$urate'('first$umovers',sk2(sk3))) ),
inference(superposition,[status(thm)],[d32,d202]) ).
cnf(d204,plain,
( greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3)))
| greater(zero,'growth$urate'('first$umovers',sk2(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater(zero,'growth$urate'('first$umovers',sk2(sk3))) ),
inference(superposition,[status(thm)],[d174,d203]) ).
cnf(d205,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3)))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero)
| 'growth$urate'('first$umovers',sk2(sk3)) = zero ),
inference(resolution,[status(thm)],[d12,c7]) ).
cnf(d206,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3)))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero)
| 'growth$urate'('first$umovers',sk2(sk3)) = zero ),
inference(resolution,[status(thm)],[c17,d205]) ).
cnf(d207,plain,
( greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3)))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero)
| 'growth$urate'('first$umovers',sk2(sk3)) = zero ),
inference(resolution,[status(thm)],[d154,d206]) ).
cnf(d208,plain,
( greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3)))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero) ),
inference(superposition,[status(thm)],[d207,d203]) ).
cnf(d209,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3))) ),
inference(resolution,[status(thm)],[d208,d158]) ).
cnf(d210,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3)))
| ~ greater(zero,'growth$urate'('first$umovers',sk2(sk3))) ),
inference(superposition,[status(thm)],[d32,d209]) ).
cnf(d211,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3))) ),
inference(resolution,[status(thm)],[d210,d204]) ).
cnf(d212,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3)) ),
inference(resolution,[status(thm)],[d211,d201]) ).
cnf(d213,plain,
( greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero)
| greater('growth$urate'('first$umovers',sk2(sk3)),zero)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero) ),
inference(superposition,[status(thm)],[d165,d203]) ).
cnf(d214,plain,
( ~ greater(X0,'growth$urate'('first$umovers',sk2(sk3)))
| greater(X0,zero)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero) ),
inference(resolution,[status(thm)],[d213,c0]) ).
cnf(d215,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero)
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero) ),
inference(resolution,[status(thm)],[d214,d203]) ).
cnf(d216,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3)) ),
inference(resolution,[status(thm)],[d215,d158]) ).
cnf(d217,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3)) ),
inference(resolution,[status(thm)],[d216,d212]) ).
cnf(d218,plain,
( 'greater$uor$uequal'(sk4(sk2(sk3)),equilibrium(sk3))
| greater(sk4(sk2(sk3)),equilibrium(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3)) ),
inference(resolution,[status(thm)],[d217,d35]) ).
cnf(d219,plain,
( 'greater$uor$uequal'(sk4(sk2(sk3)),equilibrium(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d218,c3]) ).
cnf(d220,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk2(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk2(sk3))) = zero
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3)) ),
inference(resolution,[status(thm)],[d219,c5]) ).
cnf(d221,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk2(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[c17,d220]) ).
cnf(d222,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk2(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[d31,d221]) ).
cnf(d223,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk2(sk3))),zero)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero) ),
inference(superposition,[status(thm)],[d222,d199]) ).
cnf(d224,plain,
( ~ greater(X0,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| greater(X0,zero)
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero) ),
inference(resolution,[status(thm)],[d223,c0]) ).
cnf(d225,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero) ),
inference(resolution,[status(thm)],[d224,d199]) ).
cnf(d226,plain,
( ~ 'in$uenvironment'(sk3,sk2(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3)) ),
inference(resolution,[status(thm)],[d225,c21]) ).
cnf(d227,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[d9,d226]) ).
cnf(d228,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk2(sk3))) = zero
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3)) ),
inference(resolution,[status(thm)],[d219,c12]) ).
cnf(d229,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[c17,d228]) ).
cnf(d230,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[d31,d229]) ).
cnf(d231,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(superposition,[status(thm)],[d230,d199]) ).
cnf(d232,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[d231,d227]) ).
cnf(d233,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3)) ),
inference(resolution,[status(thm)],[d232,d200]) ).
cnf(d234,plain,
( subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3))
| subpopulations('first$umovers','efficient$uproducers',sk3,sk1(sk3)) ),
inference(resolution,[status(thm)],[d233,d227]) ).
cnf(d235,plain,
( ~ stable(sk3)
| ~ environment(sk3)
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),'growth$urate'('first$umovers',sk1(sk3))) ),
inference(resolution,[status(thm)],[d234,d30]) ).
cnf(d236,plain,
( ~ stable(sk3)
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),'growth$urate'('first$umovers',sk1(sk3))) ),
inference(resolution,[status(thm)],[c17,d235]) ).
cnf(d237,plain,
greater('growth$urate'('efficient$uproducers',sk1(sk3)),'growth$urate'('first$umovers',sk1(sk3))),
inference(resolution,[status(thm)],[c18,d236]) ).
cnf(d238,plain,
( 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),zero)
| greater('growth$urate'('first$umovers',sk1(sk3)),zero)
| 'growth$urate'('first$umovers',sk1(sk3)) = zero ),
inference(resolution,[status(thm)],[d234,d102]) ).
cnf(d239,plain,
( 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),zero)
| greater('growth$urate'('first$umovers',sk1(sk3)),zero)
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),zero) ),
inference(superposition,[status(thm)],[d238,d237]) ).
cnf(d240,plain,
( ~ greater(X0,'growth$urate'('first$umovers',sk1(sk3)))
| greater(X0,zero)
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),zero) ),
inference(resolution,[status(thm)],[d239,c0]) ).
cnf(d241,plain,
( 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),zero)
| greater('growth$urate'('efficient$uproducers',sk1(sk3)),zero) ),
inference(resolution,[status(thm)],[d240,d237]) ).
cnf(d242,plain,
( greater(sk4(sk1(sk3)),sk1(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3)) ),
inference(resolution,[status(thm)],[d241,d28]) ).
cnf(d243,plain,
( greater(sk4(sk1(sk3)),sk1(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk4(sk1(sk3)),sk1(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk1(sk3))) ),
inference(superposition,[status(thm)],[d26,d242]) ).
cnf(d244,plain,
( ~ greater(X0,'growth$urate'('efficient$uproducers',sk1(sk3)))
| greater(X0,'growth$urate'('first$umovers',sk1(sk3))) ),
inference(resolution,[status(thm)],[d237,c0]) ).
cnf(d245,plain,
( 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk1(sk3)))
| greater(zero,'growth$urate'('first$umovers',sk1(sk3)))
| 'growth$urate'('efficient$uproducers',sk1(sk3)) = zero ),
inference(resolution,[status(thm)],[d234,d113]) ).
cnf(d246,plain,
( 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk1(sk3)))
| greater(zero,'growth$urate'('first$umovers',sk1(sk3)))
| greater(zero,'growth$urate'('first$umovers',sk1(sk3))) ),
inference(superposition,[status(thm)],[d245,d237]) ).
cnf(d247,plain,
( 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk4(sk1(sk3)),sk1(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk1(sk3))) ),
inference(resolution,[status(thm)],[d246,d243]) ).
cnf(d248,plain,
( greater(zero,'growth$urate'('first$umovers',sk1(sk3)))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk4(sk1(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d247,d244]) ).
cnf(d249,plain,
( 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk4(sk1(sk3)),sk1(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk4(sk1(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d248,d243]) ).
cnf(d250,plain,
( 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3))
| greater(sk4(sk1(sk3)),equilibrium(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3)) ),
inference(resolution,[status(thm)],[d249,d25]) ).
cnf(d251,plain,
( 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| 'greater$uor$uequal'(sk2(sk3),sk1(sk3)) ),
inference(resolution,[status(thm)],[d250,c3]) ).
cnf(d252,plain,
( greater(sk2(sk3),sk1(sk3))
| sk1(sk3) = sk2(sk3)
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d251,c2]) ).
cnf(d253,plain,
( 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(sk2(sk3),sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(superposition,[status(thm)],[d252,d10]) ).
cnf(d254,plain,
( ~ greater(X0,sk2(sk3))
| greater(X0,sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d253,c0]) ).
cnf(d255,plain,
( ~ stable(sk3)
| ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),'growth$urate'('first$umovers',sk2(sk3)))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d251,c14]) ).
cnf(d256,plain,
( ~ stable(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),'growth$urate'('first$umovers',sk2(sk3))) ),
inference(resolution,[status(thm)],[c17,d255]) ).
cnf(d257,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk2(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),'growth$urate'('first$umovers',sk2(sk3))) ),
inference(resolution,[status(thm)],[c18,d256]) ).
cnf(d258,plain,
( 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),'growth$urate'('first$umovers',sk2(sk3))) ),
inference(resolution,[status(thm)],[d154,d257]) ).
cnf(d259,plain,
( greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero)
| greater('growth$urate'('first$umovers',sk2(sk3)),zero)
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero) ),
inference(superposition,[status(thm)],[d165,d258]) ).
cnf(d260,plain,
( ~ greater(X0,'growth$urate'('first$umovers',sk2(sk3)))
| greater(X0,zero)
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero) ),
inference(resolution,[status(thm)],[d259,c0]) ).
cnf(d261,plain,
( 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero)
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero) ),
inference(resolution,[status(thm)],[d260,d258]) ).
cnf(d262,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d261,d158]) ).
cnf(d263,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk2(sk3))) ),
inference(superposition,[status(thm)],[d32,d262]) ).
cnf(d264,plain,
( ~ greater(X0,'growth$urate'('efficient$uproducers',sk2(sk3)))
| greater(X0,'growth$urate'('first$umovers',sk2(sk3)))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d258,c0]) ).
cnf(d265,plain,
( greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3)))
| greater(zero,'growth$urate'('first$umovers',sk2(sk3)))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(zero,'growth$urate'('first$umovers',sk2(sk3))) ),
inference(superposition,[status(thm)],[d174,d258]) ).
cnf(d266,plain,
( 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3)))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3)) ),
inference(resolution,[status(thm)],[d263,d265]) ).
cnf(d267,plain,
( 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(zero,'growth$urate'('first$umovers',sk2(sk3)))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3)) ),
inference(resolution,[status(thm)],[d266,d264]) ).
cnf(d268,plain,
( 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3)) ),
inference(resolution,[status(thm)],[d267,d263]) ).
cnf(d269,plain,
( 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3))
| greater(sk4(sk2(sk3)),sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d268,d254]) ).
cnf(d270,plain,
( 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| 'greater$uor$uequal'(sk4(sk1(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d269,c3]) ).
cnf(d271,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk1(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk1(sk3))) = zero
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d270,c5]) ).
cnf(d272,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk1(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk1(sk3))) = zero ),
inference(resolution,[status(thm)],[c17,d271]) ).
cnf(d273,plain,
( 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk1(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk1(sk3))) = zero ),
inference(resolution,[status(thm)],[d6,d272]) ).
cnf(d274,plain,
( 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero) ),
inference(superposition,[status(thm)],[d273,d7]) ).
cnf(d275,plain,
( ~ greater(X0,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| greater(X0,zero)
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero) ),
inference(resolution,[status(thm)],[d274,c0]) ).
cnf(d276,plain,
( 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero)
| greater('growth$urate'('efficient$uproducers',sk4(sk1(sk3))),zero) ),
inference(resolution,[status(thm)],[d275,d7]) ).
cnf(d277,plain,
( ~ 'in$uenvironment'(sk3,sk1(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d276,c21]) ).
cnf(d278,plain,
( 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3)))) ),
inference(resolution,[status(thm)],[d1,d277]) ).
cnf(d279,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk1(sk3))) = zero
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d270,c12]) ).
cnf(d280,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk1(sk3)))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk1(sk3))) = zero ),
inference(resolution,[status(thm)],[c17,d279]) ).
cnf(d281,plain,
( 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk1(sk3))) = zero ),
inference(resolution,[status(thm)],[d6,d280]) ).
cnf(d282,plain,
( 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3)))) ),
inference(superposition,[status(thm)],[d281,d7]) ).
cnf(d283,plain,
( 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk1(sk3)))) ),
inference(resolution,[status(thm)],[d282,d278]) ).
cnf(d284,plain,
( greater(zero,'growth$urate'('first$umovers',sk4(sk1(sk3))))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d283,d76]) ).
cnf(d285,plain,
( 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),sk1(sk3)) ),
inference(resolution,[status(thm)],[d284,d278]) ).
cnf(d286,plain,
( ~ stable(sk3)
| ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[d285,c14]) ).
cnf(d287,plain,
( ~ stable(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[c17,d286]) ).
cnf(d288,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[c18,d287]) ).
cnf(d289,plain,
greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),'growth$urate'('first$umovers',sk4(sk2(sk3)))),
inference(resolution,[status(thm)],[d31,d288]) ).
cnf(d290,plain,
( ~ greater(X0,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(X0,'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[d289,c0]) ).
cnf(d291,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| greater(X0,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| ~ greater(X0,'growth$urate'('efficient$uproducers',sk2(sk3))) ),
inference(superposition,[status(thm)],[d32,d290]) ).
cnf(d292,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(superposition,[status(thm)],[d32,d289]) ).
cnf(d293,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),'growth$urate'('first$umovers',sk2(sk3))) ),
inference(superposition,[status(thm)],[d32,d292]) ).
cnf(d294,plain,
( greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3)))
| greater(zero,'growth$urate'('first$umovers',sk2(sk3)))
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater(zero,'growth$urate'('first$umovers',sk2(sk3))) ),
inference(superposition,[status(thm)],[d174,d293]) ).
cnf(d295,plain,
( greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3)))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero)
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero) ),
inference(superposition,[status(thm)],[d207,d293]) ).
cnf(d296,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3))) ),
inference(resolution,[status(thm)],[d295,d158]) ).
cnf(d297,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3)))
| ~ greater(zero,'growth$urate'('first$umovers',sk2(sk3))) ),
inference(superposition,[status(thm)],[d32,d296]) ).
cnf(d298,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3)))
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater(zero,'growth$urate'('efficient$uproducers',sk2(sk3))) ),
inference(resolution,[status(thm)],[d297,d294]) ).
cnf(d299,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| greater(sk4(sk2(sk3)),sk2(sk3)) ),
inference(resolution,[status(thm)],[d298,d291]) ).
cnf(d300,plain,
( greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero)
| greater('growth$urate'('first$umovers',sk2(sk3)),zero)
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero) ),
inference(superposition,[status(thm)],[d165,d293]) ).
cnf(d301,plain,
( ~ greater(X0,'growth$urate'('first$umovers',sk2(sk3)))
| greater(X0,zero)
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero) ),
inference(resolution,[status(thm)],[d300,c0]) ).
cnf(d302,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3))
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero)
| greater('growth$urate'('efficient$uproducers',sk2(sk3)),zero) ),
inference(resolution,[status(thm)],[d301,d293]) ).
cnf(d303,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| greater(sk4(sk2(sk3)),sk2(sk3)) ),
inference(resolution,[status(thm)],[d302,d158]) ).
cnf(d304,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3)) ),
inference(resolution,[status(thm)],[d303,d299]) ).
cnf(d305,plain,
( 'greater$uor$uequal'(sk4(sk2(sk3)),equilibrium(sk3))
| greater(sk4(sk2(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d304,d35]) ).
cnf(d306,plain,
( 'greater$uor$uequal'(sk4(sk2(sk3)),equilibrium(sk3))
| 'greater$uor$uequal'(sk4(sk2(sk3)),equilibrium(sk3)) ),
inference(resolution,[status(thm)],[d305,c3]) ).
cnf(d307,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[d306,c12]) ).
cnf(d308,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[c17,d307]) ).
cnf(d309,plain,
( greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[d31,d308]) ).
cnf(d310,plain,
( ~ environment(sk3)
| ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk2(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[d306,c5]) ).
cnf(d311,plain,
( ~ subpopulations('first$umovers','efficient$uproducers',sk3,sk4(sk2(sk3)))
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk2(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[c17,d310]) ).
cnf(d312,plain,
( greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk2(sk3))),zero)
| 'growth$urate'('first$umovers',sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[d31,d311]) ).
cnf(d313,plain,
( greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('first$umovers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero) ),
inference(superposition,[status(thm)],[d312,d289]) ).
cnf(d314,plain,
( ~ greater(X0,'growth$urate'('first$umovers',sk4(sk2(sk3))))
| greater(X0,zero)
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero) ),
inference(resolution,[status(thm)],[d313,c0]) ).
cnf(d315,plain,
( greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero)
| greater('growth$urate'('efficient$uproducers',sk4(sk2(sk3))),zero) ),
inference(resolution,[status(thm)],[d314,d289]) ).
cnf(d316,plain,
( ~ 'in$uenvironment'(sk3,sk2(sk3))
| ~ greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(resolution,[status(thm)],[d315,c21]) ).
cnf(d317,plain,
~ greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3)))),
inference(resolution,[status(thm)],[d9,d316]) ).
cnf(d318,plain,
( greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| 'growth$urate'('efficient$uproducers',sk4(sk2(sk3))) = zero ),
inference(resolution,[status(thm)],[d317,d309]) ).
cnf(d319,plain,
( greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3))))
| greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3)))) ),
inference(superposition,[status(thm)],[d318,d289]) ).
cnf(d320,plain,
greater(zero,'growth$urate'('efficient$uproducers',sk4(sk2(sk3)))),
inference(resolution,[status(thm)],[d317,d319]) ).
cnf(d321,plain,
greater(zero,'growth$urate'('first$umovers',sk4(sk2(sk3)))),
inference(resolution,[status(thm)],[d320,d290]) ).
cnf(d322,plain,
$false,
inference(resolution,[status(thm)],[d317,d321]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT029-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n011.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sat Sep 26 00:05:15 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.44 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 194.05/50.06 % SZS status Unsatisfiable for theBenchmark.p
% 194.05/50.06 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------