%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB075+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 : 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:45 PM UTC 2026
% Result : Theorem 8.18s 2.13s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWB075+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n010.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 07:45:54 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.48 % Drodi V4.1.1
% 8.18/2.13 % Refutation found
% 8.18/2.13 % SZS status Theorem for theBenchmark: Theorem is valid
% 8.18/2.13 % SZS output start CNFRefutation for theBenchmark
% 8.18/2.13 fof(f1,axiom,(
% 8.18/2.13 (! [S,P,O] :( iext(P,S,O)=> ip(P) ) )),
% 8.18/2.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.18/2.13 fof(f2,axiom,(
% 8.18/2.13 (! [X] : ir(X) )),
% 8.18/2.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.18/2.13 fof(f90,axiom,(
% 8.18/2.13 (! [X] :( iodp(X)=> (! [Y,Z] :( iext(X,Y,Z)=> ( ir(Y)& lv(Z) ) ) )) )),
% 8.18/2.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.18/2.13 fof(f91,axiom,(
% 8.18/2.13 (! [X] :( iodp(X)=> ip(X) ) )),
% 8.18/2.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.18/2.13 fof(f92,axiom,(
% 8.18/2.13 (! [X] :( iodp(X)<=> iext(uri_rdf_type,X,uri_owl_DatatypeProperty) ) )),
% 8.18/2.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.18/2.13 fof(f266,axiom,(
% 8.18/2.13 (! [X,Y] :( iext(uri_owl_topDataProperty,X,Y)<=> ( ir(X)& lv(Y) ) ) )),
% 8.18/2.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.18/2.13 fof(f267,axiom,(
% 8.18/2.13 iodp(uri_owl_topDataProperty) ),
% 8.18/2.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.18/2.13 fof(f344,axiom,(
% 8.18/2.13 (! [P1,P2] :( iext(uri_rdfs_subPropertyOf,P1,P2)<=> ( ip(P1)& ip(P2)& (! [X,Y] :( iext(P1,X,Y)=> iext(P2,X,Y) ) )) ) )),
% 8.18/2.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.18/2.13 fof(f559,conjecture,(
% 8.18/2.13 iext(uri_rdfs_subPropertyOf,uri_ex_p,uri_owl_topDataProperty) ),
% 8.18/2.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.18/2.13 fof(f560,negated_conjecture,(
% 8.18/2.13 ~(iext(uri_rdfs_subPropertyOf,uri_ex_p,uri_owl_topDataProperty) )),
% 8.18/2.13 inference(negated_conjecture,[status(cth)],[f559])).
% 8.18/2.13 fof(f561,axiom,(
% 8.18/2.13 iext(uri_rdf_type,uri_ex_p,uri_owl_DatatypeProperty) ),
% 8.18/2.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.18/2.13 fof(f562,plain,(
% 8.18/2.13 ![S,P,O]: (~iext(P,S,O)|ip(P))),
% 8.18/2.13 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 8.18/2.13 fof(f563,plain,(
% 8.18/2.13 ![P]: ((![S,O]: ~iext(P,S,O))|ip(P))),
% 8.18/2.13 inference(miniscoping,[status(thm)],[f562])).
% 8.18/2.13 fof(f564,plain,(
% 8.18/2.13 ![X0,X1,X2]: (~iext(X0,X1,X2)|ip(X0))),
% 8.18/2.13 inference(cnf_transformation,[status(thm)],[f563])).
% 8.18/2.13 fof(f565,plain,(
% 8.18/2.13 ![X0]: (ir(X0))),
% 8.18/2.13 inference(cnf_transformation,[status(thm)],[f2])).
% 8.18/2.13 fof(f704,plain,(
% 8.18/2.13 ![X]: (~iodp(X)|(![Y,Z]: (~iext(X,Y,Z)|(ir(Y)&lv(Z)))))),
% 8.18/2.13 inference(pre_NNF_transformation,[status(thm)],[f90])).
% 8.18/2.13 fof(f706,plain,(
% 8.18/2.13 ![X0,X1,X2]: (~iodp(X0)|~iext(X0,X1,X2)|lv(X2))),
% 8.18/2.13 inference(cnf_transformation,[status(thm)],[f704])).
% 8.18/2.13 fof(f707,plain,(
% 8.18/2.13 ![X]: (~iodp(X)|ip(X))),
% 8.18/2.13 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 8.18/2.13 fof(f708,plain,(
% 8.18/2.13 ![X0]: (~iodp(X0)|ip(X0))),
% 8.18/2.13 inference(cnf_transformation,[status(thm)],[f707])).
% 8.18/2.13 fof(f709,plain,(
% 8.18/2.13 ![X]: ((~iodp(X)|iext(uri_rdf_type,X,uri_owl_DatatypeProperty))&(iodp(X)|~iext(uri_rdf_type,X,uri_owl_DatatypeProperty)))),
% 8.18/2.13 inference(NNF_transformation,[status(thm)],[f92])).
% 8.18/2.13 fof(f710,plain,(
% 8.18/2.13 (![X]: (~iodp(X)|iext(uri_rdf_type,X,uri_owl_DatatypeProperty)))&(![X]: (iodp(X)|~iext(uri_rdf_type,X,uri_owl_DatatypeProperty)))),
% 8.18/2.13 inference(miniscoping,[status(thm)],[f709])).
% 8.18/2.13 fof(f712,plain,(
% 8.18/2.13 ![X0]: (iodp(X0)|~iext(uri_rdf_type,X0,uri_owl_DatatypeProperty))),
% 8.18/2.13 inference(cnf_transformation,[status(thm)],[f710])).
% 8.18/2.13 fof(f1058,plain,(
% 8.18/2.13 ![X,Y]: ((~iext(uri_owl_topDataProperty,X,Y)|(ir(X)&lv(Y)))&(iext(uri_owl_topDataProperty,X,Y)|(~ir(X)|~lv(Y))))),
% 8.18/2.13 inference(NNF_transformation,[status(thm)],[f266])).
% 8.18/2.13 fof(f1059,plain,(
% 8.18/2.13 (![X,Y]: (~iext(uri_owl_topDataProperty,X,Y)|(ir(X)&lv(Y))))&(![X,Y]: (iext(uri_owl_topDataProperty,X,Y)|(~ir(X)|~lv(Y))))),
% 8.18/2.13 inference(miniscoping,[status(thm)],[f1058])).
% 8.18/2.13 fof(f1062,plain,(
% 8.18/2.13 ![X0,X1]: (iext(uri_owl_topDataProperty,X0,X1)|~ir(X0)|~lv(X1))),
% 8.18/2.13 inference(cnf_transformation,[status(thm)],[f1059])).
% 8.18/2.13 fof(f1063,plain,(
% 8.18/2.13 iodp(uri_owl_topDataProperty)),
% 8.18/2.13 inference(cnf_transformation,[status(thm)],[f267])).
% 8.18/2.13 fof(f1740,plain,(
% 8.18/2.13 ![P1,P2]: (iext(uri_rdfs_subPropertyOf,P1,P2)<=>((ip(P1)&ip(P2))&(![X,Y]: (~iext(P1,X,Y)|iext(P2,X,Y)))))),
% 8.18/2.13 inference(pre_NNF_transformation,[status(thm)],[f344])).
% 8.18/2.13 fof(f1741,plain,(
% 8.18/2.13 ![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))))))),
% 8.18/2.16 inference(NNF_transformation,[status(thm)],[f1740])).
% 8.18/2.16 fof(f1742,plain,(
% 8.18/2.16 (![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))))))),
% 8.18/2.16 inference(miniscoping,[status(thm)],[f1741])).
% 8.18/2.16 fof(f1743,plain,(
% 8.18/2.16 (![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))))))),
% 8.18/2.16 inference(skolemize,[status(esa),new_symbols(skolem,[sK116_skl,sK117_skl]),skolemize(X,sK116_skl(P2,P1)),skolemize(Y,sK117_skl(P2,P1))],[f1742])).
% 8.18/2.16 fof(f1747,plain,(
% 8.18/2.16 ![X0,X1]: (iext(uri_rdfs_subPropertyOf,X0,X1)|~ip(X0)|~ip(X1)|iext(X0,sK116_skl(X1,X0),sK117_skl(X1,X0)))),
% 8.18/2.16 inference(cnf_transformation,[status(thm)],[f1743])).
% 8.18/2.16 fof(f1748,plain,(
% 8.18/2.16 ![X0,X1]: (iext(uri_rdfs_subPropertyOf,X0,X1)|~ip(X0)|~ip(X1)|~iext(X1,sK116_skl(X1,X0),sK117_skl(X1,X0)))),
% 8.18/2.16 inference(cnf_transformation,[status(thm)],[f1743])).
% 8.18/2.16 fof(f2405,plain,(
% 8.18/2.16 ~iext(uri_rdfs_subPropertyOf,uri_ex_p,uri_owl_topDataProperty)),
% 8.18/2.16 inference(cnf_transformation,[status(thm)],[f560])).
% 8.18/2.16 fof(f2406,plain,(
% 8.18/2.16 iext(uri_rdf_type,uri_ex_p,uri_owl_DatatypeProperty)),
% 8.18/2.16 inference(cnf_transformation,[status(thm)],[f561])).
% 8.18/2.16 fof(f2528,plain,(
% 8.18/2.16 ![X0,X1]: (iext(uri_owl_topDataProperty,X0,X1)|~lv(X1))),
% 8.18/2.16 inference(forward_subsumption_resolution,[status(thm)],[f1062,f565])).
% 8.18/2.16 fof(f2737,plain,(
% 8.18/2.16 ip(uri_owl_topDataProperty)),
% 8.18/2.16 inference(resolution,[status(thm)],[f708,f1063])).
% 8.18/2.16 fof(f2740,plain,(
% 8.18/2.16 iodp(uri_ex_p)),
% 8.18/2.16 inference(resolution,[status(thm)],[f712,f2406])).
% 8.18/2.16 fof(f2753,plain,(
% 8.18/2.16 ip(uri_ex_p)),
% 8.18/2.16 inference(resolution,[status(thm)],[f2740,f708])).
% 8.18/2.16 fof(f2754,plain,(
% 8.18/2.16 ![X0,X1]: (~iext(uri_ex_p,X0,X1)|lv(X1))),
% 8.18/2.16 inference(resolution,[status(thm)],[f2740,f706])).
% 8.18/2.16 fof(f4614,plain,(
% 8.18/2.16 ![X0]: (iext(uri_rdfs_subPropertyOf,X0,uri_owl_topDataProperty)|~ip(X0)|iext(X0,sK116_skl(uri_owl_topDataProperty,X0),sK117_skl(uri_owl_topDataProperty,X0)))),
% 8.18/2.16 inference(resolution,[status(thm)],[f1747,f2737])).
% 8.18/2.16 fof(f4628,plain,(
% 8.18/2.16 ![X0,X1]: (iext(uri_rdfs_subPropertyOf,X0,X1)|~ip(X0)|~iext(X1,sK116_skl(X1,X0),sK117_skl(X1,X0)))),
% 8.18/2.16 inference(forward_subsumption_resolution,[status(thm)],[f1748,f564])).
% 8.18/2.16 fof(f4963,plain,(
% 8.18/2.16 iext(uri_rdfs_subPropertyOf,uri_ex_p,uri_owl_topDataProperty)|iext(uri_ex_p,sK116_skl(uri_owl_topDataProperty,uri_ex_p),sK117_skl(uri_owl_topDataProperty,uri_ex_p))),
% 8.18/2.16 inference(resolution,[status(thm)],[f4614,f2753])).
% 8.18/2.16 fof(f4979,plain,(
% 8.18/2.16 iext(uri_ex_p,sK116_skl(uri_owl_topDataProperty,uri_ex_p),sK117_skl(uri_owl_topDataProperty,uri_ex_p))),
% 8.18/2.16 inference(forward_subsumption_resolution,[status(thm)],[f4963,f2405])).
% 8.18/2.16 fof(f5149,plain,(
% 8.18/2.16 lv(sK117_skl(uri_owl_topDataProperty,uri_ex_p))),
% 8.18/2.16 inference(resolution,[status(thm)],[f4979,f2754])).
% 8.18/2.16 fof(f5154,plain,(
% 8.18/2.16 ![X0]: (iext(uri_owl_topDataProperty,X0,sK117_skl(uri_owl_topDataProperty,uri_ex_p)))),
% 8.18/2.16 inference(resolution,[status(thm)],[f5149,f2528])).
% 8.18/2.16 fof(f5503,plain,(
% 8.18/2.16 iext(uri_rdfs_subPropertyOf,uri_ex_p,uri_owl_topDataProperty)|~ip(uri_ex_p)),
% 8.18/2.16 inference(resolution,[status(thm)],[f5154,f4628])).
% 8.18/2.16 fof(f5505,plain,(
% 8.18/2.16 ~ip(uri_ex_p)),
% 8.18/2.16 inference(forward_subsumption_resolution,[status(thm)],[f5503,f2405])).
% 8.18/2.16 fof(f5506,plain,(
% 8.18/2.16 $false),
% 8.18/2.16 inference(forward_subsumption_resolution,[status(thm)],[f5505,f2753])).
% 8.18/2.16 % SZS output end CNFRefutation for theBenchmark.p
% 12.31/2.19 % Elapsed time: 1.734688 seconds
% 12.31/2.19 % CPU time: 13.051641 seconds
% 12.31/2.19 % Total memory used: 174.125 MB
% 12.31/2.19 % Net memory used: 168.348 MB
%------------------------------------------------------------------------------