Vampire---5.0.1.SAT-Sat.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : SWB018-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n009.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:06 PM UTC 2026

% Result   : Satisfiable 8.59s 2.09s
% Output   : Saturation 9.15s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u5661,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_Alt,uri_rdfs_Resource),true,true,true),true) ).

cnf(u2584,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,true,true) ).

cnf(u248,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Datatype),true,true,true),true) ).

cnf(u1415,axiom,
    true = iext(uri_rdf_type,uri_ex_w,uri_ex_Person) ).

cnf(u5282,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,uri_rdf_Property),true,true,true) ).

cnf(u2276,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Seq,X1),true,true,true),true) ).

cnf(u1940,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf__1),true,true,true),true) ).

cnf(u2075,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Statement,uri_rdfs_Class),true) ).

cnf(u550,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_value,uri_rdfs_Resource),true) ).

cnf(u1788,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_object,X0),true,true,true) ).

cnf(u1019,axiom,
    true = ifeq(iext(uri_rdf__3,X0,X1),true,true,true) ).

cnf(u1544,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_value,X0),true,true,true) ).

cnf(u21,axiom,
    true = iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property) ).

cnf(u1877,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_value,X1),true,true,true),true) ).

cnf(u151,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,X1),true,ic(X0),true) ).

cnf(u2544,axiom,
    true = ifeq(ip(uri_rdfs_member),true,true,true) ).

cnf(u2328,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_Property,X1),true,true,true),true) ).

cnf(u2945,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_List),true) ).

cnf(u5772,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Seq,uri_rdfs_Resource),true,true,true),true) ).

cnf(u2323,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,true,true) ).

cnf(u406,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_Resource),true) ).

cnf(u4263,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_isDefinedBy),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_isDefinedBy),true) ).

cnf(u1664,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_domain,uri_rdf_Property),true) ).

cnf(u1298,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_ex_Person),true,true,true) ).

cnf(u1681,axiom,
    true = ifeq(icext(X0,uri_rdf__2),true,true,true) ).

cnf(u2203,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0),true,true,true) ).

cnf(u678,axiom,
    true = icext(uri_rdf_Property,uri_rdf_object) ).

cnf(u149,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,X1),true,ic(X1),true) ).

cnf(u912,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Container),true) ).

cnf(u1196,axiom,
    true = icext(uri_rdfs_Class,uri_rdfs_Class) ).

cnf(u1570,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty),true,true,true) ).

cnf(u2089,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement) ).

cnf(u5585,axiom,
    true = ifeq(icext(uri_rdfs_Literal,X0),true,true,true) ).

cnf(u4618,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_value,uri_rdf_value),true) ).

cnf(u4624,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_value,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf_value,X0),true) ).

cnf(u1160,axiom,
    true = icext(uri_rdf_Property,uri_rdfs_subPropertyOf) ).

cnf(u1694,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Resource,X1),true,true,true),true) ).

cnf(u5611,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,X0),true) ).

cnf(u1576,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_ContainerMembershipProperty),true,true,true),true) ).

cnf(u479,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_value),true) ).

cnf(u931,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Alt,uri_rdfs_Container),true) ).

cnf(u61,axiom,
    true = iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource) ).

cnf(u824,axiom,
    true = ip(uri_owl_sameAs) ).

cnf(u293,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u1839,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_label),true,true,true),true) ).

cnf(u1698,axiom,
    true = ic(uri_rdfs_Resource) ).

cnf(u561,axiom,
    true = ifeq(iext(uri_rdf__2,X0,X1),true,icext(uri_rdfs_Resource,X1),true) ).

cnf(u1947,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,true,true) ).

cnf(u2350,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Class),true,true,true),true) ).

cnf(u3023,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_label),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_label),true) ).

cnf(u51,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource) ).

cnf(u5721,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf__1,X0),true) ).

cnf(u5142,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__3),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdf__3),true) ).

cnf(u5782,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,X0),true) ).

cnf(u1637,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_rest),true,true,true),true) ).

cnf(u306,axiom,
    true = ifeq(ip(uri_rdf__1),true,true,true) ).

cnf(u689,axiom,
    true = icext(uri_rdf_Property,uri_rdf_type) ).

cnf(u444,axiom,
    true = ifeq(iext(uri_rdfs_label,X0,X1),true,icext(uri_rdfs_Resource,X0),true) ).

cnf(u3259,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true) ).

cnf(u2583,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,true,true) ).

cnf(u1466,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_owl_sameAs,X0),true,true,true) ).

cnf(u2826,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_subPropertyOf),true,true,true),true) ).

cnf(u1778,axiom,
    true = ifeq(icext(X0,uri_rdf_subject),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,true,true),true) ).

cnf(u828,axiom,
    true = ip(uri_rdfs_range) ).

cnf(u179,axiom,
    true = iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource) ).

cnf(u5030,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true) ).

cnf(u3750,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Literal,uri_rdfs_Literal),true,true,true),true) ).

cnf(u2539,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_member),true,true,true),true) ).

cnf(u434,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_range),true) ).

cnf(u1209,axiom,
    true = icext(uri_rdfs_Class,uri_rdf_List) ).

cnf(u5143,axiom,
    true = ifeq(iext(uri_rdf__3,X0,X1),true,iext(uri_rdf__3,X0,X1),true) ).

cnf(u5381,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Datatype),true) ).

cnf(u950,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Seq),true) ).

cnf(u5418,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_subClassOf,uri_rdfs_subClassOf),true,true,true),true) ).

cnf(u1464,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_sameAs,X0),true,true,true) ).

cnf(u578,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u2171,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Bag),true,true,true) ).

cnf(u5295,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,uri_ex_Person),true,true,true) ).

cnf(u3754,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Literal,uri_rdfs_Literal),true) ).

cnf(u177,axiom,
    true = iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource) ).

cnf(u5807,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Property,uri_rdfs_Resource),true) ).

cnf(u5197,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_Alt,uri_rdf_Alt),true,true,true),true) ).

cnf(u2145,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdf_XMLLiteral),true,true,true),true) ).

cnf(u2942,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_List,uri_rdf_List),true,true,true),true) ).

cnf(u3760,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X0),true) ).

cnf(u2903,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Statement),true) ).

cnf(u1987,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,X0),true,true,true) ).

cnf(u4445,axiom,
    true = ifeq(iext(uri_rdf_object,X0,X1),true,iext(uri_rdf_object,X0,X1),true) ).

cnf(u596,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_subject),true) ).

cnf(u3104,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Statement,uri_rdfs_Resource),true) ).

cnf(u5201,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Alt,uri_rdf_Alt),true) ).

cnf(u1372,axiom,
    true = icext(uri_rdfs_Class,uri_rdf_Bag) ).

cnf(u91,axiom,
    true = iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty) ).

cnf(u323,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_label,uri_rdfs_Literal),true,true,true),true) ).

cnf(u461,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u712,axiom,
    true = ip(uri_rdf_object) ).

cnf(u346,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_member),true) ).

cnf(u3586,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_first),true) ).

cnf(u3126,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_List,uri_rdfs_Resource),true,true,true),true) ).

cnf(u4203,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u204,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdfs_Datatype),true) ).

cnf(u2682,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u2178,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdf_Bag),true,true,true),true) ).

cnf(u1096,axiom,
    true = ifeq(iext(uri_rdfs_member,X0,X1),true,true,true) ).

cnf(u975,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Resource),true,ifeq(iext(X0,X1,X2),true,true,true),true) ).

cnf(u2898,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Statement,uri_rdfs_Statement),true,true,true),true) ).

cnf(u89,axiom,
    true = iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource) ).

cnf(u1500,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,true,true) ).

cnf(u3137,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_List),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u451,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_comment,uri_rdfs_Resource),true) ).

cnf(u1878,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_value),true,true,true),true) ).

cnf(u1299,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_ex_Person),true,true,true) ).

cnf(u2202,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Alt),true,true,true) ).

cnf(u5087,axiom,
    true = ifeq(iext(uri_rdf__2,X0,X1),true,iext(uri_rdf__2,X0,X1),true) ).

cnf(u474,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf_value,uri_rdfs_Resource),true,true,true),true) ).

cnf(u2100,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf__2),true,true,true),true) ).

cnf(u5675,axiom,
    true = ifeq(icext(uri_rdf_Alt,X0),true,true,true) ).

cnf(u1884,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_comment,X0),true,true,true) ).

cnf(u1235,axiom,
    true = icext(uri_rdf_Property,uri_owl_sameAs) ).

cnf(u5631,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_Bag,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1993,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_isDefinedBy,X1),true,true,true),true) ).

cnf(u95,axiom,
    true = iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty) ).

cnf(u2464,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property) ).

cnf(u363,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_subClassOf,uri_rdfs_Class),true) ).

cnf(u716,axiom,
    true = ip(uri_rdf_rest) ).

cnf(u350,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_domain,uri_rdfs_Class),true,true,true),true) ).

cnf(u733,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,true,true),true) ).

cnf(u1001,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,X0),true,icext(uri_rdf_Property,X0),true) ).

cnf(u1487,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_owl_sameAs,uri_rdf_Property),true) ).

cnf(u1625,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u731,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,X0),true) ).

cnf(u622,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_predicate,uri_rdfs_Resource),true) ).

cnf(u4725,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_range),true) ).

cnf(u3164,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_owl_sameAs,uri_owl_sameAs),true,true,true),true) ).

cnf(u2431,axiom,
    true = ifeq(icext(X0,uri_rdf_XMLLiteral),true,true,true) ).

cnf(u1639,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u2481,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource) ).

cnf(u2540,axiom,
    true = iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property) ).

cnf(u4734,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,X1),true,iext(uri_rdfs_range,X0,X1),true) ).

cnf(u1631,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_rest,X0),true,true,true) ).

cnf(u256,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u478,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_value,uri_rdfs_Resource),true) ).

cnf(u2533,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_member,X0),true,true,true) ).

cnf(u3043,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_comment),true) ).

cnf(u234,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_type,uri_rdf_Property),true,true,true),true) ).

cnf(u1521,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,uri_rdf_nil),true,true,true),true) ).

cnf(u515,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

cnf(u2062,axiom,
    true = iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class) ).

cnf(u1949,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_List),true,true,true) ).

cnf(u5883,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf__2,X0),true) ).

cnf(u2345,axiom,
    true = ifeq(icext(X0,uri_rdfs_Class),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true,true,true),true) ).

cnf(u5023,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_type,uri_rdf_type),true) ).

cnf(u5908,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Datatype,uri_rdfs_Resource),true) ).

cnf(u1642,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,true,true) ).

cnf(u489,axiom,
    true = ifeq(iext(uri_rdfs_seeAlso,X0,X1),true,icext(uri_rdfs_Resource,X0),true) ).

cnf(u2172,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag),true,true,true) ).

cnf(u262,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_first,uri_rdf_Property),true) ).

cnf(u645,axiom,
    true = ifeq(icext(uri_rdf_Property,uri_rdf_object),true,true,true) ).

cnf(u2568,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member) ).

cnf(u1005,axiom,
    true = ifeq(iext(uri_rdf_first,X0,X1),true,true,true) ).

cnf(u1648,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_domain,X1),true,true,true),true) ).

cnf(u5754,axiom,
    true = ifeq(icext(uri_rdfs_Container,X0),true,true,true) ).

cnf(u1106,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Statement),true,true,true) ).

cnf(u643,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3),true,true,true) ).

cnf(u534,axiom,
    true = ifeq(iext(uri_rdf__3,X0,X1),true,icext(uri_rdfs_Resource,X1),true) ).

cnf(u1790,axiom,
    true = ifeq(icext(X0,uri_rdf_object),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,true,true),true) ).

cnf(u1003,axiom,
    true = ifeq(icext(uri_rdf_Alt,X0),true,icext(uri_rdfs_Container,X0),true) ).

cnf(u1789,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_object,X0),true,true,true) ).

cnf(u2979,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,X0),true) ).

cnf(u1404,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_type,X1),true,true,true),true) ).

cnf(u2314,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype) ).

cnf(u2365,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Class,uri_rdfs_Class),true) ).

