%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB054+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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 5.82s 1.91s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB054+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n010.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 : Mon Sep 21 07:44:39 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.40 % Drodi V4.1.1
% 5.82/1.91 % Refutation found
% 5.82/1.91 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.82/1.91 % SZS output start CNFRefutation for theBenchmark
% 5.82/1.91 fof(f2,axiom,(
% 5.82/1.91 (! [X] : ir(X) )),
% 5.82/1.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.82/1.91 fof(f25,axiom,(
% 5.82/1.91 (! [X,C] :( iext(uri_rdf_type,X,C)<=> icext(C,X) ) )),
% 5.82/1.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.82/1.91 fof(f119,axiom,(
% 5.82/1.91 (! [X] :( icext(uri_owl_Class,X)<=> ic(X) ) )),
% 5.82/1.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.82/1.91 fof(f163,axiom,(
% 5.82/1.91 (! [X] :( icext(uri_owl_Thing,X)<=> ir(X) ) )),
% 5.82/1.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.82/1.91 fof(f164,axiom,(
% 5.82/1.91 ic(uri_owl_Thing) ),
% 5.82/1.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.82/1.91 fof(f343,axiom,(
% 5.82/1.91 (! [C1,C2] :( iext(uri_rdfs_subClassOf,C1,C2)<=> ( ic(C1)& ic(C2)& (! [X] :( icext(C1,X)=> icext(C2,X) ) )) ) )),
% 5.82/1.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.82/1.91 fof(f559,conjecture,(
% 5.82/1.91 iext(uri_rdfs_subClassOf,uri_ex_c,uri_owl_Thing) ),
% 5.82/1.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.82/1.91 fof(f560,negated_conjecture,(
% 5.82/1.91 ~(iext(uri_rdfs_subClassOf,uri_ex_c,uri_owl_Thing) )),
% 5.82/1.91 inference(negated_conjecture,[status(cth)],[f559])).
% 5.82/1.91 fof(f561,axiom,(
% 5.82/1.91 iext(uri_rdf_type,uri_ex_c,uri_owl_Class) ),
% 5.82/1.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.82/1.91 fof(f565,plain,(
% 5.82/1.91 ![X0]: (ir(X0))),
% 5.82/1.91 inference(cnf_transformation,[status(thm)],[f2])).
% 5.82/1.91 fof(f592,plain,(
% 5.82/1.91 ![X,C]: ((~iext(uri_rdf_type,X,C)|icext(C,X))&(iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 5.82/1.91 inference(NNF_transformation,[status(thm)],[f25])).
% 5.82/1.91 fof(f593,plain,(
% 5.82/1.91 (![X,C]: (~iext(uri_rdf_type,X,C)|icext(C,X)))&(![X,C]: (iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 5.82/1.91 inference(miniscoping,[status(thm)],[f592])).
% 5.82/1.91 fof(f594,plain,(
% 5.82/1.91 ![X0,X1]: (~iext(uri_rdf_type,X0,X1)|icext(X1,X0))),
% 5.82/1.91 inference(cnf_transformation,[status(thm)],[f593])).
% 5.82/1.91 fof(f772,plain,(
% 5.82/1.91 ![X]: ((~icext(uri_owl_Class,X)|ic(X))&(icext(uri_owl_Class,X)|~ic(X)))),
% 5.82/1.91 inference(NNF_transformation,[status(thm)],[f119])).
% 5.82/1.91 fof(f773,plain,(
% 5.82/1.91 (![X]: (~icext(uri_owl_Class,X)|ic(X)))&(![X]: (icext(uri_owl_Class,X)|~ic(X)))),
% 5.82/1.91 inference(miniscoping,[status(thm)],[f772])).
% 5.82/1.91 fof(f774,plain,(
% 5.82/1.91 ![X0]: (~icext(uri_owl_Class,X0)|ic(X0))),
% 5.82/1.91 inference(cnf_transformation,[status(thm)],[f773])).
% 5.82/1.91 fof(f859,plain,(
% 5.82/1.91 ![X]: ((~icext(uri_owl_Thing,X)|ir(X))&(icext(uri_owl_Thing,X)|~ir(X)))),
% 5.82/1.91 inference(NNF_transformation,[status(thm)],[f163])).
% 5.82/1.91 fof(f860,plain,(
% 5.82/1.91 (![X]: (~icext(uri_owl_Thing,X)|ir(X)))&(![X]: (icext(uri_owl_Thing,X)|~ir(X)))),
% 5.82/1.91 inference(miniscoping,[status(thm)],[f859])).
% 5.82/1.91 fof(f862,plain,(
% 5.82/1.91 ![X0]: (icext(uri_owl_Thing,X0)|~ir(X0))),
% 5.82/1.91 inference(cnf_transformation,[status(thm)],[f860])).
% 5.82/1.91 fof(f863,plain,(
% 5.82/1.91 ic(uri_owl_Thing)),
% 5.82/1.91 inference(cnf_transformation,[status(thm)],[f164])).
% 5.82/1.91 fof(f1731,plain,(
% 5.82/1.91 ![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)<=>((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X)))))),
% 5.82/1.91 inference(pre_NNF_transformation,[status(thm)],[f343])).
% 5.82/1.91 fof(f1732,plain,(
% 5.82/1.91 ![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))))))),
% 5.82/1.91 inference(NNF_transformation,[status(thm)],[f1731])).
% 5.82/1.91 fof(f1733,plain,(
% 5.82/1.91 (![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))))))),
% 5.82/1.91 inference(miniscoping,[status(thm)],[f1732])).
% 5.82/1.91 fof(f1734,plain,(
% 5.82/1.91 (![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))))))),
% 5.82/1.91 inference(skolemize,[status(esa),new_symbols(skolem,[sK115_skl]),skolemize(X,sK115_skl(C2,C1))],[f1733])).
% 5.82/1.91 fof(f1739,plain,(
% 5.82/1.91 ![X0,X1]: (iext(uri_rdfs_subClassOf,X0,X1)|~ic(X0)|~ic(X1)|~icext(X1,sK115_skl(X1,X0)))),
% 5.82/1.91 inference(cnf_transformation,[status(thm)],[f1734])).
% 5.82/1.91 fof(f2405,plain,(
% 5.82/1.91 ~iext(uri_rdfs_subClassOf,uri_ex_c,uri_owl_Thing)),
% 5.82/1.91 inference(cnf_transformation,[status(thm)],[f560])).
% 5.82/1.93 fof(f2406,plain,(
% 5.82/1.93 iext(uri_rdf_type,uri_ex_c,uri_owl_Class)),
% 5.82/1.93 inference(cnf_transformation,[status(thm)],[f561])).
% 5.82/1.93 fof(f2538,plain,(
% 5.82/1.93 ![X0]: (icext(uri_owl_Thing,X0))),
% 5.82/1.93 inference(forward_subsumption_resolution,[status(thm)],[f862,f565])).
% 5.82/1.93 fof(f2709,plain,(
% 5.82/1.93 icext(uri_owl_Class,uri_ex_c)),
% 5.82/1.93 inference(resolution,[status(thm)],[f594,f2406])).
% 5.82/1.93 fof(f4261,plain,(
% 5.82/1.93 ic(uri_ex_c)),
% 5.82/1.93 inference(resolution,[status(thm)],[f774,f2709])).
% 5.82/1.93 fof(f4803,definition,(
% 5.82/1.93 sQ88_spl <=> (ic(uri_owl_Thing))),
% 5.82/1.93 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 5.82/1.93 fof(f4805,plain,(
% 5.82/1.93 ~ic(uri_owl_Thing)|sQ88_spl),
% 5.82/1.93 inference(component_clause,[status(thm)],[f4803])).
% 5.82/1.93 fof(f4849,plain,(
% 5.82/1.93 $false|sQ88_spl),
% 5.82/1.93 inference(forward_subsumption_resolution,[status(thm)],[f4805,f863])).
% 5.82/1.93 fof(f4850,plain,(
% 5.82/1.93 sQ88_spl),
% 5.82/1.93 inference(contradiction_clause,[status(thm)],[f4849])).
% 5.82/1.93 fof(f8893,plain,(
% 5.82/1.93 ![X0]: (iext(uri_rdfs_subClassOf,X0,uri_owl_Thing)|~ic(X0)|~ic(uri_owl_Thing))),
% 5.82/1.93 inference(resolution,[status(thm)],[f1739,f2538])).
% 5.82/1.93 fof(f8898,definition,(
% 5.82/1.93 ![X0]: (sQ589_spl <=> (iext(uri_rdfs_subClassOf,X0,uri_owl_Thing)|~ic(X0)))),
% 5.82/1.93 introduced(definition,[new_symbols(definition,[sQ589_spl])],[split_symbol_definition])).
% 5.82/1.93 fof(f8899,plain,(
% 5.82/1.93 ![X0]: (iext(uri_rdfs_subClassOf,X0,uri_owl_Thing)|~ic(X0)|~sQ589_spl)),
% 5.82/1.93 inference(component_clause,[status(thm)],[f8898])).
% 5.82/1.93 fof(f8901,plain,(
% 5.82/1.93 sQ589_spl|~sQ88_spl),
% 5.82/1.93 inference(split_clause,[status(thm)],[f8893,f8898,f4803])).
% 5.82/1.93 fof(f9112,plain,(
% 5.82/1.93 iext(uri_rdfs_subClassOf,uri_ex_c,uri_owl_Thing)|~sQ589_spl),
% 5.82/1.93 inference(resolution,[status(thm)],[f8899,f4261])).
% 5.82/1.93 fof(f9150,plain,(
% 5.82/1.93 $false|~sQ589_spl),
% 5.82/1.93 inference(forward_subsumption_resolution,[status(thm)],[f9112,f2405])).
% 5.82/1.93 fof(f9151,plain,(
% 5.82/1.93 ~sQ589_spl),
% 5.82/1.93 inference(contradiction_clause,[status(thm)],[f9150])).
% 5.82/1.93 fof(f9152,plain,(
% 5.82/1.93 $false),
% 5.82/1.93 inference(sat_refutation,[status(thm)],[f4850,f8901,f9151])).
% 5.82/1.93 % SZS output end CNFRefutation for theBenchmark.p
% 5.82/1.95 % Elapsed time: 1.582111 seconds
% 5.82/1.95 % CPU time: 11.865764 seconds
% 5.82/1.95 % Total memory used: 179.003 MB
% 5.82/1.95 % Net memory used: 172.550 MB
%------------------------------------------------------------------------------