Vampire---5.0.1.SAT-Sat.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : SWB021-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM

% Computer : n002.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue Sep 29 01:00:08 PM UTC 2026

% Result   : Satisfiable 10.72s 2.75s
% Output   : Saturation 11.80s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u661,axiom,
    true = icext(uri_rdfs_Class,uri_rdf_Bag) ).

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

cnf(u3062,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(u2066,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf__2),true,true,true),true) ).

cnf(u3082,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(u3209,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_value,uri_rdfs_Resource),true) ).

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

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

cnf(u3068,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(u3206,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_comment,uri_rdfs_Literal),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3253,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12,uri_rdf_List),true) ).

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

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

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

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

cnf(u3134,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(u404,axiom,
    true = ifeq(iext(uri_rdf_first,X1,X0),true,true,true) ).

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

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

cnf(u2998,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(u3716,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true) ).

cnf(u3127,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(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(u1593,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Datatype,X1),true,true,true),true) ).

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

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

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

cnf(u3235,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12,uri_rdf_nil),true) ).

cnf(u2990,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(u61,axiom,
    true = iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource) ).

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

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

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

cnf(u316,axiom,
    true = ip(uri_owl_oneOf) ).

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

cnf(u2715,axiom,
    true = iext(uri_rdf_type,sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11,uri_rdf_List) ).

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

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

cnf(u3001,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(u3244,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12,uri_ex_w2),true) ).

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

cnf(u189,axiom,
    true = iext(uri_rdf_rest,sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41,sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42) ).

cnf(u421,axiom,
    true = iext(uri_rdf_type,uri_owl_oneOf,uri_rdf_Property) ).

cnf(u2134,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_owl_unionOf,X0),true,icext(X0,sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41),true) ).

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

cnf(u3259,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11,uri_rdf_List),true) ).

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

cnf(u3248,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42,uri_ex_c2),true) ).

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

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

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

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

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

cnf(u2989,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(u2984,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(u2628,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32),true,true,true),true) ).

cnf(u2987,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(u3773,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(u2232,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_rest,X0),true,icext(X0,sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42),true) ).

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

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

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

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

cnf(u3002,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(u3051,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(u706,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt) ).

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

cnf(u2133,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_owl_oneOf,X0),true,icext(X0,sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21),true) ).

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

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

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

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

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

cnf(u2634,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32),true) ).

cnf(u2688,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31),true,true,true),true) ).

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

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

cnf(u3045,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32,sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33),true,true,true),true) ).

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

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

cnf(u217,axiom,
    true = iext(uri_rdf_first,sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21,uri_ex_w2) ).

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

cnf(u3043,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42,uri_rdf_nil),true,true,true),true) ).

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

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

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

cnf(u3708,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(u1625,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Property),true) ).

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

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

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

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

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

cnf(u2708,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11),true,true,true),true) ).

cnf(u3058,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(u223,axiom,
    true = iext(uri_rdf_first,sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12,uri_ex_w2) ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3046,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22,uri_rdf_nil),true,true,true),true) ).

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

cnf(u2727,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21,X1),true,true,true),true) ).

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

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

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

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

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

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

cnf(u3089,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(u540,axiom,
    true = ip(uri_rdf_object) ).

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

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

cnf(u3076,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(u3213,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_rest,uri_rdf_List),true) ).

cnf(u3092,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(u3071,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(u3322,axiom,
    true = ifeq(iext(uri_rdf_rest,X1,X0),true,iext(uri_rdf_rest,X1,X0),true) ).

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

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

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

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

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

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

cnf(u2442,axiom,
    true = icext(uri_rdf_List,sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22) ).

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

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

cnf(u3118,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(u3204,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_Resource),true) ).

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

cnf(u917,axiom,
    true = icext(uri_rdf_Property,uri_owl_unionOf) ).

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

cnf(u2088,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Datatype),true,ifeq(iext(X0,X1,uri_rdf_XMLLiteral),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

cnf(u3246,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32,uri_ex_w2),true) ).

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

cnf(u3239,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42,uri_rdf_nil),true) ).

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

cnf(u2985,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(u6425,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,uri_owl_equivalentClass),true,ifeq(sF0,true,sF0,true),true) ).

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

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

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

cnf(u319,axiom,
    true = ip(uri_owl_unionOf) ).

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

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

cnf(u3242,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21,sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22),true) ).

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

cnf(u3243,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41,sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42),true) ).

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

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

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

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

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

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