cnf(u495,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_List),true) ).

cnf(u633,axiom,
    true = ifeq(iext(uri_owl_sameAs,X0,X1),true,icext(uri_ex_Person,X0),true) ).

cnf(u260,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_nil,uri_rdf_List),true) ).

cnf(u390,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_sameAs,X0),true,icext(X0,uri_ex_w),true) ).

cnf(u2125,axiom,
    true = ifeq(icext(X0,uri_rdf__3),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,true,true),true) ).

cnf(u1989,axiom,
    true = ifeq(icext(X0,uri_rdfs_isDefinedBy),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,true,true),true) ).

cnf(u1776,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_subject,X0),true,true,true) ).

cnf(u519,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf_subject,uri_rdfs_Statement),true,true,true),true) ).

cnf(u4617,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_value),true) ).

cnf(u133,axiom,
    true = iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement) ).

cnf(u896,axiom,
    true = ifeq(iext(uri_rdfs_isDefinedBy,X0,X1),true,iext(uri_rdfs_seeAlso,X0,X1),true) ).

cnf(u279,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,icext(X0,uri_rdf_XMLLiteral),true) ).

cnf(u2442,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral) ).

cnf(u1571,axiom,
    true = ifeq(icext(X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true,true,true),true) ).

cnf(u761,axiom,
    true = ic(uri_rdfs_Class) ).

cnf(u388,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_owl_sameAs,X0),true,icext(X0,uri_ex_u),true) ).

cnf(u1678,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,X1,uri_rdf__2),true,true,true),true) ).

cnf(u917,axiom,
    true = ic(uri_rdf_Bag) ).

cnf(u1560,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf__3,X0),true,true,true) ).

cnf(u3111,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u1577,axiom,
    true = iext(uri_rdf_type,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class) ).

cnf(u2063,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Statement),true) ).

cnf(u522,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_Statement),true) ).

cnf(u1809,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_range),true) ).

cnf(u4500,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_seeAlso,uri_rdfs_seeAlso),true,true,true),true) ).

cnf(u2331,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_Property),true) ).

cnf(u2974,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_predicate),true) ).

cnf(u45,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource) ).

cnf(u1933,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf__1,X0),true,true,true) ).

cnf(u528,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf__3,uri_rdfs_Resource),true,true,true),true) ).

cnf(u407,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

cnf(u1682,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member) ).

cnf(u3361,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_member),true) ).

cnf(u300,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_type,uri_rdfs_Class),true) ).

cnf(u5430,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,X1),true,iext(uri_rdfs_subClassOf,X0,X1),true) ).

cnf(u1688,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Resource),true,true,true) ).

cnf(u559,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf__2,uri_rdfs_Resource),true) ).

cnf(u1408,axiom,
    true = ifeq(iext(uri_owl_sameAs,uri_ex_w,X0),true,true,true) ).

cnf(u2268,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Seq),true,true,true) ).

cnf(u2604,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_subClassOf,uri_rdf_Property),true,true,true),true) ).

cnf(u1316,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_ex_Person),true,true,true) ).

cnf(u35,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource) ).

cnf(u173,axiom,
    true = iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource) ).

cnf(u2352,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u319,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u1192,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,uri_rdfs_Class),true,true,true) ).

cnf(u656,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_subPropertyOf),true) ).

cnf(u290,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,icext(X0,uri_rdf_nil),true) ).

cnf(u673,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,true,true) ).

cnf(u1843,axiom,
    true = ifeq(ip(uri_rdfs_label),true,true,true) ).

cnf(u246,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_value,uri_rdf_Property),true,true,true),true) ).

cnf(u2462,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdfs_Resource) ).

cnf(u3049,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_comment),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_comment),true) ).

cnf(u687,axiom,
    true = icext(uri_rdfs_Class,uri_rdf_Property) ).

cnf(u4665,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf__1,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf__1,X0),true) ).

cnf(u5273,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true) ).

cnf(u163,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,ip(X0),true) ).

cnf(u317,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u568,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_first,uri_rdfs_Resource),true) ).

cnf(u447,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_comment,uri_rdfs_Resource),true,true,true),true) ).

cnf(u2973,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_predicate,uri_rdf_predicate),true) ).

cnf(u5031,axiom,
    true = ifeq(iext(uri_rdf_type,X0,X1),true,iext(uri_rdf_type,X0,X1),true) ).

cnf(u5162,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Bag),true) ).

cnf(u2473,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container) ).

cnf(u5556,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,X0),true,true,true) ).

cnf(u5776,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Seq,uri_rdfs_Resource),true) ).

cnf(u5286,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,uri_rdf_Alt),true,true,true) ).

cnf(u2132,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf__3),true) ).

cnf(u1695,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Resource),true,true,true),true) ).

cnf(u161,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,ip(X1),true) ).

cnf(u307,axiom,
    true = ifeq(ip(uri_rdf__2),true,true,true) ).

cnf(u5392,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,X0),true,icext(uri_rdfs_Datatype,X0),true) ).

cnf(u696,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Literal),true) ).

cnf(u2592,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_subClassOf),true,true,true),true) ).

cnf(u416,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

cnf(u5813,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true) ).

cnf(u3761,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal),true) ).

cnf(u188,axiom,
    true = ifeq(true,true,icext(uri_rdfs_Resource,X0),true) ).

cnf(u2523,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Literal,uri_rdfs_Class),true) ).

cnf(u2829,axiom,
    true = ifeq(icext(X0,uri_rdfs_subPropertyOf),true,true,true) ).

cnf(u2129,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf__3,X1),true,true,true),true) ).

cnf(u75,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource) ).

cnf(u2271,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq),true,true,true) ).

cnf(u4667,axiom,
    true = ifeq(iext(uri_rdf__1,X0,X1),true,iext(uri_rdf__1,X0,X1),true) ).

cnf(u2679,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_ex_Person,uri_rdfs_Resource),true,true,true),true) ).

cnf(u5971,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf__3,X0),true) ).

cnf(u1465,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_sameAs,X0),true,true,true) ).

cnf(u846,axiom,
    true = ip(uri_rdfs_domain) ).

cnf(u4437,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_object,uri_rdf_object),true) ).

cnf(u2403,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_Datatype,uri_rdfs_Class),true,true,true),true) ).

cnf(u73,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property) ).

cnf(u4965,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,uri_rdfs_comment),true,true,true) ).

cnf(u5605,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Resource),true) ).

cnf(u4264,axiom,
    true = ifeq(iext(uri_rdfs_isDefinedBy,X0,X1),true,iext(uri_rdfs_isDefinedBy,X0,X1),true) ).

cnf(u2245,axiom,
    true = iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class) ).

cnf(u328,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_label),true) ).

cnf(u2391,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Datatype),true,true,true),true) ).

cnf(u1868,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label) ).

cnf(u587,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_predicate),true) ).

cnf(u3790,axiom,
    true = ifeq(iext(uri_rdf_rest,X0,X1),true,iext(uri_rdf_rest,X0,X1),true) ).

cnf(u1373,axiom,
    true = icext(uri_rdfs_Class,uri_rdf_Alt) ).

cnf(u4973,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,uri_rdf_predicate),true,true,true) ).

cnf(u2624,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy) ).

cnf(u79,axiom,
    true = iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource) ).

cnf(u347,axiom,
    true = ifeq(iext(uri_rdfs_member,X0,X1),true,icext(uri_rdfs_Resource,X0),true) ).

cnf(u5086,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__2),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdf__2),true) ).

cnf(u2246,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Container),true) ).

cnf(u717,axiom,
    true = ip(uri_rdf_first) ).

cnf(u456,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf__1,uri_rdfs_Resource),true,true,true),true) ).

cnf(u5079,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__2,uri_rdf__2),true) ).

cnf(u415,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_subClassOf,uri_rdfs_Class),true) ).

cnf(u985,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u1131,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Statement),true,true,true) ).

cnf(u1609,axiom,
    true = ifeq(icext(X0,uri_rdf_first),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,true,true),true) ).

cnf(u1996,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

cnf(u715,axiom,
    true = ip(uri_rdf__1) ).

cnf(u606,axiom,
    true = ifeq(iext(uri_rdf_object,X0,X1),true,icext(uri_rdfs_Statement,X0),true) ).

cnf(u2269,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Seq,X0),true,true,true) ).

cnf(u999,axiom,
    true = ifeq(icext(uri_rdf_XMLLiteral,X0),true,icext(uri_rdfs_Literal,X0),true) ).

cnf(u3042,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_comment,uri_rdfs_comment),true) ).

cnf(u5463,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Class,uri_rdfs_Class),true) ).

cnf(u1994,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_isDefinedBy),true,true,true),true) ).

cnf(u345,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_member,uri_rdfs_Resource),true) ).

cnf(u612,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_range,X0),true,icext(X0,uri_rdf_List),true) ).

cnf(u2147,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_XMLLiteral),true) ).

cnf(u1547,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value) ).

cnf(u368,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_range,uri_rdfs_Class),true,true,true),true) ).

cnf(u462,axiom,
    true = ifeq(iext(uri_rdf__1,X0,X1),true,icext(uri_rdfs_Resource,X0),true) ).

cnf(u766,axiom,
    true = icext(uri_rdfs_Resource,X0) ).

cnf(u1587,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),true,true,true),true) ).

cnf(u1800,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,true,true) ).

cnf(u627,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_owl_sameAs,uri_ex_Person),true,true,true),true) ).

cnf(u1737,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_predicate,X0),true,true,true) ).

cnf(u2908,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Statement,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,X0),true) ).

cnf(u5723,axiom,
    true = ifeq(iext(uri_rdf__1,X0,X1),true,iext(uri_rdfs_member,X0,X1),true) ).

cnf(u3174,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_sameAs,X0),true,iext(uri_rdfs_subPropertyOf,uri_owl_sameAs,X0),true) ).

cnf(u1536,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_object,X0),true,true,true) ).

cnf(u968,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,true,true) ).

cnf(u3167,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_owl_sameAs),true) ).

cnf(u1626,axiom,
    true = ifeq(icext(X0,uri_rdf__1),true,true,true) ).

cnf(u2156,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Class),true,true,true),true) ).

cnf(u1643,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,X0),true,true,true) ).

cnf(u374,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,X1),true,icext(uri_rdfs_Class,X1),true) ).

cnf(u1882,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,X0),true,true,true) ).

cnf(u5268,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_subPropertyOf),true) ).

cnf(u216,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u648,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),true,true,true) ).

cnf(u2530,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true,true,true) ).

cnf(u5242,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true) ).

cnf(u4732,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true) ).

cnf(u755,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Datatype,uri_rdfs_Class),true,true,true),true) ).

cnf(u987,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,icext(X0,X1),true) ).

cnf(u2541,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_member),true) ).

cnf(u5744,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Container,uri_rdfs_Resource),true) ).

cnf(u247,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_subject,uri_rdf_Property),true,true,true),true) ).

cnf(u257,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__1,uri_rdf_Property),true) ).

cnf(u524,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_subject),true) ).

cnf(u443,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_label),true) ).

cnf(u372,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_range,uri_rdfs_Class),true) ).

cnf(u4364,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_subject,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,X0),true) ).

cnf(u5885,axiom,
    true = ifeq(iext(uri_rdf__2,X0,X1),true,iext(uri_rdfs_member,X0,X1),true) ).

cnf(u631,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_owl_sameAs,uri_ex_Person),true) ).

cnf(u1002,axiom,
    true = ifeq(icext(uri_rdf_Bag,X0),true,icext(uri_rdfs_Container,X0),true) ).

cnf(u1388,axiom,
    true = icext(uri_rdfs_Class,uri_rdfs_Container) ).

cnf(u2299,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,X1),true,true,true) ).

cnf(u646,axiom,
    true = ifeq(icext(uri_rdf_Property,uri_rdf_value),true,true,true) ).

cnf(u5294,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,uri_rdfs_Statement),true,true,true) ).

cnf(u935,axiom,
    true = ic(uri_rdf_Alt) ).

cnf(u245,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_object,uri_rdf_Property),true,true,true),true) ).

