%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWB031+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 : n007.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:12 PM UTC 2026
% Result : Unsatisfiable 19.39s 3.01s
% Output : CNFRefutation 19.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 19
% Syntax : Number of formulae : 92 ( 23 unt; 5 def)
% Number of atoms : 309 ( 21 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 360 ( 143 ~; 133 |; 66 &)
% ( 16 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 6 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 19 con; 0-3 aty)
% Number of variables : 143 ( 128 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X] : ir(X),
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(f43,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f145,axiom,
! [X] : ~ icext(uri_owl_Nothing,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f151,axiom,
! [X] :
( icext(uri_owl_OntologyProperty,X)
<=> ioxp(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f163,axiom,
! [X] :
( icext(uri_owl_Thing,X)
<=> ir(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f179,axiom,
ioxp(uri_owl_backwardCompatibleWith),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f287,axiom,
! [Z] :
( iext(uri_owl_unionOf,Z,uri_rdf_nil)
<=> ( ! [X] : ~ icext(Z,X)
& ic(Z) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f294,axiom,
! [Z] :
( iext(uri_owl_oneOf,Z,uri_rdf_nil)
<=> ( ! [X] : ~ icext(Z,X)
& ic(Z) ) ),
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(f351,axiom,
! [C1,C2] :
( iext(uri_owl_equivalentClass,C1,C2)
<=> ( ! [X] :
( icext(C1,X)
<=> icext(C2,X) )
& ic(C2)
& ic(C1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f356,axiom,
! [S1,A1] :
( ( iext(uri_rdf_rest,S1,uri_rdf_nil)
& iext(uri_rdf_first,S1,A1) )
=> ? [Z] :
( iext(uri_owl_distinctMembers,Z,S1)
& icext(uri_owl_AllDifferent,Z) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f559,axiom,
? [BNODE_x,BNODE_l] :
( iext(uri_rdf_rest,BNODE_l,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l,uri_ex_w)
& iext(uri_owl_oneOf,BNODE_x,BNODE_l)
& iext(uri_owl_equivalentClass,uri_owl_Thing,BNODE_x) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f563,plain,
! [X0] : ir(X0),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f590,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(f591,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)],[f590]) ).
fof(f592,plain,
! [X0,X1] :
( icext(X1,X0)
| ~ iext(uri_rdf_type,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f591]) ).
fof(f613,plain,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f615,plain,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f821,plain,
! [X0] : ~ icext(uri_owl_Nothing,X0),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f833,plain,
! [X] :
( ( ~ ioxp(X)
| icext(uri_owl_OntologyProperty,X) )
& ( ioxp(X)
| ~ icext(uri_owl_OntologyProperty,X) ) ),
inference(NNF_transformation,[status(thm)],[f151]) ).
fof(f834,plain,
( ! [X] :
( ~ ioxp(X)
| icext(uri_owl_OntologyProperty,X) )
& ! [X] :
( ioxp(X)
| ~ icext(uri_owl_OntologyProperty,X) ) ),
inference(miniscoping,[status(thm)],[f833]) ).
fof(f836,plain,
! [X0] :
( ~ ioxp(X0)
| icext(uri_owl_OntologyProperty,X0) ),
inference(cnf_transformation,[status(thm)],[f834]) ).
fof(f857,plain,
! [X] :
( ( ~ ir(X)
| icext(uri_owl_Thing,X) )
& ( ir(X)
| ~ icext(uri_owl_Thing,X) ) ),
inference(NNF_transformation,[status(thm)],[f163]) ).
fof(f858,plain,
( ! [X] :
( ~ ir(X)
| icext(uri_owl_Thing,X) )
& ! [X] :
( ir(X)
| ~ icext(uri_owl_Thing,X) ) ),
inference(miniscoping,[status(thm)],[f857]) ).
fof(f860,plain,
! [X0] :
( ~ ir(X0)
| icext(uri_owl_Thing,X0) ),
inference(cnf_transformation,[status(thm)],[f858]) ).
fof(f889,plain,
ioxp(uri_owl_backwardCompatibleWith),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f1151,plain,
! [Z] :
( ( ? [X] : icext(Z,X)
| ~ ic(Z)
| iext(uri_owl_unionOf,Z,uri_rdf_nil) )
& ( ( ! [X] : ~ icext(Z,X)
& ic(Z) )
| ~ iext(uri_owl_unionOf,Z,uri_rdf_nil) ) ),
inference(NNF_transformation,[status(thm)],[f287]) ).
fof(f1152,plain,
( ! [Z] :
( ? [X] : icext(Z,X)
| ~ ic(Z)
| iext(uri_owl_unionOf,Z,uri_rdf_nil) )
& ! [Z] :
( ( ! [X] : ~ icext(Z,X)
& ic(Z) )
| ~ iext(uri_owl_unionOf,Z,uri_rdf_nil) ) ),
inference(miniscoping,[status(thm)],[f1151]) ).
fof(f1153,plain,
( ! [Z] :
( icext(Z,sK5_skl(Z))
| ~ ic(Z)
| iext(uri_owl_unionOf,Z,uri_rdf_nil) )
& ! [Z] :
( ( ! [X] : ~ icext(Z,X)
& ic(Z) )
| ~ iext(uri_owl_unionOf,Z,uri_rdf_nil) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(X,sK5_skl(Z))],[f1152]) ).
fof(f1155,plain,
! [X0,X1] :
( ~ icext(X0,X1)
| ~ iext(uri_owl_unionOf,X0,uri_rdf_nil) ),
inference(cnf_transformation,[status(thm)],[f1153]) ).
fof(f1203,plain,
! [Z] :
( ( ? [X] : icext(Z,X)
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,uri_rdf_nil) )
& ( ( ! [X] : ~ icext(Z,X)
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,uri_rdf_nil) ) ),
inference(NNF_transformation,[status(thm)],[f294]) ).
fof(f1204,plain,
( ! [Z] :
( ? [X] : icext(Z,X)
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,uri_rdf_nil) )
& ! [Z] :
( ( ! [X] : ~ icext(Z,X)
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,uri_rdf_nil) ) ),
inference(miniscoping,[status(thm)],[f1203]) ).
fof(f1205,plain,
( ! [Z] :
( icext(Z,sK9_skl(Z))
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,uri_rdf_nil) )
& ! [Z] :
( ( ! [X] : ~ icext(Z,X)
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,uri_rdf_nil) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X,sK9_skl(Z))],[f1204]) ).
fof(f1207,plain,
! [X0,X1] :
( ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,uri_rdf_nil) ),
inference(cnf_transformation,[status(thm)],[f1205]) ).
fof(f1209,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(f1210,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)],[f1209]) ).
fof(f1211,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)],[f1210]) ).
fof(f1212,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))],[f1211]) ).
fof(f1214,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)],[f1212]) ).
fof(f1803,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(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) )
& ! [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)],[f1803]) ).
fof(f1805,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))],[f1804]) ).
fof(f1808,plain,
! [X0,X1,X2] :
( icext(X1,X2)
| ~ icext(X0,X2)
| ~ iext(uri_owl_equivalentClass,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1805]) ).
fof(f1837,plain,
! [S1,A1] :
( ? [Z] :
( iext(uri_owl_distinctMembers,Z,S1)
& icext(uri_owl_AllDifferent,Z) )
| ~ iext(uri_rdf_rest,S1,uri_rdf_nil)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(pre_NNF_transformation,[status(thm)],[f356]) ).
fof(f1838,plain,
! [S1] :
( ? [Z] :
( iext(uri_owl_distinctMembers,Z,S1)
& icext(uri_owl_AllDifferent,Z) )
| ~ iext(uri_rdf_rest,S1,uri_rdf_nil)
| ! [A1] : ~ iext(uri_rdf_first,S1,A1) ),
inference(miniscoping,[status(thm)],[f1837]) ).
fof(f1839,plain,
! [S1] :
( ( iext(uri_owl_distinctMembers,sK129_skl(S1),S1)
& icext(uri_owl_AllDifferent,sK129_skl(S1)) )
| ~ iext(uri_rdf_rest,S1,uri_rdf_nil)
| ! [A1] : ~ iext(uri_rdf_first,S1,A1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK129_skl]),skolemize(Z,sK129_skl(S1))],[f1838]) ).
fof(f1840,plain,
! [X0,X1] :
( icext(uri_owl_AllDifferent,sK129_skl(X0))
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1839]) ).
fof(f2403,plain,
? [BNODE_l] :
( iext(uri_rdf_rest,BNODE_l,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l,uri_ex_w)
& ? [BNODE_x] :
( iext(uri_owl_oneOf,BNODE_x,BNODE_l)
& iext(uri_owl_equivalentClass,uri_owl_Thing,BNODE_x) ) ),
inference(miniscoping,[status(thm)],[f559]) ).
fof(f2404,plain,
( iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)
& iext(uri_rdf_first,sK199_skl,uri_ex_w)
& iext(uri_owl_oneOf,sK200_skl,sK199_skl)
& iext(uri_owl_equivalentClass,uri_owl_Thing,sK200_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK199_skl,sK200_skl]),skolemize(BNODE_l,sK199_skl),skolemize(BNODE_x,sK200_skl)],[f2403]) ).
fof(f2405,plain,
iext(uri_owl_equivalentClass,uri_owl_Thing,sK200_skl),
inference(cnf_transformation,[status(thm)],[f2404]) ).
fof(f2406,plain,
iext(uri_owl_oneOf,sK200_skl,sK199_skl),
inference(cnf_transformation,[status(thm)],[f2404]) ).
fof(f2407,plain,
iext(uri_rdf_first,sK199_skl,uri_ex_w),
inference(cnf_transformation,[status(thm)],[f2404]) ).
fof(f2408,plain,
iext(uri_rdf_rest,sK199_skl,uri_rdf_nil),
inference(cnf_transformation,[status(thm)],[f2404]) ).
fof(f2576,plain,
icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),
inference(resolution,[status(thm)],[f613,f592]) ).
fof(f2578,plain,
icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),
inference(resolution,[status(thm)],[f615,f592]) ).
fof(f3261,plain,
! [X0] : icext(uri_owl_Thing,X0),
inference(forward_subsumption_resolution,[status(thm)],[f860,f563]) ).
fof(f4031,definition,
( sQ112_spl
<=> iext(uri_owl_unionOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_nil) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f4032,plain,
( ~ sQ112_spl
| iext(uri_owl_unionOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_nil) ),
inference(component_clause,[status(thm)],[f4031]) ).
fof(f4158,definition,
( sQ128_spl
<=> iext(uri_owl_oneOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_nil) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f4159,plain,
( ~ sQ128_spl
| iext(uri_owl_oneOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_nil) ),
inference(component_clause,[status(thm)],[f4158]) ).
fof(f4183,plain,
! [X0,X1] :
( X1 = uri_ex_w
| ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sK199_skl)
| ~ iext(uri_rdf_rest,sK199_skl,uri_rdf_nil) ),
inference(resolution,[status(thm)],[f2407,f1214]) ).
fof(f4232,definition,
( sQ133_spl
<=> iext(uri_rdf_rest,sK199_skl,uri_rdf_nil) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f4234,plain,
( sQ133_spl
| ~ iext(uri_rdf_rest,sK199_skl,uri_rdf_nil) ),
inference(component_clause,[status(thm)],[f4232]) ).
fof(f4248,definition,
! [X0,X1] :
( sQ137_spl
<=> ( X1 = uri_ex_w
| ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sK199_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f4249,plain,
! [X0,X1] :
( ~ sQ137_spl
| X1 = uri_ex_w
| ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sK199_skl) ),
inference(component_clause,[status(thm)],[f4248]) ).
fof(f4251,plain,
( sQ137_spl
| ~ sQ133_spl ),
inference(split_clause,[status(thm)],[f4183,f4232,f4248]) ).
fof(f4398,plain,
( sQ133_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4234,f2408]) ).
fof(f4399,plain,
sQ133_spl,
inference(contradiction_clause,[status(thm)],[f4398]) ).
fof(f4530,plain,
! [X0] :
( ~ sQ112_spl
| ~ icext(uri_rdfs_ContainerMembershipProperty,X0) ),
inference(resolution,[status(thm)],[f4032,f1155]) ).
fof(f4552,plain,
( ~ sQ112_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2578,f4530]) ).
fof(f4559,plain,
~ sQ112_spl,
inference(contradiction_clause,[status(thm)],[f4552]) ).
fof(f4793,plain,
! [X0] :
( ~ sQ128_spl
| ~ icext(uri_rdfs_ContainerMembershipProperty,X0) ),
inference(resolution,[status(thm)],[f1207,f4159]) ).
fof(f4796,plain,
( ~ sQ128_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2576,f4793]) ).
fof(f4799,plain,
~ sQ128_spl,
inference(contradiction_clause,[status(thm)],[f4796]) ).
fof(f5164,definition,
( sQ222_spl
<=> iext(uri_owl_oneOf,uri_owl_OntologyProperty,uri_rdf_nil) ),
introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition]) ).
fof(f5165,plain,
( ~ sQ222_spl
| iext(uri_owl_oneOf,uri_owl_OntologyProperty,uri_rdf_nil) ),
inference(component_clause,[status(thm)],[f5164]) ).
fof(f5242,plain,
! [X0] :
( ~ sQ222_spl
| ~ icext(uri_owl_OntologyProperty,X0) ),
inference(resolution,[status(thm)],[f5165,f1207]) ).
fof(f5244,plain,
! [X0] :
( ~ sQ222_spl
| ~ ioxp(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f836,f5242]) ).
fof(f5248,plain,
( ~ sQ222_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f889,f5244]) ).
fof(f5263,plain,
~ sQ222_spl,
inference(contradiction_clause,[status(thm)],[f5248]) ).
fof(f5423,plain,
! [X0] :
( icext(sK200_skl,X0)
| ~ icext(uri_owl_Thing,X0) ),
inference(resolution,[status(thm)],[f1808,f2405]) ).
fof(f5424,plain,
! [X0] : icext(sK200_skl,X0),
inference(forward_subsumption_resolution,[status(thm)],[f5423,f3261]) ).
fof(f5436,plain,
! [X0] :
( ~ sQ137_spl
| X0 = uri_ex_w
| ~ icext(sK200_skl,X0) ),
inference(resolution,[status(thm)],[f4249,f2406]) ).
fof(f5437,plain,
! [X0] :
( ~ sQ137_spl
| X0 = uri_ex_w ),
inference(forward_subsumption_resolution,[status(thm)],[f5436,f5424]) ).
fof(f5438,plain,
! [X0,X1] :
( ~ sQ137_spl
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f5437,f5437]) ).
fof(f5785,plain,
! [X0,X1] :
( ~ sQ137_spl
| ~ icext(X0,X1) ),
inference(paramodulation,[status(thm)],[f5438,f821]) ).
fof(f5847,plain,
! [X0,X1] :
( ~ sQ137_spl
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1840,f5785]) ).
fof(f5848,plain,
( ~ sQ137_spl
| ~ iext(uri_rdf_rest,sK199_skl,uri_rdf_nil) ),
inference(resolution,[status(thm)],[f5847,f2407]) ).
fof(f5851,plain,
( ~ sQ137_spl
| ~ sQ133_spl ),
inference(split_clause,[status(thm)],[f5848,f4232,f4248]) ).
fof(f5852,plain,
$false,
inference(sat_refutation,[status(thm)],[f4251,f4399,f4559,f4799,f5263,f5851]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWB031+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.39 % Computer : n007.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Mon Sep 21 07:40:36 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 19.39/3.01 % Refutation found
% 19.39/3.01 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 19.39/3.01 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 12.75/3.07 % Elapsed time: 2.665647 seconds
% 12.75/3.07 % CPU time: 20.291410 seconds
% 12.75/3.07 % Total memory used: 141.193 MB
% 12.75/3.07 % Net memory used: 129.874 MB
%------------------------------------------------------------------------------