Vampire---5.0.1.SAT-Sat.s

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

% Computer : n020.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 12:59:57 PM UTC 2026

% Result   : Satisfiable 11.31s 2.44s
% Output   : Saturation 11.77s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u3989,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

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

cnf(u1612,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(u2291,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u1415,axiom,
    true = ifeq(icext(X0,uri_rdf_List),true,true,true) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(u521,axiom,
    true = ifeq(iext(uri_rdfs_comment,X0,X1),true,icext(uri_rdfs_Resource,X0),true) ).

cnf(u276,axiom,
    true = ic(uri_rdf_XMLLiteral) ).

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

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

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

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

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

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

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

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

cnf(u1589,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Statement),true) ).

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

cnf(u3096,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(u417,axiom,
    true = icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1) ).

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

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

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

cnf(u3004,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(u663,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(u2194,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment) ).

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

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

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

cnf(u2588,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(u1839,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),true) ).

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

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

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

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

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

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

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

cnf(u946,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(u2207,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_subject,X0),true,true,true) ).

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

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

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

cnf(u421,axiom,
    true = icext(uri_rdf_Property,uri_rdf_first) ).

cnf(u672,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(u2218,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value) ).

cnf(u1081,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(u444,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(u4919,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__1),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdf__1),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u584,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_object,uri_rdfs_Statement),true) ).

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

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

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

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

cnf(u1993,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class) ).

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

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

cnf(u5325,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(u712,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u2007,axiom,
    true = ifeq(icext(X0,uri_rdfs_range),true,true,true) ).

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

cnf(u1313,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_Alt,X1),true,true,true),true) ).

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

cnf(u2388,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal) ).

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

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

cnf(u2178,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(u975,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,X1,uri_rdfs_Resource),true) ).

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

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

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

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

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

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

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

cnf(u194,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(u2516,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt),true,iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt),true) ).

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

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

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

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

cnf(u2464,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_XMLLiteral),true) ).

cnf(u217,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(u2412,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf__1),true,true,true),true) ).

cnf(u363,axiom,
    true = ifeq(ip(uri_rdf_subject),true,true,true) ).

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

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

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

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

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

cnf(u2762,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(u1625,axiom,
    true = ifeq(icext(uri_rdfs_Statement,X0),true,true,true) ).

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

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

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

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

cnf(u223,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(u361,axiom,
    true = ifeq(ip(uri_rdf_object),true,true,true) ).

cnf(u1260,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(u491,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_rest,uri_rdf_List),true) ).

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

cnf(u256,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdfs_ContainerMembershipProperty),true) ).

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

cnf(u1586,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(u3193,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Literal,uri_rdfs_Resource),true) ).

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

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

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

cnf(u5247,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(u1794,axiom,
    true = ifeq(icext(X0,uri_rdfs_Seq),true,true,true) ).

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

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

cnf(u489,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(u1659,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List) ).

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

cnf(u645,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(u2302,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(u890,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),true) ).

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

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

cnf(u1406,axiom,
    true = ifeq(iext(uri_rdf_type,X0,uri_rdf_List),true,true,true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u4855,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(u1571,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource) ).

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

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

cnf(u2337,axiom,
    true = ifeq(icext(X0,uri_rdf_object),true,true,true) ).

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

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

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

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

cnf(u5683,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(u4625,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_subject,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf_subject,X0),true) ).

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

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

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

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

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

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

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

cnf(u1699,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(u1590,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Statement),true) ).

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

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

cnf(u4616,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(u3300,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_label,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdfs_label,X0),true) ).

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

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

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

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

cnf(u1446,axiom,
    true = ifeq(icext(X0,uri_rdfs_Statement),true,true,true) ).

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

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

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

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

cnf(u1884,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(u2202,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object) ).

cnf(u2345,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u190,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(u2380,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member) ).

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

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

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

cnf(u690,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(u1675,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_List,uri_rdf_List),true) ).

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

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

cnf(u1206,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(u1442,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Statement,X1),true,true,true),true) ).

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

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

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

cnf(u945,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(u2798,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(u2992,axiom,
    true = iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property) ).

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

cnf(u2369,axiom,
    true = ifeq(icext(X0,uri_rdf_value),true,true,true) ).

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

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

cnf(u435,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(u2117,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_predicate),true,true,true) ).

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

cnf(u330,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Bag),true) ).

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

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

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

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

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

