%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWB020+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 : 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 : Sun Sep 27 08:51:33 AM UTC 2026
% Result : Theorem 58.97s 16.26s
% Output : CNFRefutation 58.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 8
% Syntax : Number of formulae : 83 ( 29 unt; 0 def)
% Number of atoms : 342 ( 0 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 416 ( 157 ~; 169 |; 78 &)
% ( 7 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 21 ( 21 usr; 20 con; 0-2 aty)
% Number of variables : 165 ( 16 sgn 42 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(owl_prop_disjointwith_ext,axiom,
! [X,Y] :
( iext(uri_owl_disjointWith,X,Y)
=> ( ic(Y)
& ic(X) ) ),
file('theBenchmark.p',owl_prop_disjointwith_ext) ).
fof(owl_bool_complementof_class,axiom,
! [Z,C] :
( iext(uri_owl_complementOf,Z,C)
=> ( ! [X] :
( icext(Z,X)
<=> ~ icext(C,X) )
& ic(C)
& ic(Z) ) ),
file('theBenchmark.p',owl_bool_complementof_class) ).
fof(owl_bool_intersectionof_class_002,axiom,
! [Z,S1,C1,S2,C2] :
( ( iext(uri_rdf_rest,S2,uri_rdf_nil)
& iext(uri_rdf_first,S2,C2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,C1) )
=> ( iext(uri_owl_intersectionOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( icext(C2,X)
& icext(C1,X) ) )
& ic(C2)
& ic(C1)
& ic(Z) ) ) ),
file('theBenchmark.p',owl_bool_intersectionof_class_002) ).
fof(owl_bool_unionof_class_003,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('theBenchmark.p',owl_bool_unionof_class_003) ).
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_disjointwith,axiom,
! [C1,C2] :
( iext(uri_owl_disjointWith,C1,C2)
<=> ( ! [X] :
~ ( icext(C2,X)
& icext(C1,X) )
& ic(C2)
& ic(C1) ) ),
file('theBenchmark.p',owl_eqdis_disjointwith) ).
fof(testcase_premise_fullish_020_Logical_Complications,axiom,
? [BNODE_xs,BNODE_xc,BNODE_lu1,BNODE_lu2,BNODE_lu3,BNODE_li1,BNODE_li2] :
( iext(uri_owl_complementOf,BNODE_xc,uri_ex_c2)
& iext(uri_rdf_rest,BNODE_li2,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_li2,BNODE_xc)
& iext(uri_rdf_rest,BNODE_li1,BNODE_li2)
& iext(uri_rdf_first,BNODE_li1,uri_ex_c)
& iext(uri_owl_intersectionOf,BNODE_xs,BNODE_li1)
& iext(uri_rdfs_subClassOf,uri_ex_d,BNODE_xs)
& iext(uri_owl_disjointWith,uri_ex_d,uri_ex_c1)
& iext(uri_rdf_rest,BNODE_lu3,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_lu3,uri_ex_c3)
& iext(uri_rdf_rest,BNODE_lu2,BNODE_lu3)
& iext(uri_rdf_first,BNODE_lu2,uri_ex_c2)
& iext(uri_rdf_rest,BNODE_lu1,BNODE_lu2)
& iext(uri_rdf_first,BNODE_lu1,uri_ex_c1)
& iext(uri_owl_unionOf,uri_ex_c,BNODE_lu1) ),
file('theBenchmark.p',testcase_premise_fullish_020_Logical_Complications) ).
fof(testcase_conclusion_fullish_020_Logical_Complications,conjecture,
iext(uri_rdfs_subClassOf,uri_ex_d,uri_ex_c3),
file('theBenchmark.p',testcase_conclusion_fullish_020_Logical_Complications) ).
fof(testcase_conclusion_fullish_020_Logical_Complications_neg,negated_conjecture,
~ iext(uri_rdfs_subClassOf,uri_ex_d,uri_ex_c3),
inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_020_Logical_Complications]) ).
cnf(c_9,plain,
( ic(A)
| ~ iext(uri_owl_disjointWith,A,B) ),
inference(clausify,[status(thm)],[owl_prop_disjointwith_ext]) ).
cnf(c_13,plain,
( ~ icext(B,C)
| ~ icext(A,C)
| ~ iext(uri_owl_complementOf,A,B) ),
inference(clausify,[status(thm)],[owl_bool_complementof_class]) ).
cnf(c_18,plain,
( icext(B,F)
| ~ icext(E,F)
| ~ iext(uri_owl_intersectionOf,E,A)
| ~ iext(uri_rdf_rest,C,uri_rdf_nil)
| ~ iext(uri_rdf_first,C,D)
| ~ iext(uri_rdf_rest,A,C)
| ~ iext(uri_rdf_first,A,B) ),
inference(clausify,[status(thm)],[owl_bool_intersectionof_class_002]) ).
cnf(c_19,plain,
( icext(D,F)
| ~ icext(E,F)
| ~ iext(uri_owl_intersectionOf,E,A)
| ~ iext(uri_rdf_rest,C,uri_rdf_nil)
| ~ iext(uri_rdf_first,C,D)
| ~ iext(uri_rdf_rest,A,C)
| ~ iext(uri_rdf_first,A,B) ),
inference(clausify,[status(thm)],[owl_bool_intersectionof_class_002]) ).
cnf(c_27,plain,
( ic(F)
| ~ iext(uri_owl_unionOf,V6,A)
| ~ iext(uri_rdf_rest,E,uri_rdf_nil)
| ~ iext(uri_rdf_first,E,F)
| ~ iext(uri_rdf_rest,C,E)
| ~ iext(uri_rdf_first,C,D)
| ~ iext(uri_rdf_rest,A,C)
| ~ iext(uri_rdf_first,A,B) ),
inference(clausify,[status(thm)],[owl_bool_unionof_class_003]) ).
cnf(c_28,plain,
( icext(F,V7)
| icext(D,V7)
| icext(B,V7)
| ~ icext(V6,V7)
| ~ iext(uri_owl_unionOf,V6,A)
| ~ iext(uri_rdf_rest,E,uri_rdf_nil)
| ~ iext(uri_rdf_first,E,F)
| ~ iext(uri_rdf_rest,C,E)
| ~ iext(uri_rdf_first,C,D)
| ~ iext(uri_rdf_rest,A,C)
| ~ iext(uri_rdf_first,A,B) ),
inference(clausify,[status(thm)],[owl_bool_unionof_class_003]) ).
fof(nnf_5,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_5]) ).
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_38,plain,
( icext(B,C)
| ~ icext(A,C)
| ~ iext(uri_rdfs_subClassOf,A,B) ),
inference(split_conjunct,[status(thm)],[sk_owl_rdfsext_subclassof]) ).
cnf(c_39,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_40,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]) ).
cnf(c_41,plain,
( ~ icext(B,C)
| ~ icext(A,C)
| ~ iext(uri_owl_disjointWith,A,B) ),
inference(clausify,[status(thm)],[owl_eqdis_disjointwith]) ).
fof(nnf_7,plain,
? [BNODE_xs,BNODE_xc,BNODE_lu1,BNODE_lu2,BNODE_lu3,BNODE_li1,BNODE_li2] :
( iext(uri_owl_complementOf,BNODE_xc,uri_ex_c2)
& iext(uri_rdf_rest,BNODE_li2,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_li2,BNODE_xc)
& iext(uri_rdf_rest,BNODE_li1,BNODE_li2)
& iext(uri_rdf_first,BNODE_li1,uri_ex_c)
& iext(uri_owl_intersectionOf,BNODE_xs,BNODE_li1)
& iext(uri_rdfs_subClassOf,uri_ex_d,BNODE_xs)
& iext(uri_owl_disjointWith,uri_ex_d,uri_ex_c1)
& iext(uri_rdf_rest,BNODE_lu3,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_lu3,uri_ex_c3)
& iext(uri_rdf_rest,BNODE_lu2,BNODE_lu3)
& iext(uri_rdf_first,BNODE_lu2,uri_ex_c2)
& iext(uri_rdf_rest,BNODE_lu1,BNODE_lu2)
& iext(uri_rdf_first,BNODE_lu1,uri_ex_c1)
& iext(uri_owl_unionOf,uri_ex_c,BNODE_lu1) ),
inference(fof_nnf,[status(thm)],[testcase_premise_fullish_020_Logical_Complications]) ).
fof(sk_testcase_premise_fullish_020_Logical_Complications,plain,
( iext(uri_owl_complementOf,sK7,uri_ex_c2)
& iext(uri_rdf_rest,sK6,uri_rdf_nil)
& iext(uri_rdf_first,sK6,sK7)
& iext(uri_rdf_rest,sK5,sK6)
& iext(uri_rdf_first,sK5,uri_ex_c)
& iext(uri_owl_intersectionOf,sK4,sK5)
& iext(uri_rdfs_subClassOf,uri_ex_d,sK4)
& iext(uri_owl_disjointWith,uri_ex_d,uri_ex_c1)
& iext(uri_rdf_rest,sK3,uri_rdf_nil)
& iext(uri_rdf_first,sK3,uri_ex_c3)
& iext(uri_rdf_rest,sK2,sK3)
& iext(uri_rdf_first,sK2,uri_ex_c2)
& iext(uri_rdf_rest,sK1,sK2)
& iext(uri_rdf_first,sK1,uri_ex_c1)
& iext(uri_owl_unionOf,uri_ex_c,sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5,sK6,sK7]),skolemize(BNODE_xs,sK4),skolemize(BNODE_xc,sK7),skolemize(BNODE_lu1,sK1),skolemize(BNODE_lu2,sK2),skolemize(BNODE_lu3,sK3),skolemize(BNODE_li1,sK5),skolemize(BNODE_li2,sK6)],[nnf_7]) ).
cnf(c_44,plain,
iext(uri_owl_unionOf,uri_ex_c,sK1),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_020_Logical_Complications]) ).
cnf(c_45,plain,
iext(uri_rdf_first,sK1,uri_ex_c1),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_020_Logical_Complications]) ).
cnf(c_46,plain,
iext(uri_rdf_rest,sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_020_Logical_Complications]) ).
cnf(c_47,plain,
iext(uri_rdf_first,sK2,uri_ex_c2),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_020_Logical_Complications]) ).
cnf(c_48,plain,
iext(uri_rdf_rest,sK2,sK3),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_020_Logical_Complications]) ).
cnf(c_49,plain,
iext(uri_rdf_first,sK3,uri_ex_c3),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_020_Logical_Complications]) ).
cnf(c_50,plain,
iext(uri_rdf_rest,sK3,uri_rdf_nil),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_020_Logical_Complications]) ).
cnf(c_51,plain,
iext(uri_owl_disjointWith,uri_ex_d,uri_ex_c1),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_020_Logical_Complications]) ).
cnf(c_52,plain,
iext(uri_rdfs_subClassOf,uri_ex_d,sK4),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_020_Logical_Complications]) ).
cnf(c_53,plain,
iext(uri_owl_intersectionOf,sK4,sK5),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_020_Logical_Complications]) ).
cnf(c_54,plain,
iext(uri_rdf_first,sK5,uri_ex_c),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_020_Logical_Complications]) ).
cnf(c_55,plain,
iext(uri_rdf_rest,sK5,sK6),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_020_Logical_Complications]) ).
cnf(c_56,plain,
iext(uri_rdf_first,sK6,sK7),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_020_Logical_Complications]) ).
cnf(c_57,plain,
iext(uri_rdf_rest,sK6,uri_rdf_nil),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_020_Logical_Complications]) ).
cnf(c_58,plain,
iext(uri_owl_complementOf,sK7,uri_ex_c2),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_020_Logical_Complications]) ).
cnf(c_59,negated_conjecture,
~ iext(uri_rdfs_subClassOf,uri_ex_d,uri_ex_c3),
inference(clausify,[status(thm)],[testcase_conclusion_fullish_020_Logical_Complications_neg]) ).
cnf(c_411,plain,
( icext(E,F)
| icext(C,F)
| icext(A,F)
| ~ icext(uri_ex_c,F)
| ~ iext(uri_rdf_rest,D,uri_rdf_nil)
| ~ iext(uri_rdf_first,D,E)
| ~ iext(uri_rdf_rest,B,D)
| ~ iext(uri_rdf_first,B,C)
| ~ iext(uri_rdf_rest,sK1,B)
| ~ iext(uri_rdf_first,sK1,A) ),
inference(resolve,[status(thm)],[c_44,c_28]) ).
cnf(c_6389,plain,
( ic(D)
| ~ iext(uri_owl_unionOf,E,sK1)
| ~ iext(uri_rdf_rest,C,uri_rdf_nil)
| ~ iext(uri_rdf_first,C,D)
| ~ iext(uri_rdf_rest,A,C)
| ~ iext(uri_rdf_first,A,B)
| ~ iext(uri_rdf_rest,sK1,A) ),
inference(resolve,[status(thm)],[c_27,c_45]) ).
cnf(c_6390,plain,
( ic(C)
| ~ iext(uri_owl_unionOf,D,sK1)
| ~ iext(uri_rdf_rest,B,uri_rdf_nil)
| ~ iext(uri_rdf_first,B,C)
| ~ iext(uri_rdf_rest,sK2,B)
| ~ iext(uri_rdf_first,sK2,A) ),
inference(resolve,[status(thm)],[c_6389,c_46]) ).
cnf(c_6391,plain,
( ic(B)
| ~ iext(uri_owl_unionOf,C,sK1)
| ~ iext(uri_rdf_rest,A,uri_rdf_nil)
| ~ iext(uri_rdf_first,A,B)
| ~ iext(uri_rdf_rest,sK2,A) ),
inference(resolve,[status(thm)],[c_6390,c_47]) ).
cnf(c_6392,plain,
( ic(A)
| ~ iext(uri_owl_unionOf,B,sK1)
| ~ iext(uri_rdf_rest,sK3,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK3,A) ),
inference(resolve,[status(thm)],[c_6391,c_48]) ).
cnf(c_6393,plain,
( ic(uri_ex_c3)
| ~ iext(uri_owl_unionOf,A,sK1)
| ~ iext(uri_rdf_rest,sK3,uri_rdf_nil) ),
inference(resolve,[status(thm)],[c_6392,c_49]) ).
cnf(c_6394,plain,
( ic(uri_ex_c3)
| ~ iext(uri_owl_unionOf,A,sK1) ),
inference(resolve,[status(thm)],[c_6393,c_50]) ).
cnf(c_2343,plain,
ic(uri_ex_c3),
inference(resolve,[status(thm)],[c_6394,c_44]) ).
cnf(c_3631,plain,
( ~ icext(uri_ex_c1,A)
| ~ icext(uri_ex_d,A) ),
inference(resolve,[status(thm)],[c_51,c_41]) ).
cnf(c_3632,plain,
ic(uri_ex_d),
inference(resolve,[status(thm)],[c_51,c_9]) ).
cnf(c_3633,plain,
( icext(sK4,A)
| ~ icext(uri_ex_d,A) ),
inference(resolve,[status(thm)],[c_52,c_38]) ).
cnf(c_5349,plain,
( ~ icext(uri_ex_c2,A)
| ~ icext(sK7,A) ),
inference(resolve,[status(thm)],[c_58,c_13]) ).
cnf(c_6395,plain,
( icext(uri_ex_d,sK0(uri_ex_d,A))
| ~ ic(A)
| iext(uri_rdfs_subClassOf,uri_ex_d,A) ),
inference(resolve,[status(thm)],[c_39,c_3632]) ).
cnf(c_6396,plain,
( icext(uri_ex_d,sK0(uri_ex_d,uri_ex_c3))
| iext(uri_rdfs_subClassOf,uri_ex_d,uri_ex_c3) ),
inference(resolve,[status(thm)],[c_6395,c_2343]) ).
cnf(c_6039,negated_conjecture,
icext(uri_ex_d,sK0(uri_ex_d,uri_ex_c3)),
inference(resolve,[status(thm)],[c_59,c_6396]) ).
cnf(c_6397,negated_conjecture,
( ~ icext(uri_ex_c3,sK0(uri_ex_d,uri_ex_c3))
| ~ ic(uri_ex_c3)
| ~ ic(uri_ex_d) ),
inference(resolve,[status(thm)],[c_40,c_59]) ).
cnf(c_6398,negated_conjecture,
( ~ icext(uri_ex_c3,sK0(uri_ex_d,uri_ex_c3))
| ~ ic(uri_ex_c3) ),
inference(resolve,[status(thm)],[c_6397,c_3632]) ).
cnf(c_6043,negated_conjecture,
~ icext(uri_ex_c3,sK0(uri_ex_d,uri_ex_c3)),
inference(resolve,[status(thm)],[c_6398,c_2343]) ).
cnf(c_6293,plain,
icext(sK4,sK0(uri_ex_d,uri_ex_c3)),
inference(resolve,[status(thm)],[c_6039,c_3633]) ).
cnf(c_6294,plain,
~ icext(uri_ex_c1,sK0(uri_ex_d,uri_ex_c3)),
inference(resolve,[status(thm)],[c_6039,c_3631]) ).
cnf(c_6399,plain,
( icext(B,D)
| ~ icext(C,D)
| ~ iext(uri_owl_intersectionOf,C,sK5)
| ~ iext(uri_rdf_rest,A,uri_rdf_nil)
| ~ iext(uri_rdf_first,A,B)
| ~ iext(uri_rdf_rest,sK5,A) ),
inference(resolve,[status(thm)],[c_19,c_54]) ).
cnf(c_6400,plain,
( icext(A,C)
| ~ icext(B,C)
| ~ iext(uri_owl_intersectionOf,B,sK5)
| ~ iext(uri_rdf_rest,sK6,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK6,A) ),
inference(resolve,[status(thm)],[c_6399,c_55]) ).
cnf(c_6401,plain,
( icext(sK7,B)
| ~ icext(A,B)
| ~ iext(uri_owl_intersectionOf,A,sK5)
| ~ iext(uri_rdf_rest,sK6,uri_rdf_nil) ),
inference(resolve,[status(thm)],[c_6400,c_56]) ).
cnf(c_6402,plain,
( icext(sK7,B)
| ~ icext(A,B)
| ~ iext(uri_owl_intersectionOf,A,sK5) ),
inference(resolve,[status(thm)],[c_6401,c_57]) ).
cnf(c_6403,plain,
( icext(sK7,A)
| ~ icext(sK4,A) ),
inference(resolve,[status(thm)],[c_6402,c_53]) ).
cnf(c_6325,plain,
icext(sK7,sK0(uri_ex_d,uri_ex_c3)),
inference(resolve,[status(thm)],[c_6403,c_6293]) ).
cnf(c_6404,plain,
( icext(uri_ex_c,D)
| ~ icext(C,D)
| ~ iext(uri_owl_intersectionOf,C,sK5)
| ~ iext(uri_rdf_rest,A,uri_rdf_nil)
| ~ iext(uri_rdf_first,A,B)
| ~ iext(uri_rdf_rest,sK5,A) ),
inference(resolve,[status(thm)],[c_18,c_54]) ).
cnf(c_6405,plain,
( icext(uri_ex_c,C)
| ~ icext(B,C)
| ~ iext(uri_owl_intersectionOf,B,sK5)
| ~ iext(uri_rdf_rest,sK6,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK6,A) ),
inference(resolve,[status(thm)],[c_6404,c_55]) ).
cnf(c_6406,plain,
( icext(uri_ex_c,B)
| ~ icext(A,B)
| ~ iext(uri_owl_intersectionOf,A,sK5)
| ~ iext(uri_rdf_rest,sK6,uri_rdf_nil) ),
inference(resolve,[status(thm)],[c_6405,c_56]) ).
cnf(c_6407,plain,
( icext(uri_ex_c,B)
| ~ icext(A,B)
| ~ iext(uri_owl_intersectionOf,A,sK5) ),
inference(resolve,[status(thm)],[c_6406,c_57]) ).
cnf(c_6408,plain,
( icext(uri_ex_c,A)
| ~ icext(sK4,A) ),
inference(resolve,[status(thm)],[c_6407,c_53]) ).
cnf(c_6326,plain,
icext(uri_ex_c,sK0(uri_ex_d,uri_ex_c3)),
inference(resolve,[status(thm)],[c_6408,c_6293]) ).
cnf(c_6354,plain,
~ icext(uri_ex_c2,sK0(uri_ex_d,uri_ex_c3)),
inference(resolve,[status(thm)],[c_6325,c_5349]) ).
cnf(c_6409,plain,
( icext(D,E)
| icext(B,E)
| icext(uri_ex_c1,E)
| ~ icext(uri_ex_c,E)
| ~ iext(uri_rdf_rest,C,uri_rdf_nil)
| ~ iext(uri_rdf_first,C,D)
| ~ iext(uri_rdf_rest,A,C)
| ~ iext(uri_rdf_first,A,B)
| ~ iext(uri_rdf_rest,sK1,A) ),
inference(resolve,[status(thm)],[c_411,c_45]) ).
cnf(c_6410,plain,
( icext(C,D)
| icext(A,D)
| icext(uri_ex_c1,D)
| ~ icext(uri_ex_c,D)
| ~ iext(uri_rdf_rest,B,uri_rdf_nil)
| ~ iext(uri_rdf_first,B,C)
| ~ iext(uri_rdf_rest,sK2,B)
| ~ iext(uri_rdf_first,sK2,A) ),
inference(resolve,[status(thm)],[c_6409,c_46]) ).
cnf(c_6411,plain,
( icext(B,C)
| icext(uri_ex_c2,C)
| icext(uri_ex_c1,C)
| ~ icext(uri_ex_c,C)
| ~ iext(uri_rdf_rest,A,uri_rdf_nil)
| ~ iext(uri_rdf_first,A,B)
| ~ iext(uri_rdf_rest,sK2,A) ),
inference(resolve,[status(thm)],[c_6410,c_47]) ).
cnf(c_6412,plain,
( icext(A,B)
| icext(uri_ex_c2,B)
| icext(uri_ex_c1,B)
| ~ icext(uri_ex_c,B)
| ~ iext(uri_rdf_rest,sK3,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK3,A) ),
inference(resolve,[status(thm)],[c_6411,c_48]) ).
cnf(c_6413,plain,
( icext(uri_ex_c3,A)
| icext(uri_ex_c2,A)
| icext(uri_ex_c1,A)
| ~ icext(uri_ex_c,A)
| ~ iext(uri_rdf_rest,sK3,uri_rdf_nil) ),
inference(resolve,[status(thm)],[c_6412,c_49]) ).
cnf(c_6414,plain,
( icext(uri_ex_c3,A)
| icext(uri_ex_c2,A)
| icext(uri_ex_c1,A)
| ~ icext(uri_ex_c,A) ),
inference(resolve,[status(thm)],[c_6413,c_50]) ).
cnf(c_6415,plain,
( icext(uri_ex_c3,sK0(uri_ex_d,uri_ex_c3))
| icext(uri_ex_c2,sK0(uri_ex_d,uri_ex_c3))
| icext(uri_ex_c1,sK0(uri_ex_d,uri_ex_c3)) ),
inference(resolve,[status(thm)],[c_6414,c_6326]) ).
cnf(c_6416,plain,
( icext(uri_ex_c3,sK0(uri_ex_d,uri_ex_c3))
| icext(uri_ex_c2,sK0(uri_ex_d,uri_ex_c3)) ),
inference(resolve,[status(thm)],[c_6294,c_6415]) ).
cnf(c_6417,plain,
icext(uri_ex_c3,sK0(uri_ex_d,uri_ex_c3)),
inference(resolve,[status(thm)],[c_6354,c_6416]) ).
cnf(c_6388,plain,
$false,
inference(resolve,[status(thm)],[c_6043,c_6417]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWB020+2 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n011.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:47:31 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 417226 was started by sandbox on n011,
% 0.08/0.36 % Sat Sep 26 11:47:31 2026
% 0.08/0.36 % 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).
% 58.97/16.26
% 58.97/16.26 % SZS status Theorem for theBenchmark
% 58.97/16.26
% 58.97/16.26 % Proof 1 at 3.82 (+ 0.36) seconds.
% 58.97/16.26 % Length of proof is 48.
% 58.97/16.26 % Level of proof is 7.
% 58.97/16.26 % Maximum clause weight is 42.000.
% 58.97/16.26 % Given clauses 380.
% 58.97/16.26
% 58.97/16.26 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------