%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS157+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 : n020.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.08s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS157+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n020.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 22:56:02 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.08/0.38 % Refutation found
% 0.08/0.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.38 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.38 fof(f1,axiom,(
% 0.08/0.38 (! [X] :( cowlThing(X)& ~ cowlNothing(X) ) )),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f2,axiom,(
% 0.08/0.38 (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ) )),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f122,axiom,(
% 0.08/0.38 (! [X] :( cC216(X)<=> ( cC64(X)& cC214xcomp(X) ) ) )),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f133,axiom,(
% 0.08/0.38 (! [X] :( cC30(X)<=> ( cC28(X)& cC14(X) ) ) )),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f149,axiom,(
% 0.08/0.38 (! [X] :( cC46(X)<=> ( cC30(X)& cC44(X) ) ) )),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f202,axiom,(
% 0.08/0.38 (! [X] :( cTEST(X)<=> ( cC216(X)& cC46(X) ) ) )),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f203,axiom,(
% 0.08/0.38 cTEST(iV3102) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f220,conjecture,(
% 0.08/0.38 ( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& cC14(iV3102)& cC44(iV3102)& cC216(iV3102)& cC64(iV3102)& cC46(iV3102)& cC28(iV3102)& cowlThing(iV3102)& cC30(iV3102) ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f221,negated_conjecture,(
% 0.08/0.38 ~(( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& cC14(iV3102)& cC44(iV3102)& cC216(iV3102)& cC64(iV3102)& cC46(iV3102)& cC28(iV3102)& cowlThing(iV3102)& cC30(iV3102) ) )),
% 0.08/0.38 inference(negated_conjecture,[status(cth)],[f220])).
% 0.08/0.38 fof(f222,plain,(
% 0.08/0.38 (![X]: cowlThing(X))&(![X]: ~cowlNothing(X))),
% 0.08/0.38 inference(miniscoping,[status(thm)],[f1])).
% 0.08/0.38 fof(f223,plain,(
% 0.08/0.38 ![X0]: (cowlThing(X0))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f222])).
% 0.08/0.38 fof(f224,plain,(
% 0.08/0.38 ![X0]: (~cowlNothing(X0))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f222])).
% 0.08/0.38 fof(f225,plain,(
% 0.08/0.38 ![X]: ((~xsd_string(X)|~xsd_integer(X))&(xsd_string(X)|xsd_integer(X)))),
% 0.08/0.38 inference(NNF_transformation,[status(thm)],[f2])).
% 0.08/0.38 fof(f226,plain,(
% 0.08/0.38 (![X]: (~xsd_string(X)|~xsd_integer(X)))&(![X]: (xsd_string(X)|xsd_integer(X)))),
% 0.08/0.38 inference(miniscoping,[status(thm)],[f225])).
% 0.08/0.38 fof(f227,plain,(
% 0.08/0.38 ![X0]: (~xsd_string(X0)|~xsd_integer(X0))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f226])).
% 0.08/0.38 fof(f228,plain,(
% 0.08/0.38 ![X0]: (xsd_string(X0)|xsd_integer(X0))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f226])).
% 0.08/0.38 fof(f885,plain,(
% 0.08/0.38 ![X]: ((~cC216(X)|(cC64(X)&cC214xcomp(X)))&(cC216(X)|(~cC64(X)|~cC214xcomp(X))))),
% 0.08/0.38 inference(NNF_transformation,[status(thm)],[f122])).
% 0.08/0.38 fof(f886,plain,(
% 0.08/0.38 (![X]: (~cC216(X)|(cC64(X)&cC214xcomp(X))))&(![X]: (cC216(X)|(~cC64(X)|~cC214xcomp(X))))),
% 0.08/0.38 inference(miniscoping,[status(thm)],[f885])).
% 0.08/0.38 fof(f887,plain,(
% 0.08/0.38 ![X0]: (~cC216(X0)|cC64(X0))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f886])).
% 0.08/0.38 fof(f945,plain,(
% 0.08/0.38 ![X]: ((~cC30(X)|(cC28(X)&cC14(X)))&(cC30(X)|(~cC28(X)|~cC14(X))))),
% 0.08/0.38 inference(NNF_transformation,[status(thm)],[f133])).
% 0.08/0.38 fof(f946,plain,(
% 0.08/0.38 (![X]: (~cC30(X)|(cC28(X)&cC14(X))))&(![X]: (cC30(X)|(~cC28(X)|~cC14(X))))),
% 0.08/0.38 inference(miniscoping,[status(thm)],[f945])).
% 0.08/0.38 fof(f947,plain,(
% 0.08/0.38 ![X0]: (~cC30(X0)|cC28(X0))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f946])).
% 0.08/0.38 fof(f948,plain,(
% 0.08/0.38 ![X0]: (~cC30(X0)|cC14(X0))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f946])).
% 0.08/0.38 fof(f1033,plain,(
% 0.08/0.38 ![X]: ((~cC46(X)|(cC30(X)&cC44(X)))&(cC46(X)|(~cC30(X)|~cC44(X))))),
% 0.08/0.38 inference(NNF_transformation,[status(thm)],[f149])).
% 0.08/0.38 fof(f1034,plain,(
% 0.08/0.38 (![X]: (~cC46(X)|(cC30(X)&cC44(X))))&(![X]: (cC46(X)|(~cC30(X)|~cC44(X))))),
% 0.08/0.38 inference(miniscoping,[status(thm)],[f1033])).
% 0.08/0.38 fof(f1035,plain,(
% 0.08/0.38 ![X0]: (~cC46(X0)|cC30(X0))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f1034])).
% 0.08/0.38 fof(f1036,plain,(
% 0.08/0.38 ![X0]: (~cC46(X0)|cC44(X0))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f1034])).
% 0.08/0.38 fof(f1037,plain,(
% 0.08/0.38 ![X0]: (cC46(X0)|~cC30(X0)|~cC44(X0))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f1034])).
% 0.08/0.38 fof(f1325,plain,(
% 0.08/0.38 ![X]: ((~cTEST(X)|(cC216(X)&cC46(X)))&(cTEST(X)|(~cC216(X)|~cC46(X))))),
% 0.08/0.38 inference(NNF_transformation,[status(thm)],[f202])).
% 0.08/0.38 fof(f1326,plain,(
% 0.08/0.38 (![X]: (~cTEST(X)|(cC216(X)&cC46(X))))&(![X]: (cTEST(X)|(~cC216(X)|~cC46(X))))),
% 0.08/0.38 inference(miniscoping,[status(thm)],[f1325])).
% 0.08/0.38 fof(f1327,plain,(
% 0.08/0.38 ![X0]: (~cTEST(X0)|cC216(X0))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f1326])).
% 0.08/0.38 fof(f1328,plain,(
% 0.08/0.38 ![X0]: (~cTEST(X0)|cC46(X0))),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f1326])).
% 0.08/0.38 fof(f1330,plain,(
% 0.08/0.38 cTEST(iV3102)),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f203])).
% 0.08/0.38 fof(f1352,plain,(
% 0.08/0.38 ((((((((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: (xsd_string(X)<~>~xsd_integer(X))))|~cC14(iV3102))|~cC44(iV3102))|~cC216(iV3102))|~cC64(iV3102))|~cC46(iV3102))|~cC28(iV3102))|~cowlThing(iV3102))|~cC30(iV3102))),
% 0.08/0.38 inference(pre_NNF_transformation,[status(thm)],[f221])).
% 0.08/0.38 fof(f1353,plain,(
% 0.08/0.38 (((((((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: ((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))|~cC14(iV3102))|~cC44(iV3102))|~cC216(iV3102))|~cC64(iV3102))|~cC46(iV3102))|~cC28(iV3102))|~cowlThing(iV3102))|~cC30(iV3102)),
% 0.08/0.38 inference(NNF_transformation,[status(thm)],[f1352])).
% 0.08/0.38 fof(f1354,plain,(
% 0.08/0.38 ((((((((((?[X]: ~cowlThing(X))|(?[X]: cowlNothing(X)))|(?[X]: ((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))|~cC14(iV3102))|~cC44(iV3102))|~cC216(iV3102))|~cC64(iV3102))|~cC46(iV3102))|~cC28(iV3102))|~cowlThing(iV3102))|~cC30(iV3102)),
% 0.08/0.38 inference(miniscoping,[status(thm)],[f1353])).
% 0.08/0.38 fof(f1355,plain,(
% 0.08/0.38 (((((((((~cowlThing(sK148_skl)|cowlNothing(sK149_skl))|((xsd_string(sK150_skl)|~xsd_integer(sK150_skl))&(~xsd_string(sK150_skl)|xsd_integer(sK150_skl))))|~cC14(iV3102))|~cC44(iV3102))|~cC216(iV3102))|~cC64(iV3102))|~cC46(iV3102))|~cC28(iV3102))|~cowlThing(iV3102))|~cC30(iV3102)),
% 0.08/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK148_skl,sK149_skl,sK150_skl]),skolemize(X,sK148_skl),skolemize(X,sK149_skl),skolemize(X,sK150_skl)],[f1354])).
% 0.08/0.38 fof(f1356,plain,(
% 0.08/0.38 ~cowlThing(sK148_skl)|cowlNothing(sK149_skl)|xsd_string(sK150_skl)|~xsd_integer(sK150_skl)|~cC14(iV3102)|~cC44(iV3102)|~cC216(iV3102)|~cC64(iV3102)|~cC46(iV3102)|~cC28(iV3102)|~cowlThing(iV3102)|~cC30(iV3102)),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f1355])).
% 0.08/0.38 fof(f1357,plain,(
% 0.08/0.38 ~cowlThing(sK148_skl)|cowlNothing(sK149_skl)|~xsd_string(sK150_skl)|xsd_integer(sK150_skl)|~cC14(iV3102)|~cC44(iV3102)|~cC216(iV3102)|~cC64(iV3102)|~cC46(iV3102)|~cC28(iV3102)|~cowlThing(iV3102)|~cC30(iV3102)),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f1355])).
% 0.08/0.38 fof(f1358,definition,(
% 0.08/0.38 sQ0_spl <=> (cowlThing(sK148_skl))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f1360,plain,(
% 0.08/0.38 ~cowlThing(sK148_skl)|sQ0_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f1358])).
% 0.08/0.38 fof(f1361,definition,(
% 0.08/0.38 sQ1_spl <=> (cowlNothing(sK149_skl))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f1362,plain,(
% 0.08/0.38 cowlNothing(sK149_skl)|~sQ1_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f1361])).
% 0.08/0.38 fof(f1364,definition,(
% 0.08/0.38 sQ2_spl <=> (xsd_string(sK150_skl))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f1365,plain,(
% 0.08/0.38 xsd_string(sK150_skl)|~sQ2_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f1364])).
% 0.08/0.38 fof(f1367,definition,(
% 0.08/0.38 sQ3_spl <=> (xsd_integer(sK150_skl))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f1368,plain,(
% 0.08/0.38 xsd_integer(sK150_skl)|~sQ3_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f1367])).
% 0.08/0.38 fof(f1369,plain,(
% 0.08/0.38 ~xsd_integer(sK150_skl)|sQ3_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f1367])).
% 0.08/0.38 fof(f1370,definition,(
% 0.08/0.38 sQ4_spl <=> (cC14(iV3102))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f1372,plain,(
% 0.08/0.38 ~cC14(iV3102)|sQ4_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f1370])).
% 0.08/0.38 fof(f1373,definition,(
% 0.08/0.38 sQ5_spl <=> (cC44(iV3102))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f1375,plain,(
% 0.08/0.38 ~cC44(iV3102)|sQ5_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f1373])).
% 0.08/0.38 fof(f1376,definition,(
% 0.08/0.38 sQ6_spl <=> (cC216(iV3102))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f1378,plain,(
% 0.08/0.38 ~cC216(iV3102)|sQ6_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f1376])).
% 0.08/0.38 fof(f1379,definition,(
% 0.08/0.38 sQ7_spl <=> (cC64(iV3102))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f1381,plain,(
% 0.08/0.38 ~cC64(iV3102)|sQ7_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f1379])).
% 0.08/0.38 fof(f1382,definition,(
% 0.08/0.38 sQ8_spl <=> (cC46(iV3102))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f1385,definition,(
% 0.08/0.38 sQ9_spl <=> (cC28(iV3102))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f1387,plain,(
% 0.08/0.38 ~cC28(iV3102)|sQ9_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f1385])).
% 0.08/0.38 fof(f1388,definition,(
% 0.08/0.38 sQ10_spl <=> (cowlThing(iV3102))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f1390,plain,(
% 0.08/0.38 ~cowlThing(iV3102)|sQ10_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f1388])).
% 0.08/0.38 fof(f1391,definition,(
% 0.08/0.38 sQ11_spl <=> (cC30(iV3102))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f1393,plain,(
% 0.08/0.38 ~cC30(iV3102)|sQ11_spl),
% 0.08/0.38 inference(component_clause,[status(thm)],[f1391])).
% 0.08/0.38 fof(f1394,plain,(
% 0.08/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),
% 0.08/0.38 inference(split_clause,[status(thm)],[f1356,f1358,f1361,f1364,f1367,f1370,f1373,f1376,f1379,f1382,f1385,f1388,f1391])).
% 0.08/0.38 fof(f1395,plain,(
% 0.08/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),
% 0.08/0.38 inference(split_clause,[status(thm)],[f1357,f1358,f1361,f1364,f1367,f1370,f1373,f1376,f1379,f1382,f1385,f1388,f1391])).
% 0.08/0.38 fof(f1403,plain,(
% 0.08/0.38 cC216(iV3102)),
% 0.08/0.38 inference(resolution,[status(thm)],[f1327,f1330])).
% 0.08/0.38 fof(f1405,plain,(
% 0.08/0.38 cC46(iV3102)),
% 0.08/0.38 inference(resolution,[status(thm)],[f1328,f1330])).
% 0.08/0.38 fof(f1406,plain,(
% 0.08/0.38 cC44(iV3102)),
% 0.08/0.38 inference(resolution,[status(thm)],[f1405,f1036])).
% 0.08/0.38 fof(f1407,plain,(
% 0.08/0.38 cC30(iV3102)),
% 0.08/0.38 inference(resolution,[status(thm)],[f1405,f1035])).
% 0.08/0.38 fof(f1408,plain,(
% 0.08/0.38 $false|sQ11_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f1407,f1393])).
% 0.08/0.38 fof(f1409,plain,(
% 0.08/0.38 sQ11_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f1408])).
% 0.08/0.38 fof(f1410,plain,(
% 0.08/0.38 $false|sQ10_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f1390,f223])).
% 0.08/0.38 fof(f1411,plain,(
% 0.08/0.38 sQ10_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f1410])).
% 0.08/0.38 fof(f1413,plain,(
% 0.08/0.38 cC46(iV3102)|~cC30(iV3102)),
% 0.08/0.38 inference(resolution,[status(thm)],[f1406,f1037])).
% 0.08/0.38 fof(f1415,plain,(
% 0.08/0.38 sQ8_spl|~sQ11_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f1413,f1382,f1391])).
% 0.08/0.38 fof(f1416,plain,(
% 0.08/0.38 cC14(iV3102)),
% 0.08/0.38 inference(resolution,[status(thm)],[f1407,f948])).
% 0.08/0.38 fof(f1417,plain,(
% 0.08/0.38 cC28(iV3102)),
% 0.08/0.38 inference(resolution,[status(thm)],[f1407,f947])).
% 0.08/0.38 fof(f1420,plain,(
% 0.08/0.38 $false|sQ9_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f1417,f1387])).
% 0.08/0.38 fof(f1421,plain,(
% 0.08/0.38 sQ9_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f1420])).
% 0.08/0.38 fof(f1422,plain,(
% 0.08/0.38 ~cC216(iV3102)|sQ7_spl),
% 0.08/0.38 inference(resolution,[status(thm)],[f1381,f887])).
% 0.08/0.38 fof(f1423,plain,(
% 0.08/0.38 $false|sQ7_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f1422,f1403])).
% 0.08/0.38 fof(f1424,plain,(
% 0.08/0.38 sQ7_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f1423])).
% 0.08/0.38 fof(f1425,plain,(
% 0.08/0.38 $false|sQ6_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f1378,f1403])).
% 0.08/0.38 fof(f1426,plain,(
% 0.08/0.38 sQ6_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f1425])).
% 0.08/0.38 fof(f1427,plain,(
% 0.08/0.38 $false|sQ5_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f1375,f1406])).
% 0.08/0.38 fof(f1428,plain,(
% 0.08/0.38 sQ5_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f1427])).
% 0.08/0.38 fof(f1429,plain,(
% 0.08/0.38 $false|sQ4_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f1372,f1416])).
% 0.08/0.38 fof(f1430,plain,(
% 0.08/0.38 sQ4_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f1429])).
% 0.08/0.38 fof(f1431,plain,(
% 0.08/0.38 $false|~sQ1_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f1362,f224])).
% 0.08/0.38 fof(f1432,plain,(
% 0.08/0.38 ~sQ1_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f1431])).
% 0.08/0.38 fof(f1433,plain,(
% 0.08/0.38 $false|sQ0_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f1360,f223])).
% 0.08/0.38 fof(f1434,plain,(
% 0.08/0.38 sQ0_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f1433])).
% 0.08/0.38 fof(f1439,plain,(
% 0.08/0.38 ~xsd_string(sK150_skl)|~sQ3_spl),
% 0.08/0.38 inference(resolution,[status(thm)],[f1368,f227])).
% 0.08/0.38 fof(f1440,plain,(
% 0.08/0.38 $false|~sQ2_spl|~sQ3_spl),
% 0.08/0.38 inference(forward_subsumption_resolution,[status(thm)],[f1439,f1365])).
% 0.08/0.38 fof(f1441,plain,(
% 0.08/0.38 ~sQ2_spl|~sQ3_spl),
% 0.08/0.38 inference(contradiction_clause,[status(thm)],[f1440])).
% 0.08/0.38 fof(f1442,plain,(
% 0.08/0.38 xsd_string(sK150_skl)|sQ3_spl),
% 0.08/0.38 inference(resolution,[status(thm)],[f1369,f228])).
% 0.08/0.38 fof(f1443,plain,(
% 0.08/0.38 sQ2_spl|sQ3_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f1442,f1364,f1367])).
% 0.08/0.38 fof(f1444,plain,(
% 0.08/0.38 $false),
% 0.08/0.38 inference(sat_refutation,[status(thm)],[f1394,f1395,f1409,f1411,f1415,f1421,f1424,f1426,f1428,f1430,f1432,f1434,f1441,f1443])).
% 0.08/0.38 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/0.41 % Elapsed time: 0.045412 seconds
% 0.15/0.41 % CPU time: 0.071736 seconds
% 0.15/0.41 % Total memory used: 8.511 MB
% 0.15/0.41 % Net memory used: 8.494 MB
%------------------------------------------------------------------------------