%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS153+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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.12s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS153+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n010.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sun Sep 20 22:55:25 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.12/0.49 % Refutation found
% 0.12/0.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.49 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.49 fof(f1,axiom,(
% 0.12/0.49 (! [X] :( cowlThing(X)& ~ cowlNothing(X) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f2,axiom,(
% 0.12/0.49 (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f4,axiom,(
% 0.12/0.49 (! [X] :( cC100(X)<=> (? [Y] :( rR1(X,Y)& ~ cC98(Y) ) )) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f5,axiom,(
% 0.12/0.49 (! [X] :( cC104(X)<=> (? [Y] :( rR1(X,Y)& ~ cC102(Y) ) )) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f6,axiom,(
% 0.12/0.49 (! [X] :( cC106(X)<=> ( ~ cC100(X)& cC104(X) ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f7,axiom,(
% 0.12/0.49 (! [X] :( cC108(X)<=> ( cC28(X)& cC106(X) ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f25,axiom,(
% 0.12/0.49 (! [X] :( cC32(X)<=> ( ~ cC2(X)& ~ cC4(X) ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f26,axiom,(
% 0.12/0.49 (! [X] :( cC34(X)<=> ( ~ cC32(X)& ~ cC30(X) ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f28,axiom,(
% 0.12/0.49 (! [X] :( cC38(X)<=> ( ~ cC36(X)& cTOP(X) ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f30,axiom,(
% 0.12/0.49 (! [X] :( cC42(X)<=> (? [Y] :( rR1(X,Y)& ~ cC8(Y) ) )) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f31,axiom,(
% 0.12/0.49 (! [X] :( cC44(X)<=> ( ~ cC40(X)& cC42(X) ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f34,axiom,(
% 0.12/0.49 (! [X] :( cC50(X)<=> ( ~ cC46(X)& ~ cC48(X) ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f37,axiom,(
% 0.12/0.49 (! [X] :( cC56(X)<=> ( cC44(X)& ~ cC54(X) ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f40,axiom,(
% 0.12/0.49 (! [X] :( cC60(X)<=> (? [Y] :( rR1(X,Y)& ~ cC12(Y) ) )) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f41,axiom,(
% 0.12/0.49 (! [X] :( cC62(X)<=> ( cC60(X)& ~ cC58(X) ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f44,axiom,(
% 0.12/0.49 (! [X] :( cC68(X)<=> ( ~ cC64(X)& ~ cC66(X) ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f48,axiom,(
% 0.12/0.49 (! [X] :( cC76(X)<=> ( ~ cC74(X)& cC62(X) ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f51,axiom,(
% 0.12/0.49 (! [X] :( cC82(X)<=> ( ~ cC78(X)& cC80(X) ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f53,axiom,(
% 0.12/0.49 (! [X] :( cC86(X)<=> ( ~ cC12(X)& ~ cC2(X) ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f54,axiom,(
% 0.12/0.49 (! [X] :( cC88(X)<=> ( ~ cC84(X)& ~ cC86(X) ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f59,axiom,(
% 0.12/0.49 (! [X] :( cC98(X)<=> ( ~ cC96(X)& cC82(X) ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f60,axiom,(
% 0.12/0.49 (! [X] :( cTEST(X)<=> ( cC108(X)& cC130(X) ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f61,axiom,(
% 0.12/0.49 (! [X] :( rR1(iV16439,X)=> cC98(X) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f62,axiom,(
% 0.12/0.49 cTEST(iV16439) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f63,axiom,(
% 0.12/0.49 ~ cC100(iV16439) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f65,axiom,(
% 0.12/0.49 rR1(iV16439,iV16440) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f68,axiom,(
% 0.12/0.49 (! [X] :( rR1(iV16440,X)=> cC76(X) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f70,axiom,(
% 0.12/0.49 ~ cC102(iV16440) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f74,axiom,(
% 0.12/0.49 rR1(iV16440,iV16463) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f77,axiom,(
% 0.12/0.49 ~ cC36(iV16448) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f80,axiom,(
% 0.12/0.49 cTOP(iV16448) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f92,axiom,(
% 0.12/0.49 ~ cC58(iV16453) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f93,axiom,(
% 0.12/0.49 ~ cC74(iV16453) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f94,axiom,(
% 0.12/0.49 (! [X] :( rR1(iV16453,X)=> cC56(X) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f97,axiom,(
% 0.12/0.49 rR1(iV16453,iV16461) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f99,axiom,(
% 0.12/0.49 ~ cC40(iV16455) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f104,axiom,(
% 0.12/0.49 ~ cC54(iV16455) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f107,axiom,(
% 0.12/0.49 (! [X] :( rR1(iV16455,X)=> cC38(X) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f108,axiom,(
% 0.12/0.49 rR1(iV16455,iV16460) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f109,axiom,(
% 0.12/0.49 ~ cC36(iV16457) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f114,axiom,(
% 0.12/0.49 cTOP(iV16457) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f121,axiom,(
% 0.12/0.49 ~ cC48(iV16459) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f122,axiom,(
% 0.12/0.49 ~ cC30(iV16459) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f124,axiom,(
% 0.12/0.49 ~ cC86(iV16459) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f125,axiom,(
% 0.12/0.49 ~ cC46(iV16459) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f128,axiom,(
% 0.12/0.49 ~ cC66(iV16459) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f130,axiom,(
% 0.12/0.49 ~ cC8(iV16459) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f131,axiom,(
% 0.12/0.49 ~ cC2(iV16459) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f133,axiom,(
% 0.12/0.49 ~ cC84(iV16459) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f134,axiom,(
% 0.12/0.49 ~ cC64(iV16459) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f136,axiom,(
% 0.12/0.49 ~ cC32(iV16459) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f142,axiom,(
% 0.12/0.49 ~ cC8(iV16460) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f152,axiom,(
% 0.12/0.49 ~ cC12(iV16461) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f155,axiom,(
% 0.12/0.49 (! [X] :( rR1(iV16461,X)=> cC38(X) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f158,axiom,(
% 0.12/0.49 rR1(iV16461,iV16462) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f160,axiom,(
% 0.12/0.49 ~ cC8(iV16462) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f172,axiom,(
% 0.12/0.49 (! [X] :( rR1(iV16463,X)=> cC56(X) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f178,axiom,(
% 0.12/0.49 rR1(iV16463,iV16464) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f183,axiom,(
% 0.12/0.49 (! [X] :( rR1(iV16464,X)=> cC38(X) ) )),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f184,axiom,(
% 0.12/0.49 ~ cC12(iV16464) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f189,axiom,(
% 0.12/0.49 rR1(iV16464,iV16465) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f195,axiom,(
% 0.12/0.49 ~ cC8(iV16465) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f201,conjecture,(
% 0.12/0.49 ( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& cC106(iV16439)& cC28(iV16439)& cC130(iV16439)& cowlThing(iV16439)& cC108(iV16439)& cC104(iV16439)& cC80(iV16440)& cowlThing(iV16440)& cC82(iV16440)& cC98(iV16440)& cowlThing(iV16448)& cC38(iV16448)& cC62(iV16453)& cowlThing(iV16453)& cC76(iV16453)& cC60(iV16453)& cC44(iV16455)& cowlThing(iV16455)& cC56(iV16455)& cC42(iV16455)& cowlThing(iV16457)& cC38(iV16457)& cC68(iV16459)& cowlThing(iV16459)& cC88(iV16459)& cC50(iV16459)& cC34(iV16459)& cowlThing(iV16460)& cC38(iV16460)& cC44(iV16461)& cowlThing(iV16461)& cC56(iV16461)& cC42(iV16461)& cowlThing(iV16462)& cC38(iV16462)& cC62(iV16463)& cowlThing(iV16463)& cC76(iV16463)& cC60(iV16463)& cC44(iV16464)& cowlThing(iV16464)& cC56(iV16464)& cC42(iV16464)& cowlThing(iV16465)& cC38(iV16465) ) ),
% 0.12/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f202,negated_conjecture,(
% 0.12/0.49 ~(( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& cC106(iV16439)& cC28(iV16439)& cC130(iV16439)& cowlThing(iV16439)& cC108(iV16439)& cC104(iV16439)& cC80(iV16440)& cowlThing(iV16440)& cC82(iV16440)& cC98(iV16440)& cowlThing(iV16448)& cC38(iV16448)& cC62(iV16453)& cowlThing(iV16453)& cC76(iV16453)& cC60(iV16453)& cC44(iV16455)& cowlThing(iV16455)& cC56(iV16455)& cC42(iV16455)& cowlThing(iV16457)& cC38(iV16457)& cC68(iV16459)& cowlThing(iV16459)& cC88(iV16459)& cC50(iV16459)& cC34(iV16459)& cowlThing(iV16460)& cC38(iV16460)& cC44(iV16461)& cowlThing(iV16461)& cC56(iV16461)& cC42(iV16461)& cowlThing(iV16462)& cC38(iV16462)& cC62(iV16463)& cowlThing(iV16463)& cC76(iV16463)& cC60(iV16463)& cC44(iV16464)& cowlThing(iV16464)& cC56(iV16464)& cC42(iV16464)& cowlThing(iV16465)& cC38(iV16465) ) )),
% 0.12/0.49 inference(negated_conjecture,[status(cth)],[f201])).
% 0.12/0.49 fof(f203,plain,(
% 0.12/0.49 (![X]: cowlThing(X))&(![X]: ~cowlNothing(X))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f1])).
% 0.12/0.49 fof(f204,plain,(
% 0.12/0.49 ![X0]: (cowlThing(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f203])).
% 0.12/0.49 fof(f205,plain,(
% 0.12/0.49 ![X0]: (~cowlNothing(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f203])).
% 0.12/0.49 fof(f206,plain,(
% 0.12/0.49 ![X]: ((~xsd_string(X)|~xsd_integer(X))&(xsd_string(X)|xsd_integer(X)))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f2])).
% 0.12/0.49 fof(f207,plain,(
% 0.12/0.49 (![X]: (~xsd_string(X)|~xsd_integer(X)))&(![X]: (xsd_string(X)|xsd_integer(X)))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f206])).
% 0.12/0.49 fof(f208,plain,(
% 0.12/0.49 ![X0]: (~xsd_string(X0)|~xsd_integer(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f207])).
% 0.12/0.49 fof(f209,plain,(
% 0.12/0.49 ![X0]: (xsd_string(X0)|xsd_integer(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f207])).
% 0.12/0.49 fof(f215,plain,(
% 0.12/0.49 ![X]: ((~cC100(X)|(?[Y]: (rR1(X,Y)&~cC98(Y))))&(cC100(X)|(![Y]: (~rR1(X,Y)|cC98(Y)))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f4])).
% 0.12/0.49 fof(f216,plain,(
% 0.12/0.49 (![X]: (~cC100(X)|(?[Y]: (rR1(X,Y)&~cC98(Y)))))&(![X]: (cC100(X)|(![Y]: (~rR1(X,Y)|cC98(Y)))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f215])).
% 0.12/0.49 fof(f217,plain,(
% 0.12/0.49 (![X]: (~cC100(X)|(rR1(X,sK0_skl(X))&~cC98(sK0_skl(X)))))&(![X]: (cC100(X)|(![Y]: (~rR1(X,Y)|cC98(Y)))))),
% 0.12/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Y,sK0_skl(X))],[f216])).
% 0.12/0.49 fof(f220,plain,(
% 0.12/0.49 ![X0,X1]: (cC100(X0)|~rR1(X0,X1)|cC98(X1))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f217])).
% 0.12/0.49 fof(f221,plain,(
% 0.12/0.49 ![X]: ((~cC104(X)|(?[Y]: (rR1(X,Y)&~cC102(Y))))&(cC104(X)|(![Y]: (~rR1(X,Y)|cC102(Y)))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f5])).
% 0.12/0.49 fof(f222,plain,(
% 0.12/0.49 (![X]: (~cC104(X)|(?[Y]: (rR1(X,Y)&~cC102(Y)))))&(![X]: (cC104(X)|(![Y]: (~rR1(X,Y)|cC102(Y)))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f221])).
% 0.12/0.49 fof(f223,plain,(
% 0.12/0.49 (![X]: (~cC104(X)|(rR1(X,sK1_skl(X))&~cC102(sK1_skl(X)))))&(![X]: (cC104(X)|(![Y]: (~rR1(X,Y)|cC102(Y)))))),
% 0.12/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Y,sK1_skl(X))],[f222])).
% 0.12/0.49 fof(f224,plain,(
% 0.12/0.49 ![X0]: (~cC104(X0)|rR1(X0,sK1_skl(X0)))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f223])).
% 0.12/0.49 fof(f226,plain,(
% 0.12/0.49 ![X0,X1]: (cC104(X0)|~rR1(X0,X1)|cC102(X1))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f223])).
% 0.12/0.49 fof(f227,plain,(
% 0.12/0.49 ![X]: ((~cC106(X)|(~cC100(X)&cC104(X)))&(cC106(X)|(cC100(X)|~cC104(X))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f6])).
% 0.12/0.49 fof(f228,plain,(
% 0.12/0.49 (![X]: (~cC106(X)|(~cC100(X)&cC104(X))))&(![X]: (cC106(X)|(cC100(X)|~cC104(X))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f227])).
% 0.12/0.49 fof(f231,plain,(
% 0.12/0.49 ![X0]: (cC106(X0)|cC100(X0)|~cC104(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f228])).
% 0.12/0.49 fof(f232,plain,(
% 0.12/0.49 ![X]: ((~cC108(X)|(cC28(X)&cC106(X)))&(cC108(X)|(~cC28(X)|~cC106(X))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f7])).
% 0.12/0.49 fof(f233,plain,(
% 0.12/0.49 (![X]: (~cC108(X)|(cC28(X)&cC106(X))))&(![X]: (cC108(X)|(~cC28(X)|~cC106(X))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f232])).
% 0.12/0.49 fof(f234,plain,(
% 0.12/0.49 ![X0]: (~cC108(X0)|cC28(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f233])).
% 0.12/0.49 fof(f236,plain,(
% 0.12/0.49 ![X0]: (cC108(X0)|~cC28(X0)|~cC106(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f233])).
% 0.12/0.49 fof(f332,plain,(
% 0.12/0.49 ![X]: ((~cC32(X)|(~cC2(X)&~cC4(X)))&(cC32(X)|(cC2(X)|cC4(X))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f25])).
% 0.12/0.49 fof(f333,plain,(
% 0.12/0.49 (![X]: (~cC32(X)|(~cC2(X)&~cC4(X))))&(![X]: (cC32(X)|(cC2(X)|cC4(X))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f332])).
% 0.12/0.49 fof(f336,plain,(
% 0.12/0.49 ![X0]: (cC32(X0)|cC2(X0)|cC4(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f333])).
% 0.12/0.49 fof(f337,plain,(
% 0.12/0.49 ![X]: ((~cC34(X)|(~cC32(X)&~cC30(X)))&(cC34(X)|(cC32(X)|cC30(X))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f26])).
% 0.12/0.49 fof(f338,plain,(
% 0.12/0.49 (![X]: (~cC34(X)|(~cC32(X)&~cC30(X))))&(![X]: (cC34(X)|(cC32(X)|cC30(X))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f337])).
% 0.12/0.49 fof(f341,plain,(
% 0.12/0.49 ![X0]: (cC34(X0)|cC32(X0)|cC30(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f338])).
% 0.12/0.49 fof(f348,plain,(
% 0.12/0.49 ![X]: ((~cC38(X)|(~cC36(X)&cTOP(X)))&(cC38(X)|(cC36(X)|~cTOP(X))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f28])).
% 0.12/0.49 fof(f349,plain,(
% 0.12/0.49 (![X]: (~cC38(X)|(~cC36(X)&cTOP(X))))&(![X]: (cC38(X)|(cC36(X)|~cTOP(X))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f348])).
% 0.12/0.49 fof(f352,plain,(
% 0.12/0.49 ![X0]: (cC38(X0)|cC36(X0)|~cTOP(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f349])).
% 0.12/0.49 fof(f359,plain,(
% 0.12/0.49 ![X]: ((~cC42(X)|(?[Y]: (rR1(X,Y)&~cC8(Y))))&(cC42(X)|(![Y]: (~rR1(X,Y)|cC8(Y)))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f30])).
% 0.12/0.49 fof(f360,plain,(
% 0.12/0.49 (![X]: (~cC42(X)|(?[Y]: (rR1(X,Y)&~cC8(Y)))))&(![X]: (cC42(X)|(![Y]: (~rR1(X,Y)|cC8(Y)))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f359])).
% 0.12/0.49 fof(f361,plain,(
% 0.12/0.49 (![X]: (~cC42(X)|(rR1(X,sK14_skl(X))&~cC8(sK14_skl(X)))))&(![X]: (cC42(X)|(![Y]: (~rR1(X,Y)|cC8(Y)))))),
% 0.12/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(Y,sK14_skl(X))],[f360])).
% 0.12/0.49 fof(f364,plain,(
% 0.12/0.49 ![X0,X1]: (cC42(X0)|~rR1(X0,X1)|cC8(X1))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f361])).
% 0.12/0.49 fof(f365,plain,(
% 0.12/0.49 ![X]: ((~cC44(X)|(~cC40(X)&cC42(X)))&(cC44(X)|(cC40(X)|~cC42(X))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f31])).
% 0.12/0.49 fof(f366,plain,(
% 0.12/0.49 (![X]: (~cC44(X)|(~cC40(X)&cC42(X))))&(![X]: (cC44(X)|(cC40(X)|~cC42(X))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f365])).
% 0.12/0.49 fof(f369,plain,(
% 0.12/0.49 ![X0]: (cC44(X0)|cC40(X0)|~cC42(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f366])).
% 0.12/0.49 fof(f380,plain,(
% 0.12/0.49 ![X]: ((~cC50(X)|(~cC46(X)&~cC48(X)))&(cC50(X)|(cC46(X)|cC48(X))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f34])).
% 0.12/0.49 fof(f381,plain,(
% 0.12/0.49 (![X]: (~cC50(X)|(~cC46(X)&~cC48(X))))&(![X]: (cC50(X)|(cC46(X)|cC48(X))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f380])).
% 0.12/0.49 fof(f384,plain,(
% 0.12/0.49 ![X0]: (cC50(X0)|cC46(X0)|cC48(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f381])).
% 0.12/0.49 fof(f397,plain,(
% 0.12/0.49 ![X]: ((~cC56(X)|(cC44(X)&~cC54(X)))&(cC56(X)|(~cC44(X)|cC54(X))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f37])).
% 0.12/0.49 fof(f398,plain,(
% 0.12/0.49 (![X]: (~cC56(X)|(cC44(X)&~cC54(X))))&(![X]: (cC56(X)|(~cC44(X)|cC54(X))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f397])).
% 0.12/0.49 fof(f399,plain,(
% 0.12/0.49 ![X0]: (~cC56(X0)|cC44(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f398])).
% 0.12/0.49 fof(f401,plain,(
% 0.12/0.49 ![X0]: (cC56(X0)|~cC44(X0)|cC54(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f398])).
% 0.12/0.49 fof(f413,plain,(
% 0.12/0.49 ![X]: ((~cC60(X)|(?[Y]: (rR1(X,Y)&~cC12(Y))))&(cC60(X)|(![Y]: (~rR1(X,Y)|cC12(Y)))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f40])).
% 0.12/0.49 fof(f414,plain,(
% 0.12/0.49 (![X]: (~cC60(X)|(?[Y]: (rR1(X,Y)&~cC12(Y)))))&(![X]: (cC60(X)|(![Y]: (~rR1(X,Y)|cC12(Y)))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f413])).
% 0.12/0.49 fof(f415,plain,(
% 0.12/0.49 (![X]: (~cC60(X)|(rR1(X,sK18_skl(X))&~cC12(sK18_skl(X)))))&(![X]: (cC60(X)|(![Y]: (~rR1(X,Y)|cC12(Y)))))),
% 0.12/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(Y,sK18_skl(X))],[f414])).
% 0.12/0.49 fof(f418,plain,(
% 0.12/0.49 ![X0,X1]: (cC60(X0)|~rR1(X0,X1)|cC12(X1))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f415])).
% 0.12/0.49 fof(f419,plain,(
% 0.12/0.49 ![X]: ((~cC62(X)|(cC60(X)&~cC58(X)))&(cC62(X)|(~cC60(X)|cC58(X))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f41])).
% 0.12/0.49 fof(f420,plain,(
% 0.12/0.49 (![X]: (~cC62(X)|(cC60(X)&~cC58(X))))&(![X]: (cC62(X)|(~cC60(X)|cC58(X))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f419])).
% 0.12/0.49 fof(f423,plain,(
% 0.12/0.49 ![X0]: (cC62(X0)|~cC60(X0)|cC58(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f420])).
% 0.12/0.49 fof(f434,plain,(
% 0.12/0.49 ![X]: ((~cC68(X)|(~cC64(X)&~cC66(X)))&(cC68(X)|(cC64(X)|cC66(X))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f44])).
% 0.12/0.49 fof(f435,plain,(
% 0.12/0.49 (![X]: (~cC68(X)|(~cC64(X)&~cC66(X))))&(![X]: (cC68(X)|(cC64(X)|cC66(X))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f434])).
% 0.12/0.49 fof(f438,plain,(
% 0.12/0.49 ![X0]: (cC68(X0)|cC64(X0)|cC66(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f435])).
% 0.12/0.49 fof(f457,plain,(
% 0.12/0.49 ![X]: ((~cC76(X)|(~cC74(X)&cC62(X)))&(cC76(X)|(cC74(X)|~cC62(X))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f48])).
% 0.12/0.49 fof(f458,plain,(
% 0.12/0.49 (![X]: (~cC76(X)|(~cC74(X)&cC62(X))))&(![X]: (cC76(X)|(cC74(X)|~cC62(X))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f457])).
% 0.12/0.49 fof(f460,plain,(
% 0.12/0.49 ![X0]: (~cC76(X0)|cC62(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f458])).
% 0.12/0.49 fof(f461,plain,(
% 0.12/0.49 ![X0]: (cC76(X0)|cC74(X0)|~cC62(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f458])).
% 0.12/0.49 fof(f474,plain,(
% 0.12/0.49 ![X]: ((~cC82(X)|(~cC78(X)&cC80(X)))&(cC82(X)|(cC78(X)|~cC80(X))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f51])).
% 0.12/0.49 fof(f475,plain,(
% 0.12/0.49 (![X]: (~cC82(X)|(~cC78(X)&cC80(X))))&(![X]: (cC82(X)|(cC78(X)|~cC80(X))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f474])).
% 0.12/0.49 fof(f477,plain,(
% 0.12/0.49 ![X0]: (~cC82(X0)|cC80(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f475])).
% 0.12/0.49 fof(f484,plain,(
% 0.12/0.49 ![X]: ((~cC86(X)|(~cC12(X)&~cC2(X)))&(cC86(X)|(cC12(X)|cC2(X))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f53])).
% 0.12/0.49 fof(f485,plain,(
% 0.12/0.49 (![X]: (~cC86(X)|(~cC12(X)&~cC2(X))))&(![X]: (cC86(X)|(cC12(X)|cC2(X))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f484])).
% 0.12/0.49 fof(f488,plain,(
% 0.12/0.49 ![X0]: (cC86(X0)|cC12(X0)|cC2(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f485])).
% 0.12/0.49 fof(f489,plain,(
% 0.12/0.49 ![X]: ((~cC88(X)|(~cC84(X)&~cC86(X)))&(cC88(X)|(cC84(X)|cC86(X))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f54])).
% 0.12/0.49 fof(f490,plain,(
% 0.12/0.49 (![X]: (~cC88(X)|(~cC84(X)&~cC86(X))))&(![X]: (cC88(X)|(cC84(X)|cC86(X))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f489])).
% 0.12/0.49 fof(f493,plain,(
% 0.12/0.49 ![X0]: (cC88(X0)|cC84(X0)|cC86(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f490])).
% 0.12/0.49 fof(f518,plain,(
% 0.12/0.49 ![X]: ((~cC98(X)|(~cC96(X)&cC82(X)))&(cC98(X)|(cC96(X)|~cC82(X))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f59])).
% 0.12/0.49 fof(f519,plain,(
% 0.12/0.49 (![X]: (~cC98(X)|(~cC96(X)&cC82(X))))&(![X]: (cC98(X)|(cC96(X)|~cC82(X))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f518])).
% 0.12/0.49 fof(f521,plain,(
% 0.12/0.49 ![X0]: (~cC98(X0)|cC82(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f519])).
% 0.12/0.49 fof(f523,plain,(
% 0.12/0.49 ![X]: ((~cTEST(X)|(cC108(X)&cC130(X)))&(cTEST(X)|(~cC108(X)|~cC130(X))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f60])).
% 0.12/0.49 fof(f524,plain,(
% 0.12/0.49 (![X]: (~cTEST(X)|(cC108(X)&cC130(X))))&(![X]: (cTEST(X)|(~cC108(X)|~cC130(X))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f523])).
% 0.12/0.49 fof(f525,plain,(
% 0.12/0.49 ![X0]: (~cTEST(X0)|cC108(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f524])).
% 0.12/0.49 fof(f526,plain,(
% 0.12/0.49 ![X0]: (~cTEST(X0)|cC130(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f524])).
% 0.12/0.49 fof(f528,plain,(
% 0.12/0.49 ![X]: (~rR1(iV16439,X)|cC98(X))),
% 0.12/0.49 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 0.12/0.49 fof(f529,plain,(
% 0.12/0.49 ![X0]: (~rR1(iV16439,X0)|cC98(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f528])).
% 0.12/0.49 fof(f530,plain,(
% 0.12/0.49 cTEST(iV16439)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f62])).
% 0.12/0.49 fof(f531,plain,(
% 0.12/0.49 ~cC100(iV16439)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f63])).
% 0.12/0.49 fof(f533,plain,(
% 0.12/0.49 rR1(iV16439,iV16440)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f65])).
% 0.12/0.49 fof(f536,plain,(
% 0.12/0.49 ![X]: (~rR1(iV16440,X)|cC76(X))),
% 0.12/0.49 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 0.12/0.49 fof(f537,plain,(
% 0.12/0.49 ![X0]: (~rR1(iV16440,X0)|cC76(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f536])).
% 0.12/0.49 fof(f540,plain,(
% 0.12/0.49 ~cC102(iV16440)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f70])).
% 0.12/0.49 fof(f544,plain,(
% 0.12/0.49 rR1(iV16440,iV16463)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f74])).
% 0.12/0.49 fof(f547,plain,(
% 0.12/0.49 ~cC36(iV16448)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f77])).
% 0.12/0.49 fof(f552,plain,(
% 0.12/0.49 cTOP(iV16448)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f80])).
% 0.12/0.49 fof(f568,plain,(
% 0.12/0.49 ~cC58(iV16453)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f92])).
% 0.12/0.49 fof(f569,plain,(
% 0.12/0.49 ~cC74(iV16453)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f93])).
% 0.12/0.49 fof(f570,plain,(
% 0.12/0.49 ![X]: (~rR1(iV16453,X)|cC56(X))),
% 0.12/0.49 inference(pre_NNF_transformation,[status(thm)],[f94])).
% 0.12/0.49 fof(f571,plain,(
% 0.12/0.49 ![X0]: (~rR1(iV16453,X0)|cC56(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f570])).
% 0.12/0.49 fof(f574,plain,(
% 0.12/0.49 rR1(iV16453,iV16461)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f97])).
% 0.12/0.49 fof(f576,plain,(
% 0.12/0.49 ~cC40(iV16455)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f99])).
% 0.12/0.49 fof(f584,plain,(
% 0.12/0.49 ~cC54(iV16455)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f104])).
% 0.12/0.49 fof(f587,plain,(
% 0.12/0.49 ![X]: (~rR1(iV16455,X)|cC38(X))),
% 0.12/0.49 inference(pre_NNF_transformation,[status(thm)],[f107])).
% 0.12/0.49 fof(f588,plain,(
% 0.12/0.49 ![X0]: (~rR1(iV16455,X0)|cC38(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f587])).
% 0.12/0.49 fof(f589,plain,(
% 0.12/0.49 rR1(iV16455,iV16460)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f108])).
% 0.12/0.49 fof(f590,plain,(
% 0.12/0.49 ~cC36(iV16457)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f109])).
% 0.12/0.49 fof(f598,plain,(
% 0.12/0.49 cTOP(iV16457)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f114])).
% 0.12/0.49 fof(f606,plain,(
% 0.12/0.49 ~cC48(iV16459)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f121])).
% 0.12/0.49 fof(f607,plain,(
% 0.12/0.49 ~cC30(iV16459)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f122])).
% 0.12/0.49 fof(f609,plain,(
% 0.12/0.49 ~cC86(iV16459)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f124])).
% 0.12/0.49 fof(f610,plain,(
% 0.12/0.49 ~cC46(iV16459)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f125])).
% 0.12/0.49 fof(f613,plain,(
% 0.12/0.49 ~cC66(iV16459)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f128])).
% 0.12/0.49 fof(f615,plain,(
% 0.12/0.49 ~cC8(iV16459)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f130])).
% 0.12/0.49 fof(f616,plain,(
% 0.12/0.49 ~cC2(iV16459)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f131])).
% 0.12/0.49 fof(f618,plain,(
% 0.12/0.49 ~cC84(iV16459)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f133])).
% 0.12/0.49 fof(f619,plain,(
% 0.12/0.49 ~cC64(iV16459)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f134])).
% 0.12/0.49 fof(f621,plain,(
% 0.12/0.49 ~cC32(iV16459)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f136])).
% 0.12/0.49 fof(f628,plain,(
% 0.12/0.49 ~cC8(iV16460)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f142])).
% 0.12/0.49 fof(f643,plain,(
% 0.12/0.49 ~cC12(iV16461)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f152])).
% 0.12/0.49 fof(f647,plain,(
% 0.12/0.49 ![X]: (~rR1(iV16461,X)|cC38(X))),
% 0.12/0.49 inference(pre_NNF_transformation,[status(thm)],[f155])).
% 0.12/0.49 fof(f648,plain,(
% 0.12/0.49 ![X0]: (~rR1(iV16461,X0)|cC38(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f647])).
% 0.12/0.49 fof(f651,plain,(
% 0.12/0.49 rR1(iV16461,iV16462)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f158])).
% 0.12/0.49 fof(f653,plain,(
% 0.12/0.49 ~cC8(iV16462)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f160])).
% 0.12/0.49 fof(f670,plain,(
% 0.12/0.49 ![X]: (~rR1(iV16463,X)|cC56(X))),
% 0.12/0.49 inference(pre_NNF_transformation,[status(thm)],[f172])).
% 0.12/0.49 fof(f671,plain,(
% 0.12/0.49 ![X0]: (~rR1(iV16463,X0)|cC56(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f670])).
% 0.12/0.49 fof(f678,plain,(
% 0.12/0.49 rR1(iV16463,iV16464)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f178])).
% 0.12/0.49 fof(f684,plain,(
% 0.12/0.49 ![X]: (~rR1(iV16464,X)|cC38(X))),
% 0.12/0.49 inference(pre_NNF_transformation,[status(thm)],[f183])).
% 0.12/0.49 fof(f685,plain,(
% 0.12/0.49 ![X0]: (~rR1(iV16464,X0)|cC38(X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f684])).
% 0.12/0.49 fof(f686,plain,(
% 0.12/0.49 ~cC12(iV16464)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f184])).
% 0.12/0.49 fof(f693,plain,(
% 0.12/0.49 rR1(iV16464,iV16465)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f189])).
% 0.12/0.49 fof(f702,plain,(
% 0.12/0.49 ~cC8(iV16465)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f195])).
% 0.12/0.49 fof(f709,plain,(
% 0.12/0.49 (((((((((((((((((((((((((((((((((((((((((((((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: (xsd_string(X)<~>~xsd_integer(X))))|~cC106(iV16439))|~cC28(iV16439))|~cC130(iV16439))|~cowlThing(iV16439))|~cC108(iV16439))|~cC104(iV16439))|~cC80(iV16440))|~cowlThing(iV16440))|~cC82(iV16440))|~cC98(iV16440))|~cowlThing(iV16448))|~cC38(iV16448))|~cC62(iV16453))|~cowlThing(iV16453))|~cC76(iV16453))|~cC60(iV16453))|~cC44(iV16455))|~cowlThing(iV16455))|~cC56(iV16455))|~cC42(iV16455))|~cowlThing(iV16457))|~cC38(iV16457))|~cC68(iV16459))|~cowlThing(iV16459))|~cC88(iV16459))|~cC50(iV16459))|~cC34(iV16459))|~cowlThing(iV16460))|~cC38(iV16460))|~cC44(iV16461))|~cowlThing(iV16461))|~cC56(iV16461))|~cC42(iV16461))|~cowlThing(iV16462))|~cC38(iV16462))|~cC62(iV16463))|~cowlThing(iV16463))|~cC76(iV16463))|~cC60(iV16463))|~cC44(iV16464))|~cowlThing(iV16464))|~cC56(iV16464))|~cC42(iV16464))|~cowlThing(iV16465))|~cC38(iV16465))),
% 0.12/0.49 inference(pre_NNF_transformation,[status(thm)],[f202])).
% 0.12/0.49 fof(f710,plain,(
% 0.12/0.49 ((((((((((((((((((((((((((((((((((((((((((((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: ((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))|~cC106(iV16439))|~cC28(iV16439))|~cC130(iV16439))|~cowlThing(iV16439))|~cC108(iV16439))|~cC104(iV16439))|~cC80(iV16440))|~cowlThing(iV16440))|~cC82(iV16440))|~cC98(iV16440))|~cowlThing(iV16448))|~cC38(iV16448))|~cC62(iV16453))|~cowlThing(iV16453))|~cC76(iV16453))|~cC60(iV16453))|~cC44(iV16455))|~cowlThing(iV16455))|~cC56(iV16455))|~cC42(iV16455))|~cowlThing(iV16457))|~cC38(iV16457))|~cC68(iV16459))|~cowlThing(iV16459))|~cC88(iV16459))|~cC50(iV16459))|~cC34(iV16459))|~cowlThing(iV16460))|~cC38(iV16460))|~cC44(iV16461))|~cowlThing(iV16461))|~cC56(iV16461))|~cC42(iV16461))|~cowlThing(iV16462))|~cC38(iV16462))|~cC62(iV16463))|~cowlThing(iV16463))|~cC76(iV16463))|~cC60(iV16463))|~cC44(iV16464))|~cowlThing(iV16464))|~cC56(iV16464))|~cC42(iV16464))|~cowlThing(iV16465))|~cC38(iV16465)),
% 0.12/0.50 inference(NNF_transformation,[status(thm)],[f709])).
% 0.12/0.50 fof(f711,plain,(
% 0.12/0.50 (((((((((((((((((((((((((((((((((((((((((((((((?[X]: ~cowlThing(X))|(?[X]: cowlNothing(X)))|(?[X]: ((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))|~cC106(iV16439))|~cC28(iV16439))|~cC130(iV16439))|~cowlThing(iV16439))|~cC108(iV16439))|~cC104(iV16439))|~cC80(iV16440))|~cowlThing(iV16440))|~cC82(iV16440))|~cC98(iV16440))|~cowlThing(iV16448))|~cC38(iV16448))|~cC62(iV16453))|~cowlThing(iV16453))|~cC76(iV16453))|~cC60(iV16453))|~cC44(iV16455))|~cowlThing(iV16455))|~cC56(iV16455))|~cC42(iV16455))|~cowlThing(iV16457))|~cC38(iV16457))|~cC68(iV16459))|~cowlThing(iV16459))|~cC88(iV16459))|~cC50(iV16459))|~cC34(iV16459))|~cowlThing(iV16460))|~cC38(iV16460))|~cC44(iV16461))|~cowlThing(iV16461))|~cC56(iV16461))|~cC42(iV16461))|~cowlThing(iV16462))|~cC38(iV16462))|~cC62(iV16463))|~cowlThing(iV16463))|~cC76(iV16463))|~cC60(iV16463))|~cC44(iV16464))|~cowlThing(iV16464))|~cC56(iV16464))|~cC42(iV16464))|~cowlThing(iV16465))|~cC38(iV16465)),
% 0.12/0.50 inference(miniscoping,[status(thm)],[f710])).
% 0.12/0.50 fof(f712,plain,(
% 0.12/0.50 ((((((((((((((((((((((((((((((((((((((((((((((~cowlThing(sK28_skl)|cowlNothing(sK29_skl))|((xsd_string(sK30_skl)|~xsd_integer(sK30_skl))&(~xsd_string(sK30_skl)|xsd_integer(sK30_skl))))|~cC106(iV16439))|~cC28(iV16439))|~cC130(iV16439))|~cowlThing(iV16439))|~cC108(iV16439))|~cC104(iV16439))|~cC80(iV16440))|~cowlThing(iV16440))|~cC82(iV16440))|~cC98(iV16440))|~cowlThing(iV16448))|~cC38(iV16448))|~cC62(iV16453))|~cowlThing(iV16453))|~cC76(iV16453))|~cC60(iV16453))|~cC44(iV16455))|~cowlThing(iV16455))|~cC56(iV16455))|~cC42(iV16455))|~cowlThing(iV16457))|~cC38(iV16457))|~cC68(iV16459))|~cowlThing(iV16459))|~cC88(iV16459))|~cC50(iV16459))|~cC34(iV16459))|~cowlThing(iV16460))|~cC38(iV16460))|~cC44(iV16461))|~cowlThing(iV16461))|~cC56(iV16461))|~cC42(iV16461))|~cowlThing(iV16462))|~cC38(iV16462))|~cC62(iV16463))|~cowlThing(iV16463))|~cC76(iV16463))|~cC60(iV16463))|~cC44(iV16464))|~cowlThing(iV16464))|~cC56(iV16464))|~cC42(iV16464))|~cowlThing(iV16465))|~cC38(iV16465)),
% 0.12/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl,sK29_skl,sK30_skl]),skolemize(X,sK28_skl),skolemize(X,sK29_skl),skolemize(X,sK30_skl)],[f711])).
% 0.12/0.50 fof(f713,plain,(
% 0.12/0.50 ~cowlThing(sK28_skl)|cowlNothing(sK29_skl)|xsd_string(sK30_skl)|~xsd_integer(sK30_skl)|~cC106(iV16439)|~cC28(iV16439)|~cC130(iV16439)|~cowlThing(iV16439)|~cC108(iV16439)|~cC104(iV16439)|~cC80(iV16440)|~cowlThing(iV16440)|~cC82(iV16440)|~cC98(iV16440)|~cowlThing(iV16448)|~cC38(iV16448)|~cC62(iV16453)|~cowlThing(iV16453)|~cC76(iV16453)|~cC60(iV16453)|~cC44(iV16455)|~cowlThing(iV16455)|~cC56(iV16455)|~cC42(iV16455)|~cowlThing(iV16457)|~cC38(iV16457)|~cC68(iV16459)|~cowlThing(iV16459)|~cC88(iV16459)|~cC50(iV16459)|~cC34(iV16459)|~cowlThing(iV16460)|~cC38(iV16460)|~cC44(iV16461)|~cowlThing(iV16461)|~cC56(iV16461)|~cC42(iV16461)|~cowlThing(iV16462)|~cC38(iV16462)|~cC62(iV16463)|~cowlThing(iV16463)|~cC76(iV16463)|~cC60(iV16463)|~cC44(iV16464)|~cowlThing(iV16464)|~cC56(iV16464)|~cC42(iV16464)|~cowlThing(iV16465)|~cC38(iV16465)),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f712])).
% 0.12/0.50 fof(f714,plain,(
% 0.12/0.50 ~cowlThing(sK28_skl)|cowlNothing(sK29_skl)|~xsd_string(sK30_skl)|xsd_integer(sK30_skl)|~cC106(iV16439)|~cC28(iV16439)|~cC130(iV16439)|~cowlThing(iV16439)|~cC108(iV16439)|~cC104(iV16439)|~cC80(iV16440)|~cowlThing(iV16440)|~cC82(iV16440)|~cC98(iV16440)|~cowlThing(iV16448)|~cC38(iV16448)|~cC62(iV16453)|~cowlThing(iV16453)|~cC76(iV16453)|~cC60(iV16453)|~cC44(iV16455)|~cowlThing(iV16455)|~cC56(iV16455)|~cC42(iV16455)|~cowlThing(iV16457)|~cC38(iV16457)|~cC68(iV16459)|~cowlThing(iV16459)|~cC88(iV16459)|~cC50(iV16459)|~cC34(iV16459)|~cowlThing(iV16460)|~cC38(iV16460)|~cC44(iV16461)|~cowlThing(iV16461)|~cC56(iV16461)|~cC42(iV16461)|~cowlThing(iV16462)|~cC38(iV16462)|~cC62(iV16463)|~cowlThing(iV16463)|~cC76(iV16463)|~cC60(iV16463)|~cC44(iV16464)|~cowlThing(iV16464)|~cC56(iV16464)|~cC42(iV16464)|~cowlThing(iV16465)|~cC38(iV16465)),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f712])).
% 0.12/0.50 fof(f715,definition,(
% 0.12/0.50 sQ0_spl <=> (cowlThing(sK28_skl))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f717,plain,(
% 0.12/0.50 ~cowlThing(sK28_skl)|sQ0_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f715])).
% 0.12/0.50 fof(f718,definition,(
% 0.12/0.50 sQ1_spl <=> (cowlNothing(sK29_skl))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f719,plain,(
% 0.12/0.50 cowlNothing(sK29_skl)|~sQ1_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f718])).
% 0.12/0.50 fof(f721,definition,(
% 0.12/0.50 sQ2_spl <=> (xsd_string(sK30_skl))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f722,plain,(
% 0.12/0.50 xsd_string(sK30_skl)|~sQ2_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f721])).
% 0.12/0.50 fof(f724,definition,(
% 0.12/0.50 sQ3_spl <=> (xsd_integer(sK30_skl))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f725,plain,(
% 0.12/0.50 xsd_integer(sK30_skl)|~sQ3_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f724])).
% 0.12/0.50 fof(f726,plain,(
% 0.12/0.50 ~xsd_integer(sK30_skl)|sQ3_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f724])).
% 0.12/0.50 fof(f727,definition,(
% 0.12/0.50 sQ4_spl <=> (cC106(iV16439))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f728,plain,(
% 0.12/0.50 cC106(iV16439)|~sQ4_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f727])).
% 0.12/0.50 fof(f730,definition,(
% 0.12/0.50 sQ5_spl <=> (cC28(iV16439))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f732,plain,(
% 0.12/0.50 ~cC28(iV16439)|sQ5_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f730])).
% 0.12/0.50 fof(f733,definition,(
% 0.12/0.50 sQ6_spl <=> (cC130(iV16439))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f735,plain,(
% 0.12/0.50 ~cC130(iV16439)|sQ6_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f733])).
% 0.12/0.50 fof(f736,definition,(
% 0.12/0.50 sQ7_spl <=> (cowlThing(iV16439))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f738,plain,(
% 0.12/0.50 ~cowlThing(iV16439)|sQ7_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f736])).
% 0.12/0.50 fof(f739,definition,(
% 0.12/0.50 sQ8_spl <=> (cC108(iV16439))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f742,definition,(
% 0.12/0.50 sQ9_spl <=> (cC104(iV16439))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f743,plain,(
% 0.12/0.50 cC104(iV16439)|~sQ9_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f742])).
% 0.12/0.50 fof(f745,definition,(
% 0.12/0.50 sQ10_spl <=> (cC80(iV16440))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f747,plain,(
% 0.12/0.50 ~cC80(iV16440)|sQ10_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f745])).
% 0.12/0.50 fof(f748,definition,(
% 0.12/0.50 sQ11_spl <=> (cowlThing(iV16440))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f750,plain,(
% 0.12/0.50 ~cowlThing(iV16440)|sQ11_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f748])).
% 0.12/0.50 fof(f751,definition,(
% 0.12/0.50 sQ12_spl <=> (cC82(iV16440))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f753,plain,(
% 0.12/0.50 ~cC82(iV16440)|sQ12_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f751])).
% 0.12/0.50 fof(f754,definition,(
% 0.12/0.50 sQ13_spl <=> (cC98(iV16440))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f757,definition,(
% 0.12/0.50 sQ14_spl <=> (cowlThing(iV16448))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f759,plain,(
% 0.12/0.50 ~cowlThing(iV16448)|sQ14_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f757])).
% 0.12/0.50 fof(f760,definition,(
% 0.12/0.50 sQ15_spl <=> (cC38(iV16448))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f763,definition,(
% 0.12/0.50 sQ16_spl <=> (cC62(iV16453))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f765,plain,(
% 0.12/0.50 ~cC62(iV16453)|sQ16_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f763])).
% 0.12/0.50 fof(f766,definition,(
% 0.12/0.50 sQ17_spl <=> (cowlThing(iV16453))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f768,plain,(
% 0.12/0.50 ~cowlThing(iV16453)|sQ17_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f766])).
% 0.12/0.50 fof(f769,definition,(
% 0.12/0.50 sQ18_spl <=> (cC76(iV16453))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f771,plain,(
% 0.12/0.50 ~cC76(iV16453)|sQ18_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f769])).
% 0.12/0.50 fof(f772,definition,(
% 0.12/0.50 sQ19_spl <=> (cC60(iV16453))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f775,definition,(
% 0.12/0.50 sQ20_spl <=> (cC44(iV16455))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f777,plain,(
% 0.12/0.50 ~cC44(iV16455)|sQ20_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f775])).
% 0.12/0.50 fof(f778,definition,(
% 0.12/0.50 sQ21_spl <=> (cowlThing(iV16455))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f780,plain,(
% 0.12/0.50 ~cowlThing(iV16455)|sQ21_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f778])).
% 0.12/0.50 fof(f781,definition,(
% 0.12/0.50 sQ22_spl <=> (cC56(iV16455))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f783,plain,(
% 0.12/0.50 ~cC56(iV16455)|sQ22_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f781])).
% 0.12/0.50 fof(f784,definition,(
% 0.12/0.50 sQ23_spl <=> (cC42(iV16455))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f787,definition,(
% 0.12/0.50 sQ24_spl <=> (cowlThing(iV16457))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f789,plain,(
% 0.12/0.50 ~cowlThing(iV16457)|sQ24_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f787])).
% 0.12/0.50 fof(f790,definition,(
% 0.12/0.50 sQ25_spl <=> (cC38(iV16457))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f793,definition,(
% 0.12/0.50 sQ26_spl <=> (cC68(iV16459))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f795,plain,(
% 0.12/0.50 ~cC68(iV16459)|sQ26_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f793])).
% 0.12/0.50 fof(f796,definition,(
% 0.12/0.50 sQ27_spl <=> (cowlThing(iV16459))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f798,plain,(
% 0.12/0.50 ~cowlThing(iV16459)|sQ27_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f796])).
% 0.12/0.50 fof(f799,definition,(
% 0.12/0.50 sQ28_spl <=> (cC88(iV16459))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f801,plain,(
% 0.12/0.50 ~cC88(iV16459)|sQ28_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f799])).
% 0.12/0.50 fof(f802,definition,(
% 0.12/0.50 sQ29_spl <=> (cC50(iV16459))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f804,plain,(
% 0.12/0.50 ~cC50(iV16459)|sQ29_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f802])).
% 0.12/0.50 fof(f805,definition,(
% 0.12/0.50 sQ30_spl <=> (cC34(iV16459))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f807,plain,(
% 0.12/0.50 ~cC34(iV16459)|sQ30_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f805])).
% 0.12/0.50 fof(f808,definition,(
% 0.12/0.50 sQ31_spl <=> (cowlThing(iV16460))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f810,plain,(
% 0.12/0.50 ~cowlThing(iV16460)|sQ31_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f808])).
% 0.12/0.50 fof(f811,definition,(
% 0.12/0.50 sQ32_spl <=> (cC38(iV16460))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f813,plain,(
% 0.12/0.50 ~cC38(iV16460)|sQ32_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f811])).
% 0.12/0.50 fof(f814,definition,(
% 0.12/0.50 sQ33_spl <=> (cC44(iV16461))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f816,plain,(
% 0.12/0.50 ~cC44(iV16461)|sQ33_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f814])).
% 0.12/0.50 fof(f817,definition,(
% 0.12/0.50 sQ34_spl <=> (cowlThing(iV16461))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f819,plain,(
% 0.12/0.50 ~cowlThing(iV16461)|sQ34_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f817])).
% 0.12/0.50 fof(f820,definition,(
% 0.12/0.50 sQ35_spl <=> (cC56(iV16461))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f822,plain,(
% 0.12/0.50 ~cC56(iV16461)|sQ35_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f820])).
% 0.12/0.50 fof(f823,definition,(
% 0.12/0.50 sQ36_spl <=> (cC42(iV16461))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f826,definition,(
% 0.12/0.50 sQ37_spl <=> (cowlThing(iV16462))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f828,plain,(
% 0.12/0.50 ~cowlThing(iV16462)|sQ37_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f826])).
% 0.12/0.50 fof(f829,definition,(
% 0.12/0.50 sQ38_spl <=> (cC38(iV16462))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f831,plain,(
% 0.12/0.50 ~cC38(iV16462)|sQ38_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f829])).
% 0.12/0.50 fof(f832,definition,(
% 0.12/0.50 sQ39_spl <=> (cC62(iV16463))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f834,plain,(
% 0.12/0.50 ~cC62(iV16463)|sQ39_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f832])).
% 0.12/0.50 fof(f835,definition,(
% 0.12/0.50 sQ40_spl <=> (cowlThing(iV16463))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f837,plain,(
% 0.12/0.50 ~cowlThing(iV16463)|sQ40_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f835])).
% 0.12/0.50 fof(f838,definition,(
% 0.12/0.50 sQ41_spl <=> (cC76(iV16463))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f840,plain,(
% 0.12/0.50 ~cC76(iV16463)|sQ41_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f838])).
% 0.12/0.50 fof(f841,definition,(
% 0.12/0.50 sQ42_spl <=> (cC60(iV16463))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f844,definition,(
% 0.12/0.50 sQ43_spl <=> (cC44(iV16464))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f846,plain,(
% 0.12/0.50 ~cC44(iV16464)|sQ43_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f844])).
% 0.12/0.50 fof(f847,definition,(
% 0.12/0.50 sQ44_spl <=> (cowlThing(iV16464))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f849,plain,(
% 0.12/0.50 ~cowlThing(iV16464)|sQ44_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f847])).
% 0.12/0.50 fof(f850,definition,(
% 0.12/0.50 sQ45_spl <=> (cC56(iV16464))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f852,plain,(
% 0.12/0.50 ~cC56(iV16464)|sQ45_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f850])).
% 0.12/0.50 fof(f853,definition,(
% 0.12/0.50 sQ46_spl <=> (cC42(iV16464))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f856,definition,(
% 0.12/0.50 sQ47_spl <=> (cowlThing(iV16465))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f858,plain,(
% 0.12/0.50 ~cowlThing(iV16465)|sQ47_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f856])).
% 0.12/0.50 fof(f859,definition,(
% 0.12/0.50 sQ48_spl <=> (cC38(iV16465))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f861,plain,(
% 0.12/0.50 ~cC38(iV16465)|sQ48_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f859])).
% 0.12/0.50 fof(f862,plain,(
% 0.12/0.50 ~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.12/0.50 inference(split_clause,[status(thm)],[f713,f715,f718,f721,f724,f727,f730,f733,f736,f739,f742,f745,f748,f751,f754,f757,f760,f763,f766,f769,f772,f775,f778,f781,f784,f787,f790,f793,f796,f799,f802,f805,f808,f811,f814,f817,f820,f823,f826,f829,f832,f835,f838,f841,f844,f847,f850,f853,f856,f859])).
% 0.12/0.50 fof(f863,plain,(
% 0.12/0.50 ~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.12/0.50 inference(split_clause,[status(thm)],[f714,f715,f718,f721,f724,f727,f730,f733,f736,f739,f742,f745,f748,f751,f754,f757,f760,f763,f766,f769,f772,f775,f778,f781,f784,f787,f790,f793,f796,f799,f802,f805,f808,f811,f814,f817,f820,f823,f826,f829,f832,f835,f838,f841,f844,f847,f850,f853,f856,f859])).
% 0.12/0.50 fof(f866,plain,(
% 0.12/0.50 cC98(iV16440)),
% 0.12/0.50 inference(resolution,[status(thm)],[f533,f529])).
% 0.12/0.50 fof(f868,plain,(
% 0.12/0.50 cC100(iV16439)|cC98(iV16440)),
% 0.12/0.50 inference(resolution,[status(thm)],[f533,f220])).
% 0.12/0.50 fof(f880,definition,(
% 0.12/0.50 sQ51_spl <=> (cC100(iV16439))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f881,plain,(
% 0.12/0.50 cC100(iV16439)|~sQ51_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f880])).
% 0.12/0.50 fof(f883,plain,(
% 0.12/0.50 sQ51_spl|sQ13_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f868,f880,f754])).
% 0.12/0.50 fof(f912,plain,(
% 0.12/0.50 $false|~sQ51_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f881,f531])).
% 0.12/0.50 fof(f913,plain,(
% 0.12/0.50 ~sQ51_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f912])).
% 0.12/0.50 fof(f914,plain,(
% 0.12/0.50 cC82(iV16440)),
% 0.12/0.50 inference(resolution,[status(thm)],[f866,f521])).
% 0.12/0.50 fof(f915,plain,(
% 0.12/0.50 cC80(iV16440)),
% 0.12/0.50 inference(resolution,[status(thm)],[f914,f477])).
% 0.12/0.50 fof(f916,plain,(
% 0.12/0.50 cC76(iV16463)),
% 0.12/0.50 inference(resolution,[status(thm)],[f544,f537])).
% 0.12/0.50 fof(f965,plain,(
% 0.12/0.50 cC56(iV16461)),
% 0.12/0.50 inference(resolution,[status(thm)],[f574,f571])).
% 0.12/0.50 fof(f969,plain,(
% 0.12/0.50 cC60(iV16453)|cC12(iV16461)),
% 0.12/0.50 inference(resolution,[status(thm)],[f574,f418])).
% 0.12/0.50 fof(f993,definition,(
% 0.12/0.50 sQ78_spl <=> (cC12(iV16461))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f994,plain,(
% 0.12/0.50 cC12(iV16461)|~sQ78_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f993])).
% 0.12/0.50 fof(f996,plain,(
% 0.12/0.50 sQ19_spl|sQ78_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f969,f772,f993])).
% 0.12/0.50 fof(f1011,plain,(
% 0.12/0.50 cC38(iV16460)),
% 0.12/0.50 inference(resolution,[status(thm)],[f589,f588])).
% 0.12/0.50 fof(f1017,plain,(
% 0.12/0.50 cC42(iV16455)|cC8(iV16460)),
% 0.12/0.50 inference(resolution,[status(thm)],[f589,f364])).
% 0.12/0.50 fof(f1053,definition,(
% 0.12/0.50 sQ93_spl <=> (cC8(iV16460))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f1054,plain,(
% 0.12/0.50 cC8(iV16460)|~sQ93_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f1053])).
% 0.12/0.50 fof(f1056,plain,(
% 0.12/0.50 sQ23_spl|sQ93_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f1017,f784,f1053])).
% 0.12/0.50 fof(f1060,plain,(
% 0.12/0.50 cC104(iV16439)|cC102(iV16440)),
% 0.12/0.50 inference(resolution,[status(thm)],[f226,f533])).
% 0.12/0.50 fof(f1082,definition,(
% 0.12/0.50 sQ100_spl <=> (cC102(iV16440))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f1083,plain,(
% 0.12/0.50 cC102(iV16440)|~sQ100_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f1082])).
% 0.12/0.50 fof(f1085,plain,(
% 0.12/0.50 sQ9_spl|sQ100_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f1060,f742,f1082])).
% 0.12/0.50 fof(f1086,plain,(
% 0.12/0.50 rR1(iV16439,sK1_skl(iV16439))|~sQ9_spl),
% 0.12/0.50 inference(resolution,[status(thm)],[f743,f224])).
% 0.12/0.50 fof(f1090,plain,(
% 0.12/0.50 cC100(iV16439)|cC98(sK1_skl(iV16439))|~sQ9_spl),
% 0.12/0.50 inference(resolution,[status(thm)],[f1086,f220])).
% 0.12/0.50 fof(f1103,definition,(
% 0.12/0.50 sQ103_spl <=> (cC98(sK1_skl(iV16439)))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f1106,plain,(
% 0.12/0.50 sQ51_spl|sQ103_spl|~sQ9_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f1090,f880,f1103,f742])).
% 0.12/0.50 fof(f1123,plain,(
% 0.12/0.50 $false|~sQ100_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1083,f540])).
% 0.12/0.50 fof(f1124,plain,(
% 0.12/0.50 ~sQ100_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1123])).
% 0.12/0.50 fof(f1144,plain,(
% 0.12/0.50 cC62(iV16463)),
% 0.12/0.50 inference(resolution,[status(thm)],[f916,f460])).
% 0.12/0.50 fof(f1145,plain,(
% 0.12/0.50 cC44(iV16461)),
% 0.12/0.50 inference(resolution,[status(thm)],[f965,f399])).
% 0.12/0.50 fof(f1146,plain,(
% 0.12/0.50 cC38(iV16462)),
% 0.12/0.50 inference(resolution,[status(thm)],[f651,f648])).
% 0.12/0.50 fof(f1153,plain,(
% 0.12/0.50 cC42(iV16461)|cC8(iV16462)),
% 0.12/0.50 inference(resolution,[status(thm)],[f651,f364])).
% 0.12/0.50 fof(f1196,definition,(
% 0.12/0.50 sQ120_spl <=> (cC8(iV16462))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f1197,plain,(
% 0.12/0.50 cC8(iV16462)|~sQ120_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f1196])).
% 0.12/0.50 fof(f1199,plain,(
% 0.12/0.50 sQ36_spl|sQ120_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f1153,f823,f1196])).
% 0.12/0.50 fof(f1200,plain,(
% 0.12/0.50 cC56(iV16464)),
% 0.12/0.50 inference(resolution,[status(thm)],[f678,f671])).
% 0.12/0.50 fof(f1205,plain,(
% 0.12/0.50 cC60(iV16463)|cC12(iV16464)),
% 0.12/0.50 inference(resolution,[status(thm)],[f678,f418])).
% 0.12/0.50 fof(f1236,definition,(
% 0.12/0.50 sQ129_spl <=> (cC12(iV16464))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f1237,plain,(
% 0.12/0.50 cC12(iV16464)|~sQ129_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f1236])).
% 0.12/0.50 fof(f1239,plain,(
% 0.12/0.50 sQ42_spl|sQ129_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f1205,f841,f1236])).
% 0.12/0.50 fof(f1256,plain,(
% 0.12/0.50 cC106(iV16439)|cC100(iV16439)|~sQ9_spl),
% 0.12/0.50 inference(resolution,[status(thm)],[f231,f743])).
% 0.12/0.50 fof(f1257,plain,(
% 0.12/0.50 sQ4_spl|sQ51_spl|~sQ9_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f1256,f727,f880,f742])).
% 0.12/0.50 fof(f1259,plain,(
% 0.12/0.50 cC108(iV16439)|~cC28(iV16439)|~sQ4_spl),
% 0.12/0.50 inference(resolution,[status(thm)],[f728,f236])).
% 0.12/0.50 fof(f1261,plain,(
% 0.12/0.50 sQ8_spl|~sQ5_spl|~sQ4_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f1259,f739,f730,f727])).
% 0.12/0.50 fof(f1262,plain,(
% 0.12/0.50 ~cC108(iV16439)|sQ5_spl),
% 0.12/0.50 inference(resolution,[status(thm)],[f732,f234])).
% 0.12/0.50 fof(f1283,plain,(
% 0.12/0.50 cC38(iV16465)),
% 0.12/0.50 inference(resolution,[status(thm)],[f693,f685])).
% 0.12/0.50 fof(f1290,plain,(
% 0.12/0.50 cC42(iV16464)|cC8(iV16465)),
% 0.12/0.50 inference(resolution,[status(thm)],[f693,f364])).
% 0.12/0.50 fof(f1333,definition,(
% 0.12/0.50 sQ149_spl <=> (cC8(iV16465))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f1334,plain,(
% 0.12/0.50 cC8(iV16465)|~sQ149_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f1333])).
% 0.12/0.50 fof(f1336,plain,(
% 0.12/0.50 sQ46_spl|sQ149_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f1290,f853,f1333])).
% 0.12/0.50 fof(f1346,plain,(
% 0.12/0.50 cC44(iV16464)),
% 0.12/0.50 inference(resolution,[status(thm)],[f1200,f399])).
% 0.12/0.50 fof(f1559,plain,(
% 0.12/0.50 $false|~sQ78_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f994,f643])).
% 0.12/0.50 fof(f1560,plain,(
% 0.12/0.50 ~sQ78_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1559])).
% 0.12/0.50 fof(f1561,plain,(
% 0.12/0.50 cC108(iV16439)),
% 0.12/0.50 inference(resolution,[status(thm)],[f525,f530])).
% 0.12/0.50 fof(f1562,plain,(
% 0.12/0.50 $false|sQ5_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1561,f1262])).
% 0.12/0.50 fof(f1563,plain,(
% 0.12/0.50 sQ5_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1562])).
% 0.12/0.50 fof(f1564,plain,(
% 0.12/0.50 $false|sQ48_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f861,f1283])).
% 0.12/0.50 fof(f1565,plain,(
% 0.12/0.50 sQ48_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1564])).
% 0.12/0.50 fof(f1566,plain,(
% 0.12/0.50 $false|sQ47_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f858,f204])).
% 0.12/0.50 fof(f1567,plain,(
% 0.12/0.50 sQ47_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1566])).
% 0.12/0.50 fof(f1568,plain,(
% 0.12/0.50 $false|sQ45_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f852,f1200])).
% 0.12/0.50 fof(f1569,plain,(
% 0.12/0.50 sQ45_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1568])).
% 0.12/0.50 fof(f1570,plain,(
% 0.12/0.50 $false|sQ44_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f849,f204])).
% 0.12/0.50 fof(f1571,plain,(
% 0.12/0.50 sQ44_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1570])).
% 0.12/0.50 fof(f1572,plain,(
% 0.12/0.50 $false|sQ43_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f846,f1346])).
% 0.12/0.50 fof(f1573,plain,(
% 0.12/0.50 sQ43_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1572])).
% 0.12/0.50 fof(f1574,plain,(
% 0.12/0.50 $false|sQ41_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f840,f916])).
% 0.12/0.50 fof(f1575,plain,(
% 0.12/0.50 sQ41_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1574])).
% 0.12/0.50 fof(f1576,plain,(
% 0.12/0.50 $false|sQ40_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f837,f204])).
% 0.12/0.50 fof(f1577,plain,(
% 0.12/0.50 sQ40_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1576])).
% 0.12/0.50 fof(f1578,plain,(
% 0.12/0.50 $false|sQ39_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f834,f1144])).
% 0.12/0.50 fof(f1579,plain,(
% 0.12/0.50 sQ39_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1578])).
% 0.12/0.50 fof(f1580,plain,(
% 0.12/0.50 $false|sQ38_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f831,f1146])).
% 0.12/0.50 fof(f1581,plain,(
% 0.12/0.50 sQ38_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1580])).
% 0.12/0.50 fof(f1582,plain,(
% 0.12/0.50 $false|sQ37_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f828,f204])).
% 0.12/0.50 fof(f1583,plain,(
% 0.12/0.50 sQ37_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1582])).
% 0.12/0.50 fof(f1584,plain,(
% 0.12/0.50 $false|sQ35_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f822,f965])).
% 0.12/0.50 fof(f1585,plain,(
% 0.12/0.50 sQ35_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1584])).
% 0.12/0.50 fof(f1586,plain,(
% 0.12/0.50 $false|sQ34_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f819,f204])).
% 0.12/0.50 fof(f1587,plain,(
% 0.12/0.50 sQ34_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1586])).
% 0.12/0.50 fof(f1588,plain,(
% 0.12/0.50 $false|sQ33_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f816,f1145])).
% 0.12/0.50 fof(f1589,plain,(
% 0.12/0.50 sQ33_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1588])).
% 0.12/0.50 fof(f1590,plain,(
% 0.12/0.50 $false|sQ32_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f813,f1011])).
% 0.12/0.50 fof(f1591,plain,(
% 0.12/0.50 sQ32_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1590])).
% 0.12/0.50 fof(f1592,plain,(
% 0.12/0.50 $false|sQ31_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f810,f204])).
% 0.12/0.50 fof(f1593,plain,(
% 0.12/0.50 sQ31_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1592])).
% 0.12/0.50 fof(f1594,plain,(
% 0.12/0.50 cC130(iV16439)),
% 0.12/0.50 inference(resolution,[status(thm)],[f526,f530])).
% 0.12/0.50 fof(f1663,plain,(
% 0.12/0.50 $false|~sQ93_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1054,f628])).
% 0.12/0.50 fof(f1664,plain,(
% 0.12/0.50 ~sQ93_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1663])).
% 0.12/0.50 fof(f1741,plain,(
% 0.12/0.50 $false|~sQ120_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1197,f653])).
% 0.12/0.50 fof(f1742,plain,(
% 0.12/0.50 ~sQ120_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1741])).
% 0.12/0.50 fof(f1760,plain,(
% 0.12/0.50 cC2(iV16459)|cC4(iV16459)),
% 0.12/0.50 inference(resolution,[status(thm)],[f336,f621])).
% 0.12/0.50 fof(f1763,definition,(
% 0.12/0.50 sQ208_spl <=> (cC2(iV16459))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f1764,plain,(
% 0.12/0.50 cC2(iV16459)|~sQ208_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f1763])).
% 0.12/0.50 fof(f1766,definition,(
% 0.12/0.50 sQ209_spl <=> (cC4(iV16459))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f1769,plain,(
% 0.12/0.50 sQ208_spl|sQ209_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f1760,f1763,f1766])).
% 0.12/0.50 fof(f1770,plain,(
% 0.12/0.50 $false|~sQ208_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1764,f616])).
% 0.12/0.50 fof(f1771,plain,(
% 0.12/0.50 ~sQ208_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1770])).
% 0.12/0.50 fof(f1773,plain,(
% 0.12/0.50 cC32(iV16459)|cC30(iV16459)|sQ30_spl),
% 0.12/0.50 inference(resolution,[status(thm)],[f341,f807])).
% 0.12/0.50 fof(f1776,definition,(
% 0.12/0.50 sQ210_spl <=> (cC32(iV16459))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f1777,plain,(
% 0.12/0.50 cC32(iV16459)|~sQ210_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f1776])).
% 0.12/0.50 fof(f1779,definition,(
% 0.12/0.50 sQ211_spl <=> (cC30(iV16459))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f1780,plain,(
% 0.12/0.50 cC30(iV16459)|~sQ211_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f1779])).
% 0.12/0.50 fof(f1782,plain,(
% 0.12/0.50 sQ210_spl|sQ211_spl|sQ30_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f1773,f1776,f1779,f805])).
% 0.12/0.50 fof(f1783,plain,(
% 0.12/0.50 $false|sQ27_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f798,f204])).
% 0.12/0.50 fof(f1784,plain,(
% 0.12/0.50 sQ27_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1783])).
% 0.12/0.50 fof(f1785,plain,(
% 0.12/0.50 $false|sQ24_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f789,f204])).
% 0.12/0.50 fof(f1786,plain,(
% 0.12/0.50 sQ24_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1785])).
% 0.12/0.50 fof(f1787,plain,(
% 0.12/0.50 $false|sQ21_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f780,f204])).
% 0.12/0.50 fof(f1788,plain,(
% 0.12/0.50 sQ21_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1787])).
% 0.12/0.50 fof(f1789,plain,(
% 0.12/0.50 $false|sQ17_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f768,f204])).
% 0.12/0.50 fof(f1790,plain,(
% 0.12/0.50 sQ17_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1789])).
% 0.12/0.50 fof(f1791,plain,(
% 0.12/0.50 $false|sQ14_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f759,f204])).
% 0.12/0.50 fof(f1792,plain,(
% 0.12/0.50 sQ14_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1791])).
% 0.12/0.50 fof(f1793,plain,(
% 0.12/0.50 $false|sQ12_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f753,f914])).
% 0.12/0.50 fof(f1794,plain,(
% 0.12/0.50 sQ12_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1793])).
% 0.12/0.50 fof(f1795,plain,(
% 0.12/0.50 $false|sQ11_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f750,f204])).
% 0.12/0.50 fof(f1796,plain,(
% 0.12/0.50 sQ11_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1795])).
% 0.12/0.50 fof(f1797,plain,(
% 0.12/0.50 $false|sQ10_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f747,f915])).
% 0.12/0.50 fof(f1798,plain,(
% 0.12/0.50 sQ10_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1797])).
% 0.12/0.50 fof(f1799,plain,(
% 0.12/0.50 $false|sQ7_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f738,f204])).
% 0.12/0.50 fof(f1800,plain,(
% 0.12/0.50 sQ7_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1799])).
% 0.12/0.50 fof(f1801,plain,(
% 0.12/0.50 $false|sQ6_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f735,f1594])).
% 0.12/0.50 fof(f1802,plain,(
% 0.12/0.50 sQ6_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1801])).
% 0.12/0.50 fof(f1803,plain,(
% 0.12/0.50 $false|~sQ1_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f719,f205])).
% 0.12/0.50 fof(f1804,plain,(
% 0.12/0.50 ~sQ1_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1803])).
% 0.12/0.50 fof(f1805,plain,(
% 0.12/0.50 $false|sQ0_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f717,f204])).
% 0.12/0.50 fof(f1806,plain,(
% 0.12/0.50 sQ0_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1805])).
% 0.12/0.50 fof(f1807,plain,(
% 0.12/0.50 $false|~sQ211_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1780,f607])).
% 0.12/0.50 fof(f1808,plain,(
% 0.12/0.50 ~sQ211_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1807])).
% 0.12/0.50 fof(f1809,plain,(
% 0.12/0.50 $false|~sQ210_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1777,f621])).
% 0.12/0.50 fof(f1810,plain,(
% 0.12/0.50 ~sQ210_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1809])).
% 0.12/0.50 fof(f1861,plain,(
% 0.12/0.50 $false|~sQ129_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1237,f686])).
% 0.12/0.50 fof(f1862,plain,(
% 0.12/0.50 ~sQ129_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1861])).
% 0.12/0.50 fof(f1915,plain,(
% 0.12/0.50 $false|~sQ149_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1334,f702])).
% 0.12/0.50 fof(f1916,plain,(
% 0.12/0.50 ~sQ149_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f1915])).
% 0.12/0.50 fof(f1964,plain,(
% 0.12/0.50 cC38(iV16457)|cC36(iV16457)),
% 0.12/0.50 inference(resolution,[status(thm)],[f352,f598])).
% 0.12/0.50 fof(f1965,plain,(
% 0.12/0.50 cC38(iV16448)|cC36(iV16448)),
% 0.12/0.50 inference(resolution,[status(thm)],[f352,f552])).
% 0.12/0.50 fof(f1979,definition,(
% 0.12/0.50 sQ239_spl <=> (cC36(iV16457))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f1980,plain,(
% 0.12/0.50 cC36(iV16457)|~sQ239_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f1979])).
% 0.12/0.50 fof(f1982,plain,(
% 0.12/0.50 sQ25_spl|sQ239_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f1964,f790,f1979])).
% 0.12/0.50 fof(f1983,definition,(
% 0.12/0.50 sQ240_spl <=> (cC36(iV16448))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f1984,plain,(
% 0.12/0.50 cC36(iV16448)|~sQ240_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f1983])).
% 0.12/0.50 fof(f1986,plain,(
% 0.12/0.50 sQ15_spl|sQ240_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f1965,f760,f1983])).
% 0.12/0.50 fof(f1991,definition,(
% 0.12/0.50 sQ241_spl <=> (cC8(iV16459))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ241_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f1992,plain,(
% 0.12/0.50 cC8(iV16459)|~sQ241_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f1991])).
% 0.12/0.50 fof(f1995,plain,(
% 0.12/0.50 cC46(iV16459)|cC48(iV16459)|sQ29_spl),
% 0.12/0.50 inference(resolution,[status(thm)],[f384,f804])).
% 0.12/0.50 fof(f1998,definition,(
% 0.12/0.50 sQ242_spl <=> (cC46(iV16459))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f1999,plain,(
% 0.12/0.50 cC46(iV16459)|~sQ242_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f1998])).
% 0.12/0.50 fof(f2001,definition,(
% 0.12/0.50 sQ243_spl <=> (cC48(iV16459))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ243_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f2002,plain,(
% 0.12/0.50 cC48(iV16459)|~sQ243_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f2001])).
% 0.12/0.50 fof(f2004,plain,(
% 0.12/0.50 sQ242_spl|sQ243_spl|sQ29_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f1995,f1998,f2001,f802])).
% 0.12/0.50 fof(f2005,plain,(
% 0.12/0.50 $false|~sQ243_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2002,f606])).
% 0.12/0.50 fof(f2006,plain,(
% 0.12/0.50 ~sQ243_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f2005])).
% 0.12/0.50 fof(f2007,plain,(
% 0.12/0.50 $false|~sQ242_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1999,f610])).
% 0.12/0.50 fof(f2008,plain,(
% 0.12/0.50 ~sQ242_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f2007])).
% 0.12/0.50 fof(f2016,definition,(
% 0.12/0.50 sQ244_spl <=> (cC12(iV16459))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f2020,plain,(
% 0.12/0.50 $false|~sQ241_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1992,f615])).
% 0.12/0.50 fof(f2021,plain,(
% 0.12/0.50 ~sQ241_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f2020])).
% 0.12/0.50 fof(f2283,plain,(
% 0.12/0.50 cC12(iV16459)|cC2(iV16459)),
% 0.12/0.50 inference(resolution,[status(thm)],[f488,f609])).
% 0.12/0.50 fof(f2286,plain,(
% 0.12/0.50 sQ244_spl|sQ208_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f2283,f2016,f1763])).
% 0.12/0.50 fof(f2287,plain,(
% 0.12/0.50 cC84(iV16459)|cC86(iV16459)|sQ28_spl),
% 0.12/0.50 inference(resolution,[status(thm)],[f493,f801])).
% 0.12/0.50 fof(f2290,definition,(
% 0.12/0.50 sQ295_spl <=> (cC84(iV16459))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ295_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f2291,plain,(
% 0.12/0.50 cC84(iV16459)|~sQ295_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f2290])).
% 0.12/0.50 fof(f2293,definition,(
% 0.12/0.50 sQ296_spl <=> (cC86(iV16459))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ296_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f2294,plain,(
% 0.12/0.50 cC86(iV16459)|~sQ296_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f2293])).
% 0.12/0.50 fof(f2296,plain,(
% 0.12/0.50 sQ295_spl|sQ296_spl|sQ28_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f2287,f2290,f2293,f799])).
% 0.12/0.50 fof(f2297,plain,(
% 0.12/0.50 $false|~sQ296_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2294,f609])).
% 0.12/0.50 fof(f2298,plain,(
% 0.12/0.50 ~sQ296_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f2297])).
% 0.12/0.50 fof(f2299,plain,(
% 0.12/0.50 $false|~sQ295_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2291,f618])).
% 0.12/0.50 fof(f2300,plain,(
% 0.12/0.50 ~sQ295_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f2299])).
% 0.12/0.50 fof(f2301,plain,(
% 0.12/0.50 cC64(iV16459)|cC66(iV16459)|sQ26_spl),
% 0.12/0.50 inference(resolution,[status(thm)],[f795,f438])).
% 0.12/0.50 fof(f2302,definition,(
% 0.12/0.50 sQ297_spl <=> (cC64(iV16459))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ297_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f2303,plain,(
% 0.12/0.50 cC64(iV16459)|~sQ297_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f2302])).
% 0.12/0.50 fof(f2305,definition,(
% 0.12/0.50 sQ298_spl <=> (cC66(iV16459))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ298_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f2306,plain,(
% 0.12/0.50 cC66(iV16459)|~sQ298_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f2305])).
% 0.12/0.50 fof(f2308,plain,(
% 0.12/0.50 sQ297_spl|sQ298_spl|sQ26_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f2301,f2302,f2305,f793])).
% 0.12/0.50 fof(f2309,plain,(
% 0.12/0.50 $false|~sQ298_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2306,f613])).
% 0.12/0.50 fof(f2310,plain,(
% 0.12/0.50 ~sQ298_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f2309])).
% 0.12/0.50 fof(f2311,plain,(
% 0.12/0.50 $false|~sQ297_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2303,f619])).
% 0.12/0.50 fof(f2312,plain,(
% 0.12/0.50 ~sQ297_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f2311])).
% 0.12/0.50 fof(f2313,plain,(
% 0.12/0.50 ~cC44(iV16455)|cC54(iV16455)|sQ22_spl),
% 0.12/0.50 inference(resolution,[status(thm)],[f783,f401])).
% 0.12/0.50 fof(f2314,definition,(
% 0.12/0.50 sQ299_spl <=> (cC54(iV16455))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ299_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f2315,plain,(
% 0.12/0.50 cC54(iV16455)|~sQ299_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f2314])).
% 0.12/0.50 fof(f2317,plain,(
% 0.12/0.50 ~sQ20_spl|sQ299_spl|sQ22_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f2313,f775,f2314,f781])).
% 0.12/0.50 fof(f2318,plain,(
% 0.12/0.50 cC40(iV16455)|~cC42(iV16455)|sQ20_spl),
% 0.12/0.50 inference(resolution,[status(thm)],[f777,f369])).
% 0.12/0.50 fof(f2319,definition,(
% 0.12/0.50 sQ300_spl <=> (cC40(iV16455))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ300_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f2320,plain,(
% 0.12/0.50 cC40(iV16455)|~sQ300_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f2319])).
% 0.12/0.50 fof(f2322,plain,(
% 0.12/0.50 sQ300_spl|~sQ23_spl|sQ20_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f2318,f2319,f784,f775])).
% 0.12/0.50 fof(f2323,plain,(
% 0.12/0.50 $false|~sQ299_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2315,f584])).
% 0.12/0.50 fof(f2324,plain,(
% 0.12/0.50 ~sQ299_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f2323])).
% 0.12/0.50 fof(f2325,plain,(
% 0.12/0.50 cC74(iV16453)|~cC62(iV16453)|sQ18_spl),
% 0.12/0.50 inference(resolution,[status(thm)],[f771,f461])).
% 0.12/0.50 fof(f2326,definition,(
% 0.12/0.50 sQ301_spl <=> (cC74(iV16453))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ301_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f2327,plain,(
% 0.12/0.50 cC74(iV16453)|~sQ301_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f2326])).
% 0.12/0.50 fof(f2329,plain,(
% 0.12/0.50 sQ301_spl|~sQ16_spl|sQ18_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f2325,f2326,f763,f769])).
% 0.12/0.50 fof(f2330,plain,(
% 0.12/0.50 ~cC60(iV16453)|cC58(iV16453)|sQ16_spl),
% 0.12/0.50 inference(resolution,[status(thm)],[f765,f423])).
% 0.12/0.50 fof(f2331,definition,(
% 0.12/0.50 sQ302_spl <=> (cC58(iV16453))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f2332,plain,(
% 0.12/0.50 cC58(iV16453)|~sQ302_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f2331])).
% 0.12/0.50 fof(f2334,plain,(
% 0.12/0.50 ~sQ19_spl|sQ302_spl|sQ16_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f2330,f772,f2331,f763])).
% 0.12/0.50 fof(f2335,plain,(
% 0.12/0.50 $false|~sQ301_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2327,f569])).
% 0.12/0.50 fof(f2336,plain,(
% 0.12/0.50 ~sQ301_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f2335])).
% 0.12/0.50 fof(f2375,plain,(
% 0.12/0.50 ~xsd_string(sK30_skl)|~sQ3_spl),
% 0.12/0.50 inference(resolution,[status(thm)],[f725,f208])).
% 0.12/0.50 fof(f2376,plain,(
% 0.12/0.50 $false|~sQ2_spl|~sQ3_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2375,f722])).
% 0.12/0.50 fof(f2377,plain,(
% 0.12/0.50 ~sQ2_spl|~sQ3_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f2376])).
% 0.12/0.50 fof(f2517,plain,(
% 0.12/0.50 xsd_string(sK30_skl)|sQ3_spl),
% 0.12/0.50 inference(resolution,[status(thm)],[f726,f209])).
% 0.12/0.50 fof(f2518,plain,(
% 0.12/0.50 sQ2_spl|sQ3_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f2517,f721,f724])).
% 0.12/0.50 fof(f2519,plain,(
% 0.12/0.50 $false|~sQ240_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1984,f547])).
% 0.12/0.50 fof(f2520,plain,(
% 0.12/0.50 ~sQ240_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f2519])).
% 0.12/0.50 fof(f2521,plain,(
% 0.12/0.50 $false|~sQ239_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1980,f590])).
% 0.12/0.50 fof(f2522,plain,(
% 0.12/0.50 ~sQ239_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f2521])).
% 0.12/0.50 fof(f2523,plain,(
% 0.12/0.50 $false|~sQ302_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2332,f568])).
% 0.12/0.50 fof(f2524,plain,(
% 0.12/0.50 ~sQ302_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f2523])).
% 0.12/0.50 fof(f2525,plain,(
% 0.12/0.50 $false|~sQ300_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2320,f576])).
% 0.12/0.50 fof(f2526,plain,(
% 0.12/0.50 ~sQ300_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f2525])).
% 0.12/0.50 fof(f2527,plain,(
% 0.12/0.50 $false),
% 0.12/0.50 inference(sat_refutation,[status(thm)],[f862,f863,f883,f913,f996,f1056,f1085,f1106,f1124,f1199,f1239,f1257,f1261,f1336,f1560,f1563,f1565,f1567,f1569,f1571,f1573,f1575,f1577,f1579,f1581,f1583,f1585,f1587,f1589,f1591,f1593,f1664,f1742,f1769,f1771,f1782,f1784,f1786,f1788,f1790,f1792,f1794,f1796,f1798,f1800,f1802,f1804,f1806,f1808,f1810,f1862,f1916,f1982,f1986,f2004,f2006,f2008,f2021,f2286,f2296,f2298,f2300,f2308,f2310,f2312,f2317,f2322,f2324,f2329,f2334,f2336,f2377,f2518,f2520,f2522,f2524,f2526])).
% 0.12/0.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.51 % Elapsed time: 0.152927 seconds
% 0.12/0.51 % CPU time: 0.961199 seconds
% 0.12/0.51 % Total memory used: 45.527 MB
% 0.12/0.51 % Net memory used: 45.263 MB
%------------------------------------------------------------------------------