cnf(u263,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_type,uri_rdf_Property),true) ).

cnf(u5114,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral),true,iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral),true) ).

cnf(u385,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_sameAs),true,ifeq(iext(X0,uri_ex_w,uri_ex_u),true,true,true),true) ).

cnf(u1555,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1) ).

cnf(u745,axiom,
    true = ic(uri_rdf_Property) ).

cnf(u2683,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_ex_Person,uri_rdfs_Resource),true) ).

cnf(u5382,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Datatype,uri_rdfs_Datatype),true) ).

cnf(u2312,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource) ).

cnf(u2140,axiom,
    true = ifeq(icext(X0,uri_rdf_XMLLiteral),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true,true,true),true) ).

cnf(u4357,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_subject),true) ).

cnf(u759,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Datatype,uri_rdfs_Class),true) ).

cnf(u634,axiom,
    true = ifeq(icext(uri_rdf_Property,uri_rdf_type),true,true,true) ).

cnf(u1405,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_type),true,true,true),true) ).

cnf(u899,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_isDefinedBy),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_seeAlso),true) ).

cnf(u2509,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Literal),true) ).

cnf(u29,axiom,
    true = ifeq(iext(uri_rdf_type,X0,uri_rdf_Property),true,ip(X0),true) ).

cnf(u261,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_Property,uri_rdfs_Class),true) ).

cnf(u1807,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_range),true,true,true),true) ).

cnf(u4354,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf_subject,uri_rdf_subject),true,true,true),true) ).

cnf(u1683,axiom,
    true = ifeq(ic(uri_rdfs_Resource),true,true,true) ).

cnf(u4365,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_subject),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdf_subject),true) ).

cnf(u2440,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource) ).

cnf(u543,axiom,
    true = ifeq(iext(uri_rdf__1,X0,X1),true,icext(uri_rdfs_Resource,X1),true) ).

cnf(u1306,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_ex_Person,X1),true,true,true),true) ).

cnf(u1520,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,uri_rdf_nil,X1),true,true,true),true) ).

cnf(u762,axiom,
    true = ic(uri_rdfs_Datatype) ).

cnf(u3593,axiom,
    true = ifeq(iext(uri_rdf_first,X0,X1),true,iext(uri_rdf_first,X0,X1),true) ).

cnf(u19,axiom,
    true = iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property) ).

cnf(u157,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,X1),true,ifeq(iext(uri_rdfs_subClassOf,X2,X0),true,iext(uri_rdfs_subClassOf,X2,X1),true),true) ).

cnf(u303,axiom,
    true = ifeq(ip(uri_rdf_type),true,true,true) ).

cnf(u389,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_sameAs,X0),true,iext(X0,uri_ex_w,uri_ex_u),true) ).

cnf(u640,axiom,
    true = ifeq(icext(uri_rdf_Property,uri_rdf__1),true,true,true) ).

cnf(u1935,axiom,
    true = ifeq(icext(X0,uri_rdf__1),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,true,true),true) ).

cnf(u4626,axiom,
    true = ifeq(iext(uri_rdf_value,X0,X1),true,iext(uri_rdf_value,X0,X1),true) ).

cnf(u1049,axiom,
    true = ifeq(iext(uri_rdf_subject,X0,X1),true,true,true) ).

cnf(u5362,axiom,
    true = ifeq(icext(uri_rdf_Property,X0),true,icext(uri_rdf_Property,X0),true) ).

cnf(u5422,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_subClassOf,uri_rdfs_subClassOf),true) ).

cnf(u4444,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_object),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdf_object),true) ).

cnf(u546,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf_value,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1833,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_label,X0),true,true,true) ).

cnf(u5135,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__3,uri_rdf__3),true) ).

cnf(u17,axiom,
    true = iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property) ).

cnf(u147,axiom,
    true = ifeq(icext(X0,X1),true,ifeq(iext(uri_rdfs_subClassOf,X0,X2),true,icext(X2,X1),true),true) ).

cnf(u2342,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,true,true) ).

cnf(u301,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u552,axiom,
    true = ifeq(iext(uri_rdf_value,X0,X1),true,icext(uri_rdfs_Resource,X1),true) ).

cnf(u569,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_first),true) ).

cnf(u402,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_Resource),true,true,true),true) ).

cnf(u2724,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,X1),true,true,true) ).

cnf(u1955,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdf_List),true,true,true),true) ).

cnf(u1872,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_value,X0),true,true,true) ).

cnf(u918,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true) ).

cnf(u1317,axiom,
    true = iext(uri_rdfs_subClassOf,uri_ex_Person,uri_rdfs_Resource) ).

cnf(u3175,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_sameAs),true,iext(uri_rdfs_subPropertyOf,X0,uri_owl_sameAs),true) ).

cnf(u674,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,true,true) ).

cnf(u5169,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Bag,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Bag,X0),true) ).

cnf(u1340,axiom,
    true = icext(uri_rdfs_Class,uri_rdfs_Datatype) ).

cnf(u59,axiom,
    true = iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List) ).

cnf(u145,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class) ).

cnf(u4252,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),true,true,true),true) ).

cnf(u291,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,icext(X0,uri_rdf_Property),true) ).

cnf(u429,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_range,uri_rdf_Property),true,true,true),true) ).

cnf(u680,axiom,
    true = icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3) ).

cnf(u314,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf_type,uri_rdfs_Resource),true,true,true),true) ).

cnf(u2593,axiom,
    true = iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property) ).

cnf(u1467,axiom,
    true = ifeq(icext(X0,uri_owl_sameAs),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,true,true),true) ).

cnf(u5546,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),true) ).

cnf(u5641,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Bag,X0),true) ).

cnf(u1194,axiom,
    true = icext(uri_rdfs_Class,uri_rdfs_Resource) ).

cnf(u57,axiom,
    true = ifeq(ic(X0),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u187,axiom,
    true = ifeq(icext(uri_rdfs_Resource,X0),true,true,true) ).

cnf(u5283,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,uri_rdf_List),true,true,true) ).

cnf(u2102,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u573,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_seeAlso,uri_rdfs_Resource),true,true,true),true) ).

cnf(u442,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_label,uri_rdfs_Resource),true) ).

cnf(u2169,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Bag),true,true,true) ).

cnf(u532,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf__3,uri_rdfs_Resource),true) ).

cnf(u2608,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_subClassOf,uri_rdf_Property),true) ).

cnf(u63,axiom,
    true = iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List) ).

cnf(u1850,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_label,uri_rdf_Property),true,true,true),true) ).

cnf(u185,negated_conjecture,
    true != iext(uri_rdf_type,uri_ex_u,uri_ex_Person) ).

cnf(u2507,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Literal),true,true,true),true) ).

cnf(u2883,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u2146,axiom,
    true = iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class) ).

cnf(u684,axiom,
    true = icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1) ).

cnf(u318,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_type,uri_rdfs_Resource),true) ).

cnf(u5289,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,uri_rdfs_ContainerMembershipProperty),true,true,true) ).

cnf(u2730,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf) ).

cnf(u1957,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_List),true) ).

cnf(u5961,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf__3,uri_rdfs_member),true,true,true),true) ).

cnf(u699,axiom,
    true = ic(uri_rdfs_Literal) ).

cnf(u4625,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_value),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdf_value),true) ).

cnf(u3755,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Literal),true) ).

cnf(u3074,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_ex_Person,X0),true,iext(uri_rdfs_subClassOf,uri_ex_Person,X0),true) ).

cnf(u1509,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,true,true) ).

cnf(u1552,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf__1,X0),true,true,true) ).

cnf(u964,axiom,
    true = ifeq(iext(uri_rdf_type,X0,X1),true,true,true) ).

cnf(u2255,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_Container,uri_rdfs_Class),true,true,true),true) ).

cnf(u4967,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,uri_rdfs_isDefinedBy),true,true,true) ).

cnf(u5320,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Seq,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,X0),true) ).

cnf(u3778,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf_rest,uri_rdf_rest),true,true,true),true) ).

cnf(u1721,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource) ).

cnf(u1276,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdfs_Class),true,true,true) ).

cnf(u5378,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Datatype,uri_rdfs_Datatype),true,true,true),true) ).

cnf(u2238,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true,true,true) ).

cnf(u1677,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,uri_rdf__2,X1),true,true,true),true) ).

cnf(u1794,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_object,X1),true,true,true),true) ).

cnf(u1307,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_ex_Person),true,true,true),true) ).

cnf(u5473,axiom,
    true = ifeq(icext(uri_rdfs_Class,X0),true,icext(uri_rdfs_Class,X0),true) ).

cnf(u1607,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_first,X0),true,true,true) ).

cnf(u329,axiom,
    true = ifeq(iext(uri_rdfs_label,X0,X1),true,icext(uri_rdfs_Literal,X1),true) ).

cnf(u2508,axiom,
    true = iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class) ).

cnf(u5459,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Class,uri_rdfs_Class),true,true,true),true) ).

cnf(u613,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_rest,uri_rdf_List),true) ).

cnf(u1892,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_comment),true) ).

cnf(u586,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_predicate,uri_rdfs_Statement),true) ).

cnf(u718,axiom,
    true = ip(uri_rdf_type) ).

cnf(u4957,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,uri_rdf_rest),true,true,true) ).

cnf(u1232,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,uri_rdf_Property),true,true,true) ).

cnf(u103,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,X0),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal),true) ).

cnf(u1890,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_comment),true,true,true),true) ).

cnf(u1537,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_object),true,true,true) ).

cnf(u1735,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_predicate),true,true,true) ).

cnf(u724,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_range,X0),true,icext(X0,uri_rdf_Property),true) ).

cnf(u2259,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Container,uri_rdfs_Class),true) ).

cnf(u2969,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf_predicate,uri_rdf_predicate),true,true,true),true) ).

cnf(u43,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso) ).

cnf(u1616,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_first),true) ).

cnf(u5722,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__1),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true) ).

cnf(u2020,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_seeAlso,X0),true,true,true) ).

cnf(u739,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),true,true,true),true) ).

cnf(u630,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,X0),true,icext(X0,uri_ex_Person),true) ).

cnf(u971,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type) ).

cnf(u101,axiom,
    true = iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype) ).

cnf(u2018,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,X0),true,true,true) ).

cnf(u4956,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,uri_rdf_first),true,true,true) ).

cnf(u636,axiom,
    true = ifeq(icext(uri_rdfs_Class,uri_rdf_Property),true,true,true) ).

cnf(u1738,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_predicate,X0),true,true,true) ).

cnf(u356,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,X1),true,icext(uri_rdfs_Class,X1),true) ).

cnf(u4963,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,uri_rdf_subject),true,true,true) ).

cnf(u1731,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource) ).

cnf(u1407,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u5671,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0),true) ).

cnf(u1744,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_predicate),true,true,true),true) ).

cnf(u615,axiom,
    true = ifeq(iext(uri_rdf_rest,X0,X1),true,icext(uri_rdf_List,X1),true) ).

cnf(u986,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,X1,uri_rdfs_Resource),true) ).

cnf(u2902,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Statement,uri_rdfs_Statement),true) ).

cnf(u2909,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement),true) ).

cnf(u758,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u1777,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_subject,X0),true,true,true) ).

cnf(u2270,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Seq),true,true,true) ).

cnf(u1502,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first) ).

cnf(u5085,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf__2,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf__2,X0),true) ).

cnf(u3176,axiom,
    true = ifeq(iext(uri_owl_sameAs,X0,X1),true,iext(uri_owl_sameAs,X0,X1),true) ).

cnf(u5615,axiom,
    true = ifeq(icext(uri_rdf_XMLLiteral,X0),true,true,true) ).

cnf(u1650,axiom,
    true = iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property) ).

cnf(u497,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u1539,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object) ).

cnf(u2947,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_List),true) ).

cnf(u2531,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0),true,true,true) ).

cnf(u4505,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u5877,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__2,uri_rdfs_member),true) ).

cnf(u240,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf__1,uri_rdf_Property),true,true,true),true) ).

cnf(u4359,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_subject),true) ).

