%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT044+1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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 154.24s 154.59s
% Output : CNFRefutation 154.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT044+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.36 % Computer : n028.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 7 13:09:17 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.09/0.43 (re.compile("\."), Token.FullStop),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.09/0.43 (re.compile("\("), Token.OpenPar),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.09/0.43 (re.compile("\)"), Token.ClosePar),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.09/0.43 (re.compile("\["), Token.OpenSquare),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.09/0.43 (re.compile("\]"), Token.CloseSquare),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.43 (re.compile("~\|"), Token.Nor),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.43 (re.compile("\|"), Token.Or),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.09/0.43 (re.compile("\?"), Token.Existential),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.09/0.43 (re.compile("\s+"), Token.WhiteSpace),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.09/0.43 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.50 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.22/0.50 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.32/0.59 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.59 """
% 154.24/154.59 % Version: 1.5
% 154.24/154.59 % SZS status Theorem
% 154.24/154.59 % SZS output start CNFRefutation
% 154.24/154.59 fof(lemma_3,conjecture,(![X]:(![T0]:(![T]:((organization(X)&greater(age(X,T),age(X,T0)))=>greater(capability(X,T),capability(X,T0)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', lemma_3)).
% 154.24/154.59 fof(c9,negated_conjecture,(~(![X]:(![T0]:(![T]:((organization(X)&greater(age(X,T),age(X,T0)))=>greater(capability(X,T),capability(X,T0))))))),inference(assume_negation,[status(cth)],[lemma_3])).
% 154.24/154.59 fof(c10,negated_conjecture,(?[X]:(?[T0]:(?[T]:((organization(X)&greater(age(X,T),age(X,T0)))&~greater(capability(X,T),capability(X,T0)))))),inference(fof_nnf,[status(thm)],[c9])).
% 154.24/154.59 fof(c11,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((organization(X2)&greater(age(X2,X4),age(X2,X3)))&~greater(capability(X2,X4),capability(X2,X3)))))),inference(variable_rename,[status(thm)],[c10])).
% 154.24/154.59 fof(c12,negated_conjecture,((organization(skolem0001)&greater(age(skolem0001,skolem0003),age(skolem0001,skolem0002)))&~greater(capability(skolem0001,skolem0003),capability(skolem0001,skolem0002))),inference(skolemize,[status(esa)],[c11])).
% 154.24/154.59 cnf(c15,negated_conjecture,~greater(capability(skolem0001,skolem0003),capability(skolem0001,skolem0002)),inference(split_conjunct,[status(thm)],[c12])).
% 154.24/154.59 cnf(c13,negated_conjecture,organization(skolem0001),inference(split_conjunct,[status(thm)],[c12])).
% 154.24/154.59 cnf(c14,negated_conjecture,greater(age(skolem0001,skolem0003),age(skolem0001,skolem0002)),inference(split_conjunct,[status(thm)],[c12])).
% 154.24/154.59 fof(assumption_7,axiom,(![X]:(![T0]:(![T]:((organization(X)&greater(age(X,T),age(X,T0)))=>greater(stock_of_knowledge(X,T),stock_of_knowledge(X,T0)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_7)).
% 154.24/154.59 fof(c21,plain,(![X]:(![T0]:(![T]:((~organization(X)|~greater(age(X,T),age(X,T0)))|greater(stock_of_knowledge(X,T),stock_of_knowledge(X,T0)))))),inference(fof_nnf,[status(thm)],[assumption_7])).
% 154.24/154.59 fof(c22,plain,(![X8]:(![X9]:(![X10]:((~organization(X8)|~greater(age(X8,X10),age(X8,X9)))|greater(stock_of_knowledge(X8,X10),stock_of_knowledge(X8,X9)))))),inference(variable_rename,[status(thm)],[c21])).
% 154.24/154.59 cnf(c23,plain,~organization(X183)|~greater(age(X183,X182),age(X183,X184))|greater(stock_of_knowledge(X183,X182),stock_of_knowledge(X183,X184)),inference(split_conjunct,[status(thm)],[c22])).
% 154.24/154.59 cnf(c247,plain,~organization(skolem0001)|greater(stock_of_knowledge(skolem0001,skolem0003),stock_of_knowledge(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c23, c14])).
% 154.24/154.59 cnf(c3487,plain,greater(stock_of_knowledge(skolem0001,skolem0003),stock_of_knowledge(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c247, c13])).
% 154.24/154.59 fof(assumption_5,axiom,(![X]:(![T0]:(![T]:(organization(X)=>((((greater(stock_of_knowledge(X,T),stock_of_knowledge(X,T0))&smaller_or_equal(internal_friction(X,T),internal_friction(X,T0)))=>greater(capability(X,T),capability(X,T0)))&((smaller_or_equal(stock_of_knowledge(X,T),stock_of_knowledge(X,T0))&greater(internal_friction(X,T),internal_friction(X,T0)))=>smaller(capability(X,T),capability(X,T0))))&((stock_of_knowledge(X,T)=stock_of_knowledge(X,T0)&internal_friction(X,T)=internal_friction(X,T0))=>capability(X,T)=capability(X,T0))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_5)).
% 154.24/154.59 fof(c24,plain,(![X]:(![T0]:(![T]:(~organization(X)|((((~greater(stock_of_knowledge(X,T),stock_of_knowledge(X,T0))|~smaller_or_equal(internal_friction(X,T),internal_friction(X,T0)))|greater(capability(X,T),capability(X,T0)))&((~smaller_or_equal(stock_of_knowledge(X,T),stock_of_knowledge(X,T0))|~greater(internal_friction(X,T),internal_friction(X,T0)))|smaller(capability(X,T),capability(X,T0))))&((stock_of_knowledge(X,T)!=stock_of_knowledge(X,T0)|internal_friction(X,T)!=internal_friction(X,T0))|capability(X,T)=capability(X,T0))))))),inference(fof_nnf,[status(thm)],[assumption_5])).
% 154.24/154.59 fof(c25,plain,(![X]:(~organization(X)|(((![T0]:(![T]:((~greater(stock_of_knowledge(X,T),stock_of_knowledge(X,T0))|~smaller_or_equal(internal_friction(X,T),internal_friction(X,T0)))|greater(capability(X,T),capability(X,T0)))))&(![T0]:(![T]:((~smaller_or_equal(stock_of_knowledge(X,T),stock_of_knowledge(X,T0))|~greater(internal_friction(X,T),internal_friction(X,T0)))|smaller(capability(X,T),capability(X,T0))))))&(![T0]:(![T]:((stock_of_knowledge(X,T)!=stock_of_knowledge(X,T0)|internal_friction(X,T)!=internal_friction(X,T0))|capability(X,T)=capability(X,T0))))))),inference(shift_quantors,[status(thm)],[c24])).
% 154.24/154.59 fof(c27,plain,(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(~organization(X11)|((((~greater(stock_of_knowledge(X11,X13),stock_of_knowledge(X11,X12))|~smaller_or_equal(internal_friction(X11,X13),internal_friction(X11,X12)))|greater(capability(X11,X13),capability(X11,X12)))&((~smaller_or_equal(stock_of_knowledge(X11,X15),stock_of_knowledge(X11,X14))|~greater(internal_friction(X11,X15),internal_friction(X11,X14)))|smaller(capability(X11,X15),capability(X11,X14))))&((stock_of_knowledge(X11,X17)!=stock_of_knowledge(X11,X16)|internal_friction(X11,X17)!=internal_friction(X11,X16))|capability(X11,X17)=capability(X11,X16))))))))))),inference(shift_quantors,[status(thm)],[fof(c26,plain,(![X11]:(~organization(X11)|(((![X12]:(![X13]:((~greater(stock_of_knowledge(X11,X13),stock_of_knowledge(X11,X12))|~smaller_or_equal(internal_friction(X11,X13),internal_friction(X11,X12)))|greater(capability(X11,X13),capability(X11,X12)))))&(![X14]:(![X15]:((~smaller_or_equal(stock_of_knowledge(X11,X15),stock_of_knowledge(X11,X14))|~greater(internal_friction(X11,X15),internal_friction(X11,X14)))|smaller(capability(X11,X15),capability(X11,X14))))))&(![X16]:(![X17]:((stock_of_knowledge(X11,X17)!=stock_of_knowledge(X11,X16)|internal_friction(X11,X17)!=internal_friction(X11,X16))|capability(X11,X17)=capability(X11,X16))))))),inference(variable_rename,[status(thm)],[c25])).])).
% 154.24/154.59 fof(c28,plain,(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(((~organization(X11)|((~greater(stock_of_knowledge(X11,X13),stock_of_knowledge(X11,X12))|~smaller_or_equal(internal_friction(X11,X13),internal_friction(X11,X12)))|greater(capability(X11,X13),capability(X11,X12))))&(~organization(X11)|((~smaller_or_equal(stock_of_knowledge(X11,X15),stock_of_knowledge(X11,X14))|~greater(internal_friction(X11,X15),internal_friction(X11,X14)))|smaller(capability(X11,X15),capability(X11,X14)))))&(~organization(X11)|((stock_of_knowledge(X11,X17)!=stock_of_knowledge(X11,X16)|internal_friction(X11,X17)!=internal_friction(X11,X16))|capability(X11,X17)=capability(X11,X16))))))))))),inference(distribute,[status(thm)],[c27])).
% 154.24/154.59 cnf(c29,plain,~organization(X198)|~greater(stock_of_knowledge(X198,X197),stock_of_knowledge(X198,X196))|~smaller_or_equal(internal_friction(X198,X197),internal_friction(X198,X196))|greater(capability(X198,X197),capability(X198,X196)),inference(split_conjunct,[status(thm)],[c28])).
% 154.24/154.59 cnf(reflexivity,axiom,X37=X37,theory(equality)).
% 154.24/154.59 fof(definition_smaller_or_equal,axiom,(![X]:(![Y]:(smaller_or_equal(X,Y)<=>(smaller(X,Y)|X=Y)))),file('/export/starexec/sandbox2/benchmark/Axioms/MGT001+0.ax', definition_smaller_or_equal)).
% 154.24/154.59 fof(c54,plain,(![X]:(![Y]:((~smaller_or_equal(X,Y)|(smaller(X,Y)|X=Y))&((~smaller(X,Y)&X!=Y)|smaller_or_equal(X,Y))))),inference(fof_nnf,[status(thm)],[definition_smaller_or_equal])).
% 154.24/154.59 fof(c55,plain,((![X]:(![Y]:(~smaller_or_equal(X,Y)|(smaller(X,Y)|X=Y))))&(![X]:(![Y]:((~smaller(X,Y)&X!=Y)|smaller_or_equal(X,Y))))),inference(shift_quantors,[status(thm)],[c54])).
% 154.24/154.59 fof(c57,plain,(![X33]:(![X34]:(![X35]:(![X36]:((~smaller_or_equal(X33,X34)|(smaller(X33,X34)|X33=X34))&((~smaller(X35,X36)&X35!=X36)|smaller_or_equal(X35,X36))))))),inference(shift_quantors,[status(thm)],[fof(c56,plain,((![X33]:(![X34]:(~smaller_or_equal(X33,X34)|(smaller(X33,X34)|X33=X34))))&(![X35]:(![X36]:((~smaller(X35,X36)&X35!=X36)|smaller_or_equal(X35,X36))))),inference(variable_rename,[status(thm)],[c55])).])).
% 154.24/154.59 fof(c58,plain,(![X33]:(![X34]:(![X35]:(![X36]:((~smaller_or_equal(X33,X34)|(smaller(X33,X34)|X33=X34))&((~smaller(X35,X36)|smaller_or_equal(X35,X36))&(X35!=X36|smaller_or_equal(X35,X36)))))))),inference(distribute,[status(thm)],[c57])).
% 154.24/154.59 cnf(c61,plain,X62!=X63|smaller_or_equal(X62,X63),inference(split_conjunct,[status(thm)],[c58])).
% 154.24/154.59 cnf(c69,plain,smaller_or_equal(X64,X64),inference(resolution,[status(thm)],[c61, reflexivity])).
% 154.24/154.59 cnf(c4,axiom,X104!=X101|X103!=X102|~smaller_or_equal(X104,X103)|smaller_or_equal(X101,X102),theory(equality)).
% 154.24/154.59 cnf(c116,plain,X192!=X191|X192!=X193|smaller_or_equal(X191,X193),inference(resolution,[status(thm)],[c4, c69])).
% 154.24/154.59 cnf(c252,plain,X199!=X200|smaller_or_equal(X200,X199),inference(resolution,[status(thm)],[c116, reflexivity])).
% 154.24/154.59 fof(assumption_9,axiom,(![X]:(![T0]:(![T]:(organization(X)=>internal_friction(X,T)=internal_friction(X,T0))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_9)).
% 154.24/154.59 fof(c16,plain,(![X]:(![T0]:(![T]:(~organization(X)|internal_friction(X,T)=internal_friction(X,T0))))),inference(fof_nnf,[status(thm)],[assumption_9])).
% 154.24/154.59 fof(c17,plain,(![X]:(~organization(X)|(![T0]:(![T]:internal_friction(X,T)=internal_friction(X,T0))))),inference(shift_quantors,[status(thm)],[c16])).
% 154.24/154.59 fof(c19,plain,(![X5]:(![X6]:(![X7]:(~organization(X5)|internal_friction(X5,X7)=internal_friction(X5,X6))))),inference(shift_quantors,[status(thm)],[fof(c18,plain,(![X5]:(~organization(X5)|(![X6]:(![X7]:internal_friction(X5,X7)=internal_friction(X5,X6))))),inference(variable_rename,[status(thm)],[c17])).])).
% 154.24/154.59 cnf(c20,plain,~organization(X170)|internal_friction(X170,X169)=internal_friction(X170,X171),inference(split_conjunct,[status(thm)],[c19])).
% 154.24/154.59 cnf(c241,plain,internal_friction(skolem0001,X333)=internal_friction(skolem0001,X334),inference(resolution,[status(thm)],[c20, c13])).
% 154.24/154.59 cnf(c345,plain,smaller_or_equal(internal_friction(skolem0001,X398),internal_friction(skolem0001,X397)),inference(resolution,[status(thm)],[c241, c252])).
% 154.24/154.59 cnf(c468,plain,~organization(skolem0001)|~greater(stock_of_knowledge(skolem0001,X3174),stock_of_knowledge(skolem0001,X3173))|greater(capability(skolem0001,X3174),capability(skolem0001,X3173)),inference(resolution,[status(thm)],[c345, c29])).
% 154.24/154.59 cnf(c24678,plain,~organization(skolem0001)|greater(capability(skolem0001,skolem0003),capability(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c468, c3487])).
% 154.24/154.59 cnf(c193149,plain,greater(capability(skolem0001,skolem0003),capability(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c24678, c13])).
% 154.24/154.59 cnf(c193209,plain,$false,inference(resolution,[status(thm)],[c193149, c15])).
% 154.24/154.59 % SZS output end CNFRefutation
% 154.24/154.59
% 154.24/154.59 % Initial clauses : 31
% 154.24/154.59 % Processed clauses : 1092
% 154.24/154.59 % Factors computed : 727
% 154.24/154.59 % Resolvents computed: 192461
% 154.24/154.59 % Tautologies deleted: 38
% 154.24/154.59 % Forward subsumed : 3511
% 154.24/154.59 % Backward subsumed : 262
% 154.24/154.59 % -------- CPU Time ---------
% 154.24/154.59 % User time : 153.477 s
% 154.24/154.59 % System time : 0.729 s
% 154.24/154.59 % Total time : 154.206 s
%------------------------------------------------------------------------------