%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MED001+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:32:58 EDT 2024
% Result : Theorem 5.45s 5.64s
% Output : Refutation 5.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : MED001+1 : TPTP v8.1.2. Released v3.2.0.
% 0.03/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n013.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 15:43:23 EDT 2024
% 0.15/0.36 % CPUTime :
% 5.45/5.64 % Version: 1.5
% 5.45/5.64 % SZS status Theorem
% 5.45/5.64 % SZS output start CNFRefutation
% 5.45/5.64 fof(treatmentsn2,conjecture,(((((![X0]:((~gt(n0,X0))=>drugsu(X0)))&(![X0]:(gt(n0,X0)=>conditionhyper(X0))))&bcapacitysn(n0))&qilt27(n0))=>(![X0]:((~gt(n0,X0))=>conditionnormo(X0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', treatmentsn2)).
% 5.45/5.64 fof(c0,negated_conjecture,(~(((((![X0]:((~gt(n0,X0))=>drugsu(X0)))&(![X0]:(gt(n0,X0)=>conditionhyper(X0))))&bcapacitysn(n0))&qilt27(n0))=>(![X0]:((~gt(n0,X0))=>conditionnormo(X0))))),inference(assume_negation,[status(cth)],[treatmentsn2])).
% 5.45/5.64 fof(c1,negated_conjecture,(~(((((![X0]:(~gt(n0,X0)=>drugsu(X0)))&(![X0]:(gt(n0,X0)=>conditionhyper(X0))))&bcapacitysn(n0))&qilt27(n0))=>(![X0]:(~gt(n0,X0)=>conditionnormo(X0))))),inference(fof_simplification,[status(thm)],[c0])).
% 5.45/5.64 fof(c2,negated_conjecture,(((((![X0]:(gt(n0,X0)|drugsu(X0)))&(![X0]:(~gt(n0,X0)|conditionhyper(X0))))&bcapacitysn(n0))&qilt27(n0))&(?[X0]:(~gt(n0,X0)&~conditionnormo(X0)))),inference(fof_nnf,[status(thm)],[c1])).
% 5.45/5.64 fof(c3,negated_conjecture,(((((![X2]:(gt(n0,X2)|drugsu(X2)))&(![X3]:(~gt(n0,X3)|conditionhyper(X3))))&bcapacitysn(n0))&qilt27(n0))&(?[X4]:(~gt(n0,X4)&~conditionnormo(X4)))),inference(variable_rename,[status(thm)],[c2])).
% 5.45/5.64 fof(c5,negated_conjecture,(![X2]:(![X3]:(((((gt(n0,X2)|drugsu(X2))&(~gt(n0,X3)|conditionhyper(X3)))&bcapacitysn(n0))&qilt27(n0))&(~gt(n0,skolem0001)&~conditionnormo(skolem0001))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,(((((![X2]:(gt(n0,X2)|drugsu(X2)))&(![X3]:(~gt(n0,X3)|conditionhyper(X3))))&bcapacitysn(n0))&qilt27(n0))&(~gt(n0,skolem0001)&~conditionnormo(skolem0001))),inference(skolemize,[status(esa)],[c3])).])).
% 5.45/5.64 cnf(c11,negated_conjecture,~conditionnormo(skolem0001),inference(split_conjunct,[status(thm)],[c5])).
% 5.45/5.64 cnf(c10,negated_conjecture,~gt(n0,skolem0001),inference(split_conjunct,[status(thm)],[c5])).
% 5.45/5.64 cnf(c8,negated_conjecture,bcapacitysn(n0),inference(split_conjunct,[status(thm)],[c5])).
% 5.45/5.64 cnf(c9,negated_conjecture,qilt27(n0),inference(split_conjunct,[status(thm)],[c5])).
% 5.45/5.64 fof(sn_cure_1,axiom,(![X0]:(((((![X1]:((~gt(X0,X1))=>bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0))&(![X1]:(gt(X0,X1)=>conditionhyper(X1))))=>(![X1]:((~gt(X0,X1))=>conditionnormo(X1))))),file('/export/starexec/sandbox/benchmark/Axioms/MED001+0.ax', sn_cure_1)).
% 5.45/5.64 fof(c58,plain,(![X0]:(((((![X1]:(~gt(X0,X1)=>bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0))&(![X1]:(gt(X0,X1)=>conditionhyper(X1))))=>(![X1]:(~gt(X0,X1)=>conditionnormo(X1))))),inference(fof_simplification,[status(thm)],[sn_cure_1])).
% 5.45/5.64 fof(c59,plain,(![X0]:(((((?[X1]:(~gt(X0,X1)&~bsecretioni(X1)))|~bcapacitysn(X0))|~qilt27(X0))|(?[X1]:(gt(X0,X1)&~conditionhyper(X1))))|(![X1]:(gt(X0,X1)|conditionnormo(X1))))),inference(fof_nnf,[status(thm)],[c58])).
% 5.45/5.64 fof(c60,plain,(![X20]:(((((?[X21]:(~gt(X20,X21)&~bsecretioni(X21)))|~bcapacitysn(X20))|~qilt27(X20))|(?[X22]:(gt(X20,X22)&~conditionhyper(X22))))|(![X23]:(gt(X20,X23)|conditionnormo(X23))))),inference(variable_rename,[status(thm)],[c59])).
% 5.45/5.64 fof(c62,plain,(![X20]:(![X23]:(((((~gt(X20,skolem0011(X20))&~bsecretioni(skolem0011(X20)))|~bcapacitysn(X20))|~qilt27(X20))|(gt(X20,skolem0012(X20))&~conditionhyper(skolem0012(X20))))|(gt(X20,X23)|conditionnormo(X23))))),inference(shift_quantors,[status(thm)],[fof(c61,plain,(![X20]:(((((~gt(X20,skolem0011(X20))&~bsecretioni(skolem0011(X20)))|~bcapacitysn(X20))|~qilt27(X20))|(gt(X20,skolem0012(X20))&~conditionhyper(skolem0012(X20))))|(![X23]:(gt(X20,X23)|conditionnormo(X23))))),inference(skolemize,[status(esa)],[c60])).])).
% 5.45/5.64 fof(c63,plain,(![X20]:(![X23]:((((((~gt(X20,skolem0011(X20))|~bcapacitysn(X20))|~qilt27(X20))|gt(X20,skolem0012(X20)))|(gt(X20,X23)|conditionnormo(X23)))&((((~gt(X20,skolem0011(X20))|~bcapacitysn(X20))|~qilt27(X20))|~conditionhyper(skolem0012(X20)))|(gt(X20,X23)|conditionnormo(X23))))&(((((~bsecretioni(skolem0011(X20))|~bcapacitysn(X20))|~qilt27(X20))|gt(X20,skolem0012(X20)))|(gt(X20,X23)|conditionnormo(X23)))&((((~bsecretioni(skolem0011(X20))|~bcapacitysn(X20))|~qilt27(X20))|~conditionhyper(skolem0012(X20)))|(gt(X20,X23)|conditionnormo(X23))))))),inference(distribute,[status(thm)],[c62])).
% 5.45/5.64 cnf(c65,plain,~gt(X241,skolem0011(X241))|~bcapacitysn(X241)|~qilt27(X241)|~conditionhyper(skolem0012(X241))|gt(X241,X242)|conditionnormo(X242),inference(split_conjunct,[status(thm)],[c63])).
% 5.45/5.64 fof(xorcapacity4,axiom,(![X0]:((~bcapacityex(X0))|(~bcapacitysn(X0)))),file('/export/starexec/sandbox/benchmark/Axioms/MED001+0.ax', xorcapacity4)).
% 5.45/5.64 fof(c109,plain,(![X0]:(~bcapacityex(X0)|~bcapacitysn(X0))),inference(fof_simplification,[status(thm)],[xorcapacity4])).
% 5.45/5.64 fof(c110,plain,(![X39]:(~bcapacityex(X39)|~bcapacitysn(X39))),inference(variable_rename,[status(thm)],[c109])).
% 5.45/5.64 cnf(c111,plain,~bcapacityex(X53)|~bcapacitysn(X53),inference(split_conjunct,[status(thm)],[c110])).
% 5.45/5.64 cnf(c129,plain,~bcapacityex(n0),inference(resolution,[status(thm)],[c111, c8])).
% 5.45/5.64 fof(sulfonylurea_effect,axiom,(![X0]:(((![X1]:((~gt(X0,X1))=>drugsu(X1)))&(~bcapacityex(X0)))=>(![X1]:((~gt(X0,X1))=>bsecretioni(X1))))),file('/export/starexec/sandbox/benchmark/Axioms/MED001+0.ax', sulfonylurea_effect)).
% 5.45/5.64 fof(c76,plain,(![X0]:(((![X1]:(~gt(X0,X1)=>drugsu(X1)))&~bcapacityex(X0))=>(![X1]:(~gt(X0,X1)=>bsecretioni(X1))))),inference(fof_simplification,[status(thm)],[sulfonylurea_effect])).
% 5.45/5.64 fof(c77,plain,(![X0]:(((?[X1]:(~gt(X0,X1)&~drugsu(X1)))|bcapacityex(X0))|(![X1]:(gt(X0,X1)|bsecretioni(X1))))),inference(fof_nnf,[status(thm)],[c76])).
% 5.45/5.64 fof(c78,plain,(![X27]:(((?[X28]:(~gt(X27,X28)&~drugsu(X28)))|bcapacityex(X27))|(![X29]:(gt(X27,X29)|bsecretioni(X29))))),inference(variable_rename,[status(thm)],[c77])).
% 5.45/5.64 fof(c80,plain,(![X27]:(![X29]:(((~gt(X27,skolem0014(X27))&~drugsu(skolem0014(X27)))|bcapacityex(X27))|(gt(X27,X29)|bsecretioni(X29))))),inference(shift_quantors,[status(thm)],[fof(c79,plain,(![X27]:(((~gt(X27,skolem0014(X27))&~drugsu(skolem0014(X27)))|bcapacityex(X27))|(![X29]:(gt(X27,X29)|bsecretioni(X29))))),inference(skolemize,[status(esa)],[c78])).])).
% 5.45/5.64 fof(c81,plain,(![X27]:(![X29]:(((~gt(X27,skolem0014(X27))|bcapacityex(X27))|(gt(X27,X29)|bsecretioni(X29)))&((~drugsu(skolem0014(X27))|bcapacityex(X27))|(gt(X27,X29)|bsecretioni(X29)))))),inference(distribute,[status(thm)],[c80])).
% 5.45/5.64 cnf(c82,plain,~gt(X123,skolem0014(X123))|bcapacityex(X123)|gt(X123,X122)|bsecretioni(X122),inference(split_conjunct,[status(thm)],[c81])).
% 5.45/5.64 cnf(c6,negated_conjecture,gt(n0,X48)|drugsu(X48),inference(split_conjunct,[status(thm)],[c5])).
% 5.45/5.64 cnf(c83,plain,~drugsu(skolem0014(X106))|bcapacityex(X106)|gt(X106,X105)|bsecretioni(X105),inference(split_conjunct,[status(thm)],[c81])).
% 5.45/5.64 cnf(c184,plain,bcapacityex(X125)|gt(X125,X126)|bsecretioni(X126)|gt(n0,skolem0014(X125)),inference(resolution,[status(thm)],[c83, c6])).
% 5.45/5.64 cnf(c261,plain,bcapacityex(n0)|gt(n0,X320)|bsecretioni(X320)|gt(n0,X321)|bsecretioni(X321),inference(resolution,[status(thm)],[c184, c82])).
% 5.45/5.64 cnf(c1108,plain,bcapacityex(n0)|gt(n0,X323)|bsecretioni(X323),inference(factor,[status(thm)],[c261])).
% 5.45/5.64 cnf(c1197,plain,gt(n0,X324)|bsecretioni(X324),inference(resolution,[status(thm)],[c1108, c129])).
% 5.45/5.64 cnf(c1248,plain,bsecretioni(skolem0011(n0))|~bcapacitysn(n0)|~qilt27(n0)|~conditionhyper(skolem0012(n0))|gt(n0,X1627)|conditionnormo(X1627),inference(resolution,[status(thm)],[c1197, c65])).
% 5.45/5.64 cnf(c7,negated_conjecture,~gt(n0,X52)|conditionhyper(X52),inference(split_conjunct,[status(thm)],[c5])).
% 5.45/5.64 cnf(c64,plain,~gt(X234,skolem0011(X234))|~bcapacitysn(X234)|~qilt27(X234)|gt(X234,skolem0012(X234))|gt(X234,X235)|conditionnormo(X235),inference(split_conjunct,[status(thm)],[c63])).
% 5.45/5.64 cnf(c66,plain,~bsecretioni(skolem0011(X249))|~bcapacitysn(X249)|~qilt27(X249)|gt(X249,skolem0012(X249))|gt(X249,X250)|conditionnormo(X250),inference(split_conjunct,[status(thm)],[c63])).
% 5.45/5.64 cnf(c1279,plain,gt(n0,skolem0011(X968))|~bcapacitysn(X968)|~qilt27(X968)|gt(X968,skolem0012(X968))|gt(X968,X967)|conditionnormo(X967),inference(resolution,[status(thm)],[c1197, c66])).
% 5.45/5.64 cnf(c2222,plain,gt(n0,skolem0011(n0))|~bcapacitysn(n0)|gt(n0,skolem0012(n0))|gt(n0,X1773)|conditionnormo(X1773),inference(resolution,[status(thm)],[c1279, c9])).
% 5.45/5.64 cnf(c9913,plain,gt(n0,skolem0011(n0))|gt(n0,skolem0012(n0))|gt(n0,X1774)|conditionnormo(X1774),inference(resolution,[status(thm)],[c2222, c8])).
% 5.45/5.64 cnf(c9966,plain,gt(n0,skolem0011(n0))|gt(n0,skolem0012(n0))|conditionnormo(skolem0001),inference(resolution,[status(thm)],[c9913, c10])).
% 5.45/5.64 cnf(c10122,plain,gt(n0,skolem0011(n0))|gt(n0,skolem0012(n0)),inference(resolution,[status(thm)],[c9966, c11])).
% 5.45/5.64 cnf(c10131,plain,gt(n0,skolem0012(n0))|~bcapacitysn(n0)|~qilt27(n0)|gt(n0,X1804)|conditionnormo(X1804),inference(resolution,[status(thm)],[c10122, c64])).
% 5.45/5.64 cnf(c10285,plain,gt(n0,skolem0012(n0))|~bcapacitysn(n0)|gt(n0,X1805)|conditionnormo(X1805),inference(resolution,[status(thm)],[c10131, c9])).
% 5.45/5.64 cnf(c10309,plain,gt(n0,skolem0012(n0))|gt(n0,X1806)|conditionnormo(X1806),inference(resolution,[status(thm)],[c10285, c8])).
% 5.45/5.64 cnf(c10348,plain,gt(n0,skolem0012(n0))|conditionnormo(skolem0001),inference(resolution,[status(thm)],[c10309, c10])).
% 5.45/5.64 cnf(c10456,plain,gt(n0,skolem0012(n0)),inference(resolution,[status(thm)],[c10348, c11])).
% 5.45/5.64 cnf(c10462,plain,conditionhyper(skolem0012(n0)),inference(resolution,[status(thm)],[c10456, c7])).
% 5.45/5.64 cnf(c10477,plain,bsecretioni(skolem0011(n0))|~bcapacitysn(n0)|~qilt27(n0)|gt(n0,X1836)|conditionnormo(X1836),inference(resolution,[status(thm)],[c10462, c1248])).
% 5.45/5.64 cnf(c10519,plain,bsecretioni(skolem0011(n0))|~bcapacitysn(n0)|gt(n0,X1837)|conditionnormo(X1837),inference(resolution,[status(thm)],[c10477, c9])).
% 5.45/5.64 cnf(c10543,plain,bsecretioni(skolem0011(n0))|gt(n0,X1838)|conditionnormo(X1838),inference(resolution,[status(thm)],[c10519, c8])).
% 5.45/5.64 cnf(c10574,plain,bsecretioni(skolem0011(n0))|conditionnormo(skolem0001),inference(resolution,[status(thm)],[c10543, c10])).
% 5.45/5.64 cnf(c10640,plain,bsecretioni(skolem0011(n0)),inference(resolution,[status(thm)],[c10574, c11])).
% 5.45/5.64 cnf(c67,plain,~bsecretioni(skolem0011(X254))|~bcapacitysn(X254)|~qilt27(X254)|~conditionhyper(skolem0012(X254))|gt(X254,X255)|conditionnormo(X255),inference(split_conjunct,[status(thm)],[c63])).
% 5.45/5.64 cnf(c10479,plain,~bsecretioni(skolem0011(n0))|~bcapacitysn(n0)|~qilt27(n0)|gt(n0,X1872)|conditionnormo(X1872),inference(resolution,[status(thm)],[c10462, c67])).
% 5.45/5.64 cnf(c10775,plain,~bcapacitysn(n0)|~qilt27(n0)|gt(n0,X1873)|conditionnormo(X1873),inference(resolution,[status(thm)],[c10479, c10640])).
% 5.45/5.64 cnf(c10790,plain,~bcapacitysn(n0)|gt(n0,X1875)|conditionnormo(X1875),inference(resolution,[status(thm)],[c10775, c9])).
% 5.45/5.64 cnf(c10814,plain,gt(n0,X1876)|conditionnormo(X1876),inference(resolution,[status(thm)],[c10790, c8])).
% 5.45/5.64 cnf(c10841,plain,conditionnormo(skolem0001),inference(resolution,[status(thm)],[c10814, c10])).
% 5.45/5.64 cnf(c10899,plain,$false,inference(resolution,[status(thm)],[c10841, c11])).
% 5.45/5.64 % SZS output end CNFRefutation
% 5.45/5.64
% 5.45/5.64 % Initial clauses : 57
% 5.45/5.64 % Processed clauses : 495
% 5.45/5.64 % Factors computed : 38
% 5.45/5.64 % Resolvents computed: 10737
% 5.45/5.64 % Tautologies deleted: 99
% 5.45/5.64 % Forward subsumed : 1126
% 5.45/5.64 % Backward subsumed : 132
% 5.45/5.64 % -------- CPU Time ---------
% 5.45/5.64 % User time : 5.237 s
% 5.45/5.64 % System time : 0.041 s
% 5.45/5.64 % Total time : 5.278 s
%------------------------------------------------------------------------------