%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWB046+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 : n012.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:14 PM UTC 2026
% Result : Theorem 241.81s 30.99s
% Output : CNFRefutation 243.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 7
% Syntax : Number of formulae : 55 ( 13 unt; 0 def)
% Number of atoms : 197 ( 33 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 218 ( 76 ~; 86 |; 45 &)
% ( 7 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 12 con; 0-3 aty)
% Number of variables : 110 ( 98 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [S,P,O] :
( iext(P,S,O)
=> ip(P) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
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(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,
? [X1,X0] :
( iext(uri_rdfs_domain,uri_ex_p,X1)
& iext(uri_ex_p,uri_ex_x,uri_ex_y)
& iext(uri_owl_oneOf,X1,X0)
& iext(uri_rdf_rest,X0,uri_rdf_nil)
& iext(uri_rdf_first,X0,uri_ex_x) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f562,plain,
! [S,P,O] :
( ip(P)
| ~ iext(P,S,O) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f563,plain,
! [P] :
( ip(P)
| ! [S,O] : ~ iext(P,S,O) ),
inference(miniscoping,[status(thm)],[f562]) ).
fof(f564,plain,
! [X0,X1,X2] :
( ip(X0)
| ~ iext(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f563]) ).
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(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,
? [X1] :
( iext(uri_rdfs_domain,uri_ex_p,X1)
& iext(uri_ex_p,uri_ex_x,uri_ex_y)
& ? [X0] :
( iext(uri_owl_oneOf,X1,X0)
& iext(uri_rdf_rest,X0,uri_rdf_nil)
& iext(uri_rdf_first,X0,uri_ex_x) ) ),
inference(miniscoping,[status(thm)],[f561]) ).
fof(f2407,plain,
( iext(uri_rdfs_domain,uri_ex_p,sK199_skl)
& iext(uri_ex_p,uri_ex_x,uri_ex_y)
& iext(uri_owl_oneOf,sK199_skl,sK200_skl)
& iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)
& iext(uri_rdf_first,sK200_skl,uri_ex_x) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK199_skl,sK200_skl]),skolemize(X1,sK199_skl),skolemize(X0,sK200_skl)],[f2406]) ).
fof(f2408,plain,
iext(uri_rdf_first,sK200_skl,uri_ex_x),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2409,plain,
iext(uri_rdf_rest,sK200_skl,uri_rdf_nil),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2410,plain,
iext(uri_owl_oneOf,sK199_skl,sK200_skl),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2411,plain,
iext(uri_ex_p,uri_ex_x,uri_ex_y),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f2412,plain,
iext(uri_rdfs_domain,uri_ex_p,sK199_skl),
inference(cnf_transformation,[status(thm)],[f2407]) ).
fof(f3531,plain,
! [X0,X1] :
( X1 = uri_ex_x
| ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sK200_skl)
| ~ iext(uri_rdf_rest,sK200_skl,uri_rdf_nil) ),
inference(resolution,[status(thm)],[f1216,f2408]) ).
fof(f3532,plain,
! [X0,X1] :
( X1 = uri_ex_x
| ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sK200_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f3531,f2409]) ).
fof(f10486,plain,
! [X0] :
( X0 = uri_ex_x
| ~ icext(sK199_skl,X0) ),
inference(resolution,[status(thm)],[f2410,f3532]) ).
fof(f10555,plain,
ip(uri_ex_p),
inference(resolution,[status(thm)],[f2411,f564]) ).
fof(f10560,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)],[f10555,f2032]) ).
fof(f10561,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)],[f10555,f2031]) ).
fof(f10562,plain,
( sK173_skl(uri_ex_p) != sK174_skl(uri_ex_p)
| icext(uri_owl_InverseFunctionalProperty,uri_ex_p) ),
inference(resolution,[status(thm)],[f10555,f2033]) ).
fof(f10583,plain,
! [X0,X1] :
( icext(sK199_skl,X0)
| ~ iext(uri_ex_p,X0,X1) ),
inference(resolution,[status(thm)],[f2412,f627]) ).
fof(f10634,plain,
( icext(uri_owl_InverseFunctionalProperty,uri_ex_p)
| icext(sK199_skl,sK173_skl(uri_ex_p)) ),
inference(resolution,[status(thm)],[f10583,f10561]) ).
fof(f10635,plain,
( icext(uri_owl_InverseFunctionalProperty,uri_ex_p)
| icext(sK199_skl,sK174_skl(uri_ex_p)) ),
inference(resolution,[status(thm)],[f10583,f10560]) ).
fof(f10637,plain,
( sK173_skl(uri_ex_p) = uri_ex_x
| icext(uri_owl_InverseFunctionalProperty,uri_ex_p) ),
inference(resolution,[status(thm)],[f10634,f10486]) ).
fof(f10642,plain,
( iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty)
| sK173_skl(uri_ex_p) = uri_ex_x ),
inference(resolution,[status(thm)],[f10637,f595]) ).
fof(f10643,plain,
sK173_skl(uri_ex_p) = uri_ex_x,
inference(forward_subsumption_resolution,[status(thm)],[f10642,f2405]) ).
fof(f10647,plain,
( uri_ex_x != sK174_skl(uri_ex_p)
| icext(uri_owl_InverseFunctionalProperty,uri_ex_p) ),
inference(backward_demodulation,[status(thm)],[f10643,f10562]) ).
fof(f10648,plain,
( sK174_skl(uri_ex_p) = uri_ex_x
| icext(uri_owl_InverseFunctionalProperty,uri_ex_p) ),
inference(resolution,[status(thm)],[f10635,f10486]) ).
fof(f10651,plain,
icext(uri_owl_InverseFunctionalProperty,uri_ex_p),
inference(forward_subsumption_resolution,[status(thm)],[f10648,f10647]) ).
fof(f10655,plain,
iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),
inference(resolution,[status(thm)],[f10651,f595]) ).
fof(f10656,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f10655,f2405]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWB046+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Mon Sep 21 07:43:37 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.04/0.32 % Drodi V4.1.1
% 241.81/30.99 % Refutation found
% 241.81/30.99 % SZS status Theorem for theBenchmark: Theorem is valid
% 241.81/30.99 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 243.32/31.08 % Elapsed time: 30.769814 seconds
% 243.32/31.08 % CPU time: 243.792695 seconds
% 243.32/31.08 % Total memory used: 480.958 MB
% 243.32/31.08 % Net memory used: 454.764 MB
%------------------------------------------------------------------------------