%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT001+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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:36 AM UTC 2026
% Result : Theorem 0.56s 0.88s
% Output : CNFRefutation 0.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT001+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 : n028.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.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 7 11:35:17 UTC 2026
% 0.09/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.42 (re.compile("\?"), Token.Existential),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.13/0.49 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.13/0.49 """
% 0.13/0.49 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.13/0.49 """
% 0.25/0.58 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.25/0.58 """
% 0.56/0.88 % Version: 1.5
% 0.56/0.88 % SZS status Theorem
% 0.56/0.88 % SZS output start CNFRefutation
% 0.56/0.88 fof(t1_FOL,conjecture,(![X]:(![Y]:(![T1]:(![T2]:(![I1]:(![I2]:(![P1]:(![P2]:(((((((((organization(X,T1)&organization(Y,T2))&reorganization_free(X,T1,T1))&reorganization_free(Y,T2,T2))&inertia(X,I1,T1))&inertia(Y,I2,T2))&survival_chance(X,P1,T1))&survival_chance(Y,P2,T2))&greater(I2,I1))=>greater(P2,P1)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t1_FOL)).
% 0.56/0.88 fof(c0,negated_conjecture,(~(![X]:(![Y]:(![T1]:(![T2]:(![I1]:(![I2]:(![P1]:(![P2]:(((((((((organization(X,T1)&organization(Y,T2))&reorganization_free(X,T1,T1))&reorganization_free(Y,T2,T2))&inertia(X,I1,T1))&inertia(Y,I2,T2))&survival_chance(X,P1,T1))&survival_chance(Y,P2,T2))&greater(I2,I1))=>greater(P2,P1))))))))))),inference(assume_negation,[status(cth)],[t1_FOL])).
% 0.56/0.88 fof(c1,negated_conjecture,(?[X]:(?[Y]:(?[T1]:(?[T2]:(?[I1]:(?[I2]:(?[P1]:(?[P2]:(((((((((organization(X,T1)&organization(Y,T2))&reorganization_free(X,T1,T1))&reorganization_free(Y,T2,T2))&inertia(X,I1,T1))&inertia(Y,I2,T2))&survival_chance(X,P1,T1))&survival_chance(Y,P2,T2))&greater(I2,I1))&~greater(P2,P1)))))))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.56/0.88 fof(c2,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(((((((((organization(X2,X4)&organization(X3,X5))&reorganization_free(X2,X4,X4))&reorganization_free(X3,X5,X5))&inertia(X2,X6,X4))&inertia(X3,X7,X5))&survival_chance(X2,X8,X4))&survival_chance(X3,X9,X5))&greater(X7,X6))&~greater(X9,X8)))))))))),inference(variable_rename,[status(thm)],[c1])).
% 0.56/0.88 fof(c3,negated_conjecture,(((((((((organization(skolem0001,skolem0003)&organization(skolem0002,skolem0004))&reorganization_free(skolem0001,skolem0003,skolem0003))&reorganization_free(skolem0002,skolem0004,skolem0004))&inertia(skolem0001,skolem0005,skolem0003))&inertia(skolem0002,skolem0006,skolem0004))&survival_chance(skolem0001,skolem0007,skolem0003))&survival_chance(skolem0002,skolem0008,skolem0004))&greater(skolem0006,skolem0005))&~greater(skolem0008,skolem0007)),inference(skolemize,[status(esa)],[c2])).
% 0.56/0.88 cnf(c13,negated_conjecture,~greater(skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c3])).
% 0.56/0.88 cnf(c4,negated_conjecture,organization(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c3])).
% 0.56/0.88 cnf(c5,negated_conjecture,organization(skolem0002,skolem0004),inference(split_conjunct,[status(thm)],[c3])).
% 0.56/0.88 fof(mp1,axiom,(![X]:(![T]:(organization(X,T)=>(?[R]:reliability(X,R,T))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp1)).
% 0.56/0.88 fof(c38,plain,(![X]:(![T]:(~organization(X,T)|(?[R]:reliability(X,R,T))))),inference(fof_nnf,[status(thm)],[mp1])).
% 0.56/0.88 fof(c39,plain,(![X44]:(![X45]:(~organization(X44,X45)|(?[X46]:reliability(X44,X46,X45))))),inference(variable_rename,[status(thm)],[c38])).
% 0.56/0.88 fof(c40,plain,(![X44]:(![X45]:(~organization(X44,X45)|reliability(X44,skolem0011(X44,X45),X45)))),inference(skolemize,[status(esa)],[c39])).
% 0.56/0.88 cnf(c41,plain,~organization(X59,X60)|reliability(X59,skolem0011(X59,X60),X60),inference(split_conjunct,[status(thm)],[c40])).
% 0.56/0.88 cnf(c49,plain,reliability(skolem0001,skolem0011(skolem0001,skolem0003),skolem0003),inference(resolution,[status(thm)],[c41, c4])).
% 0.56/0.88 cnf(c50,plain,reliability(skolem0002,skolem0011(skolem0002,skolem0004),skolem0004),inference(resolution,[status(thm)],[c41, c5])).
% 0.56/0.88 fof(mp2,axiom,(![X]:(![T]:(organization(X,T)=>(?[A]:accountability(X,A,T))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp2)).
% 0.56/0.88 fof(c34,plain,(![X]:(![T]:(~organization(X,T)|(?[A]:accountability(X,A,T))))),inference(fof_nnf,[status(thm)],[mp2])).
% 0.56/0.88 fof(c35,plain,(![X41]:(![X42]:(~organization(X41,X42)|(?[X43]:accountability(X41,X43,X42))))),inference(variable_rename,[status(thm)],[c34])).
% 0.56/0.88 fof(c36,plain,(![X41]:(![X42]:(~organization(X41,X42)|accountability(X41,skolem0010(X41,X42),X42)))),inference(skolemize,[status(esa)],[c35])).
% 0.56/0.88 cnf(c37,plain,~organization(X58,X57)|accountability(X58,skolem0010(X58,X57),X57),inference(split_conjunct,[status(thm)],[c36])).
% 0.56/0.88 cnf(c47,plain,accountability(skolem0001,skolem0010(skolem0001,skolem0003),skolem0003),inference(resolution,[status(thm)],[c37, c4])).
% 0.56/0.88 cnf(c48,plain,accountability(skolem0002,skolem0010(skolem0002,skolem0004),skolem0004),inference(resolution,[status(thm)],[c37, c5])).
% 0.56/0.88 fof(mp3,axiom,(![X]:(![T]:(organization(X,T)=>(?[Rp]:reproducibility(X,Rp,T))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp3)).
% 0.56/0.88 fof(c30,plain,(![X]:(![T]:(~organization(X,T)|(?[Rp]:reproducibility(X,Rp,T))))),inference(fof_nnf,[status(thm)],[mp3])).
% 0.56/0.88 fof(c31,plain,(![X38]:(![X39]:(~organization(X38,X39)|(?[X40]:reproducibility(X38,X40,X39))))),inference(variable_rename,[status(thm)],[c30])).
% 0.56/0.88 fof(c32,plain,(![X38]:(![X39]:(~organization(X38,X39)|reproducibility(X38,skolem0009(X38,X39),X39)))),inference(skolemize,[status(esa)],[c31])).
% 0.56/0.88 cnf(c33,plain,~organization(X48,X47)|reproducibility(X48,skolem0009(X48,X47),X47),inference(split_conjunct,[status(thm)],[c32])).
% 0.56/0.88 cnf(c42,plain,reproducibility(skolem0001,skolem0009(skolem0001,skolem0003),skolem0003),inference(resolution,[status(thm)],[c33, c4])).
% 0.56/0.88 cnf(c43,plain,reproducibility(skolem0002,skolem0009(skolem0002,skolem0004),skolem0004),inference(resolution,[status(thm)],[c33, c5])).
% 0.56/0.88 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.56/0.88 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.56/0.88 fof(c20,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)],[c19])).
% 0.56/0.88 fof(c21,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)],[c20])).
% 0.56/0.88 cnf(c22,plain,~organization(X82,X79)|~organization(X80,X84)|~reliability(X82,X88,X79)|~reliability(X80,X83,X84)|~accountability(X82,X85,X79)|~accountability(X80,X81,X84)|~reproducibility(X82,X87,X79)|~reproducibility(X80,X86,X84)|~greater(X86,X87)|greater(X83,X88),inference(split_conjunct,[status(thm)],[c21])).
% 0.56/0.88 cnf(c60,plain,~organization(X228,X224)|~organization(skolem0002,skolem0004)|~reliability(X228,X227,X224)|~reliability(skolem0002,X230,skolem0004)|~accountability(X228,X226,X224)|~accountability(skolem0002,X229,skolem0004)|~reproducibility(X228,X225,X224)|~greater(skolem0009(skolem0002,skolem0004),X225)|greater(X230,X227),inference(resolution,[status(thm)],[c22, c43])).
% 0.56/0.88 cnf(c12,negated_conjecture,greater(skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c3])).
% 0.56/0.88 cnf(c6,negated_conjecture,reorganization_free(skolem0001,skolem0003,skolem0003),inference(split_conjunct,[status(thm)],[c3])).
% 0.56/0.88 cnf(c7,negated_conjecture,reorganization_free(skolem0002,skolem0004,skolem0004),inference(split_conjunct,[status(thm)],[c3])).
% 0.56/0.88 cnf(c8,negated_conjecture,inertia(skolem0001,skolem0005,skolem0003),inference(split_conjunct,[status(thm)],[c3])).
% 0.56/0.88 cnf(c9,negated_conjecture,inertia(skolem0002,skolem0006,skolem0004),inference(split_conjunct,[status(thm)],[c3])).
% 0.56/0.88 fof(a3_FOL,plain,(![X]:(![Y]:(![T1]:(![T2]:(![Rp1]:(![Rp2]:(![I1]:(![I2]:((((((((organization(X,T1)&organization(Y,T2))&reorganization_free(X,T1,T1))&reorganization_free(Y,T2,T2))&reproducibility(X,Rp1,T1))&reproducibility(Y,Rp2,T2))&inertia(X,I1,T1))&inertia(Y,I2,T2))=>(greater(Rp2,Rp1)<=>greater(I2,I1))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a3_FOL)).
% 0.56/0.88 fof(c14,plain,(![X]:(![Y]:(![T1]:(![T2]:(![Rp1]:(![Rp2]:(![I1]:(![I2]:((((((((~organization(X,T1)|~organization(Y,T2))|~reorganization_free(X,T1,T1))|~reorganization_free(Y,T2,T2))|~reproducibility(X,Rp1,T1))|~reproducibility(Y,Rp2,T2))|~inertia(X,I1,T1))|~inertia(Y,I2,T2))|((~greater(Rp2,Rp1)|greater(I2,I1))&(~greater(I2,I1)|greater(Rp2,Rp1)))))))))))),inference(fof_nnf,[status(thm)],[a3_FOL])).
% 0.56/0.88 fof(c15,plain,(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:((((((((~organization(X10,X12)|~organization(X11,X13))|~reorganization_free(X10,X12,X12))|~reorganization_free(X11,X13,X13))|~reproducibility(X10,X14,X12))|~reproducibility(X11,X15,X13))|~inertia(X10,X16,X12))|~inertia(X11,X17,X13))|((~greater(X15,X14)|greater(X17,X16))&(~greater(X17,X16)|greater(X15,X14)))))))))))),inference(variable_rename,[status(thm)],[c14])).
% 0.56/0.88 fof(c16,plain,(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(((((((((~organization(X10,X12)|~organization(X11,X13))|~reorganization_free(X10,X12,X12))|~reorganization_free(X11,X13,X13))|~reproducibility(X10,X14,X12))|~reproducibility(X11,X15,X13))|~inertia(X10,X16,X12))|~inertia(X11,X17,X13))|(~greater(X15,X14)|greater(X17,X16)))&((((((((~organization(X10,X12)|~organization(X11,X13))|~reorganization_free(X10,X12,X12))|~reorganization_free(X11,X13,X13))|~reproducibility(X10,X14,X12))|~reproducibility(X11,X15,X13))|~inertia(X10,X16,X12))|~inertia(X11,X17,X13))|(~greater(X17,X16)|greater(X15,X14)))))))))))),inference(distribute,[status(thm)],[c15])).
% 0.56/0.88 cnf(c18,plain,~organization(X63,X66)|~organization(X68,X61)|~reorganization_free(X63,X66,X66)|~reorganization_free(X68,X61,X61)|~reproducibility(X63,X65,X66)|~reproducibility(X68,X67,X61)|~inertia(X63,X64,X66)|~inertia(X68,X62,X61)|~greater(X62,X64)|greater(X67,X65),inference(split_conjunct,[status(thm)],[c16])).
% 0.56/0.88 cnf(c53,plain,~organization(X205,X207)|~organization(skolem0002,skolem0004)|~reorganization_free(X205,X207,X207)|~reorganization_free(skolem0002,skolem0004,skolem0004)|~reproducibility(X205,X204,X207)|~reproducibility(skolem0002,X208,skolem0004)|~inertia(X205,X206,X207)|~greater(skolem0006,X206)|greater(X208,X204),inference(resolution,[status(thm)],[c18, c9])).
% 0.56/0.88 cnf(c109,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~reorganization_free(skolem0001,skolem0003,skolem0003)|~reorganization_free(skolem0002,skolem0004,skolem0004)|~reproducibility(skolem0001,X313,skolem0003)|~reproducibility(skolem0002,X312,skolem0004)|~greater(skolem0006,skolem0005)|greater(X312,X313),inference(resolution,[status(thm)],[c53, c8])).
% 0.56/0.88 cnf(c130,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~reorganization_free(skolem0001,skolem0003,skolem0003)|~reorganization_free(skolem0002,skolem0004,skolem0004)|~reproducibility(skolem0001,X314,skolem0003)|~greater(skolem0006,skolem0005)|greater(skolem0009(skolem0002,skolem0004),X314),inference(resolution,[status(thm)],[c109, c43])).
% 0.56/0.88 cnf(c131,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~reorganization_free(skolem0001,skolem0003,skolem0003)|~reorganization_free(skolem0002,skolem0004,skolem0004)|~greater(skolem0006,skolem0005)|greater(skolem0009(skolem0002,skolem0004),skolem0009(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c130, c42])).
% 0.56/0.88 cnf(c132,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~reorganization_free(skolem0001,skolem0003,skolem0003)|~greater(skolem0006,skolem0005)|greater(skolem0009(skolem0002,skolem0004),skolem0009(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c131, c7])).
% 0.56/0.88 cnf(c133,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~greater(skolem0006,skolem0005)|greater(skolem0009(skolem0002,skolem0004),skolem0009(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c132, c6])).
% 0.56/0.88 cnf(c136,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|greater(skolem0009(skolem0002,skolem0004),skolem0009(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c133, c12])).
% 0.56/0.88 cnf(c137,plain,~organization(skolem0001,skolem0003)|greater(skolem0009(skolem0002,skolem0004),skolem0009(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c136, c5])).
% 0.56/0.88 cnf(c138,plain,greater(skolem0009(skolem0002,skolem0004),skolem0009(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c137, c4])).
% 0.56/0.88 cnf(c139,plain,~organization(X327,X323)|~organization(skolem0002,skolem0004)|~reliability(X327,X328,X323)|~reliability(skolem0002,X326,skolem0004)|~accountability(X327,X324,X323)|~accountability(skolem0002,X325,skolem0004)|~reproducibility(X327,skolem0009(skolem0001,skolem0003),X323)|greater(X326,X328),inference(resolution,[status(thm)],[c138, c60])).
% 0.56/0.88 cnf(c143,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~reliability(skolem0001,X330,skolem0003)|~reliability(skolem0002,X331,skolem0004)|~accountability(skolem0001,X332,skolem0003)|~accountability(skolem0002,X329,skolem0004)|greater(X331,X330),inference(resolution,[status(thm)],[c139, c42])).
% 0.56/0.88 cnf(c144,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~reliability(skolem0001,X334,skolem0003)|~reliability(skolem0002,X333,skolem0004)|~accountability(skolem0001,X335,skolem0003)|greater(X333,X334),inference(resolution,[status(thm)],[c143, c48])).
% 0.56/0.88 cnf(c145,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~reliability(skolem0001,X336,skolem0003)|~reliability(skolem0002,X337,skolem0004)|greater(X337,X336),inference(resolution,[status(thm)],[c144, c47])).
% 0.56/0.88 cnf(c146,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~reliability(skolem0001,X338,skolem0003)|greater(skolem0011(skolem0002,skolem0004),X338),inference(resolution,[status(thm)],[c145, c50])).
% 0.56/0.88 cnf(c147,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|greater(skolem0011(skolem0002,skolem0004),skolem0011(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c146, c49])).
% 0.56/0.88 cnf(c148,plain,~organization(skolem0001,skolem0003)|greater(skolem0011(skolem0002,skolem0004),skolem0011(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c147, c5])).
% 0.56/0.88 cnf(c149,plain,greater(skolem0011(skolem0002,skolem0004),skolem0011(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c148, c4])).
% 0.56/0.88 cnf(c23,plain,~organization(X103,X100)|~organization(X101,X105)|~reliability(X103,X109,X100)|~reliability(X101,X104,X105)|~accountability(X103,X106,X100)|~accountability(X101,X102,X105)|~reproducibility(X103,X108,X100)|~reproducibility(X101,X107,X105)|~greater(X107,X108)|greater(X102,X106),inference(split_conjunct,[status(thm)],[c21])).
% 0.56/0.88 cnf(c68,plain,~organization(X246,X247)|~organization(skolem0002,skolem0004)|~reliability(X246,X248,X247)|~reliability(skolem0002,X251,skolem0004)|~accountability(X246,X250,X247)|~accountability(skolem0002,X249,skolem0004)|~reproducibility(X246,X252,X247)|~greater(skolem0009(skolem0002,skolem0004),X252)|greater(X249,X250),inference(resolution,[status(thm)],[c23, c43])).
% 0.56/0.88 cnf(c140,plain,~organization(X345,X344)|~organization(skolem0002,skolem0004)|~reliability(X345,X348,X344)|~reliability(skolem0002,X346,skolem0004)|~accountability(X345,X347,X344)|~accountability(skolem0002,X343,skolem0004)|~reproducibility(X345,skolem0009(skolem0001,skolem0003),X344)|greater(X343,X347),inference(resolution,[status(thm)],[c138, c68])).
% 0.56/0.88 cnf(c150,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~reliability(skolem0001,X351,skolem0003)|~reliability(skolem0002,X352,skolem0004)|~accountability(skolem0001,X349,skolem0003)|~accountability(skolem0002,X350,skolem0004)|greater(X350,X349),inference(resolution,[status(thm)],[c140, c42])).
% 0.56/0.88 cnf(c151,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~reliability(skolem0001,X359,skolem0003)|~reliability(skolem0002,X357,skolem0004)|~accountability(skolem0001,X358,skolem0003)|greater(skolem0010(skolem0002,skolem0004),X358),inference(resolution,[status(thm)],[c150, c48])).
% 0.56/0.88 cnf(c153,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~reliability(skolem0001,X360,skolem0003)|~reliability(skolem0002,X361,skolem0004)|greater(skolem0010(skolem0002,skolem0004),skolem0010(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c151, c47])).
% 0.56/0.88 cnf(c154,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~reliability(skolem0001,X362,skolem0003)|greater(skolem0010(skolem0002,skolem0004),skolem0010(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c153, c50])).
% 0.56/0.88 cnf(c155,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|greater(skolem0010(skolem0002,skolem0004),skolem0010(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c154, c49])).
% 0.56/0.88 cnf(c156,plain,~organization(skolem0001,skolem0003)|greater(skolem0010(skolem0002,skolem0004),skolem0010(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c155, c5])).
% 0.56/0.88 cnf(c157,plain,greater(skolem0010(skolem0002,skolem0004),skolem0010(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c156, c4])).
% 0.56/0.88 cnf(c10,negated_conjecture,survival_chance(skolem0001,skolem0007,skolem0003),inference(split_conjunct,[status(thm)],[c3])).
% 0.56/0.88 cnf(c11,negated_conjecture,survival_chance(skolem0002,skolem0008,skolem0004),inference(split_conjunct,[status(thm)],[c3])).
% 0.56/0.88 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.56/0.88 fof(c25,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.56/0.88 fof(c26,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)],[c25])).
% 0.56/0.88 fof(c28,plain,(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:((((((((((~organization(X28,X36)|~organization(X29,X37))|~reliability(X28,X30,X36))|~reliability(X29,X31,X37))|~accountability(X28,X32,X36))|~accountability(X29,X33,X37))|~survival_chance(X28,X34,X36))|~survival_chance(X29,X35,X37))|~greater(X31,X30))|~greater(X33,X32))|greater(X35,X34)))))))))))),inference(shift_quantors,[status(thm)],[fof(c27,plain,(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:(![X35]:((((![X36]:(![X37]:(((((((~organization(X28,X36)|~organization(X29,X37))|~reliability(X28,X30,X36))|~reliability(X29,X31,X37))|~accountability(X28,X32,X36))|~accountability(X29,X33,X37))|~survival_chance(X28,X34,X36))|~survival_chance(X29,X35,X37))))|~greater(X31,X30))|~greater(X33,X32))|greater(X35,X34)))))))))),inference(variable_rename,[status(thm)],[c26])).])).
% 0.56/0.88 cnf(c29,plain,~organization(X135,X141)|~organization(X144,X136)|~reliability(X135,X137,X141)|~reliability(X144,X142,X136)|~accountability(X135,X143,X141)|~accountability(X144,X140,X136)|~survival_chance(X135,X139,X141)|~survival_chance(X144,X138,X136)|~greater(X142,X137)|~greater(X140,X143)|greater(X138,X139),inference(split_conjunct,[status(thm)],[c28])).
% 0.56/0.88 cnf(c84,plain,~organization(X282,X285)|~organization(skolem0002,skolem0004)|~reliability(X282,X279,X285)|~reliability(skolem0002,X281,skolem0004)|~accountability(X282,X280,X285)|~accountability(skolem0002,X284,skolem0004)|~survival_chance(X282,X283,X285)|~greater(X281,X279)|~greater(X284,X280)|greater(skolem0008,X283),inference(resolution,[status(thm)],[c29, c11])).
% 0.56/0.88 cnf(c118,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~reliability(skolem0001,X366,skolem0003)|~reliability(skolem0002,X365,skolem0004)|~accountability(skolem0001,X363,skolem0003)|~accountability(skolem0002,X364,skolem0004)|~greater(X365,X366)|~greater(X364,X363)|greater(skolem0008,skolem0007),inference(resolution,[status(thm)],[c84, c10])).
% 0.56/0.88 cnf(c158,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~reliability(skolem0001,X383,skolem0003)|~reliability(skolem0002,X382,skolem0004)|~accountability(skolem0001,X381,skolem0003)|~greater(X382,X383)|~greater(skolem0010(skolem0002,skolem0004),X381)|greater(skolem0008,skolem0007),inference(resolution,[status(thm)],[c118, c48])).
% 0.56/0.88 cnf(c164,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~reliability(skolem0001,X385,skolem0003)|~reliability(skolem0002,X384,skolem0004)|~accountability(skolem0001,skolem0010(skolem0001,skolem0003),skolem0003)|~greater(X384,X385)|greater(skolem0008,skolem0007),inference(resolution,[status(thm)],[c158, c157])).
% 0.56/0.88 cnf(c165,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~reliability(skolem0001,X386,skolem0003)|~reliability(skolem0002,X387,skolem0004)|~greater(X387,X386)|greater(skolem0008,skolem0007),inference(resolution,[status(thm)],[c164, c47])).
% 0.56/0.88 cnf(c166,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~reliability(skolem0001,X388,skolem0003)|~greater(skolem0011(skolem0002,skolem0004),X388)|greater(skolem0008,skolem0007),inference(resolution,[status(thm)],[c165, c50])).
% 0.56/0.88 cnf(c167,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|~reliability(skolem0001,skolem0011(skolem0001,skolem0003),skolem0003)|greater(skolem0008,skolem0007),inference(resolution,[status(thm)],[c166, c149])).
% 0.56/0.88 cnf(c168,plain,~organization(skolem0001,skolem0003)|~organization(skolem0002,skolem0004)|greater(skolem0008,skolem0007),inference(resolution,[status(thm)],[c167, c49])).
% 0.56/0.88 cnf(c169,plain,~organization(skolem0001,skolem0003)|greater(skolem0008,skolem0007),inference(resolution,[status(thm)],[c168, c5])).
% 0.56/0.88 cnf(c170,plain,greater(skolem0008,skolem0007),inference(resolution,[status(thm)],[c169, c4])).
% 0.56/0.88 cnf(c171,plain,$false,inference(resolution,[status(thm)],[c170, c13])).
% 0.56/0.88 % SZS output end CNFRefutation
% 0.56/0.88
% 0.56/0.88 % Initial clauses : 19
% 0.56/0.88 % Processed clauses : 128
% 0.56/0.88 % Factors computed : 23
% 0.56/0.88 % Resolvents computed: 107
% 0.56/0.88 % Tautologies deleted: 0
% 0.56/0.88 % Forward subsumed : 14
% 0.56/0.88 % Backward subsumed : 25
% 0.56/0.88 % -------- CPU Time ---------
% 0.56/0.88 % User time : 0.506 s
% 0.56/0.88 % System time : 0.022 s
% 0.56/0.88 % Total time : 0.528 s
%------------------------------------------------------------------------------