cnf(u3685,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(u1862,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Literal),true,true,true) ).

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

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

cnf(u2634,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(u458,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,X1),true,icext(uri_rdf_Property,X0),true) ).

cnf(u2699,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(u587,axiom,
    true = ifeq(iext(uri_rdf_object,X0,X1),true,icext(uri_rdfs_Statement,X0),true) ).

cnf(u3029,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso) ).

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

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

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

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

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

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

cnf(u717,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(u1872,axiom,
    true = iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class) ).

cnf(u1239,axiom,
    true = ifeq(iext(uri_rdf_type,X0,uri_rdf_XMLLiteral),true,true,true) ).

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

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

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

cnf(u1501,axiom,
    true = icext(uri_rdf_Property,uri_rdf_predicate) ).

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

cnf(u3042,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(u5667,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__1),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true) ).

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

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

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

cnf(u2147,axiom,
    true = ip(uri_rdf_predicate) ).

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

cnf(u462,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(u2783,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource) ).

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

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

cnf(u627,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(u2129,axiom,
    true = ifeq(icext(X0,uri_rdf_predicate),true,true,true) ).

cnf(u2260,axiom,
    true = ifeq(icext(X0,uri_rdfs_isDefinedBy),true,true,true) ).

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

cnf(u1248,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_XMLLiteral,X1),true,true,true),true) ).

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

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

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

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

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

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

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

cnf(u2784,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq) ).

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

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

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

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

cnf(u3302,axiom,
    true = ifeq(iext(uri_rdfs_label,X0,X1),true,iext(uri_rdfs_label,X0,X1),true) ).

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

cnf(u1126,axiom,
    true = ifeq(iext(uri_rdf_type,X0,uri_rdfs_Datatype),true,true,true) ).

cnf(u2426,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member) ).

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

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

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

cnf(u1771,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(u502,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_label),true) ).

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

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

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

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

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

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

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

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

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

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

cnf(u385,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(u1137,axiom,
    true = iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class) ).

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

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

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

cnf(u1423,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(u692,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf__2,uri_rdfs_Resource),true) ).

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

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

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

cnf(u268,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(u2509,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Alt),true) ).

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

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

cnf(u512,axiom,
    true = ifeq(iext(uri_rdf_first,X0,X1),true,icext(uri_rdf_List,X0),true) ).

cnf(u4129,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(u529,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_subject),true) ).

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

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

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

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

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

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

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

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

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

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

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

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(u2336,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_object),true) ).

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

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

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

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

cnf(u2186,axiom,
    true = ip(uri_rdfs_comment) ).

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

cnf(u412,axiom,
    true = icext(uri_rdf_Property,uri_rdf__3) ).

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

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

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

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

cnf(u1434,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Statement),true,true,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(u1062,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,true,true) ).

cnf(u1957,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(u2765,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Datatype),true) ).

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

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

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

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

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

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

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

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

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

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

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

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(u924,axiom,
    true = ip(uri_rdf__2) ).

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

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

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

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

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

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

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

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

cnf(u943,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(u57,axiom,
    true = ifeq(ic(X0),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

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

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

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

cnf(u573,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(u2224,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__2),true,true,true) ).

cnf(u3264,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(u5631,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(u2113,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,true,true) ).

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

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

cnf(u1454,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(u63,axiom,
    true = iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List) ).

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

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

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

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

cnf(u2375,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,uri_rdf__1,X1),true,true,true),true) ).

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

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

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

cnf(u699,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(u2125,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_predicate,X1),true,true,true),true) ).

cnf(u2898,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain) ).

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

cnf(u191,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(u964,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Resource),true,ifeq(iext(X0,X1,X2),true,true,true),true) ).

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

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

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

cnf(u2116,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest) ).

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

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

cnf(u357,axiom,
    true = ifeq(ip(uri_rdf_rest),true,true,true) ).

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

cnf(u596,axiom,
    true = ifeq(iext(uri_rdf_predicate,X0,X1),true,icext(uri_rdfs_Statement,X0),true) ).

cnf(u2131,axiom,
    true = ifeq(ip(uri_rdf_predicate),true,true,true) ).

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

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

cnf(u352,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Datatype),true) ).

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

cnf(u202,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(u1823,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_ContainerMembershipProperty,X1),true,true,true),true) ).

cnf(u611,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf__2,uri_rdfs_Resource),true) ).

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

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

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