cnf(u2734,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21),true) ).

cnf(u934,axiom,
    true = icext(uri_rdf_Property,uri_rdfs_domain) ).

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

cnf(u2627,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32,X1),true,true,true),true) ).

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

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

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

cnf(u2986,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(u945,axiom,
    true = icext(uri_rdf_List,uri_rdf_nil) ).

cnf(u2992,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(u75,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource) ).

cnf(u3088,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(u3109,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_owl_oneOf,uri_owl_oneOf),true,true,true),true) ).

cnf(u3056,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(u2618,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u3133,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(u73,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property) ).

cnf(u852,axiom,
    true = iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class) ).

cnf(u3249,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31,uri_ex_w1),true) ).

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

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

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

cnf(u3103,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(u805,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest) ).

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

cnf(u2624,axiom,
    true = icext(uri_rdf_List,sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32) ).

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

cnf(u201,axiom,
    true = iext(uri_rdf_rest,sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22,uri_rdf_nil) ).

cnf(u980,axiom,
    true = ip(uri_rdfs_member) ).

cnf(u3027,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32,uri_rdf_List),true,true,true),true) ).

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

cnf(u1872,axiom,
    true = iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property) ).

cnf(u2655,axiom,
    true = iext(uri_rdf_type,sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33,uri_rdf_List) ).

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

cnf(u3128,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(u2132,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_owl_oneOf,X0),true,icext(X0,sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11),true) ).

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

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

cnf(u3139,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_oneOf),true,ifeq(iext(X0,uri_ex_c1,sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11),true,true,true),true) ).

cnf(u3042,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31,sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32),true,true,true),true) ).

cnf(u207,axiom,
    true = iext(uri_rdf_first,sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41,uri_ex_c1) ).

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

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

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

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

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

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

cnf(u2707,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11,X1),true,true,true),true) ).

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

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

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

cnf(u3301,axiom,
    true = ifeq(iext(uri_owl_unionOf,X1,X0),true,iext(uri_owl_unionOf,X1,X0),true) ).

cnf(u2674,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42),true) ).

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

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

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

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

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

cnf(u3075,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(u3030,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41,uri_ex_c1),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

cnf(u2426,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12),true,true,true),true) ).

cnf(u3073,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(u3295,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_nil,uri_rdf_List),true) ).

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

cnf(u3041,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11,sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3095,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(u1561,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_first,X1),true,true,true),true) ).

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

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

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

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

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

cnf(u792,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_owl_unionOf,uri_owl_unionOf) ).

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

cnf(u2241,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_first,X0),true,icext(X0,uri_ex_c1),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2446,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(u2724,axiom,
    true = icext(uri_rdf_List,sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21) ).

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

cnf(u2620,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty),true,iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),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(u1190,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_rest),true) ).

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

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

cnf(u2231,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_rest,X0),true,icext(X0,sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22),true) ).

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

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

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

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

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

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

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

cnf(u2748,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41),true,true,true),true) ).

cnf(u187,axiom,
    true = iext(uri_owl_oneOf,uri_ex_c3,sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31) ).

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

cnf(u2229,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_rest,X0),true,icext(X0,sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32),true) ).

cnf(u2224,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_rest,X0),true,icext(X0,uri_rdf_nil),true) ).

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

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

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

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

cnf(u3093,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(u2608,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

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

cnf(u185,axiom,
    true = iext(uri_owl_oneOf,uri_ex_c1,sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11) ).

cnf(u2146,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Alt),true) ).

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

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

cnf(u3117,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(u699,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class) ).

cnf(u3013,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(u3094,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(u855,axiom,
    true = iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class) ).

cnf(u3121,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(u191,axiom,
    true = iext(uri_rdf_rest,sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42,uri_rdf_nil) ).

cnf(u3011,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(u3087,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(u3098,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(u3123,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(u3957,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__3),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true) ).

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

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

cnf(u2425,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12,X1),true,true,true),true) ).

cnf(u3026,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33,uri_rdf_List),true,true,true),true) ).

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

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

cnf(u3138,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_oneOf),true,ifeq(iext(X0,uri_ex_c2,sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21),true,true,true),true) ).

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

cnf(u2131,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_owl_oneOf,X0),true,icext(X0,sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31),true) ).

cnf(u3112,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(u3161,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Datatype,uri_rdfs_Resource),true) ).

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

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

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

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

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

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

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

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

