%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS175+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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 1.75s 1.94s
% Output : Refutation 1.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : KRS175+1 : TPTP v8.1.2. Released v3.1.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n008.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 00:08:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 1.75/1.94 % Version: 1.5
% 1.75/1.94 % SZS status Theorem
% 1.75/1.94 % SZS output start CNFRefutation
% 1.75/1.94 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_1)).
% 1.75/1.94 fof(c42,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 1.75/1.94 fof(c43,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c42])).
% 1.75/1.94 fof(c44,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c43])).
% 1.75/1.94 fof(c46,plain,(![X12]:(![X13]:((~xsd_string(X12)|~xsd_integer(X12))&(xsd_integer(X13)|xsd_string(X13))))),inference(shift_quantors,[status(thm)],[fof(c45,plain,((![X12]:(~xsd_string(X12)|~xsd_integer(X12)))&(![X13]:(xsd_integer(X13)|xsd_string(X13)))),inference(variable_rename,[status(thm)],[c44])).])).
% 1.75/1.94 cnf(c47,plain,~xsd_string(X38)|~xsd_integer(X38),inference(split_conjunct,[status(thm)],[c46])).
% 1.75/1.94 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_0)).
% 1.75/1.94 fof(c49,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 1.75/1.94 fof(c50,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c49])).
% 1.75/1.94 fof(c52,plain,(![X14]:(![X15]:(cowlThing(X14)&~cowlNothing(X15)))),inference(shift_quantors,[status(thm)],[fof(c51,plain,((![X14]:cowlThing(X14))&(![X15]:~cowlNothing(X15))),inference(variable_rename,[status(thm)],[c50])).])).
% 1.75/1.94 cnf(c54,plain,~cowlNothing(X31),inference(split_conjunct,[status(thm)],[c52])).
% 1.75/1.94 cnf(c53,plain,cowlThing(X30),inference(split_conjunct,[status(thm)],[c52])).
% 1.75/1.94 cnf(c48,plain,xsd_integer(X39)|xsd_string(X39),inference(split_conjunct,[status(thm)],[c46])).
% 1.75/1.94 fof(axiom_3,axiom,(![X]:(cA_and_B(X)<=>(cA(X)|cB(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 1.75/1.94 fof(c28,plain,(![X]:((~cA_and_B(X)|(cA(X)|cB(X)))&((~cA(X)&~cB(X))|cA_and_B(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 1.75/1.94 fof(c29,plain,((![X]:(~cA_and_B(X)|(cA(X)|cB(X))))&(![X]:((~cA(X)&~cB(X))|cA_and_B(X)))),inference(shift_quantors,[status(thm)],[c28])).
% 1.75/1.94 fof(c31,plain,(![X8]:(![X9]:((~cA_and_B(X8)|(cA(X8)|cB(X8)))&((~cA(X9)&~cB(X9))|cA_and_B(X9))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,((![X8]:(~cA_and_B(X8)|(cA(X8)|cB(X8))))&(![X9]:((~cA(X9)&~cB(X9))|cA_and_B(X9)))),inference(variable_rename,[status(thm)],[c29])).])).
% 1.75/1.94 fof(c32,plain,(![X8]:(![X9]:((~cA_and_B(X8)|(cA(X8)|cB(X8)))&((~cA(X9)|cA_and_B(X9))&(~cB(X9)|cA_and_B(X9)))))),inference(distribute,[status(thm)],[c31])).
% 1.75/1.94 cnf(c34,plain,~cA(X36)|cA_and_B(X36),inference(split_conjunct,[status(thm)],[c32])).
% 1.75/1.94 fof(axiom_2,axiom,(![X]:(cA(X)<=>X=ia)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 1.75/1.94 fof(c36,plain,(![X]:((~cA(X)|X=ia)&(X!=ia|cA(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 1.75/1.94 fof(c37,plain,((![X]:(~cA(X)|X=ia))&(![X]:(X!=ia|cA(X)))),inference(shift_quantors,[status(thm)],[c36])).
% 1.75/1.94 fof(c39,plain,(![X10]:(![X11]:((~cA(X10)|X10=ia)&(X11!=ia|cA(X11))))),inference(shift_quantors,[status(thm)],[fof(c38,plain,((![X10]:(~cA(X10)|X10=ia))&(![X11]:(X11!=ia|cA(X11)))),inference(variable_rename,[status(thm)],[c37])).])).
% 1.75/1.94 cnf(c41,plain,X50!=ia|cA(X50),inference(split_conjunct,[status(thm)],[c39])).
% 1.75/1.94 cnf(c35,plain,~cB(X37)|cA_and_B(X37),inference(split_conjunct,[status(thm)],[c32])).
% 1.75/1.94 fof(axiom_4,axiom,(![X]:(cB(X)<=>X=ib)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 1.75/1.94 fof(c22,plain,(![X]:((~cB(X)|X=ib)&(X!=ib|cB(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 1.75/1.94 fof(c23,plain,((![X]:(~cB(X)|X=ib))&(![X]:(X!=ib|cB(X)))),inference(shift_quantors,[status(thm)],[c22])).
% 1.75/1.94 fof(c25,plain,(![X6]:(![X7]:((~cB(X6)|X6=ib)&(X7!=ib|cB(X7))))),inference(shift_quantors,[status(thm)],[fof(c24,plain,((![X6]:(~cB(X6)|X6=ib))&(![X7]:(X7!=ib|cB(X7)))),inference(variable_rename,[status(thm)],[c23])).])).
% 1.75/1.94 cnf(c27,plain,X45!=ib|cB(X45),inference(split_conjunct,[status(thm)],[c25])).
% 1.75/1.94 fof(the_axiom,conjecture,(((((![X]:(cowlThing(X)&(~cowlNothing(X))))&(![X]:(xsd_string(X)<=>(~xsd_integer(X)))))&(![X]:(cA_and_B(X)<=>(X=ib|X=ia))))&cowlThing(ia))&cowlThing(ib)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', the_axiom)).
% 1.75/1.94 fof(c7,negated_conjecture,(~(((((![X]:(cowlThing(X)&(~cowlNothing(X))))&(![X]:(xsd_string(X)<=>(~xsd_integer(X)))))&(![X]:(cA_and_B(X)<=>(X=ib|X=ia))))&cowlThing(ia))&cowlThing(ib))),inference(assume_negation,[status(cth)],[the_axiom])).
% 1.75/1.94 fof(c8,negated_conjecture,(~(((((![X]:(cowlThing(X)&~cowlNothing(X)))&(![X]:(xsd_string(X)<=>~xsd_integer(X))))&(![X]:(cA_and_B(X)<=>(X=ib|X=ia))))&cowlThing(ia))&cowlThing(ib))),inference(fof_simplification,[status(thm)],[c7])).
% 1.75/1.94 fof(c9,negated_conjecture,(((((?[X]:(~cowlThing(X)|cowlNothing(X)))|(?[X]:((~xsd_string(X)|xsd_integer(X))&(xsd_string(X)|~xsd_integer(X)))))|(?[X]:((~cA_and_B(X)|(X!=ib&X!=ia))&(cA_and_B(X)|(X=ib|X=ia)))))|~cowlThing(ia))|~cowlThing(ib)),inference(fof_nnf,[status(thm)],[c8])).
% 1.75/1.94 fof(c10,negated_conjecture,((((((?[X]:~cowlThing(X))|(?[X]:cowlNothing(X)))|(?[X]:((~xsd_string(X)|xsd_integer(X))&(xsd_string(X)|~xsd_integer(X)))))|(?[X]:((~cA_and_B(X)|(X!=ib&X!=ia))&(cA_and_B(X)|(X=ib|X=ia)))))|~cowlThing(ia))|~cowlThing(ib)),inference(shift_quantors,[status(thm)],[c9])).
% 1.75/1.94 fof(c11,negated_conjecture,((((((?[X2]:~cowlThing(X2))|(?[X3]:cowlNothing(X3)))|(?[X4]:((~xsd_string(X4)|xsd_integer(X4))&(xsd_string(X4)|~xsd_integer(X4)))))|(?[X5]:((~cA_and_B(X5)|(X5!=ib&X5!=ia))&(cA_and_B(X5)|(X5=ib|X5=ia)))))|~cowlThing(ia))|~cowlThing(ib)),inference(variable_rename,[status(thm)],[c10])).
% 1.75/1.94 fof(c12,negated_conjecture,(((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|((~xsd_string(skolem0003)|xsd_integer(skolem0003))&(xsd_string(skolem0003)|~xsd_integer(skolem0003))))|((~cA_and_B(skolem0004)|(skolem0004!=ib&skolem0004!=ia))&(cA_and_B(skolem0004)|(skolem0004=ib|skolem0004=ia))))|~cowlThing(ia))|~cowlThing(ib)),inference(skolemize,[status(esa)],[c11])).
% 1.75/1.94 fof(c13,negated_conjecture,((((((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|(~cA_and_B(skolem0004)|skolem0004!=ib))|~cowlThing(ia))|~cowlThing(ib))&(((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|(~cA_and_B(skolem0004)|skolem0004!=ia))|~cowlThing(ia))|~cowlThing(ib)))&(((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|(cA_and_B(skolem0004)|(skolem0004=ib|skolem0004=ia)))|~cowlThing(ia))|~cowlThing(ib)))&(((((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|(~cA_and_B(skolem0004)|skolem0004!=ib))|~cowlThing(ia))|~cowlThing(ib))&(((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|(~cA_and_B(skolem0004)|skolem0004!=ia))|~cowlThing(ia))|~cowlThing(ib)))&(((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|(cA_and_B(skolem0004)|(skolem0004=ib|skolem0004=ia)))|~cowlThing(ia))|~cowlThing(ib)))),inference(distribute,[status(thm)],[c12])).
% 1.75/1.94 cnf(c16,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|cA_and_B(skolem0004)|skolem0004=ib|skolem0004=ia|~cowlThing(ia)|~cowlThing(ib),inference(split_conjunct,[status(thm)],[c13])).
% 1.75/1.94 cnf(c93,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|cA_and_B(skolem0004)|skolem0004=ib|skolem0004=ia|~cowlThing(ia),inference(resolution,[status(thm)],[c16, c53])).
% 1.75/1.94 cnf(c94,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|cA_and_B(skolem0004)|skolem0004=ib|skolem0004=ia,inference(resolution,[status(thm)],[c93, c53])).
% 1.75/1.94 cnf(c96,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_integer(skolem0003)|cA_and_B(skolem0004)|skolem0004=ib|skolem0004=ia,inference(resolution,[status(thm)],[c94, c48])).
% 1.75/1.94 cnf(c97,plain,cowlNothing(skolem0002)|xsd_integer(skolem0003)|cA_and_B(skolem0004)|skolem0004=ib|skolem0004=ia,inference(resolution,[status(thm)],[c96, c53])).
% 1.75/1.94 cnf(c98,plain,xsd_integer(skolem0003)|cA_and_B(skolem0004)|skolem0004=ib|skolem0004=ia,inference(resolution,[status(thm)],[c97, c54])).
% 1.75/1.94 cnf(c130,plain,xsd_integer(skolem0003)|cA_and_B(skolem0004)|skolem0004=ia|cB(skolem0004),inference(resolution,[status(thm)],[c98, c27])).
% 1.75/1.94 cnf(c155,plain,xsd_integer(skolem0003)|cA_and_B(skolem0004)|skolem0004=ia,inference(resolution,[status(thm)],[c130, c35])).
% 1.75/1.94 cnf(c164,plain,xsd_integer(skolem0003)|cA_and_B(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c155, c41])).
% 1.75/1.94 cnf(c173,plain,xsd_integer(skolem0003)|cA_and_B(skolem0004),inference(resolution,[status(thm)],[c164, c34])).
% 1.75/1.94 cnf(c174,plain,cA_and_B(skolem0004)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c173, c47])).
% 1.75/1.94 cnf(c19,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|cA_and_B(skolem0004)|skolem0004=ib|skolem0004=ia|~cowlThing(ia)|~cowlThing(ib),inference(split_conjunct,[status(thm)],[c13])).
% 1.75/1.94 cnf(c95,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|cA_and_B(skolem0004)|skolem0004=ib|skolem0004=ia|~cowlThing(ia),inference(resolution,[status(thm)],[c19, c53])).
% 1.75/1.94 cnf(c157,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|cA_and_B(skolem0004)|skolem0004=ib|skolem0004=ia,inference(resolution,[status(thm)],[c95, c53])).
% 1.75/1.94 cnf(c667,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|cA_and_B(skolem0004)|skolem0004=ib|skolem0004=ia,inference(resolution,[status(thm)],[c157, c48])).
% 1.75/1.94 cnf(c854,plain,cowlNothing(skolem0002)|xsd_string(skolem0003)|cA_and_B(skolem0004)|skolem0004=ib|skolem0004=ia,inference(resolution,[status(thm)],[c667, c53])).
% 1.75/1.94 cnf(c855,plain,xsd_string(skolem0003)|cA_and_B(skolem0004)|skolem0004=ib|skolem0004=ia,inference(resolution,[status(thm)],[c854, c54])).
% 1.75/1.94 cnf(c916,plain,cA_and_B(skolem0004)|skolem0004=ib|skolem0004=ia,inference(resolution,[status(thm)],[c855, c174])).
% 1.75/1.94 cnf(c973,plain,cA_and_B(skolem0004)|skolem0004=ia|cB(skolem0004),inference(resolution,[status(thm)],[c916, c27])).
% 1.75/1.94 cnf(c1014,plain,cA_and_B(skolem0004)|skolem0004=ia,inference(resolution,[status(thm)],[c973, c35])).
% 1.75/1.94 cnf(c1024,plain,cA_and_B(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c1014, c41])).
% 1.75/1.94 cnf(c1039,plain,cA_and_B(skolem0004),inference(resolution,[status(thm)],[c1024, c34])).
% 1.75/1.94 cnf(c14,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|~cA_and_B(skolem0004)|skolem0004!=ib|~cowlThing(ia)|~cowlThing(ib),inference(split_conjunct,[status(thm)],[c13])).
% 1.75/1.94 cnf(c26,plain,~cB(X44)|X44=ib,inference(split_conjunct,[status(thm)],[c25])).
% 1.75/1.94 cnf(c15,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|~cA_and_B(skolem0004)|skolem0004!=ia|~cowlThing(ia)|~cowlThing(ib),inference(split_conjunct,[status(thm)],[c13])).
% 1.75/1.94 cnf(c40,plain,~cA(X49)|X49=ia,inference(split_conjunct,[status(thm)],[c39])).
% 1.75/1.94 cnf(c33,plain,~cA_and_B(X60)|cA(X60)|cB(X60),inference(split_conjunct,[status(thm)],[c32])).
% 1.75/1.94 cnf(c171,plain,xsd_integer(skolem0003)|cA(skolem0004)|cB(skolem0004),inference(resolution,[status(thm)],[c164, c33])).
% 1.75/1.94 cnf(c178,plain,xsd_integer(skolem0003)|cB(skolem0004)|skolem0004=ia,inference(resolution,[status(thm)],[c171, c40])).
% 1.75/1.94 cnf(c195,plain,xsd_integer(skolem0003)|cB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|~cA_and_B(skolem0004)|~cowlThing(ia)|~cowlThing(ib),inference(resolution,[status(thm)],[c178, c15])).
% 1.75/1.94 cnf(c726,plain,xsd_integer(skolem0003)|cB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|~cA_and_B(skolem0004)|~cowlThing(ia),inference(resolution,[status(thm)],[c195, c53])).
% 1.75/1.94 cnf(c1381,plain,xsd_integer(skolem0003)|cB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|~cA_and_B(skolem0004),inference(resolution,[status(thm)],[c726, c53])).
% 1.75/1.94 cnf(c1981,plain,xsd_integer(skolem0003)|cB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c1381, c1039])).
% 1.75/1.94 cnf(c1982,plain,xsd_integer(skolem0003)|cB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002),inference(resolution,[status(thm)],[c1981, c48])).
% 1.75/1.94 cnf(c1983,plain,xsd_integer(skolem0003)|cB(skolem0004)|cowlNothing(skolem0002),inference(resolution,[status(thm)],[c1982, c53])).
% 1.75/1.94 cnf(c1990,plain,xsd_integer(skolem0003)|cB(skolem0004),inference(resolution,[status(thm)],[c1983, c54])).
% 1.75/1.94 cnf(c1997,plain,xsd_integer(skolem0003)|skolem0004=ib,inference(resolution,[status(thm)],[c1990, c26])).
% 1.75/1.94 cnf(c2013,plain,xsd_integer(skolem0003)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|~cA_and_B(skolem0004)|~cowlThing(ia)|~cowlThing(ib),inference(resolution,[status(thm)],[c1997, c14])).
% 1.75/1.94 cnf(c2518,plain,xsd_integer(skolem0003)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|~cA_and_B(skolem0004)|~cowlThing(ia),inference(resolution,[status(thm)],[c2013, c53])).
% 1.75/1.94 cnf(c2624,plain,xsd_integer(skolem0003)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|~cA_and_B(skolem0004),inference(resolution,[status(thm)],[c2518, c53])).
% 1.75/1.94 cnf(c2677,plain,xsd_integer(skolem0003)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c2624, c1039])).
% 1.75/1.94 cnf(c2678,plain,xsd_integer(skolem0003)|~cowlThing(skolem0001)|cowlNothing(skolem0002),inference(resolution,[status(thm)],[c2677, c48])).
% 1.75/1.94 cnf(c2679,plain,xsd_integer(skolem0003)|cowlNothing(skolem0002),inference(resolution,[status(thm)],[c2678, c53])).
% 1.75/1.94 cnf(c2681,plain,xsd_integer(skolem0003),inference(resolution,[status(thm)],[c2679, c54])).
% 1.75/1.94 cnf(c2682,plain,~xsd_string(skolem0003),inference(resolution,[status(thm)],[c2681, c47])).
% 1.75/1.94 cnf(c17,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cA_and_B(skolem0004)|skolem0004!=ib|~cowlThing(ia)|~cowlThing(ib),inference(split_conjunct,[status(thm)],[c13])).
% 1.75/1.94 cnf(c1992,plain,cB(skolem0004)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c1990, c47])).
% 1.75/1.94 cnf(c18,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cA_and_B(skolem0004)|skolem0004!=ia|~cowlThing(ia)|~cowlThing(ib),inference(split_conjunct,[status(thm)],[c13])).
% 1.75/1.94 cnf(c1034,plain,cA(skolem0004)|cB(skolem0004),inference(resolution,[status(thm)],[c1024, c33])).
% 1.75/1.94 cnf(c1041,plain,cB(skolem0004)|skolem0004=ia,inference(resolution,[status(thm)],[c1034, c40])).
% 1.75/1.94 cnf(c1056,plain,cB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cA_and_B(skolem0004)|~cowlThing(ia)|~cowlThing(ib),inference(resolution,[status(thm)],[c1041, c18])).
% 1.75/1.94 cnf(c1975,plain,cB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cA_and_B(skolem0004)|~cowlThing(ia),inference(resolution,[status(thm)],[c1056, c53])).
% 1.75/1.94 cnf(c2372,plain,cB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cA_and_B(skolem0004),inference(resolution,[status(thm)],[c1975, c53])).
% 1.75/1.94 cnf(c2373,plain,cB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003),inference(resolution,[status(thm)],[c2372, c1039])).
% 1.75/1.94 cnf(c2377,plain,cB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c2373, c48])).
% 1.75/1.94 cnf(c2392,plain,cB(skolem0004)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c2377, c53])).
% 1.75/1.94 cnf(c2398,plain,cB(skolem0004)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c2392, c54])).
% 1.75/1.94 cnf(c2423,plain,cB(skolem0004),inference(resolution,[status(thm)],[c2398, c1992])).
% 1.75/1.94 cnf(c2440,plain,skolem0004=ib,inference(resolution,[status(thm)],[c2423, c26])).
% 1.75/1.94 cnf(c2443,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cA_and_B(skolem0004)|~cowlThing(ia)|~cowlThing(ib),inference(resolution,[status(thm)],[c2440, c17])).
% 1.75/1.94 cnf(c2586,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cA_and_B(skolem0004)|~cowlThing(ia),inference(resolution,[status(thm)],[c2443, c53])).
% 1.75/1.94 cnf(c2684,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cA_and_B(skolem0004),inference(resolution,[status(thm)],[c2586, c53])).
% 1.75/1.94 cnf(c2685,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003),inference(resolution,[status(thm)],[c2684, c1039])).
% 1.75/1.94 cnf(c2686,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c2685, c48])).
% 1.75/1.94 cnf(c2688,plain,cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c2686, c53])).
% 1.75/1.94 cnf(c2689,plain,xsd_string(skolem0003),inference(resolution,[status(thm)],[c2688, c54])).
% 1.75/1.94 cnf(c2691,plain,$false,inference(resolution,[status(thm)],[c2689, c2682])).
% 1.75/1.94 % SZS output end CNFRefutation
% 1.75/1.94
% 1.75/1.94 % Initial clauses : 36
% 1.75/1.94 % Processed clauses : 401
% 1.75/1.94 % Factors computed : 1
% 1.75/1.94 % Resolvents computed: 2615
% 1.75/1.94 % Tautologies deleted: 76
% 1.75/1.94 % Forward subsumed : 2171
% 1.75/1.94 % Backward subsumed : 340
% 1.75/1.94 % -------- CPU Time ---------
% 1.75/1.94 % User time : 1.582 s
% 1.75/1.94 % System time : 0.012 s
% 1.75/1.94 % Total time : 1.594 s
%------------------------------------------------------------------------------