cnf(u3158,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(u1232,axiom,
    true = icext(uri_rdfs_Class,uri_rdf_XMLLiteral) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u636,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(u4067,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true) ).

cnf(u356,axiom,
    true = ifeq(ip(uri_rdf_first),true,true,true) ).

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

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

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

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

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

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

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

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

cnf(u229,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(u1539,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,uri_rdf_Property),true,true,true) ).

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

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

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

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

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

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

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

cnf(u618,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(u1905,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,true,true) ).

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

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

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

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

cnf(u2170,axiom,
    true = ifeq(ip(uri_rdfs_comment),true,true,true) ).

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

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

cnf(u2027,axiom,
    true = ifeq(iext(uri_rdf_rest,X0,uri_rdf_nil),true,true,true) ).

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

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

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

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

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

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

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

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

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

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

cnf(u2967,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(u2941,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_type),true) ).

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

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

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

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

cnf(u2258,axiom,
    true = iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property) ).

cnf(u1686,axiom,
    true = ifeq(icext(uri_rdf_List,X0),true,icext(uri_rdf_List,X0),true) ).

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

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

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

cnf(u530,axiom,
    true = ifeq(iext(uri_rdf_subject,X0,X1),true,icext(uri_rdfs_Statement,X0),true) ).

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

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

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

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

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

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

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

cnf(u3069,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(u3584,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_range,uri_rdfs_range),true) ).

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

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

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

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

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

cnf(u1069,axiom,
    true = ifeq(iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class),true,true,true) ).

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

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

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

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

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

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

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

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

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

cnf(u2080,axiom,
    true = iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property) ).

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

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

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

cnf(u1167,axiom,
    true = iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class) ).

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

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

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

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

cnf(u208,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(u927,axiom,
    true = ip(uri_rdf_first) ).

cnf(u1178,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Resource,uri_rdfs_Class),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(u2280,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_seeAlso),true,true,true) ).

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

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

cnf(u426,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(u825,axiom,
    true = ip(uri_rdfs_range) ).

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

cnf(u942,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(u1456,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Statement,uri_rdfs_Class),true) ).

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

cnf(u480,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(u47,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal) ).

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

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

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

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

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

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

cnf(u4654,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(u685,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf__1),true) ).

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

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

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

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

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

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

cnf(u2720,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource) ).

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

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

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

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

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

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

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

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

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

cnf(u2876,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(u1718,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag),true,true,true) ).

cnf(u2168,axiom,
    true = ifeq(icext(X0,uri_rdfs_comment),true,true,true) ).

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

cnf(u1870,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Literal,X1),true,true,true),true) ).

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

cnf(u2292,axiom,
    true = ifeq(icext(X0,uri_rdfs_seeAlso),true,true,true) ).

cnf(u3145,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf) ).

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

cnf(u1724,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_Bag,X1),true,true,true),true) ).

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

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

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

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

cnf(u708,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(u4939,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__2),true) ).

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

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

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

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

cnf(u2139,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(u614,axiom,
    true = ifeq(iext(uri_rdf__2,X0,X1),true,icext(uri_rdfs_Resource,X0),true) ).

cnf(u1358,axiom,
    true = ifeq(iext(uri_rdfs_label,X0,X1),true,true,true) ).

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

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

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

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

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

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

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

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

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

cnf(u1499,axiom,
    true = icext(uri_rdf_Property,uri_rdfs_comment) ).

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

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

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

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

cnf(u2911,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(u713,axiom,
    true = ifeq(iext(uri_rdfs_seeAlso,X0,X1),true,icext(uri_rdfs_Resource,X1),true) ).

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

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

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

cnf(u3191,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(u602,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf__1,uri_rdfs_Resource),true) ).

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

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

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

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

cnf(u888,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(u1738,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(u4866,axiom,
    true = ifeq(iext(uri_rdf_value,X0,X1),true,iext(uri_rdf_value,X0,X1),true) ).

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

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

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

cnf(u4015,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(u1233,axiom,
    true = icext(uri_rdfs_Class,uri_rdfs_Seq) ).

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

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

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

cnf(u1147,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(u1402,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,true,true) ).

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

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

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

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

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

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

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

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

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

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

cnf(u2849,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(u228,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Datatype),true) ).

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

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

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

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

cnf(u2017,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(u1250,axiom,
    true = iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class) ).

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

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

cnf(u1925,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(u520,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_comment),true) ).

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

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

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

cnf(u498,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(u3585,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_range),true) ).

cnf(u4058,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(u2709,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true) ).

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

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

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

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

cnf(u1308,axiom,
    true = ifeq(iext(uri_rdf_type,X0,uri_rdf_Alt),true,true,true) ).

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

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

cnf(u2069,axiom,
    true = ifeq(icext(X0,uri_rdf_first),true,true,true) ).

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

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

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

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

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

cnf(u2324,axiom,
    true = ifeq(icext(X0,uri_rdf_subject),true,true,true) ).

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

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

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

cnf(u1413,axiom,
    true = iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class) ).

