%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : MED001+1 : TPTP v5.0.0. Released v3.2.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art02.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Wed Dec 29 15:59:42 EST 2010
% Result : Theorem 1.04s
% Output : Solution 1.04s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP32126/MED001+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP32126/MED001+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP32126/MED001+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 32222
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.015 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(5, axiom,![X4]:((((![X5]:(~(gt(X4,X5))=>bsecretioni(X5))&bcapacitysn(X4))&qilt27(X4))&![X5]:(gt(X4,X5)=>conditionhyper(X5)))=>![X5]:(~(gt(X4,X5))=>conditionnormo(X5))),file('/tmp/SRASS.s.p', sn_cure_1)).
% fof(7, axiom,![X4]:(~(bcapacityex(X4))|~(bcapacitysn(X4))),file('/tmp/SRASS.s.p', xorcapacity4)).
% fof(9, axiom,![X4]:((![X5]:(~(gt(X4,X5))=>drugsu(X5))&~(bcapacityex(X4)))=>![X5]:(~(gt(X4,X5))=>bsecretioni(X5))),file('/tmp/SRASS.s.p', sulfonylurea_effect)).
% fof(19, conjecture,((((![X4]:(~(gt(n0,X4))=>drugsu(X4))&![X4]:(gt(n0,X4)=>conditionhyper(X4)))&bcapacitysn(n0))&qilt27(n0))=>![X4]:(~(gt(n0,X4))=>conditionnormo(X4))),file('/tmp/SRASS.s.p', treatmentsn2)).
% fof(20, negated_conjecture,~(((((![X4]:(~(gt(n0,X4))=>drugsu(X4))&![X4]:(gt(n0,X4)=>conditionhyper(X4)))&bcapacitysn(n0))&qilt27(n0))=>![X4]:(~(gt(n0,X4))=>conditionnormo(X4)))),inference(assume_negation,[status(cth)],[19])).
% fof(24, plain,![X4]:((((![X5]:(~(gt(X4,X5))=>bsecretioni(X5))&bcapacitysn(X4))&qilt27(X4))&![X5]:(gt(X4,X5)=>conditionhyper(X5)))=>![X5]:(~(gt(X4,X5))=>conditionnormo(X5))),inference(fof_simplification,[status(thm)],[5,theory(equality)])).
% fof(25, plain,![X4]:(~(bcapacityex(X4))|~(bcapacitysn(X4))),inference(fof_simplification,[status(thm)],[7,theory(equality)])).
% fof(27, plain,![X4]:((![X5]:(~(gt(X4,X5))=>drugsu(X5))&~(bcapacityex(X4)))=>![X5]:(~(gt(X4,X5))=>bsecretioni(X5))),inference(fof_simplification,[status(thm)],[9,theory(equality)])).
% fof(36, negated_conjecture,~(((((![X4]:(~(gt(n0,X4))=>drugsu(X4))&![X4]:(gt(n0,X4)=>conditionhyper(X4)))&bcapacitysn(n0))&qilt27(n0))=>![X4]:(~(gt(n0,X4))=>conditionnormo(X4)))),inference(fof_simplification,[status(thm)],[20,theory(equality)])).
% fof(53, plain,![X4]:((((?[X5]:(~(gt(X4,X5))&~(bsecretioni(X5)))|~(bcapacitysn(X4)))|~(qilt27(X4)))|?[X5]:(gt(X4,X5)&~(conditionhyper(X5))))|![X5]:(gt(X4,X5)|conditionnormo(X5))),inference(fof_nnf,[status(thm)],[24])).
% fof(54, plain,![X6]:((((?[X7]:(~(gt(X6,X7))&~(bsecretioni(X7)))|~(bcapacitysn(X6)))|~(qilt27(X6)))|?[X8]:(gt(X6,X8)&~(conditionhyper(X8))))|![X9]:(gt(X6,X9)|conditionnormo(X9))),inference(variable_rename,[status(thm)],[53])).
% fof(55, plain,![X6]:(((((~(gt(X6,esk3_1(X6)))&~(bsecretioni(esk3_1(X6))))|~(bcapacitysn(X6)))|~(qilt27(X6)))|(gt(X6,esk4_1(X6))&~(conditionhyper(esk4_1(X6)))))|![X9]:(gt(X6,X9)|conditionnormo(X9))),inference(skolemize,[status(esa)],[54])).
% fof(56, plain,![X6]:![X9]:((gt(X6,X9)|conditionnormo(X9))|((((~(gt(X6,esk3_1(X6)))&~(bsecretioni(esk3_1(X6))))|~(bcapacitysn(X6)))|~(qilt27(X6)))|(gt(X6,esk4_1(X6))&~(conditionhyper(esk4_1(X6)))))),inference(shift_quantors,[status(thm)],[55])).
% fof(57, plain,![X6]:![X9]:((((gt(X6,esk4_1(X6))|((~(gt(X6,esk3_1(X6)))|~(bcapacitysn(X6)))|~(qilt27(X6))))|(gt(X6,X9)|conditionnormo(X9)))&((~(conditionhyper(esk4_1(X6)))|((~(gt(X6,esk3_1(X6)))|~(bcapacitysn(X6)))|~(qilt27(X6))))|(gt(X6,X9)|conditionnormo(X9))))&(((gt(X6,esk4_1(X6))|((~(bsecretioni(esk3_1(X6)))|~(bcapacitysn(X6)))|~(qilt27(X6))))|(gt(X6,X9)|conditionnormo(X9)))&((~(conditionhyper(esk4_1(X6)))|((~(bsecretioni(esk3_1(X6)))|~(bcapacitysn(X6)))|~(qilt27(X6))))|(gt(X6,X9)|conditionnormo(X9))))),inference(distribute,[status(thm)],[56])).
% cnf(58,plain,(conditionnormo(X1)|gt(X2,X1)|~qilt27(X2)|~bcapacitysn(X2)|~bsecretioni(esk3_1(X2))|~conditionhyper(esk4_1(X2))),inference(split_conjunct,[status(thm)],[57])).
% cnf(59,plain,(conditionnormo(X1)|gt(X2,X1)|gt(X2,esk4_1(X2))|~qilt27(X2)|~bcapacitysn(X2)|~bsecretioni(esk3_1(X2))),inference(split_conjunct,[status(thm)],[57])).
% cnf(60,plain,(conditionnormo(X1)|gt(X2,X1)|~qilt27(X2)|~bcapacitysn(X2)|~gt(X2,esk3_1(X2))|~conditionhyper(esk4_1(X2))),inference(split_conjunct,[status(thm)],[57])).
% cnf(61,plain,(conditionnormo(X1)|gt(X2,X1)|gt(X2,esk4_1(X2))|~qilt27(X2)|~bcapacitysn(X2)|~gt(X2,esk3_1(X2))),inference(split_conjunct,[status(thm)],[57])).
% fof(64, plain,![X5]:(~(bcapacityex(X5))|~(bcapacitysn(X5))),inference(variable_rename,[status(thm)],[25])).
% cnf(65,plain,(~bcapacitysn(X1)|~bcapacityex(X1)),inference(split_conjunct,[status(thm)],[64])).
% fof(68, plain,![X4]:((?[X5]:(~(gt(X4,X5))&~(drugsu(X5)))|bcapacityex(X4))|![X5]:(gt(X4,X5)|bsecretioni(X5))),inference(fof_nnf,[status(thm)],[27])).
% fof(69, plain,![X6]:((?[X7]:(~(gt(X6,X7))&~(drugsu(X7)))|bcapacityex(X6))|![X8]:(gt(X6,X8)|bsecretioni(X8))),inference(variable_rename,[status(thm)],[68])).
% fof(70, plain,![X6]:(((~(gt(X6,esk5_1(X6)))&~(drugsu(esk5_1(X6))))|bcapacityex(X6))|![X8]:(gt(X6,X8)|bsecretioni(X8))),inference(skolemize,[status(esa)],[69])).
% fof(71, plain,![X6]:![X8]:((gt(X6,X8)|bsecretioni(X8))|((~(gt(X6,esk5_1(X6)))&~(drugsu(esk5_1(X6))))|bcapacityex(X6))),inference(shift_quantors,[status(thm)],[70])).
% fof(72, plain,![X6]:![X8]:(((~(gt(X6,esk5_1(X6)))|bcapacityex(X6))|(gt(X6,X8)|bsecretioni(X8)))&((~(drugsu(esk5_1(X6)))|bcapacityex(X6))|(gt(X6,X8)|bsecretioni(X8)))),inference(distribute,[status(thm)],[71])).
% cnf(73,plain,(bsecretioni(X1)|gt(X2,X1)|bcapacityex(X2)|~drugsu(esk5_1(X2))),inference(split_conjunct,[status(thm)],[72])).
% cnf(74,plain,(bsecretioni(X1)|gt(X2,X1)|bcapacityex(X2)|~gt(X2,esk5_1(X2))),inference(split_conjunct,[status(thm)],[72])).
% fof(136, negated_conjecture,((((![X4]:(gt(n0,X4)|drugsu(X4))&![X4]:(~(gt(n0,X4))|conditionhyper(X4)))&bcapacitysn(n0))&qilt27(n0))&?[X4]:(~(gt(n0,X4))&~(conditionnormo(X4)))),inference(fof_nnf,[status(thm)],[36])).
% fof(137, negated_conjecture,((((![X5]:(gt(n0,X5)|drugsu(X5))&![X6]:(~(gt(n0,X6))|conditionhyper(X6)))&bcapacitysn(n0))&qilt27(n0))&?[X7]:(~(gt(n0,X7))&~(conditionnormo(X7)))),inference(variable_rename,[status(thm)],[136])).
% fof(138, negated_conjecture,((((![X5]:(gt(n0,X5)|drugsu(X5))&![X6]:(~(gt(n0,X6))|conditionhyper(X6)))&bcapacitysn(n0))&qilt27(n0))&(~(gt(n0,esk15_0))&~(conditionnormo(esk15_0)))),inference(skolemize,[status(esa)],[137])).
% fof(139, negated_conjecture,![X5]:![X6]:(((((~(gt(n0,X6))|conditionhyper(X6))&(gt(n0,X5)|drugsu(X5)))&bcapacitysn(n0))&qilt27(n0))&(~(gt(n0,esk15_0))&~(conditionnormo(esk15_0)))),inference(shift_quantors,[status(thm)],[138])).
% cnf(140,negated_conjecture,(~conditionnormo(esk15_0)),inference(split_conjunct,[status(thm)],[139])).
% cnf(141,negated_conjecture,(~gt(n0,esk15_0)),inference(split_conjunct,[status(thm)],[139])).
% cnf(142,negated_conjecture,(qilt27(n0)),inference(split_conjunct,[status(thm)],[139])).
% cnf(143,negated_conjecture,(bcapacitysn(n0)),inference(split_conjunct,[status(thm)],[139])).
% cnf(144,negated_conjecture,(drugsu(X1)|gt(n0,X1)),inference(split_conjunct,[status(thm)],[139])).
% cnf(145,negated_conjecture,(conditionhyper(X1)|~gt(n0,X1)),inference(split_conjunct,[status(thm)],[139])).
% cnf(192,negated_conjecture,(bcapacityex(n0)|bsecretioni(X1)|gt(n0,X1)|drugsu(esk5_1(n0))),inference(spm,[status(thm)],[74,144,theory(equality)])).
% cnf(214,negated_conjecture,(conditionnormo(esk15_0)|~bsecretioni(esk3_1(n0))|~qilt27(n0)|~bcapacitysn(n0)|~conditionhyper(esk4_1(n0))),inference(spm,[status(thm)],[141,58,theory(equality)])).
% cnf(222,negated_conjecture,(conditionnormo(esk15_0)|~bsecretioni(esk3_1(n0))|$false|~bcapacitysn(n0)|~conditionhyper(esk4_1(n0))),inference(rw,[status(thm)],[214,142,theory(equality)])).
% cnf(223,negated_conjecture,(conditionnormo(esk15_0)|~bsecretioni(esk3_1(n0))|$false|$false|~conditionhyper(esk4_1(n0))),inference(rw,[status(thm)],[222,143,theory(equality)])).
% cnf(224,negated_conjecture,(conditionnormo(esk15_0)|~bsecretioni(esk3_1(n0))|~conditionhyper(esk4_1(n0))),inference(cn,[status(thm)],[223,theory(equality)])).
% cnf(225,negated_conjecture,(~bsecretioni(esk3_1(n0))|~conditionhyper(esk4_1(n0))),inference(sr,[status(thm)],[224,140,theory(equality)])).
% cnf(643,negated_conjecture,(bcapacityex(n0)|bsecretioni(X1)|gt(n0,X1)),inference(csr,[status(thm)],[192,73])).
% cnf(666,negated_conjecture,(conditionnormo(X1)|gt(n0,X1)|bcapacityex(n0)|bsecretioni(esk3_1(n0))|~qilt27(n0)|~bcapacitysn(n0)|~conditionhyper(esk4_1(n0))),inference(spm,[status(thm)],[60,643,theory(equality)])).
% cnf(667,negated_conjecture,(conditionnormo(X1)|gt(n0,esk4_1(n0))|gt(n0,X1)|bcapacityex(n0)|bsecretioni(esk3_1(n0))|~qilt27(n0)|~bcapacitysn(n0)),inference(spm,[status(thm)],[61,643,theory(equality)])).
% cnf(674,negated_conjecture,(conditionnormo(X1)|gt(n0,X1)|bcapacityex(n0)|bsecretioni(esk3_1(n0))|$false|~bcapacitysn(n0)|~conditionhyper(esk4_1(n0))),inference(rw,[status(thm)],[666,142,theory(equality)])).
% cnf(675,negated_conjecture,(conditionnormo(X1)|gt(n0,X1)|bcapacityex(n0)|bsecretioni(esk3_1(n0))|$false|$false|~conditionhyper(esk4_1(n0))),inference(rw,[status(thm)],[674,143,theory(equality)])).
% cnf(676,negated_conjecture,(conditionnormo(X1)|gt(n0,X1)|bcapacityex(n0)|bsecretioni(esk3_1(n0))|~conditionhyper(esk4_1(n0))),inference(cn,[status(thm)],[675,theory(equality)])).
% cnf(677,negated_conjecture,(conditionnormo(X1)|gt(n0,esk4_1(n0))|gt(n0,X1)|bcapacityex(n0)|bsecretioni(esk3_1(n0))|$false|~bcapacitysn(n0)),inference(rw,[status(thm)],[667,142,theory(equality)])).
% cnf(678,negated_conjecture,(conditionnormo(X1)|gt(n0,esk4_1(n0))|gt(n0,X1)|bcapacityex(n0)|bsecretioni(esk3_1(n0))|$false|$false),inference(rw,[status(thm)],[677,143,theory(equality)])).
% cnf(679,negated_conjecture,(conditionnormo(X1)|gt(n0,esk4_1(n0))|gt(n0,X1)|bcapacityex(n0)|bsecretioni(esk3_1(n0))),inference(cn,[status(thm)],[678,theory(equality)])).
% cnf(1708,negated_conjecture,(conditionhyper(esk4_1(n0))|bcapacityex(n0)|bsecretioni(esk3_1(n0))|conditionnormo(X1)|gt(n0,X1)),inference(spm,[status(thm)],[145,679,theory(equality)])).
% cnf(2437,negated_conjecture,(bcapacityex(n0)|conditionnormo(X1)|gt(n0,X1)|~conditionhyper(esk4_1(n0))),inference(csr,[status(thm)],[676,225])).
% cnf(2476,negated_conjecture,(bcapacityex(n0)|conditionnormo(esk15_0)|~conditionhyper(esk4_1(n0))),inference(spm,[status(thm)],[141,2437,theory(equality)])).
% cnf(2490,negated_conjecture,(bcapacityex(n0)|~conditionhyper(esk4_1(n0))),inference(sr,[status(thm)],[2476,140,theory(equality)])).
% cnf(2614,negated_conjecture,(bcapacityex(n0)|bsecretioni(esk3_1(n0))|conditionnormo(X1)|gt(n0,X1)),inference(csr,[status(thm)],[1708,2490])).
% cnf(2653,negated_conjecture,(bcapacityex(n0)|bsecretioni(esk3_1(n0))|conditionnormo(esk15_0)),inference(spm,[status(thm)],[141,2614,theory(equality)])).
% cnf(2667,negated_conjecture,(bcapacityex(n0)|bsecretioni(esk3_1(n0))),inference(sr,[status(thm)],[2653,140,theory(equality)])).
% cnf(2668,negated_conjecture,(conditionnormo(X1)|gt(n0,esk4_1(n0))|gt(n0,X1)|bcapacityex(n0)|~qilt27(n0)|~bcapacitysn(n0)),inference(spm,[status(thm)],[59,2667,theory(equality)])).
% cnf(2673,negated_conjecture,(conditionnormo(X1)|gt(n0,esk4_1(n0))|gt(n0,X1)|bcapacityex(n0)|$false|~bcapacitysn(n0)),inference(rw,[status(thm)],[2668,142,theory(equality)])).
% cnf(2674,negated_conjecture,(conditionnormo(X1)|gt(n0,esk4_1(n0))|gt(n0,X1)|bcapacityex(n0)|$false|$false),inference(rw,[status(thm)],[2673,143,theory(equality)])).
% cnf(2675,negated_conjecture,(conditionnormo(X1)|gt(n0,esk4_1(n0))|gt(n0,X1)|bcapacityex(n0)),inference(cn,[status(thm)],[2674,theory(equality)])).
% cnf(2759,negated_conjecture,(conditionhyper(esk4_1(n0))|bcapacityex(n0)|conditionnormo(X1)|gt(n0,X1)),inference(spm,[status(thm)],[145,2675,theory(equality)])).
% cnf(2827,negated_conjecture,(bcapacityex(n0)|conditionnormo(X1)|gt(n0,X1)),inference(csr,[status(thm)],[2759,2490])).
% cnf(2866,negated_conjecture,(bcapacityex(n0)|conditionnormo(esk15_0)),inference(spm,[status(thm)],[141,2827,theory(equality)])).
% cnf(2880,negated_conjecture,(bcapacityex(n0)),inference(sr,[status(thm)],[2866,140,theory(equality)])).
% cnf(2881,negated_conjecture,(~bcapacitysn(n0)),inference(spm,[status(thm)],[65,2880,theory(equality)])).
% cnf(2938,negated_conjecture,($false),inference(rw,[status(thm)],[2881,143,theory(equality)])).
% cnf(2939,negated_conjecture,($false),inference(cn,[status(thm)],[2938,theory(equality)])).
% cnf(2940,negated_conjecture,($false),2939,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 363
% # ...of these trivial : 0
% # ...subsumed : 78
% # ...remaining for further processing: 285
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 16
% # Backward-rewritten : 56
% # Generated clauses : 2240
% # ...of the previous two non-trivial : 2029
% # Contextual simplify-reflections : 134
% # Paramodulations : 2230
% # Factorizations : 10
% # Equation resolutions : 0
% # Current number of processed clauses: 213
% # Positive orientable unit clauses: 6
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 3
% # Non-unit-clauses : 204
% # Current number of unprocessed clauses: 1331
% # ...number of literals in the above : 10883
% # Clause-clause subsumption calls (NU) : 4093
% # Rec. Clause-clause subsumption calls : 1982
% # Unit Clause-clause subsumption calls : 106
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 2
% # Indexed BW rewrite successes : 2
% # Backwards rewriting index: 126 leaves, 1.42+/-0.738 terms/leaf
% # Paramod-from index: 34 leaves, 1.03+/-0.169 terms/leaf
% # Paramod-into index: 89 leaves, 1.19+/-0.701 terms/leaf
% # -------------------------------------------------
% # User time : 0.127 s
% # System time : 0.005 s
% # Total time : 0.132 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.25 CPU 0.34 WC
% FINAL PrfWatch: 0.25 CPU 0.34 WC
% SZS output end Solution for /tmp/SystemOnTPTP32126/MED001+1.tptp
%
%------------------------------------------------------------------------------