%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT034+2 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n020.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:31 AM UTC 2026
% Result : Theorem 0.22s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT034+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 : n020.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:32:43 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.22/0.47 start to proof:theBenchmark.p
% 0.22/0.55 % Version : CSI_E---1.1
% 0.22/0.55 % Problem : theBenchmark.p
% 0.22/0.55 % Proof found!
% 0.22/0.55 % SZS status Theorem for theBenchmark.p
% 0.22/0.55 % SZS output start Proof
% 0.22/0.55 fof(mp_greater_or_equal, axiom, ![X8, X9]:((greater_or_equal(X8,X9)<=>(greater(X8,X9)|X8=X9))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_greater_or_equal)).
% 0.22/0.55 fof(prove_t3, conjecture, ![X1, X4]:(((((environment(X1)&in_environment(X1,critical_point(X1)))&greater_or_equal(X4,appear(efficient_producers,X1)))&greater(critical_point(X1),X4))=>selection_favors(first_movers,efficient_producers,X4))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_t3)).
% 0.22/0.55 fof(mp_critical_time_points, axiom, ![X1, X4]:(((((environment(X1)&in_environment(X1,critical_point(X1)))&greater_or_equal(X4,appear(efficient_producers,X1)))&greater(critical_point(X1),X4))=>in_environment(X1,X4))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_critical_time_points)).
% 0.22/0.55 fof(mp_critical_point_means_FM_and_EP, axiom, ![X1]:(((environment(X1)&in_environment(X1,critical_point(X1)))=>subpopulations(first_movers,efficient_producers,X1,critical_point(X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_critical_point_means_FM_and_EP)).
% 0.22/0.55 fof(mp_FM_and_EP_when_EP_appears, axiom, ![X1]:(((environment(X1)&in_environment(X1,appear(efficient_producers,X1)))=>subpopulations(first_movers,efficient_producers,X1,appear(efficient_producers,X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_FM_and_EP_when_EP_appears)).
% 0.22/0.55 fof(mp_FM_and_EP_members_EP_appeared, axiom, ![X1, X4]:(((environment(X1)&subpopulations(first_movers,efficient_producers,X1,X4))=>greater_or_equal(X4,appear(efficient_producers,X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_FM_and_EP_members_EP_appeared)).
% 0.22/0.55 fof(a10, hypothesis, ![X1, X6, X7, X4]:((((((environment(X1)&subpopulations(first_movers,efficient_producers,X1,X6))&subpopulations(first_movers,efficient_producers,X1,X7))&greater_or_equal(X4,X6))&greater_or_equal(X7,X4))=>subpopulations(first_movers,efficient_producers,X1,X4))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a10)).
% 0.22/0.55 fof(mp_difference_between_founding_rates, axiom, ![X4]:(((decreases(difference(founding_rate(first_movers,X4),founding_rate(efficient_producers,X4)))&~(decreases(difference(disbanding_rate(first_movers,X4),disbanding_rate(efficient_producers,X4)))))=>decreases(difference(growth_rate(first_movers,X4),growth_rate(efficient_producers,X4))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_difference_between_founding_rates)).
% 0.22/0.55 fof(a12, hypothesis, ![X1, X4]:(((environment(X1)&subpopulations(first_movers,efficient_producers,X1,X4))=>decreases(difference(founding_rate(first_movers,X4),founding_rate(efficient_producers,X4))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a12)).
% 0.22/0.55 fof(mp_decreasing_function, axiom, ![X1, X4, X5]:((((((environment(X1)&in_environment(X1,X5))&greater_or_equal(difference(growth_rate(first_movers,X5),growth_rate(efficient_producers,X5)),zero))&greater_or_equal(X4,appear(efficient_producers,X1)))&greater(X5,X4))=>(decreases(difference(growth_rate(first_movers,X4),growth_rate(efficient_producers,X4)))=>greater(difference(growth_rate(first_movers,X4),growth_rate(efficient_producers,X4)),zero)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_decreasing_function)).
% 0.22/0.55 fof(l3, axiom, ![X1, X4]:(((environment(X1)&subpopulations(first_movers,efficient_producers,X1,X4))=>~(decreases(difference(disbanding_rate(first_movers,X4),disbanding_rate(efficient_producers,X4)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l3)).
% 0.22/0.55 fof(mp_symmetry_of_subpopulations, axiom, ![X1, X4]:(((environment(X1)&subpopulations(first_movers,efficient_producers,X1,X4))=>subpopulations(efficient_producers,first_movers,X1,X4))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_symmetry_of_subpopulations)).
% 0.22/0.55 fof(mp1_high_growth_rates, axiom, ![X1, X2, X3, X4]:((((environment(X1)&subpopulations(X2,X3,X1,X4))&greater(growth_rate(X3,X4),growth_rate(X2,X4)))=>selection_favors(X3,X2,X4))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp1_high_growth_rates)).
% 0.22/0.55 fof(mp_positive_growth_rate_difference, axiom, ![X4]:((greater(difference(growth_rate(first_movers,X4),growth_rate(efficient_producers,X4)),zero)<=>greater(growth_rate(first_movers,X4),growth_rate(efficient_producers,X4)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_positive_growth_rate_difference)).
% 0.22/0.55 fof(d1, hypothesis, ![X1, X10]:(((environment(X1)&X10=critical_point(X1))=>(~(greater(growth_rate(efficient_producers,X10),growth_rate(first_movers,X10)))&![X4]:(((subpopulations(first_movers,efficient_producers,X1,X4)&greater(X4,X10))=>greater(growth_rate(efficient_producers,X4),growth_rate(first_movers,X4))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1)).
% 0.22/0.55 fof(mp_relationship_of_growth_rates, axiom, ![X1, X4]:((((environment(X1)&subpopulations(first_movers,efficient_producers,X1,X4))&~(greater(zero,difference(growth_rate(first_movers,X4),growth_rate(efficient_producers,X4)))))=>greater_or_equal(difference(growth_rate(first_movers,X4),growth_rate(efficient_producers,X4)),zero))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_relationship_of_growth_rates)).
% 0.22/0.55 fof(mp_negative_growth_rate_difference, axiom, ![X4]:((greater(zero,difference(growth_rate(first_movers,X4),growth_rate(efficient_producers,X4)))<=>greater(growth_rate(efficient_producers,X4),growth_rate(first_movers,X4)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_negative_growth_rate_difference)).
% 0.22/0.55 fof(c_0_17, plain, ![X39, X40]:(((~greater_or_equal(X39,X40)|(greater(X39,X40)|X39=X40))&((~greater(X39,X40)|greater_or_equal(X39,X40))&(X39!=X40|greater_or_equal(X39,X40))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_greater_or_equal])])])])).
% 0.22/0.55 fof(c_0_18, negated_conjecture, ~(![X1, X4]:(((((environment(X1)&in_environment(X1,critical_point(X1)))&greater_or_equal(X4,appear(efficient_producers,X1)))&greater(critical_point(X1),X4))=>selection_favors(first_movers,efficient_producers,X4)))), inference(assume_negation,[status(cth)],[prove_t3])).
% 0.22/0.55 fof(c_0_19, plain, ![X31, X32]:((~environment(X31)|~in_environment(X31,critical_point(X31))|~greater_or_equal(X32,appear(efficient_producers,X31))|~greater(critical_point(X31),X32)|in_environment(X31,X32))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_critical_time_points])])])).
% 0.22/0.55 cnf(c_0_20, plain, (greater_or_equal(X1,X2)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.22/0.55 fof(c_0_21, plain, ![X17]:((~environment(X17)|~in_environment(X17,critical_point(X17))|subpopulations(first_movers,efficient_producers,X17,critical_point(X17)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_critical_point_means_FM_and_EP])])])).
% 0.22/0.55 fof(c_0_22, negated_conjecture, ((((environment(esk1_0)&in_environment(esk1_0,critical_point(esk1_0)))&greater_or_equal(esk2_0,appear(efficient_producers,esk1_0)))&greater(critical_point(esk1_0),esk2_0))&~selection_favors(first_movers,efficient_producers,esk2_0)), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_18])])])])).
% 0.22/0.55 fof(c_0_23, plain, ![X18]:((~environment(X18)|~in_environment(X18,appear(efficient_producers,X18))|subpopulations(first_movers,efficient_producers,X18,appear(efficient_producers,X18)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_FM_and_EP_when_EP_appears])])])).
% 0.22/0.55 cnf(c_0_24, plain, (in_environment(X1,X2)|~environment(X1)|~in_environment(X1,critical_point(X1))|~greater_or_equal(X2,appear(efficient_producers,X1))|~greater(critical_point(X1),X2)), inference(split_conjunct,[status(thm)],[c_0_19])).
% 0.22/0.55 cnf(c_0_25, plain, (greater_or_equal(X1,X1)), inference(er,[status(thm)],[c_0_20])).
% 0.22/0.55 fof(c_0_26, plain, ![X37, X38]:((~environment(X37)|~subpopulations(first_movers,efficient_producers,X37,X38)|greater_or_equal(X38,appear(efficient_producers,X37)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_FM_and_EP_members_EP_appeared])])])).
% 0.22/0.55 fof(c_0_27, hypothesis, ![X46, X47, X48, X49]:((~environment(X46)|~subpopulations(first_movers,efficient_producers,X46,X47)|~subpopulations(first_movers,efficient_producers,X46,X48)|~greater_or_equal(X49,X47)|~greater_or_equal(X48,X49)|subpopulations(first_movers,efficient_producers,X46,X49))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a10])])])).
% 0.22/0.55 cnf(c_0_28, plain, (subpopulations(first_movers,efficient_producers,X1,critical_point(X1))|~environment(X1)|~in_environment(X1,critical_point(X1))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.22/0.55 cnf(c_0_29, negated_conjecture, (in_environment(esk1_0,critical_point(esk1_0))), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.22/0.55 cnf(c_0_30, negated_conjecture, (environment(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.22/0.55 cnf(c_0_31, plain, (subpopulations(first_movers,efficient_producers,X1,appear(efficient_producers,X1))|~environment(X1)|~in_environment(X1,appear(efficient_producers,X1))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.22/0.55 cnf(c_0_32, plain, (in_environment(X1,appear(efficient_producers,X1))|~in_environment(X1,critical_point(X1))|~greater(critical_point(X1),appear(efficient_producers,X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_24, c_0_25])).
% 0.22/0.55 cnf(c_0_33, plain, (greater(X1,X2)|X1=X2|~greater_or_equal(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.22/0.55 cnf(c_0_34, plain, (greater_or_equal(X2,appear(efficient_producers,X1))|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.55 cnf(c_0_35, hypothesis, (subpopulations(first_movers,efficient_producers,X1,X4)|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater_or_equal(X4,X2)|~greater_or_equal(X3,X4)), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.22/0.55 cnf(c_0_36, negated_conjecture, (subpopulations(first_movers,efficient_producers,esk1_0,critical_point(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_29]), c_0_30])])).
% 0.22/0.55 cnf(c_0_37, plain, (subpopulations(first_movers,efficient_producers,X1,appear(efficient_producers,X1))|~in_environment(X1,critical_point(X1))|~greater(critical_point(X1),appear(efficient_producers,X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_31, c_0_32])).
% 0.22/0.55 cnf(c_0_38, plain, (X1=appear(efficient_producers,X2)|greater(X1,appear(efficient_producers,X2))|~subpopulations(first_movers,efficient_producers,X2,X1)|~environment(X2)), inference(spm,[status(thm)],[c_0_33, c_0_34])).
% 0.22/0.55 cnf(c_0_39, hypothesis, (subpopulations(first_movers,efficient_producers,esk1_0,X1)|~greater_or_equal(critical_point(esk1_0),X1)|~greater_or_equal(X1,X2)|~subpopulations(first_movers,efficient_producers,esk1_0,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_36]), c_0_30])])).
% 0.22/0.55 cnf(c_0_40, plain, (appear(efficient_producers,X1)=critical_point(X1)|subpopulations(first_movers,efficient_producers,X1,appear(efficient_producers,X1))|~in_environment(X1,critical_point(X1))|~environment(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_38]), c_0_28])).
% 0.22/0.55 cnf(c_0_41, hypothesis, (appear(efficient_producers,esk1_0)=critical_point(esk1_0)|subpopulations(first_movers,efficient_producers,esk1_0,X1)|~greater_or_equal(X1,appear(efficient_producers,esk1_0))|~greater_or_equal(critical_point(esk1_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_40]), c_0_29]), c_0_30])])).
% 0.22/0.55 cnf(c_0_42, negated_conjecture, (greater_or_equal(esk2_0,appear(efficient_producers,esk1_0))), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.22/0.55 fof(c_0_43, plain, ![X4]:(((decreases(difference(founding_rate(first_movers,X4),founding_rate(efficient_producers,X4)))&~decreases(difference(disbanding_rate(first_movers,X4),disbanding_rate(efficient_producers,X4))))=>decreases(difference(growth_rate(first_movers,X4),growth_rate(efficient_producers,X4))))), inference(fof_simplification,[status(thm)],[mp_difference_between_founding_rates])).
% 0.22/0.55 fof(c_0_44, hypothesis, ![X50, X51]:((~environment(X50)|~subpopulations(first_movers,efficient_producers,X50,X51)|decreases(difference(founding_rate(first_movers,X51),founding_rate(efficient_producers,X51))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a12])])])).
% 0.22/0.55 cnf(c_0_45, negated_conjecture, (appear(efficient_producers,esk1_0)=critical_point(esk1_0)|subpopulations(first_movers,efficient_producers,esk1_0,esk2_0)|~greater_or_equal(critical_point(esk1_0),esk2_0)), inference(spm,[status(thm)],[c_0_41, c_0_42])).
% 0.22/0.55 cnf(c_0_46, plain, (greater_or_equal(X1,X2)|~greater(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.22/0.55 cnf(c_0_47, negated_conjecture, (greater(critical_point(esk1_0),esk2_0)), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.22/0.55 fof(c_0_48, plain, ![X20, X21, X22]:((~environment(X20)|~in_environment(X20,X22)|~greater_or_equal(difference(growth_rate(first_movers,X22),growth_rate(efficient_producers,X22)),zero)|~greater_or_equal(X21,appear(efficient_producers,X20))|~greater(X22,X21)|(~decreases(difference(growth_rate(first_movers,X21),growth_rate(efficient_producers,X21)))|greater(difference(growth_rate(first_movers,X21),growth_rate(efficient_producers,X21)),zero)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_decreasing_function])])])).
% 0.22/0.55 fof(c_0_49, plain, ![X1, X4]:(((environment(X1)&subpopulations(first_movers,efficient_producers,X1,X4))=>~decreases(difference(disbanding_rate(first_movers,X4),disbanding_rate(efficient_producers,X4))))), inference(fof_simplification,[status(thm)],[l3])).
% 0.22/0.55 fof(c_0_50, plain, ![X19]:((~decreases(difference(founding_rate(first_movers,X19),founding_rate(efficient_producers,X19)))|decreases(difference(disbanding_rate(first_movers,X19),disbanding_rate(efficient_producers,X19)))|decreases(difference(growth_rate(first_movers,X19),growth_rate(efficient_producers,X19))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_43])])])).
% 0.22/0.55 cnf(c_0_51, hypothesis, (decreases(difference(founding_rate(first_movers,X2),founding_rate(efficient_producers,X2)))|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), inference(split_conjunct,[status(thm)],[c_0_44])).
% 0.22/0.55 cnf(c_0_52, negated_conjecture, (appear(efficient_producers,esk1_0)=critical_point(esk1_0)|subpopulations(first_movers,efficient_producers,esk1_0,esk2_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_46]), c_0_47])])).
% 0.22/0.55 fof(c_0_53, plain, ![X35, X36]:((~environment(X35)|~subpopulations(first_movers,efficient_producers,X35,X36)|subpopulations(efficient_producers,first_movers,X35,X36))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_symmetry_of_subpopulations])])])).
% 0.22/0.55 cnf(c_0_54, plain, (greater(difference(growth_rate(first_movers,X3),growth_rate(efficient_producers,X3)),zero)|~environment(X1)|~in_environment(X1,X2)|~greater_or_equal(difference(growth_rate(first_movers,X2),growth_rate(efficient_producers,X2)),zero)|~greater_or_equal(X3,appear(efficient_producers,X1))|~greater(X2,X3)|~decreases(difference(growth_rate(first_movers,X3),growth_rate(efficient_producers,X3)))), inference(split_conjunct,[status(thm)],[c_0_48])).
% 0.22/0.55 fof(c_0_55, plain, ![X15, X16]:((~environment(X15)|~subpopulations(first_movers,efficient_producers,X15,X16)|~decreases(difference(disbanding_rate(first_movers,X16),disbanding_rate(efficient_producers,X16))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_49])])])).
% 0.22/0.55 cnf(c_0_56, plain, (decreases(difference(disbanding_rate(first_movers,X1),disbanding_rate(efficient_producers,X1)))|decreases(difference(growth_rate(first_movers,X1),growth_rate(efficient_producers,X1)))|~decreases(difference(founding_rate(first_movers,X1),founding_rate(efficient_producers,X1)))), inference(split_conjunct,[status(thm)],[c_0_50])).
% 0.22/0.55 cnf(c_0_57, hypothesis, (appear(efficient_producers,esk1_0)=critical_point(esk1_0)|decreases(difference(founding_rate(first_movers,esk2_0),founding_rate(efficient_producers,esk2_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_52]), c_0_30])])).
% 0.22/0.55 fof(c_0_58, plain, ![X11, X12, X13, X14]:((~environment(X11)|~subpopulations(X12,X13,X11,X14)|~greater(growth_rate(X13,X14),growth_rate(X12,X14))|selection_favors(X13,X12,X14))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp1_high_growth_rates])])])).
% 0.22/0.55 cnf(c_0_59, plain, (subpopulations(efficient_producers,first_movers,X1,X2)|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), inference(split_conjunct,[status(thm)],[c_0_53])).
% 0.22/0.55 fof(c_0_60, plain, ![X24]:(((~greater(difference(growth_rate(first_movers,X24),growth_rate(efficient_producers,X24)),zero)|greater(growth_rate(first_movers,X24),growth_rate(efficient_producers,X24)))&(~greater(growth_rate(first_movers,X24),growth_rate(efficient_producers,X24))|greater(difference(growth_rate(first_movers,X24),growth_rate(efficient_producers,X24)),zero)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_positive_growth_rate_difference])])])).
% 0.22/0.55 cnf(c_0_61, negated_conjecture, (greater(difference(growth_rate(first_movers,esk2_0),growth_rate(efficient_producers,esk2_0)),zero)|~greater_or_equal(difference(growth_rate(first_movers,X1),growth_rate(efficient_producers,X1)),zero)|~in_environment(esk1_0,X1)|~decreases(difference(growth_rate(first_movers,esk2_0),growth_rate(efficient_producers,esk2_0)))|~greater(X1,esk2_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54, c_0_42]), c_0_30])])).
% 0.22/0.55 cnf(c_0_62, plain, (~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)|~decreases(difference(disbanding_rate(first_movers,X2),disbanding_rate(efficient_producers,X2)))), inference(split_conjunct,[status(thm)],[c_0_55])).
% 0.22/0.55 cnf(c_0_63, hypothesis, (appear(efficient_producers,esk1_0)=critical_point(esk1_0)|decreases(difference(disbanding_rate(first_movers,esk2_0),disbanding_rate(efficient_producers,esk2_0)))|decreases(difference(growth_rate(first_movers,esk2_0),growth_rate(efficient_producers,esk2_0)))), inference(spm,[status(thm)],[c_0_56, c_0_57])).
% 0.22/0.55 cnf(c_0_64, plain, (selection_favors(X3,X2,X4)|~environment(X1)|~subpopulations(X2,X3,X1,X4)|~greater(growth_rate(X3,X4),growth_rate(X2,X4))), inference(split_conjunct,[status(thm)],[c_0_58])).
% 0.22/0.55 cnf(c_0_65, negated_conjecture, (appear(efficient_producers,esk1_0)=critical_point(esk1_0)|subpopulations(efficient_producers,first_movers,esk1_0,esk2_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_59, c_0_52]), c_0_30])])).
% 0.22/0.55 cnf(c_0_66, negated_conjecture, (~selection_favors(first_movers,efficient_producers,esk2_0)), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.22/0.55 cnf(c_0_67, plain, (greater(growth_rate(first_movers,X1),growth_rate(efficient_producers,X1))|~greater(difference(growth_rate(first_movers,X1),growth_rate(efficient_producers,X1)),zero)), inference(split_conjunct,[status(thm)],[c_0_60])).
% 0.22/0.55 cnf(c_0_68, negated_conjecture, (greater(difference(growth_rate(first_movers,esk2_0),growth_rate(efficient_producers,esk2_0)),zero)|~greater_or_equal(difference(growth_rate(first_movers,critical_point(esk1_0)),growth_rate(efficient_producers,critical_point(esk1_0))),zero)|~decreases(difference(growth_rate(first_movers,esk2_0),growth_rate(efficient_producers,esk2_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_29]), c_0_47])])).
% 0.22/0.55 cnf(c_0_69, hypothesis, (appear(efficient_producers,esk1_0)=critical_point(esk1_0)|decreases(difference(growth_rate(first_movers,esk2_0),growth_rate(efficient_producers,esk2_0)))|~subpopulations(first_movers,efficient_producers,X1,esk2_0)|~environment(X1)), inference(spm,[status(thm)],[c_0_62, c_0_63])).
% 0.22/0.55 cnf(c_0_70, negated_conjecture, (appear(efficient_producers,esk1_0)=critical_point(esk1_0)|~greater(growth_rate(first_movers,esk2_0),growth_rate(efficient_producers,esk2_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_64, c_0_65]), c_0_30])]), c_0_66])).
% 0.22/0.55 cnf(c_0_71, negated_conjecture, (greater(growth_rate(first_movers,esk2_0),growth_rate(efficient_producers,esk2_0))|~greater_or_equal(difference(growth_rate(first_movers,critical_point(esk1_0)),growth_rate(efficient_producers,critical_point(esk1_0))),zero)|~decreases(difference(growth_rate(first_movers,esk2_0),growth_rate(efficient_producers,esk2_0)))), inference(spm,[status(thm)],[c_0_67, c_0_68])).
% 0.22/0.55 cnf(c_0_72, negated_conjecture, (appear(efficient_producers,esk1_0)=critical_point(esk1_0)|decreases(difference(growth_rate(first_movers,esk2_0),growth_rate(efficient_producers,esk2_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69, c_0_52]), c_0_30])])).
% 0.22/0.55 cnf(c_0_73, negated_conjecture, (subpopulations(first_movers,efficient_producers,esk1_0,X1)|~greater_or_equal(critical_point(esk1_0),X1)|~greater_or_equal(X1,critical_point(esk1_0))), inference(spm,[status(thm)],[c_0_39, c_0_36])).
% 0.22/0.55 cnf(c_0_74, negated_conjecture, (appear(efficient_producers,esk1_0)=critical_point(esk1_0)|~greater_or_equal(difference(growth_rate(first_movers,critical_point(esk1_0)),growth_rate(efficient_producers,critical_point(esk1_0))),zero)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_70, c_0_71]), c_0_72])).
% 0.22/0.55 cnf(c_0_75, negated_conjecture, (subpopulations(first_movers,efficient_producers,esk1_0,X1)|~greater_or_equal(X1,critical_point(esk1_0))|~greater(critical_point(esk1_0),X1)), inference(spm,[status(thm)],[c_0_73, c_0_46])).
% 0.22/0.55 cnf(c_0_76, negated_conjecture, (greater_or_equal(esk2_0,critical_point(esk1_0))|~greater_or_equal(difference(growth_rate(first_movers,critical_point(esk1_0)),growth_rate(efficient_producers,critical_point(esk1_0))),zero)), inference(spm,[status(thm)],[c_0_42, c_0_74])).
% 0.22/0.55 cnf(c_0_77, negated_conjecture, (subpopulations(first_movers,efficient_producers,esk1_0,esk2_0)|~greater_or_equal(difference(growth_rate(first_movers,critical_point(esk1_0)),growth_rate(efficient_producers,critical_point(esk1_0))),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75, c_0_76]), c_0_47])])).
% 0.22/0.55 cnf(c_0_78, negated_conjecture, (subpopulations(efficient_producers,first_movers,esk1_0,esk2_0)|~greater_or_equal(difference(growth_rate(first_movers,critical_point(esk1_0)),growth_rate(efficient_producers,critical_point(esk1_0))),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_59, c_0_77]), c_0_30])])).
% 0.22/0.55 cnf(c_0_79, negated_conjecture, (~greater_or_equal(difference(growth_rate(first_movers,critical_point(esk1_0)),growth_rate(efficient_producers,critical_point(esk1_0))),zero)|~greater(growth_rate(first_movers,esk2_0),growth_rate(efficient_producers,esk2_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_64, c_0_78]), c_0_30])]), c_0_66])).
% 0.22/0.55 fof(c_0_80, hypothesis, ![X1, X10]:(((environment(X1)&X10=critical_point(X1))=>(~greater(growth_rate(efficient_producers,X10),growth_rate(first_movers,X10))&![X4]:(((subpopulations(first_movers,efficient_producers,X1,X4)&greater(X4,X10))=>greater(growth_rate(efficient_producers,X4),growth_rate(first_movers,X4))))))), inference(fof_simplification,[status(thm)],[d1])).
% 0.22/0.55 fof(c_0_81, plain, ![X1, X4]:((((environment(X1)&subpopulations(first_movers,efficient_producers,X1,X4))&~greater(zero,difference(growth_rate(first_movers,X4),growth_rate(efficient_producers,X4))))=>greater_or_equal(difference(growth_rate(first_movers,X4),growth_rate(efficient_producers,X4)),zero))), inference(fof_simplification,[status(thm)],[mp_relationship_of_growth_rates])).
% 0.22/0.55 cnf(c_0_82, hypothesis, (decreases(difference(founding_rate(first_movers,esk2_0),founding_rate(efficient_producers,esk2_0)))|~greater_or_equal(difference(growth_rate(first_movers,critical_point(esk1_0)),growth_rate(efficient_producers,critical_point(esk1_0))),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_77]), c_0_30])])).
% 0.22/0.55 cnf(c_0_83, negated_conjecture, (~greater_or_equal(difference(growth_rate(first_movers,critical_point(esk1_0)),growth_rate(efficient_producers,critical_point(esk1_0))),zero)|~decreases(difference(growth_rate(first_movers,esk2_0),growth_rate(efficient_producers,esk2_0)))), inference(spm,[status(thm)],[c_0_79, c_0_71])).
% 0.22/0.55 fof(c_0_84, hypothesis, ![X43, X44, X45]:(((~greater(growth_rate(efficient_producers,X44),growth_rate(first_movers,X44))|(~environment(X43)|X44!=critical_point(X43)))&(~subpopulations(first_movers,efficient_producers,X43,X45)|~greater(X45,X44)|greater(growth_rate(efficient_producers,X45),growth_rate(first_movers,X45))|(~environment(X43)|X44!=critical_point(X43))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_80])])])])])).
% 0.22/0.55 fof(c_0_85, plain, ![X41, X42]:((~environment(X41)|~subpopulations(first_movers,efficient_producers,X41,X42)|greater(zero,difference(growth_rate(first_movers,X42),growth_rate(efficient_producers,X42)))|greater_or_equal(difference(growth_rate(first_movers,X42),growth_rate(efficient_producers,X42)),zero))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_81])])])).
% 0.22/0.55 cnf(c_0_86, hypothesis, (decreases(difference(disbanding_rate(first_movers,esk2_0),disbanding_rate(efficient_producers,esk2_0)))|~greater_or_equal(difference(growth_rate(first_movers,critical_point(esk1_0)),growth_rate(efficient_producers,critical_point(esk1_0))),zero)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_82]), c_0_83])).
% 0.22/0.55 cnf(c_0_87, hypothesis, (~greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))|~environment(X2)|X1!=critical_point(X2)), inference(split_conjunct,[status(thm)],[c_0_84])).
% 0.22/0.55 fof(c_0_88, plain, ![X23]:(((~greater(zero,difference(growth_rate(first_movers,X23),growth_rate(efficient_producers,X23)))|greater(growth_rate(efficient_producers,X23),growth_rate(first_movers,X23)))&(~greater(growth_rate(efficient_producers,X23),growth_rate(first_movers,X23))|greater(zero,difference(growth_rate(first_movers,X23),growth_rate(efficient_producers,X23)))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_negative_growth_rate_difference])])])).
% 0.22/0.55 cnf(c_0_89, plain, (greater(zero,difference(growth_rate(first_movers,X2),growth_rate(efficient_producers,X2)))|greater_or_equal(difference(growth_rate(first_movers,X2),growth_rate(efficient_producers,X2)),zero)|~environment(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)), inference(split_conjunct,[status(thm)],[c_0_85])).
% 0.22/0.55 cnf(c_0_90, hypothesis, (~greater_or_equal(difference(growth_rate(first_movers,critical_point(esk1_0)),growth_rate(efficient_producers,critical_point(esk1_0))),zero)|~subpopulations(first_movers,efficient_producers,X1,esk2_0)|~environment(X1)), inference(spm,[status(thm)],[c_0_62, c_0_86])).
% 0.22/0.55 cnf(c_0_91, hypothesis, (~greater(growth_rate(efficient_producers,critical_point(X1)),growth_rate(first_movers,critical_point(X1)))|~environment(X1)), inference(er,[status(thm)],[c_0_87])).
% 0.22/0.55 cnf(c_0_92, plain, (greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))|~greater(zero,difference(growth_rate(first_movers,X1),growth_rate(efficient_producers,X1)))), inference(split_conjunct,[status(thm)],[c_0_88])).
% 0.22/0.55 cnf(c_0_93, negated_conjecture, (greater_or_equal(difference(growth_rate(first_movers,critical_point(esk1_0)),growth_rate(efficient_producers,critical_point(esk1_0))),zero)|greater(zero,difference(growth_rate(first_movers,critical_point(esk1_0)),growth_rate(efficient_producers,critical_point(esk1_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_89, c_0_36]), c_0_30])])).
% 0.22/0.55 cnf(c_0_94, negated_conjecture, (~greater_or_equal(difference(growth_rate(first_movers,critical_point(esk1_0)),growth_rate(efficient_producers,critical_point(esk1_0))),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_90, c_0_77]), c_0_30])])).
% 0.22/0.55 cnf(c_0_95, hypothesis, (~greater(zero,difference(growth_rate(first_movers,critical_point(X1)),growth_rate(efficient_producers,critical_point(X1))))|~environment(X1)), inference(spm,[status(thm)],[c_0_91, c_0_92])).
% 0.22/0.55 cnf(c_0_96, negated_conjecture, (greater(zero,difference(growth_rate(first_movers,critical_point(esk1_0)),growth_rate(efficient_producers,critical_point(esk1_0))))), inference(sr,[status(thm)],[c_0_93, c_0_94])).
% 0.22/0.55 cnf(c_0_97, hypothesis, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_95, c_0_96]), c_0_30])]), ['proof']).
% 0.22/0.55 % SZS output end Proof
% 0.22/0.55 % User time : 0.022 s
% 0.22/0.55 % System time : 0.006 s
% 0.22/0.55 % Total time : 0.028 s
% 0.22/0.55 % User time : 0.118 s
% 0.22/0.55 % System time : 0.014 s
% 0.22/0.55 % Total time : 0.132 s
% 0.22/0.55
%------------------------------------------------------------------------------