cnf(u453,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(u25,axiom,
    true = iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property) ).

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

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

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

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

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

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

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

cnf(u280,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(u1063,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,true,true) ).

cnf(u410,axiom,
    true = icext(uri_rdf_Property,uri_rdf_value) ).

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

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

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

cnf(u4749,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(u1160,axiom,
    true = ifeq(ic(uri_rdfs_Resource),true,true,true) ).

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

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

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

cnf(u408,axiom,
    true = icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral) ).

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

cnf(u5657,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(u1083,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Class,uri_rdfs_Class),true) ).

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

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

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

cnf(u1072,axiom,
    true = iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class) ).

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

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

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

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

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

cnf(u564,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(u414,axiom,
    true = icext(uri_rdf_Property,uri_rdf__2) ).

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

cnf(u2735,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(u2354,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,icext(X0,uri_rdf__2),true) ).

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

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

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

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

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

cnf(u920,axiom,
    true = ip(uri_rdf_subject) ).

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

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

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

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

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

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

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

cnf(u941,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(u2482,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource) ).

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

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

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

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

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

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

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

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

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

cnf(u326,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(u1864,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal),true,true,true) ).

cnf(u1712,axiom,
    true = ifeq(icext(uri_rdf_List,X0),true,true,true) ).

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

cnf(u2461,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(u69,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container) ).

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

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

cnf(u337,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(u604,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf__1),true) ).

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

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

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

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

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

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

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

cnf(u726,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(u5642,axiom,
    true = ifeq(iext(uri_rdf__2,X0,X1),true,iext(uri_rdfs_member,X0,X1),true) ).

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

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

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

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

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

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

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

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

cnf(u1503,axiom,
    true = icext(uri_rdf_Property,uri_rdfs_seeAlso) ).

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

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

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

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

cnf(u1748,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Container),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 = iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class) ).

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

cnf(u3986,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(u471,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(u609,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(u3044,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Bag,uri_rdfs_Resource),true) ).

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

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

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

cnf(u214,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(u3168,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_predicate),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdf_predicate),true) ).

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

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

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

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

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

cnf(u99,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal) ).

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

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

cnf(u737,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_member,uri_rdfs_Resource),true) ).

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

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

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

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

cnf(u2938,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(u751,axiom,
    true = icext(uri_rdfs_Resource,X0) ).

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

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

cnf(u97,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container) ).

cnf(u2422,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,X1,uri_rdf__3),true,true,true),true) ).

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

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

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

cnf(u2037,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,uri_rdf_nil),true) ).

cnf(u1135,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Datatype,X1),true,true,true),true) ).

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

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

cnf(u2092,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(u1397,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0),true,icext(X0,uri_rdf_XMLLiteral),true) ).

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

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

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

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

cnf(u11,axiom,
    true = iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(u9,axiom,
    true = iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property) ).

cnf(u3221,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(u139,axiom,
    true = iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource) ).

cnf(u3582,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(u525,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(u2327,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_object,X0),true,true,true) ).

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

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

cnf(u2270,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(u2560,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(u15,axiom,
    true = iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property) ).

cnf(u137,axiom,
    true = iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement) ).

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

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

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

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

cnf(u921,axiom,
    true = ip(uri_rdf_value) ).

cnf(u1437,axiom,
    true = ifeq(iext(uri_rdf_type,X0,uri_rdfs_Statement),true,true,true) ).

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

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(u411,axiom,
    true = icext(uri_rdf_Property,uri_rdf_object) ).

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

cnf(u1176,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(u1936,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,true,true) ).

cnf(u507,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(u1673,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(u5659,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__1,uri_rdfs_member),true) ).

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

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

cnf(u93,axiom,
    true = iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty) ).

