%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWB004+2 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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 : Sun Sep 27 08:51:26 AM UTC 2026
% Result : Theorem 0.08s 0.41s
% Output : CNFRefutation 0.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 14
% Syntax : Number of formulae : 86 ( 24 unt; 0 def)
% Number of atoms : 267 ( 0 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 286 ( 105 ~; 132 |; 39 &)
% ( 8 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 78 ( 3 sgn 51 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(simple_ir,axiom,
! [X] : ir(X),
file('theBenchmark.p',simple_ir) ).
fof(rdfs_cext_def,axiom,
! [X,C] :
( iext(uri_rdf_type,X,C)
<=> icext(C,X) ),
file('theBenchmark.p',rdfs_cext_def) ).
fof(owl_parts_idc_cond_set,axiom,
! [X] :
( idc(X)
=> ic(X) ),
file('theBenchmark.p',owl_parts_idc_cond_set) ).
fof(owl_class_classowl_ext,axiom,
! [X] :
( icext(uri_owl_Class,X)
<=> ic(X) ),
file('theBenchmark.p',owl_class_classowl_ext) ).
fof(owl_class_classrdfs_ext,axiom,
! [X] :
( icext(uri_rdfs_Class,X)
<=> ic(X) ),
file('theBenchmark.p',owl_class_classrdfs_ext) ).
fof(owl_class_datatype_ext,axiom,
! [X] :
( icext(uri_rdfs_Datatype,X)
<=> idc(X) ),
file('theBenchmark.p',owl_class_datatype_ext) ).
fof(owl_class_thing_ext,axiom,
! [X] :
( icext(uri_owl_Thing,X)
<=> ir(X) ),
file('theBenchmark.p',owl_class_thing_ext) ).
fof(owl_rdfsext_subclassof,axiom,
! [C1,C2] :
( iext(uri_rdfs_subClassOf,C1,C2)
<=> ( ! [X] :
( icext(C1,X)
=> icext(C2,X) )
& ic(C2)
& ic(C1) ) ),
file('theBenchmark.p',owl_rdfsext_subclassof) ).
fof(owl_eqdis_equivalentclass,axiom,
! [C1,C2] :
( iext(uri_owl_equivalentClass,C1,C2)
<=> ( ! [X] :
( icext(C1,X)
<=> icext(C2,X) )
& ic(C2)
& ic(C1) ) ),
file('theBenchmark.p',owl_eqdis_equivalentclass) ).
fof(testcase_conclusion_fullish_004_Axiomatic_Triples,conjecture,
( iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)
& iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
& iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing)
& iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)
& iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
file('theBenchmark.p',testcase_conclusion_fullish_004_Axiomatic_Triples) ).
fof(testcase_conclusion_fullish_004_Axiomatic_Triples_neg,negated_conjecture,
~ ( iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)
& iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
& iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing)
& iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)
& iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_004_Axiomatic_Triples]) ).
cnf(c_11,plain,
( ~ ir(A)
| icext(uri_owl_Thing,A) ),
inference(clausify,[status(thm)],[owl_class_thing_ext]) ).
cnf(c_13,plain,
ir(A),
inference(clausify,[status(thm)],[simple_ir]) ).
cnf(c_14,plain,
( idc(A)
| ~ icext(uri_rdfs_Datatype,A) ),
inference(clausify,[status(thm)],[owl_class_datatype_ext]) ).
cnf(c_16,plain,
( ic(A)
| ~ idc(A) ),
inference(clausify,[status(thm)],[owl_parts_idc_cond_set]) ).
cnf(c_17,plain,
( ~ icext(uri_rdfs_Datatype,A)
| ic(A) ),
inference(resolve,[status(thm)],[c_16,c_14]) ).
cnf(c_19,plain,
( ~ icext(B,A)
| iext(uri_rdf_type,A,B) ),
inference(clausify,[status(thm)],[rdfs_cext_def]) ).
fof(owl_class_classowl_type,axiom,
ic(uri_owl_Class),
file('theBenchmark.p',owl_class_classowl_type) ).
cnf(c_20,plain,
ic(uri_owl_Class),
inference(clausify,[status(thm)],[owl_class_classowl_type]) ).
cnf(c_21,plain,
( ic(A)
| ~ icext(uri_owl_Class,A) ),
inference(clausify,[status(thm)],[owl_class_classowl_ext]) ).
cnf(c_22,plain,
( ~ ic(A)
| icext(uri_owl_Class,A) ),
inference(clausify,[status(thm)],[owl_class_classowl_ext]) ).
fof(owl_class_classrdfs_type,axiom,
ic(uri_rdfs_Class),
file('theBenchmark.p',owl_class_classrdfs_type) ).
cnf(c_23,plain,
ic(uri_rdfs_Class),
inference(clausify,[status(thm)],[owl_class_classrdfs_type]) ).
cnf(c_24,plain,
( ic(A)
| ~ icext(uri_rdfs_Class,A) ),
inference(clausify,[status(thm)],[owl_class_classrdfs_ext]) ).
cnf(c_25,plain,
( ~ ic(A)
| icext(uri_rdfs_Class,A) ),
inference(clausify,[status(thm)],[owl_class_classrdfs_ext]) ).
fof(owl_class_datatype_type,axiom,
ic(uri_rdfs_Datatype),
file('theBenchmark.p',owl_class_datatype_type) ).
cnf(c_26,plain,
ic(uri_rdfs_Datatype),
inference(clausify,[status(thm)],[owl_class_datatype_type]) ).
fof(owl_class_thing_type,axiom,
ic(uri_owl_Thing),
file('theBenchmark.p',owl_class_thing_type) ).
cnf(c_27,plain,
ic(uri_owl_Thing),
inference(clausify,[status(thm)],[owl_class_thing_type]) ).
fof(nnf_8,plain,
! [C1,C2] :
( ( ? [X] :
( ~ icext(C2,X)
& icext(C1,X) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_rdfs_subClassOf,C1,C2) )
& ( ( ! [X0] :
( icext(C2,X0)
| ~ icext(C1,X0) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_rdfs_subClassOf,C1,C2) ) ),
inference(fof_nnf,[status(thm)],[owl_rdfsext_subclassof]) ).
fof(sk_owl_rdfsext_subclassof_sk,plain,
! [C1,C2] :
( ( ( ~ icext(C2,sK0(C1,C2))
& icext(C1,sK0(C1,C2)) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_rdfs_subClassOf,C1,C2) )
& ( ( ! [X0] :
( icext(C2,X0)
| ~ icext(C1,X0) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_rdfs_subClassOf,C1,C2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X,sK0(C1,C2))],[nnf_8]) ).
fof(sk_owl_rdfsext_subclassof,plain,
( ! [VAR_0,VAR_1] :
( ~ icext(VAR_1,sK0(VAR_0,VAR_1))
| ~ ic(VAR_1)
| ~ ic(VAR_0)
| iext(uri_rdfs_subClassOf,VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( icext(VAR_0,sK0(VAR_0,VAR_1))
| ~ ic(VAR_1)
| ~ ic(VAR_0)
| iext(uri_rdfs_subClassOf,VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( icext(VAR_1,VAR_2)
| ~ icext(VAR_0,VAR_2)
| ~ iext(uri_rdfs_subClassOf,VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( ic(VAR_1)
| ~ iext(uri_rdfs_subClassOf,VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( ic(VAR_0)
| ~ iext(uri_rdfs_subClassOf,VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_owl_rdfsext_subclassof_sk]) ).
cnf(c_31,plain,
( icext(A,sK0(A,B))
| ~ ic(B)
| ~ ic(A)
| iext(uri_rdfs_subClassOf,A,B) ),
inference(split_conjunct,[status(thm)],[sk_owl_rdfsext_subclassof]) ).
cnf(c_32,plain,
( ~ icext(B,sK0(A,B))
| ~ ic(B)
| ~ ic(A)
| iext(uri_rdfs_subClassOf,A,B) ),
inference(split_conjunct,[status(thm)],[sk_owl_rdfsext_subclassof]) ).
fof(nnf_9,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) )
& ( ( ! [X0] :
( ( ~ icext(C2,X0)
| icext(C1,X0) )
& ( icext(C2,X0)
| ~ icext(C1,X0) ) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_owl_equivalentClass,C1,C2) ) ),
inference(fof_nnf,[status(thm)],[owl_eqdis_equivalentclass]) ).
fof(sk_owl_eqdis_equivalentclass_sk,plain,
! [C1,C2] :
( ( ( ( ~ icext(C2,sK1(C1,C2))
| ~ icext(C1,sK1(C1,C2)) )
& ( icext(C2,sK1(C1,C2))
| icext(C1,sK1(C1,C2)) ) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_owl_equivalentClass,C1,C2) )
& ( ( ! [X0] :
( ( ~ icext(C2,X0)
| icext(C1,X0) )
& ( icext(C2,X0)
| ~ icext(C1,X0) ) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_owl_equivalentClass,C1,C2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X,sK1(C1,C2))],[nnf_9]) ).
fof(sk_owl_eqdis_equivalentclass,plain,
( ! [VAR_0,VAR_1] :
( ~ icext(VAR_1,sK1(VAR_0,VAR_1))
| ~ icext(VAR_0,sK1(VAR_0,VAR_1))
| ~ ic(VAR_1)
| ~ ic(VAR_0)
| iext(uri_owl_equivalentClass,VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( icext(VAR_1,sK1(VAR_0,VAR_1))
| icext(VAR_0,sK1(VAR_0,VAR_1))
| ~ ic(VAR_1)
| ~ ic(VAR_0)
| iext(uri_owl_equivalentClass,VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ icext(VAR_1,VAR_2)
| icext(VAR_0,VAR_2)
| ~ iext(uri_owl_equivalentClass,VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( icext(VAR_1,VAR_2)
| ~ icext(VAR_0,VAR_2)
| ~ iext(uri_owl_equivalentClass,VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( ic(VAR_1)
| ~ iext(uri_owl_equivalentClass,VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( ic(VAR_0)
| ~ iext(uri_owl_equivalentClass,VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_owl_eqdis_equivalentclass_sk]) ).
cnf(c_37,plain,
( icext(B,sK1(A,B))
| icext(A,sK1(A,B))
| ~ ic(B)
| ~ ic(A)
| iext(uri_owl_equivalentClass,A,B) ),
inference(split_conjunct,[status(thm)],[sk_owl_eqdis_equivalentclass]) ).
cnf(c_38,plain,
( ~ icext(B,sK1(A,B))
| ~ icext(A,sK1(A,B))
| ~ ic(B)
| ~ ic(A)
| iext(uri_owl_equivalentClass,A,B) ),
inference(split_conjunct,[status(thm)],[sk_owl_eqdis_equivalentclass]) ).
cnf(c_39,negated_conjecture,
( ~ iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(clausify,[status(thm)],[testcase_conclusion_fullish_004_Axiomatic_Triples_neg]) ).
cnf(c_40,plain,
icext(uri_owl_Thing,A),
inference(resolve,[status(thm)],[c_11,c_13]) ).
cnf(c_45,plain,
icext(uri_owl_Class,uri_owl_Class),
inference(resolve,[status(thm)],[c_22,c_20]) ).
cnf(c_53,plain,
( icext(uri_rdfs_Datatype,sK0(uri_rdfs_Datatype,A))
| ~ ic(A)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,A) ),
inference(resolve,[status(thm)],[c_31,c_26]) ).
cnf(c_62,plain,
( icext(A,sK1(uri_owl_Class,A))
| icext(uri_owl_Class,sK1(uri_owl_Class,A))
| ~ ic(A)
| iext(uri_owl_equivalentClass,uri_owl_Class,A) ),
inference(resolve,[status(thm)],[c_37,c_20]) ).
cnf(c_307,plain,
( ~ ic(uri_owl_Thing)
| ~ ic(A)
| iext(uri_rdfs_subClassOf,A,uri_owl_Thing) ),
inference(resolve,[status(thm)],[c_40,c_32]) ).
cnf(c_71,plain,
( ~ ic(A)
| iext(uri_rdfs_subClassOf,A,uri_owl_Thing) ),
inference(resolve,[status(thm)],[c_27,c_307]) ).
cnf(c_72,plain,
iext(uri_rdf_type,A,uri_owl_Thing),
inference(resolve,[status(thm)],[c_40,c_19]) ).
cnf(c_73,negated_conjecture,
( ~ iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Class) ),
inference(resolve,[status(thm)],[c_72,c_39]) ).
cnf(c_79,plain,
iext(uri_rdf_type,uri_owl_Class,uri_owl_Class),
inference(resolve,[status(thm)],[c_45,c_19]) ).
cnf(c_80,negated_conjecture,
( ~ iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing) ),
inference(resolve,[status(thm)],[c_79,c_73]) ).
cnf(c_90,plain,
( icext(uri_rdfs_Datatype,sK0(uri_rdfs_Datatype,uri_owl_Class))
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class) ),
inference(resolve,[status(thm)],[c_53,c_20]) ).
cnf(c_99,plain,
iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing),
inference(resolve,[status(thm)],[c_71,c_20]) ).
cnf(c_100,negated_conjecture,
( ~ iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class) ),
inference(resolve,[status(thm)],[c_99,c_80]) ).
cnf(c_102,plain,
( ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| icext(uri_rdfs_Datatype,sK0(uri_rdfs_Datatype,uri_owl_Class)) ),
inference(resolve,[status(thm)],[c_90,c_100]) ).
cnf(c_118,plain,
( icext(uri_rdfs_Class,sK1(uri_owl_Class,uri_rdfs_Class))
| icext(uri_owl_Class,sK1(uri_owl_Class,uri_rdfs_Class))
| iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class) ),
inference(resolve,[status(thm)],[c_62,c_23]) ).
cnf(c_140,plain,
( icext(uri_rdfs_Datatype,sK0(uri_rdfs_Datatype,uri_owl_Class))
| icext(uri_rdfs_Class,sK1(uri_owl_Class,uri_rdfs_Class))
| icext(uri_owl_Class,sK1(uri_owl_Class,uri_rdfs_Class)) ),
inference(resolve,[status(thm)],[c_118,c_102]) ).
cnf(c_145,plain,
( ic(sK0(uri_rdfs_Datatype,uri_owl_Class))
| icext(uri_rdfs_Class,sK1(uri_owl_Class,uri_rdfs_Class))
| icext(uri_owl_Class,sK1(uri_owl_Class,uri_rdfs_Class)) ),
inference(resolve,[status(thm)],[c_140,c_17]) ).
cnf(c_148,plain,
( ic(sK1(uri_owl_Class,uri_rdfs_Class))
| ic(sK0(uri_rdfs_Datatype,uri_owl_Class))
| icext(uri_owl_Class,sK1(uri_owl_Class,uri_rdfs_Class)) ),
inference(resolve,[status(thm)],[c_145,c_24]) ).
cnf(c_308,plain,
( ic(sK1(uri_owl_Class,uri_rdfs_Class))
| ic(sK1(uri_owl_Class,uri_rdfs_Class))
| ic(sK0(uri_rdfs_Datatype,uri_owl_Class)) ),
inference(resolve,[status(thm)],[c_148,c_21]) ).
cnf(c_157,plain,
( ic(sK1(uri_owl_Class,uri_rdfs_Class))
| ic(sK0(uri_rdfs_Datatype,uri_owl_Class)) ),
inference(copy,[status(thm)],[c_308]) ).
cnf(c_177,plain,
( icext(uri_rdfs_Class,sK1(uri_owl_Class,uri_rdfs_Class))
| ic(sK0(uri_rdfs_Datatype,uri_owl_Class)) ),
inference(resolve,[status(thm)],[c_157,c_25]) ).
cnf(c_178,plain,
( icext(uri_owl_Class,sK1(uri_owl_Class,uri_rdfs_Class))
| ic(sK0(uri_rdfs_Datatype,uri_owl_Class)) ),
inference(resolve,[status(thm)],[c_157,c_22]) ).
cnf(c_309,plain,
( ~ icext(uri_owl_Class,sK1(uri_owl_Class,uri_rdfs_Class))
| ~ ic(uri_rdfs_Class)
| ~ ic(uri_owl_Class)
| iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ic(sK0(uri_rdfs_Datatype,uri_owl_Class)) ),
inference(resolve,[status(thm)],[c_177,c_38]) ).
cnf(c_310,plain,
( ~ icext(uri_owl_Class,sK1(uri_owl_Class,uri_rdfs_Class))
| ~ ic(uri_rdfs_Class)
| iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ic(sK0(uri_rdfs_Datatype,uri_owl_Class)) ),
inference(resolve,[status(thm)],[c_20,c_309]) ).
cnf(c_181,plain,
( ~ icext(uri_owl_Class,sK1(uri_owl_Class,uri_rdfs_Class))
| iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ic(sK0(uri_rdfs_Datatype,uri_owl_Class)) ),
inference(resolve,[status(thm)],[c_23,c_310]) ).
cnf(c_311,plain,
( ic(sK0(uri_rdfs_Datatype,uri_owl_Class))
| iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ic(sK0(uri_rdfs_Datatype,uri_owl_Class)) ),
inference(resolve,[status(thm)],[c_181,c_178]) ).
cnf(c_213,plain,
( iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ic(sK0(uri_rdfs_Datatype,uri_owl_Class)) ),
inference(copy,[status(thm)],[c_311]) ).
cnf(c_219,plain,
( icext(uri_rdfs_Datatype,sK0(uri_rdfs_Datatype,uri_owl_Class))
| ic(sK0(uri_rdfs_Datatype,uri_owl_Class)) ),
inference(resolve,[status(thm)],[c_213,c_102]) ).
cnf(c_312,plain,
( ic(sK0(uri_rdfs_Datatype,uri_owl_Class))
| ic(sK0(uri_rdfs_Datatype,uri_owl_Class)) ),
inference(resolve,[status(thm)],[c_219,c_17]) ).
cnf(c_227,plain,
ic(sK0(uri_rdfs_Datatype,uri_owl_Class)),
inference(copy,[status(thm)],[c_312]) ).
cnf(c_248,plain,
icext(uri_owl_Class,sK0(uri_rdfs_Datatype,uri_owl_Class)),
inference(resolve,[status(thm)],[c_227,c_22]) ).
cnf(c_313,plain,
( ~ ic(uri_owl_Class)
| ~ ic(uri_rdfs_Datatype)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class) ),
inference(resolve,[status(thm)],[c_248,c_32]) ).
cnf(c_314,plain,
( ~ ic(uri_owl_Class)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class) ),
inference(resolve,[status(thm)],[c_26,c_313]) ).
cnf(c_259,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class),
inference(resolve,[status(thm)],[c_20,c_314]) ).
cnf(c_261,negated_conjecture,
~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class),
inference(resolve,[status(thm)],[c_259,c_100]) ).
cnf(c_262,negated_conjecture,
( icext(uri_rdfs_Class,sK1(uri_owl_Class,uri_rdfs_Class))
| icext(uri_owl_Class,sK1(uri_owl_Class,uri_rdfs_Class)) ),
inference(resolve,[status(thm)],[c_261,c_118]) ).
cnf(c_275,plain,
( ic(sK1(uri_owl_Class,uri_rdfs_Class))
| icext(uri_owl_Class,sK1(uri_owl_Class,uri_rdfs_Class)) ),
inference(resolve,[status(thm)],[c_262,c_24]) ).
cnf(c_315,plain,
( ic(sK1(uri_owl_Class,uri_rdfs_Class))
| ic(sK1(uri_owl_Class,uri_rdfs_Class)) ),
inference(resolve,[status(thm)],[c_275,c_21]) ).
cnf(c_281,plain,
ic(sK1(uri_owl_Class,uri_rdfs_Class)),
inference(copy,[status(thm)],[c_315]) ).
cnf(c_301,plain,
icext(uri_rdfs_Class,sK1(uri_owl_Class,uri_rdfs_Class)),
inference(resolve,[status(thm)],[c_281,c_25]) ).
cnf(c_302,plain,
icext(uri_owl_Class,sK1(uri_owl_Class,uri_rdfs_Class)),
inference(resolve,[status(thm)],[c_281,c_22]) ).
cnf(c_316,plain,
( ~ icext(uri_owl_Class,sK1(uri_owl_Class,uri_rdfs_Class))
| ~ ic(uri_rdfs_Class)
| ~ ic(uri_owl_Class)
| iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class) ),
inference(resolve,[status(thm)],[c_301,c_38]) ).
cnf(c_317,negated_conjecture,
( ~ icext(uri_owl_Class,sK1(uri_owl_Class,uri_rdfs_Class))
| ~ ic(uri_rdfs_Class)
| ~ ic(uri_owl_Class) ),
inference(resolve,[status(thm)],[c_261,c_316]) ).
cnf(c_318,negated_conjecture,
( ~ icext(uri_owl_Class,sK1(uri_owl_Class,uri_rdfs_Class))
| ~ ic(uri_rdfs_Class) ),
inference(resolve,[status(thm)],[c_20,c_317]) ).
cnf(c_319,negated_conjecture,
~ icext(uri_owl_Class,sK1(uri_owl_Class,uri_rdfs_Class)),
inference(resolve,[status(thm)],[c_23,c_318]) ).
cnf(c_306,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_302,c_319]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB004+2 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n012.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 11:38:50 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.37 % Process 502385 was started by sandbox on n012,
% 0.08/0.37 % Sat Sep 26 11:38:50 2026
% 0.08/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.37
% 0.08/0.37 % From the command line: assign(max_seconds, 300).
% 0.08/0.41
% 0.08/0.41 % SZS status Theorem for theBenchmark
% 0.08/0.41
% 0.08/0.41 % Proof 1 at 0.02 (+ 0.01) seconds.
% 0.08/0.41 % Length of proof is 62.
% 0.08/0.41 % Level of proof is 24.
% 0.08/0.41 % Maximum clause weight is 20.000.
% 0.08/0.41 % Given clauses 151.
% 0.08/0.41
% 0.08/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------