%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT030-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:18:43 AM UTC 2026
% Result : Unsatisfiable 0.23s 0.54s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 16
% Syntax : Number of clauses : 94 ( 13 unt; 52 nHn; 94 RR)
% Number of literals : 277 ( 0 equ; 131 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-4 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% Number of variables : 38 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_l12_12,negated_conjecture,
environment(sk4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_l12_12) ).
cnf(prove_l12_13,negated_conjecture,
stable(sk4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_l12_13) ).
cnf(l1_10,plain,
( ~ environment(X2)
| ~ stable(X2)
| in_environment(X2,sk3(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1_10) ).
cnf(c0,plain,
( ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(resolution,[status(thm)],[l1_10,prove_l12_13]) ).
cnf(c1,plain,
in_environment(sk4,sk3(sk4)),
inference(resolution,[status(thm)],[c0,prove_l12_12]) ).
cnf(mp_earliest_time_growth_rate_exceeds_8,axiom,
( ~ environment(X24)
| ~ in_environment(X24,X25)
| ~ greater(growth_rate(efficient_producers,sk1(X25,X24)),growth_rate(first_movers,sk1(X25,X24)))
| ~ greater(growth_rate(efficient_producers,sk2(X24)),growth_rate(first_movers,sk2(X24))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds_8) ).
cnf(mp_earliest_time_growth_rate_exceeds_5,axiom,
( ~ environment(X11)
| ~ in_environment(X11,X12)
| greater_or_equal(sk1(X12,X11),X12)
| ~ greater(growth_rate(efficient_producers,sk2(X11)),growth_rate(first_movers,sk2(X11))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds_5) ).
cnf(mp_earliest_time_growth_rate_exceeds_7,axiom,
( ~ environment(X13)
| ~ in_environment(X13,X14)
| ~ greater(growth_rate(efficient_producers,sk1(X14,X13)),growth_rate(first_movers,sk1(X14,X13)))
| in_environment(X13,sk2(X13)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds_7) ).
cnf(mp_earliest_time_growth_rate_exceeds_2,axiom,
( ~ environment(X5)
| ~ in_environment(X5,X6)
| greater_or_equal(sk1(X6,X5),X6)
| in_environment(X5,sk2(X5)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds_2) ).
cnf(c3,plain,
( ~ environment(sk4)
| greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| in_environment(sk4,sk2(sk4)) ),
inference(resolution,[status(thm)],[mp_earliest_time_growth_rate_exceeds_2,c1]) ).
cnf(c5,plain,
( greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| in_environment(sk4,sk2(sk4)) ),
inference(resolution,[status(thm)],[c3,prove_l12_12]) ).
cnf(mp_earliest_time_growth_rate_exceeds_1,axiom,
( ~ environment(X3)
| ~ in_environment(X3,X4)
| subpopulations(first_movers,efficient_producers,X3,sk1(X4,X3))
| in_environment(X3,sk2(X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds_1) ).
cnf(c2,plain,
( ~ environment(sk4)
| subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))
| in_environment(sk4,sk2(sk4)) ),
inference(resolution,[status(thm)],[mp_earliest_time_growth_rate_exceeds_1,c1]) ).
cnf(c11,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))
| in_environment(sk4,sk2(sk4)) ),
inference(resolution,[status(thm)],[c2,prove_l12_12]) ).
cnf(l1_11,plain,
( ~ environment(X18)
| ~ stable(X18)
| ~ subpopulations(first_movers,efficient_producers,X18,X19)
| ~ greater_or_equal(X19,sk3(X18))
| greater(growth_rate(efficient_producers,X19),growth_rate(first_movers,X19)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1_11) ).
cnf(c17,plain,
( ~ environment(sk4)
| ~ stable(sk4)
| ~ greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))
| in_environment(sk4,sk2(sk4)) ),
inference(resolution,[status(thm)],[l1_11,c11]) ).
cnf(c63,plain,
( ~ environment(sk4)
| ~ stable(sk4)
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))
| in_environment(sk4,sk2(sk4)) ),
inference(resolution,[status(thm)],[c17,c5]) ).
cnf(c66,plain,
( ~ environment(sk4)
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))
| in_environment(sk4,sk2(sk4)) ),
inference(resolution,[status(thm)],[c63,prove_l12_13]) ).
cnf(c67,plain,
( greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))
| in_environment(sk4,sk2(sk4)) ),
inference(resolution,[status(thm)],[c66,prove_l12_12]) ).
cnf(c68,plain,
( in_environment(sk4,sk2(sk4))
| ~ environment(sk4)
| ~ in_environment(sk4,sk3(sk4)) ),
inference(resolution,[status(thm)],[c67,mp_earliest_time_growth_rate_exceeds_7]) ).
cnf(c77,plain,
( in_environment(sk4,sk2(sk4))
| ~ environment(sk4) ),
inference(resolution,[status(thm)],[c68,c1]) ).
cnf(c78,plain,
in_environment(sk4,sk2(sk4)),
inference(resolution,[status(thm)],[c77,prove_l12_12]) ).
cnf(prove_l12_16,negated_conjecture,
( ~ in_environment(sk4,X20)
| greater(growth_rate(efficient_producers,X20),growth_rate(first_movers,X20))
| ~ greater(growth_rate(efficient_producers,sk5(X20)),growth_rate(first_movers,sk5(X20))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_l12_16) ).
cnf(prove_l12_15,negated_conjecture,
( ~ in_environment(sk4,X7)
| greater(growth_rate(efficient_producers,X7),growth_rate(first_movers,X7))
| greater(sk5(X7),X7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_l12_15) ).
cnf(c84,plain,
( greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| greater(sk5(sk2(sk4)),sk2(sk4)) ),
inference(resolution,[status(thm)],[c78,prove_l12_15]) ).
cnf(c8,plain,
( greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| greater(sk5(sk2(sk4)),sk2(sk4)) ),
inference(resolution,[status(thm)],[c5,prove_l12_15]) ).
cnf(c23,plain,
( greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| greater(sk5(sk2(sk4)),sk2(sk4))
| ~ environment(sk4)
| ~ in_environment(sk4,X26)
| greater_or_equal(sk1(X26,sk4),X26) ),
inference(resolution,[status(thm)],[c8,mp_earliest_time_growth_rate_exceeds_5]) ).
cnf(c24,plain,
( greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| greater(sk5(sk2(sk4)),sk2(sk4))
| ~ environment(sk4) ),
inference(resolution,[status(thm)],[c23,c1]) ).
cnf(c27,plain,
( greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| greater(sk5(sk2(sk4)),sk2(sk4)) ),
inference(resolution,[status(thm)],[c24,prove_l12_12]) ).
cnf(mp_earliest_time_growth_rate_exceeds_3,axiom,
( ~ environment(X9)
| ~ in_environment(X9,X10)
| subpopulations(first_movers,efficient_producers,X9,sk1(X10,X9))
| ~ greater(growth_rate(efficient_producers,sk2(X9)),growth_rate(first_movers,sk2(X9))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds_3) ).
cnf(c85,plain,
( greater(sk5(sk2(sk4)),sk2(sk4))
| ~ environment(sk4)
| ~ in_environment(sk4,X39)
| subpopulations(first_movers,efficient_producers,sk4,sk1(X39,sk4)) ),
inference(resolution,[status(thm)],[c84,mp_earliest_time_growth_rate_exceeds_3]) ).
cnf(c101,plain,
( greater(sk5(sk2(sk4)),sk2(sk4))
| ~ environment(sk4)
| subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4)) ),
inference(resolution,[status(thm)],[c85,c1]) ).
cnf(c103,plain,
( greater(sk5(sk2(sk4)),sk2(sk4))
| subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4)) ),
inference(resolution,[status(thm)],[c101,prove_l12_12]) ).
cnf(c105,plain,
( greater(sk5(sk2(sk4)),sk2(sk4))
| ~ environment(sk4)
| ~ stable(sk4)
| ~ greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4))) ),
inference(resolution,[status(thm)],[c103,l1_11]) ).
cnf(c137,plain,
( greater(sk5(sk2(sk4)),sk2(sk4))
| ~ environment(sk4)
| ~ stable(sk4)
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4))) ),
inference(resolution,[status(thm)],[c105,c27]) ).
cnf(c139,plain,
( greater(sk5(sk2(sk4)),sk2(sk4))
| ~ environment(sk4)
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4))) ),
inference(resolution,[status(thm)],[c137,prove_l12_13]) ).
cnf(c140,plain,
( greater(sk5(sk2(sk4)),sk2(sk4))
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4))) ),
inference(resolution,[status(thm)],[c139,prove_l12_12]) ).
cnf(c144,plain,
( greater(sk5(sk2(sk4)),sk2(sk4))
| ~ environment(sk4)
| ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(resolution,[status(thm)],[c140,mp_earliest_time_growth_rate_exceeds_8]) ).
cnf(c147,plain,
( greater(sk5(sk2(sk4)),sk2(sk4))
| ~ environment(sk4)
| ~ in_environment(sk4,sk3(sk4)) ),
inference(resolution,[status(thm)],[c144,c84]) ).
cnf(c148,plain,
( greater(sk5(sk2(sk4)),sk2(sk4))
| ~ environment(sk4) ),
inference(resolution,[status(thm)],[c147,c1]) ).
cnf(c149,plain,
greater(sk5(sk2(sk4)),sk2(sk4)),
inference(resolution,[status(thm)],[c148,prove_l12_12]) ).
cnf(mp_earliest_time_growth_rate_exceeds_6,axiom,
( ~ environment(X21)
| ~ in_environment(X21,X22)
| greater_or_equal(sk1(X22,X21),X22)
| ~ subpopulations(first_movers,efficient_producers,X21,X23)
| ~ greater(X23,sk2(X21))
| greater(growth_rate(efficient_producers,X23),growth_rate(first_movers,X23)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds_6) ).
cnf(prove_l12_14,negated_conjecture,
( ~ in_environment(sk4,X8)
| greater(growth_rate(efficient_producers,X8),growth_rate(first_movers,X8))
| subpopulations(first_movers,efficient_producers,sk4,sk5(X8)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_l12_14) ).
cnf(c83,plain,
( greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4))) ),
inference(resolution,[status(thm)],[c78,prove_l12_14]) ).
cnf(c10,plain,
( greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4)) ),
inference(resolution,[status(thm)],[prove_l12_14,c5]) ).
cnf(c29,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| ~ environment(sk4)
| ~ in_environment(sk4,X30)
| greater_or_equal(sk1(X30,sk4),X30) ),
inference(resolution,[status(thm)],[c10,mp_earliest_time_growth_rate_exceeds_5]) ).
cnf(c33,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| ~ environment(sk4) ),
inference(resolution,[status(thm)],[c29,c1]) ).
cnf(c44,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4)) ),
inference(resolution,[status(thm)],[c33,prove_l12_12]) ).
cnf(c90,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| ~ environment(sk4)
| ~ in_environment(sk4,X41)
| subpopulations(first_movers,efficient_producers,sk4,sk1(X41,sk4)) ),
inference(resolution,[status(thm)],[c83,mp_earliest_time_growth_rate_exceeds_3]) ).
cnf(c111,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| ~ environment(sk4)
| subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4)) ),
inference(resolution,[status(thm)],[c90,c1]) ).
cnf(c113,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4)) ),
inference(resolution,[status(thm)],[c111,prove_l12_12]) ).
cnf(c118,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| ~ environment(sk4)
| ~ stable(sk4)
| ~ greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4))) ),
inference(resolution,[status(thm)],[c113,l1_11]) ).
cnf(c152,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| ~ environment(sk4)
| ~ stable(sk4)
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4))) ),
inference(resolution,[status(thm)],[c118,c44]) ).
cnf(c153,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| ~ environment(sk4)
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4))) ),
inference(resolution,[status(thm)],[c152,prove_l12_13]) ).
cnf(c154,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4))) ),
inference(resolution,[status(thm)],[c153,prove_l12_12]) ).
cnf(c159,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| ~ environment(sk4)
| ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(resolution,[status(thm)],[c154,mp_earliest_time_growth_rate_exceeds_8]) ).
cnf(c161,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| ~ environment(sk4)
| ~ in_environment(sk4,sk3(sk4)) ),
inference(resolution,[status(thm)],[c159,c83]) ).
cnf(c162,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| ~ environment(sk4) ),
inference(resolution,[status(thm)],[c161,c1]) ).
cnf(c163,plain,
subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4))),
inference(resolution,[status(thm)],[c162,prove_l12_12]) ).
cnf(c165,plain,
( ~ environment(sk4)
| ~ in_environment(sk4,X52)
| greater_or_equal(sk1(X52,sk4),X52)
| ~ greater(sk5(sk2(sk4)),sk2(sk4))
| greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4)))) ),
inference(resolution,[status(thm)],[c163,mp_earliest_time_growth_rate_exceeds_6]) ).
cnf(c168,plain,
( ~ environment(sk4)
| ~ in_environment(sk4,X53)
| greater_or_equal(sk1(X53,sk4),X53)
| greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4)))) ),
inference(resolution,[status(thm)],[c165,c149]) ).
cnf(c169,plain,
( ~ environment(sk4)
| greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4)))) ),
inference(resolution,[status(thm)],[c168,c1]) ).
cnf(c171,plain,
( greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4)))) ),
inference(resolution,[status(thm)],[c169,prove_l12_12]) ).
cnf(c172,plain,
( greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| ~ in_environment(sk4,sk2(sk4))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(resolution,[status(thm)],[c171,prove_l12_16]) ).
cnf(c175,plain,
( greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(resolution,[status(thm)],[c172,c78]) ).
cnf(c177,plain,
( greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| ~ environment(sk4)
| ~ in_environment(sk4,X55)
| greater_or_equal(sk1(X55,sk4),X55) ),
inference(resolution,[status(thm)],[c175,mp_earliest_time_growth_rate_exceeds_5]) ).
cnf(c179,plain,
( greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| ~ environment(sk4) ),
inference(resolution,[status(thm)],[c177,c1]) ).
cnf(c181,plain,
greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4)),
inference(resolution,[status(thm)],[c179,prove_l12_12]) ).
cnf(mp_earliest_time_growth_rate_exceeds_4,axiom,
( ~ environment(X15)
| ~ in_environment(X15,X16)
| subpopulations(first_movers,efficient_producers,X15,sk1(X16,X15))
| ~ subpopulations(first_movers,efficient_producers,X15,X17)
| ~ greater(X17,sk2(X15))
| greater(growth_rate(efficient_producers,X17),growth_rate(first_movers,X17)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds_4) ).
cnf(c167,plain,
( ~ environment(sk4)
| ~ in_environment(sk4,X62)
| subpopulations(first_movers,efficient_producers,sk4,sk1(X62,sk4))
| ~ greater(sk5(sk2(sk4)),sk2(sk4))
| greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4)))) ),
inference(resolution,[status(thm)],[c163,mp_earliest_time_growth_rate_exceeds_4]) ).
cnf(c188,plain,
( ~ environment(sk4)
| ~ in_environment(sk4,X63)
| subpopulations(first_movers,efficient_producers,sk4,sk1(X63,sk4))
| greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4)))) ),
inference(resolution,[status(thm)],[c167,c149]) ).
cnf(c189,plain,
( ~ environment(sk4)
| subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))
| greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4)))) ),
inference(resolution,[status(thm)],[c188,c1]) ).
cnf(c191,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))
| greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4)))) ),
inference(resolution,[status(thm)],[c189,prove_l12_12]) ).
cnf(c195,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))
| ~ in_environment(sk4,sk2(sk4))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(resolution,[status(thm)],[c191,prove_l12_16]) ).
cnf(c201,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(resolution,[status(thm)],[c195,c78]) ).
cnf(c205,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))
| ~ environment(sk4)
| ~ in_environment(sk4,X66)
| subpopulations(first_movers,efficient_producers,sk4,sk1(X66,sk4)) ),
inference(resolution,[status(thm)],[c201,mp_earliest_time_growth_rate_exceeds_3]) ).
cnf(c209,plain,
( subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))
| ~ environment(sk4) ),
inference(resolution,[status(thm)],[c205,c1]) ).
cnf(c211,plain,
subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4)),
inference(resolution,[status(thm)],[c209,prove_l12_12]) ).
cnf(c213,plain,
( ~ environment(sk4)
| ~ stable(sk4)
| ~ greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4))) ),
inference(resolution,[status(thm)],[c211,l1_11]) ).
cnf(c229,plain,
( ~ environment(sk4)
| ~ stable(sk4)
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4))) ),
inference(resolution,[status(thm)],[c213,c181]) ).
cnf(c230,plain,
( ~ environment(sk4)
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4))) ),
inference(resolution,[status(thm)],[c229,prove_l12_13]) ).
cnf(c231,plain,
greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4))),
inference(resolution,[status(thm)],[c230,prove_l12_12]) ).
cnf(c233,plain,
( ~ environment(sk4)
| ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(resolution,[status(thm)],[c231,mp_earliest_time_growth_rate_exceeds_8]) ).
cnf(mp_earliest_time_growth_rate_exceeds_9,axiom,
( ~ environment(X27)
| ~ in_environment(X27,X28)
| ~ greater(growth_rate(efficient_producers,sk1(X28,X27)),growth_rate(first_movers,sk1(X28,X27)))
| ~ subpopulations(first_movers,efficient_producers,X27,X29)
| ~ greater(X29,sk2(X27))
| greater(growth_rate(efficient_producers,X29),growth_rate(first_movers,X29)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds_9) ).
cnf(c234,plain,
( ~ environment(sk4)
| ~ in_environment(sk4,sk3(sk4))
| ~ subpopulations(first_movers,efficient_producers,sk4,X72)
| ~ greater(X72,sk2(sk4))
| greater(growth_rate(efficient_producers,X72),growth_rate(first_movers,X72)) ),
inference(resolution,[status(thm)],[c231,mp_earliest_time_growth_rate_exceeds_9]) ).
cnf(c238,plain,
( ~ environment(sk4)
| ~ in_environment(sk4,sk3(sk4))
| ~ greater(sk5(sk2(sk4)),sk2(sk4))
| greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4)))) ),
inference(resolution,[status(thm)],[c234,c163]) ).
cnf(c239,plain,
( ~ environment(sk4)
| ~ in_environment(sk4,sk3(sk4))
| greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4)))) ),
inference(resolution,[status(thm)],[c238,c149]) ).
cnf(c240,plain,
( ~ environment(sk4)
| greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4)))) ),
inference(resolution,[status(thm)],[c239,c1]) ).
cnf(c241,plain,
greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4)))),
inference(resolution,[status(thm)],[c240,prove_l12_12]) ).
cnf(c242,plain,
( ~ in_environment(sk4,sk2(sk4))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(resolution,[status(thm)],[c241,prove_l12_16]) ).
cnf(c243,plain,
greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))),
inference(resolution,[status(thm)],[c242,c78]) ).
cnf(c245,plain,
( ~ environment(sk4)
| ~ in_environment(sk4,sk3(sk4)) ),
inference(resolution,[status(thm)],[c243,c233]) ).
cnf(c247,plain,
~ environment(sk4),
inference(resolution,[status(thm)],[c245,c1]) ).
cnf(c248,plain,
$false,
inference(resolution,[status(thm)],[c247,prove_l12_12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT030-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.36 % Computer : n017.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 7 12:14:24 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.39 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.14/0.39 (re.compile("\."), Token.FullStop),
% 0.14/0.39 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.14/0.39 (re.compile("\("), Token.OpenPar),
% 0.14/0.39 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.14/0.39 (re.compile("\)"), Token.ClosePar),
% 0.14/0.39 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.14/0.39 (re.compile("\["), Token.OpenSquare),
% 0.14/0.39 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.14/0.39 (re.compile("\]"), Token.CloseSquare),
% 0.14/0.39 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.14/0.39 (re.compile("~\|"), Token.Nor),
% 0.14/0.39 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.14/0.39 (re.compile("\|"), Token.Or),
% 0.14/0.39 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.14/0.39 (re.compile("\?"), Token.Existential),
% 0.14/0.39 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.14/0.39 (re.compile("\s+"), Token.WhiteSpace),
% 0.14/0.39 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.14/0.39 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.14/0.42 """
% 0.14/0.42 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.14/0.42 """
% 0.23/0.46 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.46 """
% 0.23/0.54 % Version: 1.5
% 0.23/0.54 % SZS status Unsatisfiable
% 0.23/0.54 % SZS output start CNFRefutation
% See solution above
% 0.23/0.54
% 0.23/0.54 % Initial clauses : 16
% 0.23/0.54 % Processed clauses : 140
% 0.23/0.54 % Factors computed : 0
% 0.23/0.54 % Resolvents computed: 249
% 0.23/0.54 % Tautologies deleted: 0
% 0.23/0.54 % Forward subsumed : 66
% 0.23/0.54 % Backward subsumed : 110
% 0.23/0.54 % -------- CPU Time ---------
% 0.23/0.54 % User time : 0.165 s
% 0.23/0.54 % System time : 0.016 s
% 0.23/0.54 % Total time : 0.181 s
%------------------------------------------------------------------------------