cnf(u409,axiom,
    true = icext(uri_rdf_Property,uri_rdf_subject) ).

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

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

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

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

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

cnf(u4909,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(u1447,axiom,
    true = ic(uri_rdfs_Statement) ).

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

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

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

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

cnf(u1326,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(u53,axiom,
    true = ifeq(icext(X0,X1),true,iext(uri_rdf_type,X1,X0),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u1228,axiom,
    true = ifeq(icext(X0,X0),true,true,true) ).

cnf(u582,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(u3267,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_comment),true) ).

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

cnf(u944,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(u1727,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_Bag),true) ).

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

cnf(u681,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(u3900,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(u2483,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty) ).

cnf(u1726,axiom,
    true = iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class) ).

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

cnf(u2226,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2) ).

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

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

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

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

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

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

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

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

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

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

cnf(u192,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(u1290,axiom,
    true = ifeq(iext(uri_rdf__3,X0,X1),true,true,true) ).

cnf(u2239,axiom,
    true = ifeq(icext(X0,uri_rdf_rest),true,true,true) ).

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

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

cnf(u963,axiom,
    true = ifeq(iext(uri_rdf_type,X0,uri_rdfs_Resource),true,true,true) ).

cnf(u360,axiom,
    true = ifeq(ip(uri_rdf__3),true,true,true) ).

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

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

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

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

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

cnf(u348,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(u3294,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_label),true) ).

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

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

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

cnf(u83,axiom,
    true = iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource) ).

cnf(u367,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(u2893,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,X1),true,true,true) ).

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

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

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

cnf(u476,axiom,
    true = ifeq(iext(uri_rdfs_comment,X0,X1),true,icext(uri_rdfs_Literal,X1),true) ).

cnf(u3291,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(u196,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),true) ).

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

cnf(u735,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(u967,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X1),true,icext(X1,X0),true) ).

cnf(u81,axiom,
    true = iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource) ).

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

cnf(u211,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(u2406,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf__1,X0),true,true,true) ).

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

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

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

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

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

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

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

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

cnf(u879,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(u2913,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Datatype,uri_rdfs_Resource),true) ).

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

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

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

cnf(u2082,axiom,
    true = ifeq(icext(X0,uri_rdfs_label),true,true,true) ).

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

cnf(u744,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(u3123,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(u378,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_range,uri_rdfs_Class),true) ).

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

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

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

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

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

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

cnf(u1128,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Datatype),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_range,uri_rdf_type,X0),true,icext(X0,uri_rdfs_Datatype),true) ).

cnf(u2166,axiom,
    true = iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property) ).

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

cnf(u376,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(u3586,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_range),true) ).

cnf(u226,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(u3911,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,X1),true,iext(uri_rdfs_domain,X0,X1),true) ).

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

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

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

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

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

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

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

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

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

cnf(u2038,axiom,
    true = ifeq(icext(X0,uri_rdf_nil),true,true,true) ).

cnf(u1792,axiom,
    true = iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class) ).

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

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

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

cnf(u33,axiom,
    true = iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property) ).

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

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

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

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

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

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

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

cnf(u1411,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_List,X1),true,true,true),true) ).

cnf(u654,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(u2333,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_object,X1),true,true,true),true) ).

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

cnf(u39,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource) ).

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

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

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

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

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

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

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

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

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

cnf(u37,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal) ).

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

cnf(u167,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property) ).

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

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

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

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

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

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

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

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

cnf(u755,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(u922,axiom,
    true = ip(uri_rdf_object) ).

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

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

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

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

cnf(u2612,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),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(u311,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,icext(X0,uri_rdf__3),true) ).

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

cnf(u306,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_XMLLiteral),true) ).

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

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

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

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

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

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

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

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

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

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

cnf(u2533,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(u439,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

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

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

cnf(u2642,axiom,
    true = ip(uri_rdfs_member) ).

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

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

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

cnf(u77,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource) ).

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

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

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

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

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

cnf(testcase_conclusion_fullish_004_Axiomatic_Triples,negated_conjecture,
    tuple(iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing),iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class),iext(uri_rdf_type,uri_owl_Class,uri_owl_Class),iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing),iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)) != tuple(true,true,true,true,true) ).

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

cnf(u591,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(u67,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container) ).