cnf(u2825,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_subPropertyOf,X1),true,true,true),true) ).

cnf(u743,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),true) ).

cnf(u618,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf_predicate,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1905,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_comment,uri_rdf_Property),true) ).

cnf(u2427,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Datatype),true,ifeq(iext(X0,uri_rdf_XMLLiteral,X1),true,true,true),true) ).

cnf(u13,axiom,
    true = iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property) ).

cnf(u373,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_range),true) ).

cnf(u624,axiom,
    true = ifeq(iext(uri_rdf_predicate,X0,X1),true,icext(uri_rdfs_Resource,X1),true) ).

cnf(u1919,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment) ).

cnf(u2170,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Bag,X0),true,true,true) ).

cnf(u5290,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,uri_rdfs_Seq),true,true,true) ).

cnf(u2952,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true) ).

cnf(u3,axiom,
    true = ifeq(iext(X0,X1,X2),true,ip(X0),true) ).

cnf(u2027,axiom,
    true = iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property) ).

cnf(u2430,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0),true,icext(X0,uri_rdf_XMLLiteral),true) ).

cnf(u1029,axiom,
    true = ifeq(iext(uri_rdfs_isDefinedBy,X0,X1),true,true,true) ).

cnf(u898,axiom,
    true = ip(uri_rdfs_isDefinedBy) ).

cnf(u2953,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_List),true,iext(uri_rdfs_subClassOf,X0,uri_rdf_List),true) ).

cnf(u746,axiom,
    true = ic(uri_rdfs_ContainerMembershipProperty) ).

cnf(u5241,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Container,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Container,X0),true) ).

cnf(u2555,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_member,uri_rdf_Property),true) ).

cnf(u1414,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_ex_Person),true,ifeq(iext(X0,X1,uri_ex_w),true,true,true),true) ).

cnf(u141,axiom,
    true = iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement) ).

cnf(u1393,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Literal),true,true,true) ).

cnf(u287,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u501,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf_first,uri_rdf_List),true,true,true),true) ).

cnf(u3591,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true) ).

cnf(u258,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u641,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2),true,true,true) ).

cnf(u396,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_Property),true) ).

cnf(u1686,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Resource),true,true,true) ).

cnf(u244,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf__3,uri_rdf_Property),true,true,true),true) ).

cnf(u1157,axiom,
    true = icext(uri_rdf_Property,uri_rdfs_subClassOf) ).

cnf(u2056,axiom,
    true = ifeq(icext(X0,uri_rdfs_Statement),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true,true,true),true) ).

cnf(u655,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_subPropertyOf,uri_rdf_Property),true) ).

cnf(u3064,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_ex_Person,uri_ex_Person),true,true,true),true) ).

cnf(ifeq_axiom,axiom,
    ifeq(X0,X0,X1,X2) = X1 ).

cnf(u309,axiom,
    true = ifeq(ip(uri_rdf_object),true,true,true) ).

cnf(u5943,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true) ).

cnf(u131,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class) ).

cnf(u285,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u2087,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource) ).

cnf(u3584,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_first),true) ).

cnf(u1039,axiom,
    true = ifeq(iext(uri_rdfs_seeAlso,X0,X1),true,true,true) ).

cnf(u2343,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,true,true) ).

cnf(u1161,axiom,
    true = icext(uri_rdf_Property,uri_rdfs_isDefinedBy) ).

cnf(u1939,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf__1,X1),true,true,true),true) ).

cnf(u5933,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Class,uri_rdfs_Resource),true,true,true),true) ).

cnf(u3067,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_ex_Person),true) ).

cnf(u902,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true,ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Bag,X0),true,true,true),true) ).

cnf(u1301,axiom,
    true = ifeq(ic(uri_ex_Person),true,true,true) ).

cnf(u1416,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_ex_Person,X0),true,icext(X0,uri_ex_w),true) ).

cnf(u1623,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,X1,uri_rdf__1),true,true,true),true) ).

cnf(u3012,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_label,uri_rdfs_label),true,true,true),true) ).

cnf(u2805,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_subPropertyOf,uri_rdf_Property),true,true,true),true) ).

cnf(u283,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,icext(X0,uri_rdf__3),true) ).

cnf(u129,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,X1),true,ifeq(iext(X0,X2,X3),true,icext(X1,X3),true),true) ).

cnf(u3017,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_label),true) ).

cnf(u2454,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt) ).

cnf(u1649,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_domain),true,true,true),true) ).

cnf(u913,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Bag,uri_rdfs_Container),true) ).

cnf(u1197,axiom,
    true = icext(uri_rdfs_Class,uri_rdfs_Literal) ).

cnf(u5665,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Alt,uri_rdfs_Resource),true) ).

cnf(u927,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_Alt,uri_rdfs_Container),true,true,true),true) ).

cnf(u3362,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_member,uri_rdfs_member),true) ).

cnf(u41,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource) ).

cnf(u171,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,ifeq(iext(uri_rdfs_subPropertyOf,X2,X0),true,iext(uri_rdfs_subPropertyOf,X2,X1),true),true) ).

cnf(u1086,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Resource),true,true,true) ).

cnf(u1830,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_label),true,true,true) ).

cnf(u2213,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_Alt),true) ).

cnf(u296,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf_type,uri_rdfs_Class),true,true,true),true) ).

cnf(u523,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_subject,uri_rdfs_Statement),true) ).

cnf(u426,axiom,
    true = ifeq(iext(uri_rdf__3,X0,X1),true,icext(uri_rdfs_Resource,X0),true) ).

cnf(u825,axiom,
    true = ip(uri_rdfs_subClassOf) ).

cnf(u744,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u3015,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_label),true) ).

cnf(u555,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf__2,uri_rdfs_Resource),true,true,true),true) ).

cnf(u4511,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_seeAlso),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_seeAlso),true) ).

cnf(u2109,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource) ).

cnf(u3078,axiom,
    true = ifeq(icext(uri_ex_Person,X0),true,icext(uri_ex_Person,X0),true) ).

cnf(u5321,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq),true) ).

cnf(u47,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal) ).

cnf(u1834,axiom,
    true = ifeq(icext(X0,uri_rdfs_label),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,true,true),true) ).

cnf(u169,axiom,
    true = ifeq(ip(X0),true,iext(uri_rdfs_subPropertyOf,X0,X0),true) ).

cnf(u1084,axiom,
    true = ifeq(iext(uri_rdf_predicate,X0,X1),true,true,true) ).

cnf(u302,axiom,
    true = ifeq(iext(uri_rdf_type,X0,X1),true,icext(uri_rdfs_Class,X1),true) ).

cnf(u685,axiom,
    true = icext(uri_rdf_Property,uri_rdf_rest) ).

cnf(u424,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf__3,uri_rdfs_Resource),true) ).

cnf(u5552,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true) ).

cnf(u953,axiom,
    true = ic(uri_rdfs_Seq) ).

cnf(u683,axiom,
    true = icext(uri_rdf_Property,uri_rdf__1) ).

cnf(u2551,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_member,uri_rdf_Property),true,true,true),true) ).

cnf(u2237,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Container),true,true,true) ).

cnf(u4969,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,uri_rdfs_seeAlso),true,true,true) ).

cnf(u2882,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true) ).

cnf(u175,axiom,
    true = iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class) ).

cnf(u2828,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_subPropertyOf),true) ).

cnf(u1553,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__1),true,true,true) ).

cnf(u2529,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf),true,true,true) ).

cnf(u3781,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u3368,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0),true) ).

cnf(u186,axiom,
    true = ifeq(lv(X0),true,true,true) ).

cnf(u1345,axiom,
    true = icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty) ).

cnf(u1705,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_Resource,uri_rdfs_Class),true,true,true),true) ).

cnf(u2876,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Resource,uri_rdfs_Resource),true) ).

cnf(u936,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true) ).

cnf(u5581,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X0),true) ).

cnf(u3782,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_rest,uri_rdf_rest),true) ).

cnf(u597,axiom,
    true = ifeq(iext(uri_rdf_subject,X0,X1),true,icext(uri_rdfs_Resource,X1),true) ).

cnf(u336,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_comment,uri_rdfs_Literal),true) ).

cnf(u570,axiom,
    true = ifeq(iext(uri_rdf_first,X0,X1),true,icext(uri_rdfs_Resource,X1),true) ).

cnf(u957,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_owl_sameAs,uri_ex_Person),true,true,true) ).

cnf(u5873,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf__2,uri_rdfs_member),true,true,true),true) ).

cnf(u2690,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_ex_Person),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u1473,axiom,
    true = iext(uri_rdf_type,uri_owl_sameAs,uri_rdf_Property) ).

cnf(u5324,axiom,
    true = ifeq(icext(uri_rdfs_Seq,X0),true,icext(uri_rdfs_Seq,X0),true) ).

cnf(u595,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_subject,uri_rdfs_Resource),true) ).

cnf(u2071,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_Statement,uri_rdfs_Class),true,true,true),true) ).

cnf(u955,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Container,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,X0),true) ).

cnf(u3068,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_ex_Person,uri_ex_Person),true) ).

cnf(u87,axiom,
    true = iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource) ).

cnf(u2124,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf__3,X0),true,true,true) ).

cnf(u2243,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Container,X1),true,true,true),true) ).

cnf(u4210,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true) ).

cnf(u725,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_subPropertyOf,uri_rdf_Property),true) ).

cnf(u1880,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_value),true) ).

cnf(u5711,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf__1,uri_rdfs_member),true,true,true),true) ).

cnf(u5571,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Literal,uri_rdfs_Resource),true,true,true),true) ).

cnf(u4433,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf_object,uri_rdf_object),true,true,true),true) ).

cnf(u1958,axiom,
    true = ic(uri_rdf_List) ).

cnf(u2139,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral),true,true,true) ).

cnf(u614,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u5284,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,uri_rdfs_Resource),true,true,true) ).

cnf(u85,axiom,
    true = iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource) ).

cnf(u215,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdf_List),true) ).

cnf(u2394,axiom,
    true = ifeq(icext(X0,uri_rdfs_Datatype),true,true,true) ).

cnf(u1928,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,icext(X0,uri_rdf__3),true) ).

cnf(u4961,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,uri_rdf_object),true,true,true) ).

cnf(u4726,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_range,uri_rdfs_range),true) ).

cnf(u1739,axiom,
    true = ifeq(icext(X0,uri_rdf_predicate),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,true,true),true) ).

cnf(u470,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u3363,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_member),true) ).

cnf(u1531,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject) ).

cnf(u5750,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Container,X0),true) ).

cnf(u5965,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__3,uri_rdfs_member),true) ).

cnf(u1773,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate) ).

cnf(u2130,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf__3),true,true,true),true) ).

cnf(u1745,axiom,
    true = iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property) ).

cnf(u1636,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_rest,X1),true,true,true),true) ).

cnf(u1499,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,true,true) ).

cnf(u742,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Property),true) ).

cnf(u1885,axiom,
    true = ifeq(icext(X0,uri_rdfs_comment),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,true,true),true) ).

cnf(u976,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Resource),true,ifeq(iext(X0,X1,X2),true,true,true),true) ).

cnf(u359,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_subClassOf,uri_rdfs_Class),true,true,true),true) ).

cnf(u2052,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Statement),true,true,true) ).

cnf(u1651,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_domain),true) ).

cnf(u713,axiom,
    true = ip(uri_rdf__3) ).

cnf(u1883,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_comment,X0),true,true,true) ).

cnf(u1755,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_predicate,uri_rdf_Property),true,true,true),true) ).

cnf(u997,axiom,
    true = ifeq(icext(X0,X1),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1640,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,true,true) ).

cnf(u411,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_subClassOf,uri_rdfs_Class),true,true,true),true) ).

cnf(u727,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,icext(uri_rdf_Property,X1),true) ).

cnf(u1889,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_comment,X1),true,true,true),true) ).

cnf(u2236,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Container,X0),true,true,true) ).

cnf(u4214,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,X0),true,icext(uri_rdfs_ContainerMembershipProperty,X0),true) ).

cnf(u125,axiom,
    true = iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class) ).

