%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWB016+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 : n015.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:06 PM UTC 2026
% Result : Theorem 167.52s 21.77s
% Output : CNFRefutation 167.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 32
% Syntax : Number of formulae : 133 ( 29 unt; 15 def)
% Number of atoms : 397 ( 0 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 428 ( 164 ~; 165 |; 67 &)
% ( 23 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 22 ( 21 usr; 16 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 10 con; 0-2 aty)
% Number of variables : 162 ( 150 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [S,P,O] :
( iext(P,S,O)
=> ip(P) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,axiom,
iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [C] :
( ic(C)
=> iext(uri_rdfs_subClassOf,C,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [P] :
( ip(P)
=> iext(uri_rdfs_subPropertyOf,P,P) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [X] :
( idc(X)
=> ic(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f88,axiom,
! [X] :
( ioap(X)
=> ip(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f140,axiom,
idc(uri_rdfs_Literal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f202,axiom,
! [X,Y] :
( iext(uri_owl_equivalentClass,X,Y)
=> ( ic(Y)
& ic(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f203,axiom,
ip(uri_owl_equivalentClass),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f222,axiom,
ioap(uri_rdfs_isDefinedBy),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f342,axiom,
! [P,C] :
( iext(uri_rdfs_range,P,C)
<=> ( ! [X,Y] :
( iext(P,X,Y)
=> icext(C,Y) )
& ip(C)
& ip(P) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f343,axiom,
! [C1,C2] :
( iext(uri_rdfs_subClassOf,C1,C2)
<=> ( ! [X] :
( icext(C1,X)
=> icext(C2,X) )
& ic(C2)
& ic(C1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f344,axiom,
! [P1,P2] :
( iext(uri_rdfs_subPropertyOf,P1,P2)
<=> ( ! [X,Y] :
( iext(P1,X,Y)
=> iext(P2,X,Y) )
& ip(P2)
& ip(P1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f351,axiom,
! [C1,C2] :
( iext(uri_owl_equivalentClass,C1,C2)
<=> ( ! [X] :
( icext(C1,X)
<=> icext(C2,X) )
& ic(C2)
& ic(C1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f460,axiom,
idc(uri_xsd_string),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f464,axiom,
idc(uri_xsd_unsignedByte),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f559,conjecture,
iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,uri_rdfs_subClassOf),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f560,negated_conjecture,
~ iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,uri_rdfs_subClassOf),
inference(negated_conjecture,[status(cth)],[f559]) ).
fof(f561,plain,
! [S,P,O] :
( ip(P)
| ~ iext(P,S,O) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f562,plain,
! [P] :
( ip(P)
| ! [S,O] : ~ iext(P,S,O) ),
inference(miniscoping,[status(thm)],[f561]) ).
fof(f563,plain,
! [X0,X1,X2] :
( ip(X0)
| ~ iext(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f562]) ).
fof(f627,plain,
iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f658,plain,
! [C] :
( iext(uri_rdfs_subClassOf,C,C)
| ~ ic(C) ),
inference(pre_NNF_transformation,[status(thm)],[f70]) ).
fof(f659,plain,
! [X0] :
( iext(uri_rdfs_subClassOf,X0,X0)
| ~ ic(X0) ),
inference(cnf_transformation,[status(thm)],[f658]) ).
fof(f669,plain,
! [P] :
( iext(uri_rdfs_subPropertyOf,P,P)
| ~ ip(P) ),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f670,plain,
! [X0] :
( iext(uri_rdfs_subPropertyOf,X0,X0)
| ~ ip(X0) ),
inference(cnf_transformation,[status(thm)],[f669]) ).
fof(f688,plain,
! [X] :
( ic(X)
| ~ idc(X) ),
inference(pre_NNF_transformation,[status(thm)],[f85]) ).
fof(f689,plain,
! [X0] :
( ic(X0)
| ~ idc(X0) ),
inference(cnf_transformation,[status(thm)],[f688]) ).
fof(f697,plain,
! [X] :
( ip(X)
| ~ ioap(X) ),
inference(pre_NNF_transformation,[status(thm)],[f88]) ).
fof(f698,plain,
! [X0] :
( ip(X0)
| ~ ioap(X0) ),
inference(cnf_transformation,[status(thm)],[f697]) ).
fof(f815,plain,
idc(uri_rdfs_Literal),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f931,plain,
! [X,Y] :
( ( ic(Y)
& ic(X) )
| ~ iext(uri_owl_equivalentClass,X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f202]) ).
fof(f932,plain,
! [X0,X1] :
( ic(X0)
| ~ iext(uri_owl_equivalentClass,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f931]) ).
fof(f933,plain,
! [X0,X1] :
( ic(X1)
| ~ iext(uri_owl_equivalentClass,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f931]) ).
fof(f934,plain,
ip(uri_owl_equivalentClass),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f971,plain,
ioap(uri_rdfs_isDefinedBy),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f1721,plain,
! [P,C] :
( iext(uri_rdfs_range,P,C)
<=> ( ! [X,Y] :
( icext(C,Y)
| ~ iext(P,X,Y) )
& ip(C)
& ip(P) ) ),
inference(pre_NNF_transformation,[status(thm)],[f342]) ).
fof(f1722,plain,
! [P,C] :
( ( ? [X,Y] :
( ~ icext(C,Y)
& iext(P,X,Y) )
| ~ ip(C)
| ~ ip(P)
| iext(uri_rdfs_range,P,C) )
& ( ( ! [X,Y] :
( icext(C,Y)
| ~ iext(P,X,Y) )
& ip(C)
& ip(P) )
| ~ iext(uri_rdfs_range,P,C) ) ),
inference(NNF_transformation,[status(thm)],[f1721]) ).
fof(f1723,plain,
( ! [P,C] :
( ? [Y] :
( ~ icext(C,Y)
& ? [X] : iext(P,X,Y) )
| ~ ip(C)
| ~ ip(P)
| iext(uri_rdfs_range,P,C) )
& ! [P,C] :
( ( ! [Y] :
( icext(C,Y)
| ! [X] : ~ iext(P,X,Y) )
& ip(C)
& ip(P) )
| ~ iext(uri_rdfs_range,P,C) ) ),
inference(miniscoping,[status(thm)],[f1722]) ).
fof(f1724,plain,
( ! [P,C] :
( ( ~ icext(C,sK113_skl(C,P))
& iext(P,sK114_skl(C,P),sK113_skl(C,P)) )
| ~ ip(C)
| ~ ip(P)
| iext(uri_rdfs_range,P,C) )
& ! [P,C] :
( ( ! [Y] :
( icext(C,Y)
| ! [X] : ~ iext(P,X,Y) )
& ip(C)
& ip(P) )
| ~ iext(uri_rdfs_range,P,C) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK113_skl,sK114_skl]),skolemize(Y,sK113_skl(C,P)),skolemize(X,sK114_skl(C,P))],[f1723]) ).
fof(f1726,plain,
! [X0,X1] :
( ip(X1)
| ~ iext(uri_rdfs_range,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1724]) ).
fof(f1730,plain,
! [C1,C2] :
( iext(uri_rdfs_subClassOf,C1,C2)
<=> ( ! [X] :
( icext(C2,X)
| ~ icext(C1,X) )
& ic(C2)
& ic(C1) ) ),
inference(pre_NNF_transformation,[status(thm)],[f343]) ).
fof(f1731,plain,
! [C1,C2] :
( ( ? [X] :
( ~ icext(C2,X)
& icext(C1,X) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_rdfs_subClassOf,C1,C2) )
& ( ( ! [X] :
( icext(C2,X)
| ~ icext(C1,X) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_rdfs_subClassOf,C1,C2) ) ),
inference(NNF_transformation,[status(thm)],[f1730]) ).
fof(f1732,plain,
( ! [C1,C2] :
( ? [X] :
( ~ icext(C2,X)
& icext(C1,X) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_rdfs_subClassOf,C1,C2) )
& ! [C1,C2] :
( ( ! [X] :
( icext(C2,X)
| ~ icext(C1,X) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_rdfs_subClassOf,C1,C2) ) ),
inference(miniscoping,[status(thm)],[f1731]) ).
fof(f1733,plain,
( ! [C1,C2] :
( ( ~ icext(C2,sK115_skl(C2,C1))
& icext(C1,sK115_skl(C2,C1)) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_rdfs_subClassOf,C1,C2) )
& ! [C1,C2] :
( ( ! [X] :
( icext(C2,X)
| ~ icext(C1,X) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_rdfs_subClassOf,C1,C2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK115_skl]),skolemize(X,sK115_skl(C2,C1))],[f1732]) ).
fof(f1737,plain,
! [X0,X1] :
( icext(X0,sK115_skl(X1,X0))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1733]) ).
fof(f1738,plain,
! [X0,X1] :
( ~ icext(X1,sK115_skl(X1,X0))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1733]) ).
fof(f1739,plain,
! [P1,P2] :
( iext(uri_rdfs_subPropertyOf,P1,P2)
<=> ( ! [X,Y] :
( iext(P2,X,Y)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) ) ),
inference(pre_NNF_transformation,[status(thm)],[f344]) ).
fof(f1740,plain,
! [P1,P2] :
( ( ? [X,Y] :
( ~ iext(P2,X,Y)
& iext(P1,X,Y) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_rdfs_subPropertyOf,P1,P2) )
& ( ( ! [X,Y] :
( iext(P2,X,Y)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_rdfs_subPropertyOf,P1,P2) ) ),
inference(NNF_transformation,[status(thm)],[f1739]) ).
fof(f1741,plain,
( ! [P1,P2] :
( ? [X,Y] :
( ~ iext(P2,X,Y)
& iext(P1,X,Y) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_rdfs_subPropertyOf,P1,P2) )
& ! [P1,P2] :
( ( ! [X,Y] :
( iext(P2,X,Y)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_rdfs_subPropertyOf,P1,P2) ) ),
inference(miniscoping,[status(thm)],[f1740]) ).
fof(f1742,plain,
( ! [P1,P2] :
( ( ~ iext(P2,sK116_skl(P2,P1),sK117_skl(P2,P1))
& iext(P1,sK116_skl(P2,P1),sK117_skl(P2,P1)) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_rdfs_subPropertyOf,P1,P2) )
& ! [P1,P2] :
( ( ! [X,Y] :
( iext(P2,X,Y)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_rdfs_subPropertyOf,P1,P2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK116_skl,sK117_skl]),skolemize(X,sK116_skl(P2,P1)),skolemize(Y,sK117_skl(P2,P1))],[f1741]) ).
fof(f1746,plain,
! [X0,X1] :
( iext(X0,sK116_skl(X1,X0),sK117_skl(X1,X0))
| ~ ip(X1)
| ~ ip(X0)
| iext(uri_rdfs_subPropertyOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1742]) ).
fof(f1747,plain,
! [X0,X1] :
( ~ iext(X1,sK116_skl(X1,X0),sK117_skl(X1,X0))
| ~ ip(X1)
| ~ ip(X0)
| iext(uri_rdfs_subPropertyOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1742]) ).
fof(f1804,plain,
! [C1,C2] :
( ( ? [X] :
( ( icext(C2,X)
| icext(C1,X) )
& ( ~ icext(C2,X)
| ~ icext(C1,X) ) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_owl_equivalentClass,C1,C2) )
& ( ( ! [X] :
( ( ~ icext(C2,X)
| icext(C1,X) )
& ( icext(C2,X)
| ~ icext(C1,X) ) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_owl_equivalentClass,C1,C2) ) ),
inference(NNF_transformation,[status(thm)],[f351]) ).
fof(f1805,plain,
( ! [C1,C2] :
( ? [X] :
( ( icext(C2,X)
| icext(C1,X) )
& ( ~ icext(C2,X)
| ~ icext(C1,X) ) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_owl_equivalentClass,C1,C2) )
& ! [C1,C2] :
( ( ! [X] :
( ~ icext(C2,X)
| icext(C1,X) )
& ! [X] :
( icext(C2,X)
| ~ icext(C1,X) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_owl_equivalentClass,C1,C2) ) ),
inference(miniscoping,[status(thm)],[f1804]) ).
fof(f1806,plain,
( ! [C1,C2] :
( ( ( icext(C2,sK123_skl(C2,C1))
| icext(C1,sK123_skl(C2,C1)) )
& ( ~ icext(C2,sK123_skl(C2,C1))
| ~ icext(C1,sK123_skl(C2,C1)) ) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_owl_equivalentClass,C1,C2) )
& ! [C1,C2] :
( ( ! [X] :
( ~ icext(C2,X)
| icext(C1,X) )
& ! [X] :
( icext(C2,X)
| ~ icext(C1,X) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_owl_equivalentClass,C1,C2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK123_skl]),skolemize(X,sK123_skl(C2,C1))],[f1805]) ).
fof(f1809,plain,
! [X0,X1,X2] :
( icext(X1,X2)
| ~ icext(X0,X2)
| ~ iext(uri_owl_equivalentClass,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1806]) ).
fof(f2213,plain,
idc(uri_xsd_string),
inference(cnf_transformation,[status(thm)],[f460]) ).
fof(f2219,plain,
idc(uri_xsd_unsignedByte),
inference(cnf_transformation,[status(thm)],[f464]) ).
fof(f2404,plain,
~ iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,uri_rdfs_subClassOf),
inference(cnf_transformation,[status(thm)],[f560]) ).
fof(f2779,definition,
( sQ2_spl
<=> ip(uri_rdfs_isDefinedBy) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f2781,plain,
( sQ2_spl
| ~ ip(uri_rdfs_isDefinedBy) ),
inference(component_clause,[status(thm)],[f2779]) ).
fof(f2925,plain,
! [X0] :
( iext(uri_rdfs_subClassOf,X0,X0)
| ~ idc(X0) ),
inference(resolution,[status(thm)],[f689,f659]) ).
fof(f2931,plain,
iext(uri_rdfs_subClassOf,uri_xsd_unsignedByte,uri_xsd_unsignedByte),
inference(resolution,[status(thm)],[f2925,f2219]) ).
fof(f3051,plain,
iext(uri_rdfs_subClassOf,uri_xsd_string,uri_xsd_string),
inference(resolution,[status(thm)],[f2925,f2213]) ).
fof(f3239,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal),
inference(resolution,[status(thm)],[f815,f2925]) ).
fof(f3638,plain,
iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,uri_owl_equivalentClass),
inference(resolution,[status(thm)],[f670,f934]) ).
fof(f11285,definition,
! [X0,X1] :
( sQ621_spl
<=> ~ iext(uri_rdfs_subClassOf,X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ621_spl])],[split_symbol_definition]) ).
fof(f11286,plain,
! [X0,X1] :
( ~ sQ621_spl
| ~ iext(uri_rdfs_subClassOf,X0,X1) ),
inference(component_clause,[status(thm)],[f11285]) ).
fof(f11290,plain,
( ~ sQ621_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2931,f11286]) ).
fof(f11348,plain,
~ sQ621_spl,
inference(contradiction_clause,[status(thm)],[f11290]) ).
fof(f19362,definition,
( sQ1092_spl
<=> ip(uri_rdfs_Class) ),
introduced(definition,[new_symbols(definition,[sQ1092_spl])],[split_symbol_definition]) ).
fof(f19364,plain,
( sQ1092_spl
| ~ ip(uri_rdfs_Class) ),
inference(component_clause,[status(thm)],[f19362]) ).
fof(f19424,plain,
! [X0] :
( sQ1092_spl
| ~ iext(uri_rdfs_range,X0,uri_rdfs_Class) ),
inference(resolution,[status(thm)],[f19364,f1726]) ).
fof(f20161,plain,
( iext(uri_owl_equivalentClass,sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass),sK117_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass))
| ~ ip(uri_rdfs_subClassOf)
| ~ ip(uri_owl_equivalentClass) ),
inference(resolution,[status(thm)],[f1746,f2404]) ).
fof(f20174,definition,
( sQ1221_spl
<=> ip(uri_owl_equivalentClass) ),
introduced(definition,[new_symbols(definition,[sQ1221_spl])],[split_symbol_definition]) ).
fof(f20176,plain,
( sQ1221_spl
| ~ ip(uri_owl_equivalentClass) ),
inference(component_clause,[status(thm)],[f20174]) ).
fof(f20177,definition,
( sQ1222_spl
<=> ip(uri_rdfs_subClassOf) ),
introduced(definition,[new_symbols(definition,[sQ1222_spl])],[split_symbol_definition]) ).
fof(f20179,plain,
( sQ1222_spl
| ~ ip(uri_rdfs_subClassOf) ),
inference(component_clause,[status(thm)],[f20177]) ).
fof(f20180,definition,
( sQ1223_spl
<=> iext(uri_owl_equivalentClass,sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass),sK117_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass)) ),
introduced(definition,[new_symbols(definition,[sQ1223_spl])],[split_symbol_definition]) ).
fof(f20181,plain,
( ~ sQ1223_spl
| iext(uri_owl_equivalentClass,sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass),sK117_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass)) ),
inference(component_clause,[status(thm)],[f20180]) ).
fof(f20183,plain,
( sQ1223_spl
| ~ sQ1222_spl
| ~ sQ1221_spl ),
inference(split_clause,[status(thm)],[f20161,f20174,f20177,f20180]) ).
fof(f20194,plain,
( sQ1221_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20176,f934]) ).
fof(f20195,plain,
sQ1221_spl,
inference(contradiction_clause,[status(thm)],[f20194]) ).
fof(f20196,plain,
! [X0,X1] :
( ~ iext(X1,sK116_skl(X1,X0),sK117_skl(X1,X0))
| ~ ip(X0)
| iext(uri_rdfs_subPropertyOf,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1747,f563]) ).
fof(f20199,plain,
( ~ iext(uri_rdfs_subClassOf,sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass),sK117_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass))
| ~ ip(uri_owl_equivalentClass) ),
inference(resolution,[status(thm)],[f20196,f2404]) ).
fof(f20212,definition,
( sQ1228_spl
<=> iext(uri_rdfs_subClassOf,sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass),sK117_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass)) ),
introduced(definition,[new_symbols(definition,[sQ1228_spl])],[split_symbol_definition]) ).
fof(f20215,plain,
( ~ sQ1228_spl
| ~ sQ1221_spl ),
inference(split_clause,[status(thm)],[f20199,f20174,f20212]) ).
fof(f20222,plain,
! [X0,X1] :
( sQ1222_spl
| ~ iext(uri_rdfs_subClassOf,X0,X1) ),
inference(resolution,[status(thm)],[f20179,f563]) ).
fof(f20238,plain,
( sQ1222_spl
| sQ621_spl ),
inference(split_clause,[status(thm)],[f20222,f11285,f20177]) ).
fof(f20239,plain,
( ~ sQ1223_spl
| ic(sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass)) ),
inference(resolution,[status(thm)],[f20181,f932]) ).
fof(f20240,plain,
! [X0] :
( ~ sQ1223_spl
| icext(sK117_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass),X0)
| ~ icext(sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass),X0) ),
inference(resolution,[status(thm)],[f20181,f1809]) ).
fof(f20288,plain,
! [X0] :
( ~ sQ1223_spl
| ~ ic(X0)
| ~ ic(sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass))
| iext(uri_rdfs_subClassOf,sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass),X0)
| icext(sK117_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass),sK115_skl(X0,sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass))) ),
inference(resolution,[status(thm)],[f20240,f1737]) ).
fof(f20290,definition,
! [X0] :
( sQ1234_spl
<=> ( ~ ic(X0)
| iext(uri_rdfs_subClassOf,sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass),X0)
| icext(sK117_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass),sK115_skl(X0,sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass))) ) ),
introduced(definition,[new_symbols(definition,[sQ1234_spl])],[split_symbol_definition]) ).
fof(f20291,plain,
! [X0] :
( ~ sQ1234_spl
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass),X0)
| icext(sK117_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass),sK115_skl(X0,sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass))) ),
inference(component_clause,[status(thm)],[f20290]) ).
fof(f20293,definition,
( sQ1235_spl
<=> ic(sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass)) ),
introduced(definition,[new_symbols(definition,[sQ1235_spl])],[split_symbol_definition]) ).
fof(f20295,plain,
( sQ1235_spl
| ~ ic(sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass)) ),
inference(component_clause,[status(thm)],[f20293]) ).
fof(f20296,plain,
( ~ sQ1223_spl
| ~ sQ1235_spl
| sQ1234_spl ),
inference(split_clause,[status(thm)],[f20288,f20290,f20293,f20180]) ).
fof(f20304,plain,
( sQ1235_spl
| ~ sQ1223_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20295,f20239]) ).
fof(f20305,plain,
( sQ1235_spl
| ~ sQ1223_spl ),
inference(contradiction_clause,[status(thm)],[f20304]) ).
fof(f20313,definition,
( sQ1239_spl
<=> ic(sK117_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass)) ),
introduced(definition,[new_symbols(definition,[sQ1239_spl])],[split_symbol_definition]) ).
fof(f20315,plain,
( sQ1239_spl
| ~ ic(sK117_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass)) ),
inference(component_clause,[status(thm)],[f20313]) ).
fof(f20489,definition,
! [X0] :
( sQ1255_spl
<=> ~ iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,X0) ),
introduced(definition,[new_symbols(definition,[sQ1255_spl])],[split_symbol_definition]) ).
fof(f20490,plain,
! [X0] :
( ~ sQ1255_spl
| ~ iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,X0) ),
inference(component_clause,[status(thm)],[f20489]) ).
fof(f20539,plain,
( ~ sQ1255_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3638,f20490]) ).
fof(f20554,plain,
~ sQ1255_spl,
inference(contradiction_clause,[status(thm)],[f20539]) ).
fof(f20675,plain,
( sQ1092_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f627,f19424]) ).
fof(f20681,plain,
sQ1092_spl,
inference(contradiction_clause,[status(thm)],[f20675]) ).
fof(f20779,plain,
( ~ sQ1223_spl
| ic(sK117_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass)) ),
inference(resolution,[status(thm)],[f20181,f933]) ).
fof(f20780,plain,
( ~ sQ1223_spl
| sQ1239_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20779,f20315]) ).
fof(f20781,plain,
( ~ sQ1223_spl
| sQ1239_spl ),
inference(contradiction_clause,[status(thm)],[f20780]) ).
fof(f20798,plain,
( sQ2_spl
| ~ ioap(uri_rdfs_isDefinedBy) ),
inference(resolution,[status(thm)],[f2781,f698]) ).
fof(f20802,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20798,f971]) ).
fof(f20803,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f20802]) ).
fof(f22580,definition,
( sQ1598_spl
<=> idc(uri_xsd_string) ),
introduced(definition,[new_symbols(definition,[sQ1598_spl])],[split_symbol_definition]) ).
fof(f22582,plain,
( sQ1598_spl
| ~ idc(uri_xsd_string) ),
inference(component_clause,[status(thm)],[f22580]) ).
fof(f22584,definition,
! [X1] :
( sQ1599_spl
<=> ~ iext(uri_rdfs_subClassOf,uri_xsd_string,X1) ),
introduced(definition,[new_symbols(definition,[sQ1599_spl])],[split_symbol_definition]) ).
fof(f22585,plain,
! [X0] :
( ~ sQ1599_spl
| ~ iext(uri_rdfs_subClassOf,uri_xsd_string,X0) ),
inference(component_clause,[status(thm)],[f22584]) ).
fof(f22599,plain,
( sQ1598_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22582,f2213]) ).
fof(f22600,plain,
sQ1598_spl,
inference(contradiction_clause,[status(thm)],[f22599]) ).
fof(f22601,plain,
( ~ sQ1599_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3051,f22585]) ).
fof(f22610,plain,
~ sQ1599_spl,
inference(contradiction_clause,[status(thm)],[f22601]) ).
fof(f22730,definition,
( sQ1615_spl
<=> idc(uri_rdfs_Literal) ),
introduced(definition,[new_symbols(definition,[sQ1615_spl])],[split_symbol_definition]) ).
fof(f22732,plain,
( sQ1615_spl
| ~ idc(uri_rdfs_Literal) ),
inference(component_clause,[status(thm)],[f22730]) ).
fof(f22734,definition,
! [X1] :
( sQ1616_spl
<=> ~ iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X1) ),
introduced(definition,[new_symbols(definition,[sQ1616_spl])],[split_symbol_definition]) ).
fof(f22735,plain,
! [X0] :
( ~ sQ1616_spl
| ~ iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X0) ),
inference(component_clause,[status(thm)],[f22734]) ).
fof(f22749,plain,
( sQ1615_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22732,f815]) ).
fof(f22750,plain,
sQ1615_spl,
inference(contradiction_clause,[status(thm)],[f22749]) ).
fof(f22752,plain,
( ~ sQ1616_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3239,f22735]) ).
fof(f22761,plain,
~ sQ1616_spl,
inference(contradiction_clause,[status(thm)],[f22752]) ).
fof(f22785,plain,
( ~ sQ1234_spl
| ~ ic(sK117_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass))
| ~ ic(sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass))
| iext(uri_rdfs_subClassOf,sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass),sK117_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass))
| ~ ic(sK117_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass))
| iext(uri_rdfs_subClassOf,sK116_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass),sK117_skl(uri_rdfs_subClassOf,uri_owl_equivalentClass)) ),
inference(resolution,[status(thm)],[f20291,f1738]) ).
fof(f22789,plain,
( ~ sQ1234_spl
| ~ sQ1235_spl
| ~ sQ1239_spl
| sQ1228_spl ),
inference(split_clause,[status(thm)],[f22785,f20212,f20313,f20293,f20290]) ).
fof(f22794,plain,
$false,
inference(sat_refutation,[status(thm)],[f11348,f20183,f20195,f20215,f20238,f20296,f20305,f20554,f20681,f20781,f20803,f22600,f22610,f22750,f22761,f22789]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWB016+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.45 % Computer : n015.cluster.edu
% 0.17/0.45 % Model : x86_64 x86_64
% 0.17/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.45 % Memory : 8046.5625MB
% 0.17/0.45 % OS : Linux 6.8.0-71-generic
% 0.17/0.45 % CPULimit : 300
% 0.17/0.45 % WCLimit : 300
% 0.17/0.45 % DateTime : Mon Sep 21 07:42:36 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.26/0.59 % Drodi V4.1.1
% 167.52/21.77 % Refutation found
% 167.52/21.77 % SZS status Theorem for theBenchmark: Theorem is valid
% 167.52/21.77 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 138.07/22.97 % Elapsed time: 22.287299 seconds
% 138.07/22.97 % CPU time: 164.544437 seconds
% 138.07/22.97 % Total memory used: 401.314 MB
% 138.07/22.97 % Net memory used: 380.810 MB
%------------------------------------------------------------------------------