%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT027-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n011.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.25s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT027-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 7 12:14:15 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.13/0.46 start to proof:theBenchmark.p
% 0.25/0.55 % Version : CSI_E---1.1
% 0.25/0.55 % Problem : theBenchmark.p
% 0.25/0.55 % Proof found!
% 0.25/0.55 # SZS status Unsatisfiable
% 0.25/0.55 % SZS output start Proof
% 0.25/0.55 cnf(mp_long_stable_environments_28, axiom, (in_environment(X1,X3)|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~greater(X3,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_long_stable_environments_28)).
% 0.25/0.55 cnf(l10_35, hypothesis, (greater(sk2(X1),appear(efficient_producers,X1))|~environment(X1)|~stable(X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l10_35)).
% 0.25/0.55 cnf(mp_contracts_from_25, axiom, (greater_or_equal(sk1(X2,X1),X2)|contracts_from(X2,first_movers)|~environment(X1)|~stable(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_contracts_from_25)).
% 0.25/0.55 cnf(mp_EP_in_stable_environments_29, axiom, (in_environment(X1,appear(efficient_producers,X1))|~environment(X1)|~stable(X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_EP_in_stable_environments_29)).
% 0.25/0.55 cnf(prove_l9_39, negated_conjecture, (~greater(X1,appear(efficient_producers,sk3))|~contracts_from(X1,first_movers)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_l9_39)).
% 0.25/0.55 cnf(prove_l9_38, negated_conjecture, (stable(sk3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_l9_38)).
% 0.25/0.55 cnf(prove_l9_37, negated_conjecture, (environment(sk3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_l9_37)).
% 0.25/0.55 cnf(mp_contracts_from_24, axiom, (greater(cardinality_at_time(first_movers,sk1(X2,X1)),zero)|contracts_from(X2,first_movers)|~environment(X1)|~stable(X1)|~in_environment(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_contracts_from_24)).
% 0.25/0.55 cnf(mp_greater_transitivity_30, axiom, (greater(X1,X3)|~greater(X1,X2)|~greater(X2,X3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_greater_transitivity_30)).
% 0.25/0.55 cnf(mp_greater_or_equal_31, axiom, (greater(X1,X2)|X1=X2|~greater_or_equal(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_greater_or_equal_31)).
% 0.25/0.55 cnf(l10_36, hypothesis, (greater(zero,growth_rate(first_movers,X2))|~environment(X1)|~stable(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)|~greater_or_equal(X2,sk2(X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l10_36)).
% 0.25/0.55 cnf(t6_34, 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_34)).
% 0.25/0.55 cnf(mp_greater_or_equal_32, axiom, (greater_or_equal(X1,X2)|~greater(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_greater_or_equal_32)).
% 0.25/0.55 cnf(mp_non_empty_fm_and_ep_27, 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_non_empty_fm_and_ep_27)).
% 0.25/0.55 cnf(mp_contracts_from_26, axiom, (contracts_from(X2,first_movers)|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~greater(zero,growth_rate(first_movers,sk1(X2,X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_contracts_from_26)).
% 0.25/0.55 cnf(c_0_15, plain, (in_environment(X1,X3)|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~greater(X3,X2)), inference(fof_simplification,[status(thm)],[mp_long_stable_environments_28])).
% 0.25/0.55 cnf(c_0_16, hypothesis, (greater(sk2(X1),appear(efficient_producers,X1))|~environment(X1)|~stable(X1)), inference(fof_simplification,[status(thm)],[l10_35])).
% 0.25/0.55 cnf(c_0_17, plain, (greater_or_equal(sk1(X2,X1),X2)|contracts_from(X2,first_movers)|~environment(X1)|~stable(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp_contracts_from_25])).
% 0.25/0.55 cnf(c_0_18, plain, (in_environment(X1,X3)|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~greater(X3,X2)), c_0_15).
% 0.25/0.55 cnf(c_0_19, hypothesis, (greater(sk2(X1),appear(efficient_producers,X1))|~environment(X1)|~stable(X1)), c_0_16).
% 0.25/0.55 cnf(c_0_20, plain, (greater_or_equal(sk1(X2,X1),X2)|contracts_from(X2,first_movers)|~environment(X1)|~stable(X1)|~in_environment(X1,X2)), c_0_17).
% 0.25/0.55 cnf(c_0_21, hypothesis, (in_environment(X1,sk2(X2))|~in_environment(X1,appear(efficient_producers,X2))|~stable(X1)|~stable(X2)|~environment(X1)|~environment(X2)), inference(spm,[status(thm)],[c_0_18, c_0_19])).
% 0.25/0.55 cnf(c_0_22, plain, (in_environment(X1,appear(efficient_producers,X1))|~environment(X1)|~stable(X1)), inference(fof_simplification,[status(thm)],[mp_EP_in_stable_environments_29])).
% 0.25/0.55 cnf(c_0_23, negated_conjecture, (~greater(X1,appear(efficient_producers,sk3))|~contracts_from(X1,first_movers)), inference(fof_simplification,[status(thm)],[prove_l9_39])).
% 0.25/0.55 cnf(c_0_24, hypothesis, (greater_or_equal(sk1(sk2(X1),X2),sk2(X1))|contracts_from(sk2(X1),first_movers)|~in_environment(X2,appear(efficient_producers,X1))|~stable(X2)|~stable(X1)|~environment(X2)|~environment(X1)), inference(spm,[status(thm)],[c_0_20, c_0_21])).
% 0.25/0.55 cnf(c_0_25, plain, (in_environment(X1,appear(efficient_producers,X1))|~environment(X1)|~stable(X1)), c_0_22).
% 0.25/0.55 cnf(c_0_26, negated_conjecture, (~greater(X1,appear(efficient_producers,sk3))|~contracts_from(X1,first_movers)), c_0_23).
% 0.25/0.55 cnf(c_0_27, negated_conjecture, (stable(sk3)), prove_l9_38).
% 0.25/0.55 cnf(c_0_28, negated_conjecture, (environment(sk3)), prove_l9_37).
% 0.25/0.55 cnf(c_0_29, plain, (greater(cardinality_at_time(first_movers,sk1(X2,X1)),zero)|contracts_from(X2,first_movers)|~environment(X1)|~stable(X1)|~in_environment(X1,X2)), inference(fof_simplification,[status(thm)],[mp_contracts_from_24])).
% 0.25/0.55 cnf(c_0_30, plain, (greater(X1,X3)|~greater(X1,X2)|~greater(X2,X3)), inference(fof_simplification,[status(thm)],[mp_greater_transitivity_30])).
% 0.25/0.55 cnf(c_0_31, plain, (greater(X1,X2)|X1=X2|~greater_or_equal(X1,X2)), inference(fof_simplification,[status(thm)],[mp_greater_or_equal_31])).
% 0.25/0.55 cnf(c_0_32, hypothesis, (greater_or_equal(sk1(sk2(X1),X1),sk2(X1))|contracts_from(sk2(X1),first_movers)|~stable(X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_24, c_0_25])).
% 0.25/0.55 cnf(c_0_33, negated_conjecture, (~contracts_from(sk2(sk3),first_movers)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_26, c_0_19]), c_0_27]), c_0_28])])).
% 0.25/0.55 cnf(c_0_34, plain, (greater(cardinality_at_time(first_movers,sk1(X2,X1)),zero)|contracts_from(X2,first_movers)|~environment(X1)|~stable(X1)|~in_environment(X1,X2)), c_0_29).
% 0.25/0.55 cnf(c_0_35, plain, (greater(X1,X3)|~greater(X1,X2)|~greater(X2,X3)), c_0_30).
% 0.25/0.55 cnf(c_0_36, plain, (greater(X1,X2)|X1=X2|~greater_or_equal(X1,X2)), c_0_31).
% 0.25/0.55 cnf(c_0_37, negated_conjecture, (greater_or_equal(sk1(sk2(sk3),sk3),sk2(sk3))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_27]), c_0_28])]), c_0_33])).
% 0.25/0.55 cnf(c_0_38, hypothesis, (greater(zero,growth_rate(first_movers,X2))|~environment(X1)|~stable(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)|~greater_or_equal(X2,sk2(X1))), inference(fof_simplification,[status(thm)],[l10_36])).
% 0.25/0.55 cnf(c_0_39, hypothesis, (contracts_from(sk2(X1),first_movers)|greater(cardinality_at_time(first_movers,sk1(sk2(X1),X2)),zero)|~in_environment(X2,appear(efficient_producers,X1))|~stable(X2)|~stable(X1)|~environment(X2)|~environment(X1)), inference(spm,[status(thm)],[c_0_34, c_0_21])).
% 0.25/0.55 cnf(c_0_40, 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_34])).
% 0.25/0.55 cnf(c_0_41, plain, (greater_or_equal(X1,X2)|~greater(X1,X2)), inference(fof_simplification,[status(thm)],[mp_greater_or_equal_32])).
% 0.25/0.55 cnf(c_0_42, hypothesis, (greater(X1,appear(efficient_producers,X2))|~greater(X1,sk2(X2))|~stable(X2)|~environment(X2)), inference(spm,[status(thm)],[c_0_35, c_0_19])).
% 0.25/0.55 cnf(c_0_43, negated_conjecture, (sk1(sk2(sk3),sk3)=sk2(sk3)|greater(sk1(sk2(sk3),sk3),sk2(sk3))), inference(spm,[status(thm)],[c_0_36, c_0_37])).
% 0.25/0.55 cnf(c_0_44, hypothesis, (greater(zero,growth_rate(first_movers,X2))|~environment(X1)|~stable(X1)|~subpopulations(first_movers,efficient_producers,X1,X2)|~greater_or_equal(X2,sk2(X1))), c_0_38).
% 0.25/0.55 cnf(c_0_45, 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_non_empty_fm_and_ep_27])).
% 0.25/0.55 cnf(c_0_46, hypothesis, (contracts_from(sk2(X1),first_movers)|greater(cardinality_at_time(first_movers,sk1(sk2(X1),X1)),zero)|~stable(X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_39, c_0_25])).
% 0.25/0.55 cnf(c_0_47, 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_40).
% 0.25/0.55 cnf(c_0_48, plain, (greater_or_equal(X1,X2)|~greater(X1,X2)), c_0_41).
% 0.25/0.55 cnf(c_0_49, hypothesis, (sk1(sk2(sk3),sk3)=sk2(sk3)|greater(sk1(sk2(sk3),sk3),appear(efficient_producers,sk3))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_43]), c_0_27]), c_0_28])])).
% 0.25/0.55 cnf(c_0_50, plain, (contracts_from(X2,first_movers)|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~greater(zero,growth_rate(first_movers,sk1(X2,X1)))), inference(fof_simplification,[status(thm)],[mp_contracts_from_26])).
% 0.25/0.55 cnf(c_0_51, hypothesis, (greater(zero,growth_rate(first_movers,sk1(sk2(sk3),sk3)))|~subpopulations(first_movers,efficient_producers,sk3,sk1(sk2(sk3),sk3))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_37]), c_0_27]), c_0_28])])).
% 0.25/0.55 cnf(c_0_52, 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_45).
% 0.25/0.55 cnf(c_0_53, negated_conjecture, (greater(cardinality_at_time(first_movers,sk1(sk2(sk3),sk3)),zero)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46, c_0_27]), c_0_28])]), c_0_33])).
% 0.25/0.55 cnf(c_0_54, hypothesis, (greater(cardinality_at_time(efficient_producers,X1),zero)|~greater(X1,appear(efficient_producers,X2))|~in_environment(X2,X1)|~environment(X2)), inference(spm,[status(thm)],[c_0_47, c_0_48])).
% 0.25/0.55 cnf(c_0_55, hypothesis, (sk1(sk2(sk3),sk3)=sk2(sk3)|in_environment(X1,sk1(sk2(sk3),sk3))|~in_environment(X1,appear(efficient_producers,sk3))|~stable(X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_18, c_0_49])).
% 0.25/0.55 cnf(c_0_56, plain, (contracts_from(X2,first_movers)|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~greater(zero,growth_rate(first_movers,sk1(X2,X1)))), c_0_50).
% 0.25/0.55 cnf(c_0_57, hypothesis, (greater(zero,growth_rate(first_movers,sk1(sk2(sk3),sk3)))|~greater(cardinality_at_time(efficient_producers,sk1(sk2(sk3),sk3)),zero)|~in_environment(sk3,sk1(sk2(sk3),sk3))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_52]), c_0_28])]), c_0_53])])).
% 0.25/0.55 cnf(c_0_58, hypothesis, (sk1(sk2(sk3),sk3)=sk2(sk3)|greater(cardinality_at_time(efficient_producers,sk1(sk2(sk3),sk3)),zero)|~in_environment(sk3,sk1(sk2(sk3),sk3))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54, c_0_49]), c_0_28])])).
% 0.25/0.55 cnf(c_0_59, hypothesis, (sk1(sk2(sk3),sk3)=sk2(sk3)|in_environment(sk3,sk1(sk2(sk3),sk3))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_55, c_0_25]), c_0_27]), c_0_28])])).
% 0.25/0.55 cnf(c_0_60, hypothesis, (~greater(cardinality_at_time(efficient_producers,sk1(sk2(sk3),sk3)),zero)|~in_environment(sk3,sk1(sk2(sk3),sk3))|~in_environment(sk3,sk2(sk3))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_57]), c_0_27]), c_0_28])]), c_0_33])).
% 0.25/0.55 cnf(c_0_61, hypothesis, (sk1(sk2(sk3),sk3)=sk2(sk3)|greater(cardinality_at_time(efficient_producers,sk1(sk2(sk3),sk3)),zero)), inference(spm,[status(thm)],[c_0_58, c_0_59])).
% 0.25/0.55 cnf(c_0_62, hypothesis, (sk1(sk2(sk3),sk3)=sk2(sk3)|~in_environment(sk3,sk2(sk3))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_61]), c_0_59])).
% 0.25/0.55 cnf(c_0_63, hypothesis, (greater(cardinality_at_time(efficient_producers,sk2(X1)),zero)|~in_environment(X1,sk2(X1))|~stable(X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_54, c_0_19])).
% 0.25/0.55 cnf(c_0_64, hypothesis, (~greater(cardinality_at_time(efficient_producers,sk2(sk3)),zero)|~in_environment(sk3,sk2(sk3))), inference(spm,[status(thm)],[c_0_60, c_0_62])).
% 0.25/0.55 cnf(c_0_65, hypothesis, (greater(cardinality_at_time(efficient_producers,sk2(X1)),zero)|~stable(X1)|~environment(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_21]), c_0_25])).
% 0.25/0.55 cnf(c_0_66, hypothesis, (~in_environment(sk3,sk2(sk3))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_64, c_0_65]), c_0_27]), c_0_28])])).
% 0.25/0.55 cnf(c_0_67, hypothesis, (~in_environment(sk3,appear(efficient_producers,sk3))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66, c_0_21]), c_0_27]), c_0_28])])).
% 0.25/0.55 cnf(c_0_68, hypothesis, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_25]), c_0_27]), c_0_28])]), ['proof']).
% 0.25/0.55 % SZS output end Proof
% 0.25/0.55 % User time : 0.008 s
% 0.25/0.55 % System time : 0.002 s
% 0.25/0.55 % Total time : 0.010 s
% 0.25/0.55 % User time : 0.033 s
% 0.25/0.55 % System time : 0.009 s
% 0.25/0.55 % Total time : 0.042 s
% 0.25/0.55
%------------------------------------------------------------------------------