%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWB067+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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:17 PM UTC 2026
% Result : Theorem 27.69s 4.06s
% Output : CNFRefutation 2.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 274
% Syntax : Number of formulae : 985 ( 144 unt; 187 def)
% Number of atoms : 2799 ( 37 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 3039 (1225 ~;1352 |; 220 &)
% ( 225 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 199 ( 197 usr; 188 prp; 0-3 aty)
% Number of functors : 78 ( 78 usr; 54 con; 0-2 aty)
% Number of variables : 1172 (1121 !; 51 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [S,P,O] :
( iext(P,S,O)
=> ip(P) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X] : ir(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [P,C,X,Y] :
( ( iext(P,X,Y)
& iext(uri_rdfs_domain,P,C) )
=> icext(C,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [X] :
( ic(X)
<=> icext(uri_rdfs_Class,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [X] :
( ir(X)
<=> icext(uri_rdfs_Resource,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [C,D] :
( iext(uri_rdfs_subClassOf,C,D)
=> ( ! [X] :
( icext(C,X)
=> icext(D,X) )
& ic(D)
& ic(C) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [C] :
( ic(C)
=> iext(uri_rdfs_subClassOf,C,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [C,D,E] :
( ( iext(uri_rdfs_subClassOf,D,E)
& iext(uri_rdfs_subClassOf,C,D) )
=> iext(uri_rdfs_subClassOf,C,E) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f88,axiom,
! [X] :
( ioap(X)
=> ip(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f91,axiom,
! [X] :
( iodp(X)
=> ip(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f106,axiom,
ic(uri_owl_AllDifferent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f108,axiom,
ic(uri_owl_AllDisjointClasses),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f110,axiom,
ic(uri_owl_AllDisjointProperties),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f113,axiom,
! [X] :
( icext(uri_owl_AnnotationProperty,X)
<=> ioap(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f114,axiom,
ic(uri_owl_AnnotationProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f116,axiom,
ic(uri_owl_AsymmetricProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f119,axiom,
! [X] :
( icext(uri_owl_Class,X)
<=> ic(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f120,axiom,
ic(uri_owl_Class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f122,axiom,
ic(uri_rdfs_Class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f123,axiom,
! [X] :
( icext(uri_owl_DataRange,X)
<=> idc(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f124,axiom,
ic(uri_owl_DataRange),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f125,axiom,
! [X] :
( icext(uri_rdfs_Datatype,X)
<=> idc(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f126,axiom,
ic(uri_rdfs_Datatype),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f127,axiom,
! [X] :
( icext(uri_owl_DatatypeProperty,X)
<=> iodp(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f128,axiom,
ic(uri_owl_DatatypeProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f134,axiom,
ic(uri_owl_FunctionalProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f136,axiom,
ic(uri_owl_InverseFunctionalProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f140,axiom,
idc(uri_rdfs_Literal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f145,axiom,
! [X] : ~ icext(uri_owl_Nothing,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f146,axiom,
ic(uri_owl_Nothing),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f147,axiom,
! [X] :
( icext(uri_owl_ObjectProperty,X)
<=> ip(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f148,axiom,
ic(uri_owl_ObjectProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f151,axiom,
! [X] :
( icext(uri_owl_OntologyProperty,X)
<=> ioxp(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f152,axiom,
ic(uri_owl_OntologyProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f153,axiom,
! [X] :
( icext(uri_rdf_Property,X)
<=> ip(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f154,axiom,
ic(uri_rdf_Property),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f156,axiom,
ic(uri_owl_ReflexiveProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f158,axiom,
ic(uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f162,axiom,
ic(uri_owl_SymmetricProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f163,axiom,
! [X] :
( icext(uri_owl_Thing,X)
<=> ir(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f164,axiom,
ic(uri_owl_Thing),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f166,axiom,
ic(uri_owl_TransitiveProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f168,axiom,
ip(uri_owl_allValuesFrom),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f176,axiom,
ip(uri_owl_assertionProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f178,axiom,
ioap(uri_owl_backwardCompatibleWith),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f180,axiom,
! [X,Y] : ~ iext(uri_owl_bottomDataProperty,X,Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f181,axiom,
iodp(uri_owl_bottomDataProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f182,axiom,
! [X,Y] : ~ iext(uri_owl_bottomObjectProperty,X,Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f183,axiom,
ip(uri_owl_bottomObjectProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f195,axiom,
ip(uri_owl_differentFrom),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f204,axiom,
! [X,Y] :
( iext(uri_owl_equivalentProperty,X,Y)
=> ( ip(Y)
& ip(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f205,axiom,
ip(uri_owl_equivalentProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f209,axiom,
ip(uri_owl_hasSelf),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f219,axiom,
! [X,Y] :
( iext(uri_owl_inverseOf,X,Y)
=> ( ip(Y)
& ip(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f220,axiom,
ip(uri_owl_inverseOf),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f251,axiom,
ip(uri_owl_propertyDisjointWith),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f255,axiom,
ip(uri_owl_sameAs),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f257,axiom,
ioap(uri_rdfs_seeAlso),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f266,axiom,
! [X,Y] :
( iext(uri_owl_topDataProperty,X,Y)
<=> ( lv(Y)
& ir(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f267,axiom,
iodp(uri_owl_topDataProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f268,axiom,
! [X,Y] :
( iext(uri_owl_topObjectProperty,X,Y)
<=> ( ir(Y)
& ir(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f269,axiom,
ip(uri_owl_topObjectProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f273,axiom,
ioap(uri_owl_versionInfo),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f275,axiom,
ioxp(uri_owl_versionIRI),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f277,axiom,
ip(uri_owl_withRestrictions),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f280,axiom,
! [Z] :
( iext(uri_owl_intersectionOf,Z,uri_rdf_nil)
<=> ( ! [X] :
( icext(Z,X)
<=> ir(X) )
& ic(Z) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f287,axiom,
! [Z] :
( iext(uri_owl_unionOf,Z,uri_rdf_nil)
<=> ( ! [X] : ~ icext(Z,X)
& ic(Z) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f294,axiom,
! [Z] :
( iext(uri_owl_oneOf,Z,uri_rdf_nil)
<=> ( ! [X] : ~ icext(Z,X)
& ic(Z) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f341,axiom,
! [P,C] :
( iext(uri_rdfs_domain,P,C)
<=> ( ! [X,Y] :
( iext(P,X,Y)
=> icext(C,X) )
& ic(C)
& ip(P) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f343,axiom,
! [C1,C2] :
( iext(uri_rdfs_subClassOf,C1,C2)
<=> ( ! [X] :
( icext(C1,X)
=> icext(C2,X) )
& ic(C2)
& ic(C1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f345,axiom,
! [X,Y] :
( iext(uri_owl_differentFrom,X,Y)
<=> X != Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f352,axiom,
! [P1,P2] :
( iext(uri_owl_equivalentProperty,P1,P2)
<=> ( ! [X,Y] :
( iext(P1,X,Y)
<=> iext(P2,X,Y) )
& ip(P2)
& ip(P1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f354,axiom,
! [X,Y] :
( iext(uri_owl_sameAs,X,Y)
<=> X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f363,axiom,
? [Z] :
( iext(uri_owl_members,Z,uri_rdf_nil)
& icext(uri_owl_AllDifferent,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f371,axiom,
? [Z] :
( iext(uri_owl_members,Z,uri_rdf_nil)
& icext(uri_owl_AllDisjointClasses,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f379,axiom,
? [Z] :
( iext(uri_owl_members,Z,uri_rdf_nil)
& icext(uri_owl_AllDisjointProperties,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f391,axiom,
! [P1,P2] :
( iext(uri_owl_inverseOf,P1,P2)
<=> ( ! [X,Y] :
( iext(P1,X,Y)
<=> iext(P2,Y,X) )
& ip(P2)
& ip(P1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f392,axiom,
! [P] :
( icext(uri_owl_AsymmetricProperty,P)
<=> ( ! [X,Y] :
( iext(P,X,Y)
=> ~ iext(P,Y,X) )
& ip(P) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f393,axiom,
! [P] :
( icext(uri_owl_FunctionalProperty,P)
<=> ( ! [X,Y1,Y2] :
( ( iext(P,X,Y2)
& iext(P,X,Y1) )
=> Y1 = Y2 )
& ip(P) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f394,axiom,
! [P] :
( icext(uri_owl_InverseFunctionalProperty,P)
<=> ( ! [X1,X2,Y] :
( ( iext(P,X2,Y)
& iext(P,X1,Y) )
=> X1 = X2 )
& ip(P) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f396,axiom,
! [P] :
( icext(uri_owl_ReflexiveProperty,P)
<=> ( ! [X] : iext(P,X,X)
& ip(P) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f397,axiom,
! [P] :
( icext(uri_owl_SymmetricProperty,P)
<=> ( ! [X,Y] :
( iext(P,X,Y)
=> iext(P,Y,X) )
& ip(P) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f398,axiom,
! [P] :
( icext(uri_owl_TransitiveProperty,P)
<=> ( ! [X,Y,Z] :
( ( iext(P,Y,Z)
& iext(P,X,Y) )
=> iext(P,X,Z) )
& ip(P) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f472,axiom,
idc(uri_rdf_XMLLiteral),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f558,axiom,
iodp(uri_xsd_pattern),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f559,conjecture,
iext(uri_owl_equivalentProperty,uri_ex_p3,uri_ex_p1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f560,negated_conjecture,
~ iext(uri_owl_equivalentProperty,uri_ex_p3,uri_ex_p1),
inference(negated_conjecture,[status(cth)],[f559]) ).
fof(f561,axiom,
( iext(uri_owl_inverseOf,uri_ex_p2,uri_ex_p1)
& iext(uri_owl_inverseOf,uri_ex_p3,uri_ex_p2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f562,plain,
! [S,P,O] :
( ip(P)
| ~ iext(P,S,O) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f563,plain,
! [P] :
( ip(P)
| ! [S,O] : ~ iext(P,S,O) ),
inference(miniscoping,[status(thm)],[f562]) ).
fof(f564,plain,
! [X0,X1,X2] :
( ip(X0)
| ~ iext(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f563]) ).
fof(f565,plain,
! [X0] : ir(X0),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f625,plain,
! [P,C,X,Y] :
( icext(C,X)
| ~ iext(P,X,Y)
| ~ iext(uri_rdfs_domain,P,C) ),
inference(pre_NNF_transformation,[status(thm)],[f52]) ).
fof(f626,plain,
! [C,X] :
( icext(C,X)
| ! [P] :
( ! [Y] : ~ iext(P,X,Y)
| ~ iext(uri_rdfs_domain,P,C) ) ),
inference(miniscoping,[status(thm)],[f625]) ).
fof(f627,plain,
! [X0,X1,X2,X3] :
( icext(X1,X2)
| ~ iext(X0,X2,X3)
| ~ iext(uri_rdfs_domain,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f626]) ).
fof(f629,plain,
! [X] :
( ( ~ icext(uri_rdfs_Class,X)
| ic(X) )
& ( icext(uri_rdfs_Class,X)
| ~ ic(X) ) ),
inference(NNF_transformation,[status(thm)],[f54]) ).
fof(f630,plain,
( ! [X] :
( ~ icext(uri_rdfs_Class,X)
| ic(X) )
& ! [X] :
( icext(uri_rdfs_Class,X)
| ~ ic(X) ) ),
inference(miniscoping,[status(thm)],[f629]) ).
fof(f631,plain,
! [X0] :
( icext(uri_rdfs_Class,X0)
| ~ ic(X0) ),
inference(cnf_transformation,[status(thm)],[f630]) ).
fof(f633,plain,
! [X] :
( ( ~ icext(uri_rdfs_Resource,X)
| ir(X) )
& ( icext(uri_rdfs_Resource,X)
| ~ ir(X) ) ),
inference(NNF_transformation,[status(thm)],[f55]) ).
fof(f634,plain,
( ! [X] :
( ~ icext(uri_rdfs_Resource,X)
| ir(X) )
& ! [X] :
( icext(uri_rdfs_Resource,X)
| ~ ir(X) ) ),
inference(miniscoping,[status(thm)],[f633]) ).
fof(f635,plain,
! [X0] :
( icext(uri_rdfs_Resource,X0)
| ~ ir(X0) ),
inference(cnf_transformation,[status(thm)],[f634]) ).
fof(f654,plain,
! [C,D] :
( ( ! [X] :
( icext(D,X)
| ~ icext(C,X) )
& ic(D)
& ic(C) )
| ~ iext(uri_rdfs_subClassOf,C,D) ),
inference(pre_NNF_transformation,[status(thm)],[f68]) ).
fof(f657,plain,
! [X0,X1,X2] :
( icext(X1,X2)
| ~ icext(X0,X2)
| ~ iext(uri_rdfs_subClassOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f654]) ).
fof(f659,plain,
! [C] :
( iext(uri_rdfs_subClassOf,C,C)
| ~ ic(C) ),
inference(pre_NNF_transformation,[status(thm)],[f70]) ).
fof(f660,plain,
! [X0] :
( iext(uri_rdfs_subClassOf,X0,X0)
| ~ ic(X0) ),
inference(cnf_transformation,[status(thm)],[f659]) ).
fof(f661,plain,
! [C,D,E] :
( iext(uri_rdfs_subClassOf,C,E)
| ~ iext(uri_rdfs_subClassOf,D,E)
| ~ iext(uri_rdfs_subClassOf,C,D) ),
inference(pre_NNF_transformation,[status(thm)],[f71]) ).
fof(f662,plain,
! [C,E] :
( iext(uri_rdfs_subClassOf,C,E)
| ! [D] :
( ~ iext(uri_rdfs_subClassOf,D,E)
| ~ iext(uri_rdfs_subClassOf,C,D) ) ),
inference(miniscoping,[status(thm)],[f661]) ).
fof(f663,plain,
! [X0,X1,X2] :
( iext(uri_rdfs_subClassOf,X0,X2)
| ~ iext(uri_rdfs_subClassOf,X1,X2)
| ~ iext(uri_rdfs_subClassOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f662]) ).
fof(f698,plain,
! [X] :
( ip(X)
| ~ ioap(X) ),
inference(pre_NNF_transformation,[status(thm)],[f88]) ).
fof(f699,plain,
! [X0] :
( ip(X0)
| ~ ioap(X0) ),
inference(cnf_transformation,[status(thm)],[f698]) ).
fof(f707,plain,
! [X] :
( ip(X)
| ~ iodp(X) ),
inference(pre_NNF_transformation,[status(thm)],[f91]) ).
fof(f708,plain,
! [X0] :
( ip(X0)
| ~ iodp(X0) ),
inference(cnf_transformation,[status(thm)],[f707]) ).
fof(f751,plain,
ic(uri_owl_AllDifferent),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f754,plain,
ic(uri_owl_AllDisjointClasses),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f757,plain,
ic(uri_owl_AllDisjointProperties),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f761,plain,
! [X] :
( ( ~ ioap(X)
| icext(uri_owl_AnnotationProperty,X) )
& ( ioap(X)
| ~ icext(uri_owl_AnnotationProperty,X) ) ),
inference(NNF_transformation,[status(thm)],[f113]) ).
fof(f762,plain,
( ! [X] :
( ~ ioap(X)
| icext(uri_owl_AnnotationProperty,X) )
& ! [X] :
( ioap(X)
| ~ icext(uri_owl_AnnotationProperty,X) ) ),
inference(miniscoping,[status(thm)],[f761]) ).
fof(f764,plain,
! [X0] :
( ~ ioap(X0)
| icext(uri_owl_AnnotationProperty,X0) ),
inference(cnf_transformation,[status(thm)],[f762]) ).
fof(f765,plain,
ic(uri_owl_AnnotationProperty),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f768,plain,
ic(uri_owl_AsymmetricProperty),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f772,plain,
! [X] :
( ( ~ ic(X)
| icext(uri_owl_Class,X) )
& ( ic(X)
| ~ icext(uri_owl_Class,X) ) ),
inference(NNF_transformation,[status(thm)],[f119]) ).
fof(f773,plain,
( ! [X] :
( ~ ic(X)
| icext(uri_owl_Class,X) )
& ! [X] :
( ic(X)
| ~ icext(uri_owl_Class,X) ) ),
inference(miniscoping,[status(thm)],[f772]) ).
fof(f775,plain,
! [X0] :
( ~ ic(X0)
| icext(uri_owl_Class,X0) ),
inference(cnf_transformation,[status(thm)],[f773]) ).
fof(f776,plain,
ic(uri_owl_Class),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f781,plain,
ic(uri_rdfs_Class),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f782,plain,
! [X] :
( ( ~ idc(X)
| icext(uri_owl_DataRange,X) )
& ( idc(X)
| ~ icext(uri_owl_DataRange,X) ) ),
inference(NNF_transformation,[status(thm)],[f123]) ).
fof(f783,plain,
( ! [X] :
( ~ idc(X)
| icext(uri_owl_DataRange,X) )
& ! [X] :
( idc(X)
| ~ icext(uri_owl_DataRange,X) ) ),
inference(miniscoping,[status(thm)],[f782]) ).
fof(f785,plain,
! [X0] :
( ~ idc(X0)
| icext(uri_owl_DataRange,X0) ),
inference(cnf_transformation,[status(thm)],[f783]) ).
fof(f786,plain,
ic(uri_owl_DataRange),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f787,plain,
! [X] :
( ( ~ idc(X)
| icext(uri_rdfs_Datatype,X) )
& ( idc(X)
| ~ icext(uri_rdfs_Datatype,X) ) ),
inference(NNF_transformation,[status(thm)],[f125]) ).
fof(f788,plain,
( ! [X] :
( ~ idc(X)
| icext(uri_rdfs_Datatype,X) )
& ! [X] :
( idc(X)
| ~ icext(uri_rdfs_Datatype,X) ) ),
inference(miniscoping,[status(thm)],[f787]) ).
fof(f790,plain,
! [X0] :
( ~ idc(X0)
| icext(uri_rdfs_Datatype,X0) ),
inference(cnf_transformation,[status(thm)],[f788]) ).
fof(f791,plain,
ic(uri_rdfs_Datatype),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f792,plain,
! [X] :
( ( ~ iodp(X)
| icext(uri_owl_DatatypeProperty,X) )
& ( iodp(X)
| ~ icext(uri_owl_DatatypeProperty,X) ) ),
inference(NNF_transformation,[status(thm)],[f127]) ).
fof(f793,plain,
( ! [X] :
( ~ iodp(X)
| icext(uri_owl_DatatypeProperty,X) )
& ! [X] :
( iodp(X)
| ~ icext(uri_owl_DatatypeProperty,X) ) ),
inference(miniscoping,[status(thm)],[f792]) ).
fof(f795,plain,
! [X0] :
( ~ iodp(X0)
| icext(uri_owl_DatatypeProperty,X0) ),
inference(cnf_transformation,[status(thm)],[f793]) ).
fof(f796,plain,
ic(uri_owl_DatatypeProperty),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f805,plain,
ic(uri_owl_FunctionalProperty),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f808,plain,
ic(uri_owl_InverseFunctionalProperty),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f816,plain,
idc(uri_rdfs_Literal),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f823,plain,
! [X0] : ~ icext(uri_owl_Nothing,X0),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f824,plain,
ic(uri_owl_Nothing),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f825,plain,
! [X] :
( ( ~ ip(X)
| icext(uri_owl_ObjectProperty,X) )
& ( ip(X)
| ~ icext(uri_owl_ObjectProperty,X) ) ),
inference(NNF_transformation,[status(thm)],[f147]) ).
fof(f826,plain,
( ! [X] :
( ~ ip(X)
| icext(uri_owl_ObjectProperty,X) )
& ! [X] :
( ip(X)
| ~ icext(uri_owl_ObjectProperty,X) ) ),
inference(miniscoping,[status(thm)],[f825]) ).
fof(f828,plain,
! [X0] :
( ~ ip(X0)
| icext(uri_owl_ObjectProperty,X0) ),
inference(cnf_transformation,[status(thm)],[f826]) ).
fof(f829,plain,
ic(uri_owl_ObjectProperty),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f835,plain,
! [X] :
( ( ~ ioxp(X)
| icext(uri_owl_OntologyProperty,X) )
& ( ioxp(X)
| ~ icext(uri_owl_OntologyProperty,X) ) ),
inference(NNF_transformation,[status(thm)],[f151]) ).
fof(f836,plain,
( ! [X] :
( ~ ioxp(X)
| icext(uri_owl_OntologyProperty,X) )
& ! [X] :
( ioxp(X)
| ~ icext(uri_owl_OntologyProperty,X) ) ),
inference(miniscoping,[status(thm)],[f835]) ).
fof(f838,plain,
! [X0] :
( ~ ioxp(X0)
| icext(uri_owl_OntologyProperty,X0) ),
inference(cnf_transformation,[status(thm)],[f836]) ).
fof(f839,plain,
ic(uri_owl_OntologyProperty),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f840,plain,
! [X] :
( ( ~ ip(X)
| icext(uri_rdf_Property,X) )
& ( ip(X)
| ~ icext(uri_rdf_Property,X) ) ),
inference(NNF_transformation,[status(thm)],[f153]) ).
fof(f841,plain,
( ! [X] :
( ~ ip(X)
| icext(uri_rdf_Property,X) )
& ! [X] :
( ip(X)
| ~ icext(uri_rdf_Property,X) ) ),
inference(miniscoping,[status(thm)],[f840]) ).
fof(f843,plain,
! [X0] :
( ~ ip(X0)
| icext(uri_rdf_Property,X0) ),
inference(cnf_transformation,[status(thm)],[f841]) ).
fof(f844,plain,
ic(uri_rdf_Property),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f847,plain,
ic(uri_owl_ReflexiveProperty),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f852,plain,
ic(uri_rdfs_Resource),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f858,plain,
ic(uri_owl_SymmetricProperty),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f859,plain,
! [X] :
( ( ~ ir(X)
| icext(uri_owl_Thing,X) )
& ( ir(X)
| ~ icext(uri_owl_Thing,X) ) ),
inference(NNF_transformation,[status(thm)],[f163]) ).
fof(f860,plain,
( ! [X] :
( ~ ir(X)
| icext(uri_owl_Thing,X) )
& ! [X] :
( ir(X)
| ~ icext(uri_owl_Thing,X) ) ),
inference(miniscoping,[status(thm)],[f859]) ).
fof(f862,plain,
! [X0] :
( ~ ir(X0)
| icext(uri_owl_Thing,X0) ),
inference(cnf_transformation,[status(thm)],[f860]) ).
fof(f863,plain,
ic(uri_owl_Thing),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f866,plain,
ic(uri_owl_TransitiveProperty),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f870,plain,
ip(uri_owl_allValuesFrom),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f886,plain,
ip(uri_owl_assertionProperty),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f890,plain,
ioap(uri_owl_backwardCompatibleWith),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f892,plain,
! [X0,X1] : ~ iext(uri_owl_bottomDataProperty,X0,X1),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f893,plain,
iodp(uri_owl_bottomDataProperty),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f894,plain,
! [X0,X1] : ~ iext(uri_owl_bottomObjectProperty,X0,X1),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f895,plain,
ip(uri_owl_bottomObjectProperty),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f919,plain,
ip(uri_owl_differentFrom),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f936,plain,
! [X,Y] :
( ( ip(Y)
& ip(X) )
| ~ iext(uri_owl_equivalentProperty,X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f204]) ).
fof(f937,plain,
! [X0,X1] :
( ip(X0)
| ~ iext(uri_owl_equivalentProperty,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f936]) ).
fof(f938,plain,
! [X0,X1] :
( ip(X1)
| ~ iext(uri_owl_equivalentProperty,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f936]) ).
fof(f939,plain,
ip(uri_owl_equivalentProperty),
inference(cnf_transformation,[status(thm)],[f205]) ).
fof(f947,plain,
ip(uri_owl_hasSelf),
inference(cnf_transformation,[status(thm)],[f209]) ).
fof(f965,plain,
! [X,Y] :
( ( ip(Y)
& ip(X) )
| ~ iext(uri_owl_inverseOf,X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f219]) ).
fof(f966,plain,
! [X0,X1] :
( ip(X0)
| ~ iext(uri_owl_inverseOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f965]) ).
fof(f967,plain,
! [X0,X1] :
( ip(X1)
| ~ iext(uri_owl_inverseOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f965]) ).
fof(f968,plain,
ip(uri_owl_inverseOf),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f1029,plain,
ip(uri_owl_propertyDisjointWith),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f1037,plain,
ip(uri_owl_sameAs),
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f1041,plain,
ioap(uri_rdfs_seeAlso),
inference(cnf_transformation,[status(thm)],[f257]) ).
fof(f1058,plain,
! [X,Y] :
( ( ~ lv(Y)
| ~ ir(X)
| iext(uri_owl_topDataProperty,X,Y) )
& ( ( lv(Y)
& ir(X) )
| ~ iext(uri_owl_topDataProperty,X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f266]) ).
fof(f1059,plain,
( ! [X,Y] :
( ~ lv(Y)
| ~ ir(X)
| iext(uri_owl_topDataProperty,X,Y) )
& ! [X,Y] :
( ( lv(Y)
& ir(X) )
| ~ iext(uri_owl_topDataProperty,X,Y) ) ),
inference(miniscoping,[status(thm)],[f1058]) ).
fof(f1061,plain,
! [X0,X1] :
( lv(X1)
| ~ iext(uri_owl_topDataProperty,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1059]) ).
fof(f1062,plain,
! [X0,X1] :
( ~ lv(X1)
| ~ ir(X0)
| iext(uri_owl_topDataProperty,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1059]) ).
fof(f1063,plain,
iodp(uri_owl_topDataProperty),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f1064,plain,
! [X,Y] :
( ( ~ ir(Y)
| ~ ir(X)
| iext(uri_owl_topObjectProperty,X,Y) )
& ( ( ir(Y)
& ir(X) )
| ~ iext(uri_owl_topObjectProperty,X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f268]) ).
fof(f1065,plain,
( ! [X,Y] :
( ~ ir(Y)
| ~ ir(X)
| iext(uri_owl_topObjectProperty,X,Y) )
& ! [X,Y] :
( ( ir(Y)
& ir(X) )
| ~ iext(uri_owl_topObjectProperty,X,Y) ) ),
inference(miniscoping,[status(thm)],[f1064]) ).
fof(f1068,plain,
! [X0,X1] :
( ~ ir(X1)
| ~ ir(X0)
| iext(uri_owl_topObjectProperty,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1065]) ).
fof(f1069,plain,
ip(uri_owl_topObjectProperty),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f1077,plain,
ioap(uri_owl_versionInfo),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f1081,plain,
ioxp(uri_owl_versionIRI),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f1085,plain,
ip(uri_owl_withRestrictions),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f1099,plain,
! [Z] :
( ( ? [X] :
( ( ir(X)
| icext(Z,X) )
& ( ~ ir(X)
| ~ icext(Z,X) ) )
| ~ ic(Z)
| iext(uri_owl_intersectionOf,Z,uri_rdf_nil) )
& ( ( ! [X] :
( ( ~ ir(X)
| icext(Z,X) )
& ( ir(X)
| ~ icext(Z,X) ) )
& ic(Z) )
| ~ iext(uri_owl_intersectionOf,Z,uri_rdf_nil) ) ),
inference(NNF_transformation,[status(thm)],[f280]) ).
fof(f1100,plain,
( ! [Z] :
( ? [X] :
( ( ir(X)
| icext(Z,X) )
& ( ~ ir(X)
| ~ icext(Z,X) ) )
| ~ ic(Z)
| iext(uri_owl_intersectionOf,Z,uri_rdf_nil) )
& ! [Z] :
( ( ! [X] :
( ~ ir(X)
| icext(Z,X) )
& ! [X] :
( ir(X)
| ~ icext(Z,X) )
& ic(Z) )
| ~ iext(uri_owl_intersectionOf,Z,uri_rdf_nil) ) ),
inference(miniscoping,[status(thm)],[f1099]) ).
fof(f1101,plain,
( ! [Z] :
( ( ( ir(sK1_skl(Z))
| icext(Z,sK1_skl(Z)) )
& ( ~ ir(sK1_skl(Z))
| ~ icext(Z,sK1_skl(Z)) ) )
| ~ ic(Z)
| iext(uri_owl_intersectionOf,Z,uri_rdf_nil) )
& ! [Z] :
( ( ! [X] :
( ~ ir(X)
| icext(Z,X) )
& ! [X] :
( ir(X)
| ~ icext(Z,X) )
& ic(Z) )
| ~ iext(uri_owl_intersectionOf,Z,uri_rdf_nil) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(X,sK1_skl(Z))],[f1100]) ).
fof(f1104,plain,
! [X0,X1] :
( ~ ir(X1)
| icext(X0,X1)
| ~ iext(uri_owl_intersectionOf,X0,uri_rdf_nil) ),
inference(cnf_transformation,[status(thm)],[f1101]) ).
fof(f1105,plain,
! [X0] :
( ~ ir(sK1_skl(X0))
| ~ icext(X0,sK1_skl(X0))
| ~ ic(X0)
| iext(uri_owl_intersectionOf,X0,uri_rdf_nil) ),
inference(cnf_transformation,[status(thm)],[f1101]) ).
fof(f1153,plain,
! [Z] :
( ( ? [X] : icext(Z,X)
| ~ ic(Z)
| iext(uri_owl_unionOf,Z,uri_rdf_nil) )
& ( ( ! [X] : ~ icext(Z,X)
& ic(Z) )
| ~ iext(uri_owl_unionOf,Z,uri_rdf_nil) ) ),
inference(NNF_transformation,[status(thm)],[f287]) ).
fof(f1154,plain,
( ! [Z] :
( ? [X] : icext(Z,X)
| ~ ic(Z)
| iext(uri_owl_unionOf,Z,uri_rdf_nil) )
& ! [Z] :
( ( ! [X] : ~ icext(Z,X)
& ic(Z) )
| ~ iext(uri_owl_unionOf,Z,uri_rdf_nil) ) ),
inference(miniscoping,[status(thm)],[f1153]) ).
fof(f1155,plain,
( ! [Z] :
( icext(Z,sK5_skl(Z))
| ~ ic(Z)
| iext(uri_owl_unionOf,Z,uri_rdf_nil) )
& ! [Z] :
( ( ! [X] : ~ icext(Z,X)
& ic(Z) )
| ~ iext(uri_owl_unionOf,Z,uri_rdf_nil) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(X,sK5_skl(Z))],[f1154]) ).
fof(f1157,plain,
! [X0,X1] :
( ~ icext(X0,X1)
| ~ iext(uri_owl_unionOf,X0,uri_rdf_nil) ),
inference(cnf_transformation,[status(thm)],[f1155]) ).
fof(f1158,plain,
! [X0] :
( icext(X0,sK5_skl(X0))
| ~ ic(X0)
| iext(uri_owl_unionOf,X0,uri_rdf_nil) ),
inference(cnf_transformation,[status(thm)],[f1155]) ).
fof(f1205,plain,
! [Z] :
( ( ? [X] : icext(Z,X)
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,uri_rdf_nil) )
& ( ( ! [X] : ~ icext(Z,X)
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,uri_rdf_nil) ) ),
inference(NNF_transformation,[status(thm)],[f294]) ).
fof(f1206,plain,
( ! [Z] :
( ? [X] : icext(Z,X)
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,uri_rdf_nil) )
& ! [Z] :
( ( ! [X] : ~ icext(Z,X)
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,uri_rdf_nil) ) ),
inference(miniscoping,[status(thm)],[f1205]) ).
fof(f1207,plain,
( ! [Z] :
( icext(Z,sK9_skl(Z))
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,uri_rdf_nil) )
& ! [Z] :
( ( ! [X] : ~ icext(Z,X)
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,uri_rdf_nil) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X,sK9_skl(Z))],[f1206]) ).
fof(f1209,plain,
! [X0,X1] :
( ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,uri_rdf_nil) ),
inference(cnf_transformation,[status(thm)],[f1207]) ).
fof(f1210,plain,
! [X0] :
( icext(X0,sK9_skl(X0))
| ~ ic(X0)
| iext(uri_owl_oneOf,X0,uri_rdf_nil) ),
inference(cnf_transformation,[status(thm)],[f1207]) ).
fof(f1713,plain,
! [P,C] :
( iext(uri_rdfs_domain,P,C)
<=> ( ! [X,Y] :
( icext(C,X)
| ~ iext(P,X,Y) )
& ic(C)
& ip(P) ) ),
inference(pre_NNF_transformation,[status(thm)],[f341]) ).
fof(f1714,plain,
! [P,C] :
( ( ? [X,Y] :
( ~ icext(C,X)
& iext(P,X,Y) )
| ~ ic(C)
| ~ ip(P)
| iext(uri_rdfs_domain,P,C) )
& ( ( ! [X,Y] :
( icext(C,X)
| ~ iext(P,X,Y) )
& ic(C)
& ip(P) )
| ~ iext(uri_rdfs_domain,P,C) ) ),
inference(NNF_transformation,[status(thm)],[f1713]) ).
fof(f1715,plain,
( ! [P,C] :
( ? [X] :
( ~ icext(C,X)
& ? [Y] : iext(P,X,Y) )
| ~ ic(C)
| ~ ip(P)
| iext(uri_rdfs_domain,P,C) )
& ! [P,C] :
( ( ! [X] :
( icext(C,X)
| ! [Y] : ~ iext(P,X,Y) )
& ic(C)
& ip(P) )
| ~ iext(uri_rdfs_domain,P,C) ) ),
inference(miniscoping,[status(thm)],[f1714]) ).
fof(f1716,plain,
( ! [P,C] :
( ( ~ icext(C,sK111_skl(C,P))
& iext(P,sK111_skl(C,P),sK112_skl(C,P)) )
| ~ ic(C)
| ~ ip(P)
| iext(uri_rdfs_domain,P,C) )
& ! [P,C] :
( ( ! [X] :
( icext(C,X)
| ! [Y] : ~ iext(P,X,Y) )
& ic(C)
& ip(P) )
| ~ iext(uri_rdfs_domain,P,C) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK111_skl,sK112_skl]),skolemize(X,sK111_skl(C,P)),skolemize(Y,sK112_skl(C,P))],[f1715]) ).
fof(f1720,plain,
! [X0,X1] :
( iext(X0,sK111_skl(X1,X0),sK112_skl(X1,X0))
| ~ ic(X1)
| ~ ip(X0)
| iext(uri_rdfs_domain,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1716]) ).
fof(f1731,plain,
! [C1,C2] :
( iext(uri_rdfs_subClassOf,C1,C2)
<=> ( ! [X] :
( icext(C2,X)
| ~ icext(C1,X) )
& ic(C2)
& ic(C1) ) ),
inference(pre_NNF_transformation,[status(thm)],[f343]) ).
fof(f1732,plain,
! [C1,C2] :
( ( ? [X] :
( ~ icext(C2,X)
& icext(C1,X) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_rdfs_subClassOf,C1,C2) )
& ( ( ! [X] :
( icext(C2,X)
| ~ icext(C1,X) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_rdfs_subClassOf,C1,C2) ) ),
inference(NNF_transformation,[status(thm)],[f1731]) ).
fof(f1733,plain,
( ! [C1,C2] :
( ? [X] :
( ~ icext(C2,X)
& icext(C1,X) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_rdfs_subClassOf,C1,C2) )
& ! [C1,C2] :
( ( ! [X] :
( icext(C2,X)
| ~ icext(C1,X) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_rdfs_subClassOf,C1,C2) ) ),
inference(miniscoping,[status(thm)],[f1732]) ).
fof(f1734,plain,
( ! [C1,C2] :
( ( ~ icext(C2,sK115_skl(C2,C1))
& icext(C1,sK115_skl(C2,C1)) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_rdfs_subClassOf,C1,C2) )
& ! [C1,C2] :
( ( ! [X] :
( icext(C2,X)
| ~ icext(C1,X) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_rdfs_subClassOf,C1,C2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK115_skl]),skolemize(X,sK115_skl(C2,C1))],[f1733]) ).
fof(f1738,plain,
! [X0,X1] :
( icext(X0,sK115_skl(X1,X0))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1734]) ).
fof(f1739,plain,
! [X0,X1] :
( ~ icext(X1,sK115_skl(X1,X0))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1734]) ).
fof(f1749,plain,
! [X,Y] :
( ( X = Y
| iext(uri_owl_differentFrom,X,Y) )
& ( X != Y
| ~ iext(uri_owl_differentFrom,X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f345]) ).
fof(f1750,plain,
( ! [X,Y] :
( X = Y
| iext(uri_owl_differentFrom,X,Y) )
& ! [X,Y] :
( X != Y
| ~ iext(uri_owl_differentFrom,X,Y) ) ),
inference(miniscoping,[status(thm)],[f1749]) ).
fof(f1751,plain,
! [X0,X1] :
( X0 != X1
| ~ iext(uri_owl_differentFrom,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1750]) ).
fof(f1752,plain,
! [X0,X1] :
( X0 = X1
| iext(uri_owl_differentFrom,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1750]) ).
fof(f1814,plain,
! [P1,P2] :
( ( ? [X,Y] :
( ( iext(P2,X,Y)
| iext(P1,X,Y) )
& ( ~ iext(P2,X,Y)
| ~ iext(P1,X,Y) ) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_owl_equivalentProperty,P1,P2) )
& ( ( ! [X,Y] :
( ( ~ iext(P2,X,Y)
| iext(P1,X,Y) )
& ( iext(P2,X,Y)
| ~ iext(P1,X,Y) ) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_owl_equivalentProperty,P1,P2) ) ),
inference(NNF_transformation,[status(thm)],[f352]) ).
fof(f1815,plain,
( ! [P1,P2] :
( ? [X,Y] :
( ( iext(P2,X,Y)
| iext(P1,X,Y) )
& ( ~ iext(P2,X,Y)
| ~ iext(P1,X,Y) ) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_owl_equivalentProperty,P1,P2) )
& ! [P1,P2] :
( ( ! [X,Y] :
( ~ iext(P2,X,Y)
| iext(P1,X,Y) )
& ! [X,Y] :
( iext(P2,X,Y)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_owl_equivalentProperty,P1,P2) ) ),
inference(miniscoping,[status(thm)],[f1814]) ).
fof(f1816,plain,
( ! [P1,P2] :
( ( ( iext(P2,sK124_skl(P2,P1),sK125_skl(P2,P1))
| iext(P1,sK124_skl(P2,P1),sK125_skl(P2,P1)) )
& ( ~ iext(P2,sK124_skl(P2,P1),sK125_skl(P2,P1))
| ~ iext(P1,sK124_skl(P2,P1),sK125_skl(P2,P1)) ) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_owl_equivalentProperty,P1,P2) )
& ! [P1,P2] :
( ( ! [X,Y] :
( ~ iext(P2,X,Y)
| iext(P1,X,Y) )
& ! [X,Y] :
( iext(P2,X,Y)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_owl_equivalentProperty,P1,P2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK124_skl,sK125_skl]),skolemize(X,sK124_skl(P2,P1)),skolemize(Y,sK125_skl(P2,P1))],[f1815]) ).
fof(f1819,plain,
! [X0,X1,X2,X3] :
( iext(X1,X2,X3)
| ~ iext(X0,X2,X3)
| ~ iext(uri_owl_equivalentProperty,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1816]) ).
fof(f1820,plain,
! [X0,X1,X2,X3] :
( ~ iext(X1,X2,X3)
| iext(X0,X2,X3)
| ~ iext(uri_owl_equivalentProperty,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1816]) ).
fof(f1821,plain,
! [X0,X1] :
( ~ iext(X1,sK124_skl(X1,X0),sK125_skl(X1,X0))
| ~ iext(X0,sK124_skl(X1,X0),sK125_skl(X1,X0))
| ~ ip(X1)
| ~ ip(X0)
| iext(uri_owl_equivalentProperty,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1816]) ).
fof(f1822,plain,
! [X0,X1] :
( iext(X1,sK124_skl(X1,X0),sK125_skl(X1,X0))
| iext(X0,sK124_skl(X1,X0),sK125_skl(X1,X0))
| ~ ip(X1)
| ~ ip(X0)
| iext(uri_owl_equivalentProperty,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1816]) ).
fof(f1832,plain,
! [X,Y] :
( ( X != Y
| iext(uri_owl_sameAs,X,Y) )
& ( X = Y
| ~ iext(uri_owl_sameAs,X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f354]) ).
fof(f1833,plain,
( ! [X,Y] :
( X != Y
| iext(uri_owl_sameAs,X,Y) )
& ! [X,Y] :
( X = Y
| ~ iext(uri_owl_sameAs,X,Y) ) ),
inference(miniscoping,[status(thm)],[f1832]) ).
fof(f1835,plain,
! [X0,X1] :
( X0 != X1
| iext(uri_owl_sameAs,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1833]) ).
fof(f1864,plain,
( iext(uri_owl_members,sK132_skl,uri_rdf_nil)
& icext(uri_owl_AllDifferent,sK132_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK132_skl]),skolemize(Z,sK132_skl)],[f363]) ).
fof(f1865,plain,
icext(uri_owl_AllDifferent,sK132_skl),
inference(cnf_transformation,[status(thm)],[f1864]) ).
fof(f1892,plain,
( iext(uri_owl_members,sK136_skl,uri_rdf_nil)
& icext(uri_owl_AllDisjointClasses,sK136_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK136_skl]),skolemize(Z,sK136_skl)],[f371]) ).
fof(f1893,plain,
icext(uri_owl_AllDisjointClasses,sK136_skl),
inference(cnf_transformation,[status(thm)],[f1892]) ).
fof(f1926,plain,
( iext(uri_owl_members,sK144_skl,uri_rdf_nil)
& icext(uri_owl_AllDisjointProperties,sK144_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK144_skl]),skolemize(Z,sK144_skl)],[f379]) ).
fof(f1927,plain,
icext(uri_owl_AllDisjointProperties,sK144_skl),
inference(cnf_transformation,[status(thm)],[f1926]) ).
fof(f1999,plain,
! [P1,P2] :
( ( ? [X,Y] :
( ( iext(P2,Y,X)
| iext(P1,X,Y) )
& ( ~ iext(P2,Y,X)
| ~ iext(P1,X,Y) ) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_owl_inverseOf,P1,P2) )
& ( ( ! [X,Y] :
( ( ~ iext(P2,Y,X)
| iext(P1,X,Y) )
& ( iext(P2,Y,X)
| ~ iext(P1,X,Y) ) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_owl_inverseOf,P1,P2) ) ),
inference(NNF_transformation,[status(thm)],[f391]) ).
fof(f2000,plain,
( ! [P1,P2] :
( ? [X,Y] :
( ( iext(P2,Y,X)
| iext(P1,X,Y) )
& ( ~ iext(P2,Y,X)
| ~ iext(P1,X,Y) ) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_owl_inverseOf,P1,P2) )
& ! [P1,P2] :
( ( ! [X,Y] :
( ~ iext(P2,Y,X)
| iext(P1,X,Y) )
& ! [X,Y] :
( iext(P2,Y,X)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_owl_inverseOf,P1,P2) ) ),
inference(miniscoping,[status(thm)],[f1999]) ).
fof(f2001,plain,
( ! [P1,P2] :
( ( ( iext(P2,sK167_skl(P2,P1),sK166_skl(P2,P1))
| iext(P1,sK166_skl(P2,P1),sK167_skl(P2,P1)) )
& ( ~ iext(P2,sK167_skl(P2,P1),sK166_skl(P2,P1))
| ~ iext(P1,sK166_skl(P2,P1),sK167_skl(P2,P1)) ) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_owl_inverseOf,P1,P2) )
& ! [P1,P2] :
( ( ! [X,Y] :
( ~ iext(P2,Y,X)
| iext(P1,X,Y) )
& ! [X,Y] :
( iext(P2,Y,X)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_owl_inverseOf,P1,P2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK166_skl,sK167_skl]),skolemize(X,sK166_skl(P2,P1)),skolemize(Y,sK167_skl(P2,P1))],[f2000]) ).
fof(f2004,plain,
! [X0,X1,X2,X3] :
( iext(X1,X3,X2)
| ~ iext(X0,X2,X3)
| ~ iext(uri_owl_inverseOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2001]) ).
fof(f2005,plain,
! [X0,X1,X2,X3] :
( ~ iext(X1,X3,X2)
| iext(X0,X2,X3)
| ~ iext(uri_owl_inverseOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2001]) ).
fof(f2006,plain,
! [X0,X1] :
( ~ iext(X1,sK167_skl(X1,X0),sK166_skl(X1,X0))
| ~ iext(X0,sK166_skl(X1,X0),sK167_skl(X1,X0))
| ~ ip(X1)
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2001]) ).
fof(f2007,plain,
! [X0,X1] :
( iext(X1,sK167_skl(X1,X0),sK166_skl(X1,X0))
| iext(X0,sK166_skl(X1,X0),sK167_skl(X1,X0))
| ~ ip(X1)
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2001]) ).
fof(f2008,plain,
! [P] :
( icext(uri_owl_AsymmetricProperty,P)
<=> ( ! [X,Y] :
( ~ iext(P,Y,X)
| ~ iext(P,X,Y) )
& ip(P) ) ),
inference(pre_NNF_transformation,[status(thm)],[f392]) ).
fof(f2009,plain,
! [P] :
( ( ? [X,Y] :
( iext(P,Y,X)
& iext(P,X,Y) )
| ~ ip(P)
| icext(uri_owl_AsymmetricProperty,P) )
& ( ( ! [X,Y] :
( ~ iext(P,Y,X)
| ~ iext(P,X,Y) )
& ip(P) )
| ~ icext(uri_owl_AsymmetricProperty,P) ) ),
inference(NNF_transformation,[status(thm)],[f2008]) ).
fof(f2010,plain,
( ! [P] :
( ? [X,Y] :
( iext(P,Y,X)
& iext(P,X,Y) )
| ~ ip(P)
| icext(uri_owl_AsymmetricProperty,P) )
& ! [P] :
( ( ! [X,Y] :
( ~ iext(P,Y,X)
| ~ iext(P,X,Y) )
& ip(P) )
| ~ icext(uri_owl_AsymmetricProperty,P) ) ),
inference(miniscoping,[status(thm)],[f2009]) ).
fof(f2011,plain,
( ! [P] :
( ( iext(P,sK169_skl(P),sK168_skl(P))
& iext(P,sK168_skl(P),sK169_skl(P)) )
| ~ ip(P)
| icext(uri_owl_AsymmetricProperty,P) )
& ! [P] :
( ( ! [X,Y] :
( ~ iext(P,Y,X)
| ~ iext(P,X,Y) )
& ip(P) )
| ~ icext(uri_owl_AsymmetricProperty,P) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK168_skl,sK169_skl]),skolemize(X,sK168_skl(P)),skolemize(Y,sK169_skl(P))],[f2010]) ).
fof(f2014,plain,
! [X0] :
( iext(X0,sK168_skl(X0),sK169_skl(X0))
| ~ ip(X0)
| icext(uri_owl_AsymmetricProperty,X0) ),
inference(cnf_transformation,[status(thm)],[f2011]) ).
fof(f2016,plain,
! [P] :
( icext(uri_owl_FunctionalProperty,P)
<=> ( ! [X,Y1,Y2] :
( Y1 = Y2
| ~ iext(P,X,Y2)
| ~ iext(P,X,Y1) )
& ip(P) ) ),
inference(pre_NNF_transformation,[status(thm)],[f393]) ).
fof(f2017,plain,
! [P] :
( ( ? [X,Y1,Y2] :
( Y1 != Y2
& iext(P,X,Y2)
& iext(P,X,Y1) )
| ~ ip(P)
| icext(uri_owl_FunctionalProperty,P) )
& ( ( ! [X,Y1,Y2] :
( Y1 = Y2
| ~ iext(P,X,Y2)
| ~ iext(P,X,Y1) )
& ip(P) )
| ~ icext(uri_owl_FunctionalProperty,P) ) ),
inference(NNF_transformation,[status(thm)],[f2016]) ).
fof(f2018,plain,
( ! [P] :
( ? [Y1,Y2] :
( Y1 != Y2
& ? [X] :
( iext(P,X,Y2)
& iext(P,X,Y1) ) )
| ~ ip(P)
| icext(uri_owl_FunctionalProperty,P) )
& ! [P] :
( ( ! [Y1,Y2] :
( Y1 = Y2
| ! [X] :
( ~ iext(P,X,Y2)
| ~ iext(P,X,Y1) ) )
& ip(P) )
| ~ icext(uri_owl_FunctionalProperty,P) ) ),
inference(miniscoping,[status(thm)],[f2017]) ).
fof(f2019,plain,
( ! [P] :
( ( sK170_skl(P) != sK171_skl(P)
& iext(P,sK172_skl(P),sK171_skl(P))
& iext(P,sK172_skl(P),sK170_skl(P)) )
| ~ ip(P)
| icext(uri_owl_FunctionalProperty,P) )
& ! [P] :
( ( ! [Y1,Y2] :
( Y1 = Y2
| ! [X] :
( ~ iext(P,X,Y2)
| ~ iext(P,X,Y1) ) )
& ip(P) )
| ~ icext(uri_owl_FunctionalProperty,P) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK170_skl,sK171_skl,sK172_skl]),skolemize(Y1,sK170_skl(P)),skolemize(Y2,sK171_skl(P)),skolemize(X,sK172_skl(P))],[f2018]) ).
fof(f2022,plain,
! [X0] :
( iext(X0,sK172_skl(X0),sK170_skl(X0))
| ~ ip(X0)
| icext(uri_owl_FunctionalProperty,X0) ),
inference(cnf_transformation,[status(thm)],[f2019]) ).
fof(f2025,plain,
! [P] :
( icext(uri_owl_InverseFunctionalProperty,P)
<=> ( ! [X1,X2,Y] :
( X1 = X2
| ~ iext(P,X2,Y)
| ~ iext(P,X1,Y) )
& ip(P) ) ),
inference(pre_NNF_transformation,[status(thm)],[f394]) ).
fof(f2026,plain,
! [P] :
( ( ? [X1,X2,Y] :
( X1 != X2
& iext(P,X2,Y)
& iext(P,X1,Y) )
| ~ ip(P)
| icext(uri_owl_InverseFunctionalProperty,P) )
& ( ( ! [X1,X2,Y] :
( X1 = X2
| ~ iext(P,X2,Y)
| ~ iext(P,X1,Y) )
& ip(P) )
| ~ icext(uri_owl_InverseFunctionalProperty,P) ) ),
inference(NNF_transformation,[status(thm)],[f2025]) ).
fof(f2027,plain,
( ! [P] :
( ? [X1,X2] :
( X1 != X2
& ? [Y] :
( iext(P,X2,Y)
& iext(P,X1,Y) ) )
| ~ ip(P)
| icext(uri_owl_InverseFunctionalProperty,P) )
& ! [P] :
( ( ! [X1,X2] :
( X1 = X2
| ! [Y] :
( ~ iext(P,X2,Y)
| ~ iext(P,X1,Y) ) )
& ip(P) )
| ~ icext(uri_owl_InverseFunctionalProperty,P) ) ),
inference(miniscoping,[status(thm)],[f2026]) ).
fof(f2028,plain,
( ! [P] :
( ( sK173_skl(P) != sK174_skl(P)
& iext(P,sK174_skl(P),sK175_skl(P))
& iext(P,sK173_skl(P),sK175_skl(P)) )
| ~ ip(P)
| icext(uri_owl_InverseFunctionalProperty,P) )
& ! [P] :
( ( ! [X1,X2] :
( X1 = X2
| ! [Y] :
( ~ iext(P,X2,Y)
| ~ iext(P,X1,Y) ) )
& ip(P) )
| ~ icext(uri_owl_InverseFunctionalProperty,P) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK173_skl,sK174_skl,sK175_skl]),skolemize(X1,sK173_skl(P)),skolemize(X2,sK174_skl(P)),skolemize(Y,sK175_skl(P))],[f2027]) ).
fof(f2031,plain,
! [X0] :
( iext(X0,sK173_skl(X0),sK175_skl(X0))
| ~ ip(X0)
| icext(uri_owl_InverseFunctionalProperty,X0) ),
inference(cnf_transformation,[status(thm)],[f2028]) ).
fof(f2040,plain,
! [P] :
( ( ? [X] : ~ iext(P,X,X)
| ~ ip(P)
| icext(uri_owl_ReflexiveProperty,P) )
& ( ( ! [X] : iext(P,X,X)
& ip(P) )
| ~ icext(uri_owl_ReflexiveProperty,P) ) ),
inference(NNF_transformation,[status(thm)],[f396]) ).
fof(f2041,plain,
( ! [P] :
( ? [X] : ~ iext(P,X,X)
| ~ ip(P)
| icext(uri_owl_ReflexiveProperty,P) )
& ! [P] :
( ( ! [X] : iext(P,X,X)
& ip(P) )
| ~ icext(uri_owl_ReflexiveProperty,P) ) ),
inference(miniscoping,[status(thm)],[f2040]) ).
fof(f2042,plain,
( ! [P] :
( ~ iext(P,sK177_skl(P),sK177_skl(P))
| ~ ip(P)
| icext(uri_owl_ReflexiveProperty,P) )
& ! [P] :
( ( ! [X] : iext(P,X,X)
& ip(P) )
| ~ icext(uri_owl_ReflexiveProperty,P) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK177_skl]),skolemize(X,sK177_skl(P))],[f2041]) ).
fof(f2045,plain,
! [X0] :
( ~ iext(X0,sK177_skl(X0),sK177_skl(X0))
| ~ ip(X0)
| icext(uri_owl_ReflexiveProperty,X0) ),
inference(cnf_transformation,[status(thm)],[f2042]) ).
fof(f2046,plain,
! [P] :
( icext(uri_owl_SymmetricProperty,P)
<=> ( ! [X,Y] :
( iext(P,Y,X)
| ~ iext(P,X,Y) )
& ip(P) ) ),
inference(pre_NNF_transformation,[status(thm)],[f397]) ).
fof(f2047,plain,
! [P] :
( ( ? [X,Y] :
( ~ iext(P,Y,X)
& iext(P,X,Y) )
| ~ ip(P)
| icext(uri_owl_SymmetricProperty,P) )
& ( ( ! [X,Y] :
( iext(P,Y,X)
| ~ iext(P,X,Y) )
& ip(P) )
| ~ icext(uri_owl_SymmetricProperty,P) ) ),
inference(NNF_transformation,[status(thm)],[f2046]) ).
fof(f2048,plain,
( ! [P] :
( ? [X,Y] :
( ~ iext(P,Y,X)
& iext(P,X,Y) )
| ~ ip(P)
| icext(uri_owl_SymmetricProperty,P) )
& ! [P] :
( ( ! [X,Y] :
( iext(P,Y,X)
| ~ iext(P,X,Y) )
& ip(P) )
| ~ icext(uri_owl_SymmetricProperty,P) ) ),
inference(miniscoping,[status(thm)],[f2047]) ).
fof(f2049,plain,
( ! [P] :
( ( ~ iext(P,sK179_skl(P),sK178_skl(P))
& iext(P,sK178_skl(P),sK179_skl(P)) )
| ~ ip(P)
| icext(uri_owl_SymmetricProperty,P) )
& ! [P] :
( ( ! [X,Y] :
( iext(P,Y,X)
| ~ iext(P,X,Y) )
& ip(P) )
| ~ icext(uri_owl_SymmetricProperty,P) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK178_skl,sK179_skl]),skolemize(X,sK178_skl(P)),skolemize(Y,sK179_skl(P))],[f2048]) ).
fof(f2052,plain,
! [X0] :
( iext(X0,sK178_skl(X0),sK179_skl(X0))
| ~ ip(X0)
| icext(uri_owl_SymmetricProperty,X0) ),
inference(cnf_transformation,[status(thm)],[f2049]) ).
fof(f2054,plain,
! [P] :
( icext(uri_owl_TransitiveProperty,P)
<=> ( ! [X,Y,Z] :
( iext(P,X,Z)
| ~ iext(P,Y,Z)
| ~ iext(P,X,Y) )
& ip(P) ) ),
inference(pre_NNF_transformation,[status(thm)],[f398]) ).
fof(f2055,plain,
! [P] :
( ( ? [X,Y,Z] :
( ~ iext(P,X,Z)
& iext(P,Y,Z)
& iext(P,X,Y) )
| ~ ip(P)
| icext(uri_owl_TransitiveProperty,P) )
& ( ( ! [X,Y,Z] :
( iext(P,X,Z)
| ~ iext(P,Y,Z)
| ~ iext(P,X,Y) )
& ip(P) )
| ~ icext(uri_owl_TransitiveProperty,P) ) ),
inference(NNF_transformation,[status(thm)],[f2054]) ).
fof(f2056,plain,
( ! [P] :
( ? [X,Z] :
( ~ iext(P,X,Z)
& ? [Y] :
( iext(P,Y,Z)
& iext(P,X,Y) ) )
| ~ ip(P)
| icext(uri_owl_TransitiveProperty,P) )
& ! [P] :
( ( ! [X,Z] :
( iext(P,X,Z)
| ! [Y] :
( ~ iext(P,Y,Z)
| ~ iext(P,X,Y) ) )
& ip(P) )
| ~ icext(uri_owl_TransitiveProperty,P) ) ),
inference(miniscoping,[status(thm)],[f2055]) ).
fof(f2057,plain,
( ! [P] :
( ( ~ iext(P,sK180_skl(P),sK181_skl(P))
& iext(P,sK182_skl(P),sK181_skl(P))
& iext(P,sK180_skl(P),sK182_skl(P)) )
| ~ ip(P)
| icext(uri_owl_TransitiveProperty,P) )
& ! [P] :
( ( ! [X,Z] :
( iext(P,X,Z)
| ! [Y] :
( ~ iext(P,Y,Z)
| ~ iext(P,X,Y) ) )
& ip(P) )
| ~ icext(uri_owl_TransitiveProperty,P) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK180_skl,sK181_skl,sK182_skl]),skolemize(X,sK180_skl(P)),skolemize(Z,sK181_skl(P)),skolemize(Y,sK182_skl(P))],[f2056]) ).
fof(f2060,plain,
! [X0] :
( iext(X0,sK180_skl(X0),sK182_skl(X0))
| ~ ip(X0)
| icext(uri_owl_TransitiveProperty,X0) ),
inference(cnf_transformation,[status(thm)],[f2057]) ).
fof(f2232,plain,
idc(uri_rdf_XMLLiteral),
inference(cnf_transformation,[status(thm)],[f472]) ).
fof(f2404,plain,
iodp(uri_xsd_pattern),
inference(cnf_transformation,[status(thm)],[f558]) ).
fof(f2405,plain,
~ iext(uri_owl_equivalentProperty,uri_ex_p3,uri_ex_p1),
inference(cnf_transformation,[status(thm)],[f560]) ).
fof(f2406,plain,
iext(uri_owl_inverseOf,uri_ex_p3,uri_ex_p2),
inference(cnf_transformation,[status(thm)],[f561]) ).
fof(f2407,plain,
iext(uri_owl_inverseOf,uri_ex_p2,uri_ex_p1),
inference(cnf_transformation,[status(thm)],[f561]) ).
fof(f2518,plain,
! [X0] : ~ iext(uri_owl_differentFrom,X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f1751]) ).
fof(f2519,plain,
! [X0] : iext(uri_owl_sameAs,X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f1835]) ).
fof(f2533,plain,
! [X0,X1,X2] :
( ~ iext(X0,X1,X2)
| ~ iext(uri_rdfs_domain,X0,uri_owl_Nothing) ),
inference(resolution,[status(thm)],[f627,f823]) ).
fof(f2534,plain,
! [X0] : icext(uri_rdfs_Resource,X0),
inference(forward_subsumption_resolution,[status(thm)],[f635,f565]) ).
fof(f2537,plain,
! [X0,X1] :
( ~ icext(X0,X1)
| ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing) ),
inference(resolution,[status(thm)],[f657,f823]) ).
fof(f2543,plain,
! [X0] : icext(uri_owl_Thing,X0),
inference(forward_subsumption_resolution,[status(thm)],[f862,f565]) ).
fof(f2582,plain,
! [X0,X1] :
( ~ lv(X1)
| iext(uri_owl_topDataProperty,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1062,f565]) ).
fof(f2584,plain,
! [X0,X1] :
( ~ ir(X1)
| iext(uri_owl_topObjectProperty,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1068,f565]) ).
fof(f2677,plain,
! [X0,X1] :
( icext(X0,X1)
| ~ iext(uri_owl_intersectionOf,X0,uri_rdf_nil) ),
inference(forward_subsumption_resolution,[status(thm)],[f1104,f565]) ).
fof(f2678,plain,
! [X0] :
( ~ icext(X0,sK1_skl(X0))
| ~ ic(X0)
| iext(uri_owl_intersectionOf,X0,uri_rdf_nil) ),
inference(forward_subsumption_resolution,[status(thm)],[f1105,f565]) ).
fof(f2679,plain,
! [X0,X1] :
( icext(X0,X1)
| ~ icext(X0,sK1_skl(X0))
| ~ ic(X0) ),
inference(resolution,[status(thm)],[f2678,f2677]) ).
fof(f2786,plain,
! [X0,X1] :
( ~ icext(X0,X1)
| icext(X0,sK5_skl(X0))
| ~ ic(X0) ),
inference(resolution,[status(thm)],[f1158,f1157]) ).
fof(f2883,plain,
! [X0] :
( ~ ic(uri_owl_Nothing)
| ~ icext(uri_owl_Nothing,X0) ),
inference(resolution,[status(thm)],[f2537,f660]) ).
fof(f2884,definition,
! [X0] :
( sQ1_spl
<=> ~ icext(uri_owl_Nothing,X0) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f2887,definition,
( sQ2_spl
<=> ic(uri_owl_Nothing) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f2889,plain,
( sQ2_spl
| ~ ic(uri_owl_Nothing) ),
inference(component_clause,[status(thm)],[f2887]) ).
fof(f2890,plain,
( ~ sQ2_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f2883,f2884,f2887]) ).
fof(f2935,plain,
! [X0,X1] :
( ~ icext(X0,X1)
| icext(X0,sK9_skl(X0))
| ~ ic(X0) ),
inference(resolution,[status(thm)],[f1210,f1209]) ).
fof(f2976,plain,
! [X0] :
( icext(uri_owl_Thing,X0)
| ~ icext(uri_owl_Thing,sK1_skl(uri_owl_Thing)) ),
inference(resolution,[status(thm)],[f2679,f863]) ).
fof(f2979,plain,
! [X0] :
( icext(uri_rdfs_Resource,X0)
| ~ icext(uri_rdfs_Resource,sK1_skl(uri_rdfs_Resource)) ),
inference(resolution,[status(thm)],[f2679,f852]) ).
fof(f3047,definition,
( sQ5_spl
<=> icext(uri_owl_Thing,sK1_skl(uri_owl_Thing)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f3049,plain,
( sQ5_spl
| ~ icext(uri_owl_Thing,sK1_skl(uri_owl_Thing)) ),
inference(component_clause,[status(thm)],[f3047]) ).
fof(f3050,definition,
! [X0] :
( sQ6_spl
<=> icext(uri_owl_Thing,X0) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f3053,plain,
( sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f2976,f3047,f3050]) ).
fof(f3068,definition,
( sQ11_spl
<=> icext(uri_rdfs_Resource,sK1_skl(uri_rdfs_Resource)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f3070,plain,
( sQ11_spl
| ~ icext(uri_rdfs_Resource,sK1_skl(uri_rdfs_Resource)) ),
inference(component_clause,[status(thm)],[f3068]) ).
fof(f3071,definition,
! [X0] :
( sQ12_spl
<=> icext(uri_rdfs_Resource,X0) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f3074,plain,
( sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f2979,f3068,f3071]) ).
fof(f3250,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3070,f2534]) ).
fof(f3251,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f3250]) ).
fof(f3252,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3049,f2543]) ).
fof(f3253,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f3252]) ).
fof(f4123,plain,
! [X0] :
( ~ icext(uri_owl_AllDifferent,X0)
| icext(uri_owl_AllDifferent,sK5_skl(uri_owl_AllDifferent)) ),
inference(resolution,[status(thm)],[f2786,f751]) ).
fof(f4124,plain,
! [X0] :
( ~ icext(uri_owl_AllDisjointClasses,X0)
| icext(uri_owl_AllDisjointClasses,sK5_skl(uri_owl_AllDisjointClasses)) ),
inference(resolution,[status(thm)],[f2786,f754]) ).
fof(f4125,plain,
! [X0] :
( ~ icext(uri_owl_AllDisjointProperties,X0)
| icext(uri_owl_AllDisjointProperties,sK5_skl(uri_owl_AllDisjointProperties)) ),
inference(resolution,[status(thm)],[f2786,f757]) ).
fof(f4127,plain,
! [X0] :
( ~ icext(uri_owl_AnnotationProperty,X0)
| icext(uri_owl_AnnotationProperty,sK5_skl(uri_owl_AnnotationProperty)) ),
inference(resolution,[status(thm)],[f2786,f765]) ).
fof(f4128,plain,
! [X0] :
( ~ icext(uri_owl_AsymmetricProperty,X0)
| icext(uri_owl_AsymmetricProperty,sK5_skl(uri_owl_AsymmetricProperty)) ),
inference(resolution,[status(thm)],[f2786,f768]) ).
fof(f4130,plain,
! [X0] :
( ~ icext(uri_owl_Class,X0)
| icext(uri_owl_Class,sK5_skl(uri_owl_Class)) ),
inference(resolution,[status(thm)],[f2786,f776]) ).
fof(f4131,plain,
! [X0] :
( ~ icext(uri_rdfs_Class,X0)
| icext(uri_rdfs_Class,sK5_skl(uri_rdfs_Class)) ),
inference(resolution,[status(thm)],[f2786,f781]) ).
fof(f4132,plain,
! [X0] :
( ~ icext(uri_owl_DataRange,X0)
| icext(uri_owl_DataRange,sK5_skl(uri_owl_DataRange)) ),
inference(resolution,[status(thm)],[f2786,f786]) ).
fof(f4133,plain,
! [X0] :
( ~ icext(uri_rdfs_Datatype,X0)
| icext(uri_rdfs_Datatype,sK5_skl(uri_rdfs_Datatype)) ),
inference(resolution,[status(thm)],[f2786,f791]) ).
fof(f4134,plain,
! [X0] :
( ~ icext(uri_owl_DatatypeProperty,X0)
| icext(uri_owl_DatatypeProperty,sK5_skl(uri_owl_DatatypeProperty)) ),
inference(resolution,[status(thm)],[f2786,f796]) ).
fof(f4137,plain,
! [X0] :
( ~ icext(uri_owl_FunctionalProperty,X0)
| icext(uri_owl_FunctionalProperty,sK5_skl(uri_owl_FunctionalProperty)) ),
inference(resolution,[status(thm)],[f2786,f805]) ).
fof(f4138,plain,
! [X0] :
( ~ icext(uri_owl_InverseFunctionalProperty,X0)
| icext(uri_owl_InverseFunctionalProperty,sK5_skl(uri_owl_InverseFunctionalProperty)) ),
inference(resolution,[status(thm)],[f2786,f808]) ).
fof(f4143,plain,
! [X0] :
( ~ icext(uri_owl_ObjectProperty,X0)
| icext(uri_owl_ObjectProperty,sK5_skl(uri_owl_ObjectProperty)) ),
inference(resolution,[status(thm)],[f2786,f829]) ).
fof(f4145,plain,
! [X0] :
( ~ icext(uri_owl_OntologyProperty,X0)
| icext(uri_owl_OntologyProperty,sK5_skl(uri_owl_OntologyProperty)) ),
inference(resolution,[status(thm)],[f2786,f839]) ).
fof(f4146,plain,
! [X0] :
( ~ icext(uri_rdf_Property,X0)
| icext(uri_rdf_Property,sK5_skl(uri_rdf_Property)) ),
inference(resolution,[status(thm)],[f2786,f844]) ).
fof(f4147,plain,
! [X0] :
( ~ icext(uri_owl_ReflexiveProperty,X0)
| icext(uri_owl_ReflexiveProperty,sK5_skl(uri_owl_ReflexiveProperty)) ),
inference(resolution,[status(thm)],[f2786,f847]) ).
fof(f4148,plain,
! [X0] :
( ~ icext(uri_rdfs_Resource,X0)
| icext(uri_rdfs_Resource,sK5_skl(uri_rdfs_Resource)) ),
inference(resolution,[status(thm)],[f2786,f852]) ).
fof(f4150,plain,
! [X0] :
( ~ icext(uri_owl_SymmetricProperty,X0)
| icext(uri_owl_SymmetricProperty,sK5_skl(uri_owl_SymmetricProperty)) ),
inference(resolution,[status(thm)],[f2786,f858]) ).
fof(f4151,plain,
! [X0] :
( ~ icext(uri_owl_Thing,X0)
| icext(uri_owl_Thing,sK5_skl(uri_owl_Thing)) ),
inference(resolution,[status(thm)],[f2786,f863]) ).
fof(f4152,plain,
! [X0] :
( ~ icext(uri_owl_TransitiveProperty,X0)
| icext(uri_owl_TransitiveProperty,sK5_skl(uri_owl_TransitiveProperty)) ),
inference(resolution,[status(thm)],[f2786,f866]) ).
fof(f4162,definition,
( sQ65_spl
<=> icext(uri_owl_AllDifferent,sK5_skl(uri_owl_AllDifferent)) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f4165,definition,
! [X0] :
( sQ66_spl
<=> ~ icext(uri_owl_AllDifferent,X0) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f4166,plain,
! [X0] :
( ~ sQ66_spl
| ~ icext(uri_owl_AllDifferent,X0) ),
inference(component_clause,[status(thm)],[f4165]) ).
fof(f4168,plain,
( sQ66_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f4123,f4162,f4165]) ).
fof(f4169,definition,
( sQ67_spl
<=> icext(uri_owl_AllDisjointClasses,sK5_skl(uri_owl_AllDisjointClasses)) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f4172,definition,
! [X0] :
( sQ68_spl
<=> ~ icext(uri_owl_AllDisjointClasses,X0) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f4173,plain,
! [X0] :
( ~ sQ68_spl
| ~ icext(uri_owl_AllDisjointClasses,X0) ),
inference(component_clause,[status(thm)],[f4172]) ).
fof(f4175,plain,
( sQ68_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f4124,f4169,f4172]) ).
fof(f4176,definition,
( sQ69_spl
<=> icext(uri_owl_AllDisjointProperties,sK5_skl(uri_owl_AllDisjointProperties)) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f4179,definition,
! [X0] :
( sQ70_spl
<=> ~ icext(uri_owl_AllDisjointProperties,X0) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f4180,plain,
! [X0] :
( ~ sQ70_spl
| ~ icext(uri_owl_AllDisjointProperties,X0) ),
inference(component_clause,[status(thm)],[f4179]) ).
fof(f4182,plain,
( sQ70_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f4125,f4176,f4179]) ).
fof(f4190,definition,
( sQ73_spl
<=> icext(uri_owl_AnnotationProperty,sK5_skl(uri_owl_AnnotationProperty)) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f4193,definition,
! [X0] :
( sQ74_spl
<=> ~ icext(uri_owl_AnnotationProperty,X0) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f4194,plain,
! [X0] :
( ~ sQ74_spl
| ~ icext(uri_owl_AnnotationProperty,X0) ),
inference(component_clause,[status(thm)],[f4193]) ).
fof(f4196,plain,
( sQ74_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f4127,f4190,f4193]) ).
fof(f4197,definition,
( sQ75_spl
<=> icext(uri_owl_AsymmetricProperty,sK5_skl(uri_owl_AsymmetricProperty)) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f4200,definition,
! [X0] :
( sQ76_spl
<=> ~ icext(uri_owl_AsymmetricProperty,X0) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f4201,plain,
! [X0] :
( ~ sQ76_spl
| ~ icext(uri_owl_AsymmetricProperty,X0) ),
inference(component_clause,[status(thm)],[f4200]) ).
fof(f4203,plain,
( sQ76_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f4128,f4197,f4200]) ).
fof(f4211,definition,
( sQ79_spl
<=> icext(uri_owl_Class,sK5_skl(uri_owl_Class)) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f4214,definition,
! [X0] :
( sQ80_spl
<=> ~ icext(uri_owl_Class,X0) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f4215,plain,
! [X0] :
( ~ sQ80_spl
| ~ icext(uri_owl_Class,X0) ),
inference(component_clause,[status(thm)],[f4214]) ).
fof(f4217,plain,
( sQ80_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f4130,f4211,f4214]) ).
fof(f4218,definition,
( sQ81_spl
<=> icext(uri_rdfs_Class,sK5_skl(uri_rdfs_Class)) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f4221,definition,
! [X0] :
( sQ82_spl
<=> ~ icext(uri_rdfs_Class,X0) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f4222,plain,
! [X0] :
( ~ sQ82_spl
| ~ icext(uri_rdfs_Class,X0) ),
inference(component_clause,[status(thm)],[f4221]) ).
fof(f4224,plain,
( sQ82_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f4131,f4218,f4221]) ).
fof(f4225,definition,
( sQ83_spl
<=> icext(uri_owl_DataRange,sK5_skl(uri_owl_DataRange)) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f4228,definition,
! [X0] :
( sQ84_spl
<=> ~ icext(uri_owl_DataRange,X0) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f4229,plain,
! [X0] :
( ~ sQ84_spl
| ~ icext(uri_owl_DataRange,X0) ),
inference(component_clause,[status(thm)],[f4228]) ).
fof(f4231,plain,
( sQ84_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f4132,f4225,f4228]) ).
fof(f4232,definition,
( sQ85_spl
<=> icext(uri_rdfs_Datatype,sK5_skl(uri_rdfs_Datatype)) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f4235,definition,
! [X0] :
( sQ86_spl
<=> ~ icext(uri_rdfs_Datatype,X0) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f4236,plain,
! [X0] :
( ~ sQ86_spl
| ~ icext(uri_rdfs_Datatype,X0) ),
inference(component_clause,[status(thm)],[f4235]) ).
fof(f4238,plain,
( sQ86_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f4133,f4232,f4235]) ).
fof(f4239,definition,
( sQ87_spl
<=> icext(uri_owl_DatatypeProperty,sK5_skl(uri_owl_DatatypeProperty)) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f4242,definition,
! [X0] :
( sQ88_spl
<=> ~ icext(uri_owl_DatatypeProperty,X0) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f4243,plain,
! [X0] :
( ~ sQ88_spl
| ~ icext(uri_owl_DatatypeProperty,X0) ),
inference(component_clause,[status(thm)],[f4242]) ).
fof(f4245,plain,
( sQ88_spl
| sQ87_spl ),
inference(split_clause,[status(thm)],[f4134,f4239,f4242]) ).
fof(f4260,definition,
( sQ93_spl
<=> icext(uri_owl_FunctionalProperty,sK5_skl(uri_owl_FunctionalProperty)) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f4263,definition,
! [X0] :
( sQ94_spl
<=> ~ icext(uri_owl_FunctionalProperty,X0) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f4264,plain,
! [X0] :
( ~ sQ94_spl
| ~ icext(uri_owl_FunctionalProperty,X0) ),
inference(component_clause,[status(thm)],[f4263]) ).
fof(f4266,plain,
( sQ94_spl
| sQ93_spl ),
inference(split_clause,[status(thm)],[f4137,f4260,f4263]) ).
fof(f4267,definition,
( sQ95_spl
<=> icext(uri_owl_InverseFunctionalProperty,sK5_skl(uri_owl_InverseFunctionalProperty)) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f4270,definition,
! [X0] :
( sQ96_spl
<=> ~ icext(uri_owl_InverseFunctionalProperty,X0) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f4271,plain,
! [X0] :
( ~ sQ96_spl
| ~ icext(uri_owl_InverseFunctionalProperty,X0) ),
inference(component_clause,[status(thm)],[f4270]) ).
fof(f4273,plain,
( sQ96_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f4138,f4267,f4270]) ).
fof(f4299,definition,
( sQ104_spl
<=> icext(uri_owl_ObjectProperty,sK5_skl(uri_owl_ObjectProperty)) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f4302,definition,
! [X0] :
( sQ105_spl
<=> ~ icext(uri_owl_ObjectProperty,X0) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f4303,plain,
! [X0] :
( ~ sQ105_spl
| ~ icext(uri_owl_ObjectProperty,X0) ),
inference(component_clause,[status(thm)],[f4302]) ).
fof(f4305,plain,
( sQ105_spl
| sQ104_spl ),
inference(split_clause,[status(thm)],[f4143,f4299,f4302]) ).
fof(f4313,definition,
( sQ108_spl
<=> icext(uri_owl_OntologyProperty,sK5_skl(uri_owl_OntologyProperty)) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f4316,definition,
! [X0] :
( sQ109_spl
<=> ~ icext(uri_owl_OntologyProperty,X0) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f4317,plain,
! [X0] :
( ~ sQ109_spl
| ~ icext(uri_owl_OntologyProperty,X0) ),
inference(component_clause,[status(thm)],[f4316]) ).
fof(f4319,plain,
( sQ109_spl
| sQ108_spl ),
inference(split_clause,[status(thm)],[f4145,f4313,f4316]) ).
fof(f4320,definition,
( sQ110_spl
<=> icext(uri_rdf_Property,sK5_skl(uri_rdf_Property)) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f4321,plain,
( ~ sQ110_spl
| icext(uri_rdf_Property,sK5_skl(uri_rdf_Property)) ),
inference(component_clause,[status(thm)],[f4320]) ).
fof(f4323,definition,
! [X0] :
( sQ111_spl
<=> ~ icext(uri_rdf_Property,X0) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f4324,plain,
! [X0] :
( ~ sQ111_spl
| ~ icext(uri_rdf_Property,X0) ),
inference(component_clause,[status(thm)],[f4323]) ).
fof(f4326,plain,
( sQ111_spl
| sQ110_spl ),
inference(split_clause,[status(thm)],[f4146,f4320,f4323]) ).
fof(f4327,definition,
( sQ112_spl
<=> icext(uri_owl_ReflexiveProperty,sK5_skl(uri_owl_ReflexiveProperty)) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f4330,definition,
! [X0] :
( sQ113_spl
<=> ~ icext(uri_owl_ReflexiveProperty,X0) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f4331,plain,
! [X0] :
( ~ sQ113_spl
| ~ icext(uri_owl_ReflexiveProperty,X0) ),
inference(component_clause,[status(thm)],[f4330]) ).
fof(f4333,plain,
( sQ113_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f4147,f4327,f4330]) ).
fof(f4334,definition,
( sQ114_spl
<=> icext(uri_rdfs_Resource,sK5_skl(uri_rdfs_Resource)) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f4337,definition,
! [X0] :
( sQ115_spl
<=> ~ icext(uri_rdfs_Resource,X0) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f4338,plain,
! [X0] :
( ~ sQ115_spl
| ~ icext(uri_rdfs_Resource,X0) ),
inference(component_clause,[status(thm)],[f4337]) ).
fof(f4340,plain,
( sQ115_spl
| sQ114_spl ),
inference(split_clause,[status(thm)],[f4148,f4334,f4337]) ).
fof(f4348,definition,
( sQ118_spl
<=> icext(uri_owl_SymmetricProperty,sK5_skl(uri_owl_SymmetricProperty)) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f4351,definition,
! [X0] :
( sQ119_spl
<=> ~ icext(uri_owl_SymmetricProperty,X0) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f4352,plain,
! [X0] :
( ~ sQ119_spl
| ~ icext(uri_owl_SymmetricProperty,X0) ),
inference(component_clause,[status(thm)],[f4351]) ).
fof(f4354,plain,
( sQ119_spl
| sQ118_spl ),
inference(split_clause,[status(thm)],[f4150,f4348,f4351]) ).
fof(f4355,definition,
( sQ120_spl
<=> icext(uri_owl_Thing,sK5_skl(uri_owl_Thing)) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f4358,definition,
! [X0] :
( sQ121_spl
<=> ~ icext(uri_owl_Thing,X0) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f4359,plain,
! [X0] :
( ~ sQ121_spl
| ~ icext(uri_owl_Thing,X0) ),
inference(component_clause,[status(thm)],[f4358]) ).
fof(f4361,plain,
( sQ121_spl
| sQ120_spl ),
inference(split_clause,[status(thm)],[f4151,f4355,f4358]) ).
fof(f4362,definition,
( sQ122_spl
<=> icext(uri_owl_TransitiveProperty,sK5_skl(uri_owl_TransitiveProperty)) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f4365,definition,
! [X0] :
( sQ123_spl
<=> ~ icext(uri_owl_TransitiveProperty,X0) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f4366,plain,
! [X0] :
( ~ sQ123_spl
| ~ icext(uri_owl_TransitiveProperty,X0) ),
inference(component_clause,[status(thm)],[f4365]) ).
fof(f4368,plain,
( sQ123_spl
| sQ122_spl ),
inference(split_clause,[status(thm)],[f4152,f4362,f4365]) ).
fof(f4370,plain,
! [X0] :
( ~ icext(uri_owl_AllDifferent,X0)
| icext(uri_owl_AllDifferent,sK9_skl(uri_owl_AllDifferent)) ),
inference(resolution,[status(thm)],[f2935,f751]) ).
fof(f4371,plain,
! [X0] :
( ~ icext(uri_owl_AllDisjointClasses,X0)
| icext(uri_owl_AllDisjointClasses,sK9_skl(uri_owl_AllDisjointClasses)) ),
inference(resolution,[status(thm)],[f2935,f754]) ).
fof(f4372,plain,
! [X0] :
( ~ icext(uri_owl_AllDisjointProperties,X0)
| icext(uri_owl_AllDisjointProperties,sK9_skl(uri_owl_AllDisjointProperties)) ),
inference(resolution,[status(thm)],[f2935,f757]) ).
fof(f4374,plain,
! [X0] :
( ~ icext(uri_owl_AnnotationProperty,X0)
| icext(uri_owl_AnnotationProperty,sK9_skl(uri_owl_AnnotationProperty)) ),
inference(resolution,[status(thm)],[f2935,f765]) ).
fof(f4375,plain,
! [X0] :
( ~ icext(uri_owl_AsymmetricProperty,X0)
| icext(uri_owl_AsymmetricProperty,sK9_skl(uri_owl_AsymmetricProperty)) ),
inference(resolution,[status(thm)],[f2935,f768]) ).
fof(f4377,plain,
! [X0] :
( ~ icext(uri_owl_Class,X0)
| icext(uri_owl_Class,sK9_skl(uri_owl_Class)) ),
inference(resolution,[status(thm)],[f2935,f776]) ).
fof(f4378,plain,
! [X0] :
( ~ icext(uri_rdfs_Class,X0)
| icext(uri_rdfs_Class,sK9_skl(uri_rdfs_Class)) ),
inference(resolution,[status(thm)],[f2935,f781]) ).
fof(f4379,plain,
! [X0] :
( ~ icext(uri_owl_DataRange,X0)
| icext(uri_owl_DataRange,sK9_skl(uri_owl_DataRange)) ),
inference(resolution,[status(thm)],[f2935,f786]) ).
fof(f4380,plain,
! [X0] :
( ~ icext(uri_rdfs_Datatype,X0)
| icext(uri_rdfs_Datatype,sK9_skl(uri_rdfs_Datatype)) ),
inference(resolution,[status(thm)],[f2935,f791]) ).
fof(f4381,plain,
! [X0] :
( ~ icext(uri_owl_DatatypeProperty,X0)
| icext(uri_owl_DatatypeProperty,sK9_skl(uri_owl_DatatypeProperty)) ),
inference(resolution,[status(thm)],[f2935,f796]) ).
fof(f4384,plain,
! [X0] :
( ~ icext(uri_owl_FunctionalProperty,X0)
| icext(uri_owl_FunctionalProperty,sK9_skl(uri_owl_FunctionalProperty)) ),
inference(resolution,[status(thm)],[f2935,f805]) ).
fof(f4385,plain,
! [X0] :
( ~ icext(uri_owl_InverseFunctionalProperty,X0)
| icext(uri_owl_InverseFunctionalProperty,sK9_skl(uri_owl_InverseFunctionalProperty)) ),
inference(resolution,[status(thm)],[f2935,f808]) ).
fof(f4390,plain,
! [X0] :
( ~ icext(uri_owl_ObjectProperty,X0)
| icext(uri_owl_ObjectProperty,sK9_skl(uri_owl_ObjectProperty)) ),
inference(resolution,[status(thm)],[f2935,f829]) ).
fof(f4392,plain,
! [X0] :
( ~ icext(uri_owl_OntologyProperty,X0)
| icext(uri_owl_OntologyProperty,sK9_skl(uri_owl_OntologyProperty)) ),
inference(resolution,[status(thm)],[f2935,f839]) ).
fof(f4393,plain,
! [X0] :
( ~ icext(uri_rdf_Property,X0)
| icext(uri_rdf_Property,sK9_skl(uri_rdf_Property)) ),
inference(resolution,[status(thm)],[f2935,f844]) ).
fof(f4394,plain,
! [X0] :
( ~ icext(uri_owl_ReflexiveProperty,X0)
| icext(uri_owl_ReflexiveProperty,sK9_skl(uri_owl_ReflexiveProperty)) ),
inference(resolution,[status(thm)],[f2935,f847]) ).
fof(f4395,plain,
! [X0] :
( ~ icext(uri_rdfs_Resource,X0)
| icext(uri_rdfs_Resource,sK9_skl(uri_rdfs_Resource)) ),
inference(resolution,[status(thm)],[f2935,f852]) ).
fof(f4397,plain,
! [X0] :
( ~ icext(uri_owl_SymmetricProperty,X0)
| icext(uri_owl_SymmetricProperty,sK9_skl(uri_owl_SymmetricProperty)) ),
inference(resolution,[status(thm)],[f2935,f858]) ).
fof(f4398,plain,
! [X0] :
( ~ icext(uri_owl_Thing,X0)
| icext(uri_owl_Thing,sK9_skl(uri_owl_Thing)) ),
inference(resolution,[status(thm)],[f2935,f863]) ).
fof(f4399,plain,
! [X0] :
( ~ icext(uri_owl_TransitiveProperty,X0)
| icext(uri_owl_TransitiveProperty,sK9_skl(uri_owl_TransitiveProperty)) ),
inference(resolution,[status(thm)],[f2935,f866]) ).
fof(f4409,definition,
( sQ124_spl
<=> icext(uri_owl_AllDifferent,sK9_skl(uri_owl_AllDifferent)) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f4412,plain,
( sQ66_spl
| sQ124_spl ),
inference(split_clause,[status(thm)],[f4370,f4409,f4165]) ).
fof(f4413,definition,
( sQ125_spl
<=> icext(uri_owl_AllDisjointClasses,sK9_skl(uri_owl_AllDisjointClasses)) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f4416,plain,
( sQ68_spl
| sQ125_spl ),
inference(split_clause,[status(thm)],[f4371,f4413,f4172]) ).
fof(f4417,definition,
( sQ126_spl
<=> icext(uri_owl_AllDisjointProperties,sK9_skl(uri_owl_AllDisjointProperties)) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f4420,plain,
( sQ70_spl
| sQ126_spl ),
inference(split_clause,[status(thm)],[f4372,f4417,f4179]) ).
fof(f4425,definition,
( sQ128_spl
<=> icext(uri_owl_AnnotationProperty,sK9_skl(uri_owl_AnnotationProperty)) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f4428,plain,
( sQ74_spl
| sQ128_spl ),
inference(split_clause,[status(thm)],[f4374,f4425,f4193]) ).
fof(f4429,definition,
( sQ129_spl
<=> icext(uri_owl_AsymmetricProperty,sK9_skl(uri_owl_AsymmetricProperty)) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f4432,plain,
( sQ76_spl
| sQ129_spl ),
inference(split_clause,[status(thm)],[f4375,f4429,f4200]) ).
fof(f4437,definition,
( sQ131_spl
<=> icext(uri_owl_Class,sK9_skl(uri_owl_Class)) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f4440,plain,
( sQ80_spl
| sQ131_spl ),
inference(split_clause,[status(thm)],[f4377,f4437,f4214]) ).
fof(f4441,definition,
( sQ132_spl
<=> icext(uri_rdfs_Class,sK9_skl(uri_rdfs_Class)) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f4444,plain,
( sQ82_spl
| sQ132_spl ),
inference(split_clause,[status(thm)],[f4378,f4441,f4221]) ).
fof(f4445,definition,
( sQ133_spl
<=> icext(uri_owl_DataRange,sK9_skl(uri_owl_DataRange)) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f4448,plain,
( sQ84_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f4379,f4445,f4228]) ).
fof(f4449,definition,
( sQ134_spl
<=> icext(uri_rdfs_Datatype,sK9_skl(uri_rdfs_Datatype)) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f4452,plain,
( sQ86_spl
| sQ134_spl ),
inference(split_clause,[status(thm)],[f4380,f4449,f4235]) ).
fof(f4453,definition,
( sQ135_spl
<=> icext(uri_owl_DatatypeProperty,sK9_skl(uri_owl_DatatypeProperty)) ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f4456,plain,
( sQ88_spl
| sQ135_spl ),
inference(split_clause,[status(thm)],[f4381,f4453,f4242]) ).
fof(f4465,definition,
( sQ138_spl
<=> icext(uri_owl_FunctionalProperty,sK9_skl(uri_owl_FunctionalProperty)) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f4468,plain,
( sQ94_spl
| sQ138_spl ),
inference(split_clause,[status(thm)],[f4384,f4465,f4263]) ).
fof(f4469,definition,
( sQ139_spl
<=> icext(uri_owl_InverseFunctionalProperty,sK9_skl(uri_owl_InverseFunctionalProperty)) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f4472,plain,
( sQ96_spl
| sQ139_spl ),
inference(split_clause,[status(thm)],[f4385,f4469,f4270]) ).
fof(f4489,definition,
( sQ144_spl
<=> icext(uri_owl_ObjectProperty,sK9_skl(uri_owl_ObjectProperty)) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f4492,plain,
( sQ105_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f4390,f4489,f4302]) ).
fof(f4497,definition,
( sQ146_spl
<=> icext(uri_owl_OntologyProperty,sK9_skl(uri_owl_OntologyProperty)) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f4500,plain,
( sQ109_spl
| sQ146_spl ),
inference(split_clause,[status(thm)],[f4392,f4497,f4316]) ).
fof(f4501,definition,
( sQ147_spl
<=> icext(uri_rdf_Property,sK9_skl(uri_rdf_Property)) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f4504,plain,
( sQ111_spl
| sQ147_spl ),
inference(split_clause,[status(thm)],[f4393,f4501,f4323]) ).
fof(f4505,definition,
( sQ148_spl
<=> icext(uri_owl_ReflexiveProperty,sK9_skl(uri_owl_ReflexiveProperty)) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f4508,plain,
( sQ113_spl
| sQ148_spl ),
inference(split_clause,[status(thm)],[f4394,f4505,f4330]) ).
fof(f4509,definition,
( sQ149_spl
<=> icext(uri_rdfs_Resource,sK9_skl(uri_rdfs_Resource)) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f4512,plain,
( sQ115_spl
| sQ149_spl ),
inference(split_clause,[status(thm)],[f4395,f4509,f4337]) ).
fof(f4517,definition,
( sQ151_spl
<=> icext(uri_owl_SymmetricProperty,sK9_skl(uri_owl_SymmetricProperty)) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f4520,plain,
( sQ119_spl
| sQ151_spl ),
inference(split_clause,[status(thm)],[f4397,f4517,f4351]) ).
fof(f4521,definition,
( sQ152_spl
<=> icext(uri_owl_Thing,sK9_skl(uri_owl_Thing)) ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f4524,plain,
( sQ121_spl
| sQ152_spl ),
inference(split_clause,[status(thm)],[f4398,f4521,f4358]) ).
fof(f4525,definition,
( sQ153_spl
<=> icext(uri_owl_TransitiveProperty,sK9_skl(uri_owl_TransitiveProperty)) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f4528,plain,
( sQ123_spl
| sQ153_spl ),
inference(split_clause,[status(thm)],[f4399,f4525,f4365]) ).
fof(f4529,plain,
( ~ sQ121_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4359,f2543]) ).
fof(f4530,plain,
~ sQ121_spl,
inference(contradiction_clause,[status(thm)],[f4529]) ).
fof(f4531,plain,
( ~ sQ115_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4338,f2534]) ).
fof(f4532,plain,
~ sQ115_spl,
inference(contradiction_clause,[status(thm)],[f4531]) ).
fof(f4562,plain,
! [X0] :
( ~ sQ111_spl
| ~ ip(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f843,f4324]) ).
fof(f4567,plain,
( ~ sQ111_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1085,f4562]) ).
fof(f4634,plain,
~ sQ111_spl,
inference(contradiction_clause,[status(thm)],[f4567]) ).
fof(f4635,plain,
! [X0] :
( ~ sQ109_spl
| ~ ioxp(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f838,f4317]) ).
fof(f4640,plain,
( ~ sQ109_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1081,f4635]) ).
fof(f4646,plain,
~ sQ109_spl,
inference(contradiction_clause,[status(thm)],[f4640]) ).
fof(f4699,plain,
! [X0] :
( ~ sQ88_spl
| ~ iodp(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f795,f4243]) ).
fof(f4710,plain,
( ~ sQ88_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2404,f4699]) ).
fof(f4722,plain,
~ sQ88_spl,
inference(contradiction_clause,[status(thm)],[f4710]) ).
fof(f4723,plain,
! [X0] :
( ~ sQ86_spl
| ~ idc(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f790,f4236]) ).
fof(f4731,plain,
( ~ sQ86_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2232,f4723]) ).
fof(f4773,plain,
~ sQ86_spl,
inference(contradiction_clause,[status(thm)],[f4731]) ).
fof(f4778,plain,
! [X0] :
( ~ sQ82_spl
| ~ ic(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f631,f4222]) ).
fof(f4797,plain,
( ~ sQ82_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f751,f4778]) ).
fof(f4832,plain,
~ sQ82_spl,
inference(contradiction_clause,[status(thm)],[f4797]) ).
fof(f4845,plain,
! [X0] :
( ~ sQ74_spl
| ~ ioap(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f764,f4194]) ).
fof(f4850,plain,
( ~ sQ74_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1077,f4845]) ).
fof(f4860,plain,
~ sQ74_spl,
inference(contradiction_clause,[status(thm)],[f4850]) ).
fof(f4865,plain,
( ~ sQ70_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1927,f4180]) ).
fof(f4870,plain,
~ sQ70_spl,
inference(contradiction_clause,[status(thm)],[f4865]) ).
fof(f4871,plain,
( ~ sQ68_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1893,f4173]) ).
fof(f4876,plain,
~ sQ68_spl,
inference(contradiction_clause,[status(thm)],[f4871]) ).
fof(f4877,plain,
( ~ sQ66_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1865,f4166]) ).
fof(f4884,plain,
~ sQ66_spl,
inference(contradiction_clause,[status(thm)],[f4877]) ).
fof(f4915,plain,
( ~ sQ105_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f870,f4961]) ).
fof(f4961,plain,
! [X0] :
( ~ sQ105_spl
| ~ ip(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f828,f4303]) ).
fof(f4962,plain,
~ sQ105_spl,
inference(contradiction_clause,[status(thm)],[f4915]) ).
fof(f5027,plain,
( ~ sQ84_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f816,f5061]) ).
fof(f5061,plain,
! [X0] :
( ~ sQ84_spl
| ~ idc(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f785,f4229]) ).
fof(f5062,plain,
~ sQ84_spl,
inference(contradiction_clause,[status(thm)],[f5027]) ).
fof(f5093,plain,
( ~ sQ80_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f866,f5124]) ).
fof(f5124,plain,
! [X0] :
( ~ sQ80_spl
| ~ ic(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f775,f4215]) ).
fof(f5125,plain,
~ sQ80_spl,
inference(contradiction_clause,[status(thm)],[f5093]) ).
fof(f5227,plain,
! [X0,X1,X2] :
( ~ iext(X0,X1,X2)
| iext(X0,sK111_skl(uri_owl_Nothing,X0),sK112_skl(uri_owl_Nothing,X0))
| ~ ic(uri_owl_Nothing)
| ~ ip(X0) ),
inference(resolution,[status(thm)],[f1720,f2533]) ).
fof(f5253,definition,
! [X0,X1,X2] :
( sQ161_spl
<=> ( ~ iext(X0,X1,X2)
| iext(X0,sK111_skl(uri_owl_Nothing,X0),sK112_skl(uri_owl_Nothing,X0))
| ~ ip(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f5256,plain,
( ~ sQ2_spl
| sQ161_spl ),
inference(split_clause,[status(thm)],[f5227,f5253,f2887]) ).
fof(f5257,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2889,f824]) ).
fof(f5258,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f5257]) ).
fof(f5309,plain,
! [X0,X1] :
( ~ icext(X0,X1)
| icext(X0,sK115_skl(uri_owl_Nothing,X0))
| ~ ic(uri_owl_Nothing)
| ~ ic(X0) ),
inference(resolution,[status(thm)],[f1738,f2537]) ).
fof(f5326,definition,
! [X0,X1] :
( sQ171_spl
<=> ( ~ icext(X0,X1)
| icext(X0,sK115_skl(uri_owl_Nothing,X0))
| ~ ic(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition]) ).
fof(f5329,plain,
( ~ sQ2_spl
| sQ171_spl ),
inference(split_clause,[status(thm)],[f5309,f5326,f2887]) ).
fof(f5334,plain,
! [X0,X1] :
( ~ icext(X0,X1)
| ~ icext(uri_owl_Nothing,sK115_skl(uri_owl_Nothing,X0))
| ~ ic(uri_owl_Nothing)
| ~ ic(X0) ),
inference(resolution,[status(thm)],[f1739,f2537]) ).
fof(f5351,definition,
! [X0,X1] :
( sQ176_spl
<=> ( ~ icext(X0,X1)
| ~ icext(uri_owl_Nothing,sK115_skl(uri_owl_Nothing,X0))
| ~ ic(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f5354,plain,
( ~ sQ2_spl
| sQ176_spl ),
inference(split_clause,[status(thm)],[f5334,f5351,f2887]) ).
fof(f5533,plain,
ip(uri_ex_p1),
inference(resolution,[status(thm)],[f967,f2407]) ).
fof(f5534,plain,
ip(uri_ex_p2),
inference(resolution,[status(thm)],[f967,f2406]) ).
fof(f5538,plain,
ip(uri_ex_p3),
inference(resolution,[status(thm)],[f966,f2406]) ).
fof(f5590,plain,
! [X0,X1] :
( ~ iext(X1,sK124_skl(X1,X0),sK125_skl(X1,X0))
| ~ iext(X0,sK124_skl(X1,X0),sK125_skl(X1,X0))
| ~ ip(X1)
| iext(uri_owl_equivalentProperty,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1821,f564]) ).
fof(f5593,plain,
( ~ iext(uri_ex_p1,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3))
| ~ iext(uri_ex_p3,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3))
| ~ ip(uri_ex_p1) ),
inference(resolution,[status(thm)],[f5590,f2405]) ).
fof(f5598,plain,
! [X0,X1,X2,X3] :
( ~ iext(X0,X2,X3)
| iext(X1,X2,X3)
| ~ iext(X0,sK124_skl(X0,X1),sK125_skl(X0,X1))
| ~ iext(X1,sK124_skl(X0,X1),sK125_skl(X0,X1))
| ~ ip(X0) ),
inference(resolution,[status(thm)],[f5590,f1820]) ).
fof(f5599,plain,
! [X0,X1,X2,X3] :
( iext(X0,X2,X3)
| ~ iext(X1,X2,X3)
| ~ iext(X0,sK124_skl(X0,X1),sK125_skl(X0,X1))
| ~ iext(X1,sK124_skl(X0,X1),sK125_skl(X0,X1))
| ~ ip(X0) ),
inference(resolution,[status(thm)],[f5590,f1819]) ).
fof(f5600,definition,
( sQ195_spl
<=> ip(uri_ex_p1) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f5602,plain,
( sQ195_spl
| ~ ip(uri_ex_p1) ),
inference(component_clause,[status(thm)],[f5600]) ).
fof(f5603,definition,
( sQ196_spl
<=> iext(uri_ex_p3,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3)) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f5604,plain,
( ~ sQ196_spl
| iext(uri_ex_p3,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3)) ),
inference(component_clause,[status(thm)],[f5603]) ).
fof(f5605,plain,
( sQ196_spl
| ~ iext(uri_ex_p3,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3)) ),
inference(component_clause,[status(thm)],[f5603]) ).
fof(f5606,definition,
( sQ197_spl
<=> iext(uri_ex_p1,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3)) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f5607,plain,
( ~ sQ197_spl
| iext(uri_ex_p1,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3)) ),
inference(component_clause,[status(thm)],[f5606]) ).
fof(f5608,plain,
( sQ197_spl
| ~ iext(uri_ex_p1,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3)) ),
inference(component_clause,[status(thm)],[f5606]) ).
fof(f5609,plain,
( ~ sQ197_spl
| ~ sQ196_spl
| ~ sQ195_spl ),
inference(split_clause,[status(thm)],[f5593,f5600,f5603,f5606]) ).
fof(f5618,plain,
! [X0,X1,X2,X3] :
( ~ iext(X1,X2,X3)
| iext(X0,X2,X3)
| ~ iext(X1,sK124_skl(X1,X0),sK125_skl(X1,X0))
| ~ iext(X0,sK124_skl(X1,X0),sK125_skl(X1,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5598,f564]) ).
fof(f5619,plain,
! [X0,X1,X2,X3] :
( iext(X1,X2,X3)
| ~ iext(X0,X2,X3)
| ~ iext(X1,sK124_skl(X1,X0),sK125_skl(X1,X0))
| ~ iext(X0,sK124_skl(X1,X0),sK125_skl(X1,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5599,f564]) ).
fof(f5626,plain,
! [X0,X1,X2] :
( ~ ir(sK125_skl(uri_owl_topObjectProperty,X0))
| ~ iext(uri_owl_topObjectProperty,X1,X2)
| iext(X0,X1,X2)
| ~ iext(X0,sK124_skl(uri_owl_topObjectProperty,X0),sK125_skl(uri_owl_topObjectProperty,X0)) ),
inference(resolution,[status(thm)],[f5618,f2584]) ).
fof(f5628,plain,
! [X0,X1,X2] :
( sK124_skl(uri_owl_differentFrom,X0) = sK125_skl(uri_owl_differentFrom,X0)
| ~ iext(uri_owl_differentFrom,X1,X2)
| iext(X0,X1,X2)
| ~ iext(X0,sK124_skl(uri_owl_differentFrom,X0),sK125_skl(uri_owl_differentFrom,X0)) ),
inference(resolution,[status(thm)],[f5618,f1752]) ).
fof(f5637,plain,
! [X0,X1,X2] :
( ~ iext(uri_owl_topObjectProperty,X1,X2)
| iext(X0,X1,X2)
| ~ iext(X0,sK124_skl(uri_owl_topObjectProperty,X0),sK125_skl(uri_owl_topObjectProperty,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5626,f565]) ).
fof(f5651,plain,
( iext(uri_ex_p1,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3))
| iext(uri_ex_p3,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3))
| ~ ip(uri_ex_p1)
| ~ ip(uri_ex_p3) ),
inference(resolution,[status(thm)],[f1822,f2405]) ).
fof(f5656,plain,
! [X0,X1,X2,X3] :
( ~ iext(X1,X2,X3)
| iext(X0,X2,X3)
| iext(X1,sK124_skl(X1,X0),sK125_skl(X1,X0))
| iext(X0,sK124_skl(X1,X0),sK125_skl(X1,X0))
| ~ ip(X1)
| ~ ip(X0) ),
inference(resolution,[status(thm)],[f1822,f1820]) ).
fof(f5657,plain,
! [X0,X1,X2,X3] :
( iext(X1,X2,X3)
| ~ iext(X0,X2,X3)
| iext(X1,sK124_skl(X1,X0),sK125_skl(X1,X0))
| iext(X0,sK124_skl(X1,X0),sK125_skl(X1,X0))
| ~ ip(X1)
| ~ ip(X0) ),
inference(resolution,[status(thm)],[f1822,f1819]) ).
fof(f5667,definition,
( sQ202_spl
<=> ip(uri_ex_p3) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f5669,plain,
( sQ202_spl
| ~ ip(uri_ex_p3) ),
inference(component_clause,[status(thm)],[f5667]) ).
fof(f5670,plain,
( sQ197_spl
| sQ196_spl
| ~ sQ195_spl
| ~ sQ202_spl ),
inference(split_clause,[status(thm)],[f5651,f5667,f5600,f5603,f5606]) ).
fof(f5679,plain,
! [X0,X1,X2,X3] :
( ~ iext(X1,X2,X3)
| iext(X0,X2,X3)
| iext(X1,sK124_skl(X1,X0),sK125_skl(X1,X0))
| iext(X0,sK124_skl(X1,X0),sK125_skl(X1,X0))
| ~ ip(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5656,f564]) ).
fof(f5680,plain,
! [X0,X1,X2,X3] :
( iext(X0,X2,X3)
| ~ iext(X1,X2,X3)
| iext(X0,sK124_skl(X0,X1),sK125_skl(X0,X1))
| iext(X1,sK124_skl(X0,X1),sK125_skl(X0,X1))
| ~ ip(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5657,f564]) ).
fof(f5681,plain,
( sQ195_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5602,f5533]) ).
fof(f5682,plain,
sQ195_spl,
inference(contradiction_clause,[status(thm)],[f5681]) ).
fof(f5683,plain,
( sQ202_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5669,f5538]) ).
fof(f5684,plain,
sQ202_spl,
inference(contradiction_clause,[status(thm)],[f5683]) ).
fof(f5693,plain,
! [X0,X1,X2] :
( ~ ir(X2)
| iext(X0,X1,X2)
| ~ iext(X0,sK124_skl(uri_owl_topObjectProperty,X0),sK125_skl(uri_owl_topObjectProperty,X0)) ),
inference(resolution,[status(thm)],[f5637,f2584]) ).
fof(f5694,plain,
! [X0,X1,X2] :
( iext(X0,X1,X2)
| ~ iext(X0,sK124_skl(uri_owl_topObjectProperty,X0),sK125_skl(uri_owl_topObjectProperty,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5693,f565]) ).
fof(f5723,plain,
! [X0,X1] :
( ~ ir(sK125_skl(uri_owl_topObjectProperty,uri_owl_topObjectProperty))
| iext(uri_owl_topObjectProperty,X0,X1) ),
inference(resolution,[status(thm)],[f5694,f2584]) ).
fof(f5724,plain,
! [X0,X1] :
( ~ lv(sK125_skl(uri_owl_topObjectProperty,uri_owl_topDataProperty))
| iext(uri_owl_topDataProperty,X0,X1) ),
inference(resolution,[status(thm)],[f5694,f2582]) ).
fof(f5725,plain,
! [X0,X1] :
( sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom) = sK125_skl(uri_owl_topObjectProperty,uri_owl_differentFrom)
| iext(uri_owl_differentFrom,X0,X1) ),
inference(resolution,[status(thm)],[f5694,f1752]) ).
fof(f5728,plain,
! [X0,X1,X2] :
( ~ iext(uri_rdfs_subClassOf,X2,sK125_skl(uri_owl_topObjectProperty,uri_rdfs_subClassOf))
| ~ iext(uri_rdfs_subClassOf,sK124_skl(uri_owl_topObjectProperty,uri_rdfs_subClassOf),X2)
| iext(uri_rdfs_subClassOf,X0,X1) ),
inference(resolution,[status(thm)],[f5694,f663]) ).
fof(f5804,definition,
! [X0,X1] :
( sQ227_spl
<=> iext(uri_owl_topObjectProperty,X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition]) ).
fof(f5805,plain,
! [X0,X1] :
( ~ sQ227_spl
| iext(uri_owl_topObjectProperty,X0,X1) ),
inference(component_clause,[status(thm)],[f5804]) ).
fof(f5807,definition,
( sQ228_spl
<=> ir(sK125_skl(uri_owl_topObjectProperty,uri_owl_topObjectProperty)) ),
introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition]) ).
fof(f5809,plain,
( sQ228_spl
| ~ ir(sK125_skl(uri_owl_topObjectProperty,uri_owl_topObjectProperty)) ),
inference(component_clause,[status(thm)],[f5807]) ).
fof(f5810,plain,
( ~ sQ228_spl
| sQ227_spl ),
inference(split_clause,[status(thm)],[f5723,f5804,f5807]) ).
fof(f5811,definition,
! [X0,X1] :
( sQ229_spl
<=> iext(uri_owl_topDataProperty,X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition]) ).
fof(f5812,plain,
! [X0,X1] :
( ~ sQ229_spl
| iext(uri_owl_topDataProperty,X0,X1) ),
inference(component_clause,[status(thm)],[f5811]) ).
fof(f5814,definition,
( sQ230_spl
<=> lv(sK125_skl(uri_owl_topObjectProperty,uri_owl_topDataProperty)) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f5816,plain,
( sQ230_spl
| ~ lv(sK125_skl(uri_owl_topObjectProperty,uri_owl_topDataProperty)) ),
inference(component_clause,[status(thm)],[f5814]) ).
fof(f5817,plain,
( ~ sQ230_spl
| sQ229_spl ),
inference(split_clause,[status(thm)],[f5724,f5811,f5814]) ).
fof(f5818,definition,
! [X0,X1] :
( sQ231_spl
<=> iext(uri_owl_differentFrom,X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition]) ).
fof(f5819,plain,
! [X0,X1] :
( ~ sQ231_spl
| iext(uri_owl_differentFrom,X0,X1) ),
inference(component_clause,[status(thm)],[f5818]) ).
fof(f5821,definition,
( sQ232_spl
<=> sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom) = sK125_skl(uri_owl_topObjectProperty,uri_owl_differentFrom) ),
introduced(definition,[new_symbols(definition,[sQ232_spl])],[split_symbol_definition]) ).
fof(f5822,plain,
( ~ sQ232_spl
| sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom) = sK125_skl(uri_owl_topObjectProperty,uri_owl_differentFrom) ),
inference(component_clause,[status(thm)],[f5821]) ).
fof(f5824,plain,
( sQ232_spl
| sQ231_spl ),
inference(split_clause,[status(thm)],[f5725,f5818,f5821]) ).
fof(f5825,definition,
! [X0,X1] :
( sQ233_spl
<=> iext(uri_rdfs_subClassOf,X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition]) ).
fof(f5826,plain,
! [X0,X1] :
( ~ sQ233_spl
| iext(uri_rdfs_subClassOf,X0,X1) ),
inference(component_clause,[status(thm)],[f5825]) ).
fof(f5842,definition,
! [X2] :
( sQ238_spl
<=> ( ~ iext(uri_rdfs_subClassOf,X2,sK125_skl(uri_owl_topObjectProperty,uri_rdfs_subClassOf))
| ~ iext(uri_rdfs_subClassOf,sK124_skl(uri_owl_topObjectProperty,uri_rdfs_subClassOf),X2) ) ),
introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition]) ).
fof(f5845,plain,
( sQ238_spl
| sQ233_spl ),
inference(split_clause,[status(thm)],[f5728,f5825,f5842]) ).
fof(f5883,plain,
( sQ228_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5809,f565]) ).
fof(f5884,plain,
sQ228_spl,
inference(contradiction_clause,[status(thm)],[f5883]) ).
fof(f5890,plain,
! [X0,X1] :
( ~ sQ233_spl
| ~ icext(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f2537,f5826]) ).
fof(f5928,plain,
( ~ sQ110_spl
| ~ sQ233_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4321,f5890]) ).
fof(f5984,plain,
( ~ sQ110_spl
| ~ sQ233_spl ),
inference(contradiction_clause,[status(thm)],[f5928]) ).
fof(f6070,plain,
( ~ sQ231_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2518,f5819]) ).
fof(f6074,plain,
~ sQ231_spl,
inference(contradiction_clause,[status(thm)],[f6070]) ).
fof(f6075,plain,
! [X0] :
( ~ sQ229_spl
| lv(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1061,f5812]) ).
fof(f6077,plain,
! [X0,X1,X2] :
( ~ sQ229_spl
| iext(X0,X1,X2)
| ~ iext(uri_owl_topDataProperty,X1,X2)
| ~ iext(X0,sK124_skl(X0,uri_owl_topDataProperty),sK125_skl(X0,uri_owl_topDataProperty)) ),
inference(resolution,[status(thm)],[f5812,f5619]) ).
fof(f6078,plain,
! [X0,X1,X2] :
( ~ sQ229_spl
| ~ iext(uri_owl_topDataProperty,X1,X2)
| iext(X0,X1,X2)
| ~ iext(X0,sK124_skl(uri_owl_topDataProperty,X0),sK125_skl(uri_owl_topDataProperty,X0)) ),
inference(resolution,[status(thm)],[f5812,f5618]) ).
fof(f6079,plain,
! [X0,X1,X2] :
( ~ sQ229_spl
| iext(X0,X1,X2)
| ~ iext(X0,sK124_skl(X0,uri_owl_topDataProperty),sK125_skl(X0,uri_owl_topDataProperty)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6077,f5812]) ).
fof(f6080,plain,
! [X0,X1,X2] :
( ~ sQ229_spl
| iext(X0,X1,X2)
| ~ iext(X0,sK124_skl(uri_owl_topDataProperty,X0),sK125_skl(uri_owl_topDataProperty,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6078,f5812]) ).
fof(f6082,plain,
! [X0,X1,X2] :
( ~ sQ227_spl
| iext(X0,X1,X2)
| ~ iext(uri_owl_topObjectProperty,X1,X2)
| ~ iext(X0,sK124_skl(X0,uri_owl_topObjectProperty),sK125_skl(X0,uri_owl_topObjectProperty)) ),
inference(resolution,[status(thm)],[f5805,f5619]) ).
fof(f6084,plain,
! [X0,X1,X2] :
( ~ sQ227_spl
| iext(X0,X1,X2)
| ~ iext(X0,sK124_skl(X0,uri_owl_topObjectProperty),sK125_skl(X0,uri_owl_topObjectProperty)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6082,f5805]) ).
fof(f6154,plain,
! [X0,X1,X2,X3,X4] :
( ~ iext(sK125_skl(uri_owl_equivalentProperty,X0),X3,X4)
| iext(sK124_skl(uri_owl_equivalentProperty,X0),X3,X4)
| iext(uri_owl_equivalentProperty,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_equivalentProperty,X0),sK125_skl(uri_owl_equivalentProperty,X0))
| ~ ip(uri_owl_equivalentProperty) ),
inference(resolution,[status(thm)],[f5680,f1820]) ).
fof(f6155,plain,
! [X0,X1,X2,X3,X4] :
( iext(sK125_skl(uri_owl_equivalentProperty,X0),X3,X4)
| ~ iext(sK124_skl(uri_owl_equivalentProperty,X0),X3,X4)
| iext(uri_owl_equivalentProperty,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_equivalentProperty,X0),sK125_skl(uri_owl_equivalentProperty,X0))
| ~ ip(uri_owl_equivalentProperty) ),
inference(resolution,[status(thm)],[f5680,f1819]) ).
fof(f6156,definition,
( sQ251_spl
<=> ip(uri_owl_equivalentProperty) ),
introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition]) ).
fof(f6158,plain,
( sQ251_spl
| ~ ip(uri_owl_equivalentProperty) ),
inference(component_clause,[status(thm)],[f6156]) ).
fof(f6159,definition,
! [X0,X1,X2,X3,X4] :
( sQ252_spl
<=> ( ~ iext(sK125_skl(uri_owl_equivalentProperty,X0),X3,X4)
| iext(sK124_skl(uri_owl_equivalentProperty,X0),X3,X4)
| iext(uri_owl_equivalentProperty,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_equivalentProperty,X0),sK125_skl(uri_owl_equivalentProperty,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ252_spl])],[split_symbol_definition]) ).
fof(f6162,plain,
( sQ252_spl
| ~ sQ251_spl ),
inference(split_clause,[status(thm)],[f6154,f6156,f6159]) ).
fof(f6163,definition,
! [X0,X1,X2,X3,X4] :
( sQ253_spl
<=> ( iext(sK125_skl(uri_owl_equivalentProperty,X0),X3,X4)
| ~ iext(sK124_skl(uri_owl_equivalentProperty,X0),X3,X4)
| iext(uri_owl_equivalentProperty,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_equivalentProperty,X0),sK125_skl(uri_owl_equivalentProperty,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition]) ).
fof(f6166,plain,
( sQ253_spl
| ~ sQ251_spl ),
inference(split_clause,[status(thm)],[f6155,f6156,f6163]) ).
fof(f6167,plain,
( sQ251_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6158,f939]) ).
fof(f6168,plain,
sQ251_spl,
inference(contradiction_clause,[status(thm)],[f6167]) ).
fof(f6169,plain,
! [X0,X1,X2] :
( ~ sQ229_spl
| iext(X0,X1,X2)
| ~ iext(uri_owl_topDataProperty,X1,X2)
| ~ iext(X0,sK124_skl(X0,uri_owl_topDataProperty),sK125_skl(X0,uri_owl_topDataProperty)) ),
inference(resolution,[status(thm)],[f5619,f5812]) ).
fof(f6175,plain,
! [X0,X1,X2] :
( ~ sQ229_spl
| iext(X0,X1,X2)
| ~ iext(X0,sK124_skl(X0,uri_owl_topDataProperty),sK125_skl(X0,uri_owl_topDataProperty)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6169,f5812]) ).
fof(f6185,plain,
! [X0,X1] :
( ~ sQ232_spl
| ~ iext(uri_owl_topObjectProperty,X0,X1)
| iext(uri_owl_differentFrom,X0,X1)
| ~ iext(uri_owl_topObjectProperty,sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom),sK125_skl(uri_owl_topObjectProperty,uri_owl_differentFrom))
| ~ iext(uri_owl_differentFrom,sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom),sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom)) ),
inference(paramodulation,[status(thm)],[f5822,f5618]) ).
fof(f6188,plain,
! [X0,X1] :
( ~ sQ232_spl
| ~ iext(uri_owl_topObjectProperty,X0,X1)
| iext(uri_owl_differentFrom,X0,X1)
| iext(uri_owl_topObjectProperty,sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom),sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom))
| iext(uri_owl_differentFrom,sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom),sK125_skl(uri_owl_topObjectProperty,uri_owl_differentFrom))
| ~ ip(uri_owl_differentFrom) ),
inference(paramodulation,[status(thm)],[f5822,f5679]) ).
fof(f6189,definition,
( sQ254_spl
<=> iext(uri_owl_differentFrom,sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom),sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom)) ),
introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition]) ).
fof(f6191,plain,
( sQ254_spl
| ~ iext(uri_owl_differentFrom,sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom),sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom)) ),
inference(component_clause,[status(thm)],[f6189]) ).
fof(f6192,definition,
( sQ255_spl
<=> iext(uri_owl_topObjectProperty,sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom),sK125_skl(uri_owl_topObjectProperty,uri_owl_differentFrom)) ),
introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition]) ).
fof(f6194,plain,
( sQ255_spl
| ~ iext(uri_owl_topObjectProperty,sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom),sK125_skl(uri_owl_topObjectProperty,uri_owl_differentFrom)) ),
inference(component_clause,[status(thm)],[f6192]) ).
fof(f6195,definition,
! [X0,X1] :
( sQ256_spl
<=> ( ~ iext(uri_owl_topObjectProperty,X0,X1)
| iext(uri_owl_differentFrom,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition]) ).
fof(f6196,plain,
! [X0,X1] :
( ~ sQ256_spl
| ~ iext(uri_owl_topObjectProperty,X0,X1)
| iext(uri_owl_differentFrom,X0,X1) ),
inference(component_clause,[status(thm)],[f6195]) ).
fof(f6198,plain,
( ~ sQ232_spl
| sQ256_spl
| ~ sQ255_spl
| ~ sQ254_spl ),
inference(split_clause,[status(thm)],[f6185,f6189,f6192,f6195,f5821]) ).
fof(f6203,definition,
( sQ258_spl
<=> ip(uri_owl_topObjectProperty) ),
introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition]) ).
fof(f6205,plain,
( sQ258_spl
| ~ ip(uri_owl_topObjectProperty) ),
inference(component_clause,[status(thm)],[f6203]) ).
fof(f6206,definition,
( sQ259_spl
<=> iext(uri_owl_differentFrom,sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom),sK125_skl(uri_owl_topObjectProperty,uri_owl_differentFrom)) ),
introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition]) ).
fof(f6207,plain,
( ~ sQ259_spl
| iext(uri_owl_differentFrom,sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom),sK125_skl(uri_owl_topObjectProperty,uri_owl_differentFrom)) ),
inference(component_clause,[status(thm)],[f6206]) ).
fof(f6209,definition,
( sQ260_spl
<=> iext(uri_owl_topObjectProperty,sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom),sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom)) ),
introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition]) ).
fof(f6213,definition,
( sQ261_spl
<=> ip(uri_owl_differentFrom) ),
introduced(definition,[new_symbols(definition,[sQ261_spl])],[split_symbol_definition]) ).
fof(f6215,plain,
( sQ261_spl
| ~ ip(uri_owl_differentFrom) ),
inference(component_clause,[status(thm)],[f6213]) ).
fof(f6216,plain,
( ~ sQ232_spl
| sQ256_spl
| sQ260_spl
| sQ259_spl
| ~ sQ261_spl ),
inference(split_clause,[status(thm)],[f6188,f6213,f6206,f6209,f6195,f5821]) ).
fof(f6217,plain,
! [X0,X1] :
( ~ sQ256_spl
| ~ sQ227_spl
| iext(uri_owl_differentFrom,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f6196,f5805]) ).
fof(f6218,plain,
( ~ sQ259_spl
| ~ sQ232_spl
| iext(uri_owl_differentFrom,sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom),sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom)) ),
inference(forward_demodulation,[status(thm)],[f5822,f6207]) ).
fof(f6219,plain,
( sQ255_spl
| ~ sQ232_spl
| ~ iext(uri_owl_topObjectProperty,sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom),sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom)) ),
inference(forward_demodulation,[status(thm)],[f5822,f6194]) ).
fof(f6220,plain,
( sQ255_spl
| ~ sQ232_spl
| ~ sQ227_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6219,f5805]) ).
fof(f6221,plain,
( sQ255_spl
| ~ sQ232_spl
| ~ sQ227_spl ),
inference(contradiction_clause,[status(thm)],[f6220]) ).
fof(f6222,plain,
( sQ261_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6215,f919]) ).
fof(f6223,plain,
sQ261_spl,
inference(contradiction_clause,[status(thm)],[f6222]) ).
fof(f6224,plain,
( sQ258_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6205,f1069]) ).
fof(f6225,plain,
sQ258_spl,
inference(contradiction_clause,[status(thm)],[f6224]) ).
fof(f6232,plain,
( ~ sQ259_spl
| ~ sQ232_spl
| sQ254_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6218,f6191]) ).
fof(f6233,plain,
( ~ sQ259_spl
| ~ sQ232_spl
| sQ254_spl ),
inference(contradiction_clause,[status(thm)],[f6232]) ).
fof(f6234,plain,
( ~ sQ256_spl
| ~ sQ227_spl
| sQ231_spl ),
inference(split_clause,[status(thm)],[f6217,f5818,f5804,f6195]) ).
fof(f6241,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ229_spl
| ~ iext(X0,X3,X4)
| iext(uri_owl_topDataProperty,X3,X4)
| iext(uri_owl_topDataProperty,sK124_skl(X0,uri_owl_topDataProperty),sK125_skl(X0,uri_owl_topDataProperty))
| ~ ip(uri_owl_topDataProperty)
| iext(X0,X1,X2) ),
inference(resolution,[status(thm)],[f6079,f5679]) ).
fof(f6242,definition,
! [X0,X1,X2,X3,X4] :
( sQ262_spl
<=> ( ~ iext(X0,X3,X4)
| iext(uri_owl_topDataProperty,X3,X4)
| iext(uri_owl_topDataProperty,sK124_skl(X0,uri_owl_topDataProperty),sK125_skl(X0,uri_owl_topDataProperty))
| iext(X0,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ262_spl])],[split_symbol_definition]) ).
fof(f6245,definition,
( sQ263_spl
<=> ip(uri_owl_topDataProperty) ),
introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition]) ).
fof(f6247,plain,
( sQ263_spl
| ~ ip(uri_owl_topDataProperty) ),
inference(component_clause,[status(thm)],[f6245]) ).
fof(f6248,plain,
( ~ sQ229_spl
| ~ sQ263_spl
| sQ262_spl ),
inference(split_clause,[status(thm)],[f6241,f6242,f6245,f5811]) ).
fof(f6255,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ227_spl
| ~ iext(X0,X3,X4)
| iext(uri_owl_topObjectProperty,X3,X4)
| iext(uri_owl_topObjectProperty,sK124_skl(X0,uri_owl_topObjectProperty),sK125_skl(X0,uri_owl_topObjectProperty))
| ~ ip(uri_owl_topObjectProperty)
| iext(X0,X1,X2) ),
inference(resolution,[status(thm)],[f6084,f5679]) ).
fof(f6256,definition,
! [X0,X1,X2,X3,X4] :
( sQ264_spl
<=> ( ~ iext(X0,X3,X4)
| iext(uri_owl_topObjectProperty,X3,X4)
| iext(uri_owl_topObjectProperty,sK124_skl(X0,uri_owl_topObjectProperty),sK125_skl(X0,uri_owl_topObjectProperty))
| iext(X0,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ264_spl])],[split_symbol_definition]) ).
fof(f6259,plain,
( ~ sQ227_spl
| ~ sQ258_spl
| sQ264_spl ),
inference(split_clause,[status(thm)],[f6255,f6256,f6203,f5804]) ).
fof(f6268,definition,
( sQ266_spl
<=> ip(uri_rdfs_seeAlso) ),
introduced(definition,[new_symbols(definition,[sQ266_spl])],[split_symbol_definition]) ).
fof(f6270,plain,
( sQ266_spl
| ~ ip(uri_rdfs_seeAlso) ),
inference(component_clause,[status(thm)],[f6268]) ).
fof(f6295,definition,
( sQ270_spl
<=> ip(uri_owl_propertyDisjointWith) ),
introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition]) ).
fof(f6297,plain,
( sQ270_spl
| ~ ip(uri_owl_propertyDisjointWith) ),
inference(component_clause,[status(thm)],[f6295]) ).
fof(f6299,plain,
( sQ270_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6297,f1029]) ).
fof(f6300,plain,
sQ270_spl,
inference(contradiction_clause,[status(thm)],[f6299]) ).
fof(f6301,plain,
! [X0,X1,X2,X3] :
( iext(uri_owl_differentFrom,X2,X3)
| ~ iext(X1,X2,X3)
| iext(X1,sK124_skl(uri_owl_differentFrom,X1),sK125_skl(uri_owl_differentFrom,X1))
| ~ ip(uri_owl_differentFrom)
| sK124_skl(uri_owl_differentFrom,X0) = sK125_skl(uri_owl_differentFrom,X0)
| iext(X0,sK124_skl(uri_owl_differentFrom,X1),sK125_skl(uri_owl_differentFrom,X1))
| ~ iext(X0,sK124_skl(uri_owl_differentFrom,X0),sK125_skl(uri_owl_differentFrom,X0)) ),
inference(resolution,[status(thm)],[f5628,f5680]) ).
fof(f6303,definition,
! [X0,X1,X2,X3] :
( sQ271_spl
<=> ( iext(uri_owl_differentFrom,X2,X3)
| ~ iext(X1,X2,X3)
| iext(X1,sK124_skl(uri_owl_differentFrom,X1),sK125_skl(uri_owl_differentFrom,X1))
| sK124_skl(uri_owl_differentFrom,X0) = sK125_skl(uri_owl_differentFrom,X0)
| iext(X0,sK124_skl(uri_owl_differentFrom,X1),sK125_skl(uri_owl_differentFrom,X1))
| ~ iext(X0,sK124_skl(uri_owl_differentFrom,X0),sK125_skl(uri_owl_differentFrom,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition]) ).
fof(f6306,plain,
( ~ sQ261_spl
| sQ271_spl ),
inference(split_clause,[status(thm)],[f6301,f6303,f6213]) ).
fof(f6310,definition,
! [X2,X3] :
( sQ272_spl
<=> ( ~ iext(uri_owl_topObjectProperty,X2,X3)
| iext(uri_owl_topDataProperty,X2,X3) ) ),
introduced(definition,[new_symbols(definition,[sQ272_spl])],[split_symbol_definition]) ).
fof(f6311,plain,
! [X0,X1] :
( ~ sQ272_spl
| ~ iext(uri_owl_topObjectProperty,X0,X1)
| iext(uri_owl_topDataProperty,X0,X1) ),
inference(component_clause,[status(thm)],[f6310]) ).
fof(f6314,plain,
! [X0,X1] :
( ~ sQ272_spl
| ~ sQ227_spl
| iext(uri_owl_topDataProperty,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f6311,f5805]) ).
fof(f6316,plain,
( sQ230_spl
| ~ sQ229_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5816,f6075]) ).
fof(f6317,plain,
( sQ230_spl
| ~ sQ229_spl ),
inference(contradiction_clause,[status(thm)],[f6316]) ).
fof(f6318,plain,
! [X0,X1] :
( ~ sQ272_spl
| ~ sQ227_spl
| iext(uri_owl_topDataProperty,X0,X1) ),
inference(resolution,[status(thm)],[f6314,f5694]) ).
fof(f6322,plain,
( ~ sQ272_spl
| ~ sQ227_spl
| sQ229_spl ),
inference(split_clause,[status(thm)],[f6318,f5811,f5804,f6310]) ).
fof(f6425,plain,
ip(uri_owl_backwardCompatibleWith),
inference(resolution,[status(thm)],[f699,f890]) ).
fof(f6432,plain,
ip(uri_rdfs_seeAlso),
inference(resolution,[status(thm)],[f699,f1041]) ).
fof(f6434,plain,
( sQ266_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6432,f6270]) ).
fof(f6435,plain,
sQ266_spl,
inference(contradiction_clause,[status(thm)],[f6434]) ).
fof(f6509,plain,
( sQ263_spl
| ~ iodp(uri_owl_topDataProperty) ),
inference(resolution,[status(thm)],[f708,f6247]) ).
fof(f6515,plain,
( sQ263_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6509,f1063]) ).
fof(f6516,plain,
sQ263_spl,
inference(contradiction_clause,[status(thm)],[f6515]) ).
fof(f6537,definition,
( sQ286_spl
<=> ip(uri_owl_hasSelf) ),
introduced(definition,[new_symbols(definition,[sQ286_spl])],[split_symbol_definition]) ).
fof(f6539,plain,
( sQ286_spl
| ~ ip(uri_owl_hasSelf) ),
inference(component_clause,[status(thm)],[f6537]) ).
fof(f6544,plain,
( sQ286_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6539,f947]) ).
fof(f6545,plain,
sQ286_spl,
inference(contradiction_clause,[status(thm)],[f6544]) ).
fof(f6583,definition,
( sQ288_spl
<=> ip(uri_owl_backwardCompatibleWith) ),
introduced(definition,[new_symbols(definition,[sQ288_spl])],[split_symbol_definition]) ).
fof(f6585,plain,
( sQ288_spl
| ~ ip(uri_owl_backwardCompatibleWith) ),
inference(component_clause,[status(thm)],[f6583]) ).
fof(f6590,plain,
( sQ288_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6585,f6425]) ).
fof(f6591,plain,
sQ288_spl,
inference(contradiction_clause,[status(thm)],[f6590]) ).
fof(f6594,definition,
( sQ290_spl
<=> ip(uri_owl_assertionProperty) ),
introduced(definition,[new_symbols(definition,[sQ290_spl])],[split_symbol_definition]) ).
fof(f6596,plain,
( sQ290_spl
| ~ ip(uri_owl_assertionProperty) ),
inference(component_clause,[status(thm)],[f6594]) ).
fof(f6601,plain,
( sQ290_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6596,f886]) ).
fof(f6602,plain,
sQ290_spl,
inference(contradiction_clause,[status(thm)],[f6601]) ).
fof(f6603,plain,
! [X0,X1,X2] :
( iext(uri_owl_bottomObjectProperty,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_bottomObjectProperty,X0),sK125_skl(uri_owl_bottomObjectProperty,X0))
| ~ ip(uri_owl_bottomObjectProperty) ),
inference(resolution,[status(thm)],[f894,f5680]) ).
fof(f6605,definition,
( sQ292_spl
<=> ip(uri_owl_bottomObjectProperty) ),
introduced(definition,[new_symbols(definition,[sQ292_spl])],[split_symbol_definition]) ).
fof(f6607,plain,
( sQ292_spl
| ~ ip(uri_owl_bottomObjectProperty) ),
inference(component_clause,[status(thm)],[f6605]) ).
fof(f6608,definition,
! [X0,X1,X2] :
( sQ293_spl
<=> ( iext(uri_owl_bottomObjectProperty,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_bottomObjectProperty,X0),sK125_skl(uri_owl_bottomObjectProperty,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ293_spl])],[split_symbol_definition]) ).
fof(f6609,plain,
! [X0,X1,X2] :
( ~ sQ293_spl
| iext(uri_owl_bottomObjectProperty,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_bottomObjectProperty,X0),sK125_skl(uri_owl_bottomObjectProperty,X0)) ),
inference(component_clause,[status(thm)],[f6608]) ).
fof(f6611,plain,
( sQ293_spl
| ~ sQ292_spl ),
inference(split_clause,[status(thm)],[f6603,f6605,f6608]) ).
fof(f6612,plain,
( sQ292_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6607,f895]) ).
fof(f6613,plain,
sQ292_spl,
inference(contradiction_clause,[status(thm)],[f6612]) ).
fof(f6614,plain,
! [X0,X1,X2] :
( ~ sQ293_spl
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_bottomObjectProperty,X0),sK125_skl(uri_owl_bottomObjectProperty,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6609,f894]) ).
fof(f6616,plain,
! [X0,X1,X2] :
( ~ sQ293_spl
| sK124_skl(uri_owl_differentFrom,X2) = sK125_skl(uri_owl_differentFrom,X2)
| iext(X2,sK124_skl(uri_owl_bottomObjectProperty,uri_owl_differentFrom),sK125_skl(uri_owl_bottomObjectProperty,uri_owl_differentFrom))
| ~ iext(X2,sK124_skl(uri_owl_differentFrom,X2),sK125_skl(uri_owl_differentFrom,X2))
| ~ iext(uri_owl_differentFrom,X0,X1) ),
inference(resolution,[status(thm)],[f6614,f5628]) ).
fof(f6617,plain,
! [X0,X1,X2,X3] :
( ~ sQ293_spl
| ~ iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X2,X3)
| iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X2,X3)
| ~ iext(uri_owl_equivalentProperty,X0,X1) ),
inference(resolution,[status(thm)],[f6614,f1820]) ).
fof(f6618,plain,
! [X0,X1,X2,X3] :
( ~ sQ293_spl
| iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X2,X3)
| ~ iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X2,X3)
| ~ iext(uri_owl_equivalentProperty,X0,X1) ),
inference(resolution,[status(thm)],[f6614,f1819]) ).
fof(f6621,definition,
! [X0,X1] :
( sQ294_spl
<=> ~ iext(uri_owl_differentFrom,X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ294_spl])],[split_symbol_definition]) ).
fof(f6622,plain,
! [X0,X1] :
( ~ sQ294_spl
| ~ iext(uri_owl_differentFrom,X0,X1) ),
inference(component_clause,[status(thm)],[f6621]) ).
fof(f6624,definition,
! [X2] :
( sQ295_spl
<=> ( sK124_skl(uri_owl_differentFrom,X2) = sK125_skl(uri_owl_differentFrom,X2)
| iext(X2,sK124_skl(uri_owl_bottomObjectProperty,uri_owl_differentFrom),sK125_skl(uri_owl_bottomObjectProperty,uri_owl_differentFrom))
| ~ iext(X2,sK124_skl(uri_owl_differentFrom,X2),sK125_skl(uri_owl_differentFrom,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ295_spl])],[split_symbol_definition]) ).
fof(f6627,plain,
( ~ sQ293_spl
| sQ295_spl
| sQ294_spl ),
inference(split_clause,[status(thm)],[f6616,f6621,f6624,f6608]) ).
fof(f6628,definition,
! [X0,X1] :
( sQ296_spl
<=> ~ iext(uri_owl_equivalentProperty,X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ296_spl])],[split_symbol_definition]) ).
fof(f6629,plain,
! [X0,X1] :
( ~ sQ296_spl
| ~ iext(uri_owl_equivalentProperty,X0,X1) ),
inference(component_clause,[status(thm)],[f6628]) ).
fof(f6631,definition,
! [X2,X3] :
( sQ297_spl
<=> ( ~ iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X2,X3)
| iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X2,X3) ) ),
introduced(definition,[new_symbols(definition,[sQ297_spl])],[split_symbol_definition]) ).
fof(f6632,plain,
! [X0,X1] :
( ~ sQ297_spl
| ~ iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0,X1)
| iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0,X1) ),
inference(component_clause,[status(thm)],[f6631]) ).
fof(f6634,plain,
( ~ sQ293_spl
| sQ297_spl
| sQ296_spl ),
inference(split_clause,[status(thm)],[f6617,f6628,f6631,f6608]) ).
fof(f6635,definition,
! [X2,X3] :
( sQ298_spl
<=> ( iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X2,X3)
| ~ iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X2,X3) ) ),
introduced(definition,[new_symbols(definition,[sQ298_spl])],[split_symbol_definition]) ).
fof(f6636,plain,
! [X0,X1] :
( ~ sQ298_spl
| iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0,X1)
| ~ iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0,X1) ),
inference(component_clause,[status(thm)],[f6635]) ).
fof(f6638,plain,
( ~ sQ293_spl
| sQ298_spl
| sQ296_spl ),
inference(split_clause,[status(thm)],[f6618,f6628,f6635,f6608]) ).
fof(f6640,plain,
! [X0,X1,X2] :
( ~ sQ296_spl
| iext(uri_owl_equivalentProperty,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_equivalentProperty,X0),sK125_skl(uri_owl_equivalentProperty,X0))
| ~ ip(uri_owl_equivalentProperty) ),
inference(resolution,[status(thm)],[f6629,f5680]) ).
fof(f6642,definition,
! [X0,X1,X2] :
( sQ299_spl
<=> ( iext(uri_owl_equivalentProperty,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_equivalentProperty,X0),sK125_skl(uri_owl_equivalentProperty,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ299_spl])],[split_symbol_definition]) ).
fof(f6643,plain,
! [X0,X1,X2] :
( ~ sQ299_spl
| iext(uri_owl_equivalentProperty,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_equivalentProperty,X0),sK125_skl(uri_owl_equivalentProperty,X0)) ),
inference(component_clause,[status(thm)],[f6642]) ).
fof(f6645,plain,
( ~ sQ296_spl
| sQ299_spl
| ~ sQ251_spl ),
inference(split_clause,[status(thm)],[f6640,f6156,f6642,f6628]) ).
fof(f6646,plain,
! [X0,X1,X2] :
( ~ sQ299_spl
| ~ sQ296_spl
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_equivalentProperty,X0),sK125_skl(uri_owl_equivalentProperty,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6643,f6629]) ).
fof(f6648,plain,
! [X0,X1,X2] :
( ~ sQ294_spl
| iext(uri_owl_differentFrom,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_differentFrom,X0),sK125_skl(uri_owl_differentFrom,X0))
| ~ ip(uri_owl_differentFrom) ),
inference(resolution,[status(thm)],[f6622,f5680]) ).
fof(f6650,definition,
! [X0,X1,X2] :
( sQ300_spl
<=> ( iext(uri_owl_differentFrom,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_differentFrom,X0),sK125_skl(uri_owl_differentFrom,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ300_spl])],[split_symbol_definition]) ).
fof(f6651,plain,
! [X0,X1,X2] :
( ~ sQ300_spl
| iext(uri_owl_differentFrom,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_differentFrom,X0),sK125_skl(uri_owl_differentFrom,X0)) ),
inference(component_clause,[status(thm)],[f6650]) ).
fof(f6653,plain,
( ~ sQ294_spl
| sQ300_spl
| ~ sQ261_spl ),
inference(split_clause,[status(thm)],[f6648,f6213,f6650,f6621]) ).
fof(f6660,plain,
! [X0,X1] :
( ~ sQ293_spl
| ~ sQ298_spl
| ~ iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0,X1)
| iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),sK124_skl(uri_owl_bottomObjectProperty,sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty)),sK125_skl(uri_owl_bottomObjectProperty,sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty))) ),
inference(resolution,[status(thm)],[f6636,f6614]) ).
fof(f6661,plain,
! [X0,X1,X2] :
( ~ sQ298_spl
| iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0),sK125_skl(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0))
| ~ ip(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty))
| iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),sK124_skl(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0),sK125_skl(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0)) ),
inference(resolution,[status(thm)],[f6636,f5680]) ).
fof(f6666,definition,
! [X0,X1] :
( sQ302_spl
<=> ~ iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition]) ).
fof(f6667,plain,
! [X0,X1] :
( ~ sQ302_spl
| ~ iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0,X1) ),
inference(component_clause,[status(thm)],[f6666]) ).
fof(f6670,definition,
( sQ303_spl
<=> iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),sK124_skl(uri_owl_bottomObjectProperty,sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty)),sK125_skl(uri_owl_bottomObjectProperty,sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty))) ),
introduced(definition,[new_symbols(definition,[sQ303_spl])],[split_symbol_definition]) ).
fof(f6673,plain,
( ~ sQ293_spl
| ~ sQ298_spl
| sQ302_spl
| sQ303_spl ),
inference(split_clause,[status(thm)],[f6660,f6670,f6666,f6635,f6608]) ).
fof(f6674,definition,
! [X0,X1,X2] :
( sQ304_spl
<=> ( iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0),sK125_skl(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0))
| iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),sK124_skl(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0),sK125_skl(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ304_spl])],[split_symbol_definition]) ).
fof(f6677,definition,
( sQ305_spl
<=> ip(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty)) ),
introduced(definition,[new_symbols(definition,[sQ305_spl])],[split_symbol_definition]) ).
fof(f6680,plain,
( ~ sQ298_spl
| ~ sQ305_spl
| sQ304_spl ),
inference(split_clause,[status(thm)],[f6661,f6674,f6677,f6635]) ).
fof(f6683,plain,
! [X0,X1,X2] :
( iext(uri_owl_bottomDataProperty,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_bottomDataProperty,X0),sK125_skl(uri_owl_bottomDataProperty,X0))
| ~ ip(uri_owl_bottomDataProperty) ),
inference(resolution,[status(thm)],[f892,f5680]) ).
fof(f6685,definition,
( sQ306_spl
<=> ip(uri_owl_bottomDataProperty) ),
introduced(definition,[new_symbols(definition,[sQ306_spl])],[split_symbol_definition]) ).
fof(f6687,plain,
( sQ306_spl
| ~ ip(uri_owl_bottomDataProperty) ),
inference(component_clause,[status(thm)],[f6685]) ).
fof(f6688,definition,
! [X0,X1,X2] :
( sQ307_spl
<=> ( iext(uri_owl_bottomDataProperty,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_bottomDataProperty,X0),sK125_skl(uri_owl_bottomDataProperty,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ307_spl])],[split_symbol_definition]) ).
fof(f6689,plain,
! [X0,X1,X2] :
( ~ sQ307_spl
| iext(uri_owl_bottomDataProperty,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_bottomDataProperty,X0),sK125_skl(uri_owl_bottomDataProperty,X0)) ),
inference(component_clause,[status(thm)],[f6688]) ).
fof(f6691,plain,
( sQ307_spl
| ~ sQ306_spl ),
inference(split_clause,[status(thm)],[f6683,f6685,f6688]) ).
fof(f6692,plain,
! [X0,X1,X2] :
( ~ sQ307_spl
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_bottomDataProperty,X0),sK125_skl(uri_owl_bottomDataProperty,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6689,f892]) ).
fof(f6693,plain,
( sQ306_spl
| ~ iodp(uri_owl_bottomDataProperty) ),
inference(resolution,[status(thm)],[f6687,f708]) ).
fof(f6694,plain,
( sQ306_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6693,f893]) ).
fof(f6695,plain,
sQ306_spl,
inference(contradiction_clause,[status(thm)],[f6694]) ).
fof(f6715,plain,
! [X0,X1] :
( ~ sQ293_spl
| ~ iext(uri_owl_equivalentProperty,X0,X1)
| ip(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty)) ),
inference(resolution,[status(thm)],[f937,f6614]) ).
fof(f6716,plain,
! [X0,X1,X2] :
( iext(uri_owl_equivalentProperty,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_equivalentProperty,X0),sK125_skl(uri_owl_equivalentProperty,X0))
| ~ ip(uri_owl_equivalentProperty)
| ip(sK124_skl(uri_owl_equivalentProperty,X0)) ),
inference(resolution,[status(thm)],[f937,f5680]) ).
fof(f6718,plain,
( ~ sQ293_spl
| sQ296_spl
| sQ305_spl ),
inference(split_clause,[status(thm)],[f6715,f6677,f6628,f6608]) ).
fof(f6719,definition,
! [X0,X1,X2] :
( sQ308_spl
<=> ( iext(uri_owl_equivalentProperty,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_equivalentProperty,X0),sK125_skl(uri_owl_equivalentProperty,X0))
| ip(sK124_skl(uri_owl_equivalentProperty,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ308_spl])],[split_symbol_definition]) ).
fof(f6722,plain,
( ~ sQ251_spl
| sQ308_spl ),
inference(split_clause,[status(thm)],[f6716,f6719,f6156]) ).
fof(f6730,plain,
! [X0,X1,X2] :
( ~ sQ302_spl
| iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0),sK125_skl(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0))
| ~ ip(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty)) ),
inference(resolution,[status(thm)],[f6667,f5680]) ).
fof(f6732,definition,
! [X0,X1,X2] :
( sQ309_spl
<=> ( iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0),sK125_skl(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ309_spl])],[split_symbol_definition]) ).
fof(f6735,plain,
( ~ sQ302_spl
| sQ309_spl
| ~ sQ305_spl ),
inference(split_clause,[status(thm)],[f6730,f6677,f6732,f6666]) ).
fof(f6752,plain,
! [X0,X1] :
( ~ sQ307_spl
| ~ sQ297_spl
| ~ iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0,X1)
| iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),sK124_skl(uri_owl_bottomDataProperty,sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty)),sK125_skl(uri_owl_bottomDataProperty,sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty))) ),
inference(resolution,[status(thm)],[f6632,f6692]) ).
fof(f6753,plain,
! [X0,X1] :
( ~ sQ293_spl
| ~ sQ297_spl
| ~ iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0,X1)
| iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),sK124_skl(uri_owl_bottomObjectProperty,sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty)),sK125_skl(uri_owl_bottomObjectProperty,sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty))) ),
inference(resolution,[status(thm)],[f6632,f6614]) ).
fof(f6754,plain,
! [X0,X1,X2] :
( ~ sQ297_spl
| iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0),sK125_skl(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0))
| ~ ip(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty))
| iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),sK124_skl(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0),sK125_skl(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0)) ),
inference(resolution,[status(thm)],[f6632,f5680]) ).
fof(f6759,definition,
! [X0,X1] :
( sQ311_spl
<=> ~ iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ311_spl])],[split_symbol_definition]) ).
fof(f6760,plain,
! [X0,X1] :
( ~ sQ311_spl
| ~ iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0,X1) ),
inference(component_clause,[status(thm)],[f6759]) ).
fof(f6763,definition,
( sQ312_spl
<=> iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),sK124_skl(uri_owl_bottomDataProperty,sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty)),sK125_skl(uri_owl_bottomDataProperty,sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty))) ),
introduced(definition,[new_symbols(definition,[sQ312_spl])],[split_symbol_definition]) ).
fof(f6766,plain,
( ~ sQ307_spl
| ~ sQ297_spl
| sQ311_spl
| sQ312_spl ),
inference(split_clause,[status(thm)],[f6752,f6763,f6759,f6631,f6688]) ).
fof(f6767,definition,
( sQ313_spl
<=> iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),sK124_skl(uri_owl_bottomObjectProperty,sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty)),sK125_skl(uri_owl_bottomObjectProperty,sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty))) ),
introduced(definition,[new_symbols(definition,[sQ313_spl])],[split_symbol_definition]) ).
fof(f6770,plain,
( ~ sQ293_spl
| ~ sQ297_spl
| sQ311_spl
| sQ313_spl ),
inference(split_clause,[status(thm)],[f6753,f6767,f6759,f6631,f6608]) ).
fof(f6771,definition,
! [X0,X1,X2] :
( sQ314_spl
<=> ( iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0),sK125_skl(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0))
| iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),sK124_skl(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0),sK125_skl(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition]) ).
fof(f6774,definition,
( sQ315_spl
<=> ip(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty)) ),
introduced(definition,[new_symbols(definition,[sQ315_spl])],[split_symbol_definition]) ).
fof(f6777,plain,
( ~ sQ297_spl
| ~ sQ315_spl
| sQ314_spl ),
inference(split_clause,[status(thm)],[f6754,f6771,f6774,f6631]) ).
fof(f6786,plain,
! [X0,X1] :
( ~ sQ307_spl
| ~ iext(uri_owl_equivalentProperty,X0,X1)
| ip(sK125_skl(uri_owl_bottomDataProperty,uri_owl_equivalentProperty)) ),
inference(resolution,[status(thm)],[f938,f6692]) ).
fof(f6787,plain,
! [X0,X1] :
( ~ sQ293_spl
| ~ iext(uri_owl_equivalentProperty,X0,X1)
| ip(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty)) ),
inference(resolution,[status(thm)],[f938,f6614]) ).
fof(f6788,plain,
! [X0,X1,X2] :
( iext(uri_owl_equivalentProperty,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_equivalentProperty,X0),sK125_skl(uri_owl_equivalentProperty,X0))
| ~ ip(uri_owl_equivalentProperty)
| ip(sK125_skl(uri_owl_equivalentProperty,X0)) ),
inference(resolution,[status(thm)],[f938,f5680]) ).
fof(f6790,definition,
( sQ316_spl
<=> ip(sK125_skl(uri_owl_bottomDataProperty,uri_owl_equivalentProperty)) ),
introduced(definition,[new_symbols(definition,[sQ316_spl])],[split_symbol_definition]) ).
fof(f6793,plain,
( ~ sQ307_spl
| sQ296_spl
| sQ316_spl ),
inference(split_clause,[status(thm)],[f6786,f6790,f6628,f6688]) ).
fof(f6794,plain,
( ~ sQ293_spl
| sQ296_spl
| sQ315_spl ),
inference(split_clause,[status(thm)],[f6787,f6774,f6628,f6608]) ).
fof(f6795,definition,
! [X0,X1,X2] :
( sQ317_spl
<=> ( iext(uri_owl_equivalentProperty,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_owl_equivalentProperty,X0),sK125_skl(uri_owl_equivalentProperty,X0))
| ip(sK125_skl(uri_owl_equivalentProperty,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ317_spl])],[split_symbol_definition]) ).
fof(f6798,plain,
( ~ sQ251_spl
| sQ317_spl ),
inference(split_clause,[status(thm)],[f6788,f6795,f6156]) ).
fof(f6813,plain,
! [X0,X1,X2] :
( ~ sQ311_spl
| iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0),sK125_skl(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0))
| ~ ip(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty)) ),
inference(resolution,[status(thm)],[f6760,f5680]) ).
fof(f6815,definition,
! [X0,X1,X2] :
( sQ318_spl
<=> ( iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0),sK125_skl(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ318_spl])],[split_symbol_definition]) ).
fof(f6818,plain,
( ~ sQ311_spl
| sQ318_spl
| ~ sQ315_spl ),
inference(split_clause,[status(thm)],[f6813,f6774,f6815,f6759]) ).
fof(f6850,plain,
! [X0,X1] :
( iext(uri_ex_p2,X1,X0)
| ~ iext(uri_ex_p3,X0,X1) ),
inference(resolution,[status(thm)],[f2004,f2406]) ).
fof(f6851,plain,
! [X0,X1] :
( iext(uri_ex_p1,X1,X0)
| ~ iext(uri_ex_p2,X0,X1) ),
inference(resolution,[status(thm)],[f2004,f2407]) ).
fof(f6852,plain,
! [X0,X1,X2,X3] :
( ~ sQ300_spl
| iext(uri_owl_differentFrom,X2,X3)
| ~ iext(uri_owl_inverseOf,X2,X3)
| iext(sK125_skl(uri_owl_differentFrom,uri_owl_inverseOf),X1,X0)
| ~ iext(sK124_skl(uri_owl_differentFrom,uri_owl_inverseOf),X0,X1) ),
inference(resolution,[status(thm)],[f2004,f6651]) ).
fof(f6856,plain,
! [X0,X1,X2,X3] :
( ~ sQ299_spl
| ~ sQ296_spl
| ~ iext(uri_owl_inverseOf,X2,X3)
| iext(sK125_skl(uri_owl_equivalentProperty,uri_owl_inverseOf),X1,X0)
| ~ iext(sK124_skl(uri_owl_equivalentProperty,uri_owl_inverseOf),X0,X1) ),
inference(resolution,[status(thm)],[f2004,f6646]) ).
fof(f6857,plain,
! [X0,X1,X2,X3] :
( ~ sQ307_spl
| ~ iext(uri_owl_inverseOf,X2,X3)
| iext(sK125_skl(uri_owl_bottomDataProperty,uri_owl_inverseOf),X1,X0)
| ~ iext(sK124_skl(uri_owl_bottomDataProperty,uri_owl_inverseOf),X0,X1) ),
inference(resolution,[status(thm)],[f2004,f6692]) ).
fof(f6858,plain,
! [X0,X1,X2,X3] :
( ~ sQ293_spl
| ~ iext(uri_owl_inverseOf,X2,X3)
| iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_inverseOf),X1,X0)
| ~ iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_inverseOf),X0,X1) ),
inference(resolution,[status(thm)],[f2004,f6614]) ).
fof(f6859,plain,
! [X0,X1,X2,X3,X4] :
( iext(uri_owl_inverseOf,X3,X4)
| ~ iext(X0,X3,X4)
| iext(X0,sK124_skl(uri_owl_inverseOf,X0),sK125_skl(uri_owl_inverseOf,X0))
| ~ ip(uri_owl_inverseOf)
| iext(sK125_skl(uri_owl_inverseOf,X0),X2,X1)
| ~ iext(sK124_skl(uri_owl_inverseOf,X0),X1,X2) ),
inference(resolution,[status(thm)],[f2004,f5680]) ).
fof(f6861,definition,
! [X0,X1] :
( sQ319_spl
<=> ( iext(sK125_skl(uri_owl_differentFrom,uri_owl_inverseOf),X1,X0)
| ~ iext(sK124_skl(uri_owl_differentFrom,uri_owl_inverseOf),X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ319_spl])],[split_symbol_definition]) ).
fof(f6864,definition,
! [X2,X3] :
( sQ320_spl
<=> ( iext(uri_owl_differentFrom,X2,X3)
| ~ iext(uri_owl_inverseOf,X2,X3) ) ),
introduced(definition,[new_symbols(definition,[sQ320_spl])],[split_symbol_definition]) ).
fof(f6865,plain,
! [X0,X1] :
( ~ sQ320_spl
| iext(uri_owl_differentFrom,X0,X1)
| ~ iext(uri_owl_inverseOf,X0,X1) ),
inference(component_clause,[status(thm)],[f6864]) ).
fof(f6867,plain,
( ~ sQ300_spl
| sQ320_spl
| sQ319_spl ),
inference(split_clause,[status(thm)],[f6852,f6861,f6864,f6650]) ).
fof(f6889,definition,
! [X0,X1] :
( sQ327_spl
<=> ( iext(sK125_skl(uri_owl_equivalentProperty,uri_owl_inverseOf),X1,X0)
| ~ iext(sK124_skl(uri_owl_equivalentProperty,uri_owl_inverseOf),X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ327_spl])],[split_symbol_definition]) ).
fof(f6892,definition,
! [X2,X3] :
( sQ328_spl
<=> ~ iext(uri_owl_inverseOf,X2,X3) ),
introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition]) ).
fof(f6893,plain,
! [X0,X1] :
( ~ sQ328_spl
| ~ iext(uri_owl_inverseOf,X0,X1) ),
inference(component_clause,[status(thm)],[f6892]) ).
fof(f6895,plain,
( ~ sQ299_spl
| ~ sQ296_spl
| sQ328_spl
| sQ327_spl ),
inference(split_clause,[status(thm)],[f6856,f6889,f6892,f6628,f6642]) ).
fof(f6896,definition,
! [X0,X1] :
( sQ329_spl
<=> ( iext(sK125_skl(uri_owl_bottomDataProperty,uri_owl_inverseOf),X1,X0)
| ~ iext(sK124_skl(uri_owl_bottomDataProperty,uri_owl_inverseOf),X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ329_spl])],[split_symbol_definition]) ).
fof(f6899,plain,
( ~ sQ307_spl
| sQ328_spl
| sQ329_spl ),
inference(split_clause,[status(thm)],[f6857,f6896,f6892,f6688]) ).
fof(f6900,definition,
! [X0,X1] :
( sQ330_spl
<=> ( iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_inverseOf),X1,X0)
| ~ iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_inverseOf),X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ330_spl])],[split_symbol_definition]) ).
fof(f6903,plain,
( ~ sQ293_spl
| sQ328_spl
| sQ330_spl ),
inference(split_clause,[status(thm)],[f6858,f6900,f6892,f6608]) ).
fof(f6904,definition,
! [X0,X1,X2,X3,X4] :
( sQ331_spl
<=> ( iext(uri_owl_inverseOf,X3,X4)
| ~ iext(X0,X3,X4)
| iext(X0,sK124_skl(uri_owl_inverseOf,X0),sK125_skl(uri_owl_inverseOf,X0))
| iext(sK125_skl(uri_owl_inverseOf,X0),X2,X1)
| ~ iext(sK124_skl(uri_owl_inverseOf,X0),X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ331_spl])],[split_symbol_definition]) ).
fof(f6907,definition,
( sQ332_spl
<=> ip(uri_owl_inverseOf) ),
introduced(definition,[new_symbols(definition,[sQ332_spl])],[split_symbol_definition]) ).
fof(f6909,plain,
( sQ332_spl
| ~ ip(uri_owl_inverseOf) ),
inference(component_clause,[status(thm)],[f6907]) ).
fof(f6910,plain,
( ~ sQ332_spl
| sQ331_spl ),
inference(split_clause,[status(thm)],[f6859,f6904,f6907]) ).
fof(f6911,plain,
( sQ332_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6909,f968]) ).
fof(f6912,plain,
sQ332_spl,
inference(contradiction_clause,[status(thm)],[f6911]) ).
fof(f6913,plain,
! [X0,X1] :
( ~ iext(uri_ex_p2,X1,X0)
| iext(uri_ex_p3,X0,X1) ),
inference(resolution,[status(thm)],[f2005,f2406]) ).
fof(f6914,plain,
! [X0,X1] :
( ~ iext(uri_ex_p1,X1,X0)
| iext(uri_ex_p2,X0,X1) ),
inference(resolution,[status(thm)],[f2005,f2407]) ).
fof(f6915,plain,
! [X0,X1,X2,X3] :
( ~ sQ300_spl
| iext(uri_owl_differentFrom,X2,X3)
| ~ iext(uri_owl_inverseOf,X2,X3)
| ~ iext(sK125_skl(uri_owl_differentFrom,uri_owl_inverseOf),X1,X0)
| iext(sK124_skl(uri_owl_differentFrom,uri_owl_inverseOf),X0,X1) ),
inference(resolution,[status(thm)],[f2005,f6651]) ).
fof(f6916,plain,
! [X0,X1,X2,X3] :
( ~ sQ299_spl
| ~ sQ296_spl
| ~ iext(uri_owl_inverseOf,X2,X3)
| ~ iext(sK125_skl(uri_owl_equivalentProperty,uri_owl_inverseOf),X1,X0)
| iext(sK124_skl(uri_owl_equivalentProperty,uri_owl_inverseOf),X0,X1) ),
inference(resolution,[status(thm)],[f2005,f6646]) ).
fof(f6917,plain,
! [X0,X1,X2,X3] :
( ~ sQ307_spl
| ~ iext(uri_owl_inverseOf,X2,X3)
| ~ iext(sK125_skl(uri_owl_bottomDataProperty,uri_owl_inverseOf),X1,X0)
| iext(sK124_skl(uri_owl_bottomDataProperty,uri_owl_inverseOf),X0,X1) ),
inference(resolution,[status(thm)],[f2005,f6692]) ).
fof(f6918,plain,
! [X0,X1,X2,X3] :
( ~ sQ293_spl
| ~ iext(uri_owl_inverseOf,X2,X3)
| ~ iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_inverseOf),X1,X0)
| iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_inverseOf),X0,X1) ),
inference(resolution,[status(thm)],[f2005,f6614]) ).
fof(f6919,plain,
! [X0,X1,X2,X3,X4] :
( iext(uri_owl_inverseOf,X3,X4)
| ~ iext(X0,X3,X4)
| iext(X0,sK124_skl(uri_owl_inverseOf,X0),sK125_skl(uri_owl_inverseOf,X0))
| ~ ip(uri_owl_inverseOf)
| ~ iext(sK125_skl(uri_owl_inverseOf,X0),X2,X1)
| iext(sK124_skl(uri_owl_inverseOf,X0),X1,X2) ),
inference(resolution,[status(thm)],[f2005,f5680]) ).
fof(f6921,definition,
! [X0,X1] :
( sQ333_spl
<=> ( ~ iext(sK125_skl(uri_owl_differentFrom,uri_owl_inverseOf),X1,X0)
| iext(sK124_skl(uri_owl_differentFrom,uri_owl_inverseOf),X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ333_spl])],[split_symbol_definition]) ).
fof(f6924,plain,
( ~ sQ300_spl
| sQ320_spl
| sQ333_spl ),
inference(split_clause,[status(thm)],[f6915,f6921,f6864,f6650]) ).
fof(f6925,definition,
! [X0,X1] :
( sQ334_spl
<=> ( ~ iext(sK125_skl(uri_owl_equivalentProperty,uri_owl_inverseOf),X1,X0)
| iext(sK124_skl(uri_owl_equivalentProperty,uri_owl_inverseOf),X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ334_spl])],[split_symbol_definition]) ).
fof(f6928,plain,
( ~ sQ299_spl
| ~ sQ296_spl
| sQ328_spl
| sQ334_spl ),
inference(split_clause,[status(thm)],[f6916,f6925,f6892,f6628,f6642]) ).
fof(f6929,definition,
! [X0,X1] :
( sQ335_spl
<=> ( ~ iext(sK125_skl(uri_owl_bottomDataProperty,uri_owl_inverseOf),X1,X0)
| iext(sK124_skl(uri_owl_bottomDataProperty,uri_owl_inverseOf),X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ335_spl])],[split_symbol_definition]) ).
fof(f6932,plain,
( ~ sQ307_spl
| sQ328_spl
| sQ335_spl ),
inference(split_clause,[status(thm)],[f6917,f6929,f6892,f6688]) ).
fof(f6933,definition,
! [X0,X1] :
( sQ336_spl
<=> ( ~ iext(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_inverseOf),X1,X0)
| iext(sK124_skl(uri_owl_bottomObjectProperty,uri_owl_inverseOf),X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ336_spl])],[split_symbol_definition]) ).
fof(f6936,plain,
( ~ sQ293_spl
| sQ328_spl
| sQ336_spl ),
inference(split_clause,[status(thm)],[f6918,f6933,f6892,f6608]) ).
fof(f6937,definition,
! [X0,X1,X2,X3,X4] :
( sQ337_spl
<=> ( iext(uri_owl_inverseOf,X3,X4)
| ~ iext(X0,X3,X4)
| iext(X0,sK124_skl(uri_owl_inverseOf,X0),sK125_skl(uri_owl_inverseOf,X0))
| ~ iext(sK125_skl(uri_owl_inverseOf,X0),X2,X1)
| iext(sK124_skl(uri_owl_inverseOf,X0),X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ337_spl])],[split_symbol_definition]) ).
fof(f6940,plain,
( ~ sQ332_spl
| sQ337_spl ),
inference(split_clause,[status(thm)],[f6919,f6937,f6907]) ).
fof(f6943,plain,
! [X0] :
( ~ sQ229_spl
| ~ iext(X0,sK166_skl(uri_owl_topDataProperty,X0),sK167_skl(uri_owl_topDataProperty,X0))
| ~ ip(uri_owl_topDataProperty)
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_owl_topDataProperty) ),
inference(resolution,[status(thm)],[f2006,f5812]) ).
fof(f6944,plain,
! [X0] :
( ~ sQ227_spl
| ~ iext(X0,sK166_skl(uri_owl_topObjectProperty,X0),sK167_skl(uri_owl_topObjectProperty,X0))
| ~ ip(uri_owl_topObjectProperty)
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_owl_topObjectProperty) ),
inference(resolution,[status(thm)],[f2006,f5805]) ).
fof(f6953,definition,
! [X0] :
( sQ340_spl
<=> ( ~ iext(X0,sK166_skl(uri_owl_topDataProperty,X0),sK167_skl(uri_owl_topDataProperty,X0))
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_owl_topDataProperty) ) ),
introduced(definition,[new_symbols(definition,[sQ340_spl])],[split_symbol_definition]) ).
fof(f6956,plain,
( ~ sQ229_spl
| ~ sQ263_spl
| sQ340_spl ),
inference(split_clause,[status(thm)],[f6943,f6953,f6245,f5811]) ).
fof(f6957,definition,
! [X0] :
( sQ341_spl
<=> ( ~ iext(X0,sK166_skl(uri_owl_topObjectProperty,X0),sK167_skl(uri_owl_topObjectProperty,X0))
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_owl_topObjectProperty) ) ),
introduced(definition,[new_symbols(definition,[sQ341_spl])],[split_symbol_definition]) ).
fof(f6960,plain,
( ~ sQ227_spl
| ~ sQ258_spl
| sQ341_spl ),
inference(split_clause,[status(thm)],[f6944,f6957,f6203,f5804]) ).
fof(f6962,plain,
( ~ sQ328_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2406,f6893]) ).
fof(f6970,plain,
~ sQ328_spl,
inference(contradiction_clause,[status(thm)],[f6962]) ).
fof(f6980,plain,
! [X0,X1] :
( ~ sQ300_spl
| iext(uri_owl_differentFrom,X0,X1)
| ~ iext(uri_ex_p3,X0,X1)
| iext(uri_ex_p2,sK125_skl(uri_owl_differentFrom,uri_ex_p3),sK124_skl(uri_owl_differentFrom,uri_ex_p3)) ),
inference(resolution,[status(thm)],[f6850,f6651]) ).
fof(f6981,plain,
! [X0,X1] :
( ~ sQ299_spl
| ~ sQ296_spl
| ~ iext(uri_ex_p3,X0,X1)
| iext(uri_ex_p2,sK125_skl(uri_owl_equivalentProperty,uri_ex_p3),sK124_skl(uri_owl_equivalentProperty,uri_ex_p3)) ),
inference(resolution,[status(thm)],[f6850,f6646]) ).
fof(f6982,plain,
! [X0,X1] :
( ~ sQ307_spl
| ~ iext(uri_ex_p3,X0,X1)
| iext(uri_ex_p2,sK125_skl(uri_owl_bottomDataProperty,uri_ex_p3),sK124_skl(uri_owl_bottomDataProperty,uri_ex_p3)) ),
inference(resolution,[status(thm)],[f6850,f6692]) ).
fof(f6983,plain,
! [X0,X1] :
( ~ sQ293_spl
| ~ iext(uri_ex_p3,X0,X1)
| iext(uri_ex_p2,sK125_skl(uri_owl_bottomObjectProperty,uri_ex_p3),sK124_skl(uri_owl_bottomObjectProperty,uri_ex_p3)) ),
inference(resolution,[status(thm)],[f6850,f6614]) ).
fof(f6984,plain,
! [X0,X1,X2] :
( iext(uri_ex_p3,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_ex_p3,X0),sK125_skl(uri_ex_p3,X0))
| ~ ip(uri_ex_p3)
| iext(uri_ex_p2,sK125_skl(uri_ex_p3,X0),sK124_skl(uri_ex_p3,X0)) ),
inference(resolution,[status(thm)],[f6850,f5680]) ).
fof(f6986,definition,
( sQ342_spl
<=> iext(uri_ex_p2,sK125_skl(uri_owl_differentFrom,uri_ex_p3),sK124_skl(uri_owl_differentFrom,uri_ex_p3)) ),
introduced(definition,[new_symbols(definition,[sQ342_spl])],[split_symbol_definition]) ).
fof(f6989,definition,
! [X0,X1] :
( sQ343_spl
<=> ( iext(uri_owl_differentFrom,X0,X1)
| ~ iext(uri_ex_p3,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ343_spl])],[split_symbol_definition]) ).
fof(f6990,plain,
! [X0,X1] :
( ~ sQ343_spl
| iext(uri_owl_differentFrom,X0,X1)
| ~ iext(uri_ex_p3,X0,X1) ),
inference(component_clause,[status(thm)],[f6989]) ).
fof(f6992,plain,
( ~ sQ300_spl
| sQ343_spl
| sQ342_spl ),
inference(split_clause,[status(thm)],[f6980,f6986,f6989,f6650]) ).
fof(f6993,definition,
( sQ344_spl
<=> iext(uri_ex_p2,sK125_skl(uri_owl_equivalentProperty,uri_ex_p3),sK124_skl(uri_owl_equivalentProperty,uri_ex_p3)) ),
introduced(definition,[new_symbols(definition,[sQ344_spl])],[split_symbol_definition]) ).
fof(f6996,definition,
! [X0,X1] :
( sQ345_spl
<=> ~ iext(uri_ex_p3,X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ345_spl])],[split_symbol_definition]) ).
fof(f6997,plain,
! [X0,X1] :
( ~ sQ345_spl
| ~ iext(uri_ex_p3,X0,X1) ),
inference(component_clause,[status(thm)],[f6996]) ).
fof(f6999,plain,
( ~ sQ299_spl
| ~ sQ296_spl
| sQ345_spl
| sQ344_spl ),
inference(split_clause,[status(thm)],[f6981,f6993,f6996,f6628,f6642]) ).
fof(f7000,definition,
( sQ346_spl
<=> iext(uri_ex_p2,sK125_skl(uri_owl_bottomDataProperty,uri_ex_p3),sK124_skl(uri_owl_bottomDataProperty,uri_ex_p3)) ),
introduced(definition,[new_symbols(definition,[sQ346_spl])],[split_symbol_definition]) ).
fof(f7003,plain,
( ~ sQ307_spl
| sQ345_spl
| sQ346_spl ),
inference(split_clause,[status(thm)],[f6982,f7000,f6996,f6688]) ).
fof(f7004,definition,
( sQ347_spl
<=> iext(uri_ex_p2,sK125_skl(uri_owl_bottomObjectProperty,uri_ex_p3),sK124_skl(uri_owl_bottomObjectProperty,uri_ex_p3)) ),
introduced(definition,[new_symbols(definition,[sQ347_spl])],[split_symbol_definition]) ).
fof(f7007,plain,
( ~ sQ293_spl
| sQ345_spl
| sQ347_spl ),
inference(split_clause,[status(thm)],[f6983,f7004,f6996,f6608]) ).
fof(f7008,definition,
! [X0,X1,X2] :
( sQ348_spl
<=> ( iext(uri_ex_p3,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_ex_p3,X0),sK125_skl(uri_ex_p3,X0))
| iext(uri_ex_p2,sK125_skl(uri_ex_p3,X0),sK124_skl(uri_ex_p3,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ348_spl])],[split_symbol_definition]) ).
fof(f7011,plain,
( ~ sQ202_spl
| sQ348_spl ),
inference(split_clause,[status(thm)],[f6984,f7008,f5667]) ).
fof(f7016,plain,
! [X0,X1,X2] :
( ~ sQ345_spl
| iext(uri_ex_p3,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_ex_p3,X0),sK125_skl(uri_ex_p3,X0))
| ~ ip(uri_ex_p3) ),
inference(resolution,[status(thm)],[f6997,f5680]) ).
fof(f7018,definition,
! [X0,X1,X2] :
( sQ349_spl
<=> ( iext(uri_ex_p3,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_ex_p3,X0),sK125_skl(uri_ex_p3,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ349_spl])],[split_symbol_definition]) ).
fof(f7021,plain,
( ~ sQ345_spl
| sQ349_spl
| ~ sQ202_spl ),
inference(split_clause,[status(thm)],[f7016,f5667,f7018,f6996]) ).
fof(f7025,plain,
! [X0] :
( ~ sQ311_spl
| iext(X0,sK166_skl(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0),sK167_skl(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0))
| ~ ip(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty))
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty)) ),
inference(resolution,[status(thm)],[f2007,f6760]) ).
fof(f7026,plain,
! [X0] :
( ~ sQ296_spl
| iext(X0,sK166_skl(uri_owl_equivalentProperty,X0),sK167_skl(uri_owl_equivalentProperty,X0))
| ~ ip(uri_owl_equivalentProperty)
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_owl_equivalentProperty) ),
inference(resolution,[status(thm)],[f2007,f6629]) ).
fof(f7027,plain,
! [X0] :
( iext(X0,sK166_skl(uri_owl_bottomDataProperty,X0),sK167_skl(uri_owl_bottomDataProperty,X0))
| ~ ip(uri_owl_bottomDataProperty)
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_owl_bottomDataProperty) ),
inference(resolution,[status(thm)],[f2007,f892]) ).
fof(f7028,plain,
! [X0] :
( iext(X0,sK166_skl(uri_owl_bottomObjectProperty,X0),sK167_skl(uri_owl_bottomObjectProperty,X0))
| ~ ip(uri_owl_bottomObjectProperty)
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_owl_bottomObjectProperty) ),
inference(resolution,[status(thm)],[f2007,f894]) ).
fof(f7029,plain,
! [X0] :
( ~ sQ345_spl
| iext(X0,sK166_skl(uri_ex_p3,X0),sK167_skl(uri_ex_p3,X0))
| ~ ip(uri_ex_p3)
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_ex_p3) ),
inference(resolution,[status(thm)],[f2007,f6997]) ).
fof(f7030,definition,
! [X0] :
( sQ350_spl
<=> ( iext(X0,sK166_skl(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0),sK167_skl(sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty),X0))
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,sK125_skl(uri_owl_bottomObjectProperty,uri_owl_equivalentProperty)) ) ),
introduced(definition,[new_symbols(definition,[sQ350_spl])],[split_symbol_definition]) ).
fof(f7033,plain,
( ~ sQ311_spl
| ~ sQ315_spl
| sQ350_spl ),
inference(split_clause,[status(thm)],[f7025,f7030,f6774,f6759]) ).
fof(f7034,definition,
! [X0] :
( sQ351_spl
<=> ( iext(X0,sK166_skl(uri_owl_equivalentProperty,X0),sK167_skl(uri_owl_equivalentProperty,X0))
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_owl_equivalentProperty) ) ),
introduced(definition,[new_symbols(definition,[sQ351_spl])],[split_symbol_definition]) ).
fof(f7037,plain,
( ~ sQ296_spl
| ~ sQ251_spl
| sQ351_spl ),
inference(split_clause,[status(thm)],[f7026,f7034,f6156,f6628]) ).
fof(f7038,definition,
! [X0] :
( sQ352_spl
<=> ( iext(X0,sK166_skl(uri_owl_bottomDataProperty,X0),sK167_skl(uri_owl_bottomDataProperty,X0))
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_owl_bottomDataProperty) ) ),
introduced(definition,[new_symbols(definition,[sQ352_spl])],[split_symbol_definition]) ).
fof(f7041,plain,
( ~ sQ306_spl
| sQ352_spl ),
inference(split_clause,[status(thm)],[f7027,f7038,f6685]) ).
fof(f7042,definition,
! [X0] :
( sQ353_spl
<=> ( iext(X0,sK166_skl(uri_owl_bottomObjectProperty,X0),sK167_skl(uri_owl_bottomObjectProperty,X0))
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_owl_bottomObjectProperty) ) ),
introduced(definition,[new_symbols(definition,[sQ353_spl])],[split_symbol_definition]) ).
fof(f7045,plain,
( ~ sQ292_spl
| sQ353_spl ),
inference(split_clause,[status(thm)],[f7028,f7042,f6605]) ).
fof(f7046,definition,
! [X0] :
( sQ354_spl
<=> ( iext(X0,sK166_skl(uri_ex_p3,X0),sK167_skl(uri_ex_p3,X0))
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_ex_p3) ) ),
introduced(definition,[new_symbols(definition,[sQ354_spl])],[split_symbol_definition]) ).
fof(f7049,plain,
( ~ sQ345_spl
| ~ sQ202_spl
| sQ354_spl ),
inference(split_clause,[status(thm)],[f7029,f7046,f5667,f6996]) ).
fof(f7050,plain,
! [X0] :
( ~ sQ76_spl
| iext(X0,sK168_skl(X0),sK169_skl(X0))
| ~ ip(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2014,f4201]) ).
fof(f7053,plain,
( ~ sQ76_spl
| ~ ip(uri_owl_bottomObjectProperty) ),
inference(resolution,[status(thm)],[f7050,f894]) ).
fof(f7056,plain,
( ~ sQ76_spl
| ~ sQ292_spl ),
inference(split_clause,[status(thm)],[f7053,f6605,f4200]) ).
fof(f7057,plain,
! [X0] :
( iext(X0,sK166_skl(uri_ex_p2,X0),sK167_skl(uri_ex_p2,X0))
| ~ ip(uri_ex_p2)
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_ex_p2)
| iext(uri_ex_p1,sK166_skl(uri_ex_p2,X0),sK167_skl(uri_ex_p2,X0)) ),
inference(resolution,[status(thm)],[f6851,f2007]) ).
fof(f7058,plain,
! [X0,X1] :
( ~ sQ300_spl
| iext(uri_owl_differentFrom,X0,X1)
| ~ iext(uri_ex_p2,X0,X1)
| iext(uri_ex_p1,sK125_skl(uri_owl_differentFrom,uri_ex_p2),sK124_skl(uri_owl_differentFrom,uri_ex_p2)) ),
inference(resolution,[status(thm)],[f6851,f6651]) ).
fof(f7059,plain,
! [X0,X1] :
( ~ sQ299_spl
| ~ sQ296_spl
| ~ iext(uri_ex_p2,X0,X1)
| iext(uri_ex_p1,sK125_skl(uri_owl_equivalentProperty,uri_ex_p2),sK124_skl(uri_owl_equivalentProperty,uri_ex_p2)) ),
inference(resolution,[status(thm)],[f6851,f6646]) ).
fof(f7060,plain,
! [X0,X1] :
( ~ sQ307_spl
| ~ iext(uri_ex_p2,X0,X1)
| iext(uri_ex_p1,sK125_skl(uri_owl_bottomDataProperty,uri_ex_p2),sK124_skl(uri_owl_bottomDataProperty,uri_ex_p2)) ),
inference(resolution,[status(thm)],[f6851,f6692]) ).
fof(f7061,plain,
! [X0,X1] :
( ~ sQ293_spl
| ~ iext(uri_ex_p2,X0,X1)
| iext(uri_ex_p1,sK125_skl(uri_owl_bottomObjectProperty,uri_ex_p2),sK124_skl(uri_owl_bottomObjectProperty,uri_ex_p2)) ),
inference(resolution,[status(thm)],[f6851,f6614]) ).
fof(f7062,plain,
! [X0,X1,X2] :
( iext(uri_ex_p2,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_ex_p2,X0),sK125_skl(uri_ex_p2,X0))
| ~ ip(uri_ex_p2)
| iext(uri_ex_p1,sK125_skl(uri_ex_p2,X0),sK124_skl(uri_ex_p2,X0)) ),
inference(resolution,[status(thm)],[f6851,f5680]) ).
fof(f7064,definition,
! [X0] :
( sQ355_spl
<=> ( iext(X0,sK166_skl(uri_ex_p2,X0),sK167_skl(uri_ex_p2,X0))
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_ex_p2)
| iext(uri_ex_p1,sK166_skl(uri_ex_p2,X0),sK167_skl(uri_ex_p2,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ355_spl])],[split_symbol_definition]) ).
fof(f7067,definition,
( sQ356_spl
<=> ip(uri_ex_p2) ),
introduced(definition,[new_symbols(definition,[sQ356_spl])],[split_symbol_definition]) ).
fof(f7069,plain,
( sQ356_spl
| ~ ip(uri_ex_p2) ),
inference(component_clause,[status(thm)],[f7067]) ).
fof(f7070,plain,
( ~ sQ356_spl
| sQ355_spl ),
inference(split_clause,[status(thm)],[f7057,f7064,f7067]) ).
fof(f7071,definition,
( sQ357_spl
<=> iext(uri_ex_p1,sK125_skl(uri_owl_differentFrom,uri_ex_p2),sK124_skl(uri_owl_differentFrom,uri_ex_p2)) ),
introduced(definition,[new_symbols(definition,[sQ357_spl])],[split_symbol_definition]) ).
fof(f7074,definition,
! [X0,X1] :
( sQ358_spl
<=> ( iext(uri_owl_differentFrom,X0,X1)
| ~ iext(uri_ex_p2,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ358_spl])],[split_symbol_definition]) ).
fof(f7075,plain,
! [X0,X1] :
( ~ sQ358_spl
| iext(uri_owl_differentFrom,X0,X1)
| ~ iext(uri_ex_p2,X0,X1) ),
inference(component_clause,[status(thm)],[f7074]) ).
fof(f7077,plain,
( ~ sQ300_spl
| sQ358_spl
| sQ357_spl ),
inference(split_clause,[status(thm)],[f7058,f7071,f7074,f6650]) ).
fof(f7078,definition,
( sQ359_spl
<=> iext(uri_ex_p1,sK125_skl(uri_owl_equivalentProperty,uri_ex_p2),sK124_skl(uri_owl_equivalentProperty,uri_ex_p2)) ),
introduced(definition,[new_symbols(definition,[sQ359_spl])],[split_symbol_definition]) ).
fof(f7081,definition,
! [X0,X1] :
( sQ360_spl
<=> ~ iext(uri_ex_p2,X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ360_spl])],[split_symbol_definition]) ).
fof(f7082,plain,
! [X0,X1] :
( ~ sQ360_spl
| ~ iext(uri_ex_p2,X0,X1) ),
inference(component_clause,[status(thm)],[f7081]) ).
fof(f7084,plain,
( ~ sQ299_spl
| ~ sQ296_spl
| sQ360_spl
| sQ359_spl ),
inference(split_clause,[status(thm)],[f7059,f7078,f7081,f6628,f6642]) ).
fof(f7085,definition,
( sQ361_spl
<=> iext(uri_ex_p1,sK125_skl(uri_owl_bottomDataProperty,uri_ex_p2),sK124_skl(uri_owl_bottomDataProperty,uri_ex_p2)) ),
introduced(definition,[new_symbols(definition,[sQ361_spl])],[split_symbol_definition]) ).
fof(f7088,plain,
( ~ sQ307_spl
| sQ360_spl
| sQ361_spl ),
inference(split_clause,[status(thm)],[f7060,f7085,f7081,f6688]) ).
fof(f7089,definition,
( sQ362_spl
<=> iext(uri_ex_p1,sK125_skl(uri_owl_bottomObjectProperty,uri_ex_p2),sK124_skl(uri_owl_bottomObjectProperty,uri_ex_p2)) ),
introduced(definition,[new_symbols(definition,[sQ362_spl])],[split_symbol_definition]) ).
fof(f7092,plain,
( ~ sQ293_spl
| sQ360_spl
| sQ362_spl ),
inference(split_clause,[status(thm)],[f7061,f7089,f7081,f6608]) ).
fof(f7093,definition,
! [X0,X1,X2] :
( sQ363_spl
<=> ( iext(uri_ex_p2,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_ex_p2,X0),sK125_skl(uri_ex_p2,X0))
| iext(uri_ex_p1,sK125_skl(uri_ex_p2,X0),sK124_skl(uri_ex_p2,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ363_spl])],[split_symbol_definition]) ).
fof(f7096,plain,
( ~ sQ356_spl
| sQ363_spl ),
inference(split_clause,[status(thm)],[f7062,f7093,f7067]) ).
fof(f7097,plain,
( sQ356_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7069,f5534]) ).
fof(f7098,plain,
sQ356_spl,
inference(contradiction_clause,[status(thm)],[f7097]) ).
fof(f7230,plain,
! [X0] :
( ~ sQ94_spl
| iext(X0,sK172_skl(X0),sK170_skl(X0))
| ~ ip(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2022,f4264]) ).
fof(f7233,plain,
( ~ sQ94_spl
| ~ ip(uri_owl_bottomObjectProperty) ),
inference(resolution,[status(thm)],[f7230,f894]) ).
fof(f7236,plain,
( ~ sQ94_spl
| ~ sQ292_spl ),
inference(split_clause,[status(thm)],[f7233,f6605,f4263]) ).
fof(f7238,plain,
! [X0,X1] :
( ~ sQ229_spl
| ~ sQ320_spl
| iext(uri_owl_differentFrom,X0,X1)
| ~ iext(uri_owl_inverseOf,sK124_skl(uri_owl_topDataProperty,uri_owl_differentFrom),sK125_skl(uri_owl_topDataProperty,uri_owl_differentFrom)) ),
inference(resolution,[status(thm)],[f6865,f6080]) ).
fof(f7239,plain,
! [X0,X1] :
( ~ sQ320_spl
| iext(uri_owl_differentFrom,X0,X1)
| ~ iext(uri_owl_inverseOf,sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom),sK125_skl(uri_owl_topObjectProperty,uri_owl_differentFrom)) ),
inference(resolution,[status(thm)],[f6865,f5694]) ).
fof(f7240,plain,
! [X0,X1] :
( ~ sQ229_spl
| ~ sQ320_spl
| iext(uri_owl_differentFrom,X0,X1)
| ~ iext(uri_owl_inverseOf,sK124_skl(uri_owl_differentFrom,uri_owl_topDataProperty),sK125_skl(uri_owl_differentFrom,uri_owl_topDataProperty)) ),
inference(resolution,[status(thm)],[f6865,f6175]) ).
fof(f7241,plain,
! [X0,X1] :
( ~ sQ227_spl
| ~ sQ320_spl
| iext(uri_owl_differentFrom,X0,X1)
| ~ iext(uri_owl_inverseOf,sK124_skl(uri_owl_differentFrom,uri_owl_topObjectProperty),sK125_skl(uri_owl_differentFrom,uri_owl_topObjectProperty)) ),
inference(resolution,[status(thm)],[f6865,f6084]) ).
fof(f7244,definition,
( sQ384_spl
<=> iext(uri_owl_inverseOf,sK124_skl(uri_owl_topDataProperty,uri_owl_differentFrom),sK125_skl(uri_owl_topDataProperty,uri_owl_differentFrom)) ),
introduced(definition,[new_symbols(definition,[sQ384_spl])],[split_symbol_definition]) ).
fof(f7247,plain,
( ~ sQ229_spl
| ~ sQ320_spl
| sQ231_spl
| ~ sQ384_spl ),
inference(split_clause,[status(thm)],[f7238,f7244,f5818,f6864,f5811]) ).
fof(f7248,definition,
( sQ385_spl
<=> iext(uri_owl_inverseOf,sK124_skl(uri_owl_topObjectProperty,uri_owl_differentFrom),sK125_skl(uri_owl_topObjectProperty,uri_owl_differentFrom)) ),
introduced(definition,[new_symbols(definition,[sQ385_spl])],[split_symbol_definition]) ).
fof(f7251,plain,
( ~ sQ320_spl
| sQ231_spl
| ~ sQ385_spl ),
inference(split_clause,[status(thm)],[f7239,f7248,f5818,f6864]) ).
fof(f7252,definition,
( sQ386_spl
<=> iext(uri_owl_inverseOf,sK124_skl(uri_owl_differentFrom,uri_owl_topDataProperty),sK125_skl(uri_owl_differentFrom,uri_owl_topDataProperty)) ),
introduced(definition,[new_symbols(definition,[sQ386_spl])],[split_symbol_definition]) ).
fof(f7255,plain,
( ~ sQ229_spl
| ~ sQ320_spl
| sQ231_spl
| ~ sQ386_spl ),
inference(split_clause,[status(thm)],[f7240,f7252,f5818,f6864,f5811]) ).
fof(f7256,definition,
( sQ387_spl
<=> iext(uri_owl_inverseOf,sK124_skl(uri_owl_differentFrom,uri_owl_topObjectProperty),sK125_skl(uri_owl_differentFrom,uri_owl_topObjectProperty)) ),
introduced(definition,[new_symbols(definition,[sQ387_spl])],[split_symbol_definition]) ).
fof(f7259,plain,
( ~ sQ227_spl
| ~ sQ320_spl
| sQ231_spl
| ~ sQ387_spl ),
inference(split_clause,[status(thm)],[f7241,f7256,f5818,f6864,f5804]) ).
fof(f7261,plain,
! [X0] :
( iext(X0,sK166_skl(uri_ex_p2,X0),sK167_skl(uri_ex_p2,X0))
| ~ ip(uri_ex_p2)
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_ex_p2)
| iext(uri_ex_p3,sK166_skl(uri_ex_p2,X0),sK167_skl(uri_ex_p2,X0)) ),
inference(resolution,[status(thm)],[f6913,f2007]) ).
fof(f7262,plain,
! [X0,X1] :
( ~ sQ299_spl
| ~ sQ296_spl
| ~ iext(uri_ex_p2,X0,X1)
| iext(uri_ex_p3,sK125_skl(uri_owl_equivalentProperty,uri_ex_p2),sK124_skl(uri_owl_equivalentProperty,uri_ex_p2)) ),
inference(resolution,[status(thm)],[f6913,f6646]) ).
fof(f7263,plain,
! [X0,X1] :
( ~ sQ307_spl
| ~ iext(uri_ex_p2,X0,X1)
| iext(uri_ex_p3,sK125_skl(uri_owl_bottomDataProperty,uri_ex_p2),sK124_skl(uri_owl_bottomDataProperty,uri_ex_p2)) ),
inference(resolution,[status(thm)],[f6913,f6692]) ).
fof(f7264,plain,
! [X0,X1] :
( ~ sQ293_spl
| ~ iext(uri_ex_p2,X0,X1)
| iext(uri_ex_p3,sK125_skl(uri_owl_bottomObjectProperty,uri_ex_p2),sK124_skl(uri_owl_bottomObjectProperty,uri_ex_p2)) ),
inference(resolution,[status(thm)],[f6913,f6614]) ).
fof(f7265,plain,
! [X0,X1,X2] :
( iext(uri_ex_p2,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_ex_p2,X0),sK125_skl(uri_ex_p2,X0))
| ~ ip(uri_ex_p2)
| iext(uri_ex_p3,sK125_skl(uri_ex_p2,X0),sK124_skl(uri_ex_p2,X0)) ),
inference(resolution,[status(thm)],[f6913,f5680]) ).
fof(f7267,definition,
! [X0] :
( sQ388_spl
<=> ( iext(X0,sK166_skl(uri_ex_p2,X0),sK167_skl(uri_ex_p2,X0))
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_ex_p2)
| iext(uri_ex_p3,sK166_skl(uri_ex_p2,X0),sK167_skl(uri_ex_p2,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ388_spl])],[split_symbol_definition]) ).
fof(f7270,plain,
( ~ sQ356_spl
| sQ388_spl ),
inference(split_clause,[status(thm)],[f7261,f7267,f7067]) ).
fof(f7271,definition,
( sQ389_spl
<=> iext(uri_ex_p3,sK125_skl(uri_owl_equivalentProperty,uri_ex_p2),sK124_skl(uri_owl_equivalentProperty,uri_ex_p2)) ),
introduced(definition,[new_symbols(definition,[sQ389_spl])],[split_symbol_definition]) ).
fof(f7274,plain,
( ~ sQ299_spl
| ~ sQ296_spl
| sQ360_spl
| sQ389_spl ),
inference(split_clause,[status(thm)],[f7262,f7271,f7081,f6628,f6642]) ).
fof(f7275,definition,
( sQ390_spl
<=> iext(uri_ex_p3,sK125_skl(uri_owl_bottomDataProperty,uri_ex_p2),sK124_skl(uri_owl_bottomDataProperty,uri_ex_p2)) ),
introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition]) ).
fof(f7278,plain,
( ~ sQ307_spl
| sQ360_spl
| sQ390_spl ),
inference(split_clause,[status(thm)],[f7263,f7275,f7081,f6688]) ).
fof(f7279,definition,
( sQ391_spl
<=> iext(uri_ex_p3,sK125_skl(uri_owl_bottomObjectProperty,uri_ex_p2),sK124_skl(uri_owl_bottomObjectProperty,uri_ex_p2)) ),
introduced(definition,[new_symbols(definition,[sQ391_spl])],[split_symbol_definition]) ).
fof(f7282,plain,
( ~ sQ293_spl
| sQ360_spl
| sQ391_spl ),
inference(split_clause,[status(thm)],[f7264,f7279,f7081,f6608]) ).
fof(f7283,definition,
! [X0,X1,X2] :
( sQ392_spl
<=> ( iext(uri_ex_p2,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_ex_p2,X0),sK125_skl(uri_ex_p2,X0))
| iext(uri_ex_p3,sK125_skl(uri_ex_p2,X0),sK124_skl(uri_ex_p2,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ392_spl])],[split_symbol_definition]) ).
fof(f7286,plain,
( ~ sQ356_spl
| sQ392_spl ),
inference(split_clause,[status(thm)],[f7265,f7283,f7067]) ).
fof(f7295,plain,
( ~ sQ197_spl
| ~ sQ360_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5607,f7296]) ).
fof(f7296,plain,
! [X0,X1] :
( ~ sQ360_spl
| ~ iext(uri_ex_p1,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f6914,f7082]) ).
fof(f7303,plain,
( ~ sQ197_spl
| ~ sQ360_spl ),
inference(contradiction_clause,[status(thm)],[f7295]) ).
fof(f7312,plain,
! [X0] :
( ~ sQ343_spl
| iext(X0,sK166_skl(uri_ex_p3,X0),sK167_skl(uri_ex_p3,X0))
| ~ ip(uri_ex_p3)
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_ex_p3)
| iext(uri_owl_differentFrom,sK167_skl(uri_ex_p3,X0),sK166_skl(uri_ex_p3,X0)) ),
inference(resolution,[status(thm)],[f6990,f2007]) ).
fof(f7313,plain,
! [X0,X1] :
( ~ sQ299_spl
| ~ sQ296_spl
| ~ sQ343_spl
| ~ iext(uri_ex_p3,X0,X1)
| iext(uri_owl_differentFrom,sK124_skl(uri_owl_equivalentProperty,uri_ex_p3),sK125_skl(uri_owl_equivalentProperty,uri_ex_p3)) ),
inference(resolution,[status(thm)],[f6990,f6646]) ).
fof(f7314,plain,
! [X0,X1] :
( ~ sQ307_spl
| ~ sQ343_spl
| ~ iext(uri_ex_p3,X0,X1)
| iext(uri_owl_differentFrom,sK124_skl(uri_owl_bottomDataProperty,uri_ex_p3),sK125_skl(uri_owl_bottomDataProperty,uri_ex_p3)) ),
inference(resolution,[status(thm)],[f6990,f6692]) ).
fof(f7315,plain,
! [X0,X1] :
( ~ sQ293_spl
| ~ sQ343_spl
| ~ iext(uri_ex_p3,X0,X1)
| iext(uri_owl_differentFrom,sK124_skl(uri_owl_bottomObjectProperty,uri_ex_p3),sK125_skl(uri_owl_bottomObjectProperty,uri_ex_p3)) ),
inference(resolution,[status(thm)],[f6990,f6614]) ).
fof(f7316,plain,
! [X0,X1,X2] :
( ~ sQ343_spl
| iext(uri_ex_p3,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_ex_p3,X0),sK125_skl(uri_ex_p3,X0))
| ~ ip(uri_ex_p3)
| iext(uri_owl_differentFrom,sK124_skl(uri_ex_p3,X0),sK125_skl(uri_ex_p3,X0)) ),
inference(resolution,[status(thm)],[f6990,f5680]) ).
fof(f7318,definition,
! [X0] :
( sQ395_spl
<=> ( iext(X0,sK166_skl(uri_ex_p3,X0),sK167_skl(uri_ex_p3,X0))
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_ex_p3)
| iext(uri_owl_differentFrom,sK167_skl(uri_ex_p3,X0),sK166_skl(uri_ex_p3,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ395_spl])],[split_symbol_definition]) ).
fof(f7321,plain,
( ~ sQ343_spl
| ~ sQ202_spl
| sQ395_spl ),
inference(split_clause,[status(thm)],[f7312,f7318,f5667,f6989]) ).
fof(f7322,definition,
( sQ396_spl
<=> iext(uri_owl_differentFrom,sK124_skl(uri_owl_equivalentProperty,uri_ex_p3),sK125_skl(uri_owl_equivalentProperty,uri_ex_p3)) ),
introduced(definition,[new_symbols(definition,[sQ396_spl])],[split_symbol_definition]) ).
fof(f7325,plain,
( ~ sQ299_spl
| ~ sQ296_spl
| ~ sQ343_spl
| sQ345_spl
| sQ396_spl ),
inference(split_clause,[status(thm)],[f7313,f7322,f6996,f6989,f6628,f6642]) ).
fof(f7326,definition,
( sQ397_spl
<=> iext(uri_owl_differentFrom,sK124_skl(uri_owl_bottomDataProperty,uri_ex_p3),sK125_skl(uri_owl_bottomDataProperty,uri_ex_p3)) ),
introduced(definition,[new_symbols(definition,[sQ397_spl])],[split_symbol_definition]) ).
fof(f7329,plain,
( ~ sQ307_spl
| ~ sQ343_spl
| sQ345_spl
| sQ397_spl ),
inference(split_clause,[status(thm)],[f7314,f7326,f6996,f6989,f6688]) ).
fof(f7330,definition,
( sQ398_spl
<=> iext(uri_owl_differentFrom,sK124_skl(uri_owl_bottomObjectProperty,uri_ex_p3),sK125_skl(uri_owl_bottomObjectProperty,uri_ex_p3)) ),
introduced(definition,[new_symbols(definition,[sQ398_spl])],[split_symbol_definition]) ).
fof(f7333,plain,
( ~ sQ293_spl
| ~ sQ343_spl
| sQ345_spl
| sQ398_spl ),
inference(split_clause,[status(thm)],[f7315,f7330,f6996,f6989,f6608]) ).
fof(f7334,definition,
! [X0,X1,X2] :
( sQ399_spl
<=> ( iext(uri_ex_p3,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_ex_p3,X0),sK125_skl(uri_ex_p3,X0))
| iext(uri_owl_differentFrom,sK124_skl(uri_ex_p3,X0),sK125_skl(uri_ex_p3,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ399_spl])],[split_symbol_definition]) ).
fof(f7337,plain,
( ~ sQ343_spl
| ~ sQ202_spl
| sQ399_spl ),
inference(split_clause,[status(thm)],[f7316,f7334,f5667,f6989]) ).
fof(f7346,plain,
! [X0] :
( ~ sQ358_spl
| iext(X0,sK166_skl(uri_ex_p2,X0),sK167_skl(uri_ex_p2,X0))
| ~ ip(uri_ex_p2)
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_ex_p2)
| iext(uri_owl_differentFrom,sK167_skl(uri_ex_p2,X0),sK166_skl(uri_ex_p2,X0)) ),
inference(resolution,[status(thm)],[f7075,f2007]) ).
fof(f7347,plain,
! [X0,X1] :
( ~ sQ299_spl
| ~ sQ296_spl
| ~ sQ358_spl
| ~ iext(uri_ex_p2,X0,X1)
| iext(uri_owl_differentFrom,sK124_skl(uri_owl_equivalentProperty,uri_ex_p2),sK125_skl(uri_owl_equivalentProperty,uri_ex_p2)) ),
inference(resolution,[status(thm)],[f7075,f6646]) ).
fof(f7348,plain,
! [X0,X1] :
( ~ sQ307_spl
| ~ sQ358_spl
| ~ iext(uri_ex_p2,X0,X1)
| iext(uri_owl_differentFrom,sK124_skl(uri_owl_bottomDataProperty,uri_ex_p2),sK125_skl(uri_owl_bottomDataProperty,uri_ex_p2)) ),
inference(resolution,[status(thm)],[f7075,f6692]) ).
fof(f7349,plain,
! [X0,X1] :
( ~ sQ293_spl
| ~ sQ358_spl
| ~ iext(uri_ex_p2,X0,X1)
| iext(uri_owl_differentFrom,sK124_skl(uri_owl_bottomObjectProperty,uri_ex_p2),sK125_skl(uri_owl_bottomObjectProperty,uri_ex_p2)) ),
inference(resolution,[status(thm)],[f7075,f6614]) ).
fof(f7350,plain,
! [X0,X1,X2] :
( ~ sQ358_spl
| iext(uri_ex_p2,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_ex_p2,X0),sK125_skl(uri_ex_p2,X0))
| ~ ip(uri_ex_p2)
| iext(uri_owl_differentFrom,sK124_skl(uri_ex_p2,X0),sK125_skl(uri_ex_p2,X0)) ),
inference(resolution,[status(thm)],[f7075,f5680]) ).
fof(f7352,definition,
! [X0] :
( sQ400_spl
<=> ( iext(X0,sK166_skl(uri_ex_p2,X0),sK167_skl(uri_ex_p2,X0))
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,uri_ex_p2)
| iext(uri_owl_differentFrom,sK167_skl(uri_ex_p2,X0),sK166_skl(uri_ex_p2,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ400_spl])],[split_symbol_definition]) ).
fof(f7355,plain,
( ~ sQ358_spl
| ~ sQ356_spl
| sQ400_spl ),
inference(split_clause,[status(thm)],[f7346,f7352,f7067,f7074]) ).
fof(f7356,definition,
( sQ401_spl
<=> iext(uri_owl_differentFrom,sK124_skl(uri_owl_equivalentProperty,uri_ex_p2),sK125_skl(uri_owl_equivalentProperty,uri_ex_p2)) ),
introduced(definition,[new_symbols(definition,[sQ401_spl])],[split_symbol_definition]) ).
fof(f7359,plain,
( ~ sQ299_spl
| ~ sQ296_spl
| ~ sQ358_spl
| sQ360_spl
| sQ401_spl ),
inference(split_clause,[status(thm)],[f7347,f7356,f7081,f7074,f6628,f6642]) ).
fof(f7360,definition,
( sQ402_spl
<=> iext(uri_owl_differentFrom,sK124_skl(uri_owl_bottomDataProperty,uri_ex_p2),sK125_skl(uri_owl_bottomDataProperty,uri_ex_p2)) ),
introduced(definition,[new_symbols(definition,[sQ402_spl])],[split_symbol_definition]) ).
fof(f7363,plain,
( ~ sQ307_spl
| ~ sQ358_spl
| sQ360_spl
| sQ402_spl ),
inference(split_clause,[status(thm)],[f7348,f7360,f7081,f7074,f6688]) ).
fof(f7364,definition,
( sQ403_spl
<=> iext(uri_owl_differentFrom,sK124_skl(uri_owl_bottomObjectProperty,uri_ex_p2),sK125_skl(uri_owl_bottomObjectProperty,uri_ex_p2)) ),
introduced(definition,[new_symbols(definition,[sQ403_spl])],[split_symbol_definition]) ).
fof(f7367,plain,
( ~ sQ293_spl
| ~ sQ358_spl
| sQ360_spl
| sQ403_spl ),
inference(split_clause,[status(thm)],[f7349,f7364,f7081,f7074,f6608]) ).
fof(f7368,definition,
! [X0,X1,X2] :
( sQ404_spl
<=> ( iext(uri_ex_p2,X1,X2)
| ~ iext(X0,X1,X2)
| iext(X0,sK124_skl(uri_ex_p2,X0),sK125_skl(uri_ex_p2,X0))
| iext(uri_owl_differentFrom,sK124_skl(uri_ex_p2,X0),sK125_skl(uri_ex_p2,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ404_spl])],[split_symbol_definition]) ).
fof(f7371,plain,
( ~ sQ358_spl
| ~ sQ356_spl
| sQ404_spl ),
inference(split_clause,[status(thm)],[f7350,f7368,f7067,f7074]) ).
fof(f7388,plain,
( ~ sQ196_spl
| ~ sQ345_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5604,f6997]) ).
fof(f7389,plain,
( ~ sQ196_spl
| ~ sQ345_spl ),
inference(contradiction_clause,[status(thm)],[f7388]) ).
fof(f7402,plain,
! [X0,X1] :
( ~ sQ229_spl
| iext(uri_ex_p2,X0,X1)
| ~ iext(uri_ex_p1,sK125_skl(uri_owl_topDataProperty,uri_ex_p2),sK124_skl(uri_owl_topDataProperty,uri_ex_p2)) ),
inference(resolution,[status(thm)],[f6914,f6080]) ).
fof(f7403,plain,
! [X0,X1] :
( iext(uri_ex_p2,X0,X1)
| ~ iext(uri_ex_p1,sK125_skl(uri_owl_topObjectProperty,uri_ex_p2),sK124_skl(uri_owl_topObjectProperty,uri_ex_p2)) ),
inference(resolution,[status(thm)],[f6914,f5694]) ).
fof(f7404,plain,
! [X0,X1] :
( ~ sQ229_spl
| iext(uri_ex_p2,X0,X1)
| ~ iext(uri_ex_p1,sK125_skl(uri_ex_p2,uri_owl_topDataProperty),sK124_skl(uri_ex_p2,uri_owl_topDataProperty)) ),
inference(resolution,[status(thm)],[f6914,f6175]) ).
fof(f7405,plain,
! [X0,X1] :
( ~ sQ227_spl
| iext(uri_ex_p2,X0,X1)
| ~ iext(uri_ex_p1,sK125_skl(uri_ex_p2,uri_owl_topObjectProperty),sK124_skl(uri_ex_p2,uri_owl_topObjectProperty)) ),
inference(resolution,[status(thm)],[f6914,f6084]) ).
fof(f7408,definition,
( sQ405_spl
<=> iext(uri_ex_p1,sK125_skl(uri_owl_topDataProperty,uri_ex_p2),sK124_skl(uri_owl_topDataProperty,uri_ex_p2)) ),
introduced(definition,[new_symbols(definition,[sQ405_spl])],[split_symbol_definition]) ).
fof(f7411,definition,
! [X0,X1] :
( sQ406_spl
<=> iext(uri_ex_p2,X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ406_spl])],[split_symbol_definition]) ).
fof(f7412,plain,
! [X0,X1] :
( ~ sQ406_spl
| iext(uri_ex_p2,X0,X1) ),
inference(component_clause,[status(thm)],[f7411]) ).
fof(f7414,plain,
( ~ sQ229_spl
| sQ406_spl
| ~ sQ405_spl ),
inference(split_clause,[status(thm)],[f7402,f7408,f7411,f5811]) ).
fof(f7415,definition,
( sQ407_spl
<=> iext(uri_ex_p1,sK125_skl(uri_owl_topObjectProperty,uri_ex_p2),sK124_skl(uri_owl_topObjectProperty,uri_ex_p2)) ),
introduced(definition,[new_symbols(definition,[sQ407_spl])],[split_symbol_definition]) ).
fof(f7418,plain,
( sQ406_spl
| ~ sQ407_spl ),
inference(split_clause,[status(thm)],[f7403,f7415,f7411]) ).
fof(f7419,definition,
( sQ408_spl
<=> iext(uri_ex_p1,sK125_skl(uri_ex_p2,uri_owl_topDataProperty),sK124_skl(uri_ex_p2,uri_owl_topDataProperty)) ),
introduced(definition,[new_symbols(definition,[sQ408_spl])],[split_symbol_definition]) ).
fof(f7422,plain,
( ~ sQ229_spl
| sQ406_spl
| ~ sQ408_spl ),
inference(split_clause,[status(thm)],[f7404,f7419,f7411,f5811]) ).
fof(f7423,definition,
( sQ409_spl
<=> iext(uri_ex_p1,sK125_skl(uri_ex_p2,uri_owl_topObjectProperty),sK124_skl(uri_ex_p2,uri_owl_topObjectProperty)) ),
introduced(definition,[new_symbols(definition,[sQ409_spl])],[split_symbol_definition]) ).
fof(f7426,plain,
( ~ sQ227_spl
| sQ406_spl
| ~ sQ409_spl ),
inference(split_clause,[status(thm)],[f7405,f7423,f7411,f5804]) ).
fof(f7443,plain,
! [X0,X1] :
( ~ sQ345_spl
| ~ iext(uri_ex_p2,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f6913,f6997]) ).
fof(f7445,plain,
! [X0,X1] :
( ~ sQ299_spl
| ~ sQ296_spl
| ~ sQ345_spl
| ~ iext(uri_ex_p2,X0,X1) ),
inference(resolution,[status(thm)],[f7443,f6646]) ).
fof(f7452,plain,
( ~ sQ299_spl
| ~ sQ296_spl
| ~ sQ345_spl
| sQ360_spl ),
inference(split_clause,[status(thm)],[f7445,f7081,f6996,f6628,f6642]) ).
fof(f7473,plain,
! [X0] :
( ~ sQ96_spl
| iext(X0,sK173_skl(X0),sK175_skl(X0))
| ~ ip(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2031,f4271]) ).
fof(f7476,plain,
( ~ sQ96_spl
| ~ ip(uri_owl_bottomObjectProperty) ),
inference(resolution,[status(thm)],[f7473,f894]) ).
fof(f7479,plain,
( ~ sQ96_spl
| ~ sQ292_spl ),
inference(split_clause,[status(thm)],[f7476,f6605,f4270]) ).
fof(f7481,plain,
( sQ196_spl
| ~ sQ406_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5605,f7482]) ).
fof(f7482,plain,
! [X0,X1] :
( ~ sQ406_spl
| iext(uri_ex_p3,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f6913,f7412]) ).
fof(f7487,plain,
( sQ196_spl
| ~ sQ406_spl ),
inference(contradiction_clause,[status(thm)],[f7481]) ).
fof(f7507,plain,
! [X0,X1] :
( ~ sQ360_spl
| ~ iext(uri_ex_p3,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f6850,f7082]) ).
fof(f7510,plain,
! [X0,X1] :
( ~ sQ307_spl
| ~ sQ360_spl
| ~ iext(uri_ex_p3,X0,X1) ),
inference(resolution,[status(thm)],[f7507,f6692]) ).
fof(f7516,plain,
( ~ sQ307_spl
| ~ sQ360_spl
| sQ345_spl ),
inference(split_clause,[status(thm)],[f7510,f6996,f7081,f6688]) ).
fof(f7541,plain,
! [X0] :
( ~ sQ113_spl
| ~ iext(X0,sK177_skl(X0),sK177_skl(X0))
| ~ ip(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2045,f4331]) ).
fof(f7546,plain,
( ~ sQ113_spl
| ~ ip(uri_owl_sameAs) ),
inference(resolution,[status(thm)],[f7541,f2519]) ).
fof(f7552,plain,
( ~ sQ113_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7546,f1037]) ).
fof(f7553,plain,
~ sQ113_spl,
inference(contradiction_clause,[status(thm)],[f7552]) ).
fof(f7635,plain,
( sQ196_spl
| ~ iext(uri_ex_p2,sK125_skl(uri_ex_p1,uri_ex_p3),sK124_skl(uri_ex_p1,uri_ex_p3)) ),
inference(resolution,[status(thm)],[f5605,f6913]) ).
fof(f7643,plain,
! [X0] :
( ~ sQ119_spl
| iext(X0,sK178_skl(X0),sK179_skl(X0))
| ~ ip(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2052,f4352]) ).
fof(f7646,plain,
( ~ sQ119_spl
| ~ ip(uri_owl_bottomObjectProperty) ),
inference(resolution,[status(thm)],[f7643,f894]) ).
fof(f7649,plain,
( ~ sQ119_spl
| ~ sQ292_spl ),
inference(split_clause,[status(thm)],[f7646,f6605,f4351]) ).
fof(f7671,plain,
( sQ196_spl
| ~ iext(uri_ex_p1,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3)) ),
inference(resolution,[status(thm)],[f6914,f7635]) ).
fof(f7676,plain,
( sQ196_spl
| ~ sQ197_spl ),
inference(split_clause,[status(thm)],[f7671,f5606,f5603]) ).
fof(f7710,plain,
! [X0] :
( ~ sQ123_spl
| iext(X0,sK180_skl(X0),sK182_skl(X0))
| ~ ip(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2060,f4366]) ).
fof(f7713,plain,
( ~ sQ123_spl
| ~ ip(uri_owl_bottomObjectProperty) ),
inference(resolution,[status(thm)],[f7710,f894]) ).
fof(f7716,plain,
( ~ sQ123_spl
| ~ sQ292_spl ),
inference(split_clause,[status(thm)],[f7713,f6605,f4365]) ).
fof(f7754,plain,
( sQ197_spl
| ~ iext(uri_ex_p2,sK125_skl(uri_ex_p1,uri_ex_p3),sK124_skl(uri_ex_p1,uri_ex_p3)) ),
inference(resolution,[status(thm)],[f5608,f6851]) ).
fof(f7785,plain,
( sQ197_spl
| ~ iext(uri_ex_p3,sK124_skl(uri_ex_p1,uri_ex_p3),sK125_skl(uri_ex_p1,uri_ex_p3)) ),
inference(resolution,[status(thm)],[f6850,f7754]) ).
fof(f7792,plain,
( sQ197_spl
| ~ sQ196_spl ),
inference(split_clause,[status(thm)],[f7785,f5603,f5606]) ).
fof(f7795,plain,
$false,
inference(sat_refutation,[status(thm)],[f2890,f3053,f3074,f3251,f3253,f4168,f4175,f4182,f4196,f4203,f4217,f4224,f4231,f4238,f4245,f4266,f4273,f4305,f4319,f4326,f4333,f4340,f4354,f4361,f4368,f4412,f4416,f4420,f4428,f4432,f4440,f4444,f4448,f4452,f4456,f4468,f4472,f4492,f4500,f4504,f4508,f4512,f4520,f4524,f4528,f4530,f4532,f4634,f4646,f4722,f4773,f4832,f4860,f4870,f4876,f4884,f4962,f5062,f5125,f5256,f5258,f5329,f5354,f5609,f5670,f5682,f5684,f5810,f5817,f5824,f5845,f5884,f5984,f6074,f6162,f6166,f6168,f6198,f6216,f6221,f6223,f6225,f6233,f6234,f6248,f6259,f6300,f6306,f6317,f6322,f6435,f6516,f6545,f6591,f6602,f6611,f6613,f6627,f6634,f6638,f6645,f6653,f6673,f6680,f6691,f6695,f6718,f6722,f6735,f6766,f6770,f6777,f6793,f6794,f6798,f6818,f6867,f6895,f6899,f6903,f6910,f6912,f6924,f6928,f6932,f6936,f6940,f6956,f6960,f6970,f6992,f6999,f7003,f7007,f7011,f7021,f7033,f7037,f7041,f7045,f7049,f7056,f7070,f7077,f7084,f7088,f7092,f7096,f7098,f7236,f7247,f7251,f7255,f7259,f7270,f7274,f7278,f7282,f7286,f7303,f7321,f7325,f7329,f7333,f7337,f7355,f7359,f7363,f7367,f7371,f7389,f7414,f7418,f7422,f7426,f7452,f7479,f7487,f7516,f7553,f7649,f7676,f7716,f7792]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWB067+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n001.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 07:50:43 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.24/0.48 % Drodi V4.1.1
% 27.69/4.06 % Refutation found
% 27.69/4.06 % SZS status Theorem for theBenchmark: Theorem is valid
% 27.69/4.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.05/4.12 % Elapsed time: 3.657195 seconds
% 2.05/4.12 % CPU time: 28.364006 seconds
% 2.05/4.12 % Total memory used: 243.087 MB
% 2.05/4.12 % Net memory used: 232.690 MB
%------------------------------------------------------------------------------