cnf(u1831,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_label,X0),true,true,true) ).

cnf(u2093,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf__2,X0),true,true,true) ).

cnf(u487,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_seeAlso,uri_rdfs_Resource),true) ).

cnf(u380,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u5107,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),true) ).

cnf(u5464,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u2500,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Literal),true,true,true) ).

cnf(u639,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1),true,true,true) ).

cnf(u5287,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,uri_rdfs_Container),true,true,true) ).

cnf(u2049,axiom,
    true = ifeq(ic(uri_rdfs_Statement),true,true,true) ).

cnf(u7647,axiom,
    true = ifeq(icext(X0,X1),true,true,true) ).

cnf(u730,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal),true,ifeq(iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,X0),true,true,true),true) ).

cnf(u2017,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_seeAlso),true,true,true) ).

cnf(u1396,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Literal),true,true,true) ).

cnf(u115,axiom,
    true = ifeq(icext(uri_rdfs_Class,X0),true,ic(X0),true) ).

cnf(u5672,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u253,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__3,uri_rdf_Property),true) ).

cnf(u4966,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,uri_rdfs_range),true,true,true) ).

cnf(u5266,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_subPropertyOf),true) ).

cnf(u4722,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_range,uri_rdfs_range),true,true,true),true) ).

cnf(u5884,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__2),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true) ).

cnf(u1795,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_object),true,true,true),true) ).

cnf(u3130,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_List,uri_rdfs_Resource),true) ).

cnf(u2542,axiom,
    true = ifeq(icext(X0,uri_rdfs_member),true,true,true) ).

cnf(u1400,axiom,
    true = ifeq(icext(X0,uri_rdf_type),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,true,true),true) ).

cnf(u514,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_Resource),true) ).

cnf(u1801,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_range,X0),true,true,true) ).

cnf(u2137,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,X0),true,true,true) ).

cnf(u5236,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Container),true) ).

cnf(u113,axiom,
    true = ifeq(ic(X0),true,icext(uri_rdfs_Class,X0),true) ).

cnf(u892,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u243,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),true,true,true),true) ).

cnf(u2310,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0),true,true,true) ).

cnf(u1925,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,uri_rdf__3,X1),true,true,true),true) ).

cnf(u399,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,X1),true,icext(uri_rdf_Property,X0),true) ).

cnf(u5423,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

cnf(u3048,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,X0),true) ).

cnf(u498,axiom,
    true = ifeq(iext(uri_rdf_rest,X0,X1),true,icext(uri_rdf_List,X0),true) ).

cnf(u3585,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_first,uri_rdf_first),true) ).

cnf(u2582,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range) ).

cnf(u1053,axiom,
    true = ifeq(iext(uri_rdf__1,X0,X1),true,true,true) ).

cnf(u1528,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_subject,X0),true,true,true) ).

cnf(u2138,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_XMLLiteral),true,true,true) ).

cnf(u642,axiom,
    true = ifeq(icext(uri_rdf_Property,uri_rdf__2),true,true,true) ).

cnf(u2321,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,true,true) ).

cnf(u1308,axiom,
    true = iext(uri_rdf_type,uri_ex_Person,uri_rdfs_Class) ).

cnf(u27,axiom,
    true = ifeq(ip(X0),true,iext(uri_rdf_type,X0,uri_rdf_Property),true) ).

cnf(u241,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),true,true,true),true) ).

cnf(u259,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_rest,uri_rdf_Property),true) ).

cnf(u1158,axiom,
    true = icext(uri_rdf_Property,uri_rdfs_label) ).

cnf(u397,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_domain,uri_rdf_Property),true) ).

cnf(u2064,axiom,
    true = ic(uri_rdfs_Statement) ).

cnf(u1943,axiom,
    true = ifeq(ic(uri_rdf_List),true,true,true) ).

cnf(u282,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,icext(X0,uri_rdf_object),true) ).

cnf(u496,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_rest,uri_rdf_List),true) ).

cnf(u1279,axiom,
    true = icext(uri_rdfs_Class,uri_rdfs_Statement) ).

cnf(u897,axiom,
    true = ip(uri_rdfs_seeAlso) ).

cnf(u2324,axiom,
    true = ifeq(icext(X0,uri_rdf_Property),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true,true,true),true) ).

cnf(u682,axiom,
    true = icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2) ).

cnf(u1413,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_ex_Person),true,ifeq(iext(X0,uri_ex_w,X1),true,true,true),true) ).

cnf(u1627,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member) ).

cnf(u1162,axiom,
    true = icext(uri_rdf_Property,uri_rdfs_range) ).

cnf(u25,axiom,
    true = iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property) ).

cnf(u155,axiom,
    true = ifeq(ic(X0),true,iext(uri_rdfs_subClassOf,X0,X0),true) ).

cnf(u1070,axiom,
    true = ifeq(iext(uri_rdfs_comment,X0,X1),true,true,true) ).

cnf(u1156,axiom,
    true = icext(uri_rdf_Property,uri_rdfs_member) ).

cnf(u3369,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true) ).

cnf(u541,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf__1,uri_rdfs_Resource),true) ).

cnf(u280,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,icext(X0,uri_rdf_subject),true) ).

cnf(u1063,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_first,uri_rdf_List),true,true,true) ).

cnf(u5274,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true) ).

cnf(u5313,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Seq),true) ).

cnf(u1417,axiom,
    true = ifeq(icext(X0,uri_ex_w),true,true,true) ).

cnf(u2452,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource) ).

cnf(u2981,axiom,
    true = ifeq(iext(uri_rdf_predicate,X0,X1),true,iext(uri_rdf_predicate,X0,X1),true) ).

cnf(u4366,axiom,
    true = ifeq(iext(uri_rdf_subject,X0,X1),true,iext(uri_rdf_subject,X0,X1),true) ).

cnf(u2576,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,X1),true,true,true) ).

cnf(u1818,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_range,uri_rdf_Property),true,true,true),true) ).

cnf(u153,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class) ).

cnf(u932,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Alt),true) ).

cnf(u299,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u5131,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf__3,uri_rdf__3),true,true,true),true) ).

cnf(u2877,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u2872,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Resource,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1942,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u408,axiom,
    true = ifeq(iext(uri_rdfs_isDefinedBy,X0,X1),true,icext(uri_rdfs_Resource,X0),true) ).

cnf(u2471,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource) ).

cnf(u3370,axiom,
    true = ifeq(iext(uri_rdfs_member,X0,X1),true,iext(uri_rdfs_member,X0,X1),true) ).

cnf(u937,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Container,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0),true) ).

cnf(u5542,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),true,true,true),true) ).

cnf(u5310,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Seq,uri_rdfs_Seq),true,true,true),true) ).

cnf(u1948,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,true,true) ).

cnf(u1315,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_ex_Person,X0),true,true,true) ).

cnf(u5814,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u159,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property) ).

cnf(u1946,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,true,true) ).

cnf(u564,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf_first,uri_rdfs_Resource),true,true,true),true) ).

cnf(u2099,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf__2,X1),true,true,true),true) ).

cnf(u1854,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_label,uri_rdf_Property),true) ).

cnf(u2445,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdf_Property),true,true,true) ).

cnf(u2222,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_Alt,uri_rdfs_Class),true,true,true),true) ).

cnf(u1457,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_ex_Person),true) ).

cnf(u5783,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u1369,axiom,
    true = icext(uri_rdfs_Class,uri_rdf_XMLLiteral) ).

cnf(u2212,axiom,
    true = iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class) ).

cnf(u5288,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,uri_rdf_Bag),true,true,true) ).

cnf(u686,axiom,
    true = icext(uri_rdf_List,uri_rdf_nil) ).

cnf(u3253,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_domain,uri_rdfs_domain),true) ).

cnf(u920,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true,ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0),true,true,true),true) ).

cnf(u1578,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u425,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf__3),true) ).

cnf(u320,axiom,
    true = ifeq(iext(uri_rdf_type,X0,X1),true,icext(uri_rdfs_Resource,X0),true) ).

cnf(u5740,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Container,uri_rdfs_Resource),true,true,true),true) ).

cnf(u3764,axiom,
    true = ifeq(icext(uri_rdfs_Literal,X0),true,icext(uri_rdfs_Literal,X0),true) ).

cnf(u3249,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_domain,uri_rdfs_domain),true,true,true),true) ).

cnf(u1463,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_sameAs),true,true,true) ).

cnf(u1929,axiom,
    true = ifeq(icext(X0,uri_rdf__3),true,true,true) ).

cnf(u5117,axiom,
    true = ifeq(icext(uri_rdf_XMLLiteral,X0),true,icext(uri_rdf_XMLLiteral,X0),true) ).

cnf(u1860,axiom,
    true = ip(uri_rdfs_label) ).

cnf(u579,axiom,
    true = ifeq(iext(uri_rdfs_seeAlso,X0,X1),true,icext(uri_rdfs_Resource,X1),true) ).

cnf(u3254,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_domain),true) ).

cnf(u2493,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag) ).

cnf(u71,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,X0),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true) ).

cnf(u5715,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__1,uri_rdfs_member),true) ).

cnf(u5601,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Resource),true,true,true),true) ).

cnf(u5972,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__3),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true) ).

cnf(u2393,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Datatype),true) ).

cnf(u326,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_Literal),true) ).

cnf(u2632,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso) ).

cnf(u3100,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Statement,uri_rdfs_Resource),true,true,true),true) ).

cnf(u954,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true) ).

cnf(u1601,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf__2,X0),true,true,true) ).

cnf(u5141,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf__3,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf__3,X0),true) ).

cnf(u2123,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf__3,X0),true,true,true) ).

cnf(u4438,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_object),true) ).

cnf(u5947,axiom,
    true = ifeq(icext(uri_rdfs_Class,X0),true,true,true) ).

cnf(u69,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container) ).

cnf(u3110,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,X0),true) ).

cnf(u5575,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Literal,uri_rdfs_Resource),true) ).

cnf(u1986,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,X0),true,true,true) ).

cnf(u337,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_comment),true) ).

cnf(u604,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_object,uri_rdfs_Statement),true) ).

cnf(u697,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Literal),true) ).

cnf(u3140,axiom,
    true = ifeq(icext(uri_rdf_List,X0),true,true,true) ).

cnf(u1302,axiom,
    true = ifeq(icext(X0,uri_ex_Person),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true,true,true),true) ).

cnf(u1614,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_first),true,true,true),true) ).

cnf(u2114,axiom,
    true = ifeq(iext(uri_owl_sameAs,X0,X1),true,true,true) ).

cnf(u1729,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X0),true,true,true) ).

cnf(u4436,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_object),true) ).

cnf(u1483,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_owl_sameAs,uri_rdf_Property),true,true,true),true) ).

cnf(u726,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_subPropertyOf),true) ).

cnf(u4255,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

cnf(u5642,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u960,axiom,
    true = icext(uri_ex_Person,uri_ex_w) ).

cnf(u1743,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_predicate,X1),true,true,true),true) ).

cnf(u2506,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Literal,X1),true,true,true),true) ).

cnf(u465,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf__2,uri_rdfs_Resource),true,true,true),true) ).

cnf(u657,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,icext(uri_rdf_Property,X0),true) ).

cnf(u5582,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u452,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_comment),true) ).

cnf(u2392,axiom,
    true = iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class) ).

cnf(u1071,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Resource),true,true,true) ).

cnf(u711,axiom,
    true = ip(uri_rdf_value) ).

cnf(u1474,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_owl_sameAs),true) ).

cnf(u1873,axiom,
    true = ifeq(icext(X0,uri_rdf_value),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,true,true),true) ).

cnf(u1748,axiom,
    true = ifeq(ip(uri_rdf_predicate),true,true,true) ).

cnf(u1988,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_isDefinedBy,X0),true,true,true) ).

cnf(u3038,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_comment,uri_rdfs_comment),true,true,true),true) ).

cnf(u109,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,X1),true,ifeq(iext(X0,X2,X3),true,icext(X1,X2),true),true) ).

cnf(u1759,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_predicate,uri_rdf_Property),true) ).

