%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWB016+3 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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 : Tue Sep 29 01:00:37 PM UTC 2026
% Result : CounterSatisfiable 2.21s 0.82s
% Output : Saturation 2.21s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u459,axiom,
ic(uri_rdfs_Resource) ).
cnf(u495,axiom,
ip(uri_rdfs_subClassOf) ).
cnf(u499,axiom,
( ic(sK15(uri_rdfs_subClassOf,X0))
| ~ ip(X0)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0) ) ).
cnf(u503,axiom,
( ic(sK14(uri_rdfs_subClassOf,X0))
| ~ ip(X0)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0) ) ).
cnf(u507,axiom,
( ~ icext(sK14(uri_rdfs_subClassOf,X0),X1)
| ~ ip(X0)
| icext(sK15(uri_rdfs_subClassOf,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0) ) ).
cnf(u511,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,sK14(uri_rdfs_subClassOf,X0))
| iext(uri_rdfs_subClassOf,X1,sK15(uri_rdfs_subClassOf,X0))
| ~ ip(X0)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0) ) ).
cnf(u515,axiom,
( iext(uri_rdfs_subClassOf,sK14(uri_rdfs_subClassOf,X0),uri_rdfs_Resource)
| ~ ip(X0)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0) ) ).
cnf(u519,axiom,
ip(uri_rdfs_subPropertyOf) ).
cnf(u523,axiom,
( ip(sK15(uri_rdfs_subPropertyOf,X0))
| ~ ip(X0)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u527,axiom,
( ip(sK14(uri_rdfs_subPropertyOf,X0))
| ~ ip(X0)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u531,axiom,
( ~ iext(sK14(uri_rdfs_subPropertyOf,X0),X1,X2)
| ~ ip(X0)
| iext(sK15(uri_rdfs_subPropertyOf,X0),X1,X2)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u535,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X1,sK14(uri_rdfs_subPropertyOf,X0))
| iext(uri_rdfs_subPropertyOf,X1,sK15(uri_rdfs_subPropertyOf,X0))
| ~ ip(X0)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u582,axiom,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_rdfs_Resource) ).
cnf(u839,axiom,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_owl_Thing) ).
cnf(u947,axiom,
ip(uri_rdfs_domain) ).
cnf(u951,axiom,
( ic(sK15(uri_rdfs_domain,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0)
| ~ ip(X0) ) ).
cnf(u983,axiom,
( ip(sK14(uri_rdfs_domain,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0)
| ~ ip(X0) ) ).
cnf(u987,axiom,
( iext(uri_rdfs_subClassOf,sK14(uri_rdfs_subClassOf,X0),uri_owl_Thing)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0)
| ~ ip(X0) ) ).
cnf(u1202,axiom,
( ioap(sK13(uri_owl_AnnotationProperty,X0))
| iext(uri_rdfs_subClassOf,uri_owl_AnnotationProperty,X0)
| ~ ic(X0) ) ).
cnf(u1213,axiom,
( iodp(sK13(uri_owl_DatatypeProperty,X0))
| iext(uri_rdfs_subClassOf,uri_owl_DatatypeProperty,X0)
| ~ ic(X0) ) ).
cnf(u1222,axiom,
( ioxp(sK13(uri_owl_OntologyProperty,X0))
| iext(uri_rdfs_subClassOf,uri_owl_OntologyProperty,X0)
| ~ ic(X0) ) ).
cnf(u1234,axiom,
( ix(sK13(uri_owl_Ontology,X0))
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0)
| ~ ic(X0) ) ).
cnf(u1416,axiom,
iext(uri_owl_unionOf,uri_rdf_XMLLiteral,uri_rdf_nil) ).
cnf(u1426,axiom,
icext(uri_rdfs_Container,sK4(uri_rdfs_Seq)) ).
cnf(u1435,axiom,
icext(uri_rdf_Property,sK4(uri_rdfs_ContainerMembershipProperty)) ).
cnf(u1438,axiom,
~ iext(uri_owl_unionOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_nil) ).
cnf(u1444,axiom,
iext(uri_rdfs_subPropertyOf,sK4(uri_rdfs_ContainerMembershipProperty),uri_rdfs_member) ).
cnf(u1449,axiom,
icext(uri_rdfs_Container,sK4(uri_rdf_Bag)) ).
cnf(u1462,axiom,
iext(uri_owl_unionOf,uri_rdf_Alt,uri_rdf_nil) ).
cnf(u1467,axiom,
lv(sK4(uri_rdfs_Literal)) ).
cnf(u1476,axiom,
ip(sK4(uri_rdf_Property)) ).
cnf(u1485,axiom,
icext(uri_rdfs_Class,sK4(uri_rdfs_Datatype)) ).
cnf(u1488,axiom,
~ iext(uri_owl_unionOf,uri_rdfs_Datatype,uri_rdf_nil) ).
cnf(u1494,axiom,
idc(sK4(uri_rdfs_Datatype)) ).
cnf(u1499,axiom,
iext(uri_rdfs_subClassOf,sK4(uri_rdfs_Datatype),uri_rdfs_Literal) ).
cnf(u1504,axiom,
ic(sK4(uri_rdfs_Class)) ).
cnf(u1507,axiom,
~ iext(uri_owl_unionOf,uri_rdfs_Class,uri_rdf_nil) ).
cnf(u1513,axiom,
ix(sK4(uri_owl_Ontology)) ).
cnf(u1526,axiom,
iext(uri_owl_unionOf,uri_owl_OntologyProperty,uri_rdf_nil) ).
cnf(u1535,axiom,
iext(uri_owl_unionOf,uri_owl_DatatypeProperty,uri_rdf_nil) ).
cnf(u1544,axiom,
iext(uri_owl_unionOf,uri_owl_AnnotationProperty,uri_rdf_nil) ).
cnf(u1685,axiom,
iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,uri_rdf_type) ).
cnf(u1703,axiom,
iext(uri_owl_unionOf,sK4(uri_rdfs_Datatype),uri_rdf_nil) ).
cnf(u1814,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Literal) ).
cnf(u1916,axiom,
iext(uri_rdfs_subClassOf,uri_owl_OntologyProperty,uri_rdfs_Resource) ).
cnf(u1921,axiom,
iext(uri_rdfs_subClassOf,uri_owl_OntologyProperty,uri_owl_Thing) ).
cnf(u1926,axiom,
iext(uri_rdfs_subClassOf,uri_owl_OntologyProperty,uri_rdfs_Literal) ).
cnf(u2080,axiom,
icext(uri_rdfs_Class,uri_rdf_Alt) ).
cnf(u2085,axiom,
icext(uri_rdfs_Class,uri_owl_OntologyProperty) ).
cnf(u2093,axiom,
icext(uri_rdfs_Class,uri_owl_Nothing) ).
cnf(u2164,axiom,
icext(uri_rdfs_Class,uri_rdfs_Literal) ).
cnf(u2169,axiom,
icext(uri_rdfs_Class,uri_rdfs_Class) ).
cnf(u2229,axiom,
icext(uri_rdfs_Class,uri_owl_DatatypeProperty) ).
cnf(u2234,axiom,
iext(uri_rdfs_subClassOf,uri_owl_DatatypeProperty,uri_owl_Thing) ).
cnf(u2239,axiom,
iext(uri_rdfs_subClassOf,uri_owl_DatatypeProperty,uri_rdfs_Resource) ).
cnf(u2244,axiom,
iext(uri_rdfs_subClassOf,uri_owl_DatatypeProperty,uri_rdfs_Literal) ).
cnf(u2379,axiom,
icext(uri_rdfs_Class,uri_owl_Restriction) ).
cnf(u2399,axiom,
icext(uri_rdfs_Class,uri_rdfs_Container) ).
cnf(u2472,axiom,
icext(uri_rdfs_Class,uri_owl_AnnotationProperty) ).
cnf(u2477,axiom,
iext(uri_rdfs_subClassOf,uri_owl_AnnotationProperty,uri_owl_Thing) ).
cnf(u2482,axiom,
iext(uri_rdfs_subClassOf,uri_owl_AnnotationProperty,uri_rdfs_Resource) ).
cnf(u2487,axiom,
iext(uri_rdfs_subClassOf,uri_owl_AnnotationProperty,uri_rdfs_Literal) ).
cnf(u2650,axiom,
iext(uri_owl_intersectionOf,uri_rdf_Property,uri_rdf_nil) ).
cnf(u2659,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Class,uri_rdf_nil) ).
cnf(u2703,axiom,
( iext(uri_rdfs_range,X0,uri_owl_Thing)
| ~ ip(X0) ) ).
cnf(u2706,axiom,
ip(uri_owl_Thing) ).
cnf(u2914,axiom,
( ~ ic(X0)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_Property) ) ).
cnf(u2927,axiom,
iext(uri_rdfs_domain,X0,uri_rdf_Property) ).
cnf(u4274,axiom,
iext(uri_rdfs_member,sK9(sK4(uri_rdfs_ContainerMembershipProperty),uri_owl_Nothing),sK10(sK4(uri_rdfs_ContainerMembershipProperty),uri_owl_Nothing)) ).
cnf(u4287,axiom,
iext(uri_rdfs_domain,uri_rdf_predicate,uri_owl_Nothing) ).
cnf(u4292,axiom,
icext(uri_rdfs_Literal,sK10(uri_rdfs_label,uri_owl_Nothing)) ).
cnf(u4305,axiom,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_owl_Nothing) ).
cnf(u4310,axiom,
icext(uri_rdfs_Literal,sK10(uri_rdfs_comment,uri_owl_Nothing)) ).
cnf(u4319,axiom,
icext(uri_rdfs_Statement,sK9(uri_rdf_subject,uri_owl_Nothing)) ).
cnf(u4328,axiom,
icext(uri_rdfs_Statement,sK9(uri_rdf_object,uri_owl_Nothing)) ).
cnf(u4332,axiom,
iext(uri_rdfs_domain,uri_rdf_object,uri_owl_Nothing) ).
cnf(u4341,axiom,
iext(uri_rdfs_domain,uri_rdf__3,uri_owl_Nothing) ).
cnf(u4346,axiom,
iext(uri_rdfs_member,sK9(uri_rdf__2,uri_owl_Nothing),sK10(uri_rdf__2,uri_owl_Nothing)) ).
cnf(u4355,axiom,
iext(uri_rdfs_member,sK9(uri_rdf__1,uri_owl_Nothing),sK10(uri_rdf__1,uri_owl_Nothing)) ).
cnf(u4363,axiom,
( iext(sK10(uri_rdfs_subPropertyOf,uri_owl_Nothing),X0,X1)
| ~ iext(sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing),X0,X1) ) ).
cnf(u4366,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_owl_Nothing) ).
cnf(u4371,axiom,
( iext(uri_rdfs_subPropertyOf,X0,sK10(uri_rdfs_subPropertyOf,uri_owl_Nothing))
| ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing)) ) ).
cnf(u4375,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_owl_Nothing))
| iext(uri_rdfs_subClassOf,X0,sK10(uri_rdfs_subClassOf,uri_owl_Nothing)) ) ).
cnf(u4378,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_owl_Nothing) ).
cnf(u4383,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,uri_owl_Nothing),X0)
| icext(sK10(uri_rdfs_subClassOf,uri_owl_Nothing),X0) ) ).
cnf(u4387,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_owl_Nothing),X1,X0)
| icext(sK10(uri_rdfs_range,uri_owl_Nothing),X0) ) ).
cnf(u4395,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_owl_Nothing),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_owl_Nothing),X0) ) ).
cnf(u4408,axiom,
iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_owl_Nothing) ).
cnf(u4429,axiom,
iext(uri_rdfs_domain,uri_owl_onProperty,uri_owl_Nothing) ).
cnf(u4458,axiom,
iext(uri_rdfs_domain,uri_owl_hasValue,uri_owl_Nothing) ).
cnf(u4463,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_allValuesFrom,uri_owl_Nothing)) ).
cnf(u4472,axiom,
icext(sK10(uri_rdf_type,uri_owl_Nothing),sK9(uri_rdf_type,uri_owl_Nothing)) ).
cnf(u4481,axiom,
icext(uri_rdf_List,sK10(uri_owl_unionOf,uri_owl_Nothing)) ).
cnf(u4484,axiom,
~ iext(uri_rdfs_domain,uri_owl_unionOf,uri_owl_Nothing) ).
cnf(u4494,axiom,
iext(uri_rdfs_domain,uri_rdf_rest,uri_owl_Nothing) ).
cnf(u4508,axiom,
iext(uri_rdfs_domain,uri_rdf_first,uri_owl_Nothing) ).
cnf(u4513,axiom,
icext(uri_rdf_List,sK10(uri_owl_intersectionOf,uri_owl_Nothing)) ).
cnf(u4525,axiom,
iext(uri_rdfs_domain,uri_owl_complementOf,uri_owl_Nothing) ).
cnf(u5076,axiom,
iext(uri_owl_unionOf,sK9(uri_rdfs_subClassOf,uri_owl_Nothing),uri_rdf_nil) ).
cnf(u5308,axiom,
iext(uri_rdfs_member,sK9(sK4(uri_rdfs_ContainerMembershipProperty),uri_owl_Thing),sK10(sK4(uri_rdfs_ContainerMembershipProperty),uri_owl_Thing)) ).
cnf(u5321,axiom,
iext(uri_rdfs_domain,uri_rdfs_label,uri_owl_Thing) ).
cnf(u5326,axiom,
icext(uri_rdfs_Literal,sK10(uri_rdfs_comment,uri_owl_Thing)) ).
cnf(u5339,axiom,
iext(uri_rdfs_domain,uri_rdf_subject,uri_owl_Thing) ).
cnf(u5344,axiom,
icext(uri_rdfs_Statement,sK9(uri_rdf_object,uri_owl_Thing)) ).
cnf(u5348,axiom,
iext(uri_rdfs_domain,uri_rdf_object,uri_owl_Thing) ).
cnf(u5353,axiom,
iext(uri_rdfs_member,sK9(uri_rdf__2,uri_owl_Thing),sK10(uri_rdf__2,uri_owl_Thing)) ).
cnf(u5362,axiom,
iext(uri_rdfs_member,sK9(uri_rdf__1,uri_owl_Thing),sK10(uri_rdf__1,uri_owl_Thing)) ).
cnf(u5374,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_owl_Thing) ).
cnf(u5386,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_owl_Thing) ).
cnf(u5398,axiom,
iext(uri_rdfs_domain,uri_rdfs_range,uri_owl_Thing) ).
cnf(u5402,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_owl_Thing),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_owl_Thing),X0) ) ).
cnf(u5415,axiom,
iext(uri_rdfs_domain,uri_owl_allValuesFrom,uri_owl_Thing) ).
cnf(u5424,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_owl_Thing) ).
cnf(u5429,axiom,
icext(uri_rdf_List,sK10(uri_owl_unionOf,uri_owl_Thing)) ).
cnf(u5438,axiom,
icext(uri_rdf_List,sK10(uri_owl_intersectionOf,uri_owl_Thing)) ).
cnf(u5490,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_Nothing),uri_owl_Thing) ).
cnf(u5503,axiom,
icext(sK10(uri_rdfs_range,uri_owl_Nothing),sK10(sK9(uri_rdfs_range,uri_owl_Nothing),uri_owl_Nothing)) ).
cnf(u5515,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Nothing),uri_owl_Thing) ).
cnf(u5528,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK9(sK9(uri_rdfs_domain,uri_owl_Nothing),uri_owl_Nothing)) ).
cnf(u5540,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Thing),uri_owl_Thing) ).
cnf(u5553,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Thing),sK9(sK9(uri_rdfs_domain,uri_owl_Thing),uri_owl_Nothing)) ).
cnf(u5624,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Thing),sK9(sK9(uri_rdfs_domain,uri_owl_Thing),uri_rdfs_Datatype)) ).
cnf(u5637,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Nothing),uri_rdfs_Datatype) ).
cnf(u5642,axiom,
icext(sK10(uri_rdfs_range,uri_owl_Nothing),sK10(sK9(uri_rdfs_range,uri_owl_Nothing),uri_rdfs_Datatype)) ).
cnf(u5655,axiom,
iext(uri_rdfs_domain,sK4(uri_rdfs_ContainerMembershipProperty),uri_rdfs_Datatype) ).
cnf(u5660,axiom,
icext(uri_rdfs_Literal,sK10(uri_rdfs_label,uri_rdfs_Datatype)) ).
cnf(u5669,axiom,
icext(uri_rdfs_Literal,sK10(uri_rdfs_comment,uri_rdfs_Datatype)) ).
cnf(u5678,axiom,
icext(uri_rdfs_Statement,sK9(uri_rdf_subject,uri_rdfs_Datatype)) ).
cnf(u5691,axiom,
iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Datatype) ).
cnf(u5696,axiom,
iext(uri_rdfs_member,sK9(uri_rdf__2,uri_rdfs_Datatype),sK10(uri_rdf__2,uri_rdfs_Datatype)) ).
cnf(u5705,axiom,
iext(uri_rdfs_member,sK9(uri_rdf__1,uri_rdfs_Datatype),sK10(uri_rdf__1,uri_rdfs_Datatype)) ).
cnf(u5717,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdfs_Datatype) ).
cnf(u5729,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Datatype) ).
cnf(u5737,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdfs_Datatype),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdfs_Datatype),X0) ) ).
cnf(u5749,axiom,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdfs_Datatype) ).
cnf(u5754,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_allValuesFrom,uri_rdfs_Datatype)) ).
cnf(u5767,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Datatype) ).
cnf(u5776,axiom,
iext(uri_rdfs_domain,uri_owl_unionOf,uri_rdfs_Datatype) ).
cnf(u5781,axiom,
icext(uri_rdf_List,sK10(uri_owl_intersectionOf,uri_rdfs_Datatype)) ).
cnf(u5915,axiom,
iext(uri_owl_unionOf,uri_rdf__1,uri_rdf_nil) ).
cnf(u5935,axiom,
iext(uri_owl_unionOf,uri_rdf__2,uri_rdf_nil) ).
cnf(u6121,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Datatype),uri_owl_Thing) ).
cnf(u6134,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Datatype),sK10(sK9(uri_rdfs_range,uri_rdfs_Datatype),uri_owl_Nothing)) ).
cnf(u6178,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Datatype),uri_rdf_List) ).
cnf(u6187,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Thing),uri_rdf_List) ).
cnf(u6192,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK9(sK9(uri_rdfs_domain,uri_owl_Nothing),uri_rdf_List)) ).
cnf(u6205,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_Nothing),uri_rdf_List) ).
cnf(u6210,axiom,
iext(uri_rdfs_member,sK9(sK4(uri_rdfs_ContainerMembershipProperty),uri_rdf_List),sK10(sK4(uri_rdfs_ContainerMembershipProperty),uri_rdf_List)) ).
cnf(u6219,axiom,
icext(uri_rdfs_Statement,sK9(uri_rdf_subject,uri_rdf_List)) ).
cnf(u6228,axiom,
iext(uri_rdfs_member,sK9(uri_rdf__2,uri_rdf_List),sK10(uri_rdf__2,uri_rdf_List)) ).
cnf(u6241,axiom,
iext(uri_rdfs_domain,uri_rdf__1,uri_rdf_List) ).
cnf(u6249,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_List) ).
cnf(u6261,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdf_List) ).
cnf(u6273,axiom,
iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_List) ).
cnf(u6281,axiom,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_List) ).
cnf(u6290,axiom,
iext(uri_rdfs_domain,uri_owl_allValuesFrom,uri_rdf_List) ).
cnf(u6299,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdf_List) ).
cnf(u6308,axiom,
iext(uri_rdfs_domain,uri_owl_unionOf,uri_rdf_List) ).
cnf(u6313,axiom,
icext(uri_rdf_List,sK10(uri_owl_intersectionOf,uri_rdf_List)) ).
cnf(u6428,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Datatype),uri_rdf_Alt) ).
cnf(u6437,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Thing),uri_rdf_Alt) ).
cnf(u6442,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK9(sK9(uri_rdfs_domain,uri_owl_Nothing),uri_rdf_Alt)) ).
cnf(u6455,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_Nothing),uri_rdf_Alt) ).
cnf(u6460,axiom,
iext(uri_rdfs_member,sK9(sK4(uri_rdfs_ContainerMembershipProperty),uri_rdf_Alt),sK10(sK4(uri_rdfs_ContainerMembershipProperty),uri_rdf_Alt)) ).
cnf(u6469,axiom,
icext(uri_rdfs_Statement,sK9(uri_rdf_subject,uri_rdf_Alt)) ).
cnf(u6478,axiom,
iext(uri_rdfs_member,sK9(uri_rdf__2,uri_rdf_Alt),sK10(uri_rdf__2,uri_rdf_Alt)) ).
cnf(u6491,axiom,
iext(uri_rdfs_domain,uri_rdf__1,uri_rdf_Alt) ).
cnf(u6495,axiom,
( iext(sK10(uri_rdfs_subPropertyOf,uri_rdf_Alt),X0,X1)
| ~ iext(sK9(uri_rdfs_subPropertyOf,uri_rdf_Alt),X0,X1) ) ).
cnf(u6498,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Alt) ).
cnf(u6503,axiom,
( iext(uri_rdfs_subPropertyOf,X0,sK10(uri_rdfs_subPropertyOf,uri_rdf_Alt))
| ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_rdf_Alt)) ) ).
cnf(u6507,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,uri_rdf_Alt),X0)
| icext(sK10(uri_rdfs_subClassOf,uri_rdf_Alt),X0) ) ).
cnf(u6510,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdf_Alt) ).
cnf(u6515,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_rdf_Alt))
| iext(uri_rdfs_subClassOf,X0,sK10(uri_rdfs_subClassOf,uri_rdf_Alt)) ) ).
cnf(u6519,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdf_Alt),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdf_Alt),X0) ) ).
cnf(u6522,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Alt) ).
cnf(u6527,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdf_Alt),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdf_Alt),X0) ) ).
cnf(u6530,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Alt) ).
cnf(u6540,axiom,
iext(uri_rdfs_domain,uri_owl_allValuesFrom,uri_rdf_Alt) ).
cnf(u6545,axiom,
icext(sK10(uri_rdf_type,uri_rdf_Alt),sK9(uri_rdf_type,uri_rdf_Alt)) ).
cnf(u7466,axiom,
iext(uri_owl_unionOf,sK9(uri_rdfs_subClassOf,uri_rdf_Alt),uri_rdf_nil) ).
cnf(u7610,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_Alt),uri_rdf_Alt) ).
cnf(u7623,axiom,
icext(sK10(uri_rdfs_range,uri_rdf_Alt),sK10(sK9(uri_rdfs_range,uri_rdf_Alt),uri_owl_Thing)) ).
cnf(u7632,axiom,
icext(sK10(uri_rdfs_range,uri_rdf_Alt),sK10(sK9(uri_rdfs_range,uri_rdf_Alt),uri_owl_Nothing)) ).
cnf(u7676,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_Alt),uri_rdf_Alt) ).
cnf(u7689,axiom,
icext(sK10(uri_rdfs_domain,uri_rdf_Alt),sK9(sK9(uri_rdfs_domain,uri_rdf_Alt),uri_owl_Thing)) ).
cnf(u7698,axiom,
icext(sK10(uri_rdfs_domain,uri_rdf_Alt),sK9(sK9(uri_rdfs_domain,uri_rdf_Alt),uri_owl_Nothing)) ).
cnf(u7806,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK9(sK9(uri_rdfs_domain,uri_owl_Nothing),uri_rdfs_Container)) ).
cnf(u7819,axiom,
iext(uri_rdfs_domain,sK4(uri_rdfs_ContainerMembershipProperty),uri_rdfs_Container) ).
cnf(u7824,axiom,
icext(uri_rdfs_Statement,sK9(uri_rdf_subject,uri_rdfs_Container)) ).
cnf(u7837,axiom,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Container) ).
cnf(u7845,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdfs_Container) ).
cnf(u7857,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Container) ).
cnf(u7865,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdfs_Container),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdfs_Container),X0) ) ).
cnf(u7873,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdfs_Container),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdfs_Container),X0) ) ).
cnf(u7882,axiom,
icext(sK10(uri_rdf_type,uri_rdfs_Container),sK9(uri_rdf_type,uri_rdfs_Container)) ).
cnf(u7972,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Container),uri_rdf_Alt) ).
cnf(u7985,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Container),sK10(sK9(uri_rdfs_range,uri_rdfs_Container),uri_owl_Thing)) ).
cnf(u7994,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Container),sK10(sK9(uri_rdfs_range,uri_rdfs_Container),uri_owl_Nothing)) ).
cnf(u8038,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Container),uri_rdf_Alt) ).
cnf(u8051,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Container),sK9(sK9(uri_rdfs_domain,uri_rdfs_Container),uri_owl_Thing)) ).
cnf(u8060,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Container),sK9(sK9(uri_rdfs_domain,uri_rdfs_Container),uri_owl_Nothing)) ).
cnf(u8135,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK9(sK9(uri_rdfs_domain,uri_owl_Nothing),uri_rdf_Bag)) ).
cnf(u8148,axiom,
iext(uri_rdfs_domain,sK4(uri_rdfs_ContainerMembershipProperty),uri_rdf_Bag) ).
cnf(u8153,axiom,
icext(uri_rdfs_Statement,sK9(uri_rdf_subject,uri_rdf_Bag)) ).
cnf(u8166,axiom,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdf_Bag) ).
cnf(u8174,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Bag) ).
cnf(u8186,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdf_Bag) ).
cnf(u8194,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdf_Bag),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdf_Bag),X0) ) ).
cnf(u8202,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdf_Bag),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdf_Bag),X0) ) ).
cnf(u8211,axiom,
icext(sK10(uri_rdf_type,uri_rdf_Bag),sK9(uri_rdf_type,uri_rdf_Bag)) ).
cnf(u8305,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_Bag),uri_rdf_Alt) ).
cnf(u8318,axiom,
icext(sK10(uri_rdfs_range,uri_rdf_Bag),sK10(sK9(uri_rdfs_range,uri_rdf_Bag),uri_owl_Thing)) ).
cnf(u8327,axiom,
icext(sK10(uri_rdfs_range,uri_rdf_Bag),sK10(sK9(uri_rdfs_range,uri_rdf_Bag),uri_owl_Nothing)) ).
cnf(u8373,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_Bag),uri_rdf_Alt) ).
cnf(u8386,axiom,
icext(sK10(uri_rdfs_domain,uri_rdf_Bag),sK9(sK9(uri_rdfs_domain,uri_rdf_Bag),uri_owl_Thing)) ).
cnf(u8395,axiom,
icext(sK10(uri_rdfs_domain,uri_rdf_Bag),sK9(sK9(uri_rdfs_domain,uri_rdf_Bag),uri_owl_Nothing)) ).
cnf(u8476,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK9(sK9(uri_rdfs_domain,uri_owl_Nothing),uri_rdfs_ContainerMembershipProperty)) ).
cnf(u8489,axiom,
iext(uri_rdfs_domain,sK4(uri_rdfs_ContainerMembershipProperty),uri_rdfs_ContainerMembershipProperty) ).
cnf(u8494,axiom,
icext(uri_rdfs_Statement,sK9(uri_rdf_subject,uri_rdfs_ContainerMembershipProperty)) ).
cnf(u8507,axiom,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_ContainerMembershipProperty) ).
cnf(u8515,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdfs_ContainerMembershipProperty) ).
cnf(u8527,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty) ).
cnf(u8535,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X0) ) ).
cnf(u8543,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),X0) ) ).
cnf(u8552,axiom,
icext(sK10(uri_rdf_type,uri_rdfs_ContainerMembershipProperty),sK9(uri_rdf_type,uri_rdfs_ContainerMembershipProperty)) ).
cnf(u8998,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),uri_rdf_Alt) ).
cnf(u9011,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),sK10(sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),uri_owl_Thing)) ).
cnf(u9020,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),sK10(sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),uri_owl_Nothing)) ).
cnf(u9068,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),uri_rdf_Alt) ).
cnf(u9081,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),sK9(sK9(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),uri_owl_Thing)) ).
cnf(u9090,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),sK9(sK9(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),uri_owl_Nothing)) ).
cnf(u9175,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK9(sK9(uri_rdfs_domain,uri_owl_Nothing),uri_rdfs_Seq)) ).
cnf(u9188,axiom,
iext(uri_rdfs_domain,sK4(uri_rdfs_ContainerMembershipProperty),uri_rdfs_Seq) ).
cnf(u9193,axiom,
icext(uri_rdfs_Statement,sK9(uri_rdf_subject,uri_rdfs_Seq)) ).
cnf(u9206,axiom,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Seq) ).
cnf(u9214,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdfs_Seq) ).
cnf(u9226,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Seq) ).
cnf(u9234,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdfs_Seq),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdfs_Seq),X0) ) ).
cnf(u9242,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdfs_Seq),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdfs_Seq),X0) ) ).
cnf(u9251,axiom,
icext(sK10(uri_rdf_type,uri_rdfs_Seq),sK9(uri_rdf_type,uri_rdfs_Seq)) ).
cnf(u9362,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Seq),uri_rdf_Alt) ).
cnf(u9375,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Seq),sK10(sK9(uri_rdfs_range,uri_rdfs_Seq),uri_owl_Thing)) ).
cnf(u9384,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Seq),sK10(sK9(uri_rdfs_range,uri_rdfs_Seq),uri_owl_Nothing)) ).
cnf(u9432,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Seq),uri_rdf_Alt) ).
cnf(u9445,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Seq),sK9(sK9(uri_rdfs_domain,uri_rdfs_Seq),uri_owl_Thing)) ).
cnf(u9454,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Seq),sK9(sK9(uri_rdfs_domain,uri_rdfs_Seq),uri_owl_Nothing)) ).
cnf(u9541,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK9(sK9(uri_rdfs_domain,uri_owl_Nothing),uri_rdf_XMLLiteral)) ).
cnf(u9554,axiom,
iext(uri_rdfs_domain,sK4(uri_rdfs_ContainerMembershipProperty),uri_rdf_XMLLiteral) ).
cnf(u9559,axiom,
icext(uri_rdfs_Statement,sK9(uri_rdf_subject,uri_rdf_XMLLiteral)) ).
cnf(u9572,axiom,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdf_XMLLiteral) ).
cnf(u9576,axiom,
( iext(sK10(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral),X0,X1)
| ~ iext(sK9(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral),X0,X1) ) ).
cnf(u9579,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral) ).
cnf(u9584,axiom,
( iext(uri_rdfs_subPropertyOf,X0,sK10(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral))
| ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral)) ) ).
cnf(u9588,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,uri_rdf_XMLLiteral),X0)
| icext(sK10(uri_rdfs_subClassOf,uri_rdf_XMLLiteral),X0) ) ).
cnf(u9591,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdf_XMLLiteral) ).
cnf(u9596,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_rdf_XMLLiteral))
| iext(uri_rdfs_subClassOf,X0,sK10(uri_rdfs_subClassOf,uri_rdf_XMLLiteral)) ) ).
cnf(u9600,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdf_XMLLiteral),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdf_XMLLiteral),X0) ) ).
cnf(u9608,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdf_XMLLiteral),X0) ) ).
cnf(u9617,axiom,
icext(sK10(uri_rdf_type,uri_rdf_XMLLiteral),sK9(uri_rdf_type,uri_rdf_XMLLiteral)) ).
cnf(u10403,axiom,
iext(uri_owl_unionOf,sK9(uri_rdfs_subClassOf,uri_rdf_XMLLiteral),uri_rdf_nil) ).
cnf(u10564,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_XMLLiteral),uri_rdf_XMLLiteral) ).
cnf(u10577,axiom,
icext(sK10(uri_rdfs_range,uri_rdf_XMLLiteral),sK10(sK9(uri_rdfs_range,uri_rdf_XMLLiteral),uri_rdf_Alt)) ).
cnf(u10586,axiom,
icext(sK10(uri_rdfs_range,uri_rdf_XMLLiteral),sK10(sK9(uri_rdfs_range,uri_rdf_XMLLiteral),uri_owl_Thing)) ).
cnf(u10595,axiom,
icext(sK10(uri_rdfs_range,uri_rdf_XMLLiteral),sK10(sK9(uri_rdfs_range,uri_rdf_XMLLiteral),uri_owl_Nothing)) ).
cnf(u10652,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),uri_rdf_XMLLiteral) ).
cnf(u10665,axiom,
icext(sK10(uri_rdfs_domain,uri_rdf_XMLLiteral),sK9(sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),uri_rdf_Alt)) ).
cnf(u10674,axiom,
icext(sK10(uri_rdfs_domain,uri_rdf_XMLLiteral),sK9(sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),uri_owl_Thing)) ).
cnf(u10683,axiom,
icext(sK10(uri_rdfs_domain,uri_rdf_XMLLiteral),sK9(sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),uri_owl_Nothing)) ).
cnf(u10862,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK9(sK9(uri_rdfs_domain,uri_owl_Nothing),uri_rdfs_Statement)) ).
cnf(u10874,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdfs_Statement) ).
cnf(u10886,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Statement) ).
cnf(u10894,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdfs_Statement),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdfs_Statement),X0) ) ).
cnf(u10902,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdfs_Statement),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdfs_Statement),X0) ) ).
cnf(u10911,axiom,
icext(sK10(uri_rdf_type,uri_rdfs_Statement),sK9(uri_rdf_type,uri_rdfs_Statement)) ).
cnf(u11034,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Statement),uri_rdf_XMLLiteral) ).
cnf(u11047,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Statement),sK10(sK9(uri_rdfs_range,uri_rdfs_Statement),uri_rdf_Alt)) ).
cnf(u11056,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Statement),sK10(sK9(uri_rdfs_range,uri_rdfs_Statement),uri_owl_Thing)) ).
cnf(u11065,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Statement),sK10(sK9(uri_rdfs_range,uri_rdfs_Statement),uri_owl_Nothing)) ).
cnf(u11120,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Statement),uri_rdf_XMLLiteral) ).
cnf(u11133,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Statement),sK9(sK9(uri_rdfs_domain,uri_rdfs_Statement),uri_rdf_Alt)) ).
cnf(u11142,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Statement),sK9(sK9(uri_rdfs_domain,uri_rdfs_Statement),uri_owl_Thing)) ).
cnf(u11151,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Statement),sK9(sK9(uri_rdfs_domain,uri_rdfs_Statement),uri_owl_Nothing)) ).
cnf(u11812,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK9(sK9(uri_rdfs_domain,uri_owl_Nothing),uri_owl_AnnotationProperty)) ).
cnf(u11820,axiom,
( iext(sK10(uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty),X0,X1)
| ~ iext(sK9(uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty),X0,X1) ) ).
cnf(u11823,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty) ).
cnf(u11828,axiom,
( iext(uri_rdfs_subPropertyOf,X0,sK10(uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty))
| ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty)) ) ).
cnf(u11832,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,uri_owl_AnnotationProperty),X0)
| icext(sK10(uri_rdfs_subClassOf,uri_owl_AnnotationProperty),X0) ) ).
cnf(u11835,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_owl_AnnotationProperty) ).
cnf(u11840,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_owl_AnnotationProperty))
| iext(uri_rdfs_subClassOf,X0,sK10(uri_rdfs_subClassOf,uri_owl_AnnotationProperty)) ) ).
cnf(u11844,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_owl_AnnotationProperty),X1,X0)
| icext(sK10(uri_rdfs_range,uri_owl_AnnotationProperty),X0) ) ).
cnf(u11852,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_owl_AnnotationProperty),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_owl_AnnotationProperty),X0) ) ).
cnf(u11861,axiom,
icext(sK10(uri_rdf_type,uri_owl_AnnotationProperty),sK9(uri_rdf_type,uri_owl_AnnotationProperty)) ).
cnf(u12663,axiom,
iext(uri_owl_unionOf,sK9(uri_rdfs_subClassOf,uri_owl_AnnotationProperty),uri_rdf_nil) ).
cnf(u12883,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_AnnotationProperty),uri_rdf_XMLLiteral) ).
cnf(u12896,axiom,
icext(sK10(uri_rdfs_range,uri_owl_AnnotationProperty),sK10(sK9(uri_rdfs_range,uri_owl_AnnotationProperty),uri_rdf_Alt)) ).
cnf(u12901,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_AnnotationProperty),uri_owl_AnnotationProperty) ).
cnf(u12914,axiom,
icext(sK10(uri_rdfs_range,uri_owl_AnnotationProperty),sK10(sK9(uri_rdfs_range,uri_owl_AnnotationProperty),uri_owl_Thing)) ).
cnf(u12923,axiom,
icext(sK10(uri_rdfs_range,uri_owl_AnnotationProperty),sK10(sK9(uri_rdfs_range,uri_owl_AnnotationProperty),uri_owl_Nothing)) ).
cnf(u12986,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_AnnotationProperty),uri_rdf_XMLLiteral) ).
cnf(u12999,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_AnnotationProperty),sK9(sK9(uri_rdfs_domain,uri_owl_AnnotationProperty),uri_rdf_Alt)) ).
cnf(u13004,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_AnnotationProperty),uri_owl_AnnotationProperty) ).
cnf(u13017,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_AnnotationProperty),sK9(sK9(uri_rdfs_domain,uri_owl_AnnotationProperty),uri_owl_Thing)) ).
cnf(u13026,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_AnnotationProperty),sK9(sK9(uri_rdfs_domain,uri_owl_AnnotationProperty),uri_owl_Nothing)) ).
cnf(u13897,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK9(sK9(uri_rdfs_domain,uri_owl_Nothing),uri_owl_DatatypeProperty)) ).
cnf(u13905,axiom,
( iext(sK10(uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty),X0,X1)
| ~ iext(sK9(uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty),X0,X1) ) ).
cnf(u13908,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty) ).
cnf(u13913,axiom,
( iext(uri_rdfs_subPropertyOf,X0,sK10(uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty))
| ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty)) ) ).
cnf(u13917,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,uri_owl_DatatypeProperty),X0)
| icext(sK10(uri_rdfs_subClassOf,uri_owl_DatatypeProperty),X0) ) ).
cnf(u13920,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_owl_DatatypeProperty) ).
cnf(u13925,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_owl_DatatypeProperty))
| iext(uri_rdfs_subClassOf,X0,sK10(uri_rdfs_subClassOf,uri_owl_DatatypeProperty)) ) ).
cnf(u13929,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_owl_DatatypeProperty),X1,X0)
| icext(sK10(uri_rdfs_range,uri_owl_DatatypeProperty),X0) ) ).
cnf(u13937,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_owl_DatatypeProperty),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_owl_DatatypeProperty),X0) ) ).
cnf(u13946,axiom,
icext(sK10(uri_rdf_type,uri_owl_DatatypeProperty),sK9(uri_rdf_type,uri_owl_DatatypeProperty)) ).
cnf(u14756,axiom,
iext(uri_owl_unionOf,sK9(uri_rdfs_subClassOf,uri_owl_DatatypeProperty),uri_rdf_nil) ).
cnf(u15035,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_DatatypeProperty),uri_rdf_XMLLiteral) ).
cnf(u15048,axiom,
icext(sK10(uri_rdfs_range,uri_owl_DatatypeProperty),sK10(sK9(uri_rdfs_range,uri_owl_DatatypeProperty),uri_rdf_Alt)) ).
cnf(u15053,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_DatatypeProperty),uri_owl_DatatypeProperty) ).
cnf(u15066,axiom,
icext(sK10(uri_rdfs_range,uri_owl_DatatypeProperty),sK10(sK9(uri_rdfs_range,uri_owl_DatatypeProperty),uri_owl_AnnotationProperty)) ).
cnf(u15075,axiom,
icext(sK10(uri_rdfs_range,uri_owl_DatatypeProperty),sK10(sK9(uri_rdfs_range,uri_owl_DatatypeProperty),uri_owl_Thing)) ).
cnf(u15084,axiom,
icext(sK10(uri_rdfs_range,uri_owl_DatatypeProperty),sK10(sK9(uri_rdfs_range,uri_owl_DatatypeProperty),uri_owl_Nothing)) ).
cnf(u15151,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_DatatypeProperty),uri_rdf_XMLLiteral) ).
cnf(u15164,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_DatatypeProperty),sK9(sK9(uri_rdfs_domain,uri_owl_DatatypeProperty),uri_rdf_Alt)) ).
cnf(u15169,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_DatatypeProperty),uri_owl_DatatypeProperty) ).
cnf(u15182,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_DatatypeProperty),sK9(sK9(uri_rdfs_domain,uri_owl_DatatypeProperty),uri_owl_AnnotationProperty)) ).
cnf(u15191,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_DatatypeProperty),sK9(sK9(uri_rdfs_domain,uri_owl_DatatypeProperty),uri_owl_Thing)) ).
cnf(u15200,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_DatatypeProperty),sK9(sK9(uri_rdfs_domain,uri_owl_DatatypeProperty),uri_owl_Nothing)) ).
cnf(u16221,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK9(sK9(uri_rdfs_domain,uri_owl_Nothing),uri_owl_OntologyProperty)) ).
cnf(u16229,axiom,
( iext(sK10(uri_rdfs_subPropertyOf,uri_owl_OntologyProperty),X0,X1)
| ~ iext(sK9(uri_rdfs_subPropertyOf,uri_owl_OntologyProperty),X0,X1) ) ).
cnf(u16232,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_owl_OntologyProperty) ).
cnf(u16237,axiom,
( iext(uri_rdfs_subPropertyOf,X0,sK10(uri_rdfs_subPropertyOf,uri_owl_OntologyProperty))
| ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_owl_OntologyProperty)) ) ).
cnf(u16241,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,uri_owl_OntologyProperty),X0)
| icext(sK10(uri_rdfs_subClassOf,uri_owl_OntologyProperty),X0) ) ).
cnf(u16244,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_owl_OntologyProperty) ).
cnf(u16249,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_owl_OntologyProperty))
| iext(uri_rdfs_subClassOf,X0,sK10(uri_rdfs_subClassOf,uri_owl_OntologyProperty)) ) ).
cnf(u16253,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_owl_OntologyProperty),X1,X0)
| icext(sK10(uri_rdfs_range,uri_owl_OntologyProperty),X0) ) ).
cnf(u16261,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_owl_OntologyProperty),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_owl_OntologyProperty),X0) ) ).
cnf(u16270,axiom,
icext(sK10(uri_rdf_type,uri_owl_OntologyProperty),sK9(uri_rdf_type,uri_owl_OntologyProperty)) ).
cnf(u17130,axiom,
iext(uri_owl_unionOf,sK9(uri_rdfs_subClassOf,uri_owl_OntologyProperty),uri_rdf_nil) ).
cnf(u17426,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_OntologyProperty),uri_rdf_XMLLiteral) ).
cnf(u17439,axiom,
icext(sK10(uri_rdfs_range,uri_owl_OntologyProperty),sK10(sK9(uri_rdfs_range,uri_owl_OntologyProperty),uri_rdf_Alt)) ).
cnf(u17444,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_OntologyProperty),uri_owl_OntologyProperty) ).
cnf(u17457,axiom,
icext(sK10(uri_rdfs_range,uri_owl_OntologyProperty),sK10(sK9(uri_rdfs_range,uri_owl_OntologyProperty),uri_owl_DatatypeProperty)) ).
cnf(u17466,axiom,
icext(sK10(uri_rdfs_range,uri_owl_OntologyProperty),sK10(sK9(uri_rdfs_range,uri_owl_OntologyProperty),uri_owl_AnnotationProperty)) ).
cnf(u17475,axiom,
icext(sK10(uri_rdfs_range,uri_owl_OntologyProperty),sK10(sK9(uri_rdfs_range,uri_owl_OntologyProperty),uri_owl_Thing)) ).
cnf(u17484,axiom,
icext(sK10(uri_rdfs_range,uri_owl_OntologyProperty),sK10(sK9(uri_rdfs_range,uri_owl_OntologyProperty),uri_owl_Nothing)) ).
cnf(u17555,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_OntologyProperty),uri_rdf_XMLLiteral) ).
cnf(u17568,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_OntologyProperty),sK9(sK9(uri_rdfs_domain,uri_owl_OntologyProperty),uri_rdf_Alt)) ).
cnf(u17573,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_OntologyProperty),uri_owl_OntologyProperty) ).
cnf(u17586,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_OntologyProperty),sK9(sK9(uri_rdfs_domain,uri_owl_OntologyProperty),uri_owl_DatatypeProperty)) ).
cnf(u17595,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_OntologyProperty),sK9(sK9(uri_rdfs_domain,uri_owl_OntologyProperty),uri_owl_AnnotationProperty)) ).
cnf(u17604,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_OntologyProperty),sK9(sK9(uri_rdfs_domain,uri_owl_OntologyProperty),uri_owl_Thing)) ).
cnf(u17613,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_OntologyProperty),sK9(sK9(uri_rdfs_domain,uri_owl_OntologyProperty),uri_owl_Nothing)) ).
cnf(u2680,axiom,
( iext(uri_rdfs_domain,X0,uri_owl_Thing)
| ~ ip(X0) ) ).
cnf(u8819,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdf_Alt),X0) ).
cnf(u19696,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty),sK10(uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty)) ).
cnf(u8674,axiom,
iext(uri_rdfs_member,uri_owl_complementOf,X0) ).
cnf(u6382,axiom,
iext(uri_rdfs_domain,X0,uri_rdf_List) ).
cnf(u12940,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_owl_AnnotationProperty),X0) ).
cnf(u4547,axiom,
~ iext(uri_owl_onProperty,X0,X1) ).
cnf(u16210,axiom,
( icext(sK12(uri_rdfs_domain,X0),sK9(sK11(uri_rdfs_domain,X0),uri_owl_OntologyProperty))
| iext(uri_rdfs_domain,sK11(uri_rdfs_domain,X0),uri_owl_OntologyProperty)
| iext(uri_rdfs_range,uri_rdfs_domain,X0) ) ).
cnf(u18741,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Thing),X0) ).
cnf(u5941,axiom,
~ icext(uri_rdf__2,X0) ).
cnf(u8918,axiom,
( iext(uri_rdfs_member,X0,sK15(uri_rdfs_subClassOf,X1))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X1)
| ~ iext(uri_rdfs_subClassOf,X0,sK14(uri_rdfs_subClassOf,X1)) ) ).
cnf(u3241,axiom,
( iext(X0,sK9(X0,uri_owl_AnnotationProperty),sK10(X0,uri_owl_AnnotationProperty))
| iext(uri_rdfs_domain,X0,uri_owl_AnnotationProperty) ) ).
cnf(u18748,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_OntologyProperty),X0) ).
cnf(u2802,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Class) ).
cnf(u19374,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_owl_Nothing),sK10(uri_rdfs_domain,uri_owl_Nothing)) ).
cnf(u9389,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdfs_Seq),X0,X1) ).
cnf(u9801,axiom,
iext(uri_rdfs_range,sK4(uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u5193,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,uri_rdf_predicate)
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u387,axiom,
( ~ iext(uri_rdf_type,X0,X1)
| icext(X1,X0) ) ).
cnf(u314,axiom,
( iext(uri_rdf_type,X0,uri_rdfs_Literal)
| ~ lv(X0) ) ).
cnf(u5097,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u4539,axiom,
~ iext(uri_rdfs_isDefinedBy,X0,X1) ).
cnf(u6068,axiom,
( icext(sK12(uri_rdfs_subClassOf,X0),sK4(sK11(uri_rdfs_subClassOf,X0)))
| iext(uri_rdfs_range,uri_rdfs_subClassOf,X0)
| iext(uri_owl_unionOf,sK11(uri_rdfs_subClassOf,X0),uri_rdf_nil) ) ).
cnf(u6379,axiom,
iext(uri_owl_intersectionOf,uri_rdf_List,uri_rdf_nil) ).
cnf(u10696,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),X0) ).
cnf(u8804,axiom,
( iext(uri_rdfs_member,sK9(X0,uri_owl_Thing),sK10(X0,uri_owl_Thing))
| iext(uri_rdfs_domain,X0,uri_owl_Thing) ) ).
cnf(u9794,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf__2,X0) ).
cnf(u12954,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_range,uri_owl_AnnotationProperty))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u10425,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subClassOf,uri_rdf_XMLLiteral),X0) ).
cnf(u11209,axiom,
( iext(uri_rdfs_member,X0,sK10(uri_rdfs_subPropertyOf,uri_rdf_Alt))
| ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_rdf_Alt)) ) ).
cnf(u6937,axiom,
~ iext(sK9(uri_rdfs_range,uri_owl_Nothing),X0,X1) ).
cnf(u5990,axiom,
lv(X0) ).
cnf(u18730,axiom,
( iext(uri_rdfs_subPropertyOf,X1,sK10(uri_rdfs_subPropertyOf,X0))
| ~ iext(uri_rdfs_subPropertyOf,X1,sK9(uri_rdfs_subPropertyOf,X0))
| iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u10414,axiom,
iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,uri_rdf_XMLLiteral),X0) ).
cnf(u5946,axiom,
iext(uri_rdfs_subClassOf,uri_rdf__2,X0) ).
cnf(u17842,axiom,
( iext(uri_rdfs_member,X0,sK10(uri_rdfs_subPropertyOf,uri_owl_OntologyProperty))
| ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_owl_OntologyProperty)) ) ).
cnf(u9466,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdfs_Seq),X0) ).
cnf(u1048,axiom,
( iext(sK15(uri_rdfs_subPropertyOf,X0),sK14(sK14(uri_rdfs_subPropertyOf,X0),X1),sK15(sK14(uri_rdfs_subPropertyOf,X0),X1))
| ~ ip(X0)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0)
| ~ ip(X1)
| iext(uri_rdfs_subPropertyOf,sK14(uri_rdfs_subPropertyOf,X0),X1) ) ).
cnf(u11006,axiom,
iext(uri_rdfs_member,uri_rdfs_Statement,uri_rdf_nil) ).
cnf(u5109,axiom,
( iext(uri_rdfs_subClassOf,X0,sK15(uri_rdfs_subClassOf,X1))
| ~ iext(uri_rdfs_subClassOf,X0,sK14(uri_rdfs_subClassOf,X1))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X1) ) ).
cnf(u8693,axiom,
iext(uri_rdfs_member,uri_owl_Nothing,X0) ).
cnf(u7900,axiom,
( icext(sK15(uri_rdfs_range,X0),sK15(sK14(uri_rdfs_range,X0),X1))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0)
| iext(uri_rdfs_subPropertyOf,sK14(uri_rdfs_range,X0),X1) ) ).
cnf(u7709,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdf_Alt),X0) ).
cnf(u5826,axiom,
~ iext(uri_rdf_object,X0,X1) ).
cnf(u9534,axiom,
( icext(sK15(uri_rdfs_range,X0),sK10(sK14(uri_rdfs_range,X0),uri_rdf_XMLLiteral))
| iext(uri_rdfs_domain,sK14(uri_rdfs_range,X0),uri_rdf_XMLLiteral)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0) ) ).
cnf(u9463,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdfs_Seq),X0) ).
cnf(u19119,axiom,
( icext(sK10(uri_rdfs_range,X0),sK10(sK9(uri_rdfs_range,X0),X1))
| iext(uri_rdfs_domain,uri_rdfs_range,X0)
| iext(uri_rdfs_domain,sK9(uri_rdfs_range,X0),X1) ) ).
cnf(u5896,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype) ).
cnf(u8651,axiom,
iext(uri_rdfs_member,X0,uri_rdf_Property) ).
cnf(u18726,axiom,
( ~ iext(sK9(uri_rdfs_domain,X0),X1,X2)
| icext(sK10(uri_rdfs_domain,X0),X1)
| iext(uri_rdfs_domain,uri_rdfs_domain,X0) ) ).
cnf(u5186,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,uri_owl_hasValue)
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u8872,axiom,
( iext(uri_rdfs_member,sK14(X0,X1),sK15(X0,X1))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u8786,axiom,
iext(uri_rdfs_member,sK4(uri_rdfs_Datatype),X0) ).
cnf(u2773,axiom,
( ~ iext(sK11(uri_rdfs_domain,X0),X1,X2)
| icext(sK12(uri_rdfs_domain,X0),X1)
| iext(uri_rdfs_range,uri_rdfs_domain,X0) ) ).
cnf(u19712,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subPropertyOf,uri_owl_OntologyProperty),sK10(uri_rdfs_subPropertyOf,uri_owl_OntologyProperty)) ).
cnf(u8331,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdf_Bag),X0,X1) ).
cnf(u353,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,X1)
| iext(X1,X2,X3)
| ~ iext(X0,X2,X3) ) ).
cnf(u2614,axiom,
( ~ icext(X0,sK0(X0))
| ~ ic(X0)
| iext(uri_owl_intersectionOf,X0,uri_rdf_nil) ) ).
cnf(u300,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_OntologyProperty)
| ioxp(X0) ) ).
cnf(u5303,axiom,
( iext(sK15(uri_rdfs_subPropertyOf,X0),sK9(sK14(uri_rdfs_subPropertyOf,X0),uri_owl_Thing),sK10(sK14(uri_rdfs_subPropertyOf,X0),uri_owl_Thing))
| iext(uri_rdfs_domain,sK14(uri_rdfs_subPropertyOf,X0),uri_owl_Thing)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u8338,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdf_Bag),X0) ).
cnf(u17136,axiom,
~ icext(sK9(uri_rdfs_subClassOf,uri_owl_OntologyProperty),X0) ).
cnf(u18878,axiom,
( icext(sK10(uri_rdfs_subClassOf,X0),sK13(sK9(uri_rdfs_subClassOf,X0),X1))
| iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0)
| iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,X0),X1) ) ).
cnf(u406,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty) ).
cnf(u15409,axiom,
( iext(uri_rdfs_member,X0,sK10(uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty))
| ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty)) ) ).
cnf(u5188,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,uri_owl_someValuesFrom)
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u4562,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,X0) ).
cnf(u8655,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_Container) ).
cnf(u9338,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Seq,uri_rdf_nil) ).
cnf(u365,axiom,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List) ).
cnf(u18760,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),X0) ).
cnf(u296,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_DatatypeProperty)
| iodp(X0) ) ).
cnf(u15113,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_range,uri_owl_DatatypeProperty))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u18727,axiom,
( ~ iext(sK9(uri_rdfs_range,X0),X2,X1)
| icext(sK10(uri_rdfs_range,X0),X1)
| iext(uri_rdfs_domain,uri_rdfs_range,X0) ) ).
cnf(u8335,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdf_Bag),X0) ).
cnf(u6062,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Literal,uri_rdf_nil) ).
cnf(u9343,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_Seq) ).
cnf(u13040,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_owl_AnnotationProperty),X0) ).
cnf(u18753,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_Bag),X0) ).
cnf(u11206,axiom,
( ~ iext(sK9(uri_rdfs_subPropertyOf,uri_rdf_Alt),sK14(X0,sK10(uri_rdfs_subPropertyOf,uri_rdf_Alt)),sK15(X0,sK10(uri_rdfs_subPropertyOf,uri_rdf_Alt)))
| iext(uri_rdfs_subPropertyOf,X0,sK10(uri_rdfs_subPropertyOf,uri_rdf_Alt)) ) ).
cnf(u2754,axiom,
( iext(X0,sK11(X0,X1),sK12(X0,X1))
| iext(uri_rdfs_range,X0,X1) ) ).
cnf(u9095,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),X0,X1) ).
cnf(u6330,axiom,
( icext(sK12(uri_rdfs_range,X0),sK10(sK11(uri_rdfs_range,X0),uri_owl_Thing))
| iext(uri_rdfs_range,uri_rdfs_range,X0)
| iext(uri_rdfs_domain,sK11(uri_rdfs_range,X0),uri_owl_Thing) ) ).
cnf(u11208,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_rdf_Alt))
| iext(sK10(uri_rdfs_subPropertyOf,uri_rdf_Alt),X1,X2)
| ~ iext(X0,X1,X2) ) ).
cnf(u17618,axiom,
~ iext(sK9(uri_rdfs_domain,uri_owl_OntologyProperty),X0,X1) ).
cnf(u14762,axiom,
~ icext(sK9(uri_rdfs_subClassOf,uri_owl_DatatypeProperty),X0) ).
cnf(u19416,axiom,
( ~ icext(sK14(uri_rdfs_subClassOf,X0),X1)
| icext(sK15(uri_rdfs_subClassOf,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0) ) ).
cnf(u6087,axiom,
( icext(sK12(uri_rdfs_domain,X0),sK11(sK11(uri_rdfs_domain,X0),X1))
| iext(uri_rdfs_range,uri_rdfs_domain,X0)
| iext(uri_rdfs_range,sK11(uri_rdfs_domain,X0),X1) ) ).
cnf(u9099,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u5096,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_OntologyProperty)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u2777,axiom,
( iext(uri_rdfs_subPropertyOf,X1,sK12(uri_rdfs_subPropertyOf,X0))
| ~ iext(uri_rdfs_subPropertyOf,X1,sK11(uri_rdfs_subPropertyOf,X0))
| iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u4269,axiom,
( iext(sK15(uri_rdfs_subPropertyOf,X0),sK9(sK14(uri_rdfs_subPropertyOf,X0),uri_owl_Nothing),sK10(sK14(uri_rdfs_subPropertyOf,X0),uri_owl_Nothing))
| iext(uri_rdfs_domain,sK14(uri_rdfs_subPropertyOf,X0),uri_owl_Nothing)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u4712,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0) ).
cnf(u19677,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_rdf_Alt),sK10(uri_rdfs_subPropertyOf,uri_rdf_Alt)) ).
cnf(u8704,axiom,
iext(uri_rdfs_member,uri_owl_OntologyProperty,X0) ).
cnf(u3237,axiom,
( iext(X0,sK9(X0,uri_owl_Nothing),sK10(X0,uri_owl_Nothing))
| iext(uri_rdfs_domain,X0,uri_owl_Nothing) ) ).
cnf(u13053,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_owl_AnnotationProperty),X0) ).
cnf(u5204,axiom,
( iext(uri_rdfs_subPropertyOf,X0,sK15(uri_rdfs_subPropertyOf,X1))
| ~ iext(uri_rdfs_subPropertyOf,X0,sK14(uri_rdfs_subPropertyOf,X1))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X1) ) ).
cnf(u18750,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_Alt),X0) ).
cnf(u18731,axiom,
( iext(sK10(uri_rdfs_subPropertyOf,X0),X1,X2)
| iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0)
| ~ iext(sK9(uri_rdfs_subPropertyOf,X0),X1,X2) ) ).
cnf(u12669,axiom,
~ icext(sK9(uri_rdfs_subClassOf,uri_owl_AnnotationProperty),X0) ).
cnf(u10494,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,uri_rdf__2)
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u5886,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal) ).
cnf(u4915,axiom,
iext(uri_rdfs_subClassOf,uri_owl_OntologyProperty,X0) ).
cnf(u9535,axiom,
( icext(sK15(uri_rdfs_domain,X0),sK9(sK14(uri_rdfs_domain,X0),uri_rdf_XMLLiteral))
| iext(uri_rdfs_domain,sK14(uri_rdfs_domain,X0),uri_rdf_XMLLiteral)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0) ) ).
cnf(u7074,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_owl_Thing),X0) ).
cnf(u7542,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,uri_owl_allValuesFrom)
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u17632,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_owl_OntologyProperty),X0) ).
cnf(u8700,axiom,
iext(uri_rdfs_member,uri_owl_AnnotationProperty,X0) ).
cnf(u18734,axiom,
iext(uri_rdfs_domain,uri_rdf__3,X0) ).
cnf(u343,axiom,
( ~ iext(uri_rdfs_range,X0,X1)
| icext(X1,X3)
| ~ iext(X0,X2,X3) ) ).
cnf(u11214,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral))
| ~ iext(uri_rdfs_subPropertyOf,X1,X0)
| iext(uri_rdfs_subPropertyOf,X1,sK10(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral)) ) ).
cnf(u8282,axiom,
( icext(sK15(uri_rdfs_domain,X0),sK9(sK14(uri_rdfs_domain,X0),uri_owl_Thing))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0)
| iext(uri_rdfs_domain,sK14(uri_rdfs_domain,X0),uri_owl_Thing) ) ).
cnf(u8625,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_ContainerMembershipProperty) ).
cnf(u11164,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdfs_Statement),X0) ).
cnf(u17489,axiom,
~ iext(sK9(uri_rdfs_range,uri_owl_OntologyProperty),X0,X1) ).
cnf(u5898,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Datatype) ).
cnf(u2723,axiom,
ip(X0) ).
cnf(u9341,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Seq) ).
cnf(u368,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property) ).
cnf(u4152,axiom,
( iext(X0,sK9(X0,X1),sK10(X0,X1))
| iext(uri_rdfs_domain,X0,X1) ) ).
cnf(u3242,axiom,
( iext(X0,sK9(X0,uri_owl_DatatypeProperty),sK10(X0,uri_owl_DatatypeProperty))
| iext(uri_rdfs_domain,X0,uri_owl_DatatypeProperty) ) ).
cnf(u19672,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing),sK10(uri_rdfs_subPropertyOf,uri_owl_Nothing)) ).
cnf(u5831,axiom,
iext(uri_rdfs_range,uri_rdf_object,X0) ).
cnf(u6416,axiom,
( icext(sK12(uri_rdfs_range,X0),sK10(sK11(uri_rdfs_range,X0),uri_rdf_Alt))
| iext(uri_rdfs_domain,sK11(uri_rdfs_range,X0),uri_rdf_Alt)
| iext(uri_rdfs_range,uri_rdfs_range,X0) ) ).
cnf(u8971,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK14(uri_rdfs_subPropertyOf,X1))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X1)
| ~ iext(uri_rdfs_subPropertyOf,X2,X0)
| iext(uri_rdfs_subPropertyOf,X2,sK15(uri_rdfs_subPropertyOf,X1)) ) ).
cnf(u560,axiom,
( iext(uri_rdfs_subPropertyOf,sK14(uri_rdfs_subPropertyOf,X0),sK15(uri_rdfs_subPropertyOf,X0))
| ~ ip(X0)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u19421,axiom,
( icext(sK15(uri_rdfs_subClassOf,X0),sK13(sK14(uri_rdfs_subClassOf,X0),X1))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0)
| iext(uri_rdfs_subClassOf,sK14(uri_rdfs_subClassOf,X0),X1) ) ).
cnf(u8009,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_range,uri_rdfs_Container))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u6932,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf__1,X0) ).
cnf(u8835,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdfs_Container),X0) ).
cnf(u4744,axiom,
iext(uri_rdfs_range,uri_rdf__3,X0) ).
cnf(u8279,axiom,
iext(uri_rdfs_range,X0,uri_rdf_Bag) ).
cnf(u18724,axiom,
iext(uri_rdfs_domain,uri_owl_onProperty,X0) ).
cnf(u453,negated_conjecture,
~ iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,uri_rdfs_subClassOf) ).
cnf(u2923,axiom,
( ~ ic(X1)
| iext(X0,sK9(X0,X1),sK10(X0,X1))
| iext(uri_rdfs_domain,X0,X1) ) ).
cnf(u18751,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Container),X0) ).
cnf(u4675,axiom,
iext(uri_rdfs_range,uri_owl_someValuesFrom,X0) ).
cnf(u18758,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Seq),X0) ).
cnf(u1691,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,uri_owl_complementOf)
| iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type) ) ).
cnf(u6380,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdf_List) ).
cnf(u19701,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty),sK10(uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty)) ).
cnf(u445,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X1,X2)
| ~ iext(uri_rdfs_subPropertyOf,X0,X1)
| iext(uri_rdfs_subPropertyOf,X0,X2) ) ).
cnf(u18717,axiom,
( iext(uri_rdfs_member,sK9(X0,X1),sK10(X0,X1))
| iext(uri_rdfs_domain,X0,X1) ) ).
cnf(u15112,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_owl_DatatypeProperty),X0) ).
cnf(u11173,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_domain,uri_rdfs_Statement))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u1671,axiom,
~ icext(uri_owl_AnnotationProperty,X0) ).
cnf(u18735,axiom,
iext(uri_rdfs_domain,uri_rdf_object,X0) ).
cnf(u1259,axiom,
( icext(sK15(uri_rdf_type,X0),sK14(uri_rdf_type,X0))
| ~ ip(X0)
| iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0) ) ).
cnf(u4683,axiom,
iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0) ).
cnf(u11086,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdfs_Statement),X0) ).
cnf(u13887,axiom,
( icext(sK12(uri_rdfs_range,X0),sK10(sK11(uri_rdfs_range,X0),uri_owl_DatatypeProperty))
| iext(uri_rdfs_domain,sK11(uri_rdfs_range,X0),uri_owl_DatatypeProperty)
| iext(uri_rdfs_range,uri_rdfs_range,X0) ) ).
cnf(u9883,axiom,
iext(uri_rdfs_member,sK4(uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u15205,axiom,
~ iext(sK9(uri_rdfs_domain,uri_owl_DatatypeProperty),X0,X1) ).
cnf(u5110,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_owl_Nothing))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u18728,axiom,
( iext(uri_rdfs_subClassOf,X1,sK10(uri_rdfs_subClassOf,X0))
| ~ iext(uri_rdfs_subClassOf,X1,sK9(uri_rdfs_subClassOf,X0))
| iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0) ) ).
cnf(u18759,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_XMLLiteral),X0) ).
cnf(u4714,axiom,
iext(uri_rdfs_range,uri_rdf_first,X0) ).
cnf(u346,axiom,
( icext(X0,sK13(X0,X1))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u8707,axiom,
iext(uri_rdfs_member,uri_rdfs_Resource,uri_rdf_nil) ).
cnf(u305,axiom,
( iext(uri_rdf_type,X0,uri_rdf_Property)
| ~ ip(X0) ) ).
cnf(u8845,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdf_Bag),X0) ).
cnf(u8633,axiom,
( iext(uri_rdfs_member,X0,X1)
| ~ icext(X1,X0) ) ).
cnf(u2774,axiom,
( ~ iext(sK11(uri_rdfs_range,X0),X2,X1)
| icext(sK12(uri_rdfs_range,X0),X1)
| iext(uri_rdfs_range,uri_rdfs_range,X0) ) ).
cnf(u2796,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Resource) ).
cnf(u8708,axiom,
iext(uri_rdfs_member,uri_rdfs_Literal,uri_rdf_nil) ).
cnf(u13043,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_owl_AnnotationProperty),X0) ).
cnf(u18762,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Statement),X0) ).
cnf(u8719,axiom,
iext(uri_rdfs_member,uri_rdf_List,uri_rdf_nil) ).
cnf(u4545,axiom,
~ iext(uri_owl_someValuesFrom,X0,X1) ).
cnf(u11199,axiom,
( ~ iext(sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing),sK14(X0,sK10(uri_rdfs_subPropertyOf,uri_owl_Nothing)),sK15(X0,sK10(uri_rdfs_subPropertyOf,uri_owl_Nothing)))
| iext(uri_rdfs_subPropertyOf,X0,sK10(uri_rdfs_subPropertyOf,uri_owl_Nothing)) ) ).
cnf(u5895,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Datatype,uri_rdf_nil) ).
cnf(u8075,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_domain,uri_rdfs_Container))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u8268,axiom,
icext(uri_rdf_Bag,X0) ).
cnf(u19420,axiom,
( icext(sK15(uri_rdfs_subClassOf,X0),sK4(sK14(uri_rdfs_subClassOf,X0)))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0)
| iext(uri_owl_unionOf,sK14(uri_rdfs_subClassOf,X0),uri_rdf_nil) ) ).
cnf(u7897,axiom,
( icext(sK15(uri_rdfs_range,X0),sK12(sK14(uri_rdfs_range,X0),X1))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0)
| iext(uri_rdfs_range,sK14(uri_rdfs_range,X0),X1) ) ).
cnf(u4672,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,uri_owl_Nothing)
| iext(uri_rdfs_subClassOf,X1,X0) ) ).
cnf(u8656,axiom,
iext(uri_rdfs_member,X0,uri_rdf_Bag) ).
cnf(u8782,axiom,
iext(uri_rdfs_member,uri_rdf_predicate,X0) ).
cnf(u15408,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty))
| iext(sK10(uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty),X1,X2)
| ~ iext(X0,X1,X2) ) ).
cnf(u9393,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdfs_Seq),X0) ).
cnf(u8623,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty) ).
cnf(u12684,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subClassOf,uri_owl_AnnotationProperty),X0) ).
cnf(u19368,axiom,
( ~ iext(sK9(uri_rdfs_subPropertyOf,X0),sK14(X1,sK10(uri_rdfs_subPropertyOf,X0)),sK15(X1,sK10(uri_rdfs_subPropertyOf,X0)))
| iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0)
| iext(uri_rdfs_subPropertyOf,X1,sK10(uri_rdfs_subPropertyOf,X0)) ) ).
cnf(u366,axiom,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property) ).
cnf(u19644,axiom,
( iext(uri_rdfs_subClassOf,sK14(uri_rdfs_subClassOf,X0),sK15(uri_rdfs_subClassOf,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0) ) ).
cnf(u8915,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK14(uri_rdfs_subClassOf,X1))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X1)
| ~ iext(uri_rdfs_subClassOf,X2,X0)
| iext(uri_rdfs_subClassOf,X2,sK15(uri_rdfs_subClassOf,X1)) ) ).
cnf(u4553,axiom,
~ iext(uri_rdf_rest,X0,X1) ).
cnf(u7081,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_owl_Nothing),X0) ).
cnf(u8717,axiom,
iext(uri_rdfs_member,uri_owl_hasValue,X0) ).
cnf(u19655,axiom,
( iext(uri_rdfs_domain,sK14(uri_rdfs_domain,X0),sK15(uri_rdfs_domain,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0) ) ).
cnf(u17500,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_owl_OntologyProperty),X0) ).
cnf(u2778,axiom,
( iext(sK12(uri_rdfs_subPropertyOf,X0),X1,X2)
| iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0)
| ~ iext(sK11(uri_rdfs_subPropertyOf,X0),X1,X2) ) ).
cnf(u6064,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Literal) ).
cnf(u4557,axiom,
~ iext(uri_owl_complementOf,X0,X1) ).
cnf(u11172,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdfs_Statement),X0) ).
cnf(u8818,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdf_Alt),X0) ).
cnf(u10600,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdf_XMLLiteral),X0,X1) ).
cnf(u4685,axiom,
iext(uri_rdfs_range,uri_owl_hasValue,X0) ).
cnf(u8916,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK14(uri_rdfs_subClassOf,X1))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X1)
| icext(sK15(uri_rdfs_subClassOf,X1),X2)
| ~ icext(X0,X2) ) ).
cnf(u3238,axiom,
( iext(X0,sK9(X0,uri_owl_Thing),sK10(X0,uri_owl_Thing))
| iext(uri_rdfs_domain,X0,uri_owl_Thing) ) ).
cnf(u4217,axiom,
( iext(uri_rdf_type,sK13(uri_owl_Ontology,X0),uri_owl_Ontology)
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ) ).
cnf(u13193,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty))
| iext(sK10(uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty),X1,X2)
| ~ iext(X0,X1,X2) ) ).
cnf(u15099,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_owl_DatatypeProperty),X0) ).
cnf(u8005,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdfs_Container),X0) ).
cnf(u11801,axiom,
( icext(sK12(uri_rdfs_domain,X0),sK9(sK11(uri_rdfs_domain,X0),uri_owl_AnnotationProperty))
| iext(uri_rdfs_domain,sK11(uri_rdfs_domain,X0),uri_owl_AnnotationProperty)
| iext(uri_rdfs_range,uri_rdfs_domain,X0) ) ).
cnf(u1634,axiom,
~ icext(uri_owl_DatatypeProperty,X0) ).
cnf(u3255,axiom,
( iext(X0,sK9(X0,uri_rdf_XMLLiteral),sK10(X0,uri_rdf_XMLLiteral))
| iext(uri_rdfs_domain,X0,uri_rdf_XMLLiteral) ) ).
cnf(u18746,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_DatatypeProperty),X0) ).
cnf(u7557,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_range,uri_rdfs_Datatype))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u9536,axiom,
( iext(sK15(uri_rdfs_subPropertyOf,X0),sK9(sK14(uri_rdfs_subPropertyOf,X0),uri_rdf_XMLLiteral),sK10(sK14(uri_rdfs_subPropertyOf,X0),uri_rdf_XMLLiteral))
| iext(uri_rdfs_domain,sK14(uri_rdfs_subPropertyOf,X0),uri_rdf_XMLLiteral)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u277,axiom,
~ icext(uri_owl_Nothing,X0) ).
cnf(u1022,axiom,
( icext(sK15(uri_rdfs_subClassOf,X0),sK13(sK14(uri_rdfs_subClassOf,X0),X1))
| ~ ip(X0)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0)
| ~ ic(X1)
| iext(uri_rdfs_subClassOf,sK14(uri_rdfs_subClassOf,X0),X1) ) ).
cnf(u2804,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Class) ).
cnf(u8002,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdfs_Container),X0) ).
cnf(u10616,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdf_XMLLiteral),X0) ).
cnf(u11207,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_rdf_Alt))
| ~ iext(uri_rdfs_subPropertyOf,X1,X0)
| iext(uri_rdfs_subPropertyOf,X1,sK10(uri_rdfs_subPropertyOf,uri_rdf_Alt)) ) ).
cnf(u8787,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subClassOf,uri_owl_Nothing),X0) ).
cnf(u6935,axiom,
~ iext(sK9(uri_rdfs_domain,uri_owl_Thing),X0,X1) ).
cnf(u18729,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,X0),X1)
| icext(sK10(uri_rdfs_subClassOf,X0),X1)
| iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0) ) ).
cnf(u8622,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_nil) ).
cnf(u405,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty) ).
cnf(u18736,axiom,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,X0) ).
cnf(u9403,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_range,uri_rdfs_Seq))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u19362,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,X1))
| iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X1)
| ~ iext(uri_rdfs_subPropertyOf,X2,X0)
| iext(uri_rdfs_subPropertyOf,X2,sK10(uri_rdfs_subPropertyOf,X1)) ) ).
cnf(u9493,axiom,
( iext(uri_rdfs_member,sK9(X0,uri_rdf_XMLLiteral),sK10(X0,uri_rdf_XMLLiteral))
| iext(uri_rdfs_domain,X0,uri_rdf_XMLLiteral) ) ).
cnf(u8788,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_owl_Nothing),X0) ).
cnf(u18763,axiom,
( icext(sK12(uri_rdfs_domain,X0),sK9(sK11(uri_rdfs_domain,X0),X1))
| iext(uri_rdfs_domain,sK11(uri_rdfs_domain,X0),X1)
| iext(uri_rdfs_range,uri_rdfs_domain,X0) ) ).
cnf(u438,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| ~ iext(uri_rdfs_subClassOf,X0,X1)
| iext(uri_rdfs_subClassOf,X0,X2) ) ).
cnf(u8799,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_owl_Thing),X0) ).
cnf(u15089,axiom,
~ iext(sK9(uri_rdfs_range,uri_owl_DatatypeProperty),X0,X1) ).
cnf(u247,axiom,
( ~ iext(uri_owl_unionOf,X0,uri_rdf_nil)
| ~ icext(X0,X1) ) ).
cnf(u10409,axiom,
~ icext(sK9(uri_rdfs_subClassOf,uri_rdf_XMLLiteral),X0) ).
cnf(u18720,axiom,
iext(uri_rdfs_domain,uri_rdf_rest,X0) ).
cnf(u5184,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first)
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u5966,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf__2)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u1773,axiom,
icext(uri_owl_Ontology,sK4(uri_owl_Ontology)) ).
cnf(u8972,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK14(uri_rdfs_subPropertyOf,X1))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X1)
| iext(sK15(uri_rdfs_subPropertyOf,X1),X2,X3)
| ~ iext(X0,X2,X3) ) ).
cnf(u10605,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdf_XMLLiteral),X0) ).
cnf(u8795,axiom,
( iext(uri_rdfs_member,sK9(X0,uri_owl_Nothing),sK10(X0,uri_owl_Nothing))
| iext(uri_rdfs_domain,X0,uri_owl_Nothing) ) ).
cnf(u18732,axiom,
iext(uri_rdfs_domain,uri_rdf__1,X0) ).
cnf(u6332,axiom,
( icext(sK12(uri_rdfs_range,X0),sK12(sK11(uri_rdfs_range,X0),X1))
| iext(uri_rdfs_range,uri_rdfs_range,X0)
| iext(uri_rdfs_range,sK11(uri_rdfs_range,X0),X1) ) ).
cnf(u9345,axiom,
iext(uri_rdfs_member,uri_rdfs_Seq,uri_rdf_nil) ).
cnf(u386,axiom,
( iext(uri_rdf_type,X0,X1)
| ~ icext(X1,X0) ) ).
cnf(u367,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property) ).
cnf(u8777,axiom,
iext(uri_rdfs_member,uri_rdf_XMLLiteral,X0) ).
cnf(u298,axiom,
( ~ ioxp(X0)
| ~ iext(X0,X1,X2)
| ix(X1) ) ).
cnf(u9634,axiom,
~ iext(sK4(uri_rdfs_ContainerMembershipProperty),X0,X1) ).
cnf(u8344,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_range,uri_rdf_Bag))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u4742,axiom,
~ iext(uri_rdf__3,X0,X1) ).
cnf(u4173,axiom,
iext(uri_rdfs_subClassOf,X0,uri_owl_Thing) ).
cnf(u5563,axiom,
( icext(uri_owl_Ontology,sK13(uri_owl_Ontology,X0))
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ) ).
cnf(u8669,axiom,
( iext(uri_rdfs_member,X0,sK12(uri_rdfs_subClassOf,X1))
| ~ iext(uri_rdfs_subClassOf,X0,sK11(uri_rdfs_subClassOf,X1))
| iext(uri_rdfs_range,uri_rdfs_subClassOf,X1) ) ).
cnf(u7078,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_owl_Nothing),X0) ).
cnf(u8071,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdfs_Container),X0) ).
cnf(u1601,axiom,
~ icext(uri_rdf_Alt,X0) ).
cnf(u18756,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u12953,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_owl_AnnotationProperty),X0) ).
cnf(u4914,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0) ).
cnf(u5192,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_isDefinedBy)
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u6370,axiom,
icext(uri_rdf_List,X0) ).
cnf(u7955,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container) ).
cnf(u310,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_Ontology)
| ix(X0) ) ).
cnf(u11075,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdfs_Statement),X0) ).
cnf(u13192,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty))
| ~ iext(uri_rdfs_subPropertyOf,X1,X0)
| iext(uri_rdfs_subPropertyOf,X1,sK10(uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty)) ) ).
cnf(u292,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_AnnotationProperty)
| ioap(X0) ) ).
cnf(u11001,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Statement) ).
cnf(u12808,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_owl_AnnotationProperty))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u6415,axiom,
( icext(sK12(uri_rdfs_domain,X0),sK9(sK11(uri_rdfs_domain,X0),uri_rdf_Alt))
| iext(uri_rdfs_domain,sK11(uri_rdfs_domain,X0),uri_rdf_Alt)
| iext(uri_rdfs_range,uri_rdfs_domain,X0) ) ).
cnf(u14954,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_owl_DatatypeProperty))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u10990,axiom,
icext(uri_rdfs_Statement,X0) ).
cnf(u5185,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest)
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u8657,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_ContainerMembershipProperty) ).
cnf(u375,axiom,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property) ).
cnf(u8785,axiom,
iext(uri_rdfs_member,sK4(uri_owl_Ontology),uri_owl_Ontology) ).
cnf(u19372,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Nothing),sK10(uri_rdfs_domain,uri_owl_Nothing)) ).
cnf(u9032,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u8774,axiom,
iext(uri_rdfs_member,uri_rdfs_ContainerMembershipProperty,uri_rdf_nil) ).
cnf(u2775,axiom,
( ~ icext(sK11(uri_rdfs_subClassOf,X0),X1)
| icext(sK12(uri_rdfs_subClassOf,X0),X1)
| iext(uri_rdfs_range,uri_rdfs_subClassOf,X0) ) ).
cnf(u8745,axiom,
iext(uri_rdfs_member,uri_rdf__2,X0) ).
cnf(u17642,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_owl_OntologyProperty),X0) ).
cnf(u19704,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty),sK10(uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty)) ).
cnf(u371,axiom,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property) ).
cnf(u10608,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdf_XMLLiteral),X0) ).
cnf(u337,axiom,
( ~ icext(X1,sK9(X0,X1))
| ~ ic(X1)
| ~ ip(X0)
| iext(uri_rdfs_domain,X0,X1) ) ).
cnf(u18737,axiom,
iext(uri_rdfs_domain,uri_rdf_predicate,X0) ).
cnf(u8739,axiom,
iext(uri_rdfs_member,uri_rdf__1,X0) ).
cnf(u8612,axiom,
icext(uri_rdfs_ContainerMembershipProperty,X0) ).
cnf(u8409,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdf_Bag),X0) ).
cnf(u18723,axiom,
iext(uri_rdfs_domain,uri_owl_hasValue,X0) ).
cnf(u11004,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_Statement) ).
cnf(u5101,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK4(uri_rdfs_Datatype))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u8698,axiom,
iext(uri_rdfs_member,uri_rdfs_Datatype,uri_rdf_nil) ).
cnf(u18740,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_Nothing),X0) ).
cnf(u9038,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u13194,axiom,
( iext(uri_rdfs_member,X0,sK10(uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty))
| ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty)) ) ).
cnf(u1586,axiom,
~ icext(uri_owl_OntologyProperty,X0) ).
cnf(u1298,axiom,
( ~ iext(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1,X2)
| iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0)
| iext(uri_rdfs_member,X1,X2)
| ~ ic(X0) ) ).
cnf(u8751,axiom,
iext(uri_rdfs_member,uri_rdf__3,X0) ).
cnf(u17503,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_owl_OntologyProperty),X0) ).
cnf(u5187,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,uri_owl_onProperty)
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u11802,axiom,
( icext(sK12(uri_rdfs_range,X0),sK10(sK11(uri_rdfs_range,X0),uri_owl_AnnotationProperty))
| iext(uri_rdfs_domain,sK11(uri_rdfs_range,X0),uri_owl_AnnotationProperty)
| iext(uri_rdfs_range,uri_rdfs_range,X0) ) ).
cnf(u8684,axiom,
iext(uri_rdfs_member,uri_rdf_first,X0) ).
cnf(u17514,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_range,uri_owl_OntologyProperty))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u8406,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdf_Bag),X0) ).
cnf(u1567,axiom,
~ icext(uri_rdf_XMLLiteral,X0) ).
cnf(u7957,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Container) ).
cnf(u8285,axiom,
( icext(sK15(uri_rdfs_domain,X0),sK11(sK14(uri_rdfs_domain,X0),X1))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0)
| iext(uri_rdfs_range,sK14(uri_rdfs_domain,X0),X1) ) ).
cnf(u18722,axiom,
iext(uri_rdfs_domain,uri_owl_allValuesFrom,X0) ).
cnf(u451,axiom,
ir(X0) ).
cnf(u14777,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subClassOf,uri_owl_DatatypeProperty),X0) ).
cnf(u15236,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_owl_DatatypeProperty),X0) ).
cnf(u18877,axiom,
( icext(sK10(uri_rdfs_subClassOf,X0),sK4(sK9(uri_rdfs_subClassOf,X0)))
| iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0)
| iext(uri_owl_unionOf,sK9(uri_rdfs_subClassOf,X0),uri_rdf_nil) ) ).
cnf(u4709,axiom,
iext(uri_rdfs_range,uri_rdf_rest,X0) ).
cnf(u2806,axiom,
iext(uri_rdfs_range,X0,uri_rdf_Property) ).
cnf(u18764,axiom,
( icext(sK12(uri_rdfs_range,X0),sK10(sK11(uri_rdfs_range,X0),X1))
| iext(uri_rdfs_domain,sK11(uri_rdfs_range,X0),X1)
| iext(uri_rdfs_range,uri_rdfs_range,X0) ) ).
cnf(u7071,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_owl_Thing),X0) ).
cnf(u8281,axiom,
( icext(sK15(uri_rdfs_domain,X0),sK9(sK14(uri_rdfs_domain,X0),uri_owl_Nothing))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0)
| iext(uri_rdfs_domain,sK14(uri_rdfs_domain,X0),uri_owl_Nothing) ) ).
cnf(u8672,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_member) ).
cnf(u7954,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Container,uri_rdf_nil) ).
cnf(u10617,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_range,uri_rdf_XMLLiteral))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u8288,axiom,
( icext(sK15(uri_rdfs_domain,X0),sK14(sK14(uri_rdfs_domain,X0),X1))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0)
| iext(uri_rdfs_subPropertyOf,sK14(uri_rdfs_domain,X0),X1) ) ).
cnf(u7998,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdfs_Container),X0,X1) ).
cnf(u7647,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_range,uri_rdf_Alt))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u6085,axiom,
( icext(sK12(uri_rdfs_domain,X0),sK9(sK11(uri_rdfs_domain,X0),uri_owl_Nothing))
| iext(uri_rdfs_range,uri_rdfs_domain,X0)
| iext(uri_rdfs_domain,sK11(uri_rdfs_domain,X0),uri_owl_Nothing) ) ).
cnf(u19363,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,X1))
| iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X1)
| iext(sK10(uri_rdfs_subPropertyOf,X1),X2,X3)
| ~ iext(X0,X2,X3) ) ).
cnf(u18744,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_AnnotationProperty),X0) ).
cnf(u7503,axiom,
~ icext(sK9(uri_rdfs_subClassOf,uri_rdf_Alt),X0) ).
cnf(u13890,axiom,
( icext(sK15(uri_rdfs_range,X0),sK10(sK14(uri_rdfs_range,X0),uri_owl_DatatypeProperty))
| iext(uri_rdfs_domain,sK14(uri_rdfs_range,X0),uri_owl_DatatypeProperty)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0) ) ).
cnf(u8864,axiom,
iext(uri_rdfs_member,X0,X0) ).
cnf(u11761,axiom,
( iext(uri_rdfs_member,sK9(X0,uri_owl_AnnotationProperty),sK10(X0,uri_owl_AnnotationProperty))
| iext(uri_rdfs_domain,X0,uri_owl_AnnotationProperty) ) ).
cnf(u6329,axiom,
( icext(sK12(uri_rdfs_range,X0),sK10(sK11(uri_rdfs_range,X0),uri_owl_Nothing))
| iext(uri_rdfs_range,uri_rdfs_range,X0)
| iext(uri_rdfs_domain,sK11(uri_rdfs_range,X0),uri_owl_Nothing) ) ).
cnf(u4747,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf__3,X0) ).
cnf(u5100,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u10704,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),X0) ).
cnf(u19811,axiom,
( iext(uri_rdfs_subPropertyOf,sK14(uri_rdfs_subPropertyOf,X0),sK15(uri_rdfs_subPropertyOf,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u17839,axiom,
( ~ iext(sK9(uri_rdfs_subPropertyOf,uri_owl_OntologyProperty),sK14(X0,sK10(uri_rdfs_subPropertyOf,uri_owl_OntologyProperty)),sK15(X0,sK10(uri_rdfs_subPropertyOf,uri_owl_OntologyProperty)))
| iext(uri_rdfs_subPropertyOf,X0,sK10(uri_rdfs_subPropertyOf,uri_owl_OntologyProperty)) ) ).
cnf(u6063,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Literal) ).
cnf(u9340,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Seq) ).
cnf(u8728,axiom,
iext(uri_rdfs_member,uri_owl_someValuesFrom,X0) ).
cnf(u352,axiom,
( ~ iext(X1,sK14(X0,X1),sK15(X0,X1))
| ~ ip(X1)
| ~ ip(X0)
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u15102,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_owl_DatatypeProperty),X0) ).
cnf(u549,axiom,
( iext(uri_rdfs_subClassOf,sK14(uri_rdfs_subClassOf,X0),sK15(uri_rdfs_subClassOf,X0))
| ~ ip(X0)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0) ) ).
cnf(u7894,axiom,
( icext(sK15(uri_rdfs_range,X0),sK10(sK14(uri_rdfs_range,X0),uri_owl_Thing))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0)
| iext(uri_rdfs_domain,sK14(uri_rdfs_range,X0),uri_owl_Thing) ) ).
cnf(u5834,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf_object,X0) ).
cnf(u5878,axiom,
icext(uri_rdfs_Datatype,X0) ).
cnf(u11805,axiom,
( icext(sK15(uri_rdfs_range,X0),sK10(sK14(uri_rdfs_range,X0),uri_owl_AnnotationProperty))
| iext(uri_rdfs_domain,sK14(uri_rdfs_range,X0),uri_owl_AnnotationProperty)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0) ) ).
cnf(u8850,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdf_Bag),X0) ).
cnf(u18749,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_Alt),X0) ).
cnf(u16215,axiom,
( icext(sK15(uri_rdfs_domain,X0),sK9(sK14(uri_rdfs_domain,X0),uri_owl_OntologyProperty))
| iext(uri_rdfs_domain,sK14(uri_rdfs_domain,X0),uri_owl_OntologyProperty)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0) ) ).
cnf(u3243,axiom,
( iext(X0,sK9(X0,uri_owl_OntologyProperty),sK10(X0,uri_owl_OntologyProperty))
| iext(uri_rdfs_domain,X0,uri_owl_OntologyProperty) ) ).
cnf(u364,axiom,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property) ).
cnf(u8402,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdf_Bag),X0,X1) ).
cnf(u4717,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0) ).
cnf(u5926,axiom,
iext(uri_rdfs_subClassOf,uri_rdf__1,X0) ).
cnf(u19107,axiom,
( icext(sK10(uri_rdfs_domain,X0),sK9(sK9(uri_rdfs_domain,X0),X1))
| iext(uri_rdfs_domain,uri_rdfs_domain,X0)
| iext(uri_rdfs_domain,sK9(uri_rdfs_domain,X0),X1) ) ).
cnf(u9402,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdfs_Seq),X0) ).
cnf(u7895,axiom,
( icext(sK15(uri_rdfs_range,X0),sK10(sK14(uri_rdfs_range,X0),uri_rdf_Alt))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0)
| iext(uri_rdfs_domain,sK14(uri_rdfs_range,X0),uri_rdf_Alt) ) ).
cnf(u5509,axiom,
( icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK11(sK9(uri_rdfs_domain,uri_owl_Nothing),X0))
| iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_owl_Nothing),X0) ) ).
cnf(u18752,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Container),X0) ).
cnf(u5082,axiom,
~ icext(sK9(uri_rdfs_subClassOf,uri_owl_Nothing),X0) ).
cnf(u11002,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Statement) ).
cnf(u8772,axiom,
iext(uri_rdfs_member,uri_rdfs_Container,uri_rdf_nil) ).
cnf(u4555,axiom,
~ iext(uri_rdf_first,X0,X1) ).
cnf(u10415,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_rdf_XMLLiteral))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u11202,axiom,
( iext(uri_rdfs_member,X0,sK10(uri_rdfs_subPropertyOf,uri_owl_Nothing))
| ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing)) ) ).
cnf(u4559,axiom,
iext(uri_rdfs_range,uri_rdf_predicate,X0) ).
cnf(u11161,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdfs_Statement),X0) ).
cnf(u5836,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,uri_rdf_object)
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u372,axiom,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property) ).
cnf(u17151,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subClassOf,uri_owl_OntologyProperty),X0) ).
cnf(u8278,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag) ).
cnf(u13891,axiom,
( icext(sK15(uri_rdfs_domain,X0),sK9(sK14(uri_rdfs_domain,X0),uri_owl_DatatypeProperty))
| iext(uri_rdfs_domain,sK14(uri_rdfs_domain,X0),uri_owl_DatatypeProperty)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0) ) ).
cnf(u6090,axiom,
( icext(sK12(uri_rdfs_domain,X0),sK14(sK11(uri_rdfs_domain,X0),X1))
| iext(uri_rdfs_range,uri_rdfs_domain,X0)
| iext(uri_rdfs_subPropertyOf,sK11(uri_rdfs_domain,X0),X1) ) ).
cnf(u6925,axiom,
iext(uri_rdfs_subPropertyOf,uri_owl_allValuesFrom,X0) ).
cnf(u800,axiom,
icext(uri_rdfs_Resource,X0) ).
cnf(u4918,axiom,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,X0) ).
cnf(u15218,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_owl_DatatypeProperty),X0) ).
cnf(u8808,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdfs_Datatype),X0) ).
cnf(u13892,axiom,
( iext(sK15(uri_rdfs_subPropertyOf,X0),sK9(sK14(uri_rdfs_subPropertyOf,X0),uri_owl_DatatypeProperty),sK10(sK14(uri_rdfs_subPropertyOf,X0),uri_owl_DatatypeProperty))
| iext(uri_rdfs_domain,sK14(uri_rdfs_subPropertyOf,X0),uri_owl_DatatypeProperty)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u437,axiom,
( iext(uri_rdfs_subClassOf,X0,X0)
| ~ ic(X0) ) ).
cnf(u14767,axiom,
iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,uri_owl_DatatypeProperty),X0) ).
cnf(u13191,axiom,
( ~ iext(sK9(uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty),sK14(X0,sK10(uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty)),sK15(X0,sK10(uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty)))
| iext(uri_rdfs_subPropertyOf,X0,sK10(uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty)) ) ).
cnf(u19640,axiom,
( ~ iext(sK14(uri_rdfs_subPropertyOf,X0),sK14(X1,sK15(uri_rdfs_subPropertyOf,X0)),sK15(X1,sK15(uri_rdfs_subPropertyOf,X0)))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0)
| iext(uri_rdfs_subPropertyOf,X1,sK15(uri_rdfs_subPropertyOf,X0)) ) ).
cnf(u7956,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Container) ).
cnf(u5094,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_AnnotationProperty)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u342,axiom,
( ~ icext(X1,sK12(X0,X1))
| ~ ip(X1)
| ~ ip(X0)
| iext(uri_rdfs_range,X0,X1) ) ).
cnf(u18742,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Datatype),X0) ).
cnf(u4567,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,X0) ).
cnf(u11156,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdfs_Statement),X0,X1) ).
cnf(u11216,axiom,
( iext(uri_rdfs_member,X0,sK10(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral))
| ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral)) ) ).
cnf(u5921,axiom,
~ icext(uri_rdf__1,X0) ).
cnf(u1192,axiom,
( ~ icext(sK15(X0,uri_rdf_type),sK14(X0,uri_rdf_type))
| ~ ip(X0)
| iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type) ) ).
cnf(u18738,axiom,
iext(uri_rdfs_domain,sK4(uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u407,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty) ).
cnf(u338,axiom,
( ~ iext(uri_rdfs_domain,X0,X1)
| icext(X1,X2)
| ~ iext(X0,X2,X3) ) ).
cnf(u4917,axiom,
iext(uri_rdfs_subClassOf,uri_owl_AnnotationProperty,X0) ).
cnf(u1305,axiom,
( iext(uri_rdfs_member,sK14(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1),sK15(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1))
| iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0)
| ~ ic(X0)
| ~ ip(X1)
| iext(uri_rdfs_subPropertyOf,sK13(uri_rdfs_ContainerMembershipProperty,X0),X1) ) ).
cnf(u18761,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Statement),X0) ).
cnf(u297,axiom,
( ~ ioxp(X0)
| ~ iext(X0,X1,X2)
| ix(X2) ) ).
cnf(u8817,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subClassOf,uri_rdf_Alt),X0) ).
cnf(u6929,axiom,
iext(uri_rdfs_range,uri_rdf__1,X0) ).
cnf(u4216,axiom,
( ix(sK13(uri_owl_Ontology,X0))
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ) ).
cnf(u7555,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_domain,uri_owl_Thing))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u17339,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_owl_OntologyProperty))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u4913,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,X0) ).
cnf(u19685,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral),sK10(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral)) ).
cnf(u16214,axiom,
( icext(sK15(uri_rdfs_range,X0),sK10(sK14(uri_rdfs_range,X0),uri_owl_OntologyProperty))
| iext(uri_rdfs_domain,sK14(uri_rdfs_range,X0),uri_owl_OntologyProperty)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0) ) ).
cnf(u444,axiom,
( iext(uri_rdfs_subPropertyOf,X0,X0)
| ~ ip(X0) ) ).
cnf(u15215,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_owl_DatatypeProperty),X0) ).
cnf(u7553,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_range,uri_owl_Nothing))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u5887,axiom,
idc(X0) ).
cnf(u8624,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_ContainerMembershipProperty) ).
cnf(u17840,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_owl_OntologyProperty))
| ~ iext(uri_rdfs_subPropertyOf,X1,X0)
| iext(uri_rdfs_subPropertyOf,X1,sK10(uri_rdfs_subPropertyOf,uri_owl_OntologyProperty)) ) ).
cnf(u19364,axiom,
( iext(uri_rdfs_member,X0,sK10(uri_rdfs_subPropertyOf,X1))
| iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X1)
| ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,X1)) ) ).
cnf(u9530,axiom,
( icext(sK12(uri_rdfs_domain,X0),sK9(sK11(uri_rdfs_domain,X0),uri_rdf_XMLLiteral))
| iext(uri_rdfs_domain,sK11(uri_rdfs_domain,X0),uri_rdf_XMLLiteral)
| iext(uri_rdfs_range,uri_rdfs_domain,X0) ) ).
cnf(u15237,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_domain,uri_owl_DatatypeProperty))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u19115,axiom,
( icext(sK10(uri_rdfs_domain,X0),sK11(sK9(uri_rdfs_domain,X0),X1))
| iext(uri_rdfs_domain,uri_rdfs_domain,X0)
| iext(uri_rdfs_range,sK9(uri_rdfs_domain,X0),X1) ) ).
cnf(u11070,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdfs_Statement),X0,X1) ).
cnf(u10705,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_domain,uri_rdf_XMLLiteral))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u4549,axiom,
~ iext(uri_owl_hasValue,X0,X1) ).
cnf(u8064,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdfs_Container),X0,X1) ).
cnf(u9039,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u7702,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdf_Alt),X0,X1) ).
cnf(u249,axiom,
( icext(X0,sK4(X0))
| ~ ic(X0)
| iext(uri_owl_unionOf,X0,uri_rdf_nil) ) ).
cnf(u8636,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_Resource) ).
cnf(u2776,axiom,
( iext(uri_rdfs_subClassOf,X1,sK12(uri_rdfs_subClassOf,X0))
| ~ iext(uri_rdfs_subClassOf,X1,sK11(uri_rdfs_subClassOf,X0))
| iext(uri_rdfs_range,uri_rdfs_subClassOf,X0) ) ).
cnf(u9029,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u19130,axiom,
( icext(sK10(uri_rdfs_range,X0),sK15(sK9(uri_rdfs_range,X0),X1))
| iext(uri_rdfs_domain,uri_rdfs_range,X0)
| iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,X0),X1) ) ).
cnf(u5191,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,uri_rdf__3)
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u11806,axiom,
( icext(sK15(uri_rdfs_domain,X0),sK9(sK14(uri_rdfs_domain,X0),uri_owl_AnnotationProperty))
| iext(uri_rdfs_domain,sK14(uri_rdfs_domain,X0),uri_owl_AnnotationProperty)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0) ) ).
cnf(u12931,axiom,
~ iext(sK9(uri_rdfs_range,uri_owl_AnnotationProperty),X0,X1) ).
cnf(u3250,axiom,
( iext(X0,sK9(X0,uri_rdf_Alt),sK10(X0,uri_rdf_Alt))
| iext(uri_rdfs_domain,X0,uri_rdf_Alt) ) ).
cnf(u4916,axiom,
iext(uri_rdfs_subClassOf,uri_owl_DatatypeProperty,X0) ).
cnf(u9025,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X0,X1) ).
cnf(u8829,axiom,
( iext(uri_rdfs_member,sK9(X0,uri_rdf_Alt),sK10(X0,uri_rdf_Alt))
| iext(uri_rdfs_domain,X0,uri_rdf_Alt) ) ).
cnf(u8614,axiom,
iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member) ).
cnf(u19429,axiom,
( iext(uri_rdfs_range,sK14(uri_rdfs_range,X0),sK15(uri_rdfs_range,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0) ) ).
cnf(u18754,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_Bag),X0) ).
cnf(u7945,axiom,
icext(uri_rdfs_Container,X0) ).
cnf(u410,axiom,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype) ).
cnf(u8771,axiom,
iext(uri_rdfs_member,uri_rdf_Alt,X0) ).
cnf(u12943,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_owl_AnnotationProperty),X0) ).
cnf(u369,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property) ).
cnf(u2731,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdf_Property) ).
cnf(u8697,axiom,
iext(uri_rdfs_member,uri_rdfs_Class,uri_rdf_nil) ).
cnf(u10999,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Statement,uri_rdf_nil) ).
cnf(u4912,axiom,
iext(uri_rdfs_subClassOf,sK4(uri_rdfs_Datatype),X0) ).
cnf(u19680,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subPropertyOf,uri_rdf_Alt),sK10(uri_rdfs_subPropertyOf,uri_rdf_Alt)) ).
cnf(u8339,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK11(uri_rdfs_subPropertyOf,X1))
| iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X1)
| ~ iext(uri_rdfs_subPropertyOf,X2,X0)
| iext(uri_rdfs_subPropertyOf,X2,sK12(uri_rdfs_subPropertyOf,X1)) ) ).
cnf(u6335,axiom,
( icext(sK12(uri_rdfs_range,X0),sK15(sK11(uri_rdfs_range,X0),X1))
| iext(uri_rdfs_range,uri_rdfs_range,X0)
| iext(uri_rdfs_subPropertyOf,sK11(uri_rdfs_range,X0),X1) ) ).
cnf(u6086,axiom,
( icext(sK12(uri_rdfs_domain,X0),sK9(sK11(uri_rdfs_domain,X0),uri_owl_Thing))
| iext(uri_rdfs_range,uri_rdfs_domain,X0)
| iext(uri_rdfs_domain,sK11(uri_rdfs_domain,X0),uri_owl_Thing) ) ).
cnf(u422,axiom,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class) ).
cnf(u6388,axiom,
( ~ iext(sK14(uri_rdfs_range,X0),X2,X1)
| icext(sK15(uri_rdfs_range,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0) ) ).
cnf(u8671,axiom,
( iext(uri_rdfs_member,X0,sK12(uri_rdfs_subPropertyOf,X1))
| ~ iext(uri_rdfs_subPropertyOf,X0,sK11(uri_rdfs_subPropertyOf,X1))
| iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X1) ) ).
cnf(u5087,axiom,
iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,uri_owl_Nothing),X0) ).
cnf(u18725,axiom,
iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0) ).
cnf(u9791,axiom,
iext(uri_rdfs_range,uri_rdf__2,X0) ).
cnf(u11078,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdfs_Statement),X0) ).
cnf(u4537,axiom,
~ iext(uri_rdf_predicate,X0,X1) ).
cnf(u8773,axiom,
iext(uri_rdfs_member,uri_rdf_Bag,uri_rdf_nil) ).
cnf(u8340,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK11(uri_rdfs_subPropertyOf,X1))
| iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X1)
| iext(sK12(uri_rdfs_subPropertyOf,X1),X2,X3)
| ~ iext(X0,X2,X3) ) ).
cnf(u18743,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_AnnotationProperty),X0) ).
cnf(u9804,axiom,
iext(uri_rdfs_subPropertyOf,sK4(uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u4172,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource) ).
cnf(u18739,axiom,
( icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK9(sK9(uri_rdfs_domain,uri_owl_Nothing),X0))
| iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Nothing),X0) ) ).
cnf(u19636,axiom,
( iext(sK15(uri_rdfs_subPropertyOf,X0),X1,X2)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0)
| ~ iext(sK14(uri_rdfs_subPropertyOf,X0),X1,X2) ) ).
cnf(u13844,axiom,
( iext(uri_rdfs_member,sK9(X0,uri_owl_DatatypeProperty),sK10(X0,uri_owl_DatatypeProperty))
| iext(uri_rdfs_domain,X0,uri_owl_DatatypeProperty) ) ).
cnf(u13886,axiom,
( icext(sK12(uri_rdfs_domain,X0),sK9(sK11(uri_rdfs_domain,X0),uri_owl_DatatypeProperty))
| iext(uri_rdfs_domain,sK11(uri_rdfs_domain,X0),uri_owl_DatatypeProperty)
| iext(uri_rdfs_range,uri_rdfs_domain,X0) ) ).
cnf(u6918,axiom,
( ~ iext(sK14(uri_rdfs_domain,X0),X1,X2)
| icext(sK15(uri_rdfs_domain,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0) ) ).
cnf(u18769,axiom,
( iext(sK15(uri_rdfs_subPropertyOf,X0),sK9(sK14(uri_rdfs_subPropertyOf,X0),X1),sK10(sK14(uri_rdfs_subPropertyOf,X0),X1))
| iext(uri_rdfs_domain,sK14(uri_rdfs_subPropertyOf,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u19709,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_owl_OntologyProperty),sK10(uri_rdfs_subPropertyOf,uri_owl_OntologyProperty)) ).
cnf(u7640,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdf_Alt),X0) ).
cnf(u2720,axiom,
icext(uri_rdf_Property,X0) ).
cnf(u351,axiom,
( iext(X0,sK14(X0,X1),sK15(X0,X1))
| ~ ip(X1)
| ~ ip(X0)
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u4165,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class) ).
cnf(u19361,axiom,
( iext(uri_rdfs_member,X0,sK10(uri_rdfs_subClassOf,X1))
| iext(uri_rdfs_domain,uri_rdfs_subClassOf,X1)
| ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,X1)) ) ).
cnf(u1188,axiom,
( ~ icext(uri_owl_Ontology,X0)
| ix(X0) ) ).
cnf(u5095,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_DatatypeProperty)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u19693,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty),sK10(uri_rdfs_subPropertyOf,uri_owl_AnnotationProperty)) ).
cnf(u11807,axiom,
( iext(sK15(uri_rdfs_subPropertyOf,X0),sK9(sK14(uri_rdfs_subPropertyOf,X0),uri_owl_AnnotationProperty),sK10(sK14(uri_rdfs_subPropertyOf,X0),uri_owl_AnnotationProperty))
| iext(uri_rdfs_domain,sK14(uri_rdfs_subPropertyOf,X0),uri_owl_AnnotationProperty)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u4564,axiom,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,X0) ).
cnf(u15407,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty))
| ~ iext(uri_rdfs_subPropertyOf,X1,X0)
| iext(uri_rdfs_subPropertyOf,X1,sK10(uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty)) ) ).
cnf(u4729,axiom,
iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0) ).
cnf(u347,axiom,
( ~ icext(X1,sK13(X0,X1))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u18767,axiom,
( icext(sK15(uri_rdfs_range,X0),sK10(sK14(uri_rdfs_range,X0),X1))
| iext(uri_rdfs_domain,sK14(uri_rdfs_range,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0) ) ).
cnf(u8290,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK11(uri_rdfs_subClassOf,X1))
| iext(uri_rdfs_range,uri_rdfs_subClassOf,X1)
| ~ iext(uri_rdfs_subClassOf,X2,X0)
| iext(uri_rdfs_subClassOf,X2,sK12(uri_rdfs_subClassOf,X1)) ) ).
cnf(u6560,axiom,
~ iext(uri_owl_allValuesFrom,X0,X1) ).
cnf(u8764,axiom,
iext(uri_rdfs_member,uri_rdfs_isDefinedBy,X0) ).
cnf(u7507,axiom,
iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,uri_rdf_Alt),X0) ).
cnf(u9459,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdfs_Seq),X0,X1) ).
cnf(u13031,axiom,
~ iext(sK9(uri_rdfs_domain,uri_owl_AnnotationProperty),X0,X1) ).
cnf(u8400,axiom,
( ~ iext(sK11(uri_rdfs_subPropertyOf,X0),sK14(X1,sK12(uri_rdfs_subPropertyOf,X0)),sK15(X1,sK12(uri_rdfs_subPropertyOf,X0)))
| iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0)
| iext(uri_rdfs_subPropertyOf,X1,sK12(uri_rdfs_subPropertyOf,X0)) ) ).
cnf(u4726,axiom,
iext(uri_rdfs_range,uri_owl_complementOf,X0) ).
cnf(u13054,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_domain,uri_owl_AnnotationProperty))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u16166,axiom,
( iext(uri_rdfs_member,sK9(X0,uri_owl_OntologyProperty),sK10(X0,uri_owl_OntologyProperty))
| iext(uri_rdfs_domain,X0,uri_owl_OntologyProperty) ) ).
cnf(u6922,axiom,
iext(uri_rdfs_range,uri_owl_allValuesFrom,X0) ).
cnf(u2642,axiom,
iext(uri_owl_intersectionOf,uri_owl_Thing,uri_rdf_nil) ).
cnf(u8974,axiom,
( iext(uri_rdfs_member,X0,sK15(uri_rdfs_subPropertyOf,X1))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X1)
| ~ iext(uri_rdfs_subPropertyOf,X0,sK14(uri_rdfs_subPropertyOf,X1)) ) ).
cnf(u9329,axiom,
icext(uri_rdfs_Seq,X0) ).
cnf(u8758,axiom,
iext(uri_rdfs_member,uri_rdf_object,X0) ).
cnf(u7085,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdfs_Datatype),X0) ).
cnf(u8694,axiom,
iext(uri_rdfs_member,uri_owl_Thing,uri_rdf_nil) ).
cnf(u1408,axiom,
iext(uri_owl_unionOf,uri_owl_Nothing,uri_rdf_nil) ).
cnf(u17643,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_domain,uri_owl_OntologyProperty))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u5530,axiom,
( icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK14(sK9(uri_rdfs_domain,uri_owl_Nothing),X0))
| iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_owl_Nothing),X0) ) ).
cnf(u8690,axiom,
iext(uri_rdfs_member,uri_rdf_rest,X0) ).
cnf(u19127,axiom,
( icext(sK10(uri_rdfs_range,X0),sK12(sK9(uri_rdfs_range,X0),X1))
| iext(uri_rdfs_domain,uri_rdfs_range,X0)
| iext(uri_rdfs_range,sK9(uri_rdfs_range,X0),X1) ) ).
cnf(u913,axiom,
iext(uri_rdf_type,X0,uri_rdfs_Resource) ).
cnf(u8852,axiom,
( iext(uri_rdfs_member,sK11(X0,X1),sK12(X0,X1))
| iext(uri_rdfs_range,X0,X1) ) ).
cnf(u17513,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_owl_OntologyProperty),X0) ).
cnf(u9109,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u8291,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK11(uri_rdfs_subClassOf,X1))
| iext(uri_rdfs_range,uri_rdfs_subClassOf,X1)
| icext(sK12(uri_rdfs_subClassOf,X1),X2)
| ~ icext(X0,X2) ) ).
cnf(u18733,axiom,
iext(uri_rdfs_domain,uri_rdf__2,X0) ).
cnf(u10499,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK4(uri_rdfs_ContainerMembershipProperty))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u8867,axiom,
iext(uri_rdfs_member,X0,uri_owl_Thing) ).
cnf(u8283,axiom,
( icext(sK15(uri_rdfs_domain,X0),sK9(sK14(uri_rdfs_domain,X0),uri_rdf_Alt))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0)
| iext(uri_rdfs_domain,sK14(uri_rdfs_domain,X0),uri_rdf_Alt) ) ).
cnf(u19360,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,X1))
| iext(uri_rdfs_domain,uri_rdfs_subClassOf,X1)
| icext(sK10(uri_rdfs_subClassOf,X1),X2)
| ~ icext(X0,X2) ) ).
cnf(u9472,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdfs_Seq),X0) ).
cnf(u17841,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_owl_OntologyProperty))
| iext(sK10(uri_rdfs_subPropertyOf,uri_owl_OntologyProperty),X1,X2)
| ~ iext(X0,X1,X2) ) ).
cnf(u2687,axiom,
ic(X0) ).
cnf(u8840,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdfs_Container),X0) ).
cnf(u18747,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_OntologyProperty),X0) ).
cnf(u2800,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Resource) ).
cnf(u6381,axiom,
iext(uri_rdfs_range,X0,uri_rdf_List) ).
cnf(u7643,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdf_Alt),X0) ).
cnf(u8723,axiom,
iext(uri_rdfs_member,uri_owl_onProperty,X0) ).
cnf(u7546,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,uri_rdf__1)
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u4680,axiom,
iext(uri_rdfs_range,uri_owl_onProperty,X0) ).
cnf(u9339,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq) ).
cnf(u2790,axiom,
( iext(sK15(uri_rdfs_subPropertyOf,X0),sK11(sK14(uri_rdfs_subPropertyOf,X0),X1),sK12(sK14(uri_rdfs_subPropertyOf,X0),X1))
| iext(uri_rdfs_range,sK14(uri_rdfs_subPropertyOf,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u9108,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u17629,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_owl_OntologyProperty),X0) ).
cnf(u8413,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_domain,uri_rdf_Bag))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u5183,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,uri_owl_complementOf)
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u9631,axiom,
~ iext(uri_rdf__2,X0,X1) ).
cnf(u8853,axiom,
( iext(uri_rdfs_member,sK13(uri_owl_Ontology,X0),uri_owl_Ontology)
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ) ).
cnf(u4688,axiom,
iext(uri_rdfs_subPropertyOf,uri_owl_hasValue,X0) ).
cnf(u11215,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral))
| iext(sK10(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral),X1,X2)
| ~ iext(X0,X1,X2) ) ).
cnf(u7636,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdf_Alt),X0,X1) ).
cnf(u8702,axiom,
iext(uri_rdfs_member,uri_owl_DatatypeProperty,X0) ).
cnf(u19688,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral),sK10(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral)) ).
cnf(u8627,axiom,
( ~ iext(X2,X0,X1)
| iext(uri_rdfs_member,X0,X1) ) ).
cnf(u8068,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdfs_Container),X0) ).
cnf(u18755,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u1709,axiom,
~ icext(sK4(uri_rdfs_Datatype),X0) ).
cnf(u10688,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),X0,X1) ).
cnf(u370,axiom,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property) ).
cnf(u16211,axiom,
( icext(sK12(uri_rdfs_range,X0),sK10(sK11(uri_rdfs_range,X0),uri_owl_OntologyProperty))
| iext(uri_rdfs_domain,sK11(uri_rdfs_range,X0),uri_owl_OntologyProperty)
| iext(uri_rdfs_range,uri_rdfs_range,X0) ) ).
cnf(u6939,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdfs_Datatype),X0,X1) ).
cnf(u18721,axiom,
( icext(sK10(uri_rdf_type,X0),sK9(uri_rdf_type,X0))
| iext(uri_rdfs_domain,uri_rdf_type,X0) ) ).
cnf(u8712,axiom,
iext(uri_rdfs_member,uri_owl_allValuesFrom,X0) ).
cnf(u11201,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing))
| iext(sK10(uri_rdfs_subPropertyOf,uri_owl_Nothing),X1,X2)
| ~ iext(X0,X1,X2) ) ).
cnf(u8639,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_Class) ).
cnf(u10693,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),X0) ).
cnf(u9531,axiom,
( icext(sK12(uri_rdfs_range,X0),sK10(sK11(uri_rdfs_range,X0),uri_rdf_XMLLiteral))
| iext(uri_rdfs_domain,sK11(uri_rdfs_range,X0),uri_rdf_XMLLiteral)
| iext(uri_rdfs_range,uri_rdfs_range,X0) ) ).
cnf(u8664,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_Literal) ).
cnf(u6055,axiom,
icext(uri_rdfs_Literal,X0) ).
cnf(u8280,axiom,
iext(uri_rdfs_domain,X0,uri_rdf_Bag) ).
cnf(u4678,axiom,
iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0) ).
cnf(u7088,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdfs_Datatype),X0) ).
cnf(u11213,axiom,
( ~ iext(sK9(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral),sK14(X0,sK10(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral)),sK15(X0,sK10(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral)))
| iext(uri_rdfs_subPropertyOf,X0,sK10(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral)) ) ).
cnf(u348,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,X1)
| icext(X1,X2)
| ~ icext(X0,X2) ) ).
cnf(u11000,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement) ).
cnf(u8706,axiom,
iext(uri_rdfs_member,uri_rdf_Property,uri_rdf_nil) ).
cnf(u7713,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_domain,uri_rdf_Alt))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u18719,axiom,
iext(uri_rdfs_domain,uri_rdf_first,X0) ).
cnf(u11087,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_range,uri_rdfs_Statement))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u7508,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_rdf_Alt))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u6419,axiom,
( iext(sK15(uri_rdfs_subPropertyOf,X0),sK9(sK14(uri_rdfs_subPropertyOf,X0),uri_rdf_Alt),sK10(sK14(uri_rdfs_subPropertyOf,X0),uri_rdf_Alt))
| iext(uri_rdfs_domain,sK14(uri_rdfs_subPropertyOf,X0),uri_rdf_Alt)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u8277,axiom,
iext(uri_owl_intersectionOf,uri_rdf_Bag,uri_rdf_nil) ).
cnf(u18757,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Seq),X0) ).
cnf(u19669,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing),sK10(uri_rdfs_subPropertyOf,uri_owl_Nothing)) ).
cnf(u9102,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u12674,axiom,
iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,uri_owl_AnnotationProperty),X0) ).
cnf(u311,axiom,
( ~ ix(X0)
| iext(uri_rdf_type,X0,uri_owl_Ontology) ) ).
cnf(u8654,axiom,
iext(uri_rdfs_member,X0,uri_rdf_List) ).
cnf(u9473,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_domain,uri_rdfs_Seq))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u18718,axiom,
iext(uri_rdfs_domain,uri_owl_complementOf,X0) ).
cnf(u6069,axiom,
( icext(sK12(uri_rdfs_subClassOf,X0),sK13(sK11(uri_rdfs_subClassOf,X0),X1))
| iext(uri_rdfs_range,uri_rdfs_subClassOf,X0)
| iext(uri_rdfs_subClassOf,sK11(uri_rdfs_subClassOf,X0),X1) ) ).
cnf(u16216,axiom,
( iext(sK15(uri_rdfs_subPropertyOf,X0),sK9(sK14(uri_rdfs_subPropertyOf,X0),uri_owl_OntologyProperty),sK10(sK14(uri_rdfs_subPropertyOf,X0),uri_owl_OntologyProperty))
| iext(uri_rdfs_domain,sK14(uri_rdfs_subPropertyOf,X0),uri_owl_OntologyProperty)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u2639,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Resource,uri_rdf_nil) ).
cnf(u7893,axiom,
( icext(sK15(uri_rdfs_range,X0),sK10(sK14(uri_rdfs_range,X0),uri_owl_Nothing))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0)
| iext(uri_rdfs_domain,sK14(uri_rdfs_range,X0),uri_owl_Nothing) ) ).
cnf(u5897,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Datatype) ).
cnf(u19118,axiom,
( icext(sK10(uri_rdfs_domain,X0),sK14(sK9(uri_rdfs_domain,X0),X1))
| iext(uri_rdfs_domain,uri_rdfs_domain,X0)
| iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,X0),X1) ) ).
cnf(u8650,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_Datatype) ).
cnf(u623,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_isDefinedBy)
| iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_seeAlso) ) ).
cnf(u1566,axiom,
iext(uri_rdf_type,sK4(uri_owl_Ontology),uri_owl_Ontology) ).
cnf(u18768,axiom,
( icext(sK15(uri_rdfs_domain,X0),sK9(sK14(uri_rdfs_domain,X0),X1))
| iext(uri_rdfs_domain,sK14(uri_rdfs_domain,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0) ) ).
cnf(u15406,axiom,
( ~ iext(sK9(uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty),sK14(X0,sK10(uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty)),sK15(X0,sK10(uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty)))
| iext(uri_rdfs_subPropertyOf,X0,sK10(uri_rdfs_subPropertyOf,uri_owl_DatatypeProperty)) ) ).
cnf(u18745,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_DatatypeProperty),X0) ).
cnf(u9396,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdfs_Seq),X0) ).
cnf(u6562,axiom,
~ iext(uri_rdf__1,X0,X1) ).
cnf(u2666,axiom,
icext(uri_rdfs_Class,X0) ).
cnf(u19359,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,X1))
| iext(uri_rdfs_domain,uri_rdfs_subClassOf,X1)
| ~ iext(uri_rdfs_subClassOf,X2,X0)
| iext(uri_rdfs_subClassOf,X2,sK10(uri_rdfs_subClassOf,X1)) ) ).
cnf(u5947,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf__1)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u796,axiom,
icext(uri_owl_Thing,X0) ).
cnf(u7706,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdf_Alt),X0) ).
cnf(u1366,axiom,
( ~ iext(uri_owl_intersectionOf,X0,uri_rdf_nil)
| icext(X0,X1) ) ).
cnf(u17141,axiom,
iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,uri_owl_OntologyProperty),X0) ).
cnf(u285,axiom,
( iext(uri_rdf_type,X0,uri_rdfs_Class)
| ~ ic(X0) ) ).
cnf(u2765,axiom,
( icext(sK12(uri_rdf_type,X0),sK11(uri_rdf_type,X0))
| iext(uri_rdfs_range,uri_rdf_type,X0) ) ).
cnf(u11200,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing))
| ~ iext(uri_rdfs_subPropertyOf,X1,X0)
| iext(uri_rdfs_subPropertyOf,X1,sK10(uri_rdfs_subPropertyOf,uri_owl_Nothing)) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB016+3 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.38 % Computer : n018.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Mon Sep 28 07:02:25 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.41 Running first-order model finding
% 0.09/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.21/0.82 % (3195347)Will run a generic schedule for satisfiability detection.
% 2.21/0.82 % (3195355)dis+10_1_sil=32000:sp=arity:random_seed=3561927262:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.21/0.82 % (3195353)% WARNING: option uhcvi not known.
% 2.21/0.82 % (3195352)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=745196357_2999 on theBenchmark for (2999ds/0Mi)
% 2.21/0.82 % (3195353)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2179099741:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.21/0.82 % (3195354)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4123578100:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.21/0.82 % (3195356)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3504906494:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.21/0.82 % (3195357)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1689022960:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.21/0.82 % (3195358)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4128490898:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.21/0.82 % TRYING [1]
% 2.21/0.82 % TRYING [2]
% 2.21/0.82 % TRYING [3]
% 2.21/0.82 % (3195355)Instruction limit reached!
% 2.21/0.82 % (3195355)------------------------------
% 2.21/0.82 % (3195355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.21/0.82 % (3195355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/0.82 % (3195355)CaDiCaL version: 2.1.3
% 2.21/0.82 % (3195355)Termination reason: Instruction limit
% 2.21/0.82 % (3195355)Termination phase: Saturation
% 2.21/0.82 % (3195355)Time elapsed: 0.035 s
% 2.21/0.82 % (3195355)Peak memory usage: 13 MB
% 2.21/0.82 % (3195355)Instructions burned: 104 (million)
% 2.21/0.82 % (3195366)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3924752160:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.21/0.82 % TRYING [1]
% 2.21/0.82 % TRYING [2]
% 2.21/0.82 % TRYING [3]
% 2.21/0.82 % (3195356)Instruction limit reached!
% 2.21/0.82 % (3195356)------------------------------
% 2.21/0.82 % (3195356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.21/0.82 % (3195356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/0.82 % (3195356)CaDiCaL version: 2.1.3
% 2.21/0.82 % (3195356)Termination reason: Instruction limit
% 2.21/0.82 % (3195356)Termination phase: Saturation
% 2.21/0.82 % (3195356)Time elapsed: 0.050 s
% 2.21/0.82 % (3195356)Peak memory usage: 11 MB
% 2.21/0.82 % (3195356)Instructions burned: 117 (million)
% 2.21/0.82 % TRYING [4]
% 2.21/0.82 % TRYING [4]
% 2.21/0.82 % (3195357)Instruction limit reached!
% 2.21/0.82 % (3195357)------------------------------
% 2.21/0.82 % (3195357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.21/0.82 % (3195357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/0.82 % (3195357)CaDiCaL version: 2.1.3
% 2.21/0.82 % (3195357)Termination reason: Instruction limit
% 2.21/0.82 % (3195357)Termination phase: Saturation
% 2.21/0.82 % (3195357)Time elapsed: 0.069 s
% 2.21/0.82 % (3195357)Peak memory usage: 13 MB
% 2.21/0.82 % (3195357)Instructions burned: 131 (million)
% 2.21/0.82 % (3195368)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3250058269:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.21/0.82 % (3195358)Instruction limit reached!
% 2.21/0.82 % (3195358)------------------------------
% 2.21/0.82 % (3195358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.21/0.82 % (3195358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/0.82 % (3195358)CaDiCaL version: 2.1.3
% 2.21/0.82 % (3195358)Termination reason: Instruction limit
% 2.21/0.82 % (3195358)Termination phase: Saturation
% 2.21/0.82 % (3195358)Time elapsed: 0.088 s
% 2.21/0.82 % (3195358)Peak memory usage: 14 MB
% 2.21/0.82 % (3195358)Instructions burned: 160 (million)
% 2.21/0.82 % (3195370)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1295926366:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 2.21/0.82 % (3195371)ott-21_1_sil=16000:fs=off:random_seed=4083997063:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 2.21/0.82 % (3195368)Instruction limit reached!
% 2.21/0.82 % (3195368)------------------------------
% 2.21/0.82 % (3195368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.21/0.82 % (3195368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/0.82 % (3195368)CaDiCaL version: 2.1.3
% 2.21/0.82 % (3195368)Termination reason: Instruction limit
% 2.21/0.82 % (3195368)Termination phase: Saturation
% 2.21/0.82 % (3195368)Time elapsed: 0.069 s
% 2.21/0.82 % (3195368)Peak memory usage: 13 MB
% 2.21/0.82 % (3195368)Instructions burned: 133 (million)
% 2.21/0.82 % (3195374)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3371803082:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 2.21/0.82 % (3195371)Instruction limit reached!
% 2.21/0.82 % (3195371)------------------------------
% 2.21/0.82 % (3195371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.21/0.82 % (3195371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/0.82 % (3195371)CaDiCaL version: 2.1.3
% 2.21/0.82 % (3195371)Termination reason: Instruction limit
% 2.21/0.82 % (3195371)Termination phase: Saturation
% 2.21/0.82 % (3195371)Time elapsed: 0.091 s
% 2.21/0.82 % (3195371)Peak memory usage: 13 MB
% 2.21/0.82 % (3195371)Instructions burned: 180 (million)
% 2.21/0.82 % TRYING [5]
% 2.21/0.82 % (3195376)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3553347029:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 2.21/0.82 % (3195366)Instruction limit reached!
% 2.21/0.82 % (3195366)------------------------------
% 2.21/0.82 % (3195366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.21/0.82 % (3195366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/0.82 % (3195366)CaDiCaL version: 2.1.3
% 2.21/0.82 % (3195366)Termination reason: Instruction limit
% 2.21/0.82 % (3195366)Termination phase: Finite model building constraint generation
% 2.21/0.82 % (3195366)Time elapsed: 0.185 s
% 2.21/0.82 % (3195366)Peak memory usage: 27 MB
% 2.21/0.82 % (3195366)Instructions burned: 716 (million)
% 2.21/0.82 % TRYING [1]
% 2.21/0.82 % (3195378)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=352144870:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 2.21/0.82 % TRYING [2]
% 2.21/0.82 % TRYING [3]
% 2.21/0.82 % TRYING [5]
% 2.21/0.82 % TRYING [4]
% 2.21/0.82 % (3195370) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3195347-3195370"...
% 2.21/0.82 % (3195370)...printing done.
% 2.21/0.82 % SZS status CounterSatisfiable for theBenchmark
% 2.21/0.82 % SZS output start Saturation.
% See solution above
% 2.21/0.84 % SZS output start Definitions and Model Updates.
% 2.21/0.84 for all groundings,
% 2.21/0.84 whenever iext(uri_rdf_type,X0,uri_rdfs_Datatype) is false, set ~idc(X0) to true
% 2.21/0.84 for all groundings,
% 2.21/0.84 whenever iext(uri_rdf_type,X0,uri_owl_AnnotationProperty) is false, set ~ioap(X0) to true
% 2.21/0.84 for all groundings,
% 2.21/0.84 whenever iext(uri_rdf_type,X0,uri_owl_DatatypeProperty) is false, set ~iodp(X0) to true
% 2.21/0.84 for all groundings,
% 2.21/0.84 whenever iext(uri_rdf_type,X0,uri_owl_OntologyProperty) is false, set ~ioxp(X0) to true
% 2.21/0.84 % SZS output end Definitions and Model Updates.
% 2.21/0.84 % (3195370)------------------------------
% 2.21/0.84 % (3195370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.21/0.84 % (3195370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/0.84 % (3195370)CaDiCaL version: 2.1.3
% 2.21/0.84 % (3195370)Termination reason: Satisfiable
% 2.21/0.84 % (3195370)Time elapsed: 0.265 s
% 2.21/0.84 % (3195370)Peak memory usage: 18 MB
% 2.21/0.84 % (3195370)Instructions burned: 452 (million)
% 2.21/0.84 % (3195347)Success in time 0.4 s
% 2.21/0.84 % Vampire exiting
%------------------------------------------------------------------------------