%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT030-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n028.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 : Unsatisfiable 0.27s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT030-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.32 % Computer : n028.cluster.edu
% 0.08/0.32 % Model : x86_64 x86_64
% 0.08/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.32 % Memory : 8046.5625MB
% 0.08/0.32 % OS : Linux 6.8.0-71-generic
% 0.08/0.32 % CPULimit : 300
% 0.08/0.32 % WCLimit : 300
% 0.08/0.32 % DateTime : Mon Sep 7 12:21:46 UTC 2026
% 0.08/0.33 % CPUTime :
% 0.12/0.45 start to proof:theBenchmark.p
% 0.27/0.53 % Version : CSI_E---1.1
% 0.27/0.53 % Problem : theBenchmark.p
% 0.27/0.53 % Proof found!
% 0.27/0.53 # SZS status Unsatisfiable
% 0.27/0.53 % SZS output start Proof
% 0.27/0.53 cnf(l1_10, hypothesis, (in_environment(X1,sk3(X1))|~environment(X1)|~stable(X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', l1_10)).
% 0.27/0.53 cnf(mp_earliest_time_growth_rate_exceeds_1, axiom, (subpopulations(first_movers,efficient_producers,X1,sk1(X2,X1))|in_environment(X1,sk2(X1))|~environment(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds_1)).
% 0.27/0.53 cnf(prove_l12_13, negated_conjecture, (stable(sk4)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l12_13)).
% 0.27/0.53 cnf(prove_l12_12, negated_conjecture, (environment(sk4)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l12_12)).
% 0.27/0.53 cnf(mp_earliest_time_growth_rate_exceeds_2, axiom, (greater_or_equal(sk1(X2,X1),X2)|in_environment(X1,sk2(X1))|~environment(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds_2)).
% 0.27/0.53 cnf(l1_11, 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,sk3(X1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', l1_11)).
% 0.27/0.53 cnf(prove_l12_15, negated_conjecture, (greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))|greater(sk5(X1),X1)|~in_environment(sk4,X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l12_15)).
% 0.27/0.53 cnf(prove_l12_14, negated_conjecture, (greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))|subpopulations(first_movers,efficient_producers,sk4,sk5(X1))|~in_environment(sk4,X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l12_14)).
% 0.27/0.53 cnf(mp_earliest_time_growth_rate_exceeds_7, 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/sandbox/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds_7)).
% 0.27/0.53 cnf(mp_earliest_time_growth_rate_exceeds_4, 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/sandbox/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds_4)).
% 0.27/0.53 cnf(mp_earliest_time_growth_rate_exceeds_6, 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/sandbox/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds_6)).
% 0.27/0.53 cnf(mp_earliest_time_growth_rate_exceeds_9, 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/sandbox/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds_9)).
% 0.27/0.53 cnf(prove_l12_16, negated_conjecture, (greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))|~in_environment(sk4,X1)|~greater(growth_rate(efficient_producers,sk5(X1)),growth_rate(first_movers,sk5(X1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l12_16)).
% 0.27/0.53 cnf(mp_earliest_time_growth_rate_exceeds_3, 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/sandbox/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds_3)).
% 0.27/0.53 cnf(mp_earliest_time_growth_rate_exceeds_5, 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/sandbox/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds_5)).
% 0.27/0.53 cnf(mp_earliest_time_growth_rate_exceeds_8, 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/sandbox/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds_8)).
% 0.27/0.53 cnf(c_0_16, hypothesis, (in_environment(X1,sk3(X1))|~environment(X1)|~stable(X1)), inference(fof_simplification,[status(thm)],[l1_10])).
% 0.27/0.53 cnf(c_0_17, 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_1])).
% 0.27/0.53 cnf(c_0_18, hypothesis, (in_environment(X1,sk3(X1))|~environment(X1)|~stable(X1)), c_0_16).
% 0.27/0.53 cnf(c_0_19, negated_conjecture, (stable(sk4)), prove_l12_13).
% 0.27/0.53 cnf(c_0_20, negated_conjecture, (environment(sk4)), prove_l12_12).
% 0.27/0.53 cnf(c_0_21, 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_2])).
% 0.27/0.53 cnf(c_0_22, 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,sk3(X1))), inference(fof_simplification,[status(thm)],[l1_11])).
% 0.27/0.53 cnf(c_0_23, plain, (subpopulations(first_movers,efficient_producers,X1,sk1(X2,X1))|in_environment(X1,sk2(X1))|~environment(X1)|~in_environment(X1,X2)), c_0_17).
% 0.27/0.53 cnf(c_0_24, negated_conjecture, (in_environment(sk4,sk3(sk4))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_18, c_0_19]), c_0_20])])).
% 0.27/0.53 cnf(c_0_25, plain, (greater_or_equal(sk1(X2,X1),X2)|in_environment(X1,sk2(X1))|~environment(X1)|~in_environment(X1,X2)), c_0_21).
% 0.27/0.53 cnf(c_0_26, negated_conjecture, (greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))|greater(sk5(X1),X1)|~in_environment(sk4,X1)), inference(fof_simplification,[status(thm)],[prove_l12_15])).
% 0.27/0.53 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,sk3(X1))), c_0_22).
% 0.27/0.53 cnf(c_0_28, negated_conjecture, (subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))|in_environment(sk4,sk2(sk4))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_24]), c_0_20])])).
% 0.27/0.53 cnf(c_0_29, negated_conjecture, (greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))|in_environment(sk4,sk2(sk4))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_25, c_0_24]), c_0_20])])).
% 0.27/0.53 cnf(c_0_30, negated_conjecture, (greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))|subpopulations(first_movers,efficient_producers,sk4,sk5(X1))|~in_environment(sk4,X1)), inference(fof_simplification,[status(thm)],[prove_l12_14])).
% 0.27/0.53 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_7])).
% 0.27/0.53 cnf(c_0_32, negated_conjecture, (greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))|greater(sk5(X1),X1)|~in_environment(sk4,X1)), c_0_26).
% 0.27/0.53 cnf(c_0_33, hypothesis, (greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))|in_environment(sk4,sk2(sk4))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_28]), c_0_19]), c_0_20])]), c_0_29])).
% 0.27/0.53 cnf(c_0_34, 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_4])).
% 0.27/0.53 cnf(c_0_35, negated_conjecture, (greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))|subpopulations(first_movers,efficient_producers,sk4,sk5(X1))|~in_environment(sk4,X1)), c_0_30).
% 0.27/0.53 cnf(c_0_36, 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.27/0.53 cnf(c_0_37, negated_conjecture, (greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))|greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))|greater(sk5(sk2(sk4)),sk2(sk4))), inference(spm,[status(thm)],[c_0_32, c_0_33])).
% 0.27/0.53 cnf(c_0_38, 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_6])).
% 0.27/0.53 cnf(c_0_39, 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_34).
% 0.27/0.53 cnf(c_0_40, negated_conjecture, (greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))|greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))|subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))), inference(spm,[status(thm)],[c_0_35, c_0_33])).
% 0.27/0.53 cnf(c_0_41, negated_conjecture, (greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))|greater(sk5(sk2(sk4)),sk2(sk4))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36, c_0_37]), c_0_24]), c_0_20])]), c_0_32])).
% 0.27/0.53 cnf(c_0_42, 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_38).
% 0.27/0.53 cnf(c_0_43, negated_conjecture, (greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))|greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4))))|greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))|subpopulations(first_movers,efficient_producers,sk4,sk1(X1,sk4))|~in_environment(sk4,X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_40]), c_0_20])]), c_0_41])).
% 0.27/0.53 cnf(c_0_44, negated_conjecture, (greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))|greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4))))|greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))|greater_or_equal(sk1(X1,sk4),X1)|~in_environment(sk4,X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_40]), c_0_20])]), c_0_41])).
% 0.27/0.53 cnf(c_0_45, negated_conjecture, (greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))|greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4))))|greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))|subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))), inference(spm,[status(thm)],[c_0_43, c_0_24])).
% 0.27/0.53 cnf(c_0_46, negated_conjecture, (greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))|greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4))))|greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))|greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))), inference(spm,[status(thm)],[c_0_44, c_0_24])).
% 0.27/0.53 cnf(c_0_47, hypothesis, (greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))|greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4))))|greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_45]), c_0_19]), c_0_20])]), c_0_46])).
% 0.27/0.53 cnf(c_0_48, 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_9])).
% 0.27/0.53 cnf(c_0_49, hypothesis, (greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4))))|greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))|in_environment(sk4,sk2(sk4))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36, c_0_47]), c_0_24]), c_0_20])])).
% 0.27/0.53 cnf(c_0_50, 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_48).
% 0.27/0.53 cnf(c_0_51, negated_conjecture, (greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4))))|greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))|subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))), inference(spm,[status(thm)],[c_0_35, c_0_49])).
% 0.27/0.53 cnf(c_0_52, negated_conjecture, (greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))|~in_environment(sk4,X1)|~greater(growth_rate(efficient_producers,sk5(X1)),growth_rate(first_movers,sk5(X1)))), inference(fof_simplification,[status(thm)],[prove_l12_16])).
% 0.27/0.53 cnf(c_0_53, negated_conjecture, (greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4))))|greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))|~greater(growth_rate(efficient_producers,sk1(X1,sk4)),growth_rate(first_movers,sk1(X1,sk4)))|~in_environment(sk4,X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_51]), c_0_20])]), c_0_41])).
% 0.27/0.53 cnf(c_0_54, negated_conjecture, (greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))|~in_environment(sk4,X1)|~greater(growth_rate(efficient_producers,sk5(X1)),growth_rate(first_movers,sk5(X1)))), c_0_52).
% 0.27/0.53 cnf(c_0_55, hypothesis, (greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4))))|greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53, c_0_47]), c_0_24])])).
% 0.27/0.53 cnf(c_0_56, negated_conjecture, (greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))|~in_environment(sk4,sk2(sk4))), inference(spm,[status(thm)],[c_0_54, c_0_55])).
% 0.27/0.53 cnf(c_0_57, 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_3])).
% 0.27/0.53 cnf(c_0_58, hypothesis, (greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))|greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))), inference(spm,[status(thm)],[c_0_56, c_0_33])).
% 0.27/0.53 cnf(c_0_59, 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_5])).
% 0.27/0.53 cnf(c_0_60, 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_57).
% 0.27/0.53 cnf(c_0_61, hypothesis, (greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36, c_0_58]), c_0_24]), c_0_20])]), c_0_56])).
% 0.27/0.53 cnf(c_0_62, 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_59).
% 0.27/0.53 cnf(c_0_63, 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_8])).
% 0.27/0.53 cnf(c_0_64, hypothesis, (subpopulations(first_movers,efficient_producers,sk4,sk1(X1,sk4))|~in_environment(sk4,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_61]), c_0_20])])).
% 0.27/0.53 cnf(c_0_65, hypothesis, (greater_or_equal(sk1(X1,sk4),X1)|~in_environment(sk4,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_61]), c_0_20])])).
% 0.27/0.53 cnf(c_0_66, 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_63).
% 0.27/0.53 cnf(c_0_67, negated_conjecture, (subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))), inference(spm,[status(thm)],[c_0_64, c_0_24])).
% 0.27/0.53 cnf(c_0_68, negated_conjecture, (greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))), inference(spm,[status(thm)],[c_0_65, c_0_24])).
% 0.27/0.53 cnf(c_0_69, hypothesis, (~greater(growth_rate(efficient_producers,sk1(X1,sk4)),growth_rate(first_movers,sk1(X1,sk4)))|~in_environment(sk4,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66, c_0_61]), c_0_20])])).
% 0.27/0.53 cnf(c_0_70, hypothesis, (greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))), 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_27, c_0_67]), c_0_19]), c_0_20])]), c_0_68])])).
% 0.27/0.53 cnf(c_0_71, hypothesis, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69, c_0_70]), c_0_24])]), ['proof']).
% 0.27/0.53 % SZS output end Proof
% 0.27/0.53 % User time : 0.009 s
% 0.27/0.53 % System time : 0.004 s
% 0.27/0.53 % Total time : 0.013 s
% 0.27/0.53 % User time : 0.011 s
% 0.27/0.53 % System time : 0.008 s
% 0.27/0.53 % Total time : 0.019 s
% 0.27/0.53
%------------------------------------------------------------------------------