%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT045+1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n019.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:34 AM UTC 2026
% Result : Theorem 0.26s 0.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT045+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.07/0.34 % Computer : n019.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 13:09:22 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.12/0.42 start to proof:theBenchmark.p
% 0.26/0.47 % Version : CSI_E---1.1
% 0.26/0.47 % Problem : theBenchmark.p
% 0.26/0.47 % Proof found!
% 0.26/0.47 % SZS status Theorem for theBenchmark.p
% 0.26/0.47 % SZS output start Proof
% 0.26/0.47 fof(lemma_4, conjecture, ![X1, X4, X5]:(((organization(X1)&greater(age(X1,X5),age(X1,X4)))=>greater(position(X1,X5),position(X1,X4)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', lemma_4)).
% 0.26/0.47 fof(assumption_8, axiom, ![X1, X4, X5]:(((organization(X1)&greater(age(X1,X5),age(X1,X4)))=>greater(external_ties(X1,X5),external_ties(X1,X4)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_8)).
% 0.26/0.47 fof(assumption_6, axiom, ![X1, X4, X5]:((organization(X1)=>((greater(external_ties(X1,X5),external_ties(X1,X4))=>greater(position(X1,X5),position(X1,X4)))&(external_ties(X1,X5)=external_ties(X1,X4)=>position(X1,X5)=position(X1,X4))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_6)).
% 0.26/0.47 fof(c_0_3, negated_conjecture, ~(![X1, X4, X5]:(((organization(X1)&greater(age(X1,X5),age(X1,X4)))=>greater(position(X1,X5),position(X1,X4))))), inference(assume_negation,[status(cth)],[lemma_4])).
% 0.26/0.47 fof(c_0_4, plain, ![X17, X18, X19]:((~organization(X17)|~greater(age(X17,X19),age(X17,X18))|greater(external_ties(X17,X19),external_ties(X17,X18)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_8])])])).
% 0.26/0.47 fof(c_0_5, negated_conjecture, ((organization(esk1_0)&greater(age(esk1_0,esk3_0),age(esk1_0,esk2_0)))&~greater(position(esk1_0,esk3_0),position(esk1_0,esk2_0))), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_3])])])])).
% 0.26/0.47 fof(c_0_6, plain, ![X14, X15, X16]:(((~greater(external_ties(X14,X16),external_ties(X14,X15))|greater(position(X14,X16),position(X14,X15))|~organization(X14))&(external_ties(X14,X16)!=external_ties(X14,X15)|position(X14,X16)=position(X14,X15)|~organization(X14)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_6])])])])).
% 0.26/0.47 cnf(c_0_7, plain, (greater(external_ties(X1,X2),external_ties(X1,X3))|~organization(X1)|~greater(age(X1,X2),age(X1,X3))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.26/0.47 cnf(c_0_8, negated_conjecture, (greater(age(esk1_0,esk3_0),age(esk1_0,esk2_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.26/0.47 cnf(c_0_9, negated_conjecture, (organization(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.26/0.47 cnf(c_0_10, plain, (greater(position(X1,X2),position(X1,X3))|~greater(external_ties(X1,X2),external_ties(X1,X3))|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.26/0.47 cnf(c_0_11, negated_conjecture, (greater(external_ties(esk1_0,esk3_0),external_ties(esk1_0,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_7, c_0_8]), c_0_9])])).
% 0.26/0.47 cnf(c_0_12, negated_conjecture, (~greater(position(esk1_0,esk3_0),position(esk1_0,esk2_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.26/0.47 cnf(c_0_13, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10, c_0_11]), c_0_9])]), c_0_12]), ['proof']).
% 0.26/0.47 % SZS output end Proof
% 0.26/0.47 % User time : 0.005 s
% 0.26/0.47 % System time : 0.002 s
% 0.26/0.47 % Total time : 0.007 s
% 0.26/0.47 % User time : 0.006 s
% 0.26/0.47 % System time : 0.006 s
% 0.26/0.47 % Total time : 0.012 s
% 0.26/0.47
%------------------------------------------------------------------------------