%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS172+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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:52 EDT 2024
% Result : Theorem 0.49s 0.69s
% Output : Refutation 0.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : KRS172+1 : TPTP v8.1.2. Released v3.1.0.
% 0.10/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n023.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 9 00:07:08 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.49/0.69 % Version: 1.5
% 0.49/0.69 % SZS status Theorem
% 0.49/0.69 % SZS output start CNFRefutation
% 0.49/0.69 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_1)).
% 0.49/0.69 fof(c47,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.49/0.69 fof(c48,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c47])).
% 0.49/0.69 fof(c49,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c48])).
% 0.49/0.69 fof(c51,plain,(![X21]:(![X22]:((~xsd_string(X21)|~xsd_integer(X21))&(xsd_integer(X22)|xsd_string(X22))))),inference(shift_quantors,[status(thm)],[fof(c50,plain,((![X21]:(~xsd_string(X21)|~xsd_integer(X21)))&(![X22]:(xsd_integer(X22)|xsd_string(X22)))),inference(variable_rename,[status(thm)],[c49])).])).
% 0.49/0.69 cnf(c52,plain,~xsd_string(X50)|~xsd_integer(X50),inference(split_conjunct,[status(thm)],[c51])).
% 0.49/0.69 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_0)).
% 0.49/0.69 fof(c54,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.49/0.69 fof(c55,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c54])).
% 0.49/0.69 fof(c57,plain,(![X23]:(![X24]:(cowlThing(X23)&~cowlNothing(X24)))),inference(shift_quantors,[status(thm)],[fof(c56,plain,((![X23]:cowlThing(X23))&(![X24]:~cowlNothing(X24))),inference(variable_rename,[status(thm)],[c55])).])).
% 0.49/0.69 cnf(c59,plain,~cowlNothing(X48),inference(split_conjunct,[status(thm)],[c57])).
% 0.49/0.69 cnf(c58,plain,cowlThing(X47),inference(split_conjunct,[status(thm)],[c57])).
% 0.49/0.69 cnf(c53,plain,xsd_integer(X54)|xsd_string(X54),inference(split_conjunct,[status(thm)],[c51])).
% 0.49/0.69 fof(rq_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rq(C,A))=>rq(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rq_substitution_2)).
% 0.49/0.69 fof(c66,plain,(![A]:(![B]:(![C]:((A!=B|~rq(C,A))|rq(C,B))))),inference(fof_nnf,[status(thm)],[rq_substitution_2])).
% 0.49/0.69 fof(c67,plain,(![X29]:(![X30]:(![X31]:((X29!=X30|~rq(X31,X29))|rq(X31,X30))))),inference(variable_rename,[status(thm)],[c66])).
% 0.49/0.69 cnf(c68,plain,X111!=X113|~rq(X112,X111)|rq(X112,X113),inference(split_conjunct,[status(thm)],[c67])).
% 0.49/0.69 fof(axiom_2,axiom,(![X]:(cd(X)<=>rq(X,iv))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.49/0.69 fof(c41,plain,(![X]:((~cd(X)|rq(X,iv))&(~rq(X,iv)|cd(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.49/0.69 fof(c42,plain,((![X]:(~cd(X)|rq(X,iv)))&(![X]:(~rq(X,iv)|cd(X)))),inference(shift_quantors,[status(thm)],[c41])).
% 0.49/0.69 fof(c44,plain,(![X19]:(![X20]:((~cd(X19)|rq(X19,iv))&(~rq(X20,iv)|cd(X20))))),inference(shift_quantors,[status(thm)],[fof(c43,plain,((![X19]:(~cd(X19)|rq(X19,iv)))&(![X20]:(~rq(X20,iv)|cd(X20)))),inference(variable_rename,[status(thm)],[c42])).])).
% 0.49/0.69 cnf(c45,plain,~cd(X65)|rq(X65,iv),inference(split_conjunct,[status(thm)],[c44])).
% 0.49/0.69 fof(axiom_5,axiom,(![X]:(![Y]:(rp(X,Y)=>cd(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 0.49/0.69 fof(c27,plain,(![X]:(![Y]:(~rp(X,Y)|cd(X)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.49/0.69 fof(c28,plain,(![X]:((![Y]:~rp(X,Y))|cd(X))),inference(shift_quantors,[status(thm)],[c27])).
% 0.49/0.69 fof(c30,plain,(![X12]:(![X13]:(~rp(X12,X13)|cd(X12)))),inference(shift_quantors,[status(thm)],[fof(c29,plain,(![X12]:((![X13]:~rp(X12,X13))|cd(X12))),inference(variable_rename,[status(thm)],[c28])).])).
% 0.49/0.69 cnf(c31,plain,~rp(X58,X59)|cd(X58),inference(split_conjunct,[status(thm)],[c30])).
% 0.49/0.69 fof(axiom_7,axiom,(![X]:(![Y]:(rq(X,Y)=>cd(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_7)).
% 0.49/0.69 fof(c19,plain,(![X]:(![Y]:(~rq(X,Y)|cd(X)))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.49/0.69 fof(c20,plain,(![X]:((![Y]:~rq(X,Y))|cd(X))),inference(shift_quantors,[status(thm)],[c19])).
% 0.49/0.69 fof(c22,plain,(![X7]:(![X8]:(~rq(X7,X8)|cd(X7)))),inference(shift_quantors,[status(thm)],[fof(c21,plain,(![X7]:((![X8]:~rq(X7,X8))|cd(X7))),inference(variable_rename,[status(thm)],[c20])).])).
% 0.49/0.69 cnf(c23,plain,~rq(X57,X56)|cd(X57),inference(split_conjunct,[status(thm)],[c22])).
% 0.49/0.69 fof(the_axiom,conjecture,(((![X]:(cowlThing(X)&(~cowlNothing(X))))&(![X]:(xsd_string(X)<=>(~xsd_integer(X)))))&(![X]:(![Y]:(rq(X,Y)<=>rp(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', the_axiom)).
% 0.49/0.69 fof(c7,negated_conjecture,(~(((![X]:(cowlThing(X)&(~cowlNothing(X))))&(![X]:(xsd_string(X)<=>(~xsd_integer(X)))))&(![X]:(![Y]:(rq(X,Y)<=>rp(X,Y)))))),inference(assume_negation,[status(cth)],[the_axiom])).
% 0.49/0.69 fof(c8,negated_conjecture,(~(((![X]:(cowlThing(X)&~cowlNothing(X)))&(![X]:(xsd_string(X)<=>~xsd_integer(X))))&(![X]:(![Y]:(rq(X,Y)<=>rp(X,Y)))))),inference(fof_simplification,[status(thm)],[c7])).
% 0.49/0.69 fof(c9,negated_conjecture,(((?[X]:(~cowlThing(X)|cowlNothing(X)))|(?[X]:((~xsd_string(X)|xsd_integer(X))&(xsd_string(X)|~xsd_integer(X)))))|(?[X]:(?[Y]:((~rq(X,Y)|~rp(X,Y))&(rq(X,Y)|rp(X,Y)))))),inference(fof_nnf,[status(thm)],[c8])).
% 0.49/0.69 fof(c10,negated_conjecture,((((?[X]:~cowlThing(X))|(?[X]:cowlNothing(X)))|(?[X]:((~xsd_string(X)|xsd_integer(X))&(xsd_string(X)|~xsd_integer(X)))))|(?[X]:(?[Y]:((~rq(X,Y)|~rp(X,Y))&(rq(X,Y)|rp(X,Y)))))),inference(shift_quantors,[status(thm)],[c9])).
% 0.49/0.69 fof(c11,negated_conjecture,((((?[X2]:~cowlThing(X2))|(?[X3]:cowlNothing(X3)))|(?[X4]:((~xsd_string(X4)|xsd_integer(X4))&(xsd_string(X4)|~xsd_integer(X4)))))|(?[X5]:(?[X6]:((~rq(X5,X6)|~rp(X5,X6))&(rq(X5,X6)|rp(X5,X6)))))),inference(variable_rename,[status(thm)],[c10])).
% 0.49/0.69 fof(c12,negated_conjecture,(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|((~xsd_string(skolem0003)|xsd_integer(skolem0003))&(xsd_string(skolem0003)|~xsd_integer(skolem0003))))|((~rq(skolem0004,skolem0005)|~rp(skolem0004,skolem0005))&(rq(skolem0004,skolem0005)|rp(skolem0004,skolem0005)))),inference(skolemize,[status(esa)],[c11])).
% 0.49/0.69 fof(c13,negated_conjecture,(((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|(~rq(skolem0004,skolem0005)|~rp(skolem0004,skolem0005)))&(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|(rq(skolem0004,skolem0005)|rp(skolem0004,skolem0005))))&((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|(~rq(skolem0004,skolem0005)|~rp(skolem0004,skolem0005)))&(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|(rq(skolem0004,skolem0005)|rp(skolem0004,skolem0005))))),inference(distribute,[status(thm)],[c12])).
% 0.49/0.69 cnf(c15,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|rq(skolem0004,skolem0005)|rp(skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c13])).
% 0.49/0.69 cnf(c96,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_integer(skolem0003)|rq(skolem0004,skolem0005)|rp(skolem0004,skolem0005),inference(resolution,[status(thm)],[c15, c53])).
% 0.49/0.69 cnf(c97,plain,cowlNothing(skolem0002)|xsd_integer(skolem0003)|rq(skolem0004,skolem0005)|rp(skolem0004,skolem0005),inference(resolution,[status(thm)],[c96, c58])).
% 0.49/0.69 cnf(c98,plain,xsd_integer(skolem0003)|rq(skolem0004,skolem0005)|rp(skolem0004,skolem0005),inference(resolution,[status(thm)],[c97, c59])).
% 0.49/0.69 cnf(c113,plain,xsd_integer(skolem0003)|rp(skolem0004,skolem0005)|cd(skolem0004),inference(resolution,[status(thm)],[c98, c23])).
% 0.49/0.69 cnf(c127,plain,xsd_integer(skolem0003)|cd(skolem0004),inference(resolution,[status(thm)],[c113, c31])).
% 0.49/0.69 cnf(c135,plain,xsd_integer(skolem0003)|rq(skolem0004,iv),inference(resolution,[status(thm)],[c127, c45])).
% 0.49/0.69 cnf(c143,plain,xsd_integer(skolem0003)|iv!=X126|rq(skolem0004,X126),inference(resolution,[status(thm)],[c135, c68])).
% 0.49/0.69 cnf(symmetry,axiom,X52!=X51|X51=X52,theory(equality)).
% 0.49/0.69 fof(axiom_4,axiom,(![X]:(![Y]:(![Z]:((rp(X,Y)&rp(X,Z))=>Y=Z)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.49/0.69 fof(c32,plain,(![X]:(![Y]:(![Z]:((~rp(X,Y)|~rp(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.49/0.69 fof(c33,plain,(![X14]:(![X15]:(![X16]:((~rp(X14,X15)|~rp(X14,X16))|X15=X16)))),inference(variable_rename,[status(thm)],[c32])).
% 0.49/0.69 cnf(c34,plain,~rp(X107,X108)|~rp(X107,X106)|X108=X106,inference(split_conjunct,[status(thm)],[c33])).
% 0.49/0.69 fof(axiom_3,axiom,(![X]:(cd(X)<=>rp(X,iv))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.49/0.69 fof(c35,plain,(![X]:((~cd(X)|rp(X,iv))&(~rp(X,iv)|cd(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.49/0.69 fof(c36,plain,((![X]:(~cd(X)|rp(X,iv)))&(![X]:(~rp(X,iv)|cd(X)))),inference(shift_quantors,[status(thm)],[c35])).
% 0.49/0.69 fof(c38,plain,(![X17]:(![X18]:((~cd(X17)|rp(X17,iv))&(~rp(X18,iv)|cd(X18))))),inference(shift_quantors,[status(thm)],[fof(c37,plain,((![X17]:(~cd(X17)|rp(X17,iv)))&(![X18]:(~rp(X18,iv)|cd(X18)))),inference(variable_rename,[status(thm)],[c36])).])).
% 0.49/0.69 cnf(c39,plain,~cd(X63)|rp(X63,iv),inference(split_conjunct,[status(thm)],[c38])).
% 0.49/0.69 cnf(c136,plain,xsd_integer(skolem0003)|rp(skolem0004,iv),inference(resolution,[status(thm)],[c127, c39])).
% 0.49/0.69 cnf(c151,plain,xsd_integer(skolem0003)|~rp(skolem0004,X128)|X128=iv,inference(resolution,[status(thm)],[c136, c34])).
% 0.49/0.69 fof(axiom_6,axiom,(![X]:(![Y]:(![Z]:((rq(X,Y)&rq(X,Z))=>Y=Z)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 0.49/0.69 fof(c24,plain,(![X]:(![Y]:(![Z]:((~rq(X,Y)|~rq(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.49/0.69 fof(c25,plain,(![X9]:(![X10]:(![X11]:((~rq(X9,X10)|~rq(X9,X11))|X10=X11)))),inference(variable_rename,[status(thm)],[c24])).
% 0.49/0.69 cnf(c26,plain,~rq(X101,X103)|~rq(X101,X102)|X103=X102,inference(split_conjunct,[status(thm)],[c25])).
% 0.49/0.69 cnf(c139,plain,xsd_integer(skolem0003)|~rq(skolem0004,X123)|X123=iv,inference(resolution,[status(thm)],[c135, c26])).
% 0.49/0.69 cnf(c159,plain,xsd_integer(skolem0003)|skolem0005=iv|rp(skolem0004,skolem0005),inference(resolution,[status(thm)],[c139, c98])).
% 0.49/0.69 cnf(c180,plain,xsd_integer(skolem0003)|skolem0005=iv,inference(resolution,[status(thm)],[c159, c151])).
% 0.49/0.69 cnf(c187,plain,xsd_integer(skolem0003)|iv=skolem0005,inference(resolution,[status(thm)],[c180, symmetry])).
% 0.49/0.69 cnf(c203,plain,xsd_integer(skolem0003)|rq(skolem0004,skolem0005),inference(resolution,[status(thm)],[c187, c143])).
% 0.49/0.69 cnf(c14,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|~rq(skolem0004,skolem0005)|~rp(skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c13])).
% 0.49/0.69 fof(rp_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rp(C,A))=>rp(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rp_substitution_2)).
% 0.49/0.69 fof(c72,plain,(![A]:(![B]:(![C]:((A!=B|~rp(C,A))|rp(C,B))))),inference(fof_nnf,[status(thm)],[rp_substitution_2])).
% 0.49/0.69 fof(c73,plain,(![X35]:(![X36]:(![X37]:((X35!=X36|~rp(X37,X35))|rp(X37,X36))))),inference(variable_rename,[status(thm)],[c72])).
% 0.49/0.69 cnf(c74,plain,X117!=X118|~rp(X119,X117)|rp(X119,X118),inference(split_conjunct,[status(thm)],[c73])).
% 0.49/0.69 cnf(c153,plain,xsd_integer(skolem0003)|iv!=X129|rp(skolem0004,X129),inference(resolution,[status(thm)],[c136, c74])).
% 0.49/0.69 cnf(c198,plain,xsd_integer(skolem0003)|rp(skolem0004,skolem0005),inference(resolution,[status(thm)],[c187, c153])).
% 0.49/0.69 cnf(c211,plain,xsd_integer(skolem0003)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|~rq(skolem0004,skolem0005),inference(resolution,[status(thm)],[c198, c14])).
% 0.49/0.69 cnf(c265,plain,xsd_integer(skolem0003)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c211, c203])).
% 0.49/0.69 cnf(c266,plain,xsd_integer(skolem0003)|~cowlThing(skolem0001)|cowlNothing(skolem0002),inference(resolution,[status(thm)],[c265, c53])).
% 0.49/0.69 cnf(c267,plain,xsd_integer(skolem0003)|cowlNothing(skolem0002),inference(resolution,[status(thm)],[c266, c58])).
% 0.49/0.69 cnf(c270,plain,xsd_integer(skolem0003),inference(resolution,[status(thm)],[c267, c59])).
% 0.49/0.69 cnf(c271,plain,~xsd_string(skolem0003),inference(resolution,[status(thm)],[c270, c52])).
% 0.49/0.69 cnf(c17,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|rq(skolem0004,skolem0005)|rp(skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c13])).
% 0.49/0.69 cnf(c144,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|rq(skolem0004,skolem0005)|rp(skolem0004,skolem0005),inference(resolution,[status(thm)],[c17, c98])).
% 0.49/0.69 cnf(c274,plain,cowlNothing(skolem0002)|xsd_string(skolem0003)|rq(skolem0004,skolem0005)|rp(skolem0004,skolem0005),inference(resolution,[status(thm)],[c144, c58])).
% 0.49/0.69 cnf(c275,plain,xsd_string(skolem0003)|rq(skolem0004,skolem0005)|rp(skolem0004,skolem0005),inference(resolution,[status(thm)],[c274, c59])).
% 0.49/0.69 cnf(c288,plain,rq(skolem0004,skolem0005)|rp(skolem0004,skolem0005),inference(resolution,[status(thm)],[c275, c271])).
% 0.49/0.69 cnf(c301,plain,rp(skolem0004,skolem0005)|cd(skolem0004),inference(resolution,[status(thm)],[c288, c23])).
% 0.49/0.69 cnf(c313,plain,cd(skolem0004),inference(resolution,[status(thm)],[c301, c31])).
% 0.49/0.69 cnf(c319,plain,rq(skolem0004,iv),inference(resolution,[status(thm)],[c313, c45])).
% 0.49/0.69 cnf(c325,plain,iv!=X184|rq(skolem0004,X184),inference(resolution,[status(thm)],[c319, c68])).
% 0.49/0.69 cnf(c320,plain,rp(skolem0004,iv),inference(resolution,[status(thm)],[c313, c39])).
% 0.49/0.69 cnf(c327,plain,~rp(skolem0004,X186)|X186=iv,inference(resolution,[status(thm)],[c320, c34])).
% 0.49/0.69 cnf(c321,plain,~rq(skolem0004,X182)|X182=iv,inference(resolution,[status(thm)],[c319, c26])).
% 0.49/0.69 cnf(c331,plain,skolem0005=iv|rp(skolem0004,skolem0005),inference(resolution,[status(thm)],[c321, c288])).
% 0.49/0.69 cnf(c346,plain,skolem0005=iv,inference(resolution,[status(thm)],[c331, c327])).
% 0.49/0.69 cnf(c354,plain,iv=skolem0005,inference(resolution,[status(thm)],[c346, symmetry])).
% 0.49/0.69 cnf(c360,plain,rq(skolem0004,skolem0005),inference(resolution,[status(thm)],[c354, c325])).
% 0.49/0.69 cnf(c16,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~rq(skolem0004,skolem0005)|~rp(skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c13])).
% 0.49/0.69 cnf(c329,plain,iv!=X187|rp(skolem0004,X187),inference(resolution,[status(thm)],[c320, c74])).
% 0.49/0.69 cnf(c361,plain,rp(skolem0004,skolem0005),inference(resolution,[status(thm)],[c354, c329])).
% 0.49/0.69 cnf(c374,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~rq(skolem0004,skolem0005),inference(resolution,[status(thm)],[c361, c16])).
% 0.49/0.69 cnf(c408,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003),inference(resolution,[status(thm)],[c374, c360])).
% 0.49/0.69 cnf(c409,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c408, c53])).
% 0.49/0.69 cnf(c411,plain,cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c409, c58])).
% 0.49/0.69 cnf(c412,plain,xsd_string(skolem0003),inference(resolution,[status(thm)],[c411, c59])).
% 0.49/0.69 cnf(c414,plain,$false,inference(resolution,[status(thm)],[c412, c271])).
% 0.49/0.69 % SZS output end CNFRefutation
% 0.49/0.69
% 0.49/0.69 % Initial clauses : 36
% 0.49/0.69 % Processed clauses : 129
% 0.49/0.69 % Factors computed : 3
% 0.49/0.69 % Resolvents computed: 325
% 0.49/0.69 % Tautologies deleted: 12
% 0.49/0.69 % Forward subsumed : 209
% 0.49/0.69 % Backward subsumed : 71
% 0.49/0.69 % -------- CPU Time ---------
% 0.49/0.69 % User time : 0.334 s
% 0.49/0.69 % System time : 0.010 s
% 0.49/0.69 % Total time : 0.344 s
%------------------------------------------------------------------------------