%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : MGT037+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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 : Sun Sep 27 08:02:54 AM UTC 2026
% Result : Theorem 0.09s 0.39s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 16
% Syntax : Number of formulae : 120 ( 21 unt; 0 def)
% Number of atoms : 386 ( 74 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 428 ( 162 ~; 191 |; 55 &)
% ( 0 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-2 aty)
% Number of variables : 129 ( 0 sgn 57 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mp_previous_negative_growth,axiom,
! [E,T] :
( ( cardinality_at_time(efficient_producers,T) = zero
& greater_or_equal(T,appear(efficient_producers,E))
& environment(E) )
=> ? [To] :
( greater(zero,growth_rate(efficient_producers,To))
& greater(T,To)
& in_environment(E,To)
& greater(To,appear(efficient_producers,E)) ) ),
file('theBenchmark.p',mp_previous_negative_growth) ).
fof(mp_start_of_organizations,axiom,
! [E,T] :
( ( greater(appear(an_organisation,E),T)
& in_environment(E,T)
& environment(E) )
=> number_of_organizations(E,T) = zero ),
file('theBenchmark.p',mp_start_of_organizations) ).
fof(mp_non_decreasing,axiom,
! [E,T] :
( ( ~ decreases(number_of_organizations(E,T))
& in_environment(E,T)
& environment(E) )
=> ? [X] :
( ~ greater(zero,growth_rate(X,T))
& greater(cardinality_at_time(X,T),zero)
& subpopulation(X,E,T) ) ),
file('theBenchmark.p',mp_non_decreasing) ).
fof(mp_no_members,axiom,
! [E,T,X] :
( ( subpopulation(X,E,T)
& number_of_organizations(E,T) = zero
& in_environment(E,T)
& environment(E) )
=> cardinality_at_time(X,T) = zero ),
file('theBenchmark.p',mp_no_members) ).
fof(mp_subpopulations,axiom,
! [E,T] :
( ( in_environment(E,T)
& environment(E) )
=> ( subpopulation(efficient_producers,E,T)
& subpopulation(first_movers,E,T) ) ),
file('theBenchmark.p',mp_subpopulations) ).
fof(mp_empty_not_decreasing,axiom,
! [S,T] :
( cardinality_at_time(S,T) = zero
=> ~ greater(zero,growth_rate(S,T)) ),
file('theBenchmark.p',mp_empty_not_decreasing) ).
fof(mp_efficient_producers_exist,axiom,
! [E,T] :
( ( in_environment(E,T)
& environment(E) )
=> ( greater(cardinality_at_time(efficient_producers,T),zero)
| cardinality_at_time(efficient_producers,T) = zero ) ),
file('theBenchmark.p',mp_efficient_producers_exist) ).
fof(mp_constant_not_decrease,axiom,
! [X] :
( constant(X)
=> ~ decreases(X) ),
file('theBenchmark.p',mp_constant_not_decrease) ).
fof(mp_environment_inequality,axiom,
! [E,T] :
( ( in_environment(E,T)
& environment(E) )
=> ( greater(appear(an_organisation,E),T)
| greater_or_equal(T,appear(an_organisation,E)) ) ),
file('theBenchmark.p',mp_environment_inequality) ).
fof(a3,axiom,
! [E,T] :
( ( greater(number_of_organizations(E,T),zero)
& in_environment(E,T)
& environment(E) )
=> ( ( ~ greater(equilibrium(E),T)
=> constant(resources(E,T)) )
& ( greater(equilibrium(E),T)
=> decreases(resources(E,T)) ) ) ),
file('theBenchmark.p',a3) ).
fof(a1,axiom,
! [E,T] :
( ( greater_or_equal(T,appear(an_organisation,E))
& in_environment(E,T)
& environment(E) )
=> greater(number_of_organizations(E,T),zero) ),
file('theBenchmark.p',a1) ).
fof(a6,axiom,
! [E,T] :
( ( in_environment(E,T)
& environment(E) )
=> ( ( constant(resources(E,T))
=> constant(number_of_organizations(E,T)) )
& ( decreases(resources(E,T))
=> ~ decreases(number_of_organizations(E,T)) ) ) ),
file('theBenchmark.p',a6) ).
fof(a12,axiom,
! [E,S1,S2,T] :
( ( greater(resilience(S2),resilience(S1))
& ~ greater(zero,growth_rate(S1,T))
& in_environment(E,T)
& environment(E) )
=> ~ greater(zero,growth_rate(S2,T)) ),
file('theBenchmark.p',a12) ).
fof(a9,axiom,
! [E,X,T] :
( ( greater(cardinality_at_time(X,T),zero)
& subpopulation(X,E,T)
& environment(E) )
=> ( X = first_movers
| X = efficient_producers ) ),
file('theBenchmark.p',a9) ).
fof(prove_t6,conjecture,
! [E,T] :
( ( greater_or_equal(T,appear(efficient_producers,E))
& in_environment(E,T)
& environment(E) )
=> greater(cardinality_at_time(efficient_producers,T),zero) ),
file('theBenchmark.p',prove_t6) ).
fof(prove_t6_neg,negated_conjecture,
~ ! [E,T] :
( ( greater_or_equal(T,appear(efficient_producers,E))
& in_environment(E,T)
& environment(E) )
=> greater(cardinality_at_time(efficient_producers,T),zero) ),
inference(assume_negation,[status(cth)],[prove_t6]) ).
fof(nnf_15,plain,
? [E,T] :
( ~ greater(cardinality_at_time(efficient_producers,T),zero)
& greater_or_equal(T,appear(efficient_producers,E))
& in_environment(E,T)
& environment(E) ),
inference(fof_nnf,[status(thm)],[prove_t6_neg]) ).
fof(sk_prove_t6_neg,plain,
( ~ greater(cardinality_at_time(efficient_producers,sK3),zero)
& greater_or_equal(sK3,appear(efficient_producers,sK0))
& in_environment(sK0,sK3)
& environment(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK3]),skolemize(E,sK0),skolemize(T,sK3)],[nnf_15]) ).
cnf(c_16,negated_conjecture,
environment(sK0),
inference(split_conjunct,[status(thm)],[sk_prove_t6_neg]) ).
cnf(c_17,plain,
( first_movers = B
| B = efficient_producers
| ~ greater(cardinality_at_time(B,C),zero)
| ~ subpopulation(B,A,C)
| ~ environment(A) ),
inference(clausify,[status(thm)],[a9]) ).
cnf(c_18,plain,
( ~ greater(zero,growth_rate(D,B))
| ~ greater(resilience(D),resilience(C))
| greater(zero,growth_rate(C,B))
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[a12]) ).
cnf(c_19,plain,
( constant(number_of_organizations(A,B))
| ~ constant(resources(A,B))
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[a6]) ).
cnf(c_20,plain,
( ~ decreases(number_of_organizations(A,B))
| ~ decreases(resources(A,B))
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[a6]) ).
cnf(c_21,plain,
( greater(number_of_organizations(A,B),zero)
| ~ greater_or_equal(B,appear(an_organisation,A))
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[a1]) ).
cnf(c_22,plain,
( constant(resources(A,B))
| greater(equilibrium(A),B)
| ~ greater(number_of_organizations(A,B),zero)
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[a3]) ).
cnf(c_23,plain,
( decreases(resources(A,B))
| ~ greater(equilibrium(A),B)
| ~ greater(number_of_organizations(A,B),zero)
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[a3]) ).
cnf(c_24,plain,
( greater(appear(an_organisation,A),B)
| greater_or_equal(B,appear(an_organisation,A))
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[mp_environment_inequality]) ).
cnf(c_25,plain,
( greater(cardinality_at_time(efficient_producers,B),zero)
| cardinality_at_time(efficient_producers,B) = zero
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[mp_efficient_producers_exist]) ).
cnf(c_26,plain,
( subpopulation(efficient_producers,A,B)
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[mp_subpopulations]) ).
cnf(c_28,plain,
( cardinality_at_time(C,B) = zero
| ~ subpopulation(C,A,B)
| number_of_organizations(A,B) != zero
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[mp_no_members]) ).
fof(nnf_3,plain,
! [E,T] :
( ? [X] :
( ~ greater(zero,growth_rate(X,T))
& greater(cardinality_at_time(X,T),zero)
& subpopulation(X,E,T) )
| decreases(number_of_organizations(E,T))
| ~ in_environment(E,T)
| ~ environment(E) ),
inference(fof_nnf,[status(thm)],[mp_non_decreasing]) ).
fof(sk_mp_non_decreasing_sk,plain,
! [E,T] :
( ( ~ greater(zero,growth_rate(sK1(E,T),T))
& greater(cardinality_at_time(sK1(E,T),T),zero)
& subpopulation(sK1(E,T),E,T) )
| decreases(number_of_organizations(E,T))
| ~ in_environment(E,T)
| ~ environment(E) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X,sK1(E,T))],[nnf_3]) ).
fof(sk_mp_non_decreasing,plain,
( ! [VAR_0,VAR_1] :
( ~ greater(zero,growth_rate(sK1(VAR_0,VAR_1),VAR_1))
| decreases(number_of_organizations(VAR_0,VAR_1))
| ~ in_environment(VAR_0,VAR_1)
| ~ environment(VAR_0) )
& ! [VAR_0,VAR_1] :
( greater(cardinality_at_time(sK1(VAR_0,VAR_1),VAR_1),zero)
| decreases(number_of_organizations(VAR_0,VAR_1))
| ~ in_environment(VAR_0,VAR_1)
| ~ environment(VAR_0) )
& ! [VAR_0,VAR_1] :
( subpopulation(sK1(VAR_0,VAR_1),VAR_0,VAR_1)
| decreases(number_of_organizations(VAR_0,VAR_1))
| ~ in_environment(VAR_0,VAR_1)
| ~ environment(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_mp_non_decreasing_sk]) ).
cnf(c_29,plain,
( ~ greater(zero,growth_rate(sK1(A,B),B))
| decreases(number_of_organizations(A,B))
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(split_conjunct,[status(thm)],[sk_mp_non_decreasing]) ).
cnf(c_30,plain,
( greater(cardinality_at_time(sK1(A,B),B),zero)
| decreases(number_of_organizations(A,B))
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(split_conjunct,[status(thm)],[sk_mp_non_decreasing]) ).
cnf(c_31,plain,
( subpopulation(sK1(A,B),A,B)
| decreases(number_of_organizations(A,B))
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(split_conjunct,[status(thm)],[sk_mp_non_decreasing]) ).
cnf(c_32,plain,
( number_of_organizations(A,B) = zero
| ~ greater(appear(an_organisation,A),B)
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[mp_start_of_organizations]) ).
fof(nnf_1,plain,
! [E,T] :
( ? [To] :
( greater(zero,growth_rate(efficient_producers,To))
& greater(T,To)
& in_environment(E,To)
& greater(To,appear(efficient_producers,E)) )
| cardinality_at_time(efficient_producers,T) != zero
| ~ greater_or_equal(T,appear(efficient_producers,E))
| ~ environment(E) ),
inference(fof_nnf,[status(thm)],[mp_previous_negative_growth]) ).
fof(sk_mp_previous_negative_growth_sk,plain,
! [E,T] :
( ( greater(zero,growth_rate(efficient_producers,sK2(E,T)))
& greater(T,sK2(E,T))
& in_environment(E,sK2(E,T))
& greater(sK2(E,T),appear(efficient_producers,E)) )
| cardinality_at_time(efficient_producers,T) != zero
| ~ greater_or_equal(T,appear(efficient_producers,E))
| ~ environment(E) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(To,sK2(E,T))],[nnf_1]) ).
fof(sk_mp_previous_negative_growth,plain,
( ! [VAR_0,VAR_1] :
( greater(zero,growth_rate(efficient_producers,sK2(VAR_0,VAR_1)))
| cardinality_at_time(efficient_producers,VAR_1) != zero
| ~ greater_or_equal(VAR_1,appear(efficient_producers,VAR_0))
| ~ environment(VAR_0) )
& ! [VAR_0,VAR_1] :
( greater(VAR_1,sK2(VAR_0,VAR_1))
| cardinality_at_time(efficient_producers,VAR_1) != zero
| ~ greater_or_equal(VAR_1,appear(efficient_producers,VAR_0))
| ~ environment(VAR_0) )
& ! [VAR_0,VAR_1] :
( in_environment(VAR_0,sK2(VAR_0,VAR_1))
| cardinality_at_time(efficient_producers,VAR_1) != zero
| ~ greater_or_equal(VAR_1,appear(efficient_producers,VAR_0))
| ~ environment(VAR_0) )
& ! [VAR_0,VAR_1] :
( greater(sK2(VAR_0,VAR_1),appear(efficient_producers,VAR_0))
| cardinality_at_time(efficient_producers,VAR_1) != zero
| ~ greater_or_equal(VAR_1,appear(efficient_producers,VAR_0))
| ~ environment(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_mp_previous_negative_growth_sk]) ).
cnf(c_33,plain,
( greater(zero,growth_rate(efficient_producers,sK2(A,B)))
| cardinality_at_time(efficient_producers,B) != zero
| ~ greater_or_equal(B,appear(efficient_producers,A))
| ~ environment(A) ),
inference(split_conjunct,[status(thm)],[sk_mp_previous_negative_growth]) ).
cnf(c_35,plain,
( in_environment(A,sK2(A,B))
| cardinality_at_time(efficient_producers,B) != zero
| ~ greater_or_equal(B,appear(efficient_producers,A))
| ~ environment(A) ),
inference(split_conjunct,[status(thm)],[sk_mp_previous_negative_growth]) ).
cnf(c_38,negated_conjecture,
( in_environment(sK0,sK2(sK0,A))
| cardinality_at_time(efficient_producers,A) != zero
| ~ greater_or_equal(A,appear(efficient_producers,sK0)) ),
inference(resolve,[status(thm)],[c_16,c_35]) ).
cnf(c_40,negated_conjecture,
( greater(zero,growth_rate(efficient_producers,sK2(sK0,A)))
| cardinality_at_time(efficient_producers,A) != zero
| ~ greater_or_equal(A,appear(efficient_producers,sK0)) ),
inference(resolve,[status(thm)],[c_16,c_33]) ).
cnf(c_41,negated_conjecture,
( number_of_organizations(sK0,A) = zero
| ~ greater(appear(an_organisation,sK0),A)
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_16,c_32]) ).
cnf(c_42,negated_conjecture,
( subpopulation(sK1(sK0,A),sK0,A)
| decreases(number_of_organizations(sK0,A))
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_16,c_31]) ).
cnf(c_43,negated_conjecture,
( greater(cardinality_at_time(sK1(sK0,A),A),zero)
| decreases(number_of_organizations(sK0,A))
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_16,c_30]) ).
cnf(c_44,negated_conjecture,
( ~ greater(zero,growth_rate(sK1(sK0,A),A))
| decreases(number_of_organizations(sK0,A))
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_16,c_29]) ).
cnf(c_45,negated_conjecture,
( cardinality_at_time(B,A) = zero
| ~ subpopulation(B,sK0,A)
| number_of_organizations(sK0,A) != zero
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_16,c_28]) ).
cnf(c_47,negated_conjecture,
( subpopulation(efficient_producers,sK0,A)
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_16,c_26]) ).
cnf(c_48,negated_conjecture,
( greater(cardinality_at_time(efficient_producers,A),zero)
| cardinality_at_time(efficient_producers,A) = zero
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_16,c_25]) ).
cnf(c_49,negated_conjecture,
( greater(appear(an_organisation,sK0),A)
| greater_or_equal(A,appear(an_organisation,sK0))
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_16,c_24]) ).
cnf(c_50,negated_conjecture,
( decreases(resources(sK0,A))
| ~ greater(equilibrium(sK0),A)
| ~ greater(number_of_organizations(sK0,A),zero)
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_16,c_23]) ).
cnf(c_51,negated_conjecture,
( constant(resources(sK0,A))
| greater(equilibrium(sK0),A)
| ~ greater(number_of_organizations(sK0,A),zero)
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_16,c_22]) ).
cnf(c_52,negated_conjecture,
( greater(number_of_organizations(sK0,A),zero)
| ~ greater_or_equal(A,appear(an_organisation,sK0))
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_16,c_21]) ).
cnf(c_53,negated_conjecture,
( ~ decreases(number_of_organizations(sK0,A))
| ~ decreases(resources(sK0,A))
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_16,c_20]) ).
cnf(c_54,negated_conjecture,
( constant(number_of_organizations(sK0,A))
| ~ constant(resources(sK0,A))
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_16,c_19]) ).
cnf(c_55,negated_conjecture,
( ~ greater(zero,growth_rate(C,A))
| ~ greater(resilience(C),resilience(B))
| greater(zero,growth_rate(B,A))
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_16,c_18]) ).
cnf(c_56,negated_conjecture,
( first_movers = A
| A = efficient_producers
| ~ greater(cardinality_at_time(A,B),zero)
| ~ subpopulation(A,sK0,B) ),
inference(resolve,[status(thm)],[c_16,c_17]) ).
cnf(c_57,negated_conjecture,
( first_movers = A
| efficient_producers = A
| ~ greater(cardinality_at_time(A,B),zero)
| ~ subpopulation(A,sK0,B) ),
inference(copy,[status(thm)],[c_56]) ).
cnf(c_58,negated_conjecture,
~ greater(cardinality_at_time(efficient_producers,sK3),zero),
inference(split_conjunct,[status(thm)],[sk_prove_t6_neg]) ).
cnf(c_59,negated_conjecture,
greater_or_equal(sK3,appear(efficient_producers,sK0)),
inference(split_conjunct,[status(thm)],[sk_prove_t6_neg]) ).
cnf(c_60,negated_conjecture,
in_environment(sK0,sK3),
inference(split_conjunct,[status(thm)],[sk_prove_t6_neg]) ).
fof(a2,axiom,
greater(resilience(efficient_producers),resilience(first_movers)),
file('theBenchmark.p',a2) ).
cnf(c_61,plain,
greater(resilience(efficient_producers),resilience(first_movers)),
inference(clausify,[status(thm)],[a2]) ).
cnf(c_62,plain,
( ~ decreases(A)
| ~ constant(A) ),
inference(clausify,[status(thm)],[mp_constant_not_decrease]) ).
cnf(c_63,plain,
( ~ greater(zero,growth_rate(A,B))
| cardinality_at_time(A,B) != zero ),
inference(clausify,[status(thm)],[mp_empty_not_decreasing]) ).
cnf(c_64,plain,
( greater(zero,growth_rate(efficient_producers,sK2(sK0,sK3)))
| cardinality_at_time(efficient_producers,sK3) != zero ),
inference(resolve,[status(thm)],[c_59,c_40]) ).
cnf(c_66,plain,
( in_environment(sK0,sK2(sK0,sK3))
| cardinality_at_time(efficient_producers,sK3) != zero ),
inference(resolve,[status(thm)],[c_59,c_38]) ).
cnf(c_144,negated_conjecture,
( greater(cardinality_at_time(efficient_producers,sK3),zero)
| cardinality_at_time(efficient_producers,sK3) = zero ),
inference(resolve,[status(thm)],[c_60,c_48]) ).
cnf(c_74,negated_conjecture,
cardinality_at_time(efficient_producers,sK3) = zero,
inference(resolve,[status(thm)],[c_58,c_144]) ).
cnf(c_82,plain,
in_environment(sK0,sK2(sK0,sK3)),
inference(resolve,[status(thm)],[c_74,c_66]) ).
cnf(c_84,plain,
greater(zero,growth_rate(efficient_producers,sK2(sK0,sK3))),
inference(resolve,[status(thm)],[c_74,c_64]) ).
cnf(c_89,plain,
( ~ greater(zero,growth_rate(B,sK2(sK0,sK3)))
| ~ greater(resilience(B),resilience(A))
| greater(zero,growth_rate(A,sK2(sK0,sK3))) ),
inference(resolve,[status(thm)],[c_82,c_55]) ).
cnf(c_90,plain,
( constant(number_of_organizations(sK0,sK2(sK0,sK3)))
| ~ constant(resources(sK0,sK2(sK0,sK3))) ),
inference(resolve,[status(thm)],[c_82,c_54]) ).
cnf(c_91,plain,
( ~ decreases(number_of_organizations(sK0,sK2(sK0,sK3)))
| ~ decreases(resources(sK0,sK2(sK0,sK3))) ),
inference(resolve,[status(thm)],[c_82,c_53]) ).
cnf(c_92,plain,
( constant(resources(sK0,sK2(sK0,sK3)))
| greater(equilibrium(sK0),sK2(sK0,sK3))
| ~ greater(number_of_organizations(sK0,sK2(sK0,sK3)),zero) ),
inference(resolve,[status(thm)],[c_82,c_51]) ).
cnf(c_93,plain,
( decreases(resources(sK0,sK2(sK0,sK3)))
| ~ greater(equilibrium(sK0),sK2(sK0,sK3))
| ~ greater(number_of_organizations(sK0,sK2(sK0,sK3)),zero) ),
inference(resolve,[status(thm)],[c_82,c_50]) ).
cnf(c_94,plain,
( greater(appear(an_organisation,sK0),sK2(sK0,sK3))
| greater_or_equal(sK2(sK0,sK3),appear(an_organisation,sK0)) ),
inference(resolve,[status(thm)],[c_82,c_49]) ).
cnf(c_96,plain,
subpopulation(efficient_producers,sK0,sK2(sK0,sK3)),
inference(resolve,[status(thm)],[c_82,c_47]) ).
cnf(c_98,plain,
( ~ greater(zero,growth_rate(sK1(sK0,sK2(sK0,sK3)),sK2(sK0,sK3)))
| decreases(number_of_organizations(sK0,sK2(sK0,sK3))) ),
inference(resolve,[status(thm)],[c_82,c_44]) ).
cnf(c_99,plain,
( greater(cardinality_at_time(sK1(sK0,sK2(sK0,sK3)),sK2(sK0,sK3)),zero)
| decreases(number_of_organizations(sK0,sK2(sK0,sK3))) ),
inference(resolve,[status(thm)],[c_82,c_43]) ).
cnf(c_100,plain,
( subpopulation(sK1(sK0,sK2(sK0,sK3)),sK0,sK2(sK0,sK3))
| decreases(number_of_organizations(sK0,sK2(sK0,sK3))) ),
inference(resolve,[status(thm)],[c_82,c_42]) ).
cnf(c_101,plain,
( number_of_organizations(sK0,sK2(sK0,sK3)) = zero
| ~ greater(appear(an_organisation,sK0),sK2(sK0,sK3)) ),
inference(resolve,[status(thm)],[c_82,c_41]) ).
cnf(c_145,negated_conjecture,
( cardinality_at_time(efficient_producers,sK2(sK0,sK3)) = zero
| number_of_organizations(sK0,sK2(sK0,sK3)) != zero
| ~ in_environment(sK0,sK2(sK0,sK3)) ),
inference(resolve,[status(thm)],[c_96,c_45]) ).
cnf(c_103,negated_conjecture,
( cardinality_at_time(efficient_producers,sK2(sK0,sK3)) = zero
| number_of_organizations(sK0,sK2(sK0,sK3)) != zero ),
inference(resolve,[status(thm)],[c_82,c_145]) ).
cnf(c_107,plain,
cardinality_at_time(efficient_producers,sK2(sK0,sK3)) != zero,
inference(resolve,[status(thm)],[c_84,c_63]) ).
cnf(c_108,negated_conjecture,
number_of_organizations(sK0,sK2(sK0,sK3)) != zero,
inference(resolve,[status(thm)],[c_107,c_103]) ).
cnf(c_110,plain,
~ greater(appear(an_organisation,sK0),sK2(sK0,sK3)),
inference(resolve,[status(thm)],[c_108,c_101]) ).
cnf(c_111,plain,
greater_or_equal(sK2(sK0,sK3),appear(an_organisation,sK0)),
inference(resolve,[status(thm)],[c_110,c_94]) ).
cnf(c_146,negated_conjecture,
( greater(number_of_organizations(sK0,sK2(sK0,sK3)),zero)
| ~ in_environment(sK0,sK2(sK0,sK3)) ),
inference(resolve,[status(thm)],[c_111,c_52]) ).
cnf(c_112,negated_conjecture,
greater(number_of_organizations(sK0,sK2(sK0,sK3)),zero),
inference(resolve,[status(thm)],[c_82,c_146]) ).
cnf(c_113,plain,
( decreases(resources(sK0,sK2(sK0,sK3)))
| ~ greater(equilibrium(sK0),sK2(sK0,sK3)) ),
inference(resolve,[status(thm)],[c_112,c_93]) ).
cnf(c_114,plain,
( constant(resources(sK0,sK2(sK0,sK3)))
| greater(equilibrium(sK0),sK2(sK0,sK3)) ),
inference(resolve,[status(thm)],[c_112,c_92]) ).
cnf(c_147,plain,
( ~ greater(zero,growth_rate(efficient_producers,sK2(sK0,sK3)))
| greater(zero,growth_rate(first_movers,sK2(sK0,sK3))) ),
inference(resolve,[status(thm)],[c_89,c_61]) ).
cnf(c_117,plain,
greater(zero,growth_rate(first_movers,sK2(sK0,sK3))),
inference(resolve,[status(thm)],[c_84,c_147]) ).
cnf(c_119,plain,
( decreases(resources(sK0,sK2(sK0,sK3)))
| constant(resources(sK0,sK2(sK0,sK3))) ),
inference(resolve,[status(thm)],[c_114,c_113]) ).
cnf(c_120,plain,
( constant(number_of_organizations(sK0,sK2(sK0,sK3)))
| decreases(resources(sK0,sK2(sK0,sK3))) ),
inference(resolve,[status(thm)],[c_119,c_90]) ).
cnf(c_121,plain,
( ~ decreases(number_of_organizations(sK0,sK2(sK0,sK3)))
| decreases(resources(sK0,sK2(sK0,sK3))) ),
inference(resolve,[status(thm)],[c_120,c_62]) ).
cnf(c_148,negated_conjecture,
( first_movers = sK1(sK0,sK2(sK0,sK3))
| efficient_producers = sK1(sK0,sK2(sK0,sK3))
| ~ greater(cardinality_at_time(sK1(sK0,sK2(sK0,sK3)),sK2(sK0,sK3)),zero)
| decreases(number_of_organizations(sK0,sK2(sK0,sK3))) ),
inference(resolve,[status(thm)],[c_100,c_57]) ).
cnf(c_149,negated_conjecture,
( first_movers = sK1(sK0,sK2(sK0,sK3))
| sK1(sK0,sK2(sK0,sK3)) = efficient_producers
| ~ greater(cardinality_at_time(sK1(sK0,sK2(sK0,sK3)),sK2(sK0,sK3)),zero)
| decreases(number_of_organizations(sK0,sK2(sK0,sK3))) ),
inference(copy,[status(thm)],[c_148]) ).
cnf(c_122,negated_conjecture,
( sK1(sK0,sK2(sK0,sK3)) = first_movers
| sK1(sK0,sK2(sK0,sK3)) = efficient_producers
| ~ greater(cardinality_at_time(sK1(sK0,sK2(sK0,sK3)),sK2(sK0,sK3)),zero)
| decreases(number_of_organizations(sK0,sK2(sK0,sK3))) ),
inference(copy,[status(thm)],[c_149]) ).
cnf(c_150,plain,
( decreases(number_of_organizations(sK0,sK2(sK0,sK3)))
| sK1(sK0,sK2(sK0,sK3)) = first_movers
| sK1(sK0,sK2(sK0,sK3)) = efficient_producers
| decreases(number_of_organizations(sK0,sK2(sK0,sK3))) ),
inference(resolve,[status(thm)],[c_122,c_99]) ).
cnf(c_128,plain,
( sK1(sK0,sK2(sK0,sK3)) = first_movers
| sK1(sK0,sK2(sK0,sK3)) = efficient_producers
| decreases(number_of_organizations(sK0,sK2(sK0,sK3))) ),
inference(copy,[status(thm)],[c_150]) ).
cnf(c_130,plain,
( decreases(resources(sK0,sK2(sK0,sK3)))
| sK1(sK0,sK2(sK0,sK3)) = first_movers
| sK1(sK0,sK2(sK0,sK3)) = efficient_producers ),
inference(resolve,[status(thm)],[c_128,c_121]) ).
cnf(c_135,plain,
( ~ decreases(number_of_organizations(sK0,sK2(sK0,sK3)))
| sK1(sK0,sK2(sK0,sK3)) = first_movers
| sK1(sK0,sK2(sK0,sK3)) = efficient_producers ),
inference(resolve,[status(thm)],[c_130,c_91]) ).
cnf(c_151,plain,
( sK1(sK0,sK2(sK0,sK3)) = first_movers
| sK1(sK0,sK2(sK0,sK3)) = efficient_producers
| sK1(sK0,sK2(sK0,sK3)) = first_movers
| sK1(sK0,sK2(sK0,sK3)) = efficient_producers ),
inference(resolve,[status(thm)],[c_135,c_128]) ).
cnf(c_152,plain,
( sK1(sK0,sK2(sK0,sK3)) = first_movers
| sK1(sK0,sK2(sK0,sK3)) = first_movers
| sK1(sK0,sK2(sK0,sK3)) = efficient_producers ),
inference(copy,[status(thm)],[c_151]) ).
cnf(c_136,plain,
( sK1(sK0,sK2(sK0,sK3)) = first_movers
| sK1(sK0,sK2(sK0,sK3)) = efficient_producers ),
inference(copy,[status(thm)],[c_152]) ).
cnf(c_153,plain,
( ~ greater(zero,growth_rate(first_movers,sK2(sK0,sK3)))
| decreases(number_of_organizations(sK0,sK2(sK0,sK3)))
| sK1(sK0,sK2(sK0,sK3)) = efficient_producers ),
inference(paramod,[status(thm)],[c_136,c_98]) ).
cnf(c_137,plain,
( decreases(number_of_organizations(sK0,sK2(sK0,sK3)))
| sK1(sK0,sK2(sK0,sK3)) = efficient_producers ),
inference(resolve,[status(thm)],[c_117,c_153]) ).
cnf(c_138,plain,
( decreases(resources(sK0,sK2(sK0,sK3)))
| sK1(sK0,sK2(sK0,sK3)) = efficient_producers ),
inference(resolve,[status(thm)],[c_137,c_121]) ).
cnf(c_139,plain,
( ~ decreases(number_of_organizations(sK0,sK2(sK0,sK3)))
| sK1(sK0,sK2(sK0,sK3)) = efficient_producers ),
inference(resolve,[status(thm)],[c_138,c_91]) ).
cnf(c_154,plain,
( sK1(sK0,sK2(sK0,sK3)) = efficient_producers
| sK1(sK0,sK2(sK0,sK3)) = efficient_producers ),
inference(resolve,[status(thm)],[c_139,c_137]) ).
cnf(c_140,plain,
sK1(sK0,sK2(sK0,sK3)) = efficient_producers,
inference(copy,[status(thm)],[c_154]) ).
cnf(c_155,plain,
( ~ greater(zero,growth_rate(efficient_producers,sK2(sK0,sK3)))
| decreases(number_of_organizations(sK0,sK2(sK0,sK3))) ),
inference(paramod,[status(thm)],[c_140,c_98]) ).
cnf(c_141,plain,
decreases(number_of_organizations(sK0,sK2(sK0,sK3))),
inference(resolve,[status(thm)],[c_84,c_155]) ).
cnf(c_142,plain,
decreases(resources(sK0,sK2(sK0,sK3))),
inference(resolve,[status(thm)],[c_141,c_121]) ).
cnf(c_156,plain,
~ decreases(number_of_organizations(sK0,sK2(sK0,sK3))),
inference(resolve,[status(thm)],[c_142,c_91]) ).
cnf(c_143,plain,
$false,
inference(resolve,[status(thm)],[c_141,c_156]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT037+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n005.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 : Sat Sep 26 00:07:31 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 609456 was started by sandbox2 on n005,
% 0.09/0.37 % Sat Sep 26 00:07:31 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.38
% 0.09/0.38 % From the command line: assign(max_seconds, 300).
% 0.09/0.39
% 0.09/0.39 % SZS status Theorem for theBenchmark
% 0.09/0.39
% 0.09/0.39 % Proof 1 at 0.00 (+ 0.00) seconds.
% 0.09/0.39 % Length of proof is 97.
% 0.09/0.39 % Level of proof is 24.
% 0.09/0.39 % Maximum clause weight is 51.000.
% 0.09/0.39 % Given clauses 91.
% 0.09/0.39
% 0.09/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------