%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWB049+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:15 PM UTC 2026
% Result : Theorem 7.92s 1.65s
% Output : CNFRefutation 7.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 12
% Syntax : Number of formulae : 55 ( 11 unt; 4 def)
% Number of atoms : 168 ( 0 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 184 ( 71 ~; 72 |; 31 &)
% ( 9 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 5 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 95 ( 89 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [S,P,O] :
( iext(P,S,O)
=> ip(P) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X] : ir(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [X,C] :
( iext(uri_rdf_type,X,C)
<=> icext(C,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f268,axiom,
! [X,Y] :
( iext(uri_owl_topObjectProperty,X,Y)
<=> ( ir(Y)
& ir(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f352,axiom,
! [P1,P2] :
( iext(uri_owl_equivalentProperty,P1,P2)
<=> ( ! [X,Y] :
( iext(P1,X,Y)
<=> iext(P2,X,Y) )
& ip(P2)
& ip(P1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f396,axiom,
! [P] :
( icext(uri_owl_ReflexiveProperty,P)
<=> ( ! [X] : iext(P,X,X)
& ip(P) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f559,conjecture,
iext(uri_rdf_type,uri_ex_p,uri_owl_ReflexiveProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f560,negated_conjecture,
~ iext(uri_rdf_type,uri_ex_p,uri_owl_ReflexiveProperty),
inference(negated_conjecture,[status(cth)],[f559]) ).
fof(f561,axiom,
iext(uri_owl_equivalentProperty,uri_ex_p,uri_owl_topObjectProperty),
file('/export/starexec/sandbox2/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(f565,plain,
! [X0] : ir(X0),
inference(cnf_transformation,[status(thm)],[f2]) ).
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(f1064,plain,
! [X,Y] :
( ( ~ ir(Y)
| ~ ir(X)
| iext(uri_owl_topObjectProperty,X,Y) )
& ( ( ir(Y)
& ir(X) )
| ~ iext(uri_owl_topObjectProperty,X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f268]) ).
fof(f1065,plain,
( ! [X,Y] :
( ~ ir(Y)
| ~ ir(X)
| iext(uri_owl_topObjectProperty,X,Y) )
& ! [X,Y] :
( ( ir(Y)
& ir(X) )
| ~ iext(uri_owl_topObjectProperty,X,Y) ) ),
inference(miniscoping,[status(thm)],[f1064]) ).
fof(f1068,plain,
! [X0,X1] :
( ~ ir(X1)
| ~ ir(X0)
| iext(uri_owl_topObjectProperty,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1065]) ).
fof(f1814,plain,
! [P1,P2] :
( ( ? [X,Y] :
( ( iext(P2,X,Y)
| iext(P1,X,Y) )
& ( ~ iext(P2,X,Y)
| ~ iext(P1,X,Y) ) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_owl_equivalentProperty,P1,P2) )
& ( ( ! [X,Y] :
( ( ~ iext(P2,X,Y)
| iext(P1,X,Y) )
& ( iext(P2,X,Y)
| ~ iext(P1,X,Y) ) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_owl_equivalentProperty,P1,P2) ) ),
inference(NNF_transformation,[status(thm)],[f352]) ).
fof(f1815,plain,
( ! [P1,P2] :
( ? [X,Y] :
( ( iext(P2,X,Y)
| iext(P1,X,Y) )
& ( ~ iext(P2,X,Y)
| ~ iext(P1,X,Y) ) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_owl_equivalentProperty,P1,P2) )
& ! [P1,P2] :
( ( ! [X,Y] :
( ~ iext(P2,X,Y)
| iext(P1,X,Y) )
& ! [X,Y] :
( iext(P2,X,Y)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_owl_equivalentProperty,P1,P2) ) ),
inference(miniscoping,[status(thm)],[f1814]) ).
fof(f1816,plain,
( ! [P1,P2] :
( ( ( 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))
| ~ iext(P1,sK124_skl(P2,P1),sK125_skl(P2,P1)) ) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_owl_equivalentProperty,P1,P2) )
& ! [P1,P2] :
( ( ! [X,Y] :
( ~ iext(P2,X,Y)
| iext(P1,X,Y) )
& ! [X,Y] :
( iext(P2,X,Y)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_owl_equivalentProperty,P1,P2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK124_skl,sK125_skl]),skolemize(X,sK124_skl(P2,P1)),skolemize(Y,sK125_skl(P2,P1))],[f1815]) ).
fof(f1820,plain,
! [X0,X1,X2,X3] :
( ~ iext(X1,X2,X3)
| iext(X0,X2,X3)
| ~ iext(uri_owl_equivalentProperty,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1816]) ).
fof(f2040,plain,
! [P] :
( ( ? [X] : ~ iext(P,X,X)
| ~ ip(P)
| icext(uri_owl_ReflexiveProperty,P) )
& ( ( ! [X] : iext(P,X,X)
& ip(P) )
| ~ icext(uri_owl_ReflexiveProperty,P) ) ),
inference(NNF_transformation,[status(thm)],[f396]) ).
fof(f2041,plain,
( ! [P] :
( ? [X] : ~ iext(P,X,X)
| ~ ip(P)
| icext(uri_owl_ReflexiveProperty,P) )
& ! [P] :
( ( ! [X] : iext(P,X,X)
& ip(P) )
| ~ icext(uri_owl_ReflexiveProperty,P) ) ),
inference(miniscoping,[status(thm)],[f2040]) ).
fof(f2042,plain,
( ! [P] :
( ~ iext(P,sK177_skl(P),sK177_skl(P))
| ~ ip(P)
| icext(uri_owl_ReflexiveProperty,P) )
& ! [P] :
( ( ! [X] : iext(P,X,X)
& ip(P) )
| ~ icext(uri_owl_ReflexiveProperty,P) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK177_skl]),skolemize(X,sK177_skl(P))],[f2041]) ).
fof(f2044,plain,
! [X0,X1] :
( iext(X0,X1,X1)
| ~ icext(uri_owl_ReflexiveProperty,X0) ),
inference(cnf_transformation,[status(thm)],[f2042]) ).
fof(f2045,plain,
! [X0] :
( ~ iext(X0,sK177_skl(X0),sK177_skl(X0))
| ~ ip(X0)
| icext(uri_owl_ReflexiveProperty,X0) ),
inference(cnf_transformation,[status(thm)],[f2042]) ).
fof(f2405,plain,
~ iext(uri_rdf_type,uri_ex_p,uri_owl_ReflexiveProperty),
inference(cnf_transformation,[status(thm)],[f560]) ).
fof(f2406,plain,
iext(uri_owl_equivalentProperty,uri_ex_p,uri_owl_topObjectProperty),
inference(cnf_transformation,[status(thm)],[f561]) ).
fof(f2669,plain,
! [X0,X1] :
( ~ ir(X1)
| iext(uri_owl_topObjectProperty,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1068,f565]) ).
fof(f2685,plain,
! [X0,X1] :
( ~ iext(uri_owl_topObjectProperty,X0,X1)
| iext(uri_ex_p,X0,X1) ),
inference(resolution,[status(thm)],[f1820,f2406]) ).
fof(f2910,plain,
! [X0] :
( ~ iext(X0,sK177_skl(X0),sK177_skl(X0))
| icext(uri_owl_ReflexiveProperty,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2045,f564]) ).
fof(f2911,plain,
! [X0,X1] :
( iext(X0,X1,X1)
| ~ iext(X0,sK177_skl(X0),sK177_skl(X0)) ),
inference(resolution,[status(thm)],[f2910,f2044]) ).
fof(f2912,plain,
! [X0] :
( iext(uri_rdf_type,X0,uri_owl_ReflexiveProperty)
| ~ iext(X0,sK177_skl(X0),sK177_skl(X0)) ),
inference(resolution,[status(thm)],[f2910,f595]) ).
fof(f2914,plain,
! [X0] :
( ~ iext(uri_owl_topObjectProperty,sK177_skl(uri_ex_p),sK177_skl(uri_ex_p))
| iext(uri_ex_p,X0,X0) ),
inference(resolution,[status(thm)],[f2911,f2685]) ).
fof(f2916,plain,
! [X0] :
( ~ ir(sK177_skl(uri_owl_topObjectProperty))
| iext(uri_owl_topObjectProperty,X0,X0) ),
inference(resolution,[status(thm)],[f2911,f2669]) ).
fof(f2930,definition,
! [X0] :
( sQ47_spl
<=> iext(uri_ex_p,X0,X0) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f2931,plain,
! [X0] :
( ~ sQ47_spl
| iext(uri_ex_p,X0,X0) ),
inference(component_clause,[status(thm)],[f2930]) ).
fof(f2933,definition,
( sQ48_spl
<=> iext(uri_owl_topObjectProperty,sK177_skl(uri_ex_p),sK177_skl(uri_ex_p)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f2935,plain,
( sQ48_spl
| ~ iext(uri_owl_topObjectProperty,sK177_skl(uri_ex_p),sK177_skl(uri_ex_p)) ),
inference(component_clause,[status(thm)],[f2933]) ).
fof(f2936,plain,
( ~ sQ48_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f2914,f2930,f2933]) ).
fof(f2937,definition,
! [X0] :
( sQ49_spl
<=> iext(uri_owl_topObjectProperty,X0,X0) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f2938,plain,
! [X0] :
( ~ sQ49_spl
| iext(uri_owl_topObjectProperty,X0,X0) ),
inference(component_clause,[status(thm)],[f2937]) ).
fof(f2944,definition,
( sQ51_spl
<=> ir(sK177_skl(uri_owl_topObjectProperty)) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f2946,plain,
( sQ51_spl
| ~ ir(sK177_skl(uri_owl_topObjectProperty)) ),
inference(component_clause,[status(thm)],[f2944]) ).
fof(f2947,plain,
( ~ sQ51_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f2916,f2937,f2944]) ).
fof(f2982,plain,
~ iext(uri_ex_p,sK177_skl(uri_ex_p),sK177_skl(uri_ex_p)),
inference(resolution,[status(thm)],[f2912,f2405]) ).
fof(f2998,plain,
( ~ sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2982,f2931]) ).
fof(f2999,plain,
~ sQ47_spl,
inference(contradiction_clause,[status(thm)],[f2998]) ).
fof(f3000,plain,
( sQ48_spl
| ~ sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2935,f2938]) ).
fof(f3001,plain,
( sQ48_spl
| ~ sQ49_spl ),
inference(contradiction_clause,[status(thm)],[f3000]) ).
fof(f3002,plain,
( sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2946,f565]) ).
fof(f3003,plain,
sQ51_spl,
inference(contradiction_clause,[status(thm)],[f3002]) ).
fof(f3004,plain,
$false,
inference(sat_refutation,[status(thm)],[f2936,f2947,f2999,f3001,f3003]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWB049+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.45 % Computer : n004.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Mon Sep 21 07:43:35 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.24/0.60 % Drodi V4.1.1
% 7.92/1.65 % Refutation found
% 7.92/1.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.92/1.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.92/1.69 % Elapsed time: 1.209789 seconds
% 7.92/1.69 % CPU time: 8.274087 seconds
% 7.92/1.69 % Total memory used: 172.529 MB
% 7.92/1.69 % Net memory used: 167.891 MB
%------------------------------------------------------------------------------