%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT007+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n011.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:27 AM UTC 2026
% Result : Theorem 0.27s 0.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT007+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.07/0.33 % Computer : n011.cluster.edu
% 0.07/0.33 % Model : x86_64 x86_64
% 0.07/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.33 % Memory : 8046.5625MB
% 0.07/0.33 % OS : Linux 6.8.0-71-generic
% 0.07/0.33 % CPULimit : 300
% 0.07/0.33 % WCLimit : 300
% 0.07/0.33 % DateTime : Mon Sep 7 11:43:30 UTC 2026
% 0.07/0.33 % CPUTime :
% 0.13/0.45 start to proof:theBenchmark.p
% 0.27/0.52 % Version : CSI_E---1.1
% 0.27/0.52 % Problem : theBenchmark.p
% 0.27/0.52 % Proof found!
% 0.27/0.52 % SZS status Theorem for theBenchmark.p
% 0.27/0.52 % SZS output start Proof
% 0.27/0.52 fof(a6_FOL, hypothesis, ![X1, X8, X9, X10, X11, X6, X7, X14, X15]:(((((((((((organization(X1,X6)&organization(X1,X7))&reorganization(X1,X14,X15))&reliability(X1,X8,X6))&reliability(X1,X9,X7))&accountability(X1,X10,X6))&accountability(X1,X11,X7))&~(greater(X14,X6)))&greater(X7,X6))&~(greater(X7,X15)))=>(greater(X8,X9)&greater(X10,X11)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a6_FOL)).
% 0.27/0.52 fof(t7_FOL, conjecture, ![X1, X12, X13, X6, X7, X14, X15]:(((((((((organization(X1,X6)&organization(X1,X7))&reorganization(X1,X14,X15))&reproducibility(X1,X12,X6))&reproducibility(X1,X13,X7))&~(greater(X14,X6)))&greater(X7,X6))&~(greater(X7,X15)))=>greater(X12,X13))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t7_FOL)).
% 0.27/0.52 fof(mp2, axiom, ![X1, X2]:((organization(X1,X2)=>?[X4]:(accountability(X1,X4,X2)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp2)).
% 0.27/0.52 fof(a2_FOL, hypothesis, ![X1, X5, X6, X7, X8, X9, X10, X11, X12, X13]:(((((((((organization(X1,X6)&organization(X5,X7))&reliability(X1,X8,X6))&reliability(X5,X9,X7))&accountability(X1,X10,X6))&accountability(X5,X11,X7))&reproducibility(X1,X12,X6))&reproducibility(X5,X13,X7))=>(greater(X13,X12)<=>(greater(X9,X8)&greater(X11,X10))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a2_FOL)).
% 0.27/0.52 fof(mp1, axiom, ![X1, X2]:((organization(X1,X2)=>?[X3]:(reliability(X1,X3,X2)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp1)).
% 0.27/0.52 fof(c_0_5, hypothesis, ![X1, X8, X9, X10, X11, X6, X7, X14, X15]:(((((((((((organization(X1,X6)&organization(X1,X7))&reorganization(X1,X14,X15))&reliability(X1,X8,X6))&reliability(X1,X9,X7))&accountability(X1,X10,X6))&accountability(X1,X11,X7))&~greater(X14,X6))&greater(X7,X6))&~greater(X7,X15))=>(greater(X8,X9)&greater(X10,X11)))), inference(fof_simplification,[status(thm)],[a6_FOL])).
% 0.27/0.52 fof(c_0_6, negated_conjecture, ~(![X1, X12, X13, X6, X7, X14, X15]:(((((((((organization(X1,X6)&organization(X1,X7))&reorganization(X1,X14,X15))&reproducibility(X1,X12,X6))&reproducibility(X1,X13,X7))&~greater(X14,X6))&greater(X7,X6))&~greater(X7,X15))=>greater(X12,X13)))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[t7_FOL])])).
% 0.27/0.52 fof(c_0_7, hypothesis, ![X35, X36, X37, X38, X39, X40, X41, X42, X43]:(((greater(X36,X37)|(~organization(X35,X40)|~organization(X35,X41)|~reorganization(X35,X42,X43)|~reliability(X35,X36,X40)|~reliability(X35,X37,X41)|~accountability(X35,X38,X40)|~accountability(X35,X39,X41)|greater(X42,X40)|~greater(X41,X40)|greater(X41,X43)))&(greater(X38,X39)|(~organization(X35,X40)|~organization(X35,X41)|~reorganization(X35,X42,X43)|~reliability(X35,X36,X40)|~reliability(X35,X37,X41)|~accountability(X35,X38,X40)|~accountability(X35,X39,X41)|greater(X42,X40)|~greater(X41,X40)|greater(X41,X43))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_5])])])])).
% 0.27/0.52 fof(c_0_8, negated_conjecture, ((((((((organization(esk4_0,esk7_0)&organization(esk4_0,esk8_0))&reorganization(esk4_0,esk9_0,esk10_0))&reproducibility(esk4_0,esk5_0,esk7_0))&reproducibility(esk4_0,esk6_0,esk8_0))&~greater(esk9_0,esk7_0))&greater(esk8_0,esk7_0))&~greater(esk8_0,esk10_0))&~greater(esk5_0,esk6_0)), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_6])])])])).
% 0.27/0.52 cnf(c_0_9, hypothesis, (greater(X1,X2)|greater(X6,X4)|greater(X5,X7)|~organization(X3,X4)|~organization(X3,X5)|~reorganization(X3,X6,X7)|~reliability(X3,X8,X4)|~reliability(X3,X9,X5)|~accountability(X3,X1,X4)|~accountability(X3,X2,X5)|~greater(X5,X4)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.27/0.52 cnf(c_0_10, negated_conjecture, (reorganization(esk4_0,esk9_0,esk10_0)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.27/0.52 fof(c_0_11, plain, ![X19, X20]:((~organization(X19,X20)|accountability(X19,esk2_2(X19,X20),X20))), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp2])])])])).
% 0.27/0.52 cnf(c_0_12, negated_conjecture, (greater(X1,esk10_0)|greater(esk9_0,X2)|greater(X3,X4)|~greater(X1,X2)|~accountability(esk4_0,X4,X1)|~accountability(esk4_0,X3,X2)|~reliability(esk4_0,X5,X1)|~reliability(esk4_0,X6,X2)|~organization(esk4_0,X1)|~organization(esk4_0,X2)), inference(spm,[status(thm)],[c_0_9, c_0_10])).
% 0.27/0.52 cnf(c_0_13, plain, (accountability(X1,esk2_2(X1,X2),X2)|~organization(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.27/0.52 fof(c_0_14, hypothesis, ![X25, X26, X27, X28, X29, X30, X31, X32, X33, X34]:((((greater(X30,X29)|~greater(X34,X33)|(~organization(X25,X27)|~organization(X26,X28)|~reliability(X25,X29,X27)|~reliability(X26,X30,X28)|~accountability(X25,X31,X27)|~accountability(X26,X32,X28)|~reproducibility(X25,X33,X27)|~reproducibility(X26,X34,X28)))&(greater(X32,X31)|~greater(X34,X33)|(~organization(X25,X27)|~organization(X26,X28)|~reliability(X25,X29,X27)|~reliability(X26,X30,X28)|~accountability(X25,X31,X27)|~accountability(X26,X32,X28)|~reproducibility(X25,X33,X27)|~reproducibility(X26,X34,X28))))&(~greater(X30,X29)|~greater(X32,X31)|greater(X34,X33)|(~organization(X25,X27)|~organization(X26,X28)|~reliability(X25,X29,X27)|~reliability(X26,X30,X28)|~accountability(X25,X31,X27)|~accountability(X26,X32,X28)|~reproducibility(X25,X33,X27)|~reproducibility(X26,X34,X28))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a2_FOL])])])])).
% 0.27/0.52 cnf(c_0_15, negated_conjecture, (greater(X1,esk2_2(esk4_0,X2))|greater(esk9_0,X3)|greater(X2,esk10_0)|~greater(X2,X3)|~accountability(esk4_0,X1,X3)|~reliability(esk4_0,X4,X2)|~reliability(esk4_0,X5,X3)|~organization(esk4_0,X2)|~organization(esk4_0,X3)), inference(spm,[status(thm)],[c_0_12, c_0_13])).
% 0.27/0.52 fof(c_0_16, plain, ![X16, X17]:((~organization(X16,X17)|reliability(X16,esk1_2(X16,X17),X17))), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp1])])])])).
% 0.27/0.52 cnf(c_0_17, hypothesis, (greater(X5,X6)|~greater(X1,X2)|~greater(X3,X4)|~organization(X7,X8)|~organization(X9,X10)|~reliability(X7,X2,X8)|~reliability(X9,X1,X10)|~accountability(X7,X4,X8)|~accountability(X9,X3,X10)|~reproducibility(X7,X6,X8)|~reproducibility(X9,X5,X10)), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.27/0.52 cnf(c_0_18, negated_conjecture, (reproducibility(esk4_0,esk5_0,esk7_0)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.27/0.52 cnf(c_0_19, negated_conjecture, (organization(esk4_0,esk7_0)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.27/0.52 cnf(c_0_20, negated_conjecture, (greater(esk2_2(esk4_0,X1),esk2_2(esk4_0,X2))|greater(X2,esk10_0)|greater(esk9_0,X1)|~greater(X2,X1)|~reliability(esk4_0,X3,X2)|~reliability(esk4_0,X4,X1)|~organization(esk4_0,X2)|~organization(esk4_0,X1)), inference(spm,[status(thm)],[c_0_15, c_0_13])).
% 0.27/0.52 cnf(c_0_21, plain, (reliability(X1,esk1_2(X1,X2),X2)|~organization(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_16])).
% 0.27/0.52 cnf(c_0_22, hypothesis, (greater(X1,X2)|greater(X6,X4)|greater(X5,X7)|~organization(X3,X4)|~organization(X3,X5)|~reorganization(X3,X6,X7)|~reliability(X3,X1,X4)|~reliability(X3,X2,X5)|~accountability(X3,X8,X4)|~accountability(X3,X9,X5)|~greater(X5,X4)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.27/0.52 cnf(c_0_23, negated_conjecture, (greater(esk5_0,X1)|~greater(X2,X3)|~greater(X4,X5)|~reproducibility(X6,X1,X7)|~accountability(esk4_0,X2,esk7_0)|~accountability(X6,X3,X7)|~reliability(esk4_0,X4,esk7_0)|~reliability(X6,X5,X7)|~organization(X6,X7)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_17, c_0_18]), c_0_19])])).
% 0.27/0.52 cnf(c_0_24, negated_conjecture, (greater(esk2_2(esk4_0,X1),esk2_2(esk4_0,X2))|greater(esk9_0,X1)|greater(X2,esk10_0)|~greater(X2,X1)|~reliability(esk4_0,X3,X1)|~organization(esk4_0,X2)|~organization(esk4_0,X1)), inference(spm,[status(thm)],[c_0_20, c_0_21])).
% 0.27/0.52 cnf(c_0_25, negated_conjecture, (greater(X1,esk10_0)|greater(esk9_0,X2)|greater(X3,X4)|~greater(X1,X2)|~accountability(esk4_0,X5,X1)|~accountability(esk4_0,X6,X2)|~reliability(esk4_0,X4,X1)|~reliability(esk4_0,X3,X2)|~organization(esk4_0,X1)|~organization(esk4_0,X2)), inference(spm,[status(thm)],[c_0_22, c_0_10])).
% 0.27/0.52 cnf(c_0_26, negated_conjecture, (greater(esk5_0,X1)|~greater(esk2_2(esk4_0,esk7_0),X2)|~greater(X3,X4)|~reproducibility(X5,X1,X6)|~accountability(X5,X2,X6)|~reliability(esk4_0,X3,esk7_0)|~reliability(X5,X4,X6)|~organization(X5,X6)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_13]), c_0_19])])).
% 0.27/0.52 cnf(c_0_27, negated_conjecture, (greater(esk2_2(esk4_0,X1),esk2_2(esk4_0,X2))|greater(X2,esk10_0)|greater(esk9_0,X1)|~greater(X2,X1)|~organization(esk4_0,X2)|~organization(esk4_0,X1)), inference(spm,[status(thm)],[c_0_24, c_0_21])).
% 0.27/0.52 cnf(c_0_28, negated_conjecture, (~greater(esk9_0,esk7_0)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.27/0.52 cnf(c_0_29, negated_conjecture, (greater(esk9_0,X1)|greater(X2,esk10_0)|greater(X3,X4)|~greater(X2,X1)|~accountability(esk4_0,X5,X1)|~reliability(esk4_0,X4,X2)|~reliability(esk4_0,X3,X1)|~organization(esk4_0,X2)|~organization(esk4_0,X1)), inference(spm,[status(thm)],[c_0_25, c_0_13])).
% 0.27/0.52 cnf(c_0_30, negated_conjecture, (greater(X1,esk10_0)|greater(esk5_0,X2)|~greater(X1,esk7_0)|~greater(X3,X4)|~reproducibility(X5,X2,X6)|~accountability(X5,esk2_2(esk4_0,X1),X6)|~reliability(esk4_0,X3,esk7_0)|~reliability(X5,X4,X6)|~organization(esk4_0,X1)|~organization(X5,X6)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_26, c_0_27]), c_0_19])]), c_0_28])).
% 0.27/0.52 cnf(c_0_31, negated_conjecture, (greater(X1,esk10_0)|greater(esk9_0,X2)|greater(X3,X4)|~greater(X1,X2)|~reliability(esk4_0,X4,X1)|~reliability(esk4_0,X3,X2)|~organization(esk4_0,X1)|~organization(esk4_0,X2)), inference(spm,[status(thm)],[c_0_29, c_0_13])).
% 0.27/0.52 cnf(c_0_32, negated_conjecture, (greater(esk5_0,X1)|greater(X2,esk10_0)|~greater(X2,esk7_0)|~greater(X3,X4)|~reproducibility(esk4_0,X1,X2)|~reliability(esk4_0,X3,esk7_0)|~reliability(esk4_0,X4,X2)|~organization(esk4_0,X2)), inference(spm,[status(thm)],[c_0_30, c_0_13])).
% 0.27/0.52 cnf(c_0_33, negated_conjecture, (greater(X1,esk1_2(esk4_0,X2))|greater(esk9_0,X3)|greater(X2,esk10_0)|~greater(X2,X3)|~reliability(esk4_0,X1,X3)|~organization(esk4_0,X2)|~organization(esk4_0,X3)), inference(spm,[status(thm)],[c_0_31, c_0_21])).
% 0.27/0.52 cnf(c_0_34, negated_conjecture, (greater(X1,esk10_0)|greater(esk5_0,X2)|~greater(esk1_2(esk4_0,esk7_0),X3)|~greater(X1,esk7_0)|~reproducibility(esk4_0,X2,X1)|~reliability(esk4_0,X3,X1)|~organization(esk4_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_21]), c_0_19])])).
% 0.27/0.52 cnf(c_0_35, negated_conjecture, (greater(esk1_2(esk4_0,X1),esk1_2(esk4_0,X2))|greater(X2,esk10_0)|greater(esk9_0,X1)|~greater(X2,X1)|~organization(esk4_0,X2)|~organization(esk4_0,X1)), inference(spm,[status(thm)],[c_0_33, c_0_21])).
% 0.27/0.52 cnf(c_0_36, negated_conjecture, (greater(X1,esk10_0)|greater(esk5_0,X2)|greater(X3,esk10_0)|~greater(X3,esk7_0)|~greater(X1,esk7_0)|~reproducibility(esk4_0,X2,X3)|~reliability(esk4_0,esk1_2(esk4_0,X1),X3)|~organization(esk4_0,X3)|~organization(esk4_0,X1)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_35]), c_0_19])]), c_0_28])).
% 0.27/0.52 cnf(c_0_37, negated_conjecture, (greater(esk5_0,X1)|greater(X2,esk10_0)|~greater(X2,esk7_0)|~reproducibility(esk4_0,X1,X2)|~organization(esk4_0,X2)), inference(spm,[status(thm)],[c_0_36, c_0_21])).
% 0.27/0.52 cnf(c_0_38, negated_conjecture, (reproducibility(esk4_0,esk6_0,esk8_0)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.27/0.52 cnf(c_0_39, negated_conjecture, (greater(esk8_0,esk7_0)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.27/0.52 cnf(c_0_40, negated_conjecture, (organization(esk4_0,esk8_0)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.27/0.52 cnf(c_0_41, negated_conjecture, (~greater(esk5_0,esk6_0)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.27/0.52 cnf(c_0_42, negated_conjecture, (~greater(esk8_0,esk10_0)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.27/0.52 cnf(c_0_43, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_38]), c_0_39]), c_0_40])]), c_0_41]), c_0_42]), ['proof']).
% 0.27/0.52 % SZS output end Proof
% 0.27/0.52 % User time : 0.017 s
% 0.27/0.52 % System time : 0.001 s
% 0.27/0.52 % Total time : 0.018 s
% 0.27/0.52 % User time : 0.044 s
% 0.27/0.52 % System time : 0.007 s
% 0.27/0.52 % Total time : 0.051 s
% 0.27/0.52
%------------------------------------------------------------------------------