%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB047+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 : n009.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 214.92s 27.80s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWB047+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n009.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 07:43:42 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.51 % Drodi V4.1.1
% 214.92/27.80 % Refutation found
% 214.92/27.80 % SZS status Theorem for theBenchmark: Theorem is valid
% 214.92/27.80 % SZS output start CNFRefutation for theBenchmark
% 214.92/27.80 fof(f25,axiom,(
% 214.92/27.80 (! [X,C] :( iext(uri_rdf_type,X,C)<=> icext(C,X) ) )),
% 214.92/27.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.92/27.80 fof(f68,axiom,(
% 214.92/27.80 (! [C,D] :( iext(uri_rdfs_subClassOf,C,D)=> ( ic(C)& ic(D)& (! [X] :( icext(C,X)=> icext(D,X) ) )) ) )),
% 214.92/27.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.92/27.80 fof(f70,axiom,(
% 214.92/27.80 (! [C] :( ic(C)=> iext(uri_rdfs_subClassOf,C,C) ) )),
% 214.92/27.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.92/27.80 fof(f136,axiom,(
% 214.92/27.80 ic(uri_owl_InverseFunctionalProperty) ),
% 214.92/27.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.92/27.80 fof(f219,axiom,(
% 214.92/27.80 (! [X,Y] :( iext(uri_owl_inverseOf,X,Y)=> ( ip(X)& ip(Y) ) ) )),
% 214.92/27.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.92/27.80 fof(f391,axiom,(
% 214.92/27.80 (! [P1,P2] :( iext(uri_owl_inverseOf,P1,P2)<=> ( ip(P1)& ip(P2)& (! [X,Y] :( iext(P1,X,Y)<=> iext(P2,Y,X) ) )) ) )),
% 214.92/27.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.92/27.80 fof(f393,axiom,(
% 214.92/27.80 (! [P] :( icext(uri_owl_FunctionalProperty,P)<=> ( ip(P)& (! [X,Y1,Y2] :( ( iext(P,X,Y1)& iext(P,X,Y2) )=> Y1 = Y2 ) )) ) )),
% 214.92/27.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.92/27.80 fof(f394,axiom,(
% 214.92/27.80 (! [P] :( icext(uri_owl_InverseFunctionalProperty,P)<=> ( ip(P)& (! [X1,X2,Y] :( ( iext(P,X1,Y)& iext(P,X2,Y) )=> X1 = X2 ) )) ) )),
% 214.92/27.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.92/27.80 fof(f559,conjecture,(
% 214.92/27.80 iext(uri_rdf_type,uri_ex_p2,uri_owl_InverseFunctionalProperty) ),
% 214.92/27.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.92/27.80 fof(f560,negated_conjecture,(
% 214.92/27.80 ~(iext(uri_rdf_type,uri_ex_p2,uri_owl_InverseFunctionalProperty) )),
% 214.92/27.80 inference(negated_conjecture,[status(cth)],[f559])).
% 214.92/27.80 fof(f561,axiom,(
% 214.92/27.80 ( iext(uri_owl_inverseOf,uri_ex_p2,uri_ex_p1)& iext(uri_rdf_type,uri_ex_p1,uri_owl_FunctionalProperty) ) ),
% 214.92/27.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.92/27.80 fof(f592,plain,(
% 214.92/27.80 ![X,C]: ((~iext(uri_rdf_type,X,C)|icext(C,X))&(iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 214.92/27.80 inference(NNF_transformation,[status(thm)],[f25])).
% 214.92/27.80 fof(f593,plain,(
% 214.92/27.80 (![X,C]: (~iext(uri_rdf_type,X,C)|icext(C,X)))&(![X,C]: (iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 214.92/27.80 inference(miniscoping,[status(thm)],[f592])).
% 214.92/27.80 fof(f594,plain,(
% 214.92/27.80 ![X0,X1]: (~iext(uri_rdf_type,X0,X1)|icext(X1,X0))),
% 214.92/27.80 inference(cnf_transformation,[status(thm)],[f593])).
% 214.92/27.80 fof(f595,plain,(
% 214.92/27.80 ![X0,X1]: (iext(uri_rdf_type,X0,X1)|~icext(X1,X0))),
% 214.92/27.80 inference(cnf_transformation,[status(thm)],[f593])).
% 214.92/27.80 fof(f654,plain,(
% 214.92/27.80 ![C,D]: (~iext(uri_rdfs_subClassOf,C,D)|((ic(C)&ic(D))&(![X]: (~icext(C,X)|icext(D,X)))))),
% 214.92/27.80 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 214.92/27.80 fof(f657,plain,(
% 214.92/27.80 ![X0,X1,X2]: (~iext(uri_rdfs_subClassOf,X0,X1)|~icext(X0,X2)|icext(X1,X2))),
% 214.92/27.80 inference(cnf_transformation,[status(thm)],[f654])).
% 214.92/27.80 fof(f659,plain,(
% 214.92/27.80 ![C]: (~ic(C)|iext(uri_rdfs_subClassOf,C,C))),
% 214.92/27.80 inference(pre_NNF_transformation,[status(thm)],[f70])).
% 214.92/27.80 fof(f660,plain,(
% 214.92/27.80 ![X0]: (~ic(X0)|iext(uri_rdfs_subClassOf,X0,X0))),
% 214.92/27.80 inference(cnf_transformation,[status(thm)],[f659])).
% 214.92/27.80 fof(f808,plain,(
% 214.92/27.80 ic(uri_owl_InverseFunctionalProperty)),
% 214.92/27.80 inference(cnf_transformation,[status(thm)],[f136])).
% 214.92/27.80 fof(f965,plain,(
% 214.92/27.80 ![X,Y]: (~iext(uri_owl_inverseOf,X,Y)|(ip(X)&ip(Y)))),
% 214.92/27.80 inference(pre_NNF_transformation,[status(thm)],[f219])).
% 214.92/27.80 fof(f966,plain,(
% 214.92/27.80 ![X0,X1]: (~iext(uri_owl_inverseOf,X0,X1)|ip(X0))),
% 214.92/27.80 inference(cnf_transformation,[status(thm)],[f965])).
% 214.92/27.80 fof(f1999,plain,(
% 214.92/27.80 ![P1,P2]: ((~iext(uri_owl_inverseOf,P1,P2)|((ip(P1)&ip(P2))&(![X,Y]: ((~iext(P1,X,Y)|iext(P2,Y,X))&(iext(P1,X,Y)|~iext(P2,Y,X))))))&(iext(uri_owl_inverseOf,P1,P2)|((~ip(P1)|~ip(P2))|(?[X,Y]: ((~iext(P1,X,Y)|~iext(P2,Y,X))&(iext(P1,X,Y)|iext(P2,Y,X)))))))),
% 214.92/27.80 inference(NNF_transformation,[status(thm)],[f391])).
% 214.92/27.80 fof(f2000,plain,(
% 214.92/27.80 (![P1,P2]: (~iext(uri_owl_inverseOf,P1,P2)|((ip(P1)&ip(P2))&((![X,Y]: (~iext(P1,X,Y)|iext(P2,Y,X)))&(![X,Y]: (iext(P1,X,Y)|~iext(P2,Y,X)))))))&(![P1,P2]: (iext(uri_owl_inverseOf,P1,P2)|((~ip(P1)|~ip(P2))|(?[X,Y]: ((~iext(P1,X,Y)|~iext(P2,Y,X))&(iext(P1,X,Y)|iext(P2,Y,X)))))))),
% 214.92/27.81 inference(miniscoping,[status(thm)],[f1999])).
% 214.92/27.81 fof(f2001,plain,(
% 214.92/27.81 (![P1,P2]: (~iext(uri_owl_inverseOf,P1,P2)|((ip(P1)&ip(P2))&((![X,Y]: (~iext(P1,X,Y)|iext(P2,Y,X)))&(![X,Y]: (iext(P1,X,Y)|~iext(P2,Y,X)))))))&(![P1,P2]: (iext(uri_owl_inverseOf,P1,P2)|((~ip(P1)|~ip(P2))|((~iext(P1,sK166_skl(P2,P1),sK167_skl(P2,P1))|~iext(P2,sK167_skl(P2,P1),sK166_skl(P2,P1)))&(iext(P1,sK166_skl(P2,P1),sK167_skl(P2,P1))|iext(P2,sK167_skl(P2,P1),sK166_skl(P2,P1)))))))),
% 214.92/27.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK166_skl,sK167_skl]),skolemize(X,sK166_skl(P2,P1)),skolemize(Y,sK167_skl(P2,P1))],[f2000])).
% 214.92/27.81 fof(f2004,plain,(
% 214.92/27.81 ![X0,X1,X2,X3]: (~iext(uri_owl_inverseOf,X0,X1)|~iext(X0,X2,X3)|iext(X1,X3,X2))),
% 214.92/27.81 inference(cnf_transformation,[status(thm)],[f2001])).
% 214.92/27.81 fof(f2016,plain,(
% 214.92/27.81 ![P]: (icext(uri_owl_FunctionalProperty,P)<=>(ip(P)&(![X,Y1,Y2]: ((~iext(P,X,Y1)|~iext(P,X,Y2))|Y1=Y2))))),
% 214.92/27.81 inference(pre_NNF_transformation,[status(thm)],[f393])).
% 214.92/27.81 fof(f2017,plain,(
% 214.92/27.81 ![P]: ((~icext(uri_owl_FunctionalProperty,P)|(ip(P)&(![X,Y1,Y2]: ((~iext(P,X,Y1)|~iext(P,X,Y2))|Y1=Y2))))&(icext(uri_owl_FunctionalProperty,P)|(~ip(P)|(?[X,Y1,Y2]: ((iext(P,X,Y1)&iext(P,X,Y2))&~Y1=Y2)))))),
% 214.92/27.81 inference(NNF_transformation,[status(thm)],[f2016])).
% 214.92/27.81 fof(f2018,plain,(
% 214.92/27.81 (![P]: (~icext(uri_owl_FunctionalProperty,P)|(ip(P)&(![Y1,Y2]: ((![X]: (~iext(P,X,Y1)|~iext(P,X,Y2)))|Y1=Y2)))))&(![P]: (icext(uri_owl_FunctionalProperty,P)|(~ip(P)|(?[Y1,Y2]: ((?[X]: (iext(P,X,Y1)&iext(P,X,Y2)))&~Y1=Y2)))))),
% 214.92/27.81 inference(miniscoping,[status(thm)],[f2017])).
% 214.92/27.81 fof(f2019,plain,(
% 214.92/27.81 (![P]: (~icext(uri_owl_FunctionalProperty,P)|(ip(P)&(![Y1,Y2]: ((![X]: (~iext(P,X,Y1)|~iext(P,X,Y2)))|Y1=Y2)))))&(![P]: (icext(uri_owl_FunctionalProperty,P)|(~ip(P)|((iext(P,sK172_skl(P),sK170_skl(P))&iext(P,sK172_skl(P),sK171_skl(P)))&~sK170_skl(P)=sK171_skl(P)))))),
% 214.92/27.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK170_skl,sK171_skl,sK172_skl]),skolemize(Y1,sK170_skl(P)),skolemize(Y2,sK171_skl(P)),skolemize(X,sK172_skl(P))],[f2018])).
% 214.92/27.81 fof(f2021,plain,(
% 214.92/27.81 ![X0,X1,X2,X3]: (~icext(uri_owl_FunctionalProperty,X0)|~iext(X0,X1,X2)|~iext(X0,X1,X3)|X2=X3)),
% 214.92/27.81 inference(cnf_transformation,[status(thm)],[f2019])).
% 214.92/27.81 fof(f2025,plain,(
% 214.92/27.81 ![P]: (icext(uri_owl_InverseFunctionalProperty,P)<=>(ip(P)&(![X1,X2,Y]: ((~iext(P,X1,Y)|~iext(P,X2,Y))|X1=X2))))),
% 214.92/27.81 inference(pre_NNF_transformation,[status(thm)],[f394])).
% 214.92/27.81 fof(f2026,plain,(
% 214.92/27.81 ![P]: ((~icext(uri_owl_InverseFunctionalProperty,P)|(ip(P)&(![X1,X2,Y]: ((~iext(P,X1,Y)|~iext(P,X2,Y))|X1=X2))))&(icext(uri_owl_InverseFunctionalProperty,P)|(~ip(P)|(?[X1,X2,Y]: ((iext(P,X1,Y)&iext(P,X2,Y))&~X1=X2)))))),
% 214.92/27.81 inference(NNF_transformation,[status(thm)],[f2025])).
% 214.92/27.81 fof(f2027,plain,(
% 214.92/27.81 (![P]: (~icext(uri_owl_InverseFunctionalProperty,P)|(ip(P)&(![X1,X2]: ((![Y]: (~iext(P,X1,Y)|~iext(P,X2,Y)))|X1=X2)))))&(![P]: (icext(uri_owl_InverseFunctionalProperty,P)|(~ip(P)|(?[X1,X2]: ((?[Y]: (iext(P,X1,Y)&iext(P,X2,Y)))&~X1=X2)))))),
% 214.92/27.81 inference(miniscoping,[status(thm)],[f2026])).
% 214.92/27.81 fof(f2028,plain,(
% 214.92/27.81 (![P]: (~icext(uri_owl_InverseFunctionalProperty,P)|(ip(P)&(![X1,X2]: ((![Y]: (~iext(P,X1,Y)|~iext(P,X2,Y)))|X1=X2)))))&(![P]: (icext(uri_owl_InverseFunctionalProperty,P)|(~ip(P)|((iext(P,sK173_skl(P),sK175_skl(P))&iext(P,sK174_skl(P),sK175_skl(P)))&~sK173_skl(P)=sK174_skl(P)))))),
% 214.92/27.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK173_skl,sK174_skl,sK175_skl]),skolemize(X1,sK173_skl(P)),skolemize(X2,sK174_skl(P)),skolemize(Y,sK175_skl(P))],[f2027])).
% 214.92/27.81 fof(f2031,plain,(
% 214.92/27.81 ![X0]: (icext(uri_owl_InverseFunctionalProperty,X0)|~ip(X0)|iext(X0,sK173_skl(X0),sK175_skl(X0)))),
% 214.92/27.81 inference(cnf_transformation,[status(thm)],[f2028])).
% 214.92/27.81 fof(f2032,plain,(
% 214.92/27.81 ![X0]: (icext(uri_owl_InverseFunctionalProperty,X0)|~ip(X0)|iext(X0,sK174_skl(X0),sK175_skl(X0)))),
% 214.92/27.81 inference(cnf_transformation,[status(thm)],[f2028])).
% 214.92/27.81 fof(f2033,plain,(
% 214.92/27.81 ![X0]: (icext(uri_owl_InverseFunctionalProperty,X0)|~ip(X0)|~sK173_skl(X0)=sK174_skl(X0))),
% 214.92/27.81 inference(cnf_transformation,[status(thm)],[f2028])).
% 214.92/27.81 fof(f2405,plain,(
% 214.92/27.81 ~iext(uri_rdf_type,uri_ex_p2,uri_owl_InverseFunctionalProperty)),
% 214.92/27.81 inference(cnf_transformation,[status(thm)],[f560])).
% 215.75/27.89 fof(f2406,plain,(
% 215.75/27.89 iext(uri_owl_inverseOf,uri_ex_p2,uri_ex_p1)),
% 215.75/27.89 inference(cnf_transformation,[status(thm)],[f561])).
% 215.75/27.89 fof(f2407,plain,(
% 215.75/27.89 iext(uri_rdf_type,uri_ex_p1,uri_owl_FunctionalProperty)),
% 215.75/27.89 inference(cnf_transformation,[status(thm)],[f561])).
% 215.75/27.89 fof(f2716,plain,(
% 215.75/27.89 ![X0,X1,X2]: (~iext(uri_rdfs_subClassOf,X0,X1)|~icext(X0,X2)|iext(uri_rdf_type,X2,X1))),
% 215.75/27.89 inference(resolution,[status(thm)],[f657,f595])).
% 215.75/27.89 fof(f2717,plain,(
% 215.75/27.89 ![X0]: (~iext(uri_rdfs_subClassOf,X0,uri_owl_InverseFunctionalProperty)|~icext(X0,uri_ex_p2))),
% 215.75/27.89 inference(resolution,[status(thm)],[f2716,f2405])).
% 215.75/27.89 fof(f2735,plain,(
% 215.75/27.89 iext(uri_rdfs_subClassOf,uri_owl_InverseFunctionalProperty,uri_owl_InverseFunctionalProperty)),
% 215.75/27.89 inference(resolution,[status(thm)],[f660,f808])).
% 215.75/27.89 fof(f2749,plain,(
% 215.75/27.89 ~icext(uri_owl_InverseFunctionalProperty,uri_ex_p2)),
% 215.75/27.89 inference(resolution,[status(thm)],[f2735,f2717])).
% 215.75/27.89 fof(f2760,plain,(
% 215.75/27.89 icext(uri_owl_FunctionalProperty,uri_ex_p1)),
% 215.75/27.89 inference(resolution,[status(thm)],[f2407,f594])).
% 215.75/27.89 fof(f2798,plain,(
% 215.75/27.89 ip(uri_ex_p2)),
% 215.75/27.89 inference(resolution,[status(thm)],[f966,f2406])).
% 215.75/27.89 fof(f4083,plain,(
% 215.75/27.89 ![X0,X1]: (~iext(uri_ex_p2,X0,X1)|iext(uri_ex_p1,X1,X0))),
% 215.75/27.89 inference(resolution,[status(thm)],[f2004,f2406])).
% 215.75/27.89 fof(f4200,plain,(
% 215.75/27.89 icext(uri_owl_InverseFunctionalProperty,uri_ex_p2)|iext(uri_ex_p2,sK173_skl(uri_ex_p2),sK175_skl(uri_ex_p2))),
% 215.75/27.89 inference(resolution,[status(thm)],[f2031,f2798])).
% 215.75/27.89 fof(f4206,plain,(
% 215.75/27.89 iext(uri_ex_p2,sK173_skl(uri_ex_p2),sK175_skl(uri_ex_p2))),
% 215.75/27.89 inference(forward_subsumption_resolution,[status(thm)],[f4200,f2749])).
% 215.75/27.89 fof(f4232,plain,(
% 215.75/27.89 icext(uri_owl_InverseFunctionalProperty,uri_ex_p2)|iext(uri_ex_p2,sK174_skl(uri_ex_p2),sK175_skl(uri_ex_p2))),
% 215.75/27.89 inference(resolution,[status(thm)],[f2032,f2798])).
% 215.75/27.89 fof(f4237,plain,(
% 215.75/27.89 iext(uri_ex_p2,sK174_skl(uri_ex_p2),sK175_skl(uri_ex_p2))),
% 215.75/27.89 inference(forward_subsumption_resolution,[status(thm)],[f4232,f2749])).
% 215.75/27.89 fof(f4244,plain,(
% 215.75/27.89 iext(uri_ex_p1,sK175_skl(uri_ex_p2),sK173_skl(uri_ex_p2))),
% 215.75/27.89 inference(resolution,[status(thm)],[f4206,f4083])).
% 215.75/27.89 fof(f4246,plain,(
% 215.75/27.89 iext(uri_ex_p1,sK175_skl(uri_ex_p2),sK174_skl(uri_ex_p2))),
% 215.75/27.89 inference(resolution,[status(thm)],[f4237,f4083])).
% 215.75/27.89 fof(f26306,plain,(
% 215.75/27.89 ![X0,X1,X2]: (~iext(uri_ex_p1,X0,X1)|~iext(uri_ex_p1,X0,X2)|X1=X2)),
% 215.75/27.89 inference(resolution,[status(thm)],[f2021,f2760])).
% 215.75/27.89 fof(f27143,plain,(
% 215.75/27.89 ~ip(uri_ex_p2)|~sK173_skl(uri_ex_p2)=sK174_skl(uri_ex_p2)),
% 215.75/27.89 inference(resolution,[status(thm)],[f2033,f2749])).
% 215.75/27.89 fof(f27180,plain,(
% 215.75/27.89 ~sK173_skl(uri_ex_p2)=sK174_skl(uri_ex_p2)),
% 215.75/27.89 inference(forward_subsumption_resolution,[status(thm)],[f27143,f2798])).
% 215.75/27.89 fof(f29237,plain,(
% 215.75/27.89 ![X0]: (~iext(uri_ex_p1,sK175_skl(uri_ex_p2),X0)|X0=sK174_skl(uri_ex_p2))),
% 215.75/27.89 inference(resolution,[status(thm)],[f26306,f4246])).
% 215.75/27.89 fof(f29309,plain,(
% 215.75/27.89 sK173_skl(uri_ex_p2)=sK174_skl(uri_ex_p2)),
% 215.75/27.89 inference(resolution,[status(thm)],[f29237,f4244])).
% 215.75/27.89 fof(f29310,plain,(
% 215.75/27.89 $false),
% 215.75/27.89 inference(forward_subsumption_resolution,[status(thm)],[f29309,f27180])).
% 215.75/27.89 % SZS output end CNFRefutation for theBenchmark.p
% 66.39/27.98 % Elapsed time: 27.530043 seconds
% 66.39/27.98 % CPU time: 216.514026 seconds
% 66.39/27.98 % Total memory used: 593.200 MB
% 66.39/27.98 % Net memory used: 543.011 MB
%------------------------------------------------------------------------------