%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS142+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:48 EDT 2024
% Result : Theorem 1.22s 1.44s
% Output : Refutation 1.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : KRS142+1 : TPTP v8.1.2. Released v3.1.0.
% 0.11/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n014.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 00:05:23 EDT 2024
% 0.14/0.35 % CPUTime :
% 1.22/1.44 % Version: 1.5
% 1.22/1.44 % SZS status Theorem
% 1.22/1.44 % SZS output start CNFRefutation
% 1.22/1.44 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_1)).
% 1.22/1.44 fof(c37,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 1.22/1.44 fof(c38,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c37])).
% 1.22/1.44 fof(c39,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c38])).
% 1.22/1.44 fof(c41,plain,(![X14]:(![X15]:((~xsd_string(X14)|~xsd_integer(X14))&(xsd_integer(X15)|xsd_string(X15))))),inference(shift_quantors,[status(thm)],[fof(c40,plain,((![X14]:(~xsd_string(X14)|~xsd_integer(X14)))&(![X15]:(xsd_integer(X15)|xsd_string(X15)))),inference(variable_rename,[status(thm)],[c39])).])).
% 1.22/1.44 cnf(c42,plain,~xsd_string(X37)|~xsd_integer(X37),inference(split_conjunct,[status(thm)],[c41])).
% 1.22/1.44 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_0)).
% 1.22/1.44 fof(c44,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 1.22/1.44 fof(c45,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c44])).
% 1.22/1.44 fof(c47,plain,(![X16]:(![X17]:(cowlThing(X16)&~cowlNothing(X17)))),inference(shift_quantors,[status(thm)],[fof(c46,plain,((![X16]:cowlThing(X16))&(![X17]:~cowlNothing(X17))),inference(variable_rename,[status(thm)],[c45])).])).
% 1.22/1.44 cnf(c49,plain,~cowlNothing(X35),inference(split_conjunct,[status(thm)],[c47])).
% 1.22/1.44 cnf(c48,plain,cowlThing(X34),inference(split_conjunct,[status(thm)],[c47])).
% 1.22/1.44 cnf(c43,plain,xsd_integer(X38)|xsd_string(X38),inference(split_conjunct,[status(thm)],[c41])).
% 1.22/1.44 fof(axiom_2,axiom,(![X]:(cc(X)=>((?[Y0]:rp(X,Y0))&(![Y0]:(![Y1]:((rp(X,Y0)&rp(X,Y1))=>Y0=Y1)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 1.22/1.44 fof(c30,plain,(![X]:(~cc(X)|((?[Y0]:rp(X,Y0))&(![Y0]:(![Y1]:((~rp(X,Y0)|~rp(X,Y1))|Y0=Y1)))))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 1.22/1.44 fof(c31,plain,(![X10]:(~cc(X10)|((?[X11]:rp(X10,X11))&(![X12]:(![X13]:((~rp(X10,X12)|~rp(X10,X13))|X12=X13)))))),inference(variable_rename,[status(thm)],[c30])).
% 1.22/1.44 fof(c33,plain,(![X10]:(![X12]:(![X13]:(~cc(X10)|(rp(X10,skolem0008(X10))&((~rp(X10,X12)|~rp(X10,X13))|X12=X13)))))),inference(shift_quantors,[status(thm)],[fof(c32,plain,(![X10]:(~cc(X10)|(rp(X10,skolem0008(X10))&(![X12]:(![X13]:((~rp(X10,X12)|~rp(X10,X13))|X12=X13)))))),inference(skolemize,[status(esa)],[c31])).])).
% 1.22/1.44 fof(c34,plain,(![X10]:(![X12]:(![X13]:((~cc(X10)|rp(X10,skolem0008(X10)))&(~cc(X10)|((~rp(X10,X12)|~rp(X10,X13))|X12=X13)))))),inference(distribute,[status(thm)],[c33])).
% 1.22/1.44 cnf(c35,plain,~cc(X43)|rp(X43,skolem0008(X43)),inference(split_conjunct,[status(thm)],[c34])).
% 1.22/1.44 fof(the_axiom,conjecture,((((![X]:(cowlThing(X)&(~cowlNothing(X))))&(![X]:(xsd_string(X)<=>(~xsd_integer(X)))))&(![X]:(cc(X)=>(?[Y0]:rp(X,Y0)))))&(![X]:(cc(X)=>(![Y0]:(![Y1]:((rp(X,Y0)&rp(X,Y1))=>Y0=Y1)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', the_axiom)).
% 1.22/1.44 fof(c6,negated_conjecture,(~((((![X]:(cowlThing(X)&(~cowlNothing(X))))&(![X]:(xsd_string(X)<=>(~xsd_integer(X)))))&(![X]:(cc(X)=>(?[Y0]:rp(X,Y0)))))&(![X]:(cc(X)=>(![Y0]:(![Y1]:((rp(X,Y0)&rp(X,Y1))=>Y0=Y1))))))),inference(assume_negation,[status(cth)],[the_axiom])).
% 1.22/1.44 fof(c7,negated_conjecture,(~((((![X]:(cowlThing(X)&~cowlNothing(X)))&(![X]:(xsd_string(X)<=>~xsd_integer(X))))&(![X]:(cc(X)=>(?[Y0]:rp(X,Y0)))))&(![X]:(cc(X)=>(![Y0]:(![Y1]:((rp(X,Y0)&rp(X,Y1))=>Y0=Y1))))))),inference(fof_simplification,[status(thm)],[c6])).
% 1.22/1.44 fof(c8,negated_conjecture,((((?[X]:(~cowlThing(X)|cowlNothing(X)))|(?[X]:((~xsd_string(X)|xsd_integer(X))&(xsd_string(X)|~xsd_integer(X)))))|(?[X]:(cc(X)&(![Y0]:~rp(X,Y0)))))|(?[X]:(cc(X)&(?[Y0]:(?[Y1]:((rp(X,Y0)&rp(X,Y1))&Y0!=Y1)))))),inference(fof_nnf,[status(thm)],[c7])).
% 1.22/1.44 fof(c9,negated_conjecture,(((((?[X]:~cowlThing(X))|(?[X]:cowlNothing(X)))|(?[X]:((~xsd_string(X)|xsd_integer(X))&(xsd_string(X)|~xsd_integer(X)))))|(?[X]:(cc(X)&(![Y0]:~rp(X,Y0)))))|(?[X]:(cc(X)&(?[Y0]:(?[Y1]:((rp(X,Y0)&rp(X,Y1))&Y0!=Y1)))))),inference(shift_quantors,[status(thm)],[c8])).
% 1.22/1.44 fof(c10,negated_conjecture,(((((?[X2]:~cowlThing(X2))|(?[X3]:cowlNothing(X3)))|(?[X4]:((~xsd_string(X4)|xsd_integer(X4))&(xsd_string(X4)|~xsd_integer(X4)))))|(?[X5]:(cc(X5)&(![X6]:~rp(X5,X6)))))|(?[X7]:(cc(X7)&(?[X8]:(?[X9]:((rp(X7,X8)&rp(X7,X9))&X8!=X9)))))),inference(variable_rename,[status(thm)],[c9])).
% 1.22/1.44 fof(c12,negated_conjecture,(![X6]:((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|((~xsd_string(skolem0003)|xsd_integer(skolem0003))&(xsd_string(skolem0003)|~xsd_integer(skolem0003))))|(cc(skolem0004)&~rp(skolem0004,X6)))|(cc(skolem0005)&((rp(skolem0005,skolem0006)&rp(skolem0005,skolem0007))&skolem0006!=skolem0007)))),inference(shift_quantors,[status(thm)],[fof(c11,negated_conjecture,((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|((~xsd_string(skolem0003)|xsd_integer(skolem0003))&(xsd_string(skolem0003)|~xsd_integer(skolem0003))))|(cc(skolem0004)&(![X6]:~rp(skolem0004,X6))))|(cc(skolem0005)&((rp(skolem0005,skolem0006)&rp(skolem0005,skolem0007))&skolem0006!=skolem0007))),inference(skolemize,[status(esa)],[c10])).])).
% 1.22/1.44 fof(c13,negated_conjecture,(![X6]:(((((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|cc(skolem0004))|cc(skolem0005))&((((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|cc(skolem0004))|rp(skolem0005,skolem0006))&((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|cc(skolem0004))|rp(skolem0005,skolem0007)))&((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|cc(skolem0004))|skolem0006!=skolem0007)))&(((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|~rp(skolem0004,X6))|cc(skolem0005))&((((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|~rp(skolem0004,X6))|rp(skolem0005,skolem0006))&((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|~rp(skolem0004,X6))|rp(skolem0005,skolem0007)))&((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|~rp(skolem0004,X6))|skolem0006!=skolem0007))))&((((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|cc(skolem0004))|cc(skolem0005))&((((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|cc(skolem0004))|rp(skolem0005,skolem0006))&((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|cc(skolem0004))|rp(skolem0005,skolem0007)))&((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|cc(skolem0004))|skolem0006!=skolem0007)))&(((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|~rp(skolem0004,X6))|cc(skolem0005))&((((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|~rp(skolem0004,X6))|rp(skolem0005,skolem0006))&((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|~rp(skolem0004,X6))|rp(skolem0005,skolem0007)))&((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|~rp(skolem0004,X6))|skolem0006!=skolem0007)))))),inference(distribute,[status(thm)],[c12])).
% 1.22/1.44 cnf(c17,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|cc(skolem0004)|skolem0006!=skolem0007,inference(split_conjunct,[status(thm)],[c13])).
% 1.22/1.44 cnf(symmetry,axiom,X40!=X39|X39=X40,theory(equality)).
% 1.22/1.44 cnf(c14,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|cc(skolem0004)|cc(skolem0005),inference(split_conjunct,[status(thm)],[c13])).
% 1.22/1.44 cnf(c78,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_integer(skolem0003)|cc(skolem0004)|cc(skolem0005),inference(resolution,[status(thm)],[c14, c43])).
% 1.22/1.44 cnf(c81,plain,cowlNothing(skolem0002)|xsd_integer(skolem0003)|cc(skolem0004)|cc(skolem0005),inference(resolution,[status(thm)],[c78, c48])).
% 1.22/1.44 cnf(c82,plain,xsd_integer(skolem0003)|cc(skolem0004)|cc(skolem0005),inference(resolution,[status(thm)],[c81, c49])).
% 1.22/1.44 cnf(c87,plain,xsd_integer(skolem0003)|cc(skolem0005)|rp(skolem0004,skolem0008(skolem0004)),inference(resolution,[status(thm)],[c82, c35])).
% 1.22/1.44 cnf(c18,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|~rp(skolem0004,X88)|cc(skolem0005),inference(split_conjunct,[status(thm)],[c13])).
% 1.22/1.44 cnf(c105,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|cc(skolem0005),inference(resolution,[status(thm)],[c18, c87])).
% 1.22/1.44 cnf(c124,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_integer(skolem0003)|cc(skolem0005),inference(resolution,[status(thm)],[c105, c43])).
% 1.22/1.44 cnf(c125,plain,cowlNothing(skolem0002)|xsd_integer(skolem0003)|cc(skolem0005),inference(resolution,[status(thm)],[c124, c48])).
% 1.22/1.44 cnf(c126,plain,xsd_integer(skolem0003)|cc(skolem0005),inference(resolution,[status(thm)],[c125, c49])).
% 1.22/1.44 cnf(c129,plain,cc(skolem0005)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c126, c42])).
% 1.22/1.44 cnf(c22,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|cc(skolem0004)|cc(skolem0005),inference(split_conjunct,[status(thm)],[c13])).
% 1.22/1.44 cnf(c138,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|cc(skolem0004)|cc(skolem0005),inference(resolution,[status(thm)],[c22, c43])).
% 1.22/1.44 cnf(c151,plain,cowlNothing(skolem0002)|xsd_string(skolem0003)|cc(skolem0004)|cc(skolem0005),inference(resolution,[status(thm)],[c138, c48])).
% 1.22/1.44 cnf(c152,plain,xsd_string(skolem0003)|cc(skolem0004)|cc(skolem0005),inference(resolution,[status(thm)],[c151, c49])).
% 1.22/1.44 cnf(c162,plain,cc(skolem0004)|cc(skolem0005),inference(resolution,[status(thm)],[c152, c129])).
% 1.22/1.44 cnf(c165,plain,cc(skolem0005)|rp(skolem0004,skolem0008(skolem0004)),inference(resolution,[status(thm)],[c162, c35])).
% 1.22/1.44 cnf(c26,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~rp(skolem0004,X102)|cc(skolem0005),inference(split_conjunct,[status(thm)],[c13])).
% 1.22/1.44 cnf(c180,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|cc(skolem0005),inference(resolution,[status(thm)],[c26, c165])).
% 1.22/1.44 cnf(c296,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|cc(skolem0005),inference(resolution,[status(thm)],[c180, c43])).
% 1.22/1.44 cnf(c303,plain,cowlNothing(skolem0002)|xsd_string(skolem0003)|cc(skolem0005),inference(resolution,[status(thm)],[c296, c48])).
% 1.22/1.44 cnf(c304,plain,xsd_string(skolem0003)|cc(skolem0005),inference(resolution,[status(thm)],[c303, c49])).
% 1.22/1.44 cnf(c317,plain,cc(skolem0005),inference(resolution,[status(thm)],[c304, c129])).
% 1.22/1.44 cnf(c36,plain,~cc(X83)|~rp(X83,X84)|~rp(X83,X85)|X84=X85,inference(split_conjunct,[status(thm)],[c34])).
% 1.22/1.44 cnf(c130,plain,xsd_integer(skolem0003)|rp(skolem0005,skolem0008(skolem0005)),inference(resolution,[status(thm)],[c126, c35])).
% 1.22/1.44 cnf(c135,plain,xsd_integer(skolem0003)|~cc(skolem0005)|~rp(skolem0005,X101)|X101=skolem0008(skolem0005),inference(resolution,[status(thm)],[c130, c36])).
% 1.22/1.44 cnf(c16,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|cc(skolem0004)|rp(skolem0005,skolem0007),inference(split_conjunct,[status(thm)],[c13])).
% 1.22/1.44 cnf(c89,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_integer(skolem0003)|cc(skolem0004)|rp(skolem0005,skolem0007),inference(resolution,[status(thm)],[c16, c43])).
% 1.22/1.44 cnf(c226,plain,cowlNothing(skolem0002)|xsd_integer(skolem0003)|cc(skolem0004)|rp(skolem0005,skolem0007),inference(resolution,[status(thm)],[c89, c48])).
% 1.22/1.44 cnf(c247,plain,xsd_integer(skolem0003)|cc(skolem0004)|rp(skolem0005,skolem0007),inference(resolution,[status(thm)],[c226, c49])).
% 1.22/1.44 cnf(c265,plain,xsd_integer(skolem0003)|cc(skolem0004)|~cc(skolem0005)|skolem0007=skolem0008(skolem0005),inference(resolution,[status(thm)],[c247, c135])).
% 1.22/1.44 cnf(c378,plain,xsd_integer(skolem0003)|cc(skolem0004)|skolem0007=skolem0008(skolem0005),inference(resolution,[status(thm)],[c265, c317])).
% 1.22/1.44 cnf(transitivity,axiom,X49!=X48|X48!=X47|X49=X47,theory(equality)).
% 1.22/1.44 cnf(c319,plain,rp(skolem0005,skolem0008(skolem0005)),inference(resolution,[status(thm)],[c317, c35])).
% 1.22/1.44 cnf(c322,plain,~cc(skolem0005)|~rp(skolem0005,X138)|X138=skolem0008(skolem0005),inference(resolution,[status(thm)],[c319, c36])).
% 1.22/1.44 cnf(c15,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|cc(skolem0004)|rp(skolem0005,skolem0006),inference(split_conjunct,[status(thm)],[c13])).
% 1.22/1.44 cnf(c79,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_integer(skolem0003)|cc(skolem0004)|rp(skolem0005,skolem0006),inference(resolution,[status(thm)],[c15, c43])).
% 1.22/1.44 cnf(c205,plain,cowlNothing(skolem0002)|xsd_integer(skolem0003)|cc(skolem0004)|rp(skolem0005,skolem0006),inference(resolution,[status(thm)],[c79, c48])).
% 1.22/1.44 cnf(c206,plain,xsd_integer(skolem0003)|cc(skolem0004)|rp(skolem0005,skolem0006),inference(resolution,[status(thm)],[c205, c49])).
% 1.22/1.44 cnf(c217,plain,cc(skolem0004)|rp(skolem0005,skolem0006)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c206, c42])).
% 1.22/1.44 cnf(c23,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|cc(skolem0004)|rp(skolem0005,skolem0006),inference(split_conjunct,[status(thm)],[c13])).
% 1.22/1.44 cnf(c143,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|cc(skolem0004)|rp(skolem0005,skolem0006),inference(resolution,[status(thm)],[c23, c43])).
% 1.22/1.44 cnf(c404,plain,cowlNothing(skolem0002)|xsd_string(skolem0003)|cc(skolem0004)|rp(skolem0005,skolem0006),inference(resolution,[status(thm)],[c143, c48])).
% 1.22/1.44 cnf(c442,plain,xsd_string(skolem0003)|cc(skolem0004)|rp(skolem0005,skolem0006),inference(resolution,[status(thm)],[c404, c49])).
% 1.22/1.44 cnf(c469,plain,cc(skolem0004)|rp(skolem0005,skolem0006),inference(resolution,[status(thm)],[c442, c217])).
% 1.22/1.44 cnf(c480,plain,cc(skolem0004)|~cc(skolem0005)|skolem0006=skolem0008(skolem0005),inference(resolution,[status(thm)],[c469, c322])).
% 1.22/1.44 cnf(c501,plain,cc(skolem0004)|skolem0006=skolem0008(skolem0005),inference(resolution,[status(thm)],[c480, c317])).
% 1.22/1.44 cnf(c507,plain,cc(skolem0004)|skolem0008(skolem0005)=skolem0006,inference(resolution,[status(thm)],[c501, symmetry])).
% 1.22/1.44 cnf(c514,plain,cc(skolem0004)|X154!=skolem0008(skolem0005)|X154=skolem0006,inference(resolution,[status(thm)],[c507, transitivity])).
% 1.22/1.44 cnf(c575,plain,cc(skolem0004)|skolem0007=skolem0006|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c514, c378])).
% 1.22/1.44 cnf(c582,plain,cc(skolem0004)|xsd_integer(skolem0003)|skolem0006=skolem0007,inference(resolution,[status(thm)],[c575, symmetry])).
% 1.22/1.44 cnf(c589,plain,cc(skolem0004)|xsd_integer(skolem0003)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c582, c17])).
% 1.22/1.44 cnf(c1471,plain,cc(skolem0004)|xsd_integer(skolem0003)|~cowlThing(skolem0001)|cowlNothing(skolem0002),inference(resolution,[status(thm)],[c589, c43])).
% 1.22/1.44 cnf(c1472,plain,cc(skolem0004)|xsd_integer(skolem0003)|cowlNothing(skolem0002),inference(resolution,[status(thm)],[c1471, c48])).
% 1.22/1.44 cnf(c1475,plain,cc(skolem0004)|xsd_integer(skolem0003),inference(resolution,[status(thm)],[c1472, c49])).
% 1.22/1.44 cnf(c1477,plain,cc(skolem0004)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c1475, c42])).
% 1.22/1.44 cnf(c25,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|cc(skolem0004)|skolem0006!=skolem0007,inference(split_conjunct,[status(thm)],[c13])).
% 1.22/1.44 cnf(c258,plain,cc(skolem0004)|rp(skolem0005,skolem0007)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c247, c42])).
% 1.22/1.44 cnf(c24,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|cc(skolem0004)|rp(skolem0005,skolem0007),inference(split_conjunct,[status(thm)],[c13])).
% 1.22/1.44 cnf(c148,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|cc(skolem0004)|rp(skolem0005,skolem0007),inference(resolution,[status(thm)],[c24, c43])).
% 1.22/1.44 cnf(c428,plain,cowlNothing(skolem0002)|xsd_string(skolem0003)|cc(skolem0004)|rp(skolem0005,skolem0007),inference(resolution,[status(thm)],[c148, c48])).
% 1.22/1.44 cnf(c605,plain,xsd_string(skolem0003)|cc(skolem0004)|rp(skolem0005,skolem0007),inference(resolution,[status(thm)],[c428, c49])).
% 1.22/1.44 cnf(c626,plain,cc(skolem0004)|rp(skolem0005,skolem0007),inference(resolution,[status(thm)],[c605, c258])).
% 1.22/1.44 cnf(c635,plain,cc(skolem0004)|~cc(skolem0005)|skolem0007=skolem0008(skolem0005),inference(resolution,[status(thm)],[c626, c322])).
% 1.22/1.44 cnf(c657,plain,cc(skolem0004)|skolem0007=skolem0008(skolem0005),inference(resolution,[status(thm)],[c635, c317])).
% 1.22/1.44 cnf(c662,plain,cc(skolem0004)|skolem0007=skolem0006,inference(resolution,[status(thm)],[c657, c514])).
% 1.22/1.44 cnf(c672,plain,cc(skolem0004)|skolem0006=skolem0007,inference(resolution,[status(thm)],[c662, symmetry])).
% 1.22/1.44 cnf(c678,plain,cc(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003),inference(resolution,[status(thm)],[c672, c25])).
% 1.22/1.44 cnf(c1490,plain,cc(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c678, c1475])).
% 1.22/1.44 cnf(c1506,plain,cc(skolem0004)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c1490, c48])).
% 1.22/1.44 cnf(c1508,plain,cc(skolem0004)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c1506, c49])).
% 1.22/1.44 cnf(c1534,plain,cc(skolem0004),inference(resolution,[status(thm)],[c1508, c1477])).
% 1.22/1.44 cnf(c1542,plain,rp(skolem0004,skolem0008(skolem0004)),inference(resolution,[status(thm)],[c1534, c35])).
% 1.22/1.44 cnf(c21,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|~rp(skolem0004,X95)|skolem0006!=skolem0007,inference(split_conjunct,[status(thm)],[c13])).
% 1.22/1.44 cnf(c19,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|~rp(skolem0004,X91)|rp(skolem0005,skolem0006),inference(split_conjunct,[status(thm)],[c13])).
% 1.22/1.44 cnf(c219,plain,xsd_integer(skolem0003)|rp(skolem0005,skolem0006)|rp(skolem0004,skolem0008(skolem0004)),inference(resolution,[status(thm)],[c206, c35])).
% 1.22/1.44 cnf(c243,plain,xsd_integer(skolem0003)|rp(skolem0005,skolem0006)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c219, c19])).
% 1.22/1.44 cnf(c980,plain,xsd_integer(skolem0003)|rp(skolem0005,skolem0006)|~cowlThing(skolem0001)|cowlNothing(skolem0002),inference(resolution,[status(thm)],[c243, c43])).
% 1.22/1.44 cnf(c1073,plain,xsd_integer(skolem0003)|rp(skolem0005,skolem0006)|cowlNothing(skolem0002),inference(resolution,[status(thm)],[c980, c48])).
% 1.22/1.44 cnf(c1084,plain,xsd_integer(skolem0003)|rp(skolem0005,skolem0006),inference(resolution,[status(thm)],[c1073, c49])).
% 1.22/1.44 cnf(c1092,plain,xsd_integer(skolem0003)|~cc(skolem0005)|~rp(skolem0005,X251)|X251=skolem0006,inference(resolution,[status(thm)],[c1084, c36])).
% 1.22/1.44 cnf(c20,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|~rp(skolem0004,X94)|rp(skolem0005,skolem0007),inference(split_conjunct,[status(thm)],[c13])).
% 1.22/1.44 cnf(c260,plain,xsd_integer(skolem0003)|rp(skolem0005,skolem0007)|rp(skolem0004,skolem0008(skolem0004)),inference(resolution,[status(thm)],[c247, c35])).
% 1.22/1.44 cnf(c276,plain,xsd_integer(skolem0003)|rp(skolem0005,skolem0007)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c260, c20])).
% 1.22/1.44 cnf(c1102,plain,xsd_integer(skolem0003)|rp(skolem0005,skolem0007)|~cowlThing(skolem0001)|cowlNothing(skolem0002),inference(resolution,[status(thm)],[c276, c43])).
% 1.22/1.44 cnf(c1215,plain,xsd_integer(skolem0003)|rp(skolem0005,skolem0007)|cowlNothing(skolem0002),inference(resolution,[status(thm)],[c1102, c48])).
% 1.22/1.44 cnf(c1226,plain,xsd_integer(skolem0003)|rp(skolem0005,skolem0007),inference(resolution,[status(thm)],[c1215, c49])).
% 1.22/1.44 cnf(c1233,plain,xsd_integer(skolem0003)|~cc(skolem0005)|skolem0007=skolem0006,inference(resolution,[status(thm)],[c1226, c1092])).
% 1.22/1.44 cnf(c1243,plain,xsd_integer(skolem0003)|skolem0007=skolem0006,inference(resolution,[status(thm)],[c1233, c317])).
% 1.22/1.44 cnf(c1256,plain,xsd_integer(skolem0003)|skolem0006=skolem0007,inference(resolution,[status(thm)],[c1243, symmetry])).
% 1.22/1.44 cnf(c1266,plain,xsd_integer(skolem0003)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|~rp(skolem0004,X401),inference(resolution,[status(thm)],[c1256, c21])).
% 1.22/1.44 cnf(c1847,plain,xsd_integer(skolem0003)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c1266, c1542])).
% 1.22/1.44 cnf(c1848,plain,xsd_integer(skolem0003)|~cowlThing(skolem0001)|cowlNothing(skolem0002),inference(resolution,[status(thm)],[c1847, c43])).
% 1.22/1.44 cnf(c1849,plain,xsd_integer(skolem0003)|cowlNothing(skolem0002),inference(resolution,[status(thm)],[c1848, c48])).
% 1.22/1.44 cnf(c1851,plain,xsd_integer(skolem0003),inference(resolution,[status(thm)],[c1849, c49])).
% 1.22/1.44 cnf(c1852,plain,~xsd_string(skolem0003),inference(resolution,[status(thm)],[c1851, c42])).
% 1.22/1.44 cnf(c29,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~rp(skolem0004,X109)|skolem0006!=skolem0007,inference(split_conjunct,[status(thm)],[c13])).
% 1.22/1.44 cnf(c1085,plain,rp(skolem0005,skolem0006)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c1084, c42])).
% 1.22/1.44 cnf(c27,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~rp(skolem0004,X105)|rp(skolem0005,skolem0006),inference(split_conjunct,[status(thm)],[c13])).
% 1.22/1.44 cnf(c479,plain,rp(skolem0005,skolem0006)|rp(skolem0004,skolem0008(skolem0004)),inference(resolution,[status(thm)],[c469, c35])).
% 1.22/1.44 cnf(c492,plain,rp(skolem0005,skolem0006)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003),inference(resolution,[status(thm)],[c479, c27])).
% 1.22/1.44 cnf(c1577,plain,rp(skolem0005,skolem0006)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c492, c1084])).
% 1.22/1.44 cnf(c1583,plain,rp(skolem0005,skolem0006)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c1577, c48])).
% 1.22/1.44 cnf(c1591,plain,rp(skolem0005,skolem0006)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c1583, c49])).
% 1.22/1.44 cnf(c1620,plain,rp(skolem0005,skolem0006),inference(resolution,[status(thm)],[c1591, c1085])).
% 1.22/1.44 cnf(c1633,plain,~cc(skolem0005)|~rp(skolem0005,X329)|X329=skolem0006,inference(resolution,[status(thm)],[c1620, c36])).
% 1.22/1.44 cnf(c1227,plain,rp(skolem0005,skolem0007)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c1226, c42])).
% 1.22/1.44 cnf(c28,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~rp(skolem0004,X108)|rp(skolem0005,skolem0007),inference(split_conjunct,[status(thm)],[c13])).
% 1.22/1.44 cnf(c634,plain,rp(skolem0005,skolem0007)|rp(skolem0004,skolem0008(skolem0004)),inference(resolution,[status(thm)],[c626, c35])).
% 1.22/1.44 cnf(c646,plain,rp(skolem0005,skolem0007)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003),inference(resolution,[status(thm)],[c634, c28])).
% 1.22/1.44 cnf(c1698,plain,rp(skolem0005,skolem0007)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c646, c43])).
% 1.22/1.44 cnf(c1701,plain,rp(skolem0005,skolem0007)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c1698, c48])).
% 1.22/1.44 cnf(c1709,plain,rp(skolem0005,skolem0007)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c1701, c49])).
% 1.22/1.44 cnf(c1729,plain,rp(skolem0005,skolem0007),inference(resolution,[status(thm)],[c1709, c1227])).
% 1.22/1.44 cnf(c1738,plain,~cc(skolem0005)|skolem0007=skolem0006,inference(resolution,[status(thm)],[c1729, c1633])).
% 1.22/1.44 cnf(c1743,plain,skolem0007=skolem0006,inference(resolution,[status(thm)],[c1738, c317])).
% 1.22/1.44 cnf(c1751,plain,skolem0006=skolem0007,inference(resolution,[status(thm)],[c1743, symmetry])).
% 1.22/1.44 cnf(c1758,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~rp(skolem0004,X403),inference(resolution,[status(thm)],[c1751, c29])).
% 1.22/1.44 cnf(c1854,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003),inference(resolution,[status(thm)],[c1758, c1542])).
% 1.22/1.44 cnf(c1855,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c1854, c43])).
% 1.22/1.44 cnf(c1857,plain,cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c1855, c48])).
% 1.22/1.44 cnf(c1858,plain,xsd_string(skolem0003),inference(resolution,[status(thm)],[c1857, c49])).
% 1.22/1.44 cnf(c1860,plain,$false,inference(resolution,[status(thm)],[c1858, c1852])).
% 1.22/1.44 % SZS output end CNFRefutation
% 1.22/1.44
% 1.22/1.44 % Initial clauses : 38
% 1.22/1.44 % Processed clauses : 414
% 1.22/1.44 % Factors computed : 2
% 1.22/1.44 % Resolvents computed: 1788
% 1.22/1.44 % Tautologies deleted: 14
% 1.22/1.44 % Forward subsumed : 1135
% 1.22/1.44 % Backward subsumed : 338
% 1.22/1.44 % -------- CPU Time ---------
% 1.22/1.44 % User time : 1.068 s
% 1.22/1.44 % System time : 0.017 s
% 1.22/1.44 % Total time : 1.085 s
%------------------------------------------------------------------------------