%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT027+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n031.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 : Theorem 0.24s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT027+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.35 % Computer : n031.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.01/0.35 % CPULimit : 300
% 0.01/0.35 % WCLimit : 300
% 0.01/0.35 % DateTime : Mon Sep 7 12:16:26 UTC 2026
% 0.01/0.36 % CPUTime :
% 0.24/0.47 start to proof:theBenchmark.p
% 0.24/0.55 % Version : CSI_E---1.1
% 0.24/0.55 % Problem : theBenchmark.p
% 0.24/0.55 % Proof found!
% 0.24/0.55 % SZS status Theorem for theBenchmark.p
% 0.24/0.55 % SZS output start Proof
% 0.24/0.55 fof(mp_greater_transitivity, axiom, ![X6, X7, X8]:(((greater(X6,X7)&greater(X7,X8))=>greater(X6,X8))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_greater_transitivity)).
% 0.24/0.55 fof(l10, hypothesis, ![X1]:(((environment(X1)&stable(X1))=>?[X2]:((greater(X2,appear(efficient_producers,X1))&![X3]:(((subpopulations(first_movers,efficient_producers,X1,X3)&greater_or_equal(X3,X2))=>greater(zero,growth_rate(first_movers,X3)))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l10)).
% 0.24/0.55 fof(mp_greater_or_equal, axiom, ![X6, X7]:((greater_or_equal(X6,X7)<=>(greater(X6,X7)|X6=X7))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_greater_or_equal)).
% 0.24/0.55 fof(mp_contracts_from, axiom, ![X1, X2]:(((((environment(X1)&stable(X1))&in_environment(X1,X2))&![X3]:(((greater(cardinality_at_time(first_movers,X3),zero)&greater_or_equal(X3,X2))=>greater(zero,growth_rate(first_movers,X3)))))=>contracts_from(X2,first_movers))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_contracts_from)).
% 0.24/0.55 fof(t6, hypothesis, ![X1, X3]:((((environment(X1)&in_environment(X1,X3))&greater_or_equal(X3,appear(efficient_producers,X1)))=>greater(cardinality_at_time(efficient_producers,X3),zero))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t6)).
% 0.24/0.55 fof(mp_non_empty_fm_and_ep, axiom, ![X1, X3]:(((((environment(X1)&in_environment(X1,X3))&greater(cardinality_at_time(first_movers,X3),zero))&greater(cardinality_at_time(efficient_producers,X3),zero))=>subpopulations(first_movers,efficient_producers,X1,X3))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_non_empty_fm_and_ep)).
% 0.24/0.55 fof(mp_long_stable_environments, axiom, ![X1, X4, X5]:(((((environment(X1)&stable(X1))&in_environment(X1,X4))&greater(X5,X4))=>in_environment(X1,X5))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_long_stable_environments)).
% 0.24/0.55 fof(mp_EP_in_stable_environments, axiom, ![X1]:(((environment(X1)&stable(X1))=>in_environment(X1,appear(efficient_producers,X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_EP_in_stable_environments)).
% 0.24/0.55 fof(prove_l9, conjecture, ![X1]:(((environment(X1)&stable(X1))=>?[X2]:((greater(X2,appear(efficient_producers,X1))&contracts_from(X2,first_movers))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_l9)).
% 0.24/0.55 fof(c_0_9, plain, ![X18, X19, X20]:((~greater(X18,X19)|~greater(X19,X20)|greater(X18,X20))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_greater_transitivity])])])).
% 0.24/0.55 fof(c_0_10, hypothesis, ![X25, X27]:(((greater(esk2_1(X25),appear(efficient_producers,X25))|(~environment(X25)|~stable(X25)))&(~subpopulations(first_movers,efficient_producers,X25,X27)|~greater_or_equal(X27,esk2_1(X25))|greater(zero,growth_rate(first_movers,X27))|(~environment(X25)|~stable(X25))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[l10])])])])])])).
% 0.24/0.55 fof(c_0_11, plain, ![X21, X22]:(((~greater_or_equal(X21,X22)|(greater(X21,X22)|X21=X22))&((~greater(X21,X22)|greater_or_equal(X21,X22))&(X21!=X22|greater_or_equal(X21,X22))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_greater_or_equal])])])])).
% 0.24/0.55 fof(c_0_12, plain, ![X9, X10]:((((greater(cardinality_at_time(first_movers,esk1_2(X9,X10)),zero)|(~environment(X9)|~stable(X9)|~in_environment(X9,X10))|contracts_from(X10,first_movers))&(greater_or_equal(esk1_2(X9,X10),X10)|(~environment(X9)|~stable(X9)|~in_environment(X9,X10))|contracts_from(X10,first_movers)))&(~greater(zero,growth_rate(first_movers,esk1_2(X9,X10)))|(~environment(X9)|~stable(X9)|~in_environment(X9,X10))|contracts_from(X10,first_movers)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_contracts_from])])])])])).
% 0.24/0.55 fof(c_0_13, hypothesis, ![X23, X24]:((~environment(X23)|~in_environment(X23,X24)|~greater_or_equal(X24,appear(efficient_producers,X23))|greater(cardinality_at_time(efficient_producers,X24),zero))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t6])])])).
% 0.24/0.55 cnf(c_0_14, plain, (greater(X1,X3)|~greater(X1,X2)|~greater(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.24/0.55 cnf(c_0_15, hypothesis, (greater(esk2_1(X1),appear(efficient_producers,X1))|~environment(X1)|~stable(X1)), inference(split_conjunct,[status(thm)],[c_0_10])).
% 0.24/0.55 cnf(c_0_16, plain, (greater(X1,X2)|X1=X2|~greater_or_equal(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.24/0.55 cnf(c_0_17, plain, (greater_or_equal(esk1_2(X1,X2),X2)|contracts_from(X2,first_movers)|~environment(X1)|~stable(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.24/0.55 cnf(c_0_18, hypothesis, (greater(zero,growth_rate(first_movers,X2))|~subpopulations(first_movers,efficient_producers,X1,X2)|~greater_or_equal(X2,esk2_1(X1))|~environment(X1)|~stable(X1)), inference(split_conjunct,[status(thm)],[c_0_10])).
% 0.24/0.55 cnf(c_0_19, plain, (contracts_from(X2,first_movers)|~greater(zero,growth_rate(first_movers,esk1_2(X1,X2)))|~environment(X1)|~stable(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.24/0.55 fof(c_0_20, plain, ![X12, X13]:((~environment(X12)|~in_environment(X12,X13)|~greater(cardinality_at_time(first_movers,X13),zero)|~greater(cardinality_at_time(efficient_producers,X13),zero)|subpopulations(first_movers,efficient_producers,X12,X13))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_non_empty_fm_and_ep])])])).
% 0.24/0.55 cnf(c_0_21, hypothesis, (greater(cardinality_at_time(efficient_producers,X2),zero)|~environment(X1)|~in_environment(X1,X2)|~greater_or_equal(X2,appear(efficient_producers,X1))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.24/0.55 cnf(c_0_22, plain, (greater_or_equal(X1,X2)|~greater(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.24/0.55 cnf(c_0_23, hypothesis, (greater(X1,appear(efficient_producers,X2))|~greater(X1,esk2_1(X2))|~stable(X2)|~environment(X2)), inference(spm,[status(thm)],[c_0_14, c_0_15])).
% 0.24/0.55 cnf(c_0_24, plain, (esk1_2(X1,X2)=X2|contracts_from(X2,first_movers)|greater(esk1_2(X1,X2),X2)|~in_environment(X1,X2)|~stable(X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_16, c_0_17])).
% 0.24/0.55 cnf(c_0_25, hypothesis, (contracts_from(esk2_1(X1),first_movers)|~subpopulations(first_movers,efficient_producers,X1,esk1_2(X2,esk2_1(X1)))|~in_environment(X2,esk2_1(X1))|~stable(X1)|~stable(X2)|~environment(X1)|~environment(X2)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_18, c_0_17]), c_0_19])).
% 0.24/0.55 cnf(c_0_26, 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(split_conjunct,[status(thm)],[c_0_20])).
% 0.24/0.55 cnf(c_0_27, plain, (greater(cardinality_at_time(first_movers,esk1_2(X1,X2)),zero)|contracts_from(X2,first_movers)|~environment(X1)|~stable(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.24/0.55 fof(c_0_28, plain, ![X14, X15, X16]:((~environment(X14)|~stable(X14)|~in_environment(X14,X15)|~greater(X16,X15)|in_environment(X14,X16))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_long_stable_environments])])])).
% 0.24/0.55 cnf(c_0_29, 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_21, c_0_22])).
% 0.24/0.55 cnf(c_0_30, hypothesis, (esk1_2(X1,esk2_1(X2))=esk2_1(X2)|contracts_from(esk2_1(X2),first_movers)|greater(esk1_2(X1,esk2_1(X2)),appear(efficient_producers,X2))|~in_environment(X1,esk2_1(X2))|~stable(X2)|~stable(X1)|~environment(X2)|~environment(X1)), inference(spm,[status(thm)],[c_0_23, c_0_24])).
% 0.24/0.55 cnf(c_0_31, hypothesis, (contracts_from(esk2_1(X1),first_movers)|~greater(cardinality_at_time(efficient_producers,esk1_2(X2,esk2_1(X1))),zero)|~in_environment(X1,esk1_2(X2,esk2_1(X1)))|~in_environment(X2,esk2_1(X1))|~stable(X1)|~stable(X2)|~environment(X1)|~environment(X2)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_25, c_0_26]), c_0_27])).
% 0.24/0.55 cnf(c_0_32, plain, (in_environment(X1,X3)|~environment(X1)|~stable(X1)|~in_environment(X1,X2)|~greater(X3,X2)), inference(split_conjunct,[status(thm)],[c_0_28])).
% 0.24/0.55 cnf(c_0_33, plain, (greater_or_equal(X1,X2)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.24/0.55 fof(c_0_34, plain, ![X17]:((~environment(X17)|~stable(X17)|in_environment(X17,appear(efficient_producers,X17)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_EP_in_stable_environments])])])).
% 0.24/0.55 cnf(c_0_35, hypothesis, (esk1_2(X1,esk2_1(X2))=esk2_1(X2)|contracts_from(esk2_1(X2),first_movers)|~in_environment(X2,esk1_2(X1,esk2_1(X2)))|~in_environment(X1,esk2_1(X2))|~stable(X2)|~stable(X1)|~environment(X2)|~environment(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_29, c_0_30]), c_0_31])).
% 0.24/0.55 cnf(c_0_36, plain, (esk1_2(X1,X2)=X2|contracts_from(X2,first_movers)|in_environment(X3,esk1_2(X1,X2))|~in_environment(X3,X2)|~in_environment(X1,X2)|~stable(X3)|~stable(X1)|~environment(X3)|~environment(X1)), inference(spm,[status(thm)],[c_0_32, c_0_24])).
% 0.24/0.55 cnf(c_0_37, plain, (greater_or_equal(X1,X1)), inference(er,[status(thm)],[c_0_33])).
% 0.24/0.55 cnf(c_0_38, hypothesis, (greater(cardinality_at_time(efficient_producers,esk2_1(X1)),zero)|~in_environment(X1,esk2_1(X1))|~stable(X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_29, c_0_15])).
% 0.24/0.55 cnf(c_0_39, hypothesis, (in_environment(X1,esk2_1(X2))|~in_environment(X1,appear(efficient_producers,X2))|~stable(X1)|~stable(X2)|~environment(X1)|~environment(X2)), inference(spm,[status(thm)],[c_0_32, c_0_15])).
% 0.24/0.55 cnf(c_0_40, plain, (in_environment(X1,appear(efficient_producers,X1))|~environment(X1)|~stable(X1)), inference(split_conjunct,[status(thm)],[c_0_34])).
% 0.24/0.55 cnf(c_0_41, hypothesis, (esk1_2(X1,esk2_1(X2))=esk2_1(X2)|contracts_from(esk2_1(X2),first_movers)|~in_environment(X1,esk2_1(X2))|~in_environment(X2,esk2_1(X2))|~stable(X2)|~stable(X1)|~environment(X2)|~environment(X1)), inference(spm,[status(thm)],[c_0_35, c_0_36])).
% 0.24/0.55 cnf(c_0_42, hypothesis, (greater(zero,growth_rate(first_movers,esk2_1(X1)))|~subpopulations(first_movers,efficient_producers,X1,esk2_1(X1))|~stable(X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_18, c_0_37])).
% 0.24/0.55 cnf(c_0_43, hypothesis, (greater(cardinality_at_time(efficient_producers,esk2_1(X1)),zero)|~stable(X1)|~environment(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_39]), c_0_40])).
% 0.24/0.55 cnf(c_0_44, hypothesis, (esk1_2(X1,esk2_1(X2))=esk2_1(X2)|contracts_from(esk2_1(X2),first_movers)|~in_environment(X1,esk2_1(X2))|~stable(X2)|~stable(X1)|~environment(X2)|~environment(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_39]), c_0_40])).
% 0.24/0.55 cnf(c_0_45, hypothesis, (greater(zero,growth_rate(first_movers,esk2_1(X1)))|~greater(cardinality_at_time(first_movers,esk2_1(X1)),zero)|~in_environment(X1,esk2_1(X1))|~stable(X1)|~environment(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_26]), c_0_43])).
% 0.24/0.55 fof(c_0_46, negated_conjecture, ~(![X1]:(((environment(X1)&stable(X1))=>?[X2]:((greater(X2,appear(efficient_producers,X1))&contracts_from(X2,first_movers)))))), inference(assume_negation,[status(cth)],[prove_l9])).
% 0.24/0.55 cnf(c_0_47, hypothesis, (contracts_from(esk2_1(X1),first_movers)|~greater(zero,growth_rate(first_movers,esk2_1(X1)))|~in_environment(X2,esk2_1(X1))|~stable(X2)|~stable(X1)|~environment(X2)|~environment(X1)), inference(spm,[status(thm)],[c_0_19, c_0_44])).
% 0.24/0.55 cnf(c_0_48, hypothesis, (greater(zero,growth_rate(first_movers,esk2_1(X1)))|~greater(cardinality_at_time(first_movers,esk2_1(X1)),zero)|~stable(X1)|~environment(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_39]), c_0_40])).
% 0.24/0.55 cnf(c_0_49, hypothesis, (contracts_from(esk2_1(X1),first_movers)|greater(cardinality_at_time(first_movers,esk2_1(X1)),zero)|~in_environment(X2,esk2_1(X1))|~stable(X2)|~stable(X1)|~environment(X2)|~environment(X1)), inference(spm,[status(thm)],[c_0_27, c_0_44])).
% 0.24/0.55 fof(c_0_50, negated_conjecture, ![X29]:(((environment(esk3_0)&stable(esk3_0))&(~greater(X29,appear(efficient_producers,esk3_0))|~contracts_from(X29,first_movers)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_46])])])])])).
% 0.24/0.55 cnf(c_0_51, hypothesis, (contracts_from(esk2_1(X1),first_movers)|~in_environment(X2,esk2_1(X1))|~stable(X2)|~stable(X1)|~environment(X2)|~environment(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_48]), c_0_49])).
% 0.24/0.55 cnf(c_0_52, negated_conjecture, (~greater(X1,appear(efficient_producers,esk3_0))|~contracts_from(X1,first_movers)), inference(split_conjunct,[status(thm)],[c_0_50])).
% 0.24/0.55 cnf(c_0_53, negated_conjecture, (stable(esk3_0)), inference(split_conjunct,[status(thm)],[c_0_50])).
% 0.24/0.55 cnf(c_0_54, negated_conjecture, (environment(esk3_0)), inference(split_conjunct,[status(thm)],[c_0_50])).
% 0.24/0.55 cnf(c_0_55, hypothesis, (contracts_from(esk2_1(X1),first_movers)|~in_environment(X2,appear(efficient_producers,X1))|~stable(X2)|~stable(X1)|~environment(X2)|~environment(X1)), inference(spm,[status(thm)],[c_0_51, c_0_39])).
% 0.24/0.55 cnf(c_0_56, negated_conjecture, (~contracts_from(esk2_1(esk3_0),first_movers)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52, c_0_15]), c_0_53]), c_0_54])])).
% 0.24/0.55 cnf(c_0_57, hypothesis, (contracts_from(esk2_1(X1),first_movers)|~stable(X1)|~environment(X1)), inference(spm,[status(thm)],[c_0_55, c_0_40])).
% 0.24/0.55 cnf(c_0_58, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_57]), c_0_53]), c_0_54])]), ['proof']).
% 0.24/0.55 % SZS output end Proof
% 0.24/0.55 % User time : 0.007 s
% 0.24/0.55 % System time : 0.005 s
% 0.24/0.55 % Total time : 0.012 s
% 0.24/0.55 % User time : 0.025 s
% 0.24/0.55 % System time : 0.013 s
% 0.24/0.55 % Total time : 0.038 s
% 0.24/0.55
%------------------------------------------------------------------------------