%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWB004+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 : n002.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:29 PM UTC 2026
% Result : CounterSatisfiable 1.46s 0.65s
% Output : Saturation 1.46s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u473,negated_conjecture,
~ iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class) ).
cnf(u488,axiom,
ic(uri_rdfs_Resource) ).
cnf(u532,axiom,
ic(uri_rdfs_Literal) ).
cnf(u572,axiom,
ic(uri_rdf_List) ).
cnf(u577,axiom,
icext(uri_rdfs_Resource,uri_rdf_nil) ).
cnf(u628,axiom,
( iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal)
| ~ ic(X0) ) ).
cnf(u633,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Literal) ).
cnf(u684,axiom,
icext(uri_rdfs_Literal,uri_rdf_nil) ).
cnf(u710,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Literal) ).
cnf(u731,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Literal) ).
cnf(u746,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Literal) ).
cnf(u816,axiom,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_rdfs_Resource) ).
cnf(u822,axiom,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_rdfs_Literal) ).
cnf(u1004,axiom,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_owl_Thing) ).
cnf(u1073,axiom,
( ioap(sK13(uri_owl_AnnotationProperty,X0))
| iext(uri_rdfs_subClassOf,uri_owl_AnnotationProperty,X0)
| ~ ic(X0) ) ).
cnf(u1082,axiom,
( iodp(sK13(uri_owl_DatatypeProperty,X0))
| iext(uri_rdfs_subClassOf,uri_owl_DatatypeProperty,X0)
| ~ ic(X0) ) ).
cnf(u1091,axiom,
( ioxp(sK13(uri_owl_OntologyProperty,X0))
| iext(uri_rdfs_subClassOf,uri_owl_OntologyProperty,X0)
| ~ ic(X0) ) ).
cnf(u1161,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Literal) ).
cnf(u1176,axiom,
( ix(sK13(uri_owl_Ontology,X0))
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0)
| ~ ic(X0) ) ).
cnf(u1456,axiom,
iext(uri_owl_unionOf,uri_rdfs_Statement,uri_rdf_nil) ).
cnf(u1469,axiom,
icext(uri_rdf_XMLLiteral,sK4(uri_rdf_XMLLiteral)) ).
cnf(u1474,axiom,
iext(uri_owl_unionOf,uri_rdfs_Seq,uri_rdf_nil) ).
cnf(u1482,axiom,
~ iext(uri_owl_unionOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_nil) ).
cnf(u1487,axiom,
icext(uri_rdfs_ContainerMembershipProperty,sK4(uri_rdfs_ContainerMembershipProperty)) ).
cnf(u1496,axiom,
icext(uri_rdf_Bag,sK4(uri_rdf_Bag)) ).
cnf(u1505,axiom,
icext(uri_rdfs_Container,sK4(uri_rdfs_Container)) ).
cnf(u1514,axiom,
icext(uri_rdf_Alt,sK4(uri_rdf_Alt)) ).
cnf(u1523,axiom,
icext(uri_rdf_List,sK4(uri_rdf_List)) ).
cnf(u1532,axiom,
icext(uri_rdfs_Literal,sK4(uri_rdfs_Literal)) ).
cnf(u1541,axiom,
icext(uri_rdf_Property,sK4(uri_rdf_Property)) ).
cnf(u1545,axiom,
~ iext(uri_owl_unionOf,uri_rdfs_Datatype,uri_rdf_nil) ).
cnf(u1550,axiom,
icext(uri_rdfs_Datatype,sK4(uri_rdfs_Datatype)) ).
cnf(u1554,axiom,
~ iext(uri_owl_unionOf,uri_rdfs_Class,uri_rdf_nil) ).
cnf(u1559,axiom,
icext(uri_rdfs_Class,sK4(uri_rdfs_Class)) ).
cnf(u1688,axiom,
icext(uri_rdfs_Class,uri_owl_Nothing) ).
cnf(u1795,axiom,
icext(uri_rdfs_Class,uri_rdfs_Literal) ).
cnf(u1805,axiom,
icext(uri_rdfs_Class,uri_rdfs_Class) ).
cnf(u1830,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_member) ).
cnf(u1882,axiom,
iext(uri_owl_intersectionOf,uri_rdf_Property,uri_rdf_nil) ).
cnf(u1891,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Class,uri_rdf_nil) ).
cnf(u1914,axiom,
( ~ ip(X0)
| iext(uri_rdfs_range,X0,uri_owl_Thing) ) ).
cnf(u2007,axiom,
( ~ iext(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1,X2)
| iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0)
| ~ ic(X0)
| iext(uri_rdfs_member,X1,X2) ) ).
cnf(u2108,axiom,
iext(uri_rdfs_domain,sK4(uri_rdf_Property),uri_owl_Nothing) ).
cnf(u2121,axiom,
iext(sK4(uri_rdfs_ContainerMembershipProperty),sK9(sK4(uri_rdfs_ContainerMembershipProperty),uri_owl_Nothing),sK10(sK4(uri_rdfs_ContainerMembershipProperty),uri_owl_Nothing)) ).
cnf(u2126,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_member,uri_owl_Nothing) ).
cnf(u2131,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_member,uri_owl_Nothing),sK10(uri_rdfs_member,uri_owl_Nothing)) ).
cnf(u2140,axiom,
iext(uri_rdfs_label,sK9(uri_rdfs_label,uri_owl_Nothing),sK10(uri_rdfs_label,uri_owl_Nothing)) ).
cnf(u2145,axiom,
iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_owl_Nothing) ).
cnf(u2154,axiom,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_owl_Nothing) ).
cnf(u2163,axiom,
iext(uri_rdfs_domain,uri_rdfs_comment,uri_owl_Nothing) ).
cnf(u2177,axiom,
iext(uri_rdf_value,sK9(uri_rdf_value,uri_owl_Nothing),sK10(uri_rdf_value,uri_owl_Nothing)) ).
cnf(u2183,axiom,
iext(uri_rdfs_domain,uri_rdf__3,uri_owl_Nothing) ).
cnf(u2192,axiom,
iext(uri_rdfs_domain,uri_rdf__2,uri_owl_Nothing) ).
cnf(u2201,axiom,
iext(uri_rdfs_domain,uri_rdf__1,uri_owl_Nothing) ).
cnf(u2209,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_owl_Nothing) ).
cnf(u2214,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing),sK10(uri_rdfs_subPropertyOf,uri_owl_Nothing)) ).
cnf(u2218,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_owl_Nothing) ).
cnf(u2223,axiom,
iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,uri_owl_Nothing),sK10(uri_rdfs_subClassOf,uri_owl_Nothing)) ).
cnf(u2227,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_range,uri_owl_Nothing) ).
cnf(u2232,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_owl_Nothing),sK10(uri_rdfs_range,uri_owl_Nothing)) ).
cnf(u2236,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_domain,uri_owl_Nothing) ).
cnf(u2241,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Nothing),sK10(uri_rdfs_domain,uri_owl_Nothing)) ).
cnf(u2250,axiom,
iext(uri_owl_someValuesFrom,sK9(uri_owl_someValuesFrom,uri_owl_Nothing),sK10(uri_owl_someValuesFrom,uri_owl_Nothing)) ).
cnf(u2255,axiom,
iext(uri_rdfs_domain,uri_owl_onProperty,uri_owl_Nothing) ).
cnf(u2264,axiom,
iext(uri_rdfs_domain,uri_rdf_List,uri_owl_Nothing) ).
cnf(u2273,axiom,
iext(uri_rdfs_domain,uri_owl_hasValue,uri_owl_Nothing) ).
cnf(u2282,axiom,
iext(uri_rdfs_domain,uri_owl_allValuesFrom,uri_owl_Nothing) ).
cnf(u2295,axiom,
iext(uri_rdfs_Literal,sK9(uri_rdfs_Literal,uri_owl_Nothing),sK10(uri_rdfs_Literal,uri_owl_Nothing)) ).
cnf(u2304,axiom,
iext(uri_rdfs_Resource,sK9(uri_rdfs_Resource,uri_owl_Nothing),sK10(uri_rdfs_Resource,uri_owl_Nothing)) ).
cnf(u2313,axiom,
iext(uri_rdf_Property,sK9(uri_rdf_Property,uri_owl_Nothing),sK10(uri_rdf_Property,uri_owl_Nothing)) ).
cnf(u2318,axiom,
iext(uri_rdfs_domain,uri_rdfs_Class,uri_owl_Nothing) ).
cnf(u2331,axiom,
iext(uri_rdf_type,sK9(uri_rdf_type,uri_owl_Nothing),sK10(uri_rdf_type,uri_owl_Nothing)) ).
cnf(u2340,axiom,
iext(uri_owl_unionOf,sK9(uri_owl_unionOf,uri_owl_Nothing),sK10(uri_owl_unionOf,uri_owl_Nothing)) ).
cnf(u2349,axiom,
iext(uri_rdf_rest,sK9(uri_rdf_rest,uri_owl_Nothing),sK10(uri_rdf_rest,uri_owl_Nothing)) ).
cnf(u2358,axiom,
iext(uri_rdf_first,sK9(uri_rdf_first,uri_owl_Nothing),sK10(uri_rdf_first,uri_owl_Nothing)) ).
cnf(u2367,axiom,
iext(uri_owl_intersectionOf,sK9(uri_owl_intersectionOf,uri_owl_Nothing),sK10(uri_owl_intersectionOf,uri_owl_Nothing)) ).
cnf(u2376,axiom,
iext(uri_owl_complementOf,sK9(uri_owl_complementOf,uri_owl_Nothing),sK10(uri_owl_complementOf,uri_owl_Nothing)) ).
cnf(u2764,axiom,
ix(sK4(uri_owl_Ontology)) ).
cnf(u2777,axiom,
iext(uri_owl_unionOf,uri_owl_OntologyProperty,uri_rdf_nil) ).
cnf(u2786,axiom,
iext(uri_owl_unionOf,uri_owl_DatatypeProperty,uri_rdf_nil) ).
cnf(u2795,axiom,
iext(uri_owl_unionOf,uri_owl_AnnotationProperty,uri_rdf_nil) ).
cnf(u2888,axiom,
iext(uri_owl_unionOf,sK10(uri_owl_complementOf,uri_owl_Nothing),uri_rdf_nil) ).
cnf(u2941,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing),uri_rdfs_member) ).
cnf(u3023,axiom,
iext(uri_owl_unionOf,sK9(uri_rdfs_subClassOf,uri_owl_Nothing),uri_rdf_nil) ).
cnf(u3290,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing),uri_rdf_List) ).
cnf(u3299,axiom,
icext(sK10(uri_rdfs_range,uri_owl_Nothing),sK10(sK9(uri_rdfs_range,uri_owl_Nothing),uri_rdf_List)) ).
cnf(u3308,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK9(sK9(uri_rdfs_domain,uri_owl_Nothing),uri_rdf_List)) ).
cnf(u3317,axiom,
iext(uri_rdfs_member,sK9(sK4(uri_rdfs_ContainerMembershipProperty),uri_rdf_List),sK10(sK4(uri_rdfs_ContainerMembershipProperty),uri_rdf_List)) ).
cnf(u3329,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_List) ).
cnf(u3341,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdf_List) ).
cnf(u3349,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdf_List),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdf_List),X0) ) ).
cnf(u3357,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdf_List),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdf_List),X0) ) ).
cnf(u3366,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_someValuesFrom,uri_rdf_List)) ).
cnf(u3379,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdf_List) ).
cnf(u3384,axiom,
icext(uri_rdf_List,sK10(uri_owl_unionOf,uri_rdf_List)) ).
cnf(u3397,axiom,
iext(uri_rdfs_domain,uri_owl_intersectionOf,uri_rdf_List) ).
cnf(u3405,axiom,
iext(uri_rdfs_domain,uri_owl_complementOf,uri_rdf_List) ).
cnf(u3485,axiom,
icext(uri_rdf_List,sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing)) ).
cnf(u3554,axiom,
icext(sK10(uri_rdfs_domain,uri_rdf_List),sK9(sK9(uri_rdfs_domain,uri_rdf_List),uri_rdfs_Statement)) ).
cnf(u3567,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_List),uri_rdfs_Statement) ).
cnf(u3576,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing),uri_rdfs_Statement) ).
cnf(u3585,axiom,
icext(sK10(uri_rdfs_range,uri_owl_Nothing),sK10(sK9(uri_rdfs_range,uri_owl_Nothing),uri_rdfs_Statement)) ).
cnf(u3594,axiom,
icext(sK10(uri_rdfs_domain,uri_owl_Nothing),sK9(sK9(uri_rdfs_domain,uri_owl_Nothing),uri_rdfs_Statement)) ).
cnf(u3603,axiom,
iext(uri_rdfs_member,sK9(sK4(uri_rdfs_ContainerMembershipProperty),uri_rdfs_Statement),sK10(sK4(uri_rdfs_ContainerMembershipProperty),uri_rdfs_Statement)) ).
cnf(u3611,axiom,
( iext(sK10(uri_rdfs_subPropertyOf,uri_rdfs_Statement),X0,X1)
| ~ iext(sK9(uri_rdfs_subPropertyOf,uri_rdfs_Statement),X0,X1) ) ).
cnf(u3614,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdfs_Statement) ).
cnf(u3619,axiom,
( ~ iext(uri_rdfs_subPropertyOf,sK10(uri_rdfs_subPropertyOf,uri_rdfs_Statement),X0)
| iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_rdfs_Statement),X0) ) ).
cnf(u3623,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,uri_rdfs_Statement),X0)
| icext(sK10(uri_rdfs_subClassOf,uri_rdfs_Statement),X0) ) ).
cnf(u3626,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Statement) ).
cnf(u3631,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_rdfs_Statement))
| iext(uri_rdfs_subClassOf,X0,sK10(uri_rdfs_subClassOf,uri_rdfs_Statement)) ) ).
cnf(u3635,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdfs_Statement),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdfs_Statement),X0) ) ).
cnf(u3643,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdfs_Statement),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdfs_Statement),X0) ) ).
cnf(u3646,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdfs_Statement) ).
cnf(u3652,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_someValuesFrom,uri_rdfs_Statement)) ).
cnf(u3655,axiom,
~ iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_rdfs_Statement) ).
cnf(u3661,axiom,
icext(sK10(uri_rdf_type,uri_rdfs_Statement),sK9(uri_rdf_type,uri_rdfs_Statement)) ).
cnf(u3664,axiom,
~ iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Statement) ).
cnf(u3669,axiom,
( icext(sK10(uri_owl_complementOf,uri_rdfs_Statement),X0)
| icext(sK9(uri_owl_complementOf,uri_rdfs_Statement),X0) ) ).
cnf(u3672,axiom,
~ iext(uri_rdfs_domain,uri_owl_complementOf,uri_rdfs_Statement) ).
cnf(u3677,axiom,
( ~ icext(sK10(uri_owl_complementOf,uri_rdfs_Statement),X0)
| ~ icext(sK9(uri_owl_complementOf,uri_rdfs_Statement),X0) ) ).
cnf(u4212,axiom,
iext(uri_owl_unionOf,sK9(uri_rdfs_subClassOf,uri_rdfs_Statement),uri_rdf_nil) ).
cnf(u4249,axiom,
iext(uri_owl_intersectionOf,sK10(uri_owl_complementOf,uri_rdfs_Statement),uri_rdf_nil) ).
cnf(u4317,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Statement),uri_rdfs_Statement) ).
cnf(u4337,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Statement),uri_rdfs_Statement) ).
cnf(u4394,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_rdfs_Statement),uri_rdfs_member) ).
cnf(u4408,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_subPropertyOf,uri_rdfs_Statement),uri_rdfs_Statement) ).
cnf(u4459,axiom,
icext(sK10(uri_rdfs_domain,uri_rdf_List),sK9(sK9(uri_rdfs_domain,uri_rdf_List),uri_owl_Nothing)) ).
cnf(u4472,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_Nothing),uri_owl_Nothing) ).
cnf(u4481,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Nothing),uri_owl_Nothing) ).
cnf(u4561,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_List),uri_rdfs_Datatype) ).
cnf(u4570,axiom,
iext(uri_rdfs_domain,sK4(uri_rdfs_ContainerMembershipProperty),uri_rdfs_Datatype) ).
cnf(u4578,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdfs_Datatype) ).
cnf(u4590,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Datatype) ).
cnf(u4598,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdfs_Datatype),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdfs_Datatype),X0) ) ).
cnf(u4606,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdfs_Datatype),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdfs_Datatype),X0) ) ).
cnf(u4619,axiom,
iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_rdfs_Datatype) ).
cnf(u4628,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Datatype) ).
cnf(u4636,axiom,
iext(uri_rdfs_domain,uri_owl_complementOf,uri_rdfs_Datatype) ).
cnf(u4719,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Datatype),uri_owl_Nothing) ).
cnf(u4732,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Datatype),sK10(sK9(uri_rdfs_range,uri_rdfs_Datatype),uri_rdfs_Statement)) ).
cnf(u4751,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Datatype),uri_owl_Nothing) ).
cnf(u4764,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Datatype),sK9(sK9(uri_rdfs_domain,uri_rdfs_Datatype),uri_rdfs_Statement)) ).
cnf(u4820,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_List),uri_rdf_Alt) ).
cnf(u4829,axiom,
iext(uri_rdfs_domain,sK4(uri_rdfs_ContainerMembershipProperty),uri_rdf_Alt) ).
cnf(u4837,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Alt) ).
cnf(u4849,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdf_Alt) ).
cnf(u4857,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdf_Alt),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdf_Alt),X0) ) ).
cnf(u4865,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdf_Alt),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdf_Alt),X0) ) ).
cnf(u4878,axiom,
iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_rdf_Alt) ).
cnf(u4887,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdf_Alt) ).
cnf(u4895,axiom,
iext(uri_rdfs_domain,uri_owl_complementOf,uri_rdf_Alt) ).
cnf(u4997,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_Alt),uri_owl_Nothing) ).
cnf(u5010,axiom,
icext(sK10(uri_rdfs_range,uri_rdf_Alt),sK10(sK9(uri_rdfs_range,uri_rdf_Alt),uri_rdfs_Statement)) ).
cnf(u5029,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_Alt),uri_owl_Nothing) ).
cnf(u5042,axiom,
icext(sK10(uri_rdfs_domain,uri_rdf_Alt),sK9(sK9(uri_rdfs_domain,uri_rdf_Alt),uri_rdfs_Statement)) ).
cnf(u5100,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_List),uri_rdf_Bag) ).
cnf(u5109,axiom,
iext(uri_rdfs_domain,sK4(uri_rdfs_ContainerMembershipProperty),uri_rdf_Bag) ).
cnf(u5117,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Bag) ).
cnf(u5129,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdf_Bag) ).
cnf(u5137,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdf_Bag),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdf_Bag),X0) ) ).
cnf(u5145,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdf_Bag),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdf_Bag),X0) ) ).
cnf(u5158,axiom,
iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_rdf_Bag) ).
cnf(u5167,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdf_Bag) ).
cnf(u5175,axiom,
iext(uri_rdfs_domain,uri_owl_complementOf,uri_rdf_Bag) ).
cnf(u5261,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_Bag),uri_owl_Nothing) ).
cnf(u5274,axiom,
icext(sK10(uri_rdfs_range,uri_rdf_Bag),sK10(sK9(uri_rdfs_range,uri_rdf_Bag),uri_rdfs_Statement)) ).
cnf(u5293,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_Bag),uri_owl_Nothing) ).
cnf(u5306,axiom,
icext(sK10(uri_rdfs_domain,uri_rdf_Bag),sK9(sK9(uri_rdfs_domain,uri_rdf_Bag),uri_rdfs_Statement)) ).
cnf(u5366,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_List),uri_rdfs_ContainerMembershipProperty) ).
cnf(u5375,axiom,
iext(uri_rdfs_domain,sK4(uri_rdfs_ContainerMembershipProperty),uri_rdfs_ContainerMembershipProperty) ).
cnf(u5383,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdfs_ContainerMembershipProperty) ).
cnf(u5395,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty) ).
cnf(u5403,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X0) ) ).
cnf(u5411,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),X0) ) ).
cnf(u5424,axiom,
iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_rdfs_ContainerMembershipProperty) ).
cnf(u5433,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_ContainerMembershipProperty) ).
cnf(u5441,axiom,
iext(uri_rdfs_domain,uri_owl_complementOf,uri_rdfs_ContainerMembershipProperty) ).
cnf(u5859,axiom,
icext(sK14(uri_owl_complementOf,uri_rdf_type),sK14(uri_owl_complementOf,uri_rdf_type)) ).
cnf(u5987,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),uri_owl_Nothing) ).
cnf(u6000,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),sK10(sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),uri_rdfs_Statement)) ).
cnf(u6025,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),uri_owl_Nothing) ).
cnf(u6038,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),sK9(sK9(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),uri_rdfs_Statement)) ).
cnf(u6067,axiom,
icext(sK14(uri_owl_complementOf,uri_rdfs_member),sK14(uri_owl_complementOf,uri_rdfs_member)) ).
cnf(u6132,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_List),uri_rdfs_Seq) ).
cnf(u6137,axiom,
iext(uri_rdfs_member,sK9(sK4(uri_rdfs_ContainerMembershipProperty),uri_rdfs_Seq),sK10(sK4(uri_rdfs_ContainerMembershipProperty),uri_rdfs_Seq)) ).
cnf(u6140,axiom,
~ iext(uri_rdfs_domain,sK4(uri_rdfs_ContainerMembershipProperty),uri_rdfs_Seq) ).
cnf(u6145,axiom,
( iext(sK10(uri_rdfs_subPropertyOf,uri_rdfs_Seq),X0,X1)
| ~ iext(sK9(uri_rdfs_subPropertyOf,uri_rdfs_Seq),X0,X1) ) ).
cnf(u6148,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdfs_Seq) ).
cnf(u6153,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(u6157,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,uri_rdfs_Seq),X0)
| icext(sK10(uri_rdfs_subClassOf,uri_rdfs_Seq),X0) ) ).
cnf(u6160,axiom,
~ iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Seq) ).
cnf(u6165,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(u6169,axiom,
( ~ iext(sK9(uri_rdfs_range,uri_rdfs_Seq),X1,X0)
| icext(sK10(uri_rdfs_range,uri_rdfs_Seq),X0) ) ).
cnf(u6177,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdfs_Seq),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdfs_Seq),X0) ) ).
cnf(u6186,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_someValuesFrom,uri_rdfs_Seq)) ).
cnf(u6189,axiom,
~ iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_rdfs_Seq) ).
cnf(u6195,axiom,
icext(sK10(uri_rdf_type,uri_rdfs_Seq),sK9(uri_rdf_type,uri_rdfs_Seq)) ).
cnf(u6198,axiom,
~ iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Seq) ).
cnf(u6203,axiom,
( icext(sK10(uri_owl_complementOf,uri_rdfs_Seq),X0)
| icext(sK9(uri_owl_complementOf,uri_rdfs_Seq),X0) ) ).
cnf(u6206,axiom,
~ iext(uri_rdfs_domain,uri_owl_complementOf,uri_rdfs_Seq) ).
cnf(u6211,axiom,
( ~ icext(sK10(uri_owl_complementOf,uri_rdfs_Seq),X0)
| ~ icext(sK9(uri_owl_complementOf,uri_rdfs_Seq),X0) ) ).
cnf(u6800,axiom,
iext(uri_owl_unionOf,sK9(uri_rdfs_subClassOf,uri_rdfs_Seq),uri_rdf_nil) ).
cnf(u6838,axiom,
iext(uri_owl_intersectionOf,sK10(uri_owl_complementOf,uri_rdfs_Seq),uri_rdf_nil) ).
cnf(u6896,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Seq),uri_rdfs_Seq) ).
cnf(u6909,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Seq),sK10(sK9(uri_rdfs_range,uri_rdfs_Seq),uri_owl_Nothing)) ).
cnf(u6918,axiom,
icext(sK10(uri_rdfs_range,uri_rdfs_Seq),sK10(sK9(uri_rdfs_range,uri_rdfs_Seq),uri_rdfs_Statement)) ).
cnf(u6947,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Seq),uri_rdfs_Seq) ).
cnf(u6960,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Seq),sK9(sK9(uri_rdfs_domain,uri_rdfs_Seq),uri_owl_Nothing)) ).
cnf(u6969,axiom,
icext(sK10(uri_rdfs_domain,uri_rdfs_Seq),sK9(sK9(uri_rdfs_domain,uri_rdfs_Seq),uri_rdfs_Statement)) ).
cnf(u7131,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_XMLLiteral) ).
cnf(u7143,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdf_XMLLiteral) ).
cnf(u7155,axiom,
iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_XMLLiteral) ).
cnf(u7159,axiom,
( ~ iext(sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),X0,X1)
| icext(sK10(uri_rdfs_domain,uri_rdf_XMLLiteral),X0) ) ).
cnf(u7168,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_someValuesFrom,uri_rdf_XMLLiteral)) ).
cnf(u7181,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdf_XMLLiteral) ).
cnf(u7189,axiom,
iext(uri_rdfs_domain,uri_owl_complementOf,uri_rdf_XMLLiteral) ).
cnf(u7322,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),uri_rdfs_Statement) ).
cnf(u7335,axiom,
icext(sK10(uri_rdfs_domain,uri_rdf_XMLLiteral),sK9(sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),uri_rdfs_Seq)) ).
cnf(u7344,axiom,
icext(sK10(uri_rdfs_domain,uri_rdf_XMLLiteral),sK9(sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),uri_owl_Nothing)) ).
cnf(u3101,axiom,
iext(uri_rdfs_range,uri_rdf_object,X0) ).
cnf(u2584,axiom,
~ iext(uri_owl_allValuesFrom,X0,X1) ).
cnf(u7298,axiom,
iext(uri_rdfs_domain,X0,uri_rdf_XMLLiteral) ).
cnf(u6046,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),X0,X1) ).
cnf(u4486,axiom,
~ iext(sK9(uri_rdfs_domain,uri_owl_Nothing),X0,X1) ).
cnf(u2445,axiom,
~ iext(uri_rdfs_comment,X0,X1) ).
cnf(u3105,axiom,
iext(uri_rdfs_range,uri_rdfs_seeAlso,X0) ).
cnf(u406,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty) ).
cnf(u4263,axiom,
iext(uri_rdfs_subClassOf,X0,sK10(uri_owl_complementOf,uri_rdfs_Statement)) ).
cnf(u2959,axiom,
( iext(uri_rdf_type,sK13(uri_owl_Ontology,X0),uri_owl_Ontology)
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ) ).
cnf(u3107,axiom,
iext(uri_rdfs_range,sK4(uri_rdf_Property),X0) ).
cnf(u4484,axiom,
~ iext(sK9(uri_rdfs_range,uri_owl_Nothing),X0,X1) ).
cnf(u5013,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdf_Alt),X0,X1) ).
cnf(u3096,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(u7400,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_owl_Nothing),X0) ).
cnf(u5684,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_owl_Nothing),X0) ).
cnf(u5547,axiom,
iext(uri_rdfs_member,uri_rdfs_Datatype,uri_rdf_nil) ).
cnf(u6974,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdfs_Seq),X0) ).
cnf(u2587,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Resource) ).
cnf(u4141,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing),X0) ).
cnf(u5521,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_ContainerMembershipProperty) ).
cnf(u7389,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(u5536,axiom,
( icext(sK11(uri_owl_complementOf,X0),sK0(sK12(uri_owl_complementOf,X0)))
| iext(uri_rdfs_range,uri_owl_complementOf,X0)
| iext(uri_owl_intersectionOf,sK12(uri_owl_complementOf,X0),uri_rdf_nil) ) ).
cnf(u5688,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdf_Bag),X0) ).
cnf(u5538,axiom,
( icext(sK11(uri_owl_complementOf,X0),sK12(X1,sK12(uri_owl_complementOf,X0)))
| iext(uri_rdfs_range,uri_owl_complementOf,X0)
| iext(uri_rdfs_range,X1,sK12(uri_owl_complementOf,X0)) ) ).
cnf(u5692,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_owl_Nothing),X0) ).
cnf(u2715,axiom,
icext(uri_owl_Restriction,sK9(uri_owl_someValuesFrom,uri_owl_Nothing)) ).
cnf(u3120,axiom,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ icext(X2,sK5(X0,X2))
| ~ icext(X0,sK5(X0,X2))
| iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u6875,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_owl_complementOf,uri_rdfs_Seq))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u5782,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(u689,axiom,
icext(uri_rdfs_Literal,X0) ).
cnf(u5540,axiom,
( iext(uri_rdfs_member,sK11(X0,X1),sK12(X0,X1))
| iext(uri_rdfs_range,X0,X1) ) ).
cnf(u2478,axiom,
~ iext(uri_rdf__2,X0,X1) ).
cnf(u6973,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdfs_Seq),X0,X1) ).
cnf(u6079,axiom,
( iext(uri_rdfs_member,sK9(X0,uri_rdfs_Seq),sK10(X0,uri_rdfs_Seq))
| iext(uri_rdfs_domain,X0,uri_rdfs_Seq) ) ).
cnf(u7387,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,X0),X1)
| icext(sK10(uri_rdfs_subClassOf,X0),X1)
| iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0) ) ).
cnf(u5544,axiom,
iext(uri_rdfs_member,sK9(uri_owl_complementOf,uri_owl_Nothing),sK10(uri_owl_complementOf,uri_owl_Nothing)) ).
cnf(u5557,axiom,
iext(uri_rdfs_member,sK10(uri_owl_complementOf,uri_rdfs_Statement),uri_rdf_nil) ).
cnf(u7503,axiom,
( ~ icext(sK10(uri_owl_complementOf,X0),sK13(sK9(uri_owl_complementOf,X0),X1))
| iext(uri_rdfs_domain,uri_owl_complementOf,X0)
| iext(uri_rdfs_subClassOf,sK9(uri_owl_complementOf,X0),X1) ) ).
cnf(u7663,axiom,
( ~ icext(sK10(uri_owl_complementOf,X0),sK12(X1,sK10(uri_owl_complementOf,X0)))
| iext(uri_rdfs_range,X1,sK10(uri_owl_complementOf,X0))
| iext(uri_rdfs_domain,uri_owl_complementOf,X0) ) ).
cnf(u346,axiom,
( icext(X0,sK13(X0,X1))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u5576,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_Literal) ).
cnf(u5204,axiom,
icext(uri_rdf_Bag,X0) ).
cnf(u2917,axiom,
iext(uri_rdfs_domain,X0,sK9(uri_owl_complementOf,uri_owl_Nothing)) ).
cnf(u5958,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(u2915,axiom,
iext(uri_rdfs_subClassOf,X0,sK9(uri_owl_complementOf,uri_owl_Nothing)) ).
cnf(u451,axiom,
ir(X0) ).
cnf(u5593,axiom,
iext(uri_rdfs_member,sK9(uri_rdf_type,uri_owl_Nothing),sK10(uri_rdf_type,uri_owl_Nothing)) ).
cnf(u5246,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag) ).
cnf(u3430,axiom,
( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| ~ icext(X4,sK7(X0,X2,X4,X6))
| ~ icext(X0,sK7(X0,X2,X4,X6))
| iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u5694,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdf_Alt),X0) ).
cnf(u4704,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype) ).
cnf(u4324,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdfs_Statement),X0,X1) ).
cnf(u3434,axiom,
( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| ~ icext(X2,sK7(X0,X2,X4,X6))
| ~ icext(X0,sK7(X0,X2,X4,X6))
| iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u6848,axiom,
( icext(sK15(uri_rdfs_range,X0),sK10(sK14(uri_rdfs_range,X0),uri_rdfs_Statement))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0)
| iext(uri_rdfs_domain,sK14(uri_rdfs_range,X0),uri_rdfs_Statement) ) ).
cnf(u1625,axiom,
~ iext(uri_rdf_object,X0,X1) ).
cnf(u223,axiom,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| icext(X2,X3)
| ~ icext(X0,X3)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u3170,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,X0) ).
cnf(u6124,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(u256,axiom,
( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| icext(X4,X5)
| icext(X2,X5)
| ~ icext(X0,X5)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u7378,axiom,
iext(uri_rdfs_domain,uri_rdfs_Class,X0) ).
cnf(u5883,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(u4346,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdfs_Statement),X0) ).
cnf(u5728,axiom,
iext(uri_rdfs_member,uri_rdfs_Seq,X0) ).
cnf(u1642,axiom,
~ icext(uri_rdfs_Seq,X0) ).
cnf(u7548,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(u3085,axiom,
( icext(sK12(uri_rdf_type,X0),sK11(uri_rdf_type,X0))
| iext(uri_rdfs_range,uri_rdf_type,X0) ) ).
cnf(u7515,axiom,
( icext(sK9(uri_owl_complementOf,X0),sK9(X1,sK10(uri_owl_complementOf,X0)))
| iext(uri_rdfs_domain,uri_owl_complementOf,X0)
| iext(uri_rdfs_domain,X1,sK10(uri_owl_complementOf,X0)) ) ).
cnf(u7398,axiom,
iext(uri_rdfs_domain,uri_rdf_predicate,X0) ).
cnf(u7295,axiom,
iext(uri_owl_intersectionOf,uri_rdf_XMLLiteral,uri_rdf_nil) ).
cnf(u4298,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_owl_complementOf,uri_rdfs_Statement))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u7403,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Datatype),X0) ).
cnf(u4344,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdfs_Statement),X0,X1) ).
cnf(u3089,axiom,
iext(uri_rdfs_range,uri_rdf_List,X0) ).
cnf(u2696,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,X0) ).
cnf(u3091,axiom,
( icext(uri_owl_Restriction,sK11(uri_owl_someValuesFrom,X0))
| iext(uri_rdfs_range,uri_owl_someValuesFrom,X0) ) ).
cnf(u5519,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty) ).
cnf(u5764,axiom,
iext(uri_rdfs_member,sK9(uri_rdf_value,uri_owl_Nothing),sK10(uri_rdf_value,uri_owl_Nothing)) ).
cnf(u3237,axiom,
( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| icext(X4,sK6(X0,X2,X4))
| icext(X2,sK6(X0,X2,X4))
| icext(X0,sK6(X0,X2,X4))
| iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u5537,axiom,
( icext(sK11(uri_owl_complementOf,X0),sK13(X1,sK12(uri_owl_complementOf,X0)))
| iext(uri_rdfs_range,uri_owl_complementOf,X0)
| iext(uri_rdfs_subClassOf,X1,sK12(uri_owl_complementOf,X0)) ) ).
cnf(u3100,axiom,
iext(uri_rdfs_range,uri_rdf__3,X0) ).
cnf(u2974,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u2812,axiom,
iext(uri_rdfs_subClassOf,uri_owl_DatatypeProperty,X0) ).
cnf(u277,axiom,
~ icext(uri_owl_Nothing,X0) ).
cnf(u3208,axiom,
( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| icext(X4,sK2(X0,X2,X4))
| icext(X0,sK2(X0,X2,X4))
| iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u407,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty) ).
cnf(u300,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_OntologyProperty)
| ioxp(X0) ) ).
cnf(u5771,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_member) ).
cnf(u2699,axiom,
iext(uri_rdfs_range,X0,uri_rdf_Property) ).
cnf(u3104,axiom,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,X0) ).
cnf(u5674,axiom,
iext(uri_rdfs_member,uri_rdf__1,X0) ).
cnf(u4736,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdfs_Datatype),X0) ).
cnf(u4142,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing),X0) ).
cnf(u405,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty) ).
cnf(u5520,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_ContainerMembershipProperty) ).
cnf(u3243,axiom,
( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| icext(X6,sK3(X0,X2,X4,X6))
| icext(X0,sK3(X0,X2,X4,X6))
| iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u5558,axiom,
iext(uri_rdfs_member,sK9(uri_owl_intersectionOf,uri_owl_Nothing),sK10(uri_owl_intersectionOf,uri_owl_Nothing)) ).
cnf(u4285,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_rdfs_Statement))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u7356,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),X0) ).
cnf(u4665,axiom,
icext(uri_rdfs_Datatype,X0) ).
cnf(u5724,axiom,
iext(uri_rdfs_member,uri_owl_Nothing,X0) ).
cnf(u2973,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u2968,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_AnnotationProperty)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u5556,axiom,
iext(uri_rdfs_member,sK9(uri_owl_complementOf,uri_owl_Nothing),uri_rdf_nil) ).
cnf(u6846,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(u5957,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(u5046,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdf_Alt),X0) ).
cnf(u445,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,X1)
| ~ iext(uri_rdfs_subPropertyOf,X1,X2)
| iext(uri_rdfs_subPropertyOf,X0,X2) ) ).
cnf(u5560,axiom,
iext(uri_rdfs_member,sK9(uri_rdf_rest,uri_owl_Nothing),sK10(uri_rdf_rest,uri_owl_Nothing)) ).
cnf(u5594,axiom,
( iext(uri_rdfs_member,sK13(uri_owl_Ontology,X0),uri_owl_Ontology)
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ) ).
cnf(u5311,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdf_Bag),X0) ).
cnf(u7222,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(u7659,axiom,
( ~ icext(sK10(uri_owl_complementOf,X0),sK13(X1,sK10(uri_owl_complementOf,X0)))
| iext(uri_rdfs_subClassOf,X1,sK10(uri_owl_complementOf,X0))
| iext(uri_rdfs_domain,uri_owl_complementOf,X0) ) ).
cnf(u2901,axiom,
icext(sK9(uri_owl_complementOf,uri_owl_Nothing),X0) ).
cnf(u5596,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_Resource,uri_owl_Nothing),sK10(uri_rdfs_Resource,uri_owl_Nothing)) ).
cnf(u6870,axiom,
~ icext(sK9(uri_owl_complementOf,uri_rdfs_Seq),X0) ).
cnf(u7494,axiom,
iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_owl_Restriction) ).
cnf(u2914,axiom,
iext(uri_owl_intersectionOf,sK9(uri_owl_complementOf,uri_owl_Nothing),uri_rdf_nil) ).
cnf(u347,axiom,
( ~ icext(X1,sK13(X0,X1))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u3418,axiom,
( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| icext(X2,sK3(X0,X2,X4,X6))
| icext(X0,sK3(X0,X2,X4,X6))
| iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u3173,axiom,
iext(uri_rdfs_subPropertyOf,sK4(uri_rdf_Property),X0) ).
cnf(u1623,axiom,
~ iext(uri_rdf_predicate,X0,X1) ).
cnf(u3154,axiom,
iext(uri_rdfs_subPropertyOf,uri_owl_hasValue,X0) ).
cnf(u368,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property) ).
cnf(u7381,axiom,
iext(uri_rdfs_domain,uri_rdf_List,X0) ).
cnf(u5735,axiom,
iext(uri_rdfs_member,X0,X0) ).
cnf(u5706,axiom,
iext(uri_rdfs_member,X0,uri_rdf_Bag) ).
cnf(u4956,axiom,
icext(uri_rdfs_Container,X0) ).
cnf(u3167,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf_object,X0) ).
cnf(u7544,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(u3030,axiom,
~ icext(sK9(uri_rdfs_subClassOf,uri_owl_Nothing),X0) ).
cnf(u7394,axiom,
iext(uri_rdfs_domain,uri_rdf_subject,X0) ).
cnf(u5673,axiom,
iext(uri_rdfs_member,uri_owl_onProperty,X0) ).
cnf(u7405,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_List),X0) ).
cnf(u247,axiom,
( ~ iext(uri_owl_unionOf,X0,uri_rdf_nil)
| ~ icext(X0,X1) ) ).
cnf(u257,axiom,
( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| ~ icext(X4,X5)
| icext(X0,X5)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u372,axiom,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property) ).
cnf(u7414,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Seq),X0) ).
cnf(u5871,axiom,
( icext(sK14(uri_owl_complementOf,X0),sK9(X1,sK15(uri_owl_complementOf,X0)))
| iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
| iext(uri_rdfs_domain,X1,sK15(uri_owl_complementOf,X0)) ) ).
cnf(u7409,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_Bag),X0) ).
cnf(u7396,axiom,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,X0) ).
cnf(u2721,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Literal) ).
cnf(u7418,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_subPropertyOf,uri_rdfs_Statement),X0) ).
cnf(u3102,axiom,
iext(uri_rdfs_range,uri_rdf_subject,X0) ).
cnf(u5669,axiom,
iext(uri_rdfs_member,uri_rdfs_Class,X0) ).
cnf(u3095,axiom,
( ~ icext(sK11(uri_rdfs_subClassOf,X0),X1)
| icext(sK12(uri_rdfs_subClassOf,X0),X1)
| iext(uri_rdfs_range,uri_rdfs_subClassOf,X0) ) ).
cnf(u1561,axiom,
iext(uri_owl_unionOf,uri_owl_Nothing,uri_rdf_nil) ).
cnf(u7044,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_rdfs_Seq),sK10(uri_rdfs_subPropertyOf,uri_rdfs_Seq)) ).
cnf(u2958,axiom,
( ix(sK13(uri_owl_Ontology,X0))
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ) ).
cnf(u2813,axiom,
~ icext(uri_owl_AnnotationProperty,X0) ).
cnf(u3099,axiom,
iext(uri_rdfs_range,uri_rdf__2,X0) ).
cnf(u7420,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(u2440,axiom,
~ iext(uri_rdfs_isDefinedBy,X0,X1) ).
cnf(u2969,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_DatatypeProperty)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u5974,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(u1921,axiom,
icext(uri_rdfs_Class,X0) ).
cnf(u2590,axiom,
~ iext(sK4(uri_rdf_Property),X0,X1) ).
cnf(u5695,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdf_Bag),X0) ).
cnf(u7555,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(u4415,axiom,
~ iext(sK9(uri_rdfs_subPropertyOf,uri_rdfs_Statement),X0,X1) ).
cnf(u6047,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u4769,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdfs_Datatype),X0) ).
cnf(u337,axiom,
( ~ icext(X1,sK9(X0,X1))
| ~ ic(X1)
| ~ ip(X0)
| iext(uri_rdfs_domain,X0,X1) ) ).
cnf(u1435,axiom,
( ~ iext(uri_owl_intersectionOf,X0,uri_rdf_nil)
| icext(X0,X1) ) ).
cnf(u3495,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdf_List) ).
cnf(u5790,axiom,
( ~ icext(sK14(uri_owl_complementOf,X0),sK13(sK15(uri_owl_complementOf,X0),X1))
| iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
| iext(uri_rdfs_subClassOf,sK15(uri_owl_complementOf,X0),X1) ) ).
cnf(u7550,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(u6725,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdf_List),X0) ).
cnf(u2470,axiom,
( iext(X0,sK11(X0,X1),sK12(X0,X1))
| iext(uri_rdfs_range,X0,X1) ) ).
cnf(u2970,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_OntologyProperty)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u2976,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK10(uri_owl_complementOf,uri_owl_Nothing))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u7496,axiom,
iext(uri_rdfs_member,uri_owl_someValuesFrom,uri_owl_Restriction) ).
cnf(u353,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,X1)
| iext(X1,X2,X3)
| ~ iext(X0,X2,X3) ) ).
cnf(u6041,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(u7223,axiom,
( iext(uri_rdfs_member,X0,sK12(uri_rdfs_subClassOf,X1))
| iext(uri_rdfs_range,uri_rdfs_subClassOf,X1)
| ~ iext(uri_rdfs_subClassOf,X0,sK11(uri_rdfs_subClassOf,X1)) ) ).
cnf(u2411,axiom,
( icext(X0,sK4(X0))
| iext(uri_owl_unionOf,X0,uri_rdf_nil) ) ).
cnf(u964,axiom,
icext(uri_owl_Thing,X0) ).
cnf(u331,axiom,
( ~ iext(uri_owl_someValuesFrom,X0,X1)
| icext(uri_owl_Restriction,X0) ) ).
cnf(u4967,axiom,
iext(uri_rdfs_domain,X0,uri_rdf_Alt) ).
cnf(u4297,axiom,
iext(uri_rdfs_subClassOf,sK9(uri_owl_complementOf,uri_rdfs_Statement),X0) ).
cnf(u7417,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Statement),X0) ).
cnf(u3157,axiom,
( icext(uri_owl_Restriction,sK14(uri_owl_someValuesFrom,X0))
| iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0) ) ).
cnf(u7514,axiom,
( icext(sK9(uri_owl_complementOf,X0),sK12(X1,sK10(uri_owl_complementOf,X0)))
| iext(uri_rdfs_domain,uri_owl_complementOf,X0)
| iext(uri_rdfs_range,X1,sK10(uri_owl_complementOf,X0)) ) ).
cnf(u5599,axiom,
iext(uri_rdfs_member,X0,uri_owl_Thing) ).
cnf(u5683,axiom,
iext(uri_rdfs_member,sK4(uri_rdf_Property),X0) ).
cnf(u5597,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_Literal,uri_owl_Nothing),sK10(uri_rdfs_Literal,uri_owl_Nothing)) ).
cnf(u5709,axiom,
iext(uri_rdfs_member,X0,sK10(uri_owl_complementOf,uri_rdfs_Statement)) ).
cnf(u370,axiom,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property) ).
cnf(u3161,axiom,
( ~ icext(sK14(uri_rdfs_subClassOf,X0),X1)
| icext(sK15(uri_rdfs_subClassOf,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0) ) ).
cnf(u7407,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdf_Alt),X0) ).
cnf(u5670,axiom,
iext(uri_rdfs_member,uri_owl_allValuesFrom,X0) ).
cnf(u5696,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdfs_Statement),X0) ).
cnf(u3151,axiom,
( icext(sK15(uri_rdf_type,X0),sK14(uri_rdf_type,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0) ) ).
cnf(u7397,axiom,
iext(uri_rdfs_domain,uri_rdfs_seeAlso,X0) ).
cnf(u7385,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(u7520,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(u369,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property) ).
cnf(u4695,axiom,
idc(X0) ).
cnf(u7513,axiom,
( icext(sK9(uri_owl_complementOf,X0),sK13(X1,sK10(uri_owl_complementOf,X0)))
| iext(uri_rdfs_domain,uri_owl_complementOf,X0)
| iext(uri_rdfs_subClassOf,X1,sK10(uri_owl_complementOf,X0)) ) ).
cnf(u3172,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,X0) ).
cnf(u5595,axiom,
iext(uri_rdfs_member,sK9(uri_rdf_Property,uri_owl_Nothing),sK10(uri_rdf_Property,uri_owl_Nothing)) ).
cnf(u4488,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_owl_Nothing),X0) ).
cnf(u4976,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container) ).
cnf(u7391,axiom,
iext(uri_rdfs_domain,uri_rdf__2,X0) ).
cnf(u6515,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdf_List),X0) ).
cnf(u7421,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(u375,axiom,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property) ).
cnf(u4978,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Container) ).
cnf(u2820,axiom,
icext(uri_owl_Ontology,sK4(uri_owl_Ontology)) ).
cnf(u3086,axiom,
iext(uri_rdfs_range,uri_rdfs_Class,X0) ).
cnf(u7542,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(u5959,axiom,
( icext(sK12(uri_rdfs_domain,X0),sK9(sK11(uri_rdfs_domain,X0),uri_rdfs_Statement))
| iext(uri_rdfs_range,uri_rdfs_domain,X0)
| iext(uri_rdfs_domain,sK11(uri_rdfs_domain,X0),uri_rdfs_Statement) ) ).
cnf(u3079,axiom,
( icext(sK12(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_range,uri_owl_complementOf,X0)
| icext(sK11(uri_owl_complementOf,X0),X1) ) ).
cnf(u7412,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u2427,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class) ).
cnf(u4326,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdfs_Statement),X0) ).
cnf(u7415,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),X0) ).
cnf(u268,axiom,
( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| ~ icext(X2,X7)
| icext(X0,X7)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u7416,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Statement),X0) ).
cnf(u4487,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_owl_Nothing),X0) ).
cnf(u7521,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(u2574,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,uri_owl_Nothing)
| iext(uri_rdfs_subClassOf,X1,X0) ) ).
cnf(u7380,axiom,
iext(uri_rdfs_domain,uri_owl_hasValue,X0) ).
cnf(u258,axiom,
( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| ~ icext(X2,X5)
| icext(X0,X5)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u3457,axiom,
icext(uri_rdf_List,X0) ).
cnf(u7384,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(u6812,axiom,
iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,uri_rdfs_Seq),X0) ).
cnf(u6004,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X0,X1) ).
cnf(u6923,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdfs_Seq),X0) ).
cnf(u285,axiom,
( iext(uri_rdf_type,X0,uri_rdfs_Class)
| ~ ic(X0) ) ).
cnf(u7312,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(u4767,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdfs_Datatype),X0,X1) ).
cnf(u386,axiom,
( iext(uri_rdf_type,X0,X1)
| ~ icext(X1,X0) ) ).
cnf(u7300,axiom,
iext(uri_rdfs_member,X0,uri_rdf_XMLLiteral) ).
cnf(u5014,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdf_Alt),X0) ).
cnf(u5555,axiom,
iext(uri_rdfs_member,uri_rdfs_ContainerMembershipProperty,uri_rdf_nil) ).
cnf(u7616,axiom,
( iext(uri_rdfs_subClassOf,sK15(uri_owl_complementOf,X0),sK15(uri_owl_complementOf,X0))
| iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0) ) ).
cnf(u298,axiom,
( ~ ioxp(X0)
| ~ iext(X0,X1,X2)
| ix(X1) ) ).
cnf(u2954,axiom,
( iext(X0,sK14(X0,X1),sK15(X0,X1))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u2726,axiom,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,X0) ).
cnf(u5279,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdf_Bag),X0) ).
cnf(u7595,axiom,
( ~ icext(sK10(uri_owl_complementOf,X0),sK0(sK10(uri_owl_complementOf,X0)))
| iext(uri_owl_intersectionOf,sK10(uri_owl_complementOf,X0),uri_rdf_nil)
| iext(uri_rdfs_domain,uri_owl_complementOf,X0) ) ).
cnf(u5309,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdf_Bag),X0,X1) ).
cnf(u296,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_DatatypeProperty)
| iodp(X0) ) ).
cnf(u6807,axiom,
~ icext(sK9(uri_rdfs_subClassOf,uri_rdfs_Seq),X0) ).
cnf(u6040,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(u4138,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdf_List),X0) ).
cnf(u5545,axiom,
iext(uri_rdfs_member,uri_owl_Thing,uri_rdf_nil) ).
cnf(u3217,axiom,
( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| icext(X2,sK2(X0,X2,X4))
| icext(X0,sK2(X0,X2,X4))
| iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u5549,axiom,
iext(uri_rdfs_member,uri_rdfs_Resource,uri_rdf_nil) ).
cnf(u5047,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdf_Alt),X0) ).
cnf(u2450,axiom,
icext(uri_rdf_Property,X0) ).
cnf(u2720,axiom,
iext(uri_rdfs_domain,X0,uri_rdf_Property) ).
cnf(u5553,axiom,
iext(uri_rdfs_member,uri_rdfs_Container,uri_rdf_nil) ).
cnf(u6813,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_rdfs_Seq))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u5539,axiom,
( icext(sK11(uri_owl_complementOf,X0),sK9(X1,sK12(uri_owl_complementOf,X0)))
| iext(uri_rdfs_range,uri_owl_complementOf,X0)
| iext(uri_rdfs_domain,X1,sK12(uri_owl_complementOf,X0)) ) ).
cnf(u7349,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),X0) ).
cnf(u3078,axiom,
( ~ icext(sK12(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_range,uri_owl_complementOf,X0)
| ~ icext(sK11(uri_owl_complementOf,X0),X1) ) ).
cnf(u3163,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(u5691,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subPropertyOf,uri_rdfs_Statement),X0) ).
cnf(u4416,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_subPropertyOf,uri_rdfs_Statement),X0) ).
cnf(u4264,axiom,
iext(uri_rdfs_range,X0,sK10(uri_owl_complementOf,uri_rdfs_Statement)) ).
cnf(u5559,axiom,
iext(uri_rdfs_member,sK9(uri_rdf_first,uri_owl_Nothing),sK10(uri_rdf_first,uri_owl_Nothing)) ).
cnf(u5869,axiom,
( icext(sK14(uri_owl_complementOf,X0),sK13(X1,sK15(uri_owl_complementOf,X0)))
| iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
| iext(uri_rdfs_subClassOf,X1,sK15(uri_owl_complementOf,X0)) ) ).
cnf(u1870,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Literal,uri_rdf_nil) ).
cnf(u336,axiom,
( ~ ic(X1)
| iext(X0,sK9(X0,X1),sK10(X0,X1))
| ~ ip(X0)
| iext(uri_rdfs_domain,X0,X1) ) ).
cnf(u5703,axiom,
iext(uri_rdfs_member,X0,uri_rdf_List) ).
cnf(u3145,axiom,
( icext(sK15(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
| icext(sK14(uri_owl_complementOf,X0),X1) ) ).
cnf(u7243,axiom,
icext(uri_rdf_XMLLiteral,X0) ).
cnf(u5960,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(u1874,axiom,
iext(uri_owl_intersectionOf,uri_owl_Thing,uri_rdf_nil) ).
cnf(u7419,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(u342,axiom,
( ~ icext(X1,sK12(X0,X1))
| ~ ip(X1)
| ~ ip(X0)
| iext(uri_rdfs_range,X0,X1) ) ).
cnf(u3165,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf__2,X0) ).
cnf(u7512,axiom,
( icext(sK9(uri_owl_complementOf,X0),sK0(sK10(uri_owl_complementOf,X0)))
| iext(uri_rdfs_domain,uri_owl_complementOf,X0)
| iext(uri_owl_intersectionOf,sK10(uri_owl_complementOf,X0),uri_rdf_nil) ) ).
cnf(u2895,axiom,
~ icext(sK10(uri_owl_complementOf,uri_owl_Nothing),X0) ).
cnf(u5571,axiom,
iext(uri_rdfs_member,sK9(uri_owl_unionOf,uri_owl_Nothing),sK10(uri_owl_unionOf,uri_owl_Nothing)) ).
cnf(u6048,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u7373,axiom,
( iext(X0,sK9(X0,X1),sK10(X0,X1))
| iext(uri_rdfs_domain,X0,X1) ) ).
cnf(u5870,axiom,
( icext(sK14(uri_owl_complementOf,X0),sK12(X1,sK15(uri_owl_complementOf,X0)))
| iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
| iext(uri_rdfs_range,X1,sK15(uri_owl_complementOf,X0)) ) ).
cnf(u3169,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,X0) ).
cnf(u6922,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdfs_Seq),X0,X1) ).
cnf(u6337,axiom,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
| iext(uri_rdfs_subPropertyOf,X1,X0) ) ).
cnf(u3156,axiom,
iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0) ).
cnf(u7382,axiom,
iext(uri_rdfs_domain,uri_owl_onProperty,X0) ).
cnf(u5886,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(u3171,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,X0) ).
cnf(u7519,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(u3160,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(u5474,axiom,
icext(uri_rdfs_ContainerMembershipProperty,X0) ).
cnf(u5598,axiom,
iext(uri_rdfs_member,sK9(uri_owl_someValuesFrom,uri_owl_Nothing),sK10(uri_owl_someValuesFrom,uri_owl_Nothing)) ).
cnf(u4325,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdfs_Statement),X0) ).
cnf(u3158,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(u7406,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_List),X0) ).
cnf(u7411,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u5765,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_label,uri_owl_Nothing),sK10(uri_rdfs_label,uri_owl_Nothing)) ).
cnf(u7523,axiom,
( iext(uri_rdfs_member,X0,sK15(uri_rdfs_subClassOf,X1))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X1)
| ~ iext(uri_rdfs_subClassOf,X0,sK14(uri_rdfs_subClassOf,X1)) ) ).
cnf(u6005,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u3184,axiom,
( ~ icext(sK15(X0,uri_rdf_type),sK14(X0,uri_rdf_type))
| iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type) ) ).
cnf(u7399,axiom,
iext(uri_rdfs_domain,sK4(uri_rdf_Property),X0) ).
cnf(u4058,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdf_List),X0,X1) ).
cnf(u6123,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(u253,axiom,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| icext(X2,X3)
| ~ icext(X0,X3)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u4966,axiom,
iext(uri_rdfs_range,X0,uri_rdf_Alt) ).
cnf(u7302,axiom,
iext(uri_rdfs_member,uri_rdf_XMLLiteral,uri_rdf_nil) ).
cnf(u7392,axiom,
iext(uri_rdfs_domain,uri_rdf__3,X0) ).
cnf(u7543,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(u228,axiom,
( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| ~ icext(X4,X5)
| ~ icext(X2,X5)
| icext(X0,X5)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u7379,axiom,
iext(uri_rdfs_domain,uri_owl_allValuesFrom,X0) ).
cnf(u4737,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdfs_Datatype),X0) ).
cnf(u4492,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_owl_Nothing),X0) ).
cnf(u4977,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Container) ).
cnf(u3053,axiom,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ icext(X2,sK1(X0,X2))
| ~ icext(X0,sK1(X0,X2))
| iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u2692,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Resource) ).
cnf(u2582,axiom,
~ iext(uri_owl_hasValue,X0,X1) ).
cnf(u3051,axiom,
( icext(uri_owl_Ontology,sK13(uri_owl_Ontology,X0))
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ) ).
cnf(u5705,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_Container) ).
cnf(u7297,axiom,
iext(uri_rdfs_range,X0,uri_rdf_XMLLiteral) ).
cnf(u6821,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subClassOf,uri_rdfs_Seq),X0) ).
cnf(u4139,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdf_List),X0) ).
cnf(u5732,axiom,
iext(uri_rdfs_member,sK9(uri_owl_complementOf,uri_rdfs_Statement),X0) ).
cnf(u387,axiom,
( ~ iext(uri_rdf_type,X0,X1)
| icext(X1,X0) ) ).
cnf(u410,axiom,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype) ).
cnf(u5510,axiom,
( ~ iext(X0,X1,X2)
| iext(uri_rdfs_member,X1,X2) ) ).
cnf(u5548,axiom,
iext(uri_rdfs_member,uri_rdf_Property,uri_rdf_nil) ).
cnf(u2697,axiom,
iext(uri_rdfs_domain,X0,uri_owl_Thing) ).
cnf(u2576,axiom,
~ iext(uri_owl_onProperty,X0,X1) ).
cnf(u4265,axiom,
iext(uri_rdfs_domain,X0,sK10(uri_owl_complementOf,uri_rdfs_Statement)) ).
cnf(u2698,axiom,
iext(uri_rdfs_range,X0,uri_owl_Thing) ).
cnf(u5310,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdf_Bag),X0) ).
cnf(u3494,axiom,
iext(uri_owl_intersectionOf,uri_rdf_List,uri_rdf_nil) ).
cnf(u6924,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdfs_Seq),X0) ).
cnf(u3106,axiom,
iext(uri_rdfs_range,uri_rdf_predicate,X0) ).
cnf(u297,axiom,
( ~ ioxp(X0)
| ~ iext(X0,X1,X2)
| ix(X2) ) ).
cnf(u5677,axiom,
iext(uri_rdfs_member,uri_rdf_object,X0) ).
cnf(u6858,axiom,
iext(uri_rdfs_subClassOf,X0,sK10(uri_owl_complementOf,uri_rdfs_Seq)) ).
cnf(u6847,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(u3234,axiom,
( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| ~ icext(X4,sK2(X0,X2,X4))
| ~ icext(X2,sK2(X0,X2,X4))
| ~ icext(X0,sK2(X0,X2,X4))
| iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u5681,axiom,
iext(uri_rdfs_member,uri_rdfs_seeAlso,X0) ).
cnf(u1595,axiom,
iext(uri_rdf_type,X0,uri_rdfs_Literal) ).
cnf(u581,axiom,
icext(uri_rdfs_Resource,X0) ).
cnf(u7390,axiom,
iext(uri_rdfs_domain,uri_rdf__1,X0) ).
cnf(u2482,axiom,
~ iext(uri_rdf__1,X0,X1) ).
cnf(u3247,axiom,
( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| icext(X4,sK3(X0,X2,X4,X6))
| icext(X0,sK3(X0,X2,X4,X6))
| iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u5868,axiom,
( icext(sK14(uri_owl_complementOf,X0),sK0(sK15(uri_owl_complementOf,X0)))
| iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
| iext(uri_owl_intersectionOf,sK15(uri_owl_complementOf,X0),uri_rdf_nil) ) ).
cnf(u1864,axiom,
( ~ icext(X0,sK0(X0))
| ~ ic(X0)
| iext(uri_owl_intersectionOf,X0,uri_rdf_nil) ) ).
cnf(u5550,axiom,
iext(uri_rdfs_member,uri_rdfs_Literal,uri_rdf_nil) ).
cnf(u338,axiom,
( ~ iext(uri_rdfs_domain,X0,X1)
| icext(X1,X2)
| ~ iext(X0,X2,X3) ) ).
cnf(u7375,axiom,
( ~ icext(sK9(uri_owl_complementOf,X0),X1)
| ~ icext(sK10(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_domain,uri_owl_complementOf,X0) ) ).
cnf(u5575,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_Resource) ).
cnf(u3153,axiom,
iext(uri_rdfs_subPropertyOf,uri_owl_allValuesFrom,X0) ).
cnf(u5554,axiom,
iext(uri_rdfs_member,uri_rdf_Bag,uri_rdf_nil) ).
cnf(u5700,axiom,
iext(uri_rdfs_member,X0,uri_rdf_Property) ).
cnf(u5785,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(u3155,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf_List,X0) ).
cnf(u5726,axiom,
iext(uri_rdfs_member,uri_owl_DatatypeProperty,X0) ).
cnf(u4965,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt) ).
cnf(u3144,axiom,
( ~ icext(sK15(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
| ~ icext(sK14(uri_owl_complementOf,X0),X1) ) ).
cnf(u343,axiom,
( ~ iext(uri_rdfs_range,X0,X1)
| icext(X1,X3)
| ~ iext(X0,X2,X3) ) ).
cnf(u2916,axiom,
iext(uri_rdfs_range,X0,sK9(uri_owl_complementOf,uri_owl_Nothing)) ).
cnf(u3092,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(u1624,axiom,
~ iext(uri_rdf_subject,X0,X1) ).
cnf(u5730,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subClassOf,uri_owl_Nothing),X0) ).
cnf(u3164,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf__1,X0) ).
cnf(u4294,axiom,
iext(uri_owl_unionOf,sK9(uri_owl_complementOf,uri_rdfs_Statement),uri_rdf_nil) ).
cnf(u7383,axiom,
( icext(uri_owl_Restriction,sK9(uri_owl_someValuesFrom,X0))
| iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0) ) ).
cnf(u364,axiom,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property) ).
cnf(u6860,axiom,
iext(uri_rdfs_domain,X0,sK10(uri_owl_complementOf,uri_rdfs_Seq)) ).
cnf(u3168,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf_subject,X0) ).
cnf(u3049,axiom,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| icext(X2,sK1(X0,X2))
| icext(X0,sK1(X0,X2))
| iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u5469,axiom,
( ~ icext(sK11(uri_owl_complementOf,X0),sK13(sK12(uri_owl_complementOf,X0),X1))
| iext(uri_rdfs_range,uri_owl_complementOf,X0)
| iext(uri_rdfs_subClassOf,sK12(uri_owl_complementOf,X0),X1) ) ).
cnf(u237,axiom,
( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| icext(X2,X7)
| ~ icext(X0,X7)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u4735,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdfs_Datatype),X0,X1) ).
cnf(u7404,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdfs_Datatype),X0) ).
cnf(u212,axiom,
( ~ iext(uri_owl_complementOf,X0,X1)
| ~ icext(X1,X2)
| ~ icext(X0,X2) ) ).
cnf(u227,axiom,
( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| icext(X2,X5)
| ~ icext(X0,X5)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u2798,axiom,
iext(uri_rdf_type,sK4(uri_owl_Ontology),uri_owl_Ontology) ).
cnf(u7408,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_Alt),X0) ).
cnf(u2055,axiom,
( ~ ip(X0)
| iext(X0,sK9(X0,uri_owl_Nothing),sK10(X0,uri_owl_Nothing))
| iext(uri_rdfs_domain,X0,uri_owl_Nothing) ) ).
cnf(u4975,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Container,uri_rdf_nil) ).
cnf(u4219,axiom,
~ icext(sK9(uri_rdfs_subClassOf,uri_rdfs_Statement),X0) ).
cnf(u7516,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(u2693,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Class) ).
cnf(u3035,axiom,
iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,uri_owl_Nothing),X0) ).
cnf(u5247,axiom,
iext(uri_rdfs_range,X0,uri_rdf_Bag) ).
cnf(u371,axiom,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property) ).
cnf(u266,axiom,
( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| ~ icext(X6,X7)
| icext(X0,X7)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u252,axiom,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ icext(X2,X3)
| icext(X0,X3)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u2694,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Class) ).
cnf(u5729,axiom,
iext(uri_rdfs_member,uri_rdfs_Statement,X0) ).
cnf(u2700,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Literal) ).
cnf(u5277,axiom,
~ iext(sK9(uri_rdfs_range,uri_rdf_Bag),X0,X1) ).
cnf(u5731,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subClassOf,uri_rdfs_Statement),X0) ).
cnf(u7422,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(u4345,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdfs_Statement),X0) ).
cnf(u5686,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdf_List),X0) ).
cnf(u267,axiom,
( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| ~ icext(X4,X7)
| icext(X0,X7)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u7296,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral) ).
cnf(u2695,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Statement,X0) ).
cnf(u1926,axiom,
ic(X0) ).
cnf(u5015,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdf_Alt),X0) ).
cnf(u5542,axiom,
( iext(uri_rdfs_member,sK9(X0,uri_rdfs_Statement),sK10(X0,uri_rdfs_Statement))
| iext(uri_rdfs_domain,X0,uri_rdfs_Statement) ) ).
cnf(u226,axiom,
( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| icext(X4,X5)
| ~ icext(X0,X5)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u2578,axiom,
~ iext(uri_rdf_List,X0,X1) ).
cnf(u3090,axiom,
iext(uri_rdfs_range,uri_owl_onProperty,X0) ).
cnf(u305,axiom,
( iext(uri_rdf_type,X0,uri_rdf_Property)
| ~ ip(X0) ) ).
cnf(u7500,axiom,
( ~ icext(sK10(uri_owl_complementOf,X0),sK4(sK9(uri_owl_complementOf,X0)))
| iext(uri_rdfs_domain,uri_owl_complementOf,X0)
| iext(uri_owl_unionOf,sK9(uri_owl_complementOf,X0),uri_rdf_nil) ) ).
cnf(u7584,axiom,
( iext(uri_rdfs_subClassOf,sK12(uri_owl_complementOf,X0),sK12(uri_owl_complementOf,X0))
| iext(uri_rdfs_range,uri_owl_complementOf,X0) ) ).
cnf(u2453,axiom,
ip(X0) ).
cnf(u4255,axiom,
icext(sK10(uri_owl_complementOf,uri_rdfs_Statement),X0) ).
cnf(u6929,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdfs_Seq),X0) ).
cnf(u6865,axiom,
iext(uri_rdfs_member,X0,sK10(uri_owl_complementOf,uri_rdfs_Seq)) ).
cnf(u5541,axiom,
( iext(uri_rdfs_member,sK14(X0,X1),sK15(X0,X1))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u3103,axiom,
iext(uri_rdfs_range,uri_rdfs_comment,X0) ).
cnf(u5676,axiom,
iext(uri_rdfs_member,uri_rdf__3,X0) ).
cnf(u310,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_Ontology)
| ix(X0) ) ).
cnf(u5693,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdfs_Datatype),X0) ).
cnf(u5679,axiom,
iext(uri_rdfs_member,uri_rdfs_comment,X0) ).
cnf(u2466,axiom,
~ iext(uri_rdf__3,X0,X1) ).
cnf(u1585,axiom,
~ icext(uri_rdfs_Statement,X0) ).
cnf(u6078,axiom,
( iext(X0,sK9(X0,uri_rdfs_Seq),sK10(X0,uri_rdfs_Seq))
| iext(uri_rdfs_domain,X0,uri_rdfs_Seq) ) ).
cnf(u5787,axiom,
( ~ icext(sK14(uri_owl_complementOf,X0),sK4(sK15(uri_owl_complementOf,X0)))
| iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
| iext(uri_owl_unionOf,sK15(uri_owl_complementOf,X0),uri_rdf_nil) ) ).
cnf(u5678,axiom,
iext(uri_rdfs_member,uri_rdf_subject,X0) ).
cnf(u3496,axiom,
iext(uri_rdfs_range,X0,uri_rdf_List) ).
cnf(u6975,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdfs_Seq),X0) ).
cnf(u438,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| ~ iext(uri_rdfs_subClassOf,X0,X1)
| iext(uri_rdfs_subClassOf,X0,X2) ) ).
cnf(u5682,axiom,
iext(uri_rdfs_member,uri_rdf_predicate,X0) ).
cnf(u5045,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdf_Alt),X0,X1) ).
cnf(u2490,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource) ).
cnf(u5687,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdf_Alt),X0) ).
cnf(u3036,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,uri_owl_Nothing))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u2619,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal) ).
cnf(u6850,axiom,
( icext(sK15(uri_rdfs_range,X0),sK10(sK14(uri_rdfs_range,X0),uri_rdfs_Seq))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0)
| iext(uri_rdfs_domain,sK14(uri_rdfs_range,X0),uri_rdfs_Seq) ) ).
cnf(u6042,axiom,
( icext(sK15(uri_rdfs_domain,X0),sK9(sK14(uri_rdfs_domain,X0),uri_rdfs_Statement))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0)
| iext(uri_rdfs_domain,sK14(uri_rdfs_domain,X0),uri_rdfs_Statement) ) ).
cnf(u6980,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdfs_Seq),X0) ).
cnf(u3088,axiom,
iext(uri_rdfs_range,uri_owl_hasValue,X0) ).
cnf(u7395,axiom,
iext(uri_rdfs_domain,uri_rdfs_comment,X0) ).
cnf(u6052,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_domain,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u6849,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(u2900,axiom,
iext(uri_rdfs_subClassOf,sK10(uri_owl_complementOf,uri_owl_Nothing),X0) ).
cnf(u3166,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf__3,X0) ).
cnf(u5733,axiom,
iext(uri_rdfs_member,sK10(uri_owl_complementOf,uri_owl_Nothing),X0) ).
cnf(u4293,axiom,
~ icext(sK9(uri_owl_complementOf,uri_rdfs_Statement),X0) ).
cnf(u3159,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(u7374,axiom,
( iext(uri_rdfs_member,sK9(X0,X1),sK10(X0,X1))
| iext(uri_rdfs_domain,X0,X1) ) ).
cnf(u6514,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdf_List),X0) ).
cnf(u1871,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Resource,uri_rdf_nil) ).
cnf(u348,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,X1)
| icext(X1,X2)
| ~ icext(X0,X2) ) ).
cnf(u1109,axiom,
iext(uri_rdf_type,X0,uri_rdfs_Resource) ).
cnf(u3152,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_Class,X0) ).
cnf(u4705,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Datatype) ).
cnf(u6859,axiom,
iext(uri_rdfs_range,X0,sK10(uri_owl_complementOf,uri_rdfs_Seq)) ).
cnf(u367,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property) ).
cnf(u5572,axiom,
( iext(uri_rdfs_member,X0,X1)
| ~ icext(X1,X0) ) ).
cnf(u211,axiom,
( ~ iext(uri_owl_complementOf,X0,X1)
| icext(X1,X2)
| icext(X0,X2) ) ).
cnf(u365,axiom,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List) ).
cnf(u6883,axiom,
iext(uri_rdfs_member,sK9(uri_owl_complementOf,uri_rdfs_Seq),X0) ).
cnf(u238,axiom,
( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| ~ icext(X6,X7)
| ~ icext(X4,X7)
| ~ icext(X2,X7)
| icext(X0,X7)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u6500,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdf_List),X0,X1) ).
cnf(u2472,axiom,
~ iext(uri_rdfs_Class,X0,X1) ).
cnf(u3438,axiom,
( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| ~ icext(X6,sK3(X0,X2,X4,X6))
| ~ icext(X4,sK3(X0,X2,X4,X6))
| ~ icext(X2,sK3(X0,X2,X4,X6))
| ~ icext(X0,sK3(X0,X2,X4,X6))
| iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u236,axiom,
( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| icext(X4,X7)
| ~ icext(X0,X7)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u2806,axiom,
iext(uri_rdfs_subClassOf,uri_owl_OntologyProperty,X0) ).
cnf(u3162,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(u5690,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing),X0) ).
cnf(u7549,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(u3442,axiom,
( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| icext(X6,sK7(X0,X2,X4,X6))
| icext(X4,sK7(X0,X2,X4,X6))
| icext(X2,sK7(X0,X2,X4,X6))
| icext(X0,sK7(X0,X2,X4,X6))
| iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u222,axiom,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ icext(X2,X3)
| icext(X0,X3)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u5727,axiom,
iext(uri_rdfs_member,uri_owl_OntologyProperty,X0) ).
cnf(u5707,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_ContainerMembershipProperty) ).
cnf(u6844,axiom,
icext(sK10(uri_owl_complementOf,uri_rdfs_Seq),X0) ).
cnf(u7377,axiom,
( icext(sK10(uri_rdf_type,X0),sK9(uri_rdf_type,X0))
| iext(uri_rdfs_domain,uri_rdf_type,X0) ) ).
cnf(u2807,axiom,
~ icext(uri_owl_DatatypeProperty,X0) ).
cnf(u7221,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(u249,axiom,
( ~ ic(X0)
| icext(X0,sK4(X0))
| iext(uri_owl_unionOf,X0,uri_rdf_nil) ) ).
cnf(u7554,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(u6122,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(u5278,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_range,uri_rdf_Bag),X0) ).
cnf(u5704,axiom,
iext(uri_rdfs_member,X0,uri_rdf_Alt) ).
cnf(u3093,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(u7048,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_subPropertyOf,uri_rdfs_Seq),sK10(uri_rdfs_subPropertyOf,uri_rdfs_Seq)) ).
cnf(u265,axiom,
( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| icext(X6,X7)
| icext(X4,X7)
| icext(X2,X7)
| ~ icext(X0,X7)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u5248,axiom,
iext(uri_rdfs_domain,X0,uri_rdf_Bag) ).
cnf(u3097,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(u7410,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_rdf_Bag),X0) ).
cnf(u7556,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(u3094,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(u1168,axiom,
( ~ icext(uri_owl_Ontology,X0)
| ix(X0) ) ).
cnf(u2463,axiom,
( iext(X0,sK9(X0,uri_owl_Nothing),sK10(X0,uri_owl_Nothing))
| iext(uri_rdfs_domain,X0,uri_owl_Nothing) ) ).
cnf(u7401,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing),X0) ).
cnf(u3087,axiom,
iext(uri_rdfs_range,uri_owl_allValuesFrom,X0) ).
cnf(u3117,axiom,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| icext(X2,sK5(X0,X2))
| icext(X0,sK5(X0,X2))
| iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u2950,axiom,
( iext(X0,sK9(X0,uri_rdfs_Statement),sK10(X0,uri_rdfs_Statement))
| iext(uri_rdfs_domain,X0,uri_rdfs_Statement) ) ).
cnf(u7402,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_domain,uri_owl_Nothing),X0) ).
cnf(u3098,axiom,
iext(uri_rdfs_range,uri_rdf__1,X0) ).
cnf(u3225,axiom,
( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| ~ icext(X2,sK6(X0,X2,X4))
| ~ icext(X0,sK6(X0,X2,X4))
| iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u5675,axiom,
iext(uri_rdfs_member,uri_rdf__2,X0) ).
cnf(u2956,axiom,
( ~ iext(X1,sK14(X0,X1),sK15(X0,X1))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u3222,axiom,
( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| ~ icext(X4,sK6(X0,X2,X4))
| ~ icext(X0,sK6(X0,X2,X4))
| iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u2461,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdf_Property) ).
cnf(u5543,axiom,
( iext(uri_rdfs_member,sK9(X0,uri_owl_Nothing),sK10(X0,uri_owl_Nothing))
| iext(uri_rdfs_domain,X0,uri_owl_Nothing) ) ).
cnf(u2432,axiom,
~ iext(uri_rdfs_seeAlso,X0,X1) ).
cnf(u292,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_AnnotationProperty)
| ioap(X0) ) ).
cnf(u422,axiom,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class) ).
cnf(u5685,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdfs_Datatype),X0) ).
cnf(u2728,axiom,
icext(sK10(uri_rdf_type,uri_owl_Nothing),sK9(uri_rdf_type,uri_owl_Nothing)) ).
cnf(u5518,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_nil) ).
cnf(u5725,axiom,
iext(uri_rdfs_member,uri_owl_AnnotationProperty,X0) ).
cnf(u6716,axiom,
iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member) ).
cnf(u5672,axiom,
iext(uri_rdfs_member,uri_rdf_List,X0) ).
cnf(u311,axiom,
( ~ ix(X0)
| iext(uri_rdf_type,X0,uri_owl_Ontology) ) ).
cnf(u5689,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdfs_Statement),X0) ).
cnf(u1592,axiom,
lv(X0) ).
cnf(u4417,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,uri_rdfs_Statement),X0) ).
cnf(u3497,axiom,
iext(uri_rdfs_domain,X0,uri_rdf_List) ).
cnf(u7348,axiom,
~ iext(sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),X0,X1) ).
cnf(u6043,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(u7386,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(u5708,axiom,
iext(uri_rdfs_member,X0,sK9(uri_owl_complementOf,uri_owl_Nothing)) ).
cnf(u6845,axiom,
iext(uri_rdfs_member,sK10(uri_owl_complementOf,uri_rdfs_Seq),uri_rdf_nil) ).
cnf(u4768,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_rdfs_Datatype),X0) ).
cnf(u2491,axiom,
iext(uri_rdfs_subClassOf,X0,uri_owl_Thing) ).
cnf(u437,axiom,
( iext(uri_rdfs_subClassOf,X0,X0)
| ~ ic(X0) ) ).
cnf(u5552,axiom,
iext(uri_rdfs_member,uri_rdf_Alt,uri_rdf_nil) ).
cnf(u7388,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(u4924,axiom,
icext(uri_rdf_Alt,X0) ).
cnf(u4703,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Datatype,uri_rdf_nil) ).
cnf(u5466,axiom,
( ~ icext(sK11(uri_owl_complementOf,X0),sK4(sK12(uri_owl_complementOf,X0)))
| iext(uri_rdfs_range,uri_owl_complementOf,X0)
| iext(uri_owl_unionOf,sK12(uri_owl_complementOf,X0),uri_rdf_nil) ) ).
cnf(u7667,axiom,
( ~ icext(sK10(uri_owl_complementOf,X0),sK9(X1,sK10(uri_owl_complementOf,X0)))
| iext(uri_rdfs_domain,X1,sK10(uri_owl_complementOf,X0))
| iext(uri_rdfs_domain,uri_owl_complementOf,X0) ) ).
cnf(u5975,axiom,
( icext(sK12(uri_rdfs_range,X0),sK10(sK11(uri_rdfs_range,X0),uri_rdfs_Statement))
| iext(uri_rdfs_range,uri_rdfs_range,X0)
| iext(uri_rdfs_domain,sK11(uri_rdfs_range,X0),uri_rdfs_Statement) ) ).
cnf(u5973,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(u7376,axiom,
( icext(sK10(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_domain,uri_owl_complementOf,X0)
| icext(sK9(uri_owl_complementOf,X0),X1) ) ).
cnf(u7527,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(u4706,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Datatype) ).
cnf(u7350,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,uri_rdf_XMLLiteral),X0) ).
cnf(u4062,axiom,
~ iext(sK9(uri_rdfs_subPropertyOf,uri_owl_Nothing),X0,X1) ).
cnf(u5245,axiom,
iext(uri_owl_intersectionOf,uri_rdf_Bag,uri_rdf_nil) ).
cnf(u5592,axiom,
iext(uri_rdfs_member,sK4(uri_owl_Ontology),uri_owl_Ontology) ).
cnf(u7655,axiom,
( icext(sK9(uri_owl_complementOf,X0),sK13(sK9(uri_owl_complementOf,X0),X1))
| iext(uri_rdfs_subClassOf,sK9(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_domain,uri_owl_complementOf,X0) ) ).
cnf(u5671,axiom,
iext(uri_rdfs_member,uri_owl_hasValue,X0) ).
cnf(u4964,axiom,
iext(uri_owl_intersectionOf,uri_rdf_Alt,uri_rdf_nil) ).
cnf(u5976,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(u3426,axiom,
( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| ~ icext(X6,sK7(X0,X2,X4,X6))
| ~ icext(X0,sK7(X0,X2,X4,X6))
| iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u235,axiom,
( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2)
| icext(X6,X7)
| ~ icext(X0,X7)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u5600,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_Class) ).
cnf(u6871,axiom,
iext(uri_owl_unionOf,sK9(uri_owl_complementOf,uri_rdfs_Seq),uri_rdf_nil) ).
cnf(u5680,axiom,
iext(uri_rdfs_member,uri_rdfs_isDefinedBy,X0) ).
cnf(u6006,axiom,
iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u2818,axiom,
iext(uri_rdfs_subClassOf,uri_owl_AnnotationProperty,X0) ).
cnf(u3059,axiom,
iext(uri_rdfs_member,sK9(sK4(uri_rdfs_ContainerMembershipProperty),uri_owl_Nothing),sK10(sK4(uri_rdfs_ContainerMembershipProperty),uri_owl_Nothing)) ).
cnf(u366,axiom,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property) ).
cnf(u4223,axiom,
iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,uri_rdfs_Statement),X0) ).
cnf(u6010,axiom,
iext(uri_rdfs_member,sK9(uri_rdfs_range,uri_rdfs_ContainerMembershipProperty),X0) ).
cnf(u7393,axiom,
iext(uri_rdfs_domain,uri_rdf_object,X0) ).
cnf(u5699,axiom,
iext(uri_rdfs_member,X0,uri_rdfs_Datatype) ).
cnf(u7042,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(u3186,axiom,
iext(uri_rdfs_subPropertyOf,X0,X0) ).
cnf(u2801,axiom,
~ icext(uri_owl_OntologyProperty,X0) ).
cnf(u7413,axiom,
iext(uri_rdfs_domain,sK9(uri_rdfs_range,uri_rdfs_Seq),X0) ).
cnf(u4491,axiom,
iext(uri_rdfs_range,sK9(uri_rdfs_domain,uri_owl_Nothing),X0) ).
cnf(u7559,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(u1810,axiom,
( ~ icext(uri_rdfs_ContainerMembershipProperty,X2)
| ~ iext(X2,X0,X1)
| iext(uri_rdfs_member,X0,X1) ) ).
cnf(u6874,axiom,
iext(uri_rdfs_subClassOf,sK9(uri_owl_complementOf,uri_rdfs_Seq),X0) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWB004+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.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 28 06:57:22 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.39 Running first-order model finding
% 0.09/0.39 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.46/0.65 % (170751)Will run a generic schedule for satisfiability detection.
% 1.46/0.65 % (170758)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1903552085:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.46/0.65 % (170757)% WARNING: option uhcvi not known.
% 1.46/0.65 % (170756)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3210854242_2999 on theBenchmark for (2999ds/0Mi)
% 1.46/0.65 % (170759)dis+10_1_sil=32000:sp=arity:random_seed=603447264:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.46/0.65 % (170760)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1605370346:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.46/0.65 % (170761)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3116375418:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.46/0.65 % (170762)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2118034040:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.46/0.65 % (170757)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1743243506:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.46/0.65 % TRYING [1]
% 1.46/0.65 % TRYING [2]
% 1.46/0.65 % TRYING [3]
% 1.46/0.65 % (170760)Instruction limit reached!
% 1.46/0.65 % (170760)------------------------------
% 1.46/0.65 % (170760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.65 % (170760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.65 % (170760)CaDiCaL version: 2.1.3
% 1.46/0.65 % (170760)Termination reason: Instruction limit
% 1.46/0.65 % (170760)Termination phase: Saturation
% 1.46/0.65 % (170760)Time elapsed: 0.051 s
% 1.46/0.65 % (170760)Peak memory usage: 12 MB
% 1.46/0.65 % (170760)Instructions burned: 118 (million)
% 1.46/0.65 % TRYING [4]
% 1.46/0.65 % (170759)Instruction limit reached!
% 1.46/0.65 % (170759)------------------------------
% 1.46/0.65 % (170759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.65 % (170759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.65 % (170759)CaDiCaL version: 2.1.3
% 1.46/0.65 % (170759)Termination reason: Instruction limit
% 1.46/0.65 % (170759)Termination phase: Saturation
% 1.46/0.65 % (170759)Time elapsed: 0.062 s
% 1.46/0.65 % (170759)Peak memory usage: 13 MB
% 1.46/0.65 % (170759)Instructions burned: 104 (million)
% 1.46/0.65 % (170761)Instruction limit reached!
% 1.46/0.65 % (170761)------------------------------
% 1.46/0.65 % (170761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.65 % (170761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.65 % (170761)CaDiCaL version: 2.1.3
% 1.46/0.65 % (170761)Termination reason: Instruction limit
% 1.46/0.65 % (170761)Termination phase: Saturation
% 1.46/0.65 % (170761)Time elapsed: 0.069 s
% 1.46/0.65 % (170761)Peak memory usage: 13 MB
% 1.46/0.65 % (170761)Instructions burned: 131 (million)
% 1.46/0.65 % (170770)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2436499045:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.46/0.65 % (170771)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3042778723:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.46/0.65 % TRYING [1]
% 1.46/0.65 % TRYING [2]
% 1.46/0.65 % (170772)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=827788976:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.46/0.65 % TRYING [3]
% 1.46/0.65 % (170762)Instruction limit reached!
% 1.46/0.65 % (170762)------------------------------
% 1.46/0.65 % (170762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.65 % (170762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.65 % (170762)CaDiCaL version: 2.1.3
% 1.46/0.65 % (170762)Termination reason: Instruction limit
% 1.46/0.65 % (170762)Termination phase: Saturation
% 1.46/0.65 % (170762)Time elapsed: 0.091 s
% 1.46/0.65 % (170762)Peak memory usage: 14 MB
% 1.46/0.65 % (170762)Instructions burned: 160 (million)
% 1.46/0.65 % (170776)ott-21_1_sil=16000:fs=off:random_seed=748550877:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.46/0.65 % TRYING [4]
% 1.46/0.65 % (170771)Instruction limit reached!
% 1.46/0.65 % (170771)------------------------------
% 1.46/0.65 % (170771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.65 % (170771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.65 % (170771)CaDiCaL version: 2.1.3
% 1.46/0.65 % (170771)Termination reason: Instruction limit
% 1.46/0.65 % (170771)Termination phase: Saturation
% 1.46/0.65 % (170771)Time elapsed: 0.063 s
% 1.46/0.65 % (170771)Peak memory usage: 13 MB
% 1.46/0.65 % (170771)Instructions burned: 131 (million)
% 1.46/0.65 % (170778)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4085109045:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.46/0.65 % (170772) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-170751-170772"...
% 1.46/0.65 % (170772)...printing done.
% 1.46/0.65 % (170776)Instruction limit reached!
% 1.46/0.65 % (170776)------------------------------
% 1.46/0.65 % (170776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.65 % (170776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.65 % (170776)CaDiCaL version: 2.1.3
% 1.46/0.65 % (170776)Termination reason: Instruction limit
% 1.46/0.65 % (170776)Termination phase: Saturation
% 1.46/0.65 % (170776)Time elapsed: 0.089 s
% 1.46/0.65 % (170776)Peak memory usage: 13 MB
% 1.46/0.65 % (170776)Instructions burned: 180 (million)
% 1.46/0.65 % SZS status CounterSatisfiable for theBenchmark
% 1.46/0.65 % SZS output start Saturation.
% See solution above
% 1.46/0.66 % SZS output start Definitions and Model Updates.
% 1.46/0.66 for all groundings,
% 1.46/0.66 whenever iext(uri_rdf_type,X0,uri_rdfs_Datatype) is false, set ~idc(X0) to true
% 1.46/0.66 for all groundings,
% 1.46/0.66 whenever iext(uri_rdf_type,X0,uri_owl_AnnotationProperty) is false, set ~ioap(X0) to true
% 1.46/0.66 for all groundings,
% 1.46/0.66 whenever iext(uri_rdf_type,X0,uri_owl_DatatypeProperty) is false, set ~iodp(X0) to true
% 1.46/0.66 for all groundings,
% 1.46/0.66 whenever iext(uri_rdf_type,X0,uri_owl_OntologyProperty) is false, set ~ioxp(X0) to true
% 1.46/0.66 % SZS output end Definitions and Model Updates.
% 1.46/0.66 % (170772)------------------------------
% 1.46/0.66 % (170772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.66 % (170772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.66 % (170772)CaDiCaL version: 2.1.3
% 1.46/0.66 % (170772)Termination reason: Satisfiable
% 1.46/0.66 % (170772)Time elapsed: 0.112 s
% 1.46/0.66 % (170772)Peak memory usage: 15 MB
% 1.46/0.66 % (170772)Instructions burned: 171 (million)
% 1.46/0.66 % (170751)Success in time 0.248 s
% 1.46/0.66 % Vampire exiting
%------------------------------------------------------------------------------