%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT039+2 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n027.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:33 AM UTC 2026
% Result : Theorem 0.53s 0.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT039+2 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.10/0.35 % Computer : n027.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 7 12:58:45 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.24/0.49 start to proof:theBenchmark.p
% 0.53/0.62 % Version : CSI_E---1.1
% 0.53/0.62 % Problem : theBenchmark.p
% 0.53/0.62 % Proof found!
% 0.53/0.62 % SZS status Theorem for theBenchmark.p
% 0.53/0.62 % SZS output start Proof
% 0.53/0.62 fof(mp_greater_or_equal, axiom, ![X6, X7]:((greater_or_equal(X6,X7)<=>(greater(X6,X7)|X6=X7))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_greater_or_equal)).
% 0.53/0.62 fof(mp_time_of_critical_point, axiom, ![X1]:((environment(X1)=>greater_or_equal(critical_point(X1),start_time(X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_time_of_critical_point)).
% 0.53/0.62 fof(prove_t8, conjecture, ![X5]:(((observational_period(X5)&slow_change(X5))=>selection_favors(efficient_producers,first_movers,X5))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_t8)).
% 0.53/0.62 fof(mp_greater_transitivity, axiom, ![X6, X7, X8]:(((greater(X6,X7)&greater(X7,X8))=>greater(X6,X8))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_greater_transitivity)).
% 0.53/0.62 fof(mp4_critical_point, axiom, ![X5]:(((observational_period(X5)&slow_change(X5))=>![X1]:(((environment(X1)&in_environment(X5,X1))=>?[X4]:((in_environment(X1,X4)&greater(X4,critical_point(X1)))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp4_critical_point)).
% 0.53/0.62 fof(mp_environment_end_point, axiom, ![X1, X4]:(((environment(X1)&in_environment(X1,X4))=>greater_or_equal(end_time(X1),X4))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_environment_end_point)).
% 0.53/0.62 fof(mp_time_in_environment, axiom, ![X1, X4]:((((environment(X1)&greater_or_equal(X4,start_time(X1)))&greater_or_equal(end_time(X1),X4))=>in_environment(X1,X4))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_time_in_environment)).
% 0.53/0.62 fof(mp3_favoured_trategy, axiom, ![X5]:(((((observational_period(X5)&propagation_strategy(first_movers))&propagation_strategy(efficient_producers))&![X1]:(((environment(X1)&in_environment(X5,X1))=>selection_favors(efficient_producers,first_movers,end_time(X1)))))=>selection_favors(efficient_producers,first_movers,X5))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp3_favoured_trategy)).
% 0.53/0.62 fof(mp_critical_point_after_EP, axiom, ![X1]:((environment(X1)=>greater_or_equal(critical_point(X1),appear(efficient_producers,X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_critical_point_after_EP)).
% 0.53/0.62 fof(mp_organizational_sets1, axiom, propagation_strategy(first_movers), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_organizational_sets1)).
% 0.53/0.62 fof(mp_organizational_sets2, axiom, propagation_strategy(efficient_producers), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_organizational_sets2)).
% 0.53/0.62 fof(t6, hypothesis, ![X1, X4]:((((environment(X1)&in_environment(X1,X4))&greater_or_equal(X4,appear(efficient_producers,X1)))=>greater(cardinality_at_time(efficient_producers,X4),zero))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t6)).
% 0.53/0.62 fof(d1, hypothesis, ![X1, X9]:(((environment(X1)&X9=critical_point(X1))=>(~(greater(growth_rate(efficient_producers,X9),growth_rate(first_movers,X9)))&![X4]:(((subpopulations(first_movers,efficient_producers,X1,X4)&greater(X4,X9))=>greater(growth_rate(efficient_producers,X4),growth_rate(first_movers,X4))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1)).
% 0.53/0.62 fof(mp2_favour_members, axiom, ![X1, X2, X3, X4]:((((((environment(X1)&subpopulation(X2,X1,X4))&subpopulation(X3,X1,X4))&greater(cardinality_at_time(X2,X4),zero))&cardinality_at_time(X3,X4)=zero)=>selection_favors(X2,X3,X4))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp2_favour_members)).
% 0.53/0.62 fof(mp_subpopulations, axiom, ![X1, X4]:(((environment(X1)&in_environment(X1,X4))=>(subpopulation(first_movers,X1,X4)&subpopulation(efficient_producers,X1,X4)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_subpopulations)).
% 0.53/0.62 fof(mp_contains_FM_and_EP, axiom, ![X1, X4]:(((((environment(X1)&in_environment(X1,X4))&greater(cardinality_at_time(first_movers,X4),zero))&greater(cardinality_at_time(efficient_producers,X4),zero))=>subpopulations(first_movers,efficient_producers,X1,X4))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_contains_FM_and_EP)).
% 0.53/0.62 fof(mp_first_movers_exist, axiom, ![X1, X4]:(((environment(X1)&in_environment(X1,X4))=>greater_or_equal(cardinality_at_time(first_movers,X4),zero))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_first_movers_exist)).
% 0.53/0.62 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.53/0.62 fof(c_0_18, plain, ![X41, X42]:(((~greater_or_equal(X41,X42)|(greater(X41,X42)|X41=X42))&((~greater(X41,X42)|greater_or_equal(X41,X42))&(X41!=X42|greater_or_equal(X41,X42))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_greater_or_equal])])])])).
% 0.53/0.62 fof(c_0_19, plain, ![X47]:((~environment(X47)|greater_or_equal(critical_point(X47),start_time(X47)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_time_of_critical_point])])])).
% 0.53/0.62 fof(c_0_20, negated_conjecture, ~(![X5]:(((observational_period(X5)&slow_change(X5))=>selection_favors(efficient_producers,first_movers,X5)))), inference(assume_negation,[status(cth)],[prove_t8])).
% 0.53/0.62 fof(c_0_21, plain, ![X36, X37, X38]:((~greater(X36,X37)|~greater(X37,X38)|greater(X36,X38))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_greater_transitivity])])])).
% 0.53/0.62 cnf(c_0_22, plain, (greater(X1,X2)|X1=X2|~greater_or_equal(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_18])).
% 0.53/0.62 cnf(c_0_23, plain, (greater_or_equal(critical_point(X1),start_time(X1))|~environment(X1)), inference(split_conjunct,[status(thm)],[c_0_19])).
% 0.53/0.62 fof(c_0_24, plain, ![X33, X34]:(((in_environment(X34,esk3_2(X33,X34))|(~environment(X34)|~in_environment(X33,X34))|(~observational_period(X33)|~slow_change(X33)))&(greater(esk3_2(X33,X34),critical_point(X34))|(~environment(X34)|~in_environment(X33,X34))|(~observational_period(X33)|~slow_change(X33))))), 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)],[mp4_critical_point])])])])])])).
% 0.53/0.62 fof(c_0_25, negated_conjecture, ((observational_period(esk1_0)&slow_change(esk1_0))&~selection_favors(efficient_producers,first_movers,esk1_0)), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_20])])])])).
% 0.53/0.62 cnf(c_0_26, plain, (greater(X1,X3)|~greater(X1,X2)|~greater(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.53/0.62 cnf(c_0_27, plain, (start_time(X1)=critical_point(X1)|greater(critical_point(X1),start_time(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_22, c_0_23])).
% 0.53/0.62 fof(c_0_28, plain, ![X45, X46]:((~environment(X45)|~in_environment(X45,X46)|greater_or_equal(end_time(X45),X46))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_environment_end_point])])])).
% 0.53/0.62 cnf(c_0_29, plain, (in_environment(X1,esk3_2(X2,X1))|~environment(X1)|~in_environment(X2,X1)|~observational_period(X2)|~slow_change(X2)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 0.53/0.62 cnf(c_0_30, negated_conjecture, (slow_change(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 0.53/0.62 cnf(c_0_31, negated_conjecture, (observational_period(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 0.53/0.62 cnf(c_0_32, plain, (start_time(X1)=critical_point(X1)|greater(X2,start_time(X1))|~greater(X2,critical_point(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_26, c_0_27])).
% 0.53/0.62 cnf(c_0_33, plain, (greater(esk3_2(X1,X2),critical_point(X2))|~environment(X2)|~in_environment(X1,X2)|~observational_period(X1)|~slow_change(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 0.53/0.62 cnf(c_0_34, plain, (greater_or_equal(end_time(X1),X2)|~environment(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_28])).
% 0.53/0.62 cnf(c_0_35, negated_conjecture, (in_environment(X1,esk3_2(esk1_0,X1))|~in_environment(esk1_0,X1)|~environment(X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29, c_0_30]), c_0_31])])).
% 0.53/0.62 fof(c_0_36, plain, ![X43, X44]:((~environment(X43)|~greater_or_equal(X44,start_time(X43))|~greater_or_equal(end_time(X43),X44)|in_environment(X43,X44))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_time_in_environment])])])).
% 0.53/0.62 cnf(c_0_37, plain, (start_time(X1)=critical_point(X1)|greater(X2,start_time(X1))|~greater(X3,critical_point(X1))|~greater(X2,X3)|~environment(X1)), inference(spm,[status(thm)],[c_0_26, c_0_32])).
% 0.53/0.62 cnf(c_0_38, negated_conjecture, (greater(esk3_2(esk1_0,X1),critical_point(X1))|~in_environment(esk1_0,X1)|~environment(X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_33, c_0_30]), c_0_31])])).
% 0.53/0.62 cnf(c_0_39, negated_conjecture, (greater_or_equal(end_time(X1),esk3_2(esk1_0,X1))|~in_environment(esk1_0,X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_34, c_0_35])).
% 0.53/0.62 cnf(c_0_40, plain, (in_environment(X1,X2)|~environment(X1)|~greater_or_equal(X2,start_time(X1))|~greater_or_equal(end_time(X1),X2)), inference(split_conjunct,[status(thm)],[c_0_36])).
% 0.53/0.62 cnf(c_0_41, plain, (greater_or_equal(X1,X2)|~greater(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_18])).
% 0.53/0.62 cnf(c_0_42, plain, (greater_or_equal(X1,X2)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_18])).
% 0.53/0.62 fof(c_0_43, plain, ![X19]:((((environment(esk2_1(X19))|(~observational_period(X19)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers))|selection_favors(efficient_producers,first_movers,X19))&(in_environment(X19,esk2_1(X19))|(~observational_period(X19)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers))|selection_favors(efficient_producers,first_movers,X19)))&(~selection_favors(efficient_producers,first_movers,end_time(esk2_1(X19)))|(~observational_period(X19)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers))|selection_favors(efficient_producers,first_movers,X19)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp3_favoured_trategy])])])])])).
% 0.53/0.62 fof(c_0_44, plain, ![X30]:((~environment(X30)|greater_or_equal(critical_point(X30),appear(efficient_producers,X30)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_critical_point_after_EP])])])).
% 0.53/0.62 cnf(c_0_45, negated_conjecture, (start_time(X1)=critical_point(X1)|greater(X2,start_time(X1))|~in_environment(esk1_0,X1)|~greater(X2,esk3_2(esk1_0,X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_37, c_0_38])).
% 0.53/0.62 cnf(c_0_46, negated_conjecture, (esk3_2(esk1_0,X1)=end_time(X1)|greater(end_time(X1),esk3_2(esk1_0,X1))|~in_environment(esk1_0,X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_22, c_0_39])).
% 0.53/0.62 cnf(c_0_47, plain, (in_environment(X1,X2)|~greater_or_equal(end_time(X1),X2)|~greater(X2,start_time(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_40, c_0_41])).
% 0.53/0.62 cnf(c_0_48, plain, (greater_or_equal(X1,X1)), inference(er,[status(thm)],[c_0_42])).
% 0.53/0.62 cnf(c_0_49, plain, (in_environment(X1,esk2_1(X1))|selection_favors(efficient_producers,first_movers,X1)|~observational_period(X1)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)), inference(split_conjunct,[status(thm)],[c_0_43])).
% 0.53/0.62 cnf(c_0_50, plain, (propagation_strategy(first_movers)), inference(split_conjunct,[status(thm)],[mp_organizational_sets1])).
% 0.53/0.62 cnf(c_0_51, plain, (propagation_strategy(efficient_producers)), inference(split_conjunct,[status(thm)],[mp_organizational_sets2])).
% 0.53/0.62 cnf(c_0_52, plain, (environment(esk2_1(X1))|selection_favors(efficient_producers,first_movers,X1)|~observational_period(X1)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)), inference(split_conjunct,[status(thm)],[c_0_43])).
% 0.53/0.62 cnf(c_0_53, negated_conjecture, (greater(X1,critical_point(X2))|~in_environment(esk1_0,X2)|~greater(X1,esk3_2(esk1_0,X2))|~environment(X2)), inference(spm,[status(thm)],[c_0_26, c_0_38])).
% 0.53/0.62 fof(c_0_54, hypothesis, ![X31, X32]:((~environment(X31)|~in_environment(X31,X32)|~greater_or_equal(X32,appear(efficient_producers,X31))|greater(cardinality_at_time(efficient_producers,X32),zero))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t6])])])).
% 0.53/0.62 cnf(c_0_55, plain, (greater_or_equal(critical_point(X1),appear(efficient_producers,X1))|~environment(X1)), inference(split_conjunct,[status(thm)],[c_0_44])).
% 0.53/0.62 cnf(c_0_56, negated_conjecture, (esk3_2(esk1_0,X1)=end_time(X1)|start_time(X1)=critical_point(X1)|greater(end_time(X1),start_time(X1))|~in_environment(esk1_0,X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_45, c_0_46])).
% 0.53/0.62 cnf(c_0_57, plain, (in_environment(X1,end_time(X1))|~greater(end_time(X1),start_time(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_47, c_0_48])).
% 0.53/0.62 cnf(c_0_58, plain, (in_environment(X1,esk2_1(X1))|selection_favors(efficient_producers,first_movers,X1)|~observational_period(X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_49, c_0_50]), c_0_51])])).
% 0.53/0.62 cnf(c_0_59, negated_conjecture, (~selection_favors(efficient_producers,first_movers,esk1_0)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 0.53/0.62 cnf(c_0_60, plain, (selection_favors(efficient_producers,first_movers,X1)|environment(esk2_1(X1))|~observational_period(X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_52, c_0_50]), c_0_51])])).
% 0.53/0.62 cnf(c_0_61, negated_conjecture, (esk3_2(esk1_0,X1)=end_time(X1)|greater(end_time(X1),critical_point(X1))|~in_environment(esk1_0,X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_53, c_0_46])).
% 0.53/0.62 fof(c_0_62, hypothesis, ![X1, X9]:(((environment(X1)&X9=critical_point(X1))=>(~greater(growth_rate(efficient_producers,X9),growth_rate(first_movers,X9))&![X4]:(((subpopulations(first_movers,efficient_producers,X1,X4)&greater(X4,X9))=>greater(growth_rate(efficient_producers,X4),growth_rate(first_movers,X4))))))), inference(fof_simplification,[status(thm)],[d1])).
% 0.53/0.62 cnf(c_0_63, hypothesis, (greater(cardinality_at_time(efficient_producers,X2),zero)|~environment(X1)|~in_environment(X1,X2)|~greater_or_equal(X2,appear(efficient_producers,X1))), inference(split_conjunct,[status(thm)],[c_0_54])).
% 0.53/0.62 cnf(c_0_64, plain, (appear(efficient_producers,X1)=critical_point(X1)|greater(critical_point(X1),appear(efficient_producers,X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_22, c_0_55])).
% 0.53/0.62 cnf(c_0_65, negated_conjecture, (start_time(X1)=critical_point(X1)|in_environment(X1,end_time(X1))|~in_environment(esk1_0,X1)|~environment(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_56]), c_0_57])).
% 0.53/0.62 cnf(c_0_66, negated_conjecture, (in_environment(esk1_0,esk2_1(esk1_0))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_31]), c_0_59])).
% 0.53/0.62 cnf(c_0_67, negated_conjecture, (environment(esk2_1(esk1_0))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_31]), c_0_59])).
% 0.53/0.62 cnf(c_0_68, negated_conjecture, (greater(end_time(X1),critical_point(X1))|~in_environment(esk1_0,X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_38, c_0_61])).
% 0.53/0.62 fof(c_0_69, hypothesis, ![X27, X28, X29]:(((~greater(growth_rate(efficient_producers,X28),growth_rate(first_movers,X28))|(~environment(X27)|X28!=critical_point(X27)))&(~subpopulations(first_movers,efficient_producers,X27,X29)|~greater(X29,X28)|greater(growth_rate(efficient_producers,X29),growth_rate(first_movers,X29))|(~environment(X27)|X28!=critical_point(X27))))), 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_62])])])])])).
% 0.53/0.62 fof(c_0_70, plain, ![X15, X16, X17, X18]:((~environment(X15)|~subpopulation(X16,X15,X18)|~subpopulation(X17,X15,X18)|~greater(cardinality_at_time(X16,X18),zero)|cardinality_at_time(X17,X18)!=zero|selection_favors(X16,X17,X18))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp2_favour_members])])])).
% 0.53/0.62 fof(c_0_71, plain, ![X25, X26]:(((subpopulation(first_movers,X25,X26)|(~environment(X25)|~in_environment(X25,X26)))&(subpopulation(efficient_producers,X25,X26)|(~environment(X25)|~in_environment(X25,X26))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_subpopulations])])])])).
% 0.53/0.62 cnf(c_0_72, hypothesis, (greater(cardinality_at_time(efficient_producers,X1),zero)|~in_environment(X2,X1)|~greater(X1,appear(efficient_producers,X2))|~environment(X2)), inference(spm,[status(thm)],[c_0_63, c_0_41])).
% 0.53/0.62 cnf(c_0_73, plain, (appear(efficient_producers,X1)=critical_point(X1)|greater(X2,appear(efficient_producers,X1))|~greater(X2,critical_point(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_26, c_0_64])).
% 0.53/0.62 cnf(c_0_74, negated_conjecture, (start_time(esk2_1(esk1_0))=critical_point(esk2_1(esk1_0))|in_environment(esk2_1(esk1_0),end_time(esk2_1(esk1_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_66]), c_0_67])])).
% 0.53/0.62 cnf(c_0_75, negated_conjecture, (greater(end_time(esk2_1(esk1_0)),critical_point(esk2_1(esk1_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_66]), c_0_67])])).
% 0.53/0.62 cnf(c_0_76, plain, (in_environment(X1,critical_point(X1))|~greater_or_equal(end_time(X1),critical_point(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_40, c_0_23])).
% 0.53/0.62 cnf(c_0_77, hypothesis, (greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|~subpopulations(first_movers,efficient_producers,X1,X2)|~greater(X2,X3)|~environment(X1)|X3!=critical_point(X1)), inference(split_conjunct,[status(thm)],[c_0_69])).
% 0.53/0.62 fof(c_0_78, plain, ![X21, X22]:((~environment(X21)|~in_environment(X21,X22)|~greater(cardinality_at_time(first_movers,X22),zero)|~greater(cardinality_at_time(efficient_producers,X22),zero)|subpopulations(first_movers,efficient_producers,X21,X22))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_contains_FM_and_EP])])])).
% 0.53/0.62 cnf(c_0_79, plain, (selection_favors(X2,X4,X3)|~environment(X1)|~subpopulation(X2,X1,X3)|~subpopulation(X4,X1,X3)|~greater(cardinality_at_time(X2,X3),zero)|cardinality_at_time(X4,X3)!=zero), inference(split_conjunct,[status(thm)],[c_0_70])).
% 0.53/0.62 cnf(c_0_80, plain, (subpopulation(first_movers,X1,X2)|~environment(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_71])).
% 0.53/0.62 cnf(c_0_81, plain, (selection_favors(efficient_producers,first_movers,X1)|~selection_favors(efficient_producers,first_movers,end_time(esk2_1(X1)))|~observational_period(X1)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)), inference(split_conjunct,[status(thm)],[c_0_43])).
% 0.53/0.62 cnf(c_0_82, hypothesis, (appear(efficient_producers,X1)=critical_point(X1)|greater(cardinality_at_time(efficient_producers,X2),zero)|~in_environment(X1,X2)|~greater(X2,critical_point(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_72, c_0_73])).
% 0.53/0.62 cnf(c_0_83, negated_conjecture, (in_environment(esk2_1(esk1_0),end_time(esk2_1(esk1_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57, c_0_74]), c_0_75]), c_0_67])])).
% 0.53/0.62 cnf(c_0_84, plain, (in_environment(X1,critical_point(X1))|~greater(end_time(X1),critical_point(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_76, c_0_41])).
% 0.53/0.62 cnf(c_0_85, hypothesis, (greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))|~greater(X1,critical_point(X2))|~subpopulations(first_movers,efficient_producers,X2,X1)|~environment(X2)), inference(er,[status(thm)],[c_0_77])).
% 0.53/0.62 cnf(c_0_86, plain, (subpopulations(first_movers,efficient_producers,X1,X2)|~environment(X1)|~in_environment(X1,X2)|~greater(cardinality_at_time(first_movers,X2),zero)|~greater(cardinality_at_time(efficient_producers,X2),zero)), inference(split_conjunct,[status(thm)],[c_0_78])).
% 0.53/0.62 fof(c_0_87, plain, ![X23, X24]:((~environment(X23)|~in_environment(X23,X24)|greater_or_equal(cardinality_at_time(first_movers,X24),zero))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_first_movers_exist])])])).
% 0.53/0.62 cnf(c_0_88, plain, (selection_favors(X1,first_movers,X2)|cardinality_at_time(first_movers,X2)!=zero|~in_environment(X3,X2)|~subpopulation(X1,X3,X2)|~greater(cardinality_at_time(X1,X2),zero)|~environment(X3)), inference(spm,[status(thm)],[c_0_79, c_0_80])).
% 0.53/0.62 cnf(c_0_89, plain, (subpopulation(efficient_producers,X1,X2)|~environment(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_71])).
% 0.53/0.62 cnf(c_0_90, plain, (selection_favors(efficient_producers,first_movers,X1)|~observational_period(X1)|~selection_favors(efficient_producers,first_movers,end_time(esk2_1(X1)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_81, c_0_50]), c_0_51])])).
% 0.53/0.62 cnf(c_0_91, negated_conjecture, (appear(efficient_producers,esk2_1(esk1_0))=critical_point(esk2_1(esk1_0))|greater(cardinality_at_time(efficient_producers,end_time(esk2_1(esk1_0))),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82, c_0_75]), c_0_83]), c_0_67])])).
% 0.53/0.62 cnf(c_0_92, negated_conjecture, (in_environment(esk2_1(esk1_0),critical_point(esk2_1(esk1_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_84, c_0_75]), c_0_67])])).
% 0.53/0.62 cnf(c_0_93, hypothesis, (greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))|~in_environment(X2,X1)|~greater(cardinality_at_time(first_movers,X1),zero)|~greater(cardinality_at_time(efficient_producers,X1),zero)|~greater(X1,critical_point(X2))|~environment(X2)), inference(spm,[status(thm)],[c_0_85, c_0_86])).
% 0.53/0.62 cnf(c_0_94, plain, (greater_or_equal(cardinality_at_time(first_movers,X2),zero)|~environment(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_87])).
% 0.53/0.62 cnf(c_0_95, plain, (selection_favors(efficient_producers,first_movers,X1)|cardinality_at_time(first_movers,X1)!=zero|~in_environment(X2,X1)|~greater(cardinality_at_time(efficient_producers,X1),zero)|~environment(X2)), inference(spm,[status(thm)],[c_0_88, c_0_89])).
% 0.53/0.62 cnf(c_0_96, negated_conjecture, (~selection_favors(efficient_producers,first_movers,end_time(esk2_1(esk1_0)))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_90, c_0_31]), c_0_59])).
% 0.53/0.62 cnf(c_0_97, hypothesis, (greater(cardinality_at_time(efficient_producers,end_time(esk2_1(esk1_0))),zero)|greater(cardinality_at_time(efficient_producers,X1),zero)|~greater_or_equal(X1,critical_point(esk2_1(esk1_0)))|~in_environment(esk2_1(esk1_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_91]), c_0_67])])).
% 0.53/0.62 cnf(c_0_98, negated_conjecture, (greater_or_equal(end_time(esk2_1(esk1_0)),critical_point(esk2_1(esk1_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_92]), c_0_67])])).
% 0.53/0.62 cnf(c_0_99, hypothesis, (greater(growth_rate(efficient_producers,end_time(esk2_1(esk1_0))),growth_rate(first_movers,end_time(esk2_1(esk1_0))))|~in_environment(esk2_1(esk1_0),end_time(esk2_1(esk1_0)))|~greater(cardinality_at_time(first_movers,end_time(esk2_1(esk1_0))),zero)|~greater(cardinality_at_time(efficient_producers,end_time(esk2_1(esk1_0))),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_93, c_0_75]), c_0_67])])).
% 0.53/0.62 cnf(c_0_100, negated_conjecture, (greater_or_equal(cardinality_at_time(first_movers,end_time(esk2_1(esk1_0))),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_94, c_0_83]), c_0_67])])).
% 0.53/0.62 cnf(c_0_101, negated_conjecture, (cardinality_at_time(first_movers,end_time(esk2_1(esk1_0)))!=zero|~greater(cardinality_at_time(efficient_producers,end_time(esk2_1(esk1_0))),zero)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_95, c_0_83]), c_0_67])]), c_0_96])).
% 0.53/0.62 cnf(c_0_102, negated_conjecture, (greater(cardinality_at_time(efficient_producers,end_time(esk2_1(esk1_0))),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_97, c_0_98]), c_0_83])])).
% 0.53/0.62 fof(c_0_103, 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.53/0.62 cnf(c_0_104, hypothesis, (greater(growth_rate(efficient_producers,end_time(esk2_1(esk1_0))),growth_rate(first_movers,end_time(esk2_1(esk1_0))))|~greater(cardinality_at_time(first_movers,end_time(esk2_1(esk1_0))),zero)|~greater(cardinality_at_time(efficient_producers,end_time(esk2_1(esk1_0))),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_99, c_0_83])])).
% 0.53/0.62 cnf(c_0_105, negated_conjecture, (cardinality_at_time(first_movers,end_time(esk2_1(esk1_0)))=zero|greater(cardinality_at_time(first_movers,end_time(esk2_1(esk1_0))),zero)), inference(spm,[status(thm)],[c_0_22, c_0_100])).
% 0.53/0.62 cnf(c_0_106, negated_conjecture, (cardinality_at_time(first_movers,end_time(esk2_1(esk1_0)))!=zero), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_101, c_0_102])])).
% 0.53/0.62 cnf(c_0_107, 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_103])).
% 0.53/0.62 cnf(c_0_108, hypothesis, (greater(growth_rate(efficient_producers,end_time(esk2_1(esk1_0))),growth_rate(first_movers,end_time(esk2_1(esk1_0))))|~greater(cardinality_at_time(first_movers,end_time(esk2_1(esk1_0))),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_104, c_0_102])])).
% 0.53/0.62 cnf(c_0_109, negated_conjecture, (greater(cardinality_at_time(first_movers,end_time(esk2_1(esk1_0))),zero)), inference(sr,[status(thm)],[c_0_105, c_0_106])).
% 0.53/0.62 cnf(c_0_110, plain, (selection_favors(efficient_producers,first_movers,X1)|~in_environment(X2,X1)|~greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))|~greater(cardinality_at_time(first_movers,X1),zero)|~greater(cardinality_at_time(efficient_producers,X1),zero)|~environment(X2)), inference(spm,[status(thm)],[c_0_107, c_0_86])).
% 0.53/0.62 cnf(c_0_111, hypothesis, (greater(growth_rate(efficient_producers,end_time(esk2_1(esk1_0))),growth_rate(first_movers,end_time(esk2_1(esk1_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_108, c_0_109])])).
% 0.53/0.62 cnf(c_0_112, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_110, c_0_83]), c_0_67])]), c_0_96]), c_0_111]), c_0_109]), c_0_102])]), ['proof']).
% 0.53/0.62 % SZS output end Proof
% 0.53/0.62 % User time : 0.015 s
% 0.53/0.62 % System time : 0.003 s
% 0.53/0.62 % Total time : 0.019 s
% 0.53/0.62 % User time : 0.017 s
% 0.53/0.62 % System time : 0.005 s
% 0.53/0.62 % Total time : 0.022 s
% 0.53/0.62
%------------------------------------------------------------------------------