Vampire---5.0.1.SAT-Sat.s

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

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

% Result   : Satisfiable 5.79s 2.01s
% Output   : Saturation 8.42s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u661,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_object),true) ).

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

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

cnf(u248,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(u2434,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Literal,X1),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u1681,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(u1156,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_object,uri_rdfs_Statement),true,true,true) ).

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

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

cnf(u2458,axiom,
    true = ifeq(iext(uri_owl_equivalentClass,X0,X1),true,true,true) ).

cnf(u417,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(u2868,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf__2),true) ).

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

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

cnf(u404,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_owl_equivalentClass,X0),true,icext(X0,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z),true) ).

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

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

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

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

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

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

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

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

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

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

cnf(u569,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_onProperty),true,ifeq(iext(X0,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z,uri_owl_inverseOf),true,true,true),true) ).

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

cnf(u561,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(u316,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdf_Property),true) ).

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

cnf(u575,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0),true,iext(X0,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z,uri_owl_inverseOf),true) ).

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

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

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

cnf(u1953,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(u2673,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(u51,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource) ).

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

cnf(u189,negated_conjecture,
    true != iext(uri_rdfs_subClassOf,uri_ex_InversesOfFunctionalProperties,uri_owl_InverseFunctionalProperty) ).

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

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

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

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

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

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

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

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

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

cnf(u1861,axiom,
    true = iext(uri_rdfs_subClassOf,uri_owl_Restriction,uri_rdfs_Resource) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u333,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(u584,axiom,
    true = ifeq(iext(uri_rdf__1,X0,X1),true,icext(uri_rdfs_Resource,X1),true) ).

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

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

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

cnf(u833,axiom,
    true = ip(uri_owl_equivalentClass) ).

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

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

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

cnf(u3663,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(u1098,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_first,uri_rdf_List),true,true,true) ).

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

cnf(u1092,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Resource),true,true,true) ).

cnf(u2419,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_owl_Restriction),true,ifeq(iext(X0,X1,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z),true,true,true),true) ).

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

cnf(u3606,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(u346,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__3,uri_rdf_Property),true) ).

cnf(u372,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_owl_Restriction),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u6325,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(u95,axiom,
    true = iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty) ).

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

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

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

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

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

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

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

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

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

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

cnf(u223,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(u361,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_object,uri_rdf_Property),true,true,true),true) ).

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

cnf(u3634,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(u4734,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_owl_someValuesFrom,uri_owl_someValuesFrom),true) ).

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

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

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

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

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

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

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

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

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

cnf(u489,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(u756,axiom,
    true = ifeq(ip(uri_rdf__1),true,true,true) ).

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

cnf(u645,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0),true,iext(X0,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z,uri_owl_FunctionalProperty),true) ).

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

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

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

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

cnf(u643,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_owl_someValuesFrom,X0),true,icext(X0,uri_owl_FunctionalProperty),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u647,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(u522,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_value,uri_rdfs_Resource),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u4736,axiom,
    true = icext(uri_rdf_Property,uri_owl_someValuesFrom) ).

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

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

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

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

cnf(u319,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(u405,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_equivalentClass,X0),true,icext(X0,uri_ex_InversesOfFunctionalProperties),true) ).

cnf(u656,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(u290,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),true) ).

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

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

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

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

cnf(u2462,axiom,
    true = iext(uri_rdf_type,uri_owl_equivalentClass,uri_rdf_Property) ).

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

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

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

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

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

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

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

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

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

cnf(u2973,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,uri_owl_someValuesFrom) ).

cnf(u2968,axiom,
    true = ifeq(iext(uri_owl_someValuesFrom,X0,X1),true,true,true) ).

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

cnf(u3287,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(u1971,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource) ).

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

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

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

cnf(u3757,axiom,
    true = ifeq(iext(uri_owl_equivalentClass,X0,X1),true,iext(uri_owl_equivalentClass,X0,X1),true) ).

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

cnf(u3511,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(u690,axiom,
    true = ifeq(iext(uri_rdf_rest,X0,X1),true,icext(uri_rdf_List,X1),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3246,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(u2213,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_isDefinedBy,X1),true,true,true),true) ).

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

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