cnf(u341,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_member,uri_rdfs_Resource),true,true,true),true) ).

cnf(u471,axiom,
    true = ifeq(iext(uri_rdf__2,X0,X1),true,icext(uri_rdfs_Resource,X0),true) ).

cnf(u1746,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_predicate),true) ).

cnf(u609,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf_rest,uri_rdf_List),true,true,true),true) ).

cnf(u364,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

cnf(u1797,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_object),true) ).

cnf(u2235,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Container),true,true,true) ).

cnf(u1995,axiom,
    true = iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property) ).

cnf(u1901,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_comment,uri_rdf_Property),true,true,true),true) ).

cnf(u3168,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_owl_sameAs,uri_owl_sameAs),true) ).

cnf(u623,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_predicate),true) ).

cnf(u1472,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_owl_sameAs),true,true,true),true) ).

cnf(u5211,axiom,
    true = ifeq(icext(uri_rdf_Alt,X0),true,icext(uri_rdf_Alt,X0),true) ).

cnf(u714,axiom,
    true = ip(uri_rdf__2) ).

cnf(u99,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal) ).

cnf(u1510,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,true,true) ).

cnf(u237,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_nil,uri_rdf_List),true,true,true),true) ).

cnf(u383,axiom,
    true = ifeq(iext(uri_rdfs_member,X0,X1),true,icext(uri_rdfs_Resource,X1),true) ).

cnf(u469,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf__2,uri_rdfs_Resource),true) ).

cnf(u354,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_domain,uri_rdfs_Class),true) ).

cnf(u492,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf_rest,uri_rdf_List),true,true,true),true) ).

cnf(u4211,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u1782,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_subject,X1),true,true,true),true) ).

cnf(u2055,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement),true,true,true) ).

cnf(u2226,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_Alt,uri_rdfs_Class),true) ).

cnf(u4955,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,uri_rdf_type),true,true,true) ).

cnf(u97,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container) ).

cnf(u4970,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,uri_rdfs_label),true,true,true) ).

cnf(u381,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_member,uri_rdfs_Resource),true) ).

cnf(u632,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_owl_sameAs),true) ).

cnf(u1799,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,true,true) ).

cnf(u2037,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_seeAlso,uri_rdf_Property),true,true,true),true) ).

cnf(u5029,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true) ).

cnf(u881,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_seeAlso),true,ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,X0),true,true,true),true) ).

cnf(u254,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u2693,axiom,
    true = ifeq(icext(uri_ex_Person,X0),true,true,true) ).

cnf(u998,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,X0),true,icext(uri_rdfs_Class,X0),true) ).

cnf(u2041,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_seeAlso,uri_rdf_Property),true) ).

cnf(u1512,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest) ).

cnf(u895,axiom,
    true = ip(uri_rdfs_subPropertyOf) ).

cnf(u2305,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain) ).

cnf(u11,axiom,
    true = iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List) ).

cnf(u1004,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X1),true,icext(X1,X0),true) ).

cnf(u1591,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),true) ).

cnf(u2980,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_predicate),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdf_predicate),true) ).

cnf(u2053,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Statement,X0),true,true,true) ).

cnf(u760,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Datatype),true) ).

cnf(u480,axiom,
    true = ifeq(iext(uri_rdf_value,X0,X1),true,icext(uri_rdfs_Resource,X0),true) ).

cnf(u5103,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),true,true,true),true) ).

cnf(u3050,axiom,
    true = ifeq(iext(uri_rdfs_comment,X0,X1),true,iext(uri_rdfs_comment,X0,X1),true) ).

cnf(u1009,axiom,
    true = ifeq(iext(uri_rdf_value,X0,X1),true,true,true) ).

cnf(u252,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_object,uri_rdf_Property),true) ).

cnf(u5134,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__3),true) ).

cnf(u5348,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_Property,uri_rdf_Property),true,true,true),true) ).

cnf(u2311,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype),true,true,true) ).

cnf(u9,axiom,
    true = iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property) ).

cnf(u139,axiom,
    true = iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource) ).

cnf(u1613,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_first,X1),true,true,true),true) ).

cnf(u2054,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Statement),true,true,true) ).

cnf(u525,axiom,
    true = ifeq(iext(uri_rdf_subject,X0,X1),true,icext(uri_rdfs_Statement,X0),true) ).

cnf(u5352,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Property,uri_rdf_Property),true) ).

cnf(u236,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_Property,uri_rdfs_Class),true,true,true),true) ).

cnf(u242,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf__2,uri_rdf_Property),true,true,true),true) ).

cnf(u2809,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_subPropertyOf,uri_rdf_Property),true) ).

cnf(u1155,axiom,
    true = icext(uri_rdf_Property,uri_rdf_predicate) ).

cnf(u1309,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_ex_Person),true) ).

cnf(u5159,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_Bag,uri_rdf_Bag),true,true,true),true) ).

cnf(u1630,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_rest,X0),true,true,true) ).

cnf(u2560,axiom,
    true = ip(uri_rdfs_member) ).

cnf(u15,axiom,
    true = iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property) ).

cnf(u1802,axiom,
    true = ifeq(icext(X0,uri_rdfs_range),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,true,true),true) ).

cnf(u137,axiom,
    true = iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement) ).

cnf(u916,axiom,
    true = ic(uri_rdfs_Container) ).

cnf(u5267,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),true) ).

cnf(u5022,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u764,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0),true) ).

cnf(u1926,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,X1,uri_rdf__3),true,true,true),true) ).

cnf(u1808,axiom,
    true = iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property) ).

cnf(u2591,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_subClassOf,X1),true,true,true),true) ).

cnf(u5914,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0),true) ).

cnf(u1067,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Resource),true,true,true) ).

cnf(u1545,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_value),true,true,true) ).

cnf(u53,axiom,
    true = ifeq(icext(X0,X1),true,iext(uri_rdf_type,X1,X0),true) ).

cnf(u651,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_subPropertyOf,uri_rdf_Property),true,true,true),true) ).

cnf(u542,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u2205,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt),true,true,true) ).

cnf(u4504,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_seeAlso,uri_rdfs_seeAlso),true) ).

cnf(u2351,axiom,
    true = iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class) ).

cnf(u49,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource) ).

cnf(u143,axiom,
    true = iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource) ).

cnf(u1930,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member) ).

cnf(u281,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,icext(X0,uri_rdf_value),true) ).

cnf(u945,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Seq,uri_rdfs_Container),true,true,true),true) ).

cnf(u5275,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,iext(uri_rdfs_subPropertyOf,X0,X1),true) ).

cnf(u1838,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_label,X1),true,true,true),true) ).

cnf(u304,axiom,
    true = ifeq(ip(uri_rdf_first),true,true,true) ).

cnf(u398,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_domain),true) ).

cnf(u1319,axiom,
    true = iext(uri_rdfs_subClassOf,uri_ex_Person,uri_ex_Person) ).

cnf(u4660,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u4510,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,X0),true) ).

cnf(u2349,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Class,X1),true,true,true),true) ).

cnf(u4512,axiom,
    true = ifeq(iext(uri_rdfs_seeAlso,X0,X1),true,iext(uri_rdfs_seeAlso,X0,X1),true) ).

cnf(u55,axiom,
    true = ifeq(iext(uri_rdf_type,X0,X1),true,icext(X1,X0),true) ).

cnf(u1687,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,true,true) ).

cnf(u676,axiom,
    true = icext(uri_rdf_Property,uri_rdf_subject) ).

cnf(u2211,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdf_Alt),true,true,true),true) ).

cnf(u310,axiom,
    true = ifeq(ip(uri_rdf_value),true,true,true) ).

cnf(u693,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Literal),true,true,true),true) ).

cnf(u1561,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__3),true,true,true) ).

cnf(u1568,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,true,true) ).

cnf(u4655,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf__1,uri_rdf__1),true,true,true),true) ).

cnf(u3114,axiom,
    true = ifeq(icext(uri_rdfs_Statement,X0),true,true,true) ).

cnf(u2193,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_Bag,uri_rdfs_Class),true) ).

cnf(u2972,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_predicate),true) ).

cnf(u1709,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Resource,uri_rdfs_Class),true) ).

cnf(u183,axiom,
    true = iext(uri_owl_sameAs,uri_ex_w,uri_ex_u) ).

cnf(u5553,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u1690,axiom,
    true = ifeq(icext(X0,uri_rdfs_Resource),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true,true,true),true) ).

cnf(u308,axiom,
    true = ifeq(ip(uri_rdf__3),true,true,true) ).

cnf(u438,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_label,uri_rdfs_Resource),true,true,true),true) ).

cnf(u3261,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,X1),true,iext(uri_rdfs_domain,X0,X1),true) ).

cnf(u2519,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_Literal,uri_rdfs_Class),true,true,true),true) ).

cnf(u4658,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u1696,axiom,
    true = iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class) ).

cnf(u3075,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_ex_Person),true,iext(uri_rdfs_subClassOf,X0,uri_ex_Person),true) ).

cnf(u938,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true,ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Seq,X0),true,true,true),true) ).

cnf(u5080,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u582,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf_predicate,uri_rdfs_Statement),true,true,true),true) ).

cnf(u1454,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_ex_w,uri_ex_Person),true,true,true),true) ).

cnf(u181,axiom,
    true = iext(uri_rdfs_domain,uri_owl_sameAs,uri_ex_Person) ).

cnf(u588,axiom,
    true = ifeq(iext(uri_rdf_predicate,X0,X1),true,icext(uri_rdfs_Statement,X0),true) ).

cnf(u681,axiom,
    true = icext(uri_rdf_Property,uri_rdf__2) ).

cnf(u3252,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_domain),true) ).

cnf(u2483,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq) ).

cnf(u3041,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_comment),true) ).

cnf(u2173,axiom,
    true = ifeq(icext(X0,uri_rdf_Bag),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true,true,true),true) ).

cnf(u2111,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty) ).

cnf(u1458,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_ex_w,uri_ex_Person),true) ).

cnf(u5019,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf_type,uri_rdf_type),true,true,true),true) ).

cnf(u1604,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2) ).

cnf(u710,axiom,
    true = ip(uri_rdf_subject) ).

cnf(u1981,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource) ).

cnf(u327,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_label,uri_rdfs_Literal),true) ).

cnf(u1602,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__2),true,true,true) ).

cnf(u5389,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype),true) ).

cnf(u1608,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_first,X0),true,true,true) ).

cnf(u1689,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true,true,true) ).

cnf(u2239,axiom,
    true = ifeq(icext(X0,uri_rdfs_Container),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true,true,true),true) ).

cnf(u698,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_XMLLiteral),true) ).

cnf(u1660,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_domain,uri_rdf_Property),true,true,true),true) ).

cnf(u2901,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Statement),true) ).

cnf(u3022,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_label,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,X0),true) ).

cnf(u93,axiom,
    true = iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty) ).

cnf(u4962,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,uri_rdf_value),true,true,true) ).

cnf(u1871,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_value,X0),true,true,true) ).

cnf(u1730,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal),true,true,true) ).

cnf(u1066,axiom,
    true = ifeq(iext(uri_rdfs_label,X0,X1),true,true,true) ).

cnf(u5075,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf__2,uri_rdf__2),true,true,true),true) ).

cnf(u605,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_object),true) ).

cnf(u1109,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_object,uri_rdfs_Statement),true,true,true) ).

cnf(u1736,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,X0),true,true,true) ).

cnf(u1765,axiom,
    true = ip(uri_rdf_predicate) ).

cnf(u1370,axiom,
    true = icext(uri_rdfs_Class,uri_rdfs_Seq) ).

cnf(u1644,axiom,
    true = ifeq(icext(X0,uri_rdfs_domain),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,true,true),true) ).

cnf(u3358,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_member,uri_rdfs_member),true,true,true),true) ).

cnf(u1985,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_isDefinedBy),true,true,true) ).

cnf(u5421,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

cnf(u83,axiom,
    true = iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource) ).

cnf(u453,axiom,
    true = ifeq(iext(uri_rdfs_comment,X0,X1),true,icext(uri_rdfs_Resource,X0),true) ).

