%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : MGT024+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n029.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 22.56s 3.25s
% Output : CNFRefutation 22.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 7
% Syntax : Number of formulae : 77 ( 28 unt; 0 def)
% Number of atoms : 201 ( 14 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 211 ( 87 ~; 89 |; 23 &)
% ( 0 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 34 ( 0 sgn 16 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(prove_l6,plain,
! [E,T] :
( ( environment(E)
& subpopulations(first_movers,efficient_producers,E,T)
& greater_or_equal(T,equilibrium(E)) )
=> ( ( growth_rate(first_movers,T) = zero
& growth_rate(efficient_producers,T) = zero )
| ( greater(growth_rate(first_movers,T),zero)
& greater(zero,growth_rate(efficient_producers,T)) )
| ( greater(growth_rate(efficient_producers,T),zero)
& greater(zero,growth_rate(first_movers,T)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_l6) ).
fof(prove_l6_negated,plain,
~ ! [E,T] :
( ( environment(E)
& subpopulations(first_movers,efficient_producers,E,T)
& greater_or_equal(T,equilibrium(E)) )
=> ( ( growth_rate(first_movers,T) = zero
& growth_rate(efficient_producers,T) = zero )
| ( greater(growth_rate(first_movers,T),zero)
& greater(zero,growth_rate(efficient_producers,T)) )
| ( greater(growth_rate(efficient_producers,T),zero)
& greater(zero,growth_rate(first_movers,T)) ) ) ),
inference(negate_conjecture,[status(cth)],[prove_l6]) ).
cnf(16,plain,
( growth_rate(first_movers,sK2) != zero
| growth_rate(efficient_producers,sK2) != zero ),
inference(cnf,[status(esa)],[prove_l6_negated]) ).
cnf(l0,plain,
( growth_rate(first_movers,sK2) != zero
| growth_rate(efficient_producers,sK2) != zero ),
inference(instantiation,[status(thm)],[16]) ).
fof(l7,plain,
! [E,T] :
( ( environment(E)
& subpopulations(first_movers,efficient_producers,E,T)
& constant(number_of_organizations(E,T)) )
=> ( ( growth_rate(first_movers,T) = zero
& growth_rate(efficient_producers,T) = zero )
| ( greater(growth_rate(first_movers,T),zero)
& greater(zero,growth_rate(efficient_producers,T)) )
| ( greater(growth_rate(efficient_producers,T),zero)
& greater(zero,growth_rate(first_movers,T)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l7) ).
cnf(7,plain,
( ~ constant(number_of_organizations(X0,X1))
| ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| sP1(X1)
| sP0(X1)
| growth_rate(first_movers,X1) = zero ),
inference(cnf,[status(esa)],[l7]) ).
cnf(l1,plain,
( ~ constant(number_of_organizations(sK1,sK2))
| ~ environment(sK1)
| ~ subpopulations(first_movers,efficient_producers,sK1,sK2)
| sP1(sK2)
| sP0(sK2)
| growth_rate(first_movers,sK2) = zero ),
inference(instantiation,[status(thm)],[7]) ).
cnf(13,plain,
environment(sK1),
inference(cnf,[status(esa)],[prove_l6_negated]) ).
cnf(l368,plain,
environment(sK1),
inference(instantiation,[status(thm)],[13]) ).
fof(a6,plain,
! [E,T] :
( ( environment(E)
& in_environment(E,T) )
=> ( ( decreases(resources(E,T))
=> ~ decreases(number_of_organizations(E,T)) )
& ( constant(resources(E,T))
=> constant(number_of_organizations(E,T)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a6) ).
cnf(6,plain,
( ~ constant(resources(X0,X1))
| ~ environment(X0)
| ~ in_environment(X0,X1)
| constant(number_of_organizations(X0,X1)) ),
inference(cnf,[status(esa)],[a6]) ).
cnf(l2,plain,
( ~ constant(resources(sK1,sK2))
| ~ environment(sK1)
| ~ in_environment(sK1,sK2)
| constant(number_of_organizations(sK1,sK2)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(14,plain,
subpopulations(first_movers,efficient_producers,sK1,sK2),
inference(cnf,[status(esa)],[prove_l6_negated]) ).
cnf(l3,plain,
subpopulations(first_movers,efficient_producers,sK1,sK2),
inference(instantiation,[status(thm)],[14]) ).
fof(mp_time_point_occur,plain,
! [E,T] :
( ( environment(E)
& subpopulations(first_movers,efficient_producers,E,T) )
=> in_environment(E,T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_time_point_occur) ).
cnf(0,plain,
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| in_environment(X0,X1) ),
inference(cnf,[status(esa)],[mp_time_point_occur]) ).
cnf(l145,plain,
( ~ environment(sK1)
| ~ subpopulations(first_movers,efficient_producers,sK1,sK2)
| in_environment(sK1,sK2) ),
inference(instantiation,[status(thm)],[0]) ).
fof(a3,plain,
! [E,T] :
( ( environment(E)
& in_environment(E,T)
& greater(number_of_organizations(E,T),zero) )
=> ( ( greater(equilibrium(E),T)
=> decreases(resources(E,T)) )
& ( ~ greater(equilibrium(E),T)
=> constant(resources(E,T)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a3) ).
cnf(4,plain,
( ~ greater(number_of_organizations(X0,X1),zero)
| ~ environment(X0)
| ~ in_environment(X0,X1)
| constant(resources(X0,X1))
| greater(equilibrium(X0),X1) ),
inference(cnf,[status(esa)],[a3]) ).
cnf(l12,plain,
( ~ greater(number_of_organizations(sK1,sK2),zero)
| ~ environment(sK1)
| ~ in_environment(sK1,sK2)
| constant(resources(sK1,sK2))
| greater(equilibrium(sK1),sK2) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l150,plain,
environment(sK1),
inference(instantiation,[status(thm)],[13]) ).
cnf(l147,plain,
subpopulations(first_movers,efficient_producers,sK1,sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l6,plain,
environment(sK1),
inference(instantiation,[status(thm)],[13]) ).
cnf(l162,plain,
( ~ environment(sK1)
| ~ subpopulations(first_movers,efficient_producers,sK1,sK2)
| in_environment(sK1,sK2) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(8,plain,
( ~ constant(number_of_organizations(X0,X1))
| ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| sP1(X1)
| sP0(X1)
| growth_rate(efficient_producers,X1) = zero ),
inference(cnf,[status(esa)],[l7]) ).
cnf(l876,plain,
( ~ constant(number_of_organizations(sK1,sK2))
| ~ environment(sK1)
| ~ subpopulations(first_movers,efficient_producers,sK1,sK2)
| sP1(sK2)
| sP0(sK2)
| growth_rate(efficient_producers,sK2) = zero ),
inference(instantiation,[status(thm)],[8]) ).
fof(mp_equilibrium,plain,
! [E,T] :
( ( environment(E)
& greater_or_equal(T,equilibrium(E)) )
=> ~ greater(equilibrium(E),T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_equilibrium) ).
cnf(2,plain,
( ~ greater_or_equal(X0,equilibrium(X1))
| ~ greater(equilibrium(X1),X0)
| ~ environment(X1) ),
inference(cnf,[status(esa)],[mp_equilibrium]) ).
cnf(l593,plain,
( ~ greater_or_equal(sK2,equilibrium(sK1))
| ~ greater(equilibrium(sK1),sK2)
| ~ environment(sK1) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(10,plain,
( greater(growth_rate(efficient_producers,X0),zero)
| ~ sP1(X0) ),
inference(cnf,[status(esa)],[l7]) ).
cnf(l4,plain,
( greater(growth_rate(efficient_producers,sK2),zero)
| ~ sP1(sK2) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(15,plain,
greater_or_equal(sK2,equilibrium(sK1)),
inference(cnf,[status(esa)],[prove_l6_negated]) ).
cnf(l608,plain,
greater_or_equal(sK2,equilibrium(sK1)),
inference(instantiation,[status(thm)],[15]) ).
cnf(12,plain,
( greater(growth_rate(first_movers,X0),zero)
| ~ sP0(X0) ),
inference(cnf,[status(esa)],[l7]) ).
cnf(l200,plain,
( greater(growth_rate(first_movers,sK2),zero)
| ~ sP0(sK2) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l47,plain,
environment(sK1),
inference(instantiation,[status(thm)],[13]) ).
cnf(l163,plain,
subpopulations(first_movers,efficient_producers,sK1,sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l987,plain,
( greater(growth_rate(first_movers,sK2),zero)
| ~ sP0(sK2) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(17,plain,
( ~ greater(growth_rate(first_movers,sK2),zero)
| ~ greater(zero,growth_rate(efficient_producers,sK2)) ),
inference(cnf,[status(esa)],[prove_l6_negated]) ).
cnf(l201,plain,
( ~ greater(growth_rate(first_movers,sK2),zero)
| ~ greater(zero,growth_rate(efficient_producers,sK2)) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l878,plain,
( ~ constant(resources(sK1,sK2))
| ~ environment(sK1)
| ~ in_environment(sK1,sK2)
| constant(number_of_organizations(sK1,sK2)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l884,plain,
environment(sK1),
inference(instantiation,[status(thm)],[13]) ).
cnf(l179,plain,
environment(sK1),
inference(instantiation,[status(thm)],[13]) ).
cnf(18,plain,
( ~ greater(growth_rate(efficient_producers,sK2),zero)
| ~ greater(zero,growth_rate(first_movers,sK2)) ),
inference(cnf,[status(esa)],[prove_l6_negated]) ).
cnf(l8,plain,
( ~ greater(growth_rate(efficient_producers,sK2),zero)
| ~ greater(zero,growth_rate(first_movers,sK2)) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l879,plain,
( ~ greater(number_of_organizations(sK1,sK2),zero)
| ~ environment(sK1)
| ~ in_environment(sK1,sK2)
| constant(resources(sK1,sK2))
| greater(equilibrium(sK1),sK2) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l877,plain,
environment(sK1),
inference(instantiation,[status(thm)],[13]) ).
fof(mp_positive_number_of_organizations,plain,
! [E,T] :
( ( environment(E)
& subpopulations(first_movers,efficient_producers,E,T) )
=> greater(number_of_organizations(E,T),zero) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_positive_number_of_organizations) ).
cnf(1,plain,
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X1)
| greater(number_of_organizations(X0,X1),zero) ),
inference(cnf,[status(esa)],[mp_positive_number_of_organizations]) ).
cnf(l944,plain,
( ~ environment(sK1)
| ~ subpopulations(first_movers,efficient_producers,sK1,sK2)
| greater(number_of_organizations(sK1,sK2),zero) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l994,plain,
subpopulations(first_movers,efficient_producers,sK1,sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(9,plain,
( greater(zero,growth_rate(first_movers,X0))
| ~ sP1(X0) ),
inference(cnf,[status(esa)],[l7]) ).
cnf(l53,plain,
( greater(zero,growth_rate(first_movers,sK2))
| ~ sP1(sK2) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l990,plain,
( ~ greater(growth_rate(first_movers,sK2),zero)
| ~ greater(zero,growth_rate(efficient_producers,sK2)) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(11,plain,
( greater(zero,growth_rate(efficient_producers,X0))
| ~ sP0(X0) ),
inference(cnf,[status(esa)],[l7]) ).
cnf(l210,plain,
( greater(zero,growth_rate(efficient_producers,sK2))
| ~ sP0(sK2) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l847,plain,
environment(sK1),
inference(instantiation,[status(thm)],[13]) ).
cnf(l946,plain,
environment(sK1),
inference(instantiation,[status(thm)],[13]) ).
cnf(l945,plain,
environment(sK1),
inference(instantiation,[status(thm)],[13]) ).
cnf(l953,plain,
subpopulations(first_movers,efficient_producers,sK1,sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1013,plain,
( ~ environment(sK1)
| ~ subpopulations(first_movers,efficient_producers,sK1,sK2)
| in_environment(sK1,sK2) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1041,plain,
( greater(zero,growth_rate(efficient_producers,sK2))
| ~ sP0(sK2) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l51,plain,
( ~ environment(sK1)
| ~ subpopulations(first_movers,efficient_producers,sK1,sK2)
| greater(number_of_organizations(sK1,sK2),zero) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l989,plain,
( greater(zero,growth_rate(first_movers,sK2))
| ~ sP1(sK2) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1050,plain,
subpopulations(first_movers,efficient_producers,sK1,sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1021,plain,
( ~ environment(sK1)
| ~ subpopulations(first_movers,efficient_producers,sK1,sK2)
| in_environment(sK1,sK2) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1064,plain,
subpopulations(first_movers,efficient_producers,sK1,sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1020,plain,
( ~ greater_or_equal(sK2,equilibrium(sK1))
| ~ greater(equilibrium(sK1),sK2)
| ~ environment(sK1) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l58,plain,
subpopulations(first_movers,efficient_producers,sK1,sK2),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1072,plain,
environment(sK1),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1026,plain,
greater_or_equal(sK2,equilibrium(sK1)),
inference(instantiation,[status(thm)],[15]) ).
cnf(l80,plain,
environment(sK1),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1023,plain,
environment(sK1),
inference(instantiation,[status(thm)],[13]) ).
cnf(l993,plain,
( ~ greater(growth_rate(efficient_producers,sK2),zero)
| ~ greater(zero,growth_rate(first_movers,sK2)) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1054,plain,
environment(sK1),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1040,plain,
( greater(growth_rate(efficient_producers,sK2),zero)
| ~ sP1(sK2) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l368,l2,l3,l145,l12,l150,l147,l6,l162,l876,l593,l4,l608,l200,l47,l163,l987,l201,l878,l884,l179,l8,l879,l877,l944,l994,l53,l990,l210,l847,l946,l945,l953,l1013,l1041,l51,l989,l1050,l1021,l1064,l1020,l58,l1072,l1026,l80,l1023,l993,l1054,l1040]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT024+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n029.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:10:12 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % launching worker at depth: 1
% 0.09/0.37 % launching worker at depth: 2
% 0.09/0.37 % launching worker at depth: 8
% 0.09/0.37 % launching worker at depth: 4
% 0.09/0.37 % launching worker at depth: 3
% 0.09/0.37 % launching worker at depth: 6
% 0.09/0.37 % launching worker at depth: 5
% 0.09/0.37 % launching worker at depth: 7
% 0.09/0.37 % launching worker at depth: 9
% 0.09/0.37 % launching worker at depth: 10
% 0.09/0.39 % launching worker at depth: 11
% 0.86/0.48 % launching worker at depth: 12
% 22.56/3.25 % SZS status Theorem for theBenchmark
% 22.56/3.25 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------