cnf(u435,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(u1052,axiom,
    true = ifeq(iext(uri_rdfs_label,X0,X1),true,true,true) ).

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

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

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

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

cnf(u2618,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(u1734,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Resource,X1),true,true,true),true) ).

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

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

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

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

cnf(u2887,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),true,true,true) ).

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

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

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

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

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

cnf(u1862,axiom,
    true = iext(uri_rdfs_subClassOf,uri_owl_Restriction,uri_owl_Restriction) ).

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

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

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

cnf(u3905,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(u2500,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource) ).

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

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

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

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

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

cnf(u2396,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(u347,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(u717,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,icext(uri_rdf_Property,X1),true) ).

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

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

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

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

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

cnf(u1819,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(u629,axiom,
    true = ifeq(iext(uri_rdf__3,X0,X1),true,icext(uri_rdfs_Resource,X1),true) ).

cnf(u368,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z,uri_owl_Restriction),true,true,true),true) ).

cnf(u462,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(u5692,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_first),true) ).

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

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

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

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

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

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

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

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

cnf(u1626,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(u2913,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,X0),true,icext(uri_rdfs_Datatype,X0),true) ).

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

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

cnf(u374,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z,uri_owl_Restriction),true) ).

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

cnf(u1912,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_owl_Restriction),true,iext(uri_rdfs_subClassOf,X0,uri_owl_Restriction),true) ).

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

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

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

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

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

cnf(u4741,axiom,
    true = ifeq(iext(uri_owl_someValuesFrom,X0,X1),true,iext(uri_owl_someValuesFrom,X0,X1),true) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(u1760,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(u631,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(u2162,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),true) ).

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

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

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

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

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

cnf(u385,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(u745,axiom,
    true = icext(uri_rdf_Property,uri_rdf__1) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u284,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(u1574,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_ContainerMembershipProperty),true,true,true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2446,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(u671,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_predicate,uri_rdfs_Resource),true) ).

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

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

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

cnf(u552,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(u431,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_member),true) ).

cnf(u2952,axiom,
    true = iext(uri_rdf_type,uri_owl_onProperty,uri_rdf_Property) ).

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

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

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

cnf(u3427,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(u1435,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal) ).

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

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

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

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

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

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

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

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

cnf(u291,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(u2470,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource) ).

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

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

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

cnf(u400,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_equivalentClass),true,ifeq(iext(X0,uri_ex_InversesOfFunctionalProperties,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z),true,true,true),true) ).

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

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

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

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

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

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

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

cnf(u187,axiom,
    true = iext(uri_rdf_type,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z,uri_owl_Restriction) ).

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

cnf(u573,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_owl_onProperty,X0),true,icext(X0,uri_owl_inverseOf),true) ).

cnf(u312,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(u2381,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Statement,uri_rdfs_Resource),true) ).

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

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

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

cnf(u1852,axiom,
    true = ifeq(icext(X0,uri_owl_Restriction),true,true,true) ).

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

cnf(u1915,axiom,
    true = ifeq(icext(uri_owl_Restriction,X0),true,icext(uri_owl_Restriction,X0),true) ).

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

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

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

cnf(u185,axiom,
    true = iext(uri_owl_equivalentClass,uri_ex_InversesOfFunctionalProperties,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z) ).

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

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

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

cnf(u701,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(u440,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_member),true) ).

cnf(u2375,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(u1717,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_domain,uri_rdf_Property),true) ).

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

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

cnf(u340,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(u2898,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(u2736,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Datatype),true,true,true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u613,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(u5051,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_owl_onProperty,uri_owl_onProperty),true) ).

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

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

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

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

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

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

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

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

cnf(u2193,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(u103,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,X0),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal),true) ).

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

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

cnf(u5058,axiom,
    true = ifeq(iext(uri_owl_onProperty,X0,X1),true,iext(uri_owl_onProperty,X0,X1),true) ).

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

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

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

