%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT007+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n006.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 1.17s 1.47s
% Output : CNFRefutation 1.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT007+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.35 % Computer : n006.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % 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:43:16 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.14/0.42 (re.compile("\."), Token.FullStop),
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.14/0.42 (re.compile("\("), Token.OpenPar),
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.14/0.42 (re.compile("\)"), Token.ClosePar),
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.14/0.42 (re.compile("\["), Token.OpenSquare),
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.14/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.14/0.42 (re.compile("~\|"), Token.Nor),
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.14/0.42 (re.compile("\|"), Token.Or),
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.14/0.42 (re.compile("\?"), Token.Existential),
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.14/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.14/0.42 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.14/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.23/0.49 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.49 """
% 0.23/0.49 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.49 """
% 0.33/0.58 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.58 """
% 1.17/1.47 % Version: 1.5
% 1.17/1.47 % SZS status Theorem
% 1.17/1.47 % SZS output start CNFRefutation
% 1.17/1.47 fof(t7_FOL,conjecture,(![X]:(![Rp1]:(![Rp2]:(![T1]:(![T2]:(![Ta]:(![Tb]:((((((((organization(X,T1)&organization(X,T2))&reorganization(X,Ta,Tb))&reproducibility(X,Rp1,T1))&reproducibility(X,Rp2,T2))&(~greater(Ta,T1)))&greater(T2,T1))&(~greater(T2,Tb)))=>greater(Rp1,Rp2))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t7_FOL)).
% 1.17/1.47 fof(c0,negated_conjecture,(~(![X]:(![Rp1]:(![Rp2]:(![T1]:(![T2]:(![Ta]:(![Tb]:((((((((organization(X,T1)&organization(X,T2))&reorganization(X,Ta,Tb))&reproducibility(X,Rp1,T1))&reproducibility(X,Rp2,T2))&(~greater(Ta,T1)))&greater(T2,T1))&(~greater(T2,Tb)))=>greater(Rp1,Rp2)))))))))),inference(assume_negation,[status(cth)],[t7_FOL])).
% 1.17/1.47 fof(c1,negated_conjecture,(~(![X]:(![Rp1]:(![Rp2]:(![T1]:(![T2]:(![Ta]:(![Tb]:((((((((organization(X,T1)&organization(X,T2))&reorganization(X,Ta,Tb))&reproducibility(X,Rp1,T1))&reproducibility(X,Rp2,T2))&~greater(Ta,T1))&greater(T2,T1))&~greater(T2,Tb))=>greater(Rp1,Rp2)))))))))),inference(fof_simplification,[status(thm)],[c0])).
% 1.17/1.47 fof(c2,negated_conjecture,(?[X]:(?[Rp1]:(?[Rp2]:(?[T1]:(?[T2]:(?[Ta]:(?[Tb]:((((((((organization(X,T1)&organization(X,T2))&reorganization(X,Ta,Tb))&reproducibility(X,Rp1,T1))&reproducibility(X,Rp2,T2))&~greater(Ta,T1))&greater(T2,T1))&~greater(T2,Tb))&~greater(Rp1,Rp2))))))))),inference(fof_nnf,[status(thm)],[c1])).
% 1.17/1.47 fof(c3,negated_conjecture,(?[X]:(?[Rp1]:(?[Rp2]:((?[T1]:(?[T2]:(?[Ta]:(?[Tb]:(((((((organization(X,T1)&organization(X,T2))&reorganization(X,Ta,Tb))&reproducibility(X,Rp1,T1))&reproducibility(X,Rp2,T2))&~greater(Ta,T1))&greater(T2,T1))&~greater(T2,Tb))))))&~greater(Rp1,Rp2))))),inference(shift_quantors,[status(thm)],[c2])).
% 1.17/1.47 fof(c4,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((?[X5]:(?[X6]:(?[X7]:(?[X8]:(((((((organization(X2,X5)&organization(X2,X6))&reorganization(X2,X7,X8))&reproducibility(X2,X3,X5))&reproducibility(X2,X4,X6))&~greater(X7,X5))&greater(X6,X5))&~greater(X6,X8))))))&~greater(X3,X4))))),inference(variable_rename,[status(thm)],[c3])).
% 1.17/1.47 fof(c5,negated_conjecture,((((((((organization(skolem0001,skolem0004)&organization(skolem0001,skolem0005))&reorganization(skolem0001,skolem0006,skolem0007))&reproducibility(skolem0001,skolem0002,skolem0004))&reproducibility(skolem0001,skolem0003,skolem0005))&~greater(skolem0006,skolem0004))&greater(skolem0005,skolem0004))&~greater(skolem0005,skolem0007))&~greater(skolem0002,skolem0003)),inference(skolemize,[status(esa)],[c4])).
% 1.17/1.47 cnf(c14,negated_conjecture,~greater(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c5])).
% 1.17/1.47 cnf(c7,negated_conjecture,organization(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c5])).
% 1.17/1.47 cnf(c6,negated_conjecture,organization(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c5])).
% 1.17/1.47 fof(mp1,axiom,(![X]:(![T]:(organization(X,T)=>(?[R]:reliability(X,R,T))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp1)).
% 1.17/1.47 fof(c37,plain,(![X]:(![T]:(~organization(X,T)|(?[R]:reliability(X,R,T))))),inference(fof_nnf,[status(thm)],[mp1])).
% 1.17/1.47 fof(c38,plain,(![X34]:(![X35]:(~organization(X34,X35)|(?[X36]:reliability(X34,X36,X35))))),inference(variable_rename,[status(thm)],[c37])).
% 1.17/1.47 fof(c39,plain,(![X34]:(![X35]:(~organization(X34,X35)|reliability(X34,skolem0010(X34,X35),X35)))),inference(skolemize,[status(esa)],[c38])).
% 1.17/1.47 cnf(c40,plain,~organization(X50,X51)|reliability(X50,skolem0010(X50,X51),X51),inference(split_conjunct,[status(thm)],[c39])).
% 1.17/1.47 cnf(c46,plain,reliability(skolem0001,skolem0010(skolem0001,skolem0005),skolem0005),inference(resolution,[status(thm)],[c40, c7])).
% 1.17/1.47 cnf(c13,negated_conjecture,~greater(skolem0005,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 1.17/1.47 cnf(c11,negated_conjecture,~greater(skolem0006,skolem0004),inference(split_conjunct,[status(thm)],[c5])).
% 1.17/1.47 cnf(c12,negated_conjecture,greater(skolem0005,skolem0004),inference(split_conjunct,[status(thm)],[c5])).
% 1.17/1.47 cnf(c8,negated_conjecture,reorganization(skolem0001,skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 1.17/1.47 cnf(c47,plain,reliability(skolem0001,skolem0010(skolem0001,skolem0004),skolem0004),inference(resolution,[status(thm)],[c40, c6])).
% 1.17/1.47 fof(mp2,axiom,(![X]:(![T]:(organization(X,T)=>(?[A]:accountability(X,A,T))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp2)).
% 1.17/1.47 fof(c33,plain,(![X]:(![T]:(~organization(X,T)|(?[A]:accountability(X,A,T))))),inference(fof_nnf,[status(thm)],[mp2])).
% 1.17/1.47 fof(c34,plain,(![X31]:(![X32]:(~organization(X31,X32)|(?[X33]:accountability(X31,X33,X32))))),inference(variable_rename,[status(thm)],[c33])).
% 1.17/1.47 fof(c35,plain,(![X31]:(![X32]:(~organization(X31,X32)|accountability(X31,skolem0009(X31,X32),X32)))),inference(skolemize,[status(esa)],[c34])).
% 1.17/1.47 cnf(c36,plain,~organization(X40,X39)|accountability(X40,skolem0009(X40,X39),X39),inference(split_conjunct,[status(thm)],[c35])).
% 1.17/1.47 cnf(c44,plain,accountability(skolem0001,skolem0009(skolem0001,skolem0004),skolem0004),inference(resolution,[status(thm)],[c36, c6])).
% 1.17/1.47 fof(a6_FOL,plain,(![X]:(![R1]:(![R2]:(![A1]:(![A2]:(![T1]:(![T2]:(![Ta]:(![Tb]:((((((((((organization(X,T1)&organization(X,T2))&reorganization(X,Ta,Tb))&reliability(X,R1,T1))&reliability(X,R2,T2))&accountability(X,A1,T1))&accountability(X,A2,T2))&(~greater(Ta,T1)))&greater(T2,T1))&(~greater(T2,Tb)))=>(greater(R1,R2)&greater(A1,A2)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', a6_FOL)).
% 1.17/1.47 fof(c15,plain,(![X]:(![R1]:(![R2]:(![A1]:(![A2]:(![T1]:(![T2]:(![Ta]:(![Tb]:((((((((((organization(X,T1)&organization(X,T2))&reorganization(X,Ta,Tb))&reliability(X,R1,T1))&reliability(X,R2,T2))&accountability(X,A1,T1))&accountability(X,A2,T2))&~greater(Ta,T1))&greater(T2,T1))&~greater(T2,Tb))=>(greater(R1,R2)&greater(A1,A2)))))))))))),inference(fof_simplification,[status(thm)],[a6_FOL])).
% 1.17/1.47 fof(c16,plain,(![X]:(![R1]:(![R2]:(![A1]:(![A2]:(![T1]:(![T2]:(![Ta]:(![Tb]:((((((((((~organization(X,T1)|~organization(X,T2))|~reorganization(X,Ta,Tb))|~reliability(X,R1,T1))|~reliability(X,R2,T2))|~accountability(X,A1,T1))|~accountability(X,A2,T2))|greater(Ta,T1))|~greater(T2,T1))|greater(T2,Tb))|(greater(R1,R2)&greater(A1,A2)))))))))))),inference(fof_nnf,[status(thm)],[c15])).
% 1.17/1.47 fof(c17,plain,(![X]:(![R1]:(![R2]:(![A1]:(![A2]:((![T1]:(![T2]:(![Ta]:(![Tb]:(((((((((~organization(X,T1)|~organization(X,T2))|~reorganization(X,Ta,Tb))|~reliability(X,R1,T1))|~reliability(X,R2,T2))|~accountability(X,A1,T1))|~accountability(X,A2,T2))|greater(Ta,T1))|~greater(T2,T1))|greater(T2,Tb))))))|(greater(R1,R2)&greater(A1,A2)))))))),inference(shift_quantors,[status(thm)],[c16])).
% 1.17/1.47 fof(c19,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:((((((((((~organization(X9,X14)|~organization(X9,X15))|~reorganization(X9,X16,X17))|~reliability(X9,X10,X14))|~reliability(X9,X11,X15))|~accountability(X9,X12,X14))|~accountability(X9,X13,X15))|greater(X16,X14))|~greater(X15,X14))|greater(X15,X17))|(greater(X10,X11)&greater(X12,X13)))))))))))),inference(shift_quantors,[status(thm)],[fof(c18,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:((![X14]:(![X15]:(![X16]:(![X17]:(((((((((~organization(X9,X14)|~organization(X9,X15))|~reorganization(X9,X16,X17))|~reliability(X9,X10,X14))|~reliability(X9,X11,X15))|~accountability(X9,X12,X14))|~accountability(X9,X13,X15))|greater(X16,X14))|~greater(X15,X14))|greater(X15,X17))))))|(greater(X10,X11)&greater(X12,X13)))))))),inference(variable_rename,[status(thm)],[c17])).])).
% 1.17/1.47 fof(c20,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(((((((((((~organization(X9,X14)|~organization(X9,X15))|~reorganization(X9,X16,X17))|~reliability(X9,X10,X14))|~reliability(X9,X11,X15))|~accountability(X9,X12,X14))|~accountability(X9,X13,X15))|greater(X16,X14))|~greater(X15,X14))|greater(X15,X17))|greater(X10,X11))&((((((((((~organization(X9,X14)|~organization(X9,X15))|~reorganization(X9,X16,X17))|~reliability(X9,X10,X14))|~reliability(X9,X11,X15))|~accountability(X9,X12,X14))|~accountability(X9,X13,X15))|greater(X16,X14))|~greater(X15,X14))|greater(X15,X17))|greater(X12,X13)))))))))))),inference(distribute,[status(thm)],[c19])).
% 1.17/1.47 cnf(c21,plain,~organization(X46,X49)|~organization(X46,X45)|~reorganization(X46,X42,X44)|~reliability(X46,X48,X49)|~reliability(X46,X43,X45)|~accountability(X46,X41,X49)|~accountability(X46,X47,X45)|greater(X42,X49)|~greater(X45,X49)|greater(X45,X44)|greater(X48,X43),inference(split_conjunct,[status(thm)],[c20])).
% 1.17/1.47 cnf(c43,plain,accountability(skolem0001,skolem0009(skolem0001,skolem0005),skolem0005),inference(resolution,[status(thm)],[c36, c7])).
% 1.17/1.47 cnf(c48,plain,~organization(skolem0001,X137)|~organization(skolem0001,skolem0005)|~reorganization(skolem0001,X138,X135)|~reliability(skolem0001,X133,X137)|~reliability(skolem0001,X136,skolem0005)|~accountability(skolem0001,X134,X137)|greater(X138,X137)|~greater(skolem0005,X137)|greater(skolem0005,X135)|greater(X133,X136),inference(resolution,[status(thm)],[c43, c21])).
% 1.17/1.47 cnf(c88,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|~reorganization(skolem0001,X465,X467)|~reliability(skolem0001,X464,skolem0004)|~reliability(skolem0001,X466,skolem0005)|greater(X465,skolem0004)|~greater(skolem0005,skolem0004)|greater(skolem0005,X467)|greater(X464,X466),inference(resolution,[status(thm)],[c48, c44])).
% 1.17/1.47 cnf(c190,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|~reorganization(skolem0001,X469,X470)|~reliability(skolem0001,X468,skolem0004)|greater(X469,skolem0004)|~greater(skolem0005,skolem0004)|greater(skolem0005,X470)|greater(X468,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c88, c46])).
% 1.17/1.47 cnf(c191,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|~reorganization(skolem0001,X471,X472)|greater(X471,skolem0004)|~greater(skolem0005,skolem0004)|greater(skolem0005,X472)|greater(skolem0010(skolem0001,skolem0004),skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c190, c47])).
% 1.17/1.47 cnf(c192,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|greater(skolem0006,skolem0004)|~greater(skolem0005,skolem0004)|greater(skolem0005,skolem0007)|greater(skolem0010(skolem0001,skolem0004),skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c191, c8])).
% 1.17/1.47 cnf(c195,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|greater(skolem0006,skolem0004)|greater(skolem0005,skolem0007)|greater(skolem0010(skolem0001,skolem0004),skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c192, c12])).
% 1.17/1.47 cnf(c196,plain,~organization(skolem0001,skolem0004)|greater(skolem0006,skolem0004)|greater(skolem0005,skolem0007)|greater(skolem0010(skolem0001,skolem0004),skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c195, c7])).
% 1.17/1.47 cnf(c197,plain,greater(skolem0006,skolem0004)|greater(skolem0005,skolem0007)|greater(skolem0010(skolem0001,skolem0004),skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c196, c6])).
% 1.17/1.47 cnf(c198,plain,greater(skolem0005,skolem0007)|greater(skolem0010(skolem0001,skolem0004),skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c197, c11])).
% 1.17/1.47 cnf(c200,plain,greater(skolem0010(skolem0001,skolem0004),skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c198, c13])).
% 1.17/1.47 cnf(c10,negated_conjecture,reproducibility(skolem0001,skolem0003,skolem0005),inference(split_conjunct,[status(thm)],[c5])).
% 1.17/1.47 cnf(c9,negated_conjecture,reproducibility(skolem0001,skolem0002,skolem0004),inference(split_conjunct,[status(thm)],[c5])).
% 1.17/1.47 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)).
% 1.17/1.47 fof(c23,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])).
% 1.17/1.47 fof(c24,plain,(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:((((((((~organization(X18,X20)|~organization(X19,X21))|~reliability(X18,X22,X20))|~reliability(X19,X23,X21))|~accountability(X18,X24,X20))|~accountability(X19,X25,X21))|~reproducibility(X18,X26,X20))|~reproducibility(X19,X27,X21))|((~greater(X27,X26)|(greater(X23,X22)&greater(X25,X24)))&((~greater(X23,X22)|~greater(X25,X24))|greater(X27,X26)))))))))))))),inference(variable_rename,[status(thm)],[c23])).
% 1.17/1.47 fof(c25,plain,(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:((((((((((~organization(X18,X20)|~organization(X19,X21))|~reliability(X18,X22,X20))|~reliability(X19,X23,X21))|~accountability(X18,X24,X20))|~accountability(X19,X25,X21))|~reproducibility(X18,X26,X20))|~reproducibility(X19,X27,X21))|(~greater(X27,X26)|greater(X23,X22)))&((((((((~organization(X18,X20)|~organization(X19,X21))|~reliability(X18,X22,X20))|~reliability(X19,X23,X21))|~accountability(X18,X24,X20))|~accountability(X19,X25,X21))|~reproducibility(X18,X26,X20))|~reproducibility(X19,X27,X21))|(~greater(X27,X26)|greater(X25,X24))))&((((((((~organization(X18,X20)|~organization(X19,X21))|~reliability(X18,X22,X20))|~reliability(X19,X23,X21))|~accountability(X18,X24,X20))|~accountability(X19,X25,X21))|~reproducibility(X18,X26,X20))|~reproducibility(X19,X27,X21))|((~greater(X23,X22)|~greater(X25,X24))|greater(X27,X26)))))))))))))),inference(distribute,[status(thm)],[c24])).
% 1.17/1.47 cnf(c28,plain,~organization(X123,X127)|~organization(X119,X118)|~reliability(X123,X122,X127)|~reliability(X119,X120,X118)|~accountability(X123,X121,X127)|~accountability(X119,X125,X118)|~reproducibility(X123,X124,X127)|~reproducibility(X119,X126,X118)|~greater(X120,X122)|~greater(X125,X121)|greater(X126,X124),inference(split_conjunct,[status(thm)],[c25])).
% 1.17/1.47 cnf(c83,plain,~organization(X436,X439)|~organization(skolem0001,skolem0004)|~reliability(X436,X440,X439)|~reliability(skolem0001,X438,skolem0004)|~accountability(X436,X435,X439)|~accountability(skolem0001,X437,skolem0004)|~reproducibility(X436,X441,X439)|~greater(X438,X440)|~greater(X437,X435)|greater(skolem0002,X441),inference(resolution,[status(thm)],[c28, c9])).
% 1.17/1.47 cnf(c181,plain,~organization(skolem0001,skolem0005)|~organization(skolem0001,skolem0004)|~reliability(skolem0001,X585,skolem0005)|~reliability(skolem0001,X587,skolem0004)|~accountability(skolem0001,X584,skolem0005)|~accountability(skolem0001,X586,skolem0004)|~greater(X587,X585)|~greater(X586,X584)|greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c83, c10])).
% 1.17/1.47 cnf(c236,plain,~organization(skolem0001,skolem0005)|~organization(skolem0001,skolem0004)|~reliability(skolem0001,X588,skolem0005)|~reliability(skolem0001,X590,skolem0004)|~accountability(skolem0001,X589,skolem0005)|~greater(X590,X588)|~greater(skolem0009(skolem0001,skolem0004),X589)|greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c181, c44])).
% 1.17/1.47 cnf(c22,plain,~organization(X57,X60)|~organization(X57,X56)|~reorganization(X57,X53,X55)|~reliability(X57,X59,X60)|~reliability(X57,X54,X56)|~accountability(X57,X52,X60)|~accountability(X57,X58,X56)|greater(X53,X60)|~greater(X56,X60)|greater(X56,X55)|greater(X52,X58),inference(split_conjunct,[status(thm)],[c20])).
% 1.17/1.47 cnf(c51,plain,~organization(skolem0001,X173)|~organization(skolem0001,skolem0005)|~reorganization(skolem0001,X171,X175)|~reliability(skolem0001,X170,X173)|~reliability(skolem0001,X172,skolem0005)|~accountability(skolem0001,X174,X173)|greater(X171,X173)|~greater(skolem0005,X173)|greater(skolem0005,X175)|greater(X174,skolem0009(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c22, c43])).
% 1.17/1.47 cnf(c105,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|~reorganization(skolem0001,X509,X510)|~reliability(skolem0001,X507,skolem0004)|~reliability(skolem0001,X508,skolem0005)|greater(X509,skolem0004)|~greater(skolem0005,skolem0004)|greater(skolem0005,X510)|greater(skolem0009(skolem0001,skolem0004),skolem0009(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c51, c44])).
% 1.17/1.47 cnf(c211,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|~reorganization(skolem0001,X615,X616)|~reliability(skolem0001,X614,skolem0004)|greater(X615,skolem0004)|~greater(skolem0005,skolem0004)|greater(skolem0005,X616)|greater(skolem0009(skolem0001,skolem0004),skolem0009(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c105, c46])).
% 1.17/1.47 cnf(c243,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|~reorganization(skolem0001,X622,X621)|greater(X622,skolem0004)|~greater(skolem0005,skolem0004)|greater(skolem0005,X621)|greater(skolem0009(skolem0001,skolem0004),skolem0009(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c211, c47])).
% 1.17/1.47 cnf(c245,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|greater(skolem0006,skolem0004)|~greater(skolem0005,skolem0004)|greater(skolem0005,skolem0007)|greater(skolem0009(skolem0001,skolem0004),skolem0009(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c243, c8])).
% 1.17/1.47 cnf(c246,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|greater(skolem0006,skolem0004)|greater(skolem0005,skolem0007)|greater(skolem0009(skolem0001,skolem0004),skolem0009(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c245, c12])).
% 1.17/1.47 cnf(c247,plain,~organization(skolem0001,skolem0004)|greater(skolem0006,skolem0004)|greater(skolem0005,skolem0007)|greater(skolem0009(skolem0001,skolem0004),skolem0009(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c246, c7])).
% 1.17/1.47 cnf(c248,plain,greater(skolem0006,skolem0004)|greater(skolem0005,skolem0007)|greater(skolem0009(skolem0001,skolem0004),skolem0009(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c247, c6])).
% 1.17/1.47 cnf(c249,plain,greater(skolem0005,skolem0007)|greater(skolem0009(skolem0001,skolem0004),skolem0009(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c248, c11])).
% 1.17/1.47 cnf(c257,plain,greater(skolem0009(skolem0001,skolem0004),skolem0009(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c249, c13])).
% 1.17/1.47 cnf(c264,plain,~organization(skolem0001,skolem0005)|~organization(skolem0001,skolem0004)|~reliability(skolem0001,X639,skolem0005)|~reliability(skolem0001,X640,skolem0004)|~accountability(skolem0001,skolem0009(skolem0001,skolem0005),skolem0005)|~greater(X640,X639)|greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c257, c236])).
% 1.17/1.47 cnf(c269,plain,~organization(skolem0001,skolem0005)|~organization(skolem0001,skolem0004)|~reliability(skolem0001,X642,skolem0005)|~reliability(skolem0001,X641,skolem0004)|~greater(X641,X642)|greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c264, c43])).
% 1.17/1.47 cnf(c270,plain,~organization(skolem0001,skolem0005)|~organization(skolem0001,skolem0004)|~reliability(skolem0001,X643,skolem0005)|~greater(skolem0010(skolem0001,skolem0004),X643)|greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c269, c47])).
% 1.17/1.47 cnf(c271,plain,~organization(skolem0001,skolem0005)|~organization(skolem0001,skolem0004)|~reliability(skolem0001,skolem0010(skolem0001,skolem0005),skolem0005)|greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c270, c200])).
% 1.17/1.47 cnf(c272,plain,~organization(skolem0001,skolem0005)|~organization(skolem0001,skolem0004)|greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c271, c46])).
% 1.17/1.47 cnf(c273,plain,~organization(skolem0001,skolem0005)|greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c272, c6])).
% 1.17/1.47 cnf(c274,plain,greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c273, c7])).
% 1.17/1.47 cnf(c275,plain,$false,inference(resolution,[status(thm)],[c274, c14])).
% 1.17/1.47 % SZS output end CNFRefutation
% 1.17/1.47
% 1.17/1.47 % Initial clauses : 17
% 1.17/1.47 % Processed clauses : 197
% 1.17/1.47 % Factors computed : 49
% 1.17/1.47 % Resolvents computed: 186
% 1.17/1.47 % Tautologies deleted: 0
% 1.17/1.47 % Forward subsumed : 35
% 1.17/1.47 % Backward subsumed : 39
% 1.17/1.47 % -------- CPU Time ---------
% 1.17/1.47 % User time : 1.087 s
% 1.17/1.47 % System time : 0.026 s
% 1.17/1.47 % Total time : 1.113 s
%------------------------------------------------------------------------------