cnf(u205,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(u351,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u4935,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(u3275,axiom,
    true = ifeq(iext(uri_rdfs_comment,X0,X1),true,iext(uri_rdfs_comment,X0,X1),true) ).

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

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

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

cnf(u65,axiom,
    true = iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List) ).

cnf(u195,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(u1110,axiom,
    true = icext(uri_rdfs_Class,uri_rdfs_Datatype) ).

cnf(u2005,axiom,
    true = iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property) ).

cnf(u600,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(u4758,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_object,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf_object,X0),true) ).

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

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

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

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

cnf(u1804,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(u966,axiom,
    true = iext(uri_rdf_type,X0,uri_rdfs_Resource) ).

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

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

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

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

cnf(u107,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property) ).

cnf(u193,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(u339,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Seq,uri_rdfs_Container),true) ).

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

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

cnf(u362,axiom,
    true = ifeq(ip(uri_rdf_value),true,true,true) ).

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

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

cnf(u220,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(u1315,axiom,
    true = iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class) ).

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

cnf(u2663,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(u4062,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u105,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class) ).

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

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

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

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

cnf(u2506,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(u1992,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource) ).

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

cnf(u1497,axiom,
    true = icext(uri_rdf_Property,uri_rdfs_domain) ).

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

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

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

cnf(u1599,axiom,
    true = ifeq(icext(uri_rdfs_Statement,X0),true,icext(uri_rdfs_Statement,X0),true) ).

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

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

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

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

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

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

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

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

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

cnf(u2028,axiom,
    true = ifeq(iext(uri_rdf_rest,uri_rdf_nil,X0),true,true,true) ).

cnf(u1395,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Datatype),true,ifeq(iext(X0,X1,uri_rdf_XMLLiteral),true,true,true),true) ).

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

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

cnf(u23,axiom,
    true = iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property) ).

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

cnf(u516,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(u2051,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,X1),true,true,true) ).

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

cnf(u272,axiom,
    true = ic(uri_rdfs_Container) ).

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

cnf(u893,axiom,
    true = ip(uri_rdfs_subPropertyOf) ).

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

cnf(u1837,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(u2128,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_predicate),true) ).

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

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

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

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

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

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

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

