%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : MGT030-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:11:24 AM UTC 2026
% Result : Unsatisfiable 2.20s 0.66s
% Output : CNFRefutation 2.20s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named prove_l12_12ERROR: Could not build tree for root finalERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(11,plain,
environment(sk4),
inference(cnf,[status(esa)],[prove_l12_12]) ).
cnf(l0,plain,
environment(sk4),
inference(instantiation,[status(thm)],[11]) ).
cnf(0,plain,
( ~ in_environment(X0,X1)
| ~ environment(X0)
| in_environment(X0,sk2(X0))
| subpopulations(first_movers,efficient_producers,X0,sk1(X1,X0)) ),
inference(cnf,[status(esa)],[mp_earliest_time_growth_rate_exceeds_1]) ).
cnf(l1,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ environment(sk4)
| in_environment(sk4,sk2(sk4))
| subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(10,plain,
( ~ stable(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ greater_or_equal(X1,sk3(X0))
| ~ environment(X0)
| greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1)) ),
inference(cnf,[status(esa)],[l1_11]) ).
cnf(l7,plain,
( ~ stable(sk4)
| ~ subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))
| ~ greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| ~ environment(sk4)
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(9,plain,
( ~ stable(X0)
| ~ environment(X0)
| in_environment(X0,sk3(X0)) ),
inference(cnf,[status(esa)],[l1_10]) ).
cnf(l2,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(12,plain,
stable(sk4),
inference(cnf,[status(esa)],[prove_l12_13]) ).
cnf(l13,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l68,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(8,plain,
( ~ in_environment(X0,X1)
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| ~ greater(X2,sk2(X0))
| ~ greater(growth_rate(efficient_producers,sk1(X1,X0)),growth_rate(first_movers,sk1(X1,X0)))
| ~ environment(X0)
| greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)) ),
inference(cnf,[status(esa)],[mp_earliest_time_growth_rate_exceeds_9]) ).
cnf(l116,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| ~ greater(sk5(sk2(sk4)),sk2(sk4))
| ~ greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))
| ~ environment(sk4)
| greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4)))) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(1,plain,
( ~ in_environment(X0,X1)
| ~ environment(X0)
| in_environment(X0,sk2(X0))
| greater_or_equal(sk1(X1,X0),X1) ),
inference(cnf,[status(esa)],[mp_earliest_time_growth_rate_exceeds_2]) ).
cnf(l105,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ environment(sk4)
| in_environment(sk4,sk2(sk4))
| greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l131,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(14,plain,
( ~ in_environment(sk4,X0)
| greater(sk5(X0),X0)
| greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0)) ),
inference(cnf,[status(esa)],[prove_l12_15]) ).
cnf(l119,plain,
( ~ in_environment(sk4,sk2(sk4))
| greater(sk5(sk2(sk4)),sk2(sk4))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l453,plain,
( ~ in_environment(sk4,sk2(sk4))
| greater(sk5(sk2(sk4)),sk2(sk4))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l454,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(4,plain,
( ~ in_environment(X0,X1)
| ~ greater(growth_rate(efficient_producers,sk2(X0)),growth_rate(first_movers,sk2(X0)))
| ~ environment(X0)
| greater_or_equal(sk1(X1,X0),X1) ),
inference(cnf,[status(esa)],[mp_earliest_time_growth_rate_exceeds_5]) ).
cnf(l120,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| ~ environment(sk4)
| greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4)) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l455,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(15,plain,
( ~ in_environment(sk4,X0)
| ~ greater(growth_rate(efficient_producers,sk5(X0)),growth_rate(first_movers,sk5(X0)))
| greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0)) ),
inference(cnf,[status(esa)],[prove_l12_16]) ).
cnf(l452,plain,
( ~ in_environment(sk4,sk2(sk4))
| ~ greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4))))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l141,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(6,plain,
( ~ in_environment(X0,X1)
| ~ greater(growth_rate(efficient_producers,sk1(X1,X0)),growth_rate(first_movers,sk1(X1,X0)))
| ~ environment(X0)
| in_environment(X0,sk2(X0)) ),
inference(cnf,[status(esa)],[mp_earliest_time_growth_rate_exceeds_7]) ).
cnf(l457,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))
| ~ environment(sk4)
| in_environment(sk4,sk2(sk4)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(7,plain,
( ~ in_environment(X0,X1)
| ~ greater(growth_rate(efficient_producers,sk2(X0)),growth_rate(first_movers,sk2(X0)))
| ~ greater(growth_rate(efficient_producers,sk1(X1,X0)),growth_rate(first_movers,sk1(X1,X0)))
| ~ environment(X0) ),
inference(cnf,[status(esa)],[mp_earliest_time_growth_rate_exceeds_8]) ).
cnf(l464,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| ~ greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))
| ~ environment(sk4) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l301,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(5,plain,
( ~ in_environment(X0,X1)
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| ~ greater(X2,sk2(X0))
| ~ environment(X0)
| greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))
| greater_or_equal(sk1(X1,X0),X1) ),
inference(cnf,[status(esa)],[mp_earliest_time_growth_rate_exceeds_6]) ).
cnf(l188,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| ~ greater(sk5(sk2(sk4)),sk2(sk4))
| ~ environment(sk4)
| greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4))))
| greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l472,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(13,plain,
( ~ in_environment(sk4,X0)
| subpopulations(first_movers,efficient_producers,sk4,sk5(X0))
| greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0)) ),
inference(cnf,[status(esa)],[prove_l12_14]) ).
cnf(l483,plain,
( ~ in_environment(sk4,sk2(sk4))
| subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l148,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l484,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| ~ environment(sk4)
| greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4)) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l469,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l488,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l197,plain,
( ~ in_environment(sk4,sk2(sk4))
| ~ greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4))))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l225,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l458,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))
| ~ environment(sk4)
| in_environment(sk4,sk2(sk4)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l456,plain,
( ~ in_environment(sk4,sk2(sk4))
| subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l460,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l459,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))
| ~ environment(sk4)
| in_environment(sk4,sk2(sk4)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l205,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| ~ environment(sk4)
| greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4)) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l537,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l3,plain,
( ~ in_environment(sk4,sk2(sk4))
| ~ greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4))))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l505,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l342,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| ~ greater(sk5(sk2(sk4)),sk2(sk4))
| ~ environment(sk4)
| greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4))))
| greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l471,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| ~ greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))
| ~ environment(sk4) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l479,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l538,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l380,plain,
( ~ in_environment(sk4,sk2(sk4))
| greater(sk5(sk2(sk4)),sk2(sk4))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l461,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l340,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(2,plain,
( ~ in_environment(X0,X1)
| ~ greater(growth_rate(efficient_producers,sk2(X0)),growth_rate(first_movers,sk2(X0)))
| ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,sk1(X1,X0)) ),
inference(cnf,[status(esa)],[mp_earliest_time_growth_rate_exceeds_3]) ).
cnf(l422,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| ~ environment(sk4)
| subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4)) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l232,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l559,plain,
( ~ stable(sk4)
| ~ subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))
| ~ greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| ~ environment(sk4)
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l5,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| ~ greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))
| ~ environment(sk4) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l465,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l565,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| ~ greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))
| ~ environment(sk4) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l574,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l566,plain,
( ~ in_environment(sk4,sk2(sk4))
| greater(sk5(sk2(sk4)),sk2(sk4))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(3,plain,
( ~ in_environment(X0,X1)
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| ~ greater(X2,sk2(X0))
| ~ environment(X0)
| subpopulations(first_movers,efficient_producers,X0,sk1(X1,X0))
| greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)) ),
inference(cnf,[status(esa)],[mp_earliest_time_growth_rate_exceeds_4]) ).
cnf(l560,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| ~ greater(sk5(sk2(sk4)),sk2(sk4))
| ~ 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(instantiation,[status(thm)],[3]) ).
cnf(l561,plain,
( ~ stable(sk4)
| ~ subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))
| ~ greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| ~ environment(sk4)
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l563,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l36,plain,
( ~ stable(sk4)
| ~ subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))
| ~ greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| ~ environment(sk4)
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l568,plain,
( ~ in_environment(sk4,sk2(sk4))
| subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l81,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| ~ environment(sk4)
| subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4)) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l17,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l462,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| ~ greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))
| ~ environment(sk4) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l86,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l575,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l573,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l592,plain,
( ~ in_environment(sk4,sk2(sk4))
| greater(sk5(sk2(sk4)),sk2(sk4))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l343,plain,
( ~ in_environment(sk4,sk2(sk4))
| subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l562,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l600,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| ~ environment(sk4)
| subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4)) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l39,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l491,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l493,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l466,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l588,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l608,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l564,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| ~ environment(sk4)
| greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4)) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l100,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| ~ environment(sk4)
| greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4)) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l58,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l579,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| ~ greater(sk5(sk2(sk4)),sk2(sk4))
| ~ greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))
| ~ environment(sk4)
| greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4)))) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l576,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| ~ greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))
| ~ environment(sk4) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l577,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l379,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l139,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l609,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l585,plain,
( ~ in_environment(sk4,sk2(sk4))
| subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))
| greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l578,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l387,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l98,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l230,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l622,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l580,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l467,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l623,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l598,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l587,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l594,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l601,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l567,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| ~ environment(sk4)
| greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4)) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l572,plain,
( ~ stable(sk4)
| ~ subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))
| ~ greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))
| ~ environment(sk4)
| greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l607,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l604,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| ~ greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))
| ~ environment(sk4) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l646,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l589,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| ~ environment(sk4)
| subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4)) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l620,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l652,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l617,plain,
( ~ in_environment(sk4,sk3(sk4))
| ~ greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))
| ~ environment(sk4)
| subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4)) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l621,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l628,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l618,plain,
( ~ stable(sk4)
| ~ environment(sk4)
| in_environment(sk4,sk3(sk4)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l627,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(l629,plain,
stable(sk4),
inference(instantiation,[status(thm)],[12]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l7,l2,l13,l68,l116,l105,l131,l119,l453,l454,l120,l455,l452,l141,l457,l464,l301,l188,l472,l483,l148,l484,l469,l488,l197,l225,l458,l456,l460,l459,l205,l537,l3,l505,l342,l471,l479,l538,l380,l461,l340,l422,l232,l559,l5,l465,l565,l574,l566,l560,l561,l563,l36,l568,l81,l17,l462,l86,l575,l573,l592,l343,l562,l600,l39,l491,l493,l466,l588,l608,l564,l100,l58,l579,l576,l577,l379,l139,l609,l585,l578,l387,l98,l230,l622,l580,l467,l623,l598,l587,l594,l601,l567,l572,l607,l604,l646,l589,l620,l652,l617,l621,l628,l618,l627,l629]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT030-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n026.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 7 12:22:12 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.12/0.36 % launching worker at depth: 1
% 0.12/0.36 % launching worker at depth: 5
% 0.12/0.36 % launching worker at depth: 3
% 0.12/0.36 % launching worker at depth: 8
% 0.12/0.36 % launching worker at depth: 2
% 0.12/0.36 % launching worker at depth: 6
% 0.12/0.36 % launching worker at depth: 4
% 0.12/0.36 % launching worker at depth: 7
% 0.12/0.36 % launching worker at depth: 9
% 0.12/0.36 % launching worker at depth: 10
% 0.12/0.37 % launching worker at depth: 11
% 0.12/0.38 % launching worker at depth: 12
% 0.12/0.46 % launching worker at depth: 13
% 2.20/0.66 % SZS status Theorem for theBenchmark
% 2.20/0.66 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------