cnf(u1527,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(u973,axiom,
    true = ifeq(icext(uri_rdf_Bag,X0),true,icext(uri_rdfs_Container,X0),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u758,axiom,
    true = ifeq(ip(uri_rdf__3),true,true,true) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(u1656,axiom,
    true = ifeq(icext(X0,uri_rdf_type),true,true,true) ).

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

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

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

cnf(u2225,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(u2427,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Literal),true,true,true) ).

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

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

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

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

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

cnf(u2948,axiom,
    true = ifeq(iext(uri_owl_onProperty,X0,X1),true,true,true) ).

cnf(u2421,axiom,
    true = ifeq(icext(X0,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z),true,true,true) ).

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

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

cnf(u2953,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,uri_owl_onProperty) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u1412,axiom,
    true = ifeq(icext(X0,uri_rdfs_subClassOf),true,true,true) ).

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

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

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

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

cnf(u5966,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(u2349,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(u3208,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Datatype),true,ifeq(iext(X0,X1,uri_rdf_XMLLiteral),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u298,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(u3461,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Resource),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u426,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(u3517,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Seq,uri_rdfs_Resource),true) ).

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

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

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

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

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

cnf(u1593,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(u548,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

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

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

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

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

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

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

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

cnf(u2714,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(u683,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(u574,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_onProperty,X0),true,icext(X0,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z),true) ).

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

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

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

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

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

cnf(u2828,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(u2492,axiom,
    true = ifeq(icext(X0,uri_rdf_nil),true,true,true) ).

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

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

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

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

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

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

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

cnf(u3774,axiom,
    true = ifeq(icext(X0,uri_owl_equivalentClass),true,true,true) ).

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

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

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

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

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

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

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

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

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

cnf(u5764,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(u595,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(u2142,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_List,uri_rdfs_Class),true) ).

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

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

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

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

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

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

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

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

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

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

cnf(u4803,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(u2684,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Seq,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,X0),true) ).

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

cnf(u2272,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(u2701,axiom,
    true = ifeq(icext(X0,uri_rdf_first),true,true,true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2755,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(u1486,axiom,
    true = iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class) ).

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

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

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

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

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

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

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

cnf(u224,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(u1519,axiom,
    true = iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class) ).

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

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

cnf(u1889,axiom,
    true = ifeq(icext(uri_owl_Restriction,X0),true,true,true) ).

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

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

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

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

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

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

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

cnf(u1057,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Resource),true,true,true) ).

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

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

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

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

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

cnf(u639,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_someValuesFrom),true,ifeq(iext(X0,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z,uri_owl_FunctionalProperty),true,true,true),true) ).

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

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

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

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

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

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

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

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

cnf(u736,axiom,
    true = icext(uri_owl_Restriction,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z) ).

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

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

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

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

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

cnf(u228,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(u1400,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf) ).

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

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

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

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

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

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

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

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

cnf(u269,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(u399,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_type,uri_rdf_Property),true) ).

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

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

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

cnf(u1053,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Resource),true,true,true) ).

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

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

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

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

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

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

cnf(u1020,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_first,uri_rdfs_Resource),true,true,true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3752,axiom,
    true = icext(uri_rdf_Property,uri_owl_equivalentClass) ).

cnf(u2994,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(u159,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property) ).

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

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

cnf(u1854,axiom,
    true = ic(uri_owl_Restriction) ).

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

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

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

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

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

cnf(u406,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,X0),true,iext(X0,uri_ex_InversesOfFunctionalProperties,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u939,axiom,
    true = ip(uri_rdfs_subPropertyOf) ).

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

cnf(u5053,axiom,
    true = icext(uri_rdf_Property,uri_owl_onProperty) ).

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

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

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

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

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

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

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

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

cnf(u69,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u5836,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(u3916,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,X0),true) ).

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

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

cnf(u586,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(u4809,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_seeAlso,uri_rdfs_seeAlso),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(u3854,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_predicate,uri_rdf_predicate),true) ).

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

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