cnf(u1658,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource) ).

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


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SWB004-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38  % Computer : n020.cluster.edu
% 0.11/0.38  % Model    : x86_64 x86_64
% 0.11/0.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38  % Memory   : 8046.5625MB
% 0.11/0.38  % OS       : Linux 6.8.0-71-generic
% 0.11/0.38  % CPULimit : 300
% 0.11/0.38  % WCLimit  : 300
% 0.11/0.38  % DateTime : Mon Sep 28 06:55:20 UTC 2026
% 0.11/0.38  % CPUTime  : 
% 0.11/0.38  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41  Running first-order theorem proving
% 0.11/0.41  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
% 11.31/2.44  % (5979)Detected a unit-equality problem, will run specialized UEQ schedule.
% 11.31/2.44  % (5985)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=2192832235:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 11.31/2.44  % (5989)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1135054884:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 11.31/2.44  % (5986)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2766340553:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 11.31/2.44  % (5984)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=1829681103:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 11.31/2.44  % (5990)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1743758398:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 11.31/2.44  % (5988)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=833170616:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 11.31/2.44  % (5987)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=43329359:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 11.31/2.44  % (5987)Instruction limit reached! 
% 11.31/2.44  % (5987)------------------------------
% 11.31/2.44  % (5987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.44  % (5987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.44  % (5987)CaDiCaL version: 2.1.3
% 11.31/2.44  % (5987)Termination reason: Instruction limit
% 11.31/2.44  % (5987)Termination phase: Saturation
% 11.31/2.44  % (5987)Time elapsed: 0.070 s
% 11.31/2.44  % (5987)Peak memory usage: 89 MB
% 11.31/2.44  % (5987)Instructions burned: 136 (million)
% 11.31/2.44  % (5988)Refutation not found, incomplete strategy
% 11.31/2.44  % (5988)------------------------------
% 11.31/2.44  % (5988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.44  % (5988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.44  % (5988)CaDiCaL version: 2.1.3
% 11.31/2.44  % (5988)Termination reason: Refutation not found, incomplete strategy
% 11.31/2.44  % (5988)Time elapsed: 0.074 s
% 11.31/2.44  % (5988)Peak memory usage: 89 MB
% 11.31/2.44  % (5988)Instructions burned: 137 (million)
% 11.31/2.44  % (5989)Instruction limit reached! 
% 11.31/2.44  % (5989)------------------------------
% 11.31/2.44  % (5989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.44  % (5989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.44  % (5989)CaDiCaL version: 2.1.3
% 11.31/2.44  % (5989)Termination reason: Instruction limit
% 11.31/2.44  % (5989)Termination phase: Saturation
% 11.31/2.44  % (5989)Time elapsed: 0.150 s
% 11.31/2.44  % (5989)Peak memory usage: 92 MB
% 11.31/2.44  % (5989)Instructions burned: 258 (million)
% 11.31/2.44  % (5998)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1599230346:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 11.31/2.44  % (5990)Refutation not found, incomplete strategy
% 11.31/2.44  % (5990)------------------------------
% 11.31/2.44  % (5990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.44  % (5990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.44  % (5990)CaDiCaL version: 2.1.3
% 11.31/2.44  % (5990)Termination reason: Refutation not found, incomplete strategy
% 11.31/2.44  % (5990)Time elapsed: 0.237 s
% 11.31/2.44  % (5990)Peak memory usage: 92 MB
% 11.31/2.44  % (5990)Instructions burned: 466 (million)
% 11.31/2.44  % (5999)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3635514910:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 11.31/2.44  % (5988)------------------------------
% 11.31/2.44  % (5988)------------------------------
% 11.31/2.44  % (6002)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=3858025757:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 11.31/2.44  % (5990)------------------------------
% 11.31/2.44  % (5990)------------------------------
% 11.31/2.44  % (6002)Instruction limit reached! 
% 11.31/2.44  % (6002)------------------------------
% 11.31/2.44  % (6002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.44  % (6002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.44  % (6002)CaDiCaL version: 2.1.3
% 11.31/2.44  % (6002)Termination reason: Instruction limit
% 11.31/2.44  % (6002)Termination phase: Saturation
% 11.31/2.44  % (6002)Time elapsed: 0.062 s
% 11.31/2.44  % (6002)Peak memory usage: 89 MB
% 11.31/2.44  % (6002)Instructions burned: 218 (million)
% 11.31/2.44  % (6005)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=344376512:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2993 on theBenchmark for (2993ds/12125Mi)
% 11.31/2.44  % (6004)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=2689485059:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2993 on theBenchmark for (2993ds/317Mi)
% 11.31/2.44  % (6004)Instruction limit reached! 
% 11.31/2.44  % (6004)------------------------------
% 11.31/2.44  % (6004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.44  % (6004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.44  % (6004)CaDiCaL version: 2.1.3
% 11.31/2.44  % (6004)Termination reason: Instruction limit
% 11.31/2.44  % (6004)Termination phase: Saturation
% 11.31/2.44  % (6004)Time elapsed: 0.176 s
% 11.31/2.44  % (6004)Peak memory usage: 95 MB
% 11.31/2.44  % (6004)Instructions burned: 319 (million)
% 11.31/2.44  % (6008)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1662217199:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2990 on theBenchmark for (2990ds/2836Mi)
% 11.31/2.44  % (5985)First to succeed.
% 11.31/2.44  % (5985)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-5979"
% 11.31/2.44  % (6008)Also succeeded, but the first one will report.
% 11.31/2.44  % (5986)Also succeeded, but the first one will report.
% 11.31/2.44  % SZS status Satisfiable for theBenchmark
% 11.31/2.44  % SZS output start Saturation.
% See solution above
% 11.77/2.64  % SZS output start Definitions and Model Updates.
% 11.77/2.64  for all inputs,
% 11.77/2.64      define ir(X0) := true
% 11.77/2.64  % SZS output end Definitions and Model Updates.
% 11.77/2.64  % (5985)------------------------------
% 11.77/2.64  % (5985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.77/2.64  % (5985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.77/2.64  % (5985)CaDiCaL version: 2.1.3
% 11.77/2.64  % (5985)Termination reason: Satisfiable
% 11.77/2.64  % (5985)Time elapsed: 1.204 s
% 11.77/2.64  % (5985)Peak memory usage: 140 MB
% 11.77/2.64  % (5985)Instructions burned: 2328 (million)
% 11.77/2.64  % (5985)------------------------------
% 11.77/2.64  % (5985)------------------------------
% 11.77/2.64  % (5979)Success in time 1.586 s
% 11.77/2.64  % Vampire exiting
%------------------------------------------------------------------------------