%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT039-2 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n007.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 : Unsatisfiable 0.56s 0.57s
% 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.4.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.09/0.35 % Computer : n007.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:54:56 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.23/0.47 start to proof:theBenchmark.p
% 0.56/0.57 % Version : CSI_E---1.1
% 0.56/0.57 % Problem : theBenchmark.p
% 0.56/0.57 % Proof found!
% 0.56/0.57 # SZS status Unsatisfiable
% 0.56/0.57 % SZS output start Proof
% 0.56/0.57 cnf(mp_greater_or_equal_52, axiom, (greater(X1,X2)|X1=X2|~greater_or_equal(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_greater_or_equal_52)).
% 0.56/0.57 cnf(mp_time_of_critical_point_49, axiom, (greater_or_equal(critical_point(X1),start_time(X1))|~environment(X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_time_of_critical_point_49)).
% 0.56/0.57 cnf(mp_greater_transitivity_50, axiom, (greater(X1,X3)|~greater(X1,X2)|~greater(X2,X3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_greater_transitivity_50)).
% 0.56/0.57 cnf(mp4_critical_point_38, axiom, (in_environment(X2,sk2(X2,X1))|~observational_period(X1)|~slow_change(X1)|~environment(X2)|~in_environment(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp4_critical_point_38)).
% 0.56/0.57 cnf(mp4_critical_point_39, axiom, (greater(sk2(X2,X1),critical_point(X2))|~observational_period(X1)|~slow_change(X1)|~environment(X2)|~in_environment(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp4_critical_point_39)).
% 0.56/0.57 cnf(mp_environment_end_point_43, axiom, (greater_or_equal(end_time(X1),X2)|~environment(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_environment_end_point_43)).
% 0.56/0.57 cnf(prove_t8_59, negated_conjecture, (slow_change(sk3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_t8_59)).
% 0.56/0.57 cnf(prove_t8_58, negated_conjecture, (observational_period(sk3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_t8_58)).
% 0.56/0.57 cnf(mp_time_in_environment_42, axiom, (in_environment(X1,X2)|~environment(X1)|~greater_or_equal(X2,start_time(X1))|~greater_or_equal(end_time(X1),X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_time_in_environment_42)).
% 0.56/0.57 cnf(mp_greater_or_equal_53, axiom, (greater_or_equal(X1,X2)|~greater(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_greater_or_equal_53)).
% 0.56/0.57 cnf(mp_greater_or_equal_54, axiom, (greater_or_equal(X1,X2)|X1!=X2), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_greater_or_equal_54)).
% 0.56/0.57 cnf(mp3_favoured_trategy_36, axiom, (in_environment(X1,sk1(X1))|selection_favors(efficient_producers,first_movers,X1)|~observational_period(X1)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp3_favoured_trategy_36)).
% 0.56/0.57 cnf(mp3_favoured_trategy_35, axiom, (environment(sk1(X1))|selection_favors(efficient_producers,first_movers,X1)|~observational_period(X1)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp3_favoured_trategy_35)).
% 0.56/0.57 cnf(mp_critical_point_after_EP_48, axiom, (greater_or_equal(critical_point(X1),appear(efficient_producers,X1))|~environment(X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_critical_point_after_EP_48)).
% 0.56/0.57 cnf(mp_organizational_sets1_40, axiom, (propagation_strategy(first_movers)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_organizational_sets1_40)).
% 0.56/0.57 cnf(mp_organizational_sets2_41, axiom, (propagation_strategy(efficient_producers)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_organizational_sets2_41)).
% 0.56/0.57 cnf(prove_t8_60, negated_conjecture, (~selection_favors(efficient_producers,first_movers,sk3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_t8_60)).
% 0.56/0.57 cnf(t6_57, hypothesis, (greater(cardinality_at_time(efficient_producers,X2),zero)|~environment(X1)|~in_environment(X1,X2)|~greater_or_equal(X2,appear(efficient_producers,X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t6_57)).
% 0.56/0.57 cnf(d1_56, hypothesis, (greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3))|~environment(X1)|X2!=critical_point(X1)|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater(X3,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_56)).
% 0.56/0.57 cnf(mp2_favour_members_34, axiom, (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), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp2_favour_members_34)).
% 0.56/0.57 cnf(mp_subpopulations_46, axiom, (subpopulation(first_movers,X1,X2)|~environment(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_subpopulations_46)).
% 0.56/0.57 cnf(mp3_favoured_trategy_37, axiom, (selection_favors(efficient_producers,first_movers,X1)|~observational_period(X1)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)|~selection_favors(efficient_producers,first_movers,end_time(sk1(X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp3_favoured_trategy_37)).
% 0.56/0.57 cnf(mp_contains_FM_and_EP_44, axiom, (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)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_contains_FM_and_EP_44)).
% 0.56/0.57 cnf(mp_subpopulations_47, axiom, (subpopulation(efficient_producers,X1,X2)|~environment(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_subpopulations_47)).
% 0.56/0.57 cnf(mp_first_movers_exist_45, axiom, (greater_or_equal(cardinality_at_time(first_movers,X2),zero)|~environment(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_first_movers_exist_45)).
% 0.56/0.57 cnf(mp1_high_growth_rates_33, axiom, (selection_favors(X3,X2,X4)|~environment(X1)|~subpopulations(X2,X3,X1,X4)|~greater(growth_rate(X3,X4),growth_rate(X2,X4))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp1_high_growth_rates_33)).
% 0.56/0.57 cnf(c_0_26, plain, (greater(X1,X2)|X1=X2|~greater_or_equal(X1,X2)), inference(fof_simplification,[status(thm)],[mp_greater_or_equal_52])).
% 0.56/0.57 cnf(c_0_27, plain, (greater_or_equal(critical_point(X1),start_time(X1))|~environment(X1)), inference(fof_simplification,[status(thm)],[mp_time_of_critical_point_49])).
% 0.56/0.57 cnf(c_0_28, plain, (greater(X1,X3)|~greater(X1,X2)|~greater(X2,X3)), inference(fof_simplification,[status(thm)],[mp_greater_transitivity_50])).
% 0.56/0.57 cnf(c_0_29, plain, (greater(X1,X2)|X1=X2|~greater_or_equal(X1,X2)), c_0_26).
% 0.56/0.57 cnf(c_0_30, plain, (greater_or_equal(critical_point(X1),start_time(X1))|~environment(X1)), c_0_27).
% 0.56/0.57 cnf(c_0_31, plain, (in_environment(X2,sk2(X2,X1))|~observational_period(X1)|~slow_change(X1)|~environment(X2)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp4_critical_point_38])).
% 0.56/0.57 cnf(c_0_32, plain, (greater(X1,X3)|~greater(X1,X2)|~greater(X2,X3)), c_0_28).
% 0.56/0.57 cnf(c_0_33, plain, (start_time(X1)=critical_point(X1)|greater(critical_point(X1),start_time(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_29, c_0_30])).
% 0.56/0.57 cnf(c_0_34, plain, (greater(sk2(X2,X1),critical_point(X2))|~observational_period(X1)|~slow_change(X1)|~environment(X2)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp4_critical_point_39])).
% 0.56/0.57 cnf(c_0_35, plain, (greater_or_equal(end_time(X1),X2)|~environment(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp_environment_end_point_43])).
% 0.56/0.57 cnf(c_0_36, plain, (in_environment(X2,sk2(X2,X1))|~observational_period(X1)|~slow_change(X1)|~environment(X2)|~in_environment(X1,X2)), c_0_31).
% 0.56/0.57 cnf(c_0_37, negated_conjecture, (slow_change(sk3)), prove_t8_59).
% 0.56/0.57 cnf(c_0_38, negated_conjecture, (observational_period(sk3)), prove_t8_58).
% 0.56/0.57 cnf(c_0_39, 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_32, c_0_33])).
% 0.56/0.57 cnf(c_0_40, plain, (greater(sk2(X2,X1),critical_point(X2))|~observational_period(X1)|~slow_change(X1)|~environment(X2)|~in_environment(X1,X2)), c_0_34).
% 0.56/0.57 cnf(c_0_41, plain, (greater_or_equal(end_time(X1),X2)|~environment(X1)|~in_environment(X1,X2)), c_0_35).
% 0.56/0.57 cnf(c_0_42, negated_conjecture, (in_environment(X1,sk2(X1,sk3))|~in_environment(sk3,X1)|~environment(X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36, c_0_37]), c_0_38])])).
% 0.56/0.57 cnf(c_0_43, plain, (in_environment(X1,X2)|~environment(X1)|~greater_or_equal(X2,start_time(X1))|~greater_or_equal(end_time(X1),X2)), inference(fof_simplification,[status(thm)],[mp_time_in_environment_42])).
% 0.56/0.57 cnf(c_0_44, plain, (greater_or_equal(X1,X2)|~greater(X1,X2)), inference(fof_simplification,[status(thm)],[mp_greater_or_equal_53])).
% 0.56/0.57 cnf(c_0_45, plain, (greater_or_equal(X1,X2)|X1!=X2), inference(fof_simplification,[status(thm)],[mp_greater_or_equal_54])).
% 0.56/0.57 cnf(c_0_46, 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_32, c_0_39])).
% 0.56/0.57 cnf(c_0_47, negated_conjecture, (greater(sk2(X1,sk3),critical_point(X1))|~in_environment(sk3,X1)|~environment(X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_37]), c_0_38])])).
% 0.56/0.57 cnf(c_0_48, negated_conjecture, (greater_or_equal(end_time(X1),sk2(X1,sk3))|~in_environment(sk3,X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_41, c_0_42])).
% 0.56/0.57 cnf(c_0_49, plain, (in_environment(X1,X2)|~environment(X1)|~greater_or_equal(X2,start_time(X1))|~greater_or_equal(end_time(X1),X2)), c_0_43).
% 0.56/0.57 cnf(c_0_50, plain, (greater_or_equal(X1,X2)|~greater(X1,X2)), c_0_44).
% 0.56/0.57 cnf(c_0_51, plain, (greater_or_equal(X1,X2)|X1!=X2), c_0_45).
% 0.56/0.57 cnf(c_0_52, plain, (in_environment(X1,sk1(X1))|selection_favors(efficient_producers,first_movers,X1)|~observational_period(X1)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)), inference(fof_simplification,[status(thm)],[mp3_favoured_trategy_36])).
% 0.56/0.57 cnf(c_0_53, plain, (environment(sk1(X1))|selection_favors(efficient_producers,first_movers,X1)|~observational_period(X1)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)), inference(fof_simplification,[status(thm)],[mp3_favoured_trategy_35])).
% 0.56/0.57 cnf(c_0_54, plain, (greater_or_equal(critical_point(X1),appear(efficient_producers,X1))|~environment(X1)), inference(fof_simplification,[status(thm)],[mp_critical_point_after_EP_48])).
% 0.56/0.57 cnf(c_0_55, negated_conjecture, (start_time(X1)=critical_point(X1)|greater(X2,start_time(X1))|~in_environment(sk3,X1)|~greater(X2,sk2(X1,sk3))|~environment(X1)), inference(spm,[status(thm)],[c_0_46, c_0_47])).
% 0.56/0.57 cnf(c_0_56, negated_conjecture, (sk2(X1,sk3)=end_time(X1)|greater(end_time(X1),sk2(X1,sk3))|~in_environment(sk3,X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_29, c_0_48])).
% 0.56/0.57 cnf(c_0_57, 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_49, c_0_50])).
% 0.56/0.57 cnf(c_0_58, plain, (greater_or_equal(X1,X1)), inference(er,[status(thm)],[c_0_51])).
% 0.56/0.57 cnf(c_0_59, plain, (in_environment(X1,sk1(X1))|selection_favors(efficient_producers,first_movers,X1)|~observational_period(X1)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)), c_0_52).
% 0.56/0.57 cnf(c_0_60, axiom, (propagation_strategy(first_movers)), mp_organizational_sets1_40).
% 0.56/0.57 cnf(c_0_61, axiom, (propagation_strategy(efficient_producers)), mp_organizational_sets2_41).
% 0.56/0.57 cnf(c_0_62, negated_conjecture, (~selection_favors(efficient_producers,first_movers,sk3)), inference(fof_simplification,[status(thm)],[prove_t8_60])).
% 0.56/0.57 cnf(c_0_63, plain, (environment(sk1(X1))|selection_favors(efficient_producers,first_movers,X1)|~observational_period(X1)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)), c_0_53).
% 0.56/0.57 cnf(c_0_64, negated_conjecture, (greater(X1,critical_point(X2))|~in_environment(sk3,X2)|~greater(X1,sk2(X2,sk3))|~environment(X2)), inference(spm,[status(thm)],[c_0_32, c_0_47])).
% 0.56/0.57 cnf(c_0_65, hypothesis, (greater(cardinality_at_time(efficient_producers,X2),zero)|~environment(X1)|~in_environment(X1,X2)|~greater_or_equal(X2,appear(efficient_producers,X1))), inference(fof_simplification,[status(thm)],[t6_57])).
% 0.56/0.57 cnf(c_0_66, plain, (greater_or_equal(critical_point(X1),appear(efficient_producers,X1))|~environment(X1)), c_0_54).
% 0.56/0.57 cnf(c_0_67, negated_conjecture, (sk2(X1,sk3)=end_time(X1)|start_time(X1)=critical_point(X1)|greater(end_time(X1),start_time(X1))|~in_environment(sk3,X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_55, c_0_56])).
% 0.56/0.57 cnf(c_0_68, plain, (in_environment(X1,end_time(X1))|~greater(end_time(X1),start_time(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_57, c_0_58])).
% 0.56/0.57 cnf(c_0_69, plain, (in_environment(X1,sk1(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_59, c_0_60]), c_0_61])])).
% 0.56/0.57 cnf(c_0_70, negated_conjecture, (~selection_favors(efficient_producers,first_movers,sk3)), c_0_62).
% 0.56/0.57 cnf(c_0_71, plain, (selection_favors(efficient_producers,first_movers,X1)|environment(sk1(X1))|~observational_period(X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_63, c_0_60]), c_0_61])])).
% 0.56/0.57 cnf(c_0_72, negated_conjecture, (sk2(X1,sk3)=end_time(X1)|greater(end_time(X1),critical_point(X1))|~in_environment(sk3,X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_64, c_0_56])).
% 0.56/0.57 cnf(c_0_73, hypothesis, (greater(cardinality_at_time(efficient_producers,X2),zero)|~environment(X1)|~in_environment(X1,X2)|~greater_or_equal(X2,appear(efficient_producers,X1))), c_0_65).
% 0.56/0.57 cnf(c_0_74, plain, (appear(efficient_producers,X1)=critical_point(X1)|greater(critical_point(X1),appear(efficient_producers,X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_29, c_0_66])).
% 0.56/0.57 cnf(c_0_75, negated_conjecture, (start_time(X1)=critical_point(X1)|in_environment(X1,end_time(X1))|~in_environment(sk3,X1)|~environment(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_67]), c_0_68])).
% 0.56/0.57 cnf(c_0_76, negated_conjecture, (in_environment(sk3,sk1(sk3))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_69, c_0_38]), c_0_70])).
% 0.56/0.57 cnf(c_0_77, negated_conjecture, (environment(sk1(sk3))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_71, c_0_38]), c_0_70])).
% 0.56/0.57 cnf(c_0_78, negated_conjecture, (greater(end_time(X1),critical_point(X1))|~in_environment(sk3,X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_47, c_0_72])).
% 0.56/0.57 cnf(c_0_79, hypothesis, (greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3))|~environment(X1)|X2!=critical_point(X1)|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater(X3,X2)), inference(fof_simplification,[status(thm)],[d1_56])).
% 0.56/0.57 cnf(c_0_80, 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(fof_simplification,[status(thm)],[mp2_favour_members_34])).
% 0.56/0.57 cnf(c_0_81, plain, (subpopulation(first_movers,X1,X2)|~environment(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp_subpopulations_46])).
% 0.56/0.57 cnf(c_0_82, plain, (selection_favors(efficient_producers,first_movers,X1)|~observational_period(X1)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)|~selection_favors(efficient_producers,first_movers,end_time(sk1(X1)))), inference(fof_simplification,[status(thm)],[mp3_favoured_trategy_37])).
% 0.56/0.57 cnf(c_0_83, 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_73, c_0_50])).
% 0.56/0.57 cnf(c_0_84, 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_32, c_0_74])).
% 0.56/0.57 cnf(c_0_85, negated_conjecture, (start_time(sk1(sk3))=critical_point(sk1(sk3))|in_environment(sk1(sk3),end_time(sk1(sk3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75, c_0_76]), c_0_77])])).
% 0.56/0.57 cnf(c_0_86, negated_conjecture, (greater(end_time(sk1(sk3)),critical_point(sk1(sk3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_78, c_0_76]), c_0_77])])).
% 0.56/0.57 cnf(c_0_87, plain, (in_environment(X1,critical_point(X1))|~greater_or_equal(end_time(X1),critical_point(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_49, c_0_30])).
% 0.56/0.57 cnf(c_0_88, hypothesis, (greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3))|~environment(X1)|X2!=critical_point(X1)|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater(X3,X2)), c_0_79).
% 0.56/0.57 cnf(c_0_89, 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(fof_simplification,[status(thm)],[mp_contains_FM_and_EP_44])).
% 0.56/0.57 cnf(c_0_90, 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), c_0_80).
% 0.56/0.57 cnf(c_0_91, plain, (subpopulation(first_movers,X1,X2)|~environment(X1)|~in_environment(X1,X2)), c_0_81).
% 0.56/0.57 cnf(c_0_92, plain, (subpopulation(efficient_producers,X1,X2)|~environment(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp_subpopulations_47])).
% 0.56/0.57 cnf(c_0_93, plain, (selection_favors(efficient_producers,first_movers,X1)|~observational_period(X1)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)|~selection_favors(efficient_producers,first_movers,end_time(sk1(X1)))), c_0_82).
% 0.56/0.57 cnf(c_0_94, 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_83, c_0_84])).
% 0.56/0.57 cnf(c_0_95, negated_conjecture, (in_environment(sk1(sk3),end_time(sk1(sk3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_85]), c_0_86]), c_0_77])])).
% 0.56/0.57 cnf(c_0_96, plain, (in_environment(X1,critical_point(X1))|~greater(end_time(X1),critical_point(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_87, c_0_50])).
% 0.56/0.57 cnf(c_0_97, 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_88])).
% 0.56/0.57 cnf(c_0_98, 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)), c_0_89).
% 0.56/0.57 cnf(c_0_99, plain, (greater_or_equal(cardinality_at_time(first_movers,X2),zero)|~environment(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp_first_movers_exist_45])).
% 0.56/0.57 cnf(c_0_100, 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_90, c_0_91])).
% 0.56/0.57 cnf(c_0_101, plain, (subpopulation(efficient_producers,X1,X2)|~environment(X1)|~in_environment(X1,X2)), c_0_92).
% 0.56/0.57 cnf(c_0_102, plain, (selection_favors(efficient_producers,first_movers,X1)|~observational_period(X1)|~selection_favors(efficient_producers,first_movers,end_time(sk1(X1)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_93, c_0_60]), c_0_61])])).
% 0.56/0.57 cnf(c_0_103, negated_conjecture, (appear(efficient_producers,sk1(sk3))=critical_point(sk1(sk3))|greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_94, c_0_86]), c_0_95]), c_0_77])])).
% 0.56/0.57 cnf(c_0_104, negated_conjecture, (in_environment(sk1(sk3),critical_point(sk1(sk3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_96, c_0_86]), c_0_77])])).
% 0.56/0.57 cnf(c_0_105, 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_97, c_0_98])).
% 0.56/0.57 cnf(c_0_106, plain, (greater_or_equal(cardinality_at_time(first_movers,X2),zero)|~environment(X1)|~in_environment(X1,X2)), c_0_99).
% 0.56/0.57 cnf(c_0_107, 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_100, c_0_101])).
% 0.56/0.57 cnf(c_0_108, negated_conjecture, (~selection_favors(efficient_producers,first_movers,end_time(sk1(sk3)))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_102, c_0_38]), c_0_70])).
% 0.56/0.57 cnf(c_0_109, hypothesis, (greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)|greater(cardinality_at_time(efficient_producers,X1),zero)|~greater_or_equal(X1,critical_point(sk1(sk3)))|~in_environment(sk1(sk3),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73, c_0_103]), c_0_77])])).
% 0.56/0.57 cnf(c_0_110, negated_conjecture, (greater_or_equal(end_time(sk1(sk3)),critical_point(sk1(sk3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_104]), c_0_77])])).
% 0.56/0.57 cnf(c_0_111, hypothesis, (greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3))))|~in_environment(sk1(sk3),end_time(sk1(sk3)))|~greater(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)|~greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_105, c_0_86]), c_0_77])])).
% 0.56/0.57 cnf(c_0_112, negated_conjecture, (greater_or_equal(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_106, c_0_95]), c_0_77])])).
% 0.56/0.57 cnf(c_0_113, negated_conjecture, (cardinality_at_time(first_movers,end_time(sk1(sk3)))!=zero|~greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_107, c_0_95]), c_0_77])]), c_0_108])).
% 0.56/0.57 cnf(c_0_114, negated_conjecture, (greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_109, c_0_110]), c_0_95])])).
% 0.56/0.57 cnf(c_0_115, plain, (selection_favors(X3,X2,X4)|~environment(X1)|~subpopulations(X2,X3,X1,X4)|~greater(growth_rate(X3,X4),growth_rate(X2,X4))), inference(fof_simplification,[status(thm)],[mp1_high_growth_rates_33])).
% 0.56/0.57 cnf(c_0_116, hypothesis, (greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3))))|~greater(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)|~greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_111, c_0_95])])).
% 0.56/0.57 cnf(c_0_117, negated_conjecture, (cardinality_at_time(first_movers,end_time(sk1(sk3)))=zero|greater(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)), inference(spm,[status(thm)],[c_0_29, c_0_112])).
% 0.56/0.57 cnf(c_0_118, negated_conjecture, (cardinality_at_time(first_movers,end_time(sk1(sk3)))!=zero), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_113, c_0_114])])).
% 0.56/0.57 cnf(c_0_119, plain, (selection_favors(X3,X2,X4)|~environment(X1)|~subpopulations(X2,X3,X1,X4)|~greater(growth_rate(X3,X4),growth_rate(X2,X4))), c_0_115).
% 0.56/0.57 cnf(c_0_120, hypothesis, (greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3))))|~greater(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_116, c_0_114])])).
% 0.56/0.57 cnf(c_0_121, negated_conjecture, (greater(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)), inference(sr,[status(thm)],[c_0_117, c_0_118])).
% 0.56/0.57 cnf(c_0_122, 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_119, c_0_98])).
% 0.56/0.57 cnf(c_0_123, hypothesis, (greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_120, c_0_121])])).
% 0.56/0.57 cnf(c_0_124, 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_122, c_0_95]), c_0_77])]), c_0_108]), c_0_123]), c_0_121]), c_0_114])]), ['proof']).
% 0.56/0.57 % SZS output end Proof
% 0.56/0.57 % User time : 0.023 s
% 0.56/0.57 % System time : 0.003 s
% 0.56/0.57 % Total time : 0.026 s
% 0.56/0.57 % User time : 0.026 s
% 0.56/0.57 % System time : 0.005 s
% 0.56/0.57 % Total time : 0.031 s
% 0.56/0.57
%------------------------------------------------------------------------------