%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT013+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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.56s 0.81s
% Output : CNFRefutation 0.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT013+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.10/0.35 % Computer : n013.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 7 11:50:50 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.41 (re.compile("\."), Token.FullStop),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.41 (re.compile("\("), Token.OpenPar),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.41 (re.compile("\)"), Token.ClosePar),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.41 (re.compile("\["), Token.OpenSquare),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.41 (re.compile("~\|"), Token.Nor),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.41 (re.compile("\|"), Token.Or),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.42 (re.compile("\?"), Token.Existential),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.21/0.48 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.48 """
% 0.21/0.49 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.49 """
% 0.32/0.58 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.58 """
% 0.56/0.81 % Version: 1.5
% 0.56/0.81 % SZS status Theorem
% 0.56/0.81 % SZS output start CNFRefutation
% 0.56/0.81 fof(t13_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(C2,C1))=>(~greater(S1,S2)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t13_FOL)).
% 0.56/0.81 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(C2,C1))=>(~greater(S1,S2))))))))))),inference(assume_negation,[status(cth)],[t13_FOL])).
% 0.56/0.81 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(C2,C1))=>~greater(S1,S2)))))))))),inference(fof_simplification,[status(thm)],[c6])).
% 0.56/0.81 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(C2,C1))&greater(S1,S2))))))))),inference(fof_nnf,[status(thm)],[c7])).
% 0.56/0.81 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(C2,C1))&greater(S1,S2))))))),inference(shift_quantors,[status(thm)],[c8])).
% 0.56/0.81 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(X4,X3))&greater(X5,X6))))))),inference(variable_rename,[status(thm)],[c9])).
% 0.56/0.81 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(skolem0003,skolem0002))&greater(skolem0004,skolem0005)),inference(skolemize,[status(esa)],[c10])).
% 0.56/0.81 cnf(c12,negated_conjecture,organization(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c11])).
% 0.56/0.81 cnf(c13,negated_conjecture,organization(skolem0001,skolem0007),inference(split_conjunct,[status(thm)],[c11])).
% 0.56/0.81 cnf(c19,negated_conjecture,greater(skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c11])).
% 0.56/0.81 fof(mp6_1,axiom,(![X]:(![Y]:(~(greater(X,Y)&X=Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp6_1)).
% 0.56/0.81 fof(c50,plain,(![X]:(![Y]:(~greater(X,Y)|X!=Y))),inference(fof_nnf,[status(thm)],[mp6_1])).
% 0.56/0.81 fof(c51,plain,(![X33]:(![X34]:(~greater(X33,X34)|X33!=X34))),inference(variable_rename,[status(thm)],[c50])).
% 0.56/0.81 cnf(c52,plain,~greater(X51,X52)|X51!=X52,inference(split_conjunct,[status(thm)],[c51])).
% 0.56/0.81 cnf(symmetry,axiom,X37!=X36|X36=X37,theory(equality)).
% 0.56/0.81 cnf(c15,negated_conjecture,complexity(skolem0001,skolem0002,skolem0006),inference(split_conjunct,[status(thm)],[c11])).
% 0.56/0.81 cnf(c16,negated_conjecture,complexity(skolem0001,skolem0003,skolem0007),inference(split_conjunct,[status(thm)],[c11])).
% 0.56/0.81 fof(mp18,axiom,(![X]:(![C1]:(![C2]:(![T1]:(![T2]:(((((organization(X,T1)&organization(X,T2))&complexity(X,C1,T1))&complexity(X,C2,T2))&T1=T2)=>C1=C2)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp18)).
% 0.56/0.81 fof(c33,plain,(![X]:(![C1]:(![C2]:(![T1]:(![T2]:(((((~organization(X,T1)|~organization(X,T2))|~complexity(X,C1,T1))|~complexity(X,C2,T2))|T1!=T2)|C1=C2)))))),inference(fof_nnf,[status(thm)],[mp18])).
% 0.56/0.81 fof(c34,plain,(![X]:(![C1]:(![C2]:((![T1]:(![T2]:((((~organization(X,T1)|~organization(X,T2))|~complexity(X,C1,T1))|~complexity(X,C2,T2))|T1!=T2)))|C1=C2)))),inference(shift_quantors,[status(thm)],[c33])).
% 0.56/0.81 fof(c36,plain,(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(((((~organization(X19,X22)|~organization(X19,X23))|~complexity(X19,X20,X22))|~complexity(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))|~complexity(X19,X20,X22))|~complexity(X19,X21,X23))|X22!=X23)))|X20=X21)))),inference(variable_rename,[status(thm)],[c34])).])).
% 0.56/0.81 cnf(c37,plain,~organization(X112,X113)|~organization(X112,X115)|~complexity(X112,X116,X113)|~complexity(X112,X114,X115)|X113!=X115|X116=X114,inference(split_conjunct,[status(thm)],[c36])).
% 0.56/0.81 cnf(c116,plain,~organization(skolem0001,X190)|~organization(skolem0001,skolem0007)|~complexity(skolem0001,X191,X190)|X190!=skolem0007|X191=skolem0003,inference(resolution,[status(thm)],[c37, c16])).
% 0.56/0.81 cnf(c188,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|skolem0006!=skolem0007|skolem0002=skolem0003,inference(resolution,[status(thm)],[c116, c15])).
% 0.56/0.81 fof(mp15,axiom,(![X]:(![T]:(organization(X,T)=>time(T)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp15)).
% 0.56/0.81 fof(c44,plain,(![X]:(![T]:(~organization(X,T)|time(T)))),inference(fof_nnf,[status(thm)],[mp15])).
% 0.56/0.81 fof(c45,plain,(![X29]:(![X30]:(~organization(X29,X30)|time(X30)))),inference(variable_rename,[status(thm)],[c44])).
% 0.56/0.81 cnf(c46,plain,~organization(X39,X40)|time(X40),inference(split_conjunct,[status(thm)],[c45])).
% 0.56/0.81 cnf(c54,plain,time(skolem0006),inference(resolution,[status(thm)],[c46, c12])).
% 0.56/0.81 cnf(c55,plain,time(skolem0007),inference(resolution,[status(thm)],[c46, c13])).
% 0.56/0.81 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.56/0.81 fof(c41,plain,(![T1]:(![T2]:((~time(T1)|~time(T2))|((greater(T1,T2)|T1=T2)|greater(T2,T1))))),inference(fof_nnf,[status(thm)],[mp16])).
% 0.56/0.81 fof(c42,plain,(![X27]:(![X28]:((~time(X27)|~time(X28))|((greater(X27,X28)|X27=X28)|greater(X28,X27))))),inference(variable_rename,[status(thm)],[c41])).
% 0.56/0.81 cnf(c43,plain,~time(X98)|~time(X97)|greater(X98,X97)|X98=X97|greater(X97,X98),inference(split_conjunct,[status(thm)],[c42])).
% 0.56/0.81 cnf(c85,plain,~time(X106)|greater(X106,skolem0007)|X106=skolem0007|greater(skolem0007,X106),inference(resolution,[status(thm)],[c43, c55])).
% 0.56/0.81 cnf(c91,plain,greater(skolem0006,skolem0007)|skolem0006=skolem0007|greater(skolem0007,skolem0006),inference(resolution,[status(thm)],[c85, c54])).
% 0.56/0.81 cnf(c14,negated_conjecture,reorganization_free(skolem0001,skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c11])).
% 0.56/0.81 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.56/0.81 fof(c38,plain,(![X]:(![T1]:(![T2]:(~reorganization_free(X,T1,T2)|reorganization_free(X,T2,T1))))),inference(fof_nnf,[status(thm)],[mp17])).
% 0.56/0.81 fof(c39,plain,(![X24]:(![X25]:(![X26]:(~reorganization_free(X24,X25,X26)|reorganization_free(X24,X26,X25))))),inference(variable_rename,[status(thm)],[c38])).
% 0.56/0.81 cnf(c40,plain,~reorganization_free(X66,X64,X65)|reorganization_free(X66,X65,X64),inference(split_conjunct,[status(thm)],[c39])).
% 0.56/0.81 cnf(c67,plain,reorganization_free(skolem0001,skolem0007,skolem0006),inference(resolution,[status(thm)],[c40, c14])).
% 0.56/0.81 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.56/0.81 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.56/0.81 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.56/0.81 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.56/0.81 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.56/0.81 cnf(c26,plain,~organization(X103,X102)|~organization(X103,X101)|~reorganization_free(X103,X102,X101)|~complexity(X103,X100,X102)|~complexity(X103,X99,X101)|~greater(X101,X102)|~greater(X100,X99),inference(split_conjunct,[status(thm)],[c25])).
% 0.56/0.81 cnf(c87,plain,~organization(skolem0001,X163)|~organization(skolem0001,skolem0006)|~reorganization_free(skolem0001,X163,skolem0006)|~complexity(skolem0001,X164,X163)|~greater(skolem0006,X163)|~greater(X164,skolem0002),inference(resolution,[status(thm)],[c26, c15])).
% 0.56/0.81 cnf(c146,plain,~organization(skolem0001,skolem0007)|~organization(skolem0001,skolem0006)|~reorganization_free(skolem0001,skolem0007,skolem0006)|~greater(skolem0006,skolem0007)|~greater(skolem0003,skolem0002),inference(resolution,[status(thm)],[c87, c16])).
% 0.56/0.81 cnf(c241,plain,~organization(skolem0001,skolem0007)|~organization(skolem0001,skolem0006)|~greater(skolem0006,skolem0007)|~greater(skolem0003,skolem0002),inference(resolution,[status(thm)],[c146, c67])).
% 0.56/0.81 cnf(c242,plain,~organization(skolem0001,skolem0007)|~organization(skolem0001,skolem0006)|~greater(skolem0006,skolem0007),inference(resolution,[status(thm)],[c241, c19])).
% 0.56/0.81 cnf(c245,plain,~organization(skolem0001,skolem0007)|~organization(skolem0001,skolem0006)|skolem0006=skolem0007|greater(skolem0007,skolem0006),inference(resolution,[status(thm)],[c242, c91])).
% 0.56/0.81 cnf(c251,plain,~organization(skolem0001,skolem0007)|skolem0006=skolem0007|greater(skolem0007,skolem0006),inference(resolution,[status(thm)],[c245, c12])).
% 0.56/0.81 cnf(c252,plain,skolem0006=skolem0007|greater(skolem0007,skolem0006),inference(resolution,[status(thm)],[c251, c13])).
% 0.56/0.81 cnf(c254,plain,greater(skolem0007,skolem0006)|~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|skolem0002=skolem0003,inference(resolution,[status(thm)],[c252, c188])).
% 0.56/0.81 cnf(c415,plain,greater(skolem0007,skolem0006)|~organization(skolem0001,skolem0006)|skolem0002=skolem0003,inference(resolution,[status(thm)],[c254, c13])).
% 0.56/0.81 cnf(c420,plain,greater(skolem0007,skolem0006)|skolem0002=skolem0003,inference(resolution,[status(thm)],[c415, c12])).
% 0.56/0.81 cnf(c425,plain,greater(skolem0007,skolem0006)|skolem0003=skolem0002,inference(resolution,[status(thm)],[c420, symmetry])).
% 0.56/0.81 cnf(c434,plain,greater(skolem0007,skolem0006)|~greater(skolem0003,skolem0002),inference(resolution,[status(thm)],[c425, c52])).
% 0.56/0.81 cnf(c439,plain,greater(skolem0007,skolem0006),inference(resolution,[status(thm)],[c434, c19])).
% 0.56/0.81 cnf(c20,negated_conjecture,greater(skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c11])).
% 0.56/0.81 cnf(c17,negated_conjecture,size(skolem0001,skolem0004,skolem0006),inference(split_conjunct,[status(thm)],[c11])).
% 0.56/0.81 cnf(c18,negated_conjecture,size(skolem0001,skolem0005,skolem0007),inference(split_conjunct,[status(thm)],[c11])).
% 0.56/0.81 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.56/0.81 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.56/0.81 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.56/0.81 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.56/0.81 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.56/0.81 cnf(c32,plain,~organization(X109,X111)|~organization(X109,X110)|~reorganization_free(X109,X111,X110)|~size(X109,X107,X111)|~size(X109,X108,X110)|~greater(X110,X111)|~greater(X107,X108),inference(split_conjunct,[status(thm)],[c31])).
% 0.56/0.81 cnf(c95,plain,~organization(skolem0001,X174)|~organization(skolem0001,skolem0007)|~reorganization_free(skolem0001,X174,skolem0007)|~size(skolem0001,X175,X174)|~greater(skolem0007,X174)|~greater(X175,skolem0005),inference(resolution,[status(thm)],[c32, c18])).
% 0.56/0.81 cnf(c167,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|~reorganization_free(skolem0001,skolem0006,skolem0007)|~greater(skolem0007,skolem0006)|~greater(skolem0004,skolem0005),inference(resolution,[status(thm)],[c95, c17])).
% 0.56/0.81 cnf(c363,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|~greater(skolem0007,skolem0006)|~greater(skolem0004,skolem0005),inference(resolution,[status(thm)],[c167, c14])).
% 0.56/0.81 cnf(c444,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|~greater(skolem0007,skolem0006),inference(resolution,[status(thm)],[c363, c20])).
% 0.56/0.81 cnf(c445,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007),inference(resolution,[status(thm)],[c444, c439])).
% 0.56/0.81 cnf(c446,plain,~organization(skolem0001,skolem0006),inference(resolution,[status(thm)],[c445, c13])).
% 0.56/0.81 cnf(c447,plain,$false,inference(resolution,[status(thm)],[c446, c12])).
% 0.56/0.81 % SZS output end CNFRefutation
% 0.56/0.81
% 0.56/0.81 % Initial clauses : 26
% 0.56/0.81 % Processed clauses : 177
% 0.56/0.81 % Factors computed : 8
% 0.56/0.81 % Resolvents computed: 387
% 0.56/0.81 % Tautologies deleted: 24
% 0.56/0.81 % Forward subsumed : 147
% 0.56/0.81 % Backward subsumed : 109
% 0.56/0.81 % -------- CPU Time ---------
% 0.56/0.81 % User time : 0.443 s
% 0.56/0.81 % System time : 0.015 s
% 0.56/0.81 % Total time : 0.458 s
%------------------------------------------------------------------------------