%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS148+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 : n016.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.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS148+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.35 % Computer : n016.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 22:59:23 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 0.12/0.37 % Refutation found
% 0.12/0.37 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.37 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.37 fof(f1,axiom,(
% 0.12/0.37 (! [X] :( cowlThing(X)& ~ cowlNothing(X) ) )),
% 0.12/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.37 fof(f2,axiom,(
% 0.12/0.37 (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ) )),
% 0.12/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.37 fof(f12,axiom,(
% 0.12/0.37 (! [X] :( cC116(X)<=> ( cTOP(X)& ~ cC114(X) ) ) )),
% 0.12/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.37 fof(f26,axiom,(
% 0.12/0.37 (! [X] :( cC140(X)<=> ( cTOP(X)& cC138(X) ) ) )),
% 0.12/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.37 fof(f72,axiom,(
% 0.12/0.37 (! [X] :( cTEST(X)<=> ( cC140(X)& cC116(X) ) ) )),
% 0.12/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.37 fof(f73,axiom,(
% 0.12/0.37 cTEST(iV5475) ),
% 0.12/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.37 fof(f74,axiom,(
% 0.12/0.37 cTOP(iV5475) ),
% 0.12/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.37 fof(f77,axiom,(
% 0.12/0.37 ~ cC114(iV5475) ),
% 0.12/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.37 fof(f90,conjecture,(
% 0.12/0.37 ( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& cC138(iV5475)& cowlThing(iV5475)& cC116(iV5475)& cC140(iV5475) ) ),
% 0.12/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.37 fof(f91,negated_conjecture,(
% 0.12/0.37 ~(( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& cC138(iV5475)& cowlThing(iV5475)& cC116(iV5475)& cC140(iV5475) ) )),
% 0.12/0.37 inference(negated_conjecture,[status(cth)],[f90])).
% 0.12/0.37 fof(f92,plain,(
% 0.12/0.37 (![X]: cowlThing(X))&(![X]: ~cowlNothing(X))),
% 0.12/0.37 inference(miniscoping,[status(thm)],[f1])).
% 0.12/0.37 fof(f93,plain,(
% 0.12/0.37 ![X0]: (cowlThing(X0))),
% 0.12/0.37 inference(cnf_transformation,[status(thm)],[f92])).
% 0.12/0.37 fof(f94,plain,(
% 0.12/0.37 ![X0]: (~cowlNothing(X0))),
% 0.12/0.37 inference(cnf_transformation,[status(thm)],[f92])).
% 0.12/0.37 fof(f95,plain,(
% 0.12/0.37 ![X]: ((~xsd_string(X)|~xsd_integer(X))&(xsd_string(X)|xsd_integer(X)))),
% 0.12/0.37 inference(NNF_transformation,[status(thm)],[f2])).
% 0.12/0.37 fof(f96,plain,(
% 0.12/0.37 (![X]: (~xsd_string(X)|~xsd_integer(X)))&(![X]: (xsd_string(X)|xsd_integer(X)))),
% 0.12/0.37 inference(miniscoping,[status(thm)],[f95])).
% 0.12/0.37 fof(f97,plain,(
% 0.12/0.37 ![X0]: (~xsd_string(X0)|~xsd_integer(X0))),
% 0.12/0.37 inference(cnf_transformation,[status(thm)],[f96])).
% 0.12/0.37 fof(f98,plain,(
% 0.12/0.37 ![X0]: (xsd_string(X0)|xsd_integer(X0))),
% 0.12/0.37 inference(cnf_transformation,[status(thm)],[f96])).
% 0.12/0.37 fof(f148,plain,(
% 0.12/0.37 ![X]: ((~cC116(X)|(cTOP(X)&~cC114(X)))&(cC116(X)|(~cTOP(X)|cC114(X))))),
% 0.12/0.37 inference(NNF_transformation,[status(thm)],[f12])).
% 0.12/0.37 fof(f149,plain,(
% 0.12/0.37 (![X]: (~cC116(X)|(cTOP(X)&~cC114(X))))&(![X]: (cC116(X)|(~cTOP(X)|cC114(X))))),
% 0.12/0.37 inference(miniscoping,[status(thm)],[f148])).
% 0.12/0.37 fof(f152,plain,(
% 0.12/0.37 ![X0]: (cC116(X0)|~cTOP(X0)|cC114(X0))),
% 0.12/0.37 inference(cnf_transformation,[status(thm)],[f149])).
% 0.12/0.37 fof(f227,plain,(
% 0.12/0.37 ![X]: ((~cC140(X)|(cTOP(X)&cC138(X)))&(cC140(X)|(~cTOP(X)|~cC138(X))))),
% 0.12/0.37 inference(NNF_transformation,[status(thm)],[f26])).
% 0.12/0.37 fof(f228,plain,(
% 0.12/0.37 (![X]: (~cC140(X)|(cTOP(X)&cC138(X))))&(![X]: (cC140(X)|(~cTOP(X)|~cC138(X))))),
% 0.12/0.37 inference(miniscoping,[status(thm)],[f227])).
% 0.12/0.37 fof(f230,plain,(
% 0.12/0.37 ![X0]: (~cC140(X0)|cC138(X0))),
% 0.12/0.37 inference(cnf_transformation,[status(thm)],[f228])).
% 0.12/0.37 fof(f482,plain,(
% 0.12/0.37 ![X]: ((~cTEST(X)|(cC140(X)&cC116(X)))&(cTEST(X)|(~cC140(X)|~cC116(X))))),
% 0.12/0.37 inference(NNF_transformation,[status(thm)],[f72])).
% 0.12/0.37 fof(f483,plain,(
% 0.12/0.37 (![X]: (~cTEST(X)|(cC140(X)&cC116(X))))&(![X]: (cTEST(X)|(~cC140(X)|~cC116(X))))),
% 0.12/0.37 inference(miniscoping,[status(thm)],[f482])).
% 0.12/0.37 fof(f484,plain,(
% 0.12/0.37 ![X0]: (~cTEST(X0)|cC140(X0))),
% 0.12/0.37 inference(cnf_transformation,[status(thm)],[f483])).
% 0.12/0.37 fof(f487,plain,(
% 0.12/0.37 cTEST(iV5475)),
% 0.12/0.37 inference(cnf_transformation,[status(thm)],[f73])).
% 0.12/0.37 fof(f488,plain,(
% 0.12/0.37 cTOP(iV5475)),
% 0.12/0.37 inference(cnf_transformation,[status(thm)],[f74])).
% 0.12/0.37 fof(f492,plain,(
% 0.12/0.37 ~cC114(iV5475)),
% 0.12/0.37 inference(cnf_transformation,[status(thm)],[f77])).
% 0.12/0.37 fof(f508,plain,(
% 0.12/0.37 ((((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: (xsd_string(X)<~>~xsd_integer(X))))|~cC138(iV5475))|~cowlThing(iV5475))|~cC116(iV5475))|~cC140(iV5475))),
% 0.12/0.37 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 0.12/0.38 fof(f509,plain,(
% 0.12/0.38 (((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: ((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))|~cC138(iV5475))|~cowlThing(iV5475))|~cC116(iV5475))|~cC140(iV5475)),
% 0.12/0.38 inference(NNF_transformation,[status(thm)],[f508])).
% 0.12/0.38 fof(f510,plain,(
% 0.12/0.38 ((((((?[X]: ~cowlThing(X))|(?[X]: cowlNothing(X)))|(?[X]: ((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))|~cC138(iV5475))|~cowlThing(iV5475))|~cC116(iV5475))|~cC140(iV5475)),
% 0.12/0.38 inference(miniscoping,[status(thm)],[f509])).
% 0.12/0.38 fof(f511,plain,(
% 0.12/0.38 (((((~cowlThing(sK38_skl)|cowlNothing(sK39_skl))|((xsd_string(sK40_skl)|~xsd_integer(sK40_skl))&(~xsd_string(sK40_skl)|xsd_integer(sK40_skl))))|~cC138(iV5475))|~cowlThing(iV5475))|~cC116(iV5475))|~cC140(iV5475)),
% 0.12/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK38_skl,sK39_skl,sK40_skl]),skolemize(X,sK38_skl),skolemize(X,sK39_skl),skolemize(X,sK40_skl)],[f510])).
% 0.12/0.38 fof(f512,plain,(
% 0.12/0.38 ~cowlThing(sK38_skl)|cowlNothing(sK39_skl)|xsd_string(sK40_skl)|~xsd_integer(sK40_skl)|~cC138(iV5475)|~cowlThing(iV5475)|~cC116(iV5475)|~cC140(iV5475)),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f511])).
% 0.12/0.38 fof(f513,plain,(
% 0.12/0.38 ~cowlThing(sK38_skl)|cowlNothing(sK39_skl)|~xsd_string(sK40_skl)|xsd_integer(sK40_skl)|~cC138(iV5475)|~cowlThing(iV5475)|~cC116(iV5475)|~cC140(iV5475)),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f511])).
% 0.12/0.38 fof(f514,definition,(
% 0.12/0.38 sQ0_spl <=> (cowlThing(sK38_skl))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f516,plain,(
% 0.12/0.38 ~cowlThing(sK38_skl)|sQ0_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f514])).
% 0.12/0.38 fof(f517,definition,(
% 0.12/0.38 sQ1_spl <=> (cowlNothing(sK39_skl))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f518,plain,(
% 0.12/0.38 cowlNothing(sK39_skl)|~sQ1_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f517])).
% 0.12/0.38 fof(f520,definition,(
% 0.12/0.38 sQ2_spl <=> (xsd_string(sK40_skl))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f521,plain,(
% 0.12/0.38 xsd_string(sK40_skl)|~sQ2_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f520])).
% 0.12/0.38 fof(f523,definition,(
% 0.12/0.38 sQ3_spl <=> (xsd_integer(sK40_skl))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f524,plain,(
% 0.12/0.38 xsd_integer(sK40_skl)|~sQ3_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f523])).
% 0.12/0.38 fof(f525,plain,(
% 0.12/0.38 ~xsd_integer(sK40_skl)|sQ3_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f523])).
% 0.12/0.38 fof(f526,definition,(
% 0.12/0.38 sQ4_spl <=> (cC138(iV5475))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f528,plain,(
% 0.12/0.38 ~cC138(iV5475)|sQ4_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f526])).
% 0.12/0.38 fof(f529,definition,(
% 0.12/0.38 sQ5_spl <=> (cowlThing(iV5475))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f531,plain,(
% 0.12/0.38 ~cowlThing(iV5475)|sQ5_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f529])).
% 0.12/0.38 fof(f532,definition,(
% 0.12/0.38 sQ6_spl <=> (cC116(iV5475))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f535,definition,(
% 0.12/0.38 sQ7_spl <=> (cC140(iV5475))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f536,plain,(
% 0.12/0.38 cC140(iV5475)|~sQ7_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f535])).
% 0.12/0.38 fof(f537,plain,(
% 0.12/0.38 ~cC140(iV5475)|sQ7_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f535])).
% 0.12/0.38 fof(f538,plain,(
% 0.12/0.38 ~sQ0_spl|sQ1_spl|sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl),
% 0.12/0.38 inference(split_clause,[status(thm)],[f512,f514,f517,f520,f523,f526,f529,f532,f535])).
% 0.12/0.38 fof(f539,plain,(
% 0.12/0.38 ~sQ0_spl|sQ1_spl|~sQ2_spl|sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl),
% 0.12/0.38 inference(split_clause,[status(thm)],[f513,f514,f517,f520,f523,f526,f529,f532,f535])).
% 0.12/0.38 fof(f550,plain,(
% 0.12/0.38 cC116(iV5475)|cC114(iV5475)),
% 0.12/0.38 inference(resolution,[status(thm)],[f152,f488])).
% 0.12/0.38 fof(f552,definition,(
% 0.12/0.38 sQ8_spl <=> (cC114(iV5475))),
% 0.12/0.38 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.12/0.38 fof(f553,plain,(
% 0.12/0.38 cC114(iV5475)|~sQ8_spl),
% 0.12/0.38 inference(component_clause,[status(thm)],[f552])).
% 0.12/0.38 fof(f555,plain,(
% 0.12/0.38 sQ6_spl|sQ8_spl),
% 0.12/0.38 inference(split_clause,[status(thm)],[f550,f532,f552])).
% 0.12/0.38 fof(f557,plain,(
% 0.12/0.38 cC140(iV5475)),
% 0.12/0.38 inference(resolution,[status(thm)],[f484,f487])).
% 0.12/0.38 fof(f558,plain,(
% 0.12/0.38 $false|sQ7_spl),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f557,f537])).
% 0.12/0.38 fof(f559,plain,(
% 0.12/0.38 sQ7_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f558])).
% 0.12/0.38 fof(f560,plain,(
% 0.12/0.38 $false|sQ5_spl),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f531,f93])).
% 0.12/0.38 fof(f561,plain,(
% 0.12/0.38 sQ5_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f560])).
% 0.12/0.38 fof(f563,plain,(
% 0.12/0.38 cC138(iV5475)|~sQ7_spl),
% 0.12/0.38 inference(resolution,[status(thm)],[f536,f230])).
% 0.12/0.38 fof(f564,plain,(
% 0.12/0.38 $false|sQ4_spl|~sQ7_spl),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f563,f528])).
% 0.12/0.38 fof(f565,plain,(
% 0.12/0.38 sQ4_spl|~sQ7_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f564])).
% 0.12/0.38 fof(f566,plain,(
% 0.12/0.38 $false|~sQ1_spl),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f518,f94])).
% 0.12/0.38 fof(f567,plain,(
% 0.12/0.38 ~sQ1_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f566])).
% 0.12/0.38 fof(f568,plain,(
% 0.12/0.38 $false|sQ0_spl),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f516,f93])).
% 0.12/0.38 fof(f569,plain,(
% 0.12/0.38 sQ0_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f568])).
% 0.12/0.38 fof(f570,plain,(
% 0.12/0.38 ~xsd_string(sK40_skl)|~sQ3_spl),
% 0.12/0.38 inference(resolution,[status(thm)],[f524,f97])).
% 0.12/0.38 fof(f571,plain,(
% 0.12/0.38 $false|~sQ2_spl|~sQ3_spl),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f570,f521])).
% 0.12/0.38 fof(f572,plain,(
% 0.12/0.38 ~sQ2_spl|~sQ3_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f571])).
% 0.12/0.38 fof(f573,plain,(
% 0.12/0.38 xsd_string(sK40_skl)|sQ3_spl),
% 0.12/0.38 inference(resolution,[status(thm)],[f525,f98])).
% 0.12/0.38 fof(f574,plain,(
% 0.12/0.38 sQ2_spl|sQ3_spl),
% 0.12/0.38 inference(split_clause,[status(thm)],[f573,f520,f523])).
% 0.12/0.38 fof(f575,plain,(
% 0.12/0.38 $false|~sQ8_spl),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f553,f492])).
% 0.12/0.38 fof(f576,plain,(
% 0.12/0.38 ~sQ8_spl),
% 0.12/0.38 inference(contradiction_clause,[status(thm)],[f575])).
% 0.12/0.38 fof(f577,plain,(
% 0.12/0.38 $false),
% 0.12/0.38 inference(sat_refutation,[status(thm)],[f538,f539,f555,f559,f561,f565,f567,f569,f572,f574,f576])).
% 0.12/0.38 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.41 % Elapsed time: 0.042959 seconds
% 0.12/0.41 % CPU time: 0.128487 seconds
% 0.12/0.41 % Total memory used: 24.998 MB
% 0.12/0.41 % Net memory used: 24.888 MB
%------------------------------------------------------------------------------