%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS158+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 : n001.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.12s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS158+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n001.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 23:00:44 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.35 % Drodi V4.1.1
% 0.12/0.38 % Refutation found
% 0.12/0.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.38 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.38 fof(f1,axiom,(
% 0.12/0.38 (! [X] :( cowlThing(X)& ~ cowlNothing(X) ) )),
% 0.12/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f2,axiom,(
% 0.12/0.38 (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ) )),
% 0.12/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f4,axiom,(
% 0.12/0.38 (! [X] :( cC10(X)<=> (? [Y] :( rR1(X,Y)& cC2xcomp(Y) ) )) )),
% 0.12/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f6,axiom,(
% 0.12/0.38 (! [X] :( cC12(X)<=> ( cC10xcomp(X)& cC2xcomp(X) ) ) )),
% 0.12/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f7,axiom,(
% 0.12/0.38 (! [X] :( cC14(X)<=> (? [Y] :( rR1(X,Y)& cC12(Y) ) )) )),
% 0.12/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f8,axiom,(
% 0.12/0.38 (! [X] :( cC16(X)<=> ( cC14(X)& cC8(X) ) ) )),
% 0.12/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f9,axiom,(
% 0.12/0.38 (! [X] :( cC18(X)<=> ( cTOP(X)& cC16(X) ) ) )),
% 0.12/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f15,axiom,(
% 0.12/0.38 (! [X] :( cC6(X)<=> ( cC4xcomp(X)& cC2xcomp(X) ) ) )),
% 0.12/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f17,axiom,(
% 0.12/0.38 (! [X] :( cTEST(X)<=> ( cTOP(X)& cC18(X) ) ) )),
% 0.12/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f19,axiom,(
% 0.12/0.38 cTEST(iV16560) ),
% 0.12/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f20,axiom,(
% 0.12/0.38 cTOP(iV16560) ),
% 0.12/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f21,axiom,(
% 0.12/0.38 rR1(iV16560,iV16562) ),
% 0.12/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f25,axiom,(
% 0.12/0.38 cC4xcomp(iV16561) ),
% 0.12/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f26,axiom,(
% 0.12/0.38 cC2xcomp(iV16561) ),
% 0.12/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f29,axiom,(
% 0.12/0.38 cC10xcomp(iV16562) ),
% 0.12/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f30,axiom,(
% 0.12/0.38 cC2xcomp(iV16562) ),
% 0.12/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f31,conjecture,(
% 0.12/0.38 ( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& cC18(iV16560)& cC14(iV16560)& cC8(iV16560)& cC16(iV16560)& cowlThing(iV16560)& cC6(iV16561)& cowlThing(iV16561)& cC12(iV16562)& cowlThing(iV16562) ) ),
% 0.12/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f32,negated_conjecture,(
% 0.12/0.38 ~(( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& cC18(iV16560)& cC14(iV16560)& cC8(iV16560)& cC16(iV16560)& cowlThing(iV16560)& cC6(iV16561)& cowlThing(iV16561)& cC12(iV16562)& cowlThing(iV16562) ) )),
% 0.12/0.38 inference(negated_conjecture,[status(cth)],[f31])).
% 0.12/0.38 fof(f33,plain,(
% 0.12/0.38 (![X]: cowlThing(X))&(![X]: ~cowlNothing(X))),
% 0.12/0.38 inference(miniscoping,[status(thm)],[f1])).
% 0.12/0.38 fof(f34,plain,(
% 0.12/0.38 ![X0]: (cowlThing(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f33])).
% 0.12/0.38 fof(f35,plain,(
% 0.12/0.38 ![X0]: (~cowlNothing(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f33])).
% 0.12/0.38 fof(f36,plain,(
% 0.12/0.38 ![X]: ((~xsd_string(X)|~xsd_integer(X))&(xsd_string(X)|xsd_integer(X)))),
% 0.12/0.38 inference(NNF_transformation,[status(thm)],[f2])).
% 0.12/0.38 fof(f37,plain,(
% 0.12/0.38 (![X]: (~xsd_string(X)|~xsd_integer(X)))&(![X]: (xsd_string(X)|xsd_integer(X)))),
% 0.12/0.38 inference(miniscoping,[status(thm)],[f36])).
% 0.12/0.38 fof(f38,plain,(
% 0.12/0.38 ![X0]: (~xsd_string(X0)|~xsd_integer(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f37])).
% 0.12/0.38 fof(f39,plain,(
% 0.12/0.38 ![X0]: (xsd_string(X0)|xsd_integer(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f37])).
% 0.12/0.38 fof(f45,plain,(
% 0.12/0.38 ![X]: ((~cC10(X)|(?[Y]: (rR1(X,Y)&cC2xcomp(Y))))&(cC10(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.12/0.38 inference(NNF_transformation,[status(thm)],[f4])).
% 0.12/0.38 fof(f46,plain,(
% 0.12/0.38 (![X]: (~cC10(X)|(?[Y]: (rR1(X,Y)&cC2xcomp(Y)))))&(![X]: (cC10(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.12/0.38 inference(miniscoping,[status(thm)],[f45])).
% 0.12/0.38 fof(f47,plain,(
% 0.12/0.38 (![X]: (~cC10(X)|(rR1(X,sK1_skl(X))&cC2xcomp(sK1_skl(X)))))&(![X]: (cC10(X)|(![Y]: (~rR1(X,Y)|~cC2xcomp(Y)))))),
% 0.12/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Y,sK1_skl(X))],[f46])).
% 0.12/0.38 fof(f50,plain,(
% 0.12/0.38 ![X0,X1]: (cC10(X0)|~rR1(X0,X1)|~cC2xcomp(X1))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f47])).
% 0.12/0.38 fof(f57,plain,(
% 0.12/0.38 ![X]: ((~cC12(X)|(cC10xcomp(X)&cC2xcomp(X)))&(cC12(X)|(~cC10xcomp(X)|~cC2xcomp(X))))),
% 0.12/0.38 inference(NNF_transformation,[status(thm)],[f6])).
% 0.12/0.38 fof(f58,plain,(
% 0.12/0.38 (![X]: (~cC12(X)|(cC10xcomp(X)&cC2xcomp(X))))&(![X]: (cC12(X)|(~cC10xcomp(X)|~cC2xcomp(X))))),
% 0.12/0.38 inference(miniscoping,[status(thm)],[f57])).
% 0.12/0.38 fof(f59,plain,(
% 0.12/0.38 ![X0]: (~cC12(X0)|cC10xcomp(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f58])).
% 0.12/0.38 fof(f60,plain,(
% 0.12/0.38 ![X0]: (~cC12(X0)|cC2xcomp(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f58])).
% 0.12/0.38 fof(f61,plain,(
% 0.12/0.38 ![X0]: (cC12(X0)|~cC10xcomp(X0)|~cC2xcomp(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f58])).
% 0.12/0.38 fof(f62,plain,(
% 0.12/0.38 ![X]: ((~cC14(X)|(?[Y]: (rR1(X,Y)&cC12(Y))))&(cC14(X)|(![Y]: (~rR1(X,Y)|~cC12(Y)))))),
% 0.12/0.38 inference(NNF_transformation,[status(thm)],[f7])).
% 0.12/0.38 fof(f63,plain,(
% 0.12/0.38 (![X]: (~cC14(X)|(?[Y]: (rR1(X,Y)&cC12(Y)))))&(![X]: (cC14(X)|(![Y]: (~rR1(X,Y)|~cC12(Y)))))),
% 0.12/0.38 inference(miniscoping,[status(thm)],[f62])).
% 0.12/0.38 fof(f64,plain,(
% 0.12/0.38 (![X]: (~cC14(X)|(rR1(X,sK3_skl(X))&cC12(sK3_skl(X)))))&(![X]: (cC14(X)|(![Y]: (~rR1(X,Y)|~cC12(Y)))))),
% 0.12/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(Y,sK3_skl(X))],[f63])).
% 0.12/0.38 fof(f66,plain,(
% 0.12/0.38 ![X0]: (~cC14(X0)|cC12(sK3_skl(X0)))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f64])).
% 0.12/0.38 fof(f68,plain,(
% 0.12/0.38 ![X]: ((~cC16(X)|(cC14(X)&cC8(X)))&(cC16(X)|(~cC14(X)|~cC8(X))))),
% 0.12/0.38 inference(NNF_transformation,[status(thm)],[f8])).
% 0.12/0.38 fof(f69,plain,(
% 0.12/0.38 (![X]: (~cC16(X)|(cC14(X)&cC8(X))))&(![X]: (cC16(X)|(~cC14(X)|~cC8(X))))),
% 0.12/0.38 inference(miniscoping,[status(thm)],[f68])).
% 0.12/0.38 fof(f70,plain,(
% 0.12/0.38 ![X0]: (~cC16(X0)|cC14(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f69])).
% 0.12/0.38 fof(f71,plain,(
% 0.12/0.38 ![X0]: (~cC16(X0)|cC8(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f69])).
% 0.12/0.38 fof(f72,plain,(
% 0.12/0.38 ![X0]: (cC16(X0)|~cC14(X0)|~cC8(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f69])).
% 0.12/0.38 fof(f73,plain,(
% 0.12/0.38 ![X]: ((~cC18(X)|(cTOP(X)&cC16(X)))&(cC18(X)|(~cTOP(X)|~cC16(X))))),
% 0.12/0.38 inference(NNF_transformation,[status(thm)],[f9])).
% 0.12/0.38 fof(f74,plain,(
% 0.12/0.38 (![X]: (~cC18(X)|(cTOP(X)&cC16(X))))&(![X]: (cC18(X)|(~cTOP(X)|~cC16(X))))),
% 0.12/0.38 inference(miniscoping,[status(thm)],[f73])).
% 0.12/0.38 fof(f76,plain,(
% 0.12/0.38 ![X0]: (~cC18(X0)|cC16(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f74])).
% 0.12/0.38 fof(f77,plain,(
% 0.12/0.38 ![X0]: (cC18(X0)|~cTOP(X0)|~cC16(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f74])).
% 0.12/0.38 fof(f106,plain,(
% 0.12/0.38 ![X]: ((~cC6(X)|(cC4xcomp(X)&cC2xcomp(X)))&(cC6(X)|(~cC4xcomp(X)|~cC2xcomp(X))))),
% 0.12/0.38 inference(NNF_transformation,[status(thm)],[f15])).
% 0.12/0.38 fof(f107,plain,(
% 0.12/0.38 (![X]: (~cC6(X)|(cC4xcomp(X)&cC2xcomp(X))))&(![X]: (cC6(X)|(~cC4xcomp(X)|~cC2xcomp(X))))),
% 0.12/0.38 inference(miniscoping,[status(thm)],[f106])).
% 0.12/0.38 fof(f110,plain,(
% 0.12/0.38 ![X0]: (cC6(X0)|~cC4xcomp(X0)|~cC2xcomp(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f107])).
% 0.12/0.38 fof(f117,plain,(
% 0.12/0.38 ![X]: ((~cTEST(X)|(cTOP(X)&cC18(X)))&(cTEST(X)|(~cTOP(X)|~cC18(X))))),
% 0.12/0.38 inference(NNF_transformation,[status(thm)],[f17])).
% 0.12/0.38 fof(f118,plain,(
% 0.12/0.38 (![X]: (~cTEST(X)|(cTOP(X)&cC18(X))))&(![X]: (cTEST(X)|(~cTOP(X)|~cC18(X))))),
% 0.12/0.38 inference(miniscoping,[status(thm)],[f117])).
% 0.12/0.38 fof(f120,plain,(
% 0.12/0.38 ![X0]: (~cTEST(X0)|cC18(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f118])).
% 0.12/0.38 fof(f123,plain,(
% 0.12/0.38 cTEST(iV16560)),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f19])).
% 0.12/0.38 fof(f124,plain,(
% 0.12/0.38 cTOP(iV16560)),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f20])).
% 0.12/0.38 fof(f125,plain,(
% 0.12/0.38 rR1(iV16560,iV16562)),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f21])).
% 0.12/0.38 fof(f130,plain,(
% 0.12/0.38 cC4xcomp(iV16561)),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f25])).
% 0.12/0.38 fof(f131,plain,(
% 0.12/0.38 cC2xcomp(iV16561)),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f26])).
% 0.12/0.38 fof(f135,plain,(
% 0.12/0.38 cC10xcomp(iV16562)),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f29])).
% 0.12/0.38 fof(f136,plain,(
% 0.12/0.38 cC2xcomp(iV16562)),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f30])).
% 0.12/0.38 fof(f137,plain,(
% 0.12/0.38 (((((((((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: (xsd_string(X)<~>~xsd_integer(X))))|~cC18(iV16560))|~cC14(iV16560))|~cC8(iV16560))|~cC16(iV16560))|~cowlThing(iV16560))|~cC6(iV16561))|~cowlThing(iV16561))|~cC12(iV16562))|~cowlThing(iV16562))),
% 0.12/0.38 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 0.12/0.38 fof(f138,plain,(
% 0.12/0.38 ((((((((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: ((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))|~cC18(iV16560))|~cC14(iV16560))|~cC8(iV16560))|~cC16(iV16560))|~cowlThing(iV16560))|~cC6(iV16561))|~cowlThing(iV16561))|~cC12(iV16562))|~cowlThing(iV16562)),
% 0.12/0.38 inference(NNF_transformation,[status(thm)],[f137])).
% 0.12/0.38 fof(f139,plain,(
% 0.12/0.38 (((((((((((?[X]: ~cowlThing(X))|(?[X]: cowlNothing(X)))|(?[X]: ((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))|~cC18(iV16560))|~cC14(iV16560))|~cC8(iV16560))|~cC16(iV16560))|~cowlThing(iV16560))|~cC6(iV16561))|~cowlThing(iV16561))|~cC12(iV16562))|~cowlThing(iV16562)),
% 0.12/0.38 inference(miniscoping,[status(thm)],[f138])).
% 0.12/0.38 fof(f140,plain,(
% 0.12/0.38 ((((((((((~cowlThing(sK10_skl)|cowlNothing(sK11_skl))|((xsd_string(sK12_skl)|~xsd_integer(sK12_skl))&(~xsd_string(sK12_skl)|xsd_integer(sK12_skl))))|~cC18(iV16560))|~cC14(iV16560))|~cC8(iV16560))|~cC16(iV16560))|~cowlThing(iV16560))|~cC6(iV16561))|~cowlThing(iV16561))|~cC12(iV16562))|~cowlThing(iV16562)),
% 0.12/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl,sK12_skl]),skolemize(X,sK10_skl),skolemize(X,sK11_skl),skolemize(X,sK12_skl)],[f139])).
% 0.12/0.38 fof(f141,plain,(
% 0.12/0.38 ~cowlThing(sK10_skl)|cowlNothing(sK11_skl)|xsd_string(sK12_skl)|~xsd_integer(sK12_skl)|~cC18(iV16560)|~cC14(iV16560)|~cC8(iV16560)|~cC16(iV16560)|~cowlThing(iV16560)|~cC6(iV16561)|~cowlThing(iV16561)|~cC12(iV16562)|~cowlThing(iV16562)),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f140])).
% 0.12/0.38 fof(f142,plain,(
% 0.12/0.38 ~cowlThing(sK10_skl)|cowlNothing(sK11_skl)|~xsd_string(sK12_skl)|xsd_integer(sK12_skl)|~cC18(iV16560)|~cC14(iV16560)|~cC8(iV16560)|~cC16(iV16560)|~cowlThing(iV16560)|~cC6(iV16561)|~cowlThing(iV16561)|~cC12(iV16562)|~cowlThing(iV16562)),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f140])).
% 0.12/0.38 fof(f143,definition,(
% 0.12/0.38 sQ0_spl <=> (cowlThing(sK10_skl))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f145,plain,(
% 0.12/0.38 ~cowlThing(sK10_skl)|sQ0_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f143])).
% 0.12/0.38 fof(f146,definition,(
% 0.12/0.38 sQ1_spl <=> (cowlNothing(sK11_skl))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f147,plain,(
% 0.12/0.38 cowlNothing(sK11_skl)|~sQ1_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f146])).
% 0.12/0.38 fof(f149,definition,(
% 0.12/0.38 sQ2_spl <=> (xsd_string(sK12_skl))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f150,plain,(
% 0.12/0.38 xsd_string(sK12_skl)|~sQ2_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f149])).
% 0.12/0.38 fof(f152,definition,(
% 0.12/0.38 sQ3_spl <=> (xsd_integer(sK12_skl))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f153,plain,(
% 0.12/0.38 xsd_integer(sK12_skl)|~sQ3_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f152])).
% 0.12/0.38 fof(f154,plain,(
% 0.12/0.38 ~xsd_integer(sK12_skl)|sQ3_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f152])).
% 0.12/0.38 fof(f155,definition,(
% 0.12/0.38 sQ4_spl <=> (cC18(iV16560))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f158,definition,(
% 0.12/0.38 sQ5_spl <=> (cC14(iV16560))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f160,plain,(
% 0.12/0.38 ~cC14(iV16560)|sQ5_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f158])).
% 0.12/0.38 fof(f161,definition,(
% 0.12/0.38 sQ6_spl <=> (cC8(iV16560))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f163,plain,(
% 0.12/0.38 ~cC8(iV16560)|sQ6_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f161])).
% 0.12/0.38 fof(f164,definition,(
% 0.12/0.38 sQ7_spl <=> (cC16(iV16560))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f167,definition,(
% 0.12/0.38 sQ8_spl <=> (cowlThing(iV16560))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f169,plain,(
% 0.12/0.38 ~cowlThing(iV16560)|sQ8_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f167])).
% 0.12/0.38 fof(f170,definition,(
% 0.12/0.38 sQ9_spl <=> (cC6(iV16561))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f173,definition,(
% 0.12/0.38 sQ10_spl <=> (cowlThing(iV16561))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f175,plain,(
% 0.12/0.38 ~cowlThing(iV16561)|sQ10_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f173])).
% 0.12/0.38 fof(f176,definition,(
% 0.12/0.38 sQ11_spl <=> (cC12(iV16562))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f179,definition,(
% 0.12/0.38 sQ12_spl <=> (cowlThing(iV16562))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f181,plain,(
% 0.12/0.38 ~cowlThing(iV16562)|sQ12_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f179])).
% 0.12/0.38 fof(f182,plain,(
% 0.12/0.38 ~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),
% 0.12/0.38 inference(split_clause,[status(thm)],[f141,f143,f146,f149,f152,f155,f158,f161,f164,f167,f170,f173,f176,f179])).
% 0.12/0.38 fof(f183,plain,(
% 0.12/0.38 ~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),
% 0.12/0.38 inference(split_clause,[status(thm)],[f142,f143,f146,f149,f152,f155,f158,f161,f164,f167,f170,f173,f176,f179])).
% 0.12/0.38 fof(f184,plain,(
% 0.12/0.38 $false|sQ12_spl),
% 0.12/0.38 inference(backward_subsumption_resolution,[status(thm)],[f181,f34])).
% 0.12/0.38 fof(f185,plain,(
% 0.12/0.38 sQ12_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f184])).
% 0.12/0.38 fof(f188,plain,(
% 0.12/0.38 cC18(iV16560)),
% 0.12/0.38 inference(resolution,[status(thm)],[f120,f123])).
% 0.12/0.38 fof(f189,plain,(
% 0.12/0.38 cC16(iV16560)),
% 0.12/0.38 inference(resolution,[status(thm)],[f188,f76])).
% 0.12/0.38 fof(f190,plain,(
% 0.12/0.38 cC14(iV16560)),
% 0.12/0.38 inference(resolution,[status(thm)],[f189,f70])).
% 0.12/0.38 fof(f191,plain,(
% 0.12/0.38 cC16(iV16560)|~cC8(iV16560)),
% 0.12/0.38 inference(resolution,[status(thm)],[f190,f72])).
% 0.12/0.38 fof(f192,plain,(
% 0.12/0.38 sQ7_spl|~sQ6_spl),
% 0.12/0.38 inference(split_clause,[status(thm)],[f191,f164,f161])).
% 0.12/0.38 fof(f193,plain,(
% 0.12/0.38 ~cC16(iV16560)|sQ6_spl),
% 0.12/0.38 inference(resolution,[status(thm)],[f163,f71])).
% 0.12/0.38 fof(f194,plain,(
% 0.12/0.38 $false|sQ6_spl),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f193,f189])).
% 0.12/0.38 fof(f195,plain,(
% 0.12/0.38 sQ6_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f194])).
% 0.12/0.38 fof(f197,plain,(
% 0.12/0.38 cC10(iV16560)|~cC2xcomp(iV16562)),
% 0.12/0.38 inference(resolution,[status(thm)],[f50,f125])).
% 0.12/0.38 fof(f198,definition,(
% 0.12/0.38 sQ13_spl <=> (cC10(iV16560))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f201,definition,(
% 0.12/0.38 sQ14_spl <=> (cC2xcomp(iV16561))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f203,plain,(
% 0.12/0.38 ~cC2xcomp(iV16561)|sQ14_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f201])).
% 0.12/0.38 fof(f205,definition,(
% 0.12/0.38 sQ15_spl <=> (cC2xcomp(iV16562))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f207,plain,(
% 0.12/0.38 ~cC2xcomp(iV16562)|sQ15_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f205])).
% 0.12/0.38 fof(f208,plain,(
% 0.12/0.38 sQ13_spl|~sQ15_spl),
% 0.12/0.38 inference(split_clause,[status(thm)],[f197,f198,f205])).
% 0.12/0.38 fof(f211,plain,(
% 0.12/0.38 cC12(iV16562)|~cC2xcomp(iV16562)),
% 0.12/0.38 inference(resolution,[status(thm)],[f61,f135])).
% 0.12/0.38 fof(f212,plain,(
% 0.12/0.38 sQ11_spl|~sQ15_spl),
% 0.12/0.38 inference(split_clause,[status(thm)],[f211,f176,f205])).
% 0.12/0.38 fof(f213,plain,(
% 0.12/0.38 $false|sQ15_spl),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f207,f136])).
% 0.12/0.38 fof(f214,plain,(
% 0.12/0.38 sQ15_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f213])).
% 0.12/0.38 fof(f215,plain,(
% 0.12/0.38 $false|sQ10_spl),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f175,f34])).
% 0.12/0.38 fof(f216,plain,(
% 0.12/0.38 sQ10_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f215])).
% 0.12/0.38 fof(f232,plain,(
% 0.12/0.38 cC12(sK3_skl(iV16560))),
% 0.12/0.38 inference(resolution,[status(thm)],[f66,f190])).
% 0.12/0.38 fof(f234,plain,(
% 0.12/0.38 cC10xcomp(sK3_skl(iV16560))),
% 0.12/0.38 inference(resolution,[status(thm)],[f232,f59])).
% 0.12/0.38 fof(f235,plain,(
% 0.12/0.38 cC2xcomp(sK3_skl(iV16560))),
% 0.12/0.38 inference(resolution,[status(thm)],[f232,f60])).
% 0.12/0.38 fof(f236,plain,(
% 0.12/0.38 cC12(sK3_skl(iV16560))|~cC2xcomp(sK3_skl(iV16560))),
% 0.12/0.38 inference(resolution,[status(thm)],[f234,f61])).
% 0.12/0.38 fof(f237,definition,(
% 0.12/0.38 sQ17_spl <=> (cC12(sK3_skl(iV16560)))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f240,definition,(
% 0.12/0.38 sQ18_spl <=> (cC2xcomp(sK3_skl(iV16560)))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f242,plain,(
% 0.12/0.38 ~cC2xcomp(sK3_skl(iV16560))|sQ18_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f240])).
% 0.12/0.38 fof(f243,plain,(
% 0.12/0.38 sQ17_spl|~sQ18_spl),
% 0.12/0.38 inference(split_clause,[status(thm)],[f236,f237,f240])).
% 0.12/0.38 fof(f251,plain,(
% 0.12/0.38 cC18(iV16560)|~cTOP(iV16560)),
% 0.12/0.38 inference(resolution,[status(thm)],[f77,f189])).
% 0.12/0.38 fof(f252,definition,(
% 0.12/0.38 sQ19_spl <=> (cTOP(iV16560))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f254,plain,(
% 0.12/0.38 ~cTOP(iV16560)|sQ19_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f252])).
% 0.12/0.38 fof(f255,plain,(
% 0.12/0.38 sQ4_spl|~sQ19_spl),
% 0.12/0.38 inference(split_clause,[status(thm)],[f251,f155,f252])).
% 0.12/0.38 fof(f260,plain,(
% 0.12/0.38 $false|sQ18_spl),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f242,f235])).
% 0.12/0.38 fof(f261,plain,(
% 0.12/0.38 sQ18_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f260])).
% 0.12/0.38 fof(f267,plain,(
% 0.12/0.38 cC6(iV16561)|~cC2xcomp(iV16561)),
% 0.12/0.38 inference(resolution,[status(thm)],[f110,f130])).
% 0.12/0.38 fof(f276,plain,(
% 0.12/0.38 sQ9_spl|~sQ14_spl),
% 0.12/0.38 inference(split_clause,[status(thm)],[f267,f170,f201])).
% 0.12/0.38 fof(f277,plain,(
% 0.12/0.38 $false|sQ14_spl),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f203,f131])).
% 0.12/0.38 fof(f278,plain,(
% 0.12/0.38 sQ14_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f277])).
% 0.12/0.38 fof(f279,plain,(
% 0.12/0.38 $false|sQ8_spl),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f169,f34])).
% 0.12/0.38 fof(f280,plain,(
% 0.12/0.38 sQ8_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f279])).
% 0.12/0.38 fof(f281,plain,(
% 0.12/0.38 $false|sQ5_spl),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f160,f190])).
% 0.12/0.38 fof(f282,plain,(
% 0.12/0.38 sQ5_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f281])).
% 0.12/0.38 fof(f283,plain,(
% 0.12/0.38 $false|~sQ1_spl),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f147,f35])).
% 0.12/0.38 fof(f284,plain,(
% 0.12/0.38 ~sQ1_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f283])).
% 0.12/0.38 fof(f285,plain,(
% 0.12/0.38 $false|sQ0_spl),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f145,f34])).
% 0.12/0.38 fof(f286,plain,(
% 0.12/0.38 sQ0_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f285])).
% 0.12/0.38 fof(f290,plain,(
% 0.12/0.38 ~xsd_string(sK12_skl)|~sQ3_spl),
% 0.12/0.38 inference(resolution,[status(thm)],[f153,f38])).
% 0.12/0.38 fof(f291,plain,(
% 0.12/0.38 $false|~sQ2_spl|~sQ3_spl),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f290,f150])).
% 0.12/0.38 fof(f292,plain,(
% 0.12/0.38 ~sQ2_spl|~sQ3_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f291])).
% 0.12/0.38 fof(f293,plain,(
% 0.12/0.38 xsd_string(sK12_skl)|sQ3_spl),
% 0.12/0.38 inference(resolution,[status(thm)],[f154,f39])).
% 0.12/0.38 fof(f294,plain,(
% 0.12/0.38 sQ2_spl|sQ3_spl),
% 0.12/0.38 inference(split_clause,[status(thm)],[f293,f149,f152])).
% 0.12/0.38 fof(f295,plain,(
% 0.12/0.38 $false|sQ19_spl),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f254,f124])).
% 0.12/0.38 fof(f296,plain,(
% 0.12/0.38 sQ19_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f295])).
% 0.12/0.38 fof(f297,plain,(
% 0.12/0.38 $false),
% 0.12/0.38 inference(sat_refutation,[status(thm)],[f182,f183,f185,f192,f195,f208,f212,f214,f216,f243,f255,f261,f276,f278,f280,f282,f284,f286,f292,f294,f296])).
% 0.12/0.38 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.40 % Elapsed time: 0.049258 seconds
% 0.12/0.40 % CPU time: 0.121317 seconds
% 0.12/0.40 % Total memory used: 18.955 MB
% 0.12/0.40 % Net memory used: 18.861 MB
%------------------------------------------------------------------------------