%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT028-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n013.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:30 AM UTC 2026
% Result : Unsatisfiable 0.22s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT028-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.35 % Computer : n013.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 7 12:15:05 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.22/0.48 start to proof:theBenchmark.p
% 0.22/0.55 % Version : CSI_E---1.1
% 0.22/0.55 % Problem : theBenchmark.p
% 0.22/0.55 % Proof found!
% 0.22/0.55 # SZS status Unsatisfiable
% 0.22/0.55 % SZS output start Proof
% 0.22/0.55 cnf(mp_first_movers_negative_growth_1, axiom, (subpopulations(first_movers,efficient_producers,X1,sk1(X2,X1))|greater(sk2(X1),appear(efficient_producers,X1))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_first_movers_negative_growth_1)).
% 0.22/0.55 cnf(l11_7, hypothesis, (in_environment(X1,sk3(X1))|~environment(X1)|~stable(X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', l11_7)).
% 0.22/0.55 cnf(mp_first_movers_negative_growth_2, axiom, (greater_or_equal(sk1(X2,X1),X2)|greater(sk2(X1),appear(efficient_producers,X1))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_first_movers_negative_growth_2)).
% 0.22/0.55 cnf(l11_9, hypothesis, (greater(zero,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', l11_9)).
% 0.22/0.55 cnf(mp_first_movers_negative_growth_5, axiom, (greater(sk2(X1),appear(efficient_producers,X1))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~greater(zero,growth_rate(first_movers,sk1(X2,X1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_first_movers_negative_growth_5)).
% 0.22/0.55 cnf(prove_l10_11, negated_conjecture, (stable(sk4)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l10_11)).
% 0.22/0.55 cnf(prove_l10_10, negated_conjecture, (environment(sk4)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l10_10)).
% 0.22/0.55 cnf(prove_l10_12, negated_conjecture, (subpopulations(first_movers,efficient_producers,sk4,sk5(X1))|~greater(X1,appear(efficient_producers,sk4))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l10_12)).
% 0.22/0.55 cnf(prove_l10_14, negated_conjecture, (~greater(X1,appear(efficient_producers,sk4))|~greater(zero,growth_rate(first_movers,sk5(X1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l10_14)).
% 0.22/0.55 cnf(prove_l10_13, negated_conjecture, (greater_or_equal(sk5(X1),X1)|~greater(X1,appear(efficient_producers,sk4))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l10_13)).
% 0.22/0.55 cnf(mp_first_movers_negative_growth_3, axiom, (subpopulations(first_movers,efficient_producers,X1,sk1(X2,X1))|greater(zero,growth_rate(first_movers,X3))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater_or_equal(X3,sk2(X1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_first_movers_negative_growth_3)).
% 0.22/0.55 cnf(mp_first_movers_negative_growth_4, axiom, (greater_or_equal(sk1(X2,X1),X2)|greater(zero,growth_rate(first_movers,X3))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater_or_equal(X3,sk2(X1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_first_movers_negative_growth_4)).
% 0.22/0.55 cnf(mp_first_movers_negative_growth_6, axiom, (greater(zero,growth_rate(first_movers,X3))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~greater(zero,growth_rate(first_movers,sk1(X2,X1)))|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater_or_equal(X3,sk2(X1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_first_movers_negative_growth_6)).
% 0.22/0.55 cnf(c_0_13, plain, (subpopulations(first_movers,efficient_producers,X1,sk1(X2,X1))|greater(sk2(X1),appear(efficient_producers,X1))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp_first_movers_negative_growth_1])).
% 0.22/0.55 cnf(c_0_14, hypothesis, (in_environment(X1,sk3(X1))|~environment(X1)|~stable(X1)), inference(fof_simplification,[status(thm)],[l11_7])).
% 0.22/0.55 cnf(c_0_15, plain, (greater_or_equal(sk1(X2,X1),X2)|greater(sk2(X1),appear(efficient_producers,X1))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp_first_movers_negative_growth_2])).
% 0.22/0.55 cnf(c_0_16, hypothesis, (greater(zero,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)],[l11_9])).
% 0.22/0.55 cnf(c_0_17, plain, (subpopulations(first_movers,efficient_producers,X1,sk1(X2,X1))|greater(sk2(X1),appear(efficient_producers,X1))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)), c_0_13).
% 0.22/0.55 cnf(c_0_18, hypothesis, (in_environment(X1,sk3(X1))|~environment(X1)|~stable(X1)), c_0_14).
% 0.22/0.55 cnf(c_0_19, plain, (greater_or_equal(sk1(X2,X1),X2)|greater(sk2(X1),appear(efficient_producers,X1))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)), c_0_15).
% 0.22/0.55 cnf(c_0_20, hypothesis, (greater(zero,growth_rate(first_movers,X2))|~environment(X1)|~stable(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)|~greater_or_equal(X2,sk3(X1))), c_0_16).
% 0.22/0.55 cnf(c_0_21, hypothesis, (greater(sk2(X1),appear(efficient_producers,X1))|subpopulations(first_movers,efficient_producers,X1,sk1(sk3(X1),X1))|~stable(X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_17, c_0_18])).
% 0.22/0.55 cnf(c_0_22, hypothesis, (greater_or_equal(sk1(sk3(X1),X1),sk3(X1))|greater(sk2(X1),appear(efficient_producers,X1))|~stable(X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_19, c_0_18])).
% 0.22/0.55 cnf(c_0_23, plain, (greater(sk2(X1),appear(efficient_producers,X1))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~greater(zero,growth_rate(first_movers,sk1(X2,X1)))), inference(fof_simplification,[status(thm)],[mp_first_movers_negative_growth_5])).
% 0.22/0.55 cnf(c_0_24, hypothesis, (greater(zero,growth_rate(first_movers,sk1(sk3(X1),X1)))|greater(sk2(X1),appear(efficient_producers,X1))|~stable(X1)|~environment(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_21]), c_0_22])).
% 0.22/0.55 cnf(c_0_25, negated_conjecture, (stable(sk4)), prove_l10_11).
% 0.22/0.55 cnf(c_0_26, negated_conjecture, (environment(sk4)), prove_l10_10).
% 0.22/0.55 cnf(c_0_27, plain, (greater(sk2(X1),appear(efficient_producers,X1))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~greater(zero,growth_rate(first_movers,sk1(X2,X1)))), c_0_23).
% 0.22/0.55 cnf(c_0_28, negated_conjecture, (greater(zero,growth_rate(first_movers,sk1(sk3(sk4),sk4)))|greater(sk2(sk4),appear(efficient_producers,sk4))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_24, c_0_25]), c_0_26])])).
% 0.22/0.55 cnf(c_0_29, negated_conjecture, (subpopulations(first_movers,efficient_producers,sk4,sk5(X1))|~greater(X1,appear(efficient_producers,sk4))), inference(fof_simplification,[status(thm)],[prove_l10_12])).
% 0.22/0.55 cnf(c_0_30, negated_conjecture, (greater(sk2(sk4),appear(efficient_producers,sk4))|~in_environment(sk4,sk3(sk4))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_28]), c_0_25]), c_0_26])])).
% 0.22/0.55 cnf(c_0_31, negated_conjecture, (~greater(X1,appear(efficient_producers,sk4))|~greater(zero,growth_rate(first_movers,sk5(X1)))), inference(fof_simplification,[status(thm)],[prove_l10_14])).
% 0.22/0.55 cnf(c_0_32, negated_conjecture, (greater_or_equal(sk5(X1),X1)|~greater(X1,appear(efficient_producers,sk4))), inference(fof_simplification,[status(thm)],[prove_l10_13])).
% 0.22/0.55 cnf(c_0_33, plain, (subpopulations(first_movers,efficient_producers,X1,sk1(X2,X1))|greater(zero,growth_rate(first_movers,X3))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater_or_equal(X3,sk2(X1))), inference(fof_simplification,[status(thm)],[mp_first_movers_negative_growth_3])).
% 0.22/0.55 cnf(c_0_34, negated_conjecture, (subpopulations(first_movers,efficient_producers,sk4,sk5(X1))|~greater(X1,appear(efficient_producers,sk4))), c_0_29).
% 0.22/0.55 cnf(c_0_35, hypothesis, (greater(sk2(sk4),appear(efficient_producers,sk4))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_18]), c_0_25]), c_0_26])])).
% 0.22/0.55 cnf(c_0_36, negated_conjecture, (~greater(X1,appear(efficient_producers,sk4))|~greater(zero,growth_rate(first_movers,sk5(X1)))), c_0_31).
% 0.22/0.55 cnf(c_0_37, negated_conjecture, (greater_or_equal(sk5(X1),X1)|~greater(X1,appear(efficient_producers,sk4))), c_0_32).
% 0.22/0.55 cnf(c_0_38, plain, (greater_or_equal(sk1(X2,X1),X2)|greater(zero,growth_rate(first_movers,X3))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater_or_equal(X3,sk2(X1))), inference(fof_simplification,[status(thm)],[mp_first_movers_negative_growth_4])).
% 0.22/0.55 cnf(c_0_39, plain, (subpopulations(first_movers,efficient_producers,X1,sk1(X2,X1))|greater(zero,growth_rate(first_movers,X3))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater_or_equal(X3,sk2(X1))), c_0_33).
% 0.22/0.55 cnf(c_0_40, negated_conjecture, (subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))), inference(spm,[status(thm)],[c_0_34, c_0_35])).
% 0.22/0.55 cnf(c_0_41, negated_conjecture, (~greater(zero,growth_rate(first_movers,sk5(sk2(sk4))))), inference(spm,[status(thm)],[c_0_36, c_0_35])).
% 0.22/0.55 cnf(c_0_42, negated_conjecture, (greater_or_equal(sk5(sk2(sk4)),sk2(sk4))), inference(spm,[status(thm)],[c_0_37, c_0_35])).
% 0.22/0.55 cnf(c_0_43, plain, (greater_or_equal(sk1(X2,X1),X2)|greater(zero,growth_rate(first_movers,X3))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater_or_equal(X3,sk2(X1))), c_0_38).
% 0.22/0.55 cnf(c_0_44, plain, (greater(zero,growth_rate(first_movers,X3))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~greater(zero,growth_rate(first_movers,sk1(X2,X1)))|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater_or_equal(X3,sk2(X1))), inference(fof_simplification,[status(thm)],[mp_first_movers_negative_growth_6])).
% 0.22/0.55 cnf(c_0_45, negated_conjecture, (subpopulations(first_movers,efficient_producers,sk4,sk1(X1,sk4))|~in_environment(sk4,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_40]), c_0_25]), c_0_26])]), c_0_41]), c_0_42])])).
% 0.22/0.55 cnf(c_0_46, negated_conjecture, (greater_or_equal(sk1(X1,sk4),X1)|~in_environment(sk4,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_40]), c_0_25]), c_0_26])]), c_0_41]), c_0_42])])).
% 0.22/0.55 cnf(c_0_47, plain, (greater(zero,growth_rate(first_movers,X3))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~greater(zero,growth_rate(first_movers,sk1(X2,X1)))|~subpopulations(first_movers,efficient_producers,X1,X3)|~greater_or_equal(X3,sk2(X1))), c_0_44).
% 0.22/0.55 cnf(c_0_48, hypothesis, (subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_18]), c_0_25]), c_0_26])])).
% 0.22/0.55 cnf(c_0_49, hypothesis, (greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46, c_0_18]), c_0_25]), c_0_26])])).
% 0.22/0.55 cnf(c_0_50, negated_conjecture, (~greater(zero,growth_rate(first_movers,sk1(X1,sk4)))|~in_environment(sk4,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_40]), c_0_25]), c_0_26])]), c_0_41]), c_0_42])])).
% 0.22/0.55 cnf(c_0_51, hypothesis, (greater(zero,growth_rate(first_movers,sk1(sk3(sk4),sk4)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_48]), c_0_49]), c_0_25]), c_0_26])])).
% 0.22/0.55 cnf(c_0_52, negated_conjecture, (~in_environment(sk4,sk3(sk4))), inference(spm,[status(thm)],[c_0_50, c_0_51])).
% 0.22/0.55 cnf(c_0_53, hypothesis, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52, c_0_18]), c_0_25]), c_0_26])]), ['proof']).
% 0.22/0.55 % SZS output end Proof
% 0.22/0.55 % User time : 0.006 s
% 0.22/0.55 % System time : 0.002 s
% 0.22/0.55 % Total time : 0.008 s
% 0.22/0.55 % User time : 0.007 s
% 0.22/0.55 % System time : 0.006 s
% 0.22/0.55 % Total time : 0.013 s
% 0.22/0.55
%------------------------------------------------------------------------------