%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS154+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 : n005.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.14s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS154+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.09/0.36 % Computer : n005.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 22:55:18 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 0.14/0.39 % Refutation found
% 0.14/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.39 fof(f1,axiom,(
% 0.14/0.39 (! [X] :( cowlThing(X)& ~ cowlNothing(X) ) )),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f2,axiom,(
% 0.14/0.39 (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ) )),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f11,axiom,(
% 0.14/0.39 (! [X] :( cC104(X)<=> ( cC4(X)& cC34(X) ) ) )),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f16,axiom,(
% 0.14/0.39 (! [X] :( cC110(X)<=> ( cC102xcomp(X)& cC108xcomp(X) ) ) )),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f22,axiom,(
% 0.14/0.39 (! [X] :( cC114(X)<=> ( cC112xcomp(X)& cC96xcomp(X) ) ) )),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f23,axiom,(
% 0.14/0.39 (! [X] :( cC116(X)<=> ( cC114(X)& cC80(X) ) ) )),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f24,axiom,(
% 0.14/0.39 (! [X] :( cC118(X)<=> ( cC4(X)& cC10xcomp(X) ) ) )),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f28,axiom,(
% 0.14/0.39 (! [X] :( cC120(X)<=> ( cC118(X)& cC34(X) ) ) )),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f43,axiom,(
% 0.14/0.39 (! [X] :( cC136(X)<=> ( cC134xcomp(X)& cC116(X) ) ) )),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f61,axiom,(
% 0.14/0.39 (! [X] :( cC24(X)<=> ( cC16(X)& cC2(X) ) ) )),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f94,axiom,(
% 0.14/0.39 (! [X] :( cC56(X)<=> ( cC4(X)& cC10xcomp(X) ) ) )),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f95,axiom,(
% 0.14/0.39 (! [X] :( cC58(X)<=> ( cC34(X)& cC56(X) ) ) )),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f118,axiom,(
% 0.14/0.39 (! [X] :( cC80(X)<=> ( cC78xcomp(X)& cC76xcomp(X) ) ) )),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f128,axiom,(
% 0.14/0.39 (! [X] :( cC88(X)<=> ( cC16(X)& cC2(X) ) ) )),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f137,axiom,(
% 0.14/0.39 (! [X] :( cC94(X)<=> ( cC86xcomp(X)& cC92xcomp(X) ) ) )),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f147,axiom,(
% 0.14/0.39 cC16(iV822576) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f148,axiom,(
% 0.14/0.39 cC102xcomp(iV822576) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f149,axiom,(
% 0.14/0.39 cC108xcomp(iV822576) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f150,axiom,(
% 0.14/0.39 cC4(iV822576) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f152,axiom,(
% 0.14/0.39 cC112xcomp(iV822576) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f153,axiom,(
% 0.14/0.39 cC76xcomp(iV822576) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f154,axiom,(
% 0.14/0.39 cC96xcomp(iV822576) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f159,axiom,(
% 0.14/0.39 cC78xcomp(iV822576) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f161,axiom,(
% 0.14/0.39 cC134xcomp(iV822576) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f162,axiom,(
% 0.14/0.39 cC86xcomp(iV822576) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f163,axiom,(
% 0.14/0.39 cC34(iV822576) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f166,axiom,(
% 0.14/0.39 cC2(iV822576) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f168,axiom,(
% 0.14/0.39 cC10xcomp(iV822576) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f169,axiom,(
% 0.14/0.39 cC92xcomp(iV822576) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f170,conjecture,(
% 0.14/0.39 ( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& cC58(iV822576)& cC116(iV822576)& cC114(iV822576)& cowlThing(iV822576)& cC94(iV822576)& cC80(iV822576)& cC110(iV822576)& cC136(iV822576)& cC56(iV822576) ) ),
% 0.14/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f171,negated_conjecture,(
% 0.14/0.39 ~(( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& cC58(iV822576)& cC116(iV822576)& cC114(iV822576)& cowlThing(iV822576)& cC94(iV822576)& cC80(iV822576)& cC110(iV822576)& cC136(iV822576)& cC56(iV822576) ) )),
% 0.14/0.39 inference(negated_conjecture,[status(cth)],[f170])).
% 0.14/0.39 fof(f172,plain,(
% 0.14/0.39 (![X]: cowlThing(X))&(![X]: ~cowlNothing(X))),
% 0.14/0.39 inference(miniscoping,[status(thm)],[f1])).
% 0.14/0.39 fof(f173,plain,(
% 0.14/0.39 ![X0]: (cowlThing(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f172])).
% 0.14/0.39 fof(f174,plain,(
% 0.14/0.39 ![X0]: (~cowlNothing(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f172])).
% 0.14/0.39 fof(f175,plain,(
% 0.14/0.39 ![X]: ((~xsd_string(X)|~xsd_integer(X))&(xsd_string(X)|xsd_integer(X)))),
% 0.14/0.39 inference(NNF_transformation,[status(thm)],[f2])).
% 0.14/0.39 fof(f176,plain,(
% 0.14/0.39 (![X]: (~xsd_string(X)|~xsd_integer(X)))&(![X]: (xsd_string(X)|xsd_integer(X)))),
% 0.14/0.39 inference(miniscoping,[status(thm)],[f175])).
% 0.14/0.39 fof(f177,plain,(
% 0.14/0.39 ![X0]: (~xsd_string(X0)|~xsd_integer(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f176])).
% 0.14/0.39 fof(f178,plain,(
% 0.14/0.39 ![X0]: (xsd_string(X0)|xsd_integer(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f176])).
% 0.14/0.39 fof(f223,plain,(
% 0.14/0.39 ![X]: ((~cC104(X)|(cC4(X)&cC34(X)))&(cC104(X)|(~cC4(X)|~cC34(X))))),
% 0.14/0.39 inference(NNF_transformation,[status(thm)],[f11])).
% 0.14/0.39 fof(f224,plain,(
% 0.14/0.39 (![X]: (~cC104(X)|(cC4(X)&cC34(X))))&(![X]: (cC104(X)|(~cC4(X)|~cC34(X))))),
% 0.14/0.39 inference(miniscoping,[status(thm)],[f223])).
% 0.14/0.39 fof(f227,plain,(
% 0.14/0.39 ![X0]: (cC104(X0)|~cC4(X0)|~cC34(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f224])).
% 0.14/0.39 fof(f250,plain,(
% 0.14/0.39 ![X]: ((~cC110(X)|(cC102xcomp(X)&cC108xcomp(X)))&(cC110(X)|(~cC102xcomp(X)|~cC108xcomp(X))))),
% 0.14/0.39 inference(NNF_transformation,[status(thm)],[f16])).
% 0.14/0.39 fof(f251,plain,(
% 0.14/0.39 (![X]: (~cC110(X)|(cC102xcomp(X)&cC108xcomp(X))))&(![X]: (cC110(X)|(~cC102xcomp(X)|~cC108xcomp(X))))),
% 0.14/0.39 inference(miniscoping,[status(thm)],[f250])).
% 0.14/0.39 fof(f254,plain,(
% 0.14/0.39 ![X0]: (cC110(X0)|~cC102xcomp(X0)|~cC108xcomp(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f251])).
% 0.14/0.39 fof(f282,plain,(
% 0.14/0.39 ![X]: ((~cC114(X)|(cC112xcomp(X)&cC96xcomp(X)))&(cC114(X)|(~cC112xcomp(X)|~cC96xcomp(X))))),
% 0.14/0.39 inference(NNF_transformation,[status(thm)],[f22])).
% 0.14/0.39 fof(f283,plain,(
% 0.14/0.39 (![X]: (~cC114(X)|(cC112xcomp(X)&cC96xcomp(X))))&(![X]: (cC114(X)|(~cC112xcomp(X)|~cC96xcomp(X))))),
% 0.14/0.39 inference(miniscoping,[status(thm)],[f282])).
% 0.14/0.39 fof(f286,plain,(
% 0.14/0.39 ![X0]: (cC114(X0)|~cC112xcomp(X0)|~cC96xcomp(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f283])).
% 0.14/0.39 fof(f287,plain,(
% 0.14/0.39 ![X]: ((~cC116(X)|(cC114(X)&cC80(X)))&(cC116(X)|(~cC114(X)|~cC80(X))))),
% 0.14/0.39 inference(NNF_transformation,[status(thm)],[f23])).
% 0.14/0.39 fof(f288,plain,(
% 0.14/0.39 (![X]: (~cC116(X)|(cC114(X)&cC80(X))))&(![X]: (cC116(X)|(~cC114(X)|~cC80(X))))),
% 0.14/0.39 inference(miniscoping,[status(thm)],[f287])).
% 0.14/0.39 fof(f291,plain,(
% 0.14/0.39 ![X0]: (cC116(X0)|~cC114(X0)|~cC80(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f288])).
% 0.14/0.39 fof(f292,plain,(
% 0.14/0.39 ![X]: ((~cC118(X)|(cC4(X)&cC10xcomp(X)))&(cC118(X)|(~cC4(X)|~cC10xcomp(X))))),
% 0.14/0.39 inference(NNF_transformation,[status(thm)],[f24])).
% 0.14/0.39 fof(f293,plain,(
% 0.14/0.39 (![X]: (~cC118(X)|(cC4(X)&cC10xcomp(X))))&(![X]: (cC118(X)|(~cC4(X)|~cC10xcomp(X))))),
% 0.14/0.39 inference(miniscoping,[status(thm)],[f292])).
% 0.14/0.39 fof(f296,plain,(
% 0.14/0.39 ![X0]: (cC118(X0)|~cC4(X0)|~cC10xcomp(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f293])).
% 0.14/0.39 fof(f313,plain,(
% 0.14/0.39 ![X]: ((~cC120(X)|(cC118(X)&cC34(X)))&(cC120(X)|(~cC118(X)|~cC34(X))))),
% 0.14/0.39 inference(NNF_transformation,[status(thm)],[f28])).
% 0.14/0.39 fof(f314,plain,(
% 0.14/0.39 (![X]: (~cC120(X)|(cC118(X)&cC34(X))))&(![X]: (cC120(X)|(~cC118(X)|~cC34(X))))),
% 0.14/0.39 inference(miniscoping,[status(thm)],[f313])).
% 0.14/0.39 fof(f317,plain,(
% 0.14/0.39 ![X0]: (cC120(X0)|~cC118(X0)|~cC34(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f314])).
% 0.14/0.39 fof(f394,plain,(
% 0.14/0.39 ![X]: ((~cC136(X)|(cC134xcomp(X)&cC116(X)))&(cC136(X)|(~cC134xcomp(X)|~cC116(X))))),
% 0.14/0.39 inference(NNF_transformation,[status(thm)],[f43])).
% 0.14/0.39 fof(f395,plain,(
% 0.14/0.39 (![X]: (~cC136(X)|(cC134xcomp(X)&cC116(X))))&(![X]: (cC136(X)|(~cC134xcomp(X)|~cC116(X))))),
% 0.14/0.39 inference(miniscoping,[status(thm)],[f394])).
% 0.14/0.39 fof(f398,plain,(
% 0.14/0.39 ![X0]: (cC136(X0)|~cC134xcomp(X0)|~cC116(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f395])).
% 0.14/0.39 fof(f491,plain,(
% 0.14/0.39 ![X]: ((~cC24(X)|(cC16(X)&cC2(X)))&(cC24(X)|(~cC16(X)|~cC2(X))))),
% 0.14/0.39 inference(NNF_transformation,[status(thm)],[f61])).
% 0.14/0.39 fof(f492,plain,(
% 0.14/0.39 (![X]: (~cC24(X)|(cC16(X)&cC2(X))))&(![X]: (cC24(X)|(~cC16(X)|~cC2(X))))),
% 0.14/0.39 inference(miniscoping,[status(thm)],[f491])).
% 0.14/0.39 fof(f495,plain,(
% 0.14/0.39 ![X0]: (cC24(X0)|~cC16(X0)|~cC2(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f492])).
% 0.14/0.39 fof(f668,plain,(
% 0.14/0.39 ![X]: ((~cC56(X)|(cC4(X)&cC10xcomp(X)))&(cC56(X)|(~cC4(X)|~cC10xcomp(X))))),
% 0.14/0.39 inference(NNF_transformation,[status(thm)],[f94])).
% 0.14/0.39 fof(f669,plain,(
% 0.14/0.39 (![X]: (~cC56(X)|(cC4(X)&cC10xcomp(X))))&(![X]: (cC56(X)|(~cC4(X)|~cC10xcomp(X))))),
% 0.14/0.39 inference(miniscoping,[status(thm)],[f668])).
% 0.14/0.39 fof(f672,plain,(
% 0.14/0.39 ![X0]: (cC56(X0)|~cC4(X0)|~cC10xcomp(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f669])).
% 0.14/0.39 fof(f673,plain,(
% 0.14/0.39 ![X]: ((~cC58(X)|(cC34(X)&cC56(X)))&(cC58(X)|(~cC34(X)|~cC56(X))))),
% 0.14/0.39 inference(NNF_transformation,[status(thm)],[f95])).
% 0.14/0.39 fof(f674,plain,(
% 0.14/0.39 (![X]: (~cC58(X)|(cC34(X)&cC56(X))))&(![X]: (cC58(X)|(~cC34(X)|~cC56(X))))),
% 0.14/0.39 inference(miniscoping,[status(thm)],[f673])).
% 0.14/0.39 fof(f677,plain,(
% 0.14/0.39 ![X0]: (cC58(X0)|~cC34(X0)|~cC56(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f674])).
% 0.14/0.39 fof(f795,plain,(
% 0.14/0.39 ![X]: ((~cC80(X)|(cC78xcomp(X)&cC76xcomp(X)))&(cC80(X)|(~cC78xcomp(X)|~cC76xcomp(X))))),
% 0.14/0.39 inference(NNF_transformation,[status(thm)],[f118])).
% 0.14/0.39 fof(f796,plain,(
% 0.14/0.39 (![X]: (~cC80(X)|(cC78xcomp(X)&cC76xcomp(X))))&(![X]: (cC80(X)|(~cC78xcomp(X)|~cC76xcomp(X))))),
% 0.14/0.39 inference(miniscoping,[status(thm)],[f795])).
% 0.14/0.39 fof(f799,plain,(
% 0.14/0.39 ![X0]: (cC80(X0)|~cC78xcomp(X0)|~cC76xcomp(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f796])).
% 0.14/0.39 fof(f849,plain,(
% 0.14/0.39 ![X]: ((~cC88(X)|(cC16(X)&cC2(X)))&(cC88(X)|(~cC16(X)|~cC2(X))))),
% 0.14/0.39 inference(NNF_transformation,[status(thm)],[f128])).
% 0.14/0.39 fof(f850,plain,(
% 0.14/0.39 (![X]: (~cC88(X)|(cC16(X)&cC2(X))))&(![X]: (cC88(X)|(~cC16(X)|~cC2(X))))),
% 0.14/0.39 inference(miniscoping,[status(thm)],[f849])).
% 0.14/0.39 fof(f853,plain,(
% 0.14/0.39 ![X0]: (cC88(X0)|~cC16(X0)|~cC2(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f850])).
% 0.14/0.39 fof(f898,plain,(
% 0.14/0.39 ![X]: ((~cC94(X)|(cC86xcomp(X)&cC92xcomp(X)))&(cC94(X)|(~cC86xcomp(X)|~cC92xcomp(X))))),
% 0.14/0.39 inference(NNF_transformation,[status(thm)],[f137])).
% 0.14/0.39 fof(f899,plain,(
% 0.14/0.39 (![X]: (~cC94(X)|(cC86xcomp(X)&cC92xcomp(X))))&(![X]: (cC94(X)|(~cC86xcomp(X)|~cC92xcomp(X))))),
% 0.14/0.39 inference(miniscoping,[status(thm)],[f898])).
% 0.14/0.39 fof(f902,plain,(
% 0.14/0.39 ![X0]: (cC94(X0)|~cC86xcomp(X0)|~cC92xcomp(X0))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f899])).
% 0.14/0.39 fof(f951,plain,(
% 0.14/0.39 cC16(iV822576)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f147])).
% 0.14/0.39 fof(f952,plain,(
% 0.14/0.39 cC102xcomp(iV822576)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f148])).
% 0.14/0.39 fof(f953,plain,(
% 0.14/0.39 cC108xcomp(iV822576)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f149])).
% 0.14/0.39 fof(f954,plain,(
% 0.14/0.39 cC4(iV822576)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f150])).
% 0.14/0.39 fof(f956,plain,(
% 0.14/0.39 cC112xcomp(iV822576)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f152])).
% 0.14/0.39 fof(f957,plain,(
% 0.14/0.39 cC76xcomp(iV822576)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f153])).
% 0.14/0.39 fof(f958,plain,(
% 0.14/0.39 cC96xcomp(iV822576)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f154])).
% 0.14/0.39 fof(f964,plain,(
% 0.14/0.39 cC78xcomp(iV822576)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f159])).
% 0.14/0.39 fof(f967,plain,(
% 0.14/0.39 cC134xcomp(iV822576)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f161])).
% 0.14/0.39 fof(f968,plain,(
% 0.14/0.39 cC86xcomp(iV822576)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f162])).
% 0.14/0.39 fof(f969,plain,(
% 0.14/0.39 cC34(iV822576)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f163])).
% 0.14/0.39 fof(f973,plain,(
% 0.14/0.39 cC2(iV822576)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f166])).
% 0.14/0.39 fof(f975,plain,(
% 0.14/0.39 cC10xcomp(iV822576)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f168])).
% 0.14/0.39 fof(f976,plain,(
% 0.14/0.39 cC92xcomp(iV822576)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f169])).
% 0.14/0.39 fof(f977,plain,(
% 0.14/0.39 (((((((((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: (xsd_string(X)<~>~xsd_integer(X))))|~cC58(iV822576))|~cC116(iV822576))|~cC114(iV822576))|~cowlThing(iV822576))|~cC94(iV822576))|~cC80(iV822576))|~cC110(iV822576))|~cC136(iV822576))|~cC56(iV822576))),
% 0.14/0.39 inference(pre_NNF_transformation,[status(thm)],[f171])).
% 0.14/0.39 fof(f978,plain,(
% 0.14/0.39 ((((((((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: ((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))|~cC58(iV822576))|~cC116(iV822576))|~cC114(iV822576))|~cowlThing(iV822576))|~cC94(iV822576))|~cC80(iV822576))|~cC110(iV822576))|~cC136(iV822576))|~cC56(iV822576)),
% 0.14/0.39 inference(NNF_transformation,[status(thm)],[f977])).
% 0.14/0.39 fof(f979,plain,(
% 0.14/0.39 (((((((((((?[X]: ~cowlThing(X))|(?[X]: cowlNothing(X)))|(?[X]: ((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))|~cC58(iV822576))|~cC116(iV822576))|~cC114(iV822576))|~cowlThing(iV822576))|~cC94(iV822576))|~cC80(iV822576))|~cC110(iV822576))|~cC136(iV822576))|~cC56(iV822576)),
% 0.14/0.39 inference(miniscoping,[status(thm)],[f978])).
% 0.14/0.39 fof(f980,plain,(
% 0.14/0.39 ((((((((((~cowlThing(sK91_skl)|cowlNothing(sK92_skl))|((xsd_string(sK93_skl)|~xsd_integer(sK93_skl))&(~xsd_string(sK93_skl)|xsd_integer(sK93_skl))))|~cC58(iV822576))|~cC116(iV822576))|~cC114(iV822576))|~cowlThing(iV822576))|~cC94(iV822576))|~cC80(iV822576))|~cC110(iV822576))|~cC136(iV822576))|~cC56(iV822576)),
% 0.14/0.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK91_skl,sK92_skl,sK93_skl]),skolemize(X,sK91_skl),skolemize(X,sK92_skl),skolemize(X,sK93_skl)],[f979])).
% 0.14/0.39 fof(f981,plain,(
% 0.14/0.39 ~cowlThing(sK91_skl)|cowlNothing(sK92_skl)|xsd_string(sK93_skl)|~xsd_integer(sK93_skl)|~cC58(iV822576)|~cC116(iV822576)|~cC114(iV822576)|~cowlThing(iV822576)|~cC94(iV822576)|~cC80(iV822576)|~cC110(iV822576)|~cC136(iV822576)|~cC56(iV822576)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f980])).
% 0.14/0.39 fof(f982,plain,(
% 0.14/0.39 ~cowlThing(sK91_skl)|cowlNothing(sK92_skl)|~xsd_string(sK93_skl)|xsd_integer(sK93_skl)|~cC58(iV822576)|~cC116(iV822576)|~cC114(iV822576)|~cowlThing(iV822576)|~cC94(iV822576)|~cC80(iV822576)|~cC110(iV822576)|~cC136(iV822576)|~cC56(iV822576)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f980])).
% 0.14/0.39 fof(f983,definition,(
% 0.14/0.39 sQ0_spl <=> (cowlThing(sK91_skl))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f985,plain,(
% 0.14/0.39 ~cowlThing(sK91_skl)|sQ0_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f983])).
% 0.14/0.39 fof(f986,definition,(
% 0.14/0.39 sQ1_spl <=> (cowlNothing(sK92_skl))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f987,plain,(
% 0.14/0.39 cowlNothing(sK92_skl)|~sQ1_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f986])).
% 0.14/0.39 fof(f989,definition,(
% 0.14/0.39 sQ2_spl <=> (xsd_string(sK93_skl))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f990,plain,(
% 0.14/0.39 xsd_string(sK93_skl)|~sQ2_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f989])).
% 0.14/0.39 fof(f992,definition,(
% 0.14/0.39 sQ3_spl <=> (xsd_integer(sK93_skl))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f993,plain,(
% 0.14/0.39 xsd_integer(sK93_skl)|~sQ3_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f992])).
% 0.14/0.39 fof(f994,plain,(
% 0.14/0.39 ~xsd_integer(sK93_skl)|sQ3_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f992])).
% 0.14/0.39 fof(f995,definition,(
% 0.14/0.39 sQ4_spl <=> (cC58(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f998,definition,(
% 0.14/0.39 sQ5_spl <=> (cC116(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f999,plain,(
% 0.14/0.39 cC116(iV822576)|~sQ5_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f998])).
% 0.14/0.39 fof(f1001,definition,(
% 0.14/0.39 sQ6_spl <=> (cC114(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1002,plain,(
% 0.14/0.39 cC114(iV822576)|~sQ6_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f1001])).
% 0.14/0.39 fof(f1004,definition,(
% 0.14/0.39 sQ7_spl <=> (cowlThing(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1006,plain,(
% 0.14/0.39 ~cowlThing(iV822576)|sQ7_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f1004])).
% 0.14/0.39 fof(f1007,definition,(
% 0.14/0.39 sQ8_spl <=> (cC94(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1010,definition,(
% 0.14/0.39 sQ9_spl <=> (cC80(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1013,definition,(
% 0.14/0.39 sQ10_spl <=> (cC110(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1016,definition,(
% 0.14/0.39 sQ11_spl <=> (cC136(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1019,definition,(
% 0.14/0.39 sQ12_spl <=> (cC56(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1020,plain,(
% 0.14/0.39 cC56(iV822576)|~sQ12_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f1019])).
% 0.14/0.39 fof(f1022,plain,(
% 0.14/0.39 ~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.14/0.39 inference(split_clause,[status(thm)],[f981,f983,f986,f989,f992,f995,f998,f1001,f1004,f1007,f1010,f1013,f1016,f1019])).
% 0.14/0.39 fof(f1023,plain,(
% 0.14/0.39 ~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.14/0.39 inference(split_clause,[status(thm)],[f982,f983,f986,f989,f992,f995,f998,f1001,f1004,f1007,f1010,f1013,f1016,f1019])).
% 0.14/0.39 fof(f1026,plain,(
% 0.14/0.39 cC56(iV822576)|~cC4(iV822576)),
% 0.14/0.39 inference(resolution,[status(thm)],[f975,f672])).
% 0.14/0.39 fof(f1028,definition,(
% 0.14/0.39 sQ13_spl <=> (cC4(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1030,plain,(
% 0.14/0.39 ~cC4(iV822576)|sQ13_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f1028])).
% 0.14/0.39 fof(f1031,plain,(
% 0.14/0.39 sQ12_spl|~sQ13_spl),
% 0.14/0.39 inference(split_clause,[status(thm)],[f1026,f1019,f1028])).
% 0.14/0.39 fof(f1032,plain,(
% 0.14/0.39 cC58(iV822576)|~cC34(iV822576)|~sQ12_spl),
% 0.14/0.39 inference(resolution,[status(thm)],[f1020,f677])).
% 0.14/0.39 fof(f1035,definition,(
% 0.14/0.39 sQ14_spl <=> (cC34(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1037,plain,(
% 0.14/0.39 ~cC34(iV822576)|sQ14_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f1035])).
% 0.14/0.39 fof(f1038,plain,(
% 0.14/0.39 sQ4_spl|~sQ14_spl|~sQ12_spl),
% 0.14/0.39 inference(split_clause,[status(thm)],[f1032,f995,f1035,f1019])).
% 0.14/0.39 fof(f1045,plain,(
% 0.14/0.39 cC104(iV822576)|~cC34(iV822576)),
% 0.14/0.39 inference(resolution,[status(thm)],[f227,f954])).
% 0.14/0.39 fof(f1047,definition,(
% 0.14/0.39 sQ15_spl <=> (cC104(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1050,plain,(
% 0.14/0.39 sQ15_spl|~sQ14_spl),
% 0.14/0.39 inference(split_clause,[status(thm)],[f1045,f1047,f1035])).
% 0.14/0.39 fof(f1051,plain,(
% 0.14/0.39 $false|sQ14_spl),
% 0.14/0.39 inference(forward_subsumption_resolution,[status(thm)],[f1037,f969])).
% 0.14/0.39 fof(f1052,plain,(
% 0.14/0.39 sQ14_spl),
% 0.14/0.39 inference(contradiction_clause,[status(thm)],[f1051])).
% 0.14/0.39 fof(f1053,plain,(
% 0.14/0.39 $false|sQ13_spl),
% 0.14/0.39 inference(forward_subsumption_resolution,[status(thm)],[f1030,f954])).
% 0.14/0.39 fof(f1054,plain,(
% 0.14/0.39 sQ13_spl),
% 0.14/0.39 inference(contradiction_clause,[status(thm)],[f1053])).
% 0.14/0.39 fof(f1064,plain,(
% 0.14/0.39 cC110(iV822576)|~cC102xcomp(iV822576)),
% 0.14/0.39 inference(resolution,[status(thm)],[f254,f953])).
% 0.14/0.39 fof(f1065,definition,(
% 0.14/0.39 sQ16_spl <=> (cC102xcomp(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1067,plain,(
% 0.14/0.39 ~cC102xcomp(iV822576)|sQ16_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f1065])).
% 0.14/0.39 fof(f1068,plain,(
% 0.14/0.39 sQ10_spl|~sQ16_spl),
% 0.14/0.39 inference(split_clause,[status(thm)],[f1064,f1013,f1065])).
% 0.14/0.39 fof(f1076,plain,(
% 0.14/0.39 cC114(iV822576)|~cC96xcomp(iV822576)),
% 0.14/0.39 inference(resolution,[status(thm)],[f286,f956])).
% 0.14/0.39 fof(f1077,definition,(
% 0.14/0.39 sQ17_spl <=> (cC96xcomp(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1079,plain,(
% 0.14/0.39 ~cC96xcomp(iV822576)|sQ17_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f1077])).
% 0.14/0.39 fof(f1080,plain,(
% 0.14/0.39 sQ6_spl|~sQ17_spl),
% 0.14/0.39 inference(split_clause,[status(thm)],[f1076,f1001,f1077])).
% 0.14/0.39 fof(f1081,plain,(
% 0.14/0.39 cC118(iV822576)|~cC4(iV822576)),
% 0.14/0.39 inference(resolution,[status(thm)],[f296,f975])).
% 0.14/0.39 fof(f1082,definition,(
% 0.14/0.39 sQ18_spl <=> (cC118(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1083,plain,(
% 0.14/0.39 cC118(iV822576)|~sQ18_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f1082])).
% 0.14/0.39 fof(f1085,plain,(
% 0.14/0.39 sQ18_spl|~sQ13_spl),
% 0.14/0.39 inference(split_clause,[status(thm)],[f1081,f1082,f1028])).
% 0.14/0.39 fof(f1087,plain,(
% 0.14/0.39 cC116(iV822576)|~cC80(iV822576)|~sQ6_spl),
% 0.14/0.39 inference(resolution,[status(thm)],[f1002,f291])).
% 0.14/0.39 fof(f1088,plain,(
% 0.14/0.39 sQ5_spl|~sQ9_spl|~sQ6_spl),
% 0.14/0.39 inference(split_clause,[status(thm)],[f1087,f998,f1010,f1001])).
% 0.14/0.39 fof(f1097,plain,(
% 0.14/0.39 cC120(iV822576)|~cC34(iV822576)|~sQ18_spl),
% 0.14/0.39 inference(resolution,[status(thm)],[f317,f1083])).
% 0.14/0.39 fof(f1098,definition,(
% 0.14/0.39 sQ19_spl <=> (cC120(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1101,plain,(
% 0.14/0.39 sQ19_spl|~sQ14_spl|~sQ18_spl),
% 0.14/0.39 inference(split_clause,[status(thm)],[f1097,f1098,f1035,f1082])).
% 0.14/0.39 fof(f1142,plain,(
% 0.14/0.39 cC24(iV822576)|~cC2(iV822576)),
% 0.14/0.39 inference(resolution,[status(thm)],[f495,f951])).
% 0.14/0.39 fof(f1143,definition,(
% 0.14/0.39 sQ20_spl <=> (cC24(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1146,definition,(
% 0.14/0.39 sQ21_spl <=> (cC2(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1148,plain,(
% 0.14/0.39 ~cC2(iV822576)|sQ21_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f1146])).
% 0.14/0.39 fof(f1149,plain,(
% 0.14/0.39 sQ20_spl|~sQ21_spl),
% 0.14/0.39 inference(split_clause,[status(thm)],[f1142,f1143,f1146])).
% 0.14/0.39 fof(f1215,plain,(
% 0.14/0.39 cC80(iV822576)|~cC76xcomp(iV822576)),
% 0.14/0.39 inference(resolution,[status(thm)],[f799,f964])).
% 0.14/0.39 fof(f1218,definition,(
% 0.14/0.39 sQ22_spl <=> (cC76xcomp(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1220,plain,(
% 0.14/0.39 ~cC76xcomp(iV822576)|sQ22_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f1218])).
% 0.14/0.39 fof(f1221,plain,(
% 0.14/0.39 sQ9_spl|~sQ22_spl),
% 0.14/0.39 inference(split_clause,[status(thm)],[f1215,f1010,f1218])).
% 0.14/0.39 fof(f1222,plain,(
% 0.14/0.39 $false|sQ17_spl),
% 0.14/0.39 inference(forward_subsumption_resolution,[status(thm)],[f1079,f958])).
% 0.14/0.39 fof(f1223,plain,(
% 0.14/0.39 sQ17_spl),
% 0.14/0.39 inference(contradiction_clause,[status(thm)],[f1222])).
% 0.14/0.39 fof(f1224,plain,(
% 0.14/0.39 $false|sQ22_spl),
% 0.14/0.39 inference(forward_subsumption_resolution,[status(thm)],[f1220,f957])).
% 0.14/0.39 fof(f1225,plain,(
% 0.14/0.39 sQ22_spl),
% 0.14/0.39 inference(contradiction_clause,[status(thm)],[f1224])).
% 0.14/0.39 fof(f1230,plain,(
% 0.14/0.39 cC136(iV822576)|~cC134xcomp(iV822576)|~sQ5_spl),
% 0.14/0.39 inference(resolution,[status(thm)],[f999,f398])).
% 0.14/0.39 fof(f1232,definition,(
% 0.14/0.39 sQ23_spl <=> (cC134xcomp(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1234,plain,(
% 0.14/0.39 ~cC134xcomp(iV822576)|sQ23_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f1232])).
% 0.14/0.39 fof(f1235,plain,(
% 0.14/0.39 sQ11_spl|~sQ23_spl|~sQ5_spl),
% 0.14/0.39 inference(split_clause,[status(thm)],[f1230,f1016,f1232,f998])).
% 0.14/0.39 fof(f1247,plain,(
% 0.14/0.39 cC88(iV822576)|~cC2(iV822576)),
% 0.14/0.39 inference(resolution,[status(thm)],[f853,f951])).
% 0.14/0.39 fof(f1248,definition,(
% 0.14/0.39 sQ24_spl <=> (cC88(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1251,plain,(
% 0.14/0.39 sQ24_spl|~sQ21_spl),
% 0.14/0.39 inference(split_clause,[status(thm)],[f1247,f1248,f1146])).
% 0.14/0.39 fof(f1252,plain,(
% 0.14/0.39 $false|sQ21_spl),
% 0.14/0.39 inference(forward_subsumption_resolution,[status(thm)],[f1148,f973])).
% 0.14/0.39 fof(f1253,plain,(
% 0.14/0.39 sQ21_spl),
% 0.14/0.39 inference(contradiction_clause,[status(thm)],[f1252])).
% 0.14/0.39 fof(f1266,plain,(
% 0.14/0.39 cC94(iV822576)|~cC86xcomp(iV822576)),
% 0.14/0.39 inference(resolution,[status(thm)],[f902,f976])).
% 0.14/0.39 fof(f1267,definition,(
% 0.14/0.39 sQ25_spl <=> (cC86xcomp(iV822576))),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f1269,plain,(
% 0.14/0.39 ~cC86xcomp(iV822576)|sQ25_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f1267])).
% 0.14/0.39 fof(f1270,plain,(
% 0.14/0.39 sQ8_spl|~sQ25_spl),
% 0.14/0.39 inference(split_clause,[status(thm)],[f1266,f1007,f1267])).
% 0.14/0.39 fof(f1271,plain,(
% 0.14/0.39 $false|sQ7_spl),
% 0.14/0.39 inference(forward_subsumption_resolution,[status(thm)],[f1006,f173])).
% 0.14/0.39 fof(f1272,plain,(
% 0.14/0.39 sQ7_spl),
% 0.14/0.39 inference(contradiction_clause,[status(thm)],[f1271])).
% 0.14/0.39 fof(f1273,plain,(
% 0.14/0.39 $false|~sQ1_spl),
% 0.14/0.39 inference(forward_subsumption_resolution,[status(thm)],[f987,f174])).
% 0.14/0.39 fof(f1274,plain,(
% 0.14/0.39 ~sQ1_spl),
% 0.14/0.39 inference(contradiction_clause,[status(thm)],[f1273])).
% 0.14/0.39 fof(f1275,plain,(
% 0.14/0.39 $false|sQ0_spl),
% 0.14/0.39 inference(forward_subsumption_resolution,[status(thm)],[f985,f173])).
% 0.14/0.39 fof(f1276,plain,(
% 0.14/0.39 sQ0_spl),
% 0.14/0.39 inference(contradiction_clause,[status(thm)],[f1275])).
% 0.14/0.39 fof(f1279,plain,(
% 0.14/0.39 ~xsd_string(sK93_skl)|~sQ3_spl),
% 0.14/0.39 inference(resolution,[status(thm)],[f993,f177])).
% 0.14/0.39 fof(f1280,plain,(
% 0.14/0.39 $false|~sQ2_spl|~sQ3_spl),
% 0.14/0.39 inference(forward_subsumption_resolution,[status(thm)],[f1279,f990])).
% 0.14/0.39 fof(f1281,plain,(
% 0.14/0.39 ~sQ2_spl|~sQ3_spl),
% 0.14/0.39 inference(contradiction_clause,[status(thm)],[f1280])).
% 0.14/0.39 fof(f1282,plain,(
% 0.14/0.39 xsd_string(sK93_skl)|sQ3_spl),
% 0.14/0.39 inference(resolution,[status(thm)],[f994,f178])).
% 0.14/0.39 fof(f1283,plain,(
% 0.14/0.39 sQ2_spl|sQ3_spl),
% 0.14/0.39 inference(split_clause,[status(thm)],[f1282,f989,f992])).
% 0.14/0.39 fof(f1284,plain,(
% 0.14/0.39 $false|sQ25_spl),
% 0.14/0.39 inference(forward_subsumption_resolution,[status(thm)],[f1269,f968])).
% 0.14/0.39 fof(f1285,plain,(
% 0.14/0.39 sQ25_spl),
% 0.14/0.39 inference(contradiction_clause,[status(thm)],[f1284])).
% 0.14/0.39 fof(f1286,plain,(
% 0.14/0.39 $false|sQ16_spl),
% 0.14/0.39 inference(forward_subsumption_resolution,[status(thm)],[f1067,f952])).
% 0.14/0.39 fof(f1287,plain,(
% 0.14/0.39 sQ16_spl),
% 0.14/0.39 inference(contradiction_clause,[status(thm)],[f1286])).
% 0.14/0.39 fof(f1288,plain,(
% 0.14/0.39 $false|sQ23_spl),
% 0.14/0.39 inference(forward_subsumption_resolution,[status(thm)],[f1234,f967])).
% 0.14/0.39 fof(f1289,plain,(
% 0.14/0.39 sQ23_spl),
% 0.14/0.39 inference(contradiction_clause,[status(thm)],[f1288])).
% 0.14/0.39 fof(f1290,plain,(
% 0.14/0.39 $false),
% 0.14/0.39 inference(sat_refutation,[status(thm)],[f1022,f1023,f1031,f1038,f1050,f1052,f1054,f1068,f1080,f1085,f1088,f1101,f1149,f1221,f1223,f1225,f1235,f1251,f1253,f1270,f1272,f1274,f1276,f1281,f1283,f1285,f1287,f1289])).
% 0.14/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.41 % Elapsed time: 0.042293 seconds
% 0.14/0.41 % CPU time: 0.098309 seconds
% 0.14/0.41 % Total memory used: 8.934 MB
% 0.14/0.41 % Net memory used: 8.914 MB
%------------------------------------------------------------------------------