%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT023+2 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n004.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:29 AM UTC 2026
% Result : Theorem 0.25s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT023+2 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.09/0.35 % Computer : n004.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.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 7 12:07:15 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.25/0.47 start to proof:theBenchmark.p
% 0.25/0.55 % Version : CSI_E---1.1
% 0.25/0.55 % Problem : theBenchmark.p
% 0.25/0.55 % Proof found!
% 0.25/0.55 % SZS status Theorem for theBenchmark.p
% 0.25/0.55 % SZS output start Proof
% 0.25/0.55 fof(prove_l5, conjecture, ![X1]:(((environment(X1)&stable(X1))=>in_environment(X1,critical_point(X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_l5)).
% 0.25/0.55 fof(mp_earliest_time_growth_rate_exceeds, axiom, ![X1]:(((environment(X1)&?[X2]:((in_environment(X1,X2)&![X3]:(((subpopulations(first_movers,efficient_producers,X1,X3)&greater_or_equal(X3,X2))=>greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3)))))))=>?[X2]:(((in_environment(X1,X2)&~(greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))))&![X3]:(((subpopulations(first_movers,efficient_producers,X1,X3)&greater(X3,X2))=>greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3)))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds)).
% 0.25/0.55 fof(l1, hypothesis, ![X1]:(((environment(X1)&stable(X1))=>?[X2]:((in_environment(X1,X2)&![X3]:(((subpopulations(first_movers,efficient_producers,X1,X3)&greater_or_equal(X3,X2))=>greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3)))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l1)).
% 0.25/0.55 fof(d1, hypothesis, ![X1, X2]:(((((environment(X1)&~(greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))))&in_environment(X1,X2))&![X3]:(((subpopulations(first_movers,efficient_producers,X1,X3)&greater(X3,X2))=>greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3)))))=>X2=critical_point(X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1)).
% 0.25/0.55 fof(c_0_4, negated_conjecture, ~(![X1]:(((environment(X1)&stable(X1))=>in_environment(X1,critical_point(X1))))), inference(assume_negation,[status(cth)],[prove_l5])).
% 0.25/0.55 fof(c_0_5, plain, ![X1]:(((environment(X1)&?[X2]:((in_environment(X1,X2)&![X3]:(((subpopulations(first_movers,efficient_producers,X1,X3)&greater_or_equal(X3,X2))=>greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3)))))))=>?[X2]:(((in_environment(X1,X2)&~greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)))&![X3]:(((subpopulations(first_movers,efficient_producers,X1,X3)&greater(X3,X2))=>greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3)))))))), inference(fof_simplification,[status(thm)],[mp_earliest_time_growth_rate_exceeds])).
% 0.25/0.55 fof(c_0_6, hypothesis, ![X12, X14]:(((in_environment(X12,esk4_1(X12))|(~environment(X12)|~stable(X12)))&(~subpopulations(first_movers,efficient_producers,X12,X14)|~greater_or_equal(X14,esk4_1(X12))|greater(growth_rate(efficient_producers,X14),growth_rate(first_movers,X14))|(~environment(X12)|~stable(X12))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[l1])])])])])])).
% 0.25/0.55 fof(c_0_7, negated_conjecture, ((environment(esk5_0)&stable(esk5_0))&~in_environment(esk5_0,critical_point(esk5_0))), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_4])])])])).
% 0.25/0.55 fof(c_0_8, hypothesis, ![X1, X2]:(((((environment(X1)&~greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)))&in_environment(X1,X2))&![X3]:(((subpopulations(first_movers,efficient_producers,X1,X3)&greater(X3,X2))=>greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3)))))=>X2=critical_point(X1))), inference(fof_simplification,[status(thm)],[d1])).
% 0.25/0.55 fof(c_0_9, plain, ![X4, X5, X8]:((((((in_environment(X4,esk2_1(X4))|(subpopulations(first_movers,efficient_producers,X4,esk1_2(X4,X5))|~in_environment(X4,X5)|~environment(X4)))&(~greater(growth_rate(efficient_producers,esk2_1(X4)),growth_rate(first_movers,esk2_1(X4)))|(subpopulations(first_movers,efficient_producers,X4,esk1_2(X4,X5))|~in_environment(X4,X5)|~environment(X4))))&(~subpopulations(first_movers,efficient_producers,X4,X8)|~greater(X8,esk2_1(X4))|greater(growth_rate(efficient_producers,X8),growth_rate(first_movers,X8))|(subpopulations(first_movers,efficient_producers,X4,esk1_2(X4,X5))|~in_environment(X4,X5)|~environment(X4))))&(((in_environment(X4,esk2_1(X4))|(greater_or_equal(esk1_2(X4,X5),X5)|~in_environment(X4,X5)|~environment(X4)))&(~greater(growth_rate(efficient_producers,esk2_1(X4)),growth_rate(first_movers,esk2_1(X4)))|(greater_or_equal(esk1_2(X4,X5),X5)|~in_environment(X4,X5)|~environment(X4))))&(~subpopulations(first_movers,efficient_producers,X4,X8)|~greater(X8,esk2_1(X4))|greater(growth_rate(efficient_producers,X8),growth_rate(first_movers,X8))|(greater_or_equal(esk1_2(X4,X5),X5)|~in_environment(X4,X5)|~environment(X4)))))&(((in_environment(X4,esk2_1(X4))|(~greater(growth_rate(efficient_producers,esk1_2(X4,X5)),growth_rate(first_movers,esk1_2(X4,X5)))|~in_environment(X4,X5)|~environment(X4)))&(~greater(growth_rate(efficient_producers,esk2_1(X4)),growth_rate(first_movers,esk2_1(X4)))|(~greater(growth_rate(efficient_producers,esk1_2(X4,X5)),growth_rate(first_movers,esk1_2(X4,X5)))|~in_environment(X4,X5)|~environment(X4))))&(~subpopulations(first_movers,efficient_producers,X4,X8)|~greater(X8,esk2_1(X4))|greater(growth_rate(efficient_producers,X8),growth_rate(first_movers,X8))|(~greater(growth_rate(efficient_producers,esk1_2(X4,X5)),growth_rate(first_movers,esk1_2(X4,X5)))|~in_environment(X4,X5)|~environment(X4)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_5])])])])])])).
% 0.25/0.55 cnf(c_0_10, hypothesis, (in_environment(X1,esk4_1(X1))|~environment(X1)|~stable(X1)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.25/0.55 cnf(c_0_11, negated_conjecture, (stable(esk5_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.25/0.55 cnf(c_0_12, negated_conjecture, (environment(esk5_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.25/0.55 fof(c_0_13, hypothesis, ![X9, X10]:((((subpopulations(first_movers,efficient_producers,X9,esk3_2(X9,X10))|(~environment(X9)|greater(growth_rate(efficient_producers,X10),growth_rate(first_movers,X10))|~in_environment(X9,X10))|X10=critical_point(X9))&(greater(esk3_2(X9,X10),X10)|(~environment(X9)|greater(growth_rate(efficient_producers,X10),growth_rate(first_movers,X10))|~in_environment(X9,X10))|X10=critical_point(X9)))&(~greater(growth_rate(efficient_producers,esk3_2(X9,X10)),growth_rate(first_movers,esk3_2(X9,X10)))|(~environment(X9)|greater(growth_rate(efficient_producers,X10),growth_rate(first_movers,X10))|~in_environment(X9,X10))|X10=critical_point(X9)))), 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_8])])])])])).
% 0.25/0.55 cnf(c_0_14, plain, (in_environment(X1,esk2_1(X1))|greater_or_equal(esk1_2(X1,X2),X2)|~in_environment(X1,X2)|~environment(X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.25/0.55 cnf(c_0_15, negated_conjecture, (in_environment(esk5_0,esk4_1(esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10, c_0_11]), c_0_12])])).
% 0.25/0.55 cnf(c_0_16, plain, (in_environment(X1,esk2_1(X1))|subpopulations(first_movers,efficient_producers,X1,esk1_2(X1,X2))|~in_environment(X1,X2)|~environment(X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.25/0.55 cnf(c_0_17, hypothesis, (greater(esk3_2(X1,X2),X2)|greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|X2=critical_point(X1)|~environment(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.25/0.55 cnf(c_0_18, negated_conjecture, (greater_or_equal(esk1_2(esk5_0,esk4_1(esk5_0)),esk4_1(esk5_0))|in_environment(esk5_0,esk2_1(esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_14, c_0_15]), c_0_12])])).
% 0.25/0.55 cnf(c_0_19, negated_conjecture, (subpopulations(first_movers,efficient_producers,esk5_0,esk1_2(esk5_0,esk4_1(esk5_0)))|in_environment(esk5_0,esk2_1(esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_15]), c_0_12])])).
% 0.25/0.55 cnf(c_0_20, hypothesis, (greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|~subpopulations(first_movers,efficient_producers,X1,X2)|~greater_or_equal(X2,esk4_1(X1))|~environment(X1)|~stable(X1)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.25/0.55 cnf(c_0_21, negated_conjecture, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk2_1(esk5_0)),growth_rate(first_movers,esk2_1(esk5_0)))|greater(esk3_2(esk5_0,esk2_1(esk5_0)),esk2_1(esk5_0))|greater_or_equal(esk1_2(esk5_0,esk4_1(esk5_0)),esk4_1(esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_17, c_0_18]), c_0_12])])).
% 0.25/0.55 cnf(c_0_22, negated_conjecture, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk2_1(esk5_0)),growth_rate(first_movers,esk2_1(esk5_0)))|greater(esk3_2(esk5_0,esk2_1(esk5_0)),esk2_1(esk5_0))|subpopulations(first_movers,efficient_producers,esk5_0,esk1_2(esk5_0,esk4_1(esk5_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_17, c_0_19]), c_0_12])])).
% 0.25/0.55 cnf(c_0_23, plain, (in_environment(X1,esk2_1(X1))|~greater(growth_rate(efficient_producers,esk1_2(X1,X2)),growth_rate(first_movers,esk1_2(X1,X2)))|~in_environment(X1,X2)|~environment(X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.25/0.55 cnf(c_0_24, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk1_2(esk5_0,esk4_1(esk5_0))),growth_rate(first_movers,esk1_2(esk5_0,esk4_1(esk5_0))))|greater(growth_rate(efficient_producers,esk2_1(esk5_0)),growth_rate(first_movers,esk2_1(esk5_0)))|greater(esk3_2(esk5_0,esk2_1(esk5_0)),esk2_1(esk5_0))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_21]), c_0_11]), c_0_12])]), c_0_22])).
% 0.25/0.55 cnf(c_0_25, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk2_1(esk5_0)),growth_rate(first_movers,esk2_1(esk5_0)))|greater(esk3_2(esk5_0,esk2_1(esk5_0)),esk2_1(esk5_0))|in_environment(esk5_0,esk2_1(esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_24]), c_0_15]), c_0_12])])).
% 0.25/0.55 cnf(c_0_26, plain, (greater_or_equal(esk1_2(X1,X2),X2)|~greater(growth_rate(efficient_producers,esk2_1(X1)),growth_rate(first_movers,esk2_1(X1)))|~in_environment(X1,X2)|~environment(X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.25/0.55 cnf(c_0_27, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk2_1(esk5_0)),growth_rate(first_movers,esk2_1(esk5_0)))|greater(esk3_2(esk5_0,esk2_1(esk5_0)),esk2_1(esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_17, c_0_25]), c_0_12])])).
% 0.25/0.55 cnf(c_0_28, plain, (subpopulations(first_movers,efficient_producers,X1,esk1_2(X1,X2))|~greater(growth_rate(efficient_producers,esk2_1(X1)),growth_rate(first_movers,esk2_1(X1)))|~in_environment(X1,X2)|~environment(X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.25/0.55 cnf(c_0_29, plain, (~greater(growth_rate(efficient_producers,esk2_1(X1)),growth_rate(first_movers,esk2_1(X1)))|~greater(growth_rate(efficient_producers,esk1_2(X1,X2)),growth_rate(first_movers,esk1_2(X1,X2)))|~in_environment(X1,X2)|~environment(X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.25/0.55 cnf(c_0_30, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(esk3_2(esk5_0,esk2_1(esk5_0)),esk2_1(esk5_0))|greater_or_equal(esk1_2(esk5_0,X1),X1)|~in_environment(esk5_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_26, c_0_27]), c_0_12])])).
% 0.25/0.55 cnf(c_0_31, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(esk3_2(esk5_0,esk2_1(esk5_0)),esk2_1(esk5_0))|subpopulations(first_movers,efficient_producers,esk5_0,esk1_2(esk5_0,X1))|~in_environment(esk5_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_27]), c_0_12])])).
% 0.25/0.55 cnf(c_0_32, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(esk3_2(esk5_0,esk2_1(esk5_0)),esk2_1(esk5_0))|~greater(growth_rate(efficient_producers,esk1_2(esk5_0,X1)),growth_rate(first_movers,esk1_2(esk5_0,X1)))|~in_environment(esk5_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29, c_0_27]), c_0_12])])).
% 0.25/0.55 cnf(c_0_33, negated_conjecture, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(esk3_2(esk5_0,esk2_1(esk5_0)),esk2_1(esk5_0))|greater_or_equal(esk1_2(esk5_0,esk4_1(esk5_0)),esk4_1(esk5_0))), inference(spm,[status(thm)],[c_0_30, c_0_15])).
% 0.25/0.55 cnf(c_0_34, negated_conjecture, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(esk3_2(esk5_0,esk2_1(esk5_0)),esk2_1(esk5_0))|subpopulations(first_movers,efficient_producers,esk5_0,esk1_2(esk5_0,esk4_1(esk5_0)))), inference(spm,[status(thm)],[c_0_31, c_0_15])).
% 0.25/0.55 cnf(c_0_35, negated_conjecture, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(esk3_2(esk5_0,esk2_1(esk5_0)),esk2_1(esk5_0))|~greater(growth_rate(efficient_producers,esk1_2(esk5_0,esk4_1(esk5_0))),growth_rate(first_movers,esk1_2(esk5_0,esk4_1(esk5_0))))), inference(spm,[status(thm)],[c_0_32, c_0_15])).
% 0.25/0.55 cnf(c_0_36, plain, (greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|greater_or_equal(esk1_2(X1,X3),X3)|~subpopulations(first_movers,efficient_producers,X1,X2)|~greater(X2,esk2_1(X1))|~in_environment(X1,X3)|~environment(X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.25/0.55 cnf(c_0_37, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(esk3_2(esk5_0,esk2_1(esk5_0)),esk2_1(esk5_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_33]), c_0_11]), c_0_12])]), c_0_34]), c_0_35])).
% 0.25/0.55 cnf(c_0_38, plain, (greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|subpopulations(first_movers,efficient_producers,X1,esk1_2(X1,X3))|~subpopulations(first_movers,efficient_producers,X1,X2)|~greater(X2,esk2_1(X1))|~in_environment(X1,X3)|~environment(X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.25/0.55 cnf(c_0_39, plain, (greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|~subpopulations(first_movers,efficient_producers,X1,X2)|~greater(X2,esk2_1(X1))|~greater(growth_rate(efficient_producers,esk1_2(X1,X3)),growth_rate(first_movers,esk1_2(X1,X3)))|~in_environment(X1,X3)|~environment(X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.25/0.55 cnf(c_0_40, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk3_2(esk5_0,esk2_1(esk5_0))),growth_rate(first_movers,esk3_2(esk5_0,esk2_1(esk5_0))))|greater_or_equal(esk1_2(esk5_0,X1),X1)|~subpopulations(first_movers,efficient_producers,esk5_0,esk3_2(esk5_0,esk2_1(esk5_0)))|~in_environment(esk5_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36, c_0_37]), c_0_12])])).
% 0.25/0.55 cnf(c_0_41, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk3_2(esk5_0,esk2_1(esk5_0))),growth_rate(first_movers,esk3_2(esk5_0,esk2_1(esk5_0))))|subpopulations(first_movers,efficient_producers,esk5_0,esk1_2(esk5_0,X1))|~subpopulations(first_movers,efficient_producers,esk5_0,esk3_2(esk5_0,esk2_1(esk5_0)))|~in_environment(esk5_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_37]), c_0_12])])).
% 0.25/0.55 cnf(c_0_42, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk3_2(esk5_0,esk2_1(esk5_0))),growth_rate(first_movers,esk3_2(esk5_0,esk2_1(esk5_0))))|~greater(growth_rate(efficient_producers,esk1_2(esk5_0,X1)),growth_rate(first_movers,esk1_2(esk5_0,X1)))|~subpopulations(first_movers,efficient_producers,esk5_0,esk3_2(esk5_0,esk2_1(esk5_0)))|~in_environment(esk5_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_37]), c_0_12])])).
% 0.25/0.55 cnf(c_0_43, hypothesis, (subpopulations(first_movers,efficient_producers,X1,esk3_2(X1,X2))|greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|X2=critical_point(X1)|~environment(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.25/0.55 cnf(c_0_44, negated_conjecture, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk3_2(esk5_0,esk2_1(esk5_0))),growth_rate(first_movers,esk3_2(esk5_0,esk2_1(esk5_0))))|greater_or_equal(esk1_2(esk5_0,esk4_1(esk5_0)),esk4_1(esk5_0))|~subpopulations(first_movers,efficient_producers,esk5_0,esk3_2(esk5_0,esk2_1(esk5_0)))), inference(spm,[status(thm)],[c_0_40, c_0_15])).
% 0.25/0.55 cnf(c_0_45, negated_conjecture, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk3_2(esk5_0,esk2_1(esk5_0))),growth_rate(first_movers,esk3_2(esk5_0,esk2_1(esk5_0))))|subpopulations(first_movers,efficient_producers,esk5_0,esk1_2(esk5_0,esk4_1(esk5_0)))|~subpopulations(first_movers,efficient_producers,esk5_0,esk3_2(esk5_0,esk2_1(esk5_0)))), inference(spm,[status(thm)],[c_0_41, c_0_15])).
% 0.25/0.55 cnf(c_0_46, negated_conjecture, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk3_2(esk5_0,esk2_1(esk5_0))),growth_rate(first_movers,esk3_2(esk5_0,esk2_1(esk5_0))))|~greater(growth_rate(efficient_producers,esk1_2(esk5_0,esk4_1(esk5_0))),growth_rate(first_movers,esk1_2(esk5_0,esk4_1(esk5_0))))|~subpopulations(first_movers,efficient_producers,esk5_0,esk3_2(esk5_0,esk2_1(esk5_0)))), inference(spm,[status(thm)],[c_0_42, c_0_15])).
% 0.25/0.55 cnf(c_0_47, negated_conjecture, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk2_1(esk5_0)),growth_rate(first_movers,esk2_1(esk5_0)))|greater_or_equal(esk1_2(esk5_0,esk4_1(esk5_0)),esk4_1(esk5_0))|subpopulations(first_movers,efficient_producers,esk5_0,esk3_2(esk5_0,esk2_1(esk5_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_18]), c_0_12])])).
% 0.25/0.55 cnf(c_0_48, negated_conjecture, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk2_1(esk5_0)),growth_rate(first_movers,esk2_1(esk5_0)))|subpopulations(first_movers,efficient_producers,esk5_0,esk1_2(esk5_0,esk4_1(esk5_0)))|subpopulations(first_movers,efficient_producers,esk5_0,esk3_2(esk5_0,esk2_1(esk5_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_19]), c_0_12])])).
% 0.25/0.55 cnf(c_0_49, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk3_2(esk5_0,esk2_1(esk5_0))),growth_rate(first_movers,esk3_2(esk5_0,esk2_1(esk5_0))))|~subpopulations(first_movers,efficient_producers,esk5_0,esk3_2(esk5_0,esk2_1(esk5_0)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_44]), c_0_11]), c_0_12])]), c_0_45]), c_0_46])).
% 0.25/0.55 cnf(c_0_50, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk1_2(esk5_0,esk4_1(esk5_0))),growth_rate(first_movers,esk1_2(esk5_0,esk4_1(esk5_0))))|greater(growth_rate(efficient_producers,esk2_1(esk5_0)),growth_rate(first_movers,esk2_1(esk5_0)))|subpopulations(first_movers,efficient_producers,esk5_0,esk3_2(esk5_0,esk2_1(esk5_0)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_47]), c_0_11]), c_0_12])]), c_0_48])).
% 0.25/0.55 cnf(c_0_51, hypothesis, (greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|X2=critical_point(X1)|~greater(growth_rate(efficient_producers,esk3_2(X1,X2)),growth_rate(first_movers,esk3_2(X1,X2)))|~environment(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.25/0.55 cnf(c_0_52, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk1_2(esk5_0,esk4_1(esk5_0))),growth_rate(first_movers,esk1_2(esk5_0,esk4_1(esk5_0))))|greater(growth_rate(efficient_producers,esk3_2(esk5_0,esk2_1(esk5_0))),growth_rate(first_movers,esk3_2(esk5_0,esk2_1(esk5_0))))|greater(growth_rate(efficient_producers,esk2_1(esk5_0)),growth_rate(first_movers,esk2_1(esk5_0)))), inference(spm,[status(thm)],[c_0_49, c_0_50])).
% 0.25/0.55 cnf(c_0_53, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk1_2(esk5_0,esk4_1(esk5_0))),growth_rate(first_movers,esk1_2(esk5_0,esk4_1(esk5_0))))|greater(growth_rate(efficient_producers,esk2_1(esk5_0)),growth_rate(first_movers,esk2_1(esk5_0)))|~in_environment(esk5_0,esk2_1(esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_52]), c_0_12])])).
% 0.25/0.55 cnf(c_0_54, negated_conjecture, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk1_2(esk5_0,esk4_1(esk5_0))),growth_rate(first_movers,esk1_2(esk5_0,esk4_1(esk5_0))))|greater(growth_rate(efficient_producers,esk2_1(esk5_0)),growth_rate(first_movers,esk2_1(esk5_0)))|greater_or_equal(esk1_2(esk5_0,esk4_1(esk5_0)),esk4_1(esk5_0))), inference(spm,[status(thm)],[c_0_53, c_0_18])).
% 0.25/0.55 cnf(c_0_55, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk1_2(esk5_0,esk4_1(esk5_0))),growth_rate(first_movers,esk1_2(esk5_0,esk4_1(esk5_0))))|greater(growth_rate(efficient_producers,esk2_1(esk5_0)),growth_rate(first_movers,esk2_1(esk5_0)))|~subpopulations(first_movers,efficient_producers,esk5_0,esk1_2(esk5_0,esk4_1(esk5_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_54]), c_0_11]), c_0_12])])).
% 0.25/0.55 cnf(c_0_56, negated_conjecture, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk1_2(esk5_0,esk4_1(esk5_0))),growth_rate(first_movers,esk1_2(esk5_0,esk4_1(esk5_0))))|greater(growth_rate(efficient_producers,esk2_1(esk5_0)),growth_rate(first_movers,esk2_1(esk5_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_53, c_0_19]), c_0_55])).
% 0.25/0.55 cnf(c_0_57, negated_conjecture, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk2_1(esk5_0)),growth_rate(first_movers,esk2_1(esk5_0)))|in_environment(esk5_0,esk2_1(esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_56]), c_0_15]), c_0_12])])).
% 0.25/0.55 cnf(c_0_58, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk2_1(esk5_0)),growth_rate(first_movers,esk2_1(esk5_0)))|subpopulations(first_movers,efficient_producers,esk5_0,esk3_2(esk5_0,esk2_1(esk5_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_57]), c_0_12])])).
% 0.25/0.55 cnf(c_0_59, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk3_2(esk5_0,esk2_1(esk5_0))),growth_rate(first_movers,esk3_2(esk5_0,esk2_1(esk5_0))))|greater(growth_rate(efficient_producers,esk2_1(esk5_0)),growth_rate(first_movers,esk2_1(esk5_0)))), inference(spm,[status(thm)],[c_0_49, c_0_58])).
% 0.25/0.55 cnf(c_0_60, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater(growth_rate(efficient_producers,esk2_1(esk5_0)),growth_rate(first_movers,esk2_1(esk5_0)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_59]), c_0_12])]), c_0_57])).
% 0.25/0.55 cnf(c_0_61, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|greater_or_equal(esk1_2(esk5_0,X1),X1)|~in_environment(esk5_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_26, c_0_60]), c_0_12])])).
% 0.25/0.55 cnf(c_0_62, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|subpopulations(first_movers,efficient_producers,esk5_0,esk1_2(esk5_0,X1))|~in_environment(esk5_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_60]), c_0_12])])).
% 0.25/0.55 cnf(c_0_63, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)|~greater(growth_rate(efficient_producers,esk1_2(esk5_0,X1)),growth_rate(first_movers,esk1_2(esk5_0,X1)))|~in_environment(esk5_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29, c_0_60]), c_0_12])])).
% 0.25/0.55 cnf(c_0_64, negated_conjecture, (esk2_1(esk5_0)=critical_point(esk5_0)|greater_or_equal(esk1_2(esk5_0,esk4_1(esk5_0)),esk4_1(esk5_0))), inference(spm,[status(thm)],[c_0_61, c_0_15])).
% 0.25/0.55 cnf(c_0_65, negated_conjecture, (esk2_1(esk5_0)=critical_point(esk5_0)|subpopulations(first_movers,efficient_producers,esk5_0,esk1_2(esk5_0,esk4_1(esk5_0)))), inference(spm,[status(thm)],[c_0_62, c_0_15])).
% 0.25/0.55 cnf(c_0_66, negated_conjecture, (esk2_1(esk5_0)=critical_point(esk5_0)|~greater(growth_rate(efficient_producers,esk1_2(esk5_0,esk4_1(esk5_0))),growth_rate(first_movers,esk1_2(esk5_0,esk4_1(esk5_0))))), inference(spm,[status(thm)],[c_0_63, c_0_15])).
% 0.25/0.55 cnf(c_0_67, hypothesis, (esk2_1(esk5_0)=critical_point(esk5_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_64]), c_0_11]), c_0_12])]), c_0_65]), c_0_66])).
% 0.25/0.55 cnf(c_0_68, negated_conjecture, (~in_environment(esk5_0,critical_point(esk5_0))), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.25/0.55 cnf(c_0_69, negated_conjecture, (greater_or_equal(esk1_2(esk5_0,esk4_1(esk5_0)),esk4_1(esk5_0))), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_18, c_0_67]), c_0_68])).
% 0.25/0.55 cnf(c_0_70, negated_conjecture, (subpopulations(first_movers,efficient_producers,esk5_0,esk1_2(esk5_0,esk4_1(esk5_0)))), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_19, c_0_67]), c_0_68])).
% 0.25/0.55 cnf(c_0_71, hypothesis, (greater(growth_rate(efficient_producers,esk1_2(esk5_0,esk4_1(esk5_0))),growth_rate(first_movers,esk1_2(esk5_0,esk4_1(esk5_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_69]), c_0_11]), c_0_12])]), c_0_70])])).
% 0.25/0.55 cnf(c_0_72, hypothesis, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_71]), c_0_67]), c_0_15]), c_0_12])]), c_0_68]), ['proof']).
% 0.25/0.55 % SZS output end Proof
% 0.25/0.55 % User time : 0.008 s
% 0.25/0.55 % System time : 0.003 s
% 0.25/0.55 % Total time : 0.011 s
% 0.25/0.55 % User time : 0.027 s
% 0.25/0.55 % System time : 0.008 s
% 0.25/0.55 % Total time : 0.035 s
% 0.25/0.55
%------------------------------------------------------------------------------