%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT014+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n009.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.28s 0.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT014+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.34 % Computer : n009.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 11:52:52 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.14/0.46 start to proof:theBenchmark.p
% 0.28/0.54 % Version : CSI_E---1.1
% 0.28/0.54 % Problem : theBenchmark.p
% 0.28/0.54 % Proof found!
% 0.28/0.54 % SZS status Theorem for theBenchmark.p
% 0.28/0.54 % SZS output start Proof
% 0.28/0.54 fof(t11_FOL, hypothesis, ![X1, X6, X7, X4, X5]:(((((((organization(X1,X4)&organization(X1,X5))&reorganization_free(X1,X4,X5))&size(X1,X6,X4))&size(X1,X7,X5))&greater(X5,X4))=>~(greater(X6,X7)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t11_FOL)).
% 0.28/0.54 fof(t14_FOL, conjecture, ![X1, X8, X9, X6, X7, X4, X5]:(((((((((organization(X1,X4)&organization(X1,X5))&reorganization_free(X1,X4,X5))&complexity(X1,X8,X4))&complexity(X1,X9,X5))&size(X1,X6,X4))&size(X1,X7,X5))&greater(X7,X6))=>~(greater(X8,X9)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t14_FOL)).
% 0.28/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.28/0.54 fof(mp15, axiom, ![X1, X3]:((organization(X1,X3)=>time(X3))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp15)).
% 0.28/0.54 fof(t12_FOL, hypothesis, ![X1, X8, X9, X4, X5]:(((((((organization(X1,X4)&organization(X1,X5))&reorganization_free(X1,X4,X5))&complexity(X1,X8,X4))&complexity(X1,X9,X5))&greater(X5,X4))=>~(greater(X8,X9)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t12_FOL)).
% 0.28/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.28/0.54 fof(mp19, axiom, ![X1, X6, X7, X4, X5]:((((((organization(X1,X4)&organization(X1,X5))&size(X1,X6,X4))&size(X1,X7,X5))&X4=X5)=>X6=X7)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp19)).
% 0.28/0.54 fof(mp6_1, axiom, ![X1, X2]:(~((greater(X1,X2)&X1=X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp6_1)).
% 0.28/0.54 fof(c_0_8, hypothesis, ![X1, X6, X7, X4, X5]:(((((((organization(X1,X4)&organization(X1,X5))&reorganization_free(X1,X4,X5))&size(X1,X6,X4))&size(X1,X7,X5))&greater(X5,X4))=>~greater(X6,X7))), inference(fof_simplification,[status(thm)],[t11_FOL])).
% 0.28/0.54 fof(c_0_9, negated_conjecture, ~(![X1, X8, X9, X6, X7, X4, X5]:(((((((((organization(X1,X4)&organization(X1,X5))&reorganization_free(X1,X4,X5))&complexity(X1,X8,X4))&complexity(X1,X9,X5))&size(X1,X6,X4))&size(X1,X7,X5))&greater(X7,X6))=>~greater(X8,X9)))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[t14_FOL])])).
% 0.28/0.54 fof(c_0_10, hypothesis, ![X23, X24, X25, X26, X27]:((~organization(X23,X26)|~organization(X23,X27)|~reorganization_free(X23,X26,X27)|~size(X23,X24,X26)|~size(X23,X25,X27)|~greater(X27,X26)|~greater(X24,X25))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_8])])])).
% 0.28/0.54 fof(c_0_11, 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(esk5_0,esk4_0))&greater(esk2_0,esk3_0)), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_9])])])).
% 0.28/0.54 fof(c_0_12, plain, ![X38, X39, X40]:((~reorganization_free(X38,X39,X40)|reorganization_free(X38,X40,X39))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp17])])])).
% 0.28/0.54 fof(c_0_13, plain, ![X41, X42]:((~organization(X41,X42)|time(X42))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp15])])])).
% 0.28/0.54 cnf(c_0_14, 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_10])).
% 0.28/0.54 cnf(c_0_15, negated_conjecture, (size(esk1_0,esk4_0,esk6_0)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.28/0.54 cnf(c_0_16, negated_conjecture, (organization(esk1_0,esk6_0)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.28/0.54 cnf(c_0_17, plain, (reorganization_free(X1,X3,X2)|~reorganization_free(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.28/0.54 cnf(c_0_18, negated_conjecture, (reorganization_free(esk1_0,esk6_0,esk7_0)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.28/0.54 fof(c_0_19, hypothesis, ![X1, X8, X9, X4, X5]:(((((((organization(X1,X4)&organization(X1,X5))&reorganization_free(X1,X4,X5))&complexity(X1,X8,X4))&complexity(X1,X9,X5))&greater(X5,X4))=>~greater(X8,X9))), inference(fof_simplification,[status(thm)],[t12_FOL])).
% 0.28/0.54 fof(c_0_20, plain, ![X21, X22]:((~time(X21)|~time(X22)|(greater(X21,X22)|X21=X22|greater(X22,X21)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp16])])])).
% 0.28/0.54 cnf(c_0_21, plain, (time(X2)|~organization(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.28/0.54 cnf(c_0_22, negated_conjecture, (organization(esk1_0,esk7_0)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.28/0.54 cnf(c_0_23, negated_conjecture, (~size(esk1_0,X1,X2)|~reorganization_free(esk1_0,X2,esk6_0)|~organization(esk1_0,X2)|~greater(X1,esk4_0)|~greater(esk6_0,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_14, c_0_15]), c_0_16])])).
% 0.28/0.54 cnf(c_0_24, negated_conjecture, (reorganization_free(esk1_0,esk7_0,esk6_0)), inference(spm,[status(thm)],[c_0_17, c_0_18])).
% 0.28/0.54 fof(c_0_25, hypothesis, ![X28, X29, X30, X31, X32]:((~organization(X28,X31)|~organization(X28,X32)|~reorganization_free(X28,X31,X32)|~complexity(X28,X29,X31)|~complexity(X28,X30,X32)|~greater(X32,X31)|~greater(X29,X30))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_19])])])).
% 0.28/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_20])).
% 0.28/0.54 cnf(c_0_27, negated_conjecture, (time(esk7_0)), inference(spm,[status(thm)],[c_0_21, c_0_22])).
% 0.28/0.54 cnf(c_0_28, negated_conjecture, (~size(esk1_0,X1,esk7_0)|~greater(esk6_0,esk7_0)|~greater(X1,esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_24]), c_0_22])])).
% 0.28/0.54 cnf(c_0_29, negated_conjecture, (size(esk1_0,esk5_0,esk7_0)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.28/0.54 cnf(c_0_30, negated_conjecture, (greater(esk5_0,esk4_0)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.28/0.54 cnf(c_0_31, 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_25])).
% 0.28/0.54 cnf(c_0_32, negated_conjecture, (complexity(esk1_0,esk3_0,esk7_0)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.28/0.54 fof(c_0_33, plain, ![X33, X34, X35, X36, X37]:((~organization(X33,X36)|~organization(X33,X37)|~size(X33,X34,X36)|~size(X33,X35,X37)|X36!=X37|X34=X35)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp19])])])).
% 0.28/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.28/0.54 cnf(c_0_35, negated_conjecture, (time(esk6_0)), inference(spm,[status(thm)],[c_0_21, c_0_16])).
% 0.28/0.54 cnf(c_0_36, negated_conjecture, (~greater(esk6_0,esk7_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_29]), c_0_30])])).
% 0.28/0.54 cnf(c_0_37, negated_conjecture, (~complexity(esk1_0,X1,X2)|~reorganization_free(esk1_0,X2,esk7_0)|~organization(esk1_0,X2)|~greater(X1,esk3_0)|~greater(esk7_0,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_32]), c_0_22])])).
% 0.28/0.54 cnf(c_0_38, negated_conjecture, (complexity(esk1_0,esk2_0,esk6_0)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.28/0.54 cnf(c_0_39, negated_conjecture, (greater(esk2_0,esk3_0)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.28/0.54 cnf(c_0_40, plain, (X4=X5|~organization(X1,X2)|~organization(X1,X3)|~size(X1,X4,X2)|~size(X1,X5,X3)|X2!=X3), inference(split_conjunct,[status(thm)],[c_0_33])).
% 0.28/0.54 cnf(c_0_41, negated_conjecture, (esk7_0=esk6_0|greater(esk7_0,esk6_0)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_35]), c_0_36])).
% 0.28/0.54 cnf(c_0_42, 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_37, c_0_38]), c_0_18]), c_0_16]), c_0_39])])).
% 0.28/0.54 cnf(c_0_43, plain, (X1=X2|~size(X3,X2,X4)|~size(X3,X1,X4)|~organization(X3,X4)), inference(er,[status(thm)],[c_0_40])).
% 0.28/0.54 cnf(c_0_44, negated_conjecture, (esk7_0=esk6_0), inference(sr,[status(thm)],[c_0_41, c_0_42])).
% 0.28/0.54 fof(c_0_45, plain, ![X17, X18]:((~greater(X17,X18)|X17!=X18)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp6_1])])])).
% 0.28/0.54 cnf(c_0_46, negated_conjecture, (X1=esk4_0|~size(esk1_0,X1,esk6_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_15]), c_0_16])])).
% 0.28/0.54 cnf(c_0_47, negated_conjecture, (size(esk1_0,esk5_0,esk6_0)), inference(rw,[status(thm)],[c_0_29, c_0_44])).
% 0.28/0.54 cnf(c_0_48, plain, (~greater(X1,X2)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_45])).
% 0.28/0.54 cnf(c_0_49, negated_conjecture, (esk4_0=esk5_0), inference(spm,[status(thm)],[c_0_46, c_0_47])).
% 0.28/0.54 cnf(c_0_50, plain, (~greater(X1,X1)), inference(er,[status(thm)],[c_0_48])).
% 0.28/0.54 cnf(c_0_51, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_49]), c_0_50]), ['proof']).
% 0.28/0.54 % SZS output end Proof
% 0.28/0.54 % User time : 0.007 s
% 0.28/0.54 % System time : 0.002 s
% 0.28/0.54 % Total time : 0.009 s
% 0.28/0.54 % User time : 0.009 s
% 0.28/0.54 % System time : 0.005 s
% 0.28/0.54 % Total time : 0.014 s
% 0.28/0.54
%------------------------------------------------------------------------------