%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB009+3 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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 02:37:26 PM UTC 2026
% Result : Theorem 0.11s 0.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWB009+3 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n008.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 21 07:38:53 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.11/0.36 % Drodi V4.1.1
% 0.11/0.48 % Refutation found
% 0.11/0.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/0.48 % SZS output start CNFRefutation for theBenchmark
% 0.11/0.48 fof(f48,axiom,(
% 0.11/0.48 (! [X,Y] :( iext(uri_owl_someValuesFrom,X,Y)=> ( icext(uri_owl_Restriction,X)& ic(Y) ) ) )),
% 0.11/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.48 fof(f54,axiom,(
% 0.11/0.48 (! [C1,C2] :( iext(uri_rdfs_subClassOf,C1,C2)<=> ( ic(C1)& ic(C2)& (! [X] :( icext(C1,X)=> icext(C2,X) ) )) ) )),
% 0.11/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.48 fof(f58,axiom,(
% 0.11/0.48 (! [Z,P,C] :( ( iext(uri_owl_someValuesFrom,Z,C)& iext(uri_owl_onProperty,Z,P) )=> (! [X] :( icext(Z,X)<=> (? [Y] :( iext(P,X,Y)& icext(C,Y) ) )) )) )),
% 0.11/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.48 fof(f80,axiom,(
% 0.11/0.48 (! [X,C] :( iext(uri_rdf_type,X,C)<=> icext(C,X) ) )),
% 0.11/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.48 fof(f125,axiom,(
% 0.11/0.48 (! [C] :( ic(C)=> iext(uri_rdfs_subClassOf,C,C) ) )),
% 0.11/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.48 fof(f139,conjecture,(
% 0.11/0.48 (? [BNODE_x] :( iext(uri_ex_p,uri_ex_s,BNODE_x)& iext(uri_rdf_type,BNODE_x,uri_ex_c) ) )),
% 0.11/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.48 fof(f140,negated_conjecture,(
% 0.11/0.48 ~((? [BNODE_x] :( iext(uri_ex_p,uri_ex_s,BNODE_x)& iext(uri_rdf_type,BNODE_x,uri_ex_c) ) ))),
% 0.11/0.48 inference(negated_conjecture,[status(cth)],[f139])).
% 0.11/0.48 fof(f141,axiom,(
% 0.11/0.48 (? [BNODE_z] :( iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)& iext(uri_rdf_type,uri_ex_c,uri_owl_Class)& iext(uri_rdf_type,uri_ex_s,BNODE_z)& iext(uri_rdf_type,BNODE_z,uri_owl_Restriction)& iext(uri_owl_onProperty,BNODE_z,uri_ex_p)& iext(uri_owl_someValuesFrom,BNODE_z,uri_ex_c) ) )),
% 0.11/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.48 fof(f334,plain,(
% 0.11/0.48 ![X,Y]: (~iext(uri_owl_someValuesFrom,X,Y)|(icext(uri_owl_Restriction,X)&ic(Y)))),
% 0.11/0.48 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 0.11/0.48 fof(f336,plain,(
% 0.11/0.48 ![X0,X1]: (~iext(uri_owl_someValuesFrom,X0,X1)|ic(X1))),
% 0.11/0.48 inference(cnf_transformation,[status(thm)],[f334])).
% 0.11/0.48 fof(f360,plain,(
% 0.11/0.48 ![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)<=>((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X)))))),
% 0.11/0.48 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 0.11/0.48 fof(f361,plain,(
% 0.11/0.48 ![C1,C2]: ((~iext(uri_rdfs_subClassOf,C1,C2)|((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X)))))&(iext(uri_rdfs_subClassOf,C1,C2)|((~ic(C1)|~ic(C2))|(?[X]: (icext(C1,X)&~icext(C2,X))))))),
% 0.11/0.48 inference(NNF_transformation,[status(thm)],[f360])).
% 0.11/0.48 fof(f362,plain,(
% 0.11/0.48 (![C1,C2]: (~iext(uri_rdfs_subClassOf,C1,C2)|((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X))))))&(![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)|((~ic(C1)|~ic(C2))|(?[X]: (icext(C1,X)&~icext(C2,X))))))),
% 0.11/0.48 inference(miniscoping,[status(thm)],[f361])).
% 0.11/0.48 fof(f363,plain,(
% 0.11/0.48 (![C1,C2]: (~iext(uri_rdfs_subClassOf,C1,C2)|((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X))))))&(![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)|((~ic(C1)|~ic(C2))|(icext(C1,sK13_skl(C2,C1))&~icext(C2,sK13_skl(C2,C1))))))),
% 0.11/0.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(X,sK13_skl(C2,C1))],[f362])).
% 0.11/0.48 fof(f366,plain,(
% 0.11/0.48 ![X0,X1,X2]: (~iext(uri_rdfs_subClassOf,X0,X1)|~icext(X0,X2)|icext(X1,X2))),
% 0.11/0.48 inference(cnf_transformation,[status(thm)],[f363])).
% 0.11/0.48 fof(f390,plain,(
% 0.11/0.48 ![Z,P,C]: ((~iext(uri_owl_someValuesFrom,Z,C)|~iext(uri_owl_onProperty,Z,P))|(![X]: (icext(Z,X)<=>(?[Y]: (iext(P,X,Y)&icext(C,Y))))))),
% 0.11/0.48 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 0.11/0.48 fof(f391,plain,(
% 0.11/0.48 ![Z,P,C]: ((~iext(uri_owl_someValuesFrom,Z,C)|~iext(uri_owl_onProperty,Z,P))|(![X]: ((~icext(Z,X)|(?[Y]: (iext(P,X,Y)&icext(C,Y))))&(icext(Z,X)|(![Y]: (~iext(P,X,Y)|~icext(C,Y)))))))),
% 0.11/0.48 inference(NNF_transformation,[status(thm)],[f390])).
% 0.11/0.48 fof(f392,plain,(
% 0.11/0.48 ![Z,P,C]: ((~iext(uri_owl_someValuesFrom,Z,C)|~iext(uri_owl_onProperty,Z,P))|((![X]: (~icext(Z,X)|(?[Y]: (iext(P,X,Y)&icext(C,Y)))))&(![X]: (icext(Z,X)|(![Y]: (~iext(P,X,Y)|~icext(C,Y)))))))),
% 0.11/0.48 inference(miniscoping,[status(thm)],[f391])).
% 0.11/0.48 fof(f393,plain,(
% 0.11/0.48 ![Z,P,C]: ((~iext(uri_owl_someValuesFrom,Z,C)|~iext(uri_owl_onProperty,Z,P))|((![X]: (~icext(Z,X)|(iext(P,X,sK17_skl(X,C,P,Z))&icext(C,sK17_skl(X,C,P,Z)))))&(![X]: (icext(Z,X)|(![Y]: (~iext(P,X,Y)|~icext(C,Y)))))))),
% 0.11/0.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(Y,sK17_skl(X,C,P,Z))],[f392])).
% 0.11/0.48 fof(f394,plain,(
% 0.11/0.48 ![X0,X1,X2,X3]: (~iext(uri_owl_someValuesFrom,X0,X1)|~iext(uri_owl_onProperty,X0,X2)|~icext(X0,X3)|iext(X2,X3,sK17_skl(X3,X1,X2,X0)))),
% 0.11/0.48 inference(cnf_transformation,[status(thm)],[f393])).
% 0.11/0.48 fof(f395,plain,(
% 0.11/0.48 ![X0,X1,X2,X3]: (~iext(uri_owl_someValuesFrom,X0,X1)|~iext(uri_owl_onProperty,X0,X2)|~icext(X0,X3)|icext(X1,sK17_skl(X3,X1,X2,X0)))),
% 0.11/0.48 inference(cnf_transformation,[status(thm)],[f393])).
% 0.11/0.48 fof(f421,plain,(
% 0.11/0.48 ![X,C]: ((~iext(uri_rdf_type,X,C)|icext(C,X))&(iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 0.11/0.48 inference(NNF_transformation,[status(thm)],[f80])).
% 0.11/0.48 fof(f422,plain,(
% 0.11/0.48 (![X,C]: (~iext(uri_rdf_type,X,C)|icext(C,X)))&(![X,C]: (iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 0.11/0.48 inference(miniscoping,[status(thm)],[f421])).
% 0.11/0.48 fof(f423,plain,(
% 0.11/0.48 ![X0,X1]: (~iext(uri_rdf_type,X0,X1)|icext(X1,X0))),
% 0.11/0.48 inference(cnf_transformation,[status(thm)],[f422])).
% 0.11/0.48 fof(f424,plain,(
% 0.11/0.48 ![X0,X1]: (iext(uri_rdf_type,X0,X1)|~icext(X1,X0))),
% 0.11/0.48 inference(cnf_transformation,[status(thm)],[f422])).
% 0.11/0.48 fof(f488,plain,(
% 0.11/0.48 ![C]: (~ic(C)|iext(uri_rdfs_subClassOf,C,C))),
% 0.11/0.48 inference(pre_NNF_transformation,[status(thm)],[f125])).
% 0.11/0.48 fof(f489,plain,(
% 0.11/0.48 ![X0]: (~ic(X0)|iext(uri_rdfs_subClassOf,X0,X0))),
% 0.11/0.48 inference(cnf_transformation,[status(thm)],[f488])).
% 0.11/0.48 fof(f514,plain,(
% 0.11/0.48 (![BNODE_x]: (~iext(uri_ex_p,uri_ex_s,BNODE_x)|~iext(uri_rdf_type,BNODE_x,uri_ex_c)))),
% 0.11/0.48 inference(pre_NNF_transformation,[status(thm)],[f140])).
% 0.11/0.48 fof(f515,plain,(
% 0.11/0.48 ![X0]: (~iext(uri_ex_p,uri_ex_s,X0)|~iext(uri_rdf_type,X0,uri_ex_c))),
% 0.11/0.48 inference(cnf_transformation,[status(thm)],[f514])).
% 0.11/0.48 fof(f516,plain,(
% 0.11/0.48 (((((iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_c,uri_owl_Class))&iext(uri_rdf_type,uri_ex_s,sK18_skl))&iext(uri_rdf_type,sK18_skl,uri_owl_Restriction))&iext(uri_owl_onProperty,sK18_skl,uri_ex_p))&iext(uri_owl_someValuesFrom,sK18_skl,uri_ex_c))),
% 0.11/0.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(BNODE_z,sK18_skl)],[f141])).
% 0.11/0.48 fof(f519,plain,(
% 0.11/0.48 iext(uri_rdf_type,uri_ex_s,sK18_skl)),
% 0.11/0.48 inference(cnf_transformation,[status(thm)],[f516])).
% 0.11/0.48 fof(f521,plain,(
% 0.11/0.48 iext(uri_owl_onProperty,sK18_skl,uri_ex_p)),
% 0.11/0.48 inference(cnf_transformation,[status(thm)],[f516])).
% 0.11/0.48 fof(f522,plain,(
% 0.11/0.48 iext(uri_owl_someValuesFrom,sK18_skl,uri_ex_c)),
% 0.11/0.48 inference(cnf_transformation,[status(thm)],[f516])).
% 0.11/0.48 fof(f535,plain,(
% 0.11/0.48 icext(sK18_skl,uri_ex_s)),
% 0.11/0.48 inference(resolution,[status(thm)],[f423,f519])).
% 0.11/0.48 fof(f750,plain,(
% 0.11/0.48 ic(uri_ex_c)),
% 0.11/0.48 inference(resolution,[status(thm)],[f336,f522])).
% 0.11/0.48 fof(f1264,plain,(
% 0.11/0.48 ![X0,X1,X2]: (~iext(uri_rdfs_subClassOf,X0,X1)|~icext(X0,X2)|iext(uri_rdf_type,X2,X1))),
% 0.11/0.48 inference(resolution,[status(thm)],[f366,f424])).
% 0.11/0.48 fof(f1286,definition,(
% 0.11/0.48 sQ54_spl <=> (ic(uri_ex_c))),
% 0.11/0.48 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.11/0.48 fof(f1288,plain,(
% 0.11/0.48 ~ic(uri_ex_c)|sQ54_spl),
% 0.11/0.48 inference(component_clause,[status(thm)],[f1286])).
% 0.11/0.48 fof(f1810,plain,(
% 0.11/0.48 ![X0,X1]: (~iext(uri_owl_onProperty,sK18_skl,X0)|~icext(sK18_skl,X1)|iext(X0,X1,sK17_skl(X1,uri_ex_c,X0,sK18_skl)))),
% 0.11/0.48 inference(resolution,[status(thm)],[f394,f522])).
% 0.11/0.48 fof(f1831,plain,(
% 0.11/0.48 ![X0]: (~icext(sK18_skl,X0)|iext(uri_ex_p,X0,sK17_skl(X0,uri_ex_c,uri_ex_p,sK18_skl)))),
% 0.11/0.48 inference(resolution,[status(thm)],[f1810,f521])).
% 0.11/0.48 fof(f2031,plain,(
% 0.11/0.48 ![X0,X1]: (~iext(uri_owl_onProperty,sK18_skl,X0)|~icext(sK18_skl,X1)|icext(uri_ex_c,sK17_skl(X1,uri_ex_c,X0,sK18_skl)))),
% 0.11/0.48 inference(resolution,[status(thm)],[f395,f522])).
% 0.11/0.48 fof(f2307,plain,(
% 0.11/0.48 ~icext(sK18_skl,uri_ex_s)|~iext(uri_rdf_type,sK17_skl(uri_ex_s,uri_ex_c,uri_ex_p,sK18_skl),uri_ex_c)),
% 0.11/0.48 inference(resolution,[status(thm)],[f1831,f515])).
% 0.11/0.48 fof(f2309,definition,(
% 0.11/0.48 sQ171_spl <=> (icext(sK18_skl,uri_ex_s))),
% 0.11/0.48 introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition])).
% 0.11/0.48 fof(f2311,plain,(
% 0.11/0.48 ~icext(sK18_skl,uri_ex_s)|sQ171_spl),
% 0.11/0.48 inference(component_clause,[status(thm)],[f2309])).
% 0.11/0.50 fof(f2312,definition,(
% 0.11/0.50 sQ172_spl <=> (iext(uri_rdf_type,sK17_skl(uri_ex_s,uri_ex_c,uri_ex_p,sK18_skl),uri_ex_c))),
% 0.11/0.50 introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 0.11/0.50 fof(f2314,plain,(
% 0.11/0.50 ~iext(uri_rdf_type,sK17_skl(uri_ex_s,uri_ex_c,uri_ex_p,sK18_skl),uri_ex_c)|sQ172_spl),
% 0.11/0.50 inference(component_clause,[status(thm)],[f2312])).
% 0.11/0.50 fof(f2315,plain,(
% 0.11/0.50 ~sQ171_spl|~sQ172_spl),
% 0.11/0.50 inference(split_clause,[status(thm)],[f2307,f2309,f2312])).
% 0.11/0.50 fof(f2320,plain,(
% 0.11/0.50 $false|sQ171_spl),
% 0.11/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2311,f535])).
% 0.11/0.50 fof(f2321,plain,(
% 0.11/0.50 sQ171_spl),
% 0.11/0.50 inference(contradiction_clause,[status(thm)],[f2320])).
% 0.11/0.50 fof(f2427,plain,(
% 0.11/0.50 ![X0]: (~iext(uri_rdfs_subClassOf,X0,uri_ex_c)|~icext(X0,sK17_skl(uri_ex_s,uri_ex_c,uri_ex_p,sK18_skl))|sQ172_spl)),
% 0.11/0.50 inference(resolution,[status(thm)],[f2314,f1264])).
% 0.11/0.50 fof(f2430,plain,(
% 0.11/0.50 ~icext(uri_ex_c,sK17_skl(uri_ex_s,uri_ex_c,uri_ex_p,sK18_skl))|~ic(uri_ex_c)|sQ172_spl),
% 0.11/0.50 inference(resolution,[status(thm)],[f2427,f489])).
% 0.11/0.50 fof(f2431,definition,(
% 0.11/0.50 sQ185_spl <=> (icext(uri_ex_c,sK17_skl(uri_ex_s,uri_ex_c,uri_ex_p,sK18_skl)))),
% 0.11/0.50 introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition])).
% 0.11/0.50 fof(f2433,plain,(
% 0.11/0.50 ~icext(uri_ex_c,sK17_skl(uri_ex_s,uri_ex_c,uri_ex_p,sK18_skl))|sQ185_spl),
% 0.11/0.50 inference(component_clause,[status(thm)],[f2431])).
% 0.11/0.50 fof(f2434,plain,(
% 0.11/0.50 ~sQ185_spl|~sQ54_spl|sQ172_spl),
% 0.11/0.50 inference(split_clause,[status(thm)],[f2430,f2431,f1286,f2312])).
% 0.11/0.50 fof(f2435,plain,(
% 0.11/0.50 ~iext(uri_owl_onProperty,sK18_skl,uri_ex_p)|~icext(sK18_skl,uri_ex_s)|sQ185_spl),
% 0.11/0.50 inference(resolution,[status(thm)],[f2433,f2031])).
% 0.11/0.50 fof(f2439,definition,(
% 0.11/0.50 sQ186_spl <=> (iext(uri_owl_onProperty,sK18_skl,uri_ex_p))),
% 0.11/0.50 introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition])).
% 0.11/0.50 fof(f2441,plain,(
% 0.11/0.50 ~iext(uri_owl_onProperty,sK18_skl,uri_ex_p)|sQ186_spl),
% 0.11/0.50 inference(component_clause,[status(thm)],[f2439])).
% 0.11/0.50 fof(f2442,plain,(
% 0.11/0.50 ~sQ186_spl|~sQ171_spl|sQ185_spl),
% 0.11/0.50 inference(split_clause,[status(thm)],[f2435,f2439,f2309,f2431])).
% 0.11/0.50 fof(f2443,plain,(
% 0.11/0.50 $false|sQ186_spl),
% 0.11/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2441,f521])).
% 0.11/0.50 fof(f2444,plain,(
% 0.11/0.50 sQ186_spl),
% 0.11/0.50 inference(contradiction_clause,[status(thm)],[f2443])).
% 0.11/0.50 fof(f2445,plain,(
% 0.11/0.50 $false|sQ54_spl),
% 0.11/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1288,f750])).
% 0.11/0.50 fof(f2446,plain,(
% 0.11/0.50 sQ54_spl),
% 0.11/0.50 inference(contradiction_clause,[status(thm)],[f2445])).
% 0.11/0.50 fof(f2447,plain,(
% 0.11/0.50 $false),
% 0.11/0.50 inference(sat_refutation,[status(thm)],[f2315,f2321,f2434,f2442,f2444,f2446])).
% 0.11/0.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.11/0.51 % Elapsed time: 0.152603 seconds
% 0.11/0.51 % CPU time: 0.956790 seconds
% 0.11/0.51 % Total memory used: 40.829 MB
% 0.11/0.51 % Net memory used: 39.793 MB
%------------------------------------------------------------------------------