%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT045+1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %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:18:46 AM UTC 2026
% Result : Theorem 87.96s 88.24s
% Output : CNFRefutation 87.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT045+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.37 % Computer : n018.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 7 13:10:52 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.16/0.43 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.16/0.43 (re.compile("\."), Token.FullStop),
% 0.16/0.43 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.16/0.43 (re.compile("\("), Token.OpenPar),
% 0.16/0.43 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.16/0.43 (re.compile("\)"), Token.ClosePar),
% 0.16/0.43 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.16/0.43 (re.compile("\["), Token.OpenSquare),
% 0.16/0.43 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.16/0.43 (re.compile("\]"), Token.CloseSquare),
% 0.16/0.44 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.16/0.44 (re.compile("~\|"), Token.Nor),
% 0.16/0.44 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.16/0.44 (re.compile("\|"), Token.Or),
% 0.16/0.44 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.16/0.44 (re.compile("\?"), Token.Existential),
% 0.16/0.44 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.16/0.44 (re.compile("\s+"), Token.WhiteSpace),
% 0.16/0.44 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.16/0.44 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.24/0.51 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.24/0.51 """
% 0.24/0.51 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.24/0.51 """
% 0.34/0.60 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.34/0.60 """
% 87.96/88.24 % Version: 1.5
% 87.96/88.24 % SZS status Theorem
% 87.96/88.24 % SZS output start CNFRefutation
% 87.96/88.24 fof(lemma_4,conjecture,(![X]:(![T0]:(![T]:((organization(X)&greater(age(X,T),age(X,T0)))=>greater(position(X,T),position(X,T0)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', lemma_4)).
% 87.96/88.24 fof(c8,negated_conjecture,(~(![X]:(![T0]:(![T]:((organization(X)&greater(age(X,T),age(X,T0)))=>greater(position(X,T),position(X,T0))))))),inference(assume_negation,[status(cth)],[lemma_4])).
% 87.96/88.24 fof(c9,negated_conjecture,(?[X]:(?[T0]:(?[T]:((organization(X)&greater(age(X,T),age(X,T0)))&~greater(position(X,T),position(X,T0)))))),inference(fof_nnf,[status(thm)],[c8])).
% 87.96/88.24 fof(c10,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((organization(X2)&greater(age(X2,X4),age(X2,X3)))&~greater(position(X2,X4),position(X2,X3)))))),inference(variable_rename,[status(thm)],[c9])).
% 87.96/88.24 fof(c11,negated_conjecture,((organization(skolem0001)&greater(age(skolem0001,skolem0003),age(skolem0001,skolem0002)))&~greater(position(skolem0001,skolem0003),position(skolem0001,skolem0002))),inference(skolemize,[status(esa)],[c10])).
% 87.96/88.24 cnf(c14,negated_conjecture,~greater(position(skolem0001,skolem0003),position(skolem0001,skolem0002)),inference(split_conjunct,[status(thm)],[c11])).
% 87.96/88.24 cnf(c12,negated_conjecture,organization(skolem0001),inference(split_conjunct,[status(thm)],[c11])).
% 87.96/88.24 fof(assumption_6,axiom,(![X]:(![T0]:(![T]:(organization(X)=>((greater(external_ties(X,T),external_ties(X,T0))=>greater(position(X,T),position(X,T0)))&(external_ties(X,T)=external_ties(X,T0)=>position(X,T)=position(X,T0))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_6)).
% 87.96/88.24 fof(c18,plain,(![X]:(![T0]:(![T]:(~organization(X)|((~greater(external_ties(X,T),external_ties(X,T0))|greater(position(X,T),position(X,T0)))&(external_ties(X,T)!=external_ties(X,T0)|position(X,T)=position(X,T0))))))),inference(fof_nnf,[status(thm)],[assumption_6])).
% 87.96/88.24 fof(c19,plain,(![X]:(~organization(X)|((![T0]:(![T]:(~greater(external_ties(X,T),external_ties(X,T0))|greater(position(X,T),position(X,T0)))))&(![T0]:(![T]:(external_ties(X,T)!=external_ties(X,T0)|position(X,T)=position(X,T0))))))),inference(shift_quantors,[status(thm)],[c18])).
% 87.96/88.24 fof(c21,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(~organization(X8)|((~greater(external_ties(X8,X10),external_ties(X8,X9))|greater(position(X8,X10),position(X8,X9)))&(external_ties(X8,X12)!=external_ties(X8,X11)|position(X8,X12)=position(X8,X11))))))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,(![X8]:(~organization(X8)|((![X9]:(![X10]:(~greater(external_ties(X8,X10),external_ties(X8,X9))|greater(position(X8,X10),position(X8,X9)))))&(![X11]:(![X12]:(external_ties(X8,X12)!=external_ties(X8,X11)|position(X8,X12)=position(X8,X11))))))),inference(variable_rename,[status(thm)],[c19])).])).
% 87.96/88.24 fof(c22,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:((~organization(X8)|(~greater(external_ties(X8,X10),external_ties(X8,X9))|greater(position(X8,X10),position(X8,X9))))&(~organization(X8)|(external_ties(X8,X12)!=external_ties(X8,X11)|position(X8,X12)=position(X8,X11))))))))),inference(distribute,[status(thm)],[c21])).
% 87.96/88.24 cnf(c23,plain,~organization(X166)|~greater(external_ties(X166,X165),external_ties(X166,X164))|greater(position(X166,X165),position(X166,X164)),inference(split_conjunct,[status(thm)],[c22])).
% 87.96/88.24 cnf(c13,negated_conjecture,greater(age(skolem0001,skolem0003),age(skolem0001,skolem0002)),inference(split_conjunct,[status(thm)],[c11])).
% 87.96/88.24 fof(assumption_8,axiom,(![X]:(![T0]:(![T]:((organization(X)&greater(age(X,T),age(X,T0)))=>greater(external_ties(X,T),external_ties(X,T0)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_8)).
% 87.96/88.24 fof(c15,plain,(![X]:(![T0]:(![T]:((~organization(X)|~greater(age(X,T),age(X,T0)))|greater(external_ties(X,T),external_ties(X,T0)))))),inference(fof_nnf,[status(thm)],[assumption_8])).
% 87.96/88.24 fof(c16,plain,(![X5]:(![X6]:(![X7]:((~organization(X5)|~greater(age(X5,X7),age(X5,X6)))|greater(external_ties(X5,X7),external_ties(X5,X6)))))),inference(variable_rename,[status(thm)],[c15])).
% 87.96/88.24 cnf(c17,plain,~organization(X152)|~greater(age(X152,X151),age(X152,X153))|greater(external_ties(X152,X151),external_ties(X152,X153)),inference(split_conjunct,[status(thm)],[c16])).
% 87.96/88.24 cnf(c213,plain,~organization(skolem0001)|greater(external_ties(skolem0001,skolem0003),external_ties(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c17, c13])).
% 87.96/88.24 cnf(c2262,plain,greater(external_ties(skolem0001,skolem0003),external_ties(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c213, c12])).
% 87.96/88.24 cnf(c2267,plain,~organization(skolem0001)|greater(position(skolem0001,skolem0003),position(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c2262, c23])).
% 87.96/88.24 cnf(c125607,plain,greater(position(skolem0001,skolem0003),position(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c2267, c12])).
% 87.96/88.24 cnf(c125695,plain,$false,inference(resolution,[status(thm)],[c125607, c14])).
% 87.96/88.24 % SZS output end CNFRefutation
% 87.96/88.24
% 87.96/88.24 % Initial clauses : 28
% 87.96/88.24 % Processed clauses : 842
% 87.96/88.24 % Factors computed : 609
% 87.96/88.24 % Resolvents computed: 125043
% 87.96/88.24 % Tautologies deleted: 24
% 87.96/88.24 % Forward subsumed : 2959
% 87.96/88.24 % Backward subsumed : 230
% 87.96/88.24 % -------- CPU Time ---------
% 87.96/88.24 % User time : 87.452 s
% 87.96/88.24 % System time : 0.406 s
% 87.96/88.24 % Total time : 87.858 s
%------------------------------------------------------------------------------