%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS155+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 : n014.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.13s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS155+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.09/0.35 % Computer : n014.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 22:55:05 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 0.13/0.40 % Refutation found
% 0.13/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.40 fof(f1,axiom,(
% 0.13/0.40 (! [X] :( cowlThing(X)& ~ cowlNothing(X) ) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f2,axiom,(
% 0.13/0.40 (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f3,axiom,(
% 0.13/0.40 (! [X] :( cC10(X)<=> ( cC4(X)& cC8(X) ) ) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f6,axiom,(
% 0.13/0.40 (! [X] :( cC14(X)<=> (? [Y] :( rR1(X,Y)& cTOP(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f14,axiom,(
% 0.13/0.40 (! [X] :( cC20(X)<=> (? [Y] :( rR1(X,Y)& cC2xcomp(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f15,axiom,(
% 0.13/0.40 (! [X] :( cC20(X)<=> (? [Y0] : ra_Px5(X,Y0) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f16,axiom,(
% 0.13/0.40 (! [X] :( cC20xcomp(X)<=> ~ (? [Y] : ra_Px5(X,Y) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f17,axiom,(
% 0.13/0.40 (! [X] :( cC22(X)<=> (? [Y] :( rR1(X,Y)& cC2xcomp(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f19,axiom,(
% 0.13/0.40 (! [X] :( cC26(X)<=> ( cC24(X)& cC20xcomp(X) ) ) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f30,axiom,(
% 0.13/0.40 (! [X] :( cC34(X)<=> (? [Y] :( rR1(X,Y)& cC32xcomp(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f36,axiom,(
% 0.13/0.40 (! [X] :( cC4(X)<=> (? [Y] :( rR1(X,Y)& cC2xcomp(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f45,axiom,(
% 0.13/0.40 (! [X] :( cC48(X)<=> (? [Y] :( rR1(X,Y)& cC2xcomp(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f58,axiom,(
% 0.13/0.40 (! [X] :( cC58(X)<=> (? [Y] :( rR1(X,Y)& cC2(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f60,axiom,(
% 0.13/0.40 (! [X] :( cC6(X)<=> (? [Y] :( rR1(X,Y)& cC2xcomp(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f62,axiom,(
% 0.13/0.40 (! [X] :( cC60(X)<=> ( cC2xcomp(X)& cC58(X) ) ) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f63,axiom,(
% 0.13/0.40 (! [X] :( cC62(X)<=> (? [Y] :( rR1(X,Y)& cC60(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f66,axiom,(
% 0.13/0.40 (! [X] :( cC64(X)<=> (? [Y] :( rR1(X,Y)& cC2(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f67,axiom,(
% 0.13/0.40 (! [X] :( cC66(X)<=> ( cC2xcomp(X)& cC64(X) ) ) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f68,axiom,(
% 0.13/0.40 (! [X] :( cC68(X)<=> (? [Y] :( rR1(X,Y)& cC66(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f77,axiom,(
% 0.13/0.40 (! [X] :( cC78(X)<=> (? [Y] :( rR1(X,Y)& cC2xcomp(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f80,axiom,(
% 0.13/0.40 (! [X] :( cC8(X)<=> (? [Y] :( rR1(X,Y)& cC6xcomp(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f81,axiom,(
% 0.13/0.40 (! [X] :( cC80(X)<=> ( cC78xcomp(X)& cC2xcomp(X) ) ) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f83,axiom,(
% 0.13/0.40 (! [X] :( cC82(X)<=> (? [Y] :( rR1(X,Y)& cC80(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f104,axiom,(
% 0.13/0.40 rR1(iV8467,iV8471) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f105,axiom,(
% 0.13/0.40 rR1(iV8467,iV8470) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f106,axiom,(
% 0.13/0.40 rR1(iV8467,iV8469) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f107,axiom,(
% 0.13/0.40 rR1(iV8467,iV8474) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f111,axiom,(
% 0.13/0.40 rR1(iV8467,iV8472) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f112,axiom,(
% 0.13/0.40 cC2xcomp(iV8468) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f114,axiom,(
% 0.13/0.40 cC6xcomp(iV8469) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f117,axiom,(
% 0.13/0.40 cTOP(iV8470) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f119,axiom,(
% 0.13/0.40 cC78xcomp(iV8471) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f120,axiom,(
% 0.13/0.40 cC2xcomp(iV8471) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f123,axiom,(
% 0.13/0.40 cC2xcomp(iV8472) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f125,axiom,(
% 0.13/0.40 rR1(iV8472,iV8476) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f126,axiom,(
% 0.13/0.40 cC2xcomp(iV8473) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f128,axiom,(
% 0.13/0.40 cC32xcomp(iV8474) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f131,axiom,(
% 0.13/0.40 cC2xcomp(iV8475) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f133,axiom,(
% 0.13/0.40 cC2(iV8476) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f135,conjecture,(
% 0.13/0.40 ( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& cC20(iV8467)& cC4(iV8467)& cC8(iV8467)& cC82(iV8467)& cC62(iV8467)& cC14(iV8467)& cC34(iV8467)& cC10(iV8467)& cowlThing(iV8467)& cC48(iV8467)& cowlThing(iV8471)& cC80(iV8471)& cC58(iV8472)& cC60(iV8472)& cowlThing(iV8472) ) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f136,negated_conjecture,(
% 0.13/0.40 ~(( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& cC20(iV8467)& cC4(iV8467)& cC8(iV8467)& cC82(iV8467)& cC62(iV8467)& cC14(iV8467)& cC34(iV8467)& cC10(iV8467)& cowlThing(iV8467)& cC48(iV8467)& cowlThing(iV8471)& cC80(iV8471)& cC58(iV8472)& cC60(iV8472)& cowlThing(iV8472) ) )),
% 0.13/0.40 inference(negated_conjecture,[status(cth)],[f135])).
% 0.13/0.40 fof(f137,plain,(
% 0.13/0.40 (![X]: cowlThing(X))&(![X]: ~cowlNothing(X))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f1])).
% 0.13/0.40 fof(f138,plain,(
% 0.13/0.40 ![X0]: (cowlThing(X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f137])).
% 0.13/0.40 fof(f139,plain,(
% 0.13/0.40 ![X0]: (~cowlNothing(X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f137])).
% 0.13/0.40 fof(f140,plain,(
% 0.13/0.40 ![X]: ((~xsd_string(X)|~xsd_integer(X))&(xsd_string(X)|xsd_integer(X)))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f2])).
% 0.13/0.40 fof(f141,plain,(
% 0.13/0.40 (![X]: (~xsd_string(X)|~xsd_integer(X)))&(![X]: (xsd_string(X)|xsd_integer(X)))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f140])).
% 0.13/0.40 fof(f142,plain,(
% 0.13/0.40 ![X0]: (~xsd_string(X0)|~xsd_integer(X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f141])).
% 0.13/0.40 fof(f143,plain,(
% 0.13/0.40 ![X0]: (xsd_string(X0)|xsd_integer(X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f141])).
% 0.13/0.40 fof(f144,plain,(
% 0.13/0.40 ![X]: ((~cC10(X)|(cC4(X)&cC8(X)))&(cC10(X)|(~cC4(X)|~cC8(X))))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f3])).
% 0.13/0.40 fof(f145,plain,(
% 0.13/0.40 (![X]: (~cC10(X)|(cC4(X)&cC8(X))))&(![X]: (cC10(X)|(~cC4(X)|~cC8(X))))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f144])).
% 0.13/0.40 fof(f148,plain,(
% 0.13/0.40 ![X0]: (cC10(X0)|~cC4(X0)|~cC8(X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f145])).
% 0.13/0.40 fof(f161,plain,(
% 0.13/0.40 ![X]: ((~cC14(X)|(?[Y]: (rR1(X,Y)&cTOP(Y))))&(cC14(X)|(![Y]: (~rR1(X,Y)|~cTOP(Y)))))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f6])).
% 0.13/0.40 fof(f162,plain,(
% 0.13/0.40 (![X]: (~cC14(X)|(?[Y]: (rR1(X,Y)&cTOP(Y)))))&(![X]: (cC14(X)|(![Y]: (~rR1(X,Y)|~cTOP(Y)))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f161])).
% 0.13/0.41 fof(f163,plain,(
% 0.13/0.41 (![X]: (~cC14(X)|(rR1(X,sK2_skl(X))&cTOP(sK2_skl(X)))))&(![X]: (cC14(X)|(![Y]: (~rR1(X,Y)|~cTOP(Y)))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Y,sK2_skl(X))],[f162])).
% 0.13/0.41 fof(f166,plain,(
% 0.13/0.41 ![X0,X1]: (cC14(X0)|~rR1(X0,X1)|~cTOP(X1))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f163])).
% 0.13/0.41 fof(f205,plain,(
% 0.13/0.41 ![X]: ((~cC20(X)|(?[Y]: (rR1(X,Y)&cC2xcomp(Y))))&(cC20(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f14])).
% 0.13/0.41 fof(f206,plain,(
% 0.13/0.41 (![X]: (~cC20(X)|(?[Y]: (rR1(X,Y)&cC2xcomp(Y)))))&(![X]: (cC20(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f205])).
% 0.13/0.41 fof(f207,plain,(
% 0.13/0.41 (![X]: (~cC20(X)|(rR1(X,sK9_skl(X))&cC2xcomp(sK9_skl(X)))))&(![X]: (cC20(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(Y,sK9_skl(X))],[f206])).
% 0.13/0.41 fof(f208,plain,(
% 0.13/0.41 ![X0]: (~cC20(X0)|rR1(X0,sK9_skl(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f207])).
% 0.13/0.41 fof(f209,plain,(
% 0.13/0.41 ![X0]: (~cC20(X0)|cC2xcomp(sK9_skl(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f207])).
% 0.13/0.41 fof(f210,plain,(
% 0.13/0.41 ![X0,X1]: (cC20(X0)|~rR1(X0,X1)|~cC2xcomp(X1))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f207])).
% 0.13/0.41 fof(f211,plain,(
% 0.13/0.41 ![X]: ((~cC20(X)|(?[Y0]: ra_Px5(X,Y0)))&(cC20(X)|(![Y0]: ~ra_Px5(X,Y0))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f15])).
% 0.13/0.41 fof(f212,plain,(
% 0.13/0.41 (![X]: (~cC20(X)|(?[Y0]: ra_Px5(X,Y0))))&(![X]: (cC20(X)|(![Y0]: ~ra_Px5(X,Y0))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f211])).
% 0.13/0.41 fof(f213,plain,(
% 0.13/0.41 (![X]: (~cC20(X)|ra_Px5(X,sK10_skl(X))))&(![X]: (cC20(X)|(![Y0]: ~ra_Px5(X,Y0))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(Y0,sK10_skl(X))],[f212])).
% 0.13/0.41 fof(f214,plain,(
% 0.13/0.41 ![X0]: (~cC20(X0)|ra_Px5(X0,sK10_skl(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f213])).
% 0.13/0.41 fof(f216,plain,(
% 0.13/0.41 ![X]: (cC20xcomp(X)<=>(![Y]: ~ra_Px5(X,Y)))),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.13/0.41 fof(f217,plain,(
% 0.13/0.41 ![X]: ((~cC20xcomp(X)|(![Y]: ~ra_Px5(X,Y)))&(cC20xcomp(X)|(?[Y]: ra_Px5(X,Y))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f216])).
% 0.13/0.41 fof(f218,plain,(
% 0.13/0.41 (![X]: (~cC20xcomp(X)|(![Y]: ~ra_Px5(X,Y))))&(![X]: (cC20xcomp(X)|(?[Y]: ra_Px5(X,Y))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f217])).
% 0.13/0.41 fof(f219,plain,(
% 0.13/0.41 (![X]: (~cC20xcomp(X)|(![Y]: ~ra_Px5(X,Y))))&(![X]: (cC20xcomp(X)|ra_Px5(X,sK11_skl(X))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(Y,sK11_skl(X))],[f218])).
% 0.13/0.41 fof(f220,plain,(
% 0.13/0.41 ![X0,X1]: (~cC20xcomp(X0)|~ra_Px5(X0,X1))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f219])).
% 0.13/0.41 fof(f222,plain,(
% 0.13/0.41 ![X]: ((~cC22(X)|(?[Y]: (rR1(X,Y)&cC2xcomp(Y))))&(cC22(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f17])).
% 0.13/0.41 fof(f223,plain,(
% 0.13/0.41 (![X]: (~cC22(X)|(?[Y]: (rR1(X,Y)&cC2xcomp(Y)))))&(![X]: (cC22(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f222])).
% 0.13/0.41 fof(f224,plain,(
% 0.13/0.41 (![X]: (~cC22(X)|(rR1(X,sK12_skl(X))&cC2xcomp(sK12_skl(X)))))&(![X]: (cC22(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(Y,sK12_skl(X))],[f223])).
% 0.13/0.41 fof(f226,plain,(
% 0.13/0.41 ![X0]: (~cC22(X0)|cC2xcomp(sK12_skl(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f224])).
% 0.13/0.41 fof(f227,plain,(
% 0.13/0.41 ![X0,X1]: (cC22(X0)|~rR1(X0,X1)|~cC2xcomp(X1))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f224])).
% 0.13/0.41 fof(f234,plain,(
% 0.13/0.41 ![X]: ((~cC26(X)|(cC24(X)&cC20xcomp(X)))&(cC26(X)|(~cC24(X)|~cC20xcomp(X))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f19])).
% 0.13/0.41 fof(f235,plain,(
% 0.13/0.41 (![X]: (~cC26(X)|(cC24(X)&cC20xcomp(X))))&(![X]: (cC26(X)|(~cC24(X)|~cC20xcomp(X))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f234])).
% 0.13/0.41 fof(f237,plain,(
% 0.13/0.41 ![X0]: (~cC26(X0)|cC20xcomp(X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f235])).
% 0.13/0.41 fof(f294,plain,(
% 0.13/0.41 ![X]: ((~cC34(X)|(?[Y]: (rR1(X,Y)&cC32xcomp(Y))))&(cC34(X)|(![Y]: (~rR1(X,Y)|~cC32xcomp(Y)))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f30])).
% 0.13/0.41 fof(f295,plain,(
% 0.13/0.41 (![X]: (~cC34(X)|(?[Y]: (rR1(X,Y)&cC32xcomp(Y)))))&(![X]: (cC34(X)|(![Y]: (~rR1(X,Y)|~cC32xcomp(Y)))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f294])).
% 0.13/0.41 fof(f296,plain,(
% 0.13/0.41 (![X]: (~cC34(X)|(rR1(X,sK23_skl(X))&cC32xcomp(sK23_skl(X)))))&(![X]: (cC34(X)|(![Y]: (~rR1(X,Y)|~cC32xcomp(Y)))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(Y,sK23_skl(X))],[f295])).
% 0.13/0.41 fof(f299,plain,(
% 0.13/0.41 ![X0,X1]: (cC34(X0)|~rR1(X0,X1)|~cC32xcomp(X1))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f296])).
% 0.13/0.41 fof(f329,plain,(
% 0.13/0.41 ![X]: ((~cC4(X)|(?[Y]: (rR1(X,Y)&cC2xcomp(Y))))&(cC4(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f36])).
% 0.13/0.41 fof(f330,plain,(
% 0.13/0.41 (![X]: (~cC4(X)|(?[Y]: (rR1(X,Y)&cC2xcomp(Y)))))&(![X]: (cC4(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f329])).
% 0.13/0.41 fof(f331,plain,(
% 0.13/0.41 (![X]: (~cC4(X)|(rR1(X,sK29_skl(X))&cC2xcomp(sK29_skl(X)))))&(![X]: (cC4(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(Y,sK29_skl(X))],[f330])).
% 0.13/0.41 fof(f332,plain,(
% 0.13/0.41 ![X0]: (~cC4(X0)|rR1(X0,sK29_skl(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f331])).
% 0.13/0.41 fof(f333,plain,(
% 0.13/0.41 ![X0]: (~cC4(X0)|cC2xcomp(sK29_skl(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f331])).
% 0.13/0.41 fof(f334,plain,(
% 0.13/0.41 ![X0,X1]: (cC4(X0)|~rR1(X0,X1)|~cC2xcomp(X1))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f331])).
% 0.13/0.41 fof(f379,plain,(
% 0.13/0.41 ![X]: ((~cC48(X)|(?[Y]: (rR1(X,Y)&cC2xcomp(Y))))&(cC48(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f45])).
% 0.13/0.41 fof(f380,plain,(
% 0.13/0.41 (![X]: (~cC48(X)|(?[Y]: (rR1(X,Y)&cC2xcomp(Y)))))&(![X]: (cC48(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f379])).
% 0.13/0.41 fof(f381,plain,(
% 0.13/0.41 (![X]: (~cC48(X)|(rR1(X,sK36_skl(X))&cC2xcomp(sK36_skl(X)))))&(![X]: (cC48(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl]),skolemize(Y,sK36_skl(X))],[f380])).
% 0.13/0.41 fof(f382,plain,(
% 0.13/0.41 ![X0]: (~cC48(X0)|rR1(X0,sK36_skl(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f381])).
% 0.13/0.41 fof(f383,plain,(
% 0.13/0.41 ![X0]: (~cC48(X0)|cC2xcomp(sK36_skl(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f381])).
% 0.13/0.41 fof(f384,plain,(
% 0.13/0.41 ![X0,X1]: (cC48(X0)|~rR1(X0,X1)|~cC2xcomp(X1))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f381])).
% 0.13/0.41 fof(f451,plain,(
% 0.13/0.41 ![X]: ((~cC58(X)|(?[Y]: (rR1(X,Y)&cC2(Y))))&(cC58(X)|(![Y]: (~rR1(X,Y)|~cC2(Y)))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f58])).
% 0.13/0.41 fof(f452,plain,(
% 0.13/0.41 (![X]: (~cC58(X)|(?[Y]: (rR1(X,Y)&cC2(Y)))))&(![X]: (cC58(X)|(![Y]: (~rR1(X,Y)|~cC2(Y)))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f451])).
% 0.13/0.41 fof(f453,plain,(
% 0.13/0.41 (![X]: (~cC58(X)|(rR1(X,sK47_skl(X))&cC2(sK47_skl(X)))))&(![X]: (cC58(X)|(![Y]: (~rR1(X,Y)|~cC2(Y)))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl]),skolemize(Y,sK47_skl(X))],[f452])).
% 0.13/0.41 fof(f456,plain,(
% 0.13/0.41 ![X0,X1]: (cC58(X0)|~rR1(X0,X1)|~cC2(X1))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f453])).
% 0.13/0.41 fof(f463,plain,(
% 0.13/0.41 ![X]: ((~cC6(X)|(?[Y]: (rR1(X,Y)&cC2xcomp(Y))))&(cC6(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f60])).
% 0.13/0.41 fof(f464,plain,(
% 0.13/0.41 (![X]: (~cC6(X)|(?[Y]: (rR1(X,Y)&cC2xcomp(Y)))))&(![X]: (cC6(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f463])).
% 0.13/0.41 fof(f465,plain,(
% 0.13/0.41 (![X]: (~cC6(X)|(rR1(X,sK49_skl(X))&cC2xcomp(sK49_skl(X)))))&(![X]: (cC6(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK49_skl]),skolemize(Y,sK49_skl(X))],[f464])).
% 0.13/0.41 fof(f466,plain,(
% 0.13/0.41 ![X0]: (~cC6(X0)|rR1(X0,sK49_skl(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f465])).
% 0.13/0.41 fof(f467,plain,(
% 0.13/0.41 ![X0]: (~cC6(X0)|cC2xcomp(sK49_skl(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f465])).
% 0.13/0.41 fof(f468,plain,(
% 0.13/0.41 ![X0,X1]: (cC6(X0)|~rR1(X0,X1)|~cC2xcomp(X1))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f465])).
% 0.13/0.41 fof(f474,plain,(
% 0.13/0.41 ![X]: ((~cC60(X)|(cC2xcomp(X)&cC58(X)))&(cC60(X)|(~cC2xcomp(X)|~cC58(X))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f62])).
% 0.13/0.41 fof(f475,plain,(
% 0.13/0.41 (![X]: (~cC60(X)|(cC2xcomp(X)&cC58(X))))&(![X]: (cC60(X)|(~cC2xcomp(X)|~cC58(X))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f474])).
% 0.13/0.41 fof(f476,plain,(
% 0.13/0.41 ![X0]: (~cC60(X0)|cC2xcomp(X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f475])).
% 0.13/0.41 fof(f477,plain,(
% 0.13/0.41 ![X0]: (~cC60(X0)|cC58(X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f475])).
% 0.13/0.41 fof(f478,plain,(
% 0.13/0.41 ![X0]: (cC60(X0)|~cC2xcomp(X0)|~cC58(X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f475])).
% 0.13/0.41 fof(f479,plain,(
% 0.13/0.41 ![X]: ((~cC62(X)|(?[Y]: (rR1(X,Y)&cC60(Y))))&(cC62(X)|(![Y]: (~rR1(X,Y)|~cC60(Y)))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f63])).
% 0.13/0.41 fof(f480,plain,(
% 0.13/0.41 (![X]: (~cC62(X)|(?[Y]: (rR1(X,Y)&cC60(Y)))))&(![X]: (cC62(X)|(![Y]: (~rR1(X,Y)|~cC60(Y)))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f479])).
% 0.13/0.41 fof(f481,plain,(
% 0.13/0.41 (![X]: (~cC62(X)|(rR1(X,sK51_skl(X))&cC60(sK51_skl(X)))))&(![X]: (cC62(X)|(![Y]: (~rR1(X,Y)|~cC60(Y)))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK51_skl]),skolemize(Y,sK51_skl(X))],[f480])).
% 0.13/0.41 fof(f483,plain,(
% 0.13/0.41 ![X0]: (~cC62(X0)|cC60(sK51_skl(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f481])).
% 0.13/0.41 fof(f484,plain,(
% 0.13/0.41 ![X0,X1]: (cC62(X0)|~rR1(X0,X1)|~cC60(X1))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f481])).
% 0.13/0.41 fof(f496,plain,(
% 0.13/0.41 ![X]: ((~cC64(X)|(?[Y]: (rR1(X,Y)&cC2(Y))))&(cC64(X)|(![Y]: (~rR1(X,Y)|~cC2(Y)))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f66])).
% 0.13/0.41 fof(f497,plain,(
% 0.13/0.41 (![X]: (~cC64(X)|(?[Y]: (rR1(X,Y)&cC2(Y)))))&(![X]: (cC64(X)|(![Y]: (~rR1(X,Y)|~cC2(Y)))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f496])).
% 0.13/0.41 fof(f498,plain,(
% 0.13/0.41 (![X]: (~cC64(X)|(rR1(X,sK54_skl(X))&cC2(sK54_skl(X)))))&(![X]: (cC64(X)|(![Y]: (~rR1(X,Y)|~cC2(Y)))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK54_skl]),skolemize(Y,sK54_skl(X))],[f497])).
% 0.13/0.41 fof(f501,plain,(
% 0.13/0.41 ![X0,X1]: (cC64(X0)|~rR1(X0,X1)|~cC2(X1))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f498])).
% 0.13/0.41 fof(f502,plain,(
% 0.13/0.41 ![X]: ((~cC66(X)|(cC2xcomp(X)&cC64(X)))&(cC66(X)|(~cC2xcomp(X)|~cC64(X))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f67])).
% 0.13/0.41 fof(f503,plain,(
% 0.13/0.41 (![X]: (~cC66(X)|(cC2xcomp(X)&cC64(X))))&(![X]: (cC66(X)|(~cC2xcomp(X)|~cC64(X))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f502])).
% 0.13/0.41 fof(f504,plain,(
% 0.13/0.41 ![X0]: (~cC66(X0)|cC2xcomp(X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f503])).
% 0.13/0.41 fof(f505,plain,(
% 0.13/0.41 ![X0]: (~cC66(X0)|cC64(X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f503])).
% 0.13/0.41 fof(f506,plain,(
% 0.13/0.41 ![X0]: (cC66(X0)|~cC2xcomp(X0)|~cC64(X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f503])).
% 0.13/0.41 fof(f507,plain,(
% 0.13/0.41 ![X]: ((~cC68(X)|(?[Y]: (rR1(X,Y)&cC66(Y))))&(cC68(X)|(![Y]: (~rR1(X,Y)|~cC66(Y)))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f68])).
% 0.13/0.41 fof(f508,plain,(
% 0.13/0.41 (![X]: (~cC68(X)|(?[Y]: (rR1(X,Y)&cC66(Y)))))&(![X]: (cC68(X)|(![Y]: (~rR1(X,Y)|~cC66(Y)))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f507])).
% 0.13/0.41 fof(f509,plain,(
% 0.13/0.41 (![X]: (~cC68(X)|(rR1(X,sK55_skl(X))&cC66(sK55_skl(X)))))&(![X]: (cC68(X)|(![Y]: (~rR1(X,Y)|~cC66(Y)))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK55_skl]),skolemize(Y,sK55_skl(X))],[f508])).
% 0.13/0.41 fof(f511,plain,(
% 0.13/0.41 ![X0]: (~cC68(X0)|cC66(sK55_skl(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f509])).
% 0.13/0.41 fof(f512,plain,(
% 0.13/0.41 ![X0,X1]: (cC68(X0)|~rR1(X0,X1)|~cC66(X1))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f509])).
% 0.13/0.41 fof(f557,plain,(
% 0.13/0.41 ![X]: ((~cC78(X)|(?[Y]: (rR1(X,Y)&cC2xcomp(Y))))&(cC78(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f77])).
% 0.13/0.41 fof(f558,plain,(
% 0.13/0.41 (![X]: (~cC78(X)|(?[Y]: (rR1(X,Y)&cC2xcomp(Y)))))&(![X]: (cC78(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f557])).
% 0.13/0.41 fof(f559,plain,(
% 0.13/0.41 (![X]: (~cC78(X)|(rR1(X,sK62_skl(X))&cC2xcomp(sK62_skl(X)))))&(![X]: (cC78(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK62_skl]),skolemize(Y,sK62_skl(X))],[f558])).
% 0.13/0.41 fof(f561,plain,(
% 0.13/0.41 ![X0]: (~cC78(X0)|cC2xcomp(sK62_skl(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f559])).
% 0.13/0.41 fof(f562,plain,(
% 0.13/0.41 ![X0,X1]: (cC78(X0)|~rR1(X0,X1)|~cC2xcomp(X1))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f559])).
% 0.13/0.41 fof(f574,plain,(
% 0.13/0.41 ![X]: ((~cC8(X)|(?[Y]: (rR1(X,Y)&cC6xcomp(Y))))&(cC8(X)|(![Y]: (~rR1(X,Y)|~cC6xcomp(Y)))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f80])).
% 0.13/0.41 fof(f575,plain,(
% 0.13/0.41 (![X]: (~cC8(X)|(?[Y]: (rR1(X,Y)&cC6xcomp(Y)))))&(![X]: (cC8(X)|(![Y]: (~rR1(X,Y)|~cC6xcomp(Y)))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f574])).
% 0.13/0.41 fof(f576,plain,(
% 0.13/0.41 (![X]: (~cC8(X)|(rR1(X,sK65_skl(X))&cC6xcomp(sK65_skl(X)))))&(![X]: (cC8(X)|(![Y]: (~rR1(X,Y)|~cC6xcomp(Y)))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK65_skl]),skolemize(Y,sK65_skl(X))],[f575])).
% 0.13/0.41 fof(f579,plain,(
% 0.13/0.41 ![X0,X1]: (cC8(X0)|~rR1(X0,X1)|~cC6xcomp(X1))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f576])).
% 0.13/0.41 fof(f580,plain,(
% 0.13/0.41 ![X]: ((~cC80(X)|(cC78xcomp(X)&cC2xcomp(X)))&(cC80(X)|(~cC78xcomp(X)|~cC2xcomp(X))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f81])).
% 0.13/0.41 fof(f581,plain,(
% 0.13/0.41 (![X]: (~cC80(X)|(cC78xcomp(X)&cC2xcomp(X))))&(![X]: (cC80(X)|(~cC78xcomp(X)|~cC2xcomp(X))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f580])).
% 0.13/0.41 fof(f584,plain,(
% 0.13/0.41 ![X0]: (cC80(X0)|~cC78xcomp(X0)|~cC2xcomp(X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f581])).
% 0.13/0.41 fof(f591,plain,(
% 0.13/0.41 ![X]: ((~cC82(X)|(?[Y]: (rR1(X,Y)&cC80(Y))))&(cC82(X)|(![Y]: (~rR1(X,Y)|~cC80(Y)))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f83])).
% 0.13/0.41 fof(f592,plain,(
% 0.13/0.41 (![X]: (~cC82(X)|(?[Y]: (rR1(X,Y)&cC80(Y)))))&(![X]: (cC82(X)|(![Y]: (~rR1(X,Y)|~cC80(Y)))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f591])).
% 0.13/0.41 fof(f593,plain,(
% 0.13/0.41 (![X]: (~cC82(X)|(rR1(X,sK67_skl(X))&cC80(sK67_skl(X)))))&(![X]: (cC82(X)|(![Y]: (~rR1(X,Y)|~cC80(Y)))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK67_skl]),skolemize(Y,sK67_skl(X))],[f592])).
% 0.13/0.41 fof(f596,plain,(
% 0.13/0.41 ![X0,X1]: (cC82(X0)|~rR1(X0,X1)|~cC80(X1))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f593])).
% 0.13/0.41 fof(f680,plain,(
% 0.13/0.41 rR1(iV8467,iV8471)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f104])).
% 0.13/0.41 fof(f681,plain,(
% 0.13/0.41 rR1(iV8467,iV8470)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f105])).
% 0.13/0.41 fof(f682,plain,(
% 0.13/0.41 rR1(iV8467,iV8469)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f106])).
% 0.13/0.41 fof(f683,plain,(
% 0.13/0.41 rR1(iV8467,iV8474)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f107])).
% 0.13/0.41 fof(f687,plain,(
% 0.13/0.41 rR1(iV8467,iV8472)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f111])).
% 0.13/0.41 fof(f688,plain,(
% 0.13/0.41 cC2xcomp(iV8468)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f112])).
% 0.13/0.41 fof(f690,plain,(
% 0.13/0.41 cC6xcomp(iV8469)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f114])).
% 0.13/0.41 fof(f694,plain,(
% 0.13/0.41 cTOP(iV8470)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f117])).
% 0.13/0.41 fof(f696,plain,(
% 0.13/0.41 cC78xcomp(iV8471)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f119])).
% 0.13/0.41 fof(f697,plain,(
% 0.13/0.41 cC2xcomp(iV8471)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f120])).
% 0.13/0.41 fof(f701,plain,(
% 0.13/0.41 cC2xcomp(iV8472)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f123])).
% 0.13/0.41 fof(f703,plain,(
% 0.13/0.41 rR1(iV8472,iV8476)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f125])).
% 0.13/0.41 fof(f704,plain,(
% 0.13/0.41 cC2xcomp(iV8473)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f126])).
% 0.13/0.41 fof(f706,plain,(
% 0.13/0.41 cC32xcomp(iV8474)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f128])).
% 0.13/0.41 fof(f710,plain,(
% 0.13/0.41 cC2xcomp(iV8475)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f131])).
% 0.13/0.41 fof(f712,plain,(
% 0.13/0.41 cC2(iV8476)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f133])).
% 0.13/0.41 fof(f714,plain,(
% 0.13/0.41 (((((((((((((((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: (xsd_string(X)<~>~xsd_integer(X))))|~cC20(iV8467))|~cC4(iV8467))|~cC8(iV8467))|~cC82(iV8467))|~cC62(iV8467))|~cC14(iV8467))|~cC34(iV8467))|~cC10(iV8467))|~cowlThing(iV8467))|~cC48(iV8467))|~cowlThing(iV8471))|~cC80(iV8471))|~cC58(iV8472))|~cC60(iV8472))|~cowlThing(iV8472))),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f136])).
% 0.13/0.41 fof(f715,plain,(
% 0.13/0.41 ((((((((((((((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: ((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))|~cC20(iV8467))|~cC4(iV8467))|~cC8(iV8467))|~cC82(iV8467))|~cC62(iV8467))|~cC14(iV8467))|~cC34(iV8467))|~cC10(iV8467))|~cowlThing(iV8467))|~cC48(iV8467))|~cowlThing(iV8471))|~cC80(iV8471))|~cC58(iV8472))|~cC60(iV8472))|~cowlThing(iV8472)),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f714])).
% 0.13/0.41 fof(f716,plain,(
% 0.13/0.41 (((((((((((((((((?[X]: ~cowlThing(X))|(?[X]: cowlNothing(X)))|(?[X]: ((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))|~cC20(iV8467))|~cC4(iV8467))|~cC8(iV8467))|~cC82(iV8467))|~cC62(iV8467))|~cC14(iV8467))|~cC34(iV8467))|~cC10(iV8467))|~cowlThing(iV8467))|~cC48(iV8467))|~cowlThing(iV8471))|~cC80(iV8471))|~cC58(iV8472))|~cC60(iV8472))|~cowlThing(iV8472)),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f715])).
% 0.13/0.41 fof(f717,plain,(
% 0.13/0.41 ((((((((((((((((~cowlThing(sK79_skl)|cowlNothing(sK80_skl))|((xsd_string(sK81_skl)|~xsd_integer(sK81_skl))&(~xsd_string(sK81_skl)|xsd_integer(sK81_skl))))|~cC20(iV8467))|~cC4(iV8467))|~cC8(iV8467))|~cC82(iV8467))|~cC62(iV8467))|~cC14(iV8467))|~cC34(iV8467))|~cC10(iV8467))|~cowlThing(iV8467))|~cC48(iV8467))|~cowlThing(iV8471))|~cC80(iV8471))|~cC58(iV8472))|~cC60(iV8472))|~cowlThing(iV8472)),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK79_skl,sK80_skl,sK81_skl]),skolemize(X,sK79_skl),skolemize(X,sK80_skl),skolemize(X,sK81_skl)],[f716])).
% 0.13/0.41 fof(f718,plain,(
% 0.13/0.41 ~cowlThing(sK79_skl)|cowlNothing(sK80_skl)|xsd_string(sK81_skl)|~xsd_integer(sK81_skl)|~cC20(iV8467)|~cC4(iV8467)|~cC8(iV8467)|~cC82(iV8467)|~cC62(iV8467)|~cC14(iV8467)|~cC34(iV8467)|~cC10(iV8467)|~cowlThing(iV8467)|~cC48(iV8467)|~cowlThing(iV8471)|~cC80(iV8471)|~cC58(iV8472)|~cC60(iV8472)|~cowlThing(iV8472)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f717])).
% 0.13/0.41 fof(f719,plain,(
% 0.13/0.41 ~cowlThing(sK79_skl)|cowlNothing(sK80_skl)|~xsd_string(sK81_skl)|xsd_integer(sK81_skl)|~cC20(iV8467)|~cC4(iV8467)|~cC8(iV8467)|~cC82(iV8467)|~cC62(iV8467)|~cC14(iV8467)|~cC34(iV8467)|~cC10(iV8467)|~cowlThing(iV8467)|~cC48(iV8467)|~cowlThing(iV8471)|~cC80(iV8471)|~cC58(iV8472)|~cC60(iV8472)|~cowlThing(iV8472)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f717])).
% 0.13/0.41 fof(f720,definition,(
% 0.13/0.41 sQ0_spl <=> (cowlThing(sK79_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f722,plain,(
% 0.13/0.41 ~cowlThing(sK79_skl)|sQ0_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f720])).
% 0.13/0.41 fof(f723,definition,(
% 0.13/0.41 sQ1_spl <=> (cowlNothing(sK80_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f724,plain,(
% 0.13/0.41 cowlNothing(sK80_skl)|~sQ1_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f723])).
% 0.13/0.41 fof(f726,definition,(
% 0.13/0.41 sQ2_spl <=> (xsd_string(sK81_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f727,plain,(
% 0.13/0.41 xsd_string(sK81_skl)|~sQ2_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f726])).
% 0.13/0.41 fof(f729,definition,(
% 0.13/0.41 sQ3_spl <=> (xsd_integer(sK81_skl))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f730,plain,(
% 0.13/0.41 xsd_integer(sK81_skl)|~sQ3_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f729])).
% 0.13/0.41 fof(f731,plain,(
% 0.13/0.41 ~xsd_integer(sK81_skl)|sQ3_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f729])).
% 0.13/0.41 fof(f732,definition,(
% 0.13/0.41 sQ4_spl <=> (cC20(iV8467))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f733,plain,(
% 0.13/0.41 cC20(iV8467)|~sQ4_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f732])).
% 0.13/0.41 fof(f735,definition,(
% 0.13/0.41 sQ5_spl <=> (cC4(iV8467))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f736,plain,(
% 0.13/0.41 cC4(iV8467)|~sQ5_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f735])).
% 0.13/0.41 fof(f738,definition,(
% 0.13/0.41 sQ6_spl <=> (cC8(iV8467))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f740,plain,(
% 0.13/0.41 ~cC8(iV8467)|sQ6_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f738])).
% 0.13/0.41 fof(f741,definition,(
% 0.13/0.41 sQ7_spl <=> (cC82(iV8467))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f743,plain,(
% 0.13/0.41 ~cC82(iV8467)|sQ7_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f741])).
% 0.13/0.41 fof(f744,definition,(
% 0.13/0.41 sQ8_spl <=> (cC62(iV8467))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f746,plain,(
% 0.13/0.41 ~cC62(iV8467)|sQ8_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f744])).
% 0.13/0.41 fof(f747,definition,(
% 0.13/0.41 sQ9_spl <=> (cC14(iV8467))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f749,plain,(
% 0.13/0.41 ~cC14(iV8467)|sQ9_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f747])).
% 0.13/0.41 fof(f750,definition,(
% 0.13/0.41 sQ10_spl <=> (cC34(iV8467))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f752,plain,(
% 0.13/0.41 ~cC34(iV8467)|sQ10_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f750])).
% 0.13/0.41 fof(f753,definition,(
% 0.13/0.41 sQ11_spl <=> (cC10(iV8467))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f756,definition,(
% 0.13/0.41 sQ12_spl <=> (cowlThing(iV8467))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f758,plain,(
% 0.13/0.41 ~cowlThing(iV8467)|sQ12_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f756])).
% 0.13/0.41 fof(f759,definition,(
% 0.13/0.41 sQ13_spl <=> (cC48(iV8467))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f760,plain,(
% 0.13/0.41 cC48(iV8467)|~sQ13_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f759])).
% 0.13/0.41 fof(f762,definition,(
% 0.13/0.41 sQ14_spl <=> (cowlThing(iV8471))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f764,plain,(
% 0.13/0.41 ~cowlThing(iV8471)|sQ14_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f762])).
% 0.13/0.41 fof(f765,definition,(
% 0.13/0.41 sQ15_spl <=> (cC80(iV8471))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f766,plain,(
% 0.13/0.41 cC80(iV8471)|~sQ15_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f765])).
% 0.13/0.41 fof(f768,definition,(
% 0.13/0.41 sQ16_spl <=> (cC58(iV8472))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f770,plain,(
% 0.13/0.41 ~cC58(iV8472)|sQ16_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f768])).
% 0.13/0.41 fof(f771,definition,(
% 0.13/0.41 sQ17_spl <=> (cC60(iV8472))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f772,plain,(
% 0.13/0.41 cC60(iV8472)|~sQ17_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f771])).
% 0.13/0.41 fof(f774,definition,(
% 0.13/0.41 sQ18_spl <=> (cowlThing(iV8472))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f776,plain,(
% 0.13/0.41 ~cowlThing(iV8472)|sQ18_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f774])).
% 0.13/0.41 fof(f777,plain,(
% 0.13/0.41 ~sQ0_spl|sQ1_spl|sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|~sQ16_spl|~sQ17_spl|~sQ18_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f718,f720,f723,f726,f729,f732,f735,f738,f741,f744,f747,f750,f753,f756,f759,f762,f765,f768,f771,f774])).
% 0.13/0.41 fof(f778,plain,(
% 0.13/0.41 ~sQ0_spl|sQ1_spl|~sQ2_spl|sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|~sQ16_spl|~sQ17_spl|~sQ18_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f719,f720,f723,f726,f729,f732,f735,f738,f741,f744,f747,f750,f753,f756,f759,f762,f765,f768,f771,f774])).
% 0.13/0.41 fof(f779,plain,(
% 0.13/0.41 $false|sQ18_spl),
% 0.13/0.41 inference(backward_subsumption_resolution,[status(thm)],[f776,f138])).
% 0.13/0.41 fof(f780,plain,(
% 0.13/0.41 sQ18_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f779])).
% 0.13/0.41 fof(f784,definition,(
% 0.13/0.41 sQ19_spl <=> (cC2xcomp(iV8471))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f786,plain,(
% 0.13/0.41 ~cC2xcomp(iV8471)|sQ19_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f784])).
% 0.13/0.41 fof(f788,plain,(
% 0.13/0.41 cC20(iV8467)|~cC2xcomp(iV8472)),
% 0.13/0.41 inference(resolution,[status(thm)],[f687,f210])).
% 0.13/0.41 fof(f789,definition,(
% 0.13/0.41 sQ20_spl <=> (cC2xcomp(iV8472))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f791,plain,(
% 0.13/0.41 ~cC2xcomp(iV8472)|sQ20_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f789])).
% 0.13/0.41 fof(f792,plain,(
% 0.13/0.41 sQ4_spl|~sQ20_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f788,f732,f789])).
% 0.13/0.41 fof(f793,plain,(
% 0.13/0.41 $false|sQ20_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f791,f701])).
% 0.13/0.41 fof(f794,plain,(
% 0.13/0.41 sQ20_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f793])).
% 0.13/0.41 fof(f799,plain,(
% 0.13/0.41 $false|sQ19_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f786,f697])).
% 0.13/0.41 fof(f800,plain,(
% 0.13/0.41 sQ19_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f799])).
% 0.13/0.41 fof(f806,plain,(
% 0.13/0.41 ![X0]: (cC58(X0)|~rR1(X0,iV8476))),
% 0.13/0.41 inference(resolution,[status(thm)],[f712,f456])).
% 0.13/0.41 fof(f808,plain,(
% 0.13/0.41 ![X0]: (cC14(X0)|~rR1(X0,iV8470))),
% 0.13/0.41 inference(resolution,[status(thm)],[f166,f694])).
% 0.13/0.41 fof(f840,definition,(
% 0.13/0.41 sQ24_spl <=> (cC2xcomp(iV8468))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f842,plain,(
% 0.13/0.41 ~cC2xcomp(iV8468)|sQ24_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f840])).
% 0.13/0.41 fof(f846,plain,(
% 0.13/0.41 $false|sQ24_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f842,f688])).
% 0.13/0.41 fof(f847,plain,(
% 0.13/0.41 sQ24_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f846])).
% 0.13/0.41 fof(f851,definition,(
% 0.13/0.41 sQ25_spl <=> (cC2xcomp(iV8473))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f853,plain,(
% 0.13/0.41 ~cC2xcomp(iV8473)|sQ25_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f851])).
% 0.13/0.41 fof(f857,plain,(
% 0.13/0.41 $false|sQ25_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f853,f704])).
% 0.13/0.41 fof(f858,plain,(
% 0.13/0.41 sQ25_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f857])).
% 0.13/0.41 fof(f862,definition,(
% 0.13/0.41 sQ26_spl <=> (cC2xcomp(iV8475))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f864,plain,(
% 0.13/0.41 ~cC2xcomp(iV8475)|sQ26_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f862])).
% 0.13/0.41 fof(f868,plain,(
% 0.13/0.41 $false|sQ26_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f864,f710])).
% 0.13/0.41 fof(f869,plain,(
% 0.13/0.41 sQ26_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f868])).
% 0.13/0.41 fof(f870,plain,(
% 0.13/0.41 cC58(iV8472)),
% 0.13/0.41 inference(resolution,[status(thm)],[f703,f806])).
% 0.13/0.41 fof(f889,plain,(
% 0.13/0.41 cC60(iV8472)|~cC2xcomp(iV8472)),
% 0.13/0.41 inference(resolution,[status(thm)],[f870,f478])).
% 0.13/0.41 fof(f890,plain,(
% 0.13/0.41 sQ17_spl|~sQ20_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f889,f771,f789])).
% 0.13/0.41 fof(f891,plain,(
% 0.13/0.41 $false|sQ16_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f770,f870])).
% 0.13/0.41 fof(f892,plain,(
% 0.13/0.41 sQ16_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f891])).
% 0.13/0.41 fof(f893,plain,(
% 0.13/0.41 ![X0]: (cC62(X0)|~rR1(X0,iV8472)|~sQ17_spl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f772,f484])).
% 0.13/0.41 fof(f900,plain,(
% 0.13/0.41 cC62(iV8467)|~sQ17_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f893,f687])).
% 0.13/0.41 fof(f929,plain,(
% 0.13/0.41 $false|sQ14_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f764,f138])).
% 0.13/0.41 fof(f930,plain,(
% 0.13/0.41 sQ14_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f929])).
% 0.13/0.41 fof(f931,plain,(
% 0.13/0.41 $false|sQ12_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f758,f138])).
% 0.13/0.41 fof(f932,plain,(
% 0.13/0.41 sQ12_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f931])).
% 0.13/0.41 fof(f933,plain,(
% 0.13/0.41 $false|~sQ17_spl|sQ8_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f746,f900])).
% 0.13/0.41 fof(f934,plain,(
% 0.13/0.41 ~sQ17_spl|sQ8_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f933])).
% 0.13/0.41 fof(f935,plain,(
% 0.13/0.41 $false|~sQ1_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f724,f139])).
% 0.13/0.41 fof(f936,plain,(
% 0.13/0.41 ~sQ1_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f935])).
% 0.13/0.41 fof(f937,plain,(
% 0.13/0.41 $false|sQ0_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f722,f138])).
% 0.13/0.41 fof(f938,plain,(
% 0.13/0.41 sQ0_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f937])).
% 0.13/0.41 fof(f947,plain,(
% 0.13/0.41 rR1(iV8467,sK9_skl(iV8467))|~sQ4_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f208,f733])).
% 0.13/0.41 fof(f948,plain,(
% 0.13/0.41 ra_Px5(iV8467,sK10_skl(iV8467))|~sQ4_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f214,f733])).
% 0.13/0.41 fof(f949,plain,(
% 0.13/0.41 cC48(iV8467)|~cC2xcomp(sK9_skl(iV8467))|~sQ4_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f947,f384])).
% 0.13/0.41 fof(f952,definition,(
% 0.13/0.41 sQ33_spl <=> (cC2xcomp(sK9_skl(iV8467)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f954,plain,(
% 0.13/0.41 ~cC2xcomp(sK9_skl(iV8467))|sQ33_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f952])).
% 0.13/0.41 fof(f955,plain,(
% 0.13/0.41 sQ13_spl|~sQ33_spl|~sQ4_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f949,f759,f952,f732])).
% 0.13/0.41 fof(f958,plain,(
% 0.13/0.41 ~cC20(iV8467)|sQ33_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f954,f209])).
% 0.13/0.41 fof(f960,plain,(
% 0.13/0.41 $false|~sQ4_spl|sQ33_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f958,f733])).
% 0.13/0.41 fof(f961,plain,(
% 0.13/0.41 ~sQ4_spl|sQ33_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f960])).
% 0.13/0.41 fof(f982,plain,(
% 0.13/0.41 ![X0]: (cC22(X0)|~rR1(X0,iV8472))),
% 0.13/0.41 inference(resolution,[status(thm)],[f227,f701])).
% 0.13/0.41 fof(f985,plain,(
% 0.13/0.41 cC22(iV8467)),
% 0.13/0.41 inference(resolution,[status(thm)],[f982,f687])).
% 0.13/0.41 fof(f991,definition,(
% 0.13/0.41 sQ34_spl <=> (cC2xcomp(sK12_skl(iV8467)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f993,plain,(
% 0.13/0.41 ~cC2xcomp(sK12_skl(iV8467))|sQ34_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f991])).
% 0.13/0.41 fof(f997,plain,(
% 0.13/0.41 ~cC22(iV8467)|sQ34_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f993,f226])).
% 0.13/0.41 fof(f999,plain,(
% 0.13/0.41 $false|sQ34_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f997,f985])).
% 0.13/0.41 fof(f1000,plain,(
% 0.13/0.41 sQ34_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f999])).
% 0.13/0.41 fof(f1014,plain,(
% 0.13/0.41 cC60(sK51_skl(iV8467))|~sQ17_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f483,f900])).
% 0.13/0.41 fof(f1016,plain,(
% 0.13/0.41 cC58(sK51_skl(iV8467))|~sQ17_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f1014,f477])).
% 0.13/0.41 fof(f1017,plain,(
% 0.13/0.41 cC2xcomp(sK51_skl(iV8467))|~sQ17_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f1014,f476])).
% 0.13/0.41 fof(f1018,plain,(
% 0.13/0.41 cC60(sK51_skl(iV8467))|~cC2xcomp(sK51_skl(iV8467))|~sQ17_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f1016,f478])).
% 0.13/0.41 fof(f1019,definition,(
% 0.13/0.41 sQ35_spl <=> (cC60(sK51_skl(iV8467)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f1022,definition,(
% 0.13/0.41 sQ36_spl <=> (cC2xcomp(sK51_skl(iV8467)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f1024,plain,(
% 0.13/0.41 ~cC2xcomp(sK51_skl(iV8467))|sQ36_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f1022])).
% 0.13/0.41 fof(f1025,plain,(
% 0.13/0.41 sQ35_spl|~sQ36_spl|~sQ17_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f1018,f1019,f1022,f771])).
% 0.13/0.41 fof(f1031,plain,(
% 0.13/0.41 cC14(iV8467)),
% 0.13/0.41 inference(resolution,[status(thm)],[f808,f681])).
% 0.13/0.41 fof(f1035,plain,(
% 0.13/0.41 ![X0]: (cC34(X0)|~rR1(X0,iV8474))),
% 0.13/0.41 inference(resolution,[status(thm)],[f299,f706])).
% 0.13/0.41 fof(f1074,plain,(
% 0.13/0.41 cC34(iV8467)),
% 0.13/0.41 inference(resolution,[status(thm)],[f1035,f683])).
% 0.13/0.41 fof(f1079,plain,(
% 0.13/0.41 rR1(iV8467,sK29_skl(iV8467))|~sQ5_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f332,f736])).
% 0.13/0.41 fof(f1084,definition,(
% 0.13/0.41 sQ38_spl <=> (cC2xcomp(sK29_skl(iV8467)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f1086,plain,(
% 0.13/0.41 ~cC2xcomp(sK29_skl(iV8467))|sQ38_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f1084])).
% 0.13/0.41 fof(f1090,plain,(
% 0.13/0.41 ~cC4(iV8467)|sQ38_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f1086,f333])).
% 0.13/0.41 fof(f1092,plain,(
% 0.13/0.41 $false|~sQ5_spl|sQ38_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1090,f736])).
% 0.13/0.41 fof(f1093,plain,(
% 0.13/0.41 ~sQ5_spl|sQ38_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f1092])).
% 0.13/0.41 fof(f1220,plain,(
% 0.13/0.41 rR1(iV8467,sK36_skl(iV8467))|~sQ13_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f382,f760])).
% 0.13/0.41 fof(f1235,plain,(
% 0.13/0.41 cC4(iV8467)|~cC2xcomp(sK36_skl(iV8467))|~sQ13_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f1220,f334])).
% 0.13/0.41 fof(f1237,definition,(
% 0.13/0.41 sQ46_spl <=> (cC2xcomp(sK36_skl(iV8467)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f1239,plain,(
% 0.13/0.41 ~cC2xcomp(sK36_skl(iV8467))|sQ46_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f1237])).
% 0.13/0.41 fof(f1241,plain,(
% 0.13/0.41 sQ5_spl|~sQ46_spl|~sQ13_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f1235,f735,f1237,f759])).
% 0.13/0.41 fof(f1243,plain,(
% 0.13/0.41 ~cC48(iV8467)|sQ46_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f1239,f383])).
% 0.13/0.41 fof(f1245,plain,(
% 0.13/0.41 $false|~sQ13_spl|sQ46_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1243,f760])).
% 0.13/0.41 fof(f1246,plain,(
% 0.13/0.41 ~sQ13_spl|sQ46_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f1245])).
% 0.13/0.41 fof(f1399,plain,(
% 0.13/0.41 cC6(iV8467)|~cC2xcomp(sK29_skl(iV8467))|~sQ5_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f468,f1079])).
% 0.13/0.41 fof(f1424,definition,(
% 0.13/0.41 sQ57_spl <=> (cC6(iV8467))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f1425,plain,(
% 0.13/0.41 cC6(iV8467)|~sQ57_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f1424])).
% 0.13/0.41 fof(f1429,plain,(
% 0.13/0.41 sQ57_spl|~sQ38_spl|~sQ5_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f1399,f1424,f1084,f735])).
% 0.13/0.41 fof(f1442,plain,(
% 0.13/0.41 rR1(iV8467,sK49_skl(iV8467))|~sQ57_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f1425,f466])).
% 0.13/0.41 fof(f1443,plain,(
% 0.13/0.41 cC2xcomp(sK49_skl(iV8467))|~sQ57_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f1425,f467])).
% 0.13/0.41 fof(f1452,definition,(
% 0.13/0.41 sQ58_spl <=> (cC2xcomp(sK49_skl(iV8467)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f1454,plain,(
% 0.13/0.41 ~cC2xcomp(sK49_skl(iV8467))|sQ58_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f1452])).
% 0.13/0.41 fof(f1480,plain,(
% 0.13/0.41 $false|~sQ57_spl|sQ58_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1454,f1443])).
% 0.13/0.41 fof(f1481,plain,(
% 0.13/0.41 ~sQ57_spl|sQ58_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f1480])).
% 0.13/0.41 fof(f1500,plain,(
% 0.13/0.41 $false|~sQ17_spl|sQ36_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1024,f1017])).
% 0.13/0.41 fof(f1501,plain,(
% 0.13/0.41 ~sQ17_spl|sQ36_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f1500])).
% 0.13/0.41 fof(f1557,plain,(
% 0.13/0.41 ![X0]: (cC64(X0)|~rR1(X0,iV8476))),
% 0.13/0.41 inference(resolution,[status(thm)],[f501,f712])).
% 0.13/0.41 fof(f1578,plain,(
% 0.13/0.41 cC64(iV8472)),
% 0.13/0.41 inference(resolution,[status(thm)],[f1557,f703])).
% 0.13/0.41 fof(f1579,plain,(
% 0.13/0.41 cC66(iV8472)|~cC2xcomp(iV8472)),
% 0.13/0.41 inference(resolution,[status(thm)],[f1578,f506])).
% 0.13/0.41 fof(f1582,definition,(
% 0.13/0.41 sQ61_spl <=> (cC66(iV8472))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f1583,plain,(
% 0.13/0.41 cC66(iV8472)|~sQ61_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f1582])).
% 0.13/0.41 fof(f1585,plain,(
% 0.13/0.41 sQ61_spl|~sQ20_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f1579,f1582,f789])).
% 0.13/0.41 fof(f1615,plain,(
% 0.13/0.41 ![X0]: (cC68(X0)|~rR1(X0,iV8472)|~sQ61_spl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f512,f1583])).
% 0.13/0.41 fof(f1732,plain,(
% 0.13/0.41 cC68(iV8467)|~sQ61_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f1615,f687])).
% 0.13/0.41 fof(f1735,plain,(
% 0.13/0.41 cC66(sK55_skl(iV8467))|~sQ61_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f1732,f511])).
% 0.13/0.41 fof(f1737,plain,(
% 0.13/0.41 cC64(sK55_skl(iV8467))|~sQ61_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f1735,f505])).
% 0.13/0.41 fof(f1738,plain,(
% 0.13/0.41 cC2xcomp(sK55_skl(iV8467))|~sQ61_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f1735,f504])).
% 0.13/0.41 fof(f1739,plain,(
% 0.13/0.41 cC66(sK55_skl(iV8467))|~cC2xcomp(sK55_skl(iV8467))|~sQ61_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f1737,f506])).
% 0.13/0.41 fof(f1742,definition,(
% 0.13/0.41 sQ66_spl <=> (cC66(sK55_skl(iV8467)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f1745,definition,(
% 0.13/0.41 sQ67_spl <=> (cC2xcomp(sK55_skl(iV8467)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f1747,plain,(
% 0.13/0.41 ~cC2xcomp(sK55_skl(iV8467))|sQ67_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f1745])).
% 0.13/0.41 fof(f1748,plain,(
% 0.13/0.41 sQ66_spl|~sQ67_spl|~sQ61_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f1739,f1742,f1745,f1582])).
% 0.13/0.41 fof(f1754,definition,(
% 0.13/0.41 sQ68_spl <=> (cC26(iV8467))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f1755,plain,(
% 0.13/0.41 cC26(iV8467)|~sQ68_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f1754])).
% 0.13/0.41 fof(f1793,plain,(
% 0.13/0.41 cC20xcomp(iV8467)|~sQ68_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f1755,f237])).
% 0.13/0.41 fof(f1795,plain,(
% 0.13/0.41 ![X0]: (~ra_Px5(iV8467,X0)|~sQ68_spl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f1793,f220])).
% 0.13/0.41 fof(f1796,plain,(
% 0.13/0.41 $false|~sQ68_spl|~sQ4_spl),
% 0.13/0.41 inference(backward_subsumption_resolution,[status(thm)],[f948,f1795])).
% 0.13/0.41 fof(f1798,plain,(
% 0.13/0.41 ~sQ68_spl|~sQ4_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f1796])).
% 0.13/0.41 fof(f1824,plain,(
% 0.13/0.41 $false|~sQ61_spl|sQ67_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1747,f1738])).
% 0.13/0.41 fof(f1825,plain,(
% 0.13/0.41 ~sQ61_spl|sQ67_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f1824])).
% 0.13/0.41 fof(f1854,plain,(
% 0.13/0.41 ![X0]: (cC78(X0)|~rR1(X0,sK49_skl(iV8467))|~sQ57_spl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f562,f1443])).
% 0.13/0.41 fof(f1880,plain,(
% 0.13/0.41 cC78(iV8467)|~sQ57_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f1854,f1442])).
% 0.13/0.41 fof(f1883,plain,(
% 0.13/0.41 cC2xcomp(sK62_skl(iV8467))|~sQ57_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f1880,f561])).
% 0.13/0.41 fof(f1903,definition,(
% 0.13/0.41 sQ74_spl <=> (cC2xcomp(sK62_skl(iV8467)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f1905,plain,(
% 0.13/0.41 ~cC2xcomp(sK62_skl(iV8467))|sQ74_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f1903])).
% 0.13/0.41 fof(f1910,plain,(
% 0.13/0.41 $false|~sQ57_spl|sQ74_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1905,f1883])).
% 0.13/0.41 fof(f1911,plain,(
% 0.13/0.41 ~sQ57_spl|sQ74_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f1910])).
% 0.13/0.41 fof(f1917,plain,(
% 0.13/0.41 ![X0]: (cC8(X0)|~rR1(X0,iV8469))),
% 0.13/0.41 inference(resolution,[status(thm)],[f579,f690])).
% 0.13/0.41 fof(f1919,plain,(
% 0.13/0.41 cC80(iV8471)|~cC2xcomp(iV8471)),
% 0.13/0.41 inference(resolution,[status(thm)],[f584,f696])).
% 0.13/0.41 fof(f1921,plain,(
% 0.13/0.41 sQ15_spl|~sQ19_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f1919,f765,f784])).
% 0.13/0.41 fof(f1924,plain,(
% 0.13/0.41 ![X0]: (cC82(X0)|~rR1(X0,iV8471)|~sQ15_spl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f766,f596])).
% 0.13/0.41 fof(f1926,plain,(
% 0.13/0.41 cC82(iV8467)|~sQ15_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f1924,f680])).
% 0.13/0.41 fof(f1945,plain,(
% 0.13/0.41 cC8(iV8467)),
% 0.13/0.41 inference(resolution,[status(thm)],[f1917,f682])).
% 0.13/0.41 fof(f1947,plain,(
% 0.13/0.41 cC10(iV8467)|~cC4(iV8467)),
% 0.13/0.41 inference(resolution,[status(thm)],[f1945,f148])).
% 0.13/0.41 fof(f1948,plain,(
% 0.13/0.41 sQ11_spl|~sQ5_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f1947,f753,f735])).
% 0.13/0.41 fof(f1949,plain,(
% 0.13/0.41 $false|sQ10_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f752,f1074])).
% 0.13/0.41 fof(f1950,plain,(
% 0.13/0.41 sQ10_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f1949])).
% 0.13/0.41 fof(f1951,plain,(
% 0.13/0.41 $false|sQ9_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f749,f1031])).
% 0.13/0.41 fof(f1952,plain,(
% 0.13/0.41 sQ9_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f1951])).
% 0.13/0.41 fof(f1953,plain,(
% 0.13/0.41 $false|~sQ15_spl|sQ7_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f743,f1926])).
% 0.13/0.41 fof(f1954,plain,(
% 0.13/0.41 ~sQ15_spl|sQ7_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f1953])).
% 0.13/0.41 fof(f1955,plain,(
% 0.13/0.41 $false|sQ6_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f740,f1945])).
% 0.13/0.41 fof(f1956,plain,(
% 0.13/0.41 sQ6_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f1955])).
% 0.13/0.41 fof(f1961,plain,(
% 0.13/0.41 ~xsd_string(sK81_skl)|~sQ3_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f730,f142])).
% 0.13/0.41 fof(f1962,plain,(
% 0.13/0.41 $false|~sQ2_spl|~sQ3_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1961,f727])).
% 0.13/0.41 fof(f1963,plain,(
% 0.13/0.41 ~sQ2_spl|~sQ3_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f1962])).
% 0.13/0.41 fof(f1964,plain,(
% 0.13/0.41 xsd_string(sK81_skl)|sQ3_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f731,f143])).
% 0.13/0.41 fof(f1965,plain,(
% 0.13/0.41 sQ2_spl|sQ3_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f1964,f726,f729])).
% 0.13/0.41 fof(f1966,plain,(
% 0.13/0.41 $false),
% 0.13/0.41 inference(sat_refutation,[status(thm)],[f777,f778,f780,f792,f794,f800,f847,f858,f869,f890,f892,f930,f932,f934,f936,f938,f955,f961,f1000,f1025,f1093,f1241,f1246,f1429,f1481,f1501,f1585,f1748,f1798,f1825,f1911,f1921,f1948,f1950,f1952,f1954,f1956,f1963,f1965])).
% 0.13/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.43 % Elapsed time: 0.067523 seconds
% 0.13/0.43 % CPU time: 0.261006 seconds
% 0.13/0.43 % Total memory used: 31.487 MB
% 0.13/0.43 % Net memory used: 31.320 MB
%------------------------------------------------------------------------------