%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWB053+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 : n011.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 2.69s 1.06s
% Output : CNFRefutation 2.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 9
% Syntax : Number of formulae : 37 ( 14 unt; 2 def)
% Number of atoms : 103 ( 0 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 109 ( 43 ~; 39 |; 20 &)
% ( 6 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 3 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 43 ( 41 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f25,axiom,
! [X,C] :
( iext(uri_rdf_type,X,C)
<=> icext(C,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f119,axiom,
! [X] :
( icext(uri_owl_Class,X)
<=> ic(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f145,axiom,
! [X] : ~ icext(uri_owl_Nothing,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f146,axiom,
ic(uri_owl_Nothing),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f559,conjecture,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_ex_c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f560,negated_conjecture,
~ iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_ex_c),
inference(negated_conjecture,[status(cth)],[f559]) ).
fof(f561,axiom,
iext(uri_rdf_type,uri_ex_c,uri_owl_Class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
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(f772,plain,
! [X] :
( ( ~ ic(X)
| icext(uri_owl_Class,X) )
& ( ic(X)
| ~ icext(uri_owl_Class,X) ) ),
inference(NNF_transformation,[status(thm)],[f119]) ).
fof(f773,plain,
( ! [X] :
( ~ ic(X)
| icext(uri_owl_Class,X) )
& ! [X] :
( ic(X)
| ~ icext(uri_owl_Class,X) ) ),
inference(miniscoping,[status(thm)],[f772]) ).
fof(f774,plain,
! [X0] :
( ic(X0)
| ~ icext(uri_owl_Class,X0) ),
inference(cnf_transformation,[status(thm)],[f773]) ).
fof(f823,plain,
! [X0] : ~ icext(uri_owl_Nothing,X0),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f824,plain,
ic(uri_owl_Nothing),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f1731,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(f1732,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)],[f1731]) ).
fof(f1733,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)],[f1732]) ).
fof(f1734,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))],[f1733]) ).
fof(f1738,plain,
! [X0,X1] :
( icext(X0,sK115_skl(X1,X0))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1734]) ).
fof(f2405,plain,
~ iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_ex_c),
inference(cnf_transformation,[status(thm)],[f560]) ).
fof(f2406,plain,
iext(uri_rdf_type,uri_ex_c,uri_owl_Class),
inference(cnf_transformation,[status(thm)],[f561]) ).
fof(f2627,plain,
icext(uri_owl_Class,uri_ex_c),
inference(resolution,[status(thm)],[f594,f2406]) ).
fof(f3903,plain,
! [X0] :
( ~ ic(X0)
| ~ ic(uri_owl_Nothing)
| iext(uri_rdfs_subClassOf,uri_owl_Nothing,X0) ),
inference(resolution,[status(thm)],[f1738,f823]) ).
fof(f3958,definition,
! [X0] :
( sQ146_spl
<=> ( ~ ic(X0)
| iext(uri_rdfs_subClassOf,uri_owl_Nothing,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f3959,plain,
! [X0] :
( ~ sQ146_spl
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,uri_owl_Nothing,X0) ),
inference(component_clause,[status(thm)],[f3958]) ).
fof(f3961,definition,
( sQ147_spl
<=> ic(uri_owl_Nothing) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f3963,plain,
( sQ147_spl
| ~ ic(uri_owl_Nothing) ),
inference(component_clause,[status(thm)],[f3961]) ).
fof(f3964,plain,
( ~ sQ147_spl
| sQ146_spl ),
inference(split_clause,[status(thm)],[f3903,f3958,f3961]) ).
fof(f3979,plain,
( ~ sQ146_spl
| ~ ic(uri_ex_c) ),
inference(resolution,[status(thm)],[f3959,f2405]) ).
fof(f4030,plain,
( sQ147_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3963,f824]) ).
fof(f4031,plain,
sQ147_spl,
inference(contradiction_clause,[status(thm)],[f4030]) ).
fof(f4106,plain,
ic(uri_ex_c),
inference(resolution,[status(thm)],[f774,f2627]) ).
fof(f4108,plain,
( ~ sQ146_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4106,f3979]) ).
fof(f4109,plain,
~ sQ146_spl,
inference(contradiction_clause,[status(thm)],[f4108]) ).
fof(f4110,plain,
$false,
inference(sat_refutation,[status(thm)],[f3964,f4031,f4109]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWB053+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n011.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 07:44:10 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.18/0.51 % Drodi V4.1.1
% 2.69/1.06 % Refutation found
% 2.69/1.06 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.69/1.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.17/1.11 % Elapsed time: 0.640739 seconds
% 2.17/1.11 % CPU time: 4.333840 seconds
% 2.17/1.11 % Total memory used: 160.199 MB
% 2.17/1.11 % Net memory used: 156.607 MB
%------------------------------------------------------------------------------