cnf(u2664,axiom,
    true = icext(uri_rdf_List,sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42) ).

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

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

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

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

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

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

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

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

cnf(u231,negated_conjecture,
    true != sF0 ).

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

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

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

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

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

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

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

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

cnf(u3039,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41,sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42),true,true,true),true) ).

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

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

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

cnf(u3137,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_unionOf),true,ifeq(iext(X0,uri_ex_c4,sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41),true,true,true),true) ).

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

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

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

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

cnf(u3086,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(u3300,axiom,
    true = ifeq(iext(uri_owl_oneOf,X1,X0),true,iext(uri_owl_oneOf,X1,X0),true) ).

cnf(u2667,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42,X1),true,true,true),true) ).

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

cnf(u3079,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(u2068,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_object),true,true,true),true) ).

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

cnf(u215,axiom,
    true = iext(uri_rdf_first,sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32,uri_ex_w2) ).

cnf(u3070,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(u13,axiom,
    true = iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property) ).

cnf(u219,axiom,
    true = iext(uri_rdf_first,sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22,uri_ex_w3) ).

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

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

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

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

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

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

cnf(u3072,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(u3207,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_domain,uri_rdfs_Class),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3262,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41,uri_rdf_List),true) ).

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

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

cnf(u3124,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(u1161,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Seq),true) ).

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

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

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

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

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

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

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

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

cnf(u3723,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(u1174,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,uri_rdf_nil),true) ).

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

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

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

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

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

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

cnf(u1178,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_subClassOf),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(u1172,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,icext(X0,uri_rdf__3),true) ).

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

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

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

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

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

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

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

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

cnf(u2997,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(u1176,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_owl_unionOf),true) ).

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

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

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

cnf(u315,axiom,
    true = ifeq(sF0,true,ip(uri_owl_equivalentClass),true) ).

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

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

cnf(u424,axiom,
    true = iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property) ).

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

cnf(u2714,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11),true) ).

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

cnf(u2237,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_first,X0),true,icext(X0,uri_ex_c2),true) ).

cnf(u3024,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31,uri_rdf_List),true,true,true),true) ).

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

cnf(u3101,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(u3078,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(u702,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq) ).

cnf(u3141,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_equivalentClass),true,ifeq(iext(X0,uri_ex_c3,uri_ex_c4),true,sF0,true),true) ).

cnf(u3010,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(u936,axiom,
    true = icext(uri_rdf_Property,uri_rdf_value) ).

cnf(u3135,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(u3250,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11,uri_ex_w1),true) ).

cnf(u3107,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(u3728,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_List),true) ).

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

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

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

cnf(u3145,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_unionOf,X0),true,iext(X0,uri_ex_c4,sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41),true) ).

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

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

cnf(u3142,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_oneOf,X0),true,iext(X0,uri_ex_c3,sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31),true) ).

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

cnf(u3096,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(u87,axiom,
    true = iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource) ).

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

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

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

cnf(u2648,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33),true,true,true),true) ).

cnf(u3120,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(u1600,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_unionOf,X0),true,icext(X0,uri_ex_c4),true) ).

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

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

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

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

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

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

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

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

cnf(u2433,axiom,
    true = iext(uri_rdf_type,sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12,uri_rdf_List) ).

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

cnf(u3009,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(u3156,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Alt,uri_rdfs_Container),true) ).

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

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

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

cnf(u3023,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11,uri_rdf_List),true,true,true),true) ).

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

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

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

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

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

cnf(u2755,axiom,
    true = iext(uri_rdf_type,sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41,uri_rdf_List) ).

cnf(u213,axiom,
    true = iext(uri_rdf_first,sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31,uri_ex_w1) ).

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

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

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

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

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

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

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

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

cnf(u2453,axiom,
    true = iext(uri_rdf_type,sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22,uri_rdf_List) ).

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

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

cnf(u3054,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(u1781,axiom,
    true = icext(uri_rdf_Property,uri_rdf_predicate) ).

cnf(u203,axiom,
    true = iext(uri_rdf_rest,sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11,sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12) ).

cnf(u3125,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(u3288,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),true) ).

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

cnf(u230,axiom,
    iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4) = sF0 ).

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

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

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

cnf(u3065,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(u2071,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_domain),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3053,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(u3048,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(u3294,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_rest,uri_rdf_Property),true) ).

cnf(u2996,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(u2582,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0),true) ).

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

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

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

