%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : MGT026+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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 : Theorem 53.26s 7.14s
% Output : CNFRefutation 53.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 11
% Syntax : Number of formulae : 53 ( 16 unt; 0 def)
% Number of atoms : 153 ( 10 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 166 ( 66 ~; 65 |; 22 &)
% ( 1 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 58 ( 0 sgn 29 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(prove_l8,plain,
! [E,T] :
( ( environment(E)
& in_environment(E,T)
& greater(T,critical_point(E)) )
=> selection_favors(efficient_producers,first_movers,T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l8) ).
fof(prove_l8_negated,plain,
~ ! [E,T] :
( ( environment(E)
& in_environment(E,T)
& greater(T,critical_point(E)) )
=> selection_favors(efficient_producers,first_movers,T) ),
inference(negate_conjecture,[status(cth)],[prove_l8]) ).
cnf(14,plain,
environment(sK1),
inference(cnf,[status(esa)],[prove_l8_negated]) ).
cnf(l0,plain,
environment(sK1),
inference(instantiation,[status(thm)],[14]) ).
fof(t6,plain,
! [E,T] :
( ( environment(E)
& in_environment(E,T)
& greater_or_equal(T,appear(efficient_producers,E)) )
=> greater(cardinality_at_time(efficient_producers,T),zero) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6) ).
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]) ).
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]) ).
fof(mp_non_empty_fm_and_ep,plain,
! [E,T] :
( ( environment(E)
& in_environment(E,T)
& greater(cardinality_at_time(first_movers,T),zero)
& greater(cardinality_at_time(efficient_producers,T),zero) )
=> subpopulations(first_movers,efficient_producers,E,T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_non_empty_fm_and_ep) ).
cnf(2,plain,
( ~ environment(X0)
| ~ greater(cardinality_at_time(efficient_producers,X1),zero)
| ~ greater(cardinality_at_time(first_movers,X1),zero)
| ~ in_environment(X0,X1)
| subpopulations(first_movers,efficient_producers,X0,X1) ),
inference(cnf,[status(esa)],[mp_non_empty_fm_and_ep]) ).
cnf(l3,plain,
( ~ environment(sK1)
| ~ greater(cardinality_at_time(efficient_producers,sK2),zero)
| ~ greater(cardinality_at_time(first_movers,sK2),zero)
| ~ in_environment(sK1,sK2)
| subpopulations(first_movers,efficient_producers,sK1,sK2) ),
inference(instantiation,[status(thm)],[2]) ).
fof(mp1_high_growth_rates,plain,
! [E,S1,S2,T] :
( ( environment(E)
& subpopulations(S1,S2,E,T)
& greater(growth_rate(S2,T),growth_rate(S1,T)) )
=> selection_favors(S2,S1,T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp1_high_growth_rates) ).
cnf(0,plain,
( ~ environment(X0)
| ~ subpopulations(X1,X2,X0,X3)
| ~ greater(growth_rate(X2,X3),growth_rate(X1,X3))
| selection_favors(X2,X1,X3) ),
inference(cnf,[status(esa)],[mp1_high_growth_rates]) ).
cnf(l343,plain,
( ~ environment(sK1)
| ~ subpopulations(first_movers,efficient_producers,sK1,sK2)
| ~ greater(growth_rate(efficient_producers,sK2),growth_rate(first_movers,sK2))
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(17,plain,
~ selection_favors(efficient_producers,first_movers,sK2),
inference(cnf,[status(esa)],[prove_l8_negated]) ).
cnf(l1278,plain,
~ selection_favors(efficient_producers,first_movers,sK2),
inference(instantiation,[status(thm)],[17]) ).
fof(mp_greater_or_equal,plain,
! [X,Y] :
( greater_or_equal(X,Y)
<=> ( greater(X,Y)
| X = Y ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal) ).
cnf(9,plain,
( ~ greater(X0,X1)
| greater_or_equal(X0,X1) ),
inference(cnf,[status(esa)],[mp_greater_or_equal]) ).
cnf(l1025,plain,
( ~ greater(sK2,appear(efficient_producers,sK1))
| greater_or_equal(sK2,appear(efficient_producers,sK1)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(15,plain,
in_environment(sK1,sK2),
inference(cnf,[status(esa)],[prove_l8_negated]) ).
cnf(l6,plain,
in_environment(sK1,sK2),
inference(instantiation,[status(thm)],[15]) ).
fof(d1,plain,
! [E,Tc] :
( ( environment(E)
& Tc = critical_point(E) )
=> ( ~ greater(growth_rate(efficient_producers,Tc),growth_rate(first_movers,Tc))
& ! [T] :
( ( subpopulations(first_movers,efficient_producers,E,T)
& greater(T,Tc) )
=> greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1) ).
cnf(12,plain,
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| X2 != critical_point(X0)
| ~ greater(X1,X2)
| greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1)) ),
inference(cnf,[status(esa)],[d1]) ).
cnf(l364,plain,
( ~ environment(sK1)
| ~ subpopulations(first_movers,efficient_producers,sK1,sK2)
| critical_point(sK1) != critical_point(sK1)
| ~ greater(sK2,critical_point(sK1))
| greater(growth_rate(efficient_producers,sK2),growth_rate(first_movers,sK2)) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l1024,plain,
in_environment(sK1,sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(8,plain,
( ~ greater_or_equal(X0,X1)
| X0 = X1
| greater(X0,X1) ),
inference(cnf,[status(esa)],[mp_greater_or_equal]) ).
cnf(l337,plain,
( ~ greater_or_equal(cardinality_at_time(first_movers,sK2),zero)
| cardinality_at_time(first_movers,sK2) = zero
| greater(cardinality_at_time(first_movers,sK2),zero) ),
inference(instantiation,[status(thm)],[8]) ).
fof(mp_greater_transitivity,plain,
! [X,Y,Z] :
( ( greater(X,Y)
& greater(Y,Z) )
=> greater(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_transitivity) ).
cnf(7,plain,
( ~ greater(X0,X1)
| ~ greater(X1,X2)
| greater(X0,X2) ),
inference(cnf,[status(esa)],[mp_greater_transitivity]) ).
cnf(l1027,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(16,plain,
greater(sK2,critical_point(sK1)),
inference(cnf,[status(esa)],[prove_l8_negated]) ).
cnf(l1061,plain,
greater(sK2,critical_point(sK1)),
inference(instantiation,[status(thm)],[16]) ).
fof(mp_first_movers_exist,plain,
! [E,T] :
( ( environment(E)
& in_environment(E,T) )
=> greater_or_equal(cardinality_at_time(first_movers,T),zero) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_first_movers_exist) ).
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]) ).
cnf(l354,plain,
( ~ environment(sK1)
| ~ in_environment(sK1,sK2)
| greater_or_equal(cardinality_at_time(first_movers,sK2),zero) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1034,plain,
( ~ greater_or_equal(critical_point(sK1),appear(efficient_producers,sK1))
| critical_point(sK1) = appear(efficient_producers,sK1)
| greater(critical_point(sK1),appear(efficient_producers,sK1)) ),
inference(instantiation,[status(thm)],[8]) ).
fof(mp_critical_point_after_EP,plain,
! [E] :
( environment(E)
=> greater_or_equal(critical_point(E),appear(efficient_producers,E)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_critical_point_after_EP) ).
cnf(6,plain,
( ~ environment(X0)
| greater_or_equal(critical_point(X0),appear(efficient_producers,X0)) ),
inference(cnf,[status(esa)],[mp_critical_point_after_EP]) ).
cnf(l1069,plain,
( ~ environment(sK1)
| greater_or_equal(critical_point(sK1),appear(efficient_producers,sK1)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l435,plain,
in_environment(sK1,sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1301,plain,
greater(sK2,critical_point(sK1)),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1115,plain,
greater(sK2,critical_point(sK1)),
inference(instantiation,[status(thm)],[16]) ).
fof(mp2_favour_members,plain,
! [E,S1,S2,T] :
( ( environment(E)
& subpopulation(S1,E,T)
& subpopulation(S2,E,T)
& greater(cardinality_at_time(S1,T),zero)
& cardinality_at_time(S2,T) = zero )
=> selection_favors(S1,S2,T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp2_favour_members) ).
cnf(1,plain,
( ~ environment(X0)
| ~ subpopulation(X1,X0,X2)
| ~ subpopulation(X3,X0,X2)
| cardinality_at_time(X3,X2) != zero
| ~ greater(cardinality_at_time(X1,X2),zero)
| selection_favors(X1,X3,X2) ),
inference(cnf,[status(esa)],[mp2_favour_members]) ).
cnf(l371,plain,
( ~ environment(sK1)
| ~ subpopulation(efficient_producers,sK1,sK2)
| ~ subpopulation(first_movers,sK1,sK2)
| cardinality_at_time(first_movers,sK2) != zero
| ~ greater(cardinality_at_time(efficient_producers,sK2),zero)
| selection_favors(efficient_producers,first_movers,sK2) ),
inference(instantiation,[status(thm)],[1]) ).
fof(mp_subpopulations,plain,
! [E,T] :
( ( environment(E)
& in_environment(E,T) )
=> ( subpopulation(first_movers,E,T)
& subpopulation(efficient_producers,E,T) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_subpopulations) ).
cnf(5,plain,
( ~ environment(X0)
| ~ in_environment(X0,X1)
| subpopulation(efficient_producers,X0,X1) ),
inference(cnf,[status(esa)],[mp_subpopulations]) ).
cnf(l537,plain,
( ~ environment(sK1)
| ~ in_environment(sK1,sK2)
| subpopulation(efficient_producers,sK1,sK2) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l554,plain,
in_environment(sK1,sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(4,plain,
( ~ environment(X0)
| ~ in_environment(X0,X1)
| subpopulation(first_movers,X0,X1) ),
inference(cnf,[status(esa)],[mp_subpopulations]) ).
cnf(l552,plain,
( ~ environment(sK1)
| ~ in_environment(sK1,sK2)
| subpopulation(first_movers,sK1,sK2) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l593,plain,
in_environment(sK1,sK2),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1297,plain,
~ selection_favors(efficient_producers,first_movers,sK2),
inference(instantiation,[status(thm)],[17]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l3,l343,l1278,l1025,l6,l364,l1024,l337,l1027,l1061,l354,l1034,l1069,l435,l1301,l1115,l371,l537,l554,l552,l593,l1297]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT026+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n003.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.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 7 12:13:09 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % launching worker at depth: 1
% 0.09/0.36 % launching worker at depth: 5
% 0.09/0.36 % launching worker at depth: 3
% 0.09/0.36 % launching worker at depth: 4
% 0.09/0.36 % launching worker at depth: 7
% 0.09/0.36 % launching worker at depth: 6
% 0.09/0.36 % launching worker at depth: 8
% 0.09/0.36 % launching worker at depth: 2
% 0.09/0.37 % launching worker at depth: 9
% 0.09/0.37 % launching worker at depth: 10
% 0.13/0.39 % launching worker at depth: 11
% 2.35/0.65 % launching worker at depth: 12
% 10.67/1.74 % launching worker at depth: 13
% 53.26/7.14 % SZS status Theorem for theBenchmark
% 53.26/7.14 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------