%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT004+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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.47s 0.80s
% Output : CNFRefutation 0.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT004+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.34 % Computer : n010.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 7 11:35:41 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.13/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.40 (re.compile("\."), Token.FullStop),
% 0.13/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.40 (re.compile("\("), Token.OpenPar),
% 0.13/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.40 (re.compile("\)"), Token.ClosePar),
% 0.13/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.40 (re.compile("\["), Token.OpenSquare),
% 0.13/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.40 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.40 (re.compile("~\|"), Token.Nor),
% 0.13/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.40 (re.compile("\|"), Token.Or),
% 0.13/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.40 (re.compile("\?"), Token.Existential),
% 0.13/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.40 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.40 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.24/0.47 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.24/0.47 """
% 0.24/0.48 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.24/0.48 """
% 0.34/0.57 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.34/0.57 """
% 0.47/0.80 % Version: 1.5
% 0.47/0.80 % SZS status Theorem
% 0.47/0.80 % SZS output start CNFRefutation
% 0.47/0.80 fof(t4_FOL,conjecture,(![X]:(![P1]:(![P2]:(![T1]:(![T2]:(![Ta]:(![Tb]:((((((((organization(X,T1)&organization(X,T2))&reorganization(X,Ta,Tb))&survival_chance(X,P1,T1))&survival_chance(X,P2,T2))&(~greater(Ta,T1)))&greater(T2,T1))&(~greater(T2,Tb)))=>greater(P1,P2))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t4_FOL)).
% 0.47/0.80 fof(c0,negated_conjecture,(~(![X]:(![P1]:(![P2]:(![T1]:(![T2]:(![Ta]:(![Tb]:((((((((organization(X,T1)&organization(X,T2))&reorganization(X,Ta,Tb))&survival_chance(X,P1,T1))&survival_chance(X,P2,T2))&(~greater(Ta,T1)))&greater(T2,T1))&(~greater(T2,Tb)))=>greater(P1,P2)))))))))),inference(assume_negation,[status(cth)],[t4_FOL])).
% 0.47/0.80 fof(c1,negated_conjecture,(~(![X]:(![P1]:(![P2]:(![T1]:(![T2]:(![Ta]:(![Tb]:((((((((organization(X,T1)&organization(X,T2))&reorganization(X,Ta,Tb))&survival_chance(X,P1,T1))&survival_chance(X,P2,T2))&~greater(Ta,T1))&greater(T2,T1))&~greater(T2,Tb))=>greater(P1,P2)))))))))),inference(fof_simplification,[status(thm)],[c0])).
% 0.47/0.80 fof(c2,negated_conjecture,(?[X]:(?[P1]:(?[P2]:(?[T1]:(?[T2]:(?[Ta]:(?[Tb]:((((((((organization(X,T1)&organization(X,T2))&reorganization(X,Ta,Tb))&survival_chance(X,P1,T1))&survival_chance(X,P2,T2))&~greater(Ta,T1))&greater(T2,T1))&~greater(T2,Tb))&~greater(P1,P2))))))))),inference(fof_nnf,[status(thm)],[c1])).
% 0.47/0.80 fof(c3,negated_conjecture,(?[X]:(?[P1]:(?[P2]:((?[T1]:(?[T2]:(?[Ta]:(?[Tb]:(((((((organization(X,T1)&organization(X,T2))&reorganization(X,Ta,Tb))&survival_chance(X,P1,T1))&survival_chance(X,P2,T2))&~greater(Ta,T1))&greater(T2,T1))&~greater(T2,Tb))))))&~greater(P1,P2))))),inference(shift_quantors,[status(thm)],[c2])).
% 0.47/0.80 fof(c4,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((?[X5]:(?[X6]:(?[X7]:(?[X8]:(((((((organization(X2,X5)&organization(X2,X6))&reorganization(X2,X7,X8))&survival_chance(X2,X3,X5))&survival_chance(X2,X4,X6))&~greater(X7,X5))&greater(X6,X5))&~greater(X6,X8))))))&~greater(X3,X4))))),inference(variable_rename,[status(thm)],[c3])).
% 0.47/0.80 fof(c5,negated_conjecture,((((((((organization(skolem0001,skolem0004)&organization(skolem0001,skolem0005))&reorganization(skolem0001,skolem0006,skolem0007))&survival_chance(skolem0001,skolem0002,skolem0004))&survival_chance(skolem0001,skolem0003,skolem0005))&~greater(skolem0006,skolem0004))&greater(skolem0005,skolem0004))&~greater(skolem0005,skolem0007))&~greater(skolem0002,skolem0003)),inference(skolemize,[status(esa)],[c4])).
% 0.47/0.80 cnf(c14,negated_conjecture,~greater(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c5])).
% 0.47/0.80 cnf(c7,negated_conjecture,organization(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c5])).
% 0.47/0.80 cnf(c6,negated_conjecture,organization(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c5])).
% 0.47/0.80 fof(mp1,axiom,(![X]:(![T]:(organization(X,T)=>(?[R]:reliability(X,R,T))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp1)).
% 0.47/0.80 fof(c32,plain,(![X]:(![T]:(~organization(X,T)|(?[R]:reliability(X,R,T))))),inference(fof_nnf,[status(thm)],[mp1])).
% 0.47/0.80 fof(c33,plain,(![X31]:(![X32]:(~organization(X31,X32)|(?[X33]:reliability(X31,X33,X32))))),inference(variable_rename,[status(thm)],[c32])).
% 0.47/0.80 fof(c34,plain,(![X31]:(![X32]:(~organization(X31,X32)|reliability(X31,skolem0009(X31,X32),X32)))),inference(skolemize,[status(esa)],[c33])).
% 0.47/0.80 cnf(c35,plain,~organization(X37,X36)|reliability(X37,skolem0009(X37,X36),X36),inference(split_conjunct,[status(thm)],[c34])).
% 0.47/0.80 cnf(c38,plain,reliability(skolem0001,skolem0009(skolem0001,skolem0005),skolem0005),inference(resolution,[status(thm)],[c35, c7])).
% 0.47/0.80 cnf(c13,negated_conjecture,~greater(skolem0005,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 0.47/0.80 cnf(c11,negated_conjecture,~greater(skolem0006,skolem0004),inference(split_conjunct,[status(thm)],[c5])).
% 0.47/0.80 cnf(c12,negated_conjecture,greater(skolem0005,skolem0004),inference(split_conjunct,[status(thm)],[c5])).
% 0.47/0.80 cnf(c8,negated_conjecture,reorganization(skolem0001,skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 0.47/0.80 cnf(c39,plain,reliability(skolem0001,skolem0009(skolem0001,skolem0004),skolem0004),inference(resolution,[status(thm)],[c35, c6])).
% 0.47/0.80 fof(mp2,axiom,(![X]:(![T]:(organization(X,T)=>(?[A]:accountability(X,A,T))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp2)).
% 0.47/0.80 fof(c28,plain,(![X]:(![T]:(~organization(X,T)|(?[A]:accountability(X,A,T))))),inference(fof_nnf,[status(thm)],[mp2])).
% 0.47/0.80 fof(c29,plain,(![X28]:(![X29]:(~organization(X28,X29)|(?[X30]:accountability(X28,X30,X29))))),inference(variable_rename,[status(thm)],[c28])).
% 0.47/0.80 fof(c30,plain,(![X28]:(![X29]:(~organization(X28,X29)|accountability(X28,skolem0008(X28,X29),X29)))),inference(skolemize,[status(esa)],[c29])).
% 0.47/0.80 cnf(c31,plain,~organization(X35,X34)|accountability(X35,skolem0008(X35,X34),X34),inference(split_conjunct,[status(thm)],[c30])).
% 0.47/0.80 cnf(c37,plain,accountability(skolem0001,skolem0008(skolem0001,skolem0004),skolem0004),inference(resolution,[status(thm)],[c31, c6])).
% 0.47/0.80 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/sandbox2/benchmark/theBenchmark.p', a6_FOL)).
% 0.47/0.80 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])).
% 0.47/0.80 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])).
% 0.47/0.80 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])).
% 0.47/0.80 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])).])).
% 0.47/0.80 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])).
% 0.57/0.80 cnf(c21,plain,~organization(X40,X45)|~organization(X40,X41)|~reorganization(X40,X44,X46)|~reliability(X40,X39,X45)|~reliability(X40,X43,X41)|~accountability(X40,X38,X45)|~accountability(X40,X42,X41)|greater(X44,X45)|~greater(X41,X45)|greater(X41,X46)|greater(X39,X43),inference(split_conjunct,[status(thm)],[c20])).
% 0.57/0.80 cnf(c36,plain,accountability(skolem0001,skolem0008(skolem0001,skolem0005),skolem0005),inference(resolution,[status(thm)],[c31, c7])).
% 0.57/0.80 cnf(c41,plain,~organization(skolem0001,X109)|~organization(skolem0001,skolem0005)|~reorganization(skolem0001,X113,X111)|~reliability(skolem0001,X112,X109)|~reliability(skolem0001,X108,skolem0005)|~accountability(skolem0001,X110,X109)|greater(X113,X109)|~greater(skolem0005,X109)|greater(skolem0005,X111)|greater(X112,X108),inference(resolution,[status(thm)],[c36, c21])).
% 0.57/0.80 cnf(c63,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|~reorganization(skolem0001,X221,X219)|~reliability(skolem0001,X220,skolem0004)|~reliability(skolem0001,X222,skolem0005)|greater(X221,skolem0004)|~greater(skolem0005,skolem0004)|greater(skolem0005,X219)|greater(X220,X222),inference(resolution,[status(thm)],[c41, c37])).
% 0.57/0.80 cnf(c97,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|~reorganization(skolem0001,X224,X223)|~reliability(skolem0001,X225,skolem0004)|greater(X224,skolem0004)|~greater(skolem0005,skolem0004)|greater(skolem0005,X223)|greater(X225,skolem0009(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c63, c38])).
% 0.57/0.80 cnf(c98,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|~reorganization(skolem0001,X226,X227)|greater(X226,skolem0004)|~greater(skolem0005,skolem0004)|greater(skolem0005,X227)|greater(skolem0009(skolem0001,skolem0004),skolem0009(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c97, c39])).
% 0.57/0.80 cnf(c99,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)],[c98, c8])).
% 0.57/0.80 cnf(c100,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|greater(skolem0006,skolem0004)|greater(skolem0005,skolem0007)|greater(skolem0009(skolem0001,skolem0004),skolem0009(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c99, c12])).
% 0.57/0.80 cnf(c102,plain,~organization(skolem0001,skolem0004)|greater(skolem0006,skolem0004)|greater(skolem0005,skolem0007)|greater(skolem0009(skolem0001,skolem0004),skolem0009(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c100, c7])).
% 0.57/0.80 cnf(c103,plain,greater(skolem0006,skolem0004)|greater(skolem0005,skolem0007)|greater(skolem0009(skolem0001,skolem0004),skolem0009(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c102, c6])).
% 0.57/0.80 cnf(c104,plain,greater(skolem0005,skolem0007)|greater(skolem0009(skolem0001,skolem0004),skolem0009(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c103, c11])).
% 0.57/0.80 cnf(c106,plain,greater(skolem0009(skolem0001,skolem0004),skolem0009(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c104, c13])).
% 0.57/0.80 cnf(c10,negated_conjecture,survival_chance(skolem0001,skolem0003,skolem0005),inference(split_conjunct,[status(thm)],[c5])).
% 0.57/0.80 cnf(c9,negated_conjecture,survival_chance(skolem0001,skolem0002,skolem0004),inference(split_conjunct,[status(thm)],[c5])).
% 0.57/0.80 fof(a1_FOL,plain,(![X]:(![Y]:(![R1]:(![R2]:(![A1]:(![A2]:(![P1]:(![P2]:(![T1]:(![T2]:((((((((((organization(X,T1)&organization(Y,T2))&reliability(X,R1,T1))&reliability(Y,R2,T2))&accountability(X,A1,T1))&accountability(Y,A2,T2))&survival_chance(X,P1,T1))&survival_chance(Y,P2,T2))&greater(R2,R1))&greater(A2,A1))=>greater(P2,P1)))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a1_FOL)).
% 0.57/0.80 fof(c23,plain,(![X]:(![Y]:(![R1]:(![R2]:(![A1]:(![A2]:(![P1]:(![P2]:(![T1]:(![T2]:((((((((((~organization(X,T1)|~organization(Y,T2))|~reliability(X,R1,T1))|~reliability(Y,R2,T2))|~accountability(X,A1,T1))|~accountability(Y,A2,T2))|~survival_chance(X,P1,T1))|~survival_chance(Y,P2,T2))|~greater(R2,R1))|~greater(A2,A1))|greater(P2,P1)))))))))))),inference(fof_nnf,[status(thm)],[a1_FOL])).
% 0.57/0.80 fof(c24,plain,(![X]:(![Y]:(![R1]:(![R2]:(![A1]:(![A2]:(![P1]:(![P2]:((((![T1]:(![T2]:(((((((~organization(X,T1)|~organization(Y,T2))|~reliability(X,R1,T1))|~reliability(Y,R2,T2))|~accountability(X,A1,T1))|~accountability(Y,A2,T2))|~survival_chance(X,P1,T1))|~survival_chance(Y,P2,T2))))|~greater(R2,R1))|~greater(A2,A1))|greater(P2,P1)))))))))),inference(shift_quantors,[status(thm)],[c23])).
% 0.57/0.80 fof(c26,plain,(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:((((((((((~organization(X18,X26)|~organization(X19,X27))|~reliability(X18,X20,X26))|~reliability(X19,X21,X27))|~accountability(X18,X22,X26))|~accountability(X19,X23,X27))|~survival_chance(X18,X24,X26))|~survival_chance(X19,X25,X27))|~greater(X21,X20))|~greater(X23,X22))|greater(X25,X24)))))))))))),inference(shift_quantors,[status(thm)],[fof(c25,plain,(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:((((![X26]:(![X27]:(((((((~organization(X18,X26)|~organization(X19,X27))|~reliability(X18,X20,X26))|~reliability(X19,X21,X27))|~accountability(X18,X22,X26))|~accountability(X19,X23,X27))|~survival_chance(X18,X24,X26))|~survival_chance(X19,X25,X27))))|~greater(X21,X20))|~greater(X23,X22))|greater(X25,X24)))))))))),inference(variable_rename,[status(thm)],[c24])).])).
% 0.57/0.80 cnf(c27,plain,~organization(X79,X85)|~organization(X84,X80)|~reliability(X79,X83,X85)|~reliability(X84,X82,X80)|~accountability(X79,X87,X85)|~accountability(X84,X81,X80)|~survival_chance(X79,X86,X85)|~survival_chance(X84,X88,X80)|~greater(X82,X83)|~greater(X81,X87)|greater(X88,X86),inference(split_conjunct,[status(thm)],[c26])).
% 0.57/0.80 cnf(c56,plain,~organization(X209,X214)|~organization(skolem0001,skolem0004)|~reliability(X209,X212,X214)|~reliability(skolem0001,X211,skolem0004)|~accountability(X209,X208,X214)|~accountability(skolem0001,X210,skolem0004)|~survival_chance(X209,X213,X214)|~greater(X211,X212)|~greater(X210,X208)|greater(skolem0002,X213),inference(resolution,[status(thm)],[c27, c9])).
% 0.57/0.80 cnf(c95,plain,~organization(skolem0001,skolem0005)|~organization(skolem0001,skolem0004)|~reliability(skolem0001,X253,skolem0005)|~reliability(skolem0001,X255,skolem0004)|~accountability(skolem0001,X254,skolem0005)|~accountability(skolem0001,X256,skolem0004)|~greater(X255,X253)|~greater(X256,X254)|greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c56, c10])).
% 0.57/0.80 cnf(c112,plain,~organization(skolem0001,skolem0005)|~organization(skolem0001,skolem0004)|~reliability(skolem0001,X257,skolem0005)|~reliability(skolem0001,X259,skolem0004)|~accountability(skolem0001,X258,skolem0005)|~greater(X259,X257)|~greater(skolem0008(skolem0001,skolem0004),X258)|greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c95, c37])).
% 0.57/0.80 cnf(c22,plain,~organization(X56,X61)|~organization(X56,X57)|~reorganization(X56,X60,X62)|~reliability(X56,X55,X61)|~reliability(X56,X59,X57)|~accountability(X56,X54,X61)|~accountability(X56,X58,X57)|greater(X60,X61)|~greater(X57,X61)|greater(X57,X62)|greater(X54,X58),inference(split_conjunct,[status(thm)],[c20])).
% 0.57/0.80 cnf(c47,plain,~organization(skolem0001,X168)|~organization(skolem0001,skolem0005)|~reorganization(skolem0001,X163,X165)|~reliability(skolem0001,X167,X168)|~reliability(skolem0001,X164,skolem0005)|~accountability(skolem0001,X166,X168)|greater(X163,X168)|~greater(skolem0005,X168)|greater(skolem0005,X165)|greater(X166,skolem0008(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c22, c36])).
% 0.57/0.80 cnf(c81,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|~reorganization(skolem0001,X262,X261)|~reliability(skolem0001,X264,skolem0004)|~reliability(skolem0001,X263,skolem0005)|greater(X262,skolem0004)|~greater(skolem0005,skolem0004)|greater(skolem0005,X261)|greater(skolem0008(skolem0001,skolem0004),skolem0008(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c47, c37])).
% 0.57/0.80 cnf(c114,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|~reorganization(skolem0001,X271,X270)|~reliability(skolem0001,X272,skolem0004)|greater(X271,skolem0004)|~greater(skolem0005,skolem0004)|greater(skolem0005,X270)|greater(skolem0008(skolem0001,skolem0004),skolem0008(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c81, c38])).
% 0.57/0.80 cnf(c117,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|~reorganization(skolem0001,X274,X273)|greater(X274,skolem0004)|~greater(skolem0005,skolem0004)|greater(skolem0005,X273)|greater(skolem0008(skolem0001,skolem0004),skolem0008(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c114, c39])).
% 0.57/0.80 cnf(c118,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|greater(skolem0006,skolem0004)|~greater(skolem0005,skolem0004)|greater(skolem0005,skolem0007)|greater(skolem0008(skolem0001,skolem0004),skolem0008(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c117, c8])).
% 0.57/0.80 cnf(c119,plain,~organization(skolem0001,skolem0004)|~organization(skolem0001,skolem0005)|greater(skolem0006,skolem0004)|greater(skolem0005,skolem0007)|greater(skolem0008(skolem0001,skolem0004),skolem0008(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c118, c12])).
% 0.57/0.80 cnf(c120,plain,~organization(skolem0001,skolem0004)|greater(skolem0006,skolem0004)|greater(skolem0005,skolem0007)|greater(skolem0008(skolem0001,skolem0004),skolem0008(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c119, c7])).
% 0.57/0.80 cnf(c121,plain,greater(skolem0006,skolem0004)|greater(skolem0005,skolem0007)|greater(skolem0008(skolem0001,skolem0004),skolem0008(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c120, c6])).
% 0.57/0.80 cnf(c122,plain,greater(skolem0005,skolem0007)|greater(skolem0008(skolem0001,skolem0004),skolem0008(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c121, c11])).
% 0.57/0.80 cnf(c126,plain,greater(skolem0008(skolem0001,skolem0004),skolem0008(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c122, c13])).
% 0.57/0.80 cnf(c133,plain,~organization(skolem0001,skolem0005)|~organization(skolem0001,skolem0004)|~reliability(skolem0001,X288,skolem0005)|~reliability(skolem0001,X287,skolem0004)|~accountability(skolem0001,skolem0008(skolem0001,skolem0005),skolem0005)|~greater(X287,X288)|greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c126, c112])).
% 0.57/0.80 cnf(c134,plain,~organization(skolem0001,skolem0005)|~organization(skolem0001,skolem0004)|~reliability(skolem0001,X289,skolem0005)|~reliability(skolem0001,X290,skolem0004)|~greater(X290,X289)|greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c133, c36])).
% 0.57/0.80 cnf(c135,plain,~organization(skolem0001,skolem0005)|~organization(skolem0001,skolem0004)|~reliability(skolem0001,X291,skolem0005)|~greater(skolem0009(skolem0001,skolem0004),X291)|greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c134, c39])).
% 0.57/0.80 cnf(c136,plain,~organization(skolem0001,skolem0005)|~organization(skolem0001,skolem0004)|~reliability(skolem0001,skolem0009(skolem0001,skolem0005),skolem0005)|greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c135, c106])).
% 0.57/0.80 cnf(c137,plain,~organization(skolem0001,skolem0005)|~organization(skolem0001,skolem0004)|greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c136, c38])).
% 0.57/0.80 cnf(c138,plain,~organization(skolem0001,skolem0005)|greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c137, c6])).
% 0.57/0.80 cnf(c139,plain,greater(skolem0002,skolem0003),inference(resolution,[status(thm)],[c138, c7])).
% 0.57/0.80 cnf(c140,plain,$false,inference(resolution,[status(thm)],[c139, c14])).
% 0.57/0.80 % SZS output end CNFRefutation
% 0.57/0.80
% 0.57/0.80 % Initial clauses : 14
% 0.57/0.80 % Processed clauses : 98
% 0.57/0.80 % Factors computed : 17
% 0.57/0.80 % Resolvents computed: 88
% 0.57/0.80 % Tautologies deleted: 0
% 0.57/0.80 % Forward subsumed : 18
% 0.57/0.80 % Backward subsumed : 30
% 0.57/0.80 % -------- CPU Time ---------
% 0.57/0.80 % User time : 0.425 s
% 0.57/0.80 % System time : 0.029 s
% 0.57/0.80 % Total time : 0.454 s
%------------------------------------------------------------------------------