%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT006+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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:37 AM UTC 2026
% Result : Theorem 0.24s 0.51s
% Output : CNFRefutation 0.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT006+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.36 % Computer : n004.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 11:41:45 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.40 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.14/0.40 (re.compile("\."), Token.FullStop),
% 0.14/0.40 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.14/0.40 (re.compile("\("), Token.OpenPar),
% 0.14/0.40 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.14/0.40 (re.compile("\)"), Token.ClosePar),
% 0.14/0.40 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.14/0.40 (re.compile("\["), Token.OpenSquare),
% 0.14/0.40 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.14/0.40 (re.compile("\]"), Token.CloseSquare),
% 0.14/0.40 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.14/0.40 (re.compile("~\|"), Token.Nor),
% 0.14/0.40 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.14/0.40 (re.compile("\|"), Token.Or),
% 0.14/0.40 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.14/0.40 (re.compile("\?"), Token.Existential),
% 0.14/0.40 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.14/0.40 (re.compile("\s+"), Token.WhiteSpace),
% 0.14/0.40 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.14/0.40 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.14/0.43 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.14/0.43 """
% 0.14/0.43 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.14/0.43 """
% 0.14/0.47 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.14/0.47 """
% 0.24/0.51 % Version: 1.5
% 0.24/0.51 % SZS status Theorem
% 0.24/0.51 % SZS output start CNFRefutation
% 0.24/0.51 fof(t6_FOL,conjecture,(![X]:(![R1]:(![R2]:(![A1]:(![A2]:(![T1]:(![T2]:((((((((organization(X,T1)&organization(X,T2))&reorganization_free(X,T1,T2))&reliability(X,R1,T1))&reliability(X,R2,T2))&accountability(X,A1,T1))&accountability(X,A2,T2))&greater(T2,T1))=>(greater(R2,R1)&greater(A2,A1)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t6_FOL)).
% 0.24/0.51 fof(c0,negated_conjecture,(~(![X]:(![R1]:(![R2]:(![A1]:(![A2]:(![T1]:(![T2]:((((((((organization(X,T1)&organization(X,T2))&reorganization_free(X,T1,T2))&reliability(X,R1,T1))&reliability(X,R2,T2))&accountability(X,A1,T1))&accountability(X,A2,T2))&greater(T2,T1))=>(greater(R2,R1)&greater(A2,A1))))))))))),inference(assume_negation,[status(cth)],[t6_FOL])).
% 0.24/0.51 fof(c1,negated_conjecture,(?[X]:(?[R1]:(?[R2]:(?[A1]:(?[A2]:(?[T1]:(?[T2]:((((((((organization(X,T1)&organization(X,T2))&reorganization_free(X,T1,T2))&reliability(X,R1,T1))&reliability(X,R2,T2))&accountability(X,A1,T1))&accountability(X,A2,T2))&greater(T2,T1))&(~greater(R2,R1)|~greater(A2,A1)))))))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.24/0.51 fof(c2,negated_conjecture,(?[X]:(?[R1]:(?[R2]:(?[A1]:(?[A2]:((?[T1]:(?[T2]:(((((((organization(X,T1)&organization(X,T2))&reorganization_free(X,T1,T2))&reliability(X,R1,T1))&reliability(X,R2,T2))&accountability(X,A1,T1))&accountability(X,A2,T2))&greater(T2,T1))))&(~greater(R2,R1)|~greater(A2,A1)))))))),inference(shift_quantors,[status(thm)],[c1])).
% 0.24/0.51 fof(c3,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:((?[X7]:(?[X8]:(((((((organization(X2,X7)&organization(X2,X8))&reorganization_free(X2,X7,X8))&reliability(X2,X3,X7))&reliability(X2,X4,X8))&accountability(X2,X5,X7))&accountability(X2,X6,X8))&greater(X8,X7))))&(~greater(X4,X3)|~greater(X6,X5)))))))),inference(variable_rename,[status(thm)],[c2])).
% 0.24/0.51 fof(c4,negated_conjecture,((((((((organization(skolem0001,skolem0006)&organization(skolem0001,skolem0007))&reorganization_free(skolem0001,skolem0006,skolem0007))&reliability(skolem0001,skolem0002,skolem0006))&reliability(skolem0001,skolem0003,skolem0007))&accountability(skolem0001,skolem0004,skolem0006))&accountability(skolem0001,skolem0005,skolem0007))&greater(skolem0007,skolem0006))&(~greater(skolem0003,skolem0002)|~greater(skolem0005,skolem0004))),inference(skolemize,[status(esa)],[c3])).
% 0.24/0.51 cnf(c5,negated_conjecture,organization(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c4])).
% 0.24/0.51 cnf(c6,negated_conjecture,organization(skolem0001,skolem0007),inference(split_conjunct,[status(thm)],[c4])).
% 0.24/0.51 cnf(c8,negated_conjecture,reliability(skolem0001,skolem0002,skolem0006),inference(split_conjunct,[status(thm)],[c4])).
% 0.24/0.51 cnf(c9,negated_conjecture,reliability(skolem0001,skolem0003,skolem0007),inference(split_conjunct,[status(thm)],[c4])).
% 0.24/0.51 cnf(c10,negated_conjecture,accountability(skolem0001,skolem0004,skolem0006),inference(split_conjunct,[status(thm)],[c4])).
% 0.24/0.51 cnf(c11,negated_conjecture,accountability(skolem0001,skolem0005,skolem0007),inference(split_conjunct,[status(thm)],[c4])).
% 0.24/0.51 fof(mp3,axiom,(![X]:(![T]:(organization(X,T)=>(?[Rp]:reproducibility(X,Rp,T))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp3)).
% 0.24/0.51 fof(c25,plain,(![X]:(![T]:(~organization(X,T)|(?[Rp]:reproducibility(X,Rp,T))))),inference(fof_nnf,[status(thm)],[mp3])).
% 0.24/0.51 fof(c26,plain,(![X24]:(![X25]:(~organization(X24,X25)|(?[X26]:reproducibility(X24,X26,X25))))),inference(variable_rename,[status(thm)],[c25])).
% 0.24/0.51 fof(c27,plain,(![X24]:(![X25]:(~organization(X24,X25)|reproducibility(X24,skolem0008(X24,X25),X25)))),inference(skolemize,[status(esa)],[c26])).
% 0.24/0.51 cnf(c28,plain,~organization(X28,X27)|reproducibility(X28,skolem0008(X28,X27),X27),inference(split_conjunct,[status(thm)],[c27])).
% 0.24/0.51 cnf(c30,plain,reproducibility(skolem0001,skolem0008(skolem0001,skolem0006),skolem0006),inference(resolution,[status(thm)],[c28, c5])).
% 0.24/0.51 cnf(c12,negated_conjecture,greater(skolem0007,skolem0006),inference(split_conjunct,[status(thm)],[c4])).
% 0.24/0.51 cnf(c7,negated_conjecture,reorganization_free(skolem0001,skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c4])).
% 0.24/0.51 cnf(c29,plain,reproducibility(skolem0001,skolem0008(skolem0001,skolem0007),skolem0007),inference(resolution,[status(thm)],[c28, c6])).
% 0.24/0.51 fof(a4_FOL,plain,(![X]:(![Rp1]:(![Rp2]:(![T1]:(![T2]:((((((organization(X,T1)&organization(X,T2))&reorganization_free(X,T1,T2))&reproducibility(X,Rp1,T1))&reproducibility(X,Rp2,T2))&greater(T2,T1))=>greater(Rp2,Rp1))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', a4_FOL)).
% 0.24/0.51 fof(c14,plain,(![X]:(![Rp1]:(![Rp2]:(![T1]:(![T2]:((((((~organization(X,T1)|~organization(X,T2))|~reorganization_free(X,T1,T2))|~reproducibility(X,Rp1,T1))|~reproducibility(X,Rp2,T2))|~greater(T2,T1))|greater(Rp2,Rp1))))))),inference(fof_nnf,[status(thm)],[a4_FOL])).
% 0.24/0.51 fof(c15,plain,(![X]:(![Rp1]:(![Rp2]:((![T1]:(![T2]:(((((~organization(X,T1)|~organization(X,T2))|~reorganization_free(X,T1,T2))|~reproducibility(X,Rp1,T1))|~reproducibility(X,Rp2,T2))|~greater(T2,T1))))|greater(Rp2,Rp1))))),inference(shift_quantors,[status(thm)],[c14])).
% 0.24/0.51 fof(c17,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:((((((~organization(X9,X12)|~organization(X9,X13))|~reorganization_free(X9,X12,X13))|~reproducibility(X9,X10,X12))|~reproducibility(X9,X11,X13))|~greater(X13,X12))|greater(X11,X10))))))),inference(shift_quantors,[status(thm)],[fof(c16,plain,(![X9]:(![X10]:(![X11]:((![X12]:(![X13]:(((((~organization(X9,X12)|~organization(X9,X13))|~reorganization_free(X9,X12,X13))|~reproducibility(X9,X10,X12))|~reproducibility(X9,X11,X13))|~greater(X13,X12))))|greater(X11,X10))))),inference(variable_rename,[status(thm)],[c15])).])).
% 0.24/0.51 cnf(c18,plain,~organization(X29,X31)|~organization(X29,X32)|~reorganization_free(X29,X31,X32)|~reproducibility(X29,X30,X31)|~reproducibility(X29,X33,X32)|~greater(X32,X31)|greater(X33,X30),inference(split_conjunct,[status(thm)],[c17])).
% 0.24/0.51 cnf(c32,plain,~organization(skolem0001,X37)|~organization(skolem0001,skolem0007)|~reorganization_free(skolem0001,X37,skolem0007)|~reproducibility(skolem0001,X38,X37)|~greater(skolem0007,X37)|greater(skolem0008(skolem0001,skolem0007),X38),inference(resolution,[status(thm)],[c18, c29])).
% 0.24/0.51 cnf(c37,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|~reorganization_free(skolem0001,skolem0006,skolem0007)|~greater(skolem0007,skolem0006)|greater(skolem0008(skolem0001,skolem0007),skolem0008(skolem0001,skolem0006)),inference(resolution,[status(thm)],[c32, c30])).
% 0.24/0.51 cnf(c45,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|~greater(skolem0007,skolem0006)|greater(skolem0008(skolem0001,skolem0007),skolem0008(skolem0001,skolem0006)),inference(resolution,[status(thm)],[c37, c7])).
% 0.24/0.51 cnf(c49,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|greater(skolem0008(skolem0001,skolem0007),skolem0008(skolem0001,skolem0006)),inference(resolution,[status(thm)],[c45, c12])).
% 0.24/0.51 cnf(c50,plain,~organization(skolem0001,skolem0006)|greater(skolem0008(skolem0001,skolem0007),skolem0008(skolem0001,skolem0006)),inference(resolution,[status(thm)],[c49, c6])).
% 0.24/0.51 cnf(c51,plain,greater(skolem0008(skolem0001,skolem0007),skolem0008(skolem0001,skolem0006)),inference(resolution,[status(thm)],[c50, c5])).
% 0.24/0.51 fof(a2_FOL,plain,(![X]:(![Y]:(![T1]:(![T2]:(![R1]:(![R2]:(![A1]:(![A2]:(![Rp1]:(![Rp2]:((((((((organization(X,T1)&organization(Y,T2))&reliability(X,R1,T1))&reliability(Y,R2,T2))&accountability(X,A1,T1))&accountability(Y,A2,T2))&reproducibility(X,Rp1,T1))&reproducibility(Y,Rp2,T2))=>(greater(Rp2,Rp1)<=>(greater(R2,R1)&greater(A2,A1)))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', a2_FOL)).
% 0.24/0.51 fof(c19,plain,(![X]:(![Y]:(![T1]:(![T2]:(![R1]:(![R2]:(![A1]:(![A2]:(![Rp1]:(![Rp2]:((((((((~organization(X,T1)|~organization(Y,T2))|~reliability(X,R1,T1))|~reliability(Y,R2,T2))|~accountability(X,A1,T1))|~accountability(Y,A2,T2))|~reproducibility(X,Rp1,T1))|~reproducibility(Y,Rp2,T2))|((~greater(Rp2,Rp1)|(greater(R2,R1)&greater(A2,A1)))&((~greater(R2,R1)|~greater(A2,A1))|greater(Rp2,Rp1)))))))))))))),inference(fof_nnf,[status(thm)],[a2_FOL])).
% 0.24/0.51 fof(c20,plain,(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:((((((((~organization(X14,X16)|~organization(X15,X17))|~reliability(X14,X18,X16))|~reliability(X15,X19,X17))|~accountability(X14,X20,X16))|~accountability(X15,X21,X17))|~reproducibility(X14,X22,X16))|~reproducibility(X15,X23,X17))|((~greater(X23,X22)|(greater(X19,X18)&greater(X21,X20)))&((~greater(X19,X18)|~greater(X21,X20))|greater(X23,X22)))))))))))))),inference(variable_rename,[status(thm)],[c19])).
% 0.24/0.51 fof(c21,plain,(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:((((((((((~organization(X14,X16)|~organization(X15,X17))|~reliability(X14,X18,X16))|~reliability(X15,X19,X17))|~accountability(X14,X20,X16))|~accountability(X15,X21,X17))|~reproducibility(X14,X22,X16))|~reproducibility(X15,X23,X17))|(~greater(X23,X22)|greater(X19,X18)))&((((((((~organization(X14,X16)|~organization(X15,X17))|~reliability(X14,X18,X16))|~reliability(X15,X19,X17))|~accountability(X14,X20,X16))|~accountability(X15,X21,X17))|~reproducibility(X14,X22,X16))|~reproducibility(X15,X23,X17))|(~greater(X23,X22)|greater(X21,X20))))&((((((((~organization(X14,X16)|~organization(X15,X17))|~reliability(X14,X18,X16))|~reliability(X15,X19,X17))|~accountability(X14,X20,X16))|~accountability(X15,X21,X17))|~reproducibility(X14,X22,X16))|~reproducibility(X15,X23,X17))|((~greater(X19,X18)|~greater(X21,X20))|greater(X23,X22)))))))))))))),inference(distribute,[status(thm)],[c20])).
% 0.24/0.51 cnf(c22,plain,~organization(X45,X46)|~organization(X48,X41)|~reliability(X45,X44,X46)|~reliability(X48,X42,X41)|~accountability(X45,X43,X46)|~accountability(X48,X40,X41)|~reproducibility(X45,X39,X46)|~reproducibility(X48,X47,X41)|~greater(X47,X39)|greater(X42,X44),inference(split_conjunct,[status(thm)],[c21])).
% 0.24/0.51 cnf(c39,plain,~organization(X94,X92)|~organization(skolem0001,skolem0007)|~reliability(X94,X95,X92)|~reliability(skolem0001,X93,skolem0007)|~accountability(X94,X98,X92)|~accountability(skolem0001,X97,skolem0007)|~reproducibility(X94,X96,X92)|~greater(skolem0008(skolem0001,skolem0007),X96)|greater(X93,X95),inference(resolution,[status(thm)],[c22, c29])).
% 0.24/0.51 cnf(c59,plain,~organization(X104,X99)|~organization(skolem0001,skolem0007)|~reliability(X104,X100,X99)|~reliability(skolem0001,X101,skolem0007)|~accountability(X104,X103,X99)|~accountability(skolem0001,X102,skolem0007)|~reproducibility(X104,skolem0008(skolem0001,skolem0006),X99)|greater(X101,X100),inference(resolution,[status(thm)],[c39, c51])).
% 0.24/0.51 cnf(c60,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|~reliability(skolem0001,X105,skolem0006)|~reliability(skolem0001,X106,skolem0007)|~accountability(skolem0001,X108,skolem0006)|~accountability(skolem0001,X107,skolem0007)|greater(X106,X105),inference(resolution,[status(thm)],[c59, c30])).
% 0.24/0.51 cnf(c61,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|~reliability(skolem0001,X117,skolem0006)|~reliability(skolem0001,X116,skolem0007)|~accountability(skolem0001,X118,skolem0006)|greater(X116,X117),inference(resolution,[status(thm)],[c60, c11])).
% 0.24/0.51 cnf(c62,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|~reliability(skolem0001,X120,skolem0006)|~reliability(skolem0001,X119,skolem0007)|greater(X119,X120),inference(resolution,[status(thm)],[c61, c10])).
% 0.24/0.51 cnf(c63,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|~reliability(skolem0001,X121,skolem0006)|greater(skolem0003,X121),inference(resolution,[status(thm)],[c62, c9])).
% 0.24/0.51 cnf(c64,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|greater(skolem0003,skolem0002),inference(resolution,[status(thm)],[c63, c8])).
% 0.24/0.51 cnf(c65,plain,~organization(skolem0001,skolem0006)|greater(skolem0003,skolem0002),inference(resolution,[status(thm)],[c64, c6])).
% 0.24/0.51 cnf(c66,plain,greater(skolem0003,skolem0002),inference(resolution,[status(thm)],[c65, c5])).
% 0.24/0.51 cnf(c13,negated_conjecture,~greater(skolem0003,skolem0002)|~greater(skolem0005,skolem0004),inference(split_conjunct,[status(thm)],[c4])).
% 0.24/0.51 cnf(c23,plain,~organization(X64,X65)|~organization(X67,X60)|~reliability(X64,X63,X65)|~reliability(X67,X61,X60)|~accountability(X64,X62,X65)|~accountability(X67,X59,X60)|~reproducibility(X64,X58,X65)|~reproducibility(X67,X66,X60)|~greater(X66,X58)|greater(X59,X62),inference(split_conjunct,[status(thm)],[c21])).
% 0.24/0.51 cnf(c47,plain,~organization(X135,X131)|~organization(skolem0001,skolem0007)|~reliability(X135,X136,X131)|~reliability(skolem0001,X130,skolem0007)|~accountability(X135,X134,X131)|~accountability(skolem0001,X132,skolem0007)|~reproducibility(X135,X133,X131)|~greater(skolem0008(skolem0001,skolem0007),X133)|greater(X132,X134),inference(resolution,[status(thm)],[c23, c29])).
% 0.24/0.51 cnf(c67,plain,~organization(X137,X142)|~organization(skolem0001,skolem0007)|~reliability(X137,X140,X142)|~reliability(skolem0001,X139,skolem0007)|~accountability(X137,X138,X142)|~accountability(skolem0001,X141,skolem0007)|~reproducibility(X137,skolem0008(skolem0001,skolem0006),X142)|greater(X141,X138),inference(resolution,[status(thm)],[c47, c51])).
% 0.24/0.51 cnf(c68,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|~reliability(skolem0001,X146,skolem0006)|~reliability(skolem0001,X143,skolem0007)|~accountability(skolem0001,X144,skolem0006)|~accountability(skolem0001,X145,skolem0007)|greater(X145,X144),inference(resolution,[status(thm)],[c67, c30])).
% 0.24/0.51 cnf(c69,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|~reliability(skolem0001,X154,skolem0006)|~reliability(skolem0001,X156,skolem0007)|~accountability(skolem0001,X155,skolem0006)|greater(skolem0005,X155),inference(resolution,[status(thm)],[c68, c11])).
% 0.24/0.51 cnf(c70,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|~reliability(skolem0001,X158,skolem0006)|~reliability(skolem0001,X157,skolem0007)|greater(skolem0005,skolem0004),inference(resolution,[status(thm)],[c69, c10])).
% 0.24/0.51 cnf(c71,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|~reliability(skolem0001,X159,skolem0006)|greater(skolem0005,skolem0004),inference(resolution,[status(thm)],[c70, c9])).
% 0.24/0.51 cnf(c72,plain,~organization(skolem0001,skolem0006)|~organization(skolem0001,skolem0007)|greater(skolem0005,skolem0004),inference(resolution,[status(thm)],[c71, c8])).
% 0.24/0.51 cnf(c73,plain,~organization(skolem0001,skolem0006)|greater(skolem0005,skolem0004),inference(resolution,[status(thm)],[c72, c6])).
% 0.24/0.51 cnf(c74,plain,greater(skolem0005,skolem0004),inference(resolution,[status(thm)],[c73, c5])).
% 0.24/0.51 cnf(c75,plain,~greater(skolem0003,skolem0002),inference(resolution,[status(thm)],[c74, c13])).
% 0.24/0.51 cnf(c76,plain,$false,inference(resolution,[status(thm)],[c75, c66])).
% 0.24/0.51 % SZS output end CNFRefutation
% 0.24/0.51
% 0.24/0.51 % Initial clauses : 14
% 0.24/0.51 % Processed clauses : 54
% 0.24/0.51 % Factors computed : 4
% 0.24/0.51 % Resolvents computed: 44
% 0.24/0.51 % Tautologies deleted: 0
% 0.24/0.51 % Forward subsumed : 2
% 0.24/0.51 % Backward subsumed : 13
% 0.24/0.51 % -------- CPU Time ---------
% 0.24/0.51 % User time : 0.130 s
% 0.24/0.51 % System time : 0.014 s
% 0.24/0.51 % Total time : 0.144 s
%------------------------------------------------------------------------------