%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB071+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 : 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:44 PM UTC 2026
% Result : Theorem 143.56s 18.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB071+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.11/0.36 % Computer : n010.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 07:45:09 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.41 % Drodi V4.1.1
% 143.56/18.66 % Refutation found
% 143.56/18.66 % SZS status Theorem for theBenchmark: Theorem is valid
% 143.56/18.66 % SZS output start CNFRefutation for theBenchmark
% 143.56/18.66 fof(f1,axiom,(
% 143.56/18.66 (! [S,P,O] :( iext(P,S,O)=> ip(P) ) )),
% 143.56/18.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 143.56/18.66 fof(f2,axiom,(
% 143.56/18.66 (! [X] : ir(X) )),
% 143.56/18.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 143.56/18.66 fof(f25,axiom,(
% 143.56/18.66 (! [X,C] :( iext(uri_rdf_type,X,C)<=> icext(C,X) ) )),
% 143.56/18.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 143.56/18.66 fof(f345,axiom,(
% 143.56/18.66 (! [X,Y] :( iext(uri_owl_differentFrom,X,Y)<=> X != Y ) )),
% 143.56/18.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 143.56/18.66 fof(f393,axiom,(
% 143.56/18.66 (! [P] :( icext(uri_owl_FunctionalProperty,P)<=> ( ip(P)& (! [X,Y1,Y2] :( ( iext(P,X,Y1)& iext(P,X,Y2) )=> Y1 = Y2 ) )) ) )),
% 143.56/18.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 143.56/18.66 fof(f405,axiom,(
% 143.56/18.66 (! [P,A1,A2] :( ( ir(A1)& ip(P)& ir(A2)& ~ iext(P,A1,A2) )=> (? [Z] :( iext(uri_owl_sourceIndividual,Z,A1)& iext(uri_owl_assertionProperty,Z,P)& iext(uri_owl_targetIndividual,Z,A2) ) )) )),
% 143.56/18.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 143.56/18.66 fof(f559,conjecture,(
% 143.56/18.66 (? [X0] :( iext(uri_owl_sourceIndividual,X0,uri_ex_s)& iext(uri_owl_assertionProperty,X0,uri_ex_p)& iext(uri_owl_targetIndividual,X0,uri_ex_o2) ) )),
% 143.56/18.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 143.56/18.66 fof(f560,negated_conjecture,(
% 143.56/18.66 ~((? [X0] :( iext(uri_owl_sourceIndividual,X0,uri_ex_s)& iext(uri_owl_assertionProperty,X0,uri_ex_p)& iext(uri_owl_targetIndividual,X0,uri_ex_o2) ) ))),
% 143.56/18.66 inference(negated_conjecture,[status(cth)],[f559])).
% 143.56/18.66 fof(f561,axiom,(
% 143.56/18.66 ( iext(uri_rdf_type,uri_ex_p,uri_owl_FunctionalProperty)& iext(uri_ex_p,uri_ex_s,uri_ex_o1)& iext(uri_owl_differentFrom,uri_ex_o2,uri_ex_o1) ) ),
% 143.56/18.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 143.56/18.66 fof(f562,plain,(
% 143.56/18.66 ![S,P,O]: (~iext(P,S,O)|ip(P))),
% 143.56/18.66 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 143.56/18.66 fof(f563,plain,(
% 143.56/18.66 ![P]: ((![S,O]: ~iext(P,S,O))|ip(P))),
% 143.56/18.66 inference(miniscoping,[status(thm)],[f562])).
% 143.56/18.66 fof(f564,plain,(
% 143.56/18.66 ![X0,X1,X2]: (~iext(X0,X1,X2)|ip(X0))),
% 143.56/18.66 inference(cnf_transformation,[status(thm)],[f563])).
% 143.56/18.66 fof(f565,plain,(
% 143.56/18.66 ![X0]: (ir(X0))),
% 143.56/18.66 inference(cnf_transformation,[status(thm)],[f2])).
% 143.56/18.66 fof(f592,plain,(
% 143.56/18.66 ![X,C]: ((~iext(uri_rdf_type,X,C)|icext(C,X))&(iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 143.56/18.66 inference(NNF_transformation,[status(thm)],[f25])).
% 143.56/18.66 fof(f593,plain,(
% 143.56/18.66 (![X,C]: (~iext(uri_rdf_type,X,C)|icext(C,X)))&(![X,C]: (iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 143.56/18.66 inference(miniscoping,[status(thm)],[f592])).
% 143.56/18.66 fof(f594,plain,(
% 143.56/18.66 ![X0,X1]: (~iext(uri_rdf_type,X0,X1)|icext(X1,X0))),
% 143.56/18.66 inference(cnf_transformation,[status(thm)],[f593])).
% 143.56/18.66 fof(f1749,plain,(
% 143.56/18.66 ![X,Y]: ((~iext(uri_owl_differentFrom,X,Y)|~X=Y)&(iext(uri_owl_differentFrom,X,Y)|X=Y))),
% 143.56/18.66 inference(NNF_transformation,[status(thm)],[f345])).
% 143.56/18.66 fof(f1750,plain,(
% 143.56/18.66 (![X,Y]: (~iext(uri_owl_differentFrom,X,Y)|~X=Y))&(![X,Y]: (iext(uri_owl_differentFrom,X,Y)|X=Y))),
% 143.56/18.66 inference(miniscoping,[status(thm)],[f1749])).
% 143.56/18.66 fof(f1751,plain,(
% 143.56/18.66 ![X0,X1]: (~iext(uri_owl_differentFrom,X0,X1)|~X0=X1)),
% 143.56/18.66 inference(cnf_transformation,[status(thm)],[f1750])).
% 143.56/18.66 fof(f2016,plain,(
% 143.56/18.66 ![P]: (icext(uri_owl_FunctionalProperty,P)<=>(ip(P)&(![X,Y1,Y2]: ((~iext(P,X,Y1)|~iext(P,X,Y2))|Y1=Y2))))),
% 143.56/18.66 inference(pre_NNF_transformation,[status(thm)],[f393])).
% 143.56/18.66 fof(f2017,plain,(
% 143.56/18.66 ![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)))))),
% 143.56/18.66 inference(NNF_transformation,[status(thm)],[f2016])).
% 143.56/18.66 fof(f2018,plain,(
% 143.56/18.66 (![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)))))),
% 143.56/18.66 inference(miniscoping,[status(thm)],[f2017])).
% 143.56/18.66 fof(f2019,plain,(
% 143.56/18.66 (![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)))))),
% 143.56/18.68 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])).
% 143.56/18.68 fof(f2021,plain,(
% 143.56/18.68 ![X0,X1,X2,X3]: (~icext(uri_owl_FunctionalProperty,X0)|~iext(X0,X1,X2)|~iext(X0,X1,X3)|X2=X3)),
% 143.56/18.68 inference(cnf_transformation,[status(thm)],[f2019])).
% 143.56/18.68 fof(f2126,plain,(
% 143.56/18.68 ![P,A1,A2]: ((((~ir(A1)|~ip(P))|~ir(A2))|iext(P,A1,A2))|(?[Z]: ((iext(uri_owl_sourceIndividual,Z,A1)&iext(uri_owl_assertionProperty,Z,P))&iext(uri_owl_targetIndividual,Z,A2))))),
% 143.56/18.68 inference(pre_NNF_transformation,[status(thm)],[f405])).
% 143.56/18.68 fof(f2127,plain,(
% 143.56/18.68 ![P,A1,A2]: ((((~ir(A1)|~ip(P))|~ir(A2))|iext(P,A1,A2))|((iext(uri_owl_sourceIndividual,sK198_skl(A2,A1,P),A1)&iext(uri_owl_assertionProperty,sK198_skl(A2,A1,P),P))&iext(uri_owl_targetIndividual,sK198_skl(A2,A1,P),A2)))),
% 143.56/18.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK198_skl]),skolemize(Z,sK198_skl(A2,A1,P))],[f2126])).
% 143.56/18.68 fof(f2128,plain,(
% 143.56/18.68 ![X0,X1,X2]: (~ir(X0)|~ip(X1)|~ir(X2)|iext(X1,X0,X2)|iext(uri_owl_sourceIndividual,sK198_skl(X2,X0,X1),X0))),
% 143.56/18.68 inference(cnf_transformation,[status(thm)],[f2127])).
% 143.56/18.68 fof(f2129,plain,(
% 143.56/18.68 ![X0,X1,X2]: (~ir(X0)|~ip(X1)|~ir(X2)|iext(X1,X0,X2)|iext(uri_owl_assertionProperty,sK198_skl(X2,X0,X1),X1))),
% 143.56/18.68 inference(cnf_transformation,[status(thm)],[f2127])).
% 143.56/18.68 fof(f2130,plain,(
% 143.56/18.68 ![X0,X1,X2]: (~ir(X0)|~ip(X1)|~ir(X2)|iext(X1,X0,X2)|iext(uri_owl_targetIndividual,sK198_skl(X2,X0,X1),X2))),
% 143.56/18.68 inference(cnf_transformation,[status(thm)],[f2127])).
% 143.56/18.68 fof(f2405,plain,(
% 143.56/18.68 (![X0]: ((~iext(uri_owl_sourceIndividual,X0,uri_ex_s)|~iext(uri_owl_assertionProperty,X0,uri_ex_p))|~iext(uri_owl_targetIndividual,X0,uri_ex_o2)))),
% 143.56/18.68 inference(pre_NNF_transformation,[status(thm)],[f560])).
% 143.56/18.68 fof(f2406,plain,(
% 143.56/18.68 ![X0]: (~iext(uri_owl_sourceIndividual,X0,uri_ex_s)|~iext(uri_owl_assertionProperty,X0,uri_ex_p)|~iext(uri_owl_targetIndividual,X0,uri_ex_o2))),
% 143.56/18.68 inference(cnf_transformation,[status(thm)],[f2405])).
% 143.56/18.68 fof(f2407,plain,(
% 143.56/18.68 iext(uri_rdf_type,uri_ex_p,uri_owl_FunctionalProperty)),
% 143.56/18.68 inference(cnf_transformation,[status(thm)],[f561])).
% 143.56/18.68 fof(f2408,plain,(
% 143.56/18.68 iext(uri_ex_p,uri_ex_s,uri_ex_o1)),
% 143.56/18.68 inference(cnf_transformation,[status(thm)],[f561])).
% 143.56/18.68 fof(f2409,plain,(
% 143.56/18.68 iext(uri_owl_differentFrom,uri_ex_o2,uri_ex_o1)),
% 143.56/18.68 inference(cnf_transformation,[status(thm)],[f561])).
% 143.56/18.68 fof(f2517,plain,(
% 143.56/18.68 ![X0]: (~iext(uri_owl_differentFrom,X0,X0))),
% 143.56/18.68 inference(destructive_equality_resolution,[status(thm)],[f1751])).
% 143.56/18.68 fof(f2543,plain,(
% 143.56/18.68 ![X0,X1,X2]: (~ip(X0)|~ir(X1)|iext(X0,X2,X1)|iext(uri_owl_sourceIndividual,sK198_skl(X1,X2,X0),X2))),
% 143.56/18.68 inference(forward_subsumption_resolution,[status(thm)],[f2128,f565])).
% 143.56/18.68 fof(f2544,plain,(
% 143.56/18.68 ![X0,X1,X2]: (~ip(X0)|~ir(X1)|iext(X0,X2,X1)|iext(uri_owl_assertionProperty,sK198_skl(X1,X2,X0),X0))),
% 143.56/18.68 inference(forward_subsumption_resolution,[status(thm)],[f2129,f565])).
% 143.56/18.68 fof(f2545,plain,(
% 143.56/18.68 ![X0,X1,X2]: (~ip(X0)|~ir(X1)|iext(X0,X2,X1)|iext(uri_owl_targetIndividual,sK198_skl(X1,X2,X0),X1))),
% 143.56/18.68 inference(forward_subsumption_resolution,[status(thm)],[f2130,f565])).
% 143.56/18.68 fof(f2549,plain,(
% 143.56/18.68 ip(uri_ex_p)),
% 143.56/18.68 inference(resolution,[status(thm)],[f564,f2408])).
% 143.56/18.68 fof(f2583,plain,(
% 143.56/18.68 icext(uri_owl_FunctionalProperty,uri_ex_p)),
% 143.56/18.68 inference(resolution,[status(thm)],[f594,f2407])).
% 143.56/18.68 fof(f9807,plain,(
% 143.56/18.68 ![X0,X1,X2]: (~iext(uri_ex_p,X0,X1)|~iext(uri_ex_p,X0,X2)|X1=X2)),
% 143.56/18.68 inference(resolution,[status(thm)],[f2021,f2583])).
% 143.56/18.68 fof(f9879,plain,(
% 143.56/18.68 ![X0]: (~iext(uri_ex_p,uri_ex_s,X0)|X0=uri_ex_o1)),
% 143.56/18.68 inference(resolution,[status(thm)],[f9807,f2408])).
% 143.56/18.68 fof(f10650,plain,(
% 143.56/18.68 ![X0,X1]: (~ir(X0)|iext(uri_ex_p,X1,X0)|iext(uri_owl_sourceIndividual,sK198_skl(X0,X1,uri_ex_p),X1))),
% 143.56/18.68 inference(resolution,[status(thm)],[f2543,f2549])).
% 143.56/18.68 fof(f10691,plain,(
% 143.56/18.68 ![X0,X1]: (iext(uri_ex_p,X0,X1)|iext(uri_owl_sourceIndividual,sK198_skl(X1,X0,uri_ex_p),X0))),
% 143.56/18.68 inference(forward_subsumption_resolution,[status(thm)],[f10650,f565])).
% 143.56/18.68 fof(f10695,plain,(
% 143.56/18.68 ![X0]: (iext(uri_ex_p,uri_ex_s,X0)|~iext(uri_owl_assertionProperty,sK198_skl(X0,uri_ex_s,uri_ex_p),uri_ex_p)|~iext(uri_owl_targetIndividual,sK198_skl(X0,uri_ex_s,uri_ex_p),uri_ex_o2))),
% 143.56/18.77 inference(resolution,[status(thm)],[f10691,f2406])).
% 143.56/18.77 fof(f10983,plain,(
% 143.56/18.77 ![X0,X1]: (~ir(X0)|iext(uri_ex_p,X1,X0)|iext(uri_owl_assertionProperty,sK198_skl(X0,X1,uri_ex_p),uri_ex_p))),
% 143.56/18.77 inference(resolution,[status(thm)],[f2544,f2549])).
% 143.56/18.77 fof(f11024,plain,(
% 143.56/18.77 ![X0]: (iext(uri_ex_p,uri_ex_s,X0)|~iext(uri_owl_targetIndividual,sK198_skl(X0,uri_ex_s,uri_ex_p),uri_ex_o2))),
% 143.56/18.77 inference(backward_subsumption_resolution,[status(thm)],[f10695,f11025])).
% 143.56/18.77 fof(f11025,plain,(
% 143.56/18.77 ![X0,X1]: (iext(uri_ex_p,X0,X1)|iext(uri_owl_assertionProperty,sK198_skl(X1,X0,uri_ex_p),uri_ex_p))),
% 143.56/18.77 inference(forward_subsumption_resolution,[status(thm)],[f10983,f565])).
% 143.56/18.77 fof(f11067,plain,(
% 143.56/18.77 ![X0,X1]: (~ir(X0)|iext(uri_ex_p,X1,X0)|iext(uri_owl_targetIndividual,sK198_skl(X0,X1,uri_ex_p),X0))),
% 143.56/18.77 inference(resolution,[status(thm)],[f2545,f2549])).
% 143.56/18.77 fof(f11108,plain,(
% 143.56/18.77 ![X0,X1]: (iext(uri_ex_p,X0,X1)|iext(uri_owl_targetIndividual,sK198_skl(X1,X0,uri_ex_p),X1))),
% 143.56/18.77 inference(forward_subsumption_resolution,[status(thm)],[f11067,f565])).
% 143.56/18.77 fof(f11645,plain,(
% 143.56/18.77 iext(uri_ex_p,uri_ex_s,uri_ex_o2)|iext(uri_ex_p,uri_ex_s,uri_ex_o2)),
% 143.56/18.77 inference(resolution,[status(thm)],[f11108,f11024])).
% 143.56/18.77 fof(f11651,plain,(
% 143.56/18.77 iext(uri_ex_p,uri_ex_s,uri_ex_o2)),
% 143.56/18.77 inference(duplicate_literals_removal,[status(thm)],[f11645])).
% 143.56/18.77 fof(f11978,plain,(
% 143.56/18.77 uri_ex_o2=uri_ex_o1),
% 143.56/18.77 inference(resolution,[status(thm)],[f11651,f9879])).
% 143.56/18.77 fof(f11990,plain,(
% 143.56/18.77 iext(uri_owl_differentFrom,uri_ex_o2,uri_ex_o2)),
% 143.56/18.77 inference(backward_demodulation,[status(thm)],[f11978,f2409])).
% 143.56/18.77 fof(f11991,plain,(
% 143.56/18.77 $false),
% 143.56/18.77 inference(forward_subsumption_resolution,[status(thm)],[f11990,f2517])).
% 143.56/18.77 % SZS output end CNFRefutation for theBenchmark.p
% 36.64/18.81 % Elapsed time: 18.428021 seconds
% 36.64/18.81 % CPU time: 145.506248 seconds
% 36.64/18.81 % Total memory used: 535.768 MB
% 36.64/18.81 % Net memory used: 506.387 MB
%------------------------------------------------------------------------------