%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT058+1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:48 AM UTC 2026
% Result : Theorem 0.91s 1.15s
% Output : CNFRefutation 0.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : MGT058+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.06 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.16/0.42 % Computer : n029.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 7 13:32:56 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.16/0.48 (re.compile("\."), Token.FullStop),
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.16/0.48 (re.compile("\("), Token.OpenPar),
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.16/0.48 (re.compile("\)"), Token.ClosePar),
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.16/0.48 (re.compile("\["), Token.OpenSquare),
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.16/0.48 (re.compile("\]"), Token.CloseSquare),
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.16/0.48 (re.compile("~\|"), Token.Nor),
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.16/0.48 (re.compile("\|"), Token.Or),
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.16/0.48 (re.compile("\?"), Token.Existential),
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.16/0.48 (re.compile("\s+"), Token.WhiteSpace),
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.16/0.48 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.27/0.54 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.27/0.54 """
% 0.27/0.54 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.27/0.54 """
% 0.36/0.62 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.36/0.62 """
% 0.91/1.15 % Version: 1.5
% 0.91/1.15 % SZS status Theorem
% 0.91/1.15 % SZS output start CNFRefutation
% 0.91/1.15 fof(lemma_10,conjecture,(![X]:((((organization(X)&(?[T0]:age(X,T0)=zero))&greater_or_equal(sigma,zero))&greater_or_equal(tau,zero))=>(~(fragile_position(X)&robust_position(X))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', lemma_10)).
% 0.91/1.15 fof(c9,negated_conjecture,(~(![X]:((((organization(X)&(?[T0]:age(X,T0)=zero))&greater_or_equal(sigma,zero))&greater_or_equal(tau,zero))=>(~(fragile_position(X)&robust_position(X)))))),inference(assume_negation,[status(cth)],[lemma_10])).
% 0.91/1.15 fof(c10,negated_conjecture,(?[X]:((((organization(X)&(?[T0]:age(X,T0)=zero))&greater_or_equal(sigma,zero))&greater_or_equal(tau,zero))&(fragile_position(X)&robust_position(X)))),inference(fof_nnf,[status(thm)],[c9])).
% 0.91/1.15 fof(c11,negated_conjecture,(?[X2]:((((organization(X2)&(?[X3]:age(X2,X3)=zero))&greater_or_equal(sigma,zero))&greater_or_equal(tau,zero))&(fragile_position(X2)&robust_position(X2)))),inference(variable_rename,[status(thm)],[c10])).
% 0.91/1.15 fof(c12,negated_conjecture,((((organization(skolem0001)&age(skolem0001,skolem0002)=zero)&greater_or_equal(sigma,zero))&greater_or_equal(tau,zero))&(fragile_position(skolem0001)&robust_position(skolem0001))),inference(skolemize,[status(esa)],[c11])).
% 0.91/1.15 cnf(c18,negated_conjecture,robust_position(skolem0001),inference(split_conjunct,[status(thm)],[c12])).
% 0.91/1.15 cnf(c17,negated_conjecture,fragile_position(skolem0001),inference(split_conjunct,[status(thm)],[c12])).
% 0.91/1.15 fof(definition_3,axiom,(![X]:(fragile_position(X)<=>(![T]:((smaller_or_equal(age(X,T),sigma)=>positional_advantage(X,T))&(greater(age(X,T),sigma)=>(~positional_advantage(X,T))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', definition_3)).
% 0.91/1.15 fof(c32,plain,(![X]:(fragile_position(X)<=>(![T]:((smaller_or_equal(age(X,T),sigma)=>positional_advantage(X,T))&(greater(age(X,T),sigma)=>~positional_advantage(X,T)))))),inference(fof_simplification,[status(thm)],[definition_3])).
% 0.91/1.15 fof(c33,plain,(![X]:((~fragile_position(X)|(![T]:((~smaller_or_equal(age(X,T),sigma)|positional_advantage(X,T))&(~greater(age(X,T),sigma)|~positional_advantage(X,T)))))&((?[T]:((smaller_or_equal(age(X,T),sigma)&~positional_advantage(X,T))|(greater(age(X,T),sigma)&positional_advantage(X,T))))|fragile_position(X)))),inference(fof_nnf,[status(thm)],[c32])).
% 0.91/1.15 fof(c34,plain,((![X]:(~fragile_position(X)|((![T]:(~smaller_or_equal(age(X,T),sigma)|positional_advantage(X,T)))&(![T]:(~greater(age(X,T),sigma)|~positional_advantage(X,T))))))&(![X]:(((?[T]:(smaller_or_equal(age(X,T),sigma)&~positional_advantage(X,T)))|(?[T]:(greater(age(X,T),sigma)&positional_advantage(X,T))))|fragile_position(X)))),inference(shift_quantors,[status(thm)],[c33])).
% 0.91/1.15 fof(c35,plain,((![X10]:(~fragile_position(X10)|((![X11]:(~smaller_or_equal(age(X10,X11),sigma)|positional_advantage(X10,X11)))&(![X12]:(~greater(age(X10,X12),sigma)|~positional_advantage(X10,X12))))))&(![X13]:(((?[X14]:(smaller_or_equal(age(X13,X14),sigma)&~positional_advantage(X13,X14)))|(?[X15]:(greater(age(X13,X15),sigma)&positional_advantage(X13,X15))))|fragile_position(X13)))),inference(variable_rename,[status(thm)],[c34])).
% 0.91/1.15 fof(c37,plain,(![X10]:(![X11]:(![X12]:(![X13]:((~fragile_position(X10)|((~smaller_or_equal(age(X10,X11),sigma)|positional_advantage(X10,X11))&(~greater(age(X10,X12),sigma)|~positional_advantage(X10,X12))))&(((smaller_or_equal(age(X13,skolem0005(X13)),sigma)&~positional_advantage(X13,skolem0005(X13)))|(greater(age(X13,skolem0006(X13)),sigma)&positional_advantage(X13,skolem0006(X13))))|fragile_position(X13))))))),inference(shift_quantors,[status(thm)],[fof(c36,plain,((![X10]:(~fragile_position(X10)|((![X11]:(~smaller_or_equal(age(X10,X11),sigma)|positional_advantage(X10,X11)))&(![X12]:(~greater(age(X10,X12),sigma)|~positional_advantage(X10,X12))))))&(![X13]:(((smaller_or_equal(age(X13,skolem0005(X13)),sigma)&~positional_advantage(X13,skolem0005(X13)))|(greater(age(X13,skolem0006(X13)),sigma)&positional_advantage(X13,skolem0006(X13))))|fragile_position(X13)))),inference(skolemize,[status(esa)],[c35])).])).
% 0.91/1.15 fof(c38,plain,(![X10]:(![X11]:(![X12]:(![X13]:(((~fragile_position(X10)|(~smaller_or_equal(age(X10,X11),sigma)|positional_advantage(X10,X11)))&(~fragile_position(X10)|(~greater(age(X10,X12),sigma)|~positional_advantage(X10,X12))))&((((smaller_or_equal(age(X13,skolem0005(X13)),sigma)|greater(age(X13,skolem0006(X13)),sigma))|fragile_position(X13))&((smaller_or_equal(age(X13,skolem0005(X13)),sigma)|positional_advantage(X13,skolem0006(X13)))|fragile_position(X13)))&(((~positional_advantage(X13,skolem0005(X13))|greater(age(X13,skolem0006(X13)),sigma))|fragile_position(X13))&((~positional_advantage(X13,skolem0005(X13))|positional_advantage(X13,skolem0006(X13)))|fragile_position(X13))))))))),inference(distribute,[status(thm)],[c37])).
% 0.91/1.15 cnf(c39,plain,~fragile_position(X161)|~smaller_or_equal(age(X161,X160),sigma)|positional_advantage(X161,X160),inference(split_conjunct,[status(thm)],[c38])).
% 0.91/1.15 cnf(symmetry,axiom,X36!=X37|X37=X36,theory(equality)).
% 0.91/1.15 cnf(c14,negated_conjecture,age(skolem0001,skolem0002)=zero,inference(split_conjunct,[status(thm)],[c12])).
% 0.91/1.15 cnf(c94,plain,zero=age(skolem0001,skolem0002),inference(resolution,[status(thm)],[c14, symmetry])).
% 0.91/1.15 cnf(reflexivity,axiom,X35=X35,theory(equality)).
% 0.91/1.15 cnf(c1,axiom,X70!=X69|X71!=X68|~smaller_or_equal(X70,X71)|smaller_or_equal(X69,X68),theory(equality)).
% 0.91/1.15 fof(definition_smaller_or_equal,axiom,(![X]:(![Y]:(smaller_or_equal(X,Y)<=>(smaller(X,Y)|X=Y)))),file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax', definition_smaller_or_equal)).
% 0.91/1.15 fof(c67,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])).
% 0.91/1.15 fof(c68,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)],[c67])).
% 0.91/1.15 fof(c70,plain,(![X31]:(![X32]:(![X33]:(![X34]:((~smaller_or_equal(X31,X32)|(smaller(X31,X32)|X31=X32))&((~smaller(X33,X34)&X33!=X34)|smaller_or_equal(X33,X34))))))),inference(shift_quantors,[status(thm)],[fof(c69,plain,((![X31]:(![X32]:(~smaller_or_equal(X31,X32)|(smaller(X31,X32)|X31=X32))))&(![X33]:(![X34]:((~smaller(X33,X34)&X33!=X34)|smaller_or_equal(X33,X34))))),inference(variable_rename,[status(thm)],[c68])).])).
% 0.91/1.15 fof(c71,plain,(![X31]:(![X32]:(![X33]:(![X34]:((~smaller_or_equal(X31,X32)|(smaller(X31,X32)|X31=X32))&((~smaller(X33,X34)|smaller_or_equal(X33,X34))&(X33!=X34|smaller_or_equal(X33,X34)))))))),inference(distribute,[status(thm)],[c70])).
% 0.91/1.15 cnf(c74,plain,X61!=X60|smaller_or_equal(X61,X60),inference(split_conjunct,[status(thm)],[c71])).
% 0.91/1.15 cnf(c82,plain,smaller_or_equal(X62,X62),inference(resolution,[status(thm)],[c74, reflexivity])).
% 0.91/1.15 cnf(c84,plain,X109!=X108|X109!=X110|smaller_or_equal(X108,X110),inference(resolution,[status(thm)],[c1, c82])).
% 0.91/1.15 cnf(c140,plain,X114!=X113|smaller_or_equal(X113,X114),inference(resolution,[status(thm)],[c84, reflexivity])).
% 0.91/1.15 fof(meaning_postulate_greater_strict,axiom,(![X]:(![Y]:(~(greater(X,Y)&greater(Y,X))))),file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax', meaning_postulate_greater_strict)).
% 0.91/1.15 fof(c50,plain,(![X]:(![Y]:(~greater(X,Y)|~greater(Y,X)))),inference(fof_nnf,[status(thm)],[meaning_postulate_greater_strict])).
% 0.91/1.15 fof(c51,plain,(![X21]:(![X22]:(~greater(X21,X22)|~greater(X22,X21)))),inference(variable_rename,[status(thm)],[c50])).
% 0.91/1.15 cnf(c52,plain,~greater(X39,X40)|~greater(X40,X39),inference(split_conjunct,[status(thm)],[c51])).
% 0.91/1.15 cnf(c73,plain,~smaller(X55,X54)|smaller_or_equal(X55,X54),inference(split_conjunct,[status(thm)],[c71])).
% 0.91/1.15 fof(meaning_postulate_greater_comparable,axiom,(![X]:(![Y]:((smaller(X,Y)|X=Y)|greater(X,Y)))),file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax', meaning_postulate_greater_comparable)).
% 0.91/1.15 fof(c45,plain,(![X16]:(![X17]:((smaller(X16,X17)|X16=X17)|greater(X16,X17)))),inference(variable_rename,[status(thm)],[meaning_postulate_greater_comparable])).
% 0.91/1.15 cnf(c46,plain,smaller(X87,X88)|X87=X88|greater(X87,X88),inference(split_conjunct,[status(thm)],[c45])).
% 0.91/1.15 cnf(c112,plain,X135=X136|greater(X135,X136)|smaller_or_equal(X135,X136),inference(resolution,[status(thm)],[c46, c73])).
% 0.91/1.15 cnf(c198,plain,greater(X137,X138)|smaller_or_equal(X137,X138),inference(resolution,[status(thm)],[c112, c74])).
% 0.91/1.15 cnf(c220,plain,smaller_or_equal(X146,X147)|~greater(X147,X146),inference(resolution,[status(thm)],[c198, c52])).
% 0.91/1.15 cnf(c15,negated_conjecture,greater_or_equal(sigma,zero),inference(split_conjunct,[status(thm)],[c12])).
% 0.91/1.15 fof(definition_greater_or_equal,axiom,(![X]:(![Y]:(greater_or_equal(X,Y)<=>(greater(X,Y)|X=Y)))),file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax', definition_greater_or_equal)).
% 0.91/1.15 fof(c59,plain,(![X]:(![Y]:((~greater_or_equal(X,Y)|(greater(X,Y)|X=Y))&((~greater(X,Y)&X!=Y)|greater_or_equal(X,Y))))),inference(fof_nnf,[status(thm)],[definition_greater_or_equal])).
% 0.91/1.15 fof(c60,plain,((![X]:(![Y]:(~greater_or_equal(X,Y)|(greater(X,Y)|X=Y))))&(![X]:(![Y]:((~greater(X,Y)&X!=Y)|greater_or_equal(X,Y))))),inference(shift_quantors,[status(thm)],[c59])).
% 0.91/1.15 fof(c62,plain,(![X27]:(![X28]:(![X29]:(![X30]:((~greater_or_equal(X27,X28)|(greater(X27,X28)|X27=X28))&((~greater(X29,X30)&X29!=X30)|greater_or_equal(X29,X30))))))),inference(shift_quantors,[status(thm)],[fof(c61,plain,((![X27]:(![X28]:(~greater_or_equal(X27,X28)|(greater(X27,X28)|X27=X28))))&(![X29]:(![X30]:((~greater(X29,X30)&X29!=X30)|greater_or_equal(X29,X30))))),inference(variable_rename,[status(thm)],[c60])).])).
% 0.91/1.15 fof(c63,plain,(![X27]:(![X28]:(![X29]:(![X30]:((~greater_or_equal(X27,X28)|(greater(X27,X28)|X27=X28))&((~greater(X29,X30)|greater_or_equal(X29,X30))&(X29!=X30|greater_or_equal(X29,X30)))))))),inference(distribute,[status(thm)],[c62])).
% 0.91/1.15 cnf(c64,plain,~greater_or_equal(X98,X99)|greater(X98,X99)|X98=X99,inference(split_conjunct,[status(thm)],[c63])).
% 0.91/1.15 cnf(c128,plain,greater(sigma,zero)|sigma=zero,inference(resolution,[status(thm)],[c64, c15])).
% 0.91/1.15 cnf(c367,plain,sigma=zero|smaller_or_equal(zero,sigma),inference(resolution,[status(thm)],[c128, c220])).
% 0.91/1.15 cnf(c583,plain,smaller_or_equal(zero,sigma),inference(resolution,[status(thm)],[c367, c140])).
% 0.91/1.15 cnf(c589,plain,zero!=X748|sigma!=X749|smaller_or_equal(X748,X749),inference(resolution,[status(thm)],[c583, c1])).
% 0.91/1.15 cnf(c1994,plain,zero!=X750|smaller_or_equal(X750,sigma),inference(resolution,[status(thm)],[c589, reflexivity])).
% 0.91/1.15 cnf(c2004,plain,smaller_or_equal(age(skolem0001,skolem0002),sigma),inference(resolution,[status(thm)],[c1994, c94])).
% 0.91/1.15 cnf(c2011,plain,~fragile_position(skolem0001)|positional_advantage(skolem0001,skolem0002),inference(resolution,[status(thm)],[c2004, c39])).
% 0.91/1.15 cnf(c2015,plain,positional_advantage(skolem0001,skolem0002),inference(resolution,[status(thm)],[c2011, c17])).
% 0.91/1.15 fof(definition_4,axiom,(![X]:(robust_position(X)<=>(![T]:((smaller_or_equal(age(X,T),tau)=>(~positional_advantage(X,T)))&(greater(age(X,T),tau)=>positional_advantage(X,T)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', definition_4)).
% 0.91/1.15 fof(c19,plain,(![X]:(robust_position(X)<=>(![T]:((smaller_or_equal(age(X,T),tau)=>~positional_advantage(X,T))&(greater(age(X,T),tau)=>positional_advantage(X,T)))))),inference(fof_simplification,[status(thm)],[definition_4])).
% 0.91/1.16 fof(c20,plain,(![X]:((~robust_position(X)|(![T]:((~smaller_or_equal(age(X,T),tau)|~positional_advantage(X,T))&(~greater(age(X,T),tau)|positional_advantage(X,T)))))&((?[T]:((smaller_or_equal(age(X,T),tau)&positional_advantage(X,T))|(greater(age(X,T),tau)&~positional_advantage(X,T))))|robust_position(X)))),inference(fof_nnf,[status(thm)],[c19])).
% 0.91/1.16 fof(c21,plain,((![X]:(~robust_position(X)|((![T]:(~smaller_or_equal(age(X,T),tau)|~positional_advantage(X,T)))&(![T]:(~greater(age(X,T),tau)|positional_advantage(X,T))))))&(![X]:(((?[T]:(smaller_or_equal(age(X,T),tau)&positional_advantage(X,T)))|(?[T]:(greater(age(X,T),tau)&~positional_advantage(X,T))))|robust_position(X)))),inference(shift_quantors,[status(thm)],[c20])).
% 0.91/1.16 fof(c22,plain,((![X4]:(~robust_position(X4)|((![X5]:(~smaller_or_equal(age(X4,X5),tau)|~positional_advantage(X4,X5)))&(![X6]:(~greater(age(X4,X6),tau)|positional_advantage(X4,X6))))))&(![X7]:(((?[X8]:(smaller_or_equal(age(X7,X8),tau)&positional_advantage(X7,X8)))|(?[X9]:(greater(age(X7,X9),tau)&~positional_advantage(X7,X9))))|robust_position(X7)))),inference(variable_rename,[status(thm)],[c21])).
% 0.91/1.16 fof(c24,plain,(![X4]:(![X5]:(![X6]:(![X7]:((~robust_position(X4)|((~smaller_or_equal(age(X4,X5),tau)|~positional_advantage(X4,X5))&(~greater(age(X4,X6),tau)|positional_advantage(X4,X6))))&(((smaller_or_equal(age(X7,skolem0003(X7)),tau)&positional_advantage(X7,skolem0003(X7)))|(greater(age(X7,skolem0004(X7)),tau)&~positional_advantage(X7,skolem0004(X7))))|robust_position(X7))))))),inference(shift_quantors,[status(thm)],[fof(c23,plain,((![X4]:(~robust_position(X4)|((![X5]:(~smaller_or_equal(age(X4,X5),tau)|~positional_advantage(X4,X5)))&(![X6]:(~greater(age(X4,X6),tau)|positional_advantage(X4,X6))))))&(![X7]:(((smaller_or_equal(age(X7,skolem0003(X7)),tau)&positional_advantage(X7,skolem0003(X7)))|(greater(age(X7,skolem0004(X7)),tau)&~positional_advantage(X7,skolem0004(X7))))|robust_position(X7)))),inference(skolemize,[status(esa)],[c22])).])).
% 0.91/1.16 fof(c25,plain,(![X4]:(![X5]:(![X6]:(![X7]:(((~robust_position(X4)|(~smaller_or_equal(age(X4,X5),tau)|~positional_advantage(X4,X5)))&(~robust_position(X4)|(~greater(age(X4,X6),tau)|positional_advantage(X4,X6))))&((((smaller_or_equal(age(X7,skolem0003(X7)),tau)|greater(age(X7,skolem0004(X7)),tau))|robust_position(X7))&((smaller_or_equal(age(X7,skolem0003(X7)),tau)|~positional_advantage(X7,skolem0004(X7)))|robust_position(X7)))&(((positional_advantage(X7,skolem0003(X7))|greater(age(X7,skolem0004(X7)),tau))|robust_position(X7))&((positional_advantage(X7,skolem0003(X7))|~positional_advantage(X7,skolem0004(X7)))|robust_position(X7))))))))),inference(distribute,[status(thm)],[c24])).
% 0.91/1.16 cnf(c26,plain,~robust_position(X116)|~smaller_or_equal(age(X116,X117),tau)|~positional_advantage(X116,X117),inference(split_conjunct,[status(thm)],[c25])).
% 0.91/1.16 cnf(c16,negated_conjecture,greater_or_equal(tau,zero),inference(split_conjunct,[status(thm)],[c12])).
% 0.91/1.16 cnf(c129,plain,greater(tau,zero)|tau=zero,inference(resolution,[status(thm)],[c64, c16])).
% 0.91/1.16 cnf(c385,plain,tau=zero|smaller_or_equal(zero,tau),inference(resolution,[status(thm)],[c129, c220])).
% 0.91/1.16 cnf(c668,plain,smaller_or_equal(zero,tau),inference(resolution,[status(thm)],[c385, c140])).
% 0.91/1.16 cnf(c674,plain,zero!=X757|tau!=X758|smaller_or_equal(X757,X758),inference(resolution,[status(thm)],[c668, c1])).
% 0.91/1.16 cnf(c2187,plain,zero!=X759|smaller_or_equal(X759,tau),inference(resolution,[status(thm)],[c674, reflexivity])).
% 0.91/1.16 cnf(c2197,plain,smaller_or_equal(age(skolem0001,skolem0002),tau),inference(resolution,[status(thm)],[c2187, c94])).
% 0.91/1.16 cnf(c2203,plain,~robust_position(skolem0001)|~positional_advantage(skolem0001,skolem0002),inference(resolution,[status(thm)],[c2197, c26])).
% 0.91/1.16 cnf(c2233,plain,~robust_position(skolem0001),inference(resolution,[status(thm)],[c2203, c2015])).
% 0.91/1.16 cnf(c2235,plain,$false,inference(resolution,[status(thm)],[c2233, c18])).
% 0.91/1.16 % SZS output end CNFRefutation
% 0.91/1.16
% 0.91/1.16 % Initial clauses : 41
% 0.91/1.16 % Processed clauses : 227
% 0.91/1.16 % Factors computed : 36
% 0.91/1.16 % Resolvents computed: 2135
% 0.91/1.16 % Tautologies deleted: 17
% 0.91/1.16 % Forward subsumed : 358
% 0.91/1.16 % Backward subsumed : 12
% 0.91/1.16 % -------- CPU Time ---------
% 0.91/1.16 % User time : 0.706 s
% 0.91/1.16 % System time : 0.023 s
% 0.91/1.16 % Total time : 0.729 s
%------------------------------------------------------------------------------