%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWB007+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:31 PM UTC 2026
% Result : CounterSatisfiable 0.94s 0.62s
% Output : Saturation 0.94s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u470,negated_conjecture,
~ iext(uri_rdfs_range,uri_ex_p,uri_ex_c2) ).
cnf(u479,axiom,
ic(uri_rdfs_Resource) ).
cnf(u513,axiom,
ic(uri_rdf_Property) ).
cnf(u518,axiom,
icext(uri_rdfs_Resource,uri_rdf_first) ).
cnf(u524,axiom,
ic(uri_rdf_List) ).
cnf(u529,axiom,
icext(uri_rdfs_Resource,uri_rdf_nil) ).
cnf(u566,axiom,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_rdfs_Resource) ).
cnf(u628,axiom,
icext(uri_rdfs_Resource,uri_rdf_rest) ).
cnf(u633,axiom,
icext(uri_rdfs_Resource,uri_rdf__1) ).
cnf(u638,axiom,
icext(uri_rdfs_Resource,uri_rdf__2) ).
cnf(u643,axiom,
icext(uri_rdfs_Resource,uri_rdf__3) ).
cnf(u648,axiom,
icext(uri_rdfs_Resource,uri_rdf_object) ).
cnf(u653,axiom,
icext(uri_rdfs_Resource,uri_rdf_value) ).
cnf(u658,axiom,
icext(uri_rdfs_Resource,uri_rdf_subject) ).
cnf(u663,axiom,
icext(uri_rdfs_Resource,uri_rdf_type) ).
cnf(u728,axiom,
ic(uri_rdfs_Datatype) ).
cnf(u733,axiom,
icext(uri_rdfs_Resource,uri_rdf_XMLLiteral) ).
cnf(u907,axiom,
icext(uri_rdfs_Class,uri_owl_Thing) ).
cnf(u1028,axiom,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_owl_Thing) ).
cnf(u1117,axiom,
( ioap(sK13(uri_owl_AnnotationProperty,X0))
| iext(uri_rdfs_subClassOf,uri_owl_AnnotationProperty,X0)
| ~ ic(X0) ) ).
cnf(u1126,axiom,
( iodp(sK13(uri_owl_DatatypeProperty,X0))
| iext(uri_rdfs_subClassOf,uri_owl_DatatypeProperty,X0)
| ~ ic(X0) ) ).
cnf(u1135,axiom,
( ioxp(sK13(uri_owl_OntologyProperty,X0))
| iext(uri_rdfs_subClassOf,uri_owl_OntologyProperty,X0)
| ~ ic(X0) ) ).
cnf(u1207,axiom,
( ix(sK13(uri_owl_Ontology,X0))
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0)
| ~ ic(X0) ) ).
cnf(u1489,axiom,
~ iext(uri_owl_unionOf,uri_ex_c1,uri_rdf_nil) ).
cnf(u1494,axiom,
icext(uri_ex_c1,sK4(uri_ex_c1)) ).
cnf(u1503,axiom,
icext(uri_ex_c,sK4(uri_ex_c)) ).
cnf(u1508,axiom,
iext(uri_owl_unionOf,uri_rdfs_Statement,uri_rdf_nil) ).
cnf(u1517,axiom,
iext(uri_owl_unionOf,uri_rdf_XMLLiteral,uri_rdf_nil) ).
cnf(u1526,axiom,
iext(uri_owl_unionOf,uri_rdfs_Seq,uri_rdf_nil) ).
cnf(u1539,axiom,
icext(uri_rdfs_ContainerMembershipProperty,sK4(uri_rdfs_ContainerMembershipProperty)) ).
cnf(u1544,axiom,
iext(uri_owl_unionOf,uri_rdf_Bag,uri_rdf_nil) ).
cnf(u1557,axiom,
icext(uri_rdfs_Container,sK4(uri_rdfs_Container)) ).
cnf(u1566,axiom,
icext(uri_rdf_Alt,sK4(uri_rdf_Alt)) ).
cnf(u1575,axiom,
icext(uri_rdf_List,sK4(uri_rdf_List)) ).
cnf(u1584,axiom,
icext(uri_rdfs_Literal,sK4(uri_rdfs_Literal)) ).
cnf(u1593,axiom,
icext(uri_rdf_Property,sK4(uri_rdf_Property)) ).
cnf(u1602,axiom,
icext(uri_rdfs_Datatype,sK4(uri_rdfs_Datatype)) ).
cnf(u1611,axiom,
icext(uri_rdfs_Class,sK4(uri_rdfs_Class)) ).
cnf(u1705,axiom,
icext(uri_rdfs_Class,uri_owl_Nothing) ).
cnf(u1775,axiom,
iext(uri_owl_unionOf,sK4(uri_rdfs_Datatype),uri_rdf_nil) ).
cnf(u1791,axiom,
iext(uri_owl_unionOf,sK4(uri_rdfs_Class),uri_rdf_nil) ).
cnf(u1994,axiom,
iext(uri_owl_intersectionOf,uri_rdf_Property,uri_rdf_nil) ).
cnf(u2003,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Class,uri_rdf_nil) ).
cnf(u2249,axiom,
ix(sK4(uri_owl_Ontology)) ).
cnf(u2262,axiom,
iext(uri_owl_unionOf,uri_owl_OntologyProperty,uri_rdf_nil) ).
cnf(u2271,axiom,
iext(uri_owl_unionOf,uri_owl_DatatypeProperty,uri_rdf_nil) ).
cnf(u2280,axiom,
iext(uri_owl_unionOf,uri_owl_AnnotationProperty,uri_rdf_nil) ).
cnf(u2938,axiom,
icext(sK14(uri_owl_complementOf,uri_rdf_type),sK14(uri_owl_complementOf,uri_rdf_type)) ).
cnf(u248,axiom,
( ~ iext(uri_owl_unionOf,X0,uri_rdf_nil)
| ~ icext(X0,X1) ) ).
cnf(u2289,axiom,
iext(uri_rdfs_subClassOf,uri_owl_OntologyProperty,X0) ).
cnf(u2706,axiom,
( lv(sK12(uri_rdfs_label,X0))
| iext(uri_rdfs_range,uri_rdfs_label,X0) ) ).
cnf(u2544,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(u2945,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(u2959,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(u1401,axiom,
( lv(sK13(sK13(uri_rdfs_Datatype,X0),X1))
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0)
| ~ ic(X1)
| iext(uri_rdfs_subClassOf,sK13(uri_rdfs_Datatype,X0),X1) ) ).
cnf(u2862,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(u2868,axiom,
( iext(uri_rdfs_seeAlso,sK9(uri_rdfs_isDefinedBy,X0),sK10(uri_rdfs_isDefinedBy,X0))
| iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,X0) ) ).
cnf(u2873,axiom,
iext(uri_rdfs_domain,uri_rdf_object,X0) ).
cnf(u293,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_AnnotationProperty)
| ioap(X0) ) ).
cnf(u423,axiom,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class) ).
cnf(u575,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing)
| iext(uri_rdfs_subClassOf,X0,uri_ex_c1) ) ).
cnf(u2887,axiom,
iext(uri_rdfs_domain,uri_owl_onProperty,uri_owl_Restriction) ).
cnf(u421,axiom,
( ~ icext(uri_rdfs_Literal,X0)
| lv(X0) ) ).
cnf(u306,axiom,
( iext(uri_rdf_type,X0,uri_rdf_Property)
| ~ ip(X0) ) ).
cnf(u2859,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,X0),X1)
| icext(sK10(uri_rdfs_subClassOf,X0),X1)
| iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0) ) ).
cnf(u2750,axiom,
( iext(uri_rdfs_member,sK14(sK4(uri_rdfs_ContainerMembershipProperty),X0),sK15(sK4(uri_rdfs_ContainerMembershipProperty),X0))
| iext(uri_rdfs_subPropertyOf,sK4(uri_rdfs_ContainerMembershipProperty),X0) ) ).
cnf(u2984,axiom,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
| iext(uri_rdfs_subPropertyOf,sK13(uri_rdfs_ContainerMembershipProperty,X1),X0)
| iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X1) ) ).
cnf(u1734,axiom,
iext(uri_rdfs_subPropertyOf,sK4(uri_rdfs_ContainerMembershipProperty),uri_rdfs_member) ).
cnf(u1865,axiom,
( iext(uri_rdfs_member,X0,X1)
| ~ iext(uri_rdf__1,X0,X1) ) ).
cnf(u2658,axiom,
( icext(uri_rdf_List,sK12(uri_rdf_rest,X0))
| iext(uri_rdfs_range,uri_rdf_rest,X0) ) ).
cnf(u706,axiom,
icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2) ).
cnf(u2652,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(u323,axiom,
( ~ iext(uri_owl_hasValue,X0,X1)
| icext(uri_owl_Restriction,X0) ) ).
cnf(u2128,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,X0) ).
cnf(u372,axiom,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property) ).
cnf(u2774,axiom,
( ~ iext(uri_rdf__1,sK14(X0,uri_rdfs_member),sK15(X0,uri_rdfs_member))
| iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member) ) ).
cnf(u2917,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(u2761,axiom,
( lv(sK15(uri_rdfs_label,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_label,X0) ) ).
cnf(u2667,axiom,
( ~ iext(uri_owl_hasValue,sK11(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_range,uri_owl_onProperty,X0)
| ~ iext(sK12(uri_owl_onProperty,X0),X2,X1)
| icext(sK11(uri_owl_onProperty,X0),X2) ) ).
cnf(u2157,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(u2930,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(u2775,axiom,
iext(uri_rdfs_subPropertyOf,X0,X0) ).
cnf(u2657,axiom,
( icext(uri_rdf_List,sK11(uri_rdf_rest,X0))
| iext(uri_rdfs_range,uri_rdf_rest,X0) ) ).
cnf(u2412,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK4(uri_rdfs_Datatype))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u363,axiom,
( ~ iext(uri_owl_someValuesFrom,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| iext(X1,X3,sK17(X1,X2,X3))
| ~ icext(X0,X3) ) ).
cnf(u2671,axiom,
( icext(sK12(uri_owl_someValuesFrom,X0),sK17(X1,sK12(uri_owl_someValuesFrom,X0),X2))
| ~ iext(uri_owl_onProperty,sK11(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_range,uri_owl_someValuesFrom,X0)
| ~ icext(sK11(uri_owl_someValuesFrom,X0),X2) ) ).
cnf(u2762,axiom,
( iext(uri_rdf_type,sK15(uri_rdfs_label,X0),uri_rdfs_Literal)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_label,X0) ) ).
cnf(u2148,axiom,
iext(uri_rdfs_range,X0,uri_rdf_Property) ).
cnf(u2062,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty) ) ).
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(u2010,axiom,
icext(uri_rdf_Property,X0) ).
cnf(u361,axiom,
( ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_hasValue,X0,X2)
| iext(X1,X3,X2)
| ~ icext(X0,X3) ) ).
cnf(u2918,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(u1399,axiom,
( ~ icext(sK13(uri_rdfs_Datatype,X0),X1)
| lv(X1)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0) ) ).
cnf(u1753,axiom,
icext(uri_rdfs_Container,sK4(uri_rdf_Alt)) ).
cnf(u2929,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(u2046,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container) ) ).
cnf(u2059,axiom,
( iext(X0,sK14(X0,X1),sK15(X0,X1))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u2690,axiom,
( ~ iext(uri_rdf_object,X0,X1)
| icext(X2,X1) ) ).
cnf(u390,axiom,
iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List) ).
cnf(u2696,axiom,
iext(uri_rdfs_range,uri_owl_unionOf,uri_rdf_List) ).
cnf(u2846,axiom,
( icext(uri_owl_Restriction,sK9(uri_owl_hasValue,X0))
| iext(uri_rdfs_domain,uri_owl_hasValue,X0) ) ).
cnf(u2852,axiom,
( icext(uri_owl_Restriction,sK9(uri_owl_onProperty,X0))
| iext(uri_rdfs_domain,uri_owl_onProperty,X0) ) ).
cnf(u388,axiom,
( ~ iext(uri_rdf_type,X0,X1)
| icext(X1,X0) ) ).
cnf(u3111,axiom,
( iext(uri_rdfs_subClassOf,sK15(uri_owl_complementOf,X0),sK15(uri_owl_complementOf,X0))
| iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0) ) ).
cnf(u2857,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(u2100,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u2178,axiom,
iext(uri_rdfs_subClassOf,sK4(uri_rdfs_Class),X0) ).
cnf(u2974,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(u2871,axiom,
( icext(uri_ex_c1,sK10(uri_ex_p,X0))
| iext(uri_rdfs_domain,uri_ex_p,X0) ) ).
cnf(u2701,axiom,
( lv(sK12(uri_rdfs_comment,X0))
| iext(uri_rdfs_range,uri_rdfs_comment,X0) ) ).
cnf(u407,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty) ).
cnf(u2580,axiom,
iext(uri_rdfs_domain,X0,uri_rdf_Property) ).
cnf(u2985,axiom,
( iext(uri_rdfs_subPropertyOf,sK13(uri_rdfs_ContainerMembershipProperty,X0),uri_rdfs_member)
| iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0) ) ).
cnf(u1446,axiom,
( iext(uri_rdfs_subPropertyOf,sK13(uri_rdfs_ContainerMembershipProperty,X0),uri_rdfs_member)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0) ) ).
cnf(u2352,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| ~ iext(uri_rdfs_subClassOf,X1,X0)
| iext(uri_rdfs_subClassOf,X1,uri_rdf_Alt) ) ).
cnf(u2612,axiom,
( ix(sK13(uri_owl_Ontology,X0))
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ) ).
cnf(u2843,axiom,
( icext(uri_rdf_List,sK10(uri_owl_unionOf,X0))
| iext(uri_rdfs_domain,uri_owl_unionOf,X0) ) ).
cnf(u1444,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member) ).
cnf(u2734,axiom,
( icext(sK15(uri_owl_someValuesFrom,X0),sK17(X1,sK15(uri_owl_someValuesFrom,X0),X2))
| ~ iext(uri_owl_onProperty,sK14(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0)
| ~ icext(sK14(uri_owl_someValuesFrom,X0),X2) ) ).
cnf(u317,axiom,
( ~ iext(uri_owl_allValuesFrom,X0,X1)
| icext(uri_owl_Restriction,X0) ) ).
cnf(u2858,axiom,
( ~ iext(sK9(uri_rdfs_range,X0),X1,X2)
| iext(uri_rdfs_domain,uri_rdfs_range,X0)
| icext(sK10(uri_rdfs_range,X0),X2) ) ).
cnf(u2740,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(u1199,axiom,
( ~ icext(uri_owl_Ontology,X0)
| ix(X0) ) ).
cnf(u2617,axiom,
( iext(uri_rdf_type,sK13(uri_owl_Ontology,X0),uri_owl_Ontology)
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ) ).
cnf(u2757,axiom,
( ~ iext(uri_rdf_object,X1,X2)
| iext(X0,X1,X2) ) ).
cnf(u2745,axiom,
( icext(uri_rdfs_Literal,sK15(uri_rdfs_comment,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,X0) ) ).
cnf(u2758,axiom,
( lv(sK15(uri_rdfs_comment,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,X0) ) ).
cnf(u2899,axiom,
( lv(sK10(uri_rdfs_label,X0))
| iext(uri_rdfs_domain,uri_rdfs_label,X0) ) ).
cnf(u2245,axiom,
( icext(uri_rdfs_Literal,sK4(sK13(uri_rdfs_Datatype,X0)))
| iext(uri_owl_unionOf,sK13(uri_rdfs_Datatype,X0),uri_rdf_nil)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0) ) ).
cnf(u458,axiom,
iext(uri_owl_sameAs,uri_ex_c1,uri_ex_c2) ).
cnf(u2746,axiom,
( iext(uri_rdfs_seeAlso,sK14(uri_rdfs_isDefinedBy,X0),sK15(uri_rdfs_isDefinedBy,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,X0) ) ).
cnf(u1868,axiom,
( ~ iext(sK4(uri_rdfs_ContainerMembershipProperty),X0,X1)
| iext(uri_rdfs_member,X0,X1) ) ).
cnf(u3029,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(u2653,axiom,
( ~ icext(sK12(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_range,uri_owl_complementOf,X0)
| ~ icext(sK11(uri_owl_complementOf,X0),X1) ) ).
cnf(u2759,axiom,
( iext(uri_rdf_type,sK15(uri_rdfs_comment,X0),uri_rdfs_Literal)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,X0) ) ).
cnf(u1866,axiom,
( iext(uri_rdfs_member,X0,X1)
| ~ iext(uri_rdf__2,X0,X1) ) ).
cnf(u347,axiom,
( icext(X0,sK13(X0,X1))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u334,axiom,
( ~ iext(uri_owl_unionOf,X0,X1)
| icext(uri_rdf_List,X1) ) ).
cnf(u717,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal) ) ).
cnf(u456,axiom,
iext(uri_rdfs_subClassOf,uri_ex_c,uri_ex_c1) ).
cnf(u2655,axiom,
( icext(uri_rdf_List,sK12(uri_owl_intersectionOf,X0))
| iext(uri_rdfs_range,uri_owl_intersectionOf,X0) ) ).
cnf(u3042,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(u2980,axiom,
( ~ iext(sK13(uri_rdfs_ContainerMembershipProperty,X2),X0,X1)
| iext(uri_rdfs_member,X0,X1)
| iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X2) ) ).
cnf(u2147,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Class) ).
cnf(u368,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property) ).
cnf(u1645,axiom,
( ~ iext(uri_rdf_object,X0,X1)
| icext(uri_rdfs_Statement,X0) ) ).
cnf(u2674,axiom,
( ~ iext(sK11(uri_rdfs_range,X0),X1,X2)
| iext(uri_rdfs_range,uri_rdfs_range,X0)
| icext(sK12(uri_rdfs_range,X0),X2) ) ).
cnf(u2913,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(u1643,axiom,
( ~ iext(uri_rdf_first,X0,X1)
| icext(uri_rdf_List,X0) ) ).
cnf(u2680,axiom,
iext(uri_rdfs_range,uri_rdf_subject,X0) ).
cnf(u3030,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(u2530,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(u1649,axiom,
icext(uri_ex_c1,sK4(uri_ex_c)) ).
cnf(u2036,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,X0) ).
cnf(u1403,axiom,
( icext(uri_rdfs_Literal,sK13(sK13(uri_rdfs_Datatype,X0),X1))
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0)
| ~ ic(X1)
| iext(uri_rdfs_subClassOf,sK13(uri_rdfs_Datatype,X0),X1)
| ~ ic(X0) ) ).
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(X2,X5)
| ~ icext(X0,X5)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u3041,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(u2284,axiom,
~ icext(uri_owl_OntologyProperty,X0) ).
cnf(u2721,axiom,
( icext(uri_rdf_List,sK15(uri_rdf_rest,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0) ) ).
cnf(u2685,axiom,
( icext(uri_ex_c1,sK12(uri_ex_p,X0))
| iext(uri_rdfs_range,uri_ex_p,X0) ) ).
cnf(u2057,axiom,
( iext(X0,sK11(X0,X1),sK12(X0,X1))
| iext(uri_rdfs_range,X0,X1) ) ).
cnf(u500,axiom,
( ~ icext(uri_ex_c,X0)
| icext(uri_ex_c1,X0) ) ).
cnf(u2683,axiom,
( icext(uri_rdfs_Literal,sK12(uri_rdfs_label,X0))
| iext(uri_rdfs_range,uri_rdfs_label,X0) ) ).
cnf(u2841,axiom,
( icext(uri_rdf_List,sK9(uri_rdf_rest,X0))
| iext(uri_rdfs_domain,uri_rdf_rest,X0) ) ).
cnf(u2175,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(u2290,axiom,
~ icext(uri_owl_DatatypeProperty,X0) ).
cnf(u2958,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(u1064,axiom,
( ~ icext(uri_rdfs_Datatype,X0)
| idc(X0) ) ).
cnf(u2855,axiom,
( icext(sK10(uri_owl_someValuesFrom,X0),sK17(X1,sK10(uri_owl_someValuesFrom,X0),X2))
| ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0)
| ~ icext(sK9(uri_owl_someValuesFrom,X0),X2) ) ).
cnf(u229,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(u2581,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Resource) ).
cnf(u2969,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(u2303,axiom,
icext(uri_owl_Ontology,sK4(uri_owl_Ontology)) ).
cnf(u2336,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_AnnotationProperty)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u2983,axiom,
( iext(uri_rdfs_member,sK14(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1),sK15(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1))
| iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0)
| iext(uri_rdfs_subPropertyOf,sK13(uri_rdfs_ContainerMembershipProperty,X0),X1) ) ).
cnf(u1935,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing) ) ).
cnf(u412,axiom,
( ~ icext(uri_rdfs_Datatype,X0)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal) ) ).
cnf(u299,axiom,
( ~ ioxp(X0)
| ~ iext(X0,X1,X2)
| ix(X1) ) ).
cnf(u2611,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(u2718,axiom,
( icext(uri_rdf_List,sK15(uri_owl_intersectionOf,X0))
| iext(uri_rdfs_subPropertyOf,uri_owl_intersectionOf,X0) ) ).
cnf(u301,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_OntologyProperty)
| ioxp(X0) ) ).
cnf(u1847,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK4(uri_rdfs_Datatype))
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal) ) ).
cnf(u2957,axiom,
( icext(sK15(uri_rdfs_domain,X0),sK9(sK14(uri_rdfs_domain,X0),X1))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0)
| iext(uri_rdfs_domain,sK14(uri_rdfs_domain,X0),X1) ) ).
cnf(u2952,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(u2842,axiom,
( icext(uri_rdf_List,sK10(uri_rdf_rest,X0))
| iext(uri_rdfs_domain,uri_rdf_rest,X0) ) ).
cnf(u2724,axiom,
( icext(uri_owl_Restriction,sK14(uri_owl_allValuesFrom,X0))
| iext(uri_rdfs_subPropertyOf,uri_owl_allValuesFrom,X0) ) ).
cnf(u2741,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(u2955,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(u2848,axiom,
( ~ iext(uri_owl_allValuesFrom,sK9(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_domain,uri_owl_onProperty,X0)
| ~ iext(sK10(uri_owl_onProperty,X0),X2,X3)
| icext(X1,X3)
| ~ icext(sK9(uri_owl_onProperty,X0),X2) ) ).
cnf(u2739,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(u314,axiom,
( ~ iext(uri_rdf_type,X0,uri_rdfs_Literal)
| lv(X0) ) ).
cnf(u2970,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(u2976,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(u2748,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,X0) ).
cnf(u312,axiom,
( ~ ix(X0)
| iext(uri_rdf_type,X0,uri_owl_Ontology) ) ).
cnf(u2729,axiom,
( ~ iext(uri_owl_hasValue,sK14(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0)
| iext(sK15(uri_owl_onProperty,X0),X2,X1)
| ~ icext(sK14(uri_owl_onProperty,X0),X2) ) ).
cnf(u2113,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,X0) ).
cnf(u2730,axiom,
( ~ iext(uri_owl_hasValue,sK14(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0)
| ~ iext(sK15(uri_owl_onProperty,X0),X2,X1)
| icext(sK14(uri_owl_onProperty,X0),X2) ) ).
cnf(u2736,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(u1978,axiom,
( ~ icext(X0,sK0(X0))
| ~ ic(X0)
| iext(uri_owl_intersectionOf,X0,uri_rdf_nil) ) ).
cnf(u964,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container) ) ).
cnf(u446,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,X1)
| ~ iext(uri_rdfs_subPropertyOf,X1,X2)
| iext(uri_rdfs_subPropertyOf,X0,X2) ) ).
cnf(u2399,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| ~ iext(uri_rdfs_subClassOf,X1,X0)
| iext(uri_rdfs_subClassOf,X1,uri_ex_c) ) ).
cnf(u329,axiom,
( ~ iext(uri_owl_onProperty,X0,X1)
| icext(uri_owl_Restriction,X0) ) ).
cnf(u2158,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Statement,X0) ).
cnf(u2244,axiom,
( iext(uri_owl_unionOf,sK13(uri_rdfs_Datatype,X0),uri_rdf_nil)
| lv(sK4(sK13(uri_rdfs_Datatype,X0)))
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0) ) ).
cnf(u2527,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(u1890,axiom,
~ icext(sK4(uri_rdfs_Datatype),X0) ).
cnf(u2897,axiom,
( iext(uri_rdf_type,sK10(uri_rdfs_comment,X0),uri_rdfs_Literal)
| iext(uri_rdfs_domain,uri_rdfs_comment,X0) ) ).
cnf(u358,axiom,
( ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_allValuesFrom,X0,X2)
| iext(X1,X3,sK16(X1,X2,X3))
| icext(X0,X3) ) ).
cnf(u2664,axiom,
( ~ iext(uri_owl_allValuesFrom,sK11(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_range,uri_owl_onProperty,X0)
| ~ iext(sK12(uri_owl_onProperty,X0),X2,X3)
| icext(X1,X3)
| ~ icext(sK11(uri_owl_onProperty,X0),X2) ) ).
cnf(u1757,axiom,
iext(uri_rdf_type,sK4(uri_rdfs_Literal),uri_rdfs_Literal) ).
cnf(u2410,axiom,
iext(uri_rdfs_subClassOf,sK4(uri_rdfs_Datatype),X0) ).
cnf(u369,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property) ).
cnf(u1755,axiom,
lv(sK4(uri_rdfs_Literal)) ).
cnf(u3039,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(u2146,axiom,
iext(uri_rdfs_range,X0,uri_owl_Thing) ).
cnf(u2283,axiom,
( ~ icext(X1,sK9(X0,X1))
| iext(uri_rdfs_domain,X0,X1) ) ).
cnf(u2771,axiom,
( ~ icext(sK15(X0,uri_rdf_type),sK14(X0,uri_rdf_type))
| iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type) ) ).
cnf(u2669,axiom,
( ~ iext(uri_owl_onProperty,sK11(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_range,uri_owl_someValuesFrom,X0)
| ~ icext(sK12(uri_owl_someValuesFrom,X0),X2)
| ~ iext(X1,X3,X2)
| icext(sK11(uri_owl_someValuesFrom,X0),X3) ) ).
cnf(u497,axiom,
icext(uri_ex_c1,uri_ex_w) ).
cnf(u2947,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(u1899,axiom,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
| iext(uri_rdfs_subPropertyOf,uri_rdf__3,X0) ) ).
cnf(u2839,axiom,
( icext(uri_rdf_List,sK10(uri_owl_intersectionOf,X0))
| iext(uri_rdfs_domain,uri_owl_intersectionOf,X0) ) ).
cnf(u373,axiom,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property) ).
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(X4,X7)
| icext(X0,X7)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u2953,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(u287,axiom,
( ~ idc(X0)
| ~ icext(X0,X1)
| lv(X1) ) ).
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(X4,X5)
| icext(X0,X5)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u396,axiom,
( ~ icext(uri_rdfs_ContainerMembershipProperty,X0)
| iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member) ) ).
cnf(u1157,axiom,
( icext(uri_rdfs_Literal,sK13(uri_rdfs_Literal,X0))
| iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X0)
| ~ ic(X0) ) ).
cnf(u2595,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(u2282,axiom,
iext(uri_rdf_type,sK4(uri_owl_Ontology),uri_owl_Ontology) ).
cnf(u2087,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| iext(uri_rdfs_subClassOf,X0,uri_ex_c1) ) ).
cnf(u553,axiom,
( icext(uri_ex_c1,sK13(uri_ex_c,X0))
| iext(uri_rdfs_subClassOf,uri_ex_c,X0)
| ~ ic(X0) ) ).
cnf(u2708,axiom,
( iext(uri_rdf_type,sK12(uri_rdfs_label,X0),uri_rdfs_Literal)
| iext(uri_rdfs_range,uri_rdfs_label,X0) ) ).
cnf(u2725,axiom,
( icext(uri_owl_Restriction,sK14(uri_owl_hasValue,X0))
| iext(uri_rdfs_subPropertyOf,uri_owl_hasValue,X0) ) ).
cnf(u2723,axiom,
( icext(sK15(uri_rdf_type,X0),sK14(uri_rdf_type,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0) ) ).
cnf(u298,axiom,
( ~ ioxp(X0)
| ~ iext(X0,X1,X2)
| ix(X2) ) ).
cnf(u384,axiom,
iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal) ).
cnf(u2954,axiom,
( icext(sK12(uri_rdfs_range,X0),sK10(sK11(uri_rdfs_range,X0),X1))
| iext(uri_rdfs_range,uri_rdfs_range,X0)
| iext(uri_rdfs_domain,sK11(uri_rdfs_range,X0),X1) ) ).
cnf(u2585,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(u1896,axiom,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,X0)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,X0) ) ).
cnf(u2726,axiom,
( ~ iext(uri_owl_allValuesFrom,sK14(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0)
| iext(sK15(uri_owl_onProperty,X0),X2,sK16(sK15(uri_owl_onProperty,X0),X1,X2))
| icext(sK14(uri_owl_onProperty,X0),X2) ) ).
cnf(u2869,axiom,
( icext(uri_rdfs_Literal,sK10(uri_rdfs_label,X0))
| iext(uri_rdfs_domain,uri_rdfs_label,X0) ) ).
cnf(u2960,axiom,
( icext(sK15(uri_rdfs_range,X0),sK10(sK14(uri_rdfs_range,X0),X1))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0)
| iext(uri_rdfs_domain,sK14(uri_rdfs_range,X0),X1) ) ).
cnf(u2599,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(u2465,axiom,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,X0) ).
cnf(u2732,axiom,
( ~ iext(uri_owl_onProperty,sK14(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0)
| ~ icext(sK15(uri_owl_someValuesFrom,X0),X2)
| ~ iext(X1,X3,X2)
| icext(sK14(uri_owl_someValuesFrom,X0),X3) ) ).
cnf(u2867,axiom,
( icext(uri_rdfs_Literal,sK10(uri_rdfs_comment,X0))
| iext(uri_rdfs_domain,uri_rdfs_comment,X0) ) ).
cnf(u1830,axiom,
~ icext(uri_rdfs_Statement,X0) ).
cnf(u557,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,uri_owl_Nothing)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,X1,X0) ) ).
cnf(u1410,axiom,
( ~ icext(sK13(uri_rdfs_Datatype,X0),X1)
| ~ ic(X0)
| icext(uri_rdfs_Literal,X1)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0) ) ).
cnf(u2727,axiom,
( ~ iext(uri_owl_allValuesFrom,sK14(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0)
| ~ iext(sK15(uri_owl_onProperty,X0),X2,X3)
| icext(X1,X3)
| ~ icext(sK14(uri_owl_onProperty,X0),X2) ) ).
cnf(u315,axiom,
( ~ lv(X0)
| iext(uri_rdf_type,X0,uri_rdfs_Literal) ) ).
cnf(u1214,axiom,
( iext(uri_rdf_type,sK13(uri_rdfs_Literal,X0),uri_rdfs_Literal)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X0) ) ).
cnf(u2623,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(u2720,axiom,
( icext(uri_rdf_List,sK14(uri_rdf_rest,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0) ) ).
cnf(u2737,axiom,
( ~ iext(sK14(uri_rdfs_range,X0),X1,X2)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0)
| icext(sK15(uri_rdfs_range,X0),X2) ) ).
cnf(u2870,axiom,
iext(uri_rdfs_domain,uri_rdf_predicate,X0) ).
cnf(u2751,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf_object,X0) ).
cnf(u1099,axiom,
( idc(sK13(uri_rdfs_Datatype,X0))
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0) ) ).
cnf(u2876,axiom,
( ~ iext(uri_rdf_object,X1,X2)
| icext(X0,X1) ) ).
cnf(u364,axiom,
( ~ iext(uri_owl_someValuesFrom,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ icext(X2,X4)
| ~ iext(X1,X3,X4)
| icext(X0,X3) ) ).
cnf(u2115,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u595,axiom,
( ~ iext(uri_rdfs_label,X0,X1)
| icext(uri_rdfs_Literal,X1) ) ).
cnf(u1613,axiom,
iext(uri_owl_unionOf,uri_owl_Nothing,uri_rdf_nil) ).
cnf(u2881,axiom,
iext(uri_rdfs_domain,uri_owl_allValuesFrom,uri_owl_Restriction) ).
cnf(u614,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container) ) ).
cnf(u1741,axiom,
~ icext(uri_rdf_Bag,X0) ).
cnf(u585,axiom,
( ~ iext(uri_rdfs_comment,X0,X1)
| icext(uri_rdfs_Literal,X1) ) ).
cnf(u2130,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u867,axiom,
icext(uri_owl_Thing,X0) ).
cnf(u2926,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(u1653,axiom,
~ icext(uri_rdf_XMLLiteral,X0) ).
cnf(u213,axiom,
( ~ iext(uri_owl_complementOf,X0,X1)
| ~ icext(X1,X2)
| ~ icext(X0,X2) ) ).
cnf(u359,axiom,
( ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_allValuesFrom,X0,X2)
| ~ icext(X2,sK16(X1,X2,X3))
| icext(X0,X3) ) ).
cnf(u2995,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,sK13(uri_rdfs_Datatype,X0))
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0)
| lv(sK4(sK13(uri_rdfs_Datatype,X0)))
| iext(uri_rdfs_subClassOf,X1,X2) ) ).
cnf(u224,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(u2143,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdf_Property) ).
cnf(u1764,axiom,
idc(sK4(uri_rdfs_Datatype)) ).
cnf(u357,axiom,
( ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_allValuesFrom,X0,X2)
| ~ iext(X1,X3,X4)
| icext(X2,X4)
| ~ icext(X0,X3) ) ).
cnf(u2154,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(u1402,axiom,
( iext(uri_rdf_type,sK13(sK13(uri_rdfs_Datatype,X0),X1),uri_rdfs_Literal)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0)
| ~ ic(X1)
| iext(uri_rdfs_subClassOf,sK13(uri_rdfs_Datatype,X0),X1)
| ~ ic(X0) ) ).
cnf(u2722,axiom,
( icext(uri_rdf_List,sK15(uri_owl_unionOf,X0))
| iext(uri_rdfs_subPropertyOf,uri_owl_unionOf,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(u2031,axiom,
( ~ icext(X1,sK12(X0,X1))
| iext(uri_rdfs_range,X0,X1) ) ).
cnf(u370,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property) ).
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(X2,X5)
| ~ icext(X0,X5)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u2923,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(u2579,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Class) ).
cnf(u269,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(u520,axiom,
icext(uri_rdf_List,uri_rdf_nil) ).
cnf(u3048,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(u2093,axiom,
iext(uri_rdfs_subClassOf,X0,uri_owl_Thing) ).
cnf(u3051,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(u2296,axiom,
~ icext(uri_owl_AnnotationProperty,X0) ).
cnf(u2321,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_DatatypeProperty)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u2588,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(u259,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(u2853,axiom,
( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0)
| ~ icext(sK10(uri_owl_someValuesFrom,X0),X2)
| ~ iext(X1,X3,X2)
| icext(sK9(uri_owl_someValuesFrom,X0),X3) ) ).
cnf(u1413,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,sK13(uri_rdfs_Datatype,X0))
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0)
| iext(uri_rdfs_subClassOf,X1,uri_rdfs_Literal) ) ).
cnf(u2716,axiom,
( ~ icext(sK15(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
| ~ icext(sK14(uri_owl_complementOf,X0),X1) ) ).
cnf(u2851,axiom,
( ~ iext(uri_owl_hasValue,sK9(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_domain,uri_owl_onProperty,X0)
| ~ iext(sK10(uri_owl_onProperty,X0),X2,X1)
| icext(sK9(uri_owl_onProperty,X0),X2) ) ).
cnf(u387,axiom,
( iext(uri_rdf_type,X0,X1)
| ~ icext(X1,X0) ) ).
cnf(u1063,axiom,
idc(uri_rdf_XMLLiteral) ).
cnf(u2981,axiom,
( iext(uri_rdfs_member,sK9(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1),sK10(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1))
| iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0)
| iext(uri_rdfs_domain,sK13(uri_rdfs_ContainerMembershipProperty,X0),X1) ) ).
cnf(u2866,axiom,
iext(uri_rdfs_domain,uri_rdf_subject,X0) ).
cnf(u2979,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(u2872,axiom,
( iext(uri_rdfs_member,sK9(sK4(uri_rdfs_ContainerMembershipProperty),X0),sK10(sK4(uri_rdfs_ContainerMembershipProperty),X0))
| iext(uri_rdfs_domain,sK4(uri_rdfs_ContainerMembershipProperty),X0) ) ).
cnf(u286,axiom,
( iext(uri_rdf_type,X0,uri_rdfs_Class)
| ~ ic(X0) ) ).
cnf(u408,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty) ).
cnf(u2607,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(u297,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_DatatypeProperty)
| iodp(X0) ) ).
cnf(u3043,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(u2854,axiom,
( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0)
| iext(X1,X2,sK17(X1,sK10(uri_owl_someValuesFrom,X0),X2))
| ~ icext(sK9(uri_owl_someValuesFrom,X0),X2) ) ).
cnf(u2735,axiom,
( icext(uri_owl_Restriction,sK14(uri_owl_someValuesFrom,X0))
| iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0) ) ).
cnf(u2860,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(u1443,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member) ).
cnf(u2365,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| ~ iext(uri_rdfs_subClassOf,X1,X0)
| iext(uri_rdfs_subClassOf,X1,uri_rdf_Bag) ) ).
cnf(u425,axiom,
( ~ iext(uri_rdfs_range,X0,X1)
| ~ iext(X0,X2,X3)
| icext(X1,X3) ) ).
cnf(u2603,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(u2982,axiom,
( iext(uri_rdfs_member,sK11(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1),sK12(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1))
| iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0)
| iext(uri_rdfs_range,sK13(uri_rdfs_ContainerMembershipProperty,X0),X1) ) ).
cnf(u2988,axiom,
( ~ icext(sK13(uri_rdfs_Datatype,X0),X1)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0)
| lv(sK4(sK13(uri_rdfs_Datatype,X0))) ) ).
cnf(u1858,axiom,
~ icext(sK4(uri_rdfs_Class),X0) ).
cnf(u2993,axiom,
( iext(uri_rdfs_subClassOf,sK13(uri_rdfs_Datatype,X0),X1)
| lv(sK4(sK13(uri_rdfs_Datatype,X0)))
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0) ) ).
cnf(u1864,axiom,
( ~ iext(uri_rdfs_isDefinedBy,X0,X1)
| iext(uri_rdfs_seeAlso,X0,X1) ) ).
cnf(u1986,axiom,
iext(uri_owl_intersectionOf,uri_owl_Thing,uri_rdf_nil) ).
cnf(u452,axiom,
ir(X0) ).
cnf(u1867,axiom,
( iext(uri_rdfs_member,X0,X1)
| ~ iext(uri_rdf__3,X0,X1) ) ).
cnf(u3038,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(u609,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container) ) ).
cnf(u3044,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(u3049,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(u1660,axiom,
~ icext(uri_rdfs_Seq,X0) ).
cnf(u2670,axiom,
( ~ iext(uri_owl_onProperty,sK11(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_range,uri_owl_someValuesFrom,X0)
| iext(X1,X2,sK17(X1,sK12(uri_owl_someValuesFrom,X0),X2))
| ~ icext(sK11(uri_owl_someValuesFrom,X0),X2) ) ).
cnf(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(X4,X7)
| ~ icext(X0,X7)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u2909,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(u2015,axiom,
ip(X0) ).
cnf(u354,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,X1)
| iext(X1,X2,X3)
| ~ iext(X0,X2,X3) ) ).
cnf(u2676,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(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(X4,X5)
| ~ icext(X0,X5)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u2037,axiom,
( icext(X0,sK4(X0))
| iext(uri_owl_unionOf,X0,uri_rdf_nil) ) ).
cnf(u2055,axiom,
( iext(X0,sK9(X0,X1),sK10(X0,X1))
| iext(uri_rdfs_domain,X0,X1) ) ).
cnf(u3032,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(u2922,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(u2083,axiom,
( iext(uri_rdfs_subClassOf,X0,uri_ex_c)
| ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral) ) ).
cnf(u254,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(u2693,axiom,
iext(uri_rdfs_range,uri_owl_intersectionOf,uri_rdf_List) ).
cnf(u895,axiom,
icext(uri_rdfs_Resource,X0) ).
cnf(u371,axiom,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property) ).
cnf(u2717,axiom,
( icext(sK15(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
| icext(sK14(uri_owl_complementOf,X0),X1) ) ).
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(X4,X7)
| icext(X2,X7)
| ~ icext(X0,X7)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u2295,axiom,
iext(uri_rdfs_subClassOf,uri_owl_DatatypeProperty,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(X2,X7)
| ~ icext(X0,X7)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u2681,axiom,
( icext(uri_rdfs_Literal,sK12(uri_rdfs_comment,X0))
| iext(uri_rdfs_range,uri_rdfs_comment,X0) ) ).
cnf(u2837,axiom,
( ~ icext(sK10(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_domain,uri_owl_complementOf,X0)
| ~ icext(sK9(uri_owl_complementOf,X0),X1) ) ).
cnf(u2773,axiom,
( ~ iext(uri_rdf__2,sK14(X0,uri_rdfs_member),sK15(X0,uri_rdfs_member))
| iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member) ) ).
cnf(u394,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container) ).
cnf(u2682,axiom,
( iext(uri_rdfs_seeAlso,sK11(uri_rdfs_isDefinedBy,X0),sK12(uri_rdfs_isDefinedBy,X0))
| iext(uri_rdfs_range,uri_rdfs_isDefinedBy,X0) ) ).
cnf(u2850,axiom,
( ~ iext(uri_owl_hasValue,sK9(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_domain,uri_owl_onProperty,X0)
| iext(sK10(uri_owl_onProperty,X0),X2,X1)
| ~ icext(sK9(uri_owl_onProperty,X0),X2) ) ).
cnf(u2963,axiom,
( ~ icext(sK9(uri_owl_complementOf,X0),sK4(sK10(uri_owl_complementOf,X0)))
| iext(uri_rdfs_domain,uri_owl_complementOf,X0)
| iext(uri_owl_unionOf,sK10(uri_owl_complementOf,X0),uri_rdf_nil) ) ).
cnf(u1182,axiom,
iext(uri_rdf_type,X0,uri_rdfs_Resource) ).
cnf(u2861,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(u2856,axiom,
( icext(uri_owl_Restriction,sK9(uri_owl_someValuesFrom,X0))
| iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0) ) ).
cnf(u392,axiom,
iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List) ).
cnf(u712,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container) ) ).
cnf(u411,axiom,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype) ).
cnf(u2838,axiom,
( icext(sK10(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_domain,uri_owl_complementOf,X0)
| icext(sK9(uri_owl_complementOf,X0),X1) ) ).
cnf(u2719,axiom,
( icext(uri_rdf_List,sK14(uri_rdf_first,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0) ) ).
cnf(u507,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_ex_c)
| iext(uri_rdfs_subClassOf,X0,uri_ex_c1) ) ).
cnf(u2844,axiom,
( icext(sK10(uri_rdf_type,X0),sK9(uri_rdf_type,X0))
| iext(uri_rdfs_domain,uri_rdf_type,X0) ) ).
cnf(u2849,axiom,
( ~ iext(uri_owl_allValuesFrom,sK9(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_domain,uri_owl_onProperty,X0)
| ~ icext(X1,sK16(sK10(uri_owl_onProperty,X0),X1,X2))
| icext(sK9(uri_owl_onProperty,X0),X2) ) ).
cnf(u2092,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource) ).
cnf(u2616,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(u2966,axiom,
( ~ icext(sK9(uri_owl_complementOf,X0),sK13(sK10(uri_owl_complementOf,X0),X1))
| iext(uri_rdfs_domain,uri_owl_complementOf,X0)
| iext(uri_rdfs_subClassOf,sK10(uri_owl_complementOf,X0),X1) ) ).
cnf(u1972,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_List) ) ).
cnf(u2738,axiom,
( ~ icext(sK14(uri_rdfs_subClassOf,X0),X1)
| icext(sK15(uri_rdfs_subClassOf,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0) ) ).
cnf(u438,axiom,
( iext(uri_rdfs_subClassOf,X0,X0)
| ~ ic(X0) ) ).
cnf(u2744,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf_subject,X0) ).
cnf(u1467,axiom,
( ~ iext(uri_owl_intersectionOf,X0,uri_rdf_nil)
| icext(X0,X1) ) ).
cnf(u1853,axiom,
~ iext(uri_rdf_subject,X0,X1) ).
cnf(u2490,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(u2619,axiom,
( icext(uri_owl_Ontology,sK13(uri_owl_Ontology,X0))
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ) ).
cnf(u2749,axiom,
( icext(uri_ex_c1,sK15(uri_ex_p,X0))
| iext(uri_rdfs_subPropertyOf,uri_ex_p,X0) ) ).
cnf(u2900,axiom,
( iext(uri_rdf_type,sK10(uri_rdfs_label,X0),uri_rdfs_Literal)
| iext(uri_rdfs_domain,uri_rdfs_label,X0) ) ).
cnf(u2747,axiom,
( icext(uri_rdfs_Literal,sK15(uri_rdfs_label,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_label,X0) ) ).
cnf(u2919,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(u325,axiom,
( ~ iext(uri_owl_intersectionOf,X0,X1)
| icext(uri_rdf_List,X1) ) ).
cnf(u455,axiom,
iext(uri_rdfs_range,uri_ex_p,uri_ex_c1) ).
cnf(u348,axiom,
( ~ icext(X1,sK13(X0,X1))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u2382,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| ~ iext(uri_rdfs_subClassOf,X1,X0)
| iext(uri_rdfs_subClassOf,X1,uri_rdfs_Seq) ) ).
cnf(u607,axiom,
( ~ iext(uri_rdf_rest,X0,X1)
| icext(uri_rdf_List,X1) ) ).
cnf(u3033,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(u1644,axiom,
( ~ iext(uri_rdf_rest,X0,X1)
| icext(uri_rdf_List,X0) ) ).
cnf(u702,axiom,
icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1) ).
cnf(u2654,axiom,
( icext(sK12(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_range,uri_owl_complementOf,X0)
| icext(sK11(uri_owl_complementOf,X0),X1) ) ).
cnf(u367,axiom,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property) ).
cnf(u721,axiom,
icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral) ).
cnf(u2660,axiom,
( icext(sK12(uri_rdf_type,X0),sK11(uri_rdf_type,X0))
| iext(uri_rdfs_range,uri_rdf_type,X0) ) ).
cnf(u2677,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(u610,axiom,
( ~ icext(uri_rdf_Alt,X0)
| icext(uri_rdfs_Container,X0) ) ).
cnf(u1897,axiom,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
| iext(uri_rdfs_subPropertyOf,uri_rdf__1,X0) ) ).
cnf(u2675,axiom,
( ~ icext(sK11(uri_rdfs_subClassOf,X0),X1)
| icext(sK12(uri_rdfs_subClassOf,X0),X1)
| iext(uri_rdfs_range,uri_rdfs_subClassOf,X0) ) ).
cnf(u406,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty) ).
cnf(u365,axiom,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property) ).
cnf(u2906,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(u2678,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(u982,axiom,
( lv(sK13(uri_rdfs_Literal,X0))
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X0) ) ).
cnf(u2912,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(u2025,axiom,
icext(uri_rdfs_Class,X0) ).
cnf(u2684,axiom,
iext(uri_rdfs_range,uri_rdf_predicate,X0) ).
cnf(u988,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal) ) ).
cnf(u2160,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u2039,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class) ).
cnf(u3034,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(u2665,axiom,
( ~ iext(uri_owl_allValuesFrom,sK11(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_range,uri_owl_onProperty,X0)
| ~ icext(X1,sK16(sK12(uri_owl_onProperty,X0),X1,X2))
| icext(sK11(uri_owl_onProperty,X0),X2) ) ).
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(X6,X7)
| ~ icext(X0,X7)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u3040,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(u376,axiom,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property) ).
cnf(u2666,axiom,
( ~ iext(uri_owl_hasValue,sK11(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_range,uri_owl_onProperty,X0)
| iext(sK12(uri_owl_onProperty,X0),X2,X1)
| ~ icext(sK11(uri_owl_onProperty,X0),X2) ) ).
cnf(u2672,axiom,
( icext(uri_owl_Restriction,sK11(uri_owl_someValuesFrom,X0))
| iext(uri_rdfs_range,uri_owl_someValuesFrom,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(X6,X7)
| icext(X0,X7)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u2845,axiom,
( icext(uri_owl_Restriction,sK9(uri_owl_allValuesFrom,X0))
| iext(uri_rdfs_domain,uri_owl_allValuesFrom,X0) ) ).
cnf(u2840,axiom,
( icext(uri_rdf_List,sK9(uri_rdf_first,X0))
| iext(uri_rdfs_domain,uri_rdf_first,X0) ) ).
cnf(u382,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso) ).
cnf(u504,axiom,
( ~ iext(uri_ex_p,X0,X1)
| icext(uri_ex_c1,X1) ) ).
cnf(u2962,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(u2042,axiom,
( iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt)
| ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral) ) ).
cnf(u2067,axiom,
( iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral) ) ).
cnf(u2703,axiom,
( iext(uri_rdf_type,sK12(uri_rdfs_comment,X0),uri_rdfs_Literal)
| iext(uri_rdfs_range,uri_rdfs_comment,X0) ) ).
cnf(u2180,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK4(uri_rdfs_Class))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u289,axiom,
( ~ iext(uri_rdf_type,X0,uri_rdfs_Datatype)
| idc(X0) ) ).
cnf(u250,axiom,
( ~ ic(X0)
| icext(X0,sK4(X0))
| iext(uri_owl_unionOf,X0,uri_rdf_nil) ) ).
cnf(u2951,axiom,
( icext(sK12(uri_rdfs_domain,X0),sK9(sK11(uri_rdfs_domain,X0),X1))
| iext(uri_rdfs_range,uri_rdfs_domain,X0)
| iext(uri_rdfs_domain,sK11(uri_rdfs_domain,X0),X1) ) ).
cnf(u393,axiom,
iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List) ).
cnf(u2076,axiom,
( ~ iext(X1,sK14(X0,X1),sK15(X0,X1))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u294,axiom,
( ~ iodp(X0)
| ~ iext(X0,X1,X2)
| lv(X2) ) ).
cnf(u2950,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(u2847,axiom,
( ~ iext(uri_owl_allValuesFrom,sK9(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_domain,uri_owl_onProperty,X0)
| iext(sK10(uri_owl_onProperty,X0),X2,sK16(sK10(uri_owl_onProperty,X0),X1,X2))
| icext(sK9(uri_owl_onProperty,X0),X2) ) ).
cnf(u2177,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(u2956,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(u1954,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype) ) ).
cnf(u3121,axiom,
( iext(uri_rdfs_subClassOf,sK10(uri_owl_complementOf,X0),sK10(uri_owl_complementOf,X0))
| iext(uri_rdfs_domain,uri_owl_complementOf,X0) ) ).
cnf(u2961,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(u422,axiom,
( ~ lv(X0)
| icext(uri_rdfs_Literal,X0) ) ).
cnf(u2728,axiom,
( ~ iext(uri_owl_allValuesFrom,sK14(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0)
| ~ icext(X1,sK16(sK15(uri_owl_onProperty,X0),X1,X2))
| icext(sK14(uri_owl_onProperty,X0),X2) ) ).
cnf(u2975,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(u694,axiom,
( icext(uri_rdfs_Container,sK13(uri_rdf_Alt,X0))
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0) ) ).
cnf(u1837,axiom,
~ iext(uri_rdf_predicate,X0,X1) ).
cnf(u311,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_Ontology)
| ix(X0) ) ).
cnf(u2467,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u1442,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member) ).
cnf(u2733,axiom,
( ~ iext(uri_owl_onProperty,sK14(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0)
| iext(X1,X2,sK17(X1,sK15(uri_owl_someValuesFrom,X0),X2))
| ~ icext(sK14(uri_owl_someValuesFrom,X0),X2) ) ).
cnf(u439,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| ~ iext(uri_rdfs_subClassOf,X0,X1)
| iext(uri_rdfs_subClassOf,X0,X2) ) ).
cnf(u2884,axiom,
iext(uri_rdfs_domain,uri_owl_hasValue,uri_owl_Restriction) ).
cnf(u2731,axiom,
( icext(uri_owl_Restriction,sK14(uri_owl_onProperty,X0))
| iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0) ) ).
cnf(u2366,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| ~ icext(X0,X1) ) ).
cnf(u2686,axiom,
( iext(uri_rdfs_member,sK11(sK4(uri_rdfs_ContainerMembershipProperty),X0),sK12(sK4(uri_rdfs_ContainerMembershipProperty),X0))
| iext(uri_rdfs_range,sK4(uri_rdfs_ContainerMembershipProperty),X0) ) ).
cnf(u1983,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Resource,uri_rdf_nil) ).
cnf(u332,axiom,
( ~ iext(uri_owl_someValuesFrom,X0,X1)
| icext(uri_owl_Restriction,X0) ) ).
cnf(u457,axiom,
iext(uri_rdf_type,uri_ex_w,uri_ex_c1) ).
cnf(u2661,axiom,
( icext(uri_owl_Restriction,sK11(uri_owl_allValuesFrom,X0))
| iext(uri_rdfs_range,uri_owl_allValuesFrom,X0) ) ).
cnf(u2659,axiom,
( icext(uri_rdf_List,sK12(uri_owl_unionOf,X0))
| iext(uri_rdfs_range,uri_owl_unionOf,X0) ) ).
cnf(u349,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,X1)
| icext(X1,X2)
| ~ icext(X0,X2) ) ).
cnf(u2890,axiom,
iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_owl_Restriction) ).
cnf(u2772,axiom,
( ~ iext(uri_rdf__3,sK14(X0,uri_rdfs_member),sK15(X0,uri_rdfs_member))
| iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member) ) ).
cnf(u2662,axiom,
( icext(uri_owl_Restriction,sK11(uri_owl_hasValue,X0))
| iext(uri_rdfs_range,uri_owl_hasValue,X0) ) ).
cnf(u2896,axiom,
( lv(sK10(uri_rdfs_comment,X0))
| iext(uri_rdfs_domain,uri_rdfs_comment,X0) ) ).
cnf(u2668,axiom,
( icext(uri_owl_Restriction,sK11(uri_owl_onProperty,X0))
| iext(uri_rdfs_range,uri_owl_onProperty,X0) ) ).
cnf(u339,axiom,
( ~ iext(uri_rdfs_domain,X0,X1)
| icext(X1,X2)
| ~ iext(X0,X2,X3) ) ).
cnf(u2149,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Resource) ).
cnf(u362,axiom,
( ~ iext(uri_owl_someValuesFrom,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| icext(X2,sK17(X1,X2,X3))
| ~ icext(X0,X3) ) ).
cnf(u707,axiom,
icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3) ).
cnf(u2663,axiom,
( ~ iext(uri_owl_allValuesFrom,sK11(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_range,uri_owl_onProperty,X0)
| iext(sK12(uri_owl_onProperty,X0),X2,sK16(sK12(uri_owl_onProperty,X0),X1,X2))
| icext(sK11(uri_owl_onProperty,X0),X2) ) ).
cnf(u3105,axiom,
( iext(uri_rdfs_subClassOf,sK12(uri_owl_complementOf,X0),sK12(uri_owl_complementOf,X0))
| iext(uri_rdfs_range,uri_owl_complementOf,X0) ) ).
cnf(u360,axiom,
( ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_hasValue,X0,X2)
| ~ iext(X1,X3,X2)
| icext(X0,X3) ) ).
cnf(u1900,axiom,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
| iext(uri_rdfs_subPropertyOf,sK4(uri_rdfs_ContainerMembershipProperty),X0) ) ).
cnf(u2656,axiom,
( icext(uri_rdf_List,sK11(uri_rdf_first,X0))
| iext(uri_rdfs_range,uri_rdf_first,X0) ) ).
cnf(u1898,axiom,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
| iext(uri_rdfs_subPropertyOf,uri_rdf__2,X0) ) ).
cnf(u2673,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(u379,axiom,
iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal) ).
cnf(u366,axiom,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List) ).
cnf(u2687,axiom,
iext(uri_rdfs_range,uri_rdf_object,X0) ).
cnf(u2301,axiom,
iext(uri_rdfs_subClassOf,uri_owl_AnnotationProperty,X0) ).
cnf(u2946,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(u239,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(u2051,axiom,
( iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag)
| ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral) ) ).
cnf(u2032,axiom,
ic(X0) ).
cnf(u2306,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_OntologyProperty)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u1409,axiom,
( iext(uri_rdfs_subClassOf,sK13(uri_rdfs_Datatype,X0),uri_rdfs_Literal)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0)
| ~ ic(X0) ) ).
cnf(u2078,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement) ) ).
cnf(u2578,axiom,
iext(uri_rdfs_domain,X0,uri_owl_Thing) ).
cnf(u278,axiom,
~ icext(uri_owl_Nothing,X0) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB007+3 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n002.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 06:58:52 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 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
% 0.94/0.62 % (172374)Will run a generic schedule for satisfiability detection.
% 0.94/0.62 % (172382)dis+10_1_sil=32000:sp=arity:random_seed=4287290817:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.94/0.62 % (172380)% WARNING: option uhcvi not known.
% 0.94/0.62 % (172381)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3739624517:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.94/0.62 % (172379)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1445486362_2999 on theBenchmark for (2999ds/0Mi)
% 0.94/0.62 % (172383)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=357606705:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.94/0.62 % (172380)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2973216935:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.94/0.62 % (172385)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2030023476:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.94/0.62 % (172384)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4103843387:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.94/0.62 % TRYING [1]
% 0.94/0.62 % TRYING [2]
% 0.94/0.62 % TRYING [3]
% 0.94/0.62 % (172382)Instruction limit reached!
% 0.94/0.62 % (172382)------------------------------
% 0.94/0.62 % (172382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.62 % (172382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.62 % (172382)CaDiCaL version: 2.1.3
% 0.94/0.62 % (172382)Termination reason: Instruction limit
% 0.94/0.62 % (172382)Termination phase: Saturation
% 0.94/0.62 % (172382)Time elapsed: 0.034 s
% 0.94/0.62 % (172382)Peak memory usage: 13 MB
% 0.94/0.62 % (172382)Instructions burned: 104 (million)
% 0.94/0.62 % (172393)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1473716852:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.94/0.62 % TRYING [1]
% 0.94/0.62 % TRYING [2]
% 0.94/0.62 % TRYING [3]
% 0.94/0.62 % (172383)Instruction limit reached!
% 0.94/0.62 % (172383)------------------------------
% 0.94/0.62 % (172383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.62 % (172383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.62 % (172383)CaDiCaL version: 2.1.3
% 0.94/0.62 % (172383)Termination reason: Instruction limit
% 0.94/0.62 % (172383)Termination phase: Saturation
% 0.94/0.62 % (172383)Time elapsed: 0.049 s
% 0.94/0.62 % (172383)Peak memory usage: 11 MB
% 0.94/0.62 % (172383)Instructions burned: 117 (million)
% 0.94/0.62 % TRYING [4]
% 0.94/0.62 % TRYING [4]
% 0.94/0.62 % (172395)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3592620734:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.94/0.62 % (172384)Instruction limit reached!
% 0.94/0.62 % (172384)------------------------------
% 0.94/0.62 % (172384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.62 % (172384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.62 % (172384)CaDiCaL version: 2.1.3
% 0.94/0.62 % (172384)Termination reason: Instruction limit
% 0.94/0.62 % (172384)Termination phase: Saturation
% 0.94/0.62 % (172384)Time elapsed: 0.068 s
% 0.94/0.62 % (172384)Peak memory usage: 13 MB
% 0.94/0.62 % (172384)Instructions burned: 132 (million)
% 0.94/0.62 % (172397)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=3025514872:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.94/0.62 % (172385)Instruction limit reached!
% 0.94/0.62 % (172385)------------------------------
% 0.94/0.62 % (172385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.62 % (172385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.62 % (172385)CaDiCaL version: 2.1.3
% 0.94/0.62 % (172385)Termination reason: Instruction limit
% 0.94/0.62 % (172385)Termination phase: Saturation
% 0.94/0.62 % (172385)Time elapsed: 0.097 s
% 0.94/0.62 % (172385)Peak memory usage: 14 MB
% 0.94/0.62 % (172385)Instructions burned: 159 (million)
% 0.94/0.62 % (172399)ott-21_1_sil=16000:fs=off:random_seed=3026559971:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.94/0.62 % (172395)Instruction limit reached!
% 0.94/0.62 % (172395)------------------------------
% 0.94/0.62 % (172395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.62 % (172395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.62 % (172395)CaDiCaL version: 2.1.3
% 0.94/0.62 % (172395)Termination reason: Instruction limit
% 0.94/0.62 % (172395)Termination phase: Saturation
% 0.94/0.62 % (172395)Time elapsed: 0.064 s
% 0.94/0.62 % (172395)Peak memory usage: 13 MB
% 0.94/0.62 % (172395)Instructions burned: 133 (million)
% 0.94/0.62 % (172401)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1837622081:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 0.94/0.62 % (172397) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-172374-172397"...
% 0.94/0.62 % (172397)...printing done.
% 0.94/0.62 % SZS status CounterSatisfiable for theBenchmark
% 0.94/0.62 % SZS output start Saturation.
% See solution above
% 0.94/0.63 % SZS output start Definitions and Model Updates.
% 0.94/0.63 for all groundings,
% 0.94/0.63 whenever iext(uri_rdf_type,X0,uri_rdfs_Datatype) is false, set ~idc(X0) to true
% 0.94/0.63 for all groundings,
% 0.94/0.63 whenever iext(uri_rdf_type,X0,uri_owl_AnnotationProperty) is false, set ~ioap(X0) to true
% 0.94/0.63 for all groundings,
% 0.94/0.63 whenever iext(uri_rdf_type,X0,uri_owl_DatatypeProperty) is false, set ~iodp(X0) to true
% 0.94/0.63 for all groundings,
% 0.94/0.63 whenever iext(uri_rdf_type,X0,uri_owl_OntologyProperty) is false, set ~ioxp(X0) to true
% 0.94/0.63 % SZS output end Definitions and Model Updates.
% 0.94/0.63 % (172397)------------------------------
% 0.94/0.63 % (172397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.63 % (172397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.63 % (172397)CaDiCaL version: 2.1.3
% 0.94/0.63 % (172397)Termination reason: Satisfiable
% 0.94/0.63 % (172397)Time elapsed: 0.065 s
% 0.94/0.63 % (172397)Peak memory usage: 14 MB
% 0.94/0.63 % (172397)Instructions burned: 98 (million)
% 0.94/0.63 % (172374)Success in time 0.195 s
% 0.94/0.63 % Vampire exiting
%------------------------------------------------------------------------------