%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT010+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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:38 AM UTC 2026
% Result : Theorem 0.46s 0.79s
% Output : CNFRefutation 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT010+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.35 % Computer : n016.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 7 11:52:32 UTC 2026
% 0.08/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.41 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.41 (re.compile("\?"), Token.Existential),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.41 (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.22/0.48 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.48 """
% 0.22/0.49 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.32/0.58 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.58 """
% 0.46/0.79 % Version: 1.5
% 0.46/0.79 % SZS status Theorem
% 0.46/0.79 % SZS output start CNFRefutation
% 0.46/0.79 fof(t10_FOL,conjecture,(![X]:(![Y]:(![C]:(![R1]:(![R2]:(![A1]:(![A2]:(![S1]:(![S2]:(![T1]:(![T2]:(((((((((((((organization(X,T1)&organization(Y,T2))&reorganization_free(X,T1,T1))&reorganization_free(Y,T2,T2))&class(X,C,T1))&class(Y,C,T2))&reliability(X,R1,T1))&reliability(Y,R2,T2))&accountability(X,A1,T1))&accountability(Y,A2,T2))&size(X,S1,T1))&size(Y,S2,T2))&greater(S2,S1))=>(greater(R2,R1)&greater(A2,A1)))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t10_FOL)).
% 0.46/0.79 fof(c0,negated_conjecture,(~(![X]:(![Y]:(![C]:(![R1]:(![R2]:(![A1]:(![A2]:(![S1]:(![S2]:(![T1]:(![T2]:(((((((((((((organization(X,T1)&organization(Y,T2))&reorganization_free(X,T1,T1))&reorganization_free(Y,T2,T2))&class(X,C,T1))&class(Y,C,T2))&reliability(X,R1,T1))&reliability(Y,R2,T2))&accountability(X,A1,T1))&accountability(Y,A2,T2))&size(X,S1,T1))&size(Y,S2,T2))&greater(S2,S1))=>(greater(R2,R1)&greater(A2,A1))))))))))))))),inference(assume_negation,[status(cth)],[t10_FOL])).
% 0.46/0.79 fof(c1,negated_conjecture,(?[X]:(?[Y]:(?[C]:(?[R1]:(?[R2]:(?[A1]:(?[A2]:(?[S1]:(?[S2]:(?[T1]:(?[T2]:(((((((((((((organization(X,T1)&organization(Y,T2))&reorganization_free(X,T1,T1))&reorganization_free(Y,T2,T2))&class(X,C,T1))&class(Y,C,T2))&reliability(X,R1,T1))&reliability(Y,R2,T2))&accountability(X,A1,T1))&accountability(Y,A2,T2))&size(X,S1,T1))&size(Y,S2,T2))&greater(S2,S1))&(~greater(R2,R1)|~greater(A2,A1)))))))))))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.46/0.79 fof(c2,negated_conjecture,(?[X]:(?[Y]:(?[C]:(?[R1]:(?[R2]:(?[A1]:(?[A2]:((?[S1]:(?[S2]:((?[T1]:(?[T2]:(((((((((((organization(X,T1)&organization(Y,T2))&reorganization_free(X,T1,T1))&reorganization_free(Y,T2,T2))&class(X,C,T1))&class(Y,C,T2))&reliability(X,R1,T1))&reliability(Y,R2,T2))&accountability(X,A1,T1))&accountability(Y,A2,T2))&size(X,S1,T1))&size(Y,S2,T2))))&greater(S2,S1))))&(~greater(R2,R1)|~greater(A2,A1)))))))))),inference(shift_quantors,[status(thm)],[c1])).
% 0.46/0.79 fof(c3,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:((?[X9]:(?[X10]:((?[X11]:(?[X12]:(((((((((((organization(X2,X11)&organization(X3,X12))&reorganization_free(X2,X11,X11))&reorganization_free(X3,X12,X12))&class(X2,X4,X11))&class(X3,X4,X12))&reliability(X2,X5,X11))&reliability(X3,X6,X12))&accountability(X2,X7,X11))&accountability(X3,X8,X12))&size(X2,X9,X11))&size(X3,X10,X12))))&greater(X10,X9))))&(~greater(X6,X5)|~greater(X8,X7)))))))))),inference(variable_rename,[status(thm)],[c2])).
% 0.46/0.79 fof(c4,negated_conjecture,(((((((((((((organization(skolem0001,skolem0010)&organization(skolem0002,skolem0011))&reorganization_free(skolem0001,skolem0010,skolem0010))&reorganization_free(skolem0002,skolem0011,skolem0011))&class(skolem0001,skolem0003,skolem0010))&class(skolem0002,skolem0003,skolem0011))&reliability(skolem0001,skolem0004,skolem0010))&reliability(skolem0002,skolem0005,skolem0011))&accountability(skolem0001,skolem0006,skolem0010))&accountability(skolem0002,skolem0007,skolem0011))&size(skolem0001,skolem0008,skolem0010))&size(skolem0002,skolem0009,skolem0011))&greater(skolem0009,skolem0008))&(~greater(skolem0005,skolem0004)|~greater(skolem0007,skolem0006))),inference(skolemize,[status(esa)],[c3])).
% 0.46/0.79 cnf(c18,negated_conjecture,~greater(skolem0005,skolem0004)|~greater(skolem0007,skolem0006),inference(split_conjunct,[status(thm)],[c4])).
% 0.46/0.79 cnf(c5,negated_conjecture,organization(skolem0001,skolem0010),inference(split_conjunct,[status(thm)],[c4])).
% 0.46/0.79 cnf(c6,negated_conjecture,organization(skolem0002,skolem0011),inference(split_conjunct,[status(thm)],[c4])).
% 0.46/0.79 cnf(c11,negated_conjecture,reliability(skolem0001,skolem0004,skolem0010),inference(split_conjunct,[status(thm)],[c4])).
% 0.46/0.79 cnf(c12,negated_conjecture,reliability(skolem0002,skolem0005,skolem0011),inference(split_conjunct,[status(thm)],[c4])).
% 0.46/0.79 cnf(c13,negated_conjecture,accountability(skolem0001,skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c4])).
% 0.46/0.79 cnf(c14,negated_conjecture,accountability(skolem0002,skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c4])).
% 0.46/0.79 fof(mp3,axiom,(![X]:(![T]:(organization(X,T)=>(?[Rp]:reproducibility(X,Rp,T))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp3)).
% 0.46/0.79 fof(c30,plain,(![X]:(![T]:(~organization(X,T)|(?[Rp]:reproducibility(X,Rp,T))))),inference(fof_nnf,[status(thm)],[mp3])).
% 0.46/0.79 fof(c31,plain,(![X32]:(![X33]:(~organization(X32,X33)|(?[X34]:reproducibility(X32,X34,X33))))),inference(variable_rename,[status(thm)],[c30])).
% 0.46/0.79 fof(c32,plain,(![X32]:(![X33]:(~organization(X32,X33)|reproducibility(X32,skolem0012(X32,X33),X33)))),inference(skolemize,[status(esa)],[c31])).
% 0.46/0.79 cnf(c33,plain,~organization(X36,X35)|reproducibility(X36,skolem0012(X36,X35),X35),inference(split_conjunct,[status(thm)],[c32])).
% 0.46/0.79 cnf(c35,plain,reproducibility(skolem0001,skolem0012(skolem0001,skolem0010),skolem0010),inference(resolution,[status(thm)],[c33, c5])).
% 0.46/0.79 cnf(c34,plain,reproducibility(skolem0002,skolem0012(skolem0002,skolem0011),skolem0011),inference(resolution,[status(thm)],[c33, c6])).
% 0.46/0.79 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/sandbox2/benchmark/theBenchmark.p', a2_FOL)).
% 0.46/0.79 fof(c24,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.46/0.79 fof(c25,plain,(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:((((((((~organization(X22,X24)|~organization(X23,X25))|~reliability(X22,X26,X24))|~reliability(X23,X27,X25))|~accountability(X22,X28,X24))|~accountability(X23,X29,X25))|~reproducibility(X22,X30,X24))|~reproducibility(X23,X31,X25))|((~greater(X31,X30)|(greater(X27,X26)&greater(X29,X28)))&((~greater(X27,X26)|~greater(X29,X28))|greater(X31,X30)))))))))))))),inference(variable_rename,[status(thm)],[c24])).
% 0.46/0.79 fof(c26,plain,(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:((((((((((~organization(X22,X24)|~organization(X23,X25))|~reliability(X22,X26,X24))|~reliability(X23,X27,X25))|~accountability(X22,X28,X24))|~accountability(X23,X29,X25))|~reproducibility(X22,X30,X24))|~reproducibility(X23,X31,X25))|(~greater(X31,X30)|greater(X27,X26)))&((((((((~organization(X22,X24)|~organization(X23,X25))|~reliability(X22,X26,X24))|~reliability(X23,X27,X25))|~accountability(X22,X28,X24))|~accountability(X23,X29,X25))|~reproducibility(X22,X30,X24))|~reproducibility(X23,X31,X25))|(~greater(X31,X30)|greater(X29,X28))))&((((((((~organization(X22,X24)|~organization(X23,X25))|~reliability(X22,X26,X24))|~reliability(X23,X27,X25))|~accountability(X22,X28,X24))|~accountability(X23,X29,X25))|~reproducibility(X22,X30,X24))|~reproducibility(X23,X31,X25))|((~greater(X27,X26)|~greater(X29,X28))|greater(X31,X30)))))))))))))),inference(distribute,[status(thm)],[c25])).
% 0.46/0.79 cnf(c28,plain,~organization(X81,X83)|~organization(X88,X86)|~reliability(X81,X82,X83)|~reliability(X88,X90,X86)|~accountability(X81,X89,X83)|~accountability(X88,X84,X86)|~reproducibility(X81,X85,X83)|~reproducibility(X88,X87,X86)|~greater(X87,X85)|greater(X84,X89),inference(split_conjunct,[status(thm)],[c26])).
% 0.46/0.79 cnf(c55,plain,~organization(X157,X153)|~organization(skolem0002,skolem0011)|~reliability(X157,X158,X153)|~reliability(skolem0002,X152,skolem0011)|~accountability(X157,X156,X153)|~accountability(skolem0002,X154,skolem0011)|~reproducibility(X157,X155,X153)|~greater(skolem0012(skolem0002,skolem0011),X155)|greater(X154,X156),inference(resolution,[status(thm)],[c28, c34])).
% 0.46/0.79 cnf(c17,negated_conjecture,greater(skolem0009,skolem0008),inference(split_conjunct,[status(thm)],[c4])).
% 0.46/0.79 cnf(c7,negated_conjecture,reorganization_free(skolem0001,skolem0010,skolem0010),inference(split_conjunct,[status(thm)],[c4])).
% 0.46/0.79 cnf(c8,negated_conjecture,reorganization_free(skolem0002,skolem0011,skolem0011),inference(split_conjunct,[status(thm)],[c4])).
% 0.46/0.79 cnf(c9,negated_conjecture,class(skolem0001,skolem0003,skolem0010),inference(split_conjunct,[status(thm)],[c4])).
% 0.46/0.79 cnf(c10,negated_conjecture,class(skolem0002,skolem0003,skolem0011),inference(split_conjunct,[status(thm)],[c4])).
% 0.46/0.79 cnf(c15,negated_conjecture,size(skolem0001,skolem0008,skolem0010),inference(split_conjunct,[status(thm)],[c4])).
% 0.46/0.79 cnf(c16,negated_conjecture,size(skolem0002,skolem0009,skolem0011),inference(split_conjunct,[status(thm)],[c4])).
% 0.46/0.79 fof(t9_FOL,plain,(![X]:(![Y]:(![C]:(![Rp1]:(![Rp2]:(![S1]:(![S2]:(![T1]:(![T2]:(((((((((((organization(X,T1)&organization(Y,T2))&reorganization_free(X,T1,T1))&reorganization_free(Y,T2,T2))&class(X,C,T1))&class(Y,C,T2))&reproducibility(X,Rp1,T1))&reproducibility(Y,Rp2,T2))&size(X,S1,T1))&size(Y,S2,T2))&greater(S2,S1))=>greater(Rp2,Rp1))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t9_FOL)).
% 0.46/0.79 fof(c19,plain,(![X]:(![Y]:(![C]:(![Rp1]:(![Rp2]:(![S1]:(![S2]:(![T1]:(![T2]:(((((((((((~organization(X,T1)|~organization(Y,T2))|~reorganization_free(X,T1,T1))|~reorganization_free(Y,T2,T2))|~class(X,C,T1))|~class(Y,C,T2))|~reproducibility(X,Rp1,T1))|~reproducibility(Y,Rp2,T2))|~size(X,S1,T1))|~size(Y,S2,T2))|~greater(S2,S1))|greater(Rp2,Rp1))))))))))),inference(fof_nnf,[status(thm)],[t9_FOL])).
% 0.46/0.79 fof(c20,plain,(![X]:(![Y]:(![C]:(![Rp1]:(![Rp2]:((![S1]:(![S2]:((![T1]:(![T2]:(((((((((~organization(X,T1)|~organization(Y,T2))|~reorganization_free(X,T1,T1))|~reorganization_free(Y,T2,T2))|~class(X,C,T1))|~class(Y,C,T2))|~reproducibility(X,Rp1,T1))|~reproducibility(Y,Rp2,T2))|~size(X,S1,T1))|~size(Y,S2,T2))))|~greater(S2,S1))))|greater(Rp2,Rp1))))))),inference(shift_quantors,[status(thm)],[c19])).
% 0.46/0.79 fof(c22,plain,(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(((((((((((~organization(X13,X20)|~organization(X14,X21))|~reorganization_free(X13,X20,X20))|~reorganization_free(X14,X21,X21))|~class(X13,X15,X20))|~class(X14,X15,X21))|~reproducibility(X13,X16,X20))|~reproducibility(X14,X17,X21))|~size(X13,X18,X20))|~size(X14,X19,X21))|~greater(X19,X18))|greater(X17,X16))))))))))),inference(shift_quantors,[status(thm)],[fof(c21,plain,(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:((![X18]:(![X19]:((![X20]:(![X21]:(((((((((~organization(X13,X20)|~organization(X14,X21))|~reorganization_free(X13,X20,X20))|~reorganization_free(X14,X21,X21))|~class(X13,X15,X20))|~class(X14,X15,X21))|~reproducibility(X13,X16,X20))|~reproducibility(X14,X17,X21))|~size(X13,X18,X20))|~size(X14,X19,X21))))|~greater(X19,X18))))|greater(X17,X16))))))),inference(variable_rename,[status(thm)],[c20])).])).
% 0.46/0.79 cnf(c23,plain,~organization(X38,X43)|~organization(X37,X42)|~reorganization_free(X38,X43,X43)|~reorganization_free(X37,X42,X42)|~class(X38,X44,X43)|~class(X37,X44,X42)|~reproducibility(X38,X39,X43)|~reproducibility(X37,X40,X42)|~size(X38,X45,X43)|~size(X37,X41,X42)|~greater(X41,X45)|greater(X40,X39),inference(split_conjunct,[status(thm)],[c22])).
% 0.46/0.79 cnf(c38,plain,~organization(X168,X170)|~organization(skolem0002,skolem0011)|~reorganization_free(X168,X170,X170)|~reorganization_free(skolem0002,skolem0011,skolem0011)|~class(X168,X169,X170)|~class(skolem0002,X169,skolem0011)|~reproducibility(X168,X166,X170)|~reproducibility(skolem0002,X167,skolem0011)|~size(X168,X171,X170)|~greater(skolem0009,X171)|greater(X167,X166),inference(resolution,[status(thm)],[c23, c16])).
% 0.46/0.79 cnf(c70,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0011)|~reorganization_free(skolem0001,skolem0010,skolem0010)|~reorganization_free(skolem0002,skolem0011,skolem0011)|~class(skolem0001,X231,skolem0010)|~class(skolem0002,X231,skolem0011)|~reproducibility(skolem0001,X230,skolem0010)|~reproducibility(skolem0002,X232,skolem0011)|~greater(skolem0009,skolem0008)|greater(X232,X230),inference(resolution,[status(thm)],[c38, c15])).
% 0.46/0.79 cnf(c93,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0011)|~reorganization_free(skolem0001,skolem0010,skolem0010)|~reorganization_free(skolem0002,skolem0011,skolem0011)|~class(skolem0001,X266,skolem0010)|~class(skolem0002,X266,skolem0011)|~reproducibility(skolem0001,X267,skolem0010)|~greater(skolem0009,skolem0008)|greater(skolem0012(skolem0002,skolem0011),X267),inference(resolution,[status(thm)],[c70, c34])).
% 0.46/0.79 cnf(c106,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0011)|~reorganization_free(skolem0001,skolem0010,skolem0010)|~reorganization_free(skolem0002,skolem0011,skolem0011)|~class(skolem0001,X268,skolem0010)|~class(skolem0002,X268,skolem0011)|~greater(skolem0009,skolem0008)|greater(skolem0012(skolem0002,skolem0011),skolem0012(skolem0001,skolem0010)),inference(resolution,[status(thm)],[c93, c35])).
% 0.46/0.79 cnf(c108,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0011)|~reorganization_free(skolem0001,skolem0010,skolem0010)|~reorganization_free(skolem0002,skolem0011,skolem0011)|~class(skolem0001,skolem0003,skolem0010)|~greater(skolem0009,skolem0008)|greater(skolem0012(skolem0002,skolem0011),skolem0012(skolem0001,skolem0010)),inference(resolution,[status(thm)],[c106, c10])).
% 0.46/0.79 cnf(c109,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0011)|~reorganization_free(skolem0001,skolem0010,skolem0010)|~reorganization_free(skolem0002,skolem0011,skolem0011)|~greater(skolem0009,skolem0008)|greater(skolem0012(skolem0002,skolem0011),skolem0012(skolem0001,skolem0010)),inference(resolution,[status(thm)],[c108, c9])).
% 0.46/0.79 cnf(c110,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0011)|~reorganization_free(skolem0001,skolem0010,skolem0010)|~greater(skolem0009,skolem0008)|greater(skolem0012(skolem0002,skolem0011),skolem0012(skolem0001,skolem0010)),inference(resolution,[status(thm)],[c109, c8])).
% 0.46/0.79 cnf(c111,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0011)|~greater(skolem0009,skolem0008)|greater(skolem0012(skolem0002,skolem0011),skolem0012(skolem0001,skolem0010)),inference(resolution,[status(thm)],[c110, c7])).
% 0.46/0.79 cnf(c112,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0011)|greater(skolem0012(skolem0002,skolem0011),skolem0012(skolem0001,skolem0010)),inference(resolution,[status(thm)],[c111, c17])).
% 0.46/0.79 cnf(c113,plain,~organization(skolem0001,skolem0010)|greater(skolem0012(skolem0002,skolem0011),skolem0012(skolem0001,skolem0010)),inference(resolution,[status(thm)],[c112, c6])).
% 0.46/0.79 cnf(c114,plain,greater(skolem0012(skolem0002,skolem0011),skolem0012(skolem0001,skolem0010)),inference(resolution,[status(thm)],[c113, c5])).
% 0.46/0.79 cnf(c115,plain,~organization(X272,X269)|~organization(skolem0002,skolem0011)|~reliability(X272,X273,X269)|~reliability(skolem0002,X271,skolem0011)|~accountability(X272,X274,X269)|~accountability(skolem0002,X270,skolem0011)|~reproducibility(X272,skolem0012(skolem0001,skolem0010),X269)|greater(X270,X274),inference(resolution,[status(thm)],[c114, c55])).
% 0.46/0.79 cnf(c117,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0011)|~reliability(skolem0001,X281,skolem0010)|~reliability(skolem0002,X282,skolem0011)|~accountability(skolem0001,X284,skolem0010)|~accountability(skolem0002,X283,skolem0011)|greater(X283,X284),inference(resolution,[status(thm)],[c115, c35])).
% 0.46/0.79 cnf(c119,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0011)|~reliability(skolem0001,X286,skolem0010)|~reliability(skolem0002,X287,skolem0011)|~accountability(skolem0001,X285,skolem0010)|greater(skolem0007,X285),inference(resolution,[status(thm)],[c117, c14])).
% 0.46/0.79 cnf(c120,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0011)|~reliability(skolem0001,X289,skolem0010)|~reliability(skolem0002,X288,skolem0011)|greater(skolem0007,skolem0006),inference(resolution,[status(thm)],[c119, c13])).
% 0.46/0.80 cnf(c121,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0011)|~reliability(skolem0001,X290,skolem0010)|greater(skolem0007,skolem0006),inference(resolution,[status(thm)],[c120, c12])).
% 0.46/0.80 cnf(c122,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0011)|greater(skolem0007,skolem0006),inference(resolution,[status(thm)],[c121, c11])).
% 0.46/0.80 cnf(c123,plain,~organization(skolem0001,skolem0010)|greater(skolem0007,skolem0006),inference(resolution,[status(thm)],[c122, c6])).
% 0.46/0.80 cnf(c125,plain,greater(skolem0007,skolem0006),inference(resolution,[status(thm)],[c123, c5])).
% 0.46/0.80 cnf(c126,plain,~greater(skolem0005,skolem0004),inference(resolution,[status(thm)],[c125, c18])).
% 0.46/0.80 cnf(c27,plain,~organization(X58,X60)|~organization(X65,X63)|~reliability(X58,X59,X60)|~reliability(X65,X67,X63)|~accountability(X58,X66,X60)|~accountability(X65,X61,X63)|~reproducibility(X58,X62,X60)|~reproducibility(X65,X64,X63)|~greater(X64,X62)|greater(X67,X59),inference(split_conjunct,[status(thm)],[c26])).
% 0.46/0.80 cnf(c47,plain,~organization(X123,X122)|~organization(skolem0002,skolem0011)|~reliability(X123,X127,X122)|~reliability(skolem0002,X126,skolem0011)|~accountability(X123,X124,X122)|~accountability(skolem0002,X125,skolem0011)|~reproducibility(X123,X121,X122)|~greater(skolem0012(skolem0002,skolem0011),X121)|greater(X126,X127),inference(resolution,[status(thm)],[c27, c34])).
% 0.46/0.80 cnf(c116,plain,~organization(X275,X279)|~organization(skolem0002,skolem0011)|~reliability(X275,X280,X279)|~reliability(skolem0002,X276,skolem0011)|~accountability(X275,X277,X279)|~accountability(skolem0002,X278,skolem0011)|~reproducibility(X275,skolem0012(skolem0001,skolem0010),X279)|greater(X276,X280),inference(resolution,[status(thm)],[c114, c47])).
% 0.46/0.80 cnf(c118,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0011)|~reliability(skolem0001,X294,skolem0010)|~reliability(skolem0002,X292,skolem0011)|~accountability(skolem0001,X293,skolem0010)|~accountability(skolem0002,X291,skolem0011)|greater(X292,X294),inference(resolution,[status(thm)],[c116, c35])).
% 0.46/0.80 cnf(c124,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0011)|~reliability(skolem0001,X295,skolem0010)|~reliability(skolem0002,X296,skolem0011)|~accountability(skolem0001,X297,skolem0010)|greater(X296,X295),inference(resolution,[status(thm)],[c118, c14])).
% 0.46/0.80 cnf(c127,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0011)|~reliability(skolem0001,X299,skolem0010)|~reliability(skolem0002,X298,skolem0011)|greater(X298,X299),inference(resolution,[status(thm)],[c124, c13])).
% 0.46/0.80 cnf(c128,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0011)|~reliability(skolem0001,X300,skolem0010)|greater(skolem0005,X300),inference(resolution,[status(thm)],[c127, c12])).
% 0.46/0.80 cnf(c129,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0011)|greater(skolem0005,skolem0004),inference(resolution,[status(thm)],[c128, c11])).
% 0.46/0.80 cnf(c130,plain,~organization(skolem0001,skolem0010)|greater(skolem0005,skolem0004),inference(resolution,[status(thm)],[c129, c6])).
% 0.46/0.80 cnf(c131,plain,greater(skolem0005,skolem0004),inference(resolution,[status(thm)],[c130, c5])).
% 0.46/0.80 cnf(c132,plain,$false,inference(resolution,[status(thm)],[c131, c126])).
% 0.46/0.80 % SZS output end CNFRefutation
% 0.46/0.80
% 0.46/0.80 % Initial clauses : 19
% 0.46/0.80 % Processed clauses : 106
% 0.46/0.80 % Factors computed : 10
% 0.46/0.80 % Resolvents computed: 89
% 0.46/0.80 % Tautologies deleted: 0
% 0.46/0.80 % Forward subsumed : 11
% 0.46/0.80 % Backward subsumed : 28
% 0.46/0.80 % -------- CPU Time ---------
% 0.46/0.80 % User time : 0.417 s
% 0.46/0.80 % System time : 0.025 s
% 0.46/0.80 % Total time : 0.442 s
%------------------------------------------------------------------------------