%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : MGT026-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:23 AM UTC 2026
% Result : Unsatisfiable 161.83s 20.79s
% Output : CNFRefutation 161.83s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named prove_l8_42ERROR: Could not build tree for root finalERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(14,plain,
environment(sk1),
inference(cnf,[status(esa)],[prove_l8_42]) ).
cnf(l0,plain,
environment(sk1),
inference(instantiation,[status(thm)],[14]) ).
cnf(13,plain,
( ~ greater_or_equal(X0,appear(efficient_producers,X1))
| ~ environment(X1)
| ~ in_environment(X1,X0)
| greater(cardinality_at_time(efficient_producers,X0),zero) ),
inference(cnf,[status(esa)],[t6_41]) ).
cnf(l1,plain,
( ~ greater_or_equal(sk2,appear(efficient_producers,sk1))
| ~ environment(sk1)
| ~ in_environment(sk1,sk2)
| greater(cardinality_at_time(efficient_producers,sk2),zero) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(15,plain,
in_environment(sk1,sk2),
inference(cnf,[status(esa)],[prove_l8_43]) ).
cnf(l11,plain,
in_environment(sk1,sk2),
inference(instantiation,[status(thm)],[15]) ).
cnf(8,plain,
( ~ greater_or_equal(X0,X1)
| greater(X0,X1)
| X0 = X1 ),
inference(cnf,[status(esa)],[mp_greater_or_equal_36]) ).
cnf(l428,plain,
( ~ greater_or_equal(critical_point(sk1),appear(efficient_producers,sk1))
| greater(critical_point(sk1),appear(efficient_producers,sk1))
| critical_point(sk1) = appear(efficient_producers,sk1) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(2,plain,
( ~ greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater(cardinality_at_time(first_movers,X0),zero)
| ~ environment(X1)
| ~ in_environment(X1,X0)
| subpopulations(first_movers,efficient_producers,X1,X0) ),
inference(cnf,[status(esa)],[mp_non_empty_fm_and_ep_30]) ).
cnf(l435,plain,
( ~ greater(cardinality_at_time(efficient_producers,sk2),zero)
| ~ greater(cardinality_at_time(first_movers,sk2),zero)
| ~ environment(sk1)
| ~ in_environment(sk1,sk2)
| subpopulations(first_movers,efficient_producers,sk1,sk2) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(9,plain,
( ~ greater(X0,X1)
| greater_or_equal(X0,X1) ),
inference(cnf,[status(esa)],[mp_greater_or_equal_37]) ).
cnf(l17,plain,
( ~ greater(sk2,critical_point(sk1))
| greater_or_equal(sk2,critical_point(sk1)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l446,plain,
( ~ greater_or_equal(cardinality_at_time(first_movers,sk2),zero)
| greater(cardinality_at_time(first_movers,sk2),zero)
| cardinality_at_time(first_movers,sk2) = zero ),
inference(instantiation,[status(thm)],[8]) ).
cnf(3,plain,
( ~ environment(X0)
| ~ in_environment(X0,X1)
| greater_or_equal(cardinality_at_time(first_movers,X1),zero) ),
inference(cnf,[status(esa)],[mp_first_movers_exist_31]) ).
cnf(l448,plain,
( ~ environment(sk1)
| ~ in_environment(sk1,sk2)
| greater_or_equal(cardinality_at_time(first_movers,sk2),zero) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(0,plain,
( ~ greater(growth_rate(X0,X1),growth_rate(X2,X1))
| ~ subpopulations(X2,X0,X3,X1)
| ~ environment(X3)
| selection_favors(X0,X2,X1) ),
inference(cnf,[status(esa)],[mp1_high_growth_rates_28]) ).
cnf(l436,plain,
( ~ greater(growth_rate(efficient_producers,sk2),growth_rate(first_movers,sk2))
| ~ subpopulations(first_movers,efficient_producers,sk1,sk2)
| ~ environment(sk1)
| selection_favors(efficient_producers,first_movers,sk2) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(12,plain,
( ~ greater(X0,X1)
| X1 != critical_point(X2)
| ~ subpopulations(first_movers,efficient_producers,X2,X0)
| ~ environment(X2)
| greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0)) ),
inference(cnf,[status(esa)],[d1_40]) ).
cnf(l492,plain,
( ~ greater(sk2,critical_point(sk1))
| critical_point(sk1) != critical_point(sk1)
| ~ subpopulations(first_movers,efficient_producers,sk1,sk2)
| ~ environment(sk1)
| greater(growth_rate(efficient_producers,sk2),growth_rate(first_movers,sk2)) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(16,plain,
greater(sk2,critical_point(sk1)),
inference(cnf,[status(esa)],[prove_l8_44]) ).
cnf(l32,plain,
greater(sk2,critical_point(sk1)),
inference(instantiation,[status(thm)],[16]) ).
cnf(17,plain,
~ selection_favors(efficient_producers,first_movers,sk2),
inference(cnf,[status(esa)],[prove_l8_45]) ).
cnf(l1142,plain,
~ selection_favors(efficient_producers,first_movers,sk2),
inference(instantiation,[status(thm)],[17]) ).
cnf(7,plain,
( ~ greater(X0,X1)
| ~ greater(X1,X2)
| greater(X0,X2) ),
inference(cnf,[status(esa)],[mp_greater_transitivity_35]) ).
cnf(l433,plain,
( ~ greater(sk2,critical_point(sk1))
| ~ greater(critical_point(sk1),appear(efficient_producers,sk1))
| greater(sk2,appear(efficient_producers,sk1)) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(6,plain,
( ~ environment(X0)
| greater_or_equal(critical_point(X0),appear(efficient_producers,X0)) ),
inference(cnf,[status(esa)],[mp_critical_point_after_EP_34]) ).
cnf(l437,plain,
( ~ environment(sk1)
| greater_or_equal(critical_point(sk1),appear(efficient_producers,sk1)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l541,plain,
in_environment(sk1,sk2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l949,plain,
in_environment(sk1,sk2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l493,plain,
greater(sk2,critical_point(sk1)),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1177,plain,
( ~ greater(sk2,appear(efficient_producers,sk1))
| greater_or_equal(sk2,appear(efficient_producers,sk1)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(1,plain,
( ~ greater(cardinality_at_time(X0,X1),zero)
| cardinality_at_time(X2,X1) != zero
| ~ subpopulation(X0,X3,X1)
| ~ subpopulation(X2,X3,X1)
| ~ environment(X3)
| selection_favors(X0,X2,X1) ),
inference(cnf,[status(esa)],[mp2_favour_members_29]) ).
cnf(l1183,plain,
( ~ greater(cardinality_at_time(efficient_producers,sk2),zero)
| cardinality_at_time(first_movers,sk2) != zero
| ~ subpopulation(efficient_producers,sk1,sk2)
| ~ subpopulation(first_movers,sk1,sk2)
| ~ environment(sk1)
| selection_favors(efficient_producers,first_movers,sk2) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l439,plain,
greater(sk2,critical_point(sk1)),
inference(instantiation,[status(thm)],[16]) ).
cnf(5,plain,
( ~ environment(X0)
| ~ in_environment(X0,X1)
| subpopulation(efficient_producers,X0,X1) ),
inference(cnf,[status(esa)],[mp_subpopulations_33]) ).
cnf(l1193,plain,
( ~ environment(sk1)
| ~ in_environment(sk1,sk2)
| subpopulation(efficient_producers,sk1,sk2) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1207,plain,
in_environment(sk1,sk2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1213,plain,
~ selection_favors(efficient_producers,first_movers,sk2),
inference(instantiation,[status(thm)],[17]) ).
cnf(4,plain,
( ~ environment(X0)
| ~ in_environment(X0,X1)
| subpopulation(first_movers,X0,X1) ),
inference(cnf,[status(esa)],[mp_subpopulations_32]) ).
cnf(l1208,plain,
( ~ environment(sk1)
| ~ in_environment(sk1,sk2)
| subpopulation(first_movers,sk1,sk2) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2953,plain,
in_environment(sk1,sk2),
inference(instantiation,[status(thm)],[15]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l11,l428,l435,l17,l446,l448,l436,l492,l32,l1142,l433,l437,l541,l949,l493,l1177,l1183,l439,l1193,l1207,l1213,l1208,l2953]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT026-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n006.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 7 12:12:31 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 % launching worker at depth: 1
% 0.13/0.36 % launching worker at depth: 5
% 0.13/0.36 % launching worker at depth: 3
% 0.13/0.36 % launching worker at depth: 4
% 0.13/0.36 % launching worker at depth: 6
% 0.13/0.36 % launching worker at depth: 7
% 0.13/0.36 % launching worker at depth: 8
% 0.13/0.36 % launching worker at depth: 2
% 0.13/0.36 % launching worker at depth: 9
% 0.13/0.36 % launching worker at depth: 10
% 0.13/0.39 % launching worker at depth: 11
% 2.35/0.66 % launching worker at depth: 12
% 22.27/3.20 % launching worker at depth: 13
% 161.83/20.79 % SZS status Theorem for theBenchmark
% 161.83/20.79 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------