%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB053+1 : 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 : n006.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:43 PM UTC 2026
% Result : Theorem 9.36s 6.74s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWB053+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/5.44 % Computer : n006.cluster.edu
% 0.17/5.44 % Model : x86_64 x86_64
% 0.17/5.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.44 % Memory : 8046.5625MB
% 0.17/5.44 % OS : Linux 6.8.0-71-generic
% 0.17/5.45 % CPULimit : 300
% 0.17/5.45 % WCLimit : 300
% 0.17/5.45 % DateTime : Mon Sep 21 07:44:02 UTC 2026
% 0.17/5.45 % CPUTime :
% 0.21/5.52 % Drodi V4.1.1
% 9.36/6.74 % Refutation found
% 9.36/6.74 % SZS status Theorem for theBenchmark: Theorem is valid
% 9.36/6.74 % SZS output start CNFRefutation for theBenchmark
% 9.36/6.74 fof(f25,axiom,(
% 9.36/6.74 (! [X,C] :( iext(uri_rdf_type,X,C)<=> icext(C,X) ) )),
% 9.36/6.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.36/6.74 fof(f119,axiom,(
% 9.36/6.74 (! [X] :( icext(uri_owl_Class,X)<=> ic(X) ) )),
% 9.36/6.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.36/6.74 fof(f145,axiom,(
% 9.36/6.74 (! [X] : ~ icext(uri_owl_Nothing,X) )),
% 9.36/6.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.36/6.74 fof(f146,axiom,(
% 9.36/6.74 ic(uri_owl_Nothing) ),
% 9.36/6.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.36/6.74 fof(f343,axiom,(
% 9.36/6.74 (! [C1,C2] :( iext(uri_rdfs_subClassOf,C1,C2)<=> ( ic(C1)& ic(C2)& (! [X] :( icext(C1,X)=> icext(C2,X) ) )) ) )),
% 9.36/6.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.36/6.74 fof(f559,conjecture,(
% 9.36/6.74 iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_ex_c) ),
% 9.36/6.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.36/6.74 fof(f560,negated_conjecture,(
% 9.36/6.74 ~(iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_ex_c) )),
% 9.36/6.74 inference(negated_conjecture,[status(cth)],[f559])).
% 9.36/6.74 fof(f561,axiom,(
% 9.36/6.74 iext(uri_rdf_type,uri_ex_c,uri_owl_Class) ),
% 9.36/6.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.36/6.74 fof(f592,plain,(
% 9.36/6.74 ![X,C]: ((~iext(uri_rdf_type,X,C)|icext(C,X))&(iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 9.36/6.74 inference(NNF_transformation,[status(thm)],[f25])).
% 9.36/6.74 fof(f593,plain,(
% 9.36/6.74 (![X,C]: (~iext(uri_rdf_type,X,C)|icext(C,X)))&(![X,C]: (iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 9.36/6.74 inference(miniscoping,[status(thm)],[f592])).
% 9.36/6.74 fof(f594,plain,(
% 9.36/6.74 ![X0,X1]: (~iext(uri_rdf_type,X0,X1)|icext(X1,X0))),
% 9.36/6.74 inference(cnf_transformation,[status(thm)],[f593])).
% 9.36/6.74 fof(f772,plain,(
% 9.36/6.74 ![X]: ((~icext(uri_owl_Class,X)|ic(X))&(icext(uri_owl_Class,X)|~ic(X)))),
% 9.36/6.74 inference(NNF_transformation,[status(thm)],[f119])).
% 9.36/6.74 fof(f773,plain,(
% 9.36/6.74 (![X]: (~icext(uri_owl_Class,X)|ic(X)))&(![X]: (icext(uri_owl_Class,X)|~ic(X)))),
% 9.36/6.74 inference(miniscoping,[status(thm)],[f772])).
% 9.36/6.74 fof(f774,plain,(
% 9.36/6.74 ![X0]: (~icext(uri_owl_Class,X0)|ic(X0))),
% 9.36/6.74 inference(cnf_transformation,[status(thm)],[f773])).
% 9.36/6.74 fof(f823,plain,(
% 9.36/6.74 ![X0]: (~icext(uri_owl_Nothing,X0))),
% 9.36/6.74 inference(cnf_transformation,[status(thm)],[f145])).
% 9.36/6.74 fof(f824,plain,(
% 9.36/6.74 ic(uri_owl_Nothing)),
% 9.36/6.74 inference(cnf_transformation,[status(thm)],[f146])).
% 9.36/6.74 fof(f1731,plain,(
% 9.36/6.74 ![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)<=>((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X)))))),
% 9.36/6.74 inference(pre_NNF_transformation,[status(thm)],[f343])).
% 9.36/6.74 fof(f1732,plain,(
% 9.36/6.74 ![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))))))),
% 9.36/6.74 inference(NNF_transformation,[status(thm)],[f1731])).
% 9.36/6.74 fof(f1733,plain,(
% 9.36/6.74 (![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))))))),
% 9.36/6.74 inference(miniscoping,[status(thm)],[f1732])).
% 9.36/6.74 fof(f1734,plain,(
% 9.36/6.74 (![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,sK115_skl(C2,C1))&~icext(C2,sK115_skl(C2,C1))))))),
% 9.36/6.74 inference(skolemize,[status(esa),new_symbols(skolem,[sK115_skl]),skolemize(X,sK115_skl(C2,C1))],[f1733])).
% 9.36/6.74 fof(f1738,plain,(
% 9.36/6.74 ![X0,X1]: (iext(uri_rdfs_subClassOf,X0,X1)|~ic(X0)|~ic(X1)|icext(X0,sK115_skl(X1,X0)))),
% 9.36/6.74 inference(cnf_transformation,[status(thm)],[f1734])).
% 9.36/6.74 fof(f2405,plain,(
% 9.36/6.74 ~iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_ex_c)),
% 9.36/6.74 inference(cnf_transformation,[status(thm)],[f560])).
% 9.36/6.74 fof(f2406,plain,(
% 9.36/6.74 iext(uri_rdf_type,uri_ex_c,uri_owl_Class)),
% 9.36/6.74 inference(cnf_transformation,[status(thm)],[f561])).
% 9.36/6.74 fof(f2712,plain,(
% 9.36/6.74 icext(uri_owl_Class,uri_ex_c)),
% 9.36/6.74 inference(resolution,[status(thm)],[f594,f2406])).
% 9.36/6.74 fof(f4630,plain,(
% 9.36/6.74 ic(uri_ex_c)),
% 9.36/6.74 inference(resolution,[status(thm)],[f774,f2712])).
% 9.36/6.74 fof(f10004,plain,(
% 9.36/6.74 ![X0]: (iext(uri_rdfs_subClassOf,uri_owl_Nothing,X0)|~ic(X0)|icext(uri_owl_Nothing,sK115_skl(X0,uri_owl_Nothing)))),
% 9.36/6.75 inference(resolution,[status(thm)],[f1738,f824])).
% 9.36/6.75 fof(f10012,plain,(
% 9.36/6.75 ![X0]: (iext(uri_rdfs_subClassOf,uri_owl_Nothing,X0)|~ic(X0))),
% 9.36/6.75 inference(forward_subsumption_resolution,[status(thm)],[f10004,f823])).
% 9.36/6.75 fof(f10118,plain,(
% 9.36/6.75 iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_ex_c)),
% 9.36/6.75 inference(resolution,[status(thm)],[f10012,f4630])).
% 9.36/6.75 fof(f10156,plain,(
% 9.36/6.75 $false),
% 9.36/6.75 inference(forward_subsumption_resolution,[status(thm)],[f10118,f2405])).
% 9.36/6.75 % SZS output end CNFRefutation for theBenchmark.p
% 9.36/6.77 % Elapsed time: 1.312858 seconds
% 9.36/6.77 % CPU time: 9.686151 seconds
% 9.36/6.77 % Total memory used: 174.823 MB
% 9.36/6.77 % Net memory used: 168.776 MB
%------------------------------------------------------------------------------