%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT014+1 : TPTP v9.3.0. Released v2.0.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:39 AM UTC 2026
% Result : Theorem 0.26s 0.56s
% Output : CNFRefutation 0.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT014+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.06/0.34 % Computer : n028.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Mon Sep 7 11:55:02 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.06/0.37 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.06/0.37 (re.compile("\."), Token.FullStop),
% 0.06/0.37 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.06/0.37 (re.compile("\("), Token.OpenPar),
% 0.06/0.37 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.06/0.37 (re.compile("\)"), Token.ClosePar),
% 0.06/0.37 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.06/0.37 (re.compile("\["), Token.OpenSquare),
% 0.06/0.37 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.06/0.37 (re.compile("\]"), Token.CloseSquare),
% 0.06/0.37 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.06/0.37 (re.compile("~\|"), Token.Nor),
% 0.06/0.37 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.06/0.37 (re.compile("\|"), Token.Or),
% 0.06/0.37 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.06/0.37 (re.compile("\?"), Token.Existential),
% 0.06/0.37 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.06/0.37 (re.compile("\s+"), Token.WhiteSpace),
% 0.06/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.06/0.38 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.16/0.41 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.16/0.41 """
% 0.16/0.41 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.16/0.41 """
% 0.16/0.45 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.16/0.45 """
% 0.26/0.56 % Version: 1.5
% 0.26/0.56 % SZS status Theorem
% 0.26/0.56 % SZS output start CNFRefutation
% 0.26/0.56 fof(t14_FOL,conjecture,(![X]:(![C1]:(![C2]:(![S1]:(![S2]:(![T1]:(![T2]:((((((((organization(X,T1)&organization(X,T2))&reorganization_free(X,T1,T2))&complexity(X,C1,T1))&complexity(X,C2,T2))&size(X,S1,T1))&size(X,S2,T2))&greater(S2,S1))=>(~greater(C1,C2)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t14_FOL)).
% 0.26/0.56 fof(c6,negated_conjecture,(~(![X]:(![C1]:(![C2]:(![S1]:(![S2]:(![T1]:(![T2]:((((((((organization(X,T1)&organization(X,T2))&reorganization_free(X,T1,T2))&complexity(X,C1,T1))&complexity(X,C2,T2))&size(X,S1,T1))&size(X,S2,T2))&greater(S2,S1))=>(~greater(C1,C2))))))))))),inference(assume_negation,[status(cth)],[t14_FOL])).
% 0.26/0.56 fof(c7,negated_conjecture,(~(![X]:(![C1]:(![C2]:(![S1]:(![S2]:(![T1]:(![T2]:((((((((organization(X,T1)&organization(X,T2))&reorganization_free(X,T1,T2))&complexity(X,C1,T1))&complexity(X,C2,T2))&size(X,S1,T1))&size(X,S2,T2))&greater(S2,S1))=>~greater(C1,C2)))))))))),inference(fof_simplification,[status(thm)],[c6])).
% 0.26/0.56 fof(c8,negated_conjecture,(?[X]:(?[C1]:(?[C2]:(?[S1]:(?[S2]:(?[T1]:(?[T2]:((((((((organization(X,T1)&organization(X,T2))&reorganization_free(X,T1,T2))&complexity(X,C1,T1))&complexity(X,C2,T2))&size(X,S1,T1))&size(X,S2,T2))&greater(S2,S1))&greater(C1,C2))))))))),inference(fof_nnf,[status(thm)],[c7])).
% 0.26/0.56 fof(c9,negated_conjecture,(?[X]:(?[C1]:(?[C2]:((?[S1]:(?[S2]:((?[T1]:(?[T2]:((((((organization(X,T1)&organization(X,T2))&reorganization_free(X,T1,T2))&complexity(X,C1,T1))&complexity(X,C2,T2))&size(X,S1,T1))&size(X,S2,T2))))&greater(S2,S1))))&greater(C1,C2))))),inference(shift_quantors,[status(thm)],[c8])).
% 0.26/0.56 fof(c10,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((?[X5]:(?[X6]:((?[X7]:(?[X8]:((((((organization(X2,X7)&organization(X2,X8))&reorganization_free(X2,X7,X8))&complexity(X2,X3,X7))&complexity(X2,X4,X8))&size(X2,X5,X7))&size(X2,X6,X8))))&greater(X6,X5))))&greater(X3,X4))))),inference(variable_rename,[status(thm)],[c9])).
% 0.26/0.56 fof(c11,negated_conjecture,((((((((organization(skolem0001,skolem0006)&organization(skolem0001,skolem0007))&reorganization_free(skolem0001,skolem0006,skolem0007))&complexity(skolem0001,skolem0002,skolem0006))&complexity(skolem0001,skolem0003,skolem0007))&size(skolem0001,skolem0004,skolem0006))&size(skolem0001,skolem0005,skolem0007))&greater(skolem0005,skolem0004))&greater(skolem0002,skolem0003)),inference(skolemize,[status(esa)],[c10])).
% 0.26/0.56 cnf(c13,negated_conjecture,organization(skolem0001,skolem0007),inference(split_conjunct,[status(thm)],[c11])).
% 0.26/0.56 cnf(c12,negated_conjecture,organization(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c11])).
% 0.26/0.56 cnf(c19,negated_conjecture,greater(skolem0005,skolem0004),inference(split_conjunct,[status(thm)],[c11])).
% 0.26/0.56 fof(mp6_1,axiom,(![X]:(![Y]:(~(greater(X,Y)&X=Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp6_1)).
% 0.26/0.56 fof(c50,plain,(![X]:(![Y]:(~greater(X,Y)|X!=Y))),inference(fof_nnf,[status(thm)],[mp6_1])).
% 0.26/0.56 fof(c51,plain,(![X33]:(![X34]:(~greater(X33,X34)|X33!=X34))),inference(variable_rename,[status(thm)],[c50])).
% 0.26/0.56 cnf(c52,plain,~greater(X51,X52)|X51!=X52,inference(split_conjunct,[status(thm)],[c51])).
% 0.26/0.56 cnf(symmetry,axiom,X37!=X36|X36=X37,theory(equality)).
% 0.26/0.56 cnf(c17,negated_conjecture,size(skolem0001,skolem0004,skolem0006),inference(split_conjunct,[status(thm)],[c11])).
% 0.26/0.56 cnf(c18,negated_conjecture,size(skolem0001,skolem0005,skolem0007),inference(split_conjunct,[status(thm)],[c11])).
% 0.26/0.56 fof(mp19,axiom,(![X]:(![S1]:(![S2]:(![T1]:(![T2]:(((((organization(X,T1)&organization(X,T2))&size(X,S1,T1))&size(X,S2,T2))&T1=T2)=>S1=S2)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp19)).
% 0.26/0.56 fof(c33,plain,(![X]:(![S1]:(![S2]:(![T1]:(![T2]:(((((~organization(X,T1)|~organization(X,T2))|~size(X,S1,T1))|~size(X,S2,T2))|T1!=T2)|S1=S2)))))),inference(fof_nnf,[status(thm)],[mp19])).
% 0.26/0.56 fof(c34,plain,(![X]:(![S1]:(![S2]:((![T1]:(![T2]:((((~organization(X,T1)|~organization(X,T2))|~size(X,S1,T1))|~size(X,S2,T2))|T1!=T2)))|S1=S2)))),inference(shift_quantors,[status(thm)],[c33])).
% 0.26/0.56 fof(c36,plain,(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(((((~organization(X19,X22)|~organization(X19,X23))|~size(X19,X20,X22))|~size(X19,X21,X23))|X22!=X23)|X20=X21)))))),inference(shift_quantors,[status(thm)],[fof(c35,plain,(![X19]:(![X20]:(![X21]:((![X22]:(![X23]:((((~organization(X19,X22)|~organization(X19,X23))|~size(X19,X20,X22))|~size(X19,X21,X23))|X22!=X23)))|X20=X21)))),inference(variable_rename,[status(thm)],[c34])).])).
% 0.26/0.56 cnf(c37,plain,~organization(X112,X113)|~organization(X112,X116)|~size(X112,X114,X113)|~size(X112,X115,X116)|X113!=X116|X114=X115,inference(split_conjunct,[status(thm)],[c36])).
% 0.26/0.56 cnf(c116,plain,~organization(skolem0001,X190)|~organization(skolem0001,skolem0007)|~size(skolem0001,X191,X190)|X190!=skolem0007|X191=skolem0005,inference(resolution,[status(thm)],[c37, c18])).
% 0.26/0.56 cnf(c188,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|skolem0006!=skolem0007|skolem0004=skolem0005,inference(resolution,[status(thm)],[c116, c17])).
% 0.26/0.56 fof(mp15,axiom,(![X]:(![T]:(organization(X,T)=>time(T)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp15)).
% 0.26/0.56 fof(c44,plain,(![X]:(![T]:(~organization(X,T)|time(T)))),inference(fof_nnf,[status(thm)],[mp15])).
% 0.26/0.56 fof(c45,plain,(![X29]:(![X30]:(~organization(X29,X30)|time(X30)))),inference(variable_rename,[status(thm)],[c44])).
% 0.26/0.56 cnf(c46,plain,~organization(X40,X39)|time(X39),inference(split_conjunct,[status(thm)],[c45])).
% 0.26/0.56 cnf(c54,plain,time(skolem0006),inference(resolution,[status(thm)],[c46, c12])).
% 0.26/0.56 cnf(c55,plain,time(skolem0007),inference(resolution,[status(thm)],[c46, c13])).
% 0.26/0.56 fof(mp16,axiom,(![T1]:(![T2]:((time(T1)&time(T2))=>((greater(T1,T2)|T1=T2)|greater(T2,T1))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp16)).
% 0.26/0.56 fof(c41,plain,(![T1]:(![T2]:((~time(T1)|~time(T2))|((greater(T1,T2)|T1=T2)|greater(T2,T1))))),inference(fof_nnf,[status(thm)],[mp16])).
% 0.26/0.56 fof(c42,plain,(![X27]:(![X28]:((~time(X27)|~time(X28))|((greater(X27,X28)|X27=X28)|greater(X28,X27))))),inference(variable_rename,[status(thm)],[c41])).
% 0.26/0.56 cnf(c43,plain,~time(X97)|~time(X98)|greater(X97,X98)|X97=X98|greater(X98,X97),inference(split_conjunct,[status(thm)],[c42])).
% 0.26/0.56 cnf(c85,plain,~time(X106)|greater(X106,skolem0007)|X106=skolem0007|greater(skolem0007,X106),inference(resolution,[status(thm)],[c43, c55])).
% 0.26/0.56 cnf(c91,plain,greater(skolem0006,skolem0007)|skolem0006=skolem0007|greater(skolem0007,skolem0006),inference(resolution,[status(thm)],[c85, c54])).
% 0.26/0.56 cnf(c20,negated_conjecture,greater(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c11])).
% 0.26/0.56 cnf(c14,negated_conjecture,reorganization_free(skolem0001,skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c11])).
% 0.26/0.56 cnf(c15,negated_conjecture,complexity(skolem0001,skolem0002,skolem0006),inference(split_conjunct,[status(thm)],[c11])).
% 0.26/0.56 cnf(c16,negated_conjecture,complexity(skolem0001,skolem0003,skolem0007),inference(split_conjunct,[status(thm)],[c11])).
% 0.26/0.56 fof(t12_FOL,plain,(![X]:(![C1]:(![C2]:(![T1]:(![T2]:((((((organization(X,T1)&organization(X,T2))&reorganization_free(X,T1,T2))&complexity(X,C1,T1))&complexity(X,C2,T2))&greater(T2,T1))=>(~greater(C1,C2)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t12_FOL)).
% 0.26/0.56 fof(c21,plain,(![X]:(![C1]:(![C2]:(![T1]:(![T2]:((((((organization(X,T1)&organization(X,T2))&reorganization_free(X,T1,T2))&complexity(X,C1,T1))&complexity(X,C2,T2))&greater(T2,T1))=>~greater(C1,C2))))))),inference(fof_simplification,[status(thm)],[t12_FOL])).
% 0.26/0.56 fof(c22,plain,(![X]:(![C1]:(![C2]:(![T1]:(![T2]:((((((~organization(X,T1)|~organization(X,T2))|~reorganization_free(X,T1,T2))|~complexity(X,C1,T1))|~complexity(X,C2,T2))|~greater(T2,T1))|~greater(C1,C2))))))),inference(fof_nnf,[status(thm)],[c21])).
% 0.26/0.56 fof(c23,plain,(![X]:(![C1]:(![C2]:((![T1]:(![T2]:(((((~organization(X,T1)|~organization(X,T2))|~reorganization_free(X,T1,T2))|~complexity(X,C1,T1))|~complexity(X,C2,T2))|~greater(T2,T1))))|~greater(C1,C2))))),inference(shift_quantors,[status(thm)],[c22])).
% 0.26/0.56 fof(c25,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:((((((~organization(X9,X12)|~organization(X9,X13))|~reorganization_free(X9,X12,X13))|~complexity(X9,X10,X12))|~complexity(X9,X11,X13))|~greater(X13,X12))|~greater(X10,X11))))))),inference(shift_quantors,[status(thm)],[fof(c24,plain,(![X9]:(![X10]:(![X11]:((![X12]:(![X13]:(((((~organization(X9,X12)|~organization(X9,X13))|~reorganization_free(X9,X12,X13))|~complexity(X9,X10,X12))|~complexity(X9,X11,X13))|~greater(X13,X12))))|~greater(X10,X11))))),inference(variable_rename,[status(thm)],[c23])).])).
% 0.26/0.56 cnf(c26,plain,~organization(X102,X99)|~organization(X102,X100)|~reorganization_free(X102,X99,X100)|~complexity(X102,X101,X99)|~complexity(X102,X103,X100)|~greater(X100,X99)|~greater(X101,X103),inference(split_conjunct,[status(thm)],[c25])).
% 0.26/0.56 cnf(c88,plain,~organization(skolem0001,X168)|~organization(skolem0001,skolem0007)|~reorganization_free(skolem0001,X168,skolem0007)|~complexity(skolem0001,X167,X168)|~greater(skolem0007,X168)|~greater(X167,skolem0003),inference(resolution,[status(thm)],[c26, c16])).
% 0.26/0.56 cnf(c149,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|~reorganization_free(skolem0001,skolem0006,skolem0007)|~greater(skolem0007,skolem0006)|~greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c88, c15])).
% 0.26/0.56 cnf(c245,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|~greater(skolem0007,skolem0006)|~greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c149, c14])).
% 0.26/0.56 cnf(c246,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|~greater(skolem0007,skolem0006),inference(resolution,[status(thm)],[c245, c20])).
% 0.26/0.56 cnf(c251,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|greater(skolem0006,skolem0007)|skolem0006=skolem0007,inference(resolution,[status(thm)],[c246, c91])).
% 0.26/0.56 cnf(c255,plain,~organization(skolem0001,skolem0006)|greater(skolem0006,skolem0007)|skolem0006=skolem0007,inference(resolution,[status(thm)],[c251, c13])).
% 0.26/0.56 cnf(c256,plain,greater(skolem0006,skolem0007)|skolem0006=skolem0007,inference(resolution,[status(thm)],[c255, c12])).
% 0.26/0.56 cnf(c265,plain,greater(skolem0006,skolem0007)|~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|skolem0004=skolem0005,inference(resolution,[status(thm)],[c256, c188])).
% 0.26/0.56 cnf(c424,plain,greater(skolem0006,skolem0007)|~organization(skolem0001,skolem0006)|skolem0004=skolem0005,inference(resolution,[status(thm)],[c265, c13])).
% 0.26/0.56 cnf(c425,plain,greater(skolem0006,skolem0007)|skolem0004=skolem0005,inference(resolution,[status(thm)],[c424, c12])).
% 0.26/0.56 cnf(c434,plain,greater(skolem0006,skolem0007)|skolem0005=skolem0004,inference(resolution,[status(thm)],[c425, symmetry])).
% 0.26/0.56 cnf(c438,plain,greater(skolem0006,skolem0007)|~greater(skolem0005,skolem0004),inference(resolution,[status(thm)],[c434, c52])).
% 0.26/0.56 cnf(c444,plain,greater(skolem0006,skolem0007),inference(resolution,[status(thm)],[c438, c19])).
% 0.26/0.56 fof(mp17,axiom,(![X]:(![T1]:(![T2]:(reorganization_free(X,T1,T2)=>reorganization_free(X,T2,T1))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp17)).
% 0.26/0.56 fof(c38,plain,(![X]:(![T1]:(![T2]:(~reorganization_free(X,T1,T2)|reorganization_free(X,T2,T1))))),inference(fof_nnf,[status(thm)],[mp17])).
% 0.26/0.56 fof(c39,plain,(![X24]:(![X25]:(![X26]:(~reorganization_free(X24,X25,X26)|reorganization_free(X24,X26,X25))))),inference(variable_rename,[status(thm)],[c38])).
% 0.26/0.56 cnf(c40,plain,~reorganization_free(X65,X64,X66)|reorganization_free(X65,X66,X64),inference(split_conjunct,[status(thm)],[c39])).
% 0.26/0.56 cnf(c67,plain,reorganization_free(skolem0001,skolem0007,skolem0006),inference(resolution,[status(thm)],[c40, c14])).
% 0.26/0.56 fof(t11_FOL,plain,(![X]:(![S1]:(![S2]:(![T1]:(![T2]:((((((organization(X,T1)&organization(X,T2))&reorganization_free(X,T1,T2))&size(X,S1,T1))&size(X,S2,T2))&greater(T2,T1))=>(~greater(S1,S2)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t11_FOL)).
% 0.26/0.56 fof(c27,plain,(![X]:(![S1]:(![S2]:(![T1]:(![T2]:((((((organization(X,T1)&organization(X,T2))&reorganization_free(X,T1,T2))&size(X,S1,T1))&size(X,S2,T2))&greater(T2,T1))=>~greater(S1,S2))))))),inference(fof_simplification,[status(thm)],[t11_FOL])).
% 0.26/0.56 fof(c28,plain,(![X]:(![S1]:(![S2]:(![T1]:(![T2]:((((((~organization(X,T1)|~organization(X,T2))|~reorganization_free(X,T1,T2))|~size(X,S1,T1))|~size(X,S2,T2))|~greater(T2,T1))|~greater(S1,S2))))))),inference(fof_nnf,[status(thm)],[c27])).
% 0.26/0.56 fof(c29,plain,(![X]:(![S1]:(![S2]:((![T1]:(![T2]:(((((~organization(X,T1)|~organization(X,T2))|~reorganization_free(X,T1,T2))|~size(X,S1,T1))|~size(X,S2,T2))|~greater(T2,T1))))|~greater(S1,S2))))),inference(shift_quantors,[status(thm)],[c28])).
% 0.26/0.56 fof(c31,plain,(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:((((((~organization(X14,X17)|~organization(X14,X18))|~reorganization_free(X14,X17,X18))|~size(X14,X15,X17))|~size(X14,X16,X18))|~greater(X18,X17))|~greater(X15,X16))))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,(![X14]:(![X15]:(![X16]:((![X17]:(![X18]:(((((~organization(X14,X17)|~organization(X14,X18))|~reorganization_free(X14,X17,X18))|~size(X14,X15,X17))|~size(X14,X16,X18))|~greater(X18,X17))))|~greater(X15,X16))))),inference(variable_rename,[status(thm)],[c29])).])).
% 0.26/0.56 cnf(c32,plain,~organization(X107,X108)|~organization(X107,X109)|~reorganization_free(X107,X108,X109)|~size(X107,X111,X108)|~size(X107,X110,X109)|~greater(X109,X108)|~greater(X111,X110),inference(split_conjunct,[status(thm)],[c31])).
% 0.26/0.56 cnf(c94,plain,~organization(skolem0001,X171)|~organization(skolem0001,skolem0006)|~reorganization_free(skolem0001,X171,skolem0006)|~size(skolem0001,X172,X171)|~greater(skolem0006,X171)|~greater(X172,skolem0004),inference(resolution,[status(thm)],[c32, c17])).
% 0.26/0.56 cnf(c159,plain,~organization(skolem0001,skolem0007)|~organization(skolem0001,skolem0006)|~reorganization_free(skolem0001,skolem0007,skolem0006)|~greater(skolem0006,skolem0007)|~greater(skolem0005,skolem0004),inference(resolution,[status(thm)],[c94, c18])).
% 0.26/0.56 cnf(c327,plain,~organization(skolem0001,skolem0007)|~organization(skolem0001,skolem0006)|~greater(skolem0006,skolem0007)|~greater(skolem0005,skolem0004),inference(resolution,[status(thm)],[c159, c67])).
% 0.26/0.56 cnf(c449,plain,~organization(skolem0001,skolem0007)|~organization(skolem0001,skolem0006)|~greater(skolem0006,skolem0007),inference(resolution,[status(thm)],[c327, c19])).
% 0.26/0.56 cnf(c450,plain,~organization(skolem0001,skolem0007)|~organization(skolem0001,skolem0006),inference(resolution,[status(thm)],[c449, c444])).
% 0.26/0.56 cnf(c451,plain,~organization(skolem0001,skolem0007),inference(resolution,[status(thm)],[c450, c12])).
% 0.26/0.56 cnf(c452,plain,$false,inference(resolution,[status(thm)],[c451, c13])).
% 0.26/0.56 % SZS output end CNFRefutation
% 0.26/0.56
% 0.26/0.56 % Initial clauses : 26
% 0.26/0.56 % Processed clauses : 178
% 0.26/0.56 % Factors computed : 8
% 0.26/0.56 % Resolvents computed: 392
% 0.26/0.56 % Tautologies deleted: 24
% 0.26/0.56 % Forward subsumed : 146
% 0.26/0.56 % Backward subsumed : 110
% 0.26/0.56 % -------- CPU Time ---------
% 0.26/0.56 % User time : 0.202 s
% 0.26/0.56 % System time : 0.015 s
% 0.26/0.56 % Total time : 0.217 s
%------------------------------------------------------------------------------