%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWB026+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 : n019.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:10 PM UTC 2026
% Result : Theorem 274.19s 35.06s
% Output : CNFRefutation 134.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 7
% Syntax : Number of formulae : 59 ( 13 unt; 0 def)
% Number of atoms : 244 ( 36 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 276 ( 91 ~; 102 |; 70 &)
% ( 9 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 21 ( 21 usr; 15 con; 0-3 aty)
% Number of variables : 132 ( 112 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f25,axiom,
! [X,C] :
( iext(uri_rdf_type,X,C)
<=> icext(C,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [P,C,X,Y] :
( ( iext(P,X,Y)
& iext(uri_rdfs_domain,P,C) )
=> icext(C,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f295,axiom,
! [Z,S1,A1] :
( ( iext(uri_rdf_rest,S1,uri_rdf_nil)
& iext(uri_rdf_first,S1,A1) )
=> ( iext(uri_owl_oneOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> X = A1 )
& ic(Z) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f341,axiom,
! [P,C] :
( iext(uri_rdfs_domain,P,C)
<=> ( ! [X,Y] :
( iext(P,X,Y)
=> icext(C,X) )
& ic(C)
& ip(P) ) ),
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_x1,BNODE_x2,BNODE_l1,BNODE_l2] :
( iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l2,uri_ex_u)
& iext(uri_owl_oneOf,BNODE_x2,BNODE_l2)
& iext(uri_rdfs_range,uri_ex_p,BNODE_x2)
& iext(uri_rdf_rest,BNODE_l1,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l1,uri_ex_w)
& iext(uri_owl_oneOf,BNODE_x1,BNODE_l1)
& iext(uri_rdfs_domain,uri_ex_p,BNODE_x1) ),
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(f625,plain,
! [P,C,X,Y] :
( icext(C,X)
| ~ iext(P,X,Y)
| ~ iext(uri_rdfs_domain,P,C) ),
inference(pre_NNF_transformation,[status(thm)],[f52]) ).
fof(f626,plain,
! [C,X] :
( icext(C,X)
| ! [P] :
( ! [Y] : ~ iext(P,X,Y)
| ~ iext(uri_rdfs_domain,P,C) ) ),
inference(miniscoping,[status(thm)],[f625]) ).
fof(f627,plain,
! [X0,X1,X2,X3] :
( icext(X1,X2)
| ~ iext(X0,X2,X3)
| ~ iext(uri_rdfs_domain,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f626]) ).
fof(f1211,plain,
! [Z,S1,A1] :
( ( iext(uri_owl_oneOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> X = A1 )
& ic(Z) ) )
| ~ iext(uri_rdf_rest,S1,uri_rdf_nil)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(pre_NNF_transformation,[status(thm)],[f295]) ).
fof(f1212,plain,
! [Z,S1,A1] :
( ( ( ? [X] :
( ( X = A1
| icext(Z,X) )
& ( X != A1
| ~ icext(Z,X) ) )
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,S1) )
& ( ( ! [X] :
( ( X != A1
| icext(Z,X) )
& ( X = A1
| ~ icext(Z,X) ) )
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S1,uri_rdf_nil)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(NNF_transformation,[status(thm)],[f1211]) ).
fof(f1213,plain,
! [S1,A1] :
( ( ! [Z] :
( ? [X] :
( ( X = A1
| icext(Z,X) )
& ( X != A1
| ~ icext(Z,X) ) )
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,S1) )
& ! [Z] :
( ( ! [X] :
( X != A1
| icext(Z,X) )
& ! [X] :
( X = A1
| ~ icext(Z,X) )
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S1,uri_rdf_nil)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(miniscoping,[status(thm)],[f1212]) ).
fof(f1214,plain,
! [S1,A1] :
( ( ! [Z] :
( ( ( sK10_skl(Z,A1,S1) = A1
| icext(Z,sK10_skl(Z,A1,S1)) )
& ( sK10_skl(Z,A1,S1) != A1
| ~ icext(Z,sK10_skl(Z,A1,S1)) ) )
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,S1) )
& ! [Z] :
( ( ! [X] :
( X != A1
| icext(Z,X) )
& ! [X] :
( X = A1
| ~ icext(Z,X) )
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S1,uri_rdf_nil)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X,sK10_skl(Z,A1,S1))],[f1213]) ).
fof(f1216,plain,
! [X0,X1,X2,X3] :
( X3 = X1
| ~ icext(X2,X3)
| ~ iext(uri_owl_oneOf,X2,X0)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1214]) ).
fof(f1713,plain,
! [P,C] :
( iext(uri_rdfs_domain,P,C)
<=> ( ! [X,Y] :
( icext(C,X)
| ~ iext(P,X,Y) )
& ic(C)
& ip(P) ) ),
inference(pre_NNF_transformation,[status(thm)],[f341]) ).
fof(f1714,plain,
! [P,C] :
( ( ? [X,Y] :
( ~ icext(C,X)
& iext(P,X,Y) )
| ~ ic(C)
| ~ ip(P)
| iext(uri_rdfs_domain,P,C) )
& ( ( ! [X,Y] :
( icext(C,X)
| ~ iext(P,X,Y) )
& ic(C)
& ip(P) )
| ~ iext(uri_rdfs_domain,P,C) ) ),
inference(NNF_transformation,[status(thm)],[f1713]) ).
fof(f1715,plain,
( ! [P,C] :
( ? [X] :
( ~ icext(C,X)
& ? [Y] : iext(P,X,Y) )
| ~ ic(C)
| ~ ip(P)
| iext(uri_rdfs_domain,P,C) )
& ! [P,C] :
( ( ! [X] :
( icext(C,X)
| ! [Y] : ~ iext(P,X,Y) )
& ic(C)
& ip(P) )
| ~ iext(uri_rdfs_domain,P,C) ) ),
inference(miniscoping,[status(thm)],[f1714]) ).
fof(f1716,plain,
( ! [P,C] :
( ( ~ icext(C,sK111_skl(C,P))
& iext(P,sK111_skl(C,P),sK112_skl(C,P)) )
| ~ ic(C)
| ~ ip(P)
| iext(uri_rdfs_domain,P,C) )
& ! [P,C] :
( ( ! [X] :
( icext(C,X)
| ! [Y] : ~ iext(P,X,Y) )
& ic(C)
& ip(P) )
| ~ iext(uri_rdfs_domain,P,C) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK111_skl,sK112_skl]),skolemize(X,sK111_skl(C,P)),skolemize(Y,sK112_skl(C,P))],[f1715]) ).
fof(f1717,plain,
! [X0,X1] :
( ip(X0)
| ~ iext(uri_rdfs_domain,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1716]) ).
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_l2] :
( iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l2,uri_ex_u)
& ? [BNODE_x2] :
( iext(uri_owl_oneOf,BNODE_x2,BNODE_l2)
& iext(uri_rdfs_range,uri_ex_p,BNODE_x2)
& ? [BNODE_l1] :
( iext(uri_rdf_rest,BNODE_l1,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l1,uri_ex_w)
& ? [BNODE_x1] :
( iext(uri_owl_oneOf,BNODE_x1,BNODE_l1)
& iext(uri_rdfs_domain,uri_ex_p,BNODE_x1) ) ) ) ),
inference(miniscoping,[status(thm)],[f561]) ).
fof(f2407,plain,
( iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)
& iext(uri_rdf_first,sK199_skl,uri_ex_u)
& iext(uri_owl_oneOf,sK200_skl,sK199_skl)
& iext(uri_rdfs_range,uri_ex_p,sK200_skl)
& iext(uri_rdf_rest,sK201_skl,uri_rdf_nil)
& iext(uri_rdf_first,sK201_skl,uri_ex_w)
& iext(uri_owl_oneOf,sK202_skl,sK201_skl)
& iext(uri_rdfs_domain,uri_ex_p,sK202_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK199_skl,sK200_skl,sK201_skl,sK202_skl]),skolemize(BNODE_l2,sK199_skl),skolemize(BNODE_x2,sK200_skl),skolemize(BNODE_l1,sK201_skl),skolemize(BNODE_x1,sK202_skl)],[f2406]) ).
fof(f2408,plain,
iext(uri_rdfs_domain,uri_ex_p,sK202_skl),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2409,plain,
iext(uri_owl_oneOf,sK202_skl,sK201_skl),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2410,plain,
iext(uri_rdf_first,sK201_skl,uri_ex_w),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2411,plain,
iext(uri_rdf_rest,sK201_skl,uri_rdf_nil),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f3554,plain,
! [X0,X1] :
( X1 = uri_ex_w
| ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sK201_skl)
| ~ iext(uri_rdf_rest,sK201_skl,uri_rdf_nil) ),
inference(resolution,[status(thm)],[f1216,f2410]) ).
fof(f3556,plain,
! [X0,X1] :
( X1 = uri_ex_w
| ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sK201_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f3554,f2411]) ).
fof(f10821,plain,
! [X0,X1] :
( icext(sK202_skl,X0)
| ~ iext(uri_ex_p,X0,X1) ),
inference(resolution,[status(thm)],[f2408,f627]) ).
fof(f10823,plain,
ip(uri_ex_p),
inference(resolution,[status(thm)],[f2408,f1717]) ).
fof(f10839,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)],[f10823,f2032]) ).
fof(f10840,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)],[f10823,f2031]) ).
fof(f10841,plain,
( sK173_skl(uri_ex_p) != sK174_skl(uri_ex_p)
| icext(uri_owl_InverseFunctionalProperty,uri_ex_p) ),
inference(resolution,[status(thm)],[f10823,f2033]) ).
fof(f10860,plain,
( icext(sK202_skl,sK174_skl(uri_ex_p))
| icext(uri_owl_InverseFunctionalProperty,uri_ex_p) ),
inference(resolution,[status(thm)],[f10839,f10821]) ).
fof(f10899,plain,
( icext(sK202_skl,sK173_skl(uri_ex_p))
| icext(uri_owl_InverseFunctionalProperty,uri_ex_p) ),
inference(resolution,[status(thm)],[f10840,f10821]) ).
fof(f10925,plain,
! [X0] :
( X0 = uri_ex_w
| ~ icext(sK202_skl,X0) ),
inference(resolution,[status(thm)],[f2409,f3556]) ).
fof(f10934,plain,
( icext(uri_owl_InverseFunctionalProperty,uri_ex_p)
| sK173_skl(uri_ex_p) = uri_ex_w ),
inference(resolution,[status(thm)],[f10925,f10899]) ).
fof(f10935,plain,
( icext(uri_owl_InverseFunctionalProperty,uri_ex_p)
| sK174_skl(uri_ex_p) = uri_ex_w ),
inference(resolution,[status(thm)],[f10925,f10860]) ).
fof(f10938,plain,
( iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty)
| sK173_skl(uri_ex_p) = uri_ex_w ),
inference(resolution,[status(thm)],[f10934,f595]) ).
fof(f10939,plain,
sK173_skl(uri_ex_p) = uri_ex_w,
inference(forward_subsumption_resolution,[status(thm)],[f10938,f2405]) ).
fof(f10944,plain,
( uri_ex_w != sK174_skl(uri_ex_p)
| icext(uri_owl_InverseFunctionalProperty,uri_ex_p) ),
inference(backward_demodulation,[status(thm)],[f10939,f10841]) ).
fof(f10947,plain,
( iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty)
| sK174_skl(uri_ex_p) = uri_ex_w ),
inference(resolution,[status(thm)],[f10935,f595]) ).
fof(f10948,plain,
sK174_skl(uri_ex_p) = uri_ex_w,
inference(forward_subsumption_resolution,[status(thm)],[f10947,f2405]) ).
fof(f10953,plain,
( uri_ex_w != uri_ex_w
| icext(uri_owl_InverseFunctionalProperty,uri_ex_p) ),
inference(forward_demodulation,[status(thm)],[f10948,f10944]) ).
fof(f10954,plain,
icext(uri_owl_InverseFunctionalProperty,uri_ex_p),
inference(trivial_equality_resolution,[status(thm)],[f10953]) ).
fof(f10957,plain,
iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),
inference(resolution,[status(thm)],[f10954,f595]) ).
fof(f10958,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f10957,f2405]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWB026+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n019.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 07:41:51 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.41 % Drodi V4.1.1
% 274.19/35.06 % Refutation found
% 274.19/35.06 % SZS status Theorem for theBenchmark: Theorem is valid
% 274.19/35.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 134.16/35.17 % Elapsed time: 34.792340 seconds
% 134.16/35.17 % CPU time: 275.098694 seconds
% 134.16/35.17 % Total memory used: 480.090 MB
% 134.16/35.17 % Net memory used: 453.700 MB
%------------------------------------------------------------------------------