%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWB027+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:11 PM UTC 2026
% Result : Timeout 295.87s 37.84s
% Output : None
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 7
% Syntax : Number of formulae : 62 ( 13 unt; 0 def)
% Number of atoms : 303 ( 17 equ)
% Maximal formula atoms : 18 ( 4 avg)
% Number of connectives : 381 ( 140 ~; 151 |; 79 &)
% ( 8 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 12 con; 0-4 aty)
% Number of variables : 184 ( 162 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f25,axiom,
! [X,C] :
( iext(uri_rdf_type,X,C)
<=> icext(C,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f354,axiom,
! [X,Y] :
( iext(uri_owl_sameAs,X,Y)
<=> X = Y ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f389,axiom,
! [P,S1,P1,S2,P2] :
( ( iext(uri_rdf_rest,S2,uri_rdf_nil)
& iext(uri_rdf_first,S2,P2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,P1) )
=> ( iext(uri_owl_propertyChainAxiom,P,S1)
<=> ( ! [Y0,Y1,Y2] :
( ( iext(P2,Y1,Y2)
& iext(P1,Y0,Y1) )
=> iext(P,Y0,Y2) )
& ip(P2)
& ip(P1)
& ip(P) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f391,axiom,
! [P1,P2] :
( iext(uri_owl_inverseOf,P1,P2)
<=> ( ! [X,Y] :
( iext(P1,X,Y)
<=> iext(P2,Y,X) )
& ip(P2)
& ip(P1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f394,axiom,
! [P] :
( icext(uri_owl_InverseFunctionalProperty,P)
<=> ( ! [X1,X2,Y] :
( ( iext(P,X2,Y)
& iext(P,X1,Y) )
=> X1 = X2 )
& ip(P) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f559,conjecture,
iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f560,negated_conjecture,
~ iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),
inference(negated_conjecture,[status(cth)],[f559]) ).
fof(f561,axiom,
? [BNODE_l1,BNODE_l2,BNODE_v] :
( iext(uri_owl_inverseOf,BNODE_v,uri_ex_p)
& iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l2,BNODE_v)
& iext(uri_rdf_rest,BNODE_l1,BNODE_l2)
& iext(uri_rdf_first,BNODE_l1,uri_ex_p)
& iext(uri_owl_propertyChainAxiom,uri_owl_sameAs,BNODE_l1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f592,plain,
! [X,C] :
( ( ~ icext(C,X)
| iext(uri_rdf_type,X,C) )
& ( icext(C,X)
| ~ iext(uri_rdf_type,X,C) ) ),
inference(NNF_transformation,[status(thm)],[f25]) ).
fof(f593,plain,
( ! [X,C] :
( ~ icext(C,X)
| iext(uri_rdf_type,X,C) )
& ! [X,C] :
( icext(C,X)
| ~ iext(uri_rdf_type,X,C) ) ),
inference(miniscoping,[status(thm)],[f592]) ).
fof(f595,plain,
! [X0,X1] :
( ~ icext(X1,X0)
| iext(uri_rdf_type,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f593]) ).
fof(f1832,plain,
! [X,Y] :
( ( X != Y
| iext(uri_owl_sameAs,X,Y) )
& ( X = Y
| ~ iext(uri_owl_sameAs,X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f354]) ).
fof(f1833,plain,
( ! [X,Y] :
( X != Y
| iext(uri_owl_sameAs,X,Y) )
& ! [X,Y] :
( X = Y
| ~ iext(uri_owl_sameAs,X,Y) ) ),
inference(miniscoping,[status(thm)],[f1832]) ).
fof(f1834,plain,
! [X0,X1] :
( X0 = X1
| ~ iext(uri_owl_sameAs,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1833]) ).
fof(f1975,plain,
! [P,S1,P1,S2,P2] :
( ( iext(uri_owl_propertyChainAxiom,P,S1)
<=> ( ! [Y0,Y1,Y2] :
( iext(P,Y0,Y2)
| ~ iext(P2,Y1,Y2)
| ~ iext(P1,Y0,Y1) )
& ip(P2)
& ip(P1)
& ip(P) ) )
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,P2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,P1) ),
inference(pre_NNF_transformation,[status(thm)],[f389]) ).
fof(f1976,plain,
! [P,S1,P1,S2,P2] :
( ( ( ? [Y0,Y1,Y2] :
( ~ iext(P,Y0,Y2)
& iext(P2,Y1,Y2)
& iext(P1,Y0,Y1) )
| ~ ip(P2)
| ~ ip(P1)
| ~ ip(P)
| iext(uri_owl_propertyChainAxiom,P,S1) )
& ( ( ! [Y0,Y1,Y2] :
( iext(P,Y0,Y2)
| ~ iext(P2,Y1,Y2)
| ~ iext(P1,Y0,Y1) )
& ip(P2)
& ip(P1)
& ip(P) )
| ~ iext(uri_owl_propertyChainAxiom,P,S1) ) )
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,P2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,P1) ),
inference(NNF_transformation,[status(thm)],[f1975]) ).
fof(f1977,plain,
! [S1,P1,P2] :
( ( ! [P] :
( ? [Y0,Y2] :
( ~ iext(P,Y0,Y2)
& ? [Y1] :
( iext(P2,Y1,Y2)
& iext(P1,Y0,Y1) ) )
| ~ ip(P2)
| ~ ip(P1)
| ~ ip(P)
| iext(uri_owl_propertyChainAxiom,P,S1) )
& ! [P] :
( ( ! [Y0,Y2] :
( iext(P,Y0,Y2)
| ! [Y1] :
( ~ iext(P2,Y1,Y2)
| ~ iext(P1,Y0,Y1) ) )
& ip(P2)
& ip(P1)
& ip(P) )
| ~ iext(uri_owl_propertyChainAxiom,P,S1) ) )
| ! [S2] :
( ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,P2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,P1) ) ),
inference(miniscoping,[status(thm)],[f1976]) ).
fof(f1978,plain,
! [S1,P1,P2] :
( ( ! [P] :
( ( ~ iext(P,sK159_skl(P,P2,P1,S1),sK160_skl(P,P2,P1,S1))
& iext(P2,sK161_skl(P,P2,P1,S1),sK160_skl(P,P2,P1,S1))
& iext(P1,sK159_skl(P,P2,P1,S1),sK161_skl(P,P2,P1,S1)) )
| ~ ip(P2)
| ~ ip(P1)
| ~ ip(P)
| iext(uri_owl_propertyChainAxiom,P,S1) )
& ! [P] :
( ( ! [Y0,Y2] :
( iext(P,Y0,Y2)
| ! [Y1] :
( ~ iext(P2,Y1,Y2)
| ~ iext(P1,Y0,Y1) ) )
& ip(P2)
& ip(P1)
& ip(P) )
| ~ iext(uri_owl_propertyChainAxiom,P,S1) ) )
| ! [S2] :
( ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,P2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,P1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK159_skl,sK160_skl,sK161_skl]),skolemize(Y0,sK159_skl(P,P2,P1,S1)),skolemize(Y2,sK160_skl(P,P2,P1,S1)),skolemize(Y1,sK161_skl(P,P2,P1,S1))],[f1977]) ).
fof(f1980,plain,
! [X0,X1,X2,X3,X4] :
( ip(X1)
| ~ iext(uri_owl_propertyChainAxiom,X4,X0)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1978]) ).
fof(f1982,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( iext(X4,X5,X7)
| ~ iext(X3,X6,X7)
| ~ iext(X1,X5,X6)
| ~ iext(uri_owl_propertyChainAxiom,X4,X0)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1978]) ).
fof(f1999,plain,
! [P1,P2] :
( ( ? [X,Y] :
( ( iext(P2,Y,X)
| iext(P1,X,Y) )
& ( ~ iext(P2,Y,X)
| ~ iext(P1,X,Y) ) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_owl_inverseOf,P1,P2) )
& ( ( ! [X,Y] :
( ( ~ iext(P2,Y,X)
| iext(P1,X,Y) )
& ( iext(P2,Y,X)
| ~ iext(P1,X,Y) ) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_owl_inverseOf,P1,P2) ) ),
inference(NNF_transformation,[status(thm)],[f391]) ).
fof(f2000,plain,
( ! [P1,P2] :
( ? [X,Y] :
( ( iext(P2,Y,X)
| iext(P1,X,Y) )
& ( ~ iext(P2,Y,X)
| ~ iext(P1,X,Y) ) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_owl_inverseOf,P1,P2) )
& ! [P1,P2] :
( ( ! [X,Y] :
( ~ iext(P2,Y,X)
| iext(P1,X,Y) )
& ! [X,Y] :
( iext(P2,Y,X)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_owl_inverseOf,P1,P2) ) ),
inference(miniscoping,[status(thm)],[f1999]) ).
fof(f2001,plain,
( ! [P1,P2] :
( ( ( 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))
| ~ iext(P1,sK166_skl(P2,P1),sK167_skl(P2,P1)) ) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_owl_inverseOf,P1,P2) )
& ! [P1,P2] :
( ( ! [X,Y] :
( ~ iext(P2,Y,X)
| iext(P1,X,Y) )
& ! [X,Y] :
( iext(P2,Y,X)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_owl_inverseOf,P1,P2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK166_skl,sK167_skl]),skolemize(X,sK166_skl(P2,P1)),skolemize(Y,sK167_skl(P2,P1))],[f2000]) ).
fof(f2005,plain,
! [X0,X1,X2,X3] :
( ~ iext(X1,X3,X2)
| iext(X0,X2,X3)
| ~ iext(uri_owl_inverseOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2001]) ).
fof(f2025,plain,
! [P] :
( icext(uri_owl_InverseFunctionalProperty,P)
<=> ( ! [X1,X2,Y] :
( X1 = X2
| ~ iext(P,X2,Y)
| ~ iext(P,X1,Y) )
& ip(P) ) ),
inference(pre_NNF_transformation,[status(thm)],[f394]) ).
fof(f2026,plain,
! [P] :
( ( ? [X1,X2,Y] :
( X1 != X2
& iext(P,X2,Y)
& iext(P,X1,Y) )
| ~ ip(P)
| icext(uri_owl_InverseFunctionalProperty,P) )
& ( ( ! [X1,X2,Y] :
( X1 = X2
| ~ iext(P,X2,Y)
| ~ iext(P,X1,Y) )
& ip(P) )
| ~ icext(uri_owl_InverseFunctionalProperty,P) ) ),
inference(NNF_transformation,[status(thm)],[f2025]) ).
fof(f2027,plain,
( ! [P] :
( ? [X1,X2] :
( X1 != X2
& ? [Y] :
( iext(P,X2,Y)
& iext(P,X1,Y) ) )
| ~ ip(P)
| icext(uri_owl_InverseFunctionalProperty,P) )
& ! [P] :
( ( ! [X1,X2] :
( X1 = X2
| ! [Y] :
( ~ iext(P,X2,Y)
| ~ iext(P,X1,Y) ) )
& ip(P) )
| ~ icext(uri_owl_InverseFunctionalProperty,P) ) ),
inference(miniscoping,[status(thm)],[f2026]) ).
fof(f2028,plain,
( ! [P] :
( ( sK173_skl(P) != sK174_skl(P)
& iext(P,sK174_skl(P),sK175_skl(P))
& iext(P,sK173_skl(P),sK175_skl(P)) )
| ~ ip(P)
| icext(uri_owl_InverseFunctionalProperty,P) )
& ! [P] :
( ( ! [X1,X2] :
( X1 = X2
| ! [Y] :
( ~ iext(P,X2,Y)
| ~ iext(P,X1,Y) ) )
& ip(P) )
| ~ icext(uri_owl_InverseFunctionalProperty,P) ) ),
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]) ).
fof(f2031,plain,
! [X0] :
( iext(X0,sK173_skl(X0),sK175_skl(X0))
| ~ ip(X0)
| icext(uri_owl_InverseFunctionalProperty,X0) ),
inference(cnf_transformation,[status(thm)],[f2028]) ).
fof(f2032,plain,
! [X0] :
( iext(X0,sK174_skl(X0),sK175_skl(X0))
| ~ ip(X0)
| icext(uri_owl_InverseFunctionalProperty,X0) ),
inference(cnf_transformation,[status(thm)],[f2028]) ).
fof(f2033,plain,
! [X0] :
( sK173_skl(X0) != sK174_skl(X0)
| ~ ip(X0)
| icext(uri_owl_InverseFunctionalProperty,X0) ),
inference(cnf_transformation,[status(thm)],[f2028]) ).
fof(f2405,plain,
~ iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),
inference(cnf_transformation,[status(thm)],[f560]) ).
fof(f2406,plain,
? [BNODE_v] :
( iext(uri_owl_inverseOf,BNODE_v,uri_ex_p)
& ? [BNODE_l2] :
( iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l2,BNODE_v)
& ? [BNODE_l1] :
( iext(uri_rdf_rest,BNODE_l1,BNODE_l2)
& iext(uri_rdf_first,BNODE_l1,uri_ex_p)
& iext(uri_owl_propertyChainAxiom,uri_owl_sameAs,BNODE_l1) ) ) ),
inference(miniscoping,[status(thm)],[f561]) ).
fof(f2407,plain,
( iext(uri_owl_inverseOf,sK199_skl,uri_ex_p)
& iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)
& iext(uri_rdf_first,sK200_skl,sK199_skl)
& iext(uri_rdf_rest,sK201_skl,sK200_skl)
& iext(uri_rdf_first,sK201_skl,uri_ex_p)
& iext(uri_owl_propertyChainAxiom,uri_owl_sameAs,sK201_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK199_skl,sK200_skl,sK201_skl]),skolemize(BNODE_v,sK199_skl),skolemize(BNODE_l2,sK200_skl),skolemize(BNODE_l1,sK201_skl)],[f2406]) ).
fof(f2408,plain,
iext(uri_owl_propertyChainAxiom,uri_owl_sameAs,sK201_skl),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2409,plain,
iext(uri_rdf_first,sK201_skl,uri_ex_p),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2410,plain,
iext(uri_rdf_rest,sK201_skl,sK200_skl),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2411,plain,
iext(uri_rdf_first,sK200_skl,sK199_skl),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2412,plain,
iext(uri_rdf_rest,sK200_skl,uri_rdf_nil),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2413,plain,
iext(uri_owl_inverseOf,sK199_skl,uri_ex_p),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f4080,plain,
! [X0,X1,X2] :
( ip(uri_ex_p)
| ~ iext(uri_owl_propertyChainAxiom,X2,sK201_skl)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sK201_skl,X0) ),
inference(resolution,[status(thm)],[f1980,f2409]) ).
fof(f4082,plain,
! [X0,X1] :
( ip(uri_ex_p)
| ~ iext(uri_owl_propertyChainAxiom,X1,sK201_skl)
| ~ iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK200_skl,X0) ),
inference(resolution,[status(thm)],[f4080,f2410]) ).
fof(f4083,plain,
! [X0,X1] :
( ip(uri_ex_p)
| ~ iext(uri_owl_propertyChainAxiom,X1,sK201_skl)
| ~ iext(uri_rdf_first,sK200_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4082,f2412]) ).
fof(f4382,plain,
! [X0,X1,X2,X3,X4,X5] :
( iext(X2,X3,X5)
| ~ iext(X1,X4,X5)
| ~ iext(uri_ex_p,X3,X4)
| ~ iext(uri_owl_propertyChainAxiom,X2,sK201_skl)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sK201_skl,X0) ),
inference(resolution,[status(thm)],[f1982,f2409]) ).
fof(f4384,plain,
! [X0,X1,X2,X3,X4] :
( iext(X1,X2,X4)
| ~ iext(X0,X3,X4)
| ~ iext(uri_ex_p,X2,X3)
| ~ iext(uri_owl_propertyChainAxiom,X1,sK201_skl)
| ~ iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK200_skl,X0) ),
inference(resolution,[status(thm)],[f4382,f2410]) ).
fof(f4385,plain,
! [X0,X1,X2,X3,X4] :
( iext(X1,X2,X4)
| ~ iext(X0,X3,X4)
| ~ iext(uri_ex_p,X2,X3)
| ~ iext(uri_owl_propertyChainAxiom,X1,sK201_skl)
| ~ iext(uri_rdf_first,sK200_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4384,f2412]) ).
fof(f4420,plain,
! [X0] :
( ip(uri_ex_p)
| ~ iext(uri_owl_propertyChainAxiom,X0,sK201_skl) ),
inference(resolution,[status(thm)],[f4083,f2411]) ).
fof(f4541,plain,
ip(uri_ex_p),
inference(resolution,[status(thm)],[f4420,f2408]) ).
fof(f4543,plain,
( iext(uri_ex_p,sK174_skl(uri_ex_p),sK175_skl(uri_ex_p))
| icext(uri_owl_InverseFunctionalProperty,uri_ex_p) ),
inference(resolution,[status(thm)],[f4541,f2032]) ).
fof(f4544,plain,
( iext(uri_ex_p,sK173_skl(uri_ex_p),sK175_skl(uri_ex_p))
| icext(uri_owl_InverseFunctionalProperty,uri_ex_p) ),
inference(resolution,[status(thm)],[f4541,f2031]) ).
fof(f4545,plain,
( sK173_skl(uri_ex_p) != sK174_skl(uri_ex_p)
| icext(uri_owl_InverseFunctionalProperty,uri_ex_p) ),
inference(resolution,[status(thm)],[f4541,f2033]) ).
fof(f4604,plain,
! [X0,X1,X2,X3] :
( iext(X0,X1,X3)
| ~ iext(sK199_skl,X2,X3)
| ~ iext(uri_ex_p,X1,X2)
| ~ iext(uri_owl_propertyChainAxiom,X0,sK201_skl) ),
inference(resolution,[status(thm)],[f4385,f2411]) ).
fof(f10738,plain,
! [X0,X1,X2] :
( iext(uri_owl_sameAs,X0,X2)
| ~ iext(sK199_skl,X1,X2)
| ~ iext(uri_ex_p,X0,X1) ),
inference(resolution,[status(thm)],[f4604,f2408]) ).
fof(f10748,plain,
! [X0,X1] :
( ~ iext(uri_ex_p,X1,X0)
| iext(sK199_skl,X0,X1) ),
inference(resolution,[status(thm)],[f2413,f2005]) ).
fof(f10758,plain,
( icext(uri_owl_InverseFunctionalProperty,uri_ex_p)
| iext(sK199_skl,sK175_skl(uri_ex_p),sK174_skl(uri_ex_p)) ),
inference(resolution,[status(thm)],[f10748,f4543]) ).
fof(f10991,plain,
! [X0] :
( icext(uri_owl_InverseFunctionalProperty,uri_ex_p)
| iext(uri_owl_sameAs,sK173_skl(uri_ex_p),X0)
| ~ iext(sK199_skl,sK175_skl(uri_ex_p),X0) ),
inference(resolution,[status(thm)],[f10738,f4544]) ).
fof(f10993,plain,
( icext(uri_owl_InverseFunctionalProperty,uri_ex_p)
| icext(uri_owl_InverseFunctionalProperty,uri_ex_p)
| iext(uri_owl_sameAs,sK173_skl(uri_ex_p),sK174_skl(uri_ex_p)) ),
inference(resolution,[status(thm)],[f10991,f10758]) ).
fof(f10995,plain,
( icext(uri_owl_InverseFunctionalProperty,uri_ex_p)
| iext(uri_owl_sameAs,sK173_skl(uri_ex_p),sK174_skl(uri_ex_p)) ),
inference(duplicate_literals_removal,[status(thm)],[f10993]) ).
fof(f10997,plain,
( sK173_skl(uri_ex_p) = sK174_skl(uri_ex_p)
| icext(uri_owl_InverseFunctionalProperty,uri_ex_p) ),
inference(resolution,[status(thm)],[f10995,f1834]) ).
fof(f11003,plain,
icext(uri_owl_InverseFunctionalProperty,uri_ex_p),
inference(forward_subsumption_resolution,[status(thm)],[f10997,f4545]) ).
fof(f11006,plain,
iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),
inference(resolution,[status(thm)],[f11003,f595]) ).
fof(f11007,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f11006,f2405]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB027+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n006.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 07:41:42 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.40 % Drodi V4.1.1
% 295.87/37.84 % Refutation found
% 295.87/37.84 % SZS status Theorem for theBenchmark: Theorem is valid
% 295.87/37.84 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 74.40/37.94 % Elapsed time: 37.568466 seconds
% 74.40/37.94 % CPU time: 296.958704 seconds
% 74.40/37.94 % Total memory used: 460.684 MB
% 74.40/37.94 % Net memory used: 433.656 MB
%------------------------------------------------------------------------------