%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS167+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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:51 EDT 2024
% Result : Theorem 0.71s 0.89s
% Output : Refutation 0.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : KRS167+1 : TPTP v8.1.2. Released v3.1.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n027.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 9 00:05:38 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.71/0.89 % Version: 1.5
% 0.71/0.89 % SZS status Theorem
% 0.71/0.89 % SZS output start CNFRefutation
% 0.71/0.89 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_1)).
% 0.71/0.89 fof(c40,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.71/0.89 fof(c41,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c40])).
% 0.71/0.89 fof(c42,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c41])).
% 0.71/0.89 fof(c44,plain,(![X22]:(![X23]:((~xsd_string(X22)|~xsd_integer(X22))&(xsd_integer(X23)|xsd_string(X23))))),inference(shift_quantors,[status(thm)],[fof(c43,plain,((![X22]:(~xsd_string(X22)|~xsd_integer(X22)))&(![X23]:(xsd_integer(X23)|xsd_string(X23)))),inference(variable_rename,[status(thm)],[c42])).])).
% 0.71/0.89 cnf(c45,plain,~xsd_string(X47)|~xsd_integer(X47),inference(split_conjunct,[status(thm)],[c44])).
% 0.71/0.89 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_0)).
% 0.71/0.89 fof(c47,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.71/0.89 fof(c48,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c47])).
% 0.71/0.89 fof(c50,plain,(![X24]:(![X25]:(cowlThing(X24)&~cowlNothing(X25)))),inference(shift_quantors,[status(thm)],[fof(c49,plain,((![X24]:cowlThing(X24))&(![X25]:~cowlNothing(X25))),inference(variable_rename,[status(thm)],[c48])).])).
% 0.71/0.89 cnf(c52,plain,~cowlNothing(X45),inference(split_conjunct,[status(thm)],[c50])).
% 0.71/0.89 cnf(c51,plain,cowlThing(X44),inference(split_conjunct,[status(thm)],[c50])).
% 0.71/0.89 cnf(c46,plain,xsd_integer(X48)|xsd_string(X48),inference(split_conjunct,[status(thm)],[c44])).
% 0.71/0.89 fof(axiom_3,axiom,(![X]:(cc2(X)<=>((?[Y0]:rp(X,Y0))&(![Y0]:(![Y1]:((rp(X,Y0)&rp(X,Y1))=>Y0=Y1)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.71/0.89 fof(c18,plain,(![X]:((~cc2(X)|((?[Y0]:rp(X,Y0))&(![Y0]:(![Y1]:((~rp(X,Y0)|~rp(X,Y1))|Y0=Y1)))))&(((![Y0]:~rp(X,Y0))|(?[Y0]:(?[Y1]:((rp(X,Y0)&rp(X,Y1))&Y0!=Y1))))|cc2(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.71/0.89 fof(c19,plain,((![X]:(~cc2(X)|((?[Y0]:rp(X,Y0))&(![Y0]:(![Y1]:((~rp(X,Y0)|~rp(X,Y1))|Y0=Y1))))))&(![X]:(((![Y0]:~rp(X,Y0))|(?[Y0]:(?[Y1]:((rp(X,Y0)&rp(X,Y1))&Y0!=Y1))))|cc2(X)))),inference(shift_quantors,[status(thm)],[c18])).
% 0.71/0.89 fof(c20,plain,((![X6]:(~cc2(X6)|((?[X7]:rp(X6,X7))&(![X8]:(![X9]:((~rp(X6,X8)|~rp(X6,X9))|X8=X9))))))&(![X10]:(((![X11]:~rp(X10,X11))|(?[X12]:(?[X13]:((rp(X10,X12)&rp(X10,X13))&X12!=X13))))|cc2(X10)))),inference(variable_rename,[status(thm)],[c19])).
% 0.71/0.89 fof(c22,plain,(![X6]:(![X8]:(![X9]:(![X10]:(![X11]:((~cc2(X6)|(rp(X6,skolem0005(X6))&((~rp(X6,X8)|~rp(X6,X9))|X8=X9)))&((~rp(X10,X11)|((rp(X10,skolem0006(X10))&rp(X10,skolem0007(X10)))&skolem0006(X10)!=skolem0007(X10)))|cc2(X10)))))))),inference(shift_quantors,[status(thm)],[fof(c21,plain,((![X6]:(~cc2(X6)|(rp(X6,skolem0005(X6))&(![X8]:(![X9]:((~rp(X6,X8)|~rp(X6,X9))|X8=X9))))))&(![X10]:(((![X11]:~rp(X10,X11))|((rp(X10,skolem0006(X10))&rp(X10,skolem0007(X10)))&skolem0006(X10)!=skolem0007(X10)))|cc2(X10)))),inference(skolemize,[status(esa)],[c20])).])).
% 0.71/0.89 fof(c23,plain,(![X6]:(![X8]:(![X9]:(![X10]:(![X11]:(((~cc2(X6)|rp(X6,skolem0005(X6)))&(~cc2(X6)|((~rp(X6,X8)|~rp(X6,X9))|X8=X9)))&((((~rp(X10,X11)|rp(X10,skolem0006(X10)))|cc2(X10))&((~rp(X10,X11)|rp(X10,skolem0007(X10)))|cc2(X10)))&((~rp(X10,X11)|skolem0006(X10)!=skolem0007(X10))|cc2(X10))))))))),inference(distribute,[status(thm)],[c22])).
% 0.71/0.89 cnf(c24,plain,~cc2(X53)|rp(X53,skolem0005(X53)),inference(split_conjunct,[status(thm)],[c23])).
% 0.71/0.89 cnf(c27,plain,~rp(X101,X102)|rp(X101,skolem0007(X101))|cc2(X101),inference(split_conjunct,[status(thm)],[c23])).
% 0.71/0.89 fof(axiom_2,axiom,(![X]:(cc1(X)<=>((?[Y0]:rp(X,Y0))&(![Y0]:(![Y1]:((rp(X,Y0)&rp(X,Y1))=>Y0=Y1)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.71/0.89 fof(c29,plain,(![X]:((~cc1(X)|((?[Y0]:rp(X,Y0))&(![Y0]:(![Y1]:((~rp(X,Y0)|~rp(X,Y1))|Y0=Y1)))))&(((![Y0]:~rp(X,Y0))|(?[Y0]:(?[Y1]:((rp(X,Y0)&rp(X,Y1))&Y0!=Y1))))|cc1(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.71/0.89 fof(c30,plain,((![X]:(~cc1(X)|((?[Y0]:rp(X,Y0))&(![Y0]:(![Y1]:((~rp(X,Y0)|~rp(X,Y1))|Y0=Y1))))))&(![X]:(((![Y0]:~rp(X,Y0))|(?[Y0]:(?[Y1]:((rp(X,Y0)&rp(X,Y1))&Y0!=Y1))))|cc1(X)))),inference(shift_quantors,[status(thm)],[c29])).
% 0.71/0.89 fof(c31,plain,((![X14]:(~cc1(X14)|((?[X15]:rp(X14,X15))&(![X16]:(![X17]:((~rp(X14,X16)|~rp(X14,X17))|X16=X17))))))&(![X18]:(((![X19]:~rp(X18,X19))|(?[X20]:(?[X21]:((rp(X18,X20)&rp(X18,X21))&X20!=X21))))|cc1(X18)))),inference(variable_rename,[status(thm)],[c30])).
% 0.71/0.89 fof(c33,plain,(![X14]:(![X16]:(![X17]:(![X18]:(![X19]:((~cc1(X14)|(rp(X14,skolem0008(X14))&((~rp(X14,X16)|~rp(X14,X17))|X16=X17)))&((~rp(X18,X19)|((rp(X18,skolem0009(X18))&rp(X18,skolem0010(X18)))&skolem0009(X18)!=skolem0010(X18)))|cc1(X18)))))))),inference(shift_quantors,[status(thm)],[fof(c32,plain,((![X14]:(~cc1(X14)|(rp(X14,skolem0008(X14))&(![X16]:(![X17]:((~rp(X14,X16)|~rp(X14,X17))|X16=X17))))))&(![X18]:(((![X19]:~rp(X18,X19))|((rp(X18,skolem0009(X18))&rp(X18,skolem0010(X18)))&skolem0009(X18)!=skolem0010(X18)))|cc1(X18)))),inference(skolemize,[status(esa)],[c31])).])).
% 0.71/0.89 fof(c34,plain,(![X14]:(![X16]:(![X17]:(![X18]:(![X19]:(((~cc1(X14)|rp(X14,skolem0008(X14)))&(~cc1(X14)|((~rp(X14,X16)|~rp(X14,X17))|X16=X17)))&((((~rp(X18,X19)|rp(X18,skolem0009(X18)))|cc1(X18))&((~rp(X18,X19)|rp(X18,skolem0010(X18)))|cc1(X18)))&((~rp(X18,X19)|skolem0009(X18)!=skolem0010(X18))|cc1(X18))))))))),inference(distribute,[status(thm)],[c33])).
% 0.71/0.89 cnf(c35,plain,~cc1(X54)|rp(X54,skolem0008(X54)),inference(split_conjunct,[status(thm)],[c34])).
% 0.71/0.89 fof(the_axiom,conjecture,(((![X]:(cowlThing(X)&(~cowlNothing(X))))&(![X]:(xsd_string(X)<=>(~xsd_integer(X)))))&(![X]:(cc1(X)<=>cc2(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', the_axiom)).
% 0.71/0.89 fof(c7,negated_conjecture,(~(((![X]:(cowlThing(X)&(~cowlNothing(X))))&(![X]:(xsd_string(X)<=>(~xsd_integer(X)))))&(![X]:(cc1(X)<=>cc2(X))))),inference(assume_negation,[status(cth)],[the_axiom])).
% 0.71/0.89 fof(c8,negated_conjecture,(~(((![X]:(cowlThing(X)&~cowlNothing(X)))&(![X]:(xsd_string(X)<=>~xsd_integer(X))))&(![X]:(cc1(X)<=>cc2(X))))),inference(fof_simplification,[status(thm)],[c7])).
% 0.71/0.89 fof(c9,negated_conjecture,(((?[X]:(~cowlThing(X)|cowlNothing(X)))|(?[X]:((~xsd_string(X)|xsd_integer(X))&(xsd_string(X)|~xsd_integer(X)))))|(?[X]:((~cc1(X)|~cc2(X))&(cc1(X)|cc2(X))))),inference(fof_nnf,[status(thm)],[c8])).
% 0.71/0.89 fof(c10,negated_conjecture,((((?[X]:~cowlThing(X))|(?[X]:cowlNothing(X)))|(?[X]:((~xsd_string(X)|xsd_integer(X))&(xsd_string(X)|~xsd_integer(X)))))|(?[X]:((~cc1(X)|~cc2(X))&(cc1(X)|cc2(X))))),inference(shift_quantors,[status(thm)],[c9])).
% 0.71/0.89 fof(c11,negated_conjecture,((((?[X2]:~cowlThing(X2))|(?[X3]:cowlNothing(X3)))|(?[X4]:((~xsd_string(X4)|xsd_integer(X4))&(xsd_string(X4)|~xsd_integer(X4)))))|(?[X5]:((~cc1(X5)|~cc2(X5))&(cc1(X5)|cc2(X5))))),inference(variable_rename,[status(thm)],[c10])).
% 0.71/0.89 fof(c12,negated_conjecture,(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|((~xsd_string(skolem0003)|xsd_integer(skolem0003))&(xsd_string(skolem0003)|~xsd_integer(skolem0003))))|((~cc1(skolem0004)|~cc2(skolem0004))&(cc1(skolem0004)|cc2(skolem0004)))),inference(skolemize,[status(esa)],[c11])).
% 0.71/0.89 fof(c13,negated_conjecture,(((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|(~cc1(skolem0004)|~cc2(skolem0004)))&(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|(cc1(skolem0004)|cc2(skolem0004))))&((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|(~cc1(skolem0004)|~cc2(skolem0004)))&(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|(cc1(skolem0004)|cc2(skolem0004))))),inference(distribute,[status(thm)],[c12])).
% 0.71/0.89 cnf(c15,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|cc1(skolem0004)|cc2(skolem0004),inference(split_conjunct,[status(thm)],[c13])).
% 0.71/0.89 cnf(c85,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_integer(skolem0003)|cc1(skolem0004)|cc2(skolem0004),inference(resolution,[status(thm)],[c15, c46])).
% 0.71/0.89 cnf(c88,plain,cowlNothing(skolem0002)|xsd_integer(skolem0003)|cc1(skolem0004)|cc2(skolem0004),inference(resolution,[status(thm)],[c85, c51])).
% 0.71/0.89 cnf(c89,plain,xsd_integer(skolem0003)|cc1(skolem0004)|cc2(skolem0004),inference(resolution,[status(thm)],[c88, c52])).
% 0.71/0.89 cnf(c98,plain,cc1(skolem0004)|cc2(skolem0004)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c89, c45])).
% 0.71/0.89 cnf(c17,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|cc1(skolem0004)|cc2(skolem0004),inference(split_conjunct,[status(thm)],[c13])).
% 0.71/0.89 cnf(c95,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|cc1(skolem0004)|cc2(skolem0004),inference(resolution,[status(thm)],[c17, c46])).
% 0.71/0.89 cnf(c188,plain,cowlNothing(skolem0002)|xsd_string(skolem0003)|cc1(skolem0004)|cc2(skolem0004),inference(resolution,[status(thm)],[c95, c51])).
% 0.71/0.89 cnf(c189,plain,xsd_string(skolem0003)|cc1(skolem0004)|cc2(skolem0004),inference(resolution,[status(thm)],[c188, c52])).
% 0.71/0.89 cnf(c201,plain,cc1(skolem0004)|cc2(skolem0004),inference(resolution,[status(thm)],[c189, c98])).
% 0.71/0.89 cnf(c212,plain,cc2(skolem0004)|rp(skolem0004,skolem0008(skolem0004)),inference(resolution,[status(thm)],[c201, c35])).
% 0.71/0.89 cnf(c222,plain,cc2(skolem0004)|rp(skolem0004,skolem0007(skolem0004)),inference(resolution,[status(thm)],[c212, c27])).
% 0.71/0.89 cnf(c28,plain,~rp(X112,X113)|skolem0006(X112)!=skolem0007(X112)|cc2(X112),inference(split_conjunct,[status(thm)],[c23])).
% 0.71/0.89 cnf(c26,plain,~rp(X99,X100)|rp(X99,skolem0006(X99))|cc2(X99),inference(split_conjunct,[status(thm)],[c23])).
% 0.71/0.89 cnf(c220,plain,cc2(skolem0004)|rp(skolem0004,skolem0006(skolem0004)),inference(resolution,[status(thm)],[c212, c26])).
% 0.71/0.89 cnf(c36,plain,~cc1(X115)|~rp(X115,X114)|~rp(X115,X116)|X114=X116,inference(split_conjunct,[status(thm)],[c34])).
% 0.71/0.89 cnf(c223,plain,cc2(skolem0004)|~cc1(skolem0004)|~rp(skolem0004,X153)|X153=skolem0008(skolem0004),inference(resolution,[status(thm)],[c212, c36])).
% 0.71/0.89 cnf(c435,plain,cc2(skolem0004)|~cc1(skolem0004)|skolem0006(skolem0004)=skolem0008(skolem0004),inference(resolution,[status(thm)],[c223, c220])).
% 0.71/0.89 cnf(c503,plain,cc2(skolem0004)|skolem0006(skolem0004)=skolem0008(skolem0004),inference(resolution,[status(thm)],[c435, c201])).
% 0.71/0.89 cnf(transitivity,axiom,X57!=X59|X59!=X58|X57=X58,theory(equality)).
% 0.71/0.89 cnf(symmetry,axiom,X49!=X50|X50=X49,theory(equality)).
% 0.71/0.89 cnf(c427,plain,cc2(skolem0004)|~cc1(skolem0004)|skolem0007(skolem0004)=skolem0008(skolem0004),inference(resolution,[status(thm)],[c223, c222])).
% 0.71/0.89 cnf(c441,plain,cc2(skolem0004)|skolem0007(skolem0004)=skolem0008(skolem0004),inference(resolution,[status(thm)],[c427, c201])).
% 0.71/0.89 cnf(c451,plain,cc2(skolem0004)|skolem0008(skolem0004)=skolem0007(skolem0004),inference(resolution,[status(thm)],[c441, symmetry])).
% 0.71/0.89 cnf(c458,plain,cc2(skolem0004)|X167!=skolem0008(skolem0004)|X167=skolem0007(skolem0004),inference(resolution,[status(thm)],[c451, transitivity])).
% 0.71/0.89 cnf(c647,plain,cc2(skolem0004)|skolem0006(skolem0004)=skolem0007(skolem0004),inference(resolution,[status(thm)],[c458, c503])).
% 0.71/0.89 cnf(c661,plain,cc2(skolem0004)|~rp(skolem0004,X168),inference(resolution,[status(thm)],[c647, c28])).
% 0.71/0.89 cnf(c670,plain,cc2(skolem0004),inference(resolution,[status(thm)],[c661, c222])).
% 0.71/0.89 cnf(c682,plain,rp(skolem0004,skolem0005(skolem0004)),inference(resolution,[status(thm)],[c670, c24])).
% 0.71/0.89 cnf(c39,plain,~rp(X119,X120)|skolem0009(X119)!=skolem0010(X119)|cc1(X119),inference(split_conjunct,[status(thm)],[c34])).
% 0.71/0.89 cnf(c37,plain,~rp(X103,X104)|rp(X103,skolem0009(X103))|cc1(X103),inference(split_conjunct,[status(thm)],[c34])).
% 0.71/0.89 cnf(c214,plain,cc1(skolem0004)|rp(skolem0004,skolem0005(skolem0004)),inference(resolution,[status(thm)],[c201, c24])).
% 0.71/0.89 cnf(c229,plain,cc1(skolem0004)|rp(skolem0004,skolem0009(skolem0004)),inference(resolution,[status(thm)],[c214, c37])).
% 0.71/0.89 cnf(c25,plain,~cc2(X107)|~rp(X107,X108)|~rp(X107,X109)|X108=X109,inference(split_conjunct,[status(thm)],[c23])).
% 0.71/0.89 cnf(c694,plain,~cc2(skolem0004)|~rp(skolem0004,X179)|X179=skolem0005(skolem0004),inference(resolution,[status(thm)],[c682, c25])).
% 0.71/0.89 cnf(c716,plain,~cc2(skolem0004)|skolem0009(skolem0004)=skolem0005(skolem0004)|cc1(skolem0004),inference(resolution,[status(thm)],[c694, c229])).
% 0.71/0.89 cnf(c759,plain,skolem0009(skolem0004)=skolem0005(skolem0004)|cc1(skolem0004),inference(resolution,[status(thm)],[c716, c670])).
% 0.71/0.89 cnf(c38,plain,~rp(X105,X106)|rp(X105,skolem0010(X105))|cc1(X105),inference(split_conjunct,[status(thm)],[c34])).
% 0.71/0.89 cnf(c231,plain,cc1(skolem0004)|rp(skolem0004,skolem0010(skolem0004)),inference(resolution,[status(thm)],[c214, c38])).
% 0.71/0.89 cnf(c715,plain,~cc2(skolem0004)|skolem0010(skolem0004)=skolem0005(skolem0004)|cc1(skolem0004),inference(resolution,[status(thm)],[c694, c231])).
% 0.71/0.89 cnf(c720,plain,skolem0010(skolem0004)=skolem0005(skolem0004)|cc1(skolem0004),inference(resolution,[status(thm)],[c715, c670])).
% 0.71/0.89 cnf(c727,plain,cc1(skolem0004)|skolem0005(skolem0004)=skolem0010(skolem0004),inference(resolution,[status(thm)],[c720, symmetry])).
% 0.71/0.89 cnf(c738,plain,cc1(skolem0004)|X200!=skolem0005(skolem0004)|X200=skolem0010(skolem0004),inference(resolution,[status(thm)],[c727, transitivity])).
% 0.71/0.89 cnf(c892,plain,cc1(skolem0004)|skolem0009(skolem0004)=skolem0010(skolem0004),inference(resolution,[status(thm)],[c738, c759])).
% 0.71/0.89 cnf(c898,plain,cc1(skolem0004)|~rp(skolem0004,X202),inference(resolution,[status(thm)],[c892, c39])).
% 0.71/0.89 cnf(c910,plain,cc1(skolem0004),inference(resolution,[status(thm)],[c898, c682])).
% 0.71/0.89 cnf(c14,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|~cc1(skolem0004)|~cc2(skolem0004),inference(split_conjunct,[status(thm)],[c13])).
% 0.71/0.89 cnf(c681,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|~cc1(skolem0004),inference(resolution,[status(thm)],[c670, c14])).
% 0.71/0.89 cnf(c971,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c681, c910])).
% 0.71/0.89 cnf(c972,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c971, c46])).
% 0.71/0.89 cnf(c973,plain,cowlNothing(skolem0002)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c972, c51])).
% 0.71/0.89 cnf(c974,plain,xsd_integer(skolem0003),inference(resolution,[status(thm)],[c973, c52])).
% 0.71/0.89 cnf(c976,plain,~xsd_string(skolem0003),inference(resolution,[status(thm)],[c974, c45])).
% 0.71/0.89 cnf(c16,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cc1(skolem0004)|~cc2(skolem0004),inference(split_conjunct,[status(thm)],[c13])).
% 0.71/0.89 cnf(c683,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cc1(skolem0004),inference(resolution,[status(thm)],[c670, c16])).
% 0.71/0.89 cnf(c978,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003),inference(resolution,[status(thm)],[c683, c910])).
% 0.71/0.89 cnf(c979,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c978, c974])).
% 0.71/0.89 cnf(c981,plain,cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c979, c51])).
% 0.71/0.89 cnf(c982,plain,xsd_string(skolem0003),inference(resolution,[status(thm)],[c981, c52])).
% 0.71/0.89 cnf(c984,plain,$false,inference(resolution,[status(thm)],[c982, c976])).
% 0.71/0.89 % SZS output end CNFRefutation
% 0.71/0.89
% 0.71/0.89 % Initial clauses : 36
% 0.71/0.89 % Processed clauses : 200
% 0.71/0.89 % Factors computed : 3
% 0.71/0.89 % Resolvents computed: 905
% 0.71/0.89 % Tautologies deleted: 34
% 0.71/0.89 % Forward subsumed : 414
% 0.71/0.89 % Backward subsumed : 145
% 0.71/0.89 % -------- CPU Time ---------
% 0.71/0.89 % User time : 0.526 s
% 0.71/0.89 % System time : 0.018 s
% 0.71/0.89 % Total time : 0.544 s
%------------------------------------------------------------------------------