%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWB075+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 : n016.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:18 PM UTC 2026
% Result : Theorem 126.43s 16.40s
% Output : CNFRefutation 95.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 30
% Syntax : Number of formulae : 123 ( 27 unt; 11 def)
% Number of atoms : 363 ( 0 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 390 ( 150 ~; 145 |; 66 &)
% ( 23 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 20 ( 19 usr; 11 prp; 0-4 aty)
% Number of functors : 23 ( 23 usr; 19 con; 0-2 aty)
% Number of variables : 187 ( 179 !; 8 ?)
% 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(f18,axiom,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
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(f32,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f90,axiom,
! [X] :
( iodp(X)
=> ! [Y,Z] :
( iext(X,Y,Z)
=> ( lv(Z)
& ir(Y) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f91,axiom,
! [X] :
( iodp(X)
=> ip(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [X] :
( iodp(X)
<=> iext(uri_rdf_type,X,uri_owl_DatatypeProperty) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f127,axiom,
! [X] :
( icext(uri_owl_DatatypeProperty,X)
<=> iodp(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f222,axiom,
ioap(uri_rdfs_isDefinedBy),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f266,axiom,
! [X,Y] :
( iext(uri_owl_topDataProperty,X,Y)
<=> ( lv(Y)
& ir(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f267,axiom,
iodp(uri_owl_topDataProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f290,axiom,
! [Z,S1,C1,S2,C2,S3,C3] :
( ( iext(uri_rdf_rest,S3,uri_rdf_nil)
& iext(uri_rdf_first,S3,C3)
& iext(uri_rdf_rest,S2,S3)
& iext(uri_rdf_first,S2,C2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,C1) )
=> ( iext(uri_owl_unionOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( icext(C3,X)
| icext(C2,X)
| icext(C1,X) ) )
& ic(C3)
& ic(C2)
& ic(C1)
& ic(Z) ) ) ),
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(f353,axiom,
! [P1,P2] :
( iext(uri_owl_propertyDisjointWith,P1,P2)
<=> ( ! [X,Y] :
~ ( iext(P2,X,Y)
& iext(P1,X,Y) )
& ip(P2)
& ip(P1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f481,axiom,
! [X] :
~ ( icext(uri_rdf_XMLLiteral,X)
& icext(uri_xsd_anyURI,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f559,conjecture,
iext(uri_rdfs_subPropertyOf,uri_ex_p,uri_owl_topDataProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f560,negated_conjecture,
~ iext(uri_rdfs_subPropertyOf,uri_ex_p,uri_owl_topDataProperty),
inference(negated_conjecture,[status(cth)],[f559]) ).
fof(f561,axiom,
iext(uri_rdf_type,uri_ex_p,uri_owl_DatatypeProperty),
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(f585,plain,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f586,plain,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
inference(cnf_transformation,[status(thm)],[f19]) ).
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(f594,plain,
! [X0,X1] :
( icext(X1,X0)
| ~ iext(uri_rdf_type,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f593]) ).
fof(f603,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f704,plain,
! [X] :
( ! [Y,Z] :
( ( lv(Z)
& ir(Y) )
| ~ iext(X,Y,Z) )
| ~ iodp(X) ),
inference(pre_NNF_transformation,[status(thm)],[f90]) ).
fof(f706,plain,
! [X0,X1,X2] :
( ~ iext(X0,X2,X1)
| lv(X1)
| ~ iodp(X0) ),
inference(cnf_transformation,[status(thm)],[f704]) ).
fof(f707,plain,
! [X] :
( ip(X)
| ~ iodp(X) ),
inference(pre_NNF_transformation,[status(thm)],[f91]) ).
fof(f708,plain,
! [X0] :
( ~ iodp(X0)
| ip(X0) ),
inference(cnf_transformation,[status(thm)],[f707]) ).
fof(f709,plain,
! [X] :
( ( ~ iext(uri_rdf_type,X,uri_owl_DatatypeProperty)
| iodp(X) )
& ( iext(uri_rdf_type,X,uri_owl_DatatypeProperty)
| ~ iodp(X) ) ),
inference(NNF_transformation,[status(thm)],[f92]) ).
fof(f710,plain,
( ! [X] :
( ~ iext(uri_rdf_type,X,uri_owl_DatatypeProperty)
| iodp(X) )
& ! [X] :
( iext(uri_rdf_type,X,uri_owl_DatatypeProperty)
| ~ iodp(X) ) ),
inference(miniscoping,[status(thm)],[f709]) ).
fof(f712,plain,
! [X0] :
( ~ iext(uri_rdf_type,X0,uri_owl_DatatypeProperty)
| iodp(X0) ),
inference(cnf_transformation,[status(thm)],[f710]) ).
fof(f792,plain,
! [X] :
( ( ~ iodp(X)
| icext(uri_owl_DatatypeProperty,X) )
& ( iodp(X)
| ~ icext(uri_owl_DatatypeProperty,X) ) ),
inference(NNF_transformation,[status(thm)],[f127]) ).
fof(f793,plain,
( ! [X] :
( ~ iodp(X)
| icext(uri_owl_DatatypeProperty,X) )
& ! [X] :
( iodp(X)
| ~ icext(uri_owl_DatatypeProperty,X) ) ),
inference(miniscoping,[status(thm)],[f792]) ).
fof(f794,plain,
! [X0] :
( ~ icext(uri_owl_DatatypeProperty,X0)
| iodp(X0) ),
inference(cnf_transformation,[status(thm)],[f793]) ).
fof(f972,plain,
ioap(uri_rdfs_isDefinedBy),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f1058,plain,
! [X,Y] :
( ( ~ lv(Y)
| ~ ir(X)
| iext(uri_owl_topDataProperty,X,Y) )
& ( ( lv(Y)
& ir(X) )
| ~ iext(uri_owl_topDataProperty,X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f266]) ).
fof(f1059,plain,
( ! [X,Y] :
( ~ lv(Y)
| ~ ir(X)
| iext(uri_owl_topDataProperty,X,Y) )
& ! [X,Y] :
( ( lv(Y)
& ir(X) )
| ~ iext(uri_owl_topDataProperty,X,Y) ) ),
inference(miniscoping,[status(thm)],[f1058]) ).
fof(f1062,plain,
! [X0,X1] :
( ~ lv(X1)
| ~ ir(X0)
| iext(uri_owl_topDataProperty,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1059]) ).
fof(f1063,plain,
iodp(uri_owl_topDataProperty),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f1182,plain,
! [Z,S1,C1,S2,C2,S3,C3] :
( ( iext(uri_owl_unionOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( icext(C3,X)
| icext(C2,X)
| icext(C1,X) ) )
& ic(C3)
& ic(C2)
& ic(C1)
& ic(Z) ) )
| ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,C3)
| ~ iext(uri_rdf_rest,S2,S3)
| ~ iext(uri_rdf_first,S2,C2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(pre_NNF_transformation,[status(thm)],[f290]) ).
fof(f1183,definition,
! [C1,C2,C3,X] :
( sP1_prd(X,C3,C2,C1)
<=> ( icext(C3,X)
| icext(C2,X)
| icext(C1,X) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f1740,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(f1741,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)],[f1740]) ).
fof(f1742,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)],[f1741]) ).
fof(f1743,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))],[f1742]) ).
fof(f1747,plain,
! [X0,X1] :
( ~ ip(X1)
| iext(uri_rdfs_subPropertyOf,X1,X0)
| iext(X1,sK116_skl(X0,X1),sK117_skl(X0,X1))
| ~ ip(X0) ),
inference(cnf_transformation,[status(thm)],[f1743]) ).
fof(f1748,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)],[f1743]) ).
fof(f1823,plain,
! [P1,P2] :
( iext(uri_owl_propertyDisjointWith,P1,P2)
<=> ( ! [X,Y] :
( ~ iext(P2,X,Y)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) ) ),
inference(pre_NNF_transformation,[status(thm)],[f353]) ).
fof(f1824,plain,
! [P1,P2] :
( ( ? [X,Y] :
( iext(P2,X,Y)
& iext(P1,X,Y) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_owl_propertyDisjointWith,P1,P2) )
& ( ( ! [X,Y] :
( ~ iext(P2,X,Y)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_owl_propertyDisjointWith,P1,P2) ) ),
inference(NNF_transformation,[status(thm)],[f1823]) ).
fof(f1825,plain,
( ! [P1,P2] :
( ? [X,Y] :
( iext(P2,X,Y)
& iext(P1,X,Y) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_owl_propertyDisjointWith,P1,P2) )
& ! [P1,P2] :
( ( ! [X,Y] :
( ~ iext(P2,X,Y)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_owl_propertyDisjointWith,P1,P2) ) ),
inference(miniscoping,[status(thm)],[f1824]) ).
fof(f1826,plain,
( ! [P1,P2] :
( ( iext(P2,sK126_skl(P2,P1),sK127_skl(P2,P1))
& iext(P1,sK126_skl(P2,P1),sK127_skl(P2,P1)) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_owl_propertyDisjointWith,P1,P2) )
& ! [P1,P2] :
( ( ! [X,Y] :
( ~ iext(P2,X,Y)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_owl_propertyDisjointWith,P1,P2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK126_skl,sK127_skl]),skolemize(X,sK126_skl(P2,P1)),skolemize(Y,sK127_skl(P2,P1))],[f1825]) ).
fof(f1829,plain,
! [X0,X1,X2,X3] :
( ~ iext(uri_owl_propertyDisjointWith,X3,X0)
| ~ iext(X3,X1,X2)
| ~ iext(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f1826]) ).
fof(f2249,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(pre_NNF_transformation,[status(thm)],[f481]) ).
fof(f2250,plain,
! [X0] :
( ~ icext(uri_rdf_XMLLiteral,X0)
| ~ icext(uri_xsd_anyURI,X0) ),
inference(cnf_transformation,[status(thm)],[f2249]) ).
fof(f2405,plain,
~ iext(uri_rdfs_subPropertyOf,uri_ex_p,uri_owl_topDataProperty),
inference(cnf_transformation,[status(thm)],[f560]) ).
fof(f2406,plain,
iext(uri_rdf_type,uri_ex_p,uri_owl_DatatypeProperty),
inference(cnf_transformation,[status(thm)],[f561]) ).
fof(f2413,plain,
! [C1,C2,C3,X] :
( ( ( ~ icext(C3,X)
& ~ icext(C2,X)
& ~ icext(C1,X) )
| sP1_prd(X,C3,C2,C1) )
& ( icext(C3,X)
| icext(C2,X)
| icext(C1,X)
| ~ sP1_prd(X,C3,C2,C1) ) ),
inference(NNF_transformation,[status(thm)],[f1183]) ).
fof(f2414,plain,
( ! [C1,C2,C3,X] :
( ( ~ icext(C3,X)
& ~ icext(C2,X)
& ~ icext(C1,X) )
| sP1_prd(X,C3,C2,C1) )
& ! [C1,C2,C3,X] :
( icext(C3,X)
| icext(C2,X)
| icext(C1,X)
| ~ sP1_prd(X,C3,C2,C1) ) ),
inference(miniscoping,[status(thm)],[f2413]) ).
fof(f2415,plain,
! [X0,X1,X2,X3] :
( ~ sP1_prd(X1,X3,X2,X0)
| icext(X3,X1)
| icext(X2,X1)
| icext(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2414]) ).
fof(f2418,plain,
! [X0,X1,X2,X3] :
( ~ icext(X1,X0)
| sP1_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f2414]) ).
fof(f2553,plain,
! [X0,X1] :
( ~ ip(X1)
| iext(uri_rdfs_subPropertyOf,X1,X0)
| ~ iext(X0,sK116_skl(X0,X1),sK117_skl(X0,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1748,f564]) ).
fof(f2554,plain,
! [X0,X1] :
( ~ lv(X1)
| iext(uri_owl_topDataProperty,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1062,f565]) ).
fof(f2787,plain,
icext(uri_owl_DatatypeProperty,uri_ex_p),
inference(resolution,[status(thm)],[f594,f2406]) ).
fof(f2790,plain,
! [X0,X1] : sP1_prd(uri_ex_p,uri_owl_DatatypeProperty,X0,X1),
inference(resolution,[status(thm)],[f2787,f2418]) ).
fof(f2875,definition,
( sQ6_spl
<=> ioap(uri_rdfs_isDefinedBy) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f2877,plain,
( sQ6_spl
| ~ ioap(uri_rdfs_isDefinedBy) ),
inference(component_clause,[status(thm)],[f2875]) ).
fof(f3062,plain,
! [X0,X1] :
( icext(uri_owl_DatatypeProperty,uri_ex_p)
| icext(X1,uri_ex_p)
| icext(X0,uri_ex_p) ),
inference(resolution,[status(thm)],[f2415,f2790]) ).
fof(f3066,definition,
! [X0] :
( sQ17_spl
<=> icext(X0,uri_ex_p) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f3067,plain,
! [X0] :
( ~ sQ17_spl
| icext(X0,uri_ex_p) ),
inference(component_clause,[status(thm)],[f3066]) ).
fof(f3069,definition,
( sQ18_spl
<=> icext(uri_owl_DatatypeProperty,uri_ex_p) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f3070,plain,
( ~ sQ18_spl
| icext(uri_owl_DatatypeProperty,uri_ex_p) ),
inference(component_clause,[status(thm)],[f3069]) ).
fof(f3072,plain,
( sQ18_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f3062,f3066,f3069]) ).
fof(f3094,plain,
( ~ sQ17_spl
| ~ icext(uri_xsd_anyURI,uri_ex_p) ),
inference(resolution,[status(thm)],[f3067,f2250]) ).
fof(f3110,plain,
( ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3094,f3067]) ).
fof(f3111,plain,
~ sQ17_spl,
inference(contradiction_clause,[status(thm)],[f3110]) ).
fof(f4188,definition,
! [X0] :
( sQ55_spl
<=> ~ iext(uri_rdfs_range,uri_rdfs_isDefinedBy,X0) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f4189,plain,
! [X0] :
( ~ sQ55_spl
| ~ iext(uri_rdfs_range,uri_rdfs_isDefinedBy,X0) ),
inference(component_clause,[status(thm)],[f4188]) ).
fof(f4213,definition,
! [X0] :
( sQ57_spl
<=> ~ iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,X0) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f4214,plain,
! [X0] :
( ~ sQ57_spl
| ~ iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,X0) ),
inference(component_clause,[status(thm)],[f4213]) ).
fof(f5846,plain,
( ~ ip(uri_ex_p)
| ~ ip(uri_owl_topDataProperty)
| iext(uri_ex_p,sK116_skl(uri_owl_topDataProperty,uri_ex_p),sK117_skl(uri_owl_topDataProperty,uri_ex_p)) ),
inference(resolution,[status(thm)],[f1747,f2405]) ).
fof(f5855,definition,
( sQ163_spl
<=> iext(uri_ex_p,sK116_skl(uri_owl_topDataProperty,uri_ex_p),sK117_skl(uri_owl_topDataProperty,uri_ex_p)) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f5856,plain,
( ~ sQ163_spl
| iext(uri_ex_p,sK116_skl(uri_owl_topDataProperty,uri_ex_p),sK117_skl(uri_owl_topDataProperty,uri_ex_p)) ),
inference(component_clause,[status(thm)],[f5855]) ).
fof(f5858,definition,
( sQ164_spl
<=> ip(uri_owl_topDataProperty) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f5860,plain,
( sQ164_spl
| ~ ip(uri_owl_topDataProperty) ),
inference(component_clause,[status(thm)],[f5858]) ).
fof(f5861,definition,
( sQ165_spl
<=> ip(uri_ex_p) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f5863,plain,
( sQ165_spl
| ~ ip(uri_ex_p) ),
inference(component_clause,[status(thm)],[f5861]) ).
fof(f5864,plain,
( ~ sQ165_spl
| ~ sQ164_spl
| sQ163_spl ),
inference(split_clause,[status(thm)],[f5846,f5855,f5858,f5861]) ).
fof(f5883,definition,
! [X0] :
( sQ169_spl
<=> iext(uri_owl_propertyDisjointWith,X0,X0) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f5884,plain,
! [X0] :
( ~ sQ169_spl
| iext(uri_owl_propertyDisjointWith,X0,X0) ),
inference(component_clause,[status(thm)],[f5883]) ).
fof(f5895,plain,
( sQ165_spl
| ~ iodp(uri_ex_p) ),
inference(resolution,[status(thm)],[f5863,f708]) ).
fof(f5907,plain,
( sQ164_spl
| ~ iodp(uri_owl_topDataProperty) ),
inference(resolution,[status(thm)],[f5860,f708]) ).
fof(f5910,plain,
( sQ164_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5907,f1063]) ).
fof(f5911,plain,
sQ164_spl,
inference(contradiction_clause,[status(thm)],[f5910]) ).
fof(f6057,plain,
( ~ iext(uri_owl_topDataProperty,sK116_skl(uri_owl_topDataProperty,uri_ex_p),sK117_skl(uri_owl_topDataProperty,uri_ex_p))
| ~ ip(uri_ex_p) ),
inference(resolution,[status(thm)],[f2553,f2405]) ).
fof(f6062,definition,
( sQ174_spl
<=> iext(uri_owl_topDataProperty,sK116_skl(uri_owl_topDataProperty,uri_ex_p),sK117_skl(uri_owl_topDataProperty,uri_ex_p)) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f6064,plain,
( sQ174_spl
| ~ iext(uri_owl_topDataProperty,sK116_skl(uri_owl_topDataProperty,uri_ex_p),sK117_skl(uri_owl_topDataProperty,uri_ex_p)) ),
inference(component_clause,[status(thm)],[f6062]) ).
fof(f6065,plain,
( ~ sQ174_spl
| ~ sQ165_spl ),
inference(split_clause,[status(thm)],[f6057,f5861,f6062]) ).
fof(f6082,plain,
( sQ165_spl
| ~ iext(uri_rdf_type,uri_ex_p,uri_owl_DatatypeProperty) ),
inference(resolution,[status(thm)],[f5895,f712]) ).
fof(f6083,plain,
( sQ165_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6082,f2406]) ).
fof(f6084,plain,
sQ165_spl,
inference(contradiction_clause,[status(thm)],[f6083]) ).
fof(f6210,plain,
( sQ174_spl
| ~ lv(sK117_skl(uri_owl_topDataProperty,uri_ex_p)) ),
inference(resolution,[status(thm)],[f6064,f2554]) ).
fof(f6222,plain,
! [X0,X1] :
( sQ174_spl
| ~ iodp(X0)
| ~ iext(X0,X1,sK117_skl(uri_owl_topDataProperty,uri_ex_p)) ),
inference(resolution,[status(thm)],[f6210,f706]) ).
fof(f6609,plain,
( ~ sQ57_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f585,f4214]) ).
fof(f6610,plain,
~ sQ57_spl,
inference(contradiction_clause,[status(thm)],[f6609]) ).
fof(f6611,plain,
( ~ sQ55_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f586,f4189]) ).
fof(f6612,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2877,f972]) ).
fof(f6613,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f6612]) ).
fof(f6614,plain,
~ sQ55_spl,
inference(contradiction_clause,[status(thm)],[f6611]) ).
fof(f6780,plain,
! [X0,X1,X2] :
( ~ sQ169_spl
| ~ iext(X0,X1,X2)
| ~ iext(X0,X1,X2) ),
inference(resolution,[status(thm)],[f5884,f1829]) ).
fof(f6824,plain,
( ~ sQ169_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f603,f7017]) ).
fof(f7017,plain,
! [X0,X1,X2] :
( ~ sQ169_spl
| ~ iext(X0,X1,X2) ),
inference(duplicate_literals_removal,[status(thm)],[f6780]) ).
fof(f7018,plain,
~ sQ169_spl,
inference(contradiction_clause,[status(thm)],[f6824]) ).
fof(f7130,plain,
( ~ sQ163_spl
| sQ174_spl
| ~ iodp(uri_ex_p) ),
inference(resolution,[status(thm)],[f6222,f5856]) ).
fof(f7416,plain,
( ~ sQ18_spl
| iodp(uri_ex_p) ),
inference(resolution,[status(thm)],[f794,f3070]) ).
fof(f7417,plain,
( ~ sQ18_spl
| ~ sQ163_spl
| sQ174_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7416,f7130]) ).
fof(f7418,plain,
( ~ sQ18_spl
| ~ sQ163_spl
| sQ174_spl ),
inference(contradiction_clause,[status(thm)],[f7417]) ).
fof(f7419,plain,
$false,
inference(sat_refutation,[status(thm)],[f3072,f3111,f5864,f5911,f6065,f6084,f6610,f6613,f6614,f7018,f7418]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB075+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n016.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 07:50:22 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.42 % Drodi V4.1.1
% 126.43/16.40 % Refutation found
% 126.43/16.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 126.43/16.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 5.49/17.19 % Elapsed time: 16.795971 seconds
% 5.49/17.19 % CPU time: 127.667495 seconds
% 5.49/17.19 % Total memory used: 376.526 MB
% 5.49/17.19 % Net memory used: 342.814 MB
%------------------------------------------------------------------------------