%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB049+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 : n018.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:42 PM UTC 2026
% Result : Theorem 14.75s 2.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB049+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.37 % Computer : n018.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 07:45:43 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.42 % Drodi V4.1.1
% 14.75/2.58 % Refutation found
% 14.75/2.58 % SZS status Theorem for theBenchmark: Theorem is valid
% 14.75/2.58 % SZS output start CNFRefutation for theBenchmark
% 14.75/2.58 fof(f1,axiom,(
% 14.75/2.58 (! [S,P,O] :( iext(P,S,O)=> ip(P) ) )),
% 14.75/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.75/2.58 fof(f2,axiom,(
% 14.75/2.58 (! [X] : ir(X) )),
% 14.75/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.75/2.58 fof(f25,axiom,(
% 14.75/2.58 (! [X,C] :( iext(uri_rdf_type,X,C)<=> icext(C,X) ) )),
% 14.75/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.75/2.58 fof(f68,axiom,(
% 14.75/2.58 (! [C,D] :( iext(uri_rdfs_subClassOf,C,D)=> ( ic(C)& ic(D)& (! [X] :( icext(C,X)=> icext(D,X) ) )) ) )),
% 14.75/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.75/2.58 fof(f70,axiom,(
% 14.75/2.58 (! [C] :( ic(C)=> iext(uri_rdfs_subClassOf,C,C) ) )),
% 14.75/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.75/2.58 fof(f156,axiom,(
% 14.75/2.58 ic(uri_owl_ReflexiveProperty) ),
% 14.75/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.75/2.58 fof(f268,axiom,(
% 14.75/2.58 (! [X,Y] :( iext(uri_owl_topObjectProperty,X,Y)<=> ( ir(X)& ir(Y) ) ) )),
% 14.75/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.75/2.58 fof(f352,axiom,(
% 14.75/2.58 (! [P1,P2] :( iext(uri_owl_equivalentProperty,P1,P2)<=> ( ip(P1)& ip(P2)& (! [X,Y] :( iext(P1,X,Y)<=> iext(P2,X,Y) ) )) ) )),
% 14.75/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.75/2.58 fof(f396,axiom,(
% 14.75/2.58 (! [P] :( icext(uri_owl_ReflexiveProperty,P)<=> ( ip(P)& (! [X] : iext(P,X,X) )) ) )),
% 14.75/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.75/2.58 fof(f559,conjecture,(
% 14.75/2.58 iext(uri_rdf_type,uri_ex_p,uri_owl_ReflexiveProperty) ),
% 14.75/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.75/2.58 fof(f560,negated_conjecture,(
% 14.75/2.58 ~(iext(uri_rdf_type,uri_ex_p,uri_owl_ReflexiveProperty) )),
% 14.75/2.58 inference(negated_conjecture,[status(cth)],[f559])).
% 14.75/2.58 fof(f561,axiom,(
% 14.75/2.58 iext(uri_owl_equivalentProperty,uri_ex_p,uri_owl_topObjectProperty) ),
% 14.75/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.75/2.58 fof(f562,plain,(
% 14.75/2.58 ![S,P,O]: (~iext(P,S,O)|ip(P))),
% 14.75/2.58 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 14.75/2.58 fof(f563,plain,(
% 14.75/2.58 ![P]: ((![S,O]: ~iext(P,S,O))|ip(P))),
% 14.75/2.58 inference(miniscoping,[status(thm)],[f562])).
% 14.75/2.58 fof(f564,plain,(
% 14.75/2.58 ![X0,X1,X2]: (~iext(X0,X1,X2)|ip(X0))),
% 14.75/2.58 inference(cnf_transformation,[status(thm)],[f563])).
% 14.75/2.58 fof(f565,plain,(
% 14.75/2.58 ![X0]: (ir(X0))),
% 14.75/2.58 inference(cnf_transformation,[status(thm)],[f2])).
% 14.75/2.58 fof(f592,plain,(
% 14.75/2.58 ![X,C]: ((~iext(uri_rdf_type,X,C)|icext(C,X))&(iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 14.75/2.58 inference(NNF_transformation,[status(thm)],[f25])).
% 14.75/2.58 fof(f593,plain,(
% 14.75/2.58 (![X,C]: (~iext(uri_rdf_type,X,C)|icext(C,X)))&(![X,C]: (iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 14.75/2.58 inference(miniscoping,[status(thm)],[f592])).
% 14.75/2.58 fof(f595,plain,(
% 14.75/2.58 ![X0,X1]: (iext(uri_rdf_type,X0,X1)|~icext(X1,X0))),
% 14.75/2.58 inference(cnf_transformation,[status(thm)],[f593])).
% 14.75/2.58 fof(f654,plain,(
% 14.75/2.58 ![C,D]: (~iext(uri_rdfs_subClassOf,C,D)|((ic(C)&ic(D))&(![X]: (~icext(C,X)|icext(D,X)))))),
% 14.75/2.58 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 14.75/2.58 fof(f657,plain,(
% 14.75/2.58 ![X0,X1,X2]: (~iext(uri_rdfs_subClassOf,X0,X1)|~icext(X0,X2)|icext(X1,X2))),
% 14.75/2.58 inference(cnf_transformation,[status(thm)],[f654])).
% 14.75/2.58 fof(f659,plain,(
% 14.75/2.58 ![C]: (~ic(C)|iext(uri_rdfs_subClassOf,C,C))),
% 14.75/2.58 inference(pre_NNF_transformation,[status(thm)],[f70])).
% 14.75/2.58 fof(f660,plain,(
% 14.75/2.58 ![X0]: (~ic(X0)|iext(uri_rdfs_subClassOf,X0,X0))),
% 14.75/2.58 inference(cnf_transformation,[status(thm)],[f659])).
% 14.75/2.58 fof(f847,plain,(
% 14.75/2.58 ic(uri_owl_ReflexiveProperty)),
% 14.75/2.58 inference(cnf_transformation,[status(thm)],[f156])).
% 14.75/2.58 fof(f1064,plain,(
% 14.75/2.58 ![X,Y]: ((~iext(uri_owl_topObjectProperty,X,Y)|(ir(X)&ir(Y)))&(iext(uri_owl_topObjectProperty,X,Y)|(~ir(X)|~ir(Y))))),
% 14.75/2.58 inference(NNF_transformation,[status(thm)],[f268])).
% 14.75/2.58 fof(f1065,plain,(
% 14.75/2.58 (![X,Y]: (~iext(uri_owl_topObjectProperty,X,Y)|(ir(X)&ir(Y))))&(![X,Y]: (iext(uri_owl_topObjectProperty,X,Y)|(~ir(X)|~ir(Y))))),
% 14.75/2.58 inference(miniscoping,[status(thm)],[f1064])).
% 14.75/2.58 fof(f1068,plain,(
% 14.75/2.58 ![X0,X1]: (iext(uri_owl_topObjectProperty,X0,X1)|~ir(X0)|~ir(X1))),
% 14.75/2.58 inference(cnf_transformation,[status(thm)],[f1065])).
% 14.75/2.58 fof(f1814,plain,(
% 14.75/2.58 ![P1,P2]: ((~iext(uri_owl_equivalentProperty,P1,P2)|((ip(P1)&ip(P2))&(![X,Y]: ((~iext(P1,X,Y)|iext(P2,X,Y))&(iext(P1,X,Y)|~iext(P2,X,Y))))))&(iext(uri_owl_equivalentProperty,P1,P2)|((~ip(P1)|~ip(P2))|(?[X,Y]: ((~iext(P1,X,Y)|~iext(P2,X,Y))&(iext(P1,X,Y)|iext(P2,X,Y)))))))),
% 16.68/2.59 inference(NNF_transformation,[status(thm)],[f352])).
% 16.68/2.59 fof(f1815,plain,(
% 16.68/2.59 (![P1,P2]: (~iext(uri_owl_equivalentProperty,P1,P2)|((ip(P1)&ip(P2))&((![X,Y]: (~iext(P1,X,Y)|iext(P2,X,Y)))&(![X,Y]: (iext(P1,X,Y)|~iext(P2,X,Y)))))))&(![P1,P2]: (iext(uri_owl_equivalentProperty,P1,P2)|((~ip(P1)|~ip(P2))|(?[X,Y]: ((~iext(P1,X,Y)|~iext(P2,X,Y))&(iext(P1,X,Y)|iext(P2,X,Y)))))))),
% 16.68/2.59 inference(miniscoping,[status(thm)],[f1814])).
% 16.68/2.59 fof(f1816,plain,(
% 16.68/2.59 (![P1,P2]: (~iext(uri_owl_equivalentProperty,P1,P2)|((ip(P1)&ip(P2))&((![X,Y]: (~iext(P1,X,Y)|iext(P2,X,Y)))&(![X,Y]: (iext(P1,X,Y)|~iext(P2,X,Y)))))))&(![P1,P2]: (iext(uri_owl_equivalentProperty,P1,P2)|((~ip(P1)|~ip(P2))|((~iext(P1,sK124_skl(P2,P1),sK125_skl(P2,P1))|~iext(P2,sK124_skl(P2,P1),sK125_skl(P2,P1)))&(iext(P1,sK124_skl(P2,P1),sK125_skl(P2,P1))|iext(P2,sK124_skl(P2,P1),sK125_skl(P2,P1)))))))),
% 16.68/2.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK124_skl,sK125_skl]),skolemize(X,sK124_skl(P2,P1)),skolemize(Y,sK125_skl(P2,P1))],[f1815])).
% 16.68/2.59 fof(f1820,plain,(
% 16.68/2.59 ![X0,X1,X2,X3]: (~iext(uri_owl_equivalentProperty,X0,X1)|iext(X0,X2,X3)|~iext(X1,X2,X3))),
% 16.68/2.59 inference(cnf_transformation,[status(thm)],[f1816])).
% 16.68/2.59 fof(f2040,plain,(
% 16.68/2.59 ![P]: ((~icext(uri_owl_ReflexiveProperty,P)|(ip(P)&(![X]: iext(P,X,X))))&(icext(uri_owl_ReflexiveProperty,P)|(~ip(P)|(?[X]: ~iext(P,X,X)))))),
% 16.68/2.59 inference(NNF_transformation,[status(thm)],[f396])).
% 16.68/2.59 fof(f2041,plain,(
% 16.68/2.59 (![P]: (~icext(uri_owl_ReflexiveProperty,P)|(ip(P)&(![X]: iext(P,X,X)))))&(![P]: (icext(uri_owl_ReflexiveProperty,P)|(~ip(P)|(?[X]: ~iext(P,X,X)))))),
% 16.68/2.59 inference(miniscoping,[status(thm)],[f2040])).
% 16.68/2.59 fof(f2042,plain,(
% 16.68/2.59 (![P]: (~icext(uri_owl_ReflexiveProperty,P)|(ip(P)&(![X]: iext(P,X,X)))))&(![P]: (icext(uri_owl_ReflexiveProperty,P)|(~ip(P)|~iext(P,sK177_skl(P),sK177_skl(P)))))),
% 16.68/2.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK177_skl]),skolemize(X,sK177_skl(P))],[f2041])).
% 16.68/2.59 fof(f2045,plain,(
% 16.68/2.59 ![X0]: (icext(uri_owl_ReflexiveProperty,X0)|~ip(X0)|~iext(X0,sK177_skl(X0),sK177_skl(X0)))),
% 16.68/2.59 inference(cnf_transformation,[status(thm)],[f2042])).
% 16.68/2.59 fof(f2405,plain,(
% 16.68/2.59 ~iext(uri_rdf_type,uri_ex_p,uri_owl_ReflexiveProperty)),
% 16.68/2.59 inference(cnf_transformation,[status(thm)],[f560])).
% 16.68/2.59 fof(f2406,plain,(
% 16.68/2.59 iext(uri_owl_equivalentProperty,uri_ex_p,uri_owl_topObjectProperty)),
% 16.68/2.59 inference(cnf_transformation,[status(thm)],[f561])).
% 16.68/2.59 fof(f2621,plain,(
% 16.68/2.59 iext(uri_rdfs_subClassOf,uri_owl_ReflexiveProperty,uri_owl_ReflexiveProperty)),
% 16.68/2.59 inference(resolution,[status(thm)],[f660,f847])).
% 16.68/2.59 fof(f2794,plain,(
% 16.68/2.59 ![X0,X1,X2]: (~iext(uri_rdfs_subClassOf,X0,X1)|~icext(X0,X2)|iext(uri_rdf_type,X2,X1))),
% 16.68/2.59 inference(resolution,[status(thm)],[f657,f595])).
% 16.68/2.59 fof(f2811,plain,(
% 16.68/2.59 ![X0]: (~iext(uri_rdfs_subClassOf,X0,uri_owl_ReflexiveProperty)|~icext(X0,uri_ex_p))),
% 16.68/2.59 inference(resolution,[status(thm)],[f2794,f2405])).
% 16.68/2.59 fof(f2815,plain,(
% 16.68/2.59 ~icext(uri_owl_ReflexiveProperty,uri_ex_p)),
% 16.68/2.59 inference(resolution,[status(thm)],[f2811,f2621])).
% 16.68/2.59 fof(f2979,plain,(
% 16.68/2.59 ![X0,X1]: (iext(uri_owl_topObjectProperty,X0,X1)|~ir(X1))),
% 16.68/2.59 inference(forward_subsumption_resolution,[status(thm)],[f1068,f565])).
% 16.68/2.59 fof(f2980,plain,(
% 16.68/2.59 ![X0,X1]: (iext(uri_owl_topObjectProperty,X0,X1))),
% 16.68/2.59 inference(resolution,[status(thm)],[f2979,f565])).
% 16.68/2.59 fof(f3061,plain,(
% 16.68/2.59 ![X0,X1]: (iext(uri_ex_p,X0,X1)|~iext(uri_owl_topObjectProperty,X0,X1))),
% 16.68/2.59 inference(resolution,[status(thm)],[f1820,f2406])).
% 16.68/2.59 fof(f3062,plain,(
% 16.68/2.59 ![X0,X1]: (iext(uri_ex_p,X0,X1))),
% 16.68/2.59 inference(forward_subsumption_resolution,[status(thm)],[f3061,f2980])).
% 16.68/2.59 fof(f3127,plain,(
% 16.68/2.59 ![X0]: (icext(uri_owl_ReflexiveProperty,X0)|~iext(X0,sK177_skl(X0),sK177_skl(X0)))),
% 16.68/2.59 inference(forward_subsumption_resolution,[status(thm)],[f2045,f564])).
% 16.68/2.59 fof(f3128,plain,(
% 16.68/2.59 icext(uri_owl_ReflexiveProperty,uri_ex_p)),
% 16.68/2.59 inference(resolution,[status(thm)],[f3127,f3062])).
% 16.68/2.59 fof(f3138,plain,(
% 16.68/2.59 $false),
% 16.68/2.59 inference(forward_subsumption_resolution,[status(thm)],[f3128,f2815])).
% 16.68/2.59 % SZS output end CNFRefutation for theBenchmark.p
% 16.68/2.64 % Elapsed time: 2.249555 seconds
% 16.68/2.64 % CPU time: 17.143249 seconds
% 16.68/2.64 % Total memory used: 207.898 MB
% 16.68/2.64 % Net memory used: 197.553 MB
%------------------------------------------------------------------------------