%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS132+1 : TPTP v8.1.2. Released v3.1.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 : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:28:47 EDT 2024
% Result : Theorem 0.63s 0.80s
% Output : Refutation 0.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : KRS132+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n028.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 00:11:38 EDT 2024
% 0.13/0.36 % CPUTime :
% 0.63/0.80 % Version: 1.5
% 0.63/0.80 % SZS status Theorem
% 0.63/0.80 % SZS output start CNFRefutation
% 0.63/0.80 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_0)).
% 0.63/0.80 fof(c90,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.63/0.80 fof(c91,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c90])).
% 0.63/0.80 fof(c93,plain,(![X38]:(![X39]:(cowlThing(X38)&~cowlNothing(X39)))),inference(shift_quantors,[status(thm)],[fof(c92,plain,((![X38]:cowlThing(X38))&(![X39]:~cowlNothing(X39))),inference(variable_rename,[status(thm)],[c91])).])).
% 0.63/0.80 cnf(c95,plain,~cowlNothing(X41),inference(split_conjunct,[status(thm)],[c93])).
% 0.63/0.80 cnf(c94,plain,cowlThing(X40),inference(split_conjunct,[status(thm)],[c93])).
% 0.63/0.80 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_1)).
% 0.63/0.80 fof(c83,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.63/0.80 fof(c84,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c83])).
% 0.63/0.80 fof(c85,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c84])).
% 0.63/0.80 fof(c87,plain,(![X36]:(![X37]:((~xsd_string(X36)|~xsd_integer(X36))&(xsd_integer(X37)|xsd_string(X37))))),inference(shift_quantors,[status(thm)],[fof(c86,plain,((![X36]:(~xsd_string(X36)|~xsd_integer(X36)))&(![X37]:(xsd_integer(X37)|xsd_string(X37)))),inference(variable_rename,[status(thm)],[c85])).])).
% 0.63/0.80 cnf(c89,plain,xsd_integer(X45)|xsd_string(X45),inference(split_conjunct,[status(thm)],[c87])).
% 0.63/0.80 fof(axiom_9,axiom,(![X]:(cnotAorB(X)<=>(cnotB(X)&cnotA(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_9)).
% 0.63/0.80 fof(c22,plain,(![X]:((~cnotAorB(X)|(cnotB(X)&cnotA(X)))&((~cnotB(X)|~cnotA(X))|cnotAorB(X)))),inference(fof_nnf,[status(thm)],[axiom_9])).
% 0.63/0.80 fof(c23,plain,((![X]:(~cnotAorB(X)|(cnotB(X)&cnotA(X))))&(![X]:((~cnotB(X)|~cnotA(X))|cnotAorB(X)))),inference(shift_quantors,[status(thm)],[c22])).
% 0.63/0.80 fof(c25,plain,(![X10]:(![X11]:((~cnotAorB(X10)|(cnotB(X10)&cnotA(X10)))&((~cnotB(X11)|~cnotA(X11))|cnotAorB(X11))))),inference(shift_quantors,[status(thm)],[fof(c24,plain,((![X10]:(~cnotAorB(X10)|(cnotB(X10)&cnotA(X10))))&(![X11]:((~cnotB(X11)|~cnotA(X11))|cnotAorB(X11)))),inference(variable_rename,[status(thm)],[c23])).])).
% 0.63/0.80 fof(c26,plain,(![X10]:(![X11]:(((~cnotAorB(X10)|cnotB(X10))&(~cnotAorB(X10)|cnotA(X10)))&((~cnotB(X11)|~cnotA(X11))|cnotAorB(X11))))),inference(distribute,[status(thm)],[c25])).
% 0.63/0.80 cnf(c28,plain,~cnotAorB(X43)|cnotA(X43),inference(split_conjunct,[status(thm)],[c26])).
% 0.63/0.80 fof(axiom_8,axiom,(![X]:(cnotAorB(X)<=>(![Y]:(rs(X,Y)=>cNothing(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_8)).
% 0.63/0.80 fof(c30,plain,(![X]:((~cnotAorB(X)|(![Y]:(~rs(X,Y)|cNothing(Y))))&((?[Y]:(rs(X,Y)&~cNothing(Y)))|cnotAorB(X)))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.63/0.80 fof(c31,plain,((![X]:(~cnotAorB(X)|(![Y]:(~rs(X,Y)|cNothing(Y)))))&(![X]:((?[Y]:(rs(X,Y)&~cNothing(Y)))|cnotAorB(X)))),inference(shift_quantors,[status(thm)],[c30])).
% 0.63/0.80 fof(c32,plain,((![X12]:(~cnotAorB(X12)|(![X13]:(~rs(X12,X13)|cNothing(X13)))))&(![X14]:((?[X15]:(rs(X14,X15)&~cNothing(X15)))|cnotAorB(X14)))),inference(variable_rename,[status(thm)],[c31])).
% 0.63/0.80 fof(c34,plain,(![X12]:(![X13]:(![X14]:((~cnotAorB(X12)|(~rs(X12,X13)|cNothing(X13)))&((rs(X14,skolem0006(X14))&~cNothing(skolem0006(X14)))|cnotAorB(X14)))))),inference(shift_quantors,[status(thm)],[fof(c33,plain,((![X12]:(~cnotAorB(X12)|(![X13]:(~rs(X12,X13)|cNothing(X13)))))&(![X14]:((rs(X14,skolem0006(X14))&~cNothing(skolem0006(X14)))|cnotAorB(X14)))),inference(skolemize,[status(esa)],[c32])).])).
% 0.63/0.80 fof(c35,plain,(![X12]:(![X13]:(![X14]:((~cnotAorB(X12)|(~rs(X12,X13)|cNothing(X13)))&((rs(X14,skolem0006(X14))|cnotAorB(X14))&(~cNothing(skolem0006(X14))|cnotAorB(X14))))))),inference(distribute,[status(thm)],[c34])).
% 0.63/0.80 cnf(c37,plain,rs(X57,skolem0006(X57))|cnotAorB(X57),inference(split_conjunct,[status(thm)],[c35])).
% 0.63/0.80 cnf(c99,plain,rs(X64,skolem0006(X64))|cnotA(X64),inference(resolution,[status(thm)],[c37, c28])).
% 0.63/0.80 fof(axiom_3,axiom,(![X]:(cAorB(X)<=>(?[Y]:(rs(X,Y)&cowlThing(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.63/0.80 fof(c65,plain,(![X]:((~cAorB(X)|(?[Y]:(rs(X,Y)&cowlThing(Y))))&((![Y]:(~rs(X,Y)|~cowlThing(Y)))|cAorB(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.63/0.80 fof(c66,plain,((![X]:(~cAorB(X)|(?[Y]:(rs(X,Y)&cowlThing(Y)))))&(![X]:((![Y]:(~rs(X,Y)|~cowlThing(Y)))|cAorB(X)))),inference(shift_quantors,[status(thm)],[c65])).
% 0.63/0.80 fof(c67,plain,((![X28]:(~cAorB(X28)|(?[X29]:(rs(X28,X29)&cowlThing(X29)))))&(![X30]:((![X31]:(~rs(X30,X31)|~cowlThing(X31)))|cAorB(X30)))),inference(variable_rename,[status(thm)],[c66])).
% 0.63/0.80 fof(c69,plain,(![X28]:(![X30]:(![X31]:((~cAorB(X28)|(rs(X28,skolem0010(X28))&cowlThing(skolem0010(X28))))&((~rs(X30,X31)|~cowlThing(X31))|cAorB(X30)))))),inference(shift_quantors,[status(thm)],[fof(c68,plain,((![X28]:(~cAorB(X28)|(rs(X28,skolem0010(X28))&cowlThing(skolem0010(X28)))))&(![X30]:((![X31]:(~rs(X30,X31)|~cowlThing(X31)))|cAorB(X30)))),inference(skolemize,[status(esa)],[c67])).])).
% 0.63/0.80 fof(c70,plain,(![X28]:(![X30]:(![X31]:(((~cAorB(X28)|rs(X28,skolem0010(X28)))&(~cAorB(X28)|cowlThing(skolem0010(X28))))&((~rs(X30,X31)|~cowlThing(X31))|cAorB(X30)))))),inference(distribute,[status(thm)],[c69])).
% 0.63/0.80 cnf(c73,plain,~rs(X73,X74)|~cowlThing(X74)|cAorB(X73),inference(split_conjunct,[status(thm)],[c70])).
% 0.63/0.80 cnf(c108,plain,~cowlThing(skolem0006(X85))|cAorB(X85)|cnotA(X85),inference(resolution,[status(thm)],[c73, c99])).
% 0.63/0.80 cnf(c120,plain,cAorB(X86)|cnotA(X86),inference(resolution,[status(thm)],[c108, c94])).
% 0.63/0.80 fof(the_axiom,conjecture,(((![X]:(cowlThing(X)&(~cowlNothing(X))))&(![X]:(xsd_string(X)<=>(~xsd_integer(X)))))&(![X]:(cAorB(X)<=>(cB(X)|cA(X))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', the_axiom)).
% 0.63/0.80 fof(c0,negated_conjecture,(~(((![X]:(cowlThing(X)&(~cowlNothing(X))))&(![X]:(xsd_string(X)<=>(~xsd_integer(X)))))&(![X]:(cAorB(X)<=>(cB(X)|cA(X)))))),inference(assume_negation,[status(cth)],[the_axiom])).
% 0.63/0.80 fof(c1,negated_conjecture,(~(((![X]:(cowlThing(X)&~cowlNothing(X)))&(![X]:(xsd_string(X)<=>~xsd_integer(X))))&(![X]:(cAorB(X)<=>(cB(X)|cA(X)))))),inference(fof_simplification,[status(thm)],[c0])).
% 0.63/0.80 fof(c2,negated_conjecture,(((?[X]:(~cowlThing(X)|cowlNothing(X)))|(?[X]:((~xsd_string(X)|xsd_integer(X))&(xsd_string(X)|~xsd_integer(X)))))|(?[X]:((~cAorB(X)|(~cB(X)&~cA(X)))&(cAorB(X)|(cB(X)|cA(X)))))),inference(fof_nnf,[status(thm)],[c1])).
% 0.63/0.80 fof(c3,negated_conjecture,((((?[X]:~cowlThing(X))|(?[X]:cowlNothing(X)))|(?[X]:((~xsd_string(X)|xsd_integer(X))&(xsd_string(X)|~xsd_integer(X)))))|(?[X]:((~cAorB(X)|(~cB(X)&~cA(X)))&(cAorB(X)|(cB(X)|cA(X)))))),inference(shift_quantors,[status(thm)],[c2])).
% 0.63/0.80 fof(c4,negated_conjecture,((((?[X2]:~cowlThing(X2))|(?[X3]:cowlNothing(X3)))|(?[X4]:((~xsd_string(X4)|xsd_integer(X4))&(xsd_string(X4)|~xsd_integer(X4)))))|(?[X5]:((~cAorB(X5)|(~cB(X5)&~cA(X5)))&(cAorB(X5)|(cB(X5)|cA(X5)))))),inference(variable_rename,[status(thm)],[c3])).
% 0.63/0.80 fof(c5,negated_conjecture,(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|((~xsd_string(skolem0003)|xsd_integer(skolem0003))&(xsd_string(skolem0003)|~xsd_integer(skolem0003))))|((~cAorB(skolem0004)|(~cB(skolem0004)&~cA(skolem0004)))&(cAorB(skolem0004)|(cB(skolem0004)|cA(skolem0004))))),inference(skolemize,[status(esa)],[c4])).
% 0.63/0.80 fof(c6,negated_conjecture,((((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|(~cAorB(skolem0004)|~cB(skolem0004)))&(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|(~cAorB(skolem0004)|~cA(skolem0004))))&(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|(cAorB(skolem0004)|(cB(skolem0004)|cA(skolem0004)))))&(((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|(~cAorB(skolem0004)|~cB(skolem0004)))&(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|(~cAorB(skolem0004)|~cA(skolem0004))))&(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|(cAorB(skolem0004)|(cB(skolem0004)|cA(skolem0004)))))),inference(distribute,[status(thm)],[c5])).
% 0.63/0.81 cnf(c11,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cAorB(skolem0004)|~cA(skolem0004),inference(split_conjunct,[status(thm)],[c6])).
% 0.63/0.81 fof(axiom_7,axiom,(![X]:(cnotA(X)<=>(![Y]:(rq(X,Y)=>cNothing(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_7)).
% 0.63/0.81 fof(c39,plain,(![X]:((~cnotA(X)|(![Y]:(~rq(X,Y)|cNothing(Y))))&((?[Y]:(rq(X,Y)&~cNothing(Y)))|cnotA(X)))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.63/0.81 fof(c40,plain,((![X]:(~cnotA(X)|(![Y]:(~rq(X,Y)|cNothing(Y)))))&(![X]:((?[Y]:(rq(X,Y)&~cNothing(Y)))|cnotA(X)))),inference(shift_quantors,[status(thm)],[c39])).
% 0.63/0.81 fof(c41,plain,((![X16]:(~cnotA(X16)|(![X17]:(~rq(X16,X17)|cNothing(X17)))))&(![X18]:((?[X19]:(rq(X18,X19)&~cNothing(X19)))|cnotA(X18)))),inference(variable_rename,[status(thm)],[c40])).
% 0.63/0.81 fof(c43,plain,(![X16]:(![X17]:(![X18]:((~cnotA(X16)|(~rq(X16,X17)|cNothing(X17)))&((rq(X18,skolem0007(X18))&~cNothing(skolem0007(X18)))|cnotA(X18)))))),inference(shift_quantors,[status(thm)],[fof(c42,plain,((![X16]:(~cnotA(X16)|(![X17]:(~rq(X16,X17)|cNothing(X17)))))&(![X18]:((rq(X18,skolem0007(X18))&~cNothing(skolem0007(X18)))|cnotA(X18)))),inference(skolemize,[status(esa)],[c41])).])).
% 0.63/0.81 fof(c44,plain,(![X16]:(![X17]:(![X18]:((~cnotA(X16)|(~rq(X16,X17)|cNothing(X17)))&((rq(X18,skolem0007(X18))|cnotA(X18))&(~cNothing(skolem0007(X18))|cnotA(X18))))))),inference(distribute,[status(thm)],[c43])).
% 0.63/0.81 cnf(c46,plain,rq(X58,skolem0007(X58))|cnotA(X58),inference(split_conjunct,[status(thm)],[c44])).
% 0.63/0.81 fof(axiom_2,axiom,(![X]:(cA(X)<=>(?[Y]:(rq(X,Y)&cowlThing(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.63/0.81 fof(c74,plain,(![X]:((~cA(X)|(?[Y]:(rq(X,Y)&cowlThing(Y))))&((![Y]:(~rq(X,Y)|~cowlThing(Y)))|cA(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.63/0.81 fof(c75,plain,((![X]:(~cA(X)|(?[Y]:(rq(X,Y)&cowlThing(Y)))))&(![X]:((![Y]:(~rq(X,Y)|~cowlThing(Y)))|cA(X)))),inference(shift_quantors,[status(thm)],[c74])).
% 0.63/0.81 fof(c76,plain,((![X32]:(~cA(X32)|(?[X33]:(rq(X32,X33)&cowlThing(X33)))))&(![X34]:((![X35]:(~rq(X34,X35)|~cowlThing(X35)))|cA(X34)))),inference(variable_rename,[status(thm)],[c75])).
% 0.63/0.81 fof(c78,plain,(![X32]:(![X34]:(![X35]:((~cA(X32)|(rq(X32,skolem0011(X32))&cowlThing(skolem0011(X32))))&((~rq(X34,X35)|~cowlThing(X35))|cA(X34)))))),inference(shift_quantors,[status(thm)],[fof(c77,plain,((![X32]:(~cA(X32)|(rq(X32,skolem0011(X32))&cowlThing(skolem0011(X32)))))&(![X34]:((![X35]:(~rq(X34,X35)|~cowlThing(X35)))|cA(X34)))),inference(skolemize,[status(esa)],[c76])).])).
% 0.63/0.81 fof(c79,plain,(![X32]:(![X34]:(![X35]:(((~cA(X32)|rq(X32,skolem0011(X32)))&(~cA(X32)|cowlThing(skolem0011(X32))))&((~rq(X34,X35)|~cowlThing(X35))|cA(X34)))))),inference(distribute,[status(thm)],[c78])).
% 0.63/0.81 cnf(c82,plain,~rq(X75,X76)|~cowlThing(X76)|cA(X75),inference(split_conjunct,[status(thm)],[c79])).
% 0.63/0.81 cnf(c111,plain,~cowlThing(skolem0007(X104))|cA(X104)|cnotA(X104),inference(resolution,[status(thm)],[c82, c46])).
% 0.63/0.81 cnf(c154,plain,cA(X105)|cnotA(X105),inference(resolution,[status(thm)],[c111, c94])).
% 0.63/0.81 cnf(c157,plain,cnotA(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cAorB(skolem0004),inference(resolution,[status(thm)],[c154, c11])).
% 0.63/0.81 cnf(c265,plain,cnotA(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003),inference(resolution,[status(thm)],[c157, c120])).
% 0.63/0.81 cnf(c625,plain,cnotA(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c265, c89])).
% 0.63/0.81 cnf(c626,plain,cnotA(skolem0004)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c625, c94])).
% 0.63/0.81 cnf(c636,plain,cnotA(skolem0004)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c626, c95])).
% 0.63/0.81 cnf(c88,plain,~xsd_string(X44)|~xsd_integer(X44),inference(split_conjunct,[status(thm)],[c87])).
% 0.63/0.81 cnf(c8,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|~cAorB(skolem0004)|~cA(skolem0004),inference(split_conjunct,[status(thm)],[c6])).
% 0.63/0.81 cnf(c158,plain,cnotA(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|~cAorB(skolem0004),inference(resolution,[status(thm)],[c154, c8])).
% 0.63/0.81 cnf(c276,plain,cnotA(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c158, c120])).
% 0.63/0.81 cnf(c656,plain,cnotA(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c276, c89])).
% 0.63/0.81 cnf(c658,plain,cnotA(skolem0004)|cowlNothing(skolem0002)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c656, c94])).
% 0.63/0.81 cnf(c668,plain,cnotA(skolem0004)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c658, c95])).
% 0.63/0.81 cnf(c679,plain,cnotA(skolem0004)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c668, c88])).
% 0.63/0.81 cnf(c682,plain,cnotA(skolem0004),inference(resolution,[status(thm)],[c679, c636])).
% 0.63/0.81 cnf(c45,plain,~cnotA(X70)|~rq(X70,X69)|cNothing(X69),inference(split_conjunct,[status(thm)],[c44])).
% 0.63/0.81 cnf(c80,plain,~cA(X62)|rq(X62,skolem0011(X62)),inference(split_conjunct,[status(thm)],[c79])).
% 0.63/0.81 cnf(c27,plain,~cnotAorB(X42)|cnotB(X42),inference(split_conjunct,[status(thm)],[c26])).
% 0.63/0.81 cnf(c98,plain,rs(X63,skolem0006(X63))|cnotB(X63),inference(resolution,[status(thm)],[c37, c27])).
% 0.63/0.81 cnf(c109,plain,~cowlThing(skolem0006(X94))|cAorB(X94)|cnotB(X94),inference(resolution,[status(thm)],[c73, c98])).
% 0.63/0.81 cnf(c140,plain,cAorB(X95)|cnotB(X95),inference(resolution,[status(thm)],[c109, c94])).
% 0.63/0.81 cnf(c7,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|~cAorB(skolem0004)|~cB(skolem0004),inference(split_conjunct,[status(thm)],[c6])).
% 0.63/0.81 fof(axiom_10,axiom,(![X]:(cnotB(X)<=>(![Y]:(rr(X,Y)=>cNothing(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_10)).
% 0.63/0.81 fof(c13,plain,(![X]:((~cnotB(X)|(![Y]:(~rr(X,Y)|cNothing(Y))))&((?[Y]:(rr(X,Y)&~cNothing(Y)))|cnotB(X)))),inference(fof_nnf,[status(thm)],[axiom_10])).
% 0.63/0.81 fof(c14,plain,((![X]:(~cnotB(X)|(![Y]:(~rr(X,Y)|cNothing(Y)))))&(![X]:((?[Y]:(rr(X,Y)&~cNothing(Y)))|cnotB(X)))),inference(shift_quantors,[status(thm)],[c13])).
% 0.63/0.81 fof(c15,plain,((![X6]:(~cnotB(X6)|(![X7]:(~rr(X6,X7)|cNothing(X7)))))&(![X8]:((?[X9]:(rr(X8,X9)&~cNothing(X9)))|cnotB(X8)))),inference(variable_rename,[status(thm)],[c14])).
% 0.63/0.81 fof(c17,plain,(![X6]:(![X7]:(![X8]:((~cnotB(X6)|(~rr(X6,X7)|cNothing(X7)))&((rr(X8,skolem0005(X8))&~cNothing(skolem0005(X8)))|cnotB(X8)))))),inference(shift_quantors,[status(thm)],[fof(c16,plain,((![X6]:(~cnotB(X6)|(![X7]:(~rr(X6,X7)|cNothing(X7)))))&(![X8]:((rr(X8,skolem0005(X8))&~cNothing(skolem0005(X8)))|cnotB(X8)))),inference(skolemize,[status(esa)],[c15])).])).
% 0.63/0.81 fof(c18,plain,(![X6]:(![X7]:(![X8]:((~cnotB(X6)|(~rr(X6,X7)|cNothing(X7)))&((rr(X8,skolem0005(X8))|cnotB(X8))&(~cNothing(skolem0005(X8))|cnotB(X8))))))),inference(distribute,[status(thm)],[c17])).
% 0.63/0.81 cnf(c20,plain,rr(X55,skolem0005(X55))|cnotB(X55),inference(split_conjunct,[status(thm)],[c18])).
% 0.63/0.81 fof(axiom_4,axiom,(![X]:(cB(X)<=>(?[Y]:(rr(X,Y)&cowlThing(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.63/0.81 fof(c56,plain,(![X]:((~cB(X)|(?[Y]:(rr(X,Y)&cowlThing(Y))))&((![Y]:(~rr(X,Y)|~cowlThing(Y)))|cB(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.63/0.81 fof(c57,plain,((![X]:(~cB(X)|(?[Y]:(rr(X,Y)&cowlThing(Y)))))&(![X]:((![Y]:(~rr(X,Y)|~cowlThing(Y)))|cB(X)))),inference(shift_quantors,[status(thm)],[c56])).
% 0.63/0.81 fof(c58,plain,((![X24]:(~cB(X24)|(?[X25]:(rr(X24,X25)&cowlThing(X25)))))&(![X26]:((![X27]:(~rr(X26,X27)|~cowlThing(X27)))|cB(X26)))),inference(variable_rename,[status(thm)],[c57])).
% 0.63/0.81 fof(c60,plain,(![X24]:(![X26]:(![X27]:((~cB(X24)|(rr(X24,skolem0009(X24))&cowlThing(skolem0009(X24))))&((~rr(X26,X27)|~cowlThing(X27))|cB(X26)))))),inference(shift_quantors,[status(thm)],[fof(c59,plain,((![X24]:(~cB(X24)|(rr(X24,skolem0009(X24))&cowlThing(skolem0009(X24)))))&(![X26]:((![X27]:(~rr(X26,X27)|~cowlThing(X27)))|cB(X26)))),inference(skolemize,[status(esa)],[c58])).])).
% 0.63/0.81 fof(c61,plain,(![X24]:(![X26]:(![X27]:(((~cB(X24)|rr(X24,skolem0009(X24)))&(~cB(X24)|cowlThing(skolem0009(X24))))&((~rr(X26,X27)|~cowlThing(X27))|cB(X26)))))),inference(distribute,[status(thm)],[c60])).
% 0.63/0.81 cnf(c64,plain,~rr(X71,X72)|~cowlThing(X72)|cB(X71),inference(split_conjunct,[status(thm)],[c61])).
% 0.63/0.81 cnf(c107,plain,~cowlThing(skolem0005(X82))|cB(X82)|cnotB(X82),inference(resolution,[status(thm)],[c64, c20])).
% 0.63/0.81 cnf(c114,plain,cB(X83)|cnotB(X83),inference(resolution,[status(thm)],[c107, c94])).
% 0.63/0.81 cnf(c115,plain,cnotB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|~cAorB(skolem0004),inference(resolution,[status(thm)],[c114, c7])).
% 0.63/0.81 cnf(c186,plain,cnotB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c115, c140])).
% 0.63/0.81 cnf(c491,plain,cnotB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c186, c89])).
% 0.63/0.81 cnf(c492,plain,cnotB(skolem0004)|cowlNothing(skolem0002)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c491, c94])).
% 0.63/0.81 cnf(c496,plain,cnotB(skolem0004)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c492, c95])).
% 0.63/0.81 cnf(c501,plain,cnotB(skolem0004)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c496, c88])).
% 0.63/0.81 cnf(c10,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cAorB(skolem0004)|~cB(skolem0004),inference(split_conjunct,[status(thm)],[c6])).
% 0.63/0.81 cnf(c116,plain,cnotB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cAorB(skolem0004),inference(resolution,[status(thm)],[c114, c10])).
% 0.63/0.81 cnf(c190,plain,cnotB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003),inference(resolution,[status(thm)],[c116, c140])).
% 0.63/0.81 cnf(c525,plain,cnotB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c190, c496])).
% 0.63/0.81 cnf(c527,plain,cnotB(skolem0004)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c525, c94])).
% 0.63/0.81 cnf(c531,plain,cnotB(skolem0004)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c527, c95])).
% 0.63/0.81 cnf(c542,plain,cnotB(skolem0004),inference(resolution,[status(thm)],[c531, c501])).
% 0.63/0.81 cnf(c19,plain,~cnotB(X65)|~rr(X65,X66)|cNothing(X66),inference(split_conjunct,[status(thm)],[c18])).
% 0.63/0.81 cnf(c62,plain,~cB(X60)|rr(X60,skolem0009(X60)),inference(split_conjunct,[status(thm)],[c61])).
% 0.63/0.81 cnf(c29,plain,~cnotB(X56)|~cnotA(X56)|cnotAorB(X56),inference(split_conjunct,[status(thm)],[c26])).
% 0.63/0.81 cnf(c159,plain,cA(X107)|~cnotB(X107)|cnotAorB(X107),inference(resolution,[status(thm)],[c154, c29])).
% 0.63/0.81 cnf(c168,plain,cA(X109)|cnotAorB(X109)|cB(X109),inference(resolution,[status(thm)],[c159, c114])).
% 0.63/0.81 cnf(c36,plain,~cnotAorB(X67)|~rs(X67,X68)|cNothing(X68),inference(split_conjunct,[status(thm)],[c35])).
% 0.63/0.81 cnf(c71,plain,~cAorB(X61)|rs(X61,skolem0010(X61)),inference(split_conjunct,[status(thm)],[c70])).
% 0.63/0.81 cnf(c12,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|cAorB(skolem0004)|cB(skolem0004)|cA(skolem0004),inference(split_conjunct,[status(thm)],[c6])).
% 0.63/0.81 cnf(c112,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|cAorB(skolem0004)|cB(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c12, c89])).
% 0.63/0.81 cnf(c155,plain,cowlNothing(skolem0002)|xsd_string(skolem0003)|cAorB(skolem0004)|cB(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c112, c94])).
% 0.63/0.81 cnf(c252,plain,xsd_string(skolem0003)|cAorB(skolem0004)|cB(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c155, c95])).
% 0.63/0.81 cnf(c9,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|cAorB(skolem0004)|cB(skolem0004)|cA(skolem0004),inference(split_conjunct,[status(thm)],[c6])).
% 0.63/0.81 cnf(c97,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_integer(skolem0003)|cAorB(skolem0004)|cB(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c9, c89])).
% 0.63/0.81 cnf(c113,plain,cowlNothing(skolem0002)|xsd_integer(skolem0003)|cAorB(skolem0004)|cB(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c97, c94])).
% 0.63/0.81 cnf(c177,plain,xsd_integer(skolem0003)|cAorB(skolem0004)|cB(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c113, c95])).
% 0.63/0.81 cnf(c294,plain,cAorB(skolem0004)|cB(skolem0004)|cA(skolem0004)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c177, c88])).
% 0.63/0.81 cnf(c322,plain,cAorB(skolem0004)|cB(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c294, c252])).
% 0.63/0.81 cnf(c327,plain,cB(skolem0004)|cA(skolem0004)|rs(skolem0004,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c322, c71])).
% 0.63/0.81 cnf(c347,plain,cB(skolem0004)|cA(skolem0004)|~cnotAorB(skolem0004)|cNothing(skolem0010(skolem0004)),inference(resolution,[status(thm)],[c327, c36])).
% 0.63/0.81 cnf(c405,plain,cB(skolem0004)|cA(skolem0004)|cNothing(skolem0010(skolem0004)),inference(resolution,[status(thm)],[c347, c168])).
% 0.63/0.81 fof(axiom_6,axiom,(![X]:(cNothing(X)=>(~(?[Y]:rp(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 0.63/0.81 fof(c48,plain,(![X]:(~cNothing(X)|(![Y]:~rp(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.63/0.81 fof(c50,plain,(![X20]:(![X21]:(~cNothing(X20)|~rp(X20,X21)))),inference(shift_quantors,[status(thm)],[fof(c49,plain,(![X20]:(~cNothing(X20)|(![X21]:~rp(X20,X21)))),inference(variable_rename,[status(thm)],[c48])).])).
% 0.63/0.81 cnf(c51,plain,~cNothing(X47)|~rp(X47,X48),inference(split_conjunct,[status(thm)],[c50])).
% 0.63/0.81 fof(axiom_5,axiom,(![X]:(cNothing(X)=>(?[Y0]:rp(X,Y0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 0.63/0.81 fof(c52,plain,(![X]:(~cNothing(X)|(?[Y0]:rp(X,Y0)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.63/0.81 fof(c53,plain,(![X22]:(~cNothing(X22)|(?[X23]:rp(X22,X23)))),inference(variable_rename,[status(thm)],[c52])).
% 0.63/0.81 fof(c54,plain,(![X22]:(~cNothing(X22)|rp(X22,skolem0008(X22)))),inference(skolemize,[status(esa)],[c53])).
% 0.63/0.81 cnf(c55,plain,~cNothing(X59)|rp(X59,skolem0008(X59)),inference(split_conjunct,[status(thm)],[c54])).
% 0.63/0.81 cnf(c422,plain,cB(skolem0004)|cA(skolem0004)|rp(skolem0010(skolem0004),skolem0008(skolem0010(skolem0004))),inference(resolution,[status(thm)],[c405, c55])).
% 0.63/0.81 cnf(c726,plain,cB(skolem0004)|cA(skolem0004)|~cNothing(skolem0010(skolem0004)),inference(resolution,[status(thm)],[c422, c51])).
% 0.63/0.81 cnf(c727,plain,cB(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c726, c405])).
% 0.63/0.81 cnf(c732,plain,cA(skolem0004)|rr(skolem0004,skolem0009(skolem0004)),inference(resolution,[status(thm)],[c727, c62])).
% 0.63/0.81 cnf(c739,plain,cA(skolem0004)|~cnotB(skolem0004)|cNothing(skolem0009(skolem0004)),inference(resolution,[status(thm)],[c732, c19])).
% 0.63/0.81 cnf(c748,plain,cA(skolem0004)|cNothing(skolem0009(skolem0004)),inference(resolution,[status(thm)],[c739, c542])).
% 0.63/0.81 cnf(c756,plain,cA(skolem0004)|rp(skolem0009(skolem0004),skolem0008(skolem0009(skolem0004))),inference(resolution,[status(thm)],[c748, c55])).
% 0.63/0.81 cnf(c781,plain,cA(skolem0004)|~cNothing(skolem0009(skolem0004)),inference(resolution,[status(thm)],[c756, c51])).
% 0.63/0.81 cnf(c783,plain,cA(skolem0004),inference(resolution,[status(thm)],[c781, c748])).
% 0.63/0.81 cnf(c784,plain,rq(skolem0004,skolem0011(skolem0004)),inference(resolution,[status(thm)],[c783, c80])).
% 0.63/0.81 cnf(c788,plain,~cnotA(skolem0004)|cNothing(skolem0011(skolem0004)),inference(resolution,[status(thm)],[c784, c45])).
% 0.63/0.81 cnf(c791,plain,cNothing(skolem0011(skolem0004)),inference(resolution,[status(thm)],[c788, c682])).
% 0.63/0.81 cnf(c796,plain,rp(skolem0011(skolem0004),skolem0008(skolem0011(skolem0004))),inference(resolution,[status(thm)],[c791, c55])).
% 0.63/0.81 cnf(c797,plain,~cNothing(skolem0011(skolem0004)),inference(resolution,[status(thm)],[c796, c51])).
% 0.63/0.81 cnf(c798,plain,$false,inference(resolution,[status(thm)],[c797, c791])).
% 0.63/0.81 % SZS output end CNFRefutation
% 0.63/0.81
% 0.63/0.81 % Initial clauses : 33
% 0.63/0.81 % Processed clauses : 159
% 0.63/0.81 % Factors computed : 0
% 0.63/0.81 % Resolvents computed: 703
% 0.63/0.81 % Tautologies deleted: 22
% 0.63/0.81 % Forward subsumed : 260
% 0.63/0.81 % Backward subsumed : 93
% 0.63/0.81 % -------- CPU Time ---------
% 0.63/0.81 % User time : 0.440 s
% 0.63/0.81 % System time : 0.010 s
% 0.63/0.81 % Total time : 0.450 s
%------------------------------------------------------------------------------