%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT023-2 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:04:29 AM UTC 2026
% Result : Unsatisfiable 0.25s 0.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT023-2 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.07/0.34 % Computer : n004.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 7 12:07:30 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.13/0.46 start to proof:theBenchmark.p
% 0.25/0.52 % Version : CSI_E---1.1
% 0.25/0.52 % Problem : theBenchmark.p
% 0.25/0.52 % Proof found!
% 0.25/0.52 # SZS status Unsatisfiable
% 0.25/0.52 % SZS output start Proof
% 0.25/0.52 cnf(l1_31, hypothesis, (in_environment(X1,sk4(X1))|~environment(X1)|~stable(X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l1_31)).
% 0.25/0.52 cnf(mp_earliest_time_growth_rate_exceeds_20, axiom, (greater_or_equal(sk1(X2,X1),X2)|in_environment(X1,sk2(X1))|~environment(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds_20)).
% 0.25/0.52 cnf(prove_l5_34, negated_conjecture, (stable(sk5)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_l5_34)).
% 0.25/0.52 cnf(prove_l5_33, negated_conjecture, (environment(sk5)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_l5_33)).
% 0.25/0.52 cnf(mp_earliest_time_growth_rate_exceeds_19, axiom, (subpopulations(first_movers,efficient_producers,X1,sk1(X2,X1))|in_environment(X1,sk2(X1))|~environment(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds_19)).
% 0.25/0.52 cnf(d1_29, hypothesis, (greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|greater(sk3(X2,X1),X2)|X2=critical_point(X1)|~environment(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_29)).
% 0.25/0.52 cnf(l1_32, hypothesis, (greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|~environment(X1)|~stable(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)|~greater_or_equal(X2,sk4(X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l1_32)).
% 0.25/0.52 cnf(mp_earliest_time_growth_rate_exceeds_25, axiom, (in_environment(X1,sk2(X1))|~environment(X1)|~in_environment(X1,X2)|~greater(growth_rate(efficient_producers,sk1(X2,X1)),growth_rate(first_movers,sk1(X2,X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds_25)).
% 0.25/0.52 cnf(mp_earliest_time_growth_rate_exceeds_23, axiom, (greater_or_equal(sk1(X2,X1),X2)|~environment(X1)|~in_environment(X1,X2)|~greater(growth_rate(efficient_producers,sk2(X1)),growth_rate(first_movers,sk2(X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds_23)).
% 0.25/0.52 cnf(mp_earliest_time_growth_rate_exceeds_21, axiom, (subpopulations(first_movers,efficient_producers,X1,sk1(X2,X1))|~environment(X1)|~in_environment(X1,X2)|~greater(growth_rate(efficient_producers,sk2(X1)),growth_rate(first_movers,sk2(X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds_21)).
% 0.25/0.52 cnf(mp_earliest_time_growth_rate_exceeds_26, axiom, (~environment(X1)|~in_environment(X1,X2)|~greater(growth_rate(efficient_producers,sk1(X2,X1)),growth_rate(first_movers,sk1(X2,X1)))|~greater(growth_rate(efficient_producers,sk2(X1)),growth_rate(first_movers,sk2(X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds_26)).
% 0.25/0.52 cnf(mp_earliest_time_growth_rate_exceeds_24, axiom, (greater_or_equal(sk1(X2,X1),X2)|greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3))|~environment(X1)|~in_environment(X1,X2)|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater(X3,sk2(X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds_24)).
% 0.25/0.52 cnf(mp_earliest_time_growth_rate_exceeds_22, axiom, (subpopulations(first_movers,efficient_producers,X1,sk1(X2,X1))|greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3))|~environment(X1)|~in_environment(X1,X2)|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater(X3,sk2(X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds_22)).
% 0.25/0.52 cnf(mp_earliest_time_growth_rate_exceeds_27, axiom, (greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3))|~environment(X1)|~in_environment(X1,X2)|~greater(growth_rate(efficient_producers,sk1(X2,X1)),growth_rate(first_movers,sk1(X2,X1)))|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater(X3,sk2(X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds_27)).
% 0.25/0.52 cnf(d1_28, hypothesis, (greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|subpopulations(first_movers,efficient_producers,X1,sk3(X2,X1))|X2=critical_point(X1)|~environment(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_28)).
% 0.25/0.52 cnf(d1_30, hypothesis, (greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|X2=critical_point(X1)|~environment(X1)|~in_environment(X1,X2)|~greater(growth_rate(efficient_producers,sk3(X2,X1)),growth_rate(first_movers,sk3(X2,X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_30)).
% 0.25/0.52 cnf(prove_l5_35, negated_conjecture, (~in_environment(sk5,critical_point(sk5))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_l5_35)).
% 0.25/0.52 cnf(c_0_17, hypothesis, (in_environment(X1,sk4(X1))|~environment(X1)|~stable(X1)), inference(fof_simplification,[status(thm)],[l1_31])).
% 0.25/0.52 cnf(c_0_18, plain, (greater_or_equal(sk1(X2,X1),X2)|in_environment(X1,sk2(X1))|~environment(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp_earliest_time_growth_rate_exceeds_20])).
% 0.25/0.52 cnf(c_0_19, hypothesis, (in_environment(X1,sk4(X1))|~environment(X1)|~stable(X1)), c_0_17).
% 0.25/0.52 cnf(c_0_20, negated_conjecture, (stable(sk5)), prove_l5_34).
% 0.25/0.52 cnf(c_0_21, negated_conjecture, (environment(sk5)), prove_l5_33).
% 0.25/0.52 cnf(c_0_22, plain, (subpopulations(first_movers,efficient_producers,X1,sk1(X2,X1))|in_environment(X1,sk2(X1))|~environment(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp_earliest_time_growth_rate_exceeds_19])).
% 0.25/0.52 cnf(c_0_23, hypothesis, (greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|greater(sk3(X2,X1),X2)|X2=critical_point(X1)|~environment(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[d1_29])).
% 0.25/0.52 cnf(c_0_24, plain, (greater_or_equal(sk1(X2,X1),X2)|in_environment(X1,sk2(X1))|~environment(X1)|~in_environment(X1,X2)), c_0_18).
% 0.25/0.52 cnf(c_0_25, negated_conjecture, (in_environment(sk5,sk4(sk5))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_19, c_0_20]), c_0_21])])).
% 0.25/0.52 cnf(c_0_26, plain, (subpopulations(first_movers,efficient_producers,X1,sk1(X2,X1))|in_environment(X1,sk2(X1))|~environment(X1)|~in_environment(X1,X2)), c_0_22).
% 0.25/0.52 cnf(c_0_27, hypothesis, (greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|~environment(X1)|~stable(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)|~greater_or_equal(X2,sk4(X1))), inference(fof_simplification,[status(thm)],[l1_32])).
% 0.25/0.52 cnf(c_0_28, hypothesis, (greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|greater(sk3(X2,X1),X2)|X2=critical_point(X1)|~environment(X1)|~in_environment(X1,X2)), c_0_23).
% 0.25/0.52 cnf(c_0_29, negated_conjecture, (greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))|in_environment(sk5,sk2(sk5))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_24, c_0_25]), c_0_21])])).
% 0.25/0.52 cnf(c_0_30, negated_conjecture, (subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))|in_environment(sk5,sk2(sk5))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_26, c_0_25]), c_0_21])])).
% 0.25/0.52 cnf(c_0_31, plain, (in_environment(X1,sk2(X1))|~environment(X1)|~in_environment(X1,X2)|~greater(growth_rate(efficient_producers,sk1(X2,X1)),growth_rate(first_movers,sk1(X2,X1)))), inference(fof_simplification,[status(thm)],[mp_earliest_time_growth_rate_exceeds_25])).
% 0.25/0.52 cnf(c_0_32, hypothesis, (greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|~environment(X1)|~stable(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)|~greater_or_equal(X2,sk4(X1))), c_0_27).
% 0.25/0.52 cnf(c_0_33, negated_conjecture, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))|greater(sk3(sk2(sk5),sk5),sk2(sk5))|greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_29]), c_0_21])])).
% 0.25/0.52 cnf(c_0_34, negated_conjecture, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))|greater(sk3(sk2(sk5),sk5),sk2(sk5))|subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_30]), c_0_21])])).
% 0.25/0.52 cnf(c_0_35, plain, (in_environment(X1,sk2(X1))|~environment(X1)|~in_environment(X1,X2)|~greater(growth_rate(efficient_producers,sk1(X2,X1)),growth_rate(first_movers,sk1(X2,X1)))), c_0_31).
% 0.25/0.52 cnf(c_0_36, hypothesis, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5)))|greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))|greater(sk3(sk2(sk5),sk5),sk2(sk5))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_33]), c_0_20]), c_0_21])]), c_0_34])).
% 0.25/0.52 cnf(c_0_37, plain, (greater_or_equal(sk1(X2,X1),X2)|~environment(X1)|~in_environment(X1,X2)|~greater(growth_rate(efficient_producers,sk2(X1)),growth_rate(first_movers,sk2(X1)))), inference(fof_simplification,[status(thm)],[mp_earliest_time_growth_rate_exceeds_23])).
% 0.25/0.52 cnf(c_0_38, hypothesis, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))|greater(sk3(sk2(sk5),sk5),sk2(sk5))|in_environment(sk5,sk2(sk5))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_36]), c_0_25]), c_0_21])])).
% 0.25/0.52 cnf(c_0_39, plain, (subpopulations(first_movers,efficient_producers,X1,sk1(X2,X1))|~environment(X1)|~in_environment(X1,X2)|~greater(growth_rate(efficient_producers,sk2(X1)),growth_rate(first_movers,sk2(X1)))), inference(fof_simplification,[status(thm)],[mp_earliest_time_growth_rate_exceeds_21])).
% 0.25/0.52 cnf(c_0_40, plain, (~environment(X1)|~in_environment(X1,X2)|~greater(growth_rate(efficient_producers,sk1(X2,X1)),growth_rate(first_movers,sk1(X2,X1)))|~greater(growth_rate(efficient_producers,sk2(X1)),growth_rate(first_movers,sk2(X1)))), inference(fof_simplification,[status(thm)],[mp_earliest_time_growth_rate_exceeds_26])).
% 0.25/0.52 cnf(c_0_41, plain, (greater_or_equal(sk1(X2,X1),X2)|~environment(X1)|~in_environment(X1,X2)|~greater(growth_rate(efficient_producers,sk2(X1)),growth_rate(first_movers,sk2(X1)))), c_0_37).
% 0.25/0.52 cnf(c_0_42, hypothesis, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))|greater(sk3(sk2(sk5),sk5),sk2(sk5))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_38]), c_0_21])])).
% 0.25/0.52 cnf(c_0_43, plain, (subpopulations(first_movers,efficient_producers,X1,sk1(X2,X1))|~environment(X1)|~in_environment(X1,X2)|~greater(growth_rate(efficient_producers,sk2(X1)),growth_rate(first_movers,sk2(X1)))), c_0_39).
% 0.25/0.52 cnf(c_0_44, plain, (~environment(X1)|~in_environment(X1,X2)|~greater(growth_rate(efficient_producers,sk1(X2,X1)),growth_rate(first_movers,sk1(X2,X1)))|~greater(growth_rate(efficient_producers,sk2(X1)),growth_rate(first_movers,sk2(X1)))), c_0_40).
% 0.25/0.52 cnf(c_0_45, hypothesis, (sk2(sk5)=critical_point(sk5)|greater(sk3(sk2(sk5),sk5),sk2(sk5))|greater_or_equal(sk1(X1,sk5),X1)|~in_environment(sk5,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_42]), c_0_21])])).
% 0.25/0.52 cnf(c_0_46, hypothesis, (sk2(sk5)=critical_point(sk5)|greater(sk3(sk2(sk5),sk5),sk2(sk5))|subpopulations(first_movers,efficient_producers,sk5,sk1(X1,sk5))|~in_environment(sk5,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_42]), c_0_21])])).
% 0.25/0.52 cnf(c_0_47, hypothesis, (sk2(sk5)=critical_point(sk5)|greater(sk3(sk2(sk5),sk5),sk2(sk5))|~greater(growth_rate(efficient_producers,sk1(X1,sk5)),growth_rate(first_movers,sk1(X1,sk5)))|~in_environment(sk5,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_42]), c_0_21])])).
% 0.25/0.52 cnf(c_0_48, plain, (greater_or_equal(sk1(X2,X1),X2)|greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3))|~environment(X1)|~in_environment(X1,X2)|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater(X3,sk2(X1))), inference(fof_simplification,[status(thm)],[mp_earliest_time_growth_rate_exceeds_24])).
% 0.25/0.52 cnf(c_0_49, negated_conjecture, (sk2(sk5)=critical_point(sk5)|greater(sk3(sk2(sk5),sk5),sk2(sk5))|greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))), inference(spm,[status(thm)],[c_0_45, c_0_25])).
% 0.25/0.52 cnf(c_0_50, negated_conjecture, (sk2(sk5)=critical_point(sk5)|greater(sk3(sk2(sk5),sk5),sk2(sk5))|subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))), inference(spm,[status(thm)],[c_0_46, c_0_25])).
% 0.25/0.52 cnf(c_0_51, negated_conjecture, (sk2(sk5)=critical_point(sk5)|greater(sk3(sk2(sk5),sk5),sk2(sk5))|~greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5)))), inference(spm,[status(thm)],[c_0_47, c_0_25])).
% 0.25/0.52 cnf(c_0_52, plain, (subpopulations(first_movers,efficient_producers,X1,sk1(X2,X1))|greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3))|~environment(X1)|~in_environment(X1,X2)|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater(X3,sk2(X1))), inference(fof_simplification,[status(thm)],[mp_earliest_time_growth_rate_exceeds_22])).
% 0.25/0.52 cnf(c_0_53, plain, (greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3))|~environment(X1)|~in_environment(X1,X2)|~greater(growth_rate(efficient_producers,sk1(X2,X1)),growth_rate(first_movers,sk1(X2,X1)))|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater(X3,sk2(X1))), inference(fof_simplification,[status(thm)],[mp_earliest_time_growth_rate_exceeds_27])).
% 0.25/0.52 cnf(c_0_54, plain, (greater_or_equal(sk1(X2,X1),X2)|greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3))|~environment(X1)|~in_environment(X1,X2)|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater(X3,sk2(X1))), c_0_48).
% 0.25/0.52 cnf(c_0_55, hypothesis, (sk2(sk5)=critical_point(sk5)|greater(sk3(sk2(sk5),sk5),sk2(sk5))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_49]), c_0_20]), c_0_21])]), c_0_50]), c_0_51])).
% 0.25/0.52 cnf(c_0_56, plain, (subpopulations(first_movers,efficient_producers,X1,sk1(X2,X1))|greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3))|~environment(X1)|~in_environment(X1,X2)|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater(X3,sk2(X1))), c_0_52).
% 0.25/0.52 cnf(c_0_57, plain, (greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3))|~environment(X1)|~in_environment(X1,X2)|~greater(growth_rate(efficient_producers,sk1(X2,X1)),growth_rate(first_movers,sk1(X2,X1)))|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater(X3,sk2(X1))), c_0_53).
% 0.25/0.52 cnf(c_0_58, hypothesis, (greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|subpopulations(first_movers,efficient_producers,X1,sk3(X2,X1))|X2=critical_point(X1)|~environment(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[d1_28])).
% 0.25/0.52 cnf(c_0_59, hypothesis, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5)))|greater_or_equal(sk1(X1,sk5),X1)|~subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))|~in_environment(sk5,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54, c_0_55]), c_0_21])])).
% 0.25/0.52 cnf(c_0_60, hypothesis, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5)))|subpopulations(first_movers,efficient_producers,sk5,sk1(X1,sk5))|~subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))|~in_environment(sk5,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_55]), c_0_21])])).
% 0.25/0.52 cnf(c_0_61, hypothesis, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5)))|~greater(growth_rate(efficient_producers,sk1(X1,sk5)),growth_rate(first_movers,sk1(X1,sk5)))|~subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))|~in_environment(sk5,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57, c_0_55]), c_0_21])])).
% 0.25/0.52 cnf(c_0_62, hypothesis, (greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|subpopulations(first_movers,efficient_producers,X1,sk3(X2,X1))|X2=critical_point(X1)|~environment(X1)|~in_environment(X1,X2)), c_0_58).
% 0.25/0.52 cnf(c_0_63, negated_conjecture, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5)))|greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))|~subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))), inference(spm,[status(thm)],[c_0_59, c_0_25])).
% 0.25/0.52 cnf(c_0_64, negated_conjecture, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5)))|subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))|~subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))), inference(spm,[status(thm)],[c_0_60, c_0_25])).
% 0.25/0.52 cnf(c_0_65, negated_conjecture, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5)))|~greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5)))|~subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))), inference(spm,[status(thm)],[c_0_61, c_0_25])).
% 0.25/0.52 cnf(c_0_66, negated_conjecture, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))|greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))|subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_29]), c_0_21])])).
% 0.25/0.52 cnf(c_0_67, negated_conjecture, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))|subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))|subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_30]), c_0_21])])).
% 0.25/0.52 cnf(c_0_68, hypothesis, (greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|X2=critical_point(X1)|~environment(X1)|~in_environment(X1,X2)|~greater(growth_rate(efficient_producers,sk3(X2,X1)),growth_rate(first_movers,sk3(X2,X1)))), inference(fof_simplification,[status(thm)],[d1_30])).
% 0.25/0.52 cnf(c_0_69, hypothesis, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5)))|~subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_63]), c_0_20]), c_0_21])]), c_0_64]), c_0_65])).
% 0.25/0.52 cnf(c_0_70, hypothesis, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5)))|greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))|subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_66]), c_0_20]), c_0_21])]), c_0_67])).
% 0.25/0.52 cnf(c_0_71, hypothesis, (greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))|X2=critical_point(X1)|~environment(X1)|~in_environment(X1,X2)|~greater(growth_rate(efficient_producers,sk3(X2,X1)),growth_rate(first_movers,sk3(X2,X1)))), c_0_68).
% 0.25/0.52 cnf(c_0_72, hypothesis, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5)))|greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5)))|greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))), inference(spm,[status(thm)],[c_0_69, c_0_70])).
% 0.25/0.52 cnf(c_0_73, hypothesis, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5)))|greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))|~in_environment(sk5,sk2(sk5))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_71, c_0_72]), c_0_21])])).
% 0.25/0.52 cnf(c_0_74, negated_conjecture, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5)))|greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))|greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))), inference(spm,[status(thm)],[c_0_73, c_0_29])).
% 0.25/0.52 cnf(c_0_75, hypothesis, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5)))|greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))|~subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_74]), c_0_20]), c_0_21])])).
% 0.25/0.52 cnf(c_0_76, negated_conjecture, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5)))|greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_73, c_0_30]), c_0_75])).
% 0.25/0.52 cnf(c_0_77, negated_conjecture, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))|in_environment(sk5,sk2(sk5))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_76]), c_0_25]), c_0_21])])).
% 0.25/0.52 cnf(c_0_78, hypothesis, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))|subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_77]), c_0_21])])).
% 0.25/0.52 cnf(c_0_79, hypothesis, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk3(sk2(sk5),sk5)),growth_rate(first_movers,sk3(sk2(sk5),sk5)))|greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))), inference(spm,[status(thm)],[c_0_69, c_0_78])).
% 0.25/0.52 cnf(c_0_80, hypothesis, (sk2(sk5)=critical_point(sk5)|greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_71, c_0_79]), c_0_21])]), c_0_77])).
% 0.25/0.52 cnf(c_0_81, hypothesis, (sk2(sk5)=critical_point(sk5)|greater_or_equal(sk1(X1,sk5),X1)|~in_environment(sk5,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_80]), c_0_21])])).
% 0.25/0.52 cnf(c_0_82, hypothesis, (sk2(sk5)=critical_point(sk5)|subpopulations(first_movers,efficient_producers,sk5,sk1(X1,sk5))|~in_environment(sk5,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_80]), c_0_21])])).
% 0.25/0.52 cnf(c_0_83, hypothesis, (sk2(sk5)=critical_point(sk5)|~greater(growth_rate(efficient_producers,sk1(X1,sk5)),growth_rate(first_movers,sk1(X1,sk5)))|~in_environment(sk5,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_80]), c_0_21])])).
% 0.25/0.52 cnf(c_0_84, negated_conjecture, (sk2(sk5)=critical_point(sk5)|greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))), inference(spm,[status(thm)],[c_0_81, c_0_25])).
% 0.25/0.52 cnf(c_0_85, negated_conjecture, (sk2(sk5)=critical_point(sk5)|subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))), inference(spm,[status(thm)],[c_0_82, c_0_25])).
% 0.25/0.52 cnf(c_0_86, negated_conjecture, (sk2(sk5)=critical_point(sk5)|~greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5)))), inference(spm,[status(thm)],[c_0_83, c_0_25])).
% 0.25/0.52 cnf(c_0_87, negated_conjecture, (~in_environment(sk5,critical_point(sk5))), inference(fof_simplification,[status(thm)],[prove_l5_35])).
% 0.25/0.52 cnf(c_0_88, hypothesis, (sk2(sk5)=critical_point(sk5)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_84]), c_0_20]), c_0_21])]), c_0_85]), c_0_86])).
% 0.25/0.52 cnf(c_0_89, negated_conjecture, (~in_environment(sk5,critical_point(sk5))), c_0_87).
% 0.25/0.52 cnf(c_0_90, negated_conjecture, (greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_88]), c_0_89])).
% 0.25/0.52 cnf(c_0_91, negated_conjecture, (subpopulations(first_movers,efficient_producers,sk5,sk1(sk4(sk5),sk5))), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_88]), c_0_89])).
% 0.25/0.52 cnf(c_0_92, hypothesis, (greater(growth_rate(efficient_producers,sk1(sk4(sk5),sk5)),growth_rate(first_movers,sk1(sk4(sk5),sk5)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_90]), c_0_20]), c_0_21])]), c_0_91])])).
% 0.25/0.52 cnf(c_0_93, hypothesis, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_92]), c_0_88]), c_0_25]), c_0_21])]), c_0_89]), ['proof']).
% 0.25/0.52 % SZS output end Proof
% 0.25/0.52 % User time : 0.006 s
% 0.25/0.52 % System time : 0.003 s
% 0.25/0.52 % Total time : 0.009 s
% 0.25/0.52 % User time : 0.008 s
% 0.25/0.52 % System time : 0.006 s
% 0.25/0.52 % Total time : 0.014 s
% 0.25/0.52
%------------------------------------------------------------------------------