%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS146+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 : n002.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.09s 0.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS146+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.54 % Computer : n002.cluster.edu
% 0.09/0.54 % Model : x86_64 x86_64
% 0.09/0.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.54 % Memory : 8046.5625MB
% 0.09/0.54 % OS : Linux 6.8.0-71-generic
% 0.09/0.54 % CPULimit : 300
% 0.09/0.54 % WCLimit : 300
% 0.09/0.54 % DateTime : Sun Sep 20 22:57:18 UTC 2026
% 0.09/0.54 % CPUTime :
% 0.09/0.55 % Drodi V4.1.1
% 0.09/0.57 % Refutation found
% 0.09/0.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.57 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.57 fof(f1,axiom,(
% 0.09/0.57 (! [X] :( cowlThing(X)& ~ cowlNothing(X) ) )),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f2,axiom,(
% 0.09/0.57 (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ) )),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f5,axiom,(
% 0.09/0.57 (! [X] :( cC104(X)<=> ( cC34(X)& cC4(X) ) ) )),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f9,axiom,(
% 0.09/0.57 (! [X] :( cC112(X)<=> ( ~ cC110(X)& cC4(X) ) ) )),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f10,axiom,(
% 0.09/0.57 (! [X] :( cC114(X)<=> ( ~ cC96(X)& ~ cC112(X) ) ) )),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f11,axiom,(
% 0.09/0.57 (! [X] :( cC116(X)<=> ( cC114(X)& cC80(X) ) ) )),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f12,axiom,(
% 0.09/0.57 (! [X] :( cC118(X)<=> ( ~ cC10(X)& cC4(X) ) ) )),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f22,axiom,(
% 0.09/0.57 (! [X] :( cC136(X)<=> ( cC116(X)& ~ cC134(X) ) ) )),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f44,axiom,(
% 0.09/0.57 (! [X] :( cC56(X)<=> ( cC4(X)& ~ cC10(X) ) ) )),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f45,axiom,(
% 0.09/0.57 (! [X] :( cC58(X)<=> ( cC34(X)& cC56(X) ) ) )),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f55,axiom,(
% 0.09/0.57 (! [X] :( cC76(X)<=> ( ~ cC2(X)& cC4(X) ) ) )),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f58,axiom,(
% 0.09/0.57 (! [X] :( cC80(X)<=> ( ~ cC78(X)& ~ cC76(X) ) ) )),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f66,axiom,(
% 0.09/0.57 (! [X] :( cC96(X)<=> ( ~ cC94(X)& cC2(X) ) ) )),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f72,axiom,(
% 0.09/0.57 ~ cC134(iV822576) ),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f75,axiom,(
% 0.09/0.57 cC34(iV822576) ),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f76,axiom,(
% 0.09/0.57 cC4(iV822576) ),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f77,axiom,(
% 0.09/0.57 ~ cC96(iV822576) ),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f85,axiom,(
% 0.09/0.57 ~ cC10(iV822576) ),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f87,axiom,(
% 0.09/0.57 ~ cC76(iV822576) ),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f88,axiom,(
% 0.09/0.57 ~ cC112(iV822576) ),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f89,axiom,(
% 0.09/0.57 ~ cC78(iV822576) ),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f92,conjecture,(
% 0.09/0.57 ( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& cC94(iV822576)& cowlThing(iV822576)& cC58(iV822576)& cC116(iV822576)& cC56(iV822576)& cC110(iV822576)& cC114(iV822576)& cC136(iV822576)& cC80(iV822576) ) ),
% 0.09/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f93,negated_conjecture,(
% 0.09/0.57 ~(( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& cC94(iV822576)& cowlThing(iV822576)& cC58(iV822576)& cC116(iV822576)& cC56(iV822576)& cC110(iV822576)& cC114(iV822576)& cC136(iV822576)& cC80(iV822576) ) )),
% 0.09/0.57 inference(negated_conjecture,[status(cth)],[f92])).
% 0.09/0.57 fof(f94,plain,(
% 0.09/0.57 (![X]: cowlThing(X))&(![X]: ~cowlNothing(X))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f1])).
% 0.09/0.57 fof(f95,plain,(
% 0.09/0.57 ![X0]: (cowlThing(X0))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f94])).
% 0.09/0.57 fof(f96,plain,(
% 0.09/0.57 ![X0]: (~cowlNothing(X0))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f94])).
% 0.09/0.57 fof(f97,plain,(
% 0.09/0.57 ![X]: ((~xsd_string(X)|~xsd_integer(X))&(xsd_string(X)|xsd_integer(X)))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f2])).
% 0.09/0.57 fof(f98,plain,(
% 0.09/0.57 (![X]: (~xsd_string(X)|~xsd_integer(X)))&(![X]: (xsd_string(X)|xsd_integer(X)))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f97])).
% 0.09/0.57 fof(f99,plain,(
% 0.09/0.57 ![X0]: (~xsd_string(X0)|~xsd_integer(X0))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f98])).
% 0.09/0.57 fof(f100,plain,(
% 0.09/0.57 ![X0]: (xsd_string(X0)|xsd_integer(X0))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f98])).
% 0.09/0.57 fof(f112,plain,(
% 0.09/0.57 ![X]: ((~cC104(X)|(cC34(X)&cC4(X)))&(cC104(X)|(~cC34(X)|~cC4(X))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f5])).
% 0.09/0.57 fof(f113,plain,(
% 0.09/0.57 (![X]: (~cC104(X)|(cC34(X)&cC4(X))))&(![X]: (cC104(X)|(~cC34(X)|~cC4(X))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f112])).
% 0.09/0.57 fof(f116,plain,(
% 0.09/0.57 ![X0]: (cC104(X0)|~cC34(X0)|~cC4(X0))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f113])).
% 0.09/0.57 fof(f133,plain,(
% 0.09/0.57 ![X]: ((~cC112(X)|(~cC110(X)&cC4(X)))&(cC112(X)|(cC110(X)|~cC4(X))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f9])).
% 0.09/0.57 fof(f134,plain,(
% 0.09/0.57 (![X]: (~cC112(X)|(~cC110(X)&cC4(X))))&(![X]: (cC112(X)|(cC110(X)|~cC4(X))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f133])).
% 0.09/0.57 fof(f137,plain,(
% 0.09/0.57 ![X0]: (cC112(X0)|cC110(X0)|~cC4(X0))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f134])).
% 0.09/0.57 fof(f138,plain,(
% 0.09/0.57 ![X]: ((~cC114(X)|(~cC96(X)&~cC112(X)))&(cC114(X)|(cC96(X)|cC112(X))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f10])).
% 0.09/0.57 fof(f139,plain,(
% 0.09/0.57 (![X]: (~cC114(X)|(~cC96(X)&~cC112(X))))&(![X]: (cC114(X)|(cC96(X)|cC112(X))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f138])).
% 0.09/0.57 fof(f142,plain,(
% 0.09/0.57 ![X0]: (cC114(X0)|cC96(X0)|cC112(X0))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f139])).
% 0.09/0.57 fof(f143,plain,(
% 0.09/0.57 ![X]: ((~cC116(X)|(cC114(X)&cC80(X)))&(cC116(X)|(~cC114(X)|~cC80(X))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f11])).
% 0.09/0.57 fof(f144,plain,(
% 0.09/0.57 (![X]: (~cC116(X)|(cC114(X)&cC80(X))))&(![X]: (cC116(X)|(~cC114(X)|~cC80(X))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f143])).
% 0.09/0.57 fof(f147,plain,(
% 0.09/0.57 ![X0]: (cC116(X0)|~cC114(X0)|~cC80(X0))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f144])).
% 0.09/0.57 fof(f148,plain,(
% 0.09/0.57 ![X]: ((~cC118(X)|(~cC10(X)&cC4(X)))&(cC118(X)|(cC10(X)|~cC4(X))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f12])).
% 0.09/0.57 fof(f149,plain,(
% 0.09/0.57 (![X]: (~cC118(X)|(~cC10(X)&cC4(X))))&(![X]: (cC118(X)|(cC10(X)|~cC4(X))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f148])).
% 0.09/0.57 fof(f152,plain,(
% 0.09/0.57 ![X0]: (cC118(X0)|cC10(X0)|~cC4(X0))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f149])).
% 0.09/0.57 fof(f200,plain,(
% 0.09/0.57 ![X]: ((~cC136(X)|(cC116(X)&~cC134(X)))&(cC136(X)|(~cC116(X)|cC134(X))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f22])).
% 0.09/0.57 fof(f201,plain,(
% 0.09/0.57 (![X]: (~cC136(X)|(cC116(X)&~cC134(X))))&(![X]: (cC136(X)|(~cC116(X)|cC134(X))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f200])).
% 0.09/0.57 fof(f204,plain,(
% 0.09/0.57 ![X0]: (cC136(X0)|~cC116(X0)|cC134(X0))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f201])).
% 0.09/0.57 fof(f315,plain,(
% 0.09/0.57 ![X]: ((~cC56(X)|(cC4(X)&~cC10(X)))&(cC56(X)|(~cC4(X)|cC10(X))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f44])).
% 0.09/0.57 fof(f316,plain,(
% 0.09/0.57 (![X]: (~cC56(X)|(cC4(X)&~cC10(X))))&(![X]: (cC56(X)|(~cC4(X)|cC10(X))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f315])).
% 0.09/0.57 fof(f319,plain,(
% 0.09/0.57 ![X0]: (cC56(X0)|~cC4(X0)|cC10(X0))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f316])).
% 0.09/0.57 fof(f320,plain,(
% 0.09/0.57 ![X]: ((~cC58(X)|(cC34(X)&cC56(X)))&(cC58(X)|(~cC34(X)|~cC56(X))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f45])).
% 0.09/0.57 fof(f321,plain,(
% 0.09/0.57 (![X]: (~cC58(X)|(cC34(X)&cC56(X))))&(![X]: (cC58(X)|(~cC34(X)|~cC56(X))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f320])).
% 0.09/0.57 fof(f324,plain,(
% 0.09/0.57 ![X0]: (cC58(X0)|~cC34(X0)|~cC56(X0))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f321])).
% 0.09/0.57 fof(f372,plain,(
% 0.09/0.57 ![X]: ((~cC76(X)|(~cC2(X)&cC4(X)))&(cC76(X)|(cC2(X)|~cC4(X))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f55])).
% 0.09/0.57 fof(f373,plain,(
% 0.09/0.57 (![X]: (~cC76(X)|(~cC2(X)&cC4(X))))&(![X]: (cC76(X)|(cC2(X)|~cC4(X))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f372])).
% 0.09/0.57 fof(f376,plain,(
% 0.09/0.57 ![X0]: (cC76(X0)|cC2(X0)|~cC4(X0))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f373])).
% 0.09/0.57 fof(f387,plain,(
% 0.09/0.57 ![X]: ((~cC80(X)|(~cC78(X)&~cC76(X)))&(cC80(X)|(cC78(X)|cC76(X))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f58])).
% 0.09/0.57 fof(f388,plain,(
% 0.09/0.57 (![X]: (~cC80(X)|(~cC78(X)&~cC76(X))))&(![X]: (cC80(X)|(cC78(X)|cC76(X))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f387])).
% 0.09/0.57 fof(f391,plain,(
% 0.09/0.57 ![X0]: (cC80(X0)|cC78(X0)|cC76(X0))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f388])).
% 0.09/0.57 fof(f429,plain,(
% 0.09/0.57 ![X]: ((~cC96(X)|(~cC94(X)&cC2(X)))&(cC96(X)|(cC94(X)|~cC2(X))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f66])).
% 0.09/0.57 fof(f430,plain,(
% 0.09/0.57 (![X]: (~cC96(X)|(~cC94(X)&cC2(X))))&(![X]: (cC96(X)|(cC94(X)|~cC2(X))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f429])).
% 0.09/0.57 fof(f433,plain,(
% 0.09/0.57 ![X0]: (cC96(X0)|cC94(X0)|~cC2(X0))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f430])).
% 0.09/0.57 fof(f447,plain,(
% 0.09/0.57 ~cC134(iV822576)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f72])).
% 0.09/0.57 fof(f451,plain,(
% 0.09/0.57 cC34(iV822576)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f75])).
% 0.09/0.57 fof(f452,plain,(
% 0.09/0.57 cC4(iV822576)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f76])).
% 0.09/0.57 fof(f453,plain,(
% 0.09/0.57 ~cC96(iV822576)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f77])).
% 0.09/0.57 fof(f462,plain,(
% 0.09/0.57 ~cC10(iV822576)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f85])).
% 0.09/0.57 fof(f464,plain,(
% 0.09/0.57 ~cC76(iV822576)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f87])).
% 0.09/0.57 fof(f465,plain,(
% 0.09/0.57 ~cC112(iV822576)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f88])).
% 0.09/0.57 fof(f466,plain,(
% 0.09/0.57 ~cC78(iV822576)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f89])).
% 0.09/0.57 fof(f470,plain,(
% 0.09/0.57 (((((((((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: (xsd_string(X)<~>~xsd_integer(X))))|~cC94(iV822576))|~cowlThing(iV822576))|~cC58(iV822576))|~cC116(iV822576))|~cC56(iV822576))|~cC110(iV822576))|~cC114(iV822576))|~cC136(iV822576))|~cC80(iV822576))),
% 0.09/0.57 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 0.09/0.57 fof(f471,plain,(
% 0.09/0.57 ((((((((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: ((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))|~cC94(iV822576))|~cowlThing(iV822576))|~cC58(iV822576))|~cC116(iV822576))|~cC56(iV822576))|~cC110(iV822576))|~cC114(iV822576))|~cC136(iV822576))|~cC80(iV822576)),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f470])).
% 0.09/0.57 fof(f472,plain,(
% 0.09/0.57 (((((((((((?[X]: ~cowlThing(X))|(?[X]: cowlNothing(X)))|(?[X]: ((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))|~cC94(iV822576))|~cowlThing(iV822576))|~cC58(iV822576))|~cC116(iV822576))|~cC56(iV822576))|~cC110(iV822576))|~cC114(iV822576))|~cC136(iV822576))|~cC80(iV822576)),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f471])).
% 0.09/0.57 fof(f473,plain,(
% 0.09/0.57 ((((((((((~cowlThing(sK13_skl)|cowlNothing(sK14_skl))|((xsd_string(sK15_skl)|~xsd_integer(sK15_skl))&(~xsd_string(sK15_skl)|xsd_integer(sK15_skl))))|~cC94(iV822576))|~cowlThing(iV822576))|~cC58(iV822576))|~cC116(iV822576))|~cC56(iV822576))|~cC110(iV822576))|~cC114(iV822576))|~cC136(iV822576))|~cC80(iV822576)),
% 0.09/0.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl]),skolemize(X,sK13_skl),skolemize(X,sK14_skl),skolemize(X,sK15_skl)],[f472])).
% 0.09/0.57 fof(f474,plain,(
% 0.09/0.57 ~cowlThing(sK13_skl)|cowlNothing(sK14_skl)|xsd_string(sK15_skl)|~xsd_integer(sK15_skl)|~cC94(iV822576)|~cowlThing(iV822576)|~cC58(iV822576)|~cC116(iV822576)|~cC56(iV822576)|~cC110(iV822576)|~cC114(iV822576)|~cC136(iV822576)|~cC80(iV822576)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f473])).
% 0.09/0.57 fof(f475,plain,(
% 0.09/0.57 ~cowlThing(sK13_skl)|cowlNothing(sK14_skl)|~xsd_string(sK15_skl)|xsd_integer(sK15_skl)|~cC94(iV822576)|~cowlThing(iV822576)|~cC58(iV822576)|~cC116(iV822576)|~cC56(iV822576)|~cC110(iV822576)|~cC114(iV822576)|~cC136(iV822576)|~cC80(iV822576)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f473])).
% 0.09/0.57 fof(f476,definition,(
% 0.09/0.57 sQ0_spl <=> (cowlThing(sK13_skl))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f478,plain,(
% 0.09/0.57 ~cowlThing(sK13_skl)|sQ0_spl),
% 0.09/0.57 inference(component_clause,[status(thm)],[f476])).
% 0.09/0.57 fof(f479,definition,(
% 0.09/0.57 sQ1_spl <=> (cowlNothing(sK14_skl))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f480,plain,(
% 0.09/0.57 cowlNothing(sK14_skl)|~sQ1_spl),
% 0.09/0.57 inference(component_clause,[status(thm)],[f479])).
% 0.09/0.57 fof(f482,definition,(
% 0.09/0.57 sQ2_spl <=> (xsd_string(sK15_skl))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f483,plain,(
% 0.09/0.57 xsd_string(sK15_skl)|~sQ2_spl),
% 0.09/0.57 inference(component_clause,[status(thm)],[f482])).
% 0.09/0.57 fof(f485,definition,(
% 0.09/0.57 sQ3_spl <=> (xsd_integer(sK15_skl))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f486,plain,(
% 0.09/0.57 xsd_integer(sK15_skl)|~sQ3_spl),
% 0.09/0.57 inference(component_clause,[status(thm)],[f485])).
% 0.09/0.57 fof(f487,plain,(
% 0.09/0.57 ~xsd_integer(sK15_skl)|sQ3_spl),
% 0.09/0.57 inference(component_clause,[status(thm)],[f485])).
% 0.09/0.57 fof(f488,definition,(
% 0.09/0.57 sQ4_spl <=> (cC94(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f490,plain,(
% 0.09/0.57 ~cC94(iV822576)|sQ4_spl),
% 0.09/0.57 inference(component_clause,[status(thm)],[f488])).
% 0.09/0.57 fof(f491,definition,(
% 0.09/0.57 sQ5_spl <=> (cowlThing(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f493,plain,(
% 0.09/0.57 ~cowlThing(iV822576)|sQ5_spl),
% 0.09/0.57 inference(component_clause,[status(thm)],[f491])).
% 0.09/0.57 fof(f494,definition,(
% 0.09/0.57 sQ6_spl <=> (cC58(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f497,definition,(
% 0.09/0.57 sQ7_spl <=> (cC116(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f498,plain,(
% 0.09/0.57 cC116(iV822576)|~sQ7_spl),
% 0.09/0.57 inference(component_clause,[status(thm)],[f497])).
% 0.09/0.57 fof(f500,definition,(
% 0.09/0.57 sQ8_spl <=> (cC56(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f501,plain,(
% 0.09/0.57 cC56(iV822576)|~sQ8_spl),
% 0.09/0.57 inference(component_clause,[status(thm)],[f500])).
% 0.09/0.57 fof(f503,definition,(
% 0.09/0.57 sQ9_spl <=> (cC110(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f506,definition,(
% 0.09/0.57 sQ10_spl <=> (cC114(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f509,definition,(
% 0.09/0.57 sQ11_spl <=> (cC136(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f512,definition,(
% 0.09/0.57 sQ12_spl <=> (cC80(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f513,plain,(
% 0.09/0.57 cC80(iV822576)|~sQ12_spl),
% 0.09/0.57 inference(component_clause,[status(thm)],[f512])).
% 0.09/0.57 fof(f515,plain,(
% 0.09/0.57 ~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.09/0.57 inference(split_clause,[status(thm)],[f474,f476,f479,f482,f485,f488,f491,f494,f497,f500,f503,f506,f509,f512])).
% 0.09/0.57 fof(f516,plain,(
% 0.09/0.57 ~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.09/0.57 inference(split_clause,[status(thm)],[f475,f476,f479,f482,f485,f488,f491,f494,f497,f500,f503,f506,f509,f512])).
% 0.09/0.57 fof(f519,plain,(
% 0.09/0.57 cC56(iV822576)|cC10(iV822576)),
% 0.09/0.57 inference(resolution,[status(thm)],[f452,f319])).
% 0.09/0.57 fof(f523,definition,(
% 0.09/0.57 sQ14_spl <=> (cC34(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f525,plain,(
% 0.09/0.57 ~cC34(iV822576)|sQ14_spl),
% 0.09/0.57 inference(component_clause,[status(thm)],[f523])).
% 0.09/0.57 fof(f527,definition,(
% 0.09/0.57 sQ15_spl <=> (cC10(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f528,plain,(
% 0.09/0.57 cC10(iV822576)|~sQ15_spl),
% 0.09/0.57 inference(component_clause,[status(thm)],[f527])).
% 0.09/0.57 fof(f530,plain,(
% 0.09/0.57 sQ8_spl|sQ15_spl),
% 0.09/0.57 inference(split_clause,[status(thm)],[f519,f500,f527])).
% 0.09/0.57 fof(f531,plain,(
% 0.09/0.57 cC58(iV822576)|~cC34(iV822576)|~sQ8_spl),
% 0.09/0.57 inference(resolution,[status(thm)],[f501,f324])).
% 0.09/0.57 fof(f534,plain,(
% 0.09/0.57 sQ6_spl|~sQ14_spl|~sQ8_spl),
% 0.09/0.57 inference(split_clause,[status(thm)],[f531,f494,f523,f500])).
% 0.09/0.57 fof(f537,plain,(
% 0.09/0.57 cC114(iV822576)|cC112(iV822576)),
% 0.09/0.57 inference(resolution,[status(thm)],[f453,f142])).
% 0.09/0.57 fof(f538,definition,(
% 0.09/0.57 sQ16_spl <=> (cC112(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f539,plain,(
% 0.09/0.57 cC112(iV822576)|~sQ16_spl),
% 0.09/0.57 inference(component_clause,[status(thm)],[f538])).
% 0.09/0.57 fof(f541,plain,(
% 0.09/0.57 sQ10_spl|sQ16_spl),
% 0.09/0.57 inference(split_clause,[status(thm)],[f537,f506,f538])).
% 0.09/0.57 fof(f555,plain,(
% 0.09/0.57 $false|~sQ15_spl),
% 0.09/0.57 inference(forward_subsumption_resolution,[status(thm)],[f528,f462])).
% 0.09/0.57 fof(f556,plain,(
% 0.09/0.57 ~sQ15_spl),
% 0.09/0.57 inference(contradiction_clause,[status(thm)],[f555])).
% 0.09/0.57 fof(f563,plain,(
% 0.09/0.57 cC118(iV822576)|~cC4(iV822576)),
% 0.09/0.57 inference(resolution,[status(thm)],[f462,f152])).
% 0.09/0.57 fof(f564,definition,(
% 0.09/0.57 sQ20_spl <=> (cC118(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f567,definition,(
% 0.09/0.57 sQ21_spl <=> (cC4(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f569,plain,(
% 0.09/0.57 ~cC4(iV822576)|sQ21_spl),
% 0.09/0.57 inference(component_clause,[status(thm)],[f567])).
% 0.09/0.57 fof(f570,plain,(
% 0.09/0.57 sQ20_spl|~sQ21_spl),
% 0.09/0.57 inference(split_clause,[status(thm)],[f563,f564,f567])).
% 0.09/0.57 fof(f571,plain,(
% 0.09/0.57 cC2(iV822576)|~cC4(iV822576)),
% 0.09/0.57 inference(resolution,[status(thm)],[f464,f376])).
% 0.09/0.57 fof(f572,definition,(
% 0.09/0.57 sQ22_spl <=> (cC2(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f575,plain,(
% 0.09/0.57 sQ22_spl|~sQ21_spl),
% 0.09/0.57 inference(split_clause,[status(thm)],[f571,f572,f567])).
% 0.09/0.57 fof(f576,plain,(
% 0.09/0.57 $false|sQ21_spl),
% 0.09/0.57 inference(forward_subsumption_resolution,[status(thm)],[f569,f452])).
% 0.09/0.57 fof(f577,plain,(
% 0.09/0.57 sQ21_spl),
% 0.09/0.57 inference(contradiction_clause,[status(thm)],[f576])).
% 0.09/0.57 fof(f578,plain,(
% 0.09/0.57 cC104(iV822576)|~cC34(iV822576)),
% 0.09/0.57 inference(resolution,[status(thm)],[f116,f452])).
% 0.09/0.57 fof(f579,definition,(
% 0.09/0.57 sQ23_spl <=> (cC104(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f582,plain,(
% 0.09/0.57 sQ23_spl|~sQ14_spl),
% 0.09/0.57 inference(split_clause,[status(thm)],[f578,f579,f523])).
% 0.09/0.57 fof(f585,plain,(
% 0.09/0.57 cC110(iV822576)|~cC4(iV822576)),
% 0.09/0.57 inference(resolution,[status(thm)],[f465,f137])).
% 0.09/0.57 fof(f586,plain,(
% 0.09/0.57 sQ9_spl|~sQ21_spl),
% 0.09/0.57 inference(split_clause,[status(thm)],[f585,f503,f567])).
% 0.09/0.57 fof(f588,plain,(
% 0.09/0.57 cC80(iV822576)|cC76(iV822576)),
% 0.09/0.57 inference(resolution,[status(thm)],[f466,f391])).
% 0.09/0.57 fof(f590,definition,(
% 0.09/0.57 sQ24_spl <=> (cC76(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f591,plain,(
% 0.09/0.57 cC76(iV822576)|~sQ24_spl),
% 0.09/0.57 inference(component_clause,[status(thm)],[f590])).
% 0.09/0.57 fof(f593,plain,(
% 0.09/0.57 sQ12_spl|sQ24_spl),
% 0.09/0.57 inference(split_clause,[status(thm)],[f588,f512,f590])).
% 0.09/0.57 fof(f595,plain,(
% 0.09/0.57 cC116(iV822576)|~cC114(iV822576)|~sQ12_spl),
% 0.09/0.57 inference(resolution,[status(thm)],[f513,f147])).
% 0.09/0.57 fof(f596,plain,(
% 0.09/0.57 sQ7_spl|~sQ10_spl|~sQ12_spl),
% 0.09/0.57 inference(split_clause,[status(thm)],[f595,f497,f506,f512])).
% 0.09/0.57 fof(f597,plain,(
% 0.09/0.57 $false|~sQ16_spl),
% 0.09/0.57 inference(forward_subsumption_resolution,[status(thm)],[f539,f465])).
% 0.09/0.57 fof(f598,plain,(
% 0.09/0.57 ~sQ16_spl),
% 0.09/0.57 inference(contradiction_clause,[status(thm)],[f597])).
% 0.09/0.57 fof(f599,plain,(
% 0.09/0.57 $false|~sQ24_spl),
% 0.09/0.57 inference(forward_subsumption_resolution,[status(thm)],[f591,f464])).
% 0.09/0.57 fof(f600,plain,(
% 0.09/0.57 ~sQ24_spl),
% 0.09/0.57 inference(contradiction_clause,[status(thm)],[f599])).
% 0.09/0.57 fof(f611,plain,(
% 0.09/0.57 cC136(iV822576)|cC134(iV822576)|~sQ7_spl),
% 0.09/0.57 inference(resolution,[status(thm)],[f498,f204])).
% 0.09/0.57 fof(f614,definition,(
% 0.09/0.57 sQ26_spl <=> (cC134(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f615,plain,(
% 0.09/0.57 cC134(iV822576)|~sQ26_spl),
% 0.09/0.57 inference(component_clause,[status(thm)],[f614])).
% 0.09/0.57 fof(f617,plain,(
% 0.09/0.57 sQ11_spl|sQ26_spl|~sQ7_spl),
% 0.09/0.57 inference(split_clause,[status(thm)],[f611,f509,f614,f497])).
% 0.09/0.57 fof(f618,plain,(
% 0.09/0.57 $false|sQ5_spl),
% 0.09/0.57 inference(forward_subsumption_resolution,[status(thm)],[f493,f95])).
% 0.09/0.57 fof(f619,plain,(
% 0.09/0.57 sQ5_spl),
% 0.09/0.57 inference(contradiction_clause,[status(thm)],[f618])).
% 0.09/0.57 fof(f624,plain,(
% 0.09/0.57 cC96(iV822576)|~cC2(iV822576)|sQ4_spl),
% 0.09/0.57 inference(resolution,[status(thm)],[f490,f433])).
% 0.09/0.57 fof(f626,definition,(
% 0.09/0.57 sQ27_spl <=> (cC96(iV822576))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.09/0.57 fof(f627,plain,(
% 0.09/0.57 cC96(iV822576)|~sQ27_spl),
% 0.09/0.57 inference(component_clause,[status(thm)],[f626])).
% 0.09/0.57 fof(f629,plain,(
% 0.09/0.57 sQ27_spl|~sQ22_spl|sQ4_spl),
% 0.09/0.57 inference(split_clause,[status(thm)],[f624,f626,f572,f488])).
% 0.09/0.57 fof(f637,plain,(
% 0.09/0.57 $false|~sQ1_spl),
% 0.09/0.57 inference(forward_subsumption_resolution,[status(thm)],[f480,f96])).
% 0.09/0.57 fof(f638,plain,(
% 0.09/0.57 ~sQ1_spl),
% 0.09/0.57 inference(contradiction_clause,[status(thm)],[f637])).
% 0.14/0.58 fof(f639,plain,(
% 0.14/0.58 $false|sQ0_spl),
% 0.14/0.58 inference(forward_subsumption_resolution,[status(thm)],[f478,f95])).
% 0.14/0.58 fof(f640,plain,(
% 0.14/0.58 sQ0_spl),
% 0.14/0.58 inference(contradiction_clause,[status(thm)],[f639])).
% 0.14/0.58 fof(f641,plain,(
% 0.14/0.58 $false|~sQ27_spl),
% 0.14/0.58 inference(forward_subsumption_resolution,[status(thm)],[f627,f453])).
% 0.14/0.58 fof(f642,plain,(
% 0.14/0.58 ~sQ27_spl),
% 0.14/0.58 inference(contradiction_clause,[status(thm)],[f641])).
% 0.14/0.58 fof(f643,plain,(
% 0.14/0.58 ~xsd_string(sK15_skl)|~sQ3_spl),
% 0.14/0.58 inference(resolution,[status(thm)],[f486,f99])).
% 0.14/0.58 fof(f644,plain,(
% 0.14/0.58 $false|~sQ2_spl|~sQ3_spl),
% 0.14/0.58 inference(forward_subsumption_resolution,[status(thm)],[f643,f483])).
% 0.14/0.58 fof(f645,plain,(
% 0.14/0.58 ~sQ2_spl|~sQ3_spl),
% 0.14/0.58 inference(contradiction_clause,[status(thm)],[f644])).
% 0.14/0.58 fof(f646,plain,(
% 0.14/0.58 xsd_string(sK15_skl)|sQ3_spl),
% 0.14/0.58 inference(resolution,[status(thm)],[f487,f100])).
% 0.14/0.58 fof(f647,plain,(
% 0.14/0.58 sQ2_spl|sQ3_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f646,f482,f485])).
% 0.14/0.58 fof(f648,plain,(
% 0.14/0.58 $false|sQ14_spl),
% 0.14/0.58 inference(forward_subsumption_resolution,[status(thm)],[f525,f451])).
% 0.14/0.58 fof(f649,plain,(
% 0.14/0.58 sQ14_spl),
% 0.14/0.58 inference(contradiction_clause,[status(thm)],[f648])).
% 0.14/0.58 fof(f650,plain,(
% 0.14/0.58 $false|~sQ26_spl),
% 0.14/0.58 inference(forward_subsumption_resolution,[status(thm)],[f615,f447])).
% 0.14/0.58 fof(f651,plain,(
% 0.14/0.58 ~sQ26_spl),
% 0.14/0.58 inference(contradiction_clause,[status(thm)],[f650])).
% 0.14/0.58 fof(f652,plain,(
% 0.14/0.58 $false),
% 0.14/0.58 inference(sat_refutation,[status(thm)],[f515,f516,f530,f534,f541,f556,f570,f575,f577,f582,f586,f593,f596,f598,f600,f617,f619,f629,f638,f640,f642,f645,f647,f649,f651])).
% 0.14/0.58 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.60 % Elapsed time: 0.055254 seconds
% 0.14/0.60 % CPU time: 0.139553 seconds
% 0.14/0.60 % Total memory used: 24.667 MB
% 0.14/0.60 % Net memory used: 24.523 MB
%------------------------------------------------------------------------------