%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB067+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 : n002.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 22.82s 3.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB067+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n002.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 07:47:46 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.14/0.40 % Drodi V4.1.1
% 22.82/3.37 % Refutation found
% 22.82/3.37 % SZS status Theorem for theBenchmark: Theorem is valid
% 22.82/3.37 % SZS output start CNFRefutation for theBenchmark
% 22.82/3.37 fof(f1,axiom,(
% 22.82/3.37 (! [S,P,O] :( iext(P,S,O)=> ip(P) ) )),
% 22.82/3.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.82/3.37 fof(f219,axiom,(
% 22.82/3.37 (! [X,Y] :( iext(uri_owl_inverseOf,X,Y)=> ( ip(X)& ip(Y) ) ) )),
% 22.82/3.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.82/3.37 fof(f352,axiom,(
% 22.82/3.37 (! [P1,P2] :( iext(uri_owl_equivalentProperty,P1,P2)<=> ( ip(P1)& ip(P2)& (! [X,Y] :( iext(P1,X,Y)<=> iext(P2,X,Y) ) )) ) )),
% 22.82/3.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.82/3.37 fof(f391,axiom,(
% 22.82/3.37 (! [P1,P2] :( iext(uri_owl_inverseOf,P1,P2)<=> ( ip(P1)& ip(P2)& (! [X,Y] :( iext(P1,X,Y)<=> iext(P2,Y,X) ) )) ) )),
% 22.82/3.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.82/3.37 fof(f559,conjecture,(
% 22.82/3.37 iext(uri_owl_equivalentProperty,uri_ex_p3,uri_ex_p1) ),
% 22.82/3.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.82/3.37 fof(f560,negated_conjecture,(
% 22.82/3.37 ~(iext(uri_owl_equivalentProperty,uri_ex_p3,uri_ex_p1) )),
% 22.82/3.37 inference(negated_conjecture,[status(cth)],[f559])).
% 22.82/3.37 fof(f561,axiom,(
% 22.82/3.37 ( iext(uri_owl_inverseOf,uri_ex_p3,uri_ex_p2)& iext(uri_owl_inverseOf,uri_ex_p2,uri_ex_p1) ) ),
% 22.82/3.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.82/3.37 fof(f562,plain,(
% 22.82/3.37 ![S,P,O]: (~iext(P,S,O)|ip(P))),
% 22.82/3.37 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 22.82/3.37 fof(f563,plain,(
% 22.82/3.37 ![P]: ((![S,O]: ~iext(P,S,O))|ip(P))),
% 22.82/3.37 inference(miniscoping,[status(thm)],[f562])).
% 22.82/3.37 fof(f564,plain,(
% 22.82/3.37 ![X0,X1,X2]: (~iext(X0,X1,X2)|ip(X0))),
% 22.82/3.37 inference(cnf_transformation,[status(thm)],[f563])).
% 22.82/3.37 fof(f965,plain,(
% 22.82/3.37 ![X,Y]: (~iext(uri_owl_inverseOf,X,Y)|(ip(X)&ip(Y)))),
% 22.82/3.37 inference(pre_NNF_transformation,[status(thm)],[f219])).
% 22.82/3.37 fof(f966,plain,(
% 22.82/3.37 ![X0,X1]: (~iext(uri_owl_inverseOf,X0,X1)|ip(X0))),
% 22.82/3.37 inference(cnf_transformation,[status(thm)],[f965])).
% 22.82/3.37 fof(f967,plain,(
% 22.82/3.37 ![X0,X1]: (~iext(uri_owl_inverseOf,X0,X1)|ip(X1))),
% 22.82/3.37 inference(cnf_transformation,[status(thm)],[f965])).
% 22.82/3.37 fof(f1814,plain,(
% 22.82/3.37 ![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)))))))),
% 22.82/3.37 inference(NNF_transformation,[status(thm)],[f352])).
% 22.82/3.37 fof(f1815,plain,(
% 22.82/3.37 (![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)))))))),
% 22.82/3.37 inference(miniscoping,[status(thm)],[f1814])).
% 22.82/3.37 fof(f1816,plain,(
% 22.82/3.37 (![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)))))))),
% 22.82/3.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK124_skl,sK125_skl]),skolemize(X,sK124_skl(P2,P1)),skolemize(Y,sK125_skl(P2,P1))],[f1815])).
% 22.82/3.38 fof(f1821,plain,(
% 22.82/3.38 ![X0,X1]: (iext(uri_owl_equivalentProperty,X0,X1)|~ip(X0)|~ip(X1)|~iext(X0,sK124_skl(X1,X0),sK125_skl(X1,X0))|~iext(X1,sK124_skl(X1,X0),sK125_skl(X1,X0)))),
% 22.82/3.38 inference(cnf_transformation,[status(thm)],[f1816])).
% 22.82/3.38 fof(f1822,plain,(
% 22.82/3.38 ![X0,X1]: (iext(uri_owl_equivalentProperty,X0,X1)|~ip(X0)|~ip(X1)|iext(X0,sK124_skl(X1,X0),sK125_skl(X1,X0))|iext(X1,sK124_skl(X1,X0),sK125_skl(X1,X0)))),
% 22.82/3.38 inference(cnf_transformation,[status(thm)],[f1816])).
% 22.82/3.38 fof(f1999,plain,(
% 22.82/3.38 ![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)))))))),
% 22.82/3.38 inference(NNF_transformation,[status(thm)],[f391])).
% 22.82/3.38 fof(f2000,plain,(
% 22.82/3.38 (![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)))))))),
% 22.82/3.38 inference(miniscoping,[status(thm)],[f1999])).
% 22.82/3.38 fof(f2001,plain,(
% 22.82/3.38 (![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)))))))),
% 22.82/3.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK166_skl,sK167_skl]),skolemize(X,sK166_skl(P2,P1)),skolemize(Y,sK167_skl(P2,P1))],[f2000])).
% 22.82/3.38 fof(f2004,plain,(
% 22.82/3.38 ![X0,X1,X2,X3]: (~iext(uri_owl_inverseOf,X0,X1)|~iext(X0,X2,X3)|iext(X1,X3,X2))),
% 22.82/3.38 inference(cnf_transformation,[status(thm)],[f2001])).
% 22.82/3.38 fof(f2005,plain,(
% 22.82/3.38 ![X0,X1,X2,X3]: (~iext(uri_owl_inverseOf,X0,X1)|iext(X0,X2,X3)|~iext(X1,X3,X2))),
% 22.82/3.38 inference(cnf_transformation,[status(thm)],[f2001])).
% 22.82/3.38 fof(f2405,plain,(
% 22.82/3.38 ~iext(uri_owl_equivalentProperty,uri_ex_p3,uri_ex_p1)),
% 22.82/3.38 inference(cnf_transformation,[status(thm)],[f560])).
% 22.82/3.38 fof(f2406,plain,(
% 22.82/3.38 iext(uri_owl_inverseOf,uri_ex_p3,uri_ex_p2)),
% 22.82/3.38 inference(cnf_transformation,[status(thm)],[f561])).
% 22.82/3.38 fof(f2407,plain,(
% 22.82/3.38 iext(uri_owl_inverseOf,uri_ex_p2,uri_ex_p1)),
% 22.82/3.38 inference(cnf_transformation,[status(thm)],[f561])).
% 22.82/3.38 fof(f2856,plain,(
% 22.82/3.38 ip(uri_ex_p3)),
% 22.82/3.38 inference(resolution,[status(thm)],[f966,f2406])).
% 22.82/3.38 fof(f2872,plain,(
% 22.82/3.38 ip(uri_ex_p1)),
% 22.82/3.38 inference(resolution,[status(thm)],[f967,f2407])).
% 22.82/3.38 fof(f4695,plain,(
% 22.82/3.38 ![X0,X1]: (iext(uri_owl_equivalentProperty,X0,X1)|~ip(X1)|~iext(X0,sK124_skl(X1,X0),sK125_skl(X1,X0))|~iext(X1,sK124_skl(X1,X0),sK125_skl(X1,X0)))),
% 22.82/3.38 inference(forward_subsumption_resolution,[status(thm)],[f1821,f564])).
% 22.82/3.38 fof(f4742,plain,(
% 22.82/3.38 ![X0]: (iext(uri_owl_equivalentProperty,X0,uri_ex_p1)|~ip(X0)|iext(X0,sK124_skl(uri_ex_p1,X0),sK125_skl(uri_ex_p1,X0))|iext(uri_ex_p1,sK124_skl(uri_ex_p1,X0),sK125_skl(uri_ex_p1,X0)))),
% 22.82/3.38 inference(resolution,[status(thm)],[f1822,f2872])).
% 22.82/3.38 fof(f5923,plain,(
% 22.82/3.38 ![X0,X1]: (~iext(uri_ex_p2,X0,X1)|iext(uri_ex_p1,X1,X0))),
% 22.82/3.38 inference(resolution,[status(thm)],[f2004,f2407])).
% 22.82/3.38 fof(f5924,plain,(
% 22.82/3.38 ![X0,X1]: (~iext(uri_ex_p3,X0,X1)|iext(uri_ex_p2,X1,X0))),
% 22.82/3.38 inference(resolution,[status(thm)],[f2004,f2406])).
% 22.82/3.38 fof(f5926,plain,(
% 22.82/3.38 ![X0,X1]: (iext(uri_ex_p2,X0,X1)|~iext(uri_ex_p1,X1,X0))),
% 22.82/3.38 inference(resolution,[status(thm)],[f2005,f2407])).
% 22.82/3.38 fof(f5927,plain,(
% 22.82/3.38 ![X0,X1]: (iext(uri_ex_p3,X0,X1)|~iext(uri_ex_p2,X1,X0))),
% 22.82/3.38 inference(resolution,[status(thm)],[f2005,f2406])).
% 22.82/3.38 fof(f7635,plain,(
% 22.82/3.38 iext(uri_owl_equivalentProperty,uri_ex_p3,uri_ex_p1)|iext(uri_ex_p3,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3))|iext(uri_ex_p1,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3))),
% 22.82/3.38 inference(resolution,[status(thm)],[f4742,f2856])).
% 22.82/3.38 fof(f7680,plain,(
% 22.82/3.38 iext(uri_ex_p3,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3))|iext(uri_ex_p1,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3))),
% 22.82/3.38 inference(forward_subsumption_resolution,[status(thm)],[f7635,f2405])).
% 22.82/3.38 fof(f7992,plain,(
% 22.82/3.38 iext(uri_ex_p3,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3))|iext(uri_ex_p2,sK125_skl(uri_ex_p1,uri_ex_p3),sK124_skl(uri_ex_p1,uri_ex_p3))),
% 22.82/3.38 inference(resolution,[status(thm)],[f7680,f5926])).
% 22.82/3.38 fof(f7995,plain,(
% 22.82/3.38 iext(uri_ex_p2,sK125_skl(uri_ex_p1,uri_ex_p3),sK124_skl(uri_ex_p1,uri_ex_p3))),
% 22.82/3.38 inference(forward_subsumption_resolution,[status(thm)],[f7992,f5924])).
% 22.82/3.38 fof(f7996,plain,(
% 22.82/3.38 iext(uri_ex_p3,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3))),
% 22.82/3.38 inference(resolution,[status(thm)],[f7995,f5927])).
% 22.82/3.38 fof(f7997,plain,(
% 22.82/3.38 iext(uri_ex_p1,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3))),
% 22.82/3.38 inference(resolution,[status(thm)],[f7995,f5923])).
% 22.82/3.38 fof(f8084,plain,(
% 22.82/3.38 iext(uri_owl_equivalentProperty,uri_ex_p3,uri_ex_p1)|~ip(uri_ex_p1)|~iext(uri_ex_p3,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3))),
% 22.82/3.40 inference(resolution,[status(thm)],[f7997,f4695])).
% 22.82/3.40 fof(f8086,plain,(
% 22.82/3.40 ~ip(uri_ex_p1)|~iext(uri_ex_p3,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3))),
% 22.82/3.40 inference(forward_subsumption_resolution,[status(thm)],[f8084,f2405])).
% 22.82/3.40 fof(f8088,plain,(
% 22.82/3.40 ~iext(uri_ex_p3,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3))),
% 22.82/3.40 inference(forward_subsumption_resolution,[status(thm)],[f8086,f2872])).
% 22.82/3.40 fof(f8089,plain,(
% 22.82/3.40 $false),
% 22.82/3.40 inference(backward_subsumption_resolution,[status(thm)],[f7996,f8088])).
% 22.82/3.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.79/3.41 % Elapsed time: 3.040597 seconds
% 0.79/3.41 % CPU time: 23.520145 seconds
% 0.79/3.41 % Total memory used: 219.974 MB
% 0.79/3.41 % Net memory used: 211.261 MB
%------------------------------------------------------------------------------