%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT023-2 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.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 : Unsatisfiable 1.27s 1.51s
% Output : CNFRefutation 1.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 19
% Syntax : Number of clauses : 122 ( 15 unt; 77 nHn; 121 RR)
% Number of literals : 380 ( 40 equ; 155 neg)
% Maximal clause size : 6 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-2 aty)
% Number of variables : 55 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_l5_35,negated_conjecture,
~ in_environment(sk5,critical_point(sk5)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_l5_35) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c7,axiom,
( X40 != X39
| X37 != X38
| ~ in_environment(X40,X37)
| in_environment(X39,X38) ),
theory(equality) ).
cnf(prove_l5_33,negated_conjecture,
environment(sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_l5_33) ).
cnf(prove_l5_34,negated_conjecture,
stable(sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_l5_34) ).
cnf(l1_31,plain,
( ~ environment(X16)
| ~ stable(X16)
| in_environment(X16,sk4(X16)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1_31) ).
cnf(c15,plain,
( ~ environment(sk5)
| in_environment(sk5,sk4(sk5)) ),
inference(resolution,[status(thm)],[l1_31,prove_l5_34]) ).
cnf(c21,plain,
in_environment(sk5,sk4(sk5)),
inference(resolution,[status(thm)],[c15,prove_l5_33]) ).
cnf(mp_earliest_time_growth_rate_exceeds_25,axiom,
( ~ environment(X75)
| ~ in_environment(X75,X76)
| ~ greater(growth_rate(efficient_producers,sk1(X76,X75)),growth_rate(first_movers,sk1(X76,X75)))
| in_environment(X75,sk2(X75)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds_25) ).
cnf(mp_earliest_time_growth_rate_exceeds_20,axiom,
( ~ environment(X14)
| ~ in_environment(X14,X15)
| greater_or_equal(sk1(X15,X14),X15)
| in_environment(X14,sk2(X14)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds_20) ).
cnf(c23,plain,
( ~ environment(sk5)
| greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| in_environment(sk5,sk2(sk5)) ),
inference(resolution,[status(thm)],[c21,mp_earliest_time_growth_rate_exceeds_20]) ).
cnf(c39,plain,
( greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| in_environment(sk5,sk2(sk5)) ),
inference(resolution,[status(thm)],[c23,prove_l5_33]) ).
cnf(mp_earliest_time_growth_rate_exceeds_19,axiom,
( ~ environment(X5)
| ~ in_environment(X5,X6)
| subpopulations(first_movers,efficient_producers,X5,sk1(X6,X5))
| in_environment(X5,sk2(X5)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds_19) ).
cnf(c22,plain,
( ~ environment(sk5)
| subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))
| in_environment(sk5,sk2(sk5)) ),
inference(resolution,[status(thm)],[c21,mp_earliest_time_growth_rate_exceeds_19]) ).
cnf(c44,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))
| in_environment(sk5,sk2(sk5)) ),
inference(resolution,[status(thm)],[c22,prove_l5_33]) ).
cnf(l1_32,plain,
( ~ environment(X120)
| ~ stable(X120)
| ~ subpopulations(first_movers,efficient_producers,X120,X121)
| ~ greater_or_equal(X121,sk4(X120))
| greater(growth_rate(efficient_producers,X121),growth_rate(first_movers,X121)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1_32) ).
cnf(c61,plain,
( ~ environment(sk5)
| ~ stable(sk5)
| ~ greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5)))
| in_environment(sk5,sk2(sk5)) ),
inference(resolution,[status(thm)],[l1_32,c44]) ).
cnf(c191,plain,
( ~ environment(sk5)
| ~ stable(sk5)
| greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5)))
| in_environment(sk5,sk2(sk5)) ),
inference(resolution,[status(thm)],[c61,c39]) ).
cnf(c192,plain,
( ~ environment(sk5)
| greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5)))
| in_environment(sk5,sk2(sk5)) ),
inference(resolution,[status(thm)],[c191,prove_l5_34]) ).
cnf(c193,plain,
( greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5)))
| in_environment(sk5,sk2(sk5)) ),
inference(resolution,[status(thm)],[c192,prove_l5_33]) ).
cnf(c194,plain,
( in_environment(sk5,sk2(sk5))
| ~ environment(sk5)
| ~ in_environment(sk5,sk4(sk5)) ),
inference(resolution,[status(thm)],[c193,mp_earliest_time_growth_rate_exceeds_25]) ).
cnf(c203,plain,
( in_environment(sk5,sk2(sk5))
| ~ environment(sk5) ),
inference(resolution,[status(thm)],[c194,c21]) ).
cnf(c204,plain,
in_environment(sk5,sk2(sk5)),
inference(resolution,[status(thm)],[c203,prove_l5_33]) ).
cnf(c206,plain,
( sk5 != X153
| sk2(sk5) != X152
| in_environment(X153,X152) ),
inference(resolution,[status(thm)],[c204,c7]) ).
cnf(mp_earliest_time_growth_rate_exceeds_26,axiom,
( ~ environment(X89)
| ~ in_environment(X89,X90)
| ~ greater(growth_rate(efficient_producers,sk1(X90,X89)),growth_rate(first_movers,sk1(X90,X89)))
| ~ greater(growth_rate(efficient_producers,sk2(X89)),growth_rate(first_movers,sk2(X89))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds_26) ).
cnf(mp_earliest_time_growth_rate_exceeds_23,axiom,
( ~ environment(X49)
| ~ in_environment(X49,X50)
| greater_or_equal(sk1(X50,X49),X50)
| ~ greater(growth_rate(efficient_producers,sk2(X49)),growth_rate(first_movers,sk2(X49))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds_23) ).
cnf(d1_30,plain,
( ~ environment(X118)
| greater(growth_rate(efficient_producers,X119),growth_rate(first_movers,X119))
| ~ in_environment(X118,X119)
| ~ greater(growth_rate(efficient_producers,sk3(X119,X118)),growth_rate(first_movers,sk3(X119,X118)))
| X119 = critical_point(X118) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_30) ).
cnf(d1_29,plain,
( ~ environment(X116)
| greater(growth_rate(efficient_producers,X117),growth_rate(first_movers,X117))
| ~ in_environment(X116,X117)
| greater(sk3(X117,X116),X117)
| X117 = critical_point(X116) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_29) ).
cnf(c208,plain,
( ~ environment(sk5)
| greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| greater(sk3(sk2(sk5),sk5),sk2(sk5))
| sk2(sk5) = critical_point(sk5) ),
inference(resolution,[status(thm)],[c204,d1_29]) ).
cnf(c212,plain,
( greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| greater(sk3(sk2(sk5),sk5),sk2(sk5))
| sk2(sk5) = critical_point(sk5) ),
inference(resolution,[status(thm)],[c208,prove_l5_33]) ).
cnf(c218,plain,
( greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| greater(sk3(sk2(sk5),sk5),sk2(sk5))
| sk5 != X196
| in_environment(X196,critical_point(sk5)) ),
inference(resolution,[status(thm)],[c212,c206]) ).
cnf(c373,plain,
( greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| greater(sk3(sk2(sk5),sk5),sk2(sk5))
| in_environment(sk5,critical_point(sk5)) ),
inference(resolution,[status(thm)],[c218,reflexivity]) ).
cnf(c381,plain,
( greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| greater(sk3(sk2(sk5),sk5),sk2(sk5)) ),
inference(resolution,[status(thm)],[c373,prove_l5_35]) ).
cnf(c213,plain,
( greater(sk3(sk2(sk5),sk5),sk2(sk5))
| sk2(sk5) = critical_point(sk5)
| ~ environment(sk5)
| ~ in_environment(sk5,X163)
| greater_or_equal(sk1(X163,sk5),X163) ),
inference(resolution,[status(thm)],[c212,mp_earliest_time_growth_rate_exceeds_23]) ).
cnf(c235,plain,
( greater(sk3(sk2(sk5),sk5),sk2(sk5))
| sk2(sk5) = critical_point(sk5)
| ~ environment(sk5)
| greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5)) ),
inference(resolution,[status(thm)],[c213,c21]) ).
cnf(c315,plain,
( greater(sk3(sk2(sk5),sk5),sk2(sk5))
| sk2(sk5) = critical_point(sk5)
| greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5)) ),
inference(resolution,[status(thm)],[c235,prove_l5_33]) ).
cnf(c318,plain,
( greater(sk3(sk2(sk5),sk5),sk2(sk5))
| greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| sk5 != X176
| in_environment(X176,critical_point(sk5)) ),
inference(resolution,[status(thm)],[c315,c206]) ).
cnf(c355,plain,
( greater(sk3(sk2(sk5),sk5),sk2(sk5))
| greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| in_environment(sk5,critical_point(sk5)) ),
inference(resolution,[status(thm)],[c318,reflexivity]) ).
cnf(c361,plain,
( greater(sk3(sk2(sk5),sk5),sk2(sk5))
| greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5)) ),
inference(resolution,[status(thm)],[c355,prove_l5_35]) ).
cnf(mp_earliest_time_growth_rate_exceeds_21,axiom,
( ~ environment(X25)
| ~ in_environment(X25,X26)
| subpopulations(first_movers,efficient_producers,X25,sk1(X26,X25))
| ~ greater(growth_rate(efficient_producers,sk2(X25)),growth_rate(first_movers,sk2(X25))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds_21) ).
cnf(c387,plain,
( greater(sk3(sk2(sk5),sk5),sk2(sk5))
| ~ environment(sk5)
| ~ in_environment(sk5,X199)
| subpopulations(first_movers,efficient_producers,sk5,sk1(X199,sk5)) ),
inference(resolution,[status(thm)],[c381,mp_earliest_time_growth_rate_exceeds_21]) ).
cnf(c393,plain,
( greater(sk3(sk2(sk5),sk5),sk2(sk5))
| ~ environment(sk5)
| subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5)) ),
inference(resolution,[status(thm)],[c387,c21]) ).
cnf(c400,plain,
( greater(sk3(sk2(sk5),sk5),sk2(sk5))
| subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5)) ),
inference(resolution,[status(thm)],[c393,prove_l5_33]) ).
cnf(c402,plain,
( greater(sk3(sk2(sk5),sk5),sk2(sk5))
| ~ environment(sk5)
| ~ stable(sk5)
| ~ greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5))) ),
inference(resolution,[status(thm)],[c400,l1_32]) ).
cnf(c743,plain,
( greater(sk3(sk2(sk5),sk5),sk2(sk5))
| ~ environment(sk5)
| ~ stable(sk5)
| greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5))) ),
inference(resolution,[status(thm)],[c402,c361]) ).
cnf(c744,plain,
( greater(sk3(sk2(sk5),sk5),sk2(sk5))
| ~ environment(sk5)
| greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5))) ),
inference(resolution,[status(thm)],[c743,prove_l5_34]) ).
cnf(c745,plain,
( greater(sk3(sk2(sk5),sk5),sk2(sk5))
| greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5))) ),
inference(resolution,[status(thm)],[c744,prove_l5_33]) ).
cnf(c750,plain,
( greater(sk3(sk2(sk5),sk5),sk2(sk5))
| ~ environment(sk5)
| ~ in_environment(sk5,sk4(sk5))
| ~ greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5))) ),
inference(resolution,[status(thm)],[c745,mp_earliest_time_growth_rate_exceeds_26]) ).
cnf(c752,plain,
( greater(sk3(sk2(sk5),sk5),sk2(sk5))
| ~ environment(sk5)
| ~ in_environment(sk5,sk4(sk5)) ),
inference(resolution,[status(thm)],[c750,c381]) ).
cnf(c753,plain,
( greater(sk3(sk2(sk5),sk5),sk2(sk5))
| ~ environment(sk5) ),
inference(resolution,[status(thm)],[c752,c21]) ).
cnf(c754,plain,
greater(sk3(sk2(sk5),sk5),sk2(sk5)),
inference(resolution,[status(thm)],[c753,prove_l5_33]) ).
cnf(mp_earliest_time_growth_rate_exceeds_24,axiom,
( ~ environment(X61)
| ~ in_environment(X61,X62)
| greater_or_equal(sk1(X62,X61),X62)
| ~ subpopulations(first_movers,efficient_producers,X61,X60)
| ~ greater(X60,sk2(X61))
| greater(growth_rate(efficient_producers,X60),growth_rate(first_movers,X60)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds_24) ).
cnf(d1_28,plain,
( ~ environment(X111)
| greater(growth_rate(efficient_producers,X112),growth_rate(first_movers,X112))
| ~ in_environment(X111,X112)
| subpopulations(first_movers,efficient_producers,X111,sk3(X112,X111))
| X112 = critical_point(X111) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_28) ).
cnf(c207,plain,
( ~ environment(sk5)
| greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| sk2(sk5) = critical_point(sk5) ),
inference(resolution,[status(thm)],[c204,d1_28]) ).
cnf(c453,plain,
( greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| sk2(sk5) = critical_point(sk5) ),
inference(resolution,[status(thm)],[c207,prove_l5_33]) ).
cnf(c463,plain,
( greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| sk5 != X321
| in_environment(X321,critical_point(sk5)) ),
inference(resolution,[status(thm)],[c453,c206]) ).
cnf(c660,plain,
( greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| in_environment(sk5,critical_point(sk5)) ),
inference(resolution,[status(thm)],[c463,reflexivity]) ).
cnf(c672,plain,
( greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5)) ),
inference(resolution,[status(thm)],[c660,prove_l5_35]) ).
cnf(c454,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| sk2(sk5) = critical_point(sk5)
| ~ environment(sk5)
| ~ in_environment(sk5,X295)
| greater_or_equal(sk1(X295,sk5),X295) ),
inference(resolution,[status(thm)],[c453,mp_earliest_time_growth_rate_exceeds_23]) ).
cnf(c485,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| sk2(sk5) = critical_point(sk5)
| ~ environment(sk5)
| greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5)) ),
inference(resolution,[status(thm)],[c454,c21]) ).
cnf(c586,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| sk2(sk5) = critical_point(sk5)
| greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5)) ),
inference(resolution,[status(thm)],[c485,prove_l5_33]) ).
cnf(c593,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| sk5 != X309
| in_environment(X309,critical_point(sk5)) ),
inference(resolution,[status(thm)],[c586,c206]) ).
cnf(c637,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| in_environment(sk5,critical_point(sk5)) ),
inference(resolution,[status(thm)],[c593,reflexivity]) ).
cnf(c647,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5)) ),
inference(resolution,[status(thm)],[c637,prove_l5_35]) ).
cnf(c679,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| ~ environment(sk5)
| ~ in_environment(sk5,X325)
| subpopulations(first_movers,efficient_producers,sk5,sk1(X325,sk5)) ),
inference(resolution,[status(thm)],[c672,mp_earliest_time_growth_rate_exceeds_21]) ).
cnf(c688,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| ~ environment(sk5)
| subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5)) ),
inference(resolution,[status(thm)],[c679,c21]) ).
cnf(c698,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5)) ),
inference(resolution,[status(thm)],[c688,prove_l5_33]) ).
cnf(c703,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| ~ environment(sk5)
| ~ stable(sk5)
| ~ greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5))) ),
inference(resolution,[status(thm)],[c698,l1_32]) ).
cnf(c760,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| ~ environment(sk5)
| ~ stable(sk5)
| greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5))) ),
inference(resolution,[status(thm)],[c703,c647]) ).
cnf(c761,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| ~ environment(sk5)
| greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5))) ),
inference(resolution,[status(thm)],[c760,prove_l5_34]) ).
cnf(c762,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5))) ),
inference(resolution,[status(thm)],[c761,prove_l5_33]) ).
cnf(c770,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| ~ environment(sk5)
| ~ in_environment(sk5,sk4(sk5))
| ~ greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5))) ),
inference(resolution,[status(thm)],[c762,mp_earliest_time_growth_rate_exceeds_26]) ).
cnf(c771,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| ~ environment(sk5)
| ~ in_environment(sk5,sk4(sk5)) ),
inference(resolution,[status(thm)],[c770,c672]) ).
cnf(c772,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))
| ~ environment(sk5) ),
inference(resolution,[status(thm)],[c771,c21]) ).
cnf(c773,plain,
subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5)),
inference(resolution,[status(thm)],[c772,prove_l5_33]) ).
cnf(c776,plain,
( ~ environment(sk5)
| ~ in_environment(sk5,X663)
| greater_or_equal(sk1(X663,sk5),X663)
| ~ greater(sk3(sk2(sk5),sk5),sk2(sk5))
| greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5))) ),
inference(resolution,[status(thm)],[c773,mp_earliest_time_growth_rate_exceeds_24]) ).
cnf(c782,plain,
( ~ environment(sk5)
| ~ in_environment(sk5,X664)
| greater_or_equal(sk1(X664,sk5),X664)
| greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5))) ),
inference(resolution,[status(thm)],[c776,c754]) ).
cnf(c784,plain,
( ~ environment(sk5)
| greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5))) ),
inference(resolution,[status(thm)],[c782,c21]) ).
cnf(c789,plain,
( greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5))) ),
inference(resolution,[status(thm)],[c784,prove_l5_33]) ).
cnf(c791,plain,
( greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| ~ environment(sk5)
| greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| ~ in_environment(sk5,sk2(sk5))
| sk2(sk5) = critical_point(sk5) ),
inference(resolution,[status(thm)],[c789,d1_30]) ).
cnf(c880,plain,
( greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| ~ environment(sk5)
| greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| sk2(sk5) = critical_point(sk5) ),
inference(resolution,[status(thm)],[c791,c204]) ).
cnf(c881,plain,
( greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| sk2(sk5) = critical_point(sk5) ),
inference(resolution,[status(thm)],[c880,prove_l5_33]) ).
cnf(c883,plain,
( greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| sk2(sk5) = critical_point(sk5)
| ~ environment(sk5)
| ~ in_environment(sk5,X738)
| greater_or_equal(sk1(X738,sk5),X738) ),
inference(resolution,[status(thm)],[c881,mp_earliest_time_growth_rate_exceeds_23]) ).
cnf(c906,plain,
( greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| sk2(sk5) = critical_point(sk5)
| ~ environment(sk5) ),
inference(resolution,[status(thm)],[c883,c21]) ).
cnf(c907,plain,
( greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| sk2(sk5) = critical_point(sk5) ),
inference(resolution,[status(thm)],[c906,prove_l5_33]) ).
cnf(c909,plain,
( greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| sk5 != X740
| in_environment(X740,critical_point(sk5)) ),
inference(resolution,[status(thm)],[c907,c206]) ).
cnf(c945,plain,
( greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| in_environment(sk5,critical_point(sk5)) ),
inference(resolution,[status(thm)],[c909,reflexivity]) ).
cnf(c951,plain,
greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5)),
inference(resolution,[status(thm)],[c945,prove_l5_35]) ).
cnf(mp_earliest_time_growth_rate_exceeds_22,axiom,
( ~ environment(X35)
| ~ in_environment(X35,X36)
| subpopulations(first_movers,efficient_producers,X35,sk1(X36,X35))
| ~ subpopulations(first_movers,efficient_producers,X35,X34)
| ~ greater(X34,sk2(X35))
| greater(growth_rate(efficient_producers,X34),growth_rate(first_movers,X34)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds_22) ).
cnf(c777,plain,
( ~ environment(sk5)
| ~ in_environment(sk5,X802)
| subpopulations(first_movers,efficient_producers,sk5,sk1(X802,sk5))
| ~ greater(sk3(sk2(sk5),sk5),sk2(sk5))
| greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5))) ),
inference(resolution,[status(thm)],[c773,mp_earliest_time_growth_rate_exceeds_22]) ).
cnf(c957,plain,
( ~ environment(sk5)
| ~ in_environment(sk5,X803)
| subpopulations(first_movers,efficient_producers,sk5,sk1(X803,sk5))
| greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5))) ),
inference(resolution,[status(thm)],[c777,c754]) ).
cnf(c959,plain,
( ~ environment(sk5)
| subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))
| greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5))) ),
inference(resolution,[status(thm)],[c957,c21]) ).
cnf(c967,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))
| greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5))) ),
inference(resolution,[status(thm)],[c959,prove_l5_33]) ).
cnf(c972,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))
| ~ environment(sk5)
| greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| ~ in_environment(sk5,sk2(sk5))
| sk2(sk5) = critical_point(sk5) ),
inference(resolution,[status(thm)],[c967,d1_30]) ).
cnf(c1071,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))
| ~ environment(sk5)
| greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| sk2(sk5) = critical_point(sk5) ),
inference(resolution,[status(thm)],[c972,c204]) ).
cnf(c1072,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))
| greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| sk2(sk5) = critical_point(sk5) ),
inference(resolution,[status(thm)],[c1071,prove_l5_33]) ).
cnf(c1080,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))
| greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| sk5 != X874
| in_environment(X874,critical_point(sk5)) ),
inference(resolution,[status(thm)],[c1072,c206]) ).
cnf(c1126,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))
| greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| in_environment(sk5,critical_point(sk5)) ),
inference(resolution,[status(thm)],[c1080,reflexivity]) ).
cnf(c1139,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))
| greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5))) ),
inference(resolution,[status(thm)],[c1126,prove_l5_35]) ).
cnf(c1149,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))
| ~ environment(sk5)
| ~ in_environment(sk5,X877)
| subpopulations(first_movers,efficient_producers,sk5,sk1(X877,sk5)) ),
inference(resolution,[status(thm)],[c1139,mp_earliest_time_growth_rate_exceeds_21]) ).
cnf(c1154,plain,
( subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))
| ~ environment(sk5) ),
inference(resolution,[status(thm)],[c1149,c21]) ).
cnf(c1155,plain,
subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5)),
inference(resolution,[status(thm)],[c1154,prove_l5_33]) ).
cnf(c1156,plain,
( ~ environment(sk5)
| ~ stable(sk5)
| ~ greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))
| greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5))) ),
inference(resolution,[status(thm)],[c1155,l1_32]) ).
cnf(c1164,plain,
( ~ environment(sk5)
| ~ stable(sk5)
| greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5))) ),
inference(resolution,[status(thm)],[c1156,c951]) ).
cnf(c1165,plain,
( ~ environment(sk5)
| greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5))) ),
inference(resolution,[status(thm)],[c1164,prove_l5_34]) ).
cnf(c1166,plain,
greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5))),
inference(resolution,[status(thm)],[c1165,prove_l5_33]) ).
cnf(c1167,plain,
( ~ environment(sk5)
| ~ in_environment(sk5,sk4(sk5))
| ~ greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5))) ),
inference(resolution,[status(thm)],[c1166,mp_earliest_time_growth_rate_exceeds_26]) ).
cnf(mp_earliest_time_growth_rate_exceeds_27,axiom,
( ~ environment(X98)
| ~ in_environment(X98,X99)
| ~ greater(growth_rate(efficient_producers,sk1(X99,X98)),growth_rate(first_movers,sk1(X99,X98)))
| ~ subpopulations(first_movers,efficient_producers,X98,X97)
| ~ greater(X97,sk2(X98))
| greater(growth_rate(efficient_producers,X97),growth_rate(first_movers,X97)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_earliest_time_growth_rate_exceeds_27) ).
cnf(c1169,plain,
( ~ environment(sk5)
| ~ in_environment(sk5,sk4(sk5))
| ~ subpopulations(first_movers,efficient_producers,sk5,X905)
| ~ greater(X905,sk2(sk5))
| greater(growth_rate(efficient_producers,X905),growth_rate(first_movers,X905)) ),
inference(resolution,[status(thm)],[c1166,mp_earliest_time_growth_rate_exceeds_27]) ).
cnf(c1174,plain,
( ~ environment(sk5)
| ~ in_environment(sk5,sk4(sk5))
| ~ greater(sk3(sk2(sk5),sk5),sk2(sk5))
| greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5))) ),
inference(resolution,[status(thm)],[c1169,c773]) ).
cnf(c1177,plain,
( ~ environment(sk5)
| ~ in_environment(sk5,sk4(sk5))
| greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5))) ),
inference(resolution,[status(thm)],[c1174,c754]) ).
cnf(c1178,plain,
( ~ environment(sk5)
| greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5))) ),
inference(resolution,[status(thm)],[c1177,c21]) ).
cnf(c1179,plain,
greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5))),
inference(resolution,[status(thm)],[c1178,prove_l5_33]) ).
cnf(c1180,plain,
( ~ environment(sk5)
| greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| ~ in_environment(sk5,sk2(sk5))
| sk2(sk5) = critical_point(sk5) ),
inference(resolution,[status(thm)],[c1179,d1_30]) ).
cnf(c1184,plain,
( ~ environment(sk5)
| greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| sk2(sk5) = critical_point(sk5) ),
inference(resolution,[status(thm)],[c1180,c204]) ).
cnf(c1185,plain,
( greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))
| sk2(sk5) = critical_point(sk5) ),
inference(resolution,[status(thm)],[c1184,prove_l5_33]) ).
cnf(c1188,plain,
( sk2(sk5) = critical_point(sk5)
| ~ environment(sk5)
| ~ in_environment(sk5,sk4(sk5)) ),
inference(resolution,[status(thm)],[c1185,c1167]) ).
cnf(c1209,plain,
( sk2(sk5) = critical_point(sk5)
| ~ environment(sk5) ),
inference(resolution,[status(thm)],[c1188,c21]) ).
cnf(c1210,plain,
sk2(sk5) = critical_point(sk5),
inference(resolution,[status(thm)],[c1209,prove_l5_33]) ).
cnf(c1211,plain,
( sk5 != X930
| in_environment(X930,critical_point(sk5)) ),
inference(resolution,[status(thm)],[c1210,c206]) ).
cnf(c1246,plain,
in_environment(sk5,critical_point(sk5)),
inference(resolution,[status(thm)],[c1211,reflexivity]) ).
cnf(c1250,plain,
$false,
inference(resolution,[status(thm)],[c1246,prove_l5_35]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT023-2 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.10/0.36 % Computer : n007.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 7 12:05:26 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.15/0.43 (re.compile("\."), Token.FullStop),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.15/0.43 (re.compile("\("), Token.OpenPar),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.15/0.43 (re.compile("\)"), Token.ClosePar),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.15/0.43 (re.compile("\["), Token.OpenSquare),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.15/0.43 (re.compile("\]"), Token.CloseSquare),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.15/0.43 (re.compile("~\|"), Token.Nor),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.15/0.43 (re.compile("\|"), Token.Or),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.15/0.43 (re.compile("\?"), Token.Existential),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.15/0.43 (re.compile("\s+"), Token.WhiteSpace),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.15/0.43 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.26/0.50 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.26/0.50 """
% 0.26/0.51 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.26/0.51 """
% 0.35/0.60 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.35/0.60 """
% 1.27/1.51 % Version: 1.5
% 1.27/1.51 % SZS status Unsatisfiable
% 1.27/1.51 % SZS output start CNFRefutation
% See solution above
% 1.27/1.51
% 1.27/1.51 % Initial clauses : 32
% 1.27/1.51 % Processed clauses : 357
% 1.27/1.51 % Factors computed : 4
% 1.27/1.51 % Resolvents computed: 1237
% 1.27/1.51 % Tautologies deleted: 4
% 1.27/1.51 % Forward subsumed : 771
% 1.27/1.51 % Backward subsumed : 260
% 1.27/1.51 % -------- CPU Time ---------
% 1.27/1.51 % User time : 1.119 s
% 1.27/1.51 % System time : 0.028 s
% 1.27/1.51 % Total time : 1.147 s
%------------------------------------------------------------------------------