%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS161+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 : n003.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:21 PM UTC 2026
% Result : Theorem 0.13s 0.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS161+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.10/0.36 % Computer : n003.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 22:56:45 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.43 % Refutation found
% 0.13/0.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.43 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.43 fof(f1,axiom,(
% 0.13/0.43 (! [X] :( cowlThing(X)& ~ cowlNothing(X) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f2,axiom,(
% 0.13/0.43 (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f11,axiom,(
% 0.13/0.43 (! [X] :( cC104(X)<=> (? [Y] :( rR1(X,Y)& cC102xcomp(Y) ) )) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f12,axiom,(
% 0.13/0.43 (! [X] :( cC106(X)<=> ( cC104(X)& cC100xcomp(X) ) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f13,axiom,(
% 0.13/0.43 (! [X] :( cC108(X)<=> ( cC28(X)& cC106(X) ) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f53,axiom,(
% 0.13/0.43 (! [X] :( cC34(X)<=> ( cC30xcomp(X)& cC32xcomp(X) ) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f58,axiom,(
% 0.13/0.43 (! [X] :( cC38(X)<=> ( cTOP(X)& cC36xcomp(X) ) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f66,axiom,(
% 0.13/0.43 (! [X] :( cC42(X)<=> (? [Y] :( rR1(X,Y)& cC8xcomp(Y) ) )) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f67,axiom,(
% 0.13/0.43 (! [X] :( cC44(X)<=> ( cC40xcomp(X)& cC42(X) ) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f74,axiom,(
% 0.13/0.43 (! [X] :( cC50(X)<=> ( cC46xcomp(X)& cC48xcomp(X) ) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f83,axiom,(
% 0.13/0.43 (! [X] :( cC56(X)<=> ( cC54xcomp(X)& cC44(X) ) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f92,axiom,(
% 0.13/0.43 (! [X] :( cC60(X)<=> (? [Y] :( rR1(X,Y)& cC12xcomp(Y) ) )) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f93,axiom,(
% 0.13/0.43 (! [X] :( cC62(X)<=> ( cC60(X)& cC58xcomp(X) ) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f101,axiom,(
% 0.13/0.43 (! [X] :( cC68(X)<=> ( cC64xcomp(X)& cC66xcomp(X) ) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f113,axiom,(
% 0.13/0.43 (! [X] :( cC76(X)<=> ( cC74xcomp(X)& cC62(X) ) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f121,axiom,(
% 0.13/0.43 (! [X] :( cC82(X)<=> ( cC80(X)& cC78xcomp(X) ) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f129,axiom,(
% 0.13/0.43 (! [X] :( cC88(X)<=> ( cC84xcomp(X)& cC86xcomp(X) ) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f144,axiom,(
% 0.13/0.43 (! [X] :( cC98(X)<=> ( cC96xcomp(X)& cC82(X) ) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f146,axiom,(
% 0.13/0.43 (! [X] :( cTEST(X)<=> ( cC108(X)& cC130(X) ) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f147,axiom,(
% 0.13/0.43 (! [X] :( rR1(iV16439,X)=> cC98(X) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f149,axiom,(
% 0.13/0.43 cC100xcomp(iV16439) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f150,axiom,(
% 0.13/0.43 cTEST(iV16439) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f151,axiom,(
% 0.13/0.43 rR1(iV16439,iV16440) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f157,axiom,(
% 0.13/0.43 (! [X] :( rR1(iV16440,X)=> cC76(X) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f158,axiom,(
% 0.13/0.43 cC102xcomp(iV16440) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f160,axiom,(
% 0.13/0.43 rR1(iV16440,iV16463) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f164,axiom,(
% 0.13/0.43 cTOP(iV16448) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f169,axiom,(
% 0.13/0.43 cC36xcomp(iV16448) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f171,axiom,(
% 0.13/0.43 (! [X] :( rR1(iV16448,X)=> cC88(X) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f173,axiom,(
% 0.13/0.43 rR1(iV16448,iV16449) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f175,axiom,(
% 0.13/0.43 cC74xcomp(iV16453) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f179,axiom,(
% 0.13/0.43 (! [X] :( rR1(iV16453,X)=> cC56(X) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f182,axiom,(
% 0.13/0.43 cC58xcomp(iV16453) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f183,axiom,(
% 0.13/0.43 rR1(iV16453,iV16461) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f186,axiom,(
% 0.13/0.43 cC40xcomp(iV16455) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f189,axiom,(
% 0.13/0.43 (! [X] :( rR1(iV16455,X)=> cC38(X) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f191,axiom,(
% 0.13/0.43 cC54xcomp(iV16455) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f194,axiom,(
% 0.13/0.43 rR1(iV16455,iV16460) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f198,axiom,(
% 0.13/0.43 cTOP(iV16457) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f202,axiom,(
% 0.13/0.43 cC36xcomp(iV16457) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f210,axiom,(
% 0.13/0.43 cC30xcomp(iV16459) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f211,axiom,(
% 0.13/0.43 cC84xcomp(iV16459) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f213,axiom,(
% 0.13/0.43 cC46xcomp(iV16459) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f214,axiom,(
% 0.13/0.43 cC64xcomp(iV16459) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f216,axiom,(
% 0.13/0.43 cC86xcomp(iV16459) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f217,axiom,(
% 0.13/0.43 cC32xcomp(iV16459) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f218,axiom,(
% 0.13/0.43 cC48xcomp(iV16459) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f222,axiom,(
% 0.13/0.43 cC66xcomp(iV16459) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f228,axiom,(
% 0.13/0.43 cC8xcomp(iV16460) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f238,axiom,(
% 0.13/0.43 cC12xcomp(iV16461) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f242,axiom,(
% 0.13/0.43 (! [X] :( rR1(iV16461,X)=> cC38(X) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f244,axiom,(
% 0.13/0.43 rR1(iV16461,iV16462) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f262,axiom,(
% 0.13/0.43 (! [X] :( rR1(iV16463,X)=> cC56(X) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f264,axiom,(
% 0.13/0.43 rR1(iV16463,iV16464) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f266,axiom,(
% 0.13/0.43 (! [X] :( rR1(iV16464,X)=> cC38(X) ) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f275,axiom,(
% 0.13/0.43 rR1(iV16464,iV16465) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f287,conjecture,(
% 0.13/0.43 ( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& cC130(iV16439)& cC108(iV16439)& cC104(iV16439)& cC106(iV16439)& cC28(iV16439)& cowlThing(iV16439)& cC98(iV16440)& cC80(iV16440)& cC82(iV16440)& cowlThing(iV16440)& cC38(iV16448)& cowlThing(iV16448)& cC76(iV16453)& cC62(iV16453)& cowlThing(iV16453)& cC60(iV16453)& cC56(iV16455)& cC44(iV16455)& cC42(iV16455)& cowlThing(iV16455)& cC38(iV16457)& cowlThing(iV16457)& cC50(iV16459)& cC88(iV16459)& cC34(iV16459)& cC68(iV16459)& cowlThing(iV16459)& cC38(iV16460)& cowlThing(iV16460)& cC42(iV16461)& cC56(iV16461)& cC44(iV16461)& cowlThing(iV16461)& cC38(iV16462)& cowlThing(iV16462)& cC76(iV16463)& cC62(iV16463)& cowlThing(iV16463)& cC60(iV16463)& cC56(iV16464)& cC42(iV16464)& cC44(iV16464)& cowlThing(iV16464)& cC38(iV16465)& cowlThing(iV16465) ) ),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f288,negated_conjecture,(
% 0.13/0.43 ~(( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& cC130(iV16439)& cC108(iV16439)& cC104(iV16439)& cC106(iV16439)& cC28(iV16439)& cowlThing(iV16439)& cC98(iV16440)& cC80(iV16440)& cC82(iV16440)& cowlThing(iV16440)& cC38(iV16448)& cowlThing(iV16448)& cC76(iV16453)& cC62(iV16453)& cowlThing(iV16453)& cC60(iV16453)& cC56(iV16455)& cC44(iV16455)& cC42(iV16455)& cowlThing(iV16455)& cC38(iV16457)& cowlThing(iV16457)& cC50(iV16459)& cC88(iV16459)& cC34(iV16459)& cC68(iV16459)& cowlThing(iV16459)& cC38(iV16460)& cowlThing(iV16460)& cC42(iV16461)& cC56(iV16461)& cC44(iV16461)& cowlThing(iV16461)& cC38(iV16462)& cowlThing(iV16462)& cC76(iV16463)& cC62(iV16463)& cowlThing(iV16463)& cC60(iV16463)& cC56(iV16464)& cC42(iV16464)& cC44(iV16464)& cowlThing(iV16464)& cC38(iV16465)& cowlThing(iV16465) ) )),
% 0.13/0.43 inference(negated_conjecture,[status(cth)],[f287])).
% 0.13/0.43 fof(f289,plain,(
% 0.13/0.43 (![X]: cowlThing(X))&(![X]: ~cowlNothing(X))),
% 0.13/0.43 inference(miniscoping,[status(thm)],[f1])).
% 0.13/0.43 fof(f290,plain,(
% 0.13/0.43 ![X0]: (cowlThing(X0))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f289])).
% 0.13/0.43 fof(f291,plain,(
% 0.13/0.43 ![X0]: (~cowlNothing(X0))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f289])).
% 0.13/0.43 fof(f292,plain,(
% 0.13/0.43 ![X]: ((~xsd_string(X)|~xsd_integer(X))&(xsd_string(X)|xsd_integer(X)))),
% 0.13/0.43 inference(NNF_transformation,[status(thm)],[f2])).
% 0.13/0.43 fof(f293,plain,(
% 0.13/0.43 (![X]: (~xsd_string(X)|~xsd_integer(X)))&(![X]: (xsd_string(X)|xsd_integer(X)))),
% 0.13/0.43 inference(miniscoping,[status(thm)],[f292])).
% 0.13/0.43 fof(f294,plain,(
% 0.13/0.43 ![X0]: (~xsd_string(X0)|~xsd_integer(X0))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f293])).
% 0.13/0.43 fof(f295,plain,(
% 0.13/0.43 ![X0]: (xsd_string(X0)|xsd_integer(X0))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f293])).
% 0.13/0.43 fof(f340,plain,(
% 0.13/0.43 ![X]: ((~cC104(X)|(?[Y]: (rR1(X,Y)&cC102xcomp(Y))))&(cC104(X)|(![Y]: (~rR1(X,Y)|~cC102xcomp(Y)))))),
% 0.13/0.43 inference(NNF_transformation,[status(thm)],[f11])).
% 0.13/0.43 fof(f341,plain,(
% 0.13/0.43 (![X]: (~cC104(X)|(?[Y]: (rR1(X,Y)&cC102xcomp(Y)))))&(![X]: (cC104(X)|(![Y]: (~rR1(X,Y)|~cC102xcomp(Y)))))),
% 0.13/0.43 inference(miniscoping,[status(thm)],[f340])).
% 0.13/0.43 fof(f342,plain,(
% 0.13/0.43 (![X]: (~cC104(X)|(rR1(X,sK7_skl(X))&cC102xcomp(sK7_skl(X)))))&(![X]: (cC104(X)|(![Y]: (~rR1(X,Y)|~cC102xcomp(Y)))))),
% 0.13/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(Y,sK7_skl(X))],[f341])).
% 0.13/0.43 fof(f345,plain,(
% 0.13/0.43 ![X0,X1]: (cC104(X0)|~rR1(X0,X1)|~cC102xcomp(X1))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f342])).
% 0.13/0.43 fof(f346,plain,(
% 0.13/0.43 ![X]: ((~cC106(X)|(cC104(X)&cC100xcomp(X)))&(cC106(X)|(~cC104(X)|~cC100xcomp(X))))),
% 0.13/0.43 inference(NNF_transformation,[status(thm)],[f12])).
% 0.13/0.43 fof(f347,plain,(
% 0.13/0.43 (![X]: (~cC106(X)|(cC104(X)&cC100xcomp(X))))&(![X]: (cC106(X)|(~cC104(X)|~cC100xcomp(X))))),
% 0.13/0.43 inference(miniscoping,[status(thm)],[f346])).
% 0.13/0.43 fof(f350,plain,(
% 0.13/0.43 ![X0]: (cC106(X0)|~cC104(X0)|~cC100xcomp(X0))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f347])).
% 0.13/0.43 fof(f351,plain,(
% 0.13/0.43 ![X]: ((~cC108(X)|(cC28(X)&cC106(X)))&(cC108(X)|(~cC28(X)|~cC106(X))))),
% 0.13/0.43 inference(NNF_transformation,[status(thm)],[f13])).
% 0.13/0.43 fof(f352,plain,(
% 0.13/0.43 (![X]: (~cC108(X)|(cC28(X)&cC106(X))))&(![X]: (cC108(X)|(~cC28(X)|~cC106(X))))),
% 0.13/0.43 inference(miniscoping,[status(thm)],[f351])).
% 0.13/0.43 fof(f353,plain,(
% 0.13/0.43 ![X0]: (~cC108(X0)|cC28(X0))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f352])).
% 0.13/0.43 fof(f355,plain,(
% 0.13/0.43 ![X0]: (cC108(X0)|~cC28(X0)|~cC106(X0))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f352])).
% 0.13/0.43 fof(f571,plain,(
% 0.13/0.43 ![X]: ((~cC34(X)|(cC30xcomp(X)&cC32xcomp(X)))&(cC34(X)|(~cC30xcomp(X)|~cC32xcomp(X))))),
% 0.13/0.43 inference(NNF_transformation,[status(thm)],[f53])).
% 0.13/0.43 fof(f572,plain,(
% 0.13/0.43 (![X]: (~cC34(X)|(cC30xcomp(X)&cC32xcomp(X))))&(![X]: (cC34(X)|(~cC30xcomp(X)|~cC32xcomp(X))))),
% 0.13/0.43 inference(miniscoping,[status(thm)],[f571])).
% 0.13/0.43 fof(f575,plain,(
% 0.13/0.43 ![X0]: (cC34(X0)|~cC30xcomp(X0)|~cC32xcomp(X0))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f572])).
% 0.13/0.43 fof(f599,plain,(
% 0.13/0.43 ![X]: ((~cC38(X)|(cTOP(X)&cC36xcomp(X)))&(cC38(X)|(~cTOP(X)|~cC36xcomp(X))))),
% 0.13/0.43 inference(NNF_transformation,[status(thm)],[f58])).
% 0.13/0.43 fof(f600,plain,(
% 0.13/0.43 (![X]: (~cC38(X)|(cTOP(X)&cC36xcomp(X))))&(![X]: (cC38(X)|(~cTOP(X)|~cC36xcomp(X))))),
% 0.13/0.43 inference(miniscoping,[status(thm)],[f599])).
% 0.13/0.43 fof(f603,plain,(
% 0.13/0.43 ![X0]: (cC38(X0)|~cTOP(X0)|~cC36xcomp(X0))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f600])).
% 0.13/0.43 fof(f643,plain,(
% 0.13/0.43 ![X]: ((~cC42(X)|(?[Y]: (rR1(X,Y)&cC8xcomp(Y))))&(cC42(X)|(![Y]: (~rR1(X,Y)|~cC8xcomp(Y)))))),
% 0.13/0.43 inference(NNF_transformation,[status(thm)],[f66])).
% 0.13/0.43 fof(f644,plain,(
% 0.13/0.43 (![X]: (~cC42(X)|(?[Y]: (rR1(X,Y)&cC8xcomp(Y)))))&(![X]: (cC42(X)|(![Y]: (~rR1(X,Y)|~cC8xcomp(Y)))))),
% 0.13/0.43 inference(miniscoping,[status(thm)],[f643])).
% 0.13/0.43 fof(f645,plain,(
% 0.13/0.43 (![X]: (~cC42(X)|(rR1(X,sK50_skl(X))&cC8xcomp(sK50_skl(X)))))&(![X]: (cC42(X)|(![Y]: (~rR1(X,Y)|~cC8xcomp(Y)))))),
% 0.13/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK50_skl]),skolemize(Y,sK50_skl(X))],[f644])).
% 0.13/0.43 fof(f648,plain,(
% 0.13/0.43 ![X0,X1]: (cC42(X0)|~rR1(X0,X1)|~cC8xcomp(X1))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f645])).
% 0.13/0.43 fof(f649,plain,(
% 0.13/0.43 ![X]: ((~cC44(X)|(cC40xcomp(X)&cC42(X)))&(cC44(X)|(~cC40xcomp(X)|~cC42(X))))),
% 0.13/0.43 inference(NNF_transformation,[status(thm)],[f67])).
% 0.13/0.43 fof(f650,plain,(
% 0.13/0.43 (![X]: (~cC44(X)|(cC40xcomp(X)&cC42(X))))&(![X]: (cC44(X)|(~cC40xcomp(X)|~cC42(X))))),
% 0.13/0.43 inference(miniscoping,[status(thm)],[f649])).
% 0.13/0.43 fof(f652,plain,(
% 0.13/0.43 ![X0]: (~cC44(X0)|cC42(X0))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f650])).
% 0.13/0.43 fof(f653,plain,(
% 0.13/0.43 ![X0]: (cC44(X0)|~cC40xcomp(X0)|~cC42(X0))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f650])).
% 0.13/0.43 fof(f686,plain,(
% 0.13/0.43 ![X]: ((~cC50(X)|(cC46xcomp(X)&cC48xcomp(X)))&(cC50(X)|(~cC46xcomp(X)|~cC48xcomp(X))))),
% 0.13/0.43 inference(NNF_transformation,[status(thm)],[f74])).
% 0.13/0.43 fof(f687,plain,(
% 0.13/0.44 (![X]: (~cC50(X)|(cC46xcomp(X)&cC48xcomp(X))))&(![X]: (cC50(X)|(~cC46xcomp(X)|~cC48xcomp(X))))),
% 0.13/0.44 inference(miniscoping,[status(thm)],[f686])).
% 0.13/0.44 fof(f690,plain,(
% 0.13/0.44 ![X0]: (cC50(X0)|~cC46xcomp(X0)|~cC48xcomp(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f687])).
% 0.13/0.44 fof(f736,plain,(
% 0.13/0.44 ![X]: ((~cC56(X)|(cC54xcomp(X)&cC44(X)))&(cC56(X)|(~cC54xcomp(X)|~cC44(X))))),
% 0.13/0.44 inference(NNF_transformation,[status(thm)],[f83])).
% 0.13/0.44 fof(f737,plain,(
% 0.13/0.44 (![X]: (~cC56(X)|(cC54xcomp(X)&cC44(X))))&(![X]: (cC56(X)|(~cC54xcomp(X)|~cC44(X))))),
% 0.13/0.44 inference(miniscoping,[status(thm)],[f736])).
% 0.13/0.44 fof(f739,plain,(
% 0.13/0.44 ![X0]: (~cC56(X0)|cC44(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f737])).
% 0.13/0.44 fof(f740,plain,(
% 0.13/0.44 ![X0]: (cC56(X0)|~cC54xcomp(X0)|~cC44(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f737])).
% 0.13/0.44 fof(f785,plain,(
% 0.13/0.44 ![X]: ((~cC60(X)|(?[Y]: (rR1(X,Y)&cC12xcomp(Y))))&(cC60(X)|(![Y]: (~rR1(X,Y)|~cC12xcomp(Y)))))),
% 0.13/0.44 inference(NNF_transformation,[status(thm)],[f92])).
% 0.13/0.44 fof(f786,plain,(
% 0.13/0.44 (![X]: (~cC60(X)|(?[Y]: (rR1(X,Y)&cC12xcomp(Y)))))&(![X]: (cC60(X)|(![Y]: (~rR1(X,Y)|~cC12xcomp(Y)))))),
% 0.13/0.44 inference(miniscoping,[status(thm)],[f785])).
% 0.13/0.44 fof(f787,plain,(
% 0.13/0.44 (![X]: (~cC60(X)|(rR1(X,sK70_skl(X))&cC12xcomp(sK70_skl(X)))))&(![X]: (cC60(X)|(![Y]: (~rR1(X,Y)|~cC12xcomp(Y)))))),
% 0.13/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK70_skl]),skolemize(Y,sK70_skl(X))],[f786])).
% 0.13/0.44 fof(f790,plain,(
% 0.13/0.44 ![X0,X1]: (cC60(X0)|~rR1(X0,X1)|~cC12xcomp(X1))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f787])).
% 0.13/0.44 fof(f791,plain,(
% 0.13/0.44 ![X]: ((~cC62(X)|(cC60(X)&cC58xcomp(X)))&(cC62(X)|(~cC60(X)|~cC58xcomp(X))))),
% 0.13/0.44 inference(NNF_transformation,[status(thm)],[f93])).
% 0.13/0.44 fof(f792,plain,(
% 0.13/0.44 (![X]: (~cC62(X)|(cC60(X)&cC58xcomp(X))))&(![X]: (cC62(X)|(~cC60(X)|~cC58xcomp(X))))),
% 0.13/0.44 inference(miniscoping,[status(thm)],[f791])).
% 0.13/0.44 fof(f793,plain,(
% 0.13/0.44 ![X0]: (~cC62(X0)|cC60(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f792])).
% 0.13/0.44 fof(f795,plain,(
% 0.13/0.44 ![X0]: (cC62(X0)|~cC60(X0)|~cC58xcomp(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f792])).
% 0.13/0.44 fof(f833,plain,(
% 0.13/0.44 ![X]: ((~cC68(X)|(cC64xcomp(X)&cC66xcomp(X)))&(cC68(X)|(~cC64xcomp(X)|~cC66xcomp(X))))),
% 0.13/0.44 inference(NNF_transformation,[status(thm)],[f101])).
% 0.13/0.44 fof(f834,plain,(
% 0.13/0.44 (![X]: (~cC68(X)|(cC64xcomp(X)&cC66xcomp(X))))&(![X]: (cC68(X)|(~cC64xcomp(X)|~cC66xcomp(X))))),
% 0.13/0.44 inference(miniscoping,[status(thm)],[f833])).
% 0.13/0.44 fof(f837,plain,(
% 0.13/0.44 ![X0]: (cC68(X0)|~cC64xcomp(X0)|~cC66xcomp(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f834])).
% 0.13/0.44 fof(f900,plain,(
% 0.13/0.44 ![X]: ((~cC76(X)|(cC74xcomp(X)&cC62(X)))&(cC76(X)|(~cC74xcomp(X)|~cC62(X))))),
% 0.13/0.44 inference(NNF_transformation,[status(thm)],[f113])).
% 0.13/0.44 fof(f901,plain,(
% 0.13/0.44 (![X]: (~cC76(X)|(cC74xcomp(X)&cC62(X))))&(![X]: (cC76(X)|(~cC74xcomp(X)|~cC62(X))))),
% 0.13/0.44 inference(miniscoping,[status(thm)],[f900])).
% 0.13/0.44 fof(f903,plain,(
% 0.13/0.44 ![X0]: (~cC76(X0)|cC62(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f901])).
% 0.13/0.44 fof(f904,plain,(
% 0.13/0.44 ![X0]: (cC76(X0)|~cC74xcomp(X0)|~cC62(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f901])).
% 0.13/0.44 fof(f945,plain,(
% 0.13/0.44 ![X]: ((~cC82(X)|(cC80(X)&cC78xcomp(X)))&(cC82(X)|(~cC80(X)|~cC78xcomp(X))))),
% 0.13/0.44 inference(NNF_transformation,[status(thm)],[f121])).
% 0.13/0.44 fof(f946,plain,(
% 0.13/0.44 (![X]: (~cC82(X)|(cC80(X)&cC78xcomp(X))))&(![X]: (cC82(X)|(~cC80(X)|~cC78xcomp(X))))),
% 0.13/0.44 inference(miniscoping,[status(thm)],[f945])).
% 0.13/0.44 fof(f947,plain,(
% 0.13/0.44 ![X0]: (~cC82(X0)|cC80(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f946])).
% 0.13/0.44 fof(f987,plain,(
% 0.13/0.44 ![X]: ((~cC88(X)|(cC84xcomp(X)&cC86xcomp(X)))&(cC88(X)|(~cC84xcomp(X)|~cC86xcomp(X))))),
% 0.13/0.44 inference(NNF_transformation,[status(thm)],[f129])).
% 0.13/0.44 fof(f988,plain,(
% 0.13/0.44 (![X]: (~cC88(X)|(cC84xcomp(X)&cC86xcomp(X))))&(![X]: (cC88(X)|(~cC84xcomp(X)|~cC86xcomp(X))))),
% 0.13/0.44 inference(miniscoping,[status(thm)],[f987])).
% 0.13/0.44 fof(f989,plain,(
% 0.13/0.44 ![X0]: (~cC88(X0)|cC84xcomp(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f988])).
% 0.13/0.44 fof(f990,plain,(
% 0.13/0.44 ![X0]: (~cC88(X0)|cC86xcomp(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f988])).
% 0.13/0.44 fof(f991,plain,(
% 0.13/0.44 ![X0]: (cC88(X0)|~cC84xcomp(X0)|~cC86xcomp(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f988])).
% 0.13/0.44 fof(f1071,plain,(
% 0.13/0.44 ![X]: ((~cC98(X)|(cC96xcomp(X)&cC82(X)))&(cC98(X)|(~cC96xcomp(X)|~cC82(X))))),
% 0.13/0.44 inference(NNF_transformation,[status(thm)],[f144])).
% 0.13/0.44 fof(f1072,plain,(
% 0.13/0.44 (![X]: (~cC98(X)|(cC96xcomp(X)&cC82(X))))&(![X]: (cC98(X)|(~cC96xcomp(X)|~cC82(X))))),
% 0.13/0.44 inference(miniscoping,[status(thm)],[f1071])).
% 0.13/0.44 fof(f1074,plain,(
% 0.13/0.44 ![X0]: (~cC98(X0)|cC82(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f1072])).
% 0.13/0.44 fof(f1082,plain,(
% 0.13/0.44 ![X]: ((~cTEST(X)|(cC108(X)&cC130(X)))&(cTEST(X)|(~cC108(X)|~cC130(X))))),
% 0.13/0.44 inference(NNF_transformation,[status(thm)],[f146])).
% 0.13/0.44 fof(f1083,plain,(
% 0.13/0.44 (![X]: (~cTEST(X)|(cC108(X)&cC130(X))))&(![X]: (cTEST(X)|(~cC108(X)|~cC130(X))))),
% 0.13/0.44 inference(miniscoping,[status(thm)],[f1082])).
% 0.13/0.44 fof(f1084,plain,(
% 0.13/0.44 ![X0]: (~cTEST(X0)|cC108(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f1083])).
% 0.13/0.44 fof(f1085,plain,(
% 0.13/0.44 ![X0]: (~cTEST(X0)|cC130(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f1083])).
% 0.13/0.44 fof(f1087,plain,(
% 0.13/0.44 ![X]: (~rR1(iV16439,X)|cC98(X))),
% 0.13/0.44 inference(pre_NNF_transformation,[status(thm)],[f147])).
% 0.13/0.44 fof(f1088,plain,(
% 0.13/0.44 ![X0]: (~rR1(iV16439,X0)|cC98(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f1087])).
% 0.13/0.44 fof(f1090,plain,(
% 0.13/0.44 cC100xcomp(iV16439)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f149])).
% 0.13/0.44 fof(f1091,plain,(
% 0.13/0.44 cTEST(iV16439)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f150])).
% 0.13/0.44 fof(f1092,plain,(
% 0.13/0.44 rR1(iV16439,iV16440)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f151])).
% 0.13/0.44 fof(f1099,plain,(
% 0.13/0.44 ![X]: (~rR1(iV16440,X)|cC76(X))),
% 0.13/0.44 inference(pre_NNF_transformation,[status(thm)],[f157])).
% 0.13/0.44 fof(f1100,plain,(
% 0.13/0.44 ![X0]: (~rR1(iV16440,X0)|cC76(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f1099])).
% 0.13/0.44 fof(f1101,plain,(
% 0.13/0.44 cC102xcomp(iV16440)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f158])).
% 0.13/0.44 fof(f1103,plain,(
% 0.13/0.44 rR1(iV16440,iV16463)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f160])).
% 0.13/0.44 fof(f1107,plain,(
% 0.13/0.44 cTOP(iV16448)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f164])).
% 0.13/0.44 fof(f1115,plain,(
% 0.13/0.44 cC36xcomp(iV16448)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f169])).
% 0.13/0.44 fof(f1117,plain,(
% 0.13/0.44 ![X]: (~rR1(iV16448,X)|cC88(X))),
% 0.13/0.44 inference(pre_NNF_transformation,[status(thm)],[f171])).
% 0.13/0.44 fof(f1118,plain,(
% 0.13/0.44 ![X0]: (~rR1(iV16448,X0)|cC88(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f1117])).
% 0.13/0.44 fof(f1120,plain,(
% 0.13/0.44 rR1(iV16448,iV16449)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f173])).
% 0.13/0.44 fof(f1122,plain,(
% 0.13/0.44 cC74xcomp(iV16453)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f175])).
% 0.13/0.44 fof(f1127,plain,(
% 0.13/0.44 ![X]: (~rR1(iV16453,X)|cC56(X))),
% 0.13/0.44 inference(pre_NNF_transformation,[status(thm)],[f179])).
% 0.13/0.44 fof(f1128,plain,(
% 0.13/0.44 ![X0]: (~rR1(iV16453,X0)|cC56(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f1127])).
% 0.13/0.44 fof(f1132,plain,(
% 0.13/0.44 cC58xcomp(iV16453)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f182])).
% 0.13/0.44 fof(f1133,plain,(
% 0.13/0.44 rR1(iV16453,iV16461)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f183])).
% 0.13/0.44 fof(f1137,plain,(
% 0.13/0.44 cC40xcomp(iV16455)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f186])).
% 0.13/0.44 fof(f1141,plain,(
% 0.13/0.44 ![X]: (~rR1(iV16455,X)|cC38(X))),
% 0.13/0.44 inference(pre_NNF_transformation,[status(thm)],[f189])).
% 0.13/0.44 fof(f1142,plain,(
% 0.13/0.44 ![X0]: (~rR1(iV16455,X0)|cC38(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f1141])).
% 0.13/0.44 fof(f1144,plain,(
% 0.13/0.44 cC54xcomp(iV16455)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f191])).
% 0.13/0.44 fof(f1148,plain,(
% 0.13/0.44 rR1(iV16455,iV16460)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f194])).
% 0.13/0.44 fof(f1154,plain,(
% 0.13/0.44 cTOP(iV16457)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f198])).
% 0.13/0.44 fof(f1159,plain,(
% 0.13/0.44 cC36xcomp(iV16457)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f202])).
% 0.13/0.44 fof(f1168,plain,(
% 0.13/0.44 cC30xcomp(iV16459)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f210])).
% 0.13/0.44 fof(f1169,plain,(
% 0.13/0.44 cC84xcomp(iV16459)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f211])).
% 0.13/0.44 fof(f1171,plain,(
% 0.13/0.44 cC46xcomp(iV16459)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f213])).
% 0.13/0.44 fof(f1172,plain,(
% 0.13/0.44 cC64xcomp(iV16459)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f214])).
% 0.13/0.44 fof(f1174,plain,(
% 0.13/0.44 cC86xcomp(iV16459)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f216])).
% 0.13/0.44 fof(f1175,plain,(
% 0.13/0.44 cC32xcomp(iV16459)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f217])).
% 0.13/0.44 fof(f1176,plain,(
% 0.13/0.44 cC48xcomp(iV16459)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f218])).
% 0.13/0.44 fof(f1180,plain,(
% 0.13/0.44 cC66xcomp(iV16459)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f222])).
% 0.13/0.44 fof(f1188,plain,(
% 0.13/0.44 cC8xcomp(iV16460)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f228])).
% 0.13/0.44 fof(f1202,plain,(
% 0.13/0.44 cC12xcomp(iV16461)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f238])).
% 0.13/0.44 fof(f1207,plain,(
% 0.13/0.44 ![X]: (~rR1(iV16461,X)|cC38(X))),
% 0.13/0.44 inference(pre_NNF_transformation,[status(thm)],[f242])).
% 0.13/0.44 fof(f1208,plain,(
% 0.13/0.44 ![X0]: (~rR1(iV16461,X0)|cC38(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f1207])).
% 0.13/0.44 fof(f1210,plain,(
% 0.13/0.44 rR1(iV16461,iV16462)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f244])).
% 0.13/0.44 fof(f1234,plain,(
% 0.13/0.44 ![X]: (~rR1(iV16463,X)|cC56(X))),
% 0.13/0.44 inference(pre_NNF_transformation,[status(thm)],[f262])).
% 0.13/0.44 fof(f1235,plain,(
% 0.13/0.44 ![X0]: (~rR1(iV16463,X0)|cC56(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f1234])).
% 0.13/0.44 fof(f1237,plain,(
% 0.13/0.44 rR1(iV16463,iV16464)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f264])).
% 0.13/0.44 fof(f1239,plain,(
% 0.13/0.44 ![X]: (~rR1(iV16464,X)|cC38(X))),
% 0.13/0.44 inference(pre_NNF_transformation,[status(thm)],[f266])).
% 0.13/0.44 fof(f1240,plain,(
% 0.13/0.44 ![X0]: (~rR1(iV16464,X0)|cC38(X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f1239])).
% 0.13/0.44 fof(f1252,plain,(
% 0.13/0.44 rR1(iV16464,iV16465)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f275])).
% 0.13/0.44 fof(f1268,plain,(
% 0.13/0.44 (((((((((((((((((((((((((((((((((((((((((((((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: (xsd_string(X)<~>~xsd_integer(X))))|~cC130(iV16439))|~cC108(iV16439))|~cC104(iV16439))|~cC106(iV16439))|~cC28(iV16439))|~cowlThing(iV16439))|~cC98(iV16440))|~cC80(iV16440))|~cC82(iV16440))|~cowlThing(iV16440))|~cC38(iV16448))|~cowlThing(iV16448))|~cC76(iV16453))|~cC62(iV16453))|~cowlThing(iV16453))|~cC60(iV16453))|~cC56(iV16455))|~cC44(iV16455))|~cC42(iV16455))|~cowlThing(iV16455))|~cC38(iV16457))|~cowlThing(iV16457))|~cC50(iV16459))|~cC88(iV16459))|~cC34(iV16459))|~cC68(iV16459))|~cowlThing(iV16459))|~cC38(iV16460))|~cowlThing(iV16460))|~cC42(iV16461))|~cC56(iV16461))|~cC44(iV16461))|~cowlThing(iV16461))|~cC38(iV16462))|~cowlThing(iV16462))|~cC76(iV16463))|~cC62(iV16463))|~cowlThing(iV16463))|~cC60(iV16463))|~cC56(iV16464))|~cC42(iV16464))|~cC44(iV16464))|~cowlThing(iV16464))|~cC38(iV16465))|~cowlThing(iV16465))),
% 0.13/0.44 inference(pre_NNF_transformation,[status(thm)],[f288])).
% 0.13/0.44 fof(f1269,plain,(
% 0.13/0.44 ((((((((((((((((((((((((((((((((((((((((((((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: ((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))|~cC130(iV16439))|~cC108(iV16439))|~cC104(iV16439))|~cC106(iV16439))|~cC28(iV16439))|~cowlThing(iV16439))|~cC98(iV16440))|~cC80(iV16440))|~cC82(iV16440))|~cowlThing(iV16440))|~cC38(iV16448))|~cowlThing(iV16448))|~cC76(iV16453))|~cC62(iV16453))|~cowlThing(iV16453))|~cC60(iV16453))|~cC56(iV16455))|~cC44(iV16455))|~cC42(iV16455))|~cowlThing(iV16455))|~cC38(iV16457))|~cowlThing(iV16457))|~cC50(iV16459))|~cC88(iV16459))|~cC34(iV16459))|~cC68(iV16459))|~cowlThing(iV16459))|~cC38(iV16460))|~cowlThing(iV16460))|~cC42(iV16461))|~cC56(iV16461))|~cC44(iV16461))|~cowlThing(iV16461))|~cC38(iV16462))|~cowlThing(iV16462))|~cC76(iV16463))|~cC62(iV16463))|~cowlThing(iV16463))|~cC60(iV16463))|~cC56(iV16464))|~cC42(iV16464))|~cC44(iV16464))|~cowlThing(iV16464))|~cC38(iV16465))|~cowlThing(iV16465)),
% 0.13/0.44 inference(NNF_transformation,[status(thm)],[f1268])).
% 0.13/0.44 fof(f1270,plain,(
% 0.13/0.44 (((((((((((((((((((((((((((((((((((((((((((((((?[X]: ~cowlThing(X))|(?[X]: cowlNothing(X)))|(?[X]: ((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))|~cC130(iV16439))|~cC108(iV16439))|~cC104(iV16439))|~cC106(iV16439))|~cC28(iV16439))|~cowlThing(iV16439))|~cC98(iV16440))|~cC80(iV16440))|~cC82(iV16440))|~cowlThing(iV16440))|~cC38(iV16448))|~cowlThing(iV16448))|~cC76(iV16453))|~cC62(iV16453))|~cowlThing(iV16453))|~cC60(iV16453))|~cC56(iV16455))|~cC44(iV16455))|~cC42(iV16455))|~cowlThing(iV16455))|~cC38(iV16457))|~cowlThing(iV16457))|~cC50(iV16459))|~cC88(iV16459))|~cC34(iV16459))|~cC68(iV16459))|~cowlThing(iV16459))|~cC38(iV16460))|~cowlThing(iV16460))|~cC42(iV16461))|~cC56(iV16461))|~cC44(iV16461))|~cowlThing(iV16461))|~cC38(iV16462))|~cowlThing(iV16462))|~cC76(iV16463))|~cC62(iV16463))|~cowlThing(iV16463))|~cC60(iV16463))|~cC56(iV16464))|~cC42(iV16464))|~cC44(iV16464))|~cowlThing(iV16464))|~cC38(iV16465))|~cowlThing(iV16465)),
% 0.13/0.44 inference(miniscoping,[status(thm)],[f1269])).
% 0.13/0.44 fof(f1271,plain,(
% 0.13/0.44 ((((((((((((((((((((((((((((((((((((((((((((((~cowlThing(sK114_skl)|cowlNothing(sK115_skl))|((xsd_string(sK116_skl)|~xsd_integer(sK116_skl))&(~xsd_string(sK116_skl)|xsd_integer(sK116_skl))))|~cC130(iV16439))|~cC108(iV16439))|~cC104(iV16439))|~cC106(iV16439))|~cC28(iV16439))|~cowlThing(iV16439))|~cC98(iV16440))|~cC80(iV16440))|~cC82(iV16440))|~cowlThing(iV16440))|~cC38(iV16448))|~cowlThing(iV16448))|~cC76(iV16453))|~cC62(iV16453))|~cowlThing(iV16453))|~cC60(iV16453))|~cC56(iV16455))|~cC44(iV16455))|~cC42(iV16455))|~cowlThing(iV16455))|~cC38(iV16457))|~cowlThing(iV16457))|~cC50(iV16459))|~cC88(iV16459))|~cC34(iV16459))|~cC68(iV16459))|~cowlThing(iV16459))|~cC38(iV16460))|~cowlThing(iV16460))|~cC42(iV16461))|~cC56(iV16461))|~cC44(iV16461))|~cowlThing(iV16461))|~cC38(iV16462))|~cowlThing(iV16462))|~cC76(iV16463))|~cC62(iV16463))|~cowlThing(iV16463))|~cC60(iV16463))|~cC56(iV16464))|~cC42(iV16464))|~cC44(iV16464))|~cowlThing(iV16464))|~cC38(iV16465))|~cowlThing(iV16465)),
% 0.13/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK114_skl,sK115_skl,sK116_skl]),skolemize(X,sK114_skl),skolemize(X,sK115_skl),skolemize(X,sK116_skl)],[f1270])).
% 0.13/0.44 fof(f1272,plain,(
% 0.13/0.44 ~cowlThing(sK114_skl)|cowlNothing(sK115_skl)|xsd_string(sK116_skl)|~xsd_integer(sK116_skl)|~cC130(iV16439)|~cC108(iV16439)|~cC104(iV16439)|~cC106(iV16439)|~cC28(iV16439)|~cowlThing(iV16439)|~cC98(iV16440)|~cC80(iV16440)|~cC82(iV16440)|~cowlThing(iV16440)|~cC38(iV16448)|~cowlThing(iV16448)|~cC76(iV16453)|~cC62(iV16453)|~cowlThing(iV16453)|~cC60(iV16453)|~cC56(iV16455)|~cC44(iV16455)|~cC42(iV16455)|~cowlThing(iV16455)|~cC38(iV16457)|~cowlThing(iV16457)|~cC50(iV16459)|~cC88(iV16459)|~cC34(iV16459)|~cC68(iV16459)|~cowlThing(iV16459)|~cC38(iV16460)|~cowlThing(iV16460)|~cC42(iV16461)|~cC56(iV16461)|~cC44(iV16461)|~cowlThing(iV16461)|~cC38(iV16462)|~cowlThing(iV16462)|~cC76(iV16463)|~cC62(iV16463)|~cowlThing(iV16463)|~cC60(iV16463)|~cC56(iV16464)|~cC42(iV16464)|~cC44(iV16464)|~cowlThing(iV16464)|~cC38(iV16465)|~cowlThing(iV16465)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f1271])).
% 0.13/0.44 fof(f1273,plain,(
% 0.13/0.44 ~cowlThing(sK114_skl)|cowlNothing(sK115_skl)|~xsd_string(sK116_skl)|xsd_integer(sK116_skl)|~cC130(iV16439)|~cC108(iV16439)|~cC104(iV16439)|~cC106(iV16439)|~cC28(iV16439)|~cowlThing(iV16439)|~cC98(iV16440)|~cC80(iV16440)|~cC82(iV16440)|~cowlThing(iV16440)|~cC38(iV16448)|~cowlThing(iV16448)|~cC76(iV16453)|~cC62(iV16453)|~cowlThing(iV16453)|~cC60(iV16453)|~cC56(iV16455)|~cC44(iV16455)|~cC42(iV16455)|~cowlThing(iV16455)|~cC38(iV16457)|~cowlThing(iV16457)|~cC50(iV16459)|~cC88(iV16459)|~cC34(iV16459)|~cC68(iV16459)|~cowlThing(iV16459)|~cC38(iV16460)|~cowlThing(iV16460)|~cC42(iV16461)|~cC56(iV16461)|~cC44(iV16461)|~cowlThing(iV16461)|~cC38(iV16462)|~cowlThing(iV16462)|~cC76(iV16463)|~cC62(iV16463)|~cowlThing(iV16463)|~cC60(iV16463)|~cC56(iV16464)|~cC42(iV16464)|~cC44(iV16464)|~cowlThing(iV16464)|~cC38(iV16465)|~cowlThing(iV16465)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f1271])).
% 0.13/0.44 fof(f1274,definition,(
% 0.13/0.44 sQ0_spl <=> (cowlThing(sK114_skl))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1276,plain,(
% 0.13/0.44 ~cowlThing(sK114_skl)|sQ0_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1274])).
% 0.13/0.44 fof(f1277,definition,(
% 0.13/0.44 sQ1_spl <=> (cowlNothing(sK115_skl))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1278,plain,(
% 0.13/0.44 cowlNothing(sK115_skl)|~sQ1_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1277])).
% 0.13/0.44 fof(f1280,definition,(
% 0.13/0.44 sQ2_spl <=> (xsd_string(sK116_skl))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1281,plain,(
% 0.13/0.44 xsd_string(sK116_skl)|~sQ2_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1280])).
% 0.13/0.44 fof(f1283,definition,(
% 0.13/0.44 sQ3_spl <=> (xsd_integer(sK116_skl))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1284,plain,(
% 0.13/0.44 xsd_integer(sK116_skl)|~sQ3_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1283])).
% 0.13/0.44 fof(f1285,plain,(
% 0.13/0.44 ~xsd_integer(sK116_skl)|sQ3_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1283])).
% 0.13/0.44 fof(f1286,definition,(
% 0.13/0.44 sQ4_spl <=> (cC130(iV16439))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1288,plain,(
% 0.13/0.44 ~cC130(iV16439)|sQ4_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1286])).
% 0.13/0.44 fof(f1289,definition,(
% 0.13/0.44 sQ5_spl <=> (cC108(iV16439))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1292,definition,(
% 0.13/0.44 sQ6_spl <=> (cC104(iV16439))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1295,definition,(
% 0.13/0.44 sQ7_spl <=> (cC106(iV16439))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1296,plain,(
% 0.13/0.44 cC106(iV16439)|~sQ7_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1295])).
% 0.13/0.44 fof(f1298,definition,(
% 0.13/0.44 sQ8_spl <=> (cC28(iV16439))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1300,plain,(
% 0.13/0.44 ~cC28(iV16439)|sQ8_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1298])).
% 0.13/0.44 fof(f1301,definition,(
% 0.13/0.44 sQ9_spl <=> (cowlThing(iV16439))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1303,plain,(
% 0.13/0.44 ~cowlThing(iV16439)|sQ9_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1301])).
% 0.13/0.44 fof(f1304,definition,(
% 0.13/0.44 sQ10_spl <=> (cC98(iV16440))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1306,plain,(
% 0.13/0.44 ~cC98(iV16440)|sQ10_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1304])).
% 0.13/0.44 fof(f1307,definition,(
% 0.13/0.44 sQ11_spl <=> (cC80(iV16440))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1309,plain,(
% 0.13/0.44 ~cC80(iV16440)|sQ11_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1307])).
% 0.13/0.44 fof(f1310,definition,(
% 0.13/0.44 sQ12_spl <=> (cC82(iV16440))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1312,plain,(
% 0.13/0.44 ~cC82(iV16440)|sQ12_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1310])).
% 0.13/0.44 fof(f1313,definition,(
% 0.13/0.44 sQ13_spl <=> (cowlThing(iV16440))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1315,plain,(
% 0.13/0.44 ~cowlThing(iV16440)|sQ13_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1313])).
% 0.13/0.44 fof(f1316,definition,(
% 0.13/0.44 sQ14_spl <=> (cC38(iV16448))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1319,definition,(
% 0.13/0.44 sQ15_spl <=> (cowlThing(iV16448))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1321,plain,(
% 0.13/0.44 ~cowlThing(iV16448)|sQ15_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1319])).
% 0.13/0.44 fof(f1322,definition,(
% 0.13/0.44 sQ16_spl <=> (cC76(iV16453))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1325,definition,(
% 0.13/0.44 sQ17_spl <=> (cC62(iV16453))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1327,plain,(
% 0.13/0.44 ~cC62(iV16453)|sQ17_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1325])).
% 0.13/0.44 fof(f1328,definition,(
% 0.13/0.44 sQ18_spl <=> (cowlThing(iV16453))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1330,plain,(
% 0.13/0.44 ~cowlThing(iV16453)|sQ18_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1328])).
% 0.13/0.44 fof(f1331,definition,(
% 0.13/0.44 sQ19_spl <=> (cC60(iV16453))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1333,plain,(
% 0.13/0.44 ~cC60(iV16453)|sQ19_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1331])).
% 0.13/0.44 fof(f1334,definition,(
% 0.13/0.44 sQ20_spl <=> (cC56(iV16455))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1336,plain,(
% 0.13/0.44 ~cC56(iV16455)|sQ20_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1334])).
% 0.13/0.44 fof(f1337,definition,(
% 0.13/0.44 sQ21_spl <=> (cC44(iV16455))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1339,plain,(
% 0.13/0.44 ~cC44(iV16455)|sQ21_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1337])).
% 0.13/0.44 fof(f1340,definition,(
% 0.13/0.44 sQ22_spl <=> (cC42(iV16455))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1342,plain,(
% 0.13/0.44 ~cC42(iV16455)|sQ22_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1340])).
% 0.13/0.44 fof(f1343,definition,(
% 0.13/0.44 sQ23_spl <=> (cowlThing(iV16455))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1345,plain,(
% 0.13/0.44 ~cowlThing(iV16455)|sQ23_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1343])).
% 0.13/0.44 fof(f1346,definition,(
% 0.13/0.44 sQ24_spl <=> (cC38(iV16457))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1349,definition,(
% 0.13/0.44 sQ25_spl <=> (cowlThing(iV16457))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1351,plain,(
% 0.13/0.44 ~cowlThing(iV16457)|sQ25_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1349])).
% 0.13/0.44 fof(f1352,definition,(
% 0.13/0.44 sQ26_spl <=> (cC50(iV16459))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1354,plain,(
% 0.13/0.44 ~cC50(iV16459)|sQ26_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1352])).
% 0.13/0.44 fof(f1355,definition,(
% 0.13/0.44 sQ27_spl <=> (cC88(iV16459))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1358,definition,(
% 0.13/0.44 sQ28_spl <=> (cC34(iV16459))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1360,plain,(
% 0.13/0.44 ~cC34(iV16459)|sQ28_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1358])).
% 0.13/0.44 fof(f1361,definition,(
% 0.13/0.44 sQ29_spl <=> (cC68(iV16459))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1363,plain,(
% 0.13/0.44 ~cC68(iV16459)|sQ29_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1361])).
% 0.13/0.44 fof(f1364,definition,(
% 0.13/0.44 sQ30_spl <=> (cowlThing(iV16459))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1366,plain,(
% 0.13/0.44 ~cowlThing(iV16459)|sQ30_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1364])).
% 0.13/0.44 fof(f1367,definition,(
% 0.13/0.44 sQ31_spl <=> (cC38(iV16460))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1369,plain,(
% 0.13/0.44 ~cC38(iV16460)|sQ31_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1367])).
% 0.13/0.44 fof(f1370,definition,(
% 0.13/0.44 sQ32_spl <=> (cowlThing(iV16460))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1372,plain,(
% 0.13/0.44 ~cowlThing(iV16460)|sQ32_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1370])).
% 0.13/0.44 fof(f1373,definition,(
% 0.13/0.44 sQ33_spl <=> (cC42(iV16461))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1375,plain,(
% 0.13/0.44 ~cC42(iV16461)|sQ33_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1373])).
% 0.13/0.44 fof(f1376,definition,(
% 0.13/0.44 sQ34_spl <=> (cC56(iV16461))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1378,plain,(
% 0.13/0.44 ~cC56(iV16461)|sQ34_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1376])).
% 0.13/0.44 fof(f1379,definition,(
% 0.13/0.44 sQ35_spl <=> (cC44(iV16461))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1381,plain,(
% 0.13/0.44 ~cC44(iV16461)|sQ35_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1379])).
% 0.13/0.44 fof(f1382,definition,(
% 0.13/0.44 sQ36_spl <=> (cowlThing(iV16461))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1384,plain,(
% 0.13/0.44 ~cowlThing(iV16461)|sQ36_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1382])).
% 0.13/0.44 fof(f1385,definition,(
% 0.13/0.44 sQ37_spl <=> (cC38(iV16462))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1387,plain,(
% 0.13/0.44 ~cC38(iV16462)|sQ37_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1385])).
% 0.13/0.44 fof(f1388,definition,(
% 0.13/0.44 sQ38_spl <=> (cowlThing(iV16462))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1390,plain,(
% 0.13/0.44 ~cowlThing(iV16462)|sQ38_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1388])).
% 0.13/0.44 fof(f1391,definition,(
% 0.13/0.44 sQ39_spl <=> (cC76(iV16463))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1393,plain,(
% 0.13/0.44 ~cC76(iV16463)|sQ39_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1391])).
% 0.13/0.44 fof(f1394,definition,(
% 0.13/0.44 sQ40_spl <=> (cC62(iV16463))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1396,plain,(
% 0.13/0.44 ~cC62(iV16463)|sQ40_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1394])).
% 0.13/0.44 fof(f1397,definition,(
% 0.13/0.44 sQ41_spl <=> (cowlThing(iV16463))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1399,plain,(
% 0.13/0.44 ~cowlThing(iV16463)|sQ41_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1397])).
% 0.13/0.44 fof(f1400,definition,(
% 0.13/0.44 sQ42_spl <=> (cC60(iV16463))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1402,plain,(
% 0.13/0.44 ~cC60(iV16463)|sQ42_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1400])).
% 0.13/0.44 fof(f1403,definition,(
% 0.13/0.44 sQ43_spl <=> (cC56(iV16464))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1405,plain,(
% 0.13/0.44 ~cC56(iV16464)|sQ43_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1403])).
% 0.13/0.44 fof(f1406,definition,(
% 0.13/0.44 sQ44_spl <=> (cC42(iV16464))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1408,plain,(
% 0.13/0.44 ~cC42(iV16464)|sQ44_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1406])).
% 0.13/0.44 fof(f1409,definition,(
% 0.13/0.44 sQ45_spl <=> (cC44(iV16464))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1411,plain,(
% 0.13/0.44 ~cC44(iV16464)|sQ45_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1409])).
% 0.13/0.44 fof(f1412,definition,(
% 0.13/0.44 sQ46_spl <=> (cowlThing(iV16464))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1414,plain,(
% 0.13/0.44 ~cowlThing(iV16464)|sQ46_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1412])).
% 0.13/0.44 fof(f1415,definition,(
% 0.13/0.44 sQ47_spl <=> (cC38(iV16465))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1417,plain,(
% 0.13/0.44 ~cC38(iV16465)|sQ47_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1415])).
% 0.13/0.44 fof(f1418,definition,(
% 0.13/0.44 sQ48_spl <=> (cowlThing(iV16465))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1420,plain,(
% 0.13/0.44 ~cowlThing(iV16465)|sQ48_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1418])).
% 0.13/0.44 fof(f1421,plain,(
% 0.13/0.44 ~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|~sQ19_spl|~sQ20_spl|~sQ21_spl|~sQ22_spl|~sQ23_spl|~sQ24_spl|~sQ25_spl|~sQ26_spl|~sQ27_spl|~sQ28_spl|~sQ29_spl|~sQ30_spl|~sQ31_spl|~sQ32_spl|~sQ33_spl|~sQ34_spl|~sQ35_spl|~sQ36_spl|~sQ37_spl|~sQ38_spl|~sQ39_spl|~sQ40_spl|~sQ41_spl|~sQ42_spl|~sQ43_spl|~sQ44_spl|~sQ45_spl|~sQ46_spl|~sQ47_spl|~sQ48_spl),
% 0.13/0.44 inference(split_clause,[status(thm)],[f1272,f1274,f1277,f1280,f1283,f1286,f1289,f1292,f1295,f1298,f1301,f1304,f1307,f1310,f1313,f1316,f1319,f1322,f1325,f1328,f1331,f1334,f1337,f1340,f1343,f1346,f1349,f1352,f1355,f1358,f1361,f1364,f1367,f1370,f1373,f1376,f1379,f1382,f1385,f1388,f1391,f1394,f1397,f1400,f1403,f1406,f1409,f1412,f1415,f1418])).
% 0.13/0.44 fof(f1422,plain,(
% 0.13/0.44 ~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|~sQ19_spl|~sQ20_spl|~sQ21_spl|~sQ22_spl|~sQ23_spl|~sQ24_spl|~sQ25_spl|~sQ26_spl|~sQ27_spl|~sQ28_spl|~sQ29_spl|~sQ30_spl|~sQ31_spl|~sQ32_spl|~sQ33_spl|~sQ34_spl|~sQ35_spl|~sQ36_spl|~sQ37_spl|~sQ38_spl|~sQ39_spl|~sQ40_spl|~sQ41_spl|~sQ42_spl|~sQ43_spl|~sQ44_spl|~sQ45_spl|~sQ46_spl|~sQ47_spl|~sQ48_spl),
% 0.13/0.44 inference(split_clause,[status(thm)],[f1273,f1274,f1277,f1280,f1283,f1286,f1289,f1292,f1295,f1298,f1301,f1304,f1307,f1310,f1313,f1316,f1319,f1322,f1325,f1328,f1331,f1334,f1337,f1340,f1343,f1346,f1349,f1352,f1355,f1358,f1361,f1364,f1367,f1370,f1373,f1376,f1379,f1382,f1385,f1388,f1391,f1394,f1397,f1400,f1403,f1406,f1409,f1412,f1415,f1418])).
% 0.13/0.44 fof(f1423,plain,(
% 0.13/0.44 $false|sQ48_spl),
% 0.13/0.44 inference(backward_subsumption_resolution,[status(thm)],[f1420,f290])).
% 0.13/0.44 fof(f1424,plain,(
% 0.13/0.44 sQ48_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1423])).
% 0.13/0.44 fof(f1427,plain,(
% 0.13/0.44 cC104(iV16439)|~cC102xcomp(iV16440)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1092,f345])).
% 0.13/0.44 fof(f1428,definition,(
% 0.13/0.44 sQ49_spl <=> (cC102xcomp(iV16440))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1430,plain,(
% 0.13/0.44 ~cC102xcomp(iV16440)|sQ49_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1428])).
% 0.13/0.44 fof(f1431,plain,(
% 0.13/0.44 sQ6_spl|~sQ49_spl),
% 0.13/0.44 inference(split_clause,[status(thm)],[f1427,f1292,f1428])).
% 0.13/0.44 fof(f1440,plain,(
% 0.13/0.44 cC98(iV16440)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1088,f1092])).
% 0.13/0.44 fof(f1444,plain,(
% 0.13/0.44 cC82(iV16440)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1440,f1074])).
% 0.13/0.44 fof(f1445,plain,(
% 0.13/0.44 cC80(iV16440)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1444,f947])).
% 0.13/0.44 fof(f1446,plain,(
% 0.13/0.44 cC76(iV16463)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1100,f1103])).
% 0.13/0.44 fof(f1447,plain,(
% 0.13/0.44 cC62(iV16463)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1446,f903])).
% 0.13/0.44 fof(f1448,plain,(
% 0.13/0.44 cC60(iV16463)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1447,f793])).
% 0.13/0.44 fof(f1492,plain,(
% 0.13/0.44 cC56(iV16461)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1128,f1133])).
% 0.13/0.44 fof(f1493,plain,(
% 0.13/0.44 cC38(iV16460)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1142,f1148])).
% 0.13/0.44 fof(f1496,plain,(
% 0.13/0.44 cC44(iV16461)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1492,f739])).
% 0.13/0.44 fof(f1497,plain,(
% 0.13/0.44 cC42(iV16461)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1496,f652])).
% 0.13/0.44 fof(f1498,plain,(
% 0.13/0.44 ![X0]: (cC42(X0)|~rR1(X0,iV16460))),
% 0.13/0.44 inference(resolution,[status(thm)],[f1188,f648])).
% 0.13/0.44 fof(f1499,plain,(
% 0.13/0.44 ![X0]: (cC60(X0)|~rR1(X0,iV16461))),
% 0.13/0.44 inference(resolution,[status(thm)],[f1202,f790])).
% 0.13/0.44 fof(f1502,plain,(
% 0.13/0.44 cC38(iV16462)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1208,f1210])).
% 0.13/0.44 fof(f1503,plain,(
% 0.13/0.44 cC56(iV16464)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1235,f1237])).
% 0.13/0.44 fof(f1504,plain,(
% 0.13/0.44 cC44(iV16464)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1503,f739])).
% 0.13/0.44 fof(f1505,plain,(
% 0.13/0.44 cC42(iV16464)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1504,f652])).
% 0.13/0.44 fof(f1506,plain,(
% 0.13/0.44 cC38(iV16465)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1240,f1252])).
% 0.13/0.44 fof(f1507,plain,(
% 0.13/0.44 $false|sQ47_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1506,f1417])).
% 0.13/0.44 fof(f1508,plain,(
% 0.13/0.44 sQ47_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1507])).
% 0.13/0.44 fof(f1509,plain,(
% 0.13/0.44 $false|sQ46_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1414,f290])).
% 0.13/0.44 fof(f1510,plain,(
% 0.13/0.44 sQ46_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1509])).
% 0.13/0.44 fof(f1511,plain,(
% 0.13/0.44 $false|sQ45_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1411,f1504])).
% 0.13/0.44 fof(f1512,plain,(
% 0.13/0.44 sQ45_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1511])).
% 0.13/0.44 fof(f1513,plain,(
% 0.13/0.44 $false|sQ44_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1408,f1505])).
% 0.13/0.44 fof(f1514,plain,(
% 0.13/0.44 sQ44_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1513])).
% 0.13/0.44 fof(f1515,plain,(
% 0.13/0.44 $false|sQ43_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1405,f1503])).
% 0.13/0.44 fof(f1516,plain,(
% 0.13/0.44 sQ43_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1515])).
% 0.13/0.44 fof(f1517,plain,(
% 0.13/0.44 $false|sQ42_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1402,f1448])).
% 0.13/0.44 fof(f1518,plain,(
% 0.13/0.44 sQ42_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1517])).
% 0.13/0.44 fof(f1519,plain,(
% 0.13/0.44 $false|sQ41_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1399,f290])).
% 0.13/0.44 fof(f1520,plain,(
% 0.13/0.44 sQ41_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1519])).
% 0.13/0.44 fof(f1521,plain,(
% 0.13/0.44 $false|sQ40_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1396,f1447])).
% 0.13/0.44 fof(f1522,plain,(
% 0.13/0.44 sQ40_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1521])).
% 0.13/0.44 fof(f1523,plain,(
% 0.13/0.44 $false|sQ39_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1393,f1446])).
% 0.13/0.44 fof(f1524,plain,(
% 0.13/0.44 sQ39_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1523])).
% 0.13/0.44 fof(f1525,plain,(
% 0.13/0.44 $false|sQ38_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1390,f290])).
% 0.13/0.44 fof(f1526,plain,(
% 0.13/0.44 sQ38_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1525])).
% 0.13/0.44 fof(f1527,plain,(
% 0.13/0.44 $false|sQ37_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1387,f1502])).
% 0.13/0.44 fof(f1528,plain,(
% 0.13/0.44 sQ37_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1527])).
% 0.13/0.44 fof(f1529,plain,(
% 0.13/0.44 $false|sQ36_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1384,f290])).
% 0.13/0.44 fof(f1530,plain,(
% 0.13/0.44 sQ36_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1529])).
% 0.13/0.44 fof(f1531,plain,(
% 0.13/0.44 $false|sQ35_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1381,f1496])).
% 0.13/0.44 fof(f1532,plain,(
% 0.13/0.44 sQ35_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1531])).
% 0.13/0.44 fof(f1533,plain,(
% 0.13/0.44 $false|sQ34_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1378,f1492])).
% 0.13/0.44 fof(f1534,plain,(
% 0.13/0.44 sQ34_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1533])).
% 0.13/0.44 fof(f1535,plain,(
% 0.13/0.44 $false|sQ33_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1375,f1497])).
% 0.13/0.44 fof(f1536,plain,(
% 0.13/0.44 sQ33_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1535])).
% 0.13/0.44 fof(f1537,plain,(
% 0.13/0.44 $false|sQ32_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1372,f290])).
% 0.13/0.44 fof(f1538,plain,(
% 0.13/0.44 sQ32_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1537])).
% 0.13/0.44 fof(f1539,plain,(
% 0.13/0.44 $false|sQ31_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1369,f1493])).
% 0.13/0.44 fof(f1540,plain,(
% 0.13/0.44 sQ31_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1539])).
% 0.13/0.44 fof(f1541,plain,(
% 0.13/0.44 $false|sQ30_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1366,f290])).
% 0.13/0.44 fof(f1542,plain,(
% 0.13/0.44 sQ30_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1541])).
% 0.13/0.44 fof(f1560,plain,(
% 0.13/0.44 cC106(iV16439)|~cC104(iV16439)),
% 0.13/0.44 inference(resolution,[status(thm)],[f350,f1090])).
% 0.13/0.44 fof(f1561,plain,(
% 0.13/0.44 sQ7_spl|~sQ6_spl),
% 0.13/0.44 inference(split_clause,[status(thm)],[f1560,f1295,f1292])).
% 0.13/0.44 fof(f1562,plain,(
% 0.13/0.44 $false|sQ49_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1430,f1101])).
% 0.13/0.44 fof(f1563,plain,(
% 0.13/0.44 sQ49_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1562])).
% 0.13/0.44 fof(f1566,plain,(
% 0.13/0.44 cC108(iV16439)|~cC28(iV16439)|~sQ7_spl),
% 0.13/0.44 inference(resolution,[status(thm)],[f1296,f355])).
% 0.13/0.44 fof(f1568,plain,(
% 0.13/0.44 sQ5_spl|~sQ8_spl|~sQ7_spl),
% 0.13/0.44 inference(split_clause,[status(thm)],[f1566,f1289,f1298,f1295])).
% 0.13/0.44 fof(f1569,plain,(
% 0.13/0.44 ~cC108(iV16439)|sQ8_spl),
% 0.13/0.44 inference(resolution,[status(thm)],[f1300,f353])).
% 0.13/0.44 fof(f1572,plain,(
% 0.13/0.44 cC42(iV16455)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1498,f1148])).
% 0.13/0.44 fof(f1578,plain,(
% 0.13/0.44 cC60(iV16453)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1499,f1133])).
% 0.13/0.44 fof(f1652,plain,(
% 0.13/0.44 cC108(iV16439)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1084,f1091])).
% 0.13/0.44 fof(f1653,plain,(
% 0.13/0.44 $false|sQ8_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1652,f1569])).
% 0.13/0.44 fof(f1654,plain,(
% 0.13/0.44 sQ8_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1653])).
% 0.13/0.44 fof(f1656,plain,(
% 0.13/0.44 cC130(iV16439)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1085,f1091])).
% 0.13/0.44 fof(f1677,plain,(
% 0.13/0.44 cC88(iV16449)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1120,f1118])).
% 0.13/0.44 fof(f1689,plain,(
% 0.13/0.44 cC86xcomp(iV16449)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1677,f990])).
% 0.13/0.44 fof(f1690,plain,(
% 0.13/0.44 cC84xcomp(iV16449)),
% 0.13/0.44 inference(resolution,[status(thm)],[f1677,f989])).
% 0.13/0.44 fof(f1822,plain,(
% 0.13/0.44 cC38(iV16457)|~cC36xcomp(iV16457)),
% 0.13/0.44 inference(resolution,[status(thm)],[f603,f1154])).
% 0.13/0.44 fof(f1823,plain,(
% 0.13/0.44 cC38(iV16448)|~cC36xcomp(iV16448)),
% 0.13/0.44 inference(resolution,[status(thm)],[f603,f1107])).
% 0.13/0.44 fof(f1837,definition,(
% 0.13/0.44 sQ79_spl <=> (cC36xcomp(iV16457))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1839,plain,(
% 0.13/0.44 ~cC36xcomp(iV16457)|sQ79_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1837])).
% 0.13/0.44 fof(f1840,plain,(
% 0.13/0.44 sQ24_spl|~sQ79_spl),
% 0.13/0.44 inference(split_clause,[status(thm)],[f1822,f1346,f1837])).
% 0.13/0.44 fof(f1841,definition,(
% 0.13/0.44 sQ80_spl <=> (cC36xcomp(iV16448))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1843,plain,(
% 0.13/0.44 ~cC36xcomp(iV16448)|sQ80_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1841])).
% 0.13/0.44 fof(f1844,plain,(
% 0.13/0.44 sQ14_spl|~sQ80_spl),
% 0.13/0.44 inference(split_clause,[status(thm)],[f1823,f1316,f1841])).
% 0.13/0.44 fof(f1916,plain,(
% 0.13/0.44 $false|sQ25_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1351,f290])).
% 0.13/0.44 fof(f1917,plain,(
% 0.13/0.44 sQ25_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1916])).
% 0.13/0.44 fof(f1918,plain,(
% 0.13/0.44 $false|sQ23_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1345,f290])).
% 0.13/0.44 fof(f1919,plain,(
% 0.13/0.44 sQ23_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1918])).
% 0.13/0.44 fof(f1920,plain,(
% 0.13/0.44 $false|sQ22_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1342,f1572])).
% 0.13/0.44 fof(f1921,plain,(
% 0.13/0.44 sQ22_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1920])).
% 0.13/0.44 fof(f1922,plain,(
% 0.13/0.44 $false|sQ19_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1333,f1578])).
% 0.13/0.44 fof(f1923,plain,(
% 0.13/0.44 sQ19_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1922])).
% 0.13/0.44 fof(f1924,plain,(
% 0.13/0.44 $false|sQ18_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1330,f290])).
% 0.13/0.44 fof(f1925,plain,(
% 0.13/0.44 sQ18_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1924])).
% 0.13/0.44 fof(f1926,plain,(
% 0.13/0.44 $false|sQ15_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1321,f290])).
% 0.13/0.44 fof(f1927,plain,(
% 0.13/0.44 sQ15_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1926])).
% 0.13/0.44 fof(f1928,plain,(
% 0.13/0.44 $false|sQ13_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1315,f290])).
% 0.13/0.44 fof(f1929,plain,(
% 0.13/0.44 sQ13_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1928])).
% 0.13/0.44 fof(f1930,plain,(
% 0.13/0.44 $false|sQ12_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1312,f1444])).
% 0.13/0.44 fof(f1931,plain,(
% 0.13/0.44 sQ12_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1930])).
% 0.13/0.44 fof(f1932,plain,(
% 0.13/0.44 $false|sQ11_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1309,f1445])).
% 0.13/0.44 fof(f1933,plain,(
% 0.13/0.44 sQ11_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1932])).
% 0.13/0.44 fof(f1934,plain,(
% 0.13/0.44 $false|sQ10_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1306,f1440])).
% 0.13/0.44 fof(f1935,plain,(
% 0.13/0.44 sQ10_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1934])).
% 0.13/0.44 fof(f1936,plain,(
% 0.13/0.44 $false|sQ9_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1303,f290])).
% 0.13/0.44 fof(f1937,plain,(
% 0.13/0.44 sQ9_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1936])).
% 0.13/0.44 fof(f1938,plain,(
% 0.13/0.44 $false|sQ4_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1288,f1656])).
% 0.13/0.44 fof(f1939,plain,(
% 0.13/0.44 sQ4_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1938])).
% 0.13/0.44 fof(f1940,plain,(
% 0.13/0.44 $false|~sQ1_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1278,f291])).
% 0.13/0.44 fof(f1941,plain,(
% 0.13/0.44 ~sQ1_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1940])).
% 0.13/0.44 fof(f1942,plain,(
% 0.13/0.44 $false|sQ0_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1276,f290])).
% 0.13/0.44 fof(f1943,plain,(
% 0.13/0.44 sQ0_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1942])).
% 0.13/0.44 fof(f1944,plain,(
% 0.13/0.44 ~cC30xcomp(iV16459)|~cC32xcomp(iV16459)|sQ28_spl),
% 0.13/0.44 inference(resolution,[status(thm)],[f1360,f575])).
% 0.13/0.44 fof(f1945,definition,(
% 0.13/0.44 sQ87_spl <=> (cC30xcomp(iV16459))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1947,plain,(
% 0.13/0.44 ~cC30xcomp(iV16459)|sQ87_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1945])).
% 0.13/0.44 fof(f1948,definition,(
% 0.13/0.44 sQ88_spl <=> (cC32xcomp(iV16459))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1950,plain,(
% 0.13/0.44 ~cC32xcomp(iV16459)|sQ88_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1948])).
% 0.13/0.44 fof(f1951,plain,(
% 0.13/0.44 ~sQ87_spl|~sQ88_spl|sQ28_spl),
% 0.13/0.44 inference(split_clause,[status(thm)],[f1944,f1945,f1948,f1358])).
% 0.13/0.44 fof(f1952,plain,(
% 0.13/0.44 $false|sQ88_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1950,f1175])).
% 0.13/0.44 fof(f1953,plain,(
% 0.13/0.44 sQ88_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1952])).
% 0.13/0.44 fof(f1954,plain,(
% 0.13/0.44 $false|sQ87_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1947,f1168])).
% 0.13/0.44 fof(f1955,plain,(
% 0.13/0.44 sQ87_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1954])).
% 0.13/0.44 fof(f1956,plain,(
% 0.13/0.44 ~cC40xcomp(iV16455)|~cC42(iV16455)|sQ21_spl),
% 0.13/0.44 inference(resolution,[status(thm)],[f1339,f653])).
% 0.13/0.44 fof(f1957,definition,(
% 0.13/0.44 sQ89_spl <=> (cC40xcomp(iV16455))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1959,plain,(
% 0.13/0.44 ~cC40xcomp(iV16455)|sQ89_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1957])).
% 0.13/0.44 fof(f1960,plain,(
% 0.13/0.44 ~sQ89_spl|~sQ22_spl|sQ21_spl),
% 0.13/0.44 inference(split_clause,[status(thm)],[f1956,f1957,f1340,f1337])).
% 0.13/0.44 fof(f1961,plain,(
% 0.13/0.44 $false|sQ89_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1959,f1137])).
% 0.13/0.44 fof(f1962,plain,(
% 0.13/0.44 sQ89_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1961])).
% 0.13/0.44 fof(f1977,plain,(
% 0.13/0.44 ~cC46xcomp(iV16459)|~cC48xcomp(iV16459)|sQ26_spl),
% 0.13/0.44 inference(resolution,[status(thm)],[f690,f1354])).
% 0.13/0.44 fof(f1980,definition,(
% 0.13/0.44 sQ90_spl <=> (cC46xcomp(iV16459))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1982,plain,(
% 0.13/0.44 ~cC46xcomp(iV16459)|sQ90_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1980])).
% 0.13/0.44 fof(f1983,definition,(
% 0.13/0.44 sQ91_spl <=> (cC48xcomp(iV16459))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f1985,plain,(
% 0.13/0.44 ~cC48xcomp(iV16459)|sQ91_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f1983])).
% 0.13/0.44 fof(f1986,plain,(
% 0.13/0.44 ~sQ90_spl|~sQ91_spl|sQ26_spl),
% 0.13/0.44 inference(split_clause,[status(thm)],[f1977,f1980,f1983,f1352])).
% 0.13/0.44 fof(f1987,plain,(
% 0.13/0.44 $false|sQ91_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1985,f1176])).
% 0.13/0.44 fof(f1988,plain,(
% 0.13/0.44 sQ91_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1987])).
% 0.13/0.44 fof(f1989,plain,(
% 0.13/0.44 $false|sQ90_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1982,f1171])).
% 0.13/0.44 fof(f1990,plain,(
% 0.13/0.44 sQ90_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f1989])).
% 0.13/0.44 fof(f2029,plain,(
% 0.13/0.44 ~cC54xcomp(iV16455)|~cC44(iV16455)|sQ20_spl),
% 0.13/0.44 inference(resolution,[status(thm)],[f740,f1336])).
% 0.13/0.44 fof(f2032,definition,(
% 0.13/0.44 sQ96_spl <=> (cC54xcomp(iV16455))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f2034,plain,(
% 0.13/0.44 ~cC54xcomp(iV16455)|sQ96_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f2032])).
% 0.13/0.44 fof(f2035,plain,(
% 0.13/0.44 ~sQ96_spl|~sQ21_spl|sQ20_spl),
% 0.13/0.44 inference(split_clause,[status(thm)],[f2029,f2032,f1337,f1334])).
% 0.13/0.44 fof(f2036,plain,(
% 0.13/0.44 $false|sQ96_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f2034,f1144])).
% 0.13/0.44 fof(f2037,plain,(
% 0.13/0.44 sQ96_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f2036])).
% 0.13/0.44 fof(f2071,plain,(
% 0.13/0.44 ~cC60(iV16453)|~cC58xcomp(iV16453)|sQ17_spl),
% 0.13/0.44 inference(resolution,[status(thm)],[f795,f1327])).
% 0.13/0.44 fof(f2074,definition,(
% 0.13/0.44 sQ98_spl <=> (cC58xcomp(iV16453))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f2076,plain,(
% 0.13/0.44 ~cC58xcomp(iV16453)|sQ98_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f2074])).
% 0.13/0.44 fof(f2077,plain,(
% 0.13/0.44 ~sQ19_spl|~sQ98_spl|sQ17_spl),
% 0.13/0.44 inference(split_clause,[status(thm)],[f2071,f1331,f2074,f1325])).
% 0.13/0.44 fof(f2078,plain,(
% 0.13/0.44 $false|sQ98_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f2076,f1132])).
% 0.13/0.44 fof(f2079,plain,(
% 0.13/0.44 sQ98_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f2078])).
% 0.13/0.44 fof(f2129,plain,(
% 0.13/0.44 ~cC64xcomp(iV16459)|~cC66xcomp(iV16459)|sQ29_spl),
% 0.13/0.44 inference(resolution,[status(thm)],[f837,f1363])).
% 0.13/0.44 fof(f2132,definition,(
% 0.13/0.44 sQ100_spl <=> (cC64xcomp(iV16459))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f2134,plain,(
% 0.13/0.44 ~cC64xcomp(iV16459)|sQ100_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f2132])).
% 0.13/0.44 fof(f2135,definition,(
% 0.13/0.44 sQ101_spl <=> (cC66xcomp(iV16459))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f2137,plain,(
% 0.13/0.44 ~cC66xcomp(iV16459)|sQ101_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f2135])).
% 0.13/0.44 fof(f2138,plain,(
% 0.13/0.44 ~sQ100_spl|~sQ101_spl|sQ29_spl),
% 0.13/0.44 inference(split_clause,[status(thm)],[f2129,f2132,f2135,f1361])).
% 0.13/0.44 fof(f2139,plain,(
% 0.13/0.44 $false|sQ101_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f2137,f1180])).
% 0.13/0.44 fof(f2140,plain,(
% 0.13/0.44 sQ101_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f2139])).
% 0.13/0.44 fof(f2141,plain,(
% 0.13/0.44 $false|sQ100_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f2134,f1172])).
% 0.13/0.44 fof(f2142,plain,(
% 0.13/0.44 sQ100_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f2141])).
% 0.13/0.44 fof(f2240,plain,(
% 0.13/0.44 cC76(iV16453)|~cC62(iV16453)),
% 0.13/0.44 inference(resolution,[status(thm)],[f904,f1122])).
% 0.13/0.44 fof(f2243,plain,(
% 0.13/0.44 sQ16_spl|~sQ17_spl),
% 0.13/0.44 inference(split_clause,[status(thm)],[f2240,f1322,f1325])).
% 0.13/0.44 fof(f2858,plain,(
% 0.13/0.44 cC88(iV16449)|~cC84xcomp(iV16449)),
% 0.13/0.44 inference(resolution,[status(thm)],[f991,f1689])).
% 0.13/0.44 fof(f2859,plain,(
% 0.13/0.44 cC88(iV16459)|~cC84xcomp(iV16459)),
% 0.13/0.44 inference(resolution,[status(thm)],[f991,f1174])).
% 0.13/0.44 fof(f2860,definition,(
% 0.13/0.44 sQ223_spl <=> (cC88(iV16449))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f2863,definition,(
% 0.13/0.44 sQ224_spl <=> (cC84xcomp(iV16449))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f2865,plain,(
% 0.13/0.44 ~cC84xcomp(iV16449)|sQ224_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f2863])).
% 0.13/0.44 fof(f2866,plain,(
% 0.13/0.44 sQ223_spl|~sQ224_spl),
% 0.13/0.44 inference(split_clause,[status(thm)],[f2858,f2860,f2863])).
% 0.13/0.44 fof(f2867,definition,(
% 0.13/0.44 sQ225_spl <=> (cC84xcomp(iV16459))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition])).
% 0.13/0.44 fof(f2869,plain,(
% 0.13/0.44 ~cC84xcomp(iV16459)|sQ225_spl),
% 0.13/0.44 inference(component_clause,[status(thm)],[f2867])).
% 0.13/0.44 fof(f2870,plain,(
% 0.13/0.44 sQ27_spl|~sQ225_spl),
% 0.13/0.44 inference(split_clause,[status(thm)],[f2859,f1355,f2867])).
% 0.13/0.44 fof(f2871,plain,(
% 0.13/0.44 $false|sQ225_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f2869,f1169])).
% 0.13/0.44 fof(f2872,plain,(
% 0.13/0.44 sQ225_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f2871])).
% 0.13/0.44 fof(f2873,plain,(
% 0.13/0.44 $false|sQ224_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f2865,f1690])).
% 0.13/0.44 fof(f2874,plain,(
% 0.13/0.44 sQ224_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f2873])).
% 0.13/0.44 fof(f2879,plain,(
% 0.13/0.44 ~xsd_string(sK116_skl)|~sQ3_spl),
% 0.13/0.44 inference(resolution,[status(thm)],[f1284,f294])).
% 0.13/0.44 fof(f2880,plain,(
% 0.13/0.44 $false|~sQ2_spl|~sQ3_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f2879,f1281])).
% 0.13/0.44 fof(f2881,plain,(
% 0.13/0.44 ~sQ2_spl|~sQ3_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f2880])).
% 0.13/0.44 fof(f2902,plain,(
% 0.13/0.44 xsd_string(sK116_skl)|sQ3_spl),
% 0.13/0.44 inference(resolution,[status(thm)],[f1285,f295])).
% 0.13/0.44 fof(f2903,plain,(
% 0.13/0.44 sQ2_spl|sQ3_spl),
% 0.13/0.44 inference(split_clause,[status(thm)],[f2902,f1280,f1283])).
% 0.13/0.44 fof(f2904,plain,(
% 0.13/0.44 $false|sQ80_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1843,f1115])).
% 0.13/0.44 fof(f2905,plain,(
% 0.13/0.44 sQ80_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f2904])).
% 0.13/0.44 fof(f2906,plain,(
% 0.13/0.44 $false|sQ79_spl),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1839,f1159])).
% 0.13/0.44 fof(f2907,plain,(
% 0.13/0.44 sQ79_spl),
% 0.13/0.44 inference(contradiction_clause,[status(thm)],[f2906])).
% 0.13/0.44 fof(f2908,plain,(
% 0.13/0.44 $false),
% 0.13/0.44 inference(sat_refutation,[status(thm)],[f1421,f1422,f1424,f1431,f1508,f1510,f1512,f1514,f1516,f1518,f1520,f1522,f1524,f1526,f1528,f1530,f1532,f1534,f1536,f1538,f1540,f1542,f1561,f1563,f1568,f1654,f1840,f1844,f1917,f1919,f1921,f1923,f1925,f1927,f1929,f1931,f1933,f1935,f1937,f1939,f1941,f1943,f1951,f1953,f1955,f1960,f1962,f1986,f1988,f1990,f2035,f2037,f2077,f2079,f2138,f2140,f2142,f2243,f2866,f2870,f2872,f2874,f2881,f2903,f2905,f2907])).
% 0.13/0.44 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.45 % Elapsed time: 0.087376 seconds
% 0.13/0.45 % CPU time: 0.429195 seconds
% 0.13/0.45 % Total memory used: 43.652 MB
% 0.13/0.45 % Net memory used: 43.517 MB
%------------------------------------------------------------------------------