%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT039+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n020.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:32 AM UTC 2026
% Result : Theorem 0.24s 0.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT039+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.07/0.34 % Computer : n020.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:54:58 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.13/0.46 start to proof:theBenchmark.p
% 0.24/0.52 % Version : CSI_E---1.1
% 0.24/0.52 % Problem : theBenchmark.p
% 0.24/0.52 % Proof found!
% 0.24/0.52 % SZS status Theorem for theBenchmark.p
% 0.24/0.52 % SZS output start Proof
% 0.24/0.52 fof(mp_greater_transitivity, axiom, ![X4, X5, X6]:(((greater(X4,X5)&greater(X5,X6))=>greater(X4,X6))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_greater_transitivity)).
% 0.24/0.52 fof(mp4_critical_point, axiom, ![X1]:(((observational_period(X1)&slow_change(X1))=>![X2]:(((environment(X2)&in_environment(X1,X2))=>?[X3]:((in_environment(X2,X3)&greater(X3,critical_point(X2)))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp4_critical_point)).
% 0.24/0.52 fof(mp_greater_or_equal, axiom, ![X4, X5]:((greater_or_equal(X4,X5)<=>(greater(X4,X5)|X4=X5))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_greater_or_equal)).
% 0.24/0.52 fof(mp_environment_end_point, axiom, ![X2, X3]:(((environment(X2)&in_environment(X2,X3))=>greater_or_equal(end_time(X2),X3))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_environment_end_point)).
% 0.24/0.52 fof(mp_time_in_environment, axiom, ![X2, X3]:((((environment(X2)&greater_or_equal(X3,start_time(X2)))&greater_or_equal(end_time(X2),X3))=>in_environment(X2,X3))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_time_in_environment)).
% 0.24/0.52 fof(mp_time_of_critical_point, axiom, ![X2]:((environment(X2)=>greater_or_equal(critical_point(X2),start_time(X2)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_time_of_critical_point)).
% 0.24/0.52 fof(mp3_favoured_trategy, axiom, ![X1]:(((((observational_period(X1)&propagation_strategy(first_movers))&propagation_strategy(efficient_producers))&![X2]:(((environment(X2)&in_environment(X1,X2))=>selection_favors(efficient_producers,first_movers,end_time(X2)))))=>selection_favors(efficient_producers,first_movers,X1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp3_favoured_trategy)).
% 0.24/0.52 fof(mp_organizational_sets1, axiom, propagation_strategy(first_movers), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_organizational_sets1)).
% 0.24/0.52 fof(mp_organizational_sets2, axiom, propagation_strategy(efficient_producers), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_organizational_sets2)).
% 0.24/0.52 fof(l8, hypothesis, ![X2, X3]:((((environment(X2)&in_environment(X2,X3))&greater(X3,critical_point(X2)))=>selection_favors(efficient_producers,first_movers,X3))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', l8)).
% 0.24/0.52 fof(prove_t8, conjecture, ![X1]:(((observational_period(X1)&slow_change(X1))=>selection_favors(efficient_producers,first_movers,X1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_t8)).
% 0.24/0.52 fof(c_0_11, plain, ![X12, X13, X14]:((~greater(X12,X13)|~greater(X13,X14)|greater(X12,X14))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_greater_transitivity])])])).
% 0.24/0.52 fof(c_0_12, plain, ![X17, X18]:(((in_environment(X18,esk3_2(X17,X18))|(~environment(X18)|~in_environment(X17,X18))|(~observational_period(X17)|~slow_change(X17)))&(greater(esk3_2(X17,X18),critical_point(X18))|(~environment(X18)|~in_environment(X17,X18))|(~observational_period(X17)|~slow_change(X17))))), 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)],[mp4_critical_point])])])])])])).
% 0.24/0.52 fof(c_0_13, plain, ![X15, X16]:(((~greater_or_equal(X15,X16)|(greater(X15,X16)|X15=X16))&((~greater(X15,X16)|greater_or_equal(X15,X16))&(X15!=X16|greater_or_equal(X15,X16))))), 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.52 fof(c_0_14, plain, ![X21, X22]:((~environment(X21)|~in_environment(X21,X22)|greater_or_equal(end_time(X21),X22))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_environment_end_point])])])).
% 0.24/0.52 cnf(c_0_15, plain, (greater(X1,X3)|~greater(X1,X2)|~greater(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.24/0.52 cnf(c_0_16, plain, (greater(esk3_2(X1,X2),critical_point(X2))|~environment(X2)|~in_environment(X1,X2)|~observational_period(X1)|~slow_change(X1)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.24/0.52 cnf(c_0_17, plain, (greater(X1,X2)|X1=X2|~greater_or_equal(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.24/0.52 cnf(c_0_18, plain, (greater_or_equal(end_time(X1),X2)|~environment(X1)|~in_environment(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.24/0.52 fof(c_0_19, plain, ![X23, X24]:((~environment(X23)|~greater_or_equal(X24,start_time(X23))|~greater_or_equal(end_time(X23),X24)|in_environment(X23,X24))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_time_in_environment])])])).
% 0.24/0.52 fof(c_0_20, plain, ![X20]:((~environment(X20)|greater_or_equal(critical_point(X20),start_time(X20)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp_time_of_critical_point])])])).
% 0.24/0.52 cnf(c_0_21, plain, (greater(X1,critical_point(X2))|~greater(X1,esk3_2(X3,X2))|~slow_change(X3)|~in_environment(X3,X2)|~environment(X2)|~observational_period(X3)), inference(spm,[status(thm)],[c_0_15, c_0_16])).
% 0.24/0.52 cnf(c_0_22, plain, (end_time(X1)=X2|greater(end_time(X1),X2)|~in_environment(X1,X2)|~environment(X1)), inference(spm,[status(thm)],[c_0_17, c_0_18])).
% 0.24/0.52 fof(c_0_23, plain, ![X10]:((((environment(esk2_1(X10))|(~observational_period(X10)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers))|selection_favors(efficient_producers,first_movers,X10))&(in_environment(X10,esk2_1(X10))|(~observational_period(X10)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers))|selection_favors(efficient_producers,first_movers,X10)))&(~selection_favors(efficient_producers,first_movers,end_time(esk2_1(X10)))|(~observational_period(X10)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers))|selection_favors(efficient_producers,first_movers,X10)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp3_favoured_trategy])])])])])).
% 0.24/0.52 cnf(c_0_24, plain, (in_environment(X1,X2)|~environment(X1)|~greater_or_equal(X2,start_time(X1))|~greater_or_equal(end_time(X1),X2)), inference(split_conjunct,[status(thm)],[c_0_19])).
% 0.24/0.52 cnf(c_0_25, plain, (greater_or_equal(X1,X2)|~greater(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.24/0.52 cnf(c_0_26, plain, (greater_or_equal(X1,X2)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.24/0.52 cnf(c_0_27, plain, (greater_or_equal(critical_point(X1),start_time(X1))|~environment(X1)), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.24/0.52 cnf(c_0_28, plain, (end_time(X1)=esk3_2(X2,X3)|greater(end_time(X1),critical_point(X3))|~slow_change(X2)|~in_environment(X1,esk3_2(X2,X3))|~in_environment(X2,X3)|~environment(X3)|~environment(X1)|~observational_period(X2)), inference(spm,[status(thm)],[c_0_21, c_0_22])).
% 0.24/0.52 cnf(c_0_29, plain, (in_environment(X1,esk3_2(X2,X1))|~environment(X1)|~in_environment(X2,X1)|~observational_period(X2)|~slow_change(X2)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.24/0.52 cnf(c_0_30, plain, (in_environment(X1,esk2_1(X1))|selection_favors(efficient_producers,first_movers,X1)|~observational_period(X1)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.24/0.52 cnf(c_0_31, plain, (propagation_strategy(first_movers)), inference(split_conjunct,[status(thm)],[mp_organizational_sets1])).
% 0.24/0.52 cnf(c_0_32, plain, (propagation_strategy(efficient_producers)), inference(split_conjunct,[status(thm)],[mp_organizational_sets2])).
% 0.24/0.52 cnf(c_0_33, plain, (environment(esk2_1(X1))|selection_favors(efficient_producers,first_movers,X1)|~observational_period(X1)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.24/0.52 cnf(c_0_34, plain, (in_environment(X1,X2)|~greater_or_equal(end_time(X1),X2)|~greater(X2,start_time(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_24, c_0_25])).
% 0.24/0.52 cnf(c_0_35, plain, (greater_or_equal(X1,X1)), inference(er,[status(thm)],[c_0_26])).
% 0.24/0.52 cnf(c_0_36, plain, (start_time(X1)=critical_point(X1)|greater(critical_point(X1),start_time(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_17, c_0_27])).
% 0.24/0.52 fof(c_0_37, hypothesis, ![X7, X8]:((~environment(X7)|~in_environment(X7,X8)|~greater(X8,critical_point(X7))|selection_favors(efficient_producers,first_movers,X8))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[l8])])])).
% 0.24/0.52 cnf(c_0_38, plain, (esk3_2(X1,X2)=end_time(X2)|greater(end_time(X2),critical_point(X2))|~slow_change(X1)|~in_environment(X1,X2)|~environment(X2)|~observational_period(X1)), inference(spm,[status(thm)],[c_0_28, c_0_29])).
% 0.24/0.52 cnf(c_0_39, plain, (selection_favors(efficient_producers,first_movers,X1)|in_environment(X1,esk2_1(X1))|~observational_period(X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31]), c_0_32])])).
% 0.24/0.52 cnf(c_0_40, plain, (selection_favors(efficient_producers,first_movers,X1)|environment(esk2_1(X1))|~observational_period(X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_31]), c_0_32])])).
% 0.24/0.52 cnf(c_0_41, plain, (selection_favors(efficient_producers,first_movers,X1)|~selection_favors(efficient_producers,first_movers,end_time(esk2_1(X1)))|~observational_period(X1)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.24/0.52 cnf(c_0_42, plain, (in_environment(X1,end_time(X1))|~greater(end_time(X1),start_time(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_34, c_0_35])).
% 0.24/0.52 cnf(c_0_43, plain, (start_time(X1)=critical_point(X1)|greater(X2,start_time(X1))|~greater(X2,critical_point(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_15, c_0_36])).
% 0.24/0.52 cnf(c_0_44, hypothesis, (selection_favors(efficient_producers,first_movers,X2)|~environment(X1)|~in_environment(X1,X2)|~greater(X2,critical_point(X1))), inference(split_conjunct,[status(thm)],[c_0_37])).
% 0.24/0.52 cnf(c_0_45, plain, (esk3_2(X1,esk2_1(X1))=end_time(esk2_1(X1))|greater(end_time(esk2_1(X1)),critical_point(esk2_1(X1)))|selection_favors(efficient_producers,first_movers,X1)|~slow_change(X1)|~observational_period(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_39]), c_0_40])).
% 0.24/0.52 cnf(c_0_46, plain, (selection_favors(efficient_producers,first_movers,X1)|~selection_favors(efficient_producers,first_movers,end_time(esk2_1(X1)))|~observational_period(X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_41, c_0_31]), c_0_32])])).
% 0.24/0.52 cnf(c_0_47, plain, (start_time(X1)=critical_point(X1)|in_environment(X1,end_time(X1))|~greater(end_time(X1),critical_point(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_42, c_0_43])).
% 0.24/0.52 cnf(c_0_48, hypothesis, (esk3_2(X1,esk2_1(X1))=end_time(esk2_1(X1))|selection_favors(efficient_producers,first_movers,X1)|~slow_change(X1)|~in_environment(esk2_1(X1),end_time(esk2_1(X1)))|~observational_period(X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_45]), c_0_40]), c_0_46])).
% 0.24/0.52 cnf(c_0_49, plain, (in_environment(X1,end_time(X2))|~greater_or_equal(end_time(X1),end_time(X2))|~in_environment(X2,start_time(X1))|~environment(X1)|~environment(X2)), inference(spm,[status(thm)],[c_0_24, c_0_18])).
% 0.24/0.52 cnf(c_0_50, hypothesis, (selection_favors(efficient_producers,first_movers,esk3_2(X1,X2))|~slow_change(X1)|~in_environment(X1,X2)|~environment(X2)|~observational_period(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_16]), c_0_29])).
% 0.24/0.52 cnf(c_0_51, plain, (esk3_2(X1,esk2_1(X1))=end_time(esk2_1(X1))|start_time(esk2_1(X1))=critical_point(esk2_1(X1))|selection_favors(efficient_producers,first_movers,X1)|~slow_change(X1)|~observational_period(X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_45]), c_0_40]), c_0_48])).
% 0.24/0.52 cnf(c_0_52, plain, (in_environment(X1,critical_point(X1))|~greater_or_equal(end_time(X1),critical_point(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_24, c_0_27])).
% 0.24/0.52 cnf(c_0_53, plain, (in_environment(X1,end_time(X1))|~in_environment(X1,start_time(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_49, c_0_35])).
% 0.24/0.52 cnf(c_0_54, hypothesis, (start_time(esk2_1(X1))=critical_point(esk2_1(X1))|selection_favors(efficient_producers,first_movers,X1)|~slow_change(X1)|~observational_period(X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_51]), c_0_40]), c_0_39]), c_0_46])).
% 0.24/0.52 cnf(c_0_55, plain, (in_environment(X1,critical_point(X1))|~greater(end_time(X1),critical_point(X1))|~environment(X1)), inference(spm,[status(thm)],[c_0_52, c_0_25])).
% 0.24/0.52 cnf(c_0_56, hypothesis, (selection_favors(efficient_producers,first_movers,X1)|in_environment(esk2_1(X1),end_time(esk2_1(X1)))|~slow_change(X1)|~in_environment(esk2_1(X1),critical_point(esk2_1(X1)))|~observational_period(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_53, c_0_54]), c_0_40])).
% 0.24/0.52 cnf(c_0_57, plain, (esk3_2(X1,esk2_1(X1))=end_time(esk2_1(X1))|selection_favors(efficient_producers,first_movers,X1)|in_environment(esk2_1(X1),critical_point(esk2_1(X1)))|~slow_change(X1)|~observational_period(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_55, c_0_45]), c_0_40])).
% 0.24/0.52 fof(c_0_58, negated_conjecture, ~(![X1]:(((observational_period(X1)&slow_change(X1))=>selection_favors(efficient_producers,first_movers,X1)))), inference(assume_negation,[status(cth)],[prove_t8])).
% 0.24/0.52 cnf(c_0_59, hypothesis, (esk3_2(X1,esk2_1(X1))=end_time(esk2_1(X1))|selection_favors(efficient_producers,first_movers,X1)|~slow_change(X1)|~observational_period(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_57]), c_0_48])).
% 0.24/0.52 fof(c_0_60, negated_conjecture, ((observational_period(esk1_0)&slow_change(esk1_0))&~selection_favors(efficient_producers,first_movers,esk1_0)), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_58])])])])).
% 0.24/0.52 cnf(c_0_61, hypothesis, (selection_favors(efficient_producers,first_movers,X1)|~slow_change(X1)|~observational_period(X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_59]), c_0_40]), c_0_39]), c_0_46])).
% 0.24/0.52 cnf(c_0_62, negated_conjecture, (slow_change(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_60])).
% 0.24/0.52 cnf(c_0_63, negated_conjecture, (observational_period(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_60])).
% 0.24/0.52 cnf(c_0_64, negated_conjecture, (~selection_favors(efficient_producers,first_movers,esk1_0)), inference(split_conjunct,[status(thm)],[c_0_60])).
% 0.24/0.52 cnf(c_0_65, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_62]), c_0_63])]), c_0_64]), ['proof']).
% 0.24/0.52 % SZS output end Proof
% 0.24/0.52 % User time : 0.013 s
% 0.24/0.52 % System time : 0.002 s
% 0.24/0.52 % Total time : 0.015 s
% 0.24/0.52 % User time : 0.015 s
% 0.24/0.52 % System time : 0.004 s
% 0.24/0.52 % Total time : 0.020 s
% 0.24/0.52
%------------------------------------------------------------------------------