%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT025+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:18:41 AM UTC 2026
% Result : Theorem 221.05s 221.38s
% Output : CNFRefutation 221.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 11
% Syntax : Number of formulae : 172 ( 19 unt; 0 def)
% Number of atoms : 708 ( 98 equ)
% Maximal formula atoms : 40 ( 4 avg)
% Number of connectives : 840 ( 304 ~; 452 |; 72 &)
% ( 0 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 157 ( 4 sgn 62 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(prove_l7,conjecture,
! [E,T] :
( ( environment(E)
& subpopulations(first_movers,efficient_producers,E,T)
& constant(number_of_organizations(E,T)) )
=> ( ( growth_rate(first_movers,T) = zero
& growth_rate(efficient_producers,T) = zero )
| ( greater(growth_rate(first_movers,T),zero)
& greater(zero,growth_rate(efficient_producers,T)) )
| ( greater(growth_rate(efficient_producers,T),zero)
& greater(zero,growth_rate(first_movers,T)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_l7) ).
fof(c12,negated_conjecture,
~ ! [E,T] :
( ( environment(E)
& subpopulations(first_movers,efficient_producers,E,T)
& constant(number_of_organizations(E,T)) )
=> ( ( growth_rate(first_movers,T) = zero
& growth_rate(efficient_producers,T) = zero )
| ( greater(growth_rate(first_movers,T),zero)
& greater(zero,growth_rate(efficient_producers,T)) )
| ( greater(growth_rate(efficient_producers,T),zero)
& greater(zero,growth_rate(first_movers,T)) ) ) ),
inference(assume_negation,[status(cth)],[prove_l7]) ).
fof(c13,negated_conjecture,
? [E,T] :
( environment(E)
& subpopulations(first_movers,efficient_producers,E,T)
& constant(number_of_organizations(E,T))
& ( growth_rate(first_movers,T) != zero
| growth_rate(efficient_producers,T) != zero )
& ( ~ greater(growth_rate(first_movers,T),zero)
| ~ greater(zero,growth_rate(efficient_producers,T)) )
& ( ~ greater(growth_rate(efficient_producers,T),zero)
| ~ greater(zero,growth_rate(first_movers,T)) ) ),
inference(fof_nnf,[status(thm)],[c12]) ).
fof(c14,negated_conjecture,
? [X2,X3] :
( environment(X2)
& subpopulations(first_movers,efficient_producers,X2,X3)
& constant(number_of_organizations(X2,X3))
& ( growth_rate(first_movers,X3) != zero
| growth_rate(efficient_producers,X3) != zero )
& ( ~ greater(growth_rate(first_movers,X3),zero)
| ~ greater(zero,growth_rate(efficient_producers,X3)) )
& ( ~ greater(growth_rate(efficient_producers,X3),zero)
| ~ greater(zero,growth_rate(first_movers,X3)) ) ),
inference(variable_rename,[status(thm)],[c13]) ).
fof(c15,negated_conjecture,
( environment(skolem0001)
& subpopulations(first_movers,efficient_producers,skolem0001,skolem0002)
& constant(number_of_organizations(skolem0001,skolem0002))
& ( growth_rate(first_movers,skolem0002) != zero
| growth_rate(efficient_producers,skolem0002) != zero )
& ( ~ greater(growth_rate(first_movers,skolem0002),zero)
| ~ greater(zero,growth_rate(efficient_producers,skolem0002)) )
& ( ~ greater(growth_rate(efficient_producers,skolem0002),zero)
| ~ greater(zero,growth_rate(first_movers,skolem0002)) ) ),
inference(skolemize,[status(esa)],[c14]) ).
cnf(c16,negated_conjecture,
environment(skolem0001),
inference(split_conjunct,[status(thm)],[c15]) ).
cnf(c17,negated_conjecture,
subpopulations(first_movers,efficient_producers,skolem0001,skolem0002),
inference(split_conjunct,[status(thm)],[c15]) ).
fof(mp_time_point_occur,axiom,
! [E,T] :
( ( environment(E)
& subpopulations(first_movers,efficient_producers,E,T) )
=> in_environment(E,T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_time_point_occur) ).
fof(c27,plain,
! [E,T] :
( ~ environment(E)
| ~ subpopulations(first_movers,efficient_producers,E,T)
| in_environment(E,T) ),
inference(fof_nnf,[status(thm)],[mp_time_point_occur]) ).
fof(c28,plain,
! [X7,X8] :
( ~ environment(X7)
| ~ subpopulations(first_movers,efficient_producers,X7,X8)
| in_environment(X7,X8) ),
inference(variable_rename,[status(thm)],[c27]) ).
cnf(c29,plain,
( ~ environment(X102)
| ~ subpopulations(first_movers,efficient_producers,X102,X103)
| in_environment(X102,X103) ),
inference(split_conjunct,[status(thm)],[c28]) ).
cnf(c86,plain,
( ~ environment(skolem0001)
| in_environment(skolem0001,skolem0002) ),
inference(resolution,[status(thm)],[c29,c17]) ).
cnf(c87,plain,
in_environment(skolem0001,skolem0002),
inference(resolution,[status(thm)],[c86,c16]) ).
fof(mp_subpopulations,axiom,
! [E,T] :
( ( environment(E)
& in_environment(E,T) )
=> ( subpopulation(first_movers,E,T)
& subpopulation(efficient_producers,E,T) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_subpopulations) ).
fof(c52,plain,
! [E,T] :
( ~ environment(E)
| ~ in_environment(E,T)
| ( subpopulation(first_movers,E,T)
& subpopulation(efficient_producers,E,T) ) ),
inference(fof_nnf,[status(thm)],[mp_subpopulations]) ).
fof(c53,plain,
! [X17,X18] :
( ~ environment(X17)
| ~ in_environment(X17,X18)
| ( subpopulation(first_movers,X17,X18)
& subpopulation(efficient_producers,X17,X18) ) ),
inference(variable_rename,[status(thm)],[c52]) ).
fof(c54,plain,
! [X17,X18] :
( ( ~ environment(X17)
| ~ in_environment(X17,X18)
| subpopulation(first_movers,X17,X18) )
& ( ~ environment(X17)
| ~ in_environment(X17,X18)
| subpopulation(efficient_producers,X17,X18) ) ),
inference(distribute,[status(thm)],[c53]) ).
cnf(c55,plain,
( ~ environment(X52)
| ~ in_environment(X52,X53)
| subpopulation(first_movers,X52,X53) ),
inference(split_conjunct,[status(thm)],[c54]) ).
cnf(c88,plain,
( ~ environment(skolem0001)
| subpopulation(first_movers,skolem0001,skolem0002) ),
inference(resolution,[status(thm)],[c87,c55]) ).
cnf(c90,plain,
subpopulation(first_movers,skolem0001,skolem0002),
inference(resolution,[status(thm)],[c88,c16]) ).
fof(mp_non_zero_producers,axiom,
! [E,T] :
( ( environment(E)
& subpopulations(first_movers,efficient_producers,E,T) )
=> ( greater(cardinality_at_time(first_movers,T),zero)
& greater(cardinality_at_time(efficient_producers,T),zero) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_non_zero_producers) ).
fof(c30,plain,
! [E,T] :
( ~ environment(E)
| ~ subpopulations(first_movers,efficient_producers,E,T)
| ( greater(cardinality_at_time(first_movers,T),zero)
& greater(cardinality_at_time(efficient_producers,T),zero) ) ),
inference(fof_nnf,[status(thm)],[mp_non_zero_producers]) ).
fof(c31,plain,
! [X9,X10] :
( ~ environment(X9)
| ~ subpopulations(first_movers,efficient_producers,X9,X10)
| ( greater(cardinality_at_time(first_movers,X10),zero)
& greater(cardinality_at_time(efficient_producers,X10),zero) ) ),
inference(variable_rename,[status(thm)],[c30]) ).
fof(c32,plain,
! [X9,X10] :
( ( ~ environment(X9)
| ~ subpopulations(first_movers,efficient_producers,X9,X10)
| greater(cardinality_at_time(first_movers,X10),zero) )
& ( ~ environment(X9)
| ~ subpopulations(first_movers,efficient_producers,X9,X10)
| greater(cardinality_at_time(efficient_producers,X10),zero) ) ),
inference(distribute,[status(thm)],[c31]) ).
cnf(c33,plain,
( ~ environment(X164)
| ~ subpopulations(first_movers,efficient_producers,X164,X163)
| greater(cardinality_at_time(first_movers,X163),zero) ),
inference(split_conjunct,[status(thm)],[c32]) ).
cnf(c106,plain,
( ~ environment(skolem0001)
| greater(cardinality_at_time(first_movers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c33,c17]) ).
cnf(c107,plain,
greater(cardinality_at_time(first_movers,skolem0002),zero),
inference(resolution,[status(thm)],[c106,c16]) ).
fof(mp_growth_rate,axiom,
! [X,E,T] :
( ( environment(E)
& in_environment(E,T)
& subpopulation(X,E,T)
& greater(cardinality_at_time(X,T),zero) )
=> ( ( constant(cardinality_at_time(X,T))
=> growth_rate(X,T) = zero )
& ( increases(cardinality_at_time(X,T))
=> greater(growth_rate(X,T),zero) )
& ( decreases(cardinality_at_time(X,T))
=> greater(zero,growth_rate(X,T)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_growth_rate) ).
fof(c35,plain,
! [X,E,T] :
( ~ environment(E)
| ~ in_environment(E,T)
| ~ subpopulation(X,E,T)
| ~ greater(cardinality_at_time(X,T),zero)
| ( ( ~ constant(cardinality_at_time(X,T))
| growth_rate(X,T) = zero )
& ( ~ increases(cardinality_at_time(X,T))
| greater(growth_rate(X,T),zero) )
& ( ~ decreases(cardinality_at_time(X,T))
| greater(zero,growth_rate(X,T)) ) ) ),
inference(fof_nnf,[status(thm)],[mp_growth_rate]) ).
fof(c36,plain,
! [X11,X12,X13] :
( ~ environment(X12)
| ~ in_environment(X12,X13)
| ~ subpopulation(X11,X12,X13)
| ~ greater(cardinality_at_time(X11,X13),zero)
| ( ( ~ constant(cardinality_at_time(X11,X13))
| growth_rate(X11,X13) = zero )
& ( ~ increases(cardinality_at_time(X11,X13))
| greater(growth_rate(X11,X13),zero) )
& ( ~ decreases(cardinality_at_time(X11,X13))
| greater(zero,growth_rate(X11,X13)) ) ) ),
inference(variable_rename,[status(thm)],[c35]) ).
fof(c37,plain,
! [X11,X12,X13] :
( ( ~ environment(X12)
| ~ in_environment(X12,X13)
| ~ subpopulation(X11,X12,X13)
| ~ greater(cardinality_at_time(X11,X13),zero)
| ~ constant(cardinality_at_time(X11,X13))
| growth_rate(X11,X13) = zero )
& ( ~ environment(X12)
| ~ in_environment(X12,X13)
| ~ subpopulation(X11,X12,X13)
| ~ greater(cardinality_at_time(X11,X13),zero)
| ~ increases(cardinality_at_time(X11,X13))
| greater(growth_rate(X11,X13),zero) )
& ( ~ environment(X12)
| ~ in_environment(X12,X13)
| ~ subpopulation(X11,X12,X13)
| ~ greater(cardinality_at_time(X11,X13),zero)
| ~ decreases(cardinality_at_time(X11,X13))
| greater(zero,growth_rate(X11,X13)) ) ),
inference(distribute,[status(thm)],[c36]) ).
cnf(c39,plain,
( ~ environment(X187)
| ~ in_environment(X187,X185)
| ~ subpopulation(X186,X187,X185)
| ~ greater(cardinality_at_time(X186,X185),zero)
| ~ increases(cardinality_at_time(X186,X185))
| greater(growth_rate(X186,X185),zero) ),
inference(split_conjunct,[status(thm)],[c37]) ).
cnf(c124,plain,
( ~ environment(X221)
| ~ in_environment(X221,skolem0002)
| ~ subpopulation(first_movers,X221,skolem0002)
| ~ increases(cardinality_at_time(first_movers,skolem0002))
| greater(growth_rate(first_movers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c39,c107]) ).
cnf(c56,plain,
( ~ environment(X54)
| ~ in_environment(X54,X55)
| subpopulation(efficient_producers,X54,X55) ),
inference(split_conjunct,[status(thm)],[c54]) ).
cnf(c89,plain,
( ~ environment(skolem0001)
| subpopulation(efficient_producers,skolem0001,skolem0002) ),
inference(resolution,[status(thm)],[c87,c56]) ).
cnf(c92,plain,
subpopulation(efficient_producers,skolem0001,skolem0002),
inference(resolution,[status(thm)],[c89,c16]) ).
cnf(c34,plain,
( ~ environment(X172)
| ~ subpopulations(first_movers,efficient_producers,X172,X171)
| greater(cardinality_at_time(efficient_producers,X171),zero) ),
inference(split_conjunct,[status(thm)],[c32]) ).
cnf(c112,plain,
( ~ environment(skolem0001)
| greater(cardinality_at_time(efficient_producers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c34,c17]) ).
cnf(c113,plain,
greater(cardinality_at_time(efficient_producers,skolem0002),zero),
inference(resolution,[status(thm)],[c112,c16]) ).
cnf(c123,plain,
( ~ environment(X220)
| ~ in_environment(X220,skolem0002)
| ~ subpopulation(efficient_producers,X220,skolem0002)
| ~ increases(cardinality_at_time(efficient_producers,skolem0002))
| greater(growth_rate(efficient_producers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c39,c113]) ).
cnf(c20,negated_conjecture,
( ~ greater(growth_rate(first_movers,skolem0002),zero)
| ~ greater(zero,growth_rate(efficient_producers,skolem0002)) ),
inference(split_conjunct,[status(thm)],[c15]) ).
cnf(c40,plain,
( ~ environment(X196)
| ~ in_environment(X196,X194)
| ~ subpopulation(X195,X196,X194)
| ~ greater(cardinality_at_time(X195,X194),zero)
| ~ decreases(cardinality_at_time(X195,X194))
| greater(zero,growth_rate(X195,X194)) ),
inference(split_conjunct,[status(thm)],[c37]) ).
cnf(c128,plain,
( ~ environment(X222)
| ~ in_environment(X222,skolem0002)
| ~ subpopulation(efficient_producers,X222,skolem0002)
| ~ decreases(cardinality_at_time(efficient_producers,skolem0002))
| greater(zero,growth_rate(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c40,c113]) ).
cnf(c38,plain,
( ~ environment(X177)
| ~ in_environment(X177,X175)
| ~ subpopulation(X176,X177,X175)
| ~ greater(cardinality_at_time(X176,X175),zero)
| ~ constant(cardinality_at_time(X176,X175))
| growth_rate(X176,X175) = zero ),
inference(split_conjunct,[status(thm)],[c37]) ).
cnf(c118,plain,
( ~ environment(X219)
| ~ in_environment(X219,skolem0002)
| ~ subpopulation(first_movers,X219,skolem0002)
| ~ constant(cardinality_at_time(first_movers,skolem0002))
| growth_rate(first_movers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c38,c107]) ).
cnf(reflexivity,axiom,
X22 = X22,
theory(equality) ).
fof(mp_abc_sum_increase,axiom,
! [A,B,C] :
( ( A = sum(B,C)
& constant(A) )
=> ( ( constant(B)
& constant(C) )
| ( increases(B)
& decreases(C) )
| ( decreases(B)
& increases(C) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_abc_sum_increase) ).
fof(c41,plain,
! [A,B,C] :
( A != sum(B,C)
| ~ constant(A)
| ( constant(B)
& constant(C) )
| ( increases(B)
& decreases(C) )
| ( decreases(B)
& increases(C) ) ),
inference(fof_nnf,[status(thm)],[mp_abc_sum_increase]) ).
fof(c42,plain,
! [X14,X15,X16] :
( X14 != sum(X15,X16)
| ~ constant(X14)
| ( constant(X15)
& constant(X16) )
| ( increases(X15)
& decreases(X16) )
| ( decreases(X15)
& increases(X16) ) ),
inference(variable_rename,[status(thm)],[c41]) ).
fof(c43,plain,
! [X14,X15,X16] :
( ( X14 != sum(X15,X16)
| ~ constant(X14)
| constant(X15)
| increases(X15)
| decreases(X15) )
& ( X14 != sum(X15,X16)
| ~ constant(X14)
| constant(X15)
| increases(X15)
| increases(X16) )
& ( X14 != sum(X15,X16)
| ~ constant(X14)
| constant(X15)
| decreases(X16)
| decreases(X15) )
& ( X14 != sum(X15,X16)
| ~ constant(X14)
| constant(X15)
| decreases(X16)
| increases(X16) )
& ( X14 != sum(X15,X16)
| ~ constant(X14)
| constant(X16)
| increases(X15)
| decreases(X15) )
& ( X14 != sum(X15,X16)
| ~ constant(X14)
| constant(X16)
| increases(X15)
| increases(X16) )
& ( X14 != sum(X15,X16)
| ~ constant(X14)
| constant(X16)
| decreases(X16)
| decreases(X15) )
& ( X14 != sum(X15,X16)
| ~ constant(X14)
| constant(X16)
| decreases(X16)
| increases(X16) ) ),
inference(distribute,[status(thm)],[c42]) ).
cnf(c47,plain,
( X138 != sum(X139,X140)
| ~ constant(X138)
| constant(X139)
| decreases(X140)
| increases(X140) ),
inference(split_conjunct,[status(thm)],[c43]) ).
cnf(c101,plain,
( ~ constant(sum(X142,X141))
| constant(X142)
| decreases(X141)
| increases(X141) ),
inference(resolution,[status(thm)],[c47,reflexivity]) ).
cnf(c18,negated_conjecture,
constant(number_of_organizations(skolem0001,skolem0002)),
inference(split_conjunct,[status(thm)],[c15]) ).
cnf(c8,axiom,
( X36 != X35
| ~ constant(X36)
| constant(X35) ),
theory(equality) ).
fof(mp_only_members,axiom,
! [E,X,T] :
( ( environment(E)
& subpopulation(X,E,T)
& ( greater(cardinality_at_time(X,T),zero)
=> ( X = efficient_producers
| X = first_movers ) ) )
=> number_of_organizations(E,T) = sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_only_members) ).
fof(c57,plain,
! [E,X,T] :
( ~ environment(E)
| ~ subpopulation(X,E,T)
| ( greater(cardinality_at_time(X,T),zero)
& X != efficient_producers
& X != first_movers )
| number_of_organizations(E,T) = sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)) ),
inference(fof_nnf,[status(thm)],[mp_only_members]) ).
fof(c58,plain,
! [X19,X20,X21] :
( ~ environment(X19)
| ~ subpopulation(X20,X19,X21)
| ( greater(cardinality_at_time(X20,X21),zero)
& X20 != efficient_producers
& X20 != first_movers )
| number_of_organizations(X19,X21) = sum(cardinality_at_time(first_movers,X21),cardinality_at_time(efficient_producers,X21)) ),
inference(variable_rename,[status(thm)],[c57]) ).
fof(c59,plain,
! [X19,X20,X21] :
( ( ~ environment(X19)
| ~ subpopulation(X20,X19,X21)
| greater(cardinality_at_time(X20,X21),zero)
| number_of_organizations(X19,X21) = sum(cardinality_at_time(first_movers,X21),cardinality_at_time(efficient_producers,X21)) )
& ( ~ environment(X19)
| ~ subpopulation(X20,X19,X21)
| X20 != efficient_producers
| number_of_organizations(X19,X21) = sum(cardinality_at_time(first_movers,X21),cardinality_at_time(efficient_producers,X21)) )
& ( ~ environment(X19)
| ~ subpopulation(X20,X19,X21)
| X20 != first_movers
| number_of_organizations(X19,X21) = sum(cardinality_at_time(first_movers,X21),cardinality_at_time(efficient_producers,X21)) ) ),
inference(distribute,[status(thm)],[c58]) ).
cnf(c61,plain,
( ~ environment(X212)
| ~ subpopulation(X214,X212,X213)
| X214 != efficient_producers
| number_of_organizations(X212,X213) = sum(cardinality_at_time(first_movers,X213),cardinality_at_time(efficient_producers,X213)) ),
inference(split_conjunct,[status(thm)],[c59]) ).
cnf(c136,plain,
( ~ environment(skolem0001)
| efficient_producers != efficient_producers
| number_of_organizations(skolem0001,skolem0002) = sum(cardinality_at_time(first_movers,skolem0002),cardinality_at_time(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c61,c92]) ).
cnf(c140,plain,
( ~ environment(skolem0001)
| number_of_organizations(skolem0001,skolem0002) = sum(cardinality_at_time(first_movers,skolem0002),cardinality_at_time(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c136,reflexivity]) ).
cnf(c141,plain,
number_of_organizations(skolem0001,skolem0002) = sum(cardinality_at_time(first_movers,skolem0002),cardinality_at_time(efficient_producers,skolem0002)),
inference(resolution,[status(thm)],[c140,c16]) ).
cnf(c148,plain,
( ~ constant(number_of_organizations(skolem0001,skolem0002))
| constant(sum(cardinality_at_time(first_movers,skolem0002),cardinality_at_time(efficient_producers,skolem0002))) ),
inference(resolution,[status(thm)],[c141,c8]) ).
cnf(c186,plain,
constant(sum(cardinality_at_time(first_movers,skolem0002),cardinality_at_time(efficient_producers,skolem0002))),
inference(resolution,[status(thm)],[c148,c18]) ).
cnf(c188,plain,
( constant(cardinality_at_time(first_movers,skolem0002))
| decreases(cardinality_at_time(efficient_producers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c186,c101]) ).
cnf(c197,plain,
( decreases(cardinality_at_time(efficient_producers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(X375)
| ~ in_environment(X375,skolem0002)
| ~ subpopulation(first_movers,X375,skolem0002)
| growth_rate(first_movers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c188,c118]) ).
cnf(c966,plain,
( decreases(cardinality_at_time(efficient_producers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002)
| growth_rate(first_movers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c197,c90]) ).
cnf(c7606,plain,
( decreases(cardinality_at_time(efficient_producers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(skolem0001)
| growth_rate(first_movers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c966,c87]) ).
cnf(c7652,plain,
( decreases(cardinality_at_time(efficient_producers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002))
| growth_rate(first_movers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c7606,c16]) ).
cnf(c19,negated_conjecture,
( growth_rate(first_movers,skolem0002) != zero
| growth_rate(efficient_producers,skolem0002) != zero ),
inference(split_conjunct,[status(thm)],[c15]) ).
cnf(c117,plain,
( ~ environment(X218)
| ~ in_environment(X218,skolem0002)
| ~ subpopulation(efficient_producers,X218,skolem0002)
| ~ constant(cardinality_at_time(efficient_producers,skolem0002))
| growth_rate(efficient_producers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c38,c113]) ).
cnf(c51,plain,
( X158 != sum(X159,X160)
| ~ constant(X158)
| constant(X160)
| decreases(X160)
| increases(X160) ),
inference(split_conjunct,[status(thm)],[c43]) ).
cnf(c105,plain,
( ~ constant(sum(X162,X161))
| constant(X161)
| decreases(X161)
| increases(X161) ),
inference(resolution,[status(thm)],[c51,reflexivity]) ).
cnf(c190,plain,
( constant(cardinality_at_time(efficient_producers,skolem0002))
| decreases(cardinality_at_time(efficient_producers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c186,c105]) ).
cnf(c202,plain,
( decreases(cardinality_at_time(efficient_producers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(X412)
| ~ in_environment(X412,skolem0002)
| ~ subpopulation(efficient_producers,X412,skolem0002)
| growth_rate(efficient_producers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c190,c117]) ).
cnf(c1006,plain,
( decreases(cardinality_at_time(efficient_producers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002)
| growth_rate(efficient_producers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c202,c92]) ).
cnf(c11931,plain,
( decreases(cardinality_at_time(efficient_producers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(skolem0001)
| growth_rate(efficient_producers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c1006,c87]) ).
cnf(c11932,plain,
( decreases(cardinality_at_time(efficient_producers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002))
| growth_rate(efficient_producers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c11931,c16]) ).
cnf(c11979,plain,
( decreases(cardinality_at_time(efficient_producers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002))
| growth_rate(first_movers,skolem0002) != zero ),
inference(resolution,[status(thm)],[c11932,c19]) ).
cnf(c12001,plain,
( decreases(cardinality_at_time(efficient_producers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c11979,c7652]) ).
cnf(c12002,plain,
( increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(X1189)
| ~ in_environment(X1189,skolem0002)
| ~ subpopulation(efficient_producers,X1189,skolem0002)
| greater(zero,growth_rate(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c12001,c128]) ).
cnf(c12364,plain,
( increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002)
| greater(zero,growth_rate(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c12002,c92]) ).
cnf(c12365,plain,
( increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(skolem0001)
| greater(zero,growth_rate(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c12364,c87]) ).
cnf(c12544,plain,
( increases(cardinality_at_time(efficient_producers,skolem0002))
| greater(zero,growth_rate(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c12365,c16]) ).
cnf(c12546,plain,
( increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ greater(growth_rate(first_movers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c12544,c20]) ).
cnf(c45,plain,
( X128 != sum(X129,X130)
| ~ constant(X128)
| constant(X129)
| increases(X129)
| increases(X130) ),
inference(split_conjunct,[status(thm)],[c43]) ).
cnf(c99,plain,
( ~ constant(sum(X132,X131))
| constant(X132)
| increases(X132)
| increases(X131) ),
inference(resolution,[status(thm)],[c45,reflexivity]) ).
cnf(c187,plain,
( constant(cardinality_at_time(first_movers,skolem0002))
| increases(cardinality_at_time(first_movers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c186,c99]) ).
cnf(c199,plain,
( ~ environment(X391)
| ~ in_environment(X391,skolem0002)
| ~ subpopulation(first_movers,X391,skolem0002)
| greater(growth_rate(first_movers,skolem0002),zero)
| constant(cardinality_at_time(first_movers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c124,c187]) ).
cnf(c988,plain,
( ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002)
| greater(growth_rate(first_movers,skolem0002),zero)
| constant(cardinality_at_time(first_movers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c199,c90]) ).
cnf(c9695,plain,
( ~ environment(skolem0001)
| greater(growth_rate(first_movers,skolem0002),zero)
| constant(cardinality_at_time(first_movers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c988,c87]) ).
cnf(c9696,plain,
( greater(growth_rate(first_movers,skolem0002),zero)
| constant(cardinality_at_time(first_movers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c9695,c16]) ).
cnf(c12548,plain,
( increases(cardinality_at_time(efficient_producers,skolem0002))
| constant(cardinality_at_time(first_movers,skolem0002)) ),
inference(resolution,[status(thm)],[c12546,c9696]) ).
cnf(c12551,plain,
( increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(X1204)
| ~ in_environment(X1204,skolem0002)
| ~ subpopulation(first_movers,X1204,skolem0002)
| growth_rate(first_movers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c12548,c118]) ).
cnf(c12701,plain,
( increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002)
| growth_rate(first_movers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c12551,c90]) ).
cnf(c12702,plain,
( increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(skolem0001)
| growth_rate(first_movers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c12701,c87]) ).
cnf(c12774,plain,
( increases(cardinality_at_time(efficient_producers,skolem0002))
| growth_rate(first_movers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c12702,c16]) ).
cnf(c49,plain,
( X148 != sum(X149,X150)
| ~ constant(X148)
| constant(X150)
| increases(X149)
| increases(X150) ),
inference(split_conjunct,[status(thm)],[c43]) ).
cnf(c103,plain,
( ~ constant(sum(X151,X152))
| constant(X152)
| increases(X151)
| increases(X152) ),
inference(resolution,[status(thm)],[c49,reflexivity]) ).
cnf(c192,plain,
( constant(cardinality_at_time(efficient_producers,skolem0002))
| increases(cardinality_at_time(first_movers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c186,c103]) ).
cnf(c205,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(X440)
| ~ in_environment(X440,skolem0002)
| ~ subpopulation(efficient_producers,X440,skolem0002)
| growth_rate(efficient_producers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c192,c117]) ).
cnf(c1249,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002)
| growth_rate(efficient_producers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c205,c92]) ).
cnf(c194769,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(skolem0001)
| growth_rate(efficient_producers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c1249,c87]) ).
cnf(c194770,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002))
| growth_rate(efficient_producers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c194769,c16]) ).
cnf(c194942,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002))
| growth_rate(first_movers,skolem0002) != zero ),
inference(resolution,[status(thm)],[c194770,c19]) ).
cnf(c195503,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| increases(cardinality_at_time(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c194942,c12774]) ).
cnf(c195504,plain,
( increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(X6383)
| ~ in_environment(X6383,skolem0002)
| ~ subpopulation(first_movers,X6383,skolem0002)
| greater(growth_rate(first_movers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c195503,c124]) ).
cnf(c197488,plain,
( increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002)
| greater(growth_rate(first_movers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c195504,c90]) ).
cnf(c197711,plain,
( increases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(skolem0001)
| greater(growth_rate(first_movers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c197488,c87]) ).
cnf(c197712,plain,
( increases(cardinality_at_time(efficient_producers,skolem0002))
| greater(growth_rate(first_movers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c197711,c16]) ).
cnf(c197714,plain,
increases(cardinality_at_time(efficient_producers,skolem0002)),
inference(resolution,[status(thm)],[c197712,c12546]) ).
cnf(c197717,plain,
( ~ environment(X6388)
| ~ in_environment(X6388,skolem0002)
| ~ subpopulation(efficient_producers,X6388,skolem0002)
| greater(growth_rate(efficient_producers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c197714,c123]) ).
cnf(c197865,plain,
( ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002)
| greater(growth_rate(efficient_producers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c197717,c92]) ).
cnf(c197866,plain,
( ~ environment(skolem0001)
| greater(growth_rate(efficient_producers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c197865,c87]) ).
cnf(c197867,plain,
greater(growth_rate(efficient_producers,skolem0002),zero),
inference(resolution,[status(thm)],[c197866,c16]) ).
cnf(c21,negated_conjecture,
( ~ greater(growth_rate(efficient_producers,skolem0002),zero)
| ~ greater(zero,growth_rate(first_movers,skolem0002)) ),
inference(split_conjunct,[status(thm)],[c15]) ).
cnf(c129,plain,
( ~ environment(X225)
| ~ in_environment(X225,skolem0002)
| ~ subpopulation(first_movers,X225,skolem0002)
| ~ decreases(cardinality_at_time(first_movers,skolem0002))
| greater(zero,growth_rate(first_movers,skolem0002)) ),
inference(resolution,[status(thm)],[c40,c107]) ).
cnf(c44,plain,
( X115 != sum(X116,X117)
| ~ constant(X115)
| constant(X116)
| increases(X116)
| decreases(X116) ),
inference(split_conjunct,[status(thm)],[c43]) ).
cnf(c97,plain,
( ~ constant(sum(X126,X127))
| constant(X126)
| increases(X126)
| decreases(X126) ),
inference(resolution,[status(thm)],[c44,reflexivity]) ).
cnf(c189,plain,
( constant(cardinality_at_time(first_movers,skolem0002))
| increases(cardinality_at_time(first_movers,skolem0002))
| decreases(cardinality_at_time(first_movers,skolem0002)) ),
inference(resolution,[status(thm)],[c186,c97]) ).
cnf(c200,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| decreases(cardinality_at_time(first_movers,skolem0002))
| ~ environment(X399)
| ~ in_environment(X399,skolem0002)
| ~ subpopulation(first_movers,X399,skolem0002)
| growth_rate(first_movers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c189,c118]) ).
cnf(c999,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| decreases(cardinality_at_time(first_movers,skolem0002))
| ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002)
| growth_rate(first_movers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c200,c90]) ).
cnf(c9928,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| decreases(cardinality_at_time(first_movers,skolem0002))
| ~ environment(skolem0001)
| growth_rate(first_movers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c999,c87]) ).
cnf(c9929,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| decreases(cardinality_at_time(first_movers,skolem0002))
| growth_rate(first_movers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c9928,c16]) ).
cnf(c48,plain,
( X143 != sum(X144,X145)
| ~ constant(X143)
| constant(X145)
| increases(X144)
| decreases(X144) ),
inference(split_conjunct,[status(thm)],[c43]) ).
cnf(c102,plain,
( ~ constant(sum(X147,X146))
| constant(X146)
| increases(X147)
| decreases(X147) ),
inference(resolution,[status(thm)],[c48,reflexivity]) ).
cnf(c193,plain,
( constant(cardinality_at_time(efficient_producers,skolem0002))
| increases(cardinality_at_time(first_movers,skolem0002))
| decreases(cardinality_at_time(first_movers,skolem0002)) ),
inference(resolution,[status(thm)],[c186,c102]) ).
cnf(c208,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| decreases(cardinality_at_time(first_movers,skolem0002))
| ~ environment(X473)
| ~ in_environment(X473,skolem0002)
| ~ subpopulation(efficient_producers,X473,skolem0002)
| growth_rate(efficient_producers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c193,c117]) ).
cnf(c1612,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| decreases(cardinality_at_time(first_movers,skolem0002))
| ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002)
| growth_rate(efficient_producers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c208,c92]) ).
cnf(c200788,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| decreases(cardinality_at_time(first_movers,skolem0002))
| ~ environment(skolem0001)
| growth_rate(efficient_producers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c1612,c87]) ).
cnf(c200789,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| decreases(cardinality_at_time(first_movers,skolem0002))
| growth_rate(efficient_producers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c200788,c16]) ).
cnf(c200897,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| decreases(cardinality_at_time(first_movers,skolem0002))
| growth_rate(first_movers,skolem0002) != zero ),
inference(resolution,[status(thm)],[c200789,c19]) ).
cnf(c201091,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| decreases(cardinality_at_time(first_movers,skolem0002)) ),
inference(resolution,[status(thm)],[c200897,c9929]) ).
cnf(c201094,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| ~ environment(X6575)
| ~ in_environment(X6575,skolem0002)
| ~ subpopulation(first_movers,X6575,skolem0002)
| greater(zero,growth_rate(first_movers,skolem0002)) ),
inference(resolution,[status(thm)],[c201091,c129]) ).
cnf(c202694,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002)
| greater(zero,growth_rate(first_movers,skolem0002)) ),
inference(resolution,[status(thm)],[c201094,c90]) ).
cnf(c202695,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| ~ environment(skolem0001)
| greater(zero,growth_rate(first_movers,skolem0002)) ),
inference(resolution,[status(thm)],[c202694,c87]) ).
cnf(c202696,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| greater(zero,growth_rate(first_movers,skolem0002)) ),
inference(resolution,[status(thm)],[c202695,c16]) ).
cnf(c202698,plain,
( increases(cardinality_at_time(first_movers,skolem0002))
| ~ greater(growth_rate(efficient_producers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c202696,c21]) ).
cnf(c202700,plain,
increases(cardinality_at_time(first_movers,skolem0002)),
inference(resolution,[status(thm)],[c202698,c197867]) ).
cnf(c202701,plain,
( ~ environment(X6577)
| ~ in_environment(X6577,skolem0002)
| ~ subpopulation(first_movers,X6577,skolem0002)
| greater(growth_rate(first_movers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c202700,c124]) ).
cnf(c202702,plain,
( ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002)
| greater(growth_rate(first_movers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c202701,c90]) ).
cnf(c202703,plain,
( ~ environment(skolem0001)
| greater(growth_rate(first_movers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c202702,c87]) ).
cnf(c202704,plain,
greater(growth_rate(first_movers,skolem0002),zero),
inference(resolution,[status(thm)],[c202703,c16]) ).
cnf(symmetry,axiom,
( X23 != X24
| X24 = X23 ),
theory(equality) ).
cnf(c46,plain,
( X133 != sum(X134,X135)
| ~ constant(X133)
| constant(X134)
| decreases(X135)
| decreases(X134) ),
inference(split_conjunct,[status(thm)],[c43]) ).
cnf(c100,plain,
( ~ constant(sum(X137,X136))
| constant(X137)
| decreases(X136)
| decreases(X137) ),
inference(resolution,[status(thm)],[c46,reflexivity]) ).
cnf(c191,plain,
( constant(cardinality_at_time(first_movers,skolem0002))
| decreases(cardinality_at_time(efficient_producers,skolem0002))
| decreases(cardinality_at_time(first_movers,skolem0002)) ),
inference(resolution,[status(thm)],[c186,c100]) ).
cnf(c204,plain,
( decreases(cardinality_at_time(efficient_producers,skolem0002))
| decreases(cardinality_at_time(first_movers,skolem0002))
| ~ environment(X429)
| ~ in_environment(X429,skolem0002)
| ~ subpopulation(first_movers,X429,skolem0002)
| growth_rate(first_movers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c191,c118]) ).
cnf(c1128,plain,
( decreases(cardinality_at_time(efficient_producers,skolem0002))
| decreases(cardinality_at_time(first_movers,skolem0002))
| ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002)
| growth_rate(first_movers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c204,c90]) ).
cnf(c186079,plain,
( decreases(cardinality_at_time(efficient_producers,skolem0002))
| decreases(cardinality_at_time(first_movers,skolem0002))
| ~ environment(skolem0001)
| growth_rate(first_movers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c1128,c87]) ).
cnf(c186881,plain,
( decreases(cardinality_at_time(efficient_producers,skolem0002))
| decreases(cardinality_at_time(first_movers,skolem0002))
| growth_rate(first_movers,skolem0002) = zero ),
inference(resolution,[status(thm)],[c186079,c16]) ).
cnf(c186985,plain,
( decreases(cardinality_at_time(efficient_producers,skolem0002))
| decreases(cardinality_at_time(first_movers,skolem0002))
| zero = growth_rate(first_movers,skolem0002) ),
inference(resolution,[status(thm)],[c186881,symmetry]) ).
cnf(c6,axiom,
( X105 != X104
| X106 != X107
| ~ greater(X105,X106)
| greater(X104,X107) ),
theory(equality) ).
cnf(c201093,plain,
( decreases(cardinality_at_time(first_movers,skolem0002))
| ~ environment(X6562)
| ~ in_environment(X6562,skolem0002)
| ~ subpopulation(first_movers,X6562,skolem0002)
| greater(growth_rate(first_movers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c201091,c124]) ).
cnf(c202387,plain,
( decreases(cardinality_at_time(first_movers,skolem0002))
| ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002)
| greater(growth_rate(first_movers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c201093,c90]) ).
cnf(c202388,plain,
( decreases(cardinality_at_time(first_movers,skolem0002))
| ~ environment(skolem0001)
| greater(growth_rate(first_movers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c202387,c87]) ).
cnf(c202389,plain,
( decreases(cardinality_at_time(first_movers,skolem0002))
| greater(growth_rate(first_movers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c202388,c16]) ).
cnf(c202535,plain,
( decreases(cardinality_at_time(first_movers,skolem0002))
| growth_rate(first_movers,skolem0002) != X6567
| zero != X6566
| greater(X6567,X6566) ),
inference(resolution,[status(thm)],[c202389,c6]) ).
cnf(c202536,plain,
( decreases(cardinality_at_time(first_movers,skolem0002))
| zero != X6569
| greater(zero,X6569)
| decreases(cardinality_at_time(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c202535,c186881]) ).
cnf(c202541,plain,
( decreases(cardinality_at_time(first_movers,skolem0002))
| greater(zero,growth_rate(first_movers,skolem0002))
| decreases(cardinality_at_time(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c202536,c186985]) ).
cnf(c202545,plain,
( greater(zero,growth_rate(first_movers,skolem0002))
| decreases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(X6587)
| ~ in_environment(X6587,skolem0002)
| ~ subpopulation(first_movers,X6587,skolem0002) ),
inference(resolution,[status(thm)],[c202541,c129]) ).
cnf(c202994,plain,
( greater(zero,growth_rate(first_movers,skolem0002))
| decreases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002) ),
inference(resolution,[status(thm)],[c202545,c90]) ).
cnf(c202995,plain,
( greater(zero,growth_rate(first_movers,skolem0002))
| decreases(cardinality_at_time(efficient_producers,skolem0002))
| ~ environment(skolem0001) ),
inference(resolution,[status(thm)],[c202994,c87]) ).
cnf(c202996,plain,
( greater(zero,growth_rate(first_movers,skolem0002))
| decreases(cardinality_at_time(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c202995,c16]) ).
cnf(c202997,plain,
( decreases(cardinality_at_time(efficient_producers,skolem0002))
| ~ greater(growth_rate(efficient_producers,skolem0002),zero) ),
inference(resolution,[status(thm)],[c202996,c21]) ).
cnf(c203000,plain,
decreases(cardinality_at_time(efficient_producers,skolem0002)),
inference(resolution,[status(thm)],[c202997,c197867]) ).
cnf(c203570,plain,
( ~ environment(X6592)
| ~ in_environment(X6592,skolem0002)
| ~ subpopulation(efficient_producers,X6592,skolem0002)
| greater(zero,growth_rate(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c203000,c128]) ).
cnf(c203571,plain,
( ~ environment(skolem0001)
| ~ in_environment(skolem0001,skolem0002)
| greater(zero,growth_rate(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c203570,c92]) ).
cnf(c203572,plain,
( ~ environment(skolem0001)
| greater(zero,growth_rate(efficient_producers,skolem0002)) ),
inference(resolution,[status(thm)],[c203571,c87]) ).
cnf(c203573,plain,
greater(zero,growth_rate(efficient_producers,skolem0002)),
inference(resolution,[status(thm)],[c203572,c16]) ).
cnf(c203574,plain,
~ greater(growth_rate(first_movers,skolem0002),zero),
inference(resolution,[status(thm)],[c203573,c20]) ).
cnf(c203611,plain,
$false,
inference(resolution,[status(thm)],[c203574,c202704]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT025+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.38 % Computer : n020.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 7 12:10:58 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.45 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.45 (re.compile("\."), Token.FullStop),
% 0.12/0.45 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.45 (re.compile("\("), Token.OpenPar),
% 0.12/0.45 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.45 (re.compile("\)"), Token.ClosePar),
% 0.12/0.45 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.45 (re.compile("\["), Token.OpenSquare),
% 0.12/0.45 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.45 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.45 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.45 (re.compile("~\|"), Token.Nor),
% 0.12/0.45 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.45 (re.compile("\|"), Token.Or),
% 0.12/0.45 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.45 (re.compile("\?"), Token.Existential),
% 0.12/0.45 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.45 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.45 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.45 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.23/0.52 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.52 """
% 0.23/0.52 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.52 """
% 0.33/0.62 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.62 """
% 221.05/221.38 % Version: 1.5
% 221.05/221.38 % SZS status Theorem
% 221.05/221.38 % SZS output start CNFRefutation
% See solution above
% 221.05/221.38
% 221.05/221.38 % Initial clauses : 41
% 221.05/221.38 % Processed clauses : 3173
% 221.05/221.38 % Factors computed : 5
% 221.05/221.38 % Resolvents computed: 203544
% 221.05/221.38 % Tautologies deleted: 6
% 221.05/221.38 % Forward subsumed : 1472
% 221.05/221.38 % Backward subsumed : 2155
% 221.05/221.38 % -------- CPU Time ---------
% 221.05/221.38 % User time : 219.767 s
% 221.05/221.38 % System time : 1.212 s
% 221.05/221.38 % Total time : 220.979 s
%------------------------------------------------------------------------------