%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWB028+3 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n026.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:48 PM UTC 2026
% Result : CounterSatisfiable 1.89s 0.80s
% Output : Saturation 1.89s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u464,axiom,
ic(uri_rdfs_Resource) ).
cnf(u495,axiom,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_rdfs_Resource) ).
cnf(u737,axiom,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_owl_Thing) ).
cnf(u1014,axiom,
( ioap(sK13(uri_owl_AnnotationProperty,X0))
| iext(uri_rdfs_subClassOf,uri_owl_AnnotationProperty,X0)
| ~ ic(X0) ) ).
cnf(u1023,axiom,
( iodp(sK13(uri_owl_DatatypeProperty,X0))
| iext(uri_rdfs_subClassOf,uri_owl_DatatypeProperty,X0)
| ~ ic(X0) ) ).
cnf(u1032,axiom,
( ioxp(sK13(uri_owl_OntologyProperty,X0))
| iext(uri_rdfs_subClassOf,uri_owl_OntologyProperty,X0)
| ~ ic(X0) ) ).
cnf(u1065,axiom,
( ix(sK13(uri_owl_Ontology,X0))
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0)
| ~ ic(X0) ) ).
cnf(u1145,axiom,
iext(uri_owl_unionOf,uri_owl_FunctionalProperty,uri_rdf_nil) ).
cnf(u1158,axiom,
icext(uri_rdfs_Statement,sK4(uri_rdfs_Statement)) ).
cnf(u1163,axiom,
iext(uri_owl_unionOf,uri_rdf_XMLLiteral,uri_rdf_nil) ).
cnf(u1172,axiom,
iext(uri_owl_unionOf,uri_rdfs_Seq,uri_rdf_nil) ).
cnf(u1180,axiom,
~ iext(uri_owl_unionOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_nil) ).
cnf(u1185,axiom,
icext(uri_rdfs_ContainerMembershipProperty,sK4(uri_rdfs_ContainerMembershipProperty)) ).
cnf(u1194,axiom,
icext(uri_rdf_Bag,sK4(uri_rdf_Bag)) ).
cnf(u1198,axiom,
~ iext(uri_owl_unionOf,uri_rdfs_Container,uri_rdf_nil) ).
cnf(u1203,axiom,
icext(uri_rdfs_Container,sK4(uri_rdfs_Container)) ).
cnf(u1208,axiom,
iext(uri_owl_unionOf,uri_rdf_Alt,uri_rdf_nil) ).
cnf(u1221,axiom,
icext(uri_rdf_List,sK4(uri_rdf_List)) ).
cnf(u1230,axiom,
icext(uri_rdfs_Literal,sK4(uri_rdfs_Literal)) ).
cnf(u1239,axiom,
icext(uri_rdf_Property,sK4(uri_rdf_Property)) ).
cnf(u1248,axiom,
icext(uri_rdfs_Datatype,sK4(uri_rdfs_Datatype)) ).
cnf(u1257,axiom,
icext(uri_rdfs_Class,sK4(uri_rdfs_Class)) ).
cnf(u1359,axiom,
iext(uri_owl_unionOf,sK4(uri_rdfs_Datatype),uri_rdf_nil) ).
cnf(u1410,axiom,
iext(uri_owl_unionOf,sK4(uri_rdfs_Class),uri_rdf_nil) ).
cnf(u1522,axiom,
icext(uri_rdfs_Class,uri_owl_Nothing) ).
cnf(u1560,axiom,
icext(uri_rdfs_Class,uri_rdfs_Literal) ).
cnf(u1565,axiom,
icext(uri_rdfs_Class,uri_rdfs_Class) ).
cnf(u1571,axiom,
~ iext(uri_owl_unionOf,uri_owl_Restriction,uri_rdf_nil) ).
cnf(u1576,axiom,
icext(uri_owl_Restriction,sK4(uri_owl_Restriction)) ).
cnf(u1624,axiom,
icext(uri_rdfs_Class,uri_owl_FunctionalProperty) ).
cnf(u1629,axiom,
iext(uri_rdfs_subClassOf,uri_owl_FunctionalProperty,uri_owl_Thing) ).
cnf(u1634,axiom,
iext(uri_rdfs_subClassOf,uri_owl_FunctionalProperty,uri_rdfs_Resource) ).
cnf(u1639,axiom,
iext(uri_rdfs_subClassOf,uri_owl_FunctionalProperty,uri_rdfs_Literal) ).
cnf(u1754,axiom,
icext(uri_rdfs_Class,uri_rdfs_Container) ).
cnf(u2026,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_member) ).
cnf(u2156,axiom,
iext(uri_owl_intersectionOf,uri_rdf_Property,uri_rdf_nil) ).
cnf(u2165,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Class,uri_rdf_nil) ).
cnf(u2278,axiom,
~ icext(sK18,X1) ).
cnf(u2386,axiom,
( ~ ic(X0)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_Property) ) ).
cnf(u2396,axiom,
ic(sK18) ).
cnf(u2400,axiom,
( iext(uri_rdfs_subClassOf,sK18,X0)
| ~ ic(X0) ) ).
cnf(u2405,axiom,
iext(uri_rdfs_domain,X0,uri_rdf_Property) ).
cnf(u3055,axiom,
icext(uri_rdfs_Class,sK18) ).
cnf(u3312,axiom,
iext(uri_rdfs_subClassOf,sK18,uri_rdfs_Resource) ).
cnf(u3520,axiom,
iext(uri_rdfs_subClassOf,sK18,uri_owl_Thing) ).
cnf(u3810,axiom,
iext(uri_rdfs_subClassOf,sK4(uri_rdfs_Class),uri_rdf_Property) ).
cnf(u3815,axiom,
iext(uri_rdfs_subClassOf,sK4(uri_rdfs_Class),uri_owl_Thing) ).
cnf(u3820,axiom,
iext(uri_rdfs_subClassOf,sK4(uri_rdfs_Class),uri_rdfs_Resource) ).
cnf(u4167,axiom,
ix(sK4(uri_owl_Ontology)) ).
cnf(u4180,axiom,
iext(uri_owl_unionOf,uri_owl_OntologyProperty,uri_rdf_nil) ).
cnf(u4189,axiom,
iext(uri_owl_unionOf,uri_owl_DatatypeProperty,uri_rdf_nil) ).
cnf(u4198,axiom,
iext(uri_owl_unionOf,uri_owl_AnnotationProperty,uri_rdf_nil) ).
cnf(u5027,axiom,
iext(uri_rdfs_domain,sK4(uri_rdfs_ContainerMembershipProperty),uri_owl_Nothing) ).
cnf(u5036,axiom,
iext(uri_rdfs_domain,uri_rdf_predicate,uri_owl_Nothing) ).
cnf(u5041,axiom,
icext(uri_rdfs_Literal,sK10(uri_rdfs_label,uri_owl_Nothing)) ).
cnf(u5045,axiom,
iext(uri_rdfs_domain,uri_rdfs_label,uri_owl_Nothing) ).
cnf(u5054,axiom,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_owl_Nothing) ).
cnf(u5064,axiom,
icext(uri_rdfs_Literal,sK10(uri_rdfs_comment,uri_owl_Nothing)) ).
cnf(u5077,axiom,
iext(uri_rdfs_domain,uri_rdf_subject,uri_owl_Nothing) ).
cnf(u5082,axiom,
icext(uri_rdfs_Statement,sK9(uri_rdf_object,uri_owl_Nothing)) ).
cnf(u5086,axiom,
iext(uri_rdfs_domain,uri_rdf_object,uri_owl_Nothing) ).
cnf(u5091,axiom,
iext(uri_rdfs_member,sK9(uri_rdf__3,uri_owl_Nothing),sK10(uri_rdf__3,uri_owl_Nothing)) ).
cnf(u5100,axiom,
iext(uri_rdfs_member,sK9(uri_rdf__2,uri_owl_Nothing),sK10(uri_rdf__2,uri_owl_Nothing)) ).
cnf(u5104,axiom,
iext(uri_rdfs_domain,uri_rdf__2,uri_owl_Nothing) ).
cnf(u5109,axiom,
iext(uri_rdfs_member,sK9(uri_rdf__1,uri_owl_Nothing),sK10(uri_rdf__1,uri_owl_Nothing)) ).
cnf(u5113,axiom,
iext(uri_rdfs_domain,uri_rdf__1,uri_owl_Nothing) ).
cnf(u5117,axiom,
( iext(sK10(uri_rdfs_subPropertyOf,uri_owl_Nothing),X0,X1)
| ~ iext(sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing),X0,X1) ) ).
cnf(u5120,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_owl_Nothing) ).
cnf(u5125,axiom,
( ~ iext(uri_rdfs_subPropertyOf,sK10(uri_rdfs_subPropertyOf,uri_owl_Nothing),X0)
| iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing),X0) ) ).
cnf(u5129,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(u5132,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_owl_Nothing) ).
cnf(u5137,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,uri_owl_Nothing),X0)
| icext(sK10(uri_rdfs_subClassOf,uri_owl_Nothing),X0) ) ).
cnf(u5141,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_owl_Nothing),X1,X0)
| icext(sK10(uri_rdfs_range,uri_owl_Nothing),X0) ) ).
cnf(u5149,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_owl_Nothing),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_owl_Nothing),X0) ) ).
cnf(u5158,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_someValuesFrom,uri_owl_Nothing)) ).
cnf(u5161,axiom,
~ iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_owl_Nothing) ).
cnf(u5166,axiom,
( icext(sK10(uri_owl_someValuesFrom,uri_owl_Nothing),sK17(X0,sK10(uri_owl_someValuesFrom,uri_owl_Nothing),X1))
| ~ icext(sK9(uri_owl_someValuesFrom,uri_owl_Nothing),X1)
| ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,uri_owl_Nothing),X0) ) ).
cnf(u5170,axiom,
( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,uri_owl_Nothing),X0)
| ~ icext(sK9(uri_owl_someValuesFrom,uri_owl_Nothing),X1)
| iext(X0,X1,sK17(X0,sK10(uri_owl_someValuesFrom,uri_owl_Nothing),X1)) ) ).
cnf(u5174,axiom,
( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,uri_owl_Nothing),X0)
| icext(sK9(uri_owl_someValuesFrom,uri_owl_Nothing),X2)
| ~ iext(X0,X2,X1)
| ~ icext(sK10(uri_owl_someValuesFrom,uri_owl_Nothing),X1) ) ).
cnf(u5179,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_onProperty,uri_owl_Nothing)) ).
cnf(u5192,axiom,
iext(uri_rdfs_domain,uri_owl_hasValue,uri_owl_Nothing) ).
cnf(u5209,axiom,
iext(uri_rdfs_domain,uri_owl_allValuesFrom,uri_owl_Nothing) ).
cnf(u5226,axiom,
icext(sK10(uri_rdf_type,uri_owl_Nothing),sK9(uri_rdf_type,uri_owl_Nothing)) ).
cnf(u5235,axiom,
icext(uri_rdf_List,sK10(uri_owl_unionOf,uri_owl_Nothing)) ).
cnf(u5238,axiom,
~ iext(uri_rdfs_domain,uri_owl_unionOf,uri_owl_Nothing) ).
cnf(u5248,axiom,
iext(uri_rdfs_domain,uri_rdf_rest,uri_owl_Nothing) ).
cnf(u5258,axiom,
icext(uri_rdf_List,sK9(uri_rdf_first,uri_owl_Nothing)) ).
cnf(u5267,axiom,
icext(uri_rdf_List,sK10(uri_owl_intersectionOf,uri_owl_Nothing)) ).
cnf(u5270,axiom,
~ iext(uri_rdfs_domain,uri_owl_intersectionOf,uri_owl_Nothing) ).
cnf(u5279,axiom,
iext(uri_rdfs_domain,uri_owl_complementOf,uri_owl_Nothing) ).
cnf(u5352,axiom,
iext(uri_rdfs_member,sK9(sK4(uri_rdfs_ContainerMembershipProperty),uri_owl_Thing),sK10(sK4(uri_rdfs_ContainerMembershipProperty),uri_owl_Thing)) ).
cnf(u5365,axiom,
iext(uri_rdfs_domain,uri_rdfs_label,uri_owl_Thing) ).
cnf(u5374,axiom,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_owl_Thing) ).
cnf(u5384,axiom,
icext(uri_rdfs_Literal,sK10(uri_rdfs_comment,uri_owl_Thing)) ).
cnf(u5393,axiom,
icext(uri_rdfs_Statement,sK9(uri_rdf_subject,uri_owl_Thing)) ).
cnf(u5402,axiom,
icext(uri_rdfs_Statement,sK9(uri_rdf_object,uri_owl_Thing)) ).
cnf(u5406,axiom,
iext(uri_rdfs_domain,uri_rdf_object,uri_owl_Thing) ).
cnf(u5411,axiom,
iext(uri_rdfs_member,sK9(uri_rdf__3,uri_owl_Thing),sK10(uri_rdf__3,uri_owl_Thing)) ).
cnf(u5420,axiom,
iext(uri_rdfs_member,sK9(uri_rdf__2,uri_owl_Thing),sK10(uri_rdf__2,uri_owl_Thing)) ).
cnf(u5424,axiom,
iext(uri_rdfs_domain,uri_rdf__2,uri_owl_Thing) ).
cnf(u5429,axiom,
iext(uri_rdfs_member,sK9(uri_rdf__1,uri_owl_Thing),sK10(uri_rdf__1,uri_owl_Thing)) ).
cnf(u5433,axiom,
iext(uri_rdfs_domain,uri_rdf__1,uri_owl_Thing) ).
cnf(u5441,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_owl_Thing) ).
cnf(u5453,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_owl_Thing) ).
cnf(u5461,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_owl_Thing),X1,X0)
| icext(sK10(uri_rdfs_range,uri_owl_Thing),X0) ) ).
cnf(u5473,axiom,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_owl_Thing) ).
cnf(u5482,axiom,
iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_owl_Thing) ).
cnf(u5499,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_onProperty,uri_owl_Thing)) ).
cnf(u5512,axiom,
iext(uri_rdfs_domain,uri_owl_hasValue,uri_owl_Thing) ).
cnf(u5529,axiom,
iext(uri_rdfs_domain,uri_owl_allValuesFrom,uri_owl_Thing) ).
cnf(u5550,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_owl_Thing) ).
cnf(u5559,axiom,
iext(uri_rdfs_domain,uri_owl_unionOf,uri_owl_Thing) ).
cnf(u5568,axiom,
iext(uri_rdfs_domain,uri_rdf_rest,uri_owl_Thing) ).
cnf(u5578,axiom,
icext(uri_rdf_List,sK9(uri_rdf_first,uri_owl_Thing)) ).
cnf(u5587,axiom,
icext(uri_rdf_List,sK10(uri_owl_intersectionOf,uri_owl_Thing)) ).
cnf(u5599,axiom,
iext(uri_rdfs_domain,uri_owl_complementOf,uri_owl_Thing) ).
cnf(u6467,axiom,
iext(uri_owl_unionOf,sK9(uri_rdfs_subClassOf,uri_owl_Nothing),uri_rdf_nil) ).
cnf(u6557,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_Nothing),uri_owl_Thing) ).
cnf(u6570,axiom,
icext(sK10(uri_rdfs_range,uri_owl_Nothing),sK10(sK9(uri_rdfs_range,uri_owl_Nothing),uri_owl_Nothing)) ).
cnf(u6580,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Nothing),uri_owl_Thing) ).
cnf(u6593,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK9(sK9(uri_rdfs_domain,uri_owl_Nothing),uri_owl_Nothing)) ).
cnf(u6603,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_Thing),uri_owl_Thing) ).
cnf(u6616,axiom,
icext(sK10(uri_rdfs_range,uri_owl_Thing),sK10(sK9(uri_rdfs_range,uri_owl_Thing),uri_owl_Nothing)) ).
cnf(u6697,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_Thing),uri_rdfs_Datatype) ).
cnf(u6706,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Nothing),uri_rdfs_Datatype) ).
cnf(u6711,axiom,
icext(sK10(uri_rdfs_range,uri_owl_Nothing),sK10(sK9(uri_rdfs_range,uri_owl_Nothing),uri_rdfs_Datatype)) ).
cnf(u6724,axiom,
iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Datatype) ).
cnf(u6729,axiom,
icext(uri_rdfs_Literal,sK10(uri_rdfs_comment,uri_rdfs_Datatype)) ).
cnf(u6738,axiom,
icext(uri_rdfs_Statement,sK9(uri_rdf_object,uri_rdfs_Datatype)) ).
cnf(u6747,axiom,
iext(uri_rdfs_member,sK9(uri_rdf__3,uri_rdfs_Datatype),sK10(uri_rdf__3,uri_rdfs_Datatype)) ).
cnf(u6760,axiom,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Datatype) ).
cnf(u6765,axiom,
iext(uri_rdfs_member,sK9(uri_rdf__1,uri_rdfs_Datatype),sK10(uri_rdf__1,uri_rdfs_Datatype)) ).
cnf(u6777,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdfs_Datatype) ).
cnf(u6789,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Datatype) ).
cnf(u6797,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdfs_Datatype),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdfs_Datatype),X0) ) ).
cnf(u6805,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdfs_Datatype),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdfs_Datatype),X0) ) ).
cnf(u6818,axiom,
iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_rdfs_Datatype) ).
cnf(u6835,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_onProperty,uri_rdfs_Datatype)) ).
cnf(u6848,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Datatype) ).
cnf(u6857,axiom,
iext(uri_rdfs_domain,uri_owl_unionOf,uri_rdfs_Datatype) ).
cnf(u6866,axiom,
iext(uri_rdfs_domain,uri_rdf_first,uri_rdfs_Datatype) ).
cnf(u6871,axiom,
icext(uri_rdf_List,sK10(uri_owl_intersectionOf,uri_rdfs_Datatype)) ).
cnf(u7081,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Datatype),uri_owl_Thing) ).
cnf(u7094,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Datatype),sK10(sK9(uri_rdfs_range,uri_rdfs_Datatype),uri_owl_Nothing)) ).
cnf(u7104,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Datatype),uri_owl_Thing) ).
cnf(u7117,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Datatype),sK9(sK9(uri_rdfs_domain,uri_rdfs_Datatype),uri_owl_Nothing)) ).
cnf(u7163,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Datatype),uri_rdf_List) ).
cnf(u7172,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Datatype),uri_rdf_List) ).
cnf(u7177,axiom,
icext(sK10(uri_rdfs_range,uri_owl_Thing),sK10(sK9(uri_rdfs_range,uri_owl_Thing),uri_rdf_List)) ).
cnf(u7190,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Nothing),uri_rdf_List) ).
cnf(u7195,axiom,
icext(sK10(uri_rdfs_range,uri_owl_Nothing),sK10(sK9(uri_rdfs_range,uri_owl_Nothing),uri_rdf_List)) ).
cnf(u7204,axiom,
icext(uri_rdfs_Statement,sK9(uri_rdf_object,uri_rdf_List)) ).
cnf(u7213,axiom,
iext(uri_rdfs_member,sK9(uri_rdf__3,uri_rdf_List),sK10(uri_rdf__3,uri_rdf_List)) ).
cnf(u7226,axiom,
iext(uri_rdfs_domain,uri_rdf__1,uri_rdf_List) ).
cnf(u7234,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_List) ).
cnf(u7246,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdf_List) ).
cnf(u7254,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdf_List),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdf_List),X0) ) ).
cnf(u7266,axiom,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_List) ).
cnf(u7275,axiom,
iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_rdf_List) ).
cnf(u7292,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_onProperty,uri_rdf_List)) ).
cnf(u7305,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdf_List) ).
cnf(u7314,axiom,
iext(uri_rdfs_domain,uri_owl_unionOf,uri_rdf_List) ).
cnf(u7319,axiom,
icext(uri_rdf_List,sK10(uri_owl_intersectionOf,uri_rdf_List)) ).
cnf(u7417,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_List),uri_owl_Thing) ).
cnf(u7430,axiom,
icext(sK10(uri_rdfs_range,uri_rdf_List),sK10(sK9(uri_rdfs_range,uri_rdf_List),uri_owl_Nothing)) ).
cnf(u7475,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_List),uri_rdf_Alt) ).
cnf(u7484,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Datatype),uri_rdf_Alt) ).
cnf(u7489,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Datatype),sK10(sK9(uri_rdfs_range,uri_rdfs_Datatype),uri_rdf_Alt)) ).
cnf(u7502,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_Thing),uri_rdf_Alt) ).
cnf(u7507,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK9(sK9(uri_rdfs_domain,uri_owl_Nothing),uri_rdf_Alt)) ).
cnf(u7516,axiom,
icext(sK10(uri_rdfs_range,uri_owl_Nothing),sK10(sK9(uri_rdfs_range,uri_owl_Nothing),uri_rdf_Alt)) ).
cnf(u7525,axiom,
icext(uri_rdfs_Statement,sK9(uri_rdf_object,uri_rdf_Alt)) ).
cnf(u7538,axiom,
iext(uri_rdfs_domain,uri_rdf__3,uri_rdf_Alt) ).
cnf(u7542,axiom,
( iext(sK10(uri_rdfs_subPropertyOf,uri_rdf_Alt),X0,X1)
| ~ iext(sK9(uri_rdfs_subPropertyOf,uri_rdf_Alt),X0,X1) ) ).
cnf(u7545,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Alt) ).
cnf(u7550,axiom,
( ~ iext(uri_rdfs_subPropertyOf,sK10(uri_rdfs_subPropertyOf,uri_rdf_Alt),X0)
| iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_rdf_Alt),X0) ) ).
cnf(u7554,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,uri_rdf_Alt),X0)
| icext(sK10(uri_rdfs_subClassOf,uri_rdf_Alt),X0) ) ).
cnf(u7557,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdf_Alt) ).
cnf(u7562,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(u7566,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdf_Alt),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdf_Alt),X0) ) ).
cnf(u7574,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdf_Alt),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdf_Alt),X0) ) ).
cnf(u7577,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Alt) ).
cnf(u7583,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_someValuesFrom,uri_rdf_Alt)) ).
cnf(u7586,axiom,
~ iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_rdf_Alt) ).
cnf(u7591,axiom,
( icext(sK10(uri_owl_someValuesFrom,uri_rdf_Alt),sK17(X0,sK10(uri_owl_someValuesFrom,uri_rdf_Alt),X1))
| ~ icext(sK9(uri_owl_someValuesFrom,uri_rdf_Alt),X1)
| ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,uri_rdf_Alt),X0) ) ).
cnf(u7595,axiom,
( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,uri_rdf_Alt),X0)
| ~ icext(sK9(uri_owl_someValuesFrom,uri_rdf_Alt),X1)
| iext(X0,X1,sK17(X0,sK10(uri_owl_someValuesFrom,uri_rdf_Alt),X1)) ) ).
cnf(u7599,axiom,
( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,uri_rdf_Alt),X0)
| icext(sK9(uri_owl_someValuesFrom,uri_rdf_Alt),X2)
| ~ iext(X0,X2,X1)
| ~ icext(sK10(uri_owl_someValuesFrom,uri_rdf_Alt),X1) ) ).
cnf(u7604,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_onProperty,uri_rdf_Alt)) ).
cnf(u7607,axiom,
~ iext(uri_rdfs_domain,uri_owl_onProperty,uri_rdf_Alt) ).
cnf(u7613,axiom,
icext(sK10(uri_rdf_type,uri_rdf_Alt),sK9(uri_rdf_type,uri_rdf_Alt)) ).
cnf(u8545,axiom,
iext(uri_owl_unionOf,sK9(uri_rdfs_subClassOf,uri_rdf_Alt),uri_rdf_nil) ).
cnf(u8612,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_Alt),uri_rdf_Alt) ).
cnf(u8625,axiom,
icext(sK10(uri_rdfs_range,uri_rdf_Alt),sK10(sK9(uri_rdfs_range,uri_rdf_Alt),uri_owl_Thing)) ).
cnf(u8634,axiom,
icext(sK10(uri_rdfs_range,uri_rdf_Alt),sK10(sK9(uri_rdfs_range,uri_rdf_Alt),uri_owl_Nothing)) ).
cnf(u8656,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_Alt),uri_rdf_Alt) ).
cnf(u8669,axiom,
icext(sK10(uri_rdfs_domain,uri_rdf_Alt),sK9(sK9(uri_rdfs_domain,uri_rdf_Alt),uri_owl_Thing)) ).
cnf(u8678,axiom,
icext(sK10(uri_rdfs_domain,uri_rdf_Alt),sK9(sK9(uri_rdfs_domain,uri_rdf_Alt),uri_owl_Nothing)) ).
cnf(u8790,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Datatype),sK10(sK9(uri_rdfs_range,uri_rdfs_Datatype),uri_rdfs_Container)) ).
cnf(u8803,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Nothing),uri_rdfs_Container) ).
cnf(u8808,axiom,
icext(sK10(uri_rdfs_range,uri_owl_Nothing),sK10(sK9(uri_rdfs_range,uri_owl_Nothing),uri_rdfs_Container)) ).
cnf(u8821,axiom,
iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Container) ).
cnf(u8829,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdfs_Container) ).
cnf(u8841,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Container) ).
cnf(u8853,axiom,
iext(uri_rdfs_domain,uri_rdfs_range,uri_rdfs_Container) ).
cnf(u8857,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdfs_Container),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdfs_Container),X0) ) ).
cnf(u8870,axiom,
iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_rdfs_Container) ).
cnf(u8891,axiom,
iext(uri_rdfs_domain,uri_owl_onProperty,uri_rdfs_Container) ).
cnf(u8900,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Container) ).
cnf(u8938,axiom,
icext(uri_rdfs_Container,sK9(uri_rdf_object,uri_rdf_Alt)) ).
cnf(u9014,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Container),uri_rdf_Alt) ).
cnf(u9027,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Container),sK9(sK9(uri_rdfs_domain,uri_rdfs_Container),uri_owl_Thing)) ).
cnf(u9036,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Container),sK9(sK9(uri_rdfs_domain,uri_rdfs_Container),uri_owl_Nothing)) ).
cnf(u9091,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Datatype),sK10(sK9(uri_rdfs_range,uri_rdfs_Datatype),uri_rdf_Bag)) ).
cnf(u9104,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Nothing),uri_rdf_Bag) ).
cnf(u9109,axiom,
icext(sK10(uri_rdfs_range,uri_owl_Nothing),sK10(sK9(uri_rdfs_range,uri_owl_Nothing),uri_rdf_Bag)) ).
cnf(u9121,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Bag) ).
cnf(u9133,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdf_Bag) ).
cnf(u9141,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdf_Bag),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdf_Bag),X0) ) ).
cnf(u9153,axiom,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Bag) ).
cnf(u9162,axiom,
iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_rdf_Bag) ).
cnf(u9183,axiom,
iext(uri_rdfs_domain,uri_owl_onProperty,uri_rdf_Bag) ).
cnf(u9188,axiom,
icext(sK10(uri_rdf_type,uri_rdf_Bag),sK9(uri_rdf_type,uri_rdf_Bag)) ).
cnf(u9264,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_Bag),uri_rdf_Alt) ).
cnf(u9277,axiom,
icext(sK10(uri_rdfs_range,uri_rdf_Bag),sK10(sK9(uri_rdfs_range,uri_rdf_Bag),uri_owl_Thing)) ).
cnf(u9286,axiom,
icext(sK10(uri_rdfs_range,uri_rdf_Bag),sK10(sK9(uri_rdfs_range,uri_rdf_Bag),uri_owl_Nothing)) ).
cnf(u9342,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Datatype),sK10(sK9(uri_rdfs_range,uri_rdfs_Datatype),uri_rdfs_ContainerMembershipProperty)) ).
cnf(u9355,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Nothing),uri_rdfs_ContainerMembershipProperty) ).
cnf(u9360,axiom,
icext(sK10(uri_rdfs_range,uri_owl_Nothing),sK10(sK9(uri_rdfs_range,uri_owl_Nothing),uri_rdfs_ContainerMembershipProperty)) ).
cnf(u9372,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdfs_ContainerMembershipProperty) ).
cnf(u9384,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty) ).
cnf(u9392,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X0) ) ).
cnf(u9404,axiom,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty) ).
cnf(u9413,axiom,
iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_rdfs_ContainerMembershipProperty) ).
cnf(u9434,axiom,
iext(uri_rdfs_domain,uri_owl_onProperty,uri_rdfs_ContainerMembershipProperty) ).
cnf(u9439,axiom,
icext(sK10(uri_rdf_type,uri_rdfs_ContainerMembershipProperty),sK9(uri_rdf_type,uri_rdfs_ContainerMembershipProperty)) ).
cnf(u9869,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),uri_rdf_Alt) ).
cnf(u9882,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),sK10(sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),uri_owl_Thing)) ).
cnf(u9891,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),sK10(sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),uri_owl_Nothing)) ).
cnf(u9957,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Datatype),sK10(sK9(uri_rdfs_range,uri_rdfs_Datatype),uri_rdfs_Seq)) ).
cnf(u9970,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Nothing),uri_rdfs_Seq) ).
cnf(u9975,axiom,
icext(sK10(uri_rdfs_range,uri_owl_Nothing),sK10(sK9(uri_rdfs_range,uri_owl_Nothing),uri_rdfs_Seq)) ).
cnf(u9983,axiom,
( iext(sK10(uri_rdfs_subPropertyOf,uri_rdfs_Seq),X0,X1)
| ~ iext(sK9(uri_rdfs_subPropertyOf,uri_rdfs_Seq),X0,X1) ) ).
cnf(u9986,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdfs_Seq) ).
cnf(u9991,axiom,
( ~ iext(uri_rdfs_subPropertyOf,sK10(uri_rdfs_subPropertyOf,uri_rdfs_Seq),X0)
| iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_rdfs_Seq),X0) ) ).
cnf(u9995,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,uri_rdfs_Seq),X0)
| icext(sK10(uri_rdfs_subClassOf,uri_rdfs_Seq),X0) ) ).
cnf(u9998,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Seq) ).
cnf(u10003,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_rdfs_Seq))
| iext(uri_rdfs_subClassOf,X0,sK10(uri_rdfs_subClassOf,uri_rdfs_Seq)) ) ).
cnf(u10007,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdfs_Seq),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdfs_Seq),X0) ) ).
cnf(u10015,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdfs_Seq),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdfs_Seq),X0) ) ).
cnf(u10018,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdfs_Seq) ).
cnf(u10024,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_someValuesFrom,uri_rdfs_Seq)) ).
cnf(u10027,axiom,
~ iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_rdfs_Seq) ).
cnf(u10032,axiom,
( icext(sK10(uri_owl_someValuesFrom,uri_rdfs_Seq),sK17(X0,sK10(uri_owl_someValuesFrom,uri_rdfs_Seq),X1))
| ~ icext(sK9(uri_owl_someValuesFrom,uri_rdfs_Seq),X1)
| ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,uri_rdfs_Seq),X0) ) ).
cnf(u10036,axiom,
( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,uri_rdfs_Seq),X0)
| ~ icext(sK9(uri_owl_someValuesFrom,uri_rdfs_Seq),X1)
| iext(X0,X1,sK17(X0,sK10(uri_owl_someValuesFrom,uri_rdfs_Seq),X1)) ) ).
cnf(u10040,axiom,
( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,uri_rdfs_Seq),X0)
| icext(sK9(uri_owl_someValuesFrom,uri_rdfs_Seq),X2)
| ~ iext(X0,X2,X1)
| ~ icext(sK10(uri_owl_someValuesFrom,uri_rdfs_Seq),X1) ) ).
cnf(u10045,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_onProperty,uri_rdfs_Seq)) ).
cnf(u10048,axiom,
~ iext(uri_rdfs_domain,uri_owl_onProperty,uri_rdfs_Seq) ).
cnf(u10054,axiom,
icext(sK10(uri_rdf_type,uri_rdfs_Seq),sK9(uri_rdf_type,uri_rdfs_Seq)) ).
cnf(u11102,axiom,
iext(uri_owl_unionOf,sK9(uri_rdfs_subClassOf,uri_rdfs_Seq),uri_rdf_nil) ).
cnf(u11154,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Seq),uri_rdfs_Seq) ).
cnf(u11167,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Seq),sK10(sK9(uri_rdfs_range,uri_rdfs_Seq),uri_rdf_Alt)) ).
cnf(u11176,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Seq),sK10(sK9(uri_rdfs_range,uri_rdfs_Seq),uri_owl_Thing)) ).
cnf(u11185,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Seq),sK10(sK9(uri_rdfs_range,uri_rdfs_Seq),uri_owl_Nothing)) ).
cnf(u11220,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Seq),uri_rdfs_Seq) ).
cnf(u11233,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Seq),sK9(sK9(uri_rdfs_domain,uri_rdfs_Seq),uri_rdf_Alt)) ).
cnf(u11242,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Seq),sK9(sK9(uri_rdfs_domain,uri_rdfs_Seq),uri_owl_Thing)) ).
cnf(u11251,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Seq),sK9(sK9(uri_rdfs_domain,uri_rdfs_Seq),uri_owl_Nothing)) ).
cnf(u11398,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Datatype),sK10(sK9(uri_rdfs_range,uri_rdfs_Datatype),uri_rdf_XMLLiteral)) ).
cnf(u11411,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_Nothing),uri_rdf_XMLLiteral) ).
cnf(u11415,axiom,
( iext(sK10(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral),X0,X1)
| ~ iext(sK9(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral),X0,X1) ) ).
cnf(u11418,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral) ).
cnf(u11423,axiom,
( ~ iext(uri_rdfs_subPropertyOf,sK10(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral),X0)
| iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral),X0) ) ).
cnf(u11427,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,uri_rdf_XMLLiteral),X0)
| icext(sK10(uri_rdfs_subClassOf,uri_rdf_XMLLiteral),X0) ) ).
cnf(u11430,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdf_XMLLiteral) ).
cnf(u11435,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(u11439,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdf_XMLLiteral),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdf_XMLLiteral),X0) ) ).
cnf(u11447,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdf_XMLLiteral),X0) ) ).
cnf(u11456,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_someValuesFrom,uri_rdf_XMLLiteral)) ).
cnf(u11459,axiom,
~ iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_rdf_XMLLiteral) ).
cnf(u11464,axiom,
( icext(sK10(uri_owl_someValuesFrom,uri_rdf_XMLLiteral),sK17(X0,sK10(uri_owl_someValuesFrom,uri_rdf_XMLLiteral),X1))
| ~ icext(sK9(uri_owl_someValuesFrom,uri_rdf_XMLLiteral),X1)
| ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,uri_rdf_XMLLiteral),X0) ) ).
cnf(u11468,axiom,
( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,uri_rdf_XMLLiteral),X0)
| ~ icext(sK9(uri_owl_someValuesFrom,uri_rdf_XMLLiteral),X1)
| iext(X0,X1,sK17(X0,sK10(uri_owl_someValuesFrom,uri_rdf_XMLLiteral),X1)) ) ).
cnf(u11472,axiom,
( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,uri_rdf_XMLLiteral),X0)
| icext(sK9(uri_owl_someValuesFrom,uri_rdf_XMLLiteral),X2)
| ~ iext(X0,X2,X1)
| ~ icext(sK10(uri_owl_someValuesFrom,uri_rdf_XMLLiteral),X1) ) ).
cnf(u11477,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_onProperty,uri_rdf_XMLLiteral)) ).
cnf(u11480,axiom,
~ iext(uri_rdfs_domain,uri_owl_onProperty,uri_rdf_XMLLiteral) ).
cnf(u11486,axiom,
icext(sK10(uri_rdf_type,uri_rdf_XMLLiteral),sK9(uri_rdf_type,uri_rdf_XMLLiteral)) ).
cnf(u11489,axiom,
~ iext(uri_rdfs_domain,uri_rdf_type,uri_rdf_XMLLiteral) ).
cnf(u12386,axiom,
iext(uri_owl_unionOf,sK9(uri_rdfs_subClassOf,uri_rdf_XMLLiteral),uri_rdf_nil) ).
cnf(u12439,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_XMLLiteral),uri_rdf_XMLLiteral) ).
cnf(u12452,axiom,
icext(sK10(uri_rdfs_range,uri_rdf_XMLLiteral),sK10(sK9(uri_rdfs_range,uri_rdf_XMLLiteral),uri_rdfs_Seq)) ).
cnf(u12457,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_XMLLiteral),uri_rdf_Alt) ).
cnf(u12470,axiom,
icext(sK10(uri_rdfs_range,uri_rdf_XMLLiteral),sK10(sK9(uri_rdfs_range,uri_rdf_XMLLiteral),uri_owl_Thing)) ).
cnf(u12479,axiom,
icext(sK10(uri_rdfs_range,uri_rdf_XMLLiteral),sK10(sK9(uri_rdfs_range,uri_rdf_XMLLiteral),uri_owl_Nothing)) ).
cnf(u12522,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),uri_rdf_XMLLiteral) ).
cnf(u12535,axiom,
icext(sK10(uri_rdfs_domain,uri_rdf_XMLLiteral),sK9(sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),uri_rdfs_Seq)) ).
cnf(u12540,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),uri_rdf_Alt) ).
cnf(u12553,axiom,
icext(sK10(uri_rdfs_domain,uri_rdf_XMLLiteral),sK9(sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),uri_owl_Thing)) ).
cnf(u12562,axiom,
icext(sK10(uri_rdfs_domain,uri_rdf_XMLLiteral),sK9(sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),uri_owl_Nothing)) ).
cnf(u12741,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Datatype),uri_rdfs_Statement) ).
cnf(u12749,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdfs_Statement) ).
cnf(u12761,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Statement) ).
cnf(u12769,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdfs_Statement),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdfs_Statement),X0) ) ).
cnf(u12777,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdfs_Statement),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdfs_Statement),X0) ) ).
cnf(u12790,axiom,
iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_rdfs_Statement) ).
cnf(u12811,axiom,
iext(uri_rdfs_domain,uri_owl_onProperty,uri_rdfs_Statement) ).
cnf(u12820,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Statement) ).
cnf(u12930,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Statement),uri_rdf_XMLLiteral) ).
cnf(u12943,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Statement),sK10(sK9(uri_rdfs_range,uri_rdfs_Statement),uri_rdfs_Seq)) ).
cnf(u12948,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Statement),uri_rdf_Alt) ).
cnf(u12961,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Statement),sK10(sK9(uri_rdfs_range,uri_rdfs_Statement),uri_owl_Thing)) ).
cnf(u12970,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Statement),sK10(sK9(uri_rdfs_range,uri_rdfs_Statement),uri_owl_Nothing)) ).
cnf(u13011,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Statement),uri_rdf_XMLLiteral) ).
cnf(u13024,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Statement),sK9(sK9(uri_rdfs_domain,uri_rdfs_Statement),uri_rdfs_Seq)) ).
cnf(u13029,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Statement),uri_rdf_Alt) ).
cnf(u13042,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Statement),sK9(sK9(uri_rdfs_domain,uri_rdfs_Statement),uri_owl_Thing)) ).
cnf(u13051,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Statement),sK9(sK9(uri_rdfs_domain,uri_rdfs_Statement),uri_owl_Nothing)) ).
cnf(u13136,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Datatype),uri_owl_FunctionalProperty) ).
cnf(u13140,axiom,
( iext(sK10(uri_rdfs_subPropertyOf,uri_owl_FunctionalProperty),X0,X1)
| ~ iext(sK9(uri_rdfs_subPropertyOf,uri_owl_FunctionalProperty),X0,X1) ) ).
cnf(u13143,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_owl_FunctionalProperty) ).
cnf(u13148,axiom,
( ~ iext(uri_rdfs_subPropertyOf,sK10(uri_rdfs_subPropertyOf,uri_owl_FunctionalProperty),X0)
| iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_owl_FunctionalProperty),X0) ) ).
cnf(u13152,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,uri_owl_FunctionalProperty),X0)
| icext(sK10(uri_rdfs_subClassOf,uri_owl_FunctionalProperty),X0) ) ).
cnf(u13155,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_owl_FunctionalProperty) ).
cnf(u13160,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_owl_FunctionalProperty))
| iext(uri_rdfs_subClassOf,X0,sK10(uri_rdfs_subClassOf,uri_owl_FunctionalProperty)) ) ).
cnf(u13164,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_owl_FunctionalProperty),X1,X0)
| icext(sK10(uri_rdfs_range,uri_owl_FunctionalProperty),X0) ) ).
cnf(u13172,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_owl_FunctionalProperty),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_owl_FunctionalProperty),X0) ) ).
cnf(u13181,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_someValuesFrom,uri_owl_FunctionalProperty)) ).
cnf(u13184,axiom,
~ iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_owl_FunctionalProperty) ).
cnf(u13189,axiom,
( icext(sK10(uri_owl_someValuesFrom,uri_owl_FunctionalProperty),sK17(X0,sK10(uri_owl_someValuesFrom,uri_owl_FunctionalProperty),X1))
| ~ icext(sK9(uri_owl_someValuesFrom,uri_owl_FunctionalProperty),X1)
| ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,uri_owl_FunctionalProperty),X0) ) ).
cnf(u13193,axiom,
( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,uri_owl_FunctionalProperty),X0)
| ~ icext(sK9(uri_owl_someValuesFrom,uri_owl_FunctionalProperty),X1)
| iext(X0,X1,sK17(X0,sK10(uri_owl_someValuesFrom,uri_owl_FunctionalProperty),X1)) ) ).
cnf(u13197,axiom,
( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,uri_owl_FunctionalProperty),X0)
| icext(sK9(uri_owl_someValuesFrom,uri_owl_FunctionalProperty),X2)
| ~ iext(X0,X2,X1)
| ~ icext(sK10(uri_owl_someValuesFrom,uri_owl_FunctionalProperty),X1) ) ).
cnf(u13202,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_onProperty,uri_owl_FunctionalProperty)) ).
cnf(u13205,axiom,
~ iext(uri_rdfs_domain,uri_owl_onProperty,uri_owl_FunctionalProperty) ).
cnf(u13211,axiom,
icext(sK10(uri_rdf_type,uri_owl_FunctionalProperty),sK9(uri_rdf_type,uri_owl_FunctionalProperty)) ).
cnf(u13214,axiom,
~ iext(uri_rdfs_domain,uri_rdf_type,uri_owl_FunctionalProperty) ).
cnf(u14118,axiom,
iext(uri_owl_unionOf,sK9(uri_rdfs_subClassOf,uri_owl_FunctionalProperty),uri_rdf_nil) ).
cnf(u14214,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_FunctionalProperty),uri_owl_FunctionalProperty) ).
cnf(u14227,axiom,
icext(sK10(uri_rdfs_range,uri_owl_FunctionalProperty),sK10(sK9(uri_rdfs_range,uri_owl_FunctionalProperty),uri_rdf_XMLLiteral)) ).
cnf(u14232,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_FunctionalProperty),uri_rdfs_Seq) ).
cnf(u14245,axiom,
icext(sK10(uri_rdfs_range,uri_owl_FunctionalProperty),sK10(sK9(uri_rdfs_range,uri_owl_FunctionalProperty),uri_rdf_Alt)) ).
cnf(u14254,axiom,
icext(sK10(uri_rdfs_range,uri_owl_FunctionalProperty),sK10(sK9(uri_rdfs_range,uri_owl_FunctionalProperty),uri_owl_Thing)) ).
cnf(u14263,axiom,
icext(sK10(uri_rdfs_range,uri_owl_FunctionalProperty),sK10(sK9(uri_rdfs_range,uri_owl_FunctionalProperty),uri_owl_Nothing)) ).
cnf(u14312,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_FunctionalProperty),uri_owl_FunctionalProperty) ).
cnf(u14325,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_FunctionalProperty),sK9(sK9(uri_rdfs_domain,uri_owl_FunctionalProperty),uri_rdf_XMLLiteral)) ).
cnf(u14330,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_FunctionalProperty),uri_rdfs_Seq) ).
cnf(u14343,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_FunctionalProperty),sK9(sK9(uri_rdfs_domain,uri_owl_FunctionalProperty),uri_rdf_Alt)) ).
cnf(u14352,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_FunctionalProperty),sK9(sK9(uri_rdfs_domain,uri_owl_FunctionalProperty),uri_owl_Thing)) ).
cnf(u14361,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_FunctionalProperty),sK9(sK9(uri_rdfs_domain,uri_owl_FunctionalProperty),uri_owl_Nothing)) ).
cnf(u14619,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_owl_Restriction) ).
cnf(u14631,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_owl_Restriction) ).
cnf(u14643,axiom,
iext(uri_rdfs_domain,uri_rdfs_range,uri_owl_Restriction) ).
cnf(u14647,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_owl_Restriction),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_owl_Restriction),X0) ) ).
cnf(u14660,axiom,
iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_owl_Restriction) ).
cnf(u14681,axiom,
iext(uri_rdfs_domain,uri_owl_onProperty,uri_owl_Restriction) ).
cnf(u14686,axiom,
icext(sK10(uri_rdf_type,uri_owl_Restriction),sK9(uri_rdf_type,uri_owl_Restriction)) ).
cnf(u14817,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Restriction),uri_owl_FunctionalProperty) ).
cnf(u14830,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Restriction),sK9(sK9(uri_rdfs_domain,uri_owl_Restriction),uri_rdf_XMLLiteral)) ).
cnf(u14835,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Restriction),uri_rdfs_Seq) ).
cnf(u14848,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Restriction),sK9(sK9(uri_rdfs_domain,uri_owl_Restriction),uri_rdf_Alt)) ).
cnf(u14857,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Restriction),sK9(sK9(uri_rdfs_domain,uri_owl_Restriction),uri_owl_Thing)) ).
cnf(u14866,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Restriction),sK9(sK9(uri_rdfs_domain,uri_owl_Restriction),uri_owl_Nothing)) ).
cnf(u15038,axiom,
( iext(sK10(uri_rdfs_subPropertyOf,sK18),X0,X1)
| ~ iext(sK9(uri_rdfs_subPropertyOf,sK18),X0,X1) ) ).
cnf(u15041,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,sK18) ).
cnf(u15046,axiom,
( ~ iext(uri_rdfs_subPropertyOf,sK10(uri_rdfs_subPropertyOf,sK18),X0)
| iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,sK18),X0) ) ).
cnf(u15050,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,sK18),X0)
| icext(sK10(uri_rdfs_subClassOf,sK18),X0) ) ).
cnf(u15053,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,sK18) ).
cnf(u15058,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,sK18))
| iext(uri_rdfs_subClassOf,X0,sK10(uri_rdfs_subClassOf,sK18)) ) ).
cnf(u15062,axiom,
( ~ iext(sK9(uri_rdfs_range,sK18),X1,X0)
| icext(sK10(uri_rdfs_range,sK18),X0) ) ).
cnf(u15065,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_range,sK18) ).
cnf(u15070,axiom,
( ~ iext(sK9(uri_rdfs_domain,sK18),X0,X1)
| icext(sK10(uri_rdfs_domain,sK18),X0) ) ).
cnf(u15078,axiom,
( icext(sK10(uri_owl_someValuesFrom,sK18),sK17(X0,sK10(uri_owl_someValuesFrom,sK18),X1))
| ~ icext(sK9(uri_owl_someValuesFrom,sK18),X1)
| ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,sK18),X0) ) ).
cnf(u15081,axiom,
~ iext(uri_rdfs_domain,uri_owl_someValuesFrom,sK18) ).
cnf(u15086,axiom,
( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,sK18),X0)
| ~ icext(sK9(uri_owl_someValuesFrom,sK18),X1)
| iext(X0,X1,sK17(X0,sK10(uri_owl_someValuesFrom,sK18),X1)) ) ).
cnf(u15090,axiom,
( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,sK18),X0)
| icext(sK9(uri_owl_someValuesFrom,sK18),X2)
| ~ iext(X0,X2,X1)
| ~ icext(sK10(uri_owl_someValuesFrom,sK18),X1) ) ).
cnf(u15095,axiom,
icext(sK10(uri_rdf_type,sK18),sK9(uri_rdf_type,sK18)) ).
cnf(u16093,axiom,
iext(uri_owl_unionOf,sK9(uri_rdfs_subClassOf,sK18),uri_rdf_nil) ).
cnf(u16147,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,sK18),sK18) ).
cnf(u16160,axiom,
icext(sK10(uri_rdfs_range,sK18),sK10(sK9(uri_rdfs_range,sK18),uri_owl_FunctionalProperty)) ).
cnf(u16165,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,sK18),uri_rdf_XMLLiteral) ).
cnf(u16178,axiom,
icext(sK10(uri_rdfs_range,sK18),sK10(sK9(uri_rdfs_range,sK18),uri_rdfs_Seq)) ).
cnf(u16187,axiom,
icext(sK10(uri_rdfs_range,sK18),sK10(sK9(uri_rdfs_range,sK18),uri_rdf_Alt)) ).
cnf(u16196,axiom,
icext(sK10(uri_rdfs_range,sK18),sK10(sK9(uri_rdfs_range,sK18),uri_owl_Thing)) ).
cnf(u16205,axiom,
icext(sK10(uri_rdfs_range,sK18),sK10(sK9(uri_rdfs_range,sK18),uri_owl_Nothing)) ).
cnf(u16256,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,sK18),sK18) ).
cnf(u16269,axiom,
icext(sK10(uri_rdfs_domain,sK18),sK9(sK9(uri_rdfs_domain,sK18),uri_owl_FunctionalProperty)) ).
cnf(u16274,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,sK18),uri_rdf_XMLLiteral) ).
cnf(u16287,axiom,
icext(sK10(uri_rdfs_domain,sK18),sK9(sK9(uri_rdfs_domain,sK18),uri_rdfs_Seq)) ).
cnf(u16296,axiom,
icext(sK10(uri_rdfs_domain,sK18),sK9(sK9(uri_rdfs_domain,sK18),uri_rdf_Alt)) ).
cnf(u16305,axiom,
icext(sK10(uri_rdfs_domain,sK18),sK9(sK9(uri_rdfs_domain,sK18),uri_owl_Thing)) ).
cnf(u16314,axiom,
icext(sK10(uri_rdfs_domain,sK18),sK9(sK9(uri_rdfs_domain,sK18),uri_owl_Nothing)) ).
cnf(u9668,axiom,
iext(uri_rdfs_member,sK4(uri_owl_Ontology),uri_owl_Ontology) ).
cnf(u3858,axiom,
( iext(X0,sK9(X0,uri_rdf_Alt),sK10(X0,uri_rdf_Alt))
| iext(uri_rdfs_domain,X0,uri_rdf_Alt) ) ).
cnf(u9566,axiom,
iext(uri_rdfs_member,uri_rdf_rest,X0) ).
cnf(u4321,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| ~ icext(X0,X1) ) ).
cnf(u12902,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Statement) ).
cnf(u14130,axiom,
iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,uri_owl_FunctionalProperty),X0) ).
cnf(u14796,axiom,
iext(uri_rdfs_member,X0,uri_owl_Restriction) ).
cnf(u9558,axiom,
iext(uri_rdfs_member,uri_owl_complementOf,X0) ).
cnf(u15033,axiom,
( icext(sK12(uri_rdfs_range,X0),sK10(sK11(uri_rdfs_range,X0),sK18))
| iext(uri_rdfs_domain,sK11(uri_rdfs_range,X0),sK18)
| iext(uri_rdfs_range,uri_rdfs_range,X0) ) ).
cnf(u14556,axiom,
( ~ iext(sK9(uri_rdfs_subPropertyOf,uri_owl_FunctionalProperty),sK14(X0,sK10(uri_rdfs_subPropertyOf,uri_owl_FunctionalProperty)),sK15(X0,sK10(uri_rdfs_subPropertyOf,uri_owl_FunctionalProperty)))
| iext(uri_rdfs_subPropertyOf,X0,sK10(uri_rdfs_subPropertyOf,uri_owl_FunctionalProperty)) ) ).
cnf(u13055,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdfs_Statement),X0,X1) ).
cnf(u387,axiom,
( iext(uri_rdf_type,X0,X1)
| ~ icext(X1,X0) ) ).
cnf(u9719,axiom,
( iext(uri_rdfs_member,sK9(X0,uri_owl_Thing),sK10(X0,uri_owl_Thing))
| iext(uri_rdfs_domain,X0,uri_owl_Thing) ) ).
cnf(u992,axiom,
( ~ icext(uri_owl_Ontology,X0)
| ix(X0) ) ).
cnf(u4979,axiom,
( icext(uri_owl_Ontology,sK13(uri_owl_Ontology,X0))
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ) ).
cnf(u5691,axiom,
iext(uri_rdfs_range,uri_owl_hasValue,X0) ).
cnf(u293,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_AnnotationProperty)
| ioap(X0) ) ).
cnf(u7366,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf__1,X0) ).
cnf(u16643,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(u4212,axiom,
iext(uri_rdfs_subClassOf,uri_owl_DatatypeProperty,X0) ).
cnf(u3382,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(u4200,axiom,
iext(uri_rdf_type,sK4(uri_owl_Ontology),uri_owl_Ontology) ).
cnf(u7365,axiom,
iext(uri_rdfs_range,uri_rdf__1,X0) ).
cnf(u8681,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdf_Alt),X0,X1) ).
cnf(u11114,axiom,
iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,uri_rdfs_Seq),X0) ).
cnf(u248,axiom,
( ~ iext(uri_owl_unionOf,X0,uri_rdf_nil)
| ~ icext(X0,X1) ) ).
cnf(u16636,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),X0) ).
cnf(u9681,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdf_Bag),X0) ).
cnf(u9540,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_Literal) ).
cnf(u14733,axiom,
icext(uri_owl_Restriction,X0) ).
cnf(u6966,axiom,
idc(X0) ).
cnf(u14793,axiom,
iext(uri_rdfs_subClassOf,X0,uri_owl_Restriction) ).
cnf(u2215,axiom,
( ~ icext(X1,sK12(X0,X1))
| iext(uri_rdfs_range,X0,X1) ) ).
cnf(u5771,axiom,
iext(uri_rdfs_range,uri_rdf_rest,X0) ).
cnf(u16632,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u7061,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(u8685,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdf_Alt),X0) ).
cnf(u16522,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subPropertyOf,sK18),sK10(uri_rdfs_subPropertyOf,sK18)) ).
cnf(u12483,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdf_XMLLiteral),X0,X1) ).
cnf(u2211,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdf_Property) ).
cnf(u16235,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,sK18),X0) ).
cnf(u1279,axiom,
~ icext(uri_rdfs_Seq,X0) ).
cnf(u16629,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_Alt),X0) ).
cnf(u6480,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_owl_Nothing))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u12495,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdf_XMLLiteral),X0) ).
cnf(u406,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty) ).
cnf(u5311,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,X0) ).
cnf(u365,axiom,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property) ).
cnf(u4054,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Class) ).
cnf(u6912,axiom,
~ iext(uri_rdfs_label,X0,X1) ).
cnf(u3384,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(u7397,axiom,
iext(uri_rdfs_domain,X0,uri_rdf_List) ).
cnf(u11138,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subClassOf,uri_rdfs_Seq),X0) ).
cnf(u286,axiom,
( iext(uri_rdf_type,X0,uri_rdfs_Class)
| ~ ic(X0) ) ).
cnf(u16614,axiom,
iext(uri_rdfs_domain,uri_rdf__3,X0) ).
cnf(u16624,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Datatype),X0) ).
cnf(u3108,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| iext(uri_rdfs_subClassOf,X0,sK18) ) ).
cnf(u8557,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_rdf_Alt))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u3377,axiom,
( ~ iext(uri_owl_onProperty,sK14(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0)
| iext(X1,X2,sK17(X1,sK15(uri_owl_someValuesFrom,X0),X2))
| ~ icext(sK14(uri_owl_someValuesFrom,X0),X2) ) ).
cnf(u16637,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Statement),X0) ).
cnf(u4063,axiom,
iext(uri_rdfs_subClassOf,X0,uri_owl_Thing) ).
cnf(u3002,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(u13082,axiom,
( iext(uri_rdfs_member,sK9(X0,uri_owl_FunctionalProperty),sK10(X0,uri_owl_FunctionalProperty))
| iext(uri_rdfs_domain,X0,uri_owl_FunctionalProperty) ) ).
cnf(u16320,axiom,
~ iext(sK9(uri_rdfs_domain,sK18),X0,X1) ).
cnf(u373,axiom,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property) ).
cnf(u7060,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(u13127,axiom,
( icext(sK15(uri_rdfs_domain,X0),sK9(sK14(uri_rdfs_domain,X0),uri_owl_FunctionalProperty))
| iext(uri_rdfs_domain,sK14(uri_rdfs_domain,X0),uri_owl_FunctionalProperty)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0) ) ).
cnf(u9677,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subClassOf,uri_rdf_Alt),X0) ).
cnf(u16621,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Nothing),X0) ).
cnf(u5288,axiom,
~ iext(uri_rdfs_isDefinedBy,X0,X1) ).
cnf(u14522,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(u6974,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype) ).
cnf(u16622,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_Nothing),X0) ).
cnf(u278,axiom,
~ icext(uri_owl_Nothing,X0) ).
cnf(u9594,axiom,
iext(uri_rdfs_member,uri_owl_hasValue,X0) ).
cnf(u5886,axiom,
iext(uri_rdfs_range,sK4(uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u1318,axiom,
~ icext(uri_rdf_Alt,X0) ).
cnf(u7403,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(u456,axiom,
iext(uri_owl_onProperty,sK18,uri_owl_inverseOf) ).
cnf(u11194,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdfs_Seq),X0) ).
cnf(u9620,axiom,
iext(uri_rdfs_member,uri_rdf__3,X0) ).
cnf(u16617,axiom,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,X0) ).
cnf(u6883,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(u14542,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_rdfs_Seq),sK10(uri_rdfs_subPropertyOf,uri_rdfs_Seq)) ).
cnf(u7464,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(u9571,axiom,
iext(uri_rdfs_member,uri_owl_Thing,uri_rdf_nil) ).
cnf(u7402,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(u3392,axiom,
( ~ iext(uri_rdfs_subPropertyOf,sK15(uri_rdfs_subPropertyOf,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0)
| iext(uri_rdfs_subPropertyOf,sK14(uri_rdfs_subPropertyOf,X0),X1) ) ).
cnf(u16603,axiom,
( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0)
| ~ icext(sK10(uri_owl_someValuesFrom,X0),X2)
| ~ iext(X1,X3,X2)
| icext(sK9(uri_owl_someValuesFrom,X0),X3) ) ).
cnf(u3010,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(u12912,axiom,
iext(uri_rdfs_member,uri_rdfs_Statement,uri_rdf_nil) ).
cnf(u368,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property) ).
cnf(u388,axiom,
( ~ iext(uri_rdf_type,X0,X1)
| icext(X1,X0) ) ).
cnf(u13125,axiom,
( icext(sK12(uri_rdfs_domain,X0),sK9(sK11(uri_rdfs_domain,X0),uri_owl_FunctionalProperty))
| iext(uri_rdfs_domain,sK11(uri_rdfs_domain,X0),uri_owl_FunctionalProperty)
| iext(uri_rdfs_range,uri_rdfs_domain,X0) ) ).
cnf(u339,axiom,
( ~ iext(uri_rdfs_domain,X0,X1)
| icext(X1,X2)
| ~ iext(X0,X2,X3) ) ).
cnf(u16602,axiom,
iext(uri_rdfs_domain,uri_owl_hasValue,X0) ).
cnf(u9718,axiom,
( iext(uri_rdfs_member,sK9(X0,uri_owl_Nothing),sK10(X0,uri_owl_Nothing))
| iext(uri_rdfs_domain,X0,uri_owl_Nothing) ) ).
cnf(u16615,axiom,
iext(uri_rdfs_domain,uri_rdf_object,X0) ).
cnf(u9524,axiom,
iext(uri_rdfs_member,X0,uri_owl_Thing) ).
cnf(u8641,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdf_Alt),X0) ).
cnf(u9549,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(u4062,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource) ).
cnf(u10152,axiom,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
| iext(uri_rdfs_subPropertyOf,X1,X0) ) ).
cnf(u4933,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,uri_owl_FunctionalProperty)
| iext(uri_rdfs_subClassOf,X1,X0) ) ).
cnf(u12984,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdfs_Statement),X0) ).
cnf(u16640,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_FunctionalProperty),X0) ).
cnf(u16599,axiom,
iext(uri_rdfs_domain,uri_rdf_rest,X0) ).
cnf(u2589,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Resource) ).
cnf(u12992,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdfs_Statement),X0) ).
cnf(u14798,axiom,
iext(uri_rdfs_member,uri_owl_Restriction,uri_rdf_nil) ).
cnf(u7073,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(u376,axiom,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property) ).
cnf(u16742,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(u9546,axiom,
( iext(uri_rdfs_member,X0,uri_rdfs_Seq)
| ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral) ) ).
cnf(u3863,axiom,
( iext(X0,sK9(X0,uri_rdf_XMLLiteral),sK10(X0,uri_rdf_XMLLiteral))
| iext(uri_rdfs_domain,X0,uri_rdf_XMLLiteral) ) ).
cnf(u1259,axiom,
iext(uri_owl_unionOf,uri_owl_Nothing,uri_rdf_nil) ).
cnf(u16752,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(u4687,axiom,
iext(uri_rdfs_subClassOf,sK4(uri_rdfs_Class),X0) ).
cnf(u8131,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_owl_Thing),X0) ).
cnf(u7467,axiom,
( icext(sK15(uri_rdfs_range,X0),sK10(sK14(uri_rdfs_range,X0),uri_rdf_Alt))
| iext(uri_rdfs_domain,sK14(uri_rdfs_range,X0),uri_rdf_Alt)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0) ) ).
cnf(u8637,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdf_Alt),X0,X1) ).
cnf(u1123,axiom,
( ~ iext(uri_owl_intersectionOf,X0,uri_rdf_nil)
| icext(X0,X1) ) ).
cnf(u2393,axiom,
( ~ ic(X1)
| iext(X0,sK9(X0,X1),sK10(X0,X1))
| iext(uri_rdfs_domain,X0,X1) ) ).
cnf(u3059,axiom,
iext(uri_owl_unionOf,sK18,uri_rdf_nil) ).
cnf(u11255,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdfs_Seq),X0,X1) ).
cnf(u9682,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdfs_Datatype),X0) ).
cnf(u9293,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdf_Bag),X0) ).
cnf(u12910,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_Statement) ).
cnf(u5695,axiom,
iext(uri_rdfs_range,uri_owl_allValuesFrom,X0) ).
cnf(u2205,axiom,
ip(X0) ).
cnf(u14538,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subPropertyOf,uri_rdf_Alt),sK10(uri_rdfs_subPropertyOf,uri_rdf_Alt)) ).
cnf(u411,axiom,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype) ).
cnf(u5619,axiom,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,X0) ).
cnf(u5692,axiom,
iext(uri_rdfs_subPropertyOf,uri_owl_hasValue,X0) ).
cnf(u8686,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdf_Alt),X0) ).
cnf(u4127,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u10691,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_owl_Nothing),X0) ).
cnf(u9684,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdfs_Container),X0) ).
cnf(u9651,axiom,
iext(uri_rdfs_member,uri_rdfs_ContainerMembershipProperty,uri_rdf_nil) ).
cnf(u423,axiom,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class) ).
cnf(u354,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,X1)
| iext(X1,X2,X3)
| ~ iext(X0,X2,X3) ) ).
cnf(u5624,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf_subject,X0) ).
cnf(u7620,axiom,
~ iext(uri_rdf__3,X0,X1) ).
cnf(u16730,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(u3849,axiom,
( iext(X0,sK9(X0,uri_owl_Nothing),sK10(X0,uri_owl_Nothing))
| iext(uri_rdfs_domain,X0,uri_owl_Nothing) ) ).
cnf(u11195,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdfs_Seq),X0) ).
cnf(u2258,axiom,
( iext(X0,sK11(X0,X1),sK12(X0,X1))
| iext(uri_rdfs_range,X0,X1) ) ).
cnf(u366,axiom,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List) ).
cnf(u14376,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_owl_FunctionalProperty),X0) ).
cnf(u14550,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral),sK10(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral)) ).
cnf(u9656,axiom,
iext(uri_rdfs_member,uri_rdf_XMLLiteral,X0) ).
cnf(u11352,axiom,
( iext(uri_rdfs_member,sK9(X0,uri_rdf_XMLLiteral),sK10(X0,uri_rdf_XMLLiteral))
| iext(uri_rdfs_domain,X0,uri_rdf_XMLLiteral) ) ).
cnf(u7398,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(u9043,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdfs_Container),X0) ).
cnf(u810,axiom,
iext(uri_rdf_type,X0,uri_rdfs_Resource) ).
cnf(u9648,axiom,
iext(uri_rdfs_member,uri_rdf_Alt,X0) ).
cnf(u14794,axiom,
iext(uri_rdfs_domain,X0,uri_owl_Restriction) ).
cnf(u8964,axiom,
icext(uri_rdfs_Container,X0) ).
cnf(u5680,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,uri_owl_Nothing)
| iext(uri_rdfs_subClassOf,X1,X0) ) ).
cnf(u3003,axiom,
( ~ icext(sK11(uri_rdfs_subClassOf,X0),X1)
| icext(sK12(uri_rdfs_subClassOf,X0),X1)
| iext(uri_rdfs_range,uri_rdfs_subClassOf,X0) ) ).
cnf(u2198,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,X0) ).
cnf(u9249,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag) ).
cnf(u4932,axiom,
( iext(uri_rdf_type,sK13(uri_owl_Ontology,X0),uri_owl_Ontology)
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ) ).
cnf(u8958,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf_object,X0) ).
cnf(u3134,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,sK18) ) ).
cnf(u4206,axiom,
iext(uri_rdfs_subClassOf,uri_owl_OntologyProperty,X0) ).
cnf(u9585,axiom,
iext(uri_rdfs_member,uri_rdfs_Literal,uri_rdf_nil) ).
cnf(u9533,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_ContainerMembershipProperty) ).
cnf(u3365,axiom,
( icext(sK15(uri_rdf_type,X0),sK14(uri_rdf_type,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0) ) ).
cnf(u9678,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_owl_Thing),X0) ).
cnf(u9515,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_Class) ).
cnf(u14881,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_owl_Restriction),X0) ).
cnf(u9294,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdf_Bag),X0) ).
cnf(u10939,axiom,
iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member) ).
cnf(u14870,axiom,
~ iext(sK9(uri_rdfs_domain,uri_owl_Restriction),X0,X1) ).
cnf(u5788,axiom,
iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0) ).
cnf(u12398,axiom,
iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,uri_rdf_XMLLiteral),X0) ).
cnf(u16627,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_List),X0) ).
cnf(u2058,axiom,
( iext(uri_rdfs_subClassOf,X0,uri_owl_FunctionalProperty)
| ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral) ) ).
cnf(u2191,axiom,
ic(X0) ).
cnf(u3388,axiom,
( iext(uri_rdfs_subClassOf,X1,sK15(uri_rdfs_subClassOf,X0))
| ~ iext(uri_rdfs_subClassOf,X1,sK14(uri_rdfs_subClassOf,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0) ) ).
cnf(u12907,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement) ).
cnf(u9501,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_nil) ).
cnf(u2285,axiom,
iext(uri_rdfs_subClassOf,sK18,X0) ).
cnf(u9214,axiom,
icext(uri_rdf_Bag,X0) ).
cnf(u16634,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Seq),X0) ).
cnf(u438,axiom,
( iext(uri_rdfs_subClassOf,X0,X0)
| ~ ic(X0) ) ).
cnf(u13065,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdfs_Statement),X0) ).
cnf(u7066,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(u12399,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_rdf_XMLLiteral))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u14893,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_owl_Restriction),X0) ).
cnf(u11391,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(u6474,axiom,
~ icext(sK9(uri_rdfs_subClassOf,uri_owl_Nothing),X0) ).
cnf(u16645,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(u10692,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_owl_Nothing),X0) ).
cnf(u9550,axiom,
( iext(uri_rdfs_member,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(u8913,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(u9950,axiom,
( icext(sK12(uri_rdfs_domain,X0),sK9(sK11(uri_rdfs_domain,X0),uri_rdfs_Seq))
| iext(uri_rdfs_domain,sK11(uri_rdfs_domain,X0),uri_rdfs_Seq)
| iext(uri_rdfs_range,uri_rdfs_domain,X0) ) ).
cnf(u2983,axiom,
( icext(sK12(uri_rdf_type,X0),sK11(uri_rdf_type,X0))
| iext(uri_rdfs_range,uri_rdf_type,X0) ) ).
cnf(u16759,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(u6965,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal) ).
cnf(u9542,axiom,
( iext(uri_rdfs_member,X0,uri_rdf_Alt)
| ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral) ) ).
cnf(u4568,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK4(uri_rdfs_Datatype))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u4207,axiom,
~ icext(uri_owl_DatatypeProperty,X0) ).
cnf(u9913,axiom,
( iext(uri_rdfs_member,sK9(X0,uri_rdfs_Seq),sK10(X0,uri_rdfs_Seq))
| iext(uri_rdfs_domain,X0,uri_rdfs_Seq) ) ).
cnf(u367,axiom,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property) ).
cnf(u298,axiom,
( ~ ioxp(X0)
| ~ iext(X0,X1,X2)
| ix(X2) ) ).
cnf(u2266,axiom,
( iext(uri_rdfs_subClassOf,X0,uri_owl_FunctionalProperty)
| ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq) ) ).
cnf(u446,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,X1)
| ~ iext(uri_rdfs_subPropertyOf,X1,X2)
| iext(uri_rdfs_subPropertyOf,X0,X2) ) ).
cnf(u9465,axiom,
icext(uri_rdfs_ContainerMembershipProperty,X0) ).
cnf(u9004,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(u3886,axiom,
( iext(X0,sK9(X0,sK18),sK10(X0,sK18))
| iext(uri_rdfs_domain,X0,sK18) ) ).
cnf(u16755,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(u250,axiom,
( ~ ic(X0)
| icext(X0,sK4(X0))
| iext(uri_owl_unionOf,X0,uri_rdf_nil) ) ).
cnf(u9575,axiom,
iext(uri_rdfs_member,uri_rdfs_Datatype,uri_rdf_nil) ).
cnf(u2326,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0) ).
cnf(u9906,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u5620,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,X0) ).
cnf(u9044,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdfs_Container),X0) ).
cnf(u363,axiom,
( ~ iext(uri_owl_someValuesFrom,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| iext(X1,X3,sK17(X1,X2,X3))
| ~ icext(X0,X3) ) ).
cnf(u5860,axiom,
~ iext(sK4(uri_rdfs_ContainerMembershipProperty),X0,X1) ).
cnf(u13073,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdfs_Statement),X0) ).
cnf(u12494,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdf_XMLLiteral),X0) ).
cnf(u16620,axiom,
iext(uri_rdfs_domain,sK4(uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u408,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty) ).
cnf(u16638,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Statement),X0) ).
cnf(u11261,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdfs_Seq),X0) ).
cnf(u306,axiom,
( iext(uri_rdf_type,X0,uri_rdf_Property)
| ~ ip(X0) ) ).
cnf(u14562,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subPropertyOf,uri_owl_FunctionalProperty),sK10(uri_rdfs_subPropertyOf,uri_owl_FunctionalProperty)) ).
cnf(u16635,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_XMLLiteral),X0) ).
cnf(u5290,axiom,
~ iext(uri_rdf_subject,X0,X1) ).
cnf(u9583,axiom,
iext(uri_rdfs_member,uri_rdf_Property,uri_rdf_nil) ).
cnf(u11830,axiom,
~ iext(sK9(uri_rdfs_range,uri_owl_Nothing),X0,X1) ).
cnf(u1460,axiom,
~ icext(sK4(uri_rdfs_Datatype),X0) ).
cnf(u16601,axiom,
iext(uri_rdfs_domain,uri_owl_allValuesFrom,X0) ).
cnf(u371,axiom,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property) ).
cnf(u14548,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(u16619,axiom,
iext(uri_rdfs_domain,uri_rdf_predicate,X0) ).
cnf(u4550,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| ~ iext(uri_rdfs_subClassOf,X1,X0)
| iext(uri_rdfs_subClassOf,X1,uri_owl_FunctionalProperty) ) ).
cnf(u16628,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_Alt),X0) ).
cnf(u9673,axiom,
iext(uri_rdfs_member,sK4(uri_rdfs_Datatype),X0) ).
cnf(u2252,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral) ) ).
cnf(u9895,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X0,X1) ).
cnf(u16606,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(u16518,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,sK18),sK10(uri_rdfs_subPropertyOf,sK18)) ).
cnf(u5298,axiom,
~ iext(uri_owl_hasValue,X0,X1) ).
cnf(u13064,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdfs_Statement),X0) ).
cnf(u6917,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_label,X0) ).
cnf(u349,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,X1)
| icext(X1,X2)
| ~ icext(X0,X2) ) ).
cnf(u16612,axiom,
iext(uri_rdfs_domain,uri_rdf__1,X0) ).
cnf(u16609,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,X0),X1)
| icext(sK10(uri_rdfs_subClassOf,X0),X1)
| iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0) ) ).
cnf(u455,axiom,
iext(uri_owl_someValuesFrom,sK18,uri_owl_FunctionalProperty) ).
cnf(u9589,axiom,
iext(uri_rdfs_member,uri_owl_allValuesFrom,X0) ).
cnf(u2112,axiom,
( ~ icext(X0,sK0(X0))
| ~ ic(X0)
| iext(uri_owl_intersectionOf,X0,uri_rdf_nil) ) ).
cnf(u14288,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_owl_FunctionalProperty),X0) ).
cnf(u7396,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdf_List) ).
cnf(u9581,axiom,
iext(uri_rdfs_member,uri_owl_OntologyProperty,X0) ).
cnf(u9547,axiom,
( iext(uri_rdfs_member,X0,uri_owl_FunctionalProperty)
| ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq) ) ).
cnf(u14277,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_owl_FunctionalProperty),X0) ).
cnf(u5308,axiom,
~ iext(uri_owl_complementOf,X0,X1) ).
cnf(u8911,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(u1438,axiom,
~ icext(sK4(uri_rdfs_Class),X0) ).
cnf(u7465,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(u16221,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,sK18),X0) ).
cnf(u16605,axiom,
( icext(sK10(uri_owl_someValuesFrom,X0),sK17(X1,sK10(uri_owl_someValuesFrom,X0),X2))
| ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0)
| ~ icext(sK9(uri_owl_someValuesFrom,X0),X2) ) ).
cnf(u7071,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(u16733,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(u12908,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Statement) ).
cnf(u5623,axiom,
iext(uri_rdfs_range,uri_rdf_subject,X0) ).
cnf(u8997,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Container,uri_rdf_nil) ).
cnf(u16616,axiom,
iext(uri_rdfs_domain,uri_rdf_subject,X0) ).
cnf(u9683,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdf_Alt),X0) ).
cnf(u1260,axiom,
~ icext(uri_owl_FunctionalProperty,X0) ).
cnf(u9502,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty) ).
cnf(u7059,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(u8993,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Container) ).
cnf(u4113,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u8556,axiom,
iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,uri_rdf_Alt),X0) ).
cnf(u14792,axiom,
iext(uri_owl_intersectionOf,uri_owl_Restriction,uri_rdf_nil) ).
cnf(u9663,axiom,
iext(uri_rdfs_member,uri_ex_InversesOfFunctionalProperties,sK18) ).
cnf(u16613,axiom,
iext(uri_rdfs_domain,uri_rdf__2,X0) ).
cnf(u7067,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(u16756,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(u13610,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdfs_Datatype),X0) ).
cnf(u9289,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdf_Bag),X0,X1) ).
cnf(u458,axiom,
iext(uri_owl_equivalentClass,uri_ex_InversesOfFunctionalProperties,sK18) ).
cnf(u8552,axiom,
~ icext(sK9(uri_rdfs_subClassOf,uri_rdf_Alt),X0) ).
cnf(u6985,axiom,
lv(X0) ).
cnf(u7642,axiom,
iext(uri_rdfs_range,uri_rdf__3,X0) ).
cnf(u16646,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(u364,axiom,
( ~ iext(uri_owl_someValuesFrom,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ icext(X2,X4)
| ~ iext(X1,X3,X4)
| icext(X0,X3) ) ).
cnf(u6943,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf__2,X0) ).
cnf(u5286,axiom,
~ iext(uri_rdf_predicate,X0,X1) ).
cnf(u315,axiom,
( iext(uri_rdf_type,X0,uri_rdfs_Literal)
| ~ lv(X0) ) ).
cnf(u16598,axiom,
iext(uri_rdfs_domain,uri_owl_complementOf,X0) ).
cnf(u7391,axiom,
iext(uri_rdfs_range,X0,uri_rdf_List) ).
cnf(u6412,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(u11392,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(u12983,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdfs_Statement),X0) ).
cnf(u16642,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,sK18),X0) ).
cnf(u7360,axiom,
~ iext(uri_rdf__1,X0,X1) ).
cnf(u6916,axiom,
iext(uri_rdfs_range,uri_rdfs_label,X0) ).
cnf(u16220,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,sK18),X0) ).
cnf(u7404,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(u14375,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_owl_FunctionalProperty),X0) ).
cnf(u9494,axiom,
( ~ iext(X0,X1,X2)
| iext(uri_rdfs_member,X1,X2) ) ).
cnf(u3376,axiom,
( ~ iext(uri_owl_onProperty,sK14(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0)
| ~ icext(sK15(uri_owl_someValuesFrom,X0),X2)
| ~ iext(X1,X3,X2)
| icext(sK14(uri_owl_someValuesFrom,X0),X3) ) ).
cnf(u9596,axiom,
iext(uri_rdfs_member,uri_rdf_List,uri_rdf_nil) ).
cnf(u14988,axiom,
( iext(uri_rdfs_member,sK9(X0,sK18),sK10(X0,sK18))
| iext(uri_rdfs_domain,X0,sK18) ) ).
cnf(u7072,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(u2994,axiom,
( ~ iext(uri_owl_onProperty,sK11(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_range,uri_owl_someValuesFrom,X0)
| ~ icext(sK12(uri_owl_someValuesFrom,X0),X2)
| ~ iext(X1,X3,X2)
| icext(sK11(uri_owl_someValuesFrom,X0),X3) ) ).
cnf(u12584,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),X0) ).
cnf(u9738,axiom,
iext(uri_rdfs_member,sK18,X0) ).
cnf(u7069,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(u372,axiom,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property) ).
cnf(u15034,axiom,
( icext(sK15(uri_rdfs_domain,X0),sK9(sK14(uri_rdfs_domain,X0),sK18))
| iext(uri_rdfs_domain,sK14(uri_rdfs_domain,X0),sK18)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0) ) ).
cnf(u9674,axiom,
iext(uri_rdfs_member,sK4(uri_rdfs_Class),X0) ).
cnf(u7057,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Literal) ).
cnf(u9527,axiom,
iext(uri_rdfs_member,X0,uri_rdf_Property) ).
cnf(u12576,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),X0) ).
cnf(u9661,axiom,
iext(uri_rdfs_member,uri_rdf_predicate,X0) ).
cnf(u2324,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Class) ).
cnf(u9739,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_member) ).
cnf(u8056,axiom,
~ iext(sK9(uri_rdfs_range,uri_owl_Thing),X0,X1) ).
cnf(u2197,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,X0) ).
cnf(u9574,axiom,
iext(uri_rdfs_member,uri_rdfs_Class,uri_rdf_nil) ).
cnf(u3006,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(u16100,axiom,
~ icext(sK9(uri_rdfs_subClassOf,sK18),X0) ).
cnf(u9731,axiom,
( iext(uri_rdfs_member,sK11(X0,X1),sK12(X0,X1))
| iext(uri_rdfs_range,X0,X1) ) ).
cnf(u14386,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_owl_FunctionalProperty),X0) ).
cnf(u16734,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(u6409,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(u9497,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_ContainerMembershipProperty) ).
cnf(u16744,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(u11203,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdfs_Seq),X0) ).
cnf(u9732,axiom,
( iext(uri_rdfs_member,sK13(uri_owl_Ontology,X0),uri_owl_Ontology)
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ) ).
cnf(u9952,axiom,
( icext(sK15(uri_rdfs_domain,X0),sK9(sK14(uri_rdfs_domain,X0),uri_rdfs_Seq))
| iext(uri_rdfs_domain,sK14(uri_rdfs_domain,X0),uri_rdfs_Seq)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0) ) ).
cnf(u301,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_OntologyProperty)
| ioxp(X0) ) ).
cnf(u2011,axiom,
( iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral) ) ).
cnf(u4099,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u9733,axiom,
( iext(uri_rdfs_member,sK14(X0,X1),sK15(X0,X1))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u12393,axiom,
~ icext(sK9(uri_rdfs_subClassOf,uri_rdf_XMLLiteral),X0) ).
cnf(u12859,axiom,
icext(uri_rdfs_Statement,X0) ).
cnf(u9953,axiom,
( icext(sK15(uri_rdfs_range,X0),sK10(sK14(uri_rdfs_range,X0),uri_rdfs_Seq))
| iext(uri_rdfs_domain,sK14(uri_rdfs_range,X0),uri_rdfs_Seq)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0) ) ).
cnf(u16351,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,sK18),X0) ).
cnf(u9635,axiom,
iext(uri_rdfs_member,uri_rdf_subject,X0) ).
cnf(u407,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty) ).
cnf(u338,axiom,
( ~ icext(X1,sK9(X0,X1))
| ~ ic(X1)
| ~ ip(X0)
| iext(uri_rdfs_domain,X0,X1) ) ).
cnf(u9676,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subClassOf,uri_owl_Nothing),X0) ).
cnf(u11393,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(u297,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_DatatypeProperty)
| iodp(X0) ) ).
cnf(u9627,axiom,
iext(uri_rdfs_member,uri_rdf_object,X0) ).
cnf(u3385,axiom,
( ~ icext(sK14(uri_rdfs_subClassOf,X0),X1)
| icext(sK15(uri_rdfs_subClassOf,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0) ) ).
cnf(u12503,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdf_XMLLiteral),X0) ).
cnf(u452,axiom,
ir(X0) ).
cnf(u16106,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,sK18))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u7399,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(u4220,axiom,
icext(uri_owl_Ontology,sK4(uri_owl_Ontology)) ).
cnf(u4201,axiom,
~ icext(uri_owl_OntologyProperty,X0) ).
cnf(u8957,axiom,
iext(uri_rdfs_range,uri_rdf_object,X0) ).
cnf(u2095,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing) ) ).
cnf(u12566,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),X0,X1) ).
cnf(u2148,axiom,
iext(uri_owl_intersectionOf,uri_owl_Thing,uri_rdf_nil) ).
cnf(u8998,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container) ).
cnf(u7056,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Literal,uri_rdf_nil) ).
cnf(u9613,axiom,
iext(uri_rdfs_member,uri_rdf__2,X0) ).
cnf(u5887,axiom,
iext(uri_rdfs_subPropertyOf,sK4(uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u9248,axiom,
iext(uri_owl_intersectionOf,uri_rdf_Bag,uri_rdf_nil) ).
cnf(u9530,axiom,
iext(uri_rdfs_member,X0,uri_rdf_List) ).
cnf(u10724,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_owl_Nothing),X0) ).
cnf(u14534,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_rdf_Alt),sK10(uri_rdfs_subPropertyOf,uri_rdf_Alt)) ).
cnf(u9039,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdfs_Container),X0,X1) ).
cnf(u9548,axiom,
( iext(uri_rdfs_member,X0,uri_owl_FunctionalProperty)
| ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral) ) ).
cnf(u8136,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdf_List),X0) ).
cnf(u4213,axiom,
~ icext(uri_owl_AnnotationProperty,X0) ).
cnf(u7371,axiom,
icext(uri_rdf_List,X0) ).
cnf(u16626,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Restriction),X0) ).
cnf(u7068,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(u3393,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(u5772,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0) ).
cnf(u9512,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_Resource) ).
cnf(u12974,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdfs_Statement),X0,X1) ).
cnf(u5787,axiom,
iext(uri_rdfs_range,uri_owl_complementOf,X0) ).
cnf(u369,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property) ).
cnf(u16597,axiom,
( iext(uri_rdfs_member,sK9(X0,X1),sK10(X0,X1))
| iext(uri_rdfs_domain,X0,X1) ) ).
cnf(u16623,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_Thing),X0) ).
cnf(u1969,axiom,
( iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt)
| ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral) ) ).
cnf(u8130,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_owl_Thing),X0) ).
cnf(u9577,axiom,
iext(uri_rdfs_member,uri_owl_AnnotationProperty,X0) ).
cnf(u9679,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdf_List),X0) ).
cnf(u16516,axiom,
( ~ iext(sK9(uri_rdfs_subPropertyOf,sK18),sK14(X0,sK10(uri_rdfs_subPropertyOf,sK18)),sK15(X0,sK10(uri_rdfs_subPropertyOf,sK18)))
| iext(uri_rdfs_subPropertyOf,X0,sK10(uri_rdfs_subPropertyOf,sK18)) ) ).
cnf(u16331,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,sK18),X0) ).
cnf(u312,axiom,
( ~ ix(X0)
| iext(uri_rdf_type,X0,uri_owl_Ontology) ) ).
cnf(u6937,axiom,
~ iext(uri_rdf__2,X0,X1) ).
cnf(u3862,axiom,
( iext(X0,sK9(X0,uri_rdfs_Seq),sK10(X0,uri_rdfs_Seq))
| iext(uri_rdfs_domain,X0,uri_rdfs_Seq) ) ).
cnf(u4356,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| ~ iext(uri_rdfs_subClassOf,X1,X0)
| iext(uri_rdfs_subClassOf,X1,uri_rdfs_Seq) ) ).
cnf(u11109,axiom,
~ icext(sK9(uri_rdfs_subClassOf,uri_rdfs_Seq),X0) ).
cnf(u1272,axiom,
~ icext(uri_rdf_XMLLiteral,X0) ).
cnf(u16641,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,sK18),X0) ).
cnf(u16607,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(u6880,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(u4931,axiom,
( ix(sK13(uri_owl_Ontology,X0))
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ) ).
cnf(u7062,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(u14278,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_owl_FunctionalProperty),X0) ).
cnf(u16600,axiom,
( icext(sK10(uri_rdf_type,X0),sK9(uri_rdf_type,X0))
| iext(uri_rdfs_domain,uri_rdf_type,X0) ) ).
cnf(u7050,axiom,
icext(uri_rdfs_Literal,X0) ).
cnf(u16743,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(u5304,axiom,
~ iext(uri_rdf_rest,X0,X1) ).
cnf(u16631,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_Bag),X0) ).
cnf(u16625,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Datatype),X0) ).
cnf(u2588,axiom,
iext(uri_rdfs_range,X0,uri_rdf_Property) ).
cnf(u2995,axiom,
( ~ iext(uri_owl_onProperty,sK11(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_range,uri_owl_someValuesFrom,X0)
| iext(X1,X2,sK17(X1,sK12(uri_owl_someValuesFrom,X0),X2))
| ~ icext(sK11(uri_owl_someValuesFrom,X0),X2) ) ).
cnf(u9244,axiom,
iext(uri_rdfs_range,X0,uri_rdf_Bag) ).
cnf(u16753,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(u9526,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_Datatype) ).
cnf(u9720,axiom,
( iext(uri_rdfs_member,sK9(X0,uri_rdf_Alt),sK10(X0,uri_rdf_Alt))
| iext(uri_rdfs_domain,X0,uri_rdf_Alt) ) ).
cnf(u16644,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(u14151,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subClassOf,uri_owl_FunctionalProperty),X0) ).
cnf(u14365,axiom,
~ iext(sK9(uri_rdfs_domain,uri_owl_FunctionalProperty),X0,X1) ).
cnf(u14901,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,sK4(uri_rdfs_Class))
| iext(uri_rdfs_subClassOf,X1,X0) ) ).
cnf(u5310,axiom,
iext(uri_rdfs_range,uri_rdf_predicate,X0) ).
cnf(u14558,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_owl_FunctionalProperty),sK10(uri_rdfs_subPropertyOf,uri_owl_FunctionalProperty)) ).
cnf(u16209,axiom,
~ iext(sK9(uri_rdfs_range,sK18),X0,X1) ).
cnf(u16125,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subClassOf,sK18),X0) ).
cnf(u2273,axiom,
( ~ iext(X1,sK14(X0,X1),sK15(X0,X1))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u4037,axiom,
( icext(X0,sK4(X0))
| iext(uri_owl_unionOf,X0,uri_rdf_nil) ) ).
cnf(u347,axiom,
( icext(X0,sK13(X0,X1))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u16610,axiom,
( ~ iext(uri_rdfs_subPropertyOf,sK10(uri_rdfs_subPropertyOf,X0),X1)
| iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0)
| iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,X0),X1) ) ).
cnf(u11115,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_rdfs_Seq))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u9532,axiom,
iext(uri_rdfs_member,X0,uri_rdf_Bag) ).
cnf(u11394,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(u16633,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Seq),X0) ).
cnf(u12575,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),X0) ).
cnf(u9649,axiom,
iext(uri_rdfs_member,uri_rdfs_Container,uri_rdf_nil) ).
cnf(u4034,axiom,
( iext(X0,sK9(X0,X1),sK10(X0,X1))
| iext(uri_rdfs_domain,X0,X1) ) ).
cnf(u3378,axiom,
( icext(sK15(uri_owl_someValuesFrom,X0),sK17(X1,sK15(uri_owl_someValuesFrom,X0),X2))
| ~ iext(uri_owl_onProperty,sK14(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0)
| ~ icext(sK14(uri_owl_someValuesFrom,X0),X2) ) ).
cnf(u1876,axiom,
( ~ icext(uri_rdfs_ContainerMembershipProperty,X2)
| ~ iext(X2,X0,X1)
| iext(uri_rdfs_member,X0,X1) ) ).
cnf(u11189,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdfs_Seq),X0,X1) ).
cnf(u9579,axiom,
iext(uri_rdfs_member,uri_owl_DatatypeProperty,X0) ).
cnf(u457,axiom,
iext(uri_rdf_type,sK18,uri_owl_Restriction) ).
cnf(u8058,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdf_List),X0,X1) ).
cnf(u4251,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_AnnotationProperty)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u16618,axiom,
iext(uri_rdfs_domain,uri_rdfs_label,X0) ).
cnf(u4379,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| ~ iext(uri_rdfs_subClassOf,X1,X0)
| iext(uri_rdfs_subClassOf,X1,uri_owl_FunctionalProperty) ) ).
cnf(u702,axiom,
icext(uri_rdfs_Resource,X0) ).
cnf(u9665,axiom,
iext(uri_rdfs_member,uri_owl_FunctionalProperty,X0) ).
cnf(u2179,axiom,
( iext(uri_rdfs_domain,X0,uri_owl_Thing)
| ~ ip(X0) ) ).
cnf(u13611,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdfs_Datatype),X0) ).
cnf(u14546,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subPropertyOf,uri_rdfs_Seq),sK10(uri_rdfs_subPropertyOf,uri_rdfs_Seq)) ).
cnf(u12906,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Statement,uri_rdf_nil) ).
cnf(u3722,axiom,
( ~ icext(sK15(X0,uri_rdf_type),sK14(X0,uri_rdf_type))
| iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type) ) ).
cnf(u4078,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK18)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u7395,axiom,
iext(uri_owl_intersectionOf,uri_rdf_List,uri_rdf_nil) ).
cnf(u9584,axiom,
iext(uri_rdfs_member,uri_rdfs_Resource,uri_rdf_nil) ).
cnf(u2145,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Resource,uri_rdf_nil) ).
cnf(u6975,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Datatype) ).
cnf(u3723,axiom,
iext(uri_rdfs_subPropertyOf,X0,X0) ).
cnf(u16630,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Container),X0) ).
cnf(u11843,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_owl_Nothing),X0) ).
cnf(u698,axiom,
icext(uri_owl_Thing,X0) ).
cnf(u8999,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Container) ).
cnf(u8141,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdfs_Datatype),X0) ).
cnf(u7070,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(u2232,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt) ) ).
cnf(u13597,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdfs_Datatype),X0,X1) ).
cnf(u14532,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(u6948,axiom,
icext(uri_rdfs_Datatype,X0) ).
cnf(u15035,axiom,
( icext(sK15(uri_rdfs_range,X0),sK10(sK14(uri_rdfs_range,X0),sK18))
| iext(uri_rdfs_domain,sK14(uri_rdfs_range,X0),sK18)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0) ) ).
cnf(u16608,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(u11844,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_owl_Nothing),X0) ).
cnf(u1913,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing) ) ).
cnf(u16611,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(u8914,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(u3865,axiom,
( iext(X0,sK9(X0,uri_owl_FunctionalProperty),sK10(X0,uri_owl_FunctionalProperty))
| iext(uri_rdfs_domain,X0,uri_owl_FunctionalProperty) ) ).
cnf(u9899,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u14524,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing),sK10(uri_rdfs_subPropertyOf,uri_owl_Nothing)) ).
cnf(u9606,axiom,
iext(uri_rdfs_member,uri_rdf__1,X0) ).
cnf(u16754,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(u16105,axiom,
iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,sK18),X0) ).
cnf(u14554,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral),sK10(uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral)) ).
cnf(u8060,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdfs_Datatype),X0,X1) ).
cnf(u7643,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf__3,X0) ).
cnf(u362,axiom,
( ~ iext(uri_owl_someValuesFrom,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| icext(X2,sK17(X1,X2,X3))
| ~ icext(X0,X3) ) ).
cnf(u9900,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u4237,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_DatatypeProperty)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u2180,axiom,
icext(uri_rdfs_Class,X0) ).
cnf(u16604,axiom,
( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0)
| iext(X1,X2,sK17(X1,sK10(uri_owl_someValuesFrom,X0),X2))
| ~ icext(sK9(uri_owl_someValuesFrom,X0),X2) ) ).
cnf(u2586,axiom,
iext(uri_rdfs_range,X0,uri_owl_Thing) ).
cnf(u8135,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdf_List),X0) ).
cnf(u6942,axiom,
iext(uri_rdfs_range,uri_rdf__2,X0) ).
cnf(u5300,axiom,
~ iext(uri_owl_allValuesFrom,X0,X1) ).
cnf(u14788,axiom,
iext(uri_rdfs_range,X0,uri_owl_Restriction) ).
cnf(u4688,axiom,
iext(uri_rdfs_subClassOf,uri_owl_FunctionalProperty,X0) ).
cnf(u6479,axiom,
iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,uri_owl_Nothing),X0) ).
cnf(u11945,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_owl_Nothing),X0) ).
cnf(u439,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| ~ iext(uri_rdfs_subClassOf,X0,X1)
| iext(uri_rdfs_subClassOf,X0,X2) ) ).
cnf(u370,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property) ).
cnf(u14880,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_owl_Restriction),X0) ).
cnf(u5696,axiom,
iext(uri_rdfs_subPropertyOf,uri_owl_allValuesFrom,X0) ).
cnf(u9680,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdf_Alt),X0) ).
cnf(u6973,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Datatype,uri_rdf_nil) ).
cnf(u8140,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdfs_Datatype),X0) ).
cnf(u14267,axiom,
~ iext(sK9(uri_rdfs_range,uri_owl_FunctionalProperty),X0,X1) ).
cnf(u2322,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Resource) ).
cnf(u2996,axiom,
( icext(sK12(uri_owl_someValuesFrom,X0),sK17(X1,sK12(uri_owl_someValuesFrom,X0),X2))
| ~ iext(uri_owl_onProperty,sK11(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_range,uri_owl_someValuesFrom,X0)
| ~ icext(sK11(uri_owl_someValuesFrom,X0),X2) ) ).
cnf(u13902,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdfs_Datatype),X0) ).
cnf(u11269,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdfs_Seq),X0) ).
cnf(u9672,axiom,
iext(uri_rdfs_member,sK4(uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u4689,axiom,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,X0) ).
cnf(u9531,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_Container) ).
cnf(u3850,axiom,
( iext(X0,sK9(X0,uri_owl_Thing),sK10(X0,uri_owl_Thing))
| iext(uri_rdfs_domain,X0,uri_owl_Thing) ) ).
cnf(u2202,axiom,
icext(uri_rdf_Property,X0) ).
cnf(u9570,axiom,
iext(uri_rdfs_member,uri_owl_Nothing,X0) ).
cnf(u10672,axiom,
~ iext(sK9(uri_rdfs_domain,uri_owl_Nothing),X0,X1) ).
cnf(u14528,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing),sK10(uri_rdfs_subPropertyOf,uri_owl_Nothing)) ).
cnf(u16332,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,sK18),X0) ).
cnf(u348,axiom,
( ~ icext(X1,sK13(X0,X1))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u3009,axiom,
( ~ iext(uri_rdfs_subPropertyOf,sK12(uri_rdfs_subPropertyOf,X0),X1)
| iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0)
| iext(uri_rdfs_subPropertyOf,sK11(uri_rdfs_subPropertyOf,X0),X1) ) ).
cnf(u14188,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_owl_FunctionalProperty))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u299,axiom,
( ~ ioxp(X0)
| ~ iext(X0,X1,X2)
| ix(X1) ) ).
cnf(u9503,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_ContainerMembershipProperty) ).
cnf(u9637,axiom,
iext(uri_rdfs_member,uri_rdfs_isDefinedBy,X0) ).
cnf(u8642,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdf_Alt),X0) ).
cnf(u9951,axiom,
( icext(sK12(uri_rdfs_range,X0),sK10(sK11(uri_rdfs_range,X0),uri_rdfs_Seq))
| iext(uri_rdfs_domain,sK11(uri_rdfs_range,X0),uri_rdfs_Seq)
| iext(uri_rdfs_range,uri_rdfs_range,X0) ) ).
cnf(u454,negated_conjecture,
~ iext(uri_rdfs_subClassOf,uri_ex_InversesOfFunctionalProperties,uri_owl_InverseFunctionalProperty) ).
cnf(u4218,axiom,
iext(uri_rdfs_subClassOf,uri_owl_AnnotationProperty,X0) ).
cnf(u13128,axiom,
( icext(sK15(uri_rdfs_range,X0),sK10(sK14(uri_rdfs_range,X0),uri_owl_FunctionalProperty))
| iext(uri_rdfs_domain,sK14(uri_rdfs_range,X0),uri_owl_FunctionalProperty)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0) ) ).
cnf(u15032,axiom,
( icext(sK12(uri_rdfs_domain,X0),sK9(sK11(uri_rdfs_domain,X0),sK18))
| iext(uri_rdfs_domain,sK11(uri_rdfs_domain,X0),sK18)
| iext(uri_rdfs_range,uri_rdfs_domain,X0) ) ).
cnf(u4566,axiom,
iext(uri_rdfs_subClassOf,sK4(uri_rdfs_Datatype),X0) ).
cnf(u344,axiom,
( ~ iext(uri_rdfs_range,X0,X1)
| icext(X1,X3)
| ~ iext(X0,X2,X3) ) ).
cnf(u12422,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subClassOf,uri_rdf_XMLLiteral),X0) ).
cnf(u11260,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdfs_Seq),X0) ).
cnf(u311,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_Ontology)
| ix(X0) ) ).
cnf(u9552,axiom,
iext(uri_rdfs_member,X0,X0) ).
cnf(u4320,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| ~ iext(uri_rdfs_subClassOf,X1,X0)
| iext(uri_rdfs_subClassOf,X1,uri_rdf_Alt) ) ).
cnf(u9250,axiom,
iext(uri_rdfs_domain,X0,uri_rdf_Bag) ).
cnf(u3000,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(u9653,axiom,
iext(uri_rdfs_member,uri_rdfs_Seq,X0) ).
cnf(u7466,axiom,
( icext(sK15(uri_rdfs_domain,X0),sK9(sK14(uri_rdfs_domain,X0),uri_rdf_Alt))
| iext(uri_rdfs_domain,sK14(uri_rdfs_domain,X0),uri_rdf_Alt)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0) ) ).
cnf(u14540,axiom,
( ~ iext(sK9(uri_rdfs_subPropertyOf,uri_rdfs_Seq),sK14(X0,sK10(uri_rdfs_subPropertyOf,uri_rdfs_Seq)),sK15(X0,sK10(uri_rdfs_subPropertyOf,uri_rdfs_Seq)))
| iext(uri_rdfs_subPropertyOf,X0,sK10(uri_rdfs_subPropertyOf,uri_rdfs_Seq)) ) ).
cnf(u9645,axiom,
iext(uri_rdfs_member,uri_rdfs_label,X0) ).
cnf(u4551,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| ~ icext(X0,X1) ) ).
cnf(u4058,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class) ).
cnf(u8951,axiom,
~ iext(uri_rdf_object,X0,X1) ).
cnf(u7401,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(u2260,axiom,
( iext(X0,sK14(X0,X1),sK15(X0,X1))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u9650,axiom,
iext(uri_rdfs_member,uri_rdf_Bag,uri_rdf_nil) ).
cnf(u7053,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Literal) ).
cnf(u9509,axiom,
( iext(uri_rdfs_member,X0,X1)
| ~ icext(X1,X0) ) ).
cnf(u13126,axiom,
( icext(sK12(uri_rdfs_range,X0),sK10(sK11(uri_rdfs_range,X0),uri_owl_FunctionalProperty))
| iext(uri_rdfs_domain,sK11(uri_rdfs_range,X0),uri_owl_FunctionalProperty)
| iext(uri_rdfs_range,uri_rdfs_range,X0) ) ).
cnf(u4223,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_OntologyProperty)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u16639,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_FunctionalProperty),X0) ).
cnf(u6969,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Datatype) ).
cnf(u14125,axiom,
~ icext(sK9(uri_rdfs_subClassOf,uri_owl_FunctionalProperty),X0) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB028+3 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n026.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 07:09:12 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 Running first-order model finding
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.89/0.80 % (3669226)Will run a generic schedule for satisfiability detection.
% 1.89/0.80 % (3669234)dis+10_1_sil=32000:sp=arity:random_seed=1680097517:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.89/0.80 % (3669232)% WARNING: option uhcvi not known.
% 1.89/0.80 % (3669231)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2224005158_2999 on theBenchmark for (2999ds/0Mi)
% 1.89/0.80 % (3669232)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2510482294:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.89/0.80 % (3669236)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3220275554:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.89/0.80 % (3669233)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2586496498:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.89/0.80 % (3669235)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=398525244:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.89/0.80 % (3669237)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3817736507:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.89/0.80 % TRYING [1]
% 1.89/0.80 % TRYING [2]
% 1.89/0.80 % TRYING [3]
% 1.89/0.80 % (3669234)Instruction limit reached!
% 1.89/0.80 % (3669234)------------------------------
% 1.89/0.80 % (3669234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.80 % (3669234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.80 % (3669234)CaDiCaL version: 2.1.3
% 1.89/0.80 % (3669234)Termination reason: Instruction limit
% 1.89/0.80 % (3669234)Termination phase: Saturation
% 1.89/0.80 % (3669234)Time elapsed: 0.034 s
% 1.89/0.80 % (3669234)Peak memory usage: 13 MB
% 1.89/0.80 % (3669234)Instructions burned: 105 (million)
% 1.89/0.80 % (3669245)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1026228783:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.89/0.80 % TRYING [1]
% 1.89/0.80 % TRYING [2]
% 1.89/0.80 % TRYING [3]
% 1.89/0.80 % (3669235)Instruction limit reached!
% 1.89/0.80 % (3669235)------------------------------
% 1.89/0.80 % (3669235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.80 % (3669235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.80 % (3669235)CaDiCaL version: 2.1.3
% 1.89/0.80 % (3669235)Termination reason: Instruction limit
% 1.89/0.80 % (3669235)Termination phase: Saturation
% 1.89/0.80 % (3669235)Time elapsed: 0.049 s
% 1.89/0.80 % (3669235)Peak memory usage: 11 MB
% 1.89/0.80 % (3669235)Instructions burned: 117 (million)
% 1.89/0.80 % TRYING [4]
% 1.89/0.80 % TRYING [4]
% 1.89/0.80 % (3669236)Instruction limit reached!
% 1.89/0.80 % (3669236)------------------------------
% 1.89/0.80 % (3669236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.80 % (3669236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.80 % (3669236)CaDiCaL version: 2.1.3
% 1.89/0.80 % (3669236)Termination reason: Instruction limit
% 1.89/0.80 % (3669236)Termination phase: Saturation
% 1.89/0.80 % (3669236)Time elapsed: 0.068 s
% 1.89/0.80 % (3669236)Peak memory usage: 13 MB
% 1.89/0.80 % (3669236)Instructions burned: 131 (million)
% 1.89/0.80 % (3669247)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3265387486:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.89/0.80 % (3669248)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=2029659648:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.89/0.80 % (3669237)Instruction limit reached!
% 1.89/0.80 % (3669237)------------------------------
% 1.89/0.80 % (3669237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.80 % (3669237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.80 % (3669237)CaDiCaL version: 2.1.3
% 1.89/0.80 % (3669237)Termination reason: Instruction limit
% 1.89/0.80 % (3669237)Termination phase: Saturation
% 1.89/0.80 % (3669237)Time elapsed: 0.088 s
% 1.89/0.80 % (3669237)Peak memory usage: 14 MB
% 1.89/0.80 % (3669237)Instructions burned: 160 (million)
% 1.89/0.80 % (3669251)ott-21_1_sil=16000:fs=off:random_seed=1602327584:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.89/0.80 % (3669247)Instruction limit reached!
% 1.89/0.80 % (3669247)------------------------------
% 1.89/0.80 % (3669247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.80 % (3669247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.80 % (3669247)CaDiCaL version: 2.1.3
% 1.89/0.80 % (3669247)Termination reason: Instruction limit
% 1.89/0.80 % (3669247)Termination phase: Saturation
% 1.89/0.80 % (3669247)Time elapsed: 0.065 s
% 1.89/0.80 % (3669247)Peak memory usage: 13 MB
% 1.89/0.80 % (3669247)Instructions burned: 132 (million)
% 1.89/0.80 % (3669253)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3767430934:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.89/0.80 % (3669251)Instruction limit reached!
% 1.89/0.80 % (3669251)------------------------------
% 1.89/0.80 % (3669251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.80 % (3669251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.80 % (3669251)CaDiCaL version: 2.1.3
% 1.89/0.80 % (3669251)Termination reason: Instruction limit
% 1.89/0.80 % (3669251)Termination phase: Saturation
% 1.89/0.80 % (3669251)Time elapsed: 0.091 s
% 1.89/0.80 % (3669251)Peak memory usage: 14 MB
% 1.89/0.80 % (3669251)Instructions burned: 180 (million)
% 1.89/0.80 % (3669255)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2042457699:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.89/0.80 % TRYING [5]
% 1.89/0.80 % (3669245)Instruction limit reached!
% 1.89/0.80 % (3669245)------------------------------
% 1.89/0.80 % (3669245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.80 % (3669245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.80 % (3669245)CaDiCaL version: 2.1.3
% 1.89/0.80 % (3669245)Termination reason: Instruction limit
% 1.89/0.80 % (3669245)Termination phase: Finite model building constraint generation
% 1.89/0.80 % (3669245)Time elapsed: 0.197 s
% 1.89/0.80 % (3669245)Peak memory usage: 25 MB
% 1.89/0.80 % (3669245)Instructions burned: 717 (million)
% 1.89/0.80 % TRYING [1]
% 1.89/0.80 % TRYING [2]
% 1.89/0.80 % (3669257)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1504003794:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 1.89/0.80 % TRYING [3]
% 1.89/0.80 % (3669248) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3669226-3669248"...
% 1.89/0.80 % (3669248)...printing done.
% 1.89/0.80 % SZS status CounterSatisfiable for theBenchmark
% 1.89/0.80 % SZS output start Saturation.
% See solution above
% 1.89/0.81 % SZS output start Definitions and Model Updates.
% 1.89/0.81 for all groundings,
% 1.89/0.81 whenever iext(uri_rdf_type,X0,uri_rdfs_Datatype) is false, set ~idc(X0) to true
% 1.89/0.81 for all groundings,
% 1.89/0.81 whenever iext(uri_rdf_type,X0,uri_owl_AnnotationProperty) is false, set ~ioap(X0) to true
% 1.89/0.81 for all groundings,
% 1.89/0.81 whenever iext(uri_rdf_type,X0,uri_owl_DatatypeProperty) is false, set ~iodp(X0) to true
% 1.89/0.81 for all groundings,
% 1.89/0.81 whenever iext(uri_rdf_type,X0,uri_owl_OntologyProperty) is false, set ~ioxp(X0) to true
% 1.89/0.81 % SZS output end Definitions and Model Updates.
% 1.89/0.81 % (3669248)------------------------------
% 1.89/0.81 % (3669248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.81 % (3669248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.81 % (3669248)CaDiCaL version: 2.1.3
% 1.89/0.81 % (3669248)Termination reason: Satisfiable
% 1.89/0.81 % (3669248)Time elapsed: 0.241 s
% 1.89/0.81 % (3669248)Peak memory usage: 18 MB
% 1.89/0.81 % (3669248)Instructions burned: 399 (million)
% 1.89/0.81 % (3669226)Success in time 0.376 s
% 1.89/0.81 % Vampire exiting
%------------------------------------------------------------------------------