%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB073+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 : n012.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:44 PM UTC 2026
% Result : Theorem 5.54s 1.11s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWB073+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 07:44:21 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.03/0.32 % Drodi V4.1.1
% 5.54/1.11 % Refutation found
% 5.54/1.11 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.54/1.11 % SZS output start CNFRefutation for theBenchmark
% 5.54/1.11 fof(f91,axiom,(
% 5.54/1.11 (! [X] :( iodp(X)=> ip(X) ) )),
% 5.54/1.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.54/1.11 fof(f92,axiom,(
% 5.54/1.11 (! [X] :( iodp(X)<=> iext(uri_rdf_type,X,uri_owl_DatatypeProperty) ) )),
% 5.54/1.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.54/1.11 fof(f180,axiom,(
% 5.54/1.11 (! [X,Y] : ~ iext(uri_owl_bottomDataProperty,X,Y) )),
% 5.54/1.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.54/1.11 fof(f181,axiom,(
% 5.54/1.11 iodp(uri_owl_bottomDataProperty) ),
% 5.54/1.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.54/1.11 fof(f344,axiom,(
% 5.54/1.11 (! [P1,P2] :( iext(uri_rdfs_subPropertyOf,P1,P2)<=> ( ip(P1)& ip(P2)& (! [X,Y] :( iext(P1,X,Y)=> iext(P2,X,Y) ) )) ) )),
% 5.54/1.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.54/1.11 fof(f559,conjecture,(
% 5.54/1.11 iext(uri_rdfs_subPropertyOf,uri_owl_bottomDataProperty,uri_ex_p) ),
% 5.54/1.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.54/1.11 fof(f560,negated_conjecture,(
% 5.54/1.11 ~(iext(uri_rdfs_subPropertyOf,uri_owl_bottomDataProperty,uri_ex_p) )),
% 5.54/1.11 inference(negated_conjecture,[status(cth)],[f559])).
% 5.54/1.11 fof(f561,axiom,(
% 5.54/1.11 iext(uri_rdf_type,uri_ex_p,uri_owl_DatatypeProperty) ),
% 5.54/1.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.54/1.11 fof(f707,plain,(
% 5.54/1.11 ![X]: (~iodp(X)|ip(X))),
% 5.54/1.11 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 5.54/1.11 fof(f708,plain,(
% 5.54/1.11 ![X0]: (~iodp(X0)|ip(X0))),
% 5.54/1.11 inference(cnf_transformation,[status(thm)],[f707])).
% 5.54/1.11 fof(f709,plain,(
% 5.54/1.11 ![X]: ((~iodp(X)|iext(uri_rdf_type,X,uri_owl_DatatypeProperty))&(iodp(X)|~iext(uri_rdf_type,X,uri_owl_DatatypeProperty)))),
% 5.54/1.11 inference(NNF_transformation,[status(thm)],[f92])).
% 5.54/1.11 fof(f710,plain,(
% 5.54/1.11 (![X]: (~iodp(X)|iext(uri_rdf_type,X,uri_owl_DatatypeProperty)))&(![X]: (iodp(X)|~iext(uri_rdf_type,X,uri_owl_DatatypeProperty)))),
% 5.54/1.11 inference(miniscoping,[status(thm)],[f709])).
% 5.54/1.11 fof(f712,plain,(
% 5.54/1.11 ![X0]: (iodp(X0)|~iext(uri_rdf_type,X0,uri_owl_DatatypeProperty))),
% 5.54/1.11 inference(cnf_transformation,[status(thm)],[f710])).
% 5.54/1.11 fof(f892,plain,(
% 5.54/1.11 ![X0,X1]: (~iext(uri_owl_bottomDataProperty,X0,X1))),
% 5.54/1.11 inference(cnf_transformation,[status(thm)],[f180])).
% 5.54/1.11 fof(f893,plain,(
% 5.54/1.11 iodp(uri_owl_bottomDataProperty)),
% 5.54/1.11 inference(cnf_transformation,[status(thm)],[f181])).
% 5.54/1.11 fof(f1740,plain,(
% 5.54/1.11 ![P1,P2]: (iext(uri_rdfs_subPropertyOf,P1,P2)<=>((ip(P1)&ip(P2))&(![X,Y]: (~iext(P1,X,Y)|iext(P2,X,Y)))))),
% 5.54/1.11 inference(pre_NNF_transformation,[status(thm)],[f344])).
% 5.54/1.11 fof(f1741,plain,(
% 5.54/1.11 ![P1,P2]: ((~iext(uri_rdfs_subPropertyOf,P1,P2)|((ip(P1)&ip(P2))&(![X,Y]: (~iext(P1,X,Y)|iext(P2,X,Y)))))&(iext(uri_rdfs_subPropertyOf,P1,P2)|((~ip(P1)|~ip(P2))|(?[X,Y]: (iext(P1,X,Y)&~iext(P2,X,Y))))))),
% 5.54/1.11 inference(NNF_transformation,[status(thm)],[f1740])).
% 5.54/1.11 fof(f1742,plain,(
% 5.54/1.11 (![P1,P2]: (~iext(uri_rdfs_subPropertyOf,P1,P2)|((ip(P1)&ip(P2))&(![X,Y]: (~iext(P1,X,Y)|iext(P2,X,Y))))))&(![P1,P2]: (iext(uri_rdfs_subPropertyOf,P1,P2)|((~ip(P1)|~ip(P2))|(?[X,Y]: (iext(P1,X,Y)&~iext(P2,X,Y))))))),
% 5.54/1.11 inference(miniscoping,[status(thm)],[f1741])).
% 5.54/1.11 fof(f1743,plain,(
% 5.54/1.11 (![P1,P2]: (~iext(uri_rdfs_subPropertyOf,P1,P2)|((ip(P1)&ip(P2))&(![X,Y]: (~iext(P1,X,Y)|iext(P2,X,Y))))))&(![P1,P2]: (iext(uri_rdfs_subPropertyOf,P1,P2)|((~ip(P1)|~ip(P2))|(iext(P1,sK116_skl(P2,P1),sK117_skl(P2,P1))&~iext(P2,sK116_skl(P2,P1),sK117_skl(P2,P1))))))),
% 5.54/1.11 inference(skolemize,[status(esa),new_symbols(skolem,[sK116_skl,sK117_skl]),skolemize(X,sK116_skl(P2,P1)),skolemize(Y,sK117_skl(P2,P1))],[f1742])).
% 5.54/1.11 fof(f1747,plain,(
% 5.54/1.11 ![X0,X1]: (iext(uri_rdfs_subPropertyOf,X0,X1)|~ip(X0)|~ip(X1)|iext(X0,sK116_skl(X1,X0),sK117_skl(X1,X0)))),
% 5.54/1.11 inference(cnf_transformation,[status(thm)],[f1743])).
% 5.54/1.11 fof(f2405,plain,(
% 5.54/1.11 ~iext(uri_rdfs_subPropertyOf,uri_owl_bottomDataProperty,uri_ex_p)),
% 5.54/1.11 inference(cnf_transformation,[status(thm)],[f560])).
% 5.54/1.11 fof(f2406,plain,(
% 5.54/1.11 iext(uri_rdf_type,uri_ex_p,uri_owl_DatatypeProperty)),
% 5.54/1.11 inference(cnf_transformation,[status(thm)],[f561])).
% 5.54/1.11 fof(f3123,plain,(
% 5.54/1.11 ip(uri_owl_bottomDataProperty)),
% 5.54/1.11 inference(resolution,[status(thm)],[f708,f893])).
% 5.54/1.11 fof(f4827,plain,(
% 5.54/1.11 iodp(uri_ex_p)),
% 5.54/1.11 inference(resolution,[status(thm)],[f712,f2406])).
% 5.54/1.12 fof(f5239,plain,(
% 5.54/1.12 ip(uri_ex_p)),
% 5.54/1.12 inference(resolution,[status(thm)],[f4827,f708])).
% 5.54/1.12 fof(f12328,plain,(
% 5.54/1.12 ![X0]: (iext(uri_rdfs_subPropertyOf,uri_owl_bottomDataProperty,X0)|~ip(X0)|iext(uri_owl_bottomDataProperty,sK116_skl(X0,uri_owl_bottomDataProperty),sK117_skl(X0,uri_owl_bottomDataProperty)))),
% 5.54/1.12 inference(resolution,[status(thm)],[f1747,f3123])).
% 5.54/1.12 fof(f12395,plain,(
% 5.54/1.12 ![X0]: (iext(uri_rdfs_subPropertyOf,uri_owl_bottomDataProperty,X0)|~ip(X0))),
% 5.54/1.12 inference(forward_subsumption_resolution,[status(thm)],[f12328,f892])).
% 5.54/1.12 fof(f12899,plain,(
% 5.54/1.12 iext(uri_rdfs_subPropertyOf,uri_owl_bottomDataProperty,uri_ex_p)),
% 5.54/1.12 inference(resolution,[status(thm)],[f12395,f5239])).
% 5.54/1.12 fof(f12976,plain,(
% 5.54/1.12 $false),
% 5.54/1.12 inference(forward_subsumption_resolution,[status(thm)],[f12899,f2405])).
% 5.54/1.12 % SZS output end CNFRefutation for theBenchmark.p
% 5.54/1.15 % Elapsed time: 0.844888 seconds
% 5.54/1.15 % CPU time: 6.227272 seconds
% 5.54/1.15 % Total memory used: 167.839 MB
% 5.54/1.15 % Net memory used: 162.147 MB
%------------------------------------------------------------------------------