%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT005+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n031.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 6.36s 6.65s
% Output : CNFRefutation 6.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT005+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 : n031.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:39:41 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.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.41 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.41 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.24/0.48 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.24/0.48 """
% 0.24/0.48 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.24/0.48 """
% 0.33/0.57 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.57 """
% 6.36/6.65 % Version: 1.5
% 6.36/6.65 % SZS status Theorem
% 6.36/6.65 % SZS output start CNFRefutation
% 6.36/6.65 fof(t5_FOL,conjecture,(![X]:(![Y]:(![Re]:(![C]:(![P]:(![P1]:(![P2]:(![C1]:(![C2]:(![Ta]:(![Tb]:(![Tc]:((((((((((((((((((organization(X,Ta)&organization(Y,Ta))&organization(X,Tc))&organization(Y,Tc))&class(X,C,Ta))&class(Y,C,Ta))&survival_chance(X,P,Ta))&survival_chance(Y,P,Ta))&reorganization(X,Ta,Tb))&reorganization(Y,Ta,Tc))&reorganization_type(X,Re,Ta))&reorganization_type(Y,Re,Ta))&reorganization_free(X,Tb,Tc))&survival_chance(X,P1,Tc))&survival_chance(Y,P2,Tc))&complexity(X,C1,Ta))&complexity(Y,C2,Ta))&greater(C2,C1))=>greater(P1,P2)))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t5_FOL)).
% 6.36/6.65 fof(c8,negated_conjecture,(~(![X]:(![Y]:(![Re]:(![C]:(![P]:(![P1]:(![P2]:(![C1]:(![C2]:(![Ta]:(![Tb]:(![Tc]:((((((((((((((((((organization(X,Ta)&organization(Y,Ta))&organization(X,Tc))&organization(Y,Tc))&class(X,C,Ta))&class(Y,C,Ta))&survival_chance(X,P,Ta))&survival_chance(Y,P,Ta))&reorganization(X,Ta,Tb))&reorganization(Y,Ta,Tc))&reorganization_type(X,Re,Ta))&reorganization_type(Y,Re,Ta))&reorganization_free(X,Tb,Tc))&survival_chance(X,P1,Tc))&survival_chance(Y,P2,Tc))&complexity(X,C1,Ta))&complexity(Y,C2,Ta))&greater(C2,C1))=>greater(P1,P2))))))))))))))),inference(assume_negation,[status(cth)],[t5_FOL])).
% 6.36/6.65 fof(c9,negated_conjecture,(?[X]:(?[Y]:(?[Re]:(?[C]:(?[P]:(?[P1]:(?[P2]:(?[C1]:(?[C2]:(?[Ta]:(?[Tb]:(?[Tc]:((((((((((((((((((organization(X,Ta)&organization(Y,Ta))&organization(X,Tc))&organization(Y,Tc))&class(X,C,Ta))&class(Y,C,Ta))&survival_chance(X,P,Ta))&survival_chance(Y,P,Ta))&reorganization(X,Ta,Tb))&reorganization(Y,Ta,Tc))&reorganization_type(X,Re,Ta))&reorganization_type(Y,Re,Ta))&reorganization_free(X,Tb,Tc))&survival_chance(X,P1,Tc))&survival_chance(Y,P2,Tc))&complexity(X,C1,Ta))&complexity(Y,C2,Ta))&greater(C2,C1))&~greater(P1,P2)))))))))))))),inference(fof_nnf,[status(thm)],[c8])).
% 6.36/6.65 fof(c10,negated_conjecture,(?[X]:(?[Y]:(?[Re]:(?[C]:(?[P]:(?[P1]:(?[P2]:((?[C1]:(?[C2]:((?[Ta]:(((?[Tb]:(?[Tc]:((((((((((((((organization(X,Ta)&organization(Y,Ta))&organization(X,Tc))&organization(Y,Tc))&class(X,C,Ta))&class(Y,C,Ta))&survival_chance(X,P,Ta))&survival_chance(Y,P,Ta))&reorganization(X,Ta,Tb))&reorganization(Y,Ta,Tc))&reorganization_type(X,Re,Ta))&reorganization_type(Y,Re,Ta))&reorganization_free(X,Tb,Tc))&survival_chance(X,P1,Tc))&survival_chance(Y,P2,Tc))))&complexity(X,C1,Ta))&complexity(Y,C2,Ta)))&greater(C2,C1))))&~greater(P1,P2))))))))),inference(shift_quantors,[status(thm)],[c9])).
% 6.36/6.65 fof(c11,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:((?[X9]:(?[X10]:((?[X11]:(((?[X12]:(?[X13]:((((((((((((((organization(X2,X11)&organization(X3,X11))&organization(X2,X13))&organization(X3,X13))&class(X2,X5,X11))&class(X3,X5,X11))&survival_chance(X2,X6,X11))&survival_chance(X3,X6,X11))&reorganization(X2,X11,X12))&reorganization(X3,X11,X13))&reorganization_type(X2,X4,X11))&reorganization_type(X3,X4,X11))&reorganization_free(X2,X12,X13))&survival_chance(X2,X7,X13))&survival_chance(X3,X8,X13))))&complexity(X2,X9,X11))&complexity(X3,X10,X11)))&greater(X10,X9))))&~greater(X7,X8))))))))),inference(variable_rename,[status(thm)],[c10])).
% 6.36/6.65 fof(c12,negated_conjecture,((((((((((((((((((organization(skolem0001,skolem0010)&organization(skolem0002,skolem0010))&organization(skolem0001,skolem0012))&organization(skolem0002,skolem0012))&class(skolem0001,skolem0004,skolem0010))&class(skolem0002,skolem0004,skolem0010))&survival_chance(skolem0001,skolem0005,skolem0010))&survival_chance(skolem0002,skolem0005,skolem0010))&reorganization(skolem0001,skolem0010,skolem0011))&reorganization(skolem0002,skolem0010,skolem0012))&reorganization_type(skolem0001,skolem0003,skolem0010))&reorganization_type(skolem0002,skolem0003,skolem0010))&reorganization_free(skolem0001,skolem0011,skolem0012))&survival_chance(skolem0001,skolem0006,skolem0012))&survival_chance(skolem0002,skolem0007,skolem0012))&complexity(skolem0001,skolem0008,skolem0010))&complexity(skolem0002,skolem0009,skolem0010))&greater(skolem0009,skolem0008))&~greater(skolem0006,skolem0007)),inference(skolemize,[status(esa)],[c11])).
% 6.36/6.65 cnf(c31,negated_conjecture,~greater(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 cnf(c13,negated_conjecture,organization(skolem0001,skolem0010),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 cnf(c15,negated_conjecture,organization(skolem0001,skolem0012),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 cnf(c21,negated_conjecture,reorganization(skolem0001,skolem0010,skolem0011),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 fof(mp7,axiom,(![X]:(![Ta]:(![Tb]:(reorganization(X,Ta,Tb)=>greater(Tb,Ta))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp7)).
% 6.36/6.65 fof(c51,plain,(![X]:(![Ta]:(![Tb]:(~reorganization(X,Ta,Tb)|greater(Tb,Ta))))),inference(fof_nnf,[status(thm)],[mp7])).
% 6.36/6.65 fof(c52,plain,(![X47]:(![X48]:(![X49]:(~reorganization(X47,X48,X49)|greater(X49,X48))))),inference(variable_rename,[status(thm)],[c51])).
% 6.36/6.65 cnf(c53,plain,~reorganization(X95,X94,X96)|greater(X96,X94),inference(split_conjunct,[status(thm)],[c52])).
% 6.36/6.65 cnf(c87,plain,greater(skolem0011,skolem0010),inference(resolution,[status(thm)],[c53, c21])).
% 6.36/6.65 fof(mp13,axiom,(![X]:(![T]:(![T1]:(![T2]:((((organization(X,T1)&organization(X,T2))&greater(T,T1))&greater(T2,T))=>organization(X,T)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp13)).
% 6.36/6.65 fof(c54,plain,(![X]:(![T]:(![T1]:(![T2]:((((~organization(X,T1)|~organization(X,T2))|~greater(T,T1))|~greater(T2,T))|organization(X,T)))))),inference(fof_nnf,[status(thm)],[mp13])).
% 6.36/6.65 fof(c55,plain,(![X]:(![T]:((![T1]:(![T2]:(((~organization(X,T1)|~organization(X,T2))|~greater(T,T1))|~greater(T2,T))))|organization(X,T)))),inference(shift_quantors,[status(thm)],[c54])).
% 6.36/6.65 fof(c57,plain,(![X50]:(![X51]:(![X52]:(![X53]:((((~organization(X50,X52)|~organization(X50,X53))|~greater(X51,X52))|~greater(X53,X51))|organization(X50,X51)))))),inference(shift_quantors,[status(thm)],[fof(c56,plain,(![X50]:(![X51]:((![X52]:(![X53]:(((~organization(X50,X52)|~organization(X50,X53))|~greater(X51,X52))|~greater(X53,X51))))|organization(X50,X51)))),inference(variable_rename,[status(thm)],[c55])).])).
% 6.36/6.65 cnf(c58,plain,~organization(X181,X179)|~organization(X181,X180)|~greater(X178,X179)|~greater(X180,X178)|organization(X181,X178),inference(split_conjunct,[status(thm)],[c57])).
% 6.36/6.65 cnf(c14,negated_conjecture,organization(skolem0002,skolem0010),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 cnf(c16,negated_conjecture,organization(skolem0002,skolem0012),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 cnf(c30,negated_conjecture,greater(skolem0009,skolem0008),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 cnf(c17,negated_conjecture,class(skolem0001,skolem0004,skolem0010),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 cnf(c18,negated_conjecture,class(skolem0002,skolem0004,skolem0010),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 cnf(c22,negated_conjecture,reorganization(skolem0002,skolem0010,skolem0012),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 cnf(c23,negated_conjecture,reorganization_type(skolem0001,skolem0003,skolem0010),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 cnf(c24,negated_conjecture,reorganization_type(skolem0002,skolem0003,skolem0010),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 cnf(c28,negated_conjecture,complexity(skolem0001,skolem0008,skolem0010),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 cnf(c29,negated_conjecture,complexity(skolem0002,skolem0009,skolem0010),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 fof(a10_FOL,plain,(![X]:(![Y]:(![Re]:(![C]:(![C1]:(![C2]:(![Ta]:(![Tb]:(![Tc]:((((((((((((organization(X,Ta)&organization(Y,Ta))&organization(Y,Tc))&class(X,C,Ta))&class(Y,C,Ta))&reorganization(X,Ta,Tb))&reorganization(Y,Ta,Tc))&reorganization_type(X,Re,Ta))&reorganization_type(Y,Re,Ta))&complexity(X,C1,Ta))&complexity(Y,C2,Ta))&greater(C2,C1))=>greater(Tc,Tb))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a10_FOL)).
% 6.36/6.65 fof(c37,plain,(![X]:(![Y]:(![Re]:(![C]:(![C1]:(![C2]:(![Ta]:(![Tb]:(![Tc]:((((((((((((~organization(X,Ta)|~organization(Y,Ta))|~organization(Y,Tc))|~class(X,C,Ta))|~class(Y,C,Ta))|~reorganization(X,Ta,Tb))|~reorganization(Y,Ta,Tc))|~reorganization_type(X,Re,Ta))|~reorganization_type(Y,Re,Ta))|~complexity(X,C1,Ta))|~complexity(Y,C2,Ta))|~greater(C2,C1))|greater(Tc,Tb))))))))))),inference(fof_nnf,[status(thm)],[a10_FOL])).
% 6.36/6.65 fof(c38,plain,(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:((((((((((((~organization(X26,X32)|~organization(X27,X32))|~organization(X27,X34))|~class(X26,X29,X32))|~class(X27,X29,X32))|~reorganization(X26,X32,X33))|~reorganization(X27,X32,X34))|~reorganization_type(X26,X28,X32))|~reorganization_type(X27,X28,X32))|~complexity(X26,X30,X32))|~complexity(X27,X31,X32))|~greater(X31,X30))|greater(X34,X33))))))))))),inference(variable_rename,[status(thm)],[c37])).
% 6.36/6.65 cnf(c39,plain,~organization(X167,X170)|~organization(X169,X170)|~organization(X169,X173)|~class(X167,X174,X170)|~class(X169,X174,X170)|~reorganization(X167,X170,X166)|~reorganization(X169,X170,X173)|~reorganization_type(X167,X171,X170)|~reorganization_type(X169,X171,X170)|~complexity(X167,X172,X170)|~complexity(X169,X168,X170)|~greater(X168,X172)|greater(X173,X166),inference(split_conjunct,[status(thm)],[c38])).
% 6.36/6.65 cnf(c131,plain,~organization(X363,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0002,X360)|~class(X363,X361,skolem0010)|~class(skolem0002,X361,skolem0010)|~reorganization(X363,skolem0010,X364)|~reorganization(skolem0002,skolem0010,X360)|~reorganization_type(X363,X359,skolem0010)|~reorganization_type(skolem0002,X359,skolem0010)|~complexity(X363,X362,skolem0010)|~greater(skolem0009,X362)|greater(X360,X364),inference(resolution,[status(thm)],[c39, c29])).
% 6.36/6.65 cnf(c225,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0002,X498)|~class(skolem0001,X497,skolem0010)|~class(skolem0002,X497,skolem0010)|~reorganization(skolem0001,skolem0010,X496)|~reorganization(skolem0002,skolem0010,X498)|~reorganization_type(skolem0001,X499,skolem0010)|~reorganization_type(skolem0002,X499,skolem0010)|~greater(skolem0009,skolem0008)|greater(X498,X496),inference(resolution,[status(thm)],[c131, c28])).
% 6.36/6.65 cnf(c321,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0002,X662)|~class(skolem0001,X661,skolem0010)|~class(skolem0002,X661,skolem0010)|~reorganization(skolem0001,skolem0010,X660)|~reorganization(skolem0002,skolem0010,X662)|~reorganization_type(skolem0001,skolem0003,skolem0010)|~greater(skolem0009,skolem0008)|greater(X662,X660),inference(resolution,[status(thm)],[c225, c24])).
% 6.36/6.65 cnf(c479,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0002,X902)|~class(skolem0001,X903,skolem0010)|~class(skolem0002,X903,skolem0010)|~reorganization(skolem0001,skolem0010,X904)|~reorganization(skolem0002,skolem0010,X902)|~greater(skolem0009,skolem0008)|greater(X902,X904),inference(resolution,[status(thm)],[c321, c23])).
% 6.36/6.65 cnf(c757,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0002,skolem0012)|~class(skolem0001,X1240,skolem0010)|~class(skolem0002,X1240,skolem0010)|~reorganization(skolem0001,skolem0010,X1241)|~greater(skolem0009,skolem0008)|greater(skolem0012,X1241),inference(resolution,[status(thm)],[c479, c22])).
% 6.36/6.65 cnf(c1260,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0002,skolem0012)|~class(skolem0001,X1535,skolem0010)|~class(skolem0002,X1535,skolem0010)|~greater(skolem0009,skolem0008)|greater(skolem0012,skolem0011),inference(resolution,[status(thm)],[c757, c21])).
% 6.36/6.65 cnf(c1623,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0002,skolem0012)|~class(skolem0001,skolem0004,skolem0010)|~greater(skolem0009,skolem0008)|greater(skolem0012,skolem0011),inference(resolution,[status(thm)],[c1260, c18])).
% 6.36/6.65 cnf(c1624,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0002,skolem0012)|~greater(skolem0009,skolem0008)|greater(skolem0012,skolem0011),inference(resolution,[status(thm)],[c1623, c17])).
% 6.36/6.65 cnf(c1625,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0002,skolem0012)|greater(skolem0012,skolem0011),inference(resolution,[status(thm)],[c1624, c30])).
% 6.36/6.65 cnf(c1626,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|greater(skolem0012,skolem0011),inference(resolution,[status(thm)],[c1625, c16])).
% 6.36/6.65 cnf(c1627,plain,~organization(skolem0001,skolem0010)|greater(skolem0012,skolem0011),inference(resolution,[status(thm)],[c1626, c14])).
% 6.36/6.65 cnf(c1628,plain,greater(skolem0012,skolem0011),inference(resolution,[status(thm)],[c1627, c13])).
% 6.36/6.65 cnf(c1633,plain,~organization(X1545,X1544)|~organization(X1545,skolem0012)|~greater(skolem0011,X1544)|organization(X1545,skolem0011),inference(resolution,[status(thm)],[c1628, c58])).
% 6.36/6.65 cnf(c1638,plain,~organization(X1546,skolem0010)|~organization(X1546,skolem0012)|organization(X1546,skolem0011),inference(resolution,[status(thm)],[c1633, c87])).
% 6.36/6.65 cnf(c1641,plain,~organization(skolem0001,skolem0010)|organization(skolem0001,skolem0011),inference(resolution,[status(thm)],[c1638, c15])).
% 6.36/6.65 cnf(c1645,plain,organization(skolem0001,skolem0011),inference(resolution,[status(thm)],[c1641, c13])).
% 6.36/6.65 cnf(c25,negated_conjecture,reorganization_free(skolem0001,skolem0011,skolem0012),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 cnf(c26,negated_conjecture,survival_chance(skolem0001,skolem0006,skolem0012),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 fof(t3_FOL,plain,(![X]:(![P1]:(![P2]:(![T1]:(![T2]:((((((organization(X,T1)&organization(X,T2))&reorganization_free(X,T1,T2))&survival_chance(X,P1,T1))&survival_chance(X,P2,T2))&greater(T2,T1))=>greater(P2,P1))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t3_FOL)).
% 6.36/6.65 fof(c46,plain,(![X]:(![P1]:(![P2]:(![T1]:(![T2]:((((((~organization(X,T1)|~organization(X,T2))|~reorganization_free(X,T1,T2))|~survival_chance(X,P1,T1))|~survival_chance(X,P2,T2))|~greater(T2,T1))|greater(P2,P1))))))),inference(fof_nnf,[status(thm)],[t3_FOL])).
% 6.36/6.65 fof(c47,plain,(![X]:(![P1]:(![P2]:((![T1]:(![T2]:(((((~organization(X,T1)|~organization(X,T2))|~reorganization_free(X,T1,T2))|~survival_chance(X,P1,T1))|~survival_chance(X,P2,T2))|~greater(T2,T1))))|greater(P2,P1))))),inference(shift_quantors,[status(thm)],[c46])).
% 6.36/6.65 fof(c49,plain,(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:((((((~organization(X42,X45)|~organization(X42,X46))|~reorganization_free(X42,X45,X46))|~survival_chance(X42,X43,X45))|~survival_chance(X42,X44,X46))|~greater(X46,X45))|greater(X44,X43))))))),inference(shift_quantors,[status(thm)],[fof(c48,plain,(![X42]:(![X43]:(![X44]:((![X45]:(![X46]:(((((~organization(X42,X45)|~organization(X42,X46))|~reorganization_free(X42,X45,X46))|~survival_chance(X42,X43,X45))|~survival_chance(X42,X44,X46))|~greater(X46,X45))))|greater(X44,X43))))),inference(variable_rename,[status(thm)],[c47])).])).
% 6.36/6.65 cnf(c50,plain,~organization(X202,X203)|~organization(X202,X204)|~reorganization_free(X202,X203,X204)|~survival_chance(X202,X201,X203)|~survival_chance(X202,X200,X204)|~greater(X204,X203)|greater(X200,X201),inference(split_conjunct,[status(thm)],[c49])).
% 6.36/6.65 cnf(c156,plain,~organization(skolem0001,X365)|~organization(skolem0001,skolem0012)|~reorganization_free(skolem0001,X365,skolem0012)|~survival_chance(skolem0001,X366,X365)|~greater(skolem0012,X365)|greater(skolem0006,X366),inference(resolution,[status(thm)],[c50, c26])).
% 6.36/6.65 fof(mp12,axiom,(![X]:(![T]:(organization(X,T)=>(?[P]:survival_chance(X,P,T))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp12)).
% 6.36/6.65 fof(c59,plain,(![X]:(![T]:(~organization(X,T)|(?[P]:survival_chance(X,P,T))))),inference(fof_nnf,[status(thm)],[mp12])).
% 6.36/6.65 fof(c60,plain,(![X54]:(![X55]:(~organization(X54,X55)|(?[X56]:survival_chance(X54,X56,X55))))),inference(variable_rename,[status(thm)],[c59])).
% 6.36/6.65 fof(c61,plain,(![X54]:(![X55]:(~organization(X54,X55)|survival_chance(X54,skolem0013(X54,X55),X55)))),inference(skolemize,[status(esa)],[c60])).
% 6.36/6.65 cnf(c62,plain,~organization(X103,X104)|survival_chance(X103,skolem0013(X103,X104),X104),inference(split_conjunct,[status(thm)],[c61])).
% 6.36/6.65 cnf(c1647,plain,survival_chance(skolem0001,skolem0013(skolem0001,skolem0011),skolem0011),inference(resolution,[status(thm)],[c1645, c62])).
% 6.36/6.65 cnf(c1676,plain,~organization(skolem0001,skolem0011)|~organization(skolem0001,skolem0012)|~reorganization_free(skolem0001,skolem0011,skolem0012)|~greater(skolem0012,skolem0011)|greater(skolem0006,skolem0013(skolem0001,skolem0011)),inference(resolution,[status(thm)],[c1647, c156])).
% 6.36/6.65 cnf(c1706,plain,~organization(skolem0001,skolem0011)|~organization(skolem0001,skolem0012)|~greater(skolem0012,skolem0011)|greater(skolem0006,skolem0013(skolem0001,skolem0011)),inference(resolution,[status(thm)],[c1676, c25])).
% 6.36/6.65 cnf(c1707,plain,~organization(skolem0001,skolem0011)|~organization(skolem0001,skolem0012)|greater(skolem0006,skolem0013(skolem0001,skolem0011)),inference(resolution,[status(thm)],[c1706, c1628])).
% 6.36/6.65 cnf(c1708,plain,~organization(skolem0001,skolem0011)|greater(skolem0006,skolem0013(skolem0001,skolem0011)),inference(resolution,[status(thm)],[c1707, c15])).
% 6.36/6.65 cnf(c1709,plain,greater(skolem0006,skolem0013(skolem0001,skolem0011)),inference(resolution,[status(thm)],[c1708, c1645])).
% 6.36/6.65 fof(mp11,axiom,(![X]:(![Y]:(![Z]:((greater(X,Y)&greater(Y,Z))=>greater(X,Z))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp11)).
% 6.36/6.65 fof(c63,plain,(![X]:(![Y]:(![Z]:((~greater(X,Y)|~greater(Y,Z))|greater(X,Z))))),inference(fof_nnf,[status(thm)],[mp11])).
% 6.36/6.65 fof(c64,plain,(![X57]:(![X58]:(![X59]:((~greater(X57,X58)|~greater(X58,X59))|greater(X57,X59))))),inference(variable_rename,[status(thm)],[c63])).
% 6.36/6.65 cnf(c65,plain,~greater(X107,X106)|~greater(X106,X105)|greater(X107,X105),inference(split_conjunct,[status(thm)],[c64])).
% 6.36/6.65 fof(mp6_2,axiom,(![X]:(![Y]:(~(greater(X,Y)&greater(Y,X))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp6_2)).
% 6.36/6.65 fof(c66,plain,(![X]:(![Y]:(~greater(X,Y)|~greater(Y,X)))),inference(fof_nnf,[status(thm)],[mp6_2])).
% 6.36/6.65 fof(c67,plain,(![X60]:(![X61]:(~greater(X60,X61)|~greater(X61,X60)))),inference(variable_rename,[status(thm)],[c66])).
% 6.36/6.65 cnf(c68,plain,~greater(X79,X80)|~greater(X80,X79),inference(split_conjunct,[status(thm)],[c67])).
% 6.36/6.65 cnf(c80,plain,~greater(X81,X81),inference(factor,[status(thm)],[c68])).
% 6.36/6.65 cnf(c90,plain,~greater(skolem0010,skolem0011),inference(resolution,[status(thm)],[c87, c68])).
% 6.36/6.65 cnf(c1640,plain,~organization(skolem0002,skolem0010)|organization(skolem0002,skolem0011),inference(resolution,[status(thm)],[c1638, c16])).
% 6.36/6.65 cnf(c1642,plain,organization(skolem0002,skolem0011),inference(resolution,[status(thm)],[c1640, c14])).
% 6.36/6.65 cnf(c27,negated_conjecture,survival_chance(skolem0002,skolem0007,skolem0012),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 fof(t4_FOL,plain,(![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)).
% 6.36/6.65 fof(c40,plain,(![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)],[t4_FOL])).
% 6.36/6.65 fof(c41,plain,(![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)],[c40])).
% 6.36/6.65 fof(c42,plain,(![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)],[c41])).
% 6.36/6.65 fof(c44,plain,(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:(![X41]:((((((((~organization(X35,X38)|~organization(X35,X39))|~reorganization(X35,X40,X41))|~survival_chance(X35,X36,X38))|~survival_chance(X35,X37,X39))|greater(X40,X38))|~greater(X39,X38))|greater(X39,X41))|greater(X36,X37))))))))),inference(shift_quantors,[status(thm)],[fof(c43,plain,(![X35]:(![X36]:(![X37]:((![X38]:(![X39]:(![X40]:(![X41]:(((((((~organization(X35,X38)|~organization(X35,X39))|~reorganization(X35,X40,X41))|~survival_chance(X35,X36,X38))|~survival_chance(X35,X37,X39))|greater(X40,X38))|~greater(X39,X38))|greater(X39,X41))))))|greater(X36,X37))))),inference(variable_rename,[status(thm)],[c42])).])).
% 6.36/6.65 cnf(c45,plain,~organization(X187,X188)|~organization(X187,X184)|~reorganization(X187,X182,X186)|~survival_chance(X187,X185,X188)|~survival_chance(X187,X183,X184)|greater(X182,X188)|~greater(X184,X188)|greater(X184,X186)|greater(X185,X183),inference(split_conjunct,[status(thm)],[c44])).
% 6.36/6.65 cnf(c142,plain,~organization(skolem0002,X388)|~organization(skolem0002,skolem0012)|~reorganization(skolem0002,X390,X389)|~survival_chance(skolem0002,X387,X388)|greater(X390,X388)|~greater(skolem0012,X388)|greater(skolem0012,X389)|greater(X387,skolem0007),inference(resolution,[status(thm)],[c45, c27])).
% 6.36/6.65 cnf(c1644,plain,survival_chance(skolem0002,skolem0013(skolem0002,skolem0011),skolem0011),inference(resolution,[status(thm)],[c1642, c62])).
% 6.36/6.65 cnf(c1667,plain,~organization(skolem0002,skolem0011)|~organization(skolem0002,skolem0012)|~reorganization(skolem0002,X1787,X1788)|greater(X1787,skolem0011)|~greater(skolem0012,skolem0011)|greater(skolem0012,X1788)|greater(skolem0013(skolem0002,skolem0011),skolem0007),inference(resolution,[status(thm)],[c1644, c142])).
% 6.36/6.65 cnf(c1926,plain,~organization(skolem0002,skolem0011)|~organization(skolem0002,skolem0012)|greater(skolem0010,skolem0011)|~greater(skolem0012,skolem0011)|greater(skolem0012,skolem0012)|greater(skolem0013(skolem0002,skolem0011),skolem0007),inference(resolution,[status(thm)],[c1667, c22])).
% 6.36/6.65 cnf(c1928,plain,~organization(skolem0002,skolem0011)|~organization(skolem0002,skolem0012)|greater(skolem0010,skolem0011)|greater(skolem0012,skolem0012)|greater(skolem0013(skolem0002,skolem0011),skolem0007),inference(resolution,[status(thm)],[c1926, c1628])).
% 6.36/6.65 cnf(c1929,plain,~organization(skolem0002,skolem0011)|greater(skolem0010,skolem0011)|greater(skolem0012,skolem0012)|greater(skolem0013(skolem0002,skolem0011),skolem0007),inference(resolution,[status(thm)],[c1928, c16])).
% 6.36/6.65 cnf(c1930,plain,greater(skolem0010,skolem0011)|greater(skolem0012,skolem0012)|greater(skolem0013(skolem0002,skolem0011),skolem0007),inference(resolution,[status(thm)],[c1929, c1642])).
% 6.36/6.65 cnf(c1933,plain,greater(skolem0012,skolem0012)|greater(skolem0013(skolem0002,skolem0011),skolem0007),inference(resolution,[status(thm)],[c1930, c90])).
% 6.36/6.65 cnf(c1956,plain,greater(skolem0013(skolem0002,skolem0011),skolem0007),inference(resolution,[status(thm)],[c1933, c80])).
% 6.36/6.65 cnf(c1964,plain,~greater(X1789,skolem0013(skolem0002,skolem0011))|greater(X1789,skolem0007),inference(resolution,[status(thm)],[c1956, c65])).
% 6.36/6.65 cnf(reflexivity,axiom,X64=X64,theory(equality)).
% 6.36/6.65 cnf(c0,axiom,X73!=X72|X71!=X74|~greater(X73,X71)|greater(X72,X74),theory(equality)).
% 6.36/6.65 cnf(c1713,plain,skolem0006!=X1578|skolem0013(skolem0001,skolem0011)!=X1579|greater(X1578,X1579),inference(resolution,[status(thm)],[c1709, c0])).
% 6.36/6.65 cnf(c19,negated_conjecture,survival_chance(skolem0001,skolem0005,skolem0010),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 cnf(c20,negated_conjecture,survival_chance(skolem0002,skolem0005,skolem0010),inference(split_conjunct,[status(thm)],[c12])).
% 6.36/6.65 fof(a11_FOL,plain,(![X]:(![Y]:(![Re]:(![C]:(![P]:(![P1]:(![P2]:(![C1]:(![C2]:(![Ta]:(![Tb]:(![Tc]:(((((((((((((((((organization(X,Ta)&organization(Y,Ta))&organization(X,Tb))&organization(Y,Tb))&class(X,C,Ta))&class(Y,C,Ta))&survival_chance(X,P,Ta))&survival_chance(Y,P,Ta))&reorganization(X,Ta,Tb))&reorganization(Y,Ta,Tc))&reorganization_type(X,Re,Ta))&reorganization_type(Y,Re,Ta))&survival_chance(X,P1,Tb))&survival_chance(Y,P2,Tb))&complexity(X,C1,Ta))&complexity(Y,C2,Ta))&greater(C2,C1))=>(greater(P1,P2)|P1=P2)))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a11_FOL)).
% 6.36/6.65 fof(c32,plain,(![X]:(![Y]:(![Re]:(![C]:(![P]:(![P1]:(![P2]:(![C1]:(![C2]:(![Ta]:(![Tb]:(![Tc]:(((((((((((((((((~organization(X,Ta)|~organization(Y,Ta))|~organization(X,Tb))|~organization(Y,Tb))|~class(X,C,Ta))|~class(Y,C,Ta))|~survival_chance(X,P,Ta))|~survival_chance(Y,P,Ta))|~reorganization(X,Ta,Tb))|~reorganization(Y,Ta,Tc))|~reorganization_type(X,Re,Ta))|~reorganization_type(Y,Re,Ta))|~survival_chance(X,P1,Tb))|~survival_chance(Y,P2,Tb))|~complexity(X,C1,Ta))|~complexity(Y,C2,Ta))|~greater(C2,C1))|(greater(P1,P2)|P1=P2)))))))))))))),inference(fof_nnf,[status(thm)],[a11_FOL])).
% 6.36/6.65 fof(c33,plain,(![X]:(![Y]:(![Re]:(![C]:(![P]:(![P1]:(![P2]:((![C1]:(![C2]:((![Ta]:(((![Tb]:(((((((((((((~organization(X,Ta)|~organization(Y,Ta))|~organization(X,Tb))|~organization(Y,Tb))|~class(X,C,Ta))|~class(Y,C,Ta))|~survival_chance(X,P,Ta))|~survival_chance(Y,P,Ta))|~reorganization(X,Ta,Tb))|(![Tc]:~reorganization(Y,Ta,Tc)))|~reorganization_type(X,Re,Ta))|~reorganization_type(Y,Re,Ta))|~survival_chance(X,P1,Tb))|~survival_chance(Y,P2,Tb)))|~complexity(X,C1,Ta))|~complexity(Y,C2,Ta)))|~greater(C2,C1))))|(greater(P1,P2)|P1=P2))))))))),inference(shift_quantors,[status(thm)],[c32])).
% 6.36/6.65 fof(c35,plain,(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(((((((((((((((((~organization(X14,X23)|~organization(X15,X23))|~organization(X14,X24))|~organization(X15,X24))|~class(X14,X17,X23))|~class(X15,X17,X23))|~survival_chance(X14,X18,X23))|~survival_chance(X15,X18,X23))|~reorganization(X14,X23,X24))|~reorganization(X15,X23,X25))|~reorganization_type(X14,X16,X23))|~reorganization_type(X15,X16,X23))|~survival_chance(X14,X19,X24))|~survival_chance(X15,X20,X24))|~complexity(X14,X21,X23))|~complexity(X15,X22,X23))|~greater(X22,X21))|(greater(X19,X20)|X19=X20)))))))))))))),inference(shift_quantors,[status(thm)],[fof(c34,plain,(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:((![X21]:(![X22]:((![X23]:(((![X24]:(((((((((((((~organization(X14,X23)|~organization(X15,X23))|~organization(X14,X24))|~organization(X15,X24))|~class(X14,X17,X23))|~class(X15,X17,X23))|~survival_chance(X14,X18,X23))|~survival_chance(X15,X18,X23))|~reorganization(X14,X23,X24))|(![X25]:~reorganization(X15,X23,X25)))|~reorganization_type(X14,X16,X23))|~reorganization_type(X15,X16,X23))|~survival_chance(X14,X19,X24))|~survival_chance(X15,X20,X24)))|~complexity(X14,X21,X23))|~complexity(X15,X22,X23)))|~greater(X22,X21))))|(greater(X19,X20)|X19=X20))))))))),inference(variable_rename,[status(thm)],[c33])).])).
% 6.36/6.65 cnf(c36,plain,~organization(X152,X159)|~organization(X158,X159)|~organization(X152,X155)|~organization(X158,X155)|~class(X152,X153,X159)|~class(X158,X153,X159)|~survival_chance(X152,X150,X159)|~survival_chance(X158,X150,X159)|~reorganization(X152,X159,X155)|~reorganization(X158,X159,X157)|~reorganization_type(X152,X149,X159)|~reorganization_type(X158,X149,X159)|~survival_chance(X152,X156,X155)|~survival_chance(X158,X151,X155)|~complexity(X152,X148,X159)|~complexity(X158,X154,X159)|~greater(X154,X148)|greater(X156,X151)|X156=X151,inference(split_conjunct,[status(thm)],[c35])).
% 6.36/6.65 cnf(c124,plain,~organization(X324,skolem0010)|~organization(skolem0002,skolem0010)|~organization(X324,X323)|~organization(skolem0002,X323)|~class(X324,X325,skolem0010)|~class(skolem0002,X325,skolem0010)|~survival_chance(X324,X327,skolem0010)|~survival_chance(skolem0002,X327,skolem0010)|~reorganization(X324,skolem0010,X323)|~reorganization(skolem0002,skolem0010,X321)|~reorganization_type(X324,X322,skolem0010)|~reorganization_type(skolem0002,X322,skolem0010)|~survival_chance(X324,X328,X323)|~survival_chance(skolem0002,X320,X323)|~complexity(X324,X326,skolem0010)|~greater(skolem0009,X326)|greater(X328,X320)|X328=X320,inference(resolution,[status(thm)],[c36, c29])).
% 6.36/6.65 cnf(c207,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0001,X452)|~organization(skolem0002,X452)|~class(skolem0001,X453,skolem0010)|~class(skolem0002,X453,skolem0010)|~survival_chance(skolem0001,X455,skolem0010)|~survival_chance(skolem0002,X455,skolem0010)|~reorganization(skolem0001,skolem0010,X452)|~reorganization(skolem0002,skolem0010,X457)|~reorganization_type(skolem0001,X458,skolem0010)|~reorganization_type(skolem0002,X458,skolem0010)|~survival_chance(skolem0001,X454,X452)|~survival_chance(skolem0002,X456,X452)|~greater(skolem0009,skolem0008)|greater(X454,X456)|X454=X456,inference(resolution,[status(thm)],[c124, c28])).
% 6.36/6.65 cnf(c1655,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0001,skolem0011)|~organization(skolem0002,skolem0011)|~class(skolem0001,X2458,skolem0010)|~class(skolem0002,X2458,skolem0010)|~survival_chance(skolem0001,X2454,skolem0010)|~survival_chance(skolem0002,X2454,skolem0010)|~reorganization(skolem0001,skolem0010,skolem0011)|~reorganization(skolem0002,skolem0010,X2456)|~reorganization_type(skolem0001,X2455,skolem0010)|~reorganization_type(skolem0002,X2455,skolem0010)|~survival_chance(skolem0001,X2457,skolem0011)|~greater(skolem0009,skolem0008)|greater(X2457,skolem0013(skolem0002,skolem0011))|X2457=skolem0013(skolem0002,skolem0011),inference(resolution,[status(thm)],[c1644, c207])).
% 6.36/6.65 cnf(c2434,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0001,skolem0011)|~organization(skolem0002,skolem0011)|~class(skolem0001,X2515,skolem0010)|~class(skolem0002,X2515,skolem0010)|~survival_chance(skolem0001,X2517,skolem0010)|~survival_chance(skolem0002,X2517,skolem0010)|~reorganization(skolem0001,skolem0010,skolem0011)|~reorganization(skolem0002,skolem0010,X2516)|~reorganization_type(skolem0001,X2518,skolem0010)|~reorganization_type(skolem0002,X2518,skolem0010)|~greater(skolem0009,skolem0008)|greater(skolem0013(skolem0001,skolem0011),skolem0013(skolem0002,skolem0011))|skolem0013(skolem0001,skolem0011)=skolem0013(skolem0002,skolem0011),inference(resolution,[status(thm)],[c1655, c1647])).
% 6.36/6.65 cnf(c2588,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0001,skolem0011)|~organization(skolem0002,skolem0011)|~class(skolem0001,X2658,skolem0010)|~class(skolem0002,X2658,skolem0010)|~survival_chance(skolem0001,X2659,skolem0010)|~survival_chance(skolem0002,X2659,skolem0010)|~reorganization(skolem0001,skolem0010,skolem0011)|~reorganization(skolem0002,skolem0010,X2657)|~reorganization_type(skolem0001,skolem0003,skolem0010)|~greater(skolem0009,skolem0008)|greater(skolem0013(skolem0001,skolem0011),skolem0013(skolem0002,skolem0011))|skolem0013(skolem0001,skolem0011)=skolem0013(skolem0002,skolem0011),inference(resolution,[status(thm)],[c2434, c24])).
% 6.36/6.65 cnf(c2668,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0001,skolem0011)|~organization(skolem0002,skolem0011)|~class(skolem0001,X2802,skolem0010)|~class(skolem0002,X2802,skolem0010)|~survival_chance(skolem0001,X2804,skolem0010)|~survival_chance(skolem0002,X2804,skolem0010)|~reorganization(skolem0001,skolem0010,skolem0011)|~reorganization(skolem0002,skolem0010,X2803)|~greater(skolem0009,skolem0008)|greater(skolem0013(skolem0001,skolem0011),skolem0013(skolem0002,skolem0011))|skolem0013(skolem0001,skolem0011)=skolem0013(skolem0002,skolem0011),inference(resolution,[status(thm)],[c2588, c23])).
% 6.36/6.65 cnf(c2753,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0001,skolem0011)|~organization(skolem0002,skolem0011)|~class(skolem0001,X2811,skolem0010)|~class(skolem0002,X2811,skolem0010)|~survival_chance(skolem0001,X2810,skolem0010)|~survival_chance(skolem0002,X2810,skolem0010)|~reorganization(skolem0001,skolem0010,skolem0011)|~greater(skolem0009,skolem0008)|greater(skolem0013(skolem0001,skolem0011),skolem0013(skolem0002,skolem0011))|skolem0013(skolem0001,skolem0011)=skolem0013(skolem0002,skolem0011),inference(resolution,[status(thm)],[c2668, c22])).
% 6.36/6.65 cnf(c2878,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0001,skolem0011)|~organization(skolem0002,skolem0011)|~class(skolem0001,X2948,skolem0010)|~class(skolem0002,X2948,skolem0010)|~survival_chance(skolem0001,X2949,skolem0010)|~survival_chance(skolem0002,X2949,skolem0010)|~greater(skolem0009,skolem0008)|greater(skolem0013(skolem0001,skolem0011),skolem0013(skolem0002,skolem0011))|skolem0013(skolem0001,skolem0011)=skolem0013(skolem0002,skolem0011),inference(resolution,[status(thm)],[c2753, c21])).
% 6.36/6.65 cnf(c2906,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0001,skolem0011)|~organization(skolem0002,skolem0011)|~class(skolem0001,X2950,skolem0010)|~class(skolem0002,X2950,skolem0010)|~survival_chance(skolem0001,skolem0005,skolem0010)|~greater(skolem0009,skolem0008)|greater(skolem0013(skolem0001,skolem0011),skolem0013(skolem0002,skolem0011))|skolem0013(skolem0001,skolem0011)=skolem0013(skolem0002,skolem0011),inference(resolution,[status(thm)],[c2878, c20])).
% 6.36/6.65 cnf(c2907,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0001,skolem0011)|~organization(skolem0002,skolem0011)|~class(skolem0001,X2952,skolem0010)|~class(skolem0002,X2952,skolem0010)|~greater(skolem0009,skolem0008)|greater(skolem0013(skolem0001,skolem0011),skolem0013(skolem0002,skolem0011))|skolem0013(skolem0001,skolem0011)=skolem0013(skolem0002,skolem0011),inference(resolution,[status(thm)],[c2906, c19])).
% 6.36/6.65 cnf(c2909,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0001,skolem0011)|~organization(skolem0002,skolem0011)|~class(skolem0001,skolem0004,skolem0010)|~greater(skolem0009,skolem0008)|greater(skolem0013(skolem0001,skolem0011),skolem0013(skolem0002,skolem0011))|skolem0013(skolem0001,skolem0011)=skolem0013(skolem0002,skolem0011),inference(resolution,[status(thm)],[c2907, c18])).
% 6.36/6.65 cnf(c2910,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0001,skolem0011)|~organization(skolem0002,skolem0011)|~greater(skolem0009,skolem0008)|greater(skolem0013(skolem0001,skolem0011),skolem0013(skolem0002,skolem0011))|skolem0013(skolem0001,skolem0011)=skolem0013(skolem0002,skolem0011),inference(resolution,[status(thm)],[c2909, c17])).
% 6.36/6.65 cnf(c2911,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0001,skolem0011)|~organization(skolem0002,skolem0011)|greater(skolem0013(skolem0001,skolem0011),skolem0013(skolem0002,skolem0011))|skolem0013(skolem0001,skolem0011)=skolem0013(skolem0002,skolem0011),inference(resolution,[status(thm)],[c2910, c30])).
% 6.36/6.65 cnf(c2912,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|~organization(skolem0001,skolem0011)|greater(skolem0013(skolem0001,skolem0011),skolem0013(skolem0002,skolem0011))|skolem0013(skolem0001,skolem0011)=skolem0013(skolem0002,skolem0011),inference(resolution,[status(thm)],[c2911, c1642])).
% 6.36/6.65 cnf(c2913,plain,~organization(skolem0001,skolem0010)|~organization(skolem0002,skolem0010)|greater(skolem0013(skolem0001,skolem0011),skolem0013(skolem0002,skolem0011))|skolem0013(skolem0001,skolem0011)=skolem0013(skolem0002,skolem0011),inference(resolution,[status(thm)],[c2912, c1645])).
% 6.36/6.65 cnf(c2914,plain,~organization(skolem0001,skolem0010)|greater(skolem0013(skolem0001,skolem0011),skolem0013(skolem0002,skolem0011))|skolem0013(skolem0001,skolem0011)=skolem0013(skolem0002,skolem0011),inference(resolution,[status(thm)],[c2913, c14])).
% 6.36/6.65 cnf(c2915,plain,greater(skolem0013(skolem0001,skolem0011),skolem0013(skolem0002,skolem0011))|skolem0013(skolem0001,skolem0011)=skolem0013(skolem0002,skolem0011),inference(resolution,[status(thm)],[c2914, c13])).
% 6.36/6.65 cnf(c2916,plain,skolem0013(skolem0001,skolem0011)=skolem0013(skolem0002,skolem0011)|greater(skolem0013(skolem0001,skolem0011),skolem0007),inference(resolution,[status(thm)],[c2915, c1964])).
% 6.36/6.65 cnf(c2940,plain,greater(skolem0013(skolem0001,skolem0011),skolem0007)|skolem0006!=X2955|greater(X2955,skolem0013(skolem0002,skolem0011)),inference(resolution,[status(thm)],[c2916, c1713])).
% 6.36/6.65 cnf(c2966,plain,greater(skolem0013(skolem0001,skolem0011),skolem0007)|greater(skolem0006,skolem0013(skolem0002,skolem0011)),inference(resolution,[status(thm)],[c2940, reflexivity])).
% 6.36/6.65 cnf(c2975,plain,greater(skolem0013(skolem0001,skolem0011),skolem0007)|greater(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2966, c1964])).
% 6.36/6.65 cnf(c2994,plain,greater(skolem0013(skolem0001,skolem0011),skolem0007),inference(resolution,[status(thm)],[c2975, c31])).
% 6.36/6.65 cnf(c2999,plain,~greater(X2957,skolem0013(skolem0001,skolem0011))|greater(X2957,skolem0007),inference(resolution,[status(thm)],[c2994, c65])).
% 6.36/6.65 cnf(c3006,plain,greater(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2999, c1709])).
% 6.36/6.65 cnf(c3012,plain,$false,inference(resolution,[status(thm)],[c3006, c31])).
% 6.36/6.65 % SZS output end CNFRefutation
% 6.36/6.65
% 6.36/6.65 % Initial clauses : 40
% 6.36/6.65 % Processed clauses : 1131
% 6.36/6.65 % Factors computed : 29
% 6.36/6.65 % Resolvents computed: 2913
% 6.36/6.65 % Tautologies deleted: 142
% 6.36/6.65 % Forward subsumed : 1623
% 6.36/6.65 % Backward subsumed : 827
% 6.36/6.65 % -------- CPU Time ---------
% 6.36/6.65 % User time : 6.273 s
% 6.36/6.65 % System time : 0.027 s
% 6.36/6.65 % Total time : 6.300 s
%------------------------------------------------------------------------------