%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT057+1 : TPTP v9.3.0. Released v2.4.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:48 AM UTC 2026
% Result : Theorem 27.89s 28.15s
% Output : CNFRefutation 27.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT057+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.34 % Computer : n031.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 13:32:56 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.38 (re.compile("\."), Token.FullStop),
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.38 (re.compile("\("), Token.OpenPar),
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.38 (re.compile("\)"), Token.ClosePar),
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.38 (re.compile("\["), Token.OpenSquare),
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.38 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.38 (re.compile("~\|"), Token.Nor),
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.38 (re.compile("\|"), Token.Or),
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.38 (re.compile("\?"), Token.Existential),
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.38 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.38 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.12/0.41 """
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.12/0.41 """
% 0.12/0.45 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.12/0.45 """
% 27.89/28.15 % Version: 1.5
% 27.89/28.15 % SZS status Theorem
% 27.89/28.15 % SZS output start CNFRefutation
% 27.89/28.15 fof(theorem_6,conjecture,(![X]:(![T0]:(![T1]:(![T2]:((((((organization(X)&has_endowment(X))&age(X,T0)=zero)&smaller_or_equal(age(X,T1),eta))&greater(age(X,T2),eta))&greater(eta,zero))=>(greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1))&hazard_of_mortality(X,T1)=hazard_of_mortality(X,T0))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', theorem_6)).
% 27.89/28.15 fof(c9,negated_conjecture,(~(![X]:(![T0]:(![T1]:(![T2]:((((((organization(X)&has_endowment(X))&age(X,T0)=zero)&smaller_or_equal(age(X,T1),eta))&greater(age(X,T2),eta))&greater(eta,zero))=>(greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1))&hazard_of_mortality(X,T1)=hazard_of_mortality(X,T0)))))))),inference(assume_negation,[status(cth)],[theorem_6])).
% 27.89/28.15 fof(c10,negated_conjecture,(?[X]:(?[T0]:(?[T1]:(?[T2]:((((((organization(X)&has_endowment(X))&age(X,T0)=zero)&smaller_or_equal(age(X,T1),eta))&greater(age(X,T2),eta))&greater(eta,zero))&(~greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1))|hazard_of_mortality(X,T1)!=hazard_of_mortality(X,T0))))))),inference(fof_nnf,[status(thm)],[c9])).
% 27.89/28.15 fof(c11,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:((((((organization(X2)&has_endowment(X2))&age(X2,X3)=zero)&smaller_or_equal(age(X2,X4),eta))&greater(age(X2,X5),eta))&greater(eta,zero))&(~greater(hazard_of_mortality(X2,X5),hazard_of_mortality(X2,X4))|hazard_of_mortality(X2,X4)!=hazard_of_mortality(X2,X3))))))),inference(variable_rename,[status(thm)],[c10])).
% 27.89/28.15 fof(c12,negated_conjecture,((((((organization(skolem0001)&has_endowment(skolem0001))&age(skolem0001,skolem0002)=zero)&smaller_or_equal(age(skolem0001,skolem0003),eta))&greater(age(skolem0001,skolem0004),eta))&greater(eta,zero))&(~greater(hazard_of_mortality(skolem0001,skolem0004),hazard_of_mortality(skolem0001,skolem0003))|hazard_of_mortality(skolem0001,skolem0003)!=hazard_of_mortality(skolem0001,skolem0002))),inference(skolemize,[status(esa)],[c11])).
% 27.89/28.15 cnf(c14,negated_conjecture,has_endowment(skolem0001),inference(split_conjunct,[status(thm)],[c12])).
% 27.89/28.15 cnf(c17,negated_conjecture,greater(age(skolem0001,skolem0004),eta),inference(split_conjunct,[status(thm)],[c12])).
% 27.89/28.15 fof(definition_1,axiom,(![X]:(has_endowment(X)<=>(![T]:((organization(X)&(smaller_or_equal(age(X,T),eta)=>has_immunity(X,T)))&(greater(age(X,T),eta)=>(~has_immunity(X,T))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', definition_1)).
% 27.89/28.15 fof(c27,plain,(![X]:(has_endowment(X)<=>(![T]:((organization(X)&(smaller_or_equal(age(X,T),eta)=>has_immunity(X,T)))&(greater(age(X,T),eta)=>~has_immunity(X,T)))))),inference(fof_simplification,[status(thm)],[definition_1])).
% 27.89/28.15 fof(c28,plain,(![X]:((~has_endowment(X)|(![T]:((organization(X)&(~smaller_or_equal(age(X,T),eta)|has_immunity(X,T)))&(~greater(age(X,T),eta)|~has_immunity(X,T)))))&((?[T]:((~organization(X)|(smaller_or_equal(age(X,T),eta)&~has_immunity(X,T)))|(greater(age(X,T),eta)&has_immunity(X,T))))|has_endowment(X)))),inference(fof_nnf,[status(thm)],[c27])).
% 27.89/28.15 fof(c29,plain,((![X]:(~has_endowment(X)|((organization(X)&(![T]:(~smaller_or_equal(age(X,T),eta)|has_immunity(X,T))))&(![T]:(~greater(age(X,T),eta)|~has_immunity(X,T))))))&(![X]:(((~organization(X)|(?[T]:(smaller_or_equal(age(X,T),eta)&~has_immunity(X,T))))|(?[T]:(greater(age(X,T),eta)&has_immunity(X,T))))|has_endowment(X)))),inference(shift_quantors,[status(thm)],[c28])).
% 27.89/28.15 fof(c30,plain,((![X12]:(~has_endowment(X12)|((organization(X12)&(![X13]:(~smaller_or_equal(age(X12,X13),eta)|has_immunity(X12,X13))))&(![X14]:(~greater(age(X12,X14),eta)|~has_immunity(X12,X14))))))&(![X15]:(((~organization(X15)|(?[X16]:(smaller_or_equal(age(X15,X16),eta)&~has_immunity(X15,X16))))|(?[X17]:(greater(age(X15,X17),eta)&has_immunity(X15,X17))))|has_endowment(X15)))),inference(variable_rename,[status(thm)],[c29])).
% 27.89/28.15 fof(c32,plain,(![X12]:(![X13]:(![X14]:(![X15]:((~has_endowment(X12)|((organization(X12)&(~smaller_or_equal(age(X12,X13),eta)|has_immunity(X12,X13)))&(~greater(age(X12,X14),eta)|~has_immunity(X12,X14))))&(((~organization(X15)|(smaller_or_equal(age(X15,skolem0005(X15)),eta)&~has_immunity(X15,skolem0005(X15))))|(greater(age(X15,skolem0006(X15)),eta)&has_immunity(X15,skolem0006(X15))))|has_endowment(X15))))))),inference(shift_quantors,[status(thm)],[fof(c31,plain,((![X12]:(~has_endowment(X12)|((organization(X12)&(![X13]:(~smaller_or_equal(age(X12,X13),eta)|has_immunity(X12,X13))))&(![X14]:(~greater(age(X12,X14),eta)|~has_immunity(X12,X14))))))&(![X15]:(((~organization(X15)|(smaller_or_equal(age(X15,skolem0005(X15)),eta)&~has_immunity(X15,skolem0005(X15))))|(greater(age(X15,skolem0006(X15)),eta)&has_immunity(X15,skolem0006(X15))))|has_endowment(X15)))),inference(skolemize,[status(esa)],[c30])).])).
% 27.89/28.15 fof(c33,plain,(![X12]:(![X13]:(![X14]:(![X15]:((((~has_endowment(X12)|organization(X12))&(~has_endowment(X12)|(~smaller_or_equal(age(X12,X13),eta)|has_immunity(X12,X13))))&(~has_endowment(X12)|(~greater(age(X12,X14),eta)|~has_immunity(X12,X14))))&(((((~organization(X15)|smaller_or_equal(age(X15,skolem0005(X15)),eta))|greater(age(X15,skolem0006(X15)),eta))|has_endowment(X15))&(((~organization(X15)|smaller_or_equal(age(X15,skolem0005(X15)),eta))|has_immunity(X15,skolem0006(X15)))|has_endowment(X15)))&((((~organization(X15)|~has_immunity(X15,skolem0005(X15)))|greater(age(X15,skolem0006(X15)),eta))|has_endowment(X15))&(((~organization(X15)|~has_immunity(X15,skolem0005(X15)))|has_immunity(X15,skolem0006(X15)))|has_endowment(X15))))))))),inference(distribute,[status(thm)],[c32])).
% 27.89/28.15 cnf(c36,plain,~has_endowment(X132)|~greater(age(X132,X133),eta)|~has_immunity(X132,X133),inference(split_conjunct,[status(thm)],[c33])).
% 27.89/28.15 cnf(c194,plain,~has_endowment(skolem0001)|~has_immunity(skolem0001,skolem0004),inference(resolution,[status(thm)],[c36, c17])).
% 27.89/28.15 cnf(c13,negated_conjecture,organization(skolem0001),inference(split_conjunct,[status(thm)],[c12])).
% 27.89/28.15 fof(assumption_3,axiom,(![X]:(![T0]:(![T]:(((organization(X)&has_immunity(X,T0))&(~has_immunity(X,T)))=>greater(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_3)).
% 27.89/28.15 fof(c20,plain,(![X]:(![T0]:(![T]:(((organization(X)&has_immunity(X,T0))&~has_immunity(X,T))=>greater(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)))))),inference(fof_simplification,[status(thm)],[assumption_3])).
% 27.89/28.15 fof(c21,plain,(![X]:(![T0]:(![T]:(((~organization(X)|~has_immunity(X,T0))|has_immunity(X,T))|greater(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)))))),inference(fof_nnf,[status(thm)],[c20])).
% 27.89/28.15 fof(c22,plain,(![X6]:(![X7]:(![X8]:(((~organization(X6)|~has_immunity(X6,X7))|has_immunity(X6,X8))|greater(hazard_of_mortality(X6,X8),hazard_of_mortality(X6,X7)))))),inference(variable_rename,[status(thm)],[c21])).
% 27.89/28.15 cnf(c23,plain,~organization(X111)|~has_immunity(X111,X112)|has_immunity(X111,X110)|greater(hazard_of_mortality(X111,X110),hazard_of_mortality(X111,X112)),inference(split_conjunct,[status(thm)],[c22])).
% 27.89/28.15 cnf(c16,negated_conjecture,smaller_or_equal(age(skolem0001,skolem0003),eta),inference(split_conjunct,[status(thm)],[c12])).
% 27.89/28.15 cnf(c35,plain,~has_endowment(X128)|~smaller_or_equal(age(X128,X127),eta)|has_immunity(X128,X127),inference(split_conjunct,[status(thm)],[c33])).
% 27.89/28.15 cnf(c184,plain,~has_endowment(skolem0001)|has_immunity(skolem0001,skolem0003),inference(resolution,[status(thm)],[c35, c16])).
% 27.89/28.15 cnf(c185,plain,has_immunity(skolem0001,skolem0003),inference(resolution,[status(thm)],[c184, c14])).
% 27.89/28.15 cnf(c188,plain,~organization(skolem0001)|has_immunity(skolem0001,X630)|greater(hazard_of_mortality(skolem0001,X630),hazard_of_mortality(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c185, c23])).
% 27.89/28.15 cnf(c1386,plain,has_immunity(skolem0001,X6123)|greater(hazard_of_mortality(skolem0001,X6123),hazard_of_mortality(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c188, c13])).
% 27.89/28.15 cnf(c19,negated_conjecture,~greater(hazard_of_mortality(skolem0001,skolem0004),hazard_of_mortality(skolem0001,skolem0003))|hazard_of_mortality(skolem0001,skolem0003)!=hazard_of_mortality(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c12])).
% 27.89/28.15 cnf(symmetry,axiom,X39!=X40|X40=X39,theory(equality)).
% 27.89/28.15 cnf(c15,negated_conjecture,age(skolem0001,skolem0002)=zero,inference(split_conjunct,[status(thm)],[c12])).
% 27.89/28.15 cnf(c97,plain,zero=age(skolem0001,skolem0002),inference(resolution,[status(thm)],[c15, symmetry])).
% 27.89/28.15 cnf(reflexivity,axiom,X37=X37,theory(equality)).
% 27.89/28.15 cnf(c18,negated_conjecture,greater(eta,zero),inference(split_conjunct,[status(thm)],[c12])).
% 27.89/28.15 fof(definition_smaller,axiom,(![X]:(![Y]:(smaller(X,Y)<=>greater(Y,X)))),file('/export/starexec/sandbox2/benchmark/Axioms/MGT001+0.ax', definition_smaller)).
% 27.89/28.15 fof(c49,plain,(![X]:(![Y]:((~smaller(X,Y)|greater(Y,X))&(~greater(Y,X)|smaller(X,Y))))),inference(fof_nnf,[status(thm)],[definition_smaller])).
% 27.89/28.15 fof(c50,plain,((![X]:(![Y]:(~smaller(X,Y)|greater(Y,X))))&(![X]:(![Y]:(~greater(Y,X)|smaller(X,Y))))),inference(shift_quantors,[status(thm)],[c49])).
% 27.89/28.15 fof(c52,plain,(![X25]:(![X26]:(![X27]:(![X28]:((~smaller(X25,X26)|greater(X26,X25))&(~greater(X28,X27)|smaller(X27,X28))))))),inference(shift_quantors,[status(thm)],[fof(c51,plain,((![X25]:(![X26]:(~smaller(X25,X26)|greater(X26,X25))))&(![X27]:(![X28]:(~greater(X28,X27)|smaller(X27,X28))))),inference(variable_rename,[status(thm)],[c50])).])).
% 27.89/28.15 cnf(c54,plain,~greater(X50,X51)|smaller(X51,X50),inference(split_conjunct,[status(thm)],[c52])).
% 27.89/28.15 cnf(c77,plain,smaller(zero,eta),inference(resolution,[status(thm)],[c54, c18])).
% 27.89/28.15 fof(definition_smaller_or_equal,axiom,(![X]:(![Y]:(smaller_or_equal(X,Y)<=>(smaller(X,Y)|X=Y)))),file('/export/starexec/sandbox2/benchmark/Axioms/MGT001+0.ax', definition_smaller_or_equal)).
% 27.89/28.15 fof(c63,plain,(![X]:(![Y]:((~smaller_or_equal(X,Y)|(smaller(X,Y)|X=Y))&((~smaller(X,Y)&X!=Y)|smaller_or_equal(X,Y))))),inference(fof_nnf,[status(thm)],[definition_smaller_or_equal])).
% 27.89/28.15 fof(c64,plain,((![X]:(![Y]:(~smaller_or_equal(X,Y)|(smaller(X,Y)|X=Y))))&(![X]:(![Y]:((~smaller(X,Y)&X!=Y)|smaller_or_equal(X,Y))))),inference(shift_quantors,[status(thm)],[c63])).
% 27.89/28.15 fof(c66,plain,(![X33]:(![X34]:(![X35]:(![X36]:((~smaller_or_equal(X33,X34)|(smaller(X33,X34)|X33=X34))&((~smaller(X35,X36)&X35!=X36)|smaller_or_equal(X35,X36))))))),inference(shift_quantors,[status(thm)],[fof(c65,plain,((![X33]:(![X34]:(~smaller_or_equal(X33,X34)|(smaller(X33,X34)|X33=X34))))&(![X35]:(![X36]:((~smaller(X35,X36)&X35!=X36)|smaller_or_equal(X35,X36))))),inference(variable_rename,[status(thm)],[c64])).])).
% 27.89/28.15 fof(c67,plain,(![X33]:(![X34]:(![X35]:(![X36]:((~smaller_or_equal(X33,X34)|(smaller(X33,X34)|X33=X34))&((~smaller(X35,X36)|smaller_or_equal(X35,X36))&(X35!=X36|smaller_or_equal(X35,X36)))))))),inference(distribute,[status(thm)],[c66])).
% 27.89/28.15 cnf(c69,plain,~smaller(X62,X61)|smaller_or_equal(X62,X61),inference(split_conjunct,[status(thm)],[c67])).
% 27.89/28.15 cnf(c83,plain,smaller_or_equal(zero,eta),inference(resolution,[status(thm)],[c69, c77])).
% 27.89/28.15 cnf(c2,axiom,X76!=X75|X78!=X77|~smaller_or_equal(X76,X78)|smaller_or_equal(X75,X77),theory(equality)).
% 27.89/28.15 cnf(c88,plain,zero!=X199|eta!=X198|smaller_or_equal(X199,X198),inference(resolution,[status(thm)],[c2, c83])).
% 27.89/28.15 cnf(c393,plain,zero!=X218|smaller_or_equal(X218,eta),inference(resolution,[status(thm)],[c88, reflexivity])).
% 27.89/28.15 cnf(c423,plain,smaller_or_equal(age(skolem0001,skolem0002),eta),inference(resolution,[status(thm)],[c393, c97])).
% 27.89/28.15 cnf(c454,plain,~has_endowment(skolem0001)|has_immunity(skolem0001,skolem0002),inference(resolution,[status(thm)],[c423, c35])).
% 27.89/28.15 cnf(c458,plain,has_immunity(skolem0001,skolem0002),inference(resolution,[status(thm)],[c454, c14])).
% 27.89/28.15 fof(assumption_2,axiom,(![X]:(![T0]:(![T]:(((organization(X)&has_immunity(X,T0))&has_immunity(X,T))=>hazard_of_mortality(X,T0)=hazard_of_mortality(X,T))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_2)).
% 27.89/28.15 fof(c24,plain,(![X]:(![T0]:(![T]:(((~organization(X)|~has_immunity(X,T0))|~has_immunity(X,T))|hazard_of_mortality(X,T0)=hazard_of_mortality(X,T))))),inference(fof_nnf,[status(thm)],[assumption_2])).
% 27.89/28.15 fof(c25,plain,(![X9]:(![X10]:(![X11]:(((~organization(X9)|~has_immunity(X9,X10))|~has_immunity(X9,X11))|hazard_of_mortality(X9,X10)=hazard_of_mortality(X9,X11))))),inference(variable_rename,[status(thm)],[c24])).
% 27.89/28.15 cnf(c26,plain,~organization(X125)|~has_immunity(X125,X123)|~has_immunity(X125,X124)|hazard_of_mortality(X125,X123)=hazard_of_mortality(X125,X124),inference(split_conjunct,[status(thm)],[c25])).
% 27.89/28.15 cnf(c187,plain,~organization(skolem0001)|~has_immunity(skolem0001,X624)|hazard_of_mortality(skolem0001,X624)=hazard_of_mortality(skolem0001,skolem0003),inference(resolution,[status(thm)],[c185, c26])).
% 27.89/28.15 cnf(c1384,plain,~organization(skolem0001)|hazard_of_mortality(skolem0001,skolem0002)=hazard_of_mortality(skolem0001,skolem0003),inference(resolution,[status(thm)],[c187, c458])).
% 27.89/28.15 cnf(c83865,plain,hazard_of_mortality(skolem0001,skolem0002)=hazard_of_mortality(skolem0001,skolem0003),inference(resolution,[status(thm)],[c1384, c13])).
% 27.89/28.15 cnf(c83870,plain,hazard_of_mortality(skolem0001,skolem0003)=hazard_of_mortality(skolem0001,skolem0002),inference(resolution,[status(thm)],[c83865, symmetry])).
% 27.89/28.15 cnf(c84157,plain,~greater(hazard_of_mortality(skolem0001,skolem0004),hazard_of_mortality(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c83870, c19])).
% 27.89/28.15 cnf(c84431,plain,has_immunity(skolem0001,skolem0004),inference(resolution,[status(thm)],[c84157, c1386])).
% 27.89/28.15 cnf(c84474,plain,~has_endowment(skolem0001),inference(resolution,[status(thm)],[c84431, c194])).
% 27.89/28.15 cnf(c84484,plain,$false,inference(resolution,[status(thm)],[c84474, c14])).
% 27.89/28.15 % SZS output end CNFRefutation
% 27.89/28.15
% 27.89/28.15 % Initial clauses : 39
% 27.89/28.15 % Processed clauses : 1034
% 27.89/28.15 % Factors computed : 365
% 27.89/28.15 % Resolvents computed: 84060
% 27.89/28.15 % Tautologies deleted: 19
% 27.89/28.15 % Forward subsumed : 3231
% 27.89/28.15 % Backward subsumed : 35
% 27.89/28.15 % -------- CPU Time ---------
% 27.89/28.15 % User time : 27.632 s
% 27.89/28.15 % System time : 0.173 s
% 27.89/28.15 % Total time : 27.805 s
%------------------------------------------------------------------------------