cnf(u2204,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Alt),true,true,true) ).

cnf(u338,axiom,
    true = ifeq(iext(uri_rdfs_comment,X0,X1),true,icext(uri_rdfs_Literal,X1),true) ).

cnf(u721,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_subPropertyOf,uri_rdf_Property),true,true,true),true) ).

cnf(u2660,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,true,true) ).

cnf(u1891,axiom,
    true = iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property) ).

cnf(u2510,axiom,
    true = ifeq(icext(X0,uri_rdfs_Literal),true,true,true) ).

cnf(u2136,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_XMLLiteral),true,true,true) ).

cnf(u967,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,true,true) ).

cnf(u81,axiom,
    true = iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource) ).

cnf(u365,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,X1),true,icext(uri_rdfs_Class,X0),true) ).

cnf(u1911,axiom,
    true = ip(uri_rdfs_comment) ).

cnf(u3016,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_label,uri_rdfs_label),true) ).

cnf(u417,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,X1),true,icext(uri_rdfs_Class,X1),true) ).

cnf(u2210,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_Alt,X1),true,true,true),true) ).

cnf(u4727,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_range),true) ).

cnf(u2019,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_seeAlso,X0),true,true,true) ).

cnf(u238,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_rest,uri_rdf_Property),true,true,true),true) ).

cnf(u3788,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true) ).

cnf(u982,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,X1,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1381,axiom,
    true = ifeq(icext(X0,uri_rdfs_Class),true,true,true) ).

cnf(u2912,axiom,
    true = ifeq(icext(uri_rdfs_Statement,X0),true,icext(uri_rdfs_Statement,X0),true) ).

cnf(u2025,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_seeAlso,X1),true,true,true),true) ).

cnf(u2684,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_ex_Person),true) ).

cnf(u123,axiom,
    true = ifeq(lv(X0),true,icext(uri_rdfs_Literal,X0),true) ).

cnf(u209,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u355,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_domain),true) ).

cnf(u4974,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,uri_owl_sameAs),true,true,true) ).

cnf(u2160,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Class),true) ).

cnf(u5235,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Container,uri_rdfs_Container),true) ).

cnf(u5388,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0),true) ).

cnf(u1798,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,true,true) ).

cnf(u2420,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class) ).

cnf(u894,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

cnf(u2021,axiom,
    true = ifeq(icext(X0,uri_rdfs_seeAlso),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,true,true),true) ).

cnf(u5113,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,X0),true) ).

cnf(u1575,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_ContainerMembershipProperty,X1),true,true,true),true) ).

cnf(u5024,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u1007,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_first,uri_rdfs_Resource),true,true,true) ).

cnf(u121,axiom,
    true = ifeq(icext(uri_rdfs_Literal,X0),true,lv(X0),true) ).

cnf(u251,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_value,uri_rdf_Property),true) ).

cnf(u647,axiom,
    true = ifeq(icext(uri_rdf_Property,uri_rdf_subject),true,true,true) ).

cnf(u5612,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u483,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_seeAlso,uri_rdfs_Resource),true,true,true),true) ).

cnf(u637,axiom,
    true = ifeq(icext(uri_rdf_List,uri_rdf_nil),true,true,true) ).

cnf(u2288,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_Seq,uri_rdfs_Class),true,true,true),true) ).

cnf(u2094,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf__2,X0),true,true,true) ).

cnf(u506,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_first),true) ).

cnf(u77,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource) ).

cnf(u2206,axiom,
    true = ifeq(icext(X0,uri_rdf_Alt),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true,true,true),true) ).

cnf(u635,axiom,
    true = ifeq(icext(uri_rdf_Property,uri_rdf_first),true,true,true) ).

cnf(u914,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Bag),true) ).

cnf(u2061,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Statement),true,true,true),true) ).

cnf(u3592,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true) ).

cnf(u127,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property) ).

cnf(u249,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Datatype),true) ).

cnf(u900,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,X0),true) ).

cnf(u4619,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_value),true) ).

cnf(u748,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true) ).

cnf(u382,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_member),true) ).

cnf(u2272,axiom,
    true = ifeq(icext(X0,uri_rdfs_Seq),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true,true,true),true) ).

cnf(u1159,axiom,
    true = icext(uri_rdf_Property,uri_rdfs_seeAlso) ).

cnf(u5751,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u1051,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Resource),true,true,true) ).

cnf(u1632,axiom,
    true = ifeq(icext(X0,uri_rdf_rest),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,true,true),true) ).

cnf(u763,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true) ).

cnf(u2189,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_Bag,uri_rdfs_Class),true,true,true),true) ).

cnf(u5904,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Datatype,uri_rdfs_Resource),true,true,true),true) ).

cnf(u919,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Container,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Bag,X0),true) ).

cnf(u33,axiom,
    true = iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property) ).

cnf(u255,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__2,uri_rdf_Property),true) ).

cnf(u5163,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Bag,uri_rdf_Bag),true) ).

cnf(u2689,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_ex_Person,X0),true) ).

cnf(u1164,axiom,
    true = icext(uri_rdf_Property,uri_rdfs_domain) ).

cnf(u1822,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_range,uri_rdf_Property),true) ).

cnf(u5231,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Container,uri_rdfs_Container),true,true,true),true) ).

cnf(u1840,axiom,
    true = iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property) ).

cnf(u510,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_Resource),true,true,true),true) ).

cnf(u5645,axiom,
    true = ifeq(icext(uri_rdf_Bag,X0),true,true,true) ).

cnf(u4614,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf_value,uri_rdf_value),true,true,true),true) ).

cnf(u2322,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,true,true) ).

cnf(u1785,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_subject),true) ).

cnf(u2180,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_Bag),true) ).

cnf(u289,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u39,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource) ).

cnf(u2594,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

cnf(u4659,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__1,uri_rdf__1),true) ).

cnf(u393,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_domain,uri_rdf_Property),true,true,true),true) ).

cnf(u2329,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdf_Property),true,true,true),true) ).

cnf(u1563,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3) ).

cnf(u2095,axiom,
    true = ifeq(icext(X0,uri_rdf__2),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,true,true),true) ).

cnf(u677,axiom,
    true = icext(uri_rdf_Property,uri_rdf_value) ).

cnf(u1832,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_label,X0),true,true,true) ).

cnf(u909,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_Bag,uri_rdfs_Container),true,true,true),true) ).

cnf(u2344,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true,true,true) ).

cnf(u1569,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_ContainerMembershipProperty),true,true,true) ).

cnf(u1956,axiom,
    true = iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class) ).

cnf(u675,axiom,
    true = icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral) ).

cnf(u2177,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_Bag,X1),true,true,true),true) ).

cnf(u2956,axiom,
    true = ifeq(icext(uri_rdf_List,X0),true,icext(uri_rdf_List,X0),true) ).

cnf(u5944,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u1310,axiom,
    true = ic(uri_ex_Person) ).

cnf(u37,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal) ).

cnf(u167,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property) ).

cnf(u1954,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_List,X1),true,true,true),true) ).

cnf(u305,axiom,
    true = ifeq(ip(uri_rdf_rest),true,true,true) ).

cnf(u537,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf__1,uri_rdfs_Resource),true,true,true),true) ).

cnf(u292,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,icext(X0,uri_rdf_first),true) ).

cnf(u2595,axiom,
    true = ifeq(icext(X0,uri_rdfs_subClassOf),true,true,true) ).

cnf(u1680,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u551,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_value),true) ).

cnf(u5786,axiom,
    true = ifeq(icext(uri_rdfs_Seq,X0),true,true,true) ).

cnf(u1697,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u5803,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdf_Property,uri_rdfs_Resource),true,true,true),true) ).

cnf(u5915,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u1438,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_ex_Person,uri_rdfs_Class),true,true,true),true) ).

cnf(u165,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,ifeq(iext(X0,X2,X3),true,iext(X1,X2,X3),true),true) ).

cnf(u4256,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),true) ).

cnf(u311,axiom,
    true = ifeq(ip(uri_rdf_subject),true,true,true) ).

cnf(u433,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_range,uri_rdf_Property),true) ).

cnf(u700,axiom,
    true = ic(uri_rdf_XMLLiteral) ).

cnf(u2528,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),true,true,true) ).

cnf(u420,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf__3,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1363,axiom,
    true = ifeq(icext(X0,X0),true,true,true) ).

cnf(u949,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Seq,uri_rdfs_Container),true) ).

cnf(u1471,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_owl_sameAs,X1),true,true,true),true) ).

cnf(u679,axiom,
    true = icext(uri_rdf_Property,uri_rdf__3) ).

cnf(u1442,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_ex_Person,uri_rdfs_Class),true) ).

cnf(u1841,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_label),true) ).

cnf(u3581,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdf_first,uri_rdf_first),true,true,true),true) ).

cnf(u4262,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,X0),true) ).

cnf(u5173,axiom,
    true = ifeq(icext(uri_rdf_Bag,X0),true,icext(uri_rdf_Bag,X0),true) ).

cnf(u560,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u4666,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__1),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdf__1),true) ).

cnf(u5817,axiom,
    true = ifeq(icext(uri_rdf_Property,X0),true,true,true) ).

cnf(u5106,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_XMLLiteral),true) ).

cnf(u2538,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_member,X1),true,true,true),true) ).

cnf(u2407,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Datatype,uri_rdfs_Class),true) ).

cnf(u1074,axiom,
    true = ifeq(iext(uri_rdf__2,X0,X1),true,true,true) ).

cnf(u1969,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_List,uri_rdfs_Class),true) ).

cnf(u3260,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true) ).

cnf(u2491,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource) ).

cnf(u1733,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal) ).

cnf(u4443,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_object,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf_object,X0),true) ).

cnf(u688,axiom,
    true = icext(uri_rdf_Property,uri_rdf_first) ).

cnf(u1983,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List) ).

cnf(u577,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_seeAlso,uri_rdfs_Resource),true) ).

cnf(u332,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_comment,uri_rdfs_Literal),true,true,true),true) ).

cnf(u1622,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,uri_rdf__1,X1),true,true,true),true) ).

cnf(u3136,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true) ).

cnf(u591,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf_subject,uri_rdfs_Resource),true,true,true),true) ).

cnf(u5263,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),true,true,true),true) ).

cnf(u5170,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag),true,iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag),true) ).

cnf(u67,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container) ).

cnf(u205,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdf_Property),true) ).

cnf(u2384,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Datatype),true,true,true) ).

cnf(u1506,axiom,
    true = ifeq(iext(uri_rdf_rest,X0,X1),true,true,true) ).

cnf(u2418,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource) ).

cnf(u460,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf__1,uri_rdfs_Resource),true) ).

cnf(u2661,axiom,
    true = iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property) ).

cnf(u1567,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_ContainerMembershipProperty),true,true,true) ).

cnf(u2120,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_owl_sameAs,uri_owl_sameAs) ).

cnf(u1881,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_comment),true,true,true) ).

cnf(u5973,axiom,
    true = ifeq(iext(uri_rdf__3,X0,X1),true,iext(uri_rdfs_member,X0,X1),true) ).

cnf(u2659,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,true,true) ).

cnf(u65,axiom,
    true = iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List) ).

cnf(u2390,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Datatype,X1),true,true,true),true) ).

cnf(u2361,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_Class,uri_rdfs_Class),true,true,true),true) ).

cnf(u600,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdf_object,uri_rdfs_Statement),true,true,true),true) ).

cnf(u1965,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_List,uri_rdfs_Class),true,true,true),true) ).

cnf(u5359,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true) ).

cnf(u3783,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u5314,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Seq,uri_rdfs_Seq),true) ).

cnf(u5200,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Alt),true) ).

cnf(u2662,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf) ).

cnf(u5937,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Class,uri_rdfs_Resource),true) ).

cnf(u5353,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Property),true) ).

cnf(u3789,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true) ).

cnf(u2009,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdf_Property),true) ).

cnf(u4204,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u107,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property) ).

cnf(u5245,axiom,
    true = ifeq(icext(uri_rdfs_Container,X0),true,icext(uri_rdfs_Container,X0),true) ).

