%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWB021+2 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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:08 PM UTC 2026
% Result : Theorem 7.48s 1.40s
% Output : CNFRefutation 2.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 9
% Syntax : Number of formulae : 184 ( 42 unt; 1 def)
% Number of atoms : 961 ( 121 equ)
% Maximal formula atoms : 24 ( 5 avg)
% Number of connectives : 1294 ( 517 ~; 589 |; 166 &)
% ( 17 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-4 aty)
% Number of functors : 27 ( 27 usr; 23 con; 0-5 aty)
% Number of variables : 470 ( 444 !; 26 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] :
( iext(uri_owl_oneOf,X,Y)
=> ( icext(uri_rdf_List,Y)
& ic(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] :
( iext(uri_owl_unionOf,X,Y)
=> ( icext(uri_rdf_List,Y)
& ic(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,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(f7,conjecture,
iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,negated_conjecture,
~ iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4),
inference(negated_conjecture,[status(cth)],[f7]) ).
fof(f9,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,plain,
! [X,Y] :
( ( icext(uri_rdf_List,Y)
& ic(X) )
| ~ iext(uri_owl_oneOf,X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f11,plain,
! [X0,X1] :
( ic(X0)
| ~ iext(uri_owl_oneOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f13,plain,
! [X,Y] :
( ( icext(uri_rdf_List,Y)
& ic(X) )
| ~ iext(uri_owl_unionOf,X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f14,plain,
! [X0,X1] :
( ic(X0)
| ~ iext(uri_owl_unionOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f16,plain,
! [Z,S1,C1,S2,C2] :
( ( iext(uri_owl_unionOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( icext(C2,X)
| icext(C1,X) ) )
& ic(C2)
& ic(C1)
& ic(Z) ) )
| ~ 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) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f17,plain,
! [Z,S1,C1,S2,C2] :
( ( ( ? [X] :
( ( icext(C2,X)
| icext(C1,X)
| icext(Z,X) )
& ( ( ~ icext(C2,X)
& ~ icext(C1,X) )
| ~ icext(Z,X) ) )
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(Z)
| iext(uri_owl_unionOf,Z,S1) )
& ( ( ! [X] :
( ( ( ~ icext(C2,X)
& ~ icext(C1,X) )
| icext(Z,X) )
& ( icext(C2,X)
| icext(C1,X)
| ~ icext(Z,X) ) )
& ic(C2)
& ic(C1)
& ic(Z) )
| ~ iext(uri_owl_unionOf,Z,S1) ) )
| ~ 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) ),
inference(NNF_transformation,[status(thm)],[f16]) ).
fof(f18,plain,
! [S1,C1,C2] :
( ( ! [Z] :
( ? [X] :
( ( icext(C2,X)
| icext(C1,X)
| icext(Z,X) )
& ( ( ~ icext(C2,X)
& ~ icext(C1,X) )
| ~ icext(Z,X) ) )
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(Z)
| iext(uri_owl_unionOf,Z,S1) )
& ! [Z] :
( ( ! [X] :
( ( ~ icext(C2,X)
& ~ icext(C1,X) )
| icext(Z,X) )
& ! [X] :
( icext(C2,X)
| icext(C1,X)
| ~ icext(Z,X) )
& ic(C2)
& ic(C1)
& ic(Z) )
| ~ iext(uri_owl_unionOf,Z,S1) ) )
| ! [S2] :
( ~ 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) ) ),
inference(miniscoping,[status(thm)],[f17]) ).
fof(f19,plain,
! [S1,C1,C2] :
( ( ! [Z] :
( ( ( icext(C2,sK0_skl(Z,C2,C1,S1))
| icext(C1,sK0_skl(Z,C2,C1,S1))
| icext(Z,sK0_skl(Z,C2,C1,S1)) )
& ( ( ~ icext(C2,sK0_skl(Z,C2,C1,S1))
& ~ icext(C1,sK0_skl(Z,C2,C1,S1)) )
| ~ icext(Z,sK0_skl(Z,C2,C1,S1)) ) )
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(Z)
| iext(uri_owl_unionOf,Z,S1) )
& ! [Z] :
( ( ! [X] :
( ( ~ icext(C2,X)
& ~ icext(C1,X) )
| icext(Z,X) )
& ! [X] :
( icext(C2,X)
| icext(C1,X)
| ~ icext(Z,X) )
& ic(C2)
& ic(C1)
& ic(Z) )
| ~ iext(uri_owl_unionOf,Z,S1) ) )
| ! [S2] :
( ~ 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) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X,sK0_skl(Z,C2,C1,S1))],[f18]) ).
fof(f23,plain,
! [X0,X1,X2,X3,X4,X5] :
( icext(X3,X5)
| icext(X1,X5)
| ~ icext(X4,X5)
| ~ iext(uri_owl_unionOf,X4,X0)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f24,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ icext(X1,X5)
| icext(X4,X5)
| ~ iext(uri_owl_unionOf,X4,X0)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f25,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ icext(X3,X5)
| icext(X4,X5)
| ~ iext(uri_owl_unionOf,X4,X0)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f29,plain,
! [Z,S1,A1,S2,A2] :
( ( iext(uri_owl_oneOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( X = A2
| X = A1 ) )
& ic(Z) ) )
| ~ 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) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f30,plain,
! [Z,S1,A1,S2,A2] :
( ( ( ? [X] :
( ( X = A2
| X = A1
| icext(Z,X) )
& ( ( X != A2
& X != A1 )
| ~ icext(Z,X) ) )
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,S1) )
& ( ( ! [X] :
( ( ( X != A2
& X != A1 )
| icext(Z,X) )
& ( X = A2
| X = A1
| ~ icext(Z,X) ) )
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,S1) ) )
| ~ 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) ),
inference(NNF_transformation,[status(thm)],[f29]) ).
fof(f31,plain,
! [S1,A1,A2] :
( ( ! [Z] :
( ? [X] :
( ( X = A2
| X = A1
| icext(Z,X) )
& ( ( X != A2
& X != A1 )
| ~ icext(Z,X) ) )
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,S1) )
& ! [Z] :
( ( ! [X] :
( ( X != A2
& X != A1 )
| icext(Z,X) )
& ! [X] :
( X = A2
| X = A1
| ~ icext(Z,X) )
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,S1) ) )
| ! [S2] :
( ~ 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) ) ),
inference(miniscoping,[status(thm)],[f30]) ).
fof(f32,plain,
! [S1,A1,A2] :
( ( ! [Z] :
( ( ( sK1_skl(Z,A2,A1,S1) = A2
| sK1_skl(Z,A2,A1,S1) = A1
| icext(Z,sK1_skl(Z,A2,A1,S1)) )
& ( ( sK1_skl(Z,A2,A1,S1) != A2
& sK1_skl(Z,A2,A1,S1) != A1 )
| ~ icext(Z,sK1_skl(Z,A2,A1,S1)) ) )
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,S1) )
& ! [Z] :
( ( ! [X] :
( ( X != A2
& X != A1 )
| icext(Z,X) )
& ! [X] :
( X = A2
| X = A1
| ~ icext(Z,X) )
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,S1) ) )
| ! [S2] :
( ~ 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) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(X,sK1_skl(Z,A2,A1,S1))],[f31]) ).
fof(f34,plain,
! [X0,X1,X2,X3,X4,X5] :
( X5 = X3
| X5 = X1
| ~ icext(X4,X5)
| ~ iext(uri_owl_oneOf,X4,X0)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f35,plain,
! [X0,X1,X2,X3,X4,X5] :
( X5 != X1
| icext(X4,X5)
| ~ iext(uri_owl_oneOf,X4,X0)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f36,plain,
! [X0,X1,X2,X3,X4,X5] :
( X5 != X3
| icext(X4,X5)
| ~ iext(uri_owl_oneOf,X4,X0)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f40,plain,
! [Z,S1,A1,S2,A2,S3,A3] :
( ( iext(uri_owl_oneOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( X = A3
| X = A2
| X = A1 ) )
& ic(Z) ) )
| ~ 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) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f41,definition,
! [A1,A2,A3,X] :
( sP0_prd(X,A3,A2,A1)
<=> ( X = A3
| X = A2
| X = A1 ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f42,plain,
! [Z,S1,A1,S2,A2,S3,A3] :
( ( iext(uri_owl_oneOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> sP0_prd(X,A3,A2,A1) )
& ic(Z) ) )
| ~ 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) ),
inference(formula_renaming,[status(thm)],[f40,f41]) ).
fof(f43,plain,
! [Z,S1,A1,S2,A2,S3,A3] :
( ( ( ? [X] :
( ( sP0_prd(X,A3,A2,A1)
| icext(Z,X) )
& ( ~ sP0_prd(X,A3,A2,A1)
| ~ icext(Z,X) ) )
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,S1) )
& ( ( ! [X] :
( ( ~ sP0_prd(X,A3,A2,A1)
| icext(Z,X) )
& ( sP0_prd(X,A3,A2,A1)
| ~ icext(Z,X) ) )
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,S1) ) )
| ~ 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) ),
inference(NNF_transformation,[status(thm)],[f42]) ).
fof(f44,plain,
! [S1,A1,A2,A3] :
( ( ! [Z] :
( ? [X] :
( ( sP0_prd(X,A3,A2,A1)
| icext(Z,X) )
& ( ~ sP0_prd(X,A3,A2,A1)
| ~ icext(Z,X) ) )
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,S1) )
& ! [Z] :
( ( ! [X] :
( ~ sP0_prd(X,A3,A2,A1)
| icext(Z,X) )
& ! [X] :
( sP0_prd(X,A3,A2,A1)
| ~ icext(Z,X) )
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,S1) ) )
| ! [S3] :
( ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,A3)
| ! [S2] :
( ~ iext(uri_rdf_rest,S2,S3)
| ~ iext(uri_rdf_first,S2,A2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,A1) ) ) ),
inference(miniscoping,[status(thm)],[f43]) ).
fof(f45,plain,
! [S1,A1,A2,A3] :
( ( ! [Z] :
( ( ( sP0_prd(sK2_skl(Z,A3,A2,A1,S1),A3,A2,A1)
| icext(Z,sK2_skl(Z,A3,A2,A1,S1)) )
& ( ~ sP0_prd(sK2_skl(Z,A3,A2,A1,S1),A3,A2,A1)
| ~ icext(Z,sK2_skl(Z,A3,A2,A1,S1)) ) )
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,S1) )
& ! [Z] :
( ( ! [X] :
( ~ sP0_prd(X,A3,A2,A1)
| icext(Z,X) )
& ! [X] :
( sP0_prd(X,A3,A2,A1)
| ~ icext(Z,X) )
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,S1) ) )
| ! [S3] :
( ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,A3)
| ! [S2] :
( ~ iext(uri_rdf_rest,S2,S3)
| ~ iext(uri_rdf_first,S2,A2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,A1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X,sK2_skl(Z,A3,A2,A1,S1))],[f44]) ).
fof(f47,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( sP0_prd(X7,X5,X3,X1)
| ~ icext(X6,X7)
| ~ iext(uri_owl_oneOf,X6,X0)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f48,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ sP0_prd(X7,X5,X3,X1)
| icext(X6,X7)
| ~ iext(uri_owl_oneOf,X6,X0)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f51,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)],[f6]) ).
fof(f52,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)],[f51]) ).
fof(f53,plain,
( ! [C1,C2] :
( ( ( icext(C2,sK3_skl(C2,C1))
| icext(C1,sK3_skl(C2,C1)) )
& ( ~ icext(C2,sK3_skl(C2,C1))
| ~ icext(C1,sK3_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,[sK3_skl]),skolemize(X,sK3_skl(C2,C1))],[f52]) ).
fof(f58,plain,
! [X0,X1] :
( ~ icext(X1,sK3_skl(X1,X0))
| ~ icext(X0,sK3_skl(X1,X0))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_owl_equivalentClass,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f59,plain,
! [X0,X1] :
( icext(X1,sK3_skl(X1,X0))
| icext(X0,sK3_skl(X1,X0))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_owl_equivalentClass,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f60,plain,
~ iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f61,plain,
? [BNODE_l42] :
( iext(uri_rdf_rest,BNODE_l42,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l42,uri_ex_c2)
& ? [BNODE_l41] :
( 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)
& ? [BNODE_l33] :
( iext(uri_rdf_rest,BNODE_l33,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l33,uri_ex_w3)
& ? [BNODE_l32] :
( iext(uri_rdf_rest,BNODE_l32,BNODE_l33)
& iext(uri_rdf_first,BNODE_l32,uri_ex_w2)
& ? [BNODE_l31] :
( 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)
& ? [BNODE_l22] :
( iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l22,uri_ex_w3)
& ? [BNODE_l21] :
( 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)
& ? [BNODE_l12] :
( iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l12,uri_ex_w2)
& ? [BNODE_l11] :
( 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(miniscoping,[status(thm)],[f9]) ).
fof(f62,plain,
( iext(uri_rdf_rest,sK4_skl,uri_rdf_nil)
& iext(uri_rdf_first,sK4_skl,uri_ex_c2)
& iext(uri_rdf_rest,sK5_skl,sK4_skl)
& iext(uri_rdf_first,sK5_skl,uri_ex_c1)
& iext(uri_owl_unionOf,uri_ex_c4,sK5_skl)
& iext(uri_rdf_rest,sK6_skl,uri_rdf_nil)
& iext(uri_rdf_first,sK6_skl,uri_ex_w3)
& iext(uri_rdf_rest,sK7_skl,sK6_skl)
& iext(uri_rdf_first,sK7_skl,uri_ex_w2)
& iext(uri_rdf_rest,sK8_skl,sK7_skl)
& iext(uri_rdf_first,sK8_skl,uri_ex_w1)
& iext(uri_owl_oneOf,uri_ex_c3,sK8_skl)
& iext(uri_rdf_rest,sK9_skl,uri_rdf_nil)
& iext(uri_rdf_first,sK9_skl,uri_ex_w3)
& iext(uri_rdf_rest,sK10_skl,sK9_skl)
& iext(uri_rdf_first,sK10_skl,uri_ex_w2)
& iext(uri_owl_oneOf,uri_ex_c2,sK10_skl)
& iext(uri_rdf_rest,sK11_skl,uri_rdf_nil)
& iext(uri_rdf_first,sK11_skl,uri_ex_w2)
& iext(uri_rdf_rest,sK12_skl,sK11_skl)
& iext(uri_rdf_first,sK12_skl,uri_ex_w1)
& iext(uri_owl_oneOf,uri_ex_c1,sK12_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl]),skolemize(BNODE_l42,sK4_skl),skolemize(BNODE_l41,sK5_skl),skolemize(BNODE_l33,sK6_skl),skolemize(BNODE_l32,sK7_skl),skolemize(BNODE_l31,sK8_skl),skolemize(BNODE_l22,sK9_skl),skolemize(BNODE_l21,sK10_skl),skolemize(BNODE_l12,sK11_skl),skolemize(BNODE_l11,sK12_skl)],[f61]) ).
fof(f63,plain,
iext(uri_owl_oneOf,uri_ex_c1,sK12_skl),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f64,plain,
iext(uri_rdf_first,sK12_skl,uri_ex_w1),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f65,plain,
iext(uri_rdf_rest,sK12_skl,sK11_skl),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f66,plain,
iext(uri_rdf_first,sK11_skl,uri_ex_w2),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f67,plain,
iext(uri_rdf_rest,sK11_skl,uri_rdf_nil),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f68,plain,
iext(uri_owl_oneOf,uri_ex_c2,sK10_skl),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f69,plain,
iext(uri_rdf_first,sK10_skl,uri_ex_w2),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f70,plain,
iext(uri_rdf_rest,sK10_skl,sK9_skl),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f71,plain,
iext(uri_rdf_first,sK9_skl,uri_ex_w3),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f72,plain,
iext(uri_rdf_rest,sK9_skl,uri_rdf_nil),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f73,plain,
iext(uri_owl_oneOf,uri_ex_c3,sK8_skl),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f74,plain,
iext(uri_rdf_first,sK8_skl,uri_ex_w1),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f75,plain,
iext(uri_rdf_rest,sK8_skl,sK7_skl),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f76,plain,
iext(uri_rdf_first,sK7_skl,uri_ex_w2),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f77,plain,
iext(uri_rdf_rest,sK7_skl,sK6_skl),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f78,plain,
iext(uri_rdf_first,sK6_skl,uri_ex_w3),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f79,plain,
iext(uri_rdf_rest,sK6_skl,uri_rdf_nil),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f80,plain,
iext(uri_owl_unionOf,uri_ex_c4,sK5_skl),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f81,plain,
iext(uri_rdf_first,sK5_skl,uri_ex_c1),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f82,plain,
iext(uri_rdf_rest,sK5_skl,sK4_skl),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f83,plain,
iext(uri_rdf_first,sK4_skl,uri_ex_c2),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f84,plain,
iext(uri_rdf_rest,sK4_skl,uri_rdf_nil),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f85,plain,
! [A1,A2,A3,X] :
( ( ( X != A3
& X != A2
& X != A1 )
| sP0_prd(X,A3,A2,A1) )
& ( X = A3
| X = A2
| X = A1
| ~ sP0_prd(X,A3,A2,A1) ) ),
inference(NNF_transformation,[status(thm)],[f41]) ).
fof(f86,plain,
( ! [A1,A2,A3,X] :
( ( X != A3
& X != A2
& X != A1 )
| sP0_prd(X,A3,A2,A1) )
& ! [A1,A2,A3,X] :
( X = A3
| X = A2
| X = A1
| ~ sP0_prd(X,A3,A2,A1) ) ),
inference(miniscoping,[status(thm)],[f85]) ).
fof(f87,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| X0 = X2
| X0 = X3
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f88,plain,
! [X0,X1,X2,X3] :
( X0 != X3
| sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f89,plain,
! [X0,X1,X2,X3] :
( X0 != X2
| sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f90,plain,
! [X0,X1,X2,X3] :
( X0 != X1
| sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f91,plain,
! [X0,X1,X2,X3,X4] :
( icext(X4,X1)
| ~ iext(uri_owl_oneOf,X4,X0)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f35]) ).
fof(f92,plain,
! [X0,X1,X2,X3,X4] :
( icext(X4,X3)
| ~ iext(uri_owl_oneOf,X4,X0)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f36]) ).
fof(f93,plain,
! [X0,X1,X2] : sP0_prd(X0,X1,X2,X0),
inference(destructive_equality_resolution,[status(thm)],[f88]) ).
fof(f94,plain,
! [X0,X1,X2] : sP0_prd(X0,X1,X0,X2),
inference(destructive_equality_resolution,[status(thm)],[f89]) ).
fof(f95,plain,
! [X0,X1,X2] : sP0_prd(X0,X0,X1,X2),
inference(destructive_equality_resolution,[status(thm)],[f90]) ).
fof(f96,plain,
ic(uri_ex_c3),
inference(resolution,[status(thm)],[f11,f73]) ).
fof(f98,plain,
ic(uri_ex_c4),
inference(resolution,[status(thm)],[f14,f80]) ).
fof(f104,plain,
! [X0,X1,X2,X3] :
( icext(X2,X3)
| icext(X0,X3)
| ~ icext(uri_ex_c4,X3)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,sK5_skl,X1)
| ~ iext(uri_rdf_first,sK5_skl,X0) ),
inference(resolution,[status(thm)],[f23,f80]) ).
fof(f106,plain,
! [X0,X1,X2,X3] :
( ~ icext(X0,X3)
| icext(uri_ex_c4,X3)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,sK5_skl,X1)
| ~ iext(uri_rdf_first,sK5_skl,X0) ),
inference(resolution,[status(thm)],[f24,f80]) ).
fof(f110,plain,
! [X0,X1,X2,X3] :
( ~ icext(X2,X3)
| icext(uri_ex_c4,X3)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,sK5_skl,X1)
| ~ iext(uri_rdf_first,sK5_skl,X0) ),
inference(resolution,[status(thm)],[f25,f80]) ).
fof(f116,plain,
! [X0,X1,X2] :
( icext(uri_ex_c1,X0)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,sK12_skl,X1)
| ~ iext(uri_rdf_first,sK12_skl,X0) ),
inference(resolution,[status(thm)],[f91,f63]) ).
fof(f128,plain,
! [X0,X1,X2] :
( icext(uri_ex_c1,X2)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,sK12_skl,X1)
| ~ iext(uri_rdf_first,sK12_skl,X0) ),
inference(resolution,[status(thm)],[f92,f63]) ).
fof(f142,plain,
! [X0,X1,X2,X3] :
( X3 = uri_ex_w2
| X3 = X1
| ~ icext(X2,X3)
| ~ iext(uri_owl_oneOf,X2,X0)
| ~ iext(uri_rdf_rest,sK11_skl,uri_rdf_nil)
| ~ iext(uri_rdf_rest,X0,sK11_skl)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(resolution,[status(thm)],[f66,f34]) ).
fof(f196,plain,
! [X0,X1,X2,X3,X4,X5] :
( sP0_prd(X5,X4,X2,X0)
| ~ icext(uri_ex_c3,X5)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,sK8_skl,X1)
| ~ iext(uri_rdf_first,sK8_skl,X0) ),
inference(resolution,[status(thm)],[f47,f73]) ).
fof(f201,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( icext(X6,X5)
| ~ iext(uri_owl_oneOf,X6,X0)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(resolution,[status(thm)],[f48,f95]) ).
fof(f202,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( icext(X6,X3)
| ~ iext(uri_owl_oneOf,X6,X0)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(resolution,[status(thm)],[f48,f94]) ).
fof(f203,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( icext(X6,X1)
| ~ iext(uri_owl_oneOf,X6,X0)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(resolution,[status(thm)],[f48,f93]) ).
fof(f232,plain,
! [X0,X1,X2] :
( icext(uri_ex_c2,X2)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,sK10_skl,X1)
| ~ iext(uri_rdf_first,sK10_skl,X0) ),
inference(resolution,[status(thm)],[f68,f92]) ).
fof(f234,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| X3 = X0
| ~ icext(uri_ex_c2,X3)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,sK10_skl,X1)
| ~ iext(uri_rdf_first,sK10_skl,X0) ),
inference(resolution,[status(thm)],[f68,f34]) ).
fof(f240,plain,
! [X0] :
( icext(X0,sK3_skl(X0,uri_ex_c3))
| icext(uri_ex_c3,sK3_skl(X0,uri_ex_c3))
| ~ ic(X0)
| iext(uri_owl_equivalentClass,uri_ex_c3,X0) ),
inference(resolution,[status(thm)],[f59,f96]) ).
fof(f394,plain,
! [X0,X1,X2,X3] :
( sP0_prd(X3,X2,X1,X0)
| ~ icext(uri_ex_c3,X3)
| ~ iext(uri_rdf_rest,sK6_skl,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK6_skl,X2)
| ~ iext(uri_rdf_first,sK7_skl,X1)
| ~ iext(uri_rdf_rest,sK8_skl,sK7_skl)
| ~ iext(uri_rdf_first,sK8_skl,X0) ),
inference(resolution,[status(thm)],[f77,f196]) ).
fof(f409,plain,
! [X0,X1,X2,X3] :
( sP0_prd(X3,X2,X1,X0)
| ~ icext(uri_ex_c3,X3)
| ~ iext(uri_rdf_rest,sK6_skl,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK6_skl,X2)
| ~ iext(uri_rdf_first,sK7_skl,X1)
| ~ iext(uri_rdf_first,sK8_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f394,f75]) ).
fof(f489,plain,
! [X0,X1,X2] :
( icext(X1,X2)
| icext(X0,X2)
| ~ icext(uri_ex_c4,X2)
| ~ iext(uri_rdf_rest,sK4_skl,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK4_skl,X1)
| ~ iext(uri_rdf_first,sK5_skl,X0) ),
inference(resolution,[status(thm)],[f82,f104]) ).
fof(f533,plain,
( icext(uri_ex_c4,sK3_skl(uri_ex_c4,uri_ex_c3))
| icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4) ),
inference(resolution,[status(thm)],[f240,f98]) ).
fof(f535,plain,
( icext(uri_ex_c4,sK3_skl(uri_ex_c4,uri_ex_c3))
| icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3)) ),
inference(forward_subsumption_resolution,[status(thm)],[f533,f60]) ).
fof(f560,plain,
! [X0,X1,X2] :
( ~ icext(X1,X2)
| icext(uri_ex_c4,X2)
| ~ iext(uri_rdf_first,sK4_skl,X1)
| ~ iext(uri_rdf_rest,sK5_skl,sK4_skl)
| ~ iext(uri_rdf_first,sK5_skl,X0) ),
inference(resolution,[status(thm)],[f84,f110]) ).
fof(f564,plain,
! [X0,X1,X2] :
( ~ icext(X0,X2)
| icext(uri_ex_c4,X2)
| ~ iext(uri_rdf_first,sK4_skl,X1)
| ~ iext(uri_rdf_rest,sK5_skl,sK4_skl)
| ~ iext(uri_rdf_first,sK5_skl,X0) ),
inference(resolution,[status(thm)],[f84,f106]) ).
fof(f589,plain,
! [X0,X1,X2] :
( ~ icext(X1,X2)
| icext(uri_ex_c4,X2)
| ~ iext(uri_rdf_first,sK4_skl,X1)
| ~ iext(uri_rdf_first,sK5_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f560,f82]) ).
fof(f590,plain,
! [X0,X1,X2] :
( ~ icext(X0,X2)
| icext(uri_ex_c4,X2)
| ~ iext(uri_rdf_first,sK4_skl,X1)
| ~ iext(uri_rdf_first,sK5_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f564,f82]) ).
fof(f624,plain,
! [X0,X1] :
( icext(uri_ex_c1,X0)
| ~ iext(uri_rdf_rest,sK11_skl,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK11_skl,X1)
| ~ iext(uri_rdf_first,sK12_skl,X0) ),
inference(resolution,[status(thm)],[f116,f65]) ).
fof(f629,plain,
! [X0,X1] :
( icext(uri_ex_c1,X0)
| ~ iext(uri_rdf_first,sK11_skl,X1)
| ~ iext(uri_rdf_first,sK12_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f624,f67]) ).
fof(f646,plain,
! [X0] :
( icext(uri_ex_c1,uri_ex_w1)
| ~ iext(uri_rdf_first,sK11_skl,X0) ),
inference(resolution,[status(thm)],[f629,f64]) ).
fof(f647,plain,
icext(uri_ex_c1,uri_ex_w1),
inference(resolution,[status(thm)],[f646,f66]) ).
fof(f666,plain,
! [X0,X1] :
( ~ icext(X0,X1)
| icext(uri_ex_c4,X1)
| ~ iext(uri_rdf_first,sK4_skl,X0) ),
inference(resolution,[status(thm)],[f589,f81]) ).
fof(f667,plain,
! [X0,X1,X2,X3] :
( sP0_prd(X3,X2,X1,X0)
| ~ icext(uri_ex_c3,X3)
| ~ iext(uri_rdf_first,sK6_skl,X2)
| ~ iext(uri_rdf_first,sK7_skl,X1)
| ~ iext(uri_rdf_first,sK8_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f409,f79]) ).
fof(f668,plain,
! [X0,X1,X2] :
( sP0_prd(X2,X1,X0,uri_ex_w1)
| ~ icext(uri_ex_c3,X2)
| ~ iext(uri_rdf_first,sK6_skl,X1)
| ~ iext(uri_rdf_first,sK7_skl,X0) ),
inference(resolution,[status(thm)],[f667,f74]) ).
fof(f671,plain,
! [X0] :
( ~ icext(uri_ex_c2,X0)
| icext(uri_ex_c4,X0) ),
inference(resolution,[status(thm)],[f666,f83]) ).
fof(f673,plain,
! [X0,X1] :
( ~ icext(uri_ex_c1,X1)
| icext(uri_ex_c4,X1)
| ~ iext(uri_rdf_first,sK4_skl,X0) ),
inference(resolution,[status(thm)],[f590,f81]) ).
fof(f674,plain,
! [X0] :
( ~ icext(uri_ex_c1,X0)
| icext(uri_ex_c4,X0) ),
inference(resolution,[status(thm)],[f673,f83]) ).
fof(f678,plain,
! [X0,X1] :
( icext(uri_ex_c1,X1)
| ~ iext(uri_rdf_rest,sK11_skl,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK11_skl,X1)
| ~ iext(uri_rdf_first,sK12_skl,X0) ),
inference(resolution,[status(thm)],[f128,f65]) ).
fof(f683,plain,
! [X0,X1] :
( icext(uri_ex_c1,X1)
| ~ iext(uri_rdf_first,sK11_skl,X1)
| ~ iext(uri_rdf_first,sK12_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f678,f67]) ).
fof(f691,plain,
icext(uri_ex_c4,uri_ex_w1),
inference(resolution,[status(thm)],[f674,f647]) ).
fof(f697,plain,
! [X0] :
( icext(uri_ex_c1,X0)
| ~ iext(uri_rdf_first,sK11_skl,X0) ),
inference(resolution,[status(thm)],[f683,f64]) ).
fof(f698,plain,
icext(uri_ex_c1,uri_ex_w2),
inference(resolution,[status(thm)],[f697,f66]) ).
fof(f706,plain,
! [X0,X1,X2] :
( icext(X1,X2)
| icext(X0,X2)
| ~ icext(uri_ex_c4,X2)
| ~ iext(uri_rdf_first,sK4_skl,X1)
| ~ iext(uri_rdf_first,sK5_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f489,f84]) ).
fof(f707,plain,
! [X0,X1] :
( icext(X0,X1)
| icext(uri_ex_c1,X1)
| ~ icext(uri_ex_c4,X1)
| ~ iext(uri_rdf_first,sK4_skl,X0) ),
inference(resolution,[status(thm)],[f706,f81]) ).
fof(f708,plain,
! [X0] :
( icext(uri_ex_c2,X0)
| icext(uri_ex_c1,X0)
| ~ icext(uri_ex_c4,X0) ),
inference(resolution,[status(thm)],[f707,f83]) ).
fof(f710,plain,
( icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))
| icext(uri_ex_c2,sK3_skl(uri_ex_c4,uri_ex_c3))
| icext(uri_ex_c1,sK3_skl(uri_ex_c4,uri_ex_c3)) ),
inference(resolution,[status(thm)],[f708,f535]) ).
fof(f715,plain,
icext(uri_ex_c4,uri_ex_w2),
inference(resolution,[status(thm)],[f698,f674]) ).
fof(f728,plain,
! [X0,X1,X2,X3] :
( X3 = uri_ex_w2
| X3 = X1
| ~ icext(X2,X3)
| ~ iext(uri_owl_oneOf,X2,X0)
| ~ iext(uri_rdf_rest,X0,sK11_skl)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f142,f67]) ).
fof(f731,plain,
! [X0,X1] :
( X1 = uri_ex_w2
| X1 = X0
| ~ icext(uri_ex_c1,X1)
| ~ iext(uri_rdf_rest,sK12_skl,sK11_skl)
| ~ iext(uri_rdf_first,sK12_skl,X0) ),
inference(resolution,[status(thm)],[f728,f63]) ).
fof(f733,plain,
! [X0,X1] :
( X1 = uri_ex_w2
| X1 = X0
| ~ icext(uri_ex_c1,X1)
| ~ iext(uri_rdf_first,sK12_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f731,f65]) ).
fof(f759,plain,
! [X0] :
( X0 = uri_ex_w2
| X0 = uri_ex_w1
| ~ icext(uri_ex_c1,X0) ),
inference(resolution,[status(thm)],[f733,f64]) ).
fof(f804,plain,
! [X0,X1] :
( sP0_prd(X1,X0,uri_ex_w2,uri_ex_w1)
| ~ icext(uri_ex_c3,X1)
| ~ iext(uri_rdf_first,sK6_skl,X0) ),
inference(resolution,[status(thm)],[f668,f76]) ).
fof(f805,plain,
! [X0] :
( sP0_prd(X0,uri_ex_w3,uri_ex_w2,uri_ex_w1)
| ~ icext(uri_ex_c3,X0) ),
inference(resolution,[status(thm)],[f804,f78]) ).
fof(f1121,plain,
! [X0,X1,X2,X3,X4] :
( icext(uri_ex_c3,X4)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,sK8_skl,X1)
| ~ iext(uri_rdf_first,sK8_skl,X0) ),
inference(resolution,[status(thm)],[f201,f73]) ).
fof(f1139,plain,
! [X0,X1,X2,X3] :
( icext(uri_ex_c3,X3)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,sK7_skl,X2)
| ~ iext(uri_rdf_first,sK7_skl,X1)
| ~ iext(uri_rdf_first,sK8_skl,X0) ),
inference(resolution,[status(thm)],[f1121,f75]) ).
fof(f1231,plain,
! [X0,X1,X2,X3,X4] :
( icext(uri_ex_c3,X2)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,sK8_skl,X1)
| ~ iext(uri_rdf_first,sK8_skl,X0) ),
inference(resolution,[status(thm)],[f202,f73]) ).
fof(f1299,plain,
! [X0,X1,X2,X3,X4] :
( icext(uri_ex_c3,X0)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,sK8_skl,X1)
| ~ iext(uri_rdf_first,sK8_skl,X0) ),
inference(resolution,[status(thm)],[f203,f73]) ).
fof(f1340,plain,
! [X0,X1,X2] :
( icext(uri_ex_c3,X1)
| ~ iext(uri_rdf_rest,sK6_skl,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK6_skl,X2)
| ~ iext(uri_rdf_first,sK7_skl,X1)
| ~ iext(uri_rdf_rest,sK8_skl,sK7_skl)
| ~ iext(uri_rdf_first,sK8_skl,X0) ),
inference(resolution,[status(thm)],[f1231,f77]) ).
fof(f1352,plain,
! [X0,X1,X2] :
( icext(uri_ex_c3,X1)
| ~ iext(uri_rdf_rest,sK6_skl,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK6_skl,X2)
| ~ iext(uri_rdf_first,sK7_skl,X1)
| ~ iext(uri_rdf_first,sK8_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1340,f75]) ).
fof(f1359,plain,
! [X0,X1,X2] :
( icext(uri_ex_c3,X0)
| ~ iext(uri_rdf_rest,sK6_skl,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK6_skl,X2)
| ~ iext(uri_rdf_first,sK7_skl,X1)
| ~ iext(uri_rdf_rest,sK8_skl,sK7_skl)
| ~ iext(uri_rdf_first,sK8_skl,X0) ),
inference(resolution,[status(thm)],[f1299,f77]) ).
fof(f1371,plain,
! [X0,X1,X2] :
( icext(uri_ex_c3,X0)
| ~ iext(uri_rdf_rest,sK6_skl,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK6_skl,X2)
| ~ iext(uri_rdf_first,sK7_skl,X1)
| ~ iext(uri_rdf_first,sK8_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1359,f75]) ).
fof(f1560,plain,
! [X0,X1] :
( icext(uri_ex_c2,X1)
| ~ iext(uri_rdf_rest,sK9_skl,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK9_skl,X1)
| ~ iext(uri_rdf_first,sK10_skl,X0) ),
inference(resolution,[status(thm)],[f232,f70]) ).
fof(f1565,plain,
! [X0,X1] :
( icext(uri_ex_c2,X1)
| ~ iext(uri_rdf_first,sK9_skl,X1)
| ~ iext(uri_rdf_first,sK10_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1560,f72]) ).
fof(f1577,plain,
! [X0,X1,X2] :
( icext(uri_ex_c3,X2)
| ~ iext(uri_rdf_rest,sK6_skl,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK6_skl,X2)
| ~ iext(uri_rdf_first,sK7_skl,X1)
| ~ iext(uri_rdf_first,sK8_skl,X0) ),
inference(resolution,[status(thm)],[f1139,f77]) ).
fof(f1582,plain,
! [X0,X1,X2] :
( icext(uri_ex_c3,X2)
| ~ iext(uri_rdf_first,sK6_skl,X2)
| ~ iext(uri_rdf_first,sK7_skl,X1)
| ~ iext(uri_rdf_first,sK8_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1577,f79]) ).
fof(f1588,plain,
! [X0,X1] :
( icext(uri_ex_c3,X1)
| ~ iext(uri_rdf_first,sK6_skl,X1)
| ~ iext(uri_rdf_first,sK7_skl,X0) ),
inference(resolution,[status(thm)],[f1582,f74]) ).
fof(f1590,plain,
! [X0] :
( icext(uri_ex_c2,X0)
| ~ iext(uri_rdf_first,sK9_skl,X0) ),
inference(resolution,[status(thm)],[f1565,f69]) ).
fof(f1591,plain,
icext(uri_ex_c2,uri_ex_w3),
inference(resolution,[status(thm)],[f1590,f71]) ).
fof(f1592,plain,
icext(uri_ex_c4,uri_ex_w3),
inference(resolution,[status(thm)],[f1591,f671]) ).
fof(f1593,plain,
! [X0,X1,X2] :
( X2 = X1
| X2 = X0
| ~ icext(uri_ex_c2,X2)
| ~ iext(uri_rdf_rest,sK9_skl,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK9_skl,X1)
| ~ iext(uri_rdf_first,sK10_skl,X0) ),
inference(resolution,[status(thm)],[f234,f70]) ).
fof(f1598,plain,
! [X0,X1,X2] :
( X2 = X1
| X2 = X0
| ~ icext(uri_ex_c2,X2)
| ~ iext(uri_rdf_first,sK9_skl,X1)
| ~ iext(uri_rdf_first,sK10_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1593,f72]) ).
fof(f1658,plain,
! [X0] :
( icext(uri_ex_c3,X0)
| ~ iext(uri_rdf_first,sK6_skl,X0) ),
inference(resolution,[status(thm)],[f1588,f76]) ).
fof(f1659,plain,
icext(uri_ex_c3,uri_ex_w3),
inference(resolution,[status(thm)],[f1658,f78]) ).
fof(f1789,plain,
! [X0,X1] :
( X1 = X0
| X1 = uri_ex_w2
| ~ icext(uri_ex_c2,X1)
| ~ iext(uri_rdf_first,sK9_skl,X0) ),
inference(resolution,[status(thm)],[f1598,f69]) ).
fof(f1790,plain,
! [X0] :
( X0 = uri_ex_w3
| X0 = uri_ex_w2
| ~ icext(uri_ex_c2,X0) ),
inference(resolution,[status(thm)],[f1789,f71]) ).
fof(f1800,plain,
( icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))
| icext(uri_ex_c1,sK3_skl(uri_ex_c4,uri_ex_c3))
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w3
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2 ),
inference(resolution,[status(thm)],[f1790,f710]) ).
fof(f1829,plain,
( sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w1
| icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w3
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2 ),
inference(resolution,[status(thm)],[f1800,f759]) ).
fof(f1831,plain,
( sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w1
| icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w3
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2 ),
inference(duplicate_literals_removal,[status(thm)],[f1829]) ).
fof(f1832,plain,
( sP0_prd(sK3_skl(uri_ex_c4,uri_ex_c3),uri_ex_w3,uri_ex_w2,uri_ex_w1)
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w1
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w3
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2 ),
inference(resolution,[status(thm)],[f1831,f805]) ).
fof(f1833,plain,
( sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w1
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w3
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2 ),
inference(forward_subsumption_resolution,[status(thm)],[f1832,f87]) ).
fof(f1839,plain,
( sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w1
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2
| ~ icext(uri_ex_c4,uri_ex_w3)
| ~ icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))
| ~ ic(uri_ex_c4)
| ~ ic(uri_ex_c3)
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4) ),
inference(paramodulation,[status(thm)],[f1833,f58]) ).
fof(f1843,plain,
( sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w1
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2
| ~ icext(uri_ex_c4,uri_ex_w3)
| ~ icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))
| ~ ic(uri_ex_c4)
| ~ ic(uri_ex_c3) ),
inference(forward_subsumption_resolution,[status(thm)],[f1839,f60]) ).
fof(f1844,plain,
! [X0,X1,X2] :
( icext(uri_ex_c3,X1)
| ~ iext(uri_rdf_first,sK6_skl,X2)
| ~ iext(uri_rdf_first,sK7_skl,X1)
| ~ iext(uri_rdf_first,sK8_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1352,f79]) ).
fof(f1845,plain,
! [X0,X1] :
( icext(uri_ex_c3,X0)
| ~ iext(uri_rdf_first,sK6_skl,X1)
| ~ iext(uri_rdf_first,sK7_skl,X0) ),
inference(resolution,[status(thm)],[f1844,f74]) ).
fof(f1848,plain,
! [X0] :
( icext(uri_ex_c3,uri_ex_w2)
| ~ iext(uri_rdf_first,sK6_skl,X0) ),
inference(resolution,[status(thm)],[f1845,f76]) ).
fof(f1849,plain,
icext(uri_ex_c3,uri_ex_w2),
inference(resolution,[status(thm)],[f1848,f78]) ).
fof(f1861,plain,
( sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w1
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2
| ~ icext(uri_ex_c4,uri_ex_w3)
| ~ icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))
| ~ ic(uri_ex_c4) ),
inference(forward_subsumption_resolution,[status(thm)],[f1843,f96]) ).
fof(f1862,plain,
( sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w1
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w1
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2
| ~ icext(uri_ex_c4,uri_ex_w3)
| ~ icext(uri_ex_c3,uri_ex_w3)
| ~ ic(uri_ex_c4) ),
inference(paramodulation,[status(thm)],[f1833,f1861]) ).
fof(f1863,plain,
( sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w1
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2
| ~ icext(uri_ex_c4,uri_ex_w3)
| ~ icext(uri_ex_c3,uri_ex_w3)
| ~ ic(uri_ex_c4) ),
inference(duplicate_literals_removal,[status(thm)],[f1862]) ).
fof(f1864,plain,
( sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w1
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2
| ~ icext(uri_ex_c4,uri_ex_w3)
| ~ icext(uri_ex_c3,uri_ex_w3) ),
inference(forward_subsumption_resolution,[status(thm)],[f1863,f98]) ).
fof(f1870,plain,
( sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w1
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2
| ~ icext(uri_ex_c4,uri_ex_w3) ),
inference(forward_subsumption_resolution,[status(thm)],[f1864,f1659]) ).
fof(f1871,plain,
( sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w1
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2 ),
inference(resolution,[status(thm)],[f1870,f1592]) ).
fof(f1878,plain,
( sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2
| ~ icext(uri_ex_c4,uri_ex_w1)
| ~ icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))
| ~ ic(uri_ex_c4)
| ~ ic(uri_ex_c3)
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4) ),
inference(paramodulation,[status(thm)],[f1871,f58]) ).
fof(f1882,plain,
( sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2
| ~ icext(uri_ex_c4,uri_ex_w1)
| ~ icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))
| ~ ic(uri_ex_c4)
| ~ ic(uri_ex_c3) ),
inference(forward_subsumption_resolution,[status(thm)],[f1878,f60]) ).
fof(f1938,plain,
( sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2
| ~ icext(uri_ex_c4,uri_ex_w1)
| ~ icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))
| ~ ic(uri_ex_c4) ),
inference(forward_subsumption_resolution,[status(thm)],[f1882,f96]) ).
fof(f1940,plain,
( sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2
| sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2
| ~ icext(uri_ex_c4,uri_ex_w1)
| ~ icext(uri_ex_c3,uri_ex_w1)
| ~ ic(uri_ex_c4) ),
inference(paramodulation,[status(thm)],[f1871,f1938]) ).
fof(f1943,plain,
( sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2
| ~ icext(uri_ex_c4,uri_ex_w1)
| ~ icext(uri_ex_c3,uri_ex_w1)
| ~ ic(uri_ex_c4) ),
inference(duplicate_literals_removal,[status(thm)],[f1940]) ).
fof(f1944,plain,
( sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2
| ~ icext(uri_ex_c4,uri_ex_w1)
| ~ icext(uri_ex_c3,uri_ex_w1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1943,f98]) ).
fof(f1956,plain,
( sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2
| ~ icext(uri_ex_c3,uri_ex_w1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1944,f691]) ).
fof(f1967,plain,
! [X0,X1,X2] :
( icext(uri_ex_c3,X0)
| ~ iext(uri_rdf_first,sK6_skl,X2)
| ~ iext(uri_rdf_first,sK7_skl,X1)
| ~ iext(uri_rdf_first,sK8_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1371,f79]) ).
fof(f1968,plain,
! [X0,X1] :
( icext(uri_ex_c3,uri_ex_w1)
| ~ iext(uri_rdf_first,sK6_skl,X1)
| ~ iext(uri_rdf_first,sK7_skl,X0) ),
inference(resolution,[status(thm)],[f1967,f74]) ).
fof(f1969,plain,
! [X0] :
( icext(uri_ex_c3,uri_ex_w1)
| ~ iext(uri_rdf_first,sK6_skl,X0) ),
inference(resolution,[status(thm)],[f1968,f76]) ).
fof(f1970,plain,
icext(uri_ex_c3,uri_ex_w1),
inference(resolution,[status(thm)],[f1969,f78]) ).
fof(f1971,plain,
sK3_skl(uri_ex_c4,uri_ex_c3) = uri_ex_w2,
inference(backward_subsumption_resolution,[status(thm)],[f1956,f1970]) ).
fof(f2065,plain,
( ~ icext(uri_ex_c4,uri_ex_w2)
| ~ icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))
| ~ ic(uri_ex_c4)
| ~ ic(uri_ex_c3)
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4) ),
inference(paramodulation,[status(thm)],[f1971,f58]) ).
fof(f2071,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(forward_demodulation,[status(thm)],[f1971,f2065]) ).
fof(f2072,plain,
( ~ icext(uri_ex_c4,uri_ex_w2)
| ~ icext(uri_ex_c3,uri_ex_w2)
| ~ ic(uri_ex_c4)
| ~ ic(uri_ex_c3) ),
inference(forward_subsumption_resolution,[status(thm)],[f2071,f60]) ).
fof(f2073,plain,
( ~ icext(uri_ex_c4,uri_ex_w2)
| ~ icext(uri_ex_c3,uri_ex_w2)
| ~ ic(uri_ex_c4) ),
inference(forward_subsumption_resolution,[status(thm)],[f2072,f96]) ).
fof(f2074,plain,
( ~ icext(uri_ex_c3,uri_ex_w2)
| ~ ic(uri_ex_c4) ),
inference(resolution,[status(thm)],[f2073,f715]) ).
fof(f2075,plain,
~ icext(uri_ex_c3,uri_ex_w2),
inference(forward_subsumption_resolution,[status(thm)],[f2074,f98]) ).
fof(f2076,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f2075,f1849]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB021+2 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.38 % Computer : n016.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 : Mon Sep 21 07:45:10 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.40 % Drodi V4.1.1
% 7.48/1.40 % Refutation found
% 7.48/1.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.48/1.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.33/1.42 % Elapsed time: 1.024971 seconds
% 2.33/1.42 % CPU time: 7.776328 seconds
% 2.33/1.42 % Total memory used: 146.568 MB
% 2.33/1.42 % Net memory used: 136.455 MB
%------------------------------------------------------------------------------