%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS147+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:00:20 PM UTC 2026
% Result : Theorem 0.11s 0.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS147+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n011.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 20 22:54:40 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 0.11/0.44 % Refutation found
% 0.11/0.44 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/0.44 % SZS output start CNFRefutation for theBenchmark
% 0.11/0.44 fof(f1,axiom,(
% 0.11/0.44 (! [X] :( cowlThing(X)& ~ cowlNothing(X) ) )),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f2,axiom,(
% 0.11/0.44 (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ) )),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f3,axiom,(
% 0.11/0.44 (! [X] :( cC10(X)<=> ( cC4(X)& cC8(X) ) ) )),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f5,axiom,(
% 0.11/0.44 (! [X] :( cC14(X)<=> (? [Y] :( rR1(X,Y)& cTOP(Y) ) )) )),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f8,axiom,(
% 0.11/0.44 (! [X] :( cC20(X)<=> (? [Y] :( rR1(X,Y)& ~ cC2(Y) ) )) )),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f15,axiom,(
% 0.11/0.44 (! [X] :( cC34(X)<=> (? [Y] :( rR1(X,Y)& ~ cC32(Y) ) )) )),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f18,axiom,(
% 0.11/0.44 (! [X] :( cC4(X)<=> (? [Y] :( rR1(X,Y)& ~ cC2(Y) ) )) )),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f23,axiom,(
% 0.11/0.44 (! [X] :( cC48(X)<=> (? [Y] :( rR1(X,Y)& ~ cC2(Y) ) )) )),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f28,axiom,(
% 0.11/0.44 (! [X] :( cC58(X)<=> (? [Y] :( rR1(X,Y)& cC2(Y) ) )) )),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f30,axiom,(
% 0.11/0.44 (! [X] :( cC60(X)<=> ( cC58(X)& ~ cC2(X) ) ) )),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f31,axiom,(
% 0.11/0.44 (! [X] :( cC62(X)<=> (? [Y] :( rR1(X,Y)& cC60(Y) ) )) )),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f40,axiom,(
% 0.11/0.44 (! [X] :( cC8(X)<=> (? [Y] :( rR1(X,Y)& ~ cC6(Y) ) )) )),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f41,axiom,(
% 0.11/0.44 (! [X] :( cC80(X)<=> ( ~ cC2(X)& ~ cC78(X) ) ) )),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f42,axiom,(
% 0.11/0.44 (! [X] :( cC82(X)<=> (? [Y] :( rR1(X,Y)& cC80(Y) ) )) )),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f56,axiom,(
% 0.11/0.44 rR1(iV8467,iV8471) ),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f59,axiom,(
% 0.11/0.44 rR1(iV8467,iV8469) ),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f61,axiom,(
% 0.11/0.44 rR1(iV8467,iV8472) ),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f62,axiom,(
% 0.11/0.44 rR1(iV8467,iV8474) ),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f63,axiom,(
% 0.11/0.44 rR1(iV8467,iV8470) ),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f66,axiom,(
% 0.11/0.44 ~ cC6(iV8469) ),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f69,axiom,(
% 0.11/0.44 cTOP(iV8470) ),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f71,axiom,(
% 0.11/0.44 ~ cC2(iV8471) ),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f72,axiom,(
% 0.11/0.44 ~ cC78(iV8471) ),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f75,axiom,(
% 0.11/0.44 ~ cC2(iV8472) ),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f77,axiom,(
% 0.11/0.44 rR1(iV8472,iV8476) ),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f81,axiom,(
% 0.11/0.44 ~ cC32(iV8474) ),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f85,axiom,(
% 0.11/0.44 cC2(iV8476) ),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f87,conjecture,(
% 0.11/0.44 ( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& cC10(iV8467)& cC48(iV8467)& cC4(iV8467)& cC82(iV8467)& cC14(iV8467)& cC8(iV8467)& cC20(iV8467)& cowlThing(iV8467)& cC62(iV8467)& cC34(iV8467)& cowlThing(iV8471)& cC80(iV8471)& cC60(iV8472)& cowlThing(iV8472)& cC58(iV8472) ) ),
% 0.11/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.44 fof(f88,negated_conjecture,(
% 0.11/0.44 ~(( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& cC10(iV8467)& cC48(iV8467)& cC4(iV8467)& cC82(iV8467)& cC14(iV8467)& cC8(iV8467)& cC20(iV8467)& cowlThing(iV8467)& cC62(iV8467)& cC34(iV8467)& cowlThing(iV8471)& cC80(iV8471)& cC60(iV8472)& cowlThing(iV8472)& cC58(iV8472) ) )),
% 0.11/0.44 inference(negated_conjecture,[status(cth)],[f87])).
% 0.11/0.44 fof(f89,plain,(
% 0.11/0.44 (![X]: cowlThing(X))&(![X]: ~cowlNothing(X))),
% 0.11/0.44 inference(miniscoping,[status(thm)],[f1])).
% 0.11/0.44 fof(f90,plain,(
% 0.11/0.44 ![X0]: (cowlThing(X0))),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f89])).
% 0.11/0.44 fof(f91,plain,(
% 0.11/0.44 ![X0]: (~cowlNothing(X0))),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f89])).
% 0.11/0.44 fof(f92,plain,(
% 0.11/0.44 ![X]: ((~xsd_string(X)|~xsd_integer(X))&(xsd_string(X)|xsd_integer(X)))),
% 0.11/0.44 inference(NNF_transformation,[status(thm)],[f2])).
% 0.11/0.44 fof(f93,plain,(
% 0.11/0.44 (![X]: (~xsd_string(X)|~xsd_integer(X)))&(![X]: (xsd_string(X)|xsd_integer(X)))),
% 0.11/0.44 inference(miniscoping,[status(thm)],[f92])).
% 0.11/0.44 fof(f94,plain,(
% 0.11/0.44 ![X0]: (~xsd_string(X0)|~xsd_integer(X0))),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f93])).
% 0.11/0.44 fof(f95,plain,(
% 0.11/0.44 ![X0]: (xsd_string(X0)|xsd_integer(X0))),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f93])).
% 0.11/0.44 fof(f96,plain,(
% 0.11/0.44 ![X]: ((~cC10(X)|(cC4(X)&cC8(X)))&(cC10(X)|(~cC4(X)|~cC8(X))))),
% 0.11/0.44 inference(NNF_transformation,[status(thm)],[f3])).
% 0.11/0.44 fof(f97,plain,(
% 0.11/0.44 (![X]: (~cC10(X)|(cC4(X)&cC8(X))))&(![X]: (cC10(X)|(~cC4(X)|~cC8(X))))),
% 0.11/0.44 inference(miniscoping,[status(thm)],[f96])).
% 0.11/0.44 fof(f99,plain,(
% 0.11/0.44 ![X0]: (~cC10(X0)|cC8(X0))),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f97])).
% 0.11/0.44 fof(f100,plain,(
% 0.11/0.44 ![X0]: (cC10(X0)|~cC4(X0)|~cC8(X0))),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f97])).
% 0.11/0.44 fof(f107,plain,(
% 0.11/0.44 ![X]: ((~cC14(X)|(?[Y]: (rR1(X,Y)&cTOP(Y))))&(cC14(X)|(![Y]: (~rR1(X,Y)|~cTOP(Y)))))),
% 0.11/0.44 inference(NNF_transformation,[status(thm)],[f5])).
% 0.11/0.44 fof(f108,plain,(
% 0.11/0.44 (![X]: (~cC14(X)|(?[Y]: (rR1(X,Y)&cTOP(Y)))))&(![X]: (cC14(X)|(![Y]: (~rR1(X,Y)|~cTOP(Y)))))),
% 0.11/0.44 inference(miniscoping,[status(thm)],[f107])).
% 0.11/0.44 fof(f109,plain,(
% 0.11/0.44 (![X]: (~cC14(X)|(rR1(X,sK1_skl(X))&cTOP(sK1_skl(X)))))&(![X]: (cC14(X)|(![Y]: (~rR1(X,Y)|~cTOP(Y)))))),
% 0.11/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Y,sK1_skl(X))],[f108])).
% 0.11/0.44 fof(f112,plain,(
% 0.11/0.44 ![X0,X1]: (cC14(X0)|~rR1(X0,X1)|~cTOP(X1))),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f109])).
% 0.11/0.44 fof(f124,plain,(
% 0.11/0.44 ![X]: ((~cC20(X)|(?[Y]: (rR1(X,Y)&~cC2(Y))))&(cC20(X)|(![Y]: (~rR1(X,Y)|cC2(Y)))))),
% 0.11/0.44 inference(NNF_transformation,[status(thm)],[f8])).
% 0.11/0.44 fof(f125,plain,(
% 0.11/0.44 (![X]: (~cC20(X)|(?[Y]: (rR1(X,Y)&~cC2(Y)))))&(![X]: (cC20(X)|(![Y]: (~rR1(X,Y)|cC2(Y)))))),
% 0.11/0.44 inference(miniscoping,[status(thm)],[f124])).
% 0.11/0.44 fof(f126,plain,(
% 0.11/0.44 (![X]: (~cC20(X)|(rR1(X,sK3_skl(X))&~cC2(sK3_skl(X)))))&(![X]: (cC20(X)|(![Y]: (~rR1(X,Y)|cC2(Y)))))),
% 0.11/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(Y,sK3_skl(X))],[f125])).
% 0.11/0.44 fof(f129,plain,(
% 0.11/0.44 ![X0,X1]: (cC20(X0)|~rR1(X0,X1)|cC2(X1))),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f126])).
% 0.11/0.44 fof(f164,plain,(
% 0.11/0.44 ![X]: ((~cC34(X)|(?[Y]: (rR1(X,Y)&~cC32(Y))))&(cC34(X)|(![Y]: (~rR1(X,Y)|cC32(Y)))))),
% 0.11/0.44 inference(NNF_transformation,[status(thm)],[f15])).
% 0.11/0.44 fof(f165,plain,(
% 0.11/0.44 (![X]: (~cC34(X)|(?[Y]: (rR1(X,Y)&~cC32(Y)))))&(![X]: (cC34(X)|(![Y]: (~rR1(X,Y)|cC32(Y)))))),
% 0.11/0.44 inference(miniscoping,[status(thm)],[f164])).
% 0.11/0.44 fof(f166,plain,(
% 0.11/0.44 (![X]: (~cC34(X)|(rR1(X,sK8_skl(X))&~cC32(sK8_skl(X)))))&(![X]: (cC34(X)|(![Y]: (~rR1(X,Y)|cC32(Y)))))),
% 0.11/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(Y,sK8_skl(X))],[f165])).
% 0.11/0.44 fof(f169,plain,(
% 0.11/0.44 ![X0,X1]: (cC34(X0)|~rR1(X0,X1)|cC32(X1))),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f166])).
% 0.11/0.44 fof(f182,plain,(
% 0.11/0.44 ![X]: ((~cC4(X)|(?[Y]: (rR1(X,Y)&~cC2(Y))))&(cC4(X)|(![Y]: (~rR1(X,Y)|cC2(Y)))))),
% 0.11/0.44 inference(NNF_transformation,[status(thm)],[f18])).
% 0.11/0.44 fof(f183,plain,(
% 0.11/0.44 (![X]: (~cC4(X)|(?[Y]: (rR1(X,Y)&~cC2(Y)))))&(![X]: (cC4(X)|(![Y]: (~rR1(X,Y)|cC2(Y)))))),
% 0.11/0.44 inference(miniscoping,[status(thm)],[f182])).
% 0.11/0.44 fof(f184,plain,(
% 0.11/0.44 (![X]: (~cC4(X)|(rR1(X,sK11_skl(X))&~cC2(sK11_skl(X)))))&(![X]: (cC4(X)|(![Y]: (~rR1(X,Y)|cC2(Y)))))),
% 0.11/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(Y,sK11_skl(X))],[f183])).
% 0.11/0.44 fof(f187,plain,(
% 0.11/0.44 ![X0,X1]: (cC4(X0)|~rR1(X0,X1)|cC2(X1))),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f184])).
% 0.11/0.44 fof(f210,plain,(
% 0.11/0.44 ![X]: ((~cC48(X)|(?[Y]: (rR1(X,Y)&~cC2(Y))))&(cC48(X)|(![Y]: (~rR1(X,Y)|cC2(Y)))))),
% 0.11/0.44 inference(NNF_transformation,[status(thm)],[f23])).
% 0.11/0.44 fof(f211,plain,(
% 0.11/0.44 (![X]: (~cC48(X)|(?[Y]: (rR1(X,Y)&~cC2(Y)))))&(![X]: (cC48(X)|(![Y]: (~rR1(X,Y)|cC2(Y)))))),
% 0.11/0.44 inference(miniscoping,[status(thm)],[f210])).
% 0.11/0.44 fof(f212,plain,(
% 0.11/0.44 (![X]: (~cC48(X)|(rR1(X,sK14_skl(X))&~cC2(sK14_skl(X)))))&(![X]: (cC48(X)|(![Y]: (~rR1(X,Y)|cC2(Y)))))),
% 0.11/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(Y,sK14_skl(X))],[f211])).
% 0.11/0.44 fof(f215,plain,(
% 0.11/0.44 ![X0,X1]: (cC48(X0)|~rR1(X0,X1)|cC2(X1))),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f212])).
% 0.11/0.44 fof(f238,plain,(
% 0.11/0.44 ![X]: ((~cC58(X)|(?[Y]: (rR1(X,Y)&cC2(Y))))&(cC58(X)|(![Y]: (~rR1(X,Y)|~cC2(Y)))))),
% 0.11/0.44 inference(NNF_transformation,[status(thm)],[f28])).
% 0.11/0.44 fof(f239,plain,(
% 0.11/0.44 (![X]: (~cC58(X)|(?[Y]: (rR1(X,Y)&cC2(Y)))))&(![X]: (cC58(X)|(![Y]: (~rR1(X,Y)|~cC2(Y)))))),
% 0.11/0.44 inference(miniscoping,[status(thm)],[f238])).
% 0.11/0.44 fof(f240,plain,(
% 0.11/0.44 (![X]: (~cC58(X)|(rR1(X,sK17_skl(X))&cC2(sK17_skl(X)))))&(![X]: (cC58(X)|(![Y]: (~rR1(X,Y)|~cC2(Y)))))),
% 0.11/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(Y,sK17_skl(X))],[f239])).
% 0.11/0.44 fof(f243,plain,(
% 0.11/0.44 ![X0,X1]: (cC58(X0)|~rR1(X0,X1)|~cC2(X1))),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f240])).
% 0.11/0.44 fof(f250,plain,(
% 0.11/0.44 ![X]: ((~cC60(X)|(cC58(X)&~cC2(X)))&(cC60(X)|(~cC58(X)|cC2(X))))),
% 0.11/0.44 inference(NNF_transformation,[status(thm)],[f30])).
% 0.11/0.44 fof(f251,plain,(
% 0.11/0.44 (![X]: (~cC60(X)|(cC58(X)&~cC2(X))))&(![X]: (cC60(X)|(~cC58(X)|cC2(X))))),
% 0.11/0.44 inference(miniscoping,[status(thm)],[f250])).
% 0.11/0.44 fof(f252,plain,(
% 0.11/0.44 ![X0]: (~cC60(X0)|cC58(X0))),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f251])).
% 0.11/0.44 fof(f254,plain,(
% 0.11/0.44 ![X0]: (cC60(X0)|~cC58(X0)|cC2(X0))),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f251])).
% 0.11/0.44 fof(f255,plain,(
% 0.11/0.44 ![X]: ((~cC62(X)|(?[Y]: (rR1(X,Y)&cC60(Y))))&(cC62(X)|(![Y]: (~rR1(X,Y)|~cC60(Y)))))),
% 0.11/0.44 inference(NNF_transformation,[status(thm)],[f31])).
% 0.11/0.44 fof(f256,plain,(
% 0.11/0.44 (![X]: (~cC62(X)|(?[Y]: (rR1(X,Y)&cC60(Y)))))&(![X]: (cC62(X)|(![Y]: (~rR1(X,Y)|~cC60(Y)))))),
% 0.11/0.44 inference(miniscoping,[status(thm)],[f255])).
% 0.11/0.44 fof(f257,plain,(
% 0.11/0.44 (![X]: (~cC62(X)|(rR1(X,sK19_skl(X))&cC60(sK19_skl(X)))))&(![X]: (cC62(X)|(![Y]: (~rR1(X,Y)|~cC60(Y)))))),
% 0.11/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl]),skolemize(Y,sK19_skl(X))],[f256])).
% 0.11/0.44 fof(f260,plain,(
% 0.11/0.44 ![X0,X1]: (cC62(X0)|~rR1(X0,X1)|~cC60(X1))),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f257])).
% 0.11/0.44 fof(f306,plain,(
% 0.11/0.44 ![X]: ((~cC8(X)|(?[Y]: (rR1(X,Y)&~cC6(Y))))&(cC8(X)|(![Y]: (~rR1(X,Y)|cC6(Y)))))),
% 0.11/0.44 inference(NNF_transformation,[status(thm)],[f40])).
% 0.11/0.44 fof(f307,plain,(
% 0.11/0.44 (![X]: (~cC8(X)|(?[Y]: (rR1(X,Y)&~cC6(Y)))))&(![X]: (cC8(X)|(![Y]: (~rR1(X,Y)|cC6(Y)))))),
% 0.11/0.44 inference(miniscoping,[status(thm)],[f306])).
% 0.11/0.44 fof(f308,plain,(
% 0.11/0.44 (![X]: (~cC8(X)|(rR1(X,sK25_skl(X))&~cC6(sK25_skl(X)))))&(![X]: (cC8(X)|(![Y]: (~rR1(X,Y)|cC6(Y)))))),
% 0.11/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl]),skolemize(Y,sK25_skl(X))],[f307])).
% 0.11/0.44 fof(f311,plain,(
% 0.11/0.44 ![X0,X1]: (cC8(X0)|~rR1(X0,X1)|cC6(X1))),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f308])).
% 0.11/0.44 fof(f312,plain,(
% 0.11/0.44 ![X]: ((~cC80(X)|(~cC2(X)&~cC78(X)))&(cC80(X)|(cC2(X)|cC78(X))))),
% 0.11/0.44 inference(NNF_transformation,[status(thm)],[f41])).
% 0.11/0.44 fof(f313,plain,(
% 0.11/0.44 (![X]: (~cC80(X)|(~cC2(X)&~cC78(X))))&(![X]: (cC80(X)|(cC2(X)|cC78(X))))),
% 0.11/0.44 inference(miniscoping,[status(thm)],[f312])).
% 0.11/0.44 fof(f316,plain,(
% 0.11/0.44 ![X0]: (cC80(X0)|cC2(X0)|cC78(X0))),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f313])).
% 0.11/0.44 fof(f317,plain,(
% 0.11/0.44 ![X]: ((~cC82(X)|(?[Y]: (rR1(X,Y)&cC80(Y))))&(cC82(X)|(![Y]: (~rR1(X,Y)|~cC80(Y)))))),
% 0.11/0.44 inference(NNF_transformation,[status(thm)],[f42])).
% 0.11/0.44 fof(f318,plain,(
% 0.11/0.44 (![X]: (~cC82(X)|(?[Y]: (rR1(X,Y)&cC80(Y)))))&(![X]: (cC82(X)|(![Y]: (~rR1(X,Y)|~cC80(Y)))))),
% 0.11/0.44 inference(miniscoping,[status(thm)],[f317])).
% 0.11/0.44 fof(f319,plain,(
% 0.11/0.44 (![X]: (~cC82(X)|(rR1(X,sK26_skl(X))&cC80(sK26_skl(X)))))&(![X]: (cC82(X)|(![Y]: (~rR1(X,Y)|~cC80(Y)))))),
% 0.11/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(Y,sK26_skl(X))],[f318])).
% 0.11/0.44 fof(f322,plain,(
% 0.11/0.44 ![X0,X1]: (cC82(X0)|~rR1(X0,X1)|~cC80(X1))),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f319])).
% 0.11/0.44 fof(f368,plain,(
% 0.11/0.44 rR1(iV8467,iV8471)),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f56])).
% 0.11/0.44 fof(f371,plain,(
% 0.11/0.44 rR1(iV8467,iV8469)),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f59])).
% 0.11/0.44 fof(f373,plain,(
% 0.11/0.44 rR1(iV8467,iV8472)),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f61])).
% 0.11/0.44 fof(f374,plain,(
% 0.11/0.44 rR1(iV8467,iV8474)),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f62])).
% 0.11/0.44 fof(f375,plain,(
% 0.11/0.44 rR1(iV8467,iV8470)),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f63])).
% 0.11/0.44 fof(f378,plain,(
% 0.11/0.44 ~cC6(iV8469)),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f66])).
% 0.11/0.44 fof(f382,plain,(
% 0.11/0.44 cTOP(iV8470)),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f69])).
% 0.11/0.44 fof(f384,plain,(
% 0.11/0.44 ~cC2(iV8471)),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f71])).
% 0.11/0.44 fof(f385,plain,(
% 0.11/0.44 ~cC78(iV8471)),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f72])).
% 0.11/0.44 fof(f389,plain,(
% 0.11/0.44 ~cC2(iV8472)),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f75])).
% 0.11/0.44 fof(f391,plain,(
% 0.11/0.44 rR1(iV8472,iV8476)),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f77])).
% 0.11/0.44 fof(f396,plain,(
% 0.11/0.44 ~cC32(iV8474)),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f81])).
% 0.11/0.44 fof(f400,plain,(
% 0.11/0.44 cC2(iV8476)),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f85])).
% 0.11/0.44 fof(f402,plain,(
% 0.11/0.44 (((((((((((((((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: (xsd_string(X)<~>~xsd_integer(X))))|~cC10(iV8467))|~cC48(iV8467))|~cC4(iV8467))|~cC82(iV8467))|~cC14(iV8467))|~cC8(iV8467))|~cC20(iV8467))|~cowlThing(iV8467))|~cC62(iV8467))|~cC34(iV8467))|~cowlThing(iV8471))|~cC80(iV8471))|~cC60(iV8472))|~cowlThing(iV8472))|~cC58(iV8472))),
% 0.11/0.44 inference(pre_NNF_transformation,[status(thm)],[f88])).
% 0.11/0.44 fof(f403,plain,(
% 0.11/0.44 ((((((((((((((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: ((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))|~cC10(iV8467))|~cC48(iV8467))|~cC4(iV8467))|~cC82(iV8467))|~cC14(iV8467))|~cC8(iV8467))|~cC20(iV8467))|~cowlThing(iV8467))|~cC62(iV8467))|~cC34(iV8467))|~cowlThing(iV8471))|~cC80(iV8471))|~cC60(iV8472))|~cowlThing(iV8472))|~cC58(iV8472)),
% 0.11/0.44 inference(NNF_transformation,[status(thm)],[f402])).
% 0.11/0.44 fof(f404,plain,(
% 0.11/0.44 (((((((((((((((((?[X]: ~cowlThing(X))|(?[X]: cowlNothing(X)))|(?[X]: ((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))|~cC10(iV8467))|~cC48(iV8467))|~cC4(iV8467))|~cC82(iV8467))|~cC14(iV8467))|~cC8(iV8467))|~cC20(iV8467))|~cowlThing(iV8467))|~cC62(iV8467))|~cC34(iV8467))|~cowlThing(iV8471))|~cC80(iV8471))|~cC60(iV8472))|~cowlThing(iV8472))|~cC58(iV8472)),
% 0.11/0.44 inference(miniscoping,[status(thm)],[f403])).
% 0.11/0.44 fof(f405,plain,(
% 0.11/0.44 ((((((((((((((((~cowlThing(sK31_skl)|cowlNothing(sK32_skl))|((xsd_string(sK33_skl)|~xsd_integer(sK33_skl))&(~xsd_string(sK33_skl)|xsd_integer(sK33_skl))))|~cC10(iV8467))|~cC48(iV8467))|~cC4(iV8467))|~cC82(iV8467))|~cC14(iV8467))|~cC8(iV8467))|~cC20(iV8467))|~cowlThing(iV8467))|~cC62(iV8467))|~cC34(iV8467))|~cowlThing(iV8471))|~cC80(iV8471))|~cC60(iV8472))|~cowlThing(iV8472))|~cC58(iV8472)),
% 0.11/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK31_skl,sK32_skl,sK33_skl]),skolemize(X,sK31_skl),skolemize(X,sK32_skl),skolemize(X,sK33_skl)],[f404])).
% 0.11/0.44 fof(f406,plain,(
% 0.11/0.44 ~cowlThing(sK31_skl)|cowlNothing(sK32_skl)|xsd_string(sK33_skl)|~xsd_integer(sK33_skl)|~cC10(iV8467)|~cC48(iV8467)|~cC4(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC20(iV8467)|~cowlThing(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cowlThing(iV8471)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)|~cC58(iV8472)),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f405])).
% 0.11/0.44 fof(f407,plain,(
% 0.11/0.44 ~cowlThing(sK31_skl)|cowlNothing(sK32_skl)|~xsd_string(sK33_skl)|xsd_integer(sK33_skl)|~cC10(iV8467)|~cC48(iV8467)|~cC4(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC20(iV8467)|~cowlThing(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cowlThing(iV8471)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)|~cC58(iV8472)),
% 0.11/0.44 inference(cnf_transformation,[status(thm)],[f405])).
% 0.11/0.44 fof(f408,plain,(
% 0.11/0.44 cowlNothing(sK32_skl)|~xsd_string(sK33_skl)|xsd_integer(sK33_skl)|~cC10(iV8467)|~cC48(iV8467)|~cC4(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC20(iV8467)|~cowlThing(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cowlThing(iV8471)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)|~cC58(iV8472)),
% 0.11/0.44 inference(backward_subsumption_resolution,[status(thm)],[f407,f90])).
% 0.11/0.44 fof(f409,plain,(
% 0.11/0.44 cowlNothing(sK32_skl)|xsd_string(sK33_skl)|~xsd_integer(sK33_skl)|~cC10(iV8467)|~cC48(iV8467)|~cC4(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC20(iV8467)|~cowlThing(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cowlThing(iV8471)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)|~cC58(iV8472)),
% 0.11/0.44 inference(backward_subsumption_resolution,[status(thm)],[f406,f90])).
% 0.11/0.44 fof(f410,plain,(
% 0.11/0.44 cowlNothing(sK32_skl)|~xsd_string(sK33_skl)|xsd_integer(sK33_skl)|~cC10(iV8467)|~cC48(iV8467)|~cC4(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC20(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cowlThing(iV8471)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)|~cC58(iV8472)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f408,f90])).
% 0.11/0.44 fof(f411,plain,(
% 0.11/0.44 cowlNothing(sK32_skl)|xsd_string(sK33_skl)|~xsd_integer(sK33_skl)|~cC10(iV8467)|~cC48(iV8467)|~cC4(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC20(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cowlThing(iV8471)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)|~cC58(iV8472)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f409,f90])).
% 0.11/0.44 fof(f414,plain,(
% 0.11/0.44 ~xsd_string(sK33_skl)|xsd_integer(sK33_skl)|~cC10(iV8467)|~cC48(iV8467)|~cC4(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC20(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cowlThing(iV8471)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)|~cC58(iV8472)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f410,f91])).
% 0.11/0.44 fof(f418,plain,(
% 0.11/0.44 ~xsd_string(sK33_skl)|xsd_integer(sK33_skl)|~cC10(iV8467)|~cC48(iV8467)|~cC4(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC20(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)|~cC58(iV8472)),
% 0.11/0.44 inference(resolution,[status(thm)],[f414,f90])).
% 0.11/0.44 fof(f426,plain,(
% 0.11/0.44 xsd_integer(sK33_skl)|~cC10(iV8467)|~cC48(iV8467)|~cC4(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC20(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)|~cC58(iV8472)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f418,f95])).
% 0.11/0.44 fof(f434,plain,(
% 0.11/0.44 xsd_string(sK33_skl)|~xsd_integer(sK33_skl)|~cC10(iV8467)|~cC48(iV8467)|~cC4(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC20(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cowlThing(iV8471)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)|~cC58(iV8472)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f411,f91])).
% 0.11/0.44 fof(f448,plain,(
% 0.11/0.44 xsd_string(sK33_skl)|~xsd_integer(sK33_skl)|~cC10(iV8467)|~cC48(iV8467)|~cC4(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC20(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cowlThing(iV8471)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)),
% 0.11/0.44 inference(backward_subsumption_resolution,[status(thm)],[f434,f252])).
% 0.11/0.44 fof(f450,plain,(
% 0.11/0.44 ~xsd_integer(sK33_skl)|~cC10(iV8467)|~cC48(iV8467)|~cC4(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC20(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cowlThing(iV8471)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f448,f94])).
% 0.11/0.44 fof(f456,plain,(
% 0.11/0.44 ~xsd_integer(sK33_skl)|~cC48(iV8467)|~cC4(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC20(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cowlThing(iV8471)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f450,f100])).
% 0.11/0.44 fof(f466,plain,(
% 0.11/0.44 cC4(iV8467)|cC2(iV8471)),
% 0.11/0.44 inference(resolution,[status(thm)],[f368,f187])).
% 0.11/0.44 fof(f467,plain,(
% 0.11/0.44 cC20(iV8467)|cC2(iV8471)),
% 0.11/0.44 inference(resolution,[status(thm)],[f368,f129])).
% 0.11/0.44 fof(f468,plain,(
% 0.11/0.44 cC4(iV8467)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f466,f384])).
% 0.11/0.44 fof(f469,plain,(
% 0.11/0.44 cC20(iV8467)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f467,f384])).
% 0.11/0.44 fof(f470,plain,(
% 0.11/0.44 ~xsd_integer(sK33_skl)|~cC48(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC20(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cowlThing(iV8471)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)),
% 0.11/0.44 inference(backward_subsumption_resolution,[status(thm)],[f456,f468])).
% 0.11/0.44 fof(f472,plain,(
% 0.11/0.44 ~xsd_integer(sK33_skl)|~cC48(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC20(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f470,f90])).
% 0.11/0.44 fof(f474,plain,(
% 0.11/0.44 cC48(iV8467)|cC2(iV8471)),
% 0.11/0.44 inference(resolution,[status(thm)],[f215,f368])).
% 0.11/0.44 fof(f475,plain,(
% 0.11/0.44 cC48(iV8467)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f474,f384])).
% 0.11/0.44 fof(f477,plain,(
% 0.11/0.44 ~xsd_integer(sK33_skl)|~cC48(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f472,f469])).
% 0.11/0.44 fof(f481,plain,(
% 0.11/0.44 ~xsd_integer(sK33_skl)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)),
% 0.11/0.44 inference(backward_subsumption_resolution,[status(thm)],[f477,f475])).
% 0.11/0.44 fof(f483,plain,(
% 0.11/0.44 ~xsd_integer(sK33_skl)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cC80(iV8471)|~cC60(iV8472)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f481,f90])).
% 0.11/0.44 fof(f489,plain,(
% 0.11/0.44 ![X0]: (cC58(X0)|~rR1(X0,iV8476))),
% 0.11/0.44 inference(resolution,[status(thm)],[f400,f243])).
% 0.11/0.44 fof(f494,plain,(
% 0.11/0.44 ~xsd_integer(sK33_skl)|~cC82(iV8467)|~cC14(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cC80(iV8471)|~cC60(iV8472)|~cC10(iV8467)),
% 0.11/0.44 inference(resolution,[status(thm)],[f483,f99])).
% 0.11/0.44 fof(f522,plain,(
% 0.11/0.44 ~cC10(iV8467)|~cC48(iV8467)|~cC4(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC20(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)|~cC58(iV8472)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f426,f494])).
% 0.11/0.44 fof(f527,plain,(
% 0.11/0.44 ~cC10(iV8467)|~cC48(iV8467)|~cC4(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)|~cC58(iV8472)),
% 0.11/0.44 inference(resolution,[status(thm)],[f522,f469])).
% 0.11/0.44 fof(f535,plain,(
% 0.11/0.44 ~cC48(iV8467)|~cC4(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)|~cC58(iV8472)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f527,f100])).
% 0.11/0.44 fof(f644,plain,(
% 0.11/0.44 cC14(iV8467)|~cTOP(iV8470)),
% 0.11/0.44 inference(resolution,[status(thm)],[f375,f112])).
% 0.11/0.44 fof(f649,plain,(
% 0.11/0.44 cC14(iV8467)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f644,f382])).
% 0.11/0.44 fof(f654,plain,(
% 0.11/0.44 cC58(iV8472)),
% 0.11/0.44 inference(resolution,[status(thm)],[f391,f489])).
% 0.11/0.44 fof(f662,plain,(
% 0.11/0.44 cC60(iV8472)|cC2(iV8472)),
% 0.11/0.44 inference(resolution,[status(thm)],[f654,f254])).
% 0.11/0.44 fof(f663,plain,(
% 0.11/0.44 cC60(iV8472)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f662,f389])).
% 0.11/0.44 fof(f664,plain,(
% 0.11/0.44 ![X0]: (cC62(X0)|~rR1(X0,iV8472))),
% 0.11/0.44 inference(resolution,[status(thm)],[f663,f260])).
% 0.11/0.44 fof(f674,plain,(
% 0.11/0.44 cC62(iV8467)),
% 0.11/0.44 inference(resolution,[status(thm)],[f664,f373])).
% 0.11/0.44 fof(f689,plain,(
% 0.11/0.44 cC34(iV8467)|cC32(iV8474)),
% 0.11/0.44 inference(resolution,[status(thm)],[f169,f374])).
% 0.11/0.44 fof(f698,plain,(
% 0.11/0.44 cC34(iV8467)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f689,f396])).
% 0.11/0.44 fof(f799,plain,(
% 0.11/0.44 ~cC4(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)|~cC58(iV8472)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f535,f475])).
% 0.11/0.44 fof(f806,plain,(
% 0.11/0.44 ~cC4(iV8467)|~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)),
% 0.11/0.44 inference(resolution,[status(thm)],[f799,f654])).
% 0.11/0.44 fof(f812,plain,(
% 0.11/0.44 ~cC82(iV8467)|~cC14(iV8467)|~cC8(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f806,f468])).
% 0.11/0.44 fof(f921,plain,(
% 0.11/0.44 ~cC82(iV8467)|~cC8(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cC80(iV8471)|~cC60(iV8472)|~cowlThing(iV8472)),
% 0.11/0.44 inference(forward_subsumption_resolution,[status(thm)],[f812,f649])).
% 0.11/0.44 fof(f922,plain,(
% 0.11/0.44 ~cC82(iV8467)|~cC8(iV8467)|~cC62(iV8467)|~cC34(iV8467)|~cC80(iV8471)|~cC60(iV8472)),
% 0.11/0.44 inference(resolution,[status(thm)],[f921,f90])).
% 0.11/0.45 fof(f923,plain,(
% 0.11/0.45 ~cC82(iV8467)|~cC8(iV8467)|~cC34(iV8467)|~cC80(iV8471)|~cC60(iV8472)),
% 0.11/0.45 inference(forward_subsumption_resolution,[status(thm)],[f922,f674])).
% 0.11/0.45 fof(f924,plain,(
% 0.11/0.45 ~cC82(iV8467)|~cC8(iV8467)|~cC80(iV8471)|~cC60(iV8472)),
% 0.11/0.45 inference(forward_subsumption_resolution,[status(thm)],[f923,f698])).
% 0.11/0.45 fof(f1108,plain,(
% 0.11/0.45 cC8(iV8467)|cC6(iV8469)),
% 0.11/0.45 inference(resolution,[status(thm)],[f311,f371])).
% 0.11/0.45 fof(f1115,plain,(
% 0.11/0.45 cC8(iV8467)),
% 0.11/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1108,f378])).
% 0.11/0.45 fof(f1127,plain,(
% 0.11/0.45 cC80(iV8471)|cC78(iV8471)),
% 0.11/0.45 inference(resolution,[status(thm)],[f316,f384])).
% 0.11/0.45 fof(f1135,plain,(
% 0.11/0.45 cC80(iV8471)),
% 0.11/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1127,f385])).
% 0.11/0.45 fof(f1136,plain,(
% 0.11/0.45 ~cC82(iV8467)|~cC8(iV8467)|~cC60(iV8472)),
% 0.11/0.45 inference(backward_subsumption_resolution,[status(thm)],[f924,f1135])).
% 0.11/0.45 fof(f1142,plain,(
% 0.11/0.45 ![X0]: (cC82(X0)|~rR1(X0,iV8471))),
% 0.11/0.45 inference(resolution,[status(thm)],[f1135,f322])).
% 0.11/0.45 fof(f1143,plain,(
% 0.11/0.45 ~cC82(iV8467)|~cC8(iV8467)),
% 0.11/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1136,f663])).
% 0.11/0.45 fof(f1180,plain,(
% 0.11/0.45 ~cC82(iV8467)),
% 0.11/0.45 inference(backward_subsumption_resolution,[status(thm)],[f1143,f1115])).
% 0.11/0.45 fof(f1222,plain,(
% 0.11/0.45 cC82(iV8467)),
% 0.11/0.45 inference(resolution,[status(thm)],[f1142,f368])).
% 0.11/0.45 fof(f1223,plain,(
% 0.11/0.45 $false),
% 0.11/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1222,f1180])).
% 0.11/0.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.11/0.47 % Elapsed time: 0.090120 seconds
% 0.11/0.47 % CPU time: 0.477082 seconds
% 0.11/0.47 % Total memory used: 31.740 MB
% 0.11/0.47 % Net memory used: 31.541 MB
%------------------------------------------------------------------------------