cnf(u5078,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u2144,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_XMLLiteral,X1),true,true,true),true) ).

cnf(u2279,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Seq),true) ).

cnf(u362,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u977,axiom,
    true = iext(uri_rdf_type,X0,uri_rdfs_Resource) ).

cnf(u4964,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,uri_rdfs_domain),true,true,true) ).

cnf(u2005,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_isDefinedBy,uri_rdf_Property),true,true,true),true) ).

cnf(u3024,axiom,
    true = ifeq(iext(uri_rdfs_label,X0,X1),true,iext(uri_rdfs_label,X0,X1),true) ).

cnf(u1950,axiom,
    true = ifeq(icext(X0,uri_rdf_List),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true,true,true),true) ).

cnf(u3169,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_owl_sameAs),true) ).

cnf(u105,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class) ).

cnf(u1516,axiom,
    true = ifeq(icext(X0,uri_rdf_nil),true,ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_List),true,true,true),true) ).

cnf(u235,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_first,uri_rdf_Property),true,true,true),true) ).

cnf(u1894,axiom,
    true = ifeq(ip(uri_rdfs_comment),true,true,true) ).

cnf(u2277,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Seq),true,true,true),true) ).

cnf(u1529,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_subject),true,true,true) ).

cnf(u889,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),true,true,true),true) ).

cnf(u5358,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true) ).

cnf(u4733,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true) ).

cnf(u2244,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Container),true,true,true),true) ).

cnf(u2656,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,true,true) ).

cnf(u111,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class) ).

cnf(u2428,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Datatype),true,ifeq(iext(X0,X1,uri_rdf_XMLLiteral),true,true,true),true) ).

cnf(u1278,axiom,
    true = icext(uri_rdfs_Class,uri_ex_Person) ).

cnf(u732,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal),true) ).

cnf(u2278,axiom,
    true = iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class) ).

cnf(u749,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true,ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0),true,true,true),true) ).

cnf(u488,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u2060,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Statement,X1),true,true,true),true) ).

cnf(u5635,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Bag,uri_rdfs_Resource),true) ).

cnf(u5207,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0),true) ).

cnf(u1641,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,true,true) ).

cnf(u2028,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u747,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty),true,iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true) ).

cnf(u638,axiom,
    true = ifeq(icext(uri_rdf_Property,uri_rdf_rest),true,true,true) ).

cnf(u1533,axiom,
    true = ifeq(iext(uri_rdf_object,X0,X1),true,true,true) ).

cnf(u5208,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt),true,iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt),true) ).

cnf(u2946,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_List,uri_rdf_List),true) ).

cnf(u4200,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),true,true,true),true) ).

cnf(u239,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),true,true,true),true) ).

cnf(u2026,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_seeAlso),true,true,true),true) ).

cnf(u377,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_member,uri_rdfs_Resource),true,true,true),true) ).

cnf(u516,axiom,
    true = ifeq(iext(uri_rdfs_isDefinedBy,X0,X1),true,icext(uri_rdfs_Resource,X1),true) ).

cnf(u507,axiom,
    true = ifeq(iext(uri_rdf_first,X0,X1),true,icext(uri_rdf_List,X0),true) ).

cnf(u1806,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_range,X1),true,true,true),true) ).

cnf(u533,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf__3),true) ).

cnf(u5136,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__3),true) ).

cnf(u893,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),true) ).

cnf(u250,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_subject,uri_rdf_Property),true) ).

cnf(u435,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,X1),true,icext(uri_rdf_Property,X0),true) ).

cnf(u1163,axiom,
    true = icext(uri_rdf_Property,uri_rdfs_comment) ).

cnf(u5918,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,X0),true,true,true) ).

cnf(u2292,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Seq,uri_rdfs_Class),true) ).

cnf(u1523,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,uri_rdf_nil),true) ).

cnf(u4358,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_subject,uri_rdf_subject),true) ).

cnf(u1152,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_range,uri_rdf_Property),true,true,true) ).

cnf(u23,axiom,
    true = iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property) ).

cnf(u1000,axiom,
    true = ifeq(icext(uri_rdfs_Seq,X0),true,icext(uri_rdfs_Container,X0),true) ).

cnf(u1783,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_subject),true,true,true),true) ).

cnf(u505,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_first,uri_rdf_List),true) ).

cnf(u644,axiom,
    true = ifeq(icext(uri_rdf_Property,uri_rdf__3),true,true,true) ).

cnf(u2179,axiom,
    true = iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class) ).

cnf(u1934,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf__1,X0),true,true,true) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SWB018-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38  % Computer : n009.cluster.edu
% 0.12/0.38  % Model    : x86_64 x86_64
% 0.12/0.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38  % Memory   : 8046.5625MB
% 0.12/0.38  % OS       : Linux 6.8.0-71-generic
% 0.12/0.38  % CPULimit : 300
% 0.12/0.38  % WCLimit  : 300
% 0.12/0.38  % DateTime : Mon Sep 28 07:00:45 UTC 2026
% 0.12/0.38  % CPUTime  : 
% 0.12/0.38  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42  Running first-order theorem proving
% 0.12/0.42  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.59/2.09  % (2848119)Detected a unit-equality problem, will run specialized UEQ schedule.
% 8.59/2.09  % (2848220)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2527296345:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 8.59/2.09  % (2848221)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2073143851:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 8.59/2.09  % (2848222)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2697569583:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 8.59/2.09  % (2848219)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=1708832101:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 8.59/2.09  % (2848226)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3225790398:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 8.59/2.09  % (2848224)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3566625371:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 8.59/2.09  % (2848225)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=2733924652:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 8.59/2.09  % (2848222)Instruction limit reached! 
% 8.59/2.09  % (2848222)------------------------------
% 8.59/2.09  % (2848222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.59/2.09  % (2848222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/2.09  % (2848222)CaDiCaL version: 2.1.3
% 8.59/2.09  % (2848222)Termination reason: Instruction limit
% 8.59/2.09  % (2848222)Termination phase: Saturation
% 8.59/2.09  % (2848222)Time elapsed: 0.068 s
% 8.59/2.09  % (2848222)Peak memory usage: 89 MB
% 8.59/2.09  % (2848222)Instructions burned: 136 (million)
% 8.59/2.09  % (2848224)Refutation not found, incomplete strategy
% 8.59/2.09  % (2848224)------------------------------
% 8.59/2.09  % (2848224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.59/2.09  % (2848224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/2.09  % (2848224)CaDiCaL version: 2.1.3
% 8.59/2.09  % (2848224)Termination reason: Refutation not found, incomplete strategy
% 8.59/2.09  % (2848224)Time elapsed: 0.071 s
% 8.59/2.09  % (2848224)Peak memory usage: 89 MB
% 8.59/2.09  % (2848224)Instructions burned: 130 (million)
% 8.59/2.09  % (2848225)Instruction limit reached! 
% 8.59/2.09  % (2848225)------------------------------
% 8.59/2.09  % (2848225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.59/2.09  % (2848225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/2.09  % (2848225)CaDiCaL version: 2.1.3
% 8.59/2.09  % (2848225)Termination reason: Instruction limit
% 8.59/2.09  % (2848225)Termination phase: Saturation
% 8.59/2.09  % (2848225)Time elapsed: 0.149 s
% 8.59/2.09  % (2848225)Peak memory usage: 92 MB
% 8.59/2.09  % (2848225)Instructions burned: 259 (million)
% 8.59/2.09  % (2848239)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3928701841:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 8.59/2.09  % (2848226)Refutation not found, incomplete strategy
% 8.59/2.09  % (2848226)------------------------------
% 8.59/2.09  % (2848226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.59/2.09  % (2848226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/2.09  % (2848226)CaDiCaL version: 2.1.3
% 8.59/2.09  % (2848226)Termination reason: Refutation not found, incomplete strategy
% 8.59/2.09  % (2848226)Time elapsed: 0.341 s
% 8.59/2.09  % (2848226)Peak memory usage: 93 MB
% 8.59/2.09  % (2848226)Instructions burned: 505 (million)
% 8.59/2.09  % (2848224)------------------------------
% 8.59/2.09  % (2848224)------------------------------
% 8.59/2.09  % (2848252)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3589750235:i=4948:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/4948Mi)
% 8.59/2.09  % (2848278)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1463431689:i=215:ep=RSTC_2994 on theBenchmark for (2994ds/215Mi)
% 8.59/2.09  % (2848226)------------------------------
% 8.59/2.09  % (2848226)------------------------------
% 8.59/2.09  % (2848278)Instruction limit reached! 
% 8.59/2.09  % (2848278)------------------------------
% 8.59/2.09  % (2848278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.59/2.09  % (2848278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/2.09  % (2848278)CaDiCaL version: 2.1.3
% 8.59/2.09  % (2848278)Termination reason: Instruction limit
% 8.59/2.09  % (2848278)Termination phase: Saturation
% 8.59/2.09  % (2848278)Time elapsed: 0.095 s
% 8.59/2.09  % (2848278)Peak memory usage: 91 MB
% 8.59/2.09  % (2848278)Instructions burned: 216 (million)
% 8.59/2.09  % (2848329)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=4162229258:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2992 on theBenchmark for (2992ds/317Mi)
% 8.59/2.09  [W928 07:00:46.507214253 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 8.59/2.09  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.59/2.09  [W928 07:00:46.507257937 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 8.59/2.09  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.59/2.09  [W928 07:00:46.507300047 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 8.59/2.09  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.59/2.09  [W928 07:00:46.507313100 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 8.59/2.09  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.59/2.09  [W928 07:00:46.507339570 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 8.59/2.09  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.59/2.09  [W928 07:00:46.507356924 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 8.59/2.09  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.59/2.09  % (2848354)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=2281147907:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 8.59/2.09  % (2848220)First to succeed.
% 8.59/2.09  % (2848220)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2848119"
% 8.59/2.09  % (2848329)Instruction limit reached! 
% 8.59/2.09  % (2848329)------------------------------
% 8.59/2.09  % (2848329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.59/2.09  % (2848329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/2.09  % (2848329)CaDiCaL version: 2.1.3
% 8.59/2.09  % (2848329)Termination reason: Instruction limit
% 8.59/2.09  % (2848329)Termination phase: Saturation
% 8.59/2.09  % (2848329)Time elapsed: 0.174 s
% 8.59/2.09  % (2848329)Peak memory usage: 95 MB
% 8.59/2.09  % (2848329)Instructions burned: 317 (million)
% 8.59/2.09  % (2848252)Refutation not found, incomplete strategy
% 8.59/2.09  % (2848252)------------------------------
% 8.59/2.09  % (2848252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.59/2.09  % (2848252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/2.09  % (2848252)CaDiCaL version: 2.1.3
% 8.59/2.09  % (2848252)Termination reason: Refutation not found, incomplete strategy
% 8.59/2.09  % (2848252)Time elapsed: 0.568 s
% 8.59/2.09  % (2848252)Peak memory usage: 127 MB
% 8.59/2.09  % (2848252)Instructions burned: 856 (million)
% 8.59/2.09  % SZS status Satisfiable for theBenchmark
% 8.59/2.09  % SZS output start Saturation.
% See solution above
% 9.15/2.28  % SZS output start Definitions and Model Updates.
% 9.15/2.28  for all inputs,
% 9.15/2.28      define ir(X0) := true
% 9.15/2.28  % SZS output end Definitions and Model Updates.
% 9.15/2.28  % (2848220)------------------------------
% 9.15/2.28  % (2848220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.15/2.28  % (2848220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.15/2.28  % (2848220)CaDiCaL version: 2.1.3
% 9.15/2.28  % (2848220)Termination reason: Satisfiable
% 9.15/2.28  % (2848220)Time elapsed: 0.935 s
% 9.15/2.28  % (2848220)Peak memory usage: 141 MB
% 9.15/2.28  % (2848220)Instructions burned: 2446 (million)
% 9.15/2.28  % (2848220)------------------------------
% 9.15/2.28  % (2848220)------------------------------
% 9.15/2.28  % (2848119)Success in time 1.215 s
% 9.15/2.28  % Vampire exiting
%------------------------------------------------------------------------------