%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT037+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n001.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:04:32 AM UTC 2026
% Result : Theorem 0.25s 0.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT037+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.34 % Computer : n001.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 7 12:48:22 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.14/0.46 start to proof:theBenchmark.p
% 0.25/0.52 % Version : CSI_E---1.1
% 0.25/0.52 % Problem : theBenchmark.p
% 0.25/0.52 % Proof found!
% 0.25/0.52 % SZS status Theorem for theBenchmark.p
% 0.25/0.52 % SZS output start Proof
% 0.25/0.52 fof(prove_t6, conjecture, ![X1, X2]:((((environment(X1)&in_environment(X1,X2))&greater_or_equal(X2,appear(efficient_producers,X1)))=>greater(cardinality_at_time(efficient_producers,X2),zero))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_t6)).
% 0.25/0.52 fof(mp_efficient_producers_exist, axiom, ![X1, X2]:(((environment(X1)&in_environment(X1,X2))=>(cardinality_at_time(efficient_producers,X2)=zero|greater(cardinality_at_time(efficient_producers,X2),zero)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_efficient_producers_exist)).
% 0.25/0.52 fof(mp_non_decreasing, axiom, ![X1, X2]:((((environment(X1)&in_environment(X1,X2))&~(decreases(number_of_organizations(X1,X2))))=>?[X4]:(((subpopulation(X4,X1,X2)&greater(cardinality_at_time(X4,X2),zero))&~(greater(zero,growth_rate(X4,X2))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_non_decreasing)).
% 0.25/0.52 fof(mp_previous_negative_growth, axiom, ![X1, X2]:((((environment(X1)&greater_or_equal(X2,appear(efficient_producers,X1)))&cardinality_at_time(efficient_producers,X2)=zero)=>?[X3]:((((greater(X3,appear(efficient_producers,X1))&in_environment(X1,X3))&greater(X2,X3))&greater(zero,growth_rate(efficient_producers,X3)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_previous_negative_growth)).
% 0.25/0.52 fof(a12, hypothesis, ![X1, X6, X7, X2]:(((((environment(X1)&in_environment(X1,X2))&~(greater(zero,growth_rate(X6,X2))))&greater(resilience(X7),resilience(X6)))=>~(greater(zero,growth_rate(X7,X2))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a12)).
% 0.25/0.52 fof(a9, hypothesis, ![X1, X4, X2]:((((environment(X1)&subpopulation(X4,X1,X2))&greater(cardinality_at_time(X4,X2),zero))=>(X4=efficient_producers|X4=first_movers))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a9)).
% 0.25/0.52 fof(a6, hypothesis, ![X1, X2]:(((environment(X1)&in_environment(X1,X2))=>((decreases(resources(X1,X2))=>~(decreases(number_of_organizations(X1,X2))))&(constant(resources(X1,X2))=>constant(number_of_organizations(X1,X2)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a6)).
% 0.25/0.52 fof(a2, hypothesis, greater(resilience(efficient_producers),resilience(first_movers)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a2)).
% 0.25/0.52 fof(a3, hypothesis, ![X1, X2]:((((environment(X1)&in_environment(X1,X2))&greater(number_of_organizations(X1,X2),zero))=>((greater(equilibrium(X1),X2)=>decreases(resources(X1,X2)))&(~(greater(equilibrium(X1),X2))=>constant(resources(X1,X2)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a3)).
% 0.25/0.52 fof(a1, hypothesis, ![X1, X2]:((((environment(X1)&in_environment(X1,X2))&greater_or_equal(X2,appear(an_organisation,X1)))=>greater(number_of_organizations(X1,X2),zero))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a1)).
% 0.25/0.52 fof(mp_environment_inequality, axiom, ![X1, X2]:(((environment(X1)&in_environment(X1,X2))=>(greater_or_equal(X2,appear(an_organisation,X1))|greater(appear(an_organisation,X1),X2)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_environment_inequality)).
% 0.25/0.52 fof(mp_subpopulations, axiom, ![X1, X2]:(((environment(X1)&in_environment(X1,X2))=>(subpopulation(first_movers,X1,X2)&subpopulation(efficient_producers,X1,X2)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_subpopulations)).
% 0.25/0.52 fof(mp_empty_not_decreasing, axiom, ![X5, X2]:((cardinality_at_time(X5,X2)=zero=>~(greater(zero,growth_rate(X5,X2))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_empty_not_decreasing)).
% 0.25/0.52 fof(mp_no_members, axiom, ![X1, X2, X4]:(((((environment(X1)&in_environment(X1,X2))&number_of_organizations(X1,X2)=zero)&subpopulation(X4,X1,X2))=>cardinality_at_time(X4,X2)=zero)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_no_members)).
% 0.25/0.52 fof(mp_start_of_organizations, axiom, ![X1, X2]:((((environment(X1)&in_environment(X1,X2))&greater(appear(an_organisation,X1),X2))=>number_of_organizations(X1,X2)=zero)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_start_of_organizations)).
% 0.25/0.52 fof(mp_constant_not_decrease, axiom, ![X4]:((constant(X4)=>~(decreases(X4)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_constant_not_decrease)).
% 0.25/0.52 fof(c_0_16, negated_conjecture, ~(![X1, X2]:((((environment(X1)&in_environment(X1,X2))&greater_or_equal(X2,appear(efficient_producers,X1)))=>greater(cardinality_at_time(efficient_producers,X2),zero)))), inference(assume_negation,[status(cth)],[prove_t6])).
% 0.25/0.52 fof(c_0_17, plain, ![X41, X42]:((~environment(X41)|~in_environment(X41,X42)|(cardinality_at_time(efficient_producers,X42)=zero|greater(cardinality_at_time(efficient_producers,X42),zero)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_efficient_producers_exist])])])).
% 0.25/0.52 fof(c_0_18, negated_conjecture, (((environment(esk1_0)&in_environment(esk1_0,esk2_0))&greater_or_equal(esk2_0,appear(efficient_producers,esk1_0)))&~greater(cardinality_at_time(efficient_producers,esk2_0),zero)), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_16])])])])).
% 0.25/0.52 fof(c_0_19, plain, ![X1, X2]:((((environment(X1)&in_environment(X1,X2))&~decreases(number_of_organizations(X1,X2)))=>?[X4]:(((subpopulation(X4,X1,X2)&greater(cardinality_at_time(X4,X2),zero))&~greater(zero,growth_rate(X4,X2)))))), inference(fof_simplification,[status(thm)],[mp_non_decreasing])).
% 0.25/0.52 fof(c_0_20, plain, ![X30, X31]:(((((greater(esk4_2(X30,X31),appear(efficient_producers,X30))|(~environment(X30)|~greater_or_equal(X31,appear(efficient_producers,X30))|cardinality_at_time(efficient_producers,X31)!=zero))&(in_environment(X30,esk4_2(X30,X31))|(~environment(X30)|~greater_or_equal(X31,appear(efficient_producers,X30))|cardinality_at_time(efficient_producers,X31)!=zero)))&(greater(X31,esk4_2(X30,X31))|(~environment(X30)|~greater_or_equal(X31,appear(efficient_producers,X30))|cardinality_at_time(efficient_producers,X31)!=zero)))&(greater(zero,growth_rate(efficient_producers,esk4_2(X30,X31)))|(~environment(X30)|~greater_or_equal(X31,appear(efficient_producers,X30))|cardinality_at_time(efficient_producers,X31)!=zero)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_previous_negative_growth])])])])])).
% 0.25/0.52 cnf(c_0_21, plain, (cardinality_at_time(efficient_producers,X2)=zero|greater(cardinality_at_time(efficient_producers,X2),zero)|~environment(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.25/0.52 cnf(c_0_22, negated_conjecture, (in_environment(esk1_0,esk2_0)), inference(split_conjunct,[status(thm)],[c_0_18])).
% 0.25/0.52 cnf(c_0_23, negated_conjecture, (environment(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_18])).
% 0.25/0.52 cnf(c_0_24, negated_conjecture, (~greater(cardinality_at_time(efficient_producers,esk2_0),zero)), inference(split_conjunct,[status(thm)],[c_0_18])).
% 0.25/0.52 fof(c_0_25, hypothesis, ![X1, X6, X7, X2]:(((((environment(X1)&in_environment(X1,X2))&~greater(zero,growth_rate(X6,X2)))&greater(resilience(X7),resilience(X6)))=>~greater(zero,growth_rate(X7,X2)))), inference(fof_simplification,[status(thm)],[a12])).
% 0.25/0.52 fof(c_0_26, hypothesis, ![X18, X19, X20]:((~environment(X18)|~subpopulation(X19,X18,X20)|~greater(cardinality_at_time(X19,X20),zero)|(X19=efficient_producers|X19=first_movers))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a9])])])).
% 0.25/0.52 fof(c_0_27, plain, ![X24, X25]:((((subpopulation(esk3_2(X24,X25),X24,X25)|(~environment(X24)|~in_environment(X24,X25)|decreases(number_of_organizations(X24,X25))))&(greater(cardinality_at_time(esk3_2(X24,X25),X25),zero)|(~environment(X24)|~in_environment(X24,X25)|decreases(number_of_organizations(X24,X25)))))&(~greater(zero,growth_rate(esk3_2(X24,X25),X25))|(~environment(X24)|~in_environment(X24,X25)|decreases(number_of_organizations(X24,X25)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_19])])])])])).
% 0.25/0.52 cnf(c_0_28, plain, (in_environment(X1,esk4_2(X1,X2))|~environment(X1)|~greater_or_equal(X2,appear(efficient_producers,X1))|cardinality_at_time(efficient_producers,X2)!=zero), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.25/0.52 cnf(c_0_29, negated_conjecture, (greater_or_equal(esk2_0,appear(efficient_producers,esk1_0))), inference(split_conjunct,[status(thm)],[c_0_18])).
% 0.25/0.52 cnf(c_0_30, negated_conjecture, (cardinality_at_time(efficient_producers,esk2_0)=zero), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_21, c_0_22]), c_0_23])]), c_0_24])).
% 0.25/0.52 fof(c_0_31, hypothesis, ![X14, X15, X16, X17]:((~environment(X14)|~in_environment(X14,X17)|greater(zero,growth_rate(X15,X17))|~greater(resilience(X16),resilience(X15))|~greater(zero,growth_rate(X16,X17)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_25])])])).
% 0.25/0.52 cnf(c_0_32, plain, (greater(zero,growth_rate(efficient_producers,esk4_2(X1,X2)))|~environment(X1)|~greater_or_equal(X2,appear(efficient_producers,X1))|cardinality_at_time(efficient_producers,X2)!=zero), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.25/0.52 cnf(c_0_33, hypothesis, (X2=efficient_producers|X2=first_movers|~environment(X1)|~subpopulation(X2,X1,X3)|~greater(cardinality_at_time(X2,X3),zero)), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.25/0.52 cnf(c_0_34, plain, (greater(cardinality_at_time(esk3_2(X1,X2),X2),zero)|decreases(number_of_organizations(X1,X2))|~environment(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.25/0.52 cnf(c_0_35, plain, (subpopulation(esk3_2(X1,X2),X1,X2)|decreases(number_of_organizations(X1,X2))|~environment(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.25/0.52 cnf(c_0_36, negated_conjecture, (in_environment(esk1_0,esk4_2(esk1_0,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_29]), c_0_23])]), c_0_30])])).
% 0.25/0.52 cnf(c_0_37, hypothesis, (greater(zero,growth_rate(X3,X2))|~environment(X1)|~in_environment(X1,X2)|~greater(resilience(X4),resilience(X3))|~greater(zero,growth_rate(X4,X2))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.25/0.52 cnf(c_0_38, negated_conjecture, (greater(zero,growth_rate(efficient_producers,esk4_2(esk1_0,esk2_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_29]), c_0_23])]), c_0_30])])).
% 0.25/0.52 fof(c_0_39, hypothesis, ![X1, X2]:(((environment(X1)&in_environment(X1,X2))=>((decreases(resources(X1,X2))=>~decreases(number_of_organizations(X1,X2)))&(constant(resources(X1,X2))=>constant(number_of_organizations(X1,X2)))))), inference(fof_simplification,[status(thm)],[a6])).
% 0.25/0.52 cnf(c_0_40, plain, (decreases(number_of_organizations(X1,X2))|~greater(zero,growth_rate(esk3_2(X1,X2),X2))|~environment(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.25/0.52 cnf(c_0_41, hypothesis, (esk3_2(X1,X2)=first_movers|esk3_2(X1,X2)=efficient_producers|decreases(number_of_organizations(X1,X2))|~subpopulation(esk3_2(X1,X2),X3,X2)|~in_environment(X1,X2)|~environment(X3)|~environment(X1)), inference(spm,[status(thm)],[c_0_33, c_0_34])).
% 0.25/0.52 cnf(c_0_42, negated_conjecture, (subpopulation(esk3_2(esk1_0,esk4_2(esk1_0,esk2_0)),esk1_0,esk4_2(esk1_0,esk2_0))|decreases(number_of_organizations(esk1_0,esk4_2(esk1_0,esk2_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_36]), c_0_23])])).
% 0.25/0.52 cnf(c_0_43, hypothesis, (greater(zero,growth_rate(X1,esk4_2(esk1_0,esk2_0)))|~in_environment(X2,esk4_2(esk1_0,esk2_0))|~greater(resilience(efficient_producers),resilience(X1))|~environment(X2)), inference(spm,[status(thm)],[c_0_37, c_0_38])).
% 0.25/0.52 fof(c_0_44, hypothesis, ![X12, X13]:(((~decreases(resources(X12,X13))|~decreases(number_of_organizations(X12,X13))|(~environment(X12)|~in_environment(X12,X13)))&(~constant(resources(X12,X13))|constant(number_of_organizations(X12,X13))|(~environment(X12)|~in_environment(X12,X13))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_39])])])])).
% 0.25/0.52 cnf(c_0_45, negated_conjecture, (decreases(number_of_organizations(esk1_0,esk4_2(esk1_0,esk2_0)))|~greater(zero,growth_rate(esk3_2(esk1_0,esk4_2(esk1_0,esk2_0)),esk4_2(esk1_0,esk2_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_36]), c_0_23])])).
% 0.25/0.52 cnf(c_0_46, hypothesis, (esk3_2(esk1_0,esk4_2(esk1_0,esk2_0))=efficient_producers|esk3_2(esk1_0,esk4_2(esk1_0,esk2_0))=first_movers|decreases(number_of_organizations(esk1_0,esk4_2(esk1_0,esk2_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_42]), c_0_36]), c_0_23])])).
% 0.25/0.52 cnf(c_0_47, negated_conjecture, (greater(zero,growth_rate(X1,esk4_2(esk1_0,esk2_0)))|~greater(resilience(efficient_producers),resilience(X1))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_36]), c_0_23])])).
% 0.25/0.52 cnf(c_0_48, hypothesis, (greater(resilience(efficient_producers),resilience(first_movers))), inference(split_conjunct,[status(thm)],[a2])).
% 0.25/0.52 fof(c_0_49, hypothesis, ![X1, X2]:((((environment(X1)&in_environment(X1,X2))&greater(number_of_organizations(X1,X2),zero))=>((greater(equilibrium(X1),X2)=>decreases(resources(X1,X2)))&(~greater(equilibrium(X1),X2)=>constant(resources(X1,X2)))))), inference(fof_simplification,[status(thm)],[a3])).
% 0.25/0.52 cnf(c_0_50, hypothesis, (~decreases(resources(X1,X2))|~decreases(number_of_organizations(X1,X2))|~environment(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_44])).
% 0.25/0.52 cnf(c_0_51, hypothesis, (esk3_2(esk1_0,esk4_2(esk1_0,esk2_0))=first_movers|decreases(number_of_organizations(esk1_0,esk4_2(esk1_0,esk2_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_46]), c_0_38])])).
% 0.25/0.52 cnf(c_0_52, hypothesis, (greater(zero,growth_rate(first_movers,esk4_2(esk1_0,esk2_0)))), inference(spm,[status(thm)],[c_0_47, c_0_48])).
% 0.25/0.52 fof(c_0_53, hypothesis, ![X10, X11]:((~environment(X10)|~in_environment(X10,X11)|~greater_or_equal(X11,appear(an_organisation,X10))|greater(number_of_organizations(X10,X11),zero))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a1])])])).
% 0.25/0.52 fof(c_0_54, plain, ![X33, X34]:((~environment(X33)|~in_environment(X33,X34)|(greater_or_equal(X34,appear(an_organisation,X33))|greater(appear(an_organisation,X33),X34)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_environment_inequality])])])).
% 0.25/0.52 fof(c_0_55, hypothesis, ![X8, X9]:(((~greater(equilibrium(X8),X9)|decreases(resources(X8,X9))|(~environment(X8)|~in_environment(X8,X9)|~greater(number_of_organizations(X8,X9),zero)))&(greater(equilibrium(X8),X9)|constant(resources(X8,X9))|(~environment(X8)|~in_environment(X8,X9)|~greater(number_of_organizations(X8,X9),zero))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_49])])])])).
% 0.25/0.52 cnf(c_0_56, hypothesis, (~decreases(number_of_organizations(esk1_0,esk4_2(esk1_0,esk2_0)))|~decreases(resources(esk1_0,esk4_2(esk1_0,esk2_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_36]), c_0_23])])).
% 0.25/0.52 cnf(c_0_57, negated_conjecture, (decreases(number_of_organizations(esk1_0,esk4_2(esk1_0,esk2_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_51]), c_0_52])])).
% 0.25/0.52 cnf(c_0_58, hypothesis, (greater(number_of_organizations(X1,X2),zero)|~environment(X1)|~in_environment(X1,X2)|~greater_or_equal(X2,appear(an_organisation,X1))), inference(split_conjunct,[status(thm)],[c_0_53])).
% 0.25/0.52 cnf(c_0_59, plain, (greater_or_equal(X2,appear(an_organisation,X1))|greater(appear(an_organisation,X1),X2)|~environment(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_54])).
% 0.25/0.52 fof(c_0_60, plain, ![X39, X40]:(((subpopulation(first_movers,X39,X40)|(~environment(X39)|~in_environment(X39,X40)))&(subpopulation(efficient_producers,X39,X40)|(~environment(X39)|~in_environment(X39,X40))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_subpopulations])])])])).
% 0.25/0.52 cnf(c_0_61, hypothesis, (decreases(resources(X1,X2))|~greater(equilibrium(X1),X2)|~environment(X1)|~in_environment(X1,X2)|~greater(number_of_organizations(X1,X2),zero)), inference(split_conjunct,[status(thm)],[c_0_55])).
% 0.25/0.52 cnf(c_0_62, hypothesis, (~decreases(resources(esk1_0,esk4_2(esk1_0,esk2_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_56, c_0_57])])).
% 0.25/0.52 cnf(c_0_63, hypothesis, (greater(appear(an_organisation,X1),X2)|greater(number_of_organizations(X1,X2),zero)|~in_environment(X1,X2)|~environment(X1)), inference(spm,[status(thm)],[c_0_58, c_0_59])).
% 0.25/0.52 fof(c_0_64, plain, ![X5, X2]:((cardinality_at_time(X5,X2)=zero=>~greater(zero,growth_rate(X5,X2)))), inference(fof_simplification,[status(thm)],[mp_empty_not_decreasing])).
% 0.25/0.52 fof(c_0_65, plain, ![X27, X28, X29]:((~environment(X27)|~in_environment(X27,X28)|number_of_organizations(X27,X28)!=zero|~subpopulation(X29,X27,X28)|cardinality_at_time(X29,X28)=zero)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_no_members])])])).
% 0.25/0.52 cnf(c_0_66, plain, (subpopulation(efficient_producers,X1,X2)|~environment(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_60])).
% 0.25/0.52 cnf(c_0_67, hypothesis, (greater(equilibrium(X1),X2)|constant(resources(X1,X2))|~environment(X1)|~in_environment(X1,X2)|~greater(number_of_organizations(X1,X2),zero)), inference(split_conjunct,[status(thm)],[c_0_55])).
% 0.25/0.52 cnf(c_0_68, hypothesis, (~greater(number_of_organizations(esk1_0,esk4_2(esk1_0,esk2_0)),zero)|~greater(equilibrium(esk1_0),esk4_2(esk1_0,esk2_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_36]), c_0_23])]), c_0_62])).
% 0.25/0.52 cnf(c_0_69, negated_conjecture, (greater(number_of_organizations(esk1_0,esk4_2(esk1_0,esk2_0)),zero)|greater(appear(an_organisation,esk1_0),esk4_2(esk1_0,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_36]), c_0_23])])).
% 0.25/0.52 fof(c_0_70, plain, ![X37, X38]:((cardinality_at_time(X37,X38)!=zero|~greater(zero,growth_rate(X37,X38)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_64])])])).
% 0.25/0.52 cnf(c_0_71, plain, (cardinality_at_time(X3,X2)=zero|~environment(X1)|~in_environment(X1,X2)|number_of_organizations(X1,X2)!=zero|~subpopulation(X3,X1,X2)), inference(split_conjunct,[status(thm)],[c_0_65])).
% 0.25/0.52 cnf(c_0_72, negated_conjecture, (subpopulation(efficient_producers,esk1_0,esk4_2(esk1_0,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66, c_0_36]), c_0_23])])).
% 0.25/0.52 fof(c_0_73, plain, ![X35, X36]:((~environment(X35)|~in_environment(X35,X36)|~greater(appear(an_organisation,X35),X36)|number_of_organizations(X35,X36)=zero)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_start_of_organizations])])])).
% 0.25/0.52 cnf(c_0_74, hypothesis, (constant(resources(esk1_0,esk4_2(esk1_0,esk2_0)))|greater(equilibrium(esk1_0),esk4_2(esk1_0,esk2_0))|~greater(number_of_organizations(esk1_0,esk4_2(esk1_0,esk2_0)),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_36]), c_0_23])])).
% 0.25/0.52 cnf(c_0_75, negated_conjecture, (greater(appear(an_organisation,esk1_0),esk4_2(esk1_0,esk2_0))|~greater(equilibrium(esk1_0),esk4_2(esk1_0,esk2_0))), inference(spm,[status(thm)],[c_0_68, c_0_69])).
% 0.25/0.52 cnf(c_0_76, plain, (cardinality_at_time(X1,X2)!=zero|~greater(zero,growth_rate(X1,X2))), inference(split_conjunct,[status(thm)],[c_0_70])).
% 0.25/0.52 cnf(c_0_77, negated_conjecture, (cardinality_at_time(efficient_producers,esk4_2(esk1_0,esk2_0))=zero|number_of_organizations(esk1_0,esk4_2(esk1_0,esk2_0))!=zero), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_71, c_0_72]), c_0_36]), c_0_23])])).
% 0.25/0.52 fof(c_0_78, plain, ![X4]:((constant(X4)=>~decreases(X4))), inference(fof_simplification,[status(thm)],[mp_constant_not_decrease])).
% 0.25/0.52 cnf(c_0_79, hypothesis, (constant(number_of_organizations(X1,X2))|~constant(resources(X1,X2))|~environment(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_44])).
% 0.25/0.52 cnf(c_0_80, plain, (number_of_organizations(X1,X2)=zero|~environment(X1)|~in_environment(X1,X2)|~greater(appear(an_organisation,X1),X2)), inference(split_conjunct,[status(thm)],[c_0_73])).
% 0.25/0.52 cnf(c_0_81, negated_conjecture, (constant(resources(esk1_0,esk4_2(esk1_0,esk2_0)))|greater(appear(an_organisation,esk1_0),esk4_2(esk1_0,esk2_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_74, c_0_69]), c_0_75])).
% 0.25/0.52 cnf(c_0_82, negated_conjecture, (number_of_organizations(esk1_0,esk4_2(esk1_0,esk2_0))!=zero), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_76, c_0_77]), c_0_38])])).
% 0.25/0.52 fof(c_0_83, plain, ![X23]:((~constant(X23)|~decreases(X23))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_78])])])).
% 0.25/0.52 cnf(c_0_84, hypothesis, (constant(number_of_organizations(esk1_0,esk4_2(esk1_0,esk2_0)))|~constant(resources(esk1_0,esk4_2(esk1_0,esk2_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_79, c_0_36]), c_0_23])])).
% 0.25/0.52 cnf(c_0_85, negated_conjecture, (constant(resources(esk1_0,esk4_2(esk1_0,esk2_0)))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_80, c_0_81]), c_0_36]), c_0_23])]), c_0_82])).
% 0.25/0.52 cnf(c_0_86, plain, (~constant(X1)|~decreases(X1)), inference(split_conjunct,[status(thm)],[c_0_83])).
% 0.25/0.52 cnf(c_0_87, hypothesis, (constant(number_of_organizations(esk1_0,esk4_2(esk1_0,esk2_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_84, c_0_85])])).
% 0.25/0.52 cnf(c_0_88, hypothesis, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86, c_0_87]), c_0_57])]), ['proof']).
% 0.25/0.52 % SZS output end Proof
% 0.25/0.52 % User time : 0.014 s
% 0.25/0.52 % System time : 0.004 s
% 0.25/0.52 % Total time : 0.017 s
% 0.25/0.52 % User time : 0.014 s
% 0.25/0.52 % System time : 0.008 s
% 0.25/0.52 % Total time : 0.023 s
% 0.25/0.52
%------------------------------------------------------------------------------