%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT013+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n018.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:28 AM UTC 2026
% Result : Theorem 0.26s 0.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT013+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.09/0.35 % Computer : n018.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 7 11:53:22 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.47 start to proof:theBenchmark.p
% 0.26/0.54 % Version : CSI_E---1.1
% 0.26/0.54 % Problem : theBenchmark.p
% 0.26/0.54 % Proof found!
% 0.26/0.54 % SZS status Theorem for theBenchmark.p
% 0.26/0.54 % SZS output start Proof
% 0.26/0.54 fof(t13_FOL, conjecture, ![X1, X6, X7, X8, X9, X4, X5]:(((((((((organization(X1,X4)&organization(X1,X5))&reorganization_free(X1,X4,X5))&complexity(X1,X6,X4))&complexity(X1,X7,X5))&size(X1,X8,X4))&size(X1,X9,X5))&greater(X7,X6))=>~(greater(X8,X9)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t13_FOL)).
% 0.26/0.54 fof(t11_FOL, hypothesis, ![X1, X8, X9, X4, X5]:(((((((organization(X1,X4)&organization(X1,X5))&reorganization_free(X1,X4,X5))&size(X1,X8,X4))&size(X1,X9,X5))&greater(X5,X4))=>~(greater(X8,X9)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t11_FOL)).
% 0.26/0.54 fof(t12_FOL, hypothesis, ![X1, X6, X7, X4, X5]:(((((((organization(X1,X4)&organization(X1,X5))&reorganization_free(X1,X4,X5))&complexity(X1,X6,X4))&complexity(X1,X7,X5))&greater(X5,X4))=>~(greater(X6,X7)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t12_FOL)).
% 0.26/0.54 fof(mp15, axiom, ![X1, X3]:((organization(X1,X3)=>time(X3))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp15)).
% 0.26/0.54 fof(mp17, axiom, ![X1, X4, X5]:((reorganization_free(X1,X4,X5)=>reorganization_free(X1,X5,X4))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp17)).
% 0.26/0.54 fof(mp16, axiom, ![X4, X5]:(((time(X4)&time(X5))=>(greater(X4,X5)|X4=X5|greater(X5,X4)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp16)).
% 0.26/0.54 fof(mp18, axiom, ![X1, X6, X7, X4, X5]:((((((organization(X1,X4)&organization(X1,X5))&complexity(X1,X6,X4))&complexity(X1,X7,X5))&X4=X5)=>X6=X7)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp18)).
% 0.26/0.54 fof(mp6_1, axiom, ![X1, X2]:(~((greater(X1,X2)&X1=X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp6_1)).
% 0.26/0.54 fof(c_0_8, negated_conjecture, ~(![X1, X6, X7, X8, X9, X4, X5]:(((((((((organization(X1,X4)&organization(X1,X5))&reorganization_free(X1,X4,X5))&complexity(X1,X6,X4))&complexity(X1,X7,X5))&size(X1,X8,X4))&size(X1,X9,X5))&greater(X7,X6))=>~greater(X8,X9)))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[t13_FOL])])).
% 0.26/0.54 fof(c_0_9, hypothesis, ![X1, X8, X9, X4, X5]:(((((((organization(X1,X4)&organization(X1,X5))&reorganization_free(X1,X4,X5))&size(X1,X8,X4))&size(X1,X9,X5))&greater(X5,X4))=>~greater(X8,X9))), inference(fof_simplification,[status(thm)],[t11_FOL])).
% 0.26/0.54 fof(c_0_10, hypothesis, ![X1, X6, X7, X4, X5]:(((((((organization(X1,X4)&organization(X1,X5))&reorganization_free(X1,X4,X5))&complexity(X1,X6,X4))&complexity(X1,X7,X5))&greater(X5,X4))=>~greater(X6,X7))), inference(fof_simplification,[status(thm)],[t12_FOL])).
% 0.26/0.54 fof(c_0_11, plain, ![X14, X15]:((~organization(X14,X15)|time(X15))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp15])])])).
% 0.26/0.54 fof(c_0_12, negated_conjecture, ((((((((organization(esk1_0,esk6_0)&organization(esk1_0,esk7_0))&reorganization_free(esk1_0,esk6_0,esk7_0))&complexity(esk1_0,esk2_0,esk6_0))&complexity(esk1_0,esk3_0,esk7_0))&size(esk1_0,esk4_0,esk6_0))&size(esk1_0,esk5_0,esk7_0))&greater(esk3_0,esk2_0))&greater(esk4_0,esk5_0)), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_8])])])).
% 0.26/0.54 fof(c_0_13, hypothesis, ![X26, X27, X28, X29, X30]:((~organization(X26,X29)|~organization(X26,X30)|~reorganization_free(X26,X29,X30)|~size(X26,X27,X29)|~size(X26,X28,X30)|~greater(X30,X29)|~greater(X27,X28))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_9])])])).
% 0.26/0.54 fof(c_0_14, hypothesis, ![X31, X32, X33, X34, X35]:((~organization(X31,X34)|~organization(X31,X35)|~reorganization_free(X31,X34,X35)|~complexity(X31,X32,X34)|~complexity(X31,X33,X35)|~greater(X35,X34)|~greater(X32,X33))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_10])])])).
% 0.26/0.54 fof(c_0_15, plain, ![X18, X19, X20]:((~reorganization_free(X18,X19,X20)|reorganization_free(X18,X20,X19))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp17])])])).
% 0.26/0.54 fof(c_0_16, plain, ![X16, X17]:((~time(X16)|~time(X17)|(greater(X16,X17)|X16=X17|greater(X17,X16)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp16])])])).
% 0.26/0.54 cnf(c_0_17, plain, (time(X2)|~organization(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.26/0.54 cnf(c_0_18, negated_conjecture, (organization(esk1_0,esk7_0)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.26/0.54 cnf(c_0_19, hypothesis, (~organization(X1,X2)|~organization(X1,X3)|~reorganization_free(X1,X2,X3)|~size(X1,X4,X2)|~size(X1,X5,X3)|~greater(X3,X2)|~greater(X4,X5)), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.26/0.54 cnf(c_0_20, negated_conjecture, (size(esk1_0,esk5_0,esk7_0)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.26/0.54 cnf(c_0_21, hypothesis, (~organization(X1,X2)|~organization(X1,X3)|~reorganization_free(X1,X2,X3)|~complexity(X1,X4,X2)|~complexity(X1,X5,X3)|~greater(X3,X2)|~greater(X4,X5)), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.26/0.54 cnf(c_0_22, negated_conjecture, (complexity(esk1_0,esk2_0,esk6_0)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.26/0.54 cnf(c_0_23, negated_conjecture, (organization(esk1_0,esk6_0)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.26/0.54 cnf(c_0_24, plain, (reorganization_free(X1,X3,X2)|~reorganization_free(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.26/0.54 cnf(c_0_25, negated_conjecture, (reorganization_free(esk1_0,esk6_0,esk7_0)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.26/0.54 cnf(c_0_26, plain, (greater(X1,X2)|X1=X2|greater(X2,X1)|~time(X1)|~time(X2)), inference(split_conjunct,[status(thm)],[c_0_16])).
% 0.26/0.54 cnf(c_0_27, negated_conjecture, (time(esk7_0)), inference(spm,[status(thm)],[c_0_17, c_0_18])).
% 0.26/0.54 cnf(c_0_28, negated_conjecture, (~size(esk1_0,X1,X2)|~reorganization_free(esk1_0,X2,esk7_0)|~organization(esk1_0,X2)|~greater(X1,esk5_0)|~greater(esk7_0,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_19, c_0_20]), c_0_18])])).
% 0.26/0.54 cnf(c_0_29, negated_conjecture, (size(esk1_0,esk4_0,esk6_0)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.26/0.54 cnf(c_0_30, negated_conjecture, (greater(esk4_0,esk5_0)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.26/0.54 cnf(c_0_31, negated_conjecture, (~complexity(esk1_0,X1,X2)|~reorganization_free(esk1_0,X2,esk6_0)|~organization(esk1_0,X2)|~greater(X1,esk2_0)|~greater(esk6_0,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_21, c_0_22]), c_0_23])])).
% 0.26/0.54 cnf(c_0_32, negated_conjecture, (reorganization_free(esk1_0,esk7_0,esk6_0)), inference(spm,[status(thm)],[c_0_24, c_0_25])).
% 0.26/0.54 fof(c_0_33, plain, ![X21, X22, X23, X24, X25]:((~organization(X21,X24)|~organization(X21,X25)|~complexity(X21,X22,X24)|~complexity(X21,X23,X25)|X24!=X25|X22=X23)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp18])])])).
% 0.26/0.54 cnf(c_0_34, negated_conjecture, (X1=esk7_0|greater(X1,esk7_0)|greater(esk7_0,X1)|~time(X1)), inference(spm,[status(thm)],[c_0_26, c_0_27])).
% 0.26/0.54 cnf(c_0_35, negated_conjecture, (time(esk6_0)), inference(spm,[status(thm)],[c_0_17, c_0_23])).
% 0.26/0.54 cnf(c_0_36, negated_conjecture, (~greater(esk7_0,esk6_0)), 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_29]), c_0_25]), c_0_23]), c_0_30])])).
% 0.26/0.54 cnf(c_0_37, negated_conjecture, (~complexity(esk1_0,X1,esk7_0)|~greater(esk6_0,esk7_0)|~greater(X1,esk2_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_32]), c_0_18])])).
% 0.26/0.54 cnf(c_0_38, negated_conjecture, (complexity(esk1_0,esk3_0,esk7_0)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.26/0.54 cnf(c_0_39, negated_conjecture, (greater(esk3_0,esk2_0)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.26/0.54 cnf(c_0_40, plain, (X4=X5|~organization(X1,X2)|~organization(X1,X3)|~complexity(X1,X4,X2)|~complexity(X1,X5,X3)|X2!=X3), inference(split_conjunct,[status(thm)],[c_0_33])).
% 0.26/0.54 cnf(c_0_41, negated_conjecture, (esk7_0=esk6_0|greater(esk6_0,esk7_0)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_35]), c_0_36])).
% 0.26/0.54 cnf(c_0_42, negated_conjecture, (~greater(esk6_0,esk7_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_38]), c_0_39])])).
% 0.26/0.54 cnf(c_0_43, plain, (X1=X2|~complexity(X3,X2,X4)|~complexity(X3,X1,X4)|~organization(X3,X4)), inference(er,[status(thm)],[c_0_40])).
% 0.26/0.54 cnf(c_0_44, negated_conjecture, (esk7_0=esk6_0), inference(sr,[status(thm)],[c_0_41, c_0_42])).
% 0.26/0.54 fof(c_0_45, plain, ![X10, X11]:((~greater(X10,X11)|X10!=X11)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp6_1])])])).
% 0.26/0.54 cnf(c_0_46, negated_conjecture, (X1=esk2_0|~complexity(esk1_0,X1,esk6_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_22]), c_0_23])])).
% 0.26/0.54 cnf(c_0_47, negated_conjecture, (complexity(esk1_0,esk3_0,esk6_0)), inference(rw,[status(thm)],[c_0_38, c_0_44])).
% 0.26/0.54 cnf(c_0_48, plain, (~greater(X1,X2)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_45])).
% 0.26/0.54 cnf(c_0_49, negated_conjecture, (esk3_0=esk2_0), inference(spm,[status(thm)],[c_0_46, c_0_47])).
% 0.26/0.54 cnf(c_0_50, plain, (~greater(X1,X1)), inference(er,[status(thm)],[c_0_48])).
% 0.26/0.54 cnf(c_0_51, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_39, c_0_49]), c_0_50]), ['proof']).
% 0.26/0.54 % SZS output end Proof
% 0.26/0.54 % User time : 0.007 s
% 0.26/0.54 % System time : 0.001 s
% 0.26/0.54 % Total time : 0.009 s
% 0.26/0.54 % User time : 0.017 s
% 0.26/0.54 % System time : 0.007 s
% 0.26/0.54 % Total time : 0.024 s
% 0.26/0.54
%------------------------------------------------------------------------------