%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT058+1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n012.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:35 AM UTC 2026
% Result : Theorem 0.08s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : MGT058+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.01 % Command : java -jar mcs_scs.jar %d %s
% 0.04/0.29 % Computer : n012.cluster.edu
% 0.04/0.29 % Model : x86_64 x86_64
% 0.04/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.29 % Memory : 8046.5625MB
% 0.04/0.29 % OS : Linux 6.8.0-71-generic
% 0.04/0.29 % CPULimit : 300
% 0.04/0.29 % WCLimit : 300
% 0.04/0.29 % DateTime : Mon Sep 7 13:31:41 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.08/0.36 start to proof:theBenchmark.p
% 0.08/0.40 % Version : CSI_E---1.1
% 0.08/0.40 % Problem : theBenchmark.p
% 0.08/0.40 % Proof found!
% 0.08/0.40 % SZS status Theorem for theBenchmark.p
% 0.08/0.40 % SZS output start Proof
% 0.08/0.40 fof(lemma_10, conjecture, ![X1]:(((((organization(X1)&?[X5]:(age(X1,X5)=zero))&greater_or_equal(sigma,zero))&greater_or_equal(tau,zero))=>~((fragile_position(X1)&robust_position(X1))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', lemma_10)).
% 0.08/0.40 fof(definition_greater_or_equal, axiom, ![X1, X2]:((greater_or_equal(X1,X2)<=>(greater(X1,X2)|X1=X2))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax', definition_greater_or_equal)).
% 0.08/0.40 fof(definition_3, axiom, ![X1]:((fragile_position(X1)<=>![X4]:(((smaller_or_equal(age(X1,X4),sigma)=>positional_advantage(X1,X4))&(greater(age(X1,X4),sigma)=>~(positional_advantage(X1,X4))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', definition_3)).
% 0.08/0.40 fof(definition_smaller, axiom, ![X1, X2]:((smaller(X1,X2)<=>greater(X2,X1))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax', definition_smaller)).
% 0.08/0.40 fof(definition_smaller_or_equal, axiom, ![X1, X2]:((smaller_or_equal(X1,X2)<=>(smaller(X1,X2)|X1=X2))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax', definition_smaller_or_equal)).
% 0.08/0.40 fof(definition_4, axiom, ![X1]:((robust_position(X1)<=>![X4]:(((smaller_or_equal(age(X1,X4),tau)=>~(positional_advantage(X1,X4)))&(greater(age(X1,X4),tau)=>positional_advantage(X1,X4)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', definition_4)).
% 0.08/0.40 fof(c_0_6, negated_conjecture, ~(![X1]:(((((organization(X1)&?[X5]:(age(X1,X5)=zero))&greater_or_equal(sigma,zero))&greater_or_equal(tau,zero))=>~((fragile_position(X1)&robust_position(X1)))))), inference(assume_negation,[status(cth)],[lemma_10])).
% 0.08/0.40 fof(c_0_7, plain, ![X20, X21]:(((~greater_or_equal(X20,X21)|(greater(X20,X21)|X20=X21))&((~greater(X20,X21)|greater_or_equal(X20,X21))&(X20!=X21|greater_or_equal(X20,X21))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[definition_greater_or_equal])])])])).
% 0.08/0.40 fof(c_0_8, negated_conjecture, ((((organization(esk1_0)&age(esk1_0,esk2_0)=zero)&greater_or_equal(sigma,zero))&greater_or_equal(tau,zero))&(fragile_position(esk1_0)&robust_position(esk1_0))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_6])])])).
% 0.08/0.40 fof(c_0_9, plain, ![X1]:((fragile_position(X1)<=>![X4]:(((smaller_or_equal(age(X1,X4),sigma)=>positional_advantage(X1,X4))&(greater(age(X1,X4),sigma)=>~positional_advantage(X1,X4)))))), inference(fof_simplification,[status(thm)],[definition_3])).
% 0.08/0.40 fof(c_0_10, plain, ![X29, X30]:(((~smaller(X29,X30)|greater(X30,X29))&(~greater(X30,X29)|smaller(X29,X30)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[definition_smaller])])])).
% 0.08/0.40 cnf(c_0_11, plain, (greater(X1,X2)|X1=X2|~greater_or_equal(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.08/0.40 cnf(c_0_12, negated_conjecture, (greater_or_equal(sigma,zero)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.08/0.40 fof(c_0_13, plain, ![X14, X15, X16, X17]:((((~smaller_or_equal(age(X14,X15),sigma)|positional_advantage(X14,X15)|~fragile_position(X14))&(~greater(age(X14,X16),sigma)|~positional_advantage(X14,X16)|~fragile_position(X14)))&(((greater(age(X17,esk6_1(X17)),sigma)|smaller_or_equal(age(X17,esk5_1(X17)),sigma)|fragile_position(X17))&(positional_advantage(X17,esk6_1(X17))|smaller_or_equal(age(X17,esk5_1(X17)),sigma)|fragile_position(X17)))&((greater(age(X17,esk6_1(X17)),sigma)|~positional_advantage(X17,esk5_1(X17))|fragile_position(X17))&(positional_advantage(X17,esk6_1(X17))|~positional_advantage(X17,esk5_1(X17))|fragile_position(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(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_9])])])])])])])).
% 0.08/0.40 fof(c_0_14, plain, ![X27, X28]:(((~smaller_or_equal(X27,X28)|(smaller(X27,X28)|X27=X28))&((~smaller(X27,X28)|smaller_or_equal(X27,X28))&(X27!=X28|smaller_or_equal(X27,X28))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[definition_smaller_or_equal])])])])).
% 0.08/0.40 cnf(c_0_15, plain, (smaller(X2,X1)|~greater(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_10])).
% 0.08/0.40 cnf(c_0_16, negated_conjecture, (zero=sigma|greater(sigma,zero)), inference(spm,[status(thm)],[c_0_11, c_0_12])).
% 0.08/0.40 fof(c_0_17, plain, ![X1]:((robust_position(X1)<=>![X4]:(((smaller_or_equal(age(X1,X4),tau)=>~positional_advantage(X1,X4))&(greater(age(X1,X4),tau)=>positional_advantage(X1,X4)))))), inference(fof_simplification,[status(thm)],[definition_4])).
% 0.08/0.40 cnf(c_0_18, plain, (positional_advantage(X1,X2)|~smaller_or_equal(age(X1,X2),sigma)|~fragile_position(X1)), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.08/0.40 cnf(c_0_19, negated_conjecture, (age(esk1_0,esk2_0)=zero), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.08/0.40 cnf(c_0_20, negated_conjecture, (fragile_position(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.08/0.40 cnf(c_0_21, plain, (smaller_or_equal(X1,X2)|~smaller(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.08/0.40 cnf(c_0_22, negated_conjecture, (zero=sigma|smaller(zero,sigma)), inference(spm,[status(thm)],[c_0_15, c_0_16])).
% 0.08/0.40 cnf(c_0_23, negated_conjecture, (greater_or_equal(tau,zero)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.08/0.40 fof(c_0_24, plain, ![X8, X9, X10, X11]:((((~smaller_or_equal(age(X8,X9),tau)|~positional_advantage(X8,X9)|~robust_position(X8))&(~greater(age(X8,X10),tau)|positional_advantage(X8,X10)|~robust_position(X8)))&(((greater(age(X11,esk4_1(X11)),tau)|smaller_or_equal(age(X11,esk3_1(X11)),tau)|robust_position(X11))&(~positional_advantage(X11,esk4_1(X11))|smaller_or_equal(age(X11,esk3_1(X11)),tau)|robust_position(X11)))&((greater(age(X11,esk4_1(X11)),tau)|positional_advantage(X11,esk3_1(X11))|robust_position(X11))&(~positional_advantage(X11,esk4_1(X11))|positional_advantage(X11,esk3_1(X11))|robust_position(X11)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_17])])])])])])])).
% 0.08/0.40 cnf(c_0_25, negated_conjecture, (positional_advantage(esk1_0,esk2_0)|~smaller_or_equal(zero,sigma)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_18, c_0_19]), c_0_20])])).
% 0.08/0.40 cnf(c_0_26, negated_conjecture, (zero=sigma|smaller_or_equal(zero,sigma)), inference(spm,[status(thm)],[c_0_21, c_0_22])).
% 0.08/0.40 cnf(c_0_27, negated_conjecture, (zero=tau|greater(tau,zero)), inference(spm,[status(thm)],[c_0_11, c_0_23])).
% 0.08/0.40 cnf(c_0_28, plain, (~smaller_or_equal(age(X1,X2),tau)|~positional_advantage(X1,X2)|~robust_position(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 0.08/0.40 cnf(c_0_29, negated_conjecture, (zero=sigma|positional_advantage(esk1_0,esk2_0)), inference(spm,[status(thm)],[c_0_25, c_0_26])).
% 0.08/0.40 cnf(c_0_30, negated_conjecture, (robust_position(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.08/0.40 cnf(c_0_31, negated_conjecture, (zero=tau|smaller(zero,tau)), inference(spm,[status(thm)],[c_0_15, c_0_27])).
% 0.08/0.40 cnf(c_0_32, negated_conjecture, (zero=sigma|~smaller_or_equal(zero,tau)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_29]), c_0_30]), c_0_19])])).
% 0.08/0.40 cnf(c_0_33, negated_conjecture, (zero=tau|smaller_or_equal(zero,tau)), inference(spm,[status(thm)],[c_0_21, c_0_31])).
% 0.08/0.40 cnf(c_0_34, plain, (smaller_or_equal(X1,X2)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.08/0.40 cnf(c_0_35, negated_conjecture, (zero=tau|zero=sigma), inference(spm,[status(thm)],[c_0_32, c_0_33])).
% 0.08/0.40 cnf(c_0_36, plain, (smaller_or_equal(X1,X1)), inference(er,[status(thm)],[c_0_34])).
% 0.08/0.40 cnf(c_0_37, negated_conjecture, (zero=sigma|tau!=sigma), inference(ef,[status(thm)],[c_0_35])).
% 0.08/0.40 cnf(c_0_38, negated_conjecture, (zero=sigma), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_35]), c_0_36])]), c_0_37])).
% 0.08/0.40 cnf(c_0_39, negated_conjecture, (positional_advantage(esk1_0,esk2_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_25, c_0_38]), c_0_36])])).
% 0.08/0.40 cnf(c_0_40, negated_conjecture, (~smaller_or_equal(sigma,tau)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_39]), c_0_30]), c_0_19]), c_0_38])])).
% 0.08/0.40 cnf(c_0_41, negated_conjecture, (tau=sigma), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_38]), c_0_38]), c_0_40])).
% 0.08/0.40 cnf(c_0_42, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_40, c_0_41]), c_0_36])]), ['proof']).
% 0.08/0.40 % SZS output end Proof
% 0.08/0.40 % User time : 0.006 s
% 0.08/0.40 % System time : 0.000 s
% 0.08/0.40 % Total time : 0.006 s
% 0.08/0.40 % User time : 0.006 s
% 0.08/0.40 % System time : 0.003 s
% 0.08/0.40 % Total time : 0.009 s
% 0.08/0.40
%------------------------------------------------------------------------------