cnf(u471,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(u1746,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u354,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(u737,axiom,
    true = icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral) ).

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

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

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

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

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

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

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

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

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

cnf(u1995,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(u2537,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource) ).

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

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

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

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

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

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

cnf(u225,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(u1711,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(u2053,axiom,
    true = ifeq(ic(uri_rdf_List),true,true,true) ).

cnf(u760,axiom,
    true = ifeq(ip(uri_rdf_value),true,true,true) ).

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

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

cnf(u480,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(u252,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u6299,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(u49,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource) ).

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

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

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

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

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

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

cnf(u525,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(u264,axiom,
    true = ic(uri_rdfs_Seq) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u143,axiom,
    true = iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2972,axiom,
    true = iext(uri_rdf_type,uri_owl_someValuesFrom,uri_rdf_Property) ).

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

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

cnf(u183,axiom,
    true = iext(uri_owl_onProperty,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z,uri_owl_inverseOf) ).

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

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

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

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

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

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

cnf(u2136,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(u567,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_first,uri_rdfs_Resource),true) ).

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

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

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

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

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

cnf(u181,axiom,
    true = iext(uri_owl_someValuesFrom,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z,uri_owl_FunctionalProperty) ).

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

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

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

cnf(u5687,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(u681,axiom,
    true = ifeq(iext(uri_rdf_predicate,X0,X1),true,icext(uri_rdfs_Statement,X0),true) ).

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

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

cnf(u835,axiom,
    true = ip(uri_owl_someValuesFrom) ).

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

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

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

cnf(u3541,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(u93,axiom,
    true = iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u167,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property) ).

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

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

cnf(u1494,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(u1781,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(u367,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_object,uri_rdf_Property),true) ).

cnf(u453,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(u4815,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_seeAlso),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_seeAlso),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2929,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(u1140,axiom,
    true = icext(uri_rdfs_Class,uri_rdfs_Literal) ).

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

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

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

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

cnf(u2025,axiom,
    true = ifeq(icext(X0,uri_rdfs_label),true,true,true) ).

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

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

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

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

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

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

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

cnf(u2420,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_owl_Restriction,X0),true,icext(X0,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z),true) ).

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

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

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

cnf(u1838,axiom,
    true = ifeq(ic(uri_owl_Restriction),true,true,true) ).

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

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

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

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

cnf(u3874,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(u2977,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_member,X0),true,true,true) ).

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

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

cnf(u376,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(u2094,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_List),true) ).

cnf(u226,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(u3258,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u763,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(u1654,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_type),true,true,true),true) ).

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

cnf(u1853,axiom,
    true = iext(uri_rdf_type,uri_owl_Restriction,uri_rdfs_Class) ).

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

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

cnf(u265,axiom,
    true = ic(uri_rdfs_ContainerMembershipProperty) ).

cnf(u532,axiom,
    true = ifeq(iext(uri_rdf__3,X0,X1),true,icext(uri_rdfs_Resource,X0),true) ).

cnf(u2067,axiom,
    true = ifeq(icext(X0,uri_rdf_List),true,true,true) ).

cnf(u549,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_Resource),true) ).

cnf(u288,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u2437,axiom,
    true = ifeq(icext(X0,uri_rdfs_Literal),true,true,true) ).

cnf(u3466,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,X0),true) ).

cnf(u1425,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,X1,uri_rdfs_Resource),true) ).

cnf(u2970,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0),true,true,true) ).

cnf(u4740,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_someValuesFrom),true,iext(uri_rdfs_subPropertyOf,X0,uri_owl_someValuesFrom),true) ).

cnf(u1411,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

cnf(u654,axiom,
    true = ifeq(iext(uri_rdf_subject,X0,X1),true,icext(uri_rdfs_Statement,X0),true) ).

cnf(u4757,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_owl_someValuesFrom),true,true,true),true) ).

cnf(u2463,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,uri_owl_equivalentClass) ).

cnf(u5076,axiom,
    true = ifeq(icext(X0,uri_owl_onProperty),true,true,true) ).

cnf(u1016,axiom,
    true = iext(uri_rdf_type,X0,uri_rdfs_Resource) ).

cnf(u1671,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u540,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_first,uri_rdf_List),true) ).

cnf(u393,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(u2076,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource) ).

