%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWB021+2 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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 68.04s 10.23s
% Output : CNFRefutation 68.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 8
% Syntax : Number of formulae : 172 ( 39 unt; 0 def)
% Number of atoms : 785 ( 178 equ)
% Maximal formula atoms : 22 ( 4 avg)
% Number of connectives : 1001 ( 388 ~; 502 |; 98 &)
% ( 8 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 23 con; 0-2 aty)
% Number of variables : 351 ( 45 sgn 47 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(owl_prop_oneof_ext,axiom,
! [X,Y] :
( iext(uri_owl_oneOf,X,Y)
=> ( icext(uri_rdf_List,Y)
& ic(X) ) ),
file('theBenchmark.p',owl_prop_oneof_ext) ).
fof(owl_prop_unionof_ext,axiom,
! [X,Y] :
( iext(uri_owl_unionOf,X,Y)
=> ( icext(uri_rdf_List,Y)
& ic(X) ) ),
file('theBenchmark.p',owl_prop_unionof_ext) ).
fof(owl_bool_unionof_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_unionOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( icext(C2,X)
| icext(C1,X) ) )
& ic(C2)
& ic(C1)
& ic(Z) ) ) ),
file('theBenchmark.p',owl_bool_unionof_class_002) ).
fof(owl_enum_class_002,axiom,
! [Z,S1,A1,S2,A2] :
( ( iext(uri_rdf_rest,S2,uri_rdf_nil)
& iext(uri_rdf_first,S2,A2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,A1) )
=> ( iext(uri_owl_oneOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( X = A2
| X = A1 ) )
& ic(Z) ) ) ),
file('theBenchmark.p',owl_enum_class_002) ).
fof(owl_enum_class_003,axiom,
! [Z,S1,A1,S2,A2,S3,A3] :
( ( iext(uri_rdf_rest,S3,uri_rdf_nil)
& iext(uri_rdf_first,S3,A3)
& iext(uri_rdf_rest,S2,S3)
& iext(uri_rdf_first,S2,A2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,A1) )
=> ( iext(uri_owl_oneOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( X = A3
| X = A2
| X = A1 ) )
& ic(Z) ) ) ),
file('theBenchmark.p',owl_enum_class_003) ).
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_premise_fullish_021_Composite_Enumerations,axiom,
? [BNODE_l11,BNODE_l12,BNODE_l21,BNODE_l22,BNODE_l31,BNODE_l32,BNODE_l33,BNODE_l41,BNODE_l42] :
( iext(uri_rdf_rest,BNODE_l42,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l42,uri_ex_c2)
& iext(uri_rdf_rest,BNODE_l41,BNODE_l42)
& iext(uri_rdf_first,BNODE_l41,uri_ex_c1)
& iext(uri_owl_unionOf,uri_ex_c4,BNODE_l41)
& iext(uri_rdf_rest,BNODE_l33,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l33,uri_ex_w3)
& iext(uri_rdf_rest,BNODE_l32,BNODE_l33)
& iext(uri_rdf_first,BNODE_l32,uri_ex_w2)
& iext(uri_rdf_rest,BNODE_l31,BNODE_l32)
& iext(uri_rdf_first,BNODE_l31,uri_ex_w1)
& iext(uri_owl_oneOf,uri_ex_c3,BNODE_l31)
& iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l22,uri_ex_w3)
& iext(uri_rdf_rest,BNODE_l21,BNODE_l22)
& iext(uri_rdf_first,BNODE_l21,uri_ex_w2)
& iext(uri_owl_oneOf,uri_ex_c2,BNODE_l21)
& iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l12,uri_ex_w2)
& iext(uri_rdf_rest,BNODE_l11,BNODE_l12)
& iext(uri_rdf_first,BNODE_l11,uri_ex_w1)
& iext(uri_owl_oneOf,uri_ex_c1,BNODE_l11) ),
file('theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
fof(testcase_conclusion_fullish_021_Composite_Enumerations,conjecture,
iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4),
file('theBenchmark.p',testcase_conclusion_fullish_021_Composite_Enumerations) ).
fof(testcase_conclusion_fullish_021_Composite_Enumerations_neg,negated_conjecture,
~ iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4),
inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_021_Composite_Enumerations]) ).
cnf(c_9,plain,
( ic(A)
| ~ iext(uri_owl_oneOf,A,B) ),
inference(clausify,[status(thm)],[owl_prop_oneof_ext]) ).
cnf(c_11,plain,
( ic(A)
| ~ iext(uri_owl_unionOf,A,B) ),
inference(clausify,[status(thm)],[owl_prop_unionof_ext]) ).
cnf(c_15,plain,
( icext(D,F)
| icext(B,F)
| ~ icext(E,F)
| ~ iext(uri_owl_unionOf,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_unionof_class_002]) ).
cnf(c_16,plain,
( ~ icext(B,F)
| icext(E,F)
| ~ iext(uri_owl_unionOf,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_unionof_class_002]) ).
cnf(c_17,plain,
( ~ icext(D,F)
| icext(E,F)
| ~ iext(uri_owl_unionOf,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_unionof_class_002]) ).
cnf(c_21,plain,
( D = F
| B = F
| ~ icext(E,F)
| ~ iext(uri_owl_oneOf,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_enum_class_002]) ).
cnf(c_22,plain,
( B != F
| icext(E,F)
| ~ iext(uri_owl_oneOf,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_enum_class_002]) ).
cnf(c_23,plain,
( D != F
| icext(E,F)
| ~ iext(uri_owl_oneOf,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_enum_class_002]) ).
cnf(c_30,plain,
( F = V7
| D = V7
| B = V7
| ~ icext(V6,V7)
| ~ iext(uri_owl_oneOf,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_enum_class_003]) ).
cnf(c_31,plain,
( B != V7
| icext(V6,V7)
| ~ iext(uri_owl_oneOf,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_enum_class_003]) ).
cnf(c_32,plain,
( D != V7
| icext(V6,V7)
| ~ iext(uri_owl_oneOf,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_enum_class_003]) ).
cnf(c_33,plain,
( F != V7
| icext(V6,V7)
| ~ iext(uri_owl_oneOf,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_enum_class_003]) ).
fof(nnf_6,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,sK0(C1,C2))
| ~ icext(C1,sK0(C1,C2)) )
& ( icext(C2,sK0(C1,C2))
| icext(C1,sK0(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,[sK0]),skolemize(X,sK0(C1,C2))],[nnf_6]) ).
fof(sk_owl_eqdis_equivalentclass,plain,
( ! [VAR_0,VAR_1] :
( ~ icext(VAR_1,sK0(VAR_0,VAR_1))
| ~ icext(VAR_0,sK0(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,sK0(VAR_0,VAR_1))
| icext(VAR_0,sK0(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_46,plain,
( icext(B,sK0(A,B))
| icext(A,sK0(A,B))
| ~ ic(B)
| ~ ic(A)
| iext(uri_owl_equivalentClass,A,B) ),
inference(split_conjunct,[status(thm)],[sk_owl_eqdis_equivalentclass]) ).
cnf(c_47,plain,
( ~ icext(B,sK0(A,B))
| ~ icext(A,sK0(A,B))
| ~ ic(B)
| ~ ic(A)
| iext(uri_owl_equivalentClass,A,B) ),
inference(split_conjunct,[status(thm)],[sk_owl_eqdis_equivalentclass]) ).
fof(nnf_7,plain,
? [BNODE_l11,BNODE_l12,BNODE_l21,BNODE_l22,BNODE_l31,BNODE_l32,BNODE_l33,BNODE_l41,BNODE_l42] :
( iext(uri_rdf_rest,BNODE_l42,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l42,uri_ex_c2)
& iext(uri_rdf_rest,BNODE_l41,BNODE_l42)
& iext(uri_rdf_first,BNODE_l41,uri_ex_c1)
& iext(uri_owl_unionOf,uri_ex_c4,BNODE_l41)
& iext(uri_rdf_rest,BNODE_l33,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l33,uri_ex_w3)
& iext(uri_rdf_rest,BNODE_l32,BNODE_l33)
& iext(uri_rdf_first,BNODE_l32,uri_ex_w2)
& iext(uri_rdf_rest,BNODE_l31,BNODE_l32)
& iext(uri_rdf_first,BNODE_l31,uri_ex_w1)
& iext(uri_owl_oneOf,uri_ex_c3,BNODE_l31)
& iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l22,uri_ex_w3)
& iext(uri_rdf_rest,BNODE_l21,BNODE_l22)
& iext(uri_rdf_first,BNODE_l21,uri_ex_w2)
& iext(uri_owl_oneOf,uri_ex_c2,BNODE_l21)
& iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l12,uri_ex_w2)
& iext(uri_rdf_rest,BNODE_l11,BNODE_l12)
& iext(uri_rdf_first,BNODE_l11,uri_ex_w1)
& iext(uri_owl_oneOf,uri_ex_c1,BNODE_l11) ),
inference(fof_nnf,[status(thm)],[testcase_premise_fullish_021_Composite_Enumerations]) ).
fof(sk_testcase_premise_fullish_021_Composite_Enumerations,plain,
( iext(uri_rdf_rest,sK9,uri_rdf_nil)
& iext(uri_rdf_first,sK9,uri_ex_c2)
& iext(uri_rdf_rest,sK8,sK9)
& iext(uri_rdf_first,sK8,uri_ex_c1)
& iext(uri_owl_unionOf,uri_ex_c4,sK8)
& iext(uri_rdf_rest,sK7,uri_rdf_nil)
& iext(uri_rdf_first,sK7,uri_ex_w3)
& iext(uri_rdf_rest,sK6,sK7)
& iext(uri_rdf_first,sK6,uri_ex_w2)
& iext(uri_rdf_rest,sK5,sK6)
& iext(uri_rdf_first,sK5,uri_ex_w1)
& iext(uri_owl_oneOf,uri_ex_c3,sK5)
& iext(uri_rdf_rest,sK4,uri_rdf_nil)
& iext(uri_rdf_first,sK4,uri_ex_w3)
& iext(uri_rdf_rest,sK3,sK4)
& iext(uri_rdf_first,sK3,uri_ex_w2)
& iext(uri_owl_oneOf,uri_ex_c2,sK3)
& iext(uri_rdf_rest,sK2,uri_rdf_nil)
& iext(uri_rdf_first,sK2,uri_ex_w2)
& iext(uri_rdf_rest,sK1,sK2)
& iext(uri_rdf_first,sK1,uri_ex_w1)
& iext(uri_owl_oneOf,uri_ex_c1,sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9]),skolemize(BNODE_l11,sK1),skolemize(BNODE_l12,sK2),skolemize(BNODE_l21,sK3),skolemize(BNODE_l22,sK4),skolemize(BNODE_l31,sK5),skolemize(BNODE_l32,sK6),skolemize(BNODE_l33,sK7),skolemize(BNODE_l41,sK8),skolemize(BNODE_l42,sK9)],[nnf_7]) ).
cnf(c_48,plain,
iext(uri_owl_oneOf,uri_ex_c1,sK1),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_49,plain,
iext(uri_rdf_first,sK1,uri_ex_w1),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_50,plain,
iext(uri_rdf_rest,sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_51,plain,
iext(uri_rdf_first,sK2,uri_ex_w2),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_52,plain,
iext(uri_rdf_rest,sK2,uri_rdf_nil),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_53,plain,
iext(uri_owl_oneOf,uri_ex_c2,sK3),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_54,plain,
iext(uri_rdf_first,sK3,uri_ex_w2),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_55,plain,
iext(uri_rdf_rest,sK3,sK4),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_56,plain,
iext(uri_rdf_first,sK4,uri_ex_w3),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_57,plain,
iext(uri_rdf_rest,sK4,uri_rdf_nil),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_58,plain,
iext(uri_owl_oneOf,uri_ex_c3,sK5),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_59,plain,
iext(uri_rdf_first,sK5,uri_ex_w1),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_60,plain,
iext(uri_rdf_rest,sK5,sK6),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_61,plain,
iext(uri_rdf_first,sK6,uri_ex_w2),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_62,plain,
iext(uri_rdf_rest,sK6,sK7),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_63,plain,
iext(uri_rdf_first,sK7,uri_ex_w3),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_64,plain,
iext(uri_rdf_rest,sK7,uri_rdf_nil),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_65,plain,
iext(uri_owl_unionOf,uri_ex_c4,sK8),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_66,plain,
iext(uri_rdf_first,sK8,uri_ex_c1),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_67,plain,
iext(uri_rdf_rest,sK8,sK9),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_68,plain,
iext(uri_rdf_first,sK9,uri_ex_c2),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_69,plain,
iext(uri_rdf_rest,sK9,uri_rdf_nil),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_021_Composite_Enumerations]) ).
cnf(c_70,negated_conjecture,
~ iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4),
inference(clausify,[status(thm)],[testcase_conclusion_fullish_021_Composite_Enumerations_neg]) ).
cnf(c_209,plain,
( A != D
| icext(uri_ex_c1,D)
| ~ iext(uri_rdf_rest,B,uri_rdf_nil)
| ~ iext(uri_rdf_first,B,C)
| ~ iext(uri_rdf_rest,sK1,B)
| ~ iext(uri_rdf_first,sK1,A) ),
inference(resolve,[status(thm)],[c_48,c_22]) ).
cnf(c_210,plain,
( C = D
| A = D
| ~ icext(uri_ex_c1,D)
| ~ iext(uri_rdf_rest,B,uri_rdf_nil)
| ~ iext(uri_rdf_first,B,C)
| ~ iext(uri_rdf_rest,sK1,B)
| ~ iext(uri_rdf_first,sK1,A) ),
inference(resolve,[status(thm)],[c_48,c_21]) ).
cnf(c_13199,plain,
( B != D
| icext(C,D)
| ~ iext(uri_owl_oneOf,C,sK3)
| ~ iext(uri_rdf_rest,sK4,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK4,B)
| ~ iext(uri_rdf_first,sK3,A) ),
inference(resolve,[status(thm)],[c_55,c_23]) ).
cnf(c_1005,plain,
( B != D
| icext(C,D)
| ~ iext(uri_owl_oneOf,C,sK3)
| ~ iext(uri_rdf_first,sK4,B)
| ~ iext(uri_rdf_first,sK3,A) ),
inference(resolve,[status(thm)],[c_57,c_13199]) ).
cnf(c_13200,plain,
( A != D
| icext(C,D)
| ~ iext(uri_owl_oneOf,C,sK3)
| ~ iext(uri_rdf_rest,sK4,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK4,B)
| ~ iext(uri_rdf_first,sK3,A) ),
inference(resolve,[status(thm)],[c_55,c_22]) ).
cnf(c_1006,plain,
( A != D
| icext(C,D)
| ~ iext(uri_owl_oneOf,C,sK3)
| ~ iext(uri_rdf_first,sK4,B)
| ~ iext(uri_rdf_first,sK3,A) ),
inference(resolve,[status(thm)],[c_57,c_13200]) ).
cnf(c_13201,plain,
( B = D
| A = D
| ~ icext(C,D)
| ~ iext(uri_owl_oneOf,C,sK3)
| ~ iext(uri_rdf_rest,sK4,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK4,B)
| ~ iext(uri_rdf_first,sK3,A) ),
inference(resolve,[status(thm)],[c_55,c_21]) ).
cnf(c_1007,plain,
( B = D
| A = D
| ~ icext(C,D)
| ~ iext(uri_owl_oneOf,C,sK3)
| ~ iext(uri_rdf_first,sK4,B)
| ~ iext(uri_rdf_first,sK3,A) ),
inference(resolve,[status(thm)],[c_57,c_13201]) ).
cnf(c_1379,plain,
( E = F
| C = F
| A = F
| ~ icext(uri_ex_c3,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,sK5,B)
| ~ iext(uri_rdf_first,sK5,A) ),
inference(resolve,[status(thm)],[c_58,c_30]) ).
cnf(c_1384,plain,
ic(uri_ex_c3),
inference(resolve,[status(thm)],[c_58,c_9]) ).
cnf(c_13202,plain,
( D != F
| icext(E,F)
| ~ iext(uri_owl_oneOf,E,A)
| ~ iext(uri_rdf_rest,sK7,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK7,D)
| ~ iext(uri_rdf_first,sK6,C)
| ~ iext(uri_rdf_rest,A,sK6)
| ~ iext(uri_rdf_first,A,B) ),
inference(resolve,[status(thm)],[c_62,c_33]) ).
cnf(c_1831,plain,
( D != F
| icext(E,F)
| ~ iext(uri_owl_oneOf,E,A)
| ~ iext(uri_rdf_first,sK7,D)
| ~ iext(uri_rdf_first,sK6,C)
| ~ iext(uri_rdf_rest,A,sK6)
| ~ iext(uri_rdf_first,A,B) ),
inference(resolve,[status(thm)],[c_64,c_13202]) ).
cnf(c_13203,plain,
( C != F
| icext(E,F)
| ~ iext(uri_owl_oneOf,E,A)
| ~ iext(uri_rdf_rest,sK7,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK7,D)
| ~ iext(uri_rdf_first,sK6,C)
| ~ iext(uri_rdf_rest,A,sK6)
| ~ iext(uri_rdf_first,A,B) ),
inference(resolve,[status(thm)],[c_62,c_32]) ).
cnf(c_1833,plain,
( C != F
| icext(E,F)
| ~ iext(uri_owl_oneOf,E,A)
| ~ iext(uri_rdf_first,sK7,D)
| ~ iext(uri_rdf_first,sK6,C)
| ~ iext(uri_rdf_rest,A,sK6)
| ~ iext(uri_rdf_first,A,B) ),
inference(resolve,[status(thm)],[c_64,c_13203]) ).
cnf(c_13204,plain,
( B != F
| icext(E,F)
| ~ iext(uri_owl_oneOf,E,A)
| ~ iext(uri_rdf_rest,sK7,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK7,D)
| ~ iext(uri_rdf_first,sK6,C)
| ~ iext(uri_rdf_rest,A,sK6)
| ~ iext(uri_rdf_first,A,B) ),
inference(resolve,[status(thm)],[c_62,c_31]) ).
cnf(c_1835,plain,
( B != F
| icext(E,F)
| ~ iext(uri_owl_oneOf,E,A)
| ~ iext(uri_rdf_first,sK7,D)
| ~ iext(uri_rdf_first,sK6,C)
| ~ iext(uri_rdf_rest,A,sK6)
| ~ iext(uri_rdf_first,A,B) ),
inference(resolve,[status(thm)],[c_64,c_13204]) ).
cnf(c_2219,plain,
ic(uri_ex_c4),
inference(resolve,[status(thm)],[c_65,c_11]) ).
cnf(c_13205,plain,
( ~ icext(B,D)
| icext(C,D)
| ~ iext(uri_owl_unionOf,C,sK8)
| ~ iext(uri_rdf_rest,sK9,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK9,B)
| ~ iext(uri_rdf_first,sK8,A) ),
inference(resolve,[status(thm)],[c_67,c_17]) ).
cnf(c_2412,plain,
( ~ icext(B,D)
| icext(C,D)
| ~ iext(uri_owl_unionOf,C,sK8)
| ~ iext(uri_rdf_first,sK9,B)
| ~ iext(uri_rdf_first,sK8,A) ),
inference(resolve,[status(thm)],[c_69,c_13205]) ).
cnf(c_13206,plain,
( ~ icext(A,D)
| icext(C,D)
| ~ iext(uri_owl_unionOf,C,sK8)
| ~ iext(uri_rdf_rest,sK9,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK9,B)
| ~ iext(uri_rdf_first,sK8,A) ),
inference(resolve,[status(thm)],[c_67,c_16]) ).
cnf(c_2413,plain,
( ~ icext(A,D)
| icext(C,D)
| ~ iext(uri_owl_unionOf,C,sK8)
| ~ iext(uri_rdf_first,sK9,B)
| ~ iext(uri_rdf_first,sK8,A) ),
inference(resolve,[status(thm)],[c_69,c_13206]) ).
cnf(c_13207,plain,
( icext(B,D)
| icext(A,D)
| ~ icext(C,D)
| ~ iext(uri_owl_unionOf,C,sK8)
| ~ iext(uri_rdf_rest,sK9,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK9,B)
| ~ iext(uri_rdf_first,sK8,A) ),
inference(resolve,[status(thm)],[c_67,c_15]) ).
cnf(c_2414,plain,
( icext(B,D)
| icext(A,D)
| ~ icext(C,D)
| ~ iext(uri_owl_unionOf,C,sK8)
| ~ iext(uri_rdf_first,sK9,B)
| ~ iext(uri_rdf_first,sK8,A) ),
inference(resolve,[status(thm)],[c_69,c_13207]) ).
cnf(c_3225,plain,
( icext(A,sK0(uri_ex_c3,A))
| icext(uri_ex_c3,sK0(uri_ex_c3,A))
| ~ ic(A)
| iext(uri_owl_equivalentClass,uri_ex_c3,A) ),
inference(resolve,[status(thm)],[c_1384,c_46]) ).
cnf(c_13208,plain,
( A != B
| icext(uri_ex_c1,B)
| ~ iext(uri_rdf_rest,sK2,uri_rdf_nil)
| ~ iext(uri_rdf_rest,sK1,sK2)
| ~ iext(uri_rdf_first,sK1,A) ),
inference(resolve,[status(thm)],[c_209,c_51]) ).
cnf(c_13209,plain,
( A != B
| icext(uri_ex_c1,B)
| ~ iext(uri_rdf_rest,sK2,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK1,A) ),
inference(resolve,[status(thm)],[c_50,c_13208]) ).
cnf(c_3538,plain,
( A != B
| icext(uri_ex_c1,B)
| ~ iext(uri_rdf_first,sK1,A) ),
inference(resolve,[status(thm)],[c_52,c_13209]) ).
cnf(c_3539,plain,
( uri_ex_w1 != A
| icext(uri_ex_c1,A) ),
inference(resolve,[status(thm)],[c_3538,c_49]) ).
cnf(c_3540,plain,
icext(uri_ex_c1,uri_ex_w1),
inference(xxres,[status(thm)],[c_3539]) ).
cnf(c_13210,plain,
( uri_ex_w2 = B
| A = B
| ~ icext(uri_ex_c1,B)
| ~ iext(uri_rdf_rest,sK2,uri_rdf_nil)
| ~ iext(uri_rdf_rest,sK1,sK2)
| ~ iext(uri_rdf_first,sK1,A) ),
inference(resolve,[status(thm)],[c_210,c_51]) ).
cnf(c_13211,plain,
( uri_ex_w2 = B
| A = B
| ~ icext(uri_ex_c1,B)
| ~ iext(uri_rdf_rest,sK2,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK1,A) ),
inference(resolve,[status(thm)],[c_50,c_13210]) ).
cnf(c_3550,plain,
( uri_ex_w2 = B
| A = B
| ~ icext(uri_ex_c1,B)
| ~ iext(uri_rdf_first,sK1,A) ),
inference(resolve,[status(thm)],[c_52,c_13211]) ).
cnf(c_3567,plain,
( uri_ex_w2 = A
| uri_ex_w1 = A
| ~ icext(uri_ex_c1,A) ),
inference(resolve,[status(thm)],[c_3550,c_49]) ).
cnf(c_13212,plain,
( icext(uri_ex_c4,sK0(uri_ex_c3,uri_ex_c4))
| icext(uri_ex_c3,sK0(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4) ),
inference(resolve,[status(thm)],[c_3225,c_2219]) ).
cnf(c_4367,negated_conjecture,
( icext(uri_ex_c4,sK0(uri_ex_c3,uri_ex_c4))
| icext(uri_ex_c3,sK0(uri_ex_c3,uri_ex_c4)) ),
inference(resolve,[status(thm)],[c_70,c_13212]) ).
cnf(c_5214,plain,
( A != C
| icext(B,C)
| ~ iext(uri_owl_oneOf,B,sK3)
| ~ iext(uri_rdf_first,sK4,A) ),
inference(resolve,[status(thm)],[c_1005,c_54]) ).
cnf(c_5217,plain,
( uri_ex_w3 != B
| icext(A,B)
| ~ iext(uri_owl_oneOf,A,sK3) ),
inference(resolve,[status(thm)],[c_5214,c_56]) ).
cnf(c_5219,plain,
( uri_ex_w3 != A
| icext(uri_ex_c2,A) ),
inference(resolve,[status(thm)],[c_5217,c_53]) ).
cnf(c_5220,plain,
icext(uri_ex_c2,uri_ex_w3),
inference(xxres,[status(thm)],[c_5219]) ).
cnf(c_5262,plain,
( uri_ex_w2 != C
| icext(B,C)
| ~ iext(uri_owl_oneOf,B,sK3)
| ~ iext(uri_rdf_first,sK4,A) ),
inference(resolve,[status(thm)],[c_1006,c_54]) ).
cnf(c_5265,plain,
( uri_ex_w2 != B
| icext(A,B)
| ~ iext(uri_owl_oneOf,A,sK3) ),
inference(resolve,[status(thm)],[c_5262,c_56]) ).
cnf(c_5267,plain,
( uri_ex_w2 != A
| icext(uri_ex_c2,A) ),
inference(resolve,[status(thm)],[c_5265,c_53]) ).
cnf(c_5268,plain,
icext(uri_ex_c2,uri_ex_w2),
inference(xxres,[status(thm)],[c_5267]) ).
cnf(c_5439,plain,
( ~ icext(A,C)
| icext(B,C)
| ~ iext(uri_owl_unionOf,B,sK8)
| ~ iext(uri_rdf_first,sK9,A) ),
inference(resolve,[status(thm)],[c_2412,c_66]) ).
cnf(c_5442,plain,
( ~ icext(uri_ex_c2,B)
| icext(A,B)
| ~ iext(uri_owl_unionOf,A,sK8) ),
inference(resolve,[status(thm)],[c_5439,c_68]) ).
cnf(c_5444,plain,
( ~ icext(uri_ex_c2,A)
| icext(uri_ex_c4,A) ),
inference(resolve,[status(thm)],[c_5442,c_65]) ).
cnf(c_5445,plain,
icext(uri_ex_c4,uri_ex_w2),
inference(resolve,[status(thm)],[c_5444,c_5268]) ).
cnf(c_5448,plain,
icext(uri_ex_c4,uri_ex_w3),
inference(resolve,[status(thm)],[c_5444,c_5220]) ).
cnf(c_5477,plain,
( ~ icext(uri_ex_c1,C)
| icext(B,C)
| ~ iext(uri_owl_unionOf,B,sK8)
| ~ iext(uri_rdf_first,sK9,A) ),
inference(resolve,[status(thm)],[c_2413,c_66]) ).
cnf(c_5480,plain,
( ~ icext(uri_ex_c1,B)
| icext(A,B)
| ~ iext(uri_owl_unionOf,A,sK8) ),
inference(resolve,[status(thm)],[c_5477,c_68]) ).
cnf(c_5482,plain,
( ~ icext(uri_ex_c1,A)
| icext(uri_ex_c4,A) ),
inference(resolve,[status(thm)],[c_5480,c_65]) ).
cnf(c_5483,plain,
icext(uri_ex_c4,uri_ex_w1),
inference(resolve,[status(thm)],[c_5482,c_3540]) ).
cnf(c_5865,plain,
( A = C
| uri_ex_w2 = C
| ~ icext(B,C)
| ~ iext(uri_owl_oneOf,B,sK3)
| ~ iext(uri_rdf_first,sK4,A) ),
inference(resolve,[status(thm)],[c_1007,c_54]) ).
cnf(c_5871,plain,
( uri_ex_w3 = B
| uri_ex_w2 = B
| ~ icext(A,B)
| ~ iext(uri_owl_oneOf,A,sK3) ),
inference(resolve,[status(thm)],[c_5865,c_56]) ).
cnf(c_5873,plain,
( uri_ex_w3 = A
| uri_ex_w2 = A
| ~ icext(uri_ex_c2,A) ),
inference(resolve,[status(thm)],[c_5871,c_53]) ).
cnf(c_5959,plain,
( icext(A,C)
| icext(uri_ex_c1,C)
| ~ icext(B,C)
| ~ iext(uri_owl_unionOf,B,sK8)
| ~ iext(uri_rdf_first,sK9,A) ),
inference(resolve,[status(thm)],[c_2414,c_66]) ).
cnf(c_5964,plain,
( icext(uri_ex_c2,B)
| icext(uri_ex_c1,B)
| ~ icext(A,B)
| ~ iext(uri_owl_unionOf,A,sK8) ),
inference(resolve,[status(thm)],[c_5959,c_68]) ).
cnf(c_5966,plain,
( icext(uri_ex_c2,A)
| icext(uri_ex_c1,A)
| ~ icext(uri_ex_c4,A) ),
inference(resolve,[status(thm)],[c_5964,c_65]) ).
cnf(c_5983,plain,
( icext(uri_ex_c3,sK0(uri_ex_c3,uri_ex_c4))
| icext(uri_ex_c2,sK0(uri_ex_c3,uri_ex_c4))
| icext(uri_ex_c1,sK0(uri_ex_c3,uri_ex_c4)) ),
inference(resolve,[status(thm)],[c_5966,c_4367]) ).
cnf(c_13213,plain,
( B != D
| icext(C,D)
| ~ iext(uri_owl_oneOf,C,sK5)
| ~ iext(uri_rdf_first,sK7,B)
| ~ iext(uri_rdf_first,sK6,A)
| ~ iext(uri_rdf_rest,sK5,sK6) ),
inference(resolve,[status(thm)],[c_1831,c_59]) ).
cnf(c_11784,plain,
( B != D
| icext(C,D)
| ~ iext(uri_owl_oneOf,C,sK5)
| ~ iext(uri_rdf_first,sK7,B)
| ~ iext(uri_rdf_first,sK6,A) ),
inference(resolve,[status(thm)],[c_60,c_13213]) ).
cnf(c_11788,plain,
( A != C
| icext(B,C)
| ~ iext(uri_owl_oneOf,B,sK5)
| ~ iext(uri_rdf_first,sK7,A) ),
inference(resolve,[status(thm)],[c_11784,c_61]) ).
cnf(c_11791,plain,
( uri_ex_w3 != B
| icext(A,B)
| ~ iext(uri_owl_oneOf,A,sK5) ),
inference(resolve,[status(thm)],[c_11788,c_63]) ).
cnf(c_11793,plain,
( uri_ex_w3 != A
| icext(uri_ex_c3,A) ),
inference(resolve,[status(thm)],[c_11791,c_58]) ).
cnf(c_11800,plain,
icext(uri_ex_c3,uri_ex_w3),
inference(xxres,[status(thm)],[c_11793]) ).
cnf(c_13214,plain,
( A != D
| icext(C,D)
| ~ iext(uri_owl_oneOf,C,sK5)
| ~ iext(uri_rdf_first,sK7,B)
| ~ iext(uri_rdf_first,sK6,A)
| ~ iext(uri_rdf_rest,sK5,sK6) ),
inference(resolve,[status(thm)],[c_1833,c_59]) ).
cnf(c_11900,plain,
( A != D
| icext(C,D)
| ~ iext(uri_owl_oneOf,C,sK5)
| ~ iext(uri_rdf_first,sK7,B)
| ~ iext(uri_rdf_first,sK6,A) ),
inference(resolve,[status(thm)],[c_60,c_13214]) ).
cnf(c_11904,plain,
( uri_ex_w2 != C
| icext(B,C)
| ~ iext(uri_owl_oneOf,B,sK5)
| ~ iext(uri_rdf_first,sK7,A) ),
inference(resolve,[status(thm)],[c_11900,c_61]) ).
cnf(c_11907,plain,
( uri_ex_w2 != B
| icext(A,B)
| ~ iext(uri_owl_oneOf,A,sK5) ),
inference(resolve,[status(thm)],[c_11904,c_63]) ).
cnf(c_11909,plain,
( uri_ex_w2 != A
| icext(uri_ex_c3,A) ),
inference(resolve,[status(thm)],[c_11907,c_58]) ).
cnf(c_11910,plain,
icext(uri_ex_c3,uri_ex_w2),
inference(xxres,[status(thm)],[c_11909]) ).
cnf(c_13215,plain,
( uri_ex_w1 != D
| icext(C,D)
| ~ iext(uri_owl_oneOf,C,sK5)
| ~ iext(uri_rdf_first,sK7,B)
| ~ iext(uri_rdf_first,sK6,A)
| ~ iext(uri_rdf_rest,sK5,sK6) ),
inference(resolve,[status(thm)],[c_1835,c_59]) ).
cnf(c_11921,plain,
( uri_ex_w1 != D
| icext(C,D)
| ~ iext(uri_owl_oneOf,C,sK5)
| ~ iext(uri_rdf_first,sK7,B)
| ~ iext(uri_rdf_first,sK6,A) ),
inference(resolve,[status(thm)],[c_60,c_13215]) ).
cnf(c_11925,plain,
( uri_ex_w1 != C
| icext(B,C)
| ~ iext(uri_owl_oneOf,B,sK5)
| ~ iext(uri_rdf_first,sK7,A) ),
inference(resolve,[status(thm)],[c_11921,c_61]) ).
cnf(c_11928,plain,
( uri_ex_w1 != B
| icext(A,B)
| ~ iext(uri_owl_oneOf,A,sK5) ),
inference(resolve,[status(thm)],[c_11925,c_63]) ).
cnf(c_11930,plain,
( uri_ex_w1 != A
| icext(uri_ex_c3,A) ),
inference(resolve,[status(thm)],[c_11928,c_58]) ).
cnf(c_11933,plain,
icext(uri_ex_c3,uri_ex_w1),
inference(xxres,[status(thm)],[c_11930]) ).
cnf(c_13216,plain,
( C = D
| B = D
| A = D
| ~ icext(uri_ex_c3,D)
| ~ iext(uri_rdf_rest,sK7,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK7,C)
| ~ iext(uri_rdf_first,sK6,B)
| ~ iext(uri_rdf_rest,sK5,sK6)
| ~ iext(uri_rdf_first,sK5,A) ),
inference(resolve,[status(thm)],[c_1379,c_62]) ).
cnf(c_13217,plain,
( C = D
| B = D
| A = D
| ~ icext(uri_ex_c3,D)
| ~ iext(uri_rdf_rest,sK7,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK7,C)
| ~ iext(uri_rdf_first,sK6,B)
| ~ iext(uri_rdf_first,sK5,A) ),
inference(resolve,[status(thm)],[c_60,c_13216]) ).
cnf(c_12283,plain,
( C = D
| B = D
| A = D
| ~ icext(uri_ex_c3,D)
| ~ iext(uri_rdf_first,sK7,C)
| ~ iext(uri_rdf_first,sK6,B)
| ~ iext(uri_rdf_first,sK5,A) ),
inference(resolve,[status(thm)],[c_64,c_13217]) ).
cnf(c_12383,plain,
( B = C
| A = C
| uri_ex_w1 = C
| ~ icext(uri_ex_c3,C)
| ~ iext(uri_rdf_first,sK7,B)
| ~ iext(uri_rdf_first,sK6,A) ),
inference(resolve,[status(thm)],[c_12283,c_59]) ).
cnf(c_12411,plain,
( A = B
| uri_ex_w2 = B
| uri_ex_w1 = B
| ~ icext(uri_ex_c3,B)
| ~ iext(uri_rdf_first,sK7,A) ),
inference(resolve,[status(thm)],[c_12383,c_61]) ).
cnf(c_12426,plain,
( uri_ex_w3 = A
| uri_ex_w2 = A
| uri_ex_w1 = A
| ~ icext(uri_ex_c3,A) ),
inference(resolve,[status(thm)],[c_12411,c_63]) ).
cnf(c_13218,plain,
( icext(uri_ex_c2,sK0(uri_ex_c3,uri_ex_c4))
| icext(uri_ex_c1,sK0(uri_ex_c3,uri_ex_c4))
| uri_ex_w3 = sK0(uri_ex_c3,uri_ex_c4)
| uri_ex_w2 = sK0(uri_ex_c3,uri_ex_c4)
| uri_ex_w1 = sK0(uri_ex_c3,uri_ex_c4) ),
inference(resolve,[status(thm)],[c_12426,c_5983]) ).
cnf(c_13219,plain,
( icext(uri_ex_c2,sK0(uri_ex_c3,uri_ex_c4))
| icext(uri_ex_c1,sK0(uri_ex_c3,uri_ex_c4))
| uri_ex_w3 = sK0(uri_ex_c3,uri_ex_c4)
| uri_ex_w2 = sK0(uri_ex_c3,uri_ex_c4)
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(copy,[status(thm)],[c_13218]) ).
cnf(c_13220,plain,
( icext(uri_ex_c2,sK0(uri_ex_c3,uri_ex_c4))
| icext(uri_ex_c1,sK0(uri_ex_c3,uri_ex_c4))
| uri_ex_w3 = sK0(uri_ex_c3,uri_ex_c4)
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(copy,[status(thm)],[c_13219]) ).
cnf(c_12466,plain,
( icext(uri_ex_c2,sK0(uri_ex_c3,uri_ex_c4))
| icext(uri_ex_c1,sK0(uri_ex_c3,uri_ex_c4))
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(copy,[status(thm)],[c_13220]) ).
cnf(c_13221,plain,
( uri_ex_w3 = sK0(uri_ex_c3,uri_ex_c4)
| uri_ex_w2 = sK0(uri_ex_c3,uri_ex_c4)
| icext(uri_ex_c1,sK0(uri_ex_c3,uri_ex_c4))
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(resolve,[status(thm)],[c_12466,c_5873]) ).
cnf(c_13222,plain,
( uri_ex_w3 = sK0(uri_ex_c3,uri_ex_c4)
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| icext(uri_ex_c1,sK0(uri_ex_c3,uri_ex_c4))
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(copy,[status(thm)],[c_13221]) ).
cnf(c_13223,plain,
( sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| icext(uri_ex_c1,sK0(uri_ex_c3,uri_ex_c4))
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(copy,[status(thm)],[c_13222]) ).
cnf(c_13224,plain,
( sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| icext(uri_ex_c1,sK0(uri_ex_c3,uri_ex_c4))
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(copy,[status(thm)],[c_13223]) ).
cnf(c_13145,plain,
( icext(uri_ex_c1,sK0(uri_ex_c3,uri_ex_c4))
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(copy,[status(thm)],[c_13224]) ).
cnf(c_13225,plain,
( uri_ex_w2 = sK0(uri_ex_c3,uri_ex_c4)
| uri_ex_w1 = sK0(uri_ex_c3,uri_ex_c4)
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(resolve,[status(thm)],[c_13145,c_3567]) ).
cnf(c_13226,plain,
( uri_ex_w2 = sK0(uri_ex_c3,uri_ex_c4)
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(copy,[status(thm)],[c_13225]) ).
cnf(c_13227,plain,
( sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(copy,[status(thm)],[c_13226]) ).
cnf(c_13228,plain,
( sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(copy,[status(thm)],[c_13227]) ).
cnf(c_13151,plain,
( sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(copy,[status(thm)],[c_13228]) ).
cnf(c_13229,plain,
( ~ icext(uri_ex_c4,sK0(uri_ex_c3,uri_ex_c4))
| ~ icext(uri_ex_c3,uri_ex_w3)
| ~ ic(uri_ex_c4)
| ~ ic(uri_ex_c3)
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(paramod,[status(thm)],[c_13151,c_47]) ).
cnf(c_13230,negated_conjecture,
( ~ icext(uri_ex_c4,sK0(uri_ex_c3,uri_ex_c4))
| ~ icext(uri_ex_c3,uri_ex_w3)
| ~ ic(uri_ex_c4)
| ~ ic(uri_ex_c3)
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(resolve,[status(thm)],[c_70,c_13229]) ).
cnf(c_13231,negated_conjecture,
( ~ icext(uri_ex_c4,sK0(uri_ex_c3,uri_ex_c4))
| ~ icext(uri_ex_c3,uri_ex_w3)
| ~ ic(uri_ex_c4)
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(resolve,[status(thm)],[c_1384,c_13230]) ).
cnf(c_13232,negated_conjecture,
( ~ icext(uri_ex_c4,sK0(uri_ex_c3,uri_ex_c4))
| ~ icext(uri_ex_c3,uri_ex_w3)
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(resolve,[status(thm)],[c_2219,c_13231]) ).
cnf(c_13154,negated_conjecture,
( ~ icext(uri_ex_c4,sK0(uri_ex_c3,uri_ex_c4))
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(resolve,[status(thm)],[c_11800,c_13232]) ).
cnf(c_13233,plain,
( ~ icext(uri_ex_c4,uri_ex_w3)
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(paramod,[status(thm)],[c_13151,c_13154]) ).
cnf(c_13234,plain,
( ~ icext(uri_ex_c4,uri_ex_w3)
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(copy,[status(thm)],[c_13233]) ).
cnf(c_13235,plain,
( ~ icext(uri_ex_c4,uri_ex_w3)
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(copy,[status(thm)],[c_13234]) ).
cnf(c_13168,plain,
( sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(resolve,[status(thm)],[c_5448,c_13235]) ).
cnf(c_13236,plain,
( ~ icext(uri_ex_c4,sK0(uri_ex_c3,uri_ex_c4))
| ~ icext(uri_ex_c3,uri_ex_w1)
| ~ ic(uri_ex_c4)
| ~ ic(uri_ex_c3)
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2 ),
inference(paramod,[status(thm)],[c_13168,c_47]) ).
cnf(c_13237,negated_conjecture,
( ~ icext(uri_ex_c4,sK0(uri_ex_c3,uri_ex_c4))
| ~ icext(uri_ex_c3,uri_ex_w1)
| ~ ic(uri_ex_c4)
| ~ ic(uri_ex_c3)
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2 ),
inference(resolve,[status(thm)],[c_70,c_13236]) ).
cnf(c_13238,negated_conjecture,
( ~ icext(uri_ex_c4,sK0(uri_ex_c3,uri_ex_c4))
| ~ icext(uri_ex_c3,uri_ex_w1)
| ~ ic(uri_ex_c4)
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2 ),
inference(resolve,[status(thm)],[c_1384,c_13237]) ).
cnf(c_13239,negated_conjecture,
( ~ icext(uri_ex_c4,sK0(uri_ex_c3,uri_ex_c4))
| ~ icext(uri_ex_c3,uri_ex_w1)
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2 ),
inference(resolve,[status(thm)],[c_2219,c_13238]) ).
cnf(c_13171,negated_conjecture,
( ~ icext(uri_ex_c4,sK0(uri_ex_c3,uri_ex_c4))
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2 ),
inference(resolve,[status(thm)],[c_11933,c_13239]) ).
cnf(c_13240,plain,
( ~ icext(uri_ex_c4,uri_ex_w1)
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2 ),
inference(paramod,[status(thm)],[c_13168,c_13171]) ).
cnf(c_13241,plain,
( ~ icext(uri_ex_c4,uri_ex_w1)
| sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2 ),
inference(copy,[status(thm)],[c_13240]) ).
cnf(c_13193,plain,
sK0(uri_ex_c3,uri_ex_c4) = uri_ex_w2,
inference(resolve,[status(thm)],[c_5483,c_13241]) ).
cnf(c_13242,plain,
( ~ icext(uri_ex_c4,sK0(uri_ex_c3,uri_ex_c4))
| ~ icext(uri_ex_c3,uri_ex_w2)
| ~ ic(uri_ex_c4)
| ~ ic(uri_ex_c3)
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4) ),
inference(paramod,[status(thm)],[c_13193,c_47]) ).
cnf(c_13243,plain,
( ~ icext(uri_ex_c4,uri_ex_w2)
| ~ icext(uri_ex_c3,uri_ex_w2)
| ~ ic(uri_ex_c4)
| ~ ic(uri_ex_c3)
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4) ),
inference(paramod,[status(thm)],[c_13193,c_13242]) ).
cnf(c_13244,negated_conjecture,
( ~ icext(uri_ex_c4,uri_ex_w2)
| ~ icext(uri_ex_c3,uri_ex_w2)
| ~ ic(uri_ex_c4)
| ~ ic(uri_ex_c3) ),
inference(resolve,[status(thm)],[c_70,c_13243]) ).
cnf(c_13245,negated_conjecture,
( ~ icext(uri_ex_c4,uri_ex_w2)
| ~ icext(uri_ex_c3,uri_ex_w2)
| ~ ic(uri_ex_c4) ),
inference(resolve,[status(thm)],[c_1384,c_13244]) ).
cnf(c_13246,negated_conjecture,
( ~ icext(uri_ex_c4,uri_ex_w2)
| ~ icext(uri_ex_c3,uri_ex_w2) ),
inference(resolve,[status(thm)],[c_2219,c_13245]) ).
cnf(c_13247,negated_conjecture,
~ icext(uri_ex_c4,uri_ex_w2),
inference(resolve,[status(thm)],[c_11910,c_13246]) ).
cnf(c_13198,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_5445,c_13247]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB021+2 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.38 % Computer : n015.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sat Sep 26 11:51:31 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.39 % Process 3959715 was started by sandbox2 on n015,
% 0.10/0.39 % Sat Sep 26 11:51:31 2026
% 0.10/0.39 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.40
% 0.10/0.40 % From the command line: assign(max_seconds, 300).
% 68.04/10.23
% 68.04/10.23 % given #500 (T,wt=17): 5100 -iext(uri_rdf_rest,c1,c9) | -iext(uri_owl_unionOf,A,c1) | -icext(A,B) | icext(uri_ex_w1,B) | icext(uri_ex_c2,B). [resolve(278,b,68,a),unit_del(b,69)].
% 68.04/10.23
% 68.04/10.23 % given #1000 (T,wt=14): 5540 -iext(uri_rdf_rest,c7,c1) | -iext(uri_owl_oneOf,A,c7) | icext(A,B) | uri_ex_w2 != B. [resolve(4206,a,63,a)].
% 68.04/10.23
% 68.04/10.23 % given #1500 (T,wt=20): 7078 -iext(uri_rdf_rest,c2,c7) | iext(uri_owl_unionOf,uri_ex_w2,c2) | -ic(uri_ex_w2) | -ic(uri_ex_w3) | -icext(uri_ex_w2,f1(uri_ex_w2,c2,uri_ex_w2,c7,uri_ex_w3)). [factor(7068,c,d),merge(f)].
% 68.04/10.23
% 68.04/10.23 % given #2000 (T,wt=22): 2205 -iext(uri_rdf_first,c7,A) | -iext(uri_rdf_first,uri_rdf_nil,A) | -iext(uri_rdf_rest,uri_rdf_nil,c7) | -iext(uri_owl_oneOf,B,c7) | -icext(B,C) | A = C. [factor(2150,f,g)].
% 68.04/10.23
% 68.04/10.23 % given #2500 (T,wt=18): 8470 -iext(uri_rdf_rest,c5,c9) | -iext(uri_rdf_rest,c9,c2) | -iext(uri_owl_oneOf,A,c5) | icext(A,B) | uri_ex_w2 != B. [resolve(6590,b,68,a)].
% 68.04/10.23
% 68.04/10.23 % given #3000 (T,wt=22): 9509 -iext(uri_rdf_rest,c6,c3) | -iext(uri_rdf_rest,c3,uri_rdf_nil) | iext(uri_owl_unionOf,uri_ex_w2,c6) | -ic(uri_ex_w2) | -icext(uri_ex_w2,f1(uri_ex_w2,c6,uri_ex_w2,c3,uri_ex_w2)). [factor(9502,d,e),merge(f)].
% 68.04/10.23
% 68.04/10.23 % given #3500 (T,wt=25): 3385 -iext(uri_rdf_first,c1,A) | -iext(uri_rdf_rest,c1,c6) | -iext(uri_rdf_first,c6,A) | -iext(uri_rdf_first,c7,B) | -icext(uri_ex_c1,C) | A = C | B = C. [factor(3318,f,g)].
% 68.04/10.23
% 68.04/10.23 % given #4000 (T,wt=25): 8042 -iext(uri_rdf_first,uri_rdf_nil,A) | -iext(uri_rdf_rest,uri_rdf_nil,c3) | -iext(uri_rdf_rest,c3,uri_rdf_nil) | -iext(uri_owl_oneOf,B,c2) | -icext(B,C) | uri_ex_w2 = C | A = C. [factor(8020,g,i),unit_del(a,51)].
% 68.04/10.23
% 68.04/10.23 % given #4500 (T,wt=26): 2208 -iext(uri_rdf_first,A,B) | -iext(uri_rdf_rest,A,c7) | -iext(uri_rdf_first,c7,B) | iext(uri_owl_unionOf,B,A) | -ic(B) | -icext(B,f1(B,A,B,c7,B)). [factor(2162,e,f),merge(g)].
% 68.04/10.23
% 68.04/10.23 % given #5000 (T,wt=17): 13049 -iext(uri_rdf_rest,c5,c8) | -iext(uri_rdf_first,c8,uri_ex_w1) | -icext(uri_ex_c3,A) | uri_ex_w1 = A | uri_ex_c2 = A. [resolve(13046,c,67,a)].
% 68.04/10.23
% 68.04/10.23 % SZS status Theorem for theBenchmark
% 68.04/10.23
% 68.04/10.23 % Proof 1 at 8.91 (+ 0.50) seconds.
% 68.04/10.23 % Length of proof is 117.
% 68.04/10.23 % Level of proof is 14.
% 68.04/10.23 % Maximum clause weight is 40.000.
% 68.04/10.23 % Given clauses 5047.
% 68.04/10.23
% 68.04/10.23 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------