cnf(u2588,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0),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_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u397,axiom,
    true = ifeq(iext(uri_owl_oneOf,X1,X0),true,true,true) ).

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

cnf(u3111,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(u1629,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_owl_unionOf),true) ).

cnf(u3066,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(u798,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain) ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2452,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22),true) ).

cnf(u1171,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,icext(X0,uri_rdf__2),true) ).

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

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

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

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

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

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

cnf(u3104,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(u669,axiom,
    true = icext(uri_rdfs_Class,uri_rdf_Alt) ).

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

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

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

cnf(u566,axiom,
    true = ic(uri_rdfs_Container) ).

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

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

cnf(u2994,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(u2704,axiom,
    true = icext(uri_rdf_List,sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11) ).

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

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

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

cnf(u2445,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22,X1),true,true,true),true) ).

cnf(u2735,axiom,
    true = iext(uri_rdf_type,sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21,uri_rdf_List) ).

cnf(u3129,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(u1690,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_rest,X0),true,icext(X0,sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33),true) ).

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

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

cnf(u1597,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_oneOf,X0),true,icext(X0,uri_ex_c3),true) ).

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

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

cnf(u425,axiom,
    true = iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property) ).

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

cnf(u2982,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,X0),true,ifeq(sF0,true,iext(X0,uri_ex_c3,uri_ex_c4),true),true) ).

cnf(u941,axiom,
    true = icext(uri_rdf_Property,uri_rdf__2) ).

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

cnf(u3130,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(u3257,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42,uri_rdf_List),true) ).

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

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

cnf(u2988,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(u939,axiom,
    true = icext(uri_rdf_Property,uri_rdf__3) ).

cnf(u3254,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22,uri_rdf_List),true) ).

cnf(u3091,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(u71,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,X0),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true) ).

cnf(u3047,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12,uri_rdf_nil),true,true,true),true) ).

cnf(u3247,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33,uri_ex_w3),true) ).

cnf(u2993,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(u326,axiom,
    true = ip(uri_rdfs_subPropertyOf) ).

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

cnf(u3115,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(u3100,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(u3007,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(u3258,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31,uri_rdf_List),true) ).

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

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

cnf(u199,axiom,
    true = iext(uri_rdf_rest,sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21,sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22) ).

cnf(u2754,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41),true) ).

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

cnf(u3140,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_oneOf),true,ifeq(iext(X0,uri_ex_c3,sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31),true,true,true),true) ).

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

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

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

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

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

cnf(u3784,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(u197,axiom,
    true = iext(uri_rdf_rest,sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32,sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33) ).

cnf(u3144,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_oneOf,X0),true,iext(X0,uri_ex_c2,sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21),true) ).

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

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

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

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

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

cnf(u2635,axiom,
    true = iext(uri_rdf_type,sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32,uri_rdf_List) ).

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

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

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

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

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

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

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

cnf(u3038,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12,uri_ex_w2),true,true,true),true) ).

cnf(u109,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,X1),true,ifeq(iext(X0,X2,X3),true,icext(X1,X2),true),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3044,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33,uri_rdf_nil),true,true,true),true) ).

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

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

cnf(u2422,axiom,
    true = icext(uri_rdf_List,sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12) ).

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

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

cnf(u3037,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22,uri_ex_w3),true,true,true),true) ).

cnf(u3032,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11,uri_ex_w1),true,true,true),true) ).

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

cnf(u3110,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(u3804,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Statement),true) ).

cnf(u3035,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33,uri_ex_w3),true,true,true),true) ).

cnf(u5247,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_equivalentClass,uri_rdfs_Resource),true,ifeq(sF0,true,true,true),true) ).

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

cnf(u15,axiom,
    true = iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property) ).

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

cnf(u2999,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(u2747,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41,X1),true,true,true),true) ).

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

cnf(u3050,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(u2694,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31),true) ).

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

cnf(u703,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty) ).

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

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

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

cnf(u139,axiom,
    true = iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource) ).

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

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

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

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

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

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

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

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

cnf(u2695,axiom,
    true = iext(uri_rdf_type,sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31,uri_rdf_List) ).

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

cnf(u916,axiom,
    true = icext(uri_rdf_Property,uri_owl_oneOf) ).

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

cnf(u653,axiom,
    true = icext(uri_rdfs_Class,uri_rdfs_Seq) ).

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

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

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

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

cnf(u542,axiom,
    true = ip(uri_rdf__2) ).

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

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

cnf(u3679,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_List,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(u3090,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(u1180,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_subPropertyOf),true) ).

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

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

cnf(u398,axiom,
    true = ifeq(iext(uri_owl_unionOf,X1,X0),true,true,true) ).

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

cnf(u3029,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12,uri_rdf_List),true,true,true),true) ).

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

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

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

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

cnf(u3237,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32,sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33),true) ).

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

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

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

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

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

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

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

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

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

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

cnf(u3114,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(u3241,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11,sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12),true) ).

cnf(u2238,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_first,X0),true,icext(X0,uri_ex_w1),true) ).

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

cnf(u3238,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33,uri_rdf_nil),true) ).

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

cnf(u3102,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(u183,axiom,
    true = iext(uri_owl_oneOf,uri_ex_c2,sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21) ).

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

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

cnf(u1598,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_oneOf,X0),true,icext(X0,uri_ex_c1),true) ).

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

cnf(u2744,axiom,
    true = icext(uri_rdf_List,sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41) ).

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

cnf(u2991,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(u938,axiom,
    true = icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3) ).

cnf(u3031,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21,uri_ex_w2),true,true,true),true) ).

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

cnf(u181,axiom,
    true = iext(uri_owl_unionOf,uri_ex_c4,sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41) ).

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

cnf(u3099,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(u3084,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(u3036,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32,uri_ex_w2),true,true,true),true) ).

cnf(u3252,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41,uri_ex_c1),true) ).

cnf(u2226,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_rest,X0),true,icext(X0,sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33),true) ).

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

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

cnf(u3256,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33,uri_rdf_List),true) ).

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

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

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

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

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

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

cnf(u850,axiom,
    true = iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class) ).

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

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

cnf(u2647,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33,X1),true,true,true),true) ).

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

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

cnf(u576,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource) ).

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

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

cnf(u3028,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22,uri_rdf_List),true,true,true),true) ).

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

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

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

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

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

cnf(u3033,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31,uri_ex_w1),true,true,true),true) ).

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

cnf(u83,axiom,
    true = iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource) ).

cnf(u2654,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33),true) ).

cnf(u221,axiom,
    true = iext(uri_rdf_first,sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11,uri_ex_w1) ).

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

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

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

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

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

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

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

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

cnf(u2675,axiom,
    true = iext(uri_rdf_type,sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42,uri_rdf_List) ).

cnf(u81,axiom,
    true = iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource) ).

cnf(u860,axiom,
    true = iext(uri_rdf_type,X0,uri_rdfs_Resource) ).

cnf(u211,axiom,
    true = iext(uri_rdf_first,sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33,uri_ex_w3) ).

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

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

cnf(u3016,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(u3799,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(u1564,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf__2,X1),true,true,true),true) ).

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

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

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

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

cnf(u3695,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List) ).

cnf(u2684,axiom,
    true = icext(uri_rdf_List,sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31) ).

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

cnf(u209,axiom,
    true = iext(uri_rdf_first,sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42,uri_ex_c2) ).

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

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

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

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

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

cnf(u3034,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42,uri_ex_c2),true,true,true),true) ).

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

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

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

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

cnf(u3040,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21,sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22),true,true,true),true) ).

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

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

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

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

cnf(u2288,axiom,
    true = ifeq(iext(uri_rdfs_comment,X1,X0),true,icext(uri_rdfs_Literal,X0),true) ).

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

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

cnf(u2061,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_owl_equivalentClass,X0),true,ifeq(sF0,true,icext(X0,uri_ex_c4),true),true) ).

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

cnf(u791,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_owl_oneOf,uri_owl_oneOf) ).

cnf(u3255,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32,uri_rdf_List),true) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(u33,axiom,
    true = iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property) ).

cnf(u3074,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(u1164,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Container),true) ).

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

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

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

cnf(u3097,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(u1828,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_label),true) ).

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

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

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

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

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

cnf(u39,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource) ).

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

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

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

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

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

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

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

cnf(u3697,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(u2091,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Literal),true,true,true),true) ).

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

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

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

cnf(u37,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal) ).

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

cnf(u167,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property) ).

cnf(u2432,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12),true) ).

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

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

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

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

cnf(u422,axiom,
    true = iext(uri_rdf_type,uri_owl_unionOf,uri_rdf_Property) ).

cnf(u3245,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22,uri_ex_w3),true) ).

cnf(u2728,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21),true,true,true),true) ).

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

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

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

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

cnf(u2219,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_List),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(u928,axiom,
    true = icext(uri_rdf_Property,uri_rdfs_seeAlso) ).

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

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

cnf(u3022,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21,uri_rdf_List),true,true,true),true) ).

cnf(u3236,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK7_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l22,uri_rdf_nil),true) ).

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

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

cnf(u3015,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(u1592,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_XMLLiteral,X1),true,true,true),true) ).

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

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

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

cnf(u3083,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(u3251,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21,uri_ex_w2),true) ).

cnf(u3006,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(u1605,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Seq),true) ).

cnf(u3020,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK1_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l41,uri_rdf_List),true,true,true),true) ).

cnf(u3240,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31,sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32),true) ).

cnf(u3025,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42,uri_rdf_List),true,true,true),true) ).

cnf(u2233,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_first,X0),true,icext(X0,uri_ex_w2),true) ).

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

cnf(u3143,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_oneOf,X0),true,iext(X0,uri_ex_c1,sK8_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l11),true) ).

cnf(u3260,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK6_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l21,uri_rdf_List),true) ).

cnf(u77,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource) ).

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

cnf(u2234,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_first,X0),true,icext(X0,uri_ex_w3),true) ).

cnf(u3012,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(u3147,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Datatype,uri_rdfs_Class),true) ).

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

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

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

cnf(u67,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container) ).

cnf(u205,axiom,
    true = iext(uri_rdf_rest,sK9_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l12,uri_rdf_nil) ).

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

cnf(u3005,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(u3000,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(u3069,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(u705,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container) ).

cnf(u2644,axiom,
    true = icext(uri_rdf_List,sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33) ).

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

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

cnf(u3064,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(u3003,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(u3264,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_predicate,uri_rdf_Property),true) ).

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

cnf(u65,axiom,
    true = iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List) ).

cnf(u195,axiom,
    true = iext(uri_rdf_rest,sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31,sK5_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l32) ).

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

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

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

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

cnf(u3122,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(u2668,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK2_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l42),true,true,true),true) ).

cnf(u107,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property) ).

cnf(u193,axiom,
    true = iext(uri_rdf_rest,sK3_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l33,uri_rdf_nil) ).

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

cnf(u2279,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X1),true,icext(X1,uri_rdfs_Resource),true) ).

cnf(u3018,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(u977,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member) ).

cnf(u3694,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource) ).

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

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

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

cnf(u105,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class) ).

cnf(u5455,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_owl_equivalentClass,uri_rdfs_Resource),true,ifeq(sF0,true,true,true),true) ).

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

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

cnf(u1559,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_equivalentClass,X0),true,ifeq(sF0,true,icext(X0,uri_ex_c3),true),true) ).

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

cnf(u1599,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_oneOf,X0),true,icext(X0,uri_ex_c2),true) ).

cnf(u3116,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(u111,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class) ).

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

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

cnf(u3059,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(u3281,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_range,uri_rdf_Property),true) ).

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

cnf(u2687,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK4_testcase_premise_fullish_021_Composite_Enumerations_BNODE_l31,X1),true,true,true),true) ).

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

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

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

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

cnf(u3077,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(u2090,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Resource),true,true,true),true) ).

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

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

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

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

cnf(u3063,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(u766,axiom,
    true = ip(uri_rdfs_isDefinedBy) ).

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

cnf(u23,axiom,
    true = iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property) ).

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

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

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

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

cnf(u2995,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) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SWB021-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38  % Computer : n002.cluster.edu
% 0.12/0.38  % Model    : x86_64 x86_64
% 0.12/0.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38  % Memory   : 8046.5625MB
% 0.12/0.38  % OS       : Linux 6.8.0-71-generic
% 0.12/0.38  % CPULimit : 300
% 0.12/0.38  % WCLimit  : 300
% 0.12/0.38  % DateTime : Mon Sep 28 07:07:07 UTC 2026
% 0.12/0.38  % CPUTime  : 
% 0.12/0.38  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.16/0.43  Running first-order theorem proving
% 0.16/0.43  Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.72/2.75  % (175703)Detected a unit-equality problem, will run specialized UEQ schedule.
% 10.72/2.75  % (175712)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=758765234:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 10.72/2.75  % (175712)Refutation not found, incomplete strategy
% 10.72/2.75  % (175712)------------------------------
% 10.72/2.75  % (175712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.75  % (175712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.75  % (175712)CaDiCaL version: 2.1.3
% 10.72/2.75  % (175712)Termination reason: Refutation not found, incomplete strategy
% 10.72/2.75  % (175712)Time elapsed: 0.043 s
% 10.72/2.75  % (175712)Peak memory usage: 89 MB
% 10.72/2.75  % (175712)Instructions burned: 139 (million)
% 10.72/2.75  % (175714)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=4268737136:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 10.72/2.75  % (175709)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=3340218699:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 10.72/2.75  % (175710)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2709710446:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 10.72/2.75  % (175713)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=2914705294:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 10.72/2.75  % (175708)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=1887105224:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 10.72/2.75  % (175711)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2708467175:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 10.72/2.75  % (175714)Refutation not found, incomplete strategy
% 10.72/2.75  % (175714)------------------------------
% 10.72/2.75  % (175714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.75  % (175714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.75  % (175714)CaDiCaL version: 2.1.3
% 10.72/2.75  % (175714)Termination reason: Refutation not found, incomplete strategy
% 10.72/2.75  % (175714)Time elapsed: 0.035 s
% 10.72/2.75  % (175714)Peak memory usage: 88 MB
% 10.72/2.75  % (175714)Instructions burned: 67 (million)
% 10.72/2.75  % (175711)Instruction limit reached! 
% 10.72/2.75  % (175711)------------------------------
% 10.72/2.75  % (175711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.75  % (175711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.75  % (175711)CaDiCaL version: 2.1.3
% 10.72/2.75  % (175711)Termination reason: Instruction limit
% 10.72/2.75  % (175711)Termination phase: Saturation
% 10.72/2.75  % (175711)Time elapsed: 0.068 s
% 10.72/2.75  % (175711)Peak memory usage: 88 MB
% 10.72/2.75  % (175711)Instructions burned: 137 (million)
% 10.72/2.75  % (175713)Instruction limit reached! 
% 10.72/2.75  % (175713)------------------------------
% 10.72/2.75  % (175713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.75  % (175713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.75  % (175713)CaDiCaL version: 2.1.3
% 10.72/2.75  % (175713)Termination reason: Instruction limit
% 10.72/2.75  % (175713)Termination phase: Saturation
% 10.72/2.75  % (175713)Time elapsed: 0.145 s
% 10.72/2.75  % (175713)Peak memory usage: 93 MB
% 10.72/2.75  % (175713)Instructions burned: 257 (million)
% 10.72/2.75  % (175712)------------------------------
% 10.72/2.75  % (175712)------------------------------
% 10.72/2.75  % (175781)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=4253735786:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 10.72/2.75  % (175814)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1311154256:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 10.72/2.75  % (175714)------------------------------
% 10.72/2.75  % (175714)------------------------------
% 10.72/2.75  % (175811)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3646599668:i=4948:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/4948Mi)
% 10.72/2.75  % (175814)Instruction limit reached! 
% 10.72/2.75  % (175814)------------------------------
% 10.72/2.75  % (175814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.75  % (175814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.75  % (175814)CaDiCaL version: 2.1.3
% 10.72/2.75  % (175814)Termination reason: Instruction limit
% 10.72/2.75  % (175814)Termination phase: Saturation
% 10.72/2.75  % (175814)Time elapsed: 0.051 s
% 10.72/2.75  % (175814)Peak memory usage: 92 MB
% 10.72/2.75  % (175814)Instructions burned: 217 (million)
% 10.72/2.75  % (175878)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=2552136241:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2995 on theBenchmark for (2995ds/12125Mi)
% 10.72/2.75  % (175870)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=2462986602:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2995 on theBenchmark for (2995ds/317Mi)
% 10.72/2.75  % (175870)Instruction limit reached! 
% 10.72/2.75  % (175870)------------------------------
% 10.72/2.75  % (175870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.75  % (175870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.75  % (175870)CaDiCaL version: 2.1.3
% 10.72/2.75  % (175870)Termination reason: Instruction limit
% 10.72/2.75  % (175870)Termination phase: Saturation
% 10.72/2.75  % (175870)Time elapsed: 0.174 s
% 10.72/2.75  % (175870)Peak memory usage: 95 MB
% 10.72/2.75  % (175870)Instructions burned: 317 (million)
% 10.72/2.75  [W928 07:07:08.717313900 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.75  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.75  [W928 07:07:08.717350962 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.75  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.75  [W928 07:07:08.717370956 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.75  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.75  [W928 07:07:08.717377093 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.75  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.75  [W928 07:07:08.717390995 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.75  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.75  [W928 07:07:08.717396482 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.75  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.75  [W928 07:07:08.779898467 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.75  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.75  [W928 07:07:08.779945678 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.75  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.75  [W928 07:07:08.779980944 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.75  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.75  [W928 07:07:08.779993144 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.75  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.75  [W928 07:07:08.780030088 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.75  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.75  [W928 07:07:08.780042171 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type  (currently Float) in python but a tensor of type int in torchscript.
% 10.72/2.75  Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 10.72/2.75  % (175878)Refutation not found, incomplete strategy
% 10.72/2.75  % (175878)------------------------------
% 10.72/2.75  % (175878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.75  % (175878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.75  % (175878)CaDiCaL version: 2.1.3
% 10.72/2.75  % (175878)Termination reason: Refutation not found, incomplete strategy
% 10.72/2.75  % (175878)Time elapsed: 0.339 s
% 10.72/2.75  % (175878)Peak memory usage: 127 MB
% 10.72/2.75  % (175878)Instructions burned: 861 (million)
% 10.72/2.75  % (175884)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1578870201:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2992 on theBenchmark for (2992ds/2836Mi)
% 10.72/2.75  % (175811)Refutation not found, incomplete strategy
% 10.72/2.75  % (175811)------------------------------
% 10.72/2.75  % (175811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.75  % (175811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.75  % (175811)CaDiCaL version: 2.1.3
% 10.72/2.75  % (175811)Termination reason: Refutation not found, incomplete strategy
% 10.72/2.75  % (175811)Time elapsed: 0.585 s
% 10.72/2.75  % (175811)Peak memory usage: 127 MB
% 10.72/2.75  % (175811)Instructions burned: 871 (million)
% 10.72/2.75  % (175878)------------------------------
% 10.72/2.75  % (175878)------------------------------
% 10.72/2.75  % (175811)------------------------------
% 10.72/2.75  % (175811)------------------------------
% 10.72/2.75  % (175884)First to succeed.
% 10.72/2.75  % (175884)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-175703"
% 10.72/2.75  % (175886)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=4042347615:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2988 on theBenchmark for (2988ds/14534Mi)
% 10.72/2.75  % (175781)Instruction limit reached! 
% 10.72/2.75  % (175781)------------------------------
% 10.72/2.75  % (175781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.72/2.75  % (175781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.72/2.75  % (175781)CaDiCaL version: 2.1.3
% 10.72/2.75  % (175781)Termination reason: Instruction limit
% 10.72/2.75  % (175781)Termination phase: Saturation
% 10.72/2.75  % (175781)Time elapsed: 0.982 s
% 10.72/2.75  % (175781)Peak memory usage: 143 MB
% 10.72/2.75  % (175781)Instructions burned: 2052 (million)
% 10.72/2.75  % (175887)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=2030199267:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2987 on theBenchmark for (2987ds/11832Mi)
% 10.72/2.75  % (175889)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=unused:sp=const_min:spb=goal:fd=preordered:random_seed=3370253936:i=2279:fgj=on:bd=all_2986 on theBenchmark for (2986ds/2279Mi)
% 10.72/2.75  % SZS status Satisfiable for theBenchmark
% 10.72/2.75  % SZS output start Saturation.
% See solution above
% 11.80/2.84  % SZS output start Definitions and Model Updates.
% 11.80/2.84  for all inputs,
% 11.80/2.84      define ir(X0) := true
% 11.80/2.84  % SZS output end Definitions and Model Updates.
% 11.80/2.84  % (175884)------------------------------
% 11.80/2.84  % (175884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.80/2.84  % (175884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.80/2.84  % (175884)CaDiCaL version: 2.1.3
% 11.80/2.84  % (175884)Termination reason: Satisfiable
% 11.80/2.84  % (175884)Time elapsed: 0.370 s
% 11.80/2.84  % (175884)Peak memory usage: 105 MB
% 11.80/2.84  % (175884)Instructions burned: 675 (million)
% 11.80/2.84  % (175884)------------------------------
% 11.80/2.84  % (175884)------------------------------
% 11.80/2.84  % (175703)Success in time 1.563 s
% 11.80/2.84  % Vampire exiting
%------------------------------------------------------------------------------