cnf(u2095,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_List,uri_rdf_List),true) ).

cnf(u2261,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,uri_rdfs_Literal),true,true,true) ).

cnf(u2950,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0),true,true,true) ).

cnf(u909,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true,ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,true,true),true) ).

cnf(u1552,axiom,
    true = iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class) ).

cnf(u2847,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf__1,X0),true,true,true) ).

cnf(u1911,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_owl_Restriction,X0),true,iext(uri_rdfs_subClassOf,uri_owl_Restriction,X0),true) ).

cnf(u566,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_first),true) ).

cnf(u907,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true,ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0),true,true,true),true) ).

cnf(u2597,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Bag,uri_rdf_Bag),true) ).

cnf(u37,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal) ).

cnf(u4814,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,X0),true) ).

cnf(u1583,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u305,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(u3470,axiom,
    true = ifeq(icext(uri_rdf_XMLLiteral,X0),true,true,true) ).

cnf(u5777,axiom,
    true = ifeq(iext(uri_rdf_subject,X0,X1),true,iext(uri_rdf_subject,X0,X1),true) ).

cnf(u1691,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,true,true) ).

cnf(u422,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_range),true) ).

cnf(u3376,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u755,axiom,
    true = ifeq(ip(uri_rdf_rest),true,true,true) ).

cnf(u2361,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement),true) ).

cnf(u2975,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0),true,true,true) ).

cnf(u922,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty),true,iext(uri_rdfs_subClassOf,X0,uri_rdf_Property),true) ).

cnf(u3298,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X0),true) ).

cnf(u5803,axiom,
    true = ifeq(iext(uri_rdf_object,X0,X1),true,iext(uri_rdf_object,X0,X1),true) ).

cnf(u3878,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_label),true) ).

cnf(u165,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,ifeq(iext(X0,X2,X3),true,iext(X1,X2,X3),true),true) ).

cnf(u311,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_Property,uri_rdfs_Class),true) ).

cnf(u433,axiom,
    true = ifeq(iext(uri_rdfs_member,X0,X1),true,icext(uri_rdfs_Resource,X0),true) ).

cnf(u4759,axiom,
    true = ifeq(icext(X0,uri_owl_someValuesFrom),true,true,true) ).

cnf(u2528,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource) ).

cnf(u665,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(u5796,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_object,uri_rdf_object),true) ).

cnf(u2603,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag),true,iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag),true) ).

cnf(u2360,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Statement,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,X0),true) ).

cnf(u679,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_predicate),true) ).

cnf(u1442,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_XMLLiteral),true,true,true) ).

cnf(u4777,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

cnf(u2173,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_seeAlso),true,true,true) ).

cnf(u439,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u2460,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,X0),true,true,true) ).

cnf(u1185,axiom,
    true = icext(uri_rdf_Property,uri_rdfs_subPropertyOf) ).

cnf(u105,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class) ).

cnf(u1515,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Seq,X1),true,true,true),true) ).

cnf(u834,axiom,
    true = ip(uri_owl_onProperty) ).

cnf(u2773,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_rest,X1),true,true,true),true) ).

cnf(u4785,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_isDefinedBy),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_isDefinedBy),true) ).

cnf(u2555,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u5616,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,X1),true,iext(uri_rdfs_range,X0,X1),true) ).

cnf(u77,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource) ).

cnf(u2861,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf__2,X0),true,true,true) ).

cnf(u688,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u1983,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_comment,X1),true,true,true),true) ).

cnf(u3848,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(u577,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(u3012,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member) ).

cnf(u1692,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,true,true) ).

cnf(u3136,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf) ).

cnf(u591,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u5862,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(u67,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container) ).

cnf(u3000,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_member,uri_rdf_Property),true) ).

cnf(u2567,axiom,
    true = ifeq(icext(X0,uri_rdf__2),true,true,true) ).

cnf(u6055,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_subClassOf,uri_rdf_Property),true) ).

cnf(u2418,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_owl_Restriction),true,ifeq(iext(X0,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z,X1),true,true,true),true) ).

cnf(u460,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,X1),true,icext(uri_rdf_Property,X0),true) ).

cnf(u6273,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(u3553,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u1482,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_Bag,X1),true,true,true),true) ).

cnf(u2257,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,true,true) ).

cnf(u65,axiom,
    true = iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List) ).

cnf(u1476,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Bag),true,true,true) ).

cnf(u3523,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u4950,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true) ).

cnf(u2005,axiom,
    true = ip(uri_rdfs_comment) ).

cnf(u600,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u4758,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_owl_someValuesFrom),true) ).

cnf(u4943,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_domain),true) ).

cnf(u450,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_domain,uri_rdf_Property),true) ).

cnf(u2789,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_object),true) ).

cnf(u2217,axiom,
    true = iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property) ).

cnf(u1365,axiom,
    true = icext(uri_rdfs_Class,uri_owl_Restriction) ).

cnf(u4808,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u107,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property) ).

cnf(u972,axiom,
    true = ifeq(icext(uri_rdfs_ContainerMembershipProperty,X0),true,icext(uri_rdf_Property,X0),true) ).

cnf(u339,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_value,uri_rdf_Property),true) ).

cnf(u477,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_comment,uri_rdfs_Resource),true) ).

cnf(u2023,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_label),true,true,true),true) ).

cnf(u448,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_Property),true) ).

cnf(u4938,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(u2649,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Alt),true) ).

cnf(u1123,axiom,
    true = icext(uri_rdfs_Class,uri_rdf_XMLLiteral) ).

cnf(u2790,axiom,
    true = ifeq(icext(X0,uri_rdf_object),true,true,true) ).

cnf(u707,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_subPropertyOf,uri_rdf_Property),true) ).

cnf(u6312,axiom,
    true = ifeq(iext(uri_rdf__1,X0,X1),true,iext(uri_rdfs_member,X0,X1),true) ).

cnf(u2529,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt) ).

cnf(u1516,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Seq),true,true,true),true) ).

cnf(u467,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

cnf(u2277,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Literal),true) ).

cnf(u360,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_rest,uri_rdf_Property),true) ).

cnf(u6012,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(u1900,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_owl_Restriction,uri_owl_Restriction),true,true,true),true) ).

cnf(u619,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_value,uri_rdfs_Resource),true) ).

cnf(u5089,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(u4733,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_owl_someValuesFrom),true) ).

cnf(u1599,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Class),true) ).

cnf(u2656,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0),true) ).

cnf(u111,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class) ).

cnf(u5609,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_range,uri_rdfs_range),true) ).

cnf(u2428,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Literal),true,true,true) ).

cnf(u2066,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_List),true) ).

cnf(u2951,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_onProperty),true,true,true) ).

cnf(u366,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,icext(X0,uri_rdf_object),true) ).

cnf(u749,axiom,
    true = icext(uri_rdf_Property,uri_rdf_first) ).

cnf(u1904,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_owl_Restriction),true) ).

cnf(u6336,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf__3,X0),true) ).

cnf(u2028,axiom,
    true = ifeq(ip(uri_rdfs_label),true,true,true) ).

cnf(u747,axiom,
    true = icext(uri_rdf_Property,uri_rdf_rest) ).

cnf(u638,axiom,
    true = ifeq(iext(uri_rdf_subject,X0,X1),true,icext(uri_rdfs_Resource,X1),true) ).

cnf(u1533,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Seq,uri_rdfs_Class),true) ).

cnf(u5001,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_owl_equivalentClass,uri_rdf_Property),true,true,true),true) ).

cnf(u1655,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u2026,axiom,
    true = iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property) ).

cnf(u2801,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_subject),true,true,true),true) ).

cnf(u516,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(u507,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(u5849,axiom,
    true = ifeq(iext(uri_rdf_value,X0,X1),true,iext(uri_rdf_value,X0,X1),true) ).

cnf(u3861,axiom,
    true = ifeq(iext(uri_rdf_predicate,X0,X1),true,iext(uri_rdf_predicate,X0,X1),true) ).

cnf(u5603,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(u494,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u5101,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true) ).

cnf(u2815,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_value),true) ).

cnf(u1409,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_subClassOf,X1),true,true,true),true) ).

cnf(u1837,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate) ).

cnf(u531,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf__3,uri_rdfs_Resource),true) ).

cnf(u5918,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u1094,axiom,
    true = ifeq(iext(uri_rdf_predicate,X0,X1),true,true,true) ).

cnf(u5875,axiom,
    true = ifeq(iext(uri_rdf__3,X0,X1),true,iext(uri_rdf__3,X0,X1),true) ).

cnf(u3078,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy) ).

cnf(u2743,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Datatype),true,true,true),true) ).

cnf(u23,axiom,
    true = iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property) ).

cnf(u1810,axiom,
    true = ifeq(icext(X0,uri_rdf_predicate),true,true,true) ).

cnf(u2089,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(u1060,axiom,
    true = ifeq(iext(uri_rdf_value,X0,X1),true,true,true) ).

cnf(u505,axiom,
    true = ifeq(iext(uri_rdf__1,X0,X1),true,icext(uri_rdfs_Resource,X0),true) ).

cnf(u644,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0),true,icext(X0,sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z),true) ).

cnf(u4739,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0),true,iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0),true) ).

cnf(u6286,axiom,
    true = ifeq(iext(uri_rdf__2,X0,X1),true,iext(uri_rdfs_member,X0,X1),true) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : SWB028-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.40  % Computer : n009.cluster.edu
% 0.11/0.40  % Model    : x86_64 x86_64
% 0.11/0.40  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.40  % Memory   : 8046.5625MB
% 0.11/0.40  % OS       : Linux 6.8.0-71-generic
% 0.11/0.40  % CPULimit : 300
% 0.11/0.40  % WCLimit  : 300
% 0.11/0.40  % DateTime : Mon Sep 28 07:06:15 UTC 2026
% 0.11/0.41  % CPUTime  : 
% 0.11/0.41  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.44  Running first-order theorem proving
% 0.11/0.44  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.79/2.01  % (2853457)Detected a unit-equality problem, will run specialized UEQ schedule.
% 5.79/2.01  % (2853463)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=790152435:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 5.79/2.01  % (2853462)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=3190895206:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 5.79/2.01  % (2853468)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=242525641:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 5.79/2.01  % (2853466)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=907062847:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 5.79/2.01  % (2853464)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=105284123:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 5.79/2.01  % (2853465)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=4127018221:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 5.79/2.01  % (2853467)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=57591634:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 5.79/2.01  % (2853465)Instruction limit reached! 
% 5.79/2.01  % (2853465)------------------------------
% 5.79/2.01  % (2853465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.79/2.01  % (2853465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/2.01  % (2853465)CaDiCaL version: 2.1.3
% 5.79/2.01  % (2853465)Termination reason: Instruction limit
% 5.79/2.01  % (2853465)Termination phase: Saturation
% 5.79/2.01  % (2853465)Time elapsed: 0.067 s
% 5.79/2.01  % (2853465)Peak memory usage: 88 MB
% 5.79/2.01  % (2853465)Instructions burned: 138 (million)
% 5.79/2.01  % (2853466)Refutation not found, incomplete strategy
% 5.79/2.01  % (2853466)------------------------------
% 5.79/2.01  % (2853466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.79/2.01  % (2853466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/2.01  % (2853466)CaDiCaL version: 2.1.3
% 5.79/2.01  % (2853466)Termination reason: Refutation not found, incomplete strategy
% 5.79/2.01  % (2853466)Time elapsed: 0.072 s
% 5.79/2.01  % (2853466)Peak memory usage: 89 MB
% 5.79/2.01  % (2853466)Instructions burned: 133 (million)
% 5.79/2.01  % (2853467)Instruction limit reached! 
% 5.79/2.01  % (2853467)------------------------------
% 5.79/2.01  % (2853467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.79/2.01  % (2853467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/2.01  % (2853467)CaDiCaL version: 2.1.3
% 5.79/2.01  % (2853467)Termination reason: Instruction limit
% 5.79/2.01  % (2853467)Termination phase: Saturation
% 5.79/2.01  % (2853467)Time elapsed: 0.153 s
% 5.79/2.01  % (2853467)Peak memory usage: 92 MB
% 5.79/2.01  % (2853467)Instructions burned: 258 (million)
% 5.79/2.01  % (2853476)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=2746380398:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 5.79/2.01  % (2853468)Refutation not found, incomplete strategy
% 5.79/2.01  % (2853468)------------------------------
% 5.79/2.01  % (2853468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.79/2.01  % (2853468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/2.01  % (2853468)CaDiCaL version: 2.1.3
% 5.79/2.01  % (2853468)Termination reason: Refutation not found, incomplete strategy
% 5.79/2.01  % (2853468)Time elapsed: 0.273 s
% 5.79/2.01  % (2853468)Peak memory usage: 93 MB
% 5.79/2.01  % (2853468)Instructions burned: 541 (million)
% 5.79/2.01  % (2853477)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2089384838:i=4948:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/4948Mi)
% 5.79/2.01  % (2853466)------------------------------
% 5.79/2.01  % (2853466)------------------------------
% 5.79/2.01  % (2853480)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=341586804:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 5.79/2.01  % (2853468)------------------------------
% 5.79/2.01  % (2853468)------------------------------
% 5.79/2.01  % (2853480)Instruction limit reached! 
% 5.79/2.01  % (2853480)------------------------------
% 5.79/2.01  % (2853480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.79/2.01  % (2853480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/2.01  % (2853480)CaDiCaL version: 2.1.3
% 5.79/2.01  % (2853480)Termination reason: Instruction limit
% 5.79/2.01  % (2853480)Termination phase: Saturation
% 5.79/2.01  % (2853480)Time elapsed: 0.095 s
% 5.79/2.01  % (2853480)Peak memory usage: 91 MB
% 5.79/2.01  % (2853480)Instructions burned: 218 (million)
% 5.79/2.01  % (2853482)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=201628314:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2993 on theBenchmark for (2993ds/317Mi)
% 5.79/2.01  % (2853483)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=3838812652:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2993 on theBenchmark for (2993ds/12125Mi)
% 5.79/2.01  % (2853463)First to succeed.
% 5.79/2.01  % (2853463)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2853457"
% 5.79/2.01  % (2853482)Instruction limit reached! 
% 5.79/2.01  % (2853482)------------------------------
% 5.79/2.01  % (2853482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.79/2.01  % (2853482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/2.01  % (2853482)CaDiCaL version: 2.1.3
% 5.79/2.01  % (2853482)Termination reason: Instruction limit
% 5.79/2.01  % (2853482)Termination phase: Saturation
% 5.79/2.01  % (2853482)Time elapsed: 0.171 s
% 5.79/2.01  % (2853482)Peak memory usage: 96 MB
% 5.79/2.01  % (2853482)Instructions burned: 318 (million)
% 5.79/2.01  % (2853486)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=2703285128:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2990 on theBenchmark for (2990ds/2836Mi)
% 5.79/2.01  % SZS status Satisfiable for theBenchmark
% 5.79/2.01  % SZS output start Saturation.
% See solution above
% 8.42/2.11  % SZS output start Definitions and Model Updates.
% 8.42/2.11  for all inputs,
% 8.42/2.11      define ir(X0) := true
% 8.42/2.11  % SZS output end Definitions and Model Updates.
% 8.42/2.11  % (2853463)------------------------------
% 8.42/2.11  % (2853463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.42/2.11  % (2853463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/2.11  % (2853463)CaDiCaL version: 2.1.3
% 8.42/2.11  % (2853463)Termination reason: Satisfiable
% 8.42/2.11  % (2853463)Time elapsed: 0.838 s
% 8.42/2.11  % (2853463)Peak memory usage: 141 MB
% 8.42/2.11  % (2853463)Instructions burned: 2429 (million)
% 8.42/2.11  % (2853463)------------------------------
% 8.42/2.11  % (2853463)------------------------------
% 8.42/2.11  % (2853457)Success in time 1.126 s
% 8.42/2.11  % Vampire exiting